proof: add bitXor expression helper bridges

[Th0rgal]

Summary

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

Overview
Adds formal proof infrastructure for Expr.bitXor in HelperStepProofs.lean, following the same pattern as the existing bitOr bridges.

Introduces exprBitXorValue (Uint256 xor modulo EVM) with bounds and agreement with Nat.xor and the Yul xor builtin. New lemmas tie compilation to YulExpr.call "xor", source helper evaluation, and builtin IR evaluation to that shared value.

Adds right- and left-threaded compositional context/poststate theorems so helper-aware source/IR steps for bitwise xor compose through child proofs via the shared binary-builtin threading lemmas.

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

^{Reviewed by Cursor Bugbot for commit 5d9aabc. 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:43am

[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_602702c0-fdc8-453c-9f35-68e18524b9db)

[github-actions]

OpenCodeReview first-pass review

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

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