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.
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’.
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
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.
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.
Here are some of the most important constructs in Coq:
Inductive defines inductive types.
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
matchstatements ( familiar from any other functional language )
The first three chapters of SF will teach you a few basic tactics — namely,
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
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.
- If you see a recursive data structure, you should think about
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.
unfoldwill break a monolithic function into useful pieces. Other times, it will give you a
fixexpression that is harder to parse. Try
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
In the first lab of 6.826, we have to prove properties of trees. We are given a tree, defined as follows:
(* 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.
Coq has two worlds: computational (
Type) and logical (
Prop). Booleans exist in the computational world, and can be either
Props, by distinction, are uppercased
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 : boolrepresents a statement, we can assert that this statement is true by saying
b = true, which is of type
Props can be used in proofs, but not in functions.
To relate the two, we need theorems that translate between
Prop, as I quickly and painfully discovered.
Take a look at my initial definition of binsearch on a
match t with
This seems reasonable, right? However, the
beq_nat (an alias for
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
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
To illustrate this more, how about proving the proposition that
(x <? n) = false given
x > n?
First we have to do something ugly like
rewrite <- Bool.not_true_iff_false, Nat.ltb_lt.
which changes the goal like:
and only then will an automagic command like
omega be able to solve it.
What’s a better way to define
binsearch, then? The cleanest is
Function binsearch (x:nat) (t:nattree) : bool :=
Nat.compare, which returns a
comparison type, defined below:
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.
Observe these two definitions of
btree_sorted, which checks a tree is a valid BST.
Fixpoint isAscendingProp (t: list nat) : Prop :=
Function btree_sorted (t:nattree) : Prop :=
1 is flattening the tree via in-order traversal, then checking that each element in the list is 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.
In my final solution, all my functions were recursive except
btree_in, for determining membership in a list.
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:
Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m.
to split up
H0: In x (flatten t1 ++ n :: flatten t2)
H0 : In x (flatten t1) \/ n = x \/ In x (flatten t2)
I found myself repeating the same tactic patterns in my proofs. For example, when I have a series of
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
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.
Basics.v of SF, you’ll find best practices on organizing proofs. I like to use nested bullet points
*, in that order, to focus subgoals whenever I am doing
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.