A little more progress on queue.broken.c

src/examples/queue.broken.c

@@ -20,13 +20,13 @@ struct int_queueCell {
 };
 
 /*@
-predicate (datatype seq) IntQueue(pointer q) {
+predicate (datatype seq) IntQueue (pointer q) {
   take H = Owned<struct int_queue>(q);
   take Q = IntQueue1(q,H);
   return Q;
 }
 
-predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) {
+predicate (datatype seq) IntQueue1 (pointer dummy, struct int_queue H) {
   if (is_null(H.head) || is_null(H.tail)) {
     assert (is_null(H.head) && is_null(H.tail));
     return (Seq_Nil{});
@@ -81,16 +81,6 @@ extern void freeIntQueueCell (struct int_queueCell *p);
 
 // -----------------------------------------------------------------
 
-/*@
-function [rec] (datatype seq) push (datatype seq xs, i32 y) {
-  snoc (xs, y)
-}
-
-function [rec] (i32) pop (datatype seq xs, i32 y) {
-  hd (xs)
-}
-@*/
-
 struct int_queue* IntQueue_empty ()
 /*@ ensures take ret = IntQueue(return);
             ret == Seq_Nil{};
@@ -111,38 +101,40 @@ int IntQueue_pop (struct int_queue *q)
 @*/
 {
   /*@ split_case (*q).head == NULL; @*/
-  int x = q->head->first;
-  if (q->head->next == 0) {
+  /*@ split_case (*q).tail == NULL; @*/
+  // This is needed to unfold IntQueueAux, I guess?
+  /*@ split_case (*q).head == (*q).tail; @*/  // rewrite to h==t!
+  struct int_queueCell* h = q->head;
+  struct int_queueCell* t = q->tail;
+  /*@ split_case (*h).next == NULL; @*/
+  int x = h->first;
+  // This originally tested for h->next == 0, but this didn't seem to fit the structure of
+  // the verification; this way works better, at least for the first branch.  But would
+  // it have been possible to verify it the other way?
+  if (h == t) {
+    // This line was missing originally -- good pedagogy to fix in stages??
+    freeIntQueueCell(h);
     q->head = 0;
     q->tail = 0;
+    return x;
   } else {
-    q->head = q->head->next;
+    struct int_queueCell* n = h->next;
+    // Needs to deallocate here too!
+    q->head = n;
+    freeIntQueueCell(h);
+    return x;
   }
-  return x;
+  // The return was originally here -- make sure to comment on why it got moved!
 }
 
-void IntQueue_push (int x, struct int_queue *q)
-/*@ requires take before = IntQueue(q);
-    ensures take after = IntQueue(q);
-            after == snoc (before, x);
-@*/
-{
-  struct int_queueCell *c = mallocIntQueueCell();
-  c->first = x;
-  c->next = 0;
-  if (q->tail == 0) {
-    /*@ split_case (*q).head == NULL; @*/
-    /*@ apply snoc_nil(x); @*/
-    // And then this??  Trying random stuff...
-    /*@ split_case (*q).tail == NULL; @*/
-    q->head = c;
-    q->tail = c;
-  } else {
-    // This is needed next:
-    /*@ split_case (*q).head == NULL; @*/
-    // And then this??  Again, random stuff
-    /*@ split_case (*q).tail == NULL; @*/
-    q->tail->next = c;
-    q->tail = c;
-  }
-}
+
+// Notes:
+// - When I tried /*@ unfold IntQueueAux (H.head, H.tail, T.first); @*/
+//   I was confused by "the specification function `IntQueueAux' is not declared".
+//   I guess this is, again, the distinction between functions and predicates...?
+// - Seq_Cons is awkward for several reasons:
+//     - long / verbose (nothing to do about that, I guess)
+//     - Seq is capitalized, but it means seq
+//     - most important part is buried in the middle
+//     - What are the established C conventions here??
+// - lastVal can be eliminated, I think

src/examples/temp-queue3.broken.c

@@ -0,0 +1,134 @@
+/* queue.c */
+
+#include "list.h"
+#include "list_snoc_spec.h"
+
+/*@
+lemma snoc_nil (i32 foo)
+  requires true;
+  ensures snoc (Seq_Nil{}, foo) == Seq_Cons {head: foo, tail: Seq_Nil{}};
+@*/
+
+struct int_queue {
+  struct int_queueCell* head;
+  struct int_queueCell* tail;
+};
+
+struct int_queueCell {
+  int first;
+  struct int_queueCell* next;
+};
+
+/*@
+predicate (datatype seq) IntQueue (pointer q) {
+  take H = Owned<struct int_queue>(q);
+  take Q = IntQueue1(q,H);
+  return Q;
+}
+
+predicate (datatype seq) IntQueue1 (pointer dummy, struct int_queue H) {
+  if (is_null(H.head) || is_null(H.tail)) {
+    assert (is_null(H.head) && is_null(H.tail));
+    return (Seq_Nil{});
+  } else {
+    assert (!is_null(H.head) && !is_null(H.tail));
+    take T = Owned<struct int_queueCell>(H.tail);
+    assert (is_null(T.next));
+    take Q = IntQueueAux (H.head, H.tail, T.first);
+    return Q;
+  }
+}
+
+predicate (datatype seq) IntQueueAux (pointer h, pointer t, i32 lastVal) {
+  if (h == t) {
+    return (Seq_Cons{head: lastVal, tail: Seq_Nil{}});
+  } else {
+    take C = Owned<struct int_queueCell>(h);
+    take TL = IntQueueAux(C.next, t, lastVal);
+    return (Seq_Cons { head: C.first, tail: TL });
+  }
+}
+
+@*/
+
+// ---------------------------------------------------------------------
+
+extern struct int_queue *mallocIntQueue();
+/*@ spec mallocIntQueue();
+    requires true;
+    ensures take u = Block<struct int_queue>(return);
+            return != NULL;
+@*/ // 'return != NULL' should not be needed
+
+extern void freeIntQueue (struct int_queue *p);
+/*@ spec freeIntQueue(pointer p);
+    requires take u = Block<struct int_queue>(p);
+    ensures true;
+@*/
+
+extern struct int_queueCell *mallocIntQueueCell();
+/*@ spec mallocIntQueueCell();
+    requires true;
+    ensures take u = Block<struct int_queueCell>(return);
+            return != NULL;
+@*/ // 'return != NULL' should not be needed
+
+extern void freeIntQueueCell (struct int_queueCell *p);
+/*@ spec freeIntQueueCell(pointer p);
+    requires take u = Block<struct int_queueCell>(p);
+    ensures true;
+@*/
+
+// -----------------------------------------------------------------
+
+struct int_queue* IntQueue_empty ()
+/*@ ensures take ret = IntQueue(return);
+            ret == Seq_Nil{};
+@*/
+{
+  struct int_queue *p = mallocIntQueue();
+  p->head = 0;
+  p->tail = 0;
+  return p;
+}
+
+int IntQueue_pop (struct int_queue *q)
+/*@ requires take before = IntQueue(q);
+             before != Seq_Nil{};
+    ensures take after = IntQueue(q);
+            after == tl(before);
+            return == hd(before);
+@*/
+{
+  /*@ split_case (*q).head == NULL; @*/
+  /*@ split_case (*q).tail == NULL; @*/
+  // This is needed to unfold IntQueueAux, I guess?
+  /*@ split_case (*q).head == (*q).tail; @*/
+  struct int_queueCell* h = q->head;
+  /*@ split_case (*h).next == NULL; @*/
+  int x = h->first;
+  if (h->next == 0) {
+    // This line was missing originally -- good pedagogy to fix in stages??
+    freeIntQueueCell(h);
+    q->head = 0;
+    q->tail = 0;
+    return x;
+  } else {
+    // Needs to deallocate here too!
+    q->head = h->next;
+    return x;
+  }
+  // The return was originally here -- make sure to comment on why it got moved!
+}
+
+
+// Notes:
+// - When I tried /*@ unfold IntQueueAux (H.head, H.tail, T.first); @*/
+//   I was confused by "the specification function `IntQueueAux' is not declared".
+//   I guess this is, again, the distinction between functions and predicates...?
+// - Seq_Cons is awkward for several reasons:
+//     - long / verbose (nothing to do about that, I guess)
+//     - Seq is capitalized, but it means seq
+//     - most important part is buried in the middle
+//     - What are the established C conventions here??
+// - lastVal can be eliminated, I think

src/queue-example-notes.md

@@ -1,4 +1,4 @@
-# Notes
+2# Notes
 
 - Bad definition of snoc (same as rev). How to spot? Look at constraint context, specifically snoc(listQ, x) == match listQ {Seq\_Nil {} => {Seq\_Nil {}}Seq\_Cons {head: h, tail: zs} => {snoc(rev(zs), h)}}. Other big clue: applying lemma snoc_nil results in an inconsistent context. This is really nasty because snoc(Seq_Nil{}, x) ends up reducing to itself.