LiquidHaskell

Refinement Types via SMT and Predicate Abstraction

In the posts so far, we’ve seen how LiquidHaskell allows you to use SMT solvers to specify and verify numeric invariants – denominators that are non-zero, integer indices that are within the range of an array, vectors that have the right number of dimensions and so on.

However, SMT solvers are not limited to numbers, and in fact, support rather expressive logics. In the next couple of posts, let’s see how LiquidHaskell uses SMT to talk about sets of values, for example, the contents of a list, and to specify and verify properties about those sets.

27: module TalkingAboutSets where
28: 
29: import Data.Set hiding (filter, split)
30: import Prelude  hiding (reverse, filter)
31: 

Talking about Sets (In Logic)

First, we need a way to talk about sets in the refinement logic. We could roll our own special Haskell type, but why not just use the Set a type from Data.Set.

The import Data.Set , also instructs LiquidHaskell to import in the various specifications defined for the Data.Set module that we have predefined in Data/Set.spec

Let’s look at the specifications.

46: module spec Data.Set where
47: 
48: embed Set as Set_Set

The embed directive tells LiquidHaskell to model the Haskell type constructor Set with the SMT type constructor Set_Set.

First, we define the logical operators (i.e. measures)

55: measure Set_sng  :: a -> (Set a)                    -- ^ singleton
56: measure Set_cup  :: (Set a) -> (Set a) -> (Set a)   -- ^ union
57: measure Set_cap  :: (Set a) -> (Set a) -> (Set a)   -- ^ intersection
58: measure Set_dif  :: (Set a) -> (Set a) -> (Set a)   -- ^ difference 

Next, we define predicates on Sets

62: measure Set_emp  :: (Set a) -> Prop                 -- ^ emptiness
63: measure Set_mem  :: a -> (Set a) -> Prop            -- ^ membership
64: measure Set_sub  :: (Set a) -> (Set a) -> Prop      -- ^ inclusion 

Interpreted Operations

The above operators are interpreted by the SMT solver.

That is, just like the SMT solver “knows that”

74: 2 + 2 == 4

the SMT solver also “knows that”

78: (Set_sng 1) == (Set_cap (Set_sng 1) (Set_cup (Set_sng 2) (Set_sng 1)))

This is because, the above formulas belong to a decidable Theory of Sets which can be reduced to McCarthy’s more general Theory of Arrays. See this recent paper if you want to learn more about how modern SMT solvers “know” the above equality holds…

Talking about Sets (In Code)

Of course, the above operators exist purely in the realm of the refinement logic, beyond the grasp of the programmer.

To bring them down (or up, or left or right) within reach of Haskell code, we can simply assume that the various public functions in Data.Set do the Right Thing i.e. produce values that reflect the logical set operations:

First, the functions that create Set values

97: empty     :: {v:(Set a) | (Set_emp v)}
98: singleton :: x:a -> {v:(Set a) | v = (Set_sng x)}

Next, the functions that operate on elements and Set values

102: insert :: Ord a => x:a 
103:                 -> xs:(Set a) 
104:                 -> {v:(Set a) | v = (Set_cup xs (Set_sng x))}
105: 
106: delete :: Ord a => x:a 
107:                 -> xs:(Set a) 
108:                 -> {v:(Set a) | v = (Set_dif xs (Set_sng x))}

Then, the binary Set operators

112: union        :: Ord a => xs:(Set a) 
113:                       -> ys:(Set a) 
114:                       -> {v:(Set a) | v = (Set_cup xs ys)}
115: 
116: intersection :: Ord a => xs:(Set a) 
117:                       -> ys:(Set a) 
118:                       -> {v:(Set a) | v = (Set_cap xs ys)}
119: 
120: difference   :: Ord a => xs:(Set a) 
121:                       -> ys:(Set a) 
122:                       -> {v:(Set a) | v = (Set_dif xs ys)}

And finally, the predicates on Set values:

126: isSubsetOf :: Ord a => xs:(Set a) 
127:                     -> ys:(Set a) 
128:                     -> {v:Bool | (Prop v) <=> (Set_sub xs ys)}
129: 
130: member     :: Ord a => x:a 
131:                     -> xs:(Set a) 
132:                     -> {v:Bool | (Prop v) <=> (Set_mem x xs)}

