feat(evm): add proof-facing step runs

[Th0rgal]

Scope

This is F4a: generic EVMYulLean proof-facing execution infrastructure over the existing executable EvmYul.EVM.step.

It adds:

• a graph relation preserving both successful and exceptional Except results;
• an exact-length, instruction-labeled Runs relation for successful steps;
• zero, one, successor, transitivity, and determinism lemmas;
• an executable decoded-instruction runN, with soundness and completeness;
• a kernel-checked PUSH/JUMPI/JUMPDEST/RETURN fallthrough fixture that applies runN_sound.

No opcode semantics are duplicated, and there are no changes to gas accounting, accounts, X, Xi, or opcode implementations.

F4b—decomposition or equivalence results involving X/Xi—is explicitly left to a later PR. This PR makes no EIP-8282 guarantee.

Verification

• lake env lean EvmYul/EVM/Proof/Execution.lean
• lake build EvmYul
• lake build
• lake build yulSemanticsTests && lake env yulSemanticsTests
• git diff --check
• changed-Lean-file scan for sorry|admit|axiom|native_decide: zero matches

The lightweight Yul semantics test executable completed successfully. No external Ethereum conformance corpus was run.

[Th0rgal]

@codex review

Pushed 2343349. Two commits on top of 677b2d69.

The previous head did not compile. With -DautoImplicit=false the Runs inductive left instr/pre/mid/n unbound, and the concrete fixture asked rfl to evaluate seven opcodes, blowing the heartbeat limit. There are no CI checks on this branch, so that went unnoticed. Both are fixed.

What the proof API now offers

• Step / StepOk — the graph of the executable EvmYul.EVM.step, result kept as Except so exceptional executions are recorded rather than given an invented post-state. Step.deterministic.
• Runs over a trace of (fuel, gasCost, instr) entries. The per-entry labelling is forced by X: it decrements fuel each iteration and recomputes gas through C', so a run under one shared gas cost could not describe real code. trans, deterministic, and runN_iff_runs against the executable runN.
• One-step decomposition of X itself: X_zero, X_succ_of_Z_error, X_succ_of_step_error, X_succ_of_continue, X_succ_of_halt, X_succ_of_revert — a complete case analysis of one iteration, so a proof can peel X one instruction at a time without re-deriving its body.
• XStepAt / XRuns chaining those, with X_eq, length, trans, head_step, X_outOfFuel, X_success.

Two things worth your attention

1. The mirrors. X inlines W, Z and H as local lets, so no outside proof can name them. They are mirrored verbatim in this module. The mirrors are not assumed to agree with X: every decomposition theorem unfolds X and rewrites with the mirror, so drift breaks the proof rather than passing silently. If you would rather lift W/Z/H to top level in Semantics.lean and have X call them, say so — that removes the duplication, at the cost of touching core semantics.

2. Vacuity. XRuns.length previously read ∃ trace, trace.length + rem = fuel, which any list of the right length satisfies — it was not a statement about the run. XRuns is now indexed by the trace it actually executed, so the fuel accounting is real. And nothing witnessed a non-reflexive XStep, so the whole X-level layer could have been vacuous; Z_JUMPDEST now discharges the exceptional-halting check for any state that can pay Gjumpdest with stack room, yielding xStepAt_JUMPDEST and xRuns_one_JUMPDEST.

Verification

• lake build — exit 0, whole project (1119 jobs), Lean 4.31.0.
• No sorry, no project axiom, no native_decide. #print axioms on all 28 declarations returns exactly [propext, Classical.choice, Quot.sound].

Please look hardest at whether any statement is weaker than it reads, and at the mirror/X correspondence.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Keep it up!

Reviewed commit: 2343349a46

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".