feat: BitVec.extractLsb'_add_eq (#7595)

This PR implements the addition rewrite from the Bitwuzla rewrite
[BV_EXTRACT_ADD_MUL](e09c50818b/src/rewrite/rewrites_bv.cpp (L1495-L1510)),
which witness that the high bits at `i >= len` do not affect the bits of
the sum upto `len`:

```lean
theorem extractLsb'_add {w len} {x y : BitVec w} (hlen : len ≤ w) : 
    (x + y).extractLsb' 0 len = x.extractLsb' 0 len + y.extractLsb' 0 len
```

---------

Co-authored-by: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>

src/Init/Data/BitVec/Bitblast.lean

@@ -1350,4 +1350,29 @@ theorem eq_iff_eq_of_inv (f : α → BitVec w) (g : BitVec w → α) (h : ∀ x,
     have := congrArg g h'
     simpa [h] using this
 
+/-! ### Lemmas that use Bitblasting Infrastructure -/
+
+/-- The value of `(carry i x y false)` can be computed by truncating `x` and `y`
+to `len` bits where `len ≥ i`. -/
+theorem carry_extractLsb'_eq_carry {w i len : Nat} (hi : i < len)
+    {x y : BitVec w} {b : Bool}: 
+    (carry i (extractLsb' 0 len x) (extractLsb' 0 len y) b)
+    = (carry i x y b) := by
+  simp only [carry, extractLsb'_toNat, shiftRight_zero, toNat_false, Nat.add_zero, ge_iff_le,
+    decide_eq_decide]
+  have : 2 ^ i ∣ 2^len := by
+    apply Nat.pow_dvd_pow
+    omega
+  rw [Nat.mod_mod_of_dvd _ this, Nat.mod_mod_of_dvd _ this]
+
+/--
+The `[0..len)` low bits of `x + y` can be computed by truncating `x` and `y`
+to `len` bits and then adding.
+-/
+theorem extractLsb'_add {w len : Nat} {x y : BitVec w} (hlen : len ≤ w) : 
+    (x + y).extractLsb' 0 len = x.extractLsb' 0 len + y.extractLsb' 0 len := by
+  ext i hi
+  rw [getElem_extractLsb', Nat.zero_add, getLsbD_add (by omega)]
+  simp [getElem_add, carry_extractLsb'_eq_carry hi, getElem_extractLsb', Nat.zero_add]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -1081,6 +1081,17 @@ theorem getElem_eq_extractLsb' (x : BitVec w) (i : Nat) (h : i < w) :
     x[i] = (x.extractLsb' i 1 == 1#1) := by
   rw [← getLsbD_eq_getElem, getLsbD_eq_extractLsb']
 
+@[simp]
+theorem extractLsb'_zero {w start len : Nat} : (0#w).extractLsb' start len = 0#len := by
+  apply eq_of_toNat_eq
+  simp [extractLsb']
+
+@[simp]
+theorem extractLsb'_eq_zero {x : BitVec w} {start : Nat} :
+    x.extractLsb' start 0 = 0#0 := by
+  ext i hi
+  omega
+
 /-! ### allOnes -/
 
 @[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by