The class TMIP* as the paper defines it: polynomial-time tailored verifiers

Paper II, II:787 and II:1505 (clause (1) of thm:tailored_MIP*=RE): a language is in TMIP* when a polynomial-time procedure presents, on every input z, a tailored game G_z, sampling a question pair and evaluating the canonical decider in time poly(|z|), with a perfect ZPC strategy on the members and value at most 1/2 off them. MIPRE.Tailored.TMIPStarComputable (Tailored/Class.lean) is the computable version, with G_z an explicit description computed with no time bound; this file is the class itself, as Foundations/ClassMIPStar.lean is for MIP*.

The reading

A TPolyVerifier is three closed programs and one polynomial P; write B z = P(|z|).

• The sampler is MIP*'s (PolyVerifier, through toPoly): on (z, r), for a uniform seed r of length B z, a question pair of strings of length at most B z. The question distribution of G_z is the pushforward of the seed (PolyVerifier.game).
• The answer-length calculator, on (z, x, κ), outputs the number of readable (κ = false) or linear variables at the question x, read in unary, as MIPRE.Tailored.LenIs reads the calculator of a tailored normal form verifier.
• The linear-constraints processor, on (z, x, y, a^R, b^R), outputs the constraints L_xy(a^R b^R), read by Data.bitsListD, as MIPRE.Tailored.LpIs does.

tgame z is the tailored game on the strings of length at most B z, with the constraint list that rejects everything where a program does not halt (consOf), as TailoredVerifier.tgame. Efficiency (Efficient) bounds the three programs by P of the total input length, as PolyVerifier.Efficient bounds the sampler and the decider; the canonical decider itself is then a polynomial-time check on what they output (Tailored/Canonical.lean). Its running time, for tailored normal form verifiers, is Tailored/CanonicalCost.lean's; no statement here needs it.

TMIPStar L: some polynomial-time tailored verifier is efficient on every input, its doubled game has a perfect ZPC strategy on the members of L, and its game has value at most 1/2 off them. The completeness clause is read on the doubled game, as TailoredVerifier.HasPerfectZPC reads the paper's for tailored normal form verifiers and TailoredGapCompression.completeness transports it. Tailored/ClassPolyTab.lean puts the class inside the computable one, hence in RE, and Tailored/ClassVerifier.lean proves TMIPStar = IsRE from a tailored gap compression.

structure MIPRE.Tailored.TPolyVerifier : Type

A polynomial-time tailored verifier (II:1505): a sampler, an answer-length calculator, a linear-constraints processor and one polynomial time bound.

• sampler : Cost.Prog

  The sampler program; its input is encode (z, r) for the input z and a seed r.

• sampler_closed : Cost.Prog.WellScoped 1 self.sampler
• len : Cost.Prog

  The answer-length calculator; its input is encode (z, x, κ).

• len_closed : Cost.Prog.WellScoped 1 self.len
• lp : Cost.Prog

  The linear-constraints processor; its input is encode (z, x, y, a^R, b^R).

• lp_closed : Cost.Prog.WellScoped 1 self.lp
• bound : Polynomial ℕ

  The polynomial P of the time bounds.

def MIPRE.Tailored.TPolyVerifier.toPoly (V : TPolyVerifier) : PolyVerifier

The sampler and the bound, as a PolyVerifier whose decider is never used: its seeds, its question pairs and its question distribution are the tailored verifier's.

Equations

• V.toPoly = { sampler := V.sampler, sampler_closed := ⋯, decider := V.sampler, decider_closed := ⋯, bound := V.bound }

@[reducible, inline]

abbrev MIPRE.Tailored.TPolyVerifier.B (V : TPolyVerifier) (z : Cost.BitStr) : ℕ

The bound B z = P(|z|): the seed length, and the length of the questions.

Equations

• V.B z = V.toPoly.B z

def MIPRE.Tailored.TPolyVerifier.LenIs (V : TPolyVerifier) (z x : Cost.BitStr) (κ : Bool) (k : ℕ) : Prop

The answer-length calculator outputs k on (z, x, κ), read in unary.

Equations

• V.LenIs z x κ k = ∃ (t : ℕ) (d : MIPRE.Cost.Data), V.len.Runs (MIPRE.Cost.encode (z, x, κ)) d t ∧ d.spineList.length = k

