The typed oracularized game

Piece O2 of planning/oracularization.md (issue #189): the game of the paper's typed oracularized verifier (sec:orac-def) at one index, in the vocabulary the detyping compiler consumes (MIPRE.CL.Detyping.typedGame), and its two value transfers to the input verifier.

• The typed sampler's distribution. Types are the three roles, on the complete type graph with loops (roleGraph); the CL functions are the identity for the oracle and the input sampler's two functions for the isolated players (roleFamily, with CL.CLFun.ident the identity as an (ℓ + 1)-level function). The typed game samples an ordered pair of roles and one common seed, and its distribution is exactly that of SeededGame.oracular (typedGame_mu).
• Soundness. For any typed predicate whose acceptance implies the oracularized predicate after a question-dependent reading of the answers (quantumValue_typedGame_le), val* of the typed game is at most val* of the oracularization, so by lem:oracular-soundness-tensor it bounds the input verifier's value (valStar_ge_of_typed).
• Completeness. For any typed predicate that accepts the honest encodings of accepted answer pairs, a value-1 PCC strategy of 𝒱_n gives one of the doubled typed game (exists_typed_perfectPCC) --- the form CL.Detyping.DeciderProgram.verifier_hasPerfectPCC takes. It is oracleStrategy (identical operators for the two players), doubled, and pushed forward along the encoding (SyncStrategy.pushTo).
• The bit-string predicate. Answers of the typed verifier are bit strings. An oracle answers the serialization of a pair (pairEnc, read back by pairDec), an isolated player a single string; each is parsed against the cut B according to the role (parseAns), and a failed parse is rejected (oraclePred). This is the predicate of fig:oracle-decider, with the bounded parse that repairs 3 and 4 of rem:oracularization-repairs ask for, and it satisfies both hypotheses (valStar_ge_of_oraclePred, exists_oraclePred_perfectPCC). The typed decider program (piece O4) is to be shown to implement it.

The identity as a CL function

def MIPRE.CL.CLFun.trivialOn {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] (ℓ : ℕ) : CLFun F ι ℓ

The zero function with ℓ levels, every level on the empty register.

Equations

• MIPRE.CL.CLFun.trivialOn 0 = MIPRE.CL.CLFun.zero
• MIPRE.CL.CLFun.trivialOn ℓ.succ = MIPRE.CL.CLFun.cons ∅ 0 fun (x : ι → F) => MIPRE.CL.CLFun.trivialOn ℓ

@[simp]

theorem MIPRE.CL.CLFun.eval_trivialOn {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ : ℕ) (x : ι → F) : (trivialOn ℓ).eval x = 0

theorem MIPRE.CL.CLFun.exactlyOn_trivialOn {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ : ℕ) : (trivialOn ℓ).ExactlyOn ∅

def MIPRE.CL.CLFun.ident {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ : ℕ) : CLFun F ι (ℓ + 1)

The identity, as an (ℓ + 1)-level CL function: the whole space at the first level, trivial levels after it. The oracularized sampler gives it to the oracle, who receives the seed itself.

Equations

• MIPRE.CL.CLFun.ident ℓ = MIPRE.CL.CLFun.cons Finset.univ (MIPRE.CL.RegLinear.id Finset.univ) fun (x : ι → F) => MIPRE.CL.CLFun.trivialOn ℓ

@[simp]

theorem MIPRE.CL.CLFun.eval_ident {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ : ℕ) (x : ι → F) : (ident ℓ).eval x = x

theorem MIPRE.CL.CLFun.exactlyOn_ident {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ : ℕ) : (ident ℓ).ExactlyOn Finset.univ

The typed sampler's CL functions and type graph

def MIPRE.roleFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Player → CL.CLFun CL.𝔽₂ ι (ℓ + 1)) : Role → CL.CLFun CL.𝔽₂ ι (ℓ + 1)

The oracularized sampler's CL functions, one per role and the same for both players: the identity for the oracle, and the input sampler's function of the corresponding original player for an isolated player.

Equations

• MIPRE.roleFamily L MIPRE.Role.oracle = MIPRE.CL.CLFun.ident ℓ
• MIPRE.roleFamily L MIPRE.Role.alice = L MIPRE.Player.alice
• MIPRE.roleFamily L MIPRE.Role.bob = L MIPRE.Player.bob

theorem MIPRE.exactlyOn_roleFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {L : Player → CL.CLFun CL.𝔽₂ ι (ℓ + 1)} (hL : ∀ (w : Player), (L w).ExactlyOn Finset.univ) (r : Role) : (roleFamily L r).ExactlyOn Finset.univ

def MIPRE.roleGraph : Role → Role → Prop

