feat: add leading zero counter BitVec.clz and bitblaster circuit/infrastructure (#8546)

This PR adds a new `BitVec.clz` operation and a corresponding `clz`
circuit to `bv_decide`, allowing to bitblast the count leading zeroes
operation. The AIG circuit is linear in the number of bits of the
original expression, making the bitblasting convenient wrt. rewriting.
`clz` is common in numerous compiler intrinsics (see
[here](https://clang.llvm.org/docs/LanguageExtensions.html#intrinsics-support-within-constant-expressions))
and architectures (see
[here](https://en.wikipedia.org/wiki/Find_first_set)).

Co-authored by @bollu.

---------

Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Siddharth <[email protected]>

Author: 3 people

src/Init/Data/BitVec/Basic.lean

@@ -850,4 +850,15 @@ treating `x` and `y` as 2's complement signed bitvectors.
 def smulOverflow {w : Nat} (x y : BitVec w) : Bool :=
   (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1))
 
+/-- Count the number of leading zeros downward from the `n`-th bit to the `0`-th bit for the bitblaster.
+  This builds a tree of `if-then-else` lookups whose length is linear in the bitwidth,
+  and an efficient circuit for bitblasting `clz`. -/
+def clzAuxRec {w : Nat} (x : BitVec w) (n : Nat) : BitVec w :=
+  match n with
+  | 0 => if x.getLsbD 0 then BitVec.ofNat w (w - 1) else BitVec.ofNat w w
+  | n' + 1 => if x.getLsbD n then BitVec.ofNat w (w - 1 - n) else clzAuxRec x n'
+
+/-- Count the number of leading zeros. -/
+def clz (x : BitVec w) : BitVec w := clzAuxRec x (w - 1)
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -3468,6 +3468,11 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
   apply eq_of_toNat_eq
   simp [BitVec.ofNat, Fin.ofNat_sub]
 
+theorem ofNat_sub_ofNat_of_le (x y : Nat) (hy : y < 2 ^ w) (hlt : y ≤ x):
+    BitVec.ofNat w x - BitVec.ofNat w y = BitVec.ofNat w (x - y) := by
+  apply eq_of_toNat_eq
+  simp [Nat.mod_eq_of_lt hy, show 2 ^ w - y + x = 2 ^ w + (x - y) by omega, Nat.add_mod_left]
+
 @[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
 
 @[simp] protected theorem zero_sub (x : BitVec n) : 0#n - x = -x := rfl
@@ -5625,6 +5630,23 @@ theorem msb_replicate {n w : Nat} {x : BitVec w} :
   simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]
   cases n <;> cases w <;> simp
 
+/-! ### Count leading zeros -/
+
+theorem clzAuxRec_zero (x : BitVec w) :
+    x.clzAuxRec 0 = if x.getLsbD 0 then BitVec.ofNat w (w - 1) else BitVec.ofNat w w := by rfl
+
+theorem clzAuxRec_succ (x : BitVec w) :
+    x.clzAuxRec (n + 1) = if x.getLsbD (n + 1) then BitVec.ofNat w (w - 1 - (n + 1)) else BitVec.clzAuxRec x n := by rfl
+
+theorem clzAuxRec_eq_clzAuxRec_of_le (x : BitVec w) (h : w - 1 ≤ n) :
+    x.clzAuxRec n = x.clzAuxRec (w - 1) := by
+  let k := n - (w - 1)
+  rw [show n = (w - 1) + k by omega]
+  induction k
+  · case zero => simp
+  · case succ k ihk =>
+    simp [show w - 1 + (k + 1) = (w - 1 + k) + 1 by omega, clzAuxRec_succ, ihk,
+      show x.getLsbD (w - 1 + k + 1) = false by simp only [show w ≤ w - 1 + k + 1 by omega, getLsbD_of_ge]]
 
 /-! ### Inequalities (le / lt) -/
 

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -40,6 +40,7 @@ instance : ToExpr BVUnOp where
     | .rotateRight n => mkApp (mkConst ``BVUnOp.rotateRight) (toExpr n)
     | .arithShiftRightConst n => mkApp (mkConst ``BVUnOp.arithShiftRightConst) (toExpr n)
     | .reverse => mkConst ``BVUnOp.reverse
+    | .clz => mkConst ``BVUnOp.clz
   toTypeExpr := mkConst ``BVUnOp
 
 instance : ToExpr (BVExpr w) where

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -184,6 +184,8 @@ where
       return some atom
     | BitVec.reverse _ innerExpr =>
       unaryReflection innerExpr .reverse ``Std.Tactic.BVDecide.Reflect.BitVec.reverse_congr origExpr
+    | BitVec.clz _ innerExpr =>
+      unaryReflection innerExpr .clz ``Std.Tactic.BVDecide.Reflect.BitVec.clz_congr origExpr
     | _ => return none
 
   /--

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -156,6 +156,8 @@ builtin_dsimproc [simp, seval] reduceSMTSDiv ((smtSDiv _ _ : BitVec _)) := reduc
 builtin_dsimproc [simp, seval] reduceGetLsb (getLsbD _ _) := reduceGetBit ``getLsbD getLsbD
 /-- Simplification procedure for `getMsb` (most significant bit) on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceGetMsb (getMsbD _ _) := reduceGetBit ``getMsbD getMsbD
+/-- Simplification procedure for `clz` (count leading zeros) on `BitVec`. -/
+builtin_dsimproc [simp, seval] reduceClz (clz _) := reduceUnary ``BitVec.clz 2 BitVec.clz
 
 /-- Simplification procedure for `getElem`  on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceGetElem ((_ : BitVec _)[_]) := fun e => do

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -139,6 +139,10 @@ inductive BVUnOp where
   Reverse the bits in a bitvector.
   -/
   | reverse
+  /--
+  Count leading zeros.
+  -/
+  | clz
   deriving Hashable, DecidableEq
 
 namespace BVUnOp
@@ -149,6 +153,7 @@ def toString : BVUnOp → String
   | rotateRight n => s!"rotR {n}"
   | arithShiftRightConst n => s!">>a {n}"
   | reverse => "rev"
+  | clz => "clz"
 
 instance : ToString BVUnOp := ⟨toString⟩
 
@@ -161,6 +166,7 @@ def eval : BVUnOp → (BitVec w → BitVec w)
   | rotateRight n => (BitVec.rotateRight · n)
   | arithShiftRightConst n => (BitVec.sshiftRight · n)
   | reverse =>  BitVec.reverse
+  | clz => BitVec.clz
 
 @[simp] theorem eval_not : eval .not = ((~~~ ·) : BitVec w → BitVec w) := by rfl
 
@@ -178,6 +184,8 @@ theorem eval_arithShiftRightConst : eval (arithShiftRightConst n) = (BitVec.sshi
 
 @[simp] theorem eval_reverse : eval .reverse = (BitVec.reverse : BitVec w → BitVec w) := by rfl
 
+@[simp] theorem eval_clz : eval .clz = (BitVec.clz : BitVec w → BitVec w) := by rfl
+
 end BVUnOp
 
 /--

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -19,6 +19,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
 
 /-!
 This module contains the implementation of a bitblaster for `BitVec` expressions (`BVExpr`).
@@ -224,6 +225,12 @@ where
           dsimp only at heaig
           omega
         ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastReverse) ..)⟩
+      | .clz =>
+        let res := bitblast.blastClz eaig evec
+        have := by
+          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastClz)
+          omega
+        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastClz) ..)⟩
     | .append lhs rhs h =>
       let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache
       let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache
