Zero-cost De Morgan wiring

A wiring specification selects an existing Boolean input or a hardwired constant for each output. The type excludes charged logical operations, so every compiled specification has zero standard De Morgan cost.

inductive Algebraic.DeMorgan.Wiring (inputs : ℕ) : Type

One output of a pure wiring layer.

• input {inputs : ℕ} (index : Fin inputs) : Wiring inputs
• constant {inputs : ℕ} (value : Bool) : Wiring inputs

def Algebraic.DeMorgan.Wiring.eval {inputs : ℕ} (input : Fin inputs → Bool) : Wiring inputs → Bool

Interpret a wiring source against a concrete input assignment.

Equations

• Algebraic.DeMorgan.Wiring.eval input (Algebraic.DeMorgan.Wiring.input index) = input index
• Algebraic.DeMorgan.Wiring.eval input (Algebraic.DeMorgan.Wiring.constant value) = value

@[simp]

theorem Algebraic.DeMorgan.Wiring.eval_input {inputs : ℕ} (input : Fin inputs → Bool) (index : Fin inputs) : eval input (Wiring.input index) = input index

@[simp]

theorem Algebraic.DeMorgan.Wiring.eval_constant {inputs : ℕ} (input : Fin inputs → Bool) (value : Bool) : eval input (constant value) = value

def Algebraic.DeMorgan.Wiring.expression {inputs : ℕ} : Wiring inputs → Expression inputs

Compile a wiring source to its zero-cost De Morgan expression.

Equations

• (Algebraic.DeMorgan.Wiring.input index).expression = Algebraic.DeMorgan.Expression.input index
• (Algebraic.DeMorgan.Wiring.constant value).expression = Algebraic.DeMorgan.Expression.constant value

@[simp]

theorem Algebraic.DeMorgan.Wiring.expression_eval {inputs : ℕ} (source : Wiring inputs) (input : Fin inputs → Bool) : Expression.eval input source.expression = eval input source

@[simp]

theorem Algebraic.DeMorgan.Wiring.expression_standardCost {inputs : ℕ} (source : Wiring inputs) : source.expression.standardCost = 0

theorem Algebraic.DeMorgan.Wiring.eval_finAppend {leftCount inputs rightCount : ℕ} (left : Fin leftCount → Wiring inputs) (right : Fin rightCount → Wiring inputs) (input : Fin inputs → Bool) (index : Fin (leftCount + rightCount)) : eval input (Fin.append left right index) = Fin.append (fun (leftIndex : Fin leftCount) => eval input (left leftIndex)) (fun (rightIndex : Fin rightCount) => eval input (right rightIndex)) index

theorem Algebraic.DeMorgan.Wiring.eval_finAppend_apply {leftCount width inputs rightCount : ℕ} (left : Fin leftCount → Fin width → Wiring inputs) (right : Fin rightCount → Fin width → Wiring inputs) (input : Fin inputs → Bool) (index : Fin (leftCount + rightCount)) (bit : Fin width) : eval input (Fin.append left right index bit) = Fin.append (fun (leftIndex : Fin leftCount) (bit : Fin width) => eval input (left leftIndex bit)) (fun (rightIndex : Fin rightCount) (bit : Fin width) => eval input (right rightIndex bit)) index bit

def Algebraic.DeMorgan.Wiring.circuit {outputs inputs : ℕ} (specification : Fin outputs → Wiring inputs) : Circuit signature inputs outputs

Compile an arbitrary vector of input selections and constants.

Equations

• Algebraic.DeMorgan.Wiring.circuit specification = Cslib.Circuits.Circuit.parallelFin outputs fun (output : Fin outputs) => (specification output).expression.circuit

@[simp]

theorem Algebraic.DeMorgan.Wiring.circuit_size {outputs inputs : ℕ} (specification : Fin outputs → Wiring inputs) : (circuit specification).size = ∑ output : Fin outputs, (specification output).expression.gateCount

The compiled wiring layer has one gate per hardwired constant.

@[simp]

theorem Algebraic.DeMorgan.Wiring.circuit_eval {outputs inputs : ℕ} (specification : Fin outputs → Wiring inputs) (input : Fin inputs → Bool) : (circuit specification).eval interpretation input = fun (output : Fin outputs) => eval input (specification output)

@[simp]

theorem Algebraic.DeMorgan.Wiring.circuit_cost {outputs inputs : ℕ} (specification : Fin outputs → Wiring inputs) : (circuit specification).cost standardCost = 0