Completeness of the executable auxiliary predicate

The semantic acceptance relation implies executable acceptance on the attained prefixes and original-answer cutoffs of the honest strategy.

def MIPRE.Introspection.AuxiliaryDecision.answerBound {Q : ℕ} (R : ℕ) : ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr → Prop

The original answer component is bounded independently of register data.

Equations

• MIPRE.Introspection.AuxiliaryDecision.answerBound R (MIPRE.Introspection.ParsedAnswer.pair y a) = (List.length a ≤ R)
• MIPRE.Introspection.AuxiliaryDecision.answerBound R (MIPRE.Introspection.ParsedAnswer.read y yp a) = (List.length a ≤ R)
• MIPRE.Introspection.AuxiliaryDecision.answerBound R x✝ = True

def MIPRE.Introspection.AuxiliaryDecision.sourceOutput {P : Type u_1} {Q : ℕ} (s : ℕ) : QuestionType P 7 → ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr → Prop

Only Introspect endpoints claim a full source output.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.AuxiliaryDecision.sourceOutput s x✝¹ x✝ = True

theorem MIPRE.Introspection.AuxiliaryDecision.valid_bits {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {Q R : ℕ} (t : QuestionType P 7) (a : ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr) (hf : TypedPredicate.fits t a = true) (hb : answerBound R a) : AuxiliaryAnswer.Valid Q R t (AuxiliaryAnswer.bits a)

theorem MIPRE.Introspection.AuxiliaryDecision.sourceOutput_of_attained {n Q : ℕ} (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (y : Fin Q → CL.𝔽₂) (hy : ∃ (x : Fin Q → CL.𝔽₂), (padded V hs w).eval x = y) : SourceCompiler.InSource (V.sampler.dim (2 ^ n)) (CL.toBits y)

Every attained padded output has the required zero suffix.

theorem MIPRE.Introspection.AuxiliaryDecision.directed_cross_complete {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) (x y : Fin Q → CL.𝔽₂) (a b : Cost.BitStr) (ha : List.length a ≤ (2 ^ n) ^ lam) (hb : List.length b ≤ (2 ^ n) ^ lam) (hx : SourceCompiler.InSource (V.sampler.dim (2 ^ n)) (CL.toBits x)) (hy : SourceCompiler.InSource (V.sampler.dim (2 ^ n)) (CL.toBits y)) (h : sourcePredicate V hs x y a b = true) : (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

theorem MIPRE.Introspection.AuxiliaryDecision.directed_complete {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) (hfa : TypedPredicate.fits t a = true) (hfb : TypedPredicate.fits u b = true) (ha : answerBound ((2 ^ n) ^ lam) a) (hb : answerBound ((2 ^ n) ^ lam) b) (hga : PrefixGuard.holds (padded V hs) t a) (hgb : PrefixGuard.holds (padded V hs) u b) (hsa : sourceOutput (V.sampler.dim (2 ^ n)) t a) (hsb : sourceOutput (V.sampler.dim (2 ^ n)) u b) (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 : AuxiliaryQuotient.directed (padded V hs) X Z π (sourcePredicate V hs) t u a b = true) : (directed U X Z project).toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters t u (AuxiliaryAnswer.bits a) (AuxiliaryAnswer.bits b)) = true

Semantic auxiliary comparisons are executable on correctly tagged, bounded answers whose queried prefixes are attained.

theorem MIPRE.Introspection.AuxiliaryDecision.prefixGuard_canonical {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (R : ℕ) (t u : QuestionType P 7) (a : ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr) (b : Cost.BitStr) (hf : TypedPredicate.fits t a = true) : (prefixGuard U).toFun (canonical V lam n Q R parameters t u (AuxiliaryAnswer.bits a) b) = true ↔ PrefixGuard.holds (padded V hs) t a

The executable local scan is exactly the semantic prefix guard.

theorem MIPRE.Introspection.AuxiliaryDecision.guarded_complete {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 : answerBound ((2 ^ n) ^ lam) a) (hb : answerBound ((2 ^ n) ^ lam) b) (hga : PrefixGuard.holds (padded V hs) t a) (hgb : PrefixGuard.holds (padded V hs) u b) (hsa : sourceOutput (V.sampler.dim (2 ^ n)) t a) (hsb : sourceOutput (V.sampler.dim (2 ^ n)) u b) (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)) (h : AuxiliaryQuotient.check (padded V hs) X Z π (sourcePredicate V hs) DP t u a b = true) : (guarded U X Z project).toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters t u (AuxiliaryAnswer.bits a) (AuxiliaryAnswer.bits b)) = true

Both semantic orientations and their local guards pass the complete executable auxiliary kernel on honest, bounded source outputs.