The program of the repeated decider

The decider of ComputeParrepVerifier (thm:parallel-repetition; planning/repetition-verifier.md, R3(c)) as a program of the ambient model, before the s-m-n construction. On ((S̄, D̄, λ, τ, β), (n, x, y, a, b)) it

1. sanitizes x, y, a, b into bit strings (bitsProg: every element read as a bit), so that the rest of the program is total on every datum;
2. computes, in unary, s = s(n) from S̄, m = τ(|λ| + |n|), the repetition count k = 2^m, the question length k s, and the parse length B = 2^{β(|λ| + |n|)};
3. checks |x| = |y| = k s and that a, b are the serializations of the data they parse to (Data.parse, Data.toBitsPost), the four verdicts combined by andExpr;
4. runs the coordinate loop coordBody on the state (k, x, y, parse a, parse b, (D̄, n, s, B)).

prepProg is steps 1–3, returning the state of the loop or nil; its run lemma prepProg_runs is a straight line of deterministic steps, generated mechanically.

Sanitizing a list into a bit string

def MIPRE.Cost.Prog.bitsBody : Prog

Body of the sanitizer: on cons rem acc, move the head of rem, read as a bit, onto acc.

Equations

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

theorem MIPRE.Cost.Prog.bitsBody_wellScoped : WellScoped 1 bitsBody

def MIPRE.Cost.Prog.bitsProg : Prog

The sanitizer: the bits of a list, encode (bitsOf l).

Equations

