# Verifying imperative programs using `mvcgen`

The `mvcgen` tactic implements a _monadic verification condition generator_:
It breaks down a goal involving a program written using Lean's imperative `do` notation into a number of pure _verification conditions_ that discharge said goal.
A verification condition is a sub-goal that does not mention the monad underlying the `do` block.

As a "hello world" to `mvcgen`, the following example `mySum` computes the sum of an array using local mutability and a `for` loop.
Then it proves `mySum` correct relative to `Array.sum`, requiring us to specify an invariant for the loop:

import Std.Tactic.Do

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

open Std.Do

theorem mySum_correct (l : Array Nat) : mySum l = l.sum := by
  -- Focus on the part of the program which has a monadic implementation (`Id.run do ...`)
  generalize h : mySum l = x
  apply Id.of_wp_run_eq h
  -- Break down into verification conditions
  mvcgen
  -- Specify the invariant which we want to hold true 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 a prefix `xs.prefix` and a suffix `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 pure `p : Prop` into the assertion language.
  case inv1 => exact ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝
  -- 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 mleave
  -- Prove that our invariant is preserved at each step of the loop
  case vc1.step ih =>
    -- 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`.
    grind
  -- Prove that the invariant is true at the start
  case vc2.a.pre1 =>
    grind
  -- Prove that the invariant at the end of the loop implies the property we wanted
  case vc3.a.post h =>
    grind

After specifying the loop invariant, the proof can be shortened to just `all_goals mleave; grind`.
Note that the case labels have a unique prefix `vc1`, `vc2`, `vc3` etc.
Whenever referring to cases, only this prefix should be used; the suffix is merely a poor man's hint to the user where that particular VC came from.
For example,

* `vc1.step` conveys that this VC proves the inductive step for the loop
* `vc2.a.pre1` is meant to prove that the hypotheses of a goal implies the precondition of a specification (of `forIn`).
* `vc3.a.post` is meant to prove that the postcondition of a specification (of `forIn`) implies the target of the goal.

It is helpful to compare this to a traditional correctness proof:

theorem mySum_correct_traditional (l : Array Nat) : mySum l = l.sum := by
  -- Turn the array into a list
  cases l with | mk l =>
  -- Unfold `mySum` and rewrite `forIn` to `foldl`
  simp [mySum]
  -- Generalize the inductive hypothesis
  suffices h : ∀ out, List.foldl (· + ·) out l = out + l.sum by simp [h]
  -- Grind away
  induction l with grind

This proof is similarly succinct as the proof using `mvcgen`.
However, the traditional approach relies on important properties of the program:

* The `for` loop does not `break` or `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 is `pure`, that is, does not perform any effects.
(Indeed, all computations in the base monad `Id` factor through `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

* `do` blocks using control flow constructs such as (nested) `for` loops with early `return`.
* Effectful computations in non-`Id` monads.
Such computations affect the implicit monadic context (state, exceptions) in ways that need to be reflected in loop invariants.

`mvcgen` scales to these challenges with reasonable effort.

## Control flow

Let us consider another example that combines `for` loops with an early return.
Recall that `List.Nodup` is a predicate that asserts that a given list does not contain any duplicates.
The example 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

theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by
  generalize h : nodup l = r
  apply Id.of_wp_run_eq h
  mvcgen
  case inv1 =>
    exact Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun xs seen => ⌜(∀ x, x ∈ seen ↔ x ∈ xs.prefix) ∧ xs.prefix.Nodup⌝)
  all_goals mleave; grind

The proof has the same succinct structure as for the initial `mySum` example, because we again offload all proofs to `grind` and its existing framework around `List.Nodup`.
Therefore, the only difference is in the 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.)

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

theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by
  rw [nodup]
  generalize hseen : (∅ : Std.HashSet Int) = seen
  change ?lhs ↔ l.Nodup
  suffices h : ?lhs ↔ l.Nodup ∧ ∀ x ∈ l, x ∉ seen by grind
  clear hseen
  induction l generalizing seen with grind [Id.run_pure, Id.run_bind]

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` can pick up again.

The usual way to avoid replicating the control flow of a definition under proof is to use the `fun_cases` or `fun_induction` tactics.
Unfortunately, `fun_cases` does not help with control flow inside a `forIn` application, for example.
This is in contrast to `mvcgen`, which ships with support for many `forIn` implementations and is easily extended with `@[spec]` annotations for custom `forIn` implementations.
Furthermore, a `mvcgen`-powered proof will never need to copy any part of the original program.

## Compositional reasoning about effectful programs using Hoare triples

The previous examples reasoned about functions defined using `Id.run do <prog>` to make use of local mutability and early return in `<prog>`.
However, real-world programs often use `do` 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 monadic return type `M α` and compose well with other functions of that return type.
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`:

theorem mkFreshN_correct (n : Nat) : ((mkFreshN n).run' s).Nodup := by
  -- Focus on `(mkFreshN n).run' s`.
  generalize h : (mkFreshN n).run' s = x
  apply StateM.of_wp_run'_eq h
  -- 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]
  -- 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.
  case inv1 => exact ⇓⟨xs, acc⟩ state => ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝
  all_goals mleave; grind

### 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.
These can either be passed as arguments to `mvcgen` or registered in a global (or `scoped`, or `local`) database of specifications using the `@[spec]` lemma:

@[spec]
theorem mkFresh_spec (c : Nat) : ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by
  -- Unfold `mkFresh` and blast away:
  mvcgen [mkFresh]
  grind

