Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-02-15T10:36:40Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/93Using wp_ tactics without making every tiny step a function is super slow sol...2019-02-15T10:36:40ZJoshua YanovskiUsing wp_ tactics without making every tiny step a function is super slow solely because Coq has to keep proving this Closed obligationWhich would be fine, except that there is no good way right now to prove closed-ness under a binder without knowing string literals for the variable names.
Concrete example:
```coq
Definition big_blob_of_code x :=
(* huge blob of...Which would be fine, except that there is no good way right now to prove closed-ness under a binder without knowing string literals for the variable names.
Concrete example:
```coq
Definition big_blob_of_code x :=
(* huge blob of code here *)%E.
Definition foo: val :=
(λ: [ "x"; "y" ], big_blob_of_code "x" + big_blob_code "y").
```
I don't want big_blob_of_code to be a function (because it isn't in the source code, and I'd like to actually verify foo as written rather than some other thing). However, Coq takes far too long to execute `wp_rec` on my `foo`-like thing, and it only gets worse the more times it is called. It also requires an irritating number of rewrites. There may be some ways around this if you happen to have some closed values somewhere up the stack and use `Notation` for previous ones, with a typeclass instance for `Closed` for those functions, but even that is highly annoying, and proving `Closed` for any of the lower-level functions doesn't really work because of the way `solve_closed` is defined (and according to Janno, probably just can't work at all).
I don't really care what solution this has, just that there is one.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/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 @haidanghttps://gitlab.mpi-sws.org/iris/iris/-/issues/90Strong persistent framing and saved_prop_agree2017-09-12T14:34:23ZRobbert KrebbersStrong persistent framing and saved_prop_agreeProblem reported by @haidang in #71:
> If I have in my persistent context `Hx: saved_prop_own γ x` and `Hy: saved_prop_own γ y`, then `iDestruct (saved_prop_agree with "[$Hx $Hy]") as "Eq"` gives `x = x`. To get the right result, instea...Problem reported by @haidang in #71:
> If I have in my persistent context `Hx: saved_prop_own γ x` and `Hy: saved_prop_own γ y`, then `iDestruct (saved_prop_agree with "[$Hx $Hy]") as "Eq"` gives `x = x`. To get the right result, instead I need to instantiate `saved_prop_agree _ x y`, which is less convenient.Robbert KrebbersRobbert Krebbershttps://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/88More convenient destruct of pure hypotheses2020-04-07T07:01:25ZRalf 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 "...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/87Remove "dev" from list of compatible coq versions?2017-04-19T16:05:33ZJannoRemove "dev" from list of compatible coq versions?Iris currently lists "dev" as a compatible coq version. I have not tried to find out if it actually is compatible, since ssreflect currently does not compile against coq-dev. @jjourdan and I discussed this issue and we came to the conclu...Iris currently lists "dev" as a compatible coq version. I have not tried to find out if it actually is compatible, since ssreflect currently does not compile against coq-dev. @jjourdan and I discussed this issue and we came to the conclusion that "dev" should be removed and possibly replaced with a comment explaining to add it again when compiling against coq-dev. What does everyone else think?
This issue came up because the inclusion of "dev" breaks `make build-dep` in our gps development. Opam thinks coq-dev is a compatible with both ssreflect (their fault) and Iris (our fault).https://gitlab.mpi-sws.org/iris/iris/-/issues/86CoPset finite decomposition into singletons2017-05-19T15:20:29ZHai DangCoPset finite decomposition into singletonsI'm working with a proof that requires unlimited tokens, which leads me to use the disjoint union `CoPset` cmra.
In a specific subproof I need to split a finite set `X : gset positive` of tokens into singletons:
`own γ (CoPset $ of_gs...I'm working with a proof that requires unlimited tokens, which leads me to use the disjoint union `CoPset` cmra.
In a specific subproof I need to split a finite set `X : gset positive` of tokens into singletons:
`own γ (CoPset $ of_gset X) ≡ [∗ set] i ∈ X, own γ (CoPset $ of_gset {[i]}) `
With `big_opS_commute1` I can get
`own γ ([⋅ set] i ∈ X, CoPset $ of_gset {[i]}) ≡ [∗ set] i ∈ X, own γ (CoPset $ of_gset {[i]})`
And then I only need to show that
`CoPset $ of_gset X ≡ [⋅ set] i ∈ X, CoPset $ of_gset {[i]}`,
which currently there seems to be no easy way to solve.
Is there an induction principle for gset's, or any way to solve this?https://gitlab.mpi-sws.org/iris/iris/-/issues/85Proof mode goals in empty context cannot be distinguished from Coq goals2017-05-19T15:20:29ZRobbert KrebbersProof mode goals in empty context cannot be distinguished from Coq goals@jung noted this problem somewhere in lambdarust, see below for a simple example:
```coq
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)
```
We...@jung noted this problem somewhere in lambdarust, see below for a simple example:
```coq
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)
```
We could add some special symbol to the proof mode notation with the empty context? Any suggestions?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/84iDestruct on non-existing name yields "no matching clause for match"2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgiDestruct on non-existing name yields "no matching clause for match"Title says it all. Goal state:
```
============================
"Hincl" : type_incl ty1 ty2
"Hsz" : ⌜ty_size ty1 = ty_size ty2⌝
"Hoincl" : ∀ (tid0 : thread_id) (vl : list val), ty_own ty1 tid0 vl -∗ ty_own ty2 tid0 vl
"Hsincl" :...Title says it all. Goal state:
```
============================
"Hincl" : type_incl ty1 ty2
"Hsz" : ⌜ty_size ty1 = ty_size ty2⌝
"Hoincl" : ∀ (tid0 : thread_id) (vl : list val), ty_own ty1 tid0 vl -∗ ty_own ty2 tid0 vl
"Hsincl" : ∀ (κ0 : lft) (tid0 : thread_id) (l0 : loc),
ty_shr ty1 κ0 tid0 l0 -∗ ty_shr ty2 κ0 tid0 l0
--------------------------------------□
"Hshr" : ty_shr (rc ty1) κ tid l
--------------------------------------∗
ty_shr (rc ty2) κ tid l
```
Tactic: `iDestruct "Hst" as (??) "H".`
Error: `Error: No matching clauses for match.`https://gitlab.mpi-sws.org/iris/iris/-/issues/82Consider adding a "strong" always modality2018-01-31T09:21:27ZRalf Jungjung@mpi-sws.orgConsider adding a "strong" always modalityThe idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.
IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default...The idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.
IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default should be not to add anything unless we really need it -- and we got pretty far without the strong always.
So what do we have that this would enable? (I am writing "SB" for the strong box below.)
* Propositional extensionality. Not sure how useful that would be though.
* `(|=> SB P) -> SB P`, i.e. basic updates can be removed around the strong box. That seems pretty powerful, but the only application we have so far is to make the adequacy lemma nicer to state (no more "nested laters and basic updates", but just "nested laters").
* It would be possible to have the "core of a proposition" in a clean way, defined as `∀ Q, SB (Q -> □Q) -> SB (P -> Q) → □ Q`. This works because `SB P -> □ Q` is persistent.
@robbertkrebbers I seem to remember you saying that one of the Iris-based papers added the strong box. Why again did they need it?
I am not convinced that the above is enough of a reason to add the box to the core. In particular, I feel like it would be non-trivial to explain to people why we have two box-like modalities.https://gitlab.mpi-sws.org/iris/iris/-/issues/81Let iAlways clear the spatial context2017-10-27T12:33:40ZRalf Jungjung@mpi-sws.orgLet iAlways clear the spatial contextRight now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is simil...Right now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is similar to the difference between `iIntros "!>"` and `iNext` -- the latter may affect the context, the former will not. Furthermore, this is backwards compatible because iAlways will now only succeed in strictly more cases.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/80More precise error message on missing hypothesis2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgMore precise error message on missing hypothesisCurrently, when I say e.g. `iSplit "H1 H2 H3 H4"` and one of the hypotheses does not exist, the error is `hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.`. This is confusing because it indicates that none of them was found ...Currently, when I say e.g. `iSplit "H1 H2 H3 H4"` and one of the hypotheses does not exist, the error is `hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.`. This is confusing because it indicates that none of them was found (while actually, only some of them have not been found). It is also not as useful as the error would be if it would name which hypothesis has not been found.
I assume spec patterns have the same issue.https://gitlab.mpi-sws.org/iris/iris/-/issues/79Make iSplit work below existentials?2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgMake iSplit work below existentials?I have a goal of the form
```
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
```
and all my assumptions are only available later. I cannot do `iNext` because not everything is below a later, but I can do `rewrite -uPred.sep_exist_l. iSplit; f...I have a goal of the form
```
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
```
and all my assumptions are only available later. I cannot do `iNext` because not everything is below a later, but I can do `rewrite -uPred.sep_exist_l. iSplit; first done.`. This works because some part of what is below the existential does not depend on the witness.
Now I wonder, would it make sense for `iSplit` to work in this case (giving me ` ⌜#l = #l⌝` and `∃ x : vec val m, ▷ l ↦∗ x` as goals)? The rewrite I did above is not very discoverable, but neither is the `iSplit`. What do you think? @jjourdan @robbertkrebbers
(You may wonder why I have things under the existential that do not depend on the witness. The reason is that lemmas of the form `∃ x y z, P` work much better with the proofmode, because I an do a single `iDestruct ... as (x y z) ...`. If I pushed the existential down, destructing things would become much more annoying.)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/77Have iNext "pull" laters out from below other operators.2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgHave iNext "pull" laters out from below other operators.Let's say I have a goal of the shape `∃ x, ▷ Q x` (and the type of `x` is inhabited). I also have an assumption below a later. I want to strip the later from the assumption, which is okay because our goal is equivalent to `▷ ∃ x, Q x`. C...Let's say I have a goal of the shape `∃ x, ▷ Q x` (and the type of `x` is inhabited). I also have an assumption below a later. I want to strip the later from the assumption, which is okay because our goal is equivalent to `▷ ∃ x, Q x`. Currently, I have to do `rewrite -uPred.later_exist` for this.
First of all, I am wondering why `iApply uPred.later_exist` doesn't work in this context. Secondly, it'd be nice if `iNext` could also "pull" laters out of the goal if there's not yet a top-level later.https://gitlab.mpi-sws.org/iris/iris/-/issues/76`iDestruct` for big ops2017-05-19T15:20:29ZRobbert Krebbers`iDestruct` for big opsTogether with @jung and @jjourdan we discussed that it would be useful if `iDestruct` (and tactics like `iSplit` and `iFrame`) would have better support for big ops, in particular, that when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ ...Together with @jung and @jjourdan we discussed that it would be useful if `iDestruct` (and tactics like `iSplit` and `iFrame`) would have better support for big ops, in particular, that when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x
we could use `iDestruct "H" as "[H1 H2]"` to turn it into:
H1 : Φ 0 y
H2 : [∗ list] k ↦ x ∈ l, Φ (S k) x
Although this is not particularly difficult to implement (it just requires one to declare suitable `IntoAnd` instances), it gives rise to some potential ambiguity, namely, what is going to happen when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x ∗ Ψ k x
Will it split through the cons, or through the star inside of the predicate in the big op?
Currently, it will split through the ∗ due to the instance `into_and_big_sepL`. Declaring yet another `IntoAnd` instance for the `cons` case is a bad idea, as it will give rise to the ambiguity above, and we end up with tactics that will behave unpredictably.
However, I think that the `cons` instance would be much more useful than the `∗` instance, hence I propose to drop the current `∗` instance, and instead declare instances for `cons` (and possibly `app`, which does not lead to ambiguity).https://gitlab.mpi-sws.org/iris/iris/-/issues/75Build any merge request on the CI2017-05-19T15:20:29ZRobbert KrebbersBuild any merge request on the CICurrently, I have to change the `.gitlab-ci.yml` in the branch corresponding to the merge request. This is a bit cumbersome, because I have to be careful to not merge the commit in which I changed `.gitlab-ci.yml` when merging into maste...Currently, I have to change the `.gitlab-ci.yml` in the branch corresponding to the merge request. This is a bit cumbersome, because I have to be careful to not merge the commit in which I changed `.gitlab-ci.yml` when merging into master.
Would it be possible to automatically build any branch corresponding to an MR on the CI?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/74iNext does not strip off both laters from ▷ P ∗ ▷ Q2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgiNext does not strip off both laters from ▷ P ∗ ▷ QI would expect the following test to succeed:
```
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) :
▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
iIntros "H". iNext. iAssumption.
Qed.
```I would expect the following test to succeed:
```
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) :
▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
iIntros "H". iNext. iAssumption.
Qed.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/73Specialization patterns syntax extensions2017-05-19T15:20:29ZRobbert KrebbersSpecialization patterns syntax extensionsThere have been some requests to add new stuff to specialization patterns:
1. A `//` token for performing `done`. One could then write things like `[$H1 $H2 //]` or `[//]`.
2. Being able to frame in persistent specialization patterns, i...There have been some requests to add new stuff to specialization patterns:
1. A `//` token for performing `done`. One could then write things like `[$H1 $H2 //]` or `[//]`.
2. Being able to frame in persistent specialization patterns, i.e. `[# $H1 $H2]`.
3. A token, say `[$]` to solve the goal by framing, and by keeping all unused hypotheses for the subsequent goals.
However, there are some questions here:
1. I suppose we want to be able to use `//` also for pure and persistent goals. For example `[% //]` and `[# //]`.
2. What is going to happen when we do `[# H1 $H2]`. There are some obvious choices: a.) using a hypothesis without a `$` prefix is forbidden b.) ignore all hypotheses that are not prefixed with a `$` (there is no need to select hypotheses, you get all anyway, since the goal is persistent) c.) prune the context that goal.
3. What to frame? Just the spatial hypotheses, or everything (including the persistent ones)?
Anyone some ideas? I would like to have a syntax that is not too FUBARed.Robbert KrebbersRobbert Krebbers