diff --git a/_CoqProject b/_CoqProject
index 3d82b5d8b0e8d32c0d415ecdffe94559edc4f1be..e76f26654cda963f73c73d55688b11dca5ec981a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,6 +39,7 @@ theories/algebra/lib/excl_auth.v
 theories/algebra/lib/frac_auth.v
 theories/algebra/lib/ufrac_auth.v
 theories/algebra/lib/frac_agree.v
+theories/algebra/lib/gmap_auth.v
 theories/si_logic/siprop.v
 theories/si_logic/bi.v
 theories/bi/notation.v
diff --git a/theories/algebra/lib/gmap_auth.v b/theories/algebra/lib/gmap_auth.v
new file mode 100644
index 0000000000000000000000000000000000000000..0337e26b411175ae0e40d785c2f01119a3fa03f4
--- /dev/null
+++ b/theories/algebra/lib/gmap_auth.v
@@ -0,0 +1,356 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Export auth gmap updates csum.
+From iris.algebra Require Import local_updates proofmode_classes.
+From iris.base_logic Require Import base_logic.
+From iris Require Import options.
+
+(** * Authoritative CMRA over a map.
+The elements of the map are of type [(frac * agree T) + agree T].
+"Right" elements (on the [agree] side) are immutable and their (fragment) ownership is persistent.
+"Left" elements behave like the usual separation logic heap with fractional permissions.
+
+This representation and the types of [gmap_auth_auth] and [gmap_auth_frag] are
+considered unstable and will change in a future version of Iris. However,
+the [mut]/[ro] variants should be unaffected by that change. *)
+
+Local Definition mapUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
+  gmapUR K (csumR (prodR fracR (agreeR V)) (agreeR V)).
+Definition gmap_authR (K : Type) `{Countable K} (V : ofeT) : cmraT :=
+  authR (mapUR K V).
+Definition gmap_authUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
+  authUR (mapUR K V).
+
+(** The abstract state of the authoritative map is given by a [gmap K (V*bool)],
+where the [bool] indicates if the element is still mutable ([false] = "left
+element") or already read-only ([true] = "right element"). *)
+
+Section definitions.
+  Context {K : Type} `{Countable K} {V : ofeT}.
+
+  Local Definition to_auth_elem (q : frac) (e : bool * V) :
+      csumR (prodR fracR (agreeR V)) (agreeR V) :=
+    if e.1 then Cinr (to_agree e.2) else Cinl (q, to_agree e.2).
+  Local Definition to_auth_map (m : gmap K (bool * V)) : mapUR K V :=
+    to_auth_elem 1 <$> m.
+  Local Definition to_frag_elem (mq : option Qp) (v : V) :
+      csumR (prodR fracR (agreeR V)) (agreeR V) :=
+    match mq with
+    | Some q => Cinl (q, to_agree v)
+    | None => Cinr (to_agree v)
+    end.
+
+  Definition gmap_auth_auth (m : gmap K (bool * V)) : gmap_authUR K V :=
+    ● (to_auth_map m).
+  (* [(false,.)] is [λ v, (false, v)]. *)
+  Definition gmap_auth_auth_mut (m : gmap K V) : gmap_authUR K V :=
+    gmap_auth_auth ((false,.) <$> m).
+  Definition gmap_auth_auth_ro (m : gmap K V) : gmap_authUR K V :=
+    gmap_auth_auth ((true,.) <$> m).
+
+  Definition gmap_auth_frag (k : K) (mq : option Qp) (v : V) : gmap_authUR K V :=
+    â—¯ {[k := to_frag_elem mq v]}.
+  Definition gmap_auth_frag_mut (k : K) (q : Qp) (v : V) : gmap_authUR K V :=
+    gmap_auth_frag k (Some q) v.
+  Definition gmap_auth_frag_ro (k : K) (v : V) : gmap_authUR K V :=
+    gmap_auth_frag k None v.
+End definitions.
+
+Section lemmas.
+  Context {K : Type} `{Countable K} {V : ofeT}.
+  Implicit Types (m : gmap K (bool * V)) (k : K) (q : Qp) (v : V) (ro : bool) (e : bool * V).
+
+  Local Instance to_auth_elem_ne q : NonExpansive (to_auth_elem (V:=V) q).
+  Proof. intros n [v1 ro1] [v2 ro2] [??]. simpl in *. solve_proper. Qed.
+  Global Instance gmap_auth_auth_ne : NonExpansive (gmap_auth_auth (K:=K) (V:=V)).
+  Proof. solve_proper. Qed.
+  Global Instance gmap_auth_auth_mut_ne : NonExpansive (gmap_auth_auth_mut (K:=K) (V:=V)).
+  Proof. solve_proper. Qed.
+  Global Instance gmap_auth_auth_ro_ne : NonExpansive (gmap_auth_auth_ro (K:=K) (V:=V)).
+  Proof. solve_proper. Qed.
+
+  Local Instance to_frag_elem_ne oq : NonExpansive (to_frag_elem (V:=V) oq).
+  Proof. solve_proper. Qed.
+  Global Instance gmap_auth_frag_ne k oq : NonExpansive (gmap_auth_frag (V:=V) k oq).
+  Proof. solve_proper. Qed.
+  Global Instance gmap_auth_frag_mut_ne k q : NonExpansive (gmap_auth_frag_mut (V:=V) k q).
+  Proof. solve_proper. Qed.
+  Global Instance gmap_auth_frag_ro_ne k : NonExpansive (gmap_auth_frag_ro (V:=V) k).
+  Proof. solve_proper. Qed.
+
+  (** Map operations *)
+  Local Lemma to_auth_map_insert k e m :
+    to_auth_map (<[k:=e]> m) = <[k:=to_auth_elem 1 e]> (to_auth_map m).
+  Proof. by rewrite /to_auth_map fmap_insert. Qed.
+  Local Lemma to_auth_map_singleton_includedN qe n m k e :
+    {[k := to_auth_elem qe e]} ≼{n} to_auth_map m → m !! k ≡{n}≡ Some e.
+  Proof.
+    rewrite singleton_includedN_l => -[auth_e []].
+    rewrite /to_auth_map lookup_fmap fmap_Some_dist => -[e' [-> ->]] {m}.
+    rewrite Some_csum_includedN. intros [Hbot|[Hleft|Hright]].
+    - exfalso. destruct e' as [[] ?]; done.
+    - destruct Hleft as ([q v] & [q' v'] & He & He' & Hincl).
+      destruct e as [[] ev]; first done.
+      destruct e' as [[] ev']; first done.
+      f_equiv. f_equiv.
+      rewrite /to_auth_elem /= in He He'.
+      move:He He'=> [_ Heq] [_ Heq']. simplify_eq.
+      move:Hincl=> /Some_pair_includedN_total_2 [_] /to_agree_includedN. done.
+    - destruct Hright as (v & v' & He & He' & Hincl).
+      destruct e as [[] ev]; last done.
+      destruct e' as [[] ev']; last done.
+      f_equiv. f_equiv.
+      rewrite /to_auth_elem /= in He He'.
+      move:He He'=> [Heq] [Heq']. simplify_eq.
+      move:Hincl=> /Some_includedN [|].
+      * move /to_agree_injN. done.
+      * move /to_agree_includedN. done.
+  Qed.
+  Local Lemma to_auth_map_singleton_included qe m k e :
+    (∀ n, {[k := to_auth_elem qe e]} ≼{n} to_auth_map m) → m !! k ≡ Some e.
+  Proof.
+    intros Hincl. apply equiv_dist=>n.
+    by eapply to_auth_map_singleton_includedN.
+  Qed.
+  Local Lemma to_auth_map_singleton_includedI qe M m c k e :
+    to_auth_map m ≡ {[k := to_auth_elem qe e]} ⋅ c ⊢@{uPredI M} m !! k ≡ Some e.
+  Proof.
+    apply uPred.internal_eq_entails=>n Heq.
+    eapply to_auth_map_singleton_includedN.
+    by exists c.
+  Qed.
+
+  (** Composition and validity *)
+  Local Lemma to_auth_elem_valid e : ✓ to_auth_elem 1 e.
+  Proof. destruct e as [ro v]. by destruct ro. Qed.
+
+  Lemma gmap_auth_auth_valid m : ✓ gmap_auth_auth m.
+  Proof.
+    rewrite auth_auth_valid. intros l. rewrite lookup_fmap. case (m !! l); last done.
+    apply to_auth_elem_valid.
+  Qed.
+  Lemma gmap_auth_auth_mut_valid (m : gmap K V) : ✓ gmap_auth_auth_mut m.
+  Proof. apply gmap_auth_auth_valid. Qed.
+  Lemma gmap_auth_auth_ro_valid (m : gmap K V) : ✓ gmap_auth_auth_ro m.
+  Proof. apply gmap_auth_auth_valid. Qed.
+
+  Lemma gmap_auth_frag_valid k mq v : ✓ gmap_auth_frag k mq v ↔ ✓ mq.
+  Proof.
+    rewrite auth_frag_valid singleton_valid. split.
+    - destruct mq; last done. intros [??]. done.
+    - intros ?. destruct mq; split; done.
+  Qed.
+  Lemma gmap_auth_frag_mut_valid k q v : ✓ gmap_auth_frag_mut k q v ↔ ✓ q.
+  Proof. apply gmap_auth_frag_valid. Qed.
+  Lemma gmap_auth_frag_ro_valid k v : ✓ gmap_auth_frag_ro k v.
+  Proof. apply gmap_auth_frag_valid. done. Qed.
+
+  Lemma gmap_auth_frag_mut_frac_op k q1 q2 v :
+    gmap_auth_frag_mut k (q1 + q2)%Qp v ≡ gmap_auth_frag_mut k q1 v ⋅ gmap_auth_frag_mut k q2 v.
+  Proof. rewrite -auth_frag_op singleton_op -Cinl_op -pair_op agree_idemp //. Qed.
+  Lemma gmap_auth_frag_mut_op_valid k q1 q2 v1 v2 :
+    ✓ (gmap_auth_frag_mut k q1 v1 ⋅ gmap_auth_frag_mut k q2 v2) → ✓ (q1 + q2)%Qp ∧ v1 ≡ v2.
+  Proof.
+    rewrite auth_frag_valid singleton_op singleton_valid -Cinl_op -pair_op.
+    intros [? ?]. split; first done. apply to_agree_op_inv. done.
+  Qed.
+  Lemma gmap_auth_frag_mut_op_valid_L `{!LeibnizEquiv V} k q1 q2 v1 v2 :
+    ✓ (gmap_auth_frag_mut k q1 v1 ⋅ gmap_auth_frag_mut k q2 v2) → ✓ (q1 + q2)%Qp ∧ v1 = v2.
+  Proof.
+    unfold_leibniz. apply gmap_auth_frag_mut_op_valid.
+  Qed.
+
+  Lemma gmap_auth_frag_ro_op_mut_op_valid k q1 v1 v2 :
+    ¬ ✓ (gmap_auth_frag_mut k q1 v1 ⋅ gmap_auth_frag_ro k v2).
+  Proof. rewrite auth_frag_valid singleton_op singleton_valid. intros []. Qed.
+
+  Lemma gmap_auth_frag_ro_idemp k v :
+    gmap_auth_frag_ro k v ≡ gmap_auth_frag_ro k v ⋅ gmap_auth_frag_ro k v.
+  Proof. rewrite -auth_frag_op singleton_op -Cinr_op agree_idemp. done. Qed.
+
+  Lemma gmap_auth_frag_ro_op_valid k v1 v2 :
+    ✓ (gmap_auth_frag_ro k v1 ⋅ gmap_auth_frag_ro k v2) → v1 ≡ v2.
+  Proof.
+    rewrite auth_frag_valid singleton_op singleton_valid -Cinr_op.
+    apply to_agree_op_inv.
+  Qed.
+  Lemma gmap_auth_frag_ro_op_valid_L `{!LeibnizEquiv V} k v1 v2 :
+    ✓ (gmap_auth_frag_ro k v1 ⋅ gmap_auth_frag_ro k v2) → v1 = v2.
+  Proof.
+    unfold_leibniz. apply gmap_auth_frag_ro_op_valid.
+  Qed.
+
+  Lemma gmap_auth_auth_frag_valid m k mq v :
+    ✓ (gmap_auth_auth m ⋅ gmap_auth_frag k mq v) →
+    m !! k ≡ Some (if mq is None then true else false, v).
+  Proof.
+    rewrite /gmap_auth_auth /gmap_auth_frag.
+    intros [Hlk _]%auth_both_valid.
+    set (q := default 1%Qp mq).
+    eapply (to_auth_map_singleton_included q).
+    rewrite /to_auth_elem /to_frag_elem /= in Hlk *.
+    destruct mq; done.
+  Qed.
+
+  Lemma gmap_auth_auth_frag_mut_valid m k q v :
+    ✓ (gmap_auth_auth m ⋅ gmap_auth_frag_mut k q v) → m !! k ≡ Some (false, v).
+  Proof. apply gmap_auth_auth_frag_valid. Qed.
+  Lemma gmap_auth_auth_frag_mut_valid_L `{!LeibnizEquiv V} m k q v :
+    ✓ (gmap_auth_auth m ⋅ gmap_auth_frag_mut k q v) → m !! k = Some (false, v).
+  Proof. unfold_leibniz. apply gmap_auth_auth_frag_mut_valid. Qed.
+  Lemma gmap_auth_auth_mut_frag_mut_valid (m : gmap K V) k q v :
+    ✓ (gmap_auth_auth_mut m ⋅ gmap_auth_frag_mut k q v) → m !! k ≡ Some v.
+  Proof.
+    rewrite /gmap_auth_auth_mut. move /gmap_auth_auth_frag_mut_valid.
+    rewrite lookup_fmap /= fmap_Some_equiv => -[e [-> [/= _ ?]]]. by f_equiv.
+  Qed.
+  Lemma gmap_auth_auth_mut_frag_mut_valid_L `{!LeibnizEquiv V} (m : gmap K V) k q v :
+    ✓ (gmap_auth_auth_mut m ⋅ gmap_auth_frag_mut k q v) → m !! k = Some v.
+  Proof. unfold_leibniz. apply gmap_auth_auth_mut_frag_mut_valid. Qed.
+
+  Lemma gmap_auth_auth_frag_ro_valid m k v :
+    ✓ (gmap_auth_auth m ⋅ gmap_auth_frag_ro k v) → m !! k ≡ Some (true, v).
+  Proof. apply gmap_auth_auth_frag_valid. Qed.
+  Lemma gmap_auth_auth_frag_ro_valid_L `{!LeibnizEquiv V} m k v :
+    ✓ (gmap_auth_auth m ⋅ gmap_auth_frag_ro k v) → m !! k = Some (true, v).
+  Proof. unfold_leibniz. apply gmap_auth_auth_frag_ro_valid. Qed.
+  Lemma gmap_auth_auth_ro_frag_ro_valid (m : gmap K V) k v :
+    ✓ (gmap_auth_auth_ro m ⋅ gmap_auth_frag_ro k v) → m !! k ≡ Some v.
+  Proof.
+    rewrite /gmap_auth_auth_mut. move /gmap_auth_auth_frag_ro_valid.
+    rewrite lookup_fmap /= fmap_Some_equiv => -[e [-> [/= _ ?]]]. by f_equiv.
+  Qed.
+  Lemma gmap_auth_auth_ro_frag_ro_valid_L `{!LeibnizEquiv V} (m : gmap K V) k v :
+    ✓ (gmap_auth_auth_ro m ⋅ gmap_auth_frag_ro k v) → m !! k = Some v.
+  Proof. unfold_leibniz. apply gmap_auth_auth_ro_frag_ro_valid. Qed.
+
+  (** Frame-preserving updates *)
+  Lemma gmap_auth_alloc m k v ro :
+    m !! k = None →
+    gmap_auth_auth m ~~>
+      gmap_auth_auth (<[k := (ro, v)]> m) â‹…
+        gmap_auth_frag k (if ro then None else Some 1%Qp) v.
+  Proof.
+    intros Hfresh. etrans.
+    - eapply auth_update_alloc.
+      eapply (alloc_singleton_local_update _ k (to_auth_elem _ (ro, v)))=> //.
+      + rewrite lookup_fmap Hfresh. done.
+      + apply to_auth_elem_valid.
+    - apply reflexive_eq. f_equal.
+      + rewrite /gmap_auth_auth to_auth_map_insert. done.
+      + destruct ro; done.
+  Qed.
+  Lemma gmap_auth_mut_alloc (m : gmap K V) k v :
+    m !! k = None →
+    gmap_auth_auth_mut m ~~>
+      gmap_auth_auth_mut (<[k := v]> m) â‹… gmap_auth_frag_mut k 1%Qp v.
+  Proof.
+    intros Hfresh.
+    etrans; first apply (gmap_auth_alloc _ k v false).
+    - rewrite lookup_fmap Hfresh //.
+    - apply reflexive_eq. f_equal. rewrite /gmap_auth_auth_mut fmap_insert //.
+  Qed.
+  Lemma gmap_auth_ro_alloc (m : gmap K V) k v :
+    m !! k = None →
+    gmap_auth_auth_ro m ~~> gmap_auth_auth_ro (<[k := v]> m) â‹… gmap_auth_frag_ro k v.
+  Proof.
+    intros Hfresh.
+    etrans; first apply (gmap_auth_alloc _ k v true).
+    - rewrite lookup_fmap Hfresh //.
+    - apply reflexive_eq. f_equal. rewrite /gmap_auth_auth_ro fmap_insert //.
+  Qed.
+
+  Lemma gmap_auth_update m k v v' ro :
+    gmap_auth_auth m â‹… gmap_auth_frag_mut k 1%Qp v ~~>
+      gmap_auth_auth (<[k := (ro, v')]> m) â‹…
+        gmap_auth_frag k (if ro then None else Some 1%Qp) v'.
+  Proof.
+    etrans.
+    - apply cmra_update_valid0=>Hval.
+      eapply auth_update, singleton_local_update_any=>??.
+      eapply (exclusive_local_update _ (to_auth_elem _ (ro, v'))).
+      apply to_auth_elem_valid.
+    - apply reflexive_eq. f_equal.
+      + rewrite /gmap_auth_auth to_auth_map_insert. done.
+      + destruct ro; done.
+  Qed.
+  Lemma gmap_auth_freeze m k v :
+    gmap_auth_auth m â‹… gmap_auth_frag_mut k 1%Qp v ~~>
+      gmap_auth_auth (<[k := (true, v)]> m) â‹… gmap_auth_frag_ro k v.
+  Proof.
+    etrans; first apply gmap_auth_update with (ro:=true).
+    apply reflexive_eq. f_equal.
+  Qed.
+  Lemma gmap_auth_mut_update (m : gmap K V) k v v' :
+    gmap_auth_auth_mut m â‹… gmap_auth_frag_mut k 1%Qp v ~~>
+      gmap_auth_auth_mut (<[k := v']> m) â‹… gmap_auth_frag_mut k 1%Qp v'.
+  Proof.
+    etrans; first apply gmap_auth_update with (ro:=false).
+    apply reflexive_eq. rewrite /gmap_auth_auth_mut fmap_insert.
+    f_equal.
+  Qed.
+
+  (** Typeclass instances
+  (These overlap up to conversion, but the functions are made TC-opaque below.) *)
+  Global Instance gmap_auth_frag_core_id k v :
+    CoreId (gmap_auth_frag k None v).
+  Proof. apply _. Qed.
+  Global Instance gmap_auth_frag_ro_core_id k v :
+    CoreId (gmap_auth_frag_ro k v).
+  Proof. apply _. Qed.
+
+  Global Instance gmap_auth_frag_mut_is_op q q1 q2 k v :
+    IsOp q q1 q2 →
+    IsOp' (gmap_auth_frag_mut k q v) (gmap_auth_frag_mut k q1 v) (gmap_auth_frag_mut k q2 v).
+  Proof. rewrite /IsOp' /IsOp => ->. apply gmap_auth_frag_mut_frac_op. Qed.
+
+  (** Internalized properties *)
+  Lemma gmap_auth_auth_frag_validI M m k mq v :
+    ✓ (gmap_auth_auth m ⋅ gmap_auth_frag k mq v) ⊢@{uPredI M}
+    m !! k ≡ Some (if mq is None then true else false, v).
+  Proof.
+    rewrite /gmap_auth_auth /gmap_auth_frag_mut.
+    rewrite auth_both_validI. iIntros "[Hmap Hval]".
+    iDestruct "Hmap" as (c) "Hmap".
+    set (q := default 1%Qp mq).
+    iApply (to_auth_map_singleton_includedI q).
+    destruct mq; try done.
+  Qed.
+
+  Lemma gmap_auth_auth_frag_mut_validI M m k q v :
+    ✓ (gmap_auth_auth m ⋅ gmap_auth_frag_mut k q v) ⊢@{uPredI M} m !! k ≡ Some (false, v).
+  Proof. apply gmap_auth_auth_frag_validI. Qed.
+  Lemma gmap_auth_auth_ro_frag_mut_validI M (m : gmap K V) k q v :
+    ✓ (gmap_auth_auth_mut m ⋅ gmap_auth_frag_mut k q v) ⊢@{uPredI M} m !! k ≡ Some v.
+  Proof.
+    rewrite /gmap_auth_auth_mut gmap_auth_auth_frag_mut_validI lookup_fmap /=.
+    rewrite !option_equivI. destruct (m !! k); simpl; last done.
+    rewrite prod_equivI /=. iIntros "[_ Heq]". done.
+  Qed.
+  Lemma gmap_auth_auth_frag_ro_validI M m k v :
+    ✓ (gmap_auth_auth m ⋅ gmap_auth_frag_ro k v) ⊢@{uPredI M} m !! k ≡ Some (true, v).
+  Proof. apply gmap_auth_auth_frag_validI. Qed.
+  Lemma gmap_auth_auth_ro_frag_ro_validI M (m : gmap K V) k v :
+    ✓ (gmap_auth_auth_ro m ⋅ gmap_auth_frag_ro k v) ⊢@{uPredI M} m !! k ≡ Some v.
+  Proof.
+    rewrite /gmap_auth_auth_ro gmap_auth_auth_frag_ro_validI lookup_fmap /=.
+    rewrite !option_equivI. destruct (m !! k); simpl; last done.
+    rewrite prod_equivI /=. iIntros "[_ Heq]". done.
+  Qed.
+
+End lemmas.
+
+(** Functor *)
+Definition gmap_authRF (K : Type) `{Countable K} (F : oFunctor) : rFunctor :=
+  authRF (gmapURF K (csumRF (prodRF fracR (agreeRF F)) (agreeRF F))).
+Instance gmap_authRF_contractive {K : Type} `{Countable K} (F : oFunctor) :
+  oFunctorContractive F → rFunctorContractive (gmap_authRF K F).
+Proof. apply _. Qed.
+
+Definition gmap_authURF (K : Type) `{Countable K} (F : oFunctor) : urFunctor :=
+  authURF (gmapURF K (csumRF (prodRF fracR (agreeRF F)) (agreeRF F))).
+Instance gmap_authURF_contractive {K : Type} `{Countable K} (F : oFunctor) :
+  oFunctorContractive F → urFunctorContractive (gmap_authURF K F).
+Proof. apply _. Qed.
+
+Typeclasses Opaque gmap_auth_auth gmap_auth_auth_mut gmap_auth_auth_ro
+  gmap_auth_frag gmap_auth_frag_mut gmap_auth_frag_ro gmap_authRF gmap_authURF.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 192f52783daae8fb80285556d3443118d218c521..a4e2985f631d69ebac38e6574cdf109fe613e50d 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,7 +1,7 @@
 From stdpp Require Export namespaces.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth gmap frac agree namespace_map.
+From iris.algebra Require Import gmap_auth namespace_map.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 Import uPred.
@@ -57,20 +57,10 @@ of both values and ghost names for meta information, for example:
 [gmap L (option (fracR * agreeR V) ∗ option (agree gname)]. Due to the [option]s,
 this RA would be quite inconvenient to deal with. *)
 
-Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
-  gmapUR L (prodR fracR (agreeR (leibnizO V))).
-Definition gen_metaUR (L : Type) `{Countable L} : ucmraT :=
-  gmapUR L (agreeR gnameO).
-
-Definition to_gen_heap {L V} `{Countable L} : gmap L V → gen_heapUR L V :=
-  fmap (λ v, (1%Qp, to_agree (v : leibnizO V))).
-Definition to_gen_meta `{Countable L} : gmap L gname → gen_metaUR L :=
-  fmap to_agree.
-
 (** The CMRA we need. *)
 Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
