Verif_triangA client of the stack functions

Here are some functions (in stack.c) that are clients of the stack ADT. First, push the numbers 1,2,...,n onto a stack, then pop the numbers off the stack and add them up. This computes the nth triangular number, 1+2+...+n = n(n+1)/2.

void push_increasing (struct stack *st, int n) {
  int i;
  i=0;
  while (i<n) {
     i++;
     push(st,i);
  }
}

int pop_and_add (struct stack *st, int n) {
  int i=0;
  int t, s=0;
  while (i<n) {
    t=pop(st);
    s += t;
    i++;
  }
  return s;
}

int main (void) {
  struct stack *st;
  int i,t,s;
  st = newstack();
  push_increasing(st, 10);
  s = pop_and_add(st, 10);
  return s;
}

Let's verify this program!

Proofs with integers

The natural numbers have arithmetic axioms that are not very nice. For example, you might expect that a-b+b=a, but that's not true:

This just shows that if the negative numbers did not exist, it would be necessary to construct them! In reasoning about programs, as in many other kinds of mathematics, we should use the integers. In Coq the type is called Z.

The Z type does have an inductive definition . . .

but we generally prefer to reason abstractly about Z, using the lemmas in the Coq library (that the Coq developers proved from the inductive definition). The induction principle on Z, that's automatically derived from this Inductive definition, is not the one we usually want to use! Let's consider a recursive function on Z, the function that turns 5 into the list 5::4::3::2::1::nil. In the natural numbers, that's easy to define:

But in the integers Z, we cannot simply pattern-match on successor ...

... because Z.succ is a function, not a constructor. There are two ways we might define a function to produce a decreasing list of Z. First, we might use Z.of_nat and Z.to_nat:

This will work, but in doing proofs the frequent conversion between Z and nat will be awkward. If possible, we'd like to stay in the integers as much as possible. So here's another way:

When you define a Function, you must provide a measure, that is, a function from your argument-type (in this case Z) to the natural numbers, and then you must prove that each recursive call within the function body decreases the measure. In this ecase, there's only one recursive call, so there's just one proof obligation: show that if n>0 then Z.to_nat (n-1) < Z.to_nat n.

Exercise: 2 stars, standard (Zinduction)

Coq's standard induction principle for Z is not the one we usually want, so let us define a more natural induction scheme:

A theorem about the nth triangular number

Exercise: 2 stars, standard (add_list_decreasing)

Theorem: the sum of the list (n)::(n-1):: ... :: 2::1 is n*(n+1)/2.

WARNING! When using functions defined by Function, don't unfold them! Temporarily remove the (* comment *) brackets from the next line to see what happens!

Instead of unfolding decreasing we use the equation that Coq automagically defines for the Function. Try the command Search decreasing. to see all the reasoning principles that Coq defined for the new Function. We will use this one:

during the proof of this lemma, you may find the ring_simplify tactic useful. Read about it in the Coq reference manual. Basically, it takes formulas with multiplication and addition, and simplifies them. But you can do this without ring_simplify, using just ordinary rewriting with lemmas about Z.add and Z.mul.

Definitions copied from Verif_stack.v

We repeat here some material from Verif_stack.v. Normally we would break the .c file into separate modules, and do our Verifiable C proofs in separate modules; but for this example we leave out the modules. Just skip down to "End of the material repeated from Verif_stack.v". Specification of linked lists in separation logic

Specification of stack data structure

(End of the material repeated from Verif_stack.v)

Specification of the stack-client functions

Spend a few minutes studying these funspecs, and compare to the implementations in stack.c, until you understand why these might be appropriate specifications.

Putting all the funspecs together

Proofs of the stack-client function-bodies

Exercise: 3 stars, standard (body_push_increasing)

Exercise: 2 stars, standard (add_list_lemmas)

Exercise: 2 stars, standard (add_list_sublist_bounds)

Hint: you don't need induction. Useful lemmas are, sublist_same, sublist_split, add_list_nonneg, add_list_app, Forall_sublist, and use the hint tactic to learn when the list_solve tactic will be useful.

Exercise: 3 stars, standard (add_another)

Suppose we have a list il of integers, il = [5;4;3;2;1], with Znth 0 il = 5, Znth 4 il = 1, and Zlength il = 5, and we want to add them all up, 5+4+3+2+1=15. Suppose we've already added up the first i of them (let i=2 for example), that is, 5+4=9, and we want to add the next one, that is, the ith one. That is, we want to add 9+3. How do we know that won't overflow the range of C-language signed integer arithmetic? The proof goes: Every element of the list is nonnegative; the whole list adds up to a number <= Int.max_signed; and any sublist of an all-nonnegative list adds up to less-or-equal to the total of the whole list.

Next: Int.signed (Int.repr (add_list (sublist 0 i il))) = add_list (sublist 0 i il). To prove that, we'll use Int.signed_repr:

rep_lia is just like lia, but it also knows the numeric values of representation-related constants such as Int.min_signed.

Exercise: 3 stars, standard (body_pop_and_add)

This forward_call couldn't quite figure out the "Frame" for the function call. That is, it couldn't match up stack (sublist i (Zlength il) il) st with
    stack (Znth i il :: sublist (i + 1) (Zlength il) il) st.

You have to help, by doing some rewrites with sublist_split, sublist_len_1 that prove
  sublist i (Zlength il) il = Znth i il :: sublist (i+1) (Zlength il) il.

When you've rewritten the goal into,
   stack (Znth i il :: sublist (i + 1) (Zlength il) il) st
   |-- stack (Znth i il :: sublist (i + 1) (Zlength il) il) st × fold_right_sepcon Frame

then just do cancel.

And now we are ready to go forward through the C statement _s = _s + _t;

oops! we can't go forward through _s = _s + _t; because we forgot to mention temp _s in the loop invariant! Time to start over. By the way, this statement _s = _s + _t is exactly where forward will ask you to prove a subgoal in which you can use lemma add_another.

Into this lemma, paste in the failed proof just above, but adjust the loop invariant: add a LOCAL assertion for _s.

Hint: choose the loop invariant for temp _s ??? in such a way that you can make use of Lemma add_another.

Exercise: 3 stars, standard (body_main)

We assume that triang.c is linked with an implementation of malloc/free. That assumption is expressed by the create_mem_mgr axiom, which we can sep_apply here. On the other hand, if we want a complete verified system including libraries, then instead of importing floyd.library we would actually link with a malloc/free implementation, but that's beyond the scope of this chapter.

You can see that this has produced the SEP conjunct mem_mgr gv, which is useful to satisfy the precondition of newstack, push, pop, etc. Now you can finish this proof.