# WPgenWeakest Precondition Generator

Set Implicit Arguments.

From SLF Require Import WPsem.

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.

From SLF Require Import WPsem.

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.

# First Pass

_{1}(fun r ⇒ wp t

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

_{1}t

_{2}) Q.

_{2}. Instead, the beta reduction mechanism of Coq will automatically perform substitutions for Coq variables.

- how to define wpgen t as a recursive function that computes in Coq,
- how to integrate support for the frame rule in this recursive definition,
- how to carry out practical proofs using wpgen.

## Step 1: wpgen as a Recursive Function over Terms

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

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

_{1}t

_{2}) Q, the definition of wpgen is such that wpgen (trm_let x t

_{1}t

_{2}) Q is, by definition, equal to wpgen t

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

_{2}) Q). If t is a function application, wpgen t Q asserts that the current state must be described by some heap predicate H such that triple t H Q holds.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_var x ⇒ \[False]

| trm_app v

_{1}v

_{2}⇒ \∃ H, H \* \[triple t H Q]

| trm_let x t

_{1}t

_{2}⇒ wpgen t

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

_{2}) Q)

...

end. To obtain the actual definition of wpgen, we need to refine the above definition in 4 steps.

_{2}) is not made to a strict subterm of trm_let x t

_{1}t

_{2}, thus Coq rejects this definition as it stands.

_{1}t

_{2}, the context E gets extended as (x,v)::E. Observe also how, when reaching a variable x, a lookup for x into the context E is performed for recovering the value bound to x.

Fixpoint wpgen (E:ctx) (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_var x ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

_{1}v

_{2}⇒ \∃ H, H \* \[triple (isubst E t) H Q]

| trm_let x t

_{1}t

_{2}⇒ wpgen E t

_{1}(fun v ⇒ wpgen ((x,v)::E) t

_{2}Q)

...

end.

## Step 2: wpgen Reformulated to Eagerly Match on the Term

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ fun (Q:val→hprop) ⇒ Q v

| trm_var x ⇒ fun (Q:val→hprop) ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app t

_{1}t

_{2}⇒ fun (Q:val→hprop) ⇒

\∃ H, H \* \[triple (isubst E t) H Q]

| trm_let x t

_{1}t

_{2}⇒ fun (Q:val→hprop) ⇒

wpgen E t

_{1}(fun v ⇒ wpgen ((x,v)::E) t

_{2}Q)

...

end.

## Step 3: wpgen Reformulated with Auxiliary Definitions

_{1}F

_{2}be a shorthand for fun (Q:val→hprop) ⇒ F

_{1}(fun v ⇒ F

_{2}Q). Using these auxiliary definitions, the definition of wpgen can be reformulated as follows.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_app t

_{1}t

_{2}⇒ wpgen_app (isubst E t)

| trm_let x t

_{1}t

_{2}⇒ wpgen_let (wpgen E t

_{1}) (fun v ⇒ wpgen ((x,v)::E) t

_{2})

...

end. Each of the auxiliary definitions introduced for wpgen comes with a custom notation that enables a nice display of the output of wpgen. For example, the notation Let' v := F

_{1}in F

_{2}stands for wpgen_let F

_{1}(fun v ⇒ F

_{2}). Thanks to this notation, the result of computing wpgen on a source term Let x := t

_{1}in t

_{2}, which is an Coq expression of type trm, is a Coq expression of type formula displayed as Let' x := F

_{1}in F

_{2}.

## Step 4: wpgen Augmented with Support for Structural Rules

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

| trm_val v ⇒ ...

| ...

end). Without entering the details at this stage, the predicate mkstruct is a function of type formula→formula that captures the essence of the wp-style consequence-frame rule wp_conseq_frame, presented the previous chapter. This rule asserts that Q

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

_{2}implies (wp t Q

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

_{2}).

## Definition of wpgen for Each Term Construct

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ ..

| trm_seq t

_{1}t

_{2}⇒ ..

| trm_let x t

_{1}t

_{2}⇒ ..

| trm_var x ⇒ ..

| trm_app t

_{1}t

_{2}⇒ ..

| trm_fun x t

_{1}⇒ ..

| trm_fix f x t

_{1}⇒ ..

| trm_if v

_{0}t

_{1}t

_{2}⇒ ..

end). Our first goal is to figure out how to fill in the dots for each of the term constructors. The intention that guides us for filling the dot is the soundness theorem for wpgen, which takes the following form:

wpgen t Q ==> wp t Q This entailment asserts in particular that, if we are able to establish a statement of the form H ==> wpgen t Q, then we can derive from it H ==> wp t Q. The latter is also equivalent to triple t H Q. Thus, wpgen can be viewed as a practical tool to establish triples.

### Definition of wpgen for Values

The soundness theorem for wpgen requires the entailment
wpgen (trm_val v) Q ==> wp (trm_val v) Q to hold.
To satisfy this entailment, according to the rule wp_val, it suffices to
define wpgen (trm_val v) Q as Q v.
Concretely, we fill in the first dots as follows:

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

...

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

...

### Definition of wpgen for Functions

So, likewise, we can define wpgen for functions and for recursive
functions as follows:

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_fun x t

| trm_fix f x t

...
Observe that we do not attempt to recursively compute wpgen over the body
of the function. Doing so does not harm expressiveness, because the user may
request the computation of wpgen on a local function when reaching the
corresponding function definition in the proof. In chapter Wand, we
will see how to extend wpgen to eagerly process local function
definitions.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_fun x t

_{1}⇒ Q (val_fun x t_{1})| trm_fix f x t

_{1}⇒ Q (val_fix f x t_{1})...

The intention is for wpgen to admit the same semantics as wp. We thus
expect the definition of wpgen (trm_seq t
We therefore define wpgen (trm_seq t

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_seq t

...

_{1}t_{2}) Q to have a similar shape as wp t_{1}(fun v ⇒ wp t_{2}Q)._{1}t_{2}) Q as wpgen t_{1}(fun v ⇒ wpgen t_{2}Q). The definition of wpgen is thus extended as follows:Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_seq t

_{1}t_{2}⇒ wpgen t_{1}(fun v ⇒ wpgen t_{2}Q)...

### Definition of wpgen for Let-Bindings

Parameter wp_let : ∀ x t

wp 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.
We fill in the dots as follows:

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_let x t

... One important observation to make at this point is that the function wpgen is no longer structurally recursive. Indeed, whereas the first recursive call to wpgen is invoked on t
It is technically possible to convince Coq that the function wpgen
terminates, yet with great effort. Alternatively, we can circumvent the
problem altogether by casting the function in a form that makes it
structurally recursive. Concretely, we will see further on how to add as
argument to wpgen a substitution context, written E, to delay the
computation of substitutions until the leaves of the recursion.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_let x t

_{1}t_{2}⇒ wpgen t_{1}(fun v ⇒ wpgen (subst x v t_{2}) Q)... One important observation to make at this point is that the function wpgen is no longer structurally recursive. Indeed, whereas the first recursive call to wpgen is invoked on t

_{1}, which is a strict subterm of t, the second call is invoked on subst x v t_{2}, which is not a strict subterm of t.### Definition of wpgen for Variables

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_var x ⇒ \[False]

...

Lemma wp_var : ∀ x Q,

\[False] ==> wp (trm_var x) Q.

Proof using. intros. intros h Hh. destruct (hpure_inv Hh). false. Qed.

Lemma triple_var : ∀ x H Q,

False →