@@ -335,7 +342,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
         · apply Nat.le_trans <;> assumption
   · next op expr =>
     match op with
-    | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. | .reverse =>
+    | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. | .reverse | .clz =>
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [goCache_decl_eq]
       have := (goCache aig expr cache).result.property

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Clz.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Luisa Cicolini, Siddharth Bhat, Henrik Böving
+-/
+prelude
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
+import Std.Sat.AIG.If
+
+/-!
+This module contains the implementation of a bitblaster for `BitVec.clz`.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+
+variable [Hashable α] [DecidableEq α]
+
+namespace BVExpr
+namespace bitblast
+
+def blastClz (aig : AIG α) (x : AIG.RefVec aig w) :
+    AIG.RefVecEntry α w :=
+  let wconst := blastConst aig w
+  go aig x 0 wconst
+where
+  go (aig : AIG α) (x : AIG.RefVec aig w) (curr : Nat) (acc : AIG.RefVec aig w) :=
+    if hc : curr < w then
+      let lhs := blastConst aig (w := w) (w - 1 - curr)
+      let res := AIG.RefVec.ite aig ⟨x.get curr hc, lhs, acc⟩
+      let aig := res.aig
+      let acc := res.vec
+      have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
+      let x : AIG.RefVec aig w := x.cast this
+      go aig x (curr + 1) acc
+    else
+      ⟨aig, acc⟩
+  termination_by w - curr
+
+namespace blastClz
+
+end blastClz
+
+theorem blastClz.go_le_size (aig : AIG α) (curr : Nat) (acc : AIG.RefVec aig w)
+    (xc : AIG.RefVec aig w) :
+    aig.decls.size ≤ (go aig xc curr acc).aig.decls.size := by
+  unfold go
+  dsimp only
+  split
+  · refine Nat.le_trans ?_ (by apply go_le_size)
+    apply AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite)
+  · simp
+termination_by w - curr
+
+theorem blastClz.go_decl_eq (aig : AIG α) (curr : Nat) (acc : AIG.RefVec aig w)
+    (xc : AIG.RefVec aig w) :
+    ∀ (idx : Nat) h1 h2,
+        (go aig xc curr acc).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
+  generalize hgo : go aig xc curr acc = res
+  unfold go at hgo
+  dsimp only at hgo
+  split at hgo
+  · rw [← hgo]
+    intros
+    rw [blastClz.go_decl_eq, AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
+    apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
+    assumption
+  · simp [← hgo]
+termination_by w - curr
+
+instance : AIG.LawfulVecOperator α AIG.RefVec blastClz where
+  le_size := by
+    intros
+    unfold blastClz
+    dsimp only
+    apply blastClz.go_le_size
+  decl_eq := by
+    intros
+    unfold blastClz
+    dsimp only
+    apply blastClz.go_decl_eq
+
+end bitblast
+end BVExpr
+
+end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -20,6 +20,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Reverse
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Clz
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
 
 /-!
@@ -425,6 +426,12 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
         BitVec.getElem_reverse, BitVec.getMsbD_eq_getLsbD, decide_true, Bool.true_and]
       rw [goCache_denote_eq]
       exact hinv
