Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-08-09T09:45:50Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/340Polymorphic equality for HeapLang2020-08-09T09:45:50ZDan FruminPolymorphic equality for HeapLangIt would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.It would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.https://gitlab.mpi-sws.org/iris/iris/-/issues/257Auth as Views2020-08-07T18:48:23ZRalf Jungjung@mpi-sws.orgAuth as ViewsGregory [suggested](https://lists.mpi-sws.org/pipermail/iris-club/2019-July/000198.html) a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user pick some relation between them. I think it can truly be any (Coq-level) relation for discrete types; for the CMRA variant we likely need a step-indexed relation. The existing "auth" is then the special case of using the same type, and equality as the relation.
This subsumes https://gitlab.mpi-sws.org/iris/iris/merge_requests/91 by making the relation also require bijectivity. And this also could be useful for situations where we have a very right CMRA for the fragments, which often means lots of "junk" data (such as `to_agree`, of `ExclBot`). So instead of the pattern where we do `exists heap, own (● to_auth heap)`, we could have this `to_auth` in the relation.
An open question is what would happen with all our theory about local updates.
Things to do:
* [ ] Implement a generalized "auth as view" library
* [ ] Implement monotone partial bijections (https://gitlab.mpi-sws.org/iris/iris/merge_requests/91) in terms of that.Gregory [suggested](https://lists.mpi-sws.org/pipermail/iris-club/2019-July/000198.html) a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user pick some relation between them. I think it can truly be any (Coq-level) relation for discrete types; for the CMRA variant we likely need a step-indexed relation. The existing "auth" is then the special case of using the same type, and equality as the relation.
This subsumes https://gitlab.mpi-sws.org/iris/iris/merge_requests/91 by making the relation also require bijectivity. And this also could be useful for situations where we have a very right CMRA for the fragments, which often means lots of "junk" data (such as `to_agree`, of `ExclBot`). So instead of the pattern where we do `exists heap, own (● to_auth heap)`, we could have this `to_auth` in the relation.
An open question is what would happen with all our theory about local updates.
Things to do:
* [ ] Implement a generalized "auth as view" library
* [ ] Implement monotone partial bijections (https://gitlab.mpi-sws.org/iris/iris/merge_requests/91) in terms of that.https://gitlab.mpi-sws.org/iris/iris/-/issues/244Add a general lattice RA to Iris2019-11-01T14:03:35ZRalf 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. We should have that RA in Iris.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/234Syntactic type system for heap_lang2019-11-01T12:44:11ZRobbertSyntactic type system for heap_lang@dfrumin defined a syntactic type system for heap_lang in the reloc repo:
https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v
I would like to use his type system to state the fundamental theorem for the unary logical relation of heap_lang in iris-examples (https://gitlab.mpi-sws.org/iris/examples/tree/master/theories/logrel_heaplang), as right now that formalization only has semantic types and the semantic typing rules.
How about adding @dfrumin's syntactic type system to the heap_lang folder of the Iris repo?
Some things to discuss:
- [ ] It currently relies on autosubst. Using strings for binding in types will be horrible, since there we actually have to deal with capture. Do we mind having a dependency of Iris on Autosubst, or would it be better to write a manual version with De Bruijn indexes?
- [ ] It uses some fun encodings for pack and unpack (of existential types) and type abstraction and application, see https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v#L80 Are we happy with that, or are there more elegant ways of doing that?@dfrumin defined a syntactic type system for heap_lang in the reloc repo:
https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v
I would like to use his type system to state the fundamental theorem for the unary logical relation of heap_lang in iris-examples (https://gitlab.mpi-sws.org/iris/examples/tree/master/theories/logrel_heaplang), as right now that formalization only has semantic types and the semantic typing rules.
How about adding @dfrumin's syntactic type system to the heap_lang folder of the Iris repo?
Some things to discuss:
- [ ] It currently relies on autosubst. Using strings for binding in types will be horrible, since there we actually have to deal with capture. Do we mind having a dependency of Iris on Autosubst, or would it be better to write a manual version with De Bruijn indexes?
- [ ] It uses some fun encodings for pack and unpack (of existential types) and type abstraction and application, see https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v#L80 Are we happy with that, or are there more elegant ways of doing that?https://gitlab.mpi-sws.org/iris/iris/-/issues/228"expression validity" in WP2019-11-01T13:59:44ZJonas Kastberg"expression validity" in WPI propose updating the weakest precondition with a predicate over expressions,
mainly for the purpose of establishing a notion of ```well formed``` expressions.
General idea:
The idea is that some expressions might be outright invalid in the absence of certain properties on the state. A predicate on expression, that are preserved under step reduction, could be used to differentiate such expressions.
Furthermore, being able to derive certain properties about expressions when opening the weakest precondition might allow for some automation in regards to "pure" reductions that depend on the state while not changing it.
Specific Case:
My Iris instantation is a "language" over processes, where ```pstate := gmap pid (state)``` and ```pexpr := pid * expr```, where ```pid``` is a process identifier.
For modularity I have separate reduction layers, with the top-layer looking up the state of the process in the state map ```step ((p,e), <[p := σh]>σp) -> ((p,e'), <[p := σh']>σp), efs)```.
This means that every single reduction requires the process id of the expression to be in the map, even if it does not change (in case the underlying reduction is pure).
The presence of the necessary mapping is then expressed as a logical fragment, which is required by every single of my weakest precondition rules. Furthermore, I cannot do "Pure" reductions, as conceptualised with the existing ```PureExec``` class.
Proposed Solution:
Update the language instantiation to include a predicate over expressions (here named ```well_formed```), and use it in the weakest precondition.
The predicate should uphold certain properties, such as being preserved under step reduction and contexts.
```
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 κ κs n,
state_interp σ1 (κ ++ κs) n ∗ well_formed e1 ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs (length efs + n) ∗
well_formed e2 ∗
wp E e2 Φ ∗
[∗ list] i ↦ ef ∈ efs, well_formed ef ∗ wp ⊤ ef fork_post
end%I.
```
Define a lifted ```PureExecState```, which defines expressions that are reducible and "pure" assuming that the state interpretation and well-formedness predicates hold:
```
Record pure_step_state (e1 e2 : expr Λ) := {
pure_exec_val_state : to_val e1 = None;
pure_step_safe_state σ1 κ n : state_interp σ1 κ n -∗ well_formed e1 -∗ ⌜reducible_no_obs e1 σ1⌝;
pure_step_det_state σ1 κ κs e2' σ2 efs n :
state_interp σ1 (κ++κs) n -∗ well_formed e1 -∗ ⌜prim_step e1 σ1 κ e2' σ2 efs⌝ → ⌜κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []⌝
}.
```
An important property of the proposed change is that original Iris instances remain unchanged when given ```True``` as the well_formed predicate.
Points of discussion:
- It has earlier been suggested to introduce closedness of expression in a [similar manner](https://gitlab.mpi-sws.org/iris/iris/merge_requests/58). Note however that the closedness condition on expressions has been phased out of the current iteration of Iris.
- The change would mean that any WP holds trivially true for invalid expressions, which must then suddenly be considered in many places.I propose updating the weakest precondition with a predicate over expressions,
mainly for the purpose of establishing a notion of ```well formed``` expressions.
General idea:
The idea is that some expressions might be outright invalid in the absence of certain properties on the state. A predicate on expression, that are preserved under step reduction, could be used to differentiate such expressions.
Furthermore, being able to derive certain properties about expressions when opening the weakest precondition might allow for some automation in regards to "pure" reductions that depend on the state while not changing it.
Specific Case:
My Iris instantation is a "language" over processes, where ```pstate := gmap pid (state)``` and ```pexpr := pid * expr```, where ```pid``` is a process identifier.
For modularity I have separate reduction layers, with the top-layer looking up the state of the process in the state map ```step ((p,e), <[p := σh]>σp) -> ((p,e'), <[p := σh']>σp), efs)```.
This means that every single reduction requires the process id of the expression to be in the map, even if it does not change (in case the underlying reduction is pure).
The presence of the necessary mapping is then expressed as a logical fragment, which is required by every single of my weakest precondition rules. Furthermore, I cannot do "Pure" reductions, as conceptualised with the existing ```PureExec``` class.
Proposed Solution:
Update the language instantiation to include a predicate over expressions (here named ```well_formed```), and use it in the weakest precondition.
The predicate should uphold certain properties, such as being preserved under step reduction and contexts.
```
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 κ κs n,
state_interp σ1 (κ ++ κs) n ∗ well_formed e1 ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs (length efs + n) ∗
well_formed e2 ∗
wp E e2 Φ ∗
[∗ list] i ↦ ef ∈ efs, well_formed ef ∗ wp ⊤ ef fork_post
end%I.
```
Define a lifted ```PureExecState```, which defines expressions that are reducible and "pure" assuming that the state interpretation and well-formedness predicates hold:
```
Record pure_step_state (e1 e2 : expr Λ) := {
pure_exec_val_state : to_val e1 = None;
pure_step_safe_state σ1 κ n : state_interp σ1 κ n -∗ well_formed e1 -∗ ⌜reducible_no_obs e1 σ1⌝;
pure_step_det_state σ1 κ κs e2' σ2 efs n :
state_interp σ1 (κ++κs) n -∗ well_formed e1 -∗ ⌜prim_step e1 σ1 κ e2' σ2 efs⌝ → ⌜κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []⌝
}.
```
An important property of the proposed change is that original Iris instances remain unchanged when given ```True``` as the well_formed predicate.
Points of discussion:
- It has earlier been suggested to introduce closedness of expression in a [similar manner](https://gitlab.mpi-sws.org/iris/iris/merge_requests/58). Note however that the closedness condition on expressions has been phased out of the current iteration of Iris.
- The change would mean that any WP holds trivially true for invalid expressions, which must then suddenly be considered in many places.https://gitlab.mpi-sws.org/iris/iris/-/issues/227Provide a convenient way to define non-recursive ghost state2019-11-04T15:18:44ZRalf Jungjung@mpi-sws.orgProvide a convenient way to define non-recursive ghost stateIt is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
```
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
```
To make things worse, if you forget the `lockΣ`, your proof will still work. You might just have assumed false, accidentally.
Can we do better than that, at least for the simple and common case of non-recursive ghost state?It is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
```
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
```
To make things worse, if you forget the `lockΣ`, your proof will still work. You might just have assumed false, accidentally.
Can we do better than that, at least for the simple and common case of non-recursive ghost state?https://gitlab.mpi-sws.org/iris/iris/-/issues/224Define persistence otherwise (and get rid of core)2020-05-31T19:05:20ZRalf Jungjung@mpi-sws.orgDefine persistence otherwise (and get rid of core)As a preparatory step towards defining the persistence modality inside the logic (if reasonably possible), we could try to change the model of persistence in Iris to no longer use the core (and get rid of the core). As long as persistence is the only connective defined using the core, it is impossible to define an equivalent connective inside the logic, so so this is interesting both to simplify the RA axioms (and even more so the axioms for ordered RAs), and to work towards maybe eventually defining persistence inside the logic.
Cc @robbertkrebbers @jjourdan @jtassaroAs a preparatory step towards defining the persistence modality inside the logic (if reasonably possible), we could try to change the model of persistence in Iris to no longer use the core (and get rid of the core). As long as persistence is the only connective defined using the core, it is impossible to define an equivalent connective inside the logic, so so this is interesting both to simplify the RA axioms (and even more so the axioms for ordered RAs), and to work towards maybe eventually defining persistence inside the logic.
Cc @robbertkrebbers @jjourdan @jtassarohttps://gitlab.mpi-sws.org/iris/iris/-/issues/210Generic subset construction for RAs2019-11-01T12:43:59ZRalf Jungjung@mpi-sws.orgGeneric subset construction for RAsIn auth, we already implicitly use a construction that carves out a subset of an RA by restricting validity. @gparthas now needs something similar for stuff he is currently doing. We should have a general construction for this purpose.
Related to https://gitlab.mpi-sws.org/FP/iris-coq/issues/42 (which also wants to touch `auth`).In auth, we already implicitly use a construction that carves out a subset of an RA by restricting validity. @gparthas now needs something similar for stuff he is currently doing. We should have a general construction for this purpose.
Related to https://gitlab.mpi-sws.org/FP/iris-coq/issues/42 (which also wants to touch `auth`).https://gitlab.mpi-sws.org/iris/iris/-/issues/138wp_apply/Texan triple improvements2020-02-23T22:25:25ZRalf Jungjung@mpi-sws.orgwp_apply/Texan triple improvements* `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`. This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* When proving a tirple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.
Blocked by #130* `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`. This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* When proving a tirple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.
Blocked by #130https://gitlab.mpi-sws.org/iris/iris/-/issues/124heap_lang: mutable n-ary locations, n-ary products, n-ary sums2019-11-01T13:25:49ZRalf Jungjung@mpi-sws.orgheap_lang: mutable n-ary locations, n-ary products, n-ary sumsThe former is interesting to model more realistic linked lists. However, we still can't realistically do CAS on sum discriminants, so if we want to restrict CAS to "small" types, we may have to rewrite some examples.The former is interesting to model more realistic linked lists. However, we still can't realistically do CAS on sum discriminants, so if we want to restrict CAS to "small" types, we may have to rewrite some examples.https://gitlab.mpi-sws.org/iris/iris/-/issues/29Bring back Logically Atomic Triples (Coq + docs)2019-11-01T13:09:17ZJeehoon Kangjeehoon.kang@kaist.ac.krBring back Logically Atomic Triples (Coq + docs)* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendix is still in the repository (http://plv.mpi-sws.org/iris/appendix.pdf)?
- Do you have a plan to merge the appendix of POPL 2015 paper and that of ICFP 2016? It would be definitely helpful to readers like me.
---
@jung wrote
The POPL 2015 appendix has been split into two parts:
* The Iris Documentation is describing Iris in general, from the model through the base logic to the most important derived constructions. The version matching Iris 2.0 can be found on the website. It should have more derived constructions than it does, like STSs... however, we are currently in the process of redesigning how constructions like STSs describe their interface to the world, so now would be a bad time to update the documentation :/
* The details of logically atomic triples. These triples have not been ported to later versions of Iris, which is why they don't show up in the current appendix. Unfortunately, since pretty much all examples involve logically atomic triples, those are now all outdated as well. (On paper, that is.)
What, specifically, are you missing from the POPL 2015 appendix?
* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendix is still in the repository (http://plv.mpi-sws.org/iris/appendix.pdf)?
- Do you have a plan to merge the appendix of POPL 2015 paper and that of ICFP 2016? It would be definitely helpful to readers like me.
---
@jung wrote
The POPL 2015 appendix has been split into two parts:
* The Iris Documentation is describing Iris in general, from the model through the base logic to the most important derived constructions. The version matching Iris 2.0 can be found on the website. It should have more derived constructions than it does, like STSs... however, we are currently in the process of redesigning how constructions like STSs describe their interface to the world, so now would be a bad time to update the documentation :/
* The details of logically atomic triples. These triples have not been ported to later versions of Iris, which is why they don't show up in the current appendix. Unfortunately, since pretty much all examples involve logically atomic triples, those are now all outdated as well. (On paper, that is.)
What, specifically, are you missing from the POPL 2015 appendix?