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
8
9

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

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

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)) unitR.
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 () 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
29
Notation heaplet := mem.
Definition tmap := gmap ptr_id (tag_kind * heaplet).
Hai Dang's avatar
Hai Dang committed
30
Definition heapletR := gmapR loc (agreeR scalarC).
Hai Dang's avatar
Hai Dang committed
31
(* ptr_id  TagKid x (loc  Ag(Scalar)) *)
Hai Dang's avatar
Hai Dang committed
32
Definition tmapUR := gmapUR ptr_id (prodR tagKindR heapletR).
Hai Dang's avatar
Hai Dang committed
33

Hai Dang's avatar
Hai Dang committed
34
Definition to_heapR (h: heaplet) : heapletR := fmap to_agree h.
Hai Dang's avatar
Hai Dang committed
35
Definition to_tmapUR (pm: tmap) : tmapUR :=
Hai Dang's avatar
Hai Dang committed
36
37
38
39
40
41
  fmap (λ tm, (to_tagKindR tm.1, to_heapR tm.2)) pm.

Definition lmap := gmap loc ptr_id.
Definition tagR := exclR (leibnizO ptr_id).
Definition lmapUR := gmapUR loc tagR.
Definition to_tagR (t: ptr_id) := Excl t.
Hai Dang's avatar
Hai Dang committed
42

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

Hai Dang's avatar
Hai Dang committed
46
47
48
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
49

Hai Dang's avatar
Hai Dang committed
50
51
52
53
54
55
56
Instance rtm_proper : Proper (() ==> ()) rtm.
Proof. solve_proper. Qed.
Instance rcm_proper : Proper (() ==> ()) rcm.
Proof. solve_proper. Qed.
Instance rlm_proper : Proper (() ==> ()) rlm.
Proof. solve_proper. Qed.

Hai Dang's avatar
Hai Dang committed
57
58
59
60
61
62
63
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
64
(** tag_kind properties *)
Hai Dang's avatar
Hai Dang committed
65
66
67
Lemma tag_kind_incl_eq (k1 k2: tagKindR):
   k2  k1  k2  k1  k2.
Proof.
Hai Dang's avatar
Hai Dang committed
68
69
70
  move => VAL /csum_included [? |[[? [? [? [? Eq]]]]|[[] [[] [? [? LE]]]]]];
    subst; [done|..|done].
  exfalso. eapply exclusive_included; [..|apply Eq|apply VAL]. apply _.
Hai Dang's avatar
Hai Dang committed
71
Qed.
Hai Dang's avatar
Hai Dang committed
72

Hai Dang's avatar
Hai Dang committed
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.

Hai Dang's avatar
Hai Dang committed
91
92
93
Lemma tagKindR_exclusive_heaplet' (h0 h: heapletR) mb k1 :
  mb  Some (to_tagKindR tkUnique, h0)  Some (to_tagKindR k1, h) 
  h0  h  k1 = tkUnique.
Hai Dang's avatar
Hai Dang committed
94
95
Proof.
  destruct mb as [[k ?]|]; [rewrite -Some_op pair_op|rewrite left_id];
Hai Dang's avatar
Hai Dang committed
96
97
98
    intros [Eq1 Eq2]%Some_equiv_inj.
  - destruct k as [[[]|]| |], k1 ; inversion Eq1; simplify_eq.
  - destruct k1; by inversion Eq1.
Hai Dang's avatar
Hai Dang committed
99
100
Qed.

Hai Dang's avatar
Hai Dang committed
101
Lemma tagKindR_exclusive_heaplet (h0 h: heapletR) mb :
Hai Dang's avatar
Hai Dang committed
102
103
104
105
106
  Some mb  Some (to_tagKindR tkUnique, h0)  Some (to_tagKindR tkUnique, h)  False.
Proof.
  destruct mb as [c ]. rewrite -Some_op pair_op. intros [Eq _]%Some_equiv_inj.
  destruct c; inversion Eq; simpl in *; simplify_eq.
Qed.
Hai Dang's avatar
Hai Dang committed
107

