case study: Okasaki's persistent queues using the physicist method

I was teaching last week about persistent data structures, which got me thinking about Okasaki's persistent queues.

So here's the code+proof for the structure described in §6.4.2 of the book, the one that uses the so-called "physicist method". It looked easier to implement that the one using the banker method, as here a given version of the queue data structure only features a single thunk.

It was still quite interesting to see how to account for re-entrancy and manage the namespaces/na_own tokens, as we do need to reason about thunks forcing other thunks. In the end, a relatively simple strategy suffices here: associate a given thunk with a namespace indexed by an integer id. Then, this thunk has the permission to force all thunks of ids less than id (and thus is given access to the corresponding na_own tokens). When creating a new thunk that wraps an existing thunk, we simply pick the successor of the id of the wrapped thunk as the id for the new thunk.