# 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.

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.

## 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
}
```