WIP: use bool sort

Blase/Blase/MultiWidth/Defs.lean

@@ -147,6 +147,7 @@ inductive Term {wcard tcard : Nat} (bcard : Nat)
 | sext (a : Term bcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard tctx (.bv v)
 -- | bvOfBool (b : Term bcard tctx .bool) : Term bcard tctx (.bv (.const 1))
 -- | boolMsb (w : WidthExpr wcard) (x : Term bcard tctx (.bv w)) : Term bcard tctx .bool
+| ult (x y : Term bcard tctx (.bv w)) : Term bcard tctx .bool
 | boolConst (b : Bool) : Term bcard tctx .bool
 | boolVar (v : Fin bcard) : Term bcard tctx .bool
 
@@ -224,6 +225,7 @@ def TermKind.denote (wenv : WidthExpr.Env wcard) : TermKind wcard → Type
 | .bool => Bool
 | .bv w => BitVec (w.toNat wenv)
 
+-- TODO: fix name and doc
 /-- Evaluate a term to get a concrete bitvector expression. -/
 def Term.toBV {wenv : WidthExpr.Env wcard}
     {tctx : Term.Ctx wcard tcard}
@@ -232,6 +234,7 @@ def Term.toBV {wenv : WidthExpr.Env wcard}
   Term bcard tctx k → k.denote wenv
 | .ofNat w n => BitVec.ofNat (w.toNat wenv) n
 | .boolConst b => b
+| .ult x y => (x.toBV benv tenv).ult (y.toBV benv tenv)
 | .var v => tenv.get v.1 v.2
 | .add (w := w) a b =>
     let a : BitVec (w.toNat wenv) := (a.toBV benv tenv)
@@ -256,13 +259,6 @@ def Term.toBV {wenv : WidthExpr.Env wcard}
     ~~~ a
 | .boolVar v => benv v
 
-def BoolExpr.toBool
-    {tctx : Term.Ctx wcard tcard}
-    (benv : Term.BoolEnv bcard)  :
-  Term bcard tctx .bool → Bool
-| .boolVar v => benv v
-| .boolConst b => b
-
 @[simp]
 theorem Term.toBV_ofNat
     {tctx : Term.Ctx wcard tcard}
@@ -328,6 +324,7 @@ deriving DecidableEq, Repr, Inhabited, Lean.ToExpr
 
 inductive BoolBinaryRelationKind
 | eq
+| ne
 deriving DecidableEq, Repr, Inhabited, Lean.ToExpr
 
 inductive Predicate :
@@ -381,6 +378,7 @@ def Predicate.toProp {wcard tcard bcard pcard : Nat} {wenv : WidthExpr.Env wcard
     match rel with
     -- | TODO: rename 'toBV' to 'toBool'.
     | .eq => (a.toBV benv tenv) = (b.toBV benv tenv)
+    | .ne => (a.toBV benv tenv) ≠ (b.toBV benv tenv)
 namespace Nondep
 
 inductive WidthExpr where
@@ -442,6 +440,7 @@ inductive Term
 | band (w : WidthExpr) (a b : Term) : Term
 | bxor (w : WidthExpr) (a b : Term) : Term
 | bnot (w : WidthExpr)  (a : Term) : Term
+| boolUlt (w : WidthExpr) (a b : Term) : Term
 | boolVar (v : Nat) : Term
 | boolConst (b : Bool) : Term
 deriving DecidableEq, Inhabited, Repr, Lean.ToExpr
@@ -463,6 +462,7 @@ def Term.ofDep {wcard tcard bcard : Nat}
   | .band (w := w) a b => .band (.ofDep w) (.ofDep a) (.ofDep b)
   | .bxor (w := w) a b => .bxor (.ofDep w) (.ofDep a) (.ofDep b)
   | .bnot (w := w) a => .bnot (.ofDep w) (.ofDep a)
+  | .ult (w := w) x y => .boolUlt (.ofDep w) (.ofDep x) (.ofDep y)
   | .boolVar v => .boolVar v
   | .boolConst b => .boolConst b
 
@@ -484,6 +484,7 @@ def Term.width (t : Term) : WidthExpr :=
   | .band w _a _b => w
   | .bxor w _a _b => w
   | .bnot w _a => w
+  | .boolUlt w _a _b => w
   | .boolVar _v => WidthExpr.const 1 -- dummy width.
   | .boolConst _b => WidthExpr.const 1
 
@@ -528,6 +529,7 @@ def Term.tcard (t : Term) : Nat :=
   | .band _w a b => (max (Term.tcard a) (Term.tcard b))
   | .bxor _w a b => (max (Term.tcard a) (Term.tcard b))
   | .bnot _w a => (Term.tcard a)
+  | .boolUlt _w a b => max (Term.tcard a) (Term.tcard b)
   | .boolVar _v => 0
   | .boolConst _b => 0
 
@@ -542,6 +544,7 @@ def Term.bcard (t : Term) : Nat :=
   | .band _w a b => (max (Term.bcard a) (Term.bcard b))
   | .bxor _w a b => (max (Term.bcard a) (Term.bcard b))
   | .bnot _w a => (Term.bcard a)
+  | .boolUlt _w a b => max (Term.bcard a) (Term.bcard b)
   | .boolVar v => v + 1
   | .boolConst _b => 0
 
@@ -569,7 +572,7 @@ def Predicate.wcard (p : Predicate) : Nat :=
   | .binRel .slt w _a _b => w.wcard
   | .or p1 p2 => max (Predicate.wcard p1) (Predicate.wcard p2)
   | .and p1 p2 => max (Predicate.wcard p1) (Predicate.wcard p2)
-  | .boolBinRel .eq a b => max (a.wcard) (b.wcard)
+  | .boolBinRel _ a b => max (a.wcard) (b.wcard)
 def Predicate.tcard (p : Predicate) : Nat :=
   match p with
   | .var _ => 0
@@ -582,7 +585,7 @@ def Predicate.tcard (p : Predicate) : Nat :=
   | .binRel .slt w _a _b => w.wcard
   | .or p1 p2 => max (Predicate.tcard p1) (Predicate.tcard p2)
   | .and p1 p2 => max (Predicate.tcard p1) (Predicate.tcard p2)
-  | .boolBinRel .eq a b => max (a.tcard) (b.tcard)
+  | .boolBinRel _ a b => max (a.tcard) (b.tcard)
 
 def Predicate.pcard (p : Predicate) : Nat :=
   match p with
@@ -609,6 +612,7 @@ def Predicate.ofDep {wcard tcard pcard : Nat}
   | .or p1 p2 => .or (.ofDep p1) (.ofDep p2)
   | .and p1 p2 => .and (.ofDep p1) (.ofDep p2)
   | .boolBinRel .eq a b => .boolBinRel .eq (.ofDep a) (.ofDep b)
+  | .boolBinRel .ne a b => .boolBinRel .ne (.ofDep a) (.ofDep b)
 
 end Nondep
 

Blase/Blase/MultiWidth/GoodFSM.lean

@@ -734,6 +734,18 @@ def mkTermFSM (wcard tcard bcard pcard : Nat) (t : Nondep.Term) :
             (composeUnaryAux FSM.not aFsm.toFsmZext),
       width := wFsm
     }
+  | .boolUlt w a b =>  
+    let fsmA := mkTermFSM wcard tcard bcard pcard a
+    let fsmB := mkTermFSM wcard tcard bcard pcard b
+    let fsmW := mkWidthFSM wcard tcard bcard pcard w
+    { toFsmZext :=
+      -- upto 'w', don't make a decision, then
+      -- spit out what fsmTermUlt believes.
+      -- TODO: try to replace with a 'latchImmediate',
+      -- since that should be a much more long-term solution.
+      fsmW.toFsm ||| (fsmTermUlt fsmA fsmB),
+      width := fsmW
+    }
   | .boolVar v =>
     -- we cannot make a variable that allows all possible
     -- bitstreams, we should only allow '00000000' or '11111111'.
@@ -1567,6 +1579,10 @@ def mkPredicateFSMAux (wcard tcard bcard pcard : Nat) (p : Nondep.Predicate) :
       -- TODO: rename this Aux' business, it's ugly.
       let fsmEq := composeBinaryAux' FSM.nxor (fsmA.toFsmZext) (fsmB.toFsmZext)
       { toFsm := composeUnaryAux FSM.scanAnd (fsmEq) }
+    | .ne =>
+      -- TODO: rename this Aux' business, it's ugly.
+      let fsmEq := composeBinaryAux' FSM.xor (fsmA.toFsmZext) (fsmB.toFsmZext)
+      { toFsm := composeUnaryAux FSM.scanAnd (fsmEq) }
 
 theorem foo (f g : α → β) (h : f ≠ g) : ∃ x, f x ≠ g x := by
   exact Function.ne_iff.mp h
@@ -2000,23 +2016,24 @@ def isGoodPredicateFSM_mkPredicateFSMAux {wcard tcard bcard pcard : Nat}
         simp at this
         simp [this]
 
-  case boolBinRel wcard' tcard' bcard' tctx' pcard'  k a b =>
+  case boolBinRel wcard' tcard' bcard' tctx' pcard' k a b =>
     constructor
     intros wenv benv tenv penv fsmEnv htenv hpenv
     have ha := IsGoodTermBoolFSM_mkTermFSM wcard' tcard' bcard' pcard' a
     have hb := IsGoodTermBoolFSM_mkTermFSM wcard' tcard' bcard' pcard' b
-    simp [mkPredicateFSMAux, Nondep.Predicate.ofDep]
-    rw [ha.heq (benv := benv) (tenv := tenv) (henv := htenv)]
-    rw [hb.heq (benv := benv) (tenv := tenv) (henv := htenv)]
-    simp [Predicate.toProp]
-    rw [BitStream.ext_iff]
-    simp [BitStream.scanAnd_eq_decide] -- TODO: mark this a simp lemma.
-    constructor
-    · intros hp
-      simp [hp]
-    · intros hp
-      specialize hp 0 0 (by decide)
-      exact hp
+    rcases k <;>
+    · simp [mkPredicateFSMAux, Nondep.Predicate.ofDep]
+      rw [ha.heq (benv := benv) (tenv := tenv) (henv := htenv)]
+      rw [hb.heq (benv := benv) (tenv := tenv) (henv := htenv)]
+      simp [Predicate.toProp]
+      rw [BitStream.ext_iff]
+      simp [BitStream.scanAnd_eq_decide] -- TODO: mark this a simp lemma.
+      constructor
+      · intros hp
+        simp [hp]
+      · intros hp
+        specialize hp 0 0 (by decide)
+        exact hp
 
 /-- Negate the FSM so we can decide if zeroes. -/
 def mkPredicateFSMNondep (wcard tcard bcard pcard : Nat) (p : Nondep.Predicate) :

Blase/Blase/MultiWidth/Tactic.lean

@@ -622,29 +622,6 @@ def collectPredicateAtom (state : CollectState)
   let (pix, pToIx) := state.pToIx.findOrInsertVal e
   return (.var pix, { state with pToIx })
 
-/-
-Certain predicates like `ult, slt` etc return booleans, and are thus
-encoded as `a.slt b = true` instead of a prop level `a.slt b`.
-To fix this, we have a special case in the reflection that looks for this pattern,
-and then reflects it into the appropriate prop.
--/
-def collectBVBooleanEqPredicateAux (state : CollectState) (a b : Expr) :
-  Option (SolverM (MultiWidth.Nondep.Predicate × CollectState)) :=
-  let_expr true := b | none
-  let out? := match_expr a with
-    | BitVec.slt w x y => some (w, MultiWidth.BinaryRelationKind.slt, x, y)
-    | BitVec.sle w x y => some (w, MultiWidth.BinaryRelationKind.sle, x, y)
-    | BitVec.ult w x y => some (w, MultiWidth.BinaryRelationKind.ult, x, y)
-    | BitVec.ule w x y => some (w, MultiWidth.BinaryRelationKind.ule, x, y)
-    | _ => none
-  -- NOTE: Lean bug prevents us from writing this with do-notation,
-  -- so we suffer as haskellers once did.
-  out? >>= fun ((w, kind, x, y)) => some do
-    let (w, state) ← collectWidthAtom state w
-    let (tx, state) ← collectTerm state x
-    let (ty, state) ← collectTerm state y
-    pure (.binRel kind w tx ty, state)
-
 /-- Return a new expression that this is defeq to, along with the expression of the environment that this needs, under which it will be defeq. -/
 partial def collectBVPredicateAux (state : CollectState) (e : Expr) :
     SolverM (MultiWidth.Nondep.Predicate × CollectState) := do
@@ -669,13 +646,9 @@ partial def collectBVPredicateAux (state : CollectState) (e : Expr) :
       let (tb, state) ← collectTerm state b
       return (.binRel .eq w ta tb, state)
     | Bool =>
-      -- | TODO: Refactor to use our spanky new bool sort!
-      if let .some mkBoolPredicate := collectBVBooleanEqPredicateAux state a b then
-        mkBoolPredicate
-      else
-        let (a, state) ← collectBoolTerm state a
-        let (b, state) ← collectBoolTerm state b
-        return (.boolBinRel .eq a b, state)
+      let (a, state) ← collectBoolTerm state a
+      let (b, state) ← collectBoolTerm state b
+      return (.boolBinRel .eq a b, state)
     | _ => mkAtom
   | Ne α a b =>
     match_expr α with
@@ -684,6 +657,10 @@ partial def collectBVPredicateAux (state : CollectState) (e : Expr) :
       let (ta, state) ← collectTerm state a
       let (tb, state) ← collectTerm state b
       return (.binRel .ne w ta tb, state)
+    | Bool =>
+      let (a, state) ← collectBoolTerm state a
+      let (b, state) ← collectBoolTerm state b
+      return (.boolBinRel .ne a b, state)
     | _ => collectPredicateAtom state e
   | Or p q =>
     let (ta, state) ← collectBVPredicateAux state p