Lean verification of EIP-7002: system-call success and FIFO requests

What it is

A post on ethresear.ch reporting two Lean 4 theorems about the deployed 504-byte EIP-7002 contract at 0x00000961Ef480Eb55e80D19ad83579A64c007002, plus two machine-checked counterexamples. The statements are checked against Jaune, an executable EVM and block-processing semantics in Lean, for Prague, Osaka, BPO1 and BPO2. They use only Lean's standard three axioms (propext, Classical.choice, Quot.sound). The results are pinned to Blanc 7954405c, Jaune ff22ec80 and Lean v4.35.0.

How it works

• Totality (checked_system_totality): with the canonical code installed, the end-of-block system call returns .ok whatever the storage holds. Gas is computed exactly and is at most 210,000 of the 30,000,000 given. A companion theorem, history_canonical_code, shows valid histories keep the canonical code.
• FIFO (history_fifo): submissions history = emissions history ++ remainingQueue history. Submissions include calls from inside transactions, if committed. The equation respects order and multiplicity.
• Service and delivery: each block emits the first min(16, queue length) entries. An entry at zero-based position q is emitted floor(q/16) blocks after the block that computes it, and later submissions cannot delay it. This is conditional on blocks being produced.

Preconditions / Affected

The FIFO proof starts from the canonical Cancun deployment and assumes:

• No block transaction is sent from the system address 0xfffffffffffffffffffffffffffffffffffffffe, no EIP-7702 authorization is signed by it, and no contract creation runs at it, even a reverting one.
• The system address has no code right after deployment. This is the one starting fact the proof cannot derive.
• The other three system contracts (EIP-2935, EIP-4788, EIP-7251) hold canonical code at activation.
• Each block's balances plus incoming consensus-layer withdrawal credits sum to less than 2^256 wei, and there are at most 2^254 committed submissions.

flowchart TD
    A[Code at system address] --> B[User tx triggers it]
    B --> C[It calls EIP-7002]
    C --> D[Caller matches system call]
    D --> E[Queue drained before real call]

Caveats

• Drain counterexample: code at the system address, triggered by a user transaction, makes EIP-7002 treat the call as the system call and drain the queue early. It does not start from a canonical deployment, and the post does not claim mainnet can reach it. The post's own check at block 22,431,083 (last block before Prague), via three RPC providers, found the system address had no code. These are not authenticated state proofs.
• Fee gap: the bytecode computes fake_exponential in 256-bit words and its fee never exceeds the EIP's. They are equal exactly when no intermediate value wraps. Blackthorn L-8 and Sigma Prime PEC-03 flagged this before deployment. A three-block synthetic witness has an underpayment at excess 2,893, with 2,895 submissions in one block (gas limit 2^29). Computation outside the proofs shows the fees agree at every excess up to 2,892. Mainnet excess was 666 on 19 December 2025. At 2,893 even the lower fee is about 3.2×10^55 ETH, so no real account could pay it. The FIFO results therefore refer to the bytecode's fee, not the EIP's.
• Scope: nothing on Amsterdam or later forks, consensus-layer handling of requests, fee economics, storage growth, transaction inclusion, or the EIP-7251 contract.
• Trust base: results carry to mainnet only as far as Jaune matches clients. Jaune passes all 4,968 files of its manifest in the execution-specs tests@v21.0.1 fixture lane. The axiom audit cannot show the statements capture the intended protocol properties.
• Authorship: AI agents wrote the proofs and statements under the author's direction. The author asks for corrections on the three list definitions, the assumptions and the mainnet link, and for any route to system-address code the premises miss.

The related paper arXiv:2610.19764v1 covers this contract on an older snapshot (Blanc 5048a51f, Jaune 2737c8eb, Lean v4.34.0). Its verification package is Zenodo DOI 10.5281/zenodo.23351349.