The charged dependency graph

The predicates in this module describe the circuit graph after contracting zero-cost gates. A charged gate reads an input or another charged gate when one of its raw argument wires has that charged origin.

def Algebraic.DeMorgan.ChargedGate {n g : ℕ} (program : Program signature n g) (gate : Fin g) : Prop

An internal gate is charged exactly when it is an AND or OR gate.

Equations

• Algebraic.DeMorgan.ChargedGate program gate = (Algebraic.DeMorgan.binaryCost (program.lines gate).op = 1)

def Algebraic.DeMorgan.ReadsInput {n g : ℕ} (program : Program signature n g) (gate : Fin g) (input : Fin n) : Prop

A charged internal gate reads an original input through only free gates.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.DeMorgan.ReadsOnlyInput {n g : ℕ} (program : Program signature n g) (gate : Fin g) (input : Fin n) : Prop

Every argument of a charged gate contracts to a literal of one input.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.DeMorgan.UsesGate {n g : ℕ} (program : Program signature n g) (source target : Fin g) : Prop

One charged internal gate feeds another through only free gates.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.DeMorgan.SimpleOrigin {n g : ℕ} : ResidualValue n g → Prop

A contracted origin is simple when it is a constant or a signed input.

Equations

• Algebraic.DeMorgan.SimpleOrigin (Algebraic.DeMorgan.ResidualValue.constant value) = True
• Algebraic.DeMorgan.SimpleOrigin (Algebraic.DeMorgan.ResidualValue.wire negated wire) = ∃ (input : Fin n), wire = Cslib.Circuits.Wire.input input

theorem Algebraic.DeMorgan.SimpleOrigin.map_castSucc {n g : ℕ} {value : ResidualValue n g} (simple : SimpleOrigin value) : SimpleOrigin (ResidualValue.mapWires Wire.Renaming.castSucc.apply value)

Simplicity is preserved when a program is extended by one gate.

theorem Algebraic.DeMorgan.SimpleOrigin.ne_gate {n g : ℕ} {value : ResidualValue n g} (simple : SimpleOrigin value) (negated : Bool) (gate : Fin g) : value ≠ ResidualValue.wire negated (Wire.gate gate)

A simple origin cannot be the output of a charged gate.

structure Algebraic.DeMorgan.InitialChargedGate {n g : ℕ} (program : Program signature n g) : Type

An initial charged gate, presented with its two named arguments. Its arguments have no charged predecessors after contracting the free gates.

• gate : Fin g

  The selected gate.

• op : BinaryOp

  Its binary operation.

• left : Wire n g

  Its left input wire.

• right : Wire n g

  Its right input wire.

• line_eq : program.lines self.gate = binaryLine self.op self.left self.right

  The widened program line has the claimed binary presentation.

• left_simple : SimpleOrigin (origins program self.left)

  The left contracted origin is a constant or literal.

• right_simple : SimpleOrigin (origins program self.right)

  The right contracted origin is a constant or literal.

theorem Algebraic.DeMorgan.InitialChargedGate.charged {inputCount✝ a✝ : ℕ} {program : Program signature inputCount✝ a✝} (initial : InitialChargedGate program) : ChargedGate program initial.gate

Every initial charged gate is charged in the weighted De Morgan model.

inductive Algebraic.DeMorgan.InitialGatePattern {n g : ℕ} {program : Program signature n g} (initial : InitialChargedGate program) : Type

The four structural possibilities for an initial charged gate.

• constantLeft {n g : ℕ} {program : Program signature n g} {initial : InitialChargedGate program} (value : Bool) : origins program initial.left = ResidualValue.constant value → InitialGatePattern initial
• constantRight {n g : ℕ} {program : Program signature n g} {initial : InitialChargedGate program} (value : Bool) : origins program initial.right = ResidualValue.constant value → InitialGatePattern initial
• singleInput {n g : ℕ} {program : Program signature n g} {initial : InitialChargedGate program} (input : Fin n) (leftNegated rightNegated : Bool) : origins program initial.left = ResidualValue.wire leftNegated (Wire.input input) → origins program initial.right = ResidualValue.wire rightNegated (Wire.input input) → InitialGatePattern initial
• distinctInputs {n g : ℕ} {program : Program signature n g} {initial : InitialChargedGate program} (leftInput rightInput : Fin n) (leftNegated rightNegated : Bool) : leftInput ≠ rightInput → origins program initial.left = ResidualValue.wire leftNegated (Wire.input leftInput) → origins program initial.right = ResidualValue.wire rightNegated (Wire.input rightInput) → InitialGatePattern initial

noncomputable def Algebraic.DeMorgan.InitialChargedGate.pattern {n g : ℕ} {program : Program signature n g} (initial : InitialChargedGate program) : InitialGatePattern initial

Classify the two simple origins of an initial charged gate.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.DeMorgan.InitialChargedGate.readsInput_left {n g : ℕ} {program : Program signature n g} (initial : InitialChargedGate program) {input : Fin n} {negated : Bool} (origin_eq : origins program initial.left = ResidualValue.wire negated (Wire.input input)) : ReadsInput program initial.gate input

The left literal of an initial gate gives a direct-input edge.

theorem Algebraic.DeMorgan.InitialChargedGate.readsInput_right {n g : ℕ} {program : Program signature n g} (initial : InitialChargedGate program) {input : Fin n} {negated : Bool} (origin_eq : origins program initial.right = ResidualValue.wire negated (Wire.input input)) : ReadsInput program initial.gate input

