feat: enhance the rewriting rules of bv_decide (#5423)

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -219,19 +219,20 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
       sats := sats.push reflected
     else
       unusedHypotheses := unusedHypotheses.insert hyp
-  if sats.size = 0 then
+  if h : sats.size = 0 then
     let mut error := "None of the hypotheses are in the supported BitVec fragment.\n"
     error := error ++ "There are two potential fixes for this:\n"
     error := error ++ "1. If you are using custom BitVec constructs simplify them to built-in ones.\n"
     error := error ++ "2. If your problem is using only built-in ones it might currently be out of reach.\n"
     error := error ++ "   Consider expressing it in terms of different operations that are better supported."
     throwError error
-  let sat := sats.foldl (init := SatAtBVLogical.trivial) SatAtBVLogical.and
-  return {
-    bvExpr := sat.bvExpr,
-    proveFalse := sat.proveFalse,
-    unusedHypotheses := unusedHypotheses
-  }
+  else
+    let sat := sats[1:].foldl (init := sats[0]) SatAtBVLogical.and
+    return {
+      bvExpr := sat.bvExpr,
+      proveFalse := sat.proveFalse,
+      unusedHypotheses := unusedHypotheses
+    }
 
 
 def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean

@@ -61,14 +61,6 @@ partial def of (h : Expr) : M (Option SatAtBVLogical) := do
     return some ⟨bvLogical.bvExpr, proof, bvLogical.expr⟩
   | _ => return none
 
-/--
-The trivially true `BVLogicalExpr`.
--/
-def trivial : SatAtBVLogical where
-  bvExpr := .const true
-  expr := toExpr (.const true : BVLogicalExpr)
-  satAtAtoms := return mkApp (mkConst ``BVLogicalExpr.sat_true) (← M.atomsAssignment)
-
 /--
 Logical conjunction of two `ReifiedBVLogical`.
 -/

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -27,18 +27,6 @@ namespace Frontend.Normalize
 open Lean.Meta
 open Std.Tactic.BVDecide.Normalize
 
-/--
-The bitblaster for multiplication introduces symbolic branches over the right hand side.
-If we have an expression of the form `c * x` where `c` is constant we should change it to `x * c`
-such that these symbolic branches get constant folded by the AIG framework.
--/
-builtin_simproc [bv_normalize] mulConst ((_ : BitVec _) * (_ : BitVec _)) := fun e => do
-  let_expr HMul.hMul _ _ _ _ lhs rhs := e | return .continue
-  let some ⟨width, _⟩ ← Lean.Meta.getBitVecValue? lhs | return .continue
-  let new ← mkAppM ``HMul.hMul #[rhs, lhs]
-  let proof := mkApp3 (mkConst ``BitVec.mul_comm) (toExpr width) lhs rhs
-  return .done { expr := new, proof? := some proof }
-
 builtin_simproc [bv_normalize] eqToBEq (((_ : Bool) = (_ : Bool))) := fun e => do
   let_expr Eq _ lhs rhs := e | return .continue
   match_expr rhs with
@@ -65,6 +53,7 @@ def bvNormalize (g : MVarId) : MetaM Result := do
     let sevalSimprocs ← Simp.getSEvalSimprocs
 
     let simpCtx : Simp.Context := {
+      config := { failIfUnchanged := false, zetaDelta := true }
       simpTheorems := #[bvThms, sevalThms]
       congrTheorems := (← getSimpCongrTheorems)
     }

src/Std/Sat/AIG/RefVec.lean

@@ -150,6 +150,14 @@ theorem get_out_bound (s : RefVec aig len) (idx : Nat) (alt : Ref aig) (hidx : l
   · omega
   · rfl
 
+def countKnown [Inhabited α] (aig : AIG α) (s : RefVec aig len) : Nat := Id.run do
+  let folder acc ref :=
+    let decl := aig.decls[ref]!
+    match decl with
+    | .const .. => acc + 1
+    | _ => acc
+  return s.refs.foldl (init := 0) folder
+
 end RefVec
 
 structure BinaryRefVec (aig : AIG α) (len : Nat) where

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean

@@ -27,36 +27,35 @@ namespace BVExpr
 namespace bitblast
 
 def blastMul (aig : AIG BVBit) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry BVBit w :=
-  if h : w = 0 then
-    ⟨aig, h ▸ .empty⟩
+  if input.lhs.countKnown < input.rhs.countKnown then
+    blast aig input
   else
-    /-
-    theorem mulRec_zero_eq (l r : BitVec w) :
-        mulRec l r 0 = if r.getLsb 0 then l else 0 := by
-    -/
-    have : 0 < w := by omega
-    let res := blastConst aig 0
-    let aig := res.aig
-    let zero := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastConst) ..
-    let input := input.cast this
     let ⟨lhs, rhs⟩ := input
-    let res := AIG.RefVec.ite aig ⟨rhs.get 0 (by assumption), lhs, zero⟩
-    let aig := res.aig
-    let acc := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    go aig lhs rhs 1 (by omega) acc
+    blast aig ⟨rhs, lhs⟩
 where
+  blast (aig : AIG BVBit) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry BVBit w :=
+    if h : w = 0 then
+      ⟨aig, h ▸ .empty⟩
+    else
+      have : 0 < w := by omega
+      let res := blastConst aig 0
+      let aig := res.aig
+      let zero := res.vec
+      have := AIG.LawfulVecOperator.le_size (f := blastConst) ..
+      let input := input.cast this
+      let ⟨lhs, rhs⟩ := input
+      let res := AIG.RefVec.ite aig ⟨rhs.get 0 (by assumption), lhs, zero⟩
+      let aig := res.aig
+      let acc := res.vec
+      have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
+      let lhs := lhs.cast this
+      let rhs := rhs.cast this
+      go aig lhs rhs 1 (by omega) acc
+
   go (aig : AIG BVBit) (lhs rhs : AIG.RefVec aig w) (curr : Nat) (hcurr : curr ≤ w)
       (acc : AIG.RefVec aig w) :
       AIG.RefVecEntry BVBit w :=
     if h : curr < w then
-      /-
-      theorem mulRec_succ_eq (l r : BitVec w) (s : Nat) :
-          mulRec l r (s + 1) = mulRec l r s + if r.getLsb (s + 1) then (l <<< (s + 1)) else 0
-      -/
       let res := blastShiftLeftConst aig ⟨lhs, curr⟩
       let aig := res.aig
       let shifted := res.vec
@@ -120,12 +119,10 @@ theorem go_decl_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr ≤ w)
       assumption
   · simp [← hgo]
 
