Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-02-27T11:21:27Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/230"Generalizable All Variables" considered harmful2019-02-27T11:21:27ZRalf Jungjung@mpi-sws.org"Generalizable All Variables" considered harmfulOver the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting `Generalizable All Variables`. Imagine we had a type `spropC`, an OFE, and ...Over the last few days, when reflecting the way we introduce assumptions in our proofs, I came to the conclusion that I am somewhat uneasy with globally setting `Generalizable All Variables`. Imagine we had a type `spropC`, an OFE, and then consider the following preamble:
```
Section something_about_sprop.
Conext `{authG Σ (exR spropC)}.
```
Can you spot what's wrong with this? Well, we just assumed that SProp is discrete, which it is not. Ouch.
From my experiments, we can avoid over-eager generalization by adding a `!`. I have not found conclusive documentation for `!`, but it seems the least we should do is (a) add `!` basically everywhere, and (b) treat the *absence* of `!` as a big fat warning bell during code review. The latter will be hard.
But really, while `Generalizable All Variables` is very useful for some things (like the general fin map libraries in std++), I think for most code the benefits are slim. I have [ported a few files](https://gitlab.mpi-sws.org/iris/iris/commit/f5bceb45532b5c9dff9124589b93eccee722be8f) to `Generalizable No Variables`, and the additional declarations required are negligible IMO. So I think what we should aim for (but that might take a while) is for std++ to no longer set `Generalizable All Variables` (to avoid inflicting this subtle issue onto unsuspecting users), and to locally set that flag in the (few) files that really benefit.
Or maybe I am overreacting, and things are not that bad. But the thought of accidentally assuming things I don't want to assume makes me nervous. What do you think?https://gitlab.mpi-sws.org/iris/iris/-/issues/185"iApply ... with" unifies with assumptions before taking goal into account2019-11-01T13:45:51ZRalf Jungjung@mpi-sws.org"iApply ... with" unifies with assumptions before taking goal into accountThe following test case fails:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```
This is fairly an...The following test case fails:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```
This is fairly annoying when working with higher-order lemmas, for example it came up in the logically atomic context when trying to apply
```coq
Lemma astep_intro Eo Em α P β Φ x :
α x -∗
((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗
atomic_step Eo Em α P β Φ.
```
where `α : A -> PROP`. Now `iApply (astep_intro with "foo")` fails to apply in most cases because it infers the wrong `α`.https://gitlab.mpi-sws.org/iris/iris/-/issues/520"not a BI assertion" when using let-bindings2023-05-04T20:31:38ZRalf Jungjung@mpi-sws.org"not a BI assertion" when using let-bindingsThe following script used to work, but was broken by the change to -∗ notation:
```
Section tests.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_wand_below_let (P : PROP) :
let Q := (P ∗ P)%I in
Q -∗ Q.
Proof. iIntros...The following script used to work, but was broken by the change to -∗ notation:
```
Section tests.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_wand_below_let (P : PROP) :
let Q := (P ∗ P)%I in
Q -∗ Q.
Proof. iIntros "?".
```
Using `⊢` instead of `-∗` still works, but this should also work with a wand.https://gitlab.mpi-sws.org/iris/iris/-/issues/452"wp_apply ... as"2023-03-18T17:54:27ZRalf Jungjung@mpi-sws.org"wp_apply ... as"Applying a typical spec in Iris usually looks something like this:
```
wp_apply (Spec with "...").
{ (* solve precondition *) }
iIntros (x) "H".
```
The `iIntros` can be quite far removed from the `wp_apply`, if proving the precondition ...Applying a typical spec in Iris usually looks something like this:
```
wp_apply (Spec with "...").
{ (* solve precondition *) }
iIntros (x) "H".
```
The `iIntros` can be quite far removed from the `wp_apply`, if proving the precondition takes some work. Also it seems a bit odd to have this separated into two tactics.
@robbertkrebbers I wonder how feasible it would be to support `wp_apply (Spec with "...") as ...`, combining the `iIntros` into the `wp_apply`? I have actually accidentally written this last week and was a bit bummed that it did not work. ;)https://gitlab.mpi-sws.org/iris/iris/-/issues/568[coq-iris-heap-lang] Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-18T16:04:50ZRomain Tetley[coq-iris-heap-lang] Please create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (4.1.0) **does not work** with Coq `8.19.0`.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, **preferably before March 31st, 2024**?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/405https://gitlab.mpi-sws.org/iris/iris/-/issues/19[Maybe] Make uPred work on OFEs2016-11-22T15:25:52ZRalf Jungjung@mpi-sws.org[Maybe] Make uPred work on OFEsI spent some time last week talking with Santiago, a student of Andrew Appel, and trying to figure out the exact relation of their and our model. We did not reach a definitive conclusion. In particular, we could not tell where exactly ou...I spent some time last week talking with Santiago, a student of Andrew Appel, and trying to figure out the exact relation of their and our model. We did not reach a definitive conclusion. In particular, we could not tell where exactly our CMRA requirements of non-expansiveness and the extension axiom appear in their model.
However, one thing became clear: They do have a separation algebra on what Santiago called "juicy heap", which is a heap that can store either values or assertions (so, it combines our physical state and invariant maps). Separation algebras are relational, so they had no trouble with equality not being decidable. (And Santiago confirmed my belief that working with this relational composition is a *huge* pain in many other places.) However, they also did not have to go through the length of having a limit construction corresponding to what our agreement CMRA does. This is not entirely surprising, we know we don't actually need these limits and in their approach, all these proof obligations are coming up and discharged much more "on-demand", and much later. (For example, they have to be really, really careful when defining the meaning of what corresponds to our invariant assertion. If they screw up, they will only notice much later, when some proof rule does not work out. On the other hand, all we have to check is non-expansiveness of the definition.)
It would be nice if we would not have to unnecessarily complicate our model with this limit construction. That would also give us a better position when comparing with Appel's stuff ;-)
Cc @robbertkrebbers
I guess this is blocked on "sorting the canonical structure mess" ;-)https://gitlab.mpi-sws.org/iris/iris/-/issues/18[Maybe] Remove invariants2016-08-22T15:55:33ZRalf Jungjung@mpi-sws.org[Maybe] Remove invariantsI am reasonably sure that having higher-order ghost state, we can remove invariants and masks from core Iris and instead just have an assertion annotated at WP that is preserved throughout execution.
Cc @kaspersv @robbertkrebbers
...I am reasonably sure that having higher-order ghost state, we can remove invariants and masks from core Iris and instead just have an assertion annotated at WP that is preserved throughout execution.
Cc @kaspersv @robbertkrebbers
## Changes to the model
Worlds are removed from the global resources.
World satisfaction becomes *significantly* simpler: Masks are removed, and we are left with
```text
\sigma |= r := {n | r \in V_{n} /\ r.\pi = ex(\sigma)}
```
(Or maybe we still have to make this trivial at step-index 0, I am not sure.)
This simplification is the main pay-off of the change. Of course, the complexity is not just gone, but it it moved from the model to the logic -- following the usual pattern that we saw over and over again with Iris.
Masks are just removed from primitive view shifts.
For WP, of course masks are removed, but we need to add something instead: We need to add a way for an assertion to be preserved at every single step of execution. So, we get something like
```text
wp_I(e, \Lam v. Q) = \Lam r n. \All r_f, \sigma, m, ...
(\Exists r_I. I r_I (m+1) /\ (m+1) \in \sigma |= (r * r_I * r_f)) ...
=> \Exists s_1, s_2. (\Exists r_I. I r_I m /\ m \in \sigma |= (s_1 * s_2 * r_I * r_f))
...
```
In other words, besides the frame r_f, we demand that there is some resource r_I satisfying I, both before and after the step has been taken. This replaces the former existential quantification over some map defining the resources backing the invariants, which was part of world satisfaction.
# Changes to the logic
Remove the invariant assertions and all rules related to invariants or masks.
We obtain a new form of the atomic rule of consequence. This is how it looks for Hoare triples:
```text
P * I ==> P' * I'
{P'} e {Q'}_I'
Q' * I' ==> Q * I
e atomic
-------------------
{P} e {Q}_I
```
I have yet to figure out the most elegant way to write this as a WP rule.
We also need a weakening rule, maybe like this:
```text
I <=> I' * I_f
{P'} e {Q'}_I'
-------------------
{P} e {Q}_I
```
All the other rules force the I to be the same in all constituents.
# Recovering invariants
To recover invariants, we first define the `I` that we typically use for triples. It is pretty much exactly the part we removed from world satisfaction, but expressed *inside* the logic:
```
W(E) := \Exists S \in \finpowerset(N). own ... (\authfull S) *
\Sep_{i \in S \cap E} \Exists P : iProp. \later P * i |=> P
```
In other words, there is some ghost state tracking which invariants are allocated. This ghost state has the structure `Auth(\finpowerset(N))`, where we use union (*not* disjoint!) as composition on N. Furthermore, for all invariants that exist and that are enabled in the mask `E`, there is a saved proposition defining which is the invariant with that index, and the invariant is enforced.
We can then recover a WP / Hoare triple with mask `E` by using `I := W(E)`. Furthermore, we define
```
P |={E1,E2}=> Q := P * W(E1) ==> P * W(E2)
inv i P := own ... (\authfrag {i}) * i |=> P
```
We can then prove the old atomic rule of consequence, as well as the invariant-related view shifts, inside the logic.
We can go even further and, for example, allow creating an invariant that is *open*:
```text
E infinite
-------------------
W(E) ==> \Exists i \in E. inv i P * W(E \ {i})
```
This was not possible previously as there was no way to bind the `i` in the new mask.
# Open questions
Right now (in current Iris), the forked-off thread actually has a different mask than the local thread. I think to model this, we need a WP with *two* `I` annotations: One for the current thread, one for all forked-off threads. Maybe there has to be some relationship between these two. I am not sure how exactly this would look.
The weakening rule looks a little strange, and may not even be strong enough. What is the `I_f` to weaken `W(E)` to a smaller mask?https://gitlab.mpi-sws.org/iris/iris/-/issues/489`\Ref` in heaplang.sty clashes with newer versions of the hyperref package2022-11-23T13:05:11ZJonas Kastberg`\Ref` in heaplang.sty clashes with newer versions of the hyperref packageI (and @amintimany at least) have experienced some oddities when using `\Ref` macro.
It seems that the culprit is the `hyperref` package, although I have not always had the problem.
I suppose the easiest course of action would be to chan...I (and @amintimany at least) have experienced some oddities when using `\Ref` macro.
It seems that the culprit is the `hyperref` package, although I have not always had the problem.
I suppose the easiest course of action would be to change the name of the `\Ref` macro.
The problem seem to manifest in the current official version of the technical reference too
![Screenshot_2022-10-13_at_15.41.16](/uploads/4ba5b88c46d56aa1b54ac04de4eaee7c/Screenshot_2022-10-13_at_15.41.16.png)https://gitlab.mpi-sws.org/iris/iris/-/issues/50`contains` is named the wrong way around2017-01-14T21:53:11ZRalf Jungjung@mpi-sws.org`contains` is named the wrong way around``l1 `contains` l2`` confusing expresses that `l2` contains `l1`. Either the order of arguments should be changed, or the notation should be changed to e.g. `contained`.``l1 `contains` l2`` confusing expresses that `l2` contains `l1`. Either the order of arguments should be changed, or the notation should be changed to e.g. `contained`.Iris 3.0https://gitlab.mpi-sws.org/iris/iris/-/issues/157`done` loops in proofmode2018-03-07T18:16:58ZRobbert Krebbers`done` loops in proofmode```coq
Lemma test : ∃ R, R ⊢ ∀ P, P.
Proof. eexists. iIntros "?" (P). done.
``````coq
Lemma test : ∃ R, R ⊢ ∀ P, P.
Proof. eexists. iIntros "?" (P). done.
```Generalized Proofmode MergerRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/266`iDestruct 1` does not work when `Z_scope` is open2019-09-20T12:30:26ZJacques-Henri Jourdan`iDestruct 1` does not work when `Z_scope` is openIn this case, we have to write `iDestruct 1%nat`. It would be perfect to add the tactic notation for Z, too.In this case, we have to write `iDestruct 1%nat`. It would be perfect to add the tactic notation for Z, too.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/301`iExists` ignores `Opaque`2020-03-30T11:52:39ZPaolo G. Giarrusso`iExists` ignores `Opaque`Probably a WONTFIX, but this is new (presumably from !372), and Robbert asked for an example.
```coq
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import iprop.
Section foo.
Context `(Σ : gFunctors).
Defi...Probably a WONTFIX, but this is new (presumably from !372), and Robbert asked for an example.
```coq
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import iprop.
Section foo.
Context `(Σ : gFunctors).
Definition foo : iProp Σ := ∃ (x : nat), x ≡ 0.
End foo.
Opaque foo.
Lemma bar Σ : ⊢ foo Σ .
Proof.
by iExists 0. Restart.
iStartProof.
eapply coq_tactics.tac_exist.
Fail apply (class_instances_bi.from_exist_exist _).
(* The Hint Extern from !372: *)
notypeclasses refine (class_instances_bi.from_exist_exist _).
(* apply: (class_instances_bi.from_exist_exist _). (* Also works *) *)
by eexists 0.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/140`iIntoValid` failing in an unexpected way2019-12-03T12:34:58ZJacques-Henri Jourdan`iIntoValid` failing in an unexpected waySee e181f737.
I have no idea why these changes are needed to make the test pass. It seems like iIntoValid is failing in an unexpected way.See e181f737.
I have no idea why these changes are needed to make the test pass. It seems like iIntoValid is failing in an unexpected way.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/307`iIntros "%"` no longer works with universal quantification2020-04-07T15:39:37ZRalf Jungjung@mpi-sws.org`iIntros "%"` no longer works with universal quantificationThis test used to pass until yesterday, but got broken by !400:
```
Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_forall_pure P :
⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.
```
Cc @robbertkrebber...This test used to pass until yesterday, but got broken by !400:
```
Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_forall_pure P :
⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.
```
Cc @robbertkrebbers @tchajedhttps://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/225`is_closed_expr` is stronger than stability under `subst`2019-01-06T17:04:41ZDan Frumin`is_closed_expr` is stronger than stability under `subst`I think there is a discrepancy between the substitution and `is_closed_expr` for heap_lang
According to [subst](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lang.v#L400),
`subst x v' (of_val v) = of_val v`.
How...I think there is a discrepancy between the substitution and `is_closed_expr` for heap_lang
According to [subst](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lang.v#L400),
`subst x v' (of_val v) = of_val v`.
However, `is_closed_expr (of_val v) = is_closed_val v` (<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/metatheory.v#L22>) which is not always true.
That means, IIUC, that there are expressions that are not closed, but which are idempotent under the substitution.https://gitlab.mpi-sws.org/iris/iris/-/issues/299`leibnizO` finds convoluted proof for definitions2020-03-12T21:15:28ZRobbert Krebbers`leibnizO` finds convoluted proof for definitions```coq
Require Import iris.algebra.ofe.
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. rewrite /tagO /natO /tag. reflexivity.
(* Why doesn't this hold? *)
``````coq
Require Import iris.algebra.ofe.
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. rewrite /tagO /natO /tag. reflexivity.
(* Why doesn't this hold? *)
```Robbert KrebbersRobbert Krebbershttps://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.
```