proof: add expression helper context bridge

[Th0rgal]

Summary

• add public source-side expression helper witness lemmas for evalExprWithHelpers_internalCall: witness-based summary postcondition and world-preservation consequence
• add an expression-context helper bridge in HelperStepProofs.lean that packages source summary soundness, expression-call world preservation, compiled helper table evidence, and the compiled Yul evalIRCallWithInternals dispatch shape
• regenerate PrintAxioms.lean

References #2080.

Proof status

This advances the phase-3 expression-position adapter from a pure statement-head boundary witness to a semantic expression-context bridge layer:

• Source side: exprInternalHelperCallContextBridge_sourceEvidence exposes the evalExprWithHelpers reduction for Expr.internalCall, the corresponding InternalHelperSummaryContract.post fact for interpretInternalFunctionFuel, and the world-preservation consequence needed by expression contexts.
• Compiled IR side: evalIRCallWithInternals_of_compiledHelperWitness connects SupportedCompiledInternalHelperWitness to helper-aware Yul expression-call dispatch through evalIRCallWithInternals after argument evaluation.
• Inventory assembly: exprInternalHelperCallContextBridge_of_supportedEvidence packages SupportedBodyHelperInterface, summary soundness, exprCallsPreserveWorld, and SupportedRuntimeHelperTableInterface into the per-callee expression-context bridge.

This is non-vacuous for the per-callee expression helper call bridge, but it does not fully close StmtListExprInternalHelperStepInterface: the remaining architecture gap is the compositional expression compiler theorem that proves compiled Yul argument/expression contexts evaluate to the same argVals/state expected by this bridge and lifts that through arbitrary statement heads. Existing helper-surface-closed fast paths and SupportedStmtList.helperSurfaceClosed are unchanged.

Validation

• lake env lean Compiler/Proofs/IRGeneration/SourceSemantics.lean (passed)
• lake env lean Compiler/Proofs/HelperStepProofs.lean (passed)
• lean-slot lake build Compiler.Proofs.HelperStepProofs (passed; Spark offload denied for this mission path, built locally)
• python3 scripts/generate_print_axioms.py --check (passed)
• rg -n "\\bsorry\\b|\\badmit\\b|\\baxiom\\b" Compiler/Proofs/IRGeneration/SourceSemantics.lean Compiler/Proofs/HelperStepProofs.lean (no matches)
• make check (passed)

Next blocker / dispatch recommendation

Prove the expression compiler/context theorem that turns per-call bridge evidence into statement-head ExprInternalHelperHeadStepBridge values: it needs to relate SourceSemantics.evalExprWithHelpers and evalIRExprWithInternals for expression contexts containing internal helper calls, threading helper-world preservation and argument evaluation through compileExprWithInternals / statement compilation shapes.

---

Note

Low Risk
Proof-only additions in compiler verification modules with no runtime or auth changes; remaining gap is explicitly documented architecture, not partial unsafe closure.

Overview
Adds expression-position internal helper proof infrastructure so source evalExprWithHelpers and compiled evalIRCallWithInternals can be linked per callee before full statement-head closure.

In SourceSemantics, new witness-based lemmas expose summary postconditions and world preservation for Expr.internalCall under evalExprWithHelpers, without relying on private lookup hypotheses.

In HelperStepProofs, evalIRCallWithInternals_of_compiledHelperWitness shows that after Yul args evaluate, helper-aware calls dispatch through the runtime internal table; ExprInternalHelperCallContextBridge bundles source summary soundness, world preservation, compiled helper witnesses, and that IR dispatch shape; exprInternalHelperCallContextBridge_of_supportedEvidence builds bridges from the supported helper inventory; exprInternalHelperCallContextBridge_sourceEvidence packages the source-side reduction, contract post, and preservation facts.

PrintAxioms is regenerated (+4 public theorems). StmtListExprInternalHelperStepInterface is still open: a compositional expression-compiler theorem is needed to lift per-call bridges to ExprInternalHelperHeadStepBridge.

^{Reviewed by Cursor Bugbot for commit 6526713. 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 4, 2026 1:55am

[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_25ea55e1-f998-43a3-8138-da6cdcf04024)