cmra.v 9.98 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
From iris.algebra Require Export local_updates.
Hai Dang's avatar
Hai Dang committed
2 3
From iris.algebra Require Export cmra gmap gset csum agree excl.

Hai Dang's avatar
Hai Dang committed
4 5 6
From stbor.lang Require Export lang.

Set Default Proof Using "Type".
Hai Dang's avatar
Hai Dang committed
7 8 9

Inductive tag_kind := tkUnique | tkPub.
(* Ex() + Ag() *)
Hai Dang's avatar
Hai Dang committed
10
Definition tagKindR := csumR (exclR unitO) (agreeR unitO).
Hai Dang's avatar
Hai Dang committed
11

Hai Dang's avatar
Hai Dang committed
12 13 14 15
Definition to_tagKindR (tk: tag_kind) : tagKindR :=
  match tk with tkUnique => Cinl (Excl ()) | tkPub => Cinr (to_agree ()) end.

Inductive call_state := csOwned (T: gset ptr_id) | csPub.
Hai Dang's avatar
Hai Dang committed
16
(* Ex(ptr_id) + Ag() *)
Hai Dang's avatar
Hai Dang committed
17
Definition callStateR := csumR (exclR (gsetO ptr_id)) (agreeR unitO).
Hai Dang's avatar
Hai Dang committed
18

Hai Dang's avatar
Hai Dang committed
19
Definition to_callStateR (cs: call_state) : callStateR :=
Hai Dang's avatar
Hai Dang committed
20
  match cs with csOwned T => Cinl (Excl T) | csPub => Cinr (to_agree ()) end.
Hai Dang's avatar
Hai Dang committed
21 22 23 24

Definition cmap := gmap call_id call_state.
(* call_id  CallState *)
Definition cmapUR := gmapUR call_id callStateR.
Hai Dang's avatar
Hai Dang committed
25

Hai Dang's avatar
Hai Dang committed
26 27
Definition to_cmapUR (cm: cmap) : cmapUR := fmap to_callStateR cm.

Hai Dang's avatar
Hai Dang committed
28
Definition tmap := gmap ptr_id (tag_kind * mem).
Hai Dang's avatar
Hai Dang committed
29
Definition heapletR := gmapR loc (agreeR scalarC).
Hai Dang's avatar
Hai Dang committed
30
(* ptr_id  TagKid x (loc  Ag(Scalar)) *)
Hai Dang's avatar
Hai Dang committed
31
Definition tmapUR := gmapUR ptr_id (prodR tagKindR heapletR).
Hai Dang's avatar
Hai Dang committed
32

Hai Dang's avatar
Hai Dang committed
33
Definition to_heapletR (h: mem) : heapletR := fmap to_agree h.
Hai Dang's avatar
Hai Dang committed
34
Definition to_tmapUR (pm: tmap) : tmapUR :=
Hai Dang's avatar
Hai Dang committed
35
  fmap (λ tm, (to_tagKindR tm.1, to_heapletR tm.2)) pm.
Hai Dang's avatar
Hai Dang committed
36

Hai Dang's avatar
Hai Dang committed
37
Definition lmap := gmap loc (scalar * stack).
Hai Dang's avatar
Hai Dang committed
38
Definition lmapUR := gmapUR loc (csumR (exclR (leibnizO (scalar * stack))) (agreeR unitO)).
Hai Dang's avatar
Hai Dang committed
39

Hai Dang's avatar
Hai Dang committed
40 41
Definition res := (tmap * cmap * lmap)%type.
Definition resUR := prodUR (prodUR tmapUR cmapUR) lmapUR.
Hai Dang's avatar
Hai Dang committed
42

Hai Dang's avatar
Hai Dang committed
43 44 45
Definition rtm (r: resUR) : tmapUR := r.1.1.
Definition rcm (r: resUR) : cmapUR := r.1.2.
Definition rlm (r: resUR) : lmapUR := r.2.
Hai Dang's avatar
Hai Dang committed
46 47 48 49 50 51 52 53

