Structural properties and cycle-rank bounds for compiled circuit networks

Complexity/Computability/Circuit/Frontier/Compiler/Network.lean compiles a circuit c with m outputs into a multigraph (Compiler.graph c) and a constraint network (Compiler.network c I Acc), proves exactness and uniqueness of satisfying assignments, and establishes the cut-splicing lemma Compiler.eval_splice.

This file proves the graph-theoretic and counting properties of Compiler.graph c:

• Shape and connectivity. The graph is loopless (loopless), has maximum degree at most r + 1 when gates have fan-in at most r ≥ 2 (maxDegreeLE), and is connected whenever the circuit has one output (connected). Cutting along the connected component of an output vertex shows that an output depending on an input is joined to the vertex of that input (exists_reachable_of_eval_ne).
• Counting. With C consumers, W signals and m outputs, the graph has 2 C edges and W + C + m vertices, so its cycle rank is C - W - m + 1: the number of argument slots minus the number of signals, plus one. A gate of arity k has k slots, so it contributes k - 1 to the cycle rank, and a reachable input contributes -1. Hence, when the graph is connected, its cycle rank is at most (r - 1) s + 1 - |read| for s gates of positive arity and fan-in at most r (cycleRank_add_ncard_read_le). Gates of arity zero, the constants, only lower the cycle rank, so the count charges only the inner gates (Circuit.innerSize). The count holds inside every closed set of vertices, for instance a connected component (cycleRankOn_add_ncard_readIn_le), and the count of the whole graph is its case for the set of all vertices.

Main definitions

• Cslib.Circuits.Frontier.Compiler.InnerGate, Cslib.Circuits.Frontier.Compiler.InnerGateIn: reachable inner gates (positive arity), globally and within a vertex set W.

Main results

• Cslib.Circuits.Frontier.Compiler.loopless, Cslib.Circuits.Frontier.Compiler.connected: the graph is loopless, and connected when the circuit has one output.
• Cslib.Circuits.Frontier.Compiler.connected_of_reachable, Cslib.Circuits.Frontier.Compiler.exists_reachable_of_eval_ne: connectivity from a common vertex; an output depending on an input is joined to its vertex.
• Cslib.Circuits.Frontier.Compiler.maxDegreeLE: for fan-in at most r ≥ 2, the degrees are at most r + 1; for fan-in two the graph is subcubic.
• Cslib.Circuits.Frontier.Compiler.ncard_touching_add_ncard_readIn_le, Cslib.Circuits.Frontier.Compiler.cycleRankOn_add_ncard_readIn_le: the edge and cycle-rank counts inside a closed set of vertices.
• Cslib.Circuits.Frontier.Compiler.cycleRank_add_ncard_read_le: the cycle rank and the number of inputs read add up to at most (r - 1) s + 1, where s counts the inner gates.
• Cslib.Circuits.Frontier.Compiler.card_vertex_le: there are at most 2 r s + 3 m vertices.

References

• R. Ryan Williams, Nonuniform ACC Circuit Lower Bounds
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 14

The shape of the graph

