The parameter program of the answer-reduced verifier

Slice P4i of planning/aldous-lyons-track.md: the closed program arParCore κ that, on ((λ, μ, σ), n), writes the parameters of MIPRE.Tailored.AnsRed.Params in unary (arParCore_runs), the routine's parCore. Its running time is ArParCoreCost.

The parameters grow like a power of Q = (λn + 1)^μ, so no polynomial-time function of the binary input writes them in unary; as the MIP* answer reduction's parameter routine (MIPRE.AnswerReduction.ParRoutine.core), the program is a sequence of loops, each writing one number in unary in front of the data, and polynomial-time functions of the unary data between them. In order:

• the MIP* budgets' routine budCore, kept in front of the input: Q in binary (with the MIP* time bound, unused), λ replaced by 0 at the index 0, so that no loop runs longer than Q;
• Q, μ and σ in unary (pushU);
• a polynomial-time function of the unary Q, μ, σ and the binary n (f6): ◇, oW, K, σ' in unary, T = 2^K in binary from K (the bits 0^K 1), and (r, s) from the window describer's parameter function at (n, T, Q, σ');
• r, s in unary;
• 2^j in unary, j = size m and m = nIn + s computed from the unary Q, ◇, r, s;
• a polynomial-time function assembling arParams t j 17 L (K, σ') (f10).

Pushing a number in unary

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.pushU (g : Cost.PolyTimeFun Cost.Data ℕ) : Cost.Prog

A loop stage: write the number g x in unary in front of the data x.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.pushU_closed (g : Cost.PolyTimeFun Cost.Data ℕ) : Cost.Prog.WellScoped 1 (pushU g)

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.pushU_runs (g : Cost.PolyTimeFun Cost.Data ℕ) (x : Cost.Data) : ∃ (t : ℕ), (pushU g).Runs x ((Cost.encode (Cost.unary (g.toFun x))).cons x) t

The unary arithmetic

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.pow2F : Cost.PolyTimeFun Cost.Unary ℕ

2^{|u|} in binary: the bits 0^{|u|} 1.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.pow2F_apply (k : ℕ) : pow2F.toFun (Cost.unary k) = 2 ^ k

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.binF : Cost.PolyTimeFun Cost.Unary ℕ

A unary number in binary.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.binF = MIPRE.Cost.PolyTimeFun.addUnary.comp ((MIPRE.Cost.PolyTimeFun.const 0).pair (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary))

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.binF_apply (k : ℕ) : binF.toFun (Cost.unary k) = k

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.jF : Cost.PolyTimeFun Cost.Unary Cost.Unary

size m in unary, from m in unary.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.jF_apply (k : ℕ) : jF.toFun (Cost.unary k) = Cost.unary k.size

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.I6 : Type

The input of G6: σ, μ, Q in unary and n.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.I6 = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × ℕ)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.dmF : Cost.PolyTimeFun I6 Cost.Unary

◇ = (μ + 2)(Q + 4).

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.oWF : Cost.PolyTimeFun I6 Cost.Unary

oW = 2Q + 3◇ + 6.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.kF (κ : Params.ArConsts) : Cost.PolyTimeFun I6 Cost.Unary

K = E₁ (μ + 1)(oW + Q + 4).

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.sigF (κ : Params.ArConsts) : Cost.PolyTimeFun I6 Cost.Unary

σ' = c₀ + 5σ + 4(Q + ◇) + 8.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.rsF (κ : Params.ArConsts) : Cost.PolyTimeFun I6 (ℕ × ℕ)

The window describer's (r, s) at (n, T, Q, σ'), T = 2^K.

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.Z6 : Type

The output of G6: (r, s) in binary, then K, σ', Q, ◇ in unary.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.Z6 = ((ℕ × ℕ) × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.G6 (κ : Params.ArConsts) : Cost.PolyTimeFun I6 Z6

