Skip to content

WIP: Prototype a validity restriction CMRA construction

Tej Chajed requested to merge tchajed/iris-coq:cmra-restrict-valid into master

Implement a first cut at building a CMRA by restricting the validity of an existing CMRA. We demonstrate the construction by building a CmraMixin for auth that starts with a CMRA built from combinators and primitives.

The implementation actually transports a structure A:cmraT to B:Type across an isomorphism iso A B, which is a bijection using Leibniz equality. It also takes an arbitrary restriction of A's validity over B, along with all of the validity-related CMRA laws. Unlike what I attempted in !348 (closed) this is a much more principled solution, leveraging the fact that we really have an isomorphism.

The implementation is a total mess. There are three high-level problems:

  • The instances for iso are scoped too broadly. When I imported them in agree.v I got a typeclass resolution loop.
  • I'm not sure about how canonical structures work out with this approach, given the way it uses an instance of the iso typeclass.
  • The proofs for auth are extremely messy and should re-use the existing nice proofs for bits of the old auth construction.

There are also many things the auth library needs which would need to be implemented, many theorems that are generic for any subset construction.

It's not necessarily a problem, but I didn't generalize to transporting a CMRA to an OFE using a bijection that preserves equivalence, because first that's quite a bit more complicated to prove, and second because it would be harder to use for auth where we want to inherit the OFE structure from the CMRA anyway.

@robbertkrebbers and @jung is this the direction you were thinking of? Do we want to pursue this to (1) simplify auth and (2) for other users?

Background: This came up from working on a CMRA isomorphism construction (!348 (closed)), where Robbert mentioned that the motivation was to construct the auth RA by restricting the validity of an RA built from some combinators. In that MR we didn't have an idea of what the spec would look like, so the assumptions we made were rather ad-hoc.

This specific construction, and applying it to auth, was also proposed in #210, phrased as cutting the RA "from the top"; there might be another subset construction but this is the most clearly useful/possible one.

Edited by Tej Chajed

Merge request reports