A tailored verifier as a normal form verifier

Paper II, II:1757–1787. A tailored normal form verifier (S, L, LP) is a normal form verifier whose decider is the canonical decider; TailoredVerifier.ofTNFV U V is that verifier, the canonical decider written as a program (canonProg) and wrapped in the question-length check of def:normal-verifier (Verifier.ofSamplerDecider, which runs it through the universal machine U).

• tgame_accepts_iff: the n-th tailored game V.tgame n accepts (a, b) at (x, y) exactly when the canonical decider does — when the answer-length calculator and the linear-constraints processor halt, by the determinism of the model, and both reject when they do not.
• ofTNFV_accepts_iff: so the normal form verifier's decider accepts exactly what the tailored game accepts.
• valStar_ofTNFV: the values agree, for every answer bound T above the answer lengths of the tailored game (Verifier.valStar_eq_of_rejects' argument: answers longer than the lengths are rejected).
• hasPerfectPCC_ofTNFV: a perfect ZPC strategy for the doubled tailored game is a perfect PCC strategy of the doubled game of ofTNFV U V (lem:zpc-pcc).

So the existing pipeline's statements about MIPRE.Verifier — its soundness analyses in value form, its completeness notion HasPerfectPCC — apply to tailored verifiers through ofTNFV. The running time of the canonical decider, which Verifier.IsBounded of ofTNFV U V needs, is not bounded here: the halting protocol of Phase 1 reasons about tailored verifiers directly.

theorem MIPRE.Tailored.TailoredVerifier.lenOf_eq {ℓ : ℕ} (V : TailoredVerifier ℓ) {n : ℕ} {x : Cost.BitStr} {κ : Bool} {d : Cost.Data} {t : ℕ} (h : V.len.prog.Runs (Cost.encode (n, x, κ)) d t) : V.lenOf n x κ = d.spineList.length

theorem MIPRE.Tailored.TailoredVerifier.lenDefined_of {ℓ : ℕ} (V : TailoredVerifier ℓ) {n : ℕ} {x : Cost.BitStr} {d₀ d₁ : Cost.Data} {t₀ t₁ : ℕ} (h₀ : V.len.prog.Runs (Cost.encode (n, x, false)) d₀ t₀) (h₁ : V.len.prog.Runs (Cost.encode (n, x, true)) d₁ t₁) : V.LenDefined n x

theorem MIPRE.Tailored.TailoredVerifier.consOf_eq {ℓ : ℕ} (V : TailoredVerifier ℓ) {n : ℕ} {x y aR bR : Cost.BitStr} (hx : V.LenDefined n x) (hy : V.LenDefined n y) {d : Cost.Data} {t : ℕ} (h : V.lp.prog.Runs (Cost.encode (n, x, y, aR, bR)) d t) : V.consOf n x y aR bR = d.bitsListD

theorem MIPRE.Tailored.TailoredVerifier.consOf_eq_reject {ℓ : ℕ} (V : TailoredVerifier ℓ) {n : ℕ} {x y aR bR : Cost.BitStr} (h : ¬(V.LenDefined n x ∧ V.LenDefined n y ∧ ∃ (cs : List Cost.BitStr), LpIs V.lp n x y aR bR cs)) : ∃ (d : ℕ), V.consOf n x y aR bR = [rejectConstraint d]

theorem MIPRE.Tailored.TailoredVerifier.tgame_accepts_iff {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) (x y : V.Questions n) (a b : Cost.BitStr) : (V.tgame n).Accepts x y a b ↔ ∃ (t : ℕ), (canonProg V.len.prog V.lp.prog).Runs (Cost.encode (n, CL.toBits x, CL.toBits y, a, b)) (Cost.encode true) t

The tailored game accepts exactly what the canonical decider accepts.

noncomputable def MIPRE.Tailored.TailoredVerifier.ofTNFV {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) : Verifier ℓ

A tailored verifier as a normal form verifier: its sampler, and the canonical decider as a program, wrapped in the question-length check.

Equations

• V.ofTNFV U = MIPRE.Verifier.ofSamplerDecider U V.sampler (MIPRE.Tailored.canonProg V.len.prog V.lp.prog)

@[simp]

theorem MIPRE.Tailored.TailoredVerifier.ofTNFV_sampler {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) : (V.ofTNFV U).sampler = V.sampler

theorem MIPRE.Tailored.TailoredVerifier.ofTNFV_accepts_iff {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) (n : ℕ) (x y : V.Questions n) (a b : Cost.BitStr) : (V.ofTNFV U).decider.Accepts n (CL.toBits x) (CL.toBits y) a b ↔ (V.tgame n).Accepts x y a b

The normal form verifier's decider accepts exactly what the tailored game accepts.

theorem MIPRE.Tailored.TailoredVerifier.ofTNFV_game_D {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame n).maxLen ≤ T) (x y : V.Questions n) (a b : Verifier.Answers (V.tgame n).maxLen) : ((V.ofTNFV U).game n T).D x y ((Verifier.Answers.castLE hT) a) ((Verifier.Answers.castLE hT) b) = (V.tgame n).toGame.D x y a b

The decision predicates agree on the answers the tailored game has, embedded in the answers of length at most T.

theorem MIPRE.Tailored.TailoredVerifier.valStar_ofTNFV {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) (n T : ℕ) (hT : (V.tgame n).maxLen ≤ T) : (V.ofTNFV U).valStar n T = V.valStar n

The values agree, for an answer bound above the tailored game's answer lengths.

theorem MIPRE.Tailored.TailoredVerifier.hasPerfectPCC_ofTNFV {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame n).maxLen ≤ T) (h : V.HasPerfectZPC n) : (V.ofTNFV U).HasPerfectPCC n T

A perfect ZPC strategy gives a perfect PCC strategy of ofTNFV (lem:zpc-pcc), for an answer bound above the tailored game's answer lengths.