Documentation

Complexity.Computability.Circuit.Boolean.MassProduction.Pipeline

The composition bound for scheduled line recovery #

Split the inputs of f : BooleanFunction (p + w) into a prefix of p bits and a suffix of w bits, and pack f into copies copies of a line-parity code on K ^ ℓ along an injection place of the prefixes into copies, information points and bit positions. Every bit of every codeword value is a function of w bits, a resource; there are copies * |K| ^ ℓ * b of them. If every function of w bits has a circuit of size L, then t independent copies of f cost the scheduler, one circuit of size L per resource, and an overhead pipelineOverhead for the metadata lookup, scatter, gather and decoding (complexity_directProduct_le_of_isScheduler). The overhead is quasi-linear in 2 ^ p + t |K| + copies |K| ^ ℓ (pipelineOverhead_le), so the resources dominate (complexity_directProduct_le_explicit_of_isScheduler).

Sizes count all gates, constants and negations included. They bound circuit size only and do not certify the running time of a circuit constructor.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.MassProduction.pipelineOverhead (t p w ℓ b s copies : ℕ) :
ℕ

The gates of scheduled recovery beyond the scheduler and the resource circuits, for t requests with p prefix and w suffix bits, copies codes on K ^ ℓ with K of 2 ^ b elements and lines of s points: one shared lookup of 2 ^ p metadata entries, a scatter and a gather between the t * s incidences and the copies * 2 ^ (ℓ * b) slots, and t sums of s bits.

Instances For
    source
    theorem Cslib.Circuits.Boolean.MassProduction.complexity_directProduct_le_of_isScheduler {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b s t p w copies L : ℕ} (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (sched : Circuit signature (t * (ℓ * b)) (t * (s * (ℓ * b)))) (hsched : IsScheduler bits scalar sched) (hL : ∀ (g : BooleanFunction w), complexity interpretation (single g) ≤ L) (f : BooleanFunction (p + w)) :
    complexity interpretation (directProduct f t) ≤ sched.size + copies * Fintype.card K ^ ℓ * b * L + pipelineOverhead t p w ℓ b s copies

    Composition bound for scheduled line recovery. Let place put every prefix of p bits at a copy, an information point and a bit position of copies copies of a line-parity code C on K ^ ℓ, where bits identifies K additively with the bit strings of length b and scalar numbers its nonzero elements. Given a scheduler circuit sched for t requests and a bound L on the circuit size of every function of w bits, t independent copies of any f on p + w bits, each input block read as a prefix followed by a suffix, have circuit size at most the size of sched, plus L for each of the copies * |K| ^ ℓ * b resources, plus pipelineOverhead t p w ℓ b s copies. Requests may repeat, and t may be zero. Size counts every gate, constants included; it does not bound the running time of a circuit constructor.

    source
    theorem Cslib.Circuits.Boolean.MassProduction.pipelineOverhead_le {t p w ℓ b s copies : ℕ} (hs : s + 1 = 2 ^ b) (hℓ : 0 < ℓ) :
    pipelineOverhead t p w ℓ b s copies ≤ 1444 * (2 ^ p + t * (s + 1) + copies * (s + 1) ^ ℓ) * (p + w + ℓ * b + Nat.log 2 (t + copies) + 2) ^ 4

    Closed-form overhead. If s + 1 = 2 ^ b, the field size, and ℓ is positive, the overhead is at most 1444 N D ^ 4, where N = 2 ^ p + t (s + 1) + copies (s + 1) ^ ℓ bounds the numbers of table entries, incidences and slots, and D = p + w + ℓ b + ⌊log₂ (t + copies)⌋ + 2 bounds the key widths and sorting depths.

    source
    theorem Cslib.Circuits.Boolean.MassProduction.complexity_directProduct_le_explicit_of_isScheduler {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b s t p w copies L : ℕ} (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (sched : Circuit signature (t * (ℓ * b)) (t * (s * (ℓ * b)))) (hsched : IsScheduler bits scalar sched) (hL : ∀ (g : BooleanFunction w), complexity interpretation (single g) ≤ L) (f : BooleanFunction (p + w)) :
    complexity interpretation (directProduct f t) ≤ sched.size + copies * Fintype.card K ^ ℓ * b * L + 1444 * (2 ^ p + t * Fintype.card K + copies * Fintype.card K ^ ℓ) * (p + w + ℓ * b + Nat.log 2 (t + copies) + 2) ^ 4

    Explicit composition bound. Under the hypotheses of complexity_directProduct_le_of_isScheduler, t independent copies of f have circuit size at most the size of the scheduler, plus L for each of the copies * |K| ^ ℓ * b resources, plus 1444 N D ^ 4, where N = 2 ^ p + t |K| + copies |K| ^ ℓ and D = p + w + ℓ b + ⌊log₂ (t + copies)⌋ + 2. No positivity is assumed: without requests the bound is trivial, and a scheduler for at least one request forces ℓ > 0. Size counts every gate, constants included; it does not bound the running time of a circuit constructor.