WIP: this is not nice. we should have a sigma-type-based auth instead.

algebra/agree.v

@@ -354,9 +354,15 @@ Proof.
   intros a b ?. apply equiv_dist=>n. apply to_agree_injN. by apply equiv_dist.
 Qed.
 
-Lemma to_agree_uninj n (x : agree A) : ✓{n} x → ∃ y : A, to_agree y ≡{n}≡ x.
+Lemma agree_car_ne n (x y : agree A) :
+  ✓{n} x → x ≡{n}≡ y → agree_car x ≡{n}≡ agree_car y.
 Proof.
-  intros Hl. exists (agree_car x). rewrite /dist /agree_dist /=.
+  move=> /list_agrees_alt Hl [_ Hyx]. destruct (Hyx (agree_car y)) as (x' & ? & ->); first by set_solver+.
+  apply Hl; set_solver.
+Qed.
+Lemma agree_car_uninj n (x : agree A) : ✓{n} x → to_agree (agree_car x) ≡{n}≡ x.
+Proof.
+  intros Hl. rewrite /dist /agree_dist /=.
   split.
   - apply: list_setincl_singleton_in. set_solver+.
   - apply (list_agrees_iff_setincl _); first set_solver+. done.

algebra/auth.v

-From iris.algebra Require Export excl local_updates.
+From iris.algebra Require Export frac agree local_updates.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import class_instances.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
-Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
+Record auth (A : Type) :=
+  Auth { authoritative : option (prod frac (agree A)); auth_frag : A }.
 Add Printing Constructor auth.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
-Arguments auth_own {_} _.
+Arguments auth_frag {_} _.
 Notation "◯ a" := (Auth None a) (at level 20).
-Notation "● a" := (Auth (Excl' a) ∅) (at level 20).
+Notation "● a" := (Auth (Some $ (1%Qp, to_agree a)) ∅) (at level 20).
+Notation "'●{' q '}' a" := (Auth (Some $ (q%Qp, to_agree a)) ∅) (at level 20).
 
 (* COFE *)
 Section cofe.
 Context {A : ofeT}.
-Implicit Types a : excl' A.
+Implicit Types a : option (prod 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.
+  authoritative x ≡ authoritative y ∧ auth_frag x ≡ auth_frag y.
 Instance auth_dist : Dist (auth A) := λ n x y,
-  authoritative x ≡{n}≡ authoritative y ∧ auth_own x ≡{n}≡ auth_own y.
+  authoritative x ≡{n}≡ authoritative y ∧ auth_frag x ≡{n}≡ auth_frag y.
 
 Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
 Proof. by split. Qed.
@@ -32,9 +34,9 @@ Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
 Proof. by destruct 1. Qed.
 Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A).
 Proof. by destruct 1. Qed.
-Global Instance own_ne : Proper (dist n ==> dist n) (@auth_own A).
+Global Instance own_ne : Proper (dist n ==> dist n) (@auth_frag A).
 Proof. by destruct 1. Qed.
-Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
+Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_frag A).
 Proof. by destruct 1. Qed.
 
 Definition auth_ofe_mixin : OfeMixin (auth A).
@@ -50,22 +52,11 @@ Proof.
 Qed.
 Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
 
-Definition auth_compl `{Cofe A} : Compl authC := λ c,
-  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_own c)).
-Global Program Instance auth_cofe `{Cofe A} : Cofe authC :=
-  {| compl := auth_compl |}.
-Next Obligation.
-  intros ? n c; split. apply (conv_compl n (chain_map authoritative c)).
-  apply (conv_compl n (chain_map auth_own c)).
-Qed.
-
 Global Instance Auth_timeless a b :
   Timeless a → Timeless b → Timeless (Auth a b).
 Proof. by intros ?? [??] [??]; split; apply: timeless. Qed.
 Global Instance auth_discrete : Discrete A → Discrete 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.
@@ -78,51 +69,54 @@ Implicit Types x y : auth A.
 
 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
+  | Some (q, a) => (∀ n, auth_frag x ≼{n} agree_car a) ∧ ✓ q ∧ ✓ (agree_car a) ∧ ✓ a
+  | None => ✓ auth_frag 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
+  | Some (q, a) => auth_frag x ≼{n} agree_car a ∧ ✓{n} q ∧ ✓{n} (agree_car a) ∧ ✓{n} a
+  | None => ✓{n} auth_frag x
   end.
 Global Arguments auth_validN _ !_ /.
 Instance auth_pcore : PCore (auth A) := λ x,
-  Some (Auth (core (authoritative x)) (core (auth_own x))).
+  Some (Auth None (core (auth_frag x))).
 Instance auth_op : Op (auth A) := λ x y,
-  Auth (authoritative x ⋅ authoritative y) (auth_own x ⋅ auth_own y).
+  Auth (authoritative x ⋅ authoritative y) (auth_frag x ⋅ auth_frag y).
 
 Lemma auth_included (x y : auth A) :
-  x ≼ y ↔ authoritative x ≼ authoritative y ∧ auth_own x ≼ auth_own y.
+  x ≼ y ↔ authoritative x ≼ authoritative y ∧ auth_frag x ≼ auth_frag 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.
-Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
+Proof. destruct x as [[[? ?]|]]; try done. by intros [? [? [? ?]]]. Qed.
+Lemma auth_own_validN n x : ✓{n} x → ✓{n} auth_frag x.
+Proof. destruct x as [[[? ?]|]]; last done. naive_solver eauto using cmra_validN_includedN. 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
+        | Some (q, a) => auth_frag x ≼ agree_car a ∧ ✓ q ∧ ✓ (agree_car a) ∧ ✓ a
+        | None => ✓ auth_frag x
         end.
 Proof.
-  destruct x as [[[?|]|] ?]; simpl; try done.
+  destruct x as [[[? [? ?]]|] ?]; simpl; try done.
   setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
 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 auth_valid_discrete_2 `{CMRADiscrete A} q a b :
+  ✓ (●{q} a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ q ∧ ✓ a.
+Proof. rewrite auth_valid_discrete /= left_id.
+       (* FIXME RJ: This is ridicolous. *)
+       change (b ≼ a ∧ ✓ q ∧ ✓ a ∧ True ↔ b ≼ a ∧ ✓ q ∧ ✓ a). tauto. Qed.
+Lemma auth_valid_discrete_2' `{CMRADiscrete A} a b :
+  ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
+Proof. rewrite auth_valid_discrete_2. assert (✓ 1%Qp) by done. tauto. 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.
+Proof. destruct x as [[[? ?]|]]; try done. by intros [? [? [? ?]]]. Qed.
+Lemma auth_own_valid `{CMRADiscrete A} x : ✓ x → ✓ auth_frag x.
 Proof.
   rewrite auth_valid_discrete.
   destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
@@ -132,16 +126,20 @@ Lemma auth_cmra_mixin : CMRAMixin (auth A).
 Proof.
   apply cmra_total_mixin.
   - eauto.
-  - 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 y1 y2 [Hy Hy']; split; simpl; apply: cmra_op_ne; done.
+    (* FIXME: Both rewrite Hy and f_equiv fail in the first branch.  Why can they not find the instance? *)
+  - intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy'; done.
   - intros n [x a] [y b] [Hx Ha]; simpl in *.
-    destruct Hx as [?? Hx|]; first destruct Hx; intros ?; cofe_subst; auto.
-  - intros [[[?|]|] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
+    destruct Hx as [[? aa] [? bb] [Hx1 Hx2]|]; last by cofe_subst.
+    intros ?. destruct_and!.
+    assert (agree_car aa ≡{n}≡ agree_car bb) as <- by exact: agree_car_ne.
+    cofe_subst. auto.
+  - intros [[[? ?]|] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
       naive_solver eauto using O.
   - intros n [[[]|] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
   - by split; simpl; rewrite assoc.
   - by split; simpl; rewrite comm.
-  - by split; simpl; rewrite ?cmra_core_l.
+  - by split; simpl; rewrite ?cmra_core_l ?left_id.
   - by split; simpl; rewrite ?cmra_core_idemp.
   - intros ??; rewrite! auth_included; intros [??].
     by split; simpl; apply cmra_core_mono.