cmra.v 20.3 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 296
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
297 298 299 300
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
301 302 303 304 305
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
306
    by rewrite -(tagKindR_incl_eq (to_tgkR tkPub) _ VL1 (cmra_included_r _ _)).
Hai Dang's avatar
Hai Dang committed
307 308 309
  - intros _. exists (: gmap loc _). by rewrite 2!left_id HL.
Qed.

Hai Dang's avatar
Hai Dang committed
310 311 312 313 314 315 316 317 318
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
319
Lemma tmap_valid (r_f r: tmapUR) t h0 kh
Hai Dang's avatar
Hai Dang committed
320
  (Eqtg: r !! t = Some (to_tgkR tkUnique, h0)) (VN:  kh) :
Hai Dang's avatar
Hai Dang committed
321
   (r_f  r)   (r_f  (<[t:= kh]> r)).
Hai Dang's avatar
Hai Dang committed
322
Proof.
Hai Dang's avatar
Hai Dang committed
323 324
  intros VALID.
  apply (local_update_discrete_valid_frame _ _ _ VALID).
Hai Dang's avatar
Hai Dang committed
325
  have EQ := (tmap_insert_op_uniq_r _ _ _ _ kh VALID Eqtg). rewrite EQ.
Hai Dang's avatar
Hai Dang committed
326
  eapply (insert_local_update _ _ _
Hai Dang's avatar
Hai Dang committed
327
          (to_tgkR tkUnique, h0) (to_tgkR tkUnique, h0));
Hai Dang's avatar
Hai Dang committed
328
          [|exact Eqtg|by apply exclusive_local_update].
Hai Dang's avatar
Hai Dang committed
329
  by rewrite (tmap_lookup_op_uniq_r _ _ _ _ VALID Eqtg).
Hai Dang's avatar
Hai Dang committed
330 331
Qed.

Hai Dang's avatar
Hai Dang committed
332
(** heaplet *)
Hai Dang's avatar
Hai Dang committed
333
Lemma to_hplR_valid h :  (to_hplR h).
Hai Dang's avatar
Hai Dang committed
334
Proof.
Hai Dang's avatar
Hai Dang committed
335
  intros l. rewrite /to_hplR lookup_fmap.
Hai Dang's avatar
Hai Dang committed
336 337 338
  destruct (h !! l) eqn:Eq; rewrite Eq //.
Qed.

Hai Dang's avatar
Hai Dang committed
339 340
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
341
Proof.
Hai Dang's avatar
Hai Dang committed
342
  rewrite /to_hplR lookup_fmap.
