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

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

Hai Dang's avatar
Hai Dang committed
8
(** Tag map that connect tags to the heaplet that they govern *)
Hai Dang's avatar
Hai Dang committed
9 10 11
Inductive tag_kind := tkLocal | tkUnique | tkPub.
(* Ex() + Ex() + () *)
Definition tagKindR := csumR (exclR unitO) (csumR (exclR unitO) unitR).
Hai Dang's avatar
Hai Dang committed
12

Hai Dang's avatar
Hai Dang committed
13
Definition to_tgkR (tk: tag_kind) : tagKindR :=
Hai Dang's avatar
Hai Dang committed
14 15 16 17 18
  match tk with
  | tkLocal => Cinl (Excl ())
  | tkUnique => Cinr (Cinl (Excl ()))
  | tkPub => Cinr (Cinr ())
  end.
Hai Dang's avatar
Hai Dang committed
19

Hai Dang's avatar
Hai Dang committed
20 21 22 23 24
Definition heaplet := gmap loc (scalar * scalar).
Definition tmap := gmap ptr_id (tag_kind * heaplet).
Definition heapletR := gmapR loc (agreeR (prodO scalarO scalarO)).
(* ptr_id  TagKind * (loc  Ag(Scalar * Scalar)) *)
Definition tmapUR := gmapUR ptr_id (prodR tagKindR heapletR).
Hai Dang's avatar
Hai Dang committed
25

Hai Dang's avatar
Hai Dang committed
26 27 28
Definition to_hplR (h: heaplet) : heapletR := fmap to_agree h.
Definition to_tmUR (tm: tmap) : tmapUR :=
  fmap (λ kh, (to_tgkR kh.1, to_hplR kh.2)) tm.
Hai Dang's avatar
Hai Dang committed
29

Hai Dang's avatar
Hai Dang committed
30

Hai Dang's avatar
Hai Dang committed
31
Definition tag_locs := gmap ptr_id (gset loc).
Hai Dang's avatar
Hai Dang committed
32

Hai Dang's avatar
Hai Dang committed
33 34 35 36 37 38 39
(** CallId map that protects tags and their associated heaplet *)
(* Ex(tag  gset loc) *)
Definition callStateR := exclR (gmapO ptr_id (gsetO loc)).
Definition cmap := gmap call_id tag_locs.
(* call_id  CallState *)
Definition cmapUR := gmapUR call_id callStateR.
Definition to_cmUR (cm: cmap) : cmapUR := fmap Excl cm.
Hai Dang's avatar
Hai Dang committed
40

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

Hai Dang's avatar
Hai Dang committed
44 45
Definition rtm (r: resUR) : tmapUR := r.1.
Definition rcm (r: resUR) : cmapUR := r.2.
Hai Dang's avatar
Hai Dang committed
46

Hai Dang's avatar
Hai Dang committed
47 48 49 50 51
Instance rtm_proper : Proper (() ==> ()) rtm.
Proof. solve_proper. Qed.
Instance rcm_proper : Proper (() ==> ()) rcm.
Proof. solve_proper. Qed.

Hai Dang's avatar
Hai Dang committed
52 53 54 55 56 57 58
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
59
(** tag_kind properties *)
Hai Dang's avatar
Hai Dang committed
60 61 62
Lemma to_tgkR_valid k : valid (to_tgkR k).
Proof. by destruct k. Qed.

Hai Dang's avatar
Hai Dang committed
63
Lemma tagKindR_incl_eq (k1 k2: tagKindR):
Hai Dang's avatar
Hai Dang committed
64 65
   k2  k1  k2  k1  k2.
Proof.
Hai Dang's avatar
Hai Dang committed
66 67 68 69 70 71
  move => VAL /csum_included
    [?|[[? [? [? [? INCL]]]]|[x1 [x2 [? [? INCL]]]]]]; subst; [done|..].
  - exfalso. eapply exclusive_included; [..|apply INCL|apply VAL]; apply _.
  - move : INCL => /csum_included
      [? |[[? [? [? [? INCL]]]]|[[] [[] [? [? LE]]]]]]; subst; [done|..|done].
    exfalso. eapply exclusive_included; [..|apply INCL|apply VAL]; apply _.
Hai Dang's avatar
Hai Dang committed
72
Qed.
Hai Dang's avatar
Hai Dang committed
73

Hai Dang's avatar
Hai Dang committed
74
Lemma tagKindR_uniq_exclusive_l (h0 h: heapletR) mb :
Hai Dang's avatar
Hai Dang committed
75
  mb  Some (to_tgkR tkUnique, h0)  Some (to_tgkR tkPub, h)  False.
