# 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

wp t

_{1}(fun r ⇒ wp t

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

_{1}t

_{2}) Q

*compute*the weakest precondition of a term.

*unfolding*its definition. (This sentence will probably make more sense to the reader later on in the chapter.)

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

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

## The Basic Structure of wpgen

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. Recall from the previous chapter that the rule wp_val asserts that Q v entails wp (trm_val v) Q. Well, wpgen (trm_val v) Q is defined as Q v.

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

_{2}) Q) entails wp (trm_let x t

_{1}t

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

_{1}t

_{2}) Q is defined to be wpgen t

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

_{2}) Q), that is, the same expression as in wp_let only with wp replaced by wpgen.

_{1}v

_{2}. How should we define wpgen (trm_app t

_{1}t

_{2}) Q? We need to define it to be a heap predicate, call it H, such that the function call trm_app t

_{1}t

_{2}admits H as precondition and Q as postcondition. In other words, the definition of wpgen (trm_app t

_{1}t

_{2}) Q should consist of a heap predicate H such that triple t H Q holds. We do not know what this H should be, so we simply quantify it existentially. This suggests why the definition of wpgen (trm_app t

_{1}t

_{2}) Q should be \∃ H, H \* \[triple t H Q].

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

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

_{1}t

_{2}, so Coq will reject 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), where v can appear in F

_{2}. 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 going into 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 is the soundness theorem for wpgen, which has 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 H ==> wp t Q from it. The latter is also equivalent to triple t H Q. Thus, wpgen can be viewed as a practical tool for establishing 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

Following this rule, we define wpgen (trm_fun x t

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

match t with

...

| trm_fun x t

| trm_fix f x t

...
An interesting question that arises here is: why does
wpgen (trm_fun x t

_{1}) Q as Q (val_fun x t_{1}). Likewise for recursive functions, we define wpgen (trm_fix f x t_{1}) Q as Q (val_fix f x t_{1}).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})...

_{1}) Q not trigger a recursive call to wpgen on t_{1}? The long answer is detailed in the last section of this chapter (module WPgenRec). The short answer is:- it is not technically needed to recurse in the body of local functions, in the sense that the user does not loose any ability to reason about local functions;
- it may be interesting to recurse the body of local functions because it may save the need for the user to manually invoke the tactic xwp for each local function.

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

... Observe that in the above definition, the second recursive call is invoked on subst x v t

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)... Observe that in the above definition, the second recursive call is invoked on subst x v t

_{2}, which is not a strict subterm of t. As explained earlier, this recursion pattern motivates the introduction of substitution contexts, written E, to delay the computation of substitutions until the leaves of the recursion.### 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}. Yet, typically the function v

_{1}is a function specified in terms of triple. (If v

_{1}is a primitive function, or if it comes from a function argument, it might not even be the case that v

_{1}admits the shape val_fun x t

_{1}.)

_{1}v

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

_{1}v

_{2}) H Q. As suggested earlier in the chapter, the definition of wpgen (trm_app t

_{1}t

_{2}) Q needs to correspond to some heap predicate 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
However, the reasoning rule wp_if stated above features a right-hand side
of the form wp (trm_if (val_bool b) t
The formal definition is:

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, because we are working here with possibly ill-typed programs, this value is not 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). This way, if t_{0}is not a boolean value, then wpgen (trm_if t_{0}t_{1}t_{2}) Q is equivalent to \[False]. Otherwise, if t_{0}is of the form val_bool b, and we are able to perform a case analysis on b, to switch between wpgen t_{1}Q and wpgen t_{2}Q depending on the value of b.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 So Far

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

### Contexts

The "iterated substitution" operation, written isubst E t, describes the
substitution of
Its implementation is standard: the 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 for 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.

*all*the bindings from a context E into a term t.
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 it
reaches 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.
We now present the reformulated 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.

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

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

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

..

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

In the next chapter, we will establish the soundness of the wpgen. For the
moment, we simply state the soundness theorem, then explain how it can be
exploited for verifying concrete programs.

