WP Adequacy

WPAdequate m ps provides a soundness bridge: if wp x proves a postcondition P, then x is Internal.Ensures-witnessed at P. Combined with Internal.MayReturn x a, this yields P a for any value a that x may classically return.

class Std.Do.WPAdequate (m : Type u → Type v) (ps : outParam PostShape) [Monad m] [WP m ps] : Prop

A small adequacy principle: a wp-provable postcondition is Internal.Ensures-witnessed.

• ensures_of_wp {α : Type u} {x : m α} {P : α → Prop} : (⊢ₛ wp⟦x⟧ (PostCond.mayThrow fun (a : α) => ⌜P a⌝)) → Internal.Ensures P x

  A wp-provable postcondition refines x via Internal.Ensures.

instance Std.Do.instWPAdequateIdPure : WPAdequate Id PostShape.pure

instance Std.Do.instWPAdequateReaderTArg {m : Type u_1 → Type u_2} {ps : PostShape} {ρ : Type u_1} [Monad m] [WP m ps] [WPAdequate m ps] : WPAdequate (ReaderT ρ m) (PostShape.arg ρ ps)

instance Std.Do.instWPAdequateStateTArgOfLawfulMonad {m : Type u_1 → Type u_2} {ps : PostShape} {σ : Type u_1} [Monad m] [LawfulMonad m] [WP m ps] [WPAdequate m ps] : WPAdequate (StateT σ m) (PostShape.arg σ ps)

instance Std.Do.instWPAdequateExceptTExceptPureOfLawfulMonad {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [LawfulMonad m] [WP m PostShape.pure] [WPAdequate m PostShape.pure] : WPAdequate (ExceptT ε m) (PostShape.except ε PostShape.pure)

instance Std.Do.instWPAdequateOptionTExceptPUnitPureOfLawfulMonad {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [WP m PostShape.pure] [WPAdequate m PostShape.pure] : WPAdequate (OptionT m) (PostShape.except PUnit PostShape.pure)