Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-04-08T06:14:55Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/451iPoseProof with malformed pm_trm diverges2022-04-08T06:14:55ZWilliam ManskyiPoseProof with malformed pm_trm diverges<!--
When reporting a bug, please always include the version of Iris you are using.
If you are using opam, you can determine your Iris version by running
opam show coq-iris -f version
-->
Some of my Iris students stumbled across th...<!--
When reporting a bug, please always include the version of Iris you are using.
If you are using opam, you can determine your Iris version by running
opam show coq-iris -f version
-->
Some of my Iris students stumbled across this issue: when iPoseProof and derived tactics are given a bad proof mode term, they appear to run forever instead of giving an error. A minimal example:
```
Lemma test Σ (P : iProp Σ) : P -∗ P.
Proof.
iIntros "P".
iPoseProof ("P" "P") as "H". (* diverges *)
```
This is a pretty silly example, but it's easy to stumble into if you forget the `$!` or `with` notation:
```
Lemma test2 Σ (P : expr -> iProp Σ) (x : nat) : (∀ x, P x) -∗ P #x.
Proof.
iIntros "P".
iPoseProof ("P" #x) as "H". (* diverges *)
```
This appears to be the case in versions from 3.4.0 to the current dev version (dev.2022-04-07.0.8fa39f7c).https://gitlab.mpi-sws.org/iris/iris/-/issues/449Add internalised rules for derived resource algebras2022-03-04T00:38:47ZJonas KastbergAdd internalised rules for derived resource algebrasWorking with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of `auth`, which have `auth_both_valid` (in ...Working with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of `auth`, which have `auth_both_valid` (in the model), `auth_both_validN` (in the model, with step-indices), and `auth_both_validI` (in the logic).
Some derived resource algebras are missing their "internalised rules" (those of the logic).
This issue is then to address the lack of these rules.
One example of a resource algebra with missing rules are `mono_list`.
In full, to solve this issue we should:
- Identify all resource algebras with missing internalised rules
- Add the missing rules
- (Settle on a potential pipeline for future algebras to ensure that the rules are included)https://gitlab.mpi-sws.org/iris/iris/-/issues/442Potentially add Frame instances for all our Fractional instances2022-01-17T02:02:14ZRalf Jungjung@mpi-sws.orgPotentially add Frame instances for all our Fractional instancesIn https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739 we have removed the general `frame_fractional` instance and replaced it by connection-specific framing instances such as:
```
Global Instance frame_mapsto p l v q1 q2 RES :
...In https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739 we have removed the general `frame_fractional` instance and replaced it by connection-specific framing instances such as:
```
Global Instance frame_mapsto p l v q1 q2 RES :
FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
```
This is useful since it matches on the head symbol of the framed expression, which is a lot more efficient than `frame_fractional`.
However, we have more `Fractional` instances in the codebase, which for now do not support framing any more:
* `Fractional (λ q, mono_nat_auth_own γ q n)`
* `Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L)`
* `Fractional (λ q, k ↪[γ]{#q} v)` (for `ghost_map`)
* `Fractional (λ q, ghost_map_auth γ q m)`
* `Fractional (λ q, ghost_var γ q a)`
* `Fractional (cinv_own γ)`
If the need comes up, we should add them back. Also, if it was easier to add them (e.g. with some kind of macro), there'd be less hesitation to add these instances everywhere.https://gitlab.mpi-sws.org/iris/iris/-/issues/441Upstream later credits2022-10-14T16:34:37ZRalf Jungjung@mpi-sws.orgUpstream later credits@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I k...@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I keep forgetting what exactly are the `fupd` laws that we would lose by doing this, so maybe we can put that here. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/439Tracking issue for append-only list RA2022-01-21T21:41:49ZRalf 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.
The a...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.
The algebra part of this has been merged; what remains is the base_logic wrapper.
## Open issues
* 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. This is discussed in more generality at https://gitlab.mpi-sws.org/iris/iris/-/issues/412.
* Do a solid review of the API surface.https://gitlab.mpi-sws.org/iris/iris/-/issues/438Use HB.lock(-like) sealing2023-11-10T15:51:29ZRalf Jungjung@mpi-sws.orgUse HB.lock(-like) sealinghierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a dif...hierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a difference in practice.
Quoting from https://github.com/math-comp/hierarchy-builder/wiki/Locking:
```
HB.lock Definition new_concept := 999999.
Lemma test x : new_concept ^ x ^ new_concept = x ^ new_concept ^ new_concept.
Proof.
Time Fail reflexivity. (* takes 0s *)
rewrite new_concept.unlock.
Time Fail reflexivity. (* takes 7s, the original body is restored *)
Abort.
```
This is exactly the kind of locking API I always wanted: just adding a keyword in front of the `Definition`, done. This would make it a no-brainer to seal basically every `iProp` that our reusable libraries export.
TODO:
- Check if this actually works in Iris
- Decide if we want to do this, and how -- are we okay with a dependency on hierarchy-builder?https://gitlab.mpi-sws.org/iris/iris/-/issues/434Diverging `iFrame` with predicate evar2021-10-01T18:46:05ZRalf Jungjung@mpi-sws.orgDiverging `iFrame` with predicate evarThis is a minimized version of a diverging `iFrame` I found in Perennial:
```
Lemma test_iFrame_pred_evar (P Q : PROP) :
P -∗ ∃ (Φ : nat → PROP), ((∃ n, id (Φ n)) ∨ Q).
Proof. iIntros "HP". iExists _. iFrame "HP".
```
The goal at the t...This is a minimized version of a diverging `iFrame` I found in Perennial:
```
Lemma test_iFrame_pred_evar (P Q : PROP) :
P -∗ ∃ (Φ : nat → PROP), ((∃ n, id (Φ n)) ∨ Q).
Proof. iIntros "HP". iExists _. iFrame "HP".
```
The goal at the time of framing is
```
"HP" : P
--------------------------------------∗
(∃ n : nat, id (?Goal n)) ∨ Q
```
All these components seem necessary: when I remove the disjunction, the exisential, or the `id`, the divergence goes away.
In the trace, I can see that it is phantasizing a bigMS into existence, but I do not know why:
```
Debug: 1.1-1.1-1.1-1.1-1.12: simple apply @frame_instances.frame_big_sepMS_disj_union on
(Frame false P (id (?Goal a)) (?Ψ a)), 1 subgoal(s)
Debug:
1.1-1.1-1.1-1.1-1.12-1 : (Frame false P (([∗ mset] y ∈ ?X1, ?Φ y) ∗ ([∗ mset] y ∈ ?X2, ?Φ y)) (?Ψ a))
```
I think one part of the problem is that the extra `id` means that `(id (?Goal a))` does not start with an evar, so the `!` is circumvented.https://gitlab.mpi-sws.org/iris/iris/-/issues/433Tracking issue for HeapLang improvements2021-09-26T00:23:01ZTej Chajedtchajed@gmail.comTracking issue for HeapLang improvementsWe (primarily @robbertkrebbers, @jung, @tchajed, @arthuraa) have a few ideas for improving HeapLang as a language to write programs in. One way to improve HeapLang is by adding libraries, and another way is to add primitives to the langu...We (primarily @robbertkrebbers, @jung, @tchajed, @arthuraa) have a few ideas for improving HeapLang as a language to write programs in. One way to improve HeapLang is by adding libraries, and another way is to add primitives to the language.
Libraries are nice because they don't break backwards compatibility, don't make metatheory harder, and are easy to incrementally develop, test, and improve. There are already libraries floating around, so this effort would be mainly developing good specifications and ergonomics, then distributing the libraries so people can start using them.
# Library support
Some libraries we would like to support include:
- n-ary products and sums, either on the heap or as pure values
- lists and maps, either on the heap or as pure values
Here are a few concrete tasks to get started:
- [ ] Implement pattern matching for products. It would look something like `let: ("a", "b") := "p" in ...` and would bind `"a"` and `"b"` to `Fst "p"` and `Snd "p"`. This is interesting because it's the simplest example we could come up with of a derived construct with binders.
- [ ] Experiment with a nice sum pattern matching library, desugaring to `match:` but with support for a list of variants.
- [ ] Implement a generic list matching library, for list values.
- [ ] Implement a heap linked-list library. Give it a spec in terms of `list val` and then a derived spec that takes `list_rep {A:Type} (l:list A) (Φ: A -> iProp) (v:val)`, relating the list reference `v` to a Gallina list via a representation predicate for each element.
- [ ] Implement a map library along the same lines as the heap linked-list library, using a `gmap val val` and a representation predicate.
# Language improvements
One simplification to the language's representation is to consolidate constructors. The best illustration of this is [simp_lang](https://github.com/tchajed/iris-simp-lang/blob/9ae960be92d23fcf2c96fc8108d3c70c0b790db6/src/lang.v#L75-L77) which already does this; for example, `Fst`, `Snd`, `InjL`, and `InjR` are all consolidated into a single `UnOp op` constructor with a Gallina inductive `op` to identify which operation it is. One resulting simplification is that these all share the same evaluation contexts.
We could have primitive algebraic data types. This has the strong downside of requiring metatheory like logical relations to handle them in some way, whereas right now they only need cases for binary sums and products, with a simple pattern matching construct for sums that takes two lambdas. n-ary pattern matching on sums takes an arbitrary number of lambdas, which is complicated.
Adding a type discriminator would allow a generic, polymorphic equality operator. For metatheory like logical relations, most likely most users would just forbid type discrimination (eg, by not including it in the type system or logical relation), partly because it breaks abstraction.https://gitlab.mpi-sws.org/iris/iris/-/issues/431Add generalized implication lemma for sets, etc.2021-07-29T07:29:12ZSimon Friis VindumAdd generalized implication lemma for sets, etc.!697 adds stronger variants of `big_sepM_impl`. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
```coq
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X...!697 adds stronger variants of `big_sepM_impl`. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
```coq
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X1 X2 :
([∗ set] x ∈ X1, Φ k x) -∗
□ (∀ (x : X),
⌜x ∈ X2⌝ →
((⌜x ∈ X1⌝ ∧ Φ x) ∨ <affinely> ⌜x ¬∈ X1⌝) -∗
Ψ x) -∗
([∗ set] y ∈ X2, Ψ y) ∗
([∗ set] x ∈ X1∖X2, Φ x).
```https://gitlab.mpi-sws.org/iris/iris/-/issues/429Enable the use of the proofmode for proving big-op lemmas2021-07-28T12:28:45ZRalf Jungjung@mpi-sws.orgEnable the use of the proofmode for proving big-op lemmasThere are many things that are painful about `bi/big_op.v`, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.
It would be good to find s...There are many things that are painful about `bi/big_op.v`, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.
It would be good to find some way to stratify this, so that only some core set of lemmas needs to be shown without the proofmode, and the rest can use the proofmode.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/428Make `iDestruct` work on `▷ ∃` if goal is except_0/update2021-07-22T13:02:40ZRobbert KrebbersMake `iDestruct` work on `▷ ∃` if goal is except_0/updateBIs have the interesting rule `bi.later_exist_except_0` which allows to commute `▷` and `∃ x : A` even if the domain `A` of the existential is not inhabited:
```coq
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
```
I...BIs have the interesting rule `bi.later_exist_except_0` which allows to commute `▷` and `∃ x : A` even if the domain `A` of the existential is not inhabited:
```coq
bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)
```
Instead, you get an except-0 (`◇`) modality, which can be eliminated if the goal is, for example, an update modality.
This trick is not commonly known, so it would be great if the proof mode's `iDestruct` tactic could use `bi.later_exist_except_0` automatically instead of just failing when the domain `A` is not inhabited.
This is what happens now:
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import updates.
Lemma test `{BiFUpd PROP} {A} (Φ : A → PROP) (Q : PROP) E :
▷ (∃ x, Φ x) ={E}=∗ Q.
Proof.
iIntros "H".
(* Goal:
"H" : ▷ (∃ x : A, Φ x)
--------------------------------------∗
|={E}=> Q *)
(* Tactic failure: iExistDestruct: cannot destruct (▷ (∃ x : A, Φ x))%I. *)
Fail iDestruct "H" as (x) "H".
(* Works *)
iMod (bi.later_exist_except_0 with "H") as (x) "H".
```
I tried to implement what I proposed in this MR some day, but I could not find a satisfactory generalization of the `IntoExist` class. After all, that class then needs to take the goal into account to eliminate the ◇ modality.
An alternative, we could use the `pm_error` infrastructure from #413 (which still needs to be ported to `IntoExists`) to give an error that points the user to `bi.later_exist_except_0` in case the domain `A` is not inhabited.https://gitlab.mpi-sws.org/iris/iris/-/issues/427Upstreaming big_op lemmas2021-07-16T09:37:22ZMichael SammlerUpstreaming big_op lemmasRefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
len...RefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
length l1 = length l2 →
([∗ list] k↦x ∈ l1, Φ k x) -∗
□ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen); destruct l2 => //=; simpl in *.
iDestruct "Hl" as "[Hx1 Hl]". iSplitL "Hx1". by iApply "Himpl".
iApply ("IH" $! (Φ ∘ S) (Ψ ∘ S) l2 _ with "[] Hl").
iIntros "!>" (k y1 y2 ?) "Hl2 /= ?".
by iApply ("Himpl" with "[] [Hl2]").
Unshelve. lia.
Qed.
End sep_list.
Lemma big_sepL2_impl' {A B C D} (Φ : _ → _ → _ → PROP) (Ψ : _ → _ → _ → _) (l1 : list A) (l2 : list B) (l1' : list C) (l2' : list D) `{!BiAffine PROP} :
length l1 = length l1' → length l2 = length l2' →
([∗ list] k↦x;y ∈ l1; l2, Φ k x y) -∗
□ (∀ k x1 x2 y1 y2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ ⌜l1' !! k = Some y1⌝ -∗ ⌜l2' !! k = Some y2⌝ -∗ Φ k x1 x2 -∗ Ψ k y1 y2) -∗
[∗ list] k↦x;y ∈ l1';l2', Ψ k x y.
Proof.
iIntros (Hlen1 Hlen2) "Hl #Himpl".
rewrite !big_sepL2_alt. iDestruct "Hl" as (Hl1) "Hl".
iSplit. { iPureIntro. congruence. }
iApply (big_sepL_impl' with "Hl"). { rewrite !zip_with_length. lia. }
iIntros "!>" (k [x1 x2] [y1 y2]).
rewrite !lookup_zip_with_Some.
iDestruct 1 as %(?&?&?&?).
iDestruct 1 as %(?&?&?&?). simplify_eq. destruct_and!.
by iApply "Himpl".
Qed.
```
How can one prove these lemmas in a way that they can be upstreamed?https://gitlab.mpi-sws.org/iris/iris/-/issues/426Notation `≼@{A}` is missing2021-07-07T11:02:38ZRobbert KrebbersNotation `≼@{A}` is missingWe are probably missing such notations for more relations. It would be good to do a sweep.We are probably missing such notations for more relations. It would be good to do a sweep.https://gitlab.mpi-sws.org/iris/iris/-/issues/425Splitting (some of) the laws for persistence into a separate class.2023-07-25T15:46:59ZDan FruminSplitting (some of) the laws for persistence into a separate class.I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class?
The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persiste...I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class?
The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persistence modality that can be equipped onto an arbitrary BI.
For later, the BI interface includes the operation itself in the signature, and states a bunch of laws that are satisfied by a degenerate instance of the later modality, and the law that is _not_ satisfied by the degenerate version is in a separate class `BiLöb`.
Would something like that be possible for the persistence modality?
For example, the laws `bi_mixin_persistently_absorbing` and `bi_mixin_persistently_and_sep_elim` could be moved into a separate typeclass; then the remaining laws could be satisfied by the identity function.https://gitlab.mpi-sws.org/iris/iris/-/issues/424Laterable cleanup2021-07-15T07:49:33ZRalf Jungjung@mpi-sws.orgLaterable cleanuphttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `late...https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `laterable_alt`).
* [ ] Rename `make_laterable` to follow our modality naming scheme... `laterably`?
* [ ] Resolve TC backtracking issue around `persistent_laterable`
* [ ] `iMod` for `make_laterable` elimination?https://gitlab.mpi-sws.org/iris/iris/-/issues/423⌜...⌝ uses bad scopes2021-06-18T22:07:47ZRalf Jungjung@mpi-sws.org⌜...⌝ uses bad scopes`⌜x = y + z⌝` shows a really strange error: it complains that `y` is expected to have type `Type`.
The reason is [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/c93646f0489b96521e1f58880fa309a7a7a083bb/iris/bi/interface.v#L240):
```
...`⌜x = y + z⌝` shows a really strange error: it complains that `y` is expected to have type `Type`.
The reason is [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/c93646f0489b96521e1f58880fa309a7a7a083bb/iris/bi/interface.v#L240):
```
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
```
This leads to `+` being interpreted as a type.
I think we should remove `%type` here. Not sure about `%stdpp`.https://gitlab.mpi-sws.org/iris/iris/-/issues/422`iApply` does not use `FromAssumption` for goal matching2021-08-05T14:57:38ZRobbert Krebbers`iApply` does not use `FromAssumption` for goal matching```coq
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} ...```coq
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} (P : PROP) (Q : nat → PROP) :
(P -∗ ∀ n, Q n) -∗ Q 10.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
```
When using `iApply` in combination with the `with` clause, it will first `iSpecialize` and then use `iApply`, which in these examples turns to the degenerate case of `iExact`. The `iExact` tactic uses `FromAssumption` to deal with minor mismatches between the hypothesis and the goal. For example, it will eliminate ∀s and modalities (like □).
When using `iApply` without the `with` clause, it will launch a search using `IntoWand` where the goal with unified with the conclusion of the lemma. If there's a mismatch (like the ones above), it will fail.
The problem is the instance:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
Here, `Q` should match exactly. I tried strengtening it to:
```coq
Global Instance into_wand_wand p q P Q P' Q' :
FromAssumption q P P' →
FromAssumption (p && q) Q' Q →
IntoWand p q (P' -∗ Q') P Q.
```
However, that causes other problems: in some cases the above instance will be triggered instead of instances like `into_wand_bupd_args` causing the following to go wrong:
```coq
Lemma fooz `{!BiBUpd PROP} (P Q : PROP) :
(P -∗ Q) -∗ |==> Q.
Proof.
iIntros "H".
iApply "H". (* should be [|==> P], but will be [P] with the new [into_wand_wand] *)
```
This issue came up in practice Simuliris.https://gitlab.mpi-sws.org/iris/iris/-/issues/420Use siProp more in building the uPred (and BI) interfaces2023-03-04T18:40:53ZRalf 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`...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.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/419Iron slowdown investigation2021-06-17T07:20:40ZRalf Jungjung@mpi-sws.orgIron slowdown investigationIron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iri...Iron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iris from `dev.2021-03-06.3.b0708b01` to `dev.2021-06-03.0.2959900d`. I am not sure if we can do anything about that, but it would be good to at least figure out which changes caused the slowdown (though it looks like there at several, so this might be "death by a thousand cuts").https://gitlab.mpi-sws.org/iris/iris/-/issues/418library inG instances should be local2021-06-02T14:46:21ZRalf Jungjung@mpi-sws.orglibrary inG instances should be localCurrently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.Currently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.