Loops & Recursion

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)

let rec sum_lemma (n:nat)
: Lemma (sum n == n * (n + 1) / 2)
= if n = 0 then ()
  else sum_lemma (n - 1)

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'"
```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.