source: C-semantics/Mem.ma @ 153

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

Use appropriate memory chunks for 8051 pointers.

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