-end blastMul
-
-instance : AIG.LawfulVecOperator BVBit AIG.BinaryRefVec blastMul where
+instance : AIG.LawfulVecOperator BVBit AIG.BinaryRefVec blast where
   le_size := by
     intros
-    unfold blastMul
+    unfold blast
     split
     · simp
     · dsimp only
@@ -134,7 +131,7 @@ instance : AIG.LawfulVecOperator BVBit AIG.BinaryRefVec blastMul where
       apply AIG.LawfulVecOperator.le_size (f := blastConst)
   decl_eq := by
     intros
-    unfold blastMul
+    unfold blast
     split
     · simp
     · dsimp only
@@ -147,6 +144,18 @@ instance : AIG.LawfulVecOperator BVBit AIG.BinaryRefVec blastMul where
         apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
         assumption
 
+end blastMul
+
+instance : AIG.LawfulVecOperator BVBit AIG.BinaryRefVec blastMul where
+  le_size := by
+    intros
+    unfold blastMul
+    split <;> apply AIG.LawfulVecOperator.le_size (f := blastMul.blast)
+  decl_eq := by
+    intros
+    unfold blastMul
+    split <;> rw [AIG.LawfulVecOperator.decl_eq (f := blastMul.blast)]
+
 end bitblast
 end BVExpr
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean

@@ -107,21 +107,18 @@ decreasing_by
   simp only [InvImage, WellFoundedRelation.rel, Nat.lt_wfRel, sizeOf_nat, Nat.lt_eq, gt_iff_lt]
   omega
 
-
-end blastMul
-
-theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment)
+theorem denote_blast (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment)
       (input : BinaryRefVec aig w)
       (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsbD idx)
       (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsbD idx) :
       ∀ (idx : Nat) (hidx : idx < w),
-        ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
+        ⟦(blast aig input).aig, (blast aig input).vec.get idx hidx, assign.toAIGAssignment⟧
           =
         (lhs * rhs).getLsbD idx := by
   intro idx hidx
   rw [BitVec.getLsbD_mul]
-  generalize hb : blastMul aig input = res
-  unfold blastMul at hb
+  generalize hb : blast aig input = res
+  unfold blast at hb
   dsimp only at hb
   split at hb
   · omega
@@ -130,7 +127,7 @@ theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignm
     rcases this with ⟨w, hw⟩
     subst hw
     rw [← hb]
-    rw [blastMul.go_denote_eq]
+    rw [go_denote_eq]
     · intro idx hidx
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
@@ -164,6 +161,25 @@ theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignm
           · simp [Ref.hgate]
         · omega
 
