The parameter routine of the answer-reduced verifier

Slice P4h of planning/aldous-lyons-track.md. At an index n the output verifier of the answer reduction runs at parameters — the field width t, the selector width j with M = 2^j, the degree d and the dimensions ℓ, ◇, r, s of the PCP — that grow like a power of (λn + 1)^μ. Its programs read them in unary, which no polynomial-time function of the index can write: the index is read in binary. So, as the MIP* answer reduction's parameter routine (MIPRE.AnswerReduction.parProg), the parameters are computed by a program run as a stage of the output's programs, on ((λ, μ, σ), n), and the cost of that stage is bounded separately.

• ArParams, arParams: the parameters at an index, in unary, with data for the circuit function; readParams reads them back.
• ArRoutine: the parameter functions, the closed program parCore computing them, and the circuit function circF giving the circuit of a seed from the input verifier's programs, the parameters and the seed's two questions, well formed with the PCP's nIn inputs and s gates. The routine is fixed in P4i.
• ArRoutine.toLd: the routine of the low-degree half of the sampler (LdRoutine), the parameter program projected to the half's parameters.
• ArRoutine.circ: the circuit of each seed of the input verifier.

The parameters at an index

@[reducible, inline]

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

The parameters of the answer-reduced verifier at an index, in unary: the field width t, the selector width j, M = 2^j, the degree d, the dimensions ℓ, ◇, r, s of the PCP, then data for the circuit function.

Equations

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

def MIPRE.Tailored.AnsRed.Typed.arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : ArParams

The parameters of the typed data, as ArParams.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.unary_ext {u v : Cost.Unary} (h : List.length u = List.length v) : u = v

noncomputable def MIPRE.Tailored.AnsRed.Typed.pT : Cost.PolyTimeFun ArParams Cost.Unary

The field width.

Equations

• MIPRE.Tailored.AnsRed.Typed.pT = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Tailored.AnsRed.Typed.pJ : Cost.PolyTimeFun ArParams Cost.Unary

The selector width.

Equations

• MIPRE.Tailored.AnsRed.Typed.pJ = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.AnsRed.Typed.pM : Cost.PolyTimeFun ArParams Cost.Unary

M = 2^j.

Equations

• MIPRE.Tailored.AnsRed.Typed.pM = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Tailored.AnsRed.Typed.pD : Cost.PolyTimeFun ArParams Cost.Unary

The degree.

Equations

• MIPRE.Tailored.AnsRed.Typed.pD = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.AnsRed.Typed.pL : Cost.PolyTimeFun ArParams Cost.Unary

The window width ℓ of the PCP.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.pDm : Cost.PolyTimeFun ArParams Cost.Unary

The index width ◇ of the PCP.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.pR : Cost.PolyTimeFun ArParams Cost.Unary

The witness index width r of the PCP.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.pS : Cost.PolyTimeFun ArParams Cost.Unary

The number s of gates of the circuits.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.pE : Cost.PolyTimeFun ArParams Cost.Data

The data of the circuit function.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.pT_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : pT.toFun (arParams t j d L e) = Cost.unary t

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.pJ_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : pJ.toFun (arParams t j d L e) = Cost.unary j

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.pM_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : pM.toFun (arParams t j d L e) = Cost.unary (2 ^ j)

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.pD_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : pD.toFun (arParams t j d L e) = Cost.unary d

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.pL_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : pL.toFun (arParams t j d L e) = Cost.unary L.ℓ

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.pDm_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : pDm.toFun (arParams t j d L e) = Cost.unary L.dm

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.pR_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : pR.toFun (arParams t j d L e) = Cost.unary L.r

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.pS_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : pS.toFun (arParams t j d L e) = Cost.unary L.s

@[simp]

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

def MIPRE.Tailored.AnsRed.Typed.fieldAt : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data

The i-th field of a nested pair.

Equations

• MIPRE.Tailored.AnsRed.Typed.fieldAt 0 = MIPRE.Cost.PolyTimeFun.treeHead
• MIPRE.Tailored.AnsRed.Typed.fieldAt i.succ = (MIPRE.Tailored.AnsRed.Typed.fieldAt i).comp MIPRE.Cost.PolyTimeFun.treeTail

def MIPRE.Tailored.AnsRed.Typed.tailAt : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data

The tail of a nested pair after i fields.

Equations

• MIPRE.Tailored.AnsRed.Typed.tailAt 0 = MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data
• MIPRE.Tailored.AnsRed.Typed.tailAt i.succ = (MIPRE.Tailored.AnsRed.Typed.tailAt i).comp MIPRE.Cost.PolyTimeFun.treeTail

noncomputable def MIPRE.Tailored.AnsRed.Typed.readParams : Cost.PolyTimeFun Cost.Data ArParams

The parameters, read back.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.readParams_encode (p : ArParams) : readParams.toFun (Cost.encode p) = p

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldPdF : Cost.PolyTimeFun ArParams Cost.Data

The parameters of the low-degree half, LdFamily.pd: t, M and the copy's description.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ldPdF_arParams (F : LdFamily) (n d : ℕ) (L : PcpDims) (e : Cost.Data) : ldPdF.toFun (arParams (F.t n) (F.j n) d L e) = F.pd n