Note: Of course we shouldn’t and needn’t really assume, but should and will guarantee that the functions from Data.Set implement the above types. But thats a story for another day…

Proving Theorems With LiquidHaskell

OK, let’s take our refined operators from Data.Set out for a spin! One pleasant consequence of being able to precisely type the operators from Data.Set is that we have a pleasant interface for using the SMT solver to prove theorems about sets, while remaining firmly rooted in Haskell.

First, let’s write a simple function that asserts that its input is True

151: {-@ boolAssert :: {v: Bool | (Prop v)} -> {v:Bool | (Prop v)} @-}
152: {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> {VV : (GHC.Types.Bool) | (? Prop([VV]))}boolAssert True   = {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV = True)}True
153: boolAssert False  = [(GHC.Types.Char)] -> {VV : (GHC.Types.Bool) | false}error {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"boolAssert: False? Never!"

Now, we can use boolAssert to write some simple properties. (Yes, these do indeed look like QuickCheck properties – but here, instead of generating tests and executing the code, the type system is proving to us that the properties will always evaluate to True)

Let’s check that intersection is commutative …

164: forall a.
(GHC.Classes.Ord a) =>
(Data.Set.Base.Set a) -> (Data.Set.Base.Set a) -> (GHC.Types.Bool)prop_cap_comm (Data.Set.Base.Set a)x (Data.Set.Base.Set a)y 
165:   = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> {VV : (GHC.Types.Bool) | (? Prop([VV]))}boolAssert 
166:   ({VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}
 -> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)})
-> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}
-> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}$ (GHC.Types.Bool)({VV : (Data.Set.Base.Set a) | (VV = x)}x xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cap([xs; ys]))}`intersection` {VV : (Data.Set.Base.Set a) | (VV = y)}y) GHC.Classes.Eq (Data.Set.Base.Set a)== ({VV : (Data.Set.Base.Set a) | (VV = y)}y xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cap([xs; ys]))}`intersection` {VV : (Data.Set.Base.Set a) | (VV = x)}x)

that union is associative …

172: forall a.
(GHC.Classes.Ord a) =>
(Data.Set.Base.Set a)
-> (Data.Set.Base.Set a)
-> (Data.Set.Base.Set a)
-> (GHC.Types.Bool)prop_cup_assoc (Data.Set.Base.Set a)x (Data.Set.Base.Set a)y (Data.Set.Base.Set a)z 
173:   = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> {VV : (GHC.Types.Bool) | (? Prop([VV]))}boolAssert 
174:   ({VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}
 -> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)})
-> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}
-> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}$ (GHC.Types.Bool)({VV : (Data.Set.Base.Set a) | (VV = x)}x xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cup([xs; ys]))}`union` ({VV : (Data.Set.Base.Set a) | (VV = y)}y xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cup([xs; ys]))}`union` {VV : (Data.Set.Base.Set a) | (VV = z)}z)) GHC.Classes.Eq (Data.Set.Base.Set a)== (Data.Set.Base.Set a)({VV : (Data.Set.Base.Set a) | (VV = x)}x xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cup([xs; ys]))}`union` {VV : (Data.Set.Base.Set a) | (VV = y)}y) xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cup([xs; ys]))}`union` {VV : (Data.Set.Base.Set a) | (VV = z)}z

and that union distributes over intersection.

180: forall a.
(GHC.Classes.Ord a) =>
(Data.Set.Base.Set a)
-> (Data.Set.Base.Set a)
-> (Data.Set.Base.Set a)
-> (GHC.Types.Bool)prop_cap_dist (Data.Set.Base.Set a)x (Data.Set.Base.Set a)y (Data.Set.Base.Set a)z 
181:   = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> {VV : (GHC.Types.Bool) | (? Prop([VV]))}boolAssert 
182:   ({VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}
 -> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)})
-> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}
-> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}$  ({VV : (Data.Set.Base.Set a) | (VV = x)}x xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cap([xs; ys]))}`intersection` ({VV : (Data.Set.Base.Set a) | (VV = y)}y xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cup([xs; ys]))}`union` {VV : (Data.Set.Base.Set a) | (VV = z)}z)) 
183:   GHC.Classes.Eq (Data.Set.Base.Set a)== (Data.Set.Base.Set a)({VV : (Data.Set.Base.Set a) | (VV = x)}x xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cap([xs; ys]))}`intersection` {VV : (Data.Set.Base.Set a) | (VV = y)}y) xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cup([xs; ys]))}`union` ({VV : (Data.Set.Base.Set a) | (VV = x)}x xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cap([xs; ys]))}`intersection` {VV : (Data.Set.Base.Set a) | (VV = z)}z) 

Of course, while we’re at it, let’s make sure LiquidHaskell doesn’t prove anything that isn’t true …

190: forall a.
(GHC.Classes.Ord a) =>
(Data.Set.Base.Set a) -> (Data.Set.Base.Set a) -> (GHC.Types.Bool)prop_cup_dif_bad (Data.Set.Base.Set a)x (Data.Set.Base.Set a)y
191:    = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> {VV : (GHC.Types.Bool) | (? Prop([VV]))}boolAssert 
192:    ((GHC.Types.Bool)
 -> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)})
-> (GHC.Types.Bool)
-> {VV : (GHC.Types.Bool) | (? Prop([VV])),(VV != False)}$ {VV : (Data.Set.Base.Set a) | (VV = x)}x GHC.Classes.Eq (Data.Set.Base.Set a)== (Data.Set.Base.Set a)({VV : (Data.Set.Base.Set a) | (VV = x)}x xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_cup([xs; ys]))}`union` {VV : (Data.Set.Base.Set a) | (VV = y)}y) xs:(Data.Set.Base.Set a)
-> ys:(Data.Set.Base.Set a)
-> {VV : (Data.Set.Base.Set a) | (VV = Set_dif([xs; ys]))}`difference` {VV : (Data.Set.Base.Set a) | (VV = y)}y

Hmm. You do know why the above doesn’t hold, right? It would be nice to get a counterexample wouldn’t it? Well, for the moment, there is QuickCheck!

Thus, the refined types offer a nice interface for interacting with the SMT solver in order to prove theorems in LiquidHaskell. (BTW, The SBV project describes another approach for using SMT solvers from Haskell, without the indirection of refinement types.)

While the above is a nice warm up exercise to understanding how LiquidHaskell reasons about sets, our overall goal is not to prove theorems about set operators, but instead to specify and verify properties of programs.

The Set of Values in a List

Let’s see how we might reason about sets of values in regular Haskell programs.

We’ll begin with Lists, the jack-of-all-data-types. Now, instead of just talking about the number of elements in a list, we can write a measure that describes the set of elements in a list:

A measure for the elements of a list, from Data/Set.spec

221: 
222: measure listElts :: [a] -> (Set a) 
223: listElts ([])    = {v | (? Set_emp(v))}
224: listElts (x:xs)  = {v | v = (Set_cup (Set_sng x) (listElts xs)) }

That is, (listElts xs) describes the set of elements contained in a list xs.

Next, to make the specifications concise, let’s define a few predicate aliases:

232: {-@ predicate EqElts  X Y = 
233:       ((listElts X) = (listElts Y))                        @-}
234: 
235: {-@ predicate SubElts   X Y = 
236:       (Set_sub (listElts X) (listElts Y))                  @-}
237: 
238: {-@ predicate UnionElts X Y Z = 
239:       ((listElts X) = (Set_cup (listElts Y) (listElts Z))) @-}

A Trivial Identity

OK, now let’s write some code to check that the listElts measure is sensible!

248: {-@ listId    :: xs:[a] -> {v:[a] | (EqElts v xs)} @-}
249: forall a.
x1:[a]
-> {VV : [a] | (len([VV]) = len([x1])),
               (listElts([VV]) = Set_cup([listElts([x1]); listElts([x1])])),
               (listElts([VV]) = listElts([x1])),
               (listElts([x1]) = Set_cup([listElts([x1]); listElts([VV])])),
               (len([VV]) >= 0)}listId []     = forall <p :: a -> a -> Bool>.
{VV : [{VV : a | false}]<p> | (? Set_emp([listElts([VV])])),
                              (len([VV]) = 0)}[]
