source: C-semantics/Mem.ma @ 124

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

Initial work on Clight semantics with 8051 memory spaces.

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