The running time of the canonical decider

P1b deferred the cost of the canonical decider canonProg L LP (MIPRE.Tailored.Canonical): a bound on the running time of a decider in MIPRE.Verifier.TimeBoundAt quantifies over every input (n, d), malformed ones included, while the steps of canonProg are polynomial-time functions, whose bounds hold on encodings only. This file puts a total parse in front (parseDIn, the identity on encodings, canonProgT L LP) and bounds the running time.

• pushProg_runs_le, step_runs: a step of the decider, timed — the call's input built from the state, the input program run within its bound, the output pushed;
• parseDIn, canonProgT, canonProgT_runs_iff: the parse reads (n, x, y, a, b) off any data, and is the identity on encodings, so the decider accepts what canonProg accepts;
• canonProgT_halts: on every input (n, d) the decider halts within the explicit canonBound, when L and LP halt within T (|d'| + 1)^k on every (n, d') — every call's argument is a component of the parsed input, of size linear in |d|;
• canonProgT_timeBound: hence within c (T + 10^k + |n| + 1)^m (|d| + 1)^{e (k + 1)} for constants c, m, e independent of everything (dom_canonBound, with the domination tools of the repeated programs);
• esize_canonProgT: its description is 4 |L| + |LP| plus a constant.

What remains for MIPRE.Verifier.IsBounded of the normal form verifier a tailored verifier denotes, at a λ' linear in λ, is the wrapper of Verifier.ofSamplerDecider (the question-length check and the universal machine), whose explicit cost is wrapCore_cost'.

theorem MIPRE.Cost.Prog.pushProg_runs_le {F P : Prog} (hP : WellScoped 1 P) {s v r : Data} {t₁ t₂ : ℕ} (h₁ : F.Runs s v t₁) (h₂ : P.Runs v r t₂) : ∃ t ≤ t₁ + t₂ + v.size + r.size + s.size + 8, (F.pushProg P).Runs s (r.cons s) t

The total parse

noncomputable def MIPRE.Tailored.parseDIn : Cost.PolyTimeFun Cost.Data DIn

Read a decider's input (n, x, y, a, b) off any data, the identity on encodings.

Equations

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

theorem MIPRE.Tailored.parseDIn_encode (i : DIn) : parseDIn.toFun (Cost.encode i) = i

theorem MIPRE.Tailored.size_treeHead_le (d : Cost.Data) : (Cost.PolyTimeFun.treeHead.toFun d).size ≤ d.size

theorem MIPRE.Tailored.size_treeTail_le (d : Cost.Data) : (Cost.PolyTimeFun.treeTail.toFun d).size ≤ d.size

theorem MIPRE.Tailored.length_rawList_le' (d : Cost.Data) : (CL.Detyping.Program.rawList d).length ≤ d.size

theorem MIPRE.Tailored.esize_readBits_le (d : Cost.Data) : Cost.esize (CL.Detyping.Program.readBits.toFun d) ≤ 4 * d.size + 1

theorem MIPRE.Tailored.parseDIn_fst (n : ℕ) (d : Cost.Data) : (parseDIn.toFun ((Cost.encode n).cons d)).1 = n

The parsed index is the index.

theorem MIPRE.Tailored.esize_parseDIn_le (n : ℕ) (d : Cost.Data) : Cost.esize (parseDIn.toFun ((Cost.encode n).cons d)).2.1 ≤ 4 * d.size + 1 ∧ Cost.esize (parseDIn.toFun ((Cost.encode n).cons d)).2.2.1 ≤ 4 * d.size + 1 ∧ Cost.esize (parseDIn.toFun ((Cost.encode n).cons d)).2.2.2.1 ≤ 4 * d.size + 1 ∧ Cost.esize (parseDIn.toFun ((Cost.encode n).cons d)).2.2.2.2 ≤ 4 * d.size + 1

The parsed strings are of size linear in the input.

theorem MIPRE.Tailored.length_parseDIn_le (n : ℕ) (d : Cost.Data) : List.length (parseDIn.toFun ((Cost.encode n).cons d)).2.2.2.1 ≤ d.size ∧ List.length (parseDIn.toFun ((Cost.encode n).cons d)).2.2.2.2 ≤ d.size

theorem MIPRE.Tailored.esize_bool_le' (b : Bool) : Cost.esize b ≤ 3

noncomputable def MIPRE.Tailored.canonProgT (L P : Cost.Prog) : Cost.Prog

The canonical decider with a total parse in front.

Equations

• MIPRE.Tailored.canonProgT L P = MIPRE.Cost.seqProg MIPRE.Tailored.parseDIn.code (MIPRE.Tailored.canonProg L P)

theorem MIPRE.Tailored.canonProgT_wellScoped {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) : Cost.Prog.WellScoped 1 (canonProgT L P)

