proof: add byte expression helper bridges

[Th0rgal]

Summary

• add a shared Expr.byte source/Yul value for normalized byte extraction
• add compiler/source/builtin facts for Expr.byte
• add right- and left-threaded expression helper context/post-state bridges for Expr.byte
• 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 shr expression helper bridges #2188 / codex/2080-expr-helper-shr-threaded.
• PrintAxioms.lean reports 5782 theorems/lemmas (4022 public, 1760 private, 0 sorry'd).

---

Note

Low Risk
Formal proof-only changes following an established binary-op helper pattern; no runtime, auth, or production compiler behavior changes.

Overview
Extends the compiler correctness proof chain for Expr.byte using the same pattern as shr/shl: a shared exprByteValue (via Verity.Core.Uint256.byte), plus lemmas that compileExprWithInternals emits YulExpr.call "byte", source evalExprWithHelpers and Yul evalBuiltinCallWithEvmYulLeanContext agree on that value, and the result stays below evmModulus.

Adds left- and right-threaded ExprInternalHelperCompositionalContextResult / PostStateResult bridges by plugging those facts into the existing binary builtin threaded helpers ("byte", no shadowing internal byte). PrintAxioms.lean is regenerated (+8 public theorems, 5782 total).

^{Reviewed by Cursor Bugbot for commit 7d54a05. 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:18am

[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_6626c325-7f4d-4e47-a8cc-7aba28217c52)

[github-actions]

OpenCodeReview first-pass review

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

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