From 96b574df3a61e794eb8cba1c37cd1bf78e49459c Mon Sep 17 00:00:00 2001
From: Hai Dang <haidang@mpi-sws.org>
Date: Thu, 23 May 2019 17:59:00 +0200
Subject: [PATCH] Make authoritative part of auth fractional

---
 CHANGELOG.md                         |   7 +
 theories/algebra/agree.v             |   3 +-
 theories/algebra/auth.v              | 387 ++++++++++++++++++---------
 theories/algebra/frac_auth.v         |  25 +-
 theories/base_logic/lib/auth.v       |   6 +-
 theories/base_logic/lib/boxes.v      |   6 +-
 theories/base_logic/lib/gen_heap.v   |   8 +-
 theories/base_logic/lib/proph_map.v  |   4 +-
 theories/base_logic/lib/wsat.v       |   7 +-
 theories/heap_lang/lib/counter.v     |   6 +-
 theories/heap_lang/lib/ticket_lock.v |   4 +-
 theories/program_logic/ownp.v        |   8 +-
 12 files changed, 318 insertions(+), 153 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 28c4f0b84..d295f277e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -112,6 +112,13 @@ Changes in Coq:
   `(λ: x, e)` no longer add a `locked`. Instead, we made the `wp_` tactics
   smarter to no longer unfold lambdas/recs that occur behind definitions.
 * Export the fact that `iPreProp` is a COFE.
+* The CMRA `auth` now can have fractional authoritative parts. So now `auth` has
+  3 types of elements: the fractional authoritative `●{q} a`, the full
+  authoritative `● a ≡ ●{1} a`, and the non-authoritative `◯ a`. Updates are
+  only possible with the full authoritative element `● a`, while fractional
+  authoritative elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`. As a
+  consequence, `auth` is no longer a COFE and does not preserve Leibniz
+  equality.
 
 ## Iris 3.1.0 (released 2017-12-19)
 
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index cf7a5d31b..360dc4778 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -28,7 +28,8 @@ Proof.
 
 (** Note that the projection [agree_car] is not non-expansive, so it cannot be
 used in the logic. If you need to get a witness out, you should use the
-lemma [to_agree_uninjN] instead. *)
+lemma [to_agree_uninjN] instead. In general, [agree_car] should ONLY be used
+internally in this file.  *)
 Record agree (A : Type) : Type := {
   agree_car : list A;
   agree_not_nil : bool_decide (agree_car = []) = false
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index d6f038dd5..ec5d2b9bf 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,61 +1,74 @@
-From iris.algebra Require Export excl local_updates.
+From iris.algebra Require Export frac agree local_updates.
 From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
+(** Authoritative CMRA with fractional authoritative parts. [auth] has 3 types
+  of elements: the fractional authoritative `●{q} a`, the full authoritative
+  `● a ≡ ●{1} a`, and the non-authoritative `◯ a`. Updates are only possible
+  with the full authoritative element `● a`, while fractional authoritative
+  elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`.
+*)
+
+Record auth (A : Type) :=
+  Auth { auth_auth_proj : option (frac * agree A) ; auth_frag_proj : A }.
 Add Printing Constructor auth.
 Arguments Auth {_} _ _.
-Arguments authoritative {_} _.
-Arguments auth_own {_} _.
+Arguments auth_auth_proj {_} _.
+Arguments auth_frag_proj {_} _.
 Instance: Params (@Auth) 1 := {}.
-Instance: Params (@authoritative) 1 := {}.
-Instance: Params (@auth_own) 1 := {}.
-Notation "â—¯ a" := (Auth None a) (at level 20).
-Notation "● a" := (Auth (Excl' a) ε) (at level 20).
+Instance: Params (@auth_auth_proj) 1 := {}.
+Instance: Params (@auth_frag_proj) 1 := {}.
+
+Definition auth_frag {A: ucmraT} (a: A) : auth A := (Auth None a).
+Definition auth_auth {A: ucmraT} (q: Qp) (a: A): auth A :=
+  (Auth (Some (q, to_agree a)) ε).
+
+Typeclasses Opaque auth_auth auth_frag.
+
+Instance: Params (@auth_frag) 1 := {}.
+Instance: Params (@auth_auth) 1 := {}.
+
+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).
 
 (* COFE *)
 Section cofe.
 Context {A : ofeT}.
-Implicit Types a : excl' A.
+Implicit Types a : option (frac * agree A).
 Implicit Types b : A.
 Implicit Types x y : auth A.
 
 Instance auth_equiv : Equiv (auth A) := λ x y,
-  authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y.
+  auth_auth_proj x ≡ auth_auth_proj y ∧ auth_frag_proj x ≡ auth_frag_proj y.
 Instance auth_dist : Dist (auth A) := λ n x y,
-  authoritative x ≡{n}≡ authoritative y ∧ auth_own x ≡{n}≡ auth_own y.
+  auth_auth_proj x ≡{n}≡ auth_auth_proj y ∧
+  auth_frag_proj x ≡{n}≡ auth_frag_proj y.
 
 Global Instance Auth_ne : NonExpansive2 (@Auth A).
 Proof. by split. Qed.
 Global Instance Auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@Auth A).
 Proof. by split. Qed.