Hai Dang's avatar
Hai Dang committed
343
  destruct (h !! l) as [s'|] eqn:Eqs; rewrite Eqs /=; [|by inversion 1].
Hai Dang's avatar
Hai Dang committed
344
  intros Eq%Some_equiv_inj%to_agree_inj%leibniz_equiv_iff. by subst s'.
Hai Dang's avatar
Hai Dang committed
345
Qed.
Hai Dang's avatar
Hai Dang committed
346

Hai Dang's avatar
Hai Dang committed
347 348 349 350 351 352 353
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
354 355 356 357 358 359 360 361 362
(** 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
363
Lemma tmap_lookup_core_pub (pm: tmapUR) t h:
Hai Dang's avatar
Hai Dang committed
364 365
  pm !! t  Some (to_tgkR tkPub, h) 
  core pm !! t  Some (to_tgkR tkPub, h).
Hai Dang's avatar
Hai Dang committed
366
Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
Ralf Jung's avatar
Ralf Jung committed
367 368 369

(** Resources that we own. *)

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

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

Hai Dang's avatar
Hai Dang committed
376
Fixpoint locs_seq (l:loc) (n:nat) : gset loc :=
377
  match n with
Hai Dang's avatar
Hai Dang committed
378 379
  | O => 
  | S n => {[l]}  locs_seq (l + 1) n
380 381
  end.

Hai Dang's avatar
Hai Dang committed
382 383 384 385 386
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
387

Hai Dang's avatar
Hai Dang committed
388 389 390
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
391 392
(* 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
393 394

(** res_tag *)
Hai Dang's avatar
Hai Dang committed
395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427
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
428
Lemma write_hpl_lookup l vl h :
Hai Dang's avatar
Hai Dang committed
429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
  ( (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
452
  destruct (write_hpl_lookup l vl h) as [EQ1 EQ2].
Hai Dang's avatar
Hai Dang committed
453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475
  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
476
  intros Lt. destruct (write_hpl_lookup l vl h) as [EQ _].
Hai Dang's avatar
Hai Dang committed
477 478 479
  specialize (EQ _ Lt). by rewrite elem_of_dom EQ lookup_lt_is_Some.
Qed.

Hai Dang's avatar
Hai Dang committed
480 481 482 483 484 485 486
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
487 488
Lemma res_tag_alloc_local_update lsf t k h
  (FRESH: lsf.(rtm) !! t = None) :
Hai Dang's avatar
Hai Dang committed
489 490
  (lsf, ε) ~l~> (lsf  res_tag t k h, res_tag t k h).
Proof.
Hai Dang's avatar
Hai Dang committed
491 492
  destruct lsf as [[tm cm] lm]. rewrite pair_op right_id.
  apply prod_local_update_1.
Hai Dang's avatar
Hai Dang committed
493 494
  rewrite cmra_comm -insert_singleton_op //.
  apply alloc_singleton_local_update; [done|].
Hai Dang's avatar
Hai Dang committed
495
  split. by destruct k. apply to_hplR_valid.
Hai Dang's avatar
Hai Dang committed
496
Qed.
497

Hai Dang's avatar
Hai Dang committed
498 499 500
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
501
  tm !! t = None 
Hai Dang's avatar
Hai Dang committed
502
  (tm  {[t := (to_tgkR k1, to_hplR h1)]}, {[t := (to_tgkR k1, to_hplR h1)]}) ~l~>
Hai Dang's avatar
Hai Dang committed
503
  (tm  {[t := (to_tgkR k2, to_hplR h2)]}, {[t := (to_tgkR k2, to_hplR h2)]}).
Hai Dang's avatar
Hai Dang committed
504
Proof.
Hai Dang's avatar
Hai Dang committed
505
  intros.
Hai Dang's avatar
Hai Dang committed
506
  do 2 rewrite (cmra_comm tm) -insert_singleton_op //.
Hai Dang's avatar
Hai Dang committed
507
  rewrite -(insert_insert tm t (_, to_agree <$> h2)
Hai Dang's avatar
Hai Dang committed
508
                               (to_tgkR k1, to_agree <$> h1)).
Hai Dang's avatar
Hai Dang committed
509
  eapply (singleton_local_update (<[t := _]> tm : tmapUR)).
Hai Dang's avatar
Hai Dang committed
510
  - by rewrite lookup_insert.
Hai Dang's avatar
Hai Dang committed
511 512 513
  - have ?: Exclusive (to_tgkR k1, to_hplR h1).
    { destruct UNIQ; subst k1; apply _. }
    apply exclusive_local_update.
Hai Dang's avatar
Hai Dang committed
514
    split; [apply to_tgkR_valid|apply to_hplR_valid].
Hai Dang's avatar
Hai Dang committed
515 516
Qed.

Hai Dang's avatar
Hai Dang committed
517 518
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
519
  (NONE: r.(rtm) !! t = None) :
Hai Dang's avatar
Hai Dang committed
520
  (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
521
Proof.
Hai Dang's avatar
Hai Dang committed
522 523
  destruct r as [tm cm].
  apply prod_local_update_1. rewrite /=.
Hai Dang's avatar
Hai Dang committed
524
  by apply res_tag_uniq_insert_local_update_inner.
Hai Dang's avatar
Hai Dang committed
525 526
Qed.

Hai Dang's avatar
Hai Dang committed
527 528 529 530 531
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
532
Proof. by apply res_tag_uniq_local_update. Qed.
Hai Dang's avatar
Hai Dang committed
533 534

Lemma res_tag_lookup (k: tag_kind) (h: heaplet) (t: ptr_id) :
Hai Dang's avatar
Hai Dang committed
535
  (res_tag t k h).(rtm) !! t  Some (to_tgkR k, to_agree <$> h).
Hai Dang's avatar
Hai Dang committed
536 537 538 539 540
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
541 542 543 544 545 546 547 548 549 550 551 552 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


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.