The program of the repeated sampler

The sampler of ComputeParrepVerifier (thm:parallel-repetition; planning/repetition-verifier.md, R3(b)) as a program of the ambient model. It is one fixed program repSampCore univ — univ a universal machine — run through the s-m-n construction hardcode on the datum (S̄, λ, τ): its input is then ((S̄, λ, τ), (n, q)), with S̄ the input sampler's program, λ, τ in binary and q a query. It

1. asks S̄ for its dimension s = s(n), through univ;
2. on the dimension query (kind = 0, i.e. nil) runs dimProg: the numeral 2^m s with m = τ (|λ| + |n|), written as m zero bits in front of the bits of s (powBody);
3. on any other query (kind, w, j, u, y) runs lockProg: s in unary, then the block loop mapBody over u and y in blocks of s, and the concatenation of the answers.

Every input of the form ((S̄, λ, τ), (n, d)) halts: the missing components of a malformed d are nil, on which each elim stops with nil. The costs are explicit throughout, for the time bound of the repeated verifier (MIPRE.Foundations.Repeat.SamplerCost).

The dimension branch

def MIPRE.Cost.Prog.dimProg : Prog

On (s, λ, n, τ) — s in binary and nonzero, λ, n bit lists, τ in binary — the bits of 2^{τ (|λ| + |n|)} s; nil when s is nil.

Equations

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

theorem MIPRE.Cost.Prog.dimProg_wellScoped : WellScoped 1 dimProg

theorem MIPRE.Cost.Prog.dimProg_runs_nil (r : Data) : Eval [Data.nil.cons r] dimProg Data.nil 3

def MIPRE.Cost.Prog.toUnaryCost (n : ℕ) : ℕ

The cost of converting a numeral to unary (toUnaryProg_runs).

Equations

• MIPRE.Cost.Prog.toUnaryCost n = (n.size + 2) * ((n + 1) * (4 * n + 14) + 7 * MIPRE.Cost.esize n + 8 * n + 90)

def MIPRE.Cost.Prog.dimCost (tau L Λ N Ssz : ℕ) : ℕ

The cost of dimProg with exponent tau, lists of lengths L and sizes Λ + N, and a numeral of size Ssz.

Equations

• MIPRE.Cost.Prog.dimCost tau L Λ N Ssz = MIPRE.Cost.Prog.toUnaryCost tau + MIPRE.Cost.esize tau + MIPRE.Cost.Prog.powCost tau L (Λ + N + Ssz) + 2 * tau + Λ + N + Ssz + 20

theorem MIPRE.Cost.Prog.dimProg_runs (tau : ℕ) (bl bn : List Data) (h : Data) (l : List Data) : ∃ t ≤ dimCost tau (bl.length + bn.length) (Data.list bl).size (Data.list bn).size (Data.list (h :: l)).size, Eval [(Data.list (h :: l)).cons ((Data.list bl).cons ((Data.list bn).cons (encode tau)))] dimProg (Data.list (List.replicate (tau * (bl.length + bn.length)) Data.nil ++ h :: l)) t

The block branch

def MIPRE.Cost.Prog.lockProg (univ : Prog) : Prog

On (S̄, n, s, kind, w, j, u, y) — s in binary — the concatenation of the answers of S̄ on the blocks of u and y, through univ; nil when s = 0.

Equations

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

theorem MIPRE.Cost.Prog.lockProg_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.lockProg

def MIPRE.Cost.Prog.lockInput (sD nD sz kD wD jD uD yD : Data) : Data

The input of lockProg.

Equations

• MIPRE.Cost.Prog.lockInput sD nD sz kD wD jD uD yD = sD.cons (nD.cons (sz.cons (kD.cons (wD.cons (jD.cons (uD.cons yD))))))

theorem MIPRE.Cost.Prog.lockProg_runs_zero (univ : Prog) (sD nD kD wD jD uD yD : Data) : ∃ t ≤ esize 0 + toUnaryCost 0 + sD.size + nD.size + kD.size + wD.size + jD.size + uD.size + yD.size + 30, Eval [lockInput sD nD (encode 0) kD wD jD uD yD] univ.lockProg Data.nil t

def MIPRE.Cost.Prog.lockCost (s C U Y Z : ℕ) : ℕ

The cost of lockProg at dimension s, context pieces of total size C, vectors of sizes U, Y, and a bound Z on the sizes in the loop.

Equations

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

theorem MIPRE.Cost.Prog.length_chunkPairs_le (s : ℕ) (hs : 0 < s) (l y : List Data) : (Data.chunkPairs s hs l y).length ≤ l.length

theorem MIPRE.Cost.Prog.size_list_flatten_le (L : List (List Data)) (B : ℕ) : (∀ l ∈ L, (Data.list l).size ≤ B + 1) → (Data.list L.flatten).size ≤ L.length * B + 1

