The Beacon deposit contract.

Safety, after any history

Exactly the deposits made.

From a checkpoint at which the contract’s storage is the accumulator of some list of deposits, after any configured history the storage is the accumulator of that list followed by exactly the deposits whose frames were committed, in order. Rolled-back deposits are filtered out by settlement; nothing is added and nothing is lost. For a fresh deployment the initial list is empty.

theorem configuredHistory_solInv_sys {ca : Adr} {cfg : ChainConfig}
    {checkpoint future : BlockChain} {initialHistory : List B256}
    (trace : ConfiguredHistoryTrace cfg checkpoint future)
    (systemInstalled : SystemCodeInstalled checkpoint.state)
    (systemNoAuthority : ∀ p ∈ systemContracts, trace.NoAuthorityAt p.1)
    (systemNoFrame : ∀ p ∈ systemContracts, ∀ root ∈ trace.rawFrames,
      root.sevm.codeAddress = none → root.sevm.currentTarget ≠ p.1)
    (checkpointEmpty : checkpoint.state.getCode 2 = ByteArray.empty)
    (noAuthority : trace.NoAuthorityAt 2)
    (noFrame : ∀ root ∈ trace.rawFrames, root.sevm.codeAddress = none →
      root.sevm.currentTarget ≠ 2)
    (installed : checkpoint.state.getCode ca = code)
    (invariant : SolInv (checkpoint.state.getStor ca) initialHistory) :
    SolInv (future.state.getStor ca) (initialHistory ++ committedNodes ca trace)

Read the hypotheses. Two concern the contract — its code is installed and its storage accumulates initialHistory. The rest concern the environment it runs in, and every one is trace-local and finite: the four system contracts the protocol calls at every block hold their canonical code at the checkpoint; the SHA-256 precompile’s address, 0x02, holds no code there; and no transaction in the history carries an EIP-7702 authorization signed by any of those five addresses, nor does any creation target one. There is no hash premise at all: the layout is fixed, and the tree uses SHA-256.

Two companions read the count and the root off the same list: the count slot holds its length, which stays below 2³², and the contract’s root is the reference mixed Merkle root of the list (configuredHistory_count_sys, configuredHistory_root_sys).

An algorithm, proved once

The root, for every hash function.

The contract does not store its tree: it keeps a branch of 32 nodes and recomputes the root on demand. Blanc proves that this incremental algorithm computes the recursively defined depth-32 Merkle root, with the count mixed in, from any state satisfying its invariant — for every hash function H:

theorem root_correct (H : Bytes → B256) (s : Acc) (ls : List B256)
    (hInv : Inv H s ls) : Acc.root H s = mixedRootOf H ls

The history theorems instantiate H as the SHA-256 that Jaune executes for the precompile at address 0x02, which the bytecode calls. Jaune proves its optimized SHA-256 equal, on every input, to a transcription of NIST FIPS 180-4; that theorem lives in a Jaune module outside the Blanc library’s import closure, so Blanc’s axiom walk does not cover it.

Blanc.BeaconDeposit.root_correct · BeaconDepositCorrectness.lean:284

Constructed executions

A deposit, at exact gas.

After any configured history, a deposit the model accepts at the final storage — given calldata the deployed decoder accepts — executes from a fresh frame at exactly G + 656 + its body’s cost and leaves exactly G; it ends in the model’s accumulator, extends the list by exactly the new deposit-data node, changes no other account’s storage, and emits exactly the model’s DepositEvent (configuredHistory_deposit_live). The body’s cost is 14,551 plus the actual charges of reading and storing the count and of the tree insertion, whose terms depend on the deposit’s position in the tree.

The views succeed too, at exact gas: get_deposit_count costs 1,514 warm and 3,514 cold, get_deposit_root an exact cost, and supportsInterface answers true exactly for the ERC-165 and deposit interface ids. The liveness and view theorems take an entry condition at every frame the history entered at the contract: the SHA-256 precompile’s address is warm and holds no delegation. Every precompile is warm from the start of a transaction, so inside a transaction it always holds.

Statements that can fail

A premise found false, and its replacement.

An earlier family of deposit-contract statements in the repository assumed that no system contract’s code contains a call- or create-type instruction byte at any offset. That premise is false on mainnet: the canonical EIP-7002 contract carries such bytes inside its push data, at offsets 67, 123, 128 and 141, and Blanc proves the premise false of that code from the first of them (withdrawalRequestCode_not_spawnFree). The statements above replace it with the premise that the canonical code is installed — and at block 26,141,229, three providers report that mainnet’s four system contracts held exactly that code, and that the SHA-256 precompile’s address held none.

It is the kind of defect that only reading a statement against the chain can catch, and the reason the statements here are written to be read.

Where a history can start

Deployment.

Under every covered fork, the recorded creation input, run as a CREATE from the recorded deployer at nonce 0, installs the certified runtime at the contract’s mainnet address — the kernel evaluates the address from the deployer and nonce — and leaves storage that accumulates the empty list, with no hash premise (beacon_deploy_covered). It is a modeled deployment: it does not prove that the 2020 transaction was included.

Stated, so it is not inferred

Not claimed.

• That today’s storage accumulates the deposits mainnet saw: the contract’s DepositEvent logs rebuild the list of all 2,565,727 deposits, whose recomputed accumulator must match the branch slots and count in storage — a finite check that has not been run.
• Anything about revert routes and their payloads, or about the BLS validity of deposit data.
• Transaction-level liveness: a deposit carries value, which needs a value-carrying transaction envelope.
• Since EIP-6110 the beacon chain consumes the stream of DepositEvent logs; about logs there are single-call statements only.

The claim map’s deposit-contract section lists every theorem with its premises, file and line.

Context

Earlier work, and Blanc’s own deposit contract.

Park, Zhang and Roșu verified the contract’s original Vyper version in K, and then a solc 0.6.8 build of its Solidity rewrite with per-function gas bounds; the deployed bytes were compiled by solc 0.6.11. Cassez verified the incremental Merkle tree algorithm in Dafny.

Blanc also contains a reimplementation of the deposit contract in its own language, proved over its own compiled bytes and tested beside the deployed runtime — the same 6,358 bytes the theorems above are about. More on Blanc’s deposit contract.