18.1.1. Control flow

Let us consider another example that combines for loops with an early return.

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:

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.

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

18.1.3. 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] attribute:

18.1.4. Hoare triples

Std.Do.Triple.{u, v} {m : Type u → Type v} {ps : Std.Do.PostShape}
  [Std.Do.WP m ps] {α : Type u} (x : m α) (P : Std.Do.Assertion ps)
  (Q : Std.Do.PostCond α ps) : Prop
Std.Do.Triple.{u, v} {m : Type u → Type v}
  {ps : Std.Do.PostShape} [Std.Do.WP m ps]
  {α : Type u} (x : m α)
  (P : Std.Do.Assertion ps)
  (Q : Std.Do.PostCond α ps) : Prop

term ::= ...
    | A Hoare triple for reasoning about monadic programs.
A proof for `Triple x P Q` is a *specification* for `x`:
If assertion `P` holds before `x`, then postcondition `Q` holds after running `x`.

`⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`.
⦃ term ⦄ term ⦃ term ⦄

Std.Do.Triple.and.{u, v} {m : Type u → Type v} {ps : Std.Do.PostShape}
  {α : Type u} {P₁ : Std.Do.Assertion ps} {Q₁ : Std.Do.PostCond α ps}
  {P₂ : Std.Do.Assertion ps} {Q₂ : Std.Do.PostCond α ps}
  [Std.Do.WP m ps] (x : m α) (h₁ : ⦃P₁⦄ x ⦃Q₁⦄) (h₂ : ⦃P₂⦄ x ⦃Q₂⦄) :
  ⦃P₁ ∧ P₂⦄ x ⦃Q₁ ∧ₚ Q₂⦄
Std.Do.Triple.and.{u, v}
  {m : Type u → Type v}
  {ps : Std.Do.PostShape} {α : Type u}
  {P₁ : Std.Do.Assertion ps}
  {Q₁ : Std.Do.PostCond α ps}
  {P₂ : Std.Do.Assertion ps}
  {Q₂ : Std.Do.PostCond α ps}
  [Std.Do.WP m ps] (x : m α)
  (h₁ : ⦃P₁⦄ x ⦃Q₁⦄) (h₂ : ⦃P₂⦄ x ⦃Q₂⦄) :
  ⦃P₁ ∧ P₂⦄ x ⦃Q₁ ∧ₚ Q₂⦄

Std.Do.Triple.mp.{u, v} {m : Type u → Type v} {ps : Std.Do.PostShape}
  {α : Type u} {P₁ : Std.Do.Assertion ps} {Q₁ : Std.Do.PostCond α ps}
  {P₂ : Std.Do.Assertion ps} {Q₂ : Std.Do.PostCond α ps}
  [Std.Do.WP m ps] (x : m α) (h₁ : ⦃P₁⦄ x ⦃Q₁⦄)
  (h₂ : ⦃P₂⦄ x ⦃Q₁ →ₚ Q₂⦄) : ⦃P₁ ∧ P₂⦄ x ⦃Q₁ ∧ₚ Q₂⦄
Std.Do.Triple.mp.{u, v}
  {m : Type u → Type v}
  {ps : Std.Do.PostShape} {α : Type u}
  {P₁ : Std.Do.Assertion ps}
  {Q₁ : Std.Do.PostCond α ps}
  {P₂ : Std.Do.Assertion ps}
  {Q₂ : Std.Do.PostCond α ps}
  [Std.Do.WP m ps] (x : m α)
  (h₁ : ⦃P₁⦄ x ⦃Q₁⦄)
  (h₂ : ⦃P₂⦄ x ⦃Q₁ →ₚ Q₂⦄) :
  ⦃P₁ ∧ P₂⦄ x ⦃Q₁ ∧ₚ Q₂⦄

Given the meaning of Hoare triples above, the specification theorem for mkFresh says:

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: