Composing circuits

A program can be continued by a second program whose inputs are read from wires of the first. Reading them from the outputs of a circuit gives sequential composition, Circuit.comp, which evaluates to the composite of the two functions. Reading them from the original inputs gives parallel composition on shared inputs, Circuit.append, whose outputs are those of the first circuit followed by those of the second. In both cases the gate counts add.

@[simp]

theorem Fin.append_comp_castAdd {α : Type u_1} {m n : ℕ} (u : Fin m → α) (v : Fin n → α) : append u v ∘ castAdd n = u

@[simp]

theorem Fin.append_comp_natAdd {α : Type u_1} {m n : ℕ} (u : Fin m → α) (v : Fin n → α) : append u v ∘ natAdd m = v

def Cslib.Circuits.Program.appendedWire {n k g₁ g₂ : ℕ} (feed : Fin k → Wire n g₁) : Wire k g₂ → Wire n (g₁ + g₂)

For programs p : Program σ n g₁ and q : Program σ k g₂, with feed : Fin k → Wire n g₁, map a wire of q to its wire in the combined program. Inputs follow feed, and gate indices are shifted past the gates of p. This is the wire map used by Program.append below.

Equations

• Cslib.Circuits.Program.appendedWire feed (Cslib.Circuits.Wire.input i) = Cslib.Circuits.Wire.castAdd g₂ (feed i)
• Cslib.Circuits.Program.appendedWire feed (Cslib.Circuits.Wire.gate j) = Cslib.Circuits.Wire.gate (Fin.natAdd g₁ j)

@[simp]

theorem Cslib.Circuits.Program.appendedWire_input {n k g₁ g₂ : ℕ} (feed : Fin k → Wire n g₁) (i : Fin k) : appendedWire feed (Wire.input i) = Wire.castAdd g₂ (feed i)

@[simp]

theorem Cslib.Circuits.Program.appendedWire_gate {n k g₁ g₂ : ℕ} (feed : Fin k → Wire n g₁) (j : Fin g₂) : appendedWire feed (Wire.gate j) = Wire.gate (Fin.natAdd g₁ j)

def Cslib.Circuits.Program.append {σ : Signature} {n k g₁ : ℕ} (p : Program σ n g₁) (feed : Fin k → Wire n g₁) {g₂ : ℕ} (q : Program σ k g₂) : Program σ n (g₁ + g₂)

Continue p by q, reading the inputs of q from the wires feed of p.

Equations

• p.append feed Cslib.Circuits.Program.empty = p
• p.append feed (q_2.gate line) = (p.append feed q_2).gate (line.mapWires (Cslib.Circuits.Program.appendedWire feed))

theorem Cslib.Circuits.Program.trace_append_castAdd {σ : Signature} {U : Type u} {n k g₁ g₂ : ℕ} (p : Program σ n g₁) (feed : Fin k → Wire n g₁) (I : Interpretation σ U) (x : Fin n → U) (q : Program σ k g₂) (w : Wire n g₁) : (p.append feed q).trace I x (Wire.castAdd g₂ w) = p.trace I x w

The wires of p keep their values after p is continued.

theorem Cslib.Circuits.Program.trace_append_appendedWire {σ : Signature} {U : Type u} {n k g₁ g₂ : ℕ} (p : Program σ n g₁) (feed : Fin k → Wire n g₁) (I : Interpretation σ U) (x : Fin n → U) (q : Program σ k g₂) (w : Wire k g₂) : (p.append feed q).trace I x (appendedWire feed w) = q.trace I (fun (i : Fin k) => p.trace I x (feed i)) w

A wire of q carries, in the continued program, the value it has when q runs on the values of the wires feeding it.

def Cslib.Circuits.Circuit.comp {σ : Signature} {n m p : ℕ} (d : Circuit σ m p) (c : Circuit σ n m) : Circuit σ n p

Feed the outputs of c to the inputs of d.

Equations

• d.comp c = { size := c.size + d.size, program := c.program.append c.outputs d.program, outputs := Cslib.Circuits.Program.appendedWire c.outputs ∘ d.outputs }

@[simp]

theorem Cslib.Circuits.Circuit.size_comp {σ : Signature} {n m p : ℕ} (d : Circuit σ m p) (c : Circuit σ n m) : (d.comp c).size = c.size + d.size

@[simp]

theorem Cslib.Circuits.Circuit.eval_comp {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} (d : Circuit σ m p) (c : Circuit σ n m) (x : Fin n → U) : (d.comp c).eval I x = d.eval I (c.eval I x)

def Cslib.Circuits.Circuit.append {σ : Signature} {n m p : ℕ} (c : Circuit σ n m) (d : Circuit σ n p) : Circuit σ n (m + p)

Run c and d on the same inputs, listing the outputs of c before those of d.

Equations

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

@[simp]

theorem Cslib.Circuits.Circuit.size_append {σ : Signature} {n m p : ℕ} (c : Circuit σ n m) (d : Circuit σ n p) : (c.append d).size = c.size + d.size

@[simp]

theorem Cslib.Circuits.Circuit.eval_append {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} (c : Circuit σ n m) (d : Circuit σ n p) (x : Fin n → U) : (c.append d).eval I x = Fin.append (c.eval I x) (d.eval I x)

theorem Cslib.Circuits.Circuit.Computes.comp {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {c : Circuit σ n m} {d : Circuit σ m p} {f : (Fin n → U) → Fin m → U} {g : (Fin m → U) → Fin p → U} (hc : c.Computes I f) (hd : d.Computes I g) : (d.comp c).Computes I (g ∘ f)

Feeding a circuit computing f into one computing g computes g ∘ f.

theorem Cslib.Circuits.Circuit.Computes.append {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {c : Circuit σ n m} {d : Circuit σ n p} {f : (Fin n → U) → Fin m → U} {g : (Fin n → U) → Fin p → U} (hc : c.Computes I f) (hd : d.Computes I g) : (c.append d).Computes I fun (x : Fin n → U) => Fin.append (f x) (g x)

Circuits computing f and g, run side by side, compute their outputs together.

theorem Cslib.Circuits.Circuit.ComputesOn.comp {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {c : Circuit σ n m} {d : Circuit σ m p} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} {g : (Fin m → U) → Fin p → U} (hc : c.ComputesOn I S f) (hd : d.ComputesOn I (f '' S) g) : (d.comp c).ComputesOn I S (g ∘ f)

Feeding a circuit computing f on S into one computing g on the image of S computes g ∘ f on S.

theorem Cslib.Circuits.Circuit.ComputesOn.append {σ : Signature} {U : Type u} {n m p : ℕ} {I : Interpretation σ U} {c : Circuit σ n m} {d : Circuit σ n p} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} {g : (Fin n → U) → Fin p → U} (hc : c.ComputesOn I S f) (hd : d.ComputesOn I S g) : (c.append d).ComputesOn I S fun (x : Fin n → U) => Fin.append (f x) (g x)

Circuits computing f and g on S, run side by side, compute their outputs together.