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