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

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

"memory_space" to "region" replacement to match ocaml code

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