Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2022-08-12T14:48:03Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/441Merge BI and SBI canonical structures2022-08-12T14:48:03ZRobbert KrebbersMerge BI and SBI canonical structuresThis MR flattens the BI hierarchy by merging the `bi` and `sbi` canonical structures. This gives significant performance benefits on developments that nest BI formers (e.g., use `monPred`). For, example it gives a performance gain of 37%...This MR flattens the BI hierarchy by merging the `bi` and `sbi` canonical structures. This gives significant performance benefits on developments that nest BI formers (e.g., use `monPred`). For, example it gives a performance gain of 37% overall on lambdarust-weak, with improvements for individual files up to 72%, see Iris issue #303. The concrete changes are as follows:
+ The `sbi` canonical structure has been removed.
+ The `bi` canonical structure contains the later modality. For non step-indexed BIs the later modality can simply be defined as the identity function, as the `bi` canonical structure does not require the later modality to be contractive, or to satisfy the Löb rule.
+ There is a smart constructor `bi_later_mixin_id` that allows getting the later axioms for "free" if later is defined as the identity function.
+ There is a separate class `BiLöb`, and a "free" instance of that class if the later modality is contractive. A `BiLöb` instance is required for the `iLöb` tactic, and for timeless instances of implication and wand.
+ Since the `sbi` canonical structure has been removed, there is a separate type class `BiInternalEq` for BIs with a notion of internal equality. An instance of this class is needed for the `iRewrite` tactic and the various lemmas about internal equality.
+ The class `SbiEmbed` has been removed and been replaced by classes `BiEmbedLater` and `BiEmbedInternalEq`.
+ The class `BiPlainly` has been generalized to BIs without internal equality. As a consequence, there is a separate class `BiPropExt` for BIs with propositional extensionality (i.e., `■ (P ∗-∗ Q) ⊢ P ≡ Q`).
+ The class `BiEmbedPlainly` is a bi-entailment (i.e., `⎡■ P⎤ ⊣⊢ ■ ⎡P⎤` instead of `■ ⎡P⎤ ⊢ ⎡■ P⎤`) as it has been generalized to BIs without a internal equality. In the past, the left-to-right direction was obtained for "free" using the rules of internal equality.
## Some prior discussion points
- [x] Should we keep the `BiMixin` and `SbiMixin`, or merge them?
**No longer relevant. `SbiMixin` has been renamed into `BiLaterMixin`.**
- [x] Should we keep the files `derived_laws_bi` and `derived_laws_sbi`, or merge them? These files are large, so maybe we should split them in a different way.
**Let's do that in a subsequent clean up MR.**
- [x] Does the class `SbiEmbed` still make sense? I expect that embeddings exist for which we not have `⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤`, but maybe those are somewhat esoteric to justify the existence of this additional type class.
**No longer relevant. This class has been split up into `BiEmbedLater` and `BiEmbedInternalEq`.**
- [x] There are still some sections left that are called `sbi_*`. Should we merge those with other sections?
**Most of them have been removed, some that are left require more invasive changes to files. Let's do this in a separate cleanup MR.**Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/462adjust notation for step-taking updates2020-12-10T13:04:53ZRalf Jungjung@mpi-sws.orgadjust notation for step-taking updatesWhen reading the perennial code (Cc @jtassaro @tchajed) I was thoroughly confused for a bit by the step-taking fancy update notation. It just looks too much like a mask-changing update, without actually being itself mask-changing. So thi...When reading the perennial code (Cc @jtassaro @tchajed) I was thoroughly confused for a bit by the step-taking fancy update notation. It just looks too much like a mask-changing update, without actually being itself mask-changing. So this MR proposes a different notation: `|={E1}[E2]▷=> Q`, where `E1` is the "outer" mask and `E2` is the "inner" mask.Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/289Add heap_lang lib for "invariant locations": locations with a (pure) invarian...2020-08-23T07:51:13ZRalf Jungjung@mpi-sws.orgAdd heap_lang lib for "invariant locations": locations with a (pure) invariant attached to themAn "invariant" location is a location that has some invariant about its
value attached to it, and that can never be deallocated explicitly by the
program. It provides a persistent witness that will always allow reading the
location, ...An "invariant" location is a location that has some invariant about its
value attached to it, and that can never be deallocated explicitly by the
program. It provides a persistent witness that will always allow reading the
location, guaranteeing that the value read will satisfy the invariant.
This is useful for data structures like RDCSS that need to read locations long
after their ownership has been passed back to the client, but do not care *what*
it is that they are reading in that case. In that extreme case, the invariant
may just be `True`.
Since invariant locations cannot be deallocated, they only make sense when
modelling languages with garbage collection. Note that heap_lang does not
actually have explicit dealloaction. However, the proof rules we provide for
heap operations currently are conservative in the sense that they do not expose
this fact. By making "invariant" locations a separate assertion, we can keep
all the other proofs that do not need it conservative.Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/477Remove dec_agree and cofeT and use Coq #[deprecated] attribute for iAlways2020-07-15T12:35:19ZRalf Jungjung@mpi-sws.orgRemove dec_agree and cofeT and use Coq #[deprecated] attribute for iAlwaysFixes https://gitlab.mpi-sws.org/iris/iris/-/issues/296
I also just deleted things that have been in `deprecated.v` for years we cannot use `#[deprecated]` for all of them as old Coq did not support that attribute on `Notation`).Fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/296
I also just deleted things that have been in `deprecated.v` for years we cannot use `#[deprecated]` for all of them as old Coq did not support that attribute on `Notation`).Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/478Iris 3.3 changelog summary2020-07-15T11:14:46ZRalf Jungjung@mpi-sws.orgIris 3.3 changelog summaryThis adds a "summary" that we can put into the Iris 3.3 announcement; we can just link to the website for the full changelog as it is way too long.This adds a "summary" that we can put into the Iris 3.3 announcement; we can just link to the website for the full changelog as it is way too long.Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/470mention that the ASCII syntax exists (but we recommend unicode)2020-07-15T10:27:49ZRalf Jungjung@mpi-sws.orgmention that the ASCII syntax exists (but we recommend unicode)I didn't want to just push saying that "we recommend" something, hence the MR.
@robbertkrebbers @jjourdan what do you think?I didn't want to just push saying that "we recommend" something, hence the MR.
@robbertkrebbers @jjourdan what do you think?Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/476All list "map singleton" lemmas consistently use `singletonM` in their name2020-07-15T09:36:22ZRalf Jungjung@mpi-sws.orgAll list "map singleton" lemmas consistently use `singletonM` in their nameI implemented @robbertkrebbers' proposal for naming.
This is a breaking change; the following sed script helps port things that work with current master:
```
s/\blist_singleton_core\b/list_singletonM_core/g
s/\blist_lookup_singleton(...I implemented @robbertkrebbers' proposal for naming.
This is a breaking change; the following sed script helps port things that work with current master:
```
s/\blist_singleton_core\b/list_singletonM_core/g
s/\blist_lookup_singleton(|_lt|_gt|_ne)\b/list_lookup_singletonM\1/g
s/\blist_singleton_(validN|length)\b/list_singletonM_\1/g
s/\blist_alter_singleton\b/list_alter_singletonM/g
s/\blist_singleton_included\b/list_singletonM_included/g
s/\blist_singleton_updateP\b/list_singletonM_updateP/
s/\blist_singleton_snoc\b/list_singletonM_snoc/
```
Fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/309Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/435Change ascii turnstile2020-05-29T18:10:25ZGregory MalechaChange ascii turnstileThis is on top of !432 , that should be merged first.This is on top of !432 , that should be merged first.Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/432Fix `forall` parsing.2020-05-28T21:54:49ZGregory MalechaFix `forall` parsing.- This fixes a bug in the declaration of the forall notation
which was preventing Coq from recognizing the primitive
Gallina `forall`.
- The solution is to re-introduce the `forall` notation
at type scope. This overrides the primit...- This fixes a bug in the declaration of the forall notation
which was preventing Coq from recognizing the primitive
Gallina `forall`.
- The solution is to re-introduce the `forall` notation
at type scope. This overrides the primitive notation.
New tests at the bottom of the proofmode_ascii file.Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/453Remove `Open Scope Z_scope` in HeapLang2020-05-28T14:56:56ZRobbert KrebbersRemove `Open Scope Z_scope` in HeapLangI think the `Open Scope Z_scope` in `heap_lang.lang` is a mistake. While `Z`s are often useful when working with HeapLang, I don't think HeapLang should enforce that on users. Furthermore, whether one actually gets an opened `Z_scope` or...I think the `Open Scope Z_scope` in `heap_lang.lang` is a mistake. While `Z`s are often useful when working with HeapLang, I don't think HeapLang should enforce that on users. Furthermore, whether one actually gets an opened `Z_scope` or not seems to depend on the import order (see [this discussion on Mattermost](https://mattermost.mpi-sws.org/iris/pl/un4bk3uw4p8wmr437rw7ng45xh)).
In this MR I thus remove `Open Scope Z_scope`. According to grep, after this MR, there are no other scopes that are opened globally (apart from `general_if_scope` in `algebra.base` which is to patch up ssreflect).
As a consequence of this change, some `%Z` had to be inserted, while it also allowed for some `%nat`s to be removed.Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/457Remove redundant `%I` scopes in definitions.2020-05-28T14:47:12ZRobbert KrebbersRemove redundant `%I` scopes in definitions.This is a follow up of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/456#note_51710
Many uses of the `%I` scopes in `iProp` definitions are redundant. This MR removes all those that I could find.This is a follow up of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/456#note_51710
Many uses of the `%I` scopes in `iProp` definitions are redundant. This MR removes all those that I could find.Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/458Fix scopes for `plainly` following !456.2020-05-28T13:32:58ZPaolo G. GiarrussoFix scopes for `plainly` following !456.Iris 3.3https://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/429heap_lang lifting: instantiate inv_heapG and inv_heap_inv2020-05-18T11:50:05ZRalf Jungjung@mpi-sws.orgheap_lang lifting: instantiate inv_heapG and inv_heap_invThis was quite annoying in https://gitlab.mpi-sws.org/iris/examples/-/commit/99f8ad1819f75a774740419e0c9cf883a310561c, to have to explicitly pass `loc val` all the time.
However, this means that `inv_heap` will be exported by default in...This was quite annoying in https://gitlab.mpi-sws.org/iris/examples/-/commit/99f8ad1819f75a774740419e0c9cf883a310561c, to have to explicitly pass `loc val` all the time.
However, this means that `inv_heap` will be exported by default into every heap_lang user. I am a bit worried people might accidentally rely on there being a GC in their model. But maybe that's okay?Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/400Add support for pure names in intro patterns2020-04-17T07:09:15ZTej Chajedtchajed@gmail.comAdd support for pure names in intro patternsNotably this support relies on string to identifier conversion, which
works natively using Ltac2 in Coq 8.11+ and with a plugin
(https://github.com/ppedrot/coq-string-ident) in Coq 8.10. To use it,
you must replace `intro_patterns.str...Notably this support relies on string to identifier conversion, which
works natively using Ltac2 in Coq 8.11+ and with a plugin
(https://github.com/ppedrot/coq-string-ident) in Coq 8.10. To use it,
you must replace `intro_patterns.string_to_ident_binder` with a real
implementation; see string_ident.v for an Ltac2 implementation and
enable_pure_names.v for how to install it.
The syntax is `%H` (within a string intro pattern). This is technically
backwards-incompatible, because this was previously supported and parsed
as `%` and `H` separately. To restore the old behavior, separate with a
space, eg `[% H]`.
Fixes #88Iris 3.3https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/396ASCII notation2020-04-08T15:22:40ZGregory MalechaASCII notation- all ascii notation is marked "only parsing" so this PR shouldn't
change anything for anyone using only unicode notation.
- the algorithm for creating an ascii notation is pretty simple.
- \ast -> * (not for separating conjunctio...- all ascii notation is marked "only parsing" so this PR shouldn't
change anything for anyone using only unicode notation.
- the algorithm for creating an ascii notation is pretty simple.
- \ast -> * (not for separating conjunction)
- \triangleright -> |>
- \vee -> \/
- \wedge -> /\
- \forall -> forall
- \exists -> exists
- separating conjunction -> **
- we're using notation scopes to resolve ambiguities
Closes #270 Iris 3.3