simuliris issueshttps://gitlab.rts.mpi-sws.org/iris/simuliris/-/issues2022-03-02T06:34:48Zhttps://gitlab.rts.mpi-sws.org/iris/simuliris/-/issues/12upstream things2022-03-02T06:34:48ZRalf Jungjung@mpi-sws.orgupstream thingsWe have a bunch of things that should be upstreamed. @simonspies @msammler @lgaeher if you remember anything else you proved here that should be in Iris/std++, please add that to the list. :)
- [ ] all/most things in https://gitlab.mpi-...We have a bunch of things that should be upstreamed. @simonspies @msammler @lgaeher if you remember anything else you proved here that should be in Iris/std++, please add that to the list. :)
- [ ] all/most things in https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/simulang/base.v @jung (remainder blocked on https://gitlab.mpi-sws.org/iris/iris/-/issues/429)
- [x] some tweak to the fixpoint construction in https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/logic/fixpoints.v (recursive calls are non-expansive; stronger coinduction principle) @lgaeher https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/725
- [x] the things at the top of https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/simulation/slsls.v @robbertkrebbers
- [x] curry/uncurry
- [x] NonExpansive3/NonExpansive4
- [x] https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/simulation/relations.v @jung
- [x] [`IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L17) @robbertkrebbers https://gitlab.mpi-sws.org/iris/iris/-/issues/430
- [x] [`theories/stacked_borrows/logical_state.v`](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/logical_state.v): `lookup_difference_is_Some`, `lookup_union_is_Some`, `lookup_union_Some_l'` might be worth upstreaming (https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/315)
- [x] https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/adequacy.v#L9 @jung https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/318
- [ ] https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/helpers.v#L151
- [x] https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/steps_opt.v#L1138 @jung https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/319
- [x] https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/wf.v#L6 @jung
- [x] https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/parallel_subst.v#L187 (should probably become something general for `foldl` over associative/commutative [is one of them enough?] operations)