Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-10-14T16:34:37Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/441Upstream later credits2022-10-14T16:34:37ZRalf Jungjung@mpi-sws.orgUpstream later credits@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I k...@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I keep forgetting what exactly are the `fupd` laws that we would lose by doing this, so maybe we can put that here. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/420Use siProp more in building the uPred (and BI) interfaces2023-03-04T18:40:53ZRalf Jungjung@mpi-sws.orgUse siProp more in building the uPred (and BI) interfacesuPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp`...uPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/410Modality for `Timeless`2021-04-19T07:51:21ZRalf Jungjung@mpi-sws.orgModality for `Timeless`We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ ...We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/392Masks in step-taking fupd notation2020-12-10T13:37:03ZRalf Jungjung@mpi-sws.orgMasks in step-taking fupd notationEarlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gi...Earlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/357Cancelable locks2020-10-21T11:00:44ZRobbert KrebbersCancelable locksIt would be really useful to have a version of cancelable locks, where the `is_lock` predicate is equipped with a fraction. That way, we could have a couple of things:
1. A Hoare triple for the physical free operation `{{ is_lock lk 1 R...It would be really useful to have a version of cancelable locks, where the `is_lock` predicate is equipped with a fraction. That way, we could have a couple of things:
1. A Hoare triple for the physical free operation `{{ is_lock lk 1 R }} free lk {{ R }}`
2. A rule `is_lock lk 1 R ==∗ ▷ R ∗ (▷ R' ==∗ is_lock lk 1 R')` that allows a "strong update" of the payload of the lock.
Now that we have the discardable fractional permissions, we could use those to get back the ordinary lock-spec by picking the fraction to be `DfracDiscarded`.
To implement this, we probably first want to generalize cancelable invariants, by a.) adding a discardable fraction b.) adding a rule for changing the proposition in case one owns the entire fraction.
Questions:
- For locks, do we want to equip `is_lock` with a fraction, or do we want to add a token `lock_own` (which would be timeless).
- If we equip `is_lock` with a fraction, we won't break backwards compatibility that much. One just needs to add `DfracDiscarded` everywhere. If we have a token for the fraction, backwards compatibility is a bigger issue. We could of course define `is_lock ... := new_is_lock ... ∗ lock_own DfracDiscarded` or something like that.
Any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/354Discardable camera improvements2020-10-09T13:50:33ZRalf Jungjung@mpi-sws.orgDiscardable camera improvements## Generalization
I think the variant of `dfrac` that I implemented with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531 can be generalized to a "discardable-anything":
```coq
Inductive discardable (A: cmraT) :=
| DOwn : A →...## Generalization
I think the variant of `dfrac` that I implemented with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531 can be generalized to a "discardable-anything":
```coq
Inductive discardable (A: cmraT) :=
| DOwn : A → dfrac
| DDiscarded : dfrac
| DBoth : A → dfrac.
```
with validity something like
```coq
Instance discardable_valid (A: cmraT) : Valid (discardable A) := λ x,
match x with
| DOwn q => ✓ q
| DDiscarded => True
| DBoth q => exists p, ✓ (q ⋅ p)
end%Qc.
```
I think this should work... what I am not sure about is if this is useful.^^
## old [discarded](https://gitlab.mpi-sws.org/iris/iris/-/issues/354#note_57686) idea: `option Qp`
After https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/531, the public interface of `dfrac` can basically be described via a smart constructor that takes `option Qp` -- in fact I am adding such a notation in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486. We can probably rephrase all the existing lemmas in terms of that single constructor, and @robbertkrebbers agrees that that would make a better interface.
Cc @simonfv @tchajedhttps://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/341Coecisting fractional and persistent read-only ownership2020-08-25T09:34:48ZRalf Jungjung@mpi-sws.orgCoecisting fractional and persistent read-only ownershipAs part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Ri...As part of https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/486, @tchajed and @simonfv raised the point that sometimes it would be useful to convert ownership of *some fraction* of a map element to persistent read-only ownership. Right now, our encoding through `frac * agree T + agree T` (or equivalently `(frac + ()) * agree T`) requires ownership of the full fraction for that move.
I think such a construction is possible, but it requires https://gitlab.mpi-sws.org/iris/iris/-/issues/257. Then we could relate an authoritative map to a fragment that's more like `option (frac * agree T) * option (agree T)`, and ensure that the second `option` is `None` unless the sum of all fraction fragments is less than 1.https://gitlab.mpi-sws.org/iris/iris/-/issues/340Polymorphic equality for HeapLang2020-08-22T19:06:03ZDan 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/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' ...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 ...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 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/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 lo...@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 i...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 state2020-12-07T10:18:54ZRalf 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) }.
Definitio...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)2021-06-13T09:56:24ZRalf 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 persisten...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 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/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. ...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/210Generic subset construction for RAs2020-09-08T20:33:39ZRalf 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.
...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/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...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/138wp_apply/Texan triple improvements2023-05-27T18:20:26ZRalf 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 varia...* [ ] `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 triple, 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.
* [ ] What about some support for introducing the postcondition into the context (avoiding a manual `iIntros` all the time)?
Blocked by #130