Implement ORAs

[jlohse-mpi-sws]

This PR rebases iris-lean on ordered resource algebras (MoSeL) following this Zulip discussion

The main goal is being able to support distributional probabilistic logics, which all need a custom order (PSL, Lilac, Bluebell, pcOL, Amaryllis, opOL). To my understanding, the lack of ORAs is the only reason why the iris-lean implementations of Lilac and Bluebell are currently not uPred instances. The Lilac paper even explicitly mentions the lack of support for a custom order as a main obstruction for mechanizing Lilac in Iris. Another use case of ORAs are linear (non-affine) logics.

I'm putting up the draft implementation for discussion. Doing such a change would mean deviating from Iris-Rocq, since this is not yet implemented there.

All CMRA constructions generalize naturally to a custom order, Auth is affine-only.

Updates and all the uPred laws that involve weakening are affine-only: it is a known limitation that this doesn't work for linear logics.

iProp is also affine-only right now: all infrastructure for higher-order ghost state relies on updates, so I don't see a use-case for non-affine iProp right now, and making it affine-only omits a lot of side conditions.

While the original MoSeL ORA definition only allows reflexive orders, I changed this for compatibility: CMRA does not need a reflexive order, only UCMRA does.

Change List:

• the name "CMRA" now refers to ORAs, following Markus' Proposal
• The CMRA definition is no longer monolithic, but the laws are split Mathlib-style across Typeclasses that bundle the operation together with their laws (ie Op includes the CMRA laws that are only about Op). This avoids duplicating axioms for cmras with and without extension order, and is in general more modular.
• Homomorphisms now need to respect the order and preserve affiness.
• (u)ORAs with the extension order are built using (u)CMRA.withExtensionOrder. For those CMRAs, the order computationally reduces to the extension order.
• discrete CMRAs must ignore the step index for the order
• The generic ViewRel needs new monotonicity axioms and corresponding infrastructure

Currently a draft because I haven't reviewed every line of AI-generated code. I carefully checked that the code implements what it should. In case the iris-lean community agrees that ORAs should end up upstream, I'm happy to invest the additional time to review the code line-by-line before handing it over.