proof: add shr expression helper bridges

[Th0rgal]

Summary

• add a shared Expr.shr source/Yul value and builtin agreement lemma for EVM shift-right semantics
• add compiler/source/builtin facts for Expr.shr
• add right- and left-threaded expression helper context/post-state bridges for Expr.shr
• regenerate PrintAxioms.lean

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs
• python3 scripts/check_proof_length.py
• python3 scripts/generate_print_axioms.py
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• rg -n "\\b(sorry|admit|axiom)\\b|set_option\\s+autoImplicit\\s+true" Compiler/Proofs/HelperStepProofs.lean (no matches)

Notes

• Stacked on proof: add shl expression helper bridges #2187 / codex/2080-expr-helper-shl-threaded.
• PrintAxioms.lean reports 5774 theorems/lemmas (4014 public, 1760 private, 0 sorry'd).

---

Note

Low Risk
Proof-only additions mirroring established shl lemmas; no runtime or compiler behavior changes.

Overview
Extends the expression-helper correctness story to Expr.shr, following the same pattern as the recent shl work.

Adds exprShrValue (Uint256 shift-right modulo EVM), bounds and builtin agreement (exprShrValue_eq_builtin for shift ≥ 256 → 0), plus lemmas tying compilation to YulExpr.call "shr", source eval, and Yul builtin eval.

Adds right- and left-threaded ExprInternalHelperCompositionalContextResult / PostStateResult bridges so helper-aware induction can compose through shr when children are proved first.

PrintAxioms.lean is regenerated to register the nine new theorems (total count 5774, still 0 sorry).

^{Reviewed by Cursor Bugbot for commit bf53ebf. 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 11, 2026 10:10am

[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_1b84b7fd-e2c2-4acd-b9cd-ba9058d11c20)

[github-actions]

OpenCodeReview first-pass review

Status: success · Mode: medium-lean · 0 finding(s) · 2 files · 545928 tokens · 31 tool calls

No comments generated. Looks good to me.

OCR pilot metrics

• Routing: medium-lean (router-v8)
• Changed files: 2 supported / 2 total; Lean 2, trust docs 0, workflow/scripts 0, contracts 0, docs 0
• Changed lines: 266 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status success; comments 0; files 2; tokens 545928; tool calls 31; warnings 0; duration 536s
• Largest changed files: Compiler/Proofs/HelperStepProofs.lean (+255/-0), PrintAxioms.lean (+10/-1)

Pilot mode: advisory only. Codex Review remains the merge gate.