Ghost Computations

Throughout the chapters on pure F*, we made routine use of the Lemmas and ghost functions to prove properties of our programs. Lemmas, you will recall, are pure, total functions that always return unit, i.e., they have no computational significance and are erased by the F* compiler. F* ghost functions are also pure, total functions, except that they are allowed to inspect erased values in a controlled way—they too are erased by the F* compiler.

As we’ve seen already, F* lemmas and ghost functions can be directly used in Pulse code. But, these are only useful for describing properties about the pure values in scope. Often, in Pulse, one needs to write lemmas that speak about the state, manipulate vprops, etc. For this purpose, Pulse provides its own notion of ghost computations (think of these as the analog of F* lemmas and ghost functions, except they are specified using vprops); and ghost state (think of these as the analog of F* erased types, except ghost state is mutable, though still computationally irrelevant). Ghost computations are used everywhere in Pulse—we’ve already seen a few example. Ghost state is especially useful in proofs of concurrent programs.

Ghost Functions

Here’s a Pulse function that fails to check, with the error message below.

[@@expect_failure]
```pulse
fn incr_erased_non_ghost (x:erased int)
requires emp
returns y:int
ensures emp ** pure (y == x + 1)
{
  let x = reveal x;
  (x + 1)
}
```

Cannot bind ghost expression reveal x with ST computation

We should expect this to fail, since the program claims to be able to compute an integer y by incrementing an erased integer x—the x:erased int doesn’t exist at runtime, so this program cannot be compiled.

But, if we tag the function with the ghost qualifier, then this works:

ghost
fn incr_erased (x:erased int)
requires emp
returns y:int
ensures emp ** pure (y == x + 1)
{
  let x = reveal x;
  (x + 1)
}

The ghost qualifier indicates the the Pulse checker that the function is to be erased at runtime, so ghost functions are allowed to make use of F* functions with GTot effect, like FStar.Ghost.reveal.

However, for this to be sound, no compilable code is allowed to depend on the return value of a ghost function. So, the following code fails with the error below:

[@@expect_failure]
```pulse
fn use_incr_erased (x:erased int)
requires emp
returns y:int
ensures emp ** pure (y == x + 1)
{
  incr_erased x;
}
```

Expected a term with a non-informative (e.g., erased) type; got int

That is, when calling a ghost function from a non-ghost context, the return type of the ghost function must be non-informative, e.g, erased, or unit etc. The class of non-informative types and the rules for allowing F* ghost computations to be used in total contexts is described here, and the same rules apply in Pulse.

To use of incr_erased in non-ghost contexts, we have to erase its result. There are a few ways of doing this.

Here’s a verbose but explicit way, where we define a nested ghost function to wrap the call to incr_erased.

fn use_incr_erased (x:erased int)
requires emp
returns y:erased int
ensures emp ** pure (y == x + 1)
{
  ghost
  fn wrap (x:erased int)
  requires emp
  returns y:erased int
  ensures emp ** pure (y == x + 1)
  {
    let y = incr_erased x;
    hide y
  };
  wrap x
}

The library also contains Pulse.Lib.Pervasives.call_ghost that is a higher-order combinator to erase the result of a ghost call.

fn use_incr_erased_alt (x:erased int)
requires emp
returns y:erased int
ensures emp ** pure (y == x + 1)
{ 
  call_ghost incr_erased x;
}

The call_ghost combinator can be used with ghost functions of different arities, though it requires the applications to be curried in the following way.

Suppose we have a binary ghost function, like add_erased:

ghost
fn add_erased (x y:erased int)
requires emp
returns z:int
ensures emp ** pure (z == x + y)
{
  let x = reveal x;
  let y = reveal y;
  (x + y)
}

To call it in a non-ghost context, one can do the following:

fn use_add_erased (x y:erased int)
requires emp
returns z:erased int
ensures emp ** pure (z == x + y)
{
  call_ghost (add_erased x) y
}

That said, since ghost functions must have non-informative return types to be usable in non-ghost contexts, it’s usually best to define them that way to start with, rather than having to wrap them at each call site, as shown below:

ghost
fn add_erased_erased (x y:erased int)
requires emp
returns z:erased int
ensures emp ** pure (z == x + y)
{
  let x = reveal x;
  let y = reveal y;
  hide (x + y)
}

Some Primitive Ghost Functions

