proof: add bitOr expression helper bridges

[Th0rgal]

Summary

• add shared source/Yul value facts for Expr.bitOr, including builtin agreement and source helper evaluation
• add right-threaded and left-threaded compositional context/poststate bridges for Expr.bitOr helper payloads
• regenerate PrintAxioms.lean with the new bitOr 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 following the established bitAnd pattern; no runtime or compiler behavior changes.

Overview
Extends the compiler correctness proof library so Expr.bitOr is handled like other binary builtins (e.g. bitAnd): shared EVM or semantics, compile/eval alignment, and helper-composition bridges.

Adds exprBitOrValue plus lemmas that the result stays below evmModulus, matches Nat ||| on reduced operands, and agrees with Yul builtin "or". compileExprWithInternals_bitOr_of_children, evalExprWithHelpers_bitOr_of_values, and evalBuiltinCallWithEvmYulLeanContext_bitOr_of_values wire source compilation and evaluation to YulExpr.call "or".

Four threaded theorems lift child helper payloads to Expr.bitOr for ExprInternalHelperCompositionalContextResult and ExprInternalHelperCompositionalPostStateResult (right- and left-threaded), reusing the generic binary builtin scaffolding with findInternalFunction? … "or" = none.

PrintAxioms.lean is regenerated to list the nine new declarations (theorem count 5729 → 5738).

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

[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_2fe411cd-f0d2-4c81-9a9e-71620aba5b04)

[github-actions]

OpenCodeReview first-pass review

Status: success · Mode: medium-lean · 0 finding(s) · 2 files · 216026 tokens · 13 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 216026; tool calls 13; warnings 0; duration 123s
• Largest changed files: Compiler/Proofs/HelperStepProofs.lean (+238/-0), PrintAxioms.lean (+10/-1)

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