# evm-asm progress

> Snapshot: `2026-06-18` @ [`0ea3f6d81`](https://github.com/Verified-zkEVM/evm-asm/commit/0ea3f6d81299121a7d5555887dfe7f268c5e69cd)
> Lean toolchain: `leanprover/lean4:v4.30.0-rc1`
> Pinned submodules: `eth-act/zkvm-standards@05d98e4`, `ethereum/execution-specs@a0c1826`
> Regenerated by [`scripts/progress-report.sh`](scripts/progress-report.sh) from the kernel-checked
> registry in [`EvmAsm/Progress.lean`](EvmAsm/Progress.lean). `scripts/check-progress.sh` runs
> in CI and fails the build if this file drifts from the regenerated output.

<!--
  Hand-written prose interpolated by scripts/progress-report.sh.
  Edit this file to refresh narrative sections without touching the
  shell script. The kernel-checked, registry-driven tables are
  emitted by `lake exe progress-report`; everything below is
  reviewer-maintained.
-->

## Role in the L1-zkEVM stack

evm-asm is a **verified guest program core** for Ethereum L1 zero-knowledge
provers. The wider L1 zkEVM ecosystem layers are:

```
┌──────────────────────────────────────────────────────────────────┐
│  Block + execution witness  (EEST fixtures, real-chain RPC)      │
└──────────────────────────────────────────────────────────────────┘
                              │  read_input
┌──────────────────────────────────────────────────────────────────┐
│  Guest program (a stateless block validator ELF)                 │
│  - reth, ethrex, …  ← compiled from a Rust EL client             │
│  - evm-asm          ← built bottom-up from verified RV64         │
└──────────────────────────────────────────────────────────────────┘
                              │  riscv64im_zicclsm-unknown-none-elf
┌──────────────────────────────────────────────────────────────────┐
│  zkVM (Airbender / OpenVM / Risc0 / SP1 / Zisk / …)              │
│  - ere : unified host API                                        │
│  - zkvm-standards : RISC-V target + IO + accelerators + halt     │
└──────────────────────────────────────────────────────────────────┘
                              │  write_output
                              ▼
                        Post-state root
```

External anchors:

- **[`eth-act/zkvm-standards`](https://github.com/eth-act/zkvm-standards)** —
  RISC-V target, IO interface, accelerator C ABI, memory layout, termination
  semantics. evm-asm targets every published clause; current state in axis E below.
- **[`eth-act/ere`](https://github.com/eth-act/ere)** — unified Rust host API
  abstracting Airbender / OpenVM / Risc0 / SP1 / Zisk under one
  `Compiler` / `zkVMProver` / `zkVMVerifier` interface. evm-asm aims to ship as
  a sibling to the existing [`ere-guests`](https://github.com/eth-act/ere-guests)
  `stateless-validator-*` binaries.
- **[`eth-act/zkevm-benchmark-workload`](https://github.com/eth-act/zkevm-benchmark-workload)** —
  fixture-driven benchmark harness (EEST + RPC + raw-input). evm-asm's eventual
  metrics (cycles, proof size, proving/verification time) belong here.
- **[`zkevm.ethereum.foundation/blog/benchmarking-zkvms`](https://zkevm.ethereum.foundation/blog/benchmarking-zkvms)** —
  motivation for the 2026 L1-zkEVM roadmap: real-time proving, multi-zkVM
  redundancy, formal-verification leg.

## What "evm-asm is a complete guest program" means

A guest program for L1 stateless block validation must satisfy nine
obligations. The per-obligation status and the opcodes/infrastructure blocking
each one are tracked in the **kernel-checked obligation matrix** rendered below
(see the *Guest-program obligations* section) — source of truth and counts live
in [`EvmAsm/Progress/Obligations.lean`](EvmAsm/Progress/Obligations.lean), and a
fuller "what is NOT proven" ledger lives in [`DRIFT.md`](DRIFT.md).

## Axes the dashboard below tracks

| Axis | What it measures |
|---|---|
| A | **Verification depth** — kernel invariants + per-opcode proof tier |
| B | **Verification breadth** — bridges, conformance, simulation reach |
| C | **Cost surrogate** — per-opcode `cpsTripleWithin N` cycle bound (a verified gas-cost proxy) |
| D | **End-to-end runnability** — codegen registry, ziskemu round-trips, milestones |
| E | **zkvm-standards conformance** — clause-by-clause |
| F | **execution-specs conformance** — fork, reference-link audit, EEST/RPC pass rate |
| G | **Trust base** — Sail tie, dependency pins, axiom count, unverified codegen gap |
| H | **Process / CI** — guardrails, benchmark history |

Axes A.2, B.5, C.1, D are emitted from `lake exe progress-report` plus the
shell wrapper. Axes E, F, G are maintained below; refresh in this template
when the underlying state changes.

### Proof-tier rubric (axis A.2)

The per-opcode coverage table classifies each opcode by a kernel-checked
`ProofTier` in [`EvmAsm/Progress.lean`](EvmAsm/Progress.lean). The tiers
separate a *complete spec on a restricted input domain* from *half-built work*
— conflating the two is the statement-vacuity blind spot this dashboard exists
to surface (the DIV `b.getLimbN 3 = 0` trap).

| Tier | Meaning |
|---|---|
| ✅ proven | Complete top-level Hoare triple specifying the opcode's full effect, with **no** input-domain precondition. |
| 🔶 conditional | Complete top-level triple, but **gated by a nonvacuous input-domain precondition** that excludes a real input region (DIV/MOD `b.getLimbN 3 = 0`; SDIV `hStack`). Distinct from proven (no restriction) and partial (no complete triple). |
| 🟡 partial | **No** complete triple yet — only an `EvmWord.<op>_correct` lemma, a preamble/partial-effect spec, or a sub-component. |
| ⏳ execSpec | Executable-spec / handler / bridge semantics only; no RV64 subroutine produces the EVM result. |
| ✗ notStarted | Not represented in `EvmOpcode` yet (e.g. unimplemented EIPs). |

A single-point restriction (ADDMOD's `b=0`-only triple, PUSH2..32's
zero-slot-only triple) stays 🟡 partial, not 🔶 conditional. The `Cycles (N)`
column is the typed `cpsTripleWithin N` step bound (cost surrogate); see C.1.

## E — zkvm-standards conformance

| Standard clause | Status |
|---|---|
| `riscv-target` (`riscv64im_zicclsm-unknown-none-elf`) | 🟡 substrate matches; emitter still uses `rv64imac` (track in [#TBD](.)) |
| `io-interface` (`read_input` / `write_output`) | ✅ verified specs + codegen M4 |
| `c-interface-accelerators` (`zkvm_accelerators.h`) | 🟡 header vendored; per-precompile bridges Lean-only |
| `memory-layout-restrictions` | ✅ codegen uses vendor linker conventions (`-Ttext=0x80000000 -Tdata=0xa0000000`) |
| `standard-termination-semantics` | ✅ `--halt linux93` default, ADR landed |

## F — execution-specs conformance

| Aspect | Status |
|---|---|
| Reference fork | Frontier/Shanghai (most opcodes); Amsterdam draft fork referenced for SDIV/SMOD |
| Pin | `ethereum/execution-specs@ec23140` (gitlink in `.gitmodules`) |
| Per-opcode reference-link audit | manual; `EvmWord.<op>` defs cite Python files in their docstrings (not yet machine-checked) |
| EEST fixture pass rate | ✗ harness not yet wired (parking-lot dependency on D obligations 3 + 4) |
| RPC block replay | ✗ not started |

## G — Trust base

| Component | State |
|---|---|
| RV64 instruction semantics tie | `Rv64/SailEquiv/` references the official Sail RISC-V model via the `dhsorens/sail-riscv-lean` fork (`lakefile.toml`) |
| Mathlib pin | `lake-manifest.json` (refreshed alongside Lean nightly) |
| Lean toolchain pin | `lean-toolchain` (Lean 4 nightly) |
| Kernel additions | 0 literal `axiom`, 0 `sorry`. Both TCB-expanding tactics are forbidden and fully eliminated (`native_decide` 206→0, `bv_decide` 290→0), so the trusted base is only the three classical axioms (`propext`, `Classical.choice`, `Quot.sound`); the `scripts/axiom-allow.txt` burndown list is now empty. Audited by `scripts/check-axioms.sh` (axis A.1) and pre-filtered by `scripts/check-forbidden-tactics.sh`. |
| Codegen verification gap | 🟡 codegen is unverified by design (`CODEGEN.md` §Tricky bits #9). Drift caught by build-time `#guard` round-trip tests in `Codegen/RoundTripTests.lean`. |

## A.1 / H — kernel invariants

| Invariant | Status |
|---|---|
| `sorry` count in `EvmAsm/` | 0 |
| literal `axiom` declarations in `EvmAsm/` | 0 |
| trust axioms in witnessed proofs (kernel `#print axioms`) | `bv_decide` and `native_decide` both forbidden and fully eliminated (trusted base = `propext`, `Classical.choice`, `Quot.sound` only) — 0 pre-existing owner(s) remain in [`scripts/axiom-allow.txt`](scripts/axiom-allow.txt) (burndown → 0), audited by [`scripts/check-axioms.sh`](scripts/check-axioms.sh) |
| Conformance vectors (kernel-checked, `allConformanceVectors_length`) | 66 (floor in [`scripts/conformance-baseline.txt`](scripts/conformance-baseline.txt), gated by `check-conformance-floor.sh`) |
| Build CI guardrails | `check-no-warnings.sh`, `check-unimported.sh`, `check-file-size.sh`, `check-progress.sh`, `check-drift.sh`, `check-axioms.sh`, `check-conformance-floor.sh` |

## Guest-program obligations (kernel-checked)

The nine obligations a complete L1 stateless block-validation guest program must
satisfy, each with the opcodes/infrastructure blocking it. This is the
*direction* axis: opcode-tier counts cannot tell you which obligation is blocked
by what. Source of truth, per-status counts, and the opcode cross-check live in
[`EvmAsm/Progress/Obligations.lean`](EvmAsm/Progress/Obligations.lean)
(`doneCount_eq = 2`, `blockedCount_eq = 6`,
`notStartedCount_eq = 1`, and `blocker_opcodes_in_registry`,
which fails the build if any opcode blocker stops naming a real registry entry).

| Status | Count |
|---|---:|
| ✅ done | 2 |
| 🟡 blocked | 6 |
| ✗ not started | 1 |

| # | Obligation | Status | Blocked by |
|---|---|---|---|
| 1 | RV64 ELF for `riscv64im_zicclsm-unknown-none-elf` | 🟡 blocked | codegen emits `rv64imac` (one extension off `zicclsm`) |
| 2 | `read_input` / `write_output` per the IO interface | ✅ done | Rv64/SyscallSpecs.lean (codegen M4 wired) |
| 3 | RLP-decode the (block, witness) input | 🟡 blocked | RV64 RLP decoder phases 1–3 (in progress) |
| 4 | EVM interpreter loop on the decoded block | 🟡 blocked | codegen M5 (tiny EVM interpreter) not shipped |
| 5 | Full opcode coverage with verified handlers | 🟡 blocked | `MOD`, `SDIV`, `SMOD`, `ADDMOD`, `MULMOD`, `EXP`, `CALLDATACOPY`, `PUSH2..32`, execSpec-tier opcodes have no RV64 subroutine (axis A.2) |
| 6 | Accelerator ECALL bridges per `zkvm_accelerators.h` | 🟡 blocked | per-precompile EL bridges not yet codegen-wired |
| 7 | MPT verification of pre-state witness proofs | ✗ not started | — |
| 8 | Verified post-state root → public output | 🟡 blocked | obligation #4 (interpreter loop), obligation #5 (opcode coverage), obligation #6 (accelerator bridges), obligation #7 (MPT verification) |
| 9 | Halt convention per `standard-termination-semantics` | ✅ done | `--halt linux93` default; docs/host-io-halt-convention.md |


## Verification depth — A.2 opcode coverage

By **registry entry** (parameterized families collapsed; total = 85):

| Tier | Count |
|---|---:|
| ✅ proven      | 42 |
| 🔶 conditional | 2 |
| 🟡 partial     | 6 |
| ⏳ execSpec    | 32 |
| ✗ notStarted   | 3 |


By **opcode byte** (PUSH/DUP/SWAP/LOG families expanded; total = 149):

| Tier | Bytes |
|---|---:|
| ✅ proven      | 72 |
| 🔶 conditional | 2 |
| 🟡 partial     | 36 |
| ⏳ execSpec    | 36 |
| ✗ notStarted   | 3 |


### Per-opcode registry

| Opcode | Tier | Witness theorem | Cycles (N) | Notes |
|---|---|---|---:|---|
| ⏳ STOP | execSpec | `—` | — | executable-spec only; `Termination.lean` + `TerminatingArgs.lean` |
| ✅ ADD | proven | `evm_add_stack_spec_within` | 30 |  |
| ✅ MUL | proven | `evm_mul_stack_spec_within` | 63 |  |
| ✅ SUB | proven | `evm_sub_stack_spec_within` | 30 |  |
| ✅ DIV | proven | `evm_div_stack_spec_unconditional` | — | full-domain unconditional v5 DIV stack spec over divCode_noNop; wraps evm_div_stack_spec_unconditional_v5_div and the v5 lane proofs |
| 🔶 SDIV | conditional | `evm_sdiv_exact_callable_return_stack_spec_within` | — | callable+dispatch shim; evm_sdiv_stack_spec_within conditional on hStack (discharged for divisor=0 and n=1/2/3/n4-call-skip); blocked on DIV/MOD spec-layer migration (bead evm-asm-9iqmw) |
| 🔶 MOD | conditional | `evm_mod_stack_spec` | — | stack spec parametric over ModStackSpecCase (bzero / n=1,2,3, all require b.getLimbN 3 = 0); n=4 path not covered. Executable evm_mod uses divK_div128_v4 (PR #4992). Full-domain unconditional closure tracked by bead evm-asm-9iqmw / gh-61 |
| 🟡 SMOD | partial | `—` | — | smod_correct proven; no top-level Hoare triple |
| 🟡 ADDMOD | partial | `evm_addmod_b0_n0_spec_within` | — | addmod_correct proven; only b=0 stack-spec done |
| 🟡 MULMOD | partial | `—` | — | mulmod_correct proven; no top-level Hoare triple |
| 🟡 EXP | partial | `—` | — | exp_correct proven; program in active development |
| ✅ SIGNEXTEND | proven | `evm_signextend_stack_spec_within` | 28 |  |
| ✅ LT | proven | `evm_lt_stack_spec_within` | 26 |  |
| ✅ GT | proven | `evm_gt_stack_spec_within` | 26 |  |
| ✅ SLT | proven | `evm_slt_stack_spec_within` | 25 |  |
| ✅ SGT | proven | `evm_sgt_stack_spec_within` | 25 |  |
| ✅ EQ | proven | `evm_eq_stack_spec_within` | 21 |  |
| ✅ ISZERO | proven | `evm_iszero_stack_spec_within` | 12 |  |
| ✅ AND | proven | `evm_and_stack_spec_within` | 17 |  |
| ✅ OR | proven | `evm_or_stack_spec_within` | 17 |  |
| ✅ XOR | proven | `evm_xor_stack_spec_within` | 17 |  |
| ✅ NOT | proven | `evm_not_stack_spec_within` | 12 |  |
| ✅ BYTE | proven | `evm_byte_stack_spec_within` | 29 |  |
| ✅ SHL | proven | `evm_shl_stack_spec_within` | 90 |  |
| ✅ SHR | proven | `evm_shr_stack_spec_within` | 90 |  |
| ✅ SAR | proven | `evm_sar_stack_spec_within` | 95 |  |
| ⏳ KECCAK256 | execSpec | `—` | — | delegated to zkvm_keccak256 accelerator; EL/Keccak*Bridge |
| ✅ ADDRESS | proven | `Env.evm_address_stack_spec_within` | — |  |
| ⏳ BALANCE | execSpec | `—` | — | not in EvmOpcode enum yet |
| ✅ ORIGIN | proven | `Env.evm_origin_stack_spec_within` | — |  |
| ✅ CALLER | proven | `Env.evm_caller_stack_spec_within` | — |  |
| ✅ CALLVALUE | proven | `Env.evm_callvalue_stack_spec_within` | — |  |
| ⏳ CALLDATALOAD | execSpec | `—` | — | program in Calldata/LoadProgram.lean; no stack spec yet |
| ✅ CALLDATASIZE | proven | `Calldata.evm_calldatasize_stack_spec_within` | — |  |
| 🟡 CALLDATACOPY | partial | `Calldata.evm_calldatacopy_preamble_stack_spec_within` | — | preamble + partial memory effect; full loop pending |
| ⏳ CODESIZE | execSpec | `—` | — | env read in Code/Basic.lean |
| ⏳ CODECOPY | execSpec | `—` | — | Code/CopyExec.lean + CopyMemory.lean |
| ✅ GASPRICE | proven | `Env.evm_gasprice_stack_spec_within` | — |  |
| ⏳ EXTCODESIZE | execSpec | `—` | — | not in EvmOpcode enum yet |
| ⏳ EXTCODECOPY | execSpec | `—` | — | not in EvmOpcode enum yet |
| ⏳ RETURNDATASIZE | execSpec | `—` | — | ReturnDataHandlers.lean; table dispatch only |
| ⏳ RETURNDATACOPY | execSpec | `—` | — | ReturnData/CopyExec + CopyMemory |
| ⏳ EXTCODEHASH | execSpec | `—` | — | not in EvmOpcode enum yet |
| ⏳ BLOCKHASH | execSpec | `—` | — | env-bridge level |
| ✅ COINBASE | proven | `Env.evm_coinbase_stack_spec_within` | — |  |
| ✅ TIMESTAMP | proven | `Env.evm_timestamp_stack_spec_within` | — |  |
| ✅ NUMBER | proven | `Env.evm_number_stack_spec_within` | — |  |
| ✅ PREVRANDAO | proven | `Env.evm_prevrandao_stack_spec_within` | — |  |
| ✅ GASLIMIT | proven | `Env.evm_gaslimit_stack_spec_within` | — |  |
| ✅ CHAINID | proven | `Env.evm_chainid_stack_spec_within` | — |  |
| ✅ SELFBALANCE | proven | `Env.evm_selfbalance_stack_spec_within` | — |  |
| ✅ BASEFEE | proven | `Env.evm_basefee_stack_spec_within` | — |  |
| ⏳ BLOBHASH | execSpec | `—` | — | env-bridge level |
| ⏳ BLOBBASEFEE | execSpec | `—` | — | env-bridge level |
| ✅ POP | proven | `evm_pop_stack_spec_within` | 1 |  |
| ✅ MLOAD | proven | `evm_mload_stack_spec_within` | — | aligned spec proven; unaligned _public variants in progress |
| ✅ MSTORE | proven | `evm_mstore_stack_spec_within` | — | aligned spec proven; unaligned _public variants in progress |
| ✅ MSTORE8 | proven | `evm_mstore8_stack_spec_within` | 5 |  |
| ⏳ SLOAD | execSpec | `—` | — | Storage*.lean; ECALL → host |
| ⏳ SSTORE | execSpec | `—` | — | Storage*.lean; ECALL → host |
| ⏳ JUMP | execSpec | `—` | — | handled by interpreter PC update |
| ⏳ JUMPI | execSpec | `—` | — | handled by interpreter PC update |
| ⏳ PC | execSpec | `—` | — | reads EVM PC from EvmState |
| ✅ MSIZE | proven | `evm_msize_stack_spec_within` | 6 |  |
| ⏳ GAS | execSpec | `—` | — | reads remaining gas from EvmState |
| ⏳ JUMPDEST | execSpec | `—` | — | no-op opcode; gas-only |
| ✗ TLOAD | notStarted | `—` | — | EIP-1153 (Cancun); not in EvmOpcode enum |
| ✗ TSTORE | notStarted | `—` | — | EIP-1153 (Cancun); not in EvmOpcode enum |
| ✗ MCOPY | notStarted | `—` | — | EIP-5656 (Cancun); not in EvmOpcode enum |
| ✅ PUSH0 | proven | `evm_push0_stack_spec_within` | 5 |  |
| ✅ PUSH1 | proven | `evm_push1_stack_spec_within` | — |  |
| 🟡 PUSH2..32 | partial | `evm_push_zero_slot_full_stack_spec_within` | — | zero-slot only; non-zero-slot path pending; 31 byte-codes |
| ✅ DUP1..16 | proven | `evm_dup_stack_spec_within` | — | single proof generic over n=1..16 |
| ✅ SWAP1..16 | proven | `evm_swap_stack_spec_within` | — | single proof generic over n=1..16 |
| ⏳ LOG0..4 | execSpec | `—` | — | LogArgs + LogDataBridge + LogExecutionBridge; 5 byte-codes |
| ⏳ CREATE | execSpec | `—` | — | Create.lean + CreateAddress + CreateArgsBridge + CreateEffects |
| ⏳ CALL | execSpec | `—` | — | CallArgs + Call*Bridge family |
| ⏳ CALLCODE | execSpec | `—` | — | not in EvmOpcode enum yet |
| ⏳ RETURN | execSpec | `—` | — | TerminatingArgs + TerminatingExecutionBridge |
| ⏳ DELEGATECALL | execSpec | `—` | — | CallArgs kind = .delegatecall |
| ⏳ CREATE2 | execSpec | `—` | — | shared Create family |
| ⏳ STATICCALL | execSpec | `—` | — | CallArgs kind = .staticcall |
| ⏳ REVERT | execSpec | `—` | — | TerminatingArgs |
| ⏳ INVALID | execSpec | `—` | — | TerminatingArgs |
| ⏳ SELFDESTRUCT | execSpec | `—` | — | SelfdestructEffects + terminating bridge |

## C.1 — Per-opcode cycle bounds

Worst-case `cpsTripleWithin N` step bounds are listed inline in the
per-opcode coverage table above (the typed `Cycles (N)` column, sourced
from the kernel-checked `cycleBound` field of `EvmAsm/Progress.lean`).
This is the verified gas-cost surrogate.

## D — Codegen reach

- Programs in `EvmAsm/Codegen/Programs.lean` registry: **972**
- ziskemu round-trip scripts: **730** under `scripts/codegen-*.sh`
- Milestones (CODEGEN.md):

| Milestone | Status |
|---|---|
| M0 | ✅ |
| M1 | ✅ |
| M2 | ✅ |
| M3 | ⏳ |
| M4 | ✅ |
| M5a | ✅ |
| M5b | ✅ |
| M6a | ✅ |
| M6b | ✅ |
| M7 | ✅ |
| M8 | ✅ |
| M8.5 | ✅ |
| M9 | ✅ |
| M10 | ✅ |
| M11 | ✅ |
| M12 | ✅ |
| M13 | ✅ |
| M14 | ✅ |
| M15 | ✅ |
| M16 | ✅ |
| M17 | ✅ |
| M18 | ✅ |
| M19 | ✅ |
| M20 | ✅ |
| M21 | ✅ |
| M22 | ✅ |
| M23 | ✅ |
| M24 | ✅ |
| M25 | ✅ |