The proof check, as a program

Slice P4h of planning/aldous-lyons-track.md: the constraints of the proof check of the answer-reduced game (Typed.proofCons) at the oracle's point question, computed by a program from the parameters, the point, the oracle's readable answer and the seed's circuit.

• circValF: the circuit polynomial at the point, by the circuit evaluator of MIPRE.SAT.Circuit.circuitBits (circValF_eq).
• guardF: the readable checks of the proof check, the formula check and the six assignment checks, on the oracle's decoded readable answer (guardF_eq, PassesR). Each is a comparison of two field expressions in the point's coordinates and the readable values, written with the combinators of ArLpArith; the positions of the readable values are the slots' indices idxO, computed from the parameters (wAt_slot).

The proof check's linear equations, its constraints when the guard holds, follow.

The circuit polynomial at a point

noncomputable def MIPRE.Tailored.AnsRed.Typed.circValF : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.Unary × List Cost.BitStr × List SAT.Gate) Cost.BitStr

The circuit polynomial at a point, on (t, nIn, s, the point's coordinates, the gates): the evaluator of the circuit on the coordinates of its nIn inputs and s gates.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.getD_eq_getElem {α : Type u_1} (l : List α) (d : α) {i : ℕ} (h : i < l.length) : l.getD i d = l[i]

theorem MIPRE.Tailored.AnsRed.Typed.circValF_eq {t : ℕ} {ht : 1 ≤ t} {m : ℕ} (C : SAT.Circuit) (hC : C.WellFormed) (hm : C.inputs + C.size = m) (q : Fin m → Fq t ht) (pts : List Cost.BitStr) (hpts : ∀ (i : Fin m), pts.getD ↑i [] = (SAT.shoupBinField t ht).toBits (q i)) : circValF.toFun (Cost.unary t, Cost.unary C.inputs, Cost.unary C.size, pts, C.gates) = (SAT.shoupBinField t ht).toBits ((MvPolynomial.eval q) ((MvPolynomial.rename (Fin.cast hm)) C.finiteArith))

The evaluator computes the circuit polynomial at a point whose coordinates are given.

The input of the proof check

@[reducible, inline]

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

The input of the proof check: the parameters, the offset o of the oracle's answer, N, the coordinates of the point, the oracle's readable answer and the gates of the seed's circuit.

Equations

• MIPRE.Tailored.AnsRed.Typed.PrfIn = (MIPRE.Tailored.AnsRed.Typed.ArParams × MIPRE.Cost.Unary × MIPRE.Cost.Unary × List MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × List MIPRE.SAT.Gate)

noncomputable def MIPRE.Tailored.AnsRed.Typed.rP : Cost.PolyTimeFun PrfIn ArParams

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.rO : Cost.PolyTimeFun PrfIn Cost.Unary

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.rN : Cost.PolyTimeFun PrfIn Cost.Unary

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.rPts : Cost.PolyTimeFun PrfIn (List Cost.BitStr)

Equations

• MIPRE.Tailored.AnsRed.Typed.rPts = 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.rA : Cost.PolyTimeFun PrfIn Cost.BitStr

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.rG : Cost.PolyTimeFun PrfIn (List SAT.Gate)

Equations

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

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

nIn, the number of the circuits' inputs.

Equations

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

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

R, the oracle's readable count 6 + m + 2ℓ + ◇' + 3r.

Equations

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

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

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

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

theorem MIPRE.Tailored.AnsRed.Typed.rcF_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : rcF.toFun (arParams t j d L e) = Cost.unary (rSlots L).length

Atoms

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.jT {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

The field width, through ρ.

Equations

• MIPRE.Tailored.AnsRed.Typed.jT ρ = MIPRE.Tailored.AnsRed.Typed.pT.comp (MIPRE.Tailored.AnsRed.Typed.rP.comp ρ)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.jL {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

The window width ℓ, through ρ.

Equations

• MIPRE.Tailored.AnsRed.Typed.jL ρ = MIPRE.Tailored.AnsRed.Typed.pL.comp (MIPRE.Tailored.AnsRed.Typed.rP.comp ρ)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.jDm {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

The index width ◇, through ρ.

Equations

• MIPRE.Tailored.AnsRed.Typed.jDm ρ = MIPRE.Tailored.AnsRed.Typed.pDm.comp (MIPRE.Tailored.AnsRed.Typed.rP.comp ρ)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.jR {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

The witness index width r, through ρ.

Equations

• MIPRE.Tailored.AnsRed.Typed.jR ρ = MIPRE.Tailored.AnsRed.Typed.pR.comp (MIPRE.Tailored.AnsRed.Typed.rP.comp ρ)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.jOW {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

◇', through ρ.

Equations

• MIPRE.Tailored.AnsRed.Typed.jOW ρ = MIPRE.Tailored.AnsRed.Typed.oWF.comp (MIPRE.Tailored.AnsRed.Typed.rP.comp ρ)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.jM {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

m, through ρ.

Equations

• MIPRE.Tailored.AnsRed.Typed.jM ρ = MIPRE.Tailored.AnsRed.Typed.mF.comp (MIPRE.Tailored.AnsRed.Typed.rP.comp ρ)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.jRc {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

R, through ρ.

Equations

• MIPRE.Tailored.AnsRed.Typed.jRc ρ = MIPRE.Tailored.AnsRed.Typed.rcF.comp (MIPRE.Tailored.AnsRed.Typed.rP.comp ρ)

noncomputable def MIPRE.Tailored.AnsRed.Typed.qAt {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (w : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.BitStr

The point's coordinate at a wire.

Equations

• MIPRE.Tailored.AnsRed.Typed.qAt ρ w = (MIPRE.Cost.PolyTimeFun.headD []).comp (MIPRE.Cost.PolyTimeFun.drop.comp ((MIPRE.Tailored.AnsRed.Typed.rPts.comp ρ).pair w))

noncomputable def MIPRE.Tailored.AnsRed.Typed.wAt {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (w : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.BitStr

The oracle's readable value at a position.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.qAt_eq {t : ℕ} {ht : 1 ≤ t} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {L : PcpDims} {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun (ρ.toFun x)).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) {w : Cost.PolyTimeFun J Cost.Unary} (X : Fin L.m) (hw : w.toFun x = Cost.unary ↑X) : (qAt ρ w).toFun x = (SAT.shoupBinField t ht).toBits (q X)

theorem MIPRE.Tailored.AnsRed.Typed.wAt_eq {t : ℕ} {ht : 1 ≤ t} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {w : Cost.PolyTimeFun J Cost.Unary} {k : ℕ} (hw : w.toFun x = Cost.unary k) : (wAt ρ w).toFun x = (SAT.shoupBinField t ht).toBits (elt t ht (rA.toFun (ρ.toFun x)) (k * t))

theorem MIPRE.Tailored.AnsRed.Typed.vals_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} (aR : Cost.BitStr) (s : Slot L) : vals t ht j d L aR s = elt t ht aR (idxO s * t)

A readable value of the oracle's point answer is its window at the slot's position.

Wires and positions

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.uc {J : Type} [Cost.SizedEncoding J] (c : ℕ) : Cost.PolyTimeFun J Cost.Unary

A constant in unary.

Equations

• MIPRE.Tailored.AnsRed.Typed.uc c = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary c)

noncomputable def MIPRE.Tailored.AnsRed.Typed.wB0 {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

ℓ + 1, the parity wire of the window B.

Equations

• MIPRE.Tailored.AnsRed.Typed.wB0 ρ = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.jL ρ) (MIPRE.Tailored.AnsRed.Typed.uc 1)

noncomputable def MIPRE.Tailored.AnsRed.Typed.wC0 {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

ℓ + 1 + (ℓ + 1), the parity wire of the window C.

Equations

• MIPRE.Tailored.AnsRed.Typed.wC0 ρ = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.wB0 ρ) (MIPRE.Tailored.AnsRed.Typed.wB0 ρ)

noncomputable def MIPRE.Tailored.AnsRed.Typed.wVO {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The wire of index i of O.

Equations

• MIPRE.Tailored.AnsRed.Typed.wVO ρ i = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.wC0 ρ) (MIPRE.Tailored.AnsRed.Typed.uc 1)) i

noncomputable def MIPRE.Tailored.AnsRed.Typed.wVA {J : Type} [Cost.SizedEncoding J] (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The wire of index i of the window A.

Equations

• MIPRE.Tailored.AnsRed.Typed.wVA i = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.uc 1) i

noncomputable def MIPRE.Tailored.AnsRed.Typed.wVB {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The wire of index i of the window B.

Equations

• MIPRE.Tailored.AnsRed.Typed.wVB ρ i = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.wB0 ρ) (MIPRE.Tailored.AnsRed.Typed.uc 1)) i

noncomputable def MIPRE.Tailored.AnsRed.Typed.wVW {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (k : ℕ) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The wire of index i of the k-th witness index.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.wSgn {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (k : ℕ) : Cost.PolyTimeFun J Cost.Unary

The k-th sign wire.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.pαR {J : Type} [Cost.SizedEncoding J] (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of α_R X.

Equations

• MIPRE.Tailored.AnsRed.Typed.pαR i = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.uc 6) i

noncomputable def MIPRE.Tailored.AnsRed.Typed.pβA {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of β_A i.

Equations

• MIPRE.Tailored.AnsRed.Typed.pβA ρ i = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.uc 6) (MIPRE.Tailored.AnsRed.Typed.jM ρ)) i

noncomputable def MIPRE.Tailored.AnsRed.Typed.pβB {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of β_B i.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.pβO {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of β_O i.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.pβW {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (k : ℕ) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of β_W k i.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.wB0_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) : (wB0 ρ).toFun x = Cost.unary ↑L.πB

theorem MIPRE.Tailored.AnsRed.Typed.wC0_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) : (wC0 ρ).toFun x = Cost.unary ↑L.πC

theorem MIPRE.Tailored.AnsRed.Typed.wVO_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.oW) (hi : i.toFun x = Cost.unary ↑a) : (wVO ρ i).toFun x = Cost.unary ↑(L.vO a)

theorem MIPRE.Tailored.AnsRed.Typed.wVA_eq {J : Type} [Cost.SizedEncoding J] {x : J} {L : PcpDims} {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.ℓ) (hi : i.toFun x = Cost.unary ↑a) : (wVA i).toFun x = Cost.unary ↑(L.vA a)

theorem MIPRE.Tailored.AnsRed.Typed.wVB_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.ℓ) (hi : i.toFun x = Cost.unary ↑a) : (wVB ρ i).toFun x = Cost.unary ↑(L.vB a)

theorem MIPRE.Tailored.AnsRed.Typed.wVW_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) (k : Fin 3) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.r) (hi : i.toFun x = Cost.unary ↑a) : (wVW ρ (↑k) i).toFun x = Cost.unary ↑(L.vW k a)

theorem MIPRE.Tailored.AnsRed.Typed.wSgn_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) (k : Fin 6) : (wSgn ρ ↑k).toFun x = Cost.unary ↑(L.sgn k)

theorem MIPRE.Tailored.AnsRed.Typed.pαR_eq {J : Type} [Cost.SizedEncoding J] {x : J} {L : PcpDims} {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.m) (hi : i.toFun x = Cost.unary ↑a) : (pαR i).toFun x = Cost.unary (idxO (Slot.αR a))

theorem MIPRE.Tailored.AnsRed.Typed.pβA_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.ℓ) (hi : i.toFun x = Cost.unary ↑a) : (pβA ρ i).toFun x = Cost.unary (idxO (Slot.βA a))

theorem MIPRE.Tailored.AnsRed.Typed.pβB_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.ℓ) (hi : i.toFun x = Cost.unary ↑a) : (pβB ρ i).toFun x = Cost.unary (idxO (Slot.βB a))

theorem MIPRE.Tailored.AnsRed.Typed.pβO_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.oW) (hi : i.toFun x = Cost.unary ↑a) : (pβO ρ i).toFun x = Cost.unary (idxO (Slot.βO a))

theorem MIPRE.Tailored.AnsRed.Typed.pβW_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) (k : Fin 3) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.r) (hi : i.toFun x = Cost.unary ↑a) : (pβW ρ (↑k) i).toFun x = Cost.unary (idxO (Slot.βW k a))

