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/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/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>