Promoted from #1982 P1 to a standalone tracked issue (was previously only a roadmap bullet).
Problem
Solidity bitmap walks use while (bitmap != 0) { msb; clear; }. Verity downstream models fall back to index-scan + masking via bounded forEach (Morpho Midnight isHealthy/liquidate collateral walk), which hurts both source fidelity and the refinement extraction of the liquidation loop trace. CLZ is only available via consumer verity_intrinsic (EIP-7939).
Goal
- First-class (or verified-library)
msb/clz builtin with proof support.
- A source-level bitmap iterator (
forEachSetBit) that compiles to the MSB-driven loop and comes with a generic loop lemma for refinement proofs.
Acceptance
Midnight collateral walk expressible in MSB-driven form, shape-matching solc output, with the loop's refinement lemma generic rather than hand-rolled.
Promoted from #1982 P1 to a standalone tracked issue (was previously only a roadmap bullet).
Problem
Solidity bitmap walks use
while (bitmap != 0) { msb; clear; }. Verity downstream models fall back to index-scan + masking via boundedforEach(Morpho MidnightisHealthy/liquidatecollateral walk), which hurts both source fidelity and the refinement extraction of the liquidation loop trace. CLZ is only available via consumerverity_intrinsic(EIP-7939).Goal
msb/clzbuiltin with proof support.forEachSetBit) that compiles to the MSB-driven loop and comes with a generic loop lemma for refinement proofs.Acceptance
Midnight collateral walk expressible in MSB-driven form, shape-matching solc output, with the loop's refinement lemma generic rather than hand-rolled.