18. The `mvcgen` tactic🔗

The mvcgen tactic implements a monadic verification condition generator: It breaks down a goal involving a program written using Lean's imperative Lean.Parser.Term.do : termdo notation into a number of pure verification conditions (VCs) that discharge said goal. A verification condition is a sub-goal that does not mention the monad underlying the do block.

In order to use the mvcgen tactic, Std.Tactic.Do must be imported and the namespace Std.Do must be opened.

18.1. Verifying Imperative Programs Using `mvcgen`

This section is a tutorial that introduces the most important concepts of mvcgen top-down. Recall that you need to import Std.Tactic.Do and open Std.Do to run these examples:

import Std.Tactic.Do

open Std.Do

18.1.1. Preconditions and Postconditions

One style in which program specifications can be written is to provide a precondition P, which the caller of a program \mathit{prog} is expected to ensure, and a postcondition Q, which the \mathit{prog} is expected to ensure. The program \mathit{prog} satisfies the specification if running it when the precondition P holds always results in the postcondition Q holding.

In general, many different preconditions might suffice for a program to ensure the postcondition. After all, new preconditions can be generated by replacing a precondition P_1 with P_1 \wedge P_2. The weakest precondition \textbf{wp}⟦\mathit{prog}⟧(Q) of a program \mathit{prog} and postcondition Q is a precondition for which \mathit{prog} ensures the postcondition Q and is implied by all other such preconditions.

One way to prove something about the result of a program is to find the weakest precondition that guarantees the desired result, and then to show that this weakest precondition is simply true. This means that the postcondition holds no matter what.

18.1.2. Loops and Invariants

As a first example of mvcgen, the function mySum computes the sum of an array using local mutable state and a Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for loop:

def mySum (l : Array Nat) : Nat := Id.run do
  let mut out := 0
  for i in l do
    out := out + i
  return out

If mySum is correct, then it is equal to Array.sum. In mySum, the use of Lean.Parser.Term.do : termdo is an internal implementation detail—the function's signature makes no mention of any monad. Thus, the proof first manipulates the goal into a form that is amenable to the use of mvcgen, using the lemma Id.of_wp_run_eq. This lemma states that facts about the result of running a computation in the Id monad that terminates normally (Id computations never throw exceptions) can be proved by showing that the weakest precondition that ensures the desired result is true. Next, the proof uses mvcgen to replace the formulation in terms of weakest preconditions with a set of verification conditions.

While mvcgen is mostly automatic, it does require an invariant for the loop. A loop invariant is a statement that is both assumed and guaranteed by the body of the loop; if it is true when the loop begins, then it will be true when the loop terminates.

theorem mySum_correct (l : Array Nat) : mySum l = l.sum := byl:Array Nat⊢ mySum l = l.sum
  -- Focus on the part of the program with the `do` block (`Id.run ...`)
  generalize h : mySum l = xl:Array Natx:Nath:mySum l = x⊢ x = l.sum
  apply Id.of_wp_run_eq hal:Array Natx:Nath:mySum l = x⊢ ⊢ₛ
  wp⟦have out := 0;
      do
      let r ←
        forIn l out fun i r =>
            have out := r;
            have out := out + i;
            do
            pure PUnit.unit
            pure (ForInStep.yield out)
      have out : Nat := r
      pure out⟧
    (PostCond.noThrow fun a => { down := a = l.sum })
  -- Break down into verification conditions
  mvcgeninv1l:Array Natx:Nath:mySum l = x⊢ Invariant l.toList Nat PostShape.purevc1.stepl:Array Natx:Nath:mySum l = xpref✝:List Natcur✝:Natsuff✝:List Nath✝¹:l.toList = pref✝ ++ cur✝ :: suff✝b✝:Nath✝:(Prod.fst ?inv1 ({ «prefix» := pref✝, suffix := cur✝ :: suff✝, property := ⋯ }, b✝)).down⊢ (Prod.fst ?inv1 ({ «prefix» := pref✝ ++ [cur✝], suffix := suff✝, property := ⋯ }, b✝ + cur✝)).downvc2.a.prel:Array Natx:Nath:mySum l = x⊢ (Prod.fst ?inv1 ({ «prefix» := [], suffix := l.toList, property := ⋯ }, 0)).downvc3.a.post.successl:Array Natx:Nath:mySum l = xr✝:Nath✝:(Prod.fst ?inv1 ({ «prefix» := l.toList, suffix := [], property := ⋯ }, r✝)).down⊢ r✝ = l.sum
  -- Specify the invariant which should hold throughout the loop
  -- * `out` refers to the current value of the `let mut` variable
  -- * `xs` is a `List.Cursor`, which is a data structure representing
  --   a list that is split into `xs.prefix` and `xs.suffix`.
  --   It tracks how far into the loop we have gotten.
  -- Our invariant is that `out` holds the sum of the prefix.
  -- The notation ⌜p⌝ embeds a `p : Prop` into the assertion language.
  case inv1 =>l:Array Natx:Nath:mySum l = x⊢ Invariant l.toList Nat PostShape.pure exact ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝All goals completed! 🐙
  -- After specifying the invariant, we can further simplify our goals
  -- by "leaving the proof mode". `mleave` is just
  -- `simp only [...] at *` with a stable simp subset.
  all_goals mleavevc3.a.post.successl:Array Natx:Nath:mySum l = xr✝:Nath✝:l.toList.sum = r✝⊢ r✝ = l.sum
  -- Prove that our invariant is preserved at each step of the loop
  case vc1 ih =>l:Array Natx:Nath:mySum l = xpref✝:List Natcur✝:Natsuff✝:List Nath✝:l.toList = pref✝ ++ cur✝ :: suff✝b✝:Natih:pref✝.sum = b✝⊢ (pref✝ ++ [cur✝]).sum = b✝ + cur✝
    -- The goal here mentions `pref`, which binds the `prefix` field of
    -- the cursor passed to the invariant. Unpacking the
    -- (dependently-typed) cursor makes it easier for `grind`.
    grindAll goals completed! 🐙
  -- Prove that the invariant is true at the start
  case vc2 =>l:Array Natx:Nath:mySum l = x⊢ [].sum = 0
    grindAll goals completed! 🐙
  -- Prove that the invariant at the end of the loop implies the
  -- property we wanted
  case vc3 h =>l:Array Natx:Nath✝:mySum l = xr✝:Nath:l.toList.sum = r✝⊢ r✝ = l.sum
    grindAll goals completed! 🐙

Note that the case labels are actually unique prefixes of the full case labels. Whenever referring to cases, only this prefix should be used; the suffix is merely a hint to the user of where that particular VC came from. For example:

vc1.step conveys that this VC proves the inductive step for the loop
vc2.a.pre is meant to prove that the hypotheses of a goal imply the precondition of a specification (of forIn).
vc3.a.post.success is meant to prove that the postcondition of a specification (of forIn) implies the desired property.

After specifying the loop invariant, the proof can be shortened to just all_goals mleave; grind (where mleave leaves the stateful proof mode, cleaning up the proof state).

theorem mySum_correct_short (l : Array Nat) : mySum l = l.sum := byl:Array Nat⊢ mySum l = l.sum
  generalize h : mySum l = xl:Array Natx:Nath:mySum l = x⊢ x = l.sum
  apply Id.of_wp_run_eq hal:Array Natx:Nath:mySum l = x⊢ ⊢ₛ
  wp⟦have out := 0;
      do
      let r ←
        forIn l out fun i r =>
            have out := r;
            have out := out + i;
            do
            pure PUnit.unit
            pure (ForInStep.yield out)
      have out : Nat := r
      pure out⟧
    (PostCond.noThrow fun a => { down := a = l.sum })
  mvcgeninv1l:Array Natx:Nath:mySum l = x⊢ Invariant l.toList Nat PostShape.purevc1.stepl:Array Natx:Nath:mySum l = xpref✝:List Natcur✝:Natsuff✝:List Nath✝¹:l.toList = pref✝ ++ cur✝ :: suff✝b✝:Nath✝:(Prod.fst ?inv1 ({ «prefix» := pref✝, suffix := cur✝ :: suff✝, property := ⋯ }, b✝)).down⊢ (Prod.fst ?inv1 ({ «prefix» := pref✝ ++ [cur✝], suffix := suff✝, property := ⋯ }, b✝ + cur✝)).downvc2.a.prel:Array Natx:Nath:mySum l = x⊢ (Prod.fst ?inv1 ({ «prefix» := [], suffix := l.toList, property := ⋯ }, 0)).downvc3.a.post.successl:Array Natx:Nath:mySum l = xr✝:Nath✝:(Prod.fst ?inv1 ({ «prefix» := l.toList, suffix := [], property := ⋯ }, r✝)).down⊢ r✝ = l.sum
  case inv1 =>l:Array Natx:Nath:mySum l = x⊢ Invariant l.toList Nat PostShape.pure exact ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝All goals completed! 🐙
  all_goals mleavevc3.a.post.successl:Array Natx:Nath:mySum l = xr✝:Nath✝:l.toList.sum = r✝⊢ r✝ = l.sum; grindAll goals completed! 🐙

