Circuit substitution

A wire substitution may replace both formal inputs and gate wires. The causal operation in this module is Program.instantiate: it appends a source program to an ambient program, maps formal inputs to ambient wires, and allocates every source gate in its original order. Circuits inherit the same operation by mapping their designated output wires. Sequential composition Circuit.comp is CSLib's; this module adds its cost law.

structure Cslib.Circuits.Wire.Substitution (n g n' g' : ℕ) : Type

A map from one input-and-gate wire namespace to another.

• inputs : Fin n → Wire n' g'

  Image of every formal input.

• gates : Fin g → Wire n' g'

  Image of every gate wire.

def Cslib.Circuits.Wire.Substitution.apply {n g n' g' : ℕ} (θ : Substitution n g n' g') : Wire n g → Wire n' g'

Apply a wire substitution.

Equations

• θ.apply = Cslib.Circuits.Wire.elim θ.inputs θ.gates

@[instance_reducible]

instance Algebraic.Wire.Substitution.instCoeFunSubstitutionForallWire {n g n' g' : ℕ} : CoeFun (Substitution n g n' g') fun (x : Substitution n g n' g') => Wire n g → Wire n' g'

Equations

• Algebraic.Wire.Substitution.instCoeFunSubstitutionForallWire = { coe := Cslib.Circuits.Wire.Substitution.apply }

@[simp]

theorem Cslib.Circuits.Wire.Substitution.apply_input {n g n' g' : ℕ} (θ : Substitution n g n' g') (input : Fin n) : θ.apply (Wire.input input) = θ.inputs input

@[simp]

theorem Cslib.Circuits.Wire.Substitution.apply_gate {n g n' g' : ℕ} (θ : Substitution n g n' g') (gate : Fin g) : θ.apply (Wire.gate gate) = θ.gates gate

def Cslib.Circuits.Wire.Renaming.castAdd {n g : ℕ} (k : ℕ) : Renaming n g (g + k)

Include a wire namespace into one with k additional gates.

Equations

• Cslib.Circuits.Wire.Renaming.castAdd k = { gates := fun (gate : Fin g) => Cslib.Circuits.Wire.gate (Fin.castAdd k gate) }

theorem Cslib.Circuits.Wire.Renaming.castAdd_input {n g : ℕ} (k : ℕ) (input : Fin n) : (castAdd k).apply (Wire.input input) = Wire.input input

theorem Cslib.Circuits.Wire.Renaming.castAdd_gate {g n : ℕ} (k : ℕ) (gate : Fin g) : (castAdd k).apply (Wire.gate gate) = Wire.gate (Fin.castAdd k gate)

@[simp]

theorem Cslib.Circuits.Wire.Renaming.castAdd_zero_apply {n g : ℕ} (wire : Wire n g) : (castAdd 0).apply wire = wire

theorem Cslib.Circuits.Wire.Renaming.castAdd_succ_apply {n g : ℕ} (k : ℕ) (wire : Wire n g) : (castAdd (k + 1)).apply wire = ((castAdd k).apply wire).castSucc

def Cslib.Circuits.Wire.Substitution.append {n n' h : ℕ} (inputWires : Fin n → Wire n' h) (g : ℕ) : Substitution n g n' (h + g)

Map formal inputs into an ambient program and source gates to the freshly appended block of gates.

Equations

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

theorem Cslib.Circuits.Wire.Substitution.append_castSucc {n n' h g : ℕ} (inputWires : Fin n → Wire n' h) (wire : Wire n g) : (append inputWires (g + 1)).apply wire.castSucc = ((append inputWires g).apply wire).castSucc

theorem Cslib.Circuits.Wire.Substitution.append_last {n n' h g : ℕ} (inputWires : Fin n → Wire n' h) : (append inputWires (g + 1)).apply (gate (Fin.last g)) = gate (Fin.last (h + g))

