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.appendWire {n k g₁ g₂ : ℕ} (feed : Fin k → Wire n g₁) : Wire k g₂ → Wire n (g₁ + g₂)

The wire of p.append feed q that carries a wire of q: an input of q is the wire of p feeding it, and a gate of q comes after all the gates of p.

Equations

• Cslib.Circuits.Program.appendWire feed = Cslib.Circuits.Wire.elim (fun (i : Fin k) => Cslib.Circuits.Wire.castAdd g₂ (feed i)) fun (j : Fin g₂) => Cslib.Circuits.Wire.gate (Fin.natAdd g₁ j)

@[simp]

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

@[simp]

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

theorem Cslib.Circuits.Program.castAdd_succ_eq_castSucc {n g₁ g₂ : ℕ} (w : Wire n g₁) : Wire.castAdd (g₂ + 1) w = (Wire.castAdd g₂ w).castSucc

theorem Cslib.Circuits.Program.appendWire_castSucc {n k g₁ g₂ : ℕ} (feed : Fin k → Wire n g₁) (w : Wire k g₂) : appendWire feed w.castSucc = (appendWire feed w).castSucc

theorem Cslib.Circuits.Program.appendWire_last {n k g₁ g₂ : ℕ} (feed : Fin k → Wire n g₁) : appendWire feed (Wire.gate (Fin.last g₂)) = Wire.gate (Fin.last (g₁ + g₂))

def Cslib.Circuits.Program.append {σ : Signature} {n k g₁ : ℕ} (p : Program σ n g₁) (feed : Fin k → Wire n g₁) {g₂ : ℕ} : 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.gate line) = (p.append feed q).gate (line.mapWires (Cslib.Circuits.Program.appendWire 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_appendWire {σ : 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 (appendWire 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 := fun (o : Fin p) => Cslib.Circuits.Program.appendWire c.outputs (d.outputs o) }

@[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.