feat: get bv_normalize up to date with the current BitVec rewrites (#…

…5573)
leanprover · Oct 1, 2024 · 499c587 · 499c587
1 parent 863e9c0
commit 499c587
Show file tree

Hide file tree

Showing 3 changed files with 86 additions and 15 deletions.
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean
@@ -37,6 +37,33 @@ builtin_simproc [bv_normalize] eqToBEq (((_ : Bool) = (_ : Bool))) := fun e => d
     let proof := mkApp2 (mkConst ``Bool.eq_to_beq) lhs rhs
     return .done { expr := new, proof? := some proof }
 
+builtin_simproc [bv_normalize] andOnes ((_ : BitVec _) &&& (_ : BitVec _)) := fun e => do
+  let_expr HAnd.hAnd _ _ _ _ lhs rhs := e | return .continue
+  let some ⟨w, rhsValue⟩ ← getBitVecValue? rhs | return .continue
+  if rhsValue == -1#w then
+    let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.and_ones) (toExpr w) lhs
+    return .visit { expr := lhs, proof? := some proof }
+  else
+    return .continue
+
+builtin_simproc [bv_normalize] onesAnd ((_ : BitVec _) &&& (_ : BitVec _)) := fun e => do
+  let_expr HAnd.hAnd _ _ _ _ lhs rhs := e | return .continue
+  let some ⟨w, lhsValue⟩ ← getBitVecValue? lhs | return .continue
+  if lhsValue == -1#w then
+    let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.ones_and) (toExpr w) rhs
+    return .visit { expr := rhs, proof? := some proof }
+  else
+    return .continue
+
+builtin_simproc [bv_normalize] maxUlt (BitVec.ult (_ : BitVec _) (_ : BitVec _)) := fun e => do
+  let_expr BitVec.ult _ lhs rhs := e | return .continue
+  let some ⟨w, lhsValue⟩ ← getBitVecValue? lhs | return .continue
+  if lhsValue == -1#w then
+    let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.max_ult') (toExpr w) rhs
+    return .visit { expr := toExpr Bool.false, proof? := some proof }
+  else
+    return .continue
+
 /--
 A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
 the goal fully, indicated by returning `none`.

diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -51,9 +51,6 @@ section Constant
 
 attribute [bv_normalize] BitVec.add_zero
 attribute [bv_normalize] BitVec.zero_add
-attribute [bv_normalize] BitVec.neg_zero
-attribute [bv_normalize] BitVec.sub_self
-attribute [bv_normalize] BitVec.sub_zero
 attribute [bv_normalize] BitVec.setWidth_eq
 attribute [bv_normalize] BitVec.setWidth_zero
 attribute [bv_normalize] BitVec.getLsbD_zero
@@ -63,7 +60,6 @@ attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
 attribute [bv_normalize] BitVec.not_not
 
-
 end Constant
 
 @[bv_normalize]
@@ -76,13 +72,13 @@ theorem BitVec.and_zero (a : BitVec w) : a &&& 0#w = 0#w := by
   ext
   simp
 
