Loops & Recursion

In this chapter, we’ll see how various looping constructs work in Pulse, starting with while and also recursive functions.

By default, Pulse’s logic is designed for partial correctness. This means that programs are allowed to loop forever. When we say that program returns v:t satisfying a postcondition p, this should be understood to mean that the program could loop forever, but if it does return, it is guaranteed to return a v:t where the state satisfies p v.

While loops: General form

The form of a while loop is:

while ( guard )
invariant (b:bool). p
{ body }

Where

  • guard is a Pulse program that returns a b:bool

  • body is a Pulse program that returns unit

  • invariant (b:bool). p is an invariant where

    • exists* b. p must be provable before the loop is entered and as a postcondition of body.

    • exists* b. p is the precondition of the guard, and p b is its postcondition, i.e., the guard must satisfy:

      requires exists* b. p
      returns b:bool
      ensures p
      
    • the postcondition of the entire loop is invariant false.

One way to understand the invariant is that it describes program assertions at three different program points.

  • When b==true, the invariant describes the program state at the start of the loop body;

  • when b==false, the invariant describes the state at the end of the loop;

  • when b is undetermined, the invariant describes the property of the program state just before the guard is (re)executed, i.e., at the entry to the loop and at the end of loop body.

Coming up with an invariant to describe a loop often requires some careful thinking. We’ll see many examples in the remaining chapters, starting with some simple loops here.

Countdown

Here’s our first Pulse program with a loop: count_down repeatedly decrements a reference until it reaches 0.

fn count_down (x:ref nat)
requires pts_to x 'v
ensures pts_to x 0
{
    let mut keep_going = true;
    while (
        !keep_going
    )
    invariant b. 
      exists* v.
        pts_to keep_going b **
        pts_to x v **
        pure (b == false ==> v == 0)
    {
        let n = !x;
        if (n = 0) 
        {
            keep_going := false;
        } 
        else
        {
            x := n - 1;
        }
    }
}

While loops in Pulse are perhaps a bit more general than in other languages. The guard is an arbitrary Pulse program, not just a program that reads some local variables. For example, here’s another version of count_down where the guard does all the work and the loop body is empty, and we don’t need an auxiliary keep_going variable.

fn count_down2 (x:ref nat)
requires pts_to x 'v
ensures pts_to x 0
{
    while (
        let n = !x;
        if (n = 0)
        {
            false
        } 
        else
        {
            x := n - 1;
            true
        }
    )
    invariant b. 
      exists* v.
        pts_to x v **
        pure (b == false ==> v == 0)
    { () }
}

Partial correctness

The partial correctness interpretation means that the following infinitely looping variant of our program is also accepted:

fn count_down_loopy (x:ref nat)
requires pts_to x 'v
ensures pts_to x 0
{
    while (
        let n = !x;
        if (n = 0)
        {
            false
        }
        else
        {
            x := n + 1;
            true
        }
    )
    invariant b. 
      exists* v.
        pts_to x v **
        pure (b == false ==> v == 0)
    { () }
}

This program increments instead of decrement x, but it still satisfies the same invariant as before, since it always loops forever.

We do have a fragment of the Pulse logic, notably the logic of ghost and atomic computations that is guaranteed to always terminate. We plan to also support a version of the Pulse logic for general purpose sequential programs (i.e., no concurrency) that is also terminating.

Multiply by repeated addition

Our next program with a loop multiplies two natural numbers x, y by repeatedly adding y to an accumulator x times. This program has a bit of history: A 1949 paper by Alan Turing titled “Checking a Large Routine” is often cited as the first paper about proving the correctness of a computer program. The program that Turing describes is one that implements multiplication by repeated addition.

fn multiply_by_repeated_addition (x y:nat)
    requires emp
    returns z:nat
    ensures pure (z == x * y)
{
    let mut ctr : nat = 0;
    let mut acc : nat = 0;
    while (
        let c = !ctr;
        (c < x)
    )
    invariant b.
    exists* c a.
        pts_to ctr c **
        pts_to acc a **
        pure (c <= x /\
              a == (c * y) /\
              b == (c < x))
    {
        let a = !acc;
        acc := a + y;
        let c = !ctr;
        ctr := c + 1;
    };
    !acc
}

A few noteworthy points:

  • Both the counter ctr and the accumulator acc are declared nat, which implicitly, by refinement typing, provides an invariant that they are both always at least 0. This illustrates how Pulse provides a separation logic on top of F*’s existing dependent type system.

  • The invariant says that the counter never exceeds x; the accumulator is always the product of counter and y; and the loop continues so long as the counter is strictly less than x.

