chore: fix build

Author: luisacicolini

src/Init/Data/BitVec/Bitblast.lean

@@ -1980,7 +1980,7 @@ theorem clz_eq_clzAuxRec_of_false (x : BitVec w) (h : ∀ i, n < i → x.getLsbD
         rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)]
         simp only [show ¬∀ i, i < w + 1 → x.getLsbD i = false by simp; exists 0; simp [hx0],
           iff_false] at heq
-        rw [clzAux_eq_iff_forall_of_clzAuz_lt (by omega) (by omega)]
+        rw [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
@@ -2003,7 +2003,7 @@ theorem clz_eq_clzAuxRec_of_false (x : BitVec w) (h : ∀ i, n < i → x.getLsbD
         simp only [iff_false, show ¬∀ i, i < w + 1 → x.getLsbD i = false by simp; exists n + 1] at heq
         simp only [hxn, ↓reduceIte, toNat_eq, toNat_ofNat]
         rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega),
-          clzAux_eq_iff_forall_of_clzAuz_lt (by omega) (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
@@ -2021,4 +2021,12 @@ theorem clz_eq_clzAuxRec_of_eq (x : BitVec w) (h : w - 1 ≤ n) :
   intro i hi
   simp [show w ≤ i by omega]
 
+theorem clzAuxRec_eq_of_le (x : BitVec w) (hn : w ≤ n) :
+    x.clzAuxRec n = x.clzAuxRec (w - 1) := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · rw [← clz_eq_clzAuxRec_of_eq]
+    · rw [clz_eq_clzAuxRec_of_eq]; omega
+    · omega
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -5635,6 +5635,39 @@ theorem clzAux_eq_zero_iff {x : BitVec w} {n : Nat}:
   unfold clzAux
   cases n <;> simp
 
+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 hn1 : x.getLsbD (n + 1)
+    · simp only [clzAux, hn1, ↓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
+    · have h3 : 1 + x.clzAux n = n + 1 + 1 ↔ x.clzAux n = n + 1 := by omega
+      simp only [clzAux, hn1, Bool.false_eq_true, ↓reduceIte, h3, ihn]
+      constructor
+      · intro h i hin
+        by_cases hi : i ≤ n
+        · apply h
+          omega
+        · simp only [Bool.not_eq_true] at hn1
+          simp [show i = n + 1 by omega, hn1]
+      · intro h i hin
+        apply h
+        omega
+
+theorem clzAux_le {x : BitVec w} {n : Nat} :
+    clzAux x n ≤ n + 1 := by
+  induction n
+  · case zero =>
+    by_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
+
 @[simp]
 theorem clzAux_zero {x : BitVec w} : clzAux x 0 = if x.getLsbD 0 then 0 else 1 := by simp [clzAux]
 
@@ -5665,8 +5698,8 @@ theorem clzAux_eq_iff_forall_of_clzAux_lt  {x : BitVec w} (hlt : (clzAux x n < n
         intro hi
         specialize hi 0 (by omega)
         simp [hxn] at hi
-      · simp [hxn, Bool.false_eq_true, ↓reduceIte] at hlt
-        simp [show x.clzAux n < n + 1 by omega, forall_const] at ihn
+      · simp only [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, Nat.reduceSubDiff, ihn,
           and_congr_left_iff]

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

@@ -186,7 +186,6 @@ theorem eval_arithShiftRightConst : eval (arithShiftRightConst n) = (BitVec.sshi
 
 @[simp] theorem eval_clz : eval .clz = (BitVec.clz : BitVec w → BitVec w) := by rfl
 
-
 end BVUnOp
 
 /--

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

@@ -1,18 +1,10 @@
 /-
 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
+Authors: Luisa Cicolini, Siddharth Bhat, Henrik Böving
 -/
 prelude
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
-import Std.Sat.AIG
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
 import Std.Sat.AIG.If
 
 /-!
@@ -35,7 +27,6 @@ def blastClz (aig : AIG α) (x : AIG.RefVec aig w) :
 where
   go (aig : AIG α) (x : AIG.RefVec aig w) (curr : Nat) (acc : AIG.RefVec aig w) :=
     if hc : curr < w then
-      -- w - curr - 1
       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
@@ -72,8 +63,7 @@ theorem blastClz.go_decl_eq (aig : AIG α) (curr : Nat) (acc : AIG.RefVec aig w)
   split at hgo
   · rw [← hgo]
     intros
-    rw [blastClz.go_decl_eq]
-    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
+    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]
@@ -84,12 +74,12 @@ instance : AIG.LawfulVecOperator α AIG.RefVec blastClz where
     intros
     unfold blastClz
     dsimp only
-    (expose_names; exact blastClz.go_le_size aig 0 (blastConst aig ↑len) input)
+    apply blastClz.go_le_size
   decl_eq := by
     intros
     unfold blastClz
     dsimp only
-    (expose_names; exact blastClz.go_decl_eq aig 0 (blastConst aig ↑len) input idx h2 h1)
+    apply blastClz.go_decl_eq
 
 end bitblast
 end BVExpr

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

@@ -1,7 +1,7 @@
 /-
 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
+Authors: Luisa Cicolini, Siddharth Bhat, Henrik Böving
 -/
 prelude
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic