proof: package expression helper context head

[Th0rgal]

Summary

• add ExprInternalHelperCompositionalContextResult, a small expression-context payload that combines outer expression compile/evaluation correspondence with the phase-5 helper-head package
• add the direct Expr.internalCall head base theorem that reuses exprInternalHelperCallContextBridge_compileExprWithInternals_internalCall and carries source arg evaluation, compiled Yul arg evaluation to the same argVals, helper summary/world evidence, helper dispatch, and source/compiled state relation
• regenerate PrintAxioms.lean

References #2080.

Base / dependency

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

Proof status

This is a non-vacuous base-case handoff for the compositional expression-context theorem: the new result shape records the outer expression compile/evaluation facts while preserving the exact phase-5 helper-head evidence. The direct-head theorem constructs that package for Expr.internalCall.

This does not fully close arbitrary non-call expression contexts or StmtListExprInternalHelperStepInterface. The remaining proof/API blocker is the recursive expression compiler theorem over non-call Expr constructors that constructs ExprInternalHelperCompositionalContextResult for parent contexts and then a statement-head bridge for the expression-bearing Stmt cases.

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

---

Note

Low Risk
Lean proof-only additions with no changes to compilation or runtime semantics; risk is limited to proof maintenance and axiom inventory accuracy.

Overview
Adds ExprInternalHelperCompositionalContextResult, a proof obligation that ties outer expression compile/source-eval/IR-eval agreement to the existing phase-5 helper-head package (ExprInternalHelperCompiledCallContextResult). The intended follow-on is a recursive theorem over non-call Expr constructors that fills this shape for parent contexts.

Proves the direct head base case for Expr.internalCall via exprInternalHelperCompositionalContextResult_internalCall_head, reusing exprInternalHelperCallContextBridge_compileExprWithInternals_internalCall plus compile shape, arg evaluation, and value correspondence hypotheses. PrintAxioms.lean is regenerated to register the new public theorem.

This does not close arbitrary expression contexts or StmtListExprInternalHelperStepInterface; it is scaffolding for the compositional expression proof.

^{Reviewed by Cursor Bugbot for commit 0990f8f. 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 11:45am

[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_5d570dac-5d0f-45ee-9686-8eb9513942a3)