Parallel circuits on disjoint inputs

Circuit.parallel runs two circuits on separate input blocks and concatenates their outputs. Both total gate count and arbitrary weighted cost add exactly.

Main definitions

• Cslib.Circuits.Circuit.parallel: run circuits on disjoint input blocks.

Main results

• Cslib.Circuits.Circuit.eval_parallel: evaluation on the two input blocks.
• Cslib.Circuits.Circuit.cost_program_parallel: exact weighted cost.

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

Run two circuits on disjoint input blocks, retaining sharing within each circuit.

@[simp]

theorem Cslib.Circuits.Circuit.eval_parallel {σ : Signature} {U : Type u_1} {n m p q : ℕ} (c : Circuit σ n m) (d : Circuit σ p q) (I : Interpretation σ U) (x : Fin (n + p) → U) : (c.parallel d).eval I x = Fin.append (c.eval I (x ∘ Fin.castAdd p)) (d.eval I (x ∘ Fin.natAdd n))

theorem Cslib.Circuits.Circuit.cost_program_parallel {σ : Signature} {n m p q : ℕ} (c : Circuit σ n m) (d : Circuit σ p q) (cost : σ.Op → ℕ) : (c.parallel d).program.cost cost = c.program.cost cost + d.program.cost cost

Disjoint-input composition adds arbitrary weighted gate cost.

@[simp]

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