Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-07-15T16:05:09Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/306Iris 3.3 release planning2020-07-15T16:05:09ZRalf Jungjung@mpi-sws.orgIris 3.3 release planningWhat needs to happen for the release:
* [x] Add things we want to do to [the milestone](https://gitlab.mpi-sws.org/iris/iris/-/milestones/5).
* [x] Do all the things in the milestone.
* [x] Complete the CHANGELOG
* [x] Complete the sed s...What needs to happen for the release:
* [x] Add things we want to do to [the milestone](https://gitlab.mpi-sws.org/iris/iris/-/milestones/5).
* [x] Do all the things in the milestone.
* [x] Complete the CHANGELOG
* [x] Complete the sed script in the CHANGELOG.
* [x] Release a matching std++.
* [x] Write announcement.
* [x] Release opam packages on coq opam registry.
* [x] Send out announcements.Iris 3.3https://gitlab.mpi-sws.org/iris/iris/-/issues/315Port HeapLang tactics to more efficient style2020-07-15T19:27:00ZRobbert KrebbersPort HeapLang tactics to more efficient styleThe heaplang tactics do not use the `match` trick to avoid additional proof mode context arguments. They should be rewritten in the style in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/248The heaplang tactics do not use the `match` trick to avoid additional proof mode context arguments. They should be rewritten in the style in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/248https://gitlab.mpi-sws.org/iris/iris/-/issues/333Iris Library Best Practices2020-08-06T16:37:12ZRalf Jungjung@mpi-sws.orgIris Library Best PracticesWe should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered for...We should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered form. Other aspects are not mentioned; @blaisorblade pointed out that it is non-obvious that specs should not contain `own` but instead wrap those things in their own definitions that depend on `libG` instead of `inG`.https://gitlab.mpi-sws.org/iris/iris/-/issues/295Have iApply introduce equalities for subterms that cannot be unified directly2020-08-08T21:57:49ZArmaël GuéneauHave iApply introduce equalities for subterms that cannot be unified directlyThe initial motivation is to be able to go from a proof-mode goal of the form:
```
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
```
to
```
--------------------------------------∗
⌜x4 ...The initial motivation is to be able to go from a proof-mode goal of the form:
```
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
```
to
```
--------------------------------------∗
⌜x4 = z⌝
```
without relying explicitly on the names `x4` and `z`.
I'm not sure what would be the most general form of such a tactic, or what its user interface would be, though. I think it would be nice to have it as an instance of `iApply`, if that's possible. (having it in `iFrame` as well is perhaps possible but risky, for instance in the case of mapsto it should at least be restricted to mapsto with the same syntactic location...).https://gitlab.mpi-sws.org/iris/iris/-/issues/337Weird automatically generated names2020-08-12T16:46:47ZRobbert KrebbersWeird automatically generated namesAfter @tchajed's !479 the following happens:
```coq
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
```
This names the automatic...After @tchajed's !479 the following happens:
```coq
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
```
This names the automatically generated hypothesis `x`.
```
1 subgoal
PROP : bi
x : True
______________________________________(1/1)
_ : ⌜0 = 0⌝
--------------------------------------□
True
```
I don't understand where the name `x` comes from, but it's very annoying. The `∃ _ : ..., ...` pattern is often used for `inG`, and the `inG` being called `x` is very annoying. It prevents one from using `x` for other variables.
Obviously, in this case I could use `iDestruct foo as (name_for_my_inG) "?"`, but I really don't want to name that hypothesis.https://gitlab.mpi-sws.org/iris/iris/-/issues/336Use user-supplied names in iIntros (?)2020-08-12T16:46:47ZTej Chajedtchajed@gmail.comUse user-supplied names in iIntros (?)Similar to !479, the proof mode should preserve user names in binders in `iIntros (?)`.
This depends on !479 since there's some common infrastructure for representing and threading identifiers through typeclasses.Similar to !479, the proof mode should preserve user names in binders in `iIntros (?)`.
This depends on !479 since there's some common infrastructure for representing and threading identifiers through typeclasses.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.https://gitlab.mpi-sws.org/iris/iris/-/issues/318Drop support for Coq 8.9?2020-08-24T08:47:06ZRalf Jungjung@mpi-sws.orgDrop support for Coq 8.9?Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.
* https://gitlab.mpi-sws.org/iris/iris/-/issues/317 requires 8.10 I think.
* [non-canonical projections](`https://github.com/coq/coq/pull/10076`...Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.
* https://gitlab.mpi-sws.org/iris/iris/-/issues/317 requires 8.10 I think.
* [non-canonical projections](`https://github.com/coq/coq/pull/10076`)
* `change_no_check` (to stop using deprecated `convert_concl_no_check`)
* `Declare Scope` (to fix deprecated use of undeclared scopes)
Is there more?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. Ri...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/338Missing unseal tactic for siProp2020-08-30T07:04:36ZPaolo G. GiarrussoMissing unseal tactic for siProp
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_...
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl.
(* Should be siProp.unseal. *)
Ltac siProp_unseal := unseal_prepare; siProp_primitive.unseal.
```
The second part is easy, but the first not (tho it was worse before the bi-sbi merge), and deserves to be abstracted.https://gitlab.mpi-sws.org/iris/iris/-/issues/285Remove eta-expansions from sealed definitions2020-08-30T09:53:12ZRalf Jungjung@mpi-sws.orgRemove eta-expansions from sealed definitionsAs discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/352#note_42913), we plan to remove all eta-expansions from sealed definitions. That makes the unfolding `rewrite` more widely applicable.As discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/352#note_42913), we plan to remove all eta-expansions from sealed definitions. That makes the unfolding `rewrite` more widely applicable.https://gitlab.mpi-sws.org/iris/iris/-/issues/172String-free proofterms2020-09-08T16:20:11ZRalf Jungjung@mpi-sws.orgString-free prooftermsThe goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names. Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give...The goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names. Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give us significant speed-up. (We have a bet going here, with the threshold being 40% speedup. Let's see. ;)
@ppedrot, @janno and me recently spent some time thinking about this and I want to write this down before we forget. The basic idea is to have a version of `envs_entails`, say `envs_entails_nameless`, that takes two lists of propositions, instead of lists of pairs of strings and propositions. Now, we can `change` back and forth between `envs_entails named_env` and `envs_entails_nameless nameless_env` -- the two are convertible as we always have concrete lists for our environments. So before we apply any Coq tactic like `apply`, we always `change` the goal to its nameless form, and then `change` it back when we are done. These conversions are not actually recorded in the proof term; they only affect the type of the evar as stored in Coq, which is irrelevant at `Qed` time. Essentially, we use the type of the evar as per-goal mutable state to store the names in.
The main problem with this is that the `coq_tactics` would have to be written in nameless style, and the Ltac tactics wrapping them would have to take care of setting the right names in the subgoals they create. However, this is a problem that any solution to the issue will have -- if strings move out of the proof terms, we can't have them in Coq-level lemmas. Maybe Ltac2/Mtac could provide some other (less hacky) form of per-goal mutable state, but that wouldn't change this problem.https://gitlab.mpi-sws.org/iris/iris/-/issues/210Generic subset construction for RAs2020-09-08T20:33:39ZRalf Jungjung@mpi-sws.orgGeneric subset construction for RAsIn auth, we already implicitly use a construction that carves out a subset of an RA by restricting validity. @gparthas now needs something similar for stuff he is currently doing. We should have a general construction for this purpose.
...In auth, we already implicitly use a construction that carves out a subset of an RA by restricting validity. @gparthas now needs something similar for stuff he is currently doing. We should have a general construction for this purpose.
Related to https://gitlab.mpi-sws.org/FP/iris-coq/issues/42 (which also wants to touch `auth`).https://gitlab.mpi-sws.org/iris/iris/-/issues/339Add "reservation map" CMRA2020-09-09T12:29:51ZRalf Jungjung@mpi-sws.orgAdd "reservation map" CMRAFor the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an i...For the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?https://gitlab.mpi-sws.org/iris/iris/-/issues/66Use a "settings" file for setting options within the project2020-09-10T17:37:08ZRalf Jungjung@mpi-sws.orgUse a "settings" file for setting options within the projectFollowing a suggestion of PMP, we should add a file setting our options (Default Proof Using, Bullet Mode, ...) and import this everywhere. That makes it much easier to change such options in the future.
I think the only point left to d...Following a suggestion of PMP, we should add a file setting our options (Default Proof Using, Bullet Mode, ...) and import this everywhere. That makes it much easier to change such options in the future.
I think the only point left to discuss is the name of that file... I suggest putting it into the root, i.e. sth. like `theories/options.v`.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 throu...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/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/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 num...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/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 pro...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/186iAssert without any spatial assumptions should produce a persistent result2020-09-29T11:15:49ZRalf Jungjung@mpi-sws.orgiAssert without any spatial assumptions should produce a persistent resultThe following proof script should work:
```
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
```...The following proof script should work:
```
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
```
It currently fails because the update is not persistent -- however, this is an iAssert which is not provided any spatial assertions, so whatever it produces can always be put into the persistent context.