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

Last change on this file since 496 was 496, checked in by campbell, 8 years ago

First pass at moving regions to block type.

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