feat: if support and more in bv_decide (leanprover#5855)

Using the same strategy as leanprover#5852 this provides `bv_decide` support for
`Bool` and `BitVec` ifs
this in turn instantly enables support for:
- `sdiv`
- `smod`
- `abs`

and thus closes our last discrepancies to QF_BV!

Author: hargoniX

src/Init/Data/BitVec/Lemmas.lean

@@ -2115,6 +2115,8 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
 
 /-! ### abs -/
 
+theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
+
 @[simp, bv_toNat]
 theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
   simp only [BitVec.abs, neg_eq]

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

@@ -29,7 +29,6 @@ instance : ToExpr BVBinOp where
     | .mul => mkConst ``BVBinOp.mul
     | .udiv => mkConst ``BVBinOp.udiv
     | .umod => mkConst ``BVBinOp.umod
-    | .sdiv => mkConst ``BVBinOp.sdiv
   toTypeExpr := mkConst ``BVBinOp
 
 instance : ToExpr BVUnOp where
@@ -103,6 +102,7 @@ where
   | .const b => mkApp2 (mkConst ``BoolExpr.const) (toTypeExpr α) (toExpr b)
   | .not x => mkApp2 (mkConst ``BoolExpr.not) (toTypeExpr α) (go x)
   | .gate g x y => mkApp4 (mkConst ``BoolExpr.gate) (toTypeExpr α) (toExpr g) (go x) (go y)
+  | .ite d l r => mkApp4 (mkConst ``BoolExpr.ite) (toTypeExpr α) (go d) (go l) (go r)
 
 
 open Lean.Meta

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

@@ -57,7 +57,8 @@ Construct the reified version of applying the gate in `gate` to `lhs` and `rhs`.
 This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
 and `rhs`.
 -/
-def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) : M ReifiedBVLogical := do
+def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) :
+    M ReifiedBVLogical := do
   let congrThm := congrThmOfGate gate
   let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr
   let expr :=
@@ -99,6 +100,35 @@ def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
     return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
   return ⟨boolExpr, proof, expr⟩
 
+/--
+Construct the reified version of `if discrExpr then lhsExpr else rhsExpr`.
+This function assumes that `discrExpr`, lhsExpr` and `rhsExpr` are the corresponding expressions to
+`discr`, `lhs` and `rhs`.
+-/
+def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) :
+    M ReifiedBVLogical := do
+  let boolExpr := .ite discr.bvExpr lhs.bvExpr rhs.bvExpr
+  let expr :=
+    mkApp4
+      (mkConst ``BoolExpr.ite)
+      (mkConst ``BVPred)
+      discr.expr
+      lhs.expr
+      rhs.expr
+  let proof := do
+    let discrEvalExpr ← ReifiedBVLogical.mkEvalExpr discr.expr
+    let lhsEvalExpr ← ReifiedBVLogical.mkEvalExpr lhs.expr
+    let rhsEvalExpr ← ReifiedBVLogical.mkEvalExpr rhs.expr
+    let discrProof ← discr.evalsAtAtoms
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
+    return mkApp9
+      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.ite_congr)
+      discrExpr lhsExpr rhsExpr
+      discrEvalExpr lhsEvalExpr rhsEvalExpr
+      discrProof lhsProof rhsProof
+  return ⟨boolExpr, proof, expr⟩
+
 end ReifiedBVLogical
 
 end Frontend

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

@@ -18,52 +18,55 @@ open Lean.Meta
 
 /--
 This function adds the two lemmas:
-- `boolExpr = true → atomExpr = 1#1`
-- `boolExpr = false → atomExpr = 0#1`
-It assumes that `boolExpr` and `atomExpr` are the expressions corresponding to `bool` and `atom`.
-Furthermore it assumes that `atomExpr` is of the form `BitVec.ofBool boolExpr`.
+- `discrExpr = true → atomExpr = lhsExpr`
+- `discrExpr = false → atomExpr = rhsExpr`
+It assumes that `discrExpr`, `lhsExpr` and `rhsExpr` are the expressions corresponding to `discr`,
+`lhs` and `rhs`. Furthermore it assumes that `atomExpr` is of the form
+`if discrExpr = true then lhsExpr else rhsExpr`.
 -/
