iris-time-proofs merge requestshttps://gitlab.inria.fr/cambium/iris-time-proofs/-/merge_requests2020-03-15T00:32:15+01:00https://gitlab.inria.fr/cambium/iris-time-proofs/-/merge_requests/1sync heap_lang LICENSE file2020-03-15T00:32:15+01:00Ralf Jungsync heap_lang LICENSE fileWe fixed our LICENSE file in https://gitlab.mpi-sws.org/iris/iris/merge_requests/387, this syncs the fix into this repo.
Cc @gmevel @jhjourdanWe fixed our LICENSE file in https://gitlab.mpi-sws.org/iris/iris/merge_requests/387, this syncs the fix into this repo.
Cc @gmevel @jhjourdanhttps://gitlab.inria.fr/cambium/iris-time-proofs/-/merge_requests/2case study: Okasaki's persistent queues using the physicist method2023-01-03T15:29:52+01:00Armaël Guéneaucase study: Okasaki's persistent queues using the physicist methodI 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 ...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.https://gitlab.inria.fr/cambium/iris-time-proofs/-/merge_requests/3Banker's Queue, verified2023-01-27T15:46:28+01:00Armaël GuéneauBanker's Queue, verifiedRemaining cleanup TODOs:
- in Streams.v, some lemmas about the previous definition of subdebits are commented out. They should be either deleted or revived (but they were not used in any case)
- some tactic helpers are duplicated between...Remaining cleanup TODOs:
- in Streams.v, some lemmas about the previous definition of subdebits are commented out. They should be either deleted or revived (but they were not used in any case)
- some tactic helpers are duplicated between Streams.v and bqueue/Proof.v, they need to be factored out in some way or another.