Sweeping a program with a ledger

Let the special gates of a program p have a ledger in M, and let p accept the inputs whose value at a wire o lies in a set Acc. Erase the special gates. A wire is live (Frontier.Live) if it is an input or an ordinary gate of positive arity; the others are constants of the erased program, among them the constants replacing the special gates. The live circuit (Frontier.liveCircuit) is the erased program with every live wire as an output. For a guess m ∈ M, the constraint network of the live circuit accepting every value (Frontier.Ledger.network) is satisfied exactly by the run with guess m. Its graph and its sites do not depend on m: they make up the live network (Frontier.liveNetwork), which has no constraints and serves for the frontiers, components and inputs read of every guess.

The ledger sweep (Frontier.Ledger.sweep) is the sweep along a layout of the live network (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 wires whose vertices come first (the ledger so far). Two inputs with the same message can be spliced (Frontier.Ledger.mem_of_splice): the network 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.

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. Along a layout of the components one after another, some step therefore bounds the accepted set both by its width and by the inputs of its component (Frontier.Ledger.exists_ncard_le).

Main definitions

• Cslib.Circuits.Frontier.Live: the live wires of a program with erased special gates.
• Cslib.Circuits.Frontier.liveCircuit: the erased program with every live wire as an output.
• Cslib.Circuits.Frontier.liveNetwork: its graph and sites, as a network without constraints.
• Cslib.Circuits.Frontier.Ledger.network: its constraint network on a guess.
• Cslib.Circuits.Frontier.Ledger.sweep: the sweep of a program with a ledger.

Main results

• Cslib.Circuits.Frontier.Ledger.mem_of_splice: splicing two inputs with the same message.
• Cslib.Circuits.Frontier.Ledger.run_eq_of_eqOn_readIn: locality inside a closed set.
• Cslib.Circuits.Frontier.Ledger.ncard_transition_le_width, Cslib.Circuits.Frontier.Ledger.ncard_transition_le_readIn: transitions by width and by the inputs read in a closed set.
• Cslib.Circuits.Frontier.Ledger.exists_ncard_le: counting along a layout of the components.

The live circuit

def Cslib.Circuits.Frontier.Live {σ : Signature} {n s : ℕ} (p : Program σ n s) (special : Fin s → Prop) : Wire n s → Prop

A wire is live, once the special gates of p are erased, when it is an input or an ordinary gate of positive arity. The other wires are constants of the erased program: the constants replacing the special gates and the gates of arity zero.

noncomputable def Cslib.Circuits.Frontier.liveCircuit {σ : Signature} {n s : ℕ} (p : Program σ n s) (special : Fin s → Prop) [DecidablePred special] : Circuit (σ.withConstants { g : Fin s // special g }) n (Nat.card { w : Wire n s // Live p special w })

The live circuit: the program p with its special gates erased, and with every live wire as an output.

noncomputable def Cslib.Circuits.Frontier.liveNetwork {σ : Signature} {n s : ℕ} (p : Program σ n s) (special : Fin s → Prop) [DecidablePred special] (U : Type u_2) : Network U (Fin n) (Compiler.Vertex (liveCircuit p special)) (Compiler.Edge (liveCircuit p special))

The live network: the graph of the live circuit and the sites of its inputs, without constraints. It does not depend on a ledger or a guess; its frontiers, components and inputs read are those of the network of the live circuit on every guess (Frontier.Ledger.network).

theorem Cslib.Circuits.Frontier.reach_of_live {σ : Signature} {n s : ℕ} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {w : Wire n s} (hw : Live p special w) : Compiler.Reach (liveCircuit p special) w

The live wires are signals of the live circuit.

theorem Cslib.Circuits.Frontier.reach_input {σ : Signature} {n s : ℕ} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] (i : Fin n) : Compiler.Reach (liveCircuit p special) (Wire.input i)

The inputs are signals of the live circuit.

theorem Cslib.Circuits.Frontier.innerSize_liveCircuit {σ : Signature} {n s : ℕ} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] : (liveCircuit p special).innerSize = {g ∈ p.innerGates | ¬special g}.card

The inner gates of the live circuit are the ordinary inner gates.

theorem Cslib.Circuits.Frontier.card_live_le {σ : Signature} {n s : ℕ} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] : Nat.card { w : Wire n s // Live p special w } ≤ n + (liveCircuit p special).innerSize

There are at most n + s' live wires, where s' counts the ordinary inner gates.

theorem Cslib.Circuits.Frontier.read_liveNetwork {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] : (liveNetwork p special U).read = Set.univ

The live network reads every input.

theorem Cslib.Circuits.Frontier.card_vertex_liveCircuit_pos {σ : Signature} {n s : ℕ} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] (hn : 0 < n) : 0 < Nat.card (Compiler.Vertex (liveCircuit p special))

