Imported from leonardoalt/evm-smith (AGENTS.md). Install upstream with npx skills add leonardoalt/evm-smith. Copyright stays with the author.

For AI agents

This file orients an AI coding agent (Claude, Cursor, Aider, Copilot, etc.) working in this repo. Humans should read README.md first — it has the full story.

TL;DR

EVM-Smith is a Lean 4 framework for writing EVM bytecode as data and proving safety properties about it against the upstream semantics in NethermindEth/EVMYulLean. The intended workflow is: AI writes a bytecode program → AI writes a Lean proof of its correctness → lake build verifies both.

Where to look

• README.md — human-oriented documentation: what the project is, how to build, what's already proved, the limitations.
• .claude/skills/ — task-oriented playbooks. Use these when you're about to do one of the named tasks; each contains a skeleton, templates, and common pitfalls.
• EvmSmith/Framework.lean — the runtime surface (mkState, runOp, runSeq, Program).
• EvmSmith/Lemmas.lean — the proof-time surface (per-opcode step lemmas, runSeq_cons_ok fusion). Read the header comment for why this file exists and why it isn't yet upstream.
• EvmSmith/Demos/Add3/ — the canonical arithmetic worked example. Copy its shape when adding a new program. Contains Program.lean, Proofs.lean, DumpBytecode.lean (emits hex for Foundry), and foundry/ (a Foundry test suite that loads the runtime bytecode via vm.etch and exercises it with raw calldata).
• EvmSmith/Demos/Register/ — a storage-using worked example: storage[msg.sender] = x followed by a value-0 CALL to msg.sender, exposing reentrancy. Exercises CALLER/SSTORE/CALL/POP/STOP. Headline cross-transaction result: BalanceMono.lean :: register_balance_mono — Register's balance is non-decreasing across any single Ethereum transaction, under arbitrary reentrancy, sorry-free. Proof composes a per-PC bytecode walk in BytecodeFrame.lean with the EVMYulLean frame library (see "Frame library" below). End-to-end walkthrough: BALANCE_MONOTONICITY.md.
• EvmSmith/Demos/Weth/ — a wrapped-ETH token contract in raw bytecode. Function dispatch via 4-byte selectors, JUMP/JUMPI/JUMPDEST control flow, SSTORE state-update before CALL (checks-effects-interactions). 86 bytes of runtime. The cross-transaction solvency invariant is proved in Solvency.lean :: weth_solvency_invariant — Σ storage[sender] ≤ contract.balance after any single Ethereum transaction, under arbitrary reentrancy, conditional on a 5-field WethAssumptions bundle of structural facts (see REPORT_WETH.md). Foundry suite (15 tests, including invariant runs and an explicit reentrancy test) lives in Weth/foundry/.

Frame library — for proving cross-transaction / reentrancy-resistant invariants

If your contract needs to maintain a per-account invariant across an entire Ethereum transaction (Υ), through nested CALL / CREATE / SELFDESTRUCT and arbitrary reentrancy, the proof goes through the Frame library in EVMYulLean/EvmYul/Frame/ (closed in this repo's branch of EVMYulLean — see EVMYulLean/FRAME_LIBRARY.md for the overview).

The consumer entry point is ΞPreservesAtC_of_Reachable: you supply a contract-specific Reachable : EVM.State → Prop predicate that captures your bytecode trace, plus six closure obligations, and you get the per-bytecode ΞPreservesAtC C witness that feeds Υ_balanceOf_ge (the transaction-level frame).

Three reusable building blocks:

• StepShapes.lean — for each opcode, a single-step lemma describing the post-state's pc, stack, executionEnv shape after EVM.step. Coverage spans pushes, arithmetic primops, DUP/SWAP, control flow, copy ops, environment readers, and CALL.
• PcWalk.lean — step_OP_at_pc lemmas combining decode-bytecode extraction with the matching shape, so each PC case in a contract walk compresses to one tactic invocation.
• MutualFrame.lean — Θ_balanceOf_ge, Λ_balanceOf_ge, Ξ_balanceOf_ge_bundled, the joint mutual closure. Don't dive in unless you need to extend the bundle's outputs.

The proof pattern is documented in /prove-balance-invariant and demonstrated end-to-end by EvmSmith/Demos/Register/BalanceMono.lean (balance monotonicity) and EvmSmith/Demos/Weth/Solvency.lean (relative invariant under non-zero outbound CALL).

Skills

Constraints an agent should know

• EVMYulLean/ is a git submodule pointing at leonardoalt/EVMYulLean, a working fork of the NethermindEth upstream that carries the Frame library. The NethermindEth upstream alone won't satisfy the imports. When extending the framework — new step shapes, new closure-frame conjuncts, bytecode-walk machinery — modifications belong there. Use git -C EVMYulLean ... for git ops; commit and push inside the submodule, then bump the submodule pointer in this repo (one parent commit per pinned-version change). The local checkout has origin = leonardoalt/EVMYulLean and (by convention) upstream = NethermindEth/EVMYulLean for fetching upstream changes.
• Do not commit .lake/. Build artifacts.
• Byte-level round-trips are not provable. ffi.ByteArray.zeroes is opaque; any proof that depends on reading back bytes through ByteArray.write won't close. State properties at the stack / storage level instead. See the debug-proof skill for the full workaround.
• Namespace convention: the Lean namespace for a new program called <Name> is EvmSmith.<Name>, and its correctness namespace is EvmSmith.<Name>Proofs. The file path may live under EvmSmith/Demos/<Name>/ for organisational reasons; this intentional mismatch is acceptable (see EvmSmith/Demos/Add3/).
• Keep EvmSmith/Framework.lean minimal. It's the user-facing runtime API; don't accumulate helpers there. Proof-only utilities go in EvmSmith/Lemmas.lean; program-specific code goes under EvmSmith/Demos/<Name>/.

Build / verify / run

# First-time setup (skip if you cloned with --recursive):
git submodule update --init --recursive        # pulls EVMYulLean + forge-std

# Verify all proofs + tests (10-30min cold, seconds incremental):
lake build

# Run the IO demos end-to-end (Add3 + Register + Weth):
lake exe evm-smith

# Run any demo's Foundry suite (requires Foundry ≥ 1.0 on PATH):
cd EvmSmith/Demos/Add3/foundry      && forge test
cd EvmSmith/Demos/Register/foundry  && forge test
cd EvmSmith/Demos/Weth/foundry      && forge test

See README.md → "Requirements" and "Building" for the full prerequisites.

If you're about to do something big

If the task is more than a small, local change — e.g. refactoring Framework.lean, changing the proof strategy in Lemmas.lean, adding a new subdirectory structure — pause and check in with the human first. The existing design has specific justifications that are documented in-file (read the header docstrings of Framework.lean and Lemmas.lean). Don't silently rework them.