From 900ed833746a8c2a1c9dd0a01f4f74d253a8e9ac Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 11 Apr 2018 16:30:12 +0200
Subject: [PATCH] Get rid of dec_agree.

---
 theories/adequacy.v              |  6 ++--
 theories/base/accessors.v        |  2 +-
 theories/base/alloc.v            |  3 +-
 theories/base/ghosts.v           | 50 ++++++++++++++------------------
 theories/fractor.v               | 26 ++++++++---------
 theories/gps/fractional.v        |  6 ++--
 theories/gps/init.v              |  7 +++--
 theories/gps/inst_shared.v       | 11 +++----
 theories/gps/plain.v             | 28 +++++++++---------
 theories/gps/shared.v            | 26 ++++++++---------
 theories/gps/write.v             |  6 ++--
 theories/persistor.v             | 25 +++++++---------
 theories/tests/message_passing.v |  6 ++--
 13 files changed, 95 insertions(+), 107 deletions(-)

diff --git a/theories/adequacy.v b/theories/adequacy.v
index a091344b..722d5c69 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre adequacy ownp.
 From iris.base_logic Require Import lib.invariants.
-From iris.algebra Require Import auth.
+From iris.algebra Require Import auth agree.
 Set Default Proof Using "Type".
 
 From igps Require Import lang proofmode.
@@ -32,10 +32,10 @@ Definition to_hist (σ : language.state ra_lang) : Hists :=
 (* TODO: can we avoid this? *)
 (* Definition to_info (σ : language.state ra_lang) : Infos := *)
 (*   let locs := {[ mloc m | m <- msgs (mem σ) ]} in *)
-(*   let infos : gmap loc (frac.fracR * _) := to_gmap (1%Qp, DecAgree 1%positive) locs in *)
+(*   let infos : gmap loc (frac.fracR * _) := to_gmap (1%Qp, to_agree 1%positive) locs in *)
 (*   (infos). *)
 Definition to_info (σ : language.state ra_lang) : Infos :=
-  (λ _, (1%Qp, DecAgree 1%positive)) <$> to_hist σ.
+  (λ _, (1%Qp, to_agree 1%positive)) <$> to_hist σ.
 
 Lemma NoDup_omap {A B : Type} (l : list A) (f : A -> option B) : Inj (=) (=) f -> NoDup l -> NoDup (omap f l).
 Proof.
diff --git a/theories/base/accessors.v b/theories/base/accessors.v
index 34329a8e..ce3adfbd 100644
--- a/theories/base/accessors.v
+++ b/theories/base/accessors.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Import lib.invariants lib.viewshifts.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import ownp.
-From iris.algebra Require Import auth excl gmap.
+From iris.algebra Require Import auth excl gmap agree.
 
 From igps Require Import infrastructure machine lang history.
 From igps Require Export ghosts.
diff --git a/theories/base/alloc.v b/theories/base/alloc.v
index 94be0be5..5dfef341 100644
--- a/theories/base/alloc.v
+++ b/theories/base/alloc.v
@@ -1,5 +1,6 @@
 From igps.base Require Import ghosts at_shared.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import agree.
 From igps Require Import lang.
 Import lang.base.
 
@@ -102,7 +103,7 @@ Section Alloc.
     (* assert (HNone: HIST !! l = None). *)
     (*   { by rewrite Hist_Info_fresh. } *)
 
-    pose v := DecAgree 1%positive.
+    pose v := to_agree 1%positive.
 
     iMod ((Infos_alloc _ _ v) with "oAI") as "oAI"; [eauto|done|].
 
diff --git a/theories/base/ghosts.v b/theories/base/ghosts.v
index 10fecce7..47ce0670 100644
--- a/theories/base/ghosts.v
+++ b/theories/base/ghosts.v
@@ -1,8 +1,6 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth frac excl gmap.
+From iris.algebra Require Import auth frac excl gmap agree.
 From iris.program_logic Require Import ownp.
-From iris.algebra Require Import deprecated.
-Export deprecated.dec_agree.
 From iris.base_logic Require Import lib.invariants.
 From iris.algebra Require Import big_op.
 From igps Require Import lang history.
@@ -11,10 +9,10 @@ Set Bullet Behavior "Strict Subproofs".
 
 Notation History := (gset (@Val * View))%type.
 
-Definition InfoT := positive.
+Definition InfoT := positiveC.
 Definition Views := (gmapUR thread (exclR (leibnizC View))).
 Definition Hists := ((gmapUR loc (exclR (leibnizC History)))).