-Global Instance authoritative_ne: NonExpansive (@authoritative A).
+Global Instance auth_auth_proj_ne: NonExpansive (@auth_auth_proj A).
 Proof. by destruct 1. Qed.
-Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A).
+Global Instance auth_auth_proj_proper : Proper ((≡) ==> (≡)) (@auth_auth_proj A).
 Proof. by destruct 1. Qed.
-Global Instance own_ne : NonExpansive (@auth_own A).
+Global Instance auth_frag_proj_ne : NonExpansive (@auth_frag_proj A).
 Proof. by destruct 1. Qed.
-Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
+Global Instance auth_frag_proj_proper : Proper ((≡) ==> (≡)) (@auth_frag_proj A).
 Proof. by destruct 1. Qed.
 
 Definition auth_ofe_mixin : OfeMixin (auth A).
-Proof. by apply (iso_ofe_mixin (λ x, (authoritative x, auth_own x))). Qed.
+Proof. by apply (iso_ofe_mixin (λ x, (auth_auth_proj x, auth_frag_proj x))). Qed.
 Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
 
-Global Instance auth_cofe `{!Cofe A} : Cofe authC.
-Proof.
-  apply (iso_cofe (λ y : _ * _, Auth (y.1) (y.2))
-    (λ x, (authoritative x, auth_own x))); by repeat intro.
-Qed.
-
 Global Instance Auth_discrete a b :
   Discrete a → Discrete b → Discrete (Auth a b).
 Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
 Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete authC.
 Proof. intros ? [??]; apply _. Qed.
-Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
-Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
 End cofe.
 
 Arguments authC : clear implicits.
@@ -66,75 +79,145 @@ Context {A : ucmraT}.
 Implicit Types a b : A.
 Implicit Types x y : auth A.
 
+Global Instance auth_frag_ne: NonExpansive (@auth_frag A).
+Proof. done. Qed.
+Global Instance auth_frag_proper : Proper ((≡) ==> (≡)) (@auth_frag A).
+Proof. done. Qed.
+Global Instance auth_auth_ne q : NonExpansive (@auth_auth A q).
+Proof. solve_proper. Qed.
+Global Instance auth_auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@auth_auth A).
+Proof. solve_proper. Qed.
+Global Instance auth_auth_discrete q a :
+  Discrete a → Discrete (ε : A) → Discrete (●{q} a).
+Proof. intros. apply Auth_discrete; apply _. Qed.
+Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
+Proof. intros. apply Auth_discrete; apply _. Qed.
+
 Instance auth_valid : Valid (auth A) := λ x,
-  match authoritative x with
-  | Excl' a => (∀ n, auth_own x ≼{n} a) ∧ ✓ a
-  | None => ✓ auth_own x
-  | ExclBot' => False
+  match auth_auth_proj x with
+  | Some (q, ag) =>
+      ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a)
+  | None => ✓ auth_frag_proj x
   end.
 Global Arguments auth_valid !_ /.
 Instance auth_validN : ValidN (auth A) := λ n x,
-  match authoritative x with
-  | Excl' a => auth_own x ≼{n} a ∧ ✓{n} a
-  | None => ✓{n} auth_own x
-  | ExclBot' => False
+  match auth_auth_proj x with
+  | Some (q, ag) =>
+      ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a
+  | None => ✓{n} auth_frag_proj x
   end.
 Global Arguments auth_validN _ !_ /.
 Instance auth_pcore : PCore (auth A) := λ x,
-  Some (Auth (core (authoritative x)) (core (auth_own x))).
+  Some (Auth (core (auth_auth_proj x)) (core (auth_frag_proj x))).
 Instance auth_op : Op (auth A) := λ x y,
-  Auth (authoritative x â‹… authoritative y) (auth_own x â‹… auth_own y).
+  Auth (auth_auth_proj x â‹… auth_auth_proj y) (auth_frag_proj x â‹… auth_frag_proj y).
 
 Definition auth_valid_eq :
-  valid = λ x, match authoritative x with
-               | Excl' a => (∀ n, auth_own x ≼{n} a) ∧ ✓ a
-               | None => ✓ auth_own x
-               | ExclBot' => False
+  valid = λ x, match auth_auth_proj x with
+               | Some (q, ag) => ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a)
+               | None => ✓ auth_frag_proj x
                end := eq_refl _.
 Definition auth_validN_eq :
-  validN = λ n x, match authoritative x with
-                  | Excl' a => auth_own x ≼{n} a ∧ ✓{n} a
-                  | None => ✓{n} auth_own x
-                  | ExclBot' => False
+  validN = λ n x, match auth_auth_proj x with
+                  | Some (q, ag) => ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a
+                  | None => ✓{n} auth_frag_proj x
                   end := eq_refl _.
 
 Lemma auth_included (x y : auth A) :
-  x ≼ y ↔ authoritative x ≼ authoritative y ∧ auth_own x ≼ auth_own y.
+  x ≼ y ↔
+  auth_auth_proj x ≼ auth_auth_proj y ∧ auth_frag_proj x ≼ auth_frag_proj y.
 Proof.
   split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
   intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
 Qed.
 
-Lemma authoritative_validN n x : ✓{n} x → ✓{n} authoritative x.
-Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_validN n x : ✓{n} x → ✓{n} auth_own x.
+Lemma auth_auth_proj_validN n x : ✓{n} x → ✓{n} auth_auth_proj x.
+Proof. destruct x as [[[]|]]; [by intros (? & ? & -> & ?)|done]. Qed.
+Lemma auth_frag_proj_validN n x : ✓{n} x → ✓{n} auth_frag_proj x.
 Proof.
   rewrite auth_validN_eq.
-  destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
+  destruct x as [[[]|]]; [|done]. naive_solver eauto using cmra_validN_includedN.
+Qed.
+Lemma auth_auth_proj_valid x : ✓ x → ✓ auth_auth_proj x.
+Proof.
+  destruct x as [[[]|]]; [intros [? H]|done]. split; [done|].
+  intros n. by destruct (H n) as [? [-> [? ?]]].
+Qed.
+Lemma auth_frag_proj_valid x : ✓ x → ✓ auth_frag_proj x.
+Proof.
+  destruct x as [[[]|]]; [intros [? H]|done]. apply cmra_valid_validN.
+  intros n. destruct (H n) as [? [? [? ?]]].
+  naive_solver eauto using cmra_validN_includedN.
+Qed.
+
+Lemma auth_frag_validN n a : ✓{n} a ↔ ✓{n} (◯ a).
+Proof. done. Qed.
+Lemma auth_auth_frac_validN n q a :
+  ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
+Proof.
+  rewrite auth_validN_eq /=. apply and_iff_compat_l. split.
+  - by intros [?[->%to_agree_injN []]].
+  - naive_solver eauto using ucmra_unit_leastN.
+Qed.
+Lemma auth_auth_validN n a : ✓{n} a ↔ ✓{n} (● a).
+Proof.
+  rewrite auth_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
+Qed.
+Lemma auth_both_frac_validN n q a b :
+  ✓{n} (●{q} a ⋅ ◯ b) ↔ ✓{n} q ∧ b ≼{n} a ∧ ✓{n} a.
+Proof.
+  rewrite auth_validN_eq /=. apply and_iff_compat_l.
+  setoid_rewrite (left_id _ _ b). split.
+  - by intros [?[->%to_agree_injN]].
+  - naive_solver.
+Qed.
+Lemma auth_both_validN n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
+Proof.
+  rewrite auth_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
+Qed.
+
+Lemma auth_frag_valid a : ✓ a ↔ ✓ (◯ a).
+Proof. done. Qed.
+Lemma auth_auth_frac_valid q a : ✓ q ∧ ✓ a ↔ ✓ (●{q} a).
+Proof.
+  rewrite auth_valid_eq /=. apply and_iff_compat_l. split.
+  - intros. exists a. split; [done|].
+    split; by [apply ucmra_unit_leastN|apply cmra_valid_validN].
+  - intros H'. apply cmra_valid_validN. intros n.
+    by destruct (H' n) as [? [->%to_agree_injN [??]]].
+Qed.
+Lemma auth_auth_valid a : ✓ a ↔ ✓ (● a).
+Proof. rewrite -auth_auth_frac_valid frac_valid'. naive_solver. Qed.
+Lemma auth_both_frac_valid q a b : ✓ q → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
+Proof.
+  intros Val1 Val2 Incl. rewrite auth_valid_eq /=. split; [done|].
+  intros n. exists a. split; [done|]. rewrite left_id.
+  split; by [apply cmra_included_includedN|apply cmra_valid_validN].
 Qed.
+Lemma auth_both_valid a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
+Proof. intros ??. by apply auth_both_frac_valid. Qed.
 
 Lemma auth_valid_discrete `{!CmraDiscrete A} x :
