The constraints at two detyped questions, as a program

Slice P4h of planning/aldous-lyons-track.md: the last stage of the answer-reduced verifier's linear-constraints processor. From the parameters, the two questions' bits, the readable answers and the constraints of the two questions' proof checks, it decodes the edge the two graph views sit on by a finite table (edgeF), checks the readable lengths (lenOkF), and on the edge's pair of types runs the four checks' programs (finBranchF), as the typed data does (Typed.cons): lpFinal_eq. The proof checks need the circuits of the two seeds, which the routine's circuit function computes from the input verifier's programs; the processor runs it, and the proof check, as earlier stages on encodings (ArRoutine.prfInF, proof_lX, proof_lY), so that no program has to be decoded from data.

The input

@[reducible, inline]

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

The input of the processor's last stage: the parameters; the two questions' bits and the two readable answers; Alice's and Bob's questions of the input sampler at the first question's seed, then at the second's; the input verifier's programs, (λ, μ, σ) and the index.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lP : Cost.PolyTimeFun LpIn ArParams

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lX : Cost.PolyTimeFun LpIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lY : Cost.PolyTimeFun LpIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lA : Cost.PolyTimeFun LpIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lB : Cost.PolyTimeFun LpIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lAx : Cost.PolyTimeFun LpIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lBx : Cost.PolyTimeFun LpIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lAy : Cost.PolyTimeFun LpIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lBy : Cost.PolyTimeFun LpIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lV : Cost.PolyTimeFun LpIn (Cost.Prog × Cost.Prog × Cost.Prog)

Equations

• MIPRE.Tailored.AnsRed.Typed.lV = 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.lLms : Cost.PolyTimeFun LpIn (ℕ × ℕ × ℕ)

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lN : Cost.PolyTimeFun LpIn ℕ

Equations

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

The pieces of a question

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

D t = (2M + 1) t, the number of a question's low-degree bits.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.vecF (q : Cost.PolyTimeFun LpIn Cost.BitStr) : Cost.PolyTimeFun LpIn Cost.BitStr

The vector part of a question's bits: after the graph view.

Equations

• MIPRE.Tailored.AnsRed.Typed.vecF q = MIPRE.Cost.PolyTimeFun.drop.ap₂ q (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary MIPRE.Tailored.AnsRed.Typed.gdA))

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldbF (q : Cost.PolyTimeFun LpIn Cost.BitStr) : Cost.PolyTimeFun LpIn Cost.BitStr

The low-degree bits of a question: the last D t bits of its vector part.

Equations

• MIPRE.Tailored.AnsRed.Typed.ldbF q = MIPRE.AnswerReduction.rightBP.comp ((MIPRE.Tailored.AnsRed.Typed.vecF q).pair (MIPRE.Tailored.AnsRed.Typed.dtF.comp MIPRE.Tailored.AnsRed.Typed.lP))

noncomputable def MIPRE.Tailored.AnsRed.Typed.lenRq (q : Cost.PolyTimeFun LpIn Cost.BitStr) : Cost.PolyTimeFun LpIn Cost.Unary

A question's readable length, by the calculator's function.

Equations

• MIPRE.Tailored.AnsRed.Typed.lenRq q = MIPRE.Tailored.AnsRed.Typed.lenF.comp (MIPRE.Tailored.AnsRed.Typed.lP.pair (q.pair (MIPRE.Cost.PolyTimeFun.const false)))

noncomputable def MIPRE.Tailored.AnsRed.Typed.lenq (q : Cost.PolyTimeFun LpIn Cost.BitStr) : Cost.PolyTimeFun LpIn Cost.Unary

A question's length.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.nAF : Cost.PolyTimeFun LpIn Cost.Unary

The first question's length, Na.

Equations

• MIPRE.Tailored.AnsRed.Typed.nAF = MIPRE.Tailored.AnsRed.Typed.lenq MIPRE.Tailored.AnsRed.Typed.lX

