The coordinate loop of the repeated decider

The repeated decider of thm:parallel-repetition runs the input decider D̄ on each of the k coordinates of its input (planning/repetition-verifier.md, R3(c)). This module is that loop, on the state (k, remX, remY, remA, remB, ctx) — k a unary counter, remX, remY the questions still to be cut into blocks of s, remA, remB the answers still to be checked, ctx = (D̄, n, s, B):

• preProg cuts a block off remX and remY, checks that the current answers are bit strings of length at most B (okBits), and returns the query (D̄, (n, x_i, y_i, a_i, b_i)) for the universal machine with the next state, or nil when a check fails;
• stepProg runs the query through univ and continues when the answer is 1;
• finalProg accepts, once the counter is exhausted, when no answer is left over;
• coordBody is the body of the loop.

Two readings of the loop are proved: a forward one, decLoop_of_acc — the loop accepts when every coordinate passes (DecAcc) — and an inversion, decLoop_inv — the loop accepts only then, obtained from stepProg_inv by determinism of the semantics. The inversion is what the game equivalence of the repeated verifier needs, since the input decider may not halt on inputs it does not accept. A third, decLoop_runs_bounded, is the forward reading with costs, against an oracle for the answers of univ, for the time bound.

Bit strings of bounded length

def MIPRE.Cost.Prog.okBits (B : ℕ) (d : Data) : Bool

d is the encoding of a bit string of length at most B: the walk bitWalk against the unary budget B ends with the string exhausted.

Equations

• MIPRE.Cost.Prog.okBits B d = match d.bitWalk (MIPRE.Cost.Data.ofNat B) with | MIPRE.Cost.Data.nil.cons a => true | x => false

theorem MIPRE.Cost.Prog.okBits_encode (B : ℕ) (x : BitStr) : okBits B (encode x) = decide (List.length x ≤ B)

theorem MIPRE.Cost.Prog.okBits_iff (B : ℕ) (d : Data) : okBits B d = true ↔ ∃ (x : BitStr), d = encode x ∧ List.length x ≤ B

The state and the programs

def MIPRE.Cost.Prog.decCtx (dD nD : Data) (s B : ℕ) : Data

The context of the loop: the input decider D̄, the index n, and s, B in unary.

Equations

• MIPRE.Cost.Prog.decCtx dD nD s B = dD.cons (nD.cons ((MIPRE.Cost.Data.ofNat s).cons (MIPRE.Cost.Data.ofNat B)))

def MIPRE.Cost.Prog.decQuery (dD nD xi yi ai bi : Data) : Data

The query to the universal machine on one coordinate: (D̄, (n, x_i, y_i, a_i, b_i)).

Equations

• MIPRE.Cost.Prog.decQuery dD nD xi yi ai bi = dD.cons (nD.cons (xi.cons (yi.cons (ai.cons bi))))

def MIPRE.Cost.Prog.decState (uk : Data) (remX remY remA remB : List Data) (ctx : Data) : Data

The state of the loop.

Equations

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

def MIPRE.Cost.Prog.finalProg : Prog

On the exhausted counter: accept iff no answer is left over.

Equations

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

theorem MIPRE.Cost.Prog.finalProg_wellScoped : WellScoped 1 finalProg

theorem MIPRE.Cost.Prog.finalProg_runs (remX remY remA remB : List Data) (ctx : Data) : ∃ t ≤ 12, Eval [(Data.list remX).cons ((Data.list remY).cons ((Data.list remA).cons ((Data.list remB).cons ctx)))] finalProg (Data.nil.cons (Data.ofBool (decide (remA = [] ∧ remB = [])))) t

def MIPRE.Cost.Prog.preProg : Prog

Before the call: cut a block off remX and remY, check the current answers, and return the query with the next state — or nil.

Equations

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

theorem MIPRE.Cost.Prog.preProg_wellScoped : WellScoped 1 preProg

def MIPRE.Cost.Prog.preCost (s B U Y A Bs C K : ℕ) : ℕ

The cost of preProg at s, B, on remainders of sizes U, Y, answer lists of sizes A, Bs, a context of size C and a counter of size K.

Equations

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

theorem MIPRE.Cost.Prog.preProg_runs_nilA (uk : Data) (remX remY remB : List Data) (ctx : Data) : ∃ t ≤ 7, Eval [decState uk remX remY [] remB ctx] preProg Data.nil t

