proof: expose helper-return assign bridge catalog witness

[Th0rgal]

Summary

Advances #2080 for the helper-return-binding surface after #2090.

This PR keeps the existing StmtListDirectInternalHelperAssignStepInterface bridge witnesses and adds a function-body-level assembly theorem:

• stmtListDirectInternalHelperAssignStepInterface_of_perCalleeAssignBridgeCatalog

The new theorem converts the rank-induction-oriented DirectInternalHelperPerCalleeAssignBridgeCatalog into the statement-list assign interface for fn.body, reusing the existing per-callee bridge and helper-call-name seam. It does not weaken supported fragments, helper-surface gates, compiler behavior, or CI checks.

Notes

The helper-return-binding witness is non-vacuous at the interface layer: it consumes DirectInternalHelperAssignHeadStepBridge, which compiles Stmt.internalCallAssign into the Yul letMany helper call and carries the exact source/IR execution bridge.

The proof is still parameterized by the assign-head bridge. Closing that bridge directly from helper summaries remains blocked on the same architectural API gap noted in the file: a compiled-helper execution summary lemma connecting execIRInternalFunctionWithInternals / evalIRCallWithInternals to InternalHelperSummaryContract.post for the helper body.

This PR intentionally does not remove SupportedStmtList.helperSurfaceClosed or the unsupported-helper-surface gate; expression-position helper calls and structural helper recursion remain open parts of #2080.

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs passed. Spark offload rejected this mission worktree path with HTTP 403, so lean-slot built locally.
• python3 scripts/generate_print_axioms.py --check passed.
• python3 scripts/lean_lint.py --only proof_length passed.
• rg -n "\\b(sorry|admit|axiom)\\b" Compiler/Proofs/HelperStepProofs.lean; test $? -eq 1 passed.
• make check passed: 607 Python tests, all checks passed.
• lean-slot make verify passed before the final rebase. Spark offload rejected this mission worktree path with HTTP 403, so lean-slot built locally.

---

Note

Low Risk
Pure Lean proof scaffolding with no compiler, fragment, or runtime changes; the assign-head bridge remains an explicit parameter.

Overview
Adds stmtListDirectInternalHelperAssignStepInterface_of_perCalleeAssignBridgeCatalog, which turns a DirectInternalHelperPerCalleeAssignBridgeCatalog (the rank-decreasing helper-summary assign inventory) into StmtListDirectInternalHelperAssignStepInterface for fn.body, by reusing the existing per-statement-list assign bridge assembly and mapping helperCallNames membership to catalog assign entries.

Documentation in the direct helper-return-binding section is tightened to name the assign-head bridge as the remaining semantic seam; the cons_internalCallAssign proof is slightly simplified. PrintAxioms.lean registers the new public theorem.

^{Reviewed by Cursor Bugbot for commit 208d625. 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 3, 2026 5:37pm

[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_356d802d-823f-443f-aa6b-d319a2438bb5)