# User-defined Predicates

In addition to the vprop predicates and connectives that the Pulse
libraries provide, users very commonly define their own `vprops`

. We
show a few simple examples here—subsequent examples will make heavy
use of user-defined predicates. For example, see this section for
recursively defined predicates.

## Fold and Unfold with Diagonal Pairs

A simple example of a user-defined abstraction is show below.

```
let pts_to_diag
#a
(r:ref (a & a))
(v:a)
: vprop
= pts_to r (v, v)
```

`pts_to_diag r v`

is a `vprop`

defined in F* representing a
reference to a pair whose components are equal.

We can use this abstraction in a Pulse program, though we have to be explicit about folding and unfolding the predicate.

```
fn double (r:ref (int & int))
requires pts_to_diag r 'v
ensures pts_to_diag r (2 * 'v)
{
unfold (pts_to_diag r 'v);
let v = !r;
let v2 = fst v + snd v;
r := (v2, v2);
fold (pts_to_diag r v2);
}
```

The `unfold p`

command checks that `p`

is provable in the current
context by some term `q`

, and then rewrites the context by replacing
that occurrence of `q`

with the term that results from unfolding the
head symbol of `p`

. A `show_proof_state`

after the `unfold`

shows that we have a `pts_to r (reveal 'v, reveal 'v)`

in the
context, exposing the abstraction of the `pts_to_diag`

predicate.

At the end of function, we use the `fold p`

command: this checks
that the unfolding of `p`

is provable in the context by some term
`q`

and then replaces `q`

in the context with `p`

.

`fold`

and `unfold`

is currently very manual in Pulse. While in
the general case, including with recursively defined predicates,
automating the placement of folds and unfolds is challenging, many
common cases (such as the ones here) can be easily automated. We are
currently investigating adding support for this.

Some initial support for this is already available, inasmuch as Pulse can sometimes figure out the arguments to the vprops that need to be folded/unfolded. For instance, in the code below, we just mention the name of the predicate to be unfolded/folded, without needing to provide all the arguments.

```
fn double_alt (r:ref (int & int))
requires pts_to_diag r 'v
ensures pts_to_diag r (2 * 'v)
{
unfold pts_to_diag;
let v = !r;
let v2 = fst v + snd v;
r := (v2, v2);
fold pts_to_diag;
}
```

## Mutable Points

As a second, perhaps more realistic example of a user-defined abstraction, we look at defining a simple mutable data structure: a structure with two mutable integer fields, representing a 2-dimensional point.

```
noeq
type point = {
x:ref int;
y:ref int;
}
let is_point (p:point) (xy: int & int) =
pts_to p.x (fst xy) **
pts_to p.y (snd xy)
```

A `point`

is just an F* record containing two
references. Additionally, we define `is_point`

, a `vprop`

,
sometimes called a “representation predicate”, for a
`point`

. `is_point p xy`

says that `p`

is a representation of
the logical point `xy`

, where `xy`

is pure, mathematical pair.

We can define a function `move`

, which translates a point by some
offset `dx, dy`

.

```
fn move (p:point) (dx:int) (dy:int)
requires is_point p 'xy
ensures is_point p (fst 'xy + dx, snd 'xy + dy)
{
unfold is_point;
let x = !p.x;
let y = !p.y;
p.x := x + dx;
p.y := y + dy;
fold (is_point p (x + dx, y + dy));
}
```

Implementing `move`

is straightforward, but like before, we have to
`unfold`

the `is_point`

predicate first, and then fold it back up
before returning.

Unfortunately, Pulse cannot infer the instantiation of `is_point`

when folding it. A `show_proof_state`

prior to the fold should help
us see why:

We have

`pts_to p.x (x + dx) ** pts_to p.y (y + dy)`

For

`fold (is_point p.x ?w)`

to succeed, we rely on F*’s type inference to find a solution for the unsolved witness`?w`

such that`fst ?w == (x + dx)`

and`snd ?w == (y + dy)`

. This requires an eta-expansion rule for pairs to solve`?w := (x + dx, y + dy)`

, but F*’s type inference does not support such a rule for pairs.

So, sadly, we have to provide the full instantiation ```
is_point p (x +
dx, y + dy)
```