theorem MIPRE.Cost.Prog.size_list_mapAcc_le (f : List Data → List Data → Data) (pairs : List (List Data × List Data)) (Tu : ℕ) (hf : ∀ p ∈ pairs, (f p.1 p.2).size ≤ Tu) : (Data.list (mapAcc f pairs [])).size ≤ pairs.length * Tu + 1

theorem MIPRE.Cost.Prog.lockProg_runs {univ : Prog} (hU : WellScoped 1 univ) {s : ℕ} (hs : 0 < s) (sD nD kD wD jD : Data) (u y : List Data) (f : List Data → List Data → Data) (Tu Z : ℕ) (hf : ∀ p ∈ Data.chunkPairs s hs u y, ∃ t ≤ Tu, Eval [mapQuery sD nD kD wD jD (Data.list p.1) (Data.list p.2)] univ (f p.1 p.2) t) (hZ : s + (Data.list u).size + (Data.list y).size + (mapCtx sD nD kD wD jD).size + 1 + u.length * (Tu + 1) + Tu ≤ Z) : ∃ t ≤ lockCost s (mapCtx sD nD kD wD jD).size (Data.list u).size (Data.list y).size Z, Eval [lockInput sD nD (encode s) kD wD jD (Data.list u) (Data.list y)] univ.lockProg (Data.list (List.map (fun (p : List Data × List Data) => (f p.1 p.2).toList) (Data.chunkPairs s hs u y)).flatten) t

lockProg on a nonzero dimension: the block loop, then the reversal.

The core program

def MIPRE.Cost.Prog.coreDispatch (univ : Prog) : Prog

The dispatch on the kind of the query, in the environment coreEnv: dimProg on (s, λ, n, τ) when the kind is nil, lockProg on (S̄, n, s, kind, rest) otherwise.

Equations

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

theorem MIPRE.Cost.Prog.coreDispatch_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 11 univ.coreDispatch

def MIPRE.Cost.Prog.repSampCore (univ : Prog) : Prog

The core of the repeated sampler, before the s-m-n construction: on ((S̄, λ, τ), (n, q)), the dimension of S̄ at n through univ, then the dispatch.

Equations

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

theorem MIPRE.Cost.Prog.repSampCore_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.repSampCore

def MIPRE.Cost.Prog.sampParams (sD lD tD : Data) : Data

The hardcoded datum (S̄, λ, τ).

Equations

• MIPRE.Cost.Prog.sampParams sD lD tD = sD.cons (lD.cons tD)

theorem MIPRE.Cost.Prog.size_encode_dimension : (encode CL.Sampler.Query.dimension).size = 9

The size of the encoded dimension query.

def MIPRE.Cost.Prog.coreEnv (sD lD tD nD d sz : Data) : Env

The environment of the dispatch: the dimension sz, the dimension query, n, the query d, λ, τ, S̄, and the input's spine.

Equations

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

theorem MIPRE.Cost.Prog.repSampCore_prefix {univ : Prog} (hU : WellScoped 1 univ) (sD lD tD nD d : Data) {sz : Data} {td : ℕ} (hdim : Eval [sD.cons (nD.cons (encode CL.Sampler.Query.dimension))] univ sz td) {r : Data} {t : ℕ} (hc : Eval (coreEnv sD lD tD nD d sz) univ.coreDispatch r t) : Eval [(sampParams sD lD tD).cons (nD.cons d)] univ.repSampCore r (t + td + 2 * (sD.size + nD.size) + 32)

The common prefix of the core: the input taken apart and the dimension query answered, then the dispatch.

theorem MIPRE.Cost.Prog.coreDispatch_nil (univ : Prog) (sD lD tD nD sz : Data) : Eval (coreEnv sD lD tD nD Data.nil sz) univ.coreDispatch Data.nil 2

The dispatch on an empty query: nil.

theorem MIPRE.Cost.Prog.coreDispatch_dim (univ : Prog) (sD lD tD nD qr sz : Data) {r : Data} {t : ℕ} (hd : Eval [sz.cons (lD.cons (nD.cons tD))] dimProg r t) : Eval (coreEnv sD lD tD nD (Data.nil.cons qr) sz) univ.coreDispatch r (t + 2 * (sz.size + lD.size + nD.size + tD.size) + 15)

The dispatch on a dimension query (kind nil): dimProg on (sz, λ, n, τ).

theorem MIPRE.Cost.Prog.coreDispatch_lock {univ : Prog} (hU : WellScoped 1 univ) (sD lD tD nD k₀ k₁ qr sz : Data) {r : Data} {t : ℕ} (hl : Eval [sD.cons (nD.cons (sz.cons ((k₀.cons k₁).cons qr)))] univ.lockProg r t) : Eval (coreEnv sD lD tD nD ((k₀.cons k₁).cons qr) sz) univ.coreDispatch r (t + 2 * (sD.size + nD.size + sz.size + k₀.size + k₁.size + qr.size) + 20)

The dispatch on a query of nonzero kind: lockProg on (S̄, n, sz, kind, rest).