Detyping tailored games

The repository's verifiers are typed and then detyped (MIPRE.CL.Detyping): a question is a graph view followed by a content register, and the detyped predicate calls the typed one on the views of an edge, and accepts otherwise (Detyping.accepts). This file does the same for tailored games. Typed tailored data (TypedData) fixes the numbers of readable and linear variables of each type and the constraints at each pair of typed questions; the detyped tailored game (TypedData.detype) has, at a question, the lengths of the type its graph view decodes to (none when it decodes to nothing) and, at a pair of questions, the typed constraints on the views of an edge and no constraint otherwise.

The two transport lemmas reduce the obligations of MIPRE.Tailored.valStar_le_of_dec and MIPRE.Tailored.hasPerfectZPC_of_sync, for a detyped game presented by a detyped tailored game, to the typed questions of the edges: detype_accepts_of (a pair the tailored game accepts on an edge is a pair the typed constraints accept) and detype_accepts (conversely).

noncomputable def MIPRE.Tailored.typeOf {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (x : CL.Detyping.Coord T ι → ZMod 2) : Option T

The type a detyped question's graph view decodes to, for either player.

Equations

• MIPRE.Tailored.typeOf E x = Option.map Prod.snd (MIPRE.CL.Detyping.decodeView E (MIPRE.CL.pull Function.Embedding.inl x))

noncomputable def MIPRE.Tailored.edgeOf {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (x y : CL.Detyping.Coord T ι → ZMod 2) : Option (CL.Detyping.Question T ι × CL.Detyping.Question T ι)

The edge a pair of detyped questions sits on, Alice's view first: the typed pair.

Equations

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

theorem MIPRE.Tailored.accepts_eq_edgeOf {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] {A : Type u_3} {B : Type u_4} (D : CL.Detyping.Question T ι → CL.Detyping.Question T ι → A → B → Bool) (x y : CL.Detyping.Coord T ι → ZMod 2) (a : A) (b : B) : CL.Detyping.accepts E D x y a b = match edgeOf E x y with | some (u, v) => D u v a b | none => true

The detyped predicate of MIPRE.CL.Detyping calls the typed one on edgeOf, and accepts off it.

structure MIPRE.Tailored.TypedData (T : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

Typed tailored data: the numbers of readable and linear variables of each type and the controlled linear constraints at each pair of typed questions.

• lenR : T → ℕ
• lenL : T → ℕ
• cons : CL.Detyping.Question T ι → CL.Detyping.Question T ι → Cost.BitStr → Cost.BitStr → List Cost.BitStr

def MIPRE.Tailored.TypedData.Accepts {T : Type u_1} {ι : Type u_2} (D : TypedData T ι) (x y : CL.Detyping.Question T ι) (a b : Cost.BitStr) : Prop

The typed acceptance: both answers have their type's lengths, and every constraint holds.

Equations

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

noncomputable def MIPRE.Tailored.TypedData.detype {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] (D : TypedData T ι) (μ : (CL.Detyping.Coord T ι → ZMod 2) → (CL.Detyping.Coord T ι → ZMod 2) → ℝ) (hμ : ∀ (x y : CL.Detyping.Coord T ι → ZMod 2), 0 ≤ μ x y) (hμ1 : ∑ x : CL.Detyping.Coord T ι → ZMod 2, ∑ y : CL.Detyping.Coord T ι → ZMod 2, μ x y = 1) : TailoredGame (CL.Detyping.Coord T ι → ZMod 2)

The detyped tailored game, with the question distribution μ of a detyped game.

Equations

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

theorem MIPRE.Tailored.TypedData.typeOf_of_edgeOf {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] {x y : CL.Detyping.Coord T ι → ZMod 2} {u v : CL.Detyping.Question T ι} (h : edgeOf E x y = some (u, v)) : typeOf E x = some u.1 ∧ typeOf E y = some v.1 ∧ u.2 = CL.pull Function.Embedding.inr x ∧ v.2 = CL.pull Function.Embedding.inr y

theorem MIPRE.Tailored.TypedData.detype_len_of_edgeOf {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] (D : TypedData T ι) {μ : (CL.Detyping.Coord T ι → ZMod 2) → (CL.Detyping.Coord T ι → ZMod 2) → ℝ} {hμ : ∀ (x y : CL.Detyping.Coord T ι → ZMod 2), 0 ≤ μ x y} {hμ1 : ∑ x : CL.Detyping.Coord T ι → ZMod 2, ∑ y : CL.Detyping.Coord T ι → ZMod 2, μ x y = 1} {x y : CL.Detyping.Coord T ι → ZMod 2} {u v : CL.Detyping.Question T ι} (h : edgeOf E x y = some (u, v)) : (detype E D μ hμ hμ1).lenR x = D.lenR u.1 ∧ (detype E D μ hμ hμ1).lenL x = D.lenL u.1 ∧ (detype E D μ hμ hμ1).lenR y = D.lenR v.1 ∧ (detype E D μ hμ hμ1).lenL y = D.lenL v.1

theorem MIPRE.Tailored.TypedData.detype_accepts_iff_of_edgeOf {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] (D : TypedData T ι) {μ : (CL.Detyping.Coord T ι → ZMod 2) → (CL.Detyping.Coord T ι → ZMod 2) → ℝ} {hμ : ∀ (x y : CL.Detyping.Coord T ι → ZMod 2), 0 ≤ μ x y} {hμ1 : ∑ x : CL.Detyping.Coord T ι → ZMod 2, ∑ y : CL.Detyping.Coord T ι → ZMod 2, μ x y = 1} {x y : CL.Detyping.Coord T ι → ZMod 2} {u v : CL.Detyping.Question T ι} (h : edgeOf E x y = some (u, v)) (a b : Cost.BitStr) : (detype E D μ hμ hμ1).Accepts x y a b ↔ D.Accepts u v a b

On an edge, the detyped tailored game accepts exactly what the typed data accepts.

theorem MIPRE.Tailored.TypedData.detype_accepts_of_edgeOf_none {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] (D : TypedData T ι) {μ : (CL.Detyping.Coord T ι → ZMod 2) → (CL.Detyping.Coord T ι → ZMod 2) → ℝ} {hμ : ∀ (x y : CL.Detyping.Coord T ι → ZMod 2), 0 ≤ μ x y} {hμ1 : ∑ x : CL.Detyping.Coord T ι → ZMod 2, ∑ y : CL.Detyping.Coord T ι → ZMod 2, μ x y = 1} {x y : CL.Detyping.Coord T ι → ZMod 2} (h : edgeOf E x y = none) (a b : Cost.BitStr) (ha : List.length a = (detype E D μ hμ hμ1).len x) (hb : List.length b = (detype E D μ hμ hμ1).len y) : (detype E D μ hμ hμ1).Accepts x y a b

Off the edges, the detyped tailored game accepts every pair of the right lengths.

The two reductions to typed questions

noncomputable def MIPRE.Tailored.TypedData.decD {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] {A : Type u_3} (decT : CL.Detyping.Question T ι → Cost.BitStr → A) (a₀ : A) (x : CL.Detyping.Coord T ι → ZMod 2) (a : Cost.BitStr) : A

Decode a detyped answer through its question's type, a₀ off the decodable views.

Equations

• MIPRE.Tailored.TypedData.decD E decT a₀ x a = match MIPRE.Tailored.typeOf E x with | some t => decT (t, MIPRE.CL.pull Function.Embedding.inr x) a | none => a₀

noncomputable def MIPRE.Tailored.TypedData.encD {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] {A : Type u_3} (encT : CL.Detyping.Question T ι → A → Cost.BitStr) (x : CL.Detyping.Coord T ι → ZMod 2) (a : A) : Cost.BitStr

Encode a detyped answer through its question's type, [] off the decodable views.

Equations

• MIPRE.Tailored.TypedData.encD E encT x a = match MIPRE.Tailored.typeOf E x with | some t => encT (t, MIPRE.CL.pull Function.Embedding.inr x) a | none => []

theorem MIPRE.Tailored.TypedData.decD_of_edgeOf {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] {A : Type u_3} {decT : CL.Detyping.Question T ι → Cost.BitStr → A} {a₀ : A} {x y : CL.Detyping.Coord T ι → ZMod 2} {u v : CL.Detyping.Question T ι} (h : edgeOf E x y = some (u, v)) (a b : Cost.BitStr) : decD E decT a₀ x a = decT u a ∧ decD E decT a₀ y b = decT v b

theorem MIPRE.Tailored.TypedData.encD_of_edgeOf {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] {A : Type u_3} {encT : CL.Detyping.Question T ι → A → Cost.BitStr} {x y : CL.Detyping.Coord T ι → ZMod 2} {u v : CL.Detyping.Question T ι} (h : edgeOf E x y = some (u, v)) (a b : A) : encD E encT x a = encT u a ∧ encD E encT y b = encT v b

theorem MIPRE.Tailored.TypedData.detype_accepts_dec {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] (D : TypedData T ι) {μ : (CL.Detyping.Coord T ι → ZMod 2) → (CL.Detyping.Coord T ι → ZMod 2) → ℝ} {hμ : ∀ (x y : CL.Detyping.Coord T ι → ZMod 2), 0 ≤ μ x y} {hμ1 : ∑ x : CL.Detyping.Coord T ι → ZMod 2, ∑ y : CL.Detyping.Coord T ι → ZMod 2, μ x y = 1} {A : Type u_3} (Dt : CL.Detyping.Question T ι → CL.Detyping.Question T ι → A → A → Bool) (decT : CL.Detyping.Question T ι → Cost.BitStr → A) (a₀ : A) (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) (x y : CL.Detyping.Coord T ι → ZMod 2) (a b : Cost.BitStr) (hab : (detype E D μ hμ hμ1).Accepts x y a b) : CL.Detyping.accepts E Dt x y (decD E decT a₀ x a) (decD E decT a₀ y b) = true

Soundness, reduced to the edges: if on every edge a pair the typed data accepts decodes to a pair the typed predicate accepts, then every pair the detyped tailored game accepts decodes to a pair the detyped predicate accepts.

theorem MIPRE.Tailored.TypedData.detype_accepts_enc {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] (D : TypedData T ι) {μ : (CL.Detyping.Coord T ι → ZMod 2) → (CL.Detyping.Coord T ι → ZMod 2) → ℝ} {hμ : ∀ (x y : CL.Detyping.Coord T ι → ZMod 2), 0 ≤ μ x y} {hμ1 : ∑ x : CL.Detyping.Coord T ι → ZMod 2, ∑ y : CL.Detyping.Coord T ι → ZMod 2, μ x y = 1} {A : Type u_3} (Dt : CL.Detyping.Question T ι → CL.Detyping.Question T ι → A → A → Bool) (encT : CL.Detyping.Question T ι → A → Cost.BitStr) (okT : CL.Detyping.Question T ι → A → Prop) (hlen : ∀ (u : CL.Detyping.Question T ι) (a : A), 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 : A), 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)) (x y : CL.Detyping.Coord T ι → ZMod 2) (a b : A) (ha : ∀ (t : T), typeOf E x = some t → okT (t, CL.pull Function.Embedding.inr x) a) (hb : ∀ (t : T), typeOf E y = some t → okT (t, CL.pull Function.Embedding.inr y) b) (hab : CL.Detyping.accepts E Dt x y a b = true) : (detype E D μ hμ hμ1).Accepts x y (encD E encT x a) (encD E encT y b)

Completeness, reduced to the edges: if the typed encodings have the typed lengths, and on every edge an accepted pair of encodable answers encodes to a pair the typed data accepts, then every accepted pair of encodable detyped answers encodes to a pair the detyped tailored game accepts. Off the decodable views the only encodable answer encodes to [].