Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T14:12:15Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/16Document variable naming conventions2019-11-01T14:12:15ZRalf Jungjung@mpi-sws.orgDocument variable naming conventionsWe should
* [x] Convert naming.txt to markdown
* [ ] document the naming conventions for single-letter variable names
* [ ] maybe make them more consistent between Coq and LaTeX.
* [x] Document postfixes like C, T, R, G
Cc @robbertkrebbers We should
* [x] Convert naming.txt to markdown
* [ ] document the naming conventions for single-letter variable names
* [ ] maybe make them more consistent between Coq and LaTeX.
* [x] Document postfixes like C, T, R, G
Cc @robbertkrebbers https://gitlab.mpi-sws.org/iris/iris/-/issues/29Bring back Logically Atomic Triples (Coq + docs)2019-11-01T13:09:17ZJeehoon Kangjeehoon.kang@kaist.ac.krBring back Logically Atomic Triples (Coq + docs)* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendix is still in the repository (http://plv.mpi-sws.org/iris/appendix.pdf)?
- Do you have a plan to merge the appendix of POPL 2015 paper and that of ICFP 2016? It would be definitely helpful to readers like me.
---
@jung wrote
The POPL 2015 appendix has been split into two parts:
* The Iris Documentation is describing Iris in general, from the model through the base logic to the most important derived constructions. The version matching Iris 2.0 can be found on the website. It should have more derived constructions than it does, like STSs... however, we are currently in the process of redesigning how constructions like STSs describe their interface to the world, so now would be a bad time to update the documentation :/
* The details of logically atomic triples. These triples have not been ported to later versions of Iris, which is why they don't show up in the current appendix. Unfortunately, since pretty much all examples involve logically atomic triples, those are now all outdated as well. (On paper, that is.)
What, specifically, are you missing from the POPL 2015 appendix?
* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendix is still in the repository (http://plv.mpi-sws.org/iris/appendix.pdf)?
- Do you have a plan to merge the appendix of POPL 2015 paper and that of ICFP 2016? It would be definitely helpful to readers like me.
---
@jung wrote
The POPL 2015 appendix has been split into two parts:
* The Iris Documentation is describing Iris in general, from the model through the base logic to the most important derived constructions. The version matching Iris 2.0 can be found on the website. It should have more derived constructions than it does, like STSs... however, we are currently in the process of redesigning how constructions like STSs describe their interface to the world, so now would be a bad time to update the documentation :/
* The details of logically atomic triples. These triples have not been ported to later versions of Iris, which is why they don't show up in the current appendix. Unfortunately, since pretty much all examples involve logically atomic triples, those are now all outdated as well. (On paper, that is.)
What, specifically, are you missing from the POPL 2015 appendix?
https://gitlab.mpi-sws.org/iris/iris/-/issues/31iMod doesn't handle mismatched mask2020-10-02T17:23:06ZGhost UseriMod doesn't handle mismatched maskLike in
```coq
Lemma vs_demo (l: loc) (E1 E2: coPset):
((|={E1, E2}=> True) ★ l ↦ #1)%I
⊢ WP !#l @ ⊤ {{ _, True }}.
Proof.
iIntros "(HPQ & Hl)".
iVs "HPQ". (* error: not a view shift *)
```
Ideally, since load is atomic, using `iVs` here should generate two goals, the first one as a side condition saying that `E1 ⊆ ⊤`, and second one doing the view shift and send us to `E2` masked weakest pre.
cc @robbertkrebbers @jung. Hope I clarify the problem :p Like in
```coq
Lemma vs_demo (l: loc) (E1 E2: coPset):
((|={E1, E2}=> True) ★ l ↦ #1)%I
⊢ WP !#l @ ⊤ {{ _, True }}.
Proof.
iIntros "(HPQ & Hl)".
iVs "HPQ". (* error: not a view shift *)
```
Ideally, since load is atomic, using `iVs` here should generate two goals, the first one as a side condition saying that `E1 ⊆ ⊤`, and second one doing the view shift and send us to `E2` masked weakest pre.
cc @robbertkrebbers @jung. Hope I clarify the problem :p https://gitlab.mpi-sws.org/iris/iris/-/issues/78Trouble with iApply and typeclass inference order2019-11-01T13:16:44ZRalf Jungjung@mpi-sws.orgTrouble with iApply and typeclass inference orderThe following says it all:
```
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.
```The following says it all:
```
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/89Support negative selection patterns2019-11-01T13:16:44ZRalf Jungjung@mpi-sws.orgSupport negative selection patternsIt would be nice to say something like "clear everything except for ...".It would be nice to say something like "clear everything except for ...".https://gitlab.mpi-sws.org/iris/iris/-/issues/104smarter iIntros for plainly modality2019-11-01T13:16:44ZRobbert Krebberssmarter iIntros for plainly modalityThe following discussion from !71 should be addressed:
- [ ] @jung started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/71#note_20642): (+1 comment)
> Would it be a good idea or not for `iIntros` to be able to do this without us having to apply `persistently_impl_plainly`? To me, that looks very similar to how it pulls out universal quantifiers from below a box.The following discussion from !71 should be addressed:
- [ ] @jung started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/71#note_20642): (+1 comment)
> Would it be a good idea or not for `iIntros` to be able to do this without us having to apply `persistently_impl_plainly`? To me, that looks very similar to how it pulls out universal quantifiers from below a box.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/117Make some of the `wp_` tactics language independent2019-11-01T13:23:45ZRobbert KrebbersMake some of the `wp_` tactics language independentA large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.A large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.https://gitlab.mpi-sws.org/iris/iris/-/issues/123Add a general constructor from an affine BI2019-11-01T13:24:47ZRalf Jungjung@mpi-sws.orgAdd a general constructor from an affine BIIn master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just claims them to be `(ADMISSIBLE)` in a comment.
I see two ways to achieve that:
* We could provide a general way to construct a `BiMixin` from a proof of all the laws given in the appendix.
* We could do the more specific thing and first prove the appendix laws for `uPred`, and subsequently not use `unseal` when proving the `BiMixin`.In master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just claims them to be `(ADMISSIBLE)` in a comment.
I see two ways to achieve that:
* We could provide a general way to construct a `BiMixin` from a proof of all the laws given in the appendix.
* We could do the more specific thing and first prove the appendix laws for `uPred`, and subsequently not use `unseal` when proving the `BiMixin`.https://gitlab.mpi-sws.org/iris/iris/-/issues/124heap_lang: mutable n-ary locations, n-ary products, n-ary sums2019-11-01T13:25:49ZRalf Jungjung@mpi-sws.orgheap_lang: mutable n-ary locations, n-ary products, n-ary sumsThe former is interesting to model more realistic linked lists. However, we still can't realistically do CAS on sum discriminants, so if we want to restrict CAS to "small" types, we may have to rewrite some examples.The former is interesting to model more realistic linked lists. However, we still can't realistically do CAS on sum discriminants, so if we want to restrict CAS to "small" types, we may have to rewrite some examples.https://gitlab.mpi-sws.org/iris/iris/-/issues/125Make `iClear` work when there is at least one absorbing spatial hypothesis2019-11-01T13:08:25ZRobbert KrebbersMake `iClear` work when there is at least one absorbing spatial hypothesis`iClear "H"` with `H : P` currently works if either the goal is absorbing, or `P` is affine. (The same applies to `iIntros "_"`).
We could add another case: there exists at least one spatial hypothesis that is absorbing.
See also the discussion in !98 for a possible use-case.`iClear "H"` with `H : P` currently works if either the goal is absorbing, or `P` is affine. (The same applies to `iIntros "_"`).
We could add another case: there exists at least one spatial hypothesis that is absorbing.
See also the discussion in !98 for a possible use-case.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/130Make iApply "with" specialization lazier2019-11-01T13:46:23ZRobbert KrebbersMake iApply "with" specialization lazierFor example, the `[$]` specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of `swap_spec` by framing. However, this does not quite work because `wp_apply` first tries to prove the premises of the lemma by framing, and then tries to match the goal. Since framing is performed first, it instantiates evars in the wrong way. If it would first try to match the goal, and then frame, the evars would already be instantiated when framing is performed.
```coq
From iris.heap_lang Require Import proofmode notation.
Parameter swap : val.
Definition rotate_r : val := λ: "x" "y" "z",
swap "y" "z";; swap "x" "y".
Section proof.
Context `{!heapG Σ}.
Lemma swap_spec x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
Proof. Admitted.
Lemma rotate_r_spec x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_r #x #y #z
{{{ RET #(); x ↦ v3 ∗ y ↦ v1 ∗ z ↦ v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
Fail wp_apply (swap_spec with "[$]").
wp_apply (swap_spec y z with "[$]").
Admitted.
End proof.
```
It's probably easy to come up with a simpler example, but I ran into this one while preparing the Iris tutorial.
Another example:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```For example, the `[$]` specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of `swap_spec` by framing. However, this does not quite work because `wp_apply` first tries to prove the premises of the lemma by framing, and then tries to match the goal. Since framing is performed first, it instantiates evars in the wrong way. If it would first try to match the goal, and then frame, the evars would already be instantiated when framing is performed.
```coq
From iris.heap_lang Require Import proofmode notation.
Parameter swap : val.
Definition rotate_r : val := λ: "x" "y" "z",
swap "y" "z";; swap "x" "y".
Section proof.
Context `{!heapG Σ}.
Lemma swap_spec x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
Proof. Admitted.
Lemma rotate_r_spec x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_r #x #y #z
{{{ RET #(); x ↦ v3 ∗ y ↦ v1 ∗ z ↦ v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
Fail wp_apply (swap_spec with "[$]").
wp_apply (swap_spec y z with "[$]").
Admitted.
End proof.
```
It's probably easy to come up with a simpler example, but I ran into this one while preparing the Iris tutorial.
Another example:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/134Document language interface2019-11-01T13:08:15ZRobbert KrebbersDocument language interfaceIt would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own `wp_` tactics, and so on.
Considering #131, it may be good to have a separate folder with Coq related documentation, also including the current `ProofMode.md`. We could also LaTeX-ify all Coq documentation, and add it to the already existing theoretical documentation.It would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own `wp_` tactics, and so on.
Considering #131, it may be good to have a separate folder with Coq related documentation, also including the current `ProofMode.md`. We could also LaTeX-ify all Coq documentation, and add it to the already existing theoretical documentation.https://gitlab.mpi-sws.org/iris/iris/-/issues/135Use [notypeclasses refine] for all proofmode tactics2020-11-11T12:36:56ZRobbert KrebbersUse [notypeclasses refine] for all proofmode tacticsAs done ad-hoc for two tactics in 5249f4c488c0847f229b4d9e38f89145775933be to work around confusion of apply wrt canonical structures, it would be good to do this for all tactics.As done ad-hoc for two tactics in 5249f4c488c0847f229b4d9e38f89145775933be to work around confusion of apply wrt canonical structures, it would be good to do this for all tactics.https://gitlab.mpi-sws.org/iris/iris/-/issues/137Iris-internal solve_proper2019-11-01T12:51:26ZRalf Jungjung@mpi-sws.orgIris-internal solve_properWe have some cases where a variant of `solve_proper` that works *inside* the logic would be really useful:
* When using the fixed point of a monotone function (e.g., total WP).
* For showing co(ntra)variance of types in lambdaRustWe have some cases where a variant of `solve_proper` that works *inside* the logic would be really useful:
* When using the fixed point of a monotone function (e.g., total WP).
* For showing co(ntra)variance of types in lambdaRusthttps://gitlab.mpi-sws.org/iris/iris/-/issues/138wp_apply/Texan triple improvements2020-11-26T11:31:15ZRalf Jungjung@mpi-sws.orgwp_apply/Texan triple improvements* [ ] `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* [ ] `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`. This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [ ] [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* [ ] When proving a triple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.
Blocked by #130* [ ] `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* [ ] `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`. This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [ ] [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* [ ] When proving a triple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.
Blocked by #130https://gitlab.mpi-sws.org/iris/iris/-/issues/139Better names and documentation for proof mode typeclasses2020-11-23T02:33:06ZRalf Jungjung@mpi-sws.orgBetter names and documentation for proof mode typeclassesI think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs, what are the outputs, what's it supposed to do?
Don't expect people know what the `Hint Mode` sigils mean, I certainly don't. ;)
I am thinking of something like
```coq
(* Input: `P`; Outputs: `Q1`, `Q2`.
Strengthen `P` into a disjunction. Used for `iLeft`, `iRight`. *)
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
(* Input: `P`; Outputs: `Q1`, `Q2`.
Weaken `P` into a disjunction. Used for disjunction elimination patterns. *)
Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P ⊢ Q1 ∨ Q2.
```
For classes like `ElimModal` or `AddModal`, I have a hard time figuring out what they mean because they are stated in an extremely general way.I think the proof mode typeclasses should be documented better, at least the ones that are supposed to have instances added to them. Every such typeclass is essentially a "function", and should be documented as such: What are the inputs, what are the outputs, what's it supposed to do?
Don't expect people know what the `Hint Mode` sigils mean, I certainly don't. ;)
I am thinking of something like
```coq
(* Input: `P`; Outputs: `Q1`, `Q2`.
Strengthen `P` into a disjunction. Used for `iLeft`, `iRight`. *)
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
(* Input: `P`; Outputs: `Q1`, `Q2`.
Weaken `P` into a disjunction. Used for disjunction elimination patterns. *)
Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P ⊢ Q1 ∨ Q2.
```
For classes like `ElimModal` or `AddModal`, I have a hard time figuring out what they mean because they are stated in an extremely general way.https://gitlab.mpi-sws.org/iris/iris/-/issues/150Smarter iFrame: Prefer framing below `*` over framing below disjunction or wand2019-11-01T13:31:27ZRalf Jungjung@mpi-sws.orgSmarter iFrame: Prefer framing below `*` over framing below disjunction or wandWhen framing below a disjunction or a wand/implication, it can happen that `P` could have been framed elsewhere, and that would have been smarter. This is the case both for `(True \/ P) * P` and `(False -* P) * P`.
One possible way to solve this would be to have some kind of precedence for "framing positions" and not stop searching just because we found one below a disjunction/wand.When framing below a disjunction or a wand/implication, it can happen that `P` could have been framed elsewhere, and that would have been smarter. This is the case both for `(True \/ P) * P` and `(False -* P) * P`.
One possible way to solve this would be to have some kind of precedence for "framing positions" and not stop searching just because we found one below a disjunction/wand.https://gitlab.mpi-sws.org/iris/iris/-/issues/152iRewrite: Support rewriting with Coq hypotheses2019-11-01T12:51:27ZRalf Jungjung@mpi-sws.orgiRewrite: Support rewriting with Coq hypothesesiRewrite should be able to rewrite with a Coq equality embedded into Iris. Ideally, if the embedded equality is Leibniz equality, this would work even without `Proper` instances.
Cc @tslilyaiiRewrite should be able to rewrite with a Coq equality embedded into Iris. Ideally, if the embedded equality is Leibniz equality, this would work even without `Proper` instances.
Cc @tslilyaiRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/163Dealing with nested modalities in `iModIntro`2020-06-29T10:38:08ZRobbert KrebbersDealing with nested modalities in `iModIntro`We should support introducing `monPred_at P i`. Currently this presents a problem because we already have the following instance:
```coq
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 → FromModal modality_id (P i) 𝓠.
```
This instance allows introduction of e.g. updates below `monPred_at`.
When we add a `FromModal` instance for `monPred_at P i`, we end up with ambiguity when introducing `monPred_at (|==> P) i`: should `|==>` or `monPred_at` be introduced?
Concretely, we should:
- [ ] Add a `FromModal` instance for `monPred_at`
- [ ] Get the priorities of that instance and e.g. the above `from_modal_monPred_at` right
- [x] Do the same for `embed`We should support introducing `monPred_at P i`. Currently this presents a problem because we already have the following instance:
```coq
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 → FromModal modality_id (P i) 𝓠.
```
This instance allows introduction of e.g. updates below `monPred_at`.
When we add a `FromModal` instance for `monPred_at P i`, we end up with ambiguity when introducing `monPred_at (|==> P) i`: should `|==>` or `monPred_at` be introduced?
Concretely, we should:
- [ ] Add a `FromModal` instance for `monPred_at`
- [ ] Get the priorities of that instance and e.g. the above `from_modal_monPred_at` right
- [x] Do the same for `embed`https://gitlab.mpi-sws.org/iris/iris/-/issues/165Better (?) approach to control typeclass resolution based on whether some arg...2019-11-01T13:33:12ZRalf Jungjung@mpi-sws.orgBetter (?) approach to control typeclass resolution based on whether some arguments are evarsRight now, some of our typeclasses have extra variants called `KnownXXX` that use `Hint Mode` to only apply when certain arguments are not evars. This has lead to an explosion in the number of typeclasses.
Maybe a better approach would be to change the way we write some instances, and make sure they can only succeed if some arguments are not evars. I described such a solution at <https://gitlab.mpi-sws.org/FP/iris-coq/commit/a9d41b6374f44fd93629f99cfecfea3549baa0b1#note_25278>.
One possible concern is that applying such instances should fail as early as possible; if they have other premises, those shouldn't be resolved unless the evar check passes. On the other hand, the `KnownXXX` classes introduce additional coercions that typeclass resolution will try all the time, which could also be a performance issue.Right now, some of our typeclasses have extra variants called `KnownXXX` that use `Hint Mode` to only apply when certain arguments are not evars. This has lead to an explosion in the number of typeclasses.
Maybe a better approach would be to change the way we write some instances, and make sure they can only succeed if some arguments are not evars. I described such a solution at <https://gitlab.mpi-sws.org/FP/iris-coq/commit/a9d41b6374f44fd93629f99cfecfea3549baa0b1#note_25278>.
One possible concern is that applying such instances should fail as early as possible; if they have other premises, those shouldn't be resolved unless the evar check passes. On the other hand, the `KnownXXX` classes introduce additional coercions that typeclass resolution will try all the time, which could also be a performance issue.