First Pass

In previous chapters, we have introduced the notion of Separation Logic triple, written triple t H Q. In this chapter, we introduce the notion of "weakest precondition" for Separation Logic triples, written wp t Q. The intention is for wp t Q to be a heap predicate (of type hprop) such that H ==> wp t Q if and only if triple t H Q holds. The benefits of introducing weakest preconditions is two-fold.

• The use of wp greatly reduces the number of structural rules required, and thus reduces accordingly the number of tactics required for carrying out proofs in practice;
• The predicate wp will serve as guidelines for setting up in the next chapter a "characteristic formula generator", which is the key ingredient at the heart of the implementation of the CFML tool.

This chapter presents:

• the notion of weakest precondition, as captured by wp,
• the reformulation of structural rules in wp-style,
• the reformulation of reasoning rules in wp-style,

The "optional material" section presents several equivalent definitions for wp, alternative proofs for deriving wp-style reasoning rules, as well as a presentation of "Texan triples", which reformulate function specifications using magic wands instead of triples.

Notion of Weakest Precondition

Consider a term t and a postcondition Q. The expression wp t Q is called the "weakest precondition" of the term t with respect to the postcondition Q. This weakest precondition consists of a heap predicate such that, for any heap predicate H, the entailment H ==> wp t Q holds if and only if triple t H Q holds. The notion of wp might sound very mysterious at this point. Hopefully, it will become clearer through the reading of this chapter. The first critical observation is that wp is in fact nothing but a mere reformulation of the predicate eval. To see why, recall the definition of triple t H Q.
    Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
      ∀ s, H s → eval s t Q. By definition, the predicate wp should be such that H ==> wp t Q is equivalent to triple t H Q. But H ==> wp t Q unfolds to ∀ s, H s → wp t Q s. If we compare ∀ s, H s → eval s t Q with ∀ s, H s → wp t Q s, we see that wp t Q s should match eval s t Q. In other words, wp t Q should correspond to fun s ⇒ eval s t Q.

There exists several other ways of defining wp. As we show near the end of this chapter, they are all equivalent. The definition considered above is the one that leads to the simplest proofs for the reasoning rules. Indeed, reasoning rules must be proved correct with respect to the semantics, and the semantics is captured by the predicate eval. Let us now explain why wp is called a "weakest precondition". First, wp t Q is always a "valid precondition" for a triple associated with the term t and the postcondition Q.

Second, wp t Q is the "weakest" of all valid preconditions for the term t and the postcondition Q, in the sense that, for any other valid precondition H (i.e., such that triple t H Q holds), it is the case that H entails wp t Q.

Structural Rules in Weakest-Precondition Style

We next present reformulations of the frame rule and of the rule of consequence in "weakest-precondition style". Thereafter, given a term t and a postcondition Q, we say that "t produces Q" if t terminates and produces a output value and an output state that, together, satisfy the postcondition Q.

The Frame Rule

The frame rule for wp asserts that (wp t Q) \* H entails wp t (Q \*+ H). This statement can be read as follows: if you own both a piece of state satisfying H and a piece of state in which the execution of t produces Q, then you own a piece of state in which the execution of t produces Q \*+ H, that is, produces both Q and H.

The lemma is proved by exploiting the frame property on eval. (It could also be derived using wp_equiv and triple_frame, but the point here is to derive properties of wp without involving triple.)

The connection with the frame rule for triples might not be totally obvious. Recall the statement of the frame rule.
    triple t H₁ Q →
    triple t (H₁ \* H) (Q \*+ H) Let us replace the pattern triple t H Q with the pattern H ==> wp t Q, following the characteristic equivalence wp_equiv. We obtain the statement shown below.

If we exploit transitivity of entailment to eliminate H₁, then we obtain exactly wp_frame, as illustrated by the proof script below.

The Rule of Consequence

The rule of consequence for wp materializes as a covariance property: it asserts that wp t Q is covariant in Q. In other words, if Q₁ entails Q₂, then wp t Q₁ entails wp t Q₂. The corresponding formal statement appears next.

Here again, the connection with the corresponding reasoning rule for triples is not totally obvious. Recall the statement of the rule of consequence.
    triple t H₁ Q₁ →
    H₂ ==> H₁ →
    Q₁ ===> Q₂ →
    triple t H₂ Q₂ Let us replace the form triple t H Q with the form H ==> wp t Q. We obtain the following statement:

If we exploit transitivity of entailment to eliminate H₁ and H₂, then we obtain exactly wp_conseq, as illustrated by the proof script below.

The Extraction Rules

The extraction rules triple_hpure and triple_hexists have no specific counterpart with the wp presentation. Indeed, in a weakest-precondition style presentation, the extraction rules for triples correspond exactly to the extraction rules for entailment. To see why, consider for example the rule triple_hpure.

Replacing the form triple t H Q with H ==> wp t Q yields the following statement.

The above implication is just a special case of the extraction lemma for pure facts on the left on an entailment, named himpl_hstar_hpure_l, and whose statement is as follows.
    (P → (H ==> H')) →
    (\[P] \* H) ==> H'. Instantiating H' with wp t Q proves triple_hpure_with_wp.

A similar reasoning applies to the extraction rule for existentials.

The Ramified Frame Rule

Recall the ramified frame rule.

The ramified frame rule admits in weakest-precondition style, named wp_ramified. This rule admits a concise statement and subsumes all other structural rules of Separation Logic. Its very elegant statement is as follows.

The following reformulation of wp_ramified can be more practical to exploit in practice, because it applies to any goal of the form H ==> wp t Q.

Exercise: 3 stars, standard, especially useful (wp_conseq_of_wp_ramified)

Prove that wp_conseq is derivable from wp_ramified. To that end, prove the statement of wp_conseq by using only wp_ramified or wp_ramified_trans, and properties of the entailement relation.

Exercise: 3 stars, standard, especially useful (wp_frame_of_wp_ramified)

Prove that wp_frame is derivable from wp_ramified. To that end, prove the statement of wp_frame by using only wp_ramified and properties of the entailement relation.

Reasoning Rules for Terms, in Weakest-Precondition Style

Rule for Values

Recall the rule triple_val which gives a reasoning rule for establishing a triple for a value v.

If we rewrite this rule in wp style, we obtain the rule below.
    H ==> Q v →
    H ==> wp (trm_val v) Q. By exploiting transitivity of entailment, we can eliminate H. We obtain the following statement, which reads as follows: if you own a state satisfying Q v, then you own a state from which the evaluation of the value v produces Q.

Rule for Sequence

Recall the reasoning rule for a sequence trm_seq t₁ t₂.

Replacing triple t H Q with H ==> wp t Q throughout the rule gives the statement below.
      H ==> (wp t₁) (fun v ⇒ H₁) →
      H₁ ==> (wp t₂) Q →
      H ==> wp (trm_seq t₁ t₂) Q. This entailment holds for any H and H₁. Let us specialize it to H₁ := (wp t₂) Q and H := (wp t₁) (fun v ⇒ (wp t₂) Q). This leads us to the following statement, which reads as follows: if you own a state from which the evaluation of t₁ produces a state from which the evaluation of t₂ produces the postcondition Q, then you own a state from which the evaluation of the sequence t₁;t₂ produces Q.

Rule for Let-Bindings

Recall the reasoning rule for a term trm_let x t₁ t₂.

The rule of trm_let x t₁ t₂ is very similar to that for trm_seq, the only difference being the substitution of x by v in t₂, where v denotes the result of t₁.

Rule for Functions

Recall the reasoning rule for a term trm_fun x t₁, which evaluates to the value val_fun x t₁.

The rule for functions follow exactly the same pattern as for values.

A similar rule holds for the evaluation of a recursive function.

Rule for Conditionals

Recall the reasoning rule for a term triple_if b t₁ t₂.

Replacing triple using wp entailments yields:
    H ==> wp (if b then t₁ else t₂) Q →
    H ==> wp (trm_if (val_bool b) t₁ t₂) Q. which simplifies by transitivity to:
    wp (if b then t₁ else t₂) Q ==> wp (trm_if (val_bool b) t₁ t₂) Q. This statement corresponds to the wp-style reasoning rule for conditionals. The proof appears next.

Equivalently, the rule may be stated with the conditional around the calls to wp t₁ Q and wp t₂ Q.

Exercise: 1 star, standard, optional (wp_if')

Prove the alternative statement of rule wp_if, either from wp_if or directly from eval_if.

Rule For Function Applications

Recall the reasoning rule for an application (val_fun x t₁) v₂.

The corresponding wp rule is stated and proved next.

A similar rule holds for the application of a recursive function.

More Details

Combined Structural Rule

Recall the combined consequence-frame rule for triple.

Let us reformulate this rule using wp, replacing the form triple t H Q with the form H ==> wp t Q.

Exercise: 2 stars, standard, especially useful (wp_conseq_frame_trans)

Prove the combined structural rule in wp style. Hint: exploit wp_conseq_trans and wp_frame.

The combined structural rule for wp can actually be stated in a more concise way. The rule reads as follows: if you own a state from which the execution of t produces (a result and a state satisfying) Q₁ and you own H, and if you can trade the combination of Q₁ and H against Q₂, the you own a piece of state from which the execution of t produces Q₂.

Exercise: 2 stars, standard, especially useful (wp_conseq_frame)

Prove the concise version of the combined structural rule in wp style. Many proofs are possible.

Let us reformulate the rule wp_conseq_frame using a magic wand. The premise Q₁ \*+ H ===> Q₂ can be rewritten as H ==> (Q₁ \−−∗ Q₂). By replacing H with Q₁ \−−∗ Q₂ in the conclusion of wp_conseq_frame, we obtain the ramified rule for wp.
Lemma wp_ramified : ∀ t Q₁ Q₂,
  (wp t Q₁) \* (Q₁ \−−∗ Q₂) ==> (wp t Q₂). This explaination suggests how one may have come up with the statement of the ramified frame rule.

Optional Material

Weakest Preconditions Derived from Triples, a First Route

The lemma wp_equiv captures the characteristic property of wp, that is, (H ==> wp t Q) ↔ (triple t H Q). The predicate wp can be defined in terms of eval, like triple. Interestingly, wp may also be defined in terms of triple. The idea is to define wp t Q as the predicate \∃ H, H \* \[triple t H Q], which, reading litterally, is satisfied by "any" heap predicate H which is a valid precondition for a triple for the term t and the postcondition Q.

Exercise: 3 stars, standard, especially useful (wp_equiv_1)

Prove that the alternative definition wp_1 satisfies the characteristic equivalence for weakest preconditions. Hint: the proof exploits the consequence rule and the extraction rules.

Weakest Preconditions Derived From Triples, a Second Route

The concrete definition for wp given above is expressed in terms of Separation Logic combinators. In contrast to this "high level" definition, there exists a more "low level" definition, expressed directly as a function over heaps. In this alternative definition, the heap predicate wp t Q is defined as a predicate that holds of a heap h if and only if the execution of t starting in exactly the heap h produces the post-condition Q. The latter statement is formally captured as triple t (fun h' ⇒ h' = h) Q. The low-level definition of wp is thus as shown below.

Exercise: 4 stars, standard, optional (wp_equiv_2)

Prove that the low-level definition wp_2 also satisfies the characteristic equivalence H ==> wp Q ↔ triple t H Q. Hint: exploit the lemma triple_named_heap which was established as an exercise in the chapter Triples.

Characterizations of wp

First, we establish that the equivalence (triple t H Q) ↔ (H ==> wp t Q) defines a unique predicate wp. In other words, all possible definitions of wp are equivalent to each another. Thus, it really does not matter which concrete definition of wp we consider: they are all equivalent. Concretely, assume two predicates wp₁ and wp₂ to both satisfy the characteristic equivalence. We prove that they are equal.

Second, we establish that the property of "being the weakest precondition" also uniquely characterizes the definition of wp. This property is the conjunction of two facts: wp t Q must be a valid precondition for a triple involving t and Q; and wp t Q must be entailed by any valid precondition of a triple involving t and Q. These two facts correspond to wp_pre and wp_weakest.

Exercise: 2 stars, standard, especially useful (wp_equiv_iff_wp_pre_and_wp_weakest)

Prove that the conjunction of the properties wp_pre and wk_weakest is equivalent to the property wp_equiv.

Texan Triples

1. Example of Texan Triples

In this section, we show that specification triples can be presented in a different style using weakest preconditions. Consider for example the specification triple for allocation.

This specification may be equivalently reformulated in the form of an entailment, as shown below. Note that we purposely leave an empty heap predicate at the front to indicate where the precondition, if it were not empty, would go in the reformulation.

In what follows, we describe the chain of transformation that can take us from the triple form to the wp form, and establish the reciprocal. Afterwards, we will formalize the general pattern of the translation from a triple to a "texan triple", that is, to a wp-based specification. By replacing triple t H Q with H ==> wp t Q, the specification triple_ref can be reformulated as follows.

We wish to cast the RHS in the form wp (val_ref v) Q for an abstract postcondition Q. To that end, we reformulate the above statement by including a magic wand relating the postcondition (funloc p ⇒ p ~~> v) with Q.

This statement can be made slightly more readable by unfolding the definition of the magic wand for postconditions. Doing so amounts to quantifying explicitly on the result, named r.

Interestingly, the variable r, which is equal to val_loc p, can now be substituted away, further increasing readability. We obtain the specification of val_ref in "Texan triple style".

2. The General Pattern

Most specification triples can be casted in the form: triple t H (fun r ⇒ ∃ x₁ .. xN, \[r = v] \* H'). In such a specification:

• the value v may depend on the xi variables,
• the heap predicate H' may depend on r and the xi,
• the number of existentials xi may vary, possibly be zero,
• the equality \[r = v] may be removed if no pure fact is needed about r.

Such a specification triple of the form triple t H (fun r ⇒ ∃ x₁ xN, \[r = v] \* H' can be be reformulated as the Texan triple: (\∀ x₁ xN, H \−∗ Q v) ==> wp t Q. We next formalize the equivalence between the two presentations, for the specific case where the specification involves a single auxiliary variable, named x. The statement below makes it explicit that v may depend on x, and that H may depend on r and x.

3. Other Examples

The wp-style specification of ref, get and set are presented next.

Alternatively, the specifications of set and free may advertize that the output value is the unit value.

4. Exercise

Let us put to practice the use of a Texan triple on a different example. Recall the function incr and its specification (from Hprop.v).

Exercise: 3 stars, standard, especially useful (wp_incr)

State a Texan triple for incr as a lemma called wp_incr, then prove this lemma from triple_incr.

Historical Notes

The idea of weakest precondition was introduced by [Dijstra 1975] in his seminal paper "Guarded Commands, Nondeterminacy and Formal Derivation of Programs". Weakest preconditions provide a reformulation of Floyd-Hoare logic. Numerous practical verification tools leverage weakest preconditions, e.g. ESC/Java, Why3, Boogie, Spec, etc. In the context of Separation Logic in a proof assistant, the Iris framework https://iris-project.org/), developed since 2015, prevasively exploits weakest preconditions to state reasoning rules. Developers of the tools VST and Iris have advertised for the interest of this rule. The ramified frame rule was integrated in CFML 2.0 in 2018. Texan triples have been used in certain Iris-based formalizations.