proof: add shl expression helper bridges

[Th0rgal]

Summary

• add a shared Expr.shl source/Yul value and builtin agreement lemma for EVM shift-left semantics
• add compiler/source/builtin facts for Expr.shl
• add right- and left-threaded expression helper context/post-state bridges for Expr.shl
• 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 bitNot expression helper bridge #2186 / codex/2080-expr-helper-bitnot-threaded.
• PrintAxioms.lean reports 5765 theorems/lemmas (4005 public, 1760 private, 0 sorry'd).

---

Note

Low Risk
Proof-only additions in HelperStepProofs with no runtime or compiler behavior changes; axiom inventory update is mechanical.

Overview
Extends the compiler correctness proof chain for Expr.shl using the same pattern as recent bitwise helper work (bitNot, bitXor).

Adds exprShlValue and lemmas tying it to Uint256.shl, EVM modulus bounds, and the concrete builtin rule (shift < 256 vs zero). Proves compile/source/builtin alignment (compileExprWithInternals_shl_of_children, evalExprWithHelpers_shl_of_values, evalBuiltinCallWithEvmYulLeanContext_shl_of_values) and left/right-threaded ExprInternalHelperCompositionalContextResult / PostStateResult bridges so helper-step induction can treat shl like other binary builtins.

PrintAxioms.lean is regenerated to register the nine new public lemmas (theorem count 5765, up by 9).

^{Reviewed by Cursor Bugbot for commit 0935cee. Bugbot is set up for automated code reviews on this repo. Configure here.}

[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_66d3df40-7758-4d26-9c13-2d54a4967d78)

[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:03am

[github-actions]

OpenCodeReview first-pass review

Status: success · Mode: medium-lean · 0 finding(s) · 2 files · 518354 tokens · 39 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: 271 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status success; comments 0; files 2; tokens 518354; tool calls 39; warnings 0; duration 511s
• Largest changed files: Compiler/Proofs/HelperStepProofs.lean (+260/-0), PrintAxioms.lean (+10/-1)

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