The graph and constraint network of a circuit

Fix a circuit c with m outputs over any signature, an interpretation I of the signature in an alphabet U, and for each output o a set Acc o ⊆ U of accepting values. We build a constraint network (Compiler.network c I Acc) whose accepted inputs are exactly those on which every output o of the circuit lies in Acc o. A circuit deciding a set has one output; a circuit computing a function accepts every value at each of its outputs.

Only the reachable wires matter: the outputs and, recursively, the wires read by reachable gates (Reach). We call them signals (Signal). A signal is consumed by each argument slot of a reachable gate that reads it (Slot), and each output is also consumed by its own output vertex (Consumer). A circuit has unbounded fan-out, but a network of bounded degree cannot give a signal one edge per consumer. So each signal w with consumers t₀, t₁, ... is routed through a chain of junctions (Junction) j₀, j₁, ..., one per consumer:

  w --- j₀ --- j₁ --- j₂ --- ...
        |      |      |
        t₀     t₁     t₂

Each junction has one feed edge from its predecessor in the chain (the signal itself for j₀) and one deliver edge to its consumer. The constraints are:

• the vertex of an input x_i reads x_i and puts it on its outgoing edge;
• the vertex of a gate g puts g applied to its incoming argument edges on its outgoing edge;
• a junction puts its incoming value on both of its outgoing edges;
• the vertex of the output o requires its incoming value to lie in Acc o.

Exactness (Compiler.satisfies_iff). The values of the circuit satisfy the network. Conversely, in a satisfying assignment the junction constraints force all edges of a signal to carry one value, and the gate constraints, read in program order, force that value to be the value of the signal in the circuit (Compiler.eq_trace). So the satisfying assignment, if any, is unique, and along any layout the read-once branching program of the network (Cslib.Circuits.Frontier.Network.branchingProgram) is unambiguous (Compiler.unambiguous_branchingProgram).

Outputs across a cut. If the runs of the circuit on two inputs x and y agree on the edge cut of a set of vertices P, the separator lemma splices them: on an input that reads like x at P and like y elsewhere, the outputs held in P are those of x and the others are those of y (Compiler.eval_splice).

Graph-theoretic properties (looplessness, degree bounds, connectivity) and cycle-rank / read-count inequalities are proved in Complexity/Computability/Circuit/Frontier/Compiler.lean.

Main definitions

• Cslib.Circuits.Frontier.Compiler.Reach, Cslib.Circuits.Frontier.Compiler.Signal, Cslib.Circuits.Frontier.Compiler.Slot, Cslib.Circuits.Frontier.Compiler.Consumer, Cslib.Circuits.Frontier.Compiler.Junction: reachable wires, argument slots, consumers, and fan-out junctions.
• Cslib.Circuits.Frontier.Compiler.Vertex, Cslib.Circuits.Frontier.Compiler.Edge, Cslib.Circuits.Frontier.Compiler.graph: the multigraph of a circuit.
• Cslib.Circuits.Frontier.Compiler.network: the constraint network of a circuit.

Main results

• Cslib.Circuits.Frontier.Compiler.satisfies_iff, Cslib.Circuits.Frontier.Compiler.accepted_network, Cslib.Circuits.Frontier.Compiler.satisfies_unique: exactness and uniqueness of satisfying assignments.
• Cslib.Circuits.Frontier.Compiler.unambiguous_branchingProgram: the branching program of every layout is unambiguous.
• Cslib.Circuits.Frontier.Compiler.eval_splice: splicing outputs across a vertex cut.

References

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

Signals, consumers, and junctions

