proof: add helper IR WithInternals body seam

[Th0rgal]

Refs #2080

Base / dependency

Stacked on PR #2113 (paloma/issue-2080-structural-head-witnesses). Do not merge until predecessor stack is merged/green.

Live predecessor stack at creation:

• proof: make scope lift helper-world parametric #2108 open/clean: paloma/issue-2080-parametric-scope-lift
• proof: add direct helper WithInternals interfaces #2111 open/clean: paloma/issue-2080-direct-withinternals
• proof: add structural helper WithInternals assembly #2112 open/clean: paloma/issue-2080-structural-withinternals
• proof: add structural WithInternals head witnesses #2113 open/clean: paloma/issue-2080-structural-head-witnesses

Summary

• Added the WithInternals execution sibling for the helper-IR generic list theorem, preserving spec.functions through compile reconstruction and executing with execIRStmtsWithInternals.
• Added body-level preservation wrappers that consume StmtListGenericWithHelpersAndHelperIRWithInternals directly.
• Added the first split-interface body consumer for mixed WithInternals helper-free/direct/expr/structural/residual witnesses, avoiding the legacy/default-empty helper-world list seam for that path.
• Refreshed PrintAxioms.lean and proof-length allowlist entries for the new mechanical proof seams.

Validation

• lean-slot lake build Compiler.Proofs.IRGeneration.GenericInduction.Helpers ✅
• lean-slot lake build Compiler.Proofs.IRGeneration.GenericInduction.Main ✅
• lean-slot lake build Compiler.Proofs.HelperStepProofs ✅
• python3 scripts/generate_print_axioms.py --check ✅
• python3 scripts/check_proof_length.py ✅
• git diff --check ✅
• Strict touched-file proof-hole scan for sorry/admit/axiom declarations ✅

Remaining #2080 interface/gate

This slice adds the execution sibling and a body-level mixed WithInternals consumer. The top-level function path still has default-empty helper-world compile hypotheses in existing compiler wrappers, so the next slice should bridge function compilation/body compile facts to model.functions where locally coherent, then thread this body consumer into the function-level preservation route.

---

Note

Low Risk
Lean proof-only changes that extend existing IR-generation induction patterns; no runtime, auth, or deployment behavior.

Overview
Adds the spec.functions-aware execution path for helper-IR generic statement lists, so compile and execIRStmtsWithInternals stay in the real helper world instead of the legacy default-empty list seam.

In Helpers, new step/result theorems exec_compileStmtList_generic_with_helpers_and_helper_ir_with_internals_sizeOf_extraFuel_* mirror the existing helper-IR fuel induction but take StmtListGenericWithHelpersAndHelperIRWithInternals and compile with spec.functions.

In Main, new body preservation theorems consume that witness directly (supported_function_body_correct_from_exact_state_generic_helper_steps_and_helper_ir_with_internals and a split-interface variant that assembles helper-free/direct/expr/structural/residual WithInternals step interfaces into one generic list witness while keeping body compile in model.functions.

PrintAxioms and check_proof_length are updated for the four new public lemmas and their long mechanical proofs.

^{Reviewed by Cursor Bugbot for commit 0754fca. 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, Comment	Jul 7, 2026 4:47am

[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_58005f0c-bfce-4244-af55-a90c2843028e)

[Th0rgal]

Review/validation update from fallback merge worker:

• Diff reviewed against stacked base proof: add structural WithInternals head witnesses #2113 (paloma/issue-2080-structural-head-witnesses). The PR-local commits are scoped to the expected helper-IR WithInternals proof seam and generated proof metadata.
• Local validation passed:
  • lean-slot lake build Compiler.Proofs.IRGeneration.GenericInduction.Helpers
  • lean-slot lake build Compiler.Proofs.IRGeneration.GenericInduction.Main
  • lean-slot lake build Compiler.Proofs.HelperStepProofs
  • python3 scripts/generate_print_axioms.py --check
  • python3 scripts/check_proof_length.py
  • git diff --check origin/pr-2113..HEAD
• No PR-added sorry/admit/axiom declarations found; the only added sorry text is the generated zero-sorry audit summary line.
• GitHub review threads: none unresolved.

Not merging yet. Exact blockers:

1. Stack policy: predecessor PRs proof: make scope lift helper-world parametric #2108, proof: add direct helper WithInternals interfaces #2111, proof: add structural helper WithInternals assembly #2112, and proof: add structural WithInternals head witnesses #2113 are still open; proof: add helper IR WithInternals body seam #2114 must wait until the required predecessor stack is merged/green and GitHub allows a clean merge under the intended base.
2. CI is still pending on proof: add helper IR WithInternals body seam #2114 at the latest check (compiler-audits, compiler-regressions, foundry-* jobs in progress), so the PR is still UNSTABLE.
3. Cursor Bugbot did not run because the usage limit was reached; no Bugbot findings are present to resolve, but this is not a completed Bugbot review.