Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-11-10T18:03:57Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/361gen_heap: provide init lemma for non-empty heap that provides the points-to f...2020-11-10T18:03:57ZRalf Jungjung@mpi-sws.orggen_heap: provide init lemma for non-empty heap that provides the points-to factsOur current `gen_heap_init` can be used with a non-empty heap, but then the points-to facts for the initial location are lost. Sometimes however they are needed: both Perennial and time-credits violate the gen_heap abstraction to be able to initialize with a non-empty heap and obtain all the points-to facts.
We should just provide a lemma for this. However, this is blocked on `gmap_view` having such a lemma, which requires having "map fragments" besides the currently available "singleton fragments".Our current `gen_heap_init` can be used with a non-empty heap, but then the points-to facts for the initial location are lost. Sometimes however they are needed: both Perennial and time-credits violate the gen_heap abstraction to be able to initialize with a non-empty heap and obtain all the points-to facts.
We should just provide a lemma for this. However, this is blocked on `gmap_view` having such a lemma, which requires having "map fragments" besides the currently available "singleton fragments".https://gitlab.mpi-sws.org/iris/iris/-/issues/359Use the IPM to prove some example IPM extension theorems2020-10-21T11:00:32ZTej Chajedtchajed@mit.eduUse the IPM to prove some example IPM extension theoremsThe current proofs for some HeapLang tactics use a bunch of separation logic theorems manually, like this proof:
```coq
Lemma tac_wp_free Δ Δ' s E i K l v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
(let Δ'' := envs_delete false i false Δ' in
envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ? Hlk Hfin.
rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
Qed.
```
It would be much nicer to use the proof mode to do these proofs, which is also nicely circular because we're extending the proof mode using the proof mode. For example, the above proof can be written:
```coq
rewrite envs_entails_eq=> ? Hlk Hfin.
rewrite into_laterN_env_sound.
iIntros "HΔ'".
iApply wp_bind.
pose proof (envs_lookup_sound' _ false _ _ _ Hlk) as HΔ'split.
set (Δ'':=envs_delete false i false Δ') in *.
iDestruct (HΔ'split with "HΔ'") as "[Hl HΔ'']".
iApply (wp_free with "Hl").
iNext. iIntros "_".
iApply (Hfin with "HΔ''").
```
This proof isn't shorter but you can figure out how to write such a proof using only the proof mode rather than convoluted uses of theorems like `sep_mono_r` and `wand_intro_r`. This particular case become slightly messier because if you do `iDestruct envs_lookup_sound with "HΔ'"` then the proof mode reduces `envs_delete` and the result is horrendous.
I don't think we need to re-do all of the proofs; I'm thinking having a few such examples would go a long way as examples that demonstrate how to extend the IPM in a nice way. We couldn't port all of the theorems anyway since of course some of these theorems are actually used to implement the IPM.The current proofs for some HeapLang tactics use a bunch of separation logic theorems manually, like this proof:
```coq
Lemma tac_wp_free Δ Δ' s E i K l v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
(let Δ'' := envs_delete false i false Δ' in
envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ? Hlk Hfin.
rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
Qed.
```
It would be much nicer to use the proof mode to do these proofs, which is also nicely circular because we're extending the proof mode using the proof mode. For example, the above proof can be written:
```coq
rewrite envs_entails_eq=> ? Hlk Hfin.
rewrite into_laterN_env_sound.
iIntros "HΔ'".
iApply wp_bind.
pose proof (envs_lookup_sound' _ false _ _ _ Hlk) as HΔ'split.
set (Δ'':=envs_delete false i false Δ') in *.
iDestruct (HΔ'split with "HΔ'") as "[Hl HΔ'']".
iApply (wp_free with "Hl").
iNext. iIntros "_".
iApply (Hfin with "HΔ''").
```
This proof isn't shorter but you can figure out how to write such a proof using only the proof mode rather than convoluted uses of theorems like `sep_mono_r` and `wand_intro_r`. This particular case become slightly messier because if you do `iDestruct envs_lookup_sound with "HΔ'"` then the proof mode reduces `envs_delete` and the result is horrendous.
I don't think we need to re-do all of the proofs; I'm thinking having a few such examples would go a long way as examples that demonstrate how to extend the IPM in a nice way. We couldn't port all of the theorems anyway since of course some of these theorems are actually used to implement the IPM.https://gitlab.mpi-sws.org/iris/iris/-/issues/358Add a logic-level version of gmap_view2021-03-06T11:34:41ZRalf Jungjung@mpi-sws.orgAdd a logic-level version of gmap_viewWe now have `gmap_view` on the RA level, but this library seems useful enough that we want to have a logic-level wrapper as well, with notations for "owning a location in a ghost heap", so to speak. Perennial has `auth_map` (and some predecessors) for this and it is used all over the place.We now have `gmap_view` on the RA level, but this library seems useful enough that we want to have a logic-level wrapper as well, with notations for "owning a location in a ghost heap", so to speak. Perennial has `auth_map` (and some predecessors) for this and it is used all over the place.https://gitlab.mpi-sws.org/iris/iris/-/issues/357Cancelable locks2020-10-21T11:00:44ZRobbert KrebbersCancelable locksIt would be really useful to have a version of cancelable locks, where the `is_lock` predicate is equipped with a fraction. That way, we could have a couple of things:
1. A Hoare triple for the physical free operation `{{ is_lock lk 1 R }} free lk {{ R }}`
2. A rule `is_lock lk 1 R ==∗ ▷ R ∗ (▷ R' ==∗ is_lock lk 1 R')` that allows a "strong update" of the payload of the lock.
Now that we have the discardable fractional permissions, we could use those to get back the ordinary lock-spec by picking the fraction to be `DfracDiscarded`.
To implement this, we probably first want to generalize cancelable invariants, by a.) adding a discardable fraction b.) adding a rule for changing the proposition in case one owns the entire fraction.
Questions:
- For locks, do we want to equip `is_lock` with a fraction, or do we want to add a token `lock_own` (which would be timeless).
- If we equip `is_lock` with a fraction, we won't break backwards compatibility that much. One just needs to add `DfracDiscarded` everywhere. If we have a token for the fraction, backwards compatibility is a bigger issue. We could of course define `is_lock ... := new_is_lock ... ∗ lock_own DfracDiscarded` or something like that.
Any thoughts?It would be really useful to have a version of cancelable locks, where the `is_lock` predicate is equipped with a fraction. That way, we could have a couple of things:
1. A Hoare triple for the physical free operation `{{ is_lock lk 1 R }} free lk {{ R }}`
2. A rule `is_lock lk 1 R ==∗ ▷ R ∗ (▷ R' ==∗ is_lock lk 1 R')` that allows a "strong update" of the payload of the lock.
Now that we have the discardable fractional permissions, we could use those to get back the ordinary lock-spec by picking the fraction to be `DfracDiscarded`.
To implement this, we probably first want to generalize cancelable invariants, by a.) adding a discardable fraction b.) adding a rule for changing the proposition in case one owns the entire fraction.
Questions:
- For locks, do we want to equip `is_lock` with a fraction, or do we want to add a token `lock_own` (which would be timeless).
- If we equip `is_lock` with a fraction, we won't break backwards compatibility that much. One just needs to add `DfracDiscarded` everywhere. If we have a token for the fraction, backwards compatibility is a bigger issue. We could of course define `is_lock ... := new_is_lock ... ∗ lock_own DfracDiscarded` or something like that.
Any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/356gmap_view: add fraction support to gmap_view_auth2020-10-21T10:09:04ZRalf Jungjung@mpi-sws.orggmap_view: add fraction support to gmap_view_authTo fully supplement Perennial's `auth_map`, we need to equip `gmap_view_auth` with support for a fraction. `view` already supports fractions so this should not be too hard.To fully supplement Perennial's `auth_map`, we need to equip `gmap_view_auth` with support for a fraction. `view` already supports fractions so this should not be too hard.https://gitlab.mpi-sws.org/iris/iris/-/issues/355Break dependency of algebra on base_logic2020-10-20T15:11:03ZRalf Jungjung@mpi-sws.orgBreak dependency of algebra on base_logicCurrently, parts of algebra depend on base_logic for the "internalized" equality and validity lemmas. That is rather annoying as it means many things need to be recompiled to work on those parts of algebra. It also prevents us from separating the base_logic and program_logic folders into a separate package, should we ever want to do that.
The plan is to instead add a file like `base_logic/algebra.v` and prove those lemmas there, thus fixing the dependency inversion.Currently, parts of algebra depend on base_logic for the "internalized" equality and validity lemmas. That is rather annoying as it means many things need to be recompiled to work on those parts of algebra. It also prevents us from separating the base_logic and program_logic folders into a separate package, should we ever want to do that.
The plan is to instead add a file like `base_logic/algebra.v` and prove those lemmas there, thus fixing the dependency inversion.https://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/353CHANGELOG should spell out what changed in auth due to views MR better2020-10-03T10:02:54ZTej Chajedtchajed@mit.eduCHANGELOG should spell out what changed in auth due to views MR better!516 makes some changes that aren't obvious. For example, `auth_validI` is gone because it used the projections, should now explicitly use `auth_auth_validI`, `auth_frag_validI`, or `auth_both_validI` as appropriate.!516 makes some changes that aren't obvious. For example, `auth_validI` is gone because it used the projections, should now explicitly use `auth_auth_validI`, `auth_frag_validI`, or `auth_both_validI` as appropriate.https://gitlab.mpi-sws.org/iris/iris/-/issues/352Tracking issue for records2021-03-18T09:21:04ZRalf Jungjung@mpi-sws.orgTracking issue for records@tchajed, @robbertkrebbers and me are discussing ideas for equipping Iris with support for "named records", based on a first implementation of sch a scheme by Tej for Perennial. This is a tracking issue where we track which pieces of work depend on what, and what needs to be done next.
The current status is that some unforeseen issues came up after merging https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/479, but we'd rather not change the naming system until we have a way to reliably control the names used for existentials in a record. Record design itself [is blocked on some fundamental questions](https://gitlab.mpi-sws.org/iris/iris/-/issues/352#note_65075).
* [List of related MRs](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests?scope=all&utf8=%E2%9C%93&state=all&label_name[]=T-records)@tchajed, @robbertkrebbers and me are discussing ideas for equipping Iris with support for "named records", based on a first implementation of sch a scheme by Tej for Perennial. This is a tracking issue where we track which pieces of work depend on what, and what needs to be done next.
The current status is that some unforeseen issues came up after merging https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/479, but we'd rather not change the naming system until we have a way to reliably control the names used for existentials in a record. Record design itself [is blocked on some fundamental questions](https://gitlab.mpi-sws.org/iris/iris/-/issues/352#note_65075).
* [List of related MRs](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests?scope=all&utf8=%E2%9C%93&state=all&label_name[]=T-records)https://gitlab.mpi-sws.org/iris/iris/-/issues/351Decouple framing and IntoSep2021-02-03T16:32:48ZRalf Jungjung@mpi-sws.orgDecouple framing and IntoSepCurrently, `IntoSep` does a few things that can be rather expensive, like `AsFractional` conversion. This is very useful for destruct patterns, but `IntoSep` is also used for framing, and there we want to be cheap. @tchajed already disabled some `IntoSep` instances in Perennial for this reason.
It might make sense to have a separate IntoSep for framing that is more optimized for performance and, for example, does not try to exploit fractional things.
This is somewhat similar to https://gitlab.mpi-sws.org/iris/iris/-/issues/186.
To avoid making a mess, probably we should figure out https://gitlab.mpi-sws.org/iris/iris/-/issues/139 first.Currently, `IntoSep` does a few things that can be rather expensive, like `AsFractional` conversion. This is very useful for destruct patterns, but `IntoSep` is also used for framing, and there we want to be cheap. @tchajed already disabled some `IntoSep` instances in Perennial for this reason.
It might make sense to have a separate IntoSep for framing that is more optimized for performance and, for example, does not try to exploit fractional things.
This is somewhat similar to https://gitlab.mpi-sws.org/iris/iris/-/issues/186.
To avoid making a mess, probably we should figure out https://gitlab.mpi-sws.org/iris/iris/-/issues/139 first.https://gitlab.mpi-sws.org/iris/iris/-/issues/349Parameterize WP (and more) by the notion of fancy update2020-09-22T07:47:46ZRalf Jungjung@mpi-sws.orgParameterize WP (and more) by the notion of fancy updateFor Perennial, @jtassaro developed a notion of "fancy updates" that satisfies all the laws we have in Iris, plus way more. Unfortunately this means we cannot directly use anything from `base_logc/lib` and above, even though all these proofs do go through unchanged.
This change is likely not canonical enough to be upstreamable, and I see no way to make our notion of fancy updates itself general enough that @jtassaro's update are an instance of them. The design space is very wide open here.
It would thus be useful if we could parameterize the definition of WP by the notion of fancy update, and similar for some of the things in `base_logic/lib` -- everything that mentions fancy updates, basically (or at least anything useful; I don't think it is worth doing this with STS and auth). Maybe some things can be changed to use basic updates instead of fancy updates, which would avoid the need for parameterization.
Even semantic invariants themselves can be defined generally for any fancy update; the only thing that each update would need to prove is the allocation lemma(s).
@robbertkrebbers what do you think?For Perennial, @jtassaro developed a notion of "fancy updates" that satisfies all the laws we have in Iris, plus way more. Unfortunately this means we cannot directly use anything from `base_logc/lib` and above, even though all these proofs do go through unchanged.
This change is likely not canonical enough to be upstreamable, and I see no way to make our notion of fancy updates itself general enough that @jtassaro's update are an instance of them. The design space is very wide open here.
It would thus be useful if we could parameterize the definition of WP by the notion of fancy update, and similar for some of the things in `base_logic/lib` -- everything that mentions fancy updates, basically (or at least anything useful; I don't think it is worth doing this with STS and auth). Maybe some things can be changed to use basic updates instead of fancy updates, which would avoid the need for parameterization.
Even semantic invariants themselves can be defined generally for any fancy update; the only thing that each update would need to prove is the allocation lemma(s).
@robbertkrebbers what do you think?https://gitlab.mpi-sws.org/iris/iris/-/issues/348Always enabled invariants2020-09-30T19:14:58ZRalf Jungjung@mpi-sws.orgAlways enabled invariants@jtassaro has a fork of Iris with some interesting features that we might want to copy. In particular, for Perennial he added "always-enabled invariants", which have no mask, can always be opened, but cannot be kept open. The accessor lemma is (roughly):
```
Lemma ae_inv_acc_bupd E P Q :
ae_inv P -∗
(▷ P ==∗ ◇ (▷ P ∗ Q)) -∗
|={E}=> Q.
```
This seems like it could be useful beyond Perennial. In particular, this forms a layer of abstraction *beneath* the invariants that we have: `ownI` (underlying `inv`) can be defined in terms of `ae_inv` with something like
```
ownI i Q := Q ∗ ownD {[i]} ∨ ownE {[i]})
```
(That's not how Joe defined them, but I am pretty sure it could be done.)@jtassaro has a fork of Iris with some interesting features that we might want to copy. In particular, for Perennial he added "always-enabled invariants", which have no mask, can always be opened, but cannot be kept open. The accessor lemma is (roughly):
```
Lemma ae_inv_acc_bupd E P Q :
ae_inv P -∗
(▷ P ==∗ ◇ (▷ P ∗ Q)) -∗
|={E}=> Q.
```
This seems like it could be useful beyond Perennial. In particular, this forms a layer of abstraction *beneath* the invariants that we have: `ownI` (underlying `inv`) can be defined in terms of `ae_inv` with something like
```
ownI i Q := Q ∗ ownD {[i]} ∨ ownE {[i]})
```
(That's not how Joe defined them, but I am pretty sure it could be done.)https://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/346Typeclass inference fails to trigger.2020-09-21T18:08:44ZArthur Azevedo de AmorimTypeclass inference fails to trigger.I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap numbers.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import auth invariants.
Section Test.
Context `{!invG Σ, !authG Σ (gmapUR nat natR)}.
Implicit Types m : gmap nat nat.
Definition my_inv m : iProp Σ := True.
Goal ∀ γ, auth_ctx γ nroot id my_inv ={⊤}=∗ False.
iIntros (γ) "Hctx".
iMod (auth_empty γ) as "#Hinit".
iMod (auth_acc _ _ _ _ _ ε with "[Hctx Hinit]") as "Hinv"; try by eauto.
(* Inhabited (gmap nat nat) is now shelved... *)
Abort.
End Test.
```I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap numbers.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import auth invariants.
Section Test.
Context `{!invG Σ, !authG Σ (gmapUR nat natR)}.
Implicit Types m : gmap nat nat.
Definition my_inv m : iProp Σ := True.
Goal ∀ γ, auth_ctx γ nroot id my_inv ={⊤}=∗ False.
iIntros (γ) "Hctx".
iMod (auth_empty γ) as "#Hinit".
iMod (auth_acc _ _ _ _ _ ε with "[Hctx Hinit]") as "Hinv"; try by eauto.
(* Inhabited (gmap nat nat) is now shelved... *)
Abort.
End Test.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/345Check for `options.v` should only consider files in _CoqProject2020-09-12T10:10:58ZRobbert KrebbersCheck for `options.v` should only consider files in _CoqProjectNow if I have random files in my theories folder, `make` will give errors.Now if I have random files in my theories folder, `make` will give errors.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/344Set Default Goal Selector2020-11-10T19:12:02ZRalf Jungjung@mpi-sws.orgSet Default Goal SelectorAs a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.As a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.https://gitlab.mpi-sws.org/iris/iris/-/issues/343Make CI fail when proofs depend on auto-generated names2021-04-12T17:11:13ZRalf Jungjung@mpi-sws.orgMake CI fail when proofs depend on auto-generated namesWe already did it in std++, now [that this is fixed](https://github.com/coq/coq/issues/12944) it is time to do the same in Iris: make CI ensure that we do not use auto-generated names.We already did it in std++, now [that this is fixed](https://github.com/coq/coq/issues/12944) it is time to do the same in Iris: make CI ensure that we do not use auto-generated names.https://gitlab.mpi-sws.org/iris/iris/-/issues/342Missing {u,}rFunctors and conversions2020-09-10T17:45:28ZPaolo G. GiarrussoMissing {u,}rFunctors and conversionsSome missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable through the above conversion, and @jung suggests that's an oversight; OTOH, that alerted me to a bug; I only needed it because I tried writing `GFunctor (gmapRF ...)`, which does not seem useful
- `listRF` does not exist (which I noticed while grepping)Some missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable through the above conversion, and @jung suggests that's an oversight; OTOH, that alerted me to a bug; I only needed it because I tried writing `GFunctor (gmapRF ...)`, which does not seem useful
- `listRF` does not exist (which I noticed while grepping)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/340Polymorphic equality for HeapLang2020-08-22T19:06:03ZDan FruminPolymorphic equality for HeapLangIt would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.It would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.