[tcoratger]

The agreement theorem of eth_simulateV1 no longer assumes that the block passes the checks against its parent.
A new theorem proves those checks from facts about the parent, the fork, the time and the size of the block.

Closes #2108.

The problem

The agreement theorem, stateTransition_of_simulateBlock, said that a simulated block with validation and no overrides passes the state transition once its calls are signed.
It took as a hypothesis that the signed block passes checkBlock, the checks of a block alone and against its parent.
The simulated header is built to pass those checks, so the hypothesis hid part of the claim; the audit of #2512 marked it MAJOR.

The idea

checkBlock_simulateBlock proves checkBlock for the signed block.
It unfolds the simulated header and checks each rule of checkHeader_eq_ok_iff:

• the parent hash, the base fee, the gas limit and the excess blob gas come from the parent, as the header builder sets them;
• the difficulty, the nonce and the ommers hash are fixed from Paris, and the extra data is empty;
• the gas used fits the gas limit, because each call passed the gas check of its block.

What the header alone cannot give stays a hypothesis, each a fact about a real chain:

• the parent is the last block of the chain, from London on, at a fork no later than the block's;
• the block is from Paris on, one number above its parent, later in time, and its time fits 256 bits;
• the parent's gas limit is at least 5,000, the least that the gas limit rule allows;
• the parent's excess blob gas and blob gas used add up to less than 2^64, so the header's 64-bit field holds the expected value;
• the signed block fits the size limit, which the signatures change.

The agreement theorem now takes these hypotheses in place of the checks.

before: ... (hCheck : checkBlock chain.config false chain.recent (b.withTransactions txs root) = .ok ())
after:  ... (hParent : chain.recent.getLast? = some parent) (hLondon : .london ≤ parent.fork)
            (hParentFork : parent.fork ≤ fork) (hParis : .paris ≤ fork)
            (hNumber : number = parent.header.number + 1)
            (hTime : parent.header.timestamp.toNat < time) (hTimeBits : time < 2 ^ 256)
            (hGasLimit : LIMIT_MINIMUM ≤ parent.header.gasLimit)
            (hExcess : parentExcessBlobGas parent.header + parentBlobGasUsed parent.header < 2 ^ 64)
            (hSize : (do validateBlockSize (← bodyItems (b.withTransactions txs root))) = .ok ())

Example

A simulation on Mainnet after Prague, on top of a head at number 100 with a gas limit of 36,000,000:

• the simulated block has number 101, the head's hash as parent hash, and the head's gas limit;
• its base fee and excess blob gas are those that the head gives, and its difficulty and nonce are 0;
• every hypothesis holds, so checkBlock passes and the transition gives the state of the simulated block.

For reviewers

• Before Paris, the simulated difficulty is that of the base block, which the difficulty rule need not accept, so the theorem starts at Paris.
• The gas bound reads the run of the simulated calls, not the signed run, since the header carries the gas of the simulation.
• The excess blob gas hypothesis is stronger than the exact need, that the expected excess fits 64 bits; it is kept for readability.
• SOUNDNESS.md lists the new hypotheses and drops the line that the checks stay a hypothesis.

Checks

• lake build --wfail EthLib.Execution.Proofs.Rpc: passes (1727 jobs).
• lake env leanchecker EthLib.Execution.Proofs.Rpc.SimulateBlocks: passes.
• scripts/soundness_facts.py --check, scripts/check_lean_layout.py --base upstream/master, scripts/check_layers.py, lake exe check-accessors: pass.
• A FULL statement audit found no CRITICAL or MAJOR finding; its wording findings and those of a docs review are applied.

🤖 Generated with Claude Code