Independent Verification of Functional Programs

Jean-Baptiste Tristan & K. Rustan M. Leino

Verification of functional programs

We start our program verification journey with functional programming
The rules to reason about functional programs are simple, and the difficulty of verification essentially amounts to the complexity of what you are trying to prove
Functional programming should be your default programming style

Verification of functional code – specification

How do we verify functional code?
That is, how do we tell Dafny: “I want to prove that my function has this property”?
Recall that function calls are functional expressions, and as such, they are valid logical expressions

Therefore, a lemma's formula can state properties on a function

  function Increment(n: int): int {
    n + 1
  }

  lemma IncrementLarger()
    ensures forall n: int :: Increment(n) > n

  lemma InrementEvenIsOdd()
    ensures forall n: int :: n % 2 == 0 ==> Increment(n) % 2 == 1

Verifying functional code – proof

What about proofs? It is essentially like verifying mathematics
First, note that much of the language of formulas is shared with functional programming, and so reasoning about function programs is similar to reasoning about formulas
If the code uses a conditional expression, then the proof can use a conditional statement
If the code uses a match expression, then the proof can use a match statement
In simple cases, the proof follows the structure of the code

Conditional

  function Abs(x: int): int {
    if x < 0 then -x else x
  }

  lemma AbsPositive(x: int)
    ensures Abs(x) >= 0
  {
    if x < 0 {
      assert -x > 0;
    } else {
      assert x >= 0;
    }
  }

(Note the syntactic difference between the if-then-else expression and the if statement)

Pattern matching

  datatype Size =
    | Small
    | Large

  function Ounces(s: Size): int {
    match s
    case Small => 4
    case Large => 8
  }

  lemma OuncesMultiple4(s: Size)
    ensures exists n: int :: Ounces(s) == 4 * n
  {
    match s
    case Small =>
      assert Ounces(s) == 4 * 1;
    case Large =>
      assert Ounces(s) == 4 * 2;
  }

Example 1

  function Increment(n: int): int {
    n + 1
  }

  lemma IncrementLarger()
    ensures forall n: int :: Increment(n) > n
  {}

  lemma InrementEvenIsOdd()
    ensures forall n: int :: n % 2 == 0 ==> Increment(n) % 2 == 1
  {
    forall n: int
      ensures n % 2 == 0 ==> Increment(n) % 2 == 1
    {
      if n % 2 == 0 {
        assert Increment(n) == n + 1;
      }
    }
  }

Note that Dafny knows that Increment(n) == n + 1
Dafny can always use the definition of a function to reason about it

Warning: controlling dafny's knowledge

You may not want Dafny to use the definition of the function on its own

You can declare it opaque

  opaque function Increment(n: int): int {
    n + 1
  }

  lemma IncrementLarger()
    ensures forall n: int :: Increment(n) > n
  {
    reveal Increment();
  }

  lemma InrementEvenIsOdd()
    ensures forall n: int :: n % 2 == 0 ==> Increment(n) % 2 == 1
  {
    reveal Increment();
    forall n: int
      ensures n % 2 == 0 ==> Increment(n) % 2 == 1
    {
      if n % 2 == 0 {
      }
    }
  }

Recall

  datatype List<T> =
    | Nil
    | Cons(head: T, tail: List)

  function Length<T>(l: List): nat {
    if l.Nil? then 0 else 1 + Length(l.tail)
  }

  function Append<T>(l1: List, l2: List): List {
    match l1
    case Nil => l2
    case Cons(e, l) => Cons(e, Append(l, l2))
  }

Recursive programs? inductive proofs!

What about recursive functions?
Typically, a proof will be by induction, thereby calling the lemma being proved with “smaller” arguments
Every algebraic datatype induces an induction principle defined on the structure of its definition
This is called structural induction

  lemma AppendAssoc<T>(l1: List, l2: List, l3: List)
    ensures Append(Append(l1, l2), l3) == Append(l1, Append(l2, l3))
  {
    match l1
    case Nil =>
    case Cons(e, l) =>
      AppendAssoc(l, l2, l3); // this makes the proof clear to a human, but this line is not needed to convince Dafny
  }

Structural induction: take 1

For natural numbers, the induction principle to prove $P(n)$ for all $n$ is
- Prove $$P(0)$$
- Assume $$P(n)$$ , prove $$P(n+1)$$
For lists, the induction principle to prove $P(l)$ for all $l$ is:
- Prove $$P(Nil)$$
- Assume $$P(l)$$ , prove $\forall e \cdot P(Cons(e, l))$

Structural induction: take 2

Dafny actually uses much stronger induction principles
For natural numbers, the induction principle to prove $P(n)$ for all $n$ is
- Prove $$P(0)$$
- Assume $$P(m)$$ for all $m \leq n$ , prove $$P(n+1)$$
For lists, the induction principle to prove $P(l)$ for all $l$ is:
- Prove $$P(Nil)$$
- Assume $$P(i)$$ for every prefix $$i$$ of $$l$$ , prove $\forall e \cdot P(Cons(e, l))$

Structural induction: take 3

In fact, it is even more powerful than this
The induction principle is defined over all the arguments of the lemma
Ties are broken by considering the arguments in order
In the same way that ties are broken to order words in a dictionary: the lexicographic order

Example proof by induction – 1

