proof: lift expr helper result through let head

[Th0rgal]

Continues #2080 after phase 9 / #2103.

Stacking: this PR targets paloma/issue-2080-constructor-expr-bridge and depends on #2103, which remains stacked on #2102 and #2101.

What changed

• Threads the existing statement fuel slack into ExprInternalHelperHeadStepBridge, so concrete statement-head adapters can line up execIRStmtsWithInternals fuel with expression evaluation fuel.
• Adds compileStmt_letVar_of_compileExprWithInternals for singleton Stmt.letVar compilation.
• Adds exprInternalHelperHeadStepBridge_letVar_of_exprCompositionalResult, the first concrete adapter from an ExprInternalHelperCompositionalContextResult into an ExprInternalHelperHeadStepBridge for an expression-bearing statement head.

Non-vacuous status

This is a concrete statement-head lift for Stmt.letVar: the theorem consumes the phase 6-9 compositional expression payload, preserves the helper payload existential, evaluates source and helper-aware IR for the statement head, and proves the resulting stmtStepMatchesIRExecWithInternals continue case.

Remaining proof/API gaps

The adapter keeps two obligations explicit instead of faking them:

• CompiledStmtStepWithHelpersAndHelperIR.compileOk still records the legacy compileStmt ... stmt shape with the default empty internal-function list, while expression helper payloads compile with spec.functions; callers must currently provide the statement-side compile shape separately.
• ExprInternalHelperCompositionalContextResult does not yet record post-expression IR/source state preservation or old-scope binding preservation, so the letVar adapter requires those facts explicitly.

Recommended next dispatch: close those two API gaps by enriching the expression compositional result with final-state relation facts and aligning helper-aware statement compilation witnesses with spec.functions; then instantiate this letVar bridge with the phase-9 Expr.add right-helper result.

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs passed.
• rg -n "\\bsorry\\b|\\badmit\\b|\\baxiom\\b" Compiler/Proofs/HelperStepProofs.lean found no matches.
• git diff --check passed.
• lean-slot make check was attempted, but the offloaded workspace used by lean-slot is not a git repository for git ls-files; it passed property manifest/coverage/sync and contract structure checks before failing in scripts/check_paths.py with fatal: not a git repository.

---

Note

Low Risk
Lean proof-only changes in helper-step infrastructure; no runtime, auth, or deployment impact. Residual API mismatches (empty vs spec.functions compile witnesses) are documented and left for follow-up.

Overview
Continues #2080 phase 10 by wiring expression-position helper proofs up to statement heads, starting with Stmt.letVar.

ExprInternalHelperHeadStepBridge now requires IR fuel slack (sizeOf compiledIR - compiledIR.length ≤ irFuel) so statement-head adapters can align execIRStmtsWithInternals fuel with inner expression evaluation. compiledStmtStepWithHelpersAndHelperIR_of_exprHeadStepBridge forwards that hypothesis into the bridge.

New lemmas: compileStmt_letVar_of_compileExprWithInternals (singleton let compile shape from a helper-aware expression compile) and exprInternalHelperHeadStepBridge_letVar_of_exprCompositionalResult, which consumes an ExprInternalHelperCompositionalContextResult (plus explicit post-expression runtime/scope facts and name-in-scope side conditions) and proves source execStmtWithHelpers and IR execution both continue with the bound value while re-establishing scope/runtime invariants.

PrintAxioms.lean and scripts/check_proof_length.py register the new theorems (allowlist entry for the long letVar adapter proof).

^{Reviewed by Cursor Bugbot for commit 8d1e6d1. 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 6, 2026 6:49am

[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_a20856f6-88ca-40a6-b418-bfe9ffd71ce7)

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```

[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_13184542-4762-4977-b254-0ac6865764e9)

[Th0rgal]

Reviewed this PR's isolated contribution (2 commits over paloma/issue-2080-constructor-expr-bridge):

• New exprInternalHelperHeadStepBridge_letVar_of_exprCompositionalResult (first concrete letVar statement-head adapter) and compileStmt_letVar_of_compileExprWithInternals simp lemma; the added sizeOf compiledIR - compiledIR.length ≤ irFuel hypothesis on the bridge field strengthens (not weakens) the interface, and the hslack intro matches the pre-existing CompiledStmtStepWithHelpersAndHelperIR.preserves signature. No sorry/admit/axiom; PrintAxioms.lean refresh consistent (5488 → 5490, 0 sorry'd).
• CI was red on the checks job: the 124-line adapter proof exceeded the 50-line limit without an allowlist entry. Pushed 8bc3ff2 adding the scripts/check_proof_length.py allowlist entry with justification (same mechanism as Prove dynamic ABI decoder refinement #2057/Bitmap iterator surface (#1996) #2019/Transient storage fields (#1995) #2021). Local lake build Compiler.Proofs.HelperStepProofs and lean_lint --only proof_length pass.
• CI is now fully green on 8bc3ff2: https://github.com/lfglabs-dev/verity/actions/runs/28728932663 (checks, build, foundry shards, compiler audits/regressions all success).

Not merging yet: base PR #2103 (paloma/issue-2080-constructor-expr-bridge) is still open, with #2102/#2101 below it. Per series convention (#2095–#2100), this PR should be retargeted to main and squash-merged only after its parents land. No other blockers — no unresolved review threads; Bugbot's latest attempt hit a usage limit (infra, no findings; earlier pass rated the diff Low Risk).

[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_9667ffa7-c348-45b2-b816-7cc6f31acb43)