I’m currently taking the Fall 2017 iteration of 6.826, Principles of Computer Systems. This class has been offered in various forms over the years, but this iteration is quite different. It focuses on formal verification of computer systems using Coq, a language for mechanical theorem proving.

The goal of this class is to write the spec, implementation, and proofs for a formally verified RAID filesystem in Coq, then generate Haskell code from it.

I’ve been quite curious about the field of formal verification since I first learned about it last semester. I couldn’t fit Adam Chlipala’s FRAP (Formal Reasoning About Programs) into my schedule, but I didn’t want to miss out on Zeldovich and Kaashoek’s PoCS class because it seemed more practical in nature.

This is the first in a series of posts on approaching Coq and formal verification as a complete beginner.

# Environment Setup

I’d heard good things about using Emacs + Proof General for Coq, so I started using Spacemacs, which combines vim’s editing modes and keybindings with Emacs’.

I haven’t tried the default CoqIDE or Coquille in vim, but Emacs’ Coq support is pretty great. With company-coq and spacemacs-coq layers, there’s not much more you could ask for.

If you’re coming from vim, Spacemacs is a little obnoxious to get set up, though. The Coq integration is a Spacemacs ‘layer’, which is a set of configurations for a specific task. Make sure that the Coq layer activates upon opening a `.v`

file.

Perhaps I’ll do another post about all the editors I use daily — Vim, Sublime, Atom, and Spacemacs — (I’m a mongrel, I know), but for now, I’ll just direct you to some Spacemacs resources.

# Tactics, Datatypes, and Coq commands

Software Foundations is the best place to start getting your feet wet. The first three chapters — Basics, Induction, and Lists — will give you all you need to start being productive.

When you open a `.v`

Coq file in Spacemacs, Coq mode should be activated. You should now be able to access company-coq commands with the `Ctrl-C`

leader, and if you have spacemacs-coq, there’s some common commands under the `,`

leader. Start the proof using `proof-goto-point`

or an alias for it, and you’ll be able to see the goal you’re proving and the context, containing your variables and hypotheses, in a pane on the right. Note that the Coq process can only be active in one buffer at a time, so you can’t have proofs running simultaneously in several files.

Once you’ve learned the basic syntax, you should also do the Emacs `company-coq-tutorial`

to learn about all the IDE-like helpers that the layer provides.

## Coq objects

Here are some of the most important constructs in Coq:

`Definition`

,`Function`

,`Fixpoint`

, and`Inductive`

`Inductive`

defines inductive types. `Function`

and `Fixpoint`

are for recursively defined functions on inductive types. Note that `Fixpoints`

must be obviously decreasing on each recursive call, or else Coq will complain.

- Built-in datatypes such as
`Nat`

,`List`

,`Prop`

,`Bool`

. `Theorem`

,`Lemma`

,`Proof`

`match`

statements ( familiar from any other functional language )

## Getting started with tactics

The first three chapters of SF will teach you a few basic tactics — namely, `induction`

, `assert`

, `simpl`

, `reflexivity`

, `rewrite`

, `apply`

, `replace`

. Nearly all the the exercises can be completed with just these.

Once you get sufficiently advanced, you’ll be able to identify when magic commands like `auto`

or `omega`

will just solve the rest of your proof for you. `info_auto`

will show you the tactics that `auto`

is using.

You’ll start to notice patterns in how to apply tactics.

For instance,

- If you see a recursive data structure, you should think about
`destruct`

and`induction`

. Both are used to perform case analysis on a constructor of an inductively defined type; induction also generates an induction hypothesis, while destruct does not. - Sometimes,
`unfold`

will break a monolithic function into useful pieces. Other times, it will give you a`fix`

expression that is harder to parse. Try`simpl`

instead.^{2}

This cheatsheet is invaluable for most of the tactics you’ll ever need. I also found this site useful for the few most basic tactics.

When you first start out, it’s useful to be able to search for library lemmas, theorems, definitions, notation, etc. The `Search ___`

command will look for definitions and theorems. If you quote the search string like `"eqb"`

, it will look for all theorems with that as a substring.

`Locate`

can look up constants or notation, like `"?="`

. To insert the outputs of the last command as a comment (so you can refer to it without having to rerun it), spacemacs-coq provides the key sequence `, ;`

.

# Proving binary search trees (and pitfalls)

In the first lab of 6.826, we have to prove properties of trees. We are given a tree, defined as follows:

