Soundness of the Weakest Precondition Interpretation

LawfulWPMonadAttach m Pred EPred relates the wp interpretation of m to the values that a program x : m α returns. Its single field of_canReturn_wp says: if the postcondition fun a => ⌜P a⌝ follows from ⊤ under wp x, then P a holds for every a with MonadAttach.CanReturn x a.

For a transformer, MonadAttach.CanReturn speaks about the computation that remains once the reader or state argument is supplied and the Except or Option result is exposed. The of_canReturn_run_wp lemmas take the witness in that form, pairing it with wp prog at the supplied argument.

The of_run_eq_wp family at the end of the file specializes soundness to the concrete monads Id, Option, StateM, ReaderM, Except and EStateM, where the witness is an equation prog.run s = x.

class Std.WP.LawfulWPMonadAttach (m : Type u → Type v) (Pred : outParam (Type w)) (EPred : outParam (Type z)) [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : Prop

Soundness of the weakest precondition interpretation of m: a postcondition that wp proves holds of every value the program returns.

• of_canReturn_wp {α : Type u} {x : m α} {P : α → Prop} {a : α} : MonadAttach.CanReturn x a → Lean.Order.PartialOrder.rel Lean.Order.top (wp x (fun (a : α) => Lean.Order.CompleteLattice.ofProp (P a)) Lean.Order.top) → P a

  From a wp-provable postcondition and a MonadAttach.CanReturn witness, conclude P at that value.

instance Std.WP.Id.instLawfulWPMonadAttach : LawfulWPMonadAttach Id Prop EStack⟨⟩

instance Std.WP.Option.instLawfulWPMonadAttach : LawfulWPMonadAttach Option Prop (Unit → Prop)

instance Std.WP.Except.instLawfulWPMonadAttach {ε : Type u} : LawfulWPMonadAttach (Except ε) Prop (ε → Prop)

instance Std.WP.EStateM.instLawfulWPMonadAttach {ε σ : Type} : LawfulWPMonadAttach (EStateM ε σ) (σ → Prop) (ε → σ → Prop)

instance Std.WP.ExceptT.instLawfulWPMonadAttach {ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} {Pred : Type u_4} {EPred : Type u_5} [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulWPMonadAttach m Pred EPred] : LawfulWPMonadAttach (ExceptT ε m) Pred ((ε → Pred) × EPred)

instance Std.WP.OptionT.instLawfulWPMonadAttach {m : Type u → Type z} {Pred : Type u} {EPred : Type w} [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulWPMonadAttach m Pred EPred] : LawfulWPMonadAttach (OptionT m) Pred ((Unit → Pred) × EPred)

instance Std.WP.StateT.instLawfulWPMonadAttach {m : Type u → Type z} {σ : Type u} {Pred : Type v} {EPred : Type w} [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulWPMonadAttach m Pred EPred] : LawfulWPMonadAttach (StateT σ m) (σ → Pred) EPred

instance Std.WP.ReaderT.instLawfulWPMonadAttach {m : Type u → Type z} {ρ : Type u} {Pred : Type v} {EPred : Type w} [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulWPMonadAttach m Pred EPred] : LawfulWPMonadAttach (ReaderT ρ m) (ρ → Pred) EPred

Soundness at the Post-Run Computation

For a transformer T, T.of_canReturn_run_wp takes the MonadAttach.CanReturn witness for the base-monad computation that prog becomes once its arguments are supplied.

theorem Std.WP.ReaderT.of_canReturn_run_wp {m : Type u → Type z} {ρ : Type u} {Pred : Type v} {EPred : Type w} [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulWPMonadAttach m Pred EPred] {α : Type u} {prog : ReaderT ρ m α} {r : ρ} {a : α} (P : α → Prop) (hcan : MonadAttach.CanReturn (prog.run r) a) (hwp : Lean.Order.PartialOrder.rel Lean.Order.top (wp prog (fun (a : α) => Lean.Order.CompleteLattice.ofProp (P a)) Lean.Order.top r)) : P a

A wp-provable postcondition holds at every value that the post-run computation prog.run r : m α returns.

theorem Std.WP.StateT.of_canReturn_run_wp {m : Type u → Type z} {σ : Type u} {Pred : Type v} {EPred : Type w} [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulWPMonadAttach m Pred EPred] {α : Type u} {prog : StateT σ m α} {s : σ} {p : α × σ} (P : α × σ → Prop) (hcan : MonadAttach.CanReturn (prog.run s) p) (hwp : Lean.Order.PartialOrder.rel Lean.Order.top (wp prog (fun (a : α) (s' : σ) => Lean.Order.CompleteLattice.ofProp (P (a, s'))) Lean.Order.top s)) : P p

