Implication and Universal Quantification

In this chapter, we’ll learn about two more separation logic connectives, @==> and forall*. We show a few very simple examples using them, though these will be almost trivial. In the next chapter, on linked lists, we’ll see more significant uses of these connectives.

Trades, or Separating Ghost Implication

The library module I = Pulse.Lib.Stick.Util defines the operator trade (@==>) and utilities for using it. In the literature, the operator p --* q is pronounced “p magic-wand q”; p @==> q is similar, though there are some important technical differences, as we’ll see. We’ll just pronounce it p for q, or p trades for q. Here’s an informal description of what p @==> q means:

p @==> q says that if you have p then you can trade it for q. In other words, from p ** (p @==> q), you can derive q. This step of reasoning is performed using a ghost function I.elim with the signature below:

ghost
fn I.elim (p q:vprop)
requires p ** (p @==> q)
ensures q

Importantly, if you think of p as describing permission on a resource, the I.elim makes you give up the permission p and get q as a result. Note, during this step, you also lose permission on the implication, i.e., p @==> q lets you trade p for q just once.

But, how do you create a p @==> q in the first place? That’s its introduction form, shown below:

ghost
fn I.intro (p q r:vprop)
           (elim: unit -> stt_ghost unit emp_inames (r ** p) (fun _ -> q))
requires r
ensures p @==> q

That is, to introduce p @==> q, one has to show hold permission r, such that a ghost function can transform r ** p into q.

Share and Gather

Here’s a small example to see p @==> q at work.

let regain_half #a (x:GR.ref a) (v:a) =
  pts_to x #0.5R v @==> pts_to x v

The predicate regain_half says that you can trade a half-permission pts_to x #one_half v for a full permission pts_to x v. At first, this may seem counter-intuitive: how can you gain a full permission from half-permission. The thing to remember is that p @==> q itself holds permissions internally. In particular, regain_half x v holds exists* u. pts_to x #one_half u internally, such that if the context presents the other half, the eliminator can combine the two to return the full permission.

Let’s look at how to introduce regain_half:

ghost 
fn intro_regain_half (x:GR.ref int)
requires pts_to x 'v
ensures pts_to x #0.5R 'v ** regain_half x 'v
{
  ghost
  fn aux ()
  requires pts_to x #0.5R 'v ** pts_to x #0.5R 'v
  ensures pts_to x 'v
  {
    GR.gather x;
  };
  GR.share x;
  I.intro _ _ _ aux;
  fold regain_half;
}

The specification says that if we start out with pts_to x 'v then we can split it into pts_to x #one_half v and a regain_half x 'v. The normal way of splitting a permission a reference would split it into two halves—here, we just package the second half in a ghost function that allows us to gather the permission back when we need it.

In the implementation, we define an auxiliary ghost function that corresponds to the eliminator for pts_to x #one_half 'v @==> pts_to x 'v—it’s just a gather. Then, we split pts_to x 'v into halves, call I.intro passing the eliminator, and the fold it into a regain_half. All regain_half has done is to package the ghost function aux, together the half permission on x, and put it into a vprop.

Later on, if want to use regain_half, we can call its eliminator—which, effectively, calls aux with the needed permission, as shown below.

ghost
fn use_regain_half (x:GR.ref int)
requires pts_to x #0.5R 'v ** regain_half x 'v
ensures pts_to x 'v
{
  unfold regain_half;
  I.elim _ _;
}

At this point, you may be wondering why we bother to use a regain_half x 'v in the first place, since one might as well have just used pts_to x #one_half 'v and gather, and you’d be right to wonder that! In this simple usage, the (@==>) hasn’t bought us much.

Universal Quantification

Let’s look at our regain_half predicate again:

let regain_half #a (x:GR.ref a) (v:a) =
  pts_to x #0.5R v @==> pts_to x v

This predicate is not as general as it could be: to eliminate it, it requires the caller to prove that they holds pts_to x #one_half v, for the same v as was used when the trade was introduced.

One could try to generalize regain_half a bit by changing it to:

