Depth as an abstract interpretation

Assigning each operation the successor of the maximum arrival time of its arguments reproduces circuit depth exactly. Pulling this interpretation back through a translation therefore gives exact delay semantics for every source operation gadget.

def Cslib.Circuits.Signature.depthInterpretation (σ : Signature) : Interpretation σ ℕ

The arrival-time interpretation of a signature.

Equations

• σ.depthInterpretation op input = (Fin.foldl (σ.Arity op) (fun (depth : ℕ) (argument : Fin (σ.Arity op)) => max depth (input argument)) 0).succ

theorem Cslib.Circuits.Program.eval_depthInterpretation {σ : Signature} {n g : ℕ} (program : Program σ n g) : (program.eval σ.depthInterpretation fun (x : Fin n) => 0) = program.depths

Evaluating a program in the arrival-time interpretation from time-zero inputs gives its gate depths.

theorem Cslib.Circuits.Program.trace_depthInterpretation {σ : Signature} {n g : ℕ} (program : Program σ n g) : (program.trace σ.depthInterpretation fun (x : Fin n) => 0) = program.wireDepths

Evaluating all program wires in the arrival-time interpretation gives their wire depths.

theorem Cslib.Circuits.Circuit.eval_depthInterpretation {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) : (circuit.eval σ.depthInterpretation fun (x : Fin n) => 0) = circuit.outputDepths

Evaluating a circuit in the arrival-time interpretation gives exactly its designated output depths.

theorem Algebraic.Translation.compile_outputDepths {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) : (translation.compile circuit).outputDepths = circuit.eval (translation.pull τ.depthInterpretation) fun (x : Fin n) => 0

Compiled output depth is exactly source evaluation in the pulled-back target arrival-time interpretation.