inductive Cslib.Circuits.Frontier.Compiler.Reach {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Wire n c.size → Prop

A wire of a circuit is reachable when it is an output or is read by a reachable gate.

• output {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (o : Fin m) : Reach c (c.outputs o)

  The outputs are reachable.

• arg {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {g : Fin c.size} (a : Fin (σ.Arity (c.program.lines g).op)) : Reach c (Wire.gate g) → Reach c ((c.program.lines g).wires a)

  The wires read by a reachable gate are reachable.

@[reducible, inline]

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

The signals of a circuit: its reachable wires.

@[reducible, inline]

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

An argument slot of a reachable gate.

@[reducible, inline]

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

A consumer: an argument slot of a reachable gate, or an output.

def Cslib.Circuits.Frontier.Compiler.consumed {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Consumer c → Signal c

The signal read by a consumer.

noncomputable def Cslib.Circuits.Frontier.Compiler.fanout {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (w : Signal c) : ℕ

The number of consumers of a signal.

@[reducible, inline]

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

A junction: a copy of a signal for one of its consumers. The junctions of a signal w are numbered 0, ..., fanout c w - 1.

noncomputable def Cslib.Circuits.Frontier.Compiler.junctionEquiv {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Junction c ≃ Consumer c

Junctions correspond to consumers.

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.consumed_junctionEquiv {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (j : Junction c) : consumed ((junctionEquiv c) j) = j.fst

The consumer of a junction reads the signal of the junction.

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.fst_junctionEquiv_symm {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (t : Consumer c) : ((junctionEquiv c).symm t).fst = consumed t

The junction of a consumer belongs to the signal it reads.

theorem Cslib.Circuits.Frontier.Compiler.fanout_pos {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (w : Signal c) : 0 < fanout c w

Every signal has a consumer.

The graph

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

The vertices: one per signal, one per junction, and one per output.

• signal {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (w : Signal c) : Vertex c

  The vertex of a signal: an input vertex or a gate vertex.

• junction {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (j : Junction c) : Vertex c

  A junction.

• output {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (o : Fin m) : Vertex c

  The vertex of an output, which consumes it.

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

The edges: two per junction.

• feed {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (j : Junction c) : Edge c

  The edge into a junction from its predecessor in the chain.

• deliver {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (j : Junction c) : Edge c

  The edge from a junction to its consumer.

def Cslib.Circuits.Frontier.Compiler.Vertex.equiv {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Vertex c ≃ Signal c ⊕ Junction c ⊕ Fin m

Vertices are signals, junctions, and outputs.

def Cslib.Circuits.Frontier.Compiler.Edge.equiv {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Edge c ≃ Junction c ⊕ Junction c

Edges are two copies of the junctions.

instance Cslib.Circuits.Frontier.Compiler.instFiniteVertex {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Finite (Vertex c)

instance Cslib.Circuits.Frontier.Compiler.instFiniteEdge {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Finite (Edge c)

def Cslib.Circuits.Frontier.Compiler.owner {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Consumer c → Vertex c

The vertex that consumes through a consumer: a gate vertex or an output vertex.

def Cslib.Circuits.Frontier.Compiler.feeder {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Junction c → Vertex c

The vertex feeding a junction: the signal itself for its first junction, and the previous junction of the chain otherwise.

theorem Cslib.Circuits.Frontier.Compiler.feeder_ne_junction {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (j : Junction c) : feeder j ≠ Vertex.junction j

No junction feeds itself.

def Cslib.Circuits.Frontier.Compiler.src {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Edge c → Vertex c

The source of an edge.

noncomputable def Cslib.Circuits.Frontier.Compiler.tgt {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Edge c → Vertex c

The target of an edge.

def Cslib.Circuits.Frontier.Compiler.Edge.signal {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : Edge c → Signal c

The signal carried by an edge.

noncomputable def Cslib.Circuits.Frontier.Compiler.graph {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Multigraph (Vertex c) (Edge c)

The graph of a circuit: the signals, junctions and outputs, joined by the feed and deliver edges of the junctions.

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.graph_src {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : (graph c).src = src

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.graph_tgt {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : (graph c).tgt = tgt

noncomputable def Cslib.Circuits.Frontier.Compiler.deliverEdge {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (t : Consumer c) : Edge c

The edge delivering a signal to one of its consumers.

@[reducible, inline]

noncomputable abbrev Cslib.Circuits.Frontier.Compiler.argEdge {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {g : Fin c.size} (hg : Reach c (Wire.gate g)) (a : Fin (σ.Arity (c.program.lines g).op)) : Edge c

The edge delivering argument a to the reachable gate g.

@[reducible, inline]

noncomputable abbrev Cslib.Circuits.Frontier.Compiler.outEdge {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (o : Fin m) : Edge c

The edge delivering an output to its output vertex.

def Cslib.Circuits.Frontier.Compiler.head {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (w : Signal c) : Edge c

The first edge of a signal: the feed edge of its first junction.

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.signal_deliverEdge {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (t : Consumer c) : (deliverEdge t).signal = consumed t

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.tgt_deliverEdge {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (t : Consumer c) : tgt (deliverEdge t) = owner t

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.src_head {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (w : Signal c) : src (head w) = Vertex.signal w

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.signal_head {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (w : Signal c) : (head w).signal = w

theorem Cslib.Circuits.Frontier.Compiler.eq_head_of_src_eq_signal {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {e : Edge c} {w : Signal c} : src e = Vertex.signal w → e = head w

An edge leaving the vertex of a signal is the first edge of that signal.

theorem Cslib.Circuits.Frontier.Compiler.signal_of_src_eq_junction {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {e : Edge c} {j : Junction c} : src e = Vertex.junction j → e.signal = j.fst

An edge leaving a junction carries the signal of the junction.

theorem Cslib.Circuits.Frontier.Compiler.exists_slot_of_tgt_eq_signal {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {e : Edge c} {w : Signal c} (h : tgt e = Vertex.signal w) : ∃ (a : Slot c), Wire.gate (↑a).fst = ↑w ∧ e = deliverEdge (Sum.inl a)

An edge entering the vertex of a signal delivers one of the argument slots of its gate.

theorem Cslib.Circuits.Frontier.Compiler.eq_outEdge_of_tgt_eq_output {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {e : Edge c} {o : Fin m} (h : tgt e = Vertex.output o) : e = outEdge c o

An edge entering the vertex of an output delivers that output.

The network

noncomputable def Cslib.Circuits.Frontier.Compiler.emit {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) : Signal c → (Fin n → U) → (Edge c → U) → U

The value that the vertex of a signal puts on its outgoing edge: the input itself for an input wire, and the operation of the gate applied to its incoming edges for a gate wire.

def Cslib.Circuits.Frontier.Compiler.Constraint {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) : Vertex c → (Fin n → U) → (Edge c → U) → Prop

The constraint at each vertex: the vertex of a signal emits the value of the signal, a junction copies its incoming value onto its outgoing edges, and the vertex of an output requires its incoming value to be accepting.

noncomputable def Cslib.Circuits.Frontier.Compiler.site {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (i : Fin n) : Option (Vertex c)

Each reachable input is read at the vertex of its signal.

theorem Cslib.Circuits.Frontier.Compiler.site_eq_some {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {i : Fin n} {v : Vertex c} (h : site c i = some v) : ∃ (hi : Reach c (Wire.input i)), v = Vertex.signal ⟨Wire.input i, hi⟩

An input is read only at the vertex of its signal.

theorem Cslib.Circuits.Frontier.Compiler.site_of_reach {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {i : Fin n} (hi : Reach c (Wire.input i)) : site c i = some (Vertex.signal ⟨Wire.input i, hi⟩)

A reachable input is read at the vertex of its signal.

noncomputable def Cslib.Circuits.Frontier.Compiler.network {σ : Signature} {n m : ℕ} (c : Circuit σ n m) {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) : Network U (Fin n) (Vertex c) (Edge c)

The constraint network of a circuit, accepting at the output o the values in Acc o.

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.network_toMultigraph {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) : (network c I Acc).toMultigraph = graph c

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.network_site {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} (I : Interpretation σ U) (Acc : Fin m → Set U) : (network c I Acc).site = site c

Exactness

theorem Cslib.Circuits.Frontier.Compiler.satisfies_trace {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} {x : Fin n → U} (hx : ∀ (o : Fin m), c.eval I x o ∈ Acc o) : (network c I Acc).Satisfies x fun (e : Edge c) => c.program.trace I x ↑e.signal

The values of the circuit satisfy the network: every edge carries the value of its signal.

theorem Cslib.Circuits.Frontier.Compiler.feed_eq_head {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} {x : Fin n → U} {α : Edge c → U} (hα : (network c I Acc).Satisfies x α) (w : Signal c) (k : ℕ) (hk : k < fanout c w) : α (Edge.feed ⟨w, ⟨k, hk⟩⟩) = α (head w)

In a satisfying assignment, the feed edges along the chain of junctions of a signal carry the value of its first edge.

theorem Cslib.Circuits.Frontier.Compiler.eq_head {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} {x : Fin n → U} {α : Edge c → U} (hα : (network c I Acc).Satisfies x α) (e : Edge c) : α e = α (head e.signal)

In a satisfying assignment, every edge carries the value of the first edge of its signal.

theorem Cslib.Circuits.Frontier.Compiler.head_eq_trace {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} {x : Fin n → U} {α : Edge c → U} (hα : (network c I Acc).Satisfies x α) (w : Wire n c.size) (hw : Reach c w) : α (head ⟨w, hw⟩) = c.program.trace I x w

In a satisfying assignment, the first edge of every signal carries its value in the circuit.

theorem Cslib.Circuits.Frontier.Compiler.eq_trace {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} {x : Fin n → U} {α : Edge c → U} (hα : (network c I Acc).Satisfies x α) (e : Edge c) : α e = c.program.trace I x ↑e.signal

Uniqueness. A satisfying assignment puts on every edge the value of its signal in the circuit.

theorem Cslib.Circuits.Frontier.Compiler.satisfies_iff {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} {x : Fin n → U} {α : Edge c → U} : (network c I Acc).Satisfies x α ↔ (∀ (o : Fin m), c.eval I x o ∈ Acc o) ∧ α = fun (e : Edge c) => c.program.trace I x ↑e.signal

Exactness. An assignment satisfies the network exactly when every output of the circuit is accepted and the assignment puts on every edge the value of its signal in the circuit.

theorem Cslib.Circuits.Frontier.Compiler.accepted_network {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} : (network c I Acc).accepted = {x : Fin n → U | ∀ (o : Fin m), c.eval I x o ∈ Acc o}

Exactness. The network accepts exactly the inputs on which every output o of the circuit lies in Acc o.

theorem Cslib.Circuits.Frontier.Compiler.satisfies_unique {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} {x : Fin n → U} {α β : Edge c → U} (hα : (network c I Acc).Satisfies x α) (hβ : (network c I Acc).Satisfies x β) : α = β

Uniqueness. An input has at most one satisfying assignment.

theorem Cslib.Circuits.Frontier.Compiler.unambiguous_branchingProgram {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {Acc : Fin m → Set U} (π : Layout (Vertex c)) : ((network c I Acc).branchingProgram π).Unambiguous

The branching program of the network along any layout is unambiguous.

Outputs across a cut

theorem Cslib.Circuits.Frontier.Compiler.eval_splice {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {U : Type u_1} {I : Interpretation σ U} {P : Set (Vertex c)} {x y z : Fin n → U} (hcut : ∀ e ∈ (graph c).edgeCut P, c.program.trace I x ↑e.signal = c.program.trace I y ↑e.signal) (hzx : Set.EqOn z x ((network c I fun (x : Fin m) => Set.univ).readIn P)) (hzy : Set.EqOn z y ((network c I fun (x : Fin m) => Set.univ).readIn P)ᶜ) (o : Fin m) : (Vertex.output o ∈ P → c.eval I z o = c.eval I x o) ∧ (Vertex.output o ∉ P → c.eval I z o = c.eval I y o)

Outputs across a cut. In the network of a circuit computing a function, let the runs on two inputs x and y agree on the edge cut of a set of vertices P, and let z read like x at P and like y elsewhere. Then the outputs of z are those of x at the output vertices in P, and those of y at the others.