The depth of a simulation

Replacing every gate of a program by a circuit computing its operation (Program.simulate) makes each wire at most as deep as its depth in the original program when an operation op costs the depth of its replacement circuit (Program.wireDepths_simulateRenaming_le). So a circuit over one basis is simulated by a circuit over another basis whose depth is bounded by the original depth with these costs (Circuit.depth_simulate_le), at most the original depth times the largest depth of a replacement.

Main results

• Cslib.Circuits.Program.wireDepths_simulateRenaming_le: depths of simulated wires.
• Cslib.Circuits.Circuit.depth_simulate_le: the depth of a simulated circuit.
• Cslib.Circuits.Circuit.exists_simulation_depth_le: simulation with bounds on size and depth.

theorem Cslib.Circuits.Program.wireDepths_simulateRenaming_le {σ : Signature} {τ : Signature} {n g : ℕ} (p : Program σ n g) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) (w : Wire n g) : (p.simulateProgram impl).wireDepths ((p.simulateRenaming impl).apply w) ≤ wireDepthsWith (fun (op : σ.Op) => (impl op).depth) p w

The depth of a simulation: a wire of the simulating program is at most as deep as the original wire, when every operation costs the depth of the circuit replacing it.

theorem Cslib.Circuits.Circuit.depth_simulate_le {σ : Signature} {τ : Signature} {n m : ℕ} (c : Circuit σ n m) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) : (c.simulate impl).depth ≤ depthWith (fun (op : σ.Op) => (impl op).depth) c

The simulated circuit is at most as deep as the original circuit when every operation costs the depth of its replacement.

theorem Cslib.Circuits.Circuit.exists_simulation_depth_le {σ : Signature} {τ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {J : Interpretation τ U} (c : Circuit σ n m) (size depth : σ.Op → ℕ) (h : ∀ (op : σ.Op), ∃ (d : Circuit τ (σ.Arity op) 1), d.Computes J (single (I op)) ∧ d.size ≤ size op ∧ d.depth ≤ depth op) : ∃ (d : Circuit τ n m), d.eval J = c.eval I ∧ d.size ≤ c.program.cost size ∧ d.depth ≤ depthWith depth c

Simulation with bounds on size and depth: if every operation of I is computed under J by a circuit with at most size op gates and depth at most depth op, then every circuit over σ has an equivalent circuit over τ with at most c.program.cost size gates and depth at most c.depthWith depth.