Atomic Operations and Invariants

Boxable predicates

Pulse’s language of predicates, i.e., the type vprop, is stratified. The type boxable is a refinement of vprop, defined as shown below in Pulse.Lib.Core

let boxable = v:vprop { is_big v }

That is, certain vprops, i.e., those that satisfy is_big, are boxable predicates. All the predicates that we have encountered so far are boxable, except for the inv i p predicate. For example, pts_to x v is boxable; exists* x. p x is boxable if p x is boxable; etc. However inv i p is not boxable.

Why does this matter? It turns out that PulseCore, the logic on which Pulse is built, only allows turning boxable predicates into invariants. That is, while one can build an invariant such as inv i (exists* v. pts_to x v), one cannot nest invariants, i.e., there is no meaningful way to construct an instance of inv i (inv j p).

This restriction is a fundamental limitation of PulseCore: invariants cannot mention other invariants. In more technical terms, invariants are predicative. One might wonder whether this limitation is significant: after all, why might one want to construct an invariant that states that some p is already an invariant? It turns out that such predicates, although not very common, are useful and the inability to nest invariants in Pulse makes some styles of proofs awkward or perhaps even impossible. Nevertheless, forcing invariants to be predicative gives Pulse a simple foundational model in PulseCore in terms of a standard, predicative, dependently typed logic.

Let’s look next at how to turn a boxable predicate into an invariant.

Creating an invariant and boxable predicates

Let’s start by looking at how to create an invariant.

First, let’s define a predicate owns x, to mean that we hold full-permission on x.

let owns (x:ref U32.t) : v:vprop { is_big v }= exists* v. pts_to x v

Notice the type annotation on owns claims that it is boxable, and indeed F*’s refinement type checker automatically proves that it is.

Now, if we can currently prove pts_to r x then we can turn it into an invariant inv i (owns r), as shown below.

ghost
fn create_invariant (r:ref U32.t) (v:erased U32.t)
requires pts_to r v
returns i:iref
ensures inv i (owns r)
{
    fold owns;
    new_invariant (owns r)
}

Importantly, when we turn pts_to r x into inv i (owns r), we lose ownership of pts_to r x. Remember, once we have inv i (owns r), Pulse’s logic aims to prove that owns r remains true always. If we were allowed to retain pts_to r x, while also creating an inv i (owns r), we can clearly break the invariant, e.g., by freeing r.

Note, if one were to try to allocate an invariant for a non-boxable predicate, typechecking fails, as shown in the example below:

ghost
fn create_non_boxable_inv (p:vprop)
requires p
returns i:iref
ensures inv i p
{
  new_invariant p;
}

failing with an error pointing to the source location of the refinement precondition, is_big, at the call to new_invariant.

- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.
- See also ../../../lib/pulse/lib/Pulse.Lib.Core.fsti(536,29-536,37)

As you can see, although the language does not prevent you from writing inv i p for any predicate p, the only way to allocate an instance of inv i p is by provable that p is boxable. This design is convenient since the onus of proving that a predicate is boxable is only placed at the allocation site of the invariant—uses of invariants do not need to worry about the distinction between boxable and general vprops.

Opening an invariant

Now that we’ve allocated an inv i (owns r), what can we do with it? As we said earlier, one can make use of the owns r in an atomic computation, so long as we restore it at the end of the atomic step.

The with_invariants construct gives us access to the invariant within the scope of at most one atomic step, preceded or succeeded by as many ghost or unobservable steps as needed.

The general form of with_invariants is as follows, to “open” invariants i_1 to i_k in the scope of e.

with_invariants i_1 ... i_k
returns x:t
ensures post
{ e }

In many cases, the returns and ensures annotations are omitted, since it can be inferred.

This is syntactic sugar for the following nest:

with_invariants i_1 {
 ...
  with_invariants i_k
  returns x:t
  ensures post
  { e }
 ...
}

Here’s the rule for opening a single invariant inv i p using with_invariant i { e } is as follows:

• i must have type iref and inv i p must be provable in the current context, for some p:vprop

• e must have the type stt_atomic t j (p ** r) (fun x -> p ** s x). [1] That is, e requires and restores the invariant p, while also transforming r to s x, all in at most one atomic step. Further, the name_of_inv i must not be in the set j.

• with_invariants i { e } has type stt_atomic t (add_inv i j) (inv i p ** r) (fun x -> inv i p ** s x). That is, e gets to use p for a step, and from the caller’s perspective, the context was transformed from r to s, while the use of p is hidden.

• Pay attention to the add_inv i j index on with_invariants: stt_atomic (or stt_ghost) computation is indexed by the names of all the invariants that it may open.

Let’s look at a few examples to see how with_invariants works.

atomic
fn update_ref_atomic (r:ref U32.t) (i:iref) (v:U32.t)
requires inv i (owns r)
ensures inv i (owns r)
opens (singleton i)
{
  with_invariants i {    //owns r
     unfold owns;        //ghost step;  exists* u. pts_to r u
     write_atomic r v;   //atomic step; pts_to r v
     fold owns;          //ghost step;  owns r
  }
}

[@@expect_failure]
```pulse
fn double_open_bad (r:ref U32.t) (i:inv (owns r))
requires emp
ensures pure False
{
    with_invariants i {
      with_invariants i {
        unfold owns;
        unfold owns;
        pts_to_dup_impossible r;
        fold owns;
        fold owns
      }
    }
}
```

fn update_ref (r:ref U32.t) (i:iref) (v:U32.t)
requires inv i (owns r)
ensures inv i (owns r)
{                    
  with_invariants i {    //owns r
     unfold owns;        //ghost step;  exists* u. pts_to r u
     write_atomic r v;   //atomic step; pts_to r v
     fold owns;          //ghost step;  owns r
  }
}

[@@expect_failure]
```pulse 
fn update_ref_fail (r:ref U32.t) (i:iref) (v:U32.t)
requires inv i (owns r)
ensures inv i (owns r)
{
  with_invariants i {
    unfold owns;
    r := v; //not atomic
    fold owns;
  }
}
```

- This computation is not atomic nor ghost. `with_invariants`
  blocks can only contain atomic computations.