evm-asm: Instructions file for Codex

AI Agent Guide for EvmAsm

Guidance for AI agents working on the EvmAsm project. This page is the compact router: non-negotiable rules + where to find everything else. Deep material is in docs/agents/ — load a deep page only when its trigger applies.

What this project is (and where it's going)

EvmAsm is a verified macro assembler for RISC-V in Lean 4 (in the lineage of "Coq: The world's best macro assembler?", Kennedy et al., PPDP 2013), applied to one goal: a formally verified zkEVM stateless guest. The guest (stateless_guest, run under the ZisK zkVM / ziskemu) validates an Ethereum execution payload against a witness; the north-star theorem is run_stateless_guest_spec (EvmAsm/Stateless/EntrySpec.lean) — the emitted guest's output is correct per the SpecRef port of execution-specs' run_stateless_guest.

Two layers, with a CI-enforced boundary (check-layering.sh):

• The verified core (EvmAsm/ except Codegen//Tests//Examples/): machine model, separation logic, proofs, the executable spec ports. The core must NEVER import Codegen.
• EvmAsm/Codegen/: the unverified-but-emitted guest (asm strings, emission, region maps, probes) that the verification is progressively replacing routine-by-routine. Verified ↔ emitted correspondence is tied by byte-identity _eq_prog drift guards or full re-emit gates (EEST A/B) — see docs/agents/verified-replacement-strategy.md.

The center of gravity is the evm-asm-4ch8f epic ("replace every guest routine with a verified triple"). The per-opcode Evm64 track that built this substrate is largely complete (52 opcodes, kernel-checked registry in EvmAsm/Progress.lean); most new work is porting guest routines, in callee-first order, against the separation-logic state-assertion vocabulary.

Start here

1. What to work on: the in-repo sources are PLAN.md (roadmap; see CLAUDE.md for its maintenance protocol) and docs/agents/top-theorem-ledger.md (what remains for the north star). Work items are coordinated in an external issue tracker ("beads", ids like evm-asm-4ch8f.75.1) that most agents do NOT have access to — treat bead ids appearing in docs/PRs as opaque work-item references; if your session does have the tracker, use it, otherwise your task assignment supersedes.
2. Starting any 4ch8f bead → docs/agents/roadmap-4ch8f.md (layer DAG, pick-next rules, recipe table).
3. Verifying one routine → docs/agents/port-playbook.md (mechanics) + docs/agents/verified-replacement-strategy.md (what to prove, spec shape, what to do when a callee doesn't expose enough); sp-frame routines (stack frame + callee-saved regs, loops, cross-calls) → docs/porting-sp-frame-routines.md (FramePort tactics, tiered recipe).
4. What remains for the north star → docs/agents/top-theorem-ledger.md.
5. Reviewing a PR → docs/agents/review-playbook.md.
6. Live progress cockpit (GitHub Pages) → https://verified-zkevm.github.io/evm-asm/ (docs/index.html). Do not hand-edit counts into the HTML; there are none. Merge to main republishes. If you changed a Progress registry, regenerate DRIFT.md only (scripts/drift-report.sh --write).