heap.v 31.3 KB
Newer Older
1
From stdpp Require Import gmap list.
Michael Sammler's avatar
Michael Sammler committed
2
From refinedc.lang Require Export base byte layout int_type loc val struct.
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
Set Default Proof Using "Type".
Open Scope Z_scope.

(** * Heap and allocations. *)

(** ** Representation of the heap. *)

Inductive lock_state := WSt | RSt (n : nat).

Record heap_cell := HeapCell {
  hc_alloc_id   : alloc_id;   (** Allocation owning the cell. *)
  hc_lock_state : lock_state; (** Datarace detection stuff. *)
  hc_value      : mbyte;      (** Byte value. *)
}.

Definition heap := gmap addr heap_cell.

(** ** Functions and predicates for manipulating the heap. *)

(** Predicate stating that the heap [h] contains value [v] at address [a],
and that every cell involved has an allocation identifier and a lock state
that satisfy [Paid] and [Plk] respectively. *)
Fixpoint heap_lookup (a : addr) (v : val) (Paid : alloc_id  Prop)
                     (Plk : lock_state  Prop) (h : heap) : Prop :=
  match v with
  | []     => True
  | b :: v => ( aid lk, h !! a = Some (HeapCell aid lk b)  Paid aid  Plk lk) 
              heap_lookup (Z.succ a) v Paid Plk h
  end.

(** Function writing value [v] at address [a] in heap [h]. For all involved
cells in the resulting heap, an allocation id and lock state is built using
functions [faid] and [flk] respectively. These functions receive as input
the previous value of the field (if the cell previously existed in [h]). *)
Fixpoint heap_update (a : addr) (v : val) (faid : option alloc_id  alloc_id)
                     (flk : option lock_state  lock_state) (h : heap) : heap :=
  match v with
  | []     => h
  | b :: v => let update m :=
                Some {|
                  hc_alloc_id   := faid (hc_alloc_id <$> m);
                  hc_lock_state := flk (hc_lock_state <$> m);
                  hc_value      := b;
                |}
              in
              partial_alter update a (heap_update (Z.succ a) v faid flk h)
  end.

Definition heap_lookup_loc (l : loc) (v : val) (Plk : lock_state  Prop)
                           (h : heap) : Prop :=
Michael Sammler's avatar
Michael Sammler committed
53
  heap_lookup l.2 v (λ aid, l.1 = ProvAlloc (Some aid)) Plk h.
54
55
56
57
58
59

Definition heap_alloc (a : addr) (v : val) (aid : alloc_id) (h : heap) : heap :=
  heap_update a v (λ _, aid) (λ _, RSt 0%nat) h.

Definition heap_at (l : loc) (ly : layout) (v : val) (Plk : lock_state  Prop)
                   (h : heap) : Prop :=
Michael Sammler's avatar
Michael Sammler committed
60
  ( aid, l.1 = ProvAlloc (Some aid))   l `has_layout_loc` ly  v `has_layout_val` ly 
61
62
  heap_lookup_loc l v Plk h.

Michael Sammler's avatar
Michael Sammler committed
63
64
Definition heap_upd (l : loc) v flk h :=
  heap_update l.2 v (default (default dummy_alloc_id (prov_alloc_id l.1))) flk h.
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88

(** Predicate stating that the [n] first bytes from address [a] in [h] have
not been allocated. *)
Definition heap_range_free (h : heap) (a : addr) (n : nat) : Prop :=
   a', a  a' < a + n  h !! a' = None.

(** Free [n] cells starting at [a] in [h]. *)
Fixpoint heap_free (a : addr) (n : nat) (h : heap) : heap :=
  match n with
  | O   => h
  | S n => delete a (heap_free (Z.succ a) n h)
  end.

(** ** Lemmas about the heap and related operations. *)

Lemma heap_lookup_inj_val a h v1 v2 Paid1 Paid2 Plk1 Plk2:
  length v1 = length v2 
  heap_lookup a v1 Paid1 Plk1 h  heap_lookup a v2 Paid2 Plk2 h  v1 = v2.
Proof.
  elim: v1 v2 a; first by move => [|??] //.
  move => ?? IH [|??] //= ? [?] [[?[?[??]]]?] [[?[?[??]]]?]; simplify_eq.
  f_equal. by apply: IH.
Qed.

Michael Sammler's avatar
Michael Sammler committed
89
90
91
92
93
94
95
96
97
98
Lemma heap_lookup_is_Some a p v Paid Plk h:
  heap_lookup a v Paid Plk h 
  a  p < a + length v 
  is_Some (h !! p).
Proof.
  elim: v a => /=; first lia. move => b v IH a [[aid [lk [Ha _]]] H] Hp.
  destruct (decide (p = a)) as [->|]; first naive_solver.
  apply (IH (Z.succ a)) => //. lia.
Qed.

99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
Lemma heap_update_ext h a v faid1 faid2 flk1 flk2:
  ( x, faid1 x = faid2 x)  ( x, flk1 x = flk2 x) 
  heap_update a v faid1 flk1 h = heap_update a v faid2 flk2 h.
Proof.
  move => Hext1 Hext2. elim: v a => //= ?? IH ?. rewrite IH.
  apply: partial_alter_ext => ??. by rewrite Hext1 Hext2.
Qed.

Lemma heap_update_lookup_not_in_range a1 a2 v faid flk h:
  a1 < a2  a2 + length v  a1 
  heap_update a2 v faid flk h !! a1 = h !! a1.
