Phase 1C #2: Prove spec-functions-aware helper-call preservation (StmtListDirectInternalHelperCallStepInterfaceWithInternals) - #2223
Conversation
…tListDirectInternalHelperCallStepInterfaceWithInternals) Direct internal-call heads compile their arguments through compileInternalCallArgs ... spec.functions, so the legacy DirectInternalHelperHeadStepCatalog witnesses — which record the default empty internal-function compiler argument — cannot be rewrapped into the WithInternals list interface. Add the spec-functions-aware sibling catalog DirectInternalHelperHeadStepCatalogWithInternals, which carries CompiledStmtStepWithHelpersAndHelperIRWithInternals witnesses directly, and assemble the exact WithInternals void-helper-call list interface from it via the existing helperCallNames-indexed list recursion. Registers the new theorem in the axiom audit (6032 -> 6033).
|
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_a4fdd157-8bac-4088-bc19-8e158c63f6e6) |
![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: 3e4b640e1a
ℹ️ 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".
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟢 No findings from the OCR first pass. Advisory only.
No comments generated. Looks good to me.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: medium-lean (router-v10)
- Changed files: 2 supported / 2 total; Lean 2, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 65 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 2; tokens 111265; tool calls 21; warnings 0; duration 243s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+62/-0), PrintAxioms.lean (+2/-1)
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_c5578418-8cd8-4493-8f34-e8cbf8d4172c) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 201b7b5320
ℹ️ 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".
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟠 1 finding(s) (1 low) — see inline comments.
✅ Posted 1 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: medium-lean (router-v10)
- Changed files: 2 supported / 2 total; Lean 2, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 86 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 1; files 2; tokens 185623; tool calls 27; warnings 0; duration 371s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+83/-0), PrintAxioms.lean (+2/-1)
Pilot mode: advisory only. Codex Review remains the merge gate.
| \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``` |
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_80240b17-5b74-401f-aab3-f20eac5d73c4) |
OpenCodeReview first-pass review🔁 Incomplete — this run did not finish and will retry on the same commit. Do not count it as review coverage. OCR produced no JSON output OCR stderr highlightsOCR pilot metrics & packet coverageOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
1 participant
Summary
Phase 1C case 2/4. Proves the
WithInternals(spec-functions-aware) counterpart of the void helper-call list interface merged in #2222:stmtListDirectInternalHelperCallStepInterfaceWithInternals_of_headStepCatalogWhy a new catalog rather than rewrapping the existing one
Direct internal-call heads compile their arguments through
compileInternalCallArgs ... spec.functions, so their compiled IR is not determined by the default empty internal-function compiler argument recorded byDirectInternalHelperHeadStepCatalog. The legacy.callwitness therefore cannot be rewrapped into theWithInternalsinterface — the dependency on the supplied internal-function list is visible at the type level.This PR adds the spec-functions-aware sibling
DirectInternalHelperHeadStepCatalogWithInternals, which carriesCompiledStmtStepWithHelpersAndHelperIRWithInternalswitnesses directly (both the voidcalland the return-bindingassignhalves), and assembles the exact list interface from it through the existinghelperCallNames-indexed list recursionstmtListDirectInternalHelperCallStepInterfaceWithInternals_of_internalCallSteps_of_helperCallNames.No interface weakening: the conclusion is the full
StmtListDirectInternalHelperCallStepInterfaceWithInternals, mirroring the merged case-1 theorem's shape.Axiom audit updated: 6032 -> 6033 theorems (4179 -> 4180 public), regenerated with
scripts/generate_print_axioms.py.Test plan
lake buildpasseslake build PrintAxiomspasses (fresh remote build, 2569 jobs, exit 0)scripts/generate_print_axioms.pyreproducesPrintAxioms.leanbyte-identicallyscripts/check_lean_hygiene.pypasses (0 sorry, 0 native_decide, 0 allowUnsafeReducibility)sorry,admit,axiom, or unsafe escapes in changed sourceNote
Low Risk
Proof-only additions in IR generation generic induction; no runtime, auth, or compiler behavior changes—only new Lean structures and one assembly theorem plus axiom audit.
Overview
Phase 1C case 2/4: proves the
WithInternalscounterpart of assemblingStmtListDirectInternalHelperCallStepInterfacefrom a head-step catalog, without weakening the conclusion.Because direct internal-call heads compile arguments via
compileInternalCallArgs ... spec.functions, the existingDirectInternalHelperHeadStepCatalogwitnesses (empty internal-function compiler path) cannot be rewrapped. The PR introducesDirectInternalHelperCallHeadStepCatalogWithInternals, indexed byStmtOccursAtScopeso the catalog only suppliesCompiledStmtStepWithHelpersAndHelperIRWithInternalsfor voidStmt.internalCallsites at the scopes that actually occur in the function body.stmtListDirectInternalHelperCallStepInterfaceWithInternals_of_headStepCatalogwalks the body list while trackingcurrentScope, pulling catalog witnesses only when the head is a direct internal call at an embedded occurrence.PrintAxioms.leanregisters the new public theorem (6032 → 6033 total).Reviewed by Cursor Bugbot for commit ed9e1cc. Bugbot is set up for automated code reviews on this repo. Configure here.