max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: AIG doesn't need to be modified for constants (#8663)

Browse source
This commit is contained in:
Henrik Böving 2025-06-06 17:32:38 +02:00 • committed by GitHub
parent d16c4052c2
commit eddbe08118
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
35 changed files with 170 additions and 631 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Std/Sat/AIG/Cached.lean
View file

@ -49,8 +49,8 @@ A version of `AIG.mkConst` that uses the subterm cache in `AIG`. This version is
programming, for proving purposes use `AIG.mkGate` and equality theorems to this one.
-/
@[inline]
def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
⟨aig, ⟨0, val, aig.hzero⟩⟩
def mkConstCached (aig : AIG α) (val : Bool) : Ref aig :=
⟨0, val, aig.hzero⟩
/--
A version of `AIG.mkGate` that uses the subterm cache in `AIG`. This version is meant for
@ -88,7 +88,9 @@ where
let rhsVal := AIG.getConstant ⟨decls, cache, hdag, hzero, hconst⟩ input.rhs
match lhsVal, rhsVal with
-- Boundedness
| .some false, _ | _, .some false => mkConstCached ⟨decls, cache, hdag, hzero, hconst⟩ false
| .some false, _ | _, .some false =>
let ref := mkConstCached ⟨decls, cache, hdag, hzero, hconst⟩ false
⟨⟨decls, cache, hdag, hzero, hconst⟩, ref⟩
-- Left Neutrality
| .some true, _ => ⟨⟨decls, cache, hdag, hzero, hconst⟩, ⟨rhs, rinv, by assumption⟩⟩
-- Right Neutrality
@ -97,9 +99,12 @@ where
| _, _ =>
if lhs == rhs then
-- Idempotency
if linv == rinv then ⟨⟨decls, cache, hdag, hzero, hconst⟩, ⟨lhs, linv, by assumption⟩⟩
if linv == rinv then
⟨⟨decls, cache, hdag, hzero, hconst⟩, ⟨lhs, linv, by assumption⟩⟩
-- Contradiction
else mkConstCached ⟨decls, cache, hdag, hzero, hconst⟩ false
else
let ref := mkConstCached ⟨decls, cache, hdag, hzero, hconst⟩ false
⟨⟨decls, cache, hdag, hzero, hconst⟩, ref⟩
else
-- Gate couldn't be simplified
let g := decls.size

6
src/Std/Sat/AIG/CachedGatesLemmas.lean
View file

@ -61,7 +61,7 @@ instance : LawfulOperator α Ref mkNotCached where
@[simp]
theorem denote_mkNotCached {aig : AIG α} {gate : Ref aig} :
⟦aig.mkNotCached gate, assign⟧ = !⟦aig, gate, assign⟧ := by
simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate]
simp [mkNotCached]
theorem mkAndCached_le_size (aig : AIG α) (input : BinaryInput aig) :
aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size := by
@ -103,7 +103,7 @@ instance : LawfulOperator α BinaryInput mkOrCached where
theorem denote_mkOrCached {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkOrCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by
rw [← or_as_aig]
simp [mkOrCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
simp [mkOrCached]
theorem mkXorCached_le_size (aig : AIG α) {input : BinaryInput aig} :
@ -195,7 +195,7 @@ instance : LawfulOperator α BinaryInput mkImpCached where
theorem denote_mkImpCached {aig : AIG α} {input : BinaryInput aig} :
⟦aig.mkImpCached input, assign⟧ = ( !⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by
rw [← imp_as_aig]
simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
simp [mkImpCached]
end AIG

46
src/Std/Sat/AIG/CachedLemmas.lean
View file

@ -91,36 +91,12 @@ theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α} :
rw [denote_mkAtom_cached heq1]
· simp [mkAtom, denote]
theorem mkConstCached_aig (aig : AIG α) (val : Bool) : (aig.mkConstCached val).aig = aig := by
simp [mkConstCached]
/--
The AIG produced by `AIG.mkConstCached` agrees with the input AIG on all indices that are valid for
both.
-/
theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} :
(aig.mkConstCached val).aig.decls[idx]'h = aig.decls[idx] := by
simp [mkConstCached_aig]
/--
`AIG.mkConstCached` never shrinks the underlying AIG.
-/
theorem mkConstCached_le_size (aig : AIG α) (val : Bool) :
aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size := by
simp [mkConstCached_aig]
instance : LawfulOperator α (fun _ => Bool) mkConstCached where
le_size := mkConstCached_le_size
decl_eq := by
intros
apply mkConstCached_decl_eq
/--
The central equality theorem between `mkConstCached` and `mkConst`.
-/
@[simp]
theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α} :
⟦aig.mkConstCached val, assign⟧ = ⟦aig.mkConst val, assign⟧ := by
theorem denote_mkConstCached {aig : AIG α} :
⟦aig, aig.mkConstCached val, assign⟧ = val := by
simp only [mkConstCached, denote_mkConst]
unfold denote denote.go
split
@ -150,18 +126,16 @@ theorem mkGateCached.go_le_size (aig : AIG α) (input : BinaryInput aig) :
dsimp only [go]
split
· simp
· split <;> try simp [mkConstCached_le_size]
· split <;> try simp
split
· split
· simp
· simp [mkConstCached_le_size]
· split <;> simp
· simp
/--
`AIG.mkGateCached` never shrinks the underlying AIG.
-/
theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig)
: aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by
theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig) :
aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by
dsimp only [mkGateCached]
split
· apply mkGateCached.go_le_size
@ -178,11 +152,9 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : BinaryInput aig) :
simp
· split at hres
· rw [← hres]
intros
rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)]
simp
· rw [← hres]
intros
rw [LawfulOperator.decl_eq (f := AIG.mkConstCached)]
simp
· rw [← hres]
intros
simp
@ -196,7 +168,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : BinaryInput aig) :
simp
· rw [← hres]
intros
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
simp
· rw [← hres]
dsimp only
intro idx h1 h2

5
src/Std/Sat/AIG/LawfulOperator.lean
View file

@ -30,6 +30,11 @@ structure IsPrefix (decls1 decls2 : Array (Decl α)) : Prop where
-/
idx_eq : ∀ idx (h : idx < decls1.size), decls2[idx]'(by omega) = decls1[idx]'h
theorem IsPrefix.rfl {decls : Array (Decl α)} : IsPrefix decls decls := by
apply IsPrefix.of
· simp
· simp
@[simp]
theorem IsPrefix_push {decls : Array (Decl α)} : IsPrefix decls (decls.push decl) := by
apply IsPrefix.of

29
src/Std/Sat/AIG/RefVecOperator/Fold.lean
View file

