Iris issueshttps://gitlab.mpi-sws.org/iris/iris/issues2018-06-08T11:21:50Zhttps://gitlab.mpi-sws.org/iris/iris/issues/16Document variable naming conventions2018-06-08T11:21:50ZRalf 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/21iDestruct and iPureIntro2017-09-30T18:46:44ZGhost UseriDestruct and iPureIntroI recently bumped into a scenario like this:
```
H : heapN ⊥ N
o', n' : Z
============================
"~" : heap_ctx
"~1" : inv N
(∃ o n : Z,
(l ↦ (#o, #n) ∧ ■ (o < n))
★ (auth_own γ {[o := ()]} ∨ own γ (Excl ()) ★ R))
"IH" : (locked l R -★ R -★ Φ #()) -★ WP acquire #l {{ v, Φ v }}
--------------------------------------□
"H2" : ■ (o' < n')
--------------------------------------★
■ (o' < n' + 1)
```
To prove this, I have to first `iDestruct "H2" as "%"` to move `o' < n'` to Coq context, then I can `iPureIntro` and do the following proof.
My problem is, will it be good to let `iPureIntro` (or invent something on top of it) to handle the `iDestruct` here for me?
Or even more convenient, it is possible to apply pure theorems directly in this context?
Thanks!I recently bumped into a scenario like this:
```
H : heapN ⊥ N
o', n' : Z
============================
"~" : heap_ctx
"~1" : inv N
(∃ o n : Z,
(l ↦ (#o, #n) ∧ ■ (o < n))
★ (auth_own γ {[o := ()]} ∨ own γ (Excl ()) ★ R))
"IH" : (locked l R -★ R -★ Φ #()) -★ WP acquire #l {{ v, Φ v }}
--------------------------------------□
"H2" : ■ (o' < n')
--------------------------------------★
■ (o' < n' + 1)
```
To prove this, I have to first `iDestruct "H2" as "%"` to move `o' < n'` to Coq context, then I can `iPureIntro` and do the following proof.
My problem is, will it be good to let `iPureIntro` (or invent something on top of it) to handle the `iDestruct` here for me?
Or even more convenient, it is possible to apply pure theorems directly in this context?
Thanks!https://gitlab.mpi-sws.org/iris/iris/issues/29Bring back Logically Atomic Triples (Coq + docs)2018-07-13T15:53:08ZJeehoon 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/31iVs doesn't handle mismatched mask2017-09-30T18:46:23ZGhost UseriVs 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/36STSs: Consider changing the def. of frame-steps2018-10-25T08:45:13ZRalf Jungjung@mpi-sws.orgSTSs: Consider changing the def. of frame-stepsJeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:
> $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$
> This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change `frame_step` accordingly, maybe this simplifies some things a little.Jeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:
> $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$
> This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change `frame_step` accordingly, maybe this simplifies some things a little.https://gitlab.mpi-sws.org/iris/iris/issues/58Proofmode with Coq binders, and without strings2017-09-30T18:46:23ZRalf Jungjung@mpi-sws.orgProofmode with Coq binders, and without strings@janno mentioned to me some ideas for how one could make a proofmode that uses Coq names and syntax instead of strings. Just imagine, we could have nested Coq- and Iris-level intro patterns... that would cut many proofs in lambdaRust significantly. We could also not use strings, which may even help with speed. (Well, strings are not very efficient in Coq -- but I kind of doubt that's out bottleneck currently.)
I'll leave it to Janno to explain the idea, because I would totally screw that up.
I any case, even if we want to go for this, this is a long-term thing... definitely post-3.0, and definitely breaking everybody using Iris horribly (if we don't just keep the string-based stuff around).@janno mentioned to me some ideas for how one could make a proofmode that uses Coq names and syntax instead of strings. Just imagine, we could have nested Coq- and Iris-level intro patterns... that would cut many proofs in lambdaRust significantly. We could also not use strings, which may even help with speed. (Well, strings are not very efficient in Coq -- but I kind of doubt that's out bottleneck currently.)
I'll leave it to Janno to explain the idea, because I would totally screw that up.
I any case, even if we want to go for this, this is a long-term thing... definitely post-3.0, and definitely breaking everybody using Iris horribly (if we don't just keep the string-based stuff around).https://gitlab.mpi-sws.org/iris/iris/issues/66Use a "settings" file for setting options within the project2019-04-24T12:02:33ZRalf 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 discuss is the name of that file... I suggest putting it into the root, i.e. sth. like `theories/options.v`.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/71Framing in Disjunctions2017-09-30T18:46:23ZJannoFraming in Disjunctions@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize that such an instance potentially leads to unsolvable goals more often than any of the existing framing instances. So this should probably not be the default behavior of `iFrame`. Nonetheless, the functionality was extremely convenient in some places. Often, disjunctive goals could easily be closed by framing out a bunch of resources and closing the goal with a `by` prefix or a separate `done`. No `iLeft` or `iRight` was needed.
I wonder if Iris could still benefit from such rules by adding a marker in the syntax for `iFrame`, e.g. `iFrame "!H"`, which applies the more reckless disjunction framing rules. The same could be applied for specialization patterns with something like `$!H`.
What do you think?@haidang and I used to have two Instances for Frame that would let us frame out things from only one side of a disjunction. We currently do not have that instance anymore – apparently, it got lost somehow – but we miss it. I do realize that such an instance potentially leads to unsolvable goals more often than any of the existing framing instances. So this should probably not be the default behavior of `iFrame`. Nonetheless, the functionality was extremely convenient in some places. Often, disjunctive goals could easily be closed by framing out a bunch of resources and closing the goal with a `by` prefix or a separate `done`. No `iLeft` or `iRight` was needed.
I wonder if Iris could still benefit from such rules by adding a marker in the syntax for `iFrame`, e.g. `iFrame "!H"`, which applies the more reckless disjunction framing rules. The same could be applied for specialization patterns with something like `$!H`.
What do you think?RobbertRobberthttps://gitlab.mpi-sws.org/iris/iris/issues/78Trouble with iApply and typeclass inference order2019-06-17T09:41:13ZRalf 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/88More convenient destruct of pure hypotheses2017-05-15T12:06:32ZRalf Jungjung@mpi-sws.orgMore convenient destruct of pure hypothesesIt is currently pretty annoying to destruct things into the pure (Coq) context, because the assertions cannot be named. This should be fixed.
One somewhat hack-ish option would be to do this the ssreflect style. So `iDestruct ... as "[% %]"` would put two things onto the goal stack, and one would follow this tactic by `=>H1 H2` to give them names. This is somewhat non-local, but OTOH it lets us use the full power of ssreflect intro patterns.
Another option would be to somehow solve the "cannot convert string to ident"-problem, and then support patterns of the form `%H`. This will require a plugin to work in Coq 8.6, which makes it really hard to support Windows (as far as I can tell). Also, I suppose currently `%H` is parsed just like `% H`? So there would be a backwards compatibility problem when `%` starts to behave like `#` (i.e., being a modifier on the following name). We could mitigate that by detecting uses of `%H` right now and warning about them (or erroring immediately?).It is currently pretty annoying to destruct things into the pure (Coq) context, because the assertions cannot be named. This should be fixed.
One somewhat hack-ish option would be to do this the ssreflect style. So `iDestruct ... as "[% %]"` would put two things onto the goal stack, and one would follow this tactic by `=>H1 H2` to give them names. This is somewhat non-local, but OTOH it lets us use the full power of ssreflect intro patterns.
Another option would be to somehow solve the "cannot convert string to ident"-problem, and then support patterns of the form `%H`. This will require a plugin to work in Coq 8.6, which makes it really hard to support Windows (as far as I can tell). Also, I suppose currently `%H` is parsed just like `% H`? So there would be a backwards compatibility problem when `%` starts to behave like `#` (i.e., being a modifier on the following name). We could mitigate that by detecting uses of `%H` right now and warning about them (or erroring immediately?).https://gitlab.mpi-sws.org/iris/iris/issues/89Support negative selection patterns2017-05-17T12:53:36ZRalf 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 iIntros2017-10-27T08:59:33ZRobbertsmarter iIntrosThe 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.RobbertRobberthttps://gitlab.mpi-sws.org/iris/iris/issues/117Make some of the `wp_` tactics language independent2017-11-30T10:21:32ZRobbertMake 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 BI2018-05-23T13:44:08ZRalf 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 sums2018-09-18T20:35:00ZRalf 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 hypothesis2018-07-13T08:51:11ZRobbertMake `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.RobbertRobberthttps://gitlab.mpi-sws.org/iris/iris/issues/130Make `[$]` lazier2018-04-26T21:59:58ZRobbertMake `[$]` lazierThe `[$]` 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.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.RobbertRobberthttps://gitlab.mpi-sws.org/iris/iris/issues/132Formalize example that impredicative invariants and linearity are incompatible2018-07-13T08:51:11ZRobbertFormalize example that impredicative invariants and linearity are incompatibleRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/issues/134Document language interface2018-02-12T09:09:00ZRobbertDocument 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 tactics2019-06-17T09:33:28ZRobbertUse [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.