Sweeping a circuit with a ledger

Let a circuit with one output decide a set S, and let its special gates have a ledger in M. Erase the special gates. A wire is live if it is an input or a gate of positive arity of the erased program; the others are constants, among them the placeholders. Compile the erased program with outputs the output of the circuit, accepting the same values, and every live wire, accepting every value. Every live wire is then a signal of the network. For a guess m ∈ M the network of the erased program runs the circuit with the placeholders reading their values from m; its graph and its sites do not depend on m.

The ledger sweep (Frontier.Ledger.sweep) is the sweep along a layout (Frontier.Network.frontierSweep) whose extra message has two parts: the product m of the contributions of the true run (its consistent guess) and the product of the contributions of the signals whose vertices come first (the ledger so far). Two inputs with the same message can be spliced: the network of the erased program with guess m splices their runs (the separator lemma), the two parts of the ledger multiply back to m, because the constant wires contribute the same for every input, and a consistent guess yields the true run (Frontier.Ledger.mem_of_splice).

Transitions. The extra messages take at most |M|^3 pairs of values at each step (Frontier.Ledger.ncard_extra_le). Inside a closed set of vertices W, the values of the run on the edges at W depend only on the guess and the inputs read in W (Frontier.Ledger.run_eq_of_eqOn_readIn), so the transitions inside W are bounded by the inputs that W reads, however wide the layout is there.

The network of the erased program

def Complexity.Frontier.Ledger.Live {σ : Cslib.Circuits.Signature} {n : ℕ} (c : Cslib.Circuits.Circuit σ n 1) (special : ℕ → Prop) (w : Cslib.Circuits.Wire n c.size) : Prop

A wire is live when it is an input or a gate of positive arity of the erased program.

Equations

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

