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_signal_le_innerSize, Cslib.Circuits.Frontier.Compiler.card_signal_le: there are at most r s + m (hence at most r * c.size + m) reachable signals.
• 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.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.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.

@[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_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_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_signal_le_innerSize {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {r : ℕ} (hfan : c.FanInAtMost r) : Nat.card (Signal c) ≤ r * c.innerSize + m

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

theorem Cslib.Circuits.Frontier.Compiler.card_signal_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {r : ℕ} (hfan : c.FanInAtMost r) : Nat.card (Signal c) ≤ r * c.size + m

The number of signals is at most r * c.size + m for fan-in at most r.

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 {σ : 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.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.