Documentation

Std.Sat.AIG.LawfulOperator

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.

    • 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

  • )
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]
    Equations
    Instances For
      @[reducible, inline]
      abbrev Std.Sat.AIG.ExtendingRefVecEntry {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (len : Nat) :
      Equations
      Instances For
        class Std.Sat.AIG.LawfulOperator (α : Type) [Hashable α] [DecidableEq α] (β : Std.Sat.AIG αType) (f : (aig : Std.Sat.AIG α) → β aigStd.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 α) → β aigStd.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 α) → β aigStd.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 α) → β aigStd.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 α) → β aigStd.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 α) → β aigStd.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 α) → β aigStd.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 α) → β aigStd.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 α) → β aigStd.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 α) → β aigStd.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 } }