triple (trm_var x) H Q.

Proof using. intros. false. Qed.

Lemma triple_var' : ∀ x Q,

triple (trm_var x) \[False] Q.

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

\[False] ==> wp (trm_var x) Q.

Proof using. intros. intros h Hh. destruct (hpure_inv Hh). false. Qed.

Lemma triple_var : ∀ x H Q,

False →

triple (trm_var x) H Q.

Proof using. intros. false. Qed.

Lemma triple_var' : ∀ x Q,

triple (trm_var x) \[False] Q.

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

All these rules are correct, albeit totally useless.

### Definition of wpgen for Function Applications

_{1}v

_{2}. We have seen wp-style rules to reason about the application of a known function, e.g. trm_app (val_fun x t

_{1}) v

_{2}. However, if v

_{1}is an abstrat value (e.g., a Coq variable of type val), we have no reasoning rule at hand that applies. Instead, we expect to reason about an application trm_app v

_{1}v

_{2}by exhibiting a triple of the form triple (trm_app v

_{1}v

_{2}) H Q. Thus, wpgen (trm_app t

_{1}t

_{2}) Q needs to capture the fact that it describes a heap that could also be described by an H for which triple (trm_app v

_{1}v

_{2}) H Q holds.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_app t

_{1}t

_{2}⇒ ∃ H, H \* \[triple t H Q]

...

_{1}t

_{2}) Q as wp (trm_app t

_{1}t

_{2}) Q. In other words, to define wpgen for a function application, we could fall back to the semantic definition of wp.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_app t

_{1}t

_{2}⇒ wp t Q

... However, this definition would require converting the wp into a triple each time, because specifications are, by convention, expressed using the predicate triple.

_{1}t

_{2}where t

_{1}and t

_{2}are not both values, it is still correct to define wpgen (trm_app t

_{1}t

_{2})) as wp (trm_app t

_{1}t

_{2}). So, we need not bother checking in the definition of wpgen that the arguments of trm_app are actually values.

### Definition of wpgen for Conditionals

Parameter wp_if : ∀ (b:bool) t

