# DRIFT β€” trusted base & "what is NOT proven" ledger > **Generated** by `lake exe progress-report drift` from the kernel-checked > registry + obligation tracker in `EvmAsm/Progress.lean` and > `EvmAsm/Progress/Obligations.lean`. `scripts/check-drift.sh` fails the build if > this file drifts from the regenerated output β€” do **not** hand-edit. To > refresh: `scripts/drift-report.sh --write`. This is evm-asm's explicit assumptions / trusted-computing-base ledger, in the spirit of the seL4 and CompCert assumptions lists. The Lean kernel makes every *proven* statement unhackable; this file enumerates what the kernel does **not** cover, so a green dashboard is never mistaken for a fully closed guest program. ## Guest-program obligations (kernel-checked) The ten 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-checks live in [`EvmAsm/Progress/Obligations.lean`](EvmAsm/Progress/Obligations.lean) (`doneCount_eq = 2`, `blockedCount_eq = 8`, `notStartedCount_eq = 0`, plus two cross-checks that fail the build: `blocker_opcodes_in_registry` if an opcode blocker stops naming a real registry entry, and `no_proven_opcode_blockers` if one names an entry that has already reached `.proven`). **Reading the `Audited` column.** A blocker list is a claim about the present. The date + commit records when the row was last checked against the live registries; `β€”` means not since the field was introduced (#11803), so treat that row's blockers as unverified rather than current. | Status | Count | |---|---:| | βœ… done | 2 | | 🟑 blocked | 8 | | βœ— not started | 0 | | # | Obligation | Status | Blocked by | Audited | |---|---|---|---|---| | 1 | RV64 ELF for `riscv64im_zicclsm-unknown-none-elf` | 🟑 blocked | codegen emits `rv64imac` (one extension off `zicclsm`) | 2026-08-10 @372162cc2 | | 2 | `read_input` / `write_output` per the IO interface | βœ… done | Rv64/SyscallSpecs.lean (codegen M4 wired) | β€” | | 3 | RLP-decode the (block, witness) input | 🟑 blocked | `rlp_item_span` is `.conditional` on WalkedSpanForm β€” the zero-triple gap is closed (that issue landed `rlp_item_span_spec_within`), and the OUTER-HEADER half is closed too (its issue closed 2026-08-30 against the rowed encode/size family): `rlp_item_span_long_spec_within` proves the long form for every `lenlen` and `rlp_item_span_any_header_spec_within` dispatches the two arms, so the header form is no longer a restriction. Still uncovered: non-SpanForm walked items, and REJECTION of non-canonical long headers whose payload is below `0x38` (the guest now checks the leading-zero length field but still does not check `payloadLen β‰₯ 56`; the canonical-encoding domain excludes the remaining condition), `rlp_item_size` covers short forms only β€” long string `0xb8`–`0xbf` and long list `0xf8`–`0xff` uncovered (`Correspondence.lean` `rlp_item_size`), nested-list decode bridges: model-side strength mismatch CLOSED by the two-level split β€” `rlpItemDecode` stays the core's lenient span relation and `rlpItemDecodeStrictW` (`Rv64/RLP/WalkNextStrict.lean`) is the wrapper's relation with the recursive payload condition in its list arms, and the reverse bridge (`decodeAux` acceptance β†’ wrapper relation, both arms) is proven there. ⭐ TRANSCRIPTION NO LONGER BLOCKS THIS β€” both programs landed (that issue closed): `rlpWalkNextShared_prog` (`Codegen/Programs/RlpWalk.lean:162`) and `rlpValidatePayload_prog` (`:237`), each with its `_eq_prog` drift guard. ⭐ The machine tie now exists for the NON-LIST half: `rlp_walk_next_shared_nonlist_strict_spec_within` (`Codegen/Programs/RlpWalkNextStrictTie.lean`) is a `cpsTripleWithin` over `rlpWalkNextShared_prog` at `GuestAddrs.rlp_walk_next_shared` (unioned with the proven lenient core) whose post carries `rlpItemDecodeStrictW` as a conclusion; the recursive-payload conjunct is discharged by the wrapper's own prefix load and `bltu t1, 0xc0`, not by a model bridge. STILL OPEN: the LIST arms, i.e. the runs that actually enter `rlp_validate_payload`. The structural cycle is closed by a strict `cycleFuel` mutual witness including the `NestedFuel.done` terminal verified against the linked ELF (`Codegen/Programs/RlpWalkNextStrictFuelModel.lean`); both machine halves are proved under explicit premises; the sole remaining item is a fuel-indexed CPS loop contract for the long-list path at `S+88`, with no usable existing theorem to adapt | 2026-09-02 @closed-blocker-sweep | | 4 | EVM interpreter loop on the decoded block | 🟑 blocked | no simulation bridge from dispatched handlers to the SpecRef interpreter. The one-opcode `h_ADD` pilot's FOUNDATION landed (`Codegen/Proofs/ExecuteSeamBridge.lean`: `guestExec` relation, `add_limb_result_eq_add`) and its issue closed; the one-step simulation itself is NOT claimed there. ⚠️ The representation blocker this entry used to name is CLOSED and must not be re-derived: the handler-lane design work's step 3 landed `dispatchLoopBody_prog` (`Codegen/Dispatch.lean`, sixteen instructions), tied to the SHIPPED dispatcher text by `dispatchLoopFunction_eq_prog` (`rfl`) composed with `emitRuntimeDispatcherLoop_split`, so the loop is no longer a raw String. The per-opcode gas debit is likewise now visible in that Program β€” the `opcode_gas_costs` load, the `env+568` compare, the `sub`/`sd`, and the out-of-gas exit branch (table modelled at `Proofs/OpcodeTables.lean`). ⚠️ The exit label is deliberately NOT spelled in this cell: `scripts/transcription_queue.py` reads every guest symbol named in a `blockedBy` as DEMANDED work at +100 per obligation, so spelling it here would rank a 500-byte exit path nobody is blocked on near the top of the transcription queue. Name symbols here only when they ARE the remaining work. ⚠️ The PAIRING blocker this entry used to name is also CLOSED: the pairing work gave the loop body its own linker label, rebased `dispatchLoopBody_prog` onto it (the Program had been anchored 348 bytes early, at the loop HEAD, behind the code-size stop guard), and registered it in `guestImageEntries`. There IS now a `CodeReq.ofProg` at its linked entry inside `guestImageCodeReq`, and `guestImage_block_sub` lifts a triple stated over it into the image. ⚠️ PART OF the dispatch step is now PROVED and must not be re-derived: the M30 gas debit (prog idx 6..10 β€” the compare, the out-of-gas exit branch, the `sub`/`sd`) is a `cpsBranchWithin 5` at the body's linked entry, lifted into `guestImageCodeReq` and rowed in `Progress/Routines.lean` (`Codegen/Proofs/DispatchStepGas.lean`). ⚠️ The OPCODE half is now ALSO PROVED and must not be re-derived: `Codegen/Proofs/DispatchStepOpcode.lean` carries the fetch and gas-table load (prog idx 0..5), the handler-table load and the indirect `jalr` (prog idx 11..15), and `dispatchStep_body_within` β€” a `cpsBranchWithin 16` over the WHOLE body, indexed by the byte the machine fetched, whose dispatch exit PC is the LOADED handler address. A computed exit needed no new CPS rule (`cpsTripleWithin`'s exit is a term), and the ready-made `execBlock` β†’ CPS bridges could not be reused because their `exposedRegs` currency omits x1 and x20 (`regs_not_exposed_here`). ⚠️ The TABLE-CONTENTS blocker this entry used to name is ALSO CLOSED and must not be re-derived: `.data` is PROGBITS, so the loader copies its bytes in exactly as it does `.text`, and `Codegen/Proofs/GuestDataImage.lean` is the `.data` counterpart of `guestImageCodeReq` β€” it pins both dispatch tables inside that tile (`guestDataScratch`, swapped in for the havoc'd `anyBytes` tile under `guestDataScratch_weakens`, so nothing that only wanted ownership breaks). `dispatchStep_body_shipped` instantiates the whole-body triple at those pinned tables, so for every fetched byte the gas charged and the handler address reached are read out of the shipped image rather than out of two universally quantified lists, and `dispatchStep_body_shipped_controls` is the negative control that the parametric family really did admit a different `.data` image. `opcode_table_contents_not_scratch_determined` survives as the theorem saying why the pin was needed, not as an open gap. β›” THE PIN DID NOT REMOVE A BURDEN, IT MOVED ONE: `guestResidue` carries the same pinned tile, and `guestScratch_eq_window_residue` is an EQUALITY, so the two sides move together and the POST inherits the pin. That is a NEW `.64` obligation β€” the guest must not clobber either table by halt β€” and it is NOT discharged. It is gapped for a structural reason, not an unattempted one: `.64` is `TopComposition.runStatelessGuestSound_of_phases`, which still takes its six phase Props as hypotheses, and the missing fact is run-level (no store lands in the table range) with no whole-program write map to quantify over. `guestResidue_rejects_clobbered_tables` is that obligation as a theorem rather than a docstring β€” a halt heap that zeroed the second gas-table dword provably FAILS the residue β€” and `scripts/check-data-table-residue.sh` is the wired gate bounding the empirical side. ⚠️ That bound is honest but PARTIAL, and the range must NOT be described as shown-unwritten: of 11628 store sites in `.text`, 2785 have a fully constant address (32 of those land in `.data`, all at least 2056 bytes clear of the table range), and 8843 β€” 76% β€” are UNCERTIFIED because their base is unresolvable or is an anchor plus an unbounded runtime term. The gate is wired into `scripts/check-build-parallel.sh`, so the empirical half is enforced rather than recorded. What remains on the machine side is (a) the four side conditions the shipped step still carries, which are about the CODE region the machine fetches from rather than the tables (`hi`, `hbase`, `hover`, `hvalid`), and (b) the handler-side seam. And one iteration of the shipped loop ALSO runs the code-size stop guard, which sits between the head label and the body and is still an unconverted 348-byte span; measured, its HOT path is three instructions and the rest is a halt route needing two callee contracts rather than transcription (`dispatch_loop_head_not_covered`). Ranked in `docs/4ch8f-transcription-queue.md`, the `execution_requests_hash` hash-half compose is still open. (The validation-accept prefix landed domainRestricted; that work is DONE and its issue closed.) ⚠️ `stage_system_call` NO LONGER belongs on this list: its machine post landed (`stage_system_call_spec_within`, `.conditional`) β€” `a2` is 0, 1 or 2 with the STAGING-failure class 1 kept distinguishable from the EXECUTION-failure class 2 (the `InvalidBlock` propagation gap, fixed and closed), plus `a1 = 0`, `a0 = &system_call_returndata` and `system_call_mode = 0` on the failure path and `ra`/`s0` restored on every path, all of it CALLEE-INDEPENDENT because `a2` is written only by that routine's own `li` instructions. What survives is the DISCHARGE of its three named residuals `ArdCallShape` / `SscpCallShape` / `RdcCallShape`. ⚠️ The last of those is the strongest thing this lane assumes β€” it claims the whole EVM interpreter leaves the two dedicated spill cells untouched, which is why the staging routine is NOT re-entrant β€” and it has had NO open tracker since the handler-lane design issue closed 2026-09-01; everything the other two shapes pin was measured against the callee's emitted text, `assemble_execution_requests` whole-routine triple LANDED (`assemble_execution_requests_spec_within`) and `requests_hash_verify` LANDED on top of it (`requests_hash_verify_spec_within`: the assemble call is genuinely COMPOSED via `callWithin_spec`, not assumed). What survives is narrower and is a residual, not this item: the `execution_requests_hash` call at 0x8005437c stands under `ErhCallShape` because that routine's own triple covers only a NON-RETURNING validation prefix (B β†’ B+300). The hash-half discharge owner is now DONE β€” `zkvm_sha256_spec_within` exists and is consumed β€” so the sole remaining owner is the return path of `execution_requests_hash`. (The Program conversion itself is DONE, byte-identity waived, ELF byte-identical; its issue closed), `erh_hash_one` empty+nonempty tops under residual h_sha (shaCallWithinShape) landed; the discharge owner is a machine triple `zkvm_sha256_spec_within` now EXISTS in `Codegen/Proofs/HashBridgeSha256Top.lean:500` and is registered as the `.proven` `zkvm_sha256` row in `Progress/Routines.lean`. The full body spine now covers setup, block processing, padding (both `rem < 56` and `rem β‰₯ 56`), digest and output, with the exported post tied to `SpecRef.sha256`; the earlier note that padding/digest/output were deferred is stale. ⚠️ ALSO STALE, and re-measured 2026-09-02: the retirement this cell used to list as remaining work is DONE β€” `ExecutionRequestsHashShaDischarge` establishes the `callWithin` from the machine triple and BOTH `erh_hash_one` tops now say "discharged via `zkvm_sha256_spec_within` (no residual `h_sha`)", so no `shaCallWithinShape` premise survives on either. What that retirement unblocked but did not discharge is the separate hash-half five-slot compose after `validation_accept` (the parent `execution_requests_hash` composition remains open, and is the same owner the item above names). | 2026-09-02 @closed-blocker-sweep | | 5 | Full opcode coverage with verified handlers | 🟑 blocked | `RETURN`, `REVERT`, `SELFDESTRUCT`, 14 `.execSpec` entries have no RV64 subroutine (axis A.2): KECCAK256, BALANCE, EXTCODESIZE, EXTCODECOPY, EXTCODEHASH, SLOAD, SSTORE, LOG0..4, CREATE, CALL, CALLCODE, DELEGATECALL, CREATE2, STATICCALL | 2026-08-10 @372162cc2 | | 6 | Accelerator ECALL bridges per `zkvm_accelerators.h` | 🟑 blocked | 55 accelerator-site bridges remain after the landed `zkvm_keccak256` pilot: secp256k1 recovery (0x01), BN254, P256VERIFY, BLS G1, and the curve/complex accelerator families 0x802–0x80A; the 56-site census is recorded in #10552 and the family inventory is `docs/4ch8f-crypto-kernel-inventory.md`; the 56 figure counts decoded CSRRS encodings, while that inventory's 64 counts raw pre-encoded `.4byte` sites, so the two populations are not yet reconciled | 2026-08-11 @84e000579 | | 7 | MPT verification of pre-state witness proofs | 🟑 blocked | trie-walk loop spec for `mpt_walk` over `mptNodeIs`/`nodeDbIs` against `trieLookup` β€” arm pieces + kind callWithin landed (that issue closed); the surviving residual is the callee `witness_lookup_by_hash` machine triple for the HIT/general domain BEYOND `widx_count = 1`, tracked at #12996 (the successor that carries exactly the two uncovered shapes; its predecessor closed 2026-09-01 with the `widx_count = 1` scope met). TRANSCRIPTION DONE (PR 12111) and the empty-section miss triple landed. Both `wlCallWithinShape` repairs are now DONE: walk `fullCode` unions `wlhCr` (#12152), and the six `wlh_*` telemetry cells join `wlCallEntry`/`wlCallReturn` (#12162), so the generic residual is SATISFIABLE rather than vacuous. PRODUCTION empty-miss at walk sites is now enable=1: `wlCallWithinShapeEn` + three discharges `root/branch/ext_wl_enabled_empty_establishes_shape` via `wlhCallWithin_enabled_empty` over the enabled_empty top. Nested stack needs `stackFree sp0 16` (SAY SO). LEGACY enable=0 three-site `MptWalkWlEmpty` kept. PRODUCTION HIT at `widx_count = 1` is now the same shape one domain over: `wlCallWithinShapeHitEn` + three discharges `root/branch/ext_wl_enabled_hit_establishes_shape` via `wlhCallWithin_enabled_one_hit` over the enabled_one_hit top, so at the three sites the hit residual is a THEOREM on that domain, not a hypothesis. What is NOT covered (#12996): arbitrary `widx_count` (the real binary search, which first needs an index-sortedness predicate nothing states) and the linear scan with `zkvm_keccak256`. And the enable=0-shaped `MptWalkResidualChain.wlCallWithinShapeHit` (`stackFree sp0 8`, six-cell `wlTelemetry`, no `widx_*`/`wlh_indexed_*` cells, no `widx_records` bytes) is a DIFFERENT residual that stays a free `h_wl` on the hop-glue chains β€” no enable=1 arm can produce that ambient. `hp_decode_nibbles` and setup/root are RETIRED., machine triple `witness_lookup_by_hash_spec_within` at GuestAddrs.witness_lookup_by_hash for the GENERAL/HIT domain β€” production empty-miss enable=1 is proved and consumed at three walk sites, and the enable=1 HIT arm at `widx_count = 1` is now proved whole-routine (`witness_lookup_by_hash_spec_within_enabled_one_hit`, fuel 402) with the section pointer AND length free-but-matched, and CONSUMED at the three walk sites (`wlCallWithinShapeHitEn`); what remains is #12996's two shapes, arbitrary `widx_count` (the real binary search) and the linear scan with `zkvm_keccak256`. The enable=0-shaped `wlCallWithinShapeHit` on the hop-glue chains is a separate free hypothesis with NO open tracker of its own, retired only by moving those chains onto the enable=1 ambient, witness-ingest DB builder triples against `build_node_db`/`build_code_db`. ⚠️ STILL LIVE, and now UNTRACKED: the issue this item used to cite was about TRANSCRIPTION, and it closed 2026-08-12 once both guest-side builders became Programs, i.e. once a `cpsTripleWithin` became STATABLE. Neither has one, and no successor issue was opened, three-tier resolve coherence (appended DB / resolve cache / witness section) vs SpecRef's single node source β€” where `resolveCacheValidIs` (`Evm64/MptAssertions.lean`) earns its keep | 2026-09-02 @closed-blocker-sweep | | 8 | Verified post-state root β†’ public output | 🟑 blocked | obligation #4 (interpreter loop), obligation #5 (opcode coverage), obligation #6 (accelerator bridges), obligation #7 (MPT verification), guest-image `CodeReq` coverage: `guestImageCodeReq` pins only PART of `.text`. The live figure is DERIVED, not recorded β€” see the `Guest-image CodeReq coverage` section of DRIFT.md, rendered from `EvmAsm/Progress/GuestImageCoverage.lean` (`coveredBytes` from `guestImageEntries`, `textBytes` from `RegionMap.textSizeBytes`), so it cannot go stale; `scripts/guest_image_coverage.py` remains authoritative for the per-symbol GAP accounting, which needs the ELF symbol table. This cell used to quote the figures inline and two of the three literals had gone stale, which is the class `scripts/check-obligation-claims.sh` now gates. A `cr` that does not pin an address the run executes makes the triple FALSE, not weak β€” `Codegen/Proofs/TopComposition.lean:cpsTripleWithin_needs_entry_code` proves the entry-address case. So this obligation cannot be closed at the image CodeReq until coverage is complete (incl. unconverted `_start`), independently of 4/5/6/7, framing footprint: `guestFraming` now owns the measured halt-boundary registers x5, x10 and x17 in BOTH `scratch` and `residue`. The generic forcing lemmas still apply to any register omitted by a framing, but the unconverted `_start` shell remains the inherited whole-image clobber residual, so this narrow boundary set is not yet a complete image clobber theorem. (The constraint that an unpinned entry makes a phase FALSE rather than weak is unchanged; its issue closed 2026-08-12 once the coverage figure it was misquoted against was corrected at its generated source.), the composition itself is NO LONGER a blocker: `TopComposition.lean:runStatelessGuestSound_of_phases` proves `runStatelessGuestSound` from six named phase hypotheses, and `runStatelessGuestSound_demo` shows that family is jointly satisfiable (so it is not a vacuous implication) | 2026-09-02 @closed-blocker-sweep | | 9 | Halt convention per `standard-termination-semantics` | βœ… done | `--halt linux93` default; docs/host-io-halt-convention.md | β€” | | 10 | Witness reads are sound (get_account_optional composition) | 🟑 blocked | bal_canonical_sort ordering + permutation β€” the digit extractor's descriptor↔semantic-key agreement landed (that issue closed); the remaining blocker is the `.Lbalsort_pop` work-list loop's lexicographic measure, which has no precedent anywhere in `EvmAsm/Codegen/Proofs/`. ⚠️ Key uniqueness is a PRECONDITION discharged by the producer, and it is discharged for only 2 of the 6 live sort call sites (#12102), trie-walk loop spec for `mpt_walk` over mptNodeIs/nodeDbIs against trieLookup β€” arm pieces + kind callWithin + path-preserve landed (that issue closed); residual only hit/general `witness_lookup_by_hash` machine beyond `widx_count = 1` (#12996). Both `wlCallWithinShape` repairs are DONE (#12152, #12162), so the generic residual is satisfiable rather than vacuous. The three empty-section discharges at walk sites are on the production-UNREACHABLE `section_len = 0`/`widx_enabled = 0` domain; discharged and satisfiable is not the same as reached. The informative indexed domain is `widx_enabled = 1`, and BOTH indexed callee triples now exist on it (`witness_lookup_by_hash_indexed_spec_within_empty` and `…_one_hit`), each with an exhibited entry state β€” so what that domain still lacks is the PARENT at arbitrary count, not a callee contract. hp_decode_nibbles and setup/root are RETIRED. Three-tier resolve divergence stated in docs/4ch8f-slstate-specref-correspondence.md:164, machine triple `witness_lookup_by_hash_spec_within` (#12996) β€” transcription landed (PR 12111), the `section_len = 0` whole-routine triple is proved and consumed at the empty-section walk sites (#12162), and the enable=1 HIT arm is proved whole-routine at `widx_count = 1` (`witness_lookup_by_hash_spec_within_enabled_one_hit`, fuel 402) and now CONSUMED at the three walk sites on that domain (`wlCallWithinShapeHitEn`, `root/branch/ext_wl_enabled_hit_establishes_shape`). Remaining, per #12996: arbitrary `widx_count` (binary search) and the linear scan loop at a symbolic trip count with `zkvm_keccak256`. Remaining OUTSIDE #12996, and now with no open tracker at all: the enable=0-shaped `wlCallWithinShapeHit` still free on the hop-glue chains, witness-ingest DB builder triples against build_node_db/build_code_db. ⚠️ STILL LIVE, and now UNTRACKED β€” the issue this item used to cite was about transcription and closed 2026-08-12 once both builders became Programs; that made a triple STATABLE, not proved, and no successor was opened, no `cpsTripleWithin` for `witness_codes_index_build`, and only a `.conditional` empty-section one for `witness_codes_lookup_by_hash` (`witness_codes_lookup_by_hash_spec_within_empty_section`) β€” the code-DB *routines*. The predicate side is DONE and its issue closed; the general-domain routine triples remain | 2026-09-02 @closed-blocker-sweep | ## Guest-image `CodeReq` coverage `guestImageCodeReq` pins **38.61%** of `.text` β€” 133248 of 345064 bytes across 476 linked entries, leaving 211816 bytes unpinned. ⚠️ **This line is DERIVED, not recorded** β€” computed from `guestImageEntries` and `RegionMap.textSizeBytes` at render time (`EvmAsm/Progress/GuestImageCoverage.lean`), so it cannot go stale. #12129 exists because three different hand-written coverage percentages coexisted here, all stale, each under a caveat telling the reader to re-measure. Cite this line or the definitions behind it; do not copy the digits into prose, where `scripts/check-obligation-claims.sh` will reject them. Coverage matters for obligation 8 specifically: a `cr` that does not pin an address the run executes makes a triple **FALSE**, not weak β€” see `Codegen/Proofs/TopComposition.lean:cpsTripleWithin_needs_entry_code`. The per-symbol gap accounting (which ranges are unpinned, and why) needs the ELF symbol table and stays with `scripts/guest_image_coverage.py`. ## What is NOT proven ### πŸ”Ά `conditional` opcodes β€” proven only on a restricted input domain A complete top-level Hoare triple exists, but gated by a non-vacuous precondition; the excluded domain is **unverified**. | Opcode | Why not (yet) fully proven | |---|---| | `RETURN` | full standalone (depthAware=false) return-data window + halt core, from the post-gas handler entry through the RETURN-only system_call_mode capture block and the 0xa0010000 descriptor (header/22-dword-body zeroing, size@+64, clamped=min(size,176)@+248, evm_memory[offset..offset+clamped] copied to +72, first min(size,32) bytes to +0, kind=1@+32) to the shared dispatchHaltRet 2 core (evm_halt_flag:=2, x1:=resume, ret to resume&&&~~~1). The front now covers all system_call_mode cases: zero skips capture; nonzero with size>4096 skips conservatively; nonzero with size<=4096 stores system_call_returndata_len:=size and copies the full returndata window to system_call_returndata. `.conditional` remains because the memory-gas `preBody` (its .exit_outofgas branch) is framed OUT as a decision-1 TCB boundary, so the theorem still carries the post-gas memory-domain hyps (hOff/hOff32 and branch-conditional hOffCapture/hRdCapture). The seven `la` immediates stay as reconstruction hyps (shared deferred byte-check, as in the halt core). `cycleBound` stays `none`: the bound is a LOOP bound in the return-data size β€” `cpsTripleWithin (164 + 7 * size.toNat + 7 * (returnClamp size).toNat + 7 * (returnClamp32 size).toNat)` β€” not a literal. | | `REVERT` | full standalone (depthAware=false) return-data window + rollback + halt core, from the post-gas handler entry through the 0xa0010000 descriptor (header/22-dword-body zeroing, size@+64, clamped=min(size,176)@+248, evm_memory[offset..offset+clamped] copied to +72, first min(size,32) bytes to +0, kind=2@+32), the five straight-line rollback env-cell stores on x20 (env+448:=env+456, env+464:=0, env+472:=env+480), to the shared dispatchHaltRet 2 core (evm_halt_flag:=2, x1:=resume, ret to resume&&&~~~1). Near-clone of RETURN reusing its window loop closures + halt core verbatim (only the code layout shifts down 80 bytes with no capture block, the kind-store value is 2, and the rollback is appended). `.conditional` NOT because of a system_call_mode gate (REVERT has no capture block β€” that is kind==1/RETURN-only β€” so it is strictly more general than RETURN) but because (1) the memory-gas `preBody` (its .exit_outofgas branch) is framed OUT as a decision-1 TCB boundary and (2) the evm_memory well-formedness domain hyps (hOff/hOff32 etc.) restrict the input domain, exactly as in RETURN. The four `la` immediates stay as reconstruction hyps (shared deferred byte-check, as in the halt core). `cycleBound` stays `none`: the bound is a LOOP bound in the return-data size β€” `cpsTripleWithin (155 + 7 * (returnClamp size).toNat + 7 * (returnClamp32 size).toNat)` β€” not a literal. | | `SELFDESTRUCT` | halt/routing tail only β€” the shared dispatchHaltRet 4 core (evm_halt_flag:=4, x1:=.dispatch_resume, ret to resume&&&~~~1) over the verified `evm_selfdestruct` program; direct STOP/INVALID clone with routing code 4 (`.exit_selfdestruct`). The two `la`s (`evm_halt_flag`, `.dispatch_resume`) are RESOLVED via `la_resolve` (#10059), leaving only decidable `laInRange` per `la`. `.conditional` β€” NOT `.proven` unlike STOP/INVALID (whose dispatched handler IS just the halt tail, body:=[]) β€” because SELFDESTRUCT's dispatched handler (`selfdestructTailAsm`) runs a substantial effects body BEFORE this tail that is framed OUT as the residual: cold-access gas (with its own .exit_outofgas branch), new-account surcharge, EIP-6780 created-in-tx detection, balance transfer to the beneficiary, EIP-7708 log, beneficiary nonstorage record, and the CREATE-child frame_return path. A larger residual than RETURN/REVERT's gas-only preBody; a future phase proves it against `EL/SelfdestructEffects` to earn `.proven`. | ### 🟑 `partly` opcodes β€” no complete top-level triple yet Pure-spec / `_correct` lemma proven, but no end-to-end stack-spec wrap. | Opcode | Why not (yet) fully proven | |---|---| ### ⏳ `execSpec` opcodes β€” handler/bridge semantics only, no RV64 subroutine These 14 opcodes have executable-spec / handler / host-bridge semantics only; **no RV64 subroutine is proven to produce the EVM result**: KECCAK256, BALANCE, EXTCODESIZE, EXTCODECOPY, EXTCODEHASH, SLOAD, SSTORE, LOG0..4, CREATE, CALL, CALLCODE, DELEGATECALL, CREATE2, STATICCALL. ### βœ— `notStarted` opcodes β€” not represented in `EvmOpcode` | Opcode | Why not (yet) fully proven | |---|---| ## Trust boundaries (unverified by design) - **Codegen is unverified by design.** The RISC-V lowering, the ziskemu emulator, and the deferred codegen milestones (M5 EVM-interpreter loop and beyond) are explicitly outside the kernel-checked core. Drift is *fenced* by build-time `#guard` round-trip tests (`Codegen/RoundTripTests.lean`) and the conformance floor (`check-conformance-floor.sh`), not *proven*. - **Handler glue is proven per-opcode, not universally.** Each opcode is `.proven` on its verified *body* spec, but the subroutine the codegen emits, `h_`, wraps that body in glue β€” a stack-underflow guard prologue, any `preBody` clobber-saves / `la` address loads, and the advance-`x10`/`ret` tail β€” that the body spec does not cover. This handler glue is separately kernel-proven (guard + body + tail, both underflow and no-underflow paths) for `ADD` (`Codegen.Proofs.evmAddGuardedHandlerSpec`) and `CALLDATALOAD` (`Codegen.Proofs.evm_calldataload_staged_guarded_handler_spec`); for the other `.proven` opcodes (`MOD`, `EXP`, `ADDMOD`, …) the preBody glue is **not yet proven**. The final tie from the proven Program to the emitted ELF bytes is machine-checked for `h_ADD` only (`scripts/check_guarded_handler_bytes.py`); for `CALLDATALOAD` the `la` targets are proven relative to reconstruction hypotheses, with the byte-tie deferred. - **`RETURNDATACOPY`'s image omits the framed-out high-limb operand guards.** The `.proven` witness `evm_returndatacopy_body_stack_spec_within` covers the body (`base β†’ base+80`: bounds guards, operand pop / pointer setup, copy loop), but the emitted handler additionally runs, *between* the operand loads and the frame materialization, two blocks the modeled image excises along with the dynamic-gas / MSIZE glue: (i) `memDynamicU256RangeOogGuardAsm`, which sends a high-limb `size` β€” and, when `size β‰  0`, a high-limb `destOffset` β€” to `.exit_outofgas`; and (ii) an `ld`/`or`/`or`/`bnez` check sending a high-limb *source offset* (`dataOffset` limbs 1–3) to `.exit_invalid`. The triple is a statement about that excised image, so it describes only the path on which those guards fall through; on operands with nonzero high limbs the emitted handler exits before this body's postcondition is reached. Note the three bridging hypotheses `h_destOff`/`h_srcOff`/`h_sizeV` (`operand.getLimbN 0 = BitVec.ofNat 64 n`) are **naming** bridges from the stack limbs to the `Nat` offsets β€” they place no constraint on the high limbs and are not where this residual lives. Closing it means modeling those blocks in the guard image (shifting every guard branch offset) or proving the framed-out region. CALLDATACOPY carries the same class of residual β€” its source-offset normalization block is likewise `preBody` glue. *Why each excised guard is safe to excise β€” three different arguments, none of them in the proof.* Read this before treating a `RETURNDATACOPY: proven` row as covering wide operands; the justifications do not share a shape: | assumed by | justified by | holds at `size = 0`? | reasoning lives in | |---|---|---|---| | high-limb `size` | **gas** β€” `copy_gas_cost` and memory expansion both explode β‡’ `OutOfGasError` | yes | `EvmMemoryGas.lean` `memDynamicU256RangeOogGuardAsm` docstring | | high-limb `destOffset` | **gas, but conditional on `size β‰  0`** β€” quadratic expansion β‡’ `OutOfGasError`; at `size = 0` `calculate_gas_extend_memory` `continue`s and charges nothing, so the spec *accepts* it | **no β€” spec accepts** | same docstring; the guard's `beqz ` ordering mirrors `gas.py`'s `if size == 0: continue` | | high-limb source offset (`dataOffset`) | **not gas** β€” the spec's explicit `Uint(start) + Uint(size) > ulen(return_data)` β‡’ `OutOfBoundsRead` | yes β€” rejecting is *required*, not over-strict | the `h_RETURNDATACOPY` comment in `Codegen/Programs/NoopReturnData.lean` | So each excised guard matches a real execution-specs outcome (Amsterdam `vm/instructions/environment.py`, `vm/gas.py`): excising them costs coverage but hides no divergence, and in particular the guest does **not** over-reject the `size = 0` / high-limb-`destOffset` case the spec accepts. - **RV64 instruction-model fidelity.** The Lean RV64 semantics are tied to the official Sail RISC-V model via `Rv64/SailEquiv/` (the `riscv-zkvm` release pinned in `lakefile.toml`); the tie itself is a trusted reference, not a kernel theorem about real silicon. - **EVM reference semantics.** Conformance is measured against `ethereum/execution-specs` (pinned submodule); that the pinned spec faithfully encodes consensus rules is assumed, not proven here. - **Gas / memory cost modeling.** Per-opcode `cpsTripleWithin N` bounds are a verified *step-count surrogate*; the EVM gas schedule mapping is modeled, not proven equivalent to the yellow-paper schedule. - **Per-opcode handler glue.** Even for `.proven` opcodes, the handler `preBody`/tail glue around the verified subroutine β€” gas accounting (`copyWordGasAsm`), MSIZE / memory-expansion bookkeeping (`updateActiveMemorySizeAsm`), OOG guards, and offset normalization β€” is unverified `.custom` asm (the CALLDATACOPY #9880 convention). A dedicated gas-glue verification track is deferred work; until it lands, the `.proven` tier certifies the opcode's data effect, not its gas/expansion glue. - **Trusted axiom base.** Only the three classical axioms (`propext`, `Classical.choice`, `Quot.sound`); `native_decide`/`bv_decide` trust axioms are forbidden (CI-gated by `check-axioms.sh` / `check-forbidden-tactics.sh`).