The lawful operator framework provides free theorems around the typeclass LawfulOperator.
Its definition is based on section 3.3 of the AIGNET paper.
structure
Std.Sat.AIG.IsPrefix
{α : Type}
(decls1 : Array (Std.Sat.AIG.Decl α))
(decls2 : Array (Std.Sat.AIG.Decl α))
:
decls1 is a prefix of decls2
- of :: (
- size_le : decls1.size ≤ decls2.size
The prefix may never be longer than the other array.
The prefix and the other array must agree on all elements up until the bound of the prefix
- )
Instances For
theorem
Std.Sat.AIG.IsPrefix.size_le
{α : Type}
{decls1 : Array (Std.Sat.AIG.Decl α)}
{decls2 : Array (Std.Sat.AIG.Decl α)}
(self : Std.Sat.AIG.IsPrefix decls1 decls2)
:
decls1.size ≤ decls2.size
The prefix may never be longer than the other array.
theorem
Std.Sat.AIG.IsPrefix.idx_eq
{α : Type}
{decls1 : Array (Std.Sat.AIG.Decl α)}
{decls2 : Array (Std.Sat.AIG.Decl α)}
(self : Std.Sat.AIG.IsPrefix decls1 decls2)
(idx : Nat)
(h : idx < decls1.size)
:
decls2[idx] = decls1[idx]
The prefix and the other array must agree on all elements up until the bound of the prefix
@[irreducible]
theorem
Std.Sat.AIG.denote.go_eq_of_isPrefix
{α : Type}
{assign : α → Bool}
(decls1 : Array (Std.Sat.AIG.Decl α))
(decls2 : Array (Std.Sat.AIG.Decl α))
(start : Nat)
{hdag1 : Std.Sat.AIG.IsDAG α decls1}
{hdag2 : Std.Sat.AIG.IsDAG α decls2}
{hbounds1 : start < decls1.size}
{hbounds2 : start < decls2.size}
(hprefix : Std.Sat.AIG.IsPrefix decls1 decls2)
:
Std.Sat.AIG.denote.go start decls2 assign hbounds2 hdag2 = Std.Sat.AIG.denote.go start decls1 assign hbounds1 hdag1
If decls1 is a prefix of decls2 and we start evaluating decls2 at an
index in bounds of decls1 we can evaluate at decls1.
theorem
Std.Sat.AIG.denote.eq_of_isPrefix
{α : Type}
[Hashable α]
[DecidableEq α]
{assign : α → Bool}
(entry : Std.Sat.AIG.Entrypoint α)
(newAIG : Std.Sat.AIG α)
(hprefix : Std.Sat.AIG.IsPrefix entry.aig.decls newAIG.decls)
:
⟦assign, { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = ⟦assign, entry⟧
If decls1 is a prefix of decls2 and we start evaluating decls2 at an
index in bounds of decls1 we can evaluate at decls1.
@[reducible, inline]
abbrev
Std.Sat.AIG.ExtendingEntrypoint
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Std.Sat.AIG α)
:
Equations
- aig.ExtendingEntrypoint = { entry : Std.Sat.AIG.Entrypoint α // aig.decls.size ≤ entry.aig.decls.size }
Instances For
@[reducible, inline]
abbrev
Std.Sat.AIG.ExtendingRefVecEntry
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Std.Sat.AIG α)
(len : Nat)
:
Equations
- aig.ExtendingRefVecEntry len = { ref : Std.Sat.AIG.RefVecEntry α len // aig.decls.size ≤ ref.aig.decls.size }
Instances For
class
Std.Sat.AIG.LawfulOperator
(α : Type)
[Hashable α]
[DecidableEq α]
(β : Std.Sat.AIG α → Type)
(f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α)
:
A function f that takes some aig : AIG α and an argument of type β aig is called a lawful
AIG operator if it only extends the AIG but never modifies already existing nodes.
This guarantees that applying such a function will not change the semantics of any existing parts of the circuit, allowing us to perform local reasoning on the AIG.
- le_size : ∀ (aig : Std.Sat.AIG α) (input : β aig), aig.decls.size ≤ (f aig input).aig.decls.size
- decl_eq : ∀ (aig : Std.Sat.AIG α) (input : β aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (f aig input).aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]
Instances
theorem
Std.Sat.AIG.LawfulOperator.le_size
{α : Type}
:
∀ {inst : Hashable α} {inst_1 : DecidableEq α} {β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [self : Std.Sat.AIG.LawfulOperator α β f]
(aig : Std.Sat.AIG α) (input : β aig), aig.decls.size ≤ (f aig input).aig.decls.size
theorem
Std.Sat.AIG.LawfulOperator.decl_eq
{α : Type}
:
∀ {inst : Hashable α} {inst_1 : DecidableEq α} {β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [self : Std.Sat.AIG.LawfulOperator α β f]
(aig : Std.Sat.AIG α) (input : β aig) (idx : Nat) (h1 : idx < aig.decls.size)
(h2 : idx < (f aig input).aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]
theorem
Std.Sat.AIG.LawfulOperator.isPrefix_aig
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α}
[Std.Sat.AIG.LawfulOperator α β f]
(aig : Std.Sat.AIG α)
(input : β aig)
:
Std.Sat.AIG.IsPrefix aig.decls (f aig input).aig.decls
theorem
Std.Sat.AIG.LawfulOperator.lt_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α}
[Std.Sat.AIG.LawfulOperator α β f]
(entry : Std.Sat.AIG.Entrypoint α)
(input : β entry.aig)
:
entry.ref.gate < (f entry.aig input).aig.decls.size
theorem
Std.Sat.AIG.LawfulOperator.lt_size_of_lt_aig_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α}
[Std.Sat.AIG.LawfulOperator α β f]
{x : Nat}
(aig : Std.Sat.AIG α)
(input : β aig)
(h : x < aig.decls.size)
:
x < (f aig input).aig.decls.size
theorem
Std.Sat.AIG.LawfulOperator.le_size_of_le_aig_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α}
[Std.Sat.AIG.LawfulOperator α β f]
{x : Nat}
(aig : Std.Sat.AIG α)
(input : β aig)
(h : x ≤ aig.decls.size)
:
x ≤ (f aig input).aig.decls.size
@[simp]
theorem
Std.Sat.AIG.LawfulOperator.denote_input_entry
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α}
[Std.Sat.AIG.LawfulOperator α β f]
{assign : α → Bool}
(entry : Std.Sat.AIG.Entrypoint α)
{input : β entry.aig}
{h : entry.ref.gate < (f entry.aig input).aig.decls.size}
:
⟦assign, { aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, hgate := h } }⟧ = ⟦assign, entry⟧
@[simp]
theorem
Std.Sat.AIG.LawfulOperator.denote_cast_entry
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α}
[Std.Sat.AIG.LawfulOperator α β f]
{assign : α → Bool}
(entry : Std.Sat.AIG.Entrypoint α)
{input : β entry.aig}
{h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size}
:
⟦assign, { aig := (f entry.aig input).aig, ref := entry.ref.cast h }⟧ = ⟦assign, entry⟧
theorem
Std.Sat.AIG.LawfulOperator.denote_mem_prefix
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Type}
{f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α}
[Std.Sat.AIG.LawfulOperator α β f]
{assign : α → Bool}
{start : Nat}
{aig : Std.Sat.AIG α}
{input : β aig}
(h : start < aig.decls.size)
:
⟦assign, { aig := (f aig input).aig, ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, hgate := h } }⟧