feat(evm): decompose X and Ξ into runs - #6
Draft
Th0rgal wants to merge 2 commits into
Draft
Conversation
`EVM.Proof.Execution` gives six sufficient conditions for one iteration of `X` and chains the non-halting ones into `XRuns`. That leaves two gaps: the cases are never shown to be exhaustive, and `Ξ` is not covered at all. `X_succ_complete` closes the first: every `X (fuel + 1)` is one of the five positive-fuel cases, so `cases` on `XOneStep` is a complete case split. On top of it, `X_decompose` extracts from an arbitrary `X` a maximal `XRuns` prefix ending in a configuration that takes no further non-halting iteration, and `XStuck.X_terminal` shows such a configuration is out of fuel, raises, or halts — ruling the continuing case out rather than merely not choosing it. `Ξ_succ_eq` closes the second by proving `Ξ` is exactly `X` on the fresh state it builds, which transports every `X`-level result to the transaction level. The `XRuns` endings `X_revert`, `X_exception` and `X_stepError` complete `X_success`, and each gets a `Ξ` counterpart. `Ξ_empty_code` keeps the conditional `Ξ` theorems honest: a call into an account with no code decodes to `X`'s default `STOP`, halts, and returns a success, so their hypotheses are inhabited. Additive: one import plus one new module. No `sorry`, no new axiom, no `native_decide`; all new results reduce to propext/Classical.choice/Quot.sound.
3 tasks
Keep F4b Interpreter (X / Ξ / runs) and F4d Block (runUntil) both imported.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Builds on F4a (
EvmYul.EVM.Proof.Execution: theX6-case split andXRuns), which landed in #5. Additive: one import inEvmYul.leanplus one new module. F4a is not modified.What this closes
F4a's six theorems are sufficient conditions — each says that if such-and-such holds,
Xdoes such-and-such. That leaves two gaps, andΞwas not covered at all.The cases are exhaustive.
X_succ_completeshows everyX (fuel + 1)is one of five cases, packaged asXOneStep. Each constructor carries both the side conditions and the resulting value ofX, socaseson it is a complete case split that also supplies the equation for its branch.Every
Xis a maximal run plus one terminal event.X_decomposeextracts from an arbitraryXanXRunsprefix ending in a configuration that takes no further non-halting iteration.XStuck.X_terminalthen shows such a configuration is out of fuel, raises, or halts — theprogresscase is ruled out viaX_succ_completerather than merely not chosen, which is what makes the run maximal.X_runs_terminaladds thattrace.length + rem = fuel, so the fuel is accounted for exactly.ΞisXon a fresh state.Ξ_succ_eqproves that equation, transporting everyX-level result to the transaction level.xiState/xiJumps/xiResultmirror the state, jump table and result narrowing thatΞbuilds;Ξ_succ_eqis what validates them, so drift breaks the proof rather than passing silently.The
XRunsendingsX_revert,X_exceptionandX_stepErrorcomplete F4a'sX_success, and each gets aΞcounterpart (Ξ_of_XRuns_*, includingoutOfFuel).Ξ_decomposeis the transaction-level decomposition.Non-vacuity
The
Ξ_of_XRuns_*theorems are conditional, so they would hold trivially if nothing satisfied their hypotheses.Ξ_empty_codedischarges them for a real transaction: a call into an account with no code decodes past the end of the code toX's defaultSTOP, halts, and returns a success with empty output. The witness is symbolic in the account map, substate and execution environment — only the code is fixed — so it does not depend on evaluating a concrete machine state.Verification
lake buildexit 0.sorry, no project axiom, nonative_decide.#print axiomson all 15 new results: each depends only on[propext, Classical.choice, Quot.sound].Draft — not for merge yet.