This pattern is so common that mvcgen comes with special syntax for it:

theorem mySum_correct_shorter (l : Array Nat) : mySum l = l.sum := byl:Array Nat⊢ mySum l = l.sum
  generalize h : mySum l = xl:Array Natx:Nath:mySum l = x⊢ x = l.sum
  apply Id.of_wp_run_eq hal:Array Natx:Nath:mySum l = x⊢ ⊢ₛ
  wp⟦have out := 0;
      do
      let r ←
        forIn l out fun i r =>
            have out := r;
            have out := out + i;
            do
            pure PUnit.unit
            pure (ForInStep.yield out)
      have out : Nat := r
      pure out⟧
    (PostCond.noThrow fun a => { down := a = l.sum })
  mvcgen
  invariants
  · ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝
  with grindAll goals completed! 🐙

The mvcgen invariants ...with... is an abbreviation for the tactic sequence mvcgen; case inv1 => ...; all_goals mleave; grind above. It is the form that we will be using from now on.

It is helpful to compare the proof of mySum_correct_shorter to a traditional correctness proof:

theorem mySum_correct_vanilla (l : Array Nat) : mySum l = l.sum := byl:Array Nat⊢ mySum l = l.sum
  -- Turn the array into a list
  cases l with | mk l =>mkl:List Nat⊢ mySum { toList := l } = { toList := l }.sum
  -- Unfold `mySum` and rewrite `forIn` to `foldl`
  simp [mySum]mkl:List Nat⊢ List.foldl (fun b a => b + a) 0 l = l.sum
  -- Generalize the inductive hypothesis
  suffices h : ∀ out, List.foldl (· + ·) out l = out + l.sum byl:List Nath:∀ (out : Nat), List.foldl (fun x1 x2 => x1 + x2) out _fvar.53 = out + List.sum _fvar.53 := ?_mvar.2864⊢ List.foldl (fun b a => b + a) 0 l = l.sum simp [h]All goals completed! 🐙
  -- Grind away
  induction l with grindAll goals completed! 🐙

This proof is similarly succinct as the proof in mySum_correct_shorter that uses mvcgen. However, the traditional approach relies on important properties of the program:

The Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for loop does not Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break or Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`, skipping any further statements. Note that uses of the `do` keyword in other syntax like in `for _ in _ do` do not constitute a surrounding block in this sense; in supported editors, the corresponding `do` keyword of the surrounding block is highlighted when hovering over `return`. `return` not followed by a term starting on the same line is equivalent to `return ()`.return early. Otherwise, the forIn could not be rewritten to a foldl.
The loop body (· + ·) is small enough to be repeated in the proof.
The loop body does not carry out any effects in the underlying monad (that is, the only effects are those introduced by Lean.Parser.Term.do : termdo-notation). The Id monad has no effects, so all of its comptutations are pure. While forIn could still be rewritten to a foldlM, reasoning about the monadic loop body can be tough for grind.

In the following sections, we will go through several examples to learn about mvcgen and its support library, and also see where traditional proofs become difficult. This is usually caused by:

Lean.Parser.Term.do : termdo blocks using control flow constructs such as Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for loops, Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. breaks and early Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`, skipping any further statements. Note that uses of the `do` keyword in other syntax like in `for _ in _ do` do not constitute a surrounding block in this sense; in supported editors, the corresponding `do` keyword of the surrounding block is highlighted when hovering over `return`. `return` not followed by a term starting on the same line is equivalent to `return ()`.return.
The use of effects in non-Id monads, which affects the implicit monadic context (state, exceptions) in ways that need to be reflected in loop invariants.

mvcgen scales to these challenges with reasonable effort.

18.1.3. Control Flow

Let us consider another example that combines Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for loops with an early return. List.Nodup is a predicate that asserts that a given list does not contain any duplicates. The function nodup below decides this predicate:

def nodup (l : List Int) : Bool := Id.run do
  let mut seen : Std.HashSet Int := ∅
  for x in l do
    if x ∈ seen then
      return false
    seen := seen.insert x
  return true

This function is correct if it returns true for every list that satisfies List.Nodup and false for every list that does not. Just as it was in mySum, the use of Lean.Parser.Term.do : termdo-notation and the Id monad is an internal implementation detail of nodup. Thus, the proof begins by using Id.of_wp_run_eq to make the proof state amenable to mvcgen:

theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := byl:List Int⊢ nodup l = true ↔ l.Nodup
  generalize h : nodup l = rl:List Intr:Boolh:nodup l = r⊢ r = true ↔ l.Nodup
  apply Id.of_wp_run_eq hal:List Intr:Boolh:nodup l = r⊢ ⊢ₛ
  wp⟦have seen := ∅;
      do
      let r ←
        forIn l ⟨none, seen⟩ fun x r =>
            have r := r.snd;
            have seen := r;
            have __do_jp := fun seen y =>
              have seen := seen.insert x;
              do
              pure PUnit.unit
              pure (ForInStep.yield ⟨none, seen⟩);
            if x ∈ seen then pure (ForInStep.done ⟨some false, seen⟩)
            else do
              let y ← pure PUnit.unit
              __do_jp seen y
      have seen : Std.HashSet Int := r.snd
      have __do_jp : PUnit → Id Bool := fun y => pure true
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a⟧
    (PostCond.noThrow fun a => { down := a = true ↔ l.Nodup })
  mvcgen
  invariants
  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun xs seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ xs.prefix) ∧ xs.prefix.Nodup⌝)
  with grindAll goals completed! 🐙

The proof has the same succinct structure as for the initial mySum example, because we again offload all proofs to grind and its existing automation around List.Nodup. Therefore, the only difference is in the loop invariant. Since our loop has an early return, we construct the invariant using the helper function Invariant.withEarlyReturn. This function allows us to specify the invariant in three parts:

onReturn ret seen holds after the loop was left through an early return with value ret. In case of nodup, the only value that is ever returned is false, in which case nodup has decided there is a duplicate in the list.
onContinue xs seen is the regular induction step that proves the invariant is preserved each loop iteration. The iteration state is captured by the cursor xs. The given example asserts that the set seen contains all the elements of previous loop iterations and asserts that there were no duplicates so far.
onExcept must hold when the loop throws an exception. There are no exceptions in Id, so we leave it unspecified to use the default. (Exceptions will be discussed at a later point.)

Note that the form mvcgen invariants? will suggest an initial invariant using Invariant.withEarlyReturn, so there is no need to memorize the exact syntax for specifying invariants:

