use fanin

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

@@ -94,16 +94,16 @@ where
     mkApp3 (mkConst ``BVPred.getLsbD) (toExpr w) (toExpr expr) (toExpr idx)
 
 
-instance [ToExpr α] : ToExpr (BoolExpr α) where
+instance : ToExpr BVLogicalExpr where
   toExpr x := go x
-  toTypeExpr := mkApp (mkConst ``BoolExpr) (toTypeExpr α)
+  toTypeExpr := (mkConst ``BVLogicalExpr)
 where
-  go : (BoolExpr α) → Expr
-  | .literal lit => mkApp2 (mkConst ``BoolExpr.literal) (toTypeExpr α) (toExpr lit)
-  | .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)
+  go : BVLogicalExpr → Expr
+  | .atom a => mkApp (mkConst ``BVLogicalExpr.atom) (toExpr a)
+  | .const b => mkApp (mkConst ``BVLogicalExpr.const) (toExpr b)
+  | .not x => mkApp (mkConst ``BVLogicalExpr.not) (go x)
+  | .gate g x y => mkApp3 (mkConst ``BVLogicalExpr.gate) (toExpr g) (go x) (go y)
+  | .ite d l r => mkApp3 (mkConst ``BVLogicalExpr.ite) (go d) (go l) (go r)
 
 
 open Lean.Meta

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

@@ -31,8 +31,8 @@ def mkEvalExpr (expr : Expr) : M Expr := do
 Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom.
 -/
 def ofPred (bvPred : ReifiedBVPred) : M ReifiedBVLogical := do
-  let boolExpr := .literal bvPred.bvPred
-  let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
+  let boolExpr := .atom bvPred.bvPred
+  let expr := mkApp (mkConst ``BVLogicalExpr.atom) bvPred.expr
   -- important: This must be the same proof as the bvPred one in order for the cache to be correct
   let proof := bvPred.evalsAtAtoms
   return ⟨boolExpr, bvPred.originalExpr, proof, expr⟩
@@ -48,11 +48,11 @@ def boolAtom (t : Expr) : M (Option ReifiedBVLogical) := do
 Build a reified version of the constant `val`.
 -/
 def mkBoolConst (val : Bool) : M ReifiedBVLogical := do
-  let boolExpr := .const val
-  let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr val)
+  let logicalExpr := .const val
+  let expr := mkApp (mkConst ``BVLogicalExpr.const) (toExpr val)
   -- This is safe because this proof always holds definitionally.
   let proof := pure none
-  return ⟨boolExpr, toExpr val, proof, expr⟩
+  return ⟨logicalExpr, toExpr val, proof, expr⟩
 
 /--
 Construct the reified version of applying the gate in `gate` to `lhs` and `rhs`.
@@ -62,11 +62,10 @@ and `rhs`.
 def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) (origExpr : Expr) :
     M ReifiedBVLogical := do
   let congrThm := congrThmOfGate gate
-  let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr
+  let logicalExpr := .gate gate lhs.bvExpr rhs.bvExpr
   let expr :=
-    mkApp4
-      (mkConst ``BoolExpr.gate)
-      (mkConst ``BVPred)
+    mkApp3
+      (mkConst ``BVLogicalExpr.gate)
       (toExpr gate)
       lhs.expr
       rhs.expr
@@ -85,7 +84,7 @@ def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) (
       lhsExpr rhsExpr
       lhsEvalExpr rhsEvalExpr
       lhsProof rhsProof
-  return ⟨boolExpr, origExpr, proof, expr⟩
+  return ⟨logicalExpr, origExpr, proof, expr⟩
 where
   congrThmOfGate (gate : Gate) : Name :=
     match gate with
@@ -99,14 +98,14 @@ Construct the reified version of `Bool.not subExpr`.
 This function assumes that `subExpr` is the expression corresponding to `sub`.
 -/
 def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) (origExpr : Expr) : M ReifiedBVLogical := do
-  let boolExpr := .not sub.bvExpr
-  let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
+  let logicalExpr := .not sub.bvExpr
+  let expr := mkApp (mkConst ``BVLogicalExpr.not) sub.expr
   let proof := do
     -- This is safe as `not_congr` holds definitionally if the arguments are defeq.
     let some subProof ← sub.evalsAtAtoms | return none
     let subEvalExpr ← ReifiedBVLogical.mkEvalExpr sub.expr
     return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
-  return ⟨boolExpr, origExpr, proof, expr⟩
+  return ⟨logicalExpr, origExpr, proof, expr⟩
 
 /--
 Construct the reified version of `if discrExpr then lhsExpr else rhsExpr`.
