proof: bridge function exec with internals

[Th0rgal]

Base / dependency

Stacked on paloma/issue-2080-function-withinternals-bridge / PR #2115, which is still open and clean at PR creation time. This continues the #2080 L2 proof-tier stack after phase 20.

Do not merge until predecessor stack is merged/green.

Summary

• Add the execIRStmtsWithInternals append/prefix bridge needed to run generated ABI param loads before helper-aware compiled bodies.
• Add exec_genParamLoads_supported_then_extraFuel_withInternals and exec_compiledFunctionIR_withInternals_of_body_extraFuel, with the generated param-load prefix disjointness kept explicit.
• Add the direct function-level theorem supported_function_correct_with_helper_proofs_body_goal_with_internals, consuming SupportedFunctionBodyWithHelpersAndHelperIRPreservationGoal and producing preservation against execIRFunctionWithInternals directly.
• Add a contract-level API consumer wrapper compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal.
• Refresh PrintAxioms.lean and proof-length metadata for the new bridge theorems.

Validation

• lean-slot lake build Compiler.Proofs.IRGeneration.FunctionShape Compiler.Proofs.IRGeneration.Function - passed
• lean-slot lake build Compiler.Proofs.IRGeneration.Function - passed
• lean-slot lake build Compiler.Proofs.IRGeneration.Contract - passed
• lean-slot lake build Compiler.Proofs.HelperStepProofs - passed
• python3 scripts/generate_print_axioms.py --check - passed
• python3 scripts/check_proof_length.py - passed
• git diff --check - passed
• Touched proof-file scan found no new sorry, admit, or axiom declarations; matches are comments/generated audit text only.

Remaining #2080 gate

This PR exposes the first direct function-level execIRFunctionWithInternals path for exact helper-aware body goals. Whole-contract dispatch still needs a follow-up retarget that supplies the generated param-load disjointness/naming invariant and threads this direct function theorem through selector dispatch instead of the existing conservative-extension wrappers.

Refs #2080

---

Note

Low Risk
Changes are confined to Lean correctness proofs and audit metadata; no compiler runtime, auth, or execution semantics outside the proof layer.

Overview
Adds #2080 phase 21 proof infrastructure so helper-aware function correctness can be stated against execIRFunctionWithInternals when callers already discharge the exact helper-IR body goal, instead of a manual conservative-extension equality.

New execution lemmas thread generated ABI genParamLoads under execIRStmtsWithInternals (prefix/append, param-load bridge, compiled-function fuel alignment). supported_function_correct_with_helper_proofs_body_goal_with_internals packages source semantics, compilation shape, and that body goal into sourceResultMatchesIRResult for execIRFunctionWithInternals. compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal exposes the same on the contract API, with YulStmtListCallsDisjointFromInternalTable on genParamLoads as the remaining explicit premise.

PrintAxioms.lean and scripts/check_proof_length.py are updated for the new public theorems.

^{Reviewed by Cursor Bugbot for commit d95f99d. 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 1:02pm

[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_1465f991-afad-48ea-aecb-a605955c6dff)

[Th0rgal]

Codex fallback review checked the isolated #2116 diff against paloma/issue-2080-function-withinternals-bridge.

Review summary:

• The new direct WithInternals function bridge keeps the generated ABI param-load disjointness as an explicit premise and consumes the exact helper-aware body execution goal, so it does not introduce a new whole-function conservative-extension assumption on this path.
• I did not find a proof-soundness issue in the added prefix execution/consumer threading.
• No unresolved GitHub review threads were present; Bugbot did not run because Cursor reported a usage limit.
• Local checks completed: git diff --check, touched-file sorry/admit/axiom grep, and python3 scripts/check_proof_length.py passed. A local Lean build was started but stopped after GitHub CI had built the relevant proof job and merge was already blocked by policy.

Merge is blocked by policy because this stacked PR targets paloma/issue-2080-function-withinternals-bridge, and predecessor PR #2115 is still open: #2115

Additional current check blocker: build-compiler-binaries is still in progress on https://github.com/lfglabs-dev/verity/actions/runs/28868193696/job/85625122573

Blocked on open predecessor PR #2115 and pending build-compiler-binaries.