Structured Invariant identifiers
I'm starting to get pretty annoyed working with global invariant names in Iris. In particular, if I have a library that creates multiple invariants, I can parameterise its specification with an infinite set of names that the library can use. However, it is very annoying to have to refer to particular distinct elements of this set in a precise way.
I believe proof outlines would benefit if we had an invariant identifier resource, unused(mask), that expressed that no invariants existed with an identifier in mask. This would allow the allocator to choose a name for invariants upon allocation, by consuming an unused resource:
unused({ i }) * later P view-shift inv(i, P)
and of course the unused resource could be split arbitrarily:
unused(mask_1 \uplus mask_2) <=> unused(mask_1) * unused(mask_2)
Libraries would then be parameterised by a single invariant identifier i and require the user to transfer ownership of unused({ concat(i, i') }) to the library upon instantiation. This would allow the library to use any invariant identifier starting with i for its invariants. In particular, it could choose to create two invariants with identifiers concat(i, "0") and concat(i, "1"), which would automatically be distinct in proof outlines.
I don't believe it is possible to define the unused resource in Iris, so I propose to extended Iris with a primitive invariant identifier resource.
Any comments or ideas for better solutions?