Add Double Ended Queue example to tutorial #67
Conversation
Sorry! This reverts commit 2d93a9b.
|
|
||
| === Double Ended Queues | ||
|
|
||
| We have already seen an implementation of a single ended and a doubly linked list in CN. Now we can combine those ideas into a double ended queue. This is a list that allows for O(1) operations for adding or removing elements from either end of the list. Here is the C type definition: |
There was a problem hiding this comment.
I think all queues (including the earlier one) are double ended so this sentence will need some adjustment.
| /* A version of doubly linked lists that is essentially from Reynold's | ||
| original separation logic paper (https://www.cs.cmu.edu/~jcr/seplogic.pdf). | ||
| Page 10 has his definition of doubly-linked lists (dlist). | ||
|
|
||
| They're slightly different from ours in that they're "open": | ||
| there's no special treatment of null for the front of the list. | ||
|
|
||
| Technical note for the future: We could eliminate the hacky | ||
| assert_not_equal reasoning if we added this lemma: | ||
|
|
||
| lemma assert_not_equal (p, prev, cur, f, b) | ||
| requires Own_Fwd(prev, cur, f, b); | ||
| Owned<struct node>(p); | ||
| ensures Own_Fwd(prev, cur, f, b); | ||
| Owned<struct node>(p); | ||
| !ptr_eq(p,b); | ||
|
|
||
| This more specific lemma is something we could actually | ||
| (eventually) prove in Rocq, as an inductive fact derived from the | ||
| resource predicate definition. */ |
There was a problem hiding this comment.
We could also eliminate the lemma if the ownership of Back was taken eagerly, as in the queue example. One would simply need to pass the Back node struct value down into the predicate so that it can be appropriately constrained in the base case.
There was a problem hiding this comment.
This file is not mentioned in the tutorial. And the files that are mentioned don't have the assert_not_equal lemmas in them. Can you please explain?
There was a problem hiding this comment.
This is all still WIP...
There was a problem hiding this comment.
There's a bunch of writing / polishing / adding stuff still to do.
This example combines ideas from the imperative queue and doubly linked list for an even more complicated structure. Verifying this data structure includes proving equivalence of different predicates (i.e. if I "own" the queue in the forwards direction, then I "own" it in the backwards direction). As far as I know, this is the only example of proving predicates equivalent. It also shows a great example of proof by induction about ownership done entirely in CN itself.
This definitely needs a read through before it is merged. It is a convoluted example, so I'm sure I didn't explain it entirely well on the first try.