# Conditionals

To start writing interesting programs, we need a few control constructs. In this chapter, we’ll write some programs with branches of two kinds: `if/else` and `match`.

## A Simple Branching Program: Max

Here’s a simple program that returns the maximum value stored in two references.

```let max_spec x y = if x < y then y else x

```pulse
fn max #p #q (x y:ref int)
requires pts_to x #p 'vx ** pts_to y #q 'vy
returns n:int
ensures pts_to x #p 'vx ** pts_to y #q 'vy
** pure (n == max_spec 'vx 'vy)
{
let vx = !x;
let vy = !y;
if (vx > vy)
{
vx
}
else
{
vy
}
}
```
```

This program illustrates a very common specification style.

• We have a pure, F* function `max_spec`

• And a Pulse function working on mutable references, with a specification that relates it to the pure F* spec. In this case, we prove that `max` behaves like `max_spec` on the logical values that witness the contents of the two references.

The implementation of `max` uses a Pulse conditional statement. Its syntax is different from the F* `if-then-else` expression: Pulse uses a more imperative syntax with curly braces, which should be familiar from languages like C.

### Limitation: Non-tail Conditionals

Pulse’s inference machinery does not yet support conditionals that appear in non-tail position. For example, this variant of `max` fails, with the error message shown below.

```fn max_alt #p #q (x y:ref int)
requires pts_to x #p 'vx ** pts_to y #q 'vy
returns n:int
ensures pts_to x #p 'vx ** pts_to y #q 'vy
** pure (n == max_spec 'vx 'vy)
{
let mut result = 0;
let vx = !x;
let vy = !y;
if (vx > vy)
{
result := vx;
}
else
{
result := vy;
};
!result;
}
```
```Pulse cannot yet infer a postcondition for a non-tail conditional statement;
Either annotate this `if` with `returns` clause; or rewrite your code to use a tail conditional
```

Here’s an annotated version of `max_alt` that succeeds.

```fn max_alt #p #q (x y:ref int)
requires pts_to x #p 'vx ** pts_to y #q 'vy
returns n:int
ensures pts_to x #p 'vx ** pts_to y #q 'vy
** pure (n == max_spec 'vx 'vy)
{
let mut result = 0;
let vx = !x;
let vy = !y;
if (vx > vy)
ensures
exists* r.
pts_to x #p 'vx **
pts_to y #q 'vy **
pts_to result r **
pure (r == max_spec 'vx 'vy)
{
result := vx;
}
else
{
result := vy;
};
!result;
}
```

We are working on adding inference for non-tail conditionals.

## Pattern matching with nullable references

To illustrate the use of pattern matching, consider the following representation of a possibly null reference.