The complete type graph on the three roles, loops included: every ordered pair of roles is sampled.

Equations

• MIPRE.roleGraph x✝¹ x✝ = True

@[instance_reducible]

instance MIPRE.instDecidableRelRoleRoleGraph : DecidableRel roleGraph

Equations

• MIPRE.instDecidableRelRoleRoleGraph x✝¹ x✝ = isTrue trivial

theorem MIPRE.mem_roleGraph_edges (p : Role × Role) : p ∈ CL.Graph.edges roleGraph

theorem MIPRE.roleGraph_nonempty : (CL.Graph.edges roleGraph).Nonempty

theorem MIPRE.roleGraph_symm (u v : Role) : roleGraph u v → roleGraph v u

The seeded game of a CL pair, and the typed game

def MIPRE.SeededGame.ofCL {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_2} (L : Player → CL.CLFun CL.𝔽₂ ι (ℓ + 1)) (D : (ι → CL.𝔽₂) → (ι → CL.𝔽₂) → A → A → Bool) : SeededGame (ι → CL.𝔽₂) A

The seeded game presented by a pair of CL functions and a decision predicate: the game of a normal form verifier at one index, with the seed space its question space.

Equations

• MIPRE.SeededGame.ofCL L D = { LA := (L MIPRE.Player.alice).eval, LB := (L MIPRE.Player.bob).eval, D := D }

theorem MIPRE.SeededGame.roleFamily_question {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_2} (L : Player → CL.CLFun CL.𝔽₂ ι (ℓ + 1)) (D : (ι → CL.𝔽₂) → (ι → CL.𝔽₂) → A → A → Bool) (r : Role) (z : ι → CL.𝔽₂) : (r, (roleFamily L r).eval z) = (ofCL L D).oquestion r z

The role family's question is the oracularized game's.

def MIPRE.SeededGame.typedSeedEquiv {ι : Type u_1} : CL.Detyping.TypedSeed roleGraph ι ≃ Role × Role × (ι → ZMod 2)

The typed seeds of the complete graph are the ordered pairs of roles with a seed.

Equations

• MIPRE.SeededGame.typedSeedEquiv = ((Equiv.subtypeUnivEquiv MIPRE.mem_roleGraph_edges).prodCongr (Equiv.refl (ι → ZMod 2))).trans (Equiv.prodAssoc MIPRE.Role MIPRE.Role (ι → ZMod 2))

@[simp]

theorem MIPRE.SeededGame.typedSeedEquiv_apply {ι : Type u_1} (s : CL.Detyping.TypedSeed roleGraph ι) : typedSeedEquiv s = ((↑s.1).1, (↑s.1).2, s.2)

theorem MIPRE.SeededGame.typedGame_mu {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_2} (L : Player → CL.CLFun CL.𝔽₂ ι (ℓ + 1)) (D : (ι → CL.𝔽₂) → (ι → CL.𝔽₂) → A → A → Bool) {A' : Type u_3} [Fintype A'] (D' : CL.Detyping.Question Role ι → CL.Detyping.Question Role ι → A' → A' → Bool) (p q : Role × (ι → CL.𝔽₂)) : (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily L) D').μ p q = (ofCL L D).oDist p q

The typed game has the oracularization's distribution: a uniform ordered pair of roles and one common uniform seed, the oracle receiving the seed and an isolated player its original question.