Hai Dang's avatar
Hai Dang committed
108
Lemma tagKindR_valid (k: tagKindR) :
Hai Dang's avatar
Hai Dang committed
109
  valid k   k', k = to_tagKindR k'.
Hai Dang's avatar
Hai Dang committed
110
Proof.
Hai Dang's avatar
Hai Dang committed
111
  destruct k as [[[]|]|[]|]; [|done|..|done]; intros VAL.
Hai Dang's avatar
Hai Dang committed
112
  - by exists tkUnique.
Hai Dang's avatar
Hai Dang committed
113
  - by exists tkPub.
Hai Dang's avatar
Hai Dang committed
114
115
Qed.

Hai Dang's avatar
Hai Dang committed
116
(** cmap properties *)
Hai Dang's avatar
Hai Dang committed
117
Lemma cmap_lookup_op_r (cm1 cm2: cmapUR) c T (VALID:  (cm1  cm2)):
Hai Dang's avatar
Hai Dang committed
118
119
  cm2 !! c = Some (to_callStateR (csOwned T)) 
  (cm1  cm2) !! c = Some (to_callStateR (csOwned T)).
Hai Dang's avatar
Hai Dang committed
120
121
122
123
124
125
126
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
127
Lemma cmap_lookup_op_l (cm1 cm2: cmapUR) c T (VALID:  (cm1  cm2)):
Hai Dang's avatar
Hai Dang committed
128
129
  cm1 !! c = Some (to_callStateR (csOwned T)) 
  (cm1  cm2) !! c = Some (to_callStateR (csOwned T)).
Hai Dang's avatar
Hai Dang committed
130
131
132
133
134
135
136
137
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
138
139
  cm1 !! c  Some (to_callStateR (csOwned T)) 
  (cm1  cm2) !! c  Some (to_callStateR (csOwned T)).
Hai Dang's avatar
Hai Dang committed
140
141
142
143
144
145
146
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
147
148
149
150
151
152
153
154
155
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
156
157
158
159
160
161
162
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.
Hai Dang's avatar
Hai Dang committed
163
  destruct cs' as [[]|c2|]; auto; inversion 1.
Hai Dang's avatar
Hai Dang committed
164
165
Qed.

Hai Dang's avatar
Hai Dang committed
166
Lemma cmap_insert_op_r (cm1 cm2: cmapUR) c T cs (VALID:  (cm1  cm2)):
Hai Dang's avatar
Hai Dang committed
167
  cm2 !! c = Some (to_callStateR (csOwned T)) 
Hai Dang's avatar
Hai Dang committed
168
169
170
171
172
173
174
175
176
177
  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
178

Hai Dang's avatar
Hai Dang committed
179
180
181
182
183
184
185
186
187
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.

188
189
190
191
192
193
194
195
196
197
198
199
200
201
Lemma callStateR_exclusive_Some T1 T2 cs :
  Some cs  Some (to_callStateR (csOwned T1))  Some (to_callStateR (csOwned T2))  False.
Proof.
  rewrite -Some_op. intros Eq%Some_equiv_inj.
  destruct cs as [[]| |]; inversion Eq; simplify_eq.
Qed.

Lemma callStateR_exclusive_eq T1 T2 mb :
  mb  Some (to_callStateR (csOwned T1))  Some (to_callStateR (csOwned T2))  T1 = T2.
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
202
203
(** tmap properties *)
Lemma tmap_insert_op_r (pm1 pm2: tmapUR) t h0 kh (VALID:  (pm1  pm2)):
Hai Dang's avatar
Hai Dang committed
204
205
206
207
208
209
210
211
212
213
214
215
216
  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
217
Lemma tmap_lookup_op_r (pm1 pm2: tmapUR) t h0 (VALID:  (pm1  pm2)):
Hai Dang's avatar
Hai Dang committed
218
219
220
221
222
223
224
  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
225

Hai Dang's avatar
Hai Dang committed
226
227
228
229
230
231
232
233
234
Lemma tmap_lookup_op_r_unique_equiv (pm1 pm2: tmapUR) t h0 (VALID:  (pm1  pm2)):
  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