Hai Dang's avatar
Hai Dang committed
76 77 78
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
    intros [Eq _]%Some_equiv_inj.
Hai Dang's avatar
Hai Dang committed
79 80
  - destruct k as [[]|[]|]; simplify_eq.
  - simplify_eq.
Hai Dang's avatar
Hai Dang committed
81 82
Qed.

Hai Dang's avatar
Hai Dang committed
83
Lemma tagKindR_uniq_exclusive_r (h0 h: heapletR) mb :
Hai Dang's avatar
Hai Dang committed
84
  mb  Some (to_tgkR tkPub, h0)  Some (to_tgkR tkUnique, h)  False.
Hai Dang's avatar
Hai Dang committed
85 86 87
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
    intros [Eq _]%Some_equiv_inj.
Hai Dang's avatar
Hai Dang committed
88 89 90 91 92 93 94 95 96 97 98
  - destruct k as [[]|[]|]; simplify_eq.
  - simplify_eq.
Qed.

Lemma tagKindR_local_exclusive_l (h0 h: heapletR) mb :
  mb  Some (to_tgkR tkLocal, h0)  Some (to_tgkR tkPub, h)  False.
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
    intros [Eq _]%Some_equiv_inj.
  - destruct k as [[]|[]|]; simplify_eq.
  - simplify_eq.
Hai Dang's avatar
Hai Dang committed
99 100
Qed.

Hai Dang's avatar
Hai Dang committed
101 102 103 104 105 106 107 108 109
Lemma tagKindR_local_exclusive_r (h0 h: heapletR) mb :
  mb  Some (to_tgkR tkPub, h0)  Some (to_tgkR tkLocal, h)  False.
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
    intros [Eq _]%Some_equiv_inj.
  - destruct k as [[]|[]|]; simplify_eq.
  - simplify_eq.
Qed.

Hai Dang's avatar
Hai Dang committed
110
Lemma tagKindR_exclusive_heaplet' (h0 h: heapletR) mb k1 :
Hai Dang's avatar
Hai Dang committed
111
  mb  Some (to_tgkR tkUnique, h0)  Some (to_tgkR k1, h) 
Hai Dang's avatar
Hai Dang committed
112
  h0  h  k1 = tkUnique.
Hai Dang's avatar
Hai Dang committed
113 114
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
Hai Dang's avatar
Hai Dang committed
115
    intros [Eq1 Eq2]%Some_equiv_inj.
Hai Dang's avatar
Hai Dang committed
116 117
  - destruct k as [[]|[]|], k1; simplify_eq.
  - by destruct k1; simplify_eq.
Hai Dang's avatar
Hai Dang committed
118 119
Qed.

Hai Dang's avatar
Hai Dang committed
120
Lemma tagKindR_exclusive_heaplet (h0 h: heapletR) mb :
Hai Dang's avatar
Hai Dang committed
121
  Some mb  Some (to_tgkR tkUnique, h0)  Some (to_tgkR tkUnique, h)  False.
Hai Dang's avatar
Hai Dang committed
122 123
Proof.
  destruct mb as [c ]. rewrite -Some_op pair_op. intros [Eq _]%Some_equiv_inj.
Hai Dang's avatar
Hai Dang committed
124
  destruct c as [[]|[]|]; inversion Eq; simpl in *; simplify_eq.
Hai Dang's avatar
Hai Dang committed
125
Qed.
Hai Dang's avatar
Hai Dang committed
126

Hai Dang's avatar
Hai Dang committed
127 128 129 130 131 132 133
Lemma tagKindR_exclusive_local_heaplet (h0 h: heapletR) mb :
  Some mb  Some (to_tgkR tkLocal, h0)  Some (to_tgkR tkLocal, h)  False.
Proof.
  destruct mb as [c ]. rewrite -Some_op pair_op. intros [Eq _]%Some_equiv_inj.
  destruct c as [[]|[]|]; inversion Eq; simpl in *; simplify_eq.
Qed.

Hai Dang's avatar
Hai Dang committed
134 135 136
Instance to_tgkR_inj : Inj (=) (=) to_tgkR.
Proof. intros [] [] ?; by simplify_eq. Qed.

Hai Dang's avatar
Hai Dang committed
137
Lemma tagKindR_valid (k: tagKindR) :
Hai Dang's avatar
Hai Dang committed
138
  valid k   k', k = to_tgkR k'.
Hai Dang's avatar
Hai Dang committed
139
Proof.
Hai Dang's avatar
Hai Dang committed
140 141
  destruct k as [[[]|]|[[[]|]|[]|]|]; [|done|..|done| |done|done]; intros VAL.
  - by exists tkLocal.
Hai Dang's avatar
Hai Dang committed
142
  - by exists tkUnique.
