Auxiliary decision with both local prefix guards

The guards are applied to all hiding and Read endpoints, including consistency loops. This is the executable counterpart of PrefixGuard.guarded and makes its completeness and soundness transports available to the final verifier.

noncomputable def MIPRE.Introspection.AuxiliaryDecision.prefixGuard {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (Input P 7) Bool

Validate the image condition for the left endpoint's required prefix.

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.guarded {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) : Cost.PolyTimeFun (Input P 7) Bool

The complete auxiliary kernel, including the local image conditions.

Equations

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

theorem MIPRE.Introspection.AuxiliaryDecision.guarded_iff {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) (x : Input P 7) : (guarded U X Z project).toFun x = true ↔ (prefixGuard U).toFun x = true ∧ (prefixGuard U).toFun (swap.toFun x) = true ∧ (check U X Z project).toFun x = true

theorem MIPRE.Introspection.AuxiliaryDecision.check_of_guarded {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) (x : Input P 7) (h : (guarded U X Z project).toFun x = true) : (check U X Z project).toFun x = true

Guarding only removes accepting tuples.