1 | (* A `nattree` is a tree of natural numbers, where every internal |

We have to define a binary search function and a function to test whether a tree is a BST, then write proofs about the correctness of our functions. We want to prove, among other things, that our BST tester does indeed enforce the sortedness of left and right subtrees, and that binsearch can indeed find every element in the tree.

My first attempt was a **disaster**, ending with convoluted proofs that would have gotten progressively harder had I not stopped and asked for help. I’ll talk about some of the pitfalls I made, and then discuss how everything went smoother on the second try.

## Pitfall 1: The Bool and Prop worlds

Coq has two worlds: computational (`Type`

) and logical (`Prop`

). Booleans exist in the computational world, and can be either `true`

or `false`

. `Props`

, by distinction, are uppercased `True`

or `False`

.

As this answer explains,

Essentially, Coq has both because they are useful for different things: booleans correspond to facts that can be checked mechanically (i.e., with an algorithm), whereas propositions can express more concepts… If

`b : bool`

represents a statement, we can assert that this statement is true by saying`b = true`

, which is of type`Prop`

.

Note that `Props`

can be used in proofs, but not in functions.

To relate the two, we need theorems that translate between `Bool`

and `Prop`

, as I quickly and painfully discovered.

Take a look at my initial definition of binsearch on a `nattree`

t.

1 | match t with |

This seems reasonable, right? However, the `beq_nat`

(an alias for `Nat.eqb`

) and `Nat.ltb`

return `Bools`

, not `Props`

!

So, when we want to use hypotheses like `x < n`

(a `Prop`

) to prove `(x <? n) = true`

, it’s not immediate because they’re in two different worlds!^{1}

We need a lemma in Coq like

1 | Lemma ltb_lt n m : (n <? m) = true <-> n < m. |

This lemma says that the proposition `n < m`

is `True`

iff the proposition `(n <? m) = true`

is `True`

.

To illustrate this more, how about proving the proposition that `(x <? n) = false`

given `x > n`

?

First we have to do something ugly like

1 | rewrite <- Bool.not_true_iff_false, Nat.ltb_lt. |

which changes the goal like:

1 | __________________ |

and only *then* will an automagic command like `omega`

be able to solve it.

### Second attempt

What’s a better way to define `binsearch`

, then? The cleanest is

1 | Function binsearch (x:nat) (t:nattree) : bool := |

The `?=`

is `Nat.compare`

, which returns a `comparison`

type, defined below:

1 | Inductive comparison : Set := |

With this cleaner definition, we can now use the lab’s given `destruct_compare`

tactic to split our proof into three cases: `x < n`

, `x = n`

, `x > n`

.

## Pitfall 2: Non-recursive definitions

Observe these two definitions of `btree_sorted`

, which checks a tree is a valid BST.

**1:**

1 | Fixpoint isAscendingProp (t: list nat) : Prop := |

**2:**

1 | Function btree_sorted (t:nattree) : Prop := |

**1** is flattening the tree via in-order traversal, then checking that each element in the list is $\leq$ the next element. Algorithmically, this is efficient and correct, but it would lead to more work when writing proofs, since I would need more lemmas about `isAscendingProp`

that related non-adjacent elements.

Writing recursive definitions as in **2** makes the proof much easier. As my TA said, you want the definition to match how you’re writing the proof.

### Aside: Using `List`

lemmas

In my final solution, all my functions were recursive except `btree_in`

, for determining membership in a list.

1 | Function btree_in (x:nat) (t:nattree) : Prop := |

If you get comfortable with the `List`

library, then this shouldn’t be a problem. The `In`

function has some nice lemmas. I used this one a lot:

1 | Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m. |

to split up

1 | H0: In x (flatten t1 ++ n :: flatten t2) |

into

1 | H0 : In x (flatten t1) \/ n = x \/ In x (flatten t2) |

# Identifying patterns

I found myself repeating the same tactic patterns in my proofs. For example, when I have a series of `/\`

like `A /\ B /\ C`

in my hypotheses, I can split them up using `destruct_pairs`

, allowing me to use each clause individually because I know each one must be true.

If there’s a series of `\/`

in a hypothesis, you need to use multiple `destructs`

.

For example, I often ended up having `H0 : In x (flatten left_subtree) \/ n = x \/ In x (flatten right_subtree)`

in my context, and my goal was to prove *one* of those clauses.

Well, I would use `destruct`

to consider each case individually, showing that the other two non-goal clauses resulted in contradictions. Therefore, my own goal must be true.

# Conventions and sugar

In `Basics.v`

of SF, you’ll find best practices on organizing proofs. I like to use nested bullet points `-`

, `+`

, and `*`

, in that order, to focus subgoals whenever I am doing `cases`

, `induction`

, or `destruct`

. When I have an `assert`

, I wrap the proof of the assert in `{}`

.

Hopefully, you learned some pointers to get you more productive in Coq! There’s not many clear, beginner-oriented resources out there, so all of this post was constructed with trial and a lot of error.