From 12796181c286c12c43c68c202abfa3ef5aec3d5b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Sep 2020 17:06:46 +0200
Subject: [PATCH] Add documentation for auth & view.

---
 theories/algebra/auth.v | 28 ++++++++++---------
 theories/algebra/view.v | 61 ++++++++++++++++++++++++++++++-----------
 2 files changed, 60 insertions(+), 29 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 1d6798329..1284f10c8 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -3,23 +3,25 @@ From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Import base_logic.
 From iris Require Import options.
 
-(** The authoritative camera with fractional authoritative elements. The camera
-[auth] has 3 types of elements: the fractional authoritative element [●{q} a],
-the full authoritative element [● a ≡ ●{1} a], and the fragment [◯ b] (of which
-there can be several). Updates are only possible with the full authoritative
-element [● a], while fractional authoritative elements have agreement, i.e.,
-[✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)
+(** The authoritative camera with fractional authoritative elements *)
+(** The authoritative camera has 2 types of elements: the authoritative
+element [●{q} a] and the fragment [◯ b] (of which there can be several). To
+enable sharing of the authoritative element [●{q} a], it is equiped with a
+fraction [q]. Updates are only possible with the full authoritative element
+[● a] (syntax for [●{1} a]]), while fractional authoritative elements have
+agreement, i.e., [✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)
 
 (** * Definition of the view relation *)
+(** The authoritative camera is obtained by instantiating the view camera. *)
 Definition auth_view_rel_raw {A : ucmraT} (n : nat) (a b : A) : Prop :=
   b ≼{n} a ∧ ✓{n} a.
 Lemma auth_view_rel_raw_mono (A : ucmraT) n1 n2 (a1 a2 b1 b2 : A) :
-  auth_view_rel_raw n1 a1 b1 → a1 ≡{n1}≡ a2 → b2 ≼{n1} b1 → n2 ≤ n1 →
+  auth_view_rel_raw n1 a1 b1 → a1 ≡{n2}≡ a2 → b2 ≼{n2} b1 → n2 ≤ n1 →
   auth_view_rel_raw n2 a2 b2.
 Proof.
   intros [??] Ha12 ??. split.
-  - apply cmra_includedN_le with n1; [|done]. rewrite -Ha12. by trans b1.
-  - apply cmra_validN_le with n1; [|lia]. by rewrite -Ha12.
+  - trans b1; [done|]. rewrite -Ha12. by apply cmra_includedN_le with n1.
+  - rewrite -Ha12. by apply cmra_validN_le with n1.
 Qed.
 Lemma auth_view_rel_raw_valid (A : ucmraT) n (a b : A) :
   auth_view_rel_raw n a b → ✓{n} b.
@@ -38,7 +40,7 @@ Proof.
   - by apply cmra_discrete_valid_iff_0.
 Qed.
 
-(** * Definition and operations on auth *)
+(** * Definition and operations on the authoritative camera *)
 (** The type [auth] is not defined as a [Definition], but as a [Notation].
 This way, one can use [auth A] with [A : Type] instead of [A : ucmraT], and let
 canonical structure search determine the corresponding camera instance. *)
@@ -59,7 +61,7 @@ Notation "â—¯ a" := (auth_frag a) (at level 20).
 Notation "●{ q } a" := (auth_auth q a) (at level 20, format "●{ q }  a").
 Notation "● a" := (auth_auth 1 a) (at level 20).
 
-(** * Laws *)
+(** * Laws of the authoritative camera *)
 Section auth.
   Context {A : ucmraT}.
   Implicit Types a b : A.
@@ -210,8 +212,8 @@ Section auth.
     ◯ b1 ≼ ●{p} a ⋅ ◯ b2 ↔ b1 ≼ b2.
   Proof. apply view_frag_included. Qed.
 
-  (** The weaker [view_both_included] lemmas below are a consequence of the
-  [view_auth_included] and [view_frag_included] lemmas above. *)
+  (** The weaker [auth_both_included] lemmas below are a consequence of the
+  [auth_auth_included] and [auth_frag_included] lemmas above. *)
   Lemma auth_both_includedN n p1 p2 a1 a2 b1 b2 :
     ●{p1} a1 ⋅ ◯ b1 ≼{n} ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
   Proof. apply view_both_includedN. Qed.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 9b777f8ef..a0bae0dc4 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -4,23 +4,52 @@ From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Import base_logic.
 From iris Require Import options.
 
-(** The view camera with fractional authoritative parts. The camera [view] has
-3 types of elements: the fractional authoritative [●V{q} a], the full
-authoritative [●V a ≡ ●V{1} a], and the non-authoritative [◯V a]. Updates are
-only possible with the full authoritative element [●V a], while fractional
-authoritative elements have agreement: [✓ (●V{p} a ⋅ ●V{q} b) → a ≡ b]. *)
+(** The view camera with fractional authoritative elements *)
+(** The view camera, which is reminiscent of the views framework, is used to
+provide a logical/"small-footprint" "view" of some "large-footprint" piece of
+data, which can be shared in the separation logic sense, i.e., different parts
+of the data can be separately owned by different functions or threads. This is
+achieved using the two elements of the view camera:
+
+- The authoritative element [●V a], which describes the data under consideration.
+- The fragment [â—¯V b], which provides a logical view of the data [a].
+
+To enable sharing of the fragments, the type of fragments is equipped with a
+camera structure so ownership of fragments can be split. Concretely, fragments
+enjoy the rule [â—¯V (b1 â‹… b2) = â—¯V b1 â‹… â—¯V b2].
+
+To enable sharing of the authoritative element [●V{q} a], it is equipped with a
+fraction [q]. Updates are only possible with the full authoritative element
+[●V a] (syntax for [●V{1} a]]), while fractional authoritative elements have
+agreement, i.e., [✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡ a2]. *)
 
 (** * The view relation *)