declaration uses 'sorry'example (l : List Int) : nodup l ↔ l.Nodup := byl:List Int⊢ nodup l = true ↔ l.Nodup
  generalize h : nodup l = rl:List Intr:Boolh:nodup l = r⊢ r = true ↔ l.Nodup
  apply Id.of_wp_run_eq hal:List Intr:Boolh:nodup l = r⊢ ⊢ₛ
  wp⟦have seen := ∅;
      do
      let r ←
        forIn l ⟨none, seen⟩ fun x r =>
            have r := r.snd;
            have seen := r;
            have __do_jp := fun seen y =>
              have seen := seen.insert x;
              do
              pure PUnit.unit
              pure (ForInStep.yield ⟨none, seen⟩);
            if x ∈ seen then pure (ForInStep.done ⟨some false, seen⟩)
            else do
              let y ← pure PUnit.unit
              __do_jp seen y
      have seen : Std.HashSet Int := r.snd
      have __do_jp : PUnit → Id Bool := fun y => pure true
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a⟧
    (PostCond.noThrow fun a => { down := a = true ↔ l.Nodup })
  mvcgen Try this:
  [apply] invariants
  ·
    Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝) (onContinue :=
      fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)invariants?inv1l:List Intr:Boolh:nodup l = r⊢ Invariant l (MProd (Option Bool) (Std.HashSet Int)) PostShape.purevc1.step.isTruel:List Intr:Boolh:nodup l = rpref✝:List Intcur✝:Intsuff✝:List Inth✝²:l = pref✝ ++ cur✝ :: suff✝b✝:MProd (Option Bool) (Std.HashSet Int)seen✝:Std.HashSet Int := 
  [Error pretty printing expression: unknown free variable `_uniq.1563`. Falling back to raw printer.]
  MProd.snd.{0} (Option.{0} Bool) (Std.HashSet.{0} Int (instBEqOfDecidableEq.{0} Int Int.instDecidableEq) instHashableInt) _uniq.1563__do_jp✝:Std.HashSet Int → PUnit → Id (ForInStep (MProd (Option Bool) (Std.HashSet Int))) := 
  fun seen y => do
    pure PUnit.unit
    pure (ForInStep.yield ⟨none, seen.insert _fvar.1560⟩)h✝¹:cur✝ ∈ seen✝h✝:(Prod.fst ?inv1 ({ «prefix» := pref✝, suffix := cur✝ :: suff✝, property := ⋯ }, b✝)).down⊢ (Prod.fst ?inv1 ({ «prefix» := l, suffix := [], property := ⋯ }, ⟨some false, seen✝⟩)).downvc2.step.isFalsel:List Intr:Boolh:nodup l = rpref✝:List Intcur✝:Intsuff✝:List Inth✝²:l = pref✝ ++ cur✝ :: suff✝b✝:MProd (Option Bool) (Std.HashSet Int)seen✝:Std.HashSet Int := 
  [Error pretty printing expression: unknown free variable `_uniq.1563`. Falling back to raw printer.]
  MProd.snd.{0} (Option.{0} Bool) (Std.HashSet.{0} Int (instBEqOfDecidableEq.{0} Int Int.instDecidableEq) instHashableInt) _uniq.1563__do_jp✝:Std.HashSet Int → PUnit → Id (ForInStep (MProd (Option Bool) (Std.HashSet Int))) := 
  fun seen y => do
    pure PUnit.unit
    pure (ForInStep.yield ⟨none, seen.insert _fvar.1560⟩)h✝¹:¬cur✝ ∈ seen✝h✝:(Prod.fst ?inv1 ({ «prefix» := pref✝, suffix := cur✝ :: suff✝, property := ⋯ }, b✝)).down⊢ (Prod.fst ?inv1 ({ «prefix» := pref✝ ++ [cur✝], suffix := suff✝, property := ⋯ }, ⟨none, seen✝.insert cur✝⟩)).downvc3.a.prel:List Intr:Boolh:nodup l = r⊢ (Prod.fst ?inv1 ({ «prefix» := [], suffix := l, property := ⋯ }, ⟨none, ∅⟩)).downvc4.a.post.success.h_1l:List Intr:Boolh:nodup l = rr✝:MProd (Option Bool) (Std.HashSet Int)x✝:r✝.fst = noneh✝:(Prod.fst ?inv1 ({ «prefix» := l, suffix := [], property := ⋯ }, r✝)).down⊢ True ↔ l.Nodupvc5.a.post.success.h_2l:List Intr:Boolh:nodup l = rr✝:MProd (Option Bool) (Std.HashSet Int)a✝:Boolx✝:r✝.fst = some a✝h✝:(Prod.fst ?inv1 ({ «prefix» := l, suffix := [], property := ⋯ }, r✝)).down⊢ a✝ = true ↔ l.Nodup <;>inv1l:List Intr:Boolh:nodup l = r⊢ Invariant l (MProd (Option Bool) (Std.HashSet Int)) PostShape.purevc1.step.isTruel:List Intr:Boolh:nodup l = rpref✝:List Intcur✝:Intsuff✝:List Inth✝²:l = pref✝ ++ cur✝ :: suff✝b✝:MProd (Option Bool) (Std.HashSet Int)seen✝:Std.HashSet Int := 
  [Error pretty printing expression: unknown free variable `_uniq.1563`. Falling back to raw printer.]
  MProd.snd.{0} (Option.{0} Bool) (Std.HashSet.{0} Int (instBEqOfDecidableEq.{0} Int Int.instDecidableEq) instHashableInt) _uniq.1563__do_jp✝:Std.HashSet Int → PUnit → Id (ForInStep (MProd (Option Bool) (Std.HashSet Int))) := 
  fun seen y => do
    pure PUnit.unit
    pure (ForInStep.yield ⟨none, seen.insert _fvar.1560⟩)h✝¹:cur✝ ∈ seen✝h✝:(Prod.fst ?inv1 ({ «prefix» := pref✝, suffix := cur✝ :: suff✝, property := ⋯ }, b✝)).down⊢ (Prod.fst ?inv1 ({ «prefix» := l, suffix := [], property := ⋯ }, ⟨some false, seen✝⟩)).downvc2.step.isFalsel:List Intr:Boolh:nodup l = rpref✝:List Intcur✝:Intsuff✝:List Inth✝²:l = pref✝ ++ cur✝ :: suff✝b✝:MProd (Option Bool) (Std.HashSet Int)seen✝:Std.HashSet Int := 
  [Error pretty printing expression: unknown free variable `_uniq.1563`. Falling back to raw printer.]
  MProd.snd.{0} (Option.{0} Bool) (Std.HashSet.{0} Int (instBEqOfDecidableEq.{0} Int Int.instDecidableEq) instHashableInt) _uniq.1563__do_jp✝:Std.HashSet Int → PUnit → Id (ForInStep (MProd (Option Bool) (Std.HashSet Int))) := 
  fun seen y => do
    pure PUnit.unit
    pure (ForInStep.yield ⟨none, seen.insert _fvar.1560⟩)h✝¹:¬cur✝ ∈ seen✝h✝:(Prod.fst ?inv1 ({ «prefix» := pref✝, suffix := cur✝ :: suff✝, property := ⋯ }, b✝)).down⊢ (Prod.fst ?inv1 ({ «prefix» := pref✝ ++ [cur✝], suffix := suff✝, property := ⋯ }, ⟨none, seen✝.insert cur✝⟩)).downvc3.a.prel:List Intr:Boolh:nodup l = r⊢ (Prod.fst ?inv1 ({ «prefix» := [], suffix := l, property := ⋯ }, ⟨none, ∅⟩)).downvc4.a.post.success.h_1l:List Intr:Boolh:nodup l = rr✝:MProd (Option Bool) (Std.HashSet Int)x✝:r✝.fst = noneh✝:(Prod.fst ?inv1 ({ «prefix» := l, suffix := [], property := ⋯ }, r✝)).down⊢ True ↔ l.Nodupvc5.a.post.success.h_2l:List Intr:Boolh:nodup l = rr✝:MProd (Option Bool) (Std.HashSet Int)a✝:Boolx✝:r✝.fst = some a✝h✝:(Prod.fst ?inv1 ({ «prefix» := l, suffix := [], property := ⋯ }, r✝)).down⊢ a✝ = true ↔ l.Nodup sorryAll goals completed! 🐙

The tactic suggests a starting invariant. This starting point will not allow the proof to succeed—after all, if the invariant can be inferred by the system, then there's no need to make the user specify it—but it does provide a reminder of the correct syntax to use for assertions in the current monad:

Try this:
  [apply] invariants
  ·
    Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝) (onContinue :=
      fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)

Now consider the following direct (and excessively golfed) proof without mvcgen:

theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := byl:List Int⊢ nodup l = true ↔ l.Nodup
  rw [nodup]l:List Int⊢ (have seen := ∅;
      do
      let r ←
        forIn l ⟨none, seen⟩ fun x r =>
            have r := r.snd;
            have seen := r;
            have __do_jp := fun seen y =>
              have seen := seen.insert x;
              do
              pure PUnit.unit
              pure (ForInStep.yield ⟨none, seen⟩);
            if x ∈ seen then pure (ForInStep.done ⟨some false, seen⟩)
            else do
              let y ← pure PUnit.unit
              __do_jp seen y
      have seen : Std.HashSet Int := r.snd
      have __do_jp : PUnit → Id Bool := fun y => pure true
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a).run =
    true ↔
  l.Nodup
  generalize hseen : (∅ : Std.HashSet Int) = seenl:List Intseen:Std.HashSet Inthseen:∅ = seen⊢ (have seen := seen;
      do
      let r ←
        forIn l ⟨none, seen⟩ fun x r =>
            have r := r.snd;
            have seen := r;
            have __do_jp := fun seen y =>
              have seen := seen.insert x;
              do
              pure PUnit.unit
              pure (ForInStep.yield ⟨none, seen⟩);
            if x ∈ seen then pure (ForInStep.done ⟨some false, seen⟩)
            else do
              let y ← pure PUnit.unit
              __do_jp seen y
      have seen : Std.HashSet Int := r.snd
      have __do_jp : PUnit → Id Bool := fun y => pure true
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a).run =
    true ↔
  l.Nodup
  change ?lhs ↔ l.Nodupl:List Intseen:Std.HashSet Inthseen:∅ = seen⊢ (have seen := seen;
      do
      let r ←
        forIn l ⟨none, seen⟩ fun x r =>
            have r := r.snd;
            have seen := r;
            have __do_jp := fun seen y =>
              have seen := seen.insert x;
              do
              pure PUnit.unit
              pure (ForInStep.yield ⟨none, seen⟩);
            if x ∈ seen then pure (ForInStep.done ⟨some false, seen⟩)
            else do
              let y ← pure PUnit.unit
              __do_jp seen y
      have seen : Std.HashSet Int := r.snd
      have __do_jp : PUnit → Id Bool := fun y => pure true
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a).run =
    true ↔
  l.Nodup
  suffices h : ?lhs ↔ l.Nodup ∧ ∀ x ∈ l, x ∉ seen byl:List Intseen:Std.HashSet Inthseen:∅ = seenh:(have seen := _fvar.250;
      do
      let r ←
        forIn _fvar.66 ⟨none, seen⟩ fun x r =>
            have r := r.snd;
            have seen := r;
            have __do_jp := fun seen y =>
              have seen := seen.insert x;
              do
              pure PUnit.unit
              pure (ForInStep.yield ⟨none, seen⟩);
            if x ∈ seen then pure (ForInStep.done ⟨some false, seen⟩)
            else do
              let y ← pure PUnit.unit
              __do_jp seen y
      have seen : Std.HashSet Int := r.snd
      have __do_jp : PUnit → Id Bool := fun y => pure true
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a).run =
    true ↔
  List.Nodup _fvar.66 ∧ ∀ (x : Int), x ∈ _fvar.66 → ¬x ∈ _fvar.250 := 
  ?_mvar.337⊢ (have seen := seen;
      do
      let r ←
        forIn l ⟨none, seen⟩ fun x r =>
            have r := r.snd;
            have seen := r;
            have __do_jp := fun seen y =>
              have seen := seen.insert x;
              do
              pure PUnit.unit
              pure (ForInStep.yield ⟨none, seen⟩);
            if x ∈ seen then pure (ForInStep.done ⟨some false, seen⟩)
            else do
              let y ← pure PUnit.unit
              __do_jp seen y
      have seen : Std.HashSet Int := r.snd
      have __do_jp : PUnit → Id Bool := fun y => pure true
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a).run =
    true ↔
  l.Nodup grindAll goals completed! 🐙
  clear hseenl:List Intseen:Std.HashSet Int⊢ (have seen := seen;
      do
      let r ←
        forIn l ⟨none, seen⟩ fun x r =>
            have r := r.snd;
            have seen := r;
            have __do_jp := fun seen y =>
              have seen := seen.insert x;
              do
              pure PUnit.unit
              pure (ForInStep.yield ⟨none, seen⟩);
            if x ∈ seen then pure (ForInStep.done ⟨some false, seen⟩)
            else do
              let y ← pure PUnit.unit
              __do_jp seen y
      have seen : Std.HashSet Int := r.snd
      have __do_jp : PUnit → Id Bool := fun y => pure true
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a).run =
    true ↔
  l.Nodup ∧ ∀ (x : Int), x ∈ l → ¬x ∈ seen
  induction l generalizing seen with grind [Id.run_pure, Id.run_bind]All goals completed! 🐙

Some observations:

The proof is even shorter than the one with mvcgen.
The use of generalize to generalize the accumulator relies on there being exactly one occurrence of ∅ to generalize. If that were not the case, we would have to copy parts of the program into the proof. This is a no-go for larger functions.
grind splits along the control flow of the function and reasons about Id, given the right lemmas. While this works for Id.run_pure and Id.run_bind, it would not work for Id.run_seq, for example, because that lemma is not E-matchable. If grind would fail, we would be forced to do all the control flow splitting and monadic reasoning by hand until grind could pick up again.

The usual way to avoid replicating the control flow of a definition in a proof is to use the fun_cases or fun_induction tactics. Unfortunately, fun_cases does not help with control flow inside a forIn application. The mvcgen tactic, on the other hand, ships with support for many forIn implementations. It can easily be extended (with @[spec] annotations) to support custom forIn implementations. Furthermore, an mvcgen-powered proof will never need to copy any part of the original program.

18.1.4. Compositional Reasoning About Effectful Programs Using Hoare Triples

The previous examples reasoned about functions defined using Id.run Lean.Parser.Term.do : termdo <prog> to make use of local mutability and early return in <prog>. However, real-world programs often use Lean.Parser.Term.do : termdo notation and monads M to hide away state and failure conditions as implicit “effects”. In this use case, functions usually omit the M.run. Instead they have a monadic return type M α and compose well with other functions of that return type. In other words, the monad is part of the function's interface, not merely its implementation.

Here is an example involving a stateful function mkFresh that returns auto-incremented counter values:

structure Supply where
  counter : Nat

def mkFresh : StateM Supply Nat := do
  let n ← (·.counter) <$> get
  modify fun s => { s with counter := s.counter + 1 }
  pure n

def mkFreshN (n : Nat) : StateM Supply (List Nat) := do
  let mut acc := #[]
  for _ in [:n] do
    acc := acc.push (← mkFresh)
  pure acc.toList

mkFreshN n returns n “fresh” numbers, modifying the internal Supply state through mkFresh. Here, “fresh” refers to all previously generated numbers being distinct from the next generated number. We can formulate and prove a correctness property mkFreshN_correct in terms of List.Nodup: the returned list of numbers should contain no duplicates. In this proof, StateM.of_wp_run'_eq serves the same role that Id.of_wp_run_eq did in the preceding examples.

theorem mkFreshN_correct (n : Nat) : ((mkFreshN n).run' s).Nodup := bys:Supplyn:Nat⊢ List.Nodup (StateT.run' (mkFreshN n) s)
  -- Focus on `(mkFreshN n).run' s`.
  generalize h : (mkFreshN n).run' s = xs:Supplyn:Natx:Id (List Nat)h:StateT.run' (mkFreshN n) s = x⊢ List.Nodup x
  apply StateM.of_wp_run'_eq has:Supplyn:Natx:Id (List Nat)h:StateT.run' (mkFreshN n) s = x⊢ ⊢ₛ wp⟦mkFreshN n⟧ (PostCond.noThrow fun a => ⌜a.Nodup⌝) s
  -- Show something about monadic program `mkFresh n`.
  -- The `mkFreshN` and `mkFresh` arguments to `mvcgen` add to an
  -- internal `simp` set and makes `mvcgen` unfold these definitions.
  mvcgen [mkFreshN, mkFresh]
  invariants
  -- Invariant: The counter is larger than any accumulated number,
  --            and all accumulated numbers are distinct.
  -- Note that the invariant may refer to the state through function
  -- argument `state : Supply`. Since the next number to accumulate is
  -- the counter, it is distinct to all accumulated numbers.
  · ⇓⟨xs, acc⟩ state =>
      ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝
  with grindAll goals completed! 🐙

18.1.4.1. Hoare Triples

A Hoare triple (Hoare, 1969)C. A. R. Hoare (1969). “An Axiomatic Basis for Computer Programming”. Communications of the ACM.12 10pp. 576–583. consists of a precondition, a statement, and a postcondition; it asserts that if the precondition holds, then the postcondition holds after running the statement. In Lean syntax, this is written ⦃ P ⦄ prog ⦃ Q ⦄, where P is the precondition, prog : m α is the statement, and Q is the postcondition. P and Q are written in an assertion language that is determined by the specific monad m.In particular, monad's instance of the type class WP specifies the ways in which assertions may refer to the monad's state or the exceptions it may throw.

Specifications as Hoare triples are compositional because they allow statements to be sequenced. Given ⦃P⦄ stmt1 ⦃Q⦄ and ⦃P'⦄ stmt2 ⦃Q'⦄, if Q implies P' then ⦃P⦄ (do stmt1; stmt2) ⦃Q'⦄. Just as proofs about ordinary functions can rely on lemmas about the functions that they call, proofs about monadic programs can use lemmas that are specified in terms of Hoare triples.

One suitable specification for mkFresh as a Hoare triple is this translation of mkFreshN_correct:

⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄

Corner brackets embed propositions into the monadic assertion language, so ⌜p⌝ is the assertion of the proposition p. The precondition ⌜True⌝ asserts that True is true; this trivial precondition is used to state that the specification imposes no requirements on the state in which it is called. The postcondition states that the result value is a list with no duplicate elements.

A specification for the single-step mkFresh describes its effects on the monad's state:

∀ (c : Nat),
⦃fun state => ⌜state.counter = c⌝⦄
mkFresh
⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄

When working in a state monad, preconditions may be parameterized over the value of the state prior to running the code. Here, the universally quantified Nat is used to relate the initial state to the final state; the precondition is used to connect it to the initial state. Similarly, the postcondition may also accept the final state as a parameter. This Hoare triple states:

If c refers to the Supply.counter field of the Supply prestate, then running mkFresh returns c and modifies the Supply.counter of the poststate to be larger than c.

Note that this specification is lossy: mkFresh could increment its state by an arbitrary non-negative amount and still satisfy the specification. This is good, because specifications may abstract over uninteresting implementation details, ensuring resilient and small proofs.

Hoare triples are defined in terms of a logic of stateful predicates plus a weakest precondition semantics wp⟦prog⟧ that translates monadic programs into this logic. A weakest precondition semantics is an interpretation of programs as mappings from postconditions to the weakest precondition that the program would require to ensure the postcondition; in this interpretation, programs are understood as predicate transformers. The Hoare triple syntax is notation for Std.Do.Triple:

