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.

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
• Normalization of functions containing pattern matching
• No Steel <: Steel subcomp