The block loop of the repeated sampler

The repeated sampler of thm:parallel-repetition answers a marginal, linear or factor query on 𝔽₂^{k s} by cutting the vectors of the query into k blocks of s coordinates, asking the input sampler about each block, and concatenating the answers (planning/repetition-verifier.md, R3(b)). This module is that loop:

• pairTakeProg cuts the first s elements off two lists at once;
• mapBody is the body of the loop, on the state (s, remU, remY, ctx, acc): stop with acc once remU is exhausted, and otherwise cut a block off remU and remY, build the query (n, kind, w, j, blockU, blockY) from the context ctx = (S̄, n, kind, w, j), run the input sampler S̄ on it through the universal machine univ, and push the answer, reversed, onto acc;
• mapLoop_runs is the loop: its output is the reversed concatenation of the answers on the pairs of blocks Data.chunkPairs, in time (|remU| + 1) times a quadratic in a bound Z on the sizes in play and the cost Tu of one call.

The loop is uniform in the query kind: the blocks of an absent vector are empty, which is the encoding of the empty bit string, so a marginal or factor query — whose last component is empty — goes through the same code as a linear one. The answers are a parameter f of the run lemma, known only on the pairs of blocks that occur: on well-formed queries they are the input sampler's answers, on arbitrary ones whatever it halts with.

Cutting a block off two lists

def MIPRE.Cost.Prog.pairTakeProg : Prog

On cons us (cons remU remY) with us the unary numeral s: the pair of remainders and the pair of blocks, cons remU' (cons remY' (cons blockU blockY)).

Equations

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

theorem MIPRE.Cost.Prog.pairTakeProg_wellScoped : WellScoped 1 pairTakeProg

def MIPRE.Cost.Prog.pairTakeCost (s U Y : ℕ) : ℕ

The cost of pairTakeProg on a numeral s and lists of sizes U, Y.

Equations

• MIPRE.Cost.Prog.pairTakeCost s U Y = 2 * ((s + 1) * (U + Y + 2 * s + 21)) + 2 * ((U + 2) * (U + Y + 13)) + 2 * ((Y + 2) * (U + Y + 13)) + 4 * s + 8 * U + 8 * Y + 40

theorem MIPRE.Cost.Prog.pairTakeProg_runs (s : ℕ) (remU remY : List Data) : ∃ t ≤ pairTakeCost s (Data.list remU).size (Data.list remY).size, pairTakeProg.Runs ((Data.ofNat s).cons ((Data.list remU).cons (Data.list remY))) ((Data.list (List.drop s remU)).cons ((Data.list (List.drop s remY)).cons ((Data.list (List.take s remU)).cons (Data.list (List.take s remY))))) t

The loop body

def MIPRE.Cost.Prog.mapCtx (sD nD kD wD jD : Data) : Data

The context of the loop: the input sampler S̄ and the fixed part (n, kind, w, j) of the query.

Equations

• MIPRE.Cost.Prog.mapCtx sD nD kD wD jD = sD.cons (nD.cons (kD.cons (wD.cons jD)))

def MIPRE.Cost.Prog.mapQuery (sD nD kD wD jD cU cY : Data) : Data

The input of the universal machine for one block: (S̄, (n, kind, w, j, blockU, blockY)).

Equations

• MIPRE.Cost.Prog.mapQuery sD nD kD wD jD cU cY = sD.cons (nD.cons (kD.cons (wD.cons (jD.cons (cU.cons cY)))))

def MIPRE.Cost.Prog.mapState (s : ℕ) (remU remY : List Data) (ctx : Data) (acc : List Data) : Data

The state of the loop.

Equations

• MIPRE.Cost.Prog.mapState s remU remY ctx acc = (MIPRE.Cost.Data.ofNat s).cons ((MIPRE.Cost.Data.list remU).cons ((MIPRE.Cost.Data.list remY).cons (ctx.cons (MIPRE.Cost.Data.list acc))))

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

The body of the block loop, with univ the universal machine.

Equations

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

theorem MIPRE.Cost.Prog.mapBody_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.mapBody

theorem MIPRE.Cost.Prog.mapBody_stop (univ : Prog) (s : ℕ) (remY : List Data) (ctx : Data) (acc : List Data) : ∃ t ≤ (Data.list acc).size + 8, Eval [mapState s [] remY ctx acc] univ.mapBody (Data.nil.cons (Data.list acc)) t

def MIPRE.Cost.Prog.mapStepCost (s U Y C A Tu : ℕ) : ℕ