def Triple [WP m ps] {α : Type u} (prog : m α)
    (P : Assertion ps) (Q : PostCond α ps) : Prop :=
  P ⊢ₛ wp⟦prog⟧ Q

The WP type class maps a monad m to its PostShape ps, and this PostShape governs the exact shape of the Std.Do.Triple. Many of the standard monad transformers such as StateT, ReaderT and ExceptT come with a canonical WP instance. For example, StateT σ comes with a WP instance that adds a σ argument to every Assertion. Stateful entailment ⊢ₛ eta-expands through these additional σ arguments. For StateM programs, the following type is definitionally equivalent to Std.Do.Triple:

def StateMTriple {α σ : Type u} (prog : StateM σ α)
    (P : σ → ULift Prop) (Q : (α → σ → ULift Prop) × PUnit) : Prop :=
  ∀ s, (P s).down → let (a, s') := prog.run s; (Q.1 a s').down

The common postcondition notation ⇓ r => ... injects an assertion of type α → Assertion ps into PostCond α ps (the ⇓ is meant to be parsed like fun); in case of StateM by adjoining it with an empty tuple PUnit.unit. The shape of postconditions becomes more interesting once exceptions enter the picture. The notation ⌜p⌝ embeds a pure hypotheses p into a stateful assertion. Vice versa, any stateful hypothesis P is called pure if it is equivalent to ⌜p⌝ for some p. Pure, stateful hypotheses may be freely moved into the regular Lean context and back. (This can be done manually with the mpure tactic.)

18.1.4.2. Composing Specifications

Nested unfolding of definitions as in mvcgen [mkFreshN, mkFresh] is quite blunt but effective for small programs. A more compositional way is to develop individual specification lemmas for each monadic function. A specification lemma is a Hoare triple that is automatically used during verification condition generation to obtain the pre- and postconditions of each statement in a Lean.Parser.Term.do : termdo-block. When the system cannot automatically prove that the postcondition of one statement implies the precondition of the next, then this missing reasoning step becomes a verification condition.

Specification lemmas can either be passed as arguments to mvcgen or registered in a global (or scoped, or local) database of specifications using the @[spec] attribute:

@[spec]
theorem mkFresh_spec (c : Nat) :
    ⦃fun state => ⌜state.counter = c⌝⦄
    mkFresh
    ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := byc:Nat⊢ ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh ⦃PostCond.noThrow fun r state => ⌜r = c ∧ c < state.counter⌝⦄
  -- Unfold `mkFresh` and blast away:
  mvcgen [mkFresh] with grindAll goals completed! 🐙

@[spec]
theorem mkFreshN_spec (n : Nat) :
    ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := byn:Nat⊢ ⦃⌜True⌝⦄ mkFreshN n ⦃PostCond.noThrow fun r => ⌜r.Nodup⌝⦄
  -- `mvcgen [mkFreshN, mkFresh_spec]` if `mkFresh_spec` were not
  -- registered with `@[spec]`
  mvcgen [mkFreshN]
  invariants
  -- As before:
  · ⇓⟨xs, acc⟩ state =>
      ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝
  with grindAll goals completed! 🐙

The original correctness theorem can now be proved using mvcgen alone:

theorem mkFreshN_correct_compositional (n : Nat) :
    ((mkFreshN n).run' s).Nodup := bys:Supplyn:Nat⊢ List.Nodup (StateT.run' (mkFreshN n) s)
  generalize h : (mkFreshN n).run' s = xs:Supplyn:Natx:Id (List Nat)h:StateT.run' (mkFreshN n) s = x⊢ List.Nodup x
  apply StateM.of_wp_run'_eq has:Supplyn:Natx:Id (List Nat)h:StateT.run' (mkFreshN n) s = x⊢ ⊢ₛ wp⟦mkFreshN n⟧ (PostCond.noThrow fun a => ⌜a.Nodup⌝) s
  mvcgenAll goals completed! 🐙

The specification lemma mkFreshN_spec is automatically used by mvcgen.

18.1.4.3. An Advanced Note About Pure Preconditions and a Notion of Frame Rule

This subsection is a bit of a digression and can be skipped on first reading.

Say the specification for some Aeneas-inspired monadic addition function x +? y : M UInt8 has the requirement that the addition won't overflow, that is, h : x.toNat + y.toNat ≤ UInt8.size. Should this requirement be encoded as a regular Lean hypothesis of the specification (add_spec_hyp) or should this requirement be encoded as a pure precondition of the Hoare triple, using ⌜·⌝ notation (add_spec_pre)?

theorem add_spec_hyp (x y : UInt8)
    (h : x.toNat + y.toNat ≤ UInt8.size) :
    ⦃⌜True⌝⦄ x +? y ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := …

theorem add_spec_pre (x y : UInt8) :
    ⦃⌜x.toNat + y.toNat ≤ UInt8.size⌝⦄
    x +? y
    ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := …

The first approach is advisable, although it should not make a difference in practice. The VC generator will move pure hypotheses from the stateful context into the regular Lean context, so the second form turns effectively into the first form. This is referred to as framing hypotheses (cf. the mpure and mframe tactics). Hypotheses in the Lean context are part of the immutable frame of the stateful logic, because in contrast to stateful hypotheses they survive the rule of consequence.

18.1.5. Monad Transformers and Lifting

Real-world programs often use monads that are built from multiple monad transformers, with operations being frequently lifted from one monad to another. Verification of these programs requires taking this into account. We can tweak the previous example to demonstrate this.

Now, there is an application with two separate monads, both built using transformers:

abbrev CounterM := StateT Supply (ReaderM String)

abbrev AppM := StateT Bool CounterM

Instead of using StateM Supply, mkFresh uses CounterM:

def mkFresh : CounterM Nat := do
  let n ← (·.counter) <$> get
  modify fun s => { s with counter := s.counter + 1 }
  pure n

mkFreshN is defined in terms of AppM, which includes multiple states and a reader effect. The definition of mkFreshN lifts mkFresh into AppM:

def mkFreshN (n : Nat) : AppM (List Nat) := do
  let mut acc := #[]
  for _ in [:n] do
    let n ← mkFresh
    acc := acc.push n
  return acc.toList

Then the mvcgen-based proof goes through unchanged:

@[spec]
theorem declaration uses 'sorry'mkFresh_spec (c : Nat) :
    ⦃fun state => ⌜state.counter = c⌝⦄
    mkFresh
    ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := byc:Nat⊢ ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh ⦃PostCond.noThrow fun r state => ⌜r = c ∧ c < state.counter⌝⦄
  --TODO: mvcgen [mkFresh] with grind
  sorryAll goals completed! 🐙

@[spec]
theorem mkFreshN_spec (n : Nat) :
    ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := byn:Nat⊢ ⦃⌜True⌝⦄ mkFreshN n ⦃PostCond.noThrow fun r => ⌜r.Nodup⌝⦄
  -- `liftCounterM` here ensures unfolding
  mvcgen [mkFreshN]
  invariants
  · ⇓⟨xs, acc⟩ _ state =>
      ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝
  with grindAll goals completed! 🐙

The WPMonad type class asserts that wp⟦prog⟧ distributes over the Monad operations (“monad morphism”). This proof might not look much more exciting than when only a single monad was involved. However, under the radar of the user the proof builds on a cascade of specifications for MonadLift instances.

18.1.6. Exceptions

