feat: bitVec shiftLeft recurrences for bitblasting

src/Init/Data/BitVec/Bitblast.lean

@@ -290,7 +290,7 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
         simp [hik', hik'']
   · ext k
     simp
-    omega
+    by_cases hi : x.getLsb i <;> simp [hi] <;> omega
 
 /--
 Recurrence lemma: multiplying `l` with the first `s` bits of `r` is the
@@ -326,4 +326,112 @@ theorem getLsb_mul (x y : BitVec w) (i : Nat) :
   · simp
   · omega
 
+/-## shiftLeft recurrence for bitblasting -/
+
+/--
+A recurrence that describes shifting by an arbitrary bitvector
+as shifting by a constant amount.
+ -/
+def shiftLeftRec (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁ :=
+  let shiftAmt := (y &&& (twoPow w₂ n))
+  match n with
+  | 0 => x <<< shiftAmt
+  | n + 1 => (shiftLeftRec x y n) <<< shiftAmt
+
+@[simp]
+theorem shiftLeftRec_zero {x : BitVec w₁} {y : BitVec w₂} :
+    shiftLeftRec x y 0 = x <<< (y &&& twoPow w₂ 0)  := by
+  simp [shiftLeftRec]
+
+@[simp]
+theorem shiftLeftRec_succ {x : BitVec w₁} {y : BitVec w₂} :
+    shiftLeftRec x y (n + 1) =
+      (shiftLeftRec x y n) <<< (y &&& twoPow w₂ (n + 1)) := by
+  simp [shiftLeftRec]
+
+@[simp]
+theorem getLsb_ofNat_one {w i : Nat} :
+    (1#w).getLsb i = (decide (i = 0) && decide (i < w)) := by
+  rcases w with rfl | w
+  · simp
+  · simp only [getLsb, toNat_ofNat, testBit_mod_two_pow]
+    by_cases hi : i = 0
+    · simp [hi]
+    · simp only  [hi, decide_False, Bool.false_and,
+        and_eq_false_imp, decide_eq_true_eq]
+      intros _; simp [testBit, shiftRight_eq_div_pow];
+      suffices 1 / 2^i = 0 by simp [this]
+      apply Nat.div_eq_of_lt (Nat.one_lt_two_pow_iff.mpr hi)
+
+/--
+If `(y &&& z = 0)`, then shifting by `y ||| z` is the same as shifting by `y` and then by `z`.
+Note that the hypothesis `h'` is implied by `h : y &&& z = 0#w`,
+but we choose to take the additional hypothesis and leave proving it
+as an implication of `h` for a follow up PR.
+-/
+theorem shiftLeft_or_eq_shiftLeft_shiftLeft_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂}
+    (h : y &&& z = 0#w₂) (h' : y.toNat + z.toNat < 2^w₂) :
+    x <<< (y ||| z) = x <<< y <<< z := by
+  simp [← add_eq_or_of_and_eq_zero _ _ h, shiftLeft_eq', shiftLeft_add,
+    toNat_add, Nat.mod_eq_of_lt h']
+
+theorem getLsb_shiftLeft' {x : BitVec w} {y : BitVec w₂} {i : Nat} :
+    (x <<< y).getLsb i = (decide (i < w) && !decide (i < y.toNat) && x.getLsb (i - y.toNat)) := by
+  simp [shiftLeft_eq', getLsb_shiftLeft]
+
+/--
+`shiftLeftRec x y n` shifts `x` to the left by the first `n` bits of `y`.
+-/
+theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} (hn : n + 1 ≤ w₂) :
+    shiftLeftRec x y n = x <<< (y.truncate (n + 1)).zeroExtend w₂ := by
+  induction n generalizing x y
+  case zero =>
+    ext i
+    simp only [shiftLeftRec_zero, twoPow_zero_eq_one, Nat.reduceAdd, truncate_one_eq_ofBool_getLsb]
+    have heq : (y &&& 1#w₂) = zeroExtend w₂ (ofBool (y.getLsb 0)) := by
+      ext i
+      by_cases h : (↑i : Nat) = 0 <;> simp [h, Bool.and_comm]
+    simp [heq]
+  case succ n ih =>
+    simp only [shiftLeftRec_succ, and_twoPow_eq_getLsb]
+    by_cases h : y.getLsb (n + 1)
+    · simp only [h, ↓reduceIte]
+      rw [ih (hn := by omega)]
+      rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h]
+      rw [shiftLeft_or_eq_shiftLeft_shiftLeft_of_and_eq_zero]
+      · simp
+      · simp only [toNat_truncate, toNat_twoPow]
+        have hpow : 2 ^ (n + 1) < 2 ^ w₂ := by
+          apply Nat.pow_lt_pow_of_lt (by decide) (by omega)
+        have h₂ : 2 ^ (n + 1) % 2 ^ w₂ = 2 ^ (n + 1) := Nat.mod_eq_of_lt (by omega)
+        have h₁ : y.toNat % 2 ^ (n + 1) % 2 ^ w₂ = y.toNat % 2 ^ (n + 1) := by
+          apply Nat.mod_eq_of_lt
+          apply Nat.lt_of_lt_of_le (m := 2 ^ (n + 1))
+          apply Nat.mod_lt
+          apply Nat.pow_pos (by decide); omega
+        obtain h₁ : y.toNat % 2 ^ (n + 1) % 2 ^ w₂ = y.toNat % 2 ^ (n + 1) := by
+          apply Nat.mod_eq_of_lt
+          apply Nat.lt_of_lt_of_le (m := 2 ^ (n + 1)) <;> omega
+        rw [h₁, h₂]
+        rcases w₂ with rfl | w₂
+        · omega
+        · apply Nat.add_lt_add_of_lt_of_le
+          · simp only [pow_eq, Nat.mul_eq, Nat.mul_one]
+            apply Nat.lt_of_lt_of_le (m := 2 ^ (n + 1))
+            · apply Nat.mod_lt
+              · apply Nat.pow_pos (by decide)
+            · apply Nat.pow_le_pow_of_le_right (by decide) (by omega)
+          · simp only [pow_eq]
+            apply Nat.pow_le_pow_of_le_right (by decide) (by omega)
+    · simp only [h, false_eq_true, ↓reduceIte, shiftLeft_zero']
+      rw [ih (hn := by omega)]
+      rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false (i := n + 1)]
+      simp [h]
+
+theorem shiftLeft_eq_shiftLeftRec (x : BitVec w₁) (y : BitVec w₂) :
+    x <<< y = shiftLeftRec x y (w₂ - 1) := by
+  rcases w₂ with rfl | w₂
+  · simp [of_length_zero]
+  · simp [shiftLeftRec_eq (x := x) (y := y) (n := w₂) (by omega)]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -436,6 +436,12 @@ theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
   have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
   omega
 
+/-- Truncating to width 1 produces a bitvector equal to the the LSB. -/
+theorem truncate_one_eq_ofBool_getLsb {x : BitVec w} :
+    x.truncate 1 = ofBool (x.getLsb 0) := by
+  ext i
+  simp [show i = 0 by omega]
+
 /-! ## extractLsb -/
 
 @[simp]
@@ -626,6 +632,10 @@ theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
   apply eq_of_toNat_eq
   simp
 
+@[simp]
+theorem zero_shiftLeft_eq (n : Nat) : (0#w) <<< n = 0 := by
+  simp [bv_toNat]
+
 @[simp] theorem getLsb_shiftLeft (x : BitVec m) (n) :
     getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsb x (i - n)) := by
   rw [← testBit_toNat, getLsb]
@@ -691,6 +701,20 @@ theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
     (x <<< n) <<< m = x <<< (n + m) := by
   rw [shiftLeft_add]
 
+/-! ### shiftLeft reductions from BitVec to Nat -/
+
+theorem shiftLeft_eq' {x : BitVec w} {y : BitVec w₂} :
+  x <<< y = x <<< y.toNat := by rfl
+
+@[simp]
+theorem shiftLeft_zero' {x : BitVec w} :
+    x <<< (0#w₂) = x := by
+  simp [shiftLeft_eq']
+
+theorem shiftLeft_shiftLeft' {x y z : BitVec w} :
+    x <<< y <<< z = x <<< (y.toNat + z.toNat) := by
+  simp [shiftLeft_eq', shiftLeft_add]
+
 /-! ### ushiftRight -/
 
 @[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -1471,6 +1495,27 @@ theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
       apply Nat.pow_dvd_pow 2 (by omega)
     simp [Nat.mul_mod, hpow]
 
+@[simp]
+theorem and_twoPow_eq_getLsb {x : BitVec w} {i : Nat} :
+    x &&& (twoPow w i) = if x.getLsb i then twoPow w i else 0#w := by
+  ext j
+  simp only [getLsb_and, getLsb_twoPow]
+  by_cases hj : i = j <;> by_cases hx : x.getLsb i <;> simp_all
+
+theorem BitVec.toNat_twoPow {w : Nat} {i : Nat} : (twoPow w i).toNat = 2^i % 2^w := by
+  rcases w with rfl | w
+  · simp [Nat.mod_one]
+  · simp [twoPow, toNat_shiftLeft]
+    have hone : 1 < 2 ^ (w + 1) := by
+      rw [show 1 = 2^0 by simp[Nat.pow_zero]]
+      exact Nat.pow_lt_pow_of_lt (by omega) (by omega)
+    simp [Nat.mod_eq_of_lt hone, Nat.shiftLeft_eq]
+
+@[simp]
+theorem twoPow_zero_eq_one {w : Nat} : twoPow w 0 = 1#w := by
+  apply eq_of_toNat_eq
+  simp
+
 /- ### zeroExtend, truncate, and bitwise operations -/
 
 /--