gmap_view is currently limited to
gmap K V where
V: ofe, hard-coding
agree behavior for the values. This MR lifts that limitation and allows an arbitrary
V: cmra. This is needed, for instance, to equip a lambda-rust/Perennial style heap (with reader-writer locks for data race modeling) with a persistent points-to based on
dfrac: those heaps need a custom RA for handling the lock state, so the old
gmap_view doesn't cut it.
This has the downside that existing users of gmap_view now have to do all the agreement stuff themselves, which can be somewhat painful. I tried my best to add suitable lemmas that make this as easy as possible. In particular,
gmap_view_both_dfrac_valid_discrete_total synergizes well with the new
This MR is based on !957 (merged).