Depth of the CSLib circuit bridge

CSLib measures depth by Program.wireDepths: inputs have depth zero and every gate, including negations and constants, adds one. Its circuit depth Cslib.Circuits.Circuit.depth is the largest depth of a designated output wire, so outputs are free. Our Circuit.wireDepth also gives inputs depth zero and adds one per gate, while Circuit.depth charges one more layer for the output gates.

The translation Circuit.ofCslib replaces each CSLib line by one gate reading the same wires (or the first input, for constants), so it preserves every wire depth exactly, and its output gates add exactly one layer.

The converse translation Circuit.toCslib is a dual-rail construction: CSLib gates 0, …, N - 1 negate the inputs, each of our gates becomes a positive and a negative rail (the negative one by De Morgan, from the complementary rails), and each output gate becomes one CSLib gate. It has size exactly N + 2G + M, and every rail sits at most one layer above our wire, so depth grows by at most one. The two directions pin the depth class DEPTH down in CSLib terms up to an additive constant.

Both constructions reason about wire numbers in our layout Fin (N + g), which is CSLib's numbering Wire.index, and reach CSLib's inductive wires through StraightLine.wireOfIndex. They build and bound CSLib programs with Program.ofLines and Program.wireDepths_le from Complexitylib.Cslib.Circuit.Program.

Main results

• Complexity.Circuit.wireDepth_ofCslib — wire depths agree
• Complexity.Circuit.depth_ofCslib — ofCslib adds exactly one layer
• Complexity.Circuit.eval_toCslib, Complexity.Circuit.depth_toCslib_le — the dual-rail simulation is correct and adds at most one layer
• Complexity.Circuit.exists_cslib_depth_le — every fan-in-two AND/OR circuit has a CSLib circuit of size N + 2G + M and depth at most one more
• Complexity.exists_cslib_of_mem_DEPTH, Complexity.mem_DEPTH_of_cslib — DEPTH d versus CSLib circuits of depth d + 1

theorem Complexity.Circuit.ofCslibGate_depth {N g : ℕ} [NeZero N] (l : Cslib.Circuits.Line Cslib.Circuits.Boolean.signature N g) (d : Fin (N + g) → ℕ) (e : Cslib.Circuits.Wire N g → ℕ) (h0 : d firstWire = 0) (hl : ∀ (a : Fin (Cslib.Circuits.Boolean.signature.Arity l.op)), d (l.wires a).index = e (l.wires a)) : 1 + Fin.foldl (ofCslibGate l).fanIn (fun (acc : ℕ) (k : Fin (ofCslibGate l).fanIn) => max acc (d ((ofCslibGate l).inputs k))) 0 = l.depth e

The gate simulating a CSLib line has the line's depth, given matching depths on the wires it reads and depth zero on the first input.

theorem Complexity.Circuit.wireDepth_natAdd {N M : ℕ} [NeZero N] [NeZero M] {G : ℕ} (c : Circuit Basis.andOr2 N M G) (k : Fin G) : c.wireDepth (Fin.natAdd N k) = 1 + Fin.foldl (c.gates k).fanIn (fun (acc : ℕ) (a : Fin (c.gates k).fanIn) => max acc (c.wireDepth ((c.gates k).inputs a))) 0

The depth of our gate wire N + k unfolds to one more than its inputs'.

theorem Complexity.Circuit.wireDepth_ofCslib {N M : ℕ} [NeZero N] [NeZero M] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M) (w : Cslib.Circuits.Wire N c.size) : (ofCslib c).wireDepth w.index = c.program.wireDepths w

Wire depths agree. Every wire of the translation has the CSLib depth of the same wire.

theorem Complexity.Circuit.outputDepth_ofCslib {N M : ℕ} [NeZero N] [NeZero M] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M) (j : Fin M) : (ofCslib c).outputDepth j = c.outputDepths j + 1

Each output gets one extra layer. Output gate j of the translation sits one layer above CSLib's output wire j.

theorem Complexity.Circuit.depth_ofCslib {N M : ℕ} [NeZero N] [NeZero M] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M) : (ofCslib c).depth = c.depth + 1

