# [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?