Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-11-01T23:47:30Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/105Add some theory about the interaction of plainly and fancy updates2017-11-01T23:47:30ZRalf Jungjung@mpi-sws.orgAdd some theory about the interaction of plainly and fancy updates@amintimany has some theory there, we should get the reusable bits upstream.@amintimany has some theory there, we should get the reusable bits upstream.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/103Find a better name for iMod2017-11-24T15:57:13ZRalf Jungjung@mpi-sws.orgFind a better name for iModWe do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
Proposed alternatives: `iRun`, `iUpd`...We do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
Proposed alternatives: `iRun`, `iUpd`. `iUpd` is my personal favorite. I know that the tactic supports other modalities, but 99,9% of the time it is used to eliminate some form of an update. The name is more informative than `iMod`, and not more wrong.
`iRun` is slightly less informative, but also less wrong: The tactic does bind in a monad, which can be seen as "running the computation".
Cc @robbertkrebbers @jjourdan
EDIT: All right, I stand corrected on the "wrong" part. Sorry for that. It is still uninformative.https://gitlab.mpi-sws.org/iris/iris/-/issues/102`solve_proper` having troubles proving non-expansiveness2017-10-10T11:50:17ZDan Frumin`solve_proper` having troubles proving non-expansivenessIn the snippet below`solve_proper` is not able to prove non-expansiveness of a higher-order predicate.
`solve_proper` is defined as `solve_proper_core ltac:(fun _ => f_equiv)`.
However, one can use `solve_proper_core ltac:(fun _ => simp...In the snippet below`solve_proper` is not able to prove non-expansiveness of a higher-order predicate.
`solve_proper` is defined as `solve_proper_core ltac:(fun _ => f_equiv)`.
However, one can use `solve_proper_core ltac:(fun _ => simpl; f_equiv)` to automatically discharge the obligations.
Is there a reason why this simplification is not happening in `solve_proper_core`?
Is it for the performance reasons?
```coq
From iris.heap_lang Require Import lang proofmode tactics notation.
Section linkedlist.
Context `{heapG Σ}.
Program Definition pre_isLinkedList : (valC -n> iProp Σ) -n> (valC -n> iProp Σ) :=
λne P v, (⌜v = InjLV #()⌝
∨ ∃ (h t : val) (l : loc),
⌜v = InjRV (PairV h #l)⌝
∗ l ↦ t
∗ ▷ (P t))%I.
Solve Obligations with solve_proper_core ltac:(fun _ => simpl; f_equiv).
End linkedlist.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/101Make Iris run in jsCoq2017-11-30T09:53:53ZRalf Jungjung@mpi-sws.orgMake Iris run in jsCoqCurrent status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert al...Current status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert already mentioned that he wanted to look into that.https://gitlab.mpi-sws.org/iris/iris/-/issues/100Proof mode notation broken depending on import order2017-11-11T09:19:19ZRalf Jungjung@mpi-sws.orgProof mode notation broken depending on import orderIt is a long-standing issue that sometimes, depending on the order of re-exports and imports, the proof mode notation is broken. I finally decided to minimize this, and you can find the result in the [`ipm-notation-broken` branch](https...It is a long-standing issue that sometimes, depending on the order of re-exports and imports, the proof mode notation is broken. I finally decided to minimize this, and you can find the result in the [`ipm-notation-broken` branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/ipm-notation-broken). I first thought this is a Coq bug, but now I am not so sure anymore: We do have different notations in the same scope that lead to printing being ambiguous.
Namely, we have
```
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
(at level 99, Q at level 200, right associativity) : C_scope.
```
and
```
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Γ Δ) ⊢ Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
C_scope.
```
We seem to be relying on a guarantee that if one notation is strictly more specific than another one, it will have higher priority. Does Coq claim to have such a guarantee?
Maybe one possible solution would be to move the proof mode notations into a different scope, and have `iStartProof` introduce that scope (i.e., turn the goal into `(...)%ProofMode`).Iris 3.1Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/99iNext does not strip off later below existential2017-10-02T13:34:05ZRalf Jungjung@mpi-sws.orgiNext does not strip off later below existential```
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
```
Stripping off laters does happen below con...```
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
```
Stripping off laters does happen below conjunctions, but not below existentials.https://gitlab.mpi-sws.org/iris/iris/-/issues/98`iIntros.` fails to introduce `True`2017-09-27T08:45:17ZRalf Jungjung@mpi-sws.org`iIntros.` fails to introduce `True````
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
```
shows an error:
```
Tactic failure: iIntro: nothing to introduce.
``````
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
```
shows an error:
```
Tactic failure: iIntro: nothing to introduce.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/97`iIntros.` should always enter proof mode2017-09-27T08:45:18ZRalf Jungjung@mpi-sws.org`iIntros.` should always enter proof mode```
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
``````
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/96Spurious whitespace in proofmode notations2017-08-24T14:09:21ZRobbert KrebbersSpurious whitespace in proofmode notationsThis is probably a result of !59. For example:
```coq
Lemma test_iIntros_persistent P Q `{!PersistentP Q, !PersistentP R} :
(P → Q → R → P ∗ Q)%I.
Proof. iIntros "H1 H2 #H3".
```
Coq now displays:
```
_______________________________...This is probably a result of !59. For example:
```coq
Lemma test_iIntros_persistent P Q `{!PersistentP Q, !PersistentP R} :
(P → Q → R → P ∗ Q)%I.
Proof. iIntros "H1 H2 #H3".
```
Coq now displays:
```
______________________________________(1/1)
"H3" : R
--------------------------------------□
"H1" : P
"H2" : Q
--------------------------------------∗
P ∗ Q
```
So, as you can see, the printing of each context starts with a spurious whitespace.
I don't know whether this is a Coq bug, or a bug in our notation. @jung any idea?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/95Introduce implication if premise is persistent2017-08-24T08:49:51ZRalf Jungjung@mpi-sws.orgIntroduce implication if premise is persistentCurrently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the g...Currently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the goal is `box P -> Q`, introducing should be possible even for a non-empty spatial context.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/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/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.`