[Maybe] Make uPred work on OFEs
I spent some time last week talking with Santiago, a student of Andrew Appel, and trying to figure out the exact relation of their and our model. We did not reach a definitive conclusion. In particular, we could not tell where exactly our CMRA requirements of non-expansiveness and the extension axiom appear in their model.
However, one thing became clear: They do have a separation algebra on what Santiago called "juicy heap", which is a heap that can store either values or assertions (so, it combines our physical state and invariant maps). Separation algebras are relational, so they had no trouble with equality not being decidable. (And Santiago confirmed my belief that working with this relational composition is a huge pain in many other places.) However, they also did not have to go through the length of having a limit construction corresponding to what our agreement CMRA does. This is not entirely surprising, we know we don't actually need these limits and in their approach, all these proof obligations are coming up and discharged much more "on-demand", and much later. (For example, they have to be really, really careful when defining the meaning of what corresponds to our invariant assertion. If they screw up, they will only notice much later, when some proof rule does not work out. On the other hand, all we have to check is non-expansiveness of the definition.)
It would be nice if we would not have to unnecessarily complicate our model with this limit construction. That would also give us a better position when comparing with Appel's stuff ;-)
Cc @robbertkrebbers I guess this is blocked on "sorting the canonical structure mess" ;-)