[Maybe] Remove invariants
I am reasonably sure that having higher-order ghost state, we can remove invariants and masks from core Iris and instead just have an assertion annotated at WP that is preserved throughout execution.
Cc @kaspersv @robbertkrebbers
Changes to the model
Worlds are removed from the global resources. World satisfaction becomes significantly simpler: Masks are removed, and we are left with
\sigma |= r := {n | r \in V_{n} /\ r.\pi = ex(\sigma)}
(Or maybe we still have to make this trivial at step-index 0, I am not sure.) This simplification is the main pay-off of the change. Of course, the complexity is not just gone, but it it moved from the model to the logic -- following the usual pattern that we saw over and over again with Iris.
Masks are just removed from primitive view shifts. For WP, of course masks are removed, but we need to add something instead: We need to add a way for an assertion to be preserved at every single step of execution. So, we get something like
wp_I(e, \Lam v. Q) = \Lam r n. \All r_f, \sigma, m, ...
(\Exists r_I. I r_I (m+1) /\ (m+1) \in \sigma |= (r * r_I * r_f)) ...
=> \Exists s_1, s_2. (\Exists r_I. I r_I m /\ m \in \sigma |= (s_1 * s_2 * r_I * r_f))
...
In other words, besides the frame r_f, we demand that there is some resource r_I satisfying I, both before and after the step has been taken. This replaces the former existential quantification over some map defining the resources backing the invariants, which was part of world satisfaction.
Changes to the logic
Remove the invariant assertions and all rules related to invariants or masks. We obtain a new form of the atomic rule of consequence. This is how it looks for Hoare triples:
P * I ==> P' * I'
{P'} e {Q'}_I'
Q' * I' ==> Q * I
e atomic
-------------------
{P} e {Q}_I
I have yet to figure out the most elegant way to write this as a WP rule. We also need a weakening rule, maybe like this:
I <=> I' * I_f
{P'} e {Q'}_I'
-------------------
{P} e {Q}_I
All the other rules force the I to be the same in all constituents.
Recovering invariants
To recover invariants, we first define the I
that we typically use for triples. It is pretty much exactly the part we removed from world satisfaction, but expressed inside the logic:
W(E) := \Exists S \in \finpowerset(N). own ... (\authfull S) *
\Sep_{i \in S \cap E} \Exists P : iProp. \later P * i |=> P
In other words, there is some ghost state tracking which invariants are allocated. This ghost state has the structure Auth(\finpowerset(N))
, where we use union (not disjoint!) as composition on N. Furthermore, for all invariants that exist and that are enabled in the mask E
, there is a saved proposition defining which is the invariant with that index, and the invariant is enforced.
We can then recover a WP / Hoare triple with mask E
by using I := W(E)
. Furthermore, we define
P |={E1,E2}=> Q := P * W(E1) ==> P * W(E2)
inv i P := own ... (\authfrag {i}) * i |=> P
We can then prove the old atomic rule of consequence, as well as the invariant-related view shifts, inside the logic. We can go even further and, for example, allow creating an invariant that is open:
E infinite
-------------------
W(E) ==> \Exists i \in E. inv i P * W(E \ {i})
This was not possible previously as there was no way to bind the i
in the new mask.
Open questions
Right now (in current Iris), the forked-off thread actually has a different mask than the local thread. I think to model this, we need a WP with two I
annotations: One for the current thread, one for all forked-off threads. Maybe there has to be some relationship between these two. I am not sure how exactly this would look.
The weakening rule looks a little strange, and may not even be strong enough. What is the I_f
to weaken W(E)
to a smaller mask?