Phase 1C #4: Prove expression-position helper-call preservation (Expr.internalCall via Stmt.letVar)

[Th0rgal]

Summary

• proves expression-position helper-call preservation for Expr.internalCall through Stmt.letVar
• regenerates the PrintAxioms counter from 6034 to 6035
• completes Phase 1C case 4/4

References #2080 and predecessor cases #2222, #2223, and #2224.

Validation

• lake build PrintAxioms passed
• forbidden-token scan passed
• PrintAxioms counter regenerated: 6034 → 6035

---

Note

Low Risk
Proof-only Lean additions mirroring existing call/assign catalog patterns; no runtime, auth, or compiler behavior changes.

Overview
Adds Phase 1C expression-position plumbing so Stmt.letVar bindings of Expr.internalCall can feed the same helper-aware list induction as void-call and assign-call heads.

Introduces DirectInternalHelperExprCallHeadStepCatalogWithInternals, a scoped catalog of CompiledStmtStepWithHelpersAndHelperIRWithInternals witnesses for those letVar sites. stmtListDirectInternalHelperExprCallStepInterfaceWithInternals_of_headStepCatalog walks the function body (preserving prefix scopes via StmtOccursAtScope) and builds StmtListExprInternalHelperStepInterfaceWithInternals when a catalog and a coverage premise hold (every expr-helper surface hit is exactly letVar name (internalCall …)).

Registers the new theorem in PrintAxioms.lean (6034 → 6035 lemmas).

^{Reviewed by Cursor Bugbot for commit ff37d06. 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 8:31am

[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_88303684-9cf1-49f3-bd64-8f5f41182e24)

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: c05d5c159b

ℹ️ 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]

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: 75 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 (+72/-0), PrintAxioms.lean (+2/-1)

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

[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_00194e5c-8733-4fbc-9693-b12b6dd6a0ba)

[Th0rgal]

@codex review

The head has advanced with a focused fix for the existing P2 thread at Calls.lean. The dead parallel direct-expression interface was removed, and stmtListDirectInternalHelperExprCallStepInterfaceWithInternals_of_headStepCatalog now uses an explicit direct-form coverage premise to produce StmtListExprInternalHelperStepInterfaceWithInternals directly, closing the hexpr path into fullHelperAwareListWitnessWithInternals_of_allInterfaces. Please review the new exact head.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Another round soon, please!

Reviewed commit: ff37d06e56

ℹ️ 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]

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

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