The typed answer-reduced game

Piece AR-3c of planning/answer-reduction.md, concluded: the game of the typed answer-reduced verifier V̂^ar at one index, in the vocabulary the detyping compiler consumes (MIPRE.CL.Detyping.typedGame), with bit-string answers.

• The types are Role × PcpTy, on the complete type graph with loops (graph), as for the oracularized verifier.
• The CL functions are the binary family cl of MIPRE/Background/AnswerReduction/Family, the same for both players.
• The predicate (typedPred) parses both answers by their types (parse), rejects a failed parse, and otherwise decides by the answer-reduced predicate accepts on the decoded questions (decodeQ: the type, the oracle half, and the PCP half read back over F_q).
• The game check (gameCheck) runs the PCP verifier of a SAT.PcpDecider on the input verifier's question pair, read off the oracle half by the input sampler's two CL functions, and the view (z, α) in the k-bit representation the PCP reads.

accepts_of_typedPred and typedPred_enc are the two directions AR-4 and AR-5 need: acceptance of the bit-string predicate is acceptance of accepts after the parse, and accepts on answers of the right format is acceptance of their honest encodings.

@[reducible, inline]

abbrev MIPRE.AnswerReduction.ArTy : Type

The types of the answer-reduced verifier.

Equations

• MIPRE.AnswerReduction.ArTy = (MIPRE.Role × MIPRE.AnswerReduction.Pcp.PcpTy)

def MIPRE.AnswerReduction.graph : ArTy → ArTy → Prop

The complete type graph on the answer-reduced types, loops included.

Equations

• MIPRE.AnswerReduction.graph x✝¹ x✝ = True

@[instance_reducible]

instance MIPRE.AnswerReduction.instDecidableRelArTyGraph : DecidableRel graph

Equations

• MIPRE.AnswerReduction.instDecidableRelArTyGraph x✝¹ x✝ = isTrue trivial

theorem MIPRE.AnswerReduction.mem_graph_edges (p : ArTy × ArTy) : p ∈ CL.Graph.edges graph

instance MIPRE.AnswerReduction.instNonemptyTy : Nonempty LIDT.CL.Ty

theorem MIPRE.AnswerReduction.graph_nonempty : (CL.Graph.edges graph).Nonempty

@[reducible, inline]

noncomputable abbrev MIPRE.AnswerReduction.fld (P : SAT.PcpParams) (hk : 1 ≤ P.k) : SAT.BinField P.k

The field of the PCP with its k-bit representation.

Equations

• MIPRE.AnswerReduction.fld P hk = MIPRE.SAT.shoupBinField P.k hk

noncomputable def MIPRE.AnswerReduction.decodeQ {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (p : CL.Detyping.Question ArTy (Fin (dim V n P))) : Q P (Fq P hk) (Fin (V.sampler.dim n) → CL.𝔽₂)

A typed question of the answer-reduced verifier, decoded: the type, the oracle half and the PCP half.

Equations

• MIPRE.AnswerReduction.decodeQ V n P hk p = (p.1, MIPRE.AnswerReduction.oraclePart V n P p.2, MIPRE.AnswerReduction.pcpPart V n P hk p.2)

noncomputable def MIPRE.AnswerReduction.gameCheck {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) (PD : SAT.PcpDecider) (D : Cost.Prog) (T Qn σ : ℕ) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (z : Fin P.m' → Fq P hk) (α : Fin (P.m' + 6) → Fq P hk) : Bool

The game check: the PCP verifier of PD, with the input decider D and the parameters (n, T, Q, σ), on the input question pair read off the oracle half and the view (z, α).

Equations

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

noncomputable def MIPRE.AnswerReduction.typedPred {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (p q : CL.Detyping.Question ArTy (Fin (dim V n P))) (a b : Verifier.Answers B) : Bool

The typed answer-reduced predicate on bit-string answers of length at most B.

Equations

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

noncomputable def MIPRE.AnswerReduction.typedGame {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) : Game (CL.Detyping.Question ArTy (Fin (dim V n P))) (CL.Detyping.Question ArTy (Fin (dim V n P))) (Verifier.Answers B) (Verifier.Answers B)

The typed answer-reduced game at index n, with answers of length at most B.

Equations

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

theorem MIPRE.AnswerReduction.accepts_of_typedPred {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) {B : ℕ} {p q : CL.Detyping.Question ArTy (Fin (dim V n P))} {a b : Verifier.Answers B} (h : typedPred V n P hk S S' check B p q a b = true) : ∃ (u : Ans P (fld P hk).carrier) (v : Ans P (fld P hk).carrier), parse (fld P hk) p.1.2 ↑a = some u ∧ parse (fld P hk) q.1.2 ↑b = some v ∧ accepts S S' check (decodeQ V n P hk p) (decodeQ V n P hk q) u v = true

Acceptance of the bit-string predicate is acceptance of accepts after the parse.

theorem MIPRE.AnswerReduction.ansFmt_of_accepts (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') {X : Type u_1} {check' : X → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool} {p q : Q P (Fq P hk) X} {u v : Ans P (Fq P hk)} (h : accepts S S' check' p q u v = true) : ansFmt p.1.2 u = true ∧ ansFmt q.1.2 v = true

theorem MIPRE.AnswerReduction.typedPred_enc {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) {B : ℕ} {p q : CL.Detyping.Question ArTy (Fin (dim V n P))} {u v : Ans P (Fq P hk)} (h : accepts S S' check (decodeQ V n P hk p) (decodeQ V n P hk q) u v = true) (hu : List.length (enc (fld P hk) u) ≤ B) (hv : List.length (enc (fld P hk) v) ≤ B) : typedPred V n P hk S S' check B p q ⟨enc (fld P hk) u, hu⟩ ⟨enc (fld P hk) v, hv⟩ = true

accepts on two answers is acceptance of their honest encodings.