Always 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 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.)