WP Soundness

WPSound m ps is the soundness bridge from wp-style reasoning to the operational Internal.Ensures predicate: 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.WPSound (m : Type u → Type v) (ps : outParam PostShape) [Monad m] [WP m ps] : Prop

Soundness of wp: 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.

theorem Std.Do.WPSound.of_wp {m : Type u → Type u_1} {ps : PostShape} [Monad m] [WP m ps] [WPSound m ps] {α : Type u} {x : m α} {a : α} {P : α → Prop} (hmay : Internal.MayReturn x a) (hwp : ⊢ₛ wp⟦x⟧ (PostCond.mayThrow fun (a : α) => ⌜P a⌝)) : P a

From a wp-provable postcondition and an Internal.MayReturn witness, conclude P at that value.

theorem Std.Do.WPSound.of_wp_canReturn {m : Type u → Type u_1} {ps : PostShape} [Monad m] [LawfulMonad m] [WP m ps] [WPSound m ps] [MonadAttach m] [LawfulMonadAttach m] {α : Type u} {x : m α} {a : α} {P : α → Prop} (hcan : MonadAttach.CanReturn x a) (hwp : ⊢ₛ wp⟦x⟧ (PostCond.mayThrow fun (a : α) => ⌜P a⌝)) : P a

From a wp-provable postcondition and a MonadAttach.CanReturn witness, conclude P at that value. Convenient when the monad has a LawfulMonadAttach instance, since CanReturn is typically definitional.

instance Std.Do.instWPSoundIdPure : WPSound Id PostShape.pure

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

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

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

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

instance Std.Do.instWPSoundEStateMExceptArgPure {ε σ : Type u_1} : WPSound (EStateM ε σ) (PostShape.except ε (PostShape.arg σ PostShape.pure))

theorem Std.Do.Id.of_wp_run_eq {α : Type u} {x : α} {prog : Id α} (h : prog.run = x) (P : α → Prop) : (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) => { down := P a })) → P x

Soundness lemma for Id.run. Derived from WPSound.of_wp_canReturn: Id.run prog = x is the MonadAttach.CanReturn prog x witness.

Per-transformer soundness lemmas

For each transformer T, T.ensures_of_wp_run produces an Internal.Ensures over the post-run computation prog.run «args» : m _. T.of_wp_run further collapses this to a pure proposition P a when the base monad m has LawfulMonadAttach and the caller can supply a MonadAttach.CanReturn witness — the natural generalization of the Id-specialized *.of_wp_run_eq family below.

theorem Std.Do.ReaderT.ensures_of_wp_run {m : Type u → Type u_1} {ps : PostShape} [Monad m] [WP m ps] [WPSound m ps] {α ρ : Type u} {prog : ReaderT ρ m α} (r : ρ) (P : α → Prop) (hwp : ⊢ₛ wp⟦prog⟧ (PostCond.mayThrow fun (a : α) => ⌜P a⌝) r) : Internal.Ensures P (prog.run r)

A wp-provable postcondition refines the post-run computation prog.run r : m α via Internal.Ensures.

theorem Std.Do.ReaderT.of_wp_run {m : Type u → Type u_1} {ps : PostShape} [Monad m] [LawfulMonad m] [WP m ps] [WPSound m ps] [MonadAttach m] [LawfulMonadAttach m] {α ρ : Type u} {prog : ReaderT ρ m α} {r : ρ} {a : α} (P : α → Prop) (hcan : MonadAttach.CanReturn (prog.run r) a) (hwp : ⊢ₛ wp⟦prog⟧ (PostCond.mayThrow fun (a : α) => ⌜P a⌝) r) : P a

Pure-proposition soundness: from a MonadAttach.CanReturn witness for prog.run r and a wp-provable postcondition, conclude P a.

theorem Std.Do.ReaderM.of_wp_run_eq {α ρ : Type u} {x : α} {r : ρ} {prog : ReaderM ρ α} (h : ReaderT.run prog r = x) (P : α → Prop) : (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) (x : ρ) => ⌜P a⌝) r) → P x

Soundness lemma for ReaderM.run: Id-specialization of ReaderT.of_wp_run.

theorem Std.Do.StateT.ensures_of_wp_run {m : Type u → Type u_1} {ps : PostShape} [Monad m] [WP m ps] [WPSound m ps] {α σ : Type u} {prog : StateT σ m α} (s : σ) (P : α × σ → Prop) (hwp : ⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) (s' : σ) => ⌜P (a, s')⌝) s) : Internal.Ensures P (prog.run s)

A wp-provable postcondition refines the post-run computation prog.run s : m (α × σ) via Internal.Ensures.

theorem Std.Do.StateT.of_wp_run {m : Type u → Type u_1} {ps : PostShape} [Monad m] [LawfulMonad m] [WP m ps] [WPSound m ps] [MonadAttach m] [LawfulMonadAttach m] {α σ : Type u} {prog : StateT σ m α} {s : σ} {p : α × σ} (P : α × σ → Prop) (hcan : MonadAttach.CanReturn (prog.run s) p) (hwp : ⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) (s' : σ) => ⌜P (a, s')⌝) s) : P p