The readable checks

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ι₀ : Cost.PolyTimeFun PrfIn PrfIn

The identity of the proof check's input.

Equations

• MIPRE.Tailored.AnsRed.Typed.ι₀ = MIPRE.Cost.PolyTimeFun.id MIPRE.Tailored.AnsRed.Typed.PrfIn

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ι₁ : Cost.PolyTimeFun (Cost.Unary × PrfIn) PrfIn

The input, under an index.

Equations

• MIPRE.Tailored.AnsRed.Typed.ι₁ = MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgF (g : Cost.PolyTimeFun PrfIn Cost.BitStr) (term : Cost.PolyTimeFun (Cost.Unary × PrfIn) Cost.BitStr) (k : Cost.PolyTimeFun PrfIn Cost.Unary) : Cost.PolyTimeFun PrfIn Bool

An assignment check g (1 - g) = ∑_{i < k} term i.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.termF (wire pos : Cost.PolyTimeFun (Cost.Unary × PrfIn) Cost.Unary) : Cost.PolyTimeFun (Cost.Unary × PrfIn) Cost.BitStr

A term x_i (1 - x_i) β_i of an assignment check: the point's coordinate at a wire and the readable value at a position, both of the index.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgAF : Cost.PolyTimeFun PrfIn Bool

The assignment check of g_A.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgBF : Cost.PolyTimeFun PrfIn Bool

