Layered circuits and depth (ECDLP Phase 2, Stage S1)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

The flat Circuit = List (Gate n) model (Tranche 1) costs only gate count; it cannot express parallelism, so it has no notion of circuit depth (parallel time). This module adds the depth axis: a LayeredCircuit is a list of layers, each layer a group of gates intended to run in one time step (well-formed when their wires are disjoint), and depth is the number of layers.

Two bridges keep the new axis consistent with the verified flat model:

• denoteLayered_eq_denote_flatten — a layered circuit denotes the same map as its flattened gate list, so correctness is inherited from the flat circuits (the Tranche-2/3 _correct theorems).
• layeredToffoli_eq — the Toffoli count is the flattened gate list's, so the verified gate counts carry over unchanged.

What this gives, and what it does not: the framework plus two honest depth facts — a disjoint layer has depth 1 ≪ gate count (parallelism captured), and the ripple adder sequentialised has depth = gate count = 4n = O(n) (its carry chain is inherently sequential). The payoff the framework enables — a parallel-prefix / carry-lookahead adder at O(log n) depth, to compare against the ripple O(n) — is the next increment (S1 continuation), not proved here.

@[reducible, inline]

abbrev Reversible.LayeredCircuit (n : ℕ) : Type

A layered circuit: a list of layers, each layer a Circuit (group of gates) run in one parallel time step. depth is the number of layers.

Equations

• Reversible.LayeredCircuit n = List (Reversible.Circuit n)

def Reversible.denoteLayered {n : ℕ} (lc : LayeredCircuit n) (s : State n) : State n

Run a layered circuit: apply each layer in order.

Equations

• Reversible.denoteLayered lc s = List.foldl (fun (s : Reversible.State n) (layer : Reversible.Circuit n) => Reversible.denote layer s) s lc

def Reversible.flatten {n : ℕ} (lc : LayeredCircuit n) : Circuit n

Flatten a layered circuit to a flat gate list (layers concatenated in order).

Equations

• Reversible.flatten lc = List.flatMap id lc

def Reversible.depth {n : ℕ} (lc : LayeredCircuit n) : ℕ

The depth of a layered circuit: the number of layers (parallel time steps).

Equations

• Reversible.depth lc = List.length lc

theorem Reversible.denoteLayered_eq_denote_flatten {n : ℕ} (lc : LayeredCircuit n) (s : State n) : denoteLayered lc s = denote (flatten lc) s

Denotation bridge. A layered circuit computes the same state map as its flattened gate list, so the flat-model correctness theorems (rippleCirc_correct, mulCircuit_correct, …) transfer to any layering of the same gates.

theorem Reversible.layeredToffoli_eq {n : ℕ} (lc : LayeredCircuit n) : (circuitCost (flatten lc)).toffoli = (List.map (fun (layer : Circuit n) => (circuitCost layer).toffoli) lc).sum

Toffoli bridge. The Toffoli count of a layered circuit is the sum of its layers' counts (equal to the flattened gate list's), so the verified Tranche-1/3 gate counts carry over to the layered model.

Layer well-formedness (a layer is genuinely parallel iff its gates are wire-disjoint)

def Reversible.LayerWF {n : ℕ} (layer : Circuit n) : Prop

A layer is well-formed (a valid single parallel time step) when its gates act on pairwise disjoint wires. Depth is physically meaningful for layered circuits whose every layer is well-formed.

Equations

• Reversible.LayerWF layer = List.Pairwise (fun (g h : Reversible.Gate n) => Disjoint (Reversible.gateWires g) (Reversible.gateWires h)) layer

theorem Reversible.layerWF_iff {n : ℕ} (layer : Circuit n) : LayerWF layer ↔ List.Pairwise (fun (g h : Gate n) => Disjoint (gateWires g) (gateWires h)) layer

Layer well-formedness, as its defining pairwise-disjointness (interface lemma, §9.1).

def Reversible.LayeredWF {n : ℕ} (lc : LayeredCircuit n) : Prop

A layered circuit is well-formed when every layer is.

Equations

• Reversible.LayeredWF lc = ∀ layer ∈ lc, Reversible.LayerWF layer

Sequentialisation, and the ripple adder's O(n) depth

def Reversible.sequential {n : ℕ} (c : Circuit n) : LayeredCircuit n

The trivial layering: one gate per layer (fully sequential). Always well-formed (singleton layers), with depth = gate count. The depth a circuit needs if no parallelism is exploited.

Equations

