Ynot: Reasoning with the Awkward Squad

Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal.

Abstract

We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.

The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules that implement imperative finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which abstracts the implementation details and ensures that the modules properly implement the finite map abstraction.

Full Paper

The full paper is available as a PDF.

Code

Accompanying examples are available at coq sources tar ball.

Random Info

Greg and Aleks put together most of the system --- its is really cool, so take a look.. I jotted down here some comments about some of the parts of the development for the paper that I was particularly involved in.

There was an earlier hashtable implementations, but it had been written before much of the system was in place, and was showing its age.

I created the new FiniteMap interface, and implemented the Hashtable implementation (which uses FiniteMaps for its buckets). This was cool, especially as it forced me to dogfood my own interface. In particular it forced me to realize how essential Precision was, and to develop a library for precise predicates (and of course make the FiniteMap export its precisioon). For the functional model, I used a library for functional association lists that I had lying around from a previous development.

At one point I tried to make the FiniteMap dependently typed, but had trouble converting my functional association list library over to a dependently typed version. Then, Matthieu Sozeau visited us for a few days, and gave me some pointers. I was so excited that I converted over the functional library, the imperative FiniteMap interface, and the imperative hashtable implementation (and the ref-to-alist implementation) over to dependent types that night. The same night, I also wrote up the memoize library (which is just a trivial wrapper for a dependently typed finite map, which is why it was so cool). Updated the imperative code wound up being trivial. The hard part was just figuring out what injectivity axioms and eq_dep stuff I needed to convert over the functional interface. Coq documentation right now is not particularly good (ok, so neither is documentation for most of my stuff, including ynot. This is not exactly an uncommon state of affairs for research projects). The generally recommended approach (which is what I did in this case) is to find someone French to help you with your problems.

Then I added in a functional fold, and then figured out and specified the effectful fold for FiniteMaps. To test that it was strong enough to reason with, I immediately wrote a generic copy method for finite maps. After this, I of course implemented the fold, which was straightforward. This was really cool, because it is something that nobody else (JML, etc.) can approach doing --- specifying and reasoning about a higher order effectful computation. But it is absolutely crucial for reasoning! The specification also had the nice effect of ruling our concurrent modifications of the finite map that is being iterated over. This winds up being completely natural, in fact it is essentially for free. Given the pain that Java, for example, goes through to prevent this behaviour dynamically (with timestamps generally --- also note that the implementations that I have seen of this are easy to circumvent by overflowing the timestamp counter, so they don't actually guarantee safety). With seperation logic, it becomes trivial (and in fact, in some sense easier) to disallow such problems.

Then I wanted to write a splay tree implementation. Splay trees are fun because they modify the structure of the tree even on lookups. However, externally, this restructuring does not affect the tree (it does not change its model). This is an example that many systems have had problems with. I first coded up unbalanced binary search trees, partially because of a confusion on my part as to how splay trees work (particularly, that insert and delete also splay). I got that working, and then went ahead and implemented splay trees. Needless to say, the main recursive splay function is a bit of a killer. It is pretty complicated code, especially when you don't use C-isms, like break from inside of nested conditionals in a loop. After unrolling the code, I was relived to have a proof (well, eventually) that I had gotten it right. Actually, I didn't --- I confess to having introduced some bugs. The cool things was that as I was discharging proof obligations, I reached something that I could not prove, and the problem was clear. Not only that, the structure of the proof obligation essentially told me what I had messed up, and how to fix it. That was really nice.