# The Great Theorem Prover Challenge I

I was having a discussion with a coworker over lunch the other day about code reasoning and informal correctness (things like “it feels correct” and “it passes a very extensive array of tests”). At some point, the conversation strayed to the relative merits of imperative vs functional paradigms, and which one “feels” easier, as it always does. As a fairly loud proponent of functional-styled programming, I, of course, made the standard arguments about the heap and global state, etc, and was rebuffed by “the overhead of juggling abstractions”.

Now, I won’t get into why I think the response is bullshit (tl;dr if you have to “juggle” an abstraction, it’s not really a very good abstraction), but it did leave me somewhat at a loss as to how we were defining “feeling” easy. It’s a very fuzzy, subjective term, and not really one I’m prepared to go into at any depth.

This brings us to the subject of formal verification. One argument for powerful
and expressive static typesystems is to give strong compile-time guarantees,
which can aid in correctness. For example, in Python, if we create a function
that operates primarily on integers, it may not work correctly or even just
blow up if given, say, a string. This introduces a vector for bugs if we don’t
properly check the return type of some other function, and can cause crashes or
(worse) subtly wrong behavior. However, with a static typesystem, we can *know*
that the function is never called on anything but a number – because otherwise
the function wouldn’t typecheck, and the code wouldn’t compile at all!

Formal verification is taking this idea to its logical conclusion – what if we
encode *all* correctness properties inherent to the code in some way that can
be checked alongisde the code at compile time? Well, the first thing you’ll
find is that you start running into Rice’s Theorem (or more generally, the
halting problem), but you also find that there are a surprising number of
things that can be done and ways to do them.

A few months ago, I found Hillel Wayne’s Great Theorem Prover Showdown on reddit, and found the included discussion quite interesting. After that argument with my friend, I decided that I’d also bite the bullet and try it for myself.

“After all,” I thought, “it’s *functional programming*. We do proofs like that
for the entire semester in 15-150; how hard can it be to write an equivalent in
a theorem proving language?”

Now, before I go any further, let me outline my previous personal experience with formal verification:

- A brief section of a static analysis course at university discussing loop invariants and pre-/post-condition analysis (contracts)
- An even briefer single lesson about refinement types, given by some friends in the CMU PL community
- Hillel Wayne’s blog post

Note that none of the above even involved *touching* a theorem prover (the
closest I had gotten was brute-forcing some logic problems using the Z3
Haskell bindings). Not that I’m about to let that stop me. So let’s dive into
`Leftpad`

, the first challenge. I chose to approach this with Liquid Haskell because it seemed to be the
simpler of the two (Idris being the other option) to just pick up and get
running.

# The Challenge

*You can follow my progress in this repository.*

Our goal is to replicate the classic `leftPad`

function that pads a string to a
desired length.

The first thing we need to do is write the code itself. Most people attempting
this challenge did some variant on a `replicate`

solution, but I opted for a
more naturally-recursive version (this ended up being a good decision).

```
leftPad :: Int -> a -> [a] -> [a]
leftPad n x xs = leftPad' k x xs
where k = max 0 (n - size xs)
leftPad' 0 _ xs = xs
leftPad' n x xs = x : leftPad' (n-1) x xs
```

Now, let’s get onto actually proving this “correct”. Everyone with a hat in this game (including me!) will talk your ears off about how “correctness” doesn’t really mean anything without a “specification” to guide it. In this case, we’ve been helpfully provided an informal spec, but not really anything by way of a formalized contract to follow. That’s fine, part of our job is to turn informal specs into formal ones.

The specification for LeftPad, as given is:

Takes a padding character, a string, and a total length, returns the string padded to that length with that character. If length is less than the length of the string, does nothing.

Ooookay. That’s a little vague. Breaking it down, we start by looking at the inputs – “given a padding character, a string, and a total length”. This gives us our input types:

## A First Try

```
{[email protected] leftPad :: Int -> a -> [a] -> [a]
@-}
```

It’s a start, but it’s not particularly useful. To really leverage the power of LH, we need to actually use our types to prove something! The point of leftPad is to ensure that a string is the correct length, so let’s try to prove that:

```
{[email protected] reflect leftPad @-}
{[email protected] leftPad :: n:Int -> x:a -> xs:[a] ->
result:{ [a] |
size result = max n (size xs)
}
@-}
```

What this means is that the result of leftPad will be of length `n`

or the same
length of the original string, whichever is larger. We also `reflect`

our
function, so it becomes a proper term in the logic.

According to some people, this is enough. The function is “obviously” correct. Let’s test that assumption – does Liquid Haskell think that we’re done?