The assignment check of g_B.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgOF : Cost.PolyTimeFun PrfIn Bool

The assignment check of g_O.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgWF (k : ℕ) : Cost.PolyTimeFun PrfIn Bool

The assignment check of g_{W,k}.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.circVF : Cost.PolyTimeFun PrfIn Cost.BitStr

The circuit polynomial at the point.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.litF (π : Cost.PolyTimeFun PrfIn Cost.Unary) (g k : ℕ) : Cost.PolyTimeFun PrfIn Cost.BitStr

A window literal p_π w - p_ε.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.witF (k : ℕ) : Cost.PolyTimeFun PrfIn Cost.BitStr

A witness literal w - p_ε.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.formF : Cost.PolyTimeFun PrfIn Bool

The formula check.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.guardF : Cost.PolyTimeFun PrfIn Bool

The readable checks of the proof check, as a program.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.jT_ι₀ {t j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) : (jT ι₀).toFun inp = Cost.unary t

theorem MIPRE.Tailored.AnsRed.Typed.asgF_eq {t : ℕ} {ht : 1 ≤ t} {inp : PrfIn} (hT : (jT ι₀).toFun inp = Cost.unary t) {g : Cost.PolyTimeFun PrfIn Cost.BitStr} {gv : Fq t ht} (hg : g.toFun inp = (SAT.shoupBinField t ht).toBits gv) {term : Cost.PolyTimeFun (Cost.Unary × PrfIn) Cost.BitStr} {k : Cost.PolyTimeFun PrfIn Cost.Unary} {K : ℕ} (hk : k.toFun inp = Cost.unary K) (x β : Fin K → Fq t ht) (hterm : ∀ (i : Fin K), term.toFun (Cost.unary ↑i, inp) = (SAT.shoupBinField t ht).toBits (x i * (1 - x i) * β i)) : (asgF g term k).toFun inp = decide (gv * (1 - gv) = ∑ i : Fin K, x i * (1 - x i) * β i)

