Some valuable comments and invaluable proofs in flock.v

theories/lib/flock.v

@@ -50,19 +50,23 @@ Record flock_name := {
   flock_state_name : gname;
   (** -//- for keeping track of all propositions in the flock *)
   flock_props_name : gname;
-  (** -//- for keeping track of the "active" propositions,
-      once you relase the lock you need to know that the set of the active propositions
+  (** -//- for keeping track of the "active" propositions.
+      Once you relase the lock you need to know that the set of the active propositions
       has not changed since you have acquired it *)
   flock_props_active_name : gname
 }.
 
-(* Defined as `positive` so that we have a `Fresh` instance for `gset positive`.
+(** The data about pending and active propositions will be stored in
+the maps `prop_id -> _` *)
+(* `prop_id` is fefined as `positive` so that we have a `Fresh` instance for `gset positive`.
    Doubles as an invariant name. *)
 Definition prop_id := positive.
 Canonical Structure gnameC := leibnizC gname.
 
-(** The trick here is to store only ghost names associated with a 'flock resource' in the flock invariant.
-    If we start storing propositions, then we end up in the LATER HELL *)
+(** One of the tricks in this lock is to store only ghost names associated with a 'flock resource' in the flock invariant.
+    If we start storing propositions, then we end up in the LATER HELL.
+    The `lock_res_name` datastructure contains all the ghosts names needed to manage an individual proposition.
+ *)
 Record lock_res_name := {
   flock_cinv_name : gname;
   flock_token1_name : gname;
@@ -70,6 +74,22 @@ Record lock_res_name := {
 }.
 Canonical Structure lock_res_nameC := leibnizC lock_res_name.
 
+
+(** Before we define the type of flock resources, we need to have
+    access to the appropriate CMRAs.
+
+   The totality of propositions , and the pending propositions will be
+   represented as a map:
+
+   `prop_id → frac * ag (flock_res_name)`,
+
+   so a standart ghost heap. Active propositions will be modelled by a map
+
+   `excl (prop_id → frac * ag (flock_res_name))`.
+
+   In other words, this map will contain *exact* information of which propositions are active and with what fractions were they activated.
+
+ *)
 Class flockG Σ :=
   FlockG {
     flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
@@ -81,27 +101,26 @@ Class flockG Σ :=
     flock_tokens :> inG Σ (exclR unitC);
   }.
 
+Definition flockΣ : gFunctors :=
+  #[GFunctor (authR (optionUR (exclR lockstateC)))
+   ;lockΣ
+   ;cinvΣ
+   ;GFunctor (authR (optionUR (exclR (gmapC prop_id (prodC fracC lock_res_nameC)))))
+   ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR lock_res_nameC))))%CF].
+
+Instance subG_flockΣ Σ : subG flockΣ Σ → flockG Σ.
+Proof. solve_inG. Qed.
+
 Record lock_res `{flockG Σ} := {
   res_prop : iProp Σ;
   res_frac : frac;
   res_name : lock_res_name;
 }.
 
+(** A "smart constructor" for `lock_res` *)
 Definition LockRes `{flockG Σ} (R : iProp Σ) (π : frac) (ρ : lock_res_name) :=
   {| res_prop := R; res_frac := π; res_name := ρ |}.
 
