Support stored propositions
It would be nice to have support for "Stored propositions" as described in http://www-users.cs.york.ac.uk/~miked/publications/verifying_custom_sync_constructs.pdf.
@kaspersv suggested they could be hacked into Iris without changing in the model. Let me quote his mail (with some parts of my mail also being inline):
And finally, of course, there's the question whether this could be done in Iris. I am sure we could have the following proof rule:
\inv^i (P) * \inv^i (Q) => \later (P <=> Q)
Indeed, we can even strengthen it to inv^j (P) * inv^j (Q) => later (P = Q) because the interpretation of inv is slightly stronger in Iris than rintrp is in iCAP. In particular, inv^j (P) asserts that the invariant is n-equal to P, while iCAP only asserts that the region interpretation is n-equal to the given predicate when applied to any future world of the current world.
but we can't easily use the trick you did, with the 2-state STS, in order to not actually store a P in the invariant. Did you think about this?
Yes, we did think about an encoding, using two mutually exclusive ghost resources gh(0) and gh(1). The idea would be to create an invariant (P * gh(0)) / gh(1) and transfer gh(1) to the region. Then the question boils down to:
(P * gh(0)) / gh(1) = (Q * gh(0)) / gh(1) |- P = Q
I don’t think it is possible to prove this internally and we weren’t sufficiently motivated to check if it holds in the semantics, but it seems like it should.
As an alternative, @janno and me tossed around the idea of letting the user chose an arbitrary, locally non-expansive functor to construct the ghost monoid. That would allow the user to make use of my agreement construction, with "Ag(\later Prop)" being in the ghost monoid. This would then let the user do stored propositions without hacks like the above. @robbertkrebbers also seemed to like that. However, we would lose the axiom that ghost ownership is timeless, and I see no easy way to regain it for the part of the functor that has a discrete metric. So, probably, we would want to keep both a discrete monoid (where ownership is timeless) and a functor (where crazy things can happen) in the interface, and pair them together ourselves - which raises the question if that's worth it. The model would end up with a 4-tuple-monoid instead of the three-tuples is has currently (invariants, ghost, physical). Right now, I cannot imagine using any other monoid with propositions embedded. Of course it would be nice to have, for example, STSs with states indexed by propositions, but actually doing that would require making this STS a functor, and showing all the functorial properties and local non-expansiveness and so on - probably it would be much easier to go with stored propositions and index the STS by the name instead. For that reason, right now, I'd prefer the solution suggested by @kaspersv if it works.
@jtassaro: I mentioned this yesterday during our conversation.