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.