Phase 1C #3: Prove spec-functions-aware return-binding helper preservation (StmtListDirectInternalHelperAssignStepInterfaceWithInternals)

[Th0rgal]

Summary

• add an assign-only, spec-functions-aware head-step catalog for direct Stmt.internalCallAssign occurrences at their prefix-derived scopes
• derive StmtListDirectInternalHelperAssignStepInterfaceWithInternals by the same scoped list recursion used by predecessor PR Phase 1C #2: Prove spec-functions-aware helper-call preservation (StmtListDirectInternalHelperCallStepInterfaceWithInternals) #2223
• register the new public theorem in the generated axiom audit

Verification

• fresh lake build PrintAxioms (2569 jobs, exit 0; no cached terminal-job replay)
• lake env lean PrintAxioms.lean (exit 0)
• lake build (2228 jobs, exit 0)
• generated totals: 6034 theorems/lemmas (4181 public, 1853 private, 0 sorry'd)
• no escape tokens in the source diff beyond the generated 0 sorry'd total header
• source-bundle digests match the pinned predecessor base

Continues PR #2223 and addresses issue #2080, Phase 1C case 3/4.

---

Note

Low Risk
Additive Lean proof scaffolding only; no runtime, auth, or compilation behavior changes.

Overview
Adds DirectInternalHelperAssignHeadStepCatalogWithInternals, an assign-only catalog that holds CompiledStmtStepWithHelpersAndHelperIRWithInternals witnesses for each Stmt.internalCallAssign at its prefix-derived scope (via StmtOccursAtScope), matching how those heads compile through compileInternalCallArgs ... spec.functions rather than the empty-internals path in the legacy catalog.

Proves stmtListDirectInternalHelperAssignStepInterfaceWithInternals_of_headStepCatalog, which walks the function body with the same scoped list recursion as the void-call WithInternals theorem from #2223 and lifts the catalog into StmtListDirectInternalHelperAssignStepInterfaceWithInternals for the whole body.

Registers the new public theorem in the generated PrintAxioms audit (6034 total lemmas).

^{Reviewed by Cursor Bugbot for commit 4de363d. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview	Aug 2, 2026 12:25am

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot 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_84eb144d-af37-459e-bca8-90cdca75e16d)

[github-actions]

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 highlights

Error: review failed: all 2 file review(s) failed — check your LLM configuration and API key

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: 82 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status error; comments 0; files unknown; tokens 0; tool calls 0; warnings 0; duration 922s
• Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+79/-0), PrintAxioms.lean (+2/-1)

Pilot mode: advisory only. Codex Review remains the merge gate.

[Th0rgal]

Codex current-head verdict for 4de363d: APPROVE. (GitHub prevents the authenticated PR-author identity from recording a formal APPROVED review.)

Reviewed the complete diff against verified parent 9e8bb82. The change is confined to Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+79) and generated PrintAxioms.lean (+2/-1; registry count 6033→6034). DirectInternalHelperAssignHeadStepCatalogWithInternals correctly mirrors PR #2223 for Stmt.internalCallAssign, preserves prefix-derived StmtOccursAtScope indexing, and requires CompiledStmtStepWithHelpersAndHelperIRWithInternals. The list-interface theorem uses the expected induction/generalizing recursion, routes internalCallAssign to the catalog witness, rejects other constructors via simp [stmtTouchesDirectInternalHelperAssignSurface], and embeds the tail with StmtOccursAtScope.tail. No changed-source sorry, admit, or axiom escape tokens were introduced.

Non-source/generated rows are limited to the PrintAxioms theorem registration and generated total comment; both are consistent and purely additive. Existing remote-build evidence is sufficient. The lone OCR semantic review failure is classified as retryable LLM/API-key infrastructure, not a source finding. GraphQL reviewThreads was empty at review time. No blocking correctness findings.

[Th0rgal]

@codex review

Current-head verdict: APPROVE for 4de363d4635758abe7cb766df53687aa68520f33 against base 9e8bb828309e4b924c45ac9b19bb56deef41063a.

The diff is confined to the writer milestone (+79 in Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean, +2/-1 in PrintAxioms.lean). The assign-only catalog uses CompiledStmtStepWithHelpersAndHelperIRWithInternals for the exact Stmt.internalCallAssign names calleeName args occurrence at its prefix-derived scope. The list-interface theorem mirrors the predecessor's scope-generalized recursion, constructor routing, and tail occurrence embedding. PrintAxioms.lean adds the expected theorem and advances 6033→6034 (4181 public, 1853 private, 0 sorry'd). No new sorry, admit, or axiom occurs in changed source. No unresolved, non-outdated P1/P2 review threads were found. Non-source CI rows described on the PR do not indicate a source correctness defect.

[Th0rgal]

@codex review

Exact-head Codex review for 4de363d4635758abe7cb766df53687aa68520f33 against base 9e8bb828309e4b924c45ac9b19bb56deef41063a.

VERDICT: CLEAN

The assign-only spec-functions-aware catalog uses CompiledStmtStepWithHelpersAndHelperIRWithInternals for Stmt.internalCallAssign, preserves prefix-derived StmtOccursAtScope indexing, and the list-interface proof mirrors the predecessor recursion and tail embedding. The diff is confined to Calls.lean (+79) and generated PrintAxioms.lean (+2/-1), including the 6033→6034 registration update. No new sorry, admit, or axiom occurs in changed source. No unresolved non-outdated technical review threads were found.

[chatgpt-codex-connector]

Codex Review: Something went wrong. Try again later by commenting “@codex review”.

Unknown error

ℹ️ 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".

[Th0rgal]

@codex review

COMMENTED (formal APPROVE unavailable because GitHub does not allow the PR author to approve their own PR) — clean current-head review at 4de363d4635758abe7cb766df53687aa68520f33 against parent 9e8bb828309e4b924c45ac9b19bb56deef41063a.

The diff is confined to the expected changes (Calls.lean +79; PrintAxioms.lean +2/-1). The assign-only WithInternals catalog uses CompiledStmtStepWithHelpersAndHelperIRWithInternals for Stmt.internalCallAssign, preserves prefix-derived StmtOccursAtScope indexing, and the list-interface recursion mirrors the predecessor call-only theorem with correct constructor routing and tail embedding. PrintAxioms.lean adds the expected theorem and updates 6033 to 6034. No new sorry, admit, or axiom occurs in changed source. GraphQL reports zero unresolved non-outdated review threads. No source-correctness findings.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Swish!

Reviewed commit: 4de363d463

ℹ️ 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".

[Th0rgal]

APPROVE