Steel: Selectors

Steel Semantics are based on Concurrent Separation Logic with refinements, expressed in the standard requires and ensures clauses. A typical Steel function signature looks like the following

val f (#a:Type) (r:ref a) : Steel unit
  // We expect the separation logic assertion ptr r
  (ptr r)
  // After execution, we provide the separation logic assertion ptr r
  (fun _ -> ptr r)
  // Pre- and postconditions refine the separation logic assertions
  (requires fun (h:mem) -> get_ref h r == 1)
  (ensures fun (h0:mem) _ (h1:mem) -> get_ref h1 r == 2)

Nevertheless, these pre- and postconditions come with an additional requirement, they need to be frameable. Informally, we need to prove that each condition depends only on the associated separation logic predicate. In the previous example, this means proving that get_ref h r depends only on ptr r. Although doable automatically for simple refinements, this clobbers the SMT context, and can become tricky once the complexity of specifications grow.

To this end, we provide an abstraction layer on top of the Steel effect using selectors. At a high-level, we associate to each separation logic predicate in our context a projection, that returns the value(s) that this predicate encapsulates. Instead of exposing the whole memory in the requires and ensures clauses, we then provide selectors that allow us to access the projection of each resource. We prove once and for all that a specification using selectors satisfies the depends_only_on requirement. This allows to abstract over this requirement using layered effects and avoid it leaking into the VCs passed to the SMT solver. Our previous example becomes roughly the following:

val f (#a:Type) (r:ref a) : Steel unit
  // We expect the separation logic assertion ptr r
  (ptr r)
  // After execution, we provide the separation logic assertion ptr r
  (fun _ -> ptr r)
  // Pre- and postconditions now operate on selectors
  (requires fun (h:selector (ptr r)) -> project h (ptr r) == 1)
  (ensures fun (h0:selector (ptr r)) _ (h1:selector (ptr r)) -> project h1 (ptr r) == 2)

Formal definition of selectors

Before defining selectors, we first need to define projections on slprops. To this end, we define viewables that enhance separation logic assertions to pack them with projections.

type projection' (a:Type) (fp:slprop) = hmem fp -> GTot a
type projection (a:Type) (fp:slprop) = f:projection' a fp{value_depends_only_on_fp f}

type viewable = {
  fp: slprop;
  a: Type;
  sel:projection a fp
}

A projection is a function indexed by a type a and an slprop fp that, given a memory where fp is valid returns the value of type a that fp encapsulates. To be valid, this projection must depend only on the memory fragment associated to fp. For instance, for a reference r:ref a, a natural projection is sel_ref:projection a (ptr r) = fun h -> get_ref h r which returns a value of type a. Projections are intended to be used for specification purposes only. We therefore give them the GTot type, which gives more flexibility to define projections on more complex datatypes.

It is worth noting that it is always possible to package an slprop into a viewable, even when the separation logic predicate does not encapsulate any meaningful value (for instance if it is a magic wand). We can define the associated projection to be fun h -> ().

From there, we can lift star from slprop to viewable by defining an inductive type. Using an inductive type gives us more flexibility for normalization, as we will see later.

type viewables =
| VUnit: viewable -> viewables
| VStar: viewables -> viewables -> viewables

let rec t_of (v:viewables) = match v with
| VUnit v -> v.t
| VStar v1 v2 -> (t_of v1, t_of v2)

let rec fp_of (v:viewables) = ...
let rec sel_of (v:viewables) = ...

A selector is a function parametrized by the viewables in the context that returns the projection of any subresource (lifting the notion of subresource from slprop as well).

let selector (r:viewables) =
  fun (r0:viewables{exists delta. r `equiv` r0 <*> delta}) -> GTot (t_of r0)

After defining projection, and viewables as an abstraction over slprop, we can now define a new Steel effect operating on viewables and selector on top of the previous effect (that we will refer to as SteelBasic here) that used slprop, and exposed mem for refinements.

TODO: Check with actual implementation + how to incorporate layered effects

effect Steel 
  (a:Type) 
  (fp0:viewables)
  (fp1:a -> viewables) 
  (pre:selector fp0 -> GTot prop) 
  (post:(selector fp0) -> (x:a) -> (selector (fp1 x)) -> GTot prop)
= SteelBasic a 
  (fp_of fp0) 
  (fun _ -> fp_of (fp1 x))
  (requires fun h -> pre (mk_selector h fp0))
  (ensures fun h0 x h1 -> post (mk_selector h0 fp0) x (mk_selector h1 (fp1 x)))

Lifting the frame rule to Steel

To implement programs using the new Steel effect, we need to lift standard operators, such as frame

Given a function val f: unit -> Steel a inner0 inner1 pre post, we want to call it from a larger initial context outer0 and final context outer1 such that outer0 is equivalent to inner0 <*> delta for some frame delta, and outer1 x is equivalent to inner1 x <*> delta for any returned value x.

First, types for pre and post need to be reconciled with what is expected in the larger context. pre has type selector inner0 -> GTot prop, but we require type selector outer0 -> GTot prop. To this end, we provide a restriction of selectors to a subresource that preserves all projections in the subresource:

let focus_selector 
  (#outer:viewables) (h:selector outer) 
  (inner:viewables{exists delta. outer `equiv` inner <*> delta}) 
  : (selector inner)
  = fun (r:viewables{exists delta. inner `equiv` r <*> delta}) -> h r

We can then implement the frame rule in Steel // TODO: Check the actual implementation

val frame
  (#outer:viewables)
  (#inner0:viewables)
  (#a:Type)
  (#inner1:a -> viewables)
  (#[resolve_frame()]
    delta:viewables{outer `equiv` inner0 <*> delta})
  (#pre:selector inner0 -> GTot prop)
  (#post:selector inner0 -> (x:a) -> selector (inner1 x) -> GTot prop)
  ($f:unit -> Steel a inner0 inner1 pre post)
  : Steel a
          outer
          (fun x -> inner1 x <*> delta)
          (fun h -> pre (focus_selector h inner0))
          (fun h0 x h1 -> 
             post (focus_selector h0 inner0) x (focus_selector h1 (inner1 x) /\
             expand_frame_equalities delta h0 h1
          )

It's worth pointing several things in this signature. First, we do not actually take outer1 as a parameter, but instead return the equivalent inner1 x <*> delta. In conjunction with how bind works for Steel and SteelBasic, this allows F* to automatically infer the outer resource in the context at each call of frame by unification from the postresource returned by the previous function call, or by the resource initially in the context if this is the first function call.

Second, the (simplified) resolve_frame annotation in the implicit delta automatically calls a tactic based on canonicalization inside commutative monoids to infer the frame.

Lastly, instead of framing a user-supplied predicate that would depend only on the resource delta, we automatically add to the SMT context (through expand_delta_equalities, defined below) that the projection of each subresource of delta is the same in the initial and final state. We then leave it to SMT reasoning to prove the preservation of predicates depending on delta.

let expand_delta_equalities (delta:viewables)
  (#outer0:viewables{exists delta'. outer0 `equiv` delta <*> delta'}) (h0:selector outer0)
  (#outer1:viewables{exists delta'. outer1 `equiv` delta <*> delta'}) (h1:selector outer1)
  = match delta with
  | VUnit v -> h0 v == h1 v
  | VStar v1 v2 -> expand_delta_equalities v1 h0 h1 /\ expand_delta_equalities v2 h0 h1

We voluntarily only add equalities for the atomic subresources (i.e. the ones stored in VUnit). This is a trade-off between completeness of the specification and saturation of the SMT context. At the moment, we believe that selectors would almost always be called with atomic subresources, hence equalities on composite resources would not be useful. Furthermore, we can always prove such equalities from equalities on atomic subresources, or package a composite resource into an atomic one when needed. We leave this flexibility to the user.

Crafting SMT-friendly VCs through fine-tuned normalization

To improve the efficiency of the solver, we make a heavy use of normalization to craft SMT-friendly Verification Conditions. Pre and postconditions in the definition of the Steel effect are encapsulated by a call to normal, which performs normalization on all terms with the attribute __reduce__. An especially useful instance is expand_delta_equalities. By normalization, we pass to the SMT a conjunction of equalities on subresources instead of a recursive function computing it.

// TODO: Experiment with the new Steel effect, and comment about good practices to have good normalization and tactics

A typical viewables library

TODO: Present a standard, slightly complex library + design choices, including what goes in the interface, what goes in the fst, what get the reduce attribute