theorem MIPRE.Cost.Prog.preProg_runs_nilB (uk : Data) (remX remY : List Data) (a : Data) (remA : List Data) (ctx : Data) : ∃ t ≤ 8, Eval [decState uk remX remY (a :: remA) [] ctx] preProg Data.nil t

def MIPRE.Cost.Prog.preResult (dD nD : Data) (s B : ℕ) (uk : Data) (remX remY : List Data) (ai bi : Data) (remA remB : List Data) : Data

The result of preProg on a state with answers ai, bi at hand.

Equations

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

theorem MIPRE.Cost.Prog.preProg_runs (dD nD : Data) (s B : ℕ) (uk : Data) (remX remY : List Data) (ai bi : Data) (remA remB : List Data) : ∃ t ≤ preCost s B (Data.list remX).size (Data.list remY).size (Data.list (ai :: remA)).size (Data.list (bi :: remB)).size (decCtx dD nD s B).size uk.size, Eval [decState uk remX remY (ai :: remA) (bi :: remB) (decCtx dD nD s B)] preProg (preResult dD nD s B uk remX remY ai bi remA remB) t

preProg on a state with answers at hand.

The step: the call to the input decider

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

One coordinate: preProg, then the query through univ, continuing when the answer is 1 (cons nil nil), stopping with 0 otherwise.

Equations

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

theorem MIPRE.Cost.Prog.stepProg_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.stepProg

def MIPRE.Cost.Prog.stepResult (st' r : Data) : Data

The result of the step from the answer r of univ: continue with st' on 1.

Equations

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

theorem MIPRE.Cost.Prog.stepProg_runs_nil (univ : Prog) (inp : Data) {t₀ : ℕ} (hp : Eval [inp] preProg Data.nil t₀) : Eval [inp] univ.stepProg (Data.nil.cons Data.nil) (t₀ + inp.size + 7)

theorem MIPRE.Cost.Prog.stepProg_runs_call {univ : Prog} (hU : WellScoped 1 univ) (inp q st' : Data) {t₀ : ℕ} (hp : Eval [inp] preProg (q.cons st') t₀) {r : Data} {tr : ℕ} (hr : Eval [q] univ r tr) : ∃ t ≤ t₀ + tr + inp.size + q.size + st'.size + 20, Eval [inp] univ.stepProg (stepResult st' r) t

