Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-10-27T11:54:07Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/488Move iris.sty towards being a community standard2022-10-27T11:54:07ZJonas KastbergMove iris.sty towards being a community standardMy impression is that there a multiple people who take inspiration from the `iris.sty` file
when writing papers about Iris.
For one, we use (a variant of) it in the Iris Lecture Notes (Soon to be publicly available).
I find that it would...My impression is that there a multiple people who take inspiration from the `iris.sty` file
when writing papers about Iris.
For one, we use (a variant of) it in the Iris Lecture Notes (Soon to be publicly available).
I find that it would be beneficial to have a "community standard" for this collection of macros,
to guarantee that notation is uniform throughout Iris papers (while of course authors should be free to diverge from the standard as need be).
To achieve this the style-file should be kept up to date with changing notation, terminiology, etc.
While good effort has already been put towards this, I find that more improvements could be made,
e.g. by reviewing the current file on terms such as:
- Completeness of the macro set (For one there is currently no `\pointsto`)
- Names of the macros (For one `\always` seem outdated in terms of the current "persistently" terminology)
- Notation of the macros
- Formatting of macros (kerning, squashing, etc.)
The merge request !851 is an attempt at an initial step in this direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/487Adding pointer order comparison to HeapLang2022-10-14T19:33:59ZArthur Azevedo de AmorimAdding pointer order comparison to HeapLangAs the following file shows, HeapLang makes it possible to compare pointers for their relative ordering. Should we extend the primitive comparison operation on HeapLang to work on pointers as well?
[pointer_comparison.v](/uploads/f638e4...As the following file shows, HeapLang makes it possible to compare pointers for their relative ordering. Should we extend the primitive comparison operation on HeapLang to work on pointers as well?
[pointer_comparison.v](/uploads/f638e4e4e81b856b5be629e623fe608f/pointer_comparison.v)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/490Move heaplang.sty towards being a community standard2022-10-14T13:38:49ZJonas KastbergMove heaplang.sty towards being a community standardSimilarly to #488 I believe it is beneficial to more carefully curate the `heaplang.sty` file contained in this repository.
Some immediate considerations that might make sense to review are:
- The notion-style supported by the language ...Similarly to #488 I believe it is beneficial to more carefully curate the `heaplang.sty` file contained in this repository.
Some immediate considerations that might make sense to review are:
- The notion-style supported by the language macros - e.g. parentheses vs spaces for function arguments
- The naming of each macro, to avoid clashes with popular latex packages
- Discuss what similarities we want HeapLang to have with existing languages (formerly ML, but has since moved quite past it)
- Casing of constructs, both in Latex and notation. Currently we have discrepancies such as `ref` and `Alloc` even though they live on the same level. The latex macros are mostly consistent, with some outliers like `\poison` and `\fold` / `\unfold`
The MR's !852 and !853 are some initial steps in this direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/478Adding satisfiable to Iris2022-08-17T05:24:37ZSimon SpiesAdding satisfiable to IrisSeveral Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notio...Several Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notion of `satisfiable` can be added to Iris in a meaningful way and whether it can enable more modular adequacy proofs in the future.https://gitlab.mpi-sws.org/iris/iris/-/issues/476Have `known_make_absorbingly` and `make_absorbingly_default` instances in the...2022-08-15T14:17:18ZRalf Jungjung@mpi-sws.orgHave `known_make_absorbingly` and `make_absorbingly_default` instances in the same fileThe following discussion from !842 should be addressed:
> This makes me think, it's a bit annoying that the default instance and `known_make_absorbingly` are not at the same place. Could we somehow refactor that? Move the default instan...The following discussion from !842 should be addressed:
> This makes me think, it's a bit annoying that the default instance and `known_make_absorbingly` are not at the same place. Could we somehow refactor that? Move the default instances to `classes_make`, or move the other one here?https://gitlab.mpi-sws.org/iris/iris/-/issues/475Provide some way to "seal" a BI2022-08-12T14:53:14ZRalf Jungjung@mpi-sws.orgProvide some way to "seal" a BIOne reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms i...One reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms in general are just bigger.
It might be worth investigating some nice way to seal a BI (but that would probably have to be a macro):
- either lightweight sealing by just making it TC opaque and forwarding all instances
- or a proper seal that makes terms no convertible any more, and a *lot* of forwarding of things
We *do* seal `iProp` pretty heavily (in fact even more proper than the "proper" seal, this is the one place where we use a module type for sealing to be *really sure*), so Iris itself doesn't have this problem.
@robbertkrebbers IIRC you did an experiment along the lines of doing that by hand once? What were the results of that again?https://gitlab.mpi-sws.org/iris/iris/-/issues/303Canonical structures have major performance impact2022-08-12T14:48:02ZRobbert KrebbersCanonical structures have major performance impactAs I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and ...As I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and `bi` canonical structures.
- [37.40% overall on lambdarust-weak](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=masters%2Fweak_mem&var-commit1=bcc7c0be5ba2def0989d727c97d94a8492b9e40b&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi_weak&var-commit2=4ea92744abcd644f385696c398206a20a2cab7cf&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 72.22%.
- [23.28% overall on Iron](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iron&var-branch1=master&var-commit1=4dcc142742d846037be4cd94678ff8759465e6c1&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=37f90dd22db3ca477377d16ae72d761cb617412c&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 38.13%.
- [3.8% overall on Iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=9b2ad256fbf948933cdbf6c313eb244fd2439bf3&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=294ef2ef2df5478db81065f6cd5edc1d831419a1&var-config2=build-coq.8.11.0&var-group=().*&var-metric=instructions), with improvements for individual files up to 13.16%.
- [5.2% overall on lamdarust master](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=fe35f4cd910f3f3235fd3c6b6c46fc142d3ce13f&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=bea9f4a02efe48a38894fe1286add7ab25a2d2de&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 10.18%.
These differences are major, especially for the projects that use BI formers (monPred in lambdarust-weak and fracPred in Iron)! So it looks like there is really something we should investigate.https://gitlab.mpi-sws.org/iris/iris/-/issues/417Revert !118: Use ∃ instead of SIgma for extension axiom2022-08-02T16:52:12ZRobbert KrebbersRevert !118: Use ∃ instead of SIgma for extension axiomI am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet ...I am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet { multiset_car : list A }.
```
And define `dist` and `(≡)` to be modulo permutations. For permutations I use https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.SetoidPermutation.html
Unfortunately, this does not work: the extension axiom of cameras does not seem provable.
```coq
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
```
The problem is that I need to construct `z1` and `z2` as a sigma type, not an ordinary exist. But the type of permutations is a `Prop`, so I cannot do this.
Here's the whole code I have so far:
```coq
From Coq Require Import SetoidPermutation.
From iris.algebra Require Export cmra.
Lemma PermutationA_mono {A} (R1 R2 : relation A) xs1 xs2 :
(∀ x1 x2, R1 x1 x2 → R2 x1 x2) →
PermutationA R1 xs1 xs2 → PermutationA R2 xs1 xs2.
Proof. induction 2; econstructor; by eauto. Qed.
Record multiset A := MultiSet { multiset_car : list A }.
Arguments MultiSet {_} _.
Arguments multiset_car {_} _.
Section multiset.
Context {A : ofe}.
Implicit Types x y : A.
Implicit Types X Y : multiset A.
Local Instance multiset_equiv_instance : Equiv (multiset A) := λ X1 X2,
∀ n, PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_dist_instance : Dist (multiset A) := λ n X1 X2,
PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_valid_instance : Valid (multiset A) := λ _, True.
Local Instance multiset_validN_instance : ValidN (multiset A) := λ _ _, True.
Local Instance multiset_unit_instance : Unit (multiset A) := MultiSet [].
Local Instance multiset_op_instance : Op (multiset A) := λ X1 X2,
MultiSet (multiset_car X1 ++ multiset_car X2).
Local Instance multiset_pcore_instance : PCore (multiset A) := λ X, Some ε.
Global Instance multiset_singleton : Singleton A (multiset A) := λ x,
MultiSet [x].
Lemma multiset_ofe_mixin : OfeMixin (multiset A).
Proof.
split; rewrite /equiv /dist /multiset_equiv_instance /multiset_dist_instance /=.
- done.
- intros n. split.
+ by intros X.
+ intros X1 X2 ?. done.
+ intros X1 X2 X3 ??. by etrans.
- intros n X1 X2. apply PermutationA_mono, dist_S.
Qed.
Canonical Structure multisetO := Ofe (multiset A) multiset_ofe_mixin.
Global Instance multiset_ofe_discrete : OfeDiscrete A → OfeDiscrete multisetO.
Proof.
intros HA [xs1] [xs2] Hxs n. revert Hxs. apply PermutationA_mono.
by intros x1 x2 ->%(discrete _).
Qed.
Lemma multiset_cmra_mixin : CmraMixin (multiset A).
Proof.
apply cmra_total_mixin; try by eauto.
- intros X n Y1 Y2 HY. by apply (PermutationA_app _).
- by intros n X1 X2.
- intros X1 X2 X3. admit. (* boring case *)
- intros X1 X2 n. apply (PermutationA_app_comm _).
- by intros X n.
- intros X1 X2 _. exists ε. by intros n.
- intros n [xs] [ys1] [ys2] _. rewrite /equiv /dist /op
/multiset_equiv_instance /multiset_dist_instance /multiset_op_instance /=.
(* Stuck here. The witness [PermutationA (dist n) xs (ys1 ++ ys2)] basically
says how the elements in [xs] are distributed over [ys1] and [ys2].
Intuitively, it says element 0 of [xs] goes to position [i0] in
[ys1 ++ ys2], element 1 of [xs] goes to position [i1] in ys1 ++ ys2 and so
on. *)
(* I would like to use the lemma [PermutationA_decompose], but that does
not work since it gives an [∃]. *)
(* I tried to prove it by induction on the list instead, but that seems
pointless. At some point I need to invert on the [PermutationA] witness,
which is not possible. *)
induction ys1 as [|y1 ys1 IH]; intros Hxs; simpl in *.
{ by exists (MultiSet []), (MultiSet xs). }
admit.
Admitted.
Canonical Structure multisetR := Cmra (multiset A) multiset_cmra_mixin.
Lemma multiset_ucmra_mixin : UcmraMixin (multiset A).
Proof. split; [done | | done]. by intros X n. Qed.
Canonical Structure multisetUR := Ucmra (multiset A) multiset_ucmra_mixin.
Global Instance multiset_cancelable X : Cancelable X.
Proof. Admitted.
Global Instance multiset_singleton_ne : NonExpansive (singleton (B:=multiset A)).
Proof. intros n x1 x2. by repeat constructor. Qed.
Global Instance multiset_singleton_proper :
Proper ((≡) ==> (≡)) (singleton (B:=multiset A)).
Proof. apply (ne_proper _). Qed.
Global Instance multiset_singleton_dist_inj n :
Inj (dist n) (dist n) (singleton (B:=multiset A)).
Proof. intros x1 x2. Admitted.
Global Instance multiset_singleton_inj :
Inj (≡) (≡) (singleton (B:=multiset A)).
Proof.
intros x1 x2 Hx. apply equiv_dist=> n. apply (inj singleton). by rewrite Hx.
Qed.
End multiset.
Global Arguments multisetO : clear implicits.
Global Arguments multisetR : clear implicits.
Global Arguments multisetUR : clear implicits.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/205Make notation for pure and plainly affine2022-06-12T19:28:08ZRalf Jungjung@mpi-sws.orgMake notation for pure and plainly affineI think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.I think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/463Rename "head step"?2022-06-10T18:13:39ZRalf Jungjung@mpi-sws.orgRename "head step"?At some point there was a discussion on Mattermost about people objecting to the term "head step" that we use in our HeapLang operational semantics. I think there were proposals for others names, but I forgot if there was any consensus.At some point there was a discussion on Mattermost about people objecting to the term "head step" that we use in our HeapLang operational semantics. I think there were proposals for others names, but I forgot if there was any consensus.https://gitlab.mpi-sws.org/iris/iris/-/issues/462iRewrite with a Coq-level equality gives bad error message2022-05-20T17:14:58ZRalf Jungjung@mpi-sws.orgiRewrite with a Coq-level equality gives bad error messageIn a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at le...In a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at least the tactic should tell me what is wrong. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/369Document HeapLang2022-05-18T17:42:51ZRalf Jungjung@mpi-sws.orgDocument HeapLangThe HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently [my thesis](https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf#figure.3.1) and the ["Future is Our...The HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently [my thesis](https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf#figure.3.1) and the ["Future is Ours" paper](https://plv.mpi-sws.org/prophecies/paper.pdf#%5B%7B%22num%22%3A171%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C45.828%2C641.295%2Cnull%5D) describe overlapping but incomparable subsets of the operational semantics, and there are likely bits that are missing from both.https://gitlab.mpi-sws.org/iris/iris/-/issues/402iFrame performance issues2022-05-06T12:56:32ZRalf Jungjung@mpi-sws.orgiFrame performance issuesThere are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into ...There are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into disjunctions at all by default?
- Also, @tchajed noticed that `iFrame` is doing a lot of `AsFractional` everywhere, which might also be a too expensive default -- this is tracked separately in https://gitlab.mpi-sws.org/iris/iris/-/issues/351.
- Cc https://gitlab.mpi-sws.org/iris/iris/-/issues/183 for the general "power vs performance" tradeoff in `iFrame`.
- https://gitlab.mpi-sws.org/iris/iris/-/issues/434 for diverging iFrame because Hint Mode is accidentally being circumvented.https://gitlab.mpi-sws.org/iris/iris/-/issues/458Inconsistency in weakening of modalities in `iApply`2022-05-01T11:54:32ZRobbert KrebbersInconsistency in weakening of modalities in `iApply````coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens...```coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens is that the first (and failing) `iApply` directly attempts to find an `IntoWand` instance to match the conclusion of the wand with the goal. This fails because the only applicable `IntoWand` instance is:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
There is no `FromAssumption` for `Q`, so no weakening of the conclusion is performed.
In the second attempt, `iApply` will first `iSpecialize` with the wand. As such, it tries to find an `IntoWand` instance where the conclusion can be unified with an evar. Then after that, it will use `iAssumption`, which uses `FromAssumption` to weaken the modality.
## Solution
We probably should add `FromAssumption` to instances like `into_wand_wand`. I do not know if this was just an omission, or there's a reason for that. Should try.https://gitlab.mpi-sws.org/iris/iris/-/issues/16Document variable naming conventions2022-04-08T09:49:43ZRalf Jungjung@mpi-sws.orgDocument variable naming conventionsWe should
* [x] Convert naming.txt to markdown
* [ ] document the naming conventions for single-letter variable names
* [ ] maybe make them more consistent between Coq and LaTeX.
* [x] Document postfixes like C, T, R, G
Cc @robbertkreb...We should
* [x] Convert naming.txt to markdown
* [ ] document the naming conventions for single-letter variable names
* [ ] maybe make them more consistent between Coq and LaTeX.
* [x] Document postfixes like C, T, R, G
Cc @robbertkrebbers https://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/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/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.