From b97a7ef4cb103973665c4b20d6f650bbd095ec2c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 22 Mar 2025 14:25:52 +0100 Subject: [PATCH] perf: bv_decide introduce an expression level bitblasting cache (#7606) This PR introduces an expression level bitblasting cache to bv_decide. --- .../BVDecide/Bitblast/BVExpr/Basic.lean | 4 +- .../Bitblast/BVExpr/Circuit/Impl/Expr.lean | 314 ++++++---- .../Bitblast/BVExpr/Circuit/Lemmas/Expr.lean | 568 +++++++++++++----- 3 files changed, 628 insertions(+), 258 deletions(-) diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean index 3f6f999837..c18b23280a 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean @@ -74,7 +74,7 @@ inductive BVBinOp where Unsigned modulo. -/ | umod - deriving DecidableEq, Hashable + deriving Hashable, DecidableEq namespace BVBinOp @@ -135,7 +135,7 @@ inductive BVUnOp where constant `Nat` value. -/ | arithShiftRightConst (n : Nat) - deriving DecidableEq, Hashable + deriving Hashable, DecidableEq namespace BVUnOp diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean index 183a0315d7..62da1f0857 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean @@ -31,20 +31,100 @@ open Std.Sat namespace BVExpr +structure Cache.Key where + w : Nat + expr : BVExpr w + deriving DecidableEq, Hashable + +structure Cache (aig : AIG BVBit) where + map : Std.DHashMap Cache.Key (fun k => Vector (Nat × Bool) k.w) + hbound : ∀ k (h1 : k ∈ map), ∀ (h2 : i < k.1), (map.get k h1)[i].1 < aig.decls.size + +@[inline] +def Cache.empty : Cache aig := + ⟨{}, by simp⟩ + +@[inline] +def Cache.insert (cache : Cache aig) (expr : BVExpr w) (refs : AIG.RefVec aig w) : + Cache aig := + let ⟨map, hbound⟩ := cache + have := by + intro i k hk h2 + rw [Std.DHashMap.get_insert] + split + · next heq => + rcases k with ⟨w, expr⟩ + simp only [beq_iff_eq, Key.mk.injEq] at heq + rcases heq with ⟨heq1, heq2⟩ + symm at heq1 + subst heq1 + have := refs.hrefs h2 + rw [getElem_congr_coll] + · exact this + · simp + · apply hbound + ⟨map.insert ⟨w, expr⟩ refs.refs, this⟩ + +@[inline] +def Cache.get? (cache : Cache aig) (expr : BVExpr w) : Option (AIG.RefVec aig w) := + match h : cache.map.get? ⟨w, expr⟩ with + | some refs => + have : ⟨w, expr⟩ ∈ cache.map := by + rw [Std.DHashMap.mem_iff_contains, Std.DHashMap.contains_eq_isSome_get?] + simp [h] + have : cache.map.get ⟨w, expr⟩ this = refs := by + rw [Std.DHashMap.get?_eq_some_get (h := this)] at h + simpa using h + have := by + intro i hi + rw [← this] + apply cache.hbound + some ⟨refs, 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 i k hk h2 + apply Nat.lt_of_lt_of_le + · apply hbound + · exact h + ⟨map, this⟩ + +structure Return (aig : AIG BVBit) (w : Nat) where + result : AIG.ExtendingRefVecEntry aig w + cache : Cache result.val.aig + +set_option maxHeartbeats 400000 in def bitblast (aig : AIG BVBit) (expr : BVExpr w) : AIG.RefVecEntry BVBit w := - go aig expr |>.val + goCache aig expr .empty |>.result.val where - go {w : Nat} (aig : AIG BVBit) (expr : BVExpr w) : AIG.ExtendingRefVecEntry aig w := + goCache {w : Nat} (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : Return aig w := + match cache.get? expr with + | some vec => + ⟨⟨⟨aig, vec⟩, Nat.le_refl ..⟩, cache⟩ + | none => + let ⟨result, cache⟩ := go aig expr cache + ⟨result, cache.insert expr result.val.vec⟩ + termination_by (sizeOf expr, 1) + + go {w : Nat} (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : Return aig w := match expr with | .var a => let res := bitblast.blastVar aig ⟨a⟩ - ⟨res, AIG.LawfulVecOperator.le_size (f := bitblast.blastVar) ..⟩ + have := AIG.LawfulVecOperator.le_size (f := bitblast.blastVar) .. + let cache := cache.cast this + ⟨⟨res, this⟩, cache⟩ | .const val => let res := bitblast.blastConst aig val - ⟨res, AIG.LawfulVecOperator.le_size (f := bitblast.blastConst) ..⟩ - | .bin lhs op rhs => - let ⟨⟨aig, lhs⟩, hlaig⟩ := go aig lhs - let ⟨⟨aig, rhs⟩, hraig⟩ := go aig rhs + have := AIG.LawfulVecOperator.le_size (f := bitblast.blastConst) .. + let cache := cache.cast this + ⟨⟨res, this⟩, cache⟩ + | .bin lhsExpr op rhsExpr => + let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhsExpr cache + let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhsExpr cache let lhs := lhs.cast <| by dsimp only at hlaig hraig omega @@ -55,111 +135,111 @@ where apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.zip) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := AIG.RefVec.zip) ..)⟩ | .or => let res := AIG.RefVec.zip aig ⟨⟨lhs, rhs⟩, AIG.mkOrCached⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.zip) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := AIG.RefVec.zip) ..)⟩ | .xor => let res := AIG.RefVec.zip aig ⟨⟨lhs, rhs⟩, AIG.mkXorCached⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.zip) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := AIG.RefVec.zip) ..)⟩ | .add => let res := bitblast.blastAdd aig ⟨lhs, rhs⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastAdd) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastAdd) ..)⟩ | .mul => let res := bitblast.blastMul aig ⟨lhs, rhs⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastMul) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastMul) ..)⟩ | .udiv => let res := bitblast.blastUdiv aig ⟨lhs, rhs⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastUdiv) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastUdiv) ..)⟩ | .umod => let res := bitblast.blastUmod aig ⟨lhs, rhs⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastUmod) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastUmod) ..)⟩ | .un op expr => - let ⟨⟨eaig, evec⟩, heaig⟩ := go aig expr + let ⟨⟨⟨eaig, evec⟩, heaig⟩, cache⟩ := goCache aig expr cache match op with | .not => - let res := bitblast.blastNot eaig evec - have := by - apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.map) - dsimp only at heaig - omega - ⟨res, this⟩ + let res := bitblast.blastNot eaig evec + have := by + apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.map) + dsimp only at heaig + omega + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := AIG.RefVec.map) ..)⟩ | .rotateLeft distance => let res := bitblast.blastRotateLeft eaig ⟨evec, distance⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastRotateLeft) dsimp only at heaig assumption - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateLeft) ..)⟩ | .rotateRight distance => let res := bitblast.blastRotateRight eaig ⟨evec, distance⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastRotateRight) dsimp only at heaig assumption - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateRight) ..)⟩ | .arithShiftRightConst distance => let res := bitblast.blastArithShiftRightConst eaig ⟨evec, distance⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastArithShiftRightConst) dsimp only at heaig assumption - ⟨res, this⟩ - | .append lhs rhs _ => - let ⟨⟨aig, lhs⟩, hlaig⟩ := go aig lhs - let ⟨⟨aig, rhs⟩, hraig⟩ := go aig rhs + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRightConst) ..)⟩ + | .append lhs rhs h => + let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache + let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache let lhs := lhs.cast <| by dsimp only at hlaig hraig omega - let res := bitblast.blastAppend aig ⟨lhs, rhs, by omega⟩ + let res := bitblast.blastAppend aig ⟨lhs, rhs, by rw [Nat.add_comm, h]⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastAppend) dsimp only at hlaig hraig omega - ⟨res, this⟩ - | .replicate n expr _ => - let ⟨⟨aig, expr⟩, haig⟩ := go aig expr - let res := bitblast.blastReplicate aig ⟨n, expr, by omega⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastAppend) ..)⟩ + | .replicate n expr h => + let ⟨⟨⟨aig, expr⟩, haig⟩, cache⟩ := goCache aig expr cache + let res := bitblast.blastReplicate aig ⟨n, expr, h⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastReplicate) dsimp only at haig assumption - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastReplicate) ..)⟩ | .extract start len expr => - let ⟨⟨eaig, evec⟩, heaig⟩ := go aig expr + let ⟨⟨⟨eaig, evec⟩, heaig⟩, cache⟩ := goCache aig expr cache let res := bitblast.blastExtract eaig ⟨evec, start⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastExtract) dsimp only at heaig exact heaig - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastExtract) ..)⟩ | .shiftLeft lhs rhs => - let ⟨⟨aig, lhs⟩, hlaig⟩ := go aig lhs - let ⟨⟨aig, rhs⟩, hraig⟩ := go aig rhs + let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache + let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache let lhs := lhs.cast <| by dsimp only at hlaig hraig omega @@ -168,10 +248,10 @@ where apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastShiftLeft) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastShiftLeft) ..)⟩ | .shiftRight lhs rhs => - let ⟨⟨aig, lhs⟩, hlaig⟩ := go aig lhs - let ⟨⟨aig, rhs⟩, hraig⟩ := go aig rhs + let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache + let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache let lhs := lhs.cast <| by dsimp only at hlaig hraig omega @@ -180,10 +260,10 @@ where apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastShiftRight) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastShiftRight) ..)⟩ | .arithShiftRight lhs rhs => - let ⟨⟨aig, lhs⟩, hlaig⟩ := go aig lhs - let ⟨⟨aig, rhs⟩, hraig⟩ := go aig rhs + let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache + let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache let lhs := lhs.cast <| by dsimp only at hlaig hraig omega @@ -192,101 +272,113 @@ where apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastArithShiftRight) dsimp only at hlaig hraig omega - ⟨res, this⟩ + ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRight) ..)⟩ + termination_by (sizeOf expr, 0) -theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) : - ∀ (idx : Nat) (h1) (h2), (go aig expr).val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by - intros idx h1 h2 - induction expr generalizing aig with - | var => - dsimp only [go] - rw [AIG.LawfulVecOperator.decl_eq (f := blastVar)] - | const => - dsimp only [go] - rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)] - | bin lhs op rhs lih rih => + +namespace bitblast + +mutual + +theorem goCache_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : + ∀ (idx : Nat) (h1) (h2), (goCache aig expr cache).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by + generalize hres : goCache aig expr cache = 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) (expr : BVExpr w) (cache : Cache aig) : + ∀ (idx : Nat) (h1) (h2), (go aig expr cache).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by + intro idx h1 h2 + unfold go + split + · rw [AIG.LawfulVecOperator.decl_eq (f := blastVar)] + · rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)] + · next op lhsExpr rhsExpr => match op with | .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 - have := (bitblast.go aig lhs).property + 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 [rih, lih] + rw [goCache_decl_eq, goCache_decl_eq] · omega - · apply Nat.lt_of_lt_of_le h1 -- omega cannot do this :( - apply Nat.le_trans <;> assumption - | un op expr ih => + · apply Nat.lt_of_lt_of_le + · exact h1 + · apply Nat.le_trans <;> assumption + · next op expr => match op with - | .not | .rotateLeft .. | .rotateRight .. - | .arithShiftRightConst .. => - dsimp only [go] + | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. => rw [AIG.LawfulVecOperator.decl_eq] - rw [ih] - have := (go aig expr).property + rw [goCache_decl_eq] + have := (goCache aig expr cache).result.property omega - | append lhs rhs _ lih rih => - dsimp only [go] - have := (bitblast.go aig lhs).property - have := (bitblast.go aig lhs).property - have := (go (go aig lhs).1.aig rhs).property - rw [AIG.LawfulVecOperator.decl_eq (f := blastAppend)] - rw [rih, lih] + · next lhsExpr rhsExpr h => + 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 - · apply Nat.lt_of_lt_of_le h1 - apply Nat.le_trans <;> assumption - | replicate n inner _ ih => - dsimp only [go] + · apply Nat.lt_of_lt_of_le + · exact h1 + · apply Nat.le_trans <;> assumption + · next inner _ => rw [AIG.LawfulVecOperator.decl_eq (f := blastReplicate)] - rw [ih] - have := (go aig inner).property + rw [goCache_decl_eq] + have := (goCache aig inner cache).result.property omega - | extract hi lo inner ih => - dsimp only [go] + · next hi lo inner => rw [AIG.LawfulVecOperator.decl_eq (f := blastExtract)] - rw [ih] - have := (go aig inner).property + rw [goCache_decl_eq] + have := (goCache aig inner cache).result.property omega - | shiftLeft lhs rhs lih rih => - dsimp only [go] - have := (bitblast.go aig lhs).property - have := (bitblast.go aig lhs).property - have := (go (go aig lhs).1.aig rhs).property + · next rhsExpr lhsExpr => + 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 (f := blastShiftLeft)] - rw [rih, lih] + rw [goCache_decl_eq, goCache_decl_eq] · omega - · apply Nat.lt_of_lt_of_le h1 - apply Nat.le_trans <;> assumption - | shiftRight lhs rhs lih rih => - dsimp only [go] - have := (bitblast.go aig lhs).property - have := (bitblast.go aig lhs).property - have := (go (go aig lhs).1.aig rhs).property + · apply Nat.lt_of_lt_of_le + · exact h1 + · apply Nat.le_trans <;> assumption + · next rhsExpr lhsExpr => + 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 (f := blastShiftRight)] - rw [rih, lih] + rw [goCache_decl_eq, goCache_decl_eq] · omega - · apply Nat.lt_of_lt_of_le h1 - apply Nat.le_trans <;> assumption - | arithShiftRight lhs rhs lih rih => - dsimp only [go] - have := (bitblast.go aig lhs).property - have := (bitblast.go aig lhs).property - have := (go (go aig lhs).1.aig rhs).property + · apply Nat.lt_of_lt_of_le + · exact h1 + · apply Nat.le_trans <;> assumption + · next rhsExpr lhsExpr => + 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 (f := blastArithShiftRight)] - rw [rih, lih] + rw [goCache_decl_eq, goCache_decl_eq] · omega - · apply Nat.lt_of_lt_of_le h1 - apply Nat.le_trans <;> assumption + · apply Nat.lt_of_lt_of_le + · exact h1 + · apply Nat.le_trans <;> assumption +termination_by (sizeOf expr, 0) + +end + +end bitblast instance : AIG.LawfulVecOperator BVBit (fun _ w => BVExpr w) bitblast where le_size := by intro _ aig expr unfold bitblast - exact (bitblast.go aig expr).property + exact (bitblast.goCache aig expr _).result.property decl_eq := by intros unfold bitblast - apply bitblast.go_decl_eq + apply bitblast.goCache_decl_eq end BVExpr diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean index f37261bec5..ac5d0a7422 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean @@ -32,17 +32,104 @@ open Std.Sat open Std.Sat.AIG namespace BVExpr + +namespace Cache + +abbrev Inv (assign : Assignment) (aig : AIG BVBit) (cache : Cache aig) : Prop := + ∀ k (h1 : k ∈ cache.map), ∀ (i : Nat) (h2 : i < k.w), + ⟦aig, ⟨(cache.map.get k h1)[i].1, (cache.map.get k h1)[i].2, cache.hbound ..⟩, assign.toAIGAssignment⟧ + = + (k.expr.eval assign).getLsbD i + +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 k hk i h2 + specialize hinv k hk i h2 + rw [← hinv] + apply denote.eq_of_isPrefix (entry := ⟨aig1, _, _, _⟩) + exact hpref + +theorem Inv_insert (cache : Cache aig) (expr : BVExpr w) (refs : AIG.RefVec aig w) + (hinv : Inv assign aig cache) + (hrefs : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, refs.get idx hidx, assign.toAIGAssignment⟧ = (expr.eval assign).getLsbD idx) : + Inv assign aig (cache.insert expr refs) := by + intro k hk i hi + by_cases heq : ⟨w, expr⟩ = k + · rcases k with ⟨kw, kexpr⟩ + simp only [Key.mk.injEq] at heq + rcases heq with ⟨hkeq, hexpr⟩ + subst hkeq + replace hexpr := eq_of_heq hexpr + subst hexpr + have : ((cache.insert expr refs).map.get ⟨w, expr⟩ hk) = refs.refs := by + unfold Cache.insert + apply Std.DHashMap.get_insert_self + specialize hrefs i hi + rw [← hrefs] + congr 3 + all_goals + rw [getElem_congr_coll] + exact this + · have hmem : k ∈ cache.map := by + unfold Cache.insert at hk + apply Std.DHashMap.mem_of_mem_insert + · exact hk + · simp [heq] + have : ((cache.insert expr refs).map.get k hk) = cache.map.get k hmem := by + unfold Cache.insert + rw [Std.DHashMap.get_insert] + simp [heq] + specialize hinv k hmem i hi + rw [← hinv] + congr 3 + all_goals + rw [getElem_congr_coll] + exact this + +theorem get?_eq_some_iff (cache : Cache aig) (expr : BVExpr w) : + cache.get? expr = some refs ↔ cache.map.get? ⟨w, expr⟩ = some refs.refs := by + cases refs + unfold Cache.get? + split <;> simp_all + +theorem denote_eq_eval_of_get?_eq_some_of_Inv (cache : Cache aig) (expr : BVExpr w) + (refs : AIG.RefVec aig w) (hsome : cache.get? expr = some refs) (hinv : Inv assign aig cache) : + ∀ (i : Nat) (h : i < w), + ⟦aig, refs.get i h, assign.toAIGAssignment⟧ = (expr.eval assign).getLsbD i := by + intro i h + rcases refs with ⟨refs, _⟩ + rw [get?_eq_some_iff] at hsome + have hmem : ⟨w, expr⟩ ∈ cache.map := by + rw [Std.DHashMap.mem_iff_contains, Std.DHashMap.contains_eq_isSome_get?] + simp [hsome] + have : refs = cache.map.get ⟨w, expr⟩ hmem := by + rw [Std.DHashMap.get?_eq_some_get (h := hmem)] at hsome + simp only [Option.some.injEq] at hsome + rw [hsome] + specialize hinv ⟨w, expr⟩ hmem i h + rw [← hinv] + subst this + congr + +end Cache + namespace bitblast -theorem go_val_eq_bitblast (aig : AIG BVBit) (expr : BVExpr w) : - (go aig expr).val = bitblast aig expr := by +theorem goCache_val_eq_bitblast (aig : AIG BVBit) (expr : BVExpr w) : + (goCache aig expr .empty).result.val = bitblast aig expr := by rfl -theorem go_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) (start : Nat) - (hstart) : +theorem go_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) + (cache : Cache aig) (start : Nat) (hstart) : ⟦ - (go aig expr).val.aig, - ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (go aig expr).property⟩, + (go aig expr cache).result.val.aig, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (go aig expr cache).result.property⟩, assign.toAIGAssignment ⟧ = @@ -52,155 +139,345 @@ theorem go_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assig · intros apply go_decl_eq · intros - apply (go aig expr).property + apply (go aig expr cache).result.property -theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) : +theorem goCache_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) + (cache : Cache aig) (start : Nat) (hstart) : + ⟦ + (goCache aig expr cache).result.val.aig, + ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (goCache aig expr cache).result.property⟩, + assign.toAIGAssignment + ⟧ + = + ⟦aig, ⟨start, inv, hstart⟩, assign.toAIGAssignment⟧ := by + apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩) + apply IsPrefix.of + · intros + apply goCache_decl_eq + · intros + apply (goCache aig expr cache).result.property + +set_option maxHeartbeats 400000 + +mutual + + +theorem goCache_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) : + ∀ (expr : BVExpr w), + Cache.Inv assign (goCache aig expr cache).result.val.aig (goCache aig expr cache).cache := by + intro expr + generalize hres : goCache aig expr cache = res + unfold goCache at hres + split at hres + · rw [← hres] + exact hinv + · rw [← hres] + dsimp only + apply Cache.Inv_insert + · apply go_Inv_of_Inv + exact hinv + · intro idx hidx + rw [go_denote_eq] + exact hinv +termination_by expr => (sizeOf expr, 1, sizeOf aig) + +theorem go_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) : + ∀ (expr : BVExpr w), + Cache.Inv assign (go aig expr cache).result.val.aig (go aig expr cache).cache := by + intro expr + generalize hres : go aig expr cache = res + unfold go at hres + split at hres + · rw [← hres] + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig (f := blastVar) + · exact hinv + · rw [← hres] + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig (f := blastConst) + · exact hinv + · dsimp only at hres + split at hres + all_goals + rw [← hres] + dsimp only + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig + · apply goCache_Inv_of_Inv + apply goCache_Inv_of_Inv + exact hinv + · dsimp only at hres + split at hres + all_goals + rw [← hres] + dsimp only + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig + · apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + dsimp only + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig + · apply goCache_Inv_of_Inv + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + dsimp only + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig + · apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + dsimp only + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig + · apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + dsimp only + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig + · apply goCache_Inv_of_Inv + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + dsimp only + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig + · apply goCache_Inv_of_Inv + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + dsimp only + apply Cache.Inv_cast + · apply LawfulVecOperator.isPrefix_aig + · apply goCache_Inv_of_Inv + apply goCache_Inv_of_Inv + exact hinv +termination_by expr => (sizeOf expr, 0, 0) + +theorem goCache_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) + (cache : Cache aig) (hinv : Cache.Inv assign aig cache) : ∀ (idx : Nat) (hidx : idx < w), - ⟦(go aig expr).val.aig, (go aig expr).val.vec.get idx hidx, assign.toAIGAssignment⟧ + ⟦(goCache aig expr cache).result.val.aig, (goCache aig expr cache).result.val.vec.get idx hidx, assign.toAIGAssignment⟧ = (expr.eval assign).getLsbD idx := by intro idx hidx - induction expr generalizing aig idx with - | const => - simp [go, denote_blastConst] - | var => - simp [go, hidx, denote_blastVar] - | append lhs rhs hw lih rih => - rename_i lw rw - subst hw - simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append, - BitVec.getLsbD_append] + generalize hres : goCache aig expr cache = res + unfold goCache at hres + split at hres + · next heq => + rw [← hres] + apply Cache.denote_eq_eval_of_get?_eq_some_of_Inv + · exact heq + · exact hinv + · rw [← hres] + rw [go_denote_eq] + exact hinv +termination_by (sizeOf expr, 0, w) + + +theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) + (cache : Cache aig) (hinv : Cache.Inv assign aig cache) : + ∀ (idx : Nat) (hidx : idx < w), + ⟦(go aig expr cache).result.val.aig, (go aig expr cache).result.val.vec.get idx hidx, assign.toAIGAssignment⟧ + = + (expr.eval assign).getLsbD idx := by + intro idx hidx + generalize hres : go aig expr cache = res + unfold go at hres + split at hres + · rw [← hres] + simp + · rw [← hres] + simp + · dsimp only at hres + split at hres + · rw [← hres] + simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkAndCached, eval_bin, + BVBinOp.eval_and, BitVec.getLsbD_and] + congr 1 + · rw [goCache_denote_mem_prefix] + rw [goCache_denote_eq] + exact hinv + · rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkOrCached, eval_bin, + BVBinOp.eval_or, BitVec.getLsbD_or] + congr 1 + · rw [goCache_denote_mem_prefix] + rw [goCache_denote_eq] + exact hinv + · rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkXorCached, eval_bin, + BVBinOp.eval_xor, BitVec.getLsbD_xor] + congr 1 + · rw [goCache_denote_mem_prefix] + rw [goCache_denote_eq] + exact hinv + · rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + simp only [eval_bin, BVBinOp.eval_add] + rw [denote_blastAdd] + · intro idx hidx + rw [goCache_denote_mem_prefix] + simp only [RefVec.get_cast, Ref.cast_eq] + rw [goCache_denote_eq] + · exact hinv + · simp [Ref.hgate] + · intro idx hidx + rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + simp only [eval_bin, BVBinOp.eval_mul] + rw [denote_blastMul] + · intro idx hidx + rw [goCache_denote_mem_prefix] + simp only [RefVec.get_cast, Ref.cast_eq] + rw [goCache_denote_eq] + · exact hinv + · simp [Ref.hgate] + · intro idx hidx + rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + simp only [eval_bin, BVBinOp.eval_udiv] + rw [denote_blastUdiv] + · intro idx hidx + rw [goCache_denote_mem_prefix] + simp only [RefVec.get_cast, Ref.cast_eq] + rw [goCache_denote_eq] + · exact hinv + · simp [Ref.hgate] + · intro idx hidx + rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [← hres] + simp only [eval_bin, BVBinOp.eval_umod] + rw [denote_blastUmod] + · intro idx hidx + rw [goCache_denote_mem_prefix] + simp only [RefVec.get_cast, Ref.cast_eq] + rw [goCache_denote_eq] + · exact hinv + · simp [Ref.hgate] + · intro idx hidx + rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · dsimp only at hres + split at hres + · rw [← hres] + simp only [denote_blastNot, eval_un, BVUnOp.eval_not, hidx, BitVec.getLsbD_eq_getElem, + BitVec.getElem_not, Bool.not_eq_eq_eq_not, Bool.not_not] + rw [goCache_denote_eq] + · apply BitVec.getLsbD_eq_getElem + · exact hinv + · rw [← hres] + simp only [denote_blastRotateLeft, eval_un, BVUnOp.eval_rotateLeft, hidx, + BitVec.getLsbD_eq_getElem, BitVec.getElem_rotateLeft] + split + all_goals + · rw [goCache_denote_eq] + · apply BitVec.getLsbD_eq_getElem + · exact hinv + · rw [← hres] + simp only [denote_blastRotateRight, eval_un, BVUnOp.eval_rotateRight, hidx, + BitVec.getLsbD_eq_getElem, BitVec.getElem_rotateRight] + split + all_goals + · rw [goCache_denote_eq] + · apply BitVec.getLsbD_eq_getElem + · exact hinv + · rw [← hres] + simp only [denote_blastArithShiftRightConst, eval_un, BVUnOp.eval_arithShiftRightConst, hidx, + BitVec.getLsbD_eq_getElem, BitVec.getElem_sshiftRight] + split + · rw [goCache_denote_eq] + · apply BitVec.getLsbD_eq_getElem + · exact hinv + · rw [goCache_denote_eq] + · simp [BitVec.msb_eq_getLsbD_last] + · exact hinv + · next h => + subst h + rw [← hres] + simp only [denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append, BitVec.getLsbD_append] split - · next hsplit => rw [rih] - · next hsplit => rw [go_denote_mem_prefix, lih] - | replicate n expr hw ih => - subst hw - simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem] - | @extract w start len inner ih => - simp only [go, denote_blastExtract, Bool.if_false_right, eval_extract, - BitVec.getLsbD_extractLsb', hidx, decide_true, Bool.true_and] + · rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [goCache_denote_mem_prefix] + rw [goCache_denote_eq] + exact hinv + · next h => + subst h + rw [← hres] + simp only [denote_blastReplicate, eval_replicate, hidx, BitVec.getLsbD_eq_getElem, + BitVec.getElem_replicate] split - · next hsplit => - rw [ih] - · apply Eq.symm + · next h => + simp only [h, Nat.zero_mul, Nat.not_lt_zero] at hidx + · rw [goCache_denote_eq] + · apply BitVec.getLsbD_eq_getElem + · exact hinv + · rw [← hres] + simp only [denote_blastExtract, eval_extract, hidx, BitVec.getLsbD_eq_getElem, + BitVec.getElem_extractLsb'] + split + · rw [goCache_denote_eq] + exact hinv + · symm apply BitVec.getLsbD_ge omega - | shiftLeft lhs rhs lih rih => - simp only [go, eval_shiftLeft] - apply denote_blastShiftLeft - · intros - dsimp only - rw [go_denote_mem_prefix] - rw [← lih (aig := aig)] - · simp - · assumption + · rw [eval_shiftLeft, ← hres, denote_blastShiftLeft] + · intro idx hidx + rw [goCache_denote_mem_prefix] + · simp only [RefVec.get_cast, Ref.cast_eq] + rw [goCache_denote_eq] + exact hinv · simp [Ref.hgate] - · intros - rw [← rih] - | shiftRight lhs rhs lih rih => - simp only [go, eval_shiftRight] - apply denote_blastShiftRight - · intros - dsimp only - rw [go_denote_mem_prefix] - rw [← lih (aig := aig)] - · simp - · assumption + · intro idx hidx + rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [eval_shiftRight, ← hres, denote_blastShiftRight] + · intro idx hidx + rw [goCache_denote_mem_prefix] + · simp only [RefVec.get_cast, Ref.cast_eq] + rw [goCache_denote_eq] + exact hinv · simp [Ref.hgate] - · intros - rw [← rih] - | arithShiftRight lhs rhs lih rih => - simp only [go, eval_arithShiftRight] - apply denote_blastArithShiftRight - · intros - dsimp only - rw [go_denote_mem_prefix] - rw [← lih (aig := aig)] - · simp - · assumption + · intro idx hidx + rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv + · rw [eval_arithShiftRight, ← hres, denote_blastArithShiftRight] + · intro idx hidx + rw [goCache_denote_mem_prefix] + · simp only [RefVec.get_cast, Ref.cast_eq] + rw [goCache_denote_eq] + exact hinv · simp [Ref.hgate] - · intros - rw [← rih] - | bin lhs op rhs lih rih => - cases op with - | and => - simp only [go, RefVec.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and, - BitVec.getLsbD_and] - simp only [go_val_eq_bitblast, RefVec.get_cast] - rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)] - rw [← go_val_eq_bitblast] - rw [lih] - | or => - simp only [go, RefVec.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or, - BitVec.getLsbD_or] - simp only [go_val_eq_bitblast, RefVec.get_cast] - rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)] - rw [← go_val_eq_bitblast] - rw [lih] - | xor => - simp only [go, RefVec.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor, - BitVec.getLsbD_xor] - simp only [go_val_eq_bitblast, RefVec.get_cast] - rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)] - rw [← go_val_eq_bitblast] - rw [lih] - | add => - simp only [go, eval_bin, BVBinOp.eval_add] - apply denote_blastAdd - · intros - dsimp only - rw [go_denote_mem_prefix] - rw [← lih (aig := aig)] - · simp - · assumption - · simp [Ref.hgate] - · intros - rw [← rih] - | mul => - simp only [go, eval_bin, BVBinOp.eval_mul] - apply denote_blastMul - · intros - dsimp only - rw [go_denote_mem_prefix] - rw [← lih (aig := aig)] - · simp - · assumption - · simp [Ref.hgate] - · intros - rw [← rih] - | udiv => - simp only [go, eval_bin, BVBinOp.eval_udiv] - apply denote_blastUdiv - · intros - dsimp only - rw [go_denote_mem_prefix] - rw [← lih (aig := aig)] - · simp - · assumption - · simp [Ref.hgate] - · intros - rw [← rih] - | umod => - simp only [go, eval_bin, BVBinOp.eval_umod] - apply denote_blastUmod - · intros - dsimp only - rw [go_denote_mem_prefix] - rw [← lih (aig := aig)] - · simp - · assumption - · simp [Ref.hgate] - · intros - rw [← rih] - | un op expr ih => - cases op with - | not => simp [go, ih, hidx] - | rotateLeft => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem] - | rotateRight => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem] - | arithShiftRightConst n => - rename_i w - have : ¬(w ≤ idx) := by omega - simp [go, ih, this, BitVec.getLsbD_sshiftRight, BitVec.msb_eq_getLsbD_last ] + · intro idx hidx + rw [goCache_denote_eq] + apply goCache_Inv_of_Inv + exact hinv +termination_by idx => (sizeOf expr, 0, idx) + +end + end bitblast @@ -212,8 +489,9 @@ theorem denote_bitblast (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment (expr.eval assign).getLsbD idx := by intros - rw [← bitblast.go_val_eq_bitblast] - rw [bitblast.go_denote_eq] + rw [← bitblast.goCache_val_eq_bitblast] + rw [bitblast.goCache_denote_eq] + apply Cache.Inv_empty end BVExpr