The repeated decider

The decider of ComputeParrepVerifier (thm:parallel-repetition) as a Decider: the core Prog.repDecCore of MIPRE.Foundations.Repeat.DecMain, run through the self-interpreter and the s-m-n construction on ((S̄, D̄), λ, τ, β). Its acceptance is characterized exactly (repDecider_accepts_iff): on (n, x, y, a, b) it accepts iff |x| = |y| = k s, a and b are the serializations of lists of k bit strings of length at most B each, and the input decider accepts every coordinate (n, x_i, y_i, a_i, b_i), with k = 2^{τ(|λ| + |n|)}, s = s(n) the dimension of the input sampler and B = 2^{β(|λ| + |n|)} the parse length. Both directions go through the inversion lemmas of the programs, since the input decider need not halt on inputs it rejects.

noncomputable def MIPRE.Repeat.repDeciderProg (sp dp : Cost.Prog) (lam tau beta : ℕ) : Cost.Prog

The program of the repeated decider on ((S̄, D̄), λ, τ, β): the core, hardcoded.

Equations

• MIPRE.Repeat.repDeciderProg sp dp lam tau beta = MIPRE.Cost.hardcode MIPRE.Cost.selfUniversal.univ.repDecCore (MIPRE.Cost.encode ((sp, dp), lam, tau, beta))

theorem MIPRE.Repeat.repDeciderProg_wellScoped (sp dp : Cost.Prog) (lam tau beta : ℕ) : Cost.Prog.WellScoped 1 (repDeciderProg sp dp lam tau beta)

noncomputable def MIPRE.Repeat.repDecider (sp dp : Cost.Prog) (lam tau beta : ℕ) : Decider

The repeated decider (ComputeParrepVerifier, decider half).

Equations

• MIPRE.Repeat.repDecider sp dp lam tau beta = { prog := MIPRE.Repeat.repDeciderProg sp dp lam tau beta, closed := ⋯ }

theorem MIPRE.Repeat.encode_decParams (sp dp : Cost.Prog) (lam tau beta : ℕ) : Cost.encode ((sp, dp), lam, tau, beta) = Cost.Prog.decParams (Cost.encode sp) (Cost.encode dp) (Cost.encode lam) (Cost.encode tau) (Cost.encode beta)

theorem MIPRE.Repeat.repDeciderProg_runs (sp dp : Cost.Prog) (lam tau beta n : ℕ) (x y a b : Cost.BitStr) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [Cost.Prog.decInput (Cost.encode sp) (Cost.encode dp) (Cost.encode lam) (Cost.encode tau) (Cost.encode beta) (Cost.encode n) (Cost.encode x) (Cost.encode y) (Cost.encode a) (Cost.encode b)] Cost.selfUniversal.univ.decMain r t) : ∃ (t' : ℕ), (repDeciderProg sp dp lam tau beta).Runs (Cost.encode (n, x, y, a, b)) r t'

The run of the repeated decider on a well-formed input, from a run of decMain.

theorem MIPRE.Repeat.repDeciderProg_inv (sp dp : Cost.Prog) (lam tau beta n : ℕ) (x y a b : Cost.BitStr) {r : Cost.Data} {t : ℕ} (h : (repDeciderProg sp dp lam tau beta).Runs (Cost.encode (n, x, y, a, b)) r t) : ∃ (t' : ℕ), Cost.Eval [Cost.Prog.decInput (Cost.encode sp) (Cost.encode dp) (Cost.encode lam) (Cost.encode tau) (Cost.encode beta) (Cost.encode n) (Cost.encode x) (Cost.encode y) (Cost.encode a) (Cost.encode b)] Cost.selfUniversal.univ.decMain r t'

Conversely, a run of the repeated decider on a well-formed input is a run of decMain.

theorem MIPRE.Repeat.univ_accepts_iff (D : Decider) (n : ℕ) (xi yi ai bi : Cost.BitStr) : (∃ (t : ℕ), Cost.Eval [Cost.Prog.decQuery (Cost.encode D.prog) (Cost.encode n) (Cost.encode xi) (Cost.encode yi) (Cost.encode ai) (Cost.encode bi)] Cost.selfUniversal.univ (Cost.Data.nil.cons Cost.Data.nil) t) ↔ D.Accepts n xi yi ai bi

The universal machine accepts a coordinate query iff the input decider does.

theorem MIPRE.Repeat.DecAcc_iff (univ : Cost.Prog) (dD nD : Cost.Data) (s B k : ℕ) (remX remY remA remB : List Cost.Data) : univ.DecAcc dD nD s B k remX remY remA remB ↔ ∃ (aa : Fin k → Cost.BitStr) (bb : Fin k → Cost.BitStr), (remA = List.ofFn fun (i : Fin k) => Cost.encode (aa i)) ∧ (remB = List.ofFn fun (i : Fin k) => Cost.encode (bb i)) ∧ ∀ (i : Fin k), List.length (aa i) ≤ B ∧ List.length (bb i) ≤ B ∧ ∃ (t : ℕ), Cost.Eval [Cost.Prog.decQuery dD nD (Cost.Data.list (Cost.Data.chunk s (↑i) remX)) (Cost.Data.list (Cost.Data.chunk s (↑i) remY)) (Cost.encode (aa i)) (Cost.encode (bb i))] univ (Cost.Data.nil.cons Cost.Data.nil) t

The acceptance predicate of the coordinate loop, read as k-tuples of bit strings.

def MIPRE.Repeat.RepAcc {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (x y a b : Cost.BitStr) : Prop

Acceptance of the repeated decider, on the parameters (λ, τ, β) at index n, read as k-tuples: |x| = |y| = k s, a and b the serializations of lists of k bit strings of length at most B, and the input decider accepting every coordinate.

Equations

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

theorem MIPRE.Repeat.bitsOf_toList_encode (x : Cost.BitStr) : Cost.Data.bitsOf (Cost.encode x).toList = x

theorem MIPRE.Repeat.repDecider_accepts_iff {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (x y a b : Cost.BitStr) : (repDecider S.prog D.prog lam tau beta).Accepts n x y a b ↔ RepAcc S D lam tau beta n x y a b

The repeated decider accepts exactly on RepAcc.

theorem MIPRE.Repeat.repDecider_accepts_length {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (x y a b : Cost.BitStr) (h : (repDecider S.prog D.prog lam tau beta).Accepts n x y a b) : List.length x = Repetition.reps lam tau n * S.dim n ∧ List.length y = Repetition.reps lam tau n * S.dim n

The repeated decider accepts only questions of the repeated dimension.

theorem MIPRE.Repeat.length_toBitsPost_list_le (k B : ℕ) (aa : Fin k → Cost.BitStr) (h : ∀ (i : Fin k), List.length (aa i) ≤ B) : List.length (Cost.Data.list (List.ofFn fun (i : Fin k) => Cost.encode (aa i))).toBitsPost ≤ k * (4 * B + 2) + 1

The length of the serialization of a list of k bit strings of length at most B.

theorem MIPRE.Repeat.repDecider_rejectsLong {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (x y a b : Cost.BitStr) (T : ℕ) (hT : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ T) (h : (repDecider S.prog D.prog lam tau beta).Accepts n x y a b) : List.length a ≤ T ∧ List.length b ≤ T

The repeated decider rejects long answers: every accepted answer has length at most k (4B + 2) + 1.