proof: bridge compiled helper-body shape for rank-0 seam#2153
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_e13eaa1f-08c2-473c-9ef4-452499a8611d) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 4 finding(s) · 3 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 3 Lean file(s), 302 changed supported line(s). Scout model ranked 4/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
Warnings
OCR pilot metrics
Packet coverage
Pilot mode: advisory only. Codex Review remains the merge gate. Inline findings that could not be posted
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_175fbe0f-5a32-4786-8dd0-679251f74b83) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 4 finding(s) · 3 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 3 Lean file(s), 392 changed supported line(s). Scout model ranked 4/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
Warnings
OCR pilot metrics
Packet coverage
Pilot mode: advisory only. Codex Review remains the merge gate. Inline findings that could not be posted
|
![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: cd75517bc2
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_b55f011b-c53e-4cb1-b192-e228fc41ef42) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 6 finding(s) · 3 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 3 Lean file(s), 394 changed supported line(s). Scout model ranked 6/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
Warnings
OCR pilot metrics
Packet coverage
Pilot mode: advisory only. Codex Review remains the merge gate. Inline findings that could not be posted
|
# Conflicts: # PrintAxioms.lean
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_d3f13219-a908-4bdb-9b62-c88a1fada768) |
|
Codex Review: Didn't find any major issues. Bravo. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
OpenCodeReview first-pass reviewStatus: completed_with_errors · Mode: medium-lean · 1 finding(s) · 3 files · 1114554 tokens · 60 tool calls 📝 1 additional positioned finding(s) omitted from inline comments to avoid spam. Summary-only findings
Warnings
OCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
|
@codex review |
|
Codex Review: Didn't find any major issues. Keep them coming! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
| \n### CI Failure Hints\n\nFailed jobs: `build-compiler-binaries`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
…per-body-seam # Conflicts: # PrintAxioms.lean
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_34def95b-0bdf-4df6-8eb7-e5faa8645877) |
|
@codex review |
|
Codex Review: Didn't find any major issues. What shall we delve into next? Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
OpenCodeReview first-pass reviewStatus: completed_with_errors · Mode: medium-lean · 3 finding(s) · 3 files · 753585 tokens · 46 tool calls 📝 3 additional positioned finding(s) omitted from inline comments to avoid spam. Summary-only findings
Warnings
OCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
…per-body-seam # Conflicts: # PrintAxioms.lean
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_b1e1e959-4da1-42d9-b8fb-e2ab4a05e790) |
|
@codex review |
|
Codex Review: Didn't find any major issues. Keep it up! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
OpenCodeReview first-pass reviewStatus: completed_with_errors · Mode: medium-lean · 0 finding(s) · 3 files · 425983 tokens · 50 tool calls Some files could not be reviewed due to errors. Warnings
OCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_ffc37ecf-da9e-4326-aa5f-e5f8c0c7cbc1) |
OpenCodeReview first-pass reviewStatus: completed_with_errors · Mode: medium-lean · 0 finding(s) · 3 files · 399567 tokens · 34 tool calls Some files could not be reviewed due to errors. Warnings
OCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
1 participant
Summary
Compiler/Proofs/IRGeneration/HelperBodyBridge.leanwith conservative rank-0 helper-body predicates:stmtUsesReturnFamily/stmtListUsesReturnFamilystmtUsesStop/stmtListUsesStopcompileStmtWithFork_internal_shape_irrelevant_of_returnFreecompileStmtListWithFork_internal_shape_irrelevant_of_returnFreecompileInternalFunction_body_eq_external_of_returnFreefindInternalFunction?_some_eq_compiledHelper_of_witnessfindInternalFunction?_external_body_of_witness_returnFreeempty_void_helper_body_compile_shape_irrelevant_regressionPrintAxioms.leanand keeps the existing proof-length allowlist current.Refs #2080
Semantic Seam Status
This PR now consumes the existing exact helper lookup theorem
findInternalFunction?_exact_of_compileInternalFunction_mem_uniquethroughfindInternalFunction?_some_eq_compiledHelper_of_witness, with the runtime-table uniqueness hypothesis explicit in the theorem signature. It also composes that lookup with the return-free body-shape lemma infindInternalFunction?_external_body_of_witness_returnFree.The remaining blocker for the full public theorem
execIRInternalFunctionWithInternals_obeys_internal_helper_summaryis no longer helper-table lookup. It is the call-boundary semantic interface betweenexecIRInternalFunctionWithInternalsand the existing generic body theorem:execIRInternalFunctionWithInternalsenters through private interpreter boundary operationsprepareInternalCalleeState,restoreCallerVars, andinternalReturnValuesinCompiler/Proofs/IRGeneration/IRInterpreter.lean:353-365.supported_function_body_correct_from_exact_state_generic_with_helpers,Compiler/Proofs/IRGeneration/GenericInduction/Main.lean:1836) reasons aboutexecStmtListWithHelpersversusexecIRStmts, with an explicit source binding list and a caller-supplied IR state.SourceSemantics.bindInternalArgs, and that restoring caller vars preserves the world relation while void return extraction yields[].Recommended next consumption step: add that internal-call-boundary state lemma in
IRInterpreter.leanor a nearby proof module, then compose it withfindInternalFunction?_external_body_of_witness_returnFreeand the existing generic body theorem to proveexecIRInternalFunctionWithInternals_obeys_internal_helper_summaryfor void return-free/stop-free helpers. The remaining external obligation after that is discharging the explicithuniqueruntime-table uniqueness hypothesis for compiled contracts.Validation
git diff --checkpassedlean-slot lake build Compiler.Proofs.IRGeneration.HelperBodyBridgepassedlean-slot lake build Compiler.Proofs.IRGeneration.HelperBodyBridge PrintAxiomspassedpython3 scripts/generate_print_axioms.py --checkpassedpython3 scripts/check_proof_length.pypassedrg -n "\\b(sorry|admit|axiom)\\b" Compiler/Proofs/IRGeneration/HelperBodyBridge.lean || trueproduced no matchesCommit SHA:
2900c9efNote
Low Risk
Proof-only additions to the compiler verification layer with no runtime or compilation behavior changes; risk is limited to proof maintenance and axiom inventory accuracy.
Overview
Adds
Compiler/Proofs/IRGeneration/HelperBodyBridge.leanwith conservative syntactic predicates (stmtUsesReturnFamily,stmtUsesStop, and list forms) and proofs that internal-return compilation parameters do not change emitted Yul when helper bodies avoid return-family statements.The main lemmas show successful
compileInternalFunctionbodies matchcompileStmtListWithForkwith[] false, and thatfindInternalFunction?on aSupportedCompiledInternalHelperWitnessagrees with that external body shape (via the existingfindInternalFunction?_exact_of_compileInternalFunction_mem_unique, with an explicit runtime-tablehuniquepremise). A small void-helper regression instantiates the list irrelevance theorem for empty bodies.PrintAxioms.leanimports the module and registers six new public theorems;scripts/check_proof_length.pyallowlistscompileInternalFunction_body_eq_external_of_returnFree.Reviewed by Cursor Bugbot for commit b2a1826. Bugbot is set up for automated code reviews on this repo. Configure here.