Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2016-11-24T09:29:23Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/3Prove adequacy of observational view shifts2016-11-24T09:29:23ZRalf Jungjung@mpi-sws.orgProve adequacy of observational view shiftsProve an adequacy theorem that uses an observational view shift to establish that all the physical states during the execution of a program satisfy some property.
@swasey If you still want to do this, assign this issue to yourself, pl...Prove an adequacy theorem that uses an observational view shift to establish that all the physical states during the execution of a program satisfy some property.
@swasey If you still want to do this, assign this issue to yourself, please.
One thing I have been wondering is whether this result should/could somehow be generalized to the case where some *code* has to run before the invariant we talk about is actually established. I think I have some idea(s) here, that should be fleshed out on a whiteboard.David SwaseyDavid Swaseyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/12Prove stronger stepping frame rule2016-08-22T15:55:51ZRalf Jungjung@mpi-sws.orgProve stronger stepping frame ruleRight now, we have a "stepping frame rule" that looks as follows:
```text
{ P } e { Q } e is not a value
------------------------------------
{ \later R * P } e { R * Q }
```
Essentially, this allows us to step away a later ...Right now, we have a "stepping frame rule" that looks as follows:
```text
{ P } e { Q } e is not a value
------------------------------------
{ \later R * P } e { R * Q }
```
Essentially, this allows us to step away a later when framing around any non-value. (We also sometimes call this the "atomic frame rule", since atomic expressions are never values. But the one above is just as valid, and obviously stronger.)
However, I think I will need for my Rust stuff a stronger version of this rule, that allows me to strip away a later *inside an invariant* from any non-value. This comes up because I have non-atomic reads and writes that are, well, non-atomic, and I still want to strip away a later from something that is located inside an invariant[1]. This rule is rather awkward to write down in terms of Hoare triples and view shifts:
```text
R0 E1^==>^E2 \later R1 R1 E2^==>^E1 R2 { P } e { Q }_E1
e is not a value E2 <= E1
------------------------------------------------------------------
{ R0 * P } e { R2 * Q }_E1
```
It looks nicer in terms of primitive view shifts and weakest-pre:
```text
wp_E1 e Q * vs_E1^E2(\later vs_E2^E1(R))
e is not a value E2 <= E1
-------------------------------------
wp_E1 e (Q * R)
```
When we re-do the weakest-pre proofs for V2.0, I think this is the rule we should show. (And derive the old one, of course.)
[1] If you are curious: The invariant has two states "vs(P)" and "P", with an STS making sure that one can only go from the 1st state to the 2nd. The rule I need allows me to open this invariant alongside the non-atomic access, obtain "\later (vs(P) \/ P)", strip away the later, view shift to "P", and put that back into the invariant; taking out the witness that the view shift has been performed. I do not need any resource from the invariant to justify the memory access, so it's fine for that one to be non-atomic. But I *do* need to perform this view shift, because immediately after the access I will want to open the invariant again and know I get "\later P", without any more skips.
Cc: @robbertkrebbers @swasey @janno https://gitlab.mpi-sws.org/iris/iris/-/issues/373Quote does not handle ⊣⊢2020-11-05T11:12:30ZRodolphe LepigreQuote does not handle ⊣⊢The `solve_sep_equiv` tactic from `bi.tactics` cannot be used to solve goals of the form `_ ⊣⊢ _`.
This is due to `quote` only accepting goals of the form `_ ⊢ _` (see [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/b...The `solve_sep_equiv` tactic from `bi.tactics` cannot be used to solve goals of the form `_ ⊣⊢ _`.
This is due to `quote` only accepting goals of the form `_ ⊢ _` (see [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/tactics.v#L136)). Can it be made more general?https://gitlab.mpi-sws.org/iris/iris/-/issues/4Re-do the basics: Cofe's and (CM)RA's2016-01-18T16:38:26ZRalf Jungjung@mpi-sws.orgRe-do the basics: Cofe's and (CM)RA'sSlim down the algebraic hierarchy to contain only Cofe's, RA's and CMRA's, all as unbundled typeclasses and bundled canonical structures. Instead of a general notion of monotone function, we only really need one functor that maps a CMRA ...Slim down the algebraic hierarchy to contain only Cofe's, RA's and CMRA's, all as unbundled typeclasses and bundled canonical structures. Instead of a general notion of monotone function, we only really need one functor that maps a CMRA to monotone, step-indexed predicates over that CMRA. Maybe call that uPred? THat's kind of what it is, though it's not the same uPred that we had originally - that one could only deal with RA's.
Then we don't need the notion of a canonical partial order on a type - often, it's not even clear which one that should be. This also gives us the opportunity to define the metric and order on that uPred such that we can have "own(a) => valid(a)" as opposed to right now, where we have "own(a) \vs valid(a)". It's not entirely clear yet though if that latter part will actually work out without significant pain.Robbert KrebbersRobbert Krebbershttps://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/38Refactor bigops2017-04-01T19:10:03ZRalf Jungjung@mpi-sws.orgRefactor bigopsCurrently, bigops are tied to CMRAs. This is silly, because it means we have to show extension for e.g. uPred (which so far we can only do after picking a silly validity), and also because it restricts us to pick *one* operator to be use...Currently, bigops are tied to CMRAs. This is silly, because it means we have to show extension for e.g. uPred (which so far we can only do after picking a silly validity), and also because it restricts us to pick *one* operator to be used in bigops, whereas we may also want to use big conjunction.
Instead we should do sth. like ssreflect does, with a typeclass/canonical structure for this special purpose that's completely separate from the main algebraic hierarchy.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/274Regression after !329 on recursive proofs2019-12-02T14:10:16ZPaolo G. GiarrussoRegression after !329 on recursive proofsHere's a self-contained testcase:
```coq
From iris.proofmode Require Import tactics.
Section testcase.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Fixpoint test_fixpoint (n : nat) {struct n} : emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
...Here's a self-contained testcase:
```coq
From iris.proofmode Require Import tactics.
Section testcase.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Fixpoint test_fixpoint (n : nat) {struct n} : emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
Proof.
case: n => [|n] /=.
- iIntros "_ !%". reflexivity.
- iIntros "_".
(* Works *)
(* by iDestruct (test_fixpoint n with "[//]") as %->. *)
(* Fails *)
by iDestruct (test_fixpoint with "[//]") as %->.
Qed.
```
This testcase is silly, but recursive proofs for mutually recursive lemmas can make sense, especially when the proof uses a custom induction scheme that is only used once: proving it by hand has advantages, especially for automation, but can create more boilerplate than a recursive proof.
I tried out a suggestion from @robbertkrebbers, got it to work and will send a MR shortly, but I expect the result should be achieved otherwise.https://gitlab.mpi-sws.org/iris/iris/-/issues/533Regression from !931 : applying some lemmas in iIntros using intro patterns b...2023-08-04T08:14:01ZMichael SammlerRegression from !931 : applying some lemmas in iIntros using intro patterns breaksWhen porting DimSum to !931, I encountered a regression with the n-ary iTactics MR: The following code used to work, but now it gives an error "Error: Tactic failure: iStartProof: not a BI assertion.":
```
From iris.base_logic Require Ex...When porting DimSum to !931, I encountered a regression with the n-ary iTactics MR: The following code used to work, but now it gives an error "Error: Tactic failure: iStartProof: not a BI assertion.":
```
From iris.base_logic Require Export iprop.
From iris.proofmode Require Export tactics.
Lemma test {Σ} (m : gmap nat nat) i x :
⊢@{iProp Σ} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True.
Proof. iStartProof. iIntros (?%lookup_kmap_Some).
```
My suspicion is that this has to do with the `Inj` argument of `lookup_kmap_Some` and that some pure subgoal gets created for it where `iIntros` then fails.
The following variant works
```
From iris.base_logic Require Export iprop.
From iris.proofmode Require Export tactics.
Lemma test {Σ} (m : gmap nat nat) i x :
⊢@{iProp Σ} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True.
Proof. iStartProof. iIntros (?%(lookup_kmap_Some _)).
```https://gitlab.mpi-sws.org/iris/iris/-/issues/534Regression from !931 : iRevert used by iInduction is broken2023-08-04T08:15:00ZMichael SammlerRegression from !931 : iRevert used by iInduction is brokenWhen porting RefinedC to !931, I noticed that the following code now gives the error `Error: Tactic failure: iRevert: l2 is used in hypothesis "Himpl".`, while it used to work before:
```coq
From iris.algebra Require Export big_op.
From ...When porting RefinedC to !931, I noticed that the following code now gives the error `Error: Tactic failure: iRevert: l2 is used in hypothesis "Himpl".`, while it used to work before:
```coq
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' (PROP:bi) {A B} Φ (Ψ : _ → B → PROP) (l1 : list A) (l2 : list B) :
□ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros "#Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2).
```
A workaround seems to be to keep `Himpl` in the spatial context.
EDIT: The following code was always broken as noticed by Robbert:
```coq
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' {PROP : bi} {A B} (l1 : list A) (l2 : list B) :
⊢@{PROP} □ (∀ k x2, ⌜l2 !! k = Some x2⌝ -∗ True) -∗
True.
Proof. iIntros "#Himpl". iInduction l1 as [|x1 l1] "IH" forall (l2).
```https://gitlab.mpi-sws.org/iris/iris/-/issues/492Regression of [iSpecialize] and related tactics.2022-10-31T09:52:05ZRodolphe LepigreRegression of [iSpecialize] and related tactics.I noticed the following regression.
```coq
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Goal forall (PROP : bi) (P Q : PROP), (∀ (_ : tt = tt), Q) ⊢@{PROP} P.
Proof.
iIntros (???) "H".
Fail iSpecial...I noticed the following regression.
```coq
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Goal forall (PROP : bi) (P Q : PROP), (∀ (_ : tt = tt), Q) ⊢@{PROP} P.
Proof.
iIntros (???) "H".
Fail iSpecialize ("H" with "[%]"). (* Used to work before, now fails with: *)
(* Tactic failure: iSpecialize: (Forall _ : () = (), Q) not an implication/wand. *)
(* Possible (and maybe even desired) alternative (probably also worked before): *)
unshelve iSpecialize ("H" $! _).
all: done.
Qed.
```
The first `iSpecialize` pattern above was used to work with `coq-iris.dev.2022-05-04.0.10e843d9`, and it fails with `coq-iris.dev.2022-09-29.0.b335afaf` (and probably on `master`. I also reported this in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/799#note_85201, which I think introduced the regression (cc @jung).https://gitlab.mpi-sws.org/iris/iris/-/issues/254Reliance on `Export` bug2019-11-01T12:48:48ZMaxime DénèsReliance on `Export` bugDear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is...Dear Iris developers,
I'm trying to make Iris not depend on the following Coq bug: https://github.com/coq/coq/issues/10480
Unfortunately, it impacts the handling of canonical structures in Iris, which I'm not sure how to fix.
There is an easy way to observe the problem on Coq master: take `algebra.ufrac_auth`, and change the first line:
```coq
From iris.algebra Require Export auth frac.
```
into:
```coq
From iris.algebra Require Export auth.
From iris.algebra Require Export frac.
```
it will make the proof of `ufrac_auth_agreeN` fail because a view starts applying in the wrong direction...
Could you provide some guidance on how to make the file pass with the two separate `Export`s? It will probably make it compatible with the fix of the bug I mentioned above.
Thanks!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/121Remove `bi_persistently_exist_1` and `bi_plainly_exist_1` from the BI axioms2018-03-19T11:01:03ZJacques-Henri JourdanRemove `bi_persistently_exist_1` and `bi_plainly_exist_1` from the BI axiomsThey possibly not hold for linear logics.They possibly not hold for linear logics.Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/218Remove duplicate abstraction2018-10-29T13:32:07ZGhost UserRemove duplicate abstractionIn https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/proofmode/class_instances_bi.v#L13, with respect to the following three `Global Instance` declarations.
`PROP` is already abstracted as a section variable, and the extra gen...In https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/proofmode/class_instances_bi.v#L13, with respect to the following three `Global Instance` declarations.
`PROP` is already abstracted as a section variable, and the extra generality is not used.
Removing `{PROP : bi}` here is needed for compatibility with coq/coq#8820.https://gitlab.mpi-sws.org/iris/iris/-/issues/285Remove eta-expansions from sealed definitions2020-08-30T09:53:12ZRalf Jungjung@mpi-sws.orgRemove eta-expansions from sealed definitionsAs discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/352#note_42913), we plan to remove all eta-expansions from sealed definitions. That makes the unfolding `rewrite` more widely applicable.As discussed [here](https://gitlab.mpi-sws.org/iris/iris/merge_requests/352#note_42913), we plan to remove all eta-expansions from sealed definitions. That makes the unfolding `rewrite` more widely applicable.https://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/122Rename `AffineBI` and `PositiveBI`2017-12-04T18:34:10ZRobbert KrebbersRename `AffineBI` and `PositiveBI`These should be named `BiAffine` and `BiPositive` to follow the naming scheme we use elsewhere, e.g. for `OfeDiscrete` and `Cmra...`.These should be named `BiAffine` and `BiPositive` to follow the naming scheme we use elsewhere, e.g. for `OfeDiscrete` and `Cmra...`.https://gitlab.mpi-sws.org/iris/iris/-/issues/119Rename bi_later → sbi_later2017-12-04T21:22:48ZRobbert KrebbersRename bi_later → sbi_laterBy @jjourdan: is there a reason why `bi_later` is not called `sbi_later`? Likewise for except_0By @jjourdan: is there a reason why `bi_later` is not called `sbi_later`? Likewise for except_0https://gitlab.mpi-sws.org/iris/iris/-/issues/472Rename laterN_plus into laterN_add2022-08-09T21:19:10ZRobbert KrebbersRename laterN_plus into laterN_addThe following discussion from !808 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/808#note_82564): (+1 comment)
> Hmm, we already have:
>
> ```
...The following discussion from !808 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/808#note_82564): (+1 comment)
> Hmm, we already have:
>
> ```
> Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
> ```
>
> So, with plus instead of add.
>
> Since the new convention in Coq is to use add, maybe the laterN lemma should be renamed?https://gitlab.mpi-sws.org/iris/iris/-/issues/495Rename mapsto to pointsto2023-11-06T20:01:38ZRalf Jungjung@mpi-sws.orgRename mapsto to pointstoIris calls it `mapsto` because... reasons and someone got confused by LaTeX. But it's called points-to in the literature, and we should probably stop confusing people and rename this in Iris.Iris calls it `mapsto` because... reasons and someone got confused by LaTeX. But it's called points-to in the literature, and we should probably stop confusing people and rename this in Iris.