Pulse ghost functions with emp or pure _ pre and postconditions are not that interesting—such functions can usually be written with regular F* ghost functions.

Ghost functions are often used as proof steps to prove equivalences among vprops. We saw a few examples of ghost functions before—they are ghost since their implementations are compositions of ghost functions from the Pulse library.

The rewrite primitive that we saw previously is in fact a defined function in the Pulse library. Its signature looks like this:

ghost
fn __rewrite (p q:vprop)
requires p ** pure (p == q)
ensures q

Many of the other primitives like fold, unfold, etc. are defined in terms of rewrite and are ghost computations.

Other primitives like introduce exists* are also implemented in terms of library ghost functions, with signatures like the one below:

ghost
fn intro_exists (#a:Type0) (p:a -> vprop) (x:erased a)
requires p x
ensures exists* x. p x

Recursive Predicates and Ghost Lemmas

We previously saw how to define custom predicates, e.g., for representation predicates on data structures. Since a vprop is just a regular type, one can also define vprops by recursion in F*. Working with these recursive predicates in Pulse usually involves writing recursive ghost functions as lemmas. We’ll look at a simple example of this here and revisit in subsequent chapters as look at programming unbounded structures, like linked lists.

Say you have a list of references and want to describe that they all contain integers whose value is at most n. The recursive predicate all_at_most l n does just that:

let rec all_at_most (l:list (ref nat)) (n:nat)
: vprop
= match l with
  | [] -> emp
  | hd::tl -> exists* (i:nat). pts_to hd i ** pure (i <= n) ** all_at_most tl n

As we did when working with nullable references, it’s useful to define a few helper ghost functions to introduce and eliminate this predicate, for each of its cases.

The elimination and introduction functions for the [] case are very similar to what had previously with nullable references:

ghost 
fn intro_all_at_most_nil (l:list (ref nat)) (n:nat)
requires pure (l == [])
ensures all_at_most l n
{
  fold (all_at_most [] n);
  rewrite each (Nil #(ref nat)) as l;
}

ghost
fn elim_all_at_most_nil (l:list (ref nat)) (n:nat)
requires all_at_most l n ** pure (l == [])
ensures emp
{
  rewrite (all_at_most l n) as (all_at_most [] n);
  unfold (all_at_most [] n);
}

For the hd::tl case, we have to be a bit more careful in how we do the rewriting: using a regular rewrite fails, since it involves proving an equality between two higher-order terms (the body of exists* is represented in F* as a lambda term). Pulse also provides a rewrite_by function in the library that allows rewriting terms using a user-provided tactic. In this case, the tactic Pulse.Lib.Pervasives.vprop_equiv_norm equates vprops by proving them definitionally equal by normalization.

ghost
fn intro_all_at_most_cons (l:list (ref nat)) (hd:ref nat) (tl:list (ref nat)) (n:nat)
requires pts_to hd 'i ** all_at_most tl n ** pure ('i <= n) ** pure (l == hd :: tl)
ensures all_at_most l n
{
  rewrite_by (exists* (i:nat). pts_to hd i ** pure (i <= n) ** all_at_most tl n)
             (all_at_most (hd::tl) n)
             vprop_equiv_norm ();
  rewrite each (hd::tl) as l;
}

ghost
fn elim_all_at_most_cons (l:list (ref nat)) (hd:ref nat) (tl:list (ref nat)) (n:nat)
requires all_at_most l n ** pure (l == hd :: tl)
ensures exists* (i:nat). pts_to hd i ** pure (i <= n) ** all_at_most tl n
{
  rewrite (all_at_most l n) as (all_at_most (hd :: tl) n);
  rewrite_by (all_at_most (hd::tl) n)
             (exists* (i:nat). pts_to hd i ** pure (i <= n) ** all_at_most tl n)
             vprop_equiv_norm ();
}

Recursive Ghost Lemmas

Pulse allows writing recursive ghost functions as lemmas for use in Pulse code. Like F* lemmas, recursive ghost functions must be proven to terminate on all inputs—otherwise, they would not be sound.

To see this in action, let’s write a ghost function to prove that all_at_most l n can be weakened to all_at_most l m when n <= m.

ghost
fn rec weaken_at_most (l:list (ref nat)) (n:nat) (m:nat)
requires all_at_most l n ** pure (n <= m)
ensures all_at_most l m
decreases l
{
  match l {
    Nil -> {
      elim_all_at_most_nil l n;
      intro_all_at_most_nil l m
    }
    Cons hd tl -> {
      elim_all_at_most_cons l hd tl n;
      weaken_at_most tl n m;
      intro_all_at_most_cons l hd tl m
    }
  }
}

A few points to note:

Recursive functions in Pulse are defined using fn rec.

Ghost recursive functions must also have a decreases annotation—unlike in F*, Pulse does not yet attempt to infer a default decreases annotation. In this case, we are recursing on the list l.

List patterns in Pulse do not (yet) have the same syntactic sugar as in F*, i.e., you cannot write [] and hd::tl as patterns.

The proof itself is fairly straightforward:

In the Nil case, we eliminate the all_at_most predicate at n and introduce it at m.

In the Cons case, we eliminate all_at_most l n,` use the induction hypothesis to weaken the all_at_most predicate on the tl; and then introduce it again, packaging it with assumption on hd.

Mutable Ghost References

The underlying logic that Pulse is based on actually supports a very general form of ghost state based on partial commutative monoids (PCMs). Users can define their own ghost state abstractions in F* using PCMs and use these in Pulse programs. The library Pulse.Lib.GhostReference provides the simplest and most common form of ghost state: references to erased values with a fractional-permission-based ownership discipline.

We’ll use the module abbreviation module GR = Pulse.Lib.GhostReference in what follows. The library is very similar to Pulse.Lib.Reference, in that it provides:

GR.ref a: The main type of ghost references. GR.ref is an erasable type and is hence considered non-informative.

GR.pts_to (#a:Type0) (r:GR.ref a) (#p:perm) (v:a) : vprop is the main predicate provided by the library. Similar to the regular pts_to, the permission index defaults to full_perm.

Unlike ref a (and more like box a), ghost references GR.ref a are not lexically scoped: they are allocated using GR.alloc and freed using GR.free. Of course, neither allocation nor free’ing has any runtime cost—these are just ghost operations.

Reading a ghost reference using !r returns an erased a, when r:GR.ref a. Likewise, to update r, it is enough to provide a new value v:erased a.

Operations to share and gather ghost references work just as with ref.

A somewhat contrived example

Most examples that require ghost state usually involve stating interesting invariants between multiple threads, or sometimes in a sequential setting to correlate knowledge among different components. We’ll see examples of that in a later chapter. For now, here’s a small example that gives a flavor of how ghost state can be used.

Suppose we want to give a function read/write access to a reference, but want to ensure that before it returns, it resets the value of the reference to its original value. The simplest way to do that would be to give the function the following signature:

fn uses_but_resets #a (x:ref a)
requires pts_to x 'v
ensures pts_to x 'v

Here’s another way to do it, this time with ghost references.

First, we define a predicate correlated that holds full permission to a reference and half permission to a ghost reference, forcing them to hold the same value.

let correlated #a (x:ref a) (y:GR.ref a) (v:a)=
  pts_to x v ** GR.pts_to y #one_half v

Now, here’s the signature of a function use_temp: at first glance, from its signature alone, one might think that the witness v0 bound in the precondition is unrelated to the v1 bound in the postcondition.

fn use_temp (x:ref int) (y:GR.ref int)
requires exists* v0. correlated x y v0
ensures exists* v1. correlated x y v1

But, use_temp only has half-permission to the ghost reference and cannot mutate it. So, although it can mutate the reference itself, in order to return its postcondition, it must reset the reference to its initial value.

{
  unfold correlated;
  let v = !x;
  x := 17; //temporarily mutate x, give to to another function to use with full perm
  x := v; //but, we're forced to set it back to its original value
  fold correlated;
}

This property can be exploited by a caller to pass a reference to use_temp and be assured that the value is unchanged when it returns.

fn use_correlated ()
requires emp
ensures emp
{
  let mut x = 17;
  let g = GR.alloc 17;
  GR.share g;
  fold correlated;  // GR.pts_to g #one_half 17 ** correlated x g 17
  use_temp x g;     // GR.pts_to g #one_half 17 ** correlated x g ?v1
  unfold correlated; // GR.pts_to g #one_half 17 ** GR.pts_to g #one_half ?v1 ** pts_to x ?v1
  GR.gather g;       //this is the crucial step
                     // GT.pts_to g 17 ** pure (?v1 == 17) ** pts_to x ?v1
  assert (pts_to x 17);
  GR.free g;
}