Steel: surface language

The Steel project, whose scope is described in Elements of Low* v3 and explained in Steel, has moved forward a lot during the summer of 2019. The backend of Low* v3 now includes the following elements :

• A library for managing permissions;
• LowStar.Array, a redefinition of the underlying LowStar.Monotonic.Buffer that uses the permissions, with share, merge operations. Arrays with different permission ids are now disjoint, and new split and glue operations that split a buffer into two sub-parts left and right of an arbitrary index return two new loc_disjoint pointers; LowStar.Monotonic.Buffer should still be expressible using LowStar.Array for backwards compability
• The LowStar.RST monad, an abstraction over ST for resource-based reasoning about stateful programs.
• LowStar.RST.Array, a resource abstraction over LowStar.Array to expose the new permission-specific and split-glue operations in a idiomatic separation-logic-compatible way;

Users are expected to use mainly the LowStar.RST.Array library to implement and prove programs in the RST monad. However, such code currently is cumbersome to write, especially when framing is required. Hence, we propse syntax extensions to F* that could be elaborated to Low* v3 backend constructs, and ease the writing of programs in Low* v3.

Inferring the list of resources in context

A Low* v3 program is a function with the RST effect. The RST effect expects to know what resources are in the context, which are actually the memory footprint of the function. A typical backend program would look like that for now:

val f : x: a -> y: b -> z: c -> RST d
  (to_resource x <*> to_resource y <*> to_resource z)
  (fun ret -> to_resource ret <*> to_resource x <*> to_resource y <*>)

let f x y z = 
  rst_frame 
    (to_resource x <*> to_resource y <*> to_resource z) // Specifies resources initially in the context
    (to_resource x <*> to_resource y) // Resources in context after framed execution
    (fun _ -> dealloc z);
  let ret = rst_frame 
    (to_resource x <*> to_resource y)
    (to_resource ret <*> to_resource x <*> to_resource y)
    (fun _ -> create ()) 
  in
  ret

dealloc and create are themselves RST functions that operate on a smaller footprint, and the rst_frame call is here to help F* select the small footprint from the big resource context. The frame is automatically inferred by tactic, and framed resources are ensured to be unmodified. However, you can see a lot of redundancy in the arguments of rst_frame : The first argument is the resource context at this point of the program. Can this resource be made implicit by F*, for instance by being a part of the RST monad ? The second argument, which is the resource context after the function call, can be inferred: the resource context after the function is just delta <*> r_after_func where delta is the framed resource unmodified by the function call and r_after_func is the resource context returned by the called function.

These two elements should reduce the arguments of rst_frame to only the function call. Then, we can propose a syntax extension that would resemble a C-like function call:

foobar::(arg1, arg2, arg3)

instead of

rst_frame (fun _ -> foobar arg1 arg2 arg3)

It is worth noting that the rst_frame combinator would be used at each function call, even when no framing occurs. Even when nothing is framed, rst_frame might be needed for AC rewriting of starred resources in the presence of multiple arguments.

Reasoning about resource permissions

We want RST functions signatures to characterize the permissions of the resources they take as arguments and that they return. Currently, permissions are specified in the pre and post of the RST effect because they depend on the heap. This is cumbersome:

val f : (x: a) -> (y: b )-> (z: c) -> (n: U32.t) -> RST (ret: t)
  (to_resource_a x <*> to_resource_b y <*> to_resource_c z)
  (to_resource_t ret <*> to_resource_b x <*> to_resource_c y)
  (requires h0 -> get_perm h0 (to_resource x) < 1.0R /\ get_perm h1 (to_resource_c) = 1.0R) 
  (ensures h0 ret h1 -> sel (to_resource_b y) h0 == sel (to_resource_b y) h1)

Here is the syntax we want to be able to use, using the old and new selectors that restrict pre and post conditions to only talking about the resources and not the entire heap:

val f: (x: &res_a) -> (y: res_b) -> (z: res_c) -> (n: U32.t) -> RST (ret: res_t)
  (consumes (z)) // For multiple use <*> ? Or a list ?
  (requires old -> full_perm (old z))
  (ensures old ret new -> old y = new y)

Note that we no longer have the to_resource function. Instead, we have the res_a, res_b and res_c type which all should be instantiations of a resource typeclass that provides the <*> operation, the view, the inv. It is up to res_a to provide a method for retrieving the buffer or the pointer behind it if you want.

The backend should infer the aggregate of all the resources in the arguments for the "resources before" clause. For the "resources after" part, the backend will do a frame delta, removing what is in the (optional) consumes clause and adding whatever resource is returned by the function. If you want to return a tuple then we need to provide helpers like res_pair res0_t res1_t that will instantiate the typeclass correctly from multiple instantiations.

Then you have the qualifier for shared resources, "&". "&" means that the permission is above 0 (liveness) and strictly under 1, and that its value is the same in h0 and h1. Why do we add "strictly under 1" ? Because then we don't have to specify that the sel of the resource is conserved by the function. This is an opinionated choice, that will actually force the programmer to share the full resource before calling the function. But the claim is that will force the programmer to explicitly specify that most of the resources are untouched by the function, which greatly increase code readability. "&" will correspond to the most classic situation of a read-only buffer in a function, hence its special syntactic treatment.

y: res_b or z: res_c doesn't provide any information on the permission, other than it is strictly above 0: you have to specify it in the pre and post.

Sharing elaboration

Right now, resource sharing is done via an explicit function call. However, we could introduce a syntactic sugar for scoped sharing that doesn't require you to call merge explicitely:

with x' = &x, &y {
  CODE
}

You can choose to bind the second sharing pointer to a new variable or not, if you don't use it. Indeed, inside CODE you will be able to use both x' and x who will have half the original permission of x. For y, you can still use it inside CODE, but only with half of its original permission. The other half will be restored to y at the end of the scope. Because we expect a lot of functions to require "&" arguments, a lot of sharing will have to be done at function call. We can provide a special syntax for that:

let x0 = foobar::(&y, &z) in ...

Effectively translating in the backend to:

let x0 = with &y, &z {
  foobar y z
} in ...

Local mutable variables

We can go for a syntax like:

var x : U32.t = 0;
x1 = !x;
x := x1 + 1;

This could be elaborated in the backend to a specific map of local mutable variables. But if we elaborate it to a standard pointer resource, then we can do with x' = &x { ... } and allow permission manipulations on those local variables.

For a model of mutable local variables separate from resources, see: https://github.com/FStarLang/FStar/blob/0bbd0cc90345d8b969582405c3bc6aa5a8f62f33/examples/lowstar_resources/LocalVariables.fst