First Pass

In the previous chapter, we have introduced a predicate called wp to describe the weakest precondition of a term t with respect to a given postcondition Q. The weakest precondition wp is defined by the equivalence: H ==> wp t Q if and only if triple t H Q. With respect to this "characterization of the semantics of wp", we could prove "wp-style" reasoning rules. For example, the lemma wp_seq asserts: wp t₁ (fun r ⇒ wp t₂ Q) ==> wp (trm_seq t₁ t₂) Q. In this chapter, we introduce a function, called wpgen, to "effectively compute" the weakest precondition of a term. The value of wpgen t is defined recursively over the structure of the term t, and ultimately produces a formula that is logically equivalent to wp t. The major difference between wp and wpgen is that, whereas wp t is a predicate that we can reason about by "applying" reasoning rules, wpgen t is a predicate that we can reason about simply by "unfolding" its definition. Moreover, wp and wpgen differs on the way they handle variable substitution. Consider, e.g., a let-binding. The wp-style reasoning rule for a let-binding introduces a substitution of the form wp (subst x v t₂), which the user must simplify explicitly. On the contrary, when working with wpgen, all the substitutions get automatically simplified during the initial evaluation of wpgen on the source program; the end-user sees none of these substitutions. At a high level, the introduction of wpgen is a key ingredient to smoothening the user-experience of conducting interactive proofs in Separation Logic. The matter of the present chapter is to show:

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

A bonus section explains how to establish the soundness theorem for wpgen. The "first pass" section that comes next is fairly short. It only gives a bird-eye tour of the steps of the construction. Detailed explanations are provided in the main body of the chapter. As first approximation, wpgen t Q is defined as a recursive function that pattern matches on its argument t, and produces the appropriate heap predicate in each case. The definitions somewhat mimic those of wp. For example, where the rule wp_let asserts the entailment, wp t₁ (fun v ⇒ wp (subst x v t₂) Q) ==> wp (trm_let x t₁ t₂) Q, the definition of wpgen is such that wpgen (trm_let x t₁ t₂) Q is, by definition, equal to wpgen t₁ (fun v ⇒ wpgen (subst x v t₂) Q). One special case is that of applications. We define wpgen (trm_app v₁ v₂) as wp (trm_app v₁ v₂), that is, we fall back onto the semantical definition of weakest precondition.
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      | trm_val v ⇒ Q v
      | trm_var x ⇒ \[False]
      | trm_app v₁ v₂ ⇒ wp t Q
      | trm_let x t₁ t₂ ⇒ wpgen t₁ (fun v ⇒ wpgen (subst x v t₂) Q)
      ...
      end. From there, to obtain the actual definition of wpgen, we need to refine the above definition in four steps. In a first step, we modify the definition in order to make it structurally recursive. Indeed, in the above the recursive call wpgen (subst x v t₂) is not made to a strict subterm of trm_let x t₁ t₂, thus Coq refuse this definition as it stands. To fix the issue, we change the definition to the form wpgen E t Q, where E denotes an association list bindings values to variables. The intention is that wpgen E t Q computes the weakest precondition for the term obtained by substituting all the bindings from E in t. (This term is described by the operation isubst E t in the chapter.) The updated definition looks as follows. Observe how, when traversing trm_let x t₁ t₂, 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 that, morally, should have been substituted for 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₁ v₂ ⇒ wp (isubst E t) Q
      | trm_let x t₁ t₂ ⇒ wpgen E t₁ (fun v ⇒ wpgen ((x,v)::E) t₂ Q)
      ...
      end. In a second step, we slightly tweak the definition so as to swap the place where Q is taken as argument with the place where the pattern matching on t occurs. The idea is to make it obvious that wpgen E t can be computed without any knowledge of Q. The type of wpgen E t is (val→hprop)->hprop, a type which we thereafter call formula.
    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 v₁ v₂ ⇒ fun (Q:val→hprop) ⇒ wp (isubst E t) Q
      | trm_let x t₁ t₂ ⇒ fun (Q:val→hprop) ⇒
                              wpgen E t₁ (fun v ⇒ wpgen ((x,v)::E) t₂ Q)
      ...
      end. In a third step, we introduce auxiliary definitions to improve the readability of the output of calls to wpgen. For example, we let wpgen_val v be a shorthand for fun (Q:val→hprop) ⇒ Q v. Likewise, we let wpgen_let F₁ F₂ be a shorthand for fun (Q:val→hprop) ⇒ F₁ (fun v ⇒ F₂ Q). Using these auxiliary definitions, the definition of wpgen rewrites 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₁ t₂ ⇒ wp (isubst E t)
      | trm_let x t₁ t₂ ⇒ wpgen_let (wpgen E t₁) (fun v ⇒ wpgen ((x,v)::E) t₂)
      ...
      end. Each of the auxiliary definitions introduced comes with a custom notation that enables a nice display of the output of wpgen. For example, we set up the notation Let' v := F₁ in F₂ to stand for wpgen_let F₁ (fun v ⇒ F₂). Thanks to this notation, the result of computing wpgen on a source term Let x := t₁ in t₂ (which is an Coq expression of type trm) will be a formula displayed in the form Let' x := F₁ in F₂ (which is an Coq expression of type formula). Thanks to these auxiliary definitions and pieces of notation, the formula that wpgen produces as output reads pretty much like the source term provided as input. In a fourth step, we refine the definition of wpgen in order to equip it with inherent support for applications of the structural rules of the logic, namely the frame rule and the rule of consequence. To achieve this, we consider a well-crafted predicate called mkstruct, and insert it at the head of the output of every call to wpgen, including all its recursive calls. The definition of wpgen thus now admits the following structure.
    Fixpoint wpgen (E:ctx) (t:trm) : formula :=
      mkstruct (match t with
                | trm_val v ⇒ ...
                | ...
                end). Without entering the details, the predicate mkstruct is a function of type formula→formula that captures the essence of the wp-style consequence-frame structural rule. This rule, called wp_conseq_frame in the previous chapter, asserts: Q₁ \*+ H ===> Q₂ → (wp t Q₁) \* H ==> (wp t Q₂). This concludes our little journey towards the definition of wpgen. For conducting proofs in practice, there remains to state lemmas and define tactics to assist the user in the manipulation of the formula produced by wpgen. Ultimately, the end-user only manipulates CFML's "x-tactics" (recall the first two chapters), without ever being required to understand how wpgen is defined. In other words, the contents of this chapter reveals the details that we work very hard to make completely invisible to the end user.