-  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
-  gen_meta_inG :> inG Σ (authR (gen_metaUR L));
+  gen_heap_inG :> inG Σ (gmap_authR L (leibnizO V));
+  gen_meta_inG :> inG Σ (gmap_authR L gnameO);
   gen_meta_data_inG :> inG Σ (namespace_mapR (agreeR positiveO));
   gen_heap_name : gname;
   gen_meta_name : gname
@@ -79,14 +69,14 @@ Arguments gen_heap_name {L V Σ _ _} _ : assert.
 Arguments gen_meta_name {L V Σ _ _} _ : assert.
 
 Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
-  gen_meta_preG_inG :> inG Σ (authR (gen_metaUR L));
+  gen_heap_preG_inG :> inG Σ (gmap_authR L (leibnizO V));
+  gen_meta_preG_inG :> inG Σ (gmap_authR L gnameO);
   gen_meta_data_preG_inG :> inG Σ (namespace_mapR (agreeR positiveO));
 }.
 
 Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
-  GFunctor (authR (gen_heapUR L V));
-  GFunctor (authR (gen_metaUR L));
+  GFunctor (gmap_authR L (leibnizO V));
+  GFunctor (gmap_authR L gnameO);
   GFunctor (namespace_mapR (agreeR positiveO))
 ].
 
