Iris merge requestshttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests2024-10-31T16:11:09Zhttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1087Add requirement of mathpartir to pftools.sty2024-10-31T16:11:09ZIsaac van Bakelisaac.vanbakel@inf.ethz.chAdd requirement of mathpartir to pftools.styWithout this line, mathpartir.sty doesn't get pulled in to the document
despite being used for commands in pftools.sty, which is an annoyance.
I can't imagine wanting to use this file without the derivation stuff, so I expect this to not...Without this line, mathpartir.sty doesn't get pulled in to the document
despite being used for commands in pftools.sty, which is an annoyance.
I can't imagine wanting to use this file without the derivation stuff, so I expect this to not affect anyone who is trying to pull the non-mathpartir commands from the file without having the package available.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1085merge two fupd_plainly laws into one2024-11-03T20:06:09ZRalf Jungjung@mpi-sws.orgmerge two fupd_plainly laws into oneThis merges the two laws `fupd_plainly_mask_empty` and `fupd_plainly_keep_l` into a single law:
```
(** Given a mask-changing linear view shift ending in a plain proposition, and
given the precondition of the view shift, we can elimi...This merges the two laws `fupd_plainly_mask_empty` and `fupd_plainly_keep_l` into a single law:
```
(** Given a mask-changing linear view shift ending in a plain proposition, and
given the precondition of the view shift, we can eliminate the view shift
without consuming the precondition and without changing the mask. *)
fupd_plainly_keep_mask_l E E' (P R : PROP) :
(R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R;
```
IMO both of the previous laws showed some aspect of this, but there's only one underlying principle. This is also confirmed by the fact that the previous proof script for `fupd_plainly_keep_l` actually proves the new combined law without any changes (beyond introducing the new variable `E'`).
I decided to entirely remove the `fupd_plain(ly)_mask_empty` laws since one can just use `fupd_plain(ly)_mask` instead. `fupd_plainly_keep_{l,r}` are also gone since one can use `fupd_plainly_keep_mask_{l,r}` instead, but for `plain` (i.e. general `Plain` propositions rather than specifically the plainly modality) I kept the old lemma -- I expect these are the lemmas people actually use so we can have the shorter name.
That said, maybe we should just use `fupd_plainly_keep_{l,r}` as the name for the lemma with mask-changing updates? There's not a good reason I can think of to use the non-mask-changing one.
And finally I added a curried version of the lemma that should be easier to use with `iApply`:
```
Lemma fupd_plain_keep_mask E E' P R `{!Plain P} : (R ={E,E'}=∗ P) -∗ R -∗ |={E}=> P ∗ R.
```https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1082Use `refine` for `Frame` base cases.2024-10-10T08:47:50ZRobbert KrebbersUse `refine` for `Frame` base cases.This is an alternative for !916.
Instead of factoring out the uses of unification via a `Unify` type class with a single `Hint Extern`, this MR just turns the `iFrame` base instances into `Hint Extern`.
Would be useful to run timing to...This is an alternative for !916.
Instead of factoring out the uses of unification via a `Unify` type class with a single `Hint Extern`, this MR just turns the `iFrame` base instances into `Hint Extern`.
Would be useful to run timing to see if this does not suffer from the same performance problems as !916.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1078Add rule `own_forall` (base logic part of !1052)2024-10-31T07:14:25ZRobbert KrebbersAdd rule `own_forall` (base logic part of !1052)This MR is first half of !1052. It adds the rule `own_forall`, some of its corollaries, and the primitive `ownM_forall`.
For these part I refactored/shortened and improve the coding style of the proofs.
This MR does not contain the cha...This MR is first half of !1052. It adds the rule `own_forall`, some of its corollaries, and the primitive `ownM_forall`.
For these part I refactored/shortened and improve the coding style of the proofs.
This MR does not contain the changes to algebra and base_logic/lib from !1052.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1077Remove all uses of legacy `apply` in Proof Mode2024-10-10T08:32:45ZRobbert KrebbersRemove all uses of legacy `apply` in Proof ModeThis MR makes use of https://github.com/coq/coq/pull/13071, which is new in Coq 8.19. So Coq 8.18 can no longer be supported. Since we have the policy of supporting the last two Coq versions that would be OK.
This MR might make it possi...This MR makes use of https://github.com/coq/coq/pull/13071, which is new in Coq 8.19. So Coq 8.18 can no longer be supported. Since we have the policy of supporting the last two Coq versions that would be OK.
This MR might make it possible for the Coq devs to fix https://github.com/coq/coq/issues/6583, a bug which we accidentally used as a "feature".
It would be interesting to see timing and impact on reverse dependencies.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1061Use gmake for BSD systems2024-07-31T17:45:23ZYiyun LiuUse gmake for BSD systemsThis is the same PR as https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/559. The `make-package` script now checks whether the system is a BSD and if so uses `gmake` (GNU Make) instead of `make` to build the package since the latter...This is the same PR as https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/559. The `make-package` script now checks whether the system is a BSD and if so uses `gmake` (GNU Make) instead of `make` to build the package since the latter is incompatible with the GNU Makefiles generated by Coq.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1060Resolve conflicts between iris.sty and acmart2024-08-15T16:17:11ZRalf Jungjung@mpi-sws.orgResolve conflicts between iris.sty and acmart`\nequiv` and `\state` now both exist in acmart so we have to pick different names.
sed script for fixing documents:
```
sed -i -E -f- *.tex <<EOF
s/\\\nequiv\b/\\\dist/g
s/\\\nincl\b/\\\subseteqN/g
s/\\\notnequiv\b/\\\ndist/g
s/\\\nequ...`\nequiv` and `\state` now both exist in acmart so we have to pick different names.
sed script for fixing documents:
```
sed -i -E -f- *.tex <<EOF
s/\\\nequiv\b/\\\dist/g
s/\\\nincl\b/\\\subseteqN/g
s/\\\notnequiv\b/\\\ndist/g
s/\\\nequivset\b/\\\distset/g
s/\\\state\b/\\\ste/g
EOF
```https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1052Add `and_own` lemma for handling `own γ x ∧ own γ y`2024-09-24T16:31:28ZtjhanceAdd `and_own` lemma for handling `own γ x ∧ own γ y`The main purpose is to add the following result:
```coq
Lemma and_own (γ : gname) (x y : A) :
(own γ x ∧ own γ y) ⊢ ∃ z , own γ z
∗ Some x ≼ Some z
∗ Some y ≼ Some z.
```
The reason we use `Some x ≼ Some z` is be...The main purpose is to add the following result:
```coq
Lemma and_own (γ : gname) (x y : A) :
(own γ x ∧ own γ y) ⊢ ∃ z , own γ z
∗ Some x ≼ Some z
∗ Some y ≼ Some z.
```
The reason we use `Some x ≼ Some z` is because we need the comparison to be reflexive.
Here, the `≼` is defined to be an iProp version of the normal `≼`:
```coq
Definition uPred_cmra_included {Σ: gFunctors} {M: cmra} (a b : M) : iProp Σ := ∃ c , b ≡ a ⋅ c.
Infix "≼" := uPred_cmra_included (at level 70) : bi_scope.
```
We also prove some corollaries of `and_own`, e.g., for a discrete unital camera we have:
```coq
Lemma and_own_discrete_ucmra_specific {D : CmraDiscrete A} (γ : gname) (x y z : A) :
(∀ w , ✓ w → x ≼ w → y ≼ w → z ≼ w) →
(own γ x ∧ own γ y) ⊢ own γ z.
Lemma and_own_discrete_ucmra_contradiction {D : CmraDiscrete A} (γ : gname) (x y : A) :
(∀ w , ✓ w → x ≼ w → y ≼ w → False) →
(own γ x ∧ own γ y) ⊢ False.
```
All the new code is in `own.v`; I think the new `≼` should probably go somewhere else but I wasn't quite sure where.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1041Prevent iFrame from instantiating existentials under updates.2024-08-20T14:09:47ZJannoPrevent iFrame from instantiating existentials under updates.I think these cases were accidentally left out in !1035.
We've only just managed to get to most of our iris proofs in our 8.19 bump and didn't notice breakage from this omission earlier.
/cc @snyke7I think these cases were accidentally left out in !1035.
We've only just managed to get to most of our iris proofs in our 8.19 bump and didn't notice breakage from this omission earlier.
/cc @snyke7https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1020Do not use eta-expansion in `into_forall_forall`.2024-03-05T13:30:14ZRobbert KrebbersDo not use eta-expansion in `into_forall_forall`.This fixes #551.This fixes #551.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1008More documentation about _1 and _2 lemmas.2023-10-20T20:04:08ZRobbert KrebbersMore documentation about _1 and _2 lemmas.See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531#note_97838See discussion in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531#note_97838https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1007Add notations for `<affine> ⌜ ⌝` and friends.2023-10-17T08:11:01ZRobbert KrebbersAdd notations for `<affine> ⌜ ⌝` and friends.This MR adds the following notations:
- `⌜⌜ φ ⌝⌝` for `<affine> ⌜ φ ⌝`
- `⎡⎡ P ⎤⎤` for `<affine> ⎡ P ⎤`
- `x ≡≡ y` for `<affine> (x ≡ y)`
- `x ≼≼ y` for `<affine> (x ≼ y)`
So the idea is: doubling the symbol makes it affine. This shoul...This MR adds the following notations:
- `⌜⌜ φ ⌝⌝` for `<affine> ⌜ φ ⌝`
- `⎡⎡ P ⎤⎤` for `<affine> ⎡ P ⎤`
- `x ≡≡ y` for `<affine> (x ≡ y)`
- `x ≼≼ y` for `<affine> (x ≼ y)`
So the idea is: doubling the symbol makes it affine. This should also scale to `✓✓ x := <affine> (✓ x)`, once we have `✓` for any SBI.
I think this is a more feasible alternative to earlier discussions where we planned to make the ordinary notations the affine ones, because:
1. Most users of Iris don't use linear BIs, so the alternative would be an invasive change, whereas the current MR is trivial.
2. Many lemmas don't hold for the affine version. For example `f ≡ g ⊣⊢ ∀ x, f x ≡ g x` does not hold for `≡≡`. So if the affine version is the default, we need to duplicate all our lemmas, similar to how we have duplicated all lemmas for `<pers>` and `□`. This sounds like too much work for too little gain. In proofs with the present MR, you would typically move the affine version into the persistent context, thus stripping the affine modality, allowing you to use the lemmas for the non-affine version.
3. Some lemmas would need absorbing modalities for the affine versions. For example `own γ x ⊢ ✓ x` would not hold in an affine BI if `✓` where affine. (This example only applies once we have a general `own` and `✓`, there might be other examples in our current code-base already).
4. We support instances of `Embed` where `⎡ P ⎤` is affine and where it is not, so having `<affine> ⎡ _ ⎤` as the default would not be desired. For example, the embedding of `iProp` into `ironProp` is _not_ affine, so you often want to use `⎡⎡ P ⎤⎤`. However, if `BiEmbedEmp` holds, you want to use `⎡ P ⎤` (without affine modality), so that `⎡ P ⎤` is affine if `P` is affine.
**TODO:** Since there are not many uses of these new notations, we should add some tests. In particular, we should test that `⎡ ⎡ P ⎤ ⎤` is not pretty printed as `⎡⎡ P ⎤⎤`.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1004Add `IsOp` instances for `gset`, `coPset`, `gmultiset`2023-11-10T12:26:08ZIke MulderAdd `IsOp` instances for `gset`, `coPset`, `gmultiset`This MR adds `IsOp` instances for `gset`, `coPset` and `gmultiset`, and is part of the preparation for !930.
These `IsOp` instances make `iCombine` compute prettier results on `own`s of these `cmra`s.This MR adds `IsOp` instances for `gset`, `coPset` and `gmultiset`, and is part of the preparation for !930.
These `IsOp` instances make `iCombine` compute prettier results on `own`s of these `cmra`s.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/992Draft: Make sure that `?` in `iIntros`/`iDestruct` generate names that are not in the pattern2023-10-04T20:18:28ZRobbert KrebbersDraft: Make sure that `?` in `iIntros`/`iDestruct` generate names that are not in the patternSee https://mattermost.mpi-sws.org/iris/pl/samjaqqz8jb7fqepbcefxm47io where @jung wrote:
> We have another behavior change from the [ltac2 MR](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931):
> ```coq
> Lemma test_iDestruct1_...See https://mattermost.mpi-sws.org/iris/pl/samjaqqz8jb7fqepbcefxm47io where @jung wrote:
> We have another behavior change from the [ltac2 MR](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931):
> ```coq
> Lemma test_iDestruct1_pure (Φ: nat → PROP) :
> (∃ y z:nat, Φ y) -∗ ∃ x, Φ x.
> Proof.
> iDestruct 1 as (? y) "H".
> ```
> this now fails because the ? gets name y and then the later y says that the name is already used. it used to work fine, presumably because intros ? y actually does some form of lookahead and avoids picking the name y when a later pattern uses that name?
This MR fixes this issue. Thanks to @snyke7 for the Ltac2 hackery.
Reasons for WIP:
- `iIntros "(% & %y & ?)"` still fails on the same example. The problem is that we do not collect names from the Iris intro pattern. This should be simple to fix.
- We need to figure out where to put and how to name the Ltac2 stuff.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/980Avoid using specific `G` classes for locks, always use the projection `lockG` of `lock`.2023-08-30T09:52:55ZRobbert KrebbersAvoid using specific `G` classes for locks, always use the projection `lockG` of `lock`.This MR is a follow up of !979.
Always preferring the projections is similar to the way we use `acquire`/`release`/etc.
This MR also adjusts the `subG` instance to use `lockG` instead of `spin_lockG`, and tests that the conditions are ...This MR is a follow up of !979.
Always preferring the projections is similar to the way we use `acquire`/`release`/etc.
This MR also adjusts the `subG` instance to use `lockG` instead of `spin_lockG`, and tests that the conditions are resolved automatically when using adequacy.
TODO: I have only done this for spin lock, the same remains to be done for ticket lock, rw lock, atomic heap.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/972Draft: experiment: use coq's ability to infer more canonical structures2023-08-28T12:02:37ZRalf Jungjung@mpi-sws.orgDraft: experiment: use coq's ability to infer more canonical structuresI wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these `R`/`UR` terms from users. Unfortunately in one case already in this repo, it requires m...I wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these `R`/`UR` terms from users. Unfortunately in one case already in this repo, it requires more type annotations. I don't understand why Coq cannot infer that any more.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/971Draft: Attempted fix for #539, solving slow type-checking of nested `●` terms2023-08-28T20:24:30ZIke MulderDraft: Attempted fix for #539, solving slow type-checking of nested `●` termsAn attempt to fix #539. In summary, this MR:
- makes `auth` a `Definition`, instead of a `Notation`
- provides better `Canonical` instances for seeing `auth` as an `ofe`/`cmra`/`ucmra`. Previously, those of `view` were used, which can re...An attempt to fix #539. In summary, this MR:
- makes `auth` a `Definition`, instead of a `Notation`
- provides better `Canonical` instances for seeing `auth` as an `ofe`/`cmra`/`ucmra`. Previously, those of `view` were used, which can result in some very large terms.
- changes the definition of `ucmra` to an equivalent one, which ensures that the `ucmra_cmraR` coercion can compute fast on nested terms.
I believe all 3 changes are necessary to fix #539:
- The first two make it feasible to `Time Check (● (● (● (● (● (● (● (● (● (● (● (● (()))))))))))))).`
- The last one is necessary to get problems like the following to type check quickly
```
Time Lemma stack_frac_auths5 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) :
own γ1 (●F (●F (●F (●F (●F (to_agree n)))))) ⊢ own γ1 (●F (●F (●F (●F (●F (to_agree n)))))).
```
It additionally reverts !907 and instead registers a strategy that prevents unfolding `authR` and `authO`. Unfolding those would reveal the underlying `view` structure, which may cause an exponential blow-up in unification time.
I am quite interested in the timing for this MR, also for dependencies on Iris. The changes to `ucmra` might break stuff elsewhere, or make stuff slower.. in which case this might not be the way to go.
Also note that this MR uses the [`reversible` attribute](https://coq.inria.fr/refman/addendum/implicit-coercions.html#coq:attr.reversible), which means we need Coq 8.16.1+.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/953Draft: Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.2023-08-05T08:32:52ZRobbert KrebbersDraft: Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.This addresses https://gitlab.mpi-sws.org/iris/iris/-/issues/529 in part.
**TODO**: Use `_` prefix, but do that after !931 to avoid merge conflicts.This addresses https://gitlab.mpi-sws.org/iris/iris/-/issues/529 in part.
**TODO**: Use `_` prefix, but do that after !931 to avoid merge conflicts.https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/933Make bi fields non-canonical2023-10-13T14:37:45ZPaolo G. GiarrussoMake bi fields non-canonicalSuggested by @janno .Suggested by @janno .https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/930Draft: Improve validity information received from `iCombine`ing `own`s2023-11-10T12:26:50ZIke MulderDraft: Improve validity information received from `iCombine`ing `own`sDraft MR for addressing #251 and #460.
This is basically !771, but rebuilt on top of the `CombineSepAs` and `CombineSepGives` typeclasses from !872.
In the following environment:
```
"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet ...Draft MR for addressing #251 and #460.
This is basically !771, but rebuilt on top of the `CombineSepAs` and `CombineSepGives` typeclasses from !872.
In the following environment:
```
"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet E2)
```
executing `iCombine "Hγ1 Hγ2" as "Hγ" gives %[Hq HE]` will now replace "Hγ1" and "Hγ2" with a new hypothesis `"Hγ" : own γ (q1 + q2, GSet (E1 ∪ E2))` and two pure hypotheses: `Hq : q1 + q2 ≤ 1` and `HE : E1 ## E2`.
In the following environment:
```
"Hγ1" : own γ (◯ (Some (q1, GSet E1)))
"Hγ2" : own γ (● (Some (q2, GSet E2)))
```
executing `iCombine "Hγ1 Hγ2" gives %H` should give you a new pure hypotheses `H : q1 ≤ q2 ∧ E1 ⊆ E2 ∧ ((q1 < q2) ∨ (q1 ≡ q2 ∧ E1 ≡ E2))`.
It works by adding three typeclasses, `IsValidOp`, `IsValidGives` and `IsIncluded`, which try to determine an `iProp` that simplifies `✓` or `≼`. Since we are looking for an `iProp`, not a pure proposition, this approach also works for higher-order ghost state.
**Engineering questions:**
- The current approach does not simplify equivalences. If directly using rewrites in introduction patterns, this may cause slowdowns. Currently an explicit `%leibniz_equiv` on the equality is needed for faster rewrites. Fixing this would require an additional typeclass or some such for doing the simplification beforehand. For now, Robbert and I propose to leave this as such, and instead improve the `IntoPure` instance.
**Style/MR questions:**
- Does not yet have instances for all CMRA building blocks provided in `iris/algebra`, but at least supports the ones used inside the iris repository, and some others I have used in the past. How complete should this be?
- I needed some additional lemmas to simplify internal validity of e.g. `viewR`. Should these be upstreamed in a separate MR? They might not very nicely mesh with Robberts `siProp`, since they lift the `view_rel` to the logic, which only works for `uPred` currently.
**TODO:**
- Documentation is missing
- Tests are still missing
- List CMRA building blocks for which support is missing
- I added additional `IsOp` instances for `gset`, `gmultiset` and `gmap`, need to wait for MR !1004.
- ~~I added some lemmas about `IdFree` at the logic level, need to wait for MR !1005~~.
- ~~I added additional `MakeOr` instances for simplifying e.g. `False ∨ P`, need to wait for MR !940~~.
- ~~I am using `∗-∗` in `IsIncluded` to make sure I'm not dropping information. I sometimes make use of the transitivity of this, need to wait for MR !941.~~
- ~~I needed some additional lemmas to simplify internal validity of e.g. `dfracR` and `authR`, need to wait for MR !942.~~
- ~~Improve the `IntoPure` instance for leibniz equivalences in a separate MR, need to wait for MR !966~~.
- ~~Add `≼` on the BI level, need to wait for !944.~~
- ~~Remove `reservation_map` support for now.~~
Feedback is most welcome!