The decision kernel on canonical verifier inputs

The resource tuple supplied by preparation is identified with the canonical bounded-source context used in the auxiliary correctness proofs.

noncomputable def MIPRE.Introspection.DecisionKernel.canonicalInput (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T U : Label) (x y a b : Cost.BitStr) : Input

Canonical prepared input with explicit register parameters.

Equations

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

theorem MIPRE.Introspection.DecisionKernel.canonicalInput_fields (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T U : Label) (x y a b : Cost.BitStr) : leftType.toFun (canonicalInput V lam n Q R p T U x y a b) = T ∧ rightType.toFun (canonicalInput V lam n Q R p T U x y a b) = U ∧ leftBits.toFun (canonicalInput V lam n Q R p T U x y a b) = a ∧ rightBits.toFun (canonicalInput V lam n Q R p T U x y a b) = b

theorem MIPRE.Introspection.DecisionKernel.sourceContext_canonical (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T U : Label) (x y a b : Cost.BitStr) (hab : Q ≤ List.length a + List.length b) : sourceContext.toFun (canonicalInput V lam n Q R p T U x y a b) = SourcePadding.Program.queryContext V lam n false 0 0

theorem MIPRE.Introspection.DecisionKernel.auxiliaryInput_canonical (W : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T U : Label) (x y a b : Cost.BitStr) (hab : Q ≤ List.length a + List.length b) : (auxiliaryInput W).toFun (canonicalInput V lam n Q R p T U x y a b) = AuxiliaryDecision.canonical V lam n Q R p T U a b