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

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

Remove bogus pointer compatibility case.

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