The tailored halting verifier: the linear-constraints processor

Paper II, II:1887–2001 (the map F, the verifier V^{M,λ}, lem:dhalt-values), along the route of MIPRE/Foundations/Halting/Paper/Decider.lean, which this file parallels with the linear-constraints processor in the role of the decider. For a tailored gap compression TG, a machine M, a search program S' and a parameter λ, the verifier is

Vhalt TG U UT S' M λ = (S^λ, L^λ, lp M λ),

the compressed sampler and answer-length calculator at λ with the linear-constraints processor lp M λ, the efficient Kleene fixed point (Cost.kleeneFix) of P ↦ hardcode body (encode (M, (λ, P))). On (n, x, y, a^R, b^R) it runs body on its own description and the input, and body:

1. runs M on the empty input for the budget Nat.size n; if it halts, outputs the empty list of constraints, which accepts every answer pair of the right lengths;
2. otherwise runs the search program S' on the description descOf λ (lp M λ) for the budget Nat.size n; if it halts, outputs the list [J] (rejectConstraint 0), which rejects every answer pair;
3. otherwise computes the compressed linear-constraints processor Compress ((S^λ, L^λ, lp M λ), λ) of its own verifier and runs it on the input through the universal machine.

Branches 1 and 3 are the paper's F (II:1900), with "accept" the empty list and "reject" the list {J}. Branch 2 is Lin's search branch, which the existing halting layer has too: the value form of compression has no base case for soundness, and the search supplies it.

• lp_runs_iff (lem:dhalt-values): the processor's output, branch by branch.
• hasPerfectZPC_of_branch1, valStar_eq_zero_of_branch2: the first two branches decide the level outright — a perfect ZPC strategy, the trivial one (hasPerfectZPC_of_accepts_zero), and value 0.
• hasPerfectZPC_iff_W, valStar_eq_W: otherwise the level is that of the compressed verifier W, the output of TG on the verifier's own programs, with which it shares the sampler and the answer-length calculator, and whose processor outputs the same constraints there.

The construction

def MIPRE.Tailored.Halting.acceptProg : Cost.Prog

The program outputting the empty list of constraints, which accepts every answer pair of the right lengths.

Equations

• MIPRE.Tailored.Halting.acceptProg = MIPRE.Cost.Prog.const (MIPRE.Cost.encode [])

def MIPRE.Tailored.Halting.rejectProg : Cost.Prog

The program outputting the list [J], which rejects every answer pair.

Equations

• MIPRE.Tailored.Halting.rejectProg = MIPRE.Cost.Prog.const (MIPRE.Cost.encode [MIPRE.Tailored.rejectConstraint 0])

