feat: add leading zero counter BitVec.clz and bitblaster circuit/infrastructure

src/Init/Data/BitVec/Basic.lean

@@ -850,4 +850,13 @@ 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. -/
+def clzAux {w : Nat} (x : BitVec w) (n : Nat) : Nat :=
+  match n with
+  | 0 => if x.getLsbD 0 then 0 else 1
+  | n' + 1 => if x.getLsbD n then 0 else 1 + clzAux x n'
+
+/-- Count the number of leading zeroes. -/
+def clz {w : Nat} (x : BitVec w) : BitVec w := if w = 0 then 0 else BitVec.ofNat w (clzAux x (w - 1))
+
 end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -1907,4 +1907,74 @@ theorem shiftLeft_add_eq_shiftLeft_or {x y : BitVec w} :
     (y <<< x) + x =  (y <<< x) ||| x := by
   rw [BitVec.add_comm, add_shiftLeft_eq_or_shiftLeft, or_comm]
 
+/-! ### Count Leading Zeros -/
+
+/-- 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'
+
+/--
+If `x : BitVec w` has all bits larger than index `n` equal to `false`,
+then `clzAuxRec` starting from `n` will compute the `clz`.
+-/
+theorem clz_eq_clzAuxRec_of_forall_getLsbD_false (x : BitVec w) (h : ∀ i, n < i → x.getLsbD i = false) :
+    x.clz = x.clzAuxRec n := by
+  have := Nat.lt_pow_self (a := 2) (n := w) (by omega)
+  rcases w with _|w
+  · simp [of_length_zero]
+  · have hle := clzAux_le (x := x) (n := w)
+    have heq := clzAux_eq_iff (x := x) (n := w)
+    induction n
+    · case zero =>
+      simp only [clzAuxRec, zero_lt_succ, getLsbD_eq_getElem]
+      by_cases hx0 : x[0]
+      · simp only [show ¬∀ i, i < w + 1 → x.getLsbD i = false by simp; exists 0; simp [hx0],
+          iff_false] at heq
+        simp only [clz, Nat.add_eq_zero, succ_ne_self, _root_.and_false, reduceIte,
+          Nat.add_one_sub_one, hx0, toNat_eq, toNat_ofNat]
+        rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega),
+          clzAux_eq_iff_forall_of_clzAux_lt (by omega)]
+        simp only [Nat.sub_self, zero_lt_succ, getLsbD_eq_getElem, hx0, _root_.and_true]
+        intro i hi
+        apply h
+        omega
+      · simp only [clz, Nat.add_eq_zero, succ_ne_self, _root_.and_false, reduceIte,
+          Nat.add_one_sub_one, hx0, false_eq_true, toNat_eq, toNat_ofNat, Nat.mod_two_pow_self]
+        rw [Nat.mod_eq_of_lt (by omega), heq]
+        intro i hi
+        by_cases hi' : 0 < i
+        · apply h; exact hi'
+        · simp [show i = 0 by omega, hx0]
+    · case succ n ihn =>
+      by_cases hxn : x.getLsbD (n + 1)
+      · have := lt_of_getLsbD hxn
+        simp [iff_false, show ¬∀ i, i < w + 1 → x.getLsbD i = false by simp; exists n + 1] at heq
+        simp only [clz, Nat.add_eq_zero, succ_ne_self, _root_.and_false, reduceIte,
+          Nat.add_one_sub_one, clzAuxRec, hxn, toNat_eq, toNat_ofNat]
+        rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega),
+          clzAux_eq_iff_forall_of_clzAux_lt (by omega)]
+        simp only [show w - (w - (n + 1)) = n + 1 by omega, hxn, _root_.and_true]
+        intro i hi
+        apply h
+        omega
+      · simp only [clzAuxRec, hxn, false_eq_true, reduceIte]
+        apply ihn
+        intro i hi
+        by_cases hi : n + 1 < i
+        · apply h; exact hi
+        · simp [show i = n + 1 by omega, hxn]
+
+/--
+`clzAuxRec` agrees with `clz` when `clzAuxRec` is started from an index `n` that is at least `w - 1`.
+-/
+theorem clz_eq_clzAuxRec_of_le (x : BitVec w) (h : w - 1 ≤ n) :
+    x.clz = x.clzAuxRec n := by
+  rw [clz_eq_clzAuxRec_of_forall_getLsbD_false]
+  intro i hi
+  simp [show w ≤ i by omega]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -5568,6 +5568,96 @@ 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 zeroes -/
+
+/-- The number of leading zeroes is 0 if and only if the first bit checked (`x.getLsbD n`) is `true` -/
+theorem clzAux_eq_zero_iff {x : BitVec w} {n : Nat} :
+    clzAux x n = 0 ↔ x.getLsbD n = true := by
+  cases n <;> simp [clzAux]
+
+/-- The number of leading zeroes can't be larger than the number of bits clzAux checks -/
+theorem clzAux_le {x : BitVec w} {n : Nat} :
+    clzAux x n ≤ n + 1 := by
+  induction n
+  · case zero =>
+    cases hx0 : x.getLsbD 0
+    <;> simp [clzAux, hx0]
+  · case succ n ihn =>
+    by_cases hxn : x.getLsbD (n + 1)
+    · simp [clzAux, hxn]
+    · simp [clzAux, hxn]; omega
+
+/-- The number of leading zeroes is equal to the numbers of bits checked if and only if all
+  the bits from the `n`-th to the `0`-th are `false`. -/
+theorem clzAux_eq_iff {x : BitVec w} {n : Nat} :
+    clzAux x n = (n + 1) ↔ (∀ i, i < n + 1 → x.getLsbD i = false) := by
+  induction n
+  · case zero => simp [clzAux]
+  · case succ n ihn =>
+    by_cases hxn : x.getLsbD (n + 1)
+    · simp only [clzAux, hxn, reduceIte, Nat.right_eq_add, Nat.add_eq_zero, reduceCtorEq,
+        and_false, false_iff, Classical.not_forall, not_imp, Bool.not_eq_false]
+      exists n + 1, by omega
+    · simp only [clzAux, hxn, Bool.false_eq_true, reduceIte,
+        show 1 + x.clzAux n = n + 1 + 1 ↔ x.clzAux n = n + 1 by omega, ihn]
+      constructor
+      · intro hc i hin
+        by_cases hi : i ≤ n
+        · apply hc; omega
+        · simp [show i = n + 1 by omega, hxn]
+      · intro hc i hin
+        apply hc
+        omega
+
+@[simp]
+theorem clzAux_zero {x : BitVec w} : clzAux x 0 = if x.getLsbD 0 then 0 else 1 := by simp [clzAux]
+
+/-- If the number of leading zeroes is strictly smaller than the number of bits checked (i.e.,
+  not all bits are `false`), then there exists a `true` bit at a certain position `n - k` between
+  the `n`-th and the `0`-th bit, and all bits between `n` and that bit are `false` -/
+theorem clzAux_eq_iff_forall_of_clzAux_lt  {x : BitVec w} (hlt : (clzAux x n < n + 1)):
+    clzAux x n = k ↔ ((∀ i, i < k → x.getLsbD (n - i) = false) ∧ ((x.getLsbD (n - k) = true))) := by
+>>>>>>> 0743518018f9cbb69a953810b06ad9110363600c
+  induction n generalizing k
+  · case zero =>
+    rcases k with _|k
+    · simp [clzAux_eq_zero_iff]
+    · simp only [clzAux_zero, Nat.zero_le, Nat.sub_eq_zero_of_le]
+      by_cases hx0 : x.getLsbD 0
+      · simp only [hx0, reduceIte, Bool.true_eq_false, imp_false, Nat.not_lt, and_true,
+          false_iff, Classical.not_forall, Nat.not_le, show ¬ 0 = k + 1 by omega]
+        exists 0
+        omega
+      · have hiff := clzAux_eq_zero_iff (x := x) (n := 0)
+        simp only [show x.clzAux 0 = 0 by omega, true_iff] at hiff
+        simp [hiff] at hx0
+  · case succ n ihn =>
+    rcases k with _|k
+    · simp [clzAux_eq_zero_iff]
+    · simp only [clzAux, Nat.reduceSubDiff] at *
+      by_cases hxn : x.getLsbD (n + 1)
+      · simp only [hxn, reduceIte, show ¬ 0 = k + 1 by omega, false_iff, _root_.not_and, Bool.not_eq_true]
+        intro h
+        specialize h 0 (by omega)
+        simp [hxn] at h
+      · simp only [clzAux, hxn, Bool.false_eq_true, reduceIte] at hlt
+        simp only [show x.clzAux n < n + 1 by omega, forall_const] at ihn
+        simp only [hxn, Bool.false_eq_true, reduceIte,
+          show 1 + x.clzAux n = k + 1 ↔ x.clzAux n = k by omega, ihn, and_congr_left_iff]
+        intro h
+        constructor
+        · intro hi j hj
+          by_cases hj0 : j = 0
+          · simp [hj0, hxn]
+          · specialize hi (j - 1) (by omega)
+            rw [show n - (j - 1) = n + 1 - j by omega] at hi
+            exact hi
+        · intro hj i hi
+          specialize hj (1 + i)
+          rw [show n + 1 - (1 + i) = n - i by omega] at hj
+          apply hj
+          omega
+
 
 /-! ### 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/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -139,6 +139,10 @@ inductive BVUnOp where
   Reverse the bits in a bitvector.
   -/
   | reverse
+  /--
+  Count leading zeroes.
+  -/
+  | 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 := by apply 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]
+      rw [BitVec.clz_eq_clzAuxRec_of_le (x := eval assign _) (n := w - 1) (by omega), denote_blastClz]
+      intro idx hidx
+      rw [goCache_denote_eq]
+      exact hinv
   · next h =>
     subst h
     rw [← hres]