@ -19,14 +19,8 @@ variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α}
def fold (aig : AIG α) (vec : RefVec aig len)
(func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func] :
Entrypoint α :=
let res := aig.mkConstCached true
let aig := res.aig
let acc := res.ref
let input := vec.cast <| by
intros
apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
omega
go aig acc 0 len input func
let acc := aig.mkConstCached true
go aig acc 0 len vec func
where
@[specialize]
go (aig : AIG α) (acc : Ref aig) (idx : Nat) (len : Nat) (input : RefVec aig len)
@ -63,8 +57,7 @@ theorem fold_le_size {aig : AIG α} (vec : RefVec aig len)
aig.decls.size ≤ (fold aig vec func).1.decls.size := by
unfold fold
dsimp only
refine Nat.le_trans ?_ (by apply fold.go_le_size)
apply LawfulOperator.le_size (f := mkConstCached)
apply fold.go_le_size
theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefVec aig len)
(f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] :
@ -95,9 +88,6 @@ theorem fold_decl_eq {aig : AIG α} (vec : RefVec aig len)
unfold fold
dsimp only
rw [fold.go_decl_eq]
rw [LawfulOperator.decl_eq (f := mkConstCached)]
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
assumption
theorem fold_lt_size_of_lt_aig_size (aig : AIG α) (vec : RefVec aig len)
(func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func]
@ -177,18 +167,7 @@ theorem denote_fold_and {aig : AIG α} (s : RefVec aig len) :
(∀ (idx : Nat) (hidx : idx < len), ⟦aig, s.get idx hidx, assign⟧) := by
unfold fold
rw [fold.denote_go_and]
· simp only [denote_projected_entry, mkConstCached_eval_eq_mkConst_eval, denote_mkConst,
Nat.zero_le, get_cast, Ref.cast_eq, true_implies, true_and]
constructor
· intro h idx hidx
specialize h idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)] at h
rw [← h]
· intro h idx hidx
specialize h idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)]
· simp only [← h]
· apply RefVec.hrefs
· simp
· omega
end RefVec

52
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
View file

@ -21,64 +21,20 @@ namespace bitblast
variable [Hashable α] [DecidableEq α]
def blastConst (aig : AIG α) (val : BitVec w) : AIG.RefVecEntry α w :=
def blastConst (aig : AIG α) (val : BitVec w) : AIG.RefVec aig w :=
go aig val 0 (.emptyWithCapacity w) (by omega)
where
go (aig : AIG α) (val : BitVec w) (curr : Nat) (s : AIG.RefVec aig curr) (hcurr : curr ≤ w) :
AIG.RefVecEntry α w :=
AIG.RefVec aig w :=
if hcurr : curr < w then
let res := aig.mkConstCached (val.getLsbD curr)
let aig := res.aig
let bitRef := res.ref
let s := s.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let bitRef := aig.mkConstCached (val.getLsbD curr)
let s := s.push bitRef
go aig val (curr + 1) s (by omega)
else
have hcurr : curr = w := by omega
⟨aig, hcurr ▸ s⟩
hcurr ▸ s
termination_by w - curr
theorem blastConst.go_le_size {aig : AIG α} (curr : Nat) (s : AIG.RefVec aig curr) (val : BitVec w)
(hcurr : curr ≤ w) :
aig.decls.size ≤ (go aig val curr s hcurr).aig.decls.size := by
unfold go
split
· dsimp only
refine Nat.le_trans ?_ (by apply go_le_size)
apply AIG.LawfulOperator.le_size
· simp
termination_by w - curr
theorem blastConst.go_decl_eq {aig : AIG α} (i : Nat) (s : AIG.RefVec aig i) (val : BitVec w)
(hi : i ≤ w) :
∀ (curr : Nat) (h1) (h2),
(go aig val i s hi).aig.decls[curr]'h2 = aig.decls[curr]'h1 := by
generalize hgo : go aig val i s hi = res
unfold go at hgo
split at hgo
· dsimp only at hgo
rw [← hgo]
intro curr h1 h2
rw [blastConst.go_decl_eq]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
assumption
· dsimp only at hgo
rw [← hgo]
intros
simp
termination_by w - i
instance : AIG.LawfulVecOperator α (fun _ w => BitVec w) blastConst where
le_size := by
intros
unfold blastConst
apply blastConst.go_le_size
decl_eq := by
intros
unfold blastConst
apply blastConst.go_decl_eq
end bitblast
end BVExpr

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

@ -129,9 +129,7 @@ where
⟨⟨res, this⟩, cache⟩
| .const val =>
let res := bitblast.blastConst aig val
have := AIG.LawfulVecOperator.le_size (f := bitblast.blastConst) ..
let cache := cache.cast this
⟨⟨res, this⟩, cache⟩
⟨⟨⟨aig, res⟩, by simp⟩, cache⟩
| .bin lhsExpr op rhsExpr =>
let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhsExpr cache
let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhsExpr cache
@ -316,7 +314,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
unfold go
split
· rw [AIG.LawfulVecOperator.decl_eq (f := blastVar)]
· rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
· simp
· 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

11
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
View file

@ -168,10 +168,7 @@ def blastAdd (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry
blast aig ⟨rhs, lhs⟩
where
blast (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
let res := aig.mkConstCached false
let aig := res.aig
let cin := res.ref
let input := input.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let cin := aig.mkConstCached false
let ⟨lhs, rhs⟩ := input
go aig lhs rhs 0 (by omega) cin (.emptyWithCapacity w)
@ -238,16 +235,12 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blast where
intros
unfold blast
dsimp only
refine Nat.le_trans ?_ (by apply go_le_size)
apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
apply go_le_size
decl_eq := by
intros
unfold blast
dsimp only
rw [go_decl_eq]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
assumption
end blastAdd

18
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
View file

@ -28,19 +28,16 @@ structure ExtractTarget (aig : AIG α) (len : Nat) where
def blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth) :
AIG.RefVecEntry α newWidth :=
let ⟨input, start⟩ := target
let res := aig.mkConstCached false
let aig := res.aig
let falseRef := res.ref
let input := input.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
⟨aig, go input start falseRef 0 (by omega) (.emptyWithCapacity newWidth)⟩
⟨aig, go input start 0 (by omega) (.emptyWithCapacity newWidth)⟩
where
go {aig : AIG α} {w : Nat} (input : AIG.RefVec aig w) (start : Nat) (falseRef : AIG.Ref aig)
(curr : Nat) (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :
go {aig : AIG α} {w : Nat} (input : AIG.RefVec aig w) (start : Nat) (curr : Nat)
(hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :
AIG.RefVec aig newWidth :=
if h : curr < newWidth then
let falseRef := aig.mkConstCached false
let nextRef := input.getD (start + curr) falseRef
let s := s.push nextRef
go input start falseRef (curr + 1) (by omega) s
go input start (curr + 1) (by omega) s
else
have : curr = newWidth := by omega
this ▸ s
@ -50,12 +47,11 @@ instance : AIG.LawfulVecOperator α ExtractTarget blastExtract where
le_size := by
intros
unfold blastExtract
dsimp only
apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
simp
decl_eq := by
intros
unfold blastExtract
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
simp
end bitblast
end BVExpr

20
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
View file

@ -24,25 +24,11 @@ structure GetLsbDTarget (aig : AIG α) where
vec : AIG.RefVec aig w
idx : Nat
def blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) : AIG.Entrypoint α :=
def blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) : AIG.Ref aig :=
if h : target.idx < target.w then
⟨aig, target.vec.get target.idx h⟩
target.vec.get target.idx h
else
AIG.mkConstCached aig false
instance : AIG.LawfulOperator α GetLsbDTarget blastGetLsbD where
le_size := by
intros
unfold blastGetLsbD
split
· simp
· apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
decl_eq := by
intros
unfold blastGetLsbD
split
· simp
· rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
aig.mkConstCached false
end BVPred

17
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
View file

@ -41,11 +41,7 @@ where
⟨aig, h ▸ .empty⟩
else
have : 0 < w := by omega
let res := blastConst aig 0
let aig := res.aig
let zero := res.vec
have := AIG.LawfulVecOperator.le_size (f := blastConst) ..
let input := input.cast this
let zero := blastConst aig 0
let ⟨lhs, rhs⟩ := input
let res := AIG.RefVec.ite aig ⟨rhs.get 0 (by assumption), lhs, zero⟩
let aig := res.aig
@ -139,8 +135,7 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blast where
· simp
· dsimp only
refine Nat.le_trans ?_ (by apply blastMul.go_le_size)
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
apply AIG.LawfulVecOperator.le_size (f := blastConst)
apply AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite)
decl_eq := by
intros
unfold blast
@ -149,12 +144,8 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blast where
· dsimp only
rw [blastMul.go_decl_eq]
rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
assumption
end blastMul

