Completeness of a presentation from a typed strategy #
hasPerfectZPC_presented takes a perfect PCC strategy of the detyped game. The detyped game of
this repository is CL.Detyping.game, and its perfect PCC strategies come from typed ones by
CL.Detyping.complete: the typed measurement at the question a view decodes to, and the
measurement concentrated on a fixed answer a₀ off the decodable views. Its bit observables
along the encoding are those of the typed measurement at decodable views, and there are none
elsewhere (the detyped tailored game has no answer bits there). So the hypotheses of
hasPerfectZPC_presented reduce to typed ones (hasPerfectZPC_presented_typed).
theorem
MIPRE.Tailored.decodeQuestion_eq_some
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
(E : T → T → Prop)
[DecidableRel E]
{x : CL.Detyping.Coord T ι → ZMod 2}
{w : Bool}
{q : CL.Detyping.Question T ι}
(h : CL.Detyping.decodeQuestion E x = some (w, q))
:
theorem
MIPRE.Tailored.decodeQuestion_eq_none
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
(E : T → T → Prop)
[DecidableRel E]
{x : CL.Detyping.Coord T ι → ZMod 2}
(h : CL.Detyping.decodeQuestion E x = none)
:
theorem
MIPRE.Tailored.hasPerfectZPC_presented_typed
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
(E : T → T → Prop)
[DecidableRel E]
{B ℓ : ℕ}
(hE : ∀ (u v : T), E u v → E v u)
(hne : (CL.Graph.edges E).Nonempty)
(P : Bool → T → CL.CLFun (ZMod 2) ι ℓ)
(hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ)
(hℓ : 0 < ℓ)
(Dt : CL.Detyping.Question T ι → CL.Detyping.Question T ι → Verifier.Answers B → Verifier.Answers B → Bool)
(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))
(R : SyncStrategy (CL.Detyping.typedGame E hne P Dt).doubled)
(hR : R.IsPCC)
(hval : R.value = 1)
(hsupp : ∀ (q : Bool × CL.Detyping.Question T ι) (a : Verifier.Answers B), ¬okT q.2 a → R.P.M q a = 0)
(hperm :
∀ (q : Bool × CL.Detyping.Question T ι) (i : ℕ),
IsSignedPerm (pvmObs (R.P.M q) fun (a : Verifier.Answers B) => bitSign (List.getD (encT q.2 a) i false)))
(hdiag :
∀ (q : Bool × CL.Detyping.Question T ι),
∀ i < D.lenR q.2.1,
(pvmObs (R.P.M q) fun (a : Verifier.Answers B) => bitSign (List.getD (encT q.2 a) i false)).IsDiag)
:
(presented E (CL.Detyping.game E P Dt) D).doubled.HasPerfectZPC
Completeness of the presentation from a typed strategy.