Tailored normal form verifiers

Paper II of the Aldous–Lyons track (Bowen–Chapman–Vidick, arXiv:2501.00173), §2.6 (II:1630–1832). A tailored normal form verifier is four machines (S, L, LP, D): a conditionally linear sampler, an answer-length calculator, a linear-constraints processor, and the fixed canonical decider. Here the canonical decider is not a field — it is the same for every verifier (TailoredGame.Accepts) — so a TailoredVerifier ℓ is the other three:

• sampler, a CL.Sampler ℓ, as in MIPRE.Verifier;
• len, the answer-length calculator: on encode (n, x, κ) it outputs the number ℓ^κ(x) of readable (κ = false) or linear (κ = true) variables at the question x of the n-th game (LenIs);
• lp, the linear-constraints processor: on encode (n, x, y, a^R, b^R) it outputs the list of constraints L_xy(a^R, b^R) (LpIs).

Both are closed programs whose input starts with the index n, so the structure MIPRE.Decider and its running-time bound Decider.TimeBoundAt serve for them; only the decider's notion of acceptance does not apply. Their outputs are read totally, so that no output is malformed and the canonical decider, which has to read them, needs no validity check: a length in unary, as the paper writes it (II:1781) — the length of the output's spine, (Cost.Data.spineList d).length — and a constraint list by Cost.Data.bitsListD, which on the encoding of a list of bit strings is that list. The length bound is still a separate clause (LenBound), in IsBounded and in the budgets, though the running time bounds a unary output.

• TailoredVerifier.tgame n: the n-th game 𝒱_n, a TailoredGame on the sampler's questions, read off the programs: a question at which len does not halt, or a pair at which lp does not, gets the constraint list that rejects everything, as a timeout is a rejection in the paper. The programs being deterministic, the choices made in reading them off are immaterial.
• valStar n, HasPerfectZPC n: the value of 𝒱_n, and the completeness notion of the track, a perfect Z-aligned permutation strategy commuting along edges of the doubled game — what Verifier.HasPerfectPCC is for the existing pipeline.
• IsBounded λ (II:1800) and Within n R: the paper's λ-boundedness and the budgets of the stage contracts, in the relative-cost reading of MIPRE.Verifier.IsBounded, with the length clause added.

TailoredVerifier.ofTNFV (MIPRE.Tailored.OfTNFV) packages a tailored verifier as a MIPRE.Verifier, the canonical decider written as a program (MIPRE.Tailored.Canonical).

Total readings of data

def MIPRE.Cost.Data.spineList : Data → List Data

The elements along the right spine: the list a datum encodes, every datum encoding one.

Equations

• MIPRE.Cost.Data.nil.spineList = []
• (a.cons d).spineList = a :: d.spineList

@[simp]

theorem MIPRE.Cost.Data.spineList_nil : nil.spineList = []

@[simp]

theorem MIPRE.Cost.Data.spineList_cons (a d : Data) : (a.cons d).spineList = a :: d.spineList

theorem MIPRE.Cost.Data.ofList_id_spineList (d : Data) : ofList id d.spineList = d

theorem MIPRE.Cost.Data.spineList_ofList {α : Type u_1} (f : α → Data) (l : List α) : (ofList f l).spineList = List.map f l

theorem MIPRE.Cost.Data.length_spineList_ofNat (k : ℕ) : (ofNat k).spineList.length = k

A length written in unary is read back.

def MIPRE.Cost.Data.bitD : Data → Bool

A datum read as a bit: nil is false, a node true.

Equations

• MIPRE.Cost.Data.nil.bitD = false
• (a.cons d).bitD = true

@[simp]

theorem MIPRE.Cost.Data.bitD_ofBool (b : Bool) : (ofBool b).bitD = b

def MIPRE.Cost.Data.bitsD (d : Data) : BitStr

A datum read as a bit string: its spine, elementwise.

Equations

• d.bitsD = List.map MIPRE.Cost.Data.bitD d.spineList

def MIPRE.Cost.Data.bitsListD (d : Data) : List BitStr

A datum read as a list of bit strings.

Equations

• d.bitsListD = List.map MIPRE.Cost.Data.bitsD d.spineList

theorem MIPRE.Cost.Data.bitsD_encode (s : BitStr) : (encode s).bitsD = s

theorem MIPRE.Cost.Data.bitsListD_encode (cs : List BitStr) : (encode cs).bitsListD = cs

The answer-length calculator and the linear-constraints processor

def MIPRE.Tailored.LenIs (L : Decider) (n : ℕ) (x : Cost.BitStr) (κ : Bool) (k : ℕ) : Prop

