auth.v 6.71 KB
 Robbert Krebbers committed Dec 15, 2015 1 ``````Require Export modures.excl. `````` Robbert Krebbers committed Nov 22, 2015 2 3 ``````Local Arguments valid _ _ !_ /. Local Arguments validN _ _ _ !_ /. `````` Robbert Krebbers committed Nov 11, 2015 4 `````` `````` Robbert Krebbers committed Nov 20, 2015 5 ``````Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }. `````` Robbert Krebbers committed Nov 11, 2015 6 ``````Arguments Auth {_} _ _. `````` Robbert Krebbers committed Nov 20, 2015 7 ``````Arguments authoritative {_} _. `````` Robbert Krebbers committed Nov 11, 2015 8 ``````Arguments own {_} _. `````` Robbert Krebbers committed Dec 11, 2015 9 10 ``````Notation "◯ x" := (Auth ExclUnit x) (at level 20). Notation "● x" := (Auth (Excl x) ∅) (at level 20). `````` Robbert Krebbers committed Nov 11, 2015 11 `````` `````` Robbert Krebbers committed Nov 22, 2015 12 ``````(* COFE *) `````` Robbert Krebbers committed Nov 11, 2015 13 ``````Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y, `````` Robbert Krebbers committed Nov 20, 2015 14 `````` authoritative x ≡ authoritative y ∧ own x ≡ own y. `````` Robbert Krebbers committed Nov 22, 2015 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 ``````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. `````` Robbert Krebbers committed Dec 11, 2015 42 43 44 ``````Instance Auth_timeless `{Dist A, Equiv A} (x : excl A) (y : A) : Timeless x → Timeless y → Timeless (Auth x y). Proof. by intros ?? [??] [??]; split; apply (timeless _). Qed. `````` Robbert Krebbers committed Nov 22, 2015 45 46 47 48 49 `````` (* 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 `````` Robbert Krebbers committed Nov 23, 2015 50 51 `````` | Excl a => own x ≼ a ∧ ✓ a | ExclUnit => ✓ (own x) `````` Robbert Krebbers committed Nov 22, 2015 52 53 54 55 56 `````` | ExclBot => False end. Arguments auth_valid _ _ _ _ !_ /. Instance auth_validN `{Dist A, ValidN A, Op A} : ValidN (auth A) := λ n x, match authoritative x with `````` Robbert Krebbers committed Nov 23, 2015 57 58 `````` | Excl a => own x ≼{n} a ∧ ✓{n} a | ExclUnit => ✓{n} (own x) `````` Robbert Krebbers committed Nov 22, 2015 59 60 61 `````` | ExclBot => n = 0 end. Arguments auth_validN _ _ _ _ _ !_ /. `````` Robbert Krebbers committed Nov 11, 2015 62 ``````Instance auth_unit `{Unit A} : Unit (auth A) := λ x, `````` Robbert Krebbers committed Nov 20, 2015 63 `````` Auth (unit (authoritative x)) (unit (own x)). `````` Robbert Krebbers committed Nov 11, 2015 64 ``````Instance auth_op `{Op A} : Op (auth A) := λ x y, `````` Robbert Krebbers committed Nov 20, 2015 65 `````` Auth (authoritative x ⋅ authoritative y) (own x ⋅ own y). `````` Robbert Krebbers committed Nov 11, 2015 66 ``````Instance auth_minus `{Minus A} : Minus (auth A) := λ x y, `````` Robbert Krebbers committed Nov 20, 2015 67 68 69 70 71 72 73 `````` 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 committed Nov 22, 2015 74 75 76 77 78 79 80 ``````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) : `````` Robbert Krebbers committed Nov 23, 2015 81 `````` ✓{n} x → ✓{n} (authoritative x). `````` Robbert Krebbers committed Nov 22, 2015 82 ``````Proof. by destruct x as [[]]. Qed. `````` Robbert Krebbers committed Nov 23, 2015 83 ``````Lemma own_validN `{CMRA A} n (x : auth A) : ✓{n} x → ✓{n} (own x). `````` Robbert Krebbers committed Nov 22, 2015 84 85 ``````Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed. Instance auth_cmra `{CMRA A} : CMRA (auth A). `````` Robbert Krebbers committed Nov 11, 2015 86 87 ``````Proof. split. `````` Robbert Krebbers committed Nov 22, 2015 88 `````` * apply _. `````` Robbert Krebbers committed Jan 13, 2016 89 90 `````` * 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'. `````` Robbert Krebbers committed Nov 22, 2015 91 92 93 `````` * 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 committed Jan 13, 2016 94 `````` split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'. `````` Robbert Krebbers committed Nov 22, 2015 95 96 `````` * by intros [[] ?]; simpl. * intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S. `````` Robbert Krebbers committed Jan 13, 2016 97 `````` * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN `````` Robbert Krebbers committed Nov 22, 2015 98 99 `````` ?cmra_valid_validN; [naive_solver|naive_solver|]. split; [done|intros Hn; discriminate (Hn 1)]. `````` Robbert Krebbers committed Nov 11, 2015 100 101 102 103 `````` * 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 committed Nov 22, 2015 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 `````` * 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. `````` Robbert Krebbers committed Dec 15, 2015 122 ``````Instance auth_ra_empty `{CMRA A, Empty A, !RAIdentity A} : RAIdentity (auth A). `````` Robbert Krebbers committed Nov 22, 2015 123 124 125 126 ``````Proof. split; [apply (ra_empty_valid (A:=A))|]. by intros x; constructor; simpl; rewrite (left_id _ _). Qed. `````` Robbert Krebbers committed Dec 11, 2015 127 128 129 ``````Instance auth_frag_valid_timeless `{CMRA A} (x : A) : ValidTimeless x → ValidTimeless (◯ x). Proof. by intros ??; apply (valid_timeless x). Qed. `````` Robbert Krebbers committed Dec 15, 2015 130 ``````Instance auth_valid_timeless `{CMRA A, Empty A, !RAIdentity A} (x : A) : `````` Robbert Krebbers committed Dec 11, 2015 131 132 133 134 `````` ValidTimeless x → ValidTimeless (● x). Proof. by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)]. Qed. `````` Robbert Krebbers committed Dec 11, 2015 135 ``````Lemma auth_frag_op `{CMRA A} a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b. `````` Robbert Krebbers committed Nov 22, 2015 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 ``````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.``````