@@ -97,28 +87,28 @@ Proof. solve_inG. Qed.
 Section definitions.
   Context `{Countable L, hG : !gen_heapG L V Σ}.
 
-  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := ∃ m,
+  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := ∃ m : gmap L gname,
     (* 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) (● (to_gen_heap σ)) ∗
-    own (gen_meta_name hG) (● (to_gen_meta m)).
+    own (gen_heap_name hG) (gmap_auth_auth_mut (σ : gmap L (leibnizO V))) ∗
+    own (gen_meta_name hG) (gmap_auth_auth_ro (m : gmap L gnameO)).
 
   Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
-    own (gen_heap_name hG) (â—¯ {[ l := (q, to_agree (v : leibnizO V)) ]}).
+    own (gen_heap_name hG) (gmap_auth_frag_mut l q (v : leibnizO V)).
   Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
   Definition mapsto := mapsto_aux.(unseal).
   Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
 
   Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
-    ∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
+    ∃ γm, own (gen_meta_name hG) (gmap_auth_frag_ro l γm) ∗
           own γm (namespace_map_token E).
   Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
   Definition meta_token := meta_token_aux.(unseal).
   Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
 
   Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
-    ∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
+    ∃ γm, own (gen_meta_name hG) (gmap_auth_frag_ro l γm) ∗
           own γm (namespace_map_data N (to_agree (encode x))).
   Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
   Definition meta := meta_aux.(unseal).
@@ -134,43 +124,13 @@ Local Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
 Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
-Section to_gen_heap.
-  Context (L V : Type) `{Countable L}.
-  Implicit Types σ : gmap L V.
-  Implicit Types m : gmap L gname.
-
-  (** Conversion to heaps and back *)
-  Lemma to_gen_heap_valid σ : ✓ to_gen_heap σ.
-  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
-  Lemma lookup_to_gen_heap_None σ l : σ !! l = None → to_gen_heap σ !! l = None.
-  Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed.
-  Lemma gen_heap_singleton_included σ l q v :
-    {[l := (q, to_agree v)]} ≼ to_gen_heap σ → σ !! l = Some v.
-  Proof.
-    rewrite singleton_included_l=> -[[q' av] []].
-    rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
-    move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
-  Qed.
-  Lemma to_gen_heap_insert l v σ :
-    to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizO V))]> (to_gen_heap σ).
-  Proof. by rewrite /to_gen_heap fmap_insert. Qed.
-
-  Lemma to_gen_meta_valid m : ✓ to_gen_meta m.
-  Proof. intros l. rewrite lookup_fmap. by case (m !! l). Qed.
-  Lemma lookup_to_gen_meta_None m l : m !! l = None → to_gen_meta m !! l = None.
-  Proof. by rewrite /to_gen_meta lookup_fmap=> ->. Qed.
-  Lemma to_gen_meta_insert l m γm :
-    to_gen_meta (<[l:=γm]> m) = <[l:=to_agree γm]> (to_gen_meta m).
-  Proof. by rewrite /to_gen_meta fmap_insert. Qed.
-End to_gen_heap.
-
 Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ.
 Proof.