theorem MIPRE.SeededGame.quantumValue_typedGame_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_2} [Fintype A] [DecidableEq A] (L : Player → CL.CLFun CL.𝔽₂ ι (ℓ + 1)) (D : (ι → CL.𝔽₂) → (ι → CL.𝔽₂) → A → A → Bool) {A' : Type u_3} [Fintype A'] (D' : CL.Detyping.Question Role ι → CL.Detyping.Question Role ι → A' → A' → Bool) (rA : CL.Detyping.Question Role ι → A' → OAns A) (hD : ∀ (p q : CL.Detyping.Question Role ι) (a b : A'), D' p q a b = true → (ofCL L D).oaccepts p q (rA p a) (rA q b) = true) : quantumValue (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily L) D') ≤ quantumValue (ofCL L D).oracular.toGame

Soundness through a reading of the answers. A typed predicate whose acceptance implies the oracularized predicate, after the answers are read by a map that may depend on the question, has no larger quantum value than the oracularization: a strategy is played through the reading, on the same state, and the two games have the same distribution.

Pushing a synchronous strategy into another game

noncomputable def MIPRE.SyncStrategy.pushTo {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) {A' : Type u_3} [Fintype A'] [DecidableEq A'] (G' : SynchronousGame X A') (f : A → A') : SyncStrategy G'

Play a synchronous strategy on another game with the same questions, its outcomes pushed forward along f: the operator for a' is the sum over the fibre above it.

Equations

• S.pushTo G' f = { d := S.d, d_pos := ⋯, P := S.push f }

theorem MIPRE.SyncStrategy.value_le_pushTo {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) {A' : Type u_3} [Fintype A'] [DecidableEq A'] (G' : SynchronousGame X A') (f : A → A') (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) (hD : ∀ (x y : X) (a b : A), G.D x y a b = true → G'.D x y (f a) (f b) = true) : S.value ≤ (S.pushTo G' f).value

Pushing forward loses no value when every accepted tuple stays accepted and the distribution is the same.

theorem MIPRE.SyncStrategy.isPCC_pushTo {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} {S : SyncStrategy G} (hS : S.IsPCC) {A' : Type u_3} [Fintype A'] [DecidableEq A'] (G' : SynchronousGame X A') (f : A → A') (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) : (S.pushTo G' f).IsPCC

Pushing forward keeps the PCC property: sums over fibres of pairwise commuting operators commute.

The two transfers, at a normal form verifier

@[instance_reducible]

instance MIPRE.Verifier.instInhabitedAnswers (T : ℕ) : Inhabited (Answers T)

Equations

• MIPRE.Verifier.instInhabitedAnswers T = { default := ⟨[], ⋯⟩ }

@[reducible, inline]

noncomputable abbrev MIPRE.Verifier.seeded {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B : ℕ) : SeededGame (V.Questions n) (Answers B)

𝒱_n with answers of length at most B, as a seeded game: the seed space is the question space, and the seed's two images are the questions.

Equations

• V.seeded n B = MIPRE.SeededGame.ofCL (V.sampler.cl n) (V.game n B).D

theorem MIPRE.Verifier.seeded_toGame {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B : ℕ) : (V.seeded n B).toGame = V.game n B

theorem MIPRE.Verifier.valStar_ge_of_typed {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B : ℕ) {A' : Type u_1} [Fintype A'] (D' : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → CL.Detyping.Question Role (Fin (V.sampler.dim n)) → A' → A' → Bool) (rA : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → A' → OAns (Answers B)) (hD : ∀ (p q : CL.Detyping.Question Role (Fin (V.sampler.dim n))) (a b : A'), D' p q a b = true → (V.seeded n B).oaccepts p q (rA p a) (rA q b) = true) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < quantumValue (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily (V.sampler.cl n)) D')) : 1 - 24 * √ε ≤ V.valStar n B

Soundness of the typed oracularized game. For a typed predicate whose acceptance implies the oracularized predicate after a reading of the answers, val* of the typed game above 1 - ε puts val* (𝒱_n) at least 1 - 24√ε.

theorem MIPRE.Verifier.exists_typed_perfectPCC {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B : ℕ) (hV : V.HasPerfectPCC n B) {A' : Type u_1} [Fintype A'] [DecidableEq A'] (D' : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → CL.Detyping.Question Role (Fin (V.sampler.dim n)) → A' → A' → Bool) (f : OAns (Answers B) → A') (hf : ∀ (p q : Role × V.Questions n) (u v : OAns (Answers B)), (V.seeded n B).oaccepts p q u v = true → D' p q (f u) (f v) = true) : ∃ (R : SyncStrategy (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily (V.sampler.cl n)) D').doubled), R.IsPCC ∧ R.value = 1

Completeness of the typed oracularized game. For a typed predicate that accepts the encodings of every answer pair the oracularized predicate accepts, a value-1 PCC strategy of 𝒱_n gives one of the doubled typed game: oracleStrategy, with identical measurement operators for the two players, doubled and pushed forward along the encoding.

The bit-string predicate

def MIPRE.pairEnc (a b : Cost.BitStr) : Cost.BitStr

The serialization of an oracle's pair of answers: the postorder bits of the encoded pair (Cost.Data.toBitsPost), the format the repeated decider already parses.

Equations

• MIPRE.pairEnc a b = (MIPRE.Cost.encode (a, b)).toBitsPost

def MIPRE.pairDec (s : Cost.BitStr) : Option (Cost.BitStr × Cost.BitStr)

Reading a pair back from its serialization.

Equations

• MIPRE.pairDec s = MIPRE.Cost.decode (MIPRE.Cost.Data.parse s)

@[simp]

theorem MIPRE.pairDec_pairEnc (a b : Cost.BitStr) : pairDec (pairEnc a b) = some (a, b)

theorem MIPRE.length_pairEnc_le (a b : Cost.BitStr) : List.length (pairEnc a b) ≤ 4 * (List.length a + List.length b) + 3

def MIPRE.parseAns (B : ℕ) : Role → Cost.BitStr → Option (OAns (Verifier.Answers B))

The bounded parse, by the role of the player who answered: an oracle's answer must be the serialization of a pair of answers of length at most B, an isolated player's a single answer of length at most B. Anything else fails to parse, and the predicate rejects it: the paper's grouping of failed parses into one rejected outcome (repair 3), and its truncation to the cut (repair 4) made explicit.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.parseAns B MIPRE.Role.alice x✝ = if h : List.length x✝ ≤ B then some (MIPRE.OAns.single ⟨x✝, h⟩) else none
• MIPRE.parseAns B MIPRE.Role.bob x✝ = if h : List.length x✝ ≤ B then some (MIPRE.OAns.single ⟨x✝, h⟩) else none

def MIPRE.oraclePred {V : Type u_1} {B : ℕ} (S : SeededGame V (Verifier.Answers B)) (p q : Role × V) (a b : Cost.BitStr) : Bool

The typed oracularized predicate on bit-string answers (fig:oracle-decider): both answers are parsed by role, a failed parse is rejected, and otherwise the decision is the oracularized game's.

Equations

• MIPRE.oraclePred S p q a b = match MIPRE.parseAns B p.1 a, MIPRE.parseAns B q.1 b with | some u, some v => S.oaccepts p q u v | x, x_1 => false

def MIPRE.encAns {B : ℕ} : OAns (Verifier.Answers B) → Cost.BitStr

The honest encoding of an oracularized answer: an oracle's pair serialized, an isolated player's answer as it is.

Equations

• MIPRE.encAns (MIPRE.OAns.pair a b) = MIPRE.pairEnc ↑a ↑b
• MIPRE.encAns (MIPRE.OAns.single a) = ↑a

theorem MIPRE.length_encAns_le {B : ℕ} (u : OAns (Verifier.Answers B)) : List.length (encAns u) ≤ 8 * B + 3

theorem MIPRE.parseAns_encAns {B : ℕ} {r : Role} {u : OAns (Verifier.Answers B)} (h : SeededGame.shapeOk r u = true) : parseAns B r (encAns u) = some u

An answer of the right shape parses back from its honest encoding.

theorem MIPRE.oaccepts_of_oraclePred {V : Type u_1} {B : ℕ} {S : SeededGame V (Verifier.Answers B)} {p q : Role × V} {a b : Cost.BitStr} (h : oraclePred S p q a b = true) : S.oaccepts p q ((parseAns B p.1 a).getD default) ((parseAns B q.1 b).getD default) = true

Acceptance of the bit-string predicate is acceptance of the oracularized one, after the answers are read by the bounded parse.

theorem MIPRE.oraclePred_encAns {V : Type u_1} {B : ℕ} {S : SeededGame V (Verifier.Answers B)} {p q : Role × V} {u v : OAns (Verifier.Answers B)} (h : S.oaccepts p q u v = true) : oraclePred S p q (encAns u) (encAns v) = true

The bit-string predicate accepts the honest encodings of every answer pair the oracularized predicate accepts.

@[reducible, inline]

noncomputable abbrev MIPRE.Verifier.oracleTypedPred {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B T : ℕ) : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → CL.Detyping.Question Role (Fin (V.sampler.dim n)) → Answers T → Answers T → Bool

The typed oracularized predicate of 𝒱_n, with parse cut B, on answers of length at most T.

Equations

• V.oracleTypedPred n B T p q a b = MIPRE.oraclePred (V.seeded n B) p q ↑a ↑b

theorem MIPRE.Verifier.valStar_ge_of_oraclePred {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B T : ℕ) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < quantumValue (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily (V.sampler.cl n)) (V.oracleTypedPred n B T))) : 1 - 24 * √ε ≤ V.valStar n B

Soundness of the typed oracularized game of 𝒱_n: its quantum value above 1 - ε, at any output cut, puts val* (𝒱_n) at the parse cut B at least 1 - 24√ε.

theorem MIPRE.Verifier.exists_oraclePred_perfectPCC {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n B T : ℕ) (hT : 8 * B + 3 ≤ T) (hV : V.HasPerfectPCC n B) : ∃ (R : SyncStrategy (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily (V.sampler.cl n)) (V.oracleTypedPred n B T)).doubled), R.IsPCC ∧ R.value = 1

Completeness of the typed oracularized game of 𝒱_n: a value-1 PCC strategy of 𝒱_n at the parse cut B gives one of the doubled typed game, at any output cut T ≥ 8B + 3, which holds every honest encoding.