The routine

@[reducible, inline]

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

The input of the circuit function: the input verifier's programs, (λ, μ, σ), the index, the parameters, and the two questions of a seed.

Equations

• MIPRE.Tailored.AnsRed.Typed.CircIn = ((MIPRE.Cost.Prog × MIPRE.Cost.Prog × MIPRE.Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ × MIPRE.Tailored.AnsRed.Typed.ArParams × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

structure MIPRE.Tailored.AnsRed.Typed.ArRoutine : Type

A parameter routine of the answer-reduced verifier: the parameters at each (λ, μ, σ) and index, a closed program computing them from ((λ, μ, σ), n), and a polynomial-time circuit function, whose circuits are well formed with the PCP's nIn inputs and s gates.

• fam : ℕ → ℕ → ℕ → LdFamily

  The field and selector widths.

• d : ℕ → ℕ → ℕ → ℕ → ℕ

  The degree.

• L : ℕ → ℕ → ℕ → ℕ → PcpDims

  The dimensions of the PCP.

• hLM (lam mu sigma n : ℕ) : (self.L lam mu sigma n).m ≤ 2 ^ (self.fam lam mu sigma).j n
• extra : ℕ → ℕ → ℕ → ℕ → Cost.Data

  The data of the circuit function.

• parCore : Cost.Prog

  The parameter program.

• closed : Cost.Prog.WellScoped 1 self.parCore
• runs (lam mu sigma n : ℕ) : ∃ (τ : ℕ), self.parCore.Runs (Cost.encode ((lam, mu, sigma), n)) (Cost.encode (arParams ((self.fam lam mu sigma).t n) ((self.fam lam mu sigma).j n) (self.d lam mu sigma n) (self.L lam mu sigma n) (self.extra lam mu sigma n))) τ
• circF : Cost.PolyTimeFun CircIn SAT.Circuit

  The circuit function.

• circ_wf (inp : CircIn) : (self.circF.toFun inp).WellFormed
• circ_inputs (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam mu sigma n : ℕ) (x y : Cost.BitStr) : (self.circF.toFun (V, (lam, mu, sigma), n, arParams ((self.fam lam mu sigma).t n) ((self.fam lam mu sigma).j n) (self.d lam mu sigma n) (self.L lam mu sigma n) (self.extra lam mu sigma n), x, y)).inputs = (self.L lam mu sigma n).nIn
• circ_size (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam mu sigma n : ℕ) (x y : Cost.BitStr) : (self.circF.toFun (V, (lam, mu, sigma), n, arParams ((self.fam lam mu sigma).t n) ((self.fam lam mu sigma).j n) (self.d lam mu sigma n) (self.L lam mu sigma n) (self.extra lam mu sigma n), x, y)).size = (self.L lam mu sigma n).s

def MIPRE.Tailored.AnsRed.Typed.ArRoutine.params (R : ArRoutine) (lam mu sigma n : ℕ) : ArParams

The parameters at (λ, μ, σ) and n.

Equations

• R.params lam mu sigma n = MIPRE.Tailored.AnsRed.Typed.arParams ((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) (R.extra lam mu sigma n)

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.parCore_runs (R : ArRoutine) (lam mu sigma n : ℕ) : ∃ (τ : ℕ), R.parCore.Runs (Cost.encode ((lam, mu, sigma), n)) (Cost.encode (R.params lam mu sigma n)) τ

The low-degree half's routine

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

The parameter program, projected to the parameters of the low-degree half.

Equations

• R.ldCore = MIPRE.Cost.seqProg R.parCore (MIPRE.Tailored.AnsRed.Typed.ldPdF.comp MIPRE.Tailored.AnsRed.Typed.readParams).code

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.ldCore_closed (R : ArRoutine) : Cost.Prog.WellScoped 1 R.ldCore

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.ldCore_runs (R : ArRoutine) (lam mu sigma n : ℕ) : ∃ (τ : ℕ), R.ldCore.Runs (Cost.encode ((lam, mu, sigma), n)) ((R.fam lam mu sigma).pd n) τ

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.toLd (R : ArRoutine) : LdRoutine

The routine of the low-degree half: the projected parameter program, with (λ, μ, σ) hardcoded.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.toLd_fam (R : ArRoutine) : R.toLd.fam = R.fam

The circuits

def MIPRE.Tailored.AnsRed.Typed.ArRoutine.circ (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier ℓ) (z : V.Questions n) : SAT.Circuit

The circuit of a seed of the input verifier: the circuit function at the seed's two questions.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.circ_inputs' (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier ℓ) (z : V.Questions n) : (R.circ lam mu sigma n V z).inputs = (R.L lam mu sigma n).nIn

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.circ_size' (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier ℓ) (z : V.Questions n) : (R.circ lam mu sigma n V z).size = (R.L lam mu sigma n).s

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.circ_wires (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier ℓ) (z : V.Questions n) : (R.circ lam mu sigma n V z).inputs + (R.circ lam mu sigma n V z).size = (R.L lam mu sigma n).m