Proof.
  elim: v a1 a2 => // ?? IH ?? H.
  rewrite lookup_partial_alter_ne /=; first apply IH; move: H => [] /=; lia.
Qed.

Lemma heap_update_lookup_in_range a1 a2 v faid flk h:
  a2  a1 < a2 + length v 
  heap_update a2 v faid flk h !! a1 = Some {|
    hc_alloc_id := faid (hc_alloc_id <$> h !! a1);
    hc_lock_state := flk (hc_lock_state <$> h !! a1);
    hc_value := default MPoison (v !! (Z.to_nat (a1 - a2)));
  |}.
Proof.
  elim: v a1 a2.
  - move => /= a1 a2 [??]. exfalso. lia.
  - move => ?? IH a1 a2 [H1 H2]. destruct (decide (a1 = a2)) as [->|Hne].
    + rewrite lookup_partial_alter -/heap_update Z.sub_diag /=.
Michael Sammler's avatar
Michael Sammler committed
127
      rewrite heap_update_lookup_not_in_range; [done | lia].
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
    + rewrite lookup_partial_alter_ne // -/heap_update /= IH; last first.
      { rewrite /= in H2. lia. } do 3 f_equal.
      rewrite lookup_cons_ne_0; last lia. f_equal. lia.
Qed.

Lemma heap_free_delete h a1 a2 n :
  delete a1 (heap_free a2 n h) = heap_free a2 n (delete a1 h).
Proof. elim: n a2 => //= ? IH ?. by rewrite delete_commute IH. Qed.

Lemma heap_upd_ext h l v f1 f2:
  ( x, f1 x = f2 x)  heap_upd l v f1 h = heap_upd l v f2 h.
Proof. by apply heap_update_ext. Qed.

Lemma heap_at_inj_val l ly h v1 v2 Plk1 Plk2:
  heap_at l ly v1 Plk1 h  heap_at l ly v2 Plk2 h  v1 = v2.
Proof.
  move => [_[?[??]]] [_[?[??]]].
  apply: heap_lookup_inj_val => //. congruence.
Qed.

Lemma heap_lookup_loc_inj_val  l h v v' flk1 flk2 ly:
  v `has_layout_val` ly 
  heap_lookup_loc l v flk1 h  heap_at l ly v' flk2 h  v = v'.
Proof.
  move => ??[_[?[??]]]. apply: heap_lookup_inj_val => //. congruence.
Qed.

Lemma heap_upd_heap_at_id l v flk flk' h:
  heap_lookup_loc l v flk' h 
  ( st, flk (Some st) = st) 
  heap_upd l v flk h = h.
Proof.
  rewrite /heap_upd.
  elim: v l => // ?? IH ? [[?[?[H[H1 ?]]]]?] Hlookup /=.
  assert ( l, Z.succ l.2 = (l + 1).2) as -> by done.
  rewrite IH => //. apply: partial_alter_self_alt'.
  by rewrite H Hlookup H1 /=.
Qed.

Michael Sammler's avatar
Michael Sammler committed
167
Lemma heap_free_lookup_in_range a p (n : nat) h:
168
169
170
171
  a  p < a + n 
  heap_free a n h !! p = None.
Proof.
  elim: n a; first lia. move => n IH a [H1 H2] /=.
Michael Sammler's avatar
Michael Sammler committed
172
173
174
  rewrite lookup_delete_None.
  destruct (decide (a = p)) as [->|]; [by left|right].
  apply: IH. lia.
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
Qed.

Lemma heap_free_lookup_not_in_range a p (n : nat) h:
  ¬ (a  p < a + n) 
  heap_free a n h !! p = h !! p.
Proof.
  elim: n a => //= n IH a H.
  destruct (decide (a = p)) as [->|]; first lia.
  rewrite lookup_delete_ne; last done. apply IH. lia.
Qed.

(** ** Representation of allocations. *)

Record allocation :=
  Allocation {
    al_start : Z;    (* First valid address. *)
    al_len   : nat;  (* Number of allocated byte. *)
    al_alive : bool; (* Is the allocation still alive. *)
  }.

Definition al_end (al : allocation) : Z :=
  al_start al + al_len al.

Definition allocs := gmap alloc_id allocation.

Definition alloc_same_range (al1 al2 : allocation) : Prop :=
  al1.(al_start) = al2.(al_start)  al1.(al_len) = al2.(al_len).

Definition killed (al : allocation) : allocation :=
  {| al_start := al.(al_start); al_len := al.(al_len); al_alive := false; |}.

(** Smallest allocatable address (we reserve 0 for NULL). *)
Definition min_alloc_start : Z := 1.

