Circuit wires and renamings

A Wire inputCount gateCount refers to an original input or an internal gate. A valuation of wires is assembled with Wire.elim from values for the inputs and values for the gates. Wire.index numbers the inputs first and then the gates in order, so that a gate reads only wires with a smaller index.

Wire.Renaming fixes the original inputs and maps each gate to an input or gate in the target namespace. This file provides identity and composition, extension by a gate, replacement of the last gate, and renaming by a permutation.

inductive Cslib.Circuits.Wire (inputCount gateCount : ℕ) : Type

A wire is either an original input or the output of an earlier gate.

• input {inputCount gateCount : ℕ} (input : Fin inputCount) : Wire inputCount gateCount

  An original input.

• gate {inputCount gateCount : ℕ} (gate : Fin gateCount) : Wire inputCount gateCount

  The output of an internal gate.

@[instance_reducible]

instance Cslib.Circuits.instDecidableEqWire {inputCount✝ gateCount✝ : ℕ} : DecidableEq (Wire inputCount✝ gateCount✝)

Equations

• Cslib.Circuits.instDecidableEqWire = Cslib.Circuits.instDecidableEqWire.decEq

def Cslib.Circuits.instDecidableEqWire.decEq {inputCount✝ gateCount✝ : ℕ} (x✝ x✝¹ : Wire inputCount✝ gateCount✝) : Decidable (x✝ = x✝¹)

Equations

