Elemental Measures

Talking about Sets

First, we need a way to talk about sets in the refinement logic. We could roll our own special Haskell type but for now, let’s just use the Set a type from the prelude’s Data.Set.¹

LiquidHaskell Lifts the basic set operators from Data.Set into the refinement logic. That is, the prelude defines the following logical functions that correspond to the Haskell functions of the same name:

measure empty        :: Set a
measure singleton    :: a -> Set a
measure member       :: a -> Set a -> Bool
measure union        :: Set a -> Set a -> Set a
measure intersection :: Set a -> Set a -> Set a
measure difference   :: Set a -> Set a -> Set a

The above operators are interpreted by the SMT solver. That is, just like the SMT solver “knows”, via the axioms of the theory of arithmetic that: \[x = 1 + 1 \Rightarrow x = 2\] is a valid formula, i.e. holds for all \(x\), the solver “knows” that: \[x = \tsng{1} \Rightarrow y = \tsng{2} \Rightarrow x = \tcap{x}{\tcup{y}{x}}\] This is because, the above formulas belong to a decidable Theory of Sets reduces to McCarthy’s more general Theory of Arrays. ²

Proving QuickCheck Style Properties

To get the hang of whats going on, let’s do a few warm up exercises, using LiquidHaskell to prove various simple theorems about sets and operations over them.

We Refine The Set API to make it easy to write down theorems. That is, we give the operators in Data.Set refinement type signatures that precisely track their set-theoretic behavior:

empty        :: {v:Set a | v = empty}
member       :: x:a
             -> s:Set a
             -> {v:Bool | v <=> member x s}

singleton    :: x:a -> {v:Set a | v = singleton x}

union        :: x:Set a
             -> y:Set a
             -> {v:Set a | v = union x y}

intersection :: x:Set a
             -> y:Set a
             -> {v:Set a | v = intersection x y}

difference   :: x:Set a
             -> y:Set a
             -> {v:Set a | v = difference x y}

We Can Assert Theorems as QuickCheck style properties, that is, as functions from arbitrary inputs to a Bool output that must always be True. Lets define aliases for the Booleans that are always True or False

We can use True to state theorems. For example, the unexciting arithmetic equality above becomes:

Where implies is just the implication function over Bool

and Implies p q is defined as

The Commutativity of Intersection can be easily stated and proved as a QuickCheck style theorem:

The Associativity of Union can similarly be confirmed:

The Distributivity Laws for Boolean Algebra can be verified by writing properties over the relevant operators. For example, let’s check that intersection distributes over union:

Non-Theorems should be rejected. So, while we’re at it, let’s make sure LiquidHaskell doesn’t prove anything that isn’t true …

Thus, LiquidHaskell’s refined types offer a nice interface for interacting with the SMT solvers in order to prove theorems, while letting us use QuickCheck to generate counterexamples.³

Content-Aware List API

Lets return to our real goal, which is to verify properties of programs. First, we need a way to refine the list API to precisely track the set of elements in a list.

The Elements of a List can be described by a simple recursive measure that walks over the list, building up the set:

Lets write a few helpful aliases for various refined lists that will then make the subsequent specifications pithy and crisp.

• A list with elements S

• An empty list

• A list whose contents equal those of list X

• A list whose contents are a subset of list X

• A list whose contents are the union of lists X and Y

• A list whose contents are exactly X and the contents of Y

The Measures strengthens the data constructors for lists. That is we get the automatically refined types for “nil” and “cons”:

data [a] where
  []  :: ListEmp a
  (:) :: x:a -> xs:[a] -> ListUn1 a x xs

Lets take our new vocabulary out for a spin!

The Append function returns a list whose elements are the union of the elements of the input Lists:

Hint: You may want to remind yourself about the dimension-aware signature for partition from the earlier chapter.

Permutations

Next, let’s use the refined list API to prove that various sorting routines return permutations of their inputs, that is, return output lists whose elements are the same as those of the input lists.⁴

Insertion Sort is the simplest of all the list sorting routines; we build up an (ordered) output list inserting each element of the input list into the appropriate position of the output:

Thus, the output of insert has all the elements of the input xs, plus the new element x:

The above signature lets us prove that the output of the sorting routine indeed has the elements of the input:

Uniqueness

Often, we want to enforce the invariant that a particular collection contains no duplicates; as multiple copies in a collection of file handles or system resources can create unpleasant leaks. For example, the xmonad window manager creates a sophisticated zipper data structure to hold the list of active user windows and carefully maintains the invariant that that the zipper contains no duplicates. Next, let’s see how to specify and verify this invariant using LiquidHaskell, first for lists, and then for a simplified zipper.

To Specify Uniqueness we need a way of saying that a list has no duplicates. There are many ways to do so; the simplest is a measure:

We can use the above to write an alias for duplicate-free lists

Lets quickly check that the right lists are indeed unique

The Filter function returns a subset of its elements, and hence, preserves uniqueness. That is, if the input is unique, the output is too:

The Nub function constructs a unique list from an arbitrary input by traversing the input and tossing out elements that are already seen:

The key membership test is done by isin, whose output is True exactly when the element is in the given list. ⁵

Hint: This may be easier to do after you read this chapter about lemmas.

Unique Zippers

A zipper is an aggregate data structure that is used to arbitrarily traverse the structure and update its contents. For example, a zipper for a list is a data type that contains an element (called focus) that we are currently focus-ed on, a list of elements to the left of (i.e. before) the focus, and a list of elements to the right (i.e. after) the focus.

xmonad is a wonderful tiling window manager, that uses a zipper to store the set of windows being managed. xmonad requires the crucial invariant that the values in the zipper be unique, that is, be free of duplicates.

We Refine Zipper to capture the requirement that legal zippers are unique. To this end, we state that the left and right lists are unique, disjoint, and do not contain focus.

Our Refined Zipper Constructor makes illegal states unrepresentable. That is, by construction, we will ensure that every Zipper is free of duplicates. For example, it is straightforward to create a valid Zipper from a unique list:

We can Shift the Focus element to the left or right while preserving the uniqueness invariant. Here’s the code that shifts the focus to the left:

To shift to the right, we simply reverse the elements and shift to the left:

To Filter elements from a zipper, we need to take care when the focus itself, or all the elements get eliminated. In the latter case, there is no Zipper and so the operation returns a Maybe:

Thus, by using LiquidHaskell’s refinement types, and the SMT solvers native reasoning about sets, we can ensure the key uniqueness invariant holds in the presence of various tricky operations that are performed over Zippers.

Recap

In this chapter, we saw how SMT solvers can let us reason precisely about the actual contents of data structures, via the theory of sets. In particular, we saw how to:

• Lift set-theoretic primitives to refined Haskell functions from the Data.Set library,

• Define measures like elts that characterize the set of elements of structures, and unique that describe high-level application specific properties about those sets,

• Specify and verify that implementations enjoy various functional correctness properties, e.g. that sorting routines return permutations of their inputs, and various zipper operators preserve uniqueness.

Next, we present a variety of longer case-studies that illustrate the techniques developed so far on particular application domains.