Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-07-13T15:56:18Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/48Unify `iNext` and `iModIntro` (and more?)2018-07-13T15:56:18ZRobbert KrebbersUnify `iNext` and `iModIntro` (and more?)These tactics are very similar. I would be nice to generalize `iModIntro` to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized `iNext` to deal with the iterated later modality, I t...These tactics are very similar. I would be nice to generalize `iModIntro` to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized `iNext` to deal with the iterated later modality, I think this should not be too difficult.
See also the discussion as part of commit 9ae19ed5.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/94iInv without Hclose2018-07-13T15:55:27ZRalf Jungjung@mpi-sws.orgiInv without HcloseI've been talking about accessors today with @janno and @pythonsq. One place where having "actual" accessors might be useful is to avoid "Hclose"-style assumptions. I think we can prototype how that would look like by playing with iInv...I've been talking about accessors today with @janno and @pythonsq. One place where having "actual" accessors might be useful is to avoid "Hclose"-style assumptions. I think we can prototype how that would look like by playing with iInv.
Particularly, I suggest that we get rid of the last parameter of iInv (the name of the "Hclose"), and instead have it add that as an obligation to the postcondition. So, if the goal starts out being `WP e {{ v, Q }}`, then when opening `inv N I` it becomes `WP e {{ v, \later I * Q }}`. Similar things happen when the goal is a view shift.
@robbertkrebbers @jjourdan what do you think? How hard would it be to implement this? We'd probably want a new typeclass generalizing things that can be in the goal when doing iInv. I fear that typeclass will be much like the infamous "frame shift assertions"...https://gitlab.mpi-sws.org/iris/iris/-/issues/92Discussion: Better(?) Logically-Atomic Triples2018-07-13T15:54:13ZJannoDiscussion: Better(?) Logically-Atomic TriplesHey everyone,
I am doing some groundwork on logical atomicity for weak memory and I got annoyed by the "current" definition of atomic triples:
1. The quantification over the "real" precondition P seems unnecessary.
2. The box around the...Hey everyone,
I am doing some groundwork on logical atomicity for weak memory and I got annoyed by the "current" definition of atomic triples:
1. The quantification over the "real" precondition P seems unnecessary.
2. The box around the shift is an artifact of working directly with (persistent) triples.
This is the reference definition of atomic triple (taken from @zhangz's iris-atomic@13900169bafb6b6ef1d091236dba493eaa25cc95):
```coq
∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
α x ∗
((α x ={Ei, Eo}=∗ P) ∧
(∀ v, β x v ={Ei, Eo}=∗ Q v))
) -∗ {{ P }} e @ ⊤ {{ Q }}.
```
I propose the following change:
```coq
atomic_shift Eo Ei α β Φ :=
|={Eo,Ei}=> ∃ x : A,
α x ∗
((α x ={Ei,Eo}=∗ ▷ atomic_shift Eo Ei α β Φ) ∧
∀ y, β x y ={Ei,Eo}=∗ Φ y).
atomic_wp Eo Ei α β := ∀ Φ, atomic_shift Eo Ei α β Φ -∗ WP e @ Eo { Φ }
```
It should be easy enough to derive a notion of logically-atomic triples (as opposed to weakestpre) the same way we derive normal triples.
I did some initial testing by porting iris-atomic/atomic_incr.v to this definition. Apart from some inconveniences regarding boxes in the client (orthogonal to logically-atomic triples; just a proof setup problem), the proof of the spec and the client remain mostly the same. One additional (albeit entirely trivial) Löb induction had to be introduced in the client to prove the atomic shift. The spec proof already had a Löb induction and so will almost any other proof of that kind I think.
You can see the changes to the proof here: janno/iris-atomic@06d9dc7d. The definition is here: janno/iris-atomic@ba66f8bd.
Before I continue to work with this new definition in my own development I would like to gather feedback. What does everyone think of it?
I am specifically worried about examples that somehow manage to run out of steps and thus cannot get rid of the `▷` modality. I can't imagine what those would look like but they might exist. Additionally, the added complexity of requiring `iLöb` in client proofs may be considered a substantial disadvantage of this definition by some.
P.S.: This is orthogonal to (and thus hopefully compatible with) the work on using telescopes to represent an arbitrary number of binders in atomic triples. I made some progress on that, too. But it's not done.https://gitlab.mpi-sws.org/iris/iris/-/issues/154Bring back side-conditionals for `iMod`2018-07-13T08:51:28ZRobbert KrebbersBring back side-conditionals for `iMod`By @jtassaro
> So, in Iris 2.0, if I'm recalling correctly, one only had (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P under the assumption that E2 ⊆ E1 ∪ E3. I guess in the Iris 3.0 this assumption is no longer needed anymore, and so this ...By @jtassaro
> So, in Iris 2.0, if I'm recalling correctly, one only had (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P under the assumption that E2 ⊆ E1 ∪ E3. I guess in the Iris 3.0 this assumption is no longer needed anymore, and so this assumption is not part of the FUpdFacts (and I can't think of a way to jam it into the instance of ElimModal so that iMod will do the right thing). The problem is that the logic from our ESOP 2017 paper is based on Iris 2.0 style so I need this assumption. Any thoughts? Obviously I can just re-define a version of iMod that accounts for this additional hypothesis, but I'm wondering if there's a preferred way.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/146Lemmas about updates should be instantiated by default witht the current BI i...2018-07-13T08:51:27ZJacques-Henri JourdanLemmas about updates should be instantiated by default witht the current BI instead of `iProp`The instances for the `FUpd` and `FUpdFacts` type classes are set in a way that gives the priority to `iProp`? Therefore, when using lemmas about updates in `vProp`, we sometimes have to manually instantiate them with the current BI. Oth...The instances for the `FUpd` and `FUpdFacts` type classes are set in a way that gives the priority to `iProp`? Therefore, when using lemmas about updates in `vProp`, we sometimes have to manually instantiate them with the current BI. Otherwise, the lemmas are instantiated with `iProp` and used through the embedding.
See, for example https://gitlab.mpi-sws.org/FP/sra-gps/blob/gen_proofmode_WIP/theories/examples/circ_buffer.v#L236
The instances for the `AsValid` type class prioritizes the fact of not using the embedding, so we should be able to fix this issue by simply making sure the search for `AsValid` occurs before `FUpd`, but I do not know how to do that.
@robbertkrebbers, any idea?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/147Infrastructure for the `monPred_all` modality2018-07-13T08:51:27ZJacques-Henri JourdanInfrastructure for the `monPred_all` modalityIf everything in the context is objective, then we should be able to introduce the `monPred_all` modality. This should reuse the infrastructure of `iAlways`.
However, I would like to go a bit further: Actually, in the case everything in...If everything in the context is objective, then we should be able to introduce the `monPred_all` modality. This should reuse the infrastructure of `iAlways`.
However, I would like to go a bit further: Actually, in the case everything in the context is objective, and the goal is objective too, we might want to switch to Iris proofmode to get rid of embeddings and all that.https://gitlab.mpi-sws.org/iris/iris/-/issues/176Reconsider normalizing `/\ emp` into `<affine>`2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgReconsider normalizing `/\ emp` into `<affine>`I was rather surprised when running `iFrame` added an `<affine>` modality in front of a goal. @robbertkrebbers explained:
> To understand what's happening, first note that when you frame something in a general BI, it will turn it into `...I was rather surprised when running `iFrame` added an `<affine>` modality in front of a goal. @robbertkrebbers explained:
> To understand what's happening, first note that when you frame something in a general BI, it will turn it into `emp`, not `True`. So, framing let's say `P` in `P ∗ Q` turns it into `emp ∗ Q`, which then get beautified into `Q`.
> In this case, you are framing `P` in `<pers> Q ∧ P`, which will turn it into `<pers> Q ∧ emp`. This is then beautified into `<affine> <pers> Q`
I think we should not perform this normalization, and just keep it as `<pers> Q /\ emp`.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/177Improve naming of lemmas about modalities2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgImprove naming of lemmas about modalitiesThe following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1...The following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2_{swap,comm}: M1 (M2 P) ⊣⊢ M2 (M1 P)
```
However, @robbertkrebbers noted that we have plenty of lemmas of the last form. Optimizing for conciseness, we could also use
```
M1_{into,impl,entails}_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
```Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/198iAlways fails without a proper error message2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgiAlways fails without a proper error messageThe following script
```
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
```
Fails at `iAlways` saying
```
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last ca...The following script
```
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
```
Fails at `iAlways` saying
```
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last call failed.
No matching clauses for match.
```
It should either give a proper error or empty the spatial context.https://gitlab.mpi-sws.org/iris/iris/-/issues/200Framing: Make* classes lead to suboptimal results2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgFraming: Make* classes lead to suboptimal resultsFraming uses `Make*` classes to turn terms into a certain form, e.g. a leading `▷^n`. However, those classes require the original term to be *equivalent* with the converted one. This leads to situations such as
```
Lemma test_iFrame_la...Framing uses `Make*` classes to turn terms into a certain form, e.g. a leading `▷^n`. However, those classes require the original term to be *equivalent* with the converted one. This leads to situations such as
```
Lemma test_iFrame_later_rel (P : PROP) :
▷ P -∗ (▷ (P ∧ P)).
Proof. iIntros "?". iFrame.
(* Now the goal is [▷ emp] *)
```
I would expect the goal to become `emp` (and hence `iFrame` closing the goal), and indeed that would be sound (`emp` implies `▷ emp`) but it doesn't happen.https://gitlab.mpi-sws.org/iris/iris/-/issues/181wp_apply instantiates evars too far2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgwp_apply instantiates evars too far```coq
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
```
The goal is now
```
============================
--------------------------------------∗
WP ?e @ ?s;...```coq
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
```
The goal is now
```
============================
--------------------------------------∗
WP ?e @ ?s; ?E {{ v, ?Φ v }}
```
but it should be
```
============================
--------------------------------------∗
?Q
```
This is in the generalized proofmode branch.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/193Remove or fix `base_logic/deprecated.v`2018-07-13T08:51:26ZRobbert KrebbersRemove or fix `base_logic/deprecated.v`It currently contains:
```
(*
FIXME
...
*)
```It currently contains:
```
(*
FIXME
...
*)
```Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/142Handle both `emp` and `True` as context2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgHandle both `emp` and `True` as contextThe generalized proofmode for a linear logic should be able to handle both `True` and `emp` as the context, ideally both in a somewhat canonical way. However, if both spatial and persistent context are empty, that can only be either `em...The generalized proofmode for a linear logic should be able to handle both `True` and `emp` as the context, ideally both in a somewhat canonical way. However, if both spatial and persistent context are empty, that can only be either `emp` or `True`; the other one will need a different representation. Right now, it is `emp`, so the only way to represent `True` is to have it explicitly in the spatial context -- which seems pretty funny. This is related to the problem with plainly and empty contexts (https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/98#note_22868).
In particular, if the goal is `valid P`, what should `iStartProof` do? (And, for that matter, what does it do currently?) The goal is `True |- P`, so the behavior from Iris (having both contexts empty) will not work.
Some options:
* Make "both contexts are empty" mean `True`, arguing that `True` is somehow more fundamental than `emp`. That clarifies what `iStartProof` should do, but now, how should `emp` be represented? Maybe the empty spatial context is `True`, but when non-empty, we just `*` together what we have, so `emp` is represented by some `"H": emp` in the spatial context? That seems like a strange discontinuitiy though. It means if we "use up" the last spatial assertion, we have to synthesize an `emp` into the context -- not very pleasant.
* Somehow "deeply embed" this information. For example, the spatial context could be optional (`option list PROP`); when absent, it interprets to `True`, otherwise to the iterated `*`. This is also awkward in some circumstances, e.g. when the spatial context is currently missing and the goal is `P -* Q` and we do `iIntros` -- now a `True` has to be synthesized into the spatial context. So maybe the better way to "deeply embed" this is to have some boolean indicating whether the context is "precise" or whether there is a `* True` around? Seems really ugly, but this time I cannot come up with a situation where we have to synthesize an assertion.
How is this currently handled in the IPM for Iron?https://gitlab.mpi-sws.org/iris/iris/-/issues/159Find better name for "emp |- P"2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgFind better name for "emp |- P"Currently, `emp |- P` is called `bi_valid P` and is used as a coercion from `PROP` to `Prop`. This turns out to be the right definition for the coercion (i.e., `(l |-> v -* l |->{0.5} v * l |->{0.5} v)%I` is provable), but the name is d...Currently, `emp |- P` is called `bi_valid P` and is used as a coercion from `PROP` to `Prop`. This turns out to be the right definition for the coercion (i.e., `(l |-> v -* l |->{0.5} v * l |->{0.5} v)%I` is provable), but the name is dubious: Usually, validity is defined as `True |- P`. Let's try to find a better name.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/170iFresh should reserve fresh names2018-07-13T08:51:26ZJoseph TassarottiiFresh should reserve fresh namesRight now `iFresh` just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to `iFresh`. As a result, the following pattern fails:
...Right now `iFresh` just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to `iFresh`. As a result, the following pattern fails:
```
let H1 := iFresh in
let H2 := eval vm_compute in (match H1 with
| IAnon x => IAnon (1 + x)
| INamed x => IAnon 1
end) in
let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
iDestruct "H" as pat.
```
because `iDestruct` will also use `iFresh` and gets a name that conflicts with `H1`.
One solution would be to add a counter to the `envs` record which is incremented each time `iFresh` is called. This would actually also probably make `iFresh` more efficient anyway.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/156How to deal with `emp`, `True`, and friends when the BI is ambigious2018-07-13T08:40:32ZRobbert KrebbersHow to deal with `emp`, `True`, and friends when the BI is ambigiousThe following discussion from !115 should be addressed:
We often write `emp : PROP`. However, since coercions are explicit term constructors in Coq, this apparently leads to unification problems here and there.
The alternative is to wr...The following discussion from !115 should be addressed:
We often write `emp : PROP`. However, since coercions are explicit term constructors in Coq, this apparently leads to unification problems here and there.
The alternative is to write `bi_emp (PROP:=PROP)`, which is ugly.
Maybe we should have special notations to force the type arguments of `emp`, `True`, and friends.
I think ssr is also doing something like that. Depending on the outcome of this issue, we should not just address the occurrence in !115, but also fix other occurrences.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/182done when goal is evar picks unnecessarily strong2018-07-13T08:40:31ZRalf Jungjung@mpi-sws.orgdone when goal is evar picks unnecessarily strongWhen the goal is an evar (and that evar does not appear otherwise in the current goal), like in
```
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
```
then doing `done` will pick a persistent (or spa...When the goal is an evar (and that evar does not appear otherwise in the current goal), like in
```
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
```
then doing `done` will pick a persistent (or spatial, I guess) hypothesis instead of just `True` or `emp`.
Maybe we should add `bi.True_intro` with high priority to the database?https://gitlab.mpi-sws.org/iris/iris/-/issues/187Support framing in `iCombine`.2018-07-13T08:40:31ZDan FruminSupport framing in `iCombine`.I wish that the `iCombine` tactic would support framing: `iCombine "H1 H2" as "$"`.I wish that the `iCombine` tactic would support framing: `iCombine "H1 H2" as "$"`.https://gitlab.mpi-sws.org/iris/iris/-/issues/190Framing persistent hypotheses under a later in the goal2018-07-13T08:40:31ZHai DangFraming persistent hypotheses under a later in the goalI have
```
"H": P
-------------□
▷ P ∗ Q
```
`iFrame "H"` gives me back `▷ emp ∗ Q`. I was working with an affine BI.
@jtassaro suggests to generalize `make_sep_emp_l`.I have
```
"H": P
-------------□
▷ P ∗ Q
```
`iFrame "H"` gives me back `▷ emp ∗ Q`. I was working with an affine BI.
@jtassaro suggests to generalize `make_sep_emp_l`.https://gitlab.mpi-sws.org/iris/iris/-/issues/91Generalizing the Proofmode2018-07-13T08:40:30ZJannoGeneralizing the ProofmodeI am sure I have this request this issue with almost everyone already but let me summarize it here again:
In our iGPS work, we work with monotone (Iris) predicates over a type called views - though the actual type doesn't matter much. We...I am sure I have this request this issue with almost everyone already but let me summarize it here again:
In our iGPS work, we work with monotone (Iris) predicates over a type called views - though the actual type doesn't matter much. We call these predicates vPreds. In spirit, all proofs are done with respect to a "current" view which changes when taking a step – not unlike step indices, I think. However, we currently have to manually upgrade the view of our assumptions to the new view after taking a step to achieve coherence between the goal and the assumptions.
Since I am about to start another development with the same setup I wanted to gather information on how to hide the views from the potential users of our logic. I talked to @jjourdan about this and he suggested a bunch of hacky steps that could potentially make the views disappear. The approach uses a typeclasse to represent the current view of the proof. However, I think we will still suffer from some inherent drawbacks: we have to redefine connectives, the proof mode syntax, and probably many more things. If possible I would prefer a more principled solution.
Here's an incomplete list of pain points with our current setup:
1. Views show up in the proof context.
1. Views show up in the proof script. (We can mostly hide them behind custom tactics and underscores, though.)
1. We define what amounts to an incomplete copy of the uPred scope to get all the logical connectives on vPreds.
1. Because we do not want to redefine every last bit (especially lemmas) of uPred, we sometimes unfold away all the vPred stuff. This results in scope chaos, with annotations %I and %VP everywhere.
1. Once we unfold, refolding is almost impossible.
1. The typeclasses for the proofmode are not always smart enough to see through our definitions and recognize the underlying uPreds. (I think this is largely fixed but I don't quite remember what the exact issue were. They might pop up again in different circumstances)
I think that these issues could be fixed by making the proofmode more general. Maybe it would be parametrized by a BI with the more intricate parts (viewshift stuff?) parametrized by additional assumptions on the BI. Maybe different parts of it would have different parameters. I haven't thought a lot about the specifics. What I think this doesn't immediately fix is the interaction between two different logics like vPred and uPred: How does one make the proofmode aware of the two different levels? Can we get rid of the need to switch between the two logics entirely or should we try to make it possible to switch between them inside proofs?
I would love to hear your feedback on this. Maybe there are other ways of going about this? @robbertkrebbers, I know you thought about this as well. What is the best approach in your view?
/cc @haidang