From 1036512a1cd6a3384031a7ba64584fa5bb359690 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Mon, 24 Mar 2025 09:23:03 +0000 Subject: [PATCH] feat: BitVec.extractLsb'_mul_eq (#7594) This PR implements the Bitwuzla rewrites [BV_EXTRACT_ADD_MUL](https://github.com/bitwuzla/bitwuzla/blob/e09c50818b798f990bd84bf61174553fef46d561/src/rewrite/rewrites_bv.cpp#L1495-L1510), which witness that the high bits at `i >= len` do not affect the bits of the product upto `len`. ```lean theorem extractLsb'_mul {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: Alex Keizer --- src/Init/Data/BitVec/Bitblast.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index d73f3b1a8d..aadc5e03f7 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -682,6 +682,12 @@ theorem getLsbD_mul (x y : BitVec w) (i : Nat) : · simp · omega +theorem mul_eq_mulRec {x y : BitVec w} : + x * y = mulRec x y w := by + apply eq_of_getLsbD_eq + intro i hi + apply getLsbD_mul + theorem getMsbD_mul (x y : BitVec w) (i : Nat) : (x * y).getMsbD i = (mulRec x y w).getMsbD i := by simp only [mulRec_eq_mul_signExtend_setWidth] @@ -1414,4 +1420,17 @@ theorem extractLsb'_add {w len : Nat} {x y : BitVec w} (hlen : len ≤ w) : rw [getElem_extractLsb', Nat.zero_add, getLsbD_add (by omega)] simp [getElem_add, carry_extractLsb'_eq_carry hi, getElem_extractLsb', Nat.zero_add] +-- `setWidth` commutes with multiplication. -/ +theorem setWidth_mul {w len} {x y : BitVec w} (hlen : len ≤ w) : + (x * y).setWidth len = (x.setWidth len) * (y.setWidth len) := by + apply eq_of_toNat_eq + simp only [toNat_setWidth, toNat_mul, mul_mod_mod, mod_mul_mod] + rw [Nat.mod_mod_of_dvd] + exact pow_dvd_pow_iff_le_right'.mpr hlen + +/-- `extractLsb'` commutes with multiplication. -/ +theorem extractLsb'_mul {w len} {x y : BitVec w} (hlen : len ≤ w) : + (x * y).extractLsb' 0 len = (x.extractLsb' 0 len) * (y.extractLsb' 0 len) := by + simp [← setWidth_eq_extractLsb' hlen, setWidth_mul hlen] + end BitVec