proof: thread helper expr context through siblings

[Th0rgal]

Summary

• add exprInternalHelperCompositionalContextResult_of_outer_facts_threaded_head, a threaded variant of the phase-7 payload adapter where the helper-head IR expression starts from an intermediate sibling state instead of the parent entry state
• add exprInternalHelperCompositionalContextResult_binary_right_threaded_context so right-hand binary expression contexts can preserve the same helper-head payload after the left sibling advances IR state
• add small IR helpers for non-call binary expression compiler lemmas: evalIRExprsWithInternals_pair_of_values exposes left-to-right argument-state threading, and evalIRExprWithInternals_binary_builtin_of_values packages pure two-argument builtin evaluation once constructor-specific source/compile/value facts are supplied
• regenerate PrintAxioms.lean

References #2080.

Base / dependency

This PR is stacked on #2101 because #2101 is still open. Base branch: paloma/issue-2080-expression-recursive-context.

Proof status

This is a compiling, non-vacuous API bridge for the remaining helper-aware source/IR expression compiler lemma. It does not close the full recursive non-call Expr theorem or StmtListExprInternalHelperStepInterface, but it removes the key right-sibling state-shape gap: the helper payload can now be lifted from an IR state reached after evaluating an earlier sibling while the parent expression result is evaluated from the original IR state.

The statement-head lift remains blocked on constructor-specific source/compile/value facts for expression-bearing statement heads. The next dispatch should use these threaded adapters to prove concrete binary constructor cases, then consume them through ExprInternalHelperHeadStepBridge.

Validation

• 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)
• 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-library additions only; no runtime, auth, or compiler behavior changes beyond new reusable lemmas for future expression-helper proofs.

Overview
Adds helper-aware expression compositional proof bridges so binary/non-call Expr lemmas can treat IR evaluation when a left sibling has already advanced IRState, while source evaluation still uses the original runtime.

New theorems in HelperStepProofs.lean: exprInternalHelperCompositionalContextResult_of_outer_facts_threaded_head (threaded variant of the outer-facts adapter), exprInternalHelperCompositionalContextResult_binary_right_threaded_context (right-child helper payload with sibling state threading), plus evalIRExprsWithInternals_pair_of_values and evalIRExprWithInternals_binary_builtin_of_values to package left-to-right arg evaluation and pure two-argument Yul builtin IR steps for constructor-specific lemmas.

PrintAxioms.lean is regenerated to register the four new public lemmas (theorem count 5479 → 5483).

^{Reviewed by Cursor Bugbot for commit 9174d5e. 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:51pm

[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_ab069523-0cec-4a46-bdf1-a198fa450551)