Note that Dafny doesn't even need that much convincing and can do some proofs by induction all on its own
But that's not always the case

  lemma AppendAssoc<T>(l1: List, l2: List, l3: List)
    ensures Append(Append(l1, l2), l3) == Append(l1, Append(l2, l3))
  {
    match l1
    case Nil =>
    case Cons(e, l) =>
      AppendAssoc(l, l2, l3); // this makes the proof clear to a human, but this line is not needed to convince Dafny
  }

Example proof by induction – 2

  lemma AppendLength<T>(l1: List, l2: List)
    ensures Length(Append(l1, l2)) == Length(l1) + Length(l2)
  {
    match l1
    case Nil =>
    case Cons(e, l) =>
      AppendLength(l, l2); // Dafny doesn't actually need this line
  }

Generalization – 1

If you're going to remember only one slide, it should be this one
Sometimes, a proposition cannot be proved as is
Instead, you need to prove a more general result
In such cases, Dafny is hopeless, and you need to discover the generalized proposition
This can be genuinely difficult
You need to learn to recognize when you're not making progress because you are in need of generalization

Generalization – 2

Consider an alternative, tail-recursive, definition of the length function

  function LengthTr'<T>(l: List, acc: nat): nat {
    match l
    case Nil => acc
    case Cons(_, tail) => LengthTr'(tail, 1 + acc)
  }

  function LengthTr<T>(l: List): nat {
    LengthTr'(l, 0)
  }

First, note how the code had to be restructured
Indeed, we had to define a more general function
The Length function is just a special case
(As a side note, Dafny implements auto-accumulator tail recursion, so even the original definition of Length is compiled into a loop. But that's not the point of this example.)

Generalization – 3

We would like to prove the following property
It seems obvious
Clearly, this should be proved by induction on l

  lemma LengthSame<T>(l: List)
    ensures Length(l) == LengthTr(l)

Step 1: Prove that $Length(Nil) = LengthTr(Nil)$
- Easy: $$LengthTr(Nil) = LengthTr'(Nil,0) = 0 = Length(Nil)$$
Step 2: Assume that $Length(l) = LengthTr(l)$, prove $\forall e \cdot Length(Cons(e,l)) = LengthTr(Cons(e,l))$
- $$LengthTr(Cons(e,l)) = LengthTr'(Cons(e,l),0)$$
- Ouch: the induction hypothesis mentions $$Length(l) = LengthTr(l) = LengthTr'(l,0)$$
- But we are trying to say something about $$LengthTr'(Cons(e,l),0) = LengthTr'(l,1)$$
- Game over

Generalization – 4

It's not that the proposition is false
- It's just that this proof attempt that is naive
Note how $LengthTr'$ is more general than what we use it for
- Huge red flag
- The proof needs to follow that structure and be more general
We need to think about the relationship between $$Length$$ and $$LengthTr'$$
In general, we expect $$LengthTr'(l,acc)$$ to have the same value as $$LengthTr$$ except that it starts from $$acc$$ , not $$0$$
And our lemma is a special case for $$acc = 0$$

  lemma LengthSame'<T>(l: List, acc: nat)
    ensures acc + Length(l) == LengthTr'(l, acc)
  {
    match l
    case Nil =>
    case Cons(_, tail) =>
      LengthSame'(tail, acc + 1);
  }

Generalization – 5

It is crucial to understand this example
For LengthTr, it is easy, because the code hinted at the need for generalization
That's not always the case
You might face this problem when proving something by induction
If something seems like it is obvious and yet the induction hypothesis doesn't seem to help you out, step back, you might need to prove something more general

Mathematical functions

Conclusion: the logic side of Dafny allows us to reason about functional programs
It goes both ways: the programming side can help us define mathematical functions
So far, when doing mathematics, we have just posited the existence of functions and attached properties to them

  ghost function Increment(n: int): int

  lemma EssenceOfIncrement(n: int)
    ensures Increment(n) == n + 1

Defining mathematical functions

Instead we can give Increment a definition as a functional program
A non-ghost function can be used in place of a ghost one

  ghost function Increment(n: int): int {
    n + 1
  }

More consistent

A significant advantage of defining a function rather than positing its existence is that you are less likely to make a mistake by positing the existence of a function that doesn't actually exists
But you have to prove that your function terminates
To that end, you can declare a decreases clause followed by an expression that tells Dafny what should be decreasing at every iteration
Otherwise, a (programming) function may not be a valid logical function

Termination – easy case

In most cases, the underlying order is obvious and Dafny can infer it

  function Sum(n: int): int
    decreases n // this line can be omitted, because Dafny will infer it
  {
    if n <= 0 then 0 else Sum(n - 1)
  }

If Dafny infers the decreases clause, hover text in the IDE will tell you what it is

Termination – harder case

If not, you can supply a hint using a decreases clause

  function SumUpTo(counter: int, upTo: int): int
    decreases upTo - counter // here, the decreases clause is needed; Dafny will not infer it
  {
    if upTo <= counter then
      counter
    else
      counter + SumUpTo(counter + 1, upTo)
  }

Ghost

But then, why do we need ghost at all?
First, the ghost keyword guarantees that your function will not end up being used by the code
- If a function is really just meant to be used as part of the verification, declaring it ghost ensures it will not end up in your executable
Second, while all terminating functions that can be defined using functional programming exist, there exist functions that cannot be defined algorithmically
- And yet, they are useful for practical program verification…
```
  predicate P<T>(m: T, n: T)

  ghost predicate Prop<T(!new)>(m: T) {
    exists n: T :: P(m, n)
  }
```