How to prove a compiler correct
At POPL’18 (Principles of Programming Languages) last week, I ended up talking to Annie Cherkaev about her really cool DSL (domain specific language) SweetPea (which she presented at Off the Beaten Track 18, a workshop colocated with POPL), which is a “SATSampler aided language for experimental design, targeted for Psychology & Neuroscience”. In particular, we were talking about software engineering, and the work that Annie was doing to test SweetPea and increase her confidence that the implementation is correct!
The topic of how exactly one goes about proving a compiler correct
came up, and I realized that I couldn’t think of a highlevel (but
concrete) overview of what that might look like. Also, like
many compilers, hers is implemented in Haskell, so it seemed like a good
opportunity to try out the really cool work presented at the colocated
conference CPP’18 (Certified Programs and Proofs) titled “Total Haskell is Reasonable
Coq” by SpectorZabusky, Breitner, Rizkallah, and Weirich. They have
a tool (hstocoq
) that extracts Coq definitions from
(certain) terminating Haskell programs (of which at least small
compilers hopefully qualify). There are certainly limitations to this
approach (see Addendum at the bottom of the page for some discussion),
but it seems very promising from an engineering perspective.
The intention of this post is twofold:

Show how to take a compiler (albeit a tiny one) that was built with
no intention of verifying it and after the fact prove it correct. Part
of the ability to do this in such a seamless way is the wonderful
hstocoq
tool mentioned above, though there is no reason in principle you couldn’t carry out this translation manually (in practice maintenance becomes an issue, hence realistic verified compilers relying on writing their implementations within theorem provers like Coq and then extracting executable versions automatically, at least in the past – possiblyhstocoq
could change this workflow).  Give a concrete example of proving compiler correctness. By necessity, this is a very simplified scenario without a lot of the subtleties that appear in real verification efforts (e.g., undefined behavior, multiple compiler passes, linking with code after compilation, etc). On the other hand, even this simplified scenario could cover many cases of DSLs, and understanding the subtleties that come up should be much easier once you understand the basic case!
The intended audience is: people who know what compilers are (and may have implemented them!) but aren’t sure what it means to prove one correct!
All the code for this post, along with instructions to get it running, is in the repository https://github.com/dbp/howtoproveacompiler. If you have any trouble getting it going, open an issue on that repository.
DSL & Compiler
To make this simple, my source language is arithmetic expressions with adding, subtraction, and multiplication. I represent this as an explicit data structure in Haskell:
data Arith = Num Int
 Plus Arith Arith
 Minus Arith Arith
 Times Arith Arith
And a program is an Arith
. For example, the source
expression “1 + (2 * 4)” is represented as
Plus 1 (Times 2 4)
. The target of this is a sequence of
instructions for a stack machine. The idea of the stack machine is that
there is a stack of values that can be used by instructions. The target
language expressions are:
data StackOp = SNum Int
 SPlus
 SMinus
 STimes
