source: Deliverables/D3.1/C-semantics/Mem.ma @ 500

Last change on this file since 500 was 500, checked in by campbell, 9 years ago

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

File size: 114.1 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*          Sandrine Blazy, ENSIIE and INRIA Paris-Rocquencourt        *)
7(*                                                                     *)
8(*  Copyright Institut National de Recherche en Informatique et en     *)
9(*  Automatique.  All rights reserved.  This file is distributed       *)
10(*  under the terms of the GNU General Public License as published by  *)
11(*  the Free Software Foundation, either version 2 of the License, or  *)
12(*  (at your option) any later version.  This file is also distributed *)
13(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
14(*                                                                     *)
15(* *********************************************************************)
16
17(* * This file develops the memory model that is used in the dynamic
18  semantics of all the languages used in the compiler.
19  It defines a type [mem] of memory states, the following 4 basic
20  operations over memory states, and their properties:
21- [load]: read a memory chunk at a given address;
22- [store]: store a memory chunk at a given address;
23- [alloc]: allocate a fresh memory block;
24- [free]: invalidate a memory block.
25*)
26
27include "arithmetics/nat.ma".
28(*include "binary/Z.ma".*)
29(*include "datatypes/sums.ma".*)
30(*include "datatypes/list.ma".*)
31(*include "Plogic/equality.ma".*)
32
33(*include "Coqlib.ma".*)
34include "Values.ma".
35(*include "AST.ma".*)
36include "extralib.ma".
37
38definition update : ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z → A. Z → A ≝
39  λA,x,v,f.
40    λy.match eqZb y x with [ true ⇒ v | false ⇒ f y ].
41   
42lemma update_s:
43  ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A.
44  update … x v f x = v.
45#A #x #v #f whd in ⊢ (??%?);
46>(eqZb_z_z …) //;
47qed.
48
49lemma update_o:
50  ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A. ∀y: Z.
51  x ≠ y → update … x v f y = f y.
52#A #x #v #f #y #H whd in ⊢ (??%?);
53@eqZb_elim //;
54#H2 cases H;#H3 elim (H3 ?);//;
55qed.
56
57(* FIXME: workaround for lack of nunfold *)
58lemma unfold_update : ∀A,x,v,f,y. update A x v f y = match eqZb y x with [ true ⇒ v | false ⇒ f y ].
59//; qed.
60
61definition update_block : ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block → A. block → A ≝
62  λA,x,v,f.
63    λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ].
64   
65lemma update_block_s:
66  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
67  update_block … x v f x = v.
68#A * * #ix #v #f whd in ⊢ (??%?);
69>(eqZb_z_z …) //;
70qed.
71
72lemma update_block_o:
73  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. ∀y: block.
74  x ≠ y → update_block … x v f y = f y.
75#A #x #v #f #y #H whd in ⊢ (??%?);
76@eq_block_elim //;
77#H2 cases H;#H3 elim (H3 ?);//;
78qed.
79
80(* FIXME: workaround for lack of nunfold *)
81lemma unfold_update_block : ∀A,x,v,f,y.
82  update_block A x v f y = match eq_block y x with [ true ⇒ v | false ⇒ f y ].
83//; qed.
84
85
86(* * Structure of memory states *)
87
88(* A memory state is organized in several disjoint blocks.  Each block
89  has a low and a high bound that defines its size.  Each block map
90  byte offsets to the contents of this byte. *)
91
92(* The possible contents of a byte-sized memory cell.  To give intuitions,
93  a 4-byte value [v] stored at offset [d] will be represented by
94  the content [Datum(4, v)] at offset [d] and [Cont] at offsets [d+1],
95  [d+2] and [d+3].  The [Cont] contents enable detecting future writes
96  that would partially overlap the 4-byte value. *)
97
98inductive content : Type[0] ≝
99  | Undef: content                 (*r undefined contents *)
100  | Datum: nat → val → content   (*r first byte of a value *)
101  | Cont: content.          (*r continuation bytes for a multi-byte value *)
102
103definition contentmap : Type[0] ≝ Z → content.
104
105(* A memory block comprises the dimensions of the block (low and high bounds)
106  plus a mapping from byte offsets to contents.  *)
107
108record block_contents : Type[0] ≝ {
109  low: Z;
110  high: Z;
111  contents: contentmap
112}.
113
114(* A memory state is a mapping from block addresses (represented by memory
115  regions and integers) to blocks.  We also maintain the address of the next
116  unallocated block, and a proof that this address is positive. *)
117
118record mem : Type[0] ≝ {
119  blocks: block -> block_contents;
120  nextblock: Z;
121  nextblock_pos: OZ < nextblock
122}.
123
124(* * Operations on memory stores *)
125
126(* Memory reads and writes are performed by quantities called memory chunks,
127  encoding the type, size and signedness of the chunk being addressed.
128  The following functions extract the size information from a chunk. *)
129
130definition size_pointer : region → Z ≝
131λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
132
133definition size_chunk : memory_chunk → Z ≝
134  λchunk.match chunk with
135  [ Mint8signed => 1
136  | Mint8unsigned => 1
137  | Mint16signed => 2
138  | Mint16unsigned => 2
139  | Mint32 => 4
140  | Mfloat32 => 4
141  | Mfloat64 => 8
142  | Mpointer r ⇒ size_pointer r
143  ].
144
145definition pred_size_pointer : region → nat ≝
146λsp. match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
147
148definition pred_size_chunk : memory_chunk → nat ≝
149  λchunk.match chunk with
150  [ Mint8signed => 0
151  | Mint8unsigned => 0
152  | Mint16signed => 1
153  | Mint16unsigned => 1
154  | Mint32 => 3
155  | Mfloat32 => 3
156  | Mfloat64 => 7
157  | Mpointer r ⇒ pred_size_pointer r
158  ].
159
160alias symbol "plus" (instance 2) = "integer plus".
161lemma size_chunk_pred:
162  ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk.
163#chunk cases chunk;//; #r cases r; @refl
164qed.
165
166lemma size_chunk_pos:
167  ∀chunk. 0 < size_chunk chunk.
168#chunk >(size_chunk_pred ?) cases (pred_size_chunk chunk);
169normalize;//;
170qed.
171
172(* Memory reads and writes must respect alignment constraints:
173  the byte offset of the location being addressed should be an exact
174  multiple of the natural alignment for the chunk being addressed.
175  This natural alignment is defined by the following
176  [align_chunk] function.  Some target architectures
177  (e.g. the PowerPC) have no alignment constraints, which we could
178  reflect by taking [align_chunk chunk = 1].  However, other architectures
179  have stronger alignment requirements.  The following definition is
180  appropriate for PowerPC and ARM. *)
181
182definition align_chunk : memory_chunk → Z ≝
183  λchunk.match chunk return λ_.Z with
184  [ Mint8signed ⇒ 1
185  | Mint8unsigned ⇒ 1
186  | Mint16signed ⇒ 1
187  | Mint16unsigned ⇒ 1
188  | _ ⇒ 1 ].
189
190lemma align_chunk_pos:
191  ∀chunk. OZ < align_chunk chunk.
192#chunk cases chunk;normalize;//;
193qed.
194
195lemma align_size_chunk_divides:
196  ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
197#chunk cases chunk;[8:#r cases r ]normalize;/3/;
198qed.
199
200lemma align_chunk_compat:
201  ∀chunk1,chunk2.
202    size_chunk chunk1 = size_chunk chunk2 →
203      align_chunk chunk1 = align_chunk chunk2.
204#chunk1 #chunk2
205cases chunk1; try ( #r1 #cases #r1 )
206cases chunk2; try ( #r2 #cases #r2 )
207normalize;//;
208qed.
209
210(* The initial store. *)
211
212definition oneZ ≝ pos one.
213
214lemma one_pos: OZ < oneZ.
215//;
216qed.
217
218definition empty_block : Z → Z → block_contents ≝
219  λlo,hi.mk_block_contents lo hi (λy. Undef).
220
221definition empty: mem ≝
222  mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
223
224definition nullptr: block ≝ mk_block Any OZ.
225
226(* Allocation of a fresh block with the given bounds.  Return an updated
227  memory state and the address of the fresh block, which initially contains
228  undefined cells.  Note that allocation never fails: we model an
229  infinite memory. *)
230
231lemma succ_nextblock_pos:
232  ∀m. OZ < Zsucc (nextblock m). (* XXX *)
233#m lapply (nextblock_pos m);normalize;
234cases (nextblock m);//;
235#n cases n;//;
236qed.
237
238definition alloc : mem → Z → Z → region → mem × block ≝
239  λm,lo,hi,r.
240  let b ≝ mk_block r (nextblock m) in
241  〈mk_mem
242    (update_block … b
243      (empty_block lo hi)
244      (blocks m))
245    (Zsucc (nextblock m))
246    (succ_nextblock_pos m),
247    b〉.
248
249(* Freeing a block.  Return the updated memory state where the given
250  block address has been invalidated: future reads and writes to this
251  address will fail.  Note that we make no attempt to return the block
252  to an allocation pool: the given block address will never be allocated
253  later. *)
254
255definition free ≝
256  λm,b.mk_mem (update_block … b
257                (empty_block OZ OZ)
258                (blocks m))
259        (nextblock m)
260        (nextblock_pos m).
261
262(* Freeing of a list of blocks. *)
263
264definition free_list ≝
265  λm,l.foldr ?? (λb,m.free m b) m l.
266(* XXX hack for lack of reduction with restricted unfolding *)
267lemma unfold_free_list : ∀m,h,t. free_list m (h::t) = free (free_list m t) h.
268normalize; //; qed.
269
270(* Return the low and high bounds for the given block address.
271   Those bounds are 0 for freed or not yet allocated address. *)
272
273definition low_bound : mem → block → Z ≝
274  λm,b.low (blocks m b).
275definition high_bound : mem → block → Z ≝
276  λm,b.high (blocks m b).
277definition block_region: mem → block → region ≝
278  λm,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)
279
280(* A block address is valid if it was previously allocated. It remains valid
281  even after being freed. *)
282
283(* TODO: should this check for region? *)
284definition valid_block : mem → block → Prop ≝
285  λm,b.block_id b < nextblock m.
286
287(* FIXME: hacks to get around lack of nunfold *)
288lemma unfold_low_bound : ∀m,b. low_bound m b = low (blocks m b).
289//; qed.
290lemma unfold_high_bound : ∀m,b. high_bound m b = high (blocks m b).
291//; qed.
292lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock m).
293//; qed.
294
295(* Reading and writing [N] adjacent locations in a [contentmap].
296
297  We define two functions and prove some of their properties:
298  - [getN n ofs m] returns the datum at offset [ofs] in block contents [m]
299    after checking that the contents of offsets [ofs+1] to [ofs+n+1]
300    are [Cont].
301  - [setN n ofs v m] updates the block contents [m], storing the content [v]
302    at offset [ofs] and the content [Cont] at offsets [ofs+1] to [ofs+n+1].
303 *)
304
305let rec check_cont (n: nat) (p: Z) (m: contentmap) on n : bool ≝
306  match n return λ_.bool with
307  [ O ⇒ true
308  | S n1 ⇒
309      match m p with
310      [ Cont ⇒ check_cont n1 (Zplus p 1) m (* FIXME: cannot disambiguate + properly  *)
311      | _ ⇒ false ] ].
312
313(* XXX : was +, not ∨ logical or
314   is used when eqb is expected, coq idiom, is it necessary?? *)
315definition eq_nat: ∀p,q: nat. p=q ∨ p≠q.
316@decidable_eq_nat (* // not working, why *)
317qed.
318
319definition getN : nat → Z → contentmap → val ≝
320  λn,p,m.match m p with
321  [ Datum n' v ⇒
322      match andb (eqb n n') (check_cont n (p + oneZ) m) with
323      [ true ⇒ v
324      | false ⇒ Vundef ]
325  | _ ⇒
326      Vundef ].
327
328let rec set_cont (n: nat) (p: Z) (m: contentmap) on n : contentmap ≝
329  match n with
330  [ O ⇒ m
331  | S n1 ⇒ update ? p Cont (set_cont n1 (p + oneZ) m) ].
332
333definition setN : nat → Z → val → contentmap → contentmap ≝
334  λn,p,v,m.update ? p (Datum n v) (set_cont n (p + oneZ) m).
335
336(* Nonessential properties that may require arithmetic
337(* XXX: the daemons *)
338axiom daemon : ∀A:Prop.A.
339
340lemma check_cont_spec:
341  ∀n,m,p.
342  match (check_cont n p m) with
343  [ true ⇒ ∀q.p ≤ q → q < p + n → m q = Cont
344  | false ⇒ ∃q. p ≤ q ∧ q < (p + n) ∧ m q ≠ Cont ].
345#n elim n;
346[#m #p #q #Hl #Hr
347   (* derive contradiction from Hl, Hr; needs:
348      - p + O = p
349      - p ≤ q → q < p → False *)
350   napply daemon
351|#n1 #IH #m #p
352   (* whd : doesn't work either *)
353   cut (check_cont (S n1) p m = match m p with [ Undef ⇒ false | Datum _ _ ⇒ false | Cont ⇒ check_cont n1 (Zplus p oneZ) m ])
354   [@
355   |#Heq >Heq lapply (refl ? (m p));
356      cases (m p) in ⊢ (???% → %);
357      [#Heq1 %
358           [napply p
359           |% [napply daemon
360                 |@nmk #Hfalse >Hfalse in Heq1 #Heq1
361                    destruct ]
362           ]
363      |#n2 #v #Heq1 %
364           [napply p
365           | % [ (* refl≤ and  p < p + S n1 *)napply daemon
366                  |@nmk #Hfalse >Hfalse in Heq1 #Heq1
367                     destruct ]
368           ]
369      |#Heq1 lapply (IH m (p + 1));
370         lapply (refl ? (check_cont n1 (p + 1) m));
371         (* napply daemon *)
372         cases (check_cont n1 (p + 1) m) in ⊢ (???% → %);
373         whd in ⊢ (? → % → %);
374         [#H #H1 #q #Hl #Hr
375            cut (p = q ∨ p + 1 ≤ q)
376            [(* Hl *) napply daemon
377            |*;
378               [//
379               |#Hl2 @H1 //;(*Hr*)napply daemon ] ]
380         |#H #H1 cases H1;#x *;*;#Hl #Hr #Hx
381            %{ x} @
382            [@
383               [(*Hl*) napply daemon
384               |(*Hr*) napply daemon ]
385            |//]]]]
386qed.
387
388lemma check_cont_true:
389  ∀n:nat.∀m,p.
390  (∀q. p ≤ q → q < p + n → m q = Cont) →
391  check_cont n p m = true.
392#n #m #p #H lapply (check_cont_spec n m p);
393cases (check_cont n p m);//;
394whd in ⊢ (%→?);*;
395#q *;*;#Hl #Hr #Hfalse cases Hfalse;#H1 elim (H1 ?);@H //;
396qed.
397
398lemma check_cont_false:
399  ∀n:nat.∀m,p,q.
400  p ≤ q → q < p + n → m q ≠ Cont →
401  check_cont n p m = false.
402#n #m #p #q lapply (check_cont_spec n m p);
403cases (check_cont n p m);//;
404whd in ⊢ (%→?);#H
405#Hl #Hr #Hfalse cases Hfalse;#H1 elim (H1 ?);@H //;
406qed.
407
408lemma set_cont_inside:
409  ∀n:nat.∀p:Z.∀m.∀q:Z.
410  p ≤ q → q < p + n →
411  (set_cont n p m) q = Cont.
412#n elim n;
413[#p #m #q #Hl #Hr (* by Hl, Hr → False *)napply daemon
414|#n1 #IH #p #m #q #Hl #Hr
415   cut (p = q ∨ p+1 ≤ q)
416   [napply daemon
417   |*;
418      [#Heq >Heq @update_s
419      |#Hl2 whd in ⊢ (??%?);nrewrite > (? : eqZb q p = false)
420         [whd in ⊢ (??%?);napply IH
421            [napply Hl2
422            |(* Hr *) napply daemon ]
423         |(*Hl2*)napply daemon ]
424      ]
425   ]
426]
427qed.
428
429lemma set_cont_outside:
430  ∀n:nat.∀p:Z.∀m.∀q:Z.
431  q < p ∨ p + n ≤ q →
432  (set_cont n p m) q = m q.
433#n elim n
434[#p #m #q #_ @
435|#n1 #IH #p #m #q
436   #H whd in ⊢ (??%?);>(? : eqZb q p = false)
437   [whd in ⊢ (??%?);@IH cases H;
438      [#Hl % napply daemon
439      |#Hr %{2} napply daemon]
440   |(*H*)napply daemon ]
441]
442qed.
443
444lemma getN_setN_same:
445  ∀n,p,v,m.
446  getN n p (setN n p v m) = v.
447#n #p #v #m nchange in ⊢ (??(???%)?) with (update ????);
448whd in ⊢ (??%?);
449>(update_s content p ??) whd in ⊢ (??%?);
450>(eqb_n_n n)
451nrewrite > (check_cont_true ????)
452[@
453|#q #Hl #Hr >(update_o content …)
454   [/2/;
455   |(*Hl*)napply daemon ]
456]
457qed.
458
459lemma getN_setN_other:
460  ∀n1,n2:nat.∀p1,p2:Z.∀v,m.
461  p1 + n1 < p2 ∨ p2 + n2 < p1 →
462  getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m.
463#n1 #n2 #p1 #p2 #v #m #H
464ngeneralize in match (check_cont_spec n2 m (p2 + oneZ));
465lapply (refl ? (check_cont n2 (p2+oneZ) m));
466cases (check_cont n2 (p2+oneZ) m) in ⊢ (???% → %);
467#H1 whd in ⊢ (% →?); whd in ⊢ (?→(???%)); >H1
468[#H2
469   nchange in ⊢ (??(???%)?) with (update ????);
470   whd in ⊢(??%%);>(check_cont_true …)
471   [ >(check_cont_true … H2)
472       >(update_o content ?????)
473       [ >(set_cont_outside ?????) //; (* arith *) napply daemon
474       | (* arith *) napply daemon
475       ]
476   | #q #Hl #Hh >(update_o content ?????)
477       [ >(set_cont_outside ?????) /2/; (* arith *) napply daemon
478       | (* arith *) napply daemon
479       ]
480   ]
481| *; #q *;#A #B
482   nchange in ⊢ (??(???%)?) with (update ????);
483   whd in ⊢(??%%);
484   >(check_cont_false n2 (update ? p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) q …)
485   [ >(update_o content ?????)
486       [ >(set_cont_outside ?????) //; (* arith *) napply daemon
487       | napply daemon
488       ]
489   | >(update_o content ?????)
490       [ >(set_cont_outside ?????) //; (* arith *) napply daemon
491       | napply daemon
492       ]
493   | napply daemon
494   | napply daemon
495   ]
496] qed.
497
498lemma getN_setN_overlap:
499  ∀n1,n2,p1,p2,v,m.
500  p1 ≠ p2 →
501  p2 ≤ p1 + Z_of_nat n1 →  p1 ≤ p2 + Z_of_nat n2 →
502  getN n2 p2 (setN n1 p1 v m) = Vundef.
503#n1 #n2 #p1 #p2 #v #m
504#H #H1 #H2
505nchange in ⊢ (??(???%)?) with (update ????);
506whd in ⊢(??%?);>(update_o content ?????)
507[lapply (Z_compare_to_Prop p2 p1);
508   lapply (refl ? (Z_compare p2 p1));
509   cases (Z_compare p2 p1) in ⊢ (???% → %);#H3
510   [nchange in ⊢ (% → ?) with (p2 < p1);#H4
511  (* [p1] belongs to [[p2, p2 + n2 - 1]],
512     therefore [check_cont n2 (p2 + 1) ...] is false. *)
513     >(check_cont_false …)
514     [cases (set_cont n1 (p1+oneZ) m p2)
515        [1,3:@
516        |#n3 #v1 whd in ⊢ (??%?);
517           cases (eqb n2 n3);@ ]
518     |>(update_s content …) @nmk
519        #Hfalse destruct
520     |(*H2*) napply daemon
521     |(*H4*) napply daemon
522     |##skip ]
523  |whd in ⊢ (% → ?);#H4 elim H;#H5 elim (H5 ?);//;
524  |nchange in ⊢ (% → ?) with (p1 < p2);#H4
525  (* [p2] belongs to [[p1 + 1, p1 + n1 - 1]],
526     therefore [
527     set_cont n1 (p1 + 1) m p2] is [Cont]. *)
528     >(set_cont_inside …)
529     [@
530     |(*H1*)napply daemon
531     |(*H4*)napply daemon]
532  ]
533|//]
534qed.
535
536lemma getN_setN_mismatch:
537  ∀n1,n2,p,v,m.
538  n1 ≠ n2 →
539  getN n2 p (setN n1 p v m) = Vundef.
540#n1 #n2 #p #v #m #H
541nchange in ⊢ (??(???%)?) with (update ????);
542whd in ⊢(??%?);>(update_s content …)
543whd in ⊢(??%?);>(not_eq_to_eqb_false … (sym_neq … H)) //;
544qed.
545
546lemma getN_setN_characterization:
547  ∀m,v,n1,p1,n2,p2.
548  getN n2 p2 (setN n1 p1 v m) = v
549  ∨ getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m
550  ∨ getN n2 p2 (setN n1 p1 v m) = Vundef.
551#m #v #n1 #p1 #n2 #p2
552lapply (eqZb_to_Prop p1 p2); cases (eqZb p1 p2); #Hp
553[>Hp
554   @(eqb_elim n1 n2) #Hn
555   [>Hn % % //;
556   |%{2} /2/]
557|lapply (Z_compare_to_Prop (p1 + n1) p2);
558   cases  (Z_compare (p1 + n1) p2);#Hcmp
559   [% %{2} @getN_setN_other /2/
560   |lapply (Z_compare_to_Prop (p2 + n2) p1);
561      cases  (Z_compare (p2 + n2) p1);#Hcmp2
562      [% %{2} @getN_setN_other /2/
563      |%{2} @getN_setN_overlap
564         [//
565         |*:(* arith *) napply daemon]
566      |%{2} @getN_setN_overlap
567         [//
568         |*:(* arith *) napply daemon]
569      ]
570   |lapply (Z_compare_to_Prop (p2 + n2) p1);
571      cases  (Z_compare (p2 + n2) p1);#Hcmp2
572      [% %{2} @getN_setN_other /2/
573      |%{2} @getN_setN_overlap
574         [//
575         |*:(* arith *) napply daemon]
576      |%{2} @getN_setN_overlap
577         [//
578         |*:(* arith *) napply daemon]
579      ]
580   ]
581]
582qed.
583
584lemma getN_init:
585  ∀n,p.
586  getN n p (λ_.Undef) = Vundef.
587#n #p //;
588qed.
589*)
590
591(* [valid_access m chunk r b ofs] holds if a memory access (load or store)
592    of the given chunk is possible in [m] at address [b, ofs].
593    This means:
594- The block [b] is valid.
595- The range of bytes accessed is within the bounds of [b].
596- The offset [ofs] is aligned.
597- The pointer representation (i.e., region) [r] is compatible with the class of [b].
598*)
599
600inductive valid_access (m: mem) (chunk: memory_chunk) (r: region) (b: block) (ofs: Z)
601            : Prop ≝
602  | valid_access_intro:
603      valid_block m b →
604      low_bound m b ≤ ofs →
605      ofs + size_chunk chunk ≤ high_bound m b →
606      (align_chunk chunk ∣ ofs) →
607      pointer_compat b r →
608      valid_access m chunk r b ofs.
609
610(* The following function checks whether accessing the given memory chunk
611  at the given offset in the given block respects the bounds of the block. *)
612
613(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
614let rec in_bounds
615  (m:mem) (chunk:memory_chunk) (r:region) (b:block) (ofs:Z) on b : 
616    Sum (valid_access m chunk r b ofs) (Not (valid_access m chunk r b ofs)) ≝ ?.
617cases b #br #bi
618@(Zltb_elim_Type0 bi (nextblock m)) #Hnext
619[ @(Zleb_elim_Type0 (low_bound m (mk_block br bi)) ofs) #Hlo
620    [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m (mk_block br bi))) #Hhi
621        [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal
622          [ cases (pointer_compat_dec (mk_block br bi) r); #Hcl
623            [ %1 % // @Hnext ]
624          ]
625        ]
626    ]
627]
628%2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) // [ 2: @Hval | 3: @Hnext ]
629qed.
630
631lemma in_bounds_true:
632  ∀m,chunk,r,b,ofs. ∀A: Type[0]. ∀a1,a2: A.
633  valid_access m chunk r b ofs ->
634  (match in_bounds m chunk r b ofs with
635   [ inl _ ⇒ a1 | inr _ ⇒ a2 ]) = a1.
636#m #chunk #r #b #ofs #A #a1 #a2 #H
637cases (in_bounds m chunk r b ofs);normalize;#H1
638[//
639|elim (?:False); @(absurd ? H H1)]
640qed.
641
642(* [valid_pointer] holds if the given block address is valid (and can be
643  represented in a pointer with the region [r]) and the
644  given offset falls within the bounds of the corresponding block. *)
645
646definition valid_pointer : mem → region → block → Z → bool ≝
647λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧
648  Zleb (low_bound m b) ofs ∧
649  Zltb ofs (high_bound m b) ∧
650  is_pointer_compat b r.
651
652(* [load chunk m r b ofs] perform a read in memory state [m], at address
653  [b] and offset [ofs].  [None] is returned if the address is invalid
654  or the memory access is out of bounds or the address cannot be represented
655  by a pointer with region [r]. *)
656
657definition load : memory_chunk → mem → region → block → Z → option val ≝
658λchunk,m,r,b,ofs.
659  match in_bounds m chunk r b ofs with
660  [ inl _ ⇒ Some ? (load_result chunk
661           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))))
662  | inr _ ⇒ None ? ].
663
664lemma load_inv:
665  ∀chunk,m,r,b,ofs,v.
666  load chunk m r b ofs = Some ? v →
667  valid_access m chunk r b ofs ∧
668  v = load_result chunk
669           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))).
670#chunk #m #r #b #ofs #v whd in ⊢ (??%? → ?);
671cases (in_bounds m chunk r b ofs); #Haccess whd in ⊢ ((??%?) → ?); #H
672[ % //; destruct; //;
673| destruct
674]
675qed.
676
677(* [loadv chunk m addr] is similar, but the address and offset are given
678  as a single value [addr], which must be a pointer value. *)
679
680let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
681  match addr with
682  [ Vptr r b p ofs ⇒ load chunk m r b (signed ofs)
683  | _ ⇒ None ? ].
684
685(* The memory state [m] after a store of value [v] at offset [ofs]
686   in block [b]. *)
687
688definition unchecked_store : memory_chunk → mem → block → Z → val → mem ≝
689λchunk,m,b,ofs,v.
690  let c ≝ (blocks m b) in
691  mk_mem
692    (update_block ? b
693        (mk_block_contents (low c) (high c)
694                 (setN (pred_size_chunk chunk) ofs v (contents c)))
695        (blocks m))
696    (nextblock m)
697    (nextblock_pos m).
698
699(* [store chunk m r b ofs v] perform a write in memory state [m].
700  Value [v] is stored at address [b] and offset [ofs].
701  Return the updated memory store, or [None] if the address is invalid
702  or the memory access is out of bounds or the address cannot be represented
703  by a pointer with region [r]. *)
704
705definition store : memory_chunk → mem → region → block → Z → val → option mem ≝
706λchunk,m,r,b,ofs,v.
707  match in_bounds m chunk r b ofs with
708  [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v)
709  | inr _ ⇒ None ? ].
710
711lemma store_inv:
712  ∀chunk,m,r,b,ofs,v,m'.
713  store chunk m r b ofs v = Some ? m' →
714  valid_access m chunk r b ofs ∧
715  m' = unchecked_store chunk m b ofs v.
716#chunk #m #r #b #ofs #v #m' whd in ⊢ (??%? → ?);
717(*9*)
718cases (in_bounds m chunk r b ofs);#Hv whd in ⊢(??%? → ?);#Heq
719[% [//|destruct;//]
720|destruct]
721qed.
722
723(* [storev chunk m addr v] is similar, but the address and offset are given
724  as a single value [addr], which must be a pointer value. *)
725
726definition storev : memory_chunk → mem → val → val → option mem ≝
727λchunk,m,addr,v.
728  match addr with
729  [ Vptr r b p ofs ⇒ store chunk m r b (signed ofs) v
730  | _ ⇒ None ? ].
731
732(* * Properties of the memory operations *)
733
734(* ** Properties related to block validity *)
735
736lemma valid_not_valid_diff:
737  ∀m,b,b'. valid_block m b →  ¬(valid_block m b') → b ≠ b'.
738#m #b #b' #H #H' @nmk #e >e in H #H
739@(absurd ? H H')
740qed.
741
742lemma valid_access_valid_block:
743  ∀m,chunk,r,b,ofs. valid_access m chunk r b ofs → valid_block m b.
744#m #chunk #r #b #ofs #H
745elim H;//;
746qed.
747
748lemma valid_access_aligned:
749  ∀m,chunk,r,b,ofs.
750  valid_access m chunk r b ofs → (align_chunk chunk ∣ ofs).
751#m #chunk #r #b #ofs #H
752elim H;//;
753qed.
754
755lemma valid_access_compat:
756  ∀m,chunk1,chunk2,r,b,ofs.
757  size_chunk chunk1 = size_chunk chunk2 →
758  valid_access m chunk1 r b ofs →
759  valid_access m chunk2 r b ofs.
760#m #chunk #chunk2 #r #b #ofs #H1 #H2
761elim H2;#H3 #H4 #H5 #H6 #H7
762>H1 in H5 #H5
763% //;
764<(align_chunk_compat … H1) //;
765qed.
766
767(* Hint Resolve valid_not_valid_diff valid_access_valid_block valid_access_aligned: mem.*)
768
769(* ** Properties related to [load] *)
770
771theorem valid_access_load:
772  ∀m,chunk,r,b,ofs.
773  valid_access m chunk r b ofs →
774  ∃v. load chunk m r b ofs = Some ? v.
775#m #chunk #r #b #ofs #H %
776[2:whd in ⊢ (??%?);@in_bounds_true //;
777|skip]
778qed.
779
780theorem load_valid_access:
781  ∀m,chunk,r,b,ofs,v.
782  load chunk m r b ofs = Some ? v →
783  valid_access m chunk r b ofs.
784#m #chunk #r #b #ofs #v #H
785cases (load_inv … H);//;
786qed.
787
788(* Hint Resolve load_valid_access valid_access_load.*)
789
790(* ** Properties related to [store] *)
791
792lemma valid_access_store:
793  ∀m1,chunk,r,b,ofs,v.
794  valid_access m1 chunk r b ofs →
795  ∃m2. store chunk m1 r b ofs v = Some ? m2.
796#m1 #chunk #r #b #ofs #v #H
797%
798[2:@in_bounds_true //
799|skip]
800qed.
801
802(* section STORE *)
803
804lemma low_bound_store:
805  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
806  ∀b'.low_bound m2 b' = low_bound m1 b'.
807#chunk #m1 #r #b #ofs #v #m2 #STORE
808#b' cases (store_inv … STORE)
809#H1 #H2 >H2
810whd in ⊢ (??(?%?)?) whd in ⊢ (??%?)
811whd in ⊢ (??(?%)?) @eq_block_elim #E
812normalize //
813qed.
814
815lemma nextblock_store :
816  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
817  nextblock m2 = nextblock m1.
818#chunk #m1 #r #b #ofs #v #m2 #STORE
819cases (store_inv … STORE);
820#Hvalid #Heq
821>Heq %
822qed.
823
824lemma high_bound_store:
825  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
826  ∀b'. high_bound m2 b' = high_bound m1 b'.
827#chunk #m1 #r #b #ofs #v #m2 #STORE
828#b' cases (store_inv … STORE);
829#Hvalid #H
830>H
831whd in ⊢ (??(?%?)?);whd in ⊢ (??%?);
832whd in ⊢ (??(?%)?); @eq_block_elim #E
833normalize;//;
834qed.
835
836lemma region_store:
837  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
838  ∀b'. block_region m2 b' = block_region m1 b'.
839#chunk #m1 #r #b #ofs #v #m2 #STORE
840* #r #b' //
841qed.
842
843lemma store_valid_block_1:
844  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
845  ∀b'. valid_block m1 b' → valid_block m2 b'.
846#chunk #m1 #r #b #ofs #v #m2 #STORE
847#b' whd in ⊢ (% → %);#Hv
848>(nextblock_store … STORE) //;
849qed.
850
851lemma store_valid_block_2:
852  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
853  ∀b'. valid_block m2 b' → valid_block m1 b'.
854#chunk #m1 #r #b #ofs #v #m2 #STORE
855#b' whd in ⊢ (%→%);
856>(nextblock_store … STORE) //;
857qed.
858
859(*Hint Resolve store_valid_block_1 store_valid_block_2: mem.*)
860
861lemma store_valid_access_1:
862  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
863  ∀chunk',r',b',ofs'.
864  valid_access m1 chunk' r' b' ofs' → valid_access m2 chunk' r' b' ofs'.
865#chunk #m1 #r #b #ofs #v #m2 #STORE
866#chunk' #r' #b' #ofs'
867* Hv;
868#Hvb #Hl #Hr #Halign #Hptr
869% //;
870[@(store_valid_block_1 … STORE) //
871|>(low_bound_store … STORE …) //
872|>(high_bound_store … STORE …) //
873] qed.
874
875lemma store_valid_access_2:
876  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
877  ∀chunk',r',b',ofs'.
878  valid_access m2 chunk' r' b' ofs' → valid_access m1 chunk' r' b' ofs'.
879#chunk #m1 #r #b #ofs #v #m2 #STORE
880#chunk' #r' #b' #ofs'
881* Hv;
882#Hvb #Hl #Hr #Halign #Hcompat
883% //;
884[@(store_valid_block_2 … STORE) //
885|<(low_bound_store … STORE …) //
886|<(high_bound_store … STORE …) //
887] qed.
888
889lemma store_valid_access_3:
890  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
891  valid_access m1 chunk r b ofs.
892#chunk #m1 #r #b #ofs #v #m2 #STORE
893cases (store_inv … STORE);//;
894qed.
895
896(*Hint Resolve store_valid_access_1 store_valid_access_2
897             store_valid_access_3: mem.*)
898
899lemma load_compat_pointer:
900  ∀chunk,m,r,r',b,ofs,v.
901  pointer_compat b r' →
902  load chunk m r b ofs = Some ? v →
903  load chunk m r' b ofs = Some ? v.
904#chunk #m #r #r' #b #ofs #v #Hcompat #LOAD
905lapply (load_valid_access … LOAD); #Hvalid
906cut (valid_access m chunk r' b ofs);
907[ % elim Hvalid; //;
908| #Hvalid'
909    <LOAD whd in ⊢ (??%%);
910    >(in_bounds_true … (option val) ?? Hvalid)
911    >(in_bounds_true … (option val) ?? Hvalid')
912    //
913] qed.
914
915(* Nonessential properties that may require arithmetic
916theorem load_store_similar:
917  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
918  ∀chunk'.
919  size_chunk chunk' = size_chunk chunk →
920  load chunk' m2 r b ofs = Some ? (load_result chunk' v).
921#chunk #m1 #r #b #ofs #v #m2 #STORE
922#chunk' #Hsize cases (store_inv … STORE);
923#Hv #Heq
924whd in ⊢ (??%?);
925nrewrite > (in_bounds_true m2 chunk' r b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))
926               (None ?) ?);
927[>Heq
928   whd in ⊢ (??(??(? ? (? ? ? (? (? % ?)))))?);
929   >(update_s ? b ? (blocks m1)) (* XXX  too many metas for my taste *)
930   >(? : pred_size_chunk chunk = pred_size_chunk chunk')
931   [//;
932   |>(size_chunk_pred …) in Hsize #Hsize
933      >(size_chunk_pred …) in Hsize #Hsize
934      @injective_Z_of_nat @(injective_Zplus_r 1) //;]
935|@(store_valid_access_1 … STORE)
936   cases Hv;#H1 #H2 #H3 #H4 #H5 % //;
937   >(align_chunk_compat … Hsize) //]
938qed.
939
940theorem load_store_same:
941  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
942  load chunk m2 r b ofs = Some ? (load_result chunk v).
943#chunk #m1 #r #b #ofs #v #m2 #STORE
944@load_store_similar //;
945qed.
946       
947theorem load_store_other:
948  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
949  ∀chunk',r',b',ofs'.
950  b' ≠ b
951  ∨ ofs' + size_chunk chunk' ≤  ofs
952  ∨ ofs + size_chunk chunk ≤ ofs' →
953  load chunk' m2 r' b' ofs' = load chunk' m1 r' b' ofs'.
954#chunk #m1 #r #b #ofs #v #m2 #STORE
955#chunk' #r' #b' #ofs' #H
956cases (store_inv … STORE);
957#Hvalid #Heq whd in ⊢ (??%%);
958cases (in_bounds m1 chunk' r' b' ofs');
959[#Hvalid1 >(in_bounds_true m2 chunk' r' b' ofs' ? (Some ? ?) ??)
960   [whd in ⊢ (???%); @(eq_f … (Some val)) @(eq_f … (load_result chunk'))
961      >Heq whd in ⊢ (??(???(? (? % ?)))?);
962                     whd in ⊢ (??(???(? %))?);
963      lapply (eqZb_to_Prop b' b);cases (eqZb b' b);
964      whd in ⊢ (% → ?);
965      [#Heq1 >Heq1 whd in ⊢ (??(??? (? %))?);
966         >(size_chunk_pred …) in H
967         >(size_chunk_pred …) #H
968         @(getN_setN_other …) cases H
969         [*
970            [#Hfalse elim Hfalse;#H1 elim (H1 Heq1)
971            |#H1 %{2} (*H1*)napply daemon ]
972         |#H1 % (*H1*)napply daemon ]
973      |#Hneq @ ]
974   |@(store_valid_access_1 … STORE) //]
975|whd in ⊢ (? → ???%);lapply (in_bounds m2 chunk' r' b' ofs');
976   #H1 cases H1;
977   [#H2 #H3 lapply (store_valid_access_2 … STORE … H2);#Hfalse
978      cases H3;#H4 elim (H4 Hfalse)
979   |#H2 #H3 @]
980]
981qed.
982
983
984theorem load_store_overlap:
985  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
986  ∀chunk',ofs',v'. load chunk' m2 r b ofs' = Some ? v' →
987  ofs' ≠ ofs →
988  ofs < ofs' + size_chunk chunk' →
989  ofs' < ofs + size_chunk chunk →
990  v' = Vundef.
991#chunk #m1 #r #b #ofs #v #m2 #STORE
992#chunk' #ofs' #v' #H
993#H1 #H2 #H3
994cases (store_inv … STORE);
995cases (load_inv … H);
996#Hvalid #Heq #Hvalid1 #Heq1 >Heq >Heq1
997nchange in ⊢ (??(??(???(?(?%?))))?) with (mk_mem ???);
998>(update_s block_contents …)
999>(getN_setN_overlap …)
1000[cases chunk';//
1001|>(size_chunk_pred …) in H2 (*arith*) napply daemon
1002|>(size_chunk_pred …) in H3 (*arith*) napply daemon
1003|@sym_neq //]
1004qed.
1005
1006theorem load_store_overlap':
1007  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
1008  ∀chunk',ofs'.
1009  valid_access m1 chunk' r b ofs' →
1010  ofs' ≠ ofs →
1011  ofs < ofs' + size_chunk chunk' →
1012  ofs' < ofs + size_chunk chunk →
1013  load chunk' m2 r b ofs' = Some ? Vundef.
1014#chunk #m1 #r #b #ofs #v #m2 #STORE
1015#chunk' #ofs' #Hvalid #H #H1 #H2
1016cut (∃v'.load chunk' m2 r b ofs' = Some ? v')
1017[@valid_access_load
1018   @(store_valid_access_1 … STORE) //
1019|#H3 cases H3;
1020   #x #Hx >Hx @(eq_f … (Some val))
1021   @(load_store_overlap … STORE … Hx) //;]
1022qed.
1023
1024theorem load_store_mismatch:
1025  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
1026  ∀chunk',v'.
1027  load chunk' m2 r b ofs = Some ? v' →
1028  size_chunk chunk' ≠ size_chunk chunk →
1029  v' = Vundef.
1030#chunk #m1 #r #b #ofs #v #m2 #STORE
1031#chunk' #v' #H #H1
1032cases (store_inv … STORE);
1033cases (load_inv … H);
1034#Hvalid #H2 #Hvalid1 #H3
1035>H2
1036nchange in H3:(???%) with (mk_mem ???);
1037>H3 >(update_s block_contents …)
1038>(getN_setN_mismatch …)
1039[cases chunk';//;
1040|>(size_chunk_pred …) in H1 >(size_chunk_pred …)
1041   #H1 @nmk #Hfalse elim H1;#H4 @H4
1042   @(eq_f ?? (λx.1 + x) ???) //]
1043qed.
1044
1045theorem load_store_mismatch':
1046  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
1047  ∀chunk'.
1048  valid_access m1 chunk' r b ofs →
1049  size_chunk chunk' ≠ size_chunk chunk →
1050  load chunk' m2 r b ofs = Some ? Vundef.
1051#chunk #m1 #r #b #ofs #v #m2 #STORE
1052#chunk' #Hvalid #Hsize
1053cut (∃v'.load chunk' m2 r b ofs = Some ? v')
1054[@(valid_access_load …)
1055   napply
1056    (store_valid_access_1 … STORE);//
1057|*;#x #Hx >Hx @(eq_f … (Some val))
1058   @(load_store_mismatch … STORE … Hsize) //;]
1059qed.
1060
1061inductive load_store_cases
1062      (chunk1: memory_chunk) (b1: block) (ofs1: Z)
1063      (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type[0] ≝
1064  | lsc_similar:
1065      b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 = size_chunk chunk2 →
1066      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
1067  | lsc_other:
1068      b1 ≠ b2 ∨ ofs2 + size_chunk chunk2 ≤ ofs1 ∨ ofs1 + size_chunk chunk1 ≤ ofs2 →
1069      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
1070  | lsc_overlap:
1071      b1 = b2 -> ofs1 ≠ ofs2 -> ofs1 < ofs2 + size_chunk chunk2 → ofs2 < ofs1 + size_chunk chunk1 ->
1072      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
1073  | lsc_mismatch:
1074      b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 ≠ size_chunk chunk2 ->
1075      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.
1076
1077definition load_store_classification:
1078  ∀chunk1,b1,ofs1,chunk2,b2,ofs2.
1079  load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.
1080#chunk1 #b1 #ofs1 #chunk2 #b2 #ofs2
1081cases (decidable_eq_Z_Type b1 b2);#H
1082[cases (decidable_eq_Z_Type ofs1 ofs2);#H1
1083   [cases (decidable_eq_Z_Type (size_chunk chunk1) (size_chunk chunk2));#H2
1084      [@lsc_similar //;
1085      |@lsc_mismatch //;]
1086   |lapply (Z_compare_to_Prop (ofs2 + size_chunk chunk2) ofs1);
1087      cases (Z_compare (ofs2+size_chunk chunk2) ofs1);
1088      [nchange with (Zlt ? ? → ?);#H2
1089         @lsc_other % %{2} (*trivial Zlt_to_Zle BUT the statement is strange*)
1090         napply daemon
1091      |nchange with (? = ? → ?);#H2
1092         @lsc_other % %{2} (*trivial eq_to_Zle not defined *) napply daemon
1093      |nchange with (Zlt ? ? → ?);#H2
1094         lapply (Z_compare_to_Prop (ofs1 + size_chunk chunk1) ofs2);
1095         cases (Z_compare (ofs1 + size_chunk chunk1) ofs2);
1096         [nchange with (Zlt ? ? → ?);#H3
1097            @lsc_other %{2} (*trivial as previously*) napply daemon
1098         |nchange with (? = ? → ?);#H3
1099            @lsc_other %{2} (*trivial as previously*) napply daemon
1100         |nchange with (Zlt ? ? → ?);#H3
1101            @lsc_overlap //;]
1102      ]
1103   ]
1104|@lsc_other % % (* XXX // doesn't spot this! *) napply H ]
1105qed.
1106
1107theorem load_store_characterization:
1108  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
1109  ∀chunk',r',b',ofs'.
1110  valid_access m1 chunk' r' b' ofs' →
1111  load chunk' m2 r' b' ofs' =
1112    match load_store_classification chunk b ofs chunk' b' ofs' with
1113    [ lsc_similar _ _ _ ⇒ Some ? (load_result chunk' v)
1114    | lsc_other _ ⇒ load chunk' m1 r' b' ofs'
1115    | lsc_overlap _ _ _ _ ⇒ Some ? Vundef
1116    | lsc_mismatch _ _ _ ⇒ Some ? Vundef ].
1117#chunk #m1 #r #b #ofs #v #m2 #STORE
1118#chunk' #r' #b' #ofs' #Hvalid
1119cut (∃v'. load chunk' m2 r' b' ofs' = Some ? v')
1120[@valid_access_load
1121   @(store_valid_access_1 … STORE … Hvalid)
1122|*;#x #Hx
1123   cases (load_store_classification chunk b ofs chunk' b' ofs')
1124   [#H1 #H2 #H3 whd in ⊢ (???%);<H1 <H2
1125      @(load_compat_pointer … r)
1126      [ >(region_store … STORE b)
1127          cases Hvalid; //;
1128      | @(load_store_similar … STORE) //;
1129      ]
1130   |#H1 @(load_store_other … STORE)
1131      cases H1
1132      [*
1133         [#H2 % % @sym_neq //
1134         |#H2 % %{2} //]
1135      |#H2 %{2} //]
1136   |#H1 #H2 #H3 #H4 lapply (load_compat_pointer … r … Hx);
1137     [ >(region_store … STORE b')
1138         >H1 elim (store_valid_access_3 … STORE); //
1139     | <H1 in ⊢ (% → ?) #Hx'
1140         <H1 in Hx #Hx >Hx
1141      @(eq_f … (Some val)) @(load_store_overlap … STORE … Hx') /2/;
1142     ]
1143   |#H1 #H2 #H3
1144       lapply (load_compat_pointer … r … Hx);
1145       [ >(region_store … STORE b')
1146           >H1 elim (store_valid_access_3 … STORE); //
1147       | <H1 in Hx ⊢ % <H2 #Hx #Hx'
1148           >Hx @(eq_f … (Some val))
1149           @(load_store_mismatch … STORE … Hx') /2/
1150       ]
1151   ]
1152           
1153]
1154qed.
1155
1156(*lemma d : ∀a,b,c,d:nat.∀e:〈a,b〉 = 〈c,d〉. ∀P:(∀a,b,c,d,e.Prop).
1157           P a b c d e → P a b a b (refl ??).
1158#a #b #c #d #e #P #H1 destruct;*)
1159
1160(*
1161Section ALLOC.
1162
1163Variable m1: mem.
1164Variables lo hi: Z.
1165Variable m2: mem.
1166Variable b: block.
1167Hypothesis ALLOC: alloc m1 lo hi = (m2, b).
1168*)
1169
1170definition pairdisc ≝
1171λA,B.λx,y:Prod A B.
1172match x with
1173[(pair t0 t1) ⇒
1174match y with
1175[(pair u0 u1) ⇒
1176  ∀P: Type[1].
1177  (∀e0: (eq A (R0 ? t0) u0).
1178   ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].
1179
1180lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
1181#A #B #x #y #e >e cases y;
1182#a #b normalize;#P #PH @PH %
1183qed.
1184
1185lemma nextblock_alloc:
1186  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1187  nextblock m2 = Zsucc (nextblock m1).
1188#m1 #lo #hi #bcl #m2 #b #ALLOC
1189whd in ALLOC:(??%%); destruct; //;
1190qed.
1191
1192lemma alloc_result:
1193  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1194  b = nextblock m1.
1195#m1 #lo #hi #bcl #m2 #b #ALLOC
1196whd in ALLOC:(??%%); destruct; //;
1197qed.
1198
1199
1200lemma valid_block_alloc:
1201  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1202  ∀b'. valid_block m1 b' → valid_block m2 b'.
1203#m1 #lo #hi #bcl #m2 #b #ALLOC
1204#b' >(unfold_valid_block m1 b')
1205>(unfold_valid_block m2 b')
1206>(nextblock_alloc … ALLOC)
1207(* arith *) @daemon
1208qed.
1209
1210lemma fresh_block_alloc:
1211  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1212  ¬(valid_block m1 b).
1213#m1 #lo #hi #bcl #m2 #b #ALLOC
1214>(unfold_valid_block m1 b)
1215>(alloc_result … ALLOC)
1216(* arith *) @daemon
1217qed.
1218
1219lemma valid_new_block:
1220  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1221  valid_block m2 b.
1222#m1 #lo #hi #bcl #m2 #b #ALLOC
1223>(unfold_valid_block m2 b)
1224>(alloc_result … ALLOC)
1225>(nextblock_alloc … ALLOC)
1226(* arith *) @daemon
1227qed.
1228
1229(*
1230Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
1231*)
1232
1233lemma valid_block_alloc_inv:
1234  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1235  ∀b'. valid_block m2 b' → b' = b ∨ valid_block m1 b'.
1236#m1 #lo #hi #bcl #m2 #b #ALLOC
1237#b'
1238>(unfold_valid_block m2 b')
1239>(unfold_valid_block m1 b')
1240>(nextblock_alloc … ALLOC) #H
1241>(alloc_result … ALLOC)
1242(* arith *) @daemon
1243qed.
1244
1245lemma low_bound_alloc:
1246  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1247  ∀b'. low_bound m2 b' = if eqZb b' b then lo else low_bound m1 b'.
1248#m1 #lo #hi #bcl #m2 #b #ALLOC
1249whd in ALLOC:(??%%); destruct; #b'
1250>(unfold_update block_contents ????)
1251cases (eqZb b' (nextblock m1)); //;
1252qed.
1253
1254lemma low_bound_alloc_same:
1255  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1256  low_bound m2 b = lo.
1257#m1 #lo #hi #bcl #m2 #b #ALLOC
1258>(low_bound_alloc … ALLOC b)
1259>(eqZb_z_z …)
1260//;
1261qed.
1262
1263lemma low_bound_alloc_other:
1264  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1265  ∀b'. valid_block m1 b' → low_bound m2 b' = low_bound m1 b'.
1266#m1 #lo #hi #bcl #m2 #b #ALLOC
1267#b' >(low_bound_alloc … ALLOC b')
1268@eqZb_elim #Hb
1269[ >Hb #bad @False_ind @(absurd ? bad)
1270    napply (fresh_block_alloc … ALLOC)
1271| //
1272] qed.
1273
1274lemma high_bound_alloc:
1275  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1276  ∀b'. high_bound m2 b' = if eqZb b' b then hi else high_bound m1 b'.
1277#m1 #lo #hi #bcl #m2 #b #ALLOC
1278whd in ALLOC:(??%%); destruct; #b'
1279>(unfold_update block_contents ????)
1280cases (eqZb b' (nextblock m1)); //;
1281qed.
1282
1283lemma high_bound_alloc_same:
1284  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1285  high_bound m2 b = hi.
1286#m1 #lo #hi #bcl #m2 #b #ALLOC
1287>(high_bound_alloc … ALLOC b)
1288>(eqZb_z_z …)
1289//;
1290qed.
1291
1292lemma high_bound_alloc_other:
1293  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1294  ∀b'. valid_block m1 b' → high_bound m2 b' = high_bound m1 b'.
1295#m1 #lo #hi #bcl #m2 #b #ALLOC
1296#b' >(high_bound_alloc … ALLOC b')
1297@eqZb_elim #Hb
1298[ >Hb #bad @False_ind @(absurd ? bad)
1299    napply (fresh_block_alloc … ALLOC)
1300| //
1301] qed.
1302
1303lemma class_alloc:
1304  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1305  ∀b'.block_region m2 b' = if eqZb b' b then bcl else block_region m1 b'.
1306#m1 #lo #hi #bcl #m2 #b #ALLOC
1307whd in ALLOC:(??%%); destruct; #b'
1308cases (eqZb b' (nextblock m1)); //;
1309qed.
1310
1311lemma class_alloc_same:
1312  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1313  block_region m2 b = bcl.
1314#m1 #lo #hi #bcl #m2 #b #ALLOC
1315whd in ALLOC:(??%%); destruct;
1316>(eqZb_z_z ?) //;
1317qed.
1318
1319lemma class_alloc_other:
1320  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1321  ∀b'. valid_block m1 b' → block_region m2 b' = block_region m1 b'.
1322#m1 #lo #hi #bcl #m2 #b #ALLOC
1323#b' >(class_alloc … ALLOC b')
1324@eqZb_elim #Hb
1325[ >Hb #bad @False_ind @(absurd ? bad)
1326    napply (fresh_block_alloc … ALLOC)
1327| //
1328] qed.
1329
1330lemma valid_access_alloc_other:
1331  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1332  ∀chunk,r,b',ofs.
1333  valid_access m1 chunk r b' ofs →
1334  valid_access m2 chunk r b' ofs.
1335#m1 #lo #hi #bcl #m2 #b #ALLOC
1336#chunk #r #b' #ofs #H
1337cases H; #Hvalid #Hlow #Hhigh #Halign #Hcompat
1338%
1339[ @(valid_block_alloc … ALLOC) //
1340| >(low_bound_alloc_other … ALLOC b' Hvalid) //
1341| >(high_bound_alloc_other … ALLOC b' Hvalid) //
1342| //
1343| >(class_alloc_other … ALLOC b' Hvalid) //;
1344] qed.
1345
1346lemma valid_access_alloc_same:
1347  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1348  ∀chunk,r,ofs.
1349  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
1350  pointer_compat bcl r →
1351  valid_access m2 chunk r b ofs.
1352#m1 #lo #hi #bcl #m2 #b #ALLOC
1353#chunk #r #ofs #Hlo #Hhi #Halign #Hcompat
1354%
1355[ napply (valid_new_block … ALLOC)
1356| >(low_bound_alloc_same … ALLOC) //
1357| >(high_bound_alloc_same … ALLOC) //
1358| //
1359| >(class_alloc_same … ALLOC) //
1360] qed.
1361
1362(*
1363Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
1364*)
1365
1366lemma valid_access_alloc_inv:
1367  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1368  ∀chunk,r,b',ofs.
1369  valid_access m2 chunk r b' ofs →
1370  valid_access m1 chunk r b' ofs ∨
1371  (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl r)).
1372#m1 #lo #hi #bcl #m2 #b #ALLOC
1373#chunk #r #b' #ofs *;#Hblk #Hlo #Hhi #Hal #Hct
1374elim (valid_block_alloc_inv … ALLOC ? Hblk);#H
1375[ <H in ALLOC ⊢ % #ALLOC'
1376    >(low_bound_alloc_same … ALLOC') in Hlo #Hlo'
1377    >(high_bound_alloc_same … ALLOC') in Hhi #Hhi'
1378    >(class_alloc_same … ALLOC') in Hct #Hct
1379    %{2} /4/;
1380| %{1} % //;
1381  [ >(low_bound_alloc_other … ALLOC ??) in Hlo //
1382  | >(high_bound_alloc_other … ALLOC ??) in Hhi //
1383  | >(class_alloc_other … ALLOC ??) in Hct //
1384  ]
1385] qed.
1386
1387theorem load_alloc_unchanged:
1388  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 →
1389  ∀chunk,r,b',ofs.
1390  valid_block m1 b' →
1391  load chunk m2 r b' ofs = load chunk m1 r b' ofs.
1392#m1 #lo #hi #bcl #m2 #b #ALLOC
1393#chunk #r #b' #ofs #H whd in ⊢ (??%%);
1394cases (in_bounds m2 chunk r b' ofs); #H'
1395[ elim (valid_access_alloc_inv … ALLOC ???? H');
1396  [ #H'' (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error
1397  >(in_bounds_true ???? ??? H'') *) >(in_bounds_true … ? (option val) ?? H'')
1398      whd in ⊢ (??%?); (* XXX: if you do this at the point below the proof term is ill-typed. *)
1399      cut (b' ≠ b);
1400      [ @(valid_not_valid_diff … H) @(fresh_block_alloc … ALLOC)
1401      | whd in ALLOC:(??%%); destruct;
1402          >(update_o block_contents ?????) /2/;
1403      ]
1404  | *;*;#A #B #C <A in ALLOC ⊢ % #ALLOC
1405      @False_ind @(absurd ? H) napply (fresh_block_alloc … ALLOC)
1406  ]
1407| cases (in_bounds m1 chunk r b' ofs); #H'' whd in ⊢ (??%%); //;
1408    @False_ind @(absurd ? ? H') @(valid_access_alloc_other … ALLOC) //
1409] qed.
1410 
1411theorem load_alloc_other:
1412  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1413  ∀chunk,r,b',ofs,v.
1414  load chunk m1 r b' ofs = Some ? v →
1415  load chunk m2 r b' ofs = Some ? v.
1416#m1 #lo #hi #bcl #m2 #b #ALLOC
1417#chunk #r #b' #ofs #v #H
1418<H @(load_alloc_unchanged … ALLOC ???) cases (load_valid_access … H); //;
1419qed.
1420
1421theorem load_alloc_same:
1422  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1423  ∀chunk,r,ofs,v.
1424  load chunk m2 r b ofs = Some ? v →
1425  v = Vundef.
1426#m1 #lo #hi #bcl #m2 #b #ALLOC
1427#chunk #r #ofs #v #H
1428elim (load_inv … H); #H0 #H1 >H1
1429 whd in ALLOC:(??%%); (* XXX destruct; ??? *) @(pairdisc_elim … ALLOC)
1430 whd in ⊢ (??%% → ?);#e0 <e0 in ⊢ (%→?)
1431 whd in ⊢ (??%% → ?);#e1
1432<e1 <e0 >(update_s ? ? (empty_block lo hi bcl) ?)
1433normalize; cases chunk; //;
1434qed.
1435
1436theorem load_alloc_same':
1437  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
1438  ∀chunk,r,ofs.
1439  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
1440  pointer_compat bcl r →
1441  load chunk m2 r b ofs = Some ? Vundef.
1442#m1 #lo #hi #bcl #m2 #b #ALLOC
1443#chunk #r #ofs #Hlo #Hhi #Hal #Hct
1444cut (∃v. load chunk m2 r b ofs = Some ? v);
1445[ @valid_access_load % //;
1446  [ @(valid_new_block … ALLOC)
1447  | >(low_bound_alloc_same … ALLOC) //
1448  | >(high_bound_alloc_same … ALLOC) //
1449  | >(class_alloc_same … ALLOC) //
1450  ]
1451| *; #v #LOAD >LOAD @(eq_f … (Some val))
1452    @(load_alloc_same … ALLOC … LOAD)
1453] qed.
1454
1455(*
1456End ALLOC.
1457
1458Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
1459Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
1460Hint Resolve load_alloc_unchanged: mem.
1461
1462*)
1463
1464(* ** Properties related to [free]. *)
1465(*
1466Section FREE.
1467
1468Variable m: mem.
1469Variable bf: block.
1470*)
1471
1472lemma valid_block_free_1:
1473  ∀m,bf,b. valid_block m b → valid_block (free m bf) b.
1474normalize;//;
1475qed.
1476
1477lemma valid_block_free_2:
1478  ∀m,bf,b. valid_block (free m bf) b → valid_block m b.
1479normalize;//;
1480qed.
1481
1482(*
1483Hint Resolve valid_block_free_1 valid_block_free_2: mem.
1484*)
1485
1486lemma low_bound_free:
1487  ∀m,bf,b. b ≠ bf -> low_bound (free m bf) b = low_bound m b.
1488#m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
1489>(update_o block_contents …) //; @sym_neq //;
1490qed.
1491
1492lemma high_bound_free:
1493  ∀m,bf,b. b ≠ bf → high_bound (free m bf) b = high_bound m b.
1494#m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
1495>(update_o block_contents …) //; @sym_neq //;
1496qed.
1497
1498lemma low_bound_free_same:
1499  ∀m,b. low_bound (free m b) b = 0.
1500#m #b whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
1501>(update_s block_contents …) //;
1502qed.
1503
1504lemma high_bound_free_same:
1505  ∀m,b. high_bound (free m b) b = 0.
1506#m #b whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
1507>(update_s block_contents …) //;
1508qed.
1509
1510lemma class_free:
1511  ∀m,bf,b. b ≠ bf → block_region (free m bf) b = block_region m b.
1512#m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
1513>(update_o block_contents …) //; @sym_neq //;
1514qed.
1515
1516lemma valid_access_free_1:
1517  ∀m,bf,chunk,r,b,ofs.
1518  valid_access m chunk r b ofs → b ≠ bf →
1519  valid_access (free m bf) chunk r b ofs.
1520#m #bf #chunk #r #b #ofs *;#Hval #Hlo #Hhi #Hal #Hcompat #Hneq
1521% //;
1522[ @valid_block_free_1 //
1523| >(low_bound_free … Hneq) //
1524| >(high_bound_free … Hneq) //
1525| >(class_free … Hneq) //
1526] qed.
1527
1528lemma valid_access_free_2:
1529  ∀m,r,bf,chunk,ofs. ¬(valid_access (free m bf) chunk r bf ofs).
1530#m #r #bf #chunk #ofs @nmk *; #Hval #Hlo #Hhi #Hal #Hct
1531whd in Hlo:(?%?);whd in Hlo:(?(?(?%?))?); >(update_s block_contents …) in Hlo
1532whd in Hhi:(??%);whd in Hhi:(??(?(?%?))); >(update_s block_contents …) in Hhi
1533whd in ⊢ ((??%)→(?%?)→?); (* arith *) @daemon
1534qed.
1535
1536(*
1537Hint Resolve valid_access_free_1 valid_access_free_2: mem.
1538*)
1539
1540lemma valid_access_free_inv:
1541  ∀m,bf,chunk,r,b,ofs.
1542  valid_access (free m bf) chunk r b ofs →
1543  valid_access m chunk r b ofs ∧ b ≠ bf.
1544#m #bf #chunk #r #b #ofs elim (decidable_eq_Z_Type b bf);
1545[ #e >e
1546    #H @False_ind @(absurd ? H (valid_access_free_2 …))
1547| #ne *; >(low_bound_free … ne)
1548    >(high_bound_free … ne)
1549    >(class_free … ne)
1550    #Hval #Hlo #Hhi #Hal #Hct
1551    % [ % /2/; | /2/ ]
1552] qed.
1553
1554theorem load_free:
1555  ∀m,bf,chunk,r,b,ofs.
1556  b ≠ bf →
1557  load chunk (free m bf) r b ofs = load chunk m r b ofs.
1558#m #bf #chunk #r #b #ofs #ne whd in ⊢ (??%%);
1559elim (in_bounds m chunk r b ofs);
1560[ #Hval whd in ⊢ (???%); >(in_bounds_true ????? (option val) ???)
1561  [ whd in ⊢ (??(??(??(???(?(?%?)))))?); >(update_o block_contents …) //;
1562      @sym_neq //
1563  | @valid_access_free_1 //; @ne
1564  ]
1565| elim (in_bounds (free m bf) chunk r b ofs); (* XXX just // used to work *) [ 2: normalize; //; ]
1566    #H #H' @False_ind @(absurd ? ? H')
1567    elim (valid_access_free_inv …H); //;
1568] qed.
1569
1570(*
1571End FREE.
1572*)
1573
1574(* ** Properties related to [free_list] *)
1575
1576lemma valid_block_free_list_1:
1577  ∀bl,m,b. valid_block m b → valid_block (free_list m bl) b.
1578#bl elim bl;
1579[ #m #b #H whd in ⊢ (?%?); //
1580| #h #t #IH #m #b #H >(unfold_free_list m h t)
1581    @valid_block_free_1 @IH //
1582] qed.
1583
1584lemma valid_block_free_list_2:
1585  ∀bl,m,b. valid_block (free_list m bl) b → valid_block m b.
1586#bl elim bl;
1587[ #m #b #H whd in H:(?%?); //
1588| #h #t #IH #m #b >(unfold_free_list m h t) #H
1589    @IH @valid_block_free_2 //
1590] qed.
1591
1592lemma valid_access_free_list:
1593  ∀chunk,r,b,ofs,m,bl.
1594  valid_access m chunk r b ofs → ¬in_list ? b bl →
1595  valid_access (free_list m bl) chunk r b ofs.
1596#chunk #r #b #ofs #m #bl elim bl;
1597[ whd in ⊢ (?→?→(?%????)); //
1598| #h #t #IH #H #notin >(unfold_free_list m h t) @valid_access_free_1
1599    [ @IH //; @(not_to_not ??? notin) #Ht napply (in_list_cons … Ht)
1600    | @nmk #e @(absurd ?? notin) >e // ]
1601] qed.
1602
1603lemma valid_access_free_list_inv:
1604  ∀chunk,r,b,ofs,m,bl.
1605  valid_access (free_list m bl) chunk r b ofs →
1606  ¬in_list ? b bl ∧ valid_access m chunk r b ofs.
1607#chunk #r #b #ofs #m #bl elim bl;
1608[ whd in ⊢ ((?%????)→?); #H % //
1609| #h #t #IH >(unfold_free_list m h t) #H
1610    elim (valid_access_free_inv … H); #H' #ne
1611    elim (IH H'); #notin #H'' % //;
1612    @(not_to_not ??? notin) #Ht
1613    (* WTF? this is specialised to nat! @(in_list_tail t b h) *) napply daemon
1614] qed.
1615
1616(* ** Properties related to pointer validity *)
1617
1618lemma valid_pointer_valid_access:
1619  ∀m,r,b,ofs.
1620  valid_pointer m r b ofs = true ↔ valid_access m Mint8unsigned r b ofs.
1621#m #r #b #ofs whd in ⊢ (?(??%?)?); %
1622[ #H
1623    lapply (andb_true_l … H); #H'
1624    lapply (andb_true_l … H'); #H''
1625    lapply (andb_true_l … H''); #H1
1626    lapply (andb_true_r … H''); #H2
1627    lapply (andb_true_r … H'); #H3
1628    lapply (andb_true_r … H); #H4
1629    %
1630    [ >(unfold_valid_block m b) napply (Zltb_true_to_Zlt … H1)
1631    | napply (Zleb_true_to_Zle … H2)
1632    | whd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
1633    | cases ofs; /2/;
1634    | whd in H4:(??%?); elim (pointer_compat_dec (block_region m b) r) in H4;
1635        [ //; | #Hn #e whd in e:(??%%); destruct ]
1636    ]
1637| *; #Hval #Hlo #Hhi #Hal #Hct
1638    >(Zlt_to_Zltb_true … Hval)
1639    >(Zle_to_Zleb_true … Hlo)
1640    whd in Hhi:(?(??%)?); >(Zlt_to_Zltb_true … ?)
1641    [ whd in ⊢ (??%?); elim (pointer_compat_dec (block_region m b) r);
1642      [ //;
1643      | #Hct' @False_ind @(absurd … Hct Hct')
1644      ]
1645    | (* arith *) napply daemon
1646    ]
1647]
1648 qed.
1649
1650theorem valid_pointer_alloc:
1651  ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,r. ∀b,b': block. ∀ofs: Z.
1652  alloc m1 lo hi bcl = 〈m2, b'〉 →
1653  valid_pointer m1 r b ofs = true →
1654  valid_pointer m2 r b ofs = true.
1655#m1 #m2 #lo #hi #bcl #r #b #b' #ofs #ALLOC #VALID
1656lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval
1657@(proj2 ?? (valid_pointer_valid_access ????))
1658@(valid_access_alloc_other … ALLOC … Hval)
1659qed.
1660
1661theorem valid_pointer_store:
1662  ∀chunk: memory_chunk. ∀m1,m2: mem.
1663  ∀r,r': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
1664  store chunk m1 r' b' ofs' v = Some ? m2 →
1665  valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true.
1666#chunk #m1 #m2 #r #r' #b #b' #ofs #ofs' #v #STORE #VALID
1667lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval
1668@(proj2 ?? (valid_pointer_valid_access ????))
1669@(store_valid_access_1 … STORE … Hval)
1670qed.
1671
1672(* * * Generic injections between memory states. *)
1673(*
1674(* Section GENERIC_INJECT. *)
1675
1676definition meminj : Type[0] ≝ block → option (block × Z).
1677(*
1678Variable val_inj: meminj -> val -> val -> Prop.
1679
1680Hypothesis val_inj_undef:
1681  ∀mi. val_inj mi Vundef Vundef.
1682*)
1683
1684definition mem_inj ≝ λval_inj.λmi: meminj. λm1,m2: mem.
1685  ∀chunk, b1, ofs, v1, b2, delta.
1686  mi b1 = Some ? 〈b2, delta〉 →
1687  load chunk m1 b1 ofs = Some ? v1 →
1688  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2.
1689
1690(* FIXME: another nunfold hack*)
1691lemma unfold_mem_inj : ∀val_inj.∀mi: meminj. ∀m1,m2: mem.
1692  (mem_inj val_inj mi m1 m2) =
1693  (∀chunk, b1, ofs, v1, b2, delta.
1694  mi b1 = Some ? 〈b2, delta〉 →
1695  load chunk m1 b1 ofs = Some ? v1 →
1696  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2).
1697//; qed.
1698
1699lemma valid_access_inj: ∀val_inj.
1700  ∀mi,m1,m2,chunk,b1,ofs,b2,delta.
1701  mi b1 = Some ? 〈b2, delta〉 →
1702  mem_inj val_inj mi m1 m2 →
1703  valid_access m1 chunk b1 ofs →
1704  valid_access m2 chunk b2 (ofs + delta).
1705#val_inj
1706#mi #m1 #m2 #chunk #b1 #ofs #b2 #delta #H #Hinj #Hval
1707cut (∃v1. load chunk m1 b1 ofs = Some ? v1);
1708[ /2/;
1709| *;#v1 #LOAD1
1710    elim (Hinj … H LOAD1);#v2 *;#LOAD2 #VCP
1711    /2/
1712] qed.
1713
1714(*Hint Resolve valid_access_inj: mem.*)
1715*)
1716(* FIXME: can't use destruct below *)
1717lemma grumpydestruct : ∀A,v. None A = Some A v → False.
1718#A #v #H destruct;
1719qed.
1720(*
1721lemma store_unmapped_inj: ∀val_inj.
1722  ∀mi,m1,m2,r,b,ofs,v,chunk,m1'.
1723  mem_inj val_inj mi m1 m2 →
1724  mi b = None ? →
1725  store chunk m1 r b ofs v = Some ? m1' →
1726  mem_inj val_inj mi m1' m2.
1727#val_inj
1728#mi #m1 #m2 #r #b #ofs #v #chunk #m1' #Hinj #Hmi #Hstore
1729whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload
1730cut (load chunk0 m1 b1 ofs0 = Some ? v1);
1731[ <Hload @sym_eq @(load_store_other … Hstore)
1732    %{1} %{1} @nmk #eq >eq in Hmi0 >Hmi #H destruct;
1733| #Hload' @(Hinj … Hmi0 Hload')
1734] qed.
1735
1736lemma store_outside_inj: ∀val_inj.
1737  ∀mi,m1,m2,chunk,r,b,ofs,v,m2'.
1738  mem_inj val_inj mi m1 m2 →
1739  (∀b',delta.
1740    mi b' = Some ? 〈b, delta〉 →
1741    high_bound m1 b' + delta ≤ ofs
1742    ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) →
1743  store chunk m2 r b ofs v = Some ? m2' →
1744  mem_inj val_inj mi m1 m2'.
1745#val_inj
1746#mi #m1 #m2 #chunk #r #b #ofs #v #m2' #Hinj #Hbounds #Hstore
1747whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload
1748lapply (Hinj … Hmi0 Hload);*;#v2 *;#LOAD2 #VINJ
1749%{ v2} % //;
1750<LOAD2 @(load_store_other … Hstore)
1751elim (decidable_eq_Z b2 b);
1752[ #Heq >Heq in Hmi0 LOAD2 #Hmi0 #LOAD2
1753    lapply (Hbounds … Hmi0); #Hb
1754    cut (valid_access m1 chunk0 b1 ofs0); /2/;
1755    #Hv elim Hv; #Hv1 #Hlo1 #Hhi1 #Hal1
1756    elim Hb; #Hb [ %{1} %{2} (* arith *) napply daemon | %{2} (* arith *) napply daemon ]
1757| #ineq %{1} %{1} @ineq
1758] qed.
1759
1760(* XXX: use Or rather than ∨ to bring resource usage under control. *)
1761definition meminj_no_overlap ≝ λmi: meminj. λm: mem.
1762  ∀b1,b1',delta1,b2,b2',delta2.
1763  b1 ≠ b2 →
1764  mi b1 = Some ? 〈b1', delta1〉 →
1765  mi b2 = Some ? 〈b2', delta2〉 →
1766  Or (Or (Or (b1' ≠ b2')
1767             (low_bound m b1 ≥ high_bound m b1))
1768         (low_bound m b2 ≥ high_bound m b2))
1769  (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2)
1770      (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)).
1771*)
1772(* FIXME *)
1773lemma grumpydestruct1 : ∀A,x1,x2. Some A x1 = Some A x2 → x1 = x2.
1774#A #x1 #x2 #H destruct;//;
1775qed.
1776lemma grumpydestruct2 : ∀A,B,x1,y1,x2,y2. Some (A×B) 〈x1,y1〉 = Some (A×B) 〈x2,y2〉 → x1 = x2 ∧ y1 = y2.
1777#A #B #x1 #y1 #x2 #y2 #H destruct;/2/;
1778qed.
1779(*
1780lemma store_mapped_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef.
1781  ∀mi,m1,m2,b1,ofs,b2,delta,v1,v2,chunk,m1'.
1782  mem_inj val_inj mi m1 m2 →
1783  meminj_no_overlap mi m1 →
1784  mi b1 = Some ? 〈b2, delta〉 →
1785  store chunk m1 b1 ofs v1 = Some ? m1' →
1786  (∀chunk'. size_chunk chunk' = size_chunk chunk →
1787    val_inj mi (load_result chunk' v1) (load_result chunk' v2)) →
1788  ∃m2'.
1789  store chunk m2 b2 (ofs + delta) v2 = Some ? m2' ∧ mem_inj val_inj mi m1' m2'.
1790#val_inj #val_inj_undef
1791#mi #m1 #m2 #b1 #ofs #b2 #delta #v1 #v2 #chunk #m1'
1792#Hinj #Hnoover #Hb1 #STORE #Hvalinj
1793cut (∃m2'.store chunk m2 b2 (ofs + delta) v2 = Some ? m2');
1794[ @valid_access_store @(valid_access_inj ? mi ??????? Hb1 Hinj ?) (* XXX why do I have to give mi here? *) /2/
1795| *;#m2' #STORE2
1796    %{ m2'} % //;
1797    whd; #chunk' #b1' #ofs' #v #b2' #delta' #CP #LOAD1
1798    cut (valid_access m1 chunk' b1' ofs');
1799    [ @(store_valid_access_2 … STORE) @(load_valid_access … LOAD1)
1800    | #Hval
1801        lapply (load_store_characterization … STORE … Hval);
1802        elim (load_store_classification chunk b1 ofs chunk' b1' ofs');
1803        [ #e #e0 #e1 #H (* similar *)
1804            >e in Hb1 #Hb1
1805            >CP in Hb1 #Hb1 (* XXX destruct expands proof state too much;*)
1806            elim (grumpydestruct2 ?????? Hb1);
1807            #e2 #e3 <e0 >e2 >e3
1808            %{ (load_result chunk' v2)} %
1809            [ @(load_store_similar … STORE2) //
1810            | >LOAD1 in H #H whd in H:(??%%); destruct;
1811                @Hvalinj //;
1812            ]
1813         | #Hdis #H (* disjoint *)
1814             >LOAD1 in H #H
1815             lapply (Hinj … CP ?); [ @sym_eq @H | *: ]
1816             *;#v2' *;#LOAD2 #VCP
1817             %{ v2'} % //;
1818             <LOAD2 @(load_store_other … STORE2)
1819             elim (decidable_eq_Z b1 b1'); #eb1
1820             [ <eb1 in CP #CP >CP in Hb1 #eb2d
1821                 elim (grumpydestruct2 ?????? eb2d); #eb2 #ed
1822                 elim Hdis; [ #Hdis elim Hdis;
1823                               [ #eb1' @False_ind @(absurd ? eb1 eb1')
1824                               | #Hdis %{1} %{2} (* arith *) napply daemon
1825                               ] | #Hdis %{2} (* arith *) napply daemon ]
1826             | cut (valid_access m1 chunk b1 ofs); /2/; #Hval'
1827                 lapply (Hnoover … eb1 Hb1 CP);
1828                 #Ha elim Ha; #Ha
1829                 [ elim Ha; #Ha
1830                 [ elim Ha; #Ha
1831                 [ %{1} %{1} /2/
1832                 | elim Hval'; lapply (size_chunk_pos chunk); (* arith *) napply daemon ]
1833                 | elim Hval; lapply (size_chunk_pos chunk'); (* arith *) napply daemon ]
1834                 | elim Hval'; elim Hval;  (* arith *) napply daemon ]
1835             ]
1836         | #eb1 #Hofs1 #Hofs2 #Hofs3 #H (* overlapping *)
1837             <eb1 in CP #CP >CP in Hb1 #eb2d
1838             elim (grumpydestruct2 ?????? eb2d); #eb2 #ed
1839             cut (∃v2'. load chunk' m2' b2 (ofs' + delta) = Some ? v2');
1840             [ @valid_access_load @(store_valid_access_1 … STORE2) @(valid_access_inj … Hinj Hval) >eb1 //
1841             | *;#v2' #LOAD2'
1842                 cut (v2' = Vundef); [ @(load_store_overlap … STORE2 … LOAD2') (* arith *) napply daemon | ]
1843                 #ev2' %{ v2'} % //;
1844                 >LOAD1 in H #H whd in H:(??%%); >(grumpydestruct1 … H)
1845                 >ev2'
1846                 @val_inj_undef ]
1847         | #eb1 #Hofs <Hofs in Hval LOAD1 ⊢ % #Hval #LOAD1 #Hsize #H (* overlapping *)
1848             
1849             <eb1 in CP #CP >CP in Hb1 #eb2d
1850             elim (grumpydestruct2 ?????? eb2d); #eb2 #ed
1851             cut (∃v2'. load chunk' m2' b2 (ofs + delta) = Some ? v2');
1852             [ @valid_access_load @(store_valid_access_1 … STORE2) @(valid_access_inj … Hinj Hval) >eb1 //
1853             | *;#v2' #LOAD2'
1854                 cut (v2' = Vundef); [ @(load_store_mismatch … STORE2 … LOAD2' ?) @sym_neq // | ]
1855                 #ev2' %{ v2'} % //;
1856                 >LOAD1 in H #H whd in H:(??%%); >(grumpydestruct1 … H)
1857                 >ev2'
1858                 @val_inj_undef ]
1859         ]
1860     ]
1861] qed.
1862
1863definition inj_offset_aligned ≝ λdelta: Z. λsize: Z.
1864  ∀chunk. size_chunk chunk ≤ size → (align_chunk chunk ∣ delta).
1865
1866lemma alloc_parallel_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef.
1867  ∀mi,m1,m2,lo1,hi1,m1',b1,lo2,hi2,m2',b2,delta.
1868  mem_inj val_inj mi m1 m2 →
1869  alloc m1 lo1 hi1 = 〈m1', b1〉 →
1870  alloc m2 lo2 hi2 = 〈m2', b2〉 →
1871  mi b1 = Some ? 〈b2, delta〉 →
1872  lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 →
1873  inj_offset_aligned delta (hi1 - lo1) →
1874  mem_inj val_inj mi m1' m2'.
1875#val_inj #val_inj_undef
1876#mi #m1 #m2 #lo1 #hi1 #m1' #b1 #lo2 #hi2 #m2' #b2 #delta
1877#Hinj #ALLOC1 #ALLOC2 #Hbinj #Hlo #Hhi #Hal
1878whd; #chunk #b1' #ofs #v #b2' #delta' #Hbinj' #LOAD
1879lapply (valid_access_alloc_inv … m1 … ALLOC1 chunk b1' ofs ?); /2/;
1880*;
1881[ #A
1882    cut (load chunk m1 b1' ofs = Some ? v);
1883    [ <LOAD @sym_eq @(load_alloc_unchanged … ALLOC1) /2/; ]
1884    #LOAD0 lapply (Hinj … Hbinj' LOAD0); *;#v2 *;#LOAD2 #VINJ
1885    %{ v2} %
1886    [ <LOAD2 @(load_alloc_unchanged … ALLOC2)
1887        @valid_access_valid_block [ 3: @load_valid_access ]
1888        //
1889    | //
1890    ]
1891| *;*;#A #B #C
1892    >A in Hbinj' LOAD #Hbinj' #LOAD
1893    >Hbinj in Hbinj' #Hbinj' elim (grumpydestruct2 ?????? Hbinj');
1894    #eb2 #edelta <eb2 <edelta
1895    cut (v = Vundef); [ @(load_alloc_same … ALLOC1 … LOAD) ]
1896    #ev >ev
1897    cut (∃v2. load chunk m2' b2 (ofs + delta) = Some ? v2);
1898    [ @valid_access_load
1899        @(valid_access_alloc_same … ALLOC2)
1900        [ 1,2: (*arith*) @daemon
1901        | (* arith using Hal *) napply daemon
1902        ] ]
1903    *;#v2 #LOAD2
1904    cut (v2 = Vundef); [ napply (load_alloc_same … ALLOC2 … LOAD2) ]
1905    #ev2 >ev2
1906    %{ Vundef} % //;
1907] qed.
1908
1909lemma alloc_right_inj: ∀val_inj.
1910  ∀mi,m1,m2,lo,hi,b2,m2'.
1911  mem_inj val_inj mi m1 m2 →
1912  alloc m2 lo hi = 〈m2', b2〉 →
1913  mem_inj val_inj mi m1 m2'.
1914#val_inj
1915#mi #m1 #m2 #lo #hi #b2 #m2'
1916#Hinj #ALLOC
1917whd; #chunk #b1 #ofs #v1 #b2' #delta #Hbinj #LOAD
1918lapply (Hinj … Hbinj LOAD); *; #v2 *;#LOAD2 #VINJ
1919%{ v2} % //;
1920cut (valid_block m2 b2');
1921  [ @(valid_access_valid_block ? chunk ? (ofs + delta)) /2/ ]
1922#Hval
1923<LOAD2 @(load_alloc_unchanged … ALLOC … Hval)
1924qed.
1925
1926(*
1927Hypothesis val_inj_undef_any:
1928  ∀mi,v. val_inj mi Vundef v.
1929*)
1930
1931lemma alloc_left_unmapped_inj: ∀val_inj.
1932  ∀mi,m1,m2,lo,hi,b1,m1'.
1933  mem_inj val_inj mi m1 m2 →
1934  alloc m1 lo hi = 〈m1', b1〉 →
1935  mi b1 = None ? →
1936  mem_inj val_inj mi m1' m2.
1937#val_inj
1938#mi #m1 #m2 #lo #hi #b1 #m1'
1939#Hinj #ALLOC #Hbinj
1940whd;  #chunk #b1' #ofs #v1 #b2' #delta #Hbinj' #LOAD
1941lapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
1942*;
1943[ #A
1944  @(Hinj … Hbinj' )
1945  <LOAD @sym_eq @(load_alloc_unchanged … ALLOC) /2/;
1946| *;*;#A #B #C
1947  >A in Hbinj' LOAD #Hbinj' #LOAD
1948  >Hbinj in Hbinj' #bad destruct;
1949] qed.
1950
1951lemma alloc_left_mapped_inj: ∀val_inj.∀val_inj_undef_any:∀mi,v. val_inj mi Vundef v.
1952  ∀mi,m1,m2,lo,hi,b1,m1',b2,delta.
1953  mem_inj val_inj mi m1 m2 →
1954  alloc m1 lo hi = 〈m1', b1〉 →
1955  mi b1 = Some ? 〈b2, delta〉 →
1956  valid_block m2 b2 →
1957  low_bound m2 b2 ≤ lo + delta → hi + delta ≤ high_bound m2 b2 →
1958  inj_offset_aligned delta (hi - lo) →
1959  mem_inj val_inj mi m1' m2.
1960#val_inj #val_inj_undef_any
1961#mi #m1 #m2 #lo #hi #b1 #m1' #b2 #delta
1962#Hinj #ALLOC #Hbinj #Hval #Hlo #Hhi #Hal
1963whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD
1964lapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
1965*;
1966[ #A
1967    @(Hinj … Hbinj')
1968    <LOAD @sym_eq @(load_alloc_unchanged … ALLOC) /2/;
1969| *;*;#A #B *;#C #D
1970    >A in Hbinj' LOAD #Hbinj' #LOAD >Hbinj in Hbinj'
1971    #Hbinj' (* XXX destruct normalizes too much here *) elim (grumpydestruct2 ?????? Hbinj'); #eb2 #edelta
1972    <eb2 <edelta
1973    cut (v1 = Vundef); [ napply (load_alloc_same … ALLOC … LOAD) ]
1974    #ev1 >ev1
1975    cut (∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2);
1976    [ @valid_access_load % //;
1977      [ (* arith *) napply daemon
1978      | (* arith *) napply daemon
1979      | (* arith *) napply daemon
1980      ]
1981    ]
1982    *;#v2 #LOAD2 %{ v2} % //;
1983] qed.
1984
1985lemma free_parallel_inj: ∀val_inj.
1986  ∀mi,m1,m2,b1,b2,delta.
1987  mem_inj val_inj mi m1 m2 →
1988  mi b1 = Some ? 〈b2, delta〉 →
1989  (∀b,delta'. mi b = Some ? 〈b2, delta'〉 → b = b1) →
1990  mem_inj val_inj mi (free m1 b1) (free m2 b2).
1991#val_inj
1992#mi #m1 #m2 #b1 #b2 #delta #Hinj #Hb1inj #Hbinj
1993whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD
1994lapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A #B
1995cut (load chunk m1 b1' ofs = Some ? v1);
1996[ <LOAD @sym_eq @load_free @B ] #LOAD'
1997elim (Hinj … Hbinj' LOAD'); #v2 *;#LOAD2 #INJ
1998%{ v2} %
1999[ <LOAD2 @load_free
2000    @nmk #e @(absurd ?? B)
2001    >e in Hbinj' #Hbinj' @(Hbinj ?? Hbinj')
2002| //
2003] qed.
2004
2005lemma free_left_inj: ∀val_inj.
2006  ∀mi,m1,m2,b1.
2007  mem_inj val_inj mi m1 m2 →
2008  mem_inj val_inj mi (free m1 b1) m2.
2009#val_inj #mi #m1 #m2 #b1 #Hinj
2010whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD
2011lapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A #B
2012@(Hinj … Hbinj')
2013<LOAD @sym_eq @load_free @B
2014qed.
2015
2016lemma free_list_left_inj: ∀val_inj.
2017  ∀mi,bl,m1,m2.
2018  mem_inj val_inj mi m1 m2 →
2019  mem_inj val_inj mi (free_list m1 bl) m2.
2020#val_inj #mi #bl elim bl;
2021[ whd in ⊢ (?→?→?→???%?); //
2022| #h #t #IH #m1 #m2 #H >(unfold_free_list m1 h t)
2023    @free_left_inj @IH //
2024] qed.
2025
2026lemma free_right_inj: ∀val_inj.
2027  ∀mi,m1,m2,b2.
2028  mem_inj val_inj mi m1 m2 →
2029  (∀b1,delta,chunk,ofs.
2030   mi b1 = Some ? 〈b2, delta〉 → ¬(valid_access m1 chunk b1 ofs)) →
2031  mem_inj val_inj mi m1 (free m2 b2).
2032#val_inj #mi #m1 #m2 #b2 #Hinj #Hinval
2033whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD
2034cut (b2' ≠ b2);
2035[ @nmk #e >e in Hbinj' #Hbinj'
2036    @(absurd ?? (Hinval … Hbinj')) @(load_valid_access … LOAD) ]
2037#ne lapply (Hinj … Hbinj' LOAD); *;#v2 *;#LOAD2 #INJ
2038%{ v2} % //;
2039<LOAD2 @load_free @ne
2040qed.
2041
2042lemma valid_pointer_inj: ∀val_inj.
2043  ∀mi,m1,m2,b1,ofs,b2,delta.
2044  mi b1 = Some ? 〈b2, delta〉 →
2045  mem_inj val_inj mi m1 m2 →
2046  valid_pointer m1 b1 ofs = true →
2047  valid_pointer m2 b2 (ofs + delta) = true.
2048#val_inj #mi #m1 #m2 #b1 #ofs #b2 #delta #Hbinj #Hinj #VALID
2049lapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval
2050@(proj2 ?? (valid_pointer_valid_access ???))
2051@(valid_access_inj … Hval) //;
2052qed.
2053
2054(*
2055End GENERIC_INJECT.
2056*)
2057(* ** Store extensions *)
2058
2059(* A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
2060  by increasing the sizes of the memory blocks of [m1] (decreasing
2061  the low bounds, increasing the high bounds), while still keeping the
2062  same contents for block offsets that are valid in [m1]. *)
2063
2064definition inject_id : meminj ≝ λb. Some ? 〈b, OZ〉.
2065
2066definition val_inj_id ≝ λmi: meminj. λv1,v2: val. v1 = v2.
2067
2068definition extends ≝ λm1,m2: mem.
2069  nextblock m1 = nextblock m2 ∧ mem_inj val_inj_id inject_id m1 m2.
2070
2071theorem extends_refl:
2072  ∀m: mem. extends m m.
2073#m % //;
2074whd; #chunk #b1 #ofs #v1 #b2 #delta normalize in ⊢ (%→?);#H
2075(* XXX: destruct makes the goal unreadable *) elim (grumpydestruct2 ?????? H); #eb1 #edelta #LOAD
2076%{ v1} %
2077[ <edelta >(Zplus_z_OZ ofs) //;
2078| //
2079] qed.
2080
2081theorem alloc_extends:
2082  ∀m1,m2,m1',m2': mem. ∀lo1,hi1,lo2,hi2: Z. ∀b1,b2: block.
2083  extends m1 m2 →
2084  lo2 ≤ lo1 → hi1 ≤ hi2 →
2085  alloc m1 lo1 hi1 = 〈m1', b1〉 →
2086  alloc m2 lo2 hi2 = 〈m2', b2〉 →
2087  b1 = b2 ∧ extends m1' m2'.
2088#m1 #m2 #m1' #m2' #lo1 #hi1 #lo2 #hi2 #b1 #b2
2089*;#Hnext #Hinj #Hlo #Hhi #ALLOC1 #ALLOC2
2090cut (b1 = b2);
2091[ @(transitive_eq … (nextblock m1)) [ @(alloc_result … ALLOC1)
2092    | @sym_eq >Hnext napply (alloc_result … ALLOC2) ] ]
2093#eb <eb in ALLOC2 ⊢ % #ALLOC2 % //; %
2094[ >(nextblock_alloc … ALLOC1)
2095    >(nextblock_alloc … ALLOC2)
2096    //;
2097| @(alloc_parallel_inj ??????????????? ALLOC1 ALLOC2 ????)
2098  [ 1,4: normalize; //;
2099  | 3,5,6: //
2100  | 7: whd; #chunk #Hsize (* divides 0 *) napply daemon
2101  ]
2102] qed.
2103
2104theorem free_extends:
2105  ∀m1,m2: mem. ∀b: block.
2106  extends m1 m2 →
2107  extends (free m1 b) (free m2 b).
2108#m1 #m2 #b *;#Hnext #Hinj %
2109[ normalize; //;
2110| @(free_parallel_inj … Hinj)
2111  [ 2: //;
2112  | 3: normalize; #b' #delta #ee destruct; //
2113  ]
2114] qed.
2115
2116theorem load_extends:
2117  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val.
2118  extends m1 m2 →
2119  load chunk m1 r b ofs = Some ? v →
2120  load chunk m2 r b ofs = Some ? v.
2121#chunk #m1 #m2 #r #b #ofs #v
2122*;#Hnext #Hinj #LOAD
2123lapply (Hinj … LOAD); [ normalize; // | 2,3: ]
2124*;#v2 *; >(Zplus_z_OZ ofs) #LOAD2 #EQ whd in EQ;
2125//;
2126qed.
2127
2128theorem store_within_extends:
2129  ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val.
2130  extends m1 m2 →
2131  store chunk m1 r b ofs v = Some ? m1' →
2132  ∃m2'. store chunk m2 r b ofs v = Some ? m2' ∧ extends m1' m2'.
2133#chunk #m1 #m2 #m1' #b #ofs #v *;#Hnext #Hinj #STORE1
2134lapply (store_mapped_inj … Hinj ?? STORE1 ?);
2135[ 1,2,7: normalize; //
2136| (* TODO: unfolding, etc ought to tidy this up *)
2137    whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb #Hinj1 #Hinj2
2138    normalize in Hinj1 Hinj2; %{1} %{1} %{1} destruct; //
2139| 4,5,6: ##skip
2140]
2141*;#m2' *;#STORE #MINJ
2142%{ m2'} % >(Zplus_z_OZ ofs) in STORE #STORE //;
2143%
2144[ >(nextblock_store … STORE1)
2145    >(nextblock_store … STORE)
2146    //
2147| //
2148] qed.
2149
2150theorem store_outside_extends:
2151  ∀chunk: memory_chunk. ∀m1,m2,m2': mem. ∀b: block. ∀ofs: Z. ∀v: val.
2152  extends m1 m2 →
2153  ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs →
2154  store chunk m2 r b ofs v = Some ? m2' →
2155  extends m1 m2'.
2156#chunk #m1 #m2 #m2' #b #ofs #v *;#Hnext #Hinj #Houtside #STORE %
2157[ >(nextblock_store … STORE) //
2158| @(store_outside_inj … STORE) //;
2159    #b' #delta #einj normalize in einj; destruct;
2160    elim Houtside;
2161    [ #lo %{ 2} >(Zplus_z_OZ ?) /2/
2162    | #hi %{ 1}  >(Zplus_z_OZ ?) /2/
2163    ]
2164] qed.
2165
2166theorem valid_pointer_extends:
2167  ∀m1,m2,b,ofs.
2168  extends m1 m2 → valid_pointer m1 r b ofs = true →
2169  valid_pointer m2 r b ofs = true.
2170#m1 #m2 #b #ofs *;#Hnext #Hinj #VALID
2171<(Zplus_z_OZ ofs)
2172@(valid_pointer_inj … Hinj VALID) //;
2173qed.
2174
2175
2176(* * The ``less defined than'' relation over memory states *)
2177
2178(* A memory state [m1] is less defined than [m2] if, for all addresses,
2179  the value [v1] read in [m1] at this address is less defined than
2180  the value [v2] read in [m2], that is, either [v1 = v2] or [v1 = Vundef]. *)
2181
2182definition val_inj_lessdef ≝ λmi: meminj. λv1,v2: val.
2183  Val_lessdef v1 v2.
2184
2185definition lessdef ≝ λm1,m2: mem.
2186  nextblock m1 = nextblock m2 ∧
2187  mem_inj val_inj_lessdef inject_id m1 m2.
2188
2189lemma lessdef_refl:
2190  ∀m. lessdef m m.
2191#m % //;
2192whd; #chunk #b1 #ofs #v1 #b2 #delta #H #LOAD
2193whd in H:(??%?); elim (grumpydestruct2 ?????? H); #eb1 #edelta
2194%{ v1} % //;
2195qed.
2196
2197lemma load_lessdef:
2198  ∀m1,m2,chunk,b,ofs,v1.
2199  lessdef m1 m2 → load chunk m1 r b ofs = Some ? v1 →
2200  ∃v2. load chunk m2 r b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
2201#m1 #m2 #chunk #b #ofs #v1 *;#Hnext #Hinj #LOAD0
2202lapply (Hinj … LOAD0); [ whd in ⊢ (??%?); // | 2,3:##skip ]
2203*;#v2 *;#LOAD #INJ %{ v2} % //;
2204qed.
2205
2206lemma loadv_lessdef:
2207  ∀m1,m2,chunk,addr1,addr2,v1.
2208  lessdef m1 m2 → Val_lessdef addr1 addr2 →
2209  loadv chunk m1 addr1 = Some ? v1 →
2210  ∃v2. loadv chunk m2 addr2 = Some ? v2 ∧ Val_lessdef v1 v2.
2211#m1 #m2 #chunk #addr1 #addr2 #v1 #H #H0 #LOAD
2212inversion H0;
2213[ #v #e1 #e2 >e1 in LOAD cases v;
2214    [ whd in ⊢ ((??%?)→?); #H' destruct;
2215    | 2,3: #v' whd in ⊢ ((??%?)→?); #H' destruct;
2216    | #b' #off @load_lessdef //
2217    ]
2218| #v #e >e in LOAD #LOAD whd in LOAD:(??%?); destruct;
2219] qed.
2220
2221lemma store_lessdef:
2222  ∀m1,m2,chunk,b,ofs,v1,v2,m1'.
2223  lessdef m1 m2 → Val_lessdef v1 v2 →
2224  store chunk m1 r b ofs v1 = Some ? m1' →
2225  ∃m2'. store chunk m2 r b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
2226#m1 #m2 #chunk #b #ofs #v1 #v2 #m1'
2227*;#Hnext #Hinj #Hvless #STORE0
2228lapply (store_mapped_inj … Hinj … STORE0 ?);
2229[ #chunk' #Hsize whd;@load_result_lessdef napply Hvless
2230| whd in ⊢ (??%?); //
2231| whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neq
2232    whd in ⊢ ((??%?)→(??%?)→?); #e1 #e2 destruct;
2233    % % % //
2234| 7: #mi whd; //;
2235| 8: *;#m2' *;#STORE #MINJ
2236         %{ m2'} % /2/;
2237         %
2238         >(nextblock_store … STORE0)
2239         >(nextblock_store … STORE)
2240         //;
2241] qed.
2242
2243lemma storev_lessdef:
2244  ∀m1,m2,chunk,addr1,v1,addr2,v2,m1'.
2245  lessdef m1 m2 → Val_lessdef addr1 addr2 → Val_lessdef v1 v2 →
2246  storev chunk m1 addr1 v1 = Some ? m1' →
2247  ∃m2'. storev chunk m2 addr2 v2 = Some ? m2' ∧ lessdef m1' m2'.
2248#m1 #m2 #chunk #addr1 #v1 #addr2 #v2 #m1'
2249#Hmless #Haless #Hvless #STORE
2250inversion Haless;
2251[ #v #e1 #e2 >e1 in STORE cases v;
2252    [ whd in ⊢ ((??%?)→?); #H' @False_ind destruct;
2253    | 2,3: #v' whd in ⊢ ((??%?)→?); #H' destruct;
2254    | #b' #off @store_lessdef //
2255    ]
2256| #v #e >e in STORE #STORE whd in STORE:(??%?); destruct
2257] qed.
2258
2259lemma alloc_lessdef:
2260  ∀m1,m2,lo,hi,b1,m1',b2,m2'.
2261  lessdef m1 m2 → alloc m1 lo hi = 〈m1', b1〉 → alloc m2 lo hi = 〈m2', b2〉 →
2262  b1 = b2 ∧ lessdef m1' m2'.
2263#m1 #m2 #lo #hi #b1 #m1' #b2 #m2'
2264*;#Hnext #Hinj #ALLOC1 #ALLOC2
2265cut (b1 = b2);
2266[ >(alloc_result … ALLOC1) >(alloc_result … ALLOC2) //
2267]
2268#e <e in ALLOC2 ⊢ % #ALLOC2 % //;
2269%
2270[ >(nextblock_alloc … ALLOC1)
2271    >(nextblock_alloc … ALLOC2)
2272    //
2273| @(alloc_parallel_inj … Hinj ALLOC1 ALLOC2)
2274[ //
2275| 3: whd in ⊢ (??%?); //
2276| 4,5: //;
2277| 6: whd; #chunk #_ cases chunk;//;
2278] qed.
2279
2280lemma free_lessdef:
2281  ∀m1,m2,b. lessdef m1 m2 → lessdef (free m1 b) (free m2 b).
2282#m1 #m2 #b *;#Hnext #Hinj %
2283[ whd in ⊢ (??%%); //
2284| @(free_parallel_inj … Hinj) //;
2285    #b' #delta #H whd in H:(??%?); elim (grumpydestruct2 ?????? H); //
2286] qed.
2287
2288lemma free_left_lessdef:
2289  ∀m1,m2,b.
2290  lessdef m1 m2 → lessdef (free m1 b) m2.
2291#m1 #m2 #b *;#Hnext #Hinj %
2292<Hnext //;
2293@free_left_inj //;
2294qed.
2295
2296lemma free_right_lessdef:
2297  ∀m1,m2,b.
2298  lessdef m1 m2 → low_bound m1 b ≥ high_bound m1 b →
2299  lessdef m1 (free m2 b).
2300#m1 #m2 #b *;#Hnext #Hinj #Hbounds
2301% >Hnext //;
2302@free_right_inj //;
2303#b1 #delta #chunk #ofs #H whd in H:(??%?); destruct;
2304@nmk *; #H1 #H2 #H3 #H4
2305(* arith H2 and H3 contradict Hbounds. *) @daemon
2306qed.
2307
2308lemma valid_block_lessdef:
2309  ∀m1,m2,b. lessdef m1 m2 → valid_block m1 b → valid_block m2 b.
2310#m1 #m2 #b *;#Hnext #Hinj
2311 >(unfold_valid_block …) >(unfold_valid_block m2 b)
2312 //; qed.
2313
2314lemma valid_pointer_lessdef:
2315  ∀m1,m2,b,ofs.
2316  lessdef m1 m2 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true.
2317#m1 #m2 #b #ofs *;#Hnext #Hinj #VALID
2318<(Zplus_z_OZ ofs) @(valid_pointer_inj … Hinj VALID) //;
2319qed.
2320
2321
2322(* ** Memory injections *)
2323
2324(* A memory injection [f] is a function from addresses to either [None]
2325  or [Some] of an address and an offset.  It defines a correspondence
2326  between the blocks of two memory states [m1] and [m2]:
2327- if [f b = None], the block [b] of [m1] has no equivalent in [m2];
2328- if [f b = Some〈b', ofs〉], the block [b] of [m2] corresponds to
2329  a sub-block at offset [ofs] of the block [b'] in [m2].
2330*)
2331
2332(* A memory injection defines a relation between values that is the
2333  identity relation, except for pointer values which are shifted
2334  as prescribed by the memory injection. *)
2335
2336inductive val_inject (mi: meminj): val → val → Prop :=
2337  | val_inject_int:
2338      ∀i. val_inject mi (Vint i) (Vint i)
2339  | val_inject_float:
2340      ∀f. val_inject mi (Vfloat f) (Vfloat f)
2341  | val_inject_ptr:
2342      ∀b1,ofs1,b2,ofs2,x.
2343      mi b1 = Some ? 〈b2, x〉 →
2344      ofs2 = add ofs1 (repr x) →
2345      val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)
2346  | val_inject_undef: ∀v.
2347      val_inject mi Vundef v.
2348(*
2349Hint Resolve val_inject_int val_inject_float val_inject_ptr
2350             val_inject_undef.
2351*)
2352inductive val_list_inject (mi: meminj): list val → list val→ Prop:=
2353  | val_nil_inject :
2354      val_list_inject mi (nil ?) (nil ?)
2355  | val_cons_inject : ∀v,v',vl,vl'.
2356      val_inject mi v v' → val_list_inject mi vl vl'→
2357      val_list_inject mi (v :: vl) (v' :: vl'). 
2358(*
2359Hint Resolve val_nil_inject val_cons_inject.
2360*)
2361(* A memory state [m1] injects into another memory state [m2] via the
2362  memory injection [f] if the following conditions hold:
2363- loads in [m1] must have matching loads in [m2] in the sense
2364  of the [mem_inj] predicate;
2365- unallocated blocks in [m1] must be mapped to [None] by [f];
2366- if [f b = Some〈b', delta〉], [b'] must be valid in [m2];
2367- distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2];
2368- the sizes of [m2]'s blocks are representable with signed machine integers;
2369- the offsets [delta] are representable with signed machine integers.
2370*)
2371
2372record mem_inject (f: meminj) (m1,m2: mem) : Prop ≝
2373  {
2374    mi_inj:
2375      mem_inj val_inject f m1 m2;
2376    mi_freeblocks:
2377      ∀b. ¬(valid_block m1 b) → f b = None ?;
2378    mi_mappedblocks:
2379      ∀b,b',delta. f b = Some ? 〈b', delta〉 → valid_block m2 b';
2380    mi_no_overlap:
2381      meminj_no_overlap f m1;
2382    mi_range_1:
2383      ∀b,b',delta.
2384      f b = Some ? 〈b', delta〉 →
2385      min_signed ≤ delta ∧ delta ≤ max_signed;
2386    mi_range_2:
2387      ∀b,b',delta.
2388      f b = Some ? 〈b', delta〉 →
2389      delta = 0 ∨ (min_signed ≤ low_bound m2 b' ∧ high_bound m2 b' ≤ max_signed)
2390  }.
2391
2392
2393(* The following lemmas establish the absence of machine integer overflow
2394  during address computations. *)
2395
2396lemma address_inject:
2397  ∀f,m1,m2,chunk,b1,ofs1,b2,delta.
2398  mem_inject f m1 m2 →
2399  valid_access m1 chunk b1 (signed ofs1) →
2400  f b1 = Some ? 〈b2, delta〉 →
2401  signed (add ofs1 (repr delta)) = signed ofs1 + delta.
2402#f #m1 #m2 #chunk #b1 #ofs1 #b2 #delta
2403*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2404#Hvalid #Hb1inj
2405elim (mi_range_2 ??? Hb1inj);
2406[ (* delta = 0 *)
2407    #edelta >edelta
2408    >(?:repr O = zero) [ 2: // ]
2409    >(add_zero ?)
2410    >(Zplus_z_OZ …)
2411    //;
2412| (* delta ≠ 0 *)
2413    #Hrange >(add_signed ??)
2414    >(signed_repr delta ?)
2415    [ >(signed_repr ??)
2416      [ //
2417      | cut (valid_access m2 chunk b2 (signed ofs1 + delta));
2418        [ @(valid_access_inj … Hvalid) //;
2419        | *; #_ #Hlo #Hhi #_ (* arith *) napply daemon
2420        ]
2421      ]
2422    | /2/
2423    ]
2424] qed.
2425
2426lemma valid_pointer_inject_no_overflow:
2427  ∀f,m1,m2,b,ofs,b',x.
2428  mem_inject f m1 m2 →
2429  valid_pointer m1 b (signed ofs) = true →
2430  f b = Some ? 〈b', x〉 →
2431  min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed.
2432#f #m1 #m2 #b #ofs #b' #x
2433*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2434#Hvalid #Hb1inj
2435lapply ((proj1 ?? (valid_pointer_valid_access ???)) Hvalid); #Hvalid'
2436cut (valid_access m2 Mint8unsigned b' (signed ofs + x));
2437[ @(valid_access_inj … Hvalid') // ]
2438*; >(?:size_chunk Mint8unsigned = 1) [ 2: // ] #_ #Hlo #Hhi #_
2439>(signed_repr ??) [ 2: /2/; ]
2440lapply (mi_range_2 … Hb1inj); *;
2441[ #ex >ex >(Zplus_z_OZ ?) @signed_range
2442| (* arith *) napply daemon
2443] qed.
2444
2445(* XXX: should use destruct, but reduces large definitions *)
2446lemma vptr_eq: ∀b,b',i,i'. Vptr b i = Vptr b' i' → b = b' ∧ i = i'.
2447#b #b' #i #i' #e destruct; /2/; qed.
2448
2449lemma valid_pointer_inject:
2450  ∀f,m1,m2,b,ofs,b',ofs'.
2451  mem_inject f m1 m2 →
2452  valid_pointer m1 b (signed ofs) = true →
2453  val_inject f (Vptr r b ofs) (Vptr b' ofs') →
2454  valid_pointer m2 b' (signed ofs') = true.
2455#f #m1 #m2 #b #ofs #b' #ofs'
2456#Hinj #Hvalid #Hvinj inversion Hvinj;
2457[ 1,2,4: #x #H destruct; ]
2458#b0 #i #b0' #i' #delta #Hb #Hi' #eptr #eptr'
2459<(proj1 … (vptr_eq ???? eptr)) in Hb <(proj1 … (vptr_eq ???? eptr'))
2460<(proj2 … (vptr_eq ???? eptr)) in Hi' <(proj2 … (vptr_eq ???? eptr'))
2461  #Hofs #Hbinj
2462>Hofs
2463lapply (valid_pointer_inject_no_overflow … Hinj Hvalid Hbinj); #NOOV
2464elim Hinj;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2465>(add_signed ??) >(signed_repr ??) //;
2466>(signed_repr ??) /2/;
2467@(valid_pointer_inj … mi_inj Hvalid) //;
2468qed.
2469
2470lemma different_pointers_inject:
2471  ∀f,m,m',b1,ofs1,b2,ofs2,b1',delta1,b2',delta2.
2472  mem_inject f m m' →
2473  b1 ≠ b2 →
2474  valid_pointer m b1 (signed ofs1) = true →
2475  valid_pointer m b2 (signed ofs2) = true →
2476  f b1 = Some ? 〈b1', delta1〉 →
2477  f b2 = Some ? 〈b2', delta2〉 →
2478  b1' ≠ b2' ∨
2479  signed (add ofs1 (repr delta1)) ≠
2480  signed (add ofs2 (repr delta2)).
2481#f #m #m' #b1 #ofs1 #b2 #ofs2 #b1' #delta1 #b2' #delta2
2482#Hinj #neb #Hval1 #Hval2 #Hf1 #Hf2
2483lapply ((proj1 ?? (valid_pointer_valid_access …)) Hval1); #Hval1'
2484lapply ((proj1 ?? (valid_pointer_valid_access …)) Hval2); #Hval2'
2485>(address_inject … Hinj Hval1' Hf1)
2486>(address_inject … Hinj Hval2' Hf2)
2487elim Hval1'; #Hbval #Hlo #Hhi #Hal whd in Hhi:(?(??%)?);
2488elim Hval2'; #Hbval2 #Hlo2 #Hhi2 #Hal2 whd in Hhi2:(?(??%)?);
2489lapply (mi_no_overlap ??? Hinj … Hf1 Hf2 …); //;
2490*; [
2491*; [
2492*; [ /2/;
2493   | (* arith contradiction *) napply daemon ]
2494   | (* arith contradiction *) napply daemon ]
2495   | *; [ #H %{2} (* arith *) napply daemon
2496          | #H %{2} (* arith *) napply daemon  ] ]
2497qed.
2498
2499(* Relation between injections and loads. *)
2500
2501lemma load_inject:
2502  ∀f,m1,m2,chunk,b1,ofs,b2,delta,v1.
2503  mem_inject f m1 m2 →
2504  load chunk m1 b1 ofs = Some ? v1 →
2505  f b1 = Some ? 〈b2, delta〉 →
2506  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inject f v1 v2.
2507#f #m1 #m2 #chunk #b1 #ofs #b2 #delta #v1
2508*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2509#LOAD #Hbinj
2510@mi_inj //;
2511qed.
2512
2513lemma loadv_inject:
2514  ∀f,m1,m2,chunk,a1,a2,v1.
2515  mem_inject f m1 m2 →
2516  loadv chunk m1 a1 = Some ? v1 →
2517  val_inject f a1 a2 →
2518  ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_inject f v1 v2.
2519#f #m1 #m2 #chunk #a1 #a2 #v1
2520#Hinj #LOADV #Hvinj inversion Hvinj;
2521[ 1,2,4: #x #ex #ex' @False_ind destruct; ]
2522#b #ofs #b' #ofs' #delta #Hbinj #Hofs #ea1 #ea2
2523>ea1 in LOADV #LOADV
2524lapply (load_inject … Hinj LOADV … Hbinj); *; #v2 *; #LOAD #INJ
2525%{ v2} % //; >Hofs
2526<(?:signed (add ofs (repr delta)) = signed ofs + delta) in LOAD
2527[ #H @H (* XXX: used to work with /2/ *)
2528| @(address_inject … chunk … Hinj ? Hbinj) @(load_valid_access …)
2529    [ 2: @LOADV ]
2530] qed.
2531
2532(* Relation between injections and stores. *)
2533
2534inductive val_content_inject (f: meminj): memory_chunk → val → val → Prop ≝
2535  | val_content_inject_base:
2536      ∀chunk,v1,v2.
2537      val_inject f v1 v2 →
2538      val_content_inject f chunk v1 v2
2539  | val_content_inject_8:
2540      ∀chunk,n1,n2.
2541      chunk = Mint8unsigned ∨ chunk = Mint8signed →
2542      zero_ext 8 n1 = zero_ext 8 n2 →
2543      val_content_inject f chunk (Vint n1) (Vint n2)
2544  | val_content_inject_16:
2545      ∀chunk,n1,n2.
2546      chunk = Mint16unsigned ∨ chunk = Mint16signed →
2547      zero_ext 16 n1 = zero_ext 16 n2 →
2548      val_content_inject f chunk (Vint n1) (Vint n2)
2549  | val_content_inject_32:
2550      ∀f1,f2.
2551      singleoffloat f1 = singleoffloat f2 →
2552      val_content_inject f Mfloat32 (Vfloat f1) (Vfloat f2).
2553
2554(*Hint Resolve val_content_inject_base.*)
2555
2556lemma load_result_inject:
2557  ∀f,chunk,v1,v2,chunk'.
2558  val_content_inject f chunk v1 v2 →
2559  size_chunk chunk = size_chunk chunk' →
2560  val_inject f (load_result chunk' v1) (load_result chunk' v2).
2561#f #chunk #v1 #v2 #chunk'
2562#Hvci inversion Hvci;
2563[ #chunk'' #v1' #v2' #Hvinj #_ #_ #_ #Hsize inversion Hvinj;
2564  [ cases chunk'; #i #_ #_ [ 1,2,3,4,5: @ | 6,7: @4 ]
2565  | cases chunk'; #f #_ #_ [ 1,2,3,4,5: @4 | 6,7: @2 ]
2566  | cases chunk'; #b1 #ofs1 #b2 #ofs2 #delta #Hmap #Hofs #_ #_ [ 5: %{3} // | *: @4 ]
2567  | cases chunk'; #v #_ #_ %{4}
2568  ]
2569(* FIXME: the next two cases are very similar *)
2570| #chunk'' #i #i' *;#echunk >echunk #Hz #_ #_ #_
2571    elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct;
2572    [ 2,4: whd in ⊢ (??%%); >Hz @
2573    | 1,3: whd in ⊢ (??%%); >(sign_ext_equal_if_zero_equal … Hz)
2574        % [ 1,3: @I | 2,4: @leb_true_to_le % ]
2575    ]
2576| #chunk'' #i #i' *;#echunk >echunk #Hz #_ #_ #_
2577    elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct;
2578    [ 2,4: whd in ⊢ (??%%); >Hz @
2579    | 1,3: whd in ⊢ (??%%); >(sign_ext_equal_if_zero_equal … Hz)
2580        % [ 1,3: @I | 2,4: @leb_true_to_le % ]
2581    ]
2582
2583| #f #f' #float #echunk >echunk #_ #_
2584    elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct;
2585    [ %{4} | >float @2 ]
2586] qed.
2587
2588lemma store_mapped_inject_1 :
2589  ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2.
2590  mem_inject f m1 m2 →
2591  store chunk m1 b1 ofs v1 = Some ? n1 →
2592  f b1 = Some ? 〈b2, delta〉 →
2593  val_content_inject f chunk v1 v2 →
2594  ∃n2.
2595    store chunk m2 b2 (ofs + delta) v2 = Some ? n2
2596    ∧ mem_inject f n1 n2.
2597#f #chunk #m1 #b1 #ofs #v1 #n1 #m2 #b2 #delta #v2
2598*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2599#STORE1 #INJb1 #Hvcinj
2600lapply (store_mapped_inj … mi_inj mi_no_overlap INJb1 STORE1 ?); //;
2601[ #chunk' #Hchunksize @(load_result_inject … chunk …) //;
2602| ##skip ]
2603*;#n2 *;#STORE #MINJ
2604%{ n2} % //; %
2605[ (* inj *) //
2606| (* freeblocks *) #b #notvalid @mi_freeblocks
2607    @(not_to_not ??? notvalid) @(store_valid_block_1 … STORE1)
2608| (* mappedblocks *) #b #b' #delta' #INJb' @(store_valid_block_1 … STORE)
2609    /2/;
2610| (* no_overlap *) whd; #b1' #b1'' #delta1' #b2' #b2'' #delta2' #neqb'
2611    #fb1' #fb2'
2612    >(low_bound_store … STORE1 ?)  >(low_bound_store … STORE1 ?)
2613    >(high_bound_store … STORE1 ?)  >(high_bound_store … STORE1 ?)
2614    @mi_no_overlap //;
2615| (* range *) /2/;
2616| (* range 2 *) #b #b' #delta' #INJb
2617    >(low_bound_store … STORE ?)
2618    >(high_bound_store … STORE ?)
2619    @mi_range_2 //;
2620] qed.
2621
2622lemma store_mapped_inject:
2623  ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2.
2624  mem_inject f m1 m2 →
2625  store chunk m1 b1 ofs v1 = Some ? n1 →
2626  f b1 = Some ? 〈b2, delta〉 →
2627  val_inject f v1 v2 →
2628  ∃n2.
2629    store chunk m2 b2 (ofs + delta) v2 = Some ? n2
2630    ∧ mem_inject f n1 n2.
2631#f #chunk #m1 #b1 #ofs #v1 #n1 #m2 #b2 #delta #v2
2632#MINJ #STORE #INJb1 #Hvalinj @(store_mapped_inject_1 … STORE) //;
2633@val_content_inject_base //;
2634qed.
2635
2636lemma store_unmapped_inject:
2637  ∀f,chunk,m1,b1,ofs,v1,n1,m2.
2638  mem_inject f m1 m2 →
2639  store chunk m1 b1 ofs v1 = Some ? n1 →
2640  f b1 = None ? →
2641  mem_inject f n1 m2.
2642#f #chunk #m1 #b1 #ofs #v1 #n1 #m2
2643*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2644#STORE #INJb1 %
2645[ (* inj *) @(store_unmapped_inj … STORE) //
2646| (* freeblocks *) #b #notvalid @mi_freeblocks
2647    @(not_to_not ??? notvalid) @(store_valid_block_1 … STORE)
2648| (* mappedblocks *) #b #b' #delta #INJb @mi_mappedblock //;
2649| (* no_overlap *) whd; #b1' #b1'' #delta1' #b2' #b2'' #delta2' #neqb'
2650    #fb1' #fb2'
2651    >(low_bound_store … STORE ?)  >(low_bound_store … STORE ?)
2652    >(high_bound_store … STORE ?)  >(high_bound_store … STORE ?)
2653    @mi_no_overlap //;
2654| (* range *) /2/
2655| /2/
2656] qed.
2657
2658lemma storev_mapped_inject_1:
2659  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
2660  mem_inject f m1 m2 →
2661  storev chunk m1 a1 v1 = Some ? n1 →
2662  val_inject f a1 a2 →
2663  val_content_inject f chunk v1 v2 →
2664  ∃n2.
2665    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2.
2666#f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2
2667#MINJ #STORE #Hvinj #Hvcinj
2668inversion Hvinj;
2669[ 1,2,4:#x #ex1 #ex2 >ex1 in STORE whd in ⊢ ((??%?)→?); #H
2670    @False_ind destruct; ]
2671#b #ofs #b' #ofs' #delta #INJb #Hofs #ea1 #ea2
2672>Hofs >ea1 in STORE #STORE
2673lapply (store_mapped_inject_1 … MINJ STORE … INJb Hvcinj);
2674<(?:signed (add ofs (repr delta)) = signed ofs + delta) //;
2675@(address_inject … chunk … MINJ ? INJb)
2676@(store_valid_access_3 … STORE)
2677qed.
2678
2679lemma storev_mapped_inject:
2680  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
2681  mem_inject f m1 m2 →
2682  storev chunk m1 a1 v1 = Some ? n1 →
2683  val_inject f a1 a2 →
2684  val_inject f v1 v2 →
2685  ∃n2.
2686    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2.
2687#f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2 #MINJ #STOREV #Hvinj #Hvinj'
2688@(storev_mapped_inject_1 … STOREV) /2/;
2689qed.
2690
2691(* Relation between injections and [free] *)
2692
2693lemma meminj_no_overlap_free:
2694  ∀mi,m,b.
2695  meminj_no_overlap mi m →
2696  meminj_no_overlap mi (free m b).
2697#mi #m #b #H whd;#b1 #b1' #delta1 #b2 #b2' #delta2 #Hne #mi1 #mi2
2698cut (low_bound (free m b) b ≥ high_bound (free m b) b);
2699[ >(low_bound_free_same …) >(high_bound_free_same …) // ]
2700#Hbounds
2701cases (decidable_eq_Z b1 b);#e1 [ >e1 in Hne mi1 ⊢ % #Hne #mi1 ]
2702cases (decidable_eq_Z b2 b);#e2 [ 1,3: >e2 in Hne mi2 ⊢ % #Hne #mi2 ]
2703[ @False_ind elim Hne; /2/
2704| % %{2} //;
2705| % % %{2} //
2706| >(low_bound_free …) //; >(low_bound_free …) //;
2707    >(high_bound_free …) //; >(high_bound_free …) //;
2708    /2/;
2709] qed.
2710
2711lemma meminj_no_overlap_free_list:
2712  ∀mi,m,bl.
2713  meminj_no_overlap mi m →
2714  meminj_no_overlap mi (free_list m bl).
2715#mi #m #bl elim bl;
2716[ #H whd in ⊢ (??%); //
2717| #h #t #IH #H @meminj_no_overlap_free @IH //
2718] qed.
2719
2720lemma free_inject:
2721  ∀f,m1,m2,l,b.
2722  (∀b1,delta. f b1 = Some ? 〈b, delta〉 → in_list ? b1 l) →
2723  mem_inject f m1 m2 →
2724  mem_inject f (free_list m1 l) (free m2 b).
2725#f #m1 #m2 #l #b #mappedin
2726*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2727%
2728[ (* inj *)
2729    @free_right_inj [ @free_list_left_inj //; ]
2730    #b1 #delta #chunk #ofs #INJb1 @nmk #Hvalid
2731    elim (valid_access_free_list_inv … Hvalid); #b1ni #Haccess
2732    @(absurd ? (mappedin ?? INJb1) b1ni)
2733| (* freeblocks *)
2734    #b' #notvalid @mi_freeblocks @(not_to_not ??? notvalid)
2735    #H @valid_block_free_list_1 //
2736| (* mappedblocks *)
2737    #b1 #b1' #delta #INJb1 @valid_block_free_1 /2/
2738| (* overlap *)
2739    @meminj_no_overlap_free_list //
2740| (* range *)
2741    /2/
2742| #b1 #b2 #delta #INJb1 cases (decidable_eq_Z b2 b); #eb
2743    [ >eb
2744        >(low_bound_free_same ??) >(high_bound_free_same ??)
2745        %{2} (* arith *) napply daemon
2746    | >(low_bound_free …) //; >(high_bound_free …) /2/;
2747    ]
2748] qed.
2749
2750(* Monotonicity properties of memory injections. *)
2751
2752definition inject_incr : meminj → meminj → Prop ≝ λf1,f2.
2753  ∀b. f1 b = f2 b ∨ f1 b = None ?.
2754
2755lemma inject_incr_refl :
2756   ∀f. inject_incr f f .
2757#f whd;#b % //; qed.
2758
2759lemma inject_incr_trans :
2760  ∀f1,f2,f3.
2761  inject_incr f1 f2 → inject_incr f2 f3 → inject_incr f1 f3 .
2762#f1 #f2 #f3 whd in ⊢ (%→%→%);#H1 #H2 #b
2763elim (H1 b); elim (H2 b); /2/; qed.
2764
2765lemma val_inject_incr:
2766  ∀f1,f2,v,v'.
2767  inject_incr f1 f2 →
2768  val_inject f1 v v' →
2769  val_inject f2 v v'.
2770#f1 #f2 #v #v' #Hincr #Hvinj
2771inversion Hvinj;
2772[ 1,2,4: #x #_ #_ //;
2773|#b #ofs #b' #ofs' #delta #INJb #Hofs #_ #_
2774elim (Hincr b); #H
2775[ @(val_inject_ptr ??????? Hofs) /2/;
2776| @False_ind >INJb in H #H destruct;
2777] qed.
2778
2779lemma val_list_inject_incr:
2780  ∀f1,f2,vl,vl'.
2781  inject_incr f1 f2 → val_list_inject f1 vl vl' →
2782  val_list_inject f2 vl vl'.
2783#f1 #f2 #vl elim vl;
2784[ #vl' #Hincr #H inversion H; //; #v #v' #l #l0 #_ #_ #_ #H destruct;
2785| #h #t #IH #vl' #Hincr #H1 inversion H1;
2786  [ #H destruct
2787  | #h' #h'' #t' #t'' #Hinj1 #Hintt #_ #e1 #e2 destruct;
2788      %{2} /2/; @IH //; @Hincr
2789  ]
2790] qed.
2791
2792(*
2793Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.
2794*)
2795
2796(* Properties of injections and allocations. *)
2797
2798definition extend_inject ≝
2799       λb: block. λx: option (block × Z). λf: meminj.
2800  λb': block. if eqZb b' b then x else f b'.
2801
2802lemma extend_inject_incr:
2803  ∀f,b,x.
2804  f b = None ? →
2805  inject_incr f (extend_inject b x f).
2806#f #b #x #INJb whd;#b' whd in ⊢ (?(???%)?);
2807@(eqZb_elim b' b) #eb /2/;
2808qed.
2809
2810lemma alloc_right_inject:
2811  ∀f,m1,m2,lo,hi,m2',b.
2812  mem_inject f m1 m2 →
2813  alloc m2 lo hi = 〈m2', b〉 →
2814  mem_inject f m1 m2'.
2815#f #m1 #m2 #lo #hi #m2' #b
2816*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2817#ALLOC %
2818[ @(alloc_right_inj … ALLOC) //;
2819| /2/;
2820| #b1 #b2 #delta #INJb1 @(valid_block_alloc … ALLOC) /2/;
2821| //;
2822| /2/;
2823|#b1 #b2 #delta #INJb1 >(?:low_bound m2' b2 = low_bound m2 b2)
2824   [ >(?:high_bound m2' b2 = high_bound m2 b2) /2/;
2825       @high_bound_alloc_other /2/;
2826   | @low_bound_alloc_other /2/
2827   ]
2828] qed.
2829
2830lemma alloc_unmapped_inject:
2831  ∀f,m1,m2,lo,hi,m1',b.
2832  mem_inject f m1 m2 →
2833  alloc m1 lo hi = 〈m1', b〉 →
2834  mem_inject (extend_inject b (None ?) f) m1' m2 ∧
2835  inject_incr f (extend_inject b (None ?) f).
2836#f #m1 #m2 #lo #hi #m1' #b
2837*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2838#ALLOC
2839cut (inject_incr f (extend_inject b (None ?) f));
2840[ @extend_inject_incr @mi_freeblocks /2/; ]
2841#Hinject_incr % //; %
2842[ (* inj *)
2843    @(alloc_left_unmapped_inj … ALLOC)
2844    [ 2: whd in ⊢ (??%?); >(eqZb_z_z …) /2/; ]
2845    whd; #chunk #b1 #ofs #v1 #b2 #delta
2846    whd in ⊢ ((??%?)→?→?); @eqZb_elim #e whd in ⊢ ((??%?)→?→?);
2847    #Hextend #LOAD
2848    [ destruct;
2849    | lapply (mi_inj … Hextend LOAD); *; #v2 *; #LOAD2 #VINJ
2850    %{ v2} % //;
2851    @val_inject_incr //;
2852    ]
2853| (* freeblocks *)
2854    #b' #Hinvalid whd in ⊢ (??%?); @(eqZb_elim b' b) //;
2855    #neb @mi_freeblocks @(not_to_not ??? Hinvalid)
2856    @valid_block_alloc //;
2857| (* mappedblocks *)
2858    #b1 #b2 #delta whd in ⊢ (??%?→?); @(eqZb_elim b1 b) #eb
2859    [ #H destruct;
2860    | #H @(mi_mappedblock … H)
2861    ]
2862| (* overlap *)
2863    whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢ (??%?→??%?→?);
2864    >(low_bound_alloc … ALLOC ?) >(low_bound_alloc … ALLOC ?)
2865    >(high_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?)
2866    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
2867    [ destruct
2868    | lapply (eqZb_to_Prop b2 b); elim (eqZb b2 b); #e2 #INJb2
2869      [ destruct
2870      | @mi_no_overlap /2/;
2871      ]
2872    ]
2873| (* range *)
2874    #b1 #b2 #delta whd in ⊢ (??%?→?);
2875    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
2876    [ destruct
2877    | @(mi_range_1 … INJb1)
2878    ]
2879| #b1 #b2 #delta whd in ⊢ (??%?→?);
2880    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
2881    [  destruct
2882    | @(mi_range_2 … INJb1)
2883    ]
2884] qed.
2885
2886lemma alloc_mapped_inject:
2887  ∀f,m1,m2,lo,hi,m1',b,b',ofs.
2888  mem_inject f m1 m2 →
2889  alloc m1 lo hi = 〈m1', b〉 →
2890  valid_block m2 b' →
2891  min_signed ≤ ofs ∧ ofs ≤ max_signed →
2892  min_signed ≤ low_bound m2 b' →
2893  high_bound m2 b' ≤ max_signed →
2894  low_bound m2 b' ≤ lo + ofs →
2895  hi + ofs ≤ high_bound m2 b' →
2896  inj_offset_aligned ofs (hi-lo) →
2897  (∀b0,ofs0.
2898   f b0 = Some ? 〈b', ofs0〉 →
2899   high_bound m1 b0 + ofs0 ≤ lo + ofs ∨
2900   hi + ofs ≤ low_bound m1 b0 + ofs0) →
2901  mem_inject (extend_inject b (Some ? 〈b', ofs〉) f) m1' m2 ∧
2902  inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f).
2903#f #m1 #m2 #lo #hi #m1' #b #b' #ofs
2904*;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2905#ALLOC #validb' #rangeofs #rangelo #rangehi #boundlo #boundhi #injaligned #boundmapped
2906cut (inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f));
2907[ @extend_inject_incr @mi_freeblocks /2/; ]
2908#Hincr % //; %
2909[ (* inj *)
2910    @(alloc_left_mapped_inj … ALLOC … validb' boundlo boundhi) /2/;
2911    [ 2:whd in ⊢ (??%?); >(eqZb_z_z …) /2/; ]
2912    whd; #chunk #b1 #ofs' #v1 #b2 #delta #Hextend #LOAD
2913    whd in Hextend:(??%?); >(eqZb_false b1 b ?) in Hextend
2914    [ #Hextend lapply (mi_inj … Hextend LOAD);
2915        *; #v2 *; #LOAD2 #VINJ
2916    %{ v2} % //;
2917    @val_inject_incr //;
2918    | @(valid_not_valid_diff m1) /2/;
2919        @(valid_access_valid_block … chunk … ofs') /2/;
2920    ]
2921| (* freeblocks *)
2922    #b' #Hinvalid whd in ⊢ (??%?); >(eqZb_false b' b ?)
2923    [ @mi_freeblocks @(not_to_not ??? Hinvalid)
2924    @valid_block_alloc //;
2925    | @sym_neq @(valid_not_valid_diff m1') //;
2926        @(valid_new_block … ALLOC)
2927    ]
2928| (* mappedblocks *)
2929    #b1 #b2 #delta whd in ⊢ (??%?→?); @(eqZb_elim b1 b) #eb #einj
2930    [ destruct; //;
2931    | @(mi_mappedblock … einj)
2932    ]
2933| (* overlap *)
2934    whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢ (??%?→??%?→?);
2935    >(low_bound_alloc … ALLOC ?) >(low_bound_alloc … ALLOC ?)
2936    >(high_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?)
2937    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
2938    [ elim (grumpydestruct2 ?????? INJb1); #eb1' #eofs1 ]
2939    lapply (eqZb_to_Prop b2 b); elim (eqZb b2 b); #e2 #INJb2
2940    [ elim (grumpydestruct2 ?????? INJb2); #eb2' #eofs2 ]
2941    [ @False_ind >e in neb1 >e2 /2/;
2942    | elim (decidable_eq_Z b1' b2'); #e'
2943        [ <e' in INJb2 ⊢ % <eb1' <eofs1 #INJb2 lapply (boundmapped … INJb2);
2944            *; #H %{2} [ %{2 | @1 ] napply H}
2945        | %{1} %{1} %{1} napply e'
2946        ]
2947    | elim (decidable_eq_Z b1' b2'); #e'
2948        [ <e' in INJb2 ⊢ % #INJb2 elim (grumpydestruct2 ?????? INJb2); #eb' #eofs <eb' in INJb1 <eofs #INJb1 lapply (boundmapped … INJb1);
2949            *; #H %{2} [ %{1} /2/ | %{2} @H ]
2950        | %{1} %{1} %{1} napply e'
2951        ]
2952    | @mi_no_overlap /2/;
2953    ]
2954| (* range *)
2955    #b1 #b2 #delta whd in ⊢ (??%?→?);
2956    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
2957    [ destruct; /2/;
2958    | @(mi_range_1 … INJb1)
2959    ]
2960| #b1 #b2 #delta whd in ⊢ (??%?→?);
2961    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
2962    [ destruct; %{2} % /2/;
2963    | @(mi_range_2 … INJb1)
2964    ]
2965] qed.
2966
2967lemma alloc_parallel_inject:
2968  ∀f,m1,m2,lo,hi,m1',m2',b1,b2.
2969  mem_inject f m1 m2 →
2970  alloc m1 lo hi = 〈m1', b1〉 →
2971  alloc m2 lo hi = 〈m2', b2〉 →
2972  min_signed ≤ lo → hi ≤ max_signed →
2973  mem_inject (extend_inject b1 (Some ? 〈b2, OZ〉) f) m1' m2' ∧
2974  inject_incr f (extend_inject b1 (Some ? 〈b2, OZ〉) f).
2975#f #m1 #m2 #lo #hi #m1' #m2' #b1 #b2
2976#Hminj #ALLOC1 #ALLOC2 #Hlo #Hhi
2977@(alloc_mapped_inject … ALLOC1) /2/;
2978[ @(alloc_right_inject … Hminj ALLOC2)
2979| >(low_bound_alloc_same … ALLOC2) //
2980| >(high_bound_alloc_same … ALLOC2) //
2981| >(low_bound_alloc_same … ALLOC2) //
2982| >(high_bound_alloc_same … ALLOC2) //
2983| whd; (* arith *) napply daemon
2984| #b #ofs #INJb0 @False_ind
2985    elim Hminj;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
2986    lapply (mi_mappedblock … INJb0);
2987    #H @(absurd ? H ?) /2/;
2988] qed.
2989
2990definition meminj_init ≝ λm: mem.
2991  λb: block. if Zltb b (nextblock m) then Some ? 〈b, OZ〉 else None ?.
2992
2993definition mem_inject_neutral ≝ λm: mem.
2994  ∀f,chunk,b,ofs,v.
2995  load chunk m b ofs = Some ? v → val_inject f v v.
2996
2997lemma init_inject:
2998  ∀m.
2999  mem_inject_neutral m →
3000  mem_inject (meminj_init m) m m.
3001#m #neutral %
3002[ (* inj *)
3003    whd; #chunk #b1 #ofs #v1 #b2 #delta whd in ⊢ (??%?→?→?);
3004    @Zltb_elim_Type0 #ltb1 [
3005    #H elim (grumpydestruct2 ?????? H); #eb1 #edelta
3006    <eb1 <edelta #LOAD %{v1} % //;
3007    @neutral //;
3008    | #H whd in H:(??%?); destruct;
3009    ]
3010| (* free blocks *)
3011    #b >(unfold_valid_block …) whd in ⊢ (?→??%?); #notvalid
3012    @Zltb_elim_Type0 #ltb1
3013    [ @False_ind napply (absurd ? ltb1 notvalid)
3014    | //
3015    ]
3016| (* mapped blocks *)
3017    #b #b' #delta whd in ⊢ (??%?→?); >(unfold_valid_block …)
3018    @Zltb_elim_Type0 #ltb
3019    #H whd in H:(??%?); destruct; //
3020| (* overlap *)
3021    whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢(??%?→??%?→?);
3022    @Zltb_elim_Type0 #ltb1
3023    [ #H whd in H:(??%?); destruct;
3024        @Zltb_elim_Type0 #ltb2
3025        #H2 whd in H2:(??%?); destruct; % % % /2/;
3026    | #H whd in H:(??%?); destruct;
3027    ]
3028| (* range *)
3029    #b #b' #delta whd in ⊢ (??%?→?);
3030    @Zltb_elim_Type0 #ltb
3031    [ #H elim (grumpydestruct2 ?????? H); #eb #edelta <edelta
3032        (* FIXME: should be in integers.ma *) napply daemon
3033    | #H whd in H:(??%?); destruct;
3034    ]
3035| (* range *)
3036    #b #b' #delta whd in ⊢ (??%?→?);
3037    @Zltb_elim_Type0 #ltb
3038    [ #H elim (grumpydestruct2 ?????? H); #eb #edelta <edelta
3039        (* FIXME: should be in integers.ma *) napply daemon
3040    | #H whd in H:(??%?); destruct;
3041    ]
3042] qed.
3043
3044lemma getN_setN_inject:
3045  ∀f,m,v,n1,p1,n2,p2.
3046  val_inject f (getN n2 p2 m) (getN n2 p2 m) →
3047  val_inject f v v →
3048  val_inject f (getN n2 p2 (setN n1 p1 v m))
3049               (getN n2 p2 (setN n1 p1 v m)).
3050#f #m #v #n1 #p1 #n2 #p2 #injget #injv
3051cases (getN_setN_characterization m v n1 p1 n2 p2);[ * ] #A
3052>A //;
3053qed.
3054             
3055lemma getN_contents_init_data_inject:
3056  ∀f,n,ofs,id,pos.
3057  val_inject f (getN n ofs (contents_init_data pos id))
3058               (getN n ofs (contents_init_data pos id)).
3059#f #n #ofs #id elim id;
3060[ #pos >(getN_init …) //
3061| #h #t #IH #pos cases h;
3062[ 1,2,3,4,5: #x @getN_setN_inject //
3063| 6,8: #x @IH | #x #y napply IH ] (* XXX // doesn't work? *)
3064qed.
3065
3066lemma alloc_init_data_neutral:
3067  ∀m,id,m',b.
3068  mem_inject_neutral m →
3069  alloc_init_data m id = 〈m', b〉 →
3070  mem_inject_neutral m'.
3071#m #id #m' #b #Hneutral #INIT whd in INIT:(??%?); (* XXX: destruct makes a bit of a mess *)
3072@(pairdisc_elim … INIT)
3073whd in ⊢ (??%% → ?);#B <B in ⊢ (??%% → ?)
3074whd in ⊢ (??%% → ?);#A
3075whd; #f #chunk #b' #ofs #v #LOAD
3076lapply (load_inv … LOAD); *; #C #D
3077<B in D >A
3078>(unfold_update block_contents …) @eqZb_elim
3079[ #eb' #D whd in D:(???(??(???%))); >D
3080    @(load_result_inject … chunk) //; %
3081    @getN_contents_init_data_inject
3082| #neb' #D @(Hneutral ? chunk b' ofs ??) whd in ⊢ (??%?);
3083    >(in_bounds_true m chunk b' ofs (option ?) …)
3084    [ <D //
3085    | elim C; #Cval #Clo #Chi #Cal %
3086    [ >(unfold_valid_block …)
3087        >(unfold_valid_block …) in Cval <B
3088        (* arith using neb' *) napply daemon
3089    | >(?:low_bound m b' = low_bound m' b') //;
3090        whd in ⊢ (??%%); <B >A
3091        >(update_o block_contents …) //; @sym_neq //;
3092    | >(?:high_bound m b' = high_bound m' b') //;
3093        whd in ⊢ (??%%); <B >A
3094        >(update_o block_contents …) //; @sym_neq //;
3095    | //;
3096    ]
3097] qed.
3098
3099
3100(* ** Memory shifting *)
3101
3102(* A special case of memory injection where blocks are not coalesced:
3103  each source block injects in a distinct target block. *)
3104
3105definition memshift ≝ block → option Z.
3106
3107definition meminj_of_shift : memshift → meminj ≝ λmi: memshift.
3108  λb. match mi b with [ None ⇒ None ? | Some x ⇒ Some ? 〈b, x〉 ].
3109
3110definition val_shift ≝ λmi: memshift. λv1,v2: val.
3111  val_inject (meminj_of_shift mi) v1 v2.
3112
3113record mem_shift (f: memshift) (m1,m2: mem) : Prop :=
3114  {
3115    ms_inj:
3116      mem_inj val_inject (meminj_of_shift f) m1 m2;
3117    ms_samedomain:
3118      nextblock m1 = nextblock m2;
3119    ms_domain:
3120      ∀b. match f b with [ Some _ ⇒ b < nextblock m1 | None ⇒ b ≥ nextblock m1 ];
3121    ms_range_1:
3122      ∀b,delta.
3123      f b = Some ? delta →
3124      min_signed ≤ delta ∧ delta ≤ max_signed;
3125    ms_range_2:
3126      ∀b,delta.
3127      f b = Some ? delta →
3128      min_signed ≤ low_bound m2 b ∧ high_bound m2 b ≤ max_signed
3129  }.
3130
3131(* * The following lemmas establish the absence of machine integer overflow
3132  during address computations. *)
3133
3134lemma address_shift:
3135  ∀f,m1,m2,chunk,b,ofs1,delta.
3136  mem_shift f m1 m2 →
3137  valid_access m1 chunk b (signed ofs1) →
3138  f b = Some ? delta →
3139  signed (add ofs1 (repr delta)) = signed ofs1 + delta.
3140#f #m1 #m2 #chunk #b #ofs1 #delta
3141*;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 #Hvalid_access #INJb
3142elim (ms_range_2 … INJb); #Hlo #Hhi
3143>(add_signed …)
3144>(signed_repr …) >(signed_repr …) /2/;
3145cut (valid_access m2 chunk b (signed ofs1 + delta));
3146[ @(valid_access_inj ? (meminj_of_shift f) … ms_inj Hvalid_access)
3147    whd in ⊢ (??%?); >INJb // ]
3148*; (* arith *) @daemon
3149qed.
3150
3151lemma valid_pointer_shift_no_overflow:
3152  ∀f,m1,m2,b,ofs,x.
3153  mem_shift f m1 m2 →
3154  valid_pointer m1 b (signed ofs) = true →
3155  f b = Some ? x →
3156  min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed.
3157#f #m1 #m2 #b #ofs #x
3158*;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2
3159#VALID #INJb
3160lapply (proj1 ?? (valid_pointer_valid_access …) VALID); #Hvalid_access
3161cut (valid_access m2 Mint8unsigned b (signed ofs + x));
3162[ @(valid_access_inj … ms_inj Hvalid_access)
3163    whd in ⊢ (??%?); >INJb // ]
3164*;#Hvalid_block #Hlo #Hhi #Hal whd in Hhi:(?(??%)?);
3165>(signed_repr …) /2/;
3166lapply (ms_range_2 … INJb);*;#A #B
3167(* arith *) @daemon
3168qed.
3169
3170(* FIXME to get around destruct problems *)
3171lemma vptr_eq_1 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → b = b'.
3172#b #b' #ofs #ofs' #H destruct;//;
3173qed.
3174lemma vptr_eq_2 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → ofs = ofs'.
3175#b #b' #ofs #ofs' #H destruct;//;
3176qed.
3177
3178lemma valid_pointer_shift:
3179  ∀f,m1,m2,b,ofs,b',ofs'.
3180  mem_shift f m1 m2 →
3181  valid_pointer m1 b (signed ofs) = true →
3182  val_shift f (Vptr b ofs) (Vptr b' ofs') →
3183  valid_pointer m2 b' (signed ofs') = true.
3184#f #m1 #m2 #b #ofs #b' #ofs' #Hmem_shift #VALID #Hval_shift
3185whd in Hval_shift; inversion Hval_shift;
3186[ 1,2,4: #a #H destruct; ]
3187#b1 #ofs1 #b2 #ofs2 #delta #INJb1 #Hofs #eb1 #eb2
3188<(vptr_eq_1 … eb1) in INJb1 <(vptr_eq_1 … eb2) #INJb'
3189<(vptr_eq_2 … eb1) in Hofs <(vptr_eq_2 … eb2) #Hofs >Hofs
3190cut (f b = Some ? delta);
3191[ whd in INJb':(??%?); cases (f b) in INJb' ⊢ %;
3192  [ #H @(False_ind … (grumpydestruct … H)) | #delta' #H elim (grumpydestruct2 ?????? H); // ]
3193] #INJb
3194lapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV
3195elim Hmem_shift;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2
3196>(add_signed …) >(signed_repr …) //;
3197>(signed_repr …) /2/;
3198@(valid_pointer_inj … VALID) /2/;
3199qed.
3200
3201(* Relation between shifts and loads. *)
3202
3203lemma load_shift:
3204  ∀f,m1,m2,chunk,b,ofs,delta,v1.
3205  mem_shift f m1 m2 →
3206  load chunk m1 b ofs = Some ? v1 →
3207  f b = Some ? delta →
3208  ∃v2. load chunk m2 b (ofs + delta) = Some ? v2 ∧ val_shift f v1 v2.
3209#f #m1 #m2 #chunk #b #ofs #delta #v1
3210*;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2
3211#LOAD #INJb
3212whd in ⊢ (??(λ_.??%)); @(ms_inj … LOAD)
3213whd in ⊢ (??%?); >INJb //;
3214qed.
3215
3216lemma loadv_shift:
3217  ∀f,m1,m2,chunk,a1,a2,v1.
3218  mem_shift f m1 m2 →
3219  loadv chunk m1 a1 = Some ? v1 →
3220  val_shift f a1 a2 →
3221  ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_shift f v1 v2.
3222#f #m1 #m2 #chunk #a1 #a2 #v1 #Hmem_shift #LOADV #Hval_shift
3223inversion Hval_shift;
3224[ 1,2,4: #x #H >H in LOADV #H' whd in H':(??%?);@False_ind destruct; ]
3225#b1 #ofs1 #b2 #ofs2 #delta #INJb1 #Hofs #ea1 #ea2 >ea1 in LOADV #LOADV
3226lapply INJb1; whd in ⊢ (??%? → ?);
3227lapply (refl ? (f b1)); cases (f b1) in ⊢ (???% → %);
3228[ #_ whd in ⊢ (??%? → ?); #H @False_ind @(False_ind … (grumpydestruct … H))
3229| #delta' #DELTA whd in ⊢ (??%? → ?); #H elim (grumpydestruct2 ?????? H);
3230    #eb #edelta
3231] lapply (load_shift … Hmem_shift LOADV DELTA); *; #v2 *;#LOAD #INJ
3232%{ v2} % //; >Hofs >eb in LOAD >edelta
3233<(?:signed (add ofs1 (repr delta)) = signed ofs1 + delta)
3234[#H' @H' (* XXX // doesn't work *)
3235| <edelta @(address_shift … chunk … Hmem_shift … DELTA)
3236    @(load_valid_access … LOADV)
3237]
3238qed.
3239
3240(* Relation between shifts and stores. *)
3241
3242lemma store_within_shift:
3243  ∀f,chunk,m1,b,ofs,v1,n1,m2,delta,v2.
3244  mem_shift f m1 m2 →
3245  store chunk m1 b ofs v1 = Some ? n1 →
3246  f b = Some ? delta →
3247  val_shift f v1 v2 →
3248  ∃n2.
3249    store chunk m2 b (ofs + delta) v2 = Some ? n2
3250    ∧ mem_shift f n1 n2.
3251#f #chunk #m1 #b #ofs #v1 #n1 #m2 #delta #v2
3252*;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2
3253#STORE1 #INJb #Hval_shift
3254lapply (store_mapped_inj … ms_inj ?? STORE1 ?);
3255[ #chunk' #echunk @(load_result_inject … chunk) /2/;
3256| whd in ⊢ (??%?); >INJb (* XXX: // has stopped working *) napply refl
3257| whd; #b1 #b1' #delta1 #b2 #b2' #delta2
3258    whd in ⊢ (? → ??%? → ??%? → ?);
3259    elim (f b1); elim (f b2);
3260    [#_ #e1 whd in e1:(??%?);destruct;
3261    |#z #_ #e1 whd in e1:(??%?);destruct;
3262    |#z #_ #_ #e2 whd in e2:(??%?);destruct;
3263    |#delta1' #delta2' #neb #e1 #e2
3264       whd in e1:(??%?) e2:(??%?);
3265       destruct;
3266       %{1} %{1} %{1} //;
3267    ]
3268| 7: //;
3269| 4,5,6: ##skip
3270]
3271*;#n2 *;#STORE #MINJ
3272%{ n2} % //; %
3273[ (* inj *) //
3274| (* samedomain *)
3275    >(nextblock_store … STORE1)
3276    >(nextblock_store … STORE)
3277    //;
3278| (* domain *)
3279    >(nextblock_store … STORE1)
3280    //
3281| (* range *)
3282    /2/
3283| #b1 #delta1 #INJb1
3284    >(low_bound_store … STORE b1)
3285    >(high_bound_store … STORE b1)
3286    @ms_range_2 //;
3287] qed.
3288
3289lemma store_outside_shift:
3290  ∀f,chunk,m1,b,ofs,m2,v,m2',delta.
3291  mem_shift f m1 m2 →
3292  f b = Some ? delta →
3293  high_bound m1 b + delta ≤ ofs
3294  ∨ ofs + size_chunk chunk ≤ low_bound m1 b + delta →
3295  store chunk m2 b ofs v = Some ? m2' →
3296  mem_shift f m1 m2'.
3297#f #chunk #m1 #b #ofs #m2 #v #m2' #delta
3298*;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2
3299#INJb #Hbounds #STORE %
3300[ (* inj *)
3301    @(store_outside_inj … STORE) //;
3302    #b' #d' whd in ⊢ (??%? → ?); lapply (refl ? (f b')); elim (f b') in ⊢ (???% → %);
3303    [ #_ #e whd in e:(??%?); destruct;
3304    | #d'' #ef #e elim (grumpydestruct2 ?????? e); #eb #ed
3305        >eb in ef ⊢ % >ed >INJb #ed'
3306        <(grumpydestruct1 ??? ed') //
3307    ]
3308| (* samedomain *) >(nextblock_store … STORE) //
3309| (* domain *) //
3310| (* range *) /2/
3311| #b1 #delta1 #INJb1
3312    >(low_bound_store … STORE b1)
3313    >(high_bound_store … STORE b1)
3314    @ms_range_2 //;
3315] qed.
3316
3317lemma storev_shift:
3318  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
3319  mem_shift f m1 m2 →
3320  storev chunk m1 a1 v1 = Some ? n1 →
3321  val_shift f a1 a2 →
3322  val_shift f v1 v2 →
3323  ∃n2.
3324    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_shift f n1 n2.
3325#f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2
3326#Hmem_shift #STOREV #Hval_shift_a #Hval_shift_v
3327inversion Hval_shift_a;
3328[ 1,2,4: #x #H >H in STOREV #H' whd in H':(??%?); @False_ind destruct; ]
3329#b1 #ofs1 #b2 #ofs2 #delta
3330whd in ⊢ (??%? → ?); lapply (refl ? (f b1)); elim (f b1) in ⊢ (???% → %);
3331[#_ #e whd in e:(??%?); destruct; ]
3332#x #INJb1 #e elim (grumpydestruct2 ?????? e); #eb #ex
3333>ex in INJb1 #INJb1
3334#OFS #ea1 #ea2 >ea1 in STOREV #STOREV
3335lapply (store_within_shift … Hmem_shift STOREV INJb1 Hval_shift_v);
3336*; #n2 *; #A #B
3337%{ n2} % //;
3338>OFS >eb in A
3339<(?:signed (add ofs1 (repr delta)) = signed ofs1 + delta)
3340[ #H @H (* XXX /2/ *)
3341| @(address_shift … chunk … Hmem_shift ? INJb1)
3342    @(store_valid_access_3 … STOREV)
3343]
3344qed.
3345
3346(* Relation between shifts and [free]. *)
3347
3348lemma free_shift:
3349  ∀f,m1,m2,b.
3350  mem_shift f m1 m2 →
3351  mem_shift f (free m1 b) (free m2 b).
3352#f #m1 #m2 #b
3353*;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 %
3354[ (* inj *)
3355    @free_right_inj [ @free_left_inj //
3356    | #b1 #delta #chunk #ofs whd in ⊢ (??%? → ?);
3357        lapply (refl ? (f b1)); elim (f b1) in ⊢ (???% → %);
3358        [ #_ #e whd in e:(??%?); destruct;
3359        | #delta' #INJb1 #e whd in e:(??%?); destruct;
3360            napply valid_access_free_2
3361        ]
3362    ]
3363| (* samedomain *) whd in ⊢ (??%%); //
3364| (* domain *) >(?:nextblock (free m1 b) = nextblock m1) //
3365| (* range *) /2/
3366| #b' #delta #INJb' cases (decidable_eq_Z b' b); #eb
3367    [ >eb
3368        >(low_bound_free_same ??) >(high_bound_free_same ??)
3369        (* arith *) napply daemon
3370    | >(low_bound_free …) //; >(high_bound_free …) /2/;
3371    ]
3372] qed.
3373
3374(* Relation between shifts and allocation. *)
3375
3376definition shift_incr : memshift → memshift → Prop ≝ λf1,f2: memshift.
3377  ∀b. f1 b = f2 b ∨ f1 b = None ?.
3378
3379lemma shift_incr_inject_incr:
3380  ∀f1,f2.
3381  shift_incr f1 f2 → inject_incr (meminj_of_shift f1) (meminj_of_shift f2).
3382#f1 #f2 #Hshift whd in ⊢ (?%%); whd; #b
3383elim (Hshift b); #INJ >INJ /2/;
3384qed.
3385
3386lemma val_shift_incr:
3387  ∀f1,f2,v1,v2.
3388  shift_incr f1 f2 → val_shift f1 v1 v2 → val_shift f2 v1 v2.
3389#f1 #f2 #v1 #v2 #Hshift_incr whd in ⊢ (% → %);
3390@val_inject_incr
3391@shift_incr_inject_incr //;
3392qed.
3393
3394(* *
3395Remark mem_inj_incr:
3396  ∀f1,f2,m1,m2.
3397  inject_incr f1 f2 → mem_inj val_inject f1 m1 m2 → mem_inj val_inject f2 m1 m2.
3398Proof.
3399  intros; red; intros.
3400  destruct (H b1). rewrite <- H3 in H1.
3401  exploit H0; eauto. intros [v2 [A B]].
3402  exists v2; split. auto. apply val_inject_incr with f1; auto.
3403  congruence.
3404***)
3405
3406lemma alloc_shift:
3407  ∀f,m1,m2,lo1,hi1,m1',b,delta,lo2,hi2.
3408  mem_shift f m1 m2 →
3409  alloc m1 lo1 hi1 = 〈m1', b〉 →
3410  lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 →
3411  min_signed ≤ delta ∧ delta ≤ max_signed →
3412  min_signed ≤ lo2 → hi2 ≤ max_signed →
3413  inj_offset_aligned delta (hi1-lo1) →
3414  ∃f'. ∃m2'.
3415     alloc m2 lo2 hi2 = 〈m2', b〉
3416  ∧ mem_shift f' m1' m2'
3417  ∧ shift_incr f f'
3418  ∧ f' b = Some ? delta.
3419#f #m1 #m2 #lo1 #hi1 #m1' #b #delta #lo2 #hi2
3420*;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2
3421#ALLOC #Hlo_delta #Hhi_delta #Hdelta_range #Hlo_range #Hhi_range #Hinj_aligned
3422lapply (refl ? (alloc m2 lo2 hi2)); elim (alloc m2 lo2 hi2) in ⊢ (???% → %);
3423#m2' #b' #ALLOC2
3424cut (b' = b);
3425[ >(alloc_result … ALLOC) >(alloc_result … ALLOC2) // ]
3426#eb >eb
3427cut (f b = None ?);
3428[ lapply (ms_domain b); >(alloc_result … ALLOC)
3429    elim (f (nextblock m1)); //;
3430    #z (* arith *) napply daemon
3431]
3432#FB
3433letin f' ≝ (λb':block. if eqZb b' b then Some ? delta else f b');
3434cut (shift_incr f f');
3435[ whd; #b0 whd in ⊢ (?(???%)?);
3436    @eqZb_elim /2/; ]
3437#Hshift_incr
3438cut (f' b = Some ? delta);
3439[ whd in ⊢ (??%?); >(eqZb_z_z …) // ] #efb'
3440%{ f'} %{ m2'} % //; % //; % //; %
3441[ (* inj *)
3442    cut (mem_inj val_inject (meminj_of_shift f') m1 m2);
3443    [ whd; #chunk #b1 #ofs #v1 #b2 #delta2 #MINJf' #LOAD
3444        cut (meminj_of_shift f b1 = Some ? 〈b2, delta2〉);
3445        [ <MINJf' whd in ⊢ (???(?%?)); whd in ⊢ (??%%);
3446            @eqZb_elim //; #eb
3447            >eb
3448            cut (valid_block m1 b);
3449            [ @valid_access_valid_block
3450              [ 3: @load_valid_access // ]
3451            ]
3452            cut (¬valid_block m1 b); [ /2/ ]
3453            #H #H' @False_ind napply (absurd ? H' H)
3454        ] #MINJf
3455        lapply (ms_inj … MINJf LOAD); *; #v2 *; #A #B
3456        %{ v2} % //;
3457        @(val_inject_incr … B)
3458        @shift_incr_inject_incr //
3459    ] #Hmem_inj
3460    @(alloc_parallel_inj … delta Hmem_inj ALLOC ALLOC2 ?) /2/;
3461    whd in ⊢ (??%?); >efb' /2/;
3462| (* samedomain *)
3463    >(nextblock_alloc … ALLOC)
3464    >(nextblock_alloc … ALLOC2)
3465    //;
3466| (* domain *)
3467    #b0 (* FIXME: unfold *) >(refl ? (f' b0):f' b0 = if eqZb b0 b then Some ? delta else f b0)
3468    >(nextblock_alloc … ALLOC)
3469    >(alloc_result … ALLOC)
3470    @eqZb_elim #eb0
3471    [ >eb0 (* arith *) napply daemon
3472    | lapply (ms_domain b0); elim (f b0);
3473        (* arith *) napply daemon
3474    ]
3475| (* range *)
3476    #b0 #delta0 whd in ⊢ (??%? → ?);
3477    @eqZb_elim
3478    [ #_ #e <(grumpydestruct1 ??? e) //
3479    | #neb #e @(ms_range_1 … b0) @e
3480    ]
3481| #b0 #delta0 whd in ⊢ (??%? → ?);
3482    >(low_bound_alloc … ALLOC2 ?)
3483    >(high_bound_alloc … ALLOC2 ?)
3484    @eqZb_elim #eb0 >eb
3485    [ >eb0 #ed <(grumpydestruct1 ??? ed)
3486        >(eqZb_z_z ?) /3/;
3487    | #edelta0 >(eqZb_false … eb0)
3488        @ms_range_2 whd in edelta0:(??%?); //;
3489    ]
3490]
3491qed.
3492*)*)
3493(* ** Relation between signed and unsigned loads and stores *)
3494
3495(* Target processors do not distinguish between signed and unsigned
3496  stores of 8- and 16-bit quantities.  We show these are equivalent. *)
3497
3498(* Signed 8- and 16-bit stores can be performed like unsigned stores. *)
3499
3500lemma in_bounds_equiv:
3501  ∀chunk1,chunk2,m,r,b,ofs.∀A:Type[0].∀a1,a2: A.
3502  size_chunk chunk1 = size_chunk chunk2 →
3503  (match in_bounds m chunk1 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
3504  (match in_bounds m chunk2 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
3505#chunk1 #chunk2 #m #r #b #ofs #A #a1 #a2 #Hsize
3506elim (in_bounds m chunk1 r b ofs);
3507[ #H whd in ⊢ (??%?); >(in_bounds_true … A a1 a2 ?) //;
3508    @valid_access_compat //;
3509| #H whd in ⊢ (??%?); elim (in_bounds m chunk2 r b ofs); //;
3510    #H' @False_ind @(absurd ?? H)
3511    @valid_access_compat //;
3512] qed.
3513
3514lemma storev_8_signed_unsigned:
3515  ∀m,a,v.
3516  storev Mint8signed m a v = storev Mint8unsigned m a v.
3517#m #a #v whd in ⊢ (??%%) elim a //
3518#r #b #p #ofs whd in ⊢ (??%%)
3519>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
3520qed.
3521
3522lemma storev_16_signed_unsigned:
3523  ∀m,a,v.
3524  storev Mint16signed m a v = storev Mint16unsigned m a v.
3525#m #a #v whd in ⊢ (??%%) elim a //
3526#r #b #p #ofs whd in ⊢ (??%%)
3527>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
3528qed.
3529
3530(* Likewise, some target processors (e.g. the PowerPC) do not have
3531  a ``load 8-bit signed integer'' instruction. 
3532  We show that it can be synthesized as a ``load 8-bit unsigned integer''
3533  followed by a sign extension. *)
3534
3535(* Nonessential properties that may require arithmetic
3536lemma loadv_8_signed_unsigned:
3537  ∀m,a.
3538  loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a).
3539#m #a whd in ⊢ (??%(????(%))); elim a; //;
3540#r #b #ofs whd in ⊢ (??%(????%));
3541>(in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???) //;
3542elim (in_bounds m Mint8unsigned r b (signed ofs)); /2/;
3543#H whd in ⊢ (??%%);
3544elim (getN 0 (signed ofs) (contents (blocks m b)));
3545[ 1,3: //;
3546| #i whd in ⊢ (??(??%)(??%));
3547    >(sign_ext_zero_ext ?? i) [ @refl (* XXX: // ? *)
3548    | (* arith *) @daemon
3549    ]
3550| #sp cases sp; //;
3551]
3552qed.
3553*)
Note: See TracBrowser for help on using the repository browser.