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.

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
}

Frame rule

Crafting SMT-friendly VCs through fine-tuned normalization