More Details

Definition of wpgen for Term Rules

wpgen computes a heap predicate that has the same meaning as wp. In essence, wpgen takes the form of a recursive function that, like wp, expects a term t and a postcondition Q, and produces a heap predicate. The function is recursively defined and its result is guided by the structure of the term t. In essence, the definition of wpgen admits the following shape:
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      | trm_val v ⇒ ..
      | trm_seq t₁ t₂ ⇒ ..
      | trm_let x t₁ t₂ ⇒ ..
      | trm_var x ⇒ ..
      | trm_app t₁ t₂ ⇒ ..
      | trm_fun x t₁ ⇒ ..
      | trm_fix f x t₁ ⇒ ..
      | trm_if v₀ t₁ t₂ ⇒ ..
      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. Remark: the main difference between wpgen and a "traditional" weakest precondition generator (as the reader might have seen for Hoare logic) is that here we compute the weakest precondition of a raw term, that is, a term not annotated with any invariant or specification.

Definition of wpgen for Values

Consider first the case of a value v. Recall the reasoning rule for values in weakest-precondition style.

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

Definition of wpgen for Functions

Consider the case of a function definition trm_fun x t. Recall that the wp reasoning rule for functions is very similar to that for values.

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₁ ⇒ Q (val_fun x t₁)
      | trm_fix f x t₁ ⇒ Q (val_fix f x t₁)
      ... An important observation is that we here do not attempt to recursively compute wpgen over the body of the function. This is something that we could do, and that we will see how to achieve further on, yet we postpone it for now because it is relatively technical. In practice, if the program features a local function definition, the user may explicitly request the computation of wpgen over the body of that function. Thus, the fact that we do not recursively traverse functions bodies does not harm expressiveness.

Definition of wpgen for Sequence

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

