proof: bridge function internals body compile

[Th0rgal]

Base / dependency

Stacked on #2114 (paloma/issue-2080-helper-ir-withinternals), which is still open/mergeable/green. Do not merge until predecessor stack is merged/green.

Summary

• Add a parametric compileFunctionSpec shape bridge that preserves caller-provided ADT/internal-helper environments through to the body compileStmtList fact.
• Add a function-level bridge that reconstructs the model.functions body compile fact from helper-aware function compilation and threads the split WithInternals body consumer into the function proof path.
• Refresh PrintAxioms.lean and add a proof-length allowlist entry for the interface-heavy bridge after factoring the state/binding plumbing into private helpers.

Validation

• lean-slot lake build Compiler.Proofs.IRGeneration.FunctionShape Compiler.Proofs.IRGeneration.Function passed.
• lean-slot lake build Compiler.Proofs.IRGeneration.Function passed after decomposition.
• lean-slot lake build Compiler.Proofs.HelperStepProofs passed.
• lean-slot lake build Compiler.Proofs.IRGeneration.Contract passed.
• python3 scripts/generate_print_axioms.py --check passed.
• python3 scripts/check_proof_length.py passed.
• git diff --check passed.
• No sorry, admit, or axiom in touched proof files.

Refs #2080

Remaining #2080 gate

The full function-level retarget still needs the compiled-side execIRFunctionWithInternals param-loading/function execution bridge, so whole-contract dispatch can consume the helper-rich function theorem without falling back through default-empty helper-world/conservative-extension wrappers.

---

Note

Low Risk
Additive, machine-checked proof lemmas in IR generation only; no runtime or auth behavior changes.

Overview
Adds proof infrastructure for #2080 so function-level correctness can use helper-rich compileFunctionSpec facts instead of the legacy empty ADT/helper world.

FunctionShape.compileFunctionSpec_ok_components_with_internals mirrors the existing compileFunctionSpec_ok_components decomposition but threads caller adtTypes and internalFunctions through to the body compileStmtList success fact.

supported_function_body_with_internals_goal_of_compileFunctionSpec_with_internals is the main entry: from a successful helper-aware compile plus the split WithInternals step interfaces, it produces SupportedFunctionBodyWithHelpersAndHelperIRPreservationGoal with param binding state already wired. Three private lemmas factor out scope names, runtime IR alignment, and binding equality from bindSupportedParams.

PrintAxioms.lean and scripts/check_proof_length.py are updated for the new public theorem and allowlist entry.

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

[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_3d40ca88-6b75-43be-87f4-ca206c2777c2)

[Th0rgal]

Review/validation update from Codex fallback merge gate:

• Reviewed the PR-local diff against stacked base proof: add helper IR WithInternals body seam #2114 (paloma/issue-2080-helper-ir-withinternals). I did not find a trivial code issue to patch.
• Local validation passed:
  • lean-slot lake build Compiler.Proofs.IRGeneration.FunctionShape Compiler.Proofs.IRGeneration.Function
  • 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/2114...HEAD
• GitHub CI is green on proof: bridge function internals body compile #2115 at head 7e600a54f67ef66e754f2bbcab8be15d9a1719d3.
• GitHub review threads: none.
• Cursor Bugbot did not produce findings; the run reports usage limit reached.

Not merging. Exact blocker: stack policy/base dependency. #2115 is stacked on #2114, and the predecessor stack #2111, #2112, #2113, and #2114 is still open. Per the PR body and merge policy, #2115 must wait until the required predecessor stack is merged/green.