Steel: Framing

This page presents the handling of the separation logic framing in Steel.

The frame rule is at the core of separation logic, enabling modular reasoning. In its simplest form, it is defined as follows: If a computation e admits the separation logic Hoare Triple {P} e {Q}, then a framed version {P * F} e {Q * F} is derivable for any frame F.

The composition rule is also standard: If we have two computations e1 and e2 with triples {P1} e1 {Q1} and {P2} e2 {Q2}, and if Q1 ==> P2, then the triple {P1} e1; e2 {Q2} is admissible.

In a simple setting, proving the equivalence of separation logic assertions (that we will name slprops from now on) is straightforward. Let us consider P = p_1 * p_2 * p_3 and Q = q_1 * q_2. (slprop, *, emp), where emp is the empty separation logic assertion forms a commutative monoid, hence any rearrangement of p_1, p_2, p_3, such as for instance p_3 * p_1 * p_2 is equivalent to P. As such, we can rearrange the slprops inside both P and Q in some canonical order, and then efficiently check whether q_1, q_2 is a subset of p_1, p_2, p_3. If so, we can conclude that P ==> Q.

Determining separation logic implication in Steel is unfortunately harder: slprops are dependently-typed, and they are also allowed to contain program implicits that have not yet been inferred. To simplify the problem, we will instead consider separation logic equivalence. Even though the separation logic in Steel is affine, we leave it to the user to explicitly drop unwanted slprops to derive an implication from an equivalence.

The rest of this page presents our (partial) decision procedure to automate frame inference, as well as program implicits resolution when used in slprops. First, we use layered effects to automatically insert frames when needed, and collect a list of separation logic constraints. These constraints are then deferred to a tactic, which chooses the next constraint to be solved, and calls a decision procedure attempting to prove equivalence. If this decision procedure succeeds, program implicits and frames in the constraint are resolved.

Collecting Separation Logic Constraints

Inserting frames during composition

Framing is often required when composing two computations, such as {P} e1 {Q} and {R} e2 {S}. We can frame e1 with an fp:slprop, and e2 with an fp':slprop to obtain {P * fp} e1; e2 {S * fp'} as long as Q * fp ==> R * fp'. For instance, if e1 and e2 are reads to two different references r1 and r2, we wish to automatically infer the triple {pts_to r1 * pts_to r2} read r1; read r2 {pts_to r1 * pts_to r2} in Steel.

But inserting a frame at each composition leads to having to infer many frames, and applying the frame rule several times to the same computation. For instance, when composing e1, e2 and e3, we would first add a frame for the composition of e2 and e3, and then another for the composition of e1 and e2; e3. Instead, we wish to only frame each computation once.

To distinguish between framed and not-yet framed computations, we define two effects SteelF and Steel. In the first case, computation types will be of the form SteelF a (pre * ?f) (fun x -> post x * ?f) where ?f:slprop is a metavariable to be solved. In the Steel case, computation types do not contain metavariables. SteelF is only intended as an internal artifact; users should always specify their functions using the Steel effect.

Polymonadic binds and subcomps

TODO: Show signatures, relation between the two effects from framing note

Important invariant: Apart from the return application, all SteelF functions have at most one metavariable.

Atomic subcomputations

When reasoning about concurrent programs and invariants, Steel relies on a model of total, atomic actions, which are a sub-language of Steel functions where general recursion is enabled. In the framework, atomic computations have their own effect SteelAtomic which is a subeffect of Steel.

The specifics of the SteelAtomic effect are orthogonal to the framing problem, and SteelAtomic and Steel share their separation logic structure. We define two effects SteelAtomic and SteelAtomicF similarly to Steel and SteelF with the appropriate polymonadic binds and subcomps. The separation logic constraints collected are identical to the ones for general Steel computations, and also deferred to the same tactic.

Scheduling Constraints during Solving

Goals deferred to the tactic are of three sorts: uvars to be inferred (for instance ?f:slprop), equalities due to the layered effects, and slprop equivalences due to framing and composition.

