First Pass

This chapter introduces support for additional language constructs:

• assertions,
• if-statements that are not in A-normal form (needed for loops)
• while-loops,
• n-ary functions (bonus contents).

Regarding assertions, we present a reasoning rule such that:

• assertions may access to mutable data,
• assertions may perform local side-effects,
• the program remains correct whether assertions are executed or not.

Regarding loops, we explain why traditional Hoare-style reasoning rules based on loop invariants are limited, in that they prevent useful applications of the frame rule. We present alternative reasoning rules compatible with the frame rule, and demonstrate their benefits on practical examples. Regarding n-ary functions, that is, functions with several arguments, there are essentially three possible approaches:

• native n-ary functions, e.g., function(x, y) { t } in C syntax;
• curried functions, e.g., fun x ⇒ fun y ⇒ t in OCaml syntax;
• tupled functions, e.g., fun (x,y) ⇒ t in OCaml syntax.

In this chapter, we describe the first two approaches. The third approach (tupled functions) would require product data types in the source language.

Reasoning Rule for Assertions

Assume an additional primitive operation, allowing to write terms of the form val_assert t, to dynamically check at runtime that the term t produces the boolean value true, equivalently to the OCaml expression assert(t).

The reasoning rule for assertions should ensure that:

• the body of the assertion always evaluates to true,
• the program remains correct if the assertion is not evaluated.

Let us introduce a boolean flag to control the evaluation of assertions. The value of this flag is purposely left unspecified.

The program should be correct for both possible values of evaluate_assertions. The semantics of the evaluation of assertions is formally captured by the following two rules.

• The rule eval_assert_enabled applies when evaluate_assertions is set to true. The rule describes the evaluation of the body of the assertion, and the check that the output value is true.
• The rule eval_assert_disabled applies when evaluate_assertions is set to false. The rule totally ignores the body of the assertion. It treats the assertion as immediately returning the unit value, in the current state.

Note that it might be tempting to consider a "unifying" evaluation rule that evaluates the body of the assertion, checks that the result is true, and, moreover, imposes that the assertion does not modify the state.

Yet, such a rule would be overly restrictive, for two reasons. First, it might be useful for an assertion to allocate local data for evaluating a particular property. Second, there are useful examples of assertions that do modify existing cells from the heap. For example, an assertion that appears in real programs is assert (find x = find y), where the find operation finds the representative of a node from a Union-Find data structure, an operation that performs path compression. At this point, our goal is to state a reasoning rule for val_assert t that does not depend on the value of the boolean flag evaluate_assertions. In other words, we are seeking for a rule that is correct both with respect to eval_assert_enabled and with respect to eval_assert_disabled. Consider the evaluation of val_assert t in a state described by H. The output state should still be described by H, although the internal representation of the state might have changed (e.g., for path compression in the case of a Union-Find data structure). The body of the assertion should evaluate correctly in a state described by H, and should return the value true, in an output state still described by H. As usual for primitive operations, we first establish a rule for Hoare triples, then deduce a rule for Separation Logic triples.

Semantics of Conditionals not in Administrative Normal Form

To state reasoning rule for while-loops in a concise manner, it is useful to generalize the construct if b then t₁ else t₂ to the form if t₀ then t₁ else t₂. To specify the behavior of a term of the form if t₀ then t₁ else t₂, let us assume the evaluation rule shown below. This rule generalizes the rule eval_if. It first evaluates t₀ into a value v₀, then it evaluates the term if v₀ then t₁ else t₂.

With respect to this evaluation rule eval_if_trm, we can prove a correpsonding reasoning rule. We first state it in Hoare-logic, then in Separation Logic, following the usual proof pattern.

The reasoning rule can also be reformulated in weakest-precondition form. The rule below generalizes the rule wp_if.

Semantics and Basic Evaluation Rules for While-Loops

Assume the grammar of term to be extended with a loop construct trm_while t₁ t₂, corresponding to the OCaml expression while t₁ do t₂, and written While t₁ Do t₂ Done in our example programs.