Hai Dang's avatar
Hai Dang committed
143
  - by exists tkPub.
Hai Dang's avatar
Hai Dang committed
144 145
Qed.

Hai Dang's avatar
Hai Dang committed
146
(** cmap properties *)
Hai Dang's avatar
Hai Dang committed
147 148 149
Lemma cmap_lookup_op_r (cm1 cm2: cmapUR) c (Tls: tag_locs)
  (VALID:  (cm1  cm2)) :
  cm2 !! c = Some (Excl Tls)  (cm1  cm2) !! c = Some (Excl Tls).
Hai Dang's avatar
Hai Dang committed
150 151 152 153
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.
Hai Dang's avatar
Hai Dang committed
154
  destruct cs'; auto; try inversion 1.
Hai Dang's avatar
Hai Dang committed
155 156
Qed.

Hai Dang's avatar
Hai Dang committed
157 158 159
Lemma cmap_lookup_op_l (cm1 cm2: cmapUR) c (Tls: tag_locs)
  (VALID:  (cm1  cm2)) :
  cm1 !! c = Some (Excl Tls)  (cm1  cm2) !! c = Some (Excl Tls).
Hai Dang's avatar
Hai Dang committed
160 161 162 163
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.
Hai Dang's avatar
Hai Dang committed
164
  destruct cs'; auto; try inversion 1.
Hai Dang's avatar
Hai Dang committed
165 166
Qed.

Hai Dang's avatar
Hai Dang committed
167 168 169
Lemma cmap_lookup_op_l_equiv (cm1 cm2: cmapUR) c (Tls: tag_locs)
  (VALID:  (cm1  cm2)) :
  cm1 !! c  Some (Excl Tls)  (cm1  cm2) !! c  Some (Excl Tls).
Hai Dang's avatar
Hai Dang committed
170 171 172 173
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.
Hai Dang's avatar
Hai Dang committed
174
  destruct cs'; auto; try inversion 1.
Hai Dang's avatar
Hai Dang committed
175 176
Qed.

Hai Dang's avatar
Hai Dang committed
177 178 179
Lemma cmap_lookup_op_unique_included (cm1 cm2: cmapUR) c (Tls: tag_locs)
  (VALID:  cm2) (INCL: cm1  cm2) :
  cm1 !! c  Some (Excl Tls)  cm2 !! c  Some (Excl Tls).
Hai Dang's avatar
Hai Dang committed
180 181 182 183 184
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
185 186 187
Lemma cmap_insert_op_r (cm1 cm2: cmapUR) c Tls cs
  (VALID:  (cm1  cm2)):
  cm2 !! c = Some (Excl Tls) 
Hai Dang's avatar
Hai Dang committed
188 189 190 191
  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.
Hai Dang's avatar
Hai Dang committed
192
  destruct (cm1 !! c) eqn:Eqc; rewrite Eqc; [inversion 1..|].
Hai Dang's avatar
Hai Dang committed
193 194 195 196 197
  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
198

Hai Dang's avatar
Hai Dang committed
199 200
Lemma callStateR_exclusive_Some (Tls1 Tls2: tag_locs) (cs: callStateR) :
  Some cs  Some (Excl Tls1)  Some (Excl Tls2)  False.
201 202
Proof.
  rewrite -Some_op. intros Eq%Some_equiv_inj.
Hai Dang's avatar
Hai Dang committed
203
  destruct cs; inversion Eq; simplify_eq.
204 205
Qed.

Hai Dang's avatar
Hai Dang committed
206 207
Lemma callStateR_exclusive_eq (Tls1 Tls2: tag_locs) mb :
  mb  Some (Excl Tls1)  Some (Excl Tls2)  Tls1 = Tls2.
208 209 210 211 212
Proof.
  destruct mb. by intros ?%callStateR_exclusive_Some.
  rewrite left_id. intros Eq%Some_equiv_inj. by simplify_eq.
Qed.

Hai Dang's avatar
Hai Dang committed
213
(** tmap properties *)
Hai Dang's avatar
Hai Dang committed
214
Lemma tmap_insert_op_uniq_r (pm1 pm2: tmapUR) t h0 kh
Hai Dang's avatar
Hai Dang committed
215 216
  (VALID:  (pm1  pm2)) :
  pm2 !! t = Some (to_tgkR tkUnique, h0) 
Hai Dang's avatar
Hai Dang committed
217 218 219 220 221 222 223 224 225 226 227 228
  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
229
Lemma tmap_lookup_op_uniq_r (pm1 pm2: tmapUR) t h0
Hai Dang's avatar
Hai Dang committed
230 231 232
  (VALID:  (pm1  pm2)) :
  pm2 !! t = Some (to_tgkR tkUnique, h0) 
  (pm1  pm2) !! t = Some (to_tgkR tkUnique, h0).
