proof: make scope lift helper-world parametric

[Th0rgal]

Summary

Continues #2080 after phase 13 / #2107.

This PR is stacked on #2107 and targets paloma/issue-2080-spec-functions-stmt-list. It should be reviewed/merged after the existing #2102 -> #2107 chain lands.

• make the FunctionBody.compileStmt_ok_any_scope_with_surface induction parametric over internalFunctions
• add public *_with_internals wrappers for statement and statement-list scope lifting
• add compileStmtList cons reconstruction/inversion helpers under an arbitrary internal helper world
• compose the new parametric scope lift with the phase-13 exact statement-list seam, producing compileStmtList_ok_of_stmtListGenericWithHelpersAndHelperIRWithInternals
• regenerate PrintAxioms.lean

Proof status

The internal-functions-parametric any-scope path now works for the StmtListGenericWithHelpersAndHelperIRWithInternals seam: exact spec.functions head compiles can be retargeted to the caller-provided scope and reconstructed as a compiled statement list under the same spec.functions world.

This does not close every legacy/default-empty consumer yet. The next dispatch should retarget remaining consumers of StmtListGenericWithHelpersAndHelperIR / helper-free compiled compatibility in InterfaceAssembly and adjacent call sites to the WithInternals witness where expression helper payloads enter, then continue removing default-empty seams that still rely on helper-free compatibility or runtimeContract.internalFunctions = []-style assumptions.

Validation

• lake env lean Compiler/Proofs/IRGeneration/FunctionBody/Stmt.lean && lake env lean Compiler/Proofs/IRGeneration/GenericInduction/ResultRelation.lean passed
• lean-slot lake build Compiler.Proofs.IRGeneration.FunctionBody.Stmt passed; Spark offload attempted and fell back locally after HTTP 403 (host_dir does not belong to this mission or an ancestor)
• lean-slot lake build Compiler.Proofs.IRGeneration.GenericInduction.ResultRelation passed with the same Spark 403 fallback
• lean-slot lake build Compiler.Proofs.HelperStepProofs passed with the same Spark 403 fallback
• lean-slot lake build Compiler.Proofs.IRGeneration.FunctionBody.Stmt Compiler.Proofs.IRGeneration.GenericInduction.ResultRelation Compiler.Proofs.HelperStepProofs passed with the same Spark 403 fallback
• python3 scripts/lean_lint.py --only lean_hygiene passed: 0 debug commands in proofs, 0 allowUnsafeReducibility, 0 sorry, 0 native_decide in proofs
• python3 scripts/lean_lint.py --only proof_length passed
• python3 scripts/generate_print_axioms.py --check passed
• lean-slot lake build PrintAxioms passed with the same Spark 403 fallback
• lake env lean PrintAxioms.lean > axiom-report-raw.log 2>&1 passed
• make check passed fully: Ran 607 tests in 308.106s, OK, All checks passed.

---

Note

Medium Risk
Changes are confined to Lean proof infrastructure around compilation and helper-aware IR seams; mistakes could weaken verified compile/scope claims but do not touch runtime execution paths directly.

Overview
Makes statement compilation proofs respect an arbitrary internal-helper world (spec.functions) instead of assuming an empty helper table, and wires that through the WithInternals statement-list seam.

FunctionBody now threads internalFunctions through the compileStmt_ok_any_scope_with_surface induction (including compileExprWithInternals and list compilation). It adds *_with_internals scope-lift lemmas for single statements and lists, plus compileStmtList cons reconstruction and inversion under that same helper world. Existing entry points still call the aux lemma with [].

ResultRelation introduces StmtListExprInternalHelperStepInterfaceWithInternals and compileStmtList_ok_of_stmtListGenericWithHelpersAndHelperIRWithInternals, which lifts exact-scope generic witnesses to a caller inScopeNames by retargeting each head compile via the new scope API and rebuilding the list with spec.functions.

InterfaceAssembly adds assembly from the WithInternals expression-helper list interface into StmtListGenericWithHelpersAndHelperIRWithInternals. HelperStepProofs adds matching cons/whole-list builders for expression-helper bridges and refactors stmtListGenericWithHelpersAndHelperIRWithInternals_of_exprHeadStepBridges to route through that path (with an explicit “all heads are expression-helper surface” hypothesis). PrintAxioms is regenerated.

^{Reviewed by Cursor Bugbot for commit a29959d. 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 6, 2026 3:47pm

[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_08066779-d64c-4d5f-8415-02ee523fb8cc)

[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_8c03b631-4e2d-407f-a746-73c6d9bedd85)

[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_797323e3-5e4d-4294-af41-df52fdc3b9d5)

[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_388ed252-17fa-40e1-bb20-dea362f4f596)