(if b then (wp t

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

_{1}Q) else (wp t_{2}Q)) ==> wp (trm_if (val_bool b) t_{1}t_{2}) Q.
Typically, a source program may feature a conditional
trm_if (trm_var x) t
Yet, the reasoning rule wp_if stated above features a right-hand side of
the form wp (trm_if (val_bool b) t

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_if t

\∃ (b:bool), \[t

\* (if b then (wpgen t

...

_{1}t_{2}that, after substitution for x, becomes trm_if (trm_val v) t_{1}t_{2}, for some abstract v of type val. Yet, in general, this value is now know to be a boolean value. We therefore need to define wpgen for all if-statements of the form trm_if (trm_val v_{0}) t_{1}t_{2}, where v_{0}could be a value of unknown shape._{1}t_{2}) Q. It only applies when the first argument of trm_if is syntactically a boolean value b. To resolve this mismatch, the definition of wpgen for a term trm_if t_{0}t_{1}t_{2}quantifies existentially over a boolean value b such that t_{0}= trm_val (val_bool b) . The formal definition is:Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_if t

_{0}t_{1}t_{2}⇒\∃ (b:bool), \[t

_{0}= trm_val (val_bool b)]\* (if b then (wpgen t

_{1}) Q else (wpgen t_{2}) Q)...

### Summary of the Definition of wpgen for Term Rules

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_fun x t

_{1}⇒ Q (val_fun x t)

| trm_fix f x t

_{1}⇒ Q (val_fix f x t)

| trm_seq t

_{1}t

_{2}⇒ wpgen t

_{1}(fun v ⇒ wpgen t

_{2}Q)

| trm_let x t

_{1}t

_{2}⇒ wpgen t

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

_{2}) Q)

| trm_var x ⇒ \[False]

| trm_app t

_{1}t

_{2}⇒ ∃ H, H \* \[triple t H Q]

| trm_if t

_{0}t

_{1}t

_{2}⇒

\∃ (b:bool), \[t

_{0}= trm_val (val_bool b)]

\* (if b then (wpgen t

_{1}) Q else (wpgen t

_{2}) Q)

end. As pointed out earlier, this definition is not structurally recursive and thus not accepted by Coq, due to the recursive call wpgen (subst x v t

_{2}) Q . Our next step is to fix this issue.

## Computing with wpgen

### Definition of Contexts and Operations on Them

The "iterated substitution" operation, written isubst E t, describes the
substitution of all the bindings form E inside a term t. Its
implementation is standard: then function traverses the term recursively
and, when reaching a variable, performs a lookup in the context E. The
operation needs to take care to respect variable shadowing. To that end,
when traversing a binder that binds a variable x, all occurrences of x
that might previously exist in E are removed.
The formal definition of isubst involves two auxiliary functions: lookup
and removal on association lists. The definition of the operation
lookup x E on association lists is standard. It returns an option on a
value.

Fixpoint lookup (x:var) (E:ctx) : option val :=

match E with

| nil ⇒ None

| (y,v)::E

then Some v

else lookup x E

end.

match E with

| nil ⇒ None

| (y,v)::E

_{1}⇒ if var_eq x ythen Some v

else lookup x E

_{1}end.

The definition of the removal operation, written rem x E, is also
standard. It returns a filtered context.

Fixpoint rem (x:var) (E:ctx) : ctx :=

match E with

| nil ⇒ nil

| (y,v)::E

let E

if var_eq x y then E

end.

match E with

| nil ⇒ nil

| (y,v)::E

_{1}⇒let E

_{1}' := rem x E_{1}inif var_eq x y then E

_{1}' else (y,v)::E_{1}'end.

The definition of the operation isubst E t can then be expressed as a
recursive function over the term t. It invokes lookup x E when reaching
a variable x. It invokes rem x E when traversing a binding on the name
x.

Fixpoint isubst (E:ctx) (t:trm) : trm :=

match t with

| trm_val v ⇒

v

| trm_var x ⇒

match lookup x E with

| None ⇒ t

| Some v ⇒ v

end

| trm_fun x t

trm_fun x (isubst (rem x E) t

| trm_fix f x t

trm_fix f x (isubst (rem x (rem f E)) t

| trm_app t

trm_app (isubst E t

| trm_seq t

trm_seq (isubst E t

| trm_let x t

trm_let x (isubst E t

| trm_if t

trm_if (isubst E t

end.

match t with

| trm_val v ⇒

v

| trm_var x ⇒

match lookup x E with

| None ⇒ t

| Some v ⇒ v

end

| trm_fun x t

_{1}⇒trm_fun x (isubst (rem x E) t

_{1})| trm_fix f x t

_{1}⇒trm_fix f x (isubst (rem x (rem f E)) t

_{1})| trm_app t

_{1}t_{2}⇒trm_app (isubst E t

_{1}) (isubst E t_{2})| trm_seq t

_{1}t_{2}⇒trm_seq (isubst E t

_{1}) (isubst E t_{2})| trm_let x t

_{1}t_{2}⇒trm_let x (isubst E t

_{1}) (isubst (rem x E) t_{2})| trm_if t

_{0}t_{1}t_{2}⇒trm_if (isubst E t

_{0}) (isubst E t_{1}) (isubst E t_{2})end.

Remark: it is also possible to define the substitution by iterating the
unary substitution subst over the list of bindings from E. However, this
alternative approach yields a less efficient function and leads to more
complicated proofs.
In what follows, we present the definition of wpgen E t case by case.
Throughout these definitions, recall that wpgen E t is interpreted as the
weakest precondition of isubst E t.

### wpgen: the Let-Binding Case

_{1}t

_{2}) triggers a recursive call to wpgen ((x,v)::E) t

_{2}. The corresponding definition is:

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

...

| trm_let x t

_{1}t

_{2}⇒ fun Q ⇒

(wpgen E t

_{1}) (fun v ⇒ wpgen ((x,v)::E) t

_{2})

...

) end.

### wpgen: the Variable Case

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

...

| trm_var x ⇒ fun Q ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

...

) end.

### wpgen: the Application Case

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

..

| trm_app t

_{1}t

_{2}⇒ fun Q ⇒ ∃ H, H \* \[triple t H Q]

Fixpoint wpgen (t:trm) : formula :=

mkstruct (match t with

...

| trm_app v

_{1}v

_{2}⇒ fun Q ⇒ ∃ H, H \* \[triple (isubst E t) H Q]

..

### wpgen: the Function Definition Case

_{1}. Here again, the formula wpgen E t is interpreted as the weakest precondition of isubst E t.

_{1}, we obtain trm_fun x (isubst (rem x E) t

_{1}).

_{1}). The weakest precondition for that value is fun Q ⇒ Q (val_fun x (isubst (rem x E) t

_{1})).

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

...

| trm_fun x t

_{1}⇒ fun Q ⇒ Q (val_fun x (isubst (rem x E) t

_{1}))

| trm_fix f x t

_{1}⇒ fun Q ⇒ Q (val_fix f x (isubst (rem x (rem f E)) t

_{1}))

...

) end.

At last, we arrive to a definition of wpgen that type-checks in Coq, and
that can be used to effectively compute weakest preconditions in Separation
Logic.

Fixpoint wpgen (E:ctx) (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_fun x t

| trm_fix f x t

| trm_seq t

| trm_let x t

| trm_var x ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

| trm_if t

\∃ (b:bool), \[t

\* (if b then (wpgen E t

end.

match t with

| trm_val v ⇒ Q v

| trm_fun x t

_{1}⇒ Q (val_fun x (isubst (rem x E) t_{1}))| trm_fix f x t

_{1}⇒ Q (val_fix f x (isubst (rem x (rem f E)) t_{1}))| trm_seq t

_{1}t_{2}⇒ wpgen E t_{1}(fun v ⇒ wpgen E t_{2}Q)| trm_let x t

_{1}t_{2}⇒ wpgen E t_{1}(fun v ⇒ wpgen ((x,v)::E) t_{2}Q)| trm_var x ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

_{1}v_{2}⇒ \∃ H, H \* \[triple (isubst E t) H Q]| trm_if t

_{0}t_{1}t_{2}⇒\∃ (b:bool), \[t

_{0}= trm_val (val_bool b)]\* (if b then (wpgen E t

_{1}) Q else (wpgen E t_{2}) Q)end.

Compared with the presentation using the form wpgen t, the new
presentation using the form wpgen E t has the main benefits that it is
structurally recursive, thus easy to define in Coq.
Further in the chapter, we will establish the soundness of the wpgen. For
the moment, we simply state the soundness theorem, to explain how it can be
exploited for verifying concrete programs.

The entailment above asserts in particular that if we can derive
triple t H Q by proving H ==> wpgen t Q. A useful corrolary combines the
soundness theorem with the rule triple_app_fun, which allows establishing
triples for functions. Recall the rule triple_app_fun from Rules.

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.
Reformulating the rule above into a rule for wpgen takes 3 steps.
First, we rewrite the premise triple (subst x v
Second, we observe that the term subst x v
Third, according to wpgen_sound, the predicate
wp (isubst ((x,v

_{2}t_{1}) H Q using wp. It becomes H ==> wp (subst x v_{2}t_{1}) Q._{2}t_{1}is equal to isubst ((x,v_{2})::nil) t_{1}. (This equality is captured by the lemma subst_eq_isubst_one proved in the bonus section of the chapter.) Thus, the heap predicate wp (subst x v_{2}t_{1}) Q is equivalent to wp (isubst ((x,v_{2})::nil) t_{1})._{2})::nil) t_{1}) is entailed by wpgen ((x,v_{2})::nil) t_{1}. Thus, we can use the latter as premise in place of the former. We thereby obtain the following lemma, which is at the heart of the implementation of the tactic xwp.
Parameter triple_app_fun_from_wpgen : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.
Let us exploit triple_app_fun_from_wpgen to demonstrate the computation of
wpgen on a practical program. Recall the function incr (defined in
Rules), and its specification, whose statement appears below.

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

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl. (* Read the goal here... *)

Abort.

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl. (* Read the goal here... *)

Abort.

At the ned of the above proof, the goal takes the form H ==> wpgen body Q,
where H denotes the precondition, Q the postcondition, and body the
body of the function incr. Observe the invocations of wp on the
application of primitive operations. Observe that the goal is nevertheless
somewhat hard to relate to the original program. In what follows, we explain
how to remedy the situation, and set up wpgen is such a way that its
output is human-readable, moreover resembles the original source code.

## Optimizing the Readability of wpgen Output

- first, we modify the presentation of wpgen so that the fun (Q:val→hprop) ⇒ appears insides the branches of the match t with rather than around it,
- second, we introduce one auxiliary definition for each branch of the match t with,
- third, we introduce one piece of notation for each of these auxiliary definitions.

### Reability Step 1: Moving the Function below the Branches.

Fixpoint wpgen (E:ctx) (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_fun x t

_{1}⇒ Q (val_fun x (isubst (rem x E) t

_{1}))

...

end. to the equivalent form:

Fixpoint wpgen (E:ctx) (t:trm) : (val→hprop)->hprop :=

match t with

| trm_val v ⇒ fun (Q:val→hprop) ⇒ Q v

| trm_fun x t

_{1}⇒ fun (Q:val→hprop) ⇒ Q (val_fun x (isubst (rem x E) t

_{1}))

...

end.

### Readability Steps 2 and 3, Illustrated on the Case of Sequences

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

...

| trm_seq t

_{1}t

_{2}⇒ fun Q ⇒ (wpgen E t

_{1}) (fun v ⇒ wpgen E t

_{2}Q)

...

end. to the equivalent form:

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

...

| trm_seq t

_{1}t

_{2}⇒ wpgen_seq (wpgen E t

_{1}) (wpgen E t

_{2})

...

end. where wpgen_seq is defined as shown below.

Remark: above, F
With the above definitions, wgpen E (trm_seq t
Finally, we introduce a piece of notation for each case. In the case of the
sequence, we set up the notation defined next to so that any formula of the
form wpgen_seq F

_{1}and F_{2}denote the results of the recursive calls, wpgen E t_{1}and wpgen E t_{2}, respectively._{1}t_{2}) evaluates to wp_seq (wpgen E t_{1}) (wpgen E t_{2})._{1}F_{2}gets displayed as Seq F_{1}; F_{2}.
Notation "'Seq' F

((wpgen_seq F

(at level 68, right associativity,

format "'[v' 'Seq' '[' F

_{1}; F_{2}" :=((wpgen_seq F

_{1}F_{2}))(at level 68, right associativity,

format "'[v' 'Seq' '[' F

_{1}']' ';' '/' '[' F_{2}']' ']'").
Thanks to this notation, the wpgen of a sequence t

_{1}; t_{2}displays as Seq F_{1}; F_{2}where F_{1}and F_{2}denote the wpgen of t_{1}and t_{2}, respectively.### Readability Step 2: Auxiliary Definitions for other Constructs

Definition wpgen_val (v:val) : formula := fun Q ⇒

Q v.

Definition wpgen_let (F

F

Definition wpgen_if (t:trm) (F

\∃ (b:bool), \[t = trm_val (val_bool b)] \* (if b then F

Definition wpgen_fail : formula := fun Q ⇒

\[False].

Definition wpgen_var (E:ctx) (x:var) : formula :=

match lookup x E with

| None ⇒ wpgen_fail

| Some v ⇒ wpgen_val v

end.

Definition wpgen_app (t:trm) : formula := fun Q ⇒

\∃ H, H \* \[triple t H Q].

Q v.

Definition wpgen_let (F

_{1}:formula) (F2of:val→formula) : formula := fun Q ⇒F

_{1}(fun v ⇒ F2of v Q).Definition wpgen_if (t:trm) (F

_{1}F_{2}:formula) : formula := fun Q ⇒\∃ (b:bool), \[t = trm_val (val_bool b)] \* (if b then F

_{1}Q else F_{2}Q).Definition wpgen_fail : formula := fun Q ⇒

\[False].

Definition wpgen_var (E:ctx) (x:var) : formula :=

match lookup x E with

| None ⇒ wpgen_fail

| Some v ⇒ wpgen_val v

end.

Definition wpgen_app (t:trm) : formula := fun Q ⇒

\∃ H, H \* \[triple t H Q].

The new definition of wpgen reads as follows.

Module WpgenExec2.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

| trm_fix f x t

| trm_app t

| trm_seq t

| trm_let x t

| trm_if t

end.

End WpgenExec2.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

_{1}⇒ wpgen_val (val_fun x (isubst (rem x E) t_{1}))| trm_fix f x t

_{1}⇒ wpgen_val (val_fix f x (isubst (rem x (rem f E)) t_{1}))| trm_app t

_{1}t_{2}⇒ wpgen_app (isubst E t)| trm_seq t

_{1}t_{2}⇒ wpgen_seq (wpgen E t_{1}) (wpgen E t_{2})| trm_let x t

_{1}t_{2}⇒ wpgen_let (wpgen E t_{1}) (fun v ⇒ wpgen ((x,v)::E) t_{2})| trm_if t

_{0}t_{1}t_{2}⇒ wpgen_if (isubst E t_{0}) (wpgen E t_{1}) (wpgen E t_{2})end.

End WpgenExec2.

### Readability Step 3: Notation for Auxiliary Definitions

Declare Scope wpgen_scope.

Notation "'Val' v" :=

((wpgen_val v))

(at level 69) : wpgen_scope.

Notation "'Let'' x ':=' F

((wpgen_let F

(at level 69, x name, right associativity,

format "'[v' '[' 'Let'' x ':=' F

: wpgen_scope.

Notation "'If'' b 'Then' F

((wpgen_if b F

(at level 69) : wpgen_scope.

Notation "'Fail'" :=

((wpgen_fail))

(at level 69) : wpgen_scope.

Notation "'Val' v" :=

((wpgen_val v))

(at level 69) : wpgen_scope.

Notation "'Let'' x ':=' F

_{1}'in' F_{2}" :=((wpgen_let F

_{1}(fun x ⇒ F_{2})))(at level 69, x name, right associativity,

format "'[v' '[' 'Let'' x ':=' F

_{1}'in' ']' '/' '[' F_{2}']' ']'"): wpgen_scope.

Notation "'If'' b 'Then' F

_{1}'Else' F_{2}" :=((wpgen_if b F

_{1}F_{2}))(at level 69) : wpgen_scope.

Notation "'Fail'" :=

((wpgen_fail))

(at level 69) : wpgen_scope.

In addition, we introduce handy notation of the result of wpgen t where
t denotes an application. We cover here only functions of arity one or
two. The file LibSepReference.v provides arity-generic definitions.

Notation "'App' f v

((wpgen_app (trm_app f v

(at level 68, f, v

Notation "'App' f v

((wpgen_app (trm_app (trm_app f v

(at level 68, f, v

_{1}" :=((wpgen_app (trm_app f v

_{1})))(at level 68, f, v

_{1}at level 0) : wpgen_scope.Notation "'App' f v

_{1}v_{2}" :=((wpgen_app (trm_app (trm_app f v

_{1}) v_{2})))(at level 68, f, v

_{1}, v_{2}at level 0) : wpgen_scope.
Here again, we temporarily axiomatize the soundness result for the purpose
of looking at how that result can be exploited in practice.

Parameter triple_app_fun_from_wpgen : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.
Consider again the example of incr.

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

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl. (* Read the goal here... It is of the form H ==> F Q,

where F vaguely looks like the code of the body of incr. *)

Abort.

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl. (* Read the goal here... It is of the form H ==> F Q,

where F vaguely looks like the code of the body of incr. *)

Abort.

Up to proper tabulation, alpha-renaming, removal of parentheses, and removal
of quotes after Let and If), the formula F reads as:

Let n := App val_get p in

Let m := App (val_add n) 1 in

App (val_set p) m
With the introduction of intermediate definitions for wpgen and the
introduction of associated notations for each term construct, what we
achieved is that the output of wpgen is, for any input term t, a human
readable formula whose display closely resembles the syntax source code of
the term t.

Let n := App val_get p in

Let m := App (val_add n) 1 in

App (val_set p) m

## Extension of wpgen to Handle Structural Rules

### Introduction of mkstruct in the Definition of wpgen

Fixpoint wpgen (E:ctx) (t:trm) : (val→hprop)->hprop :=

mkstruct (

match t with

| trm_val v ⇒ wpgen_val v

...

end). With this definition, any output of wpgen E t is necessarily of the form mkstruct F, for some formula F describing the weakest precondition of t. The next step is to investigate what properties mkstruct should satisfy.

Because mkstruct appears between the prototype and the match in the body
of wpgen, the predicate mkstruct must have type formula→formula.

The predicate mkstruct should satisfy reasoning rules that mimic the
statements of the frame rule and the consequence rule in
weakest-precondition style (wp_frame and wp_conseq).

Parameter mkstruct_frame : ∀ (F:formula) H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Parameter mkstruct_conseq : ∀ (F:formula) Q

Q

mkstruct F Q

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Parameter mkstruct_conseq : ∀ (F:formula) Q

_{1}Q_{2},Q

_{1}===> Q_{2}→mkstruct F Q

_{1}==> mkstruct F Q_{2}.
In addition, the user manipulating a formula produced by wpgen should be
able to discard the predicate mkstruct from the head of the output when
there is no need to apply the frame rule or the rule of consequence. The
erasure property is captured by the following entailment.

Moreover, in order to complete the soundness proof for wpgen, the
predicate mkstruct should be covariant: if F

_{1}entails F_{2}, then mkstruct F_{1}should entail mkstruct F_{2}.
Parameter mkstruct_monotone : ∀ F

(∀ Q, F

mkstruct F

End MkstructProp.

_{1}F_{2}Q,(∀ Q, F

_{1}Q ==> F_{2}Q) →mkstruct F

_{1}Q ==> mkstruct F_{2}Q.End MkstructProp.

### Realization of mkstruct

The magic wand may appear somewhat puzzling, but it fact the above statement
is reminiscent from the statement of wp_ramified, which captures the
expressive power of all the structural reasoning rules of Separation Logic
at once. If we unfold the definition of the magic wand, we can see more
clearly that mkstruct F is a formula that describes a program that
produces a postcondition Q when executed in the current state if and only
if the formula F describes a program that produces a postcondtion Q

_{1}in a subset of the current state, and if the postcondition Q_{1}augmented with the remaining of the current state (i.e., the piece described by H) corresponds to the postcondition Q.
Definition mkstruct' (F:formula) : formula :=

fun (Q:val→hprop) ⇒ \∃ Q

fun (Q:val→hprop) ⇒ \∃ Q

_{1}H, F Q_{1}\* H \* \[Q_{1}\*+ H ===> Q].
The 4 properties of mkstruct can be easily verified.

Lemma mkstruct_frame : ∀ F H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Proof using. intros. unfold mkstruct. xpull. intros Q'. xsimpl*. Qed.

Lemma mkstruct_conseq : ∀ F Q

Q

mkstruct F Q

Proof using. introv WQ. unfold mkstruct. xpull. intros Q'. xsimpl*. Qed.

Lemma mkstruct_erase : ∀ F Q,

F Q ==> mkstruct F Q.

Proof using. intros. unfold mkstruct. xsimpl. Qed.

Lemma mkstruct_monotone : ∀ F

(∀ Q, F

mkstruct F

Proof using. introv WF. unfolds mkstruct. xpull. intros Q'. xchanges WF. Qed.

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Proof using. intros. unfold mkstruct. xpull. intros Q'. xsimpl*. Qed.

Lemma mkstruct_conseq : ∀ F Q

_{1}Q_{2},Q

_{1}===> Q_{2}→mkstruct F Q

_{1}==> mkstruct F Q_{2}.Proof using. introv WQ. unfold mkstruct. xpull. intros Q'. xsimpl*. Qed.

Lemma mkstruct_erase : ∀ F Q,

F Q ==> mkstruct F Q.

Proof using. intros. unfold mkstruct. xsimpl. Qed.

Lemma mkstruct_monotone : ∀ F

_{1}F_{2}Q,(∀ Q, F

_{1}Q ==> F_{2}Q) →mkstruct F

_{1}Q ==> mkstruct F_{2}Q.Proof using. introv WF. unfolds mkstruct. xpull. intros Q'. xchanges WF. Qed.

### Definition of wpgen that Includes mkstruct

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

| trm_fix f x t

| trm_app t

| trm_seq t

| trm_let x t

| trm_if t

end).

mkstruct (match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

_{1}⇒ wpgen_val (val_fun x (isubst (rem x E) t_{1}))| trm_fix f x t

_{1}⇒ wpgen_val (val_fix f x (isubst (rem x (rem f E)) t_{1}))| trm_app t

_{1}t_{2}⇒ wpgen_app (isubst E t)| trm_seq t

_{1}t_{2}⇒ wpgen_seq (wpgen E t_{1}) (wpgen E t_{2})| trm_let x t

_{1}t_{2}⇒ wpgen_let (wpgen E t_{1}) (fun v ⇒ wpgen ((x,v)::E) t_{2})| trm_if t

_{0}t_{1}t_{2}⇒ wpgen_if (isubst E t_{0}) (wpgen E t_{1}) (wpgen E t_{2})end).

To avoid clutter in reading the output of wpgen, we introduce a
lightweight shorthand to denote mkstruct F, allowing it to display simply
as `F.

Once again, we temporarily axiomatize the soundness result for the purpose
of looking at how that result can be exploited in practice.

Parameter triple_app_fun_from_wpgen : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.## Lemmas for Handling wpgen Goals

Lemma xstruct_lemma : ∀ F H Q,

H ==> F Q →

H ==> mkstruct F Q.

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

H ==> F Q →

H ==> mkstruct F Q.

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

xval_lemma reformulates the definition of wpgen_val. It just unfolds the
definition.

xlet_lemma reformulates the definition of wpgen_let. It just unfolds the
definition.

Lemma xlet_lemma : ∀ H F

H ==> F

H ==> wpgen_let F

Proof using. introv M. xchange M. Qed.

_{1}F2of Q,H ==> F

_{1}(fun v ⇒ F2of v Q) →H ==> wpgen_let F

_{1}F2of Q.Proof using. introv M. xchange M. Qed.

Likewise, xseq_lemma reformulates wpgen_seq.

Lemma xseq_lemma : ∀ H F

H ==> F

H ==> wpgen_seq F

Proof using. introv M. xchange M. Qed.

_{1}F_{2}Q,H ==> F

_{1}(fun v ⇒ F_{2}Q) →H ==> wpgen_seq F

_{1}F_{2}Q.Proof using. introv M. xchange M. Qed.

xapp_lemma applies to goals produced by wpgen on an application. In such
cases, the proof obligation is of the form H ==> (wpgen_app t) Q.
xapp_lemma reformulates the frame-consequence rule in a way that enables
exploiting a specification triple of a function to reason about a call to
that function.

Lemma xapp_lemma : ∀ t Q

triple t H

H ==> H

Q

H ==> wpgen_app t Q.

Proof using.

introv M WH WQ. unfold wpgen_app. xsimpl. applys* triple_conseq_frame M.

Qed.

_{1}H_{1}H_{2}H Q,triple t H

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

_{1}\* H_{2}→Q

_{1}\*+ H_{2}===> Q →H ==> wpgen_app t Q.

Proof using.

introv M WH WQ. unfold wpgen_app. xsimpl. applys* triple_conseq_frame M.

Qed.

xwp_lemma is another name for triple_app_fun_from_wpgen. It is used for
establishing a triple for a function application.

Lemma xwp_lemma : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

Proof using. introv M

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.Proof using. introv M

_{1}M_{2}. applys* triple_app_fun_from_wpgen. Qed.
Module ProofsWithXlemmas.

Import ExamplePrograms.

Open Scope wpgen_scope.

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

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros.

applys xwp_lemma. { reflexivity. }

(* Here the wpgen function computes. *)

simpl.

(* Observe how each node begin with mkstruct.

Observe how program variables are all eliminated. *)

applys xstruct_lemma.

applys xlet_lemma.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_get. } { xsimpl. }

xpull; intros ? →.

applys xstruct_lemma.

applys xlet_lemma.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_add. } { xsimpl. }

xpull; intros ? →.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_set. } { xsimpl. }

xsimpl.

Qed.

Import ExamplePrograms.

Open Scope wpgen_scope.

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

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros.

applys xwp_lemma. { reflexivity. }

(* Here the wpgen function computes. *)

simpl.

(* Observe how each node begin with mkstruct.

Observe how program variables are all eliminated. *)

applys xstruct_lemma.

applys xlet_lemma.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_get. } { xsimpl. }

xpull; intros ? →.

applys xstruct_lemma.

applys xlet_lemma.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_add. } { xsimpl. }

xpull; intros ? →.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_set. } { xsimpl. }

xsimpl.

Qed.

#### Exercise: 2 stars, standard, especially useful (triple_succ_using_incr_with_xlemmas)

Using x-lemmas, simplify the proof of triple_succ_using_incr, which was carried out using triples in chapter chapter Rules.
Lemma triple_succ_using_incr_with_xlemmas : ∀ (n:int),

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

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

☐

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

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

☐

## Making Proof Scripts More Concise

The tactics xval, xseq and xlet invoke the corresponding x-lemmas,
after calling xstruct if a leading mkstruct is in the way.

Tactic Notation "xstruct_if_needed" :=

try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒ xstruct end.

Tactic Notation "xval" :=

xstruct_if_needed; applys xval_lemma.

Tactic Notation "xlet" :=

xstruct_if_needed; applys xlet_lemma.

Tactic Notation "xseq" :=

xstruct_if_needed; applys xseq_lemma.

try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒ xstruct end.

Tactic Notation "xval" :=

xstruct_if_needed; applys xval_lemma.

Tactic Notation "xlet" :=

xstruct_if_needed; applys xlet_lemma.

Tactic Notation "xseq" :=

xstruct_if_needed; applys xseq_lemma.

xapp_nosubst applys xapp_lemma, after calling xseq or xlet if
applicable. Further on, we will define xapp as an enhanced version of
xapp_nosusbt that is able to automatically perform substitutions.

Tactic Notation "xseq_xlet_if_needed" :=

try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒

match F with

| wpgen_seq ?F

| wpgen_let ?F

end end.

Tactic Notation "xapp_nosubst" constr(E) :=

xseq_xlet_if_needed; xstruct_if_needed;

applys xapp_lemma E; [ xsimpl | xpull ].

try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒

match F with

| wpgen_seq ?F

_{1}?F_{2}⇒ xseq| wpgen_let ?F

_{1}?F2of ⇒ xletend end.

Tactic Notation "xapp_nosubst" constr(E) :=

xseq_xlet_if_needed; xstruct_if_needed;

applys xapp_lemma E; [ xsimpl | xpull ].

xwp applys xwp_lemma, then requests Coq to evaluate the wpgen
function. (For technical reasons, in the definition shown below we need to
explicitly request the unfolding of wpgen_var.)

Tactic Notation "xwp" :=

intros; applys xwp_lemma;

[ reflexivity

| simpl; unfold wpgen_var; simpl ].

intros; applys xwp_lemma;

[ reflexivity

| simpl; unfold wpgen_var; simpl ].

Let us revisit the previous proof scripts using x-tactics instead of
x-lemmas. The reader may contemplate the gain in conciseness.

Module ProofsWithXtactics.

Import ExamplePrograms.

Open Scope wpgen_scope.

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

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp.

xapp_nosubst triple_get. intros ? →.

xapp_nosubst triple_add. intros ? →.

xapp_nosubst triple_set.

xsimpl.

Qed.

Import ExamplePrograms.

Open Scope wpgen_scope.

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

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp.

xapp_nosubst triple_get. intros ? →.

xapp_nosubst triple_add. intros ? →.

xapp_nosubst triple_set.

xsimpl.

Qed.

#### Exercise: 2 stars, standard, especially useful (triple_succ_using_incr_with_xtactics)

Using x-tactics, verify the proof of succ_using_incr.
Lemma triple_succ_using_incr_with_xtactics : ∀ (n:int),

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

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

☐

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

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

☐

## Automated Introductions using the xapp Tactic.

Tactic Notation "xapp_try_subst" := (* for internal use only *)

try match goal with

| ⊢ ∀ (r:val), (r = _) → _ ⇒ intros ? →

| ⊢ ∀ (r:val), ∀ x, (r = _) → _ ⇒

let y := fresh x in intros ? y ->; revert y

end.

Tactic Notation "xapp" constr(E) :=

xapp_nosubst E; xapp_try_subst.

try match goal with

| ⊢ ∀ (r:val), (r = _) → _ ⇒ intros ? →

| ⊢ ∀ (r:val), ∀ x, (r = _) → _ ⇒

let y := fresh x in intros ? y ->; revert y

end.

Tactic Notation "xapp" constr(E) :=

xapp_nosubst E; xapp_try_subst.

## Database of Specification Lemmas for the xapp Tactic.

#[global] Hint Resolve triple_get triple_set triple_ref

triple_free triple_add : triple.

triple_free triple_add : triple.

The argument-free variants xapp_subst and xapp are implemented by
invoking eauto with triple to retrieve the relevant specification.
DISCLAIMER: the tactic xapp that leverages the triple database is not
able to automatically apply specifications that involve a premise that
eauto cannot solve. To exploit such specifications, one need to provide
the specification explicitly using xapp E.

Tactic Notation "xapp_nosubst" :=

xseq_xlet_if_needed; xstruct_if_needed;

applys xapp_lemma; [ solve [ eauto with triple ] | xsimpl | xpull ].

Tactic Notation "xapp" :=

xapp_nosubst; xapp_try_subst.

xseq_xlet_if_needed; xstruct_if_needed;

applys xapp_lemma; [ solve [ eauto with triple ] | xsimpl | xpull ].

Tactic Notation "xapp" :=

xapp_nosubst; xapp_try_subst.

The tactics defined in the previous sections may be used to complete proofs
like done in the first two chapters of the course. For example, here is the
proof of the increment function.

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

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp. xapp. xapp. xapp. xsimpl.

Qed.

#[global] Hint Resolve triple_incr : triple.

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp. xapp. xapp. xapp. xsimpl.

Qed.

#[global] Hint Resolve triple_incr : triple.

In summary, we have shown how to leverage wpgen, x-lemmas and x-tactics to
implement the core of a practical verification framework based on Separation
Logic.

## Tactics xconseq and xframe

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

Prove the xconseq_lemma.
Lemma xconseq_lemma : ∀ Q

H ==> mkstruct F Q

Q

H ==> mkstruct F Q

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

☐

_{1}Q_{2}H F,H ==> mkstruct F Q

_{1}→Q

_{1}===> Q_{2}→H ==> mkstruct F Q

_{2}.Proof using. (* FILL IN HERE *) Admitted.

☐

Tactic Notation "xconseq" :=

applys xconseq_lemma.

Tactic Notation "xconseq" constr(Q) :=

applys xconseq_lemma Q.

applys xconseq_lemma.

Tactic Notation "xconseq" constr(Q) :=

applys xconseq_lemma Q.

The tactic xframe enables applying the frame rule on a formula produced by
wpgen. The syntax xframe H is used to specify the heap predicate to
keep, and the syntax xframe_out H is used to specify the heap predicate to
frame out---everything else is kept.

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

Prove the xframe_lemma. Exploit the properties of mkstruct; do not try to unfold the definition of mkstruct.
Lemma xframe_lemma : ∀ H

H ==> H

H

Q

H ==> mkstruct F Q.

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

☐

_{1}H_{2}H Q Q_{1}F,H ==> H

_{1}\* H_{2}→H

_{1}==> mkstruct F Q_{1}→Q

_{1}\*+ H_{2}===> Q →H ==> mkstruct F Q.

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

☐

Tactic Notation "xframe" constr(H) :=

eapply (@xframe_lemma H); [ xsimpl | | ].

Tactic Notation "xframe_out" constr(H) :=

eapply (@xframe_lemma _ H); [ xsimpl | | ].

eapply (@xframe_lemma H); [ xsimpl | | ].

Tactic Notation "xframe_out" constr(H) :=

eapply (@xframe_lemma _ H); [ xsimpl | | ].

Let's illustrate the use of xframe on an example.

Module ProofsWithStructuralXtactics.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr_frame : ∀ (p q:loc) (n m:int),

triple (trm_app incr p)

(p ~~> n \* q ~~> m)

(fun _ ⇒ (p ~~> (n+1)) \* (q ~~> m)).

Proof using.

xwp.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr_frame : ∀ (p q:loc) (n m:int),

triple (trm_app incr p)

(p ~~> n \* q ~~> m)

(fun _ ⇒ (p ~~> (n+1)) \* (q ~~> m)).

Proof using.

xwp.

Instead of calling xapp, we put aside q ~~> m and focus on p ~~> n.

Then we can work in a smaller state that mentions only p ~~> n.

xapp. xapp. xapp.

Finally we check the check that the current state augmented with the framed
predicate q ~~> m matches with the claimed postcondition.

So far in the chapter, in the definition of wpgen, we have treated the
constructions trm_fun and trm_fix as terms directly constructing a
value, following the same pattern as for the construction trm_val.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_fun x t

| trm_fix f x t

...

end. The present section explains how to extend the definition of wpgen to make it recurse inside the body of the function definitions. Doing so does not increase expressiveness, because the user had the possibility of manually requesting the computation of wpgen on a function value of the form val_fun or val_fix. However, having wpgen automatically recurse into function bodies saves the user the need to manually make such requests. In short, doing so makes life easier for the end-user. In what follows, we show how such a version of wpgen can be set up.
The new definition of wpgen will take the shape shown below, for
well-suited definitions of wpgen_fun and wpgen_fix yet to be introduced.
In the code snippet below, vx denotes a value to which the function may be
applied, and vf denotes the value associated with the function itself.
This value is involved where the function defined by trm_fix f x t

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

| trm_val v ⇒ wpgen_val v

| trm_fun x t

| trm_fix f x t

...

end.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_fun x t

_{1}⇒ Q (val_fun x t_{1})| trm_fix f x t

_{1}⇒ Q (val_fix f x t_{1})...

end. The present section explains how to extend the definition of wpgen to make it recurse inside the body of the function definitions. Doing so does not increase expressiveness, because the user had the possibility of manually requesting the computation of wpgen on a function value of the form val_fun or val_fix. However, having wpgen automatically recurse into function bodies saves the user the need to manually make such requests. In short, doing so makes life easier for the end-user. In what follows, we show how such a version of wpgen can be set up.

_{1}invokes itself recursively inside its body t_{1}.Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

| trm_val v ⇒ wpgen_val v

| trm_fun x t

_{1}⇒ wpgen_fun (fun vx ⇒ wpgen ((x,vx)::E) t_{1})| trm_fix f x t

_{1}⇒ wpgen_fix (fun vf vx ⇒ wpgen ((f,vf)::(x,vx)::E) t_{1})...

end.

### 1. Treatment of Non-Recursive Functions

_{1}) Q, expressed in terms of wpgen t

_{1}.

_{1}, which the term trm_fun x t

_{1}evaluates to. The heap predicate wpgen (trm_fun x t

_{1}) Q should assert that that the postcondition Q holds of the result value vf, i.e., that Q vf should hold.

_{1}as we were doing previously, we would like to specify that vf denotes a function whose body admits wpgen t

_{1}as weakest precondition. To that end, we define the heap predicate wpgen (trm_fun x t

_{1}) Q to be of the form \∀ vf, \[P vf] \−∗ Q vf for a carefully crafted predicate P that describes the behavior of the function by means of its weakest precondition. This predicate P is defined further on.

_{1}. It would be correct to replace \∀ vf, ... with let vf := val_fun x t

_{1}in ..., yet we are purposely trying to abstract away from the syntax of t

_{1}, hence the universal quantification of vf.

_{1}of the function, in such a way that the user is able to derive the specification aimed for the local function vf.

Parameter triple_app_fun_from_wpgen : ∀ vf vx x t

vf = val_fun x t

H' ==> wpgen ((x,vx)::nil) t

triple (trm_app vf vx) H' Q'.

_{1}H' Q',vf = val_fun x t

_{1}→H' ==> wpgen ((x,vx)::nil) t

_{1}Q' →triple (trm_app vf vx) H' Q'.

The lemma above enables establishing a triple for an application
trm_app vf vx with precondition H' and postcondition Q', from the
premise H' ==> wgen ((x,vx)::nil) t
It therefore makes sense, in our definition of the predicate
wpgen (trm_fun x t

∀ vx H' Q', (H' ==> wpgen ((x,vx)::nil) t

triple (trm_app vf vx) H' Q' This proposition can be slightly simplified, by using wp instead of triple, allowing to eliminate H'. We thus define P vf as:

∀ vx H', wpgen ((x,vx)::nil) t
Overall, the definition of wpgen E t is as follows. Note that the
occurence of nil is replaced with E to account for the case of a
nonempty context.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

...

| trm_fun x t

let P vf :=

(∀ vx H', wpgen ((x,vx)::nil) t

\∀ vf, \[P vf] \−∗ Q vf

...

end.
The actual definition of wpgen exploits an intermediate definition called
wpgen_fun, as shown below:

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

...

| trm_fun x t

...

end. where wpgen_fun is defined as follows:

_{1}Q'._{1}) Q, which we said would take the form \∀ vf, \[P vf] \−∗ Q vf, to define P vf as:∀ vx H' Q', (H' ==> wpgen ((x,vx)::nil) t

_{1}Q') →triple (trm_app vf vx) H' Q' This proposition can be slightly simplified, by using wp instead of triple, allowing to eliminate H'. We thus define P vf as:

∀ vx H', wpgen ((x,vx)::nil) t

_{1}Q' ==> wp (trm_app vf vx) Q'Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

...

| trm_fun x t

_{1}⇒ fun Q ⇒let P vf :=

(∀ vx H', wpgen ((x,vx)::nil) t

_{1}Q' ==> wp (trm_app vf vx) Q') in\∀ vf, \[P vf] \−∗ Q vf

...

end.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

...

| trm_fun x t

_{1}⇒ wpgen_fun (fun vx ⇒ wpgen ((x,vx)::E) t_{1})...

end. where wpgen_fun is defined as follows:

Definition wpgen_fun (Fof:val→formula) : formula := fun Q ⇒

\∀ vf, \[∀ vx Q', Fof vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.

\∀ vf, \[∀ vx Q', Fof vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.

Like for other auxiliary functions associated with wpgen, we introduce a
custom notation for wpgen_fun. Here, we let Fun x := F stand for
wpgen_fun (fun x ⇒ F).

Notation "'Fun' x ':=' F

((wpgen_fun (fun x ⇒ F

(at level 69, x name, right associativity,

format "'[v' '[' 'Fun' x ':=' F

_{1}" :=((wpgen_fun (fun x ⇒ F

_{1})))(at level 69, x name, right associativity,

format "'[v' '[' 'Fun' x ':=' F

_{1}']' ']'").### 2. Treatment of Recursive Functions

_{1}is almost the same as for a non-recursive function. The main difference is that we need to add a binding in the context from the name f to the value vf. Like for trm_fun, the heap predicate wpgen (trm_fix f x t

_{1}) Q is of the form \∀ vf, \[P vf] \−∗ Q vf. The predicate P is similar to that for trm_fun, the only difference is that the context E needs to be extended not with one but with two bindings: one for the argument, and one for the function. Concretely, P is defined as:

∀ vx H', wpgen ((f,vf)::(x,vx)::nil) t

_{1}Q' ==> wp (trm_app vf vx) Q' To wrap up, to hand recursive functions, we define:

Definition wpgen_fix (Fof:val→val→formula) : formula := fun Q ⇒

\∀ vf, \[∀ vx Q', Fof vf vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.

\∀ vf, \[∀ vx Q', Fof vf vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.

Then we integrate this definition is wpgen as shown below.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

| ..

| trm_fix f x t

| ..

end Here again, we introduce a piece of notation for wpgen_fix. We let Fix f x := F stand for wpgen_fix (fun f x ⇒ F).

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

| ..

| trm_fix f x t

_{1}⇒ wpgen_fix (fun vf v ⇒ wpgen ((f,vf)::(x,v)::E) t_{1})| ..

end Here again, we introduce a piece of notation for wpgen_fix. We let Fix f x := F stand for wpgen_fix (fun f x ⇒ F).

Notation "'Fix' f x ':=' F

((wpgen_fix (fun f x ⇒ F

(at level 69, f name, x name, right associativity,

format "'[v' '[' 'Fix' f x ':=' F

_{1}" :=((wpgen_fix (fun f x ⇒ F

_{1})))(at level 69, f name, x name, right associativity,

format "'[v' '[' 'Fix' f x ':=' F

_{1}']' ']'").### 3. Final Definition of wpgen, with Processing a Local Functions

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

| trm_fix f x t

| trm_app t

| trm_seq t

| trm_let x t

| trm_if t

end.

mkstruct match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

_{1}⇒ wpgen_fun (fun v ⇒ wpgen ((x,v)::E) t_{1})| trm_fix f x t

_{1}⇒ wpgen_fix (fun vf v ⇒ wpgen ((f,vf)::(x,v)::E) t_{1})| trm_app t

_{1}t_{2}⇒ wpgen_app (isubst E t)| trm_seq t

_{1}t_{2}⇒ wpgen_seq (wpgen E t_{1}) (wpgen E t_{2})| trm_let x t

_{1}t_{2}⇒ wpgen_let (wpgen E t_{1}) (fun v ⇒ wpgen ((x,v)::E) t_{2})| trm_if t

_{0}t_{1}t_{2}⇒ wpgen_if (isubst E t_{0}) (wpgen E t_{1}) (wpgen E t_{2})end.

### 4. Tactic for Reasoning About Functions

Lemma xfun_spec_lemma : ∀ (S:val→Prop) H Q Fof,

(∀ vf,

(∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →

S vf) →

(∀ vf, S vf → (H ==> Q vf)) →

H ==> wpgen_fun Fof Q.

Proof using.

introv M

applys M

Qed.

Tactic Notation "xfun" constr(S) :=

xseq_xlet_if_needed; xstruct_if_needed; applys xfun_spec_lemma S.

(∀ vf,

(∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →

S vf) →

(∀ vf, S vf → (H ==> Q vf)) →

H ==> wpgen_fun Fof Q.

Proof using.

introv M

_{1}M_{2}. unfold wpgen_fun. xsimpl. intros vf N.applys M

_{2}. applys M_{1}. introv K. rewrite <- wp_equiv. xchange K. applys N.Qed.

Tactic Notation "xfun" constr(S) :=

xseq_xlet_if_needed; xstruct_if_needed; applys xfun_spec_lemma S.

Second, we describe the tactic xfun without argument. It applies to a goal
of the form H ==> wpgen_fun Fof Q. The tactic xfun simply provides an
hypothesis about the local function. The user may subsequently exploit this
hypothesis for reasoning about a call to that function, just like if the
code of the function was inlined at its call site. In practice, the use of
xfun without argument is most relevant for local functions that are
invoked exactly once. For example, higher-order iterators such as
List.iter or List.map are typically invoked with an ad-hoc functions
that appears exactly once.

Lemma xfun_nospec_lemma : ∀ H Q Fof,

(∀ vf,

(∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →

(H ==> Q vf)) →

H ==> wpgen_fun Fof Q.

Proof using.

introv M. unfold wpgen_fun. xsimpl. intros vf N. applys M.

introv K. rewrite <- wp_equiv. xchange K. applys N.

Qed.

Tactic Notation "xfun" :=

xseq_xlet_if_needed; xstruct_if_needed; applys xfun_nospec_lemma.

(∀ vf,

(∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →

(H ==> Q vf)) →

H ==> wpgen_fun Fof Q.

Proof using.

introv M. unfold wpgen_fun. xsimpl. intros vf N. applys M.

introv K. rewrite <- wp_equiv. xchange K. applys N.

Qed.

Tactic Notation "xfun" :=

xseq_xlet_if_needed; xstruct_if_needed; applys xfun_nospec_lemma.

A generalization of xfun that handles recursive functions may be defined
following exactly the same pattern. Details may be found in the file
LibSepReference.v
This completes our presentation of a version of wpgen that recursively
processes the local definition of non-recursive functions. An practical
example is presented next.

Consider the following example program, which involves a local function
definition, then two successive calls to that local function.

We first illustrate a call to xfun with an explicit specification. Here,
the function f is specified as incrementing the reference p. Observe
that the body function of the function f is verified only once. The
reasoning about the two calls to the function f that appears in the code
are done with respect to the specification that we provide as argument to
xfun in the proof script.

Lemma triple_myfun : ∀ (p:loc) (n:int),

triple (trm_app myfun p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+2)).

Proof using.

xwp.

xfun (fun (f:val) ⇒ ∀ (m:int),

triple (f())

(p ~~> m)

(fun _ ⇒ p ~~> (m+1))); intros f Hf.

{ intros.

applys Hf. (* Hf is the name of the hypothesis on the body of f *)

clear Hf.

xapp. (* exploits triple_incr *) xsimpl. }

xapp. (* exploits Hf. *)

xapp. (* exploits Hf. *)

replace (n+1+1) with (n+2); [|math]. xsimpl.

Qed.

triple (trm_app myfun p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+2)).

Proof using.

xwp.

xfun (fun (f:val) ⇒ ∀ (m:int),

triple (f())

(p ~~> m)

(fun _ ⇒ p ~~> (m+1))); intros f Hf.

{ intros.

applys Hf. (* Hf is the name of the hypothesis on the body of f *)

clear Hf.

xapp. (* exploits triple_incr *) xsimpl. }

xapp. (* exploits Hf. *)

xapp. (* exploits Hf. *)

replace (n+1+1) with (n+2); [|math]. xsimpl.

Qed.

We next illustrate a call to xfun without argument. The "generic
specification" that comes as hypothesis about the local function is a
proposition that describes the behavior of the function in terms of the
weakest-precondition of its body. When reasoning about a call to the
function, one can invoke this generic specification. The effect is
equivalent to that of inlining the code of the function at its call site.
The example shown below contains two calls to the function f. The script
invokes xfun without argument. Then, each of the two calls to f executes
a call to incr. Thus the proof script involves two calls to xapp that
each exploit the specification triple_incr.

Lemma triple_myfun' : ∀ (p:loc) (n:int),

triple (trm_app myfun p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+2)).

Proof using.

xwp.

xfun; intros f Hf.

xapp. (* exploits Hf *)

xapp. (* exploits triple_incr *)

xapp. (* exploits Hf *)

xapp. (* exploits triple_incr *)

replace (n+1+1) with (n+2); [|math]. xsimpl.

Qed.

End WPgenRec.

triple (trm_app myfun p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+2)).

Proof using.

xwp.

xfun; intros f Hf.

xapp. (* exploits Hf *)

xapp. (* exploits triple_incr *)

xapp. (* exploits Hf *)

xapp. (* exploits triple_incr *)

replace (n+1+1) with (n+2); [|math]. xsimpl.

Qed.

End WPgenRec.

## Historical Notes

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