Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-06-07T09:42:21Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/420Use siProp more in building the uPred (and BI) interfaces2021-06-07T09:42:21ZRalf Jungjung@mpi-sws.orgUse siProp more in building the uPred (and BI) interfacesuPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.uPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/415Tracking issue for append-only list RA2021-06-17T18:41:07ZRalf Jungjung@mpi-sws.orgTracking issue for append-only list RAThis is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Do we really want notation for the mono_list algebra elements? The main "pro" reasin here is that `dfrac` otherwise becomes somewhat painful. OTOH, mono_nat and gset_bij algebras do not have notation either. It'd be safe to start without notation
and add them on-demand.
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use.
* Do a solid review of the API surface.This is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Do we really want notation for the mono_list algebra elements? The main "pro" reasin here is that `dfrac` otherwise becomes somewhat painful. OTOH, mono_nat and gset_bij algebras do not have notation either. It'd be safe to start without notation
and add them on-demand.
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use.
* Do a solid review of the API surface.https://gitlab.mpi-sws.org/iris/iris/-/issues/414Tracking issue for monotone RA2021-05-07T08:49:48ZRalf Jungjung@mpi-sws.orgTracking issue for monotone RAThis is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* How should the RA be called? `monotone` is a very general term, it would be good to find something more specific. Currently it is called `mra` which is short but cryptic. `principal` should then likely become `mra_principal` and all lemmas be prefixed with `mra` as well.
* Do a solid review of the API surface.
Cc @amintimany @robbertkrebbersThis is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* How should the RA be called? `monotone` is a very general term, it would be good to find something more specific. Currently it is called `mra` which is short but cryptic. `principal` should then likely become `mra_principal` and all lemmas be prefixed with `mra` as well.
* Do a solid review of the API surface.
Cc @amintimany @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/412Use dfrac everywhere2021-04-23T12:47:13ZRalf Jungjung@mpi-sws.orgUse dfrac everywhere`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [ ] `algebra.lib.gmap_view`
* [ ] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more `auth`-based abstractions in `algebra.lib` but those do not expose *any* fraction on their authoritative part yet.
Some more are not actually built on top of `view`, but these are or could be exposing fractions that it might be useful to turn into `dfrac`:
* [ ] `base_logic.lib.ghost_var`
* [ ] Cancelable invariants
* [ ] Saved propositions (could be made essentially "`ghost_var` with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs *harder* to use for the common case of only needing fraction `1`. For `gset_bij`, we are already in the situation that users need to write `DfracOwn 1` a lot; I wouldn't want the same to happen e.g. for `ghost_map`.`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [ ] `algebra.lib.gmap_view`
* [ ] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more `auth`-based abstractions in `algebra.lib` but those do not expose *any* fraction on their authoritative part yet.
Some more are not actually built on top of `view`, but these are or could be exposing fractions that it might be useful to turn into `dfrac`:
* [ ] `base_logic.lib.ghost_var`
* [ ] Cancelable invariants
* [ ] Saved propositions (could be made essentially "`ghost_var` with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs *harder* to use for the common case of only needing fraction `1`. For `gset_bij`, we are already in the situation that users need to write `DfracOwn 1` a lot; I wouldn't want the same to happen e.g. for `ghost_map`.https://gitlab.mpi-sws.org/iris/iris/-/issues/407Tracking issue for list RA2021-03-17T11:50:01ZRalf Jungjung@mpi-sws.orgTracking issue for list RAThis is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.This is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.https://gitlab.mpi-sws.org/iris/iris/-/issues/406Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs2021-03-18T08:26:06ZArmaël GuéneauSlow typechecking / nonterminating Qed when using auxiliary definitions in RAs```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Definition memspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition regspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition memreg_specUR := prodUR regspecUR memspecUR.
Definition exprUR : cmraT := (exclR (leibnizO nat)).
Definition cfgUR : ucmraT := prodUR (optionUR exprUR) memreg_specUR.
Class cfgSG Σ := CFGSG {
cfg_invG :> inG Σ (authR cfgUR);
cfg_name : gname }.
Section S.
Context `{cfgSG Σ}.
Lemma spec_heap_valid (e:option (excl (leibnizO nat))) a q w
(rm: gmapUR nat (prodR fracR (agreeR (leibnizO nat))))
(mm: gmapUR nat (prodR fracR (agreeR (leibnizO nat)))) :
False →
own cfg_name (● (e,(rm,mm))) ∗
own cfg_name (◯ (ε, (∅,{[ a := (q, to_agree w) ]})))
-∗ False.
Proof. intro.
iIntros "(Hown & Ha)".
iDestruct (own_valid_2 with "Hown Ha") as "HH". exfalso. assumption.
Qed.
End S.
```
The snippet above:
- works fine with Iris 3.3
- takes a very long time at Qed with Iris 3.4 (modulo replacing `cmraT` with `cmra` in the script)
The issue seems to be with the use of auxiliary definitions to define the resource algebra `cfgUR`. Manually inlining `cfgUR` and the other auxiliary definitions in the definition of `cfgSG` makes it work again with Iris 3.4.
Since the fix is relatively simple, this issue doesn't seem to be too big of a deal, but I thought that I'd report it just in case.
Coq version used: 8.12.1 in both cases.```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Definition memspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition regspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition memreg_specUR := prodUR regspecUR memspecUR.
Definition exprUR : cmraT := (exclR (leibnizO nat)).
Definition cfgUR : ucmraT := prodUR (optionUR exprUR) memreg_specUR.
Class cfgSG Σ := CFGSG {
cfg_invG :> inG Σ (authR cfgUR);
cfg_name : gname }.
Section S.
Context `{cfgSG Σ}.
Lemma spec_heap_valid (e:option (excl (leibnizO nat))) a q w
(rm: gmapUR nat (prodR fracR (agreeR (leibnizO nat))))
(mm: gmapUR nat (prodR fracR (agreeR (leibnizO nat)))) :
False →
own cfg_name (● (e,(rm,mm))) ∗
own cfg_name (◯ (ε, (∅,{[ a := (q, to_agree w) ]})))
-∗ False.
Proof. intro.
iIntros "(Hown & Ha)".
iDestruct (own_valid_2 with "Hown Ha") as "HH". exfalso. assumption.
Qed.
End S.
```
The snippet above:
- works fine with Iris 3.3
- takes a very long time at Qed with Iris 3.4 (modulo replacing `cmraT` with `cmra` in the script)
The issue seems to be with the use of auxiliary definitions to define the resource algebra `cfgUR`. Manually inlining `cfgUR` and the other auxiliary definitions in the definition of `cfgSG` makes it work again with Iris 3.4.
Since the fix is relatively simple, this issue doesn't seem to be too big of a deal, but I thought that I'd report it just in case.
Coq version used: 8.12.1 in both cases.https://gitlab.mpi-sws.org/iris/iris/-/issues/398Use `dom` instead of `∀ k, is_Some (.. !! k) ...`2021-02-17T08:48:46ZRobbert KrebbersUse `dom` instead of `∀ k, is_Some (.. !! k) ...`See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas for `dom`. However, the fact that the set (here `gset`) has to specified explicitly might be annoying.
Note that if we perform this change, there are also some lemmas in std++ that need to be changed.See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas for `dom`. However, the fact that the set (here `gset`) has to specified explicitly might be annoying.
Note that if we perform this change, there are also some lemmas in std++ that need to be changed.https://gitlab.mpi-sws.org/iris/iris/-/issues/394Document relation between Discrete and Timeless (in appendix?)2021-01-06T13:08:34ZPaolo G. GiarrussoDocument relation between Discrete and Timeless (in appendix?)See discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/607#note_61127 by @robbertkrebbers:
> I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not so useful; Timeless P → Discrete P does not hold; discrete propositions are unlikely to exist.
> It might be worth documenting this somewhere, but I don't know what's the best place. Maybe the appendix?See discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/607#note_61127 by @robbertkrebbers:
> I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not so useful; Timeless P → Discrete P does not hold; discrete propositions are unlikely to exist.
> It might be worth documenting this somewhere, but I don't know what's the best place. Maybe the appendix?https://gitlab.mpi-sws.org/iris/iris/-/issues/391Add append-only list RA to Iris2021-05-17T16:32:27ZRalf Jungjung@mpi-sws.orgAdd append-only list RA to IrisAppend-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote [a version of this](https://gitlab.mpi-sws.org/iris/gpfsl/-/blob/graphs/theories/examples/list_cmra.v), which was forked at some point by @jtassaro [for Perennial](https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v) while also adding a logic-level wrapper for `auth (mlist T)` with the following three core assertions:
* authoritative ownership of the full trace
* persistent ownership that some list is a prefix of the trace
* persistent ownership that index i in the trace has some particular value
Perennial also has [another version of this](https://github.com/mit-pdos/perennial/blob/master/src/algebra/append_list.v) by @tchajed that is based on (the Perennial version of) `gmap_view`. And finally, @msammler has [his own implementation](https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18) that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.Append-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote [a version of this](https://gitlab.mpi-sws.org/iris/gpfsl/-/blob/graphs/theories/examples/list_cmra.v), which was forked at some point by @jtassaro [for Perennial](https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v) while also adding a logic-level wrapper for `auth (mlist T)` with the following three core assertions:
* authoritative ownership of the full trace
* persistent ownership that some list is a prefix of the trace
* persistent ownership that index i in the trace has some particular value
Perennial also has [another version of this](https://github.com/mit-pdos/perennial/blob/master/src/algebra/append_list.v) by @tchajed that is based on (the Perennial version of) `gmap_view`. And finally, @msammler has [his own implementation](https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18) that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/371Add validI lemmas for discrete RAs2020-11-05T08:41:29ZRalf Jungjung@mpi-sws.orgAdd validI lemmas for discrete RAsOur discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the `Prop`-level lemmas. But e.g. when proving equivalences, it can be useful to have a way to rewrite validity into an equivalent logical statement.
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/558 added the lemma for frac, but other RAs are still missing:
* [ ] `gset_disj`
* [ ] `coPset`, `coPset_disj`
* [ ] `sts`
* [ ] `dfrac`Our discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the `Prop`-level lemmas. But e.g. when proving equivalences, it can be useful to have a way to rewrite validity into an equivalent logical statement.
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/558 added the lemma for frac, but other RAs are still missing:
* [ ] `gset_disj`
* [ ] `coPset`, `coPset_disj`
* [ ] `sts`
* [ ] `dfrac`https://gitlab.mpi-sws.org/iris/iris/-/issues/368Remove `inv` lemmas for agree/auth/view/etc and add `_L` variants to the ↔ lemma2020-11-04T09:54:59ZRobbert KrebbersRemove `inv` lemmas for agree/auth/view/etc and add `_L` variants to the ↔ lemmaSee the discussion here https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/551#note_58488See the discussion here https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/551#note_58488https://gitlab.mpi-sws.org/iris/iris/-/issues/354Discardable camera improvements2020-10-09T13:50:33ZRalf Jungjung@mpi-sws.orgDiscardable camera improvements## Generalization
I think the variant of `dfrac` that I implemented with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531 can be generalized to a "discardable-anything":
```coq
Inductive discardable (A: cmraT) :=
| DOwn : A → dfrac
| DDiscarded : dfrac
| DBoth : A → dfrac.
```
with validity something like
```coq
Instance discardable_valid (A: cmraT) : Valid (discardable A) := λ x,
match x with
| DOwn q => ✓ q
| DDiscarded => True
| DBoth q => exists p, ✓ (q ⋅ p)
end%Qc.
```
I think this should work... what I am not sure about is if this is useful.^^
## old [discarded](https://gitlab.mpi-sws.org/iris/iris/-/issues/354#note_57686) idea: `option Qp`
After https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531, the public interface of `dfrac` can basically be described via a smart constructor that takes `option Qp` -- in fact I am adding such a notation in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486. We can probably rephrase all the existing lemmas in terms of that single constructor, and @robbertkrebbers agrees that that would make a better interface.
Cc @simonfv @tchajed## Generalization
I think the variant of `dfrac` that I implemented with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531 can be generalized to a "discardable-anything":
```coq
Inductive discardable (A: cmraT) :=
| DOwn : A → dfrac
| DDiscarded : dfrac
| DBoth : A → dfrac.
```
with validity something like
```coq
Instance discardable_valid (A: cmraT) : Valid (discardable A) := λ x,
match x with
| DOwn q => ✓ q
| DDiscarded => True
| DBoth q => exists p, ✓ (q ⋅ p)
end%Qc.
```
I think this should work... what I am not sure about is if this is useful.^^
## old [discarded](https://gitlab.mpi-sws.org/iris/iris/-/issues/354#note_57686) idea: `option Qp`
After https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531, the public interface of `dfrac` can basically be described via a smart constructor that takes `option Qp` -- in fact I am adding such a notation in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486. We can probably rephrase all the existing lemmas in terms of that single constructor, and @robbertkrebbers agrees that that would make a better interface.
Cc @simonfv @tchajedhttps://gitlab.mpi-sws.org/iris/iris/-/issues/347"solve_inG" is very slow for larger RA combinators2021-03-03T13:07:08ZRalf Jungjung@mpi-sws.org"solve_inG" is very slow for larger RA combinatorsIn his Iris fork, @jtassaro has a [rather large RA](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/wsat.v#L43) that completely explodes `solve_inG`. Before https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/498, it took around 15s, and then `Qed` took another 15s.
Since !498, they just don't terminate any more. I can make the proof itself go through by adding a `simpl in *` in `solve_inG` (before [this `intros`](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/own.v#L45)), but then `Qed` still takes forever. To make `Qed` work I added some awful hack that seemingly successfully guides Coq towards using the right reduction strategy for `Qed`.
I am not sure what we can do here, besides entirely sealing functors and thus making them non-computational (so we'd have to prove unfolding lemmas about them all, and somehow use them in `solve_inG`).In his Iris fork, @jtassaro has a [rather large RA](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/wsat.v#L43) that completely explodes `solve_inG`. Before https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/498, it took around 15s, and then `Qed` took another 15s.
Since !498, they just don't terminate any more. I can make the proof itself go through by adding a `simpl in *` in `solve_inG` (before [this `intros`](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/own.v#L45)), but then `Qed` still takes forever. To make `Qed` work I added some awful hack that seemingly successfully guides Coq towards using the right reduction strategy for `Qed`.
I am not sure what we can do here, besides entirely sealing functors and thus making them non-computational (so we'd have to prove unfolding lemmas about them all, and somehow use them in `solve_inG`).https://gitlab.mpi-sws.org/iris/iris/-/issues/341Coecisting fractional and persistent read-only ownership2020-08-25T09:34:48ZRalf Jungjung@mpi-sws.orgCoecisting fractional and persistent read-only ownershipAs part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Right now, our encoding through `frac * agree T + agree T` (or equivalently `(frac + ()) * agree T`) requires ownership of the full fraction for that move.
I think such a construction is possible, but it requires https://gitlab.mpi-sws.org/iris/iris/-/issues/257. Then we could relate an authoritative map to a fragment that's more like `option (frac * agree T) * option (agree T)`, and ensure that the second `option` is `None` unless the sum of all fraction fragments is less than 1.As part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Right now, our encoding through `frac * agree T + agree T` (or equivalently `(frac + ()) * agree T`) requires ownership of the full fraction for that move.
I think such a construction is possible, but it requires https://gitlab.mpi-sws.org/iris/iris/-/issues/257. Then we could relate an authoritative map to a fragment that's more like `option (frac * agree T) * option (agree T)`, and ensure that the second `option` is `None` unless the sum of all fraction fragments is less than 1.https://gitlab.mpi-sws.org/iris/iris/-/issues/339Add "reservation map" CMRA2020-09-09T12:29:51ZRalf Jungjung@mpi-sws.orgAdd "reservation map" CMRAFor the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?For the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?https://gitlab.mpi-sws.org/iris/iris/-/issues/321Make `contractive_proper` into a lemma, or control other instances that make ...2020-10-20T09:21:24ZPaolo G. GiarrussoMake `contractive_proper` into a lemma, or control other instances that make it costly.Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?https://gitlab.mpi-sws.org/iris/iris/-/issues/320λne should use %I for body — or add a variant using `%I`.2020-07-14T08:20:05ZPaolo G. Giarrussoλne should use %I for body — or add a variant using `%I`.For unbundled functions, I've used for a while a lambda notation that places the body automatically in `bi_scope`:
```coq
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
```
Similarly, needing both `λne` and `%I` is annoying, what about:
```coq
Notation "'λneI' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t)%I _) ..) _)
(at level 200, x binder, y binder, right associativity).
```
I'd even consider placing that annotation in `λne` itself – `algebra.ofe` could import `bi.notation`; but many non-expansive functions aren't predicates :-).For unbundled functions, I've used for a while a lambda notation that places the body automatically in `bi_scope`:
```coq
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
```
Similarly, needing both `λne` and `%I` is annoying, what about:
```coq
Notation "'λneI' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t)%I _) ..) _)
(at level 200, x binder, y binder, right associativity).
```
I'd even consider placing that annotation in `λne` itself – `algebra.ofe` could import `bi.notation`; but many non-expansive functions aren't predicates :-).Paolo G. GiarrussoPaolo G. Giarrussohttps://gitlab.mpi-sws.org/iris/iris/-/issues/312Fix setoid rewriting for function application in Iris2020-04-22T22:59:30ZPaolo G. GiarrussoFix setoid rewriting for function application in IrisSome of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called [Yannick Zakowski](https://coq.discourse.group/t/confused-with-a-failure-of-a-generalized-rewrite/783?u=blaisorblade) discovered a fix by reading rewrite's error message, and I adapted this to Iris:
```coq
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance equiv_ext_ofe_mor {A B} :
subrelation (≡@{A -n> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
Instance dist_ext_ofe_mor {A B n} :
subrelation (dist n (A := A -n> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
```
I'm going to test this in my project first, to verify the performance implication and robustness, and to find again good testcases, but I thought I'd record this here in an issue.Some of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called [Yannick Zakowski](https://coq.discourse.group/t/confused-with-a-failure-of-a-generalized-rewrite/783?u=blaisorblade) discovered a fix by reading rewrite's error message, and I adapted this to Iris:
```coq
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance equiv_ext_ofe_mor {A B} :
subrelation (≡@{A -n> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
Instance dist_ext_ofe_mor {A B n} :
subrelation (dist n (A := A -n> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
```
I'm going to test this in my project first, to verify the performance implication and robustness, and to find again good testcases, but I thought I'd record this here in an issue.https://gitlab.mpi-sws.org/iris/iris/-/issues/304Direction of _op lemmas is inconsistent with _(p)core, _valid, _included2020-04-06T18:50:12ZRalf Jungjung@mpi-sws.orgDirection of _op lemmas is inconsistent with _(p)core, _valid, _includedSee the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47448: our `_(p)core`, `_valid`, `_included` lemmas generally push the named operation "in", e.g.
```coq
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
```
However, most of our `_op` lemmas push the named operation "out":
```coq
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
```
Moreover, even with one "group" of lemmas, not all are consistent: `singleton_op`, `discrete_fun_singleton_op`, `list_singleton_op` push "in", while `cmra_morphism_(p)core` push "out" (and there might be more).
At the very least, we should make all lemmas within a "group" consistent. So, the minimal fix for this is to swap the 5 lemmas named in the last paragraph. However, we might also want to fix the larger inconsistency that the `_op` lemmas are going the other way, compared to the rest of them. The thing is, we already swapped half of them https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/303, so this starts to look like we are just going back and forth...See the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47448: our `_(p)core`, `_valid`, `_included` lemmas generally push the named operation "in", e.g.
```coq
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
```
However, most of our `_op` lemmas push the named operation "out":
```coq
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
```
Moreover, even with one "group" of lemmas, not all are consistent: `singleton_op`, `discrete_fun_singleton_op`, `list_singleton_op` push "in", while `cmra_morphism_(p)core` push "out" (and there might be more).
At the very least, we should make all lemmas within a "group" consistent. So, the minimal fix for this is to swap the 5 lemmas named in the last paragraph. However, we might also want to fix the larger inconsistency that the `_op` lemmas are going the other way, compared to the rest of them. The thing is, we already swapped half of them https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/303, so this starts to look like we are just going back and forth...https://gitlab.mpi-sws.org/iris/iris/-/issues/286Address the STS encodings lack of usefulness2020-01-30T21:32:04ZJonas KastbergAddress the STS encodings lack of usefulnessThe current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".
Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out.
Going forward we should do either of the following:
- Include a disclaimer discouraging people from using them
- Remove the encoding from the repository
- Update the implementation to be more user-friendly
I suggest doing either of the first two short-term and then possibly look into the third long-term.
It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.The current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".
Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out.
Going forward we should do either of the following:
- Include a disclaimer discouraging people from using them
- Remove the encoding from the repository
- Update the implementation to be more user-friendly
I suggest doing either of the first two short-term and then possibly look into the third long-term.
It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.