Verifying Imperative Programs Using vcgen

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.

Loops and Invariants🔗

As a first example of vcgen, 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 over 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:

If mySum is correct, then it is equal to Array.sum. The statement mySum l = l.sum mentions no monad, because Lean.Parser.Term.do : termdo is an internal implementation detail of mySum. The proof below therefore first brings the goal into the form that vcgen works on, a weakest precondition, with the lemma Id.of_run_eq_wp. 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 vcgen to replace the formulation in terms of weakest preconditions with a set of verification conditions.

While vcgen 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.

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

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. A vcgen-powered proof, on the other hand, never needs to copy any part of the original program. The vcgen tactic ships with support for many forIn implementations, and a custom forIn implementation can be supported with a specification lemma that is annotated with @[spec]. Writing such a lemma takes considerable work, because a loop specification takes the invariant as a parameter and must prove that the loop preserves it. A Std.Internal.PureForIn instance is less work: it states that the loop over a container is the loop over the list ForIn.toList of its elements. With this instance, the loop specification that ships with vcgen applies to the container.

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:

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_run'_eq_wp serves the same role that Id.of_run_eq_wp did in the preceding examples.

This proof unfolds both mkFreshN and mkFresh. In a larger program, many functions call mkFresh, and every proof about one of them like the above would unfold mkFresh again. Instead, the behavior of mkFresh can be stated once, proved once, and then used at every call. Proofs that use the specification of a function and never its code are called modular. Hoare triples are the standard form of specifications for effectful programs, and they make such modular reasoning possible.

structure Triple ... (x : Prog) [WP Prog Value Pred EPred]
    (pre : Pred) (post : Value → Pred) (epost : EPred) : Prop where
  intro ::
  le_wp : pre ⊑ wp x post epost

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.

These proofs might not look much more exciting than when only a single monad was involved. However, under the radar of the user the proofs build on a cascade of specifications for MonadLift instances. They also build on the WPMonad instances of StateT and ReaderT, which make the specifications of pure and bind available in every layer. A WPMonad instance requires only that the weakest precondition of pure and bind is at least as weak as the one that the predicate transformer monad computes. In other words, wp is a lax morphism of ordered monads.

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 vcgen copes with StateT; here we will look at the program logic's support for ExceptT.

Exceptions are the reason why a triple carries an exception postcondition next to the success postcondition. To see why, suppose there were only the success postcondition, and suppose that program prog throws an exception in a prestate satisfying P. Should we be able to prove ⦃P⦄ prog ⦃Q'⦄? There is no result value, 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 ⦃Q'⦄ asserts that, given P holds, then prog terminates normally and Q' holds for the result.

The partial correctness interpretation

⦃P⦄ prog ⦃Q'; ⊤⦄ asserts that, given P holds, and if prog terminates normally then Q' holds for the result.

A triple without an explicit exception postcondition carries the bottom assertion (⊥ : EPred) and thus has the total interpretation: an exception would have to establish ⊥, so no exception can be thrown. The top assertion (⊤ : EPred) permits every exception and yields the partial interpretation.

In the running example, ⦃P⦄ prog ⦃Q'⦄ is unprovable, but ⦃P⦄ prog ⦃Q'; ⊤⦄ is trivially provable. Between (⊥ : EPred) and (⊤ : EPred), the exception postcondition expresses a spectrum of correctness properties.

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

The following correctness property expresses this:

The exception postcondition after the semicolon applies when mkFresh throws. The monad's WP instance determines the types of both postconditions: the exception postcondition takes the thrown exception in place of the result value, and each state gives an extra parameter.

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