Atomic Operations and Invariants

Creating an invariant

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

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

let owns (x:ref U32.t) = exists* v. pts_to x v

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

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

Importantly, when we turn pts_to r x into inv (owns r), we lose ownership of pts_to r x. Remember, once we have inv (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 (owns r), we can clearly break the invariant, e.g., by freeing r.

val new_invariant (p:vprop)
: stt_unobservable (inv p) emp_inames p (fun _ -> emp)

Opening an invariant

Now that we’ve allocated an inv (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 i:inv p using with_invariant i { e } is as follows:

• i must have type inv p, 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) r s. 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_unobservable) 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.

1

Note, e may also have type stt_unobservable t j (p ** r) (fun x -> p ** s x), in which case with_invariant i { e } has type stt_unobservable t (add_inv i j) r s.

atomic
fn update_ref_atomic (r:ref U32.t) (i:inv (owns r)) (v:U32.t)
requires emp
ensures emp
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:inv (owns r)) (v:U32.t)
requires emp
ensures emp
{                    
  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:inv (owns r)) (v:U32.t)
requires emp
ensures emp
{
  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.