Weakest Precondition Interpretation

This module defines the weakest precondition interpretation WPMonad of monadic programs in terms of predicate transformers PredTrans.

An instance WPMonad m Pred EPred determines a function wpTrans : m α → PredTrans Pred EPred α that interprets a program x : m α as a predicate transformer. The function wp is the user-facing wrapper: wp x post epost computes the weakest precondition for x to satisfy normal postcondition post and exception postcondition epost.

Assertion Language Classes

Assertion is an alias type class for CompleteLattice. We use Assertion Pred for the assertion language of normal postconditions and Assertion EPred for exception postconditions.

Pre-defined instances

• WPMonad Id Prop EPost.Nil — pure computations.
• WPMonad (StateT σ m) (σ → Pred) EPred — stateful computations.
• WPMonad (ExceptT ε m) Pred (EPost.Cons (ε → Pred) EPred) — computations with exceptions.
• WPMonad (ReaderT ρ m) (ρ → Pred) EPred — reader computations.
• WPMonad (Except ε) Prop EPost⟨ε → Prop⟩ — concrete exception type.
• WPMonad (EStateM ε σ) (σ → Prop) (ε → σ → Prop) — concrete error-state monad.

WP and WPMonad Typeclasses

The WP typeclass interprets a program type Prog whose results have type Value as a monotone predicate transformer wpTrans : Prog → PredTrans Pred EPred Value.

The WPMonad typeclass adds soundness of the weakest precondition interpretation for the monadic pure and bind of a monad m, on top of a WP (m α) α Pred EPred interpretation for every result type α.

class Std.Internal.Do.WP (Prog : Type u) (Value : outParam (Type v)) (Pred : outParam (Type w)) (EPred : outParam (Type w')) [Assertion Pred] [Assertion EPred] : Type (max (max (max u v) w) w')

Weakest precondition interpretation of a program type Prog whose results have type Value, as a monotone predicate transformer over assertion language Pred with exception postconditions EPred.

• wpTrans : Prog → PredTrans Pred EPred Value

  The weakest precondition transformer for a program.

• wp_trans_monotone (x : Prog) : (wpTrans x).monotone

  Monotonicity: weaker postconditions yield weaker preconditions.

def Std.Internal.Do.WP.wp {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type w'} [Assertion Pred] [Assertion EPred] [self : WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost : EPred) : Pred

Weakest precondition of x for normal postcondition post and exception postcondition epost. The WP interpretation can be supplied explicitly via dot notation (inst.wp x post epost).

Equations

• Std.Internal.Do.wp x post epost = (Std.Internal.Do.WP.wpTrans x).apply post epost

class Std.Internal.Do.WPMonad (m : Type u → Type v) (Pred : outParam (Type w)) (EPred : outParam (Type w')) [Monad m] [Assertion Pred] [Assertion EPred] extends LawfulMonad m : Type (max (max (max (u + 1) v) w) w')

Weakest precondition monad: a monad m whose weakest precondition interpretation is sound for pure and bind. The interpretation for every result type is carried as the toWP field; an instance exposes it as a WP (m α) … interpretation.

• map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type u} (x : m α) : id <$> x = x
• comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type u} (x : m α) (y : m β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type u} (x : m α) (y : m β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type u} (g : α → β) (x : m α) : pure g <*> x = g <$> x
• map_pure {α β : Type u} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type u} (g : m (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type u} (f : α → β) (x : m α) : (do let a ← x pure (f a)) = f <$> x
• bind_map {α β : Type u} (f : m (α → β)) (x : m α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• pure_bind {α β : Type u} (x : α) (f : α → m β) : pure x >>= f = f x
• bind_assoc {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
• toWP (α : Type u) : WP (m α) α Pred EPred

  The weakest precondition interpretation of m at every result type.

• pure_le_wp_pure {α : Type u} (x : α) (post : α → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (post x) (wp (pure x) post epost)

  Soundness of pure: the postcondition applied to x implies the weakest precondition of pure x.

• bind_le_wp_bind {α β : Type u} (x : m α) (f : α → m β) (post : β → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x (fun (a : α) => wp (f a) post epost) epost) (wp (x >>= f) post epost)

  Soundness of bind: composing weakest preconditions is at least as strong as the weakest precondition of >>=.

@[instance_reducible, instance 100]

instance Std.Internal.Do.instWPOfWPMonad {m : Type u → Type v} {Pred : Type w} {EPred : Type w'} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [inst : WPMonad m Pred EPred] : WP (m α) α Pred EPred

A monadic WP interpretation is sourced from the monad's WPMonad instance. Low priority so a program type with a bespoke WP instance (e.g. a non-monadic one) is preferred.

Equations

• Std.Internal.Do.instWPOfWPMonad = Std.Internal.Do.WPMonad.toWP α

@[simp]

theorem Std.Internal.Do.WP.wpTrans_apply_eq {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) : (wpTrans x).apply = wp x

Derived WP Lemmas

Monotonicity and weakening consequences of the WP monotonicity axiom.

theorem Std.Internal.Do.WP.wp_consequence {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post post' : Value → Pred) (epost : EPred) (h : Lean.Order.PartialOrder.rel post post') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post' epost)

theorem Std.Internal.Do.WP.wp_consequence_econs {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post post' : Value → Pred) (epost epost' : EPred) (h : Lean.Order.PartialOrder.rel post post') (h' : Lean.Order.PartialOrder.rel epost epost') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post' epost')

theorem Std.Internal.Do.WP.wp_econs {Pred : Type u_2} {EPred : Type u_1} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost epost' : EPred) (h' : Lean.Order.PartialOrder.rel epost epost') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post epost')

theorem Std.Internal.Do.WP.wp_econs_bot {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x post Lean.Order.bot) (wp x post epost)

theorem Std.Internal.Do.WP.wp_consequence_le {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post post' : Value → Pred) (epost : EPred) (h : Lean.Order.PartialOrder.rel post post') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post epost)) : Lean.Order.PartialOrder.rel pre (wp x post' epost)

theorem Std.Internal.Do.WP.wp_econs_le {Pred : Type u_2} {EPred : Type u_1} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost epost' : EPred) (h : Lean.Order.PartialOrder.rel epost epost') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post epost)) : Lean.Order.PartialOrder.rel pre (wp x post epost')

theorem Std.Internal.Do.WP.wp_econs_bot_le {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] (x : Prog) (post : Value → Pred) (epost : EPred) {pre : Pred} (h : Lean.Order.PartialOrder.rel pre (wp x post Lean.Order.bot)) : Lean.Order.PartialOrder.rel pre (wp x post epost)

theorem Std.Internal.Do.wp_le_wp_of_eq {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x y : Prog} (h : x = y) (post : Value → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp y post epost) (wp x post epost)

Rewriting the program of a weakest precondition along an equation x = y weakens it: the precondition of y entails the precondition of x.

Derived WPMonad Lemmas

One-directional consequences of the WPMonad axioms for pure, bind, map, and seq.

theorem Std.Internal.Do.WPMonad.map_le_wp_map {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type z} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} (f : α → β) (x : m α) (post : β → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x (fun (a : α) => post (f a)) epost) (wp (f <$> x) post epost)

Soundness of Functor.map: mapping f over x preserves the WP.

theorem Std.Internal.Do.WPMonad.map_le_wp_map' {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type z} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} (f : α → β) (x : m α) (post : α → Pred) (post' : β → Pred) (epost : EPred) : (post = fun (a : α) => post' (f a)) → Lean.Order.PartialOrder.rel (wp x post epost) (wp (f <$> x) post' epost)

