max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: BitVec.extractLsb'_mul_eq (#7594)

Browse source 
This PR implements the Bitwuzla rewrites
[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 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 <alex@keizer.dev>
This commit is contained in:
Siddharth 2025-03-24 09:23:03 +00:00 • committed by GitHub
parent 407a92a827
commit 1036512a1c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Init/Data/BitVec/Bitblast.lean
View file

@ -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