The middle function: (σ, μ, Q, n) ↦ ((r, s), K, σ', Q, ◇).

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.dmF_apply (lam mu sigma n : ℕ) : dmF.toFun (Cost.unary sigma, Cost.unary mu, Cost.unary (Params.pQ lam mu n), n) = Cost.unary (Params.pDm lam mu n)

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.oWF_apply (lam mu sigma n : ℕ) : oWF.toFun (Cost.unary sigma, Cost.unary mu, Cost.unary (Params.pQ lam mu n), n) = Cost.unary (Params.pOW lam mu n)

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.kF_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : (kF κ).toFun (Cost.unary sigma, Cost.unary mu, Cost.unary (Params.pQ lam mu n), n) = Cost.unary (Params.pK κ lam mu n)

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.sigF_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : (sigF κ).toFun (Cost.unary sigma, Cost.unary mu, Cost.unary (Params.pQ lam mu n), n) = Cost.unary (Params.pSig κ lam mu sigma n)

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.rsF_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : (rsF κ).toFun (Cost.unary sigma, Cost.unary mu, Cost.unary (Params.pQ lam mu n), n) = (Params.pR κ lam mu sigma n, Params.pS κ lam mu sigma n)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.z6 (κ : Params.ArConsts) (lam mu sigma n : ℕ) : Z6

The value of the middle function.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.G6_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : (G6 κ).toFun (Cost.unary sigma, Cost.unary mu, Cost.unary (Params.pQ lam mu n), n) = z6 κ lam mu sigma n

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.mF : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.Unary × Cost.Unary) Cost.Unary

m = nIn + s in unary, from (Q, ◇, r, s) in unary.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.mF_apply (L : PcpDims) : mF.toFun (Cost.unary L.ℓ, Cost.unary L.dm, Cost.unary L.r, Cost.unary L.s) = Cost.unary L.m

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.I10 : Type

The input of the last function: 2^j, s, r, K, σ', Q, ◇ in unary.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.G10 (κ : Params.ArConsts) : Cost.PolyTimeFun I10 ArParams

The last function: the parameters, from (2^j, s, r, K, σ', Q, ◇) in unary.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.mF_pL (κ : Params.ArConsts) (lam mu sigma n : ℕ) : mF.toFun (Cost.unary (Params.pQ lam mu n), Cost.unary (Params.pDm lam mu n), Cost.unary (Params.pR κ lam mu sigma n), Cost.unary (Params.pS κ lam mu sigma n)) = Cost.unary (Params.pL κ lam mu sigma n).m

mF at the PCP's dimensions, with ℓ = Q.

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.G10_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : (G10 κ).toFun (Cost.unary (2 ^ Params.pJ κ lam mu sigma n), Cost.unary (Params.pS κ lam mu sigma n), Cost.unary (Params.pR κ lam mu sigma n), Cost.unary (Params.pK κ lam mu n), Cost.unary (Params.pSig κ lam mu sigma n), Cost.unary (Params.pQ lam mu n), Cost.unary (Params.pDm lam mu n)) = arParams (Params.pTw κ lam mu sigma n) (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (Params.pExtra κ lam mu sigma n)

The data between the stages

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.gQ : Cost.PolyTimeFun Cost.Data ℕ

Q in binary, after the budgets' routine.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.gQ = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeHead)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.gMu : Cost.PolyTimeFun Cost.Data ℕ

μ, after Q in unary.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.gSig : Cost.PolyTimeFun Cost.Data ℕ

σ, after μ in unary.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.f6 (κ : Params.ArConsts) : Cost.PolyTimeFun Cost.Data Cost.Data

The middle stage: (σ, μ, Q, n) read, then G6.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.gR : Cost.PolyTimeFun Cost.Data ℕ

r, after the middle stage.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.gR = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeHead)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.gS : Cost.PolyTimeFun Cost.Data ℕ

s, after r in unary.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.gS = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail))

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.g2J : Cost.PolyTimeFun Cost.Data ℕ

2^j, after s in unary.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.f10 (κ : Params.ArConsts) : Cost.PolyTimeFun Cost.Data Cost.Data