-def addOfBoolLemmas (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
-    LemmaM Unit := do
-  let some ofBoolTrueLemma ← mkOfBoolTrueLemma bool atom boolExpr atomExpr | return ()
-  LemmaM.addLemma ofBoolTrueLemma
-  let some ofBoolFalseLemma ← mkOfBoolFalseLemma bool atom boolExpr atomExpr | return ()
-  LemmaM.addLemma ofBoolFalseLemma
+def addIfLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+    (discrExpr atomExpr lhsExpr rhsExpr : Expr) : LemmaM Unit := do
+  let some trueLemma ← mkIfTrueLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  LemmaM.addLemma trueLemma
+  let some falseLemma ← mkIfFalseLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  LemmaM.addLemma falseLemma
 where
-  mkOfBoolTrueLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
-      M (Option SatAtBVLogical) := mkOfBoolLemma bool atom boolExpr atomExpr true 1#1
+  mkIfTrueLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
+    mkIfLemma true discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
 
-  mkOfBoolFalseLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
-      M (Option SatAtBVLogical) := mkOfBoolLemma bool atom boolExpr atomExpr false 0#1
+  mkIfFalseLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
+    mkIfLemma false discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
 
-  mkOfBoolLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr)
-     (boolVal : Bool) (resVal : BitVec 1) : M (Option SatAtBVLogical) := do
+  mkIfLemma (discrVal : Bool) (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
+    let resExpr := if discrVal then lhsExpr else rhsExpr
+    let resValExpr := if discrVal then lhs else rhs
     let lemmaName :=
-      match boolVal with
-      | .true => ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_true
-      | .false => ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_false
+      if discrVal then
+        ``Std.Tactic.BVDecide.Reflect.BitVec.if_true
+      else
+        ``Std.Tactic.BVDecide.Reflect.BitVec.if_false
+    let discrValExpr := toExpr discrVal
+    let discrVal ← ReifiedBVLogical.mkBoolConst discrVal
 
-    let boolValExpr := toExpr boolVal
-    let boolVal ← ReifiedBVLogical.mkBoolConst boolVal
-    let resExpr := toExpr resVal
-    let resValExpr ← ReifiedBVExpr.mkBVConst resVal
+    let eqDiscrExpr ← mkAppM ``BEq.beq #[discrExpr, discrValExpr]
+    let eqDiscr ← ReifiedBVLogical.mkGate discr discrVal discrExpr discrValExpr .beq
 
-    let eqBoolExpr ← mkAppM ``BEq.beq #[boolExpr, boolValExpr]
-    let eqBool ← ReifiedBVLogical.mkGate bool boolVal boolExpr boolValExpr .beq
-
-    let eqBVExpr ← mkAppM ``BEq.beq #[mkApp (mkConst ``BitVec.ofBool) boolExpr, resExpr]
+    let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
     let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
     let trueExpr := mkConst ``Bool.true
-    let impExpr ← mkArrow (← mkEq eqBoolExpr trueExpr) (← mkEq eqBVExpr trueExpr)
+    let impExpr ← mkArrow (← mkEq eqDiscrExpr trueExpr) (← mkEq eqBVExpr trueExpr)
     let decideImpExpr ← mkAppOptM ``Decidable.decide #[some impExpr, none]
-    let imp ← ReifiedBVLogical.mkGate eqBool eqBV eqBoolExpr eqBVExpr .imp
+    let imp ← ReifiedBVLogical.mkGate eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
       let congrProof ← imp.evalsAtAtoms
-      let lemmaProof := mkApp (mkConst lemmaName) boolExpr
+      let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
       return mkApp4
         (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
         decideImpExpr

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

@@ -47,8 +47,6 @@ where
       binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
     | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
       binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
-    | BitVec.sdiv _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
     | Complement.complement _ _ innerExpr =>
       unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
     | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
@@ -207,11 +205,15 @@ where
         .rotateRight
         ``BVUnOp.rotateRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | BitVec.ofBool boolExpr =>
-      let some bool ← ReifiedBVLogical.of boolExpr | return none
-      let atomExpr := (mkApp (mkConst ``BitVec.ofBool) boolExpr)
-      let some atom ← ReifiedBVExpr.bitVecAtom atomExpr | return none
-      addOfBoolLemmas bool atom boolExpr atomExpr
+    | ite _ discrExpr _ lhsExpr rhsExpr =>
+      let_expr Eq α discrExpr val := discrExpr | return none
+      let_expr Bool := α | return none
+      let_expr Bool.true := val | return none
+      let some atom ← ReifiedBVExpr.bitVecAtom x | return none
+      let some discr ← ReifiedBVLogical.of discrExpr | return none
+      let some lhs ← goOrAtom lhsExpr | return none
+      let some rhs ← goOrAtom rhsExpr | return none
+      addIfLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
       return some atom
     | _ => return none
 
@@ -371,6 +373,14 @@ where
       | Bool => gateReflection lhsExpr rhsExpr .beq
       | BitVec _ => goPred t
       | _ => return none
+    | ite _ discrExpr _ lhsExpr rhsExpr =>
+      let_expr Eq α discrExpr val := discrExpr | return none
+      let_expr Bool := α | return none
+      let_expr Bool.true := val | return none
+      let some discr ← goOrAtom discrExpr | return none
+      let some lhs ← goOrAtom lhsExpr | return none
+      let some rhs ← goOrAtom rhsExpr | return none
+      return some (← ReifiedBVLogical.mkIte discr lhs rhs discrExpr lhsExpr rhsExpr)
     | _ => goPred t
 
   /--

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

@@ -128,6 +128,8 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
       else
         return .continue
 
+attribute [builtin_bv_normalize_proc↓] reduceIte
+
 /--
 A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
 the goal fully, indicated by returning `none`.

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -73,10 +73,6 @@ inductive BVBinOp where
   Unsigned modulo.
   -/
   | umod
-  /--
-  Signed division.
-  -/
-  | sdiv
 
 namespace BVBinOp
 
@@ -88,7 +84,6 @@ def toString : BVBinOp → String
   | mul => "*"
   | udiv => "/ᵤ"
   | umod => "%ᵤ"
-  | sdiv => "/ₛ"
 
 instance : ToString BVBinOp := ⟨toString⟩
 
@@ -103,7 +98,6 @@ def eval : BVBinOp → (BitVec w → BitVec w → BitVec w)
   | mul => (· * ·)
   | udiv => (· / ·)
   | umod => (· % · )
-  | sdiv => BitVec.sdiv
 
 @[simp] theorem eval_and : eval .and = ((· &&& ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_or : eval .or = ((· ||| ·) : BitVec w → BitVec w → BitVec w) := by rfl
@@ -112,7 +106,6 @@ def eval : BVBinOp → (BitVec w → BitVec w → BitVec w)
 @[simp] theorem eval_mul : eval .mul = ((· * ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_udiv : eval .udiv = ((· / ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_umod : eval .umod = ((· % ·) : BitVec w → BitVec w → BitVec w) := by rfl
-@[simp] theorem eval_sdiv : eval .sdiv = (BitVec.sdiv : BitVec w → BitVec w → BitVec w) := by rfl
 
 end BVBinOp
 
@@ -448,6 +441,8 @@ def eval (assign : BVExpr.Assignment) (expr : BVLogicalExpr) : Bool :=
 @[simp] theorem eval_const : eval assign (.const b) = b := rfl
 @[simp] theorem eval_not : eval assign (.not x) = !eval assign x := rfl
 @[simp] theorem eval_gate : eval assign (.gate g x y) = g.eval (eval assign x) (eval assign y) := rfl
+@[simp] theorem eval_ite :
+  eval assign (.ite d l r) = if (eval assign d) then (eval assign l) else (eval assign r) := rfl
 
 def Sat (x : BVLogicalExpr) (assign : BVExpr.Assignment) : Prop := eval assign x = true
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -21,7 +21,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.SignExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sdiv
 
 /-!
 This module contains the implementation of a bitblaster for `BitVec` expressions (`BVExpr`).
@@ -118,13 +117,6 @@ where
           dsimp only at hlaig hraig
           omega
         ⟨res, this⟩
-      | .sdiv =>
-        let res := bitblast.blastSdiv aig ⟨lhs, rhs⟩
-        have := by
-          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastSdiv)
-          dsimp only at hlaig hraig
-          omega
-        ⟨res, this⟩
     | .un op expr =>
       let ⟨⟨eaig, evec⟩, heaig⟩ := go aig expr
       match op with
@@ -235,7 +227,7 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) :
     rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
   | bin lhs op rhs lih rih =>
     match op with
-    | .and | .or | .xor | .add | .mul | .udiv | .umod | .sdiv =>
+    | .and | .or | .xor | .add | .mul | .udiv | .umod =>
       dsimp only [go]
       have := (bitblast.go aig lhs).property
       have := (go (go aig lhs).1.aig rhs).property