User-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))
}

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;
}