Dependent Verification of Functional Programs

Jean-Baptiste Tristan & K. Rustan M. Leino

Functional code with pre/post conditions

So far, our code and proofs were largely independent from each other
On the one hand, we write our code
On the other hand, we prove properties by writing proof scripts in lemmas
It is possible to directly annotate a function with properties
Preconditions: properties we expect to hold when the function is called
Postconditions: properties we expect to hold when the function returns

Postconditions – 1

A postcondition is a property we expect the function to have

It is declared using the ensures keyword, as with lemmas

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

This defines the function and a postcondition
Of course, Dafny needs to prove the postcondition
When the function is called, the postcondition is implicitly added to Dafny's knowledge base (KB)
How should we understand the body? Is it code? Is it a proof?

Postconditions – 2

In a sense, it is both
To be more precise, it really is code, but the verifier knows how to turn code into proofs
You can also interpret it as such by ignoring the values

The recursive call to Append defines the function, but also serves as an induction hypothesis

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

Postconditions – 3

What if the code isn't a good enough proof?

  function Append<T>(l1: List, l2: List): List
    ensures Length(Append(l1, l2)) == Length(l1) + Length(l2)
    ensures forall n: nat :: n % 2 == 0 ==> exists m: nat :: n == 2 * m

Postconditions – 4

What if the code isn't a good enough proof?
Answer 1: make the postcondition a lemma

When the lemma is called, Dafny's KB is extended

  lemma SomeProperty()
    ensures forall n: nat :: n % 2 == 0 ==> exists m: nat :: n == 2 * m

  function Append<T>(l1: List, l2: List): List
    ensures Length(Append(l1, l2)) == Length(l1) + Length(l2)
    ensures forall n: nat :: n % 2 == 0 ==> exists m: nat :: n == 2 * m
  {
    SomeProperty();
    match l1
    case Nil => l2
    case Cons(e, l) => Cons(e, Append(l, l2))
  }

So far, the body of function had to be an expression, but it turns out we are also allowed to call lemmas from the proof language

Postconditions – 5

What if the code isn't a good enough proof?
Answer 2: inline proof scripts in the code

Syntactically, proof script must precede value

  function Append<T>(l1: List, l2: List): List
    ensures Length(Append(l1, l2)) == Length(l1) + Length(l2)
    ensures forall n: nat :: n % 2 == 0 ==> exists m: nat :: n == 2 * m
  {
    assert forall n: nat :: n % 2 == 0 ==> exists m: nat :: n == 2 * m by {
      forall n: nat
        ensures n % 2 == 0 ==> exists m: nat :: n == 2 * m
      {
        if n % 2 == 0 {
          assert n == 2 * (n/2);
        }
      }
    }
    match l1
    case Nil => l2
    case Cons(e, l) => Cons(e, Append(l, l2))
  }

Another example – 6

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

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

Lemmas vs postconditions – 7

Should a property be declared (“intrinsically”) as a postcondition or (“extrinsically”) a lemma?
The benefit of a postcondition is that it is automatically included in the KB: more automation
However, some properties are really extrinsic
- Example: associativity
Quantification would have a high cost on verification
- In general: having a quantified postcondition is likely to be a problem

But you can't even do it because of termination

  function Append<T(!new)>(l1: List, l2: List): List
    ensures Length(Append(l1, l2)) == Length(l1) + Length(l2)
    // ensures forall l3: List :: Append(Append(l1, l2), l3) == Append(l1, Append(l2, l3))

Preconditions – 8

A precondition is a property we require to be true when the function is called

It is declared using the requires keyword, as with lemmas

  function At<T>(l: List, index: nat): T
    requires index < Length(l)
  {
    if index == 0 then l.head else At(l.tail, index - 1)
  }

This defines the function and a precondition
To call the function, Dafny must prove precondition
The precondition is added to Dafny's KB within the function

Preconditions – 9

A function with a precondition is a partial function
In contrast, a function without precondition is total
Partial and Total functions do not have the same type
A total function from type A to B is of type A -> B
A partial function from type A to B is of type A --> B

Preconditions – 10

Preconditions can make your code simpler and faster

No need to waste time on testing for input values that you know cannot happen

  lemma AtProp<T(!new)>(l: List, idx: nat)
    requires idx < Length(l)
    ensures exists v: T :: At(l, idx) == v
  {
  }

But for every call, Dafny must prove the preconditions
If it cannot, you might need to add to the KB of the caller

Preconditions and higher-order functions

If a function argument is partial, you may need to use its requires clause

  function Hof<U, V>(f: U --> V, a: U): V
    requires f.requires(a)
  {
    f(a)
  }

Requires function

The .requires member is Boolean-valued total ghost function

  function Hof<U, V>(f: U --> V, a: U): V
    requires f.requires(a)
  {
    f(a)
  }

Should you mix code and proof? – 1

When should you use a precondition?
- If you would have thrown an exception anyway
- If it makes the code simpler, faster
When should you use a postcondition?
- If essentially every caller will want it
- If it represents an invariant
- If it can be expressed without quantifiers
- If it correspond to important preconditions
- If postcondition verifies without proof

Should you mix code and proof? – 2

Pre/post conditions come at a cost
To call a function, you must establish preconditions
- Might require some convincing
- More facts in Dafny's knowledge base
A function call establishes postconditions
- More facts in Dafny's knowledge base
Remember: it is paramount to keep KB under control

Should you mix code and proof? – 3

Don't be dogmatic
If you never use pre/post conditions
- Your code might be slower than necessary
- Your code might be more complicated that necessary
If you try to always use pre/post conditions
- The verification might be less stable
- The verification might get in the way of the code
Advice: only use pre/post conditions when there is a clear payoff
Dafny's strength is that it supports both well, so make the most of it!

Subset types – 1

You can attach a predicate to a value
Allows you not to constantly require and ensure basic properties
The predicate must be proved for any expression of that type
```
  type MyNat = n: int | 0 <= n
```
MyNat is called a subset type, because its values form of subset of its base type, int

Subset types – 2

Dafny provides a way to guarantee that a subset type is not empty
It is done using a witness clause
In the witness clause, you must provide an example of a value that satisfies the predicate
```
  type MyNat = n: int | 0 <= n witness 4
```

Subset types – tip

Always type variables whose values might contain a subset type

For example, if x and y are meant to be natural numbers

  method m(z: nat) {
    var x := z + 3; // No
    var y: nat := z + 3; // Yes
  }

Not so important for nat, but is often a good idea for more complicated subset types

Subset types – example

  ghost predicate Associative<T(!new)>(BinOp: (T, T) -> T) {
    forall x: T, y: T, z: T :: BinOp(BinOp(x, y), z) == BinOp(x, BinOp(y, z))
  }

  ghost predicate Identity<T(!new)>(BinOp: (T, T) -> T, elt: T) {
    forall x: T :: BinOp(x, elt) == x
  }

  ghost predicate Inverse<T(!new)>(BinOp: (T, T) -> T, elt: T) {
    forall x: T :: exists y: T :: BinOp(x, y) == elt && BinOp(y, x) == elt 
  }

  type Group<!T(!new)> = S: ((T, T) -> T, T) | 
      && Associative(S.0) 
      && Identity(S.0, S.1)  
      && Inverse(S.0, S.1)
      witness *

Ignore the ! and !new for now