noncomputable def MIPRE.Tailored.AnsRed.Typed.nF : Cost.PolyTimeFun LpIn Cost.Unary

The two questions' lengths, N.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.kF : Role → Cost.PolyTimeFun ArParams Cost.Unary

The number of slots of a role.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.AnsRed.Typed.kF x✝ = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 2)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ncF : LIDT.CL.Ty → Cost.PolyTimeFun ArParams Cost.Unary

The number of coefficients of a codeword at a type.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.AnsRed.Typed.ncF MIPRE.LIDT.CL.Ty.point = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 1)

noncomputable def MIPRE.Tailored.AnsRed.Typed.gatesF : Cost.PolyTimeFun SAT.Circuit (List SAT.Gate)

The gates of a circuit.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.gatesF_apply (C : SAT.Circuit) : gatesF.toFun C = C.gates

noncomputable def MIPRE.Tailored.AnsRed.Typed.ptsF (q : Cost.PolyTimeFun LpIn Cost.BitStr) : Cost.PolyTimeFun LpIn (List Cost.BitStr)

The point coordinates of a question: the first run of its low-degree blocks.

Equations

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

The checks at a pair of types

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldInF (u v : Role × LIDT.CL.Ty) : Cost.PolyTimeFun LpIn LdCIn

The low-degree checks' input at a pair of types.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ccInF (u v : Role × LIDT.CL.Ty) : Cost.PolyTimeFun LpIn ConsIn

The consistency checks' input at a pair of types.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.indInF (o : Cost.PolyTimeFun LpIn Cost.Unary) (r : Role × LIDT.CL.Ty) (q : Cost.PolyTimeFun LpIn Cost.BitStr) : Cost.PolyTimeFun LpIn IndCIn

The indifference checks' input of a question of type r at offset o.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.circQ (R : ArRoutine) (qa qb : Cost.PolyTimeFun LpIn Cost.BitStr) : Cost.PolyTimeFun LpIn SAT.Circuit

The circuit of a question's seed, from the input sampler's questions there.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.prfInF (R : ArRoutine) (o : Cost.PolyTimeFun LpIn Cost.Unary) (q aR qa qb : Cost.PolyTimeFun LpIn Cost.BitStr) : Cost.PolyTimeFun LpIn PrfIn

The proof check's input of a question at offset o, with readable answer aR.

Equations

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

The edge and the lengths

noncomputable def MIPRE.Tailored.AnsRed.Typed.selF (p : (Fin gdA → CL.𝔽₂) × (Fin gdA → CL.𝔽₂)) : Option ((Role × LIDT.CL.Ty) × Role × LIDT.CL.Ty)

The edge two graph views sit on, Alice's first.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.edgeF : Cost.PolyTimeFun LpIn (Option ((Role × LIDT.CL.Ty) × Role × LIDT.CL.Ty))

The edge of two questions, by a finite table on their graph views.

Equations

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

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

A unary number as a natural number.

Equations

• MIPRE.Tailored.AnsRed.Typed.uNat = MIPRE.Cost.PolyTimeFun.addUnary.ap₂ (MIPRE.Cost.PolyTimeFun.const 0) (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary)

noncomputable def MIPRE.Tailored.AnsRed.Typed.lenOkF : Cost.PolyTimeFun LpIn Bool

The length check: both readable answers have their questions' readable lengths.

Equations

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

The last stage

@[reducible, inline]

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

The input of the processor's last stage: the parameters, the two questions' bits and readable answers, and the constraints of the two questions' proof checks, which earlier stages compute.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.embF : Cost.PolyTimeFun LpFin LpIn

The typed view of the last stage's input, without input sampler questions or programs.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.finBranchF (u v : Role × LIDT.CL.Ty) : Cost.PolyTimeFun LpFin (List Cost.BitStr)

The checks at a pair of types: the low-degree checks at one role, the consistency checks at one low-degree type, the indifference checks of each answer, and the proof check of each oracle point answer, read off the input.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.lpFinal : Cost.PolyTimeFun LpFin (List Cost.BitStr)