• Reversible.sequential c = List.map (fun (g : Reversible.Gate n) => [g]) c

@[simp]

theorem Reversible.sequential_flatten {n : ℕ} (c : Circuit n) : flatten (sequential c) = c

@[simp]

theorem Reversible.sequential_depth {n : ℕ} (c : Circuit n) : depth (sequential c) = List.length c

theorem Reversible.sequential_wf {n : ℕ} (c : Circuit n) : LayeredWF (sequential c)

theorem Reversible.sequential_rippleCirc_correct {n m : ℕ} (L : RippleLayout m n) (s : State m) : denoteLayered (sequential (rippleCirc L)) s = denote (rippleCirc L) s

The ripple adder, fully sequentialised, denotes the verified rippleCirc (correctness inherited).

theorem Reversible.ripplePrefix_length {n m : ℕ} (L : RippleLayout m n) (k : ℕ) : List.length (ripplePrefix L k) = 4 * k

The first k slices of a ripple adder have 4k gates (four per slice).

theorem Reversible.rippleCirc_length {n m : ℕ} (L : RippleLayout m n) : List.length (rippleCirc L) = 4 * n

The ripple adder has 4n gates.

theorem Reversible.rippleCirc_sequential_depth {n m : ℕ} (L : RippleLayout m n) : depth (sequential (rippleCirc L)) = 4 * n

Ripple adder depth is O(n) (= 4n): its carry chain is inherently sequential, so sequentialising gate-by-gate is the natural layering and gives depth equal to the gate count. (Beating this to O(log n) needs a parallel-prefix / carry-lookahead adder — the comparison this framework enables, deferred to the S1 continuation.)

Parallelism captured: a disjoint layer has depth 1, far below its gate count

theorem Reversible.parallelXLayer_depth {n : ℕ} (idxs : List (Fin n)) : depth [List.map Gate.X idxs] = 1

A single layer of X-flips has depth 1, while its gate count is the number of flips — the smallest witness that the depth model is non-trivial (depth can be far below gate count).

theorem Reversible.parallelXLayer_wf {n : ℕ} (idxs : List (Fin n)) (h : idxs.Nodup) : LayeredWF [List.map Gate.X idxs]

That layer is well-formed (a genuine parallel step) when the wires are distinct: the X-flips act on disjoint wires and commute.

Log-depth computation: a parallel reduction tree (the CLA building block)

parallelXLayer shows depth 1 for independent flips, but that is not a computation. A genuine log-depth result is a reduction tree: combine n bits pairwise in a balanced tree, ⌈log₂ n⌉ layers, each layer a set of wire-disjoint gates. Below is the concrete 4-wire instance (depth 2 = log₂ 4), fully verified: every layer is well-formed (parallel), it computes the XOR (parity) of all four inputs into wire 0, and it does so in depth 2 against 3 gates — log depth, not linear. This is the primitive a carry-lookahead adder is built from (the carry prefix is a reduction tree); the general 2^k-wire tree, the full O(log n) carry-lookahead adder, and the secp256k1 (Toffoli, depth, qubits) triple are the further S1/Phase-2 steps.

def Reversible.reduceTree4 : LayeredCircuit 4

A balanced XOR reduction tree on 4 wires: two layers of wire-disjoint CNOTs accumulating the parity of all four bits into wire 0. Depth 2 = log₂ 4, 3 gates.

Equations

• Reversible.reduceTree4 = [[Reversible.Gate.CX 1 0, Reversible.Gate.CX 3 2], [Reversible.Gate.CX 2 0]]

theorem Reversible.reduceTree4_depth : depth reduceTree4 = 2

The reduction tree has depth 2 (= log₂ 4), below its 3-gate count.

theorem Reversible.reduceTree4_gateCount : List.length (flatten reduceTree4) = 3

It has 3 gates — so depth 2 < 3, logarithmic depth for a real computation (the gap widens to log₂ n vs n−1 at scale).

theorem Reversible.reduceTree4_wf : LayeredWF reduceTree4

Every layer is well-formed: the CNOTs in each layer act on disjoint wires (a valid parallel step), so the depth-2 count is physically meaningful, not three sequential steps in disguise.

theorem Reversible.reduceTree4_correct (s : State 4) : denoteLayered reduceTree4 s 0 = (s 0 ^^ s 1 ^^ s 2 ^^ s 3)

Correctness: the tree computes the XOR (parity) of all four input bits into wire 0, in depth 2. (Verified over all 2^4 input states.)