proof: lift expression helper context payload

[Th0rgal]

Summary

• add exprInternalHelperCompositionalContextResult_of_outer_facts, a proof adapter that lifts the phase-6 ExprInternalHelperCompositionalContextResult helper-head payload through an already-proved outer expression context
• add unary and binary non-call expression-context wrappers so constructor-specific proofs can preserve the same source helper argVals, compiled argument evaluation, helper-world evidence, helper dispatch, and source/compiled head-state relation
• regenerate PrintAxioms.lean for the four new public theorems

References #2080.

Base / dependency

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

Proof status

This is a compiling, non-vacuous API bridge for the recursive expression-context theorem: once a constructor-specific proof supplies the parent compile/source-eval/IR-eval facts, the adapter preserves the exact helper-head payload produced by phase 6.

This does not fully close arbitrary expression recursion or StmtListExprInternalHelperStepInterface. The remaining proof/API blocker is a uniform helper-aware source/IR expression compiler lemma for non-call Expr constructors, including sequential IR state threading for sibling expressions. The statement-head bridge should consume these adapters after that lemma is available.

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-only additions with no executable compiler or runtime behavior changes; risk is limited to proof API correctness and maintainability.

Overview
Adds proof adapters in HelperStepProofs.lean so constructor-specific lemmas can reuse the phase-6 ExprInternalHelperCompositionalContextResult helper-head payload when the parent expression’s compile, source-eval, and IR-eval facts are already proved.

exprInternalHelperCompositionalContextResult_of_outer_facts copies the existing helper-world match and ExprInternalHelperCompiledCallContextResult witness from a child “head” into the parent result, given outer hcompile / hsource / hir. Unary and binary left/right wrappers (…_unary_context, …_binary_left_context, …_binary_right_context) instantiate that adapter for common non-call expression shapes; sibling IR state threading stays in the caller’s hir hypothesis.

PrintAxioms.lean is regenerated to list the four new public theorems (5479 total lemmas). Full automatic recursion over all non-call Expr constructors is still blocked on a uniform helper-aware expression compiler lemma.

^{Reviewed by Cursor Bugbot for commit f90ac27. 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 3:49pm

[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_ba880132-09f2-4f09-a9b5-4b0468e7d343)