Refinement Types via SMT and Predicate Abstraction

One of the great things about Haskell is its brainy type system that allows one to enforce a variety of invariants at compile time, thereby nipping a large swathe of run-time errors in the bud. Refinement types allow us to use modern logic solvers (aka SAT and SMT engines) to dramatically extend the scope of invariants that can be statically verified.

## What is a Refinement Type?

In a nutshell,

Refinement Types = Types + Logical Predicates

That is, refinement types allow us to decorate types with logical predicates (think boolean-valued Haskell expressions) which constrain the set of values described by the type, and hence allow us to specify sophisticated invariants of the underlying values.

Say what?

```42: module Intro where
43:
```

Let us jump right in with a simple example, the number `0 :: Int`. As far as Haskell is concerned, the number is simply an `Int` (lets not worry about things like `Num` for the moment). So are `2`, `7`, and `904`. With refinements we can dress up these values so that they stand apart. For example, consider the binder

```54: zero' :: Int
55: {VV : (GHC.Types.Int) | (0 <= VV)}zero' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0
```

We can ascribe to the variable `zero'` the refinement type

```61: {-@ zero' :: {v: Int | 0 <= v} @-}
```

which is simply the basic type `Int` dressed up with a predicate. The binder `v` is called the value variable, and so the above denotes the set of `Int` values which are greater than `0`. Of course, we can attach other predicates to the above value, for example

Note: We will use `@`-marked comments to write refinement type annotations the Haskell source file, making these types, quite literally, machine-checked comments!

```75: {-@ zero'' :: {v: Int | (0 <= v && v < 100) } @-}
76: zero'' :: Int
77: {VV : (GHC.Types.Int) | (VV < 100),(0 <= VV)}zero'' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0
```

which states that the number is in the range `0` to `100`, or

```83: {-@ zero''' :: {v: Int | ((v mod 2) = 0) } @-}
84: zero''' :: Int
85: {VV : (GHC.Types.Int) | ((VV mod 2) = 0)}zero''' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0
```

where `mod` is the modulus operator in the refinement logic. Thus, the type above states that zero is an even number.

We can also use a singleton type that precisely describes the constant

```94: {-@ zero'''' :: {v: Int | v = 0 } @-}
95: zero'''' :: Int
96: {VV : (GHC.Types.Int) | (VV = 0)}zero'''' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0
```

(Aside: we use a different names `zero'`, `zero''` etc. for a silly technical reason – LiquidHaskell requires that we ascribe a single refinement type to a top-level name.)

Finally, we could write a single type that captures all the properties above:

```106: {-@ zero :: {v: Int | ((0 <= v) && ((v mod 2) = 0) && (v < 100)) } @-}
107: zero     :: Int
108: {VV : (GHC.Types.Int) | ((VV mod 2) = 0),(VV < 100),(0 <= VV)}zero     =  x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0
```

The key points are:

1. A refinement type is just a type decorated with logical predicates.
2. A value can have different refinement types that describe different properties.
3. If we erase the green bits (i.e. the logical predicates) we get back exactly the usual Haskell types that we know and love.
4. A vanilla Haskell type, say `Int` has the trivial refinement `true` i.e. is really `{v: Int | true}`.

We have built a refinement type-based verifier called LiquidHaskell. Lets see how we can use refinement types to specify and verify interesting program invariants in LiquidHaskell.

## Writing Safety Specifications

We can use refinement types to write various kinds of more interesting safety specifications.

First, we can write a wrapper around the usual `error` function

```133: {-@ error' :: {v: String | false } -> a  @-}
134: error'     :: String -> a
135: {VV : [(GHC.Types.Char)] | false} -> aerror'     = [(GHC.Types.Char)] -> aerror
```

The interesting thing about the type signature for `error'` is that the input type has the refinement `false`. That is, the function must only be called with `String`s that satisfy the predicate `false`. Of course, there are no such values. Thus, a program containing the above function typechecks exactly when LiquidHaskell can prove that the function `error'` is never called.

Next, we can use refinements to encode arbitrary programmer-specified assertions by defining a function

```149: {-@ lAssert     :: {v:Bool | (Prop v)} -> a -> a  @-}
150: lAssert         :: Bool -> a -> a
151: {VV : (GHC.Types.Bool) | (? Prop([VV]))} -> a -> alAssert True  ax = {VV : a | (VV = x)}x
152: lAssert False _ = {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"lAssert failure"
```

In the refinement, `(Prop v)` denotes the Haskell `Bool` value `v` interpreted as a logical predicate. In other words, the input type for this function specifies that the function must only be called with the value `True`.

## Refining Function Types : Preconditions

Lets use the above to write a divide function that only accepts non-zero denominators.

```168: divide     :: Int -> Int -> Int
169: (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)divide (GHC.Types.Int)n 0 = {VV : [(GHC.Types.Char)] | false} -> {VV : (GHC.Types.Int) | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"divide by zero"
170: divide n d = {VV : (GHC.Types.Int) | (VV = n)}n x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x / y))}`div` {VV : (GHC.Types.Int) | (VV != 0)}d
```

We can specify that the non-zero denominator precondition with a suitable refinement on the input component of the function’s type

```177: {-@ divide :: Int -> {v: Int | v != 0 } -> Int @-}
```

How does LiquidHaskell verify the above function?

The key step is that LiquidHaskell deduces that the expression `"divide by zero"` is not merely of type `String`, but in fact has the the refined type `{v:String | false}` in the context in which the call to `error'` occurs.

