Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-10-01T19:57:53Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/257Auth as Views2020-10-01T19:57:53ZRalf Jungjung@mpi-sws.orgAuth as ViewsGregory [suggested](https://lists.mpi-sws.org/pipermail/iris-club/2019-July/000198.html) a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user ...Gregory [suggested](https://lists.mpi-sws.org/pipermail/iris-club/2019-July/000198.html) a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user pick some relation between them. I think it can truly be any (Coq-level) relation for discrete types; for the CMRA variant we likely need a step-indexed relation. The existing "auth" is then the special case of using the same type, and equality as the relation.
This subsumes https://gitlab.mpi-sws.org/iris/iris/merge_requests/91 by making the relation also require bijectivity. And this also could be useful for situations where we have a very right CMRA for the fragments, which often means lots of "junk" data (such as `to_agree`, of `ExclBot`). So instead of the pattern where we do `exists heap, own (● to_auth heap)`, we could have this `to_auth` in the relation.
An open question is what would happen with all our theory about local updates.
Things to do:
* [ ] Implement a generalized "auth as view" library
* [ ] Implement monotone partial bijections (https://gitlab.mpi-sws.org/iris/iris/merge_requests/91) in terms of that.https://gitlab.mpi-sws.org/iris/iris/-/issues/256Consisent direction for `CMRA_NAME_op` lemmas.2019-08-13T16:01:57ZDan FruminConsisent direction for `CMRA_NAME_op` lemmas.I've noticed something which can be seen as a discrepancy in the lemmas.
These ones follow the pattern "constructor of the multiplication is equal to the multiplication of constructors".
```
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ ...I've noticed something which can be seen as a discrepancy in the lemmas.
These ones follow the pattern "constructor of the multiplication is equal to the multiplication of constructors".
```
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
```
These ones go the other way around: "multiplication of constructors is equal to the constructor of multiplications":
```
Lemma Cinl_op a a' : Cinl a ⋅ Cinl a' = Cinl (a ⋅ a').
Lemma Cinr_op b b' : Cinr b ⋅ Cinr b' = Cinr (b ⋅ b').
Lemma pair_op (a a' : A) (b b' : B) : (a, b) ⋅ (a', b') = (a ⋅ a', b ⋅ b').
```
Should this be changed or am I nitpicking and the (breaking) change will be too invasive?https://gitlab.mpi-sws.org/iris/iris/-/issues/255Failure to find a proof of persistence2020-03-18T20:54:41ZDmitry KhalanskiyFailure to find a proof of persistenceVersion of Iris: dev.2019-07-01.1.6e79f000
Typeclass search fails when trying to prove that a particular statement is persistent.
In resource algebra
```
authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optio...Version of Iris: dev.2019-07-01.1.6e79f000
Typeclass search fails when trying to prove that a particular statement is persistent.
In resource algebra
```
authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optionUR (exclR unitO)))
(optionUR (agreeR (boolO))))
```
proof of
```
Persistent (own γ (◯((None, None), Some (to_agree true))))
```
fails with
```
Proof search failed without reaching its limit.
```
if performed with `typeclasses eauto 10`. It similarly doesn't work with `apply _`.
The statement is actually persistent, as shown by Jonas Kastberg:
```
Proof.
apply own_core_persistent.
apply auth_frag_core_id.
apply pair_core_id; typeclasses eauto.
Qed.
```
Minimal (non-)working example: https://pastebin.com/T7zhm9Zuhttps://gitlab.mpi-sws.org/iris/iris/-/issues/254Reliance on `Export` bug2019-11-01T12:48:48ZMaxime DénèsReliance on `Export` bugDear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is...Dear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is an easy way to observe the problem on Coq master: take `algebra.ufrac_auth`, and change the first line:
```coq
From iris.algebra Require Export auth frac.
```
into:
```coq
From iris.algebra Require Export auth.
From iris.algebra Require Export frac.
```
it will make the proof of `ufrac_auth_agreeN` fail because a view starts applying in the wrong direction...
Could you provide some guidance on how to make the file pass with the two separate `Export`s? It will probably make it compatible with the fix of the bug I mentioned above.
Thanks!https://gitlab.mpi-sws.org/iris/iris/-/issues/253Constructing CMRAs by giving isomorphism to CMRAs2020-11-06T14:41:47ZPaolo G. GiarrussoConstructing CMRAs by giving isomorphism to CMRAsIris has such a construction for OFEs, and @jung asked for one on CMRAs on chat (https://mattermost.mpi-sws.org/iris/pl/h9q6eeu3ojnxfcwr1w59z76jcr).Iris has such a construction for OFEs, and @jung asked for one on CMRAs on chat (https://mattermost.mpi-sws.org/iris/pl/h9q6eeu3ojnxfcwr1w59z76jcr).https://gitlab.mpi-sws.org/iris/iris/-/issues/250equivI lemma for sigT2019-06-25T10:41:37ZPaolo G. GiarrussoequivI lemma for sigTTo use the new `sigT` construction, it helps to have an `equivI` lemma such as:
```coq
Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
x ≡ y ⊣⊢
∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y : iProp Σ.
...To use the new `sigT` construction, it helps to have an `equivI` lemma such as:
```coq
Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
x ≡ y ⊣⊢
∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y : iProp Σ.
Proof. by unseal. Qed.
```
@robbertkrebbers asks: should we have this just for iProp, or for any `sbi`?https://gitlab.mpi-sws.org/iris/iris/-/issues/249Better solvers for properness/contractiveness2020-02-13T22:39:23ZPaolo G. GiarrussoBetter solvers for properness/contractivenesssolve_proper doesn't deal well with higher-order functions. Here's my home-grown variant:
```coq
(** An ad-hoc variant of solve_proper that seems to work better when defining
proper higher-order functions. In particular, using int...solve_proper doesn't deal well with higher-order functions. Here's my home-grown variant:
```coq
(** An ad-hoc variant of solve_proper that seems to work better when defining
proper higher-order functions. In particular, using intro allows showing that a
lambda abstraction is proper if its body is proper.
Its implementation can also prove [f1 x ≡ f2 x] from [H : f1 ≡ f2]:
neither f_equiv nor rewrite deal with that, but [apply H] does. *)
Ltac solve_proper_ho_core tac :=
solve [repeat (tac (); cbn); cbn in *;
repeat match goal with H : _ ≡{_}≡ _|- _ => apply H end].
Ltac solve_proper_ho := solve_proper_ho_core
ltac:(fun _ => f_equiv || intro).
Ltac solve_contractive_ho := solve_proper_ho_core
ltac:(fun _ => f_contractive || f_equiv || intro).
```
Should we have something like this in Iris/stdpp? There's some heuristic tuning involved, but I use this rather happily...https://gitlab.mpi-sws.org/iris/iris/-/issues/248Comparison with `=` and with CAS is not the same2019-07-01T14:46:59ZRalf Jungjung@mpi-sws.orgComparison with `=` and with CAS is not the sameCurrently, `heap_lang` allows more things to be compared with `=` than with `CAS`: for the latter, one of the two values-to-be-compared has to be "unboxed", meaning that it is a literal or inl/inr of a literal. If this condition is not m...Currently, `heap_lang` allows more things to be compared with `=` than with `CAS`: for the latter, one of the two values-to-be-compared has to be "unboxed", meaning that it is a literal or inl/inr of a literal. If this condition is not met, the program is stuck.
@robbertkrebbers proposes that we should restrict `=` in a similar way. On the other hand, it is nice that `=` is a total operation currently.https://gitlab.mpi-sws.org/iris/iris/-/issues/247iInv does not behave as intended when the goal is an accessor2019-11-01T12:32:42ZRalf Jungjung@mpi-sws.orgiInv does not behave as intended when the goal is an accessorWhen the goal is of the form
```
|={⊤,∅}=> ∃ ..., P ∗ (Q ={∅,⊤}=∗ Φ )
```
I would hope `iInv N` where the invariant assertion is `I` to turn it into something like
```
|={N,∅}=> ∃ ..., P ∗ (I * Q ={∅,⊤}=∗ Φ )
```
but currently we have no...When the goal is of the form
```
|={⊤,∅}=> ∃ ..., P ∗ (Q ={∅,⊤}=∗ Φ )
```
I would hope `iInv N` where the invariant assertion is `I` to turn it into something like
```
|={N,∅}=> ∃ ..., P ∗ (I * Q ={∅,⊤}=∗ Φ )
```
but currently we have no good way to even detect the goal as an accessor, so none of this can happen.https://gitlab.mpi-sws.org/iris/iris/-/issues/246iEval (eauto) "corrupts" goal2019-06-15T11:43:47ZPaolo G. GiarrussoiEval (eauto) "corrupts" goalWhile I ran into !269, I also ended up learning that `iEval (eauto)` can "corrupt" the goal by calling `iStartProof` again:
```
1 subgoal
Σ : gFunctors
H : heapG Σ
c1, c2 : val
A1, A2, B1, B2 : lty Σ
v1, v2 : val
w2, w1 : ...While I ran into !269, I also ended up learning that `iEval (eauto)` can "corrupt" the goal by calling `iStartProof` again:
```
1 subgoal
Σ : gFunctors
H : heapG Σ
c1, c2 : val
A1, A2, B1, B2 : lty Σ
v1, v2 : val
w2, w1 : language.val heap_lang
============================
"HwB2" : B2 w2
"HwB1" : B1 w1
--------------------------------------∗
⌜--------------------------------------∗
(B1 * B2)%lty (w1, w2)%V
⌝
```
(from https://gitlab.mpi-sws.org/Blaisorblade/examples/commit/e9851f6#16adf89a84c96614a153a2ca8db8a92215d85db3_244_297).
Minimized version:
```
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
Lemma foo {Σ}: True ⊢ True : iProp Σ.
Proof.
iIntros.
iEval (info_eauto).
Show.
(*Equal to: *)
(* iEval (iStartProof; iPureIntro). *)
```
gives:
```
1 subgoal
Σ : gFunctors
a : True
============================
--------------------------------------∗
⌜?P⌝
```https://gitlab.mpi-sws.org/iris/iris/-/issues/245Add IntoAnd instance (and more) for array2019-08-13T11:19:53ZRodolphe LepigreAdd IntoAnd instance (and more) for arrayWe should add `IntoAnd` instances (and friends) for `array`.
This has been discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/267#note_37037).We should add `IntoAnd` instances (and friends) for `array`.
This has been discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/267#note_37037).Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/242Planning the Iris 3.2 release2019-11-01T12:31:44ZRalf Jungjung@mpi-sws.orgPlanning the Iris 3.2 releaseI have finally gotten around to update the documentation for the Iris 3.2 changes. Turns out that wasn't actually that much work as heap_lang is not part of the formal documentation.
That removes the last blocker for a new release! So I...I have finally gotten around to update the documentation for the Iris 3.2 changes. Turns out that wasn't actually that much work as heap_lang is not part of the formal documentation.
That removes the last blocker for a new release! So I think we should make that release soon-ish. Are there any issues or MRs that you think should be included? Let's collect them in [this milestone](https://gitlab.mpi-sws.org/iris/iris/milestones/4).
We might consider doing the release after the POPL deadline so that our Iris-using POPL submissions (if any) can claim to be compatible with Iris 3.2. But honestly I don't think that is a big factor, the artifacts should anyway bundle the right version of Iris -- and I'd rather avoid extra coordination overhead if possible.
After the release:
* [ ] Drop support for Coq 8.7, and enable the `sigT`-functor notation (at the bottom of `ofe.v`).Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/240We have ambiguous coercion paths2020-04-02T09:08:16ZRalf Jungjung@mpi-sws.orgWe have ambiguous coercion pathsWhen compiling with Coq master, we see lots of these:
```
[constRF; rFunctor_diag] : cmraT >-> Funclass
[ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass
```
Also see e.g. [this build log](https://gitlab.mpi-sws.org/iris/iris/-...When compiling with Coq master, we see lots of these:
```
[constRF; rFunctor_diag] : cmraT >-> Funclass
[ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass
```
Also see e.g. [this build log](https://gitlab.mpi-sws.org/iris/iris/-/jobs/31380).
Is this a problem? Can we do anything about it?https://gitlab.mpi-sws.org/iris/iris/-/issues/239Iris logo2021-02-05T12:43:21ZRobbert KrebbersIris logoWe need a logo for the project. The issue collects proposals so far:
By @janno:
![Janno](https://robbertkrebbers.nl/iris_logos/janno.jpg)
By @lgg:
![Janno](https://robbertkrebbers.nl/iris_logos/leon.jpg)
As @dreyer said: I think if ...We need a logo for the project. The issue collects proposals so far:
By @janno:
![Janno](https://robbertkrebbers.nl/iris_logos/janno.jpg)
By @lgg:
![Janno](https://robbertkrebbers.nl/iris_logos/leon.jpg)
As @dreyer said: I think if we all start singing I-R-I-S to the tune of YMCA, we'll really be getting somewherehttps://gitlab.mpi-sws.org/iris/iris/-/issues/238Wish: iSimpl on multiple hypothesis2019-05-22T22:53:15ZDan FruminWish: iSimpl on multiple hypothesis**A wish**: it would be nice if we could run `iSimpl` on several hypothesis: `iSimpl in "H1 H2"`.**A wish**: it would be nice if we could run `iSimpl` on several hypothesis: `iSimpl in "H1 H2"`.https://gitlab.mpi-sws.org/iris/iris/-/issues/237Stripping laterN from pure propositions when proving laterN *without except-0*2019-11-01T11:09:51ZPaolo G. GiarrussoStripping laterN from pure propositions when proving laterN *without except-0*I just proved that, for uniform predicates, when proving `▷^i Q`, you can strip `▷^i` from `"Hfoo": ▷^i ⌜ P ⌝`, for arbitrary uniform predicates. Statements:
`(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.`
`(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).`
I ...I just proved that, for uniform predicates, when proving `▷^i Q`, you can strip `▷^i` from `"Hfoo": ▷^i ⌜ P ⌝`, for arbitrary uniform predicates. Statements:
`(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.`
`(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).`
I needed this in my proof; could we add support for this in Iris? I'm not sending a MR because the code is far from ready for that.
Was this already possible? I didn't find how, and thought this would need some new variant of except-0 (an except-i modality).
- IPM suggested that wouldn't work — `iDestruct "Hfoo" as "%"` complains that `Hfoo` is not pure, even when the conclusion starts with `▷^i`.
- The proof is by case distinction on the world: in worlds `n < i`, the conclusion is trivial, while in worlds `n >= i`, we have that `▷^i ⌜ P ⌝ → P`. This must be done in the model.
My proof is easy for later, but laterN was trickier; I'm also not sure where this proof would go (since laterN is a derived connective, but the proof for laterN goes in the model).
I expect one could lift this lemma to wand as well (since `▷^i ⌜ P ⌝` is persistent, this shouldn't need going to the model).
- These lemmas are also a bit inconvenient to use; it's not clear that `IntoPure` supports such conditional tactics. A typical example, for hypothesis "Hlclw": ▷^i ⌜ nclosed_vl w 0 ⌝, is:
```
iApply (strip_pure_laterN i with "[] Hlclw").
iIntros (Hclw).
```
`iRevert "Hlclw"; iApply strip_pure_wand_laterN; iIntros (Hclw)` might also work, given a version for wand.
My proof script is:
```coq
From iris.base_logic Require Import base_logic lib.iprop.
Import uPred.
Section uPred_later_extra.
Context `{M: ucmraT}.
Implicit Types (Q: uPred M) (x: M).
Lemma laterN_pure_id i n P x: i <= n →
(▷^i uPred_pure_def P)%I n x → P.
Proof.
move => Hle H; induction i => //=.
apply IHi; first lia.
elim: i n Hle H {IHi} => [|i IHi] [|n] Hle;
unseal => // H; first lia.
apply IHi; first lia. by unseal.
Qed.
Lemma laterN_trivial i n Q x: i > n →
(▷^i Q)%I n x.
Proof.
move: i => [|i] Hle. by lia.
apply uPred_mono with i x; eauto with lia.
elim: i {Hle}; by unseal.
Qed.
Lemma strip_pure_later P Q:
(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).
Proof.
unseal; constructor => n x Hvx Hyp [|n'] // ?????.
by apply Hyp.
Qed.
Lemma strip_pure_laterN i P Q:
(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.
Proof.
unseal; constructor => n x Hvx Hyp n' //= x' ?? Hvx' H.
destruct (decide (i <= n')) as [Hle|Hge].
- by eapply Hyp, laterN_pure_id.
- by apply laterN_trivial; lia.
Qed.
End uPred_later_extra.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/236Non-expansiveness for big ops2020-03-19T11:07:23ZDan FruminNon-expansiveness for big opsA wish:
non-expansiveness for the big_op operations, e.g.
```
[∗ map] k ↦ x ∈ m, Φ k x
```
is non-expansive in `m`, if `m` is a gmap into an OFEA wish:
non-expansiveness for the big_op operations, e.g.
```
[∗ map] k ↦ x ∈ m, Φ k x
```
is non-expansive in `m`, if `m` is a gmap into an OFEhttps://gitlab.mpi-sws.org/iris/iris/-/issues/234Syntactic type system for heap_lang2020-10-01T11:28:21ZRobbert KrebbersSyntactic type system for heap_lang@dfrumin defined a syntactic type system for heap_lang in the reloc repo:
https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v
I would like to use his type system to state the fundamental theorem for the unary lo...@dfrumin defined a syntactic type system for heap_lang in the reloc repo:
https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v
I would like to use his type system to state the fundamental theorem for the unary logical relation of heap_lang in iris-examples (https://gitlab.mpi-sws.org/iris/examples/tree/master/theories/logrel_heaplang), as right now that formalization only has semantic types and the semantic typing rules.
How about adding @dfrumin's syntactic type system to the heap_lang folder of the Iris repo?
Some things to discuss:
- [ ] It currently relies on autosubst. Using strings for binding in types will be horrible, since there we actually have to deal with capture. Do we mind having a dependency of Iris on Autosubst, or would it be better to write a manual version with De Bruijn indexes?
- [ ] It uses some fun encodings for pack and unpack (of existential types) and type abstraction and application, see https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v#L80 Are we happy with that, or are there more elegant ways of doing that?https://gitlab.mpi-sws.org/iris/iris/-/issues/232Investigate slowdown caused by gset change2019-04-24T08:26:43ZRalf Jungjung@mpi-sws.orgInvestigate slowdown caused by gset change[This std++ diff](https://gitlab.mpi-sws.org/iris/stdpp/compare/b938e033...e2eb2948) caused an [80% slowdown in `algebra/gset.v`](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552558727491&to=1552560733442&var-metric=...[This std++ diff](https://gitlab.mpi-sws.org/iris/stdpp/compare/b938e033...e2eb2948) caused an [80% slowdown in `algebra/gset.v`](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552558727491&to=1552560733442&var-metric=instructions&var-project=iris&var-branch=master&var-config=coq-8.9.0&var-group=(.*)). We should find a way to fix that regression, or at least understand what causes it.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/231Allow swapping later^i and forall, later, etc.2019-11-01T11:12:12ZPaolo G. GiarrussoAllow swapping later^i and forall, later, etc.For swapping later^i and forall, an instance suffices: https://gist.github.com/Blaisorblade/3f9e41b7f044617fd5789b0d3554a2d7 (I suppose this isn't good enough for a PR).
For swapping later^i and later, I'm not sure what's the typeclass, ...For swapping later^i and forall, an instance suffices: https://gist.github.com/Blaisorblade/3f9e41b7f044617fd5789b0d3554a2d7 (I suppose this isn't good enough for a PR).
For swapping later^i and later, I'm not sure what's the typeclass, but it should be possible — I do the swaps through complicated proofs, applied inline.
Generally, I suspect all the instances for later could be lifted (by induction) to later^i, and I suspect I'd be willing to do that work (once I move).