BeaconDeposit.

Every hash in the contract is a STATICCALL to address 0x2 with a 64-byte input and a 32-byte window — twelve source-shaped sites, all retained. The proofs take the frame’s fork to be a covered one — Prague, Osaka, BPO1, or BPO2, never Amsterdam — name its precompile selection and the absence of a delegation designator at 0x2, prove the 64-byte child input, and instantiate the answer as exactly Bytes.sha256 input: environment facts, not a hash axiom. A failed call bubbles the child’s returndata byte for byte; a short success empty-reverts — both arms as the pinned solc wrapper does. The SHA-256 named here is Jaune’s, itself proved equal to a FIPS 180-4 transcription in the sibling — a strengthening no beacon statement depends on.

Three bounded walks — the 32-step root fold, the at-most-32-step insertion, the constructor’s 31 zero-hash writes — compile to tail-recursive auxiliary slots at constant stack height. The alternative was measured before it could become architecture: 179 bytes for the first slice against 4,195 unrolled, at indistinguishable elaboration cost, so no unrolled carrier and no resource ceiling was admitted. Every same-frame SSTORE site is classified: a successful deposit commits the count first, then exactly one live branch cell, and construction performs exactly 31 writes.

The decoder is a separate phase before any source guard: the 132-byte head, then, for each of the three tails, an offset and a length below 2³² and a padded tail that fits in calldata. Reordered and overlapping tails are allowed; padding contents and trailing calldata are ignored; every structural failure empty-reverts. Canonical encodings are proved decodable, and the eight guards run in source order — lengths 48/32/96, three value checks, the reconstructed root, the cap — each with the reference’s exact Error(string).

Exact gas identity is not claimed, but gas is observable, so the registry carries seven gas-row families over the committed matrix: deposit success and chained depths, rejection at each of the eight guards, the read-only selectors, dispatch and ABI rejection, precompile resource edges, construction, and the BPO2 lane. Every row is non-positive for Blanc, which is why no BD-GAS deviation row exists — the empty list is measured, not inferred from an aggregate.

Declared exclusions, load-bearing: no verification of the deployed reference, which is executed only as the finite oracle; no universal equivalence, gas parity, or liveness; no raw identity of source, dispatcher, bytes, code hash, slots, or storage root. The deployment root and open history are proved for one direct singleton shape and the Prague-only schedule, under the admission the results section states — nothing wider.

The constructor’s win is required to hold with the code deposit removed, so that a smaller deposited runtime cannot mask a dearer constructor — and it does, by 26,172 gas in both lanes. What is committed is the finite vector above, every boundary digest-pinned with falsifiers that must keep failing. Universal gas dominance is not claimed; exact parity with the deployed original is a declared freedom, not a goal.

These are measurements against the pinned Prague EELS and the pinned BPO2 target, and the page labels them as such rather than promoting them. Nothing here implies deployability or cost on any other fork, and nothing here is a statement about the artifact at 0x0000…05Fa.

The port’s first decision was made with a stopwatch. Two prototypes of the root fold — one tail-recursive loop slot with a shared continuation, one 32-way source-generated unroll — were compiled by the real compiler under an exclusive host hold: 179 bytes against 4,195, at indistinguishable wall time and memory. An unrolled artifact would have needed a carrier abstraction from the very first proof so that concrete internals never rode through a 32-copy walk; the loop needed one invariant and one reusable SHA-call boundary. The record is committed as BEACON_DEPOSIT_COST.md, and later proof work may split invariants but may not quietly replace the loops.

The open-history theorem was contracted as unconditional preservation and turned out to be false in that form — type-4 delegation at address 0x2 is real EVM. The repair was not a quieter statement but a louder one: contract-neutral trace admission over actual executions and retained frames, with fresh entry and native SHA as positive evidence at the admitted roots, re-priced with the user rather than slipped in. The same machinery is now shared, and static-child storage preservation is proved generically. A premise a theorem cannot do without should be visible in its statement, its register row, and the page that quotes it.