-@[bv_normalize]
-theorem BitVec.and_ones (a : BitVec w) : (-1#w) &&& a = a := by
+-- Used in simproc because of - normalization
+theorem BitVec.ones_and (a : BitVec w) : (-1#w) &&& a = a := by
   ext
   simp [BitVec.negOne_eq_allOnes]
 
-@[bv_normalize]
-theorem BitVec.ones_and (a : BitVec w) : a &&& (-1#w) = a := by
+-- Used in simproc because of - normalization
+theorem BitVec.and_ones (a : BitVec w) : a &&& (-1#w) = a := by
   ext
   simp [BitVec.negOne_eq_allOnes]
 
@@ -112,14 +108,19 @@ theorem BitVec.not_add (a : BitVec w) : ~~~a + a = (-1#w) := by
   rw [BitVec.add_not]
 
 @[bv_normalize]
-theorem BitVec.add_neg (a : BitVec w) : a + (-a) = 0#w := by
+theorem BitVec.add_neg (a : BitVec w) : a + (~~~a + 1#w) = 0#w := by
+  rw [← BitVec.ofNat_eq_ofNat]
+  rw [← BitVec.neg_eq_not_add]
   rw [← BitVec.sub_toAdd]
   rw [BitVec.sub_self]
 
 @[bv_normalize]
-theorem BitVec.neg_add (a : BitVec w) : (-a) + a = 0#w := by
+theorem BitVec.neg_add (a : BitVec w) : (~~~a + 1#w) + a = 0#w := by
+  rw [← BitVec.ofNat_eq_ofNat]
+  rw [← BitVec.neg_eq_not_add]
   rw [BitVec.add_comm]
-  rw [BitVec.add_neg]
+  rw [← BitVec.sub_toAdd]
+  rw [BitVec.sub_self]
 
 @[bv_normalize]
 theorem BitVec.add_same (a : BitVec w) : a + a = a * 2#w := by
@@ -212,10 +213,12 @@ theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) :
   simp
 
 @[bv_normalize]
-theorem BitVec.ofBool_getElem (a : BitVec w) (i : Nat) (h : i < w) :
-    BitVec.ofBool a[i] = a.extractLsb' i 1 := by
-  rw [← BitVec.getLsbD_eq_getElem]
-  apply ofBool_getLsbD
+theorem BitVec.getElem_eq_getLsbD (a : BitVec w) (i : Nat) (h : i < w) :
+    a[i] = a.getLsbD i := by
+  simp [BitVec.getLsbD_eq_getElem?_getD, BitVec.getElem?_eq, h]
+
+attribute [bv_normalize] BitVec.add_eq_xor
+attribute [bv_normalize] BitVec.mul_eq_and
 
 end Normalize
 end Std.Tactic.BVDecide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
@@ -26,3 +26,44 @@ theorem mem_subset_refl : mem_subset a1 a2 a1 a2 := by
   unfold mem_subset
   bv_normalize
   sorry
+
+example {x : BitVec 16} : 0#16 + x = x := by bv_normalize
+example {x : BitVec 16} : x + 0#16 = x := by bv_normalize
+example {x : BitVec 16} : x.setWidth 16 = x := by bv_normalize
+example : (0#w).setWidth 32 = 0#32 := by bv_normalize
+example : (0#w).getLsbD i = false := by bv_normalize
+example {x : BitVec 0} : x.getLsbD i = false := by bv_normalize
+example {x : BitVec 16} {b : Bool} : (x.concat b).getLsbD 0 = b := by bv_normalize
+example {x : BitVec 16} : 1 * x = x := by bv_normalize
+example {x : BitVec 16} : x * 1 = x := by bv_normalize
+example {x : BitVec 16} : ~~~(~~~x) = x := by bv_normalize
+example {x : BitVec 16} : x &&& 0 = 0 := by bv_normalize
+example {x : BitVec 16} : 0 &&& x = 0 := by bv_normalize
+example {x : BitVec 16} : (-1#16) &&& x = x := by bv_normalize 
+example {x : BitVec 16} : x &&& (-1#16) = x := by bv_normalize
+example {x : BitVec 16} : x &&& x = x := by bv_normalize
+example {x : BitVec 16} : x &&& ~~~x = 0 := by bv_normalize
+example {x : BitVec 16} : ~~~x &&& x = 0 := by bv_normalize
+example {x : BitVec 16} : x + ~~~x = -1 := by bv_normalize
+example {x : BitVec 16} : ~~~x + x = -1 := by bv_normalize
+example {x : BitVec 16} : x + (-x) = 0 := by bv_normalize
+example {x : BitVec 16} : (-x) + x = 0 := by bv_normalize
+example {x : BitVec 16} : x + x = x * 2 := by bv_normalize
+example : BitVec.sshiftRight 0#16 n = 0#16 := by bv_normalize
+example {x : BitVec 16} : BitVec.sshiftRight x 0 = x := by bv_normalize
+example {x : BitVec 16} : 0#16 * x = 0 := by bv_normalize
+example {x : BitVec 16} : x * 0#16 = 0 := by bv_normalize
+example {x : BitVec 16} : x <<< 0#16 = x := by bv_normalize
+example {x : BitVec 16} : x <<< 0 = x := by bv_normalize
+example : 0#16 <<< (n : Nat) = 0 := by bv_normalize
+example : 0#16 >>> (n : Nat) = 0 := by bv_normalize
+example {x : BitVec 16} : x >>> 0#16 = x := by bv_normalize
+example {x : BitVec 16} : x >>> 0 = x := by bv_normalize
+example {x : BitVec 16} : 0 < x ↔ (0 != x) := by bv_normalize
+example {x : BitVec 16} : ¬(-1#16 < x) := by bv_normalize
+example {x : BitVec 16} : BitVec.replicate 0 x = 0 := by bv_normalize
+example {x : BitVec 16} : BitVec.ofBool (x.getLsbD i) = x.extractLsb' i 1 := by bv_normalize
+example {x : BitVec 16} {i} {h} : BitVec.ofBool (x[i]'h) = x.extractLsb' i 1 := by bv_normalize
+example {x : BitVec 16} {i} {h} : x[i] = x.getLsbD i := by bv_normalize
+example {x y : BitVec 1} : x + y = x ^^^ y := by bv_normalize
+example {x y : BitVec 1} : x * y = x &&& y := by bv_normalize