A wp-provable postcondition holds at every value-state pair that the post-run computation prog.run s : m (α × σ) returns.

theorem Std.WP.ExceptT.of_canReturn_run_wp {m : Type u → Type z} {ε : Type u} {Pred : Type v} {EPred : Type w} [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulWPMonadAttach m Pred EPred] {α : Type u} {prog : ExceptT ε m α} {x : Except ε α} (P : Except ε α → Prop) (hcan : MonadAttach.CanReturn prog.run x) (hwp : Lean.Order.PartialOrder.rel Lean.Order.top (wp prog (fun (a : α) => Lean.Order.CompleteLattice.ofProp (P (Except.ok a))) (fun (e : ε) => Lean.Order.CompleteLattice.ofProp (P (Except.error e)), Lean.Order.top))) : P x

A wp-provable postcondition with split .ok/.error cases holds at every result that the post-run computation prog.run : m (Except ε α) returns.

theorem Std.WP.OptionT.of_canReturn_run_wp {m : Type u → Type z} {Pred : Type u} {EPred : Type w} [Monad m] [MonadAttach m] [LawfulMonadAttach m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulWPMonadAttach m Pred EPred] {α : Type u} {prog : OptionT m α} {x : Option α} (P : Option α → Prop) (hcan : MonadAttach.CanReturn prog.run x) (hwp : Lean.Order.PartialOrder.rel Lean.Order.top (wp prog (fun (a : α) => Lean.Order.CompleteLattice.ofProp (P (some a))) (fun (x : Unit) => Lean.Order.CompleteLattice.ofProp (P none), Lean.Order.top))) : P x

A wp-provable postcondition with split some/none cases holds at every result that the post-run computation prog.run : m (Option α) returns.

Soundness at a Concrete Result

Each lemma below takes the program's result as an equation and concludes a property of it.

theorem Std.WP.Id.of_run_eq_wp {α : Type u} {x : α} {prog : Id α} (h : prog.run = x) (P : α → Prop) (hwp : wp prog P ()) : P x

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

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

Soundness for Option: the postcondition takes a some case and a none case, and wp prog holds of prog itself.

theorem Std.WP.StateM.of_run_eq_wp {α σ : Type u_1} {x : α × σ} {prog : StateM σ α} {s : σ} (h : StateT.run prog s = x) (P : α × σ → Prop) (hwp : wp prog (fun (a : α) (s' : σ) => P (a, s')) () s) : P x

Soundness for StateM: if wp prog P s holds, then P holds of the value and final state of StateT.run prog s.

theorem Std.WP.StateM.of_run'_eq_wp {α σ : Type} {x : α} {prog : StateM σ α} {s : σ} (h : StateT.run' prog s = x) (P : α → Prop) (hwp : wp prog (fun (a : α) (x : σ) => P a) () s) : P x

Soundness for StateM, at the value alone: if wp prog P s holds, then P holds of StateT.run' prog s.

theorem Std.WP.ReaderM.of_run_eq_wp {α ρ : Type} {x : α} {prog : ReaderM ρ α} {r : ρ} (h : ReaderT.run prog r = x) (P : α → Prop) (hwp : wp prog (fun (a : α) (x : ρ) => P a) () r) : P x

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

theorem Std.WP.Except.of_eq_wp {ε α : Type} {x prog : Except ε α} (h : prog = x) (P : Except ε α → Prop) (hwp : wp prog (fun (a : α) => P (Except.ok a)) fun (e : ε) => P (Except.error e)) : P x

Soundness for Except: the postcondition takes an ok case and an error case, and wp prog holds of prog itself.

theorem Std.WP.EStateM.of_run_eq_wp {ε σ α : 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).