-(* TODO: DF, finish this *)
-(* Definition flockΣ : gFunctors := *)
-(*   #[GFunctor (authR (optionUR (exclR lockstateC))) *)
-(*    ;lockΣ *)
-(*    ;savedPropΣ *)
-(*    ;GFunctor fracR *)
-(*    ;GFunctor (authR (optionUR (exclR (gmapC prop_id PropPermC)))) *)
-(*    ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))%CF]. *)
-
-(* Instance subG_flockΣ Σ : subG flockΣ Σ → flockG Σ. *)
-(* Proof. solve_inG. Qed. *)
-
 Section flock.
   Context `{heapG Σ, flockG Σ}.
   Variable N : namespace.
@@ -115,13 +134,10 @@ Section flock.
   Definition token₂ (ρ : lock_res_name) : iProp Σ :=
     own (flock_token2_name ρ) (Excl ()).
 
-  (* Definition C' (X : lock_res) : iProp Σ := *)
-  (*   (res_prop X ∗ token₁ (res_name X) ∨ token₂ (res_name X))%I. *)
-
   Definition C (R : iProp Σ) (ρ : lock_res_name) : iProp Σ :=
     (R ∗ token₁ ρ ∨ token₂ ρ)%I.
 
-  (* Tokens that allow you to get all the propositions from `A` out of the invariants *)
+  (** Tokens that allow you to get all the propositions from `A` out of the invariants *)
   Definition all_tokens (P : gmap prop_id lock_res_name) : iProp Σ :=
     ([∗ map] i ↦ X ∈ P, token₂ X)%I.
 
@@ -129,11 +145,22 @@ Section flock.
   Definition from_active (A : gmap prop_id (frac * lock_res_name))
     := fmap snd A.
 
+
+  (** A flock resource `s ↦ X,π,γ` contains:
+      - Knowledge that the `s ↦{π} γ` is in the set of propositions managed by the flock;
+      - There is a cancellable invariant `C X γ`;
+      - We have π- permissiones to access that invariant.
+   *)
   Definition flock_res (γ : flock_name) (s : prop_id) (X : lock_res) : iProp Σ :=
     (own (flock_props_name γ) (◯ {[s := (res_frac X, to_agree (res_name X))]})
     ∗ cinv (resN.@s) (flock_cinv_name (res_name X)) (C (res_prop X) (res_name X))
     ∗ cinv_own (flock_cinv_name (res_name X)) (res_frac X))%I.
 
+  (** Basically says that the propositions from the map `A` are active.
+      This predicate is designed to contain enough information to deactivate those propositions.
+
+      When we are deactivating the propositions we need to make sure that the set of the active propositions has not changed. That's why we need a CMRA to keep track of the exact contents of that set.
+ *)
   Definition flocked
     (γ : flock_name) (A : gmap prop_id lock_res) : iProp Σ :=
     (∃ fa : gmap prop_id (frac * lock_res_name),
@@ -151,22 +178,38 @@ Section flock.
     : gmapUR prop_id (prodR fracR (agreeR lock_res_nameC)) :=
     fmap (λ X, (1%Qp, to_agree X)) f.
 
+  (** TODO: can we actually get rid of the `to_props_map` here? *)
   Definition flock_inv (γ : flock_name) : iProp Σ :=
     (∃ (s : lockstate)
        (** fa -- active propositions, fp -- pending propositions *)
        (fa : gmap prop_id (frac * lock_res_name))
        (fp : gmap prop_id lock_res_name),
+       (** ... and those sets are disjoint *)
        ⌜fp ##ₘ from_active fa⌝ ∗
        own (flock_state_name γ) (● (Excl' s)) ∗
+       (** the totality of resources: fp ∪ fa *)
        own (flock_props_name γ) (● to_props_map (fp ∪ from_active fa)) ∗
+       (** but we also need to know the exact contents of fa *)
        own (flock_props_active_name γ) (● Excl' fa) ∗
+       (** the invariant keeps track of the tokens (token₂) for the
+           pending resource; when we activate a resource, we transfer
+           this token to the client, which uses it to open the
+           cinvariant and get the actual proposition. *)
        all_tokens fp ∗
        match s with
        | Locked =>
+         (** If the lock is acuired, then we hold on to the token from the "old" specification *)
          locked (flock_lock_name γ) ∗
-         ([∗ map] i ↦ πX ∈ fa, own (flock_props_name γ) (◯ {[i:=(πX.1,to_agree πX.2)]}))
+         (** .. and we take hold of all the ghost pointsto `s ↦{π} ρ`.
+
+             This is necessary to have if we want to free the
+             resources. If we wish to free the resource `s ↦{1} ρ`,
+             then we need to know that it is not currently active (has
+             not been acquired). The predicate below ensures that. *)
+         ([∗ map] i ↦ πρ ∈ fa, own (flock_props_name γ) (◯ {[i:=(πρ.1,to_agree πρ.2)]}))
        | Unlocked =>
-         (* there are no active proposition *)
+         (** If the lock is NOT acquired, then there are no active
+         proposition *)
          own (flock_props_active_name γ) (◯ Excl' ∅)
        end)%I.
 
@@ -178,34 +221,46 @@ Section flock.
   (** * Lemmata **)
 
   (** ** Basic properties of the CAPs *)
-  (* Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) (π1 π2 : frac) : *)
-  (*   flock_res γ s R (π1+π2) ⊣⊢ flock_res γ s R π1 ∗ flock_res γ s R π2. *)
-  (* Proof. *)
-  (*   rewrite /flock_res. iSplit. *)
-  (*   - iDestruct 1 as (ρ) "(Hs & #Hinv & Hρ)". *)
-  (*     iDestruct "Hρ" as "[Hρ1 Hρ2]". *)
-  (*     iDestruct "Hs" as "[Hs1 Hs2]". *)
-  (*     iSplitL "Hρ1 Hs1"; iExists _; by iFrame. *)
-  (*   - iIntros "[H1 H2]". *)
-  (*     iDestruct "H1" as (ρ) "(Hs1 & #Hinv1 & Hρ1)". *)
-  (*     iDestruct "H2" as (ρ') "(Hs2 & #Hinv2 & Hρ2)". *)
-  (*     iCombine "Hs1 Hs2" as "Hs". *)
-  (*     iDestruct (own_valid with "Hs") *)
-  (*       as %Hfoo%auth_valid_discrete. *)
-  (*     simpl in Hfoo. apply singleton_valid in Hfoo. *)
-  (*     destruct Hfoo as [_ Hfoo%agree_op_inv']. *)
-  (*     fold_leibniz. rewrite -!Hfoo. *)
-  (*     iCombine "Hρ1 Hρ2" as "Hρ". *)
-  (*     rewrite !frac_op' agree_idemp. *)
-  (*     iExists ρ. by iFrame. *)
-  (* Qed. *)
-
-  (* Global Instance flock_res_fractional γ s R : Fractional (flock_res γ s R). *)
-  (* Proof. intros p q. apply flock_res_op. Qed. *)
-
-  (* Global Instance flock_res_as_fractional γ s R π : *)
-  (*   AsFractional (flock_res γ s R π) (flock_res γ s R) π. *)
-  (* Proof. split. done. apply _. Qed. *)
+  (* TODO, we only have this for the "smart constructor" *)
+  Lemma flock_res_agree (γ : flock_name) (s : prop_id) (R1 R2 : iProp Σ) ρ1 ρ2 (π1 π2 : frac) :
+    flock_res γ s (LockRes R1 π1 ρ1) -∗
+    flock_res γ s (LockRes R2 π2 ρ2) ==∗
+    ⌜ρ1 = ρ2⌝.
+  Proof.
+    rewrite /flock_res.
+    iDestruct 1 as "(Hs1 & #Hinv1 & Hρ1)".
+    iDestruct 1 as "(Hs2 & #Hinv2 & Hρ2)".
+    iCombine "Hs1 Hs2" as "Hs".
+    iDestruct (own_valid with "Hs")
+      as %Hfoo%auth_valid_discrete.
+    simpl in Hfoo. apply singleton_valid in Hfoo.
+    destruct Hfoo as [_ Hfoo%agree_op_inv']. eauto.
+  Qed.
+
+  Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) ρ (π1 π2 : frac) :
+    flock_res γ s (LockRes R (π1+π2) ρ)
+ ⊣⊢ flock_res γ s (LockRes R π1 ρ) ∗ flock_res γ s (LockRes R π2 ρ).
+  Proof.
+    rewrite /flock_res. iSplit.
+    - iDestruct 1 as "(Hs & #Hinv & Hρ)".
+      iDestruct "Hρ" as "[Hρ1 Hρ2]".
+      iDestruct "Hs" as "[Hs1 Hs2]".
+      iSplitL "Hρ1 Hs1"; by iFrame.
+    - iIntros "[H1 H2]".
+      iDestruct "H1" as "(Hs1 & #Hinv1 & Hρ1)".
+      iDestruct "H2" as "(Hs2 & #Hinv2 & Hρ2)".
+      iCombine "Hs1 Hs2" as "Hs". iFrame.
+      rewrite /C /=. iFrame "Hinv1".
+  Qed.
+
+  Global Instance flock_res_fractional γ s R ρ :
+    Fractional (λ π, flock_res γ s (LockRes R π ρ)).
+  Proof. intros p q. apply flock_res_op. Qed.
+
+  Global Instance flock_res_as_fractional γ s R π ρ :
+    AsFractional (flock_res γ s (LockRes R π ρ))
+                 (λ π, flock_res γ s (LockRes R π ρ)) π.
+  Proof. split. done. apply _. Qed.
 
   Lemma to_props_map_singleton_included fp i q ρ:
     {[i := (q, to_agree ρ)]} ≼ to_props_map fp → fp !! i = Some ρ.
@@ -596,15 +651,6 @@ Section flock.
     by apply auth_update_alloc.
   Qed.
 
-  (* THIS IS NOT TRUE *)
-  Global Instance snd_cmramorphism :
-    CmraMorphism (@snd Qp (agree lock_res_name)).
-  Proof.
-    split; first apply _.
-    - move=> n [? ?] [// ?].
-    - move=> [a b]/=. admit.
-  Admitted.
-
   Lemma acquire_flock_spec γ lk (I : gmap prop_id lock_res) :
     {{{ is_flock γ lk ∗ [∗ map] i ↦ X ∈ I, flock_res γ i X }}}
       acquire lk
@@ -681,11 +727,11 @@ Section flock.
           snd <$> f <$> I ≼ snd <$> g <$> fp
           =  to_agree o res_name <$> I ≼ to_agree <$> fp *)
         assert (((snd <$> (f <$> I)) : gmapUR prop_id (agreeR lock_res_nameC)) ≼ (snd <$> (g <$> fp))) as Hbar.
-        { (* TODO: this is the /proper/ proof of the statement, but
-             the proof is incorrect because currently projections are
-             not morphisms *)
-          eapply cmra_morphism_monotone; last exact: Hfoo.
-          apply gmap_fmap_cmra_morphism. apply _.
+        { (* TODO DOESN"T  WORK SAD *)
+          (* Check (gmap_fmap_mono snd (f <$> I) (g <$> fp)). *)
+          admit.
+          (* eapply cmra_morphism_monotone; last exact: Hfoo. *)
+          (* apply gmap_fmap_cmra_morphism. apply _. *)
         }
         rewrite -!map_fmap_compose in Hbar.
         assert ((to_agree ∘ res_name <$> I) ≼ to_agree <$> fp) as Hbaz by exact: Hbar.
@@ -748,7 +794,7 @@ Section flock.
       iFrame. iSplit; eauto.
       rewrite big_sepM_fmap.
       iApply (big_sepM_own_frag with "Hemp HI").
-  Qed.
+  Admitted.
 
   Lemma release_cancel_spec' γ lk I :
     {{{ is_flock γ lk ∗ flocked γ I }}}