array.v 12.4 KB
Newer Older
1
From stdpp Require Import fin_maps.
2
From iris.bi Require Import lib.fractional.
3
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
4
5
6
7
From iris.heap_lang Require Export lifting.
From iris.heap_lang Require Import tactics notation.
Set Default Proof Using "Type".

Ralf Jung's avatar
Ralf Jung committed
8
9
(** This file defines the [array] connective, a version of [mapsto] that works
with lists of values. It also contains array versions of the basic heap
10
operations of HeapLang. *)
Ralf Jung's avatar
Ralf Jung committed
11

12
13
14
15
16
Definition array `{!heapG Σ} (l : loc) (q : Qp) (vs : list val) : iProp Σ :=
  ([ list] i  v  vs, (l + i) {q} v)%I.
Notation "l ↦∗{ q } vs" := (array l q vs)
  (at level 20, q at level 50, format "l  ↦∗{ q }  vs") : bi_scope.
Notation "l ↦∗ vs" := (array l 1 vs)
Ralf Jung's avatar
Ralf Jung committed
17
18
  (at level 20, format "l  ↦∗  vs") : bi_scope.

19
20
21
(** We have [FromSep] and [IntoSep] instances to split the fraction (via the
[AsFractional] instance below), but not for splitting the list, as that would
lead to overlapping instances. *)
Ralf Jung's avatar
Ralf Jung committed
22

Ralf Jung's avatar
Ralf Jung committed
23
24
25
26
27
28
29
Section lifting.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types σ : state.
Implicit Types v : val.
Implicit Types vs : list val.
30
Implicit Types q : Qp.
Ralf Jung's avatar
Ralf Jung committed
31
32
33
Implicit Types l : loc.
Implicit Types sz off : nat.

34
Global Instance array_timeless l q vs : Timeless (array l q vs) := _.
Ralf Jung's avatar
Ralf Jung committed
35

36
37
38
39
40
41
Global Instance array_fractional l vs : Fractional (λ q, l ↦∗{q} vs)%I := _.
Global Instance array_as_fractional l q vs :
  AsFractional (l ↦∗{q} vs) (λ q, l ↦∗{q} vs)%I q.
Proof. split; done || apply _. Qed.

Lemma array_nil l q : l ↦∗{q} []  emp.
Ralf Jung's avatar
Ralf Jung committed
42
43
Proof. by rewrite /array. Qed.

44
Lemma array_singleton l q v : l ↦∗{q} [v]  l {q} v.
Ralf Jung's avatar
Ralf Jung committed
45
46
Proof. by rewrite /array /= right_id loc_add_0. Qed.

47
48
Lemma array_app l q vs ws :
  l ↦∗{q} (vs ++ ws)  l ↦∗{q} vs  (l + length vs) ↦∗{q} ws.
Ralf Jung's avatar
Ralf Jung committed
49
50
51
52
53
54
Proof.
  rewrite /array big_sepL_app.
  setoid_rewrite Nat2Z.inj_add.
  by setoid_rewrite loc_add_assoc.
Qed.

55
Lemma array_cons l q v vs : l ↦∗{q} (v :: vs)  l {q} v  (l + 1) ↦∗{q} vs.
Ralf Jung's avatar
Ralf Jung committed
56
57
58
59
60
61
62
Proof.
  rewrite /array big_sepL_cons loc_add_0.
  setoid_rewrite loc_add_assoc.
  setoid_rewrite Nat2Z.inj_succ.
  by setoid_rewrite Z.add_1_l.
Qed.

63
64
65
66
67
Global Instance array_cons_frame l q v vs R Q :
  Frame false R (l {q} v  (l + 1) ↦∗{q} vs) Q 
  Frame false R (l ↦∗{q} (v :: vs)) Q.
Proof. by rewrite /Frame array_cons. Qed.

68
Lemma update_array l q vs off v :
Ralf Jung's avatar
Ralf Jung committed
69
  vs !! off = Some v 
70
  l ↦∗{q} vs - ((l + off) {q} v   v', (l + off) {q} v' - l ↦∗{q} <[off:=v']>vs).
Ralf Jung's avatar
Ralf Jung committed
71
72
Proof.
  iIntros (Hlookup) "Hl".
73
  rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
Ralf Jung's avatar
Ralf Jung committed
74
75
76
77
78
79
80
  iDestruct (array_app with "Hl") as "[Hl1 Hl]".
  iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
  assert (off < length vs)%nat as H by (apply lookup_lt_is_Some; by eexists).
  rewrite take_length min_l; last by lia. iFrame "Hl2".
  iIntros (w) "Hl2".
  clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
  { apply list_lookup_insert. lia. }
81
  rewrite -[in (l ↦∗{_} <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
Ralf Jung's avatar
Ralf Jung committed
82
83
84
85
86
  iApply array_app. rewrite take_insert; last by lia. iFrame.
  iApply array_cons. rewrite take_length min_l; last by lia. iFrame.
  rewrite drop_insert; last by lia. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
87
(** * Rules for allocation *)
88
89
90
Lemma mapsto_seq_array l q v n :
  ([ list] i  seq 0 n, (l + (i : nat)) {q} v) -
  l ↦∗{q} replicate n v.
Ralf Jung's avatar
Ralf Jung committed
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
Proof.
  rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
  { done. }
  iIntros "[$ Hl]". rewrite -fmap_seq big_sepL_fmap.
  setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
  setoid_rewrite <-loc_add_assoc. iApply "IH". done.
Qed.

Lemma twp_allocN s E v n :
  0 < n 
  [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v 
         [ list] i  seq 0 (Z.to_nat n), meta_token (l + (i : nat))  }]].
Proof.
  iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN_seq; [done..|].
  iIntros (l) "Hlm". iApply "HΦ".
  iDestruct (big_sepL_sep with "Hlm") as "[Hl $]".
  by iApply mapsto_seq_array.
Qed.
110
Lemma wp_allocN s E v n :
Ralf Jung's avatar
Ralf Jung committed
111
  0 < n 
112
113
  {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v 
Ralf Jung's avatar
Ralf Jung committed
114
115
         [ list] i  seq 0 (Z.to_nat n), meta_token (l + (i : nat))  }}}.
Proof.
116
117
  iIntros (? Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
  iApply twp_allocN; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
118
Qed.
119

Ralf Jung's avatar
Ralf Jung committed
120
121
122
123
124
125
126
127
128
129
Lemma twp_allocN_vec s E v n :
  0 < n 
  [[{ True }]]
    AllocN #n v @ s ; E
  [[{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v 
         [ list] i  seq 0 (Z.to_nat n), meta_token (l + (i : nat))  }]].
Proof.
  iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN; [ lia | done | .. ].
  iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
Qed.
130
131
132
133
134
135
Lemma wp_allocN_vec s E v n :
  0 < n 
  {{{ True }}}
    AllocN #n v @ s ; E
  {{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v 
         [ list] i  seq 0 (Z.to_nat n), meta_token (l + (i : nat))  }}}.
Ralf Jung's avatar
Ralf Jung committed
136
Proof.
137
138
  iIntros (? Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
  iApply twp_allocN_vec; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
139
Qed.
140

Robbert Krebbers's avatar
Robbert Krebbers committed
141
(** * Rules for accessing array elements *)
142
Lemma twp_load_offset s E l q off vs v :
Dan Frumin's avatar
Dan Frumin committed
143
  vs !! off = Some v 
144
  [[{ l ↦∗{q} vs }]] ! #(l + off) @ s; E [[{ RET v; l ↦∗{q} vs }]].
Dan Frumin's avatar
Dan Frumin committed
145
146
Proof.
  iIntros (Hlookup Φ) "Hl HΦ".
147
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
Dan Frumin's avatar
Dan Frumin committed
148
149
150
151
  iApply (twp_load with "Hl1"). iIntros "Hl1". iApply "HΦ".
  iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
  iApply "Hl2". iApply "Hl1".
Qed.
152
153
154
155
156
157
158
Lemma wp_load_offset s E l q off vs v :
  vs !! off = Some v 
  {{{  l ↦∗{q} vs }}} ! #(l + off) @ s; E {{{ RET v; l ↦∗{q} vs }}}.
Proof.
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_load_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Dan Frumin's avatar
Dan Frumin committed
159

160
161
Lemma twp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) :
  [[{ l ↦∗{q} vs }]] ! #(l + off) @ s; E [[{ RET vs !!! off; l ↦∗{q} vs }]].
Dan Frumin's avatar
Dan Frumin committed
162
Proof. apply twp_load_offset. by apply vlookup_lookup. Qed.
163
164
165
Lemma wp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) :
  {{{  l ↦∗{q} vs }}} ! #(l + off) @ s; E {{{ RET vs !!! off; l ↦∗{q} vs }}}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
Dan Frumin's avatar
Dan Frumin committed
166
167
168
169
170
171

Lemma twp_store_offset s E l off vs v :
  is_Some (vs !! off) 
  [[{ l ↦∗ vs }]] #(l + off) <- v @ s; E [[{ RET #(); l ↦∗ <[off:=v]> vs }]].
Proof.
  iIntros ([w Hlookup] Φ) "Hl HΦ".
172
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
Dan Frumin's avatar
Dan Frumin committed
173
174
175
  iApply (twp_store with "Hl1"). iIntros "Hl1".
  iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
176
177
178
Lemma wp_store_offset s E l off vs v :
  is_Some (vs !! off) 
  {{{  l ↦∗ vs }}} #(l + off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
Ralf Jung's avatar
Ralf Jung committed
179
Proof.
180
181
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_store_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
182
Qed.
183

Dan Frumin's avatar
Dan Frumin committed
184
185
186
187
188
189
Lemma twp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
  [[{ l ↦∗ vs }]] #(l + off) <- v @ s; E [[{ RET #(); l ↦∗ vinsert off v vs }]].
Proof.
  setoid_rewrite vec_to_list_insert. apply twp_store_offset.
  eexists. by apply vlookup_lookup.
Qed.
190
191
Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
  {{{  l ↦∗ vs }}} #(l + off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
Ralf Jung's avatar
Ralf Jung committed
192
Proof.
193
194
  iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_store_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
195
Qed.
196

Dan Frumin's avatar
Dan Frumin committed
197
198
199
200
201
202
203
204
205
Lemma twp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
  vs !! off = Some v' 
  v' = v1 
  vals_compare_safe v' v1 
  [[{ l ↦∗ vs }]]
    CmpXchg #(l + off) v1 v2 @ s; E
  [[{ RET (v', #true); l ↦∗ <[off:=v2]> vs }]].
Proof.
  iIntros (Hlookup ?? Φ) "Hl HΦ".
206
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
Dan Frumin's avatar
Dan Frumin committed
207
208
209
  iApply (twp_cmpxchg_suc with "Hl1"); [done..|].
  iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
210
211
212
213
Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
  vs !! off = Some v' 
  v' = v1 
  vals_compare_safe v' v1 
Ralf Jung's avatar
Ralf Jung committed
214
215
  {{{  l ↦∗ vs }}}
    CmpXchg #(l + off) v1 v2 @ s; E
216
  {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
Ralf Jung's avatar
Ralf Jung committed
217
Proof.
218
219
  iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_suc_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
220
Qed.
221

Dan Frumin's avatar
Dan Frumin committed
222
223
224
225
226
227
228
229
230
231
Lemma twp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off = v1 
  vals_compare_safe (vs !!! off) v1 
  [[{ l ↦∗ vs }]]
    CmpXchg #(l + off) v1 v2 @ s; E
  [[{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }]].
Proof.
  intros. setoid_rewrite vec_to_list_insert. eapply twp_cmpxchg_suc_offset=> //.
  by apply vlookup_lookup.
Qed.
232
233
234
235
Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off = v1 
  vals_compare_safe (vs !!! off) v1 
  {{{  l ↦∗ vs }}}
Ralf Jung's avatar
Ralf Jung committed
236
    CmpXchg #(l + off) v1 v2 @ s; E
237
  {{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
Ralf Jung's avatar
Ralf Jung committed
238
Proof.
239
240
  iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_suc_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
241
Qed.
242

243
Lemma twp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 :
Dan Frumin's avatar
Dan Frumin committed
244
245
246
  vs !! off = Some v0 
  v0  v1 
  vals_compare_safe v0 v1 
247
  [[{ l ↦∗{q} vs }]]
Dan Frumin's avatar
Dan Frumin committed
248
    CmpXchg #(l + off) v1 v2 @ s; E
249
  [[{ RET (v0, #false); l ↦∗{q} vs }]].
Dan Frumin's avatar
Dan Frumin committed
250
251
Proof.
  iIntros (Hlookup HNEq Hcmp Φ) "Hl HΦ".
252
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
Dan Frumin's avatar
Dan Frumin committed
253
254
255
256
257
  iApply (twp_cmpxchg_fail with "Hl1"); first done.
  { destruct Hcmp; by [ left | right ]. }
  iIntros "Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2".
  rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
Qed.
258
259
260
261
Lemma wp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 :
  vs !! off = Some v0 
  v0  v1 
  vals_compare_safe v0 v1 
262
  {{{  l ↦∗{q} vs }}}
Ralf Jung's avatar
Ralf Jung committed
263
    CmpXchg #(l + off) v1 v2 @ s; E
264
265
266
267
268
269
  {{{ RET (v0, #false); l ↦∗{q} vs }}}.
Proof.
  iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_fail_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.

270
Lemma twp_cmpxchg_fail_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) v1 v2 :
Dan Frumin's avatar
Dan Frumin committed
271
272
  vs !!! off  v1 
  vals_compare_safe (vs !!! off) v1 
273
  [[{ l ↦∗{q} vs }]]
Dan Frumin's avatar
Dan Frumin committed
274
    CmpXchg #(l + off) v1 v2 @ s; E
275
  [[{ RET (vs !!! off, #false); l ↦∗{q} vs }]].
Dan Frumin's avatar
Dan Frumin committed
276
Proof. intros. eapply twp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
277
278
279
280
281
282
283
Lemma wp_cmpxchg_fail_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off  v1 
  vals_compare_safe (vs !!! off) v1 
  {{{  l ↦∗{q} vs }}}
    CmpXchg #(l + off) v1 v2 @ s; E
  {{{ RET (vs !!! off, #false); l ↦∗{q} vs }}}.
Proof. intros. eapply wp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
Ralf Jung's avatar
Ralf Jung committed
284

Dan Frumin's avatar
Dan Frumin committed
285
286
287
288
289
290
Lemma twp_faa_offset s E l off vs (i1 i2 : Z) :
  vs !! off = Some #i1 
  [[{ l ↦∗ vs }]] FAA #(l + off) #i2 @ s; E
  [[{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }]].
Proof.
  iIntros (Hlookup Φ) "Hl HΦ".
291
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
Dan Frumin's avatar
Dan Frumin committed
292
293
294
  iApply (twp_faa with "Hl1").
  iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
295
296
Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
  vs !! off = Some #i1 
Ralf Jung's avatar
Ralf Jung committed
297
  {{{  l ↦∗ vs }}} FAA #(l + off) #i2 @ s; E
298
  {{{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }}}.
Ralf Jung's avatar
Ralf Jung committed
299
Proof.
300
301
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_faa_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
302
Qed.
303

Dan Frumin's avatar
Dan Frumin committed
304
305
306
307
308
309
310
311
Lemma twp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
  vs !!! off = #i1 
  [[{ l ↦∗ vs }]] FAA #(l + off) #i2 @ s; E
  [[{ RET LitV (LitInt i1); l ↦∗ vinsert off #(i1 + i2) vs }]].
Proof.
  intros. setoid_rewrite vec_to_list_insert. apply twp_faa_offset=> //.
  by apply vlookup_lookup.
Qed.
312
313
314
315
316
317
318
319
Lemma wp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
  vs !!! off = #i1 
  {{{  l ↦∗ vs }}} FAA #(l + off) #i2 @ s; E
  {{{ RET LitV (LitInt i1); l ↦∗ vinsert off #(i1 + i2) vs }}}.
Proof.
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_faa_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Ralf Jung's avatar
Ralf Jung committed
320
End lifting.
321
322

Typeclasses Opaque array.