def Complexity.Frontier.Ledger.outs {σ : Cslib.Circuits.Signature} {n : ℕ} (c : Cslib.Circuits.Circuit σ n 1) (special : ℕ → Prop) : Option { w : Cslib.Circuits.Wire n c.size // Live c special w } → Cslib.Circuits.Wire n c.size

The outputs of the erased program: the output of the circuit, and every live wire.

Equations

• Complexity.Frontier.Ledger.outs c special none = c.outputs 0
• Complexity.Frontier.Ledger.outs c special (some w) = ↑w

def Complexity.Frontier.Ledger.accs {U : Type u_1} (Acc : Set U) {α : Type u_3} : Option α → Set U

The accepted values at the outputs of the erased program.

Equations

• Complexity.Frontier.Ledger.accs Acc none = Acc
• Complexity.Frontier.Ledger.accs Acc (some val) = Set.univ

@[reducible, inline]

abbrev Complexity.Frontier.Ledger.Vtx {σ : Cslib.Circuits.Signature} {n : ℕ} (c : Cslib.Circuits.Circuit σ n 1) (special : ℕ → Prop) : Type

The vertices of the network of the erased program.

Equations

• Complexity.Frontier.Ledger.Vtx c special = Complexity.Frontier.Compiler.Vertex (Complexity.Frontier.erase special c.program) (Complexity.Frontier.Ledger.outs c special)

@[reducible, inline]

abbrev Complexity.Frontier.Ledger.Edg {σ : Cslib.Circuits.Signature} {n : ℕ} (c : Cslib.Circuits.Circuit σ n 1) (special : ℕ → Prop) : Type

The edges of the network of the erased program.

Equations

• Complexity.Frontier.Ledger.Edg c special = Complexity.Frontier.Compiler.Edge (Complexity.Frontier.erase special c.program) (Complexity.Frontier.Ledger.outs c special)

@[reducible, inline]

noncomputable abbrev Complexity.Frontier.Ledger.net {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (Acc : Set U) (m : M) : Network U (Fin n) (Compiler.Vertex (erase special c.program) (outs c special)) (Compiler.Edge (erase special c.program) (outs c special))

The network of the erased program with the guess m, accepting the values in Acc at the output of the circuit.

Equations

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

@[reducible, inline]

noncomputable abbrev Complexity.Frontier.Ledger.fnet {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (m : M) : Network U (Fin n) (Compiler.Vertex (erase special c.program) (outs c special)) (Compiler.Edge (erase special c.program) (outs c special))

The network of the erased program with the guess m, accepting every value.

Equations

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

theorem Complexity.Frontier.Ledger.reach_of_live {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {special : ℕ → Prop} {w : Cslib.Circuits.Wire n c.size} (hw : Live c special w) : Compiler.Reach (erase special c.program) (outs c special) w

Live wires are signals.

theorem Complexity.Frontier.Ledger.run_eq_of_not_reach {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (m : M) {w : Cslib.Circuits.Wire n c.size} (hw : ¬Compiler.Reach (erase special c.program) (outs c special) w) (x y : Fin n → U) : L.run m x w = L.run m y w

A wire that is not a signal is a constant gate of the erased program, so its value in a run depends only on the guess.

def Complexity.Frontier.Ledger.wiresIn {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {special : ℕ → Prop} (P : Set (Vtx c special)) : Set (Cslib.Circuits.Wire n c.size)

The wires whose vertices lie in P.

Equations

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

noncomputable def Complexity.Frontier.Ledger.ledgerOn {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (Q : Set (Cslib.Circuits.Wire n c.size)) (v : Cslib.Circuits.Wire n c.size → U) : M

The product of the contributions of the wires in Q.

Equations

• L.ledgerOn Q v = ∏ w : Cslib.Circuits.Wire n c.size with w ∈ Q, L.contribution w (v w)

theorem Complexity.Frontier.Ledger.total_eq_mul {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (Q : Set (Cslib.Circuits.Wire n c.size)) (v : Cslib.Circuits.Wire n c.size → U) : L.total v = L.ledgerOn Q v * L.ledgerOn Qᶜ v

Splicing

theorem Complexity.Frontier.Ledger.satisfies_net {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) {Acc : Set U} {x : Fin n → U} (hx : c.program.trace I x (c.outputs 0) ∈ Acc) : (L.net Acc (L.total (c.program.trace I x))).Satisfies x fun (e : Compiler.Edge (erase special c.program) (outs c special)) => c.program.trace I x ↑e.signal

The true run satisfies the network of its consistent guess.

theorem Complexity.Frontier.Ledger.mem_of_splice {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) {Acc : Set U} {P : Set (Vtx c special)} {x y z : Fin n → U} (hx : c.program.trace I x (c.outputs 0) ∈ Acc) (hy : c.program.trace I y (c.outputs 0) ∈ Acc) (hm : L.total (c.program.trace I x) = L.total (c.program.trace I y)) (hpart : L.ledgerOn (wiresIn P) (c.program.trace I x) = L.ledgerOn (wiresIn P) (c.program.trace I y)) (hcut : Set.EqOn (fun (e : Compiler.Edge (erase special c.program) (outs c special)) => c.program.trace I x ↑e.signal) (fun (e : Compiler.Edge (erase special c.program) (outs c special)) => c.program.trace I y ↑e.signal) ((L.fnet 1).cut P)) (hzx : Set.EqOn z x ((L.fnet 1).readIn P)) (hzy : Set.EqOn z y ((L.fnet 1).readIn P)ᶜ) : c.program.trace I z (c.outputs 0) ∈ Acc

Splicing two inputs with the same message. If the runs of two inputs of S have the same consistent guess, the same ledger on P, and the same values on the cut of P, then the input that reads like the first at P and like the second elsewhere lies in S.

theorem Complexity.Frontier.Ledger.run_eq_of_eqOn_readIn {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (m : M) {W : Set (Vtx c special)} (hW : (L.fnet m).cut W = ∅) {x x' : Fin n → U} (hxx' : Set.EqOn x x' ((L.fnet m).readIn W)) {e : Edg c special} (he : e ∈ (L.fnet m).touching W) : L.run m x ↑(Compiler.Edge.signal e) = L.run m x' ↑(Compiler.Edge.signal e)

Locality inside a closed set. For a fixed guess, the values of the run on the edges at a closed set of vertices W depend only on the inputs read in W.

The sweep

theorem Complexity.Frontier.Ledger.readIn_univ {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (m : M) : (L.fnet m).readIn Set.univ = Set.univ

Every input is read, at its own vertex.

noncomputable def Complexity.Frontier.Ledger.extra {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (π : Layout (Vtx c special)) (t : ℕ) (x : Fin n → U) : M × M

The extra message at time t: the consistent guess and the ledger of the first t vertices. After the last vertex it is empty.

Equations

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

noncomputable def Complexity.Frontier.Ledger.sweep {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) (Acc : Set U) (π : Layout (Vtx c special)) : Sweep {x : Fin n → U | c.program.trace I x (c.outputs 0) ∈ Acc} ((M × M) × (Edg c special → Option U))

The sweep of a circuit with a ledger, along a layout of the network of its erased program: the frontier sweep whose extra message is the guess and the ledger so far.

Equations

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

theorem Complexity.Frontier.Ledger.ncard_extra_le {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) {Acc : Set U} (π : Layout (Vtx c special)) [Finite U] [Finite M] (t : ℕ) : ((fun (x : Fin n → U) => (L.extra π t x, L.extra π (t + 1) x)) '' {x : Fin n → U | c.program.trace I x (c.outputs 0) ∈ Acc}).ncard ≤ Nat.card M ^ 3

The extra messages take at most |M|^3 pairs of values at each step.

theorem Complexity.Frontier.Ledger.ncard_transition_le_closed {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) {Acc : Set U} (π : Layout (Vtx c special)) [Finite U] [Finite M] {t : ℕ} (ht : t < Nat.card (Vtx c special)) {W : Set (Vtx c special)} (hW : (L.fnet 1).cut W = ∅) (hv : (Equiv.symm π) ⟨t, ht⟩ ∈ W) (hC : (L.fnet 1).frontier π t ∪ (L.fnet 1).frontier π (t + 1) ⊆ (L.fnet 1).touching W) : ((L.sweep Acc π).transition t '' {x : Fin n → U | c.program.trace I x (c.outputs 0) ∈ Acc}).ncard ≤ Nat.card M ^ 3 * Nat.card U ^ ((L.fnet 1).readIn W).ncard

Transitions inside a closed set. If the vertex processed at step t lies in a closed set W that contains both frontiers, a transition is determined by the guess, the two ledgers, and the inputs read in W.

theorem Complexity.Frontier.Ledger.ncard_transition_le_width {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) {Acc : Set U} (π : Layout (Vtx c special)) [Finite U] [Finite M] {t : ℕ} (ht : t < Nat.card (Vtx c special)) : ((L.sweep Acc π).transition t '' {x : Fin n → U | c.program.trace I x (c.outputs 0) ∈ Acc}).ncard ≤ Nat.card M ^ 3 * Nat.card U ^ (((L.fnet 1).frontier π t ∪ (L.fnet 1).frontier π (t + 1)).ncard + ((L.fnet 1).readAt ((Equiv.symm π) ⟨t, ht⟩)).ncard)

Transitions by width. A transition is determined by the guess, the two ledgers, the values on the two frontiers, and the input read at the vertex processed.

theorem Complexity.Frontier.Ledger.ncard_transition_last_le {U : Type u_1} {σ : Cslib.Circuits.Signature} {n : ℕ} {c : Cslib.Circuits.Circuit σ n 1} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger c.program I special M) {Acc : Set U} (π : Layout (Vtx c special)) [Finite U] [Finite M] : ((L.sweep Acc π).transition (Nat.card (Vtx c special)) '' {x : Fin n → U | c.program.trace I x (c.outputs 0) ∈ Acc}).ncard ≤ Nat.card M ^ 3

At the last step the transition is determined by the guess and the two ledgers, since every input is read.