Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-08-02T16:52:12Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/417Revert !118: Use ∃ instead of SIgma for extension axiom2022-08-02T16:52:12ZRobbert KrebbersRevert !118: Use ∃ instead of SIgma for extension axiomI am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet ...I am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet { multiset_car : list A }.
```
And define `dist` and `(≡)` to be modulo permutations. For permutations I use https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.SetoidPermutation.html
Unfortunately, this does not work: the extension axiom of cameras does not seem provable.
```coq
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
```
The problem is that I need to construct `z1` and `z2` as a sigma type, not an ordinary exist. But the type of permutations is a `Prop`, so I cannot do this.
Here's the whole code I have so far:
```coq
From Coq Require Import SetoidPermutation.
From iris.algebra Require Export cmra.
Lemma PermutationA_mono {A} (R1 R2 : relation A) xs1 xs2 :
(∀ x1 x2, R1 x1 x2 → R2 x1 x2) →
PermutationA R1 xs1 xs2 → PermutationA R2 xs1 xs2.
Proof. induction 2; econstructor; by eauto. Qed.
Record multiset A := MultiSet { multiset_car : list A }.
Arguments MultiSet {_} _.
Arguments multiset_car {_} _.
Section multiset.
Context {A : ofe}.
Implicit Types x y : A.
Implicit Types X Y : multiset A.
Local Instance multiset_equiv_instance : Equiv (multiset A) := λ X1 X2,
∀ n, PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_dist_instance : Dist (multiset A) := λ n X1 X2,
PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_valid_instance : Valid (multiset A) := λ _, True.
Local Instance multiset_validN_instance : ValidN (multiset A) := λ _ _, True.
Local Instance multiset_unit_instance : Unit (multiset A) := MultiSet [].
Local Instance multiset_op_instance : Op (multiset A) := λ X1 X2,
MultiSet (multiset_car X1 ++ multiset_car X2).
Local Instance multiset_pcore_instance : PCore (multiset A) := λ X, Some ε.
Global Instance multiset_singleton : Singleton A (multiset A) := λ x,
MultiSet [x].
Lemma multiset_ofe_mixin : OfeMixin (multiset A).
Proof.
split; rewrite /equiv /dist /multiset_equiv_instance /multiset_dist_instance /=.
- done.
- intros n. split.
+ by intros X.
+ intros X1 X2 ?. done.
+ intros X1 X2 X3 ??. by etrans.
- intros n X1 X2. apply PermutationA_mono, dist_S.
Qed.
Canonical Structure multisetO := Ofe (multiset A) multiset_ofe_mixin.
Global Instance multiset_ofe_discrete : OfeDiscrete A → OfeDiscrete multisetO.
Proof.
intros HA [xs1] [xs2] Hxs n. revert Hxs. apply PermutationA_mono.
by intros x1 x2 ->%(discrete _).
Qed.
Lemma multiset_cmra_mixin : CmraMixin (multiset A).
Proof.
apply cmra_total_mixin; try by eauto.
- intros X n Y1 Y2 HY. by apply (PermutationA_app _).
- by intros n X1 X2.
- intros X1 X2 X3. admit. (* boring case *)
- intros X1 X2 n. apply (PermutationA_app_comm _).
- by intros X n.
- intros X1 X2 _. exists ε. by intros n.
- intros n [xs] [ys1] [ys2] _. rewrite /equiv /dist /op
/multiset_equiv_instance /multiset_dist_instance /multiset_op_instance /=.
(* Stuck here. The witness [PermutationA (dist n) xs (ys1 ++ ys2)] basically
says how the elements in [xs] are distributed over [ys1] and [ys2].
Intuitively, it says element 0 of [xs] goes to position [i0] in
[ys1 ++ ys2], element 1 of [xs] goes to position [i1] in ys1 ++ ys2 and so
on. *)
(* I would like to use the lemma [PermutationA_decompose], but that does
not work since it gives an [∃]. *)
(* I tried to prove it by induction on the list instead, but that seems
pointless. At some point I need to invert on the [PermutationA] witness,
which is not possible. *)
induction ys1 as [|y1 ys1 IH]; intros Hxs; simpl in *.
{ by exists (MultiSet []), (MultiSet xs). }
admit.
Admitted.
Canonical Structure multisetR := Cmra (multiset A) multiset_cmra_mixin.
Lemma multiset_ucmra_mixin : UcmraMixin (multiset A).
Proof. split; [done | | done]. by intros X n. Qed.
Canonical Structure multisetUR := Ucmra (multiset A) multiset_ucmra_mixin.
Global Instance multiset_cancelable X : Cancelable X.
Proof. Admitted.
Global Instance multiset_singleton_ne : NonExpansive (singleton (B:=multiset A)).
Proof. intros n x1 x2. by repeat constructor. Qed.
Global Instance multiset_singleton_proper :
Proper ((≡) ==> (≡)) (singleton (B:=multiset A)).
Proof. apply (ne_proper _). Qed.
Global Instance multiset_singleton_dist_inj n :
Inj (dist n) (dist n) (singleton (B:=multiset A)).
Proof. intros x1 x2. Admitted.
Global Instance multiset_singleton_inj :
Inj (≡) (≡) (singleton (B:=multiset A)).
Proof.
intros x1 x2 Hx. apply equiv_dist=> n. apply (inj singleton). by rewrite Hx.
Qed.
End multiset.
Global Arguments multisetO : clear implicits.
Global Arguments multisetR : clear implicits.
Global Arguments multisetUR : clear implicits.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/416big_sep lemmas fail to apply when goal is not eta-expanded2021-05-26T11:31:56ZRalf Jungjung@mpi-sws.orgbig_sep lemmas fail to apply when goal is not eta-expandedI just ran into a strange problem:
```coq
Lemma test {A B} (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) :
⊢ big_sepL2 Φ l1 l2.
Proof.
Fail iApply big_sepL2_delete.
(* The command has indeed failed with message:
Tactic failu...I just ran into a strange problem:
```coq
Lemma test {A B} (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) :
⊢ big_sepL2 Φ l1 l2.
Proof.
Fail iApply big_sepL2_delete.
(* The command has indeed failed with message:
Tactic failure: iApply: cannot apply
(([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, ?Goal k y1 y2)
∗-∗ ?Goal ?Goal2 ?Goal3 ?Goal4
∗ ([∗ list] k↦y1;y2 ∈ ?Goal0;?Goal1, if decide (k = ?Goal2) then emp else ?Goal k y1 y2))%I. *)
iApply (big_sepL2_delete Φ).
(* This works. *)
```
For some reason Coq needs to be manually given `Φ` here. That should not be the case.
The only difference between the lemma statement and the goal is an eta-expansion of `Φ`.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-conditio...@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 everywhere2023-03-18T18:30:39ZRalf 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:
* [x] `algebra.lib.gmap_view`
* [x] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more ...`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [x] `algebra.lib.gmap_view`
* [x] `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 w...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/410Modality for `Timeless`2021-04-19T07:51:21ZRalf Jungjung@mpi-sws.orgModality for `Timeless`We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ ...We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/407Tracking issue for list RA2021-03-17T11:50:01ZRalf Jungjung@mpi-sws.orgTracking issue for list RAThis is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper....This is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.https://gitlab.mpi-sws.org/iris/iris/-/issues/406Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs2021-03-18T08:26:06ZArmaël GuéneauSlow typechecking / nonterminating Qed when using auxiliary definitions in RAs```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Defin...```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Definition memspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition regspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition memreg_specUR := prodUR regspecUR memspecUR.
Definition exprUR : cmraT := (exclR (leibnizO nat)).
Definition cfgUR : ucmraT := prodUR (optionUR exprUR) memreg_specUR.
Class cfgSG Σ := CFGSG {
cfg_invG :> inG Σ (authR cfgUR);
cfg_name : gname }.
Section S.
Context `{cfgSG Σ}.
Lemma spec_heap_valid (e:option (excl (leibnizO nat))) a q w
(rm: gmapUR nat (prodR fracR (agreeR (leibnizO nat))))
(mm: gmapUR nat (prodR fracR (agreeR (leibnizO nat)))) :
False →
own cfg_name (● (e,(rm,mm))) ∗
own cfg_name (◯ (ε, (∅,{[ a := (q, to_agree w) ]})))
-∗ False.
Proof. intro.
iIntros "(Hown & Ha)".
iDestruct (own_valid_2 with "Hown Ha") as "HH". exfalso. assumption.
Qed.
End S.
```
The snippet above:
- works fine with Iris 3.3
- takes a very long time at Qed with Iris 3.4 (modulo replacing `cmraT` with `cmra` in the script)
The issue seems to be with the use of auxiliary definitions to define the resource algebra `cfgUR`. Manually inlining `cfgUR` and the other auxiliary definitions in the definition of `cfgSG` makes it work again with Iris 3.4.
Since the fix is relatively simple, this issue doesn't seem to be too big of a deal, but I thought that I'd report it just in case.
Coq version used: 8.12.1 in both cases.https://gitlab.mpi-sws.org/iris/iris/-/issues/405Tracking issue for HeapLang interpreter2021-02-16T11:03:04ZRalf Jungjung@mpi-sws.orgTracking issue for HeapLang interpreterThis is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
...This is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Generalize the monad and move it to std++, and generalize the tactics for the monad.
* Find some way to avoid the `pretty_string` instance, or move it to std++.https://gitlab.mpi-sws.org/iris/iris/-/issues/402iFrame performance issues2022-05-06T12:56:32ZRalf 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 ...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/434 for diverging iFrame because Hint Mode is accidentally being circumvented.https://gitlab.mpi-sws.org/iris/iris/-/issues/400Integrate Tej's simp-lang?2021-02-17T08:49:46ZRalf Jungjung@mpi-sws.orgIntegrate Tej's simp-lang?@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an [accompanying Youtube video](https://www.youtube.com/watch?v=HndwyM04...@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an [accompanying Youtube video](https://www.youtube.com/watch?v=HndwyM04KEU&feature=youtu.be)! I took a look and watched the video, and I really like it.
I propose we give this more visibility by referencing it from the Iris repo and website, and also we should find some way to ensure that the Coq code remains compatible with latest Iris. The easiest way to do that would be to add an "iris_simp_lang" package in this repository and move the code there. The README could go into the subfolder. @tchajed would that work for you, or did you have other plans? I don't want to appropriate your work, just ensure that it does not bitrot. I could imagine declaring you the maintainer of that subdirectory, so you could e.g. merge MRs for it yourself. @robbertkrebbers what do you think?
I also have some more specific low-level comments, which I leave here just so I do not forget -- but it probably make more sense to discuss the high-level points first. It's really just one remark so far:
* In `heap_ra`, I find it confusing that you end up basically copying (parts of) `gen_heap`. IMO it would make more sense to either use `gen_heap`, or else (for the purpose of exposition) to define something that specifically works for values and locations of this language, but then it should not be called "gen(eral)".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...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/397`iRename` fails with bad error message when not in proof mode2021-02-17T08:48:22ZRobbert Krebbers`iRename` fails with bad error message when not in proof mode```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
wit...```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
with "True".
```
The tactic probably does not call `iStartProof` at the beginning.https://gitlab.mpi-sws.org/iris/iris/-/issues/396Intro pattern `>` has wrong behavior with side-conditions of `iMod`2021-04-29T09:25:46ZRobbert KrebbersIntro pattern `>` has wrong behavior with side-conditions of `iMod````coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> ...```coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
Proof.
iIntros ">H".
```
fails with
```
In environment
Σ : gFunctors
heapG0 : heapG Σ
E1, E2 : coPset
P : iProp Σ
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11809)
(environments.env_spatial ?M11809) ?M11814"
with
"∀ (σ : language.state heap_lang) (e' : language.expr heap_lang) (κ :
list
(language.observation
heap_lang))
(σ' : language.state heap_lang) (efs : list (language.expr heap_lang)),
language.prim_step (#() #()) σ κ e' σ' efs
→ match stuckness_to_atomicity NotStuck with
| StronglyAtomic => is_Some (language.to_val e')
| WeaklyAtomic => irreducible e' σ'
end".
```
See also https://mattermost.mpi-sws.org/iris/pl/r47q3gcq4fddxnhpddj91yb1wyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/394Document relation between Discrete and Timeless (in appendix?)2021-01-06T13:08:34ZPaolo G. GiarrussoDocument relation between Discrete and Timeless (in appendix?)See discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/607#note_61127 by @robbertkrebbers:
> I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not s...See discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/607#note_61127 by @robbertkrebbers:
> I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not so useful; Timeless P → Discrete P does not hold; discrete propositions are unlikely to exist.
> It might be worth documenting this somewhere, but I don't know what's the best place. Maybe the appendix?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://gi...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 l...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/389Citation guide2020-12-08T17:17:32ZTej Chajedtchajed@gmail.comCitation guideThe docs should have a page explaining what a paper using Iris should cite, between the several Iris papers, the journal paper, and the two IPM papers.The docs should have a page explaining what a paper using Iris should cite, between the several Iris papers, the journal paper, and the two IPM papers.https://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-e...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.