And a program is a [StackOp]
. For example, the previous
example “1 + (2 * 4)” could be represented as
[SNum 1, SNum 2, SNum 4, STimes, SPlus]
. The idea is that a
number evaluates to pushing it onto the stack and plus/times evaluate by
popping two numbers off the stack and pushing the sum/product
respectively back on. But we can make this concrete by writing an
eval
function that takes an initial stack (which will
probably be empty), a program, and either produces an integer (the top
of the stack after all the instructions run) or an error (which, for
debugging sake, is the state of the stack and rest of the program when
it got stuck).
eval :: [Int] > [StackOp] > Either ([Int], [StackOp]) Int
:_) [] = Right n
eval (nSNum n:xs) = eval (n:ns) xs
eval ns (:n2:ns) (SPlus:xs) = eval (n1+n2:ns) xs
eval (n1:n2:ns) (SMinus:xs) = eval (n1n2:ns) xs
eval (n1:n2:ns) (STimes:xs) = eval (n1*n2:ns) xs
eval (n1= Left (vals, instrs) eval vals instrs
Now that we have our source and target language, and know how the target works, we can implement our compiler. Part of why this is a good small example is that the compiler is very simple!
compile :: Arith > [StackOp]
Num n) = [SNum n]
compile (Plus a1 a2) = compile a2 ++ compile a1 ++ [SPlus]
compile (Minus a1 a2) = compile a2 ++ compile a1 ++ [SMinus]
compile (Times a1 a2) = compile a2 ++ compile a1 ++ [STimes] compile (
The cases for plus/minus/times are the cases that are slightly
nonobvious, because they can contain further recursive expressions, but
if you think about what the eval
function is doing, once
the stack machine finishes evaluating everything that
a2
compiled to, the number that the left branch evaluated
to should be on the top of the stack. Then once it finishes evaluating
what a1
compiles to the number that the right branch
evaluated to should be on the top of the stack (the reversal is so that
they are in the right order when popped off). This means that evaluating
e.g. SPlus
will put the sum on the top of the stack, as
expected. That’s a pretty informal argument about correctness, but we’ll
have a chance to get more formal later.
Formalizing
Now that we have a Haskell compiler, we want to prove it correct! So
what do we do? First, we want to convert this to Coq using the hstocoq tool. There
are full instructions at https://github.com/dbp/howtoproveacompiler,
but the main command that will convert src/Compiler.hs
to
src/Compiler.v
:
STACK_YAML=hstocoq/stack.yaml stack exec hstocoq  o src/ src/Compiler.hs e hstocoq/base/edits
You can now build the Coq code with
make
And open up src/Proofs.v
using a Coq interactive mode (I
use Proof General within Emacs; with Spacemacs, this is particularly
easy: use the coq
layer!).
Proving things
We now have a Coq version of our compiler, complete with our evaluation function. So we should be able to write down a theorem that we would like to prove. What should the theorem say? Well, there are various things you could prove, but the most basic theorem in compiler correctness says essentially that running the source program and the target program “does the same thing”. This is often stated as “semantics preservation” and is often formally proven by way of a backwards simulation: whatever the target program does, the source program also should do (for a much more thorough discussion of this, check out William Bowman’s blog post, What even is compiler correctness?). In languages with ambiguity (nondeterminism, undefined behavior, this becomes much more complicated, but in our setting, we would state it as:
Theorem (informal). For all source arith expressions A, if eval [] (compile A) produces integer N then evaluating A should produce the same number N.
The issue that’s immediately apparent is that we don’t actually have a way of directly evaluating the source expression. The only thing we can do with our source expression is compile it, but if we do that, any statement we get has the behavior of the compiler baked into it (so if the compiler is wrong, we will just be proving stuff about our wrong compiler).
More philosophically, what does it even mean that the compiler is wrong? For it to be wrong, there has to be some external specification (likely, just in our head at this point) about what it was supposed to do, or in this case, about the behavior of the source language that the compiler was supposed to faithfully preserve. To prove things formally, we need to write that behavior down.
So we should add this function to our Haskell source. In a nontrivial DSL, this may be a significant part of the formalization process, but it is also incredibly important, because this is the part where you are actually specifying exactly what the source DSL means (otherwise, the only “meaning” it has is whatever the compiler happens to do, bugs and all). In this example, we can write this function as:
eval' :: Arith > Int
Num n) = n
eval' (Plus a1 a2) = (eval' a1) + (eval' a2)
eval' (Minus a1 a2) = (eval' a1)  (eval' a2)
eval' (Times a1 a2) = (eval' a1) * (eval' a2) eval' (
And we can rerun hstocoq
to get it added to our Coq
development. We can now formally state the theorem we want to prove
as:
Theorem compiler_correctness : forall a : Arith,
eval nil (compile a) = Data.Either.Right (eval' a).
I’m going to sketch out how this proof went. Proving stuff can be complex, but this maybe gives a sense of some of the thinking that goes into it. To go further, you probably want to take a course if you can find one, or follow a book like:
 Bertot and Casteron’s Coq’Art: Interactive Theorem Proving and Program Development.
 Adam Chlipala’s Certified Programming with Dependent Types
 Pierce et. al.’s Software Foundations
If you were to prove this on paper, you would proceed by induction on the structure of the arithmetic expression, so let’s start that way. The base case goes away trivially and we can expand the case for plus using:
induction a; iauto; simpl.
We see (above the line is assumptions, below what you need to prove):
IHa1 : eval nil (compile a1) = Either.Right (eval' a1)
IHa2 : eval nil (compile a2) = Either.Right (eval' a2)
============================
eval nil (compile a1 ++ compile a2 ++ SPlus :: nil) = Either.Right (eval' a1 + eval' a2)%Z
Which, if we look at it for a little while, we realize two things:

Our induction hypotheses really aren’t going to work, intuitively
because of the
Either
— our program won’t produceRight
results for the subtrees, so there probably won’t be a way to rely on these hypotheses. 
On the other hand, what does look like a Lemma we should be able to
prove has to do with evaluating a partial program. Rather than trying to
induct on the entire statement, we instead try to prove that
eval
ing acompile
d term will result in theeval'
d term on the top of the stack. This is an instance of a more general pattern – that often the toplevel statement that you want has too much specificity, and you need to instead prove something that is more general and then use it for the specific case. So here’s (a first attempt) at a Lemma we want to prove:
Lemma eval_step : forall a : Arith, forall xs : list StackOp,
eval nil (compile a ++ xs) = eval (eval' a :: nil) xs.
This is more general, and again we start by inducting on
a
, expanding and eliminating the base case:
induction a; intros; simpl; iauto.
We now end up with better inductive hypotheses:
IHa1 : forall xs : list StackOp, eval nil (compile a1 ++ xs) = eval (eval' a1 :: nil) xs
IHa2 : forall xs : list StackOp, eval nil (compile a2 ++ xs) = eval (eval' a2 :: nil) xs
============================
eval nil ((compile a1 ++ compile a2 ++ SPlus :: nil) ++ xs) =
eval ((eval' a1 + eval' a2)%Z :: nil) xs
We need to reshuffle the list associativity and then we can rewrite using the first hypotheses:
rewrite List.app_assoc_reverse. rewrite IHa1.
But now there is a problem (this is common, hence going over
it!). We want to use our second hypothesis. Once we do that, we can
reduce based on the definition of eval
and we’ll be done
(with this case, but multiplication is the same). The issue is that
IHa2
needs the stack to be empty, and the stack we now have
(since we used IHa1
) is eval' a1 :: nil
, so it
can’t be used:
IHa1 : forall xs : list StackOp, eval nil (compile a1 ++ xs) = eval (eval' a1 :: nil) xs
IHa2 : forall xs : list StackOp, eval nil (compile a2 ++ xs) = eval (eval' a2 :: nil) xs
============================
eval (eval' a1 :: nil) ((compile a2 ++ SPlus :: nil) ++ xs) =
eval ((eval' a1 + eval' a2)%Z :: nil) xs
The solution is to go back to what our Lemma statement said and generalize it now to arbitrary stacks (so in this process we’ve now generalized twice!), so that the inductive hypotheses are correspondingly stronger:
Lemma eval_step : forall a : Arith, forall s : list Num.Int, forall xs : list StackOp,
eval s (compile a ++ xs) = eval (eval' a :: s) xs.
Now if we start the proof in the same way:
induction a; intros; simpl; iauto.
We run into an odd problem. We have a silly obligation:
match s with
 nil => eval (i :: s) xs
 (_ :: nil)%list => eval (i :: s) xs
 (_ :: _ :: _)%list => eval (i :: s) xs
end = eval (i :: s) xs
Which will go away once we break apart the list s
and
simplify (if you look carefully, it has the same thing in all three
branches of the match). There are (at least) a couple approaches to
this:

We could just do it manually:
destruct s; simpl; eauto; destruct s; simpl; eauto
. But it shows up multiple times in the proof, and that’s a mess and someone reading the proof script may be confused what is going on. 
We could write a tactic for the same thing:
try match goal with [l : list _  _ ] => solve [destruct l; simpl; eauto; destruct l; simpl; eauto] end.
This has the advantage that it doesn’t depend on the name, you can call it whenever (it won’t do anything if it isn’t able to discharge the goal), but where to call it is still somewhat messy (as it’ll be in the middle of the proofs). We could hint using this tactic (using
Hint Extern
) to have it handled automatically, but I generally dislike adding global hints for tactics (unless there is a very good reason!), as it can slow things down and make understanding why proofs worked more difficult. 
We can also write lemmas for these. There are actually two cases that come up, and both are solved easily:
Lemma list_pointless_split : forall A B:Type, forall l : list A, forall x : B, match l with  nil => x  (_ :: _)%list => x end = x. Proof. destruct l; eauto. Qed. Lemma list_pointless_split' : forall A B:Type, forall l : list A, forall x : B, match l with  nil => x  (_ :: nil)%list => x  (_ :: _ :: _)%list => x end = x. Proof. destruct l; intros; eauto. destruct l; eauto. Qed.
In this style, we can then hint using these lemmas locally to where they are needed.
Now we know the proof should follow from list associativity, this
pointless list splitting, and the inductive hypotheses. We can write
this down formally (this relies on the literatecoq
library,
which is just a few tactics at this point) as:
Lemma eval_step : forall a : Arith, forall s : list Num.Int, forall xs : list StackOp,
eval s (compile a ++ xs) = eval (eval' a :: s) xs.
Proof.
hint_rewrite List.app_assoc_reverse.
hint_rewrite list_pointless_split, list_pointless_split'.
induction a; intros; simpl; iauto;
hint_rewrite IHa1, IHa2; iauto'.
Qed.
Which says that we know that we will need the associativity lemma and these list splitting lemmas somewhere. Then we proceed by induction, handle the base case, and then use the inductive hypotheses to handle the rest.
We can then go back to our main theorem, and proceed in a similar
style. We prove by induction, relying on the eval_step
lemma, and in various places needing to simplify (for the observant
reader, iauto
and iauto'
only differ in that
iauto'
does a deeper proof search).
Theorem compiler_correctness : forall a : Arith,
eval nil (compile a) = Data.Either.Right (eval' a).
Proof.
hint_rewrite eval_step.
hint_simpl.
induction a; iauto'.
Qed.
We now have a proof that the compiler that we wrote in Haskell is
correct, insofar as it preserves the meaning expressed in the
sourcelevel eval'
function to the meaning in the
eval
function in the target. This isn’t, of course, the
only theorem you could prove! Another one that would be interesting
would be that no compiled program ever got stuck (i.e., never produces a
Left
error).
As stated at the top of the post, all the code in this post is available at https://github.com/dbp/howtoproveacompiler. If you are looking for more, check out Xavier Leroy’s Oregon Programming Languages Summer School Lectures (videos are here, scroll down to find them).
Thanks to current and former PRL members, in particular Gabriel Scherer and William Bowman, for providing useful feedback on drafts of this post.
Addendum: termination
This example was so tiny we haven’t run into something that will be really common: imagine instead of the compile function shown above:
compile :: Arith > [StackOp]
Num n) = [SNum n]
compile (Plus a1 a2) = compile a2 ++ compile a1 ++ [SPlus]
compile (Minus a1 a2) = compile a2 ++ compile a1 ++ [SMinus]
compile (Times a1 a2) = compile a2 ++ compile a1 ++ [STimes] compile (
We instead wanted to take [Arith]
. This would still
work, and would result in the list of results stored on the stack (so
probably you would want to change eval
to print everything
that was on the stack at the end, not just the top). If you wrote this
compile
:
compile :: [Arith] > [StackOp]
= []
compile [] Num n:xs) = SNum n : compile xs
compile (Plus a1 a2:xs) = compile [a2] ++ compile [a1] ++ SPlus : compile xs
compile (Minus a1 a2:xs) = compile [a2] ++ compile [a1] ++ SMinus : compile xs
compile (Times a1 a2:xs) = compile [a2] ++ compile [a1] ++ STimes : compile xs compile (
You would get an error when you try to compile the output of
hstocoq
! Coq says that the compile function is not
terminating!
This is good introduction into a (major) difference between Haskell and Coq: in Haskell, any term can run forever. For a programming language, this is an inconvenience, as you can end up with code that is perhaps difficult to debug if you didn’t want it to (it’s also useful if you happen to be writing a server that is supposed to run forever!). For a language intended to be used to prove things, this feature would be a nonstarter, as it would make the logic unsound. The issue is that in Coq, (at a high level), a type is a theorem and the term that inhabits the type is a proof of that theorem. But in Haskell, you can write:
anything :: a
= anything anything
i.e., for any type, you can provide a term with that type — that is, the term that simply never returns. If that were possible in Coq, you could prove any theorem, and the entire logic would be useless (or unsound, which technically means you can prove logical falsehood, but since falsehood allows you to prove anything, it’s the same thing).
Returning to this (only slightly contrived) program, it isn’t
actually that our program runs forever (and if you do want to prove
things about programs that do, you’ll need to do much more work!), just
that Coq can’t tell that it doesn’t. In general, it’s not possible to
tell this for sufficiently powerful languages (this is what the Halting
problem says for Turing machines, and thus holds for anything with
similar expressivity). What Coq relies on is that some argument is
inductively defined (which we have: both lists and Arith
expressions) and that all recursive calls are to structurally
smaller parts of the arguments. If that holds, we are guaranteed to
terminate, as inductive types cannot be infinite (note: unlike Haskell,
Coq is not lazy, which is another difference, but we’ll ignore
that). If we look at our recursive call, we called compile
with [a1]
. While a1
is structurally smaller,
we put that inside a list and used that instead, which thus violates
what Coq was expecting.
There are various ways around this (like adding another argument
whose purpose is to track termination, or adding more sophisticated
measurements), but there is another option: adding a helper function
compile'
that does what our original compile
did: compiles a single Arith
. The intuition that leads to
trying this is that in this new compile
we are decreasing
on both the length of the list and the structure of the
Arith
, but we are trying to do both at the same time. By
separating things out, we can eliminate the issue:
compile :: [Arith] > [StackOp]
= []
compile [] :xs) = compile' x ++ compile xs
compile (x
compile' :: Arith > [StackOp]
Num n) = [SNum n]
compile' (Plus a1 a2) = compile' a2 ++ compile' a1 ++ [SPlus]
compile' (Minus a1 a2) = compile' a2 ++ compile' a1 ++ [SMinus]
compile' (Times a1 a2) = compile' a2 ++ compile' a1 ++ [STimes] compile' (
Addendum: do the proofs mean anything?
There are limitations to the approach outlined in this post. In
particular, what hstocoq
does is syntactically translate
similar constructs from Haskell to Coq, but constructs that have similar
syntax don’t necessarily have similar semantics. For example, data types
in Haskell are lazy and thus infinite, whereas inductive types in Coq
are definitely not infinite. This means that the proofs that you have
made are about the version of the program as represented in Coq, not the
original program. There are ways to make proofs about the precise
semantics of a language (e.g., Arthur Charguéraud’s CFML), but on the
other hand, program extraction (which is a core part of verified
compilers like CompCert) has the
same issue that the program being run has been converted via a similar
process as hstocoq
(from Coq to OCaml the distance is
less than from Coq to Haskell, but in principle there are similar
issues).
And yet, I think that hstocoq
has a real practical
use, in particular when you have an existing Haskell codebase that you
want to verify. You likely will need to refactor it to have
hstocoq
work, but that refactoring can be done within
Haskell, while the program continues to work (and your existing tests
continue to pass, etc). Eventually, once you finish conversion, you may
decide that it makes more sense to take the converted version as ground
truth (thus, you run hstocoq
and throw out the original,
relying on extraction after that point for an executable), but being
able to do this gradual migration (from full Haskell to essentially a
Gallinalike dialect of Haskell) seems incredibly valuable.