• Cslib.Circuits.instDecidableEqWire.decEq (Cslib.Circuits.Wire.input a) (Cslib.Circuits.Wire.input b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cslib.Circuits.instDecidableEqWire.decEq (Cslib.Circuits.Wire.input input) (Cslib.Circuits.Wire.gate gate) = isFalse ⋯
• Cslib.Circuits.instDecidableEqWire.decEq (Cslib.Circuits.Wire.gate gate) (Cslib.Circuits.Wire.input input) = isFalse ⋯
• Cslib.Circuits.instDecidableEqWire.decEq (Cslib.Circuits.Wire.gate a) (Cslib.Circuits.Wire.gate b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Cslib.Circuits.Wire.elim {inputCount gateCount : ℕ} {α : Sort u_1} (inputs : Fin inputCount → α) (gates : Fin gateCount → α) : Wire inputCount gateCount → α

Define a function on wires from its values on inputs and on gates.

Equations

• Cslib.Circuits.Wire.elim inputs gates (Cslib.Circuits.Wire.input i) = inputs i
• Cslib.Circuits.Wire.elim inputs gates (Cslib.Circuits.Wire.gate j) = gates j

@[simp]

theorem Cslib.Circuits.Wire.elim_input {inputCount gateCount : ℕ} {α : Sort u_1} (inputs : Fin inputCount → α) (gates : Fin gateCount → α) (i : Fin inputCount) : elim inputs gates (input i) = inputs i

@[simp]

theorem Cslib.Circuits.Wire.elim_gate {inputCount gateCount : ℕ} {α : Sort u_1} (inputs : Fin inputCount → α) (gates : Fin gateCount → α) (j : Fin gateCount) : elim inputs gates (gate j) = gates j

def Cslib.Circuits.Wire.equiv (inputCount gateCount : ℕ) : Wire inputCount gateCount ≃ Fin inputCount ⊕ Fin gateCount

A wire is an input or a gate.

Equations

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

@[instance_reducible]

instance Cslib.Circuits.Wire.instFintype {inputCount gateCount : ℕ} : Fintype (Wire inputCount gateCount)

Equations

• Cslib.Circuits.Wire.instFintype = Fintype.ofEquiv (Fin inputCount ⊕ Fin gateCount) (Cslib.Circuits.Wire.equiv inputCount gateCount).symm

@[simp]

theorem Cslib.Circuits.Wire.card {inputCount gateCount : ℕ} : Fintype.card (Wire inputCount gateCount) = inputCount + gateCount

def Cslib.Circuits.Wire.index {inputCount gateCount : ℕ} : Wire inputCount gateCount → Fin (inputCount + gateCount)

The position of a wire when the inputs are listed first, followed by the gates in program order. A gate reads only wires whose index is below its own.

Equations

• (Cslib.Circuits.Wire.input i).index = Fin.castAdd gateCount i
• (Cslib.Circuits.Wire.gate j).index = Fin.natAdd inputCount j

@[simp]

theorem Cslib.Circuits.Wire.index_input {inputCount gateCount : ℕ} (i : Fin inputCount) : (input i).index = Fin.castAdd gateCount i

@[simp]

theorem Cslib.Circuits.Wire.index_gate {inputCount gateCount : ℕ} (j : Fin gateCount) : (gate j).index = Fin.natAdd inputCount j

def Cslib.Circuits.Wire.castSucc {inputCount gateCount : ℕ} : Wire inputCount gateCount → Wire inputCount (gateCount + 1)

Regard a wire as a wire in a namespace with one additional gate.

Equations

• (Cslib.Circuits.Wire.input i).castSucc = Cslib.Circuits.Wire.input i
• (Cslib.Circuits.Wire.gate j).castSucc = Cslib.Circuits.Wire.gate j.castSucc

@[simp]

theorem Cslib.Circuits.Wire.castSucc_input {inputCount gateCount : ℕ} (i : Fin inputCount) : (input i).castSucc = input i

@[simp]

theorem Cslib.Circuits.Wire.castSucc_gate {inputCount gateCount : ℕ} (j : Fin gateCount) : (gate j).castSucc = gate j.castSucc

def Cslib.Circuits.Wire.lastCases {inputCount gateCount : ℕ} {motive : Wire inputCount (gateCount + 1) → Sort u_2} (last : motive (gate (Fin.last gateCount))) (castSucc : (wire : Wire inputCount gateCount) → motive wire.castSucc) (wire : Wire inputCount (gateCount + 1)) : motive wire

A wire in a namespace with one additional gate is either the new last gate or an earlier wire.

Equations

• Cslib.Circuits.Wire.lastCases last castSucc (Cslib.Circuits.Wire.input i) = castSucc (Cslib.Circuits.Wire.input i)
• Cslib.Circuits.Wire.lastCases last castSucc (Cslib.Circuits.Wire.gate j) = Fin.lastCases last (fun (j : Fin gateCount) => castSucc (Cslib.Circuits.Wire.gate j)) j

@[simp]

theorem Cslib.Circuits.Wire.lastCases_last {inputCount gateCount : ℕ} {motive : Wire inputCount (gateCount + 1) → Sort u_2} (last : motive (gate (Fin.last gateCount))) (castSucc : (wire : Wire inputCount gateCount) → motive wire.castSucc) : lastCases last castSucc (gate (Fin.last gateCount)) = last

@[simp]

theorem Cslib.Circuits.Wire.lastCases_castSucc {inputCount gateCount : ℕ} {motive : Wire inputCount (gateCount + 1) → Sort u_2} (last : motive (gate (Fin.last gateCount))) (castSucc : (wire : Wire inputCount gateCount) → motive wire.castSucc) (wire : Wire inputCount gateCount) : lastCases last castSucc wire.castSucc = castSucc wire

@[simp]

theorem Cslib.Circuits.Wire.val_index_castSucc {inputCount gateCount : ℕ} (wire : Wire inputCount gateCount) : ↑wire.castSucc.index = ↑wire.index

def Cslib.Circuits.Wire.castAdd {inputCount gateCount : ℕ} (extra : ℕ) : Wire inputCount gateCount → Wire inputCount (gateCount + extra)

Regard a wire as a wire of the same program continued by extra further gates.

Equations

• Cslib.Circuits.Wire.castAdd extra (Cslib.Circuits.Wire.input i) = Cslib.Circuits.Wire.input i
• Cslib.Circuits.Wire.castAdd extra (Cslib.Circuits.Wire.gate j) = Cslib.Circuits.Wire.gate (Fin.castAdd extra j)

@[simp]

theorem Cslib.Circuits.Wire.castAdd_input {inputCount gateCount : ℕ} (extra : ℕ) (i : Fin inputCount) : castAdd extra (input i) = input i

@[simp]

theorem Cslib.Circuits.Wire.castAdd_gate {inputCount gateCount : ℕ} (extra : ℕ) (j : Fin gateCount) : castAdd extra (gate j) = gate (Fin.castAdd extra j)

structure Cslib.Circuits.Wire.Renaming (inputCount sourceGateCount targetGateCount : ℕ) : Type

A renaming of gate wires that fixes every original input. Gate wires may be sent to either inputs or gates in the target namespace.

• gates : Fin sourceGateCount → Wire inputCount targetGateCount

  The target wire representing each source gate.

def Cslib.Circuits.Wire.Renaming.apply {inputCount sourceGateCount targetGateCount : ℕ} (ρ : Renaming inputCount sourceGateCount targetGateCount) : Wire inputCount sourceGateCount → Wire inputCount targetGateCount

Apply an input-fixing wire renaming.

Equations

• ρ.apply = Cslib.Circuits.Wire.elim Cslib.Circuits.Wire.input ρ.gates

@[instance_reducible]

instance Cslib.Circuits.Wire.Renaming.instCoeFunForall {inputCount sourceGateCount targetGateCount : ℕ} : CoeFun (Renaming inputCount sourceGateCount targetGateCount) fun (x : Renaming inputCount sourceGateCount targetGateCount) => Wire inputCount sourceGateCount → Wire inputCount targetGateCount

Equations

• Cslib.Circuits.Wire.Renaming.instCoeFunForall = { coe := Cslib.Circuits.Wire.Renaming.apply }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.apply_input {inputCount sourceGateCount targetGateCount : ℕ} (ρ : Renaming inputCount sourceGateCount targetGateCount) (input : Fin inputCount) : ρ.apply (Wire.input input) = Wire.input input

@[simp]

theorem Cslib.Circuits.Wire.Renaming.apply_gate {inputCount sourceGateCount targetGateCount : ℕ} (ρ : Renaming inputCount sourceGateCount targetGateCount) (gate : Fin sourceGateCount) : ρ.apply (Wire.gate gate) = ρ.gates gate

def Cslib.Circuits.Wire.Renaming.id {inputCount gateCount : ℕ} : Renaming inputCount gateCount gateCount

The identity wire renaming.

Equations

• Cslib.Circuits.Wire.Renaming.id = { gates := Cslib.Circuits.Wire.gate }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.id_apply {inputCount gateCount : ℕ} (wire : Wire inputCount gateCount) : id.apply wire = wire

def Cslib.Circuits.Wire.Renaming.comp {inputCount sourceGateCount middleGateCount targetGateCount : ℕ} (outer : Renaming inputCount middleGateCount targetGateCount) (inner : Renaming inputCount sourceGateCount middleGateCount) : Renaming inputCount sourceGateCount targetGateCount

Compose input-fixing wire renamings.

Equations

• outer.comp inner = { gates := outer.apply ∘ inner.gates }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.comp_apply {inputCount sourceGateCount middleGateCount targetGateCount : ℕ} (outer : Renaming inputCount middleGateCount targetGateCount) (inner : Renaming inputCount sourceGateCount middleGateCount) (wire : Wire inputCount sourceGateCount) : (outer.comp inner).apply wire = outer.apply (inner.apply wire)

def Cslib.Circuits.Wire.Renaming.castSucc {inputCount gateCount : ℕ} : Renaming inputCount gateCount (gateCount + 1)

Include all wires into a namespace with one additional gate.

Equations

• Cslib.Circuits.Wire.Renaming.castSucc = { gates := fun (gate : Fin gateCount) => Cslib.Circuits.Wire.gate gate.castSucc }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.castSucc_apply {inputCount gateCount : ℕ} (wire : Wire inputCount gateCount) : castSucc.apply wire = wire.castSucc

def Cslib.Circuits.Wire.Renaming.skipLast {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (replacement : Wire inputCount targetGateCount) : Renaming inputCount (sourceGateCount + 1) targetGateCount

Extend a renaming while replacing the new last gate by an existing wire.

Equations

• prior.skipLast replacement = { gates := fun (i : Fin (sourceGateCount + 1)) => Fin.lastCases replacement prior.gates i }

@[simp]

theorem Cslib.Circuits.Wire.Renaming.skipLast_gates_last {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (replacement : Wire inputCount targetGateCount) : (prior.skipLast replacement).gates (Fin.last sourceGateCount) = replacement

@[simp]

theorem Cslib.Circuits.Wire.Renaming.skipLast_castSucc {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (replacement : Wire inputCount targetGateCount) (wire : Wire inputCount sourceGateCount) : (prior.skipLast replacement).apply wire.castSucc = prior.apply wire

def Cslib.Circuits.Wire.Renaming.appendLast {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) : Renaming inputCount (sourceGateCount + 1) (targetGateCount + 1)

Extend a renaming and retain the new last gate as a fresh target gate.

Equations

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

@[simp]

theorem Cslib.Circuits.Wire.Renaming.appendLast_gates_last {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) : prior.appendLast.gates (Fin.last sourceGateCount) = gate (Fin.last targetGateCount)

@[simp]

theorem Cslib.Circuits.Wire.Renaming.appendLast_castSucc {inputCount sourceGateCount targetGateCount : ℕ} (prior : Renaming inputCount sourceGateCount targetGateCount) (wire : Wire inputCount sourceGateCount) : prior.appendLast.apply wire.castSucc = (prior.apply wire).castSucc

def Cslib.Circuits.Wire.Renaming.ofPermutation {inputCount gateCount : ℕ} (permutation : Equiv.Perm (Fin gateCount)) : Renaming inputCount gateCount gateCount

Rename gate wires by a permutation.

Equations

• Cslib.Circuits.Wire.Renaming.ofPermutation permutation = { gates := fun (gate : Fin gateCount) => Cslib.Circuits.Wire.gate (permutation gate) }

theorem Cslib.Circuits.Wire.Renaming.ofPermutation_gate {inputCount gateCount : ℕ} (permutation : Equiv.Perm (Fin gateCount)) (gate : Fin gateCount) : (ofPermutation permutation).apply (Wire.gate gate) = Wire.gate (permutation gate)

theorem Cslib.Circuits.Wire.Renaming.value_apply {inputCount sourceGateCount targetGateCount : ℕ} {U : Type u_1} (ρ : Renaming inputCount sourceGateCount targetGateCount) (inputs : Fin inputCount → U) (oldGates : Fin sourceGateCount → U) (newGates : Fin targetGateCount → U) (preservesGates : ∀ (gate : Fin sourceGateCount), elim inputs newGates (ρ.gates gate) = oldGates gate) (wire : Wire inputCount sourceGateCount) : elim inputs newGates (ρ.apply wire) = elim inputs oldGates wire

A source and target gate valuation agree along a renaming when they agree on the image of every source gate. Original inputs agree automatically.