The intention is for wpgen to admit the same semantics as wp. We thus expect the definition of wpgen (trm_seq t₁ t₂) Q to have a similar shape as wp t₁ (fun v ⇒ wp t₂ Q). We therefore define wpgen (trm_seq t₁ t₂) Q as wpgen t₁ (fun v ⇒ wpgen t₂ Q). The definition of wpgen thus gets refined as follows:
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      ...
      | trm_seq t₁ t₂ ⇒ wpgen t₁ (fun v ⇒ wpgen t₂ Q)
      ...

Definition of wpgen for Let-Bindings

The case of let bindings is similar to that of sequences, except that it involves a substitution. Recall the wp rule:

We fill in the dots as follows:
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      ...
      | trm_let x t₁ t₂ ⇒ wpgen t₁ (fun v ⇒ wpgen (subst x v t₂) Q)
      ... One important observation to make at this point is that the function wpgen is no longer structurally recursive. Indeed, while the first recursive call to wpgen is invoked on t₁, which is a strict subterm of t, the second call is invoked on subst x v t₂, which is not a strict subterm of 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.

Definition of wpgen for Variables

We have seen no reasoning rules for establishing a triple for a program variable, that is, to prove triple (trm_var x) H Q. Indeed, trm_var x is a stuck term: its execution does not produce an output. While a source term may contain program variables, all these variables should get substituted away before the execution reaches them. In the case of the function wpgen, a variable bound by let-binding get substituted while traversing that let-binding construct. Thus, if a free variable is reached by wpgen, it means that this variable was originally a dangling free variable, and therefore that the initial source term was invalid. Although we have presented no reasoning rules for triple (trm_var x) H Q nor for H ==> wp (trm_var x) Q, we nevertheless have to provide some meaningful definition for wpgen (trm_var x) Q. This definition should capture the fact that this case must not happen. The heap predicate \[False] captures this intention perfectly well.
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      ...
      | trm_var x ⇒ \[False]
      ... Remark: the definition of \False translates the fact that, technically, we could have stated a Separation Logic rule for free variables, using False as a premise \[False] as precondition. There are three canonical ways of presenting this rule, they are shown next.

All these rules are correct, albeit totally useless.

Definition of wpgen for Function Applications

Consider an application in A-normal form, that is, an application of the form trm_app v₁ v₂. We have seen wp-style rules to reason about the application of a known function, e.g. trm_app (val_fun x t₁) v₂. However, if v₁ is an abstrat value (e.g., a Coq variable of type val), we have no reasoning rule at hand that applies. Thus, we will simply define wpgen (trm_app v₁ v₂) Q as wp (trm_app v₁ v₂) Q. In other words, to define wpgen for a function application, we fall back to the semantic definition of wp. We thus extend the definition of wpgen as follows.
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      ...
      | trm_app v₁ v₂ ⇒ wp (trm_app v₁ v₂) Q
      ... As we carry out verification proofs in practice, when reaching an application we will face a goal of the form:
    H ==> wpgen (trm_app v₁ v₂) Q By revealing the definition of wpgen on applications, we get:
    H ==> wp (trm_app v₁ v₂) Q Then, by exploiting the equivalence with triples, we obtain:
    triple (trm_app v₁ v₂) H Q Such a proof obligation can be discharged by invoking a specification triple for the function v₁. In other words, by falling back to the semantics definition when reaching a function application, we allow the user to choose which specification lemma to exploit for reasoning about this particular function application. Remark: we assume throughout the course that terms are written in A-normal form. Nevertheless, we need to define wpgen even on terms that are not in A-normal form. One possibility is to map all these terms to \[False]. In the specific case of an application of the form trm_app t₁ t₂ where t₁ and t₂ are not both values, it is still correct to define wpgen (trm_app t₁ t₂)) as wp (trm_app t₁ t₂). So, we need not bother checking in the definition of wpgen that the arguments of trm_app are actually values. Thus, the most concise definition for wpgen on applications is:
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      ...
      | trm_app t₁ t₂ ⇒ wp t Q
      ...

Definition of wpgen for Conditionals

The last remaining case is that for conditionals. Recall the wp-style reasoning rule stated using a Coq conditional.

