17.2.1. Assertion Lattices🔗

The predicate transformer semantics of programs is based on a logic in which propositions may mention the program's state. Here, “state” refers not only to mutable state, but also to read-only values such as those that are provided via ReaderT. Different program types have different assertion types, which can be any complete lattice. More specifically, assertion types instantiate Assertion, which is a Lean.Parser.Command.classAbbrev : commandExpands ``` class abbrev C <params> := D_1, ..., D_n ``` into ``` class C <params> extends D_1, ..., D_n attribute [instance] C.mk ``` class abbrev over CompleteLattice that is recognized by vcgen.

Std.WP.Assertion.{w} (α : Type w) : Type w
Std.WP.Assertion.{w} (α : Type w) : Type w

Std.WP.Assertion.mk.{w}

rel : α → α → Prop

rel_refl : ∀ {x : α}, x ⊑ x

rel_trans : ∀ {x y z : α}, x ⊑ y → y ⊑ z → x ⊑ z

rel_antisymm : ∀ {x y : α}, x ⊑ y → y ⊑ x → x = y

has_sup : ∀ (c : α → Prop), Exists (is_sup c)

The difference between entailment and implication is that entailment is a statement in Lean's logic, while implication is internal to the assertion language: for assertions P and Q, P ⊑ Q is a Prop while P ⇨ Q is again an assertion.

Std.WP comes with Assertion instances for Prop, Unit, function types, and pairs. The lattice operations on Prop coincide with the ordinary logical connectives, with entailment being implication. The lattice operations on a function type such as Nat → Prop operate pointwise, so entailment of state predicates is universally-quantified implication. The lattice operations on a pair such as (Nat → Prop) × (Bool → Prop) operate component-wise, so entailment of paired predicates is the conjunction of entailments of the component predicates.

Ordinary propositions that do not mention the state can be embedded into any assertion lattice with corner brackets. This is written with the syntax ⌜P⌝, which is notation for Lean.Order.CompleteLattice.ofProp.

term ::= ...
    | Embedding of propositions into an CompleteLattice type. `⌜p⌝` embeds `p : Prop` as `⊤` if `p` holds
and `⊥` otherwise. ⌜term⌝

Lean.Order.CompleteLattice.ofProp.{u_1} {l : Type u_1}
  [CompleteLattice l] (p : Prop) : l
Lean.Order.CompleteLattice.ofProp.{u_1}
  {l : Type u_1} [CompleteLattice l]
  (p : Prop) : l

An assertion of the form ⌜p⌝ is pure: its truth is independent of the state. At the assertion type Prop, ⌜p⌝ is the proposition p itself, and at a state predicate type such as Nat → Prop, it is the constant predicate fun _ => p. Specifications for a concrete monad can therefore state propositions directly, as in fun s => s = n. Corner brackets are necessary when the assertion type is abstract, as in a specification that quantifies over a monad and its assertion type Pred. In this case, a proposition such as n = k is not an assertion, but ⌜n = k⌝ embeds it into Pred. The monad-polymorphic example at the end of this chapter uses corner brackets for this reason. vcgen moves pure preconditions into the ordinary Lean context, where they become hypotheses of the verification conditions.

17.2.2. Exception Postconditions🔗

A postcondition for successful termination is a function from the return value to an assertion. Programs that can throw exceptions additionally require an exception postcondition that asserts what holds when the program throws an exception. The exception postcondition type of a given monad is determined by its WP instance.

For example, the WP instance for ExceptT String (StateM Nat) Bool determines Nat → Prop as the assertion type, hence Bool → Nat → Prop as the postcondition type, and String → Nat → Prop as the exception postcondition type. A monad without exceptions has the exception postcondition type Unit.

For a base monad with assertion type Pred and exception postcondition type EPred, an exception layer such as ExceptT ε contributes one more exception postcondition, which gives the type (ε → Pred) × EPred.

Since unit and pair types come with Assertion instances, these “stacks” of exception postconditions are automatically assertions as well. The WP instances for monad transformers ensure that stacks of monad transformers have corresponding exception postcondition stacks.

term ::= ...
    | Exception postcondition stack **type**: `EStack⟨ε₁ → l, ε₂ → l⟩` is `(ε₁ → l) × (ε₂ → l) × EStack⟨⟩`. EStack⟨term,*⟩

term ::= ...
    | Exception postcondition stack **value**: `estack⟨e₁, e₂⟩` is `(e₁, e₂, ())`. estack⟨term,*⟩