-  ✓ x ↔ match authoritative x with
-        | Excl' a => auth_own x ≼ a ∧ ✓ a
-        | None => ✓ auth_own x
-        | ExclBot' => False
+  ✓ x ↔ match auth_auth_proj x with
+        | Some (q, ag) => ✓ q ∧ ∃ a, ag ≡ to_agree a ∧ auth_frag_proj x ≼ a ∧ ✓ a
+        | None => ✓ auth_frag_proj x
         end.
 Proof.
-  rewrite auth_valid_eq. destruct x as [[[?|]|] ?]; simpl; try done.
-  setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
+  rewrite auth_valid_eq. destruct x as [[[??]|] ?]; simpl; [|done].
+  setoid_rewrite <-cmra_discrete_included_iff.
+  setoid_rewrite <-(discrete_iff _ a).
+  setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using O.
 Qed.
-Lemma auth_validN_2 n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
-Proof. by rewrite auth_validN_eq /= left_id. Qed.
-Lemma auth_valid_discrete_2 `{!CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
-Proof. by rewrite auth_valid_discrete /= left_id. Qed.
-
-Lemma authoritative_valid  x : ✓ x → ✓ authoritative x.
-Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_valid `{!CmraDiscrete A} x : ✓ x → ✓ auth_own x.
+Lemma auth_frac_valid_discrete_2 `{!CmraDiscrete A} q a b :
+  ✓ (●{q} a ⋅ ◯ b) ↔ ✓ q ∧ b ≼ a ∧ ✓ a.
 Proof.
-  rewrite auth_valid_discrete.
-  destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
+  rewrite auth_valid_discrete /=. apply and_iff_compat_l.
+  setoid_rewrite (left_id _ _ b). split.
+  - by intros [?[->%to_agree_inj]].
+  - naive_solver.
 Qed.
+Lemma auth_valid_discrete_2 `{!CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
+Proof. rewrite auth_frac_valid_discrete_2 frac_valid'. naive_solver. Qed.
 
 Lemma auth_cmra_mixin : CmraMixin (auth A).
 Proof.
@@ -143,12 +226,12 @@ Proof.
   - by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
   - by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
   - intros n [x a] [y b] [Hx Ha]; simpl in *. rewrite !auth_validN_eq.
-    destruct Hx as [?? Hx|]; first destruct Hx; intros ?; ofe_subst; auto.
-  - intros [[[?|]|] ?]; rewrite /= ?auth_valid_eq
-      ?auth_validN_eq /= ?cmra_included_includedN ?cmra_valid_validN;
-      naive_solver eauto using O.
-  - intros n [[[]|] ?]; rewrite !auth_validN_eq /=;
-      naive_solver eauto using cmra_includedN_S, cmra_validN_S.
+    destruct Hx as [x y Hx|]; first destruct Hx as [? Hx];
+      [destruct x,y|]; intros VI; ofe_subst; auto.
+  - intros [[[]|] ]; rewrite /= ?auth_valid_eq ?auth_validN_eq /=
+      ?cmra_valid_validN; naive_solver.
+  - intros n [[[]|] ]; rewrite !auth_validN_eq /=;
+      naive_solver eauto using dist_S, cmra_includedN_S, cmra_validN_S.
   - by split; simpl; rewrite assoc.
   - by split; simpl; rewrite comm.
   - by split; simpl; rewrite ?cmra_core_l.
@@ -157,13 +240,17 @@ Proof.
     by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
   - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
-   intros n [[[a1|]|] b1] [[[a2|]|] b2]; rewrite auth_validN_eq;
-     naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
+    intros n [[[q1 a1]|] b1] [[[q2 a2]|] b2]; rewrite auth_validN_eq /=;
+      try naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
+    intros [? [a [Eq [? Valid]]]].
+    assert (Eq': a1 ≡{n}≡ a2). { by apply agree_op_invN; rewrite Eq. }
+    split; [naive_solver eauto using cmra_validN_op_l|].
+    exists a. rewrite -Eq -Eq' agree_idemp. naive_solver.
   - intros n x y1 y2 ? [??]; simpl in *.
-    destruct (cmra_extend n (authoritative x) (authoritative y1)
-      (authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
-    destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
-      as (b1&b2&?&?&?); auto using auth_own_validN.
+    destruct (cmra_extend n (auth_auth_proj x) (auth_auth_proj y1)
+      (auth_auth_proj y2)) as (ea1&ea2&?&?&?); auto using auth_auth_proj_validN.
+    destruct (cmra_extend n (auth_frag_proj x) (auth_frag_proj y1) (auth_frag_proj y2))
+      as (b1&b2&?&?&?); auto using auth_frag_proj_validN.
     by exists (Auth ea1 b1), (Auth ea2 b2).
 Qed.
 Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
@@ -171,9 +258,11 @@ Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
 Global Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete authR.
 Proof.
   split; first apply _.
-  intros [[[?|]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
+  intros [[[]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
   - setoid_rewrite <-cmra_discrete_included_iff.
-    rewrite -cmra_discrete_valid_iff. tauto.
+    rewrite -cmra_discrete_valid_iff.
+    setoid_rewrite <-cmra_discrete_valid_iff.
+    setoid_rewrite <-(discrete_iff _ a). tauto.
   - by rewrite -cmra_discrete_valid_iff.
 Qed.
 
@@ -183,25 +272,13 @@ Proof.
   split; simpl.
   - rewrite auth_valid_eq /=. apply ucmra_unit_valid.
   - by intros x; constructor; rewrite /= left_id.
-  - do 2 constructor; simpl; apply (core_id_core _).
+  - do 2 constructor; [done| apply (core_id_core _)].
 Qed.
 Canonical Structure authUR := UcmraT (auth A) auth_ucmra_mixin.
 
 Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
 Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
 
-(** Internalized properties *)
-Lemma auth_equivI {M} x y :
-  x ≡ y ⊣⊢@{uPredI M} authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y.
-Proof. by uPred.unseal. Qed.
-Lemma auth_validI {M} x :
-  ✓ x ⊣⊢@{uPredI M} match authoritative x with
-                    | Excl' a => (∃ b, a ≡ auth_own x ⋅ b) ∧ ✓ a
-                    | None => ✓ auth_own x
-                    | ExclBot' => False
-                    end.
-Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
-
 Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
 Proof. done. Qed.
 Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
@@ -211,21 +288,77 @@ Global Instance auth_frag_sep_homomorphism :
   MonoidHomomorphism op op (≡) (@Auth A None).
 Proof. by split; [split; try apply _|]. Qed.
 
-Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
+Lemma auth_both_frac_op q a b : Auth (Some (q,to_agree a)) b ≡ ●{q} a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
-Lemma auth_auth_valid a : ✓ a → ✓ (● a).
-Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed.
+Lemma auth_both_op a b : Auth (Some (1%Qp,to_agree a)) b ≡ ● a ⋅ ◯ b.
+Proof. by rewrite auth_both_frac_op. Qed.
+
+Lemma auth_auth_frac_op p q a: ●{p} a ⋅ ●{q} a ≡ ●{p + q} a.
+Proof.
+  intros; split; simpl; last by rewrite left_id.
+  by rewrite -Some_op pair_op agree_idemp.
+Qed.
+Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
+Proof.
+  rewrite /op /auth_op /= left_id -Some_op pair_op auth_validN_eq /=.
+  intros (?&?& Eq &?&?). apply to_agree_injN, agree_op_invN. by rewrite Eq.
+Qed.
+Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
+Proof.
+  intros ?. apply equiv_dist. intros n.
+  by eapply auth_auth_frac_op_invN, cmra_valid_validN.
+Qed.
+Lemma auth_auth_frac_op_invL `{!LeibnizEquiv A} q a p b :
+  ✓ (●{p} a ⋅ ●{q} b) → a = b.
+Proof. by intros ?%auth_auth_frac_op_inv%leibniz_equiv. Qed.
+
+(** Internalized properties *)
+Lemma auth_equivI {M} x y :
+  x ≡ y ⊣⊢@{uPredI M} auth_auth_proj x ≡ auth_auth_proj y ∧ auth_frag_proj x ≡ auth_frag_proj y.
+Proof. by uPred.unseal. Qed.
+Lemma auth_validI {M} x :
+  ✓ x ⊣⊢@{uPredI M} match auth_auth_proj x with
+                    | Some (q, ag) => ✓ q ∧
+                      ∃ a, ag ≡ to_agree a ∧ (∃ b, a ≡ auth_frag_proj x ⋅ b) ∧ ✓ a
+                    | None => ✓ auth_frag_proj x
+                    end.
+Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
+Lemma auth_frag_validI {M} (a : A):
+  ✓ (◯ a) ⊣⊢@{uPredI M} ✓ a.
+Proof. by rewrite auth_validI. Qed.
+
+Lemma auth_both_validI {M} q (a b: A) :
+  ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+Proof.
+  rewrite -auth_both_frac_op auth_validI /=. apply bi.and_proper; [done|].
+  setoid_rewrite agree_equivI. iSplit.
+  - iDestruct 1 as (a') "[#Eq [H V]]". iDestruct "H" as (b') "H".
+    iRewrite -"Eq" in "H". iRewrite -"Eq" in "V". auto.
+  - iDestruct 1 as "[H V]". iExists a. auto.
+Qed.
+Lemma auth_auth_validI {M} q (a b: A) :
+  ✓ (●{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
+Proof.
+  rewrite auth_validI /=. apply bi.and_proper; [done|].
+  setoid_rewrite agree_equivI. iSplit.
+  - iDestruct 1 as (a') "[Eq [_ V]]". by iRewrite -"Eq" in "V".
+  - iIntros "V". iExists a. iSplit; [done|]. iSplit; [|done]. iExists a.
+    by rewrite left_id.
+Qed.
 
 Lemma auth_update a b a' b' :
   (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
 Proof.
   intros Hup; apply cmra_total_update.
-  move=> n [[[?|]|] bf1] // [[bf2 Ha] ?]; do 2 red; simpl in *.
-  move: Ha; rewrite !left_id -assoc=> Ha.
-  destruct (Hup n (Some (bf1 â‹… bf2))); auto.
-  split; last done. exists bf2. by rewrite -assoc.
+  move=> n [[[??]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
+  + exfalso. move : VL => /frac_valid'.
+    rewrite frac_op'. by apply Qp_not_plus_q_ge_1.
+  + split; [done|]. apply to_agree_injN in Eq.
+    move: Ha; rewrite !left_id -assoc => Ha.
+    destruct (Hup n (Some (bf1 â‹… bf2))); [by rewrite Eq..|]. simpl in *.
+    exists a'. split; [done|]. split; [|done]. exists bf2.
+    by rewrite left_id -assoc.
 Qed.
-
 Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
 Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
 Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) → ● a ⋅ ◯ b ~~> ● a'.
@@ -236,12 +369,15 @@ Lemma auth_local_update (a b0 b1 a' b0' b1': A) :
   (● a ⋅ ◯ b0, ● a ⋅ ◯ b1) ~l~> (● a' ⋅ ◯ b0', ● a' ⋅ ◯ b1').
 Proof.
   rewrite !local_update_unital=> Hup ? ? n /=.
-  move=> [[[ac|]|] bc] /auth_validN_2 [Le Val] [] /=;
-    inversion_clear 1 as [?? Ha|]; inversion_clear Ha. (* need setoid_discriminate! *)
-  rewrite !left_id=> ?.
-  destruct (Hup n bc) as [Hval' Heq]; eauto using cmra_validN_includedN.
-  rewrite -!auth_both_op auth_validN_eq /=.
-  split_and!; [by apply cmra_included_includedN|by apply cmra_valid_validN|done].
+    move=> [[[qc ac]|] bc] /auth_both_validN [Le Val] [] /=.
+  - move => Ha. exfalso. move : Ha. rewrite right_id -Some_op pair_op.
+    move => /Some_dist_inj [/=]. rewrite frac_op' => Eq _.
+    apply (Qp_not_plus_q_ge_1 qc). by rewrite -Eq.
+  - move => _. rewrite !left_id=> ?.
+    destruct (Hup n bc) as [Hval' Heq]; eauto using cmra_validN_includedN.
+    rewrite -!auth_both_op auth_validN_eq /=.
+    split_and!; [done| |done]. exists a'.
+    split_and!; [done|by apply cmra_included_includedN|by apply cmra_valid_validN].
 Qed.
 End cmra.
 
@@ -252,41 +388,50 @@ Arguments authUR : clear implicits.
 Instance is_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
   IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
 Proof. done. Qed.
+Instance is_op_auth_auth_frac {A : ucmraT} (q q1 q2 : frac) (a : A) :
+  IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
+Proof. rewrite /IsOp' /IsOp => ->. by rewrite -auth_auth_frac_op. Qed.
 
 (* Functor *)
 Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
-  Auth (excl_map f <$> authoritative x) (f (auth_own x)).
+  Auth (prod_map id (agree_map f) <$> auth_auth_proj x) (f (auth_frag_proj x)).
 Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
-Proof. by destruct x as [[[]|]]. Qed.
+Proof. destruct x as [[[]|] ]; by rewrite // /auth_map /= agree_map_id. Qed.
 Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
   auth_map (g ∘ f) x = auth_map g (auth_map f x).
-Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_map_ext {A B : ofeT} (f g : A → B) x :
+Proof. destruct x as [[[]|] ];  by rewrite // /auth_map /= agree_map_compose. Qed.
+Lemma auth_map_ext {A B : ofeT} (f g : A → B) `{_ : NonExpansive f} x :
   (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
 Proof.
   constructor; simpl; auto.
-  apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
+  apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
 Qed.
-Instance auth_map_ne {A B : ofeT} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
+Instance auth_map_ne {A B : ofeT} (f : A -> B) {Hf : NonExpansive f} :
+  NonExpansive (auth_map f).
 Proof.
-  intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].
-  apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
+  intros n [??] [??] [??]; split; simpl in *; [|by apply Hf].
+  apply option_fmap_ne; [|done]=> x y ?. apply prod_map_ne; [done| |done].
+  by apply agree_map_ne.
 Qed.
 Instance auth_map_cmra_morphism {A B : ucmraT} (f : A → B) :
   CmraMorphism f → CmraMorphism (auth_map f).
 Proof.
   split; try apply _.
-  - intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
-      naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
+  - intros n [[[??]|] b]; rewrite !auth_validN_eq;
+      [|naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN].
+    intros [? [a' [Eq [? ?]]]]. split; [done|]. exists (f a').
+    rewrite -agree_map_to_agree -Eq.
+    naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
   - intros [??]. apply Some_proper; rewrite /auth_map /=.
     by f_equiv; rewrite /= cmra_morphism_core.
-  - intros [[?|]?] [[?|]?]; try apply Auth_proper=>//=; by rewrite cmra_morphism_op.
+  - intros [[[??]|]?] [[[??]|]?]; try apply Auth_proper=>//=; try by rewrite cmra_morphism_op.
+    by rewrite -Some_op pair_op cmra_morphism_op.
 Qed.
 Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
   CofeMor (auth_map f).
 Lemma authC_map_ne A B : NonExpansive (@authC_map A B).
-Proof. intros n f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
+Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
+  apply agreeC_map_ne; auto. Qed.
 
 Program Definition authRF (F : urFunctor) : rFunctor := {|
   rFunctor_car A B := authR (urFunctor_car F A B);
@@ -297,11 +442,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y; apply urFunctor_id.
+  apply auth_map_ext=>y. apply _. apply urFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y; apply urFunctor_compose.
+  apply auth_map_ext=>y. apply _. apply urFunctor_compose.
 Qed.
 
 Instance authRF_contractive F :
@@ -319,11 +464,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y; apply urFunctor_id.
+  apply auth_map_ext=>y. apply _. apply urFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y; apply urFunctor_compose.
+  apply auth_map_ext=>y. apply _. apply urFunctor_compose.
 Qed.
 
 Instance authURF_contractive F :
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 30cf54715..0706fe627 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -2,6 +2,13 @@ From iris.algebra Require Export frac auth.
 From iris.algebra Require Export updates local_updates.
 From iris.algebra Require Import proofmode_classes.
 
+(** Authoritative CMRA where the NON-authoritative parts can be fractional.
+  This CMRA allows the original non-authoritative element `â—¯ a` to be split into
+  fractional parts `◯!{q} a`. Using `◯! a ≡ ◯!{1} a` is in effect the same as
+  using the original `â—¯ a`. Currently, however, this CMRA hides the ability to
+  split the authoritative part into fractions.
+*)
+
 Definition frac_authR (A : cmraT) : cmraT :=
   authR (optionUR (prodR fracR A)).
 Definition frac_authUR (A : cmraT) : ucmraT :=
@@ -35,18 +42,18 @@ Section frac_auth.
   Proof. solve_proper. Qed.
 
   Global Instance frac_auth_auth_discrete a : Discrete a → Discrete (●! a).
-  Proof. intros; apply Auth_discrete; apply _. Qed.
+  Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
   Global Instance frac_auth_frag_discrete a : Discrete a → Discrete (◯! a).
-  Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed.
+  Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
 
   Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (●! a ⋅ ◯! a).
-  Proof. done. Qed.
+  Proof. by rewrite auth_both_validN. Qed.
   Lemma frac_auth_valid a : ✓ a → ✓ (●! a ⋅ ◯! a).
-  Proof. done. Qed.
+  Proof. intros. by apply auth_both_valid. Qed.
 
   Lemma frac_auth_agreeN n a b : ✓{n} (●! a ⋅ ◯! b) → a ≡{n}≡ b.
   Proof.
-    rewrite auth_validN_eq /= => -[Hincl Hvalid].
+    rewrite auth_both_validN /= => -[Hincl Hvalid].
     by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
   Qed.
   Lemma frac_auth_agree a b : ✓ (●! a ⋅ ◯! b) → a ≡ b.
@@ -57,10 +64,10 @@ Section frac_auth.
   Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.
 
   Lemma frac_auth_includedN n q a b : ✓{n} (●! a ⋅ ◯!{q} b) → Some b ≼{n} Some a.
-  Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed.
+  Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
   Lemma frac_auth_included `{CmraDiscrete A} q a b :
     ✓ (●! a ⋅ ◯!{q} b) → Some b ≼ Some a.
-  Proof. by rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
+  Proof. by rewrite auth_valid_discrete_2 /= => -[/Some_pair_included [_ ?] _]. Qed.
   Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
     ✓{n} (●! a ⋅ ◯!{q} b) → b ≼{n} a.
   Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
@@ -70,8 +77,8 @@ Section frac_auth.
 
   Lemma frac_auth_auth_validN n a : ✓{n} (●! a) ↔ ✓{n} a.
   Proof.
-    split; [by intros [_ [??]]|].
-    by repeat split; simpl; auto using ucmra_unit_leastN.
+    rewrite auth_auth_frac_validN Some_validN. split.
+    by intros [?[]]. intros. by split.
   Qed.
   Lemma frac_auth_auth_valid a : ✓ (●! a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 2664ddc3d..2a6974c29 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -94,7 +94,7 @@ Section auth.
   Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
   Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
-  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
+  Proof. by rewrite /auth_own own_valid auth_frag_validI. Qed.
   Global Instance auth_own_sep_homomorphism γ :
     WeakMonoidHomomorphism op uPred_sep (≡) (auth_own γ).
   Proof. split; try apply _. apply auth_own_op. Qed.
@@ -107,8 +107,8 @@ Section auth.
     ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜I γ⌝ ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
   Proof.
     iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
-    iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) I) as (γ) "[% Hγ]"; [done|done|].
-    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
+    iMod (own_alloc_strong (● f t ⋅ ◯ f t) I) as (γ) "[% [Hγ Hγ']]";
+      [done|by apply auth_valid_discrete_2|].
     iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
     { iNext. rewrite /auth_inv. iExists t. by iFrame. }
     eauto.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 84bbe329a..597c05835 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -1,5 +1,5 @@
 From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import auth gmap agree.
+From iris.algebra Require Import excl auth gmap agree.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
@@ -78,7 +78,7 @@ Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ ⌜b1 = b2⌝.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
-  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
+  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete_2.
 Qed.
 
 Lemma box_own_auth_update γ b1 b2 b3 :
@@ -110,7 +110,7 @@ Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iMod (own_alloc_cofinite (● Excl' false ⋅ ◯ Excl' false,
     Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
-    as (γ) "[Hdom Hγ]"; first done.
+    as (γ) "[Hdom Hγ]"; first by (split; [apply auth_valid_discrete_2|]).
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
   iDestruct "Hdom" as % ?%not_elem_of_dom.
   iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 8268ee417..cb0b414a2 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -76,7 +76,7 @@ Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
 Proof.
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { apply: auth_auth_valid. exact: to_gen_heap_valid. }
+  { rewrite -auth_auth_valid. exact: to_gen_heap_valid. }
   iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
 Qed.
 
@@ -105,7 +105,7 @@ Section gen_heap.
   Proof.
     apply wand_intro_r.
     rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
-    f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
+    f_equiv. rewrite -auth_frag_valid op_singleton singleton_valid pair_op.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
@@ -122,8 +122,8 @@ Section gen_heap.
 
   Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
   Proof.
-    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
-    by apply pure_mono=> /auth_own_valid /singleton_valid [??].
+    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid -auth_frag_valid.
+    by apply pure_mono=> /singleton_valid [??].
   Qed.
   Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
   Proof.
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 22f359492..939ee3059 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import auth list gmap.
+From iris.algebra Require Import auth excl list gmap.
 From iris.base_logic.lib Require Export own.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
@@ -111,7 +111,7 @@ Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
   (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
 Proof.
   iMod (own_alloc (● to_proph_map ∅)) as (γ) "Hh".
-  { apply: auth_auth_valid. exact: to_proph_map_valid. }
+  { rewrite -auth_auth_valid. exact: to_proph_map_valid. }
   iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
   iPureIntro. split =>//.
 Qed.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 78cb9f764..e09b59f9d 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -110,10 +110,10 @@ Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
   own invariant_name (◯ {[i := invariant_unfold P]}) ⊢
   ∃ Q, ⌜I !! i = Some Q⌝ ∗ ▷ (Q ≡ P).
 Proof.
-  rewrite -own_op own_valid auth_validI /=. iIntros "[#HI #HvI]".
+  rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
   iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
   iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
-  rewrite left_id_L lookup_fmap lookup_op lookup_singleton bi.option_equivI.
+  rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.
   case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
   iExists Q; iSplit; first done.
   iAssert (invariant_unfold Q ≡ invariant_unfold P)%I as "?".
@@ -197,7 +197,8 @@ End wsat.
 Lemma wsat_alloc `{!invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
   iIntros.
-  iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
+  iMod (own_alloc (● (∅ : gmap positive _))) as (γI) "HI";
+    first by rewrite -auth_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
   iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index b49fff3ab..cb65f706b 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -36,7 +36,8 @@ Section mono_proof.
     {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
+      first by apply auth_valid_discrete_2.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
@@ -113,7 +114,8 @@ Section contrib_spec.
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']";
+      first by apply auth_valid_discrete_2.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 017d256c7..681b7a22b 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import auth gset.
+From iris.algebra Require Import excl auth gset.
 From iris.heap_lang.lib Require Export lock.
 Set Default Proof Using "Type".
 Import uPred.
@@ -76,7 +76,7 @@ Section proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
     wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
     iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
-    { by rewrite -auth_both_op. }
+    { by apply auth_valid_discrete_2. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
       iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index d48ef7a93..0bbe407ee 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
-From iris.algebra Require Import auth.
+From iris.algebra Require Import excl auth.
 From iris.proofmode Require Import tactics classes.
 Set Default Proof Using "Type".
 
@@ -53,7 +53,8 @@ Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
   iIntros (? κs).
-  iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]"; first done.
+  iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]";
+    first by apply auth_valid_discrete_2.
   iModIntro. iExists (λ σ κs, own γσ (● (Excl' σ)))%I.
   iFrame "Hσ".
   iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
@@ -68,7 +69,8 @@ Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
 Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
   iIntros (? κs κs').
-  iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]"; first done.
+  iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]";
+    first by apply auth_valid_discrete_2.
   iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, (λ _, True%I).
   iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
-- 
GitLab