@[spec]
theorem mkFreshN_spec (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by
  -- `mvcgen [mkFreshN, mkFresh_spec]` if `mkFresh_spec` were not registered with `@[spec]`
  mvcgen [mkFreshN]
  -- As before:
  case inv1 => exact ⇓⟨xs, acc⟩ state => ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝
  all_goals mleave; grind

theorem mkFreshN_correct (n : Nat) : ((mkFreshN n).run' s).Nodup :=
  -- The type `⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄` of `mkFreshN` is definitionally equal to
  -- ∀ (n : Nat) (s : Supply), True → ((mkFreshN n).run' s).Nodup
  mkFreshN_spec n s True.intro

Here, the notation `⦃fun state => ⌜state.counter = c⌝⦄ mkFresh ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄` denotes a _Hoare triple_ (cf. `Std.Do.Triple`).
Specifications for monadic functions always have such a Hoare triple result type.

### Hoare triples

A Hoare triple `⦃P⦄ prog ⦃Q⦄` means "If the _precondition_ `P` on the state holds, then the _postcondition_ `Q` holds after running the monadic _program_ `prog`".
So the specification theorem for `mkFresh` says:

> If `c` refers to the `counter` field of the `Supply` prestate, then running `mkFresh` returns `c` and modifies the `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⟦·⟧` that translates monadic programs into this logic:

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

The `WP` type class maps a monad `m` to its `ps : PostShape`, and this `PostShape` governs the exact
shape of the `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 `Triple`:

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

example : @Triple' α σ = Triple (m := StateM σ) := rfl

The common postcondition notation `⇓ r => ...` injects an assertion of type `α → Assertion ps` into
`PostCond ps`; 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 : Prop` into a stateful assertion.
Vice versa, any stateful hypothesis `h : Assertion ps` is called _pure_ if it is equivalent to `⌜p⌝`
for some `p : Prop`.
Pure, stateful hypotheses may be freely moved into the regular Lean context and back.
(This can be done manually with the `mpure` tactic.)

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

### Monad transformer stacks

Real-world programs often orchestrate the interaction of independent subsystems through a stack of monad transformers.
We can tweak the previous example to demonstrate this.
Suppose that `mkFresh` is generalized to work in any base monad `m` under `StateT Supply`.
Furthermore, `mkFreshN` is defined in terms of a concrete monad transformer stack `AppM` and lifts `mkFresh` into `AppM`.
Then the `mvcgen`-based proof goes through unchanged:

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

abbrev AppM := StateT Bool (StateT Supply (ReaderM String))
abbrev liftCounterM : StateT Supply (ReaderM String) α → AppM α := liftM

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

@[spec]
theorem mkFresh_spec [Monad m] [WPMonad m ps] (c : Nat) :
    ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh (m := m) ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by
  mvcgen [mkFresh]
  grind

@[spec]
theorem mkFreshN_spec (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by
  mvcgen [mkFreshN, liftCounterM] -- `liftCounterM` here ensures unfolding
  case inv1 => exact ⇓⟨xs, acc⟩ _ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝
  all_goals mleave; grind

The `WPMonad` type class asserts that `wp⟦·⟧` 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.

### Exceptions

If `let mut` is the first-order pendant to `StateT`, then early `return` is the first-order pendant to `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 `α → Assertion ps` for the success case.
To see why, suppose the latter was the case, and suppose that program `prog` throws an exception in aprestate satisfying `P`.
Should we be able to prove `⦃P⦄ prog ⦃⇓ r => Q r⦄`?
Certainly, `Q` does not hold because there is no result `r` it could hold for!

So there are two reasonable options, inspired by nontermination in traditional program logics:

1. _Total_ correctness interpretation: `⦃P⦄ prog ⦃⇓ r => Q r⦄` asserts that, given `P` holds, then `prog` terminates _and_ `Q` holds for the result.
2. _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 (cf. `PostCond.noThrow`), while `⇓? r => Q r` has the partial interpretation (cf. `PostCond.mayThrow`).
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.
The following correctness property expresses this:

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 := by omega}
    pure n

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

@[spec]
theorem mkFresh_spec (c : Nat) :
    ⦃fun state => ⌜state.counter = c⌝⦄
    mkFresh
    ⦃post⟨fun r state => ⌜r = c ∧ c < state.counter⌝, fun _msg state => ⌜c = state.counter ∧ c = state.limit⌝⟩⦄ := by
  mvcgen [mkFresh]
  all_goals grind

@[spec]
theorem mkFreshN_spec (n : Nat) :
    ⦃⌜True⌝⦄
    mkFreshN n
    ⦃post⟨fun r => ⌜r.Nodup⌝, fun _msg state => ⌜state.counter = state.limit⌝⟩⦄ := by
  mvcgen [mkFreshN]
  case inv1 => exact post⟨fun ⟨xs, acc⟩ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝,
                          fun _msg state => ⌜state.counter = state.limit⌝⟩
  all_goals mleave; try grind

theorem mkFreshN_correct (n : Nat) :
    match (mkFreshN n).run s with
    | .ok    l _  => l.Nodup
    | .error _ s' => s'.counter = s'.limit := by
  generalize h : (mkFreshN n).run s = x
  apply EStateM.of_wp_run_eq h
  mvcgen

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

Every `.arg σ` layer adds another `σ → ...` layer to the language of `Assertion`s.
Every `.except ε` layer leaves the `Assertion` language unchanged, but adds another exception
condition to the postcondition.

variable (α σ ε : Type)
example : PostCond α (.arg σ .pure) = ((α → σ → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε .pure) = ((α → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → ULift Prop) × (ε → σ → ULift Prop) × PUnit) := rfl

Hence the `WP` instance for `EStateM ε σ` maps to the `PostShape` `.except ε (.arg σ .pure)`, just
as for `ExceptT ε (StateM σ)`.

## Extending `mvcgen` with support for custom monads

The `mvcgen` framework is designed to be extensible.
None of the monads 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.

/--
  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.
-/
class WP (m : Type u → Type v) (ps : outParam PostShape.{u}) where
  wp {α} (x : m α) : PredTrans ps α

/--
  A `WP` that is also a monad morphism, preserving `pure` and `bind`. (They all are.)
-/
class WPMonad (m : Type u → Type v) (ps : outParam PostShape.{u}) [Monad m]
  extends LawfulMonad m, WP m ps where
  wp_pure : ∀ {α} (a : α), wp (pure a) = pure a
  wp_bind : ∀ {α β} (x : m α) (f : α → m β), wp (do let a ← x; f a) = do let a ← wp x; wp (f a)

Suppose one wants to use `mvcgen` to generate verification conditions for programs generated by [`Aeneas`](https://github.com/AeneasVerif/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

instance : Monad Result where
  pure x := .ok x
  bind x f := match x with
  | .ok v => f v
  | .fail e => .fail e
  | .div => .div

instance : LawfulMonad Result := by
  apply LawfulMonad.mk' <;> (simp only [instMonadResult]; grind)

Support for this monad is a matter of

1. Adding a `WP` and `WPMonad` instance for `Result`
2. Registering specification lemmas for the translation of basic Rust primitives such as addition etc.

The first part is straightforward:

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

instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
  wp_pure := by intros; ext Q; simp [wp, PredTrans.pure, pure, Except.pure, Id.run]
  wp_bind x f := by
    simp only [instWP, bind]
    ext Q
    cases x <;> simp [PredTrans.bind, PredTrans.const]

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
  intro hspec
  simp only [instWP] at hspec
  split at hspec <;> simp_all

The `WP` instance above 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.
Note that this 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 (e : Error) :
    ⦃Q.2.1 e⦄ throw (m := Result) (α := α) e ⦃Q⦄ := id

@[spec]
theorem addOp_noOverflow_spec (x y : UInt32) (h : x.toNat + y.toNat < UInt32.size) :
    ⦃⌜True⌝⦄ addOp x y ⦃⇓ r => ⌜r = x + y ∧ (x + y).toNat = x.toNat + y.toNat⌝⦄ := by
  mvcgen [addOp] <;> simp_all; try grind

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
  mvcgen
  case inv1 => exact ⇓⟨xs, x⟩ => ⌜x.toNat = 4 + 5 * xs.prefix.length⌝
  all_goals simp_all [UInt32.size]; try grind

## Proof mode for stateful goals

It is a priority of `mvcgen` to break down monadic programs into VCs that are straightforward to understand.
For example, when the monad stack 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`.

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`, for `H P : Std.Do.SPred σs` will be left behind.
The assertion language `Assertion ps` translates into such an `Std.Do.SPred σs` as follows:

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

/--
  An assertion on the `.arg`s in the given predicate shape.

example : Assertion (.arg ρ .pure) = (ρ → ULift Prop) := rfl
example : Assertion (.except ε .pure) = ULift Prop := rfl
example : Assertion (.arg σ (.except ε .pure)) = (σ → ULift Prop) := rfl
example : Assertion (.except ε (.arg σ .pure)) = (σ → ULift Prop) := rfl

  This is an abbreviation for `SPred` under the hood, so all theorems about `SPred` apply.
-/
abbrev Assertion (ps : PostShape.{u}) : Type u :=
  SPred (PostShape.args ps)

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`](https://github.com/leanprover-community/iris-lean).)
The Lean 4 test file [`tests/lean/run/spredProofMode.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/spredProofMode.lean) contains many examples of that proof mode to learn from, and the reference manual has a list of all proof mode tactics.

## Further reading

* More examples can be found in Lean's test suite.
* [`tests/lean/run/doLogicTests.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/doLogicTests.lean) is a kitchen sink test file with many examples.
* [`tests/lean/run/bhaviksSampler.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/bhaviksSampler.lean) is a stubbed out example from a larger development due to Bhavik Mehta.
* [Markus Himmel's `human-eval-lean` project](https://github.com/TwoFX/human-eval-lean/) has a limited number of `mvcgen`-based proofs for imperative algorithm implementations. Contributions welcome!
* [Rish Vaishnav's ongoing `qsort` formalization](https://github.com/rish987/qsort/) is the largest example of `mvcgen` to date.
* Be sure to read the documentation comments for `Std.Do.SPred`, `Std.Do.PostCond`, `Std.Do.PredTrans`, `Std.Do.Triple` and the tactics `mvcgen`, `mspec`, `mintro`, etc.