@@ -115,11 +114,10 @@ This function assumes that `discrExpr`, lhsExpr` and `rhsExpr` are the correspon
 -/
 def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) (origExpr : Expr) :
     M ReifiedBVLogical := do
-  let boolExpr := .ite discr.bvExpr lhs.bvExpr rhs.bvExpr
+  let logicalExpr := .ite discr.bvExpr lhs.bvExpr rhs.bvExpr
   let expr :=
-    mkApp4
-      (mkConst ``BoolExpr.ite)
-      (mkConst ``BVPred)
+    mkApp3
+      (mkConst ``BVLogicalExpr.ite)
       discr.expr
       lhs.expr
       rhs.expr
@@ -141,7 +139,7 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr)
       discrExpr lhsExpr rhsExpr
       discrEvalExpr lhsEvalExpr rhsEvalExpr
       discrProof lhsProof rhsProof
-  return ⟨boolExpr, origExpr, proof, expr⟩
+  return ⟨logicalExpr, origExpr, proof, expr⟩
 
 end ReifiedBVLogical
 

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

@@ -49,7 +49,7 @@ Logical conjunction of two `ReifiedBVLogical`.
 -/
 def and (x y : SatAtBVLogical) : SatAtBVLogical where
   bvExpr := .gate .and x.bvExpr y.bvExpr
-  expr := mkApp4 (mkConst ``BoolExpr.gate) (mkConst ``BVPred) (mkConst ``Gate.and) x.expr y.expr
+  expr := mkApp3 (mkConst ``BVLogicalExpr.gate) (mkConst ``Gate.and) x.expr y.expr
   satAtAtoms :=
     return mkApp5
       (mkConst ``BVLogicalExpr.sat_and)

src/Std/Sat/AIG/Basic.lean

@@ -80,6 +80,17 @@ private theorem invert_eq_testBit (f : Fanin) : f.invert = f.val.testBit 0 := by
 theorem invert_flip (f : Fanin) : (f.flip v).invert = f.invert ^^ v := by
   cases v <;> simp [flip, invert_eq_testBit, -Nat.mod_two_not_eq_one]
 
+theorem eq_iff (f1 f2 : Fanin) : f1 = f2 ↔ (f1.gate = f2.gate ∧ f1.invert = f2.invert) := by
+  rcases f1 with ⟨f1⟩
+  rcases f2 with ⟨f2⟩
+  constructor
+  · simp_all
+  · simp only [gate, invert, Nat.one_and_eq_mod_two, Nat.mod_two_bne_zero, of.injEq, and_imp]
+    intro h1 h2
+    have : f1 % 2 = f2 % 2 := by
+      cases Nat.mod_two_eq_zero_or_one f1 <;> simp_all
+    omega
+
 end Fanin
 
 /--

src/Std/Tactic/BVDecide/Bitblast.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Std.Tactic.BVDecide.Bitblast.BoolExpr
 import Std.Tactic.BVDecide.Bitblast.BVExpr
 
 /-!

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

@@ -7,7 +7,6 @@ prelude
 import Init.Data.Hashable
 import Init.Data.BitVec
 import Init.Data.RArray
-import Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
 
 /-!
 This module contains the definition of the `BitVec` fragment that `bv_decide` internally operates
@@ -357,7 +356,6 @@ def decEq : DecidableEq (BVExpr w) := fun l r =>
         | .const .. | .var .. | .extract .. | .bin .. | .un .. | .append .. | .replicate ..
         | .shiftRight .. | .shiftLeft .. => .isFalse (by simp)
 
-
 instance : DecidableEq (BVExpr w) := decEq
 
 def toString : BVExpr w → String
@@ -476,6 +474,7 @@ inductive BVBinPred where
   Unsigned Less Than
   -/
   | ult
+deriving DecidableEq, Hashable
 
 namespace BVBinPred
 
@@ -509,6 +508,7 @@ inductive BVPred where
   Getting a constant LSB from a `BitVec`.
   -/
   | getLsbD (expr : BVExpr w) (idx : Nat)
+deriving DecidableEq, Hashable
 
 namespace BVPred
 
@@ -543,20 +543,120 @@ theorem eval_getLsbD : eval assign (.getLsbD expr idx) = (expr.eval assign).getL
 
 end BVPred
 
+inductive Gate
+  | and
+  | xor
+  | beq
+  | or
+deriving DecidableEq, Hashable
+
+namespace Gate
+
+def toString : Gate → String
+  | and => "&&"
+  | xor => "^^"
+  | beq => "=="
+  | or => "||"
+
+def eval : Gate → Bool → Bool → Bool
+  | and => (· && ·)
+  | xor => (· ^^ ·)
+  | beq => (· == ·)
+  | or => (· || ·)
+
+end Gate
+
 /--
 Boolean substructure of problems involving predicates on BitVec as atoms.
 -/
-abbrev BVLogicalExpr := BoolExpr BVPred
+inductive BVLogicalExpr
+  | atom (pred : BVPred)
+  | const (val : Bool)
+  | not (expr : BVLogicalExpr)
+  | gate (g : Gate) (lhs rhs : BVLogicalExpr)
+  | ite (discr lhs rhs : BVLogicalExpr)
+with
+  @[computed_field]
+  hashCode : BVLogicalExpr → UInt64
+   | .atom pred => mixHash 5 <| hash pred
+   | .const val => mixHash 7 <| hash val
+   | .not expr => mixHash 11 <| hashCode expr
+   | .gate g lhs rhs => mixHash 13 <| mixHash (hash g) <| mixHash (hashCode lhs) (hashCode rhs)
+   | .ite discr lhs rhs =>
+     mixHash 17 <| mixHash (hashCode discr) <| mixHash (hashCode lhs) (hashCode rhs)
 
 namespace BVLogicalExpr
 
+def toString : BVLogicalExpr → String
+  | atom a => ToString.toString a
+  | const b => ToString.toString b
+  | not x => "!" ++ toString x
+  | gate g x y => "(" ++ toString x ++ " " ++ g.toString ++ " " ++ toString y ++ ")"
+  | ite d l r => "(if " ++ toString d ++ " " ++ toString l ++ " " ++ toString r ++ ")"
+
+instance : ToString BVLogicalExpr := ⟨toString⟩
+
+instance : Hashable BVLogicalExpr where
+  hash := BVLogicalExpr.hashCode
+
+def decEq : DecidableEq BVLogicalExpr := fun l r =>
+  withPtrEqDecEq l r fun _ =>
+    if h : hash l ≠ hash r then
+      .isFalse (ne_of_apply_ne hash h)
+    else
+      match l with
+      | .atom la =>
+        match r with
+        | .atom ra =>
+          if h : la = ra then .isTrue (by simp[h]) else .isFalse (by simp [h])
+        | .const .. | .not .. | .gate .. | .ite .. => .isFalse (by simp)
+      | .const lb =>
+        match r with
+        | .const rb =>
+          if h : lb = rb then .isTrue (by simp[h]) else .isFalse (by simp [h])
+        | .atom .. | .not .. | .gate .. | .ite .. => .isFalse (by simp)
+      | .not lexp =>
+        match r with
+        | .not rexp =>
+          match decEq lexp rexp with
+          | .isTrue h => .isTrue (by simp [h])
+          | .isFalse h => .isFalse (by simp [h])
+        | .const .. | .atom .. | .gate .. | .ite .. => .isFalse (by simp)
+      | .gate lg llhs lrhs =>
+        match r with
+        | .gate rg rlhs rrhs =>
+          if h1 : lg = rg then
+            match decEq llhs rlhs, decEq lrhs rrhs with
+            | .isTrue h2, .isTrue h3 => .isTrue (by simp [h1, h2, h3])
+            | .isFalse h2, _ => .isFalse (by simp [h2])
+            | _, .isFalse h2 => .isFalse (by simp [h2])
+          else
+            .isFalse (by simp [h1])
+        | .const .. | .atom .. | .not .. | .ite .. => .isFalse (by simp)
+      | .ite ldiscr llhs lrhs =>
+        match r with
+        | .ite rdiscr rlhs rrhs =>
+          match decEq ldiscr rdiscr, decEq llhs rlhs, decEq lrhs rrhs with
+          | .isTrue h1, .isTrue h2, .isTrue h3 => .isTrue (by simp [h1, h2, h3])
+          | .isFalse h1, _, _ => .isFalse (by simp [h1])
+          | _, .isFalse h1, _ => .isFalse (by simp [h1])
+          | _, _, .isFalse h1 => .isFalse (by simp [h1])
+        | .const .. | .atom .. | .not .. | .gate .. => .isFalse (by simp)
+
+instance : DecidableEq BVLogicalExpr := decEq
+
 /--
 The semantics of boolean problems involving BitVec predicates as atoms.
 -/
 def eval (assign : BVExpr.Assignment) (expr : BVLogicalExpr) : Bool :=
-  BoolExpr.eval (·.eval assign) expr
+  match expr with
+  | .atom a => a.eval assign
+  | .const b => b
+  | .not x => !eval assign x
+  | .gate g x y => g.eval (eval assign x) (eval assign y)
+  | .ite d l r => bif d.eval assign then l.eval assign else r.eval assign
 
-@[simp] theorem eval_literal : eval assign (.literal pred) = pred.eval assign := rfl
+@[simp] theorem eval_atom : eval assign (.atom pred) = pred.eval assign := rfl
 @[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

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

@@ -310,10 +310,10 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
   · rw [AIG.LawfulVecOperator.decl_eq (f := blastVar)]
   · rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
   · next op lhsExpr rhsExpr =>
+    have hl := (goCache aig lhsExpr cache).result.property
+    have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
     match op with
     | .and | .or | .xor | .add | .mul | .udiv | .umod =>
-      have hl := (goCache aig lhsExpr cache).result.property
-      have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [goCache_decl_eq, goCache_decl_eq]
       · omega
@@ -321,11 +321,11 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
         · exact h1
         · apply Nat.le_trans <;> assumption
   · next op expr =>
+    have := (goCache aig expr cache).result.property
     match op with
     | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. =>
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [goCache_decl_eq]
-      have := (goCache aig expr cache).result.property
       omega
   · next lhsExpr rhsExpr h =>
     have hl := (goCache aig lhsExpr cache).result.property

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

@@ -18,12 +18,12 @@ namespace Std.Tactic.BVDecide
 
 open Std.Sat
 
+namespace BVPred
+
 structure Return (aig : AIG BVBit) where
   result : AIG.ExtendingEntrypoint aig
   cache : BVExpr.Cache result.val.aig
 
-namespace BVPred
-
 def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return aig :=
   let ⟨pred, cache⟩ := input
   match pred with

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

@@ -18,31 +18,97 @@ open Std.Sat Std.Sat.AIG
 
 namespace BVLogicalExpr
 
+structure Cache (aig : AIG BVBit) where
+  map : Std.HashMap BVLogicalExpr Fanin
+  hbound : ∀ k (h : k ∈ map), (map[k]'h).gate < aig.decls.size
+
+@[inline]
+def Cache.empty : Cache aig :=
+  ⟨{}, by simp⟩
+
+@[inline]
+def Cache.insert (cache : Cache aig) (expr : BVLogicalExpr) (ref : AIG.Ref aig) :
+    Cache aig :=
+  let ⟨map, hbound⟩ := cache
+  have := by
+    intro k hk
+    rw [Std.HashMap.getElem_insert]
+    split
+    · simp [ref.hgate]
+    · apply hbound
+  ⟨map.insert expr (Fanin.mk ref.gate ref.invert), this⟩
+
+@[inline]
+def Cache.get? (cache : Cache aig) (expr : BVLogicalExpr) : Option (AIG.Ref aig) :=
+  match h : cache.map[expr]? with
+  | some ref =>
+    have : expr ∈ cache.map := by
+      rw [Std.HashMap.mem_iff_contains, Std.HashMap.contains_eq_isSome_getElem?]
+      simp [h]
+    have : cache.map[expr]'this = ref := by
+      rw [Std.HashMap.getElem?_eq_some_getElem (h' := this)] at h
+      simpa using h
+    have := by
+      rw [← this]
+      apply cache.hbound
+    some ⟨ref.gate, ref.invert, this⟩
+  | none =>
+    none
+
+@[inline]
+def Cache.cast (cache : Cache aig1) (h : aig1.decls.size ≤ aig2.decls.size) :
+    Cache aig2 :=
+  let ⟨map, hbound⟩ := cache
+  have := by
+    intro k hk
+    apply Nat.lt_of_lt_of_le
+    · apply hbound
+    · exact h
+  ⟨map, this⟩
+
+structure Return (aig : AIG BVBit) where
+  result : AIG.ExtendingEntrypoint aig
+  bvCache : BVExpr.Cache result.val.aig
+  logCache : Cache result.val.aig
+
 /--
-Turn a `BoolExpr` into an `Entrypoint`.
+Turn a `BVLogicalExpr` into an `Entrypoint`.
 -/
 def bitblast (expr : BVLogicalExpr) : Entrypoint BVBit :=
-  go AIG.empty expr .empty |>.result.val
+  goCache AIG.empty expr .empty .empty |>.result.val
 where
-  go (aig : AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) : Return aig :=
+  goCache (aig : AIG BVBit) (expr : BVLogicalExpr) (bvCache : BVExpr.Cache aig)
+      (logCache : Cache aig) : Return aig :=
+    match logCache.get? expr with
+    | some ref => ⟨⟨⟨aig, ref⟩, Nat.le_refl ..⟩, bvCache, logCache⟩
+    | none =>
+      let ⟨result, bvCache, logCache⟩ := go aig expr bvCache logCache
+      ⟨result, bvCache, logCache.insert expr result.val.ref⟩
+  termination_by (sizeOf expr, 1)
+
+  go (aig : AIG BVBit) (expr : BVLogicalExpr) (bvCache : BVExpr.Cache aig) (logCache : Cache aig) :
+      Return aig :=
     match expr with
-    | .literal var => BVPred.bitblast aig ⟨var, cache⟩
+    | .atom pred =>
+      let ⟨result, bvCache⟩ := BVPred.bitblast aig ⟨pred, bvCache⟩
+      ⟨result, bvCache, logCache.cast result.property⟩
     | .const val =>
       have := LawfulOperator.le_size (f := mkConstCached) ..
-      ⟨⟨aig.mkConstCached val, this⟩, cache.cast this⟩
+      ⟨⟨aig.mkConstCached val, this⟩, bvCache.cast this, logCache.cast this⟩
     | .not expr =>
-      let ⟨⟨⟨aig, exprRef⟩, hexpr⟩, cache⟩ := go aig expr cache
+      let ⟨⟨⟨aig, exprRef⟩, hexpr⟩, bvCache, logCache⟩ := goCache aig expr bvCache logCache
       let ret := aig.mkNotCached exprRef
       have := LawfulOperator.le_size (f := mkNotCached) ..
-      let cache := cache.cast this
+      let bvCache := bvCache.cast this
+      let logCache := logCache.cast this
       have := by
         apply LawfulOperator.le_size_of_le_aig_size (f := mkNotCached)
         exact hexpr
-      ⟨⟨ret, this⟩, cache⟩
+      ⟨⟨ret, this⟩, bvCache, logCache⟩
     | .ite discr lhs rhs =>
-      let ⟨⟨⟨aig, discrRef⟩, dextend⟩, cache⟩ := go aig discr cache
-      let ⟨⟨⟨aig, lhsRef⟩, lextend⟩, cache⟩ := go aig lhs cache
-      let ⟨⟨⟨aig, rhsRef⟩, rextend⟩, cache⟩ := go aig rhs cache
+      let ⟨⟨⟨aig, discrRef⟩, dextend⟩, bvCache, logCache⟩ := goCache aig discr bvCache logCache
+      let ⟨⟨⟨aig, lhsRef⟩, lextend⟩, bvCache, logCache⟩ := goCache aig lhs bvCache logCache
+      let ⟨⟨⟨aig, rhsRef⟩, rextend⟩, bvCache, logCache⟩ := goCache aig rhs bvCache logCache
       let discrRef := discrRef.cast <| by
         dsimp only at lextend rextend ⊢
         omega
@@ -53,15 +119,16 @@ where
       let input := ⟨discrRef, lhsRef, rhsRef⟩
       let ret := aig.mkIfCached input
       have := LawfulOperator.le_size (f := mkIfCached) ..
-      let cache := cache.cast this
+      let bvCache := bvCache.cast this
+      let logCache := logCache.cast this
       have := by
         apply LawfulOperator.le_size_of_le_aig_size (f := mkIfCached)
         dsimp only at dextend lextend rextend
         omega
-      ⟨⟨ret, this⟩, cache⟩
+      ⟨⟨ret, this⟩, bvCache, logCache⟩
     | .gate g lhs rhs =>
-      let ⟨⟨⟨aig, lhsRef⟩, lextend⟩, cache⟩ := go aig lhs cache
-      let ⟨⟨⟨aig, rhsRef⟩, rextend⟩, cache⟩ := go aig rhs cache
+      let ⟨⟨⟨aig, lhsRef⟩, lextend⟩, bvCache, logCache⟩ := goCache aig lhs bvCache logCache
+      let ⟨⟨⟨aig, rhsRef⟩, rextend⟩, bvCache, logCache⟩ := goCache aig rhs bvCache logCache
       let lhsRef := lhsRef.cast <| by
         dsimp only at rextend ⊢
         omega
@@ -70,125 +137,154 @@ where
       | .and =>
         let ret := aig.mkAndCached input
         have := LawfulOperator.le_size (f := mkAndCached) ..
-        let cache := cache.cast this
+        let bvCache := bvCache.cast this
+        let logCache := logCache.cast this
         have := by
           apply LawfulOperator.le_size_of_le_aig_size (f := mkAndCached)
           dsimp only at lextend rextend
           omega
-        ⟨⟨ret, this⟩, cache⟩
+        ⟨⟨ret, this⟩, bvCache, logCache⟩
       | .xor =>
         let ret := aig.mkXorCached input
         have := LawfulOperator.le_size (f := mkXorCached) ..
-        let cache := cache.cast this
+        let bvCache := bvCache.cast this
+        let logCache := logCache.cast this
         have := by
           apply LawfulOperator.le_size_of_le_aig_size (f := mkXorCached)
           dsimp only at lextend rextend
           omega
-        ⟨⟨ret, this⟩, cache⟩
+        ⟨⟨ret, this⟩, bvCache, logCache⟩
       | .beq =>
         let ret := aig.mkBEqCached input
         have := LawfulOperator.le_size (f := mkBEqCached) ..
-        let cache := cache.cast this
+        let bvCache := bvCache.cast this
+        let logCache := logCache.cast this
         have := by
           apply LawfulOperator.le_size_of_le_aig_size (f := mkBEqCached)
           dsimp only at lextend rextend
           omega
-        ⟨⟨ret, this⟩, cache⟩
+        ⟨⟨ret, this⟩, bvCache, logCache⟩
       | .or =>
         let ret := aig.mkOrCached input
         have := LawfulOperator.le_size (f := mkOrCached) ..
-        let cache := cache.cast this
+        let bvCache := bvCache.cast this
+        let logCache := logCache.cast this
         have := by
           apply LawfulOperator.le_size_of_le_aig_size (f := mkOrCached)
           dsimp only at lextend rextend
           omega
-        ⟨⟨ret, this⟩, cache⟩
+        ⟨⟨ret, this⟩, bvCache, logCache⟩
+  termination_by (sizeOf expr, 0)
 
 namespace bitblast
 
-theorem go_le_size (aig : AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) :
-    aig.decls.size ≤ (go aig expr cache).result.val.aig.decls.size :=
-  (go aig expr cache).result.property
+theorem goCache_le_size (aig : AIG BVBit) (expr : BVLogicalExpr) (bvCache : BVExpr.Cache aig)
+    (logCache : Cache aig) :
+    aig.decls.size ≤ (goCache aig expr bvCache logCache).result.val.aig.decls.size :=
+  (goCache aig expr bvCache logCache).result.property
+
+theorem go_le_size (aig : AIG BVBit) (expr : BVLogicalExpr) (bvCache : BVExpr.Cache aig)
+    (logCache : Cache aig) :
+    aig.decls.size ≤ (go aig expr bvCache logCache).result.val.aig.decls.size :=
+  (go aig expr bvCache logCache).result.property
+
+theorem goCache_lt_size_of_lt_aig_size (aig : AIG BVBit) (expr : BVLogicalExpr)
+    (bvCache : BVExpr.Cache aig) (logCache : Cache aig) (h : x < aig.decls.size) :
+    x < (goCache aig expr bvCache logCache).result.val.aig.decls.size := by
+  apply Nat.lt_of_lt_of_le
+  · exact h
+  · apply goCache_le_size
 
 theorem go_lt_size_of_lt_aig_size (aig : AIG BVBit) (expr : BVLogicalExpr)
-    (cache : BVExpr.Cache aig) (h : x < aig.decls.size) :
-    x < (go aig expr cache).result.val.aig.decls.size := by
+    (bvCache : BVExpr.Cache aig) (logCache : Cache aig) (h : x < aig.decls.size) :
+    x < (go aig expr bvCache logCache).result.val.aig.decls.size := by
   apply Nat.lt_of_lt_of_le
   · exact h
   · apply go_le_size
 
-theorem go_decl_eq (idx) (aig : AIG BVBit) (cache : BVExpr.Cache aig) (h : idx < aig.decls.size) (hbounds) :
-    (go aig expr cache).result.val.aig.decls[idx]'hbounds = aig.decls[idx] := by
-  induction expr generalizing aig with
-  | const =>
-    simp only [go]
-    rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
-  | literal =>
-    simp only [go]
-    rw [BVPred.bitblast_decl_eq]
-  | not expr ih =>
-    simp only [go]
-    have := go_le_size aig expr cache
-    specialize ih aig cache (by omega) (by omega)
-    rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
-    assumption
-  | ite discr lhs rhs dih lih rih =>
-    simp only [go]
-    rw [AIG.LawfulOperator.decl_eq (f := mkIfCached), rih, lih, dih]
-    · apply go_lt_size_of_lt_aig_size
-      assumption
-    · apply go_lt_size_of_lt_aig_size
-      apply go_lt_size_of_lt_aig_size
-      assumption
-    · apply go_lt_size_of_lt_aig_size
-      apply go_lt_size_of_lt_aig_size
-      apply go_lt_size_of_lt_aig_size
-      assumption
-  | gate g lhs rhs lih rih =>
-    cases g with
-    | and =>
-      simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih]
-      · apply go_lt_size_of_lt_aig_size
-        assumption
-      · apply go_lt_size_of_lt_aig_size
-        apply go_lt_size_of_lt_aig_size
-        assumption
-    | xor =>
-      simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih]
-      · apply go_lt_size_of_lt_aig_size
-        assumption
-      · apply go_lt_size_of_lt_aig_size
-        apply go_lt_size_of_lt_aig_size
-        assumption
-    | beq =>
-      simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
-      · apply go_lt_size_of_lt_aig_size
-        assumption
-      · apply go_lt_size_of_lt_aig_size
-        apply go_lt_size_of_lt_aig_size
-        assumption
-    | or =>
-      simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
-      · apply go_lt_size_of_lt_aig_size
-        assumption
-      · apply go_lt_size_of_lt_aig_size
-        apply go_lt_size_of_lt_aig_size
-        assumption
+mutual
 
-theorem go_isPrefix_aig {aig : AIG BVBit} (cache : BVExpr.Cache aig) :
-    IsPrefix aig.decls (go aig expr cache).result.val.aig.decls := by
+theorem goCache_decl_eq (aig : AIG BVBit) (bvCache : BVExpr.Cache aig) (logCache : Cache aig) :
+    ∀ (idx : Nat) (h1) (h2),
+        (goCache aig expr bvCache logCache).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  generalize hres : goCache aig expr bvCache logCache = res
+  intro idx h1 h2
+  unfold goCache at hres
+  split at hres
+  · rw [getElem_congr_coll]
+    rw [← hres]
+  · symm at hres
+    subst hres
+    apply go_decl_eq
+termination_by (sizeOf expr, 1)
+
+theorem go_decl_eq (aig : AIG BVBit) (bvCache : BVExpr.Cache aig) (logCache : Cache aig) :
+    ∀ (idx : Nat) (h1) (h2), (go aig expr bvCache logCache).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  intro idx h1 h2
+  unfold go
+  split
+  · rw [BVPred.bitblast_decl_eq]
+  · rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
+  · next expr =>
+    rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
+    rw [goCache_decl_eq]
+    have := (goCache aig expr bvCache logCache).result.property
+    omega
+  · next discr lhs rhs =>
+    let discrResult := (goCache aig discr bvCache logCache)
+    let lhsResult := (goCache discrResult.1.1.aig lhs discrResult.bvCache discrResult.logCache)
+    have hd := discrResult.result.property
+    have hl := lhsResult.result.property
+    have hr := (goCache lhsResult.1.1.aig rhs lhsResult.bvCache lhsResult.logCache).result.property
+    rw [AIG.LawfulOperator.decl_eq]
+    rw [goCache_decl_eq, goCache_decl_eq, goCache_decl_eq]
+    · simp only [discrResult] at hd
+      omega
+    · apply Nat.lt_of_lt_of_le
+      · exact h1
+      · apply Nat.le_trans <;> assumption
+    · apply Nat.lt_of_lt_of_le
+      · exact h1
+      · apply Nat.le_trans
+        · assumption
+        · apply Nat.le_trans <;> assumption
+  · next g lhs rhs =>
+    let lhsResult := (goCache aig lhs bvCache logCache)
+    have hl := lhsResult.result.property
+    have hr := (goCache lhsResult.1.1.aig rhs lhsResult.bvCache lhsResult.logCache).result.property
+    match g with
+    | .and | .xor | .beq | .or =>
+      rw [AIG.LawfulOperator.decl_eq]
+      rw [goCache_decl_eq, goCache_decl_eq]
+      · simp only [lhsResult] at hl hr
+        omega
+      · apply Nat.lt_of_lt_of_le
+        · exact h1
+        · apply Nat.le_trans <;> assumption
+termination_by (sizeOf expr, 0)
+
+end
+
+theorem goCache_isPrefix_aig {aig : AIG BVBit} (bvCache : BVExpr.Cache aig)
+    (logCache : Cache aig) :
+    IsPrefix aig.decls (goCache aig expr bvCache logCache).result.val.aig.decls := by
+  apply IsPrefix.of
+  · intro idx h
+    apply goCache_decl_eq
+  · apply goCache_le_size
+
+theorem go_isPrefix_aig {aig : AIG BVBit} (bvCache : BVExpr.Cache aig)
+    (logCache : Cache aig) :
+    IsPrefix aig.decls (go aig expr bvCache logCache).result.val.aig.decls := by
   apply IsPrefix.of
   · intro idx h
     apply go_decl_eq
   · apply go_le_size
 
-theorem go_denote_mem_prefix (aig : AIG BVBit) (cache : BVExpr.Cache aig) (hstart) :
+theorem go_denote_mem_prefix (aig : AIG BVBit) (bvCache : BVExpr.Cache aig)
+    (logCache : Cache aig) (hstart) :
     ⟦
-      (go aig expr cache).result.val.aig,
+      (go aig expr bvCache logCache).result.val.aig,
       ⟨start, inv, go_lt_size_of_lt_aig_size (h := hstart) ..⟩,
       assign
     ⟧
@@ -197,6 +293,18 @@ theorem go_denote_mem_prefix (aig : AIG BVBit) (cache : BVExpr.Cache aig) (hstar
   apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply go_isPrefix_aig
 
+theorem goCache_denote_mem_prefix (aig : AIG BVBit) (bvCache : BVExpr.Cache aig)
+    (logCache : Cache aig) (hstart) :
+    ⟦
+      (goCache aig expr bvCache logCache).result.val.aig,
+      ⟨start, inv, goCache_lt_size_of_lt_aig_size (h := hstart) ..⟩,
+      assign
+    ⟧
+      =
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
+  apply goCache_isPrefix_aig
+
 end bitblast
 end BVLogicalExpr
 

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

@@ -20,89 +20,291 @@ open Std.Sat.AIG
 
 namespace BVLogicalExpr
 
+namespace Cache
+
+abbrev Inv (assign : BVExpr.Assignment) (aig : AIG BVBit) (cache : Cache aig) : Prop :=
+  ∀ expr (h : expr ∈ cache.map),
+    ⟦aig, ⟨(cache.map[expr]'h).gate, (cache.map[expr]'h).invert, cache.hbound ..⟩, assign.toAIGAssignment⟧
+      =
+    expr.eval assign
+
+theorem Inv_empty (aig : AIG BVBit) : Inv assign aig Cache.empty := by
+  intro k hk
+  simp [Cache.empty] at hk
+
+theorem Inv_cast (cache : Cache aig1) (hpref : IsPrefix aig1.decls aig2.decls)
+    (hinv : Inv assign aig1 cache):
+    Inv assign aig2 (cache.cast hpref.size_le) := by
+  unfold Cache.cast
+  intro expr hexpr
+  specialize hinv expr hexpr
+  rw [← hinv]
+  apply denote.eq_of_isPrefix (entry := ⟨aig1, _, _, _⟩)
+  exact hpref
+
+theorem Inv_insert (cache : Cache aig) (expr : BVLogicalExpr) (ref : AIG.Ref aig)
+    (hinv : Inv assign aig cache)
+    (href : ⟦aig, ref, assign.toAIGAssignment⟧ = expr.eval assign) :
+    Inv assign aig (cache.insert expr ref) := by
+  intro k hk
+  by_cases heq : expr = k
+  · subst heq
+    have : ((cache.insert expr ref).map[expr]'hk) = Fanin.mk ref.gate ref.invert := by
+      unfold Cache.insert
+      apply Std.HashMap.getElem_insert_self
+    rw [← href]
+    congr 3
+    all_goals
+      simp [this]
+  · have hmem : k ∈ cache.map := by
+      unfold Cache.insert at hk
+      apply Std.HashMap.mem_of_mem_insert
+      · exact hk
+      · simp [heq]
+    have : ((cache.insert expr ref).map[k]'hk) = cache.map[k]'hmem := by
+      unfold Cache.insert
+      rw [Std.HashMap.getElem_insert]
+      simp [heq]
+    rw [← hinv]
+    congr 3
+    all_goals
+      rw [this]
+
+theorem get?_eq_some_iff (cache : Cache aig) (expr : BVLogicalExpr) :
+    cache.get? expr = some ref ↔ cache.map[expr]? = some (Fanin.mk ref.gate ref.invert) := by
+  cases ref
+  unfold Cache.get?
+  split
+  · next ref heq =>
+    simp [heq, Fanin.eq_iff ref (.mk _ _)]
+  · next heq => simp [heq]
+
+theorem denote_eq_eval_of_get?_eq_some_of_Inv (cache : Cache aig)
+    (expr : BVLogicalExpr) (ref : AIG.Ref aig) (hsome : cache.get? expr = some ref)
+    (hinv : Inv assign aig cache) :
+    ⟦aig,  ref, assign.toAIGAssignment⟧ = expr.eval assign := by
+  rw [get?_eq_some_iff] at hsome
+  have hmem : expr ∈ cache.map := by
+    rw [Std.HashMap.mem_iff_contains, Std.HashMap.contains_eq_isSome_getElem?]
+    simp [hsome]
+  have href : cache.map[expr]'hmem = Fanin.mk ref.gate ref.invert := by
+    rw [Std.HashMap.getElem?_eq_some_getElem (h' := hmem)] at hsome
+    simp only [Option.some.injEq] at hsome
+    rw [hsome]
+  specialize hinv expr hmem
+  rw [← hinv]
+  cases ref
+  congr 3
+  all_goals
+    simp [href]
+
+end Cache
+
 namespace bitblast
 
 mutual
 
-theorem go_Inv_of_Inv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
-    (cache : BVExpr.Cache aig) (hinv : BVExpr.Cache.Inv assign aig cache) :
-    BVExpr.Cache.Inv assign (go aig expr cache).result.val.aig (go aig expr cache).cache := by
-  induction expr generalizing aig with
-  | const =>
-    simp only [go]
+theorem goCache_BvInv_of_BvInv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
+    (bvCache : BVExpr.Cache aig) (logCache : Cache aig)
+    (hinv : BVExpr.Cache.Inv assign aig bvCache) :
+    BVExpr.Cache.Inv assign (goCache aig expr bvCache logCache).result.val.aig (goCache aig expr bvCache logCache).bvCache := by
+  generalize hres : goCache aig expr bvCache logCache = res
+  unfold goCache at hres
+  split at hres
+  · rw [← hres]
+    exact hinv
+  · rw [← hres]
+    apply go_BvInv_of_BvInv
+    exact hinv
+termination_by (sizeOf expr, 1)
+
+theorem go_BvInv_of_BvInv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
+    (bvCache : BVExpr.Cache aig) (logCache : Cache aig)
+    (hinv : BVExpr.Cache.Inv assign aig bvCache) :
+    BVExpr.Cache.Inv assign (go aig expr bvCache logCache).result.val.aig (go aig expr bvCache logCache).bvCache := by
+  generalize hres : go aig expr bvCache logCache = res
+  unfold go at hres
+  split at hres
+  · rw [← hres]
+    apply BVPred.bitblast_Inv_of_Inv
+    exact hinv
+  · rw [← hres]
     apply BVExpr.Cache.Inv_cast
     apply LawfulOperator.isPrefix_aig (f := mkConstCached)
     exact hinv
-  | literal =>
-    simp only [go]
-    apply BVPred.bitblast_Inv_of_Inv
-    exact hinv
-  | not expr ih =>
-    simp only [go]
+  · next expr =>
+    rw [← hres]
     apply BVExpr.Cache.Inv_cast
     · apply LawfulOperator.isPrefix_aig (f := mkNotCached)
-    · apply ih
+    · apply goCache_BvInv_of_BvInv
       exact hinv
-  | gate g lhs rhs lih rih =>
-    cases g
-    all_goals
-      simp [go, Gate.eval]
+  · next discr lhs rhs =>
+    rw [← hres]
+    apply BVExpr.Cache.Inv_cast
+    · apply LawfulOperator.isPrefix_aig
+    · apply goCache_BvInv_of_BvInv
+      apply goCache_BvInv_of_BvInv
+      apply goCache_BvInv_of_BvInv
+      exact hinv
+  · next g lhs rhs =>
+    match g with
+    | .and | .xor | .beq | .or =>
+      rw [← hres]
       apply BVExpr.Cache.Inv_cast
       · apply LawfulOperator.isPrefix_aig
-      · apply rih
-        apply lih
+      · apply goCache_BvInv_of_BvInv
+        apply goCache_BvInv_of_BvInv
         exact hinv
-  | ite discr lhs rhs dih lih rih =>
-    simp only [go]
-    apply BVExpr.Cache.Inv_cast
-    · apply LawfulOperator.isPrefix_aig (f := mkIfCached)
-    · apply rih
-      apply lih
-      apply dih
-      exact hinv
+termination_by (sizeOf expr, 0)
 
-theorem go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
-    (cache : BVExpr.Cache aig) (hinv : BVExpr.Cache.Inv assign aig cache) :
-    ⟦(go aig expr cache).result, assign.toAIGAssignment⟧ = expr.eval assign := by
-  induction expr generalizing aig with
-  | const => simp [go]
-  | literal =>
-    simp only [go, eval_literal]
-    rw [BVPred.denote_bitblast]
-    exact hinv
-  | not expr ih =>
-    specialize ih _ _ hinv
-    simp [go, ih]
-  | gate g lhs rhs lih rih =>
-    cases g
-    all_goals
-      simp [go, Gate.eval]
-      congr 1
-      · rw [go_denote_mem_prefix]
-        apply lih
-        exact hinv
-      · apply rih
-        apply go_Inv_of_Inv
-        exact hinv
-  | ite discr lhs rhs dih lih rih =>
-    simp only [go, Ref.cast_eq, denote_mkIfCached, denote_projected_entry,
-      eval_ite, Bool.ite_eq_cond_iff]
+end
+
+mutual
+
+theorem goCache_Inv_of_Inv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
+    (bvCache : BVExpr.Cache aig) (logCache : Cache aig)
+    (hinv1 : BVExpr.Cache.Inv assign aig bvCache) (hinv2 : Cache.Inv assign aig logCache) :
+    Cache.Inv assign (goCache aig expr bvCache logCache).result.val.aig (goCache aig expr bvCache logCache).logCache := by
+  generalize hres : goCache aig expr bvCache logCache = res
+  unfold goCache at hres
+  split at hres
+  · rw [← hres]
+    exact hinv2
+  · rw [← hres]
+    apply Cache.Inv_insert
+    · apply go_Inv_of_Inv
+      · exact hinv1
+      · exact hinv2
+    · rw [go_denote_eq]
+      · exact hinv1
+      · exact hinv2
+termination_by (sizeOf expr, 1, 0)
+
+theorem go_Inv_of_Inv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
+    (bvCache : BVExpr.Cache aig) (logCache : Cache aig)
+    (hinv1 : BVExpr.Cache.Inv assign aig bvCache) (hinv2 : Cache.Inv assign aig logCache) :
+    Cache.Inv assign (go aig expr bvCache logCache).result.val.aig (go aig expr bvCache logCache).logCache := by
+  generalize hres : go aig expr bvCache logCache = res
+  unfold go at hres
+  split at hres
+  · rw [← hres]
+    apply Cache.Inv_cast
+    · dsimp only
+      apply BVPred.bitblast_aig_IsPrefix
+    · exact hinv2
+  · rw [← hres]
+    apply Cache.Inv_cast
+    apply LawfulOperator.isPrefix_aig (f := mkConstCached)
+    exact hinv2
+  · next expr =>
+    rw [← hres]
+    apply Cache.Inv_cast
+    · apply LawfulOperator.isPrefix_aig (f := mkNotCached)
+    · apply goCache_Inv_of_Inv
+      · exact hinv1
+      · exact hinv2
+  · next discr lhs rhs =>
+    rw [← hres]
+    apply Cache.Inv_cast
+    · apply LawfulOperator.isPrefix_aig
+    · apply goCache_Inv_of_Inv
+      · apply goCache_BvInv_of_BvInv
+        apply goCache_BvInv_of_BvInv
+        exact hinv1
+      · apply goCache_Inv_of_Inv
+        · apply goCache_BvInv_of_BvInv
+          exact hinv1
+        · apply goCache_Inv_of_Inv
+          · exact hinv1
+          · exact hinv2
+  · next g lhs rhs =>
+    match g with
+    | .and | .xor | .beq | .or =>
+      rw [← hres]
+      apply Cache.Inv_cast
+      · apply LawfulOperator.isPrefix_aig
+      · apply goCache_Inv_of_Inv
+        · apply goCache_BvInv_of_BvInv
+          exact hinv1
+        · apply goCache_Inv_of_Inv
+          · exact hinv1
+          · exact hinv2
+termination_by (sizeOf expr, 0, 0)
+
+theorem goCache_denote_eq (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
+    (bvCache : BVExpr.Cache aig) (logCache : Cache aig)
+    (hinv1 : BVExpr.Cache.Inv assign aig bvCache) (hinv2 : Cache.Inv assign aig logCache) :
+    ⟦(goCache aig expr bvCache logCache).result, assign.toAIGAssignment⟧ = expr.eval assign := by
+  unfold goCache
+  split
+  · next heq =>
+    apply Cache.denote_eq_eval_of_get?_eq_some_of_Inv
+    · exact heq
+    · exact hinv2
+  · rw [go_denote_eq]
+    · exact hinv1
+    · exact hinv2
+termination_by (sizeOf expr, 0, 1)
+
+theorem go_denote_eq (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment)
+    (bvCache : BVExpr.Cache aig) (logCache : Cache aig)
+    (hinv1 : BVExpr.Cache.Inv assign aig bvCache) (hinv2 : Cache.Inv assign aig logCache) :
+    ⟦(go aig expr bvCache logCache).result, assign.toAIGAssignment⟧ = expr.eval assign := by
+  unfold go
+  split
+  · rw [BVPred.denote_bitblast]
+    · simp
+    · exact hinv1
+  · simp
+  · simp only [denote_mkNotCached, denote_projected_entry, eval_not, Bool.not_eq_eq_eq_not,
+      Bool.not_not]
+    rw [goCache_denote_eq]
+    · exact hinv1
+    · exact hinv2
+  · next discr lhs rhs =>
+    simp only [Ref.cast_eq, denote_mkIfCached, denote_projected_entry, eval_ite,
+      Bool.ite_eq_cond_iff]
     apply ite_congr
-    · rw [go_denote_mem_prefix]
-      rw [go_denote_mem_prefix]
-      · specialize dih _ _ hinv
-        simp [dih]
-      · simp [Ref.hgate]
+    · rw [goCache_denote_mem_prefix]
+      rw [goCache_denote_mem_prefix]
+      rw [goCache_denote_eq]
+      · exact hinv1
+      · exact hinv2
     · intro h
-      rw [go_denote_mem_prefix]
-      apply lih
-      apply go_Inv_of_Inv
-      exact hinv
+      rw [goCache_denote_mem_prefix]
+      rw [goCache_denote_eq]
+      · apply goCache_BvInv_of_BvInv
+        exact hinv1
+      · apply goCache_Inv_of_Inv
+        · exact hinv1
+        · exact hinv2
     · intro h
-      apply rih
-      apply go_Inv_of_Inv
-      apply go_Inv_of_Inv
-      exact hinv
+      rw [goCache_denote_eq]
+      · apply goCache_BvInv_of_BvInv
+        apply goCache_BvInv_of_BvInv
+        exact hinv1
+      · apply goCache_Inv_of_Inv
+        · apply goCache_BvInv_of_BvInv
+          exact hinv1
+        · apply goCache_Inv_of_Inv
+          · exact hinv1
+          · exact hinv2
+  · next g lhs rhs =>
+    match g with
+    | .and | .xor | .beq | .or =>
+      simp only [Ref.cast_eq, denote_mkAndCached, denote_mkXorCached, denote_mkBEqCached,
+        denote_mkOrCached, denote_projected_entry, eval_gate, Gate.eval]
+      rw [goCache_denote_eq]
+      · rw [goCache_denote_mem_prefix]
+        rw [goCache_denote_eq]
+        · exact hinv1
+        · exact hinv2
+      · apply goCache_BvInv_of_BvInv
+        exact hinv1
+      · apply goCache_Inv_of_Inv
+        · exact hinv1
+        · exact hinv2
+termination_by (sizeOf expr, 0, 0)
 
 end
 
@@ -111,8 +313,9 @@ end bitblast
 theorem denote_bitblast (expr : BVLogicalExpr) (assign : BVExpr.Assignment) :
     ⟦bitblast expr, assign.toAIGAssignment⟧ = expr.eval assign := by
   unfold bitblast
-  rw [bitblast.go_eval_eq_eval]
-  apply BVExpr.Cache.Inv_empty
+  rw [bitblast.goCache_denote_eq]
+  · apply BVExpr.Cache.Inv_empty
+  · apply Cache.Inv_empty
 
 theorem unsat_of_bitblast (expr : BVLogicalExpr) : expr.bitblast.Unsat → expr.Unsat :=  by
   intro h assign

src/Std/Tactic/BVDecide/Bitblast/BoolExpr.lean

@@ -1,11 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
-
-/-!
-This directory contains the definition of generic boolean substructures for SMT-like problems.
--/

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

@@ -1,82 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-prelude
-import Init.Notation
-import Init.Data.Bool
-
-/-!
-This module contains the definition of a generic boolean substructure for SMT problems with
-`BoolExpr`. For verification purposes `BoolExpr.Sat` and `BoolExpr.Unsat` are provided.
--/
-
-namespace Std.Tactic.BVDecide
-
-inductive Gate
-  | and
-  | xor
-  | beq
-  | or
-
-namespace Gate
-
-def toString : Gate → String
-  | and => "&&"
-  | xor => "^^"
-  | beq => "=="
-  | or => "||"
-
-def eval : Gate → Bool → Bool → Bool
-  | and => (· && ·)
-  | xor => (· ^^ ·)
-  | beq => (· == ·)
-  | or => (· || ·)
-
-end Gate
-
-inductive BoolExpr (α : Type)
-  | literal : α → BoolExpr α
-  | const : Bool → BoolExpr α
-  | not : BoolExpr α → BoolExpr α
-  | gate : Gate → BoolExpr α → BoolExpr α → BoolExpr α
-  | ite : BoolExpr α → BoolExpr α → BoolExpr α → BoolExpr α
-
-namespace BoolExpr
-
-def toString [ToString α] : BoolExpr α → String
-  | literal a => ToString.toString a
-  | const b => ToString.toString b
-  | not x => "!" ++ toString x
-  | gate g x y => "(" ++ toString x ++ " " ++ g.toString ++ " " ++ toString y ++ ")"
-  | ite d l r => "(if " ++ toString d ++ " " ++ toString l ++ " " ++ toString r ++ ")"
-
-instance [ToString α] : ToString (BoolExpr α) := ⟨toString⟩
-
-def eval (a : α → Bool) : BoolExpr α → Bool
-  | .literal l => a l
-  | .const b => b
-  | .not x => !eval a x
-  | .gate g x y => g.eval (eval a x) (eval a y)
-  | .ite d l r => bif d.eval a then l.eval a else r.eval a
-
-@[simp] theorem eval_literal : eval a (.literal l) = a l := rfl
-@[simp] theorem eval_const : eval a (.const b) = b := rfl
-@[simp] theorem eval_not : eval a (.not x) = !eval a x := rfl
-@[simp] theorem eval_gate : eval a (.gate g x y) = g.eval (eval a x) (eval a y) := rfl
-@[simp] theorem eval_ite : eval a (.ite d l r) = bif d.eval a then l.eval a else r.eval a := rfl
-
-def Sat (a : α → Bool) (x : BoolExpr α) : Prop := eval a x = true
-def Unsat (x : BoolExpr α) : Prop := ∀ f, eval f x = false
-
-theorem sat_and {x y : BoolExpr α} {a : α → Bool} (hx : Sat a x) (hy : Sat a y) :
-    Sat a (BoolExpr.gate .and x y) := by
-  simp only [Sat] at *
-  simp [hx, hy, Gate.eval]
-
-theorem sat_true {a : α → Bool} : Sat a (BoolExpr.const true : BoolExpr α) := rfl
-
-end BoolExpr
-
-end Std.Tactic.BVDecide