250: listId (x:xs) = {VV : a | (VV = x)}x forall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}: forall a.
x1:[a]
-> {VV : [a] | (len([VV]) = len([x1])),
               (listElts([VV]) = Set_cup([listElts([x1]); listElts([x1])])),
               (listElts([VV]) = listElts([x1])),
               (listElts([x1]) = Set_cup([listElts([x1]); listElts([VV])])),
               (len([VV]) >= 0)}listId {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs

That is, LiquidHaskell checks that the set of elements of the output list is the same as those in the input.

A Less Trivial Identity

Next, let’s write a function to reverse a list. Of course, we’d like to verify that reverse doesn’t leave any elements behind; that is that the output has the same set of values as the input list. This is somewhat more interesting because of the tail recursive helper go. Do you understand the type that is inferred for it? (Put your mouse over go to see the inferred type.)

267: {-@ reverse       :: xs:[a] -> {v:[a] | (EqElts v xs)} @-}
268: forall a. xs:[a] -> {VV : [a] | (listElts([VV]) = listElts([xs]))}reverse           = x1:{VV : [{VV : a | false}]<\_ VV -> false> | (len([VV]) = 0)}
-> x2:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([x2])])),
               (listElts([VV]) = Set_cup([listElts([x2]); listElts([x1])])),
               (len([VV]) >= 0)}go {VV : [{VV : a | false}]<\_ VV -> false> | (? Set_emp([listElts([VV])])),
                                           (len([VV]) = 0),
                                           (len([VV]) >= 0)}[] 
269:   where 
270:     acc:{VV : [a] | (len([VV]) >= 0)}
-> x1:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([acc]);
                                          listElts([x1])])),
               (listElts([VV]) = Set_cup([listElts([x1]); listElts([acc])])),
               (len([VV]) >= 0)}go {VV : [a] | (len([VV]) >= 0)}acc []     = {VV : [a] | (VV = acc),(len([VV]) >= 0)}acc
271:     go acc (y:ys) = acc:{VV : [a] | (len([VV]) >= 0)}
-> x1:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([acc]);
                                          listElts([x1])])),
               (listElts([VV]) = Set_cup([listElts([x1]); listElts([acc])])),
               (len([VV]) >= 0)}go ({VV : a | (VV = y)}yforall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}:{VV : [a] | (VV = acc),(len([VV]) >= 0)}acc) {VV : [a] | (VV = ys),(len([VV]) >= 0)}ys

Appending Lists

Next, here’s good old append, but now with a specification that states that the output indeed includes the elements from both the input lists.

281: {-@ append       :: xs:[a] -> ys:[a] -> {v:[a]| (UnionElts v xs ys)} @-}
282: forall a.
x1:[a]
-> ys:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([ys])])),
               (listElts([VV]) = Set_cup([listElts([ys]); listElts([x1])])),
               (len([VV]) >= 0)}append []     [a]ys = {VV : [a] | (VV = ys),(len([VV]) >= 0)}ys