```
Error: Liquid Type Mismatch
33 | leftPad n x xs = leftPad' k x xs
^^^^^^^^^^^^^^^
Inferred type
VV : {v : [a] | [SNIPPED: big mess] }
not a subtype of Required type
VV : {VV : [a] | Main.size VV == Main.max n (Main.size xs)}
In Context
xs : {v : [a] | Main.size v >= 0 && len v >= 0}
n : {n : Int | n >= 0}
x : a
Error: Liquid Type Mismatch
44 | leftPad' n x xs = x : leftPad' (n-1) x xs
^^^
Inferred type
VV : {v : Int | v == ?b - (1 : int)}
not a subtype of Required type
VV : {VV : Int | VV < ?b && VV >= 0}
In Context
?b : Int
```

(if you just tried this for yourself, you may need to also define `size`

and
`max`

and reflect them into the logic)

Okay, there are two errors here. The first is that big mess of types on the
function we actuallly annotated. I’ll get there in a bit. The *second* error,
however, seems to be saying that our types are wrong for `leftPad'`

as well!
What gives?

It turns out that LH is actually smart enough to recognize that the function
won’t terminate if given an input `n < 0`

. Because we like our programs to be
decidable, this lets LH decide that the type of the first argument to
`leftPad'`

should be positive, as seen by the `VV >= 0`

. In fact, a similar
argument can be used to show an *upper* bound as well! Notice that our only
base case is `n = 0`

. This means that, in order to make progress, we should
have `n`

decrease every time – thus `VV < ?b`

. This seems like a less hard
rule than the previous, but I’m not really familiar enough to say what would
happen if we had multiple axes (or even just a nonstandard termination
condition). However, we have no conditions on the *original* input, and there’s
nothing stopping us from just passing in a negative `n`

. Thus the type
mismatch.

The crux of the issue is that LH can’t (or won’t try to) understand what
`leftPad'`

is doing, or what theorems it upholds. We can fix that by adding
some manual annotations of our own:

```
{[email protected] reflect leftPad' @-}
{[email protected] leftPad' :: n:Nat -> x:a -> xs:[a] ->
result:{[a] |
size result = n + size xs
}
@-}
```

The only new thing is `Nat`

, which means `n:{Int | n >= 0}`

^{1}.

We run it through `liquid`

and… it’s safe! Wait, what?

This blew my mind the first time I saw this. The only effort really expended by
me was to *tell Liquid Haskell what my functions should do*, and it was able to
tell me with no^{2} other information!

The key here is induction, the idea that properties hold over certain operations. If that seems a little abstract, let’s walk it through.

First, let’s make sure that the function is even well-formed. We have

```
leftPad n x xs = leftPad' k x xs
where k = max 0 (n - size xs)
```

`max`

probably has a type like `x:Int -> y:Int -> r:{Int | r >= x && r >= y}`

^{3}. This means that `max 0 i`

is a subtype of `r:{Int | r >= 0}`

automatically… which means that `k`

must have type `Nat`

, and is thus a valid
input to `leftPad'`

! `x`

and `xs`

have no special conditions, so those just
pass through.

Onto `leftPad'`

. We know that, given valid inputs, our result must satisfy
the type `r:{[a] | size r = n + size xs}`

. For our base case, we find that

```
leftPad' 0 x xs = xs
```

so `r = xs`

in this case. We also have `n = 0`

, so we want to show that

```
size xs = 0 + size xs
```

which is a no-brainer.

Next, our inductive step.

```
leftPad' n x xs = x : leftPad' (n-1) x xs
```

For this to be well-typed, we need to know a few things, namely that
`n-1`

is a `Nat`

, or that `n-1 >= 0`

. Luckily, we already know that `n >= 0`

because we’re given `n:Nat`

as a precondition. But wait, we also know that
`n != 0`

, because we pattern matched on it earlier! Thus, `n > 0`

for sure,
so `n - 1 >= 0`

is fine.

Next, we can use our “inductive hypothesis” – we can assume that an recursive
uses of `leftPad'`

are well-typed. That means, in this case, that we know that
`leftPad' (n-1) x xs`

returns something of type ```
r:{[a] | size r = n-1 + size
xs}
```

. We want to exhibit a term of type `r:{[a] | size r = n + size xs}`

. Well,
by the definition of `size`

, `x:l`

has type `r:{[a] | size r = 1 + size l}`

,
so our returned expression `x : leftPad' (n-1) x xs`

should have type
`r:{[a] | size r = 1 + size (leftPad' (n-1) x xs) }`

… which is
`r:{[a] | size r = 1 + (n-1) + size xs}`

, or *exactly what we wanted*.