The entailment above asserts in particular that we can derive triple t H Q
by proving H ==> wpgen t Q. A useful corollary combines this soundness
theorem with the rule triple_app_fun, which allows establishing triples
for functions.
Recall triple_app_fun from chapter 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, 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 next 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 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 end of the above proof fragment, the goal takes the form H ==> F Q,
where H denotes the precondition, Q the postcondition, and F is a
formula describing the body of the function incr. Inside this formula, the
reader can spot triples for the primitive operations involved. Observe that
the goal is nevertheless somewhat hard to relate to the original program. In
what follows, we explain how to remedy the situation by setting up wpgen
so that its output is human-readable and resembles the original source code.

### Consequence and Frame Properties for wpgen

#### Exercise: 3 stars, standard, especially useful (wpgen_conseq)

Prove that wpgen E t satisfies the same consequence rule as wp t. The statement is directly adapted from wp_conseq, from WPsem. Hint: begin the proof with intros t. induction t..
Lemma wpgen_conseq : ∀ t E Q

Q

wpgen E t Q

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

☐

_{1}Q_{2},Q

_{1}===> Q_{2}→wpgen E t Q

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

☐

#### Exercise: 4 stars, standard, especially useful (wpgen_frame)

Prove that wpgen E t satisfies the same frame rule as wp t. The statement is directly adapted from wp_frame, from WPsem. The sequence case is not easy.
Lemma wpgen_frame : ∀ t E H Q,

(wpgen E t Q) \* H ==> wpgen E t (Q \*+ H).

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

☐

(wpgen E t Q) \* H ==> wpgen E t (Q \*+ H).

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

☐

## Optimizing the Readability of wpgen's 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, and
- third, we introduce a 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 for 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 below.

