source: C-semantics/Mem.ma @ 125

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

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

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