Make view auth take dfrac

iris/algebra/auth.v

@@ -3,12 +3,13 @@ From iris.algebra Require Import proofmode_classes big_op.
 From iris.prelude Require Import options.
 
 (** 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]. *)
+(** The authoritative camera has 2 types of elements: the authoritative element
+[●{dq} a] and the fragment [◯ b] (of which there can be several). To enable
+sharing of the authoritative element [●{dq} a], it is equiped with a
+discardable fraction [dq]. Updates are only possible with the full
+authoritative element [● a] (syntax for [●{#1} a]]), while fractional
+authoritative elements have agreement, i.e., [✓ (●{dq1} a1 ⋅ ●{dq2} a2) → a1 ≡
+a2]. *)
 
 (** * Definition of the view relation *)
 (** The authoritative camera is obtained by instantiating the view camera. *)
@@ -61,7 +62,7 @@ Definition authO (A : ucmra) : ofe := viewO (A:=A) (B:=A) auth_view_rel.
 Definition authR (A : ucmra) : cmra := viewR (A:=A) (B:=A) auth_view_rel.
 Definition authUR (A : ucmra) : ucmra := viewUR (A:=A) (B:=A) auth_view_rel.
 
-Definition auth_auth {A: ucmra} : Qp → A → auth A := view_auth.
+Definition auth_auth {A: ucmra} : dfrac → A → auth A := view_auth.
 Definition auth_frag {A: ucmra} : A → auth A := view_frag.
 
 Typeclasses Opaque auth_auth auth_frag.
@@ -69,9 +70,13 @@ Typeclasses Opaque auth_auth auth_frag.
 Global Instance: Params (@auth_auth) 2 := {}.
 Global Instance: Params (@auth_frag) 1 := {}.
 
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
+Notation "●{ dq } a" := (auth_auth dq a) (at level 20, format "●{ dq }  a").
+Notation "●{# q } a" := (auth_auth (DfracOwn q) a) (at level 20, format "●{# q }  a").
+Notation "●□ a" := (auth_auth (DfracDiscarded) a) (at level 20).
+Notation "● a" := (auth_auth (DfracOwn 1) a) (at level 20).
 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 of the authoritative camera *)
 (** We omit the usual [equivI] lemma because it is hard to state a suitably
@@ -82,9 +87,9 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
-  Global Instance auth_auth_ne q : NonExpansive (@auth_auth A q).
+  Global Instance auth_auth_ne dq : NonExpansive (@auth_auth A dq).
   Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_auth_proper q : Proper ((≡) ==> (≡)) (@auth_auth A q).
+  Global Instance auth_auth_proper dq : Proper ((≡) ==> (≡)) (@auth_auth A dq).
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_ne : NonExpansive (@auth_frag A).
   Proof. rewrite /auth_frag. apply _. Qed.
@@ -102,8 +107,8 @@ Section auth.
 
   Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
   Proof. apply _. Qed.
-  Global Instance auth_auth_discrete q a :
-    Discrete a → Discrete (ε : A) → Discrete (●{q} a).
+  Global Instance auth_auth_discrete dq a :
+    Discrete a → Discrete (ε : A) → Discrete (●{dq} a).
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
   Proof. rewrite /auth_frag. apply _. Qed.
@@ -111,10 +116,10 @@ Section auth.
   Proof. apply _. Qed.
 
   (** Operation *)
-  Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
+  Lemma auth_auth_frac_op dq1 dq2 a : ●{dq1 ⋅ dq2} a ≡ ●{dq1} a ⋅ ●{dq2} a.
   Proof. apply view_auth_frac_op. Qed.
-  Global Instance auth_auth_frac_is_op q q1 q2 a :
-    IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
+  Global Instance auth_auth_frac_is_op dq dq1 dq2 a :
+    IsOp dq dq1 dq2 → IsOp' (●{dq} a) (●{dq1} a) (●{dq2} a).
   Proof. rewrite /auth_auth. apply _. Qed.
 
   Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
@@ -146,21 +151,21 @@ Section auth.
   Proof. apply (big_opMS_commute _). Qed.
 
   (** Validity *)
-  Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
+  Lemma auth_auth_frac_op_invN n dq1 a dq2 b : ✓{n} (●{dq1} a ⋅ ●{dq2} b) → a ≡{n}≡ b.
   Proof. apply view_auth_frac_op_invN. Qed.
-  Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
+  Lemma auth_auth_frac_op_inv dq1 a dq2 b : ✓ (●{dq1} a ⋅ ●{dq2} b) → a ≡ b.
   Proof. apply view_auth_frac_op_inv. Qed.
-  Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
-    ✓ (●{p} a ⋅ ●{q} b) → a = b.
+  Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} dq1 a dq2 b :
+    ✓ (●{dq1} a ⋅ ●{dq2} b) → a = b.
   Proof. by apply view_auth_frac_op_inv_L. Qed.
 
-  Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{n} a.
+  Lemma auth_auth_frac_validN n dq a : ✓{n} (●{dq} a) ↔ ✓dq ∧ ✓{n} a.
   Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
   Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
 
   Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
-    ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
+    ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔  ✓(q1 ⋅ q2) ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
   Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.
   Proof. apply view_auth_op_validN. Qed.
@@ -180,13 +185,13 @@ Section auth.
   Lemma auth_frag_op_validN_2 n b1 b2 : ✓{n} (b1 ⋅ b2) → ✓{n} (◯ b1 ⋅ ◯ b2).
   Proof. apply auth_frag_op_validN. Qed.
 
-  Lemma auth_both_frac_validN n q a b :
-    ✓{n} (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼{n} a ∧ ✓{n} a.
+  Lemma auth_both_frac_validN n dq a b :
+    ✓{n} (●{dq} a ⋅ ◯ b) ↔ ✓dq ∧ b ≼{n} a ∧ ✓{n} a.
   Proof. apply view_both_frac_validN. Qed.
   Lemma auth_both_validN n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
   Proof. apply view_both_validN. Qed.
 
-  Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓ a.
+  Lemma auth_auth_frac_valid dq a : ✓ (●{dq} a) ↔ ✓dq ∧ ✓ a.
   Proof.
     rewrite view_auth_frac_valid !cmra_valid_validN.
     by setoid_rewrite auth_view_rel_unit.
@@ -198,7 +203,7 @@ Section auth.
   Qed.
 
   Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
-    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
+    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓(q1 ⋅ q2) ∧ a1 ≡ a2 ∧ ✓ a1.
   Proof.
     rewrite view_auth_frac_op_valid !cmra_valid_validN.
     setoid_rewrite auth_view_rel_unit. done.
@@ -227,8 +232,8 @@ Section auth.
   (** These lemma statements are a bit awkward as we cannot possibly extract a
   single witness for [b ≼ a] from validity, we have to make do with one witness
   per step-index, i.e., [∀ n, b ≼{n} a]. *)
-  Lemma auth_both_frac_valid q a b :
-    ✓ (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
+  Lemma auth_both_frac_valid dq a b :
+    ✓ (●{dq} a ⋅ ◯ b) ↔  ✓dq ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
   Proof.
     rewrite view_both_frac_valid. apply and_iff_compat_l. split.
     - intros Hrel. split.
@@ -238,11 +243,11 @@ Section auth.
   Qed.
   Lemma auth_both_valid a b :
     ✓ (● a ⋅ ◯ b) ↔ (∀ n, b ≼{n} a) ∧ ✓ a.
-  Proof. rewrite auth_both_frac_valid. naive_solver. Qed.
+  Proof. rewrite auth_both_frac_valid. split; [naive_solver|done]. Qed.
 
   (* The reverse direction of the two lemmas below only holds if the camera is
   discrete. *)
-  Lemma auth_both_frac_valid_2 q a b : (q ≤ 1)%Qp → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
+  Lemma auth_both_frac_valid_2 dq a b : ✓dq → ✓ a → b ≼ a → ✓ (●{dq} a ⋅ ◯ b).
   Proof.
     intros. apply auth_both_frac_valid.
     naive_solver eauto using cmra_included_includedN.
@@ -250,22 +255,22 @@ Section auth.
   Lemma auth_both_valid_2 a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
   Proof. intros ??. by apply auth_both_frac_valid_2. Qed.
 
-  Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} q a b :
-    ✓ (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼ a ∧ ✓ a.
+  Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} dq a b :
+    ✓ (●{dq} a ⋅ ◯ b) ↔ ✓dq ∧ b ≼ a ∧ ✓ a.
   Proof.
     rewrite auth_both_frac_valid. setoid_rewrite <-cmra_discrete_included_iff.
     naive_solver eauto using O.
   Qed.
   Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b :
     ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
-  Proof. rewrite auth_both_frac_valid_discrete. naive_solver. Qed.
+  Proof. rewrite auth_both_frac_valid_discrete. split; [naive_solver|done]. Qed.
 
   (** Inclusion *)
-  Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
-    ●{p1} a1 ≼{n} ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2.
+  Lemma auth_auth_frac_includedN n dq1 dq2 a1 a2 b :
+    ●{dq1} a1 ≼{n} ●{dq2} a2 ⋅ ◯ b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2.
   Proof. apply view_auth_frac_includedN. Qed.
-  Lemma auth_auth_frac_included p1 p2 a1 a2 b :
-    ●{p1} a1 ≼ ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2.
+  Lemma auth_auth_frac_included dq1 dq2 a1 a2 b :
+    ●{dq1} a1 ≼ ●{dq2} a2 ⋅ ◯ b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2.
   Proof. apply view_auth_frac_included. Qed.
   Lemma auth_auth_includedN n a1 a2 b :
     ● a1 ≼{n} ● a2 ⋅ ◯ b ↔ a1 ≡{n}≡ a2.
@@ -274,20 +279,20 @@ Section auth.
     ● a1 ≼ ● a2 ⋅ ◯ b ↔ a1 ≡ a2.
   Proof. apply view_auth_included. Qed.
 
-  Lemma auth_frag_includedN n p a b1 b2 :
-    ◯ b1 ≼{n} ●{p} a ⋅ ◯ b2 ↔ b1 ≼{n} b2.
+  Lemma auth_frag_includedN n dq a b1 b2 :
+    ◯ b1 ≼{n} ●{dq} a ⋅ ◯ b2 ↔ b1 ≼{n} b2.
   Proof. apply view_frag_includedN. Qed.
-  Lemma auth_frag_included p a b1 b2 :
-    ◯ b1 ≼ ●{p} a ⋅ ◯ b2 ↔ b1 ≼ b2.
+  Lemma auth_frag_included dq a b1 b2 :
+    ◯ b1 ≼ ●{dq} a ⋅ ◯ b2 ↔ b1 ≼ b2.
   Proof. apply view_frag_included. Qed.
 
   (** The weaker [auth_both_included] lemmas below are a consequence of the
   [auth_auth_included] and [auth_frag_included] lemmas above. *)
-  Lemma auth_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
-    ●{p1} a1 ⋅ ◯ b1 ≼{n} ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
+  Lemma auth_both_frac_includedN n dq1 dq2 a1 a2 b1 b2 :
+    ●{dq1} a1 ⋅ ◯ b1 ≼{n} ●{dq2} a2 ⋅ ◯ b2 ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
   Proof. apply view_both_frac_includedN. Qed.
-  Lemma auth_both_frac_included p1 p2 a1 a2 b1 b2 :
-    ●{p1} a1 ⋅ ◯ b1 ≼ ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2 ∧ b1 ≼ b2.
+  Lemma auth_both_frac_included dq1 dq2 a1 a2 b1 b2 :
+    ●{dq1} a1 ⋅ ◯ b1 ≼ ●{dq2} a2 ⋅ ◯ b2 ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof. apply view_both_frac_included. Qed.
   Lemma auth_both_includedN n a1 a2 b1 b2 :
     ● a1 ⋅ ◯ b1 ≼{n} ● a2 ⋅ ◯ b2 ↔ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
@@ -314,9 +319,11 @@ Section auth.
     intros. etrans; first exact: auth_update_alloc.
     exact: cmra_update_op_l.
   Qed.
+  Lemma auth_update_auth_persist dq a : ●{dq} a ~~> ●□ a.
+  Proof. apply view_update_auth_persist. Qed.
 
-  Lemma auth_update_frac_alloc q a b `{!CoreId b} :
-    b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
+  Lemma auth_update_frac_alloc dq a b `{!CoreId b} :
+    b ≼ a → ●{dq} a ~~> ●{dq} a ⋅ ◯ b.
   Proof.
     intros Ha%(core_id_extract _ _). apply view_update_frac_alloc=> n bf [??].
     split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.

iris/algebra/dfrac.v

@@ -153,7 +153,7 @@ Section dfrac.
     - by destruct (Qp_add_id_free q q2).
     - by destruct (Qp_add_id_free q q1).
   Qed.
-  Global Instance frac_id_free q : IdFree (DfracOwn q).
+  Global Instance dfrac_own_id_free q : IdFree (DfracOwn q).
   Proof. intros [q'| |q'] _ [=]. by apply (Qp_add_id_free q q'). Qed.
   Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
   Proof. by constructor. Qed.

iris/algebra/lib/gmap_view.v

 From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Export view gmap dfrac.
+From iris.algebra Require Export view gmap frac dfrac.
 From iris.algebra Require Import local_updates proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -12,7 +12,7 @@ persistent read-only ownership of a key.
 
 The key frame-preserving updates are [gmap_view_alloc] to allocate a new key,
 [gmap_view_update] to update a key given full ownership of the corresponding
-fragment, and [gmap_view_freeze] to make a key read-only by discarding any
+fragment, and [gmap_view_persist] to make a key read-only by discarding any
 fraction of the corresponding fragment. Crucially, the latter does not require
 owning the authoritative element.
 
@@ -138,7 +138,7 @@ Section definitions.
   Context {K : Type} `{Countable K} {V : ofe}.
 
   Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
-    ●V{q} m.
+    ●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.
@@ -178,7 +178,7 @@ Section lemmas.
   (** Composition and validity *)
   Lemma gmap_view_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.
+  Proof. by rewrite /gmap_view_auth -dfrac_op_own view_auth_frac_op. Qed.
   Global Instance gmap_view_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.

iris/algebra/lib/gset_bij.v

@@ -106,7 +106,7 @@ Definition gset_bijUR A B `{Countable A, Countable B} : ucmra :=
   viewUR (gset_bij_view_rel (A:=A) (B:=B)).
 
 Definition gset_bij_auth `{Countable A, Countable B}
-  (q : Qp) (L : gset (A * B)) : gset_bij A B := ●V{q} L ⋅ ◯V L.
+  (dq : dfrac) (L : gset (A * B)) : gset_bij A B := ●V{dq} L ⋅ ◯V L.
 Definition gset_bij_elem `{Countable A, Countable B}
   (a : A) (b : B) : gset_bij A B := ◯V {[a, b]}.
 
@@ -118,11 +118,11 @@ Section gset_bij.
   Global Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
   Proof. apply _. Qed.
 
-  Lemma gset_bij_auth_frac_op q1 q2 L :
-    gset_bij_auth q1 L ⋅ gset_bij_auth q2 L ≡ gset_bij_auth (q1 + q2) L.
+  Lemma gset_bij_auth_frac_op dq1 dq2 L :
+    gset_bij_auth dq1 L ⋅ gset_bij_auth dq2 L ≡ gset_bij_auth (dq1 ⋅ dq2) L.
   Proof.
     rewrite /gset_bij_auth view_auth_frac_op.
-    rewrite (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
+    rewrite (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
     by rewrite -core_id_dup (comm _ (◯V _)).
   Qed.
 
@@ -132,21 +132,21 @@ Section gset_bij.
     setoid_rewrite gset_bij_view_rel_iff.
     naive_solver eauto using O.
   Qed.
-  Lemma gset_bij_auth_valid L : ✓ gset_bij_auth 1 L ↔ gset_bijective L.
+  Lemma gset_bij_auth_valid L : ✓ gset_bij_auth (DfracOwn 1) L ↔ gset_bijective L.
   Proof. rewrite gset_bij_auth_frac_valid. naive_solver by done. Qed.
 
   Lemma gset_bij_auth_empty_frac_valid q : ✓ gset_bij_auth (A:=A) (B:=B) q ∅ ↔ ✓ q.
   Proof.
     rewrite gset_bij_auth_frac_valid. naive_solver eauto using gset_bijective_empty.
   Qed.
-  Lemma gset_bij_auth_empty_valid : ✓ gset_bij_auth (A:=A) (B:=B) 1 ∅.
+  Lemma gset_bij_auth_empty_valid : ✓ gset_bij_auth (A:=A) (B:=B) (DfracOwn 1) ∅.
   Proof. by apply gset_bij_auth_empty_frac_valid. Qed.
 
-  Lemma gset_bij_auth_frac_op_valid q1 q2 L1 L2 :
-    ✓ (gset_bij_auth q1 L1 ⋅ gset_bij_auth q2 L2)
-    ↔ ✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1.
+  Lemma gset_bij_auth_frac_op_valid dq1 dq2 L1 L2 :
+    ✓ (gset_bij_auth dq1 L1 ⋅ gset_bij_auth dq2 L2)
+    ↔ ✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1.
   Proof.
-    rewrite /gset_bij_auth (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
+    rewrite /gset_bij_auth (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
     rewrite -view_frag_op (comm _ (◯V _)) assoc. split.
     - move=> /cmra_valid_op_l /view_auth_frac_op_valid.
       setoid_rewrite gset_bij_view_rel_iff. naive_solver eauto using 0.
@@ -154,7 +154,7 @@ Section gset_bij.
       apply view_both_frac_valid. setoid_rewrite gset_bij_view_rel_iff. naive_solver.
   Qed.
   Lemma gset_bij_auth_op_valid L1 L2 :
-    ✓ (gset_bij_auth 1 L1 ⋅ gset_bij_auth 1 L2) ↔ False.
+    ✓ (gset_bij_auth (DfracOwn 1) L1 ⋅ gset_bij_auth (DfracOwn 1) L2) ↔ False.
   Proof. rewrite gset_bij_auth_frac_op_valid. naive_solver. Qed.
 
   Lemma bij_both_frac_valid q L a b :
@@ -165,7 +165,7 @@ Section gset_bij.
     set_solver by eauto using O.
   Qed.
   Lemma bij_both_valid L a b :
-    ✓ (gset_bij_auth 1 L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
+    ✓ (gset_bij_auth (DfracOwn 1) L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
   Proof. rewrite bij_both_frac_valid. naive_solver by done. Qed.
 
   Lemma gset_bij_elem_agree a1 b1 a2 b2 :
@@ -185,7 +185,7 @@ Section gset_bij.
 
   Lemma gset_bij_auth_extend {L} a b :
     (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
-    gset_bij_auth 1 L ~~> gset_bij_auth 1 ({[(a, b)]} ∪ L).
+    gset_bij_auth (DfracOwn 1) L ~~> gset_bij_auth (DfracOwn 1) ({[(a, b)]} ∪ L).
   Proof.
     intros. apply view_update=> n bijL.
     rewrite !gset_bij_view_rel_iff gset_op.

iris/algebra/lib/mono_nat.v

@@ -14,7 +14,7 @@ fragment at the same value so that lemma [mono_nat_included], which states that
 [mono_nat_lb n ≼ mono_nat_auth q n], does not require a frame-preserving
 update. *)
 Definition mono_nat_auth (q : Qp) (n : nat) : mono_nat :=
-  ●{q} MaxNat n ⋅ ◯ MaxNat n.
+  ●{#q} MaxNat n ⋅ ◯ MaxNat n.
 Definition mono_nat_lb (n : nat) : mono_nat := ◯ MaxNat n.
 
 Section mono_nat.
@@ -26,8 +26,8 @@ Section mono_nat.
   Lemma mono_nat_auth_frac_op q1 q2 n :
     mono_nat_auth q1 n ⋅ mono_nat_auth q2 n ≡ mono_nat_auth (q1 + q2) n.
   Proof.
-    rewrite /mono_nat_auth auth_auth_frac_op.
-    rewrite (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite /mono_nat_auth -dfrac_op_own auth_auth_frac_op.
+    rewrite (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
     by rewrite -core_id_dup (comm _ (◯ _)).
   Qed.
 
@@ -60,7 +60,7 @@ Section mono_nat.
   Lemma mono_nat_auth_frac_op_valid q1 q2 n1 n2 :
     ✓ (mono_nat_auth q1 n1 ⋅ mono_nat_auth q2 n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
   Proof.
-    rewrite /mono_nat_auth (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite /mono_nat_auth (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
     rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
     - move=> /cmra_valid_op_l /auth_auth_frac_op_valid. naive_solver.
     - intros [? ->]. rewrite -core_id_dup -auth_auth_frac_op.

iris/base_logic/algebra.v

@@ -145,23 +145,23 @@ Section view.
   Implicit Types b : B.
   Implicit Types x y : view rel.
 
-  Lemma view_both_frac_validI_1 (relI : uPred M) q a b :
+  Lemma view_both_frac_validI_1 (relI : uPred M) dq a b :
     (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
+    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ relI.
   Proof.
     intros Hrel. uPred.unseal. split=> n x _ /=.
     rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
   Qed.
-  Lemma view_both_frac_validI_2 (relI : uPred M) q a b :
+  Lemma view_both_frac_validI_2 (relI : uPred M) dq a b :
     (∀ n (x : M), relI n x → rel n a b) →
-    ⌜q ≤ 1⌝%Qp ∧ relI ⊢ ✓ (●V{q} a ⋅ ◯V b : view rel).
+    ⌜✓dq⌝%Qp ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
   Proof.
     intros Hrel. uPred.unseal. split=> n x _ /=.
     rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
   Qed.
-  Lemma view_both_frac_validI (relI : uPred M) q a b :
+  Lemma view_both_frac_validI (relI : uPred M) dq a b :
     (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
+    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
   Proof.
     intros. apply (anti_symm _);
       [apply view_both_frac_validI_1|apply view_both_frac_validI_2]; naive_solver.
@@ -186,11 +186,11 @@ Section view.
       [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
   Qed.
 
-  Lemma view_auth_frac_validI (relI : uPred M) q a :
+  Lemma view_auth_frac_validI (relI : uPred M) dq a :
     (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V{q} a : view rel) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
+    ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
   Proof.
-    intros. rewrite -(right_id ε op (●V{q} a)). by apply view_both_frac_validI.
+    intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_frac_validI.
   Qed.
   Lemma view_auth_validI (relI : uPred M) a :
     (∀ n (x : M), relI n x ↔ rel n a ε) →
@@ -208,7 +208,7 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
-  Lemma auth_auth_frac_validI q a : ✓ (●{q} a) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ ✓ a.
+  Lemma auth_auth_frac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
   Proof.
     apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].
     split; [|done]. apply ucmra_unit_leastN.
@@ -224,8 +224,8 @@ Section auth.
     rewrite auth_view_rel_exists. by uPred.unseal.
   Qed.
 
-  Lemma auth_both_frac_validI q a b :
-    ✓ (●{q} a ⋅ ◯ b) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+  Lemma auth_both_frac_validI dq a b :
+    ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
   Proof. apply view_both_frac_validI=> n. by uPred.unseal. Qed.
   Lemma auth_both_validI a b :
     ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.

iris/base_logic/lib/gset_bij.v

@@ -38,8 +38,8 @@ Global Instance subG_gset_bijΣ `{Countable A, Countable B} Σ :
 Proof. solve_inG. Qed.
 
 Definition gset_bij_own_auth_def `{gset_bijG Σ A B} (γ : gname)
-    (q : Qp) (L : gset (A * B)) : iProp Σ :=
-  own γ (gset_bij_auth q L).
+    (dq : dfrac) (L : gset (A * B)) : iProp Σ :=
+  own γ (gset_bij_auth dq L).
 Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def). Proof. by eexists. Qed.
 Definition gset_bij_own_auth := unseal gset_bij_own_auth_aux.
 Definition gset_bij_own_auth_eq :
@@ -69,23 +69,23 @@ Section gset_bij.
   Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
 
   Global Instance gset_bij_own_auth_fractional γ L :
-    Fractional (λ q, gset_bij_own_auth γ q L).
+    Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L).
   Proof.
     intros p q. rewrite gset_bij_own_auth_eq -own_op gset_bij_auth_frac_op //.
   Qed.
   Global Instance gset_bij_own_auth_as_fractional γ q L :
-    AsFractional (gset_bij_own_auth γ q L) (λ q, gset_bij_own_auth γ q L) q.
+    AsFractional (gset_bij_own_auth γ (DfracOwn q) L) (λ q, gset_bij_own_auth γ (DfracOwn q) L) q.
   Proof. split; [auto|apply _]. Qed.
 
-  Lemma gset_bij_own_auth_agree γ q1 q2 L1 L2 :
-    gset_bij_own_auth γ q1 L1 -∗ gset_bij_own_auth γ q2 L2 -∗
-    ⌜✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1⌝.
+  Lemma gset_bij_own_auth_agree γ dq1 dq2 L1 L2 :
+    gset_bij_own_auth γ dq1 L1 -∗ gset_bij_own_auth γ dq2 L2 -∗
+    ⌜✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1⌝.
   Proof.
     rewrite gset_bij_own_auth_eq. iIntros "H1 H2".
     by iDestruct (own_valid_2 with "H1 H2") as %?%gset_bij_auth_frac_op_valid.
   Qed.
   Lemma gset_bij_own_auth_exclusive γ L1 L2 :
-    gset_bij_own_auth γ 1 L1 -∗ gset_bij_own_auth γ 1 L2 -∗ False.
+    gset_bij_own_auth γ (DfracOwn 1) L1 -∗ gset_bij_own_auth γ (DfracOwn 1) L2 -∗ False.
   Proof.
     iIntros "H1 H2".
     by iDestruct (gset_bij_own_auth_agree with "H1 H2") as %[[] _].
@@ -122,24 +122,24 @@ Section gset_bij.
 
   Lemma gset_bij_own_alloc L :
     gset_bijective L →
-    ⊢ |==> ∃ γ, gset_bij_own_auth γ 1 L ∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ (DfracOwn 1) L ∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
   Proof.
-    intro. iAssert (∃ γ, gset_bij_own_auth γ 1 L)%I with "[>]" as (γ) "Hauth".
+    intro. iAssert (∃ γ, gset_bij_own_auth γ (DfracOwn 1) L)%I with "[>]" as (γ) "Hauth".
     { rewrite gset_bij_own_auth_eq. iApply own_alloc. by apply gset_bij_auth_valid. }
     iExists γ. iModIntro. iSplit; [done|].
     by iApply gset_bij_own_elem_get_big.
   Qed.
   Lemma gset_bij_own_alloc_empty :
-    ⊢ |==> ∃ γ, gset_bij_own_auth γ 1 (∅ : gset (A * B)).
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ (DfracOwn 1) (∅ : gset (A * B)).
   Proof. iMod (gset_bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
 
   Lemma gset_bij_own_extend {γ L} a b :
     (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
-    gset_bij_own_auth γ 1 L ==∗
-    gset_bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
+    gset_bij_own_auth γ (DfracOwn 1) L ==∗
+    gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
   Proof.
     iIntros (??) "Hauth".
-    iAssert (gset_bij_own_auth γ 1 ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
+    iAssert (gset_bij_own_auth γ (DfracOwn 1) ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
     { rewrite gset_bij_own_auth_eq. iApply (own_update with "Hauth").
       by apply gset_bij_auth_extend. }
     iModIntro. iSplit; [done|].
@@ -149,8 +149,8 @@ Section gset_bij.
   Lemma gset_bij_own_extend_internal {γ L} a b :
     (∀ b', gset_bij_own_elem γ a b' -∗ False) -∗
     (∀ a', gset_bij_own_elem γ a' b -∗ False) -∗
-    gset_bij_own_auth γ 1 L ==∗
-    gset_bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
+    gset_bij_own_auth γ (DfracOwn 1) L ==∗
+    gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
   Proof.
     iIntros "Ha Hb HL".
     iAssert ⌜∀ b', (a, b') ∉ L⌝%I as %?.