Documentation

Complexitylib.Circuits.Frontier.Ledger.Count

Counting inside a closed set of vertices #

The count of the compiler (Frontier.Compiler.card_edge_add_ncard_read_le) holds inside every closed set of vertices W of the network of a program, that is, every set with no edge leaving it. The edges at W and the inputs read in W number at most (r - 1) s more than the vertices of W, for s inner gates of fan-in at most r. So the cycle rank of W and the number of inputs it reads add up to at most (r - 1) s + 1.

Inside W: the edges 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.

Main results #

source
@[reducible, inline]
abbrev Complexity.Frontier.Compiler.InnerGateIn {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (W : Set (Vertex p out)) :
Type

The reachable inner gates whose vertex lies in W.

Equations
Instances For
    source
    theorem Complexity.Frontier.Compiler.readIn_network {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} {U : Type u_2} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) (W : Set (Vertex p out)) :
    (network p out I Acc).readIn W = {i : Fin n | ∃ (hi : Reach p out (Cslib.Circuits.Wire.input i)), Vertex.signal ⟨Cslib.Circuits.Wire.input i, hi⟩ ∈ W}

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

    source
    theorem Complexity.Frontier.Compiler.card_touching_add_ncard_readIn_le_local {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} {U : Type u_2} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) {r : ℕ} (hfan : p.FanInAtMost r) {W : Set (Vertex p out)} (hW : (network p out I Acc).cut W = ∅) :
    ((network p out I Acc).touching W).ncard + ((network p out I Acc).readIn W).ncard ≤ W.ncard + (r - 1) * Nat.card (InnerGateIn W)

    The local count inside a closed set. Only the inner gates in W are charged.

    source
    theorem Complexity.Frontier.Compiler.cycleRankOn_add_ncard_readIn_le_local {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} {U : Type u_2} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) {r : ℕ} (hfan : p.FanInAtMost r) {W : Set (Vertex p out)} (hW : (network p out I Acc).cut W = ∅) (hconn : W.ncard ≤ ((network p out I Acc).touching W).ncard + 1) :
    (network p out I Acc).cycleRankOn W + ((network p out I Acc).readIn W).ncard ≤ (r - 1) * Nat.card (InnerGateIn W) + 1

    The local cycle count. A connected component pays only for its own inner gates.

    source
    theorem Complexity.Frontier.Compiler.card_touching_add_ncard_readIn_le {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} {U : Type u_2} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) {r : ℕ} (hfan : p.FanInAtMost r) {W : Set (Vertex p out)} (hW : (network p out I Acc).cut W = ∅) :
    ((network p out I Acc).touching W).ncard + ((network p out I Acc).readIn W).ncard ≤ W.ncard + (r - 1) * p.innerGates.card

    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.

    source
    theorem Complexity.Frontier.Compiler.cycleRankOn_add_ncard_readIn_le {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} {U : Type u_2} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) {r : ℕ} (hfan : p.FanInAtMost r) {W : Set (Vertex p out)} (hW : (network p out I Acc).cut W = ∅) (hconn : W.ncard ≤ ((network p out I Acc).touching W).ncard + 1) :
    (network p out I Acc).cycleRankOn W + ((network p out I Acc).readIn W).ncard ≤ (r - 1) * p.innerGates.card + 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.