Higher Order Functions

Pulse Computation Types

Here’s perhaps the simplest higher-order function: apply abstracts function application.

fn apply (#a:Type0)
         (#b:a -> Type0)
         (#pre:a -> vprop)
         (#post: (x:a -> b x -> vprop))
         (f: (x:a -> stt (b x) (pre x) (fun y -> post x y)))
         (x:a)
requires pre x
returns y:b x
ensures post x y
{
  f x
}

This function is polymorphic in the argument, result type, pre, and post-condition of a function f, which it applies to an argument x. This is the first time we have written the type of a Pulse function as an F* type. So far, we have been writing signatures of Pulse functions, using the fn/requires/ensures notation, but here we see that the type of Pulse function is of the form:

x:a -> stt b pre (fun y -> post)

where,

• like any F* function type, Pulse functions are dependent and the right hand side of the arrow can mention x

• immediately to the right of the arrow is a Pulse computation type tag, similar to F*’s Tot, or GTot, etc.

• The tag stt is the most permissive of Pulse computation type tags, allowing the function’s body to read and write the state, run forever etc., but with pre-condition pre, return type b, and post-condition fun y -> post.

Pulse provides several other kinds of computation types. For now, the most important is the constructor for ghost computations. We show below apply_ghost, the analog of apply but for ghost functions.

ghost
fn apply_ghost 
         (#a:Type0)
         (#b:a -> Type0)
         (#pre:a -> vprop)
         (#post: (x:a -> b x -> vprop))
         (f: (x:a -> stt_ghost (b x) emp_inames (pre x) (fun y -> post x y)))
         (x:a)
requires pre x
returns y:b x
ensures post x y
{
  f x
}

The type of f is similar to what we had before, but this time we have:

• computation type tag stt_ghost, indication that this function reads or writes ghost state only, and always terminates.

• the return type is b x

• the next argument is emp_inames, describes the set of invariants that a computation may open, where emp_inames means that this computation opens no invariants. For now, let’s ignore this.

• the precondition is pre x and the postcondition is fun y -> post x y.

val stt (a:Type u#a) (i:inames) (pre:vprop) (post: a -> vprop)
  : Type u#0

val stt_ghost (a:Type u#a) (i:inames) (pre:vprop) (post: a -> vprop)
  : Type u#4

Counters

For a slightly more interesting use of higher order programming, let’s look at how to program a mutable counter. We’ll start by defining the type ctr of a counter.

noeq
type ctr = {
    inv: int -> vprop;
    next: i:erased int -> stt int (inv i) (fun y -> inv (i + 1) ** pure (y == reveal i));
    destroy: i:erased int -> stt unit (inv i) (fun _ -> emp)
}

A counter packages the following:

• A predicate inv on the state, where inv i states that the current value of the counter is i, without describing exactly how the counter’s state is implemented.

• A stateful function next that expects the inv i, returns the current value i of the counter, and provides inv (i + 1).

• A stateful function destroy to deallocate the counter.

One way to implement a ctr is to represent the state with a heap-allocated reference. This is what new_counter does below:

fn new_counter ()
requires emp
returns c:ctr
ensures c.inv 0
{
    open Pulse.Lib.Box;
    let x = alloc 0;
    fn next (i:erased int)
    requires pts_to x i 
    returns j:int
    ensures pts_to x (i + 1) ** pure (j == reveal i)
    {
        let j = !x;
        x := j + 1;
        j
    };
    fn destroy (i:erased int)
    requires pts_to x i
    ensures emp
    {
       free x
    };
    let c = { inv = pts_to x; next; destroy };
    rewrite (pts_to x 0) as (c.inv 0);
    c
}

Here’s how it works.

First, we allocate a new heap reference x initialized to 0.

Pulse allows us to define functions within any scope. So, we define two local functions next and destroy, whose implementations and specifications are straightforward. The important bit is that they capture the reference x:box int in their closure.

Finally, we package next and destroy into a c:ctr, instantiating inv to Box.pts_to x, rewrite the context assertion to c.inv 0, and return c.

In a caller’s context, such as test_counter below, the fact that the counter is implemented using a single mutable heap reference is completely hidden.

fn test_counter ()
requires emp
ensures emp
{
    let c = new_counter ();
    let next = c.next;
    let destroy = c.destroy;
    let x = next _; //FIXME: Should be able to write c.next
    assert pure (x == 0);
    let x = next _;
    assert pure (x == 1);
    destroy _;
}