Here, F
With the above definitions, wgpen E (trm_seq t
Finally, we introduce a piece of notation for each case. For 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. The "format" clause in the notation definition is there only to improve the pretty-printing of formulae. The semantics of '/' is to encourage a line break. The semantics of square brackets is to delimit blocks. The "v" character next to the leading bracket encourages a vertical alignement of the blocks. Double spaces in the format clause indicate the need to pretty-print a single space, as opposed to an empty spacing.### 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: Notations 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 a handy notation for 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 whitespace, 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 have
achieved is that the output of wpgen is, for any input term t, a human-
readable formula whose display closely resembles the source code of 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.

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

Next, 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 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 remainder 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 four 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 with 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.### X-lemmas for Implementing X-tactics

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 for 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.### Example Proofs using X-lemmas

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

☐

### Definition of X-tactics

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_nosubst 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;

[ first [ reflexivity | eassumption ]

| simpl; unfold wpgen_var; simpl ].

intros; applys xwp_lemma;

[ first [ reflexivity | eassumption ]

| simpl; unfold wpgen_var; simpl ].

Now let us revisit the previous proof scripts using x-tactics instead of
x-lemmas. The reader is invited to 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, prove 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.

☐

### Improved Postprocessing for xapp.

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.
One shortcoming of the version of the xapp tactic that leverages the
triple database is that it is not able to automatically apply
specifications that involve a premise that eauto cannot solve. To exploit
such specifications, we need to provide the specification explicitly using
xapp E. This tactic is defined in LibSepReference.v. Its implementation
is a bit technical, we do not describe it here.

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.

Consider the following program, which defines a local function named f for
incrementing a reference cell p, then invokes f() twice. The purpose of
this example is to illustrate how to reason about a local function.
fun p →

let f = (fun () → incr p) in

f();

f()

let f = (fun () → incr p) in

f();

f()

There are two possible approaches to reasoning about this code.
In the first approach, we store the hypothesis capturing that f has for
code fun () → incr p, and each time we encounter a call to f, we
"inline" the code of f at the call site. This approach is very effective
when f has a unique occurrence. However, if f has multiple occurrences,
then the user has to reason several times about the same code pattern.
The second approach yields a modular proof. When reasoning about the
definition of f, we assert and prove a specification for f, then
immediately discard any information revealing what the code of f is. Then,
each time we encounter a call to f, we use xapp to leverage the
specification of the local function f, exactly like we have been doing
everywhere for reasoning about calls to top-level functions.
Let us illustrate the two approaches, and introduce on the way a few
additional x-tactics relevant for local functions.

### 1. Reasoning about Local Functions by Inlining

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

triple (incrtwice p)

(p ~~> n)

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

Proof using.

xwp.

triple (incrtwice p)

(p ~~> n)

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

Proof using.

xwp.

At this point, we have the formula for the body of the function incrtwice,
which binds (under the name v) the value fun {"u"} ⇒ {incr p}.

xlet.

By typing xlet, we focus on this value fun {"u"} ⇒ {incr p}. The tactic
xval then substitutes this value throughout the remaining of the formula.

xval.

Because the body of incrtwice contains two calls to the local function
f, the resulting formula contains two copies of the function
fun {"u"} ⇒ {incr p}. This kind of duplication, in general, is
problematic, because the size of the formulae grow significantly.

Abort.

We therefore introduce a variant of the xlet tactic, called xletval,
that processes let-bindings by introducing an equality in the Coq context.
For example, for our local function f, a fresh hypothesis named f of
type val is introduced, and an hypothesis of type asserting that f is
equal to fun {"u"} ⇒ {incr p} is provided to characterize the value f.
Let us first defined the tactic xval, then illustrate its usage.
The tactic xletval applies to formulae arising from terms of the form
let x = v

_{1}in t_{2}. It processes the binding let x = v_{1}by introducing in the goal a universal quantification over a variable x and over an hypothesis of type x = v_{1}.
Lemma xletval_lemma : ∀ H v

(∀ x, x = v

H ==> wpgen_let (mkstruct (wpgen_val v

Proof using.

introv M. applys xlet_lemma. apply xstruct_lemma.

apply xval_lemma. applys* M.

Qed.

Tactic Notation "xletval" :=

xstruct_if_needed; applys xletval_lemma.

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

triple (incrtwice p)

(p ~~> n)

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

Proof using.

xwp. xletval. intros f Hf.

_{1}F2of Q,(∀ x, x = v

_{1}→ H ==> F2of x Q) →H ==> wpgen_let (mkstruct (wpgen_val v

_{1})) F2of Q.Proof using.

introv M. applys xlet_lemma. apply xstruct_lemma.

apply xval_lemma. applys* M.

Qed.

Tactic Notation "xletval" :=

xstruct_if_needed; applys xletval_lemma.

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

triple (incrtwice p)

(p ~~> n)

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

Proof using.

xwp. xletval. intros f Hf.

As announced, reasoning about the local function definition using xletval
introduces a name f and an hypothesis Hf of type
f = <{ fun {"u"} ⇒ {incr p} }> There remains to reason about calls to the function f. Let us first show
how it could be done step by step. We will subsequently define a tactic,
named xappfun, to improve conciseness. To reason about the remaining of
the code of incrtwice, we begin by focusing on the first call to f(),
using xseq.

xseq.

At this stage, we can remove the leading mkstruct, unfold the definition
of wgpgen_app, and simplify the resulting statement using xsimpl.

We are left with proving that f() admits a certain behaviour, under the
hypothesis that the code of f is fun {"u"} ⇒ {incr p}. We can make
progress by invoking the tactic xwp, exactly as we do for reasoning about
top-level functions.

xwp.

There remains to reason about the code from the body of the function f,
that is, the instruction incr p. We can use xapp for that purpose.

xapp.

We could similarly handle the second call to f, then complete the proof.
Let us show how to do so in the next lemma, after introducing a tactic to
factorize the proof pattern for reasoning about calls to local functions.

Abort.

The tactic xappfun applies to formulae arising from function calls of the
form f v where f is a local function previously handled using xletval.
Essentially, this tactic inline the formula associated with the body of f,
specializing the body to the argument v.

Lemma xappfun_lemma : ∀ t H Q,

triple t H Q →

H ==> wpgen_app t Q.

Proof using. introv M. unfold wpgen_app. xsimpl*. Qed.

Tactic Notation "xappfun" :=

xseq_xlet_if_needed; xstruct_if_needed; applys xappfun_lemma; xwp.

triple t H Q →

H ==> wpgen_app t Q.

Proof using. introv M. unfold wpgen_app. xsimpl*. Qed.

Tactic Notation "xappfun" :=

xseq_xlet_if_needed; xstruct_if_needed; applys xappfun_lemma; xwp.

Let us revisit the previous proof using this new tactic xappfun.

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

triple (incrtwice p)

(p ~~> n)

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

Proof using.

xwp.

xletval. intros f Hf. (* Reason about the definition of f. *)

xappfun. (* Reason about the 1st call to f. *)

xapp. (* Reason about the call to incr triggered by the 1st call to f. *)

xappfun. (* Reason about the 2nd call to f. *)

xapp. (* Reason about the call to incr triggered by the 2nd call to f. *)

xsimpl. math. (* Conclude the proof. *)

Qed.

triple (incrtwice p)

(p ~~> n)

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

Proof using.

xwp.

xletval. intros f Hf. (* Reason about the definition of f. *)

xappfun. (* Reason about the 1st call to f. *)

xapp. (* Reason about the call to incr triggered by the 1st call to f. *)

xappfun. (* Reason about the 2nd call to f. *)

xapp. (* Reason about the call to incr triggered by the 2nd call to f. *)

xsimpl. math. (* Conclude the proof. *)

Qed.

This completes the presentation of the first approach. As illustrated in the
example proof above, reasoning twice about the body of the function f
leads to some duplication. The second approach shows how to avoid
duplication, by stating and proving a specification for f.

### 2. Reasoning about Local Functions Modularly

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

triple (incrtwice p)

(p ~~> n)

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

Proof using.

triple (incrtwice p)

(p ~~> n)

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

Proof using.

We begin the proof like the previous one.

xwp. xletval. intros f Hf.

As soon as f is introduced, we assert the specification of this function.

To establish this specification, we inline the code of f. This is the one
and only place where we inline the code of f.

intros. subst f.

Then, we complete the verification of f as usual.

xwp. xapp. xsimpl. }

We have introduced an hypothesis Sf that characterizes the behavior of f
by means of a triple. We can drop the hypothesis about the code of f.

clear Hf.

The remaining of the proof now proceeds just like if f was a top-level
function, using xapp for reasoning about each call to f.

xapp.

xapp.

xsimpl.

math.

Qed.

xapp.

xsimpl.

math.

Qed.

The tactic xfun applies to a formula arising from terms of the form
let f = (fun x → t

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

triple <{ f () }> (p ~~> m) (fun _ ⇒ p ~~> (m+1)))

_{1}) in t_{2}. This tactic simulates the invokation of assert over the desired specification for f. The tactic xfun takes as argument the desired specification for the function. For example, in the proof of incrtwice we will use a call of the form:xfun (fun f ⇒ ∀ (m:int),

triple <{ f () }> (p ~~> m) (fun _ ⇒ p ~~> (m+1)))

Lemma xfun_lemma : ∀ (Sof:val→Prop) H v

Sof v

(∀ x, Sof x → H ==> F2of x Q) →

H ==> wpgen_let (mkstruct (wpgen_val v

Proof using. introv Sf M. applys xletval_lemma. intros ? →. applys* M. Qed.

Tactic Notation "xfun" constr(Sof) :=

let f := fresh in let Hf := fresh in

xstruct_if_needed; applys (@xfun_lemma Sof).

_{1}F2of Q,Sof v

_{1}→(∀ x, Sof x → H ==> F2of x Q) →

H ==> wpgen_let (mkstruct (wpgen_val v

_{1})) F2of Q.Proof using. introv Sf M. applys xletval_lemma. intros ? →. applys* M. Qed.

Tactic Notation "xfun" constr(Sof) :=

let f := fresh in let Hf := fresh in

xstruct_if_needed; applys (@xfun_lemma Sof).

We are ready, at last, to show an elegant proof script for incrtwice.

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

triple (incrtwice p)

(p ~~> n)

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

Proof using.

xwp.

triple (incrtwice p)

(p ~~> n)

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

Proof using.

xwp.

The key step is to invoke xfun by providing the desired specification for
the local function f.

The verification of the local function f is similar to that of any
top-level function.

{ xwp. xapp. xsimpl. }

There remains to assign a name to the function and its specification.

intros f Sf.

The rest of the proof is the same as before.

xapp.

xapp.

xsimpl.

math.

Qed.

xapp.

xsimpl.

math.

Qed.

In summary, we have presented the tactic xfun for reasoning about local
functions using the exact same mechanisms as for reasoning about top-level
functions. The only difference is that the specification is not provided by
the user as a lemma, but as an argument to xfun. Using the tactic xfun
leads to modular proofs, whereby the body of the local function is only
processed once by the user.

### 3. Exercises on Local Functions

let f = (fun m → m + 1) in

let a = f 2 in

f a

Definition succtwice : val :=

<{ fun 'n ⇒

let 'f = (fun_ 'm ⇒ 'm + 1) in

let 'a = 'f 'n in

'f 'a }>.

<{ fun 'n ⇒

let 'f = (fun_ 'm ⇒ 'm + 1) in

let 'a = 'f 'n in

'f 'a }>.

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

Verify the function succtwice using xletval and xappfun, without using xfun.
Lemma triple_succtwice_using_xletval : ∀ (n:int),

triple (succtwice n)

\[]

(fun r ⇒ \[r = n + 2]).

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

☐

triple (succtwice n)

\[]

(fun r ⇒ \[r = n + 2]).

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

☐

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

Verify the function succtwice using xfun.
Lemma triple_succtwice_using_xfun : ∀ (n:int),

triple (succtwice n)

\[]

(fun r ⇒ \[r = n + 2]).

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

☐

triple (succtwice n)

\[]

(fun r ⇒ \[r = n + 2]).

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

☐

## Proof Structure and Proof Automation

xapp. { prove_side_1_1. } { prove_side_1_2. }

xapp. { prove_side_2_1. } { prove_side_2_2. } { prove_side_2_3. }

xapp. { prove_side_3_1. } { prove_side_3_2. } { prove_side_3_3. }

xgo. { prove_side_1_1. } { prove_side_1_2. }

{ prove_side_2_1. } { prove_side_2_2. } { prove_side_2_3. }

{ prove_side_3_1. } { prove_side_3_2. } { prove_side_3_3. }

## Additional Tactics xconseq and xframe

Lemma xconseq_lemma : ∀ Q

H ==> mkstruct F Q

Q

H ==> mkstruct F Q

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

Lemma xframe_lemma : ∀ H

H ==> H

H

Q

H ==> mkstruct F Q.

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

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

### 1. Motivation for wpgen to Recurse in Local Functions

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. This 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 simplifies and improves the efficiency of the implementation of the xfun tactic.

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

### 2. A New Definition of wpgen that Recurses in Local 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' 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' Q',

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

triple (trm_app vf vx) H' Q') in

\∀ 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 could be 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' 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

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

(∀ vx H' Q',

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

_{1}Q' →triple (trm_app vf vx) H' 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 could be defined as follows:

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

\∀ vf, \[∀ vx H' Q',

H' ==> Fof vx Q' →

triple (trm_app vf vx) H' Q']

\−∗ Q vf.

\∀ vf, \[∀ vx H' Q',

H' ==> Fof vx Q' →

triple (trm_app vf vx) H' Q']

\−∗ Q vf.

In the definition above, the assumption about vf, enclosed above in
brackets, can be slightly simplfied, by using wp instead of triple,
allowing to eliminate H'. This observation leads to a more concise
definition of wpgen_fun.

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.

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

Prove that wpgen_fun' is equivalent to wpgen_fun.
Lemma wpgen_fun_eq :

wpgen_fun = wpgen_fun'.

Proof using.

unfold wpgen_fun, wpgen_fun'. applys fun_ext_2.

intros Fof Q. applys himpl_antisym.

{ applys himpl_hforall_r. intros vf. xchange (hforall_specialize vf).

xsimpl. intros M. rewrite hwand_hpure_l. xsimpl.

introv. rewrite wp_equiv. applys M. xsimpl. }

(* FILL IN HERE *) Admitted.

☐

wpgen_fun = wpgen_fun'.

Proof using.

unfold wpgen_fun, wpgen_fun'. applys fun_ext_2.

intros Fof Q. applys himpl_antisym.

{ applys himpl_hforall_r. intros vf. xchange (hforall_specialize vf).

xsimpl. intros M. rewrite hwand_hpure_l. xsimpl.

introv. rewrite wp_equiv. applys M. xsimpl. }

(* FILL IN HERE *) Admitted.

☐

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}']' ']'").### 3. 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' Q',

H' ==> wpgen ((f,vf)::(x,vx)::E) t

_{1}Q' →

triple (trm_app vf vx) H' Q' Like for wpgen_fun, we can make the definition more concise by eliminating H'. Concretely, 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

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}']' ']'").### 4. 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.

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

applys himpl_trans_r K. applys N.

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.applys himpl_trans_r 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 with no 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. applys himpl_trans_r 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. applys himpl_trans_r 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. A practical
example is presented next.

We import here the definitions from LibSepReference, which provides the a
definition of wpgen that recurse in function bodies exactly as defined in
subsection 4 above, and which defines all the other x-tactics as previously
but for this recursive version of [wpgen].

Consider again the example program myincr, whose code is:
fun p →

let f = (fun () → incr p) in

f();

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

let f = (fun () → incr p) in

f();

f()

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

triple (trm_app incrtwice 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. *)

xsimpl. math.

Qed.

triple (trm_app incrtwice 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. *)

xsimpl. math.

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_incrtwice' : ∀ (p:loc) (n:int),

triple (trm_app incrtwice 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 *)

xsimpl. math.

Qed.

triple (trm_app incrtwice 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 *)

xsimpl. math.

Qed.

### 7. Exercise on a Local Recursive Function

let g = (fix g i → if i < b then (f i; g (i+1)) end) in

g a

Definition forloop : val :=

<{ fun 'a 'b 'f ⇒

let 'g = (fix_ 'g 'i ⇒

let 'c = 'i < 'b in

if 'c then

'f 'i ;

let 'j = 'i + 1 in

'g 'j

end) in

'g 'a }>.

<{ fun 'a 'b 'f ⇒

let 'g = (fix_ 'g 'i ⇒

let 'c = 'i < 'b in

if 'c then

'f 'i ;

let 'j = 'i + 1 in

'g 'j

end) in

'g 'a }>.

Like for the function repeat, the specification of forloop is expressed
using an invariant, named I, of type int→hprop. The hypothesis on f
asserts that a call to f i takes a state satisfying I i to a state
satisfying I (i+1). For simplicity, we specify the function only in the
case where a ≤ b.

#### Exercise: 4 stars, standard, especially useful (triple_forloop)

Verify the function forloop. Hint: provide the specification of g to xfun. To set up the induction, use the sequence: intros i. induction_wf IH: (upto b) i. intros Hi.. Besides, the tactics math_rewrite is helpful at one point in the proof.
Lemma triple_forloop : ∀ (I:int→hprop) (a b:int) (f:val),

a ≤ b →

(∀ i, a ≤ i ≤ b →

triple (f i)

(I i)

(fun u ⇒ I (i+1))) →

triple (forloop a b f)

(I a)

(fun r ⇒ I b).

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

☐

a ≤ b →

(∀ i, a ≤ i ≤ b →

triple (f i)

(I i)

(fun u ⇒ I (i+1))) →

triple (forloop a b f)

(I a)

(fun r ⇒ I b).

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

☐

## Historical Notes

*pretty*Separation Logic proof featuring local reasoning that is, allowing for maximal usage of the frame rule.

(* 2024-08-25 14:53 *)