This post discusses two ways of writing the Bind rule of Separation Logic. They are logically equivalent, but in practice, one should choose wisely between them.

The Bind rule of Separation Logic is the rule that allows reasoning about a sequence of two instructions. In the statements that follow, such a sequence takes the form bind m1 m2.

There are several ways of writing this rule. The form that is traditionally used in the Hoare logic community has two premises, along the following lines:

  WP m1 {{ φ }} -∗
  (∀ v, φ v -∗ WP (m2 v) {{ ψ }}) -∗
  WP (bind m1 m2) {{ ψ }}.

This means that, to verify the program bind m1 m2, one must first verify the subprogram m1 and establish that, when m1 terminates, some property φ holds. Then, under the assumption that φ holds when the execution of m2 begins, one must prove that it is safe to run m2. It is up to the user to choose or guess the logical assertion φ that describes the intermediate state.

The form that is most often used in the Iris community has only one premise:

  WP m1 {{ λ v, WP (m2 v) {{ ψ }} }} -∗
  WP (bind m1 m2) {{ ψ }}.

This means that, to verify the program bind m1 m2, one must first verify establish that, when m1 terminates, it is safe to run m2.

These two forms of the Bind rule are logically equivalent. The second form follows from the first one by instantiating φ with λ v, WP (m2 v) {{ ψ }}. Conversely, the first form follows from the second one and from the Consequence rule of Separation Logic.

Which form is preferable?

Does this mean that the two forms of the Bind rule are interchangeable? Not quite; there are practical reasons for preferring one over the other.

The second form can seem preferable because it does not require guessing or choosing a suitable postcondition φ. Indeed, it automatically uses the most permissive φ, which is λ v, WP (m2 v) {{ ψ }}. Thus, this form may seem as though it is more amenable to automation.

However, this second form comes with a caveat. If the verification of the subprogram m1 involves a case analysis, then it is usually desirable to limit the scope of this case analysis to just m1. In other words, the scope of the case analysis must not encompass m2, because that would imply that m2 must be verified several times.

Because the first form of the Bind rule introduces two subgoals (one for m1 and one for m2), the scope of a case analysis inside m1 is naturally limited to the first subgoal. The second form of the Bind rule does not have this property: because it has just one premise, a user who naively performs a case analysis while verifying m1 ends up having to verify m2 several times.

In summary, if m1 is a conditional construct (e.g., an if or match construct) then the middle point between m1 and m2 is a join point and the first form of the Bind rule, where the user must provide φ, should be preferred. Otherwise, the second form of the Bind rule can be used and there is no need for the user to provide φ.

This is not a deep remark. It is just a possibly-useful reminder that two logically equivalent statements can have quite different qualities in practical usage scenarios.