The answer-length calculator of the answer-reduced verifier

Slice P4h of planning/aldous-lyons-track.md: the answer-length calculator of the output tailored verifier of the answer reduction. At a detyped question, the presented game's lengths are those of the type its graph view decodes to (TypedData.detype), and the typed lengths are products: an answer of type (r, S) has a codeword count of the role — the oracle's readable or linear count, or one for an isolated role — times the coefficients of a codeword at S — one, d + 1 or M d + 1 — times the field width t (Typed.lenR, Typed.lenL).

On (n, x, κ), with (λ, μ, σ) hardcoded, the calculator first runs the parameter program of the routine (ArRoutine.parCore) on ((λ, μ, σ), n), as a stage: the parameters are written in unary and grow like a power of (λn + 1)^μ, which no polynomial-time function of the binary index can write. Then the polynomial-time function lenF reads the graph view of x, decodes it with κ into the indices of the two factors by a finite table (finiteFunction, idxAt), and multiplies the selected factors with t in unary; an undecodable view gives 0.

• lenD_lenIs: what the calculator outputs on every input;
• lenD_lenIs_question: at a detyped question, the length of the type it decodes to;
• lenD_presented: the length half of TailoredVerifier.MeetsAt.

The factors of a length

def MIPRE.Tailored.AnsRed.Typed.cntIdx : Role → Bool → ℕ

The index of a role's codeword count at a kind: the oracle's readable (0) or linear (1) count, or the one codeword of an isolated role (2).

Equations

• MIPRE.Tailored.AnsRed.Typed.cntIdx MIPRE.Role.oracle false = 0
• MIPRE.Tailored.AnsRed.Typed.cntIdx MIPRE.Role.oracle true = 1
• MIPRE.Tailored.AnsRed.Typed.cntIdx x✝¹ x✝ = 2

def MIPRE.Tailored.AnsRed.Typed.ncIdx : LIDT.CL.Ty → ℕ

The index of a type's number of coefficients: one, d + 1, M d + 1.

Equations

• MIPRE.Tailored.AnsRed.Typed.ncIdx MIPRE.LIDT.CL.Ty.point = 0
• MIPRE.Tailored.AnsRed.Typed.ncIdx MIPRE.LIDT.CL.Ty.aline = 1
• MIPRE.Tailored.AnsRed.Typed.ncIdx MIPRE.LIDT.CL.Ty.dline = 2

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.LenPar : Type

The parameters of the lengths, in unary: the field width t, the oracle's readable and linear codeword counts, d + 1 and M d + 1.

Equations

• MIPRE.Tailored.AnsRed.Typed.LenPar = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

def MIPRE.Tailored.AnsRed.Typed.lenPar (t j d : ℕ) (L : PcpDims) : LenPar

The parameters of the typed data, in unary.

Equations

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

def MIPRE.Tailored.AnsRed.Typed.lenOfIdx (p : LenPar) (ik : ℕ × ℕ) : ℕ

The length at a pair of indices: the selected count, times the selected number of coefficients, times t; 0 out of range.

Equations

• MIPRE.Tailored.AnsRed.Typed.lenOfIdx p ik = [List.length p.2.1, List.length p.2.2.1, 1].getD ik.1 0 * [1, List.length p.2.2.2.1, List.length p.2.2.2.2].getD ik.2 0 * List.length p.1

theorem MIPRE.Tailored.AnsRed.Typed.lenOfIdx_lenPar (t j d : ℕ) (L : PcpDims) (u : Role × LIDT.CL.Ty) (κ : Bool) : lenOfIdx (lenPar t j d L) (cntIdx u.1 κ, ncIdx u.2) = if κ = true then lenL t j d L u else lenR t j d L u

The typed lengths are the selected products.

The decoding of a question

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.gdA : ℕ

The number of bits of a graph view of the answer-reduced types.

Equations

• MIPRE.Tailored.AnsRed.Typed.gdA = MIPRE.CL.Detyping.graphDim (MIPRE.Role × MIPRE.LIDT.CL.Ty)

noncomputable def MIPRE.Tailored.AnsRed.Typed.idxAt (g : CL.Graph.Coord (Role × LIDT.CL.Ty) → CL.𝔽₂) (κ : Bool) : ℕ × ℕ

The indices at a graph view and a kind: those of the type it decodes to, (3, 3) when it does not decode.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.tabA (p : (Fin gdA → CL.𝔽₂) × Bool) : ℕ × ℕ

The finite table: from the bits of a graph view and a kind, the indices.

Equations

• MIPRE.Tailored.AnsRed.Typed.tabA p = MIPRE.Tailored.AnsRed.Typed.idxAt (MIPRE.CL.pull MIPRE.CL.Detyping.graphEquiv.toEmbedding p.1) p.2

noncomputable def MIPRE.Tailored.AnsRed.Typed.lenParF : Cost.PolyTimeFun ArParams LenPar

