**1.**Introduction {#intro}**1.1.**Well-Typed Programs Do Go Wrong {#gowrong}**1.2.**Refinement Types**1.3.**Audience**1.4.**Getting Started**2.**Logic & SMT**2.1.**Syntax**2.2.**Semantics {#semantics}**2.3.**Verification Conditions**2.4.**Examples: Propositions**2.5.**Examples: Arithmetic**2.6.**Examples: Uninterpreted Function**2.7.**Recap**3.**Refinement Types**3.1.**Defining Types {#definetype}**3.2.**Errors**3.3.**Subtyping**3.4.**Writing Specifications**3.5.**Refining Function Types: Pre-conditions**3.6.**Refining Function Types: Post-conditions**3.7.**Testing Values: Booleans and Propositions {#propositions}**3.8.**Putting It All Together**3.9.**Recap**4.**Polymorphism {#polymorphism}**4.1.**Specification: Vector Bounds {#vectorbounds}**4.2.**Verification: Vector Lookup**4.3.**Inference: Our First Recursive Function**4.4.**Higher-Order Functions: Bottling Recursion in a`loop`

**4.5.**Refinements and Polymorphism {#sparsetype}**4.6.**Recap**5.**Refined Datatypes {#refineddatatypes}**5.1.**Sparse Vectors Revisited {#autosmart}**5.2.**Ordered Lists {#orderedlists}**5.3.**Ordered Trees {#binarysearchtree}**5.4.**Recap**6.**Boolean Measures {#boolmeasures}**6.1.**Partial Functions**6.2.**Lifting Functions to Measures {#usingmeasures}**6.3.**A Safe List API**6.4.**Recap**7.**Numeric Measures {#numericmeasure}**7.1.**Wholemeal Programming**7.2.**Specifying List Dimensions**7.3.**Lists: Size Preserving API**7.4.**Lists: Size Reducing API {#listreducing}**7.5.**Dimension Safe Vector API**7.6.**Dimension Safe Matrix API**7.7.**Recap**8.**Elemental Measures {#setmeasure}**8.1.**Talking about Sets**8.2.**Proving QuickCheck Style Properties {#quickcheck}**8.3.**Content-Aware List API {#listelems}**8.4.**Permutations**8.5.**Uniqueness**8.6.**Unique Zippers**8.7.**Recap**9.**Case Study: Okasaki's Lazy Queues {#lazyqueue}**10.**Case Study: Associative Maps**10.1.**Specifying Maps {#mapapi}**10.2.**Using Maps: Well Scoped Expressions**10.3.**Implementing Maps: Binary Search Trees {#lemmas}**10.4.**Recap**11.**Case Study: Pointers & Bytes {#case-study-pointers}**11.1.**HeartBleeds in Haskell**11.2.**Low-level Pointer API**11.3.**A Refined Pointer API**11.4.**Assumptions vs Guarantees**11.5.**ByteString API**11.6.**Application API**11.7.**Nested ByteStrings**11.8.**Recap: Types Against Overflows**12.**Case Study: AVL Trees {#case-study-avltree}

{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--reflection" @-}
module Tutorial_02_Logic where
{- size :: xs:[a] -> {v:Int | v = size xs} @-}
ax1 :: Int -> Bool
ax2 :: Int -> Bool
ax3 :: Int -> Int -> Bool
ax4 :: Int -> Int -> Bool
ax5 :: Int -> Int -> Int -> Bool
ax6 :: Int -> Int -> Bool
congruence :: (Int -> Int) -> Int -> Int -> Bool
fx1 :: (Int -> Int) -> Int -> Bool
ex1, ex2 :: Bool -> Bool
ex3, ex3', ex4, ex6, ex7, exDeMorgan1, exDeMorgan2 :: Bool -> Bool -> Bool
infixr 9 ==>
{-@ invariant {v:[a] | size v >= 0} @-}
-- {-@ fail ex0' @-}
-- {-@ fail ex3' @-}
-- {-@ fail exDeMorgan2 @-}
-- {-@ fail ax0' @-}
-- {-@ fail ax6 @-}

As we shall see shortly, a refinement type is:

Refinement Types=Types+Logical Predicates

Let us begin by quickly recalling what we mean by “logical
predicates” in the remainder of this tutorial. ^{1} To
this end, we will describe *syntax*, that is, what predicates
*look* like, and *semantics*, which is a fancy word for
what predicates *mean*.

A *logical predicate* is, informally speaking, a Boolean
valued term drawn from a *restricted* subset of Haskell. In
particular, the expressions are drawn from the following grammar
comprising *constants*, *expressions* and
*predicates*.

**A Constant**^{2} `c`

is simply
one of the numeric values:

` c := 0, 1, 2, ...`

**A Variable** `v`

is one of `x`

,
`y`

, `z`

, etc., these will refer to (the values
of) binders in our source programs.

` v := x, y, z, ...`

**An Expression** `e`

is one of the following
forms; that is, an expression is built up as linear arithmetic
expressions over variables and constants and uninterpreted function
applications.

```
e := v -- variable
| c -- constant
| (e + e) -- addition
| (e - e) -- subtraction
| (c * e) -- multiplication by constant
| (v e1 e2 ... en) -- uninterpreted function application
| (if p then e else e) -- if-then-else
```

**Examples of Expressions** include the following:

`x + y - z`

`2 * x`

`1 + size x`

**A Relation** is one of the usual (arithmetic) comparison
operators:

```
r := == -- equality
| /= -- disequality
| >= -- greater than or equal
| <= -- less than or equal
| > -- greater than
| < -- less than
```

**A Predicate** is either an atomic predicate, obtained by
comparing two expressions, or, an application of a predicate function to
a list of arguments, or the Boolean combination of the above predicates
with the operators `&&`

(and), `||`

(or),
`==>`

(implies ^{3}), `<=>`

(if and only if ^{4}), and `not`

.

```
p := (e r e) -- binary relation
| (v e1 e2 ... en) -- predicate (or alias) application
| (p && p) -- and
| (p || p) -- or
| (p => p) | (p ==> p) -- implies
| (p <=> p) -- iff
| (not p) -- negation
| true | True
| false | False
```

**Examples of Predicates** include the following:

`x + y <= 3`

`null x`

`x < 10 ==> y < 10 ==> x + y < 20`

`0 < x + y <=> 0 < y + x`

The syntax of predicates tells us what they *look* like, that
is, what we can *write down* as valid predicates. Next, let us
turn our attention to what a predicate *means*. Intuitively, a
predicate is just a Boolean valued Haskell function with
`&&`

, `||`

, `not`

being the
usual operators and `==>`

and `<=>`

being
two special operators.

**The Implication** operator `==>`

is
equivalent to the following Haskell function. (For now, ignore the
signature: it just says the output is a `Bool`

that is equal
to the *logical* implication between the inputs `p`

and `q`

.)

{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p ==> q)} @-}
False ==> False = True
False ==> True = True
True ==> True = True
True ==> False = False

**The If-and-only-if** operator `<=>`

is
equivalent to the Haskell function:^{5}

{-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p <=> q)} @-}
False <=> False = True
False <=> True = False
True <=> True = True
True <=> False = False

**An Environment** is a mapping from variables to their
Haskell types. For example, let `G`

be an environment defined
as

```
x :: Int
y :: Int
z :: Int
```

which maps each variable `x`

, `y`

and
`z`

to the type `Int`

.

**An Assignment** under an environment, is a mapping from
variables to values of the type specified in the environment. For
example,

```
x := 1
y := 2
z := 3
```

is an assignment under `G`

that maps `x`

,
`y`

and `z`

to the `Int`

values
`1`

, `2`

and `3`

respectively.

**A Predicate Evaluates** to either `True`

or
`False`

under a given assignment. For example, the
predicate

` x + y > 10`

evaluates to `False`

given the above assignment but
evaluates to `True`

under the assignment

```
x := 10
y := 10
z := 20
```

**A Predicate is Satisfiable** in an environment if
*there exists* an assignment (in that environment) that makes the
predicate evaluate to `True`

. For example, in `G`

the predicate

` x + y == z`

is satisfiable, as the above assignment makes the predicate evaluate
to `True`

.

**A Predicate is Valid** in an environment if
*every* assignment in that environment makes the predicate
evaluate to `True`

. For example, the predicate

` x < 10 || x == 10 || x > 10`

is valid under `G`

as no matter what value we assign to
`x`

, the above predicate will evaluate to
`True`

.

LiquidHaskell works without actually *executing* your
programs. Instead, it checks that your program meets the given
specifications in roughly two steps.

First, LH combines the code and types down to a set of

*Verification Conditions*(VC) which are predicates that are valid*only if*your program satisfies a given property.^{6}Next, LH

*queries*an SMT solver to determine whether these VCs are valid. If so, it says your program is*safe*and otherwise it*rejects*your program.

**The SMT Solver decides** whether a predicate (VC) is
valid *without enumerating* and evaluating all assignments.
Indeed, it is impossible to do so as there are usually infinitely many
assignments once the predicates refer to integers or lists and so on.
Instead, the SMT solver uses a variety of sophisticated *symbolic
algorithms* to deduce whether a predicate is valid or not. This
process is the result of decades of work in mathematical logic and
decision procedures; the Ph.D
thesis of Greg Nelson is an excellent place to learn more about
these beautiful algorithms.

**We Restrict the Logic** to ensure that all our VC queries
fall within the *decidable fragment*. This makes LiquidHaskell
extremely automatic – there is *no* explicit manipulation of
proofs, just the specification of properties via types and of course,
the implementation via Haskell code! This automation comes at a price:
all our refinements *must* belong to the logic above.
Fortunately, with a bit of creativity, we can say a *lot* in this
logic. ^{7}

Finally, let’s conclude this quick overview with some examples of predicates, in order to build up our own intuition about logic and validity. Each of the below is a predicate from our refinement logic. However, we write them as raw Haskell expressions that you may be more familiar with right now, and so that we can start to use LiquidHaskell to determine whether a predicate is indeed valid or not.

**Let `TRUE` be a refined type** for `Bool`

valued expressions that *always* evaluate to `True`

.
Similarly, we can define `FALSE`

for `Bool`

valued
expressions that *always* evaluate to `False`

:^{8}

{-@ type TRUE = {v:Bool | v } @-}
{-@ type FALSE = {v:Bool | not v} @-}

Thus, a *valid predicate* is one that has the type
`TRUE`

. The simplest example of a valid predicate is just
`True`

:

{-@ ex0 :: TRUE @-}
ex0 = True

of course, `False`

is *not valid*

{-@ ex0' :: TRUE @-}
ex0' = False

We can get more interesting predicates if we use variables. For
example, the following is valid predicate says that a `Bool`

variable is either `True`

or `False`

.

{-@ ex1 :: Bool -> TRUE @-}
ex1 b = b || not b

Of course, a variable cannot be both `True`

and
`False`

, and so the below predicate is valid:

{-@ ex2 :: Bool -> FALSE @-}
ex2 b = b && not b

The next few examples illustrate the `==>`

operator.
You should read `p ==> q`

as *if* `p`

is
true *then* `q`

must also be true. Thus, the below
predicates are valid as if both `a`

and `b`

are
true, then well, `a`

is true, and `b`

is true.

{-@ ex3 :: Bool -> Bool -> TRUE @-}
ex3 a b = (a && b) ==> a
{-@ ex4 :: Bool -> Bool -> TRUE @-}
ex4 a b = (a && b) ==> b

**Exercise: (Implications and Or): **Of course, if we
replace the `&&`

with `||`

the result is
*not valid*. Can you shuffle the variables around – *without
changing the operators* – to make the formula valid?

{-@ ex3' :: Bool -> Bool -> TRUE @-}
ex3' a b = (a || b) ==> a

The following predicates are valid because they encode modus ponens: if
you know that `a`

implies `b`

and you know that
`a`

is true, then it must be the case that `b`

is
also true:

{-@ ex6 :: Bool -> Bool -> TRUE @-}
ex6 a b = (a && (a ==> b)) ==> b
{-@ ex7 :: Bool -> Bool -> TRUE @-}
ex7 a b = a ==> (a ==> b) ==> b

Recall that `p <=> q`

(read `p`

if and
only if `q`

) evaluates to `True`

exactly when
`p`

and `q`

evaluate to the *same* values
(`True`

or `False`

). It is used to encode
*equalities* between predicates. For example, we can write down
De Morgan’s
laws as the valid predicates:

{-@ exDeMorgan1 :: Bool -> Bool -> TRUE @-}
exDeMorgan1 a b = not (a || b) <=> (not a && not b)

**Exercise: (DeMorgan's Law): **The following version of
DeMorgan’s law is wrong. Can you fix it to get a valid formula?

{-@ exDeMorgan2 :: Bool -> Bool -> TRUE @-}
exDeMorgan2 a b = not (a && b) <=> (not a && not b)

Next, let’s look at some predicates involving arithmetic. The simplest ones don’t have any variables, for example:

{-@ ax0 :: TRUE @-}
ax0 = 1 + 1 == 2

Again, a predicate that evaluates to `False`

is
*not* valid:

{-@ ax0' :: TRUE @-}
ax0' = 1 + 1 == 3

**SMT Solvers determine Validity** *without*
enumerating assignments. For example, consider the predicate:

{-@ ax1 :: Int -> TRUE @-}
ax1 x = x < x + 1

It is trivially valid; as via the usual laws of arithmetic, it is
equivalent to `0 < 1`

which is `True`

independent of the value of `x`

. The SMT solver is able to
determine this validity without enumerating the infinitely many possible
values for `x`

. This kind of validity checking lies at the
heart of LiquidHaskell.

operators, as shown in the following examples:

{-@ ax2 :: Int -> TRUE @-}
ax2 x = (x < 0) ==> (0 <= 0 - x)
{-@ ax3 :: Int -> Int -> TRUE @-}
ax3 x y = (0 <= x) ==> (0 <= y) ==> (0 <= x + y)
{-@ ax4 :: Int -> Int -> TRUE @-}
ax4 x y = (x == y - 1) ==> (x + 2 == y + 1)
{-@ ax5 :: Int -> Int -> Int -> TRUE @-}
ax5 x y z = (x <= 0 && x >= 0)
==> (y == x + z)
==> (y == z)

**Exercise: (Addition and Order): **The formula below is
*not* valid. Do you know why? Change the *hypothesis*
i.e. the thing to the left of the `==>`

to make it a valid
formula.

{-@ ax6 :: Int -> Int -> TRUE @-}
ax6 x y = True ==> (x <= x + y)

We say that function symbols are *uninterpreted* in the
refinement logic, because the SMT solver does not “know” how functions
are defined. Instead, the only thing that the solver knows is the
*axiom of congruence* which states that any function
`f`

, returns equal outputs when invoked on equal inputs.

**We Test the Axiom of Congruence** by checking that the
following predicate is valid:

{-@ congruence :: (Int -> Int) -> Int -> Int -> TRUE @-}
congruence f x y = (x == y) ==> (f x == f y)

Again, remember we are *not evaluating* the code above; indeed
we *cannot* evaluate the code above because we have no definition
of `f`

. Still, the predicate is valid as the congruence axiom
holds for any possible interpretation of `f`

.

Here is a fun example; can you figure out why this predicate is indeed valid? (The SMT solver can…)

{-@ fx1 :: (Int -> Int) -> Int -> TRUE @-}
fx1 f x = (x == f (f (f x)))
==> (x == f (f (f (f (f x)))))
==> (x == f x)

To get a taste of why uninterpreted functions will prove useful,
let’s write a function to compute the `size`

of a list:

{-@ measure size @-}
{-@ size :: [a] -> Nat @-}
size :: [a] -> Int
size [] = 0
size (x:xs) = 1 + size xs

We can now verify that the following predicates are
*valid*:

{-@ fx0 :: [a] -> [a] -> TRUE @-}
fx0 xs ys = (xs == ys) ==> (size xs == size ys)

Note that to determine that the above is valid, the SMT solver does
not need to know the *meaning* or *interpretation* of
`size`

– merely that it is a function. When we need some
information about the definition, of `size`

we will put it
inside the predicate. For example, in order to prove that the following
is valid:

{-@ fx2 :: a -> [a] -> TRUE @-}
fx2 x xs = 0 < size ys
where
ys = x : xs

LiquidHaskell actually asks the SMT solver to prove the validity of a
VC predicate which states that sizes are non-negative and that since
`ys`

equals `x:xs`

, the size of `ys`

is
one more than `xs`

. ^{9}

{-@ fx2VC :: _ -> _ -> _ -> TRUE @-}
fx2VC x xs ys = (0 <= size xs)
==> (size ys == 1 + size xs)
==> (0 < size ys)

This chapter describes exactly what we, for the purposes of this
book, mean by the term *logical predicate*.

- We defined a grammar – a restricted subset of Haskell corresponding
to
`Bool`

valued expressions. - The restricted grammar lets us use SMT solvers to decide whether a
predicate is
*valid*that is, evaluates to`True`

for*all*values of the variables. - Crucially, the SMT solver determines validity
*without enumerating*and evaluating the predicates (which would take forever!) but instead by using clever symbolic algorithms.

Next, let’s see how we can use logical predicates to *specify*
and *verify* properties of real programs.

If you are comfortable with this material, e.g. if you know what the “S”, “M” and “T” stand for in SMT, and what QF-UFLIA stands for (i.e. the quantifier free theory of linear arithmetic and uninterpreted functions), then feel free skip to the next chapter.↩︎

When you see := you should read it as “is defined to be”↩︎

Read

`p ==> q`

as “if`p`

then`q`

”↩︎Read

`p <=> q`

as “if`p`

then`q`

**and**if`q`

then`p`

”↩︎An observant reader may notice that <=> is the same as == if the arguments are of type Bool↩︎

The process is described at length in this paper↩︎

In particular, we will use the uninterpreted functions to create many sophisticated abstractions.↩︎