feat(evm): runUntil, basic-block composition, and block tactics - #8
Conversation
`X` could be peeled one instruction at a time, but not reasoned about a basic block at a time. `RunUntil` composes consecutive non-halting iterations of `X` and records *why* the chain ended, so a correspondence proof can be handed the fact that the continuation begins at a block boundary rather than at an arbitrary prefix of a run. Supporting this needed two facts about `X`'s internals: that halting is a property of the opcode alone (`H_eq_none_iff`), which lets the driver decide to continue before running the instruction, and that `Z` only ever charges memory expansion (`Z_ok_state`), which lets block lemmas be phrased against the state `X` decoded in instead of against `Z`'s otherwise unnameable output. `xRunUntil` is the executable driver, validated in both directions, so a concrete block can be discharged by evaluation. `XReaches` is the trace-erased form, and `x_step` / `x_block` / `x_collapse` discharge a straight-line stretch from step facts in the context without the caller naming any intermediate state. Depends only on the merged F4a step-run layer. No axiom, no sorry.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c688f4dbb5
ℹ️ 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".
| `JUMPDEST` is included because it is where control can *arrive*, so a block that | ||
| ran through one would not be maximal. -/ | ||
| def BlockEnd (w : Operation .EVM) : Bool := | ||
| Halting w || CallFamily w || w ∈ [Operation.JUMP, .JUMPI, .JUMPDEST] |
There was a problem hiding this comment.
When execution reaches 0xfe or any unknown opcode, parseInstr decodes it as .INVALID and δ .INVALID = none, but this predicate returns false. Consequently xRunUntil BlockEnd attempts Z and returns .InvalidInstruction instead of producing an exit state, so the block-level RunUntil.X_Z_error theorem cannot be used for bytecode ending in an invalid opcode. Include .INVALID among the unconditional block-ending operations.
Useful? React with 👍 / 👎.
1 participant
Summary
F4d in the EIP-8282 parent-strength campaign. Adds the basic-block layer on top
of the merged F4a step-run decomposition (
EvmYul/EVM/Proof/Execution.lean).EvmYul.EVM.Proof.Executioncan peelXone instruction at a time, but nothingcould yet talk about a block — a maximal straight-line stretch of code, which
is the unit a correspondence proof actually wants.
XRunsis not enough on itsown: any prefix of a run is a run, so it never says why the chain ended.
New file:
EvmYul/EVM/Proof/Block.lean(one import line added toEvmYul.lean).Halting is a property of the opcode
Haltingdecides the same thingHdoes, without the machine state.H_eq_none_iffproves nothing was lost —Hreads the machine state only tofetch returned bytes on the branch that has already decided to stop. This is
what lets the executable driver decide to continue before running the
instruction.
Zis a gas frameZ_ok_state: wheneverX's exceptional-halting check accepts, the state ithands to
stepis the pre-state with memory expansion charged and nothing elsetouched. Without it every block lemma would have to be phrased against
Z'soutput, which is a state no caller can name.
Z_ok_stack_lengthadditionallyrecovers the stack depth an accepted instruction is guaranteed to have.
Z's body is a long guard chain thatsimpcannot walk (it exhausts the stepbudget) and
split_ifsre-elaborates branch by branch, soelim_guardpeels itone guard at a time.
RunUntiland compositionRunUntil stop validJumps fuel pre trace rem postchains non-halting iterationsof
Xand ends only for a reason it records:RunUntil.X_eq— the composition theorem: a block may be replaced by its endpoints.RunUntil.stopped— the exit state decodes to a stop instruction, or the fuel is gone.RunUntil.deterministic— a block is a partial function of entry state and fuel.RunUntil.length/rem_le— fuel accounting, inherited fromXRuns.RunUntil.X_success/X_revert/X_success_of_halting/X_Z_error/X_step_error— a block plus its terminating instruction determinesX's answer.RunUntil.trans_step/X_eq_trans_step— chain block, boundary instruction, next block, which is what a control-flow path actually composes.Stop conditions are just predicates on the opcode;
CallFamilyandBlockEndare supplied, and
stopOrHaltingwidens any of them to also stop at halts,since
Xstops there whether or not the caller asked.Executable driver
xRunUntilwalks the same block and is validated in both directions —xRunUntil_soundandxRunUntil_complete— so it is a decision procedure forRunUntil, and a concrete block can be discharged by evaluation while stillyielding a theorem about
X.Trace-erased runs and tactics
XReachesisXRunswith the trace existentially quantified — the form with noindex a tactic would have to invent.
x_steppeels one instruction from amatching
XStepAthypothesis,x_blockpeels the whole block, andx_collapsecarries that through to an
Xgoal. They search the local context and nothingelse, so they cannot invent a step that was never proved.
Non-vacuity
Every relation introduced here is inhabited beyond its reflexive/stopping cases,
proved symbolically for an arbitrary pre-state:
xReaches_one_JUMPDEST,runUntil_one_JUMPDEST. The tactics are exercised rather than merely defined:xReaches_two_steps,xReaches_three_steps,X_eq_of_two_steps.Notes for review
main(9d8eda70). Depends only on merged F4a — nooverlap with the F4b (feat(evm): decompose X and Ξ into runs #6) or F4c (feat(evm): F4c observation and frame lemmas #7) draft PRs, and no file they touch is
touched here.
sorry, noadmit, nonative_decide, no project-level axiom.#print axiomson every result reports onlypropext,Classical.choice,Quot.sound.Test plan
lake buildgreen on the whole library#print axiomsclean on all new resultsZ_ok_stateguard-peeling count againstZ's body