Variant of map_le_wp_map with an explicit postcondition equality hypothesis.

theorem Std.Internal.Do.WPMonad.seq_le_wp_seq {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type z} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} (f : m (α → β)) (x : m α) (post : β → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp f (fun (g : α → β) => wp x (fun (a : α) => post (g a)) epost) epost) (wp (f <*> x) post epost)

Soundness of Seq.seq: sequencing f <*> x preserves the WP.

WPMonad Instances

@[instance_reducible]

def Std.Internal.Do.Id.wpInst {α : Type u} : WP (Id α) α Prop EPost⟨⟩

Id's WP interpretation: Prop assertions and no exceptions.

Equations

• Std.Internal.Do.Id.wpInst = { wpTrans := fun (x : Id α) => { apply := fun (post : α → Prop) (_epost : EPost⟨⟩) => post x }, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.Internal.Do.Id.instWPMonad : WPMonad Id Prop EPost⟨⟩

Id is a WPMonad with Prop assertions and no exceptions.

Equations

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

@[simp]

theorem Std.Internal.Do.PredTrans.apply_pushExcept {α : Type u_1} {ε : Type u_2} {Pred : Type u_3} {EPred : Type u_4} (x : PredTrans Pred EPred (Except ε α)) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : x.pushExcept.apply post epost = x.apply (EPost.Cons.pushExcept post epost) epost.tail

@[instance_reducible]

def Std.Internal.Do.ExceptT.wpInst {m : Type u → Type z} {EPred : Type u_1} {ε α : Type u} {Pred : Type v} [Assertion Pred] [Assertion EPred] [WP (m (Except ε α)) (Except ε α) Pred EPred] : WP (ExceptT ε m α) α Pred (EPost.Cons✝ (ε → Pred) EPred)

ExceptT's WP interpretation: lift the base interpretation by adding an exception postcondition layer.

Equations

• Std.Internal.Do.ExceptT.wpInst = { wpTrans := fun (x : ExceptT ε m α) => (Std.Internal.Do.WP.wpTrans x.run).pushExcept, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.Internal.Do.ExceptT.instWPMonad {m : Type u → Type z} {EPred : Type u_1} {ε : Type u} {Pred : Type v} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : WPMonad (ExceptT ε m) Pred (EPost.Cons✝ (ε → Pred) EPred)

ExceptT lifts a WPMonad instance by adding an exception postcondition layer.

Equations

• Std.Internal.Do.ExceptT.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.4) => Std.Internal.Do.ExceptT.wpInst, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[simp]

theorem Std.Internal.Do.ExceptT.wp_apply_eq {m : Type u → Type z} {α ε : Type u} {Pred : Type u_1} {EPred : Type u_2} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (x : ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : wp x post epost = wp x.run (EPost.Cons.pushExcept post epost) epost.tail

@[instance_reducible]

def Std.Internal.Do.OptionT.wpInst {m : Type u → Type z} {EPred : Type u_1} {α Pred : Type u} [Assertion Pred] [Assertion EPred] [WP (m (Option α)) (Option α) Pred EPred] : WP (OptionT m α) α Pred (EPost.Cons✝ Pred EPred)

OptionT's WP interpretation: lift the base interpretation by adding a PUnit exception postcondition layer.

Equations

• Std.Internal.Do.OptionT.wpInst = { wpTrans := fun (x : OptionT m α) => (Std.Internal.Do.WP.wpTrans x.run).pushOption, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.Internal.Do.OptionT.instWPMonad {m : Type u → Type z} {EPred : Type u_1} {Pred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : WPMonad (OptionT m) Pred (EPost.Cons✝ Pred EPred)

OptionT lifts a WPMonad instance by adding a PUnit exception postcondition layer.

Equations

• Std.Internal.Do.OptionT.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.3) => Std.Internal.Do.OptionT.wpInst, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[simp]

theorem Std.Internal.Do.OptionT.wp_apply_eq {m : Type u → Type z} {α Pred : Type u} {EPred : Type u_1} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (x : OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : wp x post epost = wp x.run (EPost.Cons.pushOption post epost) epost.tail

@[instance_reducible]

def Std.Internal.Do.StateT.wpInst {m : Type u → Type z} {α : Type u} {EPred : Type v} {σ : Type u} {Pred : Type w} [Assertion Pred] [Assertion EPred] [WP (m (α × σ)) (α × σ) Pred EPred] : WP (StateT σ m α) α (σ → Pred) EPred

StateT's WP interpretation: lift the base interpretation by adding a state argument.

Equations

• Std.Internal.Do.StateT.wpInst = { wpTrans := fun (x : StateT σ m α) => Std.Internal.Do.pushArg fun (x_1 : σ) => Std.Internal.Do.WP.wpTrans (x.run x_1), wp_trans_monotone := ⋯ }

@[instance_reducible, instance 100]

instance Std.Internal.Do.StateT.instWPMonad {m : Type u → Type z} {EPred : Type v} {σ : Type u} {Pred : Type w} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : WPMonad (StateT σ m) (σ → Pred) EPred

StateT lifts a WPMonad instance by adding a state argument.

Equations

• Std.Internal.Do.StateT.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.4) => Std.Internal.Do.StateT.wpInst, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[simp]

theorem Std.Internal.Do.StateT.wp_apply_eq {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α σ : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (x : StateT σ m α) (post : α → σ → Pred) (epost : EPred) (s : σ) : wp x post epost s = wp (x.run s) (fun (x : α × σ) => match x with | (a, s) => post a s) epost

@[instance_reducible]

def Std.Internal.Do.ReaderT.wpInst {m : Type u → Type z} {EPred : Type u_1} {α ρ : Type u} {Pred : Type v} [Assertion Pred] [Assertion EPred] [WP (m α) α Pred EPred] : WP (ReaderT ρ m α) α (ρ → Pred) EPred

ReaderT's WP interpretation: lift the base interpretation by adding a reader argument.

Equations

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

@[instance_reducible]

instance Std.Internal.Do.ReaderT.instWPMonad {m : Type u → Type z} {EPred : Type u_1} {ρ : Type u} {Pred : Type v} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : WPMonad (ReaderT ρ m) (ρ → Pred) EPred

ReaderT lifts a WPMonad instance by adding a reader argument.

Equations

• Std.Internal.Do.ReaderT.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.4) => Std.Internal.Do.ReaderT.wpInst, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[simp]

theorem Std.Internal.Do.ReaderT.wp_apply_eq {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α ρ : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (x : ReaderT ρ m α) (post : α → ρ → Pred) (epost : EPred) (r : ρ) : wp x post epost r = wp (x.run r) (fun (a : α) => post a r) epost

Type Alias Instances

WPMonad instances for concrete monads that are type aliases for transformer stacks.

@[instance_reducible]

def Std.Internal.Do.Option.wpInst {α : Type u} : WP (Option α) α Prop Prop

Option's WP interpretation: Prop assertions and a single Prop exception postcondition.

Equations

• Std.Internal.Do.Option.wpInst = { wpTrans := fun (x : Option α) => { apply := fun (post : α → Prop) (epost : Prop) => x.elim epost post }, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.Internal.Do.Option.instWPMonad : WPMonad Option Prop Prop

Option is a WPMonad with Prop assertions and a single Prop exception postcondition.

Equations

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

@[instance_reducible]

def Std.Internal.Do.Except.wpInst {ε : Type u_1} {α : Type u} : WP (Except ε α) α Prop EPost⟨ε → Prop⟩

Except ε's WP interpretation: Prop assertions and a single exception postcondition.

Equations

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

@[instance_reducible]

instance Std.Internal.Do.Except.instWPMonad {ε : Type u_1} : WPMonad (Except ε) Prop EPost⟨ε → Prop⟩

Except ε is a WPMonad with Prop assertions and a single exception postcondition.

Equations

• Std.Internal.Do.Except.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.1) => Std.Internal.Do.Except.wpInst, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[instance_reducible]

def Std.Internal.Do.EStateM.wpInst {ε σ α : Type} : WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop)

EStateM ε σ's WP interpretation combining state and exceptions.

Equations

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

@[instance_reducible]

instance Std.Internal.Do.EStateM.instWPMonad {ε σ : Type} : WPMonad (EStateM ε σ) (σ → Prop) (ε → σ → Prop)

EStateM ε σ is a WPMonad combining state and exceptions.

Equations

• Std.Internal.Do.EStateM.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type) => Std.Internal.Do.EStateM.wpInst, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

Soundness Lemmas

These lemmas bridge wp reasoning to concrete program properties. Each one says: if wp prog ... holds, then a property P holds of the program's result.

theorem Std.Internal.Do.Id.of_wp_run_eq {α : Type u} {x : α} {prog : Id α} (h : prog.run = x) (P : α → Prop) (hwp : wp prog P epost⟨⟩) : P x

Soundness for Id: if wp prog P holds, then P holds of the result.

theorem Std.Internal.Do.Option.of_wp_eq {α : Type u} {x prog : Option α} (h : prog = x) (P : Option α → Prop) (hwp : wp prog (fun (a : α) => P (some a)) (P none)) : P x

Soundness for Option: if wp prog P holds, then P holds of the result.

theorem Std.Internal.Do.StateM.of_wp_run_eq {α σ : Type u_1} {x : α × σ} {prog : StateM σ α} {s : σ} (h : StateT.run prog s = x) (P : α × σ → Prop) (hwp : wp prog (fun (a : α) (s' : σ) => P (a, s')) epost⟨⟩ s) : P x

Soundness for StateM: if wp prog P s holds, then P holds of (prog.run s).

theorem Std.Internal.Do.StateM.of_wp_run'_eq {α σ : Type} {x : α} {prog : StateM σ α} {s : σ} (h : StateT.run' prog s = x) (P : α → Prop) (hwp : wp prog (fun (a : α) (x : σ) => P a) epost⟨⟩ s) : P x

Soundness for StateM (discarding final state).

theorem Std.Internal.Do.ReaderM.of_wp_run_eq {α ρ : Type} {x : α} {prog : ReaderM ρ α} {r : ρ} (h : ReaderT.run prog r = x) (P : α → Prop) (hwp : wp prog (fun (a : α) (x : ρ) => P a) epost⟨⟩ r) : P x

Soundness for ReaderM: if wp prog P r holds, then P holds of (prog.run r).

theorem Std.Internal.Do.Except.of_wp_eq {ε α : Type} {x prog : Except ε α} (h : prog = x) (P : Except ε α → Prop) (hwp : wp prog (fun (a : α) => P (Except.ok a)) epost⟨fun (e : ε) => P (Except.error e)⟩) : P x

Soundness for Except: if wp prog P holds, then P holds of the result.

theorem Std.Internal.Do.EStateM.of_wp_run_eq {ε σ α : Type} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α} {s : σ} (h : prog.run s = x) (P : EStateM.Result ε σ α → Prop) (hwp : wp prog (fun (a : α) (s' : σ) => P (EStateM.Result.ok a s')) (fun (e : ε) (s' : σ) => P (EStateM.Result.error e s')) s) : P x

Soundness for EStateM: if wp prog P s holds, then P holds of (prog.run s).