Iris merge requestshttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests2022-08-24T14:48:57Zhttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/847Add comments to explain the modified structure of the adequacy proof2022-08-24T14:48:57ZSimon SpiesAdd comments to explain the modified structure of the adequacy proofThis MR adds comments to Iris's adequacy proof to explain why we "run adequacy" twice.This MR adds comments to Iris's adequacy proof to explain why we "run adequacy" twice.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/843Draft: move bi_persistently_emp out of BI interface, and get a basic proof mo...2022-08-16T01:42:08ZRalf Jungjung@mpi-sws.orgDraft: move bi_persistently_emp out of BI interface, and get a basic proof mode working againThis does not fully build yet, but `make tests/heapprop_nopers.vo` works -- so it is good enough for some early feedback from @robbertkrebbers to ensure that I am generally on the right track here. :)This does not fully build yet, but `make tests/heapprop_nopers.vo` works -- so it is good enough for some early feedback from @robbertkrebbers to ensure that I am generally on the right track here. :)Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/842Make* class tweaks2022-08-16T13:17:33ZRalf Jungjung@mpi-sws.orgMake* class tweaksRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/825Allow controlling stuckness at the language level2022-08-12T14:55:56ZMichael 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.mpi-sws.org/iris/iris/-/merge_requests/820Dune build files2022-08-24T04:49:17ZPaolo G. GiarrussoDune build filesRequires https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/387.Requires https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/387.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/791make Prop-level BI connectives notation for bi_emp_valid (rather than bi_enta...2022-05-08T11:48:20ZRalf 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.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`.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/771Draft: Add simplification machinery for ✓ and ≼.2022-05-06T15:22:26ZIke MulderDraft: Add simplification machinery for ✓ and ≼.This merge request partially addresses issue #251 .
Concretely, this merge request adds an `iCombineOwn` tactic. In the following environment:
```
"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet E2)
```
executing `iCombineOwn "Hγ1 ...This merge request partially addresses issue #251 .
Concretely, this merge request adds an `iCombineOwn` tactic. In the following environment:
```
"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet E2)
```
executing `iCombineOwn "Hγ1 Hγ2" as "Hγ" gives %[Hq HE]` should replace "Hγ1" and "Hγ2" with a new hypothesis `"Hγ" : own γ (q1 + q2, GSet (E1 ∪ E2))` and two pure hypotheses: `Hq : q1 + q2 ≤ 1` and `HE : E1 ## E2`.
The "as" clause is optional. This is especially useful when you want to combine validity information for a ● and a ◯. In the following environment:
```
"Hγ1" : own γ (◯ (Some (q1, GSet E1)))
"Hγ2" : own γ (● (Some (q2, GSet E2)))
```
executing `iCombineOwn "Hγ1 Hγ2" gives %H` should give you a new pure hypotheses `H : q1 ≤ q2 ∧ E1 ⊆ E2 ∧ ((q1 < q2) ∨ (q1 ≡ q2 ∧ E1 ≡ E2))`.
It works by adding three typeclasses, `IsValidOp`, `IsValidGives` and `IsIncluded`, which try to determine an iProp that simplifies ✓ or ≼. Since we are looking for an iProp, not a pure proposition, this approach also works for higher-order ghost state.
Some current issues:
- Does not simplify equivalences. If directly using rewrites in introduction patterns, may cause slowdowns. Currently an explicit `%leibniz_equiv` on the equality is needed for faster rewrites.
- Some lemmas I used on validity and equivalence of views are still lying around in an awkward place.
- Documentation is missing
- Does not yet have instances for all CMRA building blocks provided in `iris/algebra`, but at least supports the ones used inside the iris repository, and some others I have used in the past.
Feedback is most welcome! I wasn't really sure where to place some of this stuff, so it currently resides in `iris/base_logic/`.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/764Add ∗-∗ as notation in stdpp_scope similar to -∗.2022-05-08T08:53:30ZRobbert KrebbersAdd ∗-∗ as notation in stdpp_scope similar to -∗.As the title says.As the title says.