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

• Constraints language
• Two effect system

Scheduling Constraints during Solving

• First indirection eqs
• Subcomp for return slprop
• Return eq
• Scheduling of the rest of the constraints

Inferring implicits

• Go over tactic

Adding Implicit Dynamic Frames

• Separate the goals, solve them next

Known Issues

• Refinement subtyping
• Normalization of functions containing pattern matching
• No Steel <: Steel subcomp