Soundness of the tailored presentation of the introspection verifier

The typed tailored data of the introspection verifier at its canonical parameters (tdata), and the soundness half of the presentation: on every edge, a pair of answers it accepts decodes (decT, through the kernel's parsed answers) to a pair the typed predicate of the reference verifier accepts (tdata_sound). The constraints say that the readable conditions hold and the kernel's semantic check accepts (Typed.consL_iff); the kernel's completeness (DecisionKernel.program_complete) turns that into acceptance by the kernel program on the re-encoded answers, which is the typed predicate (raw_accepts_iff). Then valStar_presented_le bounds the value of the detyped tailored game by that of the reference verifier's detyped game (valStar_tpresented_le).

noncomputable def MIPRE.Tailored.Intro.Sound.tdata (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (T : TailoredVerifier 7) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)) : TypedData Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))

The typed tailored data of the introspection verifier at its canonical parameters.

Equations

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

noncomputable def MIPRE.Tailored.Intro.Sound.decT (c : ℕ) (hc2 : 2 ≤ c) (lam n : ℕ) (T : TailoredVerifier 7) (V : Verifier 7) (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))) (tb : Cost.BitStr) : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)

The decoding of a typed tailored answer: the kernel's parsed answer read off the layout, re-encoded as the kernel's bytes.

Equations

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

theorem MIPRE.Tailored.Intro.Sound.lenR_le_len (k j R : ℕ) (t : Introspection.DecisionKernel.Label) : Typed.lenR k j R t ≤ Typed.len k j R t

theorem MIPRE.Tailored.Intro.Sound.guards_of_readOK (n : ℕ) {k : ℕ} {hk : 1 ≤ k} [NeZero k] {j R : ℕ} {T : TailoredVerifier 7} {V : Verifier 7} {hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k} {u : Introspection.DecisionKernel.Label} {a : Cost.BitStr} (ha : List.length a = Typed.len k j R u) (h : Typed.readOK k j R T V hs u a) : Introspection.PrefixGuard.holds (Introspection.AuxiliaryDecision.padded V hs) u (Typed.parsedT k hk j R T V hs u a) ∧ Introspection.AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) u (Introspection.DecisionKernel.Answer.toRaw (SAT.shoupBinField k hk) (Typed.parsedT k hk j R T V hs u a))

The readable conditions give the kernel's prefix guard and source-output condition.

theorem MIPRE.Tailored.Intro.Sound.pauliFormatted_parsedT (n : ℕ) {k : ℕ} {hk : 1 ≤ k} [NeZero k] {hodd : Odd k} {j R : ℕ} {T : TailoredVerifier 7} {V : Verifier 7} {hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k} (u : Introspection.DecisionKernel.Label) (x a : Cost.BitStr) : Introspection.DecisionKernel.Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) R u x (Typed.parsedT k hk j R T V hs u a)

The Pauli answers read off the layout are formatted.

theorem MIPRE.Tailored.Intro.Sound.tdata_sound {c : ℕ} {hc : 1 ≤ c} {hc2 : 2 ≤ c} {he : Even c} {lam n : ℕ} {T : TailoredVerifier 7} {V : Verifier 7} {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)} (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))) (ta tb : Cost.BitStr) (h : (tdata c hc he lam n T V hs kg).Accepts u v ta tb) : Introspection.DecisionCompiler.rawPredicate c hc he U (V.sampler.prog, V.decider.prog) lam n u v (decT c hc2 lam n T V hs u ta) (decT c hc2 lam n T V hs v tb) = true

Soundness on the edges: a pair of answers the typed tailored data accepts decodes to a pair the reference verifier's typed predicate accepts.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.Sound.H (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (U : Cost.ClockedUniversalMachine) (V : Verifier 7) : Game (CL.Detyping.Coord (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c hc he lam).dim n)) → ZMod 2) (CL.Detyping.Coord (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c hc he lam).dim n)) → ZMod 2) (Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) (Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n))

The reference verifier's detyped game at index n.

Equations

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

theorem MIPRE.Tailored.Intro.Sound.valStar_tpresented_le {c : ℕ} {hc : 1 ≤ c} (hc2 : 2 ≤ c) {he : Even c} {lam n : ℕ} {T : TailoredVerifier 7} {V : Verifier 7} {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)} (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) : (presented Introspection.DecisionCompiler.graph (H c hc he lam n U V) (tdata c hc he lam n T V hs kg)).valStar ≤ quantumValue (H c hc he lam n U V)

Soundness of the presentation: the detyped tailored game has val* at most the quantum value of the reference verifier's detyped game.