By definition of the effects, all framing uvars to be inferred appear in at least one equality or equivalence constraint. We thus first filter them out to present a proofstate with only constraints to be solved.

Removing indirections

Equalities are the most brittle constraints, and correspond to indirections in the layered effects. It is not sufficient for two slprops to be equivalent, they need to be definitionally equal for an equality constraint to be discharged. Therefore, they need to be solved first, to remove all indirections before deciding equivalence.

Given the calculus given previously, almost equalities are of the form ?u1 = ?u2 or ?u1 x = ?u2. Thanks to a recent change in the F* unifier, these equalities can all be solved without needlessly restricting the scopes of ?u1 or ?u2. The only exception occurs when returning a Pure value at the end of the function; the corresponding equality has the shape ?u1 x = ?u2 y, which might lead to scoping issues when trying to unify naively.

To circumvent this issue, we apply the following scheduling. We first remove indirections by solving all equalities but the one associated to a possible return, that we can identify thanks to its shape. We then solve the equivalence constraint in a subcomp application, therefore inferring the dependent slprop associated to the returned Pure value. We identify the subcomp constraints by annotating them in the effect definition. We finally solve the remaining return equalities to remove the last indirections.

Scheduling the next equivalence to solve

At this stage, we are left with only slprop equivalences to prove. Because all effectful functions require a top-level annotation, we can first ensure that the inferred computation type for the whole body matches the top-level annotation through subcomp. The corresponding constraint is solved first.

Once this is done, we traverse the list of constraints looking for one that contains at most one slprop metavariable. The existence of such a constraint relies on an invariant from our calculus: apart from constraints related to a return computation, specifications in SteelF contain at most one metavariable. Since we already solved the dependent slprop associated to the return previously, all constraints now have at most two slprops, one in each term in the equivalence.

Furthermore, after solving subcomp, the outermost constraint only contains at most one slprop. A forward symbolic execution would therefore give us a scheduling where each constraint has at most one slprop, which ensures that finding such a constraint by simply traversing the list is always possible.

Inferring implicits

Once we picked an equivalence constraint to solve, we need to decide whether the two terms are actually equivalent, inferring the implicits they might contain along the way.

We are attempting to decide whether two slprops p and q are equivalent. We first split p and q into their atomic subresources. If p = p_0 * p_1, we reify p as the list of "atoms" [0, 1] where 0 corresponds to p_0 and 1 to p_1. Similarly, if q = q_0 * q_1, we reify q as [2, 3]. If for instance p_0 and q_1 were exactly the same (not just unifiable, but syntactically equal), they would be associated to the same atom.

Denoting atoms as slprops.

When reifying slprops, we keep track in a map of what slprop each atom is associated to. Given a list of atoms l and such a map am, we thus can define a canonical denotation of l as an slprop as follows: let rec mdenote l am = match l with | [] -> emp | hd::tl -> (select hd am) * mdenote tl am

We prove once and for all that the result of the denotation is equivalent to the initial slprop before reification through Associative-Commutative rewriting. Similarly, we also prove that any permutation of the list l yields an equivalent denotation.

To prove that p and q are equivalent, we will now try to find permutations of their representations such that the corresponding denotations can be unified. Since atoms are simply natural numbers here, proving that a list of atoms is a permutation of another is straightforward: We can put both lists in canonical form (i.e. as sorted lists), use normalization to remove all intermediate function calls and reduce them to concrete lists, and check whether the two lists are equal.

Building appropriate permutations

We now need to create permutations of l1 and l2, the representations of p and q respectively, such that their denotations could be unified with each other. Our scheduler ensures that there is at most one slprop metavariable in p and q. We ensure that this metavariable can only ever occur in q, rewriting our goal using the symmetry of equivalence if needed.

We will keep two accumulators l1_del and l2_del which correspond to the atoms that have been handled already. The (implicitly) maintained invariant is that l1_del and l2_del can be unified at all times, and that l1_del@l1 (resp. l2_del@l2) is a permutation of the initial l1 (resp. l2) at all times.