-  iMod (own_alloc (● to_gen_heap σ)) as (γh) "Hh".
-  { rewrite auth_auth_valid. exact: to_gen_heap_valid. }
-  iMod (own_alloc (● to_gen_meta ∅)) as (γm) "Hm".
-  { rewrite auth_auth_valid. exact: to_gen_meta_valid. }
+  iMod (own_alloc (gmap_auth_auth_mut (σ : gmap L (leibnizO V)))) as (γh) "Hh".
+  { exact: gmap_auth_auth_mut_valid. }
+  iMod (own_alloc (gmap_auth_auth_ro (∅ : gmap L gnameO))) as (γm) "Hm".
+  { exact: gmap_auth_auth_ro_valid. }
   iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
   iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
 Qed.
@@ -181,7 +141,6 @@ Section gen_heap.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.
   Implicit Types m : gmap L gname.
-  Implicit Types h g : gen_heapUR L V.
   Implicit Types l : L.
   Implicit Types v : V.
 
@@ -190,8 +149,7 @@ Section gen_heap.
   Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
-    intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
-      singleton_op -pair_op agree_idemp.
+    intros p q. rewrite mapsto_eq /mapsto_def -own_op gmap_auth_frag_mut_frac_op //.
   Qed.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
@@ -200,9 +158,8 @@ Section gen_heap.
   Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     apply wand_intro_r.
