Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-11-11T16:57:53Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/380iDestruct does not handle some patterns that it probably could2020-11-11T16:57:53ZTej Chajedtchajed@mit.eduiDestruct does not handle some patterns that it probably couldThe pattern match in `iDestructHypGo` misses a handful of patterns that perhaps it could process. For example `IDone` could probably be given a sensible interpretation.
Similarly `iDestructHypFindPat` complains about `H //` even though that could be processed as `iDestruct ... as H; done`. It does handle `H /=` (by running `simpl` after the destruct).The pattern match in `iDestructHypGo` misses a handful of patterns that perhaps it could process. For example `IDone` could probably be given a sensible interpretation.
Similarly `iDestructHypFindPat` complains about `H //` even though that could be processed as `iDestruct ... as H; done`. It does handle `H /=` (by running `simpl` after the destruct).https://gitlab.mpi-sws.org/iris/iris/-/issues/379Make sealing consistent and document it2020-11-10T13:15:28ZRalf Jungjung@mpi-sws.orgMake sealing consistent and document itWe should document the "sealing" pattern that we use throughout Iris, and make sure that we use it in a consistent way. Things to take care of:
* Avoid eta-expanding the sealed definition; that means that the write lemma only applies to the eta-expanded term. This immediately implies that sealing should be done outside of sections.
* Add an `unseal` tactic, either as `Local Ltac` or in a module to avoid polluting the global namespace.
* There is no need to make sealed definitions `Typeclasses Opaque`.
- no eta, ergo no sections
- unseal tactic
- no TC opaque
For example, here is how sealing of a logic-level RA wrapper could look like:
```
Definition mnat_own_auth_def `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
own γ (mnat_auth_auth q n).
Definition mnat_own_auth_aux : seal (@mnat_own_auth_def). Proof. by eexists. Qed.
Definition mnat_own_auth := mnat_own_auth_aux.(unseal).
Definition mnat_own_auth_eq : @mnat_own_auth = @mnat_own_auth_def := mnat_own_auth_aux.(seal_eq).
Arguments mnat_own_auth {Σ _} γ q n.
Definition mnat_own_lb_def `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (mnat_auth_frag n).
Definition mnat_own_lb_aux : seal (@mnat_own_lb_def). Proof. by eexists. Qed.
Definition mnat_own_lb := mnat_own_lb_aux.(unseal).
Definition mnat_own_lb_eq : @mnat_own_lb = @mnat_own_lb_def := mnat_own_lb_aux.(seal_eq).
Arguments mnat_own_lb {Σ _} γ n.
Local Ltac unseal := rewrite
?mnat_own_auth_eq /mnat_own_auth_def
?mnat_own_lb_eq /mnat_own_lb_def.
```
When there are operational typeclasses involved, the `_eq` lemma should also account for those to avoid having to rewrite twice:
```
Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
Arguments monPred_bupd {_}.
Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
```We should document the "sealing" pattern that we use throughout Iris, and make sure that we use it in a consistent way. Things to take care of:
* Avoid eta-expanding the sealed definition; that means that the write lemma only applies to the eta-expanded term. This immediately implies that sealing should be done outside of sections.
* Add an `unseal` tactic, either as `Local Ltac` or in a module to avoid polluting the global namespace.
* There is no need to make sealed definitions `Typeclasses Opaque`.
- no eta, ergo no sections
- unseal tactic
- no TC opaque
For example, here is how sealing of a logic-level RA wrapper could look like:
```
Definition mnat_own_auth_def `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
own γ (mnat_auth_auth q n).
Definition mnat_own_auth_aux : seal (@mnat_own_auth_def). Proof. by eexists. Qed.
Definition mnat_own_auth := mnat_own_auth_aux.(unseal).
Definition mnat_own_auth_eq : @mnat_own_auth = @mnat_own_auth_def := mnat_own_auth_aux.(seal_eq).
Arguments mnat_own_auth {Σ _} γ q n.
Definition mnat_own_lb_def `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (mnat_auth_frag n).
Definition mnat_own_lb_aux : seal (@mnat_own_lb_def). Proof. by eexists. Qed.
Definition mnat_own_lb := mnat_own_lb_aux.(unseal).
Definition mnat_own_lb_eq : @mnat_own_lb = @mnat_own_lb_def := mnat_own_lb_aux.(seal_eq).
Arguments mnat_own_lb {Σ _} γ n.
Local Ltac unseal := rewrite
?mnat_own_auth_eq /mnat_own_auth_def
?mnat_own_lb_eq /mnat_own_lb_def.
```
When there are operational typeclasses involved, the `_eq` lemma should also account for those to avoid having to rewrite twice:
```
Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
Arguments monPred_bupd {_}.
Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/378Graveyard for obsolete code2021-06-02T22:38:25ZRobbert KrebbersGraveyard for obsolete codeThere is some obsolete code in Iris, like Hoare triples, view shifts, STS, the logic-level wrapper for auth, that have bit rot quite a bit and should basically never be used by end-users.
Since this code supports some claims in papers, it might be useful to keep it in some form. But what would be the best place?There is some obsolete code in Iris, like Hoare triples, view shifts, STS, the logic-level wrapper for auth, that have bit rot quite a bit and should basically never be used by end-users.
Since this code supports some claims in papers, it might be useful to keep it in some form. But what would be the best place?https://gitlab.mpi-sws.org/iris/iris/-/issues/375We have some lonely notations2020-11-05T12:15:18ZRalf Jungjung@mpi-sws.orgWe have some lonely notationsThe following is the list of notations that are "lonely", which means they are not in a scope: (in some heap_lang file, so there might be things this does not import)
```
Lonely notations
"✓{ n } x" := validN n x
"◯V a" := view_frag a
"◯ a" := auth_frag a
"●{ q } a" := auth_auth q a
"●V{ q } a" := view_auth q a
"●V a" := view_auth (pos_to_Qp xH) a
"● a" := auth_auth (pos_to_Qp xH) a
"↑ x" := up_close x
"'λne' x .. y , t" := OfeMor (fun x => .. (OfeMor (fun y => t)) ..)
"'λ' x .. y , t" := fun x => .. (fun y => t) ..
"x ◎ y" := ccompose x y
"x ≥ y" := ge x y
"x ≤ y" := le x y
"x ≡{ n }≡ y" := dist n x y
"x ≡{ n }@{ A }≡ y" := dist n x y
"x ~~>: y" := cmra_updateP x y
"x ~~> y" := cmra_update x y
"x ~l~> y" := local_update x y
"x ||* y" := zip_with orb x y
"x =.>* y" := Forall2 bool_le x y
"x =.> y" := bool_le x y
"x :b: y" := cons_binder x y
"p .2" := snd p
"p .1" := fst p
"ps .*2" := fmap snd ps
"ps .*1" := fmap fst ps
"TT -t> A" := tele_fun TT A
"A -n> B" := ofe_morO A B
"A -d> B" := discrete_funO (fun _ => B)
"x +b+ y" := app_binder x y
"x &&* y" := zip_with andb x y
"'[tele_arg' x ; .. ; z ]" := TargS x .. (TargS z TargO) ..
"'[tele_arg' ]" := TargO
"'[tele' x .. z ]" := TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)
"'[tele' ]" := TeleO
"(||)" := orb
" () " := tt
"(&&)" := andb
"( H 'with' pat )" := {| itrm := H; itrm_vars := hlist.hnil; itrm_hyps := pat |}
"( H $! x1 .. xn 'with' pat )" := {|
itrm := H;
itrm_vars := hlist.hcons x1 .. (hlist.hcons xn hlist.hnil) ..;
itrm_hyps := pat |}
"( H $! x1 .. xn )" := {|
itrm := H;
itrm_vars := hlist.hcons x1 .. (hlist.hcons xn hlist.hnil) ..;
itrm_hyps := EmptyString |}
"#[ Σ1 ; .. ; Σn ]" := gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..
"#[ ]" := gFunctors.nil
"# l" := LitV l
```
Many of those are from Iris or std++, and are probably oversights.The following is the list of notations that are "lonely", which means they are not in a scope: (in some heap_lang file, so there might be things this does not import)
```
Lonely notations
"✓{ n } x" := validN n x
"◯V a" := view_frag a
"◯ a" := auth_frag a
"●{ q } a" := auth_auth q a
"●V{ q } a" := view_auth q a
"●V a" := view_auth (pos_to_Qp xH) a
"● a" := auth_auth (pos_to_Qp xH) a
"↑ x" := up_close x
"'λne' x .. y , t" := OfeMor (fun x => .. (OfeMor (fun y => t)) ..)
"'λ' x .. y , t" := fun x => .. (fun y => t) ..
"x ◎ y" := ccompose x y
"x ≥ y" := ge x y
"x ≤ y" := le x y
"x ≡{ n }≡ y" := dist n x y
"x ≡{ n }@{ A }≡ y" := dist n x y
"x ~~>: y" := cmra_updateP x y
"x ~~> y" := cmra_update x y
"x ~l~> y" := local_update x y
"x ||* y" := zip_with orb x y
"x =.>* y" := Forall2 bool_le x y
"x =.> y" := bool_le x y
"x :b: y" := cons_binder x y
"p .2" := snd p
"p .1" := fst p
"ps .*2" := fmap snd ps
"ps .*1" := fmap fst ps
"TT -t> A" := tele_fun TT A
"A -n> B" := ofe_morO A B
"A -d> B" := discrete_funO (fun _ => B)
"x +b+ y" := app_binder x y
"x &&* y" := zip_with andb x y
"'[tele_arg' x ; .. ; z ]" := TargS x .. (TargS z TargO) ..
"'[tele_arg' ]" := TargO
"'[tele' x .. z ]" := TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)
"'[tele' ]" := TeleO
"(||)" := orb
" () " := tt
"(&&)" := andb
"( H 'with' pat )" := {| itrm := H; itrm_vars := hlist.hnil; itrm_hyps := pat |}
"( H $! x1 .. xn 'with' pat )" := {|
itrm := H;
itrm_vars := hlist.hcons x1 .. (hlist.hcons xn hlist.hnil) ..;
itrm_hyps := pat |}
"( H $! x1 .. xn )" := {|
itrm := H;
itrm_vars := hlist.hcons x1 .. (hlist.hcons xn hlist.hnil) ..;
itrm_hyps := EmptyString |}
"#[ Σ1 ; .. ; Σn ]" := gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..
"#[ ]" := gFunctors.nil
"# l" := LitV l
```
Many of those are from Iris or std++, and are probably oversights.https://gitlab.mpi-sws.org/iris/iris/-/issues/374Avoid sequences of "_" by adjusting lemma statements2020-11-05T12:11:02ZRalf Jungjung@mpi-sws.orgAvoid sequences of "_" by adjusting lemma statementsSome Iris lemmas are prone to needing plenty of `_` almost every time they are used. I noticed this in particular for
* most big-op lemmas that access a single element, where the to-be-accessed element needs to be given explicitly, but often other arguments come first
* several allocation lemmas such as `inv_alloc`, where the to-be-allocated thing needs to be given explicitly, but other arguments come first
* many of the update lemmas, where typically one works with `iMod`, so the new values (e.g. new lower bound for mono_nat, or new key and value for gmap) need to be given, but they are often the last arguments
There are two ways to fix this:
* reorder arguments, so that those that are likely to be determined by unification come first
* make likely-to-be-determined-by-unification arguments implicit, so that we do not have to write out their `_`
I am in favor of the second approach because it has a better failure mode: if one of those arguments ends up *not* being determined by unification, we have use `lemma (arg:=val)` to explicitly give the value for this agument. For lemmas with many arguments, this name-based approach is anyway much easier to read and write than the position-based approach (no need to remember the exact order of arguments).
However, while implicit arguments are widely used in Iris, we usually control them on a per-section basis, not a per-lemma basis. @robbertkrebbers has objected the used of implicit arguments for this reason. (That is my understanding, anyway.)Some Iris lemmas are prone to needing plenty of `_` almost every time they are used. I noticed this in particular for
* most big-op lemmas that access a single element, where the to-be-accessed element needs to be given explicitly, but often other arguments come first
* several allocation lemmas such as `inv_alloc`, where the to-be-allocated thing needs to be given explicitly, but other arguments come first
* many of the update lemmas, where typically one works with `iMod`, so the new values (e.g. new lower bound for mono_nat, or new key and value for gmap) need to be given, but they are often the last arguments
There are two ways to fix this:
* reorder arguments, so that those that are likely to be determined by unification come first
* make likely-to-be-determined-by-unification arguments implicit, so that we do not have to write out their `_`
I am in favor of the second approach because it has a better failure mode: if one of those arguments ends up *not* being determined by unification, we have use `lemma (arg:=val)` to explicitly give the value for this agument. For lemmas with many arguments, this name-based approach is anyway much easier to read and write than the position-based approach (no need to remember the exact order of arguments).
However, while implicit arguments are widely used in Iris, we usually control them on a per-section basis, not a per-lemma basis. @robbertkrebbers has objected the used of implicit arguments for this reason. (That is my understanding, anyway.)https://gitlab.mpi-sws.org/iris/iris/-/issues/373Quote does not handle ⊣⊢2020-11-05T11:12:30ZRodolphe LepigreQuote does not handle ⊣⊢The `solve_sep_equiv` tactic from `bi.tactics` cannot be used to solve goals of the form `_ ⊣⊢ _`.
This is due to `quote` only accepting goals of the form `_ ⊢ _` (see [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/tactics.v#L136)). Can it be made more general?The `solve_sep_equiv` tactic from `bi.tactics` cannot be used to solve goals of the form `_ ⊣⊢ _`.
This is due to `quote` only accepting goals of the form `_ ⊢ _` (see [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/tactics.v#L136)). Can it be made more general?https://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/370Add missing instances for `Duplicable` and fix `Hint Immediate` for `persiste...2020-11-04T12:05:50ZSimon Friis VindumAdd missing instances for `Duplicable` and fix `Hint Immediate` for `persistent_duplicable`Following the merge of !481 instances of `Duplicable` for `<subj>` and `embed` should be added.
@robbertkrebbers has kindly offered to do this.Following the merge of !481 instances of `Duplicable` for `<subj>` and `embed` should be added.
@robbertkrebbers has kindly offered to do this.https://gitlab.mpi-sws.org/iris/iris/-/issues/369Document HeapLang2020-10-30T10:30:22ZRalf Jungjung@mpi-sws.orgDocument HeapLangThe HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently my thesis and the "Future is Ours" paper describe overlapping but incomparable subsets of the operational semantics, and there are likely bits that are missing from both.The HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently my thesis and the "Future is Ours" paper 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/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/366`Export` everywhere does not permit consistent shadowing2020-11-05T11:54:13ZRalf Jungjung@mpi-sws.org`Export` everywhere does not permit consistent shadowingWhen using `Export`, even if imports are ordered consistently, there is sometimes no way to obtain consistent shadowing:
```
From stdpp Require base.
Module or.
Export stdpp.base.
Definition or_comm := 10.
End or.
Module and.
Export stdpp.base.
Definition and_comm := 11.
End and.
Module A.
Import or and.
Locate or_comm.
(*
Constant stdpp.base.or_comm
Constant Coq.Init.Logic.or_comm (shorter name to refer to it in current context is Logic.or_comm)
Constant Top.or.or_comm (shorter name to refer to it in current context is or.or_comm)
*)
Locate and_comm.
(*
Constant Top.and.and_comm
Constant Coq.Init.Logic.and_comm (shorter name to refer to it in current context is Logic.and_comm)
Constant stdpp.base.and_comm (shorter name to refer to it in current context is base.and_comm)
*)
End A.
```
Here, importing `and` overwrites `or_comm` because of the `stdpp.base` export.
I think the only way to avoid this is to avoid `Export`ing except when the re-exported symbols are conceptually really part of that library (such as `stdpp.prelude`).When using `Export`, even if imports are ordered consistently, there is sometimes no way to obtain consistent shadowing:
```
From stdpp Require base.
Module or.
Export stdpp.base.
Definition or_comm := 10.
End or.
Module and.
Export stdpp.base.
Definition and_comm := 11.
End and.
Module A.
Import or and.
Locate or_comm.
(*
Constant stdpp.base.or_comm
Constant Coq.Init.Logic.or_comm (shorter name to refer to it in current context is Logic.or_comm)
Constant Top.or.or_comm (shorter name to refer to it in current context is or.or_comm)
*)
Locate and_comm.
(*
Constant Top.and.and_comm
Constant Coq.Init.Logic.and_comm (shorter name to refer to it in current context is Logic.and_comm)
Constant stdpp.base.and_comm (shorter name to refer to it in current context is base.and_comm)
*)
End A.
```
Here, importing `and` overwrites `or_comm` because of the `stdpp.base` export.
I think the only way to avoid this is to avoid `Export`ing except when the re-exported symbols are conceptually really part of that library (such as `stdpp.prelude`).https://gitlab.mpi-sws.org/iris/iris/-/issues/364Implement typeclasses analogous to Fractional and AsFractional for discardabl...2020-10-21T10:59:16ZTej Chajedtchajed@mit.eduImplement typeclasses analogous to Fractional and AsFractional for discardable fractionsI think it would make sense to have a library analogous to fractional for discardable fractions. I think it needs to say `Φ (p ⋅ q) ⊣⊢ Φ p ∗ Φ q` like for fractions (using dfrac composition) and also perhaps `Persistent (Φ DfracDiscarded)`.I think it would make sense to have a library analogous to fractional for discardable fractions. I think it needs to say `Φ (p ⋅ q) ⊣⊢ Φ p ∗ Φ q` like for fractions (using dfrac composition) and also perhaps `Persistent (Φ DfracDiscarded)`.https://gitlab.mpi-sws.org/iris/iris/-/issues/363Collect Iris versions required by artifacts2020-11-23T12:56:33ZRalf Jungjung@mpi-sws.orgCollect Iris versions required by artifactsI'd like to clean up https://gitlab.mpi-sws.org/iris/opam, to avoid opam issues due to having too many versions of a package. However, it turns out in the past some of the Iris paper artifacts are not self-contained, and instead rely on the opam repository. We should figure out which versions of Iris are required by an artifact, and keep them in the repository.I'd like to clean up https://gitlab.mpi-sws.org/iris/opam, to avoid opam issues due to having too many versions of a package. However, it turns out in the past some of the Iris paper artifacts are not self-contained, and instead rely on the opam repository. We should figure out which versions of Iris are required by an artifact, and keep them in the repository.https://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 @tchajed