The semantics of this loop construct can be described in terms of the one-step unfolding of the loop: while t₁ do t₂ is a term that behaves exactly like the term if t₁ then (t₂; while t₁ do t₂) else ().

This evaluation rule translates directly into a reasoning rule: to prove a triple for the term while t₁ do t₂, it suffices to prove a triple for the term if t₁ then (t₂; while t₁ do t₂) else (). There is a catch in that reasoning principle, namely the fact that the loop while t₁ do t₂ appears again inside the term if t₁ then (t₂; while t₁ do t₂) else (). Nevertheless, this is not a problem if the user is carrying out a proof by induction. In that case, an induction hypothesis about the behavior of while t₁ do t₂ is available. We show an example proof further on. For the moment, let us state the reasoning rules.

Separation-Logic-friendly Reasoning Rule for While-Loops

One may be tempted to introduce an invariant-based reasoning rule for while loops. Traditional invariant-based rules from Hoare logic usually admit a relatively simple statement, because they only target partial correctness, and because the termination condition is restricted to a simple expression that does not alter the state. In our set up, targeting total correctness and a construct of the form trm_while t₁ t₂, the invariant-based reasoning rule can be stated as shown below. An invariant I describes the state at the entry and exit point of the loop. This invariant is actually of the form I b X, where the boolean value b is false to indicate that the loop has terminated, and where the value X belongs to a type A used to express the decreasing measure that justifies the termination of the loop.

The above rule is correct yet limited, because it precludes the possibility to apply the frame rule "over the remaining iterations of the loop". This possibility can be exploited by carrying a proof by induction and invoking the rule triple_while, which unfolds the loop body. In that scheme, the frame rule can be applied to the term while t₁ do t₂ that occurs in the if t₁ then (t₂; (while t₁ do t₂)) else (). We can reduce the noise associated with applying the rule triple_while by assigning a name, say t, to denote the term while t₁ do t₂. The correpsonding rule, shown below, asserts that t admits the same behavior as the term if t₁ then (t₂; t) else ().

The proof scheme that consists of setting up an induction then applying the reasoning rule triple_while' can be factored into the following lemma, which is stated using an invariant that appears only in the precondition. The postcondition is an abstract Q. With this presentation, the rule features an "invariant", yet it remains possible to invoke the frame rule over the "remaining iterations" of the loop.

The rule triple_while_inv admits a constrained precondition of the form (\∃ b X, I b X). To exploit this rule, one almost always needs to first invoke the consequence-frame rule. The rule triple_while_inv_conseq_frame, shown below, conveniently bakes in frame and consequence rules into the statement of triple_while_inv.

The above rule can be equivalently reformulated in weakest-precondition style.

More Details

Semantics and Basic Evaluation Rules for For-Loops

In the previous section, we have focused on while loops and presented encodings, evaluation rules, and reasoning rules. In this section, we present a similar construction for for-loops. A for loop takes the form trm_for x n₁ n₂ t₃, matching the OCaml syntax for x = n₁ to n₂ do t₃ done. We assume the bounds n₁ and n₂ to be already evaluated to integers---i.e., we assume A-normal form.

The semantics of for x = n₁ to n₂ do t₃ is encoded using a conditional. If n₁ ≤ n₂, then we execute the body t₃ with x bound to n₁ (that is, subst x n₁ t₃), and continue with the remainig iterations, which are described by for x = n₁+1 to n₂ do t₃ done. Eventually, we reach a situation where n₁ > n₂. At this point, the loop terminates, and returns the unit value.

The direct reasoning rules for for-loops w.r.t. Hoare triples and Separation Logic triples simply unfold the encoding.

Just like for while loops, we can reduce the noise associated with applying the rule triple_for, by pre-processing the encoding based on the conditional. This rule may be useful for carrying out proofs by induction. Follow carefully through the proof, as it exhibits reasoning patterns that are useful for the follow-up exercises.

We can derive a simpler rule for the case of loops with no iterations.

Exercise: 4 stars, standard, optional (triple_for_ge)

