Reusing circuits in synthesis arguments

A concrete circuit supplies a synthesis bound for its designated outputs. This connects circuit composition with constructions using shared wires.

theorem Cslib.Circuits.Circuit.synthesis {σ : Signature} {U : Type} {n m : ℕ} {I : Interpretation σ U} (c : Circuit σ n m) : Synthesis I (inputs n) (Set.range fun (j : Fin m) (x : Fin n → U) => c.eval I x j) c.size

Rebuild the circuit's outputs within its existing gate budget.

theorem Cslib.Circuits.Circuit.Computes.synthesis {σ : Signature} {U : Type} {n m : ℕ} {I : Interpretation σ U} {c : Circuit σ n m} {f : (Fin n → U) → Fin m → U} (hc : c.Computes I f) : Synthesis I (inputs n) (Set.range fun (j : Fin m) (x : Fin n → U) => f x j) c.size

A circuit computing f supplies a synthesis bound for all coordinates of f.