-    rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
-    f_equiv. rewrite auth_frag_valid singleton_op singleton_valid -pair_op.
-    by intros [_ ?%to_agree_op_inv_L].
+    rewrite mapsto_eq /mapsto_def -own_op own_valid discrete_valid.
+    apply pure_mono. intros [_ ?]%gmap_auth_frag_mut_op_valid_L. done.
   Qed.
 
   Lemma mapsto_combine l q1 q2 v1 v2 :
@@ -225,8 +182,8 @@ Section gen_heap.
 
   Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
   Proof.
-    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid -auth_frag_valid.
-    by apply pure_mono=> /singleton_valid [??].
+    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
+    rewrite gmap_auth_frag_mut_valid //.
   Qed.
   Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
   Proof.
@@ -261,10 +218,7 @@ Section gen_heap.
   Proof.
     rewrite meta_token_eq /meta_token_def.
     iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
-    iAssert ⌜ γm1 = γm2 ⌝%I as %->.
-    { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
-      move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
-      rewrite singleton_valid. apply: to_agree_op_inv_L. }
+    iDestruct (own_valid_2 with "Hγm1 Hγm2") as %->%gmap_auth_frag_ro_op_valid_L.
     iDestruct (own_valid_2 with "Hm1 Hm2") as %?%namespace_map_token_valid_op.
     iExists γm2. iFrame "Hγm2". rewrite namespace_map_token_union //. by iSplitL "Hm1".
   Qed.
