auth.v 6.19 KB
 Robbert Krebbers committed Nov 16, 2015 1 ``````Require Export iris.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 42 43 44 45 46 47 ``````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 `````` Robbert Krebbers committed Nov 23, 2015 48 49 `````` | Excl a => own x ≼ a ∧ ✓ a | ExclUnit => ✓ (own x) `````` Robbert Krebbers committed Nov 22, 2015 50 51 52 53 54 `````` | 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 55 56 `````` | Excl a => own x ≼{n} a ∧ ✓{n} a | ExclUnit => ✓{n} (own x) `````` Robbert Krebbers committed Nov 22, 2015 57 58 59 `````` | ExclBot => n = 0 end. Arguments auth_validN _ _ _ _ _ !_ /. `````` Robbert Krebbers committed Nov 11, 2015 60 ``````Instance auth_unit `{Unit A} : Unit (auth A) := λ x, `````` Robbert Krebbers committed Nov 20, 2015 61 `````` Auth (unit (authoritative x)) (unit (own x)). `````` Robbert Krebbers committed Nov 11, 2015 62 ``````Instance auth_op `{Op A} : Op (auth A) := λ x y, `````` Robbert Krebbers committed Nov 20, 2015 63 `````` Auth (authoritative x ⋅ authoritative y) (own x ⋅ own y). `````` Robbert Krebbers committed Nov 11, 2015 64 ``````Instance auth_minus `{Minus A} : Minus (auth A) := λ x y, `````` Robbert Krebbers committed Nov 20, 2015 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 committed Nov 22, 2015 72 73 74 75 76 77 78 ``````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 79 `````` ✓{n} x → ✓{n} (authoritative x). `````` Robbert Krebbers committed Nov 22, 2015 80 ``````Proof. by destruct x as [[]]. Qed. `````` Robbert Krebbers committed Nov 23, 2015 81 ``````Lemma own_validN `{CMRA A} n (x : auth A) : ✓{n} x → ✓{n} (own x). `````` Robbert Krebbers committed Nov 22, 2015 82 83 ``````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 84 85 ``````Proof. split. `````` Robbert Krebbers committed Nov 22, 2015 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 committed Nov 11, 2015 92 `````` split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'. `````` Robbert Krebbers committed Nov 22, 2015 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 committed Nov 11, 2015 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 committed Nov 22, 2015 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 `````` * 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. `````` Robbert Krebbers committed Dec 11, 2015 125 ``````Lemma auth_frag_op `{CMRA A} a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b. `````` Robbert Krebbers committed Nov 22, 2015 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 ``````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.``````