Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2022-05-24T17:50:09Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/750Flip atomic updates quantifiers compared to atomic triples2022-05-24T17:50:09ZPaolo G. GiarrussoFlip atomic updates quantifiers compared to atomic triplesOriginally suggested by Gregory Malecha (a while ago), and recently discussed with @haidang.
Quantifiers in atomic triples make perfect sense, but AUs and AAUUs are more confusing when used directly: there, `∃` actually means `∀`, and v...Originally suggested by Gregory Malecha (a while ago), and recently discussed with @haidang.
Quantifiers in atomic triples make perfect sense, but AUs and AAUUs are more confusing when used directly: there, `∃` actually means `∀`, and viceversa.
In this proposal, `<<< ∀ x, P x >>> e <<< ∃ y, Q x y, RET f x y >>>` expands to `∀ Φ, AU << ∃ x, P x >> ... << ∀ y, Q x y COMM Φ (f x y) >> -* WP e {{ Φ }}`; then the quantifiers in AUs match the definition and convey the right intuition.
One might fear this is inconsistent. But expanding triples moves quantifiers to the left of a wand, so flipping their polarity follows the tradition from (dependent) currying: `(∀ x, P x -∗ Q) ⊣⊢ ((∃ x, P x) -∗ Q)`.
(Tested locally with dune and Coq 8.13.2).
--------
FWIW, @swasey and @haidang also brought up arguments about caller/callee views, and about the TaDa logic. However, this MR preserves the notation for atomic triples (which agrees with TaDa), and TaDa rules seem to have similar quantifier flipping from a very superficial look (but no, I don't understand everything in flight). Finally, existentials are existentials both at introduction and elimination time; I think the only polarity flip is the one above — atomic triples use AUs in negative position.
![image](/uploads/b3d104c9bd9a53578e80e59ac80e8836/image.png)
![image](/uploads/1331b49cc57a11ffeae355590510b727/image.png)https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/690Add `big_sepM2_union_inv_*`.2021-05-26T13:32:23ZDan FruminAdd `big_sepM2_union_inv_*`.I needed a lemma like this a couple of times.
The proof ends up being quite long.
~~I can also add a symmetric case `big_sepM2_union_inv_r`, but I am not sure if there is a better way of proving it than copy-pasting the proof for the `_...I needed a lemma like this a couple of times.
The proof ends up being quite long.
~~I can also add a symmetric case `big_sepM2_union_inv_r`, but I am not sure if there is a better way of proving it than copy-pasting the proof for the `_l` case.~~https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/684Explicit visibility for Instances2021-05-25T11:32:07ZRalf Jungjung@mpi-sws.orgExplicit visibility for InstancesLike https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/263Like https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/263https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/671Add functional notations for `dist`2021-05-11T20:54:23ZYusuke MatsushitaAdd functional notations for `dist`Add functional notations for `dist` in parallel to `equiv`, namely `(≡{n}≡)`, `(≡{n}@{A}≡)`, `(x ≡{n}≡.)` and `(.≡{n}≡ y)`.Add functional notations for `dist` in parallel to `equiv`, namely `(≡{n}≡)`, `(≡{n}@{A}≡)`, `(x ≡{n}≡.)` and `(.≡{n}≡ y)`.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/656don't tie bi.weakestpre to program_logic.language (full TC approach)2021-06-18T13:30:54ZRalf Jungjung@mpi-sws.orgdon't tie bi.weakestpre to program_logic.language (full TC approach)This is my first attempt to fix #408, by making `expr` and `val` separate typeclass parameters of `Wp`. That fails type-checking in cases where coercions are involved, since TC inference fails before coercions are inserted (so e.g. using...This is my first attempt to fix #408, by making `expr` and `val` separate typeclass parameters of `Wp`. That fails type-checking in cases where coercions are involved, since TC inference fails before coercions are inserted (so e.g. using a `val` as the expression of the `WP` fails). We only rarely rely on this (3 times total in Iris master, and all of them in `tests/`), but it would be a breaking change.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/636register make_laterable as modality2021-06-18T13:50:34ZRalf Jungjung@mpi-sws.orgregister make_laterable as modalityUpamanyu (student at MIT) started looking into `make_laterable`, which made me realize that it might be worth properly registering this as a modality so we can do `iModIntro`. However, it turns out the old definition of `make_laterable` ...Upamanyu (student at MIT) started looking into `make_laterable`, which made me realize that it might be worth properly registering this as a modality so we can do `iModIntro`. However, it turns out the old definition of `make_laterable` is not suited for that: it does not satisfy the lemma
```coq
Lemma make_laterable_intro' Q :
Laterable Q →
Q -∗ make_laterable Q.
```
So, when doing `iModIntro` on a `make_laterable`, we couldn't just keep all `Laterable` things in the context -- we would additionally get an extra `◇` in front of each of them. To fix that I slightly changed the definition of `make_laterable`; most existing laws still hold (or become stronger), with one exception: there's now a `◇` in
```coq
Lemma make_laterable_elim Q :
make_laterable Q -∗ ◇ Q.
```
Still, I think the fact that `make_laterable_intro'` now holds shows that this is the better definition. Logically atomic triples (the only in-tree user of all this) are unaffected by this change, their API surface remains the same.
I also changed `make_laterable_wand` to a less surprising statement:
```coq
Lemma make_laterable_wand Q1 Q2 :
make_laterable (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
```
Sadly, for non-affine BIs, this does not imply the old way of stating that lemma, so that lemma also has to be kept around (under a new name):
```coq
Lemma make_laterable_intuitionistic_wand Q1 Q2 :
□ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
```
So, overall I'd say this MR makes `make_laterable` much more well-behaved and better integrated into the IPM for affine BIs. Figuring out something reasonable for non-affine BIs remains future work.
When there are non-laterable things in the context, `iModIntro` will add a `▷` in front of them to make them laterable. The same approach is now also used by `iAuIntro`, though that requires a hack since we cannot actually use `idModIntro` on `make_laterable` here.
Future plans: https://gitlab.mpi-sws.org/iris/iris/-/issues/424https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/626FromPure instances for big_sepM2021-05-26T09:32:54ZRalf Jungjung@mpi-sws.orgFromPure instances for big_sepMThis is inspired by instances I saw in Perennial.
Probably we could have something similar for `big_sepL` and `Forall`. Any others?This is inspired by instances I saw in Perennial.
Probably we could have something similar for `big_sepL` and `Forall`. Any others?https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/597Add monotone resource algebra2021-05-13T13:39:42ZAmin TimanyAdd monotone resource algebraThis MR adds the monotone resource algebra.This MR adds the monotone resource algebra.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/562add ghost_map library2021-03-06T11:34:41ZRalf Jungjung@mpi-sws.orgadd ghost_map libraryThis adds a logic-level version of `gmap_view`, dubbed `ghost_map` (in parallel to the existing `ghost_var`). The API mirrors that of `gen_heap`. I think this also provides everything Perennial's `auth_map` has, except for operations on ...This adds a logic-level version of `gmap_view`, dubbed `ghost_map` (in parallel to the existing `ghost_var`). The API mirrors that of `gen_heap`. I think this also provides everything Perennial's `auth_map` has, except for operations on "fragment maps" (for which we lack good support in `gmap_view`). Cc @tchajed
This seems like something with many possible uses, so I went for full sealing and also added a notation for the elements: `k ↪[γ]{dq} v`. Obviously, notation and naming are up for bikeshedding. Also for now this library enforces Leibniz equality, but I feel it might be worth supporting `Equiv` (but it would probably help -- for client usability -- to not support arbitrary OFEs).
The notation follows @robbertkrebbers's proposal of using the shortest, "most desirable" notation for the general case of a discardable fraction, and using `k ↪[γ]{#q} v` for `q: frac`. I could also imagine doing this the other way around, i.e., letting `#` indicate `dfrac`. General lemmas should be written for `dfrac` whenever possible, but clients that actually split this fraction will likely work with `1/2` and `1/4` and would have to add a `#` everywhere currently.
Fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/358https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/550Use original pattern in iDestruct error messages2020-11-11T16:55:43ZTej Chajedtchajed@mit.eduUse original pattern in iDestruct error messagesI also took the liberty of giving a specific error to `iDestruct "H" as "[H1 H2 H3]"`, because that was the actual mistake I made (I wrote `iDestruct "H" as "[$H1 H2]"` because I keep wanting to name the thing I'm framing, but of course ...I also took the liberty of giving a specific error to `iDestruct "H" as "[H1 H2 H3]"`, because that was the actual mistake I made (I wrote `iDestruct "H" as "[$H1 H2]"` because I keep wanting to name the thing I'm framing, but of course that doesn't really make sense).https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/527better support for view shift with mismatching masks2021-04-29T09:34:51ZRalf Jungjung@mpi-sws.orgbetter support for view shift with mismatching masksThis adds better support for using view shifts when the mask does not match the goal. Fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/31.
Usually the easiest way to handle such a situation is to use `fupd_intro_mask'`, but that is h...This adds better support for using view shifts when the mask does not match the goal. Fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/31.
Usually the easiest way to handle such a situation is to use `fupd_intro_mask'`, but that is hard to discover and also hard to use without repeating the masks. So with this MR, the goal is to replace that lemma by something better. There are actually two ways the lemma gets used:
* It is used to `iMod` a view shift whose first mask does not match the first mask of the goal. For this I added a new low-priority `ElimModal` instance. It is a somewhat odd instance because the assertion that "comes out" of it is `((|={E1',E1}=> emp) ∗ P)` where `P` is the conclusion of the eliminated view shift, but this still seems way more convenient and easier to discover than having to `iApply` a lemma.
* The lemma is also used to `iModIntro` when the view shift is still mask-changing. I found no good way to do anything automatic here though, so I just made a lemma that is easier to use for this purpose, `fupd_intro_mask_adjust`. (A better name might be `fupd_intro_mask` but that name is already used.)
This is *not* the most general way to handle mask mismatches, in particular for the `iMod` part. `fupd_mask_frame` encodes the most general way. But that requires reasoning about "interesting" (in)equalities of masks, some of which even have to exploit that mask membership is decidable. The only user of `fupd_mask_frame` that I know of is `fupd_mask_frame_acc`, an even more complicated lemma for handling mask mismatches, which in turn is used for `atomic_acc_mask`, which is a cute fact about atomic accessors that I am happy to know is true but which is never actually used. No Iris reverse dependency that we track on CI uses `fupd_mask_frame` or `fupd_mask_frame_acc`, but `fupd_intro_mask'` has quite a few users. So given that it seems fine for me that `iMod` would do something less general that is good enough for basically everything we saw so far.
@robbertkrebbers @tchajed what do you think?https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/514multi-package repositories2020-11-11T15:27:37ZRalf Jungjung@mpi-sws.orgmulti-package repositoriesThis MR realizes multi-package repositories: from the Iris repository, this releases a `coq-iris` package with everything except for HeapLang, and a `coq-iris-heap-lang` package with HeapLang itself. I already landed the required changes...This MR realizes multi-package repositories: from the Iris repository, this releases a `coq-iris` package with everything except for HeapLang, and a `coq-iris-heap-lang` package with HeapLang itself. I already landed the required changes in the rest of the infrastructure (CI scripts and automatic opam publishing), this is the Iris part. This is just an example, we can of course change what we separate how -- but it seemed like the most obvious first split.
For each package, there is a corresponding *Coq project* (`iris` and `iris_heap_lang`) with a separate `_CoqProject.PROJECT` file, which is generated on-demand from the main `_CoqProject` file. This means emacs and coqide treat the entire repository as a single project, and do fine-grained dependency tracking even across packages.
We also need one opam file for each package, `PACKAGE.opam`, which is hooked up to the right `_CoqProject` file via the new `make-package` script. This script does not run any tests (as tests are not associated with packages), so tests will no longer be run on `opam install`.
The files for each project are in `PROJECT/`, which is why this MR renames almost everything. It turns out we can even install HeapLang as a submodule of the Iris package, so the imports are all compatible. (That will probably work less well for splitting out algebra/, bi/, proofmode/; I am not sure if a package can have "multiple roots" and even if it can I am not sure if that is something we want to do).
Coqdoc is generated for the entire repository at once, we'll have to see how well that looks.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/450Improve framing below modalities2020-09-29T16:40:38ZRobbert KrebbersImprove framing below modalitiesThis MR improves framing below modalities:
1. It makes it possible to frame below an `<affine>` modality if the hypothesis that's framed is affine. (Previously, framing below `<affine>` was only possible if the hypothesis that's framed ...This MR improves framing below modalities:
1. It makes it possible to frame below an `<affine>` modality if the hypothesis that's framed is affine. (Previously, framing below `<affine>` was only possible if the hypothesis that's framed resides in the intuitionistic context.)
2. It will "clean up" redundant modalities among the "spine" of the frame.
Feature (2) is achieved by making the classes `MakeAffinely`, `MakeIntuitionistically`, `MakeAbsorbingly`, and `MakePersistently` "smarter". These classes already had ad-hoc "clean up" instances to avoid wrapping the input into a modality if that is not needed. For example, `MakeAffinely` would not wrap input `P` in an `<affine>` modality if `P` is affine, and would not turn input `True` into `<affine> True`, but instead turn `True` into `emp`.
This MR simply adds all combinations of "clean up" instances that I could think of. Namely:
- `MakeAffinely True emp`
- **new** `MakeAffinely (<pers> P) (□ P)`
- **new** `MakeAffinely (<absorb> P1) P2` if `BiPositive PROP` and `MakeAffinely P1 P2`
- `MakeAffinely P P` if `Affine P`
- **generalized** `MakeIntuitionistically P1 P2` if `Persistent P1` and `MakeAffinely P1 P2` (In particular, this instance maps input `<pers> P` to output `□ P`.)
- `MakeAbsorbingly emp True`
- **new** `MakeAbsorbingly (<affine> P1) P2` if `Persistent P1` and `MakeAbsorbingly P1 P2`
- **new** `MakeAbsorbingly P P` if `Absorbing P`
- **new** `MakeAbsorbingly (□ P) (<pers> P)`
- `MakePersistently emp True`
- **new** `MakePersistently P1 P2` if `Persistent P1` and `MakeAbsorbingly P1 P2` (In particular, this instance maps input `□ P` to output `<pers> P`.)
I am not sure how useful this kind of "clean up" is in practice (it is only relevant for non-affine BIs anyway), but at least it now covers all combinations that I can think of instead of just some ad-hoc combinations as was done before. I have included a number of test cases to exercise this "clean up" as part of the `iFrame` tactic.
Moreover, as as a consequence of `MakePersistently` no longer creating redundant modalities, it can now be used to implement an alternative to the adhoc combination of `FromPersistent` and `IntoAbsorbingly` in !216. Concretely, similar to !216, this MR ensures that when using the `[#]` pattern on a premise that is *not* persistent, it will wrap the goal (using `MakePersistently`) into a `<pers>` modality (specialization would fail before). If the premise is already persistent, but not absorbing, it will add an absorbing modality (as was done before).Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/439heap_lang: support deallocation2020-05-25T16:22:31ZRalf Jungjung@mpi-sws.orgheap_lang: support deallocationThis will fix https://gitlab.mpi-sws.org/iris/iris/-/issues/313 when it is ready. But it is still work-in-progress.
I am posting this to get some early feedback. The key issue to solve is remembering which locations were previously al...This will fix https://gitlab.mpi-sws.org/iris/iris/-/issues/313 when it is ready. But it is still work-in-progress.
I am posting this to get some early feedback. The key issue to solve is remembering which locations were previously allocated so that we can ensure they do not get reallocated. This is necessary to keep the `meta` mechanism sound.
The approach I took now is to make the heap be of type `gmap loc (option val)`, and `None` represents "deallocated". I think this is cleaner in terms of language specification than the alternative of tracking a `gset loc` of deallocated locations -- the latter would require an invariant to make sure no location can be both allocated and deallocated. However, a heap of `(option val)` makes `gen_heap` a bit awkward to use. It's not too horrible though, just see for yourself.
@robbertkrebbers what do you think?Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/371Add lemmas about local updates of lists2021-03-17T11:45:16ZDmitry KhalanskiyAdd lemmas about local updates of listsI had to work with lists a lot, so I needed lemmas about their local updates.
`option_local_update'` is part of this MR because I didn't find any other use for it. Maybe its proof can be simplified and inlined, but I couldn't find a way...I had to work with lists a lot, so I needed lemmas about their local updates.
`option_local_update'` is part of this MR because I didn't find any other use for it. Maybe its proof can be simplified and inlined, but I couldn't find a way.
There is a lot in this MR, and I am sure that much of this could be done in a significantly better way, so I didn't yet ensure that the style is satisfactory. I would appreciate it if we could discuss the statements of lemmas and the general approach before I tidy up the final design.Robbert KrebbersRobbert Krebbershttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/294Try getting rid of total Core typeclass2019-12-02T14:23:33ZRalf Jungjung@mpi-sws.orgTry getting rid of total Core typeclassThe only instance of `Core` (other than the default one) is for the STS. That does not seem worth it. But trying to get rid of `Core` leads to all sorts of annoyances in particular around the constructors for (CM)RAs with a unit: I thoug...The only instance of `Core` (other than the default one) is for the STS. That does not seem worth it. But trying to get rid of `Core` leads to all sorts of annoyances in particular around the constructors for (CM)RAs with a unit: I thought we should also change the `(cm)ra_total` constructors to ask for showing `pcore` non-expansive instead of `core` as it seemed more reasonable to ask for a proof of what the user actually wanted. However, that fails miserably; now "by eauto" does not solve these goals any more. Debugging showed that different instances get used for the metric/equiv of `option`, and that's about as far as I got.
@robbertkrebbers I'd appreciate if you can take a look (but this is very non-urgent).Robbert KrebbersRobbert Krebbershttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/216WIP: Make `[#]` produce goal with `<pers>` modality if premise is not persistent2020-05-25T14:15:25ZDan FruminWIP: Make `[#]` produce goal with `<pers>` modality if premise is not persistentThis is my attempt at working towards https://gitlab.mpi-sws.org/iris/iris/issues/186
Currently the `iAssert` has not been fixed yet, but I would like to see if I am at least going in the right direction.
With the modifications you c...This is my attempt at working towards https://gitlab.mpi-sws.org/iris/iris/issues/186
Currently the `iAssert` has not been fixed yet, but I would like to see if I am at least going in the right direction.
With the modifications you can now use `iSpecialize` with on persistent hypothesis to produce a persistent result.
E.g. the following works:
Lemma test_specialize `{BiBUpd PROP} (P Q : PROP) :
□ P -∗ □ (P -∗ Q) -∗ □ Q.
Proof.
iIntros "#HP #H".
iSpecialize ("H" with "[#]").
{ iIntros "!>". iAssumption. }
iAssumption.
Qed.
The following works as well:
Lemma test_specialize_2 `{BiBUpd PROP} (P Q : PROP) :
□ P -∗ □ (□ P -∗ Q) -∗ □ Q.
Proof.
iIntros "#HP #H".
iSpecialize ("H" with "[#]").
{ iIntros "!>". iAssumption. }
iAssumption.
Qed.Robbert KrebbersRobbert Krebbers