The last stage: (2^j, s, r, K, σ', Q, ◇) read, then G10.

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.x0 (lam mu sigma n : ℕ) : Cost.Data

The input.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.x0 lam mu sigma n = MIPRE.Cost.encode ((lam, mu, sigma), n)

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.x1 (lam mu sigma n : ℕ) : Cost.Data

After the budgets' routine.

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.x2 (lam mu sigma n : ℕ) : Cost.Data

After Q in unary.

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.x3 (lam mu sigma n : ℕ) : Cost.Data

After μ in unary.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.x3 lam mu sigma n = (MIPRE.Cost.encode (MIPRE.Cost.unary mu)).cons (MIPRE.Tailored.AnsRed.Typed.ArPar.x2 lam mu sigma n)

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.x4 (lam mu sigma n : ℕ) : Cost.Data

After σ in unary.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.x4 lam mu sigma n = (MIPRE.Cost.encode (MIPRE.Cost.unary sigma)).cons (MIPRE.Tailored.AnsRed.Typed.ArPar.x3 lam mu sigma n)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.y6 (κ : Params.ArConsts) (lam mu sigma n : ℕ) : Cost.Data

After the middle stage.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArPar.y6 κ lam mu sigma n = MIPRE.Cost.encode (MIPRE.Tailored.AnsRed.Typed.ArPar.z6 κ lam mu sigma n)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.y7 (κ : Params.ArConsts) (lam mu sigma n : ℕ) : Cost.Data

After r in unary.

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.y8 (κ : Params.ArConsts) (lam mu sigma n : ℕ) : Cost.Data

After s in unary.

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ArPar.y9 (κ : Params.ArConsts) (lam mu sigma n : ℕ) : Cost.Data

After 2^j in unary.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.gQ_apply (lam mu sigma n : ℕ) : gQ.toFun (x1 lam mu sigma n) = Params.pQ lam mu n

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.gMu_apply (lam mu sigma n : ℕ) : gMu.toFun (x2 lam mu sigma n) = mu

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.gSig_apply (lam mu sigma n : ℕ) : gSig.toFun (x3 lam mu sigma n) = sigma

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.f6_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : (f6 κ).toFun (x4 lam mu sigma n) = y6 κ lam mu sigma n

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.gR_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : gR.toFun (y6 κ lam mu sigma n) = Params.pR κ lam mu sigma n

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.gS_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : gS.toFun (y7 κ lam mu sigma n) = Params.pS κ lam mu sigma n

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.g2J_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : g2J.toFun (y8 κ lam mu sigma n) = 2 ^ Params.pJ κ lam mu sigma n

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.f10_apply (κ : Params.ArConsts) (lam mu sigma n : ℕ) : (f10 κ).toFun (y9 κ lam mu sigma n) = Cost.encode (arParams (Params.pTw κ lam mu sigma n) (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (Params.pExtra κ lam mu sigma n))

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.budStage : Cost.Prog

The budgets' stage: the MIP* budgets' routine, its output kept in front of the input.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.budStage_closed : Cost.Prog.WellScoped 1 budStage

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArPar.tailProg (κ : Params.ArConsts) : Cost.Prog

The stages after the budgets'.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.tailProg_closed (κ : Params.ArConsts) : Cost.Prog.WellScoped 1 (tailProg κ)

noncomputable def MIPRE.Tailored.AnsRed.Typed.arParCore (κ : Params.ArConsts) : Cost.Prog

The parameter program of the answer-reduced verifier, on ((λ, μ, σ), n).

Equations

• MIPRE.Tailored.AnsRed.Typed.arParCore κ = MIPRE.Cost.seqProg MIPRE.Tailored.AnsRed.Typed.ArPar.budStage (MIPRE.Tailored.AnsRed.Typed.ArPar.tailProg κ)

theorem MIPRE.Tailored.AnsRed.Typed.arParCore_closed (κ : Params.ArConsts) : Cost.Prog.WellScoped 1 (arParCore κ)

theorem MIPRE.Tailored.AnsRed.Typed.arParCore_runs (κ : Params.ArConsts) (lam mu sigma n : ℕ) : ∃ (τ : ℕ), (arParCore κ).Runs (Cost.encode ((lam, mu, sigma), n)) (Cost.encode (arParams (Params.pTw κ lam mu sigma n) (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (Params.pExtra κ lam mu sigma n))) τ

The parameter program computes the parameters.