(** Largest allocatable address (we never allocate the last byte to always
have valid one-past pointers. *)
Definition max_alloc_end : Z := 2 ^ (bytes_per_addr * bits_per_byte) - 2.

(** Predicate asserting that allocation [a] is in range of the allocatable
memory (e.g., does not contain NULL). *)
Definition allocation_in_range (al : allocation) : Prop :=
  min_alloc_start  al.(al_start)  al_end al  max_alloc_end.

Instance elem_of_alloc : ElemOf addr allocation :=
  λ a al, al.(al_start)  a < al_end al.

(** ** Representation of the state of the heap and allocation operations. *)

Record heap_state := {
  hs_heap   : heap;
  hs_allocs : allocs;
}.

Definition alloc_id_alive (aid : alloc_id) (st : heap_state) : Prop :=
   alloc, st.(hs_allocs) !! aid = Some alloc  alloc.(al_alive).

Definition block_alive (l : loc) (st : heap_state) : Prop :=
Michael Sammler's avatar
Michael Sammler committed
232
   aid, l.1 = ProvAlloc (Some aid)  alloc_id_alive aid st.
233
234
235
236
237
238

(** The address range between [l] and [l +ₗ n] (included) is in range of the
    allocation that contains [l]. Note that we consider the 1-past-the-end
    pointer to be in range of an allocation. *)
Definition heap_state_loc_in_bounds (l : loc) (n : nat) (st : heap_state) : Prop :=
   alloc_id al,
Michael Sammler's avatar
Michael Sammler committed
239
    l.1 = ProvAlloc (Some alloc_id) 
240
    st.(hs_allocs) !! alloc_id = Some al 
241
    allocation_in_range al 
242
243
244
    al.(al_start)  l.2 
    l.2 + n  al_end al.

Michael Sammler's avatar
Michael Sammler committed
245
246
247
248
Lemma heap_state_loc_in_bounds_has_alloc_id l n σ:
  heap_state_loc_in_bounds l n σ   aid, l.1 = ProvAlloc (Some aid).
Proof. rewrite /heap_state_loc_in_bounds. naive_solver. Qed.

249
250
251
252
253
(** Checks that the location [l] is inbounds of its allocation
(one-past-the-end is allowed) and this allocation is still alive *)
Definition valid_ptr (l : loc) (st : heap_state) : Prop :=
  block_alive l st  heap_state_loc_in_bounds l 0 st.

254
255
256
257
Lemma valid_ptr_in_allocation_range l σ:
  valid_ptr l σ  min_alloc_start  l.2  max_alloc_end.
Proof. move => [_][?][?][]?[]?[[]]???. lia. Qed.

Michael Sammler's avatar
Michael Sammler committed
258
259
260
261
Lemma valid_ptr_has_alloc_id l σ:
  valid_ptr l σ   aid, l.1 = ProvAlloc (Some aid).
Proof. rewrite /valid_ptr => ?. apply: heap_state_loc_in_bounds_has_alloc_id. naive_solver. Qed.

262
263
264
Definition addr_in_range_alloc (a : addr) (aid : alloc_id) (st : heap_state) : Prop :=
   alloc, st.(hs_allocs) !! aid = Some alloc  a  alloc.

265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
Global Instance allocation_eq_dec : EqDecision (allocation).
Proof. solve_decision. Qed.
Global Instance alloc_id_alive_dec aid st : Decision (alloc_id_alive aid st).
Proof.
  destruct (st.(hs_allocs) !! aid) as [alloc|] eqn: Haid.
  2: { right. move => [?[??]]. simplify_eq. }
  destruct (alloc.(al_alive)) eqn:?.
  - left. eexists _. naive_solver.
  - right. move => [?[??]]. destruct alloc; naive_solver.
Qed.
Global Instance block_alive_dec l st : Decision (block_alive l st).
Proof.
  destruct (l.1) as [| [aid|] |] eqn: Hl.
  1,3,4: try (right => -[?[??]]; destruct l; naive_solver).
  eapply (exists_dec_unique aid); [| apply _]. destruct l; naive_solver.
Qed.
Global Instance heap_state_loc_in_bounds_dec l n st : Decision (heap_state_loc_in_bounds l n st).
Proof.
  destruct (l.1) as [| [aid|] |] eqn: Hl.
  1,3,4: (right => -[?[??]]; destruct l; naive_solver).
  destruct (st.(hs_allocs) !! aid) as [al|] eqn:?.
  2: right => -[?[?[??]]]; destruct l; naive_solver.
  eapply (exists_dec_unique aid); [ destruct l; naive_solver|].
  eapply (exists_dec_unique al); [ destruct l; naive_solver|].
  apply _.
Qed.

Michael Sammler's avatar
Michael Sammler committed
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
(** ** Comparing pointers
  [heap_loc_eq l1 l2] returns whether two pointers compare equal.
  None means that the comparison is undefined. *)
Definition heap_loc_eq (l1 l2 : loc) (st : heap_state) : option bool :=
    (* null pointers are equal *)
  if bool_decide (l1 = NULL_loc  l2 = NULL_loc) then
    Some true
  (* function pointers are different from NULL pointers
   TODO: Check that the address of the function pointer is not 0?*)
  else if bool_decide ((l1 = NULL_loc  l2.1 = ProvFnPtr)  (l1.1 = ProvFnPtr  l2 = NULL_loc)) then
    Some false
  (* Allocations are different from NULL pointers. But the comparison
  is only defined if the location is in bounds of its allocation. *)
  else if bool_decide (l1 = NULL_loc) then
    guard (heap_state_loc_in_bounds l2 0 st);
    Some false
  else if bool_decide (l2 = NULL_loc) then
    guard (heap_state_loc_in_bounds l1 0 st);
    Some false
  (* Two function pointers compare equal if their address is equal. *)
  else if bool_decide (l1.1 = ProvFnPtr  l2.1 = ProvFnPtr) then
    Some (bool_decide (l1.2 = l2.2))
  else
  (* Two allocations can be compared if they are both alive and in
  bounds (it is ok if they have different provenances). Comparison
  compares the addresses. *)
    guard (valid_ptr l1 st);
    guard (valid_ptr l2 st);
    Some (bool_decide (l1.2 = l2.2)).

Lemma heap_loc_eq_symmetric l1 l2 st:
  heap_loc_eq l1 l2 st = heap_loc_eq l2 l1 st.
Proof.
  rewrite /heap_loc_eq.
  repeat case_bool_decide=> //; repeat case_option_guard => //; naive_solver.
Qed.

Lemma heap_loc_eq_NULL_NULL st:
  heap_loc_eq NULL_loc NULL_loc st = Some true.
Proof. rewrite /heap_loc_eq. case_bool_decide; naive_solver. Qed.

Lemma heap_loc_eq_alloc_NULL l st:
  heap_state_loc_in_bounds l 0 st 
  heap_loc_eq l NULL_loc st = Some false.
Proof.
  move => Hlib. move: (Hlib) => /heap_state_loc_in_bounds_has_alloc_id[??]. rewrite /heap_loc_eq.
  do 3 (case_bool_decide; [naive_solver|]). case_bool_decide => //. by rewrite option_guard_True.
Qed.

Lemma heap_loc_eq_fnptr_NULL l st:
  l.1 = ProvFnPtr 
  heap_loc_eq l NULL_loc st = Some false.
Proof.
  rewrite /heap_loc_eq => ?. do 3 (case_bool_decide; [naive_solver|]). naive_solver.
Qed.

Lemma heap_loc_eq_alloc_alloc l1 l2 st:
  valid_ptr l1 st 
  valid_ptr l2 st 
  heap_loc_eq l1 l2 st = Some (bool_decide (l1.2 = l2.2)).
Proof.
  move => Hv1 Hv2. move: (Hv1) => /valid_ptr_has_alloc_id[??]. move: (Hv2) => /valid_ptr_has_alloc_id[??].
  destruct l1, l2; simplify_eq/=.
  rewrite /heap_loc_eq.
  do 5 (case_bool_decide; [naive_solver|]).
  by rewrite !option_guard_True.
Qed.

360
361
362
363
364
365
366
367
368
(** ** Converting a value to a boolean (for conditionals). *)

Definition cast_to_bool (ot: op_type) (v: val) (st: heap_state) : option bool :=
  match ot with
  | IntOp it => val_to_Z v it = λ n, Some (bool_decide (n  0))
  | PtrOp    => val_to_loc v = λ l, heap_loc_eq l NULL_loc st = λ b, Some (negb b)
  | _        => None
  end.

Michael Sammler's avatar
Michael Sammler committed
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
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
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
(** ** MemCast: Transforming bytes read from memory.
  [mem_cast] is corresponds to the [abst] function in the VIP paper.

  [mem_cast] should only be called with length of [v] matching [ot] *)

Fixpoint mem_cast (v : val) (ot : op_type) (st : (gset addr * heap_state)) : val :=
  default (replicate (length v) MPoison) (
  match ot with
  | PtrOp =>
    if val_to_loc v is Some l then Some v else
      (* The following reimplements integer to pointer casts as described in the VIP paper. *)
      v'  val_to_bytes v;
      a  val_to_Z v' size_t;
      if bool_decide (a = 0) then
        Some (val_of_loc (ProvNull, a))
      else if bool_decide (a  st.1) then
        Some (val_of_loc (ProvFnPtr, a))
      else
        let l' := (ProvAlloc (head (provs_in_bytes v)), a) in
        if bool_decide (valid_ptr l' st.2) then
          Some (val_of_loc l')
        else
          Some (val_of_loc (ProvAlloc None, a))
  | IntOp it => val_to_bytes v
  (* The resize technically should not be necessary since mem_cast
  should only be called if the size is equal to the length of the
  value. But adding it makes proving mem_cast_length a lot easier. *)
  | StructOp sl ots => Some $ resize (length v) MPoison $ mjoin $ zip_with (λ f x, f x)
      (pad_struct sl.(sl_members)
                  (((λ ot, λ v, mem_cast v ot st) <$> ots))
                  (λ ly _, (replicate (ly_size ly) MPoison)))
      (reshape (ly_size <$> sl.(sl_members).*2) v)
  | UntypedOp _ => Some v
  end).

Definition mem_cast_id (v : val) (ot : op_type) : Prop :=
   st, mem_cast v ot st = v.

Lemma mem_cast_length v ot st:
  length (mem_cast v ot st) = length v.
Proof.
  destruct ot => /=.
  - destruct (val_to_bytes v) eqn:Hv => //=.
    + move: Hv => /mapM_length. lia.
    + by rewrite replicate_length.
  - case_match => //=.
    destruct (val_to_bytes v) as [v'|] eqn:Hv => //=. 2: by rewrite replicate_length.
    move: Hv => /mapM_length ->.
    destruct (val_to_Z v') eqn:Hv' => //=. 2: by rewrite replicate_length.
    move: Hv' => /val_to_Z_length /=?.
    by repeat case_match.
  - by rewrite resize_length.
  - done.
Qed.

Lemma mem_cast_id_loc l :
  mem_cast_id (val_of_loc l) PtrOp.
Proof. move => st. rewrite /mem_cast /=. by rewrite val_to_of_loc. Qed.

Lemma mem_cast_id_int it v n :
  val_to_Z v it = Some n 
  mem_cast_id v (IntOp it).
Proof. move => Hi st. rewrite /mem_cast /=. by erewrite val_to_bytes_id. Qed.

Lemma mem_cast_struct_reshape sl v st ots:
  length ots = length (field_names (sl_members sl)) 
  v `has_layout_val` sl 
  ( i v' n ly,
      reshape (ly_size <$> (sl_members sl).*2) v !! i = Some v' 
      sl_members sl !! i = Some (Some n, ly) 
      v' `has_layout_val` ly) 
  reshape (ly_size <$> (sl_members sl).*2) (mem_cast v (StructOp sl ots) st) =
  (zip_with (λ f x, f x)
            (pad_struct (sl_members sl) ((λ ot v, mem_cast v ot st) <$> ots) (λ ly _, replicate (ly_size ly) MPoison))
            (reshape (ly_size <$> (sl_members sl).*2) v)).
Proof.
  move => ? Hv Hly. rewrite /mem_cast/=-/mem_cast resize_all_alt. 2: {
    rewrite join_length Hv {1}/ly_size /=.
    apply: sum_list_eq.
    (* TODO: This is the same proof as below. Somehow unify these two proofs. *)
    apply Forall2_same_length_lookup_2.
    { rewrite !fmap_length zip_with_length reshape_length pad_struct_length !fmap_length. lia. }
    move => i n1 n2. rewrite !list_lookup_fmap.
    move => /fmap_Some[?[/fmap_Some[?[??]]?]]; simplify_eq.
    move => /fmap_Some[?[/lookup_zip_with_Some[?[?[?[Hs?]]]]?]].
    move: Hs => /pad_struct_lookup_Some[|n[?[? Hor]]]. { by rewrite fmap_length. }
    unfold field_list, var_name in *. simplify_eq/=.
    destruct Hor as [[? Hl] | [??]]; simplify_eq/=. 2: by rewrite replicate_length.
    move: Hl. rewrite list_lookup_fmap. move => /fmap_Some[?[??]]. simplify_eq.
    destruct n as [n|] => //. rewrite mem_cast_length. by erewrite Hly.
  }
  rewrite reshape_join //.
  apply Forall2_same_length_lookup_2.
  { rewrite zip_with_length reshape_length pad_struct_length !fmap_length. lia. }
  move => i v' sz /lookup_zip_with_Some[?[?[?[/pad_struct_lookup_Some Hl ?]]]].
  move: Hl => [|n[?[Hin2 Hor]]]. { rewrite fmap_length //. } simplify_eq.
  rewrite !list_lookup_fmap => /fmap_Some[?[/fmap_Some[?[Hin ?]]?]]. rewrite Hin2 in Hin. simplify_eq/=.
  destruct Hor as [[? Hl] |[??]]; simplify_eq. 2: by rewrite replicate_length.
  move: Hl. rewrite list_lookup_fmap => /fmap_Some[?[??]]. simplify_eq. rewrite mem_cast_length.
  destruct n => //. by apply: Hly.
Qed.


Typeclasses Opaque mem_cast_id.
Arguments mem_cast : simpl never.

(** ** Allocation and deallocation. *)

477
478
479
Inductive alloc_new_block : heap_state  loc  val  heap_state  Prop :=
| AllocNewBlock σ l aid v:
    let alloc := Allocation l.2 (length v) true in
Michael Sammler's avatar
Michael Sammler committed
480
    l.1 = ProvAlloc (Some aid) 
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
    σ.(hs_allocs) !! aid = None 
    allocation_in_range alloc 
    heap_range_free σ.(hs_heap) l.2 (length v) 
    alloc_new_block σ l v {|
      hs_heap   := heap_alloc l.2 v aid σ.(hs_heap);
      hs_allocs := <[aid := alloc]> σ.(hs_allocs);
    |}.

Inductive alloc_new_blocks : heap_state  list loc  list val  heap_state  Prop :=
| AllocNewBlock_nil σ :
    alloc_new_blocks σ [] [] σ
| AllocNewBlock_cons σ σ' σ'' l v ls vs :
    alloc_new_block σ l v σ' 
    alloc_new_blocks σ' ls vs σ'' 
    alloc_new_blocks σ (l :: ls) (v :: vs) σ''.

Inductive free_block : heap_state  loc  layout  heap_state  Prop :=
| FreeBlock σ l aid ly v:
    let al_alive := Allocation l.2 ly.(ly_size) true  in
    let al_dead  := Allocation l.2 ly.(ly_size) false in
Michael Sammler's avatar
Michael Sammler committed
501
    l.1 = ProvAlloc (Some aid) 
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
    σ.(hs_allocs) !! aid = Some al_alive 
    length v = ly.(ly_size) 
    heap_lookup_loc l v (λ st, st = RSt 0%nat) σ.(hs_heap) 
    free_block σ l ly {|
      hs_heap   := heap_free l.2 ly.(ly_size) σ.(hs_heap);
      hs_allocs := <[aid := al_dead]> σ.(hs_allocs);
    |}.

Inductive free_blocks : heap_state  list (loc * layout)  heap_state  Prop :=
| FreeBlocks_nil σ :
    free_blocks σ [] σ
| FreeBlocks_cons σ σ' σ'' l ly ls :
    free_block σ l ly σ' 
    free_blocks σ' ls σ'' 
    free_blocks σ ((l, ly) :: ls) σ''.

Lemma free_block_inj hs l ly hs1 hs2:
  free_block hs l ly hs1  free_block hs l ly hs2  hs1 = hs2.
Michael Sammler's avatar
Michael Sammler committed
520
Proof. destruct l. inversion 1; simplify_eq. by inversion 1; simplify_eq/=. Qed.
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
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
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671

Lemma free_blocks_inj hs1 hs2 hs ls:
  free_blocks hs ls hs1  free_blocks hs ls hs2  hs1 = hs2.
Proof.
  move Heq: {1}(hs) => hs' Hb.
  elim: Hb hs Heq. { move => ?? ->. by inversion 1. }
  move => ?????? Hb1 ? IH ??.
  inversion 1; simplify_eq. apply: IH; [|done].
  by apply: free_block_inj.
Qed.

(** ** Heap state invariant definition. *)

(** Predicate stating that every address [a] mapped by the heap of [st] has
a corresponding allocation that encompasses [a] itself. *)
Definition heap_state_heap_cell_in_range_alloc (st : heap_state) :=
   a hc,
    st.(hs_heap) !! a = Some hc 
    addr_in_range_alloc a hc.(hc_alloc_id) st.

(** Predicate stating that every address [a] mapped by the heap of [st] has
a corresponding alive allocation. *)
Definition heap_state_heap_cell_alloc_alive (st : heap_state) :=
   a hc,
    st.(hs_heap) !! a = Some hc 
    alloc_id_alive hc.(hc_alloc_id) st.

(** Predicate stating that all allocations in [st] are in range of memory
that can be allocated. *)
Definition heap_state_alloc_in_range (st : heap_state) :=
   id a,
    st.(hs_allocs) !! id = Some a 
    allocation_in_range a.

(** Predicate stating that alive allocations of [st] are disjoint. *)
Definition heap_state_alloc_disjoint (st : heap_state) :=
   id1 id2 a1 a2,
    id1  id2 
    st.(hs_allocs) !! id1 = Some a1 
    st.(hs_allocs) !! id2 = Some a2 
    alloc_id_alive id1 st 
    alloc_id_alive id2 st 
    a1 ## a2.

(** Predicate stating that every alive allocations in [st] has all of its
addresses mapped in the heap. *)
Definition heap_state_alloc_alive_in_heap (st : heap_state) :=
   id alloc,
    st.(hs_allocs) !! id = Some alloc 
    alloc_id_alive id st 
     a, a  alloc  is_Some (st.(hs_heap) !! a).

(** Invariant on the [heap_state] maintained during evaluation. *)
Definition heap_state_invariant (st : heap_state) : Prop :=
  heap_state_heap_cell_in_range_alloc st 
  heap_state_heap_cell_alloc_alive st 
  heap_state_alloc_in_range st 
  heap_state_alloc_disjoint st 
  heap_state_alloc_alive_in_heap st.

(** ** Lemmas about the heap state invariant. *)

Lemma heap_state_alloc_alive_free_disjoint σ id a n b alloc:
  heap_state_alloc_alive_in_heap σ 
  alloc_id_alive id σ 
  heap_range_free σ.(hs_heap) a n 
  σ.(hs_allocs) !! id = Some alloc 
  Allocation a n b ## alloc.
Proof.
  move => Hin_heap Halive Hfree Hal p Hp1 Hp2.
  apply (Hin_heap _ _ Hal Halive) in Hp2 as [? Hp2].
  rewrite Hfree in Hp2; first done. apply Hp1.
Qed.

Lemma alloc_new_block_invariant σ1 σ2 l v :
  alloc_new_block σ1 l v σ2 
  heap_state_invariant σ1 
  heap_state_invariant σ2.
Proof.
  move => []; clear.
  move => σ1 l aid v alloc Haid Hfresh Halloc Hrange H.
  destruct H as (Hi1&Hi2&Hi3&Hi4&Hi5). split_and!.
  - move => a [id??] /= Ha. destruct (decide (aid = id)) as [->|Hne].
    + exists alloc. split => /=; first by rewrite lookup_insert.
      destruct (decide (l.2  a < l.2 + length v)) as [|Hne] => //=.
      exfalso. rewrite heap_update_lookup_not_in_range in Ha; last first.
      { destruct (decide (a < l.2)); [left | right] => //. lia. }
      apply Hi1 in Ha. destruct Ha as [? [Ha ?]].
      by rewrite /= Hfresh in Ha.
    + destruct (decide (a < l.2  l.2 + length v  a)).
      * rewrite heap_update_lookup_not_in_range in Ha; last done.
        apply Hi1 in Ha. destruct Ha as [?[??]].
        eexists; by rewrite lookup_insert_ne.
      * exfalso. rewrite heap_update_lookup_in_range in Ha; last lia.
        by inversion Ha.
  - move => a [id??] /= Ha. destruct (decide (aid = id)) as [->|Hne].
    + exists alloc. by rewrite lookup_insert.
    + destruct (decide (a < l.2  l.2 + length v  a)).
      * rewrite heap_update_lookup_not_in_range in Ha; last done.
        apply Hi2 in Ha. destruct Ha as [?[??]].
        eexists; by rewrite lookup_insert_ne.
      * exfalso. rewrite heap_update_lookup_in_range in Ha; last lia.
        by inversion Ha.
  - move => id a. destruct (decide (id = aid)) as [->|] => /=.
    + rewrite lookup_insert => ?. by simplify_eq.
    + rewrite lookup_insert_ne => //=. apply Hi3.
  - move => id1 id2 al1 al2 /= Hne Hal1 Hal2 Hid1 Hid2.
    destruct (decide (id1 = aid)) as [->|];
    last (destruct (decide (id2 = aid)) as [->|]).
    + rewrite lookup_insert in Hal1. rewrite lookup_insert_ne // in Hal2.
      simplify_eq => ???. eapply heap_state_alloc_alive_free_disjoint => //.
      move: Hid2 => /= [al []] /=. rewrite lookup_insert_ne //. by exists al.
    + rewrite lookup_insert in Hal2. rewrite lookup_insert_ne // in Hal1.
      simplify_eq => ???. eapply heap_state_alloc_alive_free_disjoint => //.
      move: Hid1 => /= [al []] /=. rewrite lookup_insert_ne //. by exists al.
    + rewrite !lookup_insert_ne // in Hal1, Hal2. move: Hid1 Hid2.
      move => [? []] /=; rewrite lookup_insert_ne // => ??.
      move => [? []] /=; rewrite lookup_insert_ne // => ??.
      apply (Hi4 id1 id2 al1 al2) => //; by eexists.
  - move => id al /= Hal [? [/= ? Halive]] a Ha. simplify_eq.
    destruct (decide (id = aid)) as [->|].
    + rewrite lookup_insert /= in Hal.
      rewrite heap_update_lookup_in_range; naive_solver.
    + rewrite lookup_insert_ne // in Hal.
      rewrite heap_update_lookup_not_in_range; last first.
      { assert (¬ (l.2  a < l.2 + length v)); last lia. move => Hin.
        assert (is_Some (hs_heap σ1 !! a)) as [? Heq].
        { eapply Hi5 => //. by eexists. }
        by rewrite Hrange in Heq. }
      eapply (Hi5 _ _ Hal); [by eexists | done |..].
Qed.

Lemma alloc_new_blocks_invariant σ1 σ2 ls vs :
  alloc_new_blocks σ1 ls vs σ2 
  heap_state_invariant σ1 
  heap_state_invariant σ2.
Proof.
  elim => [] // ??????? Hb Hbs IH H.
  apply IH. by eapply alloc_new_block_invariant.
Qed.

Lemma free_block_invariant σ1 σ2 l ly:
  free_block σ1 l ly σ2 
  heap_state_invariant σ1 
  heap_state_invariant σ2.
Proof.
  move => []; clear.
  move => σ l aid ly v al_a al_d Haid Hal_a Hlen Hlookup H.
  destruct H as (Hi1&Hi2&Hi3&Hi4&Hi5). split_and!.
  - move => a hc /= Hhc.
    assert (¬ (l.2  a < l.2 + length v)) as Hnot_in.
Michael Sammler's avatar
Michael Sammler committed
672
    { move => ?. rewrite heap_free_lookup_in_range // in Hhc; lia. }
673
674
675
676
677
678
679
    rewrite heap_free_lookup_not_in_range in Hhc; last lia.
    destruct (Hi1 _ _ Hhc) as [al [?[??]]]. exists al. split; last done.
    rewrite /= lookup_insert_ne; first done.
    move => ?; subst aid. simplify_eq. apply Hnot_in.
    unfold al_end in *. simpl in *. lia.
  - move => a hc /= Hhc.
    assert (¬ (l.2  a < l.2 + length v)) as Hnot_in.
Michael Sammler's avatar
Michael Sammler committed
680
    { move => ?. rewrite heap_free_lookup_in_range // in Hhc; lia. }
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
    rewrite heap_free_lookup_not_in_range in Hhc; last lia.
    destruct (Hi2 _ _ Hhc) as [al [??]]. exists al.
    rewrite lookup_insert_ne; first done.
    move => Heq. destruct (Hi1 _ _ Hhc) as [?[?[??]]].
    subst al_a. simplify_eq. unfold al_end in *. simpl in *. lia.
  - move => id al /=. destruct (decide (id = aid)) as [->|].
    + rewrite lookup_insert. move => [?]. subst al.
      assert (allocation_in_range al_a); last done.
      by eapply Hi3.
    + rewrite lookup_insert_ne; last done. naive_solver.
  - move => id1 id2 al1 al2 Hne /= Hid1 Hid2 Hal1 Hal2.
    destruct (decide (id1 = aid)) as [->|];
    last (destruct (decide (id2 = aid)) as [->|]).
    + rewrite lookup_insert in Hid1. rewrite lookup_insert_ne // in Hid2.
      simplify_eq. assert (al_a ## al2); last done.
      eapply (Hi4 _ _ _ _ Hne Hal_a Hid2); first by eexists.
      move: Hal2 => [?[/=]]. rewrite lookup_insert_ne //. by eexists.
    + rewrite lookup_insert in Hid2. rewrite lookup_insert_ne // in Hid1.
      simplify_eq. assert (al1 ## al_a); last done.
      eapply (Hi4 _ _ _ _ Hne Hid1 Hal_a); last by eexists.
      move: Hal1 => [?[/=]]. rewrite lookup_insert_ne //. by eexists.
    + destruct Hal1 as [a1 [Ha1 ?]]. destruct Hal2 as [a2 [Ha2 ?]].
      rewrite !lookup_insert_ne // in Hid1, Hid2, Ha1, Ha2.
      apply (Hi4 id1 id2 al1 al2) => //; by eexists.
  - move => id al /= Hid [?[Hal1 Hal2]] a Ha. assert (id  aid) as ?.
    { move => ?; subst id. rewrite lookup_insert in Hal1. naive_solver. }
    rewrite lookup_insert_ne // in Hid, Hal1. simplify_eq.
    rewrite heap_free_lookup_not_in_range;
    first (eapply Hi5 => //; by eexists). move => ?.
    assert (al ## al_a) as Hdisj.
    { apply (Hi4 _ _ _ _ H Hid Hal_a); by eexists. }
    erewrite elem_of_disjoint in Hdisj. by eapply Hdisj.
Qed.

Lemma free_blocks_invariant σ1 σ2 ls:
  free_blocks σ1 ls σ2 
  heap_state_invariant σ1 
  heap_state_invariant σ2.
Proof.
  elim => [] // ?????? Hb Hbs IH H.
  apply IH. by eapply free_block_invariant.
Qed.

Lemma heap_update_heap_cell_in_range_alloc σ a v1 v2 Paid Plk faid flk:
  heap_state_heap_cell_in_range_alloc σ 
  heap_lookup a v1 Paid Plk σ.(hs_heap) 
  ( aid, faid (Some aid) = aid) 
  length v1 = length v2 
  heap_state_heap_cell_in_range_alloc {|
    hs_heap := heap_update a v2 faid flk σ.(hs_heap);
    hs_allocs := σ.(hs_allocs);
  |}.
Proof.
  elim: v2 v1 a => // b2 v2 IH [] // b1 v1 a1 Hσ Hcontains Hfaid [] Hlen.
  move => a2 hc H /=. rewrite /heap_lookup -/heap_lookup in Hcontains.
  move: Hcontains => [[id[?[Heq [??]]]] Hcontains].
  destruct (decide (a1 = a2)) as [->|Hne].
  - rewrite lookup_partial_alter -/heap_update in H. simplify_eq => /=.
Michael Sammler's avatar
Michael Sammler committed
739
    rewrite heap_update_lookup_not_in_range; last lia. rewrite Heq /= Hfaid.
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
    apply (Hσ a2 _ Heq).
  - rewrite lookup_partial_alter_ne // -/heap_update in H.
    by unshelve eapply (IH _ _ Hσ _ Hfaid Hlen a2 hc) => //.
Qed.

Lemma heap_update_heap_cell_alloc_alive σ a v1 v2 Paid Plk faid flk:
  heap_state_heap_cell_alloc_alive σ 
  heap_lookup a v1 Paid Plk σ.(hs_heap) 
  ( aid, faid (Some aid) = aid) 
  length v1 = length v2 
  heap_state_heap_cell_alloc_alive {|
    hs_heap := heap_update a v2 faid flk σ.(hs_heap);
    hs_allocs := σ.(hs_allocs);
  |}.
Proof.
  elim: v2 v1 a => // b2 v2 IH [] // b1 v1 a1 Hσ Hcontains Hfaid [] Hlen.
  move => a2 hc H /=. rewrite /heap_lookup -/heap_lookup in Hcontains.
  move: Hcontains => [[id[?[Heq [??]]]] Hcontains].
  destruct (decide (a1 = a2)) as [->|Hne].
  - rewrite lookup_partial_alter -/heap_update in H. simplify_eq => /=.
Michael Sammler's avatar
Michael Sammler committed
760
    rewrite heap_update_lookup_not_in_range; last lia. rewrite Heq /= Hfaid.
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
    apply (Hσ a2 _ Heq).
  - rewrite lookup_partial_alter_ne // -/heap_update in H.
    by unshelve eapply (IH _ _ Hσ _ Hfaid Hlen a2 hc) => //.
Qed.

Lemma heap_update_alloc_alive_in_heap σ a v1 v2 Paid Plk faid flk:
  heap_state_alloc_alive_in_heap σ 
  heap_lookup a v1 Paid Plk σ.(hs_heap) 
  ( aid, faid (Some aid) = aid) 
  length v1 = length v2 
  heap_state_alloc_alive_in_heap {|
    hs_heap := heap_update a v2 faid flk σ.(hs_heap);
    hs_allocs := σ.(hs_allocs);
  |}.
Proof.
  move => H Hlookup Hfaid Hlen id al /= Hal Halive p Hp.
  destruct (decide (a  p < a + length v2)).
Michael Sammler's avatar
Michael Sammler committed
778
  - rewrite heap_update_lookup_in_range //=.
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
  - rewrite heap_update_lookup_not_in_range; last lia. by eapply H.
Qed.

Lemma heap_update_heap_state_invariant σ a v1 v2 Paid Plk faid flk:
  heap_state_invariant σ 
  heap_lookup a v1 Paid Plk σ.(hs_heap) 
  ( aid, faid (Some aid) = aid) 
  length v1 = length v2 
  heap_state_invariant {|
    hs_heap := heap_update a v2 faid flk σ.(hs_heap);
    hs_allocs := σ.(hs_allocs);
  |}.
Proof.
  move => [?[?[?[??]]]] ???. split_and!.
  - by eapply heap_update_heap_cell_in_range_alloc.
  - by eapply heap_update_heap_cell_alloc_alive.
  - move => *. naive_solver.
  - move => *. naive_solver.
  - by eapply heap_update_alloc_alive_in_heap.
Qed.