Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-10-21T10:59:16Zhttps://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/358Add a logic-level version of gmap_view2020-11-02T19:03:07ZRalf 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/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/300vs doesn't use FUpd2020-03-30T09:38:01ZGregory Malechavs doesn't use FUpdIs there a reason that the definition of `vs` explicitly mentions `iProp`? In practice it means that its notation can not be used in lifted logics such as `monPred`. For example, writing `P ==> Q` works at `iProp`, but doesn't work at `monPred x (iProp _)` even though all of the other notation (that are conceptually very simple) do work at `monPred`.Is there a reason that the definition of `vs` explicitly mentions `iProp`? In practice it means that its notation can not be used in lifted logics such as `monPred`. For example, writing `P ==> Q` works at `iProp`, but doesn't work at `monPred x (iProp _)` even though all of the other notation (that are conceptually very simple) do work at `monPred`.https://gitlab.mpi-sws.org/iris/iris/-/issues/267Inconsistent order of arguments for `inv_alloc` and `cinv_alloc`.2019-11-01T13:07:58ZDan FruminInconsistent order of arguments for `inv_alloc` and `cinv_alloc`.```
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
```
vs
```
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
```
As you can see, `inv_alloc` first takes the namespace and then the mask, but `cinv_alloc` first takes the mask and the the namespace.```
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
```
vs
```
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
```
As you can see, `inv_alloc` first takes the namespace and then the mask, but `cinv_alloc` first takes the mask and the the namespace.https://gitlab.mpi-sws.org/iris/iris/-/issues/227Provide a convenient way to define non-recursive ghost state2019-11-04T15:18:44ZRalf Jungjung@mpi-sws.orgProvide a convenient way to define non-recursive ghost stateIt is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
```
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
```
To make things worse, if you forget the `lockΣ`, your proof will still work. You might just have assumed false, accidentally.
Can we do better than that, at least for the simple and common case of non-recursive ghost state?It is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
```
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
```
To make things worse, if you forget the `lockΣ`, your proof will still work. You might just have assumed false, accidentally.
Can we do better than that, at least for the simple and common case of non-recursive ghost state?