Semantic prefix guards for executable introspection

A Hide answer at level k must have an attained k-stage prefix. A Read answer must have an attained penultimate prefix. Constructor validity remains the responsibility of the existing typed format check.

def MIPRE.Introspection.PrefixGuard.holds {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) : QuestionType P ℓ → ParsedAnswer (ι → F) A PA → Prop

The local image condition imposed by the executable prefix scan.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.PrefixGuard.holds L x✝¹ x✝ = True

noncomputable def MIPRE.Introspection.PrefixGuard.check {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (t : QuestionType P ℓ) (a : ParsedAnswer (ι → F) A PA) : Bool

Boolean presentation of the local guard; executable scans implement this proposition.

Equations

• MIPRE.Introspection.PrefixGuard.check L t a = decide (MIPRE.Introspection.PrefixGuard.holds L t a)

@[simp]

theorem MIPRE.Introspection.PrefixGuard.check_eq_true {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (t : QuestionType P ℓ) (a : ParsedAnswer (ι → F) A PA) : check L t a = true ↔ holds L t a