10
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean
View file

@ -27,10 +27,7 @@ def blastNeg (aig : AIG α) (input : AIG.RefVec aig w) : AIG.RefVecEntry α w :=
let aig := res.aig
let notInput := res.vec
let res := blastConst aig 1#w
let aig := res.aig
let one := res.vec
let notInput := notInput.cast <| AIG.LawfulVecOperator.le_size (f := blastConst) ..
let one := blastConst aig 1#w
blastAdd aig ⟨notInput, one⟩
@ -40,20 +37,15 @@ instance : AIG.LawfulVecOperator α AIG.RefVec blastNeg where
unfold blastNeg
dsimp only
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastAdd)
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastConst)
apply AIG.LawfulVecOperator.le_size (f := blastNot)
decl_eq := by
intros
unfold blastNeg
dsimp only
rw [AIG.LawfulVecOperator.decl_eq (f := blastAdd)]
rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
rw [AIG.LawfulVecOperator.decl_eq (f := blastNot)]
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNot)
assumption
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNot)
assumption
end bitblast
end BVExpr

16
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
View file

@ -35,12 +35,7 @@ where
AIG.RefVecEntry α w :=
if hidx : curr < w then
if hdist : curr < distance then
let res := aig.mkConstCached false
let aig := res.aig
let zeroRef := res.ref
have hfinal := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let s := s.cast hfinal
let input := input.cast hfinal
let zeroRef := aig.mkConstCached false
let s := s.push zeroRef
go aig input distance (curr + 1) (by omega) s
else
@ -58,10 +53,8 @@ theorem blastShiftLeftConst.go_le_size (aig : AIG α) (distance : Nat) (input :
split
· dsimp only
split
· refine Nat.le_trans ?_ (by apply go_le_size)
apply AIG.LawfulOperator.le_size
· refine Nat.le_trans ?_ (by apply go_le_size)
omega
· apply go_le_size
· apply go_le_size
· simp
termination_by w - curr
@ -77,9 +70,6 @@ theorem blastShiftLeftConst.go_decl_eq (aig : AIG α) (distance : Nat) (input :
· rw [← hgo]
intro idx h1 h2
rw [blastShiftLeftConst.go_decl_eq]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
assumption
· rw [← hgo]
intro idx h1 h2
rw [blastShiftLeftConst.go_decl_eq]

16
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
View file

@ -38,12 +38,7 @@ where
let s := s.push (input.get (distance + curr) (by omega))
go aig input distance (curr + 1) (by omega) s
else
let res := aig.mkConstCached false
let aig := res.aig
let zeroRef := res.ref
have hfinal := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let s := s.cast hfinal
let input := input.cast hfinal
let zeroRef := aig.mkConstCached false
let s := s.push zeroRef
go aig input distance (curr + 1) (by omega) s
else
@ -58,10 +53,8 @@ theorem blastShiftRightConst.go_le_size (aig : AIG α) (distance : Nat) (input :
split
· dsimp only
split
· refine Nat.le_trans ?_ (by apply go_le_size)
omega
· refine Nat.le_trans ?_ (by apply go_le_size)
apply AIG.LawfulOperator.le_size
· apply go_le_size
· apply go_le_size
· simp
termination_by w - curr
@ -80,9 +73,6 @@ theorem blastShiftRightConst.go_decl_eq (aig : AIG α) (distance : Nat) (input :
· rw [← hgo]
intro idx h1 h2
rw [blastShiftRightConst.go_decl_eq]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
assumption
· simp [← hgo]
termination_by w - curr

90
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
View file

@ -57,28 +57,28 @@ structure BlastDivSubtractShiftOutput (old : AIG α) (w : Nat) where
r : AIG.RefVec aig w
hle : old.decls.size ≤ aig.decls.size
def blastDivSubtractShift (aig : AIG α) (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
def blastDivSubtractShift (aig : AIG α) (n d : AIG.RefVec aig w) (wn wr : Nat)
(q r : AIG.RefVec aig w) : BlastDivSubtractShiftOutput aig w :=
let wn := wn - 1
let wr := wr + 1
let falseRef := aig.mkConstCached false
let res := blastUdiv.blastShiftConcat aig ⟨r, n.getD wn falseRef⟩
let aig := res.aig
let r' := res.vec
have := AIG.LawfulVecOperator.le_size (f := blastUdiv.blastShiftConcat) ..
let falseRef := falseRef.cast this
let trueRef := trueRef.cast this
let d := d.cast this
let q := q.cast this
let falseRef := aig.mkConstCached false
let res := blastUdiv.blastShiftConcat aig ⟨q, falseRef⟩
let aig := res.aig
let posQ := res.vec
have := AIG.LawfulVecOperator.le_size (f := blastUdiv.blastShiftConcat) ..
let trueRef := trueRef.cast this
let d := d.cast this
let q := q.cast this
let r' := r'.cast this
let trueRef := aig.mkConstCached true
let res := blastUdiv.blastShiftConcat aig ⟨q, trueRef⟩
let aig := res.aig
let negQ := res.vec
@ -130,9 +130,9 @@ def blastDivSubtractShift (aig : AIG α) (falseRef trueRef : AIG.Ref aig) (n d :
apply AIG.LawfulVecOperator.le_size (f := blastShiftConcat)
⟨aig, wn, wr, nextQ, nextR, this⟩
theorem blastDivSubtractShift_le_size (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
theorem blastDivSubtractShift_le_size (aig : AIG α)
(n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
aig.decls.size ≤ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size := by
aig.decls.size ≤ (blastDivSubtractShift aig n d wn wr q r).aig.decls.size := by
unfold blastDivSubtractShift
dsimp only
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
@ -143,11 +143,11 @@ theorem blastDivSubtractShift_le_size (aig : AIG α) (falseRef trueRef : AIG.Ref
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv.blastShiftConcat)
apply AIG.LawfulVecOperator.le_size (f := blastUdiv.blastShiftConcat)
theorem blastDivSubtractShift_decl_eq (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
(n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
theorem blastDivSubtractShift_decl_eq (aig : AIG α) (n d : AIG.RefVec aig w) (wn wr : Nat)
(q r : AIG.RefVec aig w) :
∀ (idx : Nat) (h1) (h2),
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
generalize hres : blastDivSubtractShift aig falseRef trueRef n d wn wr q r = res
(blastDivSubtractShift aig n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
generalize hres : blastDivSubtractShift aig n d wn wr q r = res
unfold blastDivSubtractShift at hres
dsimp only at hres
rw [← hres]
@ -193,23 +193,21 @@ structure BlastUdivOutput (old : AIG α) (w : Nat) where
r : AIG.RefVec aig w
hle : old.decls.size ≤ aig.decls.size
def go (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w)
def go (aig : AIG α) (curr : Nat) (n d : AIG.RefVec aig w)
(wn wr : Nat) (q r : AIG.RefVec aig w) : BlastUdivOutput aig w :=
match curr with
| 0 => ⟨aig, q, r, by omega⟩
| curr + 1 =>
let res := blastDivSubtractShift aig falseRef trueRef n d wn wr q r
let res := blastDivSubtractShift aig n d wn wr q r
let aig := res.aig
let wn := res.wn
let wr := res.wr
let q := res.q
let r := res.r
have := res.hle
let falseRef := falseRef.cast this
let trueRef := trueRef.cast this
let n := n.cast this
let d := d.cast this
let res := go aig curr falseRef trueRef n d wn wr q r
let res := go aig curr n d wn wr q r
let aig := res.aig
let q := res.q
let r := res.r
@ -224,9 +222,9 @@ def go (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig) (n d : AIG.R
apply AIG.LawfulVecOperator.le_size (f := blastShiftConcat)
⟨aig, q, r, this⟩
theorem go_le_size (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
(n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
aig.decls.size ≤ (go aig curr falseRef trueRef n d wn wr q r).aig.decls.size := by
theorem go_le_size (aig : AIG α) (curr : Nat) (n d : AIG.RefVec aig w) (wn wr : Nat)
(q r : AIG.RefVec aig w) :
aig.decls.size ≤ (go aig curr n d wn wr q r).aig.decls.size := by
unfold go
dsimp only
split
@ -234,11 +232,11 @@ theorem go_le_size (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
· refine Nat.le_trans ?_ (by apply go_le_size)
apply blastUdiv.blastDivSubtractShift_le_size
theorem go_decl_eq (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
(n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
theorem go_decl_eq (aig : AIG α) (curr : Nat) (n d : AIG.RefVec aig w) (wn wr : Nat)
(q r : AIG.RefVec aig w) :
∀ (idx : Nat) (h1) (h2),
(go aig curr falseRef trueRef n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
generalize hgo : go aig curr falseRef trueRef n d wn wr q r = res
(go aig curr n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
generalize hgo : go aig curr n d wn wr q r = res
unfold go at hgo
dsimp only at hgo
split at hgo
@ -254,39 +252,18 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
end blastUdiv
def blastUdiv (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
let res := blastConst aig 0#w
let aig := res.aig
let zero := res.vec
let input := input.cast <| AIG.LawfulVecOperator.le_size (f := blastConst) ..
let res := aig.mkConstCached false
let aig := res.aig
let falseRef := res.ref
have := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let zero := zero.cast this
let input := input.cast this
let res := aig.mkConstCached true
let aig := res.aig
let trueRef := res.ref
have := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let falseRef := falseRef.cast this
let zero := zero.cast this
let input := input.cast this
let zero := blastConst aig 0#w
let ⟨lhs, rhs⟩ := input
let res := BVPred.mkEq aig ⟨rhs, zero⟩
let aig := res.aig
let discr := res.ref
have := AIG.LawfulOperator.le_size (f := BVPred.mkEq) ..
let falseRef := falseRef.cast this
let trueRef := trueRef.cast this
let zero := zero.cast this
let lhs := lhs.cast this
let rhs := rhs.cast this
let res := blastUdiv.go aig w falseRef trueRef lhs rhs w 0 zero zero
let res := blastUdiv.go aig w lhs rhs w 0 zero zero
let aig := res.aig
let divRes := res.q
have := blastUdiv.go_le_size ..
@ -301,38 +278,17 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastUdiv where
unfold blastUdiv
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := BVPred.mkEq)
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.le_size (f := blastConst)
apply AIG.LawfulOperator.le_size (f := BVPred.mkEq)
decl_eq := by
intros
unfold blastUdiv
rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
rw [blastUdiv.go_decl_eq]
rw [AIG.LawfulOperator.decl_eq (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
end bitblast

11
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
View file

@ -25,13 +25,10 @@ def mkUlt (aig : AIG α) (pair : AIG.BinaryRefVec aig w) : AIG.Entrypoint α :=
let res := BVExpr.bitblast.blastNot aig rhsRefs
let aig := res.aig
let rhsNotRefs := res.vec
let res := aig.mkConstCached true
let trueRef := aig.mkConstCached true
let aig := res.aig
let trueRef := res.ref
let lhsRefs := lhsRefs.cast <| by
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast.blastNot)
let rhsNotRefs := rhsNotRefs.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let res := BVExpr.bitblast.mkOverflowBit aig ⟨_, ⟨lhsRefs, rhsNotRefs⟩, trueRef⟩
let aig := res.aig
let overflowRef := res.ref
@ -44,7 +41,6 @@ instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkUlt where
dsimp only
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkNotCached)
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := BVExpr.bitblast.mkOverflowBit)
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast.blastNot)
decl_eq := by
intros
@ -52,15 +48,10 @@ instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkUlt where
dsimp only
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkNotCached)]
rw [AIG.LawfulOperator.decl_eq (f := BVExpr.bitblast.mkOverflowBit)]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast.blastNot)]
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast.blastNot)
assumption
· apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast.blastNot)
assumption
· apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast.mkOverflowBit)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast.blastNot)
assumption

48
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean
View file

@ -22,39 +22,18 @@ namespace bitblast
variable [Hashable α] [DecidableEq α]
def blastUmod (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
let res := blastConst aig 0#w
let aig := res.aig
let zero := res.vec
let input := input.cast <| AIG.LawfulVecOperator.le_size (f := blastConst) ..
let res := aig.mkConstCached false
let aig := res.aig
let falseRef := res.ref
have := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let zero := zero.cast this
let input := input.cast this
let res := aig.mkConstCached true
let aig := res.aig
let trueRef := res.ref
have := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let falseRef := falseRef.cast this
let zero := zero.cast this
let input := input.cast this
let zero := blastConst aig 0#w
let ⟨lhs, rhs⟩ := input
let res := BVPred.mkEq aig ⟨rhs, zero⟩
let aig := res.aig
let discr := res.ref
have := AIG.LawfulOperator.le_size (f := BVPred.mkEq) ..
let falseRef := falseRef.cast this
let trueRef := trueRef.cast this
let zero := zero.cast this
let lhs := lhs.cast this
let rhs := rhs.cast this
let res := blastUdiv.go aig w falseRef trueRef lhs rhs w 0 zero zero
let res := blastUdiv.go aig w lhs rhs w 0 zero zero
let aig := res.aig
let modRes := res.r
have := blastUdiv.go_le_size ..
@ -69,38 +48,17 @@ instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastUmod where
unfold blastUmod
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := BVPred.mkEq)
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.le_size (f := blastConst)
apply AIG.LawfulOperator.le_size (f := BVPred.mkEq)
decl_eq := by
intros
unfold blastUmod
rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
rw [blastUdiv.go_decl_eq]
rw [AIG.LawfulOperator.decl_eq (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
· refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastConst)
assumption
end bitblast

16
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
View file

@ -34,12 +34,7 @@ where
let s := s.push (input.get curr hcurr2)
go aig w input newWidth (curr + 1) (by omega) s
else
let res := aig.mkConstCached false
let aig := res.aig
let zeroRef := res.ref
have hcast := AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
let input := input.cast hcast
let s := s.cast hcast
let zeroRef := aig.mkConstCached false
let s := s.push zeroRef
go aig w input newWidth (curr + 1) (by omega) s
else
@ -56,10 +51,8 @@ theorem go_le_size (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth
split
· dsimp only
split
· refine Nat.le_trans ?_ (by apply go_le_size)
omega
· refine Nat.le_trans ?_ (by apply go_le_size)
apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
· apply go_le_size
· apply go_le_size
· simp
termination_by newWidth - curr
@ -78,9 +71,6 @@ theorem go_decl_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth
· rw [← hgo]
intro idx h1 h2
rw [go_decl_eq]
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
assumption
· simp [← hgo]
termination_by newWidth - curr

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

@ -57,11 +57,7 @@ def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return ai
-/
let ⟨⟨⟨aig, refs⟩, hrefs⟩, cache⟩ := BVExpr.bitblast aig ⟨expr, cache⟩
let res := blastGetLsbD aig ⟨refs, idx⟩
let cache := cache.cast (AIG.LawfulOperator.le_size (f := blastGetLsbD) ..)
have := by
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsbD)
exact hrefs
⟨⟨res, this⟩, cache⟩
⟨⟨⟨aig, res⟩, hrefs⟩, cache⟩
theorem bitblast_decl_eq (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
@ -93,10 +89,7 @@ theorem bitblast_decl_eq (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig)
assumption
| getLsbD expr idx =>
simp only [bitblast]
rw [AIG.LawfulOperator.decl_eq (f := blastGetLsbD)]
rw [BVExpr.bitblast_decl_eq]
apply BVExpr.bitblast_lt_size_of_lt_aig_size
assumption
theorem bitblast_le_size (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size := by

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

@ -28,8 +28,7 @@ where
match expr with
| .literal var => BVPred.bitblast aig ⟨var, cache⟩
| .const val =>
have := LawfulOperator.le_size (f := mkConstCached) ..
⟨⟨aig.mkConstCached val, this⟩, cache.cast this⟩
⟨⟨⟨aig, aig.mkConstCached val⟩, by simp⟩, cache⟩
| .not expr =>
let ⟨⟨⟨aig, exprRef⟩, hexpr⟩, cache⟩ := go aig expr cache
let ret := aig.mkNotCached exprRef
@ -120,9 +119,7 @@ theorem go_lt_size_of_lt_aig_size (aig : AIG BVBit) (expr : BVLogicalExpr)
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)]
| const => simp [go]
| literal =>
simp only [go]
rw [BVPred.bitblast_decl_eq]

4
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
View file

@ -31,8 +31,8 @@ theorem go_Inv_of_Inv (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.
| const =>
simp only [go]
apply BVExpr.Cache.Inv_cast
apply LawfulOperator.isPrefix_aig (f := mkConstCached)
exact hinv
· apply IsPrefix.rfl
· exact hinv
| literal =>
simp only [go]
apply BVPred.bitblast_Inv_of_Inv

42
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
View file

@ -29,7 +29,7 @@ theorem go_get_aux (aig : AIG α) (c : BitVec w) (curr : Nat) (hcurr : curr ≤
-- `generalize` would produce a type incorrect term as the proof term would talk about
-- a `go` application instead of the fresh variable.
∀ (idx : Nat) (hidx : idx < curr) (hfoo),
(go aig c curr s hcurr).vec.get idx (by omega) = (s.get idx hidx).cast hfoo := by
(go aig c curr s hcurr).get idx (by omega) = (s.get idx hidx).cast hfoo := by
intro idx hidx
generalize hgo : go aig c curr s hcurr = res
unfold go at hgo
@ -39,11 +39,6 @@ theorem go_get_aux (aig : AIG α) (c : BitVec w) (curr : Nat) (hcurr : curr ≤
intro hfoo
rw [go_get_aux]
rw [AIG.RefVec.get_push_ref_lt]
· simp only [Ref.cast, Ref.mk.injEq]
rw [AIG.RefVec.get_cast]
· simp
· assumption
· apply go_le_size
· dsimp only at hgo
rw [← hgo]
simp only [Nat.le_refl, get, Ref.gate_cast, Ref.mk.injEq, true_implies]
@ -54,38 +49,17 @@ termination_by w - curr
theorem go_get (aig : AIG α) (c : BitVec w)
(curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
∀ (idx : Nat) (hidx : idx < curr),
(go aig c curr s hcurr).vec.get idx (by omega)
=
(s.get idx hidx).cast (by apply go_le_size) := by
(go aig c curr s hcurr).get idx (by omega) = s.get idx hidx := by
intros
apply go_get_aux
theorem go_denote_mem_prefix (aig : AIG α) (idx : Nat) (hidx)
(s : AIG.RefVec aig idx) (c : BitVec w) (start : Nat) (hstart) :
⟦
(go aig c idx s hidx).aig,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
=
⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
apply IsPrefix.of
· intros
apply go_decl_eq
· intros
apply go_le_size
simp
theorem go_denote_eq (aig : AIG α) (c : BitVec w) (assign : α → Bool)
(curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
∀ (idx : Nat) (hidx1 : idx < w),
curr ≤ idx
→
⟦
(go aig c curr s hcurr).aig,
(go aig c curr s hcurr).vec.get idx hidx1,
assign
⟧
⟦aig, (go aig c curr s hcurr).get idx hidx1, assign⟧
=
c.getLsbD idx := by
intro idx hidx1 hidx2
@ -99,9 +73,7 @@ theorem go_denote_eq (aig : AIG α) (c : BitVec w) (assign : α → Bool)
rw [go_get]
rw [AIG.RefVec.get_push_ref_eq']
· rw [← heq]
rw [go_denote_mem_prefix]
· simp
· simp [Ref.hgate]
simp
· rw [heq]
| inr =>
rw [← hgo]
@ -115,9 +87,7 @@ end blastConst
@[simp]
theorem denote_blastConst (aig : AIG α) (c : BitVec w) (assign : α → Bool) :
∀ (idx : Nat) (hidx : idx < w),
⟦(blastConst aig c).aig, (blastConst aig c).vec.get idx hidx, assign⟧
=
c.getLsbD idx := by
⟦aig, (blastConst aig c).get idx hidx, assign⟧ = c.getLsbD idx := by
intros
apply blastConst.go_denote_eq
omega

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
View file

@ -195,7 +195,7 @@ theorem go_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) :
· exact hinv
· rw [← hres]
apply Cache.Inv_cast
· apply LawfulVecOperator.isPrefix_aig (f := blastConst)
· apply IsPrefix.rfl
· exact hinv
· next op lhsExpr rhsExpr =>
dsimp only at hres

13
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
View file

@ -216,19 +216,10 @@ theorem denote_blast (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
unfold blast
dsimp only
rw [blastAdd.go_denote_eq _ 0 (by omega) _ _ _ _ assign lhs rhs _ _]
· simp only [BinaryRefVec.lhs_get_cast, Ref.cast_eq, BinaryRefVec.rhs_get_cast]
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
· simp
· simp
· omega
· intros
simp only [BinaryRefVec.lhs_get_cast, Ref.cast_eq]
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
rw [hleft]
· intros
simp only [BinaryRefVec.rhs_get_cast, Ref.cast_eq]
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
rw [hright]
· simp [hright]
· assumption
end blastAdd

16
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
View file

@ -24,11 +24,11 @@ variable [Hashable α] [DecidableEq α]
namespace blastExtract
theorem go_get_aux (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat)
(hcurr : curr ≤ newWidth) (falseRef : Ref aig) (s : RefVec aig curr) :
(hcurr : curr ≤ newWidth) (s : RefVec aig curr) :
∀ (idx : Nat) (hidx1 : idx < curr),
(go input lo falseRef curr hcurr s).get idx (by omega) = s.get idx hidx1 := by
(go input lo curr hcurr s).get idx (by omega) = s.get idx hidx1 := by
intro idx hidx
generalize hgo : go input lo falseRef curr hcurr s = res
generalize hgo : go input lo curr hcurr s = res
unfold go at hgo
split at hgo
· dsimp only at hgo
@ -44,12 +44,14 @@ theorem go_get_aux (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat)
termination_by newWidth - curr
theorem go_get (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat)
(hcurr : curr ≤ newWidth) (falseRef : Ref aig) (s : RefVec aig curr) :
(hcurr : curr ≤ newWidth) (s : RefVec aig curr) :
∀ (idx : Nat) (hidx1 : idx < newWidth),
curr ≤ idx → (go input lo falseRef curr hcurr s).get idx hidx1 = input.getD (lo + idx) falseRef
curr ≤ idx → (go input lo curr hcurr s).get idx hidx1
=
input.getD (lo + idx) (aig.mkConstCached false)
:= by
intro idx hidx1 hidx2
generalize hgo : go input lo falseRef curr hcurr s = res
generalize hgo : go input lo curr hcurr s = res
unfold go at hgo
dsimp only at hgo
split at hgo
@ -90,8 +92,6 @@ theorem denote_blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth)
· dsimp only
split
· rw [RefVec.get_in_bound]
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
congr 1
· rw [RefVec.get_out_bound]
· simp
· omega

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
View file

@ -36,7 +36,7 @@ theorem denote_getD_eq_getLsbD (aig : AIG α) (assign : α → Bool) (x : BitVec
@[simp]
theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) (assign : α → Bool) :
⟦blastGetLsbD aig target, assign⟧
⟦aig, blastGetLsbD aig target, assign⟧
=
if h : target.idx < target.w then
⟦aig, target.vec.get target.idx h, assign⟧

12
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
View file

@ -144,12 +144,10 @@ theorem denote_blast (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
· omega
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hleft]
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hright]
· simp [Ref.hgate]
· intro idx hidx
@ -161,18 +159,12 @@ theorem denote_blast (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
split
· next heq =>
rw [← hright] at heq
· rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [heq, hleft]
· simp [Ref.hgate]
· simp [Ref.hgate]
· simp [heq, hleft]
· omega
· next heq =>
simp only [Bool.not_eq_true] at heq
rw [← hright] at heq
· rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [heq]
· simp [Ref.hgate]
· simp [heq]
· omega

5
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
View file

@ -38,10 +38,7 @@ theorem denote_blastNeg (aig : AIG α) (value : BitVec w) (target : RefVec aig w
dsimp only
rw [denote_blastAdd]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
rw [denote_blastNot, htarget, BitVec.getLsbD_eq_getElem]
· simp [Ref.hgate]
simp [hidx, htarget]
· simp
end bitblast

11
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
View file

@ -40,11 +40,6 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
intros
rw [go_get_aux]
rw [AIG.RefVec.get_push_ref_lt]
· simp only [Ref.cast, Ref.mk.injEq]
rw [AIG.RefVec.get_cast]
· simp
· assumption
· apply go_le_size
· rw [← hgo]
intros
rw [go_get_aux]
@ -110,7 +105,8 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
rw [go_get]
rw [AIG.RefVec.get_push_ref_eq']
· rw [go_denote_mem_prefix]
· simp
· simp only [Ref.cast_eq]
rw [denote_mkConstCached]
· simp [Ref.hgate]
· rw [heq]
· omega
@ -134,8 +130,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
· next hidx =>
rw [← hgo]
rw [go_denote_eq]
· simp only [hidx, ↓reduceDIte, RefVec.get_cast, Ref.cast_eq]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp [hidx]
· omega
· split
· omega

8
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
View file

@ -44,11 +44,6 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
intros
rw [go_get_aux]
rw [AIG.RefVec.get_push_ref_lt]
· simp only [Ref.cast, Ref.mk.injEq]
rw [AIG.RefVec.get_cast]
· simp
· assumption
· apply go_le_size
· dsimp only at hgo
rw [← hgo]
simp only [Nat.le_refl, get, Ref.gate_cast, Ref.mk.injEq, true_implies]
@ -120,7 +115,8 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
rw [go_get]
rw [AIG.RefVec.get_push_ref_eq']
· rw [go_denote_mem_prefix]
· simp
· simp only [Ref.cast_eq]
rw [denote_mkConstCached]
· simp [Ref.hgate]
· rw [heq]
| inr =>

132
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
View file

@ -57,10 +57,10 @@ theorem denote_blastShiftConcat_eq_shiftConcat (aig : AIG α) (target : ShiftCon
simp [BitVec.getLsbD_shiftConcat, hidx, denote_blastShiftConcat, hx, hb, ← BitVec.getLsbD_eq_getElem]
theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α)
(n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :
⟦
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
(blastDivSubtractShift aig n d wn wr q r).aig,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastDivSubtractShift_le_size⟩,
assign
⟧
@ -74,19 +74,16 @@ theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) (falseRef trueRef
apply blastDivSubtractShift_le_size
theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
(falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
(n d : AIG.RefVec aig w) (wn wr : Nat)
(q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
(hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
(hfalse : ⟦aig, falseRef, assign⟧ = false)
(htrue : ⟦aig, trueRef, assign⟧ = true)
:
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx) :
∀ (idx : Nat) (hidx : idx < w),
⟦
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q.get idx hidx,
(blastDivSubtractShift aig n d wn wr q r).aig,
(blastDivSubtractShift aig n d wn wr q r).q.get idx hidx,
assign
⟧
=
@ -113,7 +110,7 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
· simp [hr]
· rw [BVPred.denote_getD_eq_getLsbD]
· simp [hleft]
· simp [hfalse]
· simp
· intro idx hidx
simp only [RefVec.get_cast, Ref.cast_eq]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
@ -132,9 +129,7 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hq]
· simp [Ref.hgate]
· rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hfalse]
· simp [Ref.hgate]
· rw [denote_mkConstCached]
· intro h
simp only [RefVec.get_cast, Ref.cast_eq]
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
@ -145,24 +140,20 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [hq]
· simp [Ref.hgate]
· rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
· simp [htrue]
· simp [Ref.hgate]
· rw [denote_mkConstCached]
. simp [Ref.hgate]
theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
(falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
(n d : AIG.RefVec aig w) (wn wr : Nat)
(q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
(hfalse : ⟦aig, falseRef, assign⟧ = false)
:
∀ (idx : Nat) (hidx : idx < w),
⟦
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r.get idx hidx,
(blastDivSubtractShift aig n d wn wr q r).aig,
(blastDivSubtractShift aig n d wn wr q r).r.get idx hidx,
assign
⟧
=
@ -185,7 +176,7 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
simp [hr]
· rw [BVPred.denote_getD_eq_getLsbD]
· exact hleft
· exact hfalse
· simp
· next hdiscr =>
rw [← Normalize.BitVec.lt_ult] at hdiscr
simp only [Ref.cast_eq, id_eq, Int.reduceNeg, hdiscr, ↓reduceIte]
@ -200,7 +191,7 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
· simp [hr]
· rw [BVPred.denote_getD_eq_getLsbD]
· exact hleft
· exact hfalse
· simp
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
@ -217,7 +208,7 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
. dsimp only
rw [BVPred.denote_getD_eq_getLsbD]
· exact hleft
· exact hfalse
· simp
. simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
@ -229,10 +220,10 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
@[simp]
theorem denote_blastDivSubtractShift_wn (aig : AIG α) (lhs rhs : BitVec w)
(falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
(n d : AIG.RefVec aig w) (wn wr : Nat)
(q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
:
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
(blastDivSubtractShift aig n d wn wr q r).wn
=
(BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wn := by
unfold blastDivSubtractShift BitVec.divSubtractShift
@ -241,10 +232,10 @@ theorem denote_blastDivSubtractShift_wn (aig : AIG α) (lhs rhs : BitVec w)
@[simp]
theorem denote_blastDivSubtractShift_wr (aig : AIG α) (lhs rhs : BitVec w)
(falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
(n d : AIG.RefVec aig w) (wn wr : Nat)
(q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
:
(blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
(blastDivSubtractShift aig n d wn wr q r).wr
=
(BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wr := by
unfold blastDivSubtractShift BitVec.divSubtractShift
@ -252,18 +243,16 @@ theorem denote_blastDivSubtractShift_wr (aig : AIG α) (lhs rhs : BitVec w)
split <;> simp
theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat) (lhs rhs rbv qbv : BitVec w)
(falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w) (wn wr : Nat)
(n d q r : AIG.RefVec aig w) (wn wr : Nat)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
(hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
(hfalse : ⟦aig, falseRef, assign⟧ = false)
(htrue : ⟦aig, trueRef, assign⟧ = true)
:
∀ (idx : Nat) (hidx : idx < w),
⟦
(go aig curr falseRef trueRef n d wn wr q r).aig,
(go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx,
(go aig curr n d wn wr q r).aig,
(go aig curr n d wn wr q r).q.get idx hidx,
assign
⟧
=
@ -295,8 +284,6 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat)
· exact hright
· exact hq
· exact hr
· exact hfalse
· exact htrue
· intro idx hidx
rw [denote_blastDivSubtractShift_r (rbv := rbv) (qbv := qbv) (lhs := lhs) (rhs := rhs)]
· rw [BitVec.divSubtractShift]
@ -304,13 +291,6 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat)
· exact hleft
· exact hright
· exact hr
· exact hfalse
· rw [blastDivSubtractShift_denote_mem_prefix]
· simp [hfalse]
· simp [Ref.hgate]
· rw [blastDivSubtractShift_denote_mem_prefix]
· simp [htrue]
· simp [Ref.hgate]
· next hdiscr =>
rw [ih]
· rfl
@ -330,8 +310,6 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat)
· exact hright
· exact hq
· exact hr
· exact hfalse
· exact htrue
· intro idx hidx
rw [denote_blastDivSubtractShift_r (rbv := rbv) (qbv := qbv) (lhs := lhs) (rhs := rhs)]
· rw [BitVec.divSubtractShift]
@ -339,28 +317,19 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat)
· exact hleft
· exact hright
· exact hr
· exact hfalse
· rw [blastDivSubtractShift_denote_mem_prefix]
· simp [hfalse]
· simp [Ref.hgate]
· rw [blastDivSubtractShift_denote_mem_prefix]
· simp [htrue]
· simp [Ref.hgate]
theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
(falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w)
(n d q r : AIG.RefVec aig w)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
(hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = false)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = false)
(hfalse : ⟦aig, falseRef, assign⟧ = false)
(htrue : ⟦aig, trueRef, assign⟧ = true)
(hzero : 0#w < rhs)
:
∀ (idx : Nat) (hidx : idx < w),
⟦
(go aig w falseRef trueRef n d w 0 q r).aig,
(go aig w falseRef trueRef n d w 0 q r).q.get idx hidx,
(go aig w n d w 0 q r).aig,
(go aig w n d w 0 q r).q.get idx hidx,
assign
⟧
=
@ -373,13 +342,11 @@ theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
· exact hright
· simp [hq]
· simp [hr]
· exact hfalse
· exact htrue
theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG.Ref aig)
theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat)
(n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :
⟦
(go aig curr falseRef trueRef n d wn wr q r).aig,
(go aig curr n d wn wr q r).aig,
⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
assign
⟧
@ -414,23 +381,12 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
rw [hdiscr]
rw [blastUdiv.go_denote_mem_prefix]
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [denote_blastConst]
simp
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hright]
· simp [Ref.hgate]
simp [hright]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
rw [denote_blastConst]
simp
· simp [Ref.hgate]
simp
· next hdiscr =>
rw [blastUdiv.go_denote_mem_prefix] at hdiscr
rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr
@ -440,54 +396,28 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
rw [blastUdiv.denote_go (hzero := hzero)]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hleft]
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hright]
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq]
rw [denote_blastConst]
simp
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq]
rw [denote_blastConst]
simp
· simp [Ref.hgate]
· rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp
· simp [Ref.hgate]
· rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
· simp
· simp [Ref.hgate]
· intro idx hdix
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hright]
· simp [Ref.hgate]
simp [hright]
· intro idx hdix
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
rw [denote_blastConst]
simp
· simp [Ref.hgate]
simp
end bitblast
end BVExpr

7
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
View file

@ -35,15 +35,12 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
· simp
· dsimp only
intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot)]
apply hleft
· dsimp only
intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
rw [BVExpr.bitblast.denote_blastNot, hright, BitVec.getLsbD_eq_getElem]
· simp [Ref.hgate]
simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
rw [BVExpr.bitblast.denote_blastNot, hright, BitVec.getLsbD_eq_getElem]
end BVPred

84
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
View file

@ -26,18 +26,16 @@ namespace blastUmod
open blastUdiv
theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat) (lhs rhs rbv qbv : BitVec w)
(falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w) (wn wr : Nat)
(n d q r : AIG.RefVec aig w) (wn wr : Nat)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
(hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
(hfalse : ⟦aig, falseRef, assign⟧ = false)
(htrue : ⟦aig, trueRef, assign⟧ = true)
:
∀ (idx : Nat) (hidx : idx < w),
⟦
(go aig curr falseRef trueRef n d wn wr q r).aig,
(go aig curr falseRef trueRef n d wn wr q r).r.get idx hidx,
(go aig curr n d wn wr q r).aig,
(go aig curr n d wn wr q r).r.get idx hidx,
assign
⟧
=
@ -69,8 +67,6 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat)
· exact hright
· exact hq
· exact hr
· exact hfalse
· exact htrue
· intro idx hidx
rw [denote_blastDivSubtractShift_r (rbv := rbv) (qbv := qbv) (lhs := lhs) (rhs := rhs)]
· rw [BitVec.divSubtractShift]
@ -78,13 +74,6 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat)
· exact hleft
· exact hright
· exact hr
· exact hfalse
· rw [blastDivSubtractShift_denote_mem_prefix]
· simp [hfalse]
· simp [Ref.hgate]
· rw [blastDivSubtractShift_denote_mem_prefix]
· simp [htrue]
· simp [Ref.hgate]
· next hdiscr =>
rw [ih]
· rfl
@ -104,8 +93,6 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat)
· exact hright
· exact hq
· exact hr
· exact hfalse
· exact htrue
· intro idx hidx
rw [denote_blastDivSubtractShift_r (rbv := rbv) (qbv := qbv) (lhs := lhs) (rhs := rhs)]
· rw [BitVec.divSubtractShift]
@ -113,28 +100,19 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat)
· exact hleft
· exact hright
· exact hr
· exact hfalse
· rw [blastDivSubtractShift_denote_mem_prefix]
· simp [hfalse]
· simp [Ref.hgate]
· rw [blastDivSubtractShift_denote_mem_prefix]
· simp [htrue]
· simp [Ref.hgate]
theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
(falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w)
(n d q r : AIG.RefVec aig w)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
(hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = false)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = false)
(hfalse : ⟦aig, falseRef, assign⟧ = false)
(htrue : ⟦aig, trueRef, assign⟧ = true)
(hzero : 0#w < rhs)
:
∀ (idx : Nat) (hidx : idx < w),
⟦
(go aig w falseRef trueRef n d w 0 q r).aig,
(go aig w falseRef trueRef n d w 0 q r).r.get idx hidx,
(go aig w n d w 0 q r).aig,
(go aig w n d w 0 q r).r.get idx hidx,
assign
⟧
=
@ -147,8 +125,6 @@ theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
· exact hright
· simp [hq]
· simp [hr]
· exact hfalse
· exact htrue
end blastUmod
@ -172,24 +148,14 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
rw [hdiscr]
rw [blastUdiv.go_denote_mem_prefix]
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hleft]
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hright]
· simp [Ref.hgate]
simp [hright]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
rw [denote_blastConst]
simp
· simp [Ref.hgate]
simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
rw [denote_blastConst]
simp
· next hdiscr =>
rw [blastUdiv.go_denote_mem_prefix] at hdiscr
rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr
@ -199,54 +165,28 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
rw [blastUmod.denote_go (hzero := hzero)]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hleft]
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hright]
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq]
rw [denote_blastConst]
simp
· simp [Ref.hgate]
· intro idx hidx
rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq]
rw [denote_blastConst]
simp
· simp [Ref.hgate]
· rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp
· simp [Ref.hgate]
· rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
· simp
· simp [Ref.hgate]
· intro idx hdix
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
· simp [hright]
· simp [Ref.hgate]
simp [hright]
· intro idx hdix
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
· simp only [RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_zero]
rw [denote_blastConst]
simp
· simp [Ref.hgate]
simp
end bitblast
end BVExpr

13
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
View file

@ -43,11 +43,6 @@ theorem go_get_aux (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth
intros
rw [go_get_aux]
rw [AIG.RefVec.get_push_ref_lt]
· simp only [Ref.cast, Ref.mk.injEq]
rw [AIG.RefVec.get_cast]
· simp
· assumption
· apply go_le_size
· dsimp only at hgo
rw [← hgo]
simp only [Nat.le_refl, get, Ref.gate_cast, Ref.mk.injEq, true_implies]
@ -122,7 +117,8 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid
rw [go_get]
rw [AIG.RefVec.get_push_ref_eq']
· rw [go_denote_mem_prefix]
· simp [heq]
· simp only [Ref.cast_eq]
rw [denote_mkConstCached]
· simp [Ref.hgate]
· omega
| inr =>
@ -132,10 +128,7 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid
omega
· rw [← hgo]
rw [go_denote_eq]
· split
· omega
· rfl
· omega
omega
· omega
termination_by newWidth - curr

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
View file

@ -64,7 +64,7 @@ theorem bitblast_Inv_of_Inv (input : BVExpr.WithCache BVPred aig)
exact hinv
· dsimp only
apply BVExpr.Cache.Inv_cast
· apply AIG.LawfulOperator.isPrefix_aig (f := blastGetLsbD)
· apply IsPrefix.rfl
· apply BVExpr.bitblast_Inv_of_Inv
exact hinv