proof: thread spec functions through stmt list seam

[Th0rgal]

Continues #2080 as the next proof-tier slice after phase 12 / #2106.

Stacked on #2106 (paloma/issue-2080-spec-functions-stmt-witness) because #2106 and the earlier #2102-#2105 chain are still open. Please review/merge this after #2106.

What changed

• Add compileStmtList_cons_eq_ok_with_internals, a narrow internal-functions-parametric cons reconstruction lemma for compileStmtList.
• Add StmtListGenericWithHelpersAndHelperIRWithInternals, a spec-functions-aware statement-list seam whose heads carry CompiledStmtStepWithHelpersAndHelperIRWithInternals.
• Add exact-scope reconstruction theorem compileStmtList_ok_of_stmtListGenericWithHelpersAndHelperIRWithInternals_exact, compiling statement lists with spec.functions.
• Compose the phase-12 ExprInternalHelperHeadStepBridgeWithInternals witness through the new list seam with cons and all-heads assemblers.
• Regenerate PrintAxioms.lean for the new theorem declarations.

Current blocker / next API

This closes exact-scope list reconstruction for the spec.functions world. Full replacement of compileStmtList_ok_of_stmtListGenericWithHelpersAndHelperIR still needs an internalFunctions-parametric version of FunctionBody.compileStmt_ok_any_scope_with_surface / compileStmtList_ok_any_scope_with_surface, because the existing scope-lift proof recursively hardcodes the default empty internal-function world.

Validation

• lake env lean Compiler/Proofs/IRGeneration/GenericInduction/ResultRelation.lean
• lake env lean Compiler/Proofs/HelperStepProofs.lean
• lean-slot lake build Compiler.Proofs.IRGeneration.GenericInduction.ResultRelation
• lean-slot lake build Compiler.Proofs.HelperStepProofs
• python3 scripts/lean_lint.py --only lean_hygiene
• python3 scripts/lean_lint.py --only proof_length
• make check

Note: lean-slot attempted Spark offload but Spark returned HTTP 403 for this isolated worktree path, so the builds ran locally and passed.

---

Note

Low Risk
Additive Lean proof infrastructure only; no runtime, auth, or compiler executable changes. Residual risk is localized to formal verification maintenance and the documented gap before full list-level scope lifting.

Overview
Continues the #2080 helper/spec-functions proof tier by wiring statement lists through spec.functions instead of the default empty internal-function compile world.

ResultRelation.lean introduces StmtListGenericWithHelpersAndHelperIRWithInternals (list-level witness with CompiledStmtStepWithHelpersAndHelperIRWithInternals heads), compileStmtList_cons_eq_ok_with_internals (cons reconstruction when internalFunctions is threaded), and compileStmtList_ok_of_stmtListGenericWithHelpersAndHelperIRWithInternals_exact (from that witness, compileStmtList succeeds at the same scope with spec.functions). Arbitrary-scope lifting of the legacy compileStmtList_ok_of_stmtListGenericWithHelpersAndHelperIR is explicitly deferred until an internalFunctions-parametric scope API exists.

HelperStepProofs.lean adds cons and whole-list assemblers that turn per-statement ExprInternalHelperHeadStepBridgeWithInternals into StmtListGenericWithHelpersAndHelperIRWithInternals (narrow scaffold: all heads via expression bridges; mixed direct/residual lists still use the legacy seam).

PrintAxioms.lean registers the new public theorems (theorem count 5495 → 5499).

^{Reviewed by Cursor Bugbot for commit 3469224. 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 6:52am

[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_a8a64fb4-cb76-4f19-9f1b-65b585350d14)

[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_66ce5f6b-3c54-4f27-b732-9e8cbad042e7)

[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_e0c9cc8d-c77f-4cf4-95f5-5db12230885c)