theorem MIPRE.Tailored.canonProgT_runs_iff {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) (i : DIn) (out : Cost.Data) : (∃ (t : ℕ), (canonProgT L P).Runs (Cost.encode i) out t) ↔ ∃ (t : ℕ), (canonProg L P).Runs (Cost.encode i) out t

On encoded inputs the parse changes nothing.

One step: a call of an input program, pushed onto the state

theorem MIPRE.Tailored.step_runs {σ : Type u_1} {β : Type u_2} [Cost.SizedEncoding σ] [Cost.SizedEncoding β] (F : Cost.PolyTimeFun σ (ℕ × β)) {Q : Cost.Prog} (hQ : Cost.Prog.WellScoped 1 Q) {n T k : ℕ} (hQt : ∀ (d : Cost.Data), Cost.HaltsWithin Q ((Cost.encode n).cons d) (T * (d.size + 1) ^ k)) (s : σ) (hn : (F.toFun s).1 = n) {Z : ℕ} (hZ : Cost.esize (F.toFun s).2 + 1 ≤ Z) : ∃ (r : Cost.Data) (t : ℕ), (F.code.pushProg Q).Runs (Cost.encode s) (Cost.encode (r, s)) t ∧ r.size ≤ T * Z ^ k ∧ t ≤ 2 * Polynomial.eval (Cost.esize s) F.timeBound + 2 * (T * Z ^ k) + Cost.esize s + 8

A step of the canonical decider, timed: from the state s, build the input F s of a program Q whose first component is the index n, run Q within its time bound, and push the output.

The running time

noncomputable def MIPRE.Tailored.canonBound (T k S Z : ℕ) : ℕ

The explicit bound on the running time, from the time T · Z^k of a call and the sizes: S the size of the input, Z a bound on the calls' argument sizes.

Equations

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

theorem MIPRE.Tailored.canonProgT_halts {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) {n T k : ℕ} (hLt : ∀ (d : Cost.Data), Cost.HaltsWithin L ((Cost.encode n).cons d) (T * (d.size + 1) ^ k)) (hPt : ∀ (d : Cost.Data), Cost.HaltsWithin P ((Cost.encode n).cons d) (T * (d.size + 1) ^ k)) (d : Cost.Data) : Cost.HaltsWithin (canonProgT L P) ((Cost.encode n).cons d) (canonBound T k ((Cost.encode n).cons d).size (20 * d.size + 20))

The canonical decider halts within canonBound on every input (n, d), when L and LP halt within T (|d'| + 1)^k on every input (n, d').

The bound, dominated

noncomputable def MIPRE.Tailored.canonPoly : Polynomial ℕ

One polynomial bounding every stage, evaluated at the largest state size.

Equations

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

theorem MIPRE.Tailored.canonBound_le (T k S Z : ℕ) : canonBound T k S Z ≤ Polynomial.eval (5 * (T * Z ^ k) + Polynomial.eval S parseDIn.timeBound + 5) canonPoly

theorem MIPRE.Tailored.dom_canonBound : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K T S Z : ℕ), 1 ≤ X → 10 ^ K ≤ W → T ≤ W → S ≤ W + X → Z ≤ 20 * X → Repeat.Dom W X K c m e (canonBound T K S Z)

The canonical decider's bound is dominated: c (W + 1)^m X^{e (K + 1)}, for W above the call constant T, 10^K and the index's size, X the input's size plus one.

theorem MIPRE.Tailored.canonProgT_timeBound : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {L P : Cost.Prog}, Cost.Prog.WellScoped 1 L → Cost.Prog.WellScoped 1 P → ∀ {n T k : ℕ}, (∀ (d : Cost.Data), Cost.HaltsWithin L ((Cost.encode n).cons d) (T * (d.size + 1) ^ k)) → (∀ (d : Cost.Data), Cost.HaltsWithin P ((Cost.encode n).cons d) (T * (d.size + 1) ^ k)) → ∀ (d : Cost.Data), Cost.HaltsWithin (canonProgT L P) ((Cost.encode n).cons d) (c * (T + 10 ^ k + Cost.esize n + 1) ^ m * (d.size + 1) ^ (e * (k + 1)))

The running time of the canonical decider. There are constants c, m, e such that, when L and LP halt within T (|d| + 1)^k on every input (n, d), the canonical decider (with its total parse) halts within c (T + 10^k + |n| + 1)^m (|d| + 1)^{e (k + 1)} on every input (n, d), malformed ones included.

The description size

theorem MIPRE.Tailored.esize_canonProgT (L P : Cost.Prog) : Cost.esize (canonProgT L P) + 5 * Cost.esize Cost.Prog.nil = Cost.esize (canonProgT Cost.Prog.nil Cost.Prog.nil) + 4 * Cost.esize L + Cost.esize P

The canonical decider's description is linear in those of L and LP: L appears four times and LP once, the rest is fixed.