proof: bridge add expression helper constructor

[Th0rgal]

Restores the unique phase work from closed-unmerged #2103 after #2102 merged and the old base branch was deleted.

Summary

• add constructor-specific Expr.add source, compile, and Yul builtin value facts for helper-aware expression proofs
• add exprInternalHelperCompositionalContextResult_add_right_threaded, a non-vacuous right-child bridge that uses the threaded binary API after the left operand advances the IR state
• regenerate PrintAxioms.lean

References #2080.
Supersedes closed #2103. This branch was rebased onto main and drops the duplicate #2101/#2102 commits now already merged.

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs passed on head 8a973ce1.
• python3 scripts/generate_print_axioms.py --check passed.
• python3 scripts/check_proof_length.py passed.
• git diff --check origin/main...HEAD passed.
• rg -n "\\bsorry\\b|\\badmit\\b|\\baxiom\\b" Compiler/Proofs/HelperStepProofs.lean found no matches.

---

Note

Low Risk
Proof-only additions in HelperStepProofs with no changes to compilation or runtime semantics; axiom inventory is regenerated for tracking.

Overview
Adds constructor-specific Lean proofs for Expr.add in the helper-aware expression compositional pipeline: shared exprAddValue, compile/source/Yul-builtin value lemmas, and a uint256_ofNat EVM-modulus normalization lemma used to align source semantics with Uint256 addition.

Introduces exprInternalHelperCompositionalContextResult_add_right_threaded, the first non-internalCall expression constructor that fully discharges compile, source, and IR facts via the threaded binary API (left operand advances IR state; right child carries helper payload from the updated state).

Regenerates PrintAxioms.lean to register the five new public theorems (+5 in the inventory count).

^{Reviewed by Cursor Bugbot for commit 8a973ce. 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: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_d4f689e8-d0b4-44ef-9694-9570c7273ab1)

[Th0rgal]

Stack repair status for #2080:

• Restored the closed-unmerged proof: bridge add expression helper constructor #2103 work in this replacement PR because GitHub would not reopen proof: bridge add expression helper constructor #2103 while its deleted base branch was still recorded, and would not retarget a closed PR.
• Rebased paloma/issue-2080-constructor-expr-bridge onto main; head is 8a973ce1fb3dd998335305cbf271684e1fe7317a with only the unique constructor bridge commit.
• Rebased the downstream stack branches proof: lift expr helper result through let head #2104-proof: make scope lift helper-world parametric #2108 onto the repaired ancestry; GitHub now reports those PRs mergeable against their stacked bases.

Local validation completed:

• lean-slot lake build Compiler.Proofs.HelperStepProofs passed for this PR head.
• Top-of-stack lean-slot lake build Compiler.Proofs.HelperStepProofs passed after rebasing proof: lift expr helper result through let head #2104-proof: make scope lift helper-world parametric #2108.
• python3 scripts/generate_print_axioms.py --check passed.
• python3 scripts/check_proof_length.py passed.
• no sorry/admit/axiom matches in Compiler/Proofs/HelperStepProofs.lean.
• git diff --check passed.

Merge blocker: CI is not complete yet for this PR. Run https://github.com/lfglabs-dev/verity/actions/runs/28773176893 has changes, checks, timeout-watchdog, and build passing, but build-audits and build-compiler-binaries are still queued/pending. I am not merging until the full required rollup is green.

[Th0rgal]

Review/merge re-check for #2109:

Diff review and local validation are clean:

• Branch head remains 8a973ce1fb3dd998335305cbf271684e1fe7317a with a single commit over main.
• Diff is limited to Compiler/Proofs/HelperStepProofs.lean and PrintAxioms.lean and preserves the constructor bridge work from the closed proof: bridge add expression helper constructor #2103 replacement path.
• lean-slot lake build Compiler.Proofs.HelperStepProofs passed locally.
• python3 scripts/generate_print_axioms.py --check passed locally.
• python3 scripts/check_proof_length.py passed locally.
• git diff --check passed locally.
• No sorry/admit/axiom matches in Compiler/Proofs/HelperStepProofs.lean.
• GitHub review threads are empty; Cursor Bugbot posted only the usage-limit skip.

Merge blocker: GitHub CI is still incomplete and the PR merge state is UNSTABLE. I am not merging until the required rollup is green. Current unfinished checks are:

• compiler-audits queued
• foundry (0) queued
• foundry (2) queued
• foundry (3) queued

[Th0rgal]

Review/merge follow-up for #2109 after a bounded 45-minute CI wait:

GitHub review threads are still empty, and Cursor Bugbot still only has the usage-limit skip. The PR head remains 8a973ce1fb3dd998335305cbf271684e1fe7317a.

Merge blocker: GitHub CI is still incomplete and the PR merge state remains UNSTABLE. I am not merging until the required rollup is green. Current unfinished checks are:

• foundry (2) in progress: https://github.com/lfglabs-dev/verity/actions/runs/28773176893/job/85315944395
• foundry (3) queued: https://github.com/lfglabs-dev/verity/actions/runs/28773176893/job/85315944376

All previously queued compiler-audits and foundry (0) checks have passed, so another waiter/review pass is needed once the two remaining Foundry jobs finish.