| name | prove-soundness |
| description | Work on the stepF-to-Step soundness proofs in EVM/Equiv.lean — discharge a proof obligation, extend a helper lemma after an opcode change, or fix a broken proof. Use when touching Equiv.lean, when a soundness lemma fails to close, or after changing Step/stepF for an opcode. |
prove-soundness
Maintain EVM/Equiv.lean, which proves
stepF_sound : ¬ s.isDone → Step s (stepF s) — every transition the (total)
executable stepF takes on a non-done state, success or exception, is a valid
Step derivation (via stepFE_sound over the Except-valued stepFE). Read AGENTS.md for the
three-view architecture (Step / Eval / stepF) before editing.
The hard rule
Equiv.lean is closed — no sorry. Do not introduce sorry, admit, or
native_decide-style escape hatches to make it build. If a proof won't close,
the fix is in the proof or in a missing supporting lemma, not in weakening the
statement.
Proof structure (two layers)
- Per-helper soundness lemmas — one per
stepF.* group helper:
stopArith_sound, compBit_sound, keccak_sound, env_sound,
block_sound, system_sound, stackMemFlow_sound, push_sound,
log_sound, dup_sound, swap_sound, dupN_sound, swapN_sound,
exchange_sound. Each unfolds the helper, matches on the operation kind
and stack shape, then closes every leaf either by applying the matching
Step constructor or by deriving a contradiction from h : … = .ok _ when
stepF actually returned .error.
- Headline
stepF_sound — unfolds stepF, splits on
s.halt / s.decoded / the gas check / the operation kind, and dispatches
each Operation constructor to its helper lemma.
Eval.halted_inv (a halted state's only Eval is Eval.halted) is also
exported and does not go through stepF.
Working idioms in this file
- Contradiction leaves. When a
match arm corresponds to a stepF path
that returns .error, the hypothesis h : stepF… = .ok s' is absurd. Close
it with nomatch h / simp at h / exact absurd h … rather than fabricating
a transition.
- Constructor premises must line up — but they vary by constructor. A
typical arithmetic/stack
StepRunning success constructor takes h_op
(s.decodedOp = some .OP), h_gas
(Gas.cost op ≤ s.gasAvailable — gasAvailable is a Nat, no .toNat), and
an h_stack shape; the running guard is not a constructor premise — the
headline theorem supplies it once via the Step.running wrapper. Notable
exceptions to check before chasing arguments: StepRunning.stop has only
h_op (no h_gas, no h_stack) — but the other halts differ:
StepRunning.return_/StepRunning.revert carry h_gas, h_stack, and an
h_mem memory-expansion premise. Stackless reads like
address/coinbase/pc have h_gas but no h_stack. Read the actual
constructor. Supply each premise from the helper's match context; consumeGas
needs the gas proof explicitly.
- List witnesses.
log_sound recovers the topics list via
popN_correct (in StepF.lean): popN stk k = some (topics, rest) implies
topics.length = k ∧ stk = topics ++ rest. Reuse it rather than re-inducting.
- Decoder-width pitfall.
StepRunning.pushN takes the immediate width as an
explicit immWidth : Nat parameter (not k.val) so push soundness doesn't
need a separate decoder invariant. Preserve this if you touch PUSH.
After an opcode change
If you changed Step.lean / StepF.lean for an opcode (see "Adding or changing
an opcode" in AGENTS.md), extend the matching *_sound helper so it still
closes, then verify against the targets CI builds (warning-clean) and lake lint:
Run the build-and-lint skill's CI warning gate (the set -o pipefail +
grep warning: + exit 1 block over lake build evm_semantics vmtests), then
lake lint. A plain lake build is not enough on its own: a proof hole only
emits a declaration uses 'sorry' warning, and lake build still exits 0 —
the build-and-lint gate is what turns that warning into a non-zero exit, the same
way CI does.
A textual grep for sorry is not a reliable hole-check either: Equiv.lean's
own docstring contains the phrase (no `sorry`), so grep sorry reports a
false positive. If you grep anyway, expect only that docstring line:
grep -n 'sorry' EvmSemantics/EVM/Equiv.lean
Reporting
State whether the proof closes with no sorry and that lake build is clean.
If a lemma won't close, name the exact lemma and the leaf goal that's stuck.