Hai Dang's avatar
Hai Dang committed
233 234 235 236 237
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
238

Hai Dang's avatar
Hai Dang committed
239
Lemma tmap_lookup_op_l_uniq_equiv (pm1 pm2: tmapUR) t h0
Hai Dang's avatar
Hai Dang committed
240
  (VALID:  (pm1  pm2)):
Hai Dang's avatar
Hai Dang committed
241 242
  pm1 !! t  Some (to_tgkR tkUnique, h0) 
  (pm1  pm2) !! t  Some (to_tgkR tkUnique, h0).
Hai Dang's avatar
Hai Dang committed
243 244 245 246 247 248
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
249
Lemma tmap_lookup_op_uniq_included (pm1 pm2: tmapUR) t h0
Hai Dang's avatar
Hai Dang committed
250
  (VALID:  pm2) (INCL: pm1  pm2):
Hai Dang's avatar
Hai Dang committed
251 252
  pm1 !! t  Some (to_tgkR tkUnique, h0) 
  pm2 !! t  Some (to_tgkR tkUnique, h0).
Hai Dang's avatar
Hai Dang committed
253
Proof.
Hai Dang's avatar
Hai Dang committed
254
  destruct INCL as [cm' Eq]. rewrite Eq. apply tmap_lookup_op_l_uniq_equiv.
Hai Dang's avatar
Hai Dang committed
255 256 257
  by rewrite -Eq.
Qed.

Hai Dang's avatar
Hai Dang committed
258 259 260 261 262 263 264 265 266 267
Lemma tmap_lookup_op_r_uniq_equiv (pm1 pm2: tmapUR) t h0
  (VALID:  (pm1  pm2)) :
  pm2 !! t  Some (to_tgkR tkUnique, h0) 
  (pm1  pm2) !! t  Some (to_tgkR tkUnique, h0).
Proof.
  intros HL. eapply tmap_lookup_op_uniq_included; [done|..|exact HL].
  by apply cmra_included_r.
Qed.


Hai Dang's avatar
Hai Dang committed
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295
Lemma tmap_lookup_op_l_local_equiv (pm1 pm2: tmapUR) t h0
  (VALID:  (pm1  pm2)):
  pm1 !! t  Some (to_tgkR tkLocal, h0) 
  (pm1  pm2) !! t  Some (to_tgkR tkLocal, 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.

Lemma tmap_lookup_op_local_included (pm1 pm2: tmapUR) t h0
  (VALID:  pm2) (INCL: pm1  pm2):
  pm1 !! t  Some (to_tgkR tkLocal, h0) 
  pm2 !! t  Some (to_tgkR tkLocal, h0).
Proof.
  destruct INCL as [cm' Eq]. rewrite Eq. apply tmap_lookup_op_l_local_equiv.
  by rewrite -Eq.
Qed.

Lemma tmap_lookup_op_r_local_equiv (pm1 pm2: tmapUR) t h0
  (VALID:  (pm1  pm2)) :
  pm2 !! t  Some (to_tgkR tkLocal, h0) 
  (pm1  pm2) !! t  Some (to_tgkR tkLocal, h0).
Proof.
  intros HL. eapply tmap_lookup_op_local_included; [done|..|exact HL].
  by apply cmra_included_r.
Qed.

Hai Dang's avatar
Hai Dang committed
296 297 298 299 300 301 302 303 304 305 306 307
Lemma tmap_lookup_op_l_equiv_pub (pm1 pm2: tmapUR) t h1
  (VALID:  (pm1  pm2)):
  pm1 !! t  Some (to_tgkR tkPub, h1) 
   h2, (pm1  pm2) !! t  Some (to_tgkR tkPub, h1  h2).
Proof.
  intros HL. move : (VALID t). rewrite lookup_op.
  destruct (pm2 !! t) as [[k2 h2]|] eqn:Eqt; rewrite Eqt; rewrite -> HL.
  - rewrite -Some_op pair_op. move => [ VL1 ?]. exists h2. simpl in VL1.
    rewrite HL -Some_op pair_op.
    by rewrite -(tagKindR_incl_eq (to_tgkR tkPub) _ VL1 (cmra_included_r _ _)).
  - intros _. exists (: gmap loc _). by rewrite 2!right_id HL.
Qed.
Hai Dang's avatar
Hai Dang committed
308

Hai Dang's avatar
Hai Dang committed
309 310 311 312
Lemma tmap_lookup_op_r_equiv_pub (pm1 pm2: tmapUR) t h2
  (VALID:  (pm1  pm2)):
  pm2 !! t  Some (to_tgkR tkPub, h2) 
   h1, (pm1  pm2) !! t  Some (to_tgkR tkPub, h1  h2).
Hai Dang's avatar
Hai Dang committed
313 314 315 316 317
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.
Hai Dang's avatar
Hai Dang committed
318
    by rewrite -(tagKindR_incl_eq (to_tgkR tkPub) _ VL1 (cmra_included_r _ _)).
Hai Dang's avatar
Hai Dang committed
319 320 321
  - intros _. exists (: gmap loc _). by rewrite 2!left_id HL.
Qed.

Hai Dang's avatar
Hai Dang committed
322 323 324 325 326 327 328 329 330
Lemma tmap_lookup_op_None_inv (pm1 pm2: tmapUR) t :
  (pm1  pm2) !! t = None 
  pm1 !! t = None  pm2 !! t = None.
Proof.
  rewrite lookup_op.
  destruct (pm1 !! t) eqn:Eq1, (pm2 !! t) eqn:Eq2;
    rewrite Eq1 Eq2; [inversion 1..|done].
Qed.

Hai Dang's avatar
Hai Dang committed
331
Lemma tmap_valid (r_f r: tmapUR) t h0 kh
Hai Dang's avatar
Hai Dang committed
332
  (Eqtg: r !! t = Some (to_tgkR tkUnique, h0)) (VN:  kh) :
Hai Dang's avatar
Hai Dang committed
333
   (r_f  r)   (r_f  (<[t:= kh]> r)).
Hai Dang's avatar
Hai Dang committed
334
Proof.
Hai Dang's avatar
Hai Dang committed
335 336
  intros VALID.
  apply (local_update_discrete_valid_frame _ _ _ VALID).
Hai Dang's avatar
Hai Dang committed
337
  have EQ := (tmap_insert_op_uniq_r _ _ _ _ kh VALID Eqtg). rewrite EQ.
Hai Dang's avatar
Hai Dang committed
338
  eapply (insert_local_update _ _ _
Hai Dang's avatar
Hai Dang committed
339
          (to_tgkR tkUnique, h0) (to_tgkR tkUnique, h0));
Hai Dang's avatar
Hai Dang committed
340
          [|exact Eqtg|by apply exclusive_local_update].
Hai Dang's avatar
Hai Dang committed
341
  by rewrite (tmap_lookup_op_uniq_r _ _ _ _ VALID Eqtg).
Hai Dang's avatar
Hai Dang committed
342 343
Qed.

Hai Dang's avatar
Hai Dang committed
344
(** heaplet *)
Hai Dang's avatar
Hai Dang committed
345
Lemma to_hplR_valid h :  (to_hplR h).
Hai Dang's avatar
Hai Dang committed
346
Proof.
Hai Dang's avatar
Hai Dang committed
347
  intros l. rewrite /to_hplR lookup_fmap.
Hai Dang's avatar
Hai Dang committed
348 349 350
  destruct (h !! l) eqn:Eq; rewrite Eq //.
Qed.

Hai Dang's avatar
Hai Dang committed
351 352
Lemma to_hplR_lookup h l s :
  to_hplR h !! l  Some (to_agree s)  h !! l = Some s.
Hai Dang's avatar
Hai Dang committed
353
Proof.
Hai Dang's avatar
Hai Dang committed
354
  rewrite /to_hplR lookup_fmap.
Hai Dang's avatar
Hai Dang committed
355
  destruct (h !! l) as [s'|] eqn:Eqs; rewrite Eqs /=; [|by inversion 1].
Hai Dang's avatar
Hai Dang committed
356
  intros Eq%Some_equiv_inj%to_agree_inj%leibniz_equiv_iff. by subst s'.
Hai Dang's avatar
Hai Dang committed
357
Qed.
Hai Dang's avatar
Hai Dang committed
358

Hai Dang's avatar
Hai Dang committed
359 360 361 362 363 364 365
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
366 367 368 369 370 371 372 373 374
(** 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
375
Lemma tmap_lookup_core_pub (pm: tmapUR) t h:
Hai Dang's avatar
Hai Dang committed
376 377
  pm !! t  Some (to_tgkR tkPub, h) 
  core pm !! t  Some (to_tgkR tkPub, h).
Hai Dang's avatar
Hai Dang committed
378
Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
Ralf Jung's avatar
Ralf Jung committed
379 380 381

(** Resources that we own. *)

Ralf Jung's avatar
Ralf Jung committed
382
Definition res_tag tg tk (h: heaplet) : resUR :=
Hai Dang's avatar
Hai Dang committed
383
  ({[tg := (to_tgkR tk, to_agree <$> h)]}, ε).
Hai Dang's avatar
Hai Dang committed
384

Hai Dang's avatar
Hai Dang committed
385
Definition res_cs (c: call_id) (cs: tag_locs) : resUR :=
Hai Dang's avatar
Hai Dang committed
386
  (ε, to_cmUR {[c := cs]}).
Hai Dang's avatar
Hai Dang committed
387

Hai Dang's avatar
Hai Dang committed
388
Fixpoint locs_seq (l:loc) (n:nat) : gset loc :=
389
  match n with
Hai Dang's avatar
Hai Dang committed
390 391
  | O => 
  | S n => {[l]}  locs_seq (l + 1) n
392 393
  end.

Hai Dang's avatar
Hai Dang committed
394 395 396 397 398
Fixpoint write_hpl l (v: list (scalar * scalar)) (h: heaplet) : heaplet :=
  match v with
  | [] => h
  | sst :: v' => write_hpl (l + 1) v' (<[l:=sst]> h)
  end.
Hai Dang's avatar
Hai Dang committed
399

Hai Dang's avatar
Hai Dang committed
400 401 402
Definition res_loc l (v: list (scalar * scalar)) (t: ptr_id) : resUR :=
  res_tag t tkLocal (write_hpl l v ).

Hai Dang's avatar
Hai Dang committed
403 404
(* Definition res_mapsto (l:loc) (v: list (scalar * scalar)) (t: ptr_id) : resUR :=
  res_loc l (length v) t  res_tag t tkUnique (write_hpl l v ). *)
Hai Dang's avatar
Hai Dang committed
405 406

(** res_tag *)
Hai Dang's avatar
Hai Dang committed
407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439
Lemma locs_seq_elem_of_equiv l n i :
  (i < n)%nat  l + i  locs_seq l n.
Proof.
  revert l i. induction n as [|n IH]; intros l i.
  { simpl. split; intros. lia. exfalso. by eapply not_elem_of_empty. }
  rewrite /= elem_of_union elem_of_singleton.
  destruct i as [|i]; simpl.
  - rewrite shift_loc_0_nat. split; intros; [by left|lia].
  - rewrite (_: l + S i = (l + 1) + i).
    + rewrite -IH. split; intros CASE; [right; by lia|].
      destruct CASE as [CASE|?]; [|lia]. exfalso.
      move : CASE. rewrite shift_loc_assoc -{2}(shift_loc_0 l).
      intros ?%shift_loc_inj. lia.
    + rewrite shift_loc_assoc. f_equal. lia.
Qed.

Lemma locs_seq_elem_of l n i :
  (i < n)%nat  l + i  locs_seq l n.
Proof. by intros; apply locs_seq_elem_of_equiv. Qed.

Lemma locs_seq_elem_of_2 l n l' :
  l'  locs_seq l n   i : nat, l' = l + i  (i < n)%nat.
Proof.
  revert l. induction n as [|n IH]; simpl; intros l.
  { by intros ?%not_elem_of_empty. }
  rewrite elem_of_union elem_of_singleton.
  intros [?|[i [Eqi Lt]]%IH].
  - subst l'. exists O. rewrite shift_loc_0_nat. split; [done|lia].
  - exists (S i). split; [|lia].
    rewrite (_: l + S i = l + 1 + i) //.
    rewrite shift_loc_assoc. f_equal. lia.
Qed.

Hai Dang's avatar
Hai Dang committed
440
Lemma write_hpl_lookup l vl h :
Hai Dang's avatar
Hai Dang committed
441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
  ( (i: nat), (i < length vl)%nat  write_hpl l vl h !! (l + i) = vl !! i) 
  ( (l': loc), ( (i: nat), (i < length vl)%nat  l'  l + i) 
    write_hpl l vl h !! l' = h !! l').
Proof.
  revert l h. induction vl as [|v vl IH]; move => l h; simpl;
    [split; [intros ?; by lia|done]|].
  destruct (IH (l + 1) (<[l:=v]> h)) as [IH1 IH2]. split.
  - intros i Lt. destruct i as [|i].
    + rewrite shift_loc_0_nat /=. rewrite IH2; [by rewrite lookup_insert|].
      move => ? _.
      rewrite shift_loc_assoc -{1}(shift_loc_0 l) => /shift_loc_inj ?. by lia.
    + rewrite /= -IH1; [|lia].  by rewrite shift_loc_assoc -(Nat2Z.inj_add 1).
  - intros l' Lt. rewrite IH2.
    + rewrite lookup_insert_ne; [done|].
      move => ?. subst l'. apply (Lt O); [lia|by rewrite shift_loc_0_nat].
    + move => i Lti. rewrite shift_loc_assoc -(Nat2Z.inj_add 1).
      apply Lt. by lia.
Qed.

Lemma write_hpl_lookup_case l vl h l' :
  ( (i: nat), (i < length vl)%nat  l' = l + i  write_hpl l vl h !! (l + i) = vl !! i)
   (( (i: nat), (i < length vl)%nat  l'  l + i)  write_hpl l vl h !! l' = h !! l').
Proof.
Hai Dang's avatar
Hai Dang committed
464
  destruct (write_hpl_lookup l vl h) as [EQ1 EQ2].
Hai Dang's avatar
Hai Dang committed
465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487
  case (decide (l'.1 = l.1)) => [Eql|NEql];
    [case (decide (l.2  l'.2 < l.2 + length vl)) => [[Le Lt]|NIN]|].
  - have Eql2: l' = l + Z.of_nat (Z.to_nat (l'.2 - l.2)). {
      destruct l, l'. move : Eql Le => /= -> ?.
      rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
    have Lt1: (Z.to_nat (l'.2 - l.2) < length vl)%nat
      by rewrite -(Nat2Z.id (length _)) -Z2Nat.inj_lt; lia.
    specialize (EQ1 _ Lt1).
    rewrite -Eql2 in EQ1. left.
    exists (Z.to_nat (l'.2 - l.2)). repeat split; [done..|by rewrite -Eql2].
  - right.
    have ?: ( (i: nat), (i < length vl)%nat  l'  l + i).
    { intros i Lt Eq3. apply NIN. rewrite Eq3 /=. lia. }
    split; [done|]. by apply EQ2.
  - right.
    have ?: ( (i: nat), (i < length vl)%nat  l'  l + i).
    { intros i Lt Eq3. apply NEql. by rewrite Eq3. }
    split; [done|]. by apply EQ2.
Qed.

Lemma write_hpl_elem_of_dom l vl h i :
  (i < length vl)%nat  l + i  dom (gset loc) (write_hpl l vl h).
Proof.
Hai Dang's avatar
Hai Dang committed
488
  intros Lt. destruct (write_hpl_lookup l vl h) as [EQ _].
Hai Dang's avatar
Hai Dang committed
489 490 491
  specialize (EQ _ Lt). by rewrite elem_of_dom EQ lookup_lt_is_Some.
Qed.

Hai Dang's avatar
Hai Dang committed
492 493 494 495 496 497 498
Lemma write_hpl_is_Some l vl h i :
  (i < length vl)%nat  is_Some (write_hpl l vl h !! (l + i)).
Proof.
  intros Lt. destruct (write_hpl_lookup l vl h) as [EQ _].
  specialize (EQ _ Lt). by rewrite EQ lookup_lt_is_Some.
Qed.

Hai Dang's avatar
Hai Dang committed
499 500
Lemma res_tag_alloc_local_update lsf t k h
  (FRESH: lsf.(rtm) !! t = None) :
Hai Dang's avatar
Hai Dang committed
501 502
  (lsf, ε) ~l~> (lsf  res_tag t k h, res_tag t k h).
Proof.
Hai Dang's avatar
Hai Dang committed
503 504
  destruct lsf as [[tm cm] lm]. rewrite pair_op right_id.
  apply prod_local_update_1.
Hai Dang's avatar
Hai Dang committed
505 506
  rewrite cmra_comm -insert_singleton_op //.
  apply alloc_singleton_local_update; [done|].
Hai Dang's avatar
Hai Dang committed
507
  split. by destruct k. apply to_hplR_valid.
Hai Dang's avatar
Hai Dang committed
508
Qed.
509

Hai Dang's avatar
Hai Dang committed
510 511 512
Lemma res_tag_uniq_insert_local_update_inner
  (tm: tmapUR) t k1 k2 (h1 h2: heaplet)
  (UNIQ: k1 = tkLocal  k1 = tkUnique) :
Hai Dang's avatar
Hai Dang committed
513
  tm !! t = None 
Hai Dang's avatar
Hai Dang committed
514
  (tm  {[t := (to_tgkR k1, to_hplR h1)]}, {[t := (to_tgkR k1, to_hplR h1)]}) ~l~>
Hai Dang's avatar
Hai Dang committed
515
  (tm  {[t := (to_tgkR k2, to_hplR h2)]}, {[t := (to_tgkR k2, to_hplR h2)]}).
Hai Dang's avatar
Hai Dang committed
516
Proof.
Hai Dang's avatar
Hai Dang committed
517
  intros.
Hai Dang's avatar
Hai Dang committed
518
  do 2 rewrite (cmra_comm tm) -insert_singleton_op //.
Hai Dang's avatar
Hai Dang committed
519
  rewrite -(insert_insert tm t (_, to_agree <$> h2)
Hai Dang's avatar
Hai Dang committed
520
                               (to_tgkR k1, to_agree <$> h1)).
Hai Dang's avatar
Hai Dang committed
521
  eapply (singleton_local_update (<[t := _]> tm : tmapUR)).
Hai Dang's avatar
Hai Dang committed
522
  - by rewrite lookup_insert.
Hai Dang's avatar
Hai Dang committed
523 524 525
  - have ?: Exclusive (to_tgkR k1, to_hplR h1).
    { destruct UNIQ; subst k1; apply _. }
    apply exclusive_local_update.
Hai Dang's avatar
Hai Dang committed
526
    split; [apply to_tgkR_valid|apply to_hplR_valid].
Hai Dang's avatar
Hai Dang committed
527 528
Qed.

Hai Dang's avatar
Hai Dang committed
529 530
Lemma res_tag_uniq_local_update (r: resUR) t k h k' h'
  (UNIQ: k = tkLocal  k = tkUnique)
Hai Dang's avatar
Hai Dang committed
531
  (NONE: r.(rtm) !! t = None) :
Hai Dang's avatar
Hai Dang committed
532
  (r  res_tag t k h, res_tag t k h) ~l~> (r  res_tag t k' h', res_tag t k' h').
Hai Dang's avatar
Hai Dang committed
533
Proof.
Hai Dang's avatar
Hai Dang committed
534 535
  destruct r as [tm cm].
  apply prod_local_update_1. rewrite /=.
Hai Dang's avatar
Hai Dang committed
536
  by apply res_tag_uniq_insert_local_update_inner.
Hai Dang's avatar
Hai Dang committed
537 538
Qed.

Hai Dang's avatar
Hai Dang committed
539 540 541 542 543
Lemma res_tag_1_insert_local_update (r: resUR) (l: loc) k s1 s2 (t: ptr_id)
  (UNIQ: k = tkLocal  k = tkUnique)
  (NONE: r.(rtm) !! t = None) :
  (r  res_tag t k {[l := s1]}, res_tag t k {[l := s1]}) ~l~>
  (r  res_tag t k {[l := s2]}, res_tag t k {[l := s2]}).
Hai Dang's avatar
Hai Dang committed
544
Proof. by apply res_tag_uniq_local_update. Qed.
Hai Dang's avatar
Hai Dang committed
545 546

Lemma res_tag_lookup (k: tag_kind) (h: heaplet) (t: ptr_id) :
Hai Dang's avatar
Hai Dang committed
547
  (res_tag t k h).(rtm) !! t  Some (to_tgkR k, to_agree <$> h).
Hai Dang's avatar
Hai Dang committed
548 549 550 551 552
Proof. by rewrite lookup_insert. Qed.

Lemma res_tag_lookup_ne (k: tag_kind) (h: heaplet) (t t': ptr_id) (NEQ: t'  t) :
  (res_tag t k h).(rtm) !! t'  None.
Proof. by rewrite lookup_insert_ne. Qed.
Hai Dang's avatar
Hai Dang committed
553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589


Lemma res_tag_uniq_dealloc_local_update_inner
  (tm: tmapUR) t k h
  (UNIQ: k = tkLocal  k = tkUnique) :
  tm !! t = None 
  (tm  {[t := (to_tgkR k, h)]}, {[t := (to_tgkR k, h)]}) ~l~>
  (tm, ε).
Proof.
  intros.
  rewrite (cmra_comm tm) -insert_singleton_op //.
  rewrite -{2}(delete_insert tm t (to_tgkR k, h)) //.
  eapply (delete_singleton_local_update (<[t := _]> tm : tmapUR)).
  destruct UNIQ; subst k; apply _.
Qed.

Lemma res_tag_uniq_dealloc_local_update (r: resUR) t k h
  (UNIQ: k = tkLocal  k = tkUnique)
  (NONE: r.(rtm) !! t = None) :
  (r  res_tag t k h, res_tag t k h) ~l~> (r, ε : resUR).
Proof.
  destruct r as [tm cm]. rewrite pair_op right_id.
  apply prod_local_update_1.
  by apply res_tag_uniq_dealloc_local_update_inner.
Qed.

Lemma res_tag_uniq_dealloc_local_update_r (r: resUR) r' t k h
  (UNIQ: k = tkLocal  k = tkUnique)
  (NONE: (r  r').(rtm) !! t = None) :
  (r  r'  res_tag t k h, r'  res_tag t k h) ~l~>
  (r  r', r').
Proof.
  rewrite (cmra_comm r' (res_tag t k h)).
  rewrite -{4}(left_id ε _ r').
  by apply op_local_update_frame, res_tag_uniq_dealloc_local_update.
Qed.