+    · rw [← hres]
+      simp only [eval_un, BVUnOp.eval_clz, BitVec.clz]
+      rw [denote_blastClz]
+      intro idx hidx
+      rw [goCache_denote_eq]
+      exact hinv
   · next h =>
     subst h
     rw [← hres]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Luisa Cicolini, Siddharth Bhat, Henrik Böving
+-/
+prelude
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Const
+
+/-!
+This module contains the verification of the bitblaster for `BitVec.clz` from
+`Impl.Operations.Clz`. We prove that the accumulator of the `go` function
+at step`n` represents the portion of the `ite` nodes in the AIG constructed for
+bits `0` until `n`.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+open Std.Sat.AIG
+
+variable [Hashable α] [DecidableEq α]
+
+namespace BVExpr
+
+namespace bitblast
+namespace blastClz
+
+example (x : Nat) (hx : 0 < x) : ∃ y, x = y + 1 := by
+  exact Nat.exists_eq_add_one.mpr hx
+
+theorem go_denote_eq {w : Nat} (aig : AIG α)
+    (acc : AIG.RefVec aig w) (xc : AIG.RefVec aig w) (x : BitVec w) (assign : α → Bool)
+    (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx)
+    (hacc : ∀ (idx : Nat) (hidx : idx < w),
+      if curr = 0 then ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.ofNat w w).getLsbD idx
+      else ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.clzAuxRec x (curr - 1)).getLsbD idx)
+    :
+    ∀ (idx : Nat) (hidx : idx < w),
+        ⟦
+          (go aig xc curr acc).aig,
+          (go aig xc curr acc).vec.get idx hidx,
+          assign
+        ⟧
+          =
+        (BitVec.clzAuxRec x (w - 1)).getLsbD idx := by
+    intro idx hidx
+    generalize hgo: go aig xc curr acc = res
+    unfold go at hgo
+    split at hgo
+    · case isTrue h =>
+        simp only [BitVec.natCast_eq_ofNat, BitVec.ofNat_eq_ofNat] at hgo
+        rw [← hgo, go_denote_eq]
+        · intro idx hidx
+          rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
+          · simp [hx]
+          · simp [Ref.hgate]
+        · intro idx hidx
+          simp only [Nat.add_eq_zero, Nat.succ_ne_self, and_false, reduceIte, RefVec.get_cast,
+            Ref.cast_eq, Nat.add_one_sub_one]
+          rw [RefVec.denote_ite]
+          split
+          · next h =>
+            rw [hx] at h
+            have : 1 < 2 ^ w := by exact Nat.one_lt_two_pow_iff.mpr (by omega)
+            rcases curr with _|curr
+            · simp [denote_blastConst, BitVec.clzAuxRec_zero, h, BitVec.ofNat_sub_ofNat_of_le (x := w) (y := 1) (by omega) (by omega)]
+            · have := Nat.lt_pow_self (n := curr + 1) (a := 2) (by omega)
+              have := Nat.pow_lt_pow_of_lt (a := 2) (n := curr + 1) (m := w) (by omega) (by omega)
+              simp only [denote_blastConst, BitVec.clzAuxRec_succ, h, reduceIte]
+              rw [BitVec.ofNat_sub_ofNat_of_le (x := w) (y := 1) (by omega) (by omega),
+                  BitVec.ofNat_sub_ofNat_of_le (x := w - 1) (y := curr + 1) (by omega) (by omega)]
+          · split at hacc
+            · next h1 h2 =>
+              have hxc : x.getLsbD 0 = false := by rw [hx] at h1; simp [h2] at h1; exact h1
+              simp [hacc, h2, BitVec.clzAuxRec_zero, hxc]
+            · next h1 h2 =>
+              obtain ⟨curr, hcurr⟩ : ∃ curr', curr = curr' + 1 := by apply Nat.exists_eq_add_one.mpr (by omega)
+              subst hcurr
+              have hxc : x.getLsbD (curr + 1) = false := by rw [hx] at h1; simp at h1; exact h1
+              simp [hacc, BitVec.clzAuxRec_succ, hxc]
+    · case isFalse h =>
+      rw [← hgo]
+      simp only [show ¬curr = 0 by omega, reduceIte] at hacc
+      simp only [hacc, BitVec.clzAuxRec_eq_clzAuxRec_of_le (x := x) (n := curr - 1) (by omega)]
+
+end blastClz
+
+@[simp]
+theorem denote_blastClz (aig : AIG α) (xc : RefVec aig w) (x : BitVec w) (assign : α → Bool)
+      (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx)
+      :
+      ∀ (idx : Nat) (hidx : idx < w),
+        ⟦(blastClz aig xc).aig, (blastClz aig xc).vec.get idx hidx, assign⟧
+          =
+        (BitVec.clzAuxRec x (w - 1)).getLsbD idx := by
+  intro idx hidx
+  generalize hb : blastClz aig xc = res
+  unfold blastClz at hb
+  dsimp only at hb
+  rw [← hb, blastClz.go_denote_eq (x := x) (w := w)]
+  · exact hx
+  · intro idx hidx
+    simp only [reduceIte, BitVec.natCast_eq_ofNat]
+    rw [denote_blastConst]
+
+end bitblast
+end BVExpr
+
+end Std.Tactic.BVDecide