proof: add signextend expression helper bridges

[Th0rgal]

Summary

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

---

Note

Low Risk
Proof-only additions with no changes to compilation or runtime semantics; mirrors an established byte-helper pattern.

Overview
Adds Lean proof infrastructure for Expr.signextend in HelperStepProofs.lean, following the same pattern as the existing byte helpers.

Introduces exprSignextendValue (normalized Uint256.signextend result) plus lemmas tying compilation to YulExpr.call "signextend", source evaluation, and EVM builtin semantics. Four threaded theorems lift child compositional context and post-state results to the full signextend expression (left- and right-eval order).

PrintAxioms.lean is regenerated to register the eight new public theorems (theorem count 5782 → 5790).

^{Reviewed by Cursor Bugbot for commit 4de2bd9. 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: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_8e3271c6-256f-4da4-ada8-e3af7e2d8f4b)

[github-actions]

OpenCodeReview first-pass review

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

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