def Cslib.Circuits.Program.instantiate {σ : Signature} {n g n' h : ℕ} (source : Program σ n g) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) : Program σ n' (h + g)

Append source to ambient, replacing every formal source input by the corresponding ambient wire.

Equations

• Cslib.Circuits.Program.empty.instantiate ambient inputWires = ambient
• (source_2.gate line).instantiate ambient inputWires = (source_2.instantiate ambient inputWires).gate (line.mapWires (Cslib.Circuits.Wire.Substitution.append inputWires gateCount).apply)

theorem Cslib.Circuits.Program.instantiate_trace_ambient {σ : Signature} {n g n' h : ℕ} {U : Type u_2} (source : Program σ n g) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) (interpretation : Interpretation σ U) (input : Fin n' → U) (wire : Wire n' h) : (source.instantiate ambient inputWires).trace interpretation input ((Wire.Renaming.castAdd g).apply wire) = ambient.trace interpretation input wire

Instantiation leaves every ambient wire unchanged, up to inclusion into the extended wire namespace.

theorem Cslib.Circuits.Program.instantiate_trace {σ : Signature} {n g n' h : ℕ} {U : Type u_2} (source : Program σ n g) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) (interpretation : Interpretation σ U) (input : Fin n' → U) (wire : Wire n g) : (source.instantiate ambient inputWires).trace interpretation input ((Wire.Substitution.append inputWires g).apply wire) = source.trace interpretation (ambient.trace interpretation input ∘ inputWires) wire

Instantiation evaluates every source wire under the values supplied by the ambient input wires.

@[simp]

theorem Cslib.Circuits.Program.cost_instantiate {σ : Signature} {n g n' h : ℕ} (source : Program σ n g) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) (operationCost : Algebraic.OperationCost σ) : cost operationCost (source.instantiate ambient inputWires) = cost operationCost ambient + cost operationCost source

def Cslib.Circuits.Circuit.instantiate {σ : Signature} {n m n' h : ℕ} (source : Circuit σ n m) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) : Circuit σ n' m

Instantiate a circuit after an ambient program.

Equations

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

@[simp]

theorem Cslib.Circuits.Circuit.size_instantiate {σ : Signature} {n m n' h : ℕ} (source : Circuit σ n m) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) : (source.instantiate ambient inputWires).size = h + source.size

An instantiated circuit has the ambient gates followed by the source gates.

theorem Cslib.Circuits.Circuit.eval_instantiate {σ : Signature} {n m n' h : ℕ} {U : Type u_2} (source : Circuit σ n m) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) (interpretation : Interpretation σ U) (input : Fin n' → U) : (source.instantiate ambient inputWires).eval interpretation input = source.eval interpretation (ambient.trace interpretation input ∘ inputWires)

Circuit instantiation preserves evaluation exactly.

@[simp]

theorem Cslib.Circuits.Circuit.cost_instantiate {σ : Signature} {n m n' h : ℕ} (source : Circuit σ n m) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) (operationCost : Algebraic.OperationCost σ) : (source.instantiate ambient inputWires).cost operationCost = Program.cost operationCost ambient + source.cost operationCost

Circuit instantiation has exactly additive gate cost.

@[simp]

theorem Cslib.Circuits.Program.cost_append {σ : Signature} {n g k h : ℕ} (program : Program σ n g) (feed : Fin k → Wire n g) (continuation : Program σ k h) (operationCost : Algebraic.OperationCost σ) : cost operationCost (program.append feed continuation) = cost operationCost program + cost operationCost continuation

Continuing a program by another has exactly additive gate cost.

theorem Cslib.Circuits.Circuit.eval_comp_id {σ : Signature} {n m : ℕ} {U : Type u_2} (outer : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n → U) : (outer.comp (id σ n)).eval interpretation input = outer.eval interpretation input

theorem Cslib.Circuits.Circuit.eval_id_comp {σ : Signature} {n m : ℕ} {U : Type u_2} (inner : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n → U) : ((id σ m).comp inner).eval interpretation input = inner.eval interpretation input

@[simp]

theorem Cslib.Circuits.Circuit.cost_comp {σ : Signature} {m k n : ℕ} (outer : Circuit σ m k) (inner : Circuit σ n m) (operationCost : Algebraic.OperationCost σ) : (outer.comp inner).cost operationCost = inner.cost operationCost + outer.cost operationCost