[tcoratger]

A block body now keeps, for each transaction, the output of its message and the gas that it used before its refund.
No rule of the block reads them; eth_simulateV1 needs them for the returnData, the revert data and the maxUsedGas of its call results.

Part of #2109.

The problem

Each call result of eth_simulateV1 has a returnData and a maxUsedGas, "Maximum gas used during execution before refunds" in the schema, and a reverted call carries its revert data in its error.
The body of a block threw these away: a transaction's run kept its state, its gas used after the refund, its block gas, its logs and its error, and the body kept only receipts and logs.
The simulation runs its calls through the one body of a real block, so it could not report them without a second run.

The idea

Record the two values where they exist, and carry them out of the body.

• TransactionOutput, what a transaction's run leaves, gets messageOutput, the output of its message, and gasBeforeRefund, the gas used with a refund of 0.
  The second comes from the one formula of the gas used, so from Pectra it is at least the call data floor of EIP-7623, as the fixtures show.
• BodyOutput, what a body gives, gets results: one TransactionResult per transaction, with those two values, oldest first.

Nothing reads the new fields, so every other value that a block computes is unchanged.

New theorems:

• gasUsed_le_gasUsed_zero and runTransaction_gasUsed_le: a refund never raises the gas used, so a run's gas used is at most its gas before the refund, with any precompiles and lifted rules.
• applyTransaction_results: a transaction that enters the body, with or without the overrides of a simulation, adds one receipt and one result, the result of its run.
• applyTransactions_results_length: a body has as many results as receipts.

Example

ethSimulate-precompile-is-sending-transaction.io calls SHA-256 with the input 0x1234, from Glamsterdam.

• Without the floor, it uses 15,000 + 2 × 16 + 72 = 15,104 gas.
• Its call data floor is 15,000 + 16 × 8 = 15,128, so gasBeforeRefund is 15,128 = 0x3b18, the maxUsedGas of the fixture, equal to its gasUsed.

For reviewers

• Existing statements that build these structures change only by the new fields: runTransaction_eq_transactionStart, the initial body output in the statements of Proofs/Blocks/Transition.lean and Proofs/Blocks/Burn.lean, and a proof witness in NoninterferenceRun.lean.
• messageOutput holds the revert data on a revert and, from Byzantium, is empty after any other error; the call results will move the revert data to the error, as the fixtures do.
• From Glamsterdam, a revert puts its state gas back in the reservoir, so the value is taken at the end of the run, not at a peak; no fixture separates the two readings.

Checks

• lake build --wfail EthLib.Execution.Proofs EthLib.Engine.Proofs Exports: passes (6087 jobs).
• lake env leanchecker on the changed proof modules (Proofs.Blocks.Transition, Proofs.Transactions.Process, Proofs.Transactions.NoninterferenceRun, Proofs.Rpc.Call, Proofs.Blocks.Burn): passes.
• scripts/soundness_facts.py --check, scripts/check_lean_layout.py, scripts/check_layers.py, lake exe check-accessors, lake exe gen-bindings --check: pass.
• A FULL statement audit and a spec-fidelity review: the floor of maxUsedGas and the doc of the message output were fixed after them, and a fresh audit found no CRITICAL finding and one MAJOR doc finding, now fixed.

🤖 Generated with Claude Code