The view camera.
This MR implements #257 (closed): a view camera that generalize authoritative camera. The camera view A B rel
is parametrized by an OFE A
for the authoritative elements, a camera B
for the fragments, and a step-indexed relation rel
that relates the two.
To show that the view camera indeed generalizes the authoritative camera, I have implemented the authoritative camera auth
in terms of the view camera. The new implementation is pretty much a drop-in replacement, as shown by that fact that the whole of Iris compiles without any changes.
Some notes:
- I have defined the laws for the view relation using a canonical structure instead of a type class. My experience is that parameterizing a canonical structure (in this case, the camera instance for view) by a type class is pretty unreliable.
- I removed a bunch of lemmas about
auth
that break the abstraction of●
/◯
and used theAuth
constructor directly. This will likely cause some breakage in reverse dependencies, but I'm happy to fix that. I still need to write a bunch of documentation (as comments). I will do this after some initial feedback.
TODOs for future MRs:
- Define the heap/gmap camera (!486 (merged)) in terms of the view camera and the discardable fractions camera (!497 (merged)).
- Define the camera for monotone partial bijections (!91 (closed)) in terms of the view camera.
- Develop a theory of local updates for the view camera. Currently there are just lemmas like
view_update
that use the view relation directly in the premise. The current lemmas are sufficient to prove the local update lemmas forauth
. - Define the view relation in terms of
siProp
. To do this, it makes sense to first define validity✓
, inclusion≼
, etc, assiProp
s, otherwise there is little point to that. - Investigate sealing the view/auth definitions. It's often the case (already prior to the MR) that Coq loops if you apply the wrong auth lemma. Sealing might fix that.
Edited by Robbert Krebbers