The honest PCP of accepted answers

The completeness clause of cor:functional_viewpoint_final: the map PCP_{xy} from answers a^R, a^L, b^R, b^L at a pair of questions (x, y) of the n-th game of a tailored verifier to a PCP, for a circuit that describes the output indicator L* of the verifier through the windows of lem:ar-window-describer.

• The readable tables (honestR): the readable answers padded with zeros to 2^ℓ bits, the table O of the decoupled system (lsTable), and witnesses of the described formula for their windows (honestW, chosen once from the readable data). They depend only on a^R, b^R.
• The linear tables (honestL): Extend of the linear answers (tbl, ext), F₂-linear in a^L, b^L with coefficients read from a^R, b^R.
• identities_honest: when the game accepts the answers, the honest PCP of these tables satisfies the thirteen checks identically. L* accepts the padded strings (claim:properties_of_L*, item 1), so the circuit's formula is satisfied by their windows (lem:ar-window-describer), and the linear tables satisfy the system the table holds (claim:properties_of_L*, item 2).

Windows of strings

theorem MIPRE.Tailored.AnsRed.winOf_getD (s : Cost.BitStr) (o : ℕ) {j : ℕ} (hj : o + j / 2 < List.length s) : winOf (fun (c : ℕ) => List.getD s (o + c) false) j = SAT.tapeBits s (2 * o + j)

The window table read off a string at a cell offset is the string's tape encoding there.

theorem MIPRE.Tailored.AnsRed.winOf_getD_zero (s : Cost.BitStr) {j : ℕ} (hj : j / 2 < List.length s) : winOf (fun (c : ℕ) => List.getD s c false) j = SAT.tapeBits s j

The honest tables

noncomputable def MIPRE.Tailored.AnsRed.honestA (L : PcpDims) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (xq yq : V.Questions n) (aR bR : Cost.BitStr) : Cost.BitStr

The first string L* reads on honest answers (claim:properties_of_L*, item 1): the readable answer padded with zeros to 2^ℓ bits, then the table of the decoupled system.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.honestB (L : PcpDims) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (yq : V.Questions n) (bR : Cost.BitStr) : Cost.BitStr

The second string L* reads on honest answers: the readable answer padded with zeros.

Equations

• MIPRE.Tailored.AnsRed.honestB L V n yq bR = bR ++ List.replicate (2 ^ L.ℓ - (V.tgame n).lenR yq) false

noncomputable def MIPRE.Tailored.AnsRed.honestW (L : PcpDims) (Cc : SAT.Circuit) (A B C : ℕ → Bool) : Fin 3 → ℕ → Bool

Witnesses of the formula a circuit describes for three window tables, when there are some.

Equations

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

