Completeness of the tailored presentation of the introspection verifier, on the edges

The honest answers of the introspection verifier are byte strings in the canonical format of their label (Layout.OkLayout). The tailored presentation encodes them by the padded layout (Layout.enc), and the parsed answer the constraints read off the encoding is the kernel's decoding of the bytes (parsedT_enc). So on every edge, when the kernel accepts two such byte answers whose encodings satisfy the readable conditions, the typed tailored data accepts the two encodings (tdata_complete): the kernel's soundness (DecisionKernel.program_sound) gives its semantic check on the decoded answers, which are the parsed encodings, and Typed.consL_iff turns that into the constraints.

The parsed encoding

theorem MIPRE.Tailored.Intro.Complete.win_left {u v : Cost.BitStr} {m : ℕ} (h : List.length u = m) : win (u ++ v) 0 m = u

theorem MIPRE.Tailored.Intro.Complete.win_right {u v : Cost.BitStr} {o m : ℕ} (h : List.length u = o) : win (u ++ v) o m = List.take m v

theorem MIPRE.Tailored.Intro.Complete.take_pad_le {R : ℕ} {l : Cost.BitStr} {m : ℕ} (hm : List.length l = m) (rest : Cost.BitStr) : List.take m (pad R l ++ rest) = l

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.Complete.encL (k j R : ℕ) {n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k) (u : Introspection.DecisionKernel.Label) (bs : Cost.BitStr) : Cost.BitStr

The layout's encoding at the instance's parameters.

Equations

• MIPRE.Tailored.Intro.Complete.encL k j R T V hs u bs = MIPRE.Tailored.Intro.enc (MIPRE.Tailored.Intro.Typed.Q k j) R (MIPRE.Tailored.Intro.Typed.sR k j T V hs) u bs

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.Complete.OkL (k j R : ℕ) {n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k) (u : Introspection.DecisionKernel.Label) (bs : Cost.BitStr) : Prop

The layout's well-formedness at the instance's parameters.

Equations

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

theorem MIPRE.Tailored.Intro.Complete.parsedT_enc {k : ℕ} {hk : 1 ≤ k} {j R n : ℕ} {T : TailoredVerifier 7} {V : Verifier 7} {hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k} {u : Introspection.DecisionKernel.Label} {bs : Cost.BitStr} (h : OkL k j R T V hs u bs) : Typed.parsedT k hk j R T V hs u (encL k j R T V hs u bs) = Introspection.DecisionKernel.Answer.decode (SAT.shoupBinField k hk) (2 ^ j) (Typed.Q k j) R u bs

The parsed encoding is the kernel's decoding.

theorem MIPRE.Tailored.Intro.Complete.length_encL {k j R n : ℕ} {T : TailoredVerifier 7} {V : Verifier 7} {hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k} {u : Introspection.DecisionKernel.Label} {bs : Cost.BitStr} (h : OkL k j R T V hs u bs) : List.length (encL k j R T V hs u bs) = Typed.len k j R u

Well-formed answers encode to the label's length.

The edges

noncomputable def MIPRE.Tailored.Intro.Complete.encT {n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (c lam : ℕ) (hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (q : CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (a : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)) : Cost.BitStr

The encoding of a byte answer at a typed question.

Equations

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

def MIPRE.Tailored.Intro.Complete.okT {n : ℕ} (T : TailoredVerifier 7) (V : Verifier 7) (c lam : ℕ) (hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (q : CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (a : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)) : Prop

The encodable byte answers at a typed question: well formed, with the readable conditions at their encoding.

Equations

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

theorem MIPRE.Tailored.Intro.Complete.tdata_complete {n : ℕ} {T : TailoredVerifier 7} {V : Verifier 7} {c : ℕ} {hc : 1 ≤ c} (hc2 : 2 ≤ c) {he : Even c} {lam : ℕ} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)} {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n} (hkg : KerGens (Introspection.SourceCompiler.registerBits c lam n) kg) (hacc : Typed.AcceptsAsInput T V n) (U : Cost.ClockedUniversalMachine) (hV : V.IsBounded lam) (hn : 1 ≤ n) (u v : CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (a b : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)) (ha : okT T V c lam hs u a) (hb : okT T V c lam hs v b) (h : Introspection.DecisionCompiler.rawPredicate c hc he U (V.sampler.prog, V.decider.prog) lam n u v a b = true) : (Sound.tdata c hc he lam n T V hs kg).Accepts u v (encT T V c lam hs u a) (encT T V c lam hs v b)

Completeness on the edges: when the reference verifier's typed predicate accepts two encodable byte answers, the typed tailored data accepts their encodings.

theorem MIPRE.Tailored.Intro.Complete.hasPerfectZPC_tpresented {n : ℕ} {T : TailoredVerifier 7} {V : Verifier 7} {c : ℕ} {hc : 1 ≤ c} (hc2 : 2 ≤ c) {he : Even c} {lam : ℕ} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)} {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n} (hkg : KerGens (Introspection.SourceCompiler.registerBits c lam n) kg) (hacc : Typed.AcceptsAsInput T V n) (U : Cost.ClockedUniversalMachine) (hV : V.IsBounded lam) (hn : 1 ≤ n) (R : SyncStrategy (Introspection.DecisionCompiler.rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n).doubled) (hR : R.IsPCC) (hval : R.value = 1) (hsupp : ∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c hc he lam).dim n))) (a : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)), ¬okT T V c lam hs q.2 a → R.P.M q a = 0) (hperm : ∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c hc he lam).dim n))) (i : ℕ), IsSignedPerm (pvmObs (R.P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (encT T V c lam hs q.2 a) i false))) (hdiag : ∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c hc he lam).dim n))), ∀ i < (Sound.tdata c hc he lam n T V hs kg).lenR q.2.1, (pvmObs (R.P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (encT T V c lam hs q.2 a) i false)).IsDiag) : (presented Introspection.DecisionCompiler.graph (Sound.H c hc he lam n U V) (Sound.tdata c hc he lam n T V hs kg)).doubled.HasPerfectZPC

Completeness of the presentation: a perfect PCC strategy of the reference verifier's typed game that charges only encodable answers, whose bit observables along the encoding are signed permutations, diagonal at the readable bits, gives a perfect ZPC strategy of the doubled detyped tailored game.