Semantic soundness of the executable auxiliary predicate

Canonical byte answers accepted by the executable checks satisfy the full quotient predicate. The cross edge projects to the original bounded verifier.

noncomputable def MIPRE.Introspection.AuxiliaryDecision.sourcePredicate {n Q : ℕ} (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ Q) (x y : Fin Q → CL.𝔽₂) (a b : Cost.BitStr) : Bool

The source predicate on the padded register uses the original decision program.

Equations

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

theorem MIPRE.Introspection.AuxiliaryDecision.directed_cross_sound {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (x y : Fin Q → CL.𝔽₂) (a b : Cost.BitStr) (h : (directed U X Z project).toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters (Sum.inr (AuxType.introspect, false)) (Sum.inr (AuxType.introspect, true)) (AuxiliaryAnswer.bits (ParsedAnswer.pair x a)) (AuxiliaryAnswer.bits (ParsedAnswer.pair y b))) = true) : sourcePredicate V hs x y a b = true

theorem MIPRE.Introspection.AuxiliaryDecision.directed_sound {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (hQ : 4 ≤ Q) (hR : 3 * (2 ^ n) ^ lam ≤ Q) (π : Cost.BitStr → Fin Q → CL.𝔽₂) (t u : QuestionType P 7) (a b : ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr) (hp : ∀ (p : P) (c : Cost.BitStr), p = X ∨ p = Z → t = Sum.inl p → a = ParsedAnswer.pauli c → project.toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters t u (AuxiliaryAnswer.bits a) (AuxiliaryAnswer.bits b)) = CL.toBits (π c)) (h : (directed U X Z project).toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters t u (AuxiliaryAnswer.bits a) (AuxiliaryAnswer.bits b)) = true) : AuxiliaryQuotient.directed (padded V hs) X Z π (sourcePredicate V hs) t u a b = true

Every executable directed comparison implies its quotient semantics.

theorem MIPRE.Introspection.AuxiliaryDecision.format_canonical {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (V : Verifier 7) (lam n Q R : ℕ) (t u : QuestionType P 7) (a b : Cost.BitStr) : format.toFun (canonical V lam n Q R parameters t u a b) = true ↔ AuxiliaryAnswer.Valid Q R t a

The executable format check is the canonical auxiliary byte format.

theorem MIPRE.Introspection.AuxiliaryDecision.check_sound {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (hQ : 4 ≤ Q) (hR : 3 * (2 ^ n) ^ lam ≤ Q) (π : Cost.BitStr → Fin Q → CL.𝔽₂) (DP : P → P → Cost.BitStr → Cost.BitStr → Bool) (t u : QuestionType P 7) (a b : ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr) (ha : TypedPredicate.fits t a = true) (hb : TypedPredicate.fits u b = true) (hpa : ∀ (p : P) (c : Cost.BitStr), p = X ∨ p = Z → t = Sum.inl p → a = ParsedAnswer.pauli c → project.toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters t u (AuxiliaryAnswer.bits a) (AuxiliaryAnswer.bits b)) = CL.toBits (π c)) (hpb : ∀ (p : P) (c : Cost.BitStr), p = X ∨ p = Z → u = Sum.inl p → b = ParsedAnswer.pauli c → project.toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters u t (AuxiliaryAnswer.bits b) (AuxiliaryAnswer.bits a)) = CL.toBits (π c)) (hDP : ∀ (p q : P) (x y : Cost.BitStr), t = Sum.inl p → u = Sum.inl q → a = ParsedAnswer.pauli x → b = ParsedAnswer.pauli y → DP p q x y = true) (h : (check U X Z project).toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters t u (AuxiliaryAnswer.bits a) (AuxiliaryAnswer.bits b)) = true) : AuxiliaryQuotient.check (padded V hs) X Z π (sourcePredicate V hs) DP t u a b = true

The two executable orientations, formats and consistency together imply the complete quotient predicate. Pauli acceptance is supplied by its parser.

theorem MIPRE.Introspection.AuxiliaryDecision.check_raw_sound {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (hQ : 4 ≤ Q) (hR : 3 * (2 ^ n) ^ lam ≤ Q) (π : Cost.BitStr → Fin Q → CL.𝔽₂) (DP : P → P → Cost.BitStr → Cost.BitStr → Bool) (t u : QuestionType P 7) (a b : Cost.BitStr) (hpa : ∀ (p : P), p = X ∨ p = Z → t = Sum.inl p → project.toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters t u a b) = CL.toBits (π a)) (hpb : ∀ (p : P), p = X ∨ p = Z → u = Sum.inl p → project.toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters u t b a) = CL.toBits (π b)) (hDP : ∀ (p q : P), t = Sum.inl p → u = Sum.inl q → DP p q a b = true) (h : (check U X Z project).toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters t u a b) = true) : AuxiliaryQuotient.check (padded V hs) X Z π (sourcePredicate V hs) DP t u (AuxiliaryAnswer.decode Q t a) (AuxiliaryAnswer.decode Q u b) = true

Soundness for every raw accepted answer, including the canonical parser round trip needed to interpret same-type byte equality.