[CN] Export to Iris for resourceful lemmas

[septract]

Just to note: we had some discussion on a call whether this is actually necessary. The alternative would be to extend CN just enough to support lifting everything to pure functional datastructures, and then reason in vanilla Coq.

The downside of doing this is that whoever uses the Coq integration for CN will also need to use Iris. And we would need to pick an Iris theory to target, ideally one which doesn't require the user to understand the fancy higher order reasoning features.

Probably we should find some compelling examples where this is necessary before actually doing it.

[cp526]

Making CN do the lifting into pure functional code in principle is an interesting direction. It's not clear to me whether this would work well for the kind of low-level systems code we're looking at, where proving memory safety isn't always easily separated from the functional verification

[elaustell]

Adding on to this discussion... I'm currently working on a doubly-ended queue example here. The basic idea is that it is a doubly linked list with O(1) push and pop functions to both the head and the tail. I have two different predicates for owning a dbl queue structure: one of which steps through the list forward, claiming ownership of each node and following the next pointers, the other of which steps through the list backwards, claiming ownership of each node and following the prev pointers. This makes it very easy to write specs that push and pop to the head or tail.

Currently, if one has the resource Dbl_Queue_Forwards, they cannot call a function that requires the resource Dbl_Queue_Backwards. In order to tell CN that these are the same resource, I would like to write a lemma that says that these two resources are equivalent. This is proving difficult to prove in CN itself. My attempts can be found at the bottom of the file I linked above.