@@ -287,10 +241,7 @@ Section gen_heap.
   Proof.
     rewrite meta_eq /meta_def.
     iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
-    iAssert ⌜ γm1 = γm2 ⌝%I as %->.
-    { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
-      move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
-      rewrite singleton_valid. apply: to_agree_op_inv_L. }
+    iDestruct (own_valid_2 with "Hγm1 Hγm2") as %->%gmap_auth_frag_ro_op_valid_L.
     iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
     move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
     move=> /to_agree_op_inv_L. naive_solver.
@@ -311,20 +262,15 @@ Section gen_heap.
     iIntros (Hσl). rewrite /gen_heap_ctx mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
     iDestruct 1 as (m Hσm) "[Hσ Hm]".
     iMod (own_update with "Hσ") as "[Hσ Hl]".
-    { eapply auth_update_alloc,
-        (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizO _)))=> //.
-      by apply lookup_to_gen_heap_None. }
+    { eapply (gmap_auth_mut_alloc _ l). done. }
     iMod (own_alloc (namespace_map_token ⊤)) as (γm) "Hγm".
     { apply namespace_map_token_valid. }
     iMod (own_update with "Hm") as "[Hm Hlm]".
-    { eapply auth_update_alloc.
-      eapply (alloc_singleton_local_update _ l (to_agree γm))=> //.
-      apply lookup_to_gen_meta_None.
+    { eapply (gmap_auth_ro_alloc _ l). 
       move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
     iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
-    iExists (<[l:=γm]> m).
-    rewrite to_gen_heap_insert to_gen_meta_insert !dom_insert_L. iFrame.
-    iPureIntro. set_solver.
+    iExists (<[l:=γm]> m). iFrame. iPureIntro.
+    rewrite !dom_insert_L. set_solver.
   Qed.
 
   Lemma gen_heap_alloc_gen σ σ' :
@@ -345,8 +291,8 @@ Section gen_heap.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
     rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
-    iDestruct (own_valid_2 with "Hσ Hl")
-      as %[Hl%gen_heap_singleton_included _]%auth_both_valid_discrete; auto.
+    iDestruct (own_valid_2 with "Hσ Hl") as %?%gmap_auth_auth_mut_frag_mut_valid.
+    iPureIntro. fold_leibniz. done.
   Qed.
 
   Lemma gen_heap_update σ l v1 v2 :
@@ -354,13 +300,10 @@ Section gen_heap.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ Hm]".
     iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
-    iDestruct (own_valid_2 with "Hσ Hl")
-      as %[Hl%gen_heap_singleton_included _]%auth_both_valid_discrete.
+    iDestruct (own_valid_2 with "Hσ Hl") as %Hl%gmap_auth_auth_mut_frag_mut_valid_L.
     iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
-    { eapply auth_update, singleton_local_update,
-        (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizO _)))=> //.
-      by rewrite /to_gen_heap lookup_fmap Hl. }
-    iModIntro. iFrame "Hl". iExists m. rewrite to_gen_heap_insert. iFrame.
+    { eapply gmap_auth_mut_update. }
+    iModIntro. iFrame "Hl". iExists m. iFrame.
     iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl.
     rewrite dom_insert_L. set_solver.
   Qed.
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 0871ea090e9231239db1f06fc5bdda343e8577da..c0b015f06f3f9e28b7f1487238197e0cb4ef552a 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth excl list gmap.
+From iris.algebra Require Import gmap_auth list.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 Import uPred.
@@ -7,24 +7,18 @@ Import uPred.
 Local Notation proph_map P V := (gmap P (list V)).
 Definition proph_val_list (P V : Type) := list (P * V).
 
-Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
-  gmapUR P $ exclR $ listO $ leibnizO V.
-
-Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
-  fmap (λ vs, Excl (vs : list (leibnizO V))) pvs.
-
 (** The CMRA we need. *)
 Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
-  proph_map_inG :> inG Σ (authR (proph_mapUR P V));
+  proph_map_inG :> inG Σ (gmap_authR P (listO (leibnizO V)));
   proph_map_name : gname
 }.
 Arguments proph_map_name {_ _ _ _ _} _ : assert.
 
 Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
-  { proph_map_preG_inG :> inG Σ (authR (proph_mapUR P V)) }.
+  { proph_map_preG_inG :> inG Σ (gmap_authR P (listO $ leibnizO V)) }.
 
 Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
-  #[GFunctor (authR (proph_mapUR P V))].
+  #[GFunctor (gmap_authR P (listO $ leibnizO V))].
 
 Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
   subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
@@ -50,10 +44,10 @@ Section definitions.
   Definition proph_map_ctx pvs (ps : gset P) : iProp Σ :=
     (∃ R, ⌜proph_resolves_in_list R pvs ∧
           dom (gset _) R ⊆ ps⌝ ∗
-          own (proph_map_name pG) (● (to_proph_map R)))%I.
+          own (proph_map_name pG) (gmap_auth_auth_mut (V:=listO $ leibnizO V) R))%I.
 
   Definition proph_def (p : P) (vs : list V) : iProp Σ :=
-    own (proph_map_name pG) (â—¯ {[p := Excl vs]}).
+    own (proph_map_name pG) (gmap_auth_frag_mut (V:=listO $ leibnizO V) p 1 vs).
 
   Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
   Definition proph := proph_aux.(unseal).
@@ -78,42 +72,13 @@ Section list_resolves.
   Qed.
 End list_resolves.
 
