# SLFWPsem

Set Implicit Arguments.

From SLF (* Sep *) Require Export SLFRules.

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types v : val.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

# Chapter in a rush

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

- 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,
- (optional) alternative, equivalent definitions for wp, and alternative proofs for deriving wp-style reasoning rules.

## Notion of weakest precondition

Parameter wp : trm → (val→hprop) → hprop.

Parameter wp_equiv : ∀ t H Q,

(H ==> wp t Q) ↔ (triple t H Q).

The wp t Q is called "weakest precondition" for two reasons:
because (1) it is a precondition, and (2) it is the weakest one,
as we explain next.
First, wp t Q is always a "valid precondition" for a
triple associated with the term t and the postcondition Q.

Lemma wp_pre : ∀ t Q,

triple t (wp t Q) Q.

Proof using. intros. rewrite <- wp_equiv. applys himpl_refl. Qed.

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

Lemma wp_weakest : ∀ t H Q,

triple t H Q →

H ==> wp t Q.

Proof using. introv M. rewrite wp_equiv. applys M. Qed.

In other words, wp t Q is the "smallest" H satisfying
triple t H Q with respect to the order on heap predicates
induced by the entailment relation ==>.
There are several equivalent ways to define wp, as we show
in the optional contents of this chapter. It turns out that
the equivalence (H ==> wp t Q) ↔ (triple t H Q) fully
characterizes the predicate wp, and that it is all we need
to carry out formal reasoning.
For this reason, we postpone to further on in this chapter the
description of alternative, direct definitions for wp.

## Structural rules in weakest-precondition style

### The frame rule

The lemma is proved by exploiting the frame rule for triples
and the equivalence that characterizes wp.

The connection with the frame might not be totally obvious.
Recall the frame rule for triples.

triple t H

triple t (H
Let us replace the form triple t H Q with the form
H ==> wp t Q. We obtain the following statement.

triple t H

_{1}Q →triple t (H

_{1}\* H) (Q \*+ H)
If we exploit transitivity of entailment to eliminate H

_{1}, then we obtain exactly wp_frame, as illustrated by the proof script below.### The rule of consequence

Lemma wp_conseq : ∀ t Q

_{1}Q

_{2},

Q

_{1}===> Q

_{2}→

wp t Q

_{1}==> wp t Q

_{2}.

Proof using.

introv M. rewrite wp_equiv. applys× triple_conseq (wp t Q

_{1}) M. applys wp_pre.

Qed.

The connection with the rule of consequence is, again, not
totally obvious. Recall the rule of consequence for triples.

triple t H

H

Q

triple t H
Let us replace the form triple t H Q with the form H ==> wp t Q.
We obtain the following statement:

triple t H

_{1}Q_{1}→H

_{2}==> H_{1}→Q

_{1}===> Q_{2}→triple t H

_{2}Q_{2}Lemma wp_conseq_trans : ∀ t H

_{1}H

_{2}Q

_{1}Q

_{2},

H

_{1}==> wp t Q

_{1}→

H

_{2}==> H

_{1}→

Q

_{1}===> Q

_{2}→

H

_{2}==> wp t Q

_{2}.

If we exploit transitivity of entailment to eliminate H

_{1}and H_{2}, then we obtain exactly wp_conseq, as illustrated below.### The extraction rules

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.

(P → (H ==> H')) →

(\[P] \* H) ==> H'.

Proof using. introv M. applys himpl_hstar_hpure_l M. Qed.

A similar reasoning applies to the extraction rule for existentials.

### Rule for values

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.

H ==> Q v →

H ==> wp (trm_val v) Q.

Lemma wp_val : ∀ v Q,

Q v ==> wp (trm_val v) Q.

Proof using.

intros. rewrite wp_equiv. applys× triple_val.

Qed.

We can verify that, when migrating to the wp presentation, we have
not lost any expressiveness. To that end, we prove that triple_val is
derivable from wp_val.

Lemma triple_val_derived_from_wp_val : ∀ v H Q,

H ==> Q v →

triple (trm_val v) H Q.

Proof using. introv M. rewrite <- wp_equiv. xchange M. applys wp_val. Qed.

Parameter triple_seq : ∀ t

_{1}t

_{2}H Q H

_{1},

triple t

_{1}H (fun v ⇒ H

_{1}) →

triple t

_{2}H

_{1}Q →

triple (trm_seq t

_{1}t

_{2}) H Q.

Replacing triple t H Q with H ==> wp t Q throughout the rule
gives the statement below.

H ==> (wp t

H

H ==> wp (trm_seq t
This entailment holds for any H and H
This leads us to the following statement, which reads as follows:
if you own a state from which the evaluation of t

H ==> (wp t

_{1}) (fun v ⇒ H_{1}) →H

_{1}==> (wp t_{2}) Q →H ==> wp (trm_seq t

_{1}t_{2}) Q._{1}. Let us specialize it to H_{1}:= (wp t_{2}) Q and H := (wp t_{1}) (fun v ⇒ (wp t_{2}) Q)._{1}produces a state from which the evaluation of t_{2}produces the postcondition Q, then you own a state from which the evaluation of the sequence t_{1};t_{2}produces Q.Lemma wp_seq : ∀ t

_{1}t

_{2}Q,

wp t

_{1}(fun v ⇒ wp t

_{2}Q) ==> wp (trm_seq t

_{1}t

_{2}) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_seq.

{ rewrite× <- wp_equiv. }

{ rewrite× <- wp_equiv. }

Qed.

#### Exercise: 2 stars, standard, optional (triple_seq_from_wp_seq)

Check that wp_seq is just as expressive as triple_seq, by proving that triple_seq is derivable from wp_seq and from the structural rules for wp and/or the structural rules for triple.Lemma triple_seq_from_wp_seq : ∀ t

_{1}t

_{2}H Q H

_{1},

triple t

_{1}H (fun v ⇒ H

_{1}) →

triple t

_{2}H

_{1}Q →

triple (trm_seq t

_{1}t

_{2}) H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

### Rule for functions

_{1}, which evaluates to the value val_fun x t

_{1}.

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

Lemma wp_fun : ∀ x t Q,

Q (val_fun x t) ==> wp (trm_fun x t) Q.

Proof using. intros. rewrite wp_equiv. applys× triple_fun. Qed.

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

Lemma wp_fix : ∀ f x t Q,

Q (val_fix f x t) ==> wp (trm_fix f x t) Q.

Proof using. intros. rewrite wp_equiv. applys× triple_fix. Qed.

Parameter triple_if : ∀ b t

_{1}t

_{2}H Q,

triple (if b then t

_{1}else t

_{2}) H Q →

triple (trm_if (val_bool b) t

_{1}t

_{2}) H Q.

Replacing triple using wp entailments yields:

H ==> wp (if b then t

H ==> wp (trm_if (val_bool b) t
which simplifies by transitivity to:

wp (if b then t
This statement corresponds to the wp-style reasoning rule
for conditionals. The proof appears next.

H ==> wp (if b then t

_{1}else t_{2}) Q →H ==> wp (trm_if (val_bool b) t

_{1}t_{2}) Q.wp (if b then t

_{1}else t_{2}) Q ==> wp (trm_if (val_bool b) t_{1}t_{2}) Q.Lemma wp_if : ∀ b t

_{1}t

_{2}Q,

wp (if b then t

_{1}else t

_{2}) Q ==> wp (trm_if (val_bool b) t

_{1}t

_{2}) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_if. rewrite× <- wp_equiv.

Qed.

Parameter triple_let : ∀ x t

_{1}t

_{2}H Q Q

_{1},

triple t

_{1}H Q

_{1}→

(∀ v, triple (subst x v t

_{2}) (Q

_{1}v) Q) →

triple (trm_let x t

_{1}t

_{2}) H Q.

The rule of trm_let x t

_{1}t_{2}is very similar to that for trm_seq, the only difference being the substitution of x by v in t_{2}, where v denotes the result of t_{1}.Lemma wp_let : ∀ x t

_{1}t

_{2}Q,

wp t

_{1}(fun v ⇒ wp (subst x v t

_{2}) Q) ==> wp (trm_let x t

_{1}t

_{2}) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_let.

{ rewrite× <- wp_equiv. }

{ intros v. rewrite× <- wp_equiv. }

Qed.

### Rule for function applications

_{1}) v

_{2}.

Parameter triple_app_fun : ∀ x v

_{1}v

_{2}t

_{1}H Q,

v

_{1}= val_fun x t

_{1}→

triple (subst x v

_{2}t

_{1}) H Q →

triple (trm_app v

_{1}v

_{2}) H Q.

The corresponding wp rule is stated and proved next.

Lemma wp_app_fun : ∀ x v

_{1}v

_{2}t

_{1}Q,

v

_{1}= val_fun x t

_{1}→

wp (subst x v

_{2}t

_{1}) Q ==> wp (trm_app v

_{1}v

_{2}) Q.

Proof using.

introv EQ

_{1}. rewrite wp_equiv. applys× triple_app_fun.

rewrite× <- wp_equiv.

Qed.

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

The lemma wp_equiv captures the characteristic property of wp,
that is, (H ==> wp t Q) ↔ (triple t H Q) .
However, it does not give evidence that there exists a predicate wp
satisfying this equivalence. We next present one possible definition.
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.

First, let us prove that wp t Q is itself a valid precondition,
in the sense that triple t (wp t Q) Q always holds (as asserted
by the lemma wp_pre).
To establish this fact, we have to prove:
triple t (\∃ H, H \* \[triple t H Q]) Q.
Applying the extraction rule for existentials gives:
∀ H, triple t (H \* \[triple t H Q]) Q.
Applying the extraction rule for pure facts gives:
∀ H, (triple t H Q) → (triple t H Q), which is true.
Second, let us demonstrate that the heap predicate wp t Q
is entailed by any precondition H that satisfies triple t H Q,
as asserted by the lemma wp_weakest.
Assume triple t H Q. Let us prove H ==> wp t Q, that is
H ==> \∃ H, H \* \[triple t H Q]. Instantiating the
H on the right-hand side as the H from the left-hand side
suffices to satisfy the entailment.
Recall that the properties wp_pre and wp_weakest were derivable
from the characteristic equivalence triple t H Q ↔ H ==> wp Q.
Thus, to formalize the proofs of wp_pre and wp_weakest, all we
have to do is to establish that equivalence.

#### Exercise: 2 stars, standard, recommended (wp_equiv)

Prove that the definition wp_high satisfies the characteristic equivalence for weakest preconditions.Lemma wp_equiv : ∀ t H Q,

(H ==> wp t Q) ↔ (triple t H Q).

Proof using. (* FILL IN HERE *) Admitted.

☐

## Equivalence between all definitions of wp

_{1}and wp

_{2}to both satisfy the characteristic equivalence. We prove that they are equal.

Lemma wp_unique : ∀ wp

_{1}wp

_{2},

(∀ t H Q, (triple t H Q) ↔ (H ==> wp

_{1}t Q)) →

(∀ t H Q, (triple t H Q) ↔ (H ==> wp

_{2}t Q)) →

wp

_{1}= wp

_{2}.

Proof using.

introv M

_{1}M

_{2}. applys fun_ext_2. intros t Q. applys himpl_antisym.

{ rewrite <- M

_{2}. rewrite M

_{1}. auto. }

{ rewrite <- M

_{1}. rewrite M

_{2}. auto. }

Qed.

Recall that both wp_pre and wp_weakest are derivable from
wp_equiv. Let us also that, reciprocally, wp_equiv is derivable
from the conjunction of wp_pre and wp_weakest.
In other words, the property of "being the weakest precondition"
also uniquely characterizes the definition of wp.

Lemma wp_from_weakest_pre : ∀ wp',

(∀ t Q, triple t (wp' t Q) Q) → (* wp_pre *)

(∀ t H Q, triple t H Q → H ==> wp' t Q) → (* wp_weakest *)

(∀ t H Q, H ==> wp' t Q ↔ triple t H Q). (* wp_equiv *)

Proof using.

introv M

_{1}M

_{2}. iff M.

{ applys triple_conseq M

_{1}M. auto. }

{ applys M

_{2}. auto. }

Qed.

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 that 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.
Technically, wp t Q can be defined as:
fun (h:heap) ⇒ triple t (fun h' ⇒ h' = h) Q.
In other words, the precondition requires the input heap
to be exactly h.

One can prove that this definition of wp also satisfies the
characteristic equivalence H ==> wp Q ↔ triple t H Q.

The details of the proofs are given for the reference but are
beyond the scope of this course. Technically, the proof exploits
the lemma triple_named_heap which was established as an exercise
in the appendix of the chapter SLFHimpl.)

Proof using.

unfold wp. iff M.

{ applys triple_named_heap. intros h K.

applys triple_conseq (fun h' ⇒ h' = h) Q.

{ specializes M K. applys M. }

{ intros ? →. auto. }

{ applys qimpl_refl. } }

{ intros h K. applys triple_conseq M.

{ intros h' →. applys K. }

{ applys qimpl_refl. } }

Qed.

End WpLowLevel.

Parameter triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ x, triple t (J x) Q) →

triple t (\∃ x, J x) Q.

Replacing triple t H Q with H ==> wp t Q yields the
lemma stated below.

#### Exercise: 1 star, standard, optional (triple_hexists_in_wp)

Prove the extraction rule for existentials in wp style.Lemma triple_hexists_in_wp : ∀ t Q A (J:A→hprop),

(∀ x, (J x ==> wp t Q)) →

(\∃ x, J x) ==> wp t Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

Parameter triple_conseq_frame : ∀ H

_{2}H

_{1}Q

_{1}t H Q,

triple t H

_{1}Q

_{1}→

H ==> H

_{1}\* H

_{2}→

Q

_{1}\*+ H

_{2}===> Q →

triple t H Q.

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, recommended (wp_conseq_frame_trans)

Prove the combined structural rule in wp style. Hint: exploit wp_conseq_trans and wp_frame.Lemma wp_conseq_frame_trans : ∀ t H H

_{1}H

_{2}Q

_{1}Q,

H

_{1}==> wp t Q

_{1}→

H ==> H

_{1}\* H

_{2}→

Q

_{1}\*+ H

_{2}===> Q →

H ==> wp t Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

_{1}and you own H, and if you can trade the combination of Q

_{1}and H against Q

_{2}, the you own a piece of state from which the execution of t produces Q

_{2}.

#### Exercise: 2 stars, standard, recommended (wp_conseq_frame)

Prove the concise version of the combined structural rule in wp style. Many proofs are possible.Lemma wp_conseq_frame : ∀ t H Q

_{1}Q

_{2},

Q

_{1}\*+ H ===> Q

_{2}→

(wp t Q

_{1}) \* H ==> (wp t Q

_{2}).

Proof using. (* FILL IN HERE *) Admitted.

☐

We have established the following rule for reasoning about
conditionals using wp.

Parameter wp_if : ∀ b t

_{1}t

_{2}Q,

wp (if b then t

_{1}else t

_{2}) Q ==> wp (trm_if b t

_{1}t

_{2}) Q.

Equivalently, the rule may be stated with the conditional around
the calls to wp t

_{1}Q and wp t_{2}Q.#### Exercise: 1 star, standard, optional (wp_if')

Prove the alternative statement of rule wp_if, either from wp_if or directly from triple_if.Lemma wp_if' : ∀ b t

_{1}t

_{2}Q,

(if b then (wp t

_{1}Q) else (wp t

_{2}Q)) ==> wp (trm_if b t

_{1}t

_{2}) Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

## Definition of wp directly from hoare

Recall the definition of triple in terms of hoare.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').
In what follows, we conduct the proofs by assuming a concrete definition
for wp, namely wp_high, which lends itself better to automated proofs.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').

First, we check the equivalence between triple t H Q and H ==> wp t Q.
This proof is the same as wp_equiv from the module WpHighLevel
given earlier in this chapter.

Lemma wp_equiv : ∀ t H Q,

(H ==> wp t Q) ↔ (triple t H Q).

Proof using.

unfold wp. iff M.

{ applys× triple_conseq Q M.

applys triple_hexists. intros H'.

rewrite hstar_comm. applys× triple_hpure. }

{ xsimpl× H. }

Qed.

Second, we prove the consequence-frame rule associated with wp.
It is the only structural rule that is needed for working with
weakest preconditions.

Lemma wp_conseq_frame : ∀ t H Q

_{1}Q

_{2},

Q

_{1}\*+ H ===> Q

_{2}→

(wp t Q

_{1}) \* H ==> (wp t Q

_{2}).

The proof leverages the consequence rule for hoare triples,
and the frame property comes from the ∀ H' quantification
baked in the definition of triple.

Proof using.

introv M. unfold wp. xpull. intros H' N. xsimpl (H' \* H).

unfolds triple. intros H''. specializes N (H \* H'').

applys hoare_conseq N. { xsimpl. } { xchange M. }

Qed.

Third and last, we establish reasoning rules for terms in wp-style
directly from the corresponding rules for hoare triples.
The proof details are beyond the scope of this course.
The point here is to show that the proofs are fairly concise.

Lemma wp_val : ∀ v Q,

Q v ==> wp (trm_val v) Q.

Proof using.

intros. unfold wp. xsimpl. intros H'. applys hoare_val. xsimpl.

Qed.

Lemma wp_fun : ∀ x t Q,

Q (val_fun x t) ==> wp (trm_fun x t) Q.

Proof using.

intros. unfold wp. xsimpl. intros H'. applys hoare_fun. xsimpl.

Qed.

Lemma wp_fix : ∀ f x t Q,

Q (val_fix f x t) ==> wp (trm_fix f x t) Q.

Proof using.

intros. unfold wp. xsimpl. intros H'. applys hoare_fix. xsimpl.

Qed.

Lemma wp_if : ∀ b t

_{1}t

_{2}Q,

wp (if b then t

_{1}else t

_{2}) Q ==> wp (trm_if b t

_{1}t

_{2}) Q.

Proof using.

intros. unfold wp. xsimpl. intros H M H'.

applys hoare_if. applys M.

Qed.

Lemma wp_seq : ∀ t

_{1}t

_{2}Q,

wp t

_{1}(fun v ⇒ wp t

_{2}Q) ==> wp (trm_seq t

_{1}t

_{2}) Q.

Proof using.

intros. unfold wp. xsimpl. intros H' M

_{1}. intros H''. applys hoare_seq.

{ applys M

_{1}. }

{ repeat rewrite hstar_hexists. applys hoare_hexists; intros H'''.

rewrite (hstar_comm H'''). repeat rewrite hstar_assoc.

applys hoare_hpure. intros M

_{2}. applys hoare_conseq M

_{2}. xsimpl. xsimpl. }

Qed.

Lemma wp_let : ∀ x t

_{1}t

_{2}Q,

wp t

_{1}(fun v ⇒ wp (subst x v t

_{2}) Q) ==> wp (trm_let x t

_{1}t

_{2}) Q.

Proof using.

intros. unfold wp. xsimpl. intros H' M

_{1}. intros H''. applys hoare_let.

{ applys M

_{1}. }

{ intros v. simpl. repeat rewrite hstar_hexists.

applys hoare_hexists. intros H'''.

rewrite (hstar_comm H'''). repeat rewrite hstar_assoc.

applys hoare_hpure. intros M

_{2}. applys hoare_conseq M

_{2}. xsimpl. xsimpl. }

Qed.

Lemma wp_app_fun : ∀ x v

_{1}v

_{2}t

_{1}Q,

v

_{1}= val_fun x t

_{1}→

wp (subst x v

_{2}t

_{1}) Q ==> wp (trm_app v

_{1}v

_{2}) Q.

Proof using.

introv EQ

_{1}. unfold wp. xsimpl. intros H' M. intros H''. applys× hoare_app_fun.

Qed.

Lemma wp_app_fix : ∀ f x v

_{1}v

_{2}t

_{1}Q,

v

_{1}= val_fix f x t

_{1}→

wp (subst x v

_{2}(subst f v

_{1}t

_{1})) Q ==> wp (trm_app v

_{1}v

_{2}) Q.

Proof using.

introv EQ

_{1}. unfold wp. xsimpl. intros H' M. intros H''. applys× hoare_app_fix.

Qed.

Remark: it is technically possible to bypass even the definition of
triple and specify all functions directly using the predicate wp.
However, using triple leads to better readability of specifications,
thus it seems preferable to continue using that style for specifying
functions. (See discussion in chapter SLFWand, appendix on "Texan
triples".)