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

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

Port Clight semantics to the new-new matita syntax.

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