Input reindexing and parallel circuits

This file provides the structural circuit operations used by simultaneous evaluation arguments. Circuit.mapInputs rewires the original inputs without adding gates, Circuit.mapOutputs selects or repeats designated outputs, and Circuit.parallel places two circuits with the same input namespace side by side. Parallel composition preserves sharing within each operand and has exactly additive cost.

def Cslib.Circuits.Circuit.castCounts {σ : Signature} {n m n' m' : ℕ} (inputCount : n = n') (outputCount : m = m') (circuit : Circuit σ n m) : Circuit σ n' m'

Transport a circuit along equalities of its input and output counts. This is a structural cast; it changes no gate or wire.

Equations

• Cslib.Circuits.Circuit.castCounts inputCount outputCount circuit = inputCount ▸ outputCount ▸ circuit

@[simp]

theorem Cslib.Circuits.Circuit.eval_castCounts {σ : Signature} {U : Type u_2} {n m n' m' : ℕ} (inputCount : n = n') (outputCount : m = m') (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n' → U) : (castCounts inputCount outputCount circuit).eval interpretation input = fun (output : Fin m') => circuit.eval interpretation (input ∘ Fin.cast inputCount) (Fin.cast ⋯ output)

Casting circuit counts transports inputs and outputs by the corresponding finite-index equalities and otherwise preserves evaluation.

@[simp]

theorem Cslib.Circuits.Circuit.cost_castCounts {σ : Signature} {n m n' m' : ℕ} (inputCount : n = n') (outputCount : m = m') (circuit : Circuit σ n m) (operationCost : Algebraic.OperationCost σ) : (castCounts inputCount outputCount circuit).cost operationCost = circuit.cost operationCost

Casting circuit counts preserves weighted cost.

@[simp]

theorem Cslib.Circuits.Circuit.size_castCounts {σ : Signature} {n m n' m' : ℕ} (inputCount : n = n') (outputCount : m = m') (circuit : Circuit σ n m) : (castCounts inputCount outputCount circuit).size = circuit.size

Casting circuit counts preserves the gate count exactly.

def Cslib.Circuits.Wire.mapInputs {n n' g : ℕ} (inputMap : Fin n → Fin n') : Wire n g → Wire n' g

Reindex the original inputs of a wire while leaving its gate index unchanged.

Equations

• Cslib.Circuits.Wire.mapInputs inputMap = Cslib.Circuits.Wire.elim (Cslib.Circuits.Wire.input ∘ inputMap) Cslib.Circuits.Wire.gate

@[simp]

theorem Cslib.Circuits.Wire.mapInputs_input {n n' g : ℕ} (inputMap : Fin n → Fin n') (input : Fin n) : mapInputs inputMap (Wire.input input) = Wire.input (inputMap input)

@[simp]

theorem Cslib.Circuits.Wire.mapInputs_gate {n n' g : ℕ} (inputMap : Fin n → Fin n') (gate : Fin g) : mapInputs inputMap (Wire.gate gate) = Wire.gate gate

def Cslib.Circuits.Program.mapInputs {n n' : ℕ} {σ : Signature} {g : ℕ} (inputMap : Fin n → Fin n') : Program σ n g → Program σ n' g

Reindex every original input of a program without changing its gates.

Equations

• Cslib.Circuits.Program.mapInputs inputMap Cslib.Circuits.Program.empty = Cslib.Circuits.Program.empty
• Cslib.Circuits.Program.mapInputs inputMap (program.gate line) = (Cslib.Circuits.Program.mapInputs inputMap program).gate (line.mapWires (Cslib.Circuits.Wire.mapInputs inputMap))

