Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2019-08-13T11:22:48Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/302Fix issue #260: Error message when iLöb used on non-SBI2019-08-13T11:22:48ZRobbert KrebbersFix issue #260: Error message when iLöb used on non-SBITitle says it all.Title says it all.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/301Fix issue #259: Error message when iRevert is used on out of scope variable2019-08-13T11:26:36ZRobbert KrebbersFix issue #259: Error message when iRevert is used on out of scope variableThis fix is partly based on @Blaisorblade's but is a little less verbose.
I have also added a number of test cases.This fix is partly based on @Blaisorblade's but is a little less verbose.
I have also added a number of test cases.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/299Move array stuff to own file2019-08-13T15:43:32ZRalf Jungjung@mpi-sws.orgMove array stuff to own filehttps://gitlab.mpi-sws.org/iris/iris/issues/245 talks about `IntoAnd`, but I mirrored what we got for `big_sepL` and that's `IntoSep`.
However, I also remembered why we didn't do that for lambdaRust: there, array-mapsto is fractional, a...https://gitlab.mpi-sws.org/iris/iris/issues/245 talks about `IntoAnd`, but I mirrored what we got for `big_sepL` and that's `IntoSep`.
However, I also remembered why we didn't do that for lambdaRust: there, array-mapsto is fractional, and then there is the question whether one wants to split at the fraction or the list. We decided that the proofmode would split at the fraction. If we agree that's the more reasonable choice, we should *not* add the splitting-at-the-list now because then we couldn't extend array-mapsto to fractions later.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/298fix typo in -d> docs2019-08-12T11:51:05ZRalf Jungjung@mpi-sws.orgfix typo in -d> docsAt least I think this is just a typo.
Cc @robbertkrebbers @jjourdan @blaisorbladeAt least I think this is just a typo.
Cc @robbertkrebbers @jjourdan @blaisorbladeIris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/293Add `head_prim_fill_reducible`.2020-11-24T15:31:35ZDan FruminAdd `head_prim_fill_reducible`.A more general implication from `head_reducible` to `reducible`.A more general implication from `head_reducible` to `reducible`.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/292Add `big_sepL2_app_inv_2`.2020-11-24T15:31:35ZDan FruminAdd `big_sepL2_app_inv_2`.This is a useful lemma (at least for me), and I don't think it's directly derivable from the other two `_inv` lemmas.This is a useful lemma (at least for me), and I don't think it's directly derivable from the other two `_inv` lemmas.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/286show that pair construction commutes with taking the core2020-11-24T15:31:36ZRalf Jungjung@mpi-sws.orgshow that pair construction commutes with taking the coreI do not remember why `Core` is a typeclass. I could find exactly one other instance, and that's for STSs:
```
$ rg "Instance.*\bCore\b"
theories/algebra/cmra.v
182:Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
t...I do not remember why `Core` is a typeclass. I could find exactly one other instance, and that's for STSs:
```
$ rg "Instance.*\bCore\b"
theories/algebra/cmra.v
182:Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
theories/algebra/sts.v
199:Instance sts_core : Core (car sts) := λ x,
```
Might be worth just defining `core x := default x (pcore x)`?Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/285Mark projections for sigTO as NonExpansive and Proper2020-11-24T15:31:36ZPaolo G. GiarrussoMark projections for sigTO as NonExpansive and ProperNot urgent (can wait till after POPL).
These changes are logically part of the recent addition of sigTO. I'm using `projT1_ne`, but I added the other ones for completeness. One of these lemmas (`projT2_proper`) depends on UIP, since i...Not urgent (can wait till after POPL).
These changes are logically part of the recent addition of sigTO. I'm using `projT1_ne`, but I added the other ones for completeness. One of these lemmas (`projT2_proper`) depends on UIP, since it's almost a rephrasing of `sigT_equiv_eq_alt`.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/283heap_lang: Make binary "=" operator partial, to sync with CmpXchg2020-11-24T15:31:36ZRalf Jungjung@mpi-sws.orgheap_lang: Make binary "=" operator partial, to sync with CmpXchgThis also gets rid of [val_for_compare]-normalization; instead we introduce a
[LitErased] literal that is suited for use by erasure theorems.
Fixes https://gitlab.mpi-sws.org/iris/iris/issues/248This also gets rid of [val_for_compare]-normalization; instead we introduce a
[LitErased] literal that is suited for use by erasure theorems.
Fixes https://gitlab.mpi-sws.org/iris/iris/issues/248Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/279introduce notation for value comparison2019-06-29T22:38:38ZRalf Jungjung@mpi-sws.orgintroduce notation for value comparisonThis should make all those CAS specs much easier to read.
However, if I adjust the CAS specs now I'll have to do it all again once https://gitlab.mpi-sws.org/iris/iris/merge_requests/274 lands, so this just proposes the syntax now so ...This should make all those CAS specs much easier to read.
However, if I adjust the CAS specs now I'll have to do it all again once https://gitlab.mpi-sws.org/iris/iris/merge_requests/274 lands, so this just proposes the syntax now so the bikeshed about that can start.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/263Replace `C`s with `O`s since we use OFEs instead of COFEs.2020-11-24T15:31:38ZRobbert KrebbersReplace `C`s with `O`s since we use OFEs instead of COFEs.This closes issue #118. I hope I have caught all occurrences.
Another change:
- `ofe_fun` is now called `discrete_fun`, and the notation is now `-d>` instead of `-c>`.
I have used the following script:
```
+sed '
+s/\bCofeM...This closes issue #118. I hope I have caught all occurrences.
Another change:
- `ofe_fun` is now called `discrete_fun`, and the notation is now `-d>` instead of `-c>`.
I have used the following script:
```
+sed '
+s/\bCofeMor/OfeMor/g;
+s/\-c>/\-d>/g;
+s/\bcFunctor/oFunctor/g;
+s/\bCFunctor/OFunctor/g;
+s/\b\%CF/\%OF/g;
+s/\bconstCF/constOF/g;
+s/\bidCF/idOF/g
+s/\bdiscreteC/discreteO/g;
+s/\bleibnizC/leibnizO/g;
+s/\bunitC/unitO/g;
+s/\bprodC/prodO/g;
+s/\bsumC/sumO/g;
+s/\bboolC/boolO/g;
+s/\bnatC/natO/g;
+s/\bpositiveC/positiveO/g;
+s/\bNC/NO/g;
+s/\bZC/ZO/g;
+s/\boptionC/optionO/g;
+s/\blaterC/laterO/g;
+s/\bofe\_fun/discrete\_fun/g;
+s/\bdiscrete\_funC/discrete\_funO/g;
+s/\bofe\_morC/ofe\_morO/g;
+s/\bsigC/sigO/g;
+s/\buPredC/uPredO/g;
+s/\bcsumC/csumO/g;
+s/\bagreeC/agreeO/g;
+s/\bauthC/authO/g;
+s/\bnamespace_mapC/namespace\_mapO/g;
+s/\bcmra\_ofeC/cmra\_ofeO/g;
+s/\bucmra\_ofeC/ucmra\_ofeO/g;
+s/\bexclC/exclO/g;
+s/\bgmapC/gmapO/g;
+s/\blistC/listO/g;
+s/\bvecC/vecO/g;
+s/\bgsetC/gsetO/g;
+s/\bgset\_disjC/gset\_disjO/g;
+s/\bcoPsetC/coPsetO/g;
+s/\bgmultisetC/gmultisetO/g;
+s/\bufracC/ufracO/g
+s/\bfracC/fracO/g;
+s/\bvalidityC/validityO/g;
+s/\bbi\_ofeC/bi\_ofeO/g;
+s/\bsbi\_ofeC/sbi\_ofeO/g;
+s/\bmonPredC/monPredO/g;
+s/\bstateC/stateO/g;
+s/\bvalC/valO/g;
+s/\bexprC/exprO/g;
+s/\blocC/locO/g;
+s/\bdec\_agreeC/dec\_agreeO/g;
+s/\bgnameC/gnameO/g;
+s/\bcoPset\_disjC/coPset\_disjO/g;
+' -i $(find theories -name "*.v")
```Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/258A strong adequacy statement to rule them all2019-06-12T16:18:54ZRobbert KrebbersA strong adequacy statement to rule them allThe new adequacy statement unifies the jungle of old adequacy statement, namely `wp_strong_adequacy`, `wp_strong_all_adequacy`, and `wp_invariance`.
```coq
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} s e σ1 n κs t2 σ2 φ :
(∀ `{Hi...The new adequacy statement unifies the jungle of old adequacy statement, namely `wp_strong_adequacy`, `wp_strong_all_adequacy`, and `wp_invariance`.
```coq
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} s e σ1 n κs t2 σ2 φ :
(∀ `{Hinv : !invG Σ},
(|={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(Φ fork_post : val Λ → iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
stateI σ1 κs 0 ∗
WP e @ s; ⊤ {{ Φ }} ∗
(∀ e2 t2',
⌜ t2 = e2 :: t2' ⌝ -∗
⌜ ∀ e2, s = NotStuck → e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2) ⌝ -∗
stateI σ2 [] (length t2') -∗
from_option Φ True (to_val e2) -∗
([∗ list] v ∈ omap to_val t2', fork_post v) ={⊤,∅}=∗ ⌜ φ ⌝))%I) →
nsteps n ([e], σ1) κs (t2, σ2) →
φ.
```
This statement says that given given a proof of `WP e @ s; ⊤ {{ Φ }}` and a reduction from an initial state `([e], σ1)` to some intermediate state `(t2, σ2)`, then we can obtain a proof of a Coq proposition `φ` at the meta level, if we can prove `|={⊤,∅}=> ⌜φ⌝` in the logic under the following conditions:
- `t2 = e2 :: t2'`,
- All expressions in `t2` are either reducible or in normal form (progress),
- The state interpretation holds for `σ2`,
- If the main thread `t2` reduced to a value, the postcondition `Φ` holds,
- For any forked-off thread `t2'`, if they are a value, `fork_post` holds.
Since we do not have any requirement on `t2`, the adequacy statement applies if just the main thread has terminated (formerly `wp_strong_adequacy`), all threads have terminated (formerly `wp_strong_all_adequacy`), or no threads have terminated (formerly `wp_invariance`). In fact, it works for any combination of threads that have terminated, and will give you exactly the postconditions of those threads.
## Other changes
- I removed `wp_invariance`, and kept the more intuitive version, which was called `wp_invariance'`.
- I made `wp_adequacy` more consistent w.r.t. the other lemmas so one can also specific `post_fork`.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/249Add ghost data to locations2020-09-09T12:29:52ZRobbert KrebbersAdd ghost data to locationsThis MR makes it possible to attach "meta" or "ghost" data to locations. This is achieved by adding the following connectives to `heap_lang` and the `gen_heap` construction:
- When you allocate a location, in addition to the point-to ...This MR makes it possible to attach "meta" or "ghost" data to locations. This is achieved by adding the following connectives to `heap_lang` and the `gen_heap` construction:
- When you allocate a location, in addition to the point-to connective `l ↦ v`, you also get the token `meta_token ⊤ l`. This token is an exclusive resource that denotes that no meta data has been associated with the namespaces in the mask `⊤` for the location `l`.
- Meta data tokens can be split w.r.t. namespace masks, i.e. `meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2` if `E1 ## E2`.
- Meta data can be set using the update `meta_token l E ==∗ meta l N x` (provided `↑ N ⊆ E`, and `x : A` for any countable `A`). The `meta l N x` connective is persistent and denotes the knowledge that the meta data `x` has been associated with namespace `N` to the location `l`.
The advantage of this MR is that we can get much cleaner specs for ADTs. Currently, most specs expose some ghost name `γ` (or big tuple of ghost names) that is used for naming the ghost state used in the definition of the representation predicates. Using this MR, these ghost names `γ` can he hidden entirely, by associating them as meta data to the location `l`.
To make the system as flexible as possible, the `x : A` in `meta l N x` can be of any countable type `A`. This means that you can associate single ghost names, but also tuples of ghost names, or any arbitrary stuff you like to a location `l`.
Moreover, to further increase flexibility, instead of directly requiring the user to give an associated meta value when allocating an location, I have introduced the connective `meta_token`. This way, one could allocate the location, use some additional abstractions that may create ghost variables, and then change `meta_token` into `meta`.
To further extend that, I've indexed the `meta l N x` and `meta_token l E` predicates with a namespace `N` and mask `E`. That way, one basically has a linked-list of `meta` connectives. So, when building abstractions, one can gradually assign more ghost information to a location instead of having to do all of this at once.
This MR is much inspired by ghost record fields in tools like Verifast.
An example of an application of this MR is the spin/ticket lock spec, whose spec has become:
```coq
{{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}
{{{ is_lock lk R }}} acquire lk {{{ RET #(); locked lk ∗ R }}}
{{{ is_lock lk R ∗ locked lk ∗ R }}} release lk {{{ RET #(); True }}}
```
Note that `is_lock` and `locked` no longer have a `γ` as argument. This `γ` is hidden using `meta l nroot γ`.Iris 3.2https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/187The unbounded fractional authoritative camera2019-06-22T08:05:36ZRobbert KrebbersThe unbounded fractional authoritative cameraThe unbounded fractional authoritative camera is a version of the fractional authoritative camera that can be used with fractions `> 1`.
Most of the reasoning principles for this version of the fractional authoritative cameras are...The unbounded fractional authoritative camera is a version of the fractional authoritative camera that can be used with fractions `> 1`.
Most of the reasoning principles for this version of the fractional authoritative cameras are the same as for the original version. There are two difference:
- We get the additional rule that can be used to allocate a "surplus", i.e. if we have the authoritative element we can always increase its fraction and allocate a new fragment.
✓ (a ⋅ b) → ●?{p} a ~~> ●?{p + q} (a ⋅ b) ⋅ ◯?{q} b
- At the cost of that, we no longer have the `◯?{1} a` is an exclusive fragmental element (cf. `frac_auth_frag_validN_op_1_l`).Iris 3.2