283: append (x:xs) ys = {VV : a | (VV = x)}x forall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}: forall a.
x1:[a]
-> ys:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([ys])])),
               (listElts([VV]) = Set_cup([listElts([ys]); listElts([x1])])),
               (len([VV]) >= 0)}append {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs {VV : [a] | (VV = ys),(len([VV]) >= 0)}ys

Filtering Lists

Let’s round off the list trilogy, with filter. Here, we can verify that it returns a subset of the values of the input list.

293: {-@ filter      :: (a -> Bool) -> xs:[a] -> {v:[a]| (SubElts v xs)} @-}
294: 
295: forall a.
(a -> (GHC.Types.Bool))
-> x2:[a]
-> {VV : [a] | (? Set_sub([listElts([VV]); listElts([x2])])),
               (listElts([x2]) = Set_cup([listElts([x2]); listElts([VV])])),
               (len([VV]) >= 0)}filter a -> (GHC.Types.Bool)f []     = forall <p :: a -> a -> Bool>.
{VV : [{VV : a | false}]<p> | (? Set_emp([listElts([VV])])),
                              (len([VV]) = 0)}[]
296: filter f (x:xs) 
297:   | a -> (GHC.Types.Bool)f {VV : a | (VV = x)}x         = {VV : a | (VV = x)}x forall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}: forall a.
(a -> (GHC.Types.Bool))
-> x2:[a]
-> {VV : [a] | (? Set_sub([listElts([VV]); listElts([x2])])),
               (listElts([x2]) = Set_cup([listElts([x2]); listElts([VV])])),
               (len([VV]) >= 0)}filter a -> (GHC.Types.Bool)f {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs 
298:   | otherwise   = forall a.
(a -> (GHC.Types.Bool))
-> x2:[a]
-> {VV : [a] | (? Set_sub([listElts([VV]); listElts([x2])])),
               (listElts([x2]) = Set_cup([listElts([x2]); listElts([VV])])),
               (len([VV]) >= 0)}filter a -> (GHC.Types.Bool)f {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs

Merge Sort

Let’s conclude this entry with one larger example: mergeSort. We’d like to verify that, well, the list that is returned contains the same set of elements as the input list.

And so we will!

But first, let’s remind ourselves of how mergeSort works:

  1. split the input list into two halves,
  2. sort each half, recursively,
  3. merge the sorted halves to obtain the sorted list.

Split

We can split a list into two, roughly equal parts like so:

323: forall a.
x1:[a]
-> ({VV : [a] | (? Set_sub([listElts([VV]); listElts([x1])])),
                (listElts([x1]) = Set_cup([listElts([x1]); listElts([VV])])),
                (len([VV]) >= 0)} , {VV : [a] | (? Set_sub([listElts([VV]);
                                                            listElts([x1])])),
                                                (listElts([x1]) = Set_cup([listElts([x1]);
                                                                           listElts([VV])])),
                                                (len([VV]) >= 0)})<\x1 VV -> (? Set_sub([listElts([VV]);
                                                                                         listElts([x1])])),
                                                                             (listElts([x1]) = Set_cup([listElts([x1]);
                                                                                                        listElts([VV])])),
                                                                             (listElts([x1]) = Set_cup([listElts([x1]);
                                                                                                        listElts([VV])])),
                                                                             (len([VV]) >= 0)>split []     = forall a b <p2 :: a -> b -> Bool>. x1:a -> b<p2 x1> -> (a , b)<p2>({VV : [{VV : a | false}]<\_ VV -> false> | (? Set_emp([listElts([VV])])),
                                           (len([VV]) = 0),
                                           (len([VV]) >= 0)}[], {VV : [{VV : a | false}]<\_ VV -> false> | (? Set_emp([listElts([VV])])),
                                           (len([VV]) = 0),
                                           (len([VV]) >= 0)}[])
324: split (x:xs) = forall a b <p2 :: a -> b -> Bool>. x1:a -> b<p2 x1> -> (a , b)<p2>({VV : a | (VV = x)}xforall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}:{VV : [a] | (? Set_sub([listElts([VV]); listElts([xs])])),
            (VV = zs),
            (VV = zs),
            (len([VV]) = len([zs])),
            (listElts([VV]) = Set_cup([listElts([zs]); listElts([zs])])),
            (listElts([VV]) = listElts([zs])),
            (listElts([xs]) = Set_cup([listElts([xs]); listElts([VV])])),
            (listElts([xs]) = Set_cup([listElts([ys]); listElts([VV])])),
            (listElts([xs]) = Set_cup([listElts([ys]); listElts([VV])])),
            (listElts([zs]) = Set_cup([listElts([zs]); listElts([VV])])),
            (len([VV]) >= 0)}zs, {VV : [a] | (? Set_sub([listElts([VV]); listElts([xs])])),
            (VV = ys),
            (VV = ys),
            (len([VV]) = len([ys])),
            (listElts([VV]) = Set_cup([listElts([ys]); listElts([ys])])),
            (listElts([VV]) = listElts([ys])),
            (listElts([xs]) = Set_cup([listElts([xs]); listElts([VV])])),
            (listElts([xs]) = Set_cup([listElts([zs]); listElts([VV])])),
            (listElts([ys]) = Set_cup([listElts([ys]); listElts([VV])])),
            (len([VV]) >= 0)}ys)
325:   where 
326:     ({VV : [a] | (? Set_sub([listElts([VV]); listElts([xs])])),
            (VV = ys),
            (len([VV]) = len([ys])),
            (listElts([VV]) = Set_cup([listElts([ys]); listElts([ys])])),
            (listElts([VV]) = listElts([ys])),
            (listElts([xs]) = Set_cup([listElts([xs]); listElts([VV])])),
            (listElts([xs]) = Set_cup([listElts([zs]); listElts([VV])])),
            (listElts([ys]) = Set_cup([listElts([ys]); listElts([VV])])),
            (len([VV]) >= 0)}ys, {VV : [a] | (? Set_sub([listElts([VV]); listElts([xs])])),
            (VV = zs),
            (len([VV]) = len([zs])),
            (listElts([VV]) = Set_cup([listElts([zs]); listElts([zs])])),
            (listElts([VV]) = listElts([zs])),
            (listElts([xs]) = Set_cup([listElts([xs]); listElts([VV])])),
            (listElts([xs]) = Set_cup([listElts([ys]); listElts([VV])])),
            (listElts([xs]) = Set_cup([listElts([ys]); listElts([VV])])),
            (listElts([zs]) = Set_cup([listElts([zs]); listElts([VV])])),
            (len([VV]) >= 0)}zs) = forall a.
x1:[a]
-> ({VV : [a] | (? Set_sub([listElts([VV]); listElts([x1])])),
                (listElts([x1]) = Set_cup([listElts([x1]); listElts([VV])])),
                (len([VV]) >= 0)} , {VV : [a] | (? Set_sub([listElts([VV]);
                                                            listElts([x1])])),
                                                (listElts([x1]) = Set_cup([listElts([x1]);
                                                                           listElts([VV])])),
                                                (len([VV]) >= 0)})<\x1 VV -> (? Set_sub([listElts([VV]);
                                                                                         listElts([x1])])),
                                                                             (listElts([x1]) = Set_cup([listElts([x1]);
                                                                                                        listElts([VV])])),
                                                                             (listElts([x1]) = Set_cup([listElts([x1]);
                                                                                                        listElts([VV])])),
                                                                             (len([VV]) >= 0)>split {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs

LiquidHaskell verifies that the relevant property of split is

332: {-@ split :: xs:[a] -> ([a], [a])<{\ys zs -> (UnionElts xs ys zs)}> @-}

The funny syntax with angle brackets simply says that the output of split is a pair (ys, zs) whose union is the list of elements of the input xs. (Yes, this is indeed a dependent pair; we will revisit these later to understand whats going on with the odd syntax.)

Merge

Next, we can merge two (sorted) lists like so:

346: forall a.
(GHC.Classes.Ord a) =>
xs:[a]
-> x1:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([xs])])),
               (listElts([VV]) = Set_cup([listElts([xs]); listElts([x1])])),
               (len([VV]) >= 0)}merge [a]xs []         = {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs
347: merge [] ys         = {VV : [a] | (len([VV]) >= 0)}ys
348: merge (x:xs) (y:ys) 
349:   | {VV : a | (VV = x)}x x:a
-> y:a -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : a | (VV = y)}y          = {VV : a | (VV = x)}x forall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}: forall a.
(GHC.Classes.Ord a) =>
xs:[a]
-> x1:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([xs])])),
               (listElts([VV]) = Set_cup([listElts([xs]); listElts([x1])])),
               (len([VV]) >= 0)}merge {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs ({VV : a | (VV = y)}y forall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}: {VV : [a] | (VV = ys),(len([VV]) >= 0)}ys)
