Introducing a "step-taking" modality
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
, andmy_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
andmy_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.