The answer-length calculator L outputs k on (n, x, κ): ℓ^κ(x) = k at the question x of the n-th game, readable for κ = false, linear for κ = true — read in unary, as the length of the spine of L's output (II:1781).

Equations

• MIPRE.Tailored.LenIs L n x κ k = ∃ (t : ℕ) (d : MIPRE.Cost.Data), L.prog.Runs (MIPRE.Cost.encode (n, x, κ)) d t ∧ d.spineList.length = k

def MIPRE.Tailored.LenBound (L : Decider) (n B : ℕ) : Prop

The lengths L outputs at index n are at most B.

Equations

• MIPRE.Tailored.LenBound L n B = ∀ (x : MIPRE.Cost.BitStr) (κ : Bool) (k : ℕ), MIPRE.Tailored.LenIs L n x κ k → k ≤ B

def MIPRE.Tailored.LenTotal (L : Decider) (n d : ℕ) : Prop

L halts on every question of dimension d at index n: the paper's requirement that the answer-length calculator never output error on the sampler's questions (II:1863).

Equations

• MIPRE.Tailored.LenTotal L n d = ∀ (x : MIPRE.Cost.BitStr), List.length x = d → ∀ (κ : Bool), ∃ (k : ℕ), MIPRE.Tailored.LenIs L n x κ k

def MIPRE.Tailored.LpIs (P : Decider) (n : ℕ) (x y aR bR : Cost.BitStr) (cs : List Cost.BitStr) : Prop

The linear-constraints processor P outputs the constraint list cs on (n, x, y, a^R, b^R), its output read by Data.bitsListD.

Equations

• MIPRE.Tailored.LpIs P n x y aR bR cs = ∃ (t : ℕ) (d : MIPRE.Cost.Data), P.prog.Runs (MIPRE.Cost.encode (n, x, y, aR, bR)) d t ∧ d.bitsListD = cs

Tailored normal form verifiers

structure MIPRE.Tailored.TailoredVerifier (ℓ : ℕ) : Type

A tailored normal form verifier (II:1758), its canonical decider left implicit.

• sampler : CL.Sampler ℓ

  The sampler, producing the questions.

• len : Decider

  The answer-length calculator.

• lp : Decider

  The linear-constraints processor.

def MIPRE.Tailored.TailoredVerifier.progs {ℓ : ℕ} (V : TailoredVerifier ℓ) : Cost.Prog × Cost.Prog × Cost.Prog

The three programs, what the procedures of the pipeline read.

Equations

• V.progs = (V.sampler.prog, V.len.prog, V.lp.prog)

def MIPRE.Tailored.TailoredVerifier.size {ℓ : ℕ} (V : TailoredVerifier ℓ) : ℕ

The description length |𝒱|, the largest of the three.

Equations

• V.size = max V.sampler.size (max V.len.size V.lp.size)

@[reducible, inline]

abbrev MIPRE.Tailored.TailoredVerifier.Questions {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) : Type

The question alphabet of 𝒱_n: 𝔽₂^{s(n)}.

Equations

• V.Questions n = (Fin (V.sampler.dim n) → MIPRE.CL.𝔽₂)

noncomputable def MIPRE.Tailored.TailoredVerifier.lenOf {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) (x : Cost.BitStr) (κ : Bool) : ℕ

The length len outputs on (n, x, κ), and 0 when it does not halt.

Equations

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

def MIPRE.Tailored.TailoredVerifier.LenDefined {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) (x : Cost.BitStr) : Prop

len halts at the question x of index n, for both kinds of variables.

Equations

• V.LenDefined n x = ∀ (κ : Bool), ∃ (k : ℕ), MIPRE.Tailored.LenIs V.len n x κ k

noncomputable def MIPRE.Tailored.TailoredVerifier.consOf {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) (x y aR bR : Cost.BitStr) : List Cost.BitStr

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

Equations

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

noncomputable def MIPRE.Tailored.TailoredVerifier.tgame {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) : TailoredGame (V.Questions n)