LiquidHaskell arrives at this conclusion by using the fact that in the first equation for `divide` the denominator parameter is in fact `0 :: {v: Int | v = 0}` which contradicts the precondition (i.e. input) type.

In other words, LiquidHaskell deduces by contradiction, that the first equation is dead code and hence `error'` will not be called at run-time.

If you are paranoid, you can put in an explicit assertion

```199: divide'     :: Int -> Int -> Int
200: {VV : (GHC.Types.Int) | false}
-> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}divide' {VV : (GHC.Types.Int) | false}n 0 = {VV : [(GHC.Types.Char)] | false} -> {VV : (GHC.Types.Int) | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"divide by zero"
201: divide' n d = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}lAssert ({VV : (GHC.Types.Int) | false}d x:{VV : (GHC.Types.Int) | false}
-> y:{VV : (GHC.Types.Int) | false}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0  :  int))}0) ({VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false})
-> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}\$ {VV : (GHC.Types.Int) | false}n x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x / y))}`div` {VV : (GHC.Types.Int) | false}d
```

and LiquidHaskell will verify the assertion (by verifying the call to `lAssert`) for you.

## Refining Function Types : Postconditions

Next, lets see how we can use refinements to describe the outputs of a function. Consider the following simple absolute value function

```214: abz               :: Int -> Int
215: (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz (GHC.Types.Int)n | {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x < y))}< {VV : (GHC.Types.Int) | (VV = n)}n     = {VV : (GHC.Types.Int) | (VV = n)}n
216:       | otherwise = {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}- {VV : (GHC.Types.Int) | (VV = n)}n
```

We can use a refinement on the output type to specify that the function returns non-negative values

```223: {-@ abz :: Int -> {v: Int | 0 <= v } @-}
```

LiquidHaskell verifies that `abz` indeed enjoys the above type by deducing that `n` is trivially non-negative when `0 < n` and that in the `otherwise` case, i.e. when `not (0 < n)` the value `0 - n` is indeed non-negative (lets not worry about underflows for the moment.) LiquidHaskell is able to automatically make these arithmetic deductions by using an SMT solver which has decision built-in procedures for arithmetic, to reason about the logical refinements.

## Putting It All Together

Lets wrap up this introduction with a simple `truncate` function that connects all the dots.

```244: {-@ truncate :: Int -> Int -> Int @-}
245: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate (GHC.Types.Int)i (GHC.Types.Int)max
246:   | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i
247:   | otherwise  = {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i')
248:     where {VV : (GHC.Types.Int) | (0 <= VV)}i'   = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i
249:           {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max
```

`truncate i n` simply returns `i` if its absolute value is less the upper bound `max`, and otherwise truncates the value at the maximum. LiquidHaskell verifies that the use of `divide` is safe by inferring that at the call site

1. `i' > max'` from the branch condition.
2. `0 <= i'` from the `abz` postcondition (hover mouse over `i'`).
3. `0 <= max'` from the `abz` postcondition (hover mouse over `max'`).

From the above, LiquidHaskell infers that `i' != 0`. That is, at the call site `i' :: {v: Int | v != 0}`, thereby satisfying the precondition for `divide` and verifying that the program has no pesky divide-by-zero errors. Again, if you really want to make sure, put in an assertion

```268: {-@ truncate' :: Int -> Int -> Int @-}
269: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate' (GHC.Types.Int)i (GHC.Types.Int)max
270:   | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i
271:   | otherwise  = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> (GHC.Types.Int) -> (GHC.Types.Int)lAssert ({VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),
(VV >= zero''''),
(0 <= VV),
(VV <= i')}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),
(VV >= zero''''),
(0 <= VV),
(VV <= i')}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0  :  int))}0) ((GHC.Types.Int) -> (GHC.Types.Int))
-> (GHC.Types.Int) -> (GHC.Types.Int)\$ {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i')
272:     where {VV : (GHC.Types.Int) | (0 <= VV)}i'   = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i
273:           {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max
```

and lo! LiquidHaskell will verify it for you.

## Modular Verification

Incidentally, note the `import` statement at the top. Rather than rolling our own `lAssert` we can import and use a pre-defined version `liquidAssert` defined in an external module

```286: {-@ truncate'' :: Int -> Int -> Int @-}
287: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate'' (GHC.Types.Int)i (GHC.Types.Int)max
288:   | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i
289:   | otherwise  = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> (GHC.Types.Int) -> (GHC.Types.Int)liquidAssert ({VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),
(VV >= zero''''),
(0 <= VV),
(VV <= i')}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),
(VV >= zero''''),
(0 <= VV),
(VV <= i')}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0  :  int))}0) ((GHC.Types.Int) -> (GHC.Types.Int))
-> (GHC.Types.Int) -> (GHC.Types.Int)\$ {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i')
290:     where {VV : (GHC.Types.Int) | (0 <= VV)}i'   = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i
291:           {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max
```

In fact, LiquidHaskell comes equipped with suitable refinements for standard functions and it is easy to add refinements as we shall demonstrate in subsequent articles.

## Conclusion

This concludes our quick introduction to Refinement Types and LiquidHaskell. Hopefully you have some sense of how to

1. Specify fine-grained properties of values by decorating their types with logical predicates.
2. Encode assertions, preconditions, and postconditions with suitable function types.
3. Verify semantic properties of code by using automatic logic engines (SMT solvers) to track and establish the key relationships between program values.