theorem MIPRE.Tailored.AnsRed.Typed.termF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) {wire pos : Cost.PolyTimeFun (Cost.Unary × PrfIn) Cost.Unary} (i : ℕ) (X : Fin L.m) (k : ℕ) (hw : wire.toFun (Cost.unary i, inp) = Cost.unary ↑X) (hp : pos.toFun (Cost.unary i, inp) = Cost.unary k) : (termF wire pos).toFun (Cost.unary i, inp) = (SAT.shoupBinField t ht).toBits (q X * (1 - q X) * elt t ht (rA.toFun inp) (k * t))

theorem MIPRE.Tailored.AnsRed.Typed.wAt_slot {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {s : Slot L} {g : ℕ} (hg : idxO s = g) : (wAt ι₀ (uc g)).toFun inp = (SAT.shoupBinField t ht).toBits (vals t ht j d L (rA.toFun inp) s)

theorem MIPRE.Tailored.AnsRed.Typed.asgAF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) : asgAF.toFun inp = decide (vals t ht j d L (rA.toFun inp) Slot.gA * (1 - vals t ht j d L (rA.toFun inp) Slot.gA) = ∑ i : Fin L.ℓ, (q ∘ L.vA) i * (1 - (q ∘ L.vA) i) * vals t ht j d L (rA.toFun inp) (Slot.βA i))

