ReLoC issueshttps://gitlab.mpi-sws.org/iris/reloc/-/issues2022-08-29T09:56:03Zhttps://gitlab.mpi-sws.org/iris/reloc/-/issues/8Rules for deallocation2022-08-29T09:56:03ZDan FruminRules for deallocationInitial fix by robbert: https://gitlab.mpi-sws.org/iris/reloc/-/commit/44ca81fded28e7844fca7da4fa86fd6cafe247f8Initial fix by robbert: https://gitlab.mpi-sws.org/iris/reloc/-/commit/44ca81fded28e7844fca7da4fa86fd6cafe247f8https://gitlab.mpi-sws.org/iris/reloc/-/issues/1Logically atomic rules for the Treiber stack2022-08-24T13:27:34ZDan FruminLogically atomic rules for the Treiber stackIt would be nice if the stack refinement could be proven with logically atomic rules for the Treiber stack.It would be nice if the stack refinement could be proven with logically atomic rules for the Treiber stack.https://gitlab.mpi-sws.org/iris/reloc/-/issues/10Hiding `spec_ctx`.2021-01-20T15:46:00ZDan FruminHiding `spec_ctx`.In order to make the lower-level "interface" of ReLoC more clear, it could be worth hiding the `spec_ctx` predicate;
we can just define new `\mapstoS` and `\Mapsto` as a conjunction of `spec_ctx` and the old `mapstoS/Mapsto`.
It might b...In order to make the lower-level "interface" of ReLoC more clear, it could be worth hiding the `spec_ctx` predicate;
we can just define new `\mapstoS` and `\Mapsto` as a conjunction of `spec_ctx` and the old `mapstoS/Mapsto`.
It might be worth incorporating this into the `ext_lp` branch, depending on whether we do something similar there.https://gitlab.mpi-sws.org/iris/reloc/-/issues/9Use Iris' library for partial bijections2021-01-11T15:55:58ZDan FruminUse Iris' library for partial bijectionsSee https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/543See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/543https://gitlab.mpi-sws.org/iris/reloc/-/issues/5`solve_typed` tactic2020-03-06T13:03:12ZDan Frumin`solve_typed` tacticAutomate typing derivations.Automate typing derivations.