Circuit depth grows by exactly one. The translation of a CSLib circuit has depth one more than the CSLib circuit, the extra layer being our output gates.

def Complexity.Circuit.litIdx (N w : ℕ) (b : Bool) : ℕ

The wire of the dual-rail CSLib simulation carrying the literal b ⊕ w: input i and its negation sit at wires i and N + i, and our gate wire w ≥ N and its negation at wires 2w and 2w + 1.

Equations

• Complexity.Circuit.litIdx N w b = if w < N then if b = true then N + w else w else 2 * w + if b = true then 1 else 0

theorem Complexity.Circuit.litIdx_lt {N w k : ℕ} (b : Bool) (hw : w < N + k) : litIdx N w b < 2 * N + 2 * k

Literals of wires below N + k sit below wire 2N + 2k.

def Complexity.Circuit.opIsAnd : AndOrOp → Bool

Whether a fan-in-two AND/OR operation is an AND.

Equations

• Complexity.Circuit.opIsAnd Complexity.AndOrOp.and = true
• Complexity.Circuit.opIsAnd Complexity.AndOrOp.or = false

def Complexity.Circuit.dualLine {N W j : ℕ} (gt : Gate Basis.andOr2 W) (b : Bool) (h : ∀ (k : Fin gt.fanIn) (b' : Bool), litIdx N (↑(gt.inputs k)) b' < N + j) : Cslib.Circuits.Line Cslib.Circuits.Boolean.signature N j

The CSLib line computing b ⊕ gt from literals of the gate's inputs (by De Morgan when b is true), in a program reading N + j wires.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Circuit.dualLine_eval {N W j : ℕ} (gt : Gate Basis.andOr2 W) (b : Bool) (h : ∀ (k : Fin gt.fanIn) (b' : Bool), litIdx N (↑(gt.inputs k)) b' < N + j) (v : Cslib.Circuits.Wire N j → Bool) (val : Fin W → Bool) (hv : ∀ (w : Fin W) (b' : Bool) (i : Cslib.Circuits.Wire N j), ↑i.index = litIdx N (↑w) b' → v i = (b' ^^ val w)) : Cslib.Circuits.Boolean.interpretation (dualLine gt b h).op (v ∘ (dualLine gt b h).wires) = (b ^^ gt.eval val)

The line dualLine gt b computes b ⊕ gt from correct literal values.