+
+end blastMul
+
+theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment)
+      (input : BinaryRefVec aig w)
+      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsbD idx)
+      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsbD idx) :
+      ∀ (idx : Nat) (hidx : idx < w),
+        ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
+          =
+        (lhs * rhs).getLsbD idx := by
+  intro idx hidx
+  generalize hb : blastMul aig input = res
+  unfold blastMul at hb
+  dsimp only at hb
+  split at hb
+  · rw [← hb, blastMul.denote_blast] <;> assumption
+  · rw [BitVec.mul_comm, ← hb, blastMul.denote_blast] <;> assumption
+
 end bitblast
 end BVExpr
 

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -39,9 +39,7 @@ attribute [bv_normalize] BitVec.msb_eq_getLsbD_last
 attribute [bv_normalize] BitVec.slt_eq_ult
 attribute [bv_normalize] BitVec.sle_eq_not_slt
 
-@[bv_normalize]
-theorem BitVec.OfNat_reduce (n : Nat) : OfNat.ofNat n = BitVec.ofNat w n := by
-  rfl
+attribute [bv_normalize] BitVec.ofNat_eq_ofNat
 
 @[bv_normalize]
 theorem BitVec.ofNatLt_reduce (n : Nat) (h) : BitVec.ofNatLt n h = BitVec.ofNat w n := by
@@ -121,6 +119,10 @@ theorem BitVec.neg_add (a : BitVec w) : (-a) + a = 0#w := by
   rw [BitVec.add_comm]
   rw [BitVec.add_neg]
 
+@[bv_normalize]
+theorem BitVec.add_same (a : BitVec w) : a + a = a * 2#w := by
+  rw [BitVec.mul_two]
+
 @[bv_normalize]
 theorem BitVec.zero_sshiftRight : BitVec.sshiftRight 0#w a = 0#w := by
   ext
@@ -190,13 +192,13 @@ theorem BitVec.zero_ult' (a : BitVec w) : (BitVec.ult 0#w a) = (0#w != a) := by
   | false => simp_all
 
 theorem BitVec.max_ult (a : BitVec w) : ¬ ((-1#w) < a) := by
-rcases w with rfl | w
-· simp [bv_toNat, BitVec.toNat_of_zero_length]
-· simp only [BitVec.lt_def, BitVec.toNat_neg, BitVec.toNat_ofNat, Nat.not_lt]
-  rw [Nat.mod_eq_of_lt (a := 1) (by simp)];
-  rw [Nat.mod_eq_of_lt]
-  · omega
-  · apply Nat.sub_one_lt_of_le (Nat.pow_pos (by omega)) (Nat.le_refl ..)
+  rcases w with rfl | w
+  · simp [bv_toNat, BitVec.toNat_of_zero_length]
+  · simp only [BitVec.lt_def, BitVec.toNat_neg, BitVec.toNat_ofNat, Nat.not_lt]
+    rw [Nat.mod_eq_of_lt (a := 1) (by simp)];
+    rw [Nat.mod_eq_of_lt]
+    · omega
+    · apply Nat.sub_one_lt_of_le (Nat.pow_pos (by omega)) (Nat.le_refl ..)
 
 @[bv_normalize]
 theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -16,10 +16,6 @@ namespace Normalize
 
 attribute [bv_normalize] Bool.not_true
 attribute [bv_normalize] Bool.not_false
-attribute [bv_normalize] Bool.or_true
-attribute [bv_normalize] Bool.true_or
-attribute [bv_normalize] Bool.or_false
-attribute [bv_normalize] Bool.false_or
 attribute [bv_normalize] Bool.and_true
 attribute [bv_normalize] Bool.true_and
 attribute [bv_normalize] Bool.and_false
@@ -48,5 +44,8 @@ attribute [bv_normalize] Bool.and_self_right
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide
 
+@[bv_normalize]
+theorem Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b) := by decide
+
 end Normalize
 end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Normalize/Prop.lean

@@ -18,6 +18,11 @@ attribute [bv_normalize] and_true
 attribute [bv_normalize] true_and
 attribute [bv_normalize] or_true
 attribute [bv_normalize] true_or
+attribute [bv_normalize] eq_iff_iff
+attribute [bv_normalize] iff_true
+attribute [bv_normalize] true_iff
+attribute [bv_normalize] iff_false
+attribute [bv_normalize] false_iff
 
 end Frontend.Normalize
 end Std.Tactic.BVDecide

tests/lean/run/bv_decide_rewriter.lean

@@ -0,0 +1,11 @@
+import Std.Tactic.BVDecide
+
+theorem x_eq_y (x y : Bool) (hx : x = True) (hy : y = True) : x = y := by
+  bv_decide
+
+example (z : BitVec 64) : True := by
+  let x : BitVec 64 := 10
+  let y : BitVec 64 := 20 + z
+  have : z + (2 * x) = y := by
+    bv_decide
+  exact True.intro