theorem Cslib.Circuits.Program.eval_mapInputs {σ : Signature} {n g n' : ℕ} {U : Type u_2} (program : Program σ n g) (inputMap : Fin n → Fin n') (interpretation : Interpretation σ U) (input : Fin n' → U) : (mapInputs inputMap program).eval interpretation input = program.eval interpretation (input ∘ inputMap)

Input reindexing evaluates a program after precomposing its input.

theorem Cslib.Circuits.Program.trace_mapInputs {σ : Signature} {n g n' : ℕ} {U : Type u_2} (program : Program σ n g) (inputMap : Fin n → Fin n') (interpretation : Interpretation σ U) (input : Fin n' → U) (wire : Wire n g) : (mapInputs inputMap program).trace interpretation input (Wire.mapInputs inputMap wire) = program.trace interpretation (input ∘ inputMap) wire

Input reindexing preserves the value of every mapped wire.

@[simp]

theorem Cslib.Circuits.Program.cost_mapInputs {σ : Signature} {n g n' : ℕ} (program : Program σ n g) (inputMap : Fin n → Fin n') (operationCost : Algebraic.OperationCost σ) : cost operationCost (mapInputs inputMap program) = cost operationCost program

Input reindexing leaves every gate label, and hence every weighted cost, unchanged.

def Cslib.Circuits.Circuit.mapInputs {σ : Signature} {n m n' : ℕ} (circuit : Circuit σ n m) (inputMap : Fin n → Fin n') : Circuit σ n' m

Rewire the original inputs of a circuit without adding gates. The map may identify, duplicate, permute, or discard inputs.

Equations

• circuit.mapInputs inputMap = { size := circuit.size, program := Cslib.Circuits.Program.mapInputs inputMap circuit.program, outputs := Cslib.Circuits.Wire.mapInputs inputMap ∘ circuit.outputs }

@[simp]

theorem Cslib.Circuits.Circuit.eval_mapInputs {σ : Signature} {n m n' : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (inputMap : Fin n → Fin n') (interpretation : Interpretation σ U) (input : Fin n' → U) : (circuit.mapInputs inputMap).eval interpretation input = circuit.eval interpretation (input ∘ inputMap)

@[simp]

theorem Cslib.Circuits.Circuit.cost_mapInputs {σ : Signature} {n m n' : ℕ} (circuit : Circuit σ n m) (inputMap : Fin n → Fin n') (operationCost : Algebraic.OperationCost σ) : (circuit.mapInputs inputMap).cost operationCost = circuit.cost operationCost

@[simp]

theorem Cslib.Circuits.Circuit.size_mapInputs {σ : Signature} {n m n' : ℕ} (circuit : Circuit σ n m) (inputMap : Fin n → Fin n') : (circuit.mapInputs inputMap).size = circuit.size

def Cslib.Circuits.Circuit.mapOutputs {σ : Signature} {n m m' : ℕ} (circuit : Circuit σ n m) (outputMap : Fin m' → Fin m) : Circuit σ n m'

Select, reorder, or repeat the designated outputs of a circuit without changing its gates.

Equations

• circuit.mapOutputs outputMap = { size := circuit.size, program := circuit.program, outputs := circuit.outputs ∘ outputMap }

@[simp]

theorem Cslib.Circuits.Circuit.eval_mapOutputs {σ : Signature} {n m m' : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (outputMap : Fin m' → Fin m) (interpretation : Interpretation σ U) (input : Fin n → U) : (circuit.mapOutputs outputMap).eval interpretation input = circuit.eval interpretation input ∘ outputMap

@[simp]

theorem Cslib.Circuits.Circuit.cost_mapOutputs {σ : Signature} {n m m' : ℕ} (circuit : Circuit σ n m) (outputMap : Fin m' → Fin m) (operationCost : Algebraic.OperationCost σ) : (circuit.mapOutputs outputMap).cost operationCost = circuit.cost operationCost

@[simp]

theorem Cslib.Circuits.Circuit.size_mapOutputs {σ : Signature} {n m m' : ℕ} (circuit : Circuit σ n m) (outputMap : Fin m' → Fin m) : (circuit.mapOutputs outputMap).size = circuit.size

def Cslib.Circuits.Circuit.parallel {σ : Signature} {n m k : ℕ} (left : Circuit σ n m) (right : Circuit σ n k) : Circuit σ n (m + k)

Place two circuits with the same original inputs side by side and concatenate their designated outputs.

Equations

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

@[simp]

theorem Cslib.Circuits.Circuit.eval_parallel {σ : Signature} {n m k : ℕ} {U : Type u_2} (left : Circuit σ n m) (right : Circuit σ n k) (interpretation : Interpretation σ U) (input : Fin n → U) : (left.parallel right).eval interpretation input = Fin.append (left.eval interpretation input) (right.eval interpretation input)

Parallel composition concatenates the two output vectors.

@[simp]

theorem Cslib.Circuits.Circuit.cost_parallel {σ : Signature} {n m k : ℕ} (left : Circuit σ n m) (right : Circuit σ n k) (operationCost : Algebraic.OperationCost σ) : (left.parallel right).cost operationCost = left.cost operationCost + right.cost operationCost

Parallel composition has exactly additive weighted cost.

@[simp]

theorem Cslib.Circuits.Circuit.size_parallel {σ : Signature} {n m k : ℕ} (left : Circuit σ n m) (right : Circuit σ n k) : (left.parallel right).size = left.size + right.size

Parallel composition has exactly additive gate count.

def Cslib.Circuits.Circuit.parallelPair {σ : Signature} {n width : ℕ} (left right : Circuit σ n width) : Circuit σ n (2 * width)

Put two equally wide output vectors into the row-major two-block layout Fin (2 * width).

Equations

• left.parallelPair right = (left.parallel right).mapOutputs (Fin.cast ⋯)

@[simp]

theorem Cslib.Circuits.Circuit.size_parallelPair {σ : Signature} {n width : ℕ} (left right : Circuit σ n width) : (left.parallelPair right).size = left.size + right.size

The row-major pair has exactly additive gate count.

@[simp]

theorem Cslib.Circuits.Circuit.eval_parallelPair_apply {σ : Signature} {n width : ℕ} {U : Type u_2} (left right : Circuit σ n width) (interpretation : Interpretation σ U) (input : Fin n → U) (side : Fin 2) (coordinate : Fin width) : (left.parallelPair right).eval interpretation input (finProdFinEquiv (side, coordinate)) = Fin.cases (left.eval interpretation input coordinate) (fun (x : Fin 1) => right.eval interpretation input coordinate) side

Evaluation of parallelPair selects the indicated row-major block.

@[simp]

theorem Cslib.Circuits.Circuit.cost_parallelPair {σ : Signature} {n width : ℕ} (left right : Circuit σ n width) (operationCost : Algebraic.OperationCost σ) : (left.parallelPair right).cost operationCost = left.cost operationCost + right.cost operationCost

def Cslib.Circuits.Circuit.parallelFin {σ : Signature} {n : ℕ} (outputs : ℕ) : (Fin outputs → Circuit σ n 1) → Circuit σ n outputs

Place a finite family of scalar circuits with a common input namespace side by side. Each member may have a different gate count; the resulting gate count is their finite sum (Circuit.size_parallelFin).

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Circuits.Circuit.parallelFin 0 x_2 = (Cslib.Circuits.Circuit.id σ n).mapOutputs Fin.elim0

@[simp]

theorem Cslib.Circuits.Circuit.size_parallelFin {σ : Signature} {n : ℕ} (outputs : ℕ) (circuits : Fin outputs → Circuit σ n 1) : (parallelFin outputs circuits).size = ∑ output : Fin outputs, (circuits output).size

The gate count of a finite parallel family is the sum of its members' gate counts.

@[simp]

theorem Cslib.Circuits.Circuit.eval_parallelFin {σ : Signature} {n : ℕ} {U : Type u_2} (outputs : ℕ) (circuits : Fin outputs → Circuit σ n 1) (interpretation : Interpretation σ U) (input : Fin n → U) (output : Fin outputs) : (parallelFin outputs circuits).eval interpretation input output = (circuits output).eval interpretation input 0

parallelFin returns, at each output coordinate, the corresponding member circuit's scalar value.

@[simp]

theorem Cslib.Circuits.Circuit.cost_parallelFin {σ : Signature} {n : ℕ} (outputs : ℕ) (circuits : Fin outputs → Circuit σ n 1) (operationCost : Algebraic.OperationCost σ) : (parallelFin outputs circuits).cost operationCost = ∑ output : Fin outputs, (circuits output).cost operationCost

Exact weighted cost of a finite parallel family.

def Cslib.Circuits.Circuit.parallelFinVector {σ : Signature} {n : ℕ} (members width : ℕ) : (Fin members → Circuit σ n width) → Circuit σ n (members * width)

Place a finite family of equally wide vector circuits side by side in row-major (member, coordinate) order. The resulting gate count is the sum of the members' gate counts (Circuit.size_parallelFinVector).

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Circuits.Circuit.parallelFinVector 0 x✝¹ x✝ = (Cslib.Circuits.Circuit.id σ n).mapOutputs fun (output : Fin (0 * x✝¹)) => (Fin.cast ⋯ output).elim0

@[simp]

theorem Cslib.Circuits.Circuit.size_parallelFinVector {σ : Signature} {n : ℕ} (members width : ℕ) (circuits : Fin members → Circuit σ n width) : (parallelFinVector members width circuits).size = ∑ member : Fin members, (circuits member).size

The gate count of a finite parallel vector family is the sum of its members' gate counts.

@[simp]

theorem Cslib.Circuits.Circuit.eval_parallelFinVector {σ : Signature} {n : ℕ} {U : Type u_2} (members width : ℕ) (circuits : Fin members → Circuit σ n width) (interpretation : Interpretation σ U) (input : Fin n → U) (member : Fin members) (coordinate : Fin width) : (parallelFinVector members width circuits).eval interpretation input (finProdFinEquiv (member, coordinate)) = (circuits member).eval interpretation input coordinate

parallelFinVector evaluates the indicated member and coordinate.

@[simp]

theorem Cslib.Circuits.Circuit.cost_parallelFinVector {σ : Signature} {n : ℕ} (members width : ℕ) (circuits : Fin members → Circuit σ n width) (operationCost : Algebraic.OperationCost σ) : (parallelFinVector members width circuits).cost operationCost = ∑ member : Fin members, (circuits member).cost operationCost

Exact weighted cost of a finite parallel vector family.