theorem Complexity.Circuit.dualLine_depth_le {N W j : ℕ} (gt : Gate Basis.andOr2 W) (b : Bool) (h : ∀ (k : Fin gt.fanIn) (b' : Bool), litIdx N (↑(gt.inputs k)) b' < N + j) (e : Cslib.Circuits.Wire N j → ℕ) (d : Fin W → ℕ) (he : ∀ (w : Fin W) (b' : Bool) (i : Cslib.Circuits.Wire N j), ↑i.index = litIdx N (↑w) b' → e i ≤ d w + 1) : (dualLine gt b h).depth e ≤ 1 + Fin.foldl gt.fanIn (fun (acc : ℕ) (k : Fin gt.fanIn) => max acc (d (gt.inputs k))) 0 + 1

The line dualLine gt b sits one layer above the literals it reads.

def Complexity.Circuit.dualRailLine {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (j : Fin (N + 2 * G + M)) : Cslib.Circuits.Line Cslib.Circuits.Boolean.signature N ↑j

Line j of the dual-rail simulation of c: first the negated inputs, then each of our gates as a positive and a negative rail, then the output gates.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.Circuit.toCslib {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M

The dual-rail CSLib simulation of c, of size N + 2G + M.

Equations

• c.toCslib = { size := N + 2 * G + M, program := Cslib.Circuits.Program.ofLines (N + 2 * G + M) c.dualRailLine, outputs := fun (o : Fin M) => Cslib.Circuits.Wire.gate ⟨N + 2 * G + ↑o, ⋯⟩ }

@[simp]

theorem Complexity.Circuit.size_toCslib {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) : c.toCslib.size = N + 2 * G + M

The dual-rail simulation has size N + 2G + M.

def Complexity.Circuit.dualRailValue {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (x : BitString N) (j : Fin (N + 2 * G + M)) : Bool

The intended value of each gate of the dual-rail simulation.

Equations

• c.dualRailValue x j = if h1 : ↑j < N then !x ⟨↑j, h1⟩ else if h2 : ↑j < N + 2 * G then (↑j - N) % 2 == 1 ^^ c.wireValue x ⟨N + (↑j - N) / 2, ⋯⟩ else c.eval x ⟨↑j - N - 2 * G, ⋯⟩

theorem Complexity.Circuit.addCases_dualRailValue {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (x : BitString N) (w : Fin (N + G)) (b : Bool) (i : Fin (N + (N + 2 * G + M))) (hi : ↑i = litIdx N (↑w) b) : Fin.addCases x (c.dualRailValue x) i = (b ^^ c.wireValue x w)

Each literal wire of the dual-rail simulation carries its literal.

theorem Complexity.Circuit.program_eval_toCslib {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (x : BitString N) : c.toCslib.program.eval Cslib.Circuits.Boolean.interpretation x = c.dualRailValue x

Every gate of the dual-rail simulation computes its intended value.

theorem Complexity.Circuit.eval_toCslib {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (x : BitString N) (o : Fin M) : c.toCslib.eval Cslib.Circuits.Boolean.interpretation x o = c.eval x o

The dual-rail simulation computes what c computes.

def Complexity.Circuit.dualRailDepth {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (i : Fin (N + (N + 2 * G + M))) : ℕ

The depth certificate of the dual-rail simulation: inputs at depth zero, negated inputs at one, both rails of our wire w at wireDepth w + 1, and output o at outputDepth o + 1.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Circuit.dualRailDepth_le {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (w : Fin (N + G)) (b : Bool) (i : Fin (N + (N + 2 * G + M))) (hi : ↑i = litIdx N (↑w) b) : c.dualRailDepth i ≤ c.wireDepth w + 1

Each literal wire of the dual-rail simulation is certified one layer above its wire.

theorem Complexity.Circuit.wireDepths_toCslib_le {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (w : Cslib.Circuits.Wire N (N + 2 * G + M)) : c.toCslib.program.wireDepths w ≤ c.dualRailDepth w.index

Every wire of the dual-rail simulation meets its depth certificate.

theorem Complexity.Circuit.depth_toCslib_le {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) : c.toCslib.depth ≤ c.depth + 1

The dual-rail simulation adds at most one layer. Its depth is at most one more than the depth of c.

theorem Complexity.Circuit.exists_cslib_depth_le {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) : ∃ (c' : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M), c'.size = N + 2 * G + M ∧ (∀ (x : Fin N → Bool) (j : Fin M), c'.eval Cslib.Circuits.Boolean.interpretation x j = c.eval x j) ∧ c'.depth ≤ c.depth + 1

Our circuits run as CSLib's, with depth control. A fan-in-two AND/OR circuit with G internal gates and M outputs has a CSLib De Morgan circuit of size exactly N + 2G + M computing the same outputs, whose depth is at most one more.

theorem Complexity.exists_cslib_of_mem_DEPTH {d : ℕ → ℕ} {f : BoolFunFamily} (hf : f ∈ DEPTH d) (n : ℕ) : ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature (n + 1) 1), (c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin (n + 1) → Bool) (x_1 : Fin 1) => f (n + 1) x) ∧ c.depth ≤ d (n + 1) + 1

DEPTH d in CSLib terms, forward. A Boolean function family in DEPTH d has, at every positive length n + 1, a CSLib De Morgan circuit computing it with depth at most d (n + 1) + 1.

theorem Complexity.mem_DEPTH_of_cslib {d : ℕ → ℕ} {f : BoolFunFamily} (h : ∀ (n : ℕ) [NeZero n], ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1), (c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) ∧ c.depth ≤ d n) : f ∈ DEPTH fun (n : ℕ) => d n + 1

DEPTH in CSLib terms, backward. If every positive length n has a CSLib De Morgan circuit computing f n with depth at most d n, then f is in DEPTH (d + 1).