The cost of one iteration, in the numeral s, the sizes U, Y of the remainders, C of the context, A of the accumulator, and the cost Tu of the call.

Equations

• MIPRE.Cost.Prog.mapStepCost s U Y C A Tu = MIPRE.Cost.Prog.pairTakeCost s U Y + (Tu + 1) * (Tu + A + 12) + 6 * s + 6 * U + 6 * Y + 3 * C + 3 * A + 4 * Tu + 70

theorem MIPRE.Cost.Prog.mapBody_step {univ : Prog} (hU : WellScoped 1 univ) (s : ℕ) (h : Data) (l remY : List Data) (sD nD kD wD jD : Data) (acc : List Data) {r : Data} {tu : ℕ} (hr : Eval [mapQuery sD nD kD wD jD (Data.list (List.take s (h :: l))) (Data.list (List.take s remY))] univ r tu) : ∃ t ≤ mapStepCost s (Data.list (h :: l)).size (Data.list remY).size (mapCtx sD nD kD wD jD).size (Data.list acc).size tu, Eval [mapState s (h :: l) remY (mapCtx sD nD kD wD jD) acc] univ.mapBody ((Data.nil.cons Data.nil).cons (mapState s (List.drop s (h :: l)) (List.drop s remY) (mapCtx sD nD kD wD jD) (r.toList.reverse ++ acc))) t

One iteration: the block is cut, the call made, its answer pushed reversed onto acc.

def MIPRE.Cost.Prog.mapAcc (f : List Data → List Data → Data) (pairs : List (List Data × List Data)) (acc : List Data) : List Data

The output of the loop from the pairs of blocks: the answers, each reversed, in reverse order, in front of acc.

Equations

• MIPRE.Cost.Prog.mapAcc f pairs acc = (List.map (fun (p : List MIPRE.Cost.Data × List MIPRE.Cost.Data) => (f p.1 p.2).toList.reverse) pairs).reverse.flatten ++ acc

theorem MIPRE.Cost.Prog.mapAcc_reverse (f : List Data → List Data → Data) (pairs : List (List Data × List Data)) : (mapAcc f pairs []).reverse = (List.map (fun (p : List Data × List Data) => (f p.1 p.2).toList) pairs).flatten

Reversing the output with acc = [] gives the concatenation of the answers.

theorem MIPRE.Cost.Prog.mapAcc_cons (f : List Data → List Data → Data) (p : List Data × List Data) (pairs : List (List Data × List Data)) (acc : List Data) : mapAcc f (p :: pairs) acc = mapAcc f pairs ((f p.1 p.2).toList.reverse ++ acc)

def MIPRE.Cost.Prog.mapIter (Z : ℕ) : ℕ

The per-iteration budget of the loop, in a bound Z on the sizes in play.

Equations

• MIPRE.Cost.Prog.mapIter Z = 22 * (Z + 30) ^ 2

theorem MIPRE.Cost.Prog.pairTakeCost_le {s U Y Z : ℕ} (h : s + U + Y ≤ Z) : pairTakeCost s U Y ≤ 17 * (Z + 30) ^ 2

theorem MIPRE.Cost.Prog.mapStepCost_le {s U Y C A Tu Z : ℕ} (h : s + U + Y + C + A + Tu ≤ Z) : mapStepCost s U Y C A Tu + 1 ≤ mapIter Z

theorem MIPRE.Cost.Prog.mapLoop_runs {univ : Prog} (hU : WellScoped 1 univ) {s : ℕ} (hs : 0 < s) (sD nD kD wD jD : Data) (f : List Data → List Data → Data) (Tu Z : ℕ) (remU remY acc : List Data) (env : Env) : (∀ p ∈ Data.chunkPairs s hs remU remY, ∃ t ≤ Tu, Eval [mapQuery sD nD kD wD jD (Data.list p.1) (Data.list p.2)] univ (f p.1 p.2) t) → s + (Data.list remU).size + (Data.list remY).size + (mapCtx sD nD kD wD jD).size + (Data.list acc).size + remU.length * (Tu + 1) + Tu ≤ Z → ∃ t ≤ (remU.length + 1) * mapIter Z, Eval (mapState s remU remY (mapCtx sD nD kD wD jD) acc :: env) univ.mapBody.loop (Data.list (mapAcc f (Data.chunkPairs s hs remU remY) acc)) t

The block loop. With f the answer of the universal machine on each pair of blocks that occurs, at cost at most Tu, and Z a bound on the sizes in play, the loop from (s, remU, remY, ctx, acc) outputs mapAcc f (chunkPairs s remU remY) acc in time (|remU| + 1) · mapIter Z.