235
Lemma tmap_lookup_op_l_unique_equiv (pm1 pm2: tmapUR) t h0
Hai Dang's avatar
Hai Dang committed
236
237
238
239
240
241
242
243
244
  (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
245
Lemma tmap_lookup_op_unique_included (pm1 pm2: tmapUR) t h0
Hai Dang's avatar
Hai Dang committed
246
247
248
249
  (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
250
  destruct INCL as [cm' Eq]. rewrite Eq. apply tmap_lookup_op_l_unique_equiv.
Hai Dang's avatar
Hai Dang committed
251
252
253
  by rewrite -Eq.
Qed.

Hai Dang's avatar
Hai Dang committed
254
Lemma tmap_lookup_op_r_equiv_pub (pm1 pm2: tmapUR) t h2 (VALID:  (pm1  pm2)):
Hai Dang's avatar
Hai Dang committed
255
256
257
258
259
260
261
262
263
264
265
  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
266
Lemma tmap_valid (r_f r: tmapUR) t h0 kh
Hai Dang's avatar
Hai Dang committed
267
268
  (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
269
Proof.
Hai Dang's avatar
Hai Dang committed
270
271
  intros VALID.
  apply (local_update_discrete_valid_frame _ _ _ VALID).
Hai Dang's avatar
Hai Dang committed
272
  have EQ := (tmap_insert_op_r _ _ _ _ kh VALID Eqtg). rewrite EQ.
Hai Dang's avatar
Hai Dang committed
273
274
275
  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
276
  by rewrite (tmap_lookup_op_r _ _ _ _ VALID Eqtg).
Hai Dang's avatar
Hai Dang committed
277
278
Qed.

Hai Dang's avatar
Hai Dang committed
279
(** heaplet *)
Hai Dang's avatar
Hai Dang committed
280
Lemma to_heapR_valid h :  (to_heapR h).
Hai Dang's avatar
Hai Dang committed
281
Proof.
Hai Dang's avatar
Hai Dang committed
282
  intros l. rewrite /to_heapR lookup_fmap.
Hai Dang's avatar
Hai Dang committed
283
284
285
  destruct (h !! l) eqn:Eq; rewrite Eq //.
Qed.

Hai Dang's avatar
Hai Dang committed
286
287
Lemma to_heapR_lookup h l s :
  to_heapR h !! l  Some (to_agree s)  h !! l = Some s.
Hai Dang's avatar
Hai Dang committed
288
Proof.
Hai Dang's avatar
Hai Dang committed
289
  rewrite /to_heapR lookup_fmap.
Hai Dang's avatar
Hai Dang committed
290
291
  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
292
Qed.
Hai Dang's avatar
Hai Dang committed
293

Hai Dang's avatar
Hai Dang committed
294
295
296
297
298
299
300
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
301
302
(** lmap *)
Lemma lmap_lookup_op_r (lm1 lm2 : lmapUR) (VALID:  (lm1  lm2)) l ls :
Hai Dang's avatar
Hai Dang committed
303
  lm2 !! l  Some ls  ((lm1  lm2) !! l : optionR tagR)  Some ls.
Hai Dang's avatar
Hai Dang committed
304
305
306
307
Proof.
  intros Eq. move : (VALID l). rewrite lookup_op Eq.
  destruct (lm1 !! l) as [ls2|] eqn:Eql; rewrite Eql; [|by rewrite left_id].
  rewrite -Some_op.
Hai Dang's avatar
Hai Dang committed
308
  destruct ls, ls2; simpl; try inversion 1.
Hai Dang's avatar
Hai Dang committed
309
310
Qed.

311
312
313
314
315
316
Lemma lmap_lookup_op_l (lm1 lm2 : lmapUR) (VALID:  (lm1  lm2)) l ls :
  lm1 !! l  Some ls  (lm1  lm2) !! l  Some ls.
Proof.
  intros Eq. move : (VALID l). rewrite lookup_op Eq.
  destruct (lm2 !! l) as [ls2|] eqn:Eql; rewrite Eql; [|by rewrite right_id].
  rewrite -Some_op.
Hai Dang's avatar
Hai Dang committed
317
  destruct ls, ls2; simpl; try inversion 1.
318
319
Qed.

Hai Dang's avatar
Hai Dang committed
320
321
322
Lemma lmap_lookup_op_included (lm1 lm2 : lmapUR) (l: loc) (t: ptr_id)
  (VALID:  lm2) (INCL: (lm1 : lmapUR)  (lm2 : lmapUR)):
  (lm1 !! l : optionR tagR)  Some $ to_tagR t  (lm2 !! l : optionR tagR)  Some $ to_tagR t.
323
Proof.
Hai Dang's avatar
Hai Dang committed
324
  destruct INCL as [cm' Eq]. rewrite Eq. apply lmap_lookup_op_l. by rewrite -Eq.
325
326
Qed.

Hai Dang's avatar
Hai Dang committed
327
328
Lemma lmap_exclusive_2 t1 t2 (c: tagR) :
  Some c  Some (to_tagR t1)  Some (to_tagR t2)  False.
329
Proof.
Hai Dang's avatar
Hai Dang committed
330
331
  rewrite -Some_op. intros Eq%Some_equiv_inj.
  destruct c; inversion Eq.
332
333
Qed.

Hai Dang's avatar
Hai Dang committed
334
335
336
337
338
Lemma tagR_valid (ls: tagR) : valid ls   t, ls = to_tagR t.
Proof. destruct ls as [t|]; simpl; [|done]. naive_solver. Qed.

Lemma lmap_exclusive_eq_l t (c: tagR) (mb: optionR tagR) :
  Some c  mb  Some (to_tagR t)  c  to_tagR t.
Hai Dang's avatar
Hai Dang committed
339
Proof.
Hai Dang's avatar
Hai Dang committed
340
341
342
343
  intros Eq.
  have VALID: valid (Some c  mb) by rewrite Eq. move :Eq.
  destruct c, mb as [[]|]; simplify_eq; try done.
  rewrite right_id. by intros ?%Some_equiv_inj.
Hai Dang's avatar
Hai Dang committed
344
345
Qed.

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

(** Resources that we own. *)

Ralf Jung's avatar
Ralf Jung committed
362
Definition res_tag tg tk (h: heaplet) : resUR :=
Ralf Jung's avatar
Ralf Jung committed
363
364
  ({[tg := (to_tagKindR tk, to_agree <$> h)]}, ε, ε).

Ralf Jung's avatar
Ralf Jung committed
365
Definition res_callState (c: call_id) (cs: call_state) : resUR :=
Ralf Jung's avatar
Ralf Jung committed
366
  (ε, {[c := to_callStateR cs]}, ε).
Hai Dang's avatar
Hai Dang committed
367

Hai Dang's avatar
Hai Dang committed
368
369

Fixpoint write_local (l:loc) (n:nat) (t: ptr_id) (ls: lmap) : lmap :=
370
371
  match n with
  | O => ls
Hai Dang's avatar
Hai Dang committed
372
  | S n => <[l := t]>(write_local (l + 1) n t ls)
373
374
  end.

Hai Dang's avatar
Hai Dang committed
375
Definition res_loc l n t : resUR := (ε, fmap to_tagR (write_local l n t )).
Hai Dang's avatar
Hai Dang committed
376

Hai Dang's avatar
Hai Dang committed
377
378
Definition res_mapsto (l:loc) (v: value) (t: ptr_id) : resUR :=
  res_loc l (length v) t  res_tag t tkUnique (write_mem l v ).
Hai Dang's avatar
Hai Dang committed
379
380
381
382
383
384
385
386
387

(** res_tag *)
Lemma res_tag_alloc_local_update lsf t k h (FRESH: lsf.(rtm) !! t = None) :
  (lsf, ε) ~l~> (lsf  res_tag t k h, res_tag t k h).
Proof.
  destruct lsf as [[tm cm] lm]. rewrite 2!pair_op right_id right_id.
  apply prod_local_update_1, prod_local_update_1.
  rewrite cmra_comm -insert_singleton_op //.
  apply alloc_singleton_local_update; [done|].
Hai Dang's avatar
Hai Dang committed
388
  split. by destruct k. apply to_heapR_valid.
Hai Dang's avatar
Hai Dang committed
389
Qed.
390

Hai Dang's avatar
Hai Dang committed
391
(** res_mapsto *)
Hai Dang's avatar
Hai Dang committed
392
Lemma write_local_lookup l n t ls :
393
  ( (i: nat), (i < n)%nat 
Hai Dang's avatar
Hai Dang committed
394
    write_local l n t ls !! (l + i) = Some t) 
395
  ( (l': loc), ( (i: nat), (i < n)%nat  l'  l + i) 
Hai Dang's avatar
Hai Dang committed
396
    write_local l n t ls !! l' = ls !! l').
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
Proof.
  revert l ls. induction n as [|n IH]; intros l ls; simpl.
  { split; intros ??; [lia|done]. }
  destruct (IH (l + 1) ls) as [IH1 IH2].
  split.
  - intros i Lt. destruct i as [|i].
    + rewrite shift_loc_0_nat lookup_insert //.
    + have Eql: l + S i = (l + 1) + i.
      { rewrite shift_loc_assoc. f_equal. lia. }
      rewrite lookup_insert_ne.
      * rewrite Eql. destruct (IH (l + 1) ls) as [IH' _].
        apply IH'; lia.
      * rewrite -{1}(shift_loc_0_nat l). intros ?%shift_loc_inj. lia.
  - intros l' Lt. rewrite lookup_insert_ne.
    + apply IH2. intros i Lt'.
      rewrite (_: (l + 1) + i = l + S i); last first.
      { rewrite shift_loc_assoc. f_equal. lia. }
      apply Lt. lia.
    + specialize (Lt O ltac:(lia)). by rewrite shift_loc_0_nat in Lt.
Qed.

Hai Dang's avatar
Hai Dang committed
418
419
420
Lemma write_local_lookup_case l n t ls :
   l' t', write_local l n t ls !! l' = Some t' 
  ls !! l' = Some t'  ( i : nat, (i < n)%nat  l'  l + i) 
421
422
   i, (0  i < n)  l' = l + i.
Proof.
Hai Dang's avatar
Hai Dang committed
423
424
  destruct (write_local_lookup l n t ls) as [EQ1 EQ2].
  intros l1 t1s1 Eq'.
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
  case (decide (l1.1 = l.1)) => [Eql|NEql];
    [case (decide (l.2  l1.2 < l.2 + n)) => [[Le Lt]|NIN]|].
  - have Eql2: l1 = l + Z.of_nat (Z.to_nat (l1.2 - l.2)). {
      destruct l, l1. move : Eql Le => /= -> ?.
      rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
    right. rewrite Eql2. eexists; split; [|done].
    rewrite Eql2 /= in Lt. lia.
  - left.
    have ?:  i : nat, (i < n)%nat  l1  l + i.
    { intros i Lt Eq3. apply NIN. rewrite Eq3 /=. lia. }
     rewrite EQ2 // in Eq'.
  - left.
    have ?:  i : nat, (i < n)%nat  l1  l + i.
    { intros i Lt Eq3. apply NEql. by rewrite Eq3. }
    rewrite EQ2 // in Eq'.
Qed.

Hai Dang's avatar
Hai Dang committed
442
443
444
445
446
Lemma res_mapsto_llookup l v t :
  ( (i: nat), (i < length v)%nat 
    (res_mapsto l v t).(rlm) !! (l + i) = Some $ to_tagR t) 
  ( (l': loc), ( (i: nat), (i < length v)%nat  l'  l + i) 
    (res_mapsto l v t).(rlm) !! l' = None).
447
Proof.
Hai Dang's avatar
Hai Dang committed
448
449
450
  destruct (write_local_lookup l (length v) t ) as [EQ1 EQ2]. split.
  - intros i Lti. by rewrite /= right_id lookup_fmap (EQ1 _ Lti).
  - intros l' NEQ. by rewrite /= right_id lookup_fmap (EQ2 _ NEQ).
451
452
Qed.

Hai Dang's avatar
Hai Dang committed
453
454
455
Lemma res_mapsto_llookup_case l v t :
   l' t', ((res_mapsto l v t).(rlm) !! l' : optionR tagR)  Some t' 
  t' = to_tagR t   i, (0  i < length v)  l' = l + i.
456
Proof.
Hai Dang's avatar
Hai Dang committed
457
458
459
460
  intros l' t' Eq'. apply leibniz_equiv_iff in Eq'.
  move : Eq'. rewrite /= right_id lookup_fmap.
  destruct (write_local l (length v) t  !! l')
    as [t1|] eqn:Eql'; rewrite Eql'; [|done].
461
  simpl. intros. simplify_eq.
Hai Dang's avatar
Hai Dang committed
462
  destruct (write_local_lookup_case _ _ _ _ _ _ Eql') as [[]|Eq']; [done|].
463
  destruct Eq' as [i [[? Lti] Eqi]].
Hai Dang's avatar
Hai Dang committed
464
465
  have Lti': (Z.to_nat i < length v)%nat by rewrite Nat2Z.inj_lt Z2Nat.id.
  destruct (write_local_lookup l (length v) t ) as [EQ _].
466
467
468
469
  specialize (EQ _ Lti'). rewrite Z2Nat.id // -Eqi Eql' in EQ. simplify_eq.
  naive_solver.
Qed.

Hai Dang's avatar
Hai Dang committed
470
471
472
473
474
475
476
477
Lemma res_mapsto_llookup_1 l v t (LEN: (0 < length v)%nat) :
  ((res_mapsto l v t).(rlm) !! l : optionR tagR)  Some (to_tagR t).
Proof.
  rewrite lookup_op /= lookup_empty right_id lookup_fmap.
  destruct (length v); [lia|].
  rewrite /= lookup_insert //.
Qed.

Hai Dang's avatar
Hai Dang committed
478
479
480
481
Lemma res_mapsto_tlookup l v (t: ptr_id) :
  (res_mapsto l v t).(rtm) !! t 
    Some (to_tagKindR tkUnique, to_agree <$> (write_mem l v )).
Proof. by rewrite lookup_op /= lookup_empty left_id lookup_insert. Qed.
482

Hai Dang's avatar
Hai Dang committed
483
484
485
486
487
488
Lemma res_mapsto_tlookup_ne l v (t t': ptr_id) (NEQ: t'  t) :
  (res_mapsto l v t).(rtm) !! t'  None.
Proof. by rewrite lookup_op /= lookup_empty left_id lookup_insert_ne. Qed.

Lemma write_local_plus1 l n t :
  write_local (l + 1) n t  !! l = None.
489
Proof.
Hai Dang's avatar
Hai Dang committed
490
  destruct (write_local_lookup (l + 1) n t ) as [_ EQ].
491
492
493
494
  rewrite EQ //. intros ??. rewrite shift_loc_assoc -{1}(shift_loc_0 l).
  intros ?%shift_loc_inj. lia.
Qed.

Hai Dang's avatar
Hai Dang committed
495
496
497
Lemma write_local_res_S l n t :
  (to_tagR <$> write_local l (S n) t  : lmapUR) 
  ({[l := to_tagR t]}  (to_tagR <$> write_local (l + 1) n t ) : lmapUR).
498
Proof.
Hai Dang's avatar
Hai Dang committed
499
500
  rewrite /= fmap_insert /= insert_singleton_op //.
  rewrite lookup_fmap write_local_plus1 //.
501
502
Qed.

Hai Dang's avatar
Hai Dang committed
503
504
Lemma write_local_mem_dom l n t :
  dom (gset loc) (write_local l n t )  dom (gset loc) (init_mem l n ).
Hai Dang's avatar
Hai Dang committed
505
Proof.
Hai Dang's avatar
Hai Dang committed
506
507
  revert l. induction n as [|n IH]; simpl; intros l; [done|].
  rewrite /= 2!dom_insert IH //.
Hai Dang's avatar
Hai Dang committed
508
509
Qed.

Hai Dang's avatar
Hai Dang committed
510
Lemma write_local_res_local_update lsf l n t:
511
  ( i, (i < n)%nat  lsf !! (l + i) = None) 
Hai Dang's avatar
Hai Dang committed
512
513
  (lsf, ε) ~l~>
  (lsf  (to_tagR <$> write_local l n t ) : lmapUR, to_tagR <$> write_local l n t  : lmapUR).
514
515
516
Proof.
  revert l lsf.
  induction n as [|n IH]; intros l lsf HL.
Hai Dang's avatar
Hai Dang committed
517
518
519
  - rewrite /= fmap_empty right_id //.
  - rewrite /= write_local_res_S.
    rewrite (cmra_comm ({[l := to_tagR t]} : lmapUR) (to_tagR <$> write_local _ _ _ _)).
520
521
522
523
524
    rewrite cmra_assoc.
    etrans.
    + apply (IH (l + 1)).
      intros i Lt. rewrite shift_loc_assoc -(Nat2Z.inj_add 1).
      apply HL. lia.
Hai Dang's avatar
Hai Dang committed
525
526
527
528
    + have NEQ1: write_local (l + 1) n t  !! l = None.
      { rewrite {1}/write_local write_local_plus1 //. }
      have ?: (lsf  (to_tagR <$> write_local (l + 1) n t )) !! l = None.
      { rewrite lookup_op lookup_fmap NEQ1 right_id_L.
529
        specialize (HL O). rewrite shift_loc_0_nat in HL. apply HL. lia. }
Hai Dang's avatar
Hai Dang committed
530
531
532
      rewrite 2!(cmra_comm _  {[l := _]})
              -insert_singleton_op // -insert_singleton_op;
        [|by rewrite lookup_fmap NEQ1].
533
534
      by apply alloc_local_update.
Qed.
Hai Dang's avatar
Hai Dang committed
535

Hai Dang's avatar
Hai Dang committed
536
537
538
539
540

Lemma res_mapsto_local_alloc_local_update lsf l v t:
  lsf.(rtm) !! t = None 
  ( i, (i < length v)%nat  lsf.(rlm) !! (l + i) = None) 
  (lsf, ε) ~l~> (lsf  res_mapsto l v t, res_mapsto l v t).
Hai Dang's avatar
Hai Dang committed
541
Proof.
Hai Dang's avatar
Hai Dang committed
542
543
544
545
546
  intros FRESH1 FRESH2. destruct lsf as [[tm cm] lm].
  rewrite /res_mapsto (cmra_comm (res_loc _ _ _)).
  etrans. by apply (res_tag_alloc_local_update _ t tkUnique (write_mem l v )).
  rewrite !pair_op !right_id left_id /=. apply prod_local_update_2.
  by apply write_local_res_local_update.
Hai Dang's avatar
Hai Dang committed
547
548
Qed.

Hai Dang's avatar
Hai Dang committed
549
550
551
552
Lemma res_mapsto_1_insert_local_update (r: resUR) (l: loc) s1 s2 (t: ptr_id)
  (NONE1: r.(rlm) !! l = None) (NONE2: r.(rtm) !! t = None):
  (r  res_mapsto l [s1] t, res_mapsto l [s1] t) ~l~>
  (r  res_mapsto l [s2] t, res_mapsto l [s2] t).
Hai Dang's avatar
Hai Dang committed
553
Proof.
Hai Dang's avatar
Hai Dang committed
554
555
556
557
558
559
560
561
562
563
  intros. destruct r as [[tm cm] lm].
  rewrite !pair_op !right_id /= !left_id /=.
  do 2 (rewrite (cmra_comm tm) -insert_singleton_op; [|done]). etrans.
  - apply prod_local_update_1, prod_local_update_1.
    rewrite /= left_id.
    instantiate (1:= {[t := (Cinl (Excl ()), to_agree <$> <[l:=s2]> )]}).
    eapply (singleton_local_update (<[t := _]> tm : tmapUR)). by rewrite lookup_insert.
    apply exclusive_local_update. split; [done|apply to_heapR_valid].
  - rewrite /res_mapsto !right_id_L /= insert_insert /=.
    rewrite /res_loc /res_tag /= pair_op left_id right_id //.
Hai Dang's avatar
Hai Dang committed
564
Qed.