proof: add expression helper bridge interface witness

[Th0rgal]

Summary

• add ExprInternalHelperHeadStepBridge for expression-position internal-helper statement heads
• add bridge-to-CompiledStmtStepWithHelpersAndHelperIR and list-level StmtListExprInternalHelperStepInterface assembly theorems
• regenerate PrintAxioms.lean for the three new public proof declarations

References #2080.

Proof status

This is non-vacuous at the expression-helper interface boundary: when stmtTouchesExprInternalHelperSurface stmt = true, the list witness now consumes an exact helper-aware compiled statement step supplied by ExprInternalHelperHeadStepBridge.

The full semantic closure is still blocked by the missing expression-context API theorem documented in code: a compositional lemma connecting SourceSemantics.evalExprWithHelpers internal-call summary/world-preservation evidence to compiled Yul expression evaluation under evalIRCallWithInternals.

This PR preserves the existing helper-surface-closed fast paths and does not remove SupportedStmtList.helperSurfaceClosed.

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs (passed; Spark offload denied for this mission path, built locally)
• lake env lean Compiler/Proofs/HelperStepProofs.lean (passed)
• python3 scripts/generate_print_axioms.py --check (passed)
• make check (passed)

---

Note

Low Risk
Proof-only additions with no runtime or compiler behavior changes; helper-surface-closed fast paths are unchanged.

Overview
Adds the expression-position helper proof plumbing in HelperStepProofs.lean, parallel to the existing direct-call and direct-assign bridges.

Introduces ExprInternalHelperHeadStepBridge (compile + source/IR stmtStepMatchesIRExecWithInternals obligation for statement heads whose helper work is in expressions), then three assembly theorems: singleton CompiledStmtStepWithHelpersAndHelperIR, cons on StmtListExprInternalHelperStepInterface, and list induction from per-head bridges when stmtTouchesExprInternalHelperSurface holds.

Documentation in-file notes full semantic closure still depends on a missing compositional lemma tying evalExprWithHelpers to evalIRCallWithInternals. PrintAxioms.lean is updated to register the three new public theorems (5467 total).

^{Reviewed by Cursor Bugbot for commit b580e95. Bugbot is set up for automated code reviews on this repo. Configure here.}

[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_cd7820b8-a0c9-4191-8df8-a32a8c283eae)

[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 9:34pm