theorem MIPRE.Tailored.AnsRed.Typed.asgBF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) : asgBF.toFun inp = decide (vals t ht j d L (rA.toFun inp) Slot.gB * (1 - vals t ht j d L (rA.toFun inp) Slot.gB) = ∑ i : Fin L.ℓ, (q ∘ L.vB) i * (1 - (q ∘ L.vB) i) * vals t ht j d L (rA.toFun inp) (Slot.βB i))

theorem MIPRE.Tailored.AnsRed.Typed.asgOF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) : asgOF.toFun inp = decide (vals t ht j d L (rA.toFun inp) Slot.gO * (1 - vals t ht j d L (rA.toFun inp) Slot.gO) = ∑ i : Fin L.oW, (q ∘ L.vO) i * (1 - (q ∘ L.vO) i) * vals t ht j d L (rA.toFun inp) (Slot.βO i))

theorem MIPRE.Tailored.AnsRed.Typed.asgWF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) (k : Fin 3) : (asgWF ↑k).toFun inp = decide (vals t ht j d L (rA.toFun inp) (Slot.gW k) * (1 - vals t ht j d L (rA.toFun inp) (Slot.gW k)) = ∑ i : Fin L.r, (q ∘ L.vW k) i * (1 - (q ∘ L.vW k) i) * vals t ht j d L (rA.toFun inp) (Slot.βW k i))

theorem MIPRE.Tailored.AnsRed.Typed.formF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) (C : SAT.Circuit) (hC : C.WellFormed) (hm : C.inputs + C.size = L.m) (hin : C.inputs = L.nIn) (hs : C.size = L.s) (hG : rG.toFun inp = C.gates) : formF.toFun inp = decide ((MvPolynomial.eval q) ((MvPolynomial.rename (Fin.cast hm)) C.finiteArith) * (q L.πA * vals t ht j d L (rA.toFun inp) Slot.gA - q (L.sgn 0)) * (q L.πB * vals t ht j d L (rA.toFun inp) Slot.gB - q (L.sgn 1)) * (q L.πC * vals t ht j d L (rA.toFun inp) Slot.gO - q (L.sgn 2)) * ∏ k : Fin 3, (vals t ht j d L (rA.toFun inp) (Slot.gW k) - q (L.sgn (3 + Fin.castLE ⋯ k))) = ∑ X : Fin L.m, q X * (1 - q X) * vals t ht j d L (rA.toFun inp) (Slot.αR X))

theorem MIPRE.Tailored.AnsRed.Typed.guardF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) (C : SAT.Circuit) (hC : C.WellFormed) (hm : C.inputs + C.size = L.m) (hin : C.inputs = L.nIn) (hs : C.size = L.s) (hG : rG.toFun inp = C.gates) : guardF.toFun inp = decide (PassesR ((MvPolynomial.rename (Fin.cast hm)) C.finiteArith) (vals t ht j d L (rA.toFun inp)) q)

The guard program decides the readable checks of the proof check.