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

feat: BitVec.add_shiftLeft_eq_or_shiftLeft (#7761)

Browse source 
This PR implements the core theorem for the Bitwuzla rewrites
[NORM_BV_NOT_OR_SHL](e09c50818b/src/rewrite/rewrites_bv.cpp (L1495-L1510))
and
[BV_ADD_SHL](e09c50818b/src/rewrite/rewrites_bv.cpp (L395-L401)),
which convert the mixed-boolean-arithmetic expression into a purely
arithmetic expression:

```lean
theorem add_shiftLeft_eq_or_shiftLeft {x y : BitVec w} :
    x + (y <<< x) =  x ||| (y <<< x)
```
This commit is contained in:
Siddharth 2025-04-02 11:06:33 +01:00 • committed by GitHub
parent 336b68ec20
commit fe986b4533
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1757,4 +1757,17 @@ theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
(x ++ 0#w) + (0#v ++ y) = x ++ y := by
rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
/-- Heuristically, `y <<< x` is much larger than `x`,
and hence low bits of `y <<< x`. Thus, `x + (y <<< x) = x ||| (y <<< x).` -/
theorem add_shifLeft_eq_or_shiftLeft {x y : BitVec w} :
x + (y <<< x) = x ||| (y <<< x) := by
rw [add_eq_or_of_and_eq_zero]
ext i hi
simp only [shiftLeft_eq', getElem_and, getElem_shiftLeft, getElem_zero, and_eq_false_imp,
not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, Nat.not_lt]
intros hxi hxval
have : 2^i ≤ x.toNat := two_pow_le_toNat_of_getElem_eq_true hi hxi
have : i < 2^i := by exact Nat.lt_two_pow_self
omega
end BitVec

6
src/Init/Data/BitVec/Lemmas.lean
View file

@ -136,6 +136,12 @@ protected theorem toNat_lt_twoPow_of_le (h : m ≤ n) {x : BitVec m} :
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
theorem two_pow_le_toNat_of_getElem_eq_true {i : Nat} {x : BitVec w}
(hi : i < w) (hx : x[i] = true) : 2^i ≤ x.toNat := by
apply Nat.testBit_implies_ge
rw [← getElem_eq_testBit_toNat x i hi]
exact hx
theorem getMsb'_eq_getLsb' (x : BitVec w) (i : Fin w) :
x.getMsb' i = x.getLsb' ⟨w - 1 - i, by omega⟩ := by
simp only [getMsb', getLsb']