We need to define wpgen for all conditionals in A-normal form, i.e., all terms of the form trm_if (trm_val v₀) t₁ t₂, where v₀ could be a value of unknown shape. Typically, a program may feature a conditional trm_if (trm_var x) t₁ t₂ that, after substitution for x, becomes trm_if (trm_val v) t₁ t₂, for some abstract v of type val that we might not yet know to be a boolean value. Yet, the rule wp_if only applies when the first argument of trm_if is syntactically a boolean value b. To handle this mismatch, we set up wpgen to pattern-match a conditional as trm_if t₀ t₁ t₂, and then express using a Separation Logic existential quantifier that there should exist a boolean b such that t₀ = trm_val (val_bool b). This way, we delay the moment at which the argument of the conditional needs to be shown to be a boolean value. The formal definition is:
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      ...
      | trm_if t₀ t₁ t₂ ⇒
          \∃ (b:bool), \[t₀ = trm_val (val_bool b)]
            \* (if b then (wpgen t₁) Q else (wpgen t₂) Q)
      ...

Summary of the Definition of wpgen for Term Rules

In summary, we have defined:
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      | trm_val v ⇒ Q v
      | trm_fun x t₁ ⇒ Q (val_fun x t)
      | trm_fix f x t₁ ⇒ Q (val_fix f x t)
      | trm_seq t₁ t₂ ⇒ wpgen t₁ (fun v ⇒ wpgen t₂ Q)
      | trm_let x t₁ t₂ ⇒ wpgen t₁ (fun v ⇒ wpgen (subst x v t₂) Q)
      | trm_var x ⇒ \[False]
      | trm_app v₁ v₂ ⇒ wp t Q
      | trm_if t₀ t₁ t₂ ⇒
          \∃ (b:bool), \[t₀ = trm_val (val_bool b)]
            \* (if b then (wpgen t₁) Q else (wpgen t₂) 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₂) Q. Our next step is to fix this issue.

Computing with wpgen

wpgen is not structurally recursive because of the substitutions that takes places in-between recursive calls. To fix this, we are going to delay the substitutions until the leaves of the recursion. To that end, we introduce a substitution context, written E, to record the substitutions that should have been performed. Concretely, we modify the function to take the form wpgen E t, where E denotes a set of bindings from variables to values. The intention is that wpgen E t computes the weakest precondition for the term isubst E t, which denotes the result of substituting all bindings from E inside the term t.

Definition of Contexts and Operations on Them

The simplest way to define a context E is as an association list relating variables to values.

Before we explain how to revisit the definition of wpgen using contexts, we need to define the "iterated substitution" operation. This operation, written isubst E t, describes the substitution of all the bindings form E inside a term t. The definition of iterated substitution is relatively standard: we traverse the term recursively and, when reaching a variable, we perform a lookup in the context E. We need to take care to respect variable shadowing. To that end, when traversing a binder that binds a variable x, we remove all occurrences of x that might exist in E. 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.

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

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.

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

When wpgen traverses a let-binding, rather than eagerly performing a substitution, it simply extends the current context. Concretely, a call to wpgen E (trm_let x t₁ t₂) triggers a recursive call to wpgen ((x,v)::E) t₂. The corresponding definition is:
  Fixpoint wpgen (E:ctx) (t:trm) : formula :=
    mkstruct (match t with
      ...
      | trm_let x t₁ t₂ ⇒ fun Q ⇒
           (wpgen E t₁) (fun v ⇒ wpgen ((x,v)::E) t₂)
      ...
      ) end.

wpgen: the Variable Case

When wpgen reaches a variable, it lookups for a binding on the variable x inside the context E. Concretely, the evaluation of wpgen E (trm_var x) triggers a call to lookup x E. If the context E binds the variable x to some value v, then the operation lookup x E returns Some v. In that case, wpgen returns the weakest precondition for that value v, that is, Q v. Otherwise, if E does not bind x, the lookup operation returns None. In that case, wpgen returns \[False], which we have explained to be the weakest precondition for a stuck program.
  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

