Bitmap iterator surface (#1996)

[Th0rgal]

Summary

• Adds clz/msb expression sugar backed by a new IR opcode (0x1e) with Yul lowering
• Introduces Stmt.forEachSetBit plus macro syntax for iterating set bits of a word via MSB/CLZ-driven loop lowering
• Source/denotation semantics with execForEachSetBitLoop_succ recurrence and agreement lemmas
• Smoke contract + PropertyBitmapIteratorSmoke.t.sol property test coverage

Closes #1996

Test plan

• lake build Verity Contracts Compiler PrintAxioms — Build completed successfully
• scripts/refresh_verification_artifacts.sh — [refresh] PASS
• make check — All checks passed

---

Note

Medium Risk
Fork-dependent Yul (Osaka CLZ vs fallback) affects codegen correctness on wrong targets; large touch surface across compiler validation and proof modules increases regression risk despite smoke tests.

Overview
Introduces Stmt.forEachSetBit and macro forEachSetBit to walk set bits in a word (MSB→LSB), with clz/msb expression sugar (Osaka verbatim_1i_1o 0x1e) and stdlib clz/msb helpers.

Statement compilation is refactored to compileStmtWithFork / compileStmtListWithFork with a targetFork argument threaded from compile, constructors, internals, and externals (fixing compileValidatedCore to pass fork through). Osaka+ lowers forEachSetBit via CLZ and a captured bit mask for safe body clears; pre-Osaka uses a descending index scan loop—covered by BitmapIteratorForkSmoke.

execForEachSetBitLoop semantics and denote agreement lemmas are added; validation, usage analysis, trust surface, CEI, and IR-generation proofs are extended for the new stmt. Smoke contract BitmapIteratorSmoke and PropertyBitmapIteratorSmoke.t.sol stub tests are included.

^{Reviewed by Cursor Bugbot for commit 828830e. 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	Jun 16, 2026 10:34am

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 828830e. Configure here.}

[cursor]

Empty bitmap loop var unset

Medium Severity

Stmt.forEachSetBit lowering initializes the loop variable to literal zero before the loop, but execStmt enters execForEachSetBitLoop on the incoming state without binding that name. When the bitmap evaluates to zero, the loop never runs and the variable keeps any prior binding instead of zero, unlike Stmt.forEach and unlike emitted Yul.

Additional Locations (1)

• Verity/Core/Model/Denote.lean#L1026-L1032

 

^{Reviewed by Cursor Bugbot for commit 828830e. Configure here.}

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```