Presenting a detyped game by a detyped tailored game

The two transports of MIPRE.Tailored.Intro.Transport and the two reductions to the edges of MIPRE.Tailored.Detyping, put together: for a game H on detyped questions whose predicate calls a typed predicate Dt on the edges and accepts off them (the shape of every verifier this repository detypes, CL.Detyping.accepts), and typed tailored data D,

• valStar_presented_le: if on every edge a pair the typed data accepts decodes to one Dt accepts, then val* of the detyped tailored game is at most that of H;
• hasPerfectZPC_presented: if on every edge an accepted pair of encodable answers encodes to one the typed data accepts, with the typed lengths, then a perfect PCC strategy of H charging only encodable answers, whose bit observables along the encoding are signed permutations diagonal at the readable bits, gives a perfect permutation strategy of the detyped tailored game.

def MIPRE.Tailored.vecOf (n : ℕ) (l : Cost.BitStr) : Fin n → Bool

A list as a vector of a given length, padded with false.

Equations

• MIPRE.Tailored.vecOf n l i = List.getD l (↑i) false

theorem MIPRE.Tailored.ofFn_vecOf {n : ℕ} {l : Cost.BitStr} (h : List.length l = n) : List.ofFn (vecOf n l) = l

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.presented {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] {B : ℕ} (H : Game (CL.Detyping.Coord T ι → ZMod 2) (CL.Detyping.Coord T ι → ZMod 2) (Verifier.Answers B) (Verifier.Answers B)) (D : TypedData T ι) : TailoredGame (CL.Detyping.Coord T ι → ZMod 2)

The detyped tailored game, on the question distribution of H.

Equations

• MIPRE.Tailored.presented E H D = MIPRE.Tailored.TypedData.detype E D H.μ ⋯ ⋯

theorem MIPRE.Tailored.valStar_presented_le {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] {B : ℕ} (H : Game (CL.Detyping.Coord T ι → ZMod 2) (CL.Detyping.Coord T ι → ZMod 2) (Verifier.Answers B) (Verifier.Answers B)) (Dt : CL.Detyping.Question T ι → CL.Detyping.Question T ι → Verifier.Answers B → Verifier.Answers B → Bool) (hH : ∀ (x y : CL.Detyping.Coord T ι → ZMod 2) (a b : Verifier.Answers B), H.D x y a b = CL.Detyping.accepts E Dt x y a b) (D : TypedData T ι) (decT : CL.Detyping.Question T ι → Cost.BitStr → Verifier.Answers B) (a₀ : Verifier.Answers B) (h : ∀ (u v : CL.Detyping.Question T ι) (a b : Cost.BitStr), E u.1 v.1 → D.Accepts u v a b → Dt u v (decT u a) (decT v b) = true) : (presented E H D).valStar ≤ quantumValue H

Soundness of the presentation.

def MIPRE.Tailored.okD {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] {B : ℕ} (okT : CL.Detyping.Question T ι → Verifier.Answers B → Prop) (a₀ : Verifier.Answers B) (x : CL.Detyping.Coord T ι → ZMod 2) (a : Verifier.Answers B) : Prop

The encodable answers at a detyped question: the typed ones at a decodable view, and a₀ elsewhere.

Equations

• MIPRE.Tailored.okD E okT a₀ x a = ((∀ (t : T), MIPRE.Tailored.typeOf E x = some t → okT (t, MIPRE.CL.pull Function.Embedding.inr x) a) ∧ (MIPRE.Tailored.typeOf E x = none → a = a₀))

noncomputable def MIPRE.Tailored.encV {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] {B : ℕ} (H : Game (CL.Detyping.Coord T ι → ZMod 2) (CL.Detyping.Coord T ι → ZMod 2) (Verifier.Answers B) (Verifier.Answers B)) (D : TypedData T ι) (encT : CL.Detyping.Question T ι → Verifier.Answers B → Cost.BitStr) (x : CL.Detyping.Coord T ι → ZMod 2) (a : Verifier.Answers B) : Fin ((presented E H D).len x) → Bool

The encoding at a detyped question, as a vector of the question's length.

Equations

• MIPRE.Tailored.encV E H D encT x a = MIPRE.Tailored.vecOf ((MIPRE.Tailored.presented E H D).len x) (MIPRE.Tailored.TypedData.encD E encT x a)

theorem MIPRE.Tailored.length_encD_of_okD {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] {B : ℕ} (H : Game (CL.Detyping.Coord T ι → ZMod 2) (CL.Detyping.Coord T ι → ZMod 2) (Verifier.Answers B) (Verifier.Answers B)) (D : TypedData T ι) {encT : CL.Detyping.Question T ι → Verifier.Answers B → Cost.BitStr} {okT : CL.Detyping.Question T ι → Verifier.Answers B → Prop} (a₀ : Verifier.Answers B) (hlen : ∀ (u : CL.Detyping.Question T ι) (a : Verifier.Answers B), okT u a → List.length (encT u a) = D.lenR u.1 + D.lenL u.1) {x : CL.Detyping.Coord T ι → ZMod 2} {a : Verifier.Answers B} (ha : okD E okT a₀ x a) : List.length (TypedData.encD E encT x a) = (presented E H D).len x

theorem MIPRE.Tailored.hasPerfectZPC_presented {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] {B : ℕ} (H : Game (CL.Detyping.Coord T ι → ZMod 2) (CL.Detyping.Coord T ι → ZMod 2) (Verifier.Answers B) (Verifier.Answers B)) (Dt : CL.Detyping.Question T ι → CL.Detyping.Question T ι → Verifier.Answers B → Verifier.Answers B → Bool) (hH : ∀ (x y : CL.Detyping.Coord T ι → ZMod 2) (a b : Verifier.Answers B), H.D x y a b = CL.Detyping.accepts E Dt x y a b) (D : TypedData T ι) {encT : CL.Detyping.Question T ι → Verifier.Answers B → Cost.BitStr} {okT : CL.Detyping.Question T ι → Verifier.Answers B → Prop} (a₀ : Verifier.Answers B) (hlen : ∀ (u : CL.Detyping.Question T ι) (a : Verifier.Answers B), okT u a → List.length (encT u a) = D.lenR u.1 + D.lenL u.1) (h : ∀ (u v : CL.Detyping.Question T ι) (a b : Verifier.Answers B), E u.1 v.1 → okT u a → okT v b → Dt u v a b = true → D.Accepts u v (encT u a) (encT v b)) (S : SyncStrategy H.doubled) (hS : S.IsPCC) (hval : S.value = 1) (hsupp : ∀ (p : Bool × (CL.Detyping.Coord T ι → ZMod 2)) (a : Verifier.Answers B), ¬okD E okT a₀ p.2 a → S.P.M p a = 0) (hperm : ∀ (p : Bool × (CL.Detyping.Coord T ι → ZMod 2)) (i : Fin ((presented E H D).len p.2)), IsSignedPerm (encObs (S.P.M p) (encV E H D encT p.2) i)) (hdiag : ∀ (p : Bool × (CL.Detyping.Coord T ι → ZMod 2)) (i : Fin ((presented E H D).len p.2)), ↑i < (presented E H D).lenR p.2 → (encObs (S.P.M p) (encV E H D encT p.2) i).IsDiag) : (presented E H D).doubled.HasPerfectZPC

Completeness of the presentation.