Programs in stages, and a loop of calls to a stored program

The programs of the repeated tailored verifier (Phase 2 of planning/aldous-lyons-track.md, issue #280) are built in stages: polynomial-time functions, which prepare the next stage's input while carrying what later stages need, alternate with calls to the input programs through the universal machine. This module is the glue.

• seq p q runs q on the result of p (seq_runs, and its inversion seq_inv).
• withCtx p runs p on the second component of a pair and keeps the first: the context a later stage needs passes over a stage that does not.
• mapCall univ, on (c, [q₁, …, q_m]), runs univ on (c, qᵢ) for every i and returns the list of results. With univ the universal machine and c a program's description, it runs the program on every query. It halts with [r₁, …, r_m] when every call halts with rᵢ, at the cost of the calls plus a quadratic overhead (mapCall_runs), and only then (mapCall_inv), which is what lets a halting repeated program say that every coordinate's program halted.

Sequencing

def MIPRE.Tailored.Calls.seq (p q : Cost.Prog) : Cost.Prog

Run q on the result of p.

Equations

• MIPRE.Tailored.Calls.seq p q = p.let_ q

theorem MIPRE.Tailored.Calls.seq_wellScoped {p q : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (hq : Cost.Prog.WellScoped 1 q) : Cost.Prog.WellScoped 1 (seq p q)

theorem MIPRE.Tailored.Calls.seq_runs {p q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) {x v r : Cost.Data} {s t : ℕ} (hp : p.Runs x v s) (hq' : q.Runs v r t) : (seq p q).Runs x r (s + t + 1)

theorem MIPRE.Tailored.Calls.seq_inv {p q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) {x r : Cost.Data} {t : ℕ} (h : (seq p q).Runs x r t) : ∃ (v : Cost.Data) (s : ℕ) (t' : ℕ), s + t' + 1 = t ∧ p.Runs x v s ∧ q.Runs v r t'

theorem MIPRE.Tailored.Calls.seq_pure_runs {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (F : Cost.PolyTimeFun α β) {q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) (a : α) {r : Cost.Data} {t : ℕ} (h : q.Runs (Cost.encode (F.toFun a)) r t) : ∃ s ≤ Polynomial.eval (Cost.esize a) F.timeBound, (seq F.code q).Runs (Cost.encode a) r (s + t + 1)

A polynomial-time stage followed by q: a run of q on the stage's value is a run of the sequence.

theorem MIPRE.Tailored.Calls.seq_pure_inv {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (F : Cost.PolyTimeFun α β) {q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) (a : α) {r : Cost.Data} {t : ℕ} (h : (seq F.code q).Runs (Cost.encode a) r t) : ∃ (t' : ℕ), q.Runs (Cost.encode (F.toFun a)) r t'

Inversion of a polynomial-time stage followed by q.

theorem MIPRE.Tailored.Calls.seq_det_inv {p q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) {x v r : Cost.Data} {s t : ℕ} (hp : p.Runs x v s) (h : (seq p q).Runs x r t) : ∃ (t' : ℕ), q.Runs v r t'

Inversion of a sequence whose first stage has a known run.

Keeping a context

def MIPRE.Tailored.Calls.withCtx (p : Cost.Prog) : Cost.Prog

On cons a b, the pair cons a (p b).

Equations

• MIPRE.Tailored.Calls.withCtx p = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil ((MIPRE.Cost.Prog.var 0).cons (MIPRE.Cost.Prog.callVar 1 p))

theorem MIPRE.Tailored.Calls.withCtx_wellScoped {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) : Cost.Prog.WellScoped 1 (withCtx p)

theorem MIPRE.Tailored.Calls.withCtx_runs {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (a : Cost.Data) {b r : Cost.Data} {t : ℕ} (h : p.Runs b r t) : (withCtx p).Runs (a.cons b) (a.cons r) (a.size + b.size + t + 5)

theorem MIPRE.Tailored.Calls.withCtx_inv {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) {a b r : Cost.Data} {t : ℕ} (h : (withCtx p).Runs (a.cons b) r t) : ∃ (r' : Cost.Data), ∃ t' ≤ t, p.Runs b r' t' ∧ r = a.cons r'

The loop of calls

theorem MIPRE.Tailored.Calls.sumSize_append (l₁ l₂ : List Cost.Data) : Cost.Data.sumSize (l₁ ++ l₂) = Cost.Data.sumSize l₁ + Cost.Data.sumSize l₂

theorem MIPRE.Tailored.Calls.size_list_reverse (l : List Cost.Data) : (Cost.Data.list l.reverse).size = (Cost.Data.list l).size

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

The body of the loop, on the state cons c (cons rem acc): stop with acc when rem is empty; otherwise run univ on cons c q for the head q of rem, push the result onto acc and continue with the tail.

Equations

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

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

def MIPRE.Tailored.Calls.mapCall (univ : Cost.Prog) : Cost.Prog

The loop of calls: on cons c (list qs), the list of the results of univ on cons c q, q ∈ qs, in order.

Equations

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

theorem MIPRE.Tailored.Calls.mapCall_wellScoped {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) : Cost.Prog.WellScoped 1 (mapCall univ)

def MIPRE.Tailored.Calls.mapState (c : Cost.Data) (rem acc : List Cost.Data) : Cost.Data

The state of the loop.

Equations

• MIPRE.Tailored.Calls.mapState c rem acc = c.cons ((MIPRE.Cost.Data.list rem).cons (MIPRE.Cost.Data.list acc))

theorem MIPRE.Tailored.Calls.mapBody_stop (univ : Cost.Prog) (c : Cost.Data) (acc : List Cost.Data) : Cost.Eval [mapState c [] acc] (mapBody univ) (Cost.Data.nil.cons (Cost.Data.list acc)) ((Cost.Data.list acc).size + 6)

theorem MIPRE.Tailored.Calls.mapBody_step {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (c q : Cost.Data) (rest acc : List Cost.Data) {r : Cost.Data} {t : ℕ} (h : univ.Runs (c.cons q) r t) : Cost.Eval [mapState c (q :: rest) acc] (mapBody univ) ((Cost.Data.nil.cons Cost.Data.nil).cons (mapState c rest (r :: acc))) (t + 3 * c.size + 2 * q.size + r.size + (Cost.Data.list rest).size + (Cost.Data.list acc).size + 22)

theorem MIPRE.Tailored.Calls.mapBody_inv {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (c : Cost.Data) (rem acc : List Cost.Data) {out : Cost.Data} {t : ℕ} (h : Cost.Eval [mapState c rem acc] (mapBody univ) out t) : rem = [] ∧ out = Cost.Data.nil.cons (Cost.Data.list acc) ∨ ∃ (q : Cost.Data) (rest : List Cost.Data) (r : Cost.Data), rem = q :: rest ∧ (∃ (t' : ℕ), univ.Runs (c.cons q) r t') ∧ out = (Cost.Data.nil.cons Cost.Data.nil).cons (mapState c rest (r :: acc))

Inversion of the body: on an empty rem it stops with acc; otherwise it ran univ on the head and continues.

theorem MIPRE.Tailored.Calls.mapLoop_runs {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (c : Cost.Data) (f : Cost.Data → Cost.Data) (T Z : ℕ) (env : Cost.Env) (rem acc : List Cost.Data) : (∀ q ∈ rem, ∃ t ≤ T, univ.Runs (c.cons q) (f q) t) → (Cost.Data.list rem).size + (Cost.Data.list (List.map f rem)).size + (Cost.Data.list acc).size ≤ Z → ∃ t ≤ (rem.length + 1) * (T + 3 * c.size + 2 * Z + 25), Cost.Eval (mapState c rem acc :: env) (mapBody univ).loop (Cost.Data.list ((List.map f rem).reverse ++ acc)) t

The loop with the results known: from the state (c, rem, acc), the loop stops with the results on rem, reversed, before acc.

theorem MIPRE.Tailored.Calls.mapLoop_inv {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (c : Cost.Data) (env : Cost.Env) (rem acc : List Cost.Data) {r : Cost.Data} {t : ℕ} : Cost.Eval (mapState c rem acc :: env) (mapBody univ).loop r t → ∃ (rs : List Cost.Data), List.Forall₂ (fun (q r : Cost.Data) => ∃ (t' : ℕ), univ.Runs (c.cons q) r t') rem rs ∧ r = Cost.Data.list (rs.reverse ++ acc)

Inversion of the loop: a halting loop ran every call.

def MIPRE.Tailored.Calls.mapCallCost (m T C Z : ℕ) : ℕ

The cost of mapCall with calls of cost at most T, m queries and sizes at most Z.

Equations

• MIPRE.Tailored.Calls.mapCallCost m T C Z = (m + 1) * (T + 3 * C + 2 * Z + 25) + (m + 2) * (Z + 13) + 4 * C + 3 * Z + 20

theorem MIPRE.Tailored.Calls.mapCall_runs {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (c : Cost.Data) (qs : List Cost.Data) (f : Cost.Data → Cost.Data) (T Z : ℕ) (hq : ∀ q ∈ qs, ∃ t ≤ T, univ.Runs (c.cons q) (f q) t) (hZ : (Cost.Data.list qs).size + (Cost.Data.list (List.map f qs)).size + 1 ≤ Z) : ∃ t ≤ mapCallCost qs.length T c.size Z, (mapCall univ).Runs (c.cons (Cost.Data.list qs)) (Cost.Data.list (List.map f qs)) t

The loop of calls with the results known.

theorem MIPRE.Tailored.Calls.mapCall_inv {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (c : Cost.Data) (qs : List Cost.Data) {r : Cost.Data} {t : ℕ} (h : (mapCall univ).Runs (c.cons (Cost.Data.list qs)) r t) : ∃ (rs : List Cost.Data), List.Forall₂ (fun (q r : Cost.Data) => ∃ (t' : ℕ), univ.Runs (c.cons q) r t') qs rs ∧ r = Cost.Data.list rs

Inversion of the loop of calls: a halting run ran univ on every query, and returned the results in order.

Runs within a bound

def MIPRE.Tailored.Calls.RunsLe (p : Cost.Prog) (x r : Cost.Data) (T : ℕ) : Prop

p runs on x to r within cost T.

Equations

• MIPRE.Tailored.Calls.RunsLe p x r T = ∃ t ≤ T, p.Runs x r t

theorem MIPRE.Tailored.Calls.RunsLe.runs {p : Cost.Prog} {x r : Cost.Data} {T : ℕ} (h : RunsLe p x r T) : ∃ (t : ℕ), p.Runs x r t

theorem MIPRE.Tailored.Calls.RunsLe.mono {p : Cost.Prog} {x r : Cost.Data} {T T' : ℕ} (h : RunsLe p x r T) (hT : T ≤ T') : RunsLe p x r T'

theorem MIPRE.Tailored.Calls.RunsLe.seq {p q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) {x v r : Cost.Data} {S T : ℕ} (hp : RunsLe p x v S) (hq' : RunsLe q v r T) : RunsLe (Calls.seq p q) x r (S + T + 1)

theorem MIPRE.Tailored.Calls.RunsLe.withCtx {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (a : Cost.Data) {b r : Cost.Data} {T : ℕ} (h : RunsLe p b r T) : RunsLe (Calls.withCtx p) (a.cons b) (a.cons r) (a.size + b.size + T + 5)

theorem MIPRE.Tailored.Calls.RunsLe.pure {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (F : Cost.PolyTimeFun α β) (a : α) : RunsLe F.code (Cost.encode a) (Cost.encode (F.toFun a)) (Polynomial.eval (Cost.esize a) F.timeBound)

theorem MIPRE.Tailored.Calls.RunsLe.size_le {p : Cost.Prog} {x r : Cost.Data} {T : ℕ} (h : RunsLe p x r T) : r.size ≤ T

theorem MIPRE.Tailored.Calls.RunsLe.mapCall {univ : Cost.Prog} (hU : Cost.Prog.WellScoped 1 univ) (c : Cost.Data) (qs : List Cost.Data) (f : Cost.Data → Cost.Data) (T Z : ℕ) (hq : ∀ q ∈ qs, RunsLe univ (c.cons q) (f q) T) (hZ : (Cost.Data.list qs).size + (Cost.Data.list (List.map f qs)).size + 1 ≤ Z) : RunsLe (Calls.mapCall univ) (c.cons (Cost.Data.list qs)) (Cost.Data.list (List.map f qs)) (mapCallCost qs.length T c.size Z)