Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-05-13T09:53:35Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/271Follow-up from "Lang lemmas": intuitive explanation of mixin_step_by_val2020-05-13T09:53:35ZRalf Jungjung@mpi-sws.orgFollow-up from "Lang lemmas": intuitive explanation of mixin_step_by_valIn !324 I started a [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/324#note_41125) to find an intuitive explanation of "mixin_step_by_val". I propose this, and I still think it's good:
"Let \[fill K e1\] and \[fill K' e1'\] be two decompositions of the same expression such that \[e1'\] is reducible. Then either \[K\] is a prefix of \[K'\] (so \[e1\] actually contains \[e1'\] as its head redex), or \[e1\] is a value. In other words, there cannot be two entirely unrelated head redexes that actually reduce."
@amintimany had an objection that I did not understand:
> This does not really say anything about there not being redxes!
My response:
> Of course it does? If there are redexes, the contexts are related; thus if there are unrelated contexts, there are no redexes.
@amintimany @robbertkrebbers let's discuss here.In !324 I started a [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/324#note_41125) to find an intuitive explanation of "mixin_step_by_val". I propose this, and I still think it's good:
"Let \[fill K e1\] and \[fill K' e1'\] be two decompositions of the same expression such that \[e1'\] is reducible. Then either \[K\] is a prefix of \[K'\] (so \[e1\] actually contains \[e1'\] as its head redex), or \[e1\] is a value. In other words, there cannot be two entirely unrelated head redexes that actually reduce."
@amintimany had an objection that I did not understand:
> This does not really say anything about there not being redxes!
My response:
> Of course it does? If there are redexes, the contexts are related; thus if there are unrelated contexts, there are no redexes.
@amintimany @robbertkrebbers let's discuss here.Iris 3.3Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/257Auth as Views2020-10-01T19:57:53ZRalf 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/234Syntactic type system for heap_lang2020-10-01T11:28:21ZRobbert KrebbersSyntactic 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/215Explore getting rid of implication2019-11-01T11:07:41ZRalf Jungjung@mpi-sws.orgExplore getting rid of implicationIt seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. We could remove implication from the MoSeL interface and see what happens.
For Iris itself I mostly expect this to work, but the general linear case might make this harder. Or not.It seems possible that we don't actually need implication and could work without it (so we'd work in intuitionistic linear logic instead of the more general separation logic/BI). Seems at least interesting to figure out of that's true. We could remove implication from the MoSeL interface and see what happens.
For Iris itself I mostly expect this to work, but the general linear case might make this harder. Or not.https://gitlab.mpi-sws.org/iris/iris/-/issues/161Use `plainly_alt` as an axiom and replace most of the current ones2020-03-18T15:08:43ZJacques-Henri JourdanUse `plainly_alt` as an axiom and replace most of the current onesIn the interface for plainly, we could have `plainly_alt` as an axiom. Here are the reasons this is not a completely absurd idea:
1- Most of the axioms can be removed. Namely, the only ones remaining are:
* `bi_persistently_impl_plainly`, `bi_plainly_impl_plainly` (which I find kind of arbitrary anyway),
* `sbi_mixin_prop_ext` (which is actually one of the few current axioms of `plainly` that actually /says/ something about the BI. So this is expected that it stays.
* The axioms about the updates, but I would say these are rather about the update than about `bi_plainly`
* `sbi_mixin_later_plainly_2`, which somehow I am not able to prove. But perhaps I am missing something.
Note that for some of these axioms (except `bi_plainly_impl_plainly`, `sbi_mixin_prop_ext` and the update axioms), we could
replace "for all plain assertion P" by "for all equality", which make them understandable even without understanding what is plainly.
2- I would say the definition of `plainly_alt` is quite intuitive. Indeed, `P /\ emp = emp` is a way of internally saying `emp |- P`, which exactly means that `P` is valid. So this definition can directly be interpreted as the "internal validity".In the interface for plainly, we could have `plainly_alt` as an axiom. Here are the reasons this is not a completely absurd idea:
1- Most of the axioms can be removed. Namely, the only ones remaining are:
* `bi_persistently_impl_plainly`, `bi_plainly_impl_plainly` (which I find kind of arbitrary anyway),
* `sbi_mixin_prop_ext` (which is actually one of the few current axioms of `plainly` that actually /says/ something about the BI. So this is expected that it stays.
* The axioms about the updates, but I would say these are rather about the update than about `bi_plainly`
* `sbi_mixin_later_plainly_2`, which somehow I am not able to prove. But perhaps I am missing something.
Note that for some of these axioms (except `bi_plainly_impl_plainly`, `sbi_mixin_prop_ext` and the update axioms), we could
replace "for all plain assertion P" by "for all equality", which make them understandable even without understanding what is plainly.
2- I would say the definition of `plainly_alt` is quite intuitive. Indeed, `P /\ emp = emp` is a way of internally saying `emp |- P`, which exactly means that `P` is valid. So this definition can directly be interpreted as the "internal validity".https://gitlab.mpi-sws.org/iris/iris/-/issues/36STSs: Consider changing the def. of frame-steps2019-11-01T13:16:11ZRalf Jungjung@mpi-sws.orgSTSs: Consider changing the def. of frame-stepsJeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:
> $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$
> This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change `frame_step` accordingly, maybe this simplifies some things a little.Jeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:
> $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$
> This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change `frame_step` accordingly, maybe this simplifies some things a little.