When there are inputs, the graph of the live circuit has a vertex.

def Cslib.Circuits.Frontier.wiresIn {σ : Signature} {n s : ℕ} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] (P : Set (Compiler.Vertex (liveCircuit p special))) : Set (Wire n s)

The wires whose vertices lie in P.

@[reducible, inline]

noncomputable abbrev Cslib.Circuits.Frontier.Ledger.network {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) (m : M) : Network U (Fin n) (Compiler.Vertex (liveCircuit p special)) (Compiler.Edge (liveCircuit p special))

The constraint network of the live circuit on the guess m, accepting every value. Its satisfying assignments are the runs with guess m. Its graph and its sites are those of the live network, whatever the guess.

theorem Cslib.Circuits.Frontier.Ledger.satisfies_network {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) (m : M) (x : Fin n → U) : (L.network m).Satisfies x fun (e : Compiler.Edge (liveCircuit p special)) => L.run m x ↑e.signal

The run with guess m satisfies the network on the guess m.

theorem Cslib.Circuits.Frontier.Ledger.eq_run_of_satisfies {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) {m : M} {x : Fin n → U} {α : Compiler.Edge (liveCircuit p special) → U} (h : (L.network m).Satisfies x α) (e : Compiler.Edge (liveCircuit p special)) : α e = L.run m x ↑e.signal

A satisfying assignment of the network on the guess m is the run with guess m.

theorem Cslib.Circuits.Frontier.Ledger.run_eq_of_not_reach {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) (m : M) {w : Wire n s} (hw : ¬Compiler.Reach (liveCircuit p special) w) (x y : Fin n → U) : L.run m x w = L.run m y w

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

Splicing

theorem Cslib.Circuits.Frontier.Ledger.mem_of_splice {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) {o : Wire n s} {Acc : Set U} {P : Set (Compiler.Vertex (liveCircuit p special))} {x y z : Fin n → U} (hx : p.trace I x o ∈ Acc) (hy : p.trace I y o ∈ Acc) (hm : L.total (p.trace I x) = L.total (p.trace I y)) (hpart : L.totalOn (wiresIn P) (p.trace I x) = L.totalOn (wiresIn P) (p.trace I y)) (hcut : Set.EqOn (fun (e : Compiler.Edge (liveCircuit p special)) => p.trace I x ↑e.signal) (fun (e : Compiler.Edge (liveCircuit p special)) => p.trace I y ↑e.signal) ((liveNetwork p special U).edgeCut P)) (hzx : Set.EqOn z x ((liveNetwork p special U).readIn P)) (hzy : Set.EqOn z y ((liveNetwork p special U).readIn P)ᶜ) : p.trace I z o ∈ Acc

Splicing two inputs with the same message. Let x and y be inputs whose value at the wire o lies in Acc. If their runs have the same consistent guess, the same ledger on the wires of a set of vertices P, and the same values on the edge cut of P, then every input z that reads like x at P and like y elsewhere has its value at o in Acc as well.

