upstream things
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 iris#429) -
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 iris!725 (merged) -
the things at the top of https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/simulation/slsls.v @robbertkrebbers -
curry/uncurry -
NonExpansive3/NonExpansive4
-
-
https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/simulation/relations.v @jung -
IntoIH
instance @robbertkrebbers iris#430 (closed) -
theories/stacked_borrows/logical_state.v
:lookup_difference_is_Some
,lookup_union_is_Some
,lookup_union_Some_l'
might be worth upstreaming (stdpp!315 (merged)) -
https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/adequacy.v#L9 @jung stdpp!318 (merged) -
https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/helpers.v#L151 -
https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/steps_opt.v#L1138 @jung stdpp!319 (merged) -
https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/wf.v#L6 @jung -
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)