```let nullable_ref a = option (ref a)

let pts_to_or_null #a
(x:nullable_ref a)
(#[default_arg (`full_perm)] p:perm) //implicit argument with a default
(v:option a)
: vprop
= match x with
| None -> pure (v == None)
| Some x -> exists* w. pts_to x #p w ** pure (v == Some w)
```

### Representation predicate

We can represent a nullable ref as just an `option (ref a)` coupled with a representation predicate, `pts_to_or_null`. A few points to note:

• The notation `(#[default_arg (\`full_perm)] p:perm)` is F* syntax for an implicit argument which when omitted defaults to `full_perm`—this is exactly how predicates like `Pulse.Lib.Reference.pts_to` are defined.

• The definition is by cases: if the reference `x` is `None`, then the logical witness is `None` too.

• Otherwise, the underlying reference points to some value `w` and the logical witness `v == Some w` agrees with that value.

Note, one might consider defining it this way:

```let pts_to_or_null #a
(x:nullable_ref a)
(#[default_arg (`full_perm)] p:perm)
(v:option a)
: vprop
= match x with
| None -> pure (v == None)
| Some x -> pure (Some? v) ** pts_to x #p (Some?.v v)
```

However, unlike F*’s conjunction `p /\ q` where the well-typedness of `q` can rely on `p`, the `**` operator is not left-biased; so `(Some?.v v)` cannot be proven in this context and the definition is rejected.

Another style might be as follows:

```let pts_to_or_null #a
(x:nullable_ref a)
(#[default_arg (`full_perm)] p:perm)
(v:option a)
: vprop
= match x, v with
| None, None -> emp
| Some x, Some w -> pts_to x #p w
| _ -> pure False
```

This could also work, though it would require handling an additional (impossible) case.

Let’s try our first pattern match in Pulse:

```fn read_nullable #a #p (r:nullable_ref a)
requires pts_to_or_null r #p 'v
returns o:option a
ensures pts_to_or_null r #p 'v
** pure ('v == o)
{
match r {
Some x -> {
rewrite each r as (Some x);
unfold (pts_to_or_null (Some x) #p 'v);
let o = !x;
fold (pts_to_or_null (Some x) #p 'v);
rewrite each (Some x) as r;
Some o
}
None -> {
rewrite each r as None;
unfold (pts_to_or_null None #p 'v);
fold (pts_to_or_null None #p 'v);
rewrite each (None #(ref a)) as r;
None #a
}
}
}
```

The syntax of pattern matching in Pulse is more imperative and Rust-like than what F* uses.

• The entire body of match is enclosed within braces

• Each branch is also enclosed within braces.

• Pulse (for now) only supports simple patterns with a single top-level constructor applied to variables, or variable patterns: e.g., you cannot write `Some (Some x)` as a pattern.

The type of `read_nullable` promises to return a value equal to the logical witness of its representation predicate.

The code is a little tedious—we’ll see how to clean it up a bit shortly.

A `show_proof_state` in the `Some x` branch prints the following:

```- Current context:
pts_to_or_null r (reveal 'v)
- In typing environment:
[branch equality#684 : squash (eq2 r (Some x)),
...
```

The interesting part is the `branch equality` hypothesis, meaning that in this branch, we can assume that `(r == Some x)`. So, the first thing we do is to rewrite `r`; then we `unfold` the representation predicate; read the value `o` out of `x`; fold the predicate back; rewrite in the other direction; and return ```Some o```. The `None` case is similar.

Another difference between Pulse and F* matches is that Pulse does not provide any negated path conditions. For example, in the example below, the assertion fails, since the pattern is only a wildcard and the Pulse checker does not prove `not (Some? x)` as the path condition hypothesis for the preceding branches not taken.

```[@@expect_failure]
```pulse
fn read_nullable_alt #a #p (r:nullable_ref a)
requires pts_to_or_null r #p 'v
returns o:option a
ensures emp
{
match r {
Some x -> { admit () }
_ -> {
// we only have `r == _` in scope
// not the negation of the prior branch conditions
// i.e., unlike F*, we don't have not (Some? r)
// so the assertion below fails
assert (pure (r == None));
}
}
```
```

We plan to enhance the Pulse checker to also provide these negated path conditions.

### Helpers

When a `vprop` is defined by cases (like `pts_to_or_null`) it is very common to have to reason according to those cases when pattern matching. Instead of rewriting, unfolding, folding, and rewriting every time, one can define helper functions to handle these cases.

``````pulse
ghost
fn elim_pts_to_or_null_none #a #p (r:nullable_ref a)
requires pts_to_or_null r #p 'v ** pure (r == None)
ensures pts_to_or_null r #p 'v ** pure ('v == None)
{
rewrite each r as None;
unfold (pts_to_or_null None #p 'v);
fold (pts_to_or_null None #p 'v);
rewrite each (None #(ref a)) as r;
}
```

```pulse
ghost
fn intro_pts_to_or_null_none #a #p (r:nullable_ref a)
requires pure (r == None)
ensures pts_to_or_null r #p None
{
fold (pts_to_or_null #a None #p None);
rewrite each (None #(ref a)) as r;
}
```

```pulse
ghost
fn elim_pts_to_or_null_some #a #p (r:nullable_ref a) (x:ref a)
requires pts_to_or_null r #p 'v ** pure (r == Some x)
ensures exists* w. pts_to x #p w ** pure ('v == Some w)
{
rewrite each r as (Some x);
unfold (pts_to_or_null (Some x) #p 'v);
}
```

```pulse
ghost
fn intro_pts_to_or_null_some #a #p (r:nullable_ref a) (x:ref a)
requires pts_to x #p 'v ** pure (r == Some x)
ensures pts_to_or_null r #p (Some 'v)
{
fold (pts_to_or_null (Some x) #p (Some 'v));
rewrite each (Some x) as r;
}
```
```

These functions are all marked `ghost`, indicating that they are purely for proof purposes only.

Writing these helpers is often quite mechanical: One could imagine that the Pulse checker could automatically generate them from the definition of `pts_to_or_null`. Using F*’s metaprogramming support, a user could also auto-generate them in a custom way. For now, we write them by hand.

Using the helpers, case analyzing a nullable reference is somewhat easier:

```fn read_nullable_alt #a #p (r:nullable_ref a)
requires pts_to_or_null r #p 'v
returns o:option a
ensures pts_to_or_null r #p 'v
** pure ('v == o)
{
match r {
Some x -> {
elim_pts_to_or_null_some r x;
let o = !x;
intro_pts_to_or_null_some r x;
Some o
}
None -> {
elim_pts_to_or_null_none r;
None #a
}
}
}
```

### Writing a nullable reference

Having defined our helpers, we can use them repeatedly. For example, here is a function to write a nullable reference.

```fn write_nullable #a (r:nullable_ref a) (v:a)
requires pts_to_or_null r 'v
ensures exists* w. pts_to_or_null r w ** pure (Some? r ==> w == Some v)
{
match r {
None -> { () }
Some x -> {
elim_pts_to_or_null_some r x;
x := v;
intro_pts_to_or_null_some r x;
}
}
}
```