auth.v 9.67 KB
Newer Older
 Robbert Krebbers committed Feb 13, 2016 1 ``````From algebra Require Export excl. `````` Robbert Krebbers committed Feb 13, 2016 2 ``````From algebra Require Import functor upred. `````` Robbert Krebbers committed Nov 22, 2015 3 ``````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 Jan 19, 2016 6 ``````Add Printing Constructor auth. `````` Robbert Krebbers committed Nov 11, 2015 7 ``````Arguments Auth {_} _ _. `````` Robbert Krebbers committed Nov 20, 2015 8 ``````Arguments authoritative {_} _. `````` Robbert Krebbers committed Nov 11, 2015 9 ``````Arguments own {_} _. `````` Robbert Krebbers committed Feb 02, 2016 10 11 ``````Notation "◯ a" := (Auth ExclUnit a) (at level 20). Notation "● a" := (Auth (Excl a) ∅) (at level 20). `````` Robbert Krebbers committed Nov 11, 2015 12 `````` `````` Robbert Krebbers committed Nov 22, 2015 13 ``````(* COFE *) `````` Robbert Krebbers committed Jan 14, 2016 14 15 ``````Section cofe. Context {A : cofeT}. `````` Robbert Krebbers committed Feb 02, 2016 16 17 ``````Implicit Types a b : A. Implicit Types x y : auth A. `````` Robbert Krebbers committed Jan 14, 2016 18 19 `````` Instance auth_equiv : Equiv (auth A) := λ x y, `````` Robbert Krebbers committed Nov 20, 2015 20 `````` authoritative x ≡ authoritative y ∧ own x ≡ own y. `````` Robbert Krebbers committed Jan 14, 2016 21 ``````Instance auth_dist : Dist (auth A) := λ n x y, `````` Ralf Jung committed Feb 10, 2016 22 `````` authoritative x ≡{n}≡ authoritative y ∧ own x ≡{n}≡ own y. `````` Robbert Krebbers committed Nov 22, 2015 23 `````` `````` Robbert Krebbers committed Jan 14, 2016 24 ``````Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A). `````` Robbert Krebbers committed Nov 22, 2015 25 ``````Proof. by split. Qed. `````` Robbert Krebbers committed Feb 02, 2016 26 27 ``````Global Instance Auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@Auth A). Proof. by split. Qed. `````` Robbert Krebbers committed Jan 14, 2016 28 ``````Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A). `````` Robbert Krebbers committed Nov 22, 2015 29 ``````Proof. by destruct 1. Qed. `````` Robbert Krebbers committed Feb 02, 2016 30 31 ``````Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A). Proof. by destruct 1. Qed. `````` Robbert Krebbers committed Jan 14, 2016 32 ``````Global Instance own_ne : Proper (dist n ==> dist n) (@own A). `````` Robbert Krebbers committed Nov 22, 2015 33 ``````Proof. by destruct 1. Qed. `````` Robbert Krebbers committed Feb 02, 2016 34 35 ``````Global Instance own_proper : Proper ((≡) ==> (≡)) (@own A). Proof. by destruct 1. Qed. `````` Robbert Krebbers committed Nov 22, 2015 36 `````` `````` Robbert Krebbers committed Jan 14, 2016 37 ``````Instance auth_compl : Compl (auth A) := λ c, `````` Robbert Krebbers committed Nov 22, 2015 38 `````` Auth (compl (chain_map authoritative c)) (compl (chain_map own c)). `````` Robbert Krebbers committed Jan 14, 2016 39 ``````Definition auth_cofe_mixin : CofeMixin (auth A). `````` Robbert Krebbers committed Nov 22, 2015 40 41 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 42 `````` - intros x y; unfold dist, auth_dist, equiv, auth_equiv. `````` Robbert Krebbers committed Nov 22, 2015 43 `````` rewrite !equiv_dist; naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 44 `````` - intros n; split. `````` Robbert Krebbers committed Nov 22, 2015 45 46 47 `````` + by intros ?; split. + by intros ?? [??]; split; symmetry. + intros ??? [??] [??]; split; etransitivity; eauto. `````` Robbert Krebbers committed Feb 17, 2016 48 `````` - by intros ? [??] [??] [??]; split; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 49 50 `````` - intros n c; split. apply (conv_compl n (chain_map authoritative c)). apply (conv_compl n (chain_map own c)). `````` Robbert Krebbers committed Nov 22, 2015 51 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 52 ``````Canonical Structure authC := CofeT auth_cofe_mixin. `````` Robbert Krebbers committed Feb 12, 2016 53 54 ``````Global Instance auth_timeless (x : auth A) : Timeless (authoritative x) → Timeless (own x) → Timeless x. `````` Robbert Krebbers committed Jan 14, 2016 55 ``````Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed. `````` Robbert Krebbers committed Jan 16, 2016 56 ``````Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A). `````` Robbert Krebbers committed Feb 17, 2016 57 ``````Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed. `````` Robbert Krebbers committed Jan 14, 2016 58 59 60 ``````End cofe. Arguments authC : clear implicits. `````` Robbert Krebbers committed Nov 22, 2015 61 62 `````` (* CMRA *) `````` Robbert Krebbers committed Jan 14, 2016 63 64 ``````Section cmra. Context {A : cmraT}. `````` Robbert Krebbers committed Feb 02, 2016 65 66 ``````Implicit Types a b : A. Implicit Types x y : auth A. `````` Robbert Krebbers committed Jan 14, 2016 67 68 69 `````` Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅. Instance auth_validN : ValidN (auth A) := λ n x, `````` Robbert Krebbers committed Nov 22, 2015 70 `````` match authoritative x with `````` Robbert Krebbers committed Nov 23, 2015 71 `````` | Excl a => own x ≼{n} a ∧ ✓{n} a `````` Robbert Krebbers committed Feb 11, 2016 72 `````` | ExclUnit => ✓{n} own x `````` Robbert Krebbers committed Feb 10, 2016 73 `````` | ExclBot => False `````` Robbert Krebbers committed Nov 22, 2015 74 `````` end. `````` Robbert Krebbers committed Jan 14, 2016 75 76 ``````Global Arguments auth_validN _ !_ /. Instance auth_unit : Unit (auth A) := λ x, `````` Robbert Krebbers committed Nov 20, 2015 77 `````` Auth (unit (authoritative x)) (unit (own x)). `````` Robbert Krebbers committed Jan 14, 2016 78 ``````Instance auth_op : Op (auth A) := λ x y, `````` Robbert Krebbers committed Nov 20, 2015 79 `````` Auth (authoritative x ⋅ authoritative y) (own x ⋅ own y). `````` Robbert Krebbers committed Jan 14, 2016 80 ``````Instance auth_minus : Minus (auth A) := λ x y, `````` Robbert Krebbers committed Nov 20, 2015 81 `````` Auth (authoritative x ⩪ authoritative y) (own x ⩪ own y). `````` Robbert Krebbers committed Jan 14, 2016 82 ``````Lemma auth_included (x y : auth A) : `````` Robbert Krebbers committed Nov 20, 2015 83 84 85 86 87 `````` 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 Jan 14, 2016 88 ``````Lemma auth_includedN n (x y : auth A) : `````` Robbert Krebbers committed Nov 22, 2015 89 90 91 92 93 `````` 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. `````` Robbert Krebbers committed Feb 11, 2016 94 ``````Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} authoritative x. `````` Robbert Krebbers committed Nov 22, 2015 95 ``````Proof. by destruct x as [[]]. Qed. `````` Robbert Krebbers committed Feb 11, 2016 96 ``````Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} own x. `````` Robbert Krebbers committed Feb 01, 2016 97 ``````Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed. `````` Robbert Krebbers committed Jan 14, 2016 98 99 `````` Definition auth_cmra_mixin : CMRAMixin (auth A). `````` Robbert Krebbers committed Nov 11, 2015 100 101 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 102 103 104 `````` - 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 *; `````` Robbert Krebbers committed Feb 10, 2016 105 `````` destruct Hx; intros ?; cofe_subst; auto. `````` Robbert Krebbers committed Feb 17, 2016 106 `````` - by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy']; `````` Robbert Krebbers committed Jan 13, 2016 107 `````` split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'. `````` Robbert Krebbers committed Feb 17, 2016 108 109 110 111 112 113 `````` - 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_unit_l. - by split; simpl; rewrite ?cmra_unit_idemp. - intros n ??; rewrite! auth_includedN; intros [??]. `````` Robbert Krebbers committed Feb 01, 2016 114 `````` by split; simpl; apply cmra_unit_preservingN. `````` Robbert Krebbers committed Feb 17, 2016 115 `````` - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a). `````` Robbert Krebbers committed Feb 01, 2016 116 `````` { intros n a b1 b2 <-; apply cmra_includedN_l. } `````` Robbert Krebbers committed Nov 22, 2015 117 `````` intros n [[a1| |] b1] [[a2| |] b2]; `````` Robbert Krebbers committed Feb 01, 2016 118 `````` naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN. `````` Robbert Krebbers committed Feb 17, 2016 119 `````` - by intros n ??; rewrite auth_includedN; `````` Robbert Krebbers committed Nov 22, 2015 120 121 `````` intros [??]; split; simpl; apply cmra_op_minus. Qed. `````` Robbert Krebbers committed Jan 14, 2016 122 ``````Definition auth_cmra_extend_mixin : CMRAExtendMixin (auth A). `````` Robbert Krebbers committed Nov 22, 2015 123 124 125 ``````Proof. intros n x y1 y2 ? [??]; simpl in *. destruct (cmra_extend_op n (authoritative x) (authoritative y1) `````` Robbert Krebbers committed Feb 02, 2016 126 `````` (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN. `````` Robbert Krebbers committed Nov 22, 2015 127 `````` destruct (cmra_extend_op n (own x) (own y1) (own y2)) `````` Robbert Krebbers committed Feb 02, 2016 128 129 `````` as (b&?&?&?); auto using own_validN. by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)). `````` Robbert Krebbers committed Nov 22, 2015 130 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 131 132 ``````Canonical Structure authRA : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin. `````` Robbert Krebbers committed Feb 02, 2016 133 `````` `````` Robbert Krebbers committed Feb 13, 2016 134 135 136 137 138 139 140 141 142 143 144 145 ``````(** Internalized properties *) Lemma auth_equivI {M} (x y : auth A) : (x ≡ y)%I ≡ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M)%I. Proof. done. Qed. Lemma auth_validI {M} (x : auth A) : (✓ x)%I ≡ (match authoritative x with | Excl a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a | ExclUnit => ✓ own x | ExclBot => False end : uPred M)%I. Proof. by destruct x as [[]]. Qed. `````` Robbert Krebbers committed Feb 02, 2016 146 147 148 149 150 ``````(** The notations ◯ and ● only work for CMRAs with an empty element. So, in what follows, we assume we have an empty element. *) Context `{Empty A, !CMRAIdentity A}. Global Instance auth_cmra_identity : CMRAIdentity authRA. `````` Robbert Krebbers committed Nov 22, 2015 151 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2016 152 `````` split; simpl. `````` Robbert Krebbers committed Feb 17, 2016 153 154 155 `````` - by apply (@cmra_empty_valid A _). - by intros x; constructor; rewrite /= left_id. - apply _. `````` Robbert Krebbers committed Nov 22, 2015 156 ``````Qed. `````` Robbert Krebbers committed Feb 02, 2016 157 ``````Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b. `````` Robbert Krebbers committed Nov 22, 2015 158 ``````Proof. done. Qed. `````` Ralf Jung committed Feb 10, 2016 159 160 ``````Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b. Proof. by rewrite /op /auth_op /= left_id. Qed. `````` Robbert Krebbers committed Feb 02, 2016 161 162 `````` Lemma auth_update a a' b b' : `````` Ralf Jung committed Feb 11, 2016 163 `````` (∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) → `````` Ralf Jung committed Feb 03, 2016 164 `````` ● a ⋅ ◯ a' ~~> ● b ⋅ ◯ b'. `````` Robbert Krebbers committed Feb 02, 2016 165 ``````Proof. `````` Robbert Krebbers committed Feb 18, 2016 166 `````` move=> Hab n [[?| |] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *. `````` Robbert Krebbers committed Feb 09, 2016 167 `````` destruct (Hab n (bf1 ⋅ bf2)) as [Ha' ?]; auto. `````` Robbert Krebbers committed Feb 11, 2016 168 169 `````` { by rewrite Ha left_id assoc. } split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done]. `````` Robbert Krebbers committed Feb 02, 2016 170 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 171 `````` `````` Ralf Jung committed Feb 11, 2016 172 ``````Lemma auth_local_update L `{!LocalUpdate Lv L} a a' : `````` Robbert Krebbers committed Feb 11, 2016 173 `````` Lv a → ✓ L a' → `````` Ralf Jung committed Feb 11, 2016 174 `````` ● a' ⋅ ◯ a ~~> ● L a' ⋅ ◯ L a. `````` Robbert Krebbers committed Feb 02, 2016 175 ``````Proof. `````` Ralf Jung committed Feb 11, 2016 176 `````` intros. apply auth_update=>n af ? EQ; split; last done. `````` Ralf Jung committed Feb 11, 2016 177 `````` by rewrite EQ (local_updateN L) // -EQ. `````` Robbert Krebbers committed Feb 02, 2016 178 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 179 180 181 182 `````` Lemma auth_update_op_l a a' b : ✓ (b ⋅ a) → ● a ⋅ ◯ a' ~~> ● (b ⋅ a) ⋅ ◯ (b ⋅ a'). Proof. by intros; apply (auth_local_update _). Qed. `````` Robbert Krebbers committed Feb 02, 2016 183 ``````Lemma auth_update_op_r a a' b : `````` Ralf Jung committed Feb 03, 2016 184 `````` ✓ (a ⋅ b) → ● a ⋅ ◯ a' ~~> ● (a ⋅ b) ⋅ ◯ (a' ⋅ b). `````` Robbert Krebbers committed Feb 11, 2016 185 ``````Proof. rewrite -!(comm _ b); apply auth_update_op_l. Qed. `````` 186 `````` `````` Ralf Jung committed Feb 11, 2016 187 ``````(* This does not seem to follow from auth_local_update. `````` Ralf Jung committed Feb 11, 2016 188 `````` The trouble is that given ✓ (L a ⋅ a'), Lv a `````` Ralf Jung committed Feb 11, 2016 189 190 `````` we need ✓ (a ⋅ a'). I think this should hold for every local update, but adding an extra axiom to local updates just for this is silly. *) `````` Ralf Jung committed Feb 11, 2016 191 192 193 ``````Lemma auth_local_update_l L `{!LocalUpdate Lv L} a a' : Lv a → ✓ (L a ⋅ a') → ● (a ⋅ a') ⋅ ◯ a ~~> ● (L a ⋅ a') ⋅ ◯ L a. `````` Ralf Jung committed Feb 11, 2016 194 195 ``````Proof. intros. apply auth_update=>n af ? EQ; split; last done. `````` Ralf Jung committed Feb 11, 2016 196 `````` by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ. `````` Ralf Jung committed Feb 11, 2016 197 198 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 199 200 201 ``````End cmra. Arguments authRA : clear implicits. `````` Robbert Krebbers committed Nov 22, 2015 202 203 `````` (* Functor *) `````` Robbert Krebbers committed Feb 04, 2016 204 205 206 207 208 209 210 211 212 213 214 215 ``````Definition auth_map {A B} (f : A → B) (x : auth A) : auth B := Auth (excl_map f (authoritative x)) (f (own x)). Lemma auth_map_id {A} (x : auth A) : auth_map id x = x. Proof. by destruct x; rewrite /auth_map excl_map_id. Qed. Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) : auth_map (g ∘ f) x = auth_map g (auth_map f x). Proof. by destruct x; rewrite /auth_map excl_map_compose. Qed. Lemma auth_map_ext {A B : cofeT} (f g : A → B) x : (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x. Proof. constructor; simpl; auto using excl_map_ext. Qed. Instance auth_map_cmra_ne {A B : cofeT} n : Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B). `````` Robbert Krebbers committed Nov 22, 2015 216 ``````Proof. `````` Robbert Krebbers committed Feb 04, 2016 217 `````` intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf]. `````` Robbert Krebbers committed Nov 22, 2015 218 ``````Qed. `````` Robbert Krebbers committed Feb 04, 2016 219 220 221 ``````Instance auth_map_cmra_monotone {A B : cmraT} (f : A → B) : (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone f → CMRAMonotone (auth_map f). `````` Robbert Krebbers committed Nov 22, 2015 222 223 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 224 `````` - by intros n [x a] [y b]; rewrite !auth_includedN /=; `````` Robbert Krebbers committed Jan 14, 2016 225 `````` intros [??]; split; simpl; apply: includedN_preserving. `````` Robbert Krebbers committed Feb 17, 2016 226 `````` - intros n [[a| |] b]; rewrite /= /cmra_validN; `````` Robbert Krebbers committed Nov 22, 2015 227 228 `````` naive_solver eauto using @includedN_preserving, @validN_preserving. Qed. `````` Robbert Krebbers committed Feb 04, 2016 229 ``````Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B := `````` Robbert Krebbers committed Feb 04, 2016 230 `````` CofeMor (auth_map f). `````` Robbert Krebbers committed Feb 04, 2016 231 ``````Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B). `````` Robbert Krebbers committed Nov 22, 2015 232 ``````Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed. `````` Ralf Jung committed Feb 05, 2016 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 `````` Program Definition authF (Σ : iFunctor) : iFunctor := {| ifunctor_car := authRA ∘ Σ; ifunctor_map A B := authC_map ∘ ifunctor_map Σ |}. Next Obligation. by intros Σ A B n f g Hfg; apply authC_map_ne, ifunctor_map_ne. Qed. Next Obligation. intros Σ A x. rewrite /= -{2}(auth_map_id x). apply auth_map_ext=>y; apply ifunctor_map_id. Qed. Next Obligation. intros Σ A B C f g x. rewrite /= -auth_map_compose. apply auth_map_ext=>y; apply ifunctor_map_compose. Qed.``````