Wiring with structured coordinates

Explicit equivalences number the input and output coordinates. A selector between those coordinates lowers to ordinary circuit wiring, with no gates. Selectors need not be injective: several outputs can reuse one input. Standard finite sums and products supply executable layouts without choosing arbitrary enumerations.

Main definitions

• Cslib.Circuits.Circuit.wiringOn: wiring between explicitly numbered coordinate types.

Main results

• Cslib.Circuits.Circuit.eval_wiringOn: evaluation through the explicit coordinate numberings.
• Cslib.Circuits.Circuit.cost_program_wiringOn: structural wiring has zero weighted cost.

def Cslib.Circuits.Circuit.wiringOn {ι : Type u_1} {κ : Type u_2} {n m : ℕ} (σ : Signature) (input : ι ≃ Fin n) (output : κ ≃ Fin m) (select : κ → ι) : Circuit σ n m

Lower a coordinate selector through explicit input and output numberings.

@[simp]

theorem Cslib.Circuits.Circuit.eval_wiringOn {σ : Signature} {ι : Type u_1} {κ : Type u_2} {U : Type u_3} {n m : ℕ} (input : ι ≃ Fin n) (output : κ ≃ Fin m) (select : κ → ι) (I : Interpretation σ U) (x : Fin n → U) : (wiringOn σ input output select).eval I x = x ∘ ⇑input ∘ select ∘ ⇑output.symm

Each output reads the input selected in the structured coordinates.

theorem Cslib.Circuits.Circuit.cost_program_wiringOn {σ : Signature} {ι : Type u_1} {κ : Type u_2} {n m : ℕ} (input : ι ≃ Fin n) (output : κ ≃ Fin m) (select : κ → ι) (cost : σ.Op → ℕ) : (wiringOn σ input output select).program.cost cost = 0

Coordinate changes and fan-out introduce no weighted gate cost.

@[simp]

theorem Cslib.Circuits.Circuit.size_wiringOn {σ : Signature} {ι : Type u_1} {κ : Type u_2} {n m : ℕ} (input : ι ≃ Fin n) (output : κ ≃ Fin m) (select : κ → ι) : (wiringOn σ input output select).size = 0