gmap_view_auth: add fraction

theories/algebra/lib/gmap_view.v

@@ -132,8 +132,8 @@ Definition gmap_viewO (K : Type) `{Countable K} (V : ofeT) : ofeT :=
 Section definitions.
   Context {K : Type} `{Countable K} {V : ofeT}.
 
-  Definition gmap_view_auth (m : gmap K V) : gmap_viewR K V :=
-    ●V m.
+  Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
+    ●V{q} m.
   Definition gmap_view_frag (k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
     ◯V {[k := (dq, to_agree v)]}.
 End definitions.
@@ -142,10 +142,10 @@ Section lemmas.
   Context {K : Type} `{Countable K} {V : ofeT}.
   Implicit Types (m : gmap K V) (k : K) (q : Qp) (dq : dfrac) (v : V).
 
-  Global Instance : Params (@gmap_view_auth) 4 := {}.
-  Global Instance gmap_view_auth_ne : NonExpansive (gmap_view_auth (K:=K) (V:=V)).
+  Global Instance : Params (@gmap_view_auth) 5 := {}.
+  Global Instance gmap_view_auth_ne q : NonExpansive (gmap_view_auth (K:=K) (V:=V) q).
   Proof. solve_proper. Qed.
-  Global Instance gmap_view_auth_proper : Proper ((≡) ==> (≡)) (gmap_view_auth (K:=K) (V:=V)).
+  Global Instance gmap_view_auth_proper q : Proper ((≡) ==> (≡)) (gmap_view_auth (K:=K) (V:=V) q).
   Proof. apply ne_proper, _. Qed.
 
   Global Instance : Params (@gmap_view_frag) 6 := {}.
@@ -171,10 +171,30 @@ Section lemmas.
   Qed.
 
   (** Composition and validity *)
-  Lemma gmap_view_auth_valid m : ✓ gmap_view_auth m.
+  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ ✓ q.
   Proof.
-    apply view_auth_valid. intros n l ? Hl. rewrite lookup_empty in Hl. done.
+    rewrite view_auth_frac_valid. split; first by naive_solver.
+    intros. split; first done.
+    intros n l ? Hl. rewrite lookup_empty in Hl. done.
   Qed.
+  Lemma gmap_view_auth_valid m : ✓ gmap_view_auth 1 m.
+  Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
+
+  Lemma auth_auth_frac_op p q m :
+    gmap_view_auth (p + q) m ≡ gmap_view_auth p m ⋅ gmap_view_auth q m.
+  Proof. apply view_auth_frac_op. Qed.
+  Lemma auth_auth_frac_op_invN n p m1 q m2 :
+    ✓{n} (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡{n}≡ m2.
+  Proof. apply view_auth_frac_op_invN. Qed.
+  Lemma auth_auth_frac_op_inv p m1 q m2 :
+    ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡ m2.
+  Proof. apply view_auth_frac_op_inv. Qed.
+  Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
+    ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 = m2.
+  Proof. apply view_auth_frac_op_inv_L, _. Qed.
+  Global Instance auth_auth_frac_is_op q q1 q2 m :
+    IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
+  Proof. rewrite /gmap_view_auth. apply _. Qed.
 
   Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
   Proof.
@@ -213,28 +233,38 @@ Section lemmas.
     ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 = v2.
   Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
 
+  Lemma gmap_view_both_frac_validN n q m k dq v :
+    ✓{n} (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
+      ✓ q ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
+  Proof.
+    rewrite /gmap_view_auth /gmap_view_frag.
+    rewrite view_both_frac_validN gmap_view_rel_lookup.
+    naive_solver.
+  Qed.
   Lemma gmap_view_both_validN n m k dq v :
-    ✓{n} (gmap_view_auth m ⋅ gmap_view_frag k dq v) ↔
+    ✓{n} (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
       ✓ dq ∧ m !! k ≡{n}≡ Some v.
+  Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
+  Lemma gmap_view_both_frac_valid q m k dq v :
+    ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
+    ✓ q ∧ ✓ dq ∧ m !! k ≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
-    rewrite view_both_validN.
-    apply gmap_view_rel_lookup.
+    rewrite view_both_frac_valid. setoid_rewrite gmap_view_rel_lookup.
+    split=>[[Hq Hm]|[Hq Hm]].
+    - split; first done. split.
+      +  apply (Hm 0%nat).
+      +  apply equiv_dist=>n. apply Hm.
+    - split; first done. split.
+      + apply Hm.
+      + revert n. apply equiv_dist. apply Hm.
   Qed.
   Lemma gmap_view_both_valid m k dq v :
-    ✓ (gmap_view_auth m ⋅ gmap_view_frag k dq v) ↔
+    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
     ✓ dq ∧ m !! k ≡ Some v.
-  Proof.
-    rewrite /gmap_view_auth /gmap_view_frag.
-    rewrite view_both_valid. setoid_rewrite gmap_view_rel_lookup.
-    split; intros Hm; split.
-    - apply (Hm 0%nat).
-    - apply equiv_dist=>n. apply Hm.
-    - apply Hm.
-    - revert n. apply equiv_dist. apply Hm.
-  Qed.
+  Proof. rewrite gmap_view_both_frac_valid. naive_solver done. Qed.
   Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
-    ✓ (gmap_view_auth m ⋅ gmap_view_frag k dq v) ↔
+    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
     ✓ dq ∧ m !! k = Some v.
   Proof. unfold_leibniz. apply gmap_view_both_valid. Qed.
 
@@ -242,7 +272,7 @@ Section lemmas.
   Lemma gmap_view_alloc m k dq v :
     m !! k = None →
     ✓ dq →
-    gmap_view_auth m ~~> gmap_view_auth (<[k := v]> m) ⋅ gmap_view_frag k dq v.
+    gmap_view_auth 1 m ~~> gmap_view_auth 1 (<[k := v]> m) ⋅ gmap_view_frag k dq v.
   Proof.
     intros Hfresh Hdq. apply view_update_alloc=>n bf Hrel j [df va] /=.
     rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
@@ -261,8 +291,8 @@ Section lemmas.
   Qed.
 
   Lemma gmap_view_delete m k v :
-    gmap_view_auth m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
-    gmap_view_auth (delete k m).
+    gmap_view_auth 1 m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
+    gmap_view_auth 1 (delete k m).
   Proof.
     apply view_update_dealloc=>n bf Hrel j [df va] Hbf /=.
     destruct (decide (j = k)) as [->|Hne].
@@ -276,8 +306,8 @@ Section lemmas.
   Qed.
 
   Lemma gmap_view_update m k v v' :
-    gmap_view_auth m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
-      gmap_view_auth (<[k := v']> m) ⋅ gmap_view_frag k (DfracOwn 1) v'.
+    gmap_view_auth 1 m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
+      gmap_view_auth 1 (<[k := v']> m) ⋅ gmap_view_frag k (DfracOwn 1) v'.
   Proof.
     apply view_update=>n bf Hrel j [df va] /=.
     rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].

theories/base_logic/algebra.v

@@ -242,7 +242,7 @@ Section gmap_view.
   Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
 
   Lemma gmap_view_both_validI m k dq v :
-    ✓ (gmap_view_auth m ⋅ gmap_view_frag k dq v) ⊢@{uPredI M}
+    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ⊢@{uPredI M}
     ✓ dq ∧ m !! k ≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
@@ -257,6 +257,7 @@ Section gmap_view.
     rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
     rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
   Qed.
+
 End gmap_view.
 
 End upred.

theories/base_logic/lib/gen_heap.v

@@ -97,8 +97,8 @@ Section definitions.
     (* The [⊆] is used to avoid assigning ghost information to the locations in
     the initial heap (see [gen_heap_init]). *)
     ⌜ dom _ m ⊆ dom (gset L) σ ⌝ ∧
-    own (gen_heap_name hG) (gmap_view_auth (σ : gmap L (leibnizO V))) ∗
-    own (gen_meta_name hG) (gmap_view_auth (m : gmap L gnameO)).
+    own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO V))) ∗
+    own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L gnameO)).
 
   Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
     own (gen_heap_name hG) (gmap_view_frag l (DfracOwn q) (v : leibnizO V)).
@@ -133,9 +133,9 @@ Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_interp σ.
 Proof.
-  iMod (own_alloc (gmap_view_auth (σ : gmap L (leibnizO V)))) as (γh) "Hh".
+  iMod (own_alloc (gmap_view_auth 1 (σ : gmap L (leibnizO V)))) as (γh) "Hh".
   { exact: gmap_view_auth_valid. }
-  iMod (own_alloc (gmap_view_auth (∅ : gmap L gnameO))) as (γm) "Hm".
+  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L gnameO))) as (γm) "Hm".
   { exact: gmap_view_auth_valid. }
   iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
   iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.

theories/base_logic/lib/proph_map.v

@@ -44,7 +44,7 @@ Section definitions.
   Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
     (∃ R, ⌜proph_resolves_in_list R pvs ∧
           dom (gset _) R ⊆ ps⌝ ∗
-          own (proph_map_name pG) (gmap_view_auth (V:=listO $ leibnizO V) R))%I.
+          own (proph_map_name pG) (gmap_view_auth (V:=listO $ leibnizO V) 1 R))%I.
 
   Definition proph_def (p : P) (vs : list V) : iProp Σ :=
     own (proph_map_name pG) (gmap_view_frag (V:=listO $ leibnizO V) p (DfracOwn 1) vs).
@@ -75,7 +75,7 @@ End list_resolves.
 Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
   ⊢ |==> ∃ _ : proph_mapG P V PVS, proph_map_interp pvs ps.
 Proof.
-  iMod (own_alloc (gmap_view_auth ∅)) as (γ) "Hh".
+  iMod (own_alloc (gmap_view_auth 1 ∅)) as (γ) "Hh".
   { apply gmap_view_auth_valid. }
   iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
   iPureIntro. done.

theories/base_logic/lib/wsat.v

@@ -54,7 +54,7 @@ Instance: Params (@ownD) 3 := {}.
 
 Definition wsat `{!invG Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
-    own invariant_name (gmap_view_auth (invariant_unfold <$> I)) ∗
+    own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I)) ∗
     [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
 
 Section wsat.
@@ -106,7 +106,7 @@ Lemma ownD_singleton_twice i : ownD {[i]} ∗ ownD {[i]} ⊢ False.
 Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
 
 Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
-  own invariant_name (gmap_view_auth (invariant_unfold <$> I)) ∗
+  own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I)) ∗
   own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)) ⊢
   ∃ Q, ⌜I !! i = Some Q⌝ ∗ ▷ (Q ≡ P).
 Proof.
@@ -188,7 +188,7 @@ End wsat.
 Lemma wsat_alloc `{!invPreG Σ} : ⊢ |==> ∃ _ : invG Σ, wsat ∗ ownE ⊤.
 Proof.
   iIntros.
-  iMod (own_alloc (gmap_view_auth ∅)) as (γI) "HI";
+  iMod (own_alloc (gmap_view_auth 1 ∅)) as (γI) "HI";
     first by apply gmap_view_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.