Lemma local_update_discrete_valid_frame `{CmraDiscrete A} (r_f r r' : A) :
   (r_f  r)  (r_f  r, r) ~l~> (r_f  r', r')   (r_f  r').
Proof.
  intros VALID UPD. apply cmra_discrete_valid.
  apply (UPD O (Some r_f)); [by apply cmra_discrete_valid_iff|by rewrite /= comm].
Qed.

Hai Dang's avatar
Hai Dang committed
54
(** tag_kind properties *)
Hai Dang's avatar
Hai Dang committed
55 56 57 58 59 60 61 62 63
Lemma tag_kind_incl_eq (k1 k2: tagKindR):
   k2  k1  k2  k1  k2.
Proof.
  move => VAL /csum_included [? |[[? [? [? [? Eq]]]]|[? [? [? [? LE]]]]]];
    subst; [done|..].
  - exfalso. eapply exclusive_included; [..|apply Eq|apply VAL]. apply _.
  - apply Cinr_equiv, agree_op_inv. apply agree_included in LE.
    rewrite -LE. apply VAL.
Qed.
Hai Dang's avatar
Hai Dang committed
64

Hai Dang's avatar
Hai Dang committed
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
Lemma tagKindR_exclusive (h0 h: heapletR) mb :
  mb  Some (to_tagKindR tkUnique, h0)  Some (to_tagKindR tkPub, h)  False.
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
    intros [Eq _]%Some_equiv_inj.
  - destruct k as [[]| |]; inversion Eq.
  - inversion Eq.
Qed.

Lemma tagKindR_exclusive_2 (h0 h: heapletR) mb :
  mb  Some (to_tagKindR tkPub, h0)  Some (to_tagKindR tkUnique, h)  False.
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
    intros [Eq _]%Some_equiv_inj.
  - destruct k as [[]| |]; inversion Eq.
  - inversion Eq.
Qed.

Lemma tagKindR_exclusive_heaplet (h0 h: heapletR) mb :
  mb  Some (to_tagKindR tkUnique, h0)  Some (to_tagKindR tkUnique, h)  h0  h.
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
    intros [Eq1 Eq2]%Some_equiv_inj; [|done].
  destruct k as [[[]|]| |]; inversion Eq1; simplify_eq.
Qed.

Hai Dang's avatar
Hai Dang committed
91 92 93 94 95 96 97 98
Lemma tagKindR_valid (k: tagKindR) :
  valid k   k', k  to_tagKindR k'.
Proof.
  destruct k as [[[]|]|a |]; [|done|..|done]; intros VAL.
  - by exists tkUnique.
  - exists tkPub. by apply to_agree_uninj in VAL as [[] <-].
Qed.

Hai Dang's avatar
Hai Dang committed
99
(** cmap properties *)
Hai Dang's avatar
Hai Dang committed
100
Lemma cmap_lookup_op_r (cm1 cm2: cmapUR) c T (VALID:  (cm1  cm2)):
Hai Dang's avatar
Hai Dang committed
101 102
  cm2 !! c = Some (to_callStateR (csOwned T)) 
  (cm1  cm2) !! c = Some (to_callStateR (csOwned T)).
Hai Dang's avatar
Hai Dang committed
103 104 105 106 107 108 109
Proof.
  intros HL. move : (VALID c). rewrite lookup_op HL.
  destruct (cm1 !! c) as [cs'|] eqn:Eqc; rewrite Eqc; [|done].
  rewrite -Some_op Some_valid.
  destruct cs' as [[]|c2|]; auto; try inversion 1.
Qed.

Hai Dang's avatar
Hai Dang committed
110
Lemma cmap_lookup_op_l (cm1 cm2: cmapUR) c T (VALID:  (cm1  cm2)):
Hai Dang's avatar
Hai Dang committed
111 112
  cm1 !! c = Some (to_callStateR (csOwned T)) 
  (cm1  cm2) !! c = Some (to_callStateR (csOwned T)).
Hai Dang's avatar
Hai Dang committed
113 114 115 116 117 118 119 120
Proof.
  intros HL. move : (VALID c). rewrite lookup_op HL.
  destruct (cm2 !! c) as [cs'|] eqn:Eqc; rewrite Eqc; [|done].
  rewrite -Some_op Some_valid.
  destruct cs' as [[]|c2|]; auto; try inversion 1.
Qed.

Lemma cmap_lookup_op_l_equiv (cm1 cm2: cmapUR) c T (VALID:  (cm1  cm2)):
Hai Dang's avatar
Hai Dang committed
121 122
  cm1 !! c  Some (to_callStateR (csOwned T)) 
  (cm1  cm2) !! c  Some (to_callStateR (csOwned T)).
Hai Dang's avatar
Hai Dang committed
123 124 125 126 127 128 129
Proof.
  intros HL. move : (VALID c). rewrite lookup_op HL.
  destruct (cm2 !! c) as [cs'|] eqn:Eqc; rewrite Eqc; [|done].
  rewrite -Some_op Some_valid.
  destruct cs' as [[]|c2|]; auto; try inversion 1.
Qed.

Hai Dang's avatar
Hai Dang committed
130 131 132 133 134 135 136 137 138
Lemma cmap_lookup_op_unique_included (cm1 cm2: cmapUR)
  c T (VALID:  cm2) (INCL: cm1  cm2):
  cm1 !! c  Some (to_callStateR (csOwned T)) 
  cm2 !! c  Some (to_callStateR (csOwned T)).
Proof.
  destruct INCL as [cm' Eq]. rewrite Eq. apply cmap_lookup_op_l_equiv.
  by rewrite -Eq.
Qed.

Hai Dang's avatar
Hai Dang committed
139 140 141 142 143 144 145 146 147 148 149
Lemma cmap_lookup_op_l_equiv_pub (cm1 cm2: cmapUR) c (VALID:  (cm1  cm2)):
  cm1 !! c  Some (to_callStateR csPub) 
  (cm1  cm2) !! c  Some (to_callStateR csPub).
Proof.
  intros HL. move : (VALID c). rewrite lookup_op HL.
  destruct (cm2 !! c) as [cs'|] eqn:Eqc; rewrite Eqc; [|done].
  rewrite -Some_op Some_valid.
  destruct cs' as [[]|c2|]; auto; try inversion 1.
  rewrite /= Cinr_op. intros Eq2%agree_op_inv. by rewrite -Eq2 agree_idemp.
Qed.

Hai Dang's avatar
Hai Dang committed
150
Lemma cmap_insert_op_r (cm1 cm2: cmapUR) c T cs (VALID:  (cm1  cm2)):
Hai Dang's avatar
Hai Dang committed
151
  cm2 !! c = Some (to_callStateR (csOwned T)) 
Hai Dang's avatar
Hai Dang committed
152 153 154 155 156 157 158 159 160 161
  cm1  <[c:=cs]> cm2 = <[c:=cs]> (cm1  cm2).
Proof.
  intros HL. apply (map_eq (cm1  <[c:=cs]> cm2)). intros c'.
  move : (VALID c). rewrite 2!lookup_op HL.
  destruct (cm1 !! c) as [[| |]|] eqn:Eqc; rewrite Eqc; [inversion 1..|].
  intros VL.
  case (decide (c' = c)) => [->|?].
  - by rewrite 2!lookup_insert Eqc.
  - do 2 (rewrite lookup_insert_ne //). by rewrite lookup_op.
Qed.
Hai Dang's avatar
Hai Dang committed
162

Hai Dang's avatar
Hai Dang committed
163 164 165 166 167 168 169 170 171
Lemma callStateR_exclusive_2 T mb :
  mb  Some (to_callStateR csPub)  Some (to_callStateR (csOwned T))  False.
Proof.
  destruct mb as [cs|]; [rewrite -Some_op|rewrite left_id];
    intros Eq%Some_equiv_inj.
  - destruct cs; inversion Eq.
  - inversion Eq.
Qed.

Hai Dang's avatar
Hai Dang committed
172 173
(** tmap properties *)
Lemma tmap_insert_op_r (pm1 pm2: tmapUR) t h0 kh (VALID:  (pm1  pm2)):
Hai Dang's avatar
Hai Dang committed
174 175 176 177 178 179 180 181 182 183 184 185 186
  pm2 !! t = Some (to_tagKindR tkUnique, h0) 
  pm1  <[t:=kh]> pm2 = <[t:=kh]> (pm1  pm2).
Proof.
  intros HL. apply (map_eq (pm1  <[t:=kh]> pm2)). intros t'.
  move : (VALID t). rewrite 2!lookup_op HL.
  destruct (pm1 !! t) as [[k1 h1]|] eqn:Eqt; rewrite Eqt.
  - rewrite -Some_op pair_op. intros [?%exclusive_r]; [done|apply _].
  - intros VL.
    case (decide (t' = t)) => [->|?].
    + by rewrite 2!lookup_insert Eqt.
    + do 2 (rewrite lookup_insert_ne //). by rewrite lookup_op.
Qed.

Hai Dang's avatar
Hai Dang committed
187
Lemma tmap_lookup_op_r (pm1 pm2: tmapUR) t h0 (VALID:  (pm1  pm2)):
Hai Dang's avatar
Hai Dang committed
188 189 190 191 192 193 194
  pm2 !! t = Some (to_tagKindR tkUnique, h0) 
  (pm1  pm2) !! t = Some (to_tagKindR tkUnique, h0).
Proof.
  intros HL. move : (VALID t). rewrite lookup_op HL.
  destruct (pm1 !! t) as [[k1 h1]|] eqn:Eqt; rewrite Eqt; [|done].
  rewrite -Some_op pair_op. intros [?%exclusive_r]; [done|apply _].
Qed.
Hai Dang's avatar
Hai Dang committed
195

Hai Dang's avatar
Hai Dang committed
196
Lemma tmap_lookup_op_l_unique_equiv (pm1 pm2: tmapUR) t h0
Hai Dang's avatar
Hai Dang committed
197 198 199 200 201 202 203 204 205
  (VALID:  (pm1  pm2)):
  pm1 !! t  Some (to_tagKindR tkUnique, h0) 
  (pm1  pm2) !! t  Some (to_tagKindR tkUnique, h0).
Proof.
  intros HL. move : (VALID t). rewrite lookup_op HL.
  destruct (pm2 !! t) as [[k2 h2]|] eqn:Eqt; rewrite Eqt; [|done].
  rewrite -Some_op pair_op. intros [?%exclusive_l]; [done|apply _].
Qed.

Hai Dang's avatar
Hai Dang committed
206
Lemma tmap_lookup_op_unique_included (pm1 pm2: tmapUR) t h0
Hai Dang's avatar
Hai Dang committed
207 208 209 210
  (VALID:  pm2) (INCL: pm1  pm2):
  pm1 !! t  Some (to_tagKindR tkUnique, h0) 
  pm2 !! t  Some (to_tagKindR tkUnique, h0).
Proof.
Hai Dang's avatar
Hai Dang committed
211
  destruct INCL as [cm' Eq]. rewrite Eq. apply tmap_lookup_op_l_unique_equiv.
Hai Dang's avatar
Hai Dang committed
212 213 214
  by rewrite -Eq.
Qed.

Hai Dang's avatar
Hai Dang committed
215
Lemma tmap_lookup_op_r_equiv_pub (pm1 pm2: tmapUR) t h2 (VALID:  (pm1  pm2)):
Hai Dang's avatar
Hai Dang committed
216 217 218 219 220 221 222 223 224 225 226
  pm2 !! t  Some (to_tagKindR tkPub, h2) 
   h1, (pm1  pm2) !! t  Some (to_tagKindR tkPub, h1  h2).
Proof.
  intros HL. move : (VALID t). rewrite lookup_op.
  destruct (pm1 !! t) as [[k1 h1]|] eqn:Eqt; rewrite Eqt; rewrite -> HL.
  - rewrite -Some_op pair_op. move => [ VL1 ?]. exists h1. simpl in VL1.
    rewrite HL -Some_op pair_op.
    by rewrite -(tag_kind_incl_eq (to_tagKindR tkPub) _ VL1 (cmra_included_r _ _)).
  - intros _. exists (: gmap loc _). by rewrite 2!left_id HL.
Qed.

Hai Dang's avatar
Hai Dang committed
227
Lemma tmap_valid (r_f r: tmapUR) t h0 kh
Hai Dang's avatar
Hai Dang committed
228 229
  (Eqtg: r !! t = Some (to_tagKindR tkUnique, h0)) (VN:  kh) :
   (r_f  r)   (r_f  (<[t:= kh]> r)).
Hai Dang's avatar
Hai Dang committed
230
Proof.
Hai Dang's avatar
Hai Dang committed
231 232
  intros VALID.
  apply (local_update_discrete_valid_frame _ _ _ VALID).
Hai Dang's avatar
Hai Dang committed
233
  have EQ := (tmap_insert_op_r _ _ _ _ kh VALID Eqtg). rewrite EQ.
Hai Dang's avatar
Hai Dang committed
234 235 236
  eapply (insert_local_update _ _ _
          (to_tagKindR tkUnique, h0) (to_tagKindR tkUnique, h0));
          [|exact Eqtg|by apply exclusive_local_update].
Hai Dang's avatar
Hai Dang committed
237
  by rewrite (tmap_lookup_op_r _ _ _ _ VALID Eqtg).
Hai Dang's avatar
Hai Dang committed
238 239
Qed.

Hai Dang's avatar
Hai Dang committed
240
(** heaplet *)
Hai Dang's avatar
Hai Dang committed
241 242 243 244 245 246
Lemma to_heapletR_valid h :  (to_heapletR h).
Proof.
  intros l. rewrite /to_heapletR lookup_fmap.
  destruct (h !! l) eqn:Eq; rewrite Eq //.
Qed.

Hai Dang's avatar
Hai Dang committed
247 248
Lemma to_heapletR_lookup h l s :
  to_heapletR h !! l  Some (to_agree s)  h !! l = Some s.
Hai Dang's avatar
Hai Dang committed
249
Proof.
Hai Dang's avatar
Hai Dang committed
250 251 252
  rewrite /to_heapletR lookup_fmap.
  destruct (h !! l) as [s'|] eqn:Eqs; rewrite Eqs /=; [|by inversion 1].
  intros Eq%Some_equiv_inj%to_agree_inj. by inversion Eq.
Hai Dang's avatar
Hai Dang committed
253
Qed.
Hai Dang's avatar
Hai Dang committed
254

Hai Dang's avatar
Hai Dang committed
255 256 257 258 259 260 261
Lemma heapletR_elem_of_dom (h: heapletR) l (VALID: valid h) :
  l  dom (gset loc) h   s, h !! l  Some (to_agree s).
Proof.
  rewrite elem_of_dom. intros [sa Eqs]. move : (VALID l). rewrite Eqs.
  intros [s Eq]%to_agree_uninj. exists s. by rewrite Eq.
Qed.

Hai Dang's avatar
Hai Dang committed
262 263 264 265 266 267 268 269 270
(** The Core *)

Lemma heaplet_core (h: heapletR) : core h = h.
Proof.
  apply (map_eq (M:=gmap loc)).
  intros l. rewrite lookup_core.
  by destruct (h !! l) as [s|] eqn:Eql; rewrite Eql.
Qed.

Hai Dang's avatar
Hai Dang committed
271
Lemma tmap_lookup_core_pub (pm: tmapUR) t h:
Hai Dang's avatar
Hai Dang committed
272
  pm !! t  Some (to_tagKindR tkPub, h) 
Hai Dang's avatar
Hai Dang committed
273 274
  core pm !! t  Some (to_tagKindR tkPub, h).
Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.