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

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

Comment out daemon and its uses - we don't need the properties of the memory
model at the moment.

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