The right literal of an initial gate gives a direct-input edge.

theorem Algebraic.DeMorgan.InitialChargedGate.readsOnlyInput {n g : ℕ} {program : Program signature n g} (initial : InitialChargedGate program) {input : Fin n} {leftNegated rightNegated : Bool} (leftOrigin : origins program initial.left = ResidualValue.wire leftNegated (Wire.input input)) (rightOrigin : origins program initial.right = ResidualValue.wire rightNegated (Wire.input input)) : ReadsOnlyInput program initial.gate input

Two literals of the same input make an initial gate a single-input gate.

theorem Algebraic.DeMorgan.InitialChargedGate.not_uses {n g : ℕ} {program : Program signature n g} (initial : InitialChargedGate program) (source : Fin g) : ¬UsesGate program source initial.gate

No charged predecessor feeds an initial charged gate.

theorem Algebraic.DeMorgan.exists_initialChargedGate {n g : ℕ} (program : Program signature n g) (existsCharged : ∃ (gate : Fin g), ChargedGate program gate) : Nonempty (InitialChargedGate program)

Every nonempty collection of charged gates has an initial member.

@[simp]

theorem Algebraic.DeMorgan.chargedGate_gate_castSucc {n g : ℕ} (program : Program signature n g) (line : Line signature n g) (gate : Fin g) : ChargedGate (program.gate line) gate.castSucc ↔ ChargedGate program gate

theorem Algebraic.DeMorgan.ReadsInput.castSucc {n g : ℕ} {gate : Fin g} {input : Fin n} {program : Program signature n g} (reads : ReadsInput program gate input) (line : Line signature n g) : ReadsInput (program.gate line) gate.castSucc input

Extend a direct-input edge through an appended program gate.

theorem Algebraic.DeMorgan.ReadsInput.of_castSucc {n g : ℕ} {line : Line signature n g} {input : Fin n} {gate : Fin g} {program : Program signature n g} (reads : ReadsInput (program.gate line) gate.castSucc input) : ReadsInput program gate input

Reflect a direct-input edge from an appended program to its prefix.

theorem Algebraic.DeMorgan.ReadsInput.of_last {n g : ℕ} {input : Fin n} {program : Program signature n g} {line : Line signature n g} (reads : ReadsInput (program.gate line) (Fin.last g) input) : binaryCost line.op = 1 ∧ ∃ (argument : Fin (signature.Arity line.op)) (negated : Bool), origins program (line.wires argument) = ResidualValue.wire negated (Wire.input input)

Expose the prefix-level literal read by a charged newly-appended gate.

theorem Algebraic.DeMorgan.ReadsOnlyInput.of_castSucc {n g : ℕ} {line : Line signature n g} {input : Fin n} {gate : Fin g} {program : Program signature n g} (reads : ReadsOnlyInput (program.gate line) gate.castSucc input) : ReadsOnlyInput program gate input

Reflect a single-input charged gate from an appended program to its prefix.

theorem Algebraic.DeMorgan.ReadsOnlyInput.of_last {n g : ℕ} {input : Fin n} {program : Program signature n g} {line : Line signature n g} (reads : ReadsOnlyInput (program.gate line) (Fin.last g) input) : binaryCost line.op = 1 ∧ ∀ (argument : Fin (signature.Arity line.op)), ∃ (negated : Bool), origins program (line.wires argument) = ResidualValue.wire negated (Wire.input input)

Expose the prefix-level literals of a newly appended single-input gate.

theorem Algebraic.DeMorgan.ReadsInput.last {n g : ℕ} {program : Program signature n g} {line : Line signature n g} {input : Fin n} (charged : binaryCost line.op = 1) {argument : Fin (signature.Arity line.op)} {negated : Bool} (origin_eq : origins program (line.wires argument) = ResidualValue.wire negated (Wire.input input)) : ReadsInput (program.gate line) (Fin.last g) input

Build a direct-input edge into a newly appended charged gate.

theorem Algebraic.DeMorgan.UsesGate.castSucc {n g : ℕ} {source target : Fin g} {program : Program signature n g} (uses : UsesGate program source target) (line : Line signature n g) : UsesGate (program.gate line) source.castSucc target.castSucc

Extend a charged edge through an appended program gate.

theorem Algebraic.DeMorgan.UsesGate.of_castSucc {n g : ℕ} {line : Line signature n g} {source target : Fin g} {program : Program signature n g} (uses : UsesGate (program.gate line) source.castSucc target.castSucc) : UsesGate program source target

Reflect a charged edge from an appended program to its prefix.

theorem Algebraic.DeMorgan.UsesGate.last {n g : ℕ} {program : Program signature n g} {line : Line signature n g} {source : Fin g} (charged : binaryCost line.op = 1) {argument : Fin (signature.Arity line.op)} {negated : Bool} (origin_eq : origins program (line.wires argument) = ResidualValue.wire negated (Wire.gate source)) : UsesGate (program.gate line) source.castSucc (Fin.last g)

Build a charged edge into a newly appended charged gate.

theorem Algebraic.DeMorgan.UsesGate.ne {n g : ℕ} {program : Program signature n g} {source target : Fin g} (uses : UsesGate program source target) : source ≠ target

A charged dependency edge cannot be a self-loop.