Verif_append1List segments

Here is a little C program, append.c

    #include <stddef.h>

    struct list {int head; struct list *tail;};

    struct list *append (struct list *x, struct list *y) {
      struct list *t, *u;
      if (x==NULL)
        return y;
      else {
        t = x;
        u = t->tail;
        while (u!=NULL) {
          t = u;
          u = t->tail;
        }
        t->tail = y;
        return x;
      }
    }

In this chapter, we will learn to verify this in-place linked-list-append operation. That is, two original lists will be destructed and a new list, the concatenation of them, will be constructed in this program. As we did in previous chapters, we import VST and the C program's AST.

Specification of the append function.

Here we just copy what we have defined in Verif_reverse

Then we can easily describe the functionality of this append.

List segments.

When verifying this program, a critical step is to figure out a correct loop invariant. If we try to simulate this program, especially the loop in it, we may want a loop invariant which can be illustrated by the following diagram.

        +---+---+            +---+---+   +---+---+   +---+---+   
  x ==> |   |  ===> ... ===> |   | t ==> | b | u ==> |   |  ===> ... 
        +---+---+            +---+---+   +---+---+   +---+---+

      | <========= s1a =========> |       (b)       | <==== s1c ====> |
      | <============================= s1 ==========================> |


        +---+---+   +---+---+   +---+---+   
  y ==> |   |  ===> |   |   ==> |   |  ===> ... 
        +---+---+   +---+---+   +---+---+

      | <================ s2 =================> |

To describe this loop invariant, we need a separation logic predicate to describe the partial linked list from address x to address t with contents s1a. This must a new predicate different from listrep because listrep describes linked lists ending with NULL which is not the case here. We call this new predicate lseg, pronounced "list-segment".

Now, we can prove some useful properties about lseg.

Exercise: 1 star, standard (singleton_lseg)

It is critical to observe that a partial linked list defined by lseg s x y may have a loop. For example, the following diagram does satisfy lseg [a; b] x y.

        +---+---+   +---+---+   
  x ==> | a | y ==> | b | y ====+ 
        +---+---+   +- -+---+   |
                      ^         |
                      |         |
                      +=========+

We can prove this formally.

Is our definition of lseg wrong? The answer is no because a loopy lseg cannot connect to a nonempty linked list. For instance, we can prove that
  data_at Tsh t_list (a, y) x × data_at Tsh t_list (b, y) y × listrep [c] y

will lead to a contradication. Here, the first two separating conjuncts build a loopy lseg and the third separating conjunct is a nonempty listrep.

Important note! The proof above demonstrates the use of the sep_apply tactic. Step through that part of the proof to see what sep_apply does. Now we can prove the following theorems about partial linked lists and complete linked lists.

Exercise: 1 star, standard (lseg_lseg)

Exercise: 1 star, standard (lseg_list)

Is it possible to define lseg in a different way so that loopy situations can be banned? Yes. We discuss this near the end of the chapter.

Proof of the append function

Before verifying the functional correctness of append, we still need to add lemmas to hint databases for separation logic predicates. Readers may copy proofs from Verif_reverse or just skip down to "End of the material".

(End of the material repeated from Verif_reverse.v) In C programs, we test whether the head pointer of a linked list is null to determine whether that list is empty or not. Thus, from a separating conjunct listrep contents x, it is useful to prove contents = nil (or contents ≠ nil) when knowing that x = nullval (or x ≠ nullval). The following two lemmas state such correlation. They will be used several times in the C function append's correctness proof.

Exercise: 1 star, standard (listrep_null)

Hint: One way to prove P=Q, where P and Q are mpreds, is to apply pred_ext and then prove P|--Q and Q|--P.

Exercise: 1 star, standard (listrep_nonnull)

Again, pred_ext will be useful here.

Now, let's prove this append function correct.

Exercise: 3 stars, standard (body_append)

This if-then branch handles the cases in which x is null. In other words, s₁ should be nil. We can easily derive this by listrep_null. The rest of the proof in this branch is left as an exercise.

This time, we know that x is not null; thus s₁ should be nonempty.

After symbolically executing two assignment commands, we arrive at the while loop. As mentioned above, we can verify it using the following loop invariant.