-Definition Infos := ((gmapUR loc (prodR fracR (dec_agreeR InfoT)))).
+Definition Infos := ((gmapUR loc (prodR fracR (agreeR InfoT)))).
 
 Class foundationG Σ :=
   FoundationG {
@@ -181,7 +179,7 @@ Section GhostDefs.
     λ π V, own VN (◯ ({[π := Excl V]}: Views)).
   Definition Hist : loc -> History -> iProp Σ :=
     λ l h, own HN (◯ ({[l := Excl h]})).
-  Definition Info : loc -> frac -> dec_agree InfoT -> iProp Σ :=
+  Definition Info : loc -> frac -> agree InfoT -> iProp Σ :=
     λ l q v, own IN (◯ ({[l := (q, v)]})).
 
   Definition LInv Ï‚ l h :=
@@ -266,26 +264,20 @@ Section ValidGhosts.
 
   Lemma Infos_frag_valid_eq l (q: Qp) v (INFO: Infos)
     (Valid: ✓ (● INFO ⋅ ◯ {[l := (q, v)]}))
-    : ∃(q': Qp), INFO !! l = Some (q',v) ∧ (q ≤ q')%Qc.
+    : ∃(q': Qp), INFO !! l ≡ Some (q',v) ∧ (q ≤ q')%Qc.
   Proof.
     move/auth_valid_discrete_2 : Valid => [/lookup_included /(_ l) Incl Valid].
     rewrite lookup_singleton in Incl.
-    apply option_included in Incl as [|[qv [qv' [Eq1 [Eq2 Incl]]]]]; first done.
-    apply leibniz_equiv_iff in Eq2.
-    assert (Valid2 := lookup_valid_Some _ _ _ Valid Eq2).
-    apply leibniz_equiv in Eq2.
-    destruct Incl as [Eq|Incl].
-    - apply leibniz_equiv in Eq. rewrite -Eq -Eq1 in Eq2.
-      by exists q.
-    - inversion Eq1. subst. destruct Valid2 as [Validq Validv'].
+    apply option_included in Incl as [|[qv [qv' [[= <-] [Eq2 Incl]]]]]; [done|].
+    assert (Valid2 := lookup_valid_Some _ _ _ Valid (reflexive_eq _ _ Eq2)).
+    rewrite Eq2. clear Eq2. destruct Incl as [Eq|Incl].
+    - setoid_subst. eauto.
+    - destruct Valid2 as [_ Validv'].
       destruct qv' as [q' v'].
-      destruct Incl as [? [Inclq Incl]]. simpl in *.
-      apply leibniz_equiv in Incl. rewrite Incl in Validv'.
-      apply dec_agree_op_inv in Validv'.
-      rewrite -Validv' dec_agree_idemp in Incl. subst v'.
-      exists q'. split; first auto.
-      apply leibniz_equiv in Inclq.
-      rewrite Inclq frac_op' -{1}(Qcanon.Qcplus_0_r q).
+      destruct Incl as [? [Inclq Incl]]. simpl in *. setoid_subst.
+      apply agree_op_inv in Validv'. setoid_subst. setoid_rewrite (agree_idemp x.2).
+      eexists _. split; first by auto.
+      rewrite frac_op' -{1}(Qcanon.Qcplus_0_r q).
       apply (Qcplus_le_mono_l 0%Z (x.1) q), Qcanon.Qclt_le_weak.
       destruct x => /=. by destruct c.
   Qed.
@@ -495,7 +487,7 @@ Section UpdateGhosts.
   Collection level1 := Σ fG.
   Local Set Default Proof Using "level1".
 
-  Implicit Types (π ρ : thread) (l : loc) (V : View) (h : History) (v: dec_agreeR InfoT).
+  Implicit Types (π ρ : thread) (l : loc) (V : View) (h : History) (v: agreeR InfoT).
   Local Open Scope I.
 
   Lemma Views_update_override π V (VIEW: Views) V'
@@ -548,10 +540,10 @@ Section UpdateGhosts.
   Proof.
     move => vV. iIntros "FI".
     iDestruct (own_valid with "FI") as %Valid.
-    apply Infos_frag_valid_eq in Valid as [q' [Valid1 Valid2]].
+    apply Infos_frag_valid_eq in Valid as [q' [(?&?&?)%equiv_Some_inv_r' Valid2]].
     iMod (own_update with "[$FI]"); last iAssumption.
     apply auth_update.
-    apply: singleton_local_update; first eauto.
+    eapply singleton_local_update; first by eauto.
     by apply exclusive_local_update.
   Qed.
 
@@ -602,12 +594,12 @@ Section UpdateGhosts.
   Lemma IInv_update
     Ï‚ INFO l zv zv'
     (Inv: IInv Ï‚ INFO)
-    (Hl: INFO !! l = Some zv)
+    (Hl: INFO !! l ≡ Some zv)
     : IInv Ï‚ (<[l:=zv']> INFO).
   Proof.
-    cbn in *.
-    rewrite <-Inv.
-    have H : l ∈ dom (gset loc) INFO by apply: elem_of_dom_2.
+    cbn in *. rewrite <-Inv.
+    assert (H : l ∈ dom (gset loc) INFO).
+    { destruct (equiv_Some_inv_r' _ _ Hl) as (? &? &?). by apply: elem_of_dom_2. }
     rewrite dom_insert.
     abstract set_solver+H Inv.
   Qed.
diff --git a/theories/fractor.v b/theories/fractor.v
index 8edd8397..5790dd09 100644
--- a/theories/fractor.v
+++ b/theories/fractor.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth frac excl gmap .
+From iris.algebra Require Import auth frac excl gmap agree.
 From iris.bi Require Import big_op fractional.
 From iris.base_logic.lib Require Import cancelable_invariants.
 From stdpp Require Export namespaces.
@@ -19,7 +19,7 @@ Section Fractor.
 
   Definition fractored l φ Ψ p: iProp Σ :=
     (∃ X, Ψ l p X
-      ∗ ∃ γ, Info l p (DecAgree (encode (X,γ)))
+      ∗ ∃ γ, Info l p (to_agree (encode (X,γ)))
       ∗ cinv_own γ p ∗ cinv (fracN .@ l) γ (φ l X))%I.
 
   Global Instance fractored_proper l : Proper ((≡) ==> (≡) ==> (=) ==> (≡)) (fractored l).
@@ -65,8 +65,8 @@ Section Fractor.
   Qed.
 
   Lemma Info_join l p1 p2 v1 v2:
-    Info l p1 (DecAgree v1) ∗ Info l p2 (DecAgree v2)
-    ⊢ ⌜v1 = v2⌝ ∗ Info l (p1 + p2) (DecAgree v1).
+    Info l p1 (to_agree v1) ∗ Info l p2 (to_agree v2)
+    ⊢ ⌜v1 = v2⌝ ∗ Info l (p1 + p2) (to_agree v1).
   Proof.
     iIntros "[Info1 Info2]".
     iCombine "Info1" "Info2" as "Info".
@@ -74,9 +74,8 @@ Section Fractor.
     iDestruct (own_valid with "Info") as %Valid.
     apply singleton_valid in Valid.
     destruct Valid as [_ Valid2]. simpl in Valid2.
-    apply dec_agree_op_inv in Valid2. inversion Valid2 as [Eq].
-    iSplitR "Info"; auto.
-    by rewrite dec_agree_idemp.
+    apply agree_op_inv, (inj to_agree) in Valid2. setoid_subst.
+    iSplitR "Info"; auto. by rewrite agree_idemp.
   Qed.
 
   Lemma fractor_splitjoin l φ Ψ1 Ψ2 p1 p2:
@@ -99,9 +98,11 @@ Section Fractor.
     - iIntros "Frac".
       iDestruct "Frac" as (X) "[[Pred1 Pred2] Frac]".
       iDestruct "Frac" as (γ) "[Info [FOwn #FCtx]]".
-      rewrite fractional /Info.
-      rewrite -(dec_agree_idemp (DecAgree (encode (X,γ)))).
-      rewrite -pair_op -op_singleton auth_frag_op.
+      rewrite fractional (_:Info l (p1+p2) _ ≡ (Info l p1 _ ∗ Info l p2 _)%I);
+        last first.
+      { rewrite /Info /Infos -own_op -auth_frag_op op_singleton pair_op.
+        do 2 f_equiv. apply: fin_maps.singleton_proper.
+        by rewrite -[to_agree _]agree_idemp. }
       iDestruct "Info" as "[Info1 Info2]".
       iDestruct "FOwn" as "[FOwn1 FOwn2]".
       iSplitL "Pred1 Info1 FOwn1".
@@ -170,7 +171,7 @@ Section Fractor.
     intros Sub.
     iIntros "[#PS [Info [Inv Pred]]]".
     iMod ((cinv_alloc E (fracN .@ l) (φ l X)) with "Inv") as (γ) "[FOwn Ctx]".
-    iAssert (|={E}=> Info l 1 (DecAgree (encode (X,γ))))%I
+    iAssert (|={E}=> Info l 1 (to_agree (encode (X,γ))))%I
       with "[Info]" as ">Info".
       { iApply PSInv_Info_update => //; auto. }
     iModIntro.
@@ -186,7 +187,7 @@ Section Fractor.
     iDestruct "Frac" as (γ) "[Info [FOwn #Ctx]]".
     iMod ((cinv_cancel _ _ _ _ Sub) with "Ctx FOwn") as "Inv".
     iModIntro.
-    iExists X, (DecAgree (encode (X,γ))). by iFrame.
+    iExists X, (to_agree (encode (X,γ))). by iFrame.
   Qed.
 
   Lemma fractor_open' E l φ Ψ p:
@@ -217,5 +218,4 @@ Section Fractor.
     iModIntro. iExists X. iFrame. iIntros (Ψ') "[Inv Pred]".
     iMod ("HClose" with "Inv"). by iApply "HT".
   Qed.
-
 End Fractor.
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index 541f163a..adb3e7d5 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -487,10 +487,8 @@ Section Fractional.
       iExists γ, γ_x, e_x. iFrame "R2". iSplit; first auto.
       iCombine "ex1" "ex2" as "ex".
       iDestruct (own.own_valid with "ex") as %Val%auth_valid_discrete.
-      move: Val => [_ /= /dec_agree_op_inv Eqe].
-      inversion Eqe. subst.
-      iDestruct "ex" as "[ex1 ex2]". rewrite dec_agree_idemp.
-      iSplitL "ex1"; iFrame.
+      move: Val => [_ /= /agree_op_inv /to_agree_inj Eqe]. setoid_subst.
+      iDestruct "ex" as "[ex1 ex2]". rewrite agree_idemp. iSplitL "ex1"; iFrame.
   Qed.
 
   Lemma GPS_FP_splitjoin l s q1 q2:
diff --git a/theories/gps/init.v b/theories/gps/init.v
index 5d62222f..6adbd07d 100644
--- a/theories/gps/init.v
+++ b/theories/gps/init.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Import weakestpre.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import agree.
 From igps.gps Require Import shared.
 From igps.base Require Import na_write.
 
@@ -7,7 +8,7 @@ Section Init_Strong.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF}
           (IP : gname -> interpC Σ Prtcl) (l : loc).
   Set Default Proof Using "Type".
-  Notation state_sort := (pr_state Prtcl * (Z * View))%type.
+  Notation state_sort := (leibnizC (pr_state Prtcl * (Z * View))%type).
   Implicit Types
            (s : pr_state Prtcl)
            (ζ : state_type Prtcl)
@@ -50,8 +51,8 @@ Section Init_Strong.
     { apply auth_update, auth_local_update; [|auto|done].
       by apply gset_local_update. }
 
-    iMod (own.own_alloc (● Some (1%Qp, DecAgree ((s γ), (v, V')))
-                        ⋅ ◯ Some (1%Qp, DecAgree ((s γ), (v, V')))))
+    iMod (own.own_alloc (● Some (1%Qp, @to_agree state_sort ((s γ), (v, V')))
+                        ⋅ ◯ Some (1%Qp, @to_agree state_sort ((s γ), (v, V')))))
          as (γ_x) "[exA ex]".
       { by apply auth_valid_discrete_2. }
 
diff --git a/theories/gps/inst_shared.v b/theories/gps/inst_shared.v
index 65f0d4b2..df8757e9 100644
--- a/theories/gps/inst_shared.v
+++ b/theories/gps/inst_shared.v
@@ -1,13 +1,14 @@
 From iris.base_logic.lib Require Import invariants.
-From iris.algebra Require Export auth.
+From iris.algebra Require Export auth agree.
 
 From igps Require Export persistor fractor proofmode weakestpre viewpred.
 From igps Require Export notation na.
 From igps.gps Require Export raw.
 
-Definition state_sort_eqdec Prtcl {PF : protocol_facts Prtcl} : EqDecision (state_sort Prtcl) := _.
-Notation gps_agreeG Σ Prtcl := (own.inG Σ (dec_agreeR (EqDecision0 := state_sort_eqdec Prtcl%type) (state_sort Prtcl))).
-Definition gps_agreeΣ Prtcl (PF : protocol_facts Prtcl) : gFunctors := #[ GFunctor (constRF ((dec_agreeR (EqDecision0 := state_sort_eqdec Prtcl%type) (state_sort Prtcl)))) ].
+Class gps_agreeG Σ Prtcl :=
+  gps_agreeG_inG :> own.inG Σ (agreeR (state_sort Prtcl)).
+Definition gps_agreeΣ Prtcl : gFunctors :=
+  #[ GFunctor (constRF ((agreeR (state_sort Prtcl)))) ].
 
-Instance subG_gps_agreeΣ Σ Prtcl PF : subG (gps_agreeΣ Prtcl PF) Σ → gps_agreeG Σ Prtcl.
+Instance subG_gps_agreeΣ Σ Prtcl : subG (gps_agreeΣ Prtcl) Σ → gps_agreeG Σ Prtcl.
 Proof. solve_inG. Qed.
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index 57997687..d26ccea8 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -32,11 +32,11 @@ Section Plain.
   Definition gpsPRaw p l n : iProp :=
     (∃ (γ γ_x γx: gname) (e_x: state_sort Prtcl) ζ,
       ⌜n = encode (p,γ,γ_x,γx)⌝ ∗ gps_inv IP l γ γ_x
-      ∗ Writer γ ζ ∗ exwr γ_x 1%Qp e_x ∗ own.own γx (DecAgree e_x))%I.
+      ∗ Writer γ ζ ∗ exwr γ_x 1%Qp e_x ∗ own.own γx (to_agree e_x))%I.
 
   Definition RPRaw p s V l n : iProp :=
     (∃ (γ γ_x γx: gname) e_x,
-      ⌜n = encode (p,γ,γ_x,γx)⌝ ∗ own.own γx (DecAgree e_x)
+      ⌜n = encode (p,γ,γ_x,γx)⌝ ∗ own.own γx (to_agree e_x)
       ∗ ∃ Vr v, ⌜Vr ⊑ V⌝
               ∗ ⌜st_view e_x !! l ⊑ (Vr !! l : option positive)⌝ ∗ Reader γ {[s, (v, Vr)]})%I.
 
@@ -63,7 +63,7 @@ Section Plain.
 
   Local Instance :
     Frame false (gps_inv IP l γ γ_x) (gpsPRaw p l (encode (p,γ,γ_x,γx)))
-          (Writer γ ζ ∗ exwr γ_x 1%Qp e_x ∗ own.own γx (DecAgree e_x)).
+          (Writer γ ζ ∗ exwr γ_x 1%Qp e_x ∗ own.own γx (to_agree e_x)).
   Proof.
     intros. rewrite /Frame. iIntros "[? ?]". iExists _, _.
     iFrame "∗". iExists _, _, _. cbn. by iFrame "∗".
@@ -118,7 +118,7 @@ Section Plain.
     iNext.
     iIntros (V' γ γ_x) "(% & kS' & oI & ex & #oR & oW)"; iFrame.
 
-    iMod (own.own_alloc (DecAgree (s, (v, V')))) as (γx) "#oEx"; first done.
+    iMod (own.own_alloc (to_agree ((s, (v, V')) : state_sort _))) as (γx) "#oEx"; first done.
 
     iMod (persistor_inv_alloc E i (encode (p,γ,γ_x,γx)) l
           (gpsPRaw p) (RPRaw p s V')
@@ -154,8 +154,8 @@ Section Plain.
     subst X. apply encode_inj in H0. inversion H0. subst γ' γ_x' γx'.
 
     iCombine "Hex" "Hex'" as "He".
-    iDestruct (own.own_valid with "He") as %He%dec_agree_op_inv.
-    inversion He. subst e_x'.
+    iDestruct (own.own_valid with "He") as %He%agree_op_inv%(inj to_agree).
+    setoid_subst.
 
     iDestruct "RA" as (V_r v_r) "(% & % & #oR)".
 
@@ -169,8 +169,8 @@ Section Plain.
       iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
       iMod ("HClose" $! (RPRaw p s' j0) with "[Writer oI oR' Ex]").
       { iSplit.
-        + iNext. iExists γ, γ_x, γx, e_x, ζ. iFrame; auto.
-        + iExists γ, γ_x, γx, e_x. iFrame "Hex". iSplitL ""; first auto.
+        + iNext. iExists γ, γ_x, γx, e_x', ζ. iFrame; auto.
+        + iExists γ, γ_x, γx, e_x'. iFrame "Hex". iSplitL ""; first auto.
           iExists Vr, v. iSplit; last iFrame "oR'"; iPureIntro; auto.
           do 4 (etrans; eauto). }
       iMod ("VS" $! _ j0 with "[%] [$]") as "$"; [solve_jsl|].
@@ -221,8 +221,8 @@ Section Plain.
     subst X. apply encode_inj in H0. inversion H0. subst γ' γ_x' γx'.
 
     iCombine "Hex" "Hex'" as "He".
-    iDestruct (own.own_valid with "He") as %He%dec_agree_op_inv.
-    inversion He. subst e_x'. destruct e_x as [s_x [v_x V_x]].
+    iDestruct (own.own_valid with "He") as %He%agree_op_inv%(inj to_agree). setoid_subst.
+    destruct e_x' as [s_x [v_x V_x]].
 
     iDestruct "RA" as (V_r v_r) "(% & % & #oR)".
 
@@ -274,8 +274,8 @@ Section Plain.
     subst X. apply encode_inj in H0. inversion H0. subst γ' γ_x' γx'.
 
     iCombine "Hex" "Hex'" as "He".
-    iDestruct (own.own_valid with "He") as %He%dec_agree_op_inv.
-    inversion He. subst e_x'. destruct e_x as [s_x [v_x V_x]].
+    iDestruct (own.own_valid with "He") as %He%agree_op_inv%(inj to_agree).
+    setoid_subst. destruct e_x' as [s_x [v_x V_x]].
 
     iDestruct "RA" as (V_r v_r) "(% & % & #oR)".
 
@@ -383,8 +383,8 @@ Section Plain.
     subst X. apply encode_inj in H0. inversion H0. subst γ' γ_x' γx'.
 
     iCombine "Hex" "Hex'" as "He".
-    iDestruct (own.own_valid with "He") as %He%dec_agree_op_inv.
-    inversion He. subst e_x'. destruct e_x as [s_x [v_x V_x]].
+    iDestruct (own.own_valid with "He") as %He%agree_op_inv%(inj to_agree). setoid_subst.
+    destruct e_x' as [s_x [v_x V_x]].
 
     iDestruct "RA" as (V_r v_r) "(% & % & #oR)".
 
diff --git a/theories/gps/shared.v b/theories/gps/shared.v
index e4db3acf..5618e16b 100644
--- a/theories/gps/shared.v
+++ b/theories/gps/shared.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export auth frac excl gmap gset local_updates.
+From iris.algebra Require Export auth frac excl gmap gset local_updates agree.
 From iris.program_logic Require Import ectx_lifting.
 From iris.bi Require Import big_op.
 From iris.proofmode Require Import tactics.
@@ -25,7 +25,7 @@ Arguments pr_steps _ _ _ : clear implicits.
 
 Notation interpC Σ Prtcl := (bool -c> loc -c> pr_state Prtcl -c> Z -c> vProp Σ).
 
-Notation state_sort Prtcl := (pr_state Prtcl * (Z * View))%type.
+Notation state_sort Prtcl := (leibnizC (pr_state Prtcl * (Z * View))%type).
 Notation state_type Prtcl := (gset (state_sort Prtcl)).
 
 Section STS.
@@ -55,9 +55,9 @@ Section STS.
     unfold proofmode_classes.IsOp. rewrite -auth_frag_op. done.
   Qed.
 
-  Definition st_prst : pr_state Prtcl * (Z * View) -> _ := fst.
-  Definition st_val : pr_state Prtcl * (Z * View) -> _ := fst ∘ snd.
-  Definition st_view : pr_state Prtcl * (Z * View) -> _ := snd ∘ snd.
+  Definition st_prst : state_sort Prtcl -> _ := fst.
+  Definition st_val : state_sort Prtcl -> _ := fst ∘ snd.
+  Definition st_view : state_sort Prtcl -> _ := snd ∘ snd.
   Definition st_time := λ x s, st_view s !! x.
 
 
@@ -78,10 +78,10 @@ End STS.
 Class gpsG Σ Prtcl (PF : protocol_facts Prtcl) :=
   {
     gps_inG :> inG Σ stateR;
-    gps_ExWrG :> inG Σ (authR (optionUR (prodR fracR (dec_agreeR (state_sort Prtcl)))))
+    gps_ExWrG :> inG Σ (authR (optionUR (prodR fracR (agreeR (state_sort Prtcl)))))
   }.
 Definition gpsΣ Prtcl (PF : protocol_facts Prtcl) : gFunctors :=
-  #[ GFunctor (constRF stateR); GFunctor (constRF (authR (optionUR (prodR fracR (dec_agreeR (state_sort Prtcl)))))) ].
+  #[ GFunctor (constRF stateR); GFunctor (constRF (authR (optionUR (prodR fracR (agreeR (state_sort Prtcl)))))) ].
 
 Instance subG_gpsG {Σ} Prtcl PF : subG (gpsΣ Prtcl PF) Σ → gpsG Σ Prtcl PF.
 Proof. solve_inG. Qed.
@@ -101,12 +101,12 @@ Section Setup.
   Set Default Proof Using "Type".
   Local Notation iProp := (iProp Σ).
   Local Notation vPred := (vProp Σ).
-  Notation state_sort := (pr_state Prtcl * (Z * View))%type.
+  Notation state_sort := (leibnizC (pr_state Prtcl * (Z * View)))%type.
   Implicit Types
            (s : pr_state Prtcl)
            (ζ : state_type Prtcl)
            (e : state_sort)
-           (S : pr_state Prtcl * (Z * View))
+           (S : state_sort)
            (v : Z)
            (V : View)
            (h : History).
@@ -157,7 +157,7 @@ Section Setup.
                               - by move => [? [-> ->]].
     Qed.
 
-    Definition exwr γ_x p e := own.own γ_x (◯ (Some (p, DecAgree e))).
+    Definition exwr γ_x p e := own.own γ_x (◯ (Some (p, to_agree e))).
 
     Definition final_st s := ∀ s', s' ⊑ s.
 
@@ -171,7 +171,7 @@ Section Setup.
 
     Definition gps_inv γ γ_x : iProp
       := (∃ ζ h e_x, own.own γ (● (● ζ ⋅ ◯ ζ))
-                         ∗ own.own γ_x (● (Some (1%Qp, DecAgree e_x)))
+                         ∗ own.own γ_x (● (Some (1%Qp, to_agree e_x)))
                          ∗ Hist l h ∗ ProtoInv ζ e_x
                          ∗ ⌜init l h⌝ ∗ ⌜SortInv l ζ⌝ ∗ ⌜e_x ∈ ζ⌝
                          ∗ ⌜Consistent ζ h⌝ ∗ ⌜FinalInv e_x ζ⌝ ∗ ⌜StateInjection ζ⌝)%I.
@@ -383,12 +383,12 @@ Section Setup.
       Qed.
 
       Lemma ExWrite_agree γ e1 e2 q1 q2:
-        own.own γ (● Some (q1, DecAgree e1)) ∗ exwr γ q2 e2 ⊢ ⌜e1 = e2⌝.
+        own.own γ (● Some (q1, to_agree e1)) ∗ exwr γ q2 e2 ⊢ ⌜e1 = e2⌝.
       Proof.
         rewrite -own.own_op. iIntros "oX".
         iDestruct (own.own_valid with "oX")
           as %[oXIn%Some_included oX]%auth_valid_discrete_2.
-          by move: oXIn => [[_ []]|/prod_included[_ /DecAgree_included]].
+        by move: oXIn => [[_ /to_agree_inj]|/prod_included[_ /to_agree_included]].
       Qed.
 
     End Agreement.
diff --git a/theories/gps/write.v b/theories/gps/write.v
index c9865a03..ad85cec5 100644
--- a/theories/gps/write.v
+++ b/theories/gps/write.v
@@ -5,7 +5,7 @@ From igps.base Require Import at_write.
 Section Write.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
   Set Default Proof Using "Type".
-  Notation state_sort := (pr_state Prtcl * (Z * View))%type.
+  Notation state_sort := (leibnizC (pr_state Prtcl * (Z * View))%type).
   Implicit Types
            (s : pr_state Prtcl)
            (ζ : state_type Prtcl)
@@ -203,8 +203,8 @@ Section Write.
 
       iCombine "oAX" "ofX" as "oA".
       iMod (own.own_update _ _
-                (● Some (1%Qp, DecAgree (s', (v, V')))
-                   â‹… â—¯ Some (1%Qp, DecAgree (s', (v, V'))))
+                (● Some (1%Qp, to_agree ((s', (v, V')) : state_sort))
+                   â‹… â—¯ Some (1%Qp, to_agree ((s', (v, V')) : state_sort)))
            with "[$oA]") as "[oAX' ofX']".
         { by apply auth_update, option_local_update, exclusive_local_update. }
 
diff --git a/theories/persistor.v b/theories/persistor.v
index 876c8653..267d23d0 100644
--- a/theories/persistor.v
+++ b/theories/persistor.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Import lib.invariants.
 From iris.bi Require Import big_op.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth frac excl gmap.
+From iris.algebra Require Import auth frac excl gmap agree.
 
 Import uPred.
 
@@ -13,7 +13,7 @@ Definition persistN : namespace := nroot .@ "persistor".
 Notation persist_invN := (persistN .@ "inv").
 Notation persist_locN := (persistN .@ "loc").
 
-Definition PerInfos := gmapUR loc (dec_agreeR InfoT).
+Definition PerInfos := gmapUR loc (agreeR InfoT).
 
 Class persistorG Σ :=
   PersistorG {
@@ -41,7 +41,7 @@ Section Persistor.
     (∃ (ρ: PerInfos), own γ (● ρ) ∗  [∗ map] l↦v ∈ ρ, Info l 1 v)%I.
 
   Definition persistor_ctx l X: iProp Σ :=
-    (inv persist_invN (persistor_inv PER) ∗ own PER (◯ {[l := DecAgree X]}))%I.
+    (inv persist_invN (persistor_inv PER) ∗ own PER (◯ {[l := to_agree X]}))%I.
 
   Global Instance persistor_ctx_persistent l X:
     Persistent (persistor_ctx l X).
@@ -91,10 +91,8 @@ Section Persistor.
         iDestruct "Per2" as (X2) "[Per2 [#Inv2 #[PerCtx2 PerOwn2]]]".
         iCombine "PerOwn1" "PerOwn2" as "PerOwn".
         iDestruct (own_valid with "PerOwn") as %Valid.
-        move: Valid.
-        rewrite op_singleton
-           => /singleton_valid /dec_agree_op_inv Valid.
-        inversion Valid. subst.
+        move: Valid. rewrite op_singleton => /singleton_valid /agree_op_inv Valid.
+        apply (inj to_agree) in Valid. setoid_subst.
         iExists X2. iFrame. iFrame "Inv2". by iSplit.
       - iIntros "Per".
         iDestruct "Per" as (X) "[[Int1 Int2] #Inv]".
@@ -113,8 +111,7 @@ Section Persistor.
       iCombine "oP1" "oP2" as "oP".
       iDestruct (own_valid with "oP") as %Valid.
       rewrite op_singleton in Valid.
-        apply singleton_valid, dec_agree_op_inv in Valid.
-      inversion Valid. subst.
+      apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
       iExists X2. iFrame "P1 P2 Inv1 oP1 PC1".
     Qed.
 
@@ -128,8 +125,7 @@ Section Persistor.
       iCombine "oP1" "oP2" as "oP".
       iDestruct (own_valid with "oP") as %Valid.
       rewrite op_singleton in Valid.
-        apply singleton_valid, dec_agree_op_inv in Valid.
-      inversion Valid. subst.
+      apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
       iExists X2. iFrame "P1 P2 Inv2 oP1 PC1".
     Qed.
 
@@ -143,8 +139,7 @@ Section Persistor.
       iCombine "oP1" "oP2" as "oP".
       iDestruct (own_valid with "oP") as %Valid.
       rewrite op_singleton in Valid.
-        apply singleton_valid, dec_agree_op_inv in Valid.
-      inversion Valid. subst.
+      apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
       iExists X2. iModIntro. iFrame "P1 P2 Inv1 oP1 PC1".
     Qed.
 
@@ -162,7 +157,7 @@ Section Persistor.
       intros Sub Sub2.
       iIntros "(#PSCtx & #Ctx & Info)".
       iInv persist_invN as (ρ) ">(HA & Hρ)" "HClose" .
-      iMod (PSInv_Info_update _ _ _ (DecAgree X) with "[$PSCtx $Info]") as "Info";
+      iMod (PSInv_Info_update _ _ _ (to_agree X) with "[$PSCtx $Info]") as "Info";
       [solve_ndisj|done|..].
 
       iAssert ⌜ρ !! l = None⌝%I with "[#]" as "%". {
@@ -172,7 +167,7 @@ Section Persistor.
         iExFalso. iApply Info_Exclusive. iSplitL "Info" => //. }
       iMod (own_update with "[$HA]") as "[HA FA]".
         { apply auth_update_alloc.
-          apply: (alloc_singleton_local_update _ _ (DecAgree X)) => //. }
+          apply: (alloc_singleton_local_update _ _ (to_agree X)) => //. }
 
       iMod ("HClose" with "[HA Hρ Info]").
         { iNext. iExists _.
diff --git a/theories/tests/message_passing.v b/theories/tests/message_passing.v
index cc854283..7f662672 100644
--- a/theories/tests/message_passing.v
+++ b/theories/tests/message_passing.v
@@ -6,7 +6,7 @@ Section MP.
 
 Let Σ : gFunctors := #[ baseΣ;
                         gpsΣ protocols.boolProtocol _ ;
-                        gps_agreeΣ protocols.boolProtocol _;
+                        gps_agreeΣ protocols.boolProtocol;
                         persistorΣ;
                         uTokΣ ].
 
@@ -29,8 +29,8 @@ Proof.
     last iMod (persistor_init with "PS") as (?) "#Pers".
     { by auto. }
     iModIntro.
-    iPoseProof (message_passing_spec (fun v => ⌜v = #37⌝)%I with "[$PS $Pers]") as "T".
-    iSpecialize ("T" with "[%]"); [by intros ? ->|].
+    iDestruct (message_passing_spec (λ v, ⌜v = #37⌝)%I with "[$PS $Pers] [%]")
+      as "T"; [by intros ? ->|].
     rewrite WP_Def.wp_eq /WP_Def.wp_def /=. iApply wp_mono; cycle 1.
     + by iApply "T".
     + by iIntros ([v ?]) "[_ %]".
-- 
GitLab