Prove the specification of for loops in the case where the lower bound of the loop exceeds the upper bound of the loop. Hint: the proof shares similarities with that of triple_for'.

We can derive an reasoning rule expressed using a loop invariant: if I n₁ holds before the loop, and each iteration takes the state from I i to I (i+1), then I (n₂+1) holds after the last iteration. The benefits of this presentation, compared with triple_for', is that it bakes in the application of the induction principle.

Exercise: 5 stars, standard, especially useful (triple_for_inv_conseq_frame)

Prove the invariant-based reasoning rule for for-loops. Hint: the proof shares similarities with that of triple_for'.

Treatment of Generalized Conditionals and Loops in wpgen

The formula generator wpgen may be extended to take into account the generalized form if t₀ then t₁ else t₂. The corresponding formula is wpgen_let (aux t₀) (fun v ⇒ mkstruct (wpgen_if v (aux t₁) (aux t₂)), where wpgen_let is used to compute the wpgen of the argument of the conditional, and where wpgen_if is used to compute the wpgen of a conditional with a argument already evaluated to a value. This pattern is captured by the auxiliary definition wpgen_if_trm.
    Fixpoint wpgen (E:ctx) (t:trm) : hprop :=
      mkstruct match t with
      ...
      | trm_if t₀ t₁ t₂ ⇒ wpgen_if_trm (wpgen t₀) (wpgen t₁) (wpgen t₂)
      ... where wpgen_if_trm is defined as shown below.

The soundness of this extension of wpgen is captured by the following lemma.

To handle while loops in wpgen, we introduce the auxiliary definition wpgen_while.
    Fixpoint wpgen (E:ctx) (t:trm) : hprop :=
      mkstruct match t with
      ...
      | trm_while t₁ t₂ ⇒ wpgen_while (wpgen t₁) (wpgen t₂)
      ... The definition of wpgen_while quantifies over an abstract formula F, while denotes the behavior of the while loop. The weakest precondition for the loop w.r.t. postcondition Q is described as F Q, or, more precisely mkstruct F Q, to keep track of the fact that F denotes a formula on which one may apply any structural reasoning rule. To establish that mkstruct F Q is entailed by the heap predicate that describes the current state, the user is provided with an assumption: the fact that mkstruct F Q' can be proved from the weakest precondition of the term if t₁ then (t₂; t₃) else (), where the weakest precondition of t₃, which denotes the recursive call to the loop, is described by F.

Let us axiomatize the fact that wpgen is generalized to handle the new term construct trm_while t₁ t₂.

The soundness proof of wpgen with respect to the treatment of while-loops goes as follows.

Notation and Tactics for Manipulating While-Loops

The associated piece of notation for displaying characteristic formulae are defined as follows.

The tactic xapply is useful for applying an assumption of the form H ==> mkstruct F Q to a goal of the form H' ==> mkstruct F Q', with the ramified frame rule relating H, H', Q and Q'. In essence, xapply applies an hypothesis "modulo consequence-frame".

The tactic xwhile is useful for reasoning about a while-loop. In essence, the tactic while applies the reasoning rule wp_while.

Note: a similar construction could be set up for dealing with for loops.

Example of the Application of Frame During Loop Iterations

Consider the following function, which computes the length of a linked list with head at location p, using a while loop and a reference named a to count the number of cells being traversed.     let mlength_loop p =
      let a = ref 0 in
      let r = ref p in
      while !r != null do
        incr a;
        r := (!r).tail;
      done;
      let n = !a in
      free a;
      free r;
      n

This function is specified and verified as follows.

Let's compute the weakest precondition and pretend that xwpgen includes support for loops.

We call the xwhile tactic to handle the loop. The formula F then denotes "the behavior of the loop".

We next state the induction principle for the loop, in the form I p n ==> F Q, where I p n denotes the loop invariant, and Q describes the final output of the loop.

We carry out a proof by induction on the length of the list L.

At this point, we reason about the recursive call. We use the tactic xapply to apply the induction hypothesis modulo the frame rule. Here, the head cell of the list is framed out over the scope of the recursive call, which operates only on the tail of the list.

Reasoning Rule for Loops in an Affine Logic

Recall from Affine the combined structural rule that includes the affine top predicate \GC.

In that setting, it is useful to integrate \GC into the rule triple_while_inv_conseq_frame, to allow discarding the data allocated by the loop iterations but not described in the final postcondition.

Curried Functions of Several Arguments

We next give a quick presentation of the notation, lemmas and tactics involved in the manipulation of curried functions of several arguments. We focus here on the particular case of recursive functions with 2 arguments, to illustrate the principles at play. Set up for non-recursive and recursive functions of arity 2 and 3 can be found in the file LibSepReference. One may attempt to generalize these definitions to handle arbitrary arities. Yet, to obtain an arity-generic treatment of functions, it appears simpler to work with primitive n-ary functions, whose treatment is presented in the next section. Consider a curried recursive functions that expects two arguments: val_fix f x₁ (trm_fun x₂ t) describes such a function, where f denotes the name of the function for recursive calls, x₁ and x₂ denote the arguments, and t denotes the body. Observe that the inner function, the one that expects x₂, is not recursive, and that it is not a value but a term (because it may refer to the variable x₁ bound outside of it). We introduce the notation Fix f x₁ x₂ := t for such a recursive function with two arguments.

An application of a function with two arguments takes the form f v₁ v₂, which is actually parsed as trm_app (trm_app f v₁) v₂. This expression is an application of a term to a value, and not of a value to a value. Thus, this expression cannot be evaluated using the rule eval_app_fun. We therefore need a distinct rule for first evaluating the arguments of a function application to values, before we can evaluate the application of a value to a value. The rule eval_app_args serves that purpose. To state it, we first need to characterize whether a term is a value or not, using the predicate trm_is_val t defined next.

The statement of eval_app_args is as shown below. For an expression of the form trm_app t₁ t₂, where either t₁ or t₂ is not a value, it enables reducing both t₁ and t₂ to values, leaving a premise describing the evaluation of a term of the form trm_app v₁ v₂, for which the rule eval_app_fun applies.

Using the above rule, we can establish an evaluation rule for the term v₀ v₁ v₂. There, v₀ denotes a recursive function of two arguments named x₁ and x₂, the values v₁ and v₂ denote the two arguments, and f denotes the name of the function available for making recursive calls from the body t₁. The key idea is that the behavior of v₀ v₁ v₂ is similar to that of the term subst x₂ v₂ (subst x₁ v₁ (subst f v₀ t₁)). We state this property using the predicate eval_like, introduced in the chapter Rules.

We next derive the specification triple for applications of the form v₀ v₁ v₂.

The reasoning rule above can be reformulated in weakest-precondition style.

Finally, it is useful to extend the tactic xwp, so that it exploits the rule wp_app_fix2 in the same way as it exploits wp_app_fix. To that end, we state a lemma featuring a conclusion expressed as a triple, and a premise expressed using wpgen. Observe the substitution context associated with wpgen: it is instantiated as (f,v₀)::(x₁,v₁)::(x₂,v₂)::nil, so as to perform the relevant substitutions. Note also how the side-condition expressing the freshness conditions on the variables, using a comparison function for variables that computes in Coq.

The lemma gets integrated into the implementation of xwp as follows.

This tactic xwp also appears in the file LibSepReference.v. It is exploited in several examples from the chapter Basic.

Primitive n-ary Functions

We next present an alternative treatment to functions of several arguments. The idea is to represent function arguments using lists. The verification tool CFML is implemented following this approach. On the one hand, the manipulation of lists adds a little bit of boilerplate. On the other hand, when using this representation, all the definitions and lemmas are inherently arity-generic, that is, they work for any number of arguments. We introduce the short names vars, vals and trms to denote lists of variables, lists of values, and lists of terms, respectively. These names are not only useful to improve conciseness, they also enable the set up of useful coercions, as illustrated further on.

We assume the grammar of terms and values to include primitive n-ary functions and primitive n-ary applications, featuring list of arguments. Thereafter, for conciseness, we focus on the treatment of recursive functions, and do not describe the simpler case of non-recursive functions.

The substitution function is a bit tricky to update for dealing with list of variables. A definition along the following lines computes well, and is recognized as structurally recursive by Coq.
    Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
      let aux t := (subst y w t) in
      let aux_no_captures xs t := (If List.In y xs then t else aux t) in
      match t with
      | trm_fixs f xs t₁ ⇒ trm_fixs f xs (If f = y then t₁ else
                                            aux_no_captures xs t₁)
      | trm_apps t₀ ts ⇒ trm_apps (aux t₀) (List.map aux ts)
      ...
     end. The evaluation rules also need to be updated to handle list of arguments. A n-ary function from the grammar of terms evaluates to the corresponding n-ary function from the grammar of values.

Note that, for technical reasons, we need to ensure that list of arguments is nonempty. Indeed, a function with zero arguments would beta-reduce to its body as soon as it is defined, because it is not waiting for any argument, resulting in an infinite sequence of reductions. The application of a n-ary function to values takes the form trm_apps (trm_val v₀) ((trm_val v₁):: .. ::(trm_val vn)::nil). If the function v₀ is defined as val_fixs f xs t₁, where xs denotes the list x₁::x₂::...::xn::nil, then the beta-reduction of the function application triggers the evaluation of the term subst xn vn (... (subst x₁ v₁ (subst f v₀ t₁)) ...). To describe the evaluation rule in an arity-generic way, we need to introduce the list vs made of the values provided as arguments, that is, the list v₁::v₂::..::vn::nil. With this list vs, the n-ary application can then be written as the term trm_apps (trm_val v₀) (trms_vals vs), where the operation trms_vals converts a list of values into a list of terms by applying the constructor trm_val to every value from the list.

Note that we declare the operation trms_vals as a coercion, just like trm_val is a coercion. Doing so enables us to write a n-ary application in the form v₀ vs. To describe the iterated substitution subst xn vn (... (subst x₁ v₁ (subst f v₀ t₁)) ...), we introduce the operation substn xs vs t, which substitutes the variables xs with the values vs inside the t. It is defined recursively, by iterating calls to the function subst for substituting the variables one by one.

This substitution operation is well-behaved only if the list xs and the list vs have the same lengths. It is also needed for reasoning about the evaluation rule to guarantee that the list of variables xs contains variables that are distinct from each others and distinct from f, and to guarantee that the list xs is not empty. To formally capture all these invariants, we introduce the predicate var_fixs f xs n, where n denotes the number of arguments the function is being applied to. Typically, n is equal to the length of the list of arguments vs.

The evaluation of a recursive function v₀ defined as val_fixs f xs t₁ on a list of arguments vs triggers the evaluation of the term substn xs vs (subst f v₀ t₁), same as substn (f::xs) (v₀::vs) t₁. The evaluation rule is stated as follows, using the predicate var_fixs to enforce the appropriate invariants on the variable names.

The corresponding reasoning rule admits a somewhat similar statement.

The statement of the above lemma applies only to terms that are of the form trm_apps (trm_val v₀) (trms_vals vs). Yet, in practice, goals are generally of the form trm_apps (trm_val v₀) ((trm_val v₁):: .. :: (trm_val vn)::nil). The two forms are convertible. Yet, in most cases, Coq is not able to synthesize the list vs during the unification process. Fortunately, it is possible to reformulate the lemma using an auxiliary conversion function named trms_to_vals, whose evaluation by Coq's unification process is able to synthesize the list vs. The operation trms_to_vals ts, if all the terms in ts are of the form trm_val vi, returns a list of values vs such that ts is equal to trms_vals vs. Otherwise, the operation returns None. The definition and specification of the operation trms_to_vals are as follows.

The specification of the function trms_to_vals asserts that if trms_to_vals ts produces some list of values vs, then ts is equal to trms_vals vs.

Here is a demo showing how trms_to_vals computes in practice.