proof: add bitAnd expression helper bridges

[Th0rgal]

Summary

• add shared source/Yul value facts for Expr.bitAnd, including builtin agreement and source helper evaluation
• add right-threaded and left-threaded compositional context/poststate bridges for Expr.bitAnd helper payloads
• regenerate PrintAxioms.lean with the new bitAnd bridge declarations; total still reports 0 sorry

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)

---

Note

Low Risk
Proof-only additions in the compiler verification layer; no runtime, auth, or production code paths change.

Overview
Adds formal proof infrastructure for Expr.bitAnd in HelperStepProofs.lean, following the same pattern as existing binary ops like mod.

Introduces exprBitAndValue with lemmas for EVM modulus bounds and agreement with native &&&, plus compile/source-eval/builtin lemmas and left- and right-threaded compositional context and post-state bridges wired through the shared binary-builtin helpers (YulExpr.call "and").

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

^{Reviewed by Cursor Bugbot for commit 276bcd2. 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 9:26am

[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_9be3f290-58fa-488c-a0fc-f608787ab6be)

[github-actions]

OpenCodeReview first-pass review

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

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