350:   | otherwise       = {VV : a | (VV = y)}y forall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}: forall a.
(GHC.Classes.Ord a) =>
xs:[a]
-> x1:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([xs])])),
               (listElts([VV]) = Set_cup([listElts([xs]); listElts([x1])])),
               (len([VV]) >= 0)}merge ({VV : a | (VV = x)}x forall <p :: a -> a -> Bool>.
y:a
-> ys:[a<p y>]<p>
-> {VV : [a]<p> | (len([VV]) = (1 + len([ys]))),
                  (listElts([VV]) = Set_cup([Set_sng([y]); listElts([ys])]))}: {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs) {VV : [a] | (VV = ys),(len([VV]) >= 0)}ys

As you might expect, the elements of the returned list are the union of the elements of the input, or as LiquidHaskell might say,

357: {-@ merge :: (Ord a) => x:[a] -> y:[a] -> {v:[a]| (UnionElts v x y)} @-}

Sort

Finally, we put all the pieces together by

366: {-@ mergeSort :: (Ord a) => xs:[a] -> {v:[a] | (EqElts v xs)} @-}
367: forall a.
(GHC.Classes.Ord a) =>
x1:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([x1])])),
               (listElts([VV]) = listElts([x1])),
               (listElts([x1]) = Set_cup([listElts([x1]); listElts([VV])]))}mergeSort []  = forall <p :: a -> a -> Bool>.
{VV : [{VV : a | false}]<p> | (? Set_emp([listElts([VV])])),
                              (len([VV]) = 0)}[]