theorem MIPRE.Cost.Prog.stepProg_inv {univ : Prog} (hU : WellScoped 1 univ) (inp : Data) {out : Data} {t : ℕ} (h : Eval [inp] univ.stepProg out t) : ∃ (p : Data) (t₀ : ℕ), Eval [inp] preProg p t₀ ∧ (p = Data.nil ∧ out = Data.nil.cons Data.nil ∨ ∃ (q : Data) (st' : Data) (r : Data), p = q.cons st' ∧ (∃ (tr : ℕ), Eval [q] univ r tr) ∧ out = stepResult st' r)

Inversion of the step. A run of stepProg is a run of preProg, then, when it returns a query, a run of univ on it deciding the result.

The body

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

The body of the coordinate loop: on the exhausted counter, finalProg; otherwise the step on the decremented state.

Equations

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

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

theorem MIPRE.Cost.Prog.coordBody_stop (univ : Prog) (remX remY remA remB : List Data) (ctx : Data) : ∃ t ≤ (Data.list remX).size + (Data.list remY).size + (Data.list remA).size + (Data.list remB).size + ctx.size + 24, Eval [decState (Data.ofNat 0) remX remY remA remB ctx] univ.coordBody (Data.nil.cons (Data.ofBool (decide (remA = [] ∧ remB = [])))) t

theorem MIPRE.Cost.Prog.coordBody_step {univ : Prog} (hU : WellScoped 1 univ) (k : ℕ) (remX remY remA remB : List Data) (ctx : Data) {out : Data} {t : ℕ} (h : Eval [decState (Data.ofNat k) remX remY remA remB ctx] univ.stepProg out t) : Eval [decState (Data.ofNat (k + 1)) remX remY remA remB ctx] univ.coordBody out (t + 2 * (decState (Data.ofNat k) remX remY remA remB ctx).size + 7)

theorem MIPRE.Cost.Prog.coordBody_inv {univ : Prog} (hU : WellScoped 1 univ) (k : ℕ) (remX remY remA remB : List Data) (ctx : Data) {out : Data} {t : ℕ} (h : Eval [decState (Data.ofNat k) remX remY remA remB ctx] univ.coordBody out t) : k = 0 ∧ out = Data.nil.cons (Data.ofBool (decide (remA = [] ∧ remB = []))) ∨ ∃ (k' : ℕ), k = k' + 1 ∧ ∃ (t' : ℕ), Eval [decState (Data.ofNat k') remX remY remA remB ctx] univ.stepProg out t'

Inversion of the body. On the exhausted counter, the body stops with the verdict of finalProg; otherwise it is a run of the step on the decremented state.

The loop

def MIPRE.Cost.Prog.DecAcc (univ : Prog) (dD nD : Data) (s B : ℕ) : ℕ → List Data → List Data → List Data → List Data → Prop

Acceptance of the coordinate loop: k answers on each side, each a bit string of length at most B, and the input decider, through univ, answering 1 on every coordinate.

Equations

• One or more equations did not get rendered due to their size.
• univ.DecAcc dD nD s B 0 x✝³ x✝² x✝¹ x✝ = (x✝¹ = [] ∧ x✝ = [])
• univ.DecAcc dD nD s B n.succ x✝² x✝¹ [] x✝ = False
• univ.DecAcc dD nD s B n.succ x✝¹ x✝ (head :: tail) [] = False

theorem MIPRE.Cost.Prog.coordLoop_of_acc {univ : Prog} (hU : WellScoped 1 univ) (dD nD : Data) (s B k : ℕ) (remX remY remA remB : List Data) (env : Env) : univ.DecAcc dD nD s B k remX remY remA remB → ∃ (t : ℕ), Eval (decState (Data.ofNat k) remX remY remA remB (decCtx dD nD s B) :: env) univ.coordBody.loop (Data.nil.cons Data.nil) t

The loop accepts on DecAcc.

theorem MIPRE.Cost.Prog.coordLoop_inv {univ : Prog} (hU : WellScoped 1 univ) (dD nD : Data) (s B k : ℕ) (remX remY remA remB : List Data) (env : Env) {t : ℕ} : Eval (decState (Data.ofNat k) remX remY remA remB (decCtx dD nD s B) :: env) univ.coordBody.loop (Data.nil.cons Data.nil) t → univ.DecAcc dD nD s B k remX remY remA remB

The loop accepts only on DecAcc.

The loop with costs

def MIPRE.Cost.Prog.decQueries (dD nD : Data) (s : ℕ) : ℕ → List Data → List Data → List Data → List Data → List Data

The potential queries of the loop, in order: one per coordinate while answers remain.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Cost.Prog.decQueries dD nD s 0 x✝³ x✝² x✝¹ x✝ = []
• MIPRE.Cost.Prog.decQueries dD nD s n.succ x✝² x✝¹ [] x✝ = []
• MIPRE.Cost.Prog.decQueries dD nD s n.succ x✝¹ x✝ (head :: tail) [] = []

def MIPRE.Cost.Prog.coordIter (Z Tu : ℕ) : ℕ

The per-iteration budget of the loop, in a bound Z on the sizes and the cost Tu of a call.

Equations

• MIPRE.Cost.Prog.coordIter Z Tu = 40 * (Z + 30) ^ 2 + Tu

theorem MIPRE.Cost.Prog.preCost_le {s B U Y A Bs C K Z : ℕ} (h : s + B + U + Y + A + Bs + C + K ≤ Z) : preCost s B U Y A Bs C K ≤ 30 * (Z + 30) ^ 2

theorem MIPRE.Cost.Prog.coordLoop_runs_bounded {univ : Prog} (hU : WellScoped 1 univ) (dD nD : Data) (s B : ℕ) (fq : Data → Data) (Tu Z k : ℕ) (remX remY remA remB : List Data) (env : Env) : (∀ q ∈ decQueries dD nD s k remX remY remA remB, ∃ t ≤ Tu, Eval [q] univ (fq q) t) → s + B + (Data.list remX).size + (Data.list remY).size + (Data.list remA).size + (Data.list remB).size + (decCtx dD nD s B).size + (Data.ofNat k).size + 10 ≤ Z → ∃ (r : Data), ∃ t ≤ (k + 1) * coordIter Z Tu, Eval (decState (Data.ofNat k) remX remY remA remB (decCtx dD nD s B) :: env) univ.coordBody.loop r t

The loop halts within (k + 1) · coordIter Z Tu when univ answers every potential query within Tu and the sizes in play are bounded by Z.