The processor's last stage: on the edge of the two questions, if the readable answers have their lengths, the checks at the edge's pair of types; nothing otherwise.

Equations

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

Correctness of the pieces

theorem MIPRE.Tailored.AnsRed.Typed.kF_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) (r : Role) : (kF r).toFun (arParams t j d L e) = Cost.unary (slotsOf L r).length

theorem MIPRE.Tailored.AnsRed.Typed.ncF_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) (S : LIDT.CL.Ty) : (ncF S).toFun (arParams t j d L e) = Cost.unary (ncoef j d S)

theorem MIPRE.Tailored.AnsRed.Typed.dtF_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : dtF.toFun (arParams t j d L e) = Cost.unary (D j * t)

theorem MIPRE.Tailored.AnsRed.Typed.idxAt_of_typeOf {s : ℕ} {q : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin s) → CL.𝔽₂} {u : Role × LIDT.CL.Ty} (h : typeOf arGraph q = some u) (κ : Bool) : idxAt (CL.pull Function.Embedding.inl q) κ = (cntIdx u.1 κ, ncIdx u.2)

A typed view's indices are its type's.

theorem MIPRE.Tailored.AnsRed.Typed.edgeOf_eq_selectedEdge {s : ℕ} (x y : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin s) → CL.𝔽₂) : edgeOf arGraph x y = Option.map (fun (uv : (Role × LIDT.CL.Ty) × Role × LIDT.CL.Ty) => ((uv.1, CL.pull Function.Embedding.inr x), uv.2, CL.pull Function.Embedding.inr y)) (CL.Detyping.DeciderProgram.selectedEdge arGraph (CL.pull Function.Embedding.inl x) (CL.pull Function.Embedding.inl y))

The edge of two detyped questions is read off their selected edge.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.lpIn {s : ℕ} (p : ArParams) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin s) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) : LpIn

The input at two detyped questions.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.edgeF_lpIn {s : ℕ} (p : ArParams) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin s) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) : edgeF.toFun (lpIn p qx qy aR bR w c) = CL.Detyping.DeciderProgram.selectedEdge arGraph (CL.pull Function.Embedding.inl qx) (CL.pull Function.Embedding.inl qy)

theorem MIPRE.Tailored.AnsRed.Typed.lenF_lpIn_x {s : ℕ} (p : ArParams) (qx : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin s) → CL.𝔽₂) {t j d : ℕ} {L : PcpDims} {e : Cost.Data} (hp : p = arParams t j d L e) {u : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (κ : Bool) : lenF.toFun (p, CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv s) qx), κ) = Cost.unary (if κ = true then lenL t j d L u else lenR t j d L u)

theorem MIPRE.Tailored.AnsRed.Typed.lenOkF_lpIn {s : ℕ} (p : ArParams) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin s) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) {t j d : ℕ} {L : PcpDims} {e : Cost.Data} (hp : p = arParams t j d L e) {u v : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (hv : typeOf arGraph qy = some v) : lenOkF.toFun (lpIn p qx qy aR bR w c) = decide (List.length aR = lenR t j d L u ∧ List.length bR = lenR t j d L v)

theorem MIPRE.Tailored.AnsRed.Typed.LdFamily.sel_chi (F : LdFamily) (n : ℕ) (a : Fq (F.t n) ⋯) : ↑((F.sel n).χ a) = Introspection.SeedProgram.selectorProg.toFun (Cost.unary (F.t n), Cost.unary (F.j n), (SAT.shoupBinField (F.t n) ⋯).toBits a)

The family's selector is the introspection stage's selector program.

The checks on the processor's input

theorem MIPRE.Tailored.AnsRed.Typed.ldbF_toBits {t j d : ℕ} {L : PcpDims} {e : Cost.Data} {rV : ℕ} {p : ArParams} (hp : p = arParams t j d L e) (q : Cost.PolyTimeFun LpIn Cost.BitStr) (z : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (rV + D j * t)) → CL.𝔽₂) (inp : LpIn) (hpi : lP.toFun inp = p) (hq : q.toFun inp = CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (rV + D j * t)) z)) : (ldbF q).toFun inp = List.drop rV (CL.toBits (CL.pull Function.Embedding.inr z))