In the previous definition of wpgen (the one without contexts), we argued that, in the case where t denotes an application, the result of wpgen t Q should be simply wp t Q. In the definition of wpgen with contexts, the interpretation of wpgen E t is the weakest precondition of the term isubst E t (which denotes the result of substituting variables from E in t). When t is an application, we thus define wpgen E t as the formula fun Q ⇒ wp (isubst E t) Q, which simplifies to wp (isubst E t) after eliminating the eta-expansion.
  Fixpoint wpgen (t:trm) : formula :=
    mkstruct (match t with
      ...
      | trm_app v₁ v₂ ⇒ wp (isubst E t)
      ..

wpgen: the Function Definition Case

Consider the case where t is a function definition, for example trm_fun x t₁. Here again, the formula wpgen E t is interpreted as the weakest precondition of isubst E t. By unfolding the definition of isubst in the case where t is trm_fun x t₁, we obtain trm_fun x (isubst (rem x E) t₁). The corresponding value is trm_val x (isubst (rem x E) t₁). The weakest precondition for that value is fun Q ⇒ Q (val_fun x (isubst (rem x E) t₁)). Thus, wpgen E t handles functions, and recursive functions, as follows:
  Fixpoint wpgen (E:ctx) (t:trm) : formula :=
    mkstruct (match t with
      ...
      | trm_fun x t₁ ⇒ fun Q ⇒ Q (val_fun x (isubst (rem x E) t₁))
      | trm_fix f x t₁ ⇒ fun Q ⇒ Q (val_fix f x (isubst (rem x (rem f E)) t₁))
      ...
      ) end.

wpgen: at Last, an Executable Function

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.

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. Moreover, it is algorithmically more efficient in general, because it performs substitutions lazily rather than eagerly. Let us state the soundness theorem and its corollary for establishing triples for functions.

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.

Reformulating the rule above into a rule for wpgen takes 3 steps. First, we rewrite the premise triple (subst x v₂ t₁) H Q using wp. It becomes H ==> wp (subst x v₂ t₁) Q. Second, we observe that the term subst x v₂ t₁ is equal to isubst ((x,v₂)::nil) t₁. (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₂ t₁) Q is equivalent to wp (isubst ((x,v₂)::nil) t₁). Third, according to wpgen_sound, the predicate wp (isubst ((x,v₂)::nil) t₁) is entailed by wpgen ((x,v₂)::nil) t₁. Thus, we can use the latter as premise in place of the former. We thereby obtain the following lemma.

Executing wpgen on a Concrete Program

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.

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

To improve the readability of the formulae produced by wpgen, we take the following 3 steps:

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

We distribute the fun Q into the branches of the match t. Concretely, we change from:
 Fixpoint wpgen (E:ctx) (t:trm) (Q:val→hprop) : hprop :=
   match t with
   | trm_val v ⇒ Q v
   | trm_fun x t₁ ⇒ Q (val_fun x (isubst (rem x E) t₁))
   ...
   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₁ ⇒ fun (Q:val→hprop) ⇒ Q (val_fun x (isubst (rem x E) t₁))
   ...
   end. The result type of wpgen E t is (val→hprop)->hprop. Thereafter, we let formula be a shorthand for this type.

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

We introduce auxiliary definitions to denote the result of each of the branches of the match t construct. Concretely, we change from:
    Fixpoint wpgen (E:ctx) (t:trm) : formula :=
      match t with
      ...
      | trm_seq t₁ t₂ ⇒ fun Q ⇒ (wpgen E t₁) (fun v ⇒ wpgen E t₂ Q)
      ...
      end. to the equivalent form:
    Fixpoint wpgen (E:ctx) (t:trm) : formula :=
      match t with
      ...
      | trm_seq t₁ t₂ ⇒ wpgen_seq (wpgen E t₁) (wpgen E t₂)
      ...
     end. where wpgen_seq is defined as shown below.

Remark: above, F₁ and F₂ denote the results of the recursive calls, wpgen E t₁ and wpgen E t₂, respectively. With the above definitions, wgpen E (trm_seq t₁ t₂) evaluates to wp_seq (wpgen E t₁) (wpgen E 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₁ F₂ gets displayed as Seq F₁ ; F₂ .

Thanks to this notation, the wpgen of a sequence t₁ ; t₂ displays as Seq F₁ ; F₂ where F₁ and F₂ denote the wpgen of t₁ and t₂, respectively.

Readability Step 2: Auxiliary Definitions for other Constructs

We generalize the approach illustrated for sequences to every other term construct. The corresponding definitions are stated below. It is not required to understand the details in this subsection.

The new definition of wpgen reads as follows.

This definition is, up to unfolding of the new intermediate definitions, totally equivalent to the previous one. We will prove the soundness result and its corollary further on.

Readability Step 3: Notation for Auxiliary Definitions

We generalize the notation introduced for sequences to every other term construct. The corresponding notation is defined below. It is not required to understand the details from this subsection. To avoid conflicts with other existing notation, we write Let' and If' in place of Let and If. Here again, it is not required to understand all the details.

In addition, we introduce handy notation of the result of wpgen t where t denotes an application.

Test of wpgen with Notation.

Consider again the example of incr.

Up to proper tabulation, alpha-renaming, and removal of parentheses (and dummy 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.

Extension of wpgen to Handle Structural Rules

The definition of wpgen proposed so far integrates the logic of the reasoning rules for terms, however it lacks support for conveniently exploiting the structural rules of the logic. We fix this next, by showing how to tweak the definition of wpgen in such a way that, by construction, it satisfies both:

• the frame rule, which asserts (wpgen t Q) \* H ==> wpgen t (Q \*+ H),
• and the rule of consequence, which asserts that Q₁ ===> Q₂ implies wpgen t Q₁ ==> wpgen t Q₂.

Introduction of mkstruct in the Definition of wpgen

Recall from the previous chapter the statement of the frame rule in wp-style.

We would like wpgen to satisfy the same rule, so that we can exploit the frame rule while reasoning about a program using the heap predicate produced by wpgen. With the definition of wpgen set up so far, it is possible to prove, for any concrete term t, that the frame property (wpgen t Q) \* H ==> wpgen t (Q \*+ H) holds. However, establishing this result requires an induction over the entire structure of the term t---a lot of tedious work. Instead, we are going to tweak the definition of wpgen so as to produce, at every step of the recursion, a special token to capture the idea that whatever the details of the output predicate produced by wpgen, this predicate does satisfy the frame property. We achieve this magic by introducing a predicate called mkstruct, and inserting it at the head of the output produced by wpgen (and all of its recursive invocation) as follows:
    Fixpoint wpgen (E:ctx) (t:trm) : (val→hprop)->hprop :=
      mkstruct (
        match t with
        | trm_val v ⇒ wpgen_val v
        ...
        end). The interest of the insertion of mkstruct above is that every result of a computation of wpgen t on a concrete term t is, by construction, of the form mkstruct F for some argument F. There remains to investigate how mkstruct should be defined.

Properties of mkstruct

Let us state the properties that 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.

There remains to find a suitable definition for mkstruct that enables the frame property and the consequence property. These properties can be stated by mimicking the rules wp_frame and wp_conseq.

In addition, it should be possible to erase mkstruct from the head of the output produced wpgen t when we do not need to apply any structural rule. In other words, we need to be able to prove H ==> mkstruct F Q by proving H ==> F Q, for any H. This erasure property is captured by the following entailment.

Moreover, mkstruct should be monotone with respect to the formula: if F₁ is stronger than F₂, then mkstruct F₁ should be stronger then mkstruct F₂.

Realization of mkstruct

Fortunately, it turns out that there exists a predicate mkstruct satisfying the four required properties. To begin with, let us just pull out of our hat a definition of mkstruct that works.

We postpone to a bonus section the discussion of why it works and of how one could have guessed this definition. Again, it really does not matter the details of the definition of mkstruct. All that matters is that mkstruct satisfies the three required properties: mkstruct_frame, mkstruct_conseq, and mkstruct_erase. Let us establish these properties for the definition considered. (Proof details can be skipped over.)

An interesting property of mkstruct is it has no effect on a formula of the form wp t. Intuitively, such a formula already satisfies all the structural reasoning rules, hence adding mkstruct to it does not increase its expressive power.

Another interesting property of mkstruct is its idempotence property, that is, it is such that mkstruct (mkstruct F) = mkstruct F. Idempotence asserts that applying the predicate mkstruct more than once does not provide more expressiveness than applying it just once. Intuitively, idempotence reflects in particular the fact that two nested applications of the rule of consequence can always be combined into a single application of that rule (due to the transitivity of entailment); and that, similarly, two nested applications of the frame rule can always be combined into a single application of that rule (framing on H₁ then framing on H₂ is equivalent to framing on H₁ \* H₂).

Exercise: 3 stars, standard, especially useful (mkstruct_idempotent)

Complete the proof of the idempotence of mkstruct. Hint: leverage xpull and xsimpl.

Definition of wpgen that Includes mkstruct

Our final definition of wpgen refines the previous one by inserting the mkstruct predicate to the front of the match t with construct.

Again, we assert the soundness theorem and its corollary, and we postpone the proof.

Notation for mkstruct and Test

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.

Let us test again the readability of the output of wpgen on a concrete example.

Up to proper tabulation, alpha-renaming, and removal of parentheses (and dummy quotes after Let and If), F reads as:
    `Let n := `(App val_get p) in
    `Let m := `(App (val_add n) 1) in
    `App (val_set p) m

Lemmas for Handling wpgen Goals

The last major step of the setup of our Separation Logic based verification framework consists of lemmas and tactics to assist in the processing of formulas produced by wpgen. For each term construct, and for mkstruct, we introduce a dedicated lemma, called "x-lemma", to help with the elimination of the construct. xstruct_lemma is a reformulation of mkstruct_erase.

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.

Likewise, xseq_lemma reformulates wpgen_seq.

xapp_lemma applies to goals produced by wpgen on an application. In such cases, the proof obligation is of the form H ==> wp t Q. xapp_lemma reformulates the frame-consequence rule, and states the premise of the rule using a triple, because triples are used for stating specification lemmas.

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

An Example Proof

Let us illustrate how the "x-lemmas" help clarifying verification proof scripts.

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

Using x-lemmas, verify the proof of triple_succ_using_incr. (The proof was carried out using triples in chapter Rules.)

Making Proof Scripts More Concise

For each x-lemma, we introduce a dedicated tactic to apply that lemma and perform the associated bookkeeping. xstruct eliminates the leading mkstruct.

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

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

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

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

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

Using x-tactics, verify the proof of succ_using_incr.

Further Improvements to the xapp Tactic.

In this section, we describe two improvements to the xapp tactic. The pattern xapp_nosubst E. intros ? ->. appears frequently in the above proofs. This pattern is typically useful whenever the specification E features a postcondition of the form fun v ⇒ \[v = ..] or of the form fun v ⇒ \[v = ..] \* ... Likewise, the pattern xapp_nosubst E. intros ? p ->. appears frequently. This pattern is typically useful whenever the specification E features a postcondition of the form fun v ⇒ \∃ p, \[v = ..] \* ... . It therefore makes sense to introduce a tactic xapp E that, after calling xapp_nosubst E, attempts to invoke intros ? → or intros ? x ->; revert x. In the latter case, to ensure that the name x that we use does not modify the existing name of the bound variable, we play some Ltac hacks, captured by the tactic xapp_try_subst.

Explicitly providing arguments to xapp_nosubst or xapp is very tedious. To avoid that effort, we can set up the tactics to automatically look up for the relevant specification. To that end, we instrument eauto to exploit a database of already-established specification triples. This database, named triple, can be populated using the Hint Resolve ... : triple command, as illustrated below.

The argument-free variants xapp_subst and xapp are implemented by invoking eauto with triple to retrieve the relevant specification. The definition from Direct is slightly more powerful, in that it is also able to pick up an induction hypothesis from the context for instantiating the triple. DISCLAIMER: the tactic xapp that leverages the triple database is not able to automatically apply specifications that feature a premise that eauto cannot solve. To exploit such specifications, one need to provide the specification explicitly (using xapp E), or to exploit a more complex hint mechanism (as done in CFML). (A poor-man's workaround consists in moving all the premises inside the precondition, however doing so harms readability.)

Demo of a Practical Proof using x-Tactics.

The proof script for the verification of incr using the tactic xapps with implicit argument.

In order to enable automatically exploiting the specification of triple in the verification of succ_using_incr, which includes a function call to triple, we add it to the hint database triple.

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

Using the improved x-tactics, verify the proof of succ_using_incr.

In summary, thanks to wpgen and its associated x-tactics, we are able to verify concrete programs in Separation Logic with concise proof scripts.

Optional Material

Tactics xconseq and xframe

The tactic xconseq applies the weakening rule, from the perspective of the user, it replaces the current postcondition with a stronger one. Optionally, the tactic can be passed an explicit argument, using the syntax xconseq Q. The tactic is implemented by applying the lemma xconseq_lemma, stated below.

Exercise: 1 star, standard, optional (xconseq_lemma)

Prove the xconseq_lemma.

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.

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