proof: add bitNot expression helper bridge

[Th0rgal]

Summary

• add generic one-argument helper-aware IR builtin wrappers for unary expression constructors
• add shared source/Yul value facts for Expr.bitNot, including builtin agreement and source helper evaluation
• add unary compositional context/poststate bridges for Expr.bitNot helper payloads
• regenerate PrintAxioms.lean with the new unary/bitNot 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
Changes are confined to Lean proof lemmas and the axiom inventory; no runtime compiler or execution behavior is modified.

Overview
Extends helper-step proofs with unary IR evaluation lemmas (evalIRExprsWithInternals_single_of_value, evalIRExprWithInternals_unary_builtin_of_value) parallel to the existing two-argument builtin path, so one-arg Yul builtins can be discharged in compositional expression contexts.

Adds the full Expr.bitNot bridge: shared exprBitNotValue semantics (including Uint256.not / EVM not builtin agreement), compile/source/IR evaluation lemmas, and threaded compositional context/poststate results wired through exprInternalHelperCompositionalContextResult_unary_context.

PrintAxioms.lean is regenerated to list the new declarations (theorem count 5747 → 5756).

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

[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_395e530c-4e67-457d-bc28-637a192bffbe)

[github-actions]

OpenCodeReview first-pass review

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

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