Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-08-24T16:40:02Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/208Import Coq.Strings.Ascii before using ascii notations2018-08-24T16:40:02ZGhost UserImport Coq.Strings.Ascii before using ascii notationsI don't know how to fork a repo on gitlab (the button is grayed out), and I don't know how to make a merge request here from a branch on github, so I'm creating an issue instead for merging https://github.com/JasonGross/iris-coq/commit/5...I don't know how to fork a repo on gitlab (the button is grayed out), and I don't know how to make a merge request here from a branch on github, so I'm creating an issue instead for merging https://github.com/JasonGross/iris-coq/commit/57743dd702b4c09b6e8d7cd171c0d7852d1da39a / https://github.com/JasonGross/iris-coq/compare/fix-for-8064
Import prim token notations before using them
This is required for compatibility with
coq/coq#8064, where prim token notations no longer
follow `Require`, but instead follow `Import`.
c.f. coq/coq#8064 (comment)
All changes were made via
https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-pyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/110Import OCPL's heap_lang logic?2018-07-13T15:57:18ZDavid SwaseyImport OCPL's heap_lang logic?From !37:
> Please take a look at the heap interface in Fig. 2 of my OCPL paper (off my home page) or, more informatively, at theories/heap_lang/heap.v in the OCPL Coq development. I propose replacing the current heap_lang logic with th...From !37:
> Please take a look at the heap interface in Fig. 2 of my OCPL paper (off my home page) or, more informatively, at theories/heap_lang/heap.v in the OCPL Coq development. I propose replacing the current heap_lang logic with the strictly more expressive OCPL, and adding the OCPL examples to heap_lang/lib and tests/.
Ralf asked if I have a git repo. Yes. I will create a merge request once we settle !37. (OCPL builds on !37.)David SwaseyDavid Swaseyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/201Improve "... not found" error messages2019-01-11T09:44:12ZRalf Jungjung@mpi-sws.orgImprove "... not found" error messagesCurrently, the message says `(INamed "HQ") not found.`. Can we improve that to `"HQ" not found.`?Currently, the message says `(INamed "HQ") not found.`. Can we improve that to `"HQ" not found.`?https://gitlab.mpi-sws.org/iris/iris/-/issues/460Improve iCombine to derive validity properties of ghost state automatically2023-05-25T11:45:27ZIke MulderImprove iCombine to derive validity properties of ghost state automaticallyIt would be great if `iCombine` was also able to derive and provide validity properties of ghost state or mapsto connectives automatically. Currently, you have to search and apply such properties manually. This could be fixed if `iCombin...It would be great if `iCombine` was also able to derive and provide validity properties of ghost state or mapsto connectives automatically. Currently, you have to search and apply such properties manually. This could be fixed if `iCombine` takes an extra (optional) `gives` clause, which provides extra persistent facts (if those exist).
For example, consider the following environment:
```
"H1" : l ↦{#q1} v1
"H2" : l ↦{#q2} v2
```
executing `iCombine "H1 H2" as "H" gives %[Hq Hv]` should replace `"H1"` and `"H2"` with `"H": l ↦{#(q1 + q2)} v1` and introduces two new pure hypotheses `Hq : q1 + q2 ≤ 1` and `Hv : v1 = v2`.
The roadmap for implementing this would be split into two merge requests:
1. Change `FromSep` to only be used for `iSplit{L,R}`, change `iCombine` to rely on two new typeclasses `CombineSepAs` and `CombineSepGives`.
These would be defined as `CombineSepAs P1 P2 P := P1 ∗ P2 ⊢ P` where `P1 P2` are input, `P` output
and `CombineSepGives P1 P2 := P1 ∗ P2 ⊢ <pers> R` where `P1 P2` are input, `R` output.
This MR would provide some instances for stuff in `base_logic.lib`, `mapsto`.
The new syntax would be `iCombine "Hs" [as "H"] [gives "P"]`, where either the `as` clause or the `gives` clause must be present.
* If `as "H"` is present, all hypotheses `"Hs"` will be replaced by `"H"`, which can be an introduction pattern.
If not present, all `"Hs"` are kept as is
* If `gives "P"` is present, additionally learn persistent fact `"P"`, which can be an introduction pattern. Also supports `%?` introduction if this fact is pure.
* If more than two hypotheses are provided in `"Hs"`, repeatedly run `CombineSep` with the accumulated results
* There will be an additional boolean indicating whether `CombineSepAs` used the default instance.
2. Give general instance for `own` (= MR !771, addresses #251)
This is a summary of a discussion by @jung, @robbertkrebbers, @snyke7 and @gmalecha at the Iris Workshop. Let me know if I forgot something.https://gitlab.mpi-sws.org/iris/iris/-/issues/177Improve naming of lemmas about modalities2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgImprove naming of lemmas about modalitiesThe following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1...The following discussion from !130 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/130#note_26050): (+7 comments)
We agreed on the following scheme
```
M1_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2_{swap,comm}: M1 (M2 P) ⊣⊢ M2 (M1 P)
```
However, @robbertkrebbers noted that we have plenty of lemmas of the last form. Optimizing for conciseness, we could also use
```
M1_{into,impl,entails}_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
```Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/53Improve solve_ndisj2017-02-16T14:07:06ZRalf Jungjung@mpi-sws.orgImprove solve_ndisj<https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c72bfec9e38531b7dc70f05c2415ed1e3f806899> demonstrates some cases that `solve_ndisj` cannot handle, and it'd be great if it could. Most of them could be handled if we added
```
Hint Ex...<https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c72bfec9e38531b7dc70f05c2415ed1e3f806899> demonstrates some cases that `solve_ndisj` cannot handle, and it'd be great if it could. Most of them could be handled if we added
```
Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
```
The one remaining case is more subtle. It is solved by `assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. set_solver.`, but is there a way we can plug solve_ndisj and set_solver together so that we don't have to say in advance which inclusions we need?
Cc @robbertkrebbers @jjourdanhttps://gitlab.mpi-sws.org/iris/iris/-/issues/49Improve support of simplify_option_eq (and simplify_map_eq?) for setoids2017-11-13T18:13:54ZRalf Jungjung@mpi-sws.orgImprove support of simplify_option_eq (and simplify_map_eq?) for setoidsSome testcases:
* <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
* in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`Some testcases:
* <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c6a626adbe1bf78b34f4e74204b98007f532892d#59b3a9376af7e8ce6a745e02cef554707e5c7419_585_585>
* in lambdaRust, lifetime/primitive.v, proof of `own_ilft_auth_agree`Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/459Inconsistency in weakening of modalities in `iApply`2022-04-20T14:59:17ZRobbert KrebbersInconsistency in weakening of modalities in `iApply````coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens...```coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens is that the first (and failing) `iApply` directly attempts to find an `IntoWand` instance to match the conclusion of the wand with the goal. This fails because the only applicable `IntoWand` instance is:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
There is no `FromAssumption` for `Q`, so no weakening of the conclusion is performed.
In the second attempt, `iApply` will first `iSpecialize` with the wand. As such, it tries to find an `IntoWand` instance where the conclusion can be unified with an evar. Then after that, it will use `iAssumption`, which uses `FromAssumption` to weaken the modality.
## Solution
We probably should add `FromAssumption` to instances like `into_wand_wand`. I do not know if this was just an omission, or there's a reason for that. Should try.https://gitlab.mpi-sws.org/iris/iris/-/issues/458Inconsistency in weakening of modalities in `iApply`2022-05-01T11:54:32ZRobbert KrebbersInconsistency in weakening of modalities in `iApply````coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens...```coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens is that the first (and failing) `iApply` directly attempts to find an `IntoWand` instance to match the conclusion of the wand with the goal. This fails because the only applicable `IntoWand` instance is:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
There is no `FromAssumption` for `Q`, so no weakening of the conclusion is performed.
In the second attempt, `iApply` will first `iSpecialize` with the wand. As such, it tries to find an `IntoWand` instance where the conclusion can be unified with an evar. Then after that, it will use `iAssumption`, which uses `FromAssumption` to weaken the modality.
## Solution
We probably should add `FromAssumption` to instances like `into_wand_wand`. I do not know if this was just an omission, or there's a reason for that. Should try.https://gitlab.mpi-sws.org/iris/iris/-/issues/540Inconsistent lemma statements and names: Some_equiv_eq vs the equivalent lemm...2023-08-10T06:43:42ZRalf Jungjung@mpi-sws.orgInconsistent lemma statements and names: Some_equiv_eq vs the equivalent lemma on dist```
Some_equiv_eq:
∀ {A : Type} {H : Equiv A} (mx : option A) (y : A), mx ≡ Some y ↔ (∃ y' : A, mx = Some y' ∧ y' ≡ y)
```
vs
```
dist_Some_inv_l':
∀ {A : ofe} (n : nat) (my : option A) (x : A),
Some x ≡{n}≡ my → ∃ x' : A, Some x...```
Some_equiv_eq:
∀ {A : Type} {H : Equiv A} (mx : option A) (y : A), mx ≡ Some y ↔ (∃ y' : A, mx = Some y' ∧ y' ≡ y)
```
vs
```
dist_Some_inv_l':
∀ {A : ofe} (n : nat) (my : option A) (x : A),
Some x ≡{n}≡ my → ∃ x' : A, Some x' = my ∧ x ≡{n}≡ x'
dist_Some_inv_r':
∀ {A : ofe} (n : nat) (mx : option A) (y : A),
mx ≡{n}≡ Some y → ∃ y' : A, mx = Some y' ∧ y ≡{n}≡ y'
```https://gitlab.mpi-sws.org/iris/iris/-/issues/267Inconsistent order of arguments for `inv_alloc` and `cinv_alloc`.2019-11-01T13:07:58ZDan FruminInconsistent order of arguments for `inv_alloc` and `cinv_alloc`.```
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
```
vs
```
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
```
As you can see, `inv_a...```
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
```
vs
```
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
```
As you can see, `inv_alloc` first takes the namespace and then the mask, but `cinv_alloc` first takes the mask and the the namespace.https://gitlab.mpi-sws.org/iris/iris/-/issues/526iNext does not remove diamonds from hypotheses2023-06-29T11:00:37ZJules JacobsiNext does not remove diamonds from hypothesesiNext does not remove diamonds from hypotheses.
This feature could be useful, as otherwise you have to iMod everything.
Example:
```
From iris Require Import proofmode.tactics.
Lemma foo {PROP : bi} (P : PROP) :
◇ P ⊢ ▷ P.
Proof.
i...iNext does not remove diamonds from hypotheses.
This feature could be useful, as otherwise you have to iMod everything.
Example:
```
From iris Require Import proofmode.tactics.
Lemma foo {PROP : bi} (P : PROP) :
◇ P ⊢ ▷ P.
Proof.
iIntros "H". iNext.
Admitted.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/74iNext does not strip off both laters from ▷ P ∗ ▷ Q2017-05-19T15:20:29ZRalf Jungjung@mpi-sws.orgiNext does not strip off both laters from ▷ P ∗ ▷ QI would expect the following test to succeed:
```
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) :
▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
iIntros "H". iNext. iAssumption.
Qed.
```I would expect the following test to succeed:
```
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) :
▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
iIntros "H". iNext. iAssumption.
Qed.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/99iNext does not strip off later below existential2017-10-02T13:34:05ZRalf Jungjung@mpi-sws.orgiNext does not strip off later below existential```
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
```
Stripping off laters does happen below con...```
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
```
Stripping off laters does happen below conjunctions, but not below existentials.https://gitlab.mpi-sws.org/iris/iris/-/issues/55iNext unfolds things (more than simpl) even when there is no later to strip2018-02-20T00:50:15ZRalf Jungjung@mpi-sws.orgiNext unfolds things (more than simpl) even when there is no later to stripSee <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/02ef8176f01f8de0563a2f5a8e1444bb9ee01b6d/theories/typing/cont.v#L40>: The context goas from
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : elctx_interp E qE
"HL" ...See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/02ef8176f01f8de0563a2f5a8e1444bb9ee01b6d/theories/typing/cont.v#L40>: The context goas from
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : elctx_interp E qE
"HL" : llctx_interp L1 1
"HT" : tctx_interp tid (T' args)
```
to
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : [∗ list] k↦x ∈ E, (λ (_ : nat) (x0 : elctx_elt), elctx_elt_interp x0 qE) k x
"HL" : [∗ list] k↦x ∈ L1, (λ (_ : nat) (x0 : llctx_elt), llctx_elt_interp x0 1) k x
"HT" : [∗ list] k↦x ∈ T' args, (λ (_ : nat) (x0 : tctx_elt), tctx_elt_interp tid x0) k x
```
but no later is removed. Not even simpl unfolds these definitions.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/147Infrastructure for the `monPred_all` modality2018-07-13T08:51:27ZJacques-Henri JourdanInfrastructure for the `monPred_all` modalityIf everything in the context is objective, then we should be able to introduce the `monPred_all` modality. This should reuse the infrastructure of `iAlways`.
However, I would like to go a bit further: Actually, in the case everything in...If everything in the context is objective, then we should be able to introduce the `monPred_all` modality. This should reuse the infrastructure of `iAlways`.
However, I would like to go a bit further: Actually, in the case everything in the context is objective, and the goal is objective too, we might want to switch to Iris proofmode to get rid of embeddings and all that.https://gitlab.mpi-sws.org/iris/iris/-/issues/400Integrate Tej's simp-lang?2021-02-17T08:49:46ZRalf Jungjung@mpi-sws.orgIntegrate Tej's simp-lang?@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an [accompanying Youtube video](https://www.youtube.com/watch?v=HndwyM04...@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an [accompanying Youtube video](https://www.youtube.com/watch?v=HndwyM04KEU&feature=youtu.be)! I took a look and watched the video, and I really like it.
I propose we give this more visibility by referencing it from the Iris repo and website, and also we should find some way to ensure that the Coq code remains compatible with latest Iris. The easiest way to do that would be to add an "iris_simp_lang" package in this repository and move the code there. The README could go into the subfolder. @tchajed would that work for you, or did you have other plans? I don't want to appropriate your work, just ensure that it does not bitrot. I could imagine declaring you the maintainer of that subdirectory, so you could e.g. merge MRs for it yourself. @robbertkrebbers what do you think?
I also have some more specific low-level comments, which I leave here just so I do not forget -- but it probably make more sense to discuss the high-level points first. It's really just one remark so far:
* In `heap_ra`, I find it confusing that you end up basically copying (parts of) `gen_heap`. IMO it would make more sense to either use `gen_heap`, or else (for the purpose of exposition) to define something that specifically works for values and locations of this language, but then it should not be called "gen(eral)".https://gitlab.mpi-sws.org/iris/iris/-/issues/396Intro pattern `>` has wrong behavior with side-conditions of `iMod`2021-04-29T09:25:46ZRobbert KrebbersIntro pattern `>` has wrong behavior with side-conditions of `iMod````coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> ...```coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
Proof.
iIntros ">H".
```
fails with
```
In environment
Σ : gFunctors
heapG0 : heapG Σ
E1, E2 : coPset
P : iProp Σ
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11809)
(environments.env_spatial ?M11809) ?M11814"
with
"∀ (σ : language.state heap_lang) (e' : language.expr heap_lang) (κ :
list
(language.observation
heap_lang))
(σ' : language.state heap_lang) (efs : list (language.expr heap_lang)),
language.prim_step (#() #()) σ κ e' σ' efs
→ match stuckness_to_atomicity NotStuck with
| StronglyAtomic => is_Some (language.to_val e')
| WeaklyAtomic => irreducible e' σ'
end".
```
See also https://mattermost.mpi-sws.org/iris/pl/r47q3gcq4fddxnhpddj91yb1wyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/95Introduce implication if premise is persistent2017-08-24T08:49:51ZRalf Jungjung@mpi-sws.orgIntroduce implication if premise is persistentCurrently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the g...Currently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the goal is `box P -> Q`, introducing should be possible even for a non-empty spatial context.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/506Introducing a "step-taking" modality2023-02-16T09:40:14ZJonas KastbergIntroducing a "step-taking" modalityIn this issue I propose the introduction of a "step-taking" modality `|~>`, that captures the intuition of
"taking a step in the operational semantics", at the logical level.
The purpose of this is to allow defining ghost theories at an ...In this issue I propose the introduction of a "step-taking" modality `|~>`, that captures the intuition of
"taking a step in the operational semantics", at the logical level.
The purpose of this is to allow defining ghost theories at an abstraction-level above the program logic,
while still getting the benefits of the various later-stripping mechanisms (such as later credits) that have
been introduced in Iris.
A WIP demonstration of the modality can be found in !887.
A tl;dr is:
- Presence of multiple laters can reduce intuition behind ghost theory (and in some cases make them impossible to state (see below))
- Iris has means of stripping such multiple laters during every physical step
- One can capture the intuition of having to taking a physical step via a modality (`|~>`)
- One can then use this modality in ghost rules
Ultimately we would obtain the following:
```
TCEq (to_val e) None → E2 ⊆ E1 →
|~{E1,E2}~> P -∗
WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗
WP e @ s; E1 {{ Φ }}.
```
Ghost theory rules that were usually of the form `P -* |={E}=> Q`
will now simply have the form `P -* |~{E}~> Q`.
Now for a more detailed explanation of the benefits of this, and limitations of existing solutions, see the discussion below.
Since the addition of the later credits (and other similar later-stripping procedures),
it is now possible to strip multiple laters during a single (physical) step of the operational semantics.
This let us build nice abstractions for some ghost abstractions to hide the laters from the user (e.g. nested invariants).
However, some ghost theories are not able to fully benefit from this extension.
Consider the following ghost theory that allows bidirectional transfer of some resources `P`:
- There are two fragments that each track the resource to be transferred `P`.
- There is a context which is indexed by two numbers, that tracks how many copies of `P` is in transit in either direction.
- Resources are transferred from one side by incrementing the respective number.
- Resources are received from one side by decrementing the other number.
- Sending a resource from one side requires stripping an amount of laters corresponding to the number of resources in transit towards you (i.e. from the other side).
The later requirement is simply instrumented here for the sake of the example.
Something more realistic, which has the later requirement is the Actris Ghost Theory (pg. 45 of https://iris-project.org/pdfs/2022-lmcs-actris2-final.pdf).
We can make this concrete with the following definitions and rules:
- There are three resources `my_ctx γ n m`, `my_frag_l γ P`, and `my_frag_r γ P`.
- There are five rules:
```
1. |- |==> ∃ γ, my_ctx γ 0 0 * my_frag_l γ P * my_frag_r γ P
2. |- my_ctx γ n m * my_frag_l γ P * P ==* ▷^m my_ctx (S n) m * my_frag_l γ P
3. |- my_ctx γ n m * my_frag_r γ P * P ==* ▷^n my_ctx n (S m) * my_frag_r γ P
4. |- my_ctx γ n (S m) P * my_frag_l γ P ==* ▷ my_ctx n m * my_frag_l γ P * P
5. |- my_ctx γ (S n) m P * my_frag_r γ P ==* ▷ my_ctx n m * my_frag_r γ P * P
```
Rule 2. and 3. shows how sending a resources requires stripping multiple laters.
It is possible to employ this ghost theory for a program, thanks to the new later-stripping mechanisms.
However, imagine the following.
We build an abstraction on top of the ghost theory, to construct a new ghost theory, in which we _hide_ the context (and thereby the numbers related to how many steps we need to strip).
In the new ghost theory we have the following:
- There is a fragment for either side `my_frag_l' γ n m P` and `my_frag_r' γ n m P`,
that govern how many times a they have sent a resource (n), and how many times they have received one (m).
- There are two additional fragments `my_idx_l γ i`, `my_idx_r γ i` that are duplicable evidence of how many resources have been sent in either direction (in total)
- It is imperative that either fragment does not know about the others counter, as we wish full separation between them.
This ghost theory abstraction is achievable by putting `my_ctx` in an invariant,
that is included inside each new fragment,
along with ghost state to tie the invariant together with the former local fragment.
In this case, we cannot create a ghost theory, as we do not know the number of laters to strip, outside of the invariant!
Imagine the following rule corresponding to rule 2.:
```
my_frag_l' γ n m P * P ==* ▷^??? my_frag_l' γ (S n) m P * my_idx_l γ n
```
In fact, the only possible rule is something like the following (mask and atomicity details omitted):
```
my_frag_l' γ n P -* P -*
WP e { v. (my_frag_l' γ (S n) P * my_idx_l γ n)-* Φ v } -*
WP e { Φ }
```
This is achieved by adding fragments of the later-stripping mechanism to the internal invariant,
which then lets us strip the appropriate amount of laters in the context of a WP.
In particular, the WP lets us access the internal `state_interp`, which in turn includes the authoritative
parts of the later-stripping mechanisms.
However, this rule is very unsatisfactory, as we are now working at the level of the WP, instead of a higher level of abstraction.
As such, I propose the addition of a "step-taking" modality `|~>`.
Essentially, it would frame the later-stripping mechanism governed by the state interpretation,
while guaranteeing that it is updated appropriately.
Intuitively, it captures the notion of "taking a step" in the operational semantics.
As such, the modality would enjoy the following rule (mask and atomicity details omitted):
```
|~> Q -*
WP e { v. Q -* Φ v } -*
WP e { Φ }
```
This would allow the aforementioned ghost theory rule to be expressed as follows:
```
my_frag_l' γ n m P * P -* |~> my_frag_l' γ (S n) m P * my_idx_l γ n
```
This now preserves a higher level of abstraction, by reading as:
"I can give up my resources, _when taking a (physical) step_, to obtain the new resources".
As I do not have a deep understanding of the later credits, I cannot give a precise definition of `|~>`,
although I discussed something similar with @simonspies at the Iris Workshop 2022, who may have a good suggestion.
In the case of the simple later-stripping mechanism in HeapLang,
I have defined and mechanised the lemmas for the following in Coq:
```
|~{E1,E2}~> P ≜
∀ n, steps_auth n ={E1,E2}=∗
(steps_auth n ∗ (|={∅}▷=>^(S n) (steps_auth (S n) -∗
steps_auth (S n) ∗ |={E2,E1}=> P)))
```
For the application level, one can then determine the lower bound of `n` with the local fragments
kept inside the ghost theory, along with the given `steps_auth n`, to conclude that enough laters
can be stripped.
The `steps_auth` fragment can then be given back to resolve the left conjunct.
After the ghost step has been taken, the updated `steps_auth` can be obtained, to reflect its updates
in the local ghost state.
The weakest precondition rule can be proven, as we simply give ownership of the internal `steps_auth n`
to the `P -* |~> Q` assumption, to unify the amount of laters that can be stripped `n`.
Similarly, we give the updated `steps_auth (S n)` to resolve the final update in the step-taking modality.
I managed to prove all of the following lemmas in Coq, given my above definition of the modality:
```
TCEq (to_val e) None → E2 ⊆ E1 →
|~{E1,E2}~> P -∗
WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗
WP e @ s; E1 {{ Φ }}.
```
```
↑N ⊆ E →
my_frag_l' γ n m P -∗ P -∗
step_update E (E ∖ ↑N) (my_frag_l' γ (S n) m P ∗ my_idx_l γ n).
```
This in turn let me derive the above "ghost" rule that worked at the level of the weakest precondition:
```
my_frag_l' γ n P -* P -*
WP e { v. (my_frag_l' γ (S n) P * my_idx_l γ n)-* Φ v } -*
WP e { Φ }
```
EDIT:
Some refactoring, and added a better overview in the top
EDIT:
Added reference to MR
EDIT:
After further looking into the existing lemmas regarding later stripping in HeapLang, a suitable definition of the modality might already be found in https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/program_logic/weakestpre.v#L350
That is:
```
Definition step_update E1 E2 P : iProp Σ :=
∃ n, (∀ σ ns κs nt, state_interp σ ns κs nt ={E1,∅}=∗
⌜n ≤ S (num_laters_per_step ns)⌝) ∧
(|={E1∖E2,∅}=> |={∅}▷=>^n |={∅,E1∖E2}=> P).
```
With this, the aforementioned rule can even be changed to simply use the modality instead of the in-line
proposition.
Proving rules for this definition seems feasible too, and compositionality of the modality should work out.
EDIT: The above is not enough, as it does not capture how the ghost theory may be updated based on the new state of the state interpretation, but it does give an impression of how something like this modality was already in place in Iris.