368: mergeSort [x] = {VV : [{VV : a | false}]<\_ VV -> false> | (? Set_emp([listElts([VV])])),
                                           (len([VV]) = 0),
                                           (len([VV]) >= 0)}[{VV : a | (VV = x)}x]
369: mergeSort xs  = x:[a]
-> y:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x]);
                                          listElts([y])]))}merge (forall a.
(GHC.Classes.Ord a) =>
x1:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([x1])])),
               (listElts([VV]) = listElts([x1])),
               (listElts([x1]) = Set_cup([listElts([x1]); listElts([VV])]))}mergeSort {VV : [a] | (VV = ys),
            (VV = ys),
            (len([VV]) = len([ys])),
            (listElts([VV]) = Set_cup([listElts([ys]); listElts([ys])])),
            (listElts([VV]) = listElts([ys])),
            (listElts([ys]) = Set_cup([listElts([ys]); listElts([VV])])),
            (len([VV]) >= 0)}ys) (forall a.
(GHC.Classes.Ord a) =>
x1:[a]
-> {VV : [a] | (listElts([VV]) = Set_cup([listElts([x1]);
                                          listElts([x1])])),
               (listElts([VV]) = listElts([x1])),
               (listElts([x1]) = Set_cup([listElts([x1]); listElts([VV])]))}mergeSort {VV : [a] | (VV = zs),
            (VV = zs),
            (len([VV]) = len([zs])),
            (listElts([VV]) = Set_cup([listElts([zs]); listElts([zs])])),
            (listElts([VV]) = listElts([zs])),
            (listElts([zs]) = Set_cup([listElts([zs]); listElts([VV])])),
            (len([VV]) >= 0)}zs) 
370:   where 
371:     ({VV : [a] | (VV = ys),
            (len([VV]) = len([ys])),
            (listElts([VV]) = Set_cup([listElts([ys]); listElts([ys])])),
            (listElts([VV]) = listElts([ys])),
            (listElts([ys]) = Set_cup([listElts([ys]); listElts([VV])])),
            (len([VV]) >= 0)}ys, {VV : [a] | (VV = zs),
            (len([VV]) = len([zs])),
            (listElts([VV]) = Set_cup([listElts([zs]); listElts([zs])])),
            (listElts([VV]) = listElts([zs])),
            (listElts([zs]) = Set_cup([listElts([zs]); listElts([VV])])),
            (len([VV]) >= 0)}zs)  = xs:[a]
-> ([a] , [a])<\ys VV -> (listElts([xs]) = Set_cup([listElts([ys]);
                                                    listElts([VV])]))>split {VV : [a] | (len([VV]) >= 0)}xs

The type given to mergeSortguarantees that the set of elements in the output list is indeed the same as in the input list. Of course, it says nothing about whether the list is actually sorted.

Well, Rome wasn’t built in a day…