The n-th game 𝒱_n (the paper's def:normal-game for tailored verifiers): questions 𝔽₂^{s(n)} distributed as the sampler prescribes, lengths and constraints as len and lp compute them.

Equations

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

noncomputable def MIPRE.Tailored.TailoredVerifier.valStar {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) : ℝ

val*(𝒱_n).

Equations

• V.valStar n = (V.tgame n).valStar

def MIPRE.Tailored.TailoredVerifier.HasPerfectZPC {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) : Prop

𝒱_n has a perfect Z-aligned permutation strategy commuting along edges, on the doubled question set (Alice asked (false, x), Bob (true, y)), the reading of the paper's completeness clause that Verifier.HasPerfectPCC makes for the existing pipeline.

Equations

• V.HasPerfectZPC n = (V.tgame n).doubled.HasPerfectZPC

def MIPRE.Tailored.TailoredVerifier.IsBounded {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam : ℕ) : Prop

λ-bounded (II:1800): for n ≥ 2, the dimension and the running times of the three programs are at most n^λ — the times at degree λ in the size of the input, as in MIPRE.Verifier.IsBounded — the lengths len outputs are at most n^λ (the paper's unary output makes this a consequence of the time bound), and |𝒱| ≤ λ.

Equations

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

def MIPRE.Tailored.TailoredVerifier.Within {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) (R : Budget) : Prop

𝒱 is within the budget R at index n: the sampler within R.S and of dimension at most R.d, the answer-length calculator and the linear-constraints processor within R.D, all at degree R.k, and the lengths at most R.B — the reading of MIPRE.Verifier.Within for tailored verifiers, the decider's time becoming that of the two programs and its answer bound the bound on the lengths.

Equations

• V.Within n R = (V.sampler.TimeBoundAt n R.S R.k ∧ V.sampler.dim n ≤ R.d ∧ V.len.TimeBoundAt n R.D R.k ∧ V.lp.TimeBoundAt n R.D R.k ∧ MIPRE.Tailored.LenBound V.len n R.B)

The outputs are determined, and the game by them

theorem MIPRE.Tailored.LenIs.unique {L : Decider} {n : ℕ} {x : Cost.BitStr} {κ : Bool} {k k' : ℕ} (h : LenIs L n x κ k) (h' : LenIs L n x κ k') : k = k'

The answer-length calculator outputs one length: the model is deterministic.

theorem MIPRE.Tailored.LpIs.unique {P : Decider} {n : ℕ} {x y aR bR : Cost.BitStr} {cs cs' : List Cost.BitStr} (h : LpIs P n x y aR bR cs) (h' : LpIs P n x y aR bR cs') : cs = cs'

The linear-constraints processor outputs one list of constraints.

theorem MIPRE.Tailored.TailoredVerifier.consOf_eq_of {ℓ : ℕ} (V : TailoredVerifier ℓ) {n : ℕ} {x y aR bR : Cost.BitStr} (hx : V.LenDefined n x) (hy : V.LenDefined n y) {cs : List Cost.BitStr} (h : LpIs V.lp n x y aR bR cs) : V.consOf n x y aR bR = cs

The constraints at (x, y), when len halts at both questions and lp outputs cs.

theorem MIPRE.Tailored.TailoredVerifier.tgame_eq_of_lp {ℓ : ℕ} {S : CL.Sampler ℓ} {L P P' : Decider} {n : ℕ} (hP : ∀ (x y aR bR : Cost.BitStr) (cs : List Cost.BitStr), LpIs P n x y aR bR cs ↔ LpIs P' n x y aR bR cs) : { sampler := S, len := L, lp := P }.tgame n = { sampler := S, len := L, lp := P' }.tgame n

Two verifiers with the same sampler and answer-length calculator, whose processors output the same constraints at index n, have the same n-th game.

theorem MIPRE.Tailored.TailoredVerifier.hasPerfectZPC_congr {ℓ : ℕ} {V W : TailoredVerifier ℓ} {n : ℕ} (hS : V.sampler = W.sampler) (hL : V.len = W.len) (hP : ∀ (x y aR bR : Cost.BitStr) (cs : List Cost.BitStr), LpIs V.lp n x y aR bR cs ↔ LpIs W.lp n x y aR bR cs) : V.HasPerfectZPC n ↔ W.HasPerfectZPC n

Completeness transfers between two verifiers with the same sampler and answer-length calculator whose processors output the same constraints at index n.

theorem MIPRE.Tailored.TailoredVerifier.valStar_congr {ℓ : ℕ} {V W : TailoredVerifier ℓ} {n : ℕ} (hS : V.sampler = W.sampler) (hL : V.len = W.len) (hP : ∀ (x y aR bR : Cost.BitStr) (cs : List Cost.BitStr), LpIs V.lp n x y aR bR cs ↔ LpIs W.lp n x y aR bR cs) : V.valStar n = W.valStar n

The value transfers, under the same hypotheses.

theorem MIPRE.Tailored.TailoredVerifier.valStar_eq_zero_of_rejects {ℓ : ℕ} (V : TailoredVerifier ℓ) {n : ℕ} (h : ∀ (x y : V.Questions n) (aR bR : Cost.BitStr), ∃ (d : ℕ), rejectConstraint d ∈ V.consOf n (CL.toBits x) (CL.toBits y) aR bR) : V.valStar n = 0

A level at which every constraint list holds a rejecting constraint has value 0.