The low-degree bits of a question's vector part.

theorem MIPRE.Tailored.AnsRed.Typed.nAF_lpIn {t j d : ℕ} {L : PcpDims} {e : Cost.Data} {rV : ℕ} {p : ArParams} (hp : p = arParams t j d L e) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (rV + D j * t)) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) {u : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) : nAF.toFun (lpIn p qx qy aR bR w c) = Cost.unary (len t j d L u)

theorem MIPRE.Tailored.AnsRed.Typed.nF_lpIn {t j d : ℕ} {L : PcpDims} {e : Cost.Data} {rV : ℕ} {p : ArParams} (hp : p = arParams t j d L e) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (rV + D j * t)) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) {u v : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (hv : typeOf arGraph qy = some v) : nF.toFun (lpIn p qx qy aR bR w c) = Cost.unary (len t j d L u + len t j d L v)

theorem MIPRE.Tailored.AnsRed.Typed.ldInF_lpIn {t j d : ℕ} {L : PcpDims} {e : Cost.Data} {rV : ℕ} {p : ArParams} (hp : p = arParams t j d L e) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (rV + D j * t)) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) {u v : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (hv : typeOf arGraph qy = some v) : (ldInF u v).toFun (lpIn p qx qy aR bR w c) = ldIn (slotsOf L u.1).length (len t j d L u) (len t j d L u + len t j d L v) u.2 v.2 (CL.pull Function.Embedding.inr qx) (CL.pull Function.Embedding.inr qy)

theorem MIPRE.Tailored.AnsRed.Typed.ccInF_lpIn {t j d : ℕ} {L : PcpDims} {e : Cost.Data} {rV : ℕ} {p : ArParams} (hp : p = arParams t j d L e) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (rV + D j * t)) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) {u v : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (hv : typeOf arGraph qy = some v) : (ccInF u v).toFun (lpIn p qx qy aR bR w c) = (Cost.unary t, Cost.unary (ncoef j d u.2), Cost.unary (len t j d L u), Cost.unary (len t j d L u + len t j d L v), Cost.unary (rSlots L).length, u.1, v.1)

theorem MIPRE.Tailored.AnsRed.Typed.indInF_lX {t j d : ℕ} {L : PcpDims} {e : Cost.Data} {rV : ℕ} {p : ArParams} (hp : p = arParams t j d L e) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (rV + D j * t)) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) {u v : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (hv : typeOf arGraph qy = some v) : (indInF (Cost.PolyTimeFun.const (Cost.unary 0)) u lX).toFun (lpIn p qx qy aR bR w c) = (arParams t j d L e, Cost.unary 0, Cost.unary (len t j d L u + len t j d L v), u, List.drop rV (CL.toBits (CL.pull Function.Embedding.inr qx)))

theorem MIPRE.Tailored.AnsRed.Typed.indInF_lY {t j d : ℕ} {L : PcpDims} {e : Cost.Data} {rV : ℕ} {p : ArParams} (hp : p = arParams t j d L e) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (rV + D j * t)) → CL.𝔽₂) (aR bR : Cost.BitStr) (w : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : (Cost.Prog × Cost.Prog × Cost.Prog) × (ℕ × ℕ × ℕ) × ℕ) {u v : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (hv : typeOf arGraph qy = some v) : (indInF nAF v lY).toFun (lpIn p qx qy aR bR w c) = (arParams t j d L e, Cost.unary (len t j d L u), Cost.unary (len t j d L u + len t j d L v), v, List.drop rV (CL.toBits (CL.pull Function.Embedding.inr qy)))

theorem MIPRE.Tailored.AnsRed.Typed.ptsF_getD {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {rV : ℕ} {p : ArParams} (hp : p = arParams t j d L e) (q : Cost.PolyTimeFun LpIn Cost.BitStr) (z : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (rV + D j * t)) → CL.𝔽₂) (inp : LpIn) (hpi : lP.toFun inp = p) (hq : q.toFun inp = CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (rV + D j * t)) z)) (hLM : L.m ≤ 2 ^ j) (X : Fin L.m) : ((ptsF q).toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (ptm L hLM ((regs j).ptOf (ldPart t ht j rV (CL.pull Function.Embedding.inr z))) X)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ArRoutine.qIn (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (qx qy : 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.𝔽₂) (aR bR : Cost.BitStr) : LpIn

The processor's last stage's input at two detyped questions of the answer-reduced game: with the input sampler's questions at their seeds, and the input's programs.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.proof_lX (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (qx qy : 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.𝔽₂) (aR bR : Cost.BitStr) {u v : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (hv : typeOf arGraph qy = some v) : proofConsF.toFun ((R.prfInF (Cost.PolyTimeFun.const (Cost.unary 0)) lX lA lAx lBx).toFun (R.qIn lam mu sigma n V qx qy aR bR)) = proofCons ((R.fam lam mu sigma).j n) (R.d lam mu sigma n) (R.L lam mu sigma n) ⋯ (len ((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) u + len ((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) v) 0 (circOf (R.L lam mu sigma n) V n (R.circ lam mu sigma n V) ⋯ (rolePart ((R.fam lam mu sigma).t n) ((R.fam lam mu sigma).j n) (V.sampler.dim n) (CL.pull Function.Embedding.inr qx))) ((regs ((R.fam lam mu sigma).j n)).ptOf (ldPart ((R.fam lam mu sigma).t n) ⋯ ((R.fam lam mu sigma).j n) (V.sampler.dim n) (CL.pull Function.Embedding.inr qx))) aR

The proof check of the first question, an oracle point question, on the processor's input.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.proof_lY (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (qx qy : 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.𝔽₂) (aR bR : Cost.BitStr) {u v : Role × LIDT.CL.Ty} (hu : typeOf arGraph qx = some u) (hv : typeOf arGraph qy = some v) : proofConsF.toFun ((R.prfInF nAF lY lB lAy lBy).toFun (R.qIn lam mu sigma n V qx qy aR bR)) = proofCons ((R.fam lam mu sigma).j n) (R.d lam mu sigma n) (R.L lam mu sigma n) ⋯ (len ((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) u + len ((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) v) (len ((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) u) (circOf (R.L lam mu sigma n) V n (R.circ lam mu sigma n V) ⋯ (rolePart ((R.fam lam mu sigma).t n) ((R.fam lam mu sigma).j n) (V.sampler.dim n) (CL.pull Function.Embedding.inr qy))) ((regs ((R.fam lam mu sigma).j n)).ptOf (ldPart ((R.fam lam mu sigma).t n) ⋯ ((R.fam lam mu sigma).j n) (V.sampler.dim n) (CL.pull Function.Embedding.inr qy))) bR

The proof check of the second question, an oracle point question, on the processor's input.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpFinal_eq (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (qx qy : 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.𝔽₂) (aR bR : Cost.BitStr) {ℓ' : ℕ} (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 : ℕ) : lpFinal.toFun (R.params 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)) qx), 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)) qy), aR, bR), proofConsF.toFun ((R.prfInF (Cost.PolyTimeFun.const (Cost.unary 0)) lX lA lAx lBx).toFun (R.qIn lam mu sigma n V qx qy aR bR)), proofConsF.toFun ((R.prfInF nAF lY lB lAy lBy).toFun (R.qIn lam mu sigma n V qx qy aR bR))) = (arPresented (R.d lam mu sigma n) ⋯ ((R.fam lam mu sigma).sel n) (R.L lam mu sigma n) ⋯ V n (R.circ lam mu sigma n V) ⋯ P B).cons qx qy aR bR

The processor's last stage outputs the presented game's constraints, at every pair of detyped questions, given the constraints of the two questions' proof checks.