Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-06-30T17:27:28Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/420Use siProp more in building the uPred (and BI) interfaces2021-06-30T17:27:28ZRalf Jungjung@mpi-sws.orgUse siProp more in building the uPred (and BI) interfacesuPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.uPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/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`.https://gitlab.mpi-sws.org/iris/iris/-/issues/413Better errors when tactic fails to automatically resolve some side-condition2021-07-22T12:54:29ZRalf Jungjung@mpi-sws.orgBetter errors when tactic fails to automatically resolve some side-condition@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-condition; we could introduce something like
```
Definition pm_error (s : string) := False
```
and add instances with `error "foo"` as their side-condition; together with some support in `iSolveSideCondition` this could be used to then show better, instance-specific error messages when `iMod` fails.
2. We could add a new typeclass like `ElimModalError` that is used to compute an error message when `ElimModal` failed to find an instance.
Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as `iMod` with mismatching masks:
1. `ElimModal` already has support for a pure side-condition; we could introduce something like
```
Definition pm_error (s : string) := False
```
and add instances with `error "foo"` as their side-condition; together with some support in `iSolveSideCondition` this could be used to then show better, instance-specific error messages when `iMod` fails.
2. We could add a new typeclass like `ElimModalError` that is used to compute an error message when `ElimModal` failed to find an instance.
Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.https://gitlab.mpi-sws.org/iris/iris/-/issues/412Use dfrac everywhere2021-04-23T12:47:13ZRalf Jungjung@mpi-sws.orgUse dfrac everywhere`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [ ] `algebra.lib.gmap_view`
* [ ] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more `auth`-based abstractions in `algebra.lib` but those do not expose *any* fraction on their authoritative part yet.
Some more are not actually built on top of `view`, but these are or could be exposing fractions that it might be useful to turn into `dfrac`:
* [ ] `base_logic.lib.ghost_var`
* [ ] Cancelable invariants
* [ ] Saved propositions (could be made essentially "`ghost_var` with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs *harder* to use for the common case of only needing fraction `1`. For `gset_bij`, we are already in the situation that users need to write `DfracOwn 1` a lot; I wouldn't want the same to happen e.g. for `ghost_map`.`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [ ] `algebra.lib.gmap_view`
* [ ] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more `auth`-based abstractions in `algebra.lib` but those do not expose *any* fraction on their authoritative part yet.
Some more are not actually built on top of `view`, but these are or could be exposing fractions that it might be useful to turn into `dfrac`:
* [ ] `base_logic.lib.ghost_var`
* [ ] Cancelable invariants
* [ ] Saved propositions (could be made essentially "`ghost_var` with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs *harder* to use for the common case of only needing fraction `1`. For `gset_bij`, we are already in the situation that users need to write `DfracOwn 1` a lot; I wouldn't want the same to happen e.g. for `ghost_map`.https://gitlab.mpi-sws.org/iris/iris/-/issues/411Taking ∃ out of ▷ without Inhabited, more easily2021-04-29T09:25:44ZYusuke MatsushitaTaking ∃ out of ▷ without Inhabited, more easilyIn Iris Proof Mode, destruction of `▷ (∃ (x: A), Φ a)` into `(x) "H"` (where `"H"` will assert `▷ Φ x`) always requires `Inhabited A`, because it uses the lemma `later_exist`.
In some situations, `Inhabited A` is not known a priori.
If we use the lemma `later_exist_except_0` instead, we get `▷ Φ x` without having `Inhabited A`, under the `◇` modality.
In Iris we are often under the `◇` modality because the update modality `|=>` contains `◇`.
I hope the operation of taking `∃x` out of `▷` without `Inhabited` becomes easier to use.
One possibility is to let Iris Proof Mode apply `later_exist_except_0` when the goal is under the `◇` modality.In Iris Proof Mode, destruction of `▷ (∃ (x: A), Φ a)` into `(x) "H"` (where `"H"` will assert `▷ Φ x`) always requires `Inhabited A`, because it uses the lemma `later_exist`.
In some situations, `Inhabited A` is not known a priori.
If we use the lemma `later_exist_except_0` instead, we get `▷ Φ x` without having `Inhabited A`, under the `◇` modality.
In Iris we are often under the `◇` modality because the update modality `|=>` contains `◇`.
I hope the operation of taking `∃x` out of `▷` without `Inhabited` becomes easier to use.
One possibility is to let Iris Proof Mode apply `later_exist_except_0` when the goal is under the `◇` modality.https://gitlab.mpi-sws.org/iris/iris/-/issues/402iFrame performance issues2021-02-17T08:50:16ZRalf 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 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`.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/399Upstream more big_op lemmas from Perennial2021-02-17T08:49:05ZRalf Jungjung@mpi-sws.orgUpstream more big_op lemmas from PerennialPerennial has a bunch of big_op lemmas at <https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op>. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.Perennial has a bunch of big_op lemmas at <https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op>. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.https://gitlab.mpi-sws.org/iris/iris/-/issues/398Use `dom` instead of `∀ k, is_Some (.. !! k) ...`2021-02-17T08:48:46ZRobbert KrebbersUse `dom` instead of `∀ k, is_Some (.. !! k) ...`See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas for `dom`. However, the fact that the set (here `gset`) has to specified explicitly might be annoying.
Note that if we perform this change, there are also some lemmas in std++ that need to be changed.See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas for `dom`. However, the fact that the set (here `gset`) has to specified explicitly might be annoying.
Note that if we perform this change, there are also some lemmas in std++ that need to be changed.https://gitlab.mpi-sws.org/iris/iris/-/issues/392Masks in step-taking fupd notation2020-12-10T13:37:03ZRalf Jungjung@mpi-sws.orgMasks in step-taking fupd notationEarlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?Earlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/391Add append-only list RA to Iris2021-05-17T16:32:27ZRalf Jungjung@mpi-sws.orgAdd append-only list RA to IrisAppend-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote [a version of this](https://gitlab.mpi-sws.org/iris/gpfsl/-/blob/graphs/theories/examples/list_cmra.v), which was forked at some point by @jtassaro [for Perennial](https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v) while also adding a logic-level wrapper for `auth (mlist T)` with the following three core assertions:
* authoritative ownership of the full trace
* persistent ownership that some list is a prefix of the trace
* persistent ownership that index i in the trace has some particular value
Perennial also has [another version of this](https://github.com/mit-pdos/perennial/blob/master/src/algebra/append_list.v) by @tchajed that is based on (the Perennial version of) `gmap_view`. And finally, @msammler has [his own implementation](https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18) that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.Append-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote [a version of this](https://gitlab.mpi-sws.org/iris/gpfsl/-/blob/graphs/theories/examples/list_cmra.v), which was forked at some point by @jtassaro [for Perennial](https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v) while also adding a logic-level wrapper for `auth (mlist T)` with the following three core assertions:
* authoritative ownership of the full trace
* persistent ownership that some list is a prefix of the trace
* persistent ownership that index i in the trace has some particular value
Perennial also has [another version of this](https://github.com/mit-pdos/perennial/blob/master/src/algebra/append_list.v) by @tchajed that is based on (the Perennial version of) `gmap_view`. And finally, @msammler has [his own implementation](https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18) that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/385reshape_expr does not recognize `fill`2020-12-05T08:58:01ZRalf Jungjung@mpi-sws.orgreshape_expr does not recognize `fill`There was not much fallout from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/588, but the bits I saw look like `reshape_expr` is not able to traverse into a `fill K e`. That should be possible, right? If yes, it could avoid re-enabling that instance locally in ReLoC, C and Actris.There was not much fallout from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/588, but the bits I saw look like `reshape_expr` is not able to traverse into a `fill K e`. That should be possible, right? If yes, it could avoid re-enabling that instance locally in ReLoC, C and Actris.https://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/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/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/369Document HeapLang2021-07-01T15:42:37ZRalf 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 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.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/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/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/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/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?