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 decls2 : Array (Decl α)) : Prop

decls1 is a prefix of decls2

• of :: (
• size_le : decls1.size ≤ decls2.size

  The prefix may never be longer than the other array.

• idx_eq (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 decls2 : Array (Decl α)) (start : Nat) {hdag1 : IsDAG α decls1} {hdag2 : IsDAG α decls2} {hbounds1 : start < decls1.size} {hbounds2 : start < decls2.size} (hprefix : IsPrefix decls1 decls2) : go start decls2 assign hbounds2 hdag2 = 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 : Entrypoint α) (newAIG : AIG α) (hprefix : 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 : AIG α) : Type

Equations

• aig.ExtendingEntrypoint = { entry : Std.Sat.AIG.Entrypoint α // aig.decls.size ≤ entry.aig.decls.size }

@[reducible, inline]

abbrev Std.Sat.AIG.ExtendingRefVecEntry {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (len : Nat) : Type

Equations

• aig.ExtendingRefVecEntry len = { ref : Std.Sat.AIG.RefVecEntry α len // aig.decls.size ≤ ref.aig.decls.size }

class Std.Sat.AIG.LawfulOperator (α : Type) [Hashable α] [DecidableEq α] (β : AIG α → Type) (f : (aig : AIG α) → β aig → Entrypoint α) : Prop

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 : AIG α) (input : β aig) : aig.decls.size ≤ (f aig input).aig.decls.size
• decl_eq (aig : 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

• Std.Sat.AIG.RefVec.instLawfulOperatorFoldTargetFold
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkAndCached
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkBEqCached
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkImpCached
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkOrCached
• Std.Sat.AIG.instLawfulOperatorBinaryInputMkXorCached
• Std.Sat.AIG.instLawfulOperatorBoolMkConst
• Std.Sat.AIG.instLawfulOperatorBoolMkConstCached
• Std.Sat.AIG.instLawfulOperatorGateInputMkGate
• Std.Sat.AIG.instLawfulOperatorGateInputMkGateCached
• Std.Sat.AIG.instLawfulOperatorMkAtom
• Std.Sat.AIG.instLawfulOperatorMkAtomCached
• Std.Sat.AIG.instLawfulOperatorRefMkNotCached
• Std.Sat.AIG.instLawfulOperatorTernaryInputMkIfCached
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulOperatorFullAdderInputMkFullAdderCarry
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulOperatorFullAdderInputMkFullAdderOut
• Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.instLawfulOperatorOverflowInput
• Std.Tactic.BVDecide.BVPred.instLawfulOperatorBVBitBitblast
• Std.Tactic.BVDecide.BVPred.instLawfulOperatorBinaryRefVecMkEq
• Std.Tactic.BVDecide.BVPred.instLawfulOperatorBinaryRefVecMkUlt
• Std.Tactic.BVDecide.BVPred.instLawfulOperatorGetLsbDTargetBlastGetLsbD

theorem Std.Sat.AIG.LawfulOperator.isPrefix_aig {α : Type} [Hashable α] [DecidableEq α] {β : AIG α → Type} {f : (aig : AIG α) → β aig → Entrypoint α} [LawfulOperator α β f] (aig : AIG α) (input : β aig) : IsPrefix aig.decls (f aig input).aig.decls

theorem Std.Sat.AIG.LawfulOperator.lt_size {α : Type} [Hashable α] [DecidableEq α] {β : AIG α → Type} {f : (aig : AIG α) → β aig → Entrypoint α} [LawfulOperator α β f] (entry : 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 α] {β : AIG α → Type} {f : (aig : AIG α) → β aig → Entrypoint α} [LawfulOperator α β f] {x : Nat} (aig : 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 α] {β : AIG α → Type} {f : (aig : AIG α) → β aig → Entrypoint α} [LawfulOperator α β f] {x : Nat} (aig : 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 α] {β : AIG α → Type} {f : (aig : AIG α) → β aig → Entrypoint α} [LawfulOperator α β f] {assign : α → Bool} (entry : 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 α] {β : AIG α → Type} {f : (aig : AIG α) → β aig → Entrypoint α} [LawfulOperator α β f] {assign : α → Bool} (entry : 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 α] {β : AIG α → Type} {f : (aig : AIG α) → β aig → Entrypoint α} [LawfulOperator α β f] {assign : α → Bool} {start : Nat} {aig : 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 } }⟧