Ready, Set, Verify!

arXiv:1803.06960v2 [cs.PL] 20 Mar 2018

Applying hs-to-coq to real-world Haskell code

JOACHIM BREITNER, University of Pennsylvania, USA
ANTAL SPECTOR-ZABUSKY, University of Pennsylvania, USA
YAO LI, University of Pennsylvania, USA
CHRISTINE RIZKALLAH, University of New South Wales, Australia
JOHN WIEGLEY, BAE Systems, USA
STEPHANIE WEIRICH, University of Pennsylvania, USA
Good tools can bring mechanical verification to programs written in mainstream functional languages. We use
hs-to-coq to translate significant portions of Haskell’s containers library into Coq, and verify it against
specifications that we derive from a variety of sources including type class laws, the library’s test suite, and
interfaces from Coq’s standard library. Our work shows that it is feasible to verify mature, widely-used, highly
optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend
hs-to-coq to handle partiality, and – since we found no bugs – attest to the superb quality of well-tested
functional code.
CCS Concepts: • Software and its engineering → Software verification;
Additional Key Words and Phrases: Coq, Haskell, verification

1

INTRODUCTION

What would it take to tempt functional programmers to verify their code?
Certainly, better tools would help. We see that functional programmers who use dependentlytyped languages or proof assistants, such as Coq [The Coq development team 2016], Agda [Bove
et al. 2009], Idris [Brady 2017], and Isabelle [Nipkow et al. 2002], do verify their code, since their
tools allow it. However, adopting these platforms means rewriting everything from scratch. What
about the verification of existing code, such as libraries written in mature languages like Haskell?
Haskell programmers can reach for LiquidHaskell [Vazou et al. 2014] which smoothly integrates
the expressive power of refinement types with Haskell, using SMT solvers for fully automatic
verification. But some verification endeavors require the full strength of a mature interactive proof
assistant like Coq. The hs-to-coq tool, developed by Spector-Zabusky, Breitner, Rizkallah, and
Weirich [2018], translates Haskell types, functions and type classes into equivalent Coq code – a
form of shallow embedding – which can be verified just like normal Coq definitions.
But can this approach be used for more than the small, textbook-sized examples it has been
applied to so far? Yes, it can! In this work, we use hs-to-coq to translate and verify the two set
data structures from Haskell’s containers package.1 This codebase is not a toy. It is decades old,
highly tuned for performance, type-class polymorphic, and implemented in terms of low-level
features like bit manipulation operators and raw pointer equality. It is also an integral part of the
Haskell ecosystem. We make the following contributions:
1 Specifically,

we target version 0.5.11.0, which was released on January 22, 2018 and was the most recent release of this
library at the time of publication; it is available at https://github.com/haskell/containers/tree/v0.5.11.0.

Authors’ addresses: Joachim Breitner, joachim@cis.upenn.edu, University of Pennsylvania, 3330 Walnut St, Philadelphia,
PA, 19104, USA; Antal Spector-Zabusky, antals@cis.upenn.edu, University of Pennsylvania, 3330 Walnut St, Philadelphia,
PA, 19104, USA; Yao Li, liyao@cis.upenn.edu, University of Pennsylvania, 3330 Walnut St, Philadelphia, PA, 19104, USA;
Christine Rizkallah, criz@cis.upenn.edu, University of New South Wales, Sydney, NSW, Australia; John Wiegley, john.
wiegley@baesystems.com, BAE Systems, USA; Stephanie Weirich, sweirich@cis.upenn.edu, University of Pennsylvania,
3330 Walnut St, Philadelphia, PA, 19104, USA.

2

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich
• We demonstrate that hs-to-coq is suitable for the verification of unmodified, real-world
Haskell libraries. By “real-world”, we mean code that is up-to-date, in common use, and
optimized for performance. In Section 2 we describe the containers library in more detail
and discuss why it fits this description.
• We present a case study not just of verifying a popular Haskell library, but also of developing
a good specification of that library. This process is worth consideration because it is not at all
obvious what we mean when we say that we have “verified” a library. Section 4 discusses the
techniques that we have used to construct a rich, two-sided specification; one that draws
from diverse, cross-validated sources and yet is suitable for verification.
• We extend hs-to-coq and its associated standard libraries to support our verification goal. In
particular, in Section 5 we describe the challenges that arise when translating the Data.Set
and Data.IntSet modules, and our solutions. Notably, we drop the restriction in previous
work [Spector-Zabusky et al. 2018] that the input of the translation must be intrinsically
total. Instead, we show how to safely defer reasoning about incomplete pattern matching
and potential nontermination to later stages of the verification process.
• We increase confidence in the translation done of hs-to-coq. In one direction, properties
of the Haskell test suite turn into Coq theorems that we prove. In the other direction, the
translated code, when extracted back to Haskell, passes the original test suite.
• We provide new implementation-agnostic insight into the verification of the weight-balanced
tree data structure, as we describe in Section 6. In particular, we find the right precondition
for the central balancing operations needed to verify the particular variant used in Data.Set.

Our work provides a rich specification for Haskell’s finite set libraries that is directly and
mechanically connected to the current implementation. As a result, Haskell programmers can be
assured that these libraries behave as expected. Of course, there is a limit to the assurances that we
can provide through this sort of effort. We discuss the verification gap and other limitations of our
approach in Section 7.
We would like to have been able to claim the contribution of findings bugs in containers, but
there simply were none. Still, our efforts resulted in improvements to the containers library. First,
an insight during the verification process led to an optimization that makes the Data.Set.union
function 4% faster. Second, we discovered an incompleteness in the specification of the validity
checker used in the test suite.
The tangible artifacts of this work have been incorporated into the hs-to-coq distribution and
are available as open source tools and libraries.2
2

THE containers LIBRARY

We select the containers library for our verification efforts because it is a critical component of
the Haskell ecosystem. With over 4000 publicly available Haskell packages using on containers,
it is the third-most dependent-up package on the Haskell package repository Hackage, after base
and bytestring.3
The containers library is both mature and highly optimized. It has existed for over a decade
and has undergone many significant revisions in order to improve its performance. It contains
seven container data structures, covering support for finite sets (Data.Set and Data.IntSet),
finite maps (Data.Map and Data.IntMap), sequences (Data.Sequence), graphs (Data.Graph), and
trees (Data.Tree). However most users of the containers library only use the map and set
2 https://github.com/antalsz/hs-to-coq.
3 http://packdeps.haskellers.com/reverse

Ready, Set, Verify!

3

