First Pass

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 iff triple t H Q. The benefits of introducing weakest preconditions are twofold.

• The use of wp greatly reduces the number of structural rules required, thus reducing 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 CFML tool.

The high-level picture is:

• (1) wp and triples are equivalent presentations of the same thing.
• (2) wp has practical benefits, reducing the number of reasoning rules and tactics that are needed, by a fair amount.
• (3) specifications of functions remain more intuitive to read with triples.

The chapter presents:

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

Throughout the chapter, we aim to establish reasoning rules in wp-style directly with respect to the semantics defined by eval, as opposed to deriving wp-style rules from the reasoning rules on triples proved in the previous chapters. The interest is to present the proofs involved in the most direct construction of a program verification framework based on wp. 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.

Definition of Weakest Preconditions

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. It is 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 does. The concept of wp might seem a bit mysterious at this point. Hopefully it will become clearer in the rest of this chapter. The first critical observation is that wp is in fact nothing but a 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.

Remark: the reader may wonder why wp is not just defined to *be* eval, by simply modifying our earlier definition of eval to take its arguments in a different order. Certainly, it could be done. However, the benefits of identifying wp and eval are limited, and there are two orthogonal motivations for not following that route. Firstly, the omni-big-step predicate eval s t Q is devised as an immediate generalization of the big-step predicate eval s t s' v, by generalizing from out final configuration (s',v) to a set Q of final configurations. From the perspective of a semantics, we view the configuration (s,t) as an input and the set Q as an output, thus it would be fairly awckward to write eval t Q s, with the input state s taken as last argument. Secondly, we are looking here at a simple Separation Logic where heap predicates are predicates over the physical state. They have type heap→Prop, where heap corresponds exactly to the type of of a state s. More advanced Separation Logic feature something known as "ghost state" (used, e.g., to represent invariants associated with locks). In such logics, heap predicates are predicates over both the physical and the ghost state. In other words, the type heap in general may consist of more than just a state s. The point of this discussion is that, for more advanced Separation Logics, wp is more than just eval. Thus, there is no reason to attempt to identify the two. As intended, the entailment H ==> wp t Q holds if and only if triple t H Q does.

There are several other ways of defining wp. As we show near the end of this chapter, they are all equivalent. The definition 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 t with respect to the postcondition Q.

Second, wp t Q is the "weakest" of all valid preconditions for t and 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 the rule of consequence in weakest-precondition style. 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 mentioning triple.)

Looking at the entaileent expressed by wp_frame, the reader may wander whether the reverse entailment holds, that is, if wp t (Q \*+ H) entails (wp t Q) \* H. This reverse entailment does not hold in general. Consider the following counterexample term t, defined as let p = ref 1 in 0. This term returns 0 and produces a dangling reference cell that can be described as \∃ p, (p ~~> 1). Let Q be fun r ⇒ \[r = 0] and H be \∃ p, (p ~~> 1). The term t, executed in the empty heap, terminates with postcondition Q \*+ H. Therefore, the predicate wp t (Q \*+ H) holds of the empty heap. However, (wp t Q) \* H does not hold of the empty heap, because H, which describes one memory cell, cannot be carved out of the empty heap. We conclude that wp t (Q \*+ H) does not entail (wp t Q) \* H in general. The connection between wp_frame and the rule triple_frame is not be totally obvious. Recall the statement of the frame rule for triples.
    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 is 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₂.

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 triple t H Q with H ==> wp t Q to 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 the rule triple_hpure.

Replacing triple t H Q with H ==> wp t Q yields the following:

This implication is just a special case of the extraction lemma for pure facts on the left on an entailment, himpl_hstar_hpure_l:
    (P → (H ==> H')) →
    (\[P] \* H) ==> H'.

Similar reasoning applies to the extraction rule for existentials.

The Ramified Frame Rule

Recall the ramified frame rule:

The ramified frame rule in weakest-precondition style, named wp_ramified, admits a concise statement and subsumes all the 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. Concretely, prove wp_conseq using only wp_ramified or wp_ramified_trans, plus properties of the entailment relation.

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

Prove that wp_frame is derivable from wp_ramified. Concretely, prove wp_frame using only wp_ramified plus properties of entailment.

Reasoning Rules for Terms in Weakest-Precondition Style

Values

Recall the rule triple_val which establishes a triple for a value v.

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

Sequences

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

Replacing triple t H Q with H ==> wp t Q gives this:
      H ==> (wp t₁) (fun _ ⇒ 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 rule: 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.

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₁.

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 follows exactly the same pattern as for values.

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

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 A necessary and sufficient condition to prove a proposition of the form ∀ H, (H ==> H₁) → (H ==> H₂) is H₁ ==> H₂. Indeed, if we instantiate H with H₁, we have (H₁ ==> H₁) → (H₁ ==> H₂), thus we deduce H₁ ==> H₂. Reciprocally, if we have H₁ ==> H₂ and H ==> H₁, then by the transitivity property himpl_trans, we deduce H ==> H₂. Therefore, the previous entailment simplifies to:
    wp (if b then t₁ else t₂) Q ==> wp (trm_if (val_bool b) t₁ t₂) Q. This is the wp-style reasoning rule for conditionals.

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:

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 triple t H Q with 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 also own H; and if, furthermore, you can trade the combination of Q₁ and H against Q₂; then 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 might 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 literally, 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: use 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.

Equivalent 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

In this section, we show that specification triples can be presented in a different style using weakest preconditions. This style has appeared under the name "Texan triples" in certain work related to the Iris framework. The main motivation is to slighly simplify the implementation of the tactic xapp. The main drawback is that it makes specifications, one could argue, slightly less easy to read. For this reason, users of the Iris framework usually stick to the standard triple notation in their publications. Despite the readability issue, it may be interesting for the reader to be aware of the possibility of stating specifications directly using wp, as there might be useful applications of this technique in certain contexts.

1. An Example

Consider 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 a chain of transformations that can take us from the triple form to the wp form, and we 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 cast 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. Further Examples

The wp-style specifications 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 proof assistants, the Iris framework https://iris-project.org/),developed since 2015, prevasively exploits weakest preconditions to state reasoning rules. The developers of Iris and VST have advocated for this rule. The ramified frame rule was integrated in CFML 2.0 in 2018.