Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2022-11-23T12:36:12Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/854Add order operations for locations in HeapLang.2022-11-23T12:36:12ZArthur Azevedo de AmorimAdd order operations for locations in HeapLang.As noted in #487, it does not make sense to prevent comparing two locations for their relative order. This MR extends HeapLang to allow that.
One thing that is not clear to me is how we should express the comparison. Right now, the impl...As noted in #487, it does not make sense to prevent comparing two locations for their relative order. This MR extends HeapLang to allow that.
One thing that is not clear to me is how we should express the comparison. Right now, the implementation calls `loc_car` to extract the underlying integer. This is a bit ugly, but I don't know if it would make sense to add another order predicate just for locations.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/825Allow controlling stuckness at the language level2022-11-23T09:28:23ZMichael SammlerAllow controlling stuckness at the language levelCurrently, the safety result of Iris is that each expression is either a value or can reduce. However, there are cases where one wants to have expressions that are not values but also cannot reduce (e.g. when modelling untrusted code tha...Currently, the safety result of Iris is that each expression is either a value or can reduce. However, there are cases where one wants to have expressions that are not values but also cannot reduce (e.g. when modelling untrusted code that is allowed to get stuck or for modeling "no behavior"). Currently, Iris provides the `MaybeStuck` WP which does not require proving safety. However, using `MaybeStuck` is very coarse grained: If any part of the program uses the `MaybeStuck` WP, one looses the safety guarantees for the whole program as composing a `MaybeStuck` WP with a `NotStuck` WP results in a `MaybeStuck` WP.
This MR extends the language interface with a `stuck_allowed e σ` predicate (name open for debate) that specifies expressions that are not required to be reducible. One can obtain the `NotStuck` WP by defining `stuck_allowed e σ` as `False` and the `MaybeStuck` WP by defining `stuck_allowed e σ` as `True`.
Open questions:
- [ ] Naming
- [ ] What are the right set of axioms?
- [ ] Discussing TODOs in the code
- [ ] Should the `MaybeStuck` be removed in this MR or in a follow up MR?
- [ ] The `MaybeStuck` WP allows having both `MaybeStuck` and `NotStuck` WP for the same language while the solution in this MR fixes the notion of stuckness of a language. Is this a problem?
- [ ] Should we add a `Abort` NB expression to HeapLang to replace the [diverge](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/lib/diverge.v) library?https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/791make Prop-level BI connectives notation for bi_emp_valid (rather than bi_enta...2022-12-05T18:49:52ZRalf Jungjung@mpi-sws.orgmake Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)This implements a proposal we discussed at the workshop: make the BI connectives we have in stdpp_scope (i.e., on `Prop` level) be notation for `bi_emp_valid` rather than `bi_entails`. This has the advantage that we never implicitly have...This implements a proposal we discussed at the workshop: make the BI connectives we have in stdpp_scope (i.e., on `Prop` level) be notation for `bi_emp_valid` rather than `bi_entails`. This has the advantage that we never implicitly have a `bi_entails` somewhere in the middle of a formula. The exact location of `bi_entails` is relevant when using `rewrite` (and @gmalecha's automation); not being able to see where the turnstile is is quite confusing in those contexts.
The most painful part of this is big_op because we cannot use the proofmode there yet. The lemmas in HeapLang's proofmode.v are also outside the proofmode and I am not quite sure why. Some base_logic/lib files have some lemmas proved outside the proofmode but I don't think there is a good reason for that -- they just happen to match some of the `own` lemmas exactly, so this was a bit shorter.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/778Attempt at avoiding `unfold` to unfold primitive projections.2022-05-18T17:46:18ZRobbert KrebbersAttempt at avoiding `unfold` to unfold primitive projections.This MR is a potential solution for https://github.com/coq/coq/issues/5698
We currently declare primitive projections, e.g., those of the BI class, as `simpl never`. Our `unseal` tactics unfold these using `unfold primproj; simpl` which...This MR is a potential solution for https://github.com/coq/coq/issues/5698
We currently declare primitive projections, e.g., those of the BI class, as `simpl never`. Our `unseal` tactics unfold these using `unfold primproj; simpl` which used to work prior to Coq 5698, but relied on unexpected behavior of `simpl`.
Looking at the discussion in Coq 5698, it seems the Coq developers are working on bigger changes to primitive projections and it will be hard to support unfolding `simpl never` primitive projections in a backwards compatible way. This MR therefore gets rid of using `unfold`, but states explicit unfolding lemmas and rewrites using those.
TODO:
- [x] Adapt siProp
- [ ] Adapt monPred
- [x] Figure out if there's a good way to make sure that users don't accidentally use these lemmas, and preferably don't find them using `Search`.