Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2016-12-14T13:18:34Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/22Use agree instead of dec_agree2016-12-14T13:18:34ZRalf Jungjung@mpi-sws.orgUse agree instead of dec_agreeThis demonstrates that a list-based agreement could work, and form an OFE. I didn't bother to prove all the functor laws.
Man, this reasoning with about the lists is annoying^^.
What I don't like about this is that un-injection (`a...This demonstrates that a list-based agreement could work, and form an OFE. I didn't bother to prove all the functor laws.
Man, this reasoning with about the lists is annoying^^.
What I don't like about this is that un-injection (`agree_car`) is only non-expansive for valid elements. I want to try using a different equivalence relation, maybe I can find one where this works.
Cc @jjourdan @robbertkrebbersIris 3.0https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/25State invariants in WP and the dead of heap_ctx.2017-01-23T17:32:50ZRobbert KrebbersState invariants in WP and the dead of heap_ctx.This merge request changes the WP construction so that it takes _state interpretation_ as its parameter (part of the `irisG` type class), instead of building in the authoritative ownership of the entire state. When instantiating WP with ...This merge request changes the WP construction so that it takes _state interpretation_ as its parameter (part of the `irisG` type class), instead of building in the authoritative ownership of the entire state. When instantiating WP with a concrete language, one can choose the state interpretation. For example, for `heap_lang` we directly use `auth (gmap loc (frac * dec_agree val))`, and avoid the indirection through an invariant managing ownership of the entire state.
As a result, we no longer have to carry around `heap_ctx`.Iris 3.0Robbert KrebbersRobbert Krebbers