-(** The view camera is parametrized by a (step-indexed) relation
-[view_rel n a b] that relates the authoritative element [a] to the composition
-of all fragments [b]. This relation should be a.) down-closed w.r.t. the
-step-indexed [n], b.) non-expansive w.r.t. the argument [a], c.) monotone w.r.t.
-the argument [b], d.) ensure validity of the argument [b]. *)
+(** To relate the authoritative element [a] to its possible fragments [b], the
+view camera is parametrized by a (step-indexed) relation [view_rel n a b]. This
+relation should be a.) closed under smaller step-indexes [n], b.) non-expansive
+w.r.t. the argument [a], c.) closed under smaller [b] (which implies
+non-expansiveness w.r.t. [b]), and d.) ensure validity of the argument [b].
+
+Note 1: Instead of requiring both a step-indexed and a non-step-indexed version
+of the relation (like cameras do for validity), we use [∀ n, view_rel n] as the
+non-step-indexed version. This is anyway necessary when using [≼{n}] as the
+relation (like the authoritative camera does) as its non-step-indexed version
+is not equivalent to [∀ n, x ≼{n} y].
+
+Note 2: The view relation is defined as a canonical structure so that given a
+relation [nat → A → B → Prop], the instance with the laws can be inferred. We do
+not use type classes for this purpose because cameras themselves are represented
+using canonical structures. It has proven fragile for a canonical structure
+instance to take a type class as a parameter (in this case, [viewR] would need
+to take a class with the view relation laws). *)
 Structure view_rel (A : ofeT) (B : ucmraT) := ViewRel {
   view_rel_holds :> nat → A → B → Prop;
   view_rel_mono n1 n2 a1 a2 b1 b2 :
     view_rel_holds n1 a1 b1 →
-    a1 ≡{n1}≡ a2 → b2 ≼{n1} b1 → n2 ≤ n1 → view_rel_holds n2 a2 b2;
+    a1 ≡{n2}≡ a2 →
+    b2 ≼{n2} b1 →
+    n2 ≤ n1 →
+    view_rel_holds n2 a2 b2;
   view_rel_validN n a b :
     view_rel_holds n a b → ✓{n} b
 }.
@@ -64,7 +93,7 @@ Notation "●V{ q } a" := (view_auth q a) (at level 20, format "●V{ q }  a").
 Notation "●V a" := (view_auth 1 a) (at level 20).
 Notation "â—¯V a" := (view_frag a) (at level 20).
 
-(** * Ofe *)
+(** * The OFE structure *)
 Section ofe.
   Context {A B : ofeT} (rel : nat → A → B → Prop).
   Implicit Types a : A.
@@ -111,7 +140,7 @@ Section ofe.
   Proof. by uPred.unseal. Qed.
 End ofe.
 
-(** * Camera *)
+(** * The camera structure *)
 Section cmra.
   Context {A B} (rel : view_rel A B).
   Implicit Types a : A.
@@ -161,14 +190,14 @@ Section cmra.
   Instance view_op : Op (view rel) := λ x y,
     View (view_auth_proj x â‹… view_auth_proj y) (view_frag_proj x â‹… view_frag_proj y).
 
-  Definition view_valid_eq :
+  Local Definition view_valid_eq :
     valid = λ x,
       match view_auth_proj x with
       | Some (q, ag) =>
          ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
       | None => ✓ view_frag_proj x
       end := eq_refl _.
-  Definition view_validN_eq :
+  Local Definition view_validN_eq :
     validN = λ n x, 
       match view_auth_proj x with
       | Some (q, ag) => ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
@@ -473,7 +502,7 @@ Section cmra.
   Qed.
 End cmra.
 
-(** * Functor *)
+(** * Utilities to construct functors *)
 (** Due to the dependent type [rel] in [view] we cannot actually define
 instances of the functor structures [rFunctor] and [urFunctor]. Functors can
 only be defined for instances of [view], like [auth]. To make it more convenient
-- 
GitLab