Working with External Lemmas

List reverse

The specification of list reversal in CN relies on the familiar recursive list reverse function, with a recursive helper.

exercises/list/snoc.h

/*@
function [rec] (datatype List) Snoc(datatype List Xs, i32 Y) {
  match Xs {
    Nil {} => {
      Cons {Head: Y, Tail: Nil{}}
    }
    Cons {Head: X, Tail: Zs}  => {
      Cons{Head: X, Tail: Snoc (Zs, Y)}
    }
  }
}
@*/

exercises/list/rev.h

#include "./snoc.h"

/*@
function [rec] (datatype List) RevList(datatype List L) {
  match L {
    Nil {} => {
      Nil {}
    }
    Cons {Head : H, Tail : T}  => {
      Snoc (RevList(T), H)
    }
  }
}
@*/

To reason about the C implementation of list reverse, we need to help the SMT solver by enriching its knowledge base with a couple of facts about lists. The proofs of these facts require induction, so in CN we simply state them as lemmas and defer the proofs to Coq.

exercises/list/rev_lemmas.h

/*@
lemma Append_Nil_RList (datatype List L1)
  requires true;
  ensures Append(L1, Nil{}) == L1;

lemma Append_Cons_RList (datatype List L1, i32 X, datatype List L2)
  requires true;
  ensures Append(L1, Cons {Head: X, Tail: L2})
          == Append(Snoc(L1, X), L2);
@*/

Having stated these lemmas, we can now complete the specification and proof of IntList_rev. Note the two places where apply is used to tell the SMT solver where to pay attention to the lemmas.

exercises/list/rev.c

#include "./headers.h"
#include "./append.h"
#include "./rev.h"
#include "./rev_lemmas.h"

struct sllist* rev_aux(struct sllist* l1, struct sllist* l2)
/*@ requires take L1 = SLList_At(l1); @*/
/*@ requires take L2 = SLList_At(l2); @*/
/*@ ensures take R = SLList_At(return); @*/
/*@ ensures R == Append(RevList(L2), L1); @*/
{
  if (l2 == 0) {
    /*@ unfold RevList(L2); @*/
    /*@ unfold Append(Nil{}, L1); @*/
    return l1;
  } else {
    /*@ unfold RevList(L2); @*/
    /*@ apply Append_Cons_RList(RevList(Tl(L2)), Hd(L2), L1); @*/
    struct sllist *tmp = l2->tail;
    l2->tail = l1;
    return rev_aux(l2, tmp);
  }
}

struct sllist* rev(struct sllist* l1)
/*@ requires take L1 = SLList_At(l1); @*/
/*@ ensures take L1_Rev = SLList_At(return); @*/
/*@ ensures L1_Rev == RevList(L1); @*/
{
  /*@ apply Append_Nil_RList(RevList(L1)); @*/
  return rev_aux (0, l1);
}

For comparison, here is another way to write the program, using a while loop instead of recursion, with its specification and proof.

exercises/list/rev_alt.c

#include "./headers.h"
#include "./append.h"
#include "./rev.h"
#include "./rev_lemmas.h"

struct sllist* rev_loop(struct sllist *l)
/*@ requires take L = SLList_At(l);
    ensures  take L_post = SLList_At(return);
             L_post == RevList(L);
@*/
{
  struct sllist *last = 0;
  struct sllist *cur = l;
  /*@ apply Append_Nil_RList(RevList(L)); @*/
  while(1)
  /*@ inv take Last = SLList_At(last);
          take Cur = SLList_At(cur);
          Append(RevList(Cur), Last) == RevList(L);
  @*/
  {
    if (cur == 0) {
      /*@ unfold RevList(Nil{}); @*/
      /*@ unfold Append(Nil{}, Last); @*/
      return last;
    }
    struct sllist *tmp = cur->tail;
    cur->tail = last;
    last = cur;
    cur = tmp;
    /*@ unfold RevList(Cur); @*/
    /*@ apply Append_Cons_RList(RevList(Tl(Cur)), Hd(Cur), Last); @*/
  }
}

Exercises

Sized stacks: Fill in annotations where requested:

exercises/slf_sized_stack.c

#include "list/headers.h"
#include "list/length.c"

struct sized_stack
{
  unsigned int size;
  struct sllist *data;
};

/*@
type_synonym SizedStack = {u32 Size, datatype List Data}

predicate (SizedStack) SizedStack_At (pointer p) {
    take P = Owned<struct sized_stack>(p);
    take D = SLList_At(P.data);
    assert(P.size == Length(D));
    return { Size: P.size, Data: D };
}
@*/

extern struct sized_stack *malloc__sized_stack();
/*@
spec malloc__sized_stack();
     requires true;
     ensures take R = Block<struct sized_stack>(return);
@*/

extern void *free__sized_stack(struct sized_stack *s);
/*@
spec free__sized_stack(pointer s);
     requires take R = Block<struct sized_stack>(s);
     ensures true;
@*/

struct sized_stack *create()
/*@ ensures take R = SizedStack_At(return);
            R.Size == 0u32;
@*/
{
  struct sized_stack *s = malloc__sized_stack();
  s->size = 0;
  s->data = 0;
  /*@ unfold Length(Nil {}); @*/
  return s;
}

unsigned int sizeOf(struct sized_stack *s)
/* FILL IN HERE */
{
  return s->size;
}

void push(struct sized_stack *s, int x)
/* FILL IN HERE */
{
  struct sllist *data = slcons(x, s->data);
  s->size++;
  s->data = data;
}

int pop(struct sized_stack *s)
/* FILL IN HERE */
{
  struct sllist *data = s->data;
  if (data != 0)
  {
    int head = data->head;
    struct sllist *tail = data->tail;
    free__sllist(data);
    s->data = tail;
    s->size--;
    return head;
  }
  return 42;
}

int top(struct sized_stack *s)
/*@ requires take S = SizedStack_At(s);
             S.Size > 0u32;
    ensures  take S_post = SizedStack_At(s);
             S_post == S;
             return == Hd(S.Data);
@*/
{
  /*@ unfold Length(S.Data); @*/
  // from S.Size > 0u32 it follows that the 'else' branch is impossible
  if (s->data != 0)
  {
    return (s->data)->head;
  }
  else
  {
    // provably dead code
    return 42;
  }
}