-Section to_proph_map.
-  Context (P V : Type) `{Countable P}.
-  Implicit Types p : P.
-  Implicit Types vs : list V.
-  Implicit Types R : proph_map P V.
-
-  Lemma to_proph_map_valid R : ✓ to_proph_map R.
-  Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
-
-  Lemma to_proph_map_insert p vs R :
-    to_proph_map (<[p := vs]> R) = <[p := Excl (vs: list (leibnizO V))]> (to_proph_map R).
-  Proof. by rewrite /to_proph_map fmap_insert. Qed.
-
-  Lemma to_proph_map_delete p R :
-    to_proph_map (delete p R) = delete p (to_proph_map R).
-  Proof. by rewrite /to_proph_map fmap_delete. Qed.
-
-  Lemma lookup_to_proph_map_None R p :
-    R !! p = None → to_proph_map R !! p = None.
-  Proof. by rewrite /to_proph_map lookup_fmap=> ->. Qed.
-
-  Lemma proph_map_singleton_included R p vs :
-    {[p := Excl vs]} ≼ to_proph_map R → R !! p = Some vs.
-  Proof.
-    rewrite singleton_included_exclusive_l; last by apply to_proph_map_valid.
-    by rewrite leibniz_equiv_iff /to_proph_map lookup_fmap fmap_Some=> -[v' [-> [->]]].
-  Qed.
-End to_proph_map.
-
 Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
   ⊢ |==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps.
 Proof.
-  iMod (own_alloc (● to_proph_map ∅)) as (γ) "Hh".
-  { rewrite auth_auth_valid. exact: to_proph_map_valid. }
+  iMod (own_alloc (gmap_auth_auth_mut ∅)) as (γ) "Hh".
+  { apply gmap_auth_auth_mut_valid. }
   iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
-  iPureIntro. split =>//.
+  iPureIntro. done.
 Qed.
 
 Section proph_map.
@@ -133,9 +98,8 @@ Section proph_map.
   Proof.
     rewrite proph_eq /proph_def. iIntros "Hp1 Hp2".
     iCombine "Hp1 Hp2" as "Hp".
-    iDestruct (own_valid with "Hp") as %Hp.
-    (* FIXME: FIXME(Coq #6294): needs new unification *)
-    move:Hp. rewrite auth_frag_valid singleton_valid //.
+    iDestruct (own_valid with "Hp") as %[Hp _]%gmap_auth_frag_mut_op_valid_L.
+    done.
   Qed.
 
   Lemma proph_map_new_proph p ps pvs :
@@ -146,15 +110,13 @@ Section proph_map.
     iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
     rewrite proph_eq /proph_def.
     iMod (own_update with "H●") as "[H● H◯]".
-    { eapply auth_update_alloc, (alloc_singleton_local_update _ p (Excl _))=> //.
-      apply lookup_to_proph_map_None.
+    { eapply (gmap_auth_mut_alloc _ p).
       apply (not_elem_of_dom (D:=gset P)). set_solver. }
     iModIntro. iFrame.
-    iExists (<[p := proph_list_resolves pvs p]> R). iSplitR "H●".
-    - iPureIntro. split.
-      + apply resolves_insert; first done. set_solver.
-      + rewrite dom_insert. set_solver.
-    - by rewrite /to_proph_map fmap_insert.
+    iExists (<[p := proph_list_resolves pvs p]> R).
+    iFrame. iPureIntro. split.
+    - apply resolves_insert; first done. set_solver.
+    - rewrite dom_insert. set_solver.
   Qed.
 
   Lemma proph_map_resolve_proph p v pvs ps vs :
@@ -163,15 +125,11 @@ Section proph_map.
   Proof.
     iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
     rewrite /proph_map_ctx proph_eq /proph_def.
-    iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_both_valid_discrete.
+    iDestruct (own_valid_2 with "H● Hp") as %HR%gmap_auth_auth_mut_frag_mut_valid_L.
     assert (vs = v :: proph_list_resolves pvs p) as ->.
     { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
     iMod (own_update_2 with "H● Hp") as "[H● H◯]".
-    { (* FIXME: FIXME(Coq #6294): needs new unification *)
-      eapply auth_update. apply: singleton_local_update.
-      - by rewrite /to_proph_map lookup_fmap HR.
-      - by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizO V)))). }
-    rewrite /to_proph_map -fmap_insert.
+    { eapply gmap_auth_mut_update. }
     iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
     - iPureIntro. done.
     - iExists _. iFrame. iPureIntro. split.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 3ba248786e8b7cdfebf28bc939e44af71b20212b..cac8c5af6bd58d8129709468c312a5b616040042 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -1,6 +1,6 @@
 From stdpp Require Export coPset.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.algebra Require Import gmap_auth gset coPset.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 
@@ -9,7 +9,7 @@ exception of what's in the [invG] module. The module [invG] is thus exported in
 [fancy_updates], which [wsat] is only imported. *)
 Module invG.
   Class invG (Σ : gFunctors) : Set := WsatG {
-    inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPropO Σ)))));
+    inv_inG :> inG Σ (gmap_authR positive (laterO (iPropO Σ)));
     enabled_inG :> inG Σ coPset_disjR;
     disabled_inG :> inG Σ (gset_disjR positive);
     invariant_name : gname;
@@ -18,12 +18,12 @@ Module invG.
   }.
 
   Definition invΣ : gFunctors :=
-    #[GFunctor (authRF (gmapURF positive (agreeRF (laterOF idOF))));
+    #[GFunctor (gmap_authRF positive (laterOF idOF));
       GFunctor coPset_disjUR;
       GFunctor (gset_disjUR positive)].
 
   Class invPreG (Σ : gFunctors) : Set := WsatPreG {
-    inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPropO Σ)))));
+    inv_inPreG :> inG Σ (gmap_authR positive (laterO (iPropO Σ)));
     enabled_inPreG :> inG Σ coPset_disjR;
     disabled_inPreG :> inG Σ (gset_disjR positive);
   }.
@@ -33,10 +33,10 @@ Module invG.
 End invG.
 Import invG.
 
-Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iProp Σ)) :=
-  to_agree (Next P).
+Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
+  Next P.
 Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
-  own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
+  own invariant_name (gmap_auth_frag_ro i (invariant_unfold P)).
 Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
 Instance: Params (@invariant_unfold) 1 := {}.
@@ -54,7 +54,7 @@ Instance: Params (@ownD) 3 := {}.
 
 Definition wsat `{!invG Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
-    own invariant_name (● (invariant_unfold <$> I : gmap _ _)) ∗
+    own invariant_name (gmap_auth_auth_ro (invariant_unfold <$> I)) ∗
     [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
 
 Section wsat.
@@ -106,22 +106,15 @@ 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 (● (invariant_unfold <$> I : gmap _ _)) ∗
-  own invariant_name (◯ {[i := invariant_unfold P]}) ⊢
+  own invariant_name (gmap_auth_auth_ro (invariant_unfold <$> I)) ∗
+  own invariant_name (gmap_auth_frag_ro i (invariant_unfold P)) ⊢
   ∃ Q, ⌜I !! i = Some Q⌝ ∗ ▷ (Q ≡ P).
 Proof.
-  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 lookup_fmap lookup_op lookup_singleton 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 "?".
-  { case: (I' !! i)=> [Q'|] //=.
-    iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI.
-    iRewrite -"HvI" in "HI". by rewrite agree_idemp. }
-  rewrite /invariant_unfold.
-  by rewrite agree_equivI later_equivI.
+  rewrite -own_op own_valid gmap_auth_auth_ro_frag_ro_validI.
+  rewrite lookup_fmap option_equivI.
+  case: (I !! i)=> [Q|] /=; last by eauto.
+  iIntros "?". iExists Q; iSplit; first done.
+  by rewrite later_equivI.
 Qed.
 
 Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
@@ -159,12 +152,10 @@ Proof.
       as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
   iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
   iMod (own_update with "Hw") as "[Hw HiP]".
-  { eapply auth_update_alloc,
-     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
-    by rewrite /= lookup_fmap HIi. }
+  { eapply (gmap_auth_ro_alloc _ i). by rewrite /= lookup_fmap HIi. }
   iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
   iExists (<[i:=P]>I); iSplitL "Hw".
-  { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
+  { by rewrite fmap_insert. }
   iApply (big_sepM_insert _ I); first done.
   iFrame "HI". iLeft. by rewrite /ownD; iFrame.
 Qed.
@@ -181,13 +172,11 @@ Proof.
       as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
   iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
   iMod (own_update with "Hw") as "[Hw HiP]".
-  { eapply auth_update_alloc,
-     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
-    by rewrite /= lookup_fmap HIi. }
+  { eapply (gmap_auth_ro_alloc _ i). by rewrite /= lookup_fmap HIi. }
   iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
   rewrite -/(ownD _). iFrame "HD".
   iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
-  { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
+  { by rewrite fmap_insert. }
   iApply (big_sepM_insert _ I); first done.
   iFrame "HI". by iRight.
 Qed.
@@ -197,8 +186,8 @@ End wsat.
 Lemma wsat_alloc `{!invPreG Σ} : ⊢ |==> ∃ _ : invG Σ, wsat ∗ ownE ⊤.
 Proof.
   iIntros.
-  iMod (own_alloc (● (∅ : gmap positive _))) as (γI) "HI";
-    first by rewrite auth_auth_valid.
+  iMod (own_alloc (gmap_auth_auth_ro ∅)) as (γI) "HI";
+    first by apply gmap_auth_auth_ro_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).