noncomputable def MIPRE.Tailored.Halting.comprLp {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (lam : ℕ) (P : Cost.Prog) : Cost.Prog

The compressed linear-constraints processor of the verifier (S^λ, L^λ, P).

Equations

• MIPRE.Tailored.Halting.comprLp TG lam P = TG.compress.toFun ((TG.samplerProg.toFun lam, TG.lenProg.toFun lam, P), lam)

noncomputable def MIPRE.Tailored.Halting.prep {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyTimeFun ((Cost.Prog × ℕ × Cost.Prog) × ℕ × Cost.Data) (Cost.Prog × Cost.Data)

The three branches, as a polynomial-time function of the description (M, (λ, P)) and the input (n, rest): the program to run and its input.

Equations

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

theorem MIPRE.Tailored.Halting.prep_apply {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (P : Cost.Prog) (n : ℕ) (rest : Cost.Data) : (prep TG UT S').toFun ((M, lam, P), n, rest) = if (Cost.evalWithin M Cost.Data.nil n.size).isSome = true then (acceptProg, Cost.Data.nil) else if (Cost.evalWithin (Halting.searchP S' lam P) Cost.Data.nil n.size).isSome = true then (rejectProg, Cost.Data.nil) else (comprLp TG lam P, Cost.encode (n, rest))

noncomputable def MIPRE.Tailored.Halting.body {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.Prog

The body of the processor: run prep, then the universal machine on its output.

Equations

• MIPRE.Tailored.Halting.body TG U UT S' = (MIPRE.Tailored.Halting.prep TG UT S').code.let_ (MIPRE.Cost.Prog.callVar 0 U.univ)

theorem MIPRE.Tailored.Halting.body_wellScoped {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.Prog.WellScoped 1 (body TG U UT S')

noncomputable def MIPRE.Tailored.Halting.F {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.PolyTimeFun Cost.Prog Cost.Prog

The map whose fixed point is the processor: P ↦ hardcode body (encode (M, (λ, P))).

Equations

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

theorem MIPRE.Tailored.Halting.F_apply {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (P : Cost.Prog) : (F TG U UT S' M lam).toFun P = Cost.hardcode (body TG U UT S') (Cost.encode (M, lam, P))

noncomputable def MIPRE.Tailored.Halting.lpProg {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.Prog

The linear-constraints processor LP^{M,λ}: the efficient Kleene fixed point of F.

Equations

• MIPRE.Tailored.Halting.lpProg TG U UT S' M lam = MIPRE.Cost.kleeneFix U (MIPRE.Tailored.Halting.F TG U UT S' M lam)

noncomputable def MIPRE.Tailored.Halting.lp {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Decider

LP^{M,λ}, as a closed program.

Equations

• MIPRE.Tailored.Halting.lp TG U UT S' M lam = { prog := MIPRE.Tailored.Halting.lpProg TG U UT S' M lam, closed := ⋯ }

noncomputable def MIPRE.Tailored.Halting.Vhalt {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : TailoredVerifier ℓ

The tailored verifier V^{M,λ} (II:1925): the compressed sampler and answer-length calculator at λ, and the processor LP^{M,λ}.

Equations

• MIPRE.Tailored.Halting.Vhalt TG U UT S' M lam = { sampler := TG.sampler lam, len := TG.len lam, lp := MIPRE.Tailored.Halting.lp TG U UT S' M lam }

@[simp]

theorem MIPRE.Tailored.Halting.Vhalt_sampler {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (Vhalt TG U UT S' M lam).sampler = TG.sampler lam

@[simp]

theorem MIPRE.Tailored.Halting.Vhalt_len {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (Vhalt TG U UT S' M lam).len = TG.len lam

theorem MIPRE.Tailored.Halting.Vhalt_lp_prog {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (Vhalt TG U UT S' M lam).lp.prog = lpProg TG U UT S' M lam

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Halting.W {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : TailoredVerifier ℓ

The compressed verifier of V^{M,λ}: the output of TG on its own programs, the same at every level.

Equations

• MIPRE.Tailored.Halting.W TG U UT S' M lam = TG.output (MIPRE.Tailored.Halting.Vhalt TG U UT S' M lam).progs lam

theorem MIPRE.Tailored.Halting.W_lp_prog {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (W TG U UT S' M lam).lp.prog = comprLp TG lam (lpProg TG U UT S' M lam)

Running the processor

theorem MIPRE.Tailored.Halting.body_runs_iff {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (P : Cost.Prog × ℕ × Cost.Prog) (n : ℕ) (rest r : Cost.Data) : (∃ (t : ℕ), (body TG U UT S').Runs (Cost.encode (P, n, rest)) r t) ↔ ∃ (t : ℕ), ((prep TG UT S').toFun (P, n, rest)).1.Runs ((prep TG UT S').toFun (P, n, rest)).2 r t

A run of body on (P, (n, rest)) is a run of the program prep returns on the input it returns.

theorem MIPRE.Tailored.Halting.lpProg_runs_iff {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (v r : Cost.Data) : (∃ (t : ℕ), (lpProg TG U UT S' M lam).Runs v r t) ↔ ∃ (t : ℕ), (body TG U UT S').Runs ((Cost.encode (M, lam, lpProg TG U UT S' M lam)).cons v) r t

A run of the processor on v is a run of body on its own description and v.

@[reducible, inline]

abbrev MIPRE.Tailored.Halting.branch1 (M : Cost.Prog) (n : ℕ) : Prop

The first branch fires at the level n: M halts within Nat.size n.

Equations

• MIPRE.Tailored.Halting.branch1 M n = ((MIPRE.Cost.evalWithin M MIPRE.Cost.Data.nil n.size).isSome = true)

@[reducible, inline]

abbrev MIPRE.Tailored.Halting.branch2 {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) : Prop

The second branch fires at the level n: the search halts within Nat.size n.

Equations

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

theorem MIPRE.Tailored.Halting.lp_runs_iff {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) (rest r : Cost.Data) : (∃ (t : ℕ), (lpProg TG U UT S' M lam).Runs (Cost.encode (n, rest)) r t) ↔ if branch1 M n then r = Cost.encode [] else if branch2 TG U UT S' M lam n then r = Cost.encode [rejectConstraint 0] else ∃ (t : ℕ), (comprLp TG lam (lpProg TG U UT S' M lam)).Runs (Cost.encode (n, rest)) r t

The outputs of LP^{M,λ} (lem:dhalt-values): on an input of index n, the empty list if M halts within Nat.size n; otherwise [J] if the search halts within Nat.size n; otherwise exactly what the compressed processor outputs.

The level, by branch

theorem MIPRE.Tailored.Halting.lenDefined {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) (x : (Vhalt TG U UT S' M lam).Questions n) : (Vhalt TG U UT S' M lam).LenDefined n (CL.toBits x)

The answer-length calculator halts at every question of the sampler.

theorem MIPRE.Tailored.Halting.hasPerfectZPC_of_branch1 {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : branch1 M n) : (Vhalt TG U UT S' M lam).HasPerfectZPC n

The first branch: at a level where M has halted, V^{M,λ} has a perfect ZPC strategy, the trivial one: every constraint list is empty.

theorem MIPRE.Tailored.Halting.valStar_eq_zero_of_branch2 {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : ¬branch1 M n) (h2 : branch2 TG U UT S' M lam n) : (Vhalt TG U UT S' M lam).valStar n = 0

The second branch: at a level where the search has halted and M has not, V^{M,λ} has value 0: every constraint list holds a rejecting constraint.

theorem MIPRE.Tailored.Halting.lpIs_iff_W {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : ¬branch1 M n) (h2 : ¬branch2 TG U UT S' M lam n) (x y aR bR : Cost.BitStr) (cs : List Cost.BitStr) : LpIs (Vhalt TG U UT S' M lam).lp n x y aR bR cs ↔ LpIs (W TG U UT S' M lam).lp n x y aR bR cs

Off the first two branches, V^{M,λ} and its compressed verifier output the same constraints at the level n.

theorem MIPRE.Tailored.Halting.hasPerfectZPC_iff_W {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : ¬branch1 M n) (h2 : ¬branch2 TG U UT S' M lam n) : (Vhalt TG U UT S' M lam).HasPerfectZPC n ↔ (W TG U UT S' M lam).HasPerfectZPC n

Off the first two branches, completeness is the compressed verifier's.

theorem MIPRE.Tailored.Halting.valStar_eq_W {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : ¬branch1 M n) (h2 : ¬branch2 TG U UT S' M lam n) : (Vhalt TG U UT S' M lam).valStar n = (W TG U UT S' M lam).valStar n

Off the first two branches, the value is the compressed verifier's.