theorem Cslib.Circuits.Frontier.Compiler.loopless {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : (graph c).Loopless

The graph has no loops.

theorem Cslib.Circuits.Frontier.Compiler.ncard_slot_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {r : ℕ} (hfan : c.FanInAtMost r) (w : Wire n c.size) : {a : Slot c | Wire.gate (↑a).fst = w}.ncard ≤ r

A gate has at most r argument slots when the fan-in is at most r.

theorem Cslib.Circuits.Frontier.Compiler.eq_of_feeder_eq_junction {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {j₁ j₂ j : Junction c} : feeder j₁ = Vertex.junction j → feeder j₂ = Vertex.junction j → j₁ = j₂

Two junctions fed by the same junction are equal.

theorem Cslib.Circuits.Frontier.Compiler.maxDegreeLE {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {r : ℕ} (hr : 2 ≤ r) (hfan : c.FanInAtMost r) : (graph c).MaxDegreeLE (r + 1)

The degrees are bounded. When the gates have fan-in at most r ≥ 2, every vertex has degree at most r + 1: a gate vertex has its argument edges and one outgoing edge, a junction has three edges, and input vertices and output vertices have one. For fan-in two the graph is subcubic.

Connectivity

theorem Cslib.Circuits.Frontier.Compiler.reachable_junction_signal {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (w : Signal c) (k : ℕ) (hk : k < fanout c w) : (graph c).toSimpleGraph.Reachable (Vertex.junction ⟨w, ⟨k, hk⟩⟩) (Vertex.signal w)

The junctions of a signal are joined to its vertex along their chain.

theorem Cslib.Circuits.Frontier.Compiler.reachable_junction {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (j : Junction c) : (graph c).toSimpleGraph.Reachable (Vertex.junction j) (Vertex.signal j.fst)

Every junction is joined to the vertex of its signal.

theorem Cslib.Circuits.Frontier.Compiler.reachable_owner {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (t : Consumer c) : (graph c).toSimpleGraph.Reachable (Vertex.signal (consumed t)) (owner t)

The vertex of a signal is joined to each of its consumers.

theorem Cslib.Circuits.Frontier.Compiler.exists_reachable_signal_output {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (w : Signal c) : ∃ (o : Fin m), (graph c).toSimpleGraph.Reachable (Vertex.signal w) (Vertex.output o)

The vertex of every signal is joined to the vertex of some output.

theorem Cslib.Circuits.Frontier.Compiler.exists_reachable_output {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (v : Vertex c) : ∃ (o : Fin m), (graph c).toSimpleGraph.Reachable v (Vertex.output o)

Every vertex is joined to the vertex of some output.

theorem Cslib.Circuits.Frontier.Compiler.connected_of_reachable {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {v₀ : Vertex c} (h : ∀ (o : Fin m), (graph c).toSimpleGraph.Reachable v₀ (Vertex.output o)) : (graph c).toSimpleGraph.Connected

The graph is connected when some vertex is joined to every output vertex.

theorem Cslib.Circuits.Frontier.Compiler.connected {σ : Signature} {n : ℕ} (c : Circuit σ n 1) : (graph c).toSimpleGraph.Connected

The graph of a circuit with one output is connected.

theorem Cslib.Circuits.Frontier.Compiler.exists_reachable_of_eval_ne {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {o : Fin m} {i : Fin n} {x y : Fin n → U} (hxy : ∀ (k : Fin n), k ≠ i → x k = y k) (hne : c.eval I x o ≠ c.eval I y o) : ∃ (hi : Reach c (Wire.input i)), (graph c).toSimpleGraph.Reachable (Vertex.signal ⟨Wire.input i, hi⟩) (Vertex.output o)

An output depending on an input is joined to it. If changing only the input i changes the output o of a circuit, then the input i is read by its network, and its vertex is joined to the vertex of the output o.

Counting

theorem Cslib.Circuits.Frontier.Compiler.read_network {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) : (network c I Acc).read = {i : Fin n | Reach c (Wire.input i)}

The inputs read by the network are the reachable inputs.

theorem Cslib.Circuits.Frontier.Compiler.ncard_readAt_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) (v : Vertex c) : ((network c I Acc).readAt v).ncard ≤ 1

Each vertex reads at most one input.

theorem Cslib.Circuits.Frontier.Compiler.readIn_network {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) (W : Set (Vertex c)) : (network c I Acc).readIn W = {i : Fin n | ∃ (hi : Reach c (Wire.input i)), Vertex.signal ⟨Wire.input i, hi⟩ ∈ W}

The inputs read in a set of vertices are the reachable inputs whose vertex lies in it.

def Cslib.Circuits.Frontier.Compiler.signalEquiv {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Signal c ≃ { i : Fin n // Reach c (Wire.input i) } ⊕ { g : Fin c.size // Reach c (Wire.gate g) }

Signals are reachable inputs and reachable gates.

@[reducible, inline]

abbrev Cslib.Circuits.Frontier.Compiler.InnerGate {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Type

The reachable inner gates: the reachable gates of positive arity.

@[reducible, inline]

abbrev Cslib.Circuits.Frontier.Compiler.InnerGateIn {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (W : Set (Vertex c)) : Type

The reachable inner gates whose vertex lies in W.

theorem Cslib.Circuits.Frontier.Compiler.card_innerGate_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Nat.card (InnerGate c) ≤ c.innerSize

The reachable inner gates are inner gates.

theorem Cslib.Circuits.Frontier.Compiler.card_innerGateIn_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (W : Set (Vertex c)) : Nat.card (InnerGateIn c W) ≤ c.innerSize

The reachable inner gates in W are inner gates.

theorem Cslib.Circuits.Frontier.Compiler.card_innerGate_le_card_gate {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Nat.card (InnerGate c) ≤ Nat.card { g : Fin c.size // Reach c (Wire.gate g) }

There are at least as many reachable gates as reachable inner gates.

theorem Cslib.Circuits.Frontier.Compiler.card_slot_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {r : ℕ} (hfan : c.FanInAtMost r) (W : Set (Vertex c)) : Nat.card { t : Slot c // owner (Sum.inl t) ∈ W } ≤ r * Nat.card (InnerGateIn c W)

There are at most r slots per reachable inner gate in W; constant gates have none.

theorem Cslib.Circuits.Frontier.Compiler.card_edge {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Nat.card (Edge c) = 2 * Nat.card (Consumer c)

There are two edges per consumer.

theorem Cslib.Circuits.Frontier.Compiler.card_vertex {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Nat.card (Vertex c) = Nat.card (Signal c) + Nat.card (Consumer c) + m

There is one vertex per signal, per consumer, and per output.

theorem Cslib.Circuits.Frontier.Compiler.card_consumer {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Nat.card (Consumer c) = Nat.card (Slot c) + m

The consumers are the argument slots of reachable gates and the outputs.

theorem Cslib.Circuits.Frontier.Compiler.card_signal_le_card_consumer {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Nat.card (Signal c) ≤ Nat.card (Consumer c)

Every signal has a consumer, so there are at least as many consumers as signals.

Counting inside a closed set of vertices

Let W be a closed set of vertices, one with no edge leaving it. The edges at W are the feed and deliver edges of the junctions in W; the junctions in W are those of the consumers whose owner is in W, that is, the slots of the gates in W and the outputs in W; and the vertices of W are its signals, junctions, and outputs. A circuit with several outputs may have a disconnected graph, and the count applies to each component.

theorem Cslib.Circuits.Frontier.Compiler.ncard_touching_add_ncard_readIn_le_card_innerGateIn {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) {r : ℕ} (hfan : c.FanInAtMost r) {W : Set (Vertex c)} (hW : (graph c).edgeCut W = ∅) : ((graph c).touching W).ncard + ((network c I Acc).readIn W).ncard ≤ W.ncard + (r - 1) * Nat.card (InnerGateIn c W)

The count inside a closed set, gate by gate. For fan-in at most r, the edges at a closed set of vertices W and the inputs read in W number at most (r - 1) s_W more than the vertices of W, where s_W counts the reachable inner gates in W.

theorem Cslib.Circuits.Frontier.Compiler.ncard_touching_add_ncard_readIn_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) {r : ℕ} (hfan : c.FanInAtMost r) {W : Set (Vertex c)} (hW : (graph c).edgeCut W = ∅) : ((graph c).touching W).ncard + ((network c I Acc).readIn W).ncard ≤ W.ncard + (r - 1) * c.innerSize

The count inside a closed set. For fan-in at most r, the edges at a closed set of vertices W and the inputs read in W number at most (r - 1) s more than the vertices of W, where s counts the inner gates.

theorem Cslib.Circuits.Frontier.Compiler.cycleRankOn_add_ncard_readIn_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) {r : ℕ} (hfan : c.FanInAtMost r) {W : Set (Vertex c)} (hW : (graph c).edgeCut W = ∅) (hconn : W.ncard ≤ ((graph c).touching W).ncard + 1) : (graph c).cycleRankOn W + ((network c I Acc).readIn W).ncard ≤ (r - 1) * c.innerSize + 1

The cycle rank of a closed set. For fan-in at most r, the cycle rank of a closed set of vertices W with at least |W| - 1 edges, for instance a connected component, and the number of inputs read in W add up to at most (r - 1) s + 1, where s counts the inner gates.

Counting in the whole graph

theorem Cslib.Circuits.Frontier.Compiler.card_edge_add_ncard_read_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) {r : ℕ} (hfan : c.FanInAtMost r) : Nat.card (Edge c) + (network c I Acc).read.ncard ≤ Nat.card (Vertex c) + (r - 1) * c.innerSize

The edge count. For fan-in at most r, the edges of the graph and the inputs read by the network number at most (r - 1) s more than the vertices, where s counts the inner gates. This is the count inside the closed set of all vertices.

theorem Cslib.Circuits.Frontier.Compiler.cycleRank_add_ncard_read_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) {r : ℕ} (hfan : c.FanInAtMost r) (hconn : (graph c).toSimpleGraph.Connected) : (graph c).cycleRank + (network c I Acc).read.ncard ≤ (r - 1) * c.innerSize + 1

The cycle rank. For fan-in at most r, if the graph is connected (as it is for one output), its cycle rank and the number of inputs read by the network add up to at most (r - 1) s + 1, where s counts the inner gates.

theorem Cslib.Circuits.Frontier.Compiler.card_vertex_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {r : ℕ} (hfan : c.FanInAtMost r) : Nat.card (Vertex c) ≤ 2 * r * c.innerSize + 3 * m

The number of vertices is at most 2 r s + 3 m for fan-in at most r, where s counts the inner gates and m the outputs.