If let mut is the Lean.Parser.Term.do : termdo-equivalent of StateT, then early Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`, skipping any further statements. Note that uses of the `do` keyword in other syntax like in `for _ in _ do` do not constitute a surrounding block in this sense; in supported editors, the corresponding `do` keyword of the surrounding block is highlighted when hovering over `return`. `return` not followed by a term starting on the same line is equivalent to `return ()`.return is the equivalent of ExceptT. We have seen how the mvcgen copes with StateT; here we will look at the program logic's support for ExceptT.

Exceptions are the reason why the type of postconditions PostCond α ps is not simply a single condition of type α → Assertion ps for the success case. To see why, suppose the latter was the case, and suppose that program prog throws an exception in a prestate satisfying P. Should we be able to prove ⦃P⦄ prog ⦃⇓ r => Q' r⦄? (Recall that ⇓ is grammatically similar to fun.) There is no result r, so it is unclear what this proof means for Q'!

So there are two reasonable options, inspired by non-termination in traditional program logics:

The total correctness interpretation: ⦃P⦄ prog ⦃⇓ r => Q' r⦄ asserts that, given P holds, then prog terminates and Q' holds for the result.
The partial correctness interpretation: ⦃P⦄ prog ⦃⇓ r => Q' r⦄ asserts that, given P holds, and if prog terminates then Q' holds for the result.

The notation ⇓ r => Q' r has the total interpretation, while ⇓? r => Q' r has the partial interpretation.

syntaxPostconditions

term ::= ...
    | A postcondition expressing total correctness.
That is, it expresses that the asserted computation finishes without throwing an exception
*and* the result satisfies the given predicate `p`.
⇓ term* => term

A postcondition expressing total correctness. That is, it expresses that the asserted computation finishes without throwing an exception and the result satisfies the given predicate p.

term ::= ...
    | A postcondition expressing partial correctness.
That is, it expresses that *if* the asserted computation finishes without throwing an exception
*then* the result satisfies the given predicate `p`.
Nothing is asserted when the computation throws an exception.
⇓? term* => term

A postcondition expressing partial correctness. That is, it expresses that if the asserted computation finishes without throwing an exception then the result satisfies the given predicate p. Nothing is asserted when the computation throws an exception.

So in the running example, ⦃P⦄ prog ⦃⇓ r => Q' r⦄ is unprovable, but ⦃P⦄ prog ⦃⇓? r => Q' r⦄ is trivially provable. However, the binary choice suggests that there is actually a spectrum of correctness properties to express. The notion of postconditions PostCond in Std.Do supports this spectrum.

For example, suppose that our Supply of fresh numbers is bounded and we want to throw an exception if the supply is exhausted. Then mkFreshN should throw an exception only if the supply is indeed exhausted, as in this implementation:

structure Supply where
  counter : Nat
  limit : Nat
  property : counter ≤ limit

def mkFresh : EStateM String Supply Nat := do
  let supply ← get
  if h : supply.counter = supply.limit then
    throw s!"Supply exhausted: {supply.counter} = {supply.limit}"
  else
    let n := supply.counter
    have := supply.property
    set { supply with counter := n + 1, property := bysupply:Supplyh:¬supply.counter = supply.limitn:Nat := 
  [Error pretty printing expression: unknown free variable `_uniq.592`. Falling back to raw printer.]
  Exceptions.Supply.counter _uniq.592this:[Error pretty printing expression: unknown free variable `_uniq.592`. Falling back to raw printer.]
LE.le.{0} Nat instLENat (Exceptions.Supply.counter _uniq.592) (Exceptions.Supply.limit _uniq.592) := 
  [Error pretty printing expression: unknown free variable `_uniq.592`. Falling back to raw printer.]
  Exceptions.Supply.property _uniq.592⊢ n + 1 ≤ supply.limit grindAll goals completed! 🐙 }
    pure n

The following correctness property expresses this:

@[spec]
theorem mkFresh_spec (c : Nat) :
    ⦃fun state => ⌜state.counter = c⌝⦄
    mkFresh
    ⦃post⟨fun r state => ⌜r = c ∧ c < state.counter⌝,
          fun _ state => ⌜c = state.counter ∧ c = state.limit⌝⟩⦄ := byc:Nat⊢ ⦃fun state => ⌜state.counter = c⌝⦄
  mkFresh ⦃(fun r state => ⌜r = c ∧ c < state.counter⌝, fun x state => ⌜c = state.counter ∧ c = state.limit⌝, ())⦄
  mvcgen [mkFresh] with grindAll goals completed! 🐙

In this property, the postcondition has two branches: the first covers successful termination, and the second applies when an exception is thrown. The monad's WP instance determines both how many branches the postcondition may have and the number of parameters in each branch: each exception that might be triggered gives rise to an extra branch, and each state gives an extra parameter.

In this new monad, mkFreshN's implementation is unchanged, except for the type signature:

def mkFreshN (n : Nat) : EStateM String Supply (List Nat) := do
  let mut acc := #[]
  for _ in [:n] do
    acc := acc.push (← mkFresh)
  pure acc.toList

However, the specification lemma must account for both successful termination and exceptions being thrown, in both the postcondition and the loop invariant:

@[spec]
theorem mkFreshN_spec (n : Nat) :
    ⦃⌜True⌝⦄
    mkFreshN n
    ⦃post⟨fun r => ⌜r.Nodup⌝,
          fun _msg state => ⌜state.counter = state.limit⌝⟩⦄ := byn:Nat⊢ ⦃⌜True⌝⦄ mkFreshN n ⦃(fun r => ⌜r.Nodup⌝, fun _msg state => ⌜state.counter = state.limit⌝, ())⦄
  mvcgen [mkFreshN]
  invariants
  · post⟨fun ⟨xs, acc⟩ state =>
           ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝,
         fun _msg state => ⌜state.counter = state.limit⌝⟩
  with grindAll goals completed! 🐙

The final proof uses the specification lemmas and mvcgen, just as before:

theorem mkFreshN_correct (n : Nat) :
    match (mkFreshN n).run s with
    | .ok    l _  => l.Nodup
    | .error _ s' => s'.counter = s'.limit := bys:Supplyn:Nat⊢ match (mkFreshN n).run s with
| EStateM.Result.ok l a => l.Nodup
| EStateM.Result.error a s' => s'.counter = s'.limit
  generalize h : (mkFreshN n).run s = xs:Supplyn:Natx:EStateM.Result String Supply (List Nat)h:(mkFreshN n).run s = x⊢ match x with
| EStateM.Result.ok l a => l.Nodup
| EStateM.Result.error a s' => s'.counter = s'.limit
  apply EStateM.of_wp_run_eq has:Supplyn:Natx:EStateM.Result String Supply (List Nat)h:(mkFreshN n).run s = x⊢ ⊢ₛ
  wp⟦mkFreshN n⟧
    (fun a s' =>
      ⌜match EStateM.Result.ok a s' with
        | EStateM.Result.ok l a => l.Nodup
        | EStateM.Result.error a s' => s'.counter = s'.limit⌝,
      fun e s' =>
      ⌜match EStateM.Result.error e s' with
        | EStateM.Result.ok l a => l.Nodup
        | EStateM.Result.error a s' => s'.counter = s'.limit⌝,
      ())
    s
  mvcgenAll goals completed! 🐙

Just as any StateT σ-like monad transformer gives rise to a PostShape.arg σ layer in the ps that WP maps into, any ExceptT ε-like layer gives rise to a PostShape.except ε layer.

Every PostShape.arg σ adds another σ → ... layer to the language of Assertions. Every PostShape.except ε leaves the Assertion language unchanged, but adds another exception condition to the postcondition. Hence the WP instance for EStateM ε σ maps to the PostShape PostShape.except ε (.arg σ .pure), just as for ExceptT ε (StateM σ).

18.1.7. Extending `mvcgen` With Support for Custom Monads

The mvcgen framework is designed to be extensible. None of the monads presented so far have in any way been hard-coded into mvcgen. Rather, mvcgen relies on instances of the WP and WPMonad type class and user-provided specifications to generate verification conditions.

The WP instance defines the weakest precondition interpretation of a monad m into a predicate transformer PredTrans ps, and the matching WPMonad instance asserts that this translation distributes over the Monad operations.

structure

Std.Do.PredTrans.{u} (ps : Std.Do.PostShape) (α : Type u) : Type u
Std.Do.PredTrans.{u}
  (ps : Std.Do.PostShape) (α : Type u) :
  Type u

The type of predicate transformers for a given ps : PostShape and return type α : Type. A predicate transformer x : PredTrans ps α is a function that takes a postcondition Q : PostCond α ps and returns a precondition x.apply Q : Assertion ps.

Constructor

Std.Do.PredTrans.mk.{u}

Fields

apply : Std.Do.PostCond α ps → Std.Do.Assertion ps

Apply the predicate transformer to a postcondition.

conjunctive : Std.Do.PredTrans.Conjunctive self.apply

The predicate transformer is conjunctive: t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂. So the stronger the postcondition, the stronger the resulting precondition.

type class

Std.Do.WP.{u, v} (m : Type u → Type v)
  (ps : outParam Std.Do.PostShape) : Type (max (u + 1) v)
Std.Do.WP.{u, v} (m : Type u → Type v)
  (ps : outParam Std.Do.PostShape) :
  Type (max (u + 1) v)

A weakest precondition interpretation of a monadic program x : m α in terms of a predicate transformer PredTrans ps α. The monad m determines ps : PostShape. See the module comment for more details.

Instance Constructor

Std.Do.WP.mk.{u, v}

Methods

wp : {α : Type u} → m α → Std.Do.PredTrans ps α

Interpret a monadic program x : m α in terms of a predicate transformer PredTrans ps α.

syntaxWeakest Preconditions

term ::= ...
    | `wp⟦x⟧ Q` is defined as `(WP.wp x).apply Q`. wp⟦ term ⟧

type class

Std.Do.WPMonad.{u, v} (m : Type u → Type v)
  (ps : outParam Std.Do.PostShape) [Monad m] : Type (max (u + 1) v)
Std.Do.WPMonad.{u, v}
  (m : Type u → Type v)
  (ps : outParam Std.Do.PostShape)
  [Monad m] : Type (max (u + 1) v)

A WP that is also a monad morphism, preserving pure and bind. (They all are.)

Instance Constructor

Std.Do.WPMonad.mk.{u, v}

Extends

LawfulMonad m
Std.Do.WP m ps

Methods

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

Inherited from

LawfulMonad m
Std.Do.WP m ps

id_map : ∀ {α : Type u} (x : m α), id <$> x = x

Inherited from

LawfulMonad m
Std.Do.WP m ps

comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x

Inherited from

LawfulMonad m
Std.Do.WP m ps

seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), x <* y = Function.const β <$> x <*> y

Inherited from

LawfulMonad m
Std.Do.WP m ps

seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), x *> y = Function.const α id <$> x <*> y

Inherited from

LawfulMonad m
Std.Do.WP m ps

pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), pure g <*> x = g <$> x

Inherited from

LawfulMonad m
Std.Do.WP m ps

map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)

Inherited from

LawfulMonad m
Std.Do.WP m ps

seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g

Inherited from

LawfulMonad m
Std.Do.WP m ps

seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x

Inherited from

LawfulMonad m
Std.Do.WP m ps

bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α),
  (do
      let a ← x
      pure (f a)) =
    f <$> x

Inherited from

LawfulMonad m
Std.Do.WP m ps

bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α),
  (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x

Inherited from

LawfulMonad m
Std.Do.WP m ps

pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

Inherited from

LawfulMonad m
Std.Do.WP m ps

bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

Inherited from

LawfulMonad m
Std.Do.WP m ps

wp : {α : Type u} → m α → Std.Do.PredTrans ps α

Inherited from

LawfulMonad m
Std.Do.WP m ps

wp_pure : ∀ {α : Type u} (a : α), Std.Do.wp (pure a) = pure a

WP.wp preserves pure.

wp_bind : ∀ {α β : Type u} (x : m α) (f : α → m β),
  (Std.Do.wp do
      let a ← x
      f a) =
    do
    let a ← Std.Do.wp x
    Std.Do.wp (f a)

WP.wp preserves bind.

Suppose one wants to use mvcgen to generate verification conditions for programs generated by Aeneas. Aeneas translates Rust programs into Lean programs in the following Result monad:

inductive Error where
  | integerOverflow: Error
  -- ... more error kinds ...

inductive Result (α : Type u) where
  | ok (v: α): Result α
  | fail (e: Error): Result α
  | div

There are both Monad Result and LawfulMonad Result instances. Supporting this monad in mvcgen is a matter of:

Adding WP and WPMonad instances for Result
Registering specification lemmas for the translation of basic Rust primitives such as addition etc.

The WP instance for Result specifies a postcondition shape .except Error .pure because there are no state-like effects, but there is a single exception of type Error. The WP instance translates programs in Result α to predicate transformers in PredTrans ps α. That is, a function in PostCond α ps → Assertion ps, mapping a postcondition to its weakest precondition. The implementation of WP.wp reuses the implementation for Except Error for two of its cases, and maps diverging programs to False. The instance is named so that it can be more easily unfolded in proofs about it.

instance Result.instWP : WP Result (.except Error .pure) where
  wp
    | .ok v => wp (pure v : Except Error _)
    | .fail e => wp (throw e : Except Error _)
    | .div => PredTrans.const ⌜False⌝

The implementation of WP.wp should distribute over the basic monad operators:

instance : WPMonad Result (.except Error .pure) where
  wp_pure := by⊢ ∀ {α : Type} (a : α), wp (pure a) = pure a
    introsα✝:Typea✝:α✝⊢ wp (pure a✝) = pure a✝
    ext Qapply.a.hα✝:Typea✝:α✝Q:PostCond α✝ (PostShape.except Error PostShape.pure)⊢ (wp⟦pure a✝⟧ Q).down ↔ ((pure a✝).apply Q).down
    simp [wp, PredTrans.pure, pure, Except.pure, Id.run]All goals completed! 🐙
  wp_bind x f := byα✝:Typeβ✝:Typex:Result α✝f:α✝ → Result β✝⊢ (wp do
    let a ← x
    f a) =
  do
  let a ← wp x
  wp (f a)
    simp only [Result.instWP, bind]α✝:Typeβ✝:Typex:Result α✝f:α✝ → Result β✝⊢ (match
    match x with
    | Result.ok v => f v
    | Result.fail e => Result.fail e
    | Result.div => Result.div with
  | Result.ok v => wp (pure v)
  | Result.fail e => wp (throw e)
  | Result.div => PredTrans.const ⌜False⌝) =
  (match x with
      | Result.ok v => wp (pure v)
      | Result.fail e => wp (throw e)
      | Result.div => PredTrans.const ⌜False⌝).bind
    fun a =>
    match f a with
    | Result.ok v => wp (pure v)
    | Result.fail e => wp (throw e)
    | Result.div => PredTrans.const ⌜False⌝
    ext Qapply.a.hα✝:Typeβ✝:Typex:Result α✝f:α✝ → Result β✝Q:PostCond β✝ (PostShape.except Error PostShape.pure)⊢ ((match
          match x with
          | Result.ok v => f v
          | Result.fail e => Result.fail e
          | Result.div => Result.div with
        | Result.ok v => wp (pure v)
        | Result.fail e => wp (throw e)
        | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down ↔
  (((match x with
            | Result.ok v => wp (pure v)
            | Result.fail e => wp (throw e)
            | Result.div => PredTrans.const ⌜False⌝).bind
          fun a =>
          match f a with
          | Result.ok v => wp (pure v)
          | Result.fail e => wp (throw e)
          | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down
    cases xapply.a.h.okα✝:Typeβ✝:Typef:α✝ → Result β✝Q:PostCond β✝ (PostShape.except Error PostShape.pure)v✝:α✝⊢ ((match
          match Result.ok v✝ with
          | Result.ok v => f v
          | Result.fail e => Result.fail e
          | Result.div => Result.div with
        | Result.ok v => wp (pure v)
        | Result.fail e => wp (throw e)
        | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down ↔
  (((match Result.ok v✝ with
            | Result.ok v => wp (pure v)
            | Result.fail e => wp (throw e)
            | Result.div => PredTrans.const ⌜False⌝).bind
          fun a =>
          match f a with
          | Result.ok v => wp (pure v)
          | Result.fail e => wp (throw e)
          | Result.div => PredTrans.const ⌜False⌝).apply
      Q).downapply.a.h.failα✝:Typeβ✝:Typef:α✝ → Result β✝Q:PostCond β✝ (PostShape.except Error PostShape.pure)e✝:Error⊢ ((match
          match Result.fail e✝ with
          | Result.ok v => f v
          | Result.fail e => Result.fail e
          | Result.div => Result.div with
        | Result.ok v => wp (pure v)
        | Result.fail e => wp (throw e)
        | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down ↔
  (((match Result.fail e✝ with
            | Result.ok v => wp (pure v)
            | Result.fail e => wp (throw e)
            | Result.div => PredTrans.const ⌜False⌝).bind
          fun a =>
          match f a with
          | Result.ok v => wp (pure v)
          | Result.fail e => wp (throw e)
          | Result.div => PredTrans.const ⌜False⌝).apply
      Q).downapply.a.h.divα✝:Typeβ✝:Typef:α✝ → Result β✝Q:PostCond β✝ (PostShape.except Error PostShape.pure)⊢ ((match
          match Result.div with
          | Result.ok v => f v
          | Result.fail e => Result.fail e
          | Result.div => Result.div with
        | Result.ok v => wp (pure v)
        | Result.fail e => wp (throw e)
        | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down ↔
  (((match Result.div with
            | Result.ok v => wp (pure v)
            | Result.fail e => wp (throw e)
            | Result.div => PredTrans.const ⌜False⌝).bind
          fun a =>
          match f a with
          | Result.ok v => wp (pure v)
          | Result.fail e => wp (throw e)
          | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down <;>apply.a.h.okα✝:Typeβ✝:Typef:α✝ → Result β✝Q:PostCond β✝ (PostShape.except Error PostShape.pure)v✝:α✝⊢ ((match
          match Result.ok v✝ with
          | Result.ok v => f v
          | Result.fail e => Result.fail e
          | Result.div => Result.div with
        | Result.ok v => wp (pure v)
        | Result.fail e => wp (throw e)
        | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down ↔
  (((match Result.ok v✝ with
            | Result.ok v => wp (pure v)
            | Result.fail e => wp (throw e)
            | Result.div => PredTrans.const ⌜False⌝).bind
          fun a =>
          match f a with
          | Result.ok v => wp (pure v)
          | Result.fail e => wp (throw e)
          | Result.div => PredTrans.const ⌜False⌝).apply
      Q).downapply.a.h.failα✝:Typeβ✝:Typef:α✝ → Result β✝Q:PostCond β✝ (PostShape.except Error PostShape.pure)e✝:Error⊢ ((match
          match Result.fail e✝ with
          | Result.ok v => f v
          | Result.fail e => Result.fail e
          | Result.div => Result.div with
        | Result.ok v => wp (pure v)
        | Result.fail e => wp (throw e)
        | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down ↔
  (((match Result.fail e✝ with
            | Result.ok v => wp (pure v)
            | Result.fail e => wp (throw e)
            | Result.div => PredTrans.const ⌜False⌝).bind
          fun a =>
          match f a with
          | Result.ok v => wp (pure v)
          | Result.fail e => wp (throw e)
          | Result.div => PredTrans.const ⌜False⌝).apply
      Q).downapply.a.h.divα✝:Typeβ✝:Typef:α✝ → Result β✝Q:PostCond β✝ (PostShape.except Error PostShape.pure)⊢ ((match
          match Result.div with
          | Result.ok v => f v
          | Result.fail e => Result.fail e
          | Result.div => Result.div with
        | Result.ok v => wp (pure v)
        | Result.fail e => wp (throw e)
        | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down ↔
  (((match Result.div with
            | Result.ok v => wp (pure v)
            | Result.fail e => wp (throw e)
            | Result.div => PredTrans.const ⌜False⌝).bind
          fun a =>
          match f a with
          | Result.ok v => wp (pure v)
          | Result.fail e => wp (throw e)
          | Result.div => PredTrans.const ⌜False⌝).apply
      Q).down simp [PredTrans.bind, PredTrans.const]All goals completed! 🐙

theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) :
    (⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝,
                  fun e => ⌜P (.fail e)⌝⟩) → P x := byα:Typex:Result αP:Result α → Prop⊢ (⊢ₛ wp⟦x⟧ (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())) → P x
  intro hspecα:Typex:Result αP:Result α → Prophspec:⊢ₛ wp⟦x⟧ (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())⊢ P x
  simp only [instWP] at hspecα:Typex:Result αP:Result α → Prophspec:⊢ₛ
  (match x with
      | ok v => wp (pure v)
      | fail e => wp (throw e)
      | div => PredTrans.const ⌜False⌝).apply
    (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())⊢ P x
  split at hspech_1α:TypeP:Result α → Propx✝:Result αv✝:αhspec:⊢ₛ wp⟦pure v✝⟧ (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())⊢ P (ok v✝)h_2α:TypeP:Result α → Propx✝:Result αe✝:Errorhspec:⊢ₛ wp⟦throw e✝⟧ (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())⊢ P (fail e✝)h_3α:TypeP:Result α → Propx✝:Result αhspec:⊢ₛ (PredTrans.const ⌜False⌝).apply (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())⊢ P div <;>h_1α:TypeP:Result α → Propx✝:Result αv✝:αhspec:⊢ₛ wp⟦pure v✝⟧ (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())⊢ P (ok v✝)h_2α:TypeP:Result α → Propx✝:Result αe✝:Errorhspec:⊢ₛ wp⟦throw e✝⟧ (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())⊢ P (fail e✝)h_3α:TypeP:Result α → Propx✝:Result αhspec:⊢ₛ (PredTrans.const ⌜False⌝).apply (fun a => ⌜P (ok a)⌝, fun e => ⌜P (fail e)⌝, ())⊢ P div simp_allAll goals completed! 🐙

The definition of the WP instance determines what properties can be derived from proved specifications via Result.of_wp. This lemma defines what “weakest precondition” means.

To exemplify the second part, here is an example definition of UInt32 addition in Result that models integer overflow:

instance : MonadExcept Error Result where
  throw e := .fail e
  tryCatch x h := match x with
  | .ok v => pure v
  | .fail e => h e
  | .div => .div

def addOp (x y : UInt32) : Result UInt32 :=
  if x.toNat + y.toNat ≥ UInt32.size then
    throw .integerOverflow
  else
    pure (x + y)

There are two relevant specification lemmas to register:

@[spec]
theorem Result.throw_spec {α Q} (e : Error) :
    ⦃Q.2.1 e⦄ throw (m := Result) (α := α) e ⦃Q⦄ := id

@[spec]
theorem addOp_ok_spec {x y} (h : x.toNat + y.toNat < UInt32.size) :
    ⦃⌜True⌝⦄
    addOp x y
    ⦃⇓ r => ⌜r = x + y ∧ (x + y).toNat = x.toNat + y.toNat⌝⦄ := byx:UInt32y:UInt32h:x.toNat + y.toNat < UInt32.size⊢ ⦃⌜True⌝⦄ addOp x y ⦃PostCond.noThrow fun r => ⌜r = x + y ∧ (x + y).toNat = x.toNat + y.toNat⌝⦄
  mvcgen [addOp] with (simp_allAll goals completed! 🐙; try grindAll goals completed! 🐙)

This is already enough to prove the following example:

example :
  ⦃⌜True⌝⦄
  do let mut x ← addOp 1 3
     for _ in [:4] do
        x ← addOp x 5
     return x
  ⦃⇓ r => ⌜r.toNat = 24⌝⦄ := by⊢ ⦃⌜True⌝⦄ do
  let x ← addOp 1 3
  let r ←
    forIn [:4] x fun x r =>
        let x := r;
        do
        let r ← addOp x 5
        let x : UInt32 := r
        pure PUnit.unit
        pure (ForInStep.yield x)
  let x : UInt32 := r
  pure x ⦃PostCond.noThrow fun r => ⌜r.toNat = 24⌝⦄
  mvcgen
  invariants
  · ⇓⟨xs, x⟩ => ⌜x.toNat = 4 + 5 * xs.prefix.length⌝
  with (simp_all [UInt32.size]All goals completed! 🐙; try grindAll goals completed! 🐙)

18.1.8. Proof Mode for Stateful Goals

It is a priority of mvcgen to break down monadic programs into verification conditions that are straightforward to understand. For example, when the monad is monomorphic and all loop invariants have been instantiated, an invocation of all_goals mleave should simplify away any Std.Do.SPred-specific constructs and leave behind a goal that is easily understood by humans and grind. This all_goals mleave step is carried out automatically by mvcgen after loop invariants have been instantiated.

However, there are times when mleave will be unable to remove all Std.Do.SPred constructs. In this case, verification conditions of the form H ⊢ₛ T will be left behind. The assertion language Assertion translates into an Std.Do.SPred as follows:

abbrev PostShape.args : PostShape.{u} → List (Type u)
  | .pure => []
  | .arg σ s => σ :: PostShape.args s
  | .except _ s => PostShape.args s

abbrev Assertion (ps : PostShape.{u}) : Type u :=
  SPred (PostShape.args ps)

def

Std.Do.SPred.{u} (σs : List (Type u)) : Type u
Std.Do.SPred.{u} (σs : List (Type u)) :
  Type u

A predicate indexed by a list of states.

example : SPred [Nat, Bool] = (Nat → Bool → ULift Prop) := rfl

def

Std.Do.SPred.entails.{u} {σs : List (Type u)} (P Q : Std.Do.SPred σs) :
  Prop
Std.Do.SPred.entails.{u}
  {σs : List (Type u)}
  (P Q : Std.Do.SPred σs) : Prop

Entailment in SPred.

syntaxNotation for SPred

term ::= ...
    | Embedding of pure Lean values into `SVal`. An alias for `SPred.pure`. ⌜term⌝

term ::= ...
    | Entailment in `SPred`; sugar for `SPred.entails`. term ⊢ₛ term

term ::= ...
    | Bi-entailment in `SPred`; sugar for `SPred.bientails`. term ⊣⊢ₛ term

A common case for when a VC of the form H ⊢ₛ T is left behind is when the base monad m is polymorphic. In this case, the proof will depend on a WP m ps instance which governs the translation into the Assertion language, but the exact correspondence to σs : List (Type u) is yet unknown. To successfully discharge such a VC, mvcgen comes with an entire proof mode that is inspired by that of the Iris concurrent separation logic. (In fact, the proof mode was adapted in large part from its Lean clone, iris-lean.) The tactic reference contains a list of all proof mode tactics.

18. The mvcgen tactic🔗

18.1. Verifying Imperative Programs Using mvcgen

18.1.1. Preconditions and Postconditions

18.1.2. Loops and Invariants

18.1.3. Control Flow

18.1.4. Compositional Reasoning About Effectful Programs Using Hoare Triples

18.1.4.1. Hoare Triples

18.1.4.2. Composing Specifications

18.1.4.3. An Advanced Note About Pure Preconditions and a Notion of Frame Rule

18.1.5. Monad Transformers and Lifting

18.1.6. Exceptions

18.1.7. Extending mvcgen With Support for Custom Monads

Constructor

Fields

Instance Constructor

Methods

Instance Constructor

Extends

Methods

18.1.8. Proof Mode for Stateful Goals

18. The `mvcgen` tactic🔗

18.1. Verifying Imperative Programs Using `mvcgen`

18.1.7. Extending `mvcgen` With Support for Custom Monads