We know u is not null from the fact that the loop condition is true. Thus we can represent s1c in the form of (c :: s1d).

In the end of the loop body, we need to re-establish the loop invariant. At this point, the memory layout can be illustrated by the following diagram.

                                 new t       new u
                                   |           |
                                   |           |
                 +---+---+   +---+---+   +---+---+   +---+---+   
  x ==> ... ===> |   | t ==> | b | u ==> | c | z ==> |   |  ===> ... 
                 +---+---+   +---+---+   +---+---+   +---+---+

      | <===== s1a =====> |   (b)         (c)      | <==== s1d ====> |
      | <========== new s1a ========> |  (new b)   | <== new s1c ==> |


        +---+---+   +---+---+   +---+---+   
  y ==> |   |  ===> |   |   ==> |   |  ===> ... 
        +---+---+   +---+---+   +---+---+
      | <================ s2 =================> |

Clearly, s1a ++ b :: nil should be the new value of s1a; c should be the new value of b; s1d should be the new value of s1c; u should be the new value of t; and z should be the new value of u. The next command instantiates the existentially quantified variables in our loop invariant accordingly.

As usual, we try entailer! to solve this proof goal. This time, entailer! does not solve it directly. Instead, two simplified proof goals are left. Their proofs are left for the reader, using app_assoc, singleton_lseg and lseg_lseg.

After exiting the loop, the loop condition must be false, i.e. u is the null pointer. Thus s1c = nil and s₁ = s1a ++ [b].

The rest of the proof is standard. Hint, singleton_lseg, lseg_lseg and/or lseg_list may be useful.

Additional exercises: more proofs about list segments

For verifying the C function append, it is enough to have only three separation logic proof rules about lseg: singleton_lseg, lseg_lseg and lseg_list. The following exercises are other important properties of lseg.

Exercise: 1 star, standard: (lseg2listrep)

Exercise: 1 star, standard: (listrep2lseg)

Exercise: 2 stars, standard: (lseg_lseg_inv)

Exercise: 2 stars, standard: (loopy_lseg_no_connection)

Additional exercises: loop-free list segments

In the following exercise, try to redo the proof above using a different partial-linked-list predicate. We have mentioned that the lseg predicate allows a loopy structure, which is quite counterintuitive. Here is an alternate definition that prohibits loops:

Here, "nt" means no-touch. The difference between nt_lseg and lseg is the extra proposition x ≠ z in the nonempty situation. This extra clause in nt_lseg prevents loop structures. The proof theories of nt_lseg and lseg are a bit different as well. The following diagram shows that the counterpart of lseg_lseg is not valid!

        +---+---+   +---+---+   +---+---+   +---+---+   
  x ==> | a | u ==> | b | y ==> | c | v ==> | d | u ===+
        +---+---+   +- -+---+   +---+---+   +---+---+  |
                      ^                                |
                      |                                |
                      +================================+

In this example, both [a; b] and [c; d] are stored in loop-free partial linked lists but it is not true for their concatenation. In general, if (nt_lseg s₁ x y) and (nt_lseg s₂ y z) describe two loop-free partial linked lists, the assertion
    (nt_lseg s₁ x y × nt_lseg s₂ y z)

cannot ensure that the structure is loop free. Specifically, the address z may be used in (nt_lseg s₁ x y). In other words,
   nt_lseg s₁ x y × nt_lseg s₂ y z ⊢/- nt_lseg (s₁ ++ s₂) x z

For nt_lseg, the following proof rules are useful.

Exercise: 2 stars, standard, optional (nt_lseg)

Exercise: 2 stars, standard, optional (singleton_nt_lseg')

Exercise: 2 stars, standard, optional (nt_lseg_nt_lseg)

Hint: This lemma illustrates the most classic case where aggressive cancel can turn a provable goal into an unprovable goal. For that reason, you may need to use entailer rather than entailer! at one point.

Exercise: 2 stars, standard, optional (nt_lseg_list)

Now, we will use nt_lseg instead of lseg in the loop invariant to prove body_append.

Exercise: 3 stars, standard, optional (body_append_alter1)

Now use forward_while to verify this while loop. Remember, forward_while will generate four proof goals: current precondition implies loop invariant; loop test is safe to execute; loop body preserves invariant; and the correctness of after-loop commands.