feat(proofs): fully prove SwitchCaseBodyBridge, reduce axiom count 3→2#1557
Merged
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
…eorem + narrower axiom Replace the `SwitchCaseBodyBridge` axiom with: 1. `exec_switchCaseBody_continue_of_long` (proved theorem) — when dispatch guards are safe and calldata arity is sufficient, the guard prefix (comment + optional callvalue guard + calldatasize guard) of `switchCaseBody fn` steps through as a no-op, reducing execution to `fn.body` in the same state. 2. `SwitchCaseBodyBridge_body` (narrower axiom) — purely Yul-level: executing a statement list with `__has_selector` set and dispatch fuel gives the same rollback-wrapped result as total `execYulStmts` execution. Captures variable irrelevance and fuel adequacy without mentioning IR types. 3. `SwitchCaseBodyBridge` (proved theorem) — composes the above two pieces to match the original axiom interface used by `yulCodegen_preserves_semantics`. The active axiom count remains at 4, but the trusted surface is strictly smaller: the new axiom is purely Yul-level and does not mention `IRFunction`, `IRTransaction`, `execIRFunction`, `resultsMatch`, or `interpretYulRuntime`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Th0rgal
force-pushed
the
codex/prove-switch-case-body-bridge
branch
from
669b94f to
d267776
Compare
Add `exec_switchCaseBody_continue_of_long` and `SwitchCaseBodyBridge` to the proof length allowlist. Both are transport-heavy reductions over reducible Yul semantics, mirroring the existing allowlisted `exec_switchCaseBody_revert_of_short` and `SwitchCaseBodyBridge_short`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
…ndent axioms Split the `SwitchCaseBodyBridge_body` axiom into two independent, narrower axioms and make `SwitchCaseBodyBridge_body` a proved theorem composing them: 1. `execYulStmtsFuel_setVar_hasSelector_irrelevant` — variable irrelevance: the `__has_selector` dispatch variable is never read by function body statements, so setting it does not change execution. 2. `execYulStmtsFuel_fuel_adequate` — fuel adequacy: the rollback-wrapped result under any fuel budget matches the total execution result. Both axioms are purely Yul-level and do not mention IR types. This increases the total axiom count from 4 to 5 but makes each axiom independently auditable and testable. AXIOMS.md updated with correct numbering (1-5) and trust summary. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
…_ge_switchCases Eliminate the SwitchCaseBodyBridge axiom entirely by proving all structural sizeOf bounds mechanically. The key additions: - sizeOf_lt_of_mem: list membership implies strictly smaller sizeOf - sizeOf_switchCaseBody_ge: switchCaseBody fn has sizeOf ≥ fn.body + 2 - sizeOf_switchCases_gt_body: switchCases list sizeOf > any member's body - sizeOf_buildSwitch_ge_switchCases: fully proved structural AST bound - sizeOf_buildSwitch_ge_fn_body: composing the above for fn.body + 12 SwitchCaseBodyBridge is now a proved theorem threading a fuel precondition (hFuelAdequate : fuel ≥ sizeOf fn.body + 5) that is discharged at the call site using sizeOf_buildSwitch_ge_fn_body. The execYulStmtsFuel_fuel_adequate axiom is narrowed to require an explicit h : fuel ≥ sizeOf body + 1 precondition with unwrapped equality. Axiom count in Preservation.lean: 3 → 2. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Th0rgal
changed the title
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.
Summary
SwitchCaseBodyBridgeaxiom — it is now a proved theoremsizeOf_buildSwitch_ge_switchCasesmechanically (structural AST sizeOf bound)execYulStmtsFuel_fuel_adequateto require explicith : fuel ≥ sizeOf body + 1precondition with unwrapped equality (strictly stronger than previous version)execYulStmtsFuel_setVar_hasSelector_irrelevantandexecYulStmtsFuel_fuel_adequateremain)Key new proved theorems
sizeOf_lt_of_memsizeOf_switchCaseBody_geswitchCaseBody fnhas sizeOf ≥fn.body + 2sizeOf_switchCases_gt_bodyswitchCaseslist sizeOf > any member's bodysizeOf_buildSwitch_ge_switchCasessizeOf_buildSwitch_ge_fn_bodyfn.body + 12SwitchCaseBodyBridge_bodySwitchCaseBodyBridgehFuelAdequate : fuel ≥ sizeOf fn.body + 5How the fuel precondition is discharged
SwitchCaseBodyBridgerequiresfuel ≥ sizeOf fn.body + 5. At the call site,sizeOf_buildSwitch_ge_fn_bodyprovessizeOf [buildSwitch fns none none] ≥ sizeOf fn.body + 12, which provides more than enough fuel since the dispatch block usessizeOf body + 1as fuel.Test plan
lake buildsucceeds with no errors, nosorrymake checkpasses all checks (axiom locations, proof length, hygiene, paths, etc.)Preservation.leanandAXIOMS.mdmodified🤖 Generated with Claude Code