Specifications for programs that might throw exceptions come in two varieties. The total correctness interpretation ⦃P⦄ prog ⦃Q'⦄ asserts that, given P holds, then prog terminates normally and Q' holds for the result. The partial correctness interpretation ⦃P⦄ prog ⦃Q'; ⊤⦄ asserts that, given P holds, and if prog terminates normally then Q' holds for the result. A triple without an explicit exception postcondition carries the bottom assertion (⊥ : EPred) and thus has the total interpretation; between ⊥ and ⊤, the exception postcondition expresses a spectrum of correctness properties.

17.2.3. Predicate Transformers🔗

A predicate transformer is a function from postconditions into assertions that describe preconditions.

Lean.Order.PredTrans.{u, v, w} (Pred : Type u) (EPred : Type v)
  (α : Type w) : Type (max (max u v) w)
Lean.Order.PredTrans.{u, v, w}
  (Pred : Type u) (EPred : Type v)
  (α : Type w) : Type (max (max u v) w)

Lean.Order.PredTrans.mk.{u, v, w}

apply : (α → Pred) → EPred → Pred

The partial order on predicate transformers is inherited pointwise from the assertion lattice: x ⊑ y when x.apply post epost ⊑ y.apply post epost for all post and epost. Every predicate transformer that a WP instance produces is monotone: if post ⊑ post' and epost ⊑ epost', then x.apply post epost ⊑ x.apply post' epost'.

Lean.Order.PredTrans.monotone.{u, v, w} {Pred : Type u} {EPred : Type v}
  {α : Type w} [PartialOrder Pred] [PartialOrder EPred]
  (pt : PredTrans Pred EPred α) : Prop
Lean.Order.PredTrans.monotone.{u, v, w}
  {Pred : Type u} {EPred : Type v}
  {α : Type w} [PartialOrder Pred]
  [PartialOrder EPred]
  (pt : PredTrans Pred EPred α) : Prop

Predicate transformers form a monad. The pure operator is the identity transformer; it simply instantiates the postcondition with its argument. The bind operator composes predicate transformers.

Lean.Order.PredTrans.pure.{u, v, w} {Pred : Type u} {EPred : Type v}
  {α : Type w} (a : α) : PredTrans Pred EPred α
Lean.Order.PredTrans.pure.{u, v, w}
  {Pred : Type u} {EPred : Type v}
  {α : Type w} (a : α) :
  PredTrans Pred EPred α

Lean.Order.PredTrans.bind.{u, v, w} {Pred : Type u} {EPred : Type v}
  {α β : Type w} (x : PredTrans Pred EPred α)
  (f : α → PredTrans Pred EPred β) : PredTrans Pred EPred β
Lean.Order.PredTrans.bind.{u, v, w}
  {Pred : Type u} {EPred : Type v}
  {α β : Type w}
  (x : PredTrans Pred EPred α)
  (f : α → PredTrans Pred EPred β) :
  PredTrans Pred EPred β

The helper operators PredTrans.pushArg, PredTrans.pushExceptT, and PredTrans.pushOptionT modify a predicate transformer by adding a standard side effect. They are used to implement the WP instances for transformers such as StateT, ExceptT, and OptionT; they can also be used to implement monads that can be thought of in terms of one of these. For example, PredTrans.pushArg is typically used for state monads, but can also be used to implement a reader monad's instance, treating the reader's value as read-only state.

Lean.Order.PredTrans.pushArg.{u, v, w, z} {Pred : Type u}
  {EPred : Type v} {α : Type w} {σ : Type z}
  (x : σ → PredTrans Pred EPred (α × σ)) : PredTrans (σ → Pred) EPred α
Lean.Order.PredTrans.pushArg.{u, v, w, z}
  {Pred : Type u} {EPred : Type v}
  {α : Type w} {σ : Type z}
  (x : σ → PredTrans Pred EPred (α × σ)) :
  PredTrans (σ → Pred) EPred α

Lean.Order.PredTrans.pushExceptT.{u, v, w, z} {Pred : Type u}
  {EPred : Type v} {α : Type w} {ε : Type z}
  (x : PredTrans Pred EPred (Except ε α)) :
  PredTrans Pred ((ε → Pred) × EPred) α
Lean.Order.PredTrans.pushExceptT.{u, v, w,
    z}
  {Pred : Type u} {EPred : Type v}
  {α : Type w} {ε : Type z}
  (x :
    PredTrans Pred EPred (Except ε α)) :
  PredTrans Pred ((ε → Pred) × EPred) α

