Jacques-Henri Jourdan (8d798c30) at 07 Feb 08:18
Bump
Slightly simpler protocol for non-atomic invariants.
Anyway, I opened this MR thinking that this new version was "obviously more intuitive", and apparently I was wrong, so I'm going to close the MR since it does not bring any new feature to Iris.
I don't use a name for the "already closed" case. The full namespace is used.
As for the other "name", it's not really the name of the invariant, it's just a ghost name for the "already open" token.
So there is really not "two names". I would say there is none, apart from the ghost name of the token.
Also, this new construction avoid the use of the fairly advanced lemma gset_disj_alloc_empty_updateP_strong
.
I would say that two simple ghost states is better than one product ghost state. At least, that's what we do usually.
Sure.
I am also tempted to split the two ghost states into two (an exclusive token, with a new ghost name for each invariant, and namespaces of NA invs).
Are you convinced? Should I close the MR?