to complete the proof.

This pattern is a common problem when working with representation predicates that are indexed by complex values, e.g., pairs or records. It’s common enough that it is usually more convenient to define a helper function to fold the predicate, as shown below.

```
ghost
fn fold_is_point (p:point)
requires pts_to p.x 'x ** pts_to p.y 'y
ensures is_point p (reveal 'x, reveal 'y)
{
fold (is_point p (reveal 'x, reveal 'y))
}
```

Note

We’ve marked this helper function `ghost`

. We’ll look into
`ghost`

functions in much more detail in a later chapter.

This allows type inference to work better, as shown below.

```
fn move_alt (p:point) (dx:int) (dy:int)
requires is_point p 'xy
ensures is_point p (fst 'xy + dx, snd 'xy + dy)
{
unfold is_point;
let x = !p.x;
let y = !p.y;
p.x := x + dx;
p.y := y + dy;
fold_is_point p;
}
```

## Rewriting

In addition to `fold`

and `unfold`

, one also often uses the
`rewrite`

command when working with defined predicates. Its general
form is:

```
with x1 ... xn. rewrite p as q;
rest
```

Its behavior is to find a substitution `subst`

that instantiates the
`x1 ... xn`

as `v1 ... vn`

, such that `subst(p)`

is supported by
`c`

in the context, Pulse aims to prove that ```
subst(p) ==
subst(q)
```

and replaces `c`

in the context by `subst(q)`

and
proceeds to check `subst(rest)`

.

To illustrate this at work, consider the program below:

```
fn create_and_move ()
requires emp
ensures emp
{
let mut x = 0;
let mut y = 0;
let p = { x; y };
//pts_to x 0 ** pts_to y 0
with _v. rewrite pts_to x _v as pts_to p.x _v;
with _v. rewrite pts_to y _v as pts_to p.y _v;
//pts_to p.x 0 ** pts_to p.y 0
fold_is_point p;
move p 1 1;
assert (is_point p (1, 1));
unfold is_point;
//pts_to p.x (fst (1, 1)) ** pts_to p.y (snd (1, 1))
with _v. rewrite pts_to p.x _v as pts_to x _v;
with _v. rewrite pts_to p.y _v as pts_to y _v;
//pts_to x (fst (1, 1)) ** pts_to y (snd (1, 1))
}
```

We allocate two references and put them in the structure `p`

. Now,
to call `fold_is_point`

, we need `pts_to p.x _`

and ```
pts_to p.y
_
```

, but the context only contains `pts_to x _`

and ```
pts_to y
_
```

. The `rewrite`

command transforms the context as needed.

At the end of the function, we need to prove that `pts_to x _`

and
`pts_to y _`

as we exit the scope of `y`

and `x`

, so that they
can be reclaimed. Using `rewrite`

in the other direction
accomplishes this.

This is quite verbose. As with `fold`

and `unfold`

, fully
automated `rewrite`

in the general case is hard, but many common
cases are easy and we expect to add support for that to the Pulse
checker.

In the meantime, Pulse provides a shorthand to make some common rewrites easier.

The `rewrite each`

command has the most general form:

```
with x1 ... xn. rewrite each e1 as e1', ..., en as en' in goal
```

This is equivalent to:

```
with x1 ... xn. assert goal;
rewrite each e1 as e1', ..., en as en' in goal
```

```
rewrite each e1 as e1', ..., en as en' in goal
```

is equivalent to

```
rewrite goal as goal'
```

where `goal'`

is computed by rewriting, in parallel, every
occurrence of `ei`

as `ei'`

in `goal`

.

Finally, one can also write:

```
rewrite each e1 as e1', ..., en as en'
```

omitting the `goal`

term. In this case, the `goal`

is taken to be
the entire current `vprop`

context.

Using `rewrite each ...`

makes the code somewhat shorter:

```
fn create_and_move_alt ()
requires emp
ensures emp
{
let mut x = 0;
let mut y = 0;
let p = { x; y };
rewrite each x as p.x, y as p.y;
fold_is_point p;
move p 1 1;
assert (is_point p (1, 1));
unfold is_point;
rewrite each p.x as x, p.y as y;
}
```