The parameters of the lengths, from the routine's parameters: t, the oracle's readable count 6 + m + 2ℓ + ◇' + 3r and linear count 5 + ◇' + 2ℓ + 3◇ (with ◇' = 2ℓ + 3◇ + 6 the width of an index of O and m the number of wires), d + 1 and M d + 1.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.lenParF_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : lenParF.toFun (arParams t j d L e) = lenPar t j d L

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.LenIn : Type

The input of the calculator's function: the parameters, the question and the kind.

Equations

• MIPRE.Tailored.AnsRed.Typed.LenIn = (MIPRE.Tailored.AnsRed.Typed.ArParams × MIPRE.Cost.BitStr × Bool)

noncomputable def MIPRE.Tailored.AnsRed.Typed.lenF : Cost.PolyTimeFun LenIn Cost.Unary

The calculator's function, on the parameters, the question and the kind.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.getD_unary_length (l : List ℕ) (i : ℕ) : List.length ((List.map Cost.unary l).getD i []) = l.getD i 0

theorem MIPRE.Tailored.AnsRed.Typed.length_lenF (p : ArParams) (x : Cost.BitStr) (κ : Bool) : List.length (lenF.toFun (p, x, κ)) = lenOfIdx (lenParF.toFun p) (idxAt (CL.Detyping.graphOfBits x) κ)

The calculator

noncomputable def MIPRE.Tailored.AnsRed.Typed.parArg : Cost.PolyTimeFun Cost.Data Cost.Data

The parameter stage's argument, on ((λ, μ, σ), (n, x, κ)): ((λ, μ, σ), n).

Equations

• MIPRE.Tailored.AnsRed.Typed.parArg = MIPRE.Cost.PolyTimeFun.treePair.ap₂ MIPRE.Cost.PolyTimeFun.treeHead (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.Tailored.AnsRed.Typed.lenRead : Cost.PolyTimeFun Cost.Data LenIn

The calculator's input, read after the parameter stage.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenCore (R : ArRoutine) : Cost.Prog

The calculator's core, on ((λ, μ, σ), (n, x, κ)): the parameter stage, then lenF.

Equations

• R.lenCore = MIPRE.Cost.seqProg (MIPRE.AnswerReduction.stg MIPRE.Tailored.AnsRed.Typed.parArg R.parCore) (MIPRE.Tailored.AnsRed.Typed.lenF.comp MIPRE.Tailored.AnsRed.Typed.lenRead).code

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenCore_closed (R : ArRoutine) : Cost.Prog.WellScoped 1 R.lenCore

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenD (R : ArRoutine) (lam mu sigma : ℕ) : Decider

The answer-length calculator at (λ, μ, σ): the core with (λ, μ, σ) hardcoded.

Equations

• R.lenD lam mu sigma = { prog := MIPRE.Cost.hardcode R.lenCore (MIPRE.Cost.encode (lam, mu, sigma)), closed := ⋯ }

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenPF (R : ArRoutine) : Cost.PolyTimeFun (ℕ × ℕ × ℕ) Cost.Prog

Its program, from (λ, μ, σ), in polynomial time.

Equations

• R.lenPF = (MIPRE.Cost.PolyTimeFun.smn (ℕ × ℕ × ℕ)).comp ((MIPRE.Cost.PolyTimeFun.const R.lenCore).pair (MIPRE.Cost.PolyTimeFun.id (ℕ × ℕ × ℕ)))

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenPF_eq (R : ArRoutine) (lam mu sigma : ℕ) : R.lenPF.toFun (lam, mu, sigma) = (R.lenD lam mu sigma).prog

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenD_lenIs (R : ArRoutine) (lam mu sigma n : ℕ) (x : Cost.BitStr) (κ : Bool) : LenIs (R.lenD lam mu sigma) n x κ (lenOfIdx (lenPar ((R.fam lam mu sigma).t n) ((R.fam lam mu sigma).j n) (R.d lam mu sigma n) (R.L lam mu sigma n)) (idxAt (CL.Detyping.graphOfBits x) κ))

What the calculator outputs, on every input: the length of the type the question's graph view decodes to, at the parameters of the index.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenD_lenIs_question (R : ArRoutine) (lam mu sigma n : ℕ) {s : ℕ} (q : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin s) → CL.𝔽₂) (κ : Bool) : LenIs (R.lenD lam mu sigma) n (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv s) q)) κ ((Option.map (fun (u : Role × LIDT.CL.Ty) => lenOfIdx (lenPar ((R.fam lam mu sigma).t n) ((R.fam lam mu sigma).j n) (R.d lam mu sigma n) (R.L lam mu sigma n)) (cntIdx u.1 κ, ncIdx u.2)) (typeOf arGraph q)).getD 0)

The calculator at a detyped question: the length of the type the question decodes to, 0 when it does not decode.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenD_presented (R : ArRoutine) (lam mu sigma : ℕ) {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {Cc : V.Questions n → SAT.Circuit} {hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = (R.L lam mu sigma n).m} {ℓ : ℕ} {P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) ℓ} {B : ℕ} (q : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) : LenIs (R.lenD lam mu sigma) n (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) q)) false ((arPresented (R.d lam mu sigma n) ⋯ ((R.fam lam mu sigma).sel n) (R.L lam mu sigma n) ⋯ V n Cc hm P B).lenR q) ∧ LenIs (R.lenD lam mu sigma) n (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) q)) true ((arPresented (R.d lam mu sigma n) ⋯ ((R.fam lam mu sigma).sel n) (R.L lam mu sigma n) ⋯ V n Cc hm P B).lenL q)

The length half of TailoredVerifier.MeetsAt: the calculator outputs the presented game's lengths at the detyped questions, at the routine's parameters.