---------------------------------------------------------------------Sets are size balanced trees
-------------------------------------------------------------------data Set a = Bin {-# UNPACK #-} !Size !a !(Set a) !(Set a)
| Tip
type Size = Int
--| O(log n). Is the element in the set?
member :: Ord a => a -> Set a -> Bool
member = go
where go !_ Tip = False
go x (Bin _ y l r) = case compare x y of
LT -> go x l
GT -> go x r
EQ -> True
Fig. 1. The Set data type and its membership function5

modules;4 moreover, the map modules are essentially analogues of the set modules. Therefore, we
focus on Data.Set and Data.IntSet in this work.
2.1

Weight-balanced trees and big-endian Patricia trees

The Data.Set module implements finite sets using weight-balanced binary search trees. The
definition of the Set datatype in this module, along with its membership function, is given in
Figure 1. These sets and operations are polymorphic over the element type and require only that
this type is linearly ordered, as expressed by the Ord constraint on the member function. The member
function descends the ordered search tree to determine whether it contains a particular element.
The Size component stored with the Bin constructor is used by the operations in the library to
ensure that the tree stays balanced. The implementation maintains the balancing invariant
s 1 + s 2 ≤ 1 ∨ (s 1 ≤ 3s 2 ∧ s 2 ≤ 3s 1 ),
where s 1 and s 2 are the sizes of the left and right subtrees of a Bin constructor. This definition
is based on the description by Adams [1992], who modified the original weight-balanced tree
proposed by Nievergelt and Reingold [1972]. Thanks to this balancing, operations such as insertion,
membership testing, and deletion take time logarithmic in the size of the tree.
This type definition has been tweaked to improve the performance of the library. The annotations
on the Bin data constructor instruct the compiler to unpack the size component, removing a level
of indirection. The ! annotations indicate that all components should be strictly evaluated.
The Data.IntSet module also provides search trees, specialized to values of type Int to provide
more efficient operations, especially union. This implementation is based on big-endian Patricia
trees, as proposed in Morrison’s work on PATRICIA [1968] and described in a pure functional
setting by Okasaki and Gill [1998].
The definition of this data structure is shown in Figure 2. The core idea is to use the bits of the
stored values to decide in which subtree of a node they should be placed. In a node Bin p m s1 s2,
the mask m has exactly one bit set. All bits higher than the mask bit are equal in all elements of
calculated that 78% of the packages on Hackage that depend on containers use only sets and maps.
http://hackage.haskell.org/package/containers-0.5.11.0/docs/src/Data.Set.Internal.html#Set.
All code listings in this paper are manually reformatted and may omit module names from fully qualified names.
4 We

5 From

4

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

data IntSet = Bin {-# UNPACK #-} !Prefix {-# UNPACK #-} !Mask !IntSet !IntSet
--Invariant: Nil is never found as a child of Bin.
--Invariant: The Mask is a power of 2. It is the largest bit position at
-which two elements of the set differ.
--Invariant: Prefix is the common high-order bits that all elements share to
-the left of the Mask bit.
--Invariant: In Bin prefix mask left right, left consists of the elements
-that don't have the mask bit set; right is all the elements
-that do.
| Tip {-# UNPACK #-} !Prefix {-# UNPACK #-} !BitMap
--Invariant: The Prefix is zero for the last 5 (on 32 bit arches) or 6 bits
-(on 64 bit arches). The values of the set represented by a tip
-are the prefix plus the indices of the set bits in the bit map.
| Nil
--A number stored in a set is stored as
--* Prefix (all but last 5-6 bits) and
--* BitMap (last 5-6 bits stored as a bitmask)
-- Last 5-6 bits are called a Suffix.
type Prefix = Int
type Mask = Int
type BitMap = Word
type Key
= Int
Fig. 2. The IntSet data type6

that node; they form the prefix p. The mask bit is the highest bit that is not shared by all elements.
In particular, all elements in s1 have this bit cleared, while all elements in s2 have it set. When
looking up a value x, the mask bit of x tells us into which branch to descend.
Instead of storing a single value at the leaf of the tree, this implementation improves time and
space performance by storing the membership information of consecutive numbers as the bits of a
machine-word-sized bitmap in the Tip constructor.
The Nil constructor is the only way to represent an empty tree, and will never occur as the child
of a Bin constructor. Every well-formed IntSet is either made of Bins and Tips, or a single Nil.
2.2

A history of performance tuning

The history of the Data.Set module can be traced back to 2004, when a number of competing
search tree implementations were debated in the “Tree Wars” thread on the Haskell libraries mailing
list. Benchmarks showed that Daan Leijen’s implementation had the best performance, and it was
added to containers in 2005 as Data.Set.7
In 2010, Milan Straka thoroughly evaluated the performance of the containers library and
implemented a number of performance tweaks [Straka 2010]. This change8 replaced a fairly readable
balance and several small and descriptive helper functions with a single dense block of code. A
later change9 by Straka created two copies of this scary-looking balance, each specialized and
optimized for different preconditions.
6 From

http://hackage.haskell.org/package/containers-0.5.11.0/docs/src/Data.IntSet.Internal.html#IntSet

7 https://github.com/haskell/containers/commit/bbbba97c
8 https://github.com/haskell/containers/commit/3535fcbe
9 https://github.com/haskell/containers/commit/d17d7182

Ready, Set, Verify!

5

Adams [1992] describes two algorithms for union, intersection, and difference: “hedge
union” and “divide and conquer”. Originally containers used the former, but in 2016 its maintainers
switched to the latter,10 again based on performance measurement.
The module Data.IntSet (and Data.IntMap) has been around even longer. Okasaki and Gill
mention in their 1998 paper [Okasaki and Gill 1998] that GHC had already made use of IntSet and
IntMap for several years. In 2011, the Data.IntSet module was re-written to use machine-words
as bit maps in the leaves of the tree, as discussed at the end of Section 2.1.11 This moved the
containers library further away from the literature on Patricia trees and introduced a fair amount
of low-level bit twiddling operations (e.g., highestBitMask, lowestBitMask, and revNat).
3

OVERVIEW OF OUR VERIFICATION APPROACH

In order to verify Set and IntSet, we use hs-to-coq to translate the unmodified Haskell modules
to Gallina and then use Coq to verify the translated code. For example, consider the excerpt of the
implementation of Set in Figure 1. The hs-to-coq tool translates this input to the following Coq
definitions.12 The strictness and unpacking annotations are ignored, as they do not make sense in
Coq, and the type name Set is renamed to Set_ to avoid clashing with the Coq keyword.
Definition Size := GHC.Num.Int%type.
Inductive Set_ a : Type
:= Bin : Size -> a -> (Set_ a) -> (Set_ a) -> Set_ a
| Tip : Set_ a.
Definition member {a} `{GHC.Base.Ord a} : a -> Set_ a -> bool :=
let fix go arg_0__ arg_1__
:= match arg_0__, arg_1__ with
| _, Tip => false
| x, Bin _ y l r => match GHC.Base.compare x y with
| Lt => go x l
| Gt => go x r
| Eq => true
end
end
in go.
These definitions depend on hs-to-coq’s pre-existing translated version of GHC’s standard library
base. Here, we use the existing translation of Haskell’s Int type, the Ord type class, and Ord’s
compare method.
We carry out this translation for the Set and IntSet along with their attendant functions, and
then verify the resulting Gallina code. In Section 4 we discuss the properties that we prove about
the two data structures.
To further test that the translation from Haskell to Coq, we also used Coq’s extraction mechanism
to translate the generated Gallina code, like that seen above, back to Haskell. This process converts
the implicitly-passed type class dictionaries to ordinary explicitly-passed function arguments, but
otherwise preserves the structure of the code. By providing an interface that restores the typeclass based types, we can run the original containers test suite against this code. This process
10 https://github.com/haskell/containers/commit/c3083cfc
11 https://github.com/haskell/containers/pull/3
12 In

the file examples/containers/lib/Data/Set/Internal.v

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

Proofs

Gallina

Haskell

6

Set
IntSet
Tests
Set
IntSet

Headers, types and proof preparations
Functions and type class instances (verified)
(unverified)
"
(untranslated)
"
Tests and specifications

Tests
Lemmas about integers and bit-wise operations
Lemmas about lists and sortedness
A theory of dyadic intervals
Automation for reasoning about Ord
Set

IntSet

Instantiating Coq’s FSetInterface
Tests
0

500

1000

1500

2000

2500
3000
Lines of code

3500

4000

4500

5000

Fig. 3. A quantitative overview of the Haskell code, its translation into Coq and our proofs

helps us check that hs-to-coq preserves the semantics of the original Haskell program during the
translation process.
Figure 3 provides an overview of the Haskell code that we target, the Gallina code that we
translate it into, and the Coq proofs that we wrote. The set modules of the containers library
contain 149 functions and 22 type class instances, written in 2207 lines of code (excluding comments
and blank lines). Out of these, 15 functions and 11 type class instances (270 loc) were deemed “out
of scope” and not translated. (We discuss untranslated definitions in more detail in Sections 5.3
and 7.2.) Our translation produces 2709 lines of Gallina code.
The Set and IntSet data structures come with extensive APIs. We specify and verify a representative subset of commonly used functions (listed in Figure 4), covering 66% of the Set API and
49% of the IntSet API. This verified API is complete enough to instantiate Coq’s specification of
finite sets, along with many other specifications at varying levels of abstraction; for more detail,
see Section 4.
As Coq is not an automated theorem prover, verification of these complex data structures requires
significant effort. In total, we verified 1202 lines of Haskell; the verification of Set and IntSet
required 8.5 lines of proof per lines of code. This factor is noticeably higher for IntSet (10.0×) than
for Set (7.1×), as the latter is conceptually simpler to reason about and allowed us to achieve a
higher degree of automation using Coq tactics.
Our proofs also require the formalization of several background theories (not counted in the
proof-to-code ratio above), including: integer arithmetic and bits (1265 loc): lists and sortedness
(1489 loc); dyadic intervals, which are used for verifying IntSet (1169 loc); and support for working
with lawful Ord instances, including a complete decision procedure (453 loc).

Ready, Set, Verify!

7

Set: delete, deleteMax, deleteMin, difference, disjoint, drop, elems, empty, filter,
foldl, foldl’, foldr, foldr’, fromAscList, fromDescList, fromDistinctAscList,
fromDistinctDescList, insert, intersection, isSubsetOf, lookupMax, lookupMin,
mapMonotonic, maxView, member, minView, notMember, null, partition, singleton, size,
split, splitAt, splitMember, take, toAscList, toDescList, toList, union, unions
Instances: Eq, Eq1, Monoid, Ord, Ord1, Semigroup
Internal functions: balanceL, balanceR, combineEq, glue, insertMax, insertMin,
insertR, link, maxViewSure, merge, minViewSure, valid
IntSet: delete, difference, disjoint, elems, empty, filter, foldl, foldr, fromList,
insert, intersection, isProperSubsetOf, isSubsetOf, map, member, notMember, null,
partition, singleton, size, split, splitMember, toAscList, toDescList, toList,
union, unions
Instances: Eq, Monoid, Ord, Semigroup
Internal functions: branchMask, equal, highestBitMask, mask, nequal, nomatch,
revNat, shorter, valid, zero
Fig. 4. The verified subset of functions and type classes in Data.Set and Data.IntSet

4

SPECIFYING Set AND IntSet

The phrase “we have verified this piece of software” on its own is meaningless: the particular
specification that a piece of software is verified against matters. Good specifications are rich, twosided, formal, and live [Appel et al. 2017]. A specification is rich if it “describ[es] complex behaviors
in detail”. It is two-sided if it is “connected to both implementations and clients”. It is formal if it
is “written in a mathematical notation with clear semantics”. And it is live if it is “connected via
machine-checkable proofs to the implementation”.
All specifications of Set and IntSet that we use are formal and live by definition. They are
formal because we express the desired properties using Gallina, the language of the Coq proof
assistant; and they are live because we use hs-to-coq to automatically convert containers to
Coq where we develop and check our proofs. But how can we ensure that our specifications of Set
and IntSet are two-sided and rich? How do we know that the specifications are not just facts that
happen to be true, but are useful for the verification of larger systems? What complex behaviors of
the data structures should we specify?
To ensure that our specifications are two-sided, we use specifications that we did not invent
ourselves. Instead, we draw our specifications from a variety of diverse sources: from several parts
of the containers codebase (Sections 4.1 to 4.4), from Haskell type class laws (Section 4.5), from
pre-existing Coq theories (Section 4.6), and from a mathematical description of sets (Section 4.7).
This way, we also ensure that our specifications are rich because they describe the complex Set and
IntSet data structures at varying levels of abstraction. Finally, by verifying the code against these
disparate specifications, we not only increase the assurance that we captured all the important
behaviors of Set and IntSet, but we also cross-validate the specifications against each other.
4.1

Specifying implementation invariants

Set and IntSet are two examples of abstract types whose correctness depend on invariants.
Therefore, we define well-formedness predicates WF: Set_ e -> Prop and WF : IntSet -> Prop
and show that the operations preserve these properties. The definition of well-formedness differs
between the two types, but specifications of both are already present within containers.

8

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich
Inductive Bounded : Set_ e -> option e -> option e -> Prop :=
| BoundedTip : forall lb ub,
Bounded Tip lb ub
| BoundedBin : forall lb ub s1 s2 x sz,
Bounded s1 lb (Some x) ->
Bounded s2 (Some x) ub ->
isLB lb x = true -> (* If lb is defined, it is less than x *)
isUB ub x = true -> (* If ub is defined, it is greater than x *)
sz = (1 + size s1 + size s2) ->
balance_prop (size s1) (size s2) -> (* weights of tree are balanced *)
Bounded (Bin sz x s1 s2) lb ub.
(** Any set that has bounds is well-formed *)
Definition WF (s : Set_ e) : Prop := Bounded s None None.
Fig. 5. Well-formed weight-balanced sets

Well-formed weight-balanced trees. Our definition of WF for Set is derived from the valid function
defined in the containers library. This function checks whether the input (1) is a balanced tree,
(2) is an ordered tree, and (3) has the correct values in its size fields. It is not part of the normal,
user-facing API of containers (since all exported functions preserve well-formedness), but is
used internally by the developers for debugging and testing. For us, it is valuable as an executable
specification, with less room for ambiguity and interpretation than comments and documentation.
However, rather than using valid directly, we define well-formedness as an inductive predicate,
because we find it more useful from a proof engineering perspective. In particular, our definition
of WF, as shown in Figure 5, relies on the Bounded inductive family. Its indices express lower and
upper bounds of the elements stored in the tree; None means unbounded. At the same time, the
property also checks that the sizes of the two subtrees are balanced in the Bin case.13 Nevertheless,
we can relate the WF predicate to the valid function found in containers:
Lemma Bounded_iff_valid : forall s, WF s <-> valid s = true.
Well-formed Patricia trees. Our well-formedness definition for IntSet is derived from the comments in the IntSet data type, shown in Figure 2, where the type declaration of almost disappears
beneath a large swath of comments describing its invariants.
In this case, the documentation-derived well-formedness predicate is stronger than the corresponding valid function from the implementation – the Haskell function was missing some
necessary conditions. We reported this to the library authors,14 who have since fixed valid.
This fix to valid is an example of how verification allows us to cross-validate specifications
and ensure that the invariants written in the comments are adequately reflected by the code. On
the other hand, sometimes we discover that it is the comments in the code that are incomplete.
For example, the comment describing the precondition for balanceL in the Data.Set module was
misleading and too vague; for more detail, see Section 6.1.
13 In

the file examples/containers/theories/SetProofs.v

14 https://github.com/haskell/containers/issues/522

Ready, Set, Verify!
4.2

9

Property-based testing

At the next level of verification, we would like to show that the implementations of Set and IntSet
are correct according to the implementors of the module. We specify correctness by deriving a
definition directly from the test suite that is distributed with the containers library.
Thanks to the popularity of property-based testing within the Haskell community, this test suite
contains a wealth of precisely specified general properties expressed using QuickCheck [Claessen
and Hughes 2000]. For example, one such property states that the union operation is associative:
prop_UnionAssoc :: IntSet -> IntSet -> IntSet -> Bool
prop_UnionAssoc t1 t2 t3 = union t1 (union t2 t3) == union (union t1 t2) t3
which we can interpret as a theorem about union:15
Theorem thm_UnionAssoc:
forall t1, WF t1 -> forall t2, WF t2 -> forall t3, WF t3 ->
union t1 (union t2 t3) == union (union t1 t2) t3 = true.
We do not have to write these theorems by hand: as we describe in Section 5.8, we use hs-to-coq in
a nonstandard way to automatically turn these executable tests into Gallina propositions (i.e. types).
We have have translated IntSet’s test suite in this manner and have proven that all QuickCheck
properties about verified IntSet functions are theorems (with one exception due to our choice of
integer representation – see Section 5.5).
4.3

Numeric overflow in Set

There is one way in which we have diverged from the specification of correctness given by the
comments of the containers library. The Data.Set module states:16
Warning: The size of the set must not exceed maxBound::Int. Violation of this condition is not detected and if the size limit is exceeded, its behavior is undefined.
In practice, it makes no difference whether Int is bounded or not, as a set with (263 − 1) elements
would require at least 368 exabytes of storage. What does this imply for our specification of
Set? Should we use fixed-width integers to represent Int? This choice would closely match the
implementation, but we would have to carefully add preconditions to all our lemmas to avoid integer
overflow, greatly complicating the proofs, with little verification insight to be gained. Furthermore,
such a specification would be difficult to use by clients, who themselves would need to prove that
they satisfy such preconditions.
Instead, we translate Haskell’s Int type to Coq’s type of unbounded integers (called Z). This
mapping avoids the problem of integer overflow altogether and is arguably consistent with the
comment, as this choice replaces undefined behavior with concrete behavior. (The situation is
slightly different for IntSet; see Section 5.5.)
4.4

Rewrite rules

So far, we have only been concerned with specifying the correctness of the data structures using
the definition of correctness that is present in the original source code; the comments, the valid
functions and the QuickCheck properties. However, to be able to claim that our specifications are
two-sided, we need to show that the properties that we prove are useful to clients of the module.
One source of such properties is rewrite rules [Peyton Jones et al. 2001]. The containers library
includes a small number of such rules. These annotations instruct the compiler to replace any
15 In

the file examples/containers/theories/IntSetPropertyProofs.v

16 http://hackage.haskell.org/package/containers-0.5.11.0/docs/Data-Set.html

10

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

Class OrdLaws (t : Type) {HEq : Eq_ t} {HOrd : Ord t} {HEqLaw : EqLaws t} := {
(* The axioms *)
Ord_antisym
: forall a b, a <= b = true -> b <= a = true -> a == b = true;
Ord_trans_le : forall a b c, a <= b = true -> b <= c = true -> a <= c = true;
Ord_total
: forall a b, a <= b = true \/ b <= a = true;
(* The other operations, in terms of <= or == *)
Ord_compare_Lt : forall a b, compare a b = Lt <-> b <= a = false;
Ord_compare_Eq : forall a b, compare a b = Eq <-> a == b = true;
Ord_compare_Gt : forall a b, compare a b = Gt <-> a <= b = false;
Ord_lt_le
: forall a b, a < b = negb (b <= a);
Ord_ge_le
: forall a b, a >= b =
(b <= a);
Ord_gt_le
: forall a b, a > b = negb (a <= b)}.
Fig. 6. Our codification of the Ord type class laws

occurrence of the pattern on the left-hand side in the rule by the expression on the right hand side.
The standard example is
{-# RULES "map/map" forall f g xs. map f (map g xs) = map (f . g) xs #-}
which fuses two adjacent calls to map into one, eliminating the intermediate list.
The program transformation list fusion [Peyton Jones et al. 2001] is implemented completely in
terms of rewrite rules, and the rules in the containers library setup its functions for fusion; an
example is
{-# RULES "Set.toAscList" forall s . toAscList s = build (\c n -> foldrFB c n s) #-}
which transforms the toAscList function into an equivalent representation in terms of build.
We can view these rewrite rules as a direct specification of properties that the compiler assumes
are true during compilation. Rewrite rules are used by GHC during optimization; if any of these
properties are actually false, GHC will silently produce incorrect code. Therefore, any proof about
the correctness of GHC’s compilation of these files depends on a proof of these properties. We have
manually translated all the rules into Coq – there are only few of them, so manual translation is
viable – and have proved that the translated operations satisfy this specification.17
4.5 Type classes with laws
Many Haskell type classes come with laws that all instances of the type class should satisfy, which
provides another source of external specification that we can use. For example, an instance of Eq is
expected to implement an equivalence relation, an instance of Ord should describe a linear order,
and an instance of Monoid should be, well, a monoid.
We reflect these laws using type classes whose members are the required properties. For example,
we have defined EqLaws, OrdLaws (shown in Figure 6), and MonoidLaws. These classes can only be
instantiated if the corresponding instance is lawful.
Even though we have defined these laws ourselves, using our understanding of what they mean
for the Haskell standard library, we argue that they form a two-sided specification. In particular, we
have been clients to the Ord laws in our verification of the Set data structure. Almost all theorems
about Set must constrain the element type to one that is an instance of OrdLaws. Therefore, we
know our specification of these laws is sufficiently strong to verify this library.
17 In

the files examples/containers/theories/SetProofs.v and examples/containers/theories/IntSetProofs.v

Ready, Set, Verify!

11

At the same time, we have also shown that multiple type class instances satisfy these laws
including both set modules18 and other types such as Z, unit, tuples, option, and list.19 Because
we successfully instantiated these type classes for many types, we also know that they are not too
strong.
That said, nailing down the precise form of the type class laws can be tricky. Consider the case
of a Monoid instance for a type T. The associativity law can be stated as “for all elements x, y and z
of T, we have that x <> (y <> z) is equal to (x <> y) <> z.” But in order to write this down as part
of MonoidLaws in Coq, we need to make two decisions:
(1) What do we mean by “equal”? The first option is to use Coq’s propositional equality and
require that x <> (y <> z) = (x <> y) <> z. This would, however, prevent us from making
Set_, with (<>) = union, a member of MonoidLaws: two extensionally-equal sets may be
represented by differently structured trees. Therefore, we instead require that the two expressions are equal according to their Eq instance:(x <> (y <> z) == (x <> y) <> z) = true. The
tradeoff with this approach is that it precludes instances like MonoidLaws b -> MonoidLaws
(a -> b), since functions have no instance of Eq (and indeed, cannot have decidable equality).
For many types, however, this distinction is moot, since Haskell’s equality coincides with
structural equality; for example, this is the case for Bool, for Integer, and for IntSet itself
(although not for Set, as mentioned above). To facilitate reasoning about such types, we
provide the type class EqExact, which states that
forall {a} `{EqExact a}, x == y = true <-> x = y
(2) What do we mean by “For all elements of T”? The obvious choice is universal quantification
over all elements of T:
forall (x y z : T), x <> (y <> z) == (x <> y) <> z = true
But again, this collides with common practice in Haskell. Once again, consider Set: union
only works correctly on well-formed sets. Therefore, our approach is to define an instance
of this and other classes not for the type Set_ e, but for the type of well-formed sets, {s :
Set_ e | WF s}, where type class laws hold universally. This instance reflects the “external
view” of the data structure – clients should only have access to well-formed sets.
An alternative could be to instead constrain MonoidLaws’s theorems to hold only on members
of T that are well-formed in some general way (e.g., according to an IsWF type class that could
be instantiated at different types). In this way, we could instantiate MonoidLaws directly with
types that require well-formedness, without the need for subset types.
4.6

Specifications from the Coq standard library

Because we are working in Coq, we have access to a standard library of specifications for finite sets,
which we know are two-sided because they have already appeared in larger Coq developments. The
Coq.FSets.FSetInterface module20 provides module types that cover many common operations
and their properties. The module types come in two varieties: one that specifies sets of elements
that merely have decidable equality (WSfun, WS), and one that specifies sets of elements that can
be linearly ordered (Sfun, S). The WSfun and Sfun modules are presented as module functors that
take an OrderedType module, containing the linearly-ordered element type, as an input; the WS
and S modules are the same, but they inline this information.
18 In

the files examples/containers/theories/SetProofs.v and examples/containers/theories/IntSetProofs.v
the file base-thy/GHC/Base.v
20 https://coq.inria.fr/library/Coq.FSets.FSetInterface.html

19 In

12

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

For example, the parameterized module type WSfun provides one specification of a finite set type,
called t in the excerpt from this interface below. The element type of this set, E.t, is required to
have decidable equality.
Module Type WSfun (E : DecidableType).
Definition elt := E.t.
Parameter t : Type.
(* Set type *)
Parameter In : elt -> t -> Prop. (* Characteristic function for the Set *)
Parameter mem : elt -> t -> bool. (* Membership function *)
(* Specification of mem *)
Parameter mem_1 : forall x s, In x s -> mem x s = true.
Parameter mem_2 : forall x s, mem x s = true -> In x s.
...
End WSFun.
Every operation in this interface, such as mem above, is accompanied by a small number of properties
that specify the behavior of the operation.
We instantiate all four interfaces for Set and IntSet.21 For example, the instance for Set starts
out:
Module SetFSet (E : OrderedType) <: WSfun(E) <: WS <: Sfun(E) <: S.
Definition t := {s : Set_ elt | WF s}.
Program Definition In (x :elt) (s : t) : Prop := . . . .
Program Definition mem : elt -> t -> bool := member.
Lemma mem_1 : forall (s : t) (x : elt), In x s -> mem x s = true.
Proof. . . . (* Proof may assume that s is well-formed *) . . . Qed.
...
End SetFSet.
Instantiating these interfaces runs into two small hiccups. The first is that they talk about all
sets, not simply all well-formed sets. Therefore, as in the previous section, we instantiate these
interfaces with the subset type {s : Set_ e | WF s}. The second is that Coq’s module system does
not interact with type classes, and Set_ is defined such that its element type must be an instance
of the Ord type class. This impedance mismatch requires us to write a module which can generate
an Ord instance from a Coq OrderedType module.
By successfully instantiating this module interface, we obtain two benefits. First, we must
prove theorems that cover many of the main functions provided by containers; these theorems
are particularly valuable, since as the interface itself is heavily used by Coq users. Second, by
instantiating this interface, we connect our injected Haskell code to the Coq ecosystem, enabling
Coq users to easily use the containers-derived data structures in their developments, should they
so desire.
4.7

Abstract models as specifications

Tests, type classes and the other sources of specifications do not fully describe the intended behavior
of all functions. We therefore also have to also come up with specifications on our own. We do
21 In

the files examples/containers/theories/SetProofs.v and examples/containers/theories/IntSetProofs.v

Ready, Set, Verify!

13

this by relating a concrete search tree to the abstract set that it represents; that is, we provide a
denotational semantics. We denote a set with elements of type e as its indicator function of type
e -> bool; for Set e, we provide a denotation function sem : forall {e} `{Eq_ e}, Set_ e ->
(e -> bool), and for IntSet, we provide a denotation relation Sem : IntSet -> (N -> bool) ->
Prop.
This approach allows us to abstractly describe the meaning of operations like insert. For Set_,
we do this by providing a theorem like
Theorem insert_sem:
forall {a} `{OrdLaws a} (s : Set_ a) (x : a), WF s ->
forall (i : a), sem (insert x s) i = (i == x) || sem s i.
(For IntSet, some techincal details differ.) However, there is more we need to know about insert
than just its denotation. We also need to know that it preserves well-formedness and bounds, and
– to reason about balancing – its size. To avoid having to prove these properties independently,
we define a relation Desc that completely describes a set, by asserting that it is well-founded and
relating it to bounds, its size and its denotation:
Definition Desc (s : Set _e) (lb ub : option e) (sz : Z) (f : e -> bool) :=
Bounded s lb ub /\ size s = sz /\ (forall i, sem s i = f i).
This allows us to state a single theorem about insert, namely
Lemma insert_Desc: forall x s lb ub,
Bounded s lb ub ->
isLB lb x = true -> (* If lb is defined, it is less than x *)
isUB ub x = true -> (* If ub is defined, it is greater than x *)
Desc (insert x s) lb ub
(if sem s y then size s else (1 + size s)) (fun i => (i == x) || sem s i).
and prove everything we need to know about insert in one single inductive proof.22
Since Desc describes insert completely, it introduces a layer of abstraction that we can build
upon. In fact, we specify all functions this way, and use these specifications, rather than the concrete
implementation, to prove the other specifications. (We have an analogous Desc relation for IntSet
that describes the properties of Patricia trees.)
An alternative abstract model for finite sets is the sorted list of their elements, i.e. the result of
toAscList. The meaning of certain operations, like foldr, take or size, can naturally be expressed
in terms of toAscList, but would be very convoluted to state in terms of the indicator function,
and we use this denotation – or both – where appropriate.
5

PRODUCING VERIFIABLE CODE WITH hs-to-coq

Identifying what to prove about the code is only half of the challenge – we also need to get the
Haskell code into Coq. Ideally, the translation of Haskell code into Gallina using hs-to-coq would
be completely automatic and produce code that can be verified as easily as code written directly in
Coq – and for textbook-level examples, that is the case [Spector-Zabusky et al. 2018]. However,
working with real-world code requires adjustments to the translation process to make sure that the
output is both accepted by Coq and amenable to verification.
A core principle of our approach is that the Haskell source code does not need to be modified in
order to be verified. This principle ensures that we verify “the” containers library (not a “verified
fork”) and that the verification can be ported to a newer version of the library.
22 In

the file examples/containers/theories/SetProofs.v

14

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

The crucial feature of hs-to-coq that enables this approach is the support for edits: instructions
to treat some code differently during translation. Edits are specified in plain text files, which also
serve as a concise summary of our interventions. The hs-to-coq tool already supported many
forms of edits; for example, specifying when names need to be changed, when parts of the module
should be ignored or replaced by some other term, when we want to map Haskell types to existing
Coq types, or when a recursive function definition needs an explicit termination proof. In the
course of this work, we added new features to hs-to-coq – such as the ability to apply rewrite
rules, to handle partiality and to defer termination proofs to the verification stage – and extended
the provided base library.
In this section we demonstrate some of the challenges posed by translating real-world code, and
show how hs-to-coq’s flexibility allowed us to not only to overcome them, but also to facilitate
subsequently proving the input correct.
5.1

Unsafe pointer equality

An example of a Haskell feature that we cannot expect to translate without intervention is unsafe
pointer equality. GHC’s runtime provides the scarily named function reallyUnsafePtrEqualty#,
which the containers library wraps as ptrEq :: a -> a -> Bool. If this function returns True,
then both arguments are represented in memory by the same pointer. If this function returns False,
we know nothing – this function is underspecified and may return False even if the two pointers
are equal. This operation is used, for example, in Set.insert x s when x is already a member of s:
If ptrEq indicates that the subtree is unchanged, the function skips the redundant re-balancing
step – which enhances performance – and returns the original set rather than constructing a
semantically equivalent copy – which increases sharing.
Coq does not provide any way of reasoning about memory, so when we use hs-to-coq, we must
replace ptrEq with something else. But what?
One option is to replace the definition of ptrEq with a definition that does not do any computation
and simply always returns False. This can be done using the following edit:
replace Definition ptrEq : forall {a}, a -> a -> bool := fun _ _ _ => false.
This replacement would behave in a way that is consistent with reallyUnsafePtrEqualty#
and allows us to proceed with translation and verification. However, the code in the True branch
of an unsafe pointer equality test would be dead code in Coq, and our verification would miss bugs
possibly lurking there.
Consequently, we choose a different encoding that captures the semantics of ptrEq more precisely.
We make the definition of ptrEq opaque and partially specify its behavior.23
Definition ptrEq_spec :
{ptrEq : forall a, a -> a -> bool | forall a (x y : a), ptrEq _ x y = true -> x = y}.
Proof. apply (exist _ (fun _ _ _ => false)). intros; congruence. Qed.
Definition ptrEq : forall {a}, a -> a -> bool := proj1_sig ptrEq_spec.
Lemma ptrEq_eq : forall {a} (x:a)(y:a), ptrEq x y = true -> x = y.
Proof. exact (proj2_sig ptrEq_spec). Qed.
Here, we define the ptrEq function together with a specification as ptrEq_spec. Although the
function in ptrEq_spec also always returns false, the Qed at the end of its definition completely
hides this implementation of ptrEq. While the specification ptrEq_eq is vacuously true, making
23 In

the file examples/containers/lib/Utils/Containers/Internal/PtrEquality.v

Ready, Set, Verify!

15

Set: deleteAt, deleteFindMax, deleteFindMin, elemAt, findIndex, findMax, findMin
Instances: Data, IsList, NFData, Read, Show, Show1
Internal functions: showTree
IntSet: deleteFindMax, deleteFindMin, findMax, findMin, fromAscList,
fromDistinctAscList
Instances: Data, IsList, NFData, Read, Show
Internal functions: showTree
Fig. 7. Untranslated functions and type classes in Data.Set and Data.IntSet

this definition opaque forces verification to proceed down both paths. While could achieve the
same using Axiom, our variant protects us from accidentially introducing inconsistencies to Coq.
We do have to trust that GHC’s definition of pointer equality has this specification, but given
this assumption, we can soundly verify that pointer equality is used correctly.
5.2

Evaluation order

A shallow embedding of Haskell into Coq makes the difference between strict and lazy code vanish,
because Gallina is a total language and does not care about evaluation order. Danielsson et al.
[2006] show that such “fast and loose” reasoning does not invalidate our theorems.
Haskell has “magic” functions like seq that allow the programmer to explicitly control strictness,
and the containers library uses it. Its effect is irrelevant in Coq, and we instruct hs-to-coq to
use this simple, magic-free implementation for it:
Definition seq {a} {b} (x : a) (y : b) := y.

5.3

Eliminating unwanted parts of the code

Figure 7 lists the untranslated portions of the Set and IntSet modules. Many of these operations
are functions that we choose to ignore for the sake of verification – for example, the function
showTree in Data.Set prints the internal structure of such a set as an ASCII-art tree. This function
is not used elsewhere in the module. In the interest of a tidier and smaller output, we skip this
function using an edit:
skip showTree
Similarly, we skip functionality related to serialization (the Show and Show1 type classes), deserialization (the Read type class), generic programming (the Data type class), and overloaded list
notation (the IsList type class).
Furthermore, we skip some operations whose public API is partial. For example, evaluating
findMax empty will raise an exception, as the empty set has no maximum element. We cannot
model this exception in Coq, so we skip findMax and similar functions (findMin, deleteFindMax,
deleteFindMin, findIndex, elemAt and deleteAt). This elision is not significant because the
containers API provides total equivalents for many of these functions (e.g., lookupIndex, which
returns Nothing when the index is out of bounds).
Finally, we skip the two functions that use mutual recursion (Data.IntSet.fromAscList and
Data.IntSet.fromDistinctAscList) as this is not yet supported by hs-to-coq.

16
5.4

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich
Partiality in total functions

In contrast to the skipped functions above, some functions use partiality in their implementation
in ways that cannot be triggered by a user of the public API. In particular, they may use calls to
Haskell’s error function when an invariant is violated.
For example, the central balancing functions for Sets, balanceL and balanceR, may call error
when passed an ill-formed Set. Because our proofs only reason about well-formed sets, this code is
actually dead. It does not matter how we translate error – any term that is accepted by Coq is
good enough. However, error in Haskell has the type
error :: String -> a
which means that a call to error can inhabit any type. We cannot define such a function in Coq,
and adding it as an axiom would be glaringly unsound.
Therefore, we extended hs-to-coq to use the following definition for error:
Class Default (a :Type) := { default : a }.
Definition error {a} `{Default a} : String -> a.
Proof. exact (fun _ => default). Qed.
The type class enforces that we use error only at non-empty types, ensuring logical consistency.
Yet we will notice that something is wrong when we have to prove something about it. Just as with
ptrEq (Section 5.1), by making the definition of error opaque using Qed, we are prevented from
accidentally or intentionally using the concrete default value of a given type in a proof about
error. Furthermore, when we extract the Coq code back to Haskell for testing, we translate this
definition back to Haskell’s error function, preserving the original semantics.
This encoding is inspired by Isabelle, where all types are inhabited and there is a polymorphic
term undefined :: a that denotes an unspecified element of any type.
5.5 Translating the Int in IntSet
As discussed in Section 4.1, we map Haskell’s finite-width integer type Int to Coq’s unbounded
integer type Z in the translation of Data.Set in order to match the specification that integer
overflow is outside the scope of the specified behavior.
For IntSet, however, this choice would cause problems. Big-endian Patricia trees require that
two different elements have a highest differing bit. This is not the case for Z, where negative
numbers have an infinite number of bits set to 1; for instance, -1 is effectively an infinite sequence
of set bits. Fortunately, hs-to-coq is flexible enough to allow us to make a different choice when
translating IntSet; we can pick any suitable type where all elements have a finite number of bits
set, such as the natural numbers (N) or a fixed width integer type.
Given that Coq’s standard library provides a fairly comprehensive library of lemmas about N and
decision procedures (omega and lia) that work with it, we chose to use N for now, with the intention
to eventually switch to a 64-bit integer type. This is the appropriate generalization of IntSet to an
infinite domain. In Haskell, the domain is 64-bit words, which happen to be interpretable as negative
numbers. When we generalize to an infinite domain, we generalize to bit strings of unbounded but
finite length, which we can most simply interpret as nonnegative.
The IntSet code uses bit-level operations, like complement and negate, that do not exist for N.
To deal with this we extended hs-to-coq with support for rewrite edits like
rewrite forall x y, (x .&. complement y) = (xor x (x .&. y))
which instruct it to replace any expression that matches the left-hand side by the right hand side.
For signed or bounded integer types, both sides are equivalent. For unbounded unsigned types,

Ready, Set, Verify!

17

like Coq’s type N, the left hand side is undefined (values in N have no complement in N), while the
right hand side is perfectly fine. When we switch to bounded integers in the IntSet code, we can
remove these edits.
5.6

Low-level bit twiddling

The containers library uses highly tuned bit-twiddling algorithms to operate on IntSets. For
example, the function revNat reverses the order of the bits in a 64-bit number:
revNat :: Nat -> Nat
revNat x1 = case ((x1 `shiftRL` 1) .&. 5555555555555555) .|.
((x1 .&. 5555555555555555) `shiftLL` 1) of x2 ->
case ((x2 `shiftRL` 2) .&. 3333333333333333) .|.
((x2 .&. 3333333333333333) `shiftLL` 2) of x3 ->
case ((x3 `shiftRL` 4) .&. 0F0F0F0F0F0F0F0F) .|.
((x3 .&. 0F0F0F0F0F0F0F0F) `shiftLL` 4) of x4 ->
case ((x4 `shiftRL` 8) .&. 00FF00FF00FF00FF) .|.
((x4 .&. 00FF00FF00FF00FF) `shiftLL` 8) of x5 ->
case ((x5 `shiftRL` 16) .&. 0000FFFF0000FFFF) .|.
((x5 .&. 0000FFFF0000FFFF) `shiftLL` 16) of x6 ->
(x6 `shiftRL` 32) .|. (x6 `shiftLL` 32)
Though complicated, this code is within the scope of what hs-to-coq can translate, and we can
verify its correctness.
However, we can’t keep up with all their tricks. For example, indexOfTheOnlyBit, which was
contributed by Edward Kmett,24 takes a number with exactly one bit set and calculates the index of
said bit. It does so by unboxing the input, multiplying it by a magic constant, and using the upper 6
bits of the product as an index into a table stored in an unboxed array literal. This manifests as the
following scary-looking code:
indexOfTheOnlyBit :: Nat -> Int
indexOfTheOnlyBit bitmask = I# (lsbArray `indexInt8OffAddr#` unboxInt
(intFromNat ((bitmask * magic) `shiftRL` offset)))
where
unboxInt (I# i) = i
magic
= 0x07EDD5E59A4E28C2
offset
= 58
!lsbArray
= "\63\0\58\1\5. . . 15\8\23\7\6\5"#
We currently cannot translate this code because hs-to-coq does not yet support unboxed arrays
or unboxed integers. We therefore replace it with a simple definition based on a integer logarithm
function provided by Coq’s standard library:
redefine Definition indexOfTheOnlyBit := fun x => N.log2 x.
Similarly, we provide simpler definitions for the low-level bit-twiddling functions branchMask,
mask, zero and suffixBitMask.
5.7

Non-trivial recursion

In order to prove the correctness of Set and IntSet, we must deal with termination. There are
two reasons for this. First, we intrinsically want to prove that none of the functions provided by
containers go into an infinite loop. Second, Coq requires that all defined functions are terminating,
24 https://github.com/haskell/containers/commit/e076b33f

18

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

--Less obvious structural recursion
link :: a -> Set a -> Set a -> Set a
link x Tip r = insertMin x r
link x l Tip = insertMax x l
link x l@(Bin sizeL y ly ry) r@(Bin sizeR z lz rz)
| delta*sizeL < sizeR = balanceL z (link x l lz) rz
| delta*sizeR < sizeL = balanceR y ly (link x ry r)
| otherwise
= bin x l r
--Well-founded recursion
foldlBits :: Int -> (a -> Int -> a) -> a -> Nat -> a
foldlBits prefix f z bitmap = go bitmap z
where go 0 acc = acc
go bm acc = go (xor bm bitmask) ((f acc) $! (prefix+bi))
where !bitmask = lowestBitMask bm
!bi = indexOfTheOnlyBit bitmask
--Deferred recursion
fromDistinctAscList :: [a] -> Set a
fromDistinctAscList [] = Tip
fromDistinctAscList (x0 : xs0) = go (1::Int) (Bin 1 x0 Tip Tip) xs0
where go !_ t []
=t
go s l (x : xs) = case create s xs of (r :*: ys) ->
let !t' = link x l r in go (s `shiftL` 1) t' ys
create !_ [] = (Tip :*: [])
create s xs@(x : xs')
| s == 1
= (Bin 1 x Tip Tip :*: xs')
| otherwise = case create (s `shiftR` 1) xs of
res@(_ :*: []) -> res
(l :*: (y:ys)) -> case create (s `shiftR` 1) ys of
(r :*: zs) -> (link y l r :*: zs)
Fig. 8. Recursion styles

as unrestricted recursion would lead to logical inconsistencies. Depending on how involved the
termination argument for a given function is, we use one of the following four approaches.
5.7.1 Obvious structural recursion. By default, hs-to-coq implements recursive functions directly using Coq’s fix keyword. This works smoothly for primitive structural recursion; indeed, a
majority of the recursive functions that we encountered, such as member in Figure 1, were of this
form and required no further attention.
5.7.2 Almost-structural recursion. Another common recursion pattern can be found in binary
operations such as link in Figure 8. Here, every recursive call shrinks either or both of its arguments
to immediate subterms of the originals, leaving the others unchanged. This almost-structural
recursion is already beyond the capabilities of Coq’s termination checker. We therefore instruct
hs-to-coq to use Coq’s Program Fixpoint command to translate these functions in terms of
well-founded recursion by adding the edits
termination link {measure (size_nat arg_0__ + size_nat arg_1__)}
obligations link termination_by_omega

Ready, Set, Verify!

19

This specifies both:
(1) The termination measure, which is the sum of the sizes of the arguments (we defined the
function size_nat : IntSet -> nat).
(2) The termination proof that the measure decreases on every call. This is represented as the
Coq tactic termination_by_omega, which is a thin wrapper we defined around omega, a
Coq tactic to decide linear integer arithmetic.
We can use these edits (with size_nat and termination_by_omega) to get to Coq accepts such
recursive definitions without the need for any further proofs or manual intervention.
5.7.3 Well-founded recursion. A small number of functions recurse in a non-structural way, such
as foldlBits in Figure 8, which recurses on the input after clearing the least-significant set bit (bm
`xor` (lowestBitMask bm)). We can handle this sort of logic using the same machinery as before,
but now we have to write a specialized termination tactic and declare it in the obligations hint.
To do so, we need to prove necessary lemmas before translating the Haskell module in question.
Coq’s Program Fixpoint only supports top-level functions, but we frequently encounter local
recursive functions – the go idiom, as seen here. To support this, we extended hs-to-coq to offer
some of the convenience provided by Program Fixpoint by translating local recursive functions
using the same well-founded-recursion-based fixed-point combinator as Program Fixpoint.
5.7.4 Deferred recursion. Finally, we encounter some functions that require elaborate termination arguments, such as fromDistinctAscList in Figure 8. It has two local recursive functions,
go and create, and to convince ourselves that fromDistinctAscList is indeed terminating, we
have to reason as follows:
The function create bitshifts its first argument to the right upon each recursive call,
until the argument is 1. Ergo, it is terminating, but only for positive input – it clearly
loops if x is 0. The function go recurses on smaller lists as its third argument, but to see
that, we first have to convince ourself that the list in the tuple returned by create is
never larger than the list passed to create. Also, go calls create, so we need to ensure
that the s passed to it is positive. The go function bitshifts s to the left at every call, so
if go is called with a positive s, then s will remain positive in recursive calls. Finally,
we see that fromDistinctAscList calls go with s equal to 1, which is positive, so we
can conclude that fromDistinctAscList terminates.
If we wanted to convince Coq of this termination pattern, we would have to turn create and
go into top-level definitions, change their types to rule out invalid (non-positive) inputs, define
create using Program Fixpoint, and provide an explicit termination argument by well-founded
recursion. Then we could prove that create preserves the list lengths, which we need to define
go, again using Program Fixpoint. This is certainly possible, but it is not simple, especially in an
automatic translation.
For hard cases like these we resort to deferred termination checking, a feature that we added
to hs-to-coq. We can instruct it to use the following axiom as a very permissive fixed-point
combinator and translate the code of fromDistinctAscList essentially unchanged:
Axiom deferredFix: forall {a r} `{Default r}, ((a -> r) -> (a -> r)) -> a -> r.
On its own, deferredFix does not do anything; it merely sits in the translated code applied to
the original function body. It is consistent, since its type could be implemented by a function
that always returns default (see Section 5.4). And it does not prevent the user from running
extracted code – we can extract this axiom to the target language’s unrestricted fixpoint operator

20

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

(e.g., Data.Function.fix in Haskell), although this costs us the guarantee that the extracted code
is terminating.
When we come to verifying something about a function that is defined using deferredFix, we
need to give it meaning. We do so using a second axiom, deferredFix_eq_on, which states that
for any well-founded relation R (well_founded R), if the recursive calls in f are always at values
that are strictly R-smaller than the input (recurses_on R), then we may unroll the fixpoint of f:
Definition recurses_on {a b}
(P : a -> Prop) (R : a -> a -> Prop) (f : (a -> b) -> (a -> b))
:= forall g h x, P x -> (forall y, P y -> R y x -> g y = h y) -> f g x = f h x.
Axiom deferredFix_eq_on: forall {a b}
`{Default b} (f : (a -> b) -> (a -> b)) (P : a -> Prop) (R : a -> a -> Prop),
well_founded R -> recurses_on P R f ->
forall x, P x -> deferredFix f x = f (deferredFix f) x.
The predicate P : a -> Prop allows us to restrict the domain to inputs for which the function is
actually terminating – crucial for go and create.
The predicate recurses_on P R f characterizes the recursion pattern of f, but does so in a very
extensional way and only considers recursive calls that can actually affect the result of the function.
For instance, it would consider a recursive function defined by f n = if f n then true else true
to be terminating.
We can use this non-trivial axiom without losing too much sleep, because we can actually
implement deferredFix and deferredFix_eq_on in terms of classical logic and the axiom of
choice (as provided by the Coq module Coq.Logic.Epsilon).25 This means that both axioms are
consistent with plain Coq. We do not know if deferredFix_eq_on is strictly weaker than classical
choice, so users of hs-to-coq who want to combine the output of hs-to-coq with developments
known to be inconsistent with classical choice (e.g., homotopy type theory) should be cautious.
Pragmatically, working with deferredFix is quite convenient, as we can prove termination
together with the other specifications about these functions. The actual termination proofs themselves are not fundamentally different from the proof obligations that Program Fixpoint would
generate for us and – although not needed in this example – can be carried out even for nested
recursion through higher-order functions like map.
This approach to defining recursive functions extensionality was inspired by Isabelle’s function
package [Krauss 2006].
5.8

Translating Haskell tests to Coq types

When we translate code, we usually want to preserve the semantics of the code as much as possible.
Things are very different when we translate the QuickCheck tests defined in the containers test
suite, as we discuss in Section 4.2: whereas the semantics of the test suite in Haskell is a program
that creates random input to use as input test executable properties, we want to re-interpret these
properties as logical propositions in Coq. Put differently, we are turning executable code into types.
QuickCheck’s API provides types and type classes for writing property-based tests. In particular,
it defines an opaque type Property that describes properties that can checked using randomized
testing, a type class Testable that converts various testable types into a Property, and a type
constructor Gen that describes how to generate a random value. These are combined, for instance,
in the QuickCheck combinator
forAll :: (Show a, Testable prop) => Gen a -> (a -> prop) -> Property
25 In

the file base/GHC/DeferredFixImpl.v

Ready, Set, Verify!

21

which tests the result of a function on inputs generated by the given generator.
Since we want to prove, not test, these properties, we do not convert the QuickCheck implementation to Coq. Instead, we write a small Coq module that provides the necessary pieces of the interface
of Test.QuickCheck, but interprets these types and functions in terms of Coq propositions. In
particular:
• We use Coq’s non-computational type of propositions, Prop, instead of QuickCheck’s computational Property;
• Gen a is simply a wrapper around a logical predicate on a; and
• forAll quantifies (using Coq’s forall) over the type a, and ensures that the given function
– now a predicate – holds for all members of a that satisfy the given “generator”.
Concretely, this leads to the following adapted Coq code:
Record Gen a := MkGen { unGen : a -> Prop }.
Class Testable (a : Type) := { toProp : a -> Prop }.
Definition forAll {a prop} `{Testable prop} (g : Gen a) (p : a -> prop) : Prop :=
forall (x : a), unGen g x -> toProp (p x).
We provide similar translations for QuickCheck’s operators ===, ==>, .&&. and .||., and we replace
generators such as choose :: Random a => (a, a) -> Gen a with their corresponding predicates.
With this module in place, hs-to-coq translates the test suite into a “proof suite”. As we saw in
Section 4.2, a test like prop_UnionAssoc is now a definition of a Coq proposition, that is to say a
type, and can be used as the type of a theorem:
Theorem thm_UnionAssoc : toProp prop_UnionAssoc.
6

CONTRIBUTIONS TO containers: THEORY AND PRACTICE

We chose the Set and IntSet modules of the containers library as our target because they nicely
represent the kind of Haskell code that we want to see verified in practice. Nevertheless, the deep
understanding required to verify these modules led to new insights into the algorithms themselves
and to improvements to their Haskell implementation.
6.1

New insight into the verification of weight-balanced trees

The data structure underlying Set and Map was originally presented by Nievergelt and Reingold
[1972]. It is a binary search tree with the invariant that if s 1 is the size of the left subtree and s 2 the
size of the right subtree of a node, then
balNR (s 1 , s 2 ) B (s 1 + 1) ≤ δ · (s 2 + 1) ∧ (s 2 + 1) ≤ δ · (s 1 + 1)
holds for a balancing tuning parameter δ . In 1992, Adams suggested a variant of the balancing
condition, namely
bal(s 1 , s 2 ) B s 1 + s 2 ≤ 1 ∨ (s 1 ≤ δ · s 2 ∧ s 2 ≤ δ · s 1 ).
The conditions are very similar, but not equivalent: the former allows, for example, δ = 3, s 1 = 2
and s 2 = 0, which the latter rejects.
Initially, the containers library used Adams’s balancing condition with the parameters δ = 4
(for sets) or δ = 5 (for maps). Campbell [2010] found that these parameters are actually invalid and
exhibited a sequence of insertions and deletions that produced an unbalanced tree. Subsequently,
the containers library switched to δ = 3 in both modules. Inspired by this bug report, Hirai and
Yamamoto [2011] thoroughly analyzed this data structure with the help of a Coq formalization, and
identified the valid range for the balancing parameter, albeit only for Nievergelt and Reingold’s
variant – our proof seems to be the first mechanical verification of Adam’s variant.

22

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

Given such thorough analysis of the algorithms, we did not expect to learn anything new
about this data structure, and for the most part, this was true. Our proofs are free of any manual
calculations about tree sizes and the balancing condition. We just state the proper preconditions
for each lemma, and Coq’s automation for linear integer arithmetic, lia [Besson 2006], takes care
of the rest.
One exception was the crucial function balanceL which is used, according to the documentation
“when the left subtree might have been inserted to or when the right subtree might have been
deleted from”. This suggests the precondition
(bal(s 1 − 1, s 2 ) ∧ 0 < s 1 ) ∨ bal(s 1 , s 2 ) ∨ bal(s 1 , s 2 + 1)
corresponding to the three cases: left tree inserted to, no change, and right tree deleted from. This
is also what Hirai and Yamamoto used in their formalization of the original variant. And indeed,
this precondition is strong enough to verify that the output of balanceL is balanced – but we
found the precondition too strong. The link operation, shown in Figure 8, is supposed to balance
two arbitrary trees using balanceL. In the verification of link we were unable to satisfy this
precondition.
We found another precondition that is both strong enough for the verification of balanceL and
weak enough to allow the verification of link, namely
(bal∗ (s 1 − 1, s 2 ) ∧ 0 < s 1 ) ∨ bal(s 1 , s 2 ) ∨ bal(s 1 , s 2 + 1)
where
bal∗ (s 1 , s 2 ) B δ · s 1 ≤ δ 2 · s 2 + δ · s 2 + s 2 ∧ s 2 ≤ s 1 .
Unfortunately we cannot give much insight into why this is the right inequality – this is the
price we pay for relying completely on proof automation when verifying the balancing properties.
For us, this inequality fell out of the proof for link, where we call balanceL with trees with sizes
s 1 and s 2 , and what we know about these trees can be expressed as
∃ s sl sr , s 1 = 1 + s + sl ∧ s 2 = sr ∧ bal(sl , sr ) ∧ δ · s < 1 + sl + sr ∧ 1 ≤ s ∧ 0 ≤ sl ∧ 0 ≤ sr
As lia works best when the formulas are quantifier-free, we manually eliminated the existential
quantifiers and simplified this to arrive at bal∗ (s 1 − 1, s 2 ).
6.2

Improvements to containers

Although our verification did not find bugs in the code of the library, we were able to improve
containers: during the verification of Data.Set.union, we noticed that it was using a nested
pattern match to check if an argument is a singleton set, when it could be testing if the size was 1
directly. This change turned out to provide a 4% speedup to union and will be present in the next
version of the containers library.26
Additionally, as we mention in Section 4.1, our well-formedness property for IntSet uncovered
a weakness in the valid function for IntSet and IntMap, which was used in the test suite. The
valid function failed to ensure that some of the invariants hold recursively in the tree structure,
which was necessary for the proof. We notified the containers maintainers,27 who then made the
valid function complete.
We also provide a package, containers-verified,28 which re-exports the types and definitions
we have verified from the precise version of containers we are working with. This way, a developer
26 https://github.com/haskell/containers/commit/b1a05c3a2
27 https://github.com/haskell/containers/issues/522
28 https://hackage.haskell.org/package/containers-verified

Ready, Set, Verify!

23

who wants to use only the verified portion of the implementation can replace their dependency on
containers with a dependency on containers-verified.
7

ASSUMPTIONS AND LIMITATIONS

We have shown a way to make mechanically checked, formal statements about existing Haskell
code, and have applied this technique to verify parts of the containers library. But are the theorems
that we prove actually true? And if they are, how useful is this method?
7.1

The formalization gap

As always, when a theorem is stated about a object that does not purely exist within mathematics,
its validity depends on a number of assumption.
• First and foremost, we have to assume that Coq behaves as documented and does not allow
us to prove false theorems. This is of particular relevance because we rely on fine details of
Coq’s machinery (e.g. the behavior of Qed, Section 5.4) and optionally add consistent axioms
(see Section 5.7.4).
• The biggest assumption is that the semantics of a Gallina program, as defined by the Calculus
of Construction [Coquand and Huet 1988], models the the behavior of a running Haskell
program in a meaningful way. At this time, we cannot even attempt to close this gap, as there
are neither formal semantics nor verified compilers for Haskell.
We know that “Fast and Loose Reasoning is Morally Correct” [Danielsson et al. 2006], which
says that theorems about the total fragment of a non-total language carry over to the full
language. But since we relate two very different languages, this argument alone is not enough
to bridge the gap.
We can gain additional confidence by testing this connection: we extracted our Gallina
versions of Set and IntSet back to Haskell and successfully ran the original test suite of
containers against it. Every successful test indicates that the corresponding theorem (see
Section 4.2) is indeed a theorem about the Haskell program.
• Furthermore, we rely on hs-to-coq translating Haskell code into the correct Gallina code.
The translator itself is a sizable piece of code, unverified (and such verification is currently out
of our reach, not least because there is no formal semantics of Haskell) and therefore surely
not free of bugs. We get some confidence into the tool from manually inspecting its output
and observing that it is indeed what we would consider the “right” translation from Haskell
into Gallina, and additional confidence from the fact that we were actually able to prove the
specifications, which would not be possible if the translated code behaved differently than
intended. Moreover, extracting the translated code back to Haskell and running the test suite
also stress-tests the translation.
• The translation was not completely automatic and required manual edits. With each edit,
we add another assumption to the formalization gap: Does our underspecification of pointer
equality encompass the actual behavior of GHC’s reallyUnsafePtrEqualty#? Given our
choice of using unbounded integers, does the size field in a Set really never overflow in
practice? Are our manually written versions of low-level bit twiddling functions correct? We
list and justify our manual interventions in Section 5.
The formalization gap of our work is relatively large compared to, say, the gap for the verification
of programs written in Gallina in the first place. But for the purpose of ensuring the correctness
of the Haskell code, that is less critical. Even if one of our assumptions is flawed, it is much more
likely that the flaw will get in the way of concluding the proofs, rather than allowing us to conclude
the proofs without noticing a bug. Incomplete proofs can uncover bugs, too.

24
7.2

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich
Limitations of our approach

We proved multiple specifications about a large part of the code, but there are limits to what
theorems we can prove, and what we can prove them about.
Since we work with a shallow embedding of Haskell in Coq, we cannot make statements about
the performance of the Haskell code – which is a pity, given that the containers library contains
highly optimized code and provides clear specifications of the algorithmic complexity of their
operations. Similarly, we cannot verify that the operations are as strict or lazy as documented.
We also cannot translate and verify all code in the containers library, because some functions
use language features not yet supported by hs-to-coq, such as mutual recursion, unboxed values
and generic programming. When this affects a crucial utility function we can provide a manual
translation. This widens the formalization gap, but enables verification of code that depends on
it. When it affects less central code, e.g. the Data instances, we can simply skip the translation
(Section 5.3).
Partiality is a particular interesting limit. Coq only allows total functions, but practical Haskell
code uses partiality, often in a benign way: Calls to error in code paths that are unreachable as long
as invariants are maintained, or recursive functions that terminate on the actual arguments they
are called with, but may diverge on other inputs. Whereas Spector-Zabusky et al. [2018] considered
such code out of scope, we have found ways to deal with “internal partiality” (see Sections 5.4
and 5.7.4).
Taking a step back, it might seem that our approach may see limited adoption in the Haskell
community because it requires expertise in Coq. But though tied to a Haskell artifact, verification is
isolated from the codebase. Haskell programmers can focus on their domain, trying to get the best
performance out of the code and without having to know about verification, while proof engineers
can work solely within Coq and do not have to be fluent in Haskell.
In this paper we verify a specific version of the Haskell code, and do not discuss ongoing
maintenance of such a verification. It remains to be seen how resilient the proofs are against
changes in the Haskell code. Changes of syntactic nature, or changes to a function’s strictness,
might be swallowed by hs-to-coq. Other changes might affect the translated code, but still allow
the proofs to go through, if our proof tactics are flexible enough. In general, though, we expect that
changes in the code require changes in the proofs. Since Coq is an interactive theorem prover, it
will at least clearly point out which parts of our development need to be updated.
8
8.1

RELATED WORK
Verification of purely functional data structures

Purely functional data structures, such as those found in Okasaki’s book [1999] are frequent targets
of mechanical verification. That said, we believe that we are the first to verify the Patricia tree
algorithms that underlie Data.IntSet.
Verifying weight-balanced trees in Haskell. Similar to hs-to-coq, LiquidHaskell [Vazou et al.
2014] can be used to verify existing Haskell code. Users of this tool annotate their Haskell source
files with refinement types and other annotations. LiquidHaskell then uses an SMT solver to automatically discharge proof obligations described by the refinements. This means that LiquidHaskell
provides more automation than hs-to-coq; however, the language of Coq is higher-order and
more expressive than the language of SMT solvers. Vazou et al. [2017] compared the experiences of
using LiquidHaskell vs. plain Coq, and found that both have advantages.
Vazou et al. [2013] also described the use of LiquidHaskell to verify the Data.Map module of
finite maps from containers. Although not the same as Data.Set, this code shares the same
underlying data structure (weight-balanced trees) and the implementations of the two are similar.

Ready, Set, Verify!

25

Their verification has similarities with our work; they also use unbounded integers as the number
representation and left functions like showTree unspecified. However, we develop a richer specification, which includes a semantic description of each operation we verified, constraints about
the tree balance, and the ordering of the elements in the tree. In contrast, Vazou et al. limit their
specifications to ordering only. For example, in addition to showing that the insertion operation
preserves the order of elements of the tree, our work also shows that: (1) insertion preserves the
balancing conditions of the weight-balanced tree, (2) the size field at each node in the tree is
maintained correctly (i.e., the size equals to the number of all its descendants), and (3) the tree
returned by this operation contains the inserted element, and all elements in the original tree, but
nothing more. Although it might be possible to replicate our specifications by using theories of
finite sets and maps in SMT [Kröning et al. 2009] to encode these properties using refinement types
in LiquidHaskell, this approach has not been explored.
Furthermore, our specification also includes type class laws, and we are able to verify that Set
and IntSet have lawful instances of the Eq, Ord, Semigroup, and Monoid type classes. When Vazou
et al.’s original work was developed in 2013, LiquidHaskell did not have the capability to state and
prove these properties. Since then, there have been new developments in LiquidHaskell, particularly
refinement reflection [Vazou et al. 2018], which could make it possible to specify and prove type
class laws.
Both LiquidHaskell and hs-to-coq check for termination of Haskell functions. In LiquidHaskell,
the termination check is an option that can be deactivated, allowing the sound verification of
nonstrict, non-terminating functions [Vazou et al. 2014]. In contrast, a proof of termination is
a requirement for verifying functions using hs-to-coq [Spector-Zabusky et al. 2018]. However,
hs-to-coq is able to take advantage of many options available in Coq for proving termination of
non-trivial recursion, including structural recursion, Program Fixpoint and our own approach
based on deferredFix. This latter approach alowed us to reason about fromDistinctAscList
(see Section 5.7.4) and prove that it is indeed terminating; on the other hand, Vazou et al. deactivate
the termination check for this function.
Verifying weight-balanced trees in other languages. Hirai and Yamamoto [2011] implemented a
weight-balanced tree similar to Haskell’s Data.Set library (albeit using the balancing condition of
Nievergelt and Reingold [1972]) and mechanically verified its balancing properties in Coq. More
recently, Nipkow and Dirix [2018] extended this work to formalize similar weight-balanced trees
in Isabelle and further verified the functional correctness of insertions and deletions.
We verify more functions in the Data.Set library than prior work. Operations that are unique
to our development include foldl, isSubsetOf, and fromDistinctAscList. The code verified
both by Hirai and Yamamoto and by Nipkow and Dirix is also different from the latest containers
library; for example, it does not use of pointer equality (Section 5.1). Another difference is that Hirai
and Yamamoto defined the union, intersection, and difference functions based on the “hedge
union” algorithm, but containers has since changed to use the “divide and conquer” algorithm.
Hirai and Yamamoto specify only the balancing constraints, whereas we develop a richer specification that also includes a semantic description of each operation we verified and the ordering of
the elements in the tree. We also gained new insights about the balancing conditions of the weightbalanced tree through our verification effort (see Section 6.1). Nipkow and Dirix’s specification
contains the same properties as ours, but they only specify the behavior of insert and delete; we
have verified a significantly larger set of functions (see Figure 4).
Other verifications of balanced trees. There are many existing works on mechanically verifying
purely functional balanced trees. We briefly mention a few here. Filliâtre and Letouzey [2004]
implemented AVL trees in Coq, and verified their functional correctness as well as their balancing

26

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

conditions. Appel [2011] did the same thing for red-black trees. These implementations have now
become parts of Coq standard library. Charguéraud [2010] translated OCaml implementations of
Okasaki [1999]’s functional data structures to characteristic formulae expressed as Coq axioms.
Licata [2012] lectured on verifying red-black trees in Agda at the Oregon Programming Languages
Summer School. McBride [2014] showed how to represent the ordering relationships in Agda for
general data structures, not just binary search trees. Nipkow [2016] showed how to automatically
verify the ordering properties of eight different binary search tree structures, by specifying each
in terms of the sorted list of their elements, a method he used again in his verification of weightbalanced trees [Nipkow and Dirix 2018]. Ralston [2009] verified AVL trees in ACL2.
8.2

Verification tools for Haskell

Previous work using hs-to-coq has only applied it to small examples. Spector-Zabusky et al. [2018]
describe three case studies, two of which require less than 20 lines of Haskell. The longest example
(the Bag module taken directly from the GHC compiler) is 247 lines of code. Furthermore, none of
the reasoning required for these examples is particularly deep. Our work provides experience with
more complex, externally-sourced, industrial-strength examples.
The coq-haskell library [Wiegley 2017] is a handwritten Coq library designed to make it easier
for Haskell programmers to work in Coq. In addition to enabling easier Coq programming, it also
provides support for extracting Coq programs to Haskell.
The prototype contract checker halo [Vytiniotis et al. 2013] takes a Haskell program, uses GHC
to desugar it into the intermediate language Core, and translates the Core program into a first-order
logic formula. It then invokes an SMT solver to prove this formula; a successful proof implies that
the original program is crash-free.
Haskabelle was hs-to-coq’s counterpart in Isabelle. It translated total Haskell code into equivalent Isabelle function definitions. Similar to hs-to-coq, it parsed Haskell, desugared syntactic
constructs, and configurably adapted basic types and functions to their counterparts in Isabelle’s
standard library. It used to be bundled with the Isabelle release, but it has not been updated recently
and was dropped from the distribution.
Haskell has been used as a prototyping language for mechanically verified systems in the past. The
seL4 verified microkernel started with a Haskell prototype that was semi-automatically translated
to Isabelle/HOL [Derrin et al. 2006; Klein et al. 2009]. The authors found that the availability of the
Haskell prototype provided a machine-checkable formal executable specification of the system.
They used this prototype to refine their designs via testing, allowing them to make corrections
before full verification.
The Programmatica project [Hallgren et al. 2004] included a tool that translates Haskell code
into the Alfa proof editor. Their tool only produces valid proofs for total functions over finite data
structures. The logic of the Alfa proof assistant is based on dependent type theory, but without as
many features as Coq. In particular, the Programmatica tool compiles away type classes and nested
pattern matching; both of these features are retained by hs-to-coq.
Dybjer et al. developed a tool for automatically translating Haskell programs to the Agda/Alfa
proof assistant [2004]. They explicitly note the interplay between testing and theorem proving and
show how to verify a tautology checker. Abel et al. [2005] translate Haskell expressions into the
logic of the Agda 2 proof assistant. Their tool works later in the GHC pipeline than hs-to-coq and
translates Core expressions.
8.3

Translating other higher-order functional languages

There are many large and successful verification projects that demonstrate that functional languages
are well suited for verification. In contrast to our work, they require re-implementing the code either

Ready, Set, Verify!

27

in a new functional language, as is the case for Cogent [Amani et al. 2016; O’Connor et al. 2016]
and F* [Swamy et al. 2016], or in a proof assistant, such as HOL4 in the case of CakeML [Kumar
et al. 2014; Myreen and Owens 2014]. The CakeML and Cogent projects have a different focus than
ours, and they provide a higher assurance in their verified code. CakeML [Kumar et al. 2014] has a
verified compiler and Cogent has a certifying compiler [O’Connor et al. 2016; Rizkallah et al. 2016].
Both tools provide mechanically checked proofs that their shallow embeddings correspond to the
functional code being verified.
Cogent is a restricted higher-order functional language [O’Connor et al. 2016] that was used to
verify filesystems [Amani et al. 2016]. Its compiler produces C code, a high-level specification in
Isabelle/HOL, and an Isabelle/HOL refinement proof linking the two [O’Connor et al. 2016; Rizkallah
et al. 2016]. Chen et al. [2017] integrated property-based testing into the Cogent framework. The
authors claim that property-based testing enables an incremental approach to a fully verified system,
as it allows for the replacement of tests of properties stated in the specification by formal proofs.
Our work substantiates this claim, as indeed one of the ways in which we obtain specifications is
through the QuickCheck properties provided by Haskell as discussed in Section 4.2.
CakeML is a large subset of ML with a verified compiler and runtime system [Kumar et al. 2014].
Users of CakeML can write pure functional programs in the HOL4 proof assistant and verify them
in HOL4. They can then extract an equivalent correct by construction CakeML program. This
method has been used to verify several data structures including red black trees, crypto protocols,
and a CakeML version of the HOL light theorem prover [Myreen and Owens 2014].
F* is a general-purpose functional language that allows for a mixture of proving and generalpurpose programming [Swamy et al. 2016]. Programs can be specified using dependent and refinement types and automatically verified using one of F*’s backend SMT solvers. Its subset
Low* [Protzenko et al. 2017] has been used to verify high-assurance optimized cryptographic
libraries.
8.4

Extraction

The semantic proximity of Haskell and Coq, which we rely on, is also used in the other direction by
Coq’s support for code extraction to Haskell [Letouzey 2002]. Several projects use this feature to
verify Haskell code [Chen et al. 2015; Joseph 2014]. However, since extraction starts with Coq code
and generates Haskell, it cannot be used to verify pre-existing Haskell. Although in a certain sense
hs-to-coq and extraction are inverses, round-tripping does not produce syntactically equivalent
output in either direction. In one direction, hs-to-coq extensively annotates the resulting Coq
code; in the other, extraction ignores many Haskell features and inserts unsafe type coercions. In
this work, we use testing to verify that round-tripping produces operationally equivalent output;
this provides assurance about the correctness of both hs-to-coq and extraction.
CertiCoq [Anand et al. 2017] and Œuf [Mullen et al. 2018] are verified compilers from Gallina to
assembly. CertiCoq can compile any Gallina program, while Œuf can only compile a limited subset
of Gallina. However, Œuf provides stronger guarantees about the Gallina code that is in the limited
subset it translates.
9

CONCLUSIONS AND FUTURE WORK

We verified the two finite set modules that are part of the widely used and highly-optimized
containers library. Our efforts provide the deepest specification and verification of this code to
date, covering more of the API and proving stronger, more descriptive properties than prior work.
In future work, there is yet more to verify in containers. For example, we plan to add a version of
IntSet that uses 64-bit ints as the element type in addition to our current version with unbounded
natural numbers. That way users could choose the treatment of overflow that makes the most sense

28

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

for their application. We have also started to verify Data.Map and Data.IntMap. Because these
modules use the same algorithms as Data.Set and Data.IntSet, we already adapted some of our
existing proofs to this setting.
The fact that we did not find bugs says a lot about the tools that are already available to Haskell
programmers for producing correct code, such as a strong, expressive type system and a mature
property-based testing infrastructure. However, few would dare to extrapolate from these results to
say that all Haskell programs are bug free! Instead, we view verification as a valuable opportunity
for functional programmers and an activity that we hope will become more commonplace.
ACKNOWLEDGMENTS
This material is based upon work supported by the National Science Foundation under Grant
No. 1319880 and Grant No. 1521539.
REFERENCES
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, and Ulf Norell. 2005. Verifying Haskell Programs Using Constructive
Type Theory. In Haskell Workshop. ACM, 62–73. DOI:http://dx.doi.org/10.1145/1088348.1088355
Stephen Adams. 1992. Implementing sets efficiently in a functional language,. Research Report CSTR 92-10. University of
Southampton.
Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima,
Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. 2016.
Cogent: Verifying High-Assurance File System Implementations. In International Conference on Architectural Support
for Programming Languages and Operating Systems. Atlanta, GA, USA, 175–188. DOI:http://dx.doi.org/10.1145/2872362.
2872404
Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu
Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In CoqPL Workshop (CoqPL ’17).
Andrew W. Appel. 2011. Efficient verified red-black trees. (2011). https://www.cs.princeton.edu/~appel/papers/redblack.pdf
Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve
Zdancewic. 2017. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society of
London A: Mathematical, Physical and Engineering Sciences 375, 2104 (2017). DOI:http://dx.doi.org/10.1098/rsta.2016.0331
Frédéric Besson. 2006. Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In TYPES (Lecture Notes in Computer
Science), Vol. 4502. Springer, 48–62.
Ana Bove, Peter Dybjer, and Ulf Norell. 2009. A Brief Overview of Agda - A Functional Language with Dependent Types. In
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20,
2009. Proceedings (Lecture Notes in Computer Science), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius
Wenzel (Eds.), Vol. 5674. Springer, 73–78. DOI:http://dx.doi.org/10.1007/978-3-642-03359-9_6
Edwin Brady. 2017. Type-driven Development With Idris. Manning.
Taylor Campbell. 2010. Bug in Data.Map. (2010). http://article.gmane.org/gmane.comp.lang.haskell.libraries/13448 e-mail
to the Haskell libraries mailing list.
Arthur Charguéraud. 2010. Program verification through characteristic formulae. In ICFP. ACM, 321–332. DOI:http:
//dx.doi.org/10.1145/1932681.1863590
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash
Hoare Logic for Certifying the FSCQ File System. In SOSP. ACM, 18–37. DOI:http://dx.doi.org/10.1145/2815400.2815402
Zilin Chen, Liam O’Connor, Gabriele Keller, Gerwin Klein, and Gernot Heiser. 2017. The Cogent Case for Property-Based
Testing. In Workshop on Programming Languages and Operating Systems (PLOS) (2017-10-28). ACM, Shanghai, China,
1–7.
Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. In ICFP.
ACM, 268–279.
Thierry Coquand and Gérard P. Huet. 1988. The Calculus of Constructions. Information and Computation 76, 2/3 (1988),
95–120. DOI:http://dx.doi.org/10.1016/0890-5401(88)90005-3
Nils Anders Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. 2006. Fast and loose reasoning is morally correct.
In POPL. ACM, 206–217. DOI:http://dx.doi.org/10.1145/1111037.1111056
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and Manuel M. T. Chakravarty. 2006. Running the Manual: An
Approach to High-assurance Microkernel Development. In Haskell Symposium. ACM, 60–71. DOI:http://dx.doi.org/10.
1145/1159842.1159850

Ready, Set, Verify!

29

Peter Dybjer, Qiao Haiyan, and Makoto Takeyama. 2004. Verifying Haskell programs by combining testing, model
checking and interactive theorem proving. Information & Software Technology 46, 15 (2004), 1011–1025. DOI:http:
//dx.doi.org/10.1016/j.infsof.2004.07.002
Jean-Christophe Filliâtre and Pierre Letouzey. 2004. Functors for Proofs and Programs. In Programming Languages and
Systems, David Schmidt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 370–384.
Thomas Hallgren, James Hook, Mark P. Jones, and Richard B. Kieburtz. 2004. An overview of the programatica toolset. In
HCSS.
Yoichi Hirai and Kazuhiko Yamamoto. 2011. Balancing weight-balanced trees. Journal of Functional Programming 21, 3
(2011), 287–307. DOI:http://dx.doi.org/10.1017/S0956796811000104
Adam Megacz Joseph. 2014. Generalized Arrows. (May 2014). http://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/
EECS-2014-130.html also see http://www.megacz.com/berkeley/coq-in-ghc/.
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai
Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal
Verification of an OS Kernel. In ACM Symposium on Operating Systems Principles. ACM, Big Sky, MT, USA, 207–220.
Alexander Krauss. 2006. Partial Recursive Functions in Higher-Order Logic. In IJCAR (LNCS), Vol. 4130. Springer, 589–603.
Daniel Kröning, Philipp Rümmer, and Georg Weissenbacher. 2009. A proposal for a theory of finite sets, lists, and maps for
the SMT-LIB standard. In Informal proceedings, 7th International Workshop on Satisfiability Modulo Theories at CADE,
Vol. 22.
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML.
In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). ACM,
New York, NY, USA, 179–191.
Pierre Letouzey. 2002. A New Extraction for Coq. In TYPES (LNCS), Vol. 2646. Springer, 200–219. DOI:http://dx.doi.org/10.
1007/3-540-39185-1_12
Dan Licata. 2012. 15-150 Lecture 21: Red-Black Trees. (2012). https://www.cs.cmu.edu/~15150/previous-semesters/
2012-spring/resources/lectures/21.pdf Lecture at the Oregon Programming Language Summer School.
The Coq development team. 2016. The Coq proof assistant reference manual. LogiCal Project. http://coq.inria.fr Version
8.6.1.
Conor Thomas McBride. 2014. How to Keep Your Neighbours in Order. In Proceedings of the 19th ACM SIGPLAN International
Conference on Functional Programming (ICFP ’14). ACM, New York, NY, USA, 297–309. DOI:http://dx.doi.org/10.1145/
2628136.2628163
Donald R. Morrison. 1968. PATRICIA&Mdash;Practical Algorithm To Retrieve Information Coded in Alphanumeric. J. ACM
15, 4 (Oct. 1968), 514–534. DOI:http://dx.doi.org/10.1145/321479.321481
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman. 2018. &#338;Uf: Minimizing the Coq
Extraction TCB. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP
2018). ACM, New York, NY, USA, 172–185. DOI:http://dx.doi.org/10.1145/3167089
Magnus O. Myreen and Scott Owens. 2014. Proof-producing translation of higher-order logic into pure and stateful ML.
Journal of Functional Programming 24 (May 2014), 284–315. DOI:http://dx.doi.org/10.1017/S0956796813000282
Jürg Nievergelt and Edward M. Reingold. 1972. Binary Search Trees of Bounded Balance. In STOC. ACM, 137–142. DOI:
http://dx.doi.org/10.1145/800152.804906
Tobias Nipkow. 2016. Automatic Functional Correctness Proofs for Functional Search Trees. In Interactive Theorem Proving
(ITP 2016), J. Blanchette and S. Merz (Eds.), Vol. 9807. 307–322.
Tobias Nipkow and Stefan Dirix. 2018. Weight-Balanced Trees. Archive of Formal Proofs (March 2018). http://isa-afp.org/
entries/Weight_Balanced_Trees.html, Formal proof development.
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL - A Proof Assistant for Higher-Order Logic.
Lecture Notes in Computer Science, Vol. 2283. Springer. DOI:http://dx.doi.org/10.1007/3-540-45949-9
Liam O’Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas
Sewell, and Gerwin Klein. 2016. Refinement Through Restraint: Bringing Down the Cost of Verification. In International
Conference on Functional Programming. Nara, Japan.
Chris Okasaki. 1999. Purely functional data structures. Cambridge University Press. DOI:http://dx.doi.org/10.1017/
CBO9780511530104
Chris Okasaki and Andrew Gill. 1998. Fast Mergeable Integer Maps. In In Workshop on ML. 77–86.
Simon Peyton Jones, Andrew Tolmach, and Tony Hoare. 2001. Playing by the rules: rewriting as a practical optimisation
technique in GHC. In Haskell Workshop.
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago ZanellaBéguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. 2017.
Verified Low-level Programming Embedded in F*. Proc. ACM Program. Lang. 1, ICFP, Article 17 (Aug. 2017), 29 pages.
DOI:http://dx.doi.org/10.1145/3110261

30

Breitner, Spector-Zabusky, Li, Rizkallah, Wiegley and Weirich

Ryan Ralston. 2009. ACL2-certified AVL Trees. In Proceedings of the Eighth International Workshop on the ACL2 Theorem
Prover and Its Applications (ACL2 ’09). ACM, New York, NY, USA, 71–74. DOI:http://dx.doi.org/10.1145/1637837.1637848
Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O’Connor, Toby Murray, Gabriele
Keller, and Gerwin Klein. 2016. A Framework for the Automatic Formal Verification of Refinement from Cogent to C. In
International Conference on Interactive Theorem Proving. Nancy, France.
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. 2018. Total Haskell is reasonable Coq.
In CPP. ACM, 14–27. DOI:http://dx.doi.org/10.1145/3167092
Milan Straka. 2010. The Performance of the Haskell Containers Package. In Proceedings of the Third ACM Haskell Symposium
on Haskell (Haskell ’10). ACM, New York, NY, USA, 13–24. DOI:http://dx.doi.org/10.1145/1863523.1863526
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan
Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago ZanellaBéguelin. 2016. Dependent Types and Multi-monadic Effects in F*. In Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, New York, NY, USA, 256–270. DOI:
http://dx.doi.org/10.1145/2837614.2837655
Niki Vazou, Leonidas Lampropoulos, and Jeff Polakow. 2017. A Tale of Two Provers: Verifying Monoidal String Matching in
Liquid Haskell and Coq. In Haskell Symposium. ACM, 63–74. DOI:http://dx.doi.org/10.1145/3122955.3122963
Niki Vazou, Patrick M. Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In Proceedings of the 22Nd European
Conference on Programming Languages and Systems (ESOP’13). Springer-Verlag, Berlin, Heidelberg, 209–228. DOI:
http://dx.doi.org/10.1007/978-3-642-37036-6_13
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement Types for Haskell.
In ICFP. ACM, 269–282. DOI:http://dx.doi.org/10.1145/2628136.2628161
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2018.
Refinement reflection: complete verification with SMT. PACMPL 2, POPL (2018), 53:1–53:31. DOI:http://dx.doi.org/10.
1145/3158141
Dimitrios Vytiniotis, Simon Peyton Jones, Koen Claessen, and Dan Rosén. 2013. HALO: Haskell to Logic Through Denotational Semantics. In POPL. ACM, 431–442. DOI:http://dx.doi.org/10.1145/2429069.2429121
John Wiegley. 2017. coq-haskell: A library for formalizing Haskell types and functions in Coq. https://github.com/
jwiegley/coq-haskell. (2017).