def MIPRE.Tailored.TPolyVerifier.LpIs (V : TPolyVerifier) (z x y aR bR : Cost.BitStr) (cs : List Cost.BitStr) : Prop

The linear-constraints processor outputs cs on (z, x, y, a^R, b^R).

Equations

• V.LpIs z x y aR bR cs = ∃ (t : ℕ) (d : MIPRE.Cost.Data), V.lp.Runs (MIPRE.Cost.encode (z, x, y, aR, bR)) d t ∧ d.bitsListD = cs

noncomputable def MIPRE.Tailored.TPolyVerifier.lenOf (V : TPolyVerifier) (z x : Cost.BitStr) (κ : Bool) : ℕ

The length the calculator outputs on (z, x, κ), and 0 when it does not halt.

Equations

• V.lenOf z x κ = if h : ∃ (k : ℕ), V.LenIs z x κ k then h.choose else 0

def MIPRE.Tailored.TPolyVerifier.LenDefined (V : TPolyVerifier) (z x : Cost.BitStr) : Prop

The calculator halts at the question x, for both kinds of variables.

Equations

• V.LenDefined z x = ∀ (κ : Bool), ∃ (k : ℕ), V.LenIs z x κ k

noncomputable def MIPRE.Tailored.TPolyVerifier.consOf (V : TPolyVerifier) (z x y aR bR : Cost.BitStr) : List Cost.BitStr

The constraints at (x, y): what the processor outputs when the calculator halts at both questions and the processor halts; otherwise the list that rejects everything.

Equations

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

noncomputable def MIPRE.Tailored.TPolyVerifier.tgame (V : TPolyVerifier) (z : Cost.BitStr) : TailoredGame (Verifier.Answers (V.B z))

The game G_z: questions the strings of length at most B z, distributed as the sampler's output on a uniform seed, lengths and constraints as the calculator and the processor compute them.

Equations

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

structure MIPRE.Tailored.TPolyVerifier.Efficient (V : TPolyVerifier) (z : Cost.BitStr) : Prop

Efficiency on the input z (II:1505, clause (1)): the sampler's clause of PolyVerifier.Efficient, and the calculator and the processor halting within P of the total input length on every input.

• sampler_runs : V.toPoly.SamplerRuns z
• len_time (x : Cost.BitStr) (κ : Bool) : Cost.HaltsWithin V.len (Cost.encode (z, x, κ)) (Polynomial.eval (List.length z + List.length x) V.bound)
• lp_time (x y aR bR : Cost.BitStr) : Cost.HaltsWithin V.lp (Cost.encode (z, x, y, aR, bR)) (Polynomial.eval (List.length z + List.length x + List.length y + List.length aR + List.length bR) V.bound)

The outputs are determined

theorem MIPRE.Tailored.TPolyVerifier.LenIs.unique (V : TPolyVerifier) {z x : Cost.BitStr} {κ : Bool} {k k' : ℕ} (h : V.LenIs z x κ k) (h' : V.LenIs z x κ k') : k = k'

theorem MIPRE.Tailored.TPolyVerifier.LpIs.unique (V : TPolyVerifier) {z x y aR bR : Cost.BitStr} {cs cs' : List Cost.BitStr} (h : V.LpIs z x y aR bR cs) (h' : V.LpIs z x y aR bR cs') : cs = cs'

theorem MIPRE.Tailored.TPolyVerifier.lenOf_eq (V : TPolyVerifier) {z x : Cost.BitStr} {κ : Bool} {k : ℕ} (h : V.LenIs z x κ k) : V.lenOf z x κ = k

theorem MIPRE.Tailored.TPolyVerifier.consOf_eq (V : TPolyVerifier) {z x y aR bR : Cost.BitStr} (hx : V.LenDefined z x) (hy : V.LenDefined z y) {cs : List Cost.BitStr} (h : V.LpIs z x y aR bR cs) : V.consOf z x y aR bR = cs

def MIPRE.Tailored.TMIPStar (L : Set Cost.BitStr) : Prop

TMIP*, the paper's class (II:787). A language L is in it if some polynomial-time tailored verifier is efficient on every input, its doubled game has a perfect ZPC strategy on the members of L, and its game has value at most 1/2 off them.

Equations

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