Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2023-07-25T18:58:19Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/916`Unify` type class that factors out use of `notypeclasses refine` in proof mo...2023-07-25T18:58:19ZRobbert Krebbers`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.This has the following advantages:
- We need fewer adhoc `Hint Extern` instances for the proof mode, we can just use `Unify`.
- We can consistently use the `refine` unification algorithm when trying to unify a hypothesis/conclusion of a...This has the following advantages:
- We need fewer adhoc `Hint Extern` instances for the proof mode, we can just use `Unify`.
- We can consistently use the `refine` unification algorithm when trying to unify a hypothesis/conclusion of a lemma/wand to the goal. This is currently only done by `iAssumption`, but not by `iFrame` or `iApply`.
- It might allow us to use `Typeclasses Opaque` for all std++ operational type classes. As described in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/914#note_91480, this is currently impossible.
We could probably do some bikeshedding about the name or other implementation aspects. But I might make sense to first check out the performance impact and whether it breaks anything in the reverse dependencies. So @jung could you run timing CI, please.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/851Renamed/added macros to iris.sty2023-07-25T18:54:46ZJonas KastbergRenamed/added macros to iris.stySome suggested changes to the `iris.sty` file to make it more up-to-date with current uses.Some suggested changes to the `iris.sty` file to make it more up-to-date with current uses.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/847Add comments to explain the modified structure of the adequacy proof2023-02-01T15:14:28ZSimon SpiesAdd comments to explain the modified structure of the adequacy proofThis MR adds comments to Iris's adequacy proof to explain why we "run adequacy" twice.This MR adds comments to Iris's adequacy proof to explain why we "run adequacy" twice.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/825Allow controlling stuckness at the language level2023-03-20T13:42:12ZMichael SammlerAllow controlling stuckness at the language levelCurrently, the safety result of Iris is that each expression is either a value or can reduce. However, there are cases where one wants to have expressions that are not values but also cannot reduce (e.g. when modelling untrusted code tha...Currently, the safety result of Iris is that each expression is either a value or can reduce. However, there are cases where one wants to have expressions that are not values but also cannot reduce (e.g. when modelling untrusted code that is allowed to get stuck or for modeling "no behavior"). Currently, Iris provides the `MaybeStuck` WP which does not require proving safety. However, using `MaybeStuck` is very coarse grained: If any part of the program uses the `MaybeStuck` WP, one looses the safety guarantees for the whole program as composing a `MaybeStuck` WP with a `NotStuck` WP results in a `MaybeStuck` WP.
This MR extends the language interface with a `stuck_allowed e σ` predicate (name open for debate) that specifies expressions that are not required to be reducible. One can obtain the `NotStuck` WP by defining `stuck_allowed e σ` as `False` and the `MaybeStuck` WP by defining `stuck_allowed e σ` as `True`.
Open questions:
- [ ] Naming
- [ ] What are the right set of axioms?
- [ ] Discussing TODOs in the code
- [ ] Should the `MaybeStuck` be removed in this MR or in a follow up MR?
- [ ] The `MaybeStuck` WP allows having both `MaybeStuck` and `NotStuck` WP for the same language while the solution in this MR fixes the notion of stuckness of a language. Is this a problem?
- [ ] Should we add a `Abort` NB expression to HeapLang to replace the [diverge](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/lib/diverge.v) library?https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/776Updated suggested emacs indendation configuration2022-05-11T14:33:48ZJonas KastbergUpdated suggested emacs indendation configurationThe currently suggested indentation configuration for does not give the wanted indentations for newer version of proof-general.
For instance `∧` is no longer used, as it would indent statements as follows in newer versions of proof-gene...The currently suggested indentation configuration for does not give the wanted indentations for newer version of proof-general.
For instance `∧` is no longer used, as it would indent statements as follows in newer versions of proof-general:
```
P *
Q
```
We now rather use `->`, which indents them in the same way across versions:
```
P *
Q
```
EDIT: Typohttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/742Draft: Add simple library for priority levels and use it for `iFrame`2023-09-29T07:46:04ZRobbert KrebbersDraft: Add simple library for priority levels and use it for `iFrame`As already discussed here: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739
I now designed a solution that does not require to add an additional argument to the `Frame` class. Instead, it puts a dummy constant in the Coq contex...As already discussed here: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739
I now designed a solution that does not require to add an additional argument to the `Frame` class. Instead, it puts a dummy constant in the Coq context, and rules that have side-conditions on the priority level have a TC premise that checks if the level is OK. I have implemented the priority levels as a separate library that in principle could be used for other tactics too.
TODO:
- Figure out where the priority level library should go to. I put it in `iris.proofmode`, but in principle it has nothing to with the proof mode.
- Figure out syntax for `iFrame` and friends to give the priority level in a concise way.
- Determine what levels we need for `iFrame`. I think we don't want framing for ∧, ∨, and Fractional by default. Are there more examples? What levels would be appropriate?
- Adapt the proof scripts, I currently use `at_level` by lack of syntax.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/710WIP: Define more uPred connectives in siProp2021-11-30T16:42:32ZHai DangWIP: Define more uPred connectives in siPropThis is an experiment initially with the step 1 + 3 of #420. Then I have experimented more with 5 and 8.This is an experiment initially with the step 1 + 3 of #420. Then I have experimented more with 5 and 8.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/700Add mode for Dist2021-06-18T06:46:43ZPaolo G. GiarrussoAdd mode for Disthttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/697Add generalized implication lemma for big_sepM2021-07-31T09:50:32ZSimon Friis VindumAdd generalized implication lemma for big_sepMThis MR adds a more general version of `big_sepM_impl`. The current `big_sepM_impl` requires the map in the assumption and conclusion to be exactly the same. The variant in this MR allows the maps to be different. They don't have to agre...This MR adds a more general version of `big_sepM_impl`. The current `big_sepM_impl` requires the map in the assumption and conclusion to be exactly the same. The variant in this MR allows the maps to be different. They don't have to agree in their overlap and the domain of the map in the assumption can be both smaller or larger than the domain of the map in the conclusion.
The lemma `big_sepM_impl_strong` is the fully general lemma and `big_sepM_impl_dom_subseteq` is a variant that is easier to use when one knows that the map in the assumption is defined for at least as many keys as the map in the conclusion.
~~Note: Both the lemmas require `Φ` and `Ψ` to be affine since the map in the assumption may be larger and stuff from it may be thrown away. One can imagine variants of these lemmas where the initial map is only allowed to be smaller and where the affine requirement is lifted. For my use case I needed this more general variant though.~~
Note: This generalization makes sense for some of the other `big_sep*_impl` as well but I only needed it for `big_sepM`. If adding it for some of the others is not too much additional work then I can do that as well, but I would prefer not to 😅. Edit: See #431 for this.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/688Add missing commutations for `fupd`2021-05-31T14:22:56ZPaolo G. GiarrussoAdd missing commutations for `fupd`Suggestion from Gregory Malecha, proof scripts from me.Suggestion from Gregory Malecha, proof scripts from me.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/651Draft: More (peri)scopes for Iris2021-05-07T12:44:34ZPaolo G. GiarrussoDraft: More (peri)scopes for IrisSome ideas for discussion, in 4 differently-controversial commits:
1. Scopes for bi_car: should be uncontroversial.
2. Drop some %I that become redundant: maybe controversial
3. Drop some %I that was already redundant.
4. Add missing `%I...Some ideas for discussion, in 4 differently-controversial commits:
1. Scopes for bi_car: should be uncontroversial.
2. Drop some %I that become redundant: maybe controversial
3. Drop some %I that was already redundant.
4. Add missing `%I` for big_ops.
Which ones should we pursue?
(Not yet finished building locally.)https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/615Alternative take at "better support for view shift with mismatching masks"2021-04-29T09:35:59ZRobbert KrebbersAlternative take at "better support for view shift with mismatching masks"This is an alternative and more general take at !527. This MR generalizes the instance `elim_modal_fupd_fupd` so that it can handle fancy updates with mismatching masks by implicitly using `fupd_mask_frame_r`:
```coq
Global Instance eli...This is an alternative and more general take at !527. This MR generalizes the instance `elim_modal_fupd_fupd` so that it can handle fancy updates with mismatching masks by implicitly using `fupd_mask_frame_r`:
```coq
Global Instance elim_modal_fupd_fupd `{!BiFUpd PROP} φ p E1' E2' E1 E2 E3 P Q :
ElimFUpdChangeMask φ E1' E2' E1 E2 →
ElimModal φ p false
(|={E1',E2'}=> P) P
(|={E1,E3}=> Q) (|={E2,E3}=> Q).
```
The class `ElimFUpdChangeMask` factors our some typical cases (in all cases the resulting hypothesis is `P`):
| Hypothesis | Goal | Resulting goal | Side-condition | Instance |
|-------------------|------------------|-----------------------------|----------------|-----------------------------------|
| `\|={E1,E2}=> P` | `\|={E1,E3}=> Q` | `\|={E2,E3}=> Q` | | `elim_fupd_change_mask_same_src` |
| `\|={∅,E2}=> P` | `\|={E1,E3}=> Q` | `\|={E2 ∪ E1,E3}=> Q` | | `elim_fupd_change_mask_src_empty` |
| `\|={E2,E2}=> P` | `\|={E1,E3}=> Q` | `\|={E1,E3}=> Q` | `E2 ⊆ E1` | `elim_fupd_change_mask_no_change` |
| `\|={E2,∅}=> P` | `\|={E1,E3}=> Q` | `\|={E1 ∖ E2,E3}=> Q` | `E2 ⊆ E1` | `elim_fupd_change_mask_tgt_empty` |
| `\|={E2,E2'}=> P` | `\|={E1,E3}=> Q` | `\|={E2' ∪ E1 ∖ E2,E3}=> Q` | `E2 ⊆ E1` | `elim_fupd_change_mask_default` |
Contrary to !527, I think this MR matches up better with the usual behavior we have for eliminating modalities: it removes the modality from the hypothesis and changes the goal accordingly, while possibly generating a side-condition.
In the future we could decide to extend `ElimFUpdChangeMask` to have more sophisticated instances, e.g., for canceling out masks.
This MR furthermore includes the lemma ``fupd_intro_mask_adjust`` from !527, which I think is very useful. This MR makes sure that the lemma is consistent with some other (new and existing) variants of the lemma:
```coq
Lemma fupd_mask_subseteq E1 E2 P :
E2 ⊆ E1 →
((|={E2,E1}=> emp) ={E2}=∗ P) ={E1,E2}=∗ P.
Lemma fupd_intro_mask_subseteq E1 E2 P : (* [fupd_intro_mask_adjust] in !527 *)
E2 ⊆ E1 →
((|={E2,E1}=> emp) -∗ P) ={E1,E2}=∗ P.
Lemma fupd_mask_eq E1 E2 P : E1 = E2 → (|={E1}=> P) ={E1,E2}=∗ P. (* was [fupd_mask_same] *)
Lemma fupd_intro_mask_eq E1 E2 P : E1 = E2 → P ={E1,E2}=∗ P.
```https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/613Use class `IntoFUpd` in tactic `wp_value_head`2021-12-12T17:57:47ZRobbert KrebbersUse class `IntoFUpd` in tactic `wp_value_head`This MR adds the following class:
```coq
Class IntoFUpd `{!BiFUpd PROP} E (P Q : PROP) :=
into_fupd : P ={E}=∗ Q.
```
This class is then used to implement the "smart" update-adding in `wp_value_head`.
While the total amount of code ...This MR adds the following class:
```coq
Class IntoFUpd `{!BiFUpd PROP} E (P Q : PROP) :=
into_fupd : P ={E}=∗ Q.
```
This class is then used to implement the "smart" update-adding in `wp_value_head`.
While the total amount of code increases, most of it is general purpose. The actual code in `heaplang.proofmode` is smaller, which means that it's easier to port it to other Iris developments (like Iron, where I wanted to add this feature).https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/564Add a verified interpreter for HeapLang2021-03-18T11:10:22ZTej Chajedtchajed@gmail.comAdd a verified interpreter for HeapLangThe code in this file is pretty different from most of Iris, using a lot more automation and Ltac. If and when we are happy with the overall idea of merging an interpreter then we can figure out the naming and code style issues I'm sure ...The code in this file is pretty different from most of Iris, using a lot more automation and Ltac. If and when we are happy with the overall idea of merging an interpreter then we can figure out the naming and code style issues I'm sure this file has.
Much credit for the interpreter and proof strategy goes to Sydney Gibson, who wrote an interpreter for GooseLang that I basically back-ported to HeapLang.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/502WIP: Prototype a validity restriction CMRA construction2020-09-14T18:53:32ZTej Chajedtchajed@gmail.comWIP: Prototype a validity restriction CMRA constructionImplement a first cut at building a CMRA by restricting the validity of an existing CMRA. We demonstrate the construction by building a CmraMixin for auth that starts with a CMRA built from combinators and primitives.
The implementation...Implement a first cut at building a CMRA by restricting the validity of an existing CMRA. We demonstrate the construction by building a CmraMixin for auth that starts with a CMRA built from combinators and primitives.
The implementation actually transports a structure `A:cmraT` to `B:Type` across an isomorphism `iso A B`, which is a bijection using Leibniz equality. It also takes an arbitrary restriction of `A`'s validity over `B`, along with all of the validity-related CMRA laws. Unlike what I attempted in !348 this is a much more principled solution, leveraging the fact that we really have an isomorphism.
The implementation is a total mess. There are three high-level problems:
- The instances for `iso` are scoped too broadly. When I imported them in agree.v I got a typeclass resolution loop.
- I'm not sure about how canonical structures work out with this approach, given the way it uses an instance of the `iso` typeclass.
- The proofs for auth are extremely messy and should re-use the existing nice proofs for bits of the old auth construction.
There are also many things the auth library needs which would need to be implemented, many theorems that are generic for any subset construction.
It's not necessarily a problem, but I didn't generalize to transporting a CMRA to an OFE using a bijection that preserves equivalence, because first that's quite a bit more complicated to prove, and second because it would be harder to use for auth where we want to inherit the OFE structure from the CMRA anyway.
@robbertkrebbers and @jung is this the direction you were thinking of? Do we want to pursue this to (1) simplify auth and (2) for other users?
---
Background: This came up from working on a CMRA isomorphism construction (!348), where Robbert mentioned that the motivation was to construct the auth RA by restricting the validity of an RA built from some combinators. In that MR we didn't have an idea of what the spec would look like, so the assumptions we made were rather ad-hoc.
This specific construction, and applying it to auth, was also proposed in #210, phrased as cutting the RA "from the top"; there might be another subset construction but this is the most clearly useful/possible one.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/496Define logic `clProp` for axiom-free classical logic2021-05-12T10:21:37ZRobbert KrebbersDefine logic `clProp` for axiom-free classical logicThis MR defines a new logic `clProp` that embeds classical logic into Coq. It uses essentially the Gödel-Gentzen translation, so the propositions of `clProp` are defined as the subset of `Prop` propositions that are stable under double n...This MR defines a new logic `clProp` that embeds classical logic into Coq. It uses essentially the Gödel-Gentzen translation, so the propositions of `clProp` are defined as the subset of `Prop` propositions that are stable under double negation, and the pure, ∨, ∃ connectives of `clProp` are defined using a double negation.
The logic `clProp` is a BI, so this MR allows one to use the proof mode to carry out proofs in classical logic, without axioms! For example:
```coq
Lemma test_excluded_middle P Q : ⊢ P ∨ ¬P.
Proof.
iApply clProp.dn; iIntros "#H". iApply "H".
iRight. iIntros "HP". iApply "H". auto.
Qed.
Lemma test_peirces_law P Q : ((P → Q) → P) ⊢ P.
Proof.
iIntros "#H". iApply clProp.dn; iIntros "#HnotP". iApply "HnotP".
iApply "H". iIntros "HP". iDestruct ("HnotP" with "HP") as %[].
Qed.
```https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/474if instances for absorbing, affine and persistent2020-09-08T08:38:26ZAlix Trieuif instances for absorbing, affine and persistentI added instances of the form
```Coq
Global Instance if_persistent P Q (b: bool) : Persistent P -> Persistent Q -> Persistent (if b then P else Q).
```
for `Absorbing`, `Affine` and `Persistent`.
I only had to use the `Persistent` one i...I added instances of the form
```Coq
Global Instance if_persistent P Q (b: bool) : Persistent P -> Persistent Q -> Persistent (if b then P else Q).
```
for `Absorbing`, `Affine` and `Persistent`.
I only had to use the `Persistent` one in a development I worked on, but I figured the other instances might be useful too, so I added them.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/467WIP: Add `with M` option to `iModIntro` and use to redefine `iNext` to fix is...2020-09-29T11:30:36ZRobbert KrebbersWIP: Add `with M` option to `iModIntro` and use to redefine `iNext` to fix issue #331This allows us to not just specify a matching subterm for `iModIntro`, but also exactly what modality to introduce. This allows us to redefine `iNext` so that issue #331 can be closed.
I don't quite like the `with` syntax, so suggestion...This allows us to not just specify a matching subterm for `iModIntro`, but also exactly what modality to introduce. This allows us to redefine `iNext` so that issue #331 can be closed.
I don't quite like the `with` syntax, so suggestions for improvement are welcome.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/466Specify how to compile Iris without running the tests2020-09-30T12:37:10ZDan FruminSpecify how to compile Iris without running the testshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/455WIP: Remove `contractive_ne` and `contractive_proper` as instances.2021-02-15T11:10:25ZRobbert KrebbersWIP: Remove `contractive_ne` and `contractive_proper` as instances.This is a follow up of !454. It closes #321.
It removes `contractive_ne` and `contractive_proper` as instances, to be consistent with `ne_proper`. For all functions that are contractive, we already defined the corresponding `NonExpansiv...This is a follow up of !454. It closes #321.
It removes `contractive_ne` and `contractive_proper` as instances, to be consistent with `ne_proper`. For all functions that are contractive, we already defined the corresponding `NonExpansive` and `Proper` instances, so these instances just caused type class search to try useless paths.
These instances are sometimes useful when considering a lemma or section with a `Contractive f` parameter. Hence I added `contractive_ne` and `contractive_proper` as `Hint Immediate` so they are only used at the leaves of type class search. I have done a similar thing for `proper_ne` and `proper_ne_2`.