theorem MIPRE.Tailored.AnsRed.sat_honestW {L : PcpDims} {Cc : SAT.Circuit} {A B C : ℕ → Bool} (h : ∃ (w₁ : Fin (2 ^ L.r) → Bool) (w₂ : Fin (2 ^ L.r) → Bool) (w₃ : Fin (2 ^ L.r) → Bool), (Cc.formula6 (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r).Sat (fun (j : Fin (2 ^ (L.ℓ + 1))) => A ↑j) (fun (j : Fin (2 ^ (L.ℓ + 1))) => B ↑j) (fun (j : Fin (2 ^ (L.oW + 1))) => C ↑j) w₁ w₂ w₃) : (Cc.formula6 (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r).Sat (fun (j : Fin (2 ^ (L.ℓ + 1))) => A ↑j) (fun (j : Fin (2 ^ (L.ℓ + 1))) => B ↑j) (fun (j : Fin (2 ^ (L.oW + 1))) => C ↑j) (fun (j : Fin (2 ^ L.r)) => honestW L Cc A B C 0 ↑j) (fun (j : Fin (2 ^ L.r)) => honestW L Cc A B C 1 ↑j) fun (j : Fin (2 ^ L.r)) => honestW L Cc A B C 2 ↑j

noncomputable def MIPRE.Tailored.AnsRed.honestR (L : PcpDims) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (Cc : SAT.Circuit) (xq yq : V.Questions n) (aR bR : Cost.BitStr) : RTables

The readable tables of the honest PCP: the cells of the padded readable answers, the table O, and witnesses for their windows. They depend only on the readable answers.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.honestL (L : PcpDims) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (xq yq : V.Questions n) (aR aL bR bL : Cost.BitStr) : LTables

The linear tables of the honest PCP: Extend of the linear answers (the table of the linear answers, and three times its extension to the triangulation variables).

Equations

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

Completeness

theorem MIPRE.Tailored.AnsRed.lenIs_lenOf {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) {x : Cost.BitStr} (h : V.LenDefined n x) (κ : Bool) : LenIs V.len n x κ (V.lenOf n x κ)

theorem MIPRE.Tailored.AnsRed.lstar_accepts_honest {L : PcpDims} (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (xq yq : V.Questions n) {aR bR : Cost.BitStr} (hℓ : List.length (prm.toFun n).1 = L.ℓ) (hdm : List.length (prm.toFun n).2 = L.dm) (hx : V.LenDefined n (CL.toBits xq)) (hy : V.LenDefined n (CL.toBits yq)) (hlp : ∃ (cs : List Cost.BitStr), LpIs V.lp n (CL.toBits xq) (CL.toBits yq) aR bR cs) (haR : List.length aR = (V.tgame n).lenR xq) (hbR : List.length bR = (V.tgame n).lenR yq) (hRx : (V.tgame n).lenR xq ≤ 2 ^ L.ℓ) (hLx : (V.tgame n).lenL xq ≤ 2 ^ L.ℓ) (hRy : (V.tgame n).lenR yq ≤ 2 ^ L.ℓ) (hLy : (V.tgame n).lenL yq ≤ 2 ^ L.ℓ) (hD : ((V.tgame n).cons xq yq aR bR).length * (2 ^ L.ℓ + 2 ^ L.ℓ) + (2 ^ L.ℓ + 2 ^ L.ℓ) ≤ 2 ^ L.dm) : (lstar prm V).Accepts n (CL.toBits xq) (CL.toBits yq) (honestA L V n xq yq aR bR) (honestB L V n yq bR)

L* accepts the padded readable answers and the table (claim:properties_of_L*, item 1), when the verifier's programs halt at the two questions and the lengths fit the parameters.

theorem MIPRE.Tailored.AnsRed.length_honestA {L : PcpDims} {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (xq yq : V.Questions n) {aR bR : Cost.BitStr} (haR : List.length aR = (V.tgame n).lenR xq) (hRx : (V.tgame n).lenR xq ≤ 2 ^ L.ℓ) : List.length (honestA L V n xq yq aR bR) = 2 ^ L.ℓ + 2 ^ L.oW

theorem MIPRE.Tailored.AnsRed.length_honestB {L : PcpDims} {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (yq : V.Questions n) {bR : Cost.BitStr} (hbR : List.length bR = (V.tgame n).lenR yq) (hRy : (V.tgame n).lenR yq ≤ 2 ^ L.ℓ) : List.length (honestB L V n yq bR) = 2 ^ L.ℓ

theorem MIPRE.Tailored.AnsRed.identities_honest {F : Type u_1} [Field F] {L : PcpDims} (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) [CharP F 2] (xq yq : V.Questions n) {aR aL bR bL : Cost.BitStr} (hℓ : List.length (prm.toFun n).1 = L.ℓ) (hdm : List.length (prm.toFun n).2 = L.dm) {Cc : SAT.Circuit} {Tt : ℕ} (hWF : Cc.WellFormed) (hin : Cc.inputs = L.nIn) (hm : Cc.inputs + Cc.size = L.m) (hdesc : Cc.DescribesWindows (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r (lstar prm V) n (CL.toBits xq) (CL.toBits yq) Tt) (hT : (lstar prm V).Accepts n (CL.toBits xq) (CL.toBits yq) (honestA L V n xq yq aR bR) (honestB L V n yq bR) → (lstar prm V).AcceptsWithin n (CL.toBits xq) (CL.toBits yq) (honestA L V n xq yq aR bR) (honestB L V n yq bR) Tt) (hTlen : 2 ^ L.ℓ + 2 ^ L.oW ≤ Tt) (hx : V.LenDefined n (CL.toBits xq)) (hy : V.LenDefined n (CL.toBits yq)) (hlp : ∃ (cs : List Cost.BitStr), LpIs V.lp n (CL.toBits xq) (CL.toBits yq) aR bR cs) (haR : List.length aR = (V.tgame n).lenR xq) (haL : List.length aL = (V.tgame n).lenL xq) (hbR : List.length bR = (V.tgame n).lenR yq) (hbL : List.length bL = (V.tgame n).lenL yq) (hRx : (V.tgame n).lenR xq ≤ 2 ^ L.ℓ) (hLx : (V.tgame n).lenL xq ≤ 2 ^ L.ℓ) (hRy : (V.tgame n).lenR yq ≤ 2 ^ L.ℓ) (hLy : (V.tgame n).lenL yq ≤ 2 ^ L.ℓ) (hD : ((V.tgame n).cons xq yq aR bR).length * (2 ^ L.ℓ + 2 ^ L.ℓ) + (2 ^ L.ℓ + 2 ^ L.ℓ) ≤ 2 ^ L.dm) (hacc : (V.tgame n).Accepts xq yq (aR ++ aL) (bR ++ bL)) : Pcp.Identities ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) (induce L ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) (honestR L V n Cc xq yq aR bR) (honestL L V n xq yq aR aL bR bL))

The honest PCP of accepted answers satisfies the thirteen checks identically (cor:functional_viewpoint_final, item 1): when the game accepts the answers at (x, y) and the circuit describes the output indicator through the windows, at parameters the lengths fit and within a time L* meets on the padded strings, the honest PCP of the readable tables honestR (the padded readable answers, the table, witnesses) and the linear tables honestL (Extend of the linear answers) satisfies the checks identically.

The linear tables are linear in the linear answers

theorem MIPRE.Tailored.AnsRed.bitAt_xorBits {a b : Cost.BitStr} (h : List.length a = List.length b) (i : ℕ) : bitAt (LowDegree.BinaryPolynomial.xorBits a b) i = bitAt a i + bitAt b i

theorem MIPRE.Tailored.AnsRed.tbl_xorBits (N : ℕ) {a₁ a₂ b₁ b₂ : Cost.BitStr} (ha : List.length a₁ = List.length a₂) (hb : List.length b₁ = List.length b₂) (v : ℕ) : tbl N (LowDegree.BinaryPolynomial.xorBits a₁ a₂) (LowDegree.BinaryPolynomial.xorBits b₁ b₂) v = tbl N a₁ b₁ v + tbl N a₂ b₂ v

theorem MIPRE.Tailored.AnsRed.honestL_xorBits {L : PcpDims} {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (xq yq : V.Questions n) (aR bR : Cost.BitStr) {aL₁ aL₂ bL₁ bL₂ : Cost.BitStr} (ha : List.length aL₁ = List.length aL₂) (hb : List.length bL₁ = List.length bL₂) : honestL L V n xq yq aR (LowDegree.BinaryPolynomial.xorBits aL₁ aL₂) bR (LowDegree.BinaryPolynomial.xorBits bL₁ bL₂) = honestL L V n xq yq aR aL₁ bR bL₁ + honestL L V n xq yq aR aL₂ bR bL₂

The linear tables are F₂-linear in the linear answers, the readable answers fixed: the table of the linear answers and its extension are additive under the bitwise sum.