ReLoC issueshttps://gitlab.mpi-sws.org/iris/reloc/-/issues2024-02-16T13:32:18Zhttps://gitlab.mpi-sws.org/iris/reloc/-/issues/11Xchg lemma is Admitted2024-02-16T13:32:18ZIke MulderXchg lemma is AdmittedI was doing `Print Assumptions` and noticed an Admitted in ReLoC [here](https://gitlab.mpi-sws.org/iris/reloc/-/blob/master/theories/logic/rules.v#L197).I was doing `Print Assumptions` and noticed an Admitted in ReLoC [here](https://gitlab.mpi-sws.org/iris/reloc/-/blob/master/theories/logic/rules.v#L197).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/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/7Updating the type system and program context typing2021-01-20T15:43:27ZDan FruminUpdating the type system and program context typing- [x] Typing for unary operators
- [x] Context typing for `CTX_UnOp`
- [x] Context typing for pointer equality. Right now we have program contexts `CTX_BinOpL` and `CTX_BinOpR`; but they are only typed for operands that are integers or B...- [x] Typing for unary operators
- [x] Context typing for `CTX_UnOp`
- [x] Context typing for pointer equality. Right now we have program contexts `CTX_BinOpL` and `CTX_BinOpR`; but they are only typed for operands that are integers or Booleans.
- [ ] Add *value program contexts* similar to how we have value typing for programs.https://gitlab.mpi-sws.org/iris/reloc/-/issues/5`solve_typed` tactic2020-03-06T13:03:12ZDan Frumin`solve_typed` tacticAutomate typing derivations.Automate typing derivations.https://gitlab.mpi-sws.org/iris/reloc/-/issues/4Rules for array allocation.2021-01-20T15:42:57ZDan FruminRules for array allocation.See https://gitlab.mpi-sws.org/iris/iris/blob/31bf88ff46fd89815e49dd22dbc5fea4a77fb62e/theories/heap_lang/lifting.v#L253See https://gitlab.mpi-sws.org/iris/iris/blob/31bf88ff46fd89815e49dd22dbc5fea4a77fb62e/theories/heap_lang/lifting.v#L253Dan FruminDan Fruminhttps://gitlab.mpi-sws.org/iris/reloc/-/issues/3Rules for complex `Resolve` operations.2021-01-20T15:42:39ZDan FruminRules for complex `Resolve` operations.E.g. if you have a prophecy resolution attached to a CAS.
See:
- https://gitlab.mpi-sws.org/iris/iris/merge_requests/244
- https://gitlab.mpi-sws.org/iris/iris/blob/31bf88ff46fd89815e49dd22dbc5fea4a77fb62e/theories/heap_lang/lifting.v#L...E.g. if you have a prophecy resolution attached to a CAS.
See:
- https://gitlab.mpi-sws.org/iris/iris/merge_requests/244
- https://gitlab.mpi-sws.org/iris/iris/blob/31bf88ff46fd89815e49dd22dbc5fea4a77fb62e/theories/heap_lang/lifting.v#L459
(wp_resolve)Dan FruminDan Fruminhttps://gitlab.mpi-sws.org/iris/reloc/-/issues/2Port back the stack with helping example2020-03-06T13:01:45ZDan FruminPort back the stack with helping exampleThe old stack with helping is here: <https://gitlab.mpi-sws.org/dfrumin/logrel-conc/blob/master/theories/examples/stack/helping.v>The old stack with helping is here: <https://gitlab.mpi-sws.org/dfrumin/logrel-conc/blob/master/theories/examples/stack/helping.v>https://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.