All of this reasoning, by the way, was decided by LH with no prompting from me. The only thing I did was provide the code and the types, the typechecking happened automagically. The phrase “obviously correct” has a bit more weight after that.

## Not so Obvious

You may notice that we haven’t actually fulfilled the spec given by Hillel. For
example, a function that took a random `n`

elements from the input would also
fulfill the spec we’ve given so far. We need to also encode that the original
string is *padded* with the pad character. The way this is formalized is as
follows:

Given a list

`xs`

, fill element`x`

and a length`n`

, for any index`i`

,

- If
`i < n - size xs`

, the list element should be`x`

.- Otherwise, the list element should be the corresponding element of
`xs`

We can represent this in Haskell by introducing a separate predicate as follows:

```
{[email protected] reflect leftPadElt @-}
{[email protected] leftPadElt :: n:Int -> x:a -> xs:[a] -> i:{Nat | i < n} -> a @-}
leftPadElt :: Int -> a -> [a] -> Int -> a
leftPad Elt n x xs i
| i < k = x
| otherwise = x !! (i-k)
where k = max 0 (n - size xs)
```

Because LH doesn’t have “forall” quantification (this leads to a nasty thing called “the halting problem”), we can’t really encode something like

“For all `i`

from `0 to n`

, `leftPad n x xs !! i == leftPadElt n x xs i`

”

into the type of `leftPad`

itself. Instead, we need to show this by
demonstrating a term of type

```
n:Int -> x:a -> xs:[a] -> i:{Nat | i < n} ->
{leftPad n x xs !! i == leftPadElt n x xs i}
```

So, how do we do that? Well, any proof with no actually associated “data” (like
the list elements) can be seen as having a refinement on the type `()`

, a term
that fulfills all the conditions we need. If that’s a little hard to follow,
don’t worry – it will (hopefully!) make more sense in a moment.

There are two parts to the elements definition, one for the first `k`

elements
and one for the last `size xs`

elements, so it makes sense to split our “proof”
into two parts. Let’s take a look at the first part.

```
{[email protected] thmLeftPadA :: n:Nat -> x:a -> xs:[a] -> i:{Nat | i < n} ->
{ leftPad' n x xs !! i == x }
@-}
```

Notice that I’m using `leftPad'`

here instead of `leftPad`

. That’s because
we’ve already shown (defined) `leftPad`

to be a special case of `leftPad'`

, so
it makes sense to prove something about the easier function to reason about.

So what would a term like this look like? Well, we can start with something
simple: by definition, `leftPad' n x xs = x:[something]`

^{4}. But wait, that
means `leftPad' n x xs !! 0 == x`

always… so the result of
`thmLeftPadA n xs 0`

*already* has the right type.

```
thmLeftPadA :: Int -> a -> [a] -> Int -> ()
thmLeftPadA n x xs 0 = ()
```

What about the other case? Same as any other proof by induction!

```
thmLeftPadA :: Int -> a -> [a] -> Int -> ()
thmLeftPadA n x xs 0 = ()
thmLeftPadA n x xs i = thmLeftPadA (n-1) x xs (i-1)
```

By the same reasoning as before, we know that `i > 0`

. We actually know `n > 0`

as well, because the type `i:{Nat | i < 0}`

is uninhabited. Thus the recursive
call to `thmLeftPadA`

is well-founded. This gives us a term of type
`{leftPad' (n-1) x xs !! (i-1) == x}`

. Again by definition, `leftPad' n x xs`

is equal to `x:leftPad' (n-1) x xs`

and `(x:xs) !! i`

is `xs !! i-1`

, which
means that this is, in fact, equivalent to a term of the type we want!

The second part looks like this (the derivation is left to the reader):

```
{[email protected] thmLeftPadB ::
n:Nat -> x:a -> xs:[a] ->
i:{Nat | i >= n && i < n + size xs} ->
{ leftPad' n x xs !! i == xs !! (i-n) }
@-}
thmLeftPadB :: Int -> a -> [a] -> Int -> ()
thmLeftPadB 0 x xs i = ()
thmLeftPadB n x xs i = thmLeftPadB (n-1) x xs (i-1)
```

All that’s left is to string these two parts together into our final proof:

```
{[email protected] thmLeftPad :: n:Int -> x:a -> xs:[a] -> i:{Nat | i < n} ->
{ leftPad n x xs !! i == leftPadElt n x xs i }
@-}
thmLeftPad :: Int -> a -> [a] -> Int -> ()
thmLeftPad n x xs i
| i < k = thmLeftPadA k x xs i
| otherwise = thmLeftPadB k x xs i
where k = max 0 (n - size xs)
```

And there you have it! We have a *formally verified* leftPad.

## Leave a Comment