Lean.Order.PredTrans.pushOptionT.{u, v, w} {Pred : Type u}
  {EPred : Type v} {α : Type w} (x : PredTrans Pred EPred (Option α)) :
  PredTrans Pred ((Unit → Pred) × EPred) α
Lean.Order.PredTrans.pushOptionT.{u, v, w}
  {Pred : Type u} {EPred : Type v}
  {α : Type w}
  (x : PredTrans Pred EPred (Option α)) :
  PredTrans Pred ((Unit → Pred) × EPred) α

Std.WP.WP.{u, v, w, w'} (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')
Std.WP.WP.{u, v, w, w'} (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')

Std.WP.WP.mk.{u, v, w, w'}

wpTrans : Prog → PredTrans Pred EPred Value

wp_trans_monotone : ∀ (x : Prog), (WP.wpTrans x).monotone

Std.WP.WP.wp.{u, v, w, w'} {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
Std.WP.WP.wp.{u, v, w, w'} {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

Std.WP.WPConjunctive.{u, v, w, z} {Prog : Type u}
  {Value : outParam (Type v)} {Pred : outParam (Type w)}
  {EPred : outParam (Type z)} [Assertion Pred] [Assertion EPred]
  [WP Prog Value Pred EPred] (x : Prog) : Prop
Std.WP.WPConjunctive.{u, v, w, z}
  {Prog : Type u}
  {Value : outParam (Type v)}
  {Pred : outParam (Type w)}
  {EPred : outParam (Type z)}
  [Assertion Pred] [Assertion EPred]
  [WP Prog Value Pred EPred] (x : Prog) :
  Prop

Std.WP.WPConjunctive.mk.{u, v, w, z}

wp_meet_wp_le : ∀ (Q₁ Q₂ : Value → Pred) (E₁ E₂ : EPred), wp x Q₁ E₁ ⊓ wp x Q₂ E₂ ⊑ wp x (Q₁ ⊓ Q₂) (E₁ ⊓ E₂)

Std.WP.WPMonad.{u, v, w, w'} (m : Type u → Type v)
  (Pred : outParam (Type w)) (EPred : outParam (Type w')) [Monad m]
  [Assertion Pred] [Assertion EPred] :
  Type (max (max (max (u + 1) v) w) w')
Std.WP.WPMonad.{u, v, w, w'}
  (m : Type u → Type v)
  (Pred : outParam (Type w))
  (EPred : outParam (Type w')) [Monad m]
  [Assertion Pred] [Assertion EPred] :
  Type (max (max (max (u + 1) v) w) w')

Std.WP.WPMonad.mk.{u, v, w, w'}

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

pure_le_wp_pure : ∀ {α : Type u} (x : α) (post : α → Pred) (epost : EPred), post x ⊑ wp (pure x) post epost

bind_le_wp_bind : ∀ {α β : Type u} (x : m α) (f : α → m β) (post : β → Pred) (epost : EPred),
  wp x (fun a => wp (f a) post epost) epost ⊑ wp (x >>= f) post epost

No spec applicable to program (forIn xs [] fun x __s => pure (ForInStep.yield (x :: __s))) >>=
  pure in monad Identity. Candidates were [SpecProof.global Std.WP.Spec.bind].

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

Std.WP.StateM.of_run_eq_wp.{u_1} {α σ : 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
Std.WP.StateM.of_run_eq_wp.{u_1}
  {α σ : 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

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
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

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
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

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
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

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

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
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

17.2.4. Hoare Triples🔗

A Hoare triple (Hoare, 1969)Marginal noteShow marginal noteC. A. R. Hoare (1969). “An Axiomatic Basis for Computer Programming”. Communications of the ACM. 12(10), pp. 576–583. consists of a precondition, a program, and a postcondition. Running the program in a state for which the precondition is true results in a state where the postcondition is true.

Std.WP.Triple.{u, v, w, w'} {Pred : Type w} {EPred : Type w'}
  {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPred]
  (x : Prog) [WP Prog Value Pred EPred] (pre : Pred)
  (post : Value → Pred) (epost : EPred) : Prop
Std.WP.Triple.{u, v, w, w'}
  {Pred : Type w} {EPred : Type w'}
  {Prog : Type u} {Value : Type v}
  [Assertion Pred] [Assertion EPred]
  (x : Prog) [WP Prog Value Pred EPred]
  (pre : Pred) (post : Value → Pred)
  (epost : EPred) : Prop

Std.WP.Triple.intro.{u, v, w, w'}

le_wp : pre ⊑ wp x post epost