let regain_half #a (x:GR.ref a) (v:a) =
  (exists* u. pts_to x #one_half u) @==> pts_to x v

This is an improvement, but it still is not general enough, since it does not relate v to the existentially bound u. What we really need is a universal quantifier.

Here’s the right version of regain_half:

let regain_half_q #a (x:GR.ref a) =
  forall* u. pts_to x #0.5R u @==> pts_to x u

This says that no matter what pts_to x #one_half u the context has, they can recover full permission to it, with the same witness u.

The forall* quantifier and utilities to manipulate it are defined in Pulse.Lib.Forall.Util. The introduction and elimination forms have a similar shape to what we saw earlier for @==>:

ghost
fn FA.elim (#a:Type) (#p:a->vprop) (v:a)
requires (forall* x. p x)
ensures p v

The eliminator allows a single instantiation of the universally bound x to v.

ghost
fn FA.intro (#a:Type) (#p:a->vprop)
     (v:vprop)
     (f_elim : (x:a -> stt_ghost unit emp_inames v (fun _ -> p x)))
requires v
ensures (forall* x. p x)

The introduction form requires proving that one holds v, and that with v a ghost function can produce p x, for any x.

Note, it’s very common to have universal quantifiers and trades together, so the library also provides the following combined forms:

ghost
fn elim_forall_imp (#a:Type0) (p q: a -> vprop) (x:a)
requires (forall* x. p x @==> q x) ** p x
ensures q x

and

ghost
fn intro_forall_imp (#a:Type0) (p q: a -> vprop) (r:vprop)
         (elim: (u:a -> stt_ghost unit emp_inames
                          (r ** p u)
                          (fun _ -> q u)))
requires r
ensures forall* x. p x @==> q x

Share and Gather, Again

Here’s how one introduces regain_half_q:

ghost 
fn intro_regain_half_q (x:GR.ref int)
requires pts_to x 'v
ensures pts_to x #0.5R 'v ** regain_half_q x
{
  ghost
  fn aux1 (u:int)
  requires pts_to x #0.5R 'v ** pts_to x #0.5R u
  ensures pts_to x u
  {
    gather x;
  };
  GR.share x;
  FA.intro_forall_imp _ _ _ aux1;
  fold regain_half_q;
}

Now, when we want to use it, we can trade in any half-permission on pts_to x #one_half u, for a full permission with the same u.

ghost
fn use_regain_half_q (x:GR.ref int)
requires pts_to x #0.5R 'u ** regain_half_q x
ensures pts_to x 'u
{
  unfold regain_half_q;
  FA.elim #_ #(fun u -> pts_to x #0.5R u @==> pts_to x u) 'u;
  I.elim _ _;
}

Note using the eliminator for FA.elim is quite verbose: we need to specify the quantifier term again. The way Pulse uses F*’s unifier currently does not allow it to properly find solutions to some higher-order unification problems. We expect to fix this soon.

Trades and Ghost Steps

As a final example in this section, we show that one can use package any ghost computation into a trade, including steps that may modify the ghost state. In full generality, this makes @==> behave more like a view shift (in Iris terminology) than a wand.

Here’s a predicate can_update which says that one can trade a half permission to pts_to x #one_half u for a full permission to a different value pts_to x v.

let can_update (x:GR.ref int) = 
  forall* u v. pts_to x #0.5R u @==>
               pts_to x v

In make_can_update, we package a ghost-state update function into a binary quantifier forall* u v. ....

ghost
fn make_can_update (x:GR.ref int)
requires pts_to x 'w
ensures pts_to x #0.5R 'w ** can_update x
{
  ghost
  fn aux (u:int)
  requires pts_to x #0.5R 'w
  ensures forall* v. pts_to x #0.5R u @==> pts_to x v
  {
    ghost
    fn aux (v:int)
    requires pts_to x #0.5R 'w ** pts_to x #0.5R u
    ensures pts_to x v
    {
      gather x;
      x := v;
    };
    FA.intro_forall_imp _ _ _ aux;
  };
  share x;
  FA.intro _ aux;
  fold (can_update x);
}

And in update, below, we instantiate it to update the reference x from 'u to k, and also return back a can_update predicate to the caller, for further use.

ghost
fn update (x:GR.ref int) (k:int)
requires pts_to x #0.5R 'u ** can_update x
ensures pts_to x #0.5R k ** can_update x
{
  unfold can_update;
  FA.elim #_ #(fun u -> forall* v. pts_to x #0.5R u @==> pts_to x v) 'u;
  FA.elim #_ #(fun v -> pts_to x #0.5R 'u @==> pts_to x v) k;
  I.elim _ _;
  make_can_update x;
}