source: C-semantics/Mem.ma @ 3

Last change on this file since 3 was 3, checked in by campbell, 11 years ago

Import work-in-progress port of the CompCert? C semantics to matita.

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