theorem Cslib.Circuits.Frontier.Ledger.run_eq_of_eqOn_readIn {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) (m : M) {W : Set (Compiler.Vertex (liveCircuit p special))} (hW : (liveNetwork p special U).edgeCut W = ∅) {x x' : Fin n → U} (hxx' : Set.EqOn x x' ((liveNetwork p special U).readIn W)) {e : Compiler.Edge (liveCircuit p special)} (he : e ∈ (liveNetwork p special U).touching W) : L.run m x ↑e.signal = L.run m x' ↑e.signal

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

noncomputable def Cslib.Circuits.Frontier.Ledger.extra {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) (π : Layout (Compiler.Vertex (liveCircuit p 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 trivial.

noncomputable def Cslib.Circuits.Frontier.Ledger.sweep {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) (o : Wire n s) (Acc : Set U) (π : Layout (Compiler.Vertex (liveCircuit p special))) : Sweep {x : Fin n → U | p.trace I x o ∈ Acc} ((M × M) × (Compiler.Edge (liveCircuit p special) → Option U))

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

theorem Cslib.Circuits.Frontier.Ledger.ncard_extra_le {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) {o : Wire n s} {Acc : Set U} (π : Layout (Compiler.Vertex (liveCircuit p special))) [Finite U] [Finite M] (t : ℕ) : ((fun (x : Fin n → U) => (L.extra π t x, L.extra π (t + 1) x)) '' {x : Fin n → U | p.trace I x o ∈ Acc}).ncard ≤ Nat.card M ^ 3

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

theorem Cslib.Circuits.Frontier.Ledger.ncard_transition_le_width {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) {o : Wire n s} {Acc : Set U} (π : Layout (Compiler.Vertex (liveCircuit p special))) [Finite U] [Finite M] {t : ℕ} (ht : t < Nat.card (Compiler.Vertex (liveCircuit p special))) : ((L.sweep o Acc π).transition t '' {x : Fin n → U | p.trace I x o ∈ Acc}).ncard ≤ Nat.card M ^ 3 * Nat.card U ^ (((liveNetwork p special U).frontier π t ∪ (liveNetwork p special U).frontier π (t + 1)).ncard + ((liveNetwork p special U).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 Cslib.Circuits.Frontier.Ledger.ncard_transition_le_readIn {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) {o : Wire n s} {Acc : Set U} (π : Layout (Compiler.Vertex (liveCircuit p special))) [Finite U] [Finite M] {t : ℕ} (ht : t < Nat.card (Compiler.Vertex (liveCircuit p special))) {W : Set (Compiler.Vertex (liveCircuit p special))} (hW : (liveNetwork p special U).edgeCut W = ∅) (hv : (Equiv.symm π) ⟨t, ht⟩ ∈ W) (hC : (liveNetwork p special U).frontier π t ∪ (liveNetwork p special U).frontier π (t + 1) ⊆ (liveNetwork p special U).touching W) : ((L.sweep o Acc π).transition t '' {x : Fin n → U | p.trace I x o ∈ Acc}).ncard ≤ Nat.card M ^ 3 * Nat.card U ^ ((liveNetwork p special U).readIn W).ncard

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

theorem Cslib.Circuits.Frontier.Ledger.ncard_transition_last_le {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) {o : Wire n s} {Acc : Set U} (π : Layout (Compiler.Vertex (liveCircuit p special))) [Finite U] [Finite M] : ((L.sweep o Acc π).transition (Nat.card (Compiler.Vertex (liveCircuit p special))) '' {x : Fin n → U | p.trace I x o ∈ 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.

theorem Cslib.Circuits.Frontier.Ledger.exists_ncard_le {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) {o : Wire n s} {Acc : Set U} (π : Layout (Compiler.Vertex (liveCircuit p special))) [Finite U] [Nonempty U] [Finite M] {K : ℕ} (hfree : RectangleFree {x : Fin n → U | p.trace I x o ∈ Acc} K) (hK : K ≤ {x : Fin n → U | p.trace I x o ∈ Acc}.ncard) (hV : 0 < Nat.card (Compiler.Vertex (liveCircuit p special))) (hC : ∀ (t : ℕ) (ht : t < Nat.card (Compiler.Vertex (liveCircuit p special))), (liveNetwork p special U).frontier π t ∪ (liveNetwork p special U).frontier π (t + 1) ⊆ (liveNetwork p special U).touching ((liveNetwork p special U).component ((Equiv.symm π) ⟨t, ht⟩))) : ∃ (t : ℕ) (ht : t < Nat.card (Compiler.Vertex (liveCircuit p special))), {x : Fin n → U | p.trace I x o ∈ Acc}.ncard ≤ (K - 1) ^ 2 * (Nat.card (Compiler.Vertex (liveCircuit p special)) + 1) * Nat.card M ^ 3 * Nat.card U ^ min (((liveNetwork p special U).frontier π t ∪ (liveNetwork p special U).frontier π (t + 1)).ncard + ((liveNetwork p special U).readAt ((Equiv.symm π) ⟨t, ht⟩)).ncard) ((liveNetwork p special U).readIn ((liveNetwork p special U).component ((Equiv.symm π) ⟨t, ht⟩))).ncard

Counting along a layout of the components. Suppose that, at each step of a layout, the frontiers lie among the edges of the component of the vertex processed. Then some step t bounds the set accepted by p by (K - 1) ^ 2 (|V| + 1) |M| ^ 3 q ^ e, where q = |U| and the exponent e is the smaller of the width of the step (the two frontiers and the input read) and the number of inputs read in the component of the vertex processed.