Summing the first N numbers

This next example shows a Pulse program that sums the first n natural numbers. It illustrates how Pulse programs can developed along with pure F* specifications and lemmas.

We start with a specification of sum, a simple recursive function in F* along with a lemma that proves the well-known identity about this sum.

let rec sum (n:nat)
: nat
= if n = 0 then 0 else n + sum (n - 1)

#push-options "--z3rlimit 20"
noextract
let rec sum_lemma (n:nat)
: Lemma (sum n == n * (n + 1) / 2)
= if n = 0 then ()
  else sum_lemma (n - 1)
#pop-options

Now, let’s say we want to implement isum, an iterative version of sum, and prove that it satisfies the identity proven by sum_lemma.

#push-options "--z3cliopt 'smt.arith.nl=false'"
noextract
```pulse
fn isum (n:nat)
requires emp
returns z:nat
ensures pure ((n * (n + 1) / 2) == z)
{
    let mut acc : nat = 0;
    let mut ctr : nat = 0;
    while (
        let c = !ctr;
        (c < n)
    )
    invariant b.
    exists* c a.
        pts_to ctr c **
        pts_to acc a **
        pure (c <= n /\
              a == sum c /\
              b == (c < n))
    {
        let a = !acc;
        let c = !ctr;
        ctr := c + 1;
        acc := a + c + 1;
    };
    sum_lemma n; //call an F* lemma inside Pulse
    !acc;
}
```
#pop-options

This program is quite similar to multiply_by_repeated_addition, but with a couple of differences:

  • The invariant says that the current value of the accumulator holds the sum of the the first c numbers, i.e., we prove that the loop refines the recursive implementation of sum, without relying on any properties of non-linear arithmetic—notice, we have disabled non-linear arithmetic in Z3 with a pragma.

  • Finally, to prove the identity we’re after, we just call the F* sum_lemma that has already been proven from within Pulse, and the proof is concluded.

The program is a bit artificial, but hopefully it illustrates how Pulse programs can be shown to first refine a pure F* function, and then to rely on mathematical reasoning on those pure functions to conclude properties about the Pulse program itself.

Recursion

Pulse also supports general recursion, i.e., recursive functions that may not terminate. Here is a simple example—we’ll see more examples later.

Let’s start with a standard F* (doubly) recursive definition that computes the nth Fibonacci number.

let rec fib (n:nat) : nat =
  if n <= 1 then 1
  else fib (n - 1) + fib (n - 2)

One can also implement it in Pulse, as fib_rec while using an out-parameter to hold that values of the last two Fibonacci numbers in the sequence.

fn rec fib_rec (n:pos) (out:ref (nat & nat))
requires
    pts_to out 'v
ensures
    exists* v.
        pts_to out v **
        pure (
          fst v == fib (n - 1) /\
          snd v == fib n 
        )
{
  if ((n = 1))
  {
    //type inference in Pulse doesn't work well here:
    //it picks (1, 1) to have type (int & int)
    //so we have to annotate
    out := ((1 <: nat), (1 <: nat)); 
  }
  else
  {
    fib_rec (n - 1) out;
    let v = !out;
    out := (snd v, fst v + snd v);
  }
}

Some points to note here:

  • Recursive definitions in Pulse are introduced with fn rec.

  • So that we can easily memoize the last two values of fib, we expect the argument n to be a positive number, rather than also allowing 0.

  • A quirk shown in the comments: We need an additional type annotation to properly type (1, 1) as a pair of nats.

Of course, one can also define fibonacci iteratively, with a while loop, as shown below.

fn fib_loop (k:pos)
  requires emp
  returns r:nat
  ensures pure (r == fib k)
{
  let mut i : nat = 1;
  let mut j : nat = 1;
  let mut ctr : nat = 1;
  while (
    let c = !ctr;
    (c < k)
  )
  invariant b . 
    exists* vi vj vctr. 
        pts_to i vi **
        pts_to j vj **
        pts_to ctr vctr **
        pure (
            1 <= vctr /\
            vctr <= k /\
            vi == fib (vctr - 1) /\
            vj == fib vctr /\
            b == (vctr < k)
        )
  {
      let vi = !i;
      let vj = !j;
      let c = !ctr;
      ctr := c + 1;
      i := vj;
      j := vi + vj;
  };
  !j
}