source: src/common/Mem.ma @ 718

Last change on this file since 718 was 718, checked in by campbell, 10 years ago

Add an AST type (i.e., intermediate language type) for pointers.

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