| ✅ STOP |
proven |
evm_stop_stack_spec_within |
7 |
halt-triple over the verified evm_stop program (byte image of the emitted dispatchHaltRet 1 tail): sets evm_halt_flag := 1, points x1 at .Ldispatch_resume, and rets to resume &&& ~~~1; the two las stay hla1/hla2 reconstruction hyps as in the guard/glue precedents. First terminating/halt opcode — shape for INVALID/RETURN/REVERT/SELFDESTRUCT |
| ✅ 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_v6_stack_spec |
— |
full-domain unconditional v6 DIV stack spec over divCodeV6 (n=1 single-limb fast-path dispatch); the n≥2 / b=0 arm reuses the v5 proof (evm_div_v5_unconditional_over_divCodeV6), the n=1 fast arm is divK_fastBody_dispatchPostV5_within_v6, merged via the BNE/BEQ dispatch |
| ✅ SDIV |
proven |
evm_sdiv_exact_callable_return_result_stack_spec_within_v5 |
— |
unconditional SDIV stack spec over sdivCodeV5 (the shipped v5 codegen — signed DIV via the proven unsigned evm_div_callable_v5); the former hStack is discharged by M2's callable correctness, incoming x2/x9 generalized (both dead), x9 shed at the return |
| ✅ MOD |
proven |
evm_mod_v6_stack_spec |
— |
full-domain unconditional v6 MOD stack spec over modCodeV6 (n=1 single-limb fast-path dispatch); the n≥2 / b=0 arm reuses the v5 proof (evm_mod_v5_unconditional_over_modCodeV6), the n=1 fast arm is modK_fastBody_dispatchPostV5_within_v6, merged via the BNE/BEQ dispatch |
| ✅ SMOD |
proven |
evm_smod_exact_callable_return_result_stack_spec_within_v5 |
— |
unconditional SMOD stack spec over smodCodeV5 (the shipped v5 codegen — signed MOD via the proven unsigned evm_mod_callable_v5); the former hStack is discharged by M2's callable correctness, incoming x2/x9 generalized (both dead), x9 shed at the return. (was: nonzero path still parameterized by unsigned-MOD callable h_stack |
| ✅ ADDMOD |
proven |
evm_addmod_total_result_stack_spec_within |
— |
unconditional total ADDMOD stack spec over evm_addmod_total ∪ evm_mod_callable_v5 (the shipped codegen — issue #9704): all three runtime branches covered (N = 0 zero path; no-carry low-sum reduction; the 257-bit carry-out path computing (2^256 + r) mod N via three MOD near-calls — rMod, pow256ModN N as ((2^256−1) mod N + 1) mod N, and a pre-reduced modular add with branch-free conditional subtract). Public form evmStackIs sp [a, b, N] → evmStackIs (sp+64) [EvmWord.addmod a b N]; only dispatcher-pinned code-layout side conditions. (was: partial OR-guard domain surface over the legacy v1 callable) |
| ✅ MULMOD |
proven |
evm_mulmod_stack_spec_within |
34295 |
full-domain unconditional MULMOD stack spec for every modulus (no n ≤ 2^255 hypothesis); bit-serial 512-bit reducer. Scratchpad relocated below the stack pointer (sp + signExtend12 3936..4088 = sp-160..sp-8) so the live EVM stack is preserved |
| ✅ EXP |
proven |
evm_exp_stack_spec_within |
49447 |
unconditional EXP stack spec over the concrete appended headroom program (evm_exp_msb_saved_bit_two_mul_fixed_headroom ;; mul_callable, CodeReq.ofProg): full 256-iteration square-and-multiply loop via the proven MUL callable; pre = evmStackIs evmSp (base :: exponent :: rest) plus an explicit x2 local frame and 8 headroom dwords + 2 scratch EVM words below the live stack (evmSp-128..evmSp-32 — MULMOD below-sp precedent); post = evmStackIs (evmSp+32) (EvmWord.exp base exponent :: rest) with clobbered state shed to evmExpHeadroomPublicLeftoverFrame; only side condition is the even entry base. (was: partial headroom surface pending the public wrapper) |
| ✅ 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 |
— |
— |
witness-backed account read |
| ✅ 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 |
proven |
Calldata.evm_calldataload_staged_stack_spec_within |
— |
|
| ✅ CALLDATASIZE |
proven |
Calldata.evm_calldatasize_stack_spec_within |
— |
|
| ✅ CALLDATACOPY |
proven |
Calldata.evm_calldatacopy_stack_spec_within |
— |
|
| ✅ CODESIZE |
proven |
Code.evm_codesize_stack_spec_within |
— |
|
| ✅ CODECOPY |
proven |
Code.evm_codecopy_stack_spec_within |
— |
copy-loop body proven (mirror of CALLDATACOPY); preBody gas/MSIZE glue unverified per DRIFT |
| ✅ GASPRICE |
proven |
Env.evm_gasprice_stack_spec_within |
— |
|
| ⏳ EXTCODESIZE |
execSpec |
— |
— |
witness-backed account read |
| ⏳ EXTCODECOPY |
execSpec |
— |
— |
witness-backed code copy |
| ✅ RETURNDATASIZE |
proven |
ReturnData.evm_returndatasize_stack_spec_within |
— |
|
| ✅ RETURNDATACOPY |
proven |
ReturnData.evm_returndatacopy_body_stack_spec_within |
— |
whole-body stack triple over guards ++ setup ++ copy loop (ReturnData/{RevertProgram,RevertSpec,CopyProgram,CopyLoopSpec,CopySpec}.lean), base→base+80, composed with cpsTripleWithin_seq_perm_same_cr: the guard prefix loads the three low stack limbs, materializes evm_precompile_frame, loads the return-data length and falls through the two execution-specs bounds checks (start+size wrap, start+size>retlen — the old 256-byte frame cap was removed from the guest in #10160); setup pops the operands, takes the size≠0 skip and builds the pointers; the byte-identical bottom-tested do..while loop copies stagedBytes[start..start+size) into EVM memory (NO size≥1 gate: the size=0 path is proven too — guards fall through, operands pop, the beqz skip is taken to the exit and the postcondition degenerates to unchanged memory — so this is .proven, not .conditional, matching CALLDATACOPY whose top-tested loop exits at zero size) [destOff,destOff+size) via the Mcopy forward-loop content model, with the source region anchored at the aligned frame+16 base and the read offset carried in the pointer register (decoupled from destOff). The two invalid exits are companion witnesses (guard_{wrap,len}_invalid_stack). Same scope as CALLDATACOPY's registered witness: interleaved gas/OOG/MSIZE glue is framed out per DRIFT. RESIDUAL: the image also excises the handler's two high-limb operand guards — memDynamicU256RangeOogGuardAsm (high-limb size, and high-limb destOffset when size≠0, to .exit_outofgas) and the ld/or/or/bnez on dataOffset limbs 1-3 (to .exit_invalid) — so the triple describes only the path where those fall through. The h_destOff/h_srcOff/h_sizeV hypotheses are low-limb NAMING bridges and constrain no high limb. Each excised guard matches a real execution-specs outcome, but by three DIFFERENT arguments: high-limb size by gas; high-limb destOffset by gas only when size≠0 (at size=0 the spec charges nothing and ACCEPTS it — the guest matches via the guard's beqz ordering); high-limb dataOffset NOT by gas but by the spec's explicit start+size>len(return_data) OutOfBoundsRead, which fires at size=0 too. Costs coverage, hides no divergence; see DRIFT for the per-hypothesis table and where each argument lives. |
| ⏳ EXTCODEHASH |
execSpec |
— |
— |
witness-backed account read |
| ✅ BLOCKHASH |
proven |
BlockHash.evm_blockhash_stack_spec_within |
24 |
|
| ✅ 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 |
proven |
BlobHash.evm_blobhash_stack_spec_within |
20 |
|
| ✅ BLOBBASEFEE |
proven |
BlobBaseFee.evm_blobbasefee_stack_spec_within |
— |
|
| ✅ POP |
proven |
evm_pop_stack_spec_within |
1 |
|
| ✅ MLOAD |
proven |
evm_mload_stack_spec_within |
— |
all byte alignments; memory framed by evmMemoryIs; the explicit trailing guard band supplies the pair-read tail |
| ✅ MSTORE |
proven |
evm_mstore_stack_spec_within |
— |
aligned spec proven; unaligned _public variants in progress |
| ✅ MSTORE8 |
proven |
evm_mstore8_stack_spec_within |
5 |
|
| 🔶 SLOAD |
conditional |
Storage.evm_sload_stack_spec_within |
— |
stage-1 of the two-stage SLOAD plan: the persistent-log reverse scan (byte-identical body-as-Program of the h_SLOAD handler, base 0xa0630000, length cell env+448) is proven to replace the stack top in place with persistentLookup — the current of the most-recent committedStorageIs entry keyed by (env.ADDRESS, slotKey), or 0 on miss. .conditional because the miss→0 branch is EVM-sound only RELATIVE to the committedStorageIs snapshot supplied in the precondition; full MPT-witness verification that the snapshot faithfully reflects state root is deferred to stage-2 (post-Phase-10). Structural clone of the proven TLOAD reverse scan on the transient log. |
| ⏳ SSTORE |
execSpec |
— |
— |
Storage*.lean; ECALL → host |
| ✅ JUMP |
proven |
ControlFlow.evm_jump_stack_spec_within |
13 |
|
| ✅ JUMPI |
proven |
ControlFlow.evm_jumpi_stack_spec_within |
21 |
|
| ✅ PC |
proven |
ControlFlow.evm_pc_stack_spec_within |
— |
|
| ✅ MSIZE |
proven |
evm_msize_stack_spec_within |
6 |
|
| ✅ GAS |
proven |
GasOpcode.evm_gas_stack_spec_within |
— |
|
| ✅ JUMPDEST |
proven |
ControlFlow.evm_jumpdest_stack_spec_within |
0 |
|
| ✅ TLOAD |
proven |
Transient.evm_tload_stack_spec_within |
— |
|
| ✅ TSTORE |
proven |
Transient.evm_tstore_stack_spec_within |
— |
|
| ✅ MCOPY |
proven |
Mcopy.evm_mcopy_stack_spec_within |
— |
EIP-5656 (Cancun) overlap-aware memmove copy core proven (Mcopy/{Program,Result,ForwardLoopSpec,BackwardLoopSpec,Spec}.lean): byte-identical body-as-Program of the h_MCOPY handler tail (verified against riscv64-elf-as), TOTAL over all (destOff,srcOff,len) — the two BGEU offset comparisons dispatch to a forward (low→high) or backward (high→low) byte loop, both proven to land on the same direction-independent mcopyResult (memmove: dst window ← original src slice) via a single evolving evmMemoryIs slab with a read-sees-original invariant per direction. Stack decode + gas/MSIZE/range-guard glue unverified per DRIFT (same as CALLDATACOPY/CODECOPY). First memory→memory / overlap-aware opcode; first two-directional loop proof. |
| ✅ PUSH0 |
proven |
evm_push0_stack_spec_within |
5 |
|
| ✅ PUSH1 |
proven |
evm_push1_stack_spec_within |
— |
|
| ✅ PUSH2..32 |
proven |
evm_push_stack_spec_within |
— |
single proof generic over n=2..32; pushes the big-endian immediate; 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 |
— |
— |
ChildFrameHandlers; shared CALL family |
| 🔶 RETURN |
conditional |
Terminating.evm_return_stack_spec_within_with_capture |
— |
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). |
| ⏳ DELEGATECALL |
execSpec |
— |
— |
CallArgs kind = .delegatecall |
| ⏳ CREATE2 |
execSpec |
— |
— |
shared Create family |
| ⏳ STATICCALL |
execSpec |
— |
— |
CallArgs kind = .staticcall |
| 🔶 REVERT |
conditional |
Terminating.evm_revert_stack_spec_within |
— |
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). |
| ✅ INVALID |
proven |
evm_invalid_stack_spec_within |
7 |
halt-triple over the verified evm_invalid program (byte image of the emitted dispatchHaltRet 3 tail): sets evm_halt_flag := 3, points x1 at .Ldispatch_resume, and rets to resume &&& ~~~1; the two las stay hla1/hla2 reconstruction hyps as in the guard/glue precedents. Direct STOP clone with routing code 3 (.exit_invalid_op) |
| 🔶 SELFDESTRUCT |
conditional |
Terminating.evm_selfdestruct_stack_spec_resolved |
7 |
halt/routing tail only — the shared dispatchHaltRet 4 core (evm_halt_flag:=4, x1:=.Ldispatch_resume, ret to resume&&&~~~1) over the verified evm_selfdestruct program; direct STOP/INVALID clone with routing code 4 (.exit_selfdestruct). The two las (evm_halt_flag, .Ldispatch_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. |