proof: bridge expression helper compiler context

[Th0rgal]

Summary

• add the compiler shape theorem for Expr.internalCall through compileExprWithInternals / compileInternalCallArgs
• add a compiled expression-call context result package that threads source evalExprWithHelpers, helper summary postcondition, helper-world preservation, compiled helper lookup, evalIRCallWithInternals, and evalIRExprWithInternals
• add the non-vacuous per-callee bridge theorem composing ExprInternalHelperCallContextBridge with compiled argument evaluation evidence at the helper-call head
• regenerate PrintAxioms.lean

References #2080.

Base / dependency

#2097 is merged, so this PR targets main directly. It is not stacked.

Proof status

This advances the remaining phase-4 blocker by adding the smallest expression compiler/context bridge currently supported by the architecture:

• compileExprWithInternals_internalCall_shape exposes the compiled Yul call produced for expression-position internal helpers using the exact compileInternalCallArgs path, including expanded/forwarded helper arguments.
• exprInternalHelperCallContextBridge_compileExprWithInternals_internalCall composes the phase-4 per-callee ExprInternalHelperCallContextBridge with source argument evaluation, compiled argument evaluation to the same argVals, source summary soundness, world preservation, helper runtime lookup, evalIRCallWithInternals, and the resulting evalIRExprWithInternals call expression shape.
• Existing helper-surface-closed and expression-surface-closed fast paths are unchanged.

This is non-vacuous at the Expr.internalCall head. It does not fully close arbitrary expression contexts or StmtListExprInternalHelperStepInterface: the remaining proof/API gap is the compositional theorem lifting this helper-call head result through non-call expression contexts and statement heads while proving the compiled Yul argument context evaluates to the source helper argVals and preserving the helper-world evidence.

Validation

• 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 after regenerating PrintAxioms.lean)
• rg -n "\\bsorry\\b|\\badmit\\b|\\baxiom\\b" Compiler/Proofs/HelperStepProofs.lean (no matches)
• make check (passed)

---

Note

Low Risk
Proof-only additions in helper step proofs with no runtime or auth changes; scope is localized to compiler correctness lemmas.

Overview
Adds the phase-4 expression compiler/context handoff for Expr.internalCall heads in HelperStepProofs.lean: a compile-shape lemma via compileInternalCallArgs, a bundled ExprInternalHelperCompiledCallContextResult predicate, and a bridge theorem that ties source evalExprWithHelpers, helper summary/world preservation, and IR evalIRCallWithInternals / evalIRExprWithInternals when source and compiled args agree on argVals.

Also adds evalIRExprWithInternals_call_of_dispatch to map internal-call dispatch equalities into full expression-evaluation outcomes, and updates PrintAxioms.lean (+3 listed lemmas).

^{Reviewed by Cursor Bugbot for commit f3213e1. 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 7:47am

[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_ca61b0e4-0478-400d-a9e2-9fdada306d6e)