Pure-proposition soundness for StateT.run, generalizing StateM.of_wp_run_eq.

theorem Std.Do.StateM.of_wp_run_eq {α σ : Type} {x : α × σ} {s : σ} {prog : StateM σ α} (h : StateT.run prog s = x) (P : α × σ → Prop) : (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) (s' : σ) => ⌜P (a, s')⌝) s) → P x

Soundness lemma for StateM.run: Id-specialization of StateT.of_wp_run.

theorem Std.Do.StateM.of_wp_run'_eq {α σ : Type} {x : α} {s : σ} {prog : StateM σ α} (h : StateT.run' prog s = x) (P : α → Prop) : (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) => ⌜P a⌝) s) → P x

Soundness lemma for StateM.run': Id-specialization of StateT.of_wp_run.

theorem Std.Do.ExceptT.ensures_of_wp_run {m : Type u → Type u_1} [Monad m] [LawfulMonad m] [WP m PostShape.pure] [WPSound m PostShape.pure] {ε α : Type u} {prog : ExceptT ε m α} (P : Except ε α → Prop) (hwp : ⊢ₛ wp⟦prog⟧ (fun (a : α) => ⌜P (Except.ok a)⌝, fun (e : ε) => ⌜P (Except.error e)⌝, PUnit.unit)) : Internal.Ensures P prog.run

A wp-provable postcondition with split .ok/.error cases refines the post-run computation prog.run : m (Except ε α) via Internal.Ensures.

theorem Std.Do.ExceptT.of_wp_run {m : Type u → Type u_1} [Monad m] [LawfulMonad m] [WP m PostShape.pure] [WPSound m PostShape.pure] [MonadAttach m] [LawfulMonadAttach m] {ε α : Type u} {prog : ExceptT ε m α} {x : Except ε α} (P : Except ε α → Prop) (hcan : MonadAttach.CanReturn prog.run x) (hwp : ⊢ₛ wp⟦prog⟧ (fun (a : α) => ⌜P (Except.ok a)⌝, fun (e : ε) => ⌜P (Except.error e)⌝, PUnit.unit)) : P x

Pure-proposition soundness for ExceptT.run, generalizing Except.of_wp_eq.

theorem Std.Do.Except.of_wp_eq {ε α : Type} {x prog : Except ε α} (h : prog = x) (P : Except ε α → Prop) : (⊢ₛ wp⟦prog⟧ (fun (a : α) => ⌜P (Except.ok a)⌝, fun (e : ε) => ⌜P (Except.error e)⌝, PUnit.unit)) → P x

Soundness lemma for Except: Id-specialization of ExceptT.of_wp_run.

@[deprecated Std.Do.Except.of_wp_eq (since := "2026-01-26")]

theorem Std.Do.Except.of_wp {ε α : Type} {prog : Except ε α} (P : Except ε α → Prop) : (⊢ₛ wp⟦prog⟧ (fun (a : α) => ⌜P (Except.ok a)⌝, fun (e : ε) => ⌜P (Except.error e)⌝, PUnit.unit)) → P prog

Soundness lemma for Except without the equality hypothesis (deprecated).

theorem Std.Do.OptionT.ensures_of_wp_run {m : Type u → Type u_1} [Monad m] [LawfulMonad m] [WP m PostShape.pure] [WPSound m PostShape.pure] {α : Type u} {prog : OptionT m α} (P : Option α → Prop) (hwp : ⊢ₛ wp⟦prog⟧ (fun (a : α) => ⌜P (some a)⌝, fun (x : PUnit) => ⌜P none⌝, PUnit.unit)) : Internal.Ensures P prog.run

A wp-provable postcondition with split some/none cases refines the post-run computation prog.run : m (Option α) via Internal.Ensures.

theorem Std.Do.OptionT.of_wp_run {m : Type u → Type u_1} [Monad m] [LawfulMonad m] [WP m PostShape.pure] [WPSound m PostShape.pure] [MonadAttach m] [LawfulMonadAttach m] {α : Type u} {prog : OptionT m α} {x : Option α} (P : Option α → Prop) (hcan : MonadAttach.CanReturn prog.run x) (hwp : ⊢ₛ wp⟦prog⟧ (fun (a : α) => ⌜P (some a)⌝, fun (x : PUnit) => ⌜P none⌝, PUnit.unit)) : P x

Pure-proposition soundness for OptionT.run, generalizing Option.of_wp_eq.

theorem Std.Do.Option.of_wp_eq {α : Type} {x prog : Option α} (h : prog = x) (P : Option α → Prop) : (⊢ₛ wp⟦prog⟧ (fun (a : α) => ⌜P (some a)⌝, fun (x : PUnit) => ⌜P none⌝, PUnit.unit)) → P x

Soundness lemma for Option: Id-specialization of OptionT.of_wp_run.