/
2018-01-16-how-to-prove-a-compiler-correct.html
216 lines (211 loc) · 31.3 KB
/
2018-01-16-how-to-prove-a-compiler-correct.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>dbp.io :: How to prove a compiler correct</title>
<link rel="stylesheet" type="text/css" href="../css/default.css" />
<link rel="stylesheet" type="text/css" href="../css/syntax.css" />
</head>
<body>
<div id="navigation">
<a class="t b" href="https://dbp.io">Daniel Patterson</a>
<a class="t h" href="#">::</a>
<span class="t">
web: <a href="https://dbp.io">dbp.io</a>
</span>
<span class="t">
email: <a href="mailto:dbp@dbpmail.net">dbp@dbpmail.net</a>
</span>
<span class="t">
pubkey: <a href="../static/dbp.gpg">A98D4AF0</a>
</span>
<span class="t">
work: <a target="_blank" href="http://prl.ccs.neu.edu">prl.ccs.neu.edu</a>
</span>
</div>
<h2>How to prove a compiler correct</h2>
<p>by <em>Daniel Patterson</em> on <strong>January 16, 2018</strong></p>
<p>At POPL’18 (Principles of Programming Languages) last week, I ended up talking to <a href="https://anniecherkaev.com">Annie Cherkaev</a> about her really cool DSL (domain specific language) <a href="https://github.com/anniecherk/sweetpea">SweetPea</a>, which is a “SAT-Sampler 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 high-level (but <em>concrete</em>) 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 <a href="https://arxiv.org/abs/1711.09286">“Total Haskell is Reasonable Coq” by Spector-Zabusky, Breitner, Rizkallah, and Weirich</a>. They have a tool (<code>hs-to-coq</code>) 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.</p>
<p>The intention of this post is twofold:</p>
<ol style="list-style-type: decimal">
<li>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 <code>hs-to-coq</code> 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 <em>extracting</em> executable versions automatically, at least in the past – possibly <code>hs-to-coq</code> could change this workflow).</li>
<li>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!</li>
</ol>
<p><strong>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!</strong></p>
<blockquote>
<p>All the code for this post, along with instructions to get it running, is in the repository <a href="https://github.com/dbp/howtoproveacompiler" class="uri">https://github.com/dbp/howtoproveacompiler</a>. If you have any trouble getting it going, open an issue on that repository.</p>
</blockquote>
<h3 id="dsl-compiler">DSL & Compiler</h3>
<p>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:</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="kw">data</span> <span class="dt">Arith</span> <span class="fu">=</span> <span class="dt">Num</span> <span class="dt">Int</span>
<span class="fu">|</span> <span class="dt">Plus</span> <span class="dt">Arith</span> <span class="dt">Arith</span>
<span class="fu">|</span> <span class="dt">Minus</span> <span class="dt">Arith</span> <span class="dt">Arith</span>
<span class="fu">|</span> <span class="dt">Times</span> <span class="dt">Arith</span> <span class="dt">Arith</span></code></pre></div>
<p>And a program is an <code>Arith</code>. For example, the source expression “1 + (2 * 4)” is represented as <code>Plus 1 (Times 2 4)</code>. 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:</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="kw">data</span> <span class="dt">StackOp</span> <span class="fu">=</span> <span class="dt">SNum</span> <span class="dt">Int</span>
<span class="fu">|</span> <span class="dt">SPlus</span>
<span class="fu">|</span> <span class="dt">SMinus</span>
<span class="fu">|</span> <span class="dt">STimes</span></code></pre></div>
<p>And a program is a <code>[StackOp]</code>. For example, the previous example “1 + (2 * 4)” could be represented as <code>[SNum 1, SNum 2, SNum 4, STimes, SPlus]</code>. 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 <code>eval</code> 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).</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">eval ::</span> [<span class="dt">Int</span>] <span class="ot">-></span> [<span class="dt">StackOp</span>] <span class="ot">-></span> <span class="dt">Either</span> ([<span class="dt">Int</span>], [<span class="dt">StackOp</span>]) <span class="dt">Int</span>
eval (n<span class="fu">:</span>_) [] <span class="fu">=</span> <span class="dt">Right</span> n
eval ns (<span class="dt">SNum</span> n<span class="fu">:</span>xs) <span class="fu">=</span> eval (n<span class="fu">:</span>ns) xs
eval (n1<span class="fu">:</span>n2<span class="fu">:</span>ns) (<span class="dt">SPlus</span><span class="fu">:</span>xs) <span class="fu">=</span> eval (n1<span class="fu">+</span>n2<span class="fu">:</span>ns) xs
eval (n1<span class="fu">:</span>n2<span class="fu">:</span>ns) (<span class="dt">SMinus</span><span class="fu">:</span>xs) <span class="fu">=</span> eval (n1<span class="fu">-</span>n2<span class="fu">:</span>ns) xs
eval (n1<span class="fu">:</span>n2<span class="fu">:</span>ns) (<span class="dt">STimes</span><span class="fu">:</span>xs) <span class="fu">=</span> eval (n1<span class="fu">*</span>n2<span class="fu">:</span>ns) xs
eval vals instrs <span class="fu">=</span> <span class="dt">Left</span> (vals, instrs)</code></pre></div>
<p>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!</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">compile ::</span> <span class="dt">Arith</span> <span class="ot">-></span> [<span class="dt">StackOp</span>]
compile (<span class="dt">Num</span> n) <span class="fu">=</span> [<span class="dt">SNum</span> n]
compile (<span class="dt">Plus</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">SPlus</span>]
compile (<span class="dt">Minus</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">SMinus</span>]
compile (<span class="dt">Times</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">STimes</span>]</code></pre></div>
<p>The cases for plus/minus/times are the cases that are slightly non-obvious, because they can contain further recursive expressions, but if you think about what the <code>eval</code> function is doing, once the stack machine <em>finishes</em> evaluating everything that <code>a1</code> compiled to, the number that the left branch evaluated to should be on the top of the stack. Then once it finishes evaluating what <code>a2</code> compiles to the number that the right branch evaluated to should be on the top of the stack. This means that evaluating e.g. <code>SPlus</code> 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.</p>
<h2 id="formalizing">Formalizing</h2>
<p>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 <a href="https://github.com/antalsz/hs-to-coq">hs-to-coq</a> tool. There are full instructions at <a href="https://github.com/dbp/howtoproveacompiler" class="uri">https://github.com/dbp/howtoproveacompiler</a>, but the main command that will convert <code>src/Compiler.hs</code> to <code>src/Compiler.v</code>:</p>
<pre><code>STACK_YAML=hs-to-coq/stack.yaml stack exec hs-to-coq -- -o src/ src/Compiler.hs -e hs-to-coq/base/edits</code></pre>
<p>You can now build the Coq code with</p>
<pre><code>make</code></pre>
<p>And open up <code>src/Proofs.v</code> using a Coq interactive mode (I use Proof General within Emacs; with Spacemacs, this is particularly easy: use the <code>coq</code> layer!).</p>
<h2 id="proving-things">Proving things</h2>
<p>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, <a href="https://williamjbowman.com/blog/2017/03/24/what-even-is-compiler-correctness/">What even is compiler correctness?</a>). In languages with ambiguity (nondeterminism, undefined behavior, this becomes much more complicated, but in our setting, we would state it as:</p>
<p><strong>Theorem (informal). For all source arith expressions A, if eval [] (compile A) produces integer N then evaluating A should produce the same number N.</strong></p>
<p>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).</p>
<p>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.</p>
<p>So we should add this function to our Haskell source. In a non-trivial 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:</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">eval' ::</span> <span class="dt">Arith</span> <span class="ot">-></span> <span class="dt">Int</span>
eval' (<span class="dt">Num</span> n) <span class="fu">=</span> n
eval' (<span class="dt">Plus</span> a1 a2) <span class="fu">=</span> (eval' a1) <span class="fu">+</span> (eval' a2)
eval' (<span class="dt">Minus</span> a1 a2) <span class="fu">=</span> (eval' a1) <span class="fu">-</span> (eval' a2)
eval' (<span class="dt">Times</span> a1 a2) <span class="fu">=</span> (eval' a1) <span class="fu">*</span> (eval' a2)</code></pre></div>
<p>And we can re-run <code>hs-to-coq</code> to get it added to our Coq development. We can now formally state the theorem we want to prove as:</p>
<pre><code>Theorem compiler_correctness : forall a : Arith,
eval nil (compile a) = Data.Either.Right (eval' a).</code></pre>
<p>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:</p>
<ul>
<li>Bertot and Casteron’s <a href="https://archive.org/details/springer_10.1007-978-3-662-07964-5">Coq’Art: Interactive Theorem Proving and Program Development</a>.</li>
<li>Adam Chlipala’s <a href="http://adam.chlipala.net/cpdt/">Certified Programming with Dependent Types</a></li>
<li>Pierce et. al.’s <a href="https://softwarefoundations.cis.upenn.edu/">Software Foundations</a></li>
</ul>
<p>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:</p>
<pre><code>induction a; iauto; simpl.</code></pre>
<p>We see (above the line is assumptions, below what you need to prove):</p>
<pre><code>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</code></pre>
<p>Which, if we look at it for a little while, we realize two things:</p>
<ol style="list-style-type: decimal">
<li>Our induction hypotheses really aren’t going to work, intuitively because of the <code>Either</code> — our program won’t produce <code>Right</code> results for the subtrees, so there probably won’t be a way to rely on these hypotheses.</li>
<li>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 <code>eval</code>ing a <code>compile</code>d term will result in the <code>eval'</code>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:</li>
</ol>
<pre><code>Lemma eval_step : forall a : Arith, forall xs : list StackOp,
eval nil (compile a ++ xs) = eval (eval' a :: nil) xs.</code></pre>
<p>This is more general, and again we start by inducting on <code>a</code>, expanding and eliminating the base case:</p>
<pre><code>induction a; intros; simpl; iauto.</code></pre>
<p>We now end up with <em>better</em> inductive hypotheses:</p>
<pre><code> 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</code></pre>
<p>We need to reshuffle the list associativity and then we can rewrite using the first hypotheses:</p>
<pre><code>rewrite List.app_assoc_reverse. rewrite IHa1.</code></pre>
<p>But now there is a problem (this is <em>common</em>, hence going over it!). We want to use our second hypothesis. Once we do that, we can reduce based on the definition of <code>eval</code> and we’ll be done (with this case, but multiplication is the same). The issue is that <code>IHa2</code> needs the stack to be empty, and the stack we now have (since we used <code>IHa1</code>) is <code>eval' a1 :: nil</code>, so it can’t be used:</p>
<pre><code> 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</code></pre>
<p>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:</p>
<pre><code>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.</code></pre>
<p>Now if we start the proof in the same way:</p>
<pre><code>induction a; intros; simpl; iauto.</code></pre>
<p>We run into an odd problem. We have a silly obligation:</p>
<pre><code> match s with
| nil => eval (i :: s) xs
| (_ :: nil)%list => eval (i :: s) xs
| (_ :: _ :: _)%list => eval (i :: s) xs
end = eval (i :: s) xs</code></pre>
<p>Which will go away once we break apart the list <code>s</code> 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:</p>
<ol style="list-style-type: decimal">
<li>We could just do it manually: <code>destruct s; simpl; eauto; destruct s; simpl; eauto</code>. 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.</li>
<li><p>We could write a tactic for the same thing:</p>
<pre><code>try match goal with
|[l : list _ |- _ ] => solve [destruct l; simpl; eauto; destruct l; simpl; eauto]
end.</code></pre>
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 <code>Hint Extern</code>) 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.</li>
<li><p>We can also write lemmas for these. There are actually two cases that come up, and both are solved easily:</p>
<pre><code>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.</code></pre>
<p>In this style, we can then hint using these lemmas locally to where they are needed.</p></li>
</ol>
<p>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 <code>literatecoq</code> library, which is just a few tactics at this point) as:</p>
<pre><code>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.</code></pre>
<p>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.</p>
<p>We can then go back to our main theorem, and proceed in a similar style. We prove by induction, relying on the <code>eval_step</code> lemma, and in various places needing to simplify (for the observant reader, <code>iauto</code> and <code>iauto'</code> only differ in that <code>iauto'</code> does a deeper proof search).</p>
<pre><code>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.</code></pre>
<p>We now have a proof that the compiler that we wrote in Haskell is correct, insofar as it preserves the meaning expressed in the source-level <code>eval'</code> function to the meaning in the <code>eval</code> 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 <code>Left</code> error).</p>
<blockquote>
<p>As stated at the top of the post, all the code in this post is available at <a href="https://github.com/dbp/howtoproveacompiler" class="uri">https://github.com/dbp/howtoproveacompiler</a>. If you are looking for more, check out <a href="https://xavierleroy.org/courses/Eugene-2012/">Xavier Leroy’s Oregon Programming Languages Summer School Lectures</a> (videos are <a href="https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html">here</a>, scroll down to find them).</p>
</blockquote>
<p><br /></p>
<p>Thanks to current and former <a href="http://prl.ccs.neu.edu">PRL</a> members, in particular <a href="http://gallium.inria.fr/~scherer/">Gabriel Scherer</a> and <a href="https://williamjbowman.com/">William Bowman</a>, for providing useful feedback on drafts of this post.</p>
<p><br /><br /></p>
<h2 id="addendum-termination">Addendum: termination</h2>
<p>This example was so tiny we haven’t run into something that <em>will</em> be really common: imagine instead of the compile function shown above:</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">compile ::</span> <span class="dt">Arith</span> <span class="ot">-></span> [<span class="dt">StackOp</span>]
compile (<span class="dt">Num</span> n) <span class="fu">=</span> [<span class="dt">SNum</span> n]
compile (<span class="dt">Plus</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">SPlus</span>]
compile (<span class="dt">Minus</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">SMinus</span>]
compile (<span class="dt">Times</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">STimes</span>]</code></pre></div>
<p>We instead wanted to take <code>[Arith]</code>. This would still work, and would result in the list of results stored on the stack (so probably you would want to change <code>eval</code> to print everything that was on the stack at the end, not just the top). If you wrote this <code>compile</code>:</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">compile ::</span> [<span class="dt">Arith</span>] <span class="ot">-></span> [<span class="dt">StackOp</span>]
compile [] <span class="fu">=</span> []
compile (<span class="dt">Num</span> n<span class="fu">:</span>xs) <span class="fu">=</span> <span class="dt">SNum</span> n <span class="fu">:</span> compile xs
compile (<span class="dt">Plus</span> a1 a2<span class="fu">:</span>xs) <span class="fu">=</span> compile [a2] <span class="fu">++</span> compile [a1] <span class="fu">++</span> <span class="dt">SPlus</span> <span class="fu">:</span> compile xs
compile (<span class="dt">Minus</span> a1 a2<span class="fu">:</span>xs) <span class="fu">=</span> compile [a2] <span class="fu">++</span> compile [a1] <span class="fu">++</span> <span class="dt">SMinus</span> <span class="fu">:</span> compile xs
compile (<span class="dt">Times</span> a1 a2<span class="fu">:</span>xs) <span class="fu">=</span> compile [a2] <span class="fu">++</span> compile [a1] <span class="fu">++</span> <span class="dt">STimes</span> <span class="fu">:</span> compile xs</code></pre></div>
<p>You would get an error when you try to compile the output of <code>hs-to-coq</code>! Coq says that the compile function is not terminating!</p>
<p>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 <em>prove</em> things, this feature would be a non-starter, 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:</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">anything ::</span> a
anything <span class="fu">=</span> anything</code></pre></div>
<p>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).</p>
<p>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 <code>Arith</code> expressions) and that all recursive calls are to <em>structurally smaller</em> parts of the arguments. If that holds, we are guaranteed to terminate, as inductive types cannot be infinite (note: unlike Haskell, Coq is <em>not</em> lazy, which is another difference, but we’ll ignore that). If we look at our recursive call, we called <code>compile</code> with <code>[a1]</code>. While <code>a1</code> is structurally smaller, we put that inside a list and used that instead, which thus violates what Coq was expecting.</p>
<p>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 <code>compile'</code> that does what our original <code>compile</code> did: compiles a single <code>Arith</code>. The intuition that leads to trying this is that in this new <code>compile</code> we are decreasing on both the length of the list and the structure of the <code>Arith</code>, but we are trying to do both at the same time. By separating things out, we can eliminate the issue:</p>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">compile ::</span> [<span class="dt">Arith</span>] <span class="ot">-></span> [<span class="dt">StackOp</span>]
compile [] <span class="fu">=</span> []
compile (x<span class="fu">:</span>xs) <span class="fu">=</span> compile' x <span class="fu">++</span> compile xs
<span class="ot">compile' ::</span> <span class="dt">Arith</span> <span class="ot">-></span> [<span class="dt">StackOp</span>]
compile' (<span class="dt">Num</span> n) <span class="fu">=</span> [<span class="dt">SNum</span> n]
compile' (<span class="dt">Plus</span> a1 a2) <span class="fu">=</span> compile' a2 <span class="fu">++</span> compile' a1 <span class="fu">++</span> [<span class="dt">SPlus</span>]
compile' (<span class="dt">Minus</span> a1 a2) <span class="fu">=</span> compile' a2 <span class="fu">++</span> compile' a1 <span class="fu">++</span> [<span class="dt">SMinus</span>]
compile' (<span class="dt">Times</span> a1 a2) <span class="fu">=</span> compile' a2 <span class="fu">++</span> compile' a1 <span class="fu">++</span> [<span class="dt">STimes</span>]</code></pre></div>
<h2 id="addendum-do-the-proofs-mean-anything">Addendum: do the proofs mean anything?</h2>
<p>There are limitations to the approach outlined in this post. In particular, what <code>hs-to-coq</code> 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 <a href="http://www.chargueraud.org/softs/cfml/">CFML</a>), but on the other hand, program extraction (which is a core part of verified compilers like <a href="http://compcert.inria.fr/">CompCert</a>) has the same issue that the program being run has been converted via a similar process as <code>hs-to-coq</code> (from Coq to OCaml the distance is less than from Coq to Haskell, but in principle there are similar issues).</p>
<p>And yet, I think that <code>hs-to-coq</code> 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 <code>hs-to-coq</code> 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 <code>hs-to-coq</code> 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 Gallina-like dialect of Haskell) seems incredibly valuable.</p>
</body>
</html>