• MIPRE.Cost.Prog.bitsProg = ((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ (MIPRE.Cost.Prog.bitsBody.loop.let_ (MIPRE.Cost.Prog.callVar 0 MIPRE.Cost.Prog.revProg))

theorem MIPRE.Cost.Prog.bitsProg_wellScoped : WellScoped 1 bitsProg

theorem MIPRE.Cost.Prog.bitsBody_stop (acc : List Data) : ∃ t ≤ (Data.list acc).size + 6, Eval [(Data.list []).cons (Data.list acc)] bitsBody (Data.nil.cons (Data.list acc)) t

theorem MIPRE.Cost.Prog.bitsBody_step (h : Data) (l acc : List Data) : ∃ t ≤ (Data.list l).size + (Data.list acc).size + h.size + 12, Eval [(Data.list (h :: l)).cons (Data.list acc)] bitsBody ((Data.nil.cons Data.nil).cons ((Data.list l).cons (Data.list (Data.ofBool h.bitOf :: acc)))) t

theorem MIPRE.Cost.Prog.bitsLoop_runs (l acc : List Data) (env : Env) (S : ℕ) (hS : (Data.list l).size + (Data.list acc).size + 2 * l.length ≤ S) : ∃ t ≤ (l.length + 1) * (S + 14), Eval ((Data.list l).cons (Data.list acc) :: env) bitsBody.loop (Data.list ((List.map (fun (h : Data) => Data.ofBool h.bitOf) l).reverse ++ acc)) t

theorem MIPRE.Cost.Prog.bitsProg_runs (l : List Data) : ∃ t ≤ (l.length + 2) * ((Data.list l).size + 2 * l.length + 15) + (l.length + 2) * (4 * l.length + 20), bitsProg.Runs (Data.list l) (encode (Data.bitsOf l)) t

The sanitizer computes encode (bitsOf l) on list l.

Conjunction of four verdicts

def MIPRE.Cost.Prog.andExpr (i₁ i₂ i₃ i₄ : ℕ) : Prog

ok₁ ∧ ok₂ ∧ ok₃ ∧ ok₄ on encoded booleans at the given indices (each test extends the environment by two entries).

Equations

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

theorem MIPRE.Cost.Prog.andExpr_runs {env : Env} {i₁ i₂ i₃ i₄ : ℕ} {c₁ c₂ c₃ c₄ : Bool} (h₁ : env.get i₁ = Data.ofBool c₁) (h₂ : env.get i₂ = Data.ofBool c₂) (h₃ : env.get i₃ = Data.ofBool c₃) (h₄ : env.get i₄ = Data.ofBool c₄) : ∃ t ≤ 8, Eval env (andExpr i₁ i₂ i₃ i₄) (Data.ofBool (c₁ && c₂ && c₃ && c₄)) t

theorem MIPRE.Cost.Prog.powLoop_wellScoped : WellScoped 1 powBody.loop

theorem MIPRE.Cost.Prog.dblLoop_wellScoped : WellScoped 1 dblBody.loop

The straight-line prefix of the decider (generated)

def MIPRE.Cost.Prog.decInput (sP dP lamD tauD betaD nD xD yD aD bD : Data) : Data

The input of prepProg: (S̄, D̄, λ, τ, β, n, x, y, a, b).

Equations

• MIPRE.Cost.Prog.decInput sP dP lamD tauD betaD nD xD yD aD bD = sP.cons (dP.cons (lamD.cons (tauD.cons (betaD.cons (nD.cons (xD.cons (yD.cons (aD.cons bD))))))))

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

Steps 1–3 of the repeated decider, returning the state of the coordinate loop or nil.

Equations

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

def MIPRE.Cost.Prog.prepEnv (univ : Prog) (sP dP : Data) (lam tau beta n s : ℕ) (xD yD aD bD : Data) : Env

The environment of prepProg after its straight-line prefix, in terms of the parameters.

Equations

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

def MIPRE.Cost.Prog.bitsCost (L sz : ℕ) : ℕ

The cost of the sanitizer on a list of length L and size sz.

Equations

• MIPRE.Cost.Prog.bitsCost L sz = (L + 2) * (sz + 2 * L + 15) + (L + 2) * (4 * L + 20)

def MIPRE.Cost.Prog.lenCost (L sz : ℕ) : ℕ

The cost of lenProg on a list of length L and size sz.

Equations

• MIPRE.Cost.Prog.lenCost L sz = (L + 1 + 1) * (sz + 1 + 2 * L + 13)

def MIPRE.Cost.Prog.eqCost (l₁ l₂ : Data) : ℕ

The cost of eqBitsProg on l₁, l₂.

Equations

• MIPRE.Cost.Prog.eqCost l₁ l₂ = (l₁.spine + 1) * (l₁.size + l₂.size + 21)

def MIPRE.Cost.Prog.parseCost (x : BitStr) : ℕ

The cost of parseProg on x.

Equations

• MIPRE.Cost.Prog.parseCost x = (List.length x + 2) * ((MIPRE.Cost.encode x).size + 2 * List.length x + 25)

def MIPRE.Cost.Prog.serCost (d : Data) : ℕ

The cost of serProg on d.

Equations

• MIPRE.Cost.Prog.serCost d = (3 * d.size + 2) * (16 * d.size + 42) + (d.size + 2) * (5 * d.size + 30)

def MIPRE.Cost.Prog.prepPreCost (sP dP : Data) (lam tau beta n s : ℕ) (xD yD aD bD : Data) (td : ℕ) : ℕ

The cost of the straight-line prefix of prepProg.

Equations

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

theorem MIPRE.Cost.Prog.prepProg_prefix {univ : Prog} (hU : WellScoped 1 univ) (sP dP : Data) (lam tau beta n s : ℕ) (xD yD aD bD : Data) {td : ℕ} (hdim : Eval [sP.cons ((encode n).cons (encode CL.Sampler.Query.dimension))] univ (encode s) td) {r : Data} {t : ℕ} (hc : Eval (univ.prepEnv sP dP lam tau beta n s xD yD aD bD) ((andExpr 11 8 4 0).let_ (((var 49).cons ((var 41).cons ((var 32).cons (var 19)))).let_ (elim 1 nil ((var 27).cons ((var 21).cons ((var 20).cons ((var 11).cons ((var 7).cons (var 2))))))))) r t) : ∃ t' ≤ t + prepPreCost sP dP lam tau beta n s xD yD aD bD td, Eval [decInput sP dP (encode lam) (encode tau) (encode beta) (encode n) xD yD aD bD] univ.prepProg r t'

The full preparation, the main program and the core

def MIPRE.Cost.Prog.prepOk (lam tau n s : ℕ) (x y a b : BitStr) : Bool

The four verdicts of the checks: |x| = |y| = k s, and a, b canonical.

Equations

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

def MIPRE.Cost.Prog.prepState (dP : Data) (lam tau beta n s : ℕ) (x y a b : BitStr) : Data

The state of the coordinate loop assembled by prepProg.

Equations

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

theorem MIPRE.Cost.Prog.prepState_eq (dP : Data) (lam tau beta n s : ℕ) (x y a b : BitStr) : prepState dP lam tau beta n s x y a b = decState (Data.ofNat (2 ^ (tau * (lam.size + n.size)))) (List.map Data.ofBool x) (List.map Data.ofBool y) (Data.parse a).toList (Data.parse b).toList (decCtx dP (encode n) s (2 ^ (beta * (lam.size + n.size))))

def MIPRE.Cost.Prog.prepResult (dP : Data) (lam tau beta n s : ℕ) (x y a b : BitStr) : Data

The result of prepProg: the state when the checks pass, nil otherwise.

Equations

• MIPRE.Cost.Prog.prepResult dP lam tau beta n s x y a b = if MIPRE.Cost.Prog.prepOk lam tau n s x y a b = true then MIPRE.Cost.Prog.prepState dP lam tau beta n s x y a b else MIPRE.Cost.Data.nil

def MIPRE.Cost.Prog.prepCost (sP dP : Data) (lam tau beta n s : ℕ) (xD yD aD bD : Data) (td : ℕ) : ℕ

The cost of prepProg.

Equations

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

theorem MIPRE.Cost.Prog.prepProg_runs {univ : Prog} (hU : WellScoped 1 univ) (sP dP : Data) (lam tau beta n s : ℕ) (xD yD aD bD : Data) {td : ℕ} (hdim : Eval [sP.cons ((encode n).cons (encode CL.Sampler.Query.dimension))] univ (encode s) td) : ∃ t ≤ prepCost sP dP lam tau beta n s xD yD aD bD td, Eval [decInput sP dP (encode lam) (encode tau) (encode beta) (encode n) xD yD aD bD] univ.prepProg (prepResult dP lam tau beta n s (Data.bitsOf xD.toList) (Data.bitsOf yD.toList) (Data.bitsOf aD.toList) (Data.bitsOf bD.toList)) t

prepProg computes prepResult, on every input of the right shape.

theorem MIPRE.Cost.Prog.prepProg_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.prepProg

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

The main program: the preparation, then the coordinate loop on its state.

Equations

• univ.decMain = univ.prepProg.let_ (MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.callVar 2 univ.coordBody.loop))

theorem MIPRE.Cost.Prog.coordLoop_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.coordBody.loop

theorem MIPRE.Cost.Prog.decMain_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.decMain

theorem MIPRE.Cost.Prog.decMain_runs_nil {univ : Prog} (inp : Data) {t₀ : ℕ} (hp : Eval [inp] univ.prepProg Data.nil t₀) : Eval [inp] univ.decMain Data.nil (t₀ + 3)

theorem MIPRE.Cost.Prog.decMain_runs_state {univ : Prog} (hU : WellScoped 1 univ) (inp st₀ st₁ : Data) {t₀ t₁ : ℕ} (hp : Eval [inp] univ.prepProg (st₀.cons st₁) t₀) {r : Data} (hl : Eval [st₀.cons st₁] univ.coordBody.loop r t₁) : Eval [inp] univ.decMain r (t₀ + t₁ + (st₀.cons st₁).size + 4)

theorem MIPRE.Cost.Prog.decMain_inv {univ : Prog} (hU : WellScoped 1 univ) (inp : Data) {out : Data} {t : ℕ} (h : Eval [inp] univ.decMain out t) : ∃ (p : Data) (t₀ : ℕ), Eval [inp] univ.prepProg p t₀ ∧ (p = Data.nil ∧ out = Data.nil ∨ ∃ (st₀ : Data) (st₁ : Data), p = st₀.cons st₁ ∧ ∃ (t₁ : ℕ), Eval [st₀.cons st₁] univ.coordBody.loop out t₁)

Inversion of the main program.

def MIPRE.Cost.Prog.decParams (sP dP lamD tauD betaD : Data) : Data

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

Equations

• MIPRE.Cost.Prog.decParams sP dP lamD tauD betaD = (sP.cons dP).cons (lamD.cons (tauD.cons betaD))

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

The core of the repeated decider, before the s-m-n construction: on (((S̄, D̄), λ, τ, β), (n, x, y, a, b)), the main program on (S̄, D̄, λ, τ, β, n, x, y, a, b).

Equations

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

theorem MIPRE.Cost.Prog.repDecCore_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.repDecCore

theorem MIPRE.Cost.Prog.repDecCore_runs {univ : Prog} (hU : WellScoped 1 univ) (sP dP lamD tauD betaD nD xD yD aD bD : Data) {r : Data} {t : ℕ} (h : Eval [decInput sP dP lamD tauD betaD nD xD yD aD bD] univ.decMain r t) : Eval [(decParams sP dP lamD tauD betaD).cons (nD.cons (xD.cons (yD.cons (aD.cons bD))))] univ.repDecCore r (t + 2 * (sP.size + dP.size + lamD.size + tauD.size + betaD.size + nD.size + xD.size + yD.size + aD.size + bD.size) + 40)

theorem MIPRE.Cost.Prog.repDecCore_inv {univ : Prog} (hU : WellScoped 1 univ) (sP dP lamD tauD betaD nD xD yD aD bD : Data) {r : Data} {t : ℕ} (h : Eval [(decParams sP dP lamD tauD betaD).cons (nD.cons (xD.cons (yD.cons (aD.cons bD))))] univ.repDecCore r t) : ∃ (t' : ℕ), Eval [decInput sP dP lamD tauD betaD nD xD yD aD bD] univ.decMain r t'

Inversion of the core on an input of the right shape.

theorem MIPRE.Cost.Prog.repDecCore_runs_malformed (univ : Prog) (sP dP lamD tauD betaD nD d : Data) (hd : d = Data.nil ∨ (∃ (xD : Data), d = xD.cons Data.nil) ∨ ∃ (xD : Data) (yD : Data), d = xD.cons (yD.cons Data.nil)) : ∃ t ≤ 10, Eval [(decParams sP dP lamD tauD betaD).cons (nD.cons d)] univ.repDecCore Data.nil t

The core on a malformed (n, d): nil.