Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-09-09T12:29:51Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/339Add "reservation map" CMRA2020-09-09T12:29:51ZRalf Jungjung@mpi-sws.orgAdd "reservation map" CMRAFor the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an i...For the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?https://gitlab.mpi-sws.org/iris/iris/-/issues/123Add a general constructor from an affine BI2019-11-01T13:24:47ZRalf Jungjung@mpi-sws.orgAdd a general constructor from an affine BIIn master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just...In master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just claims them to be `(ADMISSIBLE)` in a comment.
I see two ways to achieve that:
* We could provide a general way to construct a `BiMixin` from a proof of all the laws given in the appendix.
* We could do the more specific thing and first prove the appendix laws for `uPred`, and subsequently not use `unseal` when proving the `BiMixin`.https://gitlab.mpi-sws.org/iris/iris/-/issues/244Add a general lattice RA to Iris2020-12-10T16:56:05ZRalf Jungjung@mpi-sws.orgAdd a general lattice RA to IrisHistories as monotonically growing lists are something that comes up every now and then, and it can be quite annoying to formalize. I believe we have something like that already in GPFSL, based on a general framework of (semi-) lattices....Histories as monotonically growing lists are something that comes up every now and then, and it can be quite annoying to formalize. I believe we have something like that already in GPFSL, based on a general framework of (semi-) lattices. We should have that RA in Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/391Add append-only list RA to Iris2021-05-17T16:32:27ZRalf Jungjung@mpi-sws.orgAdd append-only list RA to IrisAppend-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize l...Append-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote [a version of this](https://gitlab.mpi-sws.org/iris/gpfsl/-/blob/graphs/theories/examples/list_cmra.v), which was forked at some point by @jtassaro [for Perennial](https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v) while also adding a logic-level wrapper for `auth (mlist T)` with the following three core assertions:
* authoritative ownership of the full trace
* persistent ownership that some list is a prefix of the trace
* persistent ownership that index i in the trace has some particular value
Perennial also has [another version of this](https://github.com/mit-pdos/perennial/blob/master/src/algebra/append_list.v) by @tchajed that is based on (the Perennial version of) `gmap_view`. And finally, @msammler has [his own implementation](https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18) that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/431Add generalized implication lemma for sets, etc.2021-07-29T07:29:12ZSimon Friis VindumAdd generalized implication lemma for sets, etc.!697 adds stronger variants of `big_sepM_impl`. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
```coq
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X...!697 adds stronger variants of `big_sepM_impl`. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
```coq
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X1 X2 :
([∗ set] x ∈ X1, Φ k x) -∗
□ (∀ (x : X),
⌜x ∈ X2⌝ →
((⌜x ∈ X1⌝ ∧ Φ x) ∨ <affinely> ⌜x ¬∈ X1⌝) -∗
Ψ x) -∗
([∗ set] y ∈ X2, Ψ y) ∗
([∗ set] x ∈ X1∖X2, Φ x).
```https://gitlab.mpi-sws.org/iris/iris/-/issues/449Add internalised rules for derived resource algebras2022-03-04T00:38:47ZJonas KastbergAdd internalised rules for derived resource algebrasWorking with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of `auth`, which have `auth_both_valid` (in ...Working with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of `auth`, which have `auth_both_valid` (in the model), `auth_both_validN` (in the model, with step-indices), and `auth_both_validI` (in the logic).
Some derived resource algebras are missing their "internalised rules" (those of the logic).
This issue is then to address the lack of these rules.
One example of a resource algebra with missing rules are `mono_list`.
In full, to solve this issue we should:
- Identify all resource algebras with missing internalised rules
- Add the missing rules
- (Settle on a potential pipeline for future algebras to ensure that the rules are included)https://gitlab.mpi-sws.org/iris/iris/-/issues/517Add notion of "allowed to be stuck" terms to WP2023-03-20T12:34:43ZRalf Jungjung@mpi-sws.orgAdd notion of "allowed to be stuck" terms to WPFor some languages it makes sense to distinguish two kinds of "stuck" terms (terms that cannot take a step and aren't a value): some are "bad" and some are "good". For instance, this can be used to model a "halt the program" primitive (t...For some languages it makes sense to distinguish two kinds of "stuck" terms (terms that cannot take a step and aren't a value): some are "bad" and some are "good". For instance, this can be used to model a "halt the program" primitive (though it will only halt the current thread due to the fixed threadpool semantics). Possibly this could also be used to model "blocking" operations.
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/825 started implementing this, but did not get completed. Still some discussion we had around that MR should be taken into account when another attempt is made at implementing this feature, in particular the [proposal for naming things](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/825#note_83734).https://gitlab.mpi-sws.org/iris/iris/-/issues/569Add some sort of rule for `own ∧ own`2024-03-24T14:54:23ZRalf Jungjung@mpi-sws.orgAdd some sort of rule for `own ∧ own`The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v)...The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v).)
Amin suggested [something similar](https://mattermost.mpi-sws.org/iris/pl/tcsex43cn7d5ij5qwkk39ftd7h) a long time ago.
Not sure which formulation works best, but we should have something like that. :)
Whatever the rule is, it should be strong enough to prove things like
```
Lemma pointsto_and_sep (l1 l2:loc) (v1 v2:val) :
l1 ≠ l2 ->
l1 ↦ v1 ∧ l2 ↦ v2 -∗
l1 ↦ v1 ∗ l2 ↦ v2.
Lemma pointsto_and_eq l x y :
l ↦ x ∧ l ↦ y -∗ ⌜x = y⌝
```https://gitlab.mpi-sws.org/iris/iris/-/issues/498Add support for more tactics in spec patterns2022-11-24T20:53:20ZRalf Jungjung@mpi-sws.orgAdd support for more tactics in spec patternsOur spec patterns support `//`, but sometimes one wants to use other tactics -- most frequently `eauto with iFrame`. Would be nice to have time way to support them.
Ssreflect itself has 10 numbered patterns (not entirely sure about the ...Our spec patterns support `//`, but sometimes one wants to use other tactics -- most frequently `eauto with iFrame`. Would be nice to have time way to support them.
Ssreflect itself has 10 numbered patterns (not entirely sure about the syntax for those -- @blaisorblade?) and `/[name]` for named patterns (not sure what the syntax is for declaring one).https://gitlab.mpi-sws.org/iris/iris/-/issues/371Add validI lemmas for discrete RAs2020-11-05T08:41:29ZRalf Jungjung@mpi-sws.orgAdd validI lemmas for discrete RAsOur discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the `...Our discrete RAs lack "validI" lemmas that reflect their validity into an equivalent logical statement. Those are rarely needed because whenever one uses the proof mode, one can just turn validity into a Coq assumption and then use the `Prop`-level lemmas. But e.g. when proving equivalences, it can be useful to have a way to rewrite validity into an equivalent logical statement.
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/558 added the lemma for frac, but other RAs are still missing:
* [ ] `gset_disj`
* [ ] `coPset`, `coPset_disj`
* [ ] `sts`
* [ ] `dfrac`https://gitlab.mpi-sws.org/iris/iris/-/issues/487Adding pointer order comparison to HeapLang2022-10-14T19:33:59ZArthur Azevedo de AmorimAdding pointer order comparison to HeapLangAs the following file shows, HeapLang makes it possible to compare pointers for their relative ordering. Should we extend the primitive comparison operation on HeapLang to work on pointers as well?
[pointer_comparison.v](/uploads/f638e4...As the following file shows, HeapLang makes it possible to compare pointers for their relative ordering. Should we extend the primitive comparison operation on HeapLang to work on pointers as well?
[pointer_comparison.v](/uploads/f638e4e4e81b856b5be629e623fe608f/pointer_comparison.v)https://gitlab.mpi-sws.org/iris/iris/-/issues/478Adding satisfiable to Iris2022-08-17T05:24:37ZSimon SpiesAdding satisfiable to IrisSeveral Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notio...Several Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notion of `satisfiable` can be added to Iris in a meaningful way and whether it can enable more modular adequacy proofs in the future.https://gitlab.mpi-sws.org/iris/iris/-/issues/286Address the STS encodings lack of usefulness2020-01-30T21:32:04ZJonas KastbergAddress the STS encodings lack of usefulnessThe current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "ve...The current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".
Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out.
Going forward we should do either of the following:
- Include a disclaimer discouraging people from using them
- Remove the encoding from the repository
- Update the implementation to be more user-friendly
I suggest doing either of the first two short-term and then possibly look into the third long-term.
It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.https://gitlab.mpi-sws.org/iris/iris/-/issues/348Always enabled invariants2020-09-30T19:14:58ZRalf Jungjung@mpi-sws.orgAlways enabled invariants@jtassaro has a fork of Iris with some interesting features that we might want to copy. In particular, for Perennial he added "always-enabled invariants", which have no mask, can always be opened, but cannot be kept open. The accessor le...@jtassaro has a fork of Iris with some interesting features that we might want to copy. In particular, for Perennial he added "always-enabled invariants", which have no mask, can always be opened, but cannot be kept open. The accessor lemma is (roughly):
```
Lemma ae_inv_acc_bupd E P Q :
ae_inv P -∗
(▷ P ==∗ ◇ (▷ P ∗ Q)) -∗
|={E}=> Q.
```
This seems like it could be useful beyond Perennial. In particular, this forms a layer of abstraction *beneath* the invariants that we have: `ownI` (underlying `inv`) can be defined in terms of `ae_inv` with something like
```
ownI i Q := Q ∗ ownD {[i]} ∨ ownE {[i]})
```
(That's not how Joe defined them, but I am pretty sure it could be done.)https://gitlab.mpi-sws.org/iris/iris/-/issues/169Applying plain implications fails2019-11-01T12:51:28ZRalf Jungjung@mpi-sws.orgApplying plain implications failsHere's two testcases, both fail currently:
```coq
Lemma test_apply_affine_wand2 `{!BiPlainly PROP} (P : PROP) :
P -∗ (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q).
Proof. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ"...Here's two testcases, both fail currently:
```coq
Lemma test_apply_affine_wand2 `{!BiPlainly PROP} (P : PROP) :
P -∗ (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q).
Proof. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
Lemma test_apply_affine_impl2 `{!BiPlainly PROP} (P : PROP) :
P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).
Proof. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/308Automatically enforce use of Unicode → instead of ASCII ->2020-04-16T19:10:02ZTej Chajedtchajed@gmail.comAutomatically enforce use of Unicode → instead of ASCII ->Iris can check (at least approximately) for new uses of -> in a pre-commit hook to enforce this style. This should save @robbertkrebbers several hours of writing "Please use Unicode →" in MRs.
Here's my attempt at this. To install, you ...Iris can check (at least approximately) for new uses of -> in a pre-commit hook to enforce this style. This should save @robbertkrebbers several hours of writing "Please use Unicode →" in MRs.
Here's my attempt at this. To install, you need to copy this file to `.git/hooks/pre-commit` and make it executable.
This was tested on macOS with BSD grep, but it should be cross-platform.
```sh
#!/bin/bash
set -e
# redirect stdout to stderr
exec 1>&2
error() {
echo -e "\033[31m$1\033[0m"
}
## Check for adding ASCII -> instead of Unicode →
# first filter to Coq files not containing "ascii"
if find . -name '*.v' -and -not -name '*ascii*' -print0 |\
xargs -0 git diff --staged --unified=0 -- |\
# only check additions, not deletions
grep '^\+.*->' |\
# skip lines that legitimately use -> in Ltac
grep -v '\b(rewrite|destruct|iDestruct|iMod)\b.*->'
then
error "Please use Unicode [→] instead of [->]."
exit 1
fi
```
Note that this doesn't need to be perfect. You can always override the check with `git commit --no-verify`.
I can also add checks for `\bexists\b`, `\bforall\b`, and `\bfun\b` that should be replaced with their Unicode variants `∃`, `∀`, and `λ`.https://gitlab.mpi-sws.org/iris/iris/-/issues/529Avoid `Local Ltac` and `Local Tactic Notation`2023-09-14T16:04:32ZRobbert KrebbersAvoid `Local Ltac` and `Local Tactic Notation`There appears to be no way to call such tactics outside of the module, making debugging very difficult.
For `Local Ltac`, I think this is a Coq bug, see https://github.com/coq/coq/issues/17884
For `Local Tactic Notation`, I think it's ...There appears to be no way to call such tactics outside of the module, making debugging very difficult.
For `Local Ltac`, I think this is a Coq bug, see https://github.com/coq/coq/issues/17884
For `Local Tactic Notation`, I think it's inherently broken since `Tactic Notation` extends the grammar.https://gitlab.mpi-sws.org/iris/iris/-/issues/374Avoid sequences of "_" by adjusting lemma statements2020-11-05T12:11:02ZRalf Jungjung@mpi-sws.orgAvoid sequences of "_" by adjusting lemma statementsSome Iris lemmas are prone to needing plenty of `_` almost every time they are used. I noticed this in particular for
* most big-op lemmas that access a single element, where the to-be-accessed element needs to be given explicitly, but o...Some Iris lemmas are prone to needing plenty of `_` almost every time they are used. I noticed this in particular for
* most big-op lemmas that access a single element, where the to-be-accessed element needs to be given explicitly, but often other arguments come first
* several allocation lemmas such as `inv_alloc`, where the to-be-allocated thing needs to be given explicitly, but other arguments come first
* many of the update lemmas, where typically one works with `iMod`, so the new values (e.g. new lower bound for mono_nat, or new key and value for gmap) need to be given, but they are often the last arguments
There are two ways to fix this:
* reorder arguments, so that those that are likely to be determined by unification come first
* make likely-to-be-determined-by-unification arguments implicit, so that we do not have to write out their `_`
I am in favor of the second approach because it has a better failure mode: if one of those arguments ends up *not* being determined by unification, we have use `lemma (arg:=val)` to explicitly give the value for this agument. For lemmas with many arguments, this name-based approach is anyway much easier to read and write than the position-based approach (no need to remember the exact order of arguments).
However, while implicit arguments are widely used in Iris, we usually control them on a per-section basis, not a per-lemma basis. @robbertkrebbers has objected the used of implicit arguments for this reason. (That is my understanding, anyway.)https://gitlab.mpi-sws.org/iris/iris/-/issues/243Avoid type-level aliases for overloading of canonical structures2019-11-01T13:05:35ZRobbert KrebbersAvoid type-level aliases for overloading of canonical structuresIn https://gitlab.mpi-sws.org/iris/iris/merge_requests/187#note_36185 @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
> I have to say that I really don't like the idea of overloading a...In https://gitlab.mpi-sws.org/iris/iris/merge_requests/187#note_36185 @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
> I have to say that I really don't like the idea of overloading a canonical structure for a type... Why cannot we define `ufrac` as something like: `Record ufrac := uf_qp { qp_uf : Qp }.`? Sure, this will require some boilerplate for projecting and boxing fractions, but hoping that such hack will keep a stable behaviors seems rather optimistic!
This applies to `ufrac` (introduced in !195) and `mnat` (introduced a long time ago).https://gitlab.mpi-sws.org/iris/iris/-/issues/165Better (?) approach to control typeclass resolution based on whether some arg...2019-11-01T13:33:12ZRalf Jungjung@mpi-sws.orgBetter (?) approach to control typeclass resolution based on whether some arguments are evarsRight now, some of our typeclasses have extra variants called `KnownXXX` that use `Hint Mode` to only apply when certain arguments are not evars. This has lead to an explosion in the number of typeclasses.
Maybe a better approach would...Right now, some of our typeclasses have extra variants called `KnownXXX` that use `Hint Mode` to only apply when certain arguments are not evars. This has lead to an explosion in the number of typeclasses.
Maybe a better approach would be to change the way we write some instances, and make sure they can only succeed if some arguments are not evars. I described such a solution at <https://gitlab.mpi-sws.org/FP/iris-coq/commit/a9d41b6374f44fd93629f99cfecfea3549baa0b1#note_25278>.
One possible concern is that applying such instances should fail as early as possible; if they have other premises, those shouldn't be resolved unless the evar check passes. On the other hand, the `KnownXXX` classes introduce additional coercions that typeclass resolution will try all the time, which could also be a performance issue.