auth.v 6.2 KB
Newer Older
1
Require Export iris.excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3
Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

Robbert Krebbers's avatar
Robbert Krebbers committed
5
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Arguments Auth {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Arguments authoritative {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11
Arguments own {_} _.
Notation "∘ x" := (Auth ExclUnit x) (at level 20).
Notation "∙ x" := (Auth (Excl x) ) (at level 20).

Robbert Krebbers's avatar
Robbert Krebbers committed
12
(* COFE *)
Robbert Krebbers's avatar
Robbert Krebbers committed
13
Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  authoritative x  authoritative y  own x  own y.
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
Instance auth_dist `{Dist A} : Dist (auth A) := λ n x y,
  authoritative x ={n}= authoritative y  own x ={n}= own y.

Instance Auth_ne `{Dist A} : Proper (dist n ==> dist n ==> dist n) (@Auth A).
Proof. by split. Qed.
Instance authoritative_ne `{Dist A} :
  Proper (dist n ==> dist n) (@authoritative A).
Proof. by destruct 1. Qed.
Instance own_ne `{Dist A} : Proper (dist n ==> dist n) (@own A).
Proof. by destruct 1. Qed.

Instance auth_compl `{Cofe A} : Compl (auth A) := λ c,
  Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).

Local Instance auth_cofe `{Cofe A} : Cofe (auth A).
Proof.
  split.
  * intros x y; unfold dist, auth_dist, equiv, auth_equiv.
    rewrite !equiv_dist; naive_solver.
  * intros n; split.
    + by intros ?; split.
    + by intros ?? [??]; split; symmetry.
    + intros ??? [??] [??]; split; etransitivity; eauto.
  * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
  * by split.
  * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
    apply (conv_compl (chain_map own c) n).
Qed.

(* CMRA *)
Instance auth_empty `{Empty A} : Empty (auth A) := Auth  .
Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
  match authoritative x with
  | Excl a => own x  a  valid a
  | ExclUnit => valid (own x)
  | ExclBot => False
  end.
Arguments auth_valid _ _ _ _ !_ /.
Instance auth_validN `{Dist A, ValidN A, Op A} : ValidN (auth A) := λ n x,
  match authoritative x with
  | Excl a => own x {n} a  validN n a
  | ExclUnit => validN n (own x)
  | ExclBot => n = 0
  end.
Arguments auth_validN _ _ _ _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  Auth (unit (authoritative x)) (unit (own x)).
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Instance auth_op `{Op A} : Op (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  Auth (authoritative x  authoritative y) (own x  own y).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
65 66 67 68 69 70 71
  Auth (authoritative x  authoritative y) (own x  own y).
Lemma auth_included `{Equiv A, Op A} (x y : auth A) :
  x  y  authoritative x  authoritative y  own x  own 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74 75 76 77 78 79 80 81 82 83
Lemma auth_includedN `{Dist A, Op A} n (x y : auth A) :
  x {n} y  authoritative x {n} authoritative y  own x {n} own 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 `{CMRA A} n (x : auth A) :
  validN n x  validN n (authoritative x).
Proof. by destruct x as [[]]. Qed.
Lemma own_validN `{CMRA A} n (x : auth A) : validN n x  validN n (own x).
Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed.
Instance auth_cmra `{CMRA A} : CMRA (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87 88 89 90 91
  * apply _.
  * 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 *;
      destruct Hx as [[][]| | |]; intros ?; cofe_subst; auto.
  * by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
Robbert Krebbers's avatar
Robbert Krebbers committed
92
      split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'.
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95 96 97
  * by intros [[] ?]; simpl.
  * intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S.
  * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN,
      ?cmra_valid_validN; [naive_solver|naive_solver|].
    split; [done|intros Hn; discriminate (Hn 1)].
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100 101
  * by split; simpl; rewrite (associative _).
  * by split; simpl; rewrite (commutative _).
  * by split; simpl; rewrite ?(ra_unit_l _).
  * by split; simpl; rewrite ?(ra_unit_idempotent _).
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
  * intros n ??; rewrite! auth_includedN; intros [??].
    by split; simpl; apply cmra_unit_preserving.
  * assert ( n a b1 b2, b1  b2 {n} a  b1 {n} a).
    { intros n a b1 b2 <-; apply cmra_included_l. }
   intros n [[a1| |] b1] [[a2| |] b2];
     naive_solver eauto using cmra_valid_op_l, cmra_valid_includedN.
  * by intros n ??; rewrite auth_includedN;
      intros [??]; split; simpl; apply cmra_op_minus.
Qed.
Instance auth_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (auth A).
Proof.
  intros n x y1 y2 ? [??]; simpl in *.
  destruct (cmra_extend_op n (authoritative x) (authoritative y1)
    (authoritative y2)) as (z1&?&?&?); auto using authoritative_validN.
  destruct (cmra_extend_op n (own x) (own y1) (own y2))
    as (z2&?&?&?); auto using own_validN.
  by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)).
Qed.
Instance auth_ra_empty `{CMRA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
Proof.
  split; [apply (ra_empty_valid (A:=A))|].
  by intros x; constructor; simpl; rewrite (left_id _ _).
Qed.
Lemma auth_frag_op `{CMRA A} a b : (a  b)  a  b.
Proof. done. Qed.

(* Functor *)
Definition authRA (A : cmraT) : cmraT := CMRAT (auth A).
Instance auth_fmap : FMap auth := λ A B f x,
  Auth (f <$> authoritative x) (f (own x)).
Instance auth_fmap_cmra_ne `{Dist A, Dist B} n :
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
Proof.
  intros f g Hf [??] [??] [??]; split; [by apply excl_fmap_cmra_ne|by apply Hf].
Qed.
Instance auth_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A  B) :
  ( n, Proper (dist n ==> dist n) f)  CMRAMonotone f 
  CMRAMonotone (fmap f : auth A  auth B).
Proof.
  split.
  * by intros n [x a] [y b]; rewrite !auth_includedN; simpl;
      intros [??]; split; apply includedN_preserving.
  * intros n [[a| |] b];
      naive_solver eauto using @includedN_preserving, @validN_preserving.
Qed.
Definition authRA_map {A B : cmraT} (f : A -n> B) : authRA A -n> authRA B :=
  CofeMor (fmap f : authRA A  authRA B).
Lemma authRA_map_ne A B n : Proper (dist n ==> dist n) (@authRA_map A B).
Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.