Imperative Programming in Coq

Just as in Haskell, we can simulate writing programs that manipulate state by taking advantage of monads. Another way to think about this is that we can embed the primitives of IMP into Coq and we automatically get a higher-order, dependently-typed, stateful programming language.

In the development below, I will build a module that is parameterized by some universe of values that we can store in the heap, and then later instantiate the universe with a type of my choice. In the module, we will define basic notions of a heap, of commands as a monad which manipulates heaps, and appropriate Hoare-logic rules for reasoning about these commands.

We will model pointers using nats, but any type that provides an equality and way to generate a fresh value would do.

We will model heaps as lists of pointers and values drawn from the universe.

We will model commands of type t, as functions which take a heap, and return an optional pair of a heap and a t. So this is really a combination of the state and option monad.

The definitions of ret and bind for the monad. Unlike Haskell, we could actually prove that the monad laws hold! (This would be a good homework.)

Some notation to approximate Haskell's "do" notation.

Like Haskell's runST, we can provide a run for the monad, starting with an empty heap.

Failure -- this is like throwing an exception. A good homework for people unfamiliar with monads is to define a "try _ catch _" construct.

Allocation -- to allocate a fresh location, we run through the heap and find the biggest pointer, and simply return the next biggest pointer. Another good homework is to change the definitions here to carry along the "next available pointer" as part of the state of the system.

The new u command allocates a new location in the heap, initializes it with the value u, and returns the pointer to the freshly-allocated location.

Lookup a pointer in the heap, returning the value associated with it if any.

The read command looks up the given pointer and returns the value if any, and fails if there is no value present. It leaves the heap unchanged.

Remove the pointer p from the heap, returning a new heap.

To write u into the pointer p, we first check that p is defined in the heap, and then remove it, and add it back with the value u.

To free the pointer p, we simply remove it from the heap. Again, this will fail if p wasn't in the heap to begin with.

Hoare Logic

Now that we've defined a language of commands, we can define a logic for reasoning about commands, just as Benjamin did.

The Hoare Total-Correctness Triple {{P}}c{{Q}} holds when if we run c in a heap h satisfying P, we get back a heap h' and value v, satisfying Q h v h'. Notice that our post-conditions allow us to relate the input heap, the output value, and the output heap. The ability to refer to the initial heap is important for giving rules that are as strong as possible without having to introduce auxilliary variables.

My usual simplification tactic.

A heap h always satisfies the predicate top.

The Hoare-rule for return: We can run the command in any initial state and end up in a state where the heap is unchanged, and the return value is equal to the value we passed in. This is pretty obviously the weakest precondition needed to ensure the command won't fail, and the strongest post-condition we can show about the resulting state.

An alternative, more conventional rule. I don't like this because it forces me to come up with a predicate -- i.e., we can only use it in a context where P is already known.

The rule of consequence

The new u command can be run in any initial state h, and results in a state (p,u)::h where p is fresh. The freshness is captured by the fact that lookup h p = None, i.e., the pointer was unallocated in the pre-state.

The free p command can be run in any state where p is defined, and results in a state where p is removed.

The read p command can be run in any state where p is defined, and results in an unchanged state. The value returned is equal to the the value associated with p.

The write p u command can be run in any state where p is defined, and results in a state where p maps to u, but is otherwise unchanged.

The rule for bind is the most complicated, but that's more because we want to support dependency than anything else. Intuitively, if {{P1}}c{{Q1}} and {{P2 x}}f x{{Q2 x}}, then the compound command x <- c ; f has as the weakest pre- condition needed to ensure we don't fail that P1 holds and for any (demonically-chosen state and value) x and h' which c might compute (and hence satisfies Q1 h x h'), we can show that P2 x h' holds. Both conditions are needed to ensure that neither command will fail.

The post-condition is the strongest post-condition we can calculate as the composition of the commands. It is effectively the relational composition of the post-conditions for c and f respectively.

Again, note that we can effectively compute the pre- and post- conditions instead of forcing a prover to magically come up with appropriate conditions.

Some notation for the bind_tc rule that parallels the notation for the bind constructor.

Just for fun, we can define our own version of if.

Now we can give a proper interface to run -- we should only pass it commands that will return a value and then we can guarantee that we won't get a failure.

Alas, our universe of storable values cannot be big enough to store computations. If we try to add computations to the types in U, we get a non-positive occurrence. In short, you seem to need generally recursive types to build storable commands. Not suprisingly, this leads to termination problems, as we can use Landin's knot to build a diverging computation...

Some example commands -- some can go wrong!

Some example proofs that these commands have specifications -- one way to view this is that we are building commands and inferring specifications for them, fully automatically!

Unfortunately, the specifications that we calculate are rather unwieldy. Even these simple proofs yield default specifications that are impossible to read.

More generally, we can write a function, like swap, and give it a human-readable specification. Then we can use the combinators to build most of the proof, and all we are left with are the two verification conditions from the rule of consequence.

We first prove a key lemma from the "McCarthy" axioms of memory that allows us to reason about updates when two pointers are different.

Then we build a tactic that simplifies memory lookups

Finally, we build the proof that swap has the following nice specification.

We might like to add a new command that reads out a number or that reads out a pair.

We can define appropriate proof rules for these now.

Now we can prove that the following code will not get stuck.

Here is the proof...

Print out the proof -- it's huge!

We can even define loops and infer pre- and post-conditions for them, thanks to our ability to define predicates inductively. Here, we define a loop that iterates n times a command body.

The pre-condition for the loop can be computed by composing the pre-condition of the body P with its post-condition Q using the precomp predicate transformer.

The post-condition for the loop can be computed by composing the post-condition of the body Q with itself, using the postcomp predicate transformer.

Finally, if we can show that a loop body has pre-condition P and post-condition Q, then we can conclude that iterating the body n times results in a command with pre-condition obtained by iter_precomp P Q and post-condition obtained by iter_postcomp Q.