source: C-semantics/Mem.ma @ 14

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

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

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