perf: bv_decide introduce an expression level bitblasting cache (#7606)
This PR introduces an expression level bitblasting cache to bv_decide.
This commit is contained in:
Henrik Böving
GitHub
parent
eb0c015e7c
commit
b97a7ef4cb
3 changed files with 628 additions and 258 deletions
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue