# WPsemSemantics of Weakest Preconditions

Set Implicit Arguments.

From SLF Require Export Rules.

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types v w : val.

Implicit Types p : loc.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

From SLF Require Export Rules.

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types v w : val.

Implicit Types p : loc.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

# First Pass

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

## Notion of Weakest Precondition

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.

Definition wp (t : trm) (Q : val→hprop) : hprop :=

fun s ⇒ eval s t Q.

Lemma wp_equiv : ∀ t H Q,

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

Proof using.

iff M. { introv Hs. applys M Hs. } { introv Hs. applys M Hs. }

Qed.

fun s ⇒ eval s t Q.

Lemma wp_equiv : ∀ t H Q,

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

Proof using.

iff M. { introv Hs. applys M Hs. } { introv Hs. applys M Hs. }

Qed.

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.

Lemma wp_pre : ∀ t Q,

triple t (wp t Q) Q.

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

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

Lemma wp_weakest : ∀ t H Q,

triple t H Q →

H ==> wp t Q.

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

triple t H Q →

H ==> wp t Q.

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

## Structural Rules in Weakest-Precondition Style

### The Frame Rule

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

Proof using.

intros. unfold wp. intros h HF.

lets (h

subst. applys eval_conseq.

{ applys eval_frame M

{ xsimpl. intros h' →. applys M

Qed.

intros. unfold wp. intros h HF.

lets (h

_{1}&h_{2}&M_{1}&M_{2}&MD&MU): hstar_inv (rm HF).subst. applys eval_conseq.

{ applys eval_frame M

_{1}MD. }{ xsimpl. intros h' →. applys M

_{2}. }Qed.

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

triple t H

triple t (H

triple t H

_{1}Q →triple t (H

_{1}\* 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

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

_{1}entails Q

_{2}, then wp t Q

_{1}entails wp t Q

_{2}. The corresponding formal statement appears next.

Lemma wp_conseq : ∀ t Q

Q

wp t Q

Proof using. unfold wp. introv M. intros s Hs. applys* eval_conseq. Qed.

_{1}Q_{2},Q

_{1}===> Q_{2}→wp t Q

_{1}==> wp t Q_{2}.Proof using. unfold wp. introv M. intros s Hs. applys* eval_conseq. Qed.

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

H

Q

triple t H

triple t H

_{1}Q_{1}→H

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

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

_{2}Q_{2}Let us replace the form triple t H Q with the form H ==> wp t Q. We obtain the following statement:
Lemma wp_conseq_trans : ∀ t H

H

H

Q

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 by the proof script 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'. Instantiating H' with wp t Q proves triple_hpure_with_wp.

A similar reasoning applies to the extraction rule for existentials.

Parameter triple_ramified_frame : ∀ H

triple t H

H ==> H

triple t H Q.

_{1}Q_{1}t H Q,triple t H

_{1}Q_{1}→H ==> H

_{1}\* (Q_{1}\−−∗ Q) →triple t H Q.

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.

Lemma wp_ramified : ∀ t Q

(wp t Q

Proof using. intros. applys wp_conseq_frame. applys qwand_cancel. Qed.

_{1}Q_{2},(wp t Q

_{1}) \* (Q_{1}\−−∗ Q_{2}) ==> (wp t Q_{2}).Proof using. intros. applys wp_conseq_frame. applys qwand_cancel. Qed.

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.

Lemma wp_ramified_trans : ∀ t H Q

H ==> (wp t Q

H ==> (wp t Q

Proof using. introv M. xchange M. applys wp_ramified. Qed.

_{1}Q_{2},H ==> (wp t Q

_{1}) \* (Q_{1}\−−∗ Q_{2}) →H ==> (wp t Q

_{2}).Proof using. introv M. xchange M. applys wp_ramified. Qed.

#### 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.
Lemma wp_conseq_of_wp_ramified : ∀ t Q

Q

wp t Q

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

☐

_{1}Q_{2},Q

_{1}===> Q_{2}→wp t Q

_{1}==> wp t Q_{2}.Proof using. (* FILL IN HERE *) Admitted.

☐

#### 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.
Lemma wp_frame_of_wp_ramified : ∀ t H Q,

(wp t Q) \* H ==> wp t (Q \*+ H).

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

☐

(wp t Q) \* H ==> wp t (Q \*+ H).

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

☐

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

Lemma wp_val : ∀ v Q,

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

Proof using. unfold wp. intros. intros h K. applys* eval_val. Qed.

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

Proof using. unfold wp. intros. intros h K. applys* eval_val. Qed.

Parameter triple_seq : ∀ t

triple t

triple t

triple (trm_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 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. This entailment holds for any H and H_{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

wp t

Proof using. unfold wp. intros. intros h K. applys* eval_seq. Qed.

_{1}t_{2}Q,wp t

_{1}(fun v ⇒ wp t_{2}Q) ==> wp (trm_seq t_{1}t_{2}) Q.Proof using. unfold wp. intros. intros h K. applys* eval_seq. Qed.

Parameter triple_let : ∀ x t

triple t

(∀ v

triple (trm_let x t

_{1}t_{2}Q_{1}H Q,triple t

_{1}H Q_{1}→(∀ v

_{1}, triple (subst x v_{1}t_{2}) (Q_{1}v_{1}) 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

wp t

Proof using. unfold wp. intros. intros h K. applys* eval_let. Qed.

_{1}t_{2}Q,wp t

_{1}(fun v_{1}⇒ wp (subst x v_{1}t_{2}) Q) ==> wp (trm_let x t_{1}t_{2}) Q.Proof using. unfold wp. intros. intros h K. applys* eval_let. Qed.

### 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. unfold wp. intros. intros h K. applys* eval_fun. Qed.

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

Proof using. unfold wp. intros. intros h K. applys* eval_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. unfold wp. intros. intros h K. applys* eval_fix. Qed.

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

Proof using. unfold wp. intros. intros h K. applys* eval_fix. Qed.

Parameter triple_if : ∀ b t

triple (if b then t

triple (trm_if (val_bool 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

wp (if b then t

H ==> wp (if b then t

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

_{1}t_{2}) Q. which simplifies by transitivity to:wp (if b then t

_{1}else t_{2}) Q ==> wp (trm_if (val_bool b) t_{1}t_{2}) Q. This statement corresponds to the wp-style reasoning rule for conditionals. The proof appears next.
Lemma wp_if : ∀ b t

wp (if b then t

Proof using. unfold wp. intros. intros h K. applys* eval_if. Qed.

_{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. unfold wp. intros. intros h K. applys* eval_if. Qed.

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 eval_if.
Lemma wp_if' : ∀ b t

(if b then (wp t

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

☐

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

☐

### Rule For Function Applications

_{1}) v

_{2}.

Parameter triple_app_fun : ∀ x v

v

triple (subst x v

triple (trm_app 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

v

wp (subst x v

Proof using. unfold wp. intros. intros h K. applys* eval_app_fun. Qed.

_{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. unfold wp. intros. intros h K. applys* eval_app_fun. Qed.

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

Lemma wp_app_fix : ∀ f x v

v

wp (subst x v

Proof using. unfold wp. intros. intros h K. applys* eval_app_fix. Qed.

_{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. unfold wp. intros. intros h K. applys* eval_app_fix. Qed.

Parameter triple_conseq_frame : ∀ H

triple t H

H ==> H

Q

triple t H Q.

_{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, especially useful (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

H

H ==> H

Q

H ==> wp t Q.

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

☐

_{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, especially useful (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

Q

(wp t Q

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

☐

_{1}Q_{2},Q

_{1}\*+ H ===> Q_{2}→(wp t Q

_{1}) \* H ==> (wp t Q_{2}).Proof using. (* FILL IN HERE *) Admitted.

☐

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

_{2}can be rewritten as H ==> (Q

_{1}\−−∗ Q

_{2}). By replacing H with Q

_{1}\−−∗ Q

_{2}in the conclusion of wp_conseq_frame, we obtain the ramified rule for wp.

Lemma wp_ramified : ∀ t Q

_{1}Q

_{2},

(wp t Q

_{1}) \* (Q

_{1}\−−∗ Q

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

_{2}). This explaination suggests how one may have come up with the statement of the ramified frame rule.

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.
Lemma wp_equiv_1 : ∀ t H Q,

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

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

☐

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

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

☐

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.
Lemma wp_equiv_2 : ∀ t H Q,

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

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

☐

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

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

☐

## Characterizations of wp

_{1}and wp

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

Lemma wp_unique : ∀ wp

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

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

wp

Proof using.

introv M

{ rewrite <- M

{ rewrite <- M

Qed.

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

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.
Lemma wp_equiv_iff_wp_pre_and_wp_weakest : ∀ 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. (* FILL IN HERE *) Admitted.

☐

( (∀ 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. (* FILL IN HERE *) Admitted.

☐

### 1. Example of Texan Triples

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.

Lemma wp_ref_0 : ∀ v,

\[] ==> wp (val_ref v) (funloc p ⇒ p ~~> v).

Proof using. intros. rewrite wp_equiv. applys triple_ref. Qed.

\[] ==> wp (val_ref v) (funloc p ⇒ p ~~> v).

Proof using. intros. rewrite wp_equiv. applys triple_ref. Qed.

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.

Lemma wp_ref_1 : ∀ Q v,

((funloc p ⇒ p ~~> v) \−−∗ Q) ==> wp (val_ref v) Q.

Proof using. intros. xchange (wp_ref_0 v). applys wp_ramified. Qed.

((funloc p ⇒ p ~~> v) \−−∗ Q) ==> wp (val_ref v) Q.

Proof using. intros. xchange (wp_ref_0 v). applys wp_ramified. Qed.

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.

Lemma wp_ref_2 : ∀ Q v,

(\∀ r, (\∃ p, \[r = val_loc p] \* p ~~> v) \−∗ Q r)

==> wp (val_ref v) Q.

Proof using. intros. applys himpl_trans wp_ref_1. xsimpl. Qed.

(\∀ r, (\∃ p, \[r = val_loc p] \* p ~~> v) \−∗ Q r)

==> wp (val_ref v) Q.

Proof using. intros. applys himpl_trans wp_ref_1. xsimpl. Qed.

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

Lemma wp_ref_3 : ∀ Q v,

(\∀ p, (p ~~> v) \−∗ Q (val_loc p)) ==> wp (val_ref v) Q.

Proof using.

intros. applys himpl_trans wp_ref_2. xsimpl. intros ? p →.

xchange (hforall_specialize p).

Qed.

(\∀ p, (p ~~> v) \−∗ Q (val_loc p)) ==> wp (val_ref v) Q.

Proof using.

intros. applys himpl_trans wp_ref_2. xsimpl. intros ? p →.

xchange (hforall_specialize p).

Qed.

### 2. The General Pattern

_{1}.. 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.

_{1}xN, \[r = v] \* H' can be be reformulated as the Texan triple: (\∀ x

_{1}xN, H \−∗ Q v) ==> wp t Q.

Lemma texan_triple_equiv : ∀ t H A (Hof:val→A→hprop) (vof:A→val),

(triple t H (fun r ⇒ \∃ x, \[r = vof x] \* Hof r x))

↔ (∀ Q, H \* (\∀ x, Hof (vof x) x \−∗ Q (vof x)) ==> wp t Q).

Proof using.

intros. rewrite <- wp_equiv. iff M.

{ intros Q. xchange M. applys wp_ramified_trans.

xsimpl. intros r x →.

xchange (hforall_specialize x). }

{ applys himpl_trans M. xsimpl¬. }

Qed.

(triple t H (fun r ⇒ \∃ x, \[r = vof x] \* Hof r x))

↔ (∀ Q, H \* (\∀ x, Hof (vof x) x \−∗ Q (vof x)) ==> wp t Q).

Proof using.

intros. rewrite <- wp_equiv. iff M.

{ intros Q. xchange M. applys wp_ramified_trans.

xsimpl. intros r x →.

xchange (hforall_specialize x). }

{ applys himpl_trans M. xsimpl¬. }

Qed.

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

Lemma wp_get : ∀ v p Q,

(p ~~> v) \* (p ~~> v \−∗ Q v) ==> wp (val_get p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_get. } { applys himpl_refl. } { xsimpl. intros ? →. auto. }

Qed.

Lemma wp_set : ∀ v w p Q,

(p ~~> v) \* (\∀ r, p ~~> w \−∗ Q r) ==> wp (val_set p w) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_set. } { applys himpl_refl. }

{ intros r. xchange (hforall_specialize r). xsimpl. }

Qed.

Lemma wp_free : ∀ v p Q,

(p ~~> v) \* (\∀ r, Q r) ==> wp (val_free p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_free. } { applys himpl_refl. }

{ intros r. xchange (hforall_specialize r). }

Qed.

(p ~~> v) \* (p ~~> v \−∗ Q v) ==> wp (val_get p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_get. } { applys himpl_refl. } { xsimpl. intros ? →. auto. }

Qed.

Lemma wp_set : ∀ v w p Q,

(p ~~> v) \* (\∀ r, p ~~> w \−∗ Q r) ==> wp (val_set p w) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_set. } { applys himpl_refl. }

{ intros r. xchange (hforall_specialize r). xsimpl. }

Qed.

Lemma wp_free : ∀ v p Q,

(p ~~> v) \* (\∀ r, Q r) ==> wp (val_free p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_free. } { applys himpl_refl. }

{ intros r. xchange (hforall_specialize r). }

Qed.

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

Parameter triple_set' : ∀ w p v,

triple (val_set p w)

(p ~~> v)

(fun r ⇒ \[r = val_unit] \* p ~~> w).

Lemma wp_set' : ∀ v w p Q,

(p ~~> v) \* (p ~~> w \−∗ Q val_unit) ==> wp (val_set p w) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_set'. }

{ applys himpl_refl. }

{ xsimpl. intros ? →. auto. }

Qed.

Parameter triple_free' : ∀ p v,

triple (val_free p)

(p ~~> v)

(fun r ⇒ \[r = val_unit]).

Lemma wp_free' : ∀ v w p Q,

(p ~~> v) \* (Q val_unit) ==> wp (val_free p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_free'. }

{ applys himpl_refl. }

{ xsimpl. intros ? →. auto. }

Qed.

End WpSpecRef.

triple (val_set p w)

(p ~~> v)

(fun r ⇒ \[r = val_unit] \* p ~~> w).

Lemma wp_set' : ∀ v w p Q,

(p ~~> v) \* (p ~~> w \−∗ Q val_unit) ==> wp (val_set p w) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_set'. }

{ applys himpl_refl. }

{ xsimpl. intros ? →. auto. }

Qed.

Parameter triple_free' : ∀ p v,

triple (val_free p)

(p ~~> v)

(fun r ⇒ \[r = val_unit]).

Lemma wp_free' : ∀ v w p Q,

(p ~~> v) \* (Q val_unit) ==> wp (val_free p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_free'. }

{ applys himpl_refl. }

{ xsimpl. intros ? →. auto. }

Qed.

End WpSpecRef.

### 4. Exercise

Parameter incr : val.

Parameter triple_incr : ∀ (p:loc) (n:int),

triple (incr p)

(p ~~> n)

(fun v ⇒ \[v = val_unit] \* (p ~~> (n+1))).

Parameter triple_incr : ∀ (p:loc) (n:int),

triple (incr p)

(p ~~> n)

(fun v ⇒ \[v = val_unit] \* (p ~~> (n+1))).

#### 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.
(* FILL IN HERE *)

☐

☐

## Historical Notes

(* 2024-01-03 14:19 *)