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

Last change on this file since 484 was 484, checked in by campbell, 8 years ago

Separate out null values from integer zeros.

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