Our first step is to check whether slprops in both p and q match exactly, i.e. if atoms are the same in both representations. This is done using the function trivial_cancels. If it is the case, we remove these atoms from the lists, and input them in l1_del and l2_del.

We now iterate over what remains in the lists l1 and l2. For each element in l1, we will try to find a candidate for unification in l2.

Looking for candidates (function try_candidates)

We consider the head of the list of l1, that corresponds to an t:slprop. Because of our scheduling invariant, we know that t is not a metavariable, but it might contain unresolved program implicits (for instance if it is pts_to r ?perm v).

We traverse the list l2, trying to unify t with all slprops in l2 which are not metavariables (as t should always be able to unify with the frame metavariable). Unification attempts are done in a separate context (using a try/with) which ensures that they do not pollute the current proofstate. We have three cases:

• t could only unify with one slprop: We found a unique candidate, we move t and the corresponding candidate to l1_del and l2_del respectively.
• t did not unify with any slprop in l2 : it should likely be part of the frame in l2
• t did unify with more than one slprops: we cannot conclude about the right candidate for t.

In the last two cases, we did not successfully find a unification candidate for t. We skip t for now, and will come back to it later; in the last case, it might be that another element in l1 might be a more restricted version of t, and will only have one possible candidate.

Iterating over l1 (function equivalent_lists')

For each element in l1, we try to find an appropriate candidate as defined in the previous subsection, moving the element and the associated candidate in l2 to l1_del and l2_del respectively when the search is successful.

During our iteration, we have several cases to consider:

• If l1 is empty, we found equivalent terms for all elements in p. If l2 is also empty, we are done. If l2 only contains one element, which happens to be the frame metavariable, we are also done as it can be unified with emp. In all other cases, there are leftover slprops in l2, and we raise an error.
• If l1 is not empty, but l2 only contains one element which happens to be the frame metavariable, we are also done: All slprops left in l1 are the frame in l2.
• Else, we try to traverse the whole of l1. While doing this traversal, either we find a candidate for some element in l1, thus reducing l1, or we do not make any progress, and fail; more annotations are required from the user.

Adding Implicit Dynamic Frames

TODO

Core idea: implicit dynamic frames equalities depend on the slprops. We separate the goals, solve the ones related to slprops and can then solve the ones related to implicit dynamic frames with straightforward unification using an appropriate scheduling.

Known Issues

Refinement subtyping

Assume p: n:even -> slprop

Unification through trefl of n:nat, _:squash (is_even n) |- p 2 == ?u fails because trefl is called without smt on.

This can happen if for instance we have f (n:even) : SteelT unit (p n) (fun _ -> ...), but call it with let n:nat = 2 in f 2.

A workaround would be let n:even = 2 in f 2: If we have exactly the right type, unification succeeds. But this can become verbose and tedious quickly.

TODO: Try Guido's patch: We consider as valid candidates for unification terms that unify, but with some purely logical facts remaining left for SMT. When finally calling trefl after the permutations were built, we call it with smt on to discharge such logical facts, enabling refinement subtyping.

slprop arguments based on pattern matching

Happens often when considering references to PCMs. A PCM will often have its compose that relies on a pattern matching.

If compose appears in one of the slprop indices, unification will fail. If we have for instance pts_to r (compose v0 v1) == pts_to r (compose ?u1 ?u2) as a constraint, trefl will unfold compose. Again, without SMT, unification will fail because it will not be able to prove that all branches in both cases match.

TODO: Try Guido's patch? Not sure if it would help here. It might just better to be careful in the style of Steel functions we propose.

No Steel <: Steel subcomp:

We currently do not support a framing subcomp from Steel to Steel. There was some limitation in layered effects about adding a frame, this was conflicting with the if_then_else combinator

slprop-dependent pattern matching

TODO: One example is if_then_else (see the cond combinator), but it's something more general in pattern matching when the Steel signatures might depend on the branches.

Better handling of Pure values?: TODO, to investigate