Stages of the class verifier's programs

The sampler and the decider of the class verifier of the polynomial-time halting reduction (Halting/Paper/ClassVerifier.lean) are chains of stages: polynomial-time functions (PolyTimeFun, run by their code), calls of the universal machine on a program and an input the previous stage produced, and one binary-to-unary conversion of the sampler's dimension. The universal calls and the conversion are not PolyTimeFuns — the first is polynomial in the simulated program's own time, the second in the number it converts — so the chain is assembled at the level of programs and Eval, with forward run lemmas: each stage is a closed program, seq p q runs p then q on its output, and the cost of the chain is the sum of the stages' costs plus the sizes of the intermediate values.

• runUK univ on encode ((c, v), s) runs univ on (c, v) and returns encode (s, r), keeping the state s; runU univ returns r alone.
• unaryStage on encode (s, n) returns encode (s, unary n) (toUnaryProg).
• The polynomial-time pieces: expBits (u ↦ 2 ^ |u|), addConstU K (u ↦ unary (K + |u|)), unaryMul D (u ↦ unary (D · |u|)), lenBin (the length of a string, in binary).

Sequencing, and the universal calls

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

Run p, then the closed program q on its output.

Equations

• p.seq q = p.let_ (MIPRE.Cost.Prog.callVar 0 q)

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

theorem MIPRE.Cost.Prog.seq_runs {p q : Prog} (hq : WellScoped 1 q) {x y r : Data} {t₁ t₂ : ℕ} (hp : p.Runs x y t₁) (hq' : q.Runs y r t₂) : (p.seq q).Runs x r (t₁ + (y.size + 1 + t₂ + 1) + 1)

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

Run the universal program on the pair in the input's first component, keeping the second: encode ((c, v), s) ↦ encode (s, r) where c on v returns r.

Equations

• univ.runUK = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil ((MIPRE.Cost.Prog.callVar 0 univ).let_ ((MIPRE.Cost.Prog.var 2).cons (MIPRE.Cost.Prog.var 0)))

theorem MIPRE.Cost.Prog.runUK_wellScoped {univ : Prog} (hU : WellScoped 1 univ) : WellScoped 1 univ.runUK

theorem MIPRE.Cost.Prog.runUK_runs {univ : Prog} (hU : WellScoped 1 univ) {A B r : Data} {t : ℕ} (h : univ.Runs A r t) : ∃ t' ≤ A.size + B.size + r.size + t + 8, univ.runUK.Runs (A.cons B) (B.cons r) t'

def MIPRE.Cost.Prog.unaryStage : Prog

Convert the second component from binary to unary: encode (s, n) ↦ encode (s, unary n).

Equations

• MIPRE.Cost.Prog.unaryStage = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil ((MIPRE.Cost.Prog.var 0).cons (MIPRE.Cost.Prog.callVar 1 MIPRE.Cost.Prog.toUnaryProg))

theorem MIPRE.Cost.Prog.unaryStage_wellScoped : WellScoped 1 unaryStage

theorem MIPRE.Cost.Prog.unaryStage_runs (S : Data) (n : ℕ) : ∃ t ≤ S.size + esize n + (n.size + 2) * ((n + 1) * (4 * n + 14) + 7 * esize n + 8 * n + 90) + 5, unaryStage.Runs (S.cons (encode n)) (S.cons (Data.ofNat n)) t

Polynomial-time pieces

noncomputable def MIPRE.Cost.PolyTimeFun.expBits : PolyTimeFun Unary ℕ

u ↦ 2 ^ |u| on unary numerals, by expBitsProg.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.expBits_apply (u : Unary) : expBits.toFun u = 2 ^ List.length u

noncomputable def MIPRE.Cost.PolyTimeFun.addConstU (K : ℕ) : PolyTimeFun Unary Unary

u ↦ unary (K + |u|), by addConstProg.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.addConstU_apply (K : ℕ) (u : Unary) : (addConstU K).toFun u = unary (K + List.length u)

noncomputable def MIPRE.Cost.PolyTimeFun.unaryMul : ℕ → PolyTimeFun Unary Unary

u ↦ unary (D · |u|): D copies of u, appended.

Equations

• MIPRE.Cost.PolyTimeFun.unaryMul 0 = MIPRE.Cost.PolyTimeFun.const []
• MIPRE.Cost.PolyTimeFun.unaryMul D.succ = MIPRE.Cost.PolyTimeFun.append.comp ((MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary).pair (MIPRE.Cost.PolyTimeFun.unaryMul D))

theorem MIPRE.Cost.PolyTimeFun.unaryMul_apply (D : ℕ) (u : Unary) : (unaryMul D).toFun u = unary (D * List.length u)

noncomputable def MIPRE.Cost.PolyTimeFun.lenBin {α : Type u_1} [SizedEncoding α] : PolyTimeFun (List α) ℕ

The length of a string, in binary.

Equations

• MIPRE.Cost.PolyTimeFun.lenBin = MIPRE.Cost.PolyTimeFun.unaryToBin.comp MIPRE.Cost.PolyTimeFun.length

@[simp]

theorem MIPRE.Cost.PolyTimeFun.lenBin_apply {α : Type u_1} [SizedEncoding α] (l : List α) : lenBin.toFun l = l.length