source: C-semantics/Mem.ma @ 10

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

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File size: 121.2 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(*  XXX: reenable once I've sorted out performance a bit
1704ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem.
1705  ∀b1,b1',delta1,b2,b2',delta2.
1706  b1 ≠ b2 →
1707  mi b1 = Some ? 〈b1', delta1〉 →
1708  mi b2 = Some ? 〈b2', delta2〉 →
1709  b1' ≠ b2'
1710  ∨ low_bound m b1 ≥ high_bound m b1
1711  ∨ low_bound m b2 ≥ high_bound m b2
1712  ∨ (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2
1713  ∨ high_bound m b2 + delta2 ≤ low_bound m b1 + delta1).
1714
1715(* FIXME *)
1716nlemma grumpydestruct1 : ∀A,x1,x2. Some A x1 = Some A x2 → x1 = x2.
1717#A;#x1;#x2;#H;ndestruct;//;
1718nqed.
1719nlemma grumpydestruct2 : ∀A,B,x1,y1,x2,y2. Some (A×B) 〈x1,y1〉 = Some (A×B) 〈x2,y2〉 → x1 = x2 ∧ y1 = y2.
1720#A;#B;#x1;#y1;#x2;#y2;#H;ndestruct;/2/;
1721nqed.
1722
1723nlemma store_mapped_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef.
1724  ∀mi,m1,m2,b1,ofs,b2,delta,v1,v2,chunk,m1'.
1725  mem_inj val_inj mi m1 m2 →
1726  meminj_no_overlap mi m1 →
1727  mi b1 = Some ? 〈b2, delta〉 →
1728  store chunk m1 b1 ofs v1 = Some ? m1' →
1729  (∀chunk'. size_chunk chunk' = size_chunk chunk →
1730    val_inj mi (load_result chunk' v1) (load_result chunk' v2)) →
1731  ∃m2'.
1732  store chunk m2 b2 (ofs + delta) v2 = Some ? m2' ∧ mem_inj val_inj mi m1' m2'.
1733#val_inj;#val_inj_undef;
1734#mi;#m1;#m2;#b1;#ofs;#b2;#delta;#v1;#v2;#chunk;#m1';
1735#Hinj;#Hnoover;#Hb1;#STORE;#Hvalinj;
1736ncut (∃m2'.store chunk m2 b2 (ofs + delta) v2 = Some ? m2');
1737##[ napply valid_access_store; napply (valid_access_inj ? mi ??????? Hb1 Hinj ?); (* XXX why do I have to give mi here? *) /2/
1738##| *;#m2';#STORE2;
1739    @ m2'; @; //;
1740    nwhd; #chunk';#b1';#ofs';#v;#b2';#delta';#CP;#LOAD1;
1741    ncut (valid_access m1 chunk' b1' ofs');
1742    ##[ napply (store_valid_access_2 … STORE); napply (load_valid_access … LOAD1);
1743    ##| #Hval;
1744        nlapply (load_store_characterization … STORE … Hval);
1745        nelim (load_store_classification chunk b1 ofs chunk' b1' ofs');
1746        ##[ #e;#e0;#e1;#H; (* similar *)
1747            nrewrite > e in Hb1; #Hb1;
1748            nrewrite > CP in Hb1; #Hb1; (* XXX too long ndestruct;*)
1749            nelim (grumpydestruct2 ?????? Hb1);
1750            #e2;#e3; nrewrite < e0; nrewrite > e2; nrewrite > e3;
1751            @ (load_result chunk' v2);@;
1752            ##[ napply (load_store_similar … STORE2); //
1753            ##| nrewrite > LOAD1 in H; #H; nwhd in H:(??%%);
1754                nrewrite > (grumpydestruct1 … H); napply Hvalinj;
1755                napply sym_eq; //
1756            ##]
1757         ##| #Hdis; #H; (* disjoint *)
1758             nrewrite > LOAD1 in H; #H;
1759             nlapply (Hinj … CP ?); ##[ napply sym_eq; napply H; ##| ##*: ##]
1760             *;#v2';*;#LOAD2;#VCP;
1761             @ v2'; @; //;
1762             nrewrite < LOAD2; napply (load_store_other … STORE2);
1763             nelim (decidable_eq_Z b1 b1'); #eb1;
1764             ##[ nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
1765                 nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
1766                 nelim Hdis; ##[ #Hdis; nelim Hdis;
1767                               ##[ #eb1'; napply False_ind; napply (absurd ? eb1 eb1');
1768                               ##| #Hdis;@1;@2;(* arith *) napply daemon
1769                               ##] ##| #Hdis;@2;(* arith *) napply daemon ##]
1770             ##| ncut (valid_access m1 chunk b1 ofs); /2/; #Hval';
1771                 nlapply (Hnoover … eb1 Hb1 CP);
1772                 #Ha; nelim Ha; #Ha;
1773                 ##[ nelim Ha; #Ha;
1774                 ##[ nelim Ha; #Ha;
1775                 ##[ @1;@1;/2/
1776                 ##| nelim Hval'; nlapply (size_chunk_pos chunk); (* arith *) napply daemon ##]
1777                 ##| nelim Hval; nlapply (size_chunk_pos chunk'); (* arith *) napply daemon ##]
1778                 ##| nelim Hval'; nelim Hval;  (* arith *) napply daemon ##]
1779             ##]
1780         ##| #eb1;#Hofs1;#Hofs2;#Hofs3;#H; (* overlapping *)
1781             nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
1782             nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
1783             ncut (∃v2'. load chunk' m2' b2 (ofs' + delta) = Some ? v2');
1784             ##[ napply valid_access_load; napply (store_valid_access_1 … STORE2); napply (valid_access_inj … Hinj Hval); nrewrite > eb1; //
1785             ##| *;#v2';#LOAD2';
1786                 ncut (v2' = Vundef); ##[ napply (load_store_overlap … STORE2 … LOAD2'); (* arith *) napply daemon ##| ##]
1787                 #ev2'; @ v2'; @;//;
1788                 nrewrite > LOAD1 in H;#H; nwhd in H:(??%%); nrewrite > (grumpydestruct1 … H);
1789                 nrewrite > ev2';
1790                 napply val_inj_undef; ##]
1791         ##| #eb1;#Hofs;nrewrite < Hofs in Hval LOAD1 ⊢ %;#Hval;#LOAD1;#Hsize;#H; (* overlapping *)
1792             
1793             nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
1794             nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
1795             ncut (∃v2'. load chunk' m2' b2 (ofs + delta) = Some ? v2');
1796             ##[ napply valid_access_load; napply (store_valid_access_1 … STORE2); napply (valid_access_inj … Hinj Hval); nrewrite > eb1; //
1797             ##| *;#v2';#LOAD2';
1798                 ncut (v2' = Vundef); ##[ napply (load_store_mismatch … STORE2 … LOAD2' ?); napply sym_neq;// ##| ##]
1799                 #ev2'; @ v2'; @;//;
1800                 nrewrite > LOAD1 in H;#H; nwhd in H:(??%%); nrewrite > (grumpydestruct1 … H);
1801                 nrewrite > ev2';
1802                 napply val_inj_undef; ##]
1803         ##]
1804     ##]
1805##] nqed.
1806
1807ndefinition inj_offset_aligned ≝ λdelta: Z. λsize: Z.
1808  ∀chunk. size_chunk chunk ≤ size → (align_chunk chunk ∣ delta).
1809
1810nlemma alloc_parallel_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef.
1811  ∀mi,m1,m2,lo1,hi1,m1',b1,lo2,hi2,m2',b2,delta.
1812  mem_inj val_inj mi m1 m2 →
1813  alloc m1 lo1 hi1 = 〈m1', b1〉 →
1814  alloc m2 lo2 hi2 = 〈m2', b2〉 →
1815  mi b1 = Some ? 〈b2, delta〉 →
1816  lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 →
1817  inj_offset_aligned delta (hi1 - lo1) →
1818  mem_inj val_inj mi m1' m2'.
1819#val_inj;#val_inj_undef;
1820#mi;#m1;#m2;#lo1;#hi1;#m1';#b1;#lo2;#hi2;#m2';#b2;#delta;
1821#Hinj;#ALLOC1;#ALLOC2;#Hbinj;#Hlo;#Hhi;#Hal;
1822nwhd; #chunk;#b1';#ofs;#v;#b2';#delta';#Hbinj';#LOAD;
1823nlapply (valid_access_alloc_inv … m1 … ALLOC1 chunk b1' ofs ?); /2/;
1824*;
1825##[ #A;
1826    ncut (load chunk m1 b1' ofs = Some ? v);
1827    ##[ nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC1); /2/; ##]
1828    #LOAD0; nlapply (Hinj … Hbinj' LOAD0); *;#v2;*;#LOAD2;#VINJ;
1829    @ v2; @;
1830    ##[ nrewrite < LOAD2; napply (load_alloc_unchanged … ALLOC2);
1831        napply valid_access_valid_block; ##[ ##3: napply load_valid_access; ##]
1832        //
1833    ##| //
1834    ##]
1835##| *;*;#A;#B;#C;
1836    nrewrite > A in Hbinj' LOAD; #Hbinj';#LOAD;
1837    nrewrite > Hbinj in Hbinj'; #Hbinj'; nelim (grumpydestruct2 ?????? Hbinj');
1838    #eb2;#edelta; nrewrite < eb2; nrewrite < edelta;
1839    ncut (v = Vundef); ##[ napply (load_alloc_same … ALLOC1 … LOAD); ##]
1840    #ev; nrewrite > ev;
1841    ncut (∃v2. load chunk m2' b2 (ofs + delta) = Some ? v2);
1842    ##[ napply valid_access_load;
1843        napply (valid_access_alloc_same … ALLOC2);
1844        ##[ ##1,2: (*arith*) napply daemon;
1845        ##| (* arith using Hal *) napply daemon
1846        ##] ##]
1847    *;#v2;#LOAD2;
1848    ncut (v2 = Vundef); ##[ napply (load_alloc_same … ALLOC2 … LOAD2) ##]
1849    #ev2; nrewrite > ev2;
1850    @ Vundef; @; //;
1851##] nqed.
1852
1853nlemma alloc_right_inj: ∀val_inj.
1854  ∀mi,m1,m2,lo,hi,b2,m2'.
1855  mem_inj val_inj mi m1 m2 →
1856  alloc m2 lo hi = 〈m2', b2〉 →
1857  mem_inj val_inj mi m1 m2'.
1858#val_inj;
1859#mi;#m1;#m2;#lo;#hi;#b2;#m2';
1860#Hinj;#ALLOC;
1861nwhd; #chunk; #b1; #ofs; #v1; #b2'; #delta; #Hbinj; #LOAD;
1862nlapply (Hinj … Hbinj LOAD); *; #v2;*;#LOAD2;#VINJ;
1863@ v2; @; //;
1864ncut (valid_block m2 b2');
1865  ##[ napply (valid_access_valid_block ? chunk ? (ofs + delta)); /2/ ##]
1866#Hval;
1867nrewrite < LOAD2; napply (load_alloc_unchanged … ALLOC … Hval);
1868nqed.
1869
1870(*
1871Hypothesis val_inj_undef_any:
1872  ∀mi,v. val_inj mi Vundef v.
1873*)
1874
1875nlemma alloc_left_unmapped_inj: ∀val_inj.
1876  ∀mi,m1,m2,lo,hi,b1,m1'.
1877  mem_inj val_inj mi m1 m2 →
1878  alloc m1 lo hi = 〈m1', b1〉 →
1879  mi b1 = None ? →
1880  mem_inj val_inj mi m1' m2.
1881#val_inj;
1882#mi;#m1;#m2;#lo;#hi;#b1;#m1';
1883#Hinj;#ALLOC;#Hbinj;
1884nwhd;  #chunk; #b1'; #ofs; #v1; #b2'; #delta; #Hbinj'; #LOAD;
1885nlapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
1886*;
1887##[ #A;
1888  napply (Hinj … Hbinj' );
1889  nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC); /2/;
1890##| *;*;#A;#B;#C;
1891  nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD;
1892  nrewrite > Hbinj in Hbinj'; #bad; (* XXX ndestruct doesn't complete *) nelim (grumpydestruct ?? bad);
1893##] nqed.
1894
1895nlemma alloc_left_mapped_inj: ∀val_inj.∀val_inj_undef_any:∀mi,v. val_inj mi Vundef v.
1896  ∀mi,m1,m2,lo,hi,b1,m1',b2,delta.
1897  mem_inj val_inj mi m1 m2 →
1898  alloc m1 lo hi = 〈m1', b1〉 →
1899  mi b1 = Some ? 〈b2, delta〉 →
1900  valid_block m2 b2 →
1901  low_bound m2 b2 ≤ lo + delta → hi + delta ≤ high_bound m2 b2 →
1902  inj_offset_aligned delta (hi - lo) →
1903  mem_inj val_inj mi m1' m2.
1904#val_inj;#val_inj_undef_any;
1905#mi;#m1;#m2;#lo;#hi;#b1;#m1';#b2;#delta;
1906#Hinj;#ALLOC;#Hbinj;#Hval;#Hlo;#Hhi;#Hal;
1907nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
1908nlapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
1909*;
1910##[ #A;
1911    napply (Hinj … Hbinj');
1912    nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC); /2/;
1913##| *;*;#A;#B;*;#C;#D;
1914    nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD; nrewrite > Hbinj in Hbinj';
1915    #Hbinj'; (* XXX surprised ndestruct can't copy here *) nelim (grumpydestruct2 ?????? Hbinj'); #eb2; #edelta;
1916    nrewrite < eb2; nrewrite < edelta;
1917    ncut (v1 = Vundef); ##[ napply (load_alloc_same … ALLOC … LOAD) ##]
1918    #ev1; nrewrite > ev1;
1919    ncut (∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2);
1920    ##[ napply valid_access_load; @; //;
1921      ##[ (* arith *) napply daemon
1922      ##| (* arith *) napply daemon
1923      ##| (* arith *) napply daemon
1924      ##]
1925    ##]
1926    *;#v2;#LOAD2; @ v2; @; //;
1927##] nqed.
1928
1929nlemma free_parallel_inj: ∀val_inj.
1930  ∀mi,m1,m2,b1,b2,delta.
1931  mem_inj val_inj mi m1 m2 →
1932  mi b1 = Some ? 〈b2, delta〉 →
1933  (∀b,delta'. mi b = Some ? 〈b2, delta'〉 → b = b1) →
1934  mem_inj val_inj mi (free m1 b1) (free m2 b2).
1935#val_inj;
1936#mi;#m1;#m2;#b1;#b2;#delta; #Hinj;#Hb1inj;#Hbinj;
1937nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
1938nlapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A;#B;
1939ncut (load chunk m1 b1' ofs = Some ? v1);
1940##[ nrewrite < LOAD; napply sym_eq; napply load_free; napply B ##] #LOAD';
1941nelim (Hinj … Hbinj' LOAD'); #v2;*;#LOAD2;#INJ;
1942@ v2;@;
1943##[ nrewrite < LOAD2; napply load_free;
1944    napply nmk; #e; napply (absurd ?? B);
1945    nrewrite > e in Hbinj'; #Hbinj'; napply (Hbinj ?? Hbinj');
1946##| //
1947##] nqed.
1948
1949nlemma free_left_inj: ∀val_inj.
1950  ∀mi,m1,m2,b1.
1951  mem_inj val_inj mi m1 m2 →
1952  mem_inj val_inj mi (free m1 b1) m2.
1953#val_inj;#mi;#m1;#m2;#b1;#Hinj;
1954nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
1955nlapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A;#B;
1956napply (Hinj … Hbinj');
1957nrewrite < LOAD; napply sym_eq; napply load_free; napply B;
1958nqed.
1959
1960nlemma free_list_left_inj: ∀val_inj.
1961  ∀mi,bl,m1,m2.
1962  mem_inj val_inj mi m1 m2 →
1963  mem_inj val_inj mi (free_list m1 bl) m2.
1964#val_inj;#mi;#bl;nelim bl;
1965##[ nwhd in ⊢ (?→?→?→???%?); //
1966##| #h;#t;#IH; #m1;#m2;#H; nrewrite > (unfold_free_list m1 h t);
1967    napply free_left_inj; napply IH; //
1968##] nqed.
1969
1970nlemma free_right_inj: ∀val_inj.
1971  ∀mi,m1,m2,b2.
1972  mem_inj val_inj mi m1 m2 →
1973  (∀b1,delta,chunk,ofs.
1974   mi b1 = Some ? 〈b2, delta〉 → ¬(valid_access m1 chunk b1 ofs)) →
1975  mem_inj val_inj mi m1 (free m2 b2).
1976#val_inj;#mi;#m1;#m2;#b2; #Hinj; #Hinval;
1977nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
1978ncut (b2' ≠ b2);
1979##[ napply nmk; #e; nrewrite > e in Hbinj'; #Hbinj';
1980    napply (absurd ?? (Hinval … Hbinj')); napply (load_valid_access … LOAD); ##]
1981#ne; nlapply (Hinj … Hbinj' LOAD); *;#v2;*;#LOAD2;#INJ;
1982@ v2; @; //;
1983nrewrite < LOAD2; napply load_free; napply ne;
1984nqed.
1985
1986nlemma valid_pointer_inj: ∀val_inj.
1987  ∀mi,m1,m2,b1,ofs,b2,delta.
1988  mi b1 = Some ? 〈b2, delta〉 →
1989  mem_inj val_inj mi m1 m2 →
1990  valid_pointer m1 b1 ofs = true →
1991  valid_pointer m2 b2 (ofs + delta) = true.
1992#val_inj;#mi;#m1;#m2;#b1;#ofs;#b2;#delta;#Hbinj;#Hinj;#VALID;
1993nlapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval;
1994napply (proj2 ?? (valid_pointer_valid_access ???));
1995napply (valid_access_inj … Hval); //;
1996nqed.
1997
1998(*
1999End GENERIC_INJECT.
2000*)
2001(* ** Store extensions *)
2002
2003(* A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
2004  by increasing the sizes of the memory blocks of [m1] (decreasing
2005  the low bounds, increasing the high bounds), while still keeping the
2006  same contents for block offsets that are valid in [m1]. *)
2007
2008ndefinition inject_id : meminj ≝ λb. Some ? 〈b, OZ〉.
2009
2010ndefinition val_inj_id ≝ λmi: meminj. λv1,v2: val. v1 = v2.
2011
2012ndefinition extends ≝ λm1,m2: mem.
2013  nextblock m1 = nextblock m2 ∧ mem_inj val_inj_id inject_id m1 m2.
2014
2015ntheorem extends_refl:
2016  ∀m: mem. extends m m.
2017#m;@;//;
2018nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;nnormalize in ⊢ (%→?);#H;
2019(* XXX: *really* suprised ndestruct didn't complete *) nelim (grumpydestruct2 ?????? H); #eb1;#edelta;#LOAD;
2020@ v1; @;
2021##[ nrewrite < edelta; nrewrite > (Zplus_z_OZ ofs); //;
2022##| //
2023##] nqed.
2024
2025ntheorem alloc_extends:
2026  ∀m1,m2,m1',m2': mem. ∀lo1,hi1,lo2,hi2: Z. ∀b1,b2: block.
2027  extends m1 m2 →
2028  lo2 ≤ lo1 → hi1 ≤ hi2 →
2029  alloc m1 lo1 hi1 = 〈m1', b1〉 →
2030  alloc m2 lo2 hi2 = 〈m2', b2〉 →
2031  b1 = b2 ∧ extends m1' m2'.
2032#m1;#m2;#m1';#m2';#lo1;#hi1;#lo2;#hi2;#b1;#b2;
2033*;#Hnext;#Hinj;#Hlo;#Hhi;#ALLOC1;#ALLOC2;
2034ncut (b1 = b2);
2035##[ napply (transitive_eq … (nextblock m1)); ##[ napply (alloc_result … ALLOC1);
2036    ##| napply sym_eq; nrewrite > Hnext; napply (alloc_result … ALLOC2) ##] ##]
2037#eb; nrewrite < eb in ALLOC2 ⊢ %; #ALLOC2; @; //; @;
2038##[ nrewrite > (nextblock_alloc … ALLOC1);
2039    nrewrite > (nextblock_alloc … ALLOC2);
2040    //;
2041##| napply (alloc_parallel_inj ??????????????? ALLOC1 ALLOC2 ????);
2042  ##[ ##1,4: nnormalize; //;
2043  ##| ##3,5,6: //
2044  ##| ##7: nwhd; #chunk;#Hsize; (* divides 0 *) napply daemon
2045  ##]
2046##] nqed.
2047
2048ntheorem free_extends:
2049  ∀m1,m2: mem. ∀b: block.
2050  extends m1 m2 →
2051  extends (free m1 b) (free m2 b).
2052#m1;#m2;#b;*;#Hnext;#Hinj; @;
2053##[ nnormalize; //;
2054##| napply (free_parallel_inj … Hinj);
2055  ##[ ##2: //;
2056  ##| ##3: nnormalize; #b';#delta;#ee;
2057           nelim (grumpydestruct2 ?????? ee); //
2058  ##]
2059##] nqed.
2060
2061ntheorem load_extends:
2062  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val.
2063  extends m1 m2 →
2064  load chunk m1 b ofs = Some ? v →
2065  load chunk m2 b ofs = Some ? v.
2066#chunk;#m1;#m2;#b;#ofs;#v;
2067*;#Hnext;#Hinj;#LOAD;
2068nlapply (Hinj … LOAD); ##[ nnormalize; // ##| ##2,3: ##]
2069*;#v2;*; nrewrite > (Zplus_z_OZ ofs); #LOAD2;#EQ;nwhd in EQ;
2070//;
2071nqed.
2072
2073ntheorem store_within_extends:
2074  ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val.
2075  extends m1 m2 →
2076  store chunk m1 b ofs v = Some ? m1' →
2077  ∃m2'. store chunk m2 b ofs v = Some ? m2' ∧ extends m1' m2'.
2078#chunk;#m1;#m2;#m1';#b;#ofs;#v;*;#Hnext;#Hinj;#STORE1;
2079nlapply (store_mapped_inj … Hinj ?? STORE1 ?);
2080##[ ##1,2,7: nnormalize; //
2081##| (* TODO: unfolding, etc ought to tidy this up *)
2082    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neb;#Hinj1;#Hinj2;
2083    nnormalize in Hinj1 Hinj2; @1; @1; @1; ndestruct; //
2084##| ##4,5,6: ##skip
2085##]
2086*;#m2';*;#STORE;#MINJ;
2087@ m2'; @; nrewrite > (Zplus_z_OZ ofs) in STORE; #STORE; //;
2088@;
2089##[ nrewrite > (nextblock_store … STORE1);
2090    nrewrite > (nextblock_store … STORE);
2091    //
2092##| //
2093##] nqed.
2094
2095ntheorem store_outside_extends:
2096  ∀chunk: memory_chunk. ∀m1,m2,m2': mem. ∀b: block. ∀ofs: Z. ∀v: val.
2097  extends m1 m2 →
2098  ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs →
2099  store chunk m2 b ofs v = Some ? m2' →
2100  extends m1 m2'.
2101#chunk;#m1;#m2;#m2';#b;#ofs;#v;*;#Hnext;#Hinj;#Houtside;#STORE; @;
2102##[ nrewrite > (nextblock_store … STORE); //
2103##| napply (store_outside_inj … STORE); //;
2104    #b';#delta;#einj;nnormalize in einj; ndestruct;
2105    nelim Houtside;
2106    ##[ #lo;@ 2; nrewrite > (Zplus_z_OZ ?); //
2107    ##| #hi;@ 1;  nrewrite > (Zplus_z_OZ ?); //
2108    ##]
2109##] nqed.
2110
2111ntheorem valid_pointer_extends:
2112  ∀m1,m2,b,ofs.
2113  extends m1 m2 → valid_pointer m1 b ofs = true →
2114  valid_pointer m2 b ofs = true.
2115#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
2116nrewrite < (Zplus_z_OZ ofs);
2117napply (valid_pointer_inj … Hinj VALID); //;
2118nqed.
2119
2120
2121(* * The ``less defined than'' relation over memory states *)
2122
2123(* A memory state [m1] is less defined than [m2] if, for all addresses,
2124  the value [v1] read in [m1] at this address is less defined than
2125  the value [v2] read in [m2], that is, either [v1 = v2] or [v1 = Vundef]. *)
2126
2127ndefinition val_inj_lessdef ≝ λmi: meminj. λv1,v2: val.
2128  Val_lessdef v1 v2.
2129
2130ndefinition lessdef ≝ λm1,m2: mem.
2131  nextblock m1 = nextblock m2 ∧
2132  mem_inj val_inj_lessdef inject_id m1 m2.
2133
2134nlemma lessdef_refl:
2135  ∀m. lessdef m m.
2136#m; @; //;
2137nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;#H;#LOAD;
2138nwhd in H:(??%?); nelim (grumpydestruct2 ?????? H); #eb1; #edelta;
2139@ v1; @; //;
2140nqed.
2141
2142nlemma load_lessdef:
2143  ∀m1,m2,chunk,b,ofs,v1.
2144  lessdef m1 m2 → load chunk m1 b ofs = Some ? v1 →
2145  ∃v2. load chunk m2 b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
2146#m1;#m2;#chunk;#b;#ofs;#v1;*;#Hnext;#Hinj;#LOAD0;
2147nlapply (Hinj … LOAD0); ##[ nwhd in ⊢ (??%?); // ##| ##2,3:##skip ##]
2148*;#v2;*;#LOAD;#INJ; @ v2; @;//;
2149nqed.
2150
2151nlemma loadv_lessdef:
2152  ∀m1,m2,chunk,addr1,addr2,v1.
2153  lessdef m1 m2 → Val_lessdef addr1 addr2 →
2154  loadv chunk m1 addr1 = Some ? v1 →
2155  ∃v2. loadv chunk m2 addr2 = Some ? v2 ∧ Val_lessdef v1 v2.
2156#m1;#m2;#chunk;#addr1;#addr2;#v1;#H;#H0;#LOAD;
2157ninversion H0;
2158##[ #v; #e1;#e2; nrewrite > e1 in LOAD; ncases v;
2159    ##[ nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
2160    ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
2161    ##| #b';#off; napply load_lessdef; //
2162    ##]
2163##| #v;#e;nrewrite > e in LOAD; #LOAD; nwhd in LOAD:(??%?); napply False_ind (* XXX otherwise ndestruct takes 30s *); ndestruct
2164##] nqed.
2165
2166nlemma store_lessdef:
2167  ∀m1,m2,chunk,b,ofs,v1,v2,m1'.
2168  lessdef m1 m2 → Val_lessdef v1 v2 →
2169  store chunk m1 b ofs v1 = Some ? m1' →
2170  ∃m2'. store chunk m2 b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
2171#m1;#m2;#chunk;#b;#ofs;#v1;#v2;#m1';
2172*;#Hnext;#Hinj;#Hvless;#STORE0;
2173nlapply (store_mapped_inj … Hinj … STORE0 ?);
2174##[ #chunk';#Hsize;nwhd;napply load_result_lessdef;napply Hvless
2175##| nwhd in ⊢ (??%?); //
2176##| nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neq;
2177    nwhd in ⊢ ((??%?)→(??%?)→?); #e1; #e2; ndestruct;
2178    @;@;@;//
2179##| ##7: #mi; nwhd; //;
2180##| ##8: *;#m2';*;#STORE;#MINJ;
2181         @ m2';@; /2/;
2182         @;
2183         nrewrite > (nextblock_store … STORE0);
2184         nrewrite > (nextblock_store … STORE);
2185         //;
2186##] nqed.
2187
2188nlemma storev_lessdef:
2189  ∀m1,m2,chunk,addr1,v1,addr2,v2,m1'.
2190  lessdef m1 m2 → Val_lessdef addr1 addr2 → Val_lessdef v1 v2 →
2191  storev chunk m1 addr1 v1 = Some ? m1' →
2192  ∃m2'. storev chunk m2 addr2 v2 = Some ? m2' ∧ lessdef m1' m2'.
2193#m1;#m2;#chunk;#addr1;#v1;#addr2;#v2;#m1';
2194#Hmless;#Haless;#Hvless;#STORE;
2195ninversion Haless;
2196##[ #v; #e1;#e2; nrewrite > e1 in STORE; ncases v;
2197    ##[ nwhd in ⊢ ((??%?)→?); #H'; napply False_ind; ndestruct;
2198    ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; napply False_ind; ndestruct;
2199    ##| #b';#off; napply store_lessdef; //
2200    ##]
2201##| #v;#e;nrewrite > e in STORE; #STORE; nwhd in STORE:(??%?); napply False_ind (* XXX otherwise ndestruct fails *); ndestruct
2202##] nqed.
2203
2204nlemma alloc_lessdef:
2205  ∀m1,m2,lo,hi,b1,m1',b2,m2'.
2206  lessdef m1 m2 → alloc m1 lo hi = 〈m1', b1〉 → alloc m2 lo hi = 〈m2', b2〉 →
2207  b1 = b2 ∧ lessdef m1' m2'.
2208#m1;#m2;#lo;#hi;#b1;#m1';#b2;#m2';
2209*;#Hnext;#Hinj;#ALLOC1;#ALLOC2;
2210ncut (b1 = b2);
2211##[ nrewrite > (alloc_result … ALLOC1); nrewrite > (alloc_result … ALLOC2); //
2212##]
2213#e; nrewrite < e in ALLOC2 ⊢ %; #ALLOC2; @; //;
2214@;
2215##[ nrewrite > (nextblock_alloc … ALLOC1);
2216    nrewrite > (nextblock_alloc … ALLOC2);
2217    //
2218##| napply (alloc_parallel_inj … Hinj ALLOC1 ALLOC2);
2219##[ //
2220##| ##3: nwhd in ⊢ (??%?); //
2221##| ##4,5: //;
2222##| ##6: nwhd; #chunk;#_; nwhd; @ O; //;
2223##] nqed.
2224
2225nlemma free_lessdef:
2226  ∀m1,m2,b. lessdef m1 m2 → lessdef (free m1 b) (free m2 b).
2227#m1;#m2;#b;*;#Hnext;#Hinj; @;
2228##[ nwhd in ⊢ (??%%); //
2229##| napply (free_parallel_inj … Hinj); //;
2230    #b';#delta;#H; nwhd in H:(??%?); nelim (grumpydestruct2 ?????? H); //
2231##] nqed.
2232
2233nlemma free_left_lessdef:
2234  ∀m1,m2,b.
2235  lessdef m1 m2 → lessdef (free m1 b) m2.
2236#m1;#m2;#b;*;#Hnext;#Hinj;@;
2237nrewrite < Hnext; //;
2238napply free_left_inj; //;
2239nqed.
2240
2241nlemma free_right_lessdef:
2242  ∀m1,m2,b.
2243  lessdef m1 m2 → low_bound m1 b ≥ high_bound m1 b →
2244  lessdef m1 (free m2 b).
2245#m1;#m2;#b;*;#Hnext;#Hinj;#Hbounds;
2246@; nrewrite > Hnext; //;
2247napply free_right_inj; //;
2248#b1;#delta;#chunk;#ofs;#H; nwhd in H:(??%?); ndestruct;
2249napply nmk; *; #H1;#H2;#H3;#H4;
2250(* arith H2 and H3 contradict Hbounds. *) napply daemon;
2251nqed.
2252
2253nlemma valid_block_lessdef:
2254  ∀m1,m2,b. lessdef m1 m2 → valid_block m1 b → valid_block m2 b.
2255#m1;#m2;#b;*;#Hnext;#Hinj;
2256 nrewrite > (unfold_valid_block …); nrewrite > (unfold_valid_block m2 b);
2257 //; nqed.
2258
2259nlemma valid_pointer_lessdef:
2260  ∀m1,m2,b,ofs.
2261  lessdef m1 m2 → valid_pointer m1 b ofs = true → valid_pointer m2 b ofs = true.
2262#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
2263nrewrite < (Zplus_z_OZ ofs); napply (valid_pointer_inj … Hinj VALID); //;
2264nqed.
2265
2266
2267(* ** Memory injections *)
2268
2269(* A memory injection [f] is a function from addresses to either [None]
2270  or [Some] of an address and an offset.  It defines a correspondence
2271  between the blocks of two memory states [m1] and [m2]:
2272- if [f b = None], the block [b] of [m1] has no equivalent in [m2];
2273- if [f b = Some〈b', ofs〉], the block [b] of [m2] corresponds to
2274  a sub-block at offset [ofs] of the block [b'] in [m2].
2275*)
2276
2277(* A memory injection defines a relation between values that is the
2278  identity relation, except for pointer values which are shifted
2279  as prescribed by the memory injection. *)
2280
2281ninductive val_inject (mi: meminj): val → val → Prop :=
2282  | val_inject_int:
2283      ∀i. val_inject mi (Vint i) (Vint i)
2284  | val_inject_float:
2285      ∀f. val_inject mi (Vfloat f) (Vfloat f)
2286  | val_inject_ptr:
2287      ∀b1,ofs1,b2,ofs2,x.
2288      mi b1 = Some ? 〈b2, x〉 →
2289      ofs2 = add ofs1 (repr x) →
2290      val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)
2291  | val_inject_undef: ∀v.
2292      val_inject mi Vundef v.
2293(*
2294Hint Resolve val_inject_int val_inject_float val_inject_ptr
2295             val_inject_undef.
2296*)
2297ninductive val_list_inject (mi: meminj): list val → list val→ Prop:=
2298  | val_nil_inject :
2299      val_list_inject mi (nil ?) (nil ?)
2300  | val_cons_inject : ∀v,v',vl,vl'.
2301      val_inject mi v v' → val_list_inject mi vl vl'→
2302      val_list_inject mi (v :: vl) (v' :: vl'). 
2303(*
2304Hint Resolve val_nil_inject val_cons_inject.
2305*)
2306(* A memory state [m1] injects into another memory state [m2] via the
2307  memory injection [f] if the following conditions hold:
2308- loads in [m1] must have matching loads in [m2] in the sense
2309  of the [mem_inj] predicate;
2310- unallocated blocks in [m1] must be mapped to [None] by [f];
2311- if [f b = Some〈b', delta〉], [b'] must be valid in [m2];
2312- distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2];
2313- the sizes of [m2]'s blocks are representable with signed machine integers;
2314- the offsets [delta] are representable with signed machine integers.
2315*)
2316
2317nrecord mem_inject (f: meminj) (m1,m2: mem) : Prop ≝
2318  {
2319    mi_inj:
2320      mem_inj val_inject f m1 m2;
2321    mi_freeblocks:
2322      ∀b. ¬(valid_block m1 b) → f b = None ?;
2323    mi_mappedblocks:
2324      ∀b,b',delta. f b = Some ? 〈b', delta〉 → valid_block m2 b';
2325    mi_no_overlap:
2326      meminj_no_overlap f m1;
2327    mi_range_1:
2328      ∀b,b',delta.
2329      f b = Some ? 〈b', delta〉 →
2330      min_signed ≤ delta ∧ delta ≤ max_signed;
2331    mi_range_2:
2332      ∀b,b',delta.
2333      f b = Some ? 〈b', delta〉 →
2334      delta = 0 ∨ (min_signed ≤ low_bound m2 b' ∧ high_bound m2 b' ≤ max_signed)
2335  }.
2336
2337
2338(* The following lemmas establish the absence of machine integer overflow
2339  during address computations. *)
2340
2341nlemma address_inject:
2342  ∀f,m1,m2,chunk,b1,ofs1,b2,delta.
2343  mem_inject f m1 m2 →
2344  valid_access m1 chunk b1 (signed ofs1) →
2345  f b1 = Some ? 〈b2, delta〉 →
2346  signed (add ofs1 (repr delta)) = signed ofs1 + delta.
2347#f;#m1;#m2;#chunk;#b1;#ofs1;#b2;#delta;
2348*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2349#Hvalid;#Hb1inj;
2350nelim (mi_range_2 ??? Hb1inj);
2351##[ (* delta = 0 *)
2352    #edelta; nrewrite > edelta;
2353    nrewrite > (?:repr O = zero); ##[ ##2: // ##]
2354    nrewrite > (add_zero ?);
2355    //;
2356##| (* delta ≠ 0 *)
2357    #Hrange; nrewrite > (add_signed ??);
2358    nrewrite > (signed_repr delta ?);
2359    ##[ nrewrite > (signed_repr ??);
2360      ##[ //
2361      ##| ncut (valid_access m2 chunk b2 (signed ofs1 + delta));
2362        ##[ napply (valid_access_inj … Hvalid); //;
2363        ##| *; #_; #Hlo; #Hhi; #_; (* arith *) napply daemon
2364        ##]
2365      ##]
2366    ##| /2/
2367    ##]
2368##] nqed.
2369
2370nlemma valid_pointer_inject_no_overflow:
2371  ∀f,m1,m2,b,ofs,b',x.
2372  mem_inject f m1 m2 →
2373  valid_pointer m1 b (signed ofs) = true →
2374  f b = Some ? 〈b', x〉 →
2375  min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed.
2376#f;#m1;#m2;#b;#ofs;#b';#x;
2377*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2378#Hvalid;#Hb1inj;
2379nlapply ((proj1 ?? (valid_pointer_valid_access ???)) Hvalid); #Hvalid';
2380ncut (valid_access m2 Mint8unsigned b' (signed ofs + x));
2381##[ napply (valid_access_inj … Hvalid'); // ##]
2382*; nrewrite > (?:size_chunk Mint8unsigned = 1); ##[ ##2: // ##] #_; #Hlo; #Hhi; #_;
2383nrewrite > (signed_repr ??); ##[ ##2: /2/; ##]
2384nlapply (mi_range_2 … Hb1inj); *;
2385##[ #ex; nrewrite > ex; nrewrite > (Zplus_z_OZ ?); napply signed_range;
2386##| (* arith *) napply daemon
2387##] nqed.
2388
2389nlemma valid_pointer_inject:
2390  ∀f,m1,m2,b,ofs,b',ofs'.
2391  mem_inject f m1 m2 →
2392  valid_pointer m1 b (signed ofs) = true →
2393  val_inject f (Vptr b ofs) (Vptr b' ofs') →
2394  valid_pointer m2 b' (signed ofs') = true.
2395#f;#m1;#m2;#b;#ofs;#b';#ofs';
2396#Hinj; #Hvalid; #Hvinj; ninversion Hvinj;
2397##[ ##1,2,4: #x;#H;ndestruct; ##]
2398#b0;#i;#b0';#i';#delta;#Hb;#Hi';#eptr;#eptr';
2399(* FIXME want ndestruct to sort this out, but get assertion failure *)
2400  nrewrite > (?:b0 = b) in Hb; ##[ ##2: ndestruct; // ##]
2401  nrewrite > (?:b0' = b'); ##[ ##2: ndestruct; // ##]
2402  nrewrite > (?:i = ofs) in Hi'; ##[ ##2: ndestruct; // ##]
2403  nrewrite > (?:i' = ofs'); ##[ ##2: ndestruct; // ##]
2404  #Hofs; #Hbinj;
2405nrewrite > Hofs;
2406nlapply (valid_pointer_inject_no_overflow … Hinj Hvalid Hbinj); #NOOV;
2407nelim Hinj;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2408nrewrite > (add_signed ??); nrewrite > (signed_repr ??); //;
2409nrewrite > (signed_repr ??); /2/;
2410napply (valid_pointer_inj … mi_inj Hvalid); //;
2411nqed.
2412
2413nlemma different_pointers_inject:
2414  ∀f,m,m',b1,ofs1,b2,ofs2,b1',delta1,b2',delta2.
2415  mem_inject f m m' →
2416  b1 ≠ b2 →
2417  valid_pointer m b1 (signed ofs1) = true →
2418  valid_pointer m b2 (signed ofs2) = true →
2419  f b1 = Some ? 〈b1', delta1〉 →
2420  f b2 = Some ? 〈b2', delta2〉 →
2421  b1' ≠ b2' ∨
2422  signed (add ofs1 (repr delta1)) ≠
2423  signed (add ofs2 (repr delta2)).
2424#f;#m;#m';#b1;#ofs1;#b2;#ofs2;#b1';#delta1;#b2';#delta2;
2425#Hinj;#neb;#Hval1;#Hval2;#Hf1;#Hf2;
2426nlapply ((proj1 ?? (valid_pointer_valid_access …)) Hval1); #Hval1';
2427nlapply ((proj1 ?? (valid_pointer_valid_access …)) Hval2); #Hval2';
2428nrewrite > (address_inject … Hinj Hval1' Hf1);
2429nrewrite > (address_inject … Hinj Hval2' Hf2);
2430nelim Hval1'; #Hbval; #Hlo; #Hhi;#Hal; nwhd in Hhi:(?(??%)?);
2431nelim Hval2'; #Hbval2; #Hlo2; #Hhi2;#Hal2; nwhd in Hhi2:(?(??%)?);
2432nlapply (mi_no_overlap ??? Hinj … Hf1 Hf2 …); //;
2433*; ##[
2434*; ##[
2435*; ##[ /2/;
2436   ##| (* arith contradiction *) napply daemon ##]
2437   ##| (* arith contradiction *) napply daemon ##]
2438   ##| *; ##[ #H;@2; (* arith *) napply daemon
2439          ##| #H;@2; (* arith *) napply daemon  ##] ##]
2440nqed.
2441
2442(* Relation between injections and loads. *)
2443
2444nlemma load_inject:
2445  ∀f,m1,m2,chunk,b1,ofs,b2,delta,v1.
2446  mem_inject f m1 m2 →
2447  load chunk m1 b1 ofs = Some ? v1 →
2448  f b1 = Some ? 〈b2, delta〉 →
2449  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inject f v1 v2.
2450#f;#m1;#m2;#chunk;#b1;#ofs;#b2;#delta;#v1;
2451*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2452#LOAD;#Hbinj;
2453napply mi_inj; //;
2454nqed.
2455
2456nlemma loadv_inject:
2457  ∀f,m1,m2,chunk,a1,a2,v1.
2458  mem_inject f m1 m2 →
2459  loadv chunk m1 a1 = Some ? v1 →
2460  val_inject f a1 a2 →
2461  ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_inject f v1 v2.
2462#f;#m1;#m2;#chunk;#a1;#a2;#v1;
2463#Hinj;#LOADV;#Hvinj; ninversion Hvinj;
2464##[ ##1,2,4: #x;#ex;#ex'; napply False_ind; ndestruct; ##]
2465#b;#ofs;#b';#ofs';#delta;#Hbinj;#Hofs;#ea1;#ea2;
2466nrewrite > ea1 in LOADV; #LOADV;
2467nlapply (load_inject … Hinj LOADV … Hbinj); *; #v2; *; #LOAD; #INJ;
2468@ v2; @; //; nrewrite > Hofs;
2469nrewrite < (?:signed (add ofs (repr delta)) = signed ofs + delta) in LOAD;
2470##[ #H; napply H; (* XXX: used to work with /2/ *)
2471##| napply (address_inject … chunk … Hinj ? Hbinj); napply (load_valid_access …);
2472    ##[ ##2: napply LOADV; ##]
2473##] nqed.
2474
2475(* Relation between injections and stores. *)
2476
2477ninductive val_content_inject (f: meminj): memory_chunk → val → val → Prop ≝
2478  | val_content_inject_base:
2479      ∀chunk,v1,v2.
2480      val_inject f v1 v2 →
2481      val_content_inject f chunk v1 v2
2482  | val_content_inject_8:
2483      ∀chunk,n1,n2.
2484      chunk = Mint8unsigned ∨ chunk = Mint8signed →
2485      zero_ext 8 n1 = zero_ext 8 n2 →
2486      val_content_inject f chunk (Vint n1) (Vint n2)
2487  | val_content_inject_16:
2488      ∀chunk,n1,n2.
2489      chunk = Mint16unsigned ∨ chunk = Mint16signed →
2490      zero_ext 16 n1 = zero_ext 16 n2 →
2491      val_content_inject f chunk (Vint n1) (Vint n2)
2492  | val_content_inject_32:
2493      ∀f1,f2.
2494      singleoffloat f1 = singleoffloat f2 →
2495      val_content_inject f Mfloat32 (Vfloat f1) (Vfloat f2).
2496
2497(*Hint Resolve val_content_inject_base.*)
2498
2499nlemma load_result_inject:
2500  ∀f,chunk,v1,v2,chunk'.
2501  val_content_inject f chunk v1 v2 →
2502  size_chunk chunk = size_chunk chunk' →
2503  val_inject f (load_result chunk' v1) (load_result chunk' v2).
2504#f;#chunk;#v1;#v2;#chunk';
2505#Hvci; ninversion Hvci;
2506##[ #chunk'';#v1';#v2';#Hvinj;#_;#_;#_;#Hsize; ninversion Hvinj;
2507  ##[ ncases chunk'; #i;#_;#_; ##[ ##1,2,3,4,5: @ ##| ##6,7: @4 ##]
2508  ##| ncases chunk'; #f;#_;#_; ##[ ##1,2,3,4,5: @4 ##| ##6,7: @2 ##]
2509  ##| ncases chunk'; #b1;#ofs1;#b2;#ofs2;#delta;#Hmap;#Hofs;#_;#_; ##[ ##5: @3; // ##| ##*: @4 ##]
2510  ##| ncases chunk'; #v;#_;#_; @4;
2511  ##]
2512(* FIXME: the next two cases are the same *)
2513##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
2514    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
2515    ##[ ##2,4: nrewrite > Hz; @
2516    ##| ##1,3: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize;
2517        ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##]
2518    ##]
2519
2520##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
2521    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
2522    ##[ ##2,4: nrewrite > Hz; @
2523    ##| ##1,3: nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize;
2524        ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##]
2525    ##]
2526
2527##| #f;#f';#float;#echunk;nrewrite > echunk;#_;#_;
2528    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
2529    ##[ @4; ##| nrewrite > float; @2 ##]
2530##] nqed.
2531
2532nlemma store_mapped_inject_1 :
2533  ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2.
2534  mem_inject f m1 m2 →
2535  store chunk m1 b1 ofs v1 = Some ? n1 →
2536  f b1 = Some ? 〈b2, delta〉 →
2537  val_content_inject f chunk v1 v2 →
2538  ∃n2.
2539    store chunk m2 b2 (ofs + delta) v2 = Some ? n2
2540    ∧ mem_inject f n1 n2.
2541#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;#b2;#delta;#v2;
2542*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2543#STORE1; #INJb1; #Hvcinj;
2544nlapply (store_mapped_inj … mi_inj mi_no_overlap INJb1 STORE1 ?); //;
2545##[ #chunk';#Hchunksize;napply (load_result_inject … chunk …);//;
2546##| ##skip ##]
2547*;#n2;*;#STORE;#MINJ;
2548@ n2; @; //; @;
2549##[ (* inj *) //
2550##| (* freeblocks *) #b;#notvalid; napply mi_freeblocks;
2551    napply (not_to_not ??? notvalid); napply (store_valid_block_1 … STORE1);
2552##| (* mappedblocks *) #b;#b';#delta';#INJb';napply (store_valid_block_1 … STORE);
2553    /2/;
2554##| (* no_overlap *) nwhd; #b1';#b1'';#delta1';#b2';#b2'';#delta2';#neqb';
2555    #fb1';#fb2';
2556    nrewrite > (low_bound_store … STORE1 ?);  nrewrite > (low_bound_store … STORE1 ?);
2557    nrewrite > (high_bound_store … STORE1 ?);  nrewrite > (high_bound_store … STORE1 ?);
2558    napply mi_no_overlap; //;
2559##| (* range *) /2/;
2560##| (* range 2 *) #b;#b';#delta';#INJb;
2561    nrewrite > (low_bound_store … STORE ?);
2562    nrewrite > (high_bound_store … STORE ?);
2563    napply mi_range_2; //;
2564##] nqed.
2565
2566nlemma store_mapped_inject:
2567  ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2.
2568  mem_inject f m1 m2 →
2569  store chunk m1 b1 ofs v1 = Some ? n1 →
2570  f b1 = Some ? 〈b2, delta〉 →
2571  val_inject f v1 v2 →
2572  ∃n2.
2573    store chunk m2 b2 (ofs + delta) v2 = Some ? n2
2574    ∧ mem_inject f n1 n2.
2575#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;#b2;#delta;#v2;
2576#MINJ;#STORE;#INJb1;#Hvalinj;napply (store_mapped_inject_1 … STORE);//;
2577napply val_content_inject_base;//;
2578nqed.
2579
2580nlemma store_unmapped_inject:
2581  ∀f,chunk,m1,b1,ofs,v1,n1,m2.
2582  mem_inject f m1 m2 →
2583  store chunk m1 b1 ofs v1 = Some ? n1 →
2584  f b1 = None ? →
2585  mem_inject f n1 m2.
2586#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;
2587*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2588#STORE;#INJb1;@;
2589##[ (* inj *) napply (store_unmapped_inj … STORE); //
2590##| (* freeblocks *) #b;#notvalid; napply mi_freeblocks;
2591    napply (not_to_not ??? notvalid); napply (store_valid_block_1 … STORE);
2592##| (* mappedblocks *) #b;#b';#delta;#INJb; napply mi_mappedblock; //;
2593##| (* no_overlap *) nwhd; #b1';#b1'';#delta1';#b2';#b2'';#delta2';#neqb';
2594    #fb1';#fb2';
2595    nrewrite > (low_bound_store … STORE ?);  nrewrite > (low_bound_store … STORE ?);
2596    nrewrite > (high_bound_store … STORE ?);  nrewrite > (high_bound_store … STORE ?);
2597    napply mi_no_overlap; //;
2598##| (* range *) /2/
2599##| /2/
2600##] nqed.
2601
2602nlemma storev_mapped_inject_1:
2603  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
2604  mem_inject f m1 m2 →
2605  storev chunk m1 a1 v1 = Some ? n1 →
2606  val_inject f a1 a2 →
2607  val_content_inject f chunk v1 v2 →
2608  ∃n2.
2609    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2.
2610#f;#chunk;#m1;#a1;#v1;#n1;#m2;#a2;#v2;
2611#MINJ;#STORE;#Hvinj;#Hvcinj;
2612ninversion Hvinj;
2613##[ ##1,2,4:#x;#ex1;#ex2;nrewrite > ex1 in STORE; nwhd in ⊢ ((??%?)→?); #H;
2614    napply False_ind; ndestruct; ##]
2615#b;#ofs;#b';#ofs';#delta;#INJb;#Hofs;#ea1;#ea2;
2616nrewrite > Hofs; nrewrite > ea1 in STORE; #STORE;
2617nlapply (store_mapped_inject_1 … MINJ STORE … INJb Hvcinj);
2618nrewrite < (?:signed (add ofs (repr delta)) = signed ofs + delta); //;
2619napply (address_inject … chunk … MINJ ? INJb);
2620napply (store_valid_access_3 … STORE);
2621nqed.
2622
2623nlemma storev_mapped_inject:
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_inject f 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; #MINJ;#STOREV;#Hvinj;#Hvinj';
2632napply (storev_mapped_inject_1 … STOREV); /2/;
2633nqed.
2634
2635(* Relation between injections and [free] *)
2636
2637nlemma meminj_no_overlap_free:
2638  ∀mi,m,b.
2639  meminj_no_overlap mi m →
2640  meminj_no_overlap mi (free m b).
2641#mi;#m;#b;#H;nwhd;#b1;#b1';#delta1;#b2;#b2';#delta2;#Hne;#mi1;#mi2;
2642ncut (low_bound (free m b) b ≥ high_bound (free m b) b);
2643##[ nrewrite > (low_bound_free_same …); nrewrite > (high_bound_free_same …);// ##]
2644#Hbounds;
2645ncases (decidable_eq_Z b1 b);#e1; ##[ nrewrite > e1 in Hne mi1 ⊢ %;#Hne;#mi1;##]
2646ncases (decidable_eq_Z b2 b);#e2; ##[ ##1,3: nrewrite > e2 in Hne mi2 ⊢ %;#Hne;#mi2;##]
2647##[ napply False_ind; nelim Hne; /2/
2648##| @;@2;//;
2649##| @;@;@2;//
2650##| nrewrite > (low_bound_free …);//; nrewrite > (low_bound_free …);//;
2651    nrewrite > (high_bound_free …);//; nrewrite > (high_bound_free …);//;
2652    /2/;
2653##] nqed.
2654
2655nlemma meminj_no_overlap_free_list:
2656  ∀mi,m,bl.
2657  meminj_no_overlap mi m →
2658  meminj_no_overlap mi (free_list m bl).
2659#mi;#m;#bl; nelim bl;
2660##[ #H; nwhd in ⊢ (??%); //
2661##| #h;#t; #IH; #H; napply meminj_no_overlap_free; napply IH; //
2662##] nqed.
2663
2664nlemma free_inject:
2665  ∀f,m1,m2,l,b.
2666  (∀b1,delta. f b1 = Some ? 〈b, delta〉 → in_list ? b1 l) →
2667  mem_inject f m1 m2 →
2668  mem_inject f (free_list m1 l) (free m2 b).
2669#f;#m1;#m2;#l;#b;#mappedin;
2670*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2671@;
2672##[ (* inj *)
2673    napply free_right_inj; ##[ napply free_list_left_inj; //; ##]
2674    #b1;#delta;#chunk;#ofs;#INJb1; napply nmk; #Hvalid;
2675    nelim (valid_access_free_list_inv … Hvalid); #b1ni; #Haccess;
2676    napply (absurd ? (mappedin ?? INJb1) b1ni);
2677##| (* freeblocks *)
2678    #b';#notvalid; napply mi_freeblocks; napply (not_to_not ??? notvalid);
2679    #H; napply valid_block_free_list_1; //
2680##| (* mappedblocks *)
2681    #b1;#b1';#delta;#INJb1; napply valid_block_free_1; /2/
2682##| (* overlap *)
2683    napply meminj_no_overlap_free_list; //
2684##| (* range *)
2685    /2/
2686##| #b1;#b2;#delta;#INJb1; ncases (decidable_eq_Z b2 b); #eb;
2687    ##[ nrewrite > eb;
2688        nrewrite > (low_bound_free_same ??); nrewrite > (high_bound_free_same ??);
2689        @2; (* arith *) napply daemon
2690    ##| nrewrite > (low_bound_free …); //; nrewrite > (high_bound_free …); /2/;
2691    ##]
2692##] nqed.
2693
2694(* Monotonicity properties of memory injections. *)
2695
2696ndefinition inject_incr : meminj → meminj → Prop ≝ λf1,f2.
2697  ∀b. f1 b = f2 b ∨ f1 b = None ?.
2698
2699nlemma inject_incr_refl :
2700   ∀f. inject_incr f f .
2701#f;nwhd;#b;@;//; nqed.
2702
2703nlemma inject_incr_trans :
2704  ∀f1,f2,f3.
2705  inject_incr f1 f2 → inject_incr f2 f3 → inject_incr f1 f3 .
2706#f1;#f2;#f3;nwhd in ⊢ (%→%→%);#H1;#H2;#b;
2707nelim (H1 b); nelim (H2 b); /2/; nqed.
2708
2709nlemma val_inject_incr:
2710  ∀f1,f2,v,v'.
2711  inject_incr f1 f2 →
2712  val_inject f1 v v' →
2713  val_inject f2 v v'.
2714#f1;#f2;#v;#v';#Hincr;#Hvinj;
2715ninversion Hvinj;
2716##[ ##1,2,4: #x;#_;#_; //;
2717##|#b;#ofs;#b';#ofs';#delta; #INJb; #Hofs; #_;#_;
2718nelim (Hincr b); #H;
2719##[ napply (val_inject_ptr ??????? Hofs); /2/;
2720##| napply False_ind; nrewrite > INJb in H; #H; ndestruct;
2721##] nqed.
2722
2723nlemma val_list_inject_incr:
2724  ∀f1,f2,vl,vl'.
2725  inject_incr f1 f2 → val_list_inject f1 vl vl' →
2726  val_list_inject f2 vl vl'.
2727#f1;#f2;#vl;nelim vl;
2728##[ #vl'; #Hincr; #H; ninversion H; //; #v;#v';#l;#l0;#_;#_;#_; #H; ndestruct;
2729##| #h;#t;#IH;#vl';#Hincr;#H1; ninversion H1;
2730  ##[ #H; ndestruct
2731  ##| #h';#h'';#t';#t''; #Hinj1; #Hintt; #_; #e1; #e2; ndestruct;
2732      @2;/2/; napply IH; //; napply Hincr;
2733  ##]
2734##] nqed.
2735
2736(*
2737Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.
2738*)
2739
2740(* Properties of injections and allocations. *)
2741
2742ndefinition extend_inject ≝
2743       λb: block. λx: option (block × Z). λf: meminj.
2744  λb': block. if eqZb b' b then x else f b'.
2745
2746nlemma extend_inject_incr:
2747  ∀f,b,x.
2748  f b = None ? →
2749  inject_incr f (extend_inject b x f).
2750#f;#b;#x;#INJb;nwhd;#b'; nwhd in ⊢ (?(???%)?);
2751napply (eqZb_elim b' b); #eb; /2/;
2752nqed.
2753
2754nlemma alloc_right_inject:
2755  ∀f,m1,m2,lo,hi,m2',b.
2756  mem_inject f m1 m2 →
2757  alloc m2 lo hi = 〈m2', b〉 →
2758  mem_inject f m1 m2'.
2759#f;#m1;#m2;#lo;#hi;#m2';#b;
2760*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2761#ALLOC; @;
2762##[ napply (alloc_right_inj … ALLOC); //;
2763##| /2/;
2764##| #b1;#b2;#delta;#INJb1; napply (valid_block_alloc … ALLOC); /2/;
2765##| //;
2766##| /2/;
2767##|#b1;#b2;#delta;#INJb1; nrewrite > (?:low_bound m2' b2 = low_bound m2 b2);
2768   ##[ nrewrite > (?:high_bound m2' b2 = high_bound m2 b2); /2/;
2769       napply high_bound_alloc_other; /2/;
2770   ##| napply low_bound_alloc_other; /2/
2771   ##]
2772##] nqed.
2773
2774nlemma alloc_unmapped_inject:
2775  ∀f,m1,m2,lo,hi,m1',b.
2776  mem_inject f m1 m2 →
2777  alloc m1 lo hi = 〈m1', b〉 →
2778  mem_inject (extend_inject b (None ?) f) m1' m2 ∧
2779  inject_incr f (extend_inject b (None ?) f).
2780#f;#m1;#m2;#lo;#hi;#m1';#b;
2781*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2782#ALLOC;
2783ncut (inject_incr f (extend_inject b (None ?) f));
2784##[ napply extend_inject_incr; napply mi_freeblocks; /2/; ##]
2785#Hinject_incr; @; //; @;
2786##[ (* inj *)
2787    napply (alloc_left_unmapped_inj … ALLOC);
2788    ##[ ##2: nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); /2/; ##]
2789    nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;
2790    nwhd in ⊢ ((??%?)→?→?); napply eqZb_elim; #e; nwhd in ⊢ ((??%?)→?→?);
2791    #Hextend;#LOAD;
2792    ##[ napply False_ind; (* XXX *) napply grumpydestruct; //;
2793    ##| nlapply (mi_inj … Hextend LOAD); *; #v2; *; #LOAD2; #VINJ;
2794    @ v2; @; //;
2795    napply val_inject_incr; //;
2796    ##]
2797##| (* freeblocks *)
2798    #b';#Hinvalid; nwhd in ⊢ (??%?); napply (eqZb_elim b' b); //;
2799    #neb; napply mi_freeblocks; napply (not_to_not ??? Hinvalid);
2800    napply valid_block_alloc; //;
2801##| (* mappedblocks *)
2802    #b1;#b2;#delta; nwhd in ⊢ (??%?→?); napply (eqZb_elim b1 b); #eb;
2803    ##[ #H; ndestruct;
2804    ##| #H; napply (mi_mappedblock … H);
2805    ##]
2806##| (* overlap *)
2807    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2; #neb1; nwhd in ⊢ (??%?→??%?→?);
2808    nrewrite > (low_bound_alloc … ALLOC ?); nrewrite > (low_bound_alloc … ALLOC ?);
2809    nrewrite > (high_bound_alloc … ALLOC ?); nrewrite > (high_bound_alloc … ALLOC ?);
2810    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2811    ##[ ndestruct
2812    ##| nlapply (eqZb_to_Prop b2 b); nelim (eqZb b2 b); #e2; #INJb2;
2813      ##[ ndestruct
2814      ##| napply mi_no_overlap; /2/;
2815      ##]
2816    ##]
2817##| (* range *)
2818    #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
2819    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2820    ##[ ndestruct
2821    ##| napply (mi_range_1 … INJb1);
2822    ##]
2823##| #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
2824    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2825    ##[  ndestruct
2826    ##| napply (mi_range_2 … INJb1);
2827    ##]
2828##] nqed.
2829
2830nlemma alloc_mapped_inject:
2831  ∀f,m1,m2,lo,hi,m1',b,b',ofs.
2832  mem_inject f m1 m2 →
2833  alloc m1 lo hi = 〈m1', b〉 →
2834  valid_block m2 b' →
2835  min_signed ≤ ofs ∧ ofs ≤ max_signed →
2836  min_signed ≤ low_bound m2 b' →
2837  high_bound m2 b' ≤ max_signed →
2838  low_bound m2 b' ≤ lo + ofs →
2839  hi + ofs ≤ high_bound m2 b' →
2840  inj_offset_aligned ofs (hi-lo) →
2841  (∀b0,ofs0.
2842   f b0 = Some ? 〈b', ofs0〉 →
2843   high_bound m1 b0 + ofs0 ≤ lo + ofs ∨
2844   hi + ofs ≤ low_bound m1 b0 + ofs0) →
2845  mem_inject (extend_inject b (Some ? 〈b', ofs〉) f) m1' m2 ∧
2846  inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f).
2847#f;#m1;#m2;#lo;#hi;#m1';#b;#b';#ofs;
2848*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2849#ALLOC;#validb';#rangeofs;#rangelo;#rangehi;#boundlo;#boundhi;#injaligned;#boundmapped;
2850ncut (inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f));
2851##[ napply extend_inject_incr; napply mi_freeblocks; /2/; ##]
2852#Hincr; @; //; @;
2853##[ (* inj *)
2854    napply (alloc_left_mapped_inj … ALLOC … validb' boundlo boundhi); /2/;
2855    ##[ ##2:nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); /2/; ##]
2856    nwhd; #chunk;#b1;#ofs';#v1;#b2;#delta;#Hextend;#LOAD;
2857    nwhd in Hextend:(??%?); nrewrite > (eqZb_false b1 b ?) in Hextend;
2858    ##[ #Hextend; nlapply (mi_inj … Hextend LOAD);
2859        *; #v2; *; #LOAD2; #VINJ;
2860    @ v2; @; //;
2861    napply val_inject_incr; //;
2862    ##| napply (valid_not_valid_diff m1); /2/;
2863        napply (valid_access_valid_block … chunk … ofs'); /2/;
2864    ##]
2865##| (* freeblocks *)
2866    #b';#Hinvalid; nwhd in ⊢ (??%?); nrewrite > (eqZb_false b' b ?);
2867    ##[ napply mi_freeblocks; napply (not_to_not ??? Hinvalid);
2868    napply valid_block_alloc; //;
2869    ##| napply sym_neq; napply (valid_not_valid_diff m1'); //;
2870        napply (valid_new_block … ALLOC);
2871    ##]
2872##| (* mappedblocks *)
2873    #b1;#b2;#delta; nwhd in ⊢ (??%?→?); napply (eqZb_elim b1 b); #eb;#einj;
2874    ##[ ndestruct; //;
2875    ##| napply (mi_mappedblock … einj);
2876    ##]
2877##| (* overlap *)
2878    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2; #neb1; nwhd in ⊢ (??%?→??%?→?);
2879    nrewrite > (low_bound_alloc … ALLOC ?); nrewrite > (low_bound_alloc … ALLOC ?);
2880    nrewrite > (high_bound_alloc … ALLOC ?); nrewrite > (high_bound_alloc … ALLOC ?);
2881    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2882    ##[ nelim (grumpydestruct2 ?????? INJb1); #eb1';#eofs1 ##]
2883    nlapply (eqZb_to_Prop b2 b); nelim (eqZb b2 b); #e2; #INJb2;
2884    ##[ nelim (grumpydestruct2 ?????? INJb2); #eb2';#eofs2 ##]
2885    ##[ napply False_ind; nrewrite > e in neb1; nrewrite > e2; /2/;
2886    ##| nelim (decidable_eq_Z b1' b2'); #e';
2887        ##[ nrewrite < e' in INJb2 ⊢ %; nrewrite < eb1'; nrewrite < eofs1; #INJb2; nlapply (boundmapped … INJb2);
2888            *; #H; @2; /2/;
2889        ##| @1;@1;@1; napply e'
2890        ##]
2891    ##| nelim (decidable_eq_Z b1' b2'); #e';
2892        ##[ nrewrite < e' in INJb2 ⊢ %; #INJb2; nelim (grumpydestruct2 ?????? INJb2); #eb'; #eofs; nrewrite < eb' in INJb1; nrewrite < eofs; #INJb1; nlapply (boundmapped … INJb1);
2893            *; #H; @2; /2/;
2894        ##| @1;@1;@1; napply e'
2895        ##]
2896    ##| napply mi_no_overlap; /2/;
2897    ##]
2898##| (* range *)
2899    #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
2900    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2901    ##[ ndestruct; /2/;
2902    ##| napply (mi_range_1 … INJb1);
2903    ##]
2904##| #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
2905    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2906    ##[ ndestruct; @2;@;/2/;
2907    ##| napply (mi_range_2 … INJb1);
2908    ##]
2909##] nqed.
2910
2911nlemma alloc_parallel_inject:
2912  ∀f,m1,m2,lo,hi,m1',m2',b1,b2.
2913  mem_inject f m1 m2 →
2914  alloc m1 lo hi = 〈m1', b1〉 →
2915  alloc m2 lo hi = 〈m2', b2〉 →
2916  min_signed ≤ lo → hi ≤ max_signed →
2917  mem_inject (extend_inject b1 (Some ? 〈b2, OZ〉) f) m1' m2' ∧
2918  inject_incr f (extend_inject b1 (Some ? 〈b2, OZ〉) f).
2919#f;#m1;#m2;#lo;#hi;#m1';#m2';#b1;#b2;
2920#Hminj;#ALLOC1;#ALLOC2;#Hlo;#Hhi;
2921napply (alloc_mapped_inject … ALLOC1); /2/;
2922##[ nlapply (alloc_right_inject … Hminj ALLOC2); //;
2923##| (* TODO: add to integers *) napply daemon
2924##| nrewrite > (low_bound_alloc_same … ALLOC2); //
2925##| nrewrite > (high_bound_alloc_same … ALLOC2); //
2926##| nrewrite > (low_bound_alloc_same … ALLOC2); //
2927##| nrewrite > (high_bound_alloc_same … ALLOC2); //
2928##| nwhd; (* arith *) napply daemon
2929##| #b;#ofs;#INJb0; napply False_ind;
2930    nelim Hminj;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2931    nlapply (mi_mappedblock … INJb0);
2932    #H; napply (absurd ? H ?); /2/;
2933##] nqed.
2934
2935ndefinition meminj_init ≝ λm: mem.
2936  λb: block. if Zltb b (nextblock m) then Some ? 〈b, OZ〉 else None ?.
2937
2938ndefinition mem_inject_neutral ≝ λm: mem.
2939  ∀f,chunk,b,ofs,v.
2940  load chunk m b ofs = Some ? v → val_inject f v v.
2941
2942nlemma init_inject:
2943  ∀m.
2944  mem_inject_neutral m →
2945  mem_inject (meminj_init m) m m.
2946#m;#neutral;@;
2947##[ (* inj *)
2948    nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta; nwhd in ⊢ (??%?→?→?);
2949    napply Zltb_elim_Type0; #ltb1; ##[
2950    #H; nelim (grumpydestruct2 ?????? H); #eb1; #edelta;
2951    nrewrite < eb1; nrewrite < edelta; #LOAD; @v1; @; //;
2952    napply neutral; //;
2953    ##| #H;nwhd in H:(??%?); ndestruct;
2954    ##]
2955##| (* free blocks *)
2956    #b;nrewrite > (unfold_valid_block …); nwhd in ⊢ (?→??%?); #notvalid;
2957    napply Zltb_elim_Type0; #ltb1;
2958    ##[ napply False_ind; napply (absurd ? ltb1 notvalid)
2959    ##| //
2960    ##]
2961##| (* mapped blocks *)
2962    #b;#b';#delta;nwhd in ⊢ (??%?→?); nrewrite > (unfold_valid_block …);
2963    napply Zltb_elim_Type0; #ltb;
2964    #H; nwhd in H:(??%?); ndestruct; //
2965##| (* overlap *)
2966    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neb1; nwhd in ⊢(??%?→??%?→?);
2967    napply Zltb_elim_Type0; #ltb1;
2968    ##[ #H; nwhd in H:(??%?); ndestruct;
2969        napply Zltb_elim_Type0; #ltb2;
2970        #H2; nwhd in H2:(??%?); ndestruct; @;@;@;/2/;
2971    ##| #H; nwhd in H:(??%?); ndestruct;
2972    ##]
2973##| (* range *)
2974    #b;#b';#delta;nwhd in ⊢ (??%?→?);
2975    napply Zltb_elim_Type0; #ltb;
2976    ##[ #H; nelim (grumpydestruct2 ?????? H); #eb; #edelta; nrewrite < edelta;
2977        (* FIXME: should be in integers.ma *) napply daemon
2978    ##| #H; nwhd in H:(??%?); ndestruct;
2979    ##]
2980##| (* range *)
2981    #b;#b';#delta;nwhd in ⊢ (??%?→?);
2982    napply Zltb_elim_Type0; #ltb;
2983    ##[ #H; nelim (grumpydestruct2 ?????? H); #eb; #edelta; nrewrite < edelta;
2984        (* FIXME: should be in integers.ma *) napply daemon
2985    ##| #H; nwhd in H:(??%?); ndestruct;
2986    ##]
2987##] nqed.
2988
2989nremark getN_setN_inject:
2990  ∀f,m,v,n1,p1,n2,p2.
2991  val_inject f (getN n2 p2 m) (getN n2 p2 m) →
2992  val_inject f v v →
2993  val_inject f (getN n2 p2 (setN n1 p1 v m))
2994               (getN n2 p2 (setN n1 p1 v m)).
2995#f;#m;#v;#n1;#p1;#n2;#p2;#injget;#injv;
2996ncases (getN_setN_characterization m v n1 p1 n2 p2);##[ * ##] #A;
2997nrewrite > A; //;
2998nqed.
2999             
3000nremark getN_contents_init_data_inject:
3001  ∀f,n,ofs,id,pos.
3002  val_inject f (getN n ofs (contents_init_data pos id))
3003               (getN n ofs (contents_init_data pos id)).
3004#f;#n;#ofs;#id;nelim id;
3005##[ #pos; nrewrite > (getN_init …); //
3006##| #h;#t;#IH;#pos; ncases h;
3007##[ ##1,2,3,4,5: #x; napply getN_setN_inject; //
3008##| ##6,8: #x; napply IH ##| #x;#y;napply IH ##] (* XXX // doesn't work? *)
3009nqed.
3010
3011nlemma alloc_init_data_neutral:
3012  ∀m,id,m',b.
3013  mem_inject_neutral m →
3014  alloc_init_data m id = 〈m', b〉 →
3015  mem_inject_neutral m'.
3016#m;#id;#m';#b;#Hneutral;#INIT; nwhd in INIT:(??%?); (* XXX: ndestruct too long*)
3017napply (pairdisc_elim … INIT);
3018nwhd in ⊢ (??%% → ?);#B;nrewrite < B in ⊢ (??%% → ?);
3019nwhd in ⊢ (??%% → ?);#A;
3020nwhd; #f;#chunk;#b';#ofs;#v; #LOAD;
3021nlapply (load_inv … LOAD); *; #C; #D;
3022nrewrite < B in D; nrewrite > A;
3023nrewrite > (unfold_update block_contents …); napply eqZb_elim;
3024##[ #eb'; #D; nwhd in D:(???(??(???%))); nrewrite > D;
3025    napply (load_result_inject … chunk); //; @;
3026    napply getN_contents_init_data_inject;
3027##| #neb'; #D; napply (Hneutral ? chunk b' ofs ??); nwhd in ⊢ (??%?);
3028    nrewrite > (in_bounds_true m chunk b' ofs (option ?) …);
3029    ##[ nrewrite < D; //
3030    ##| nelim C; #Cval;#Clo;#Chi;#Cal; @;
3031    ##[ nrewrite > (unfold_valid_block …);
3032        nrewrite > (unfold_valid_block …) in Cval; nrewrite < B;
3033        (* arith using neb' *) napply daemon
3034    ##| nrewrite > (?:low_bound m b' = low_bound m' b'); //;
3035        nwhd in ⊢ (??%%); nrewrite < B; nrewrite > A;
3036        nrewrite > (update_o block_contents …); //; napply sym_neq; //;
3037    ##| nrewrite > (?:high_bound m b' = high_bound m' b'); //;
3038        nwhd in ⊢ (??%%); nrewrite < B; nrewrite > A;
3039        nrewrite > (update_o block_contents …); //; napply sym_neq; //;
3040    ##| //;
3041    ##]
3042##] nqed.
3043
3044
3045(* ** Memory shifting *)
3046
3047(* A special case of memory injection where blocks are not coalesced:
3048  each source block injects in a distinct target block. *)
3049
3050ndefinition memshift ≝ block → option Z.
3051
3052ndefinition meminj_of_shift : memshift → meminj ≝ λmi: memshift.
3053  λb. match mi b with [ None ⇒ None ? | Some x ⇒ Some ? 〈b, x〉 ].
3054
3055ndefinition val_shift ≝ λmi: memshift. λv1,v2: val.
3056  val_inject (meminj_of_shift mi) v1 v2.
3057
3058nrecord mem_shift (f: memshift) (m1,m2: mem) : Prop :=
3059  {
3060    ms_inj:
3061      mem_inj val_inject (meminj_of_shift f) m1 m2;
3062    ms_samedomain:
3063      nextblock m1 = nextblock m2;
3064    ms_domain:
3065      ∀b. match f b with [ Some _ ⇒ b < nextblock m1 | None ⇒ b ≥ nextblock m1 ];
3066    ms_range_1:
3067      ∀b,delta.
3068      f b = Some ? delta →
3069      min_signed ≤ delta ∧ delta ≤ max_signed;
3070    ms_range_2:
3071      ∀b,delta.
3072      f b = Some ? delta →
3073      min_signed ≤ low_bound m2 b ∧ high_bound m2 b ≤ max_signed
3074  }.
3075
3076(* * The following lemmas establish the absence of machine integer overflow
3077  during address computations. *)
3078
3079nlemma address_shift:
3080  ∀f,m1,m2,chunk,b,ofs1,delta.
3081  mem_shift f m1 m2 →
3082  valid_access m1 chunk b (signed ofs1) →
3083  f b = Some ? delta →
3084  signed (add ofs1 (repr delta)) = signed ofs1 + delta.
3085#f;#m1;#m2;#chunk;#b;#ofs1;#delta;
3086*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;#Hvalid_access;#INJb;
3087nelim (ms_range_2 … INJb); #Hlo;#Hhi;
3088nrewrite > (add_signed …);
3089nrewrite > (signed_repr …); nrewrite > (signed_repr …); /2/;
3090ncut (valid_access m2 chunk b (signed ofs1 + delta));
3091##[ napply (valid_access_inj ? (meminj_of_shift f) … ms_inj Hvalid_access);
3092    nwhd in ⊢ (??%?); nrewrite > INJb; // ##]
3093*; (* arith *) napply daemon;
3094nqed.
3095
3096nlemma valid_pointer_shift_no_overflow:
3097  ∀f,m1,m2,b,ofs,x.
3098  mem_shift f m1 m2 →
3099  valid_pointer m1 b (signed ofs) = true →
3100  f b = Some ? x →
3101  min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed.
3102#f;#m1;#m2;#b;#ofs;#x;
3103*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3104#VALID;#INJb;
3105nlapply (proj1 ?? (valid_pointer_valid_access …) VALID); #Hvalid_access;
3106ncut (valid_access m2 Mint8unsigned b (signed ofs + x));
3107##[ napply (valid_access_inj … ms_inj Hvalid_access);
3108    nwhd in ⊢ (??%?); nrewrite > INJb; // ##]
3109*;#Hvalid_block;#Hlo;#Hhi;#Hal; nwhd in Hhi:(?(??%)?);
3110nrewrite > (signed_repr …); /2/;
3111nlapply (ms_range_2 … INJb);*;#A;#B;
3112(* arith *) napply daemon;
3113nqed.
3114
3115(* FIXME to get around ndestruct problems *)
3116nlemma vptr_eq_1 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → b = b'.
3117#b;#b';#ofs;#ofs';#H;ndestruct;//;
3118nqed.
3119nlemma vptr_eq_2 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → ofs = ofs'.
3120#b;#b';#ofs;#ofs';#H;ndestruct;//;
3121nqed.
3122
3123nlemma valid_pointer_shift:
3124  ∀f,m1,m2,b,ofs,b',ofs'.
3125  mem_shift f m1 m2 →
3126  valid_pointer m1 b (signed ofs) = true →
3127  val_shift f (Vptr b ofs) (Vptr b' ofs') →
3128  valid_pointer m2 b' (signed ofs') = true.
3129#f;#m1;#m2;#b;#ofs;#b';#ofs';#Hmem_shift;#VALID;#Hval_shift;
3130nwhd in Hval_shift; ninversion Hval_shift;
3131##[ ##1,2,4: #a; #H; ndestruct; ##]
3132#b1;#ofs1;#b2;#ofs2;#delta;#INJb1;#Hofs;#eb1;#eb2;
3133nrewrite < (vptr_eq_1 … eb1) in INJb1; nrewrite < (vptr_eq_1 … eb2); #INJb';
3134nrewrite < (vptr_eq_2 … eb1) in Hofs; nrewrite < (vptr_eq_2 … eb2); #Hofs; nrewrite > Hofs;
3135ncut (f b = Some ? delta);
3136##[ nwhd in INJb':(??%?); ncases (f b) in INJb' ⊢ %;
3137  ##[ #H; ndestruct; ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##]
3138##] #INJb;
3139nlapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV;
3140nelim Hmem_shift;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3141nrewrite > (add_signed …); nrewrite > (signed_repr …); //;
3142nrewrite > (signed_repr …); /2/;
3143napply (valid_pointer_inj … VALID); /2/;
3144nqed.
3145
3146(* Relation between shifts and loads. *)
3147
3148nlemma load_shift:
3149  ∀f,m1,m2,chunk,b,ofs,delta,v1.
3150  mem_shift f m1 m2 →
3151  load chunk m1 b ofs = Some ? v1 →
3152  f b = Some ? delta →
3153  ∃v2. load chunk m2 b (ofs + delta) = Some ? v2 ∧ val_shift f v1 v2.
3154#f;#m1;#m2;#chunk;#b;#ofs;#delta;#v1;
3155*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3156#LOAD; #INJb;
3157nwhd in ⊢ (??(λ_.??%)); napply (ms_inj … LOAD);
3158nwhd in ⊢ (??%?); nrewrite > INJb; //;
3159nqed.
3160
3161nlemma loadv_shift:
3162  ∀f,m1,m2,chunk,a1,a2,v1.
3163  mem_shift f m1 m2 →
3164  loadv chunk m1 a1 = Some ? v1 →
3165  val_shift f a1 a2 →
3166  ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_shift f v1 v2.
3167#f;#m1;#m2;#chunk;#a1;#a2;#v1;#Hmem_shift;#LOADV;#Hval_shift;
3168ninversion Hval_shift;
3169##[ ##1,2,4: #x;#H;nrewrite > H in LOADV;#H';nwhd in H':(??%?);napply False_ind; ndestruct; ##]
3170#b1;#ofs1;#b2;#ofs2;#delta;#INJb1;#Hofs;#ea1;#ea2; nrewrite > ea1 in LOADV; #LOADV;
3171nlapply INJb1; nwhd in ⊢ (??%? → ?);
3172nlapply (refl ? (f b1)); ncases (f b1) in ⊢ (???% → %);
3173##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; ndestruct;
3174##| #delta'; #DELTA; nwhd in ⊢ (??%? → ?); #H; nelim (grumpydestruct2 ?????? H);
3175    #eb;#edelta;
3176##] nlapply (load_shift … Hmem_shift LOADV DELTA); *; #v2; *;#LOAD;#INJ;
3177@ v2; @; //; nrewrite > Hofs; nrewrite > eb in LOAD; nrewrite > edelta;
3178nrewrite < (?:signed (add ofs1 (repr delta)) = signed ofs1 + delta);
3179##[#H'; napply H'; (* XXX // doesn't work *)
3180##| nrewrite < edelta; napply (address_shift … chunk … Hmem_shift … DELTA);
3181    napply (load_valid_access … LOADV);
3182##]
3183nqed.
3184
3185(* Relation between shifts and stores. *)
3186
3187nlemma store_within_shift:
3188  ∀f,chunk,m1,b,ofs,v1,n1,m2,delta,v2.
3189  mem_shift f m1 m2 →
3190  store chunk m1 b ofs v1 = Some ? n1 →
3191  f b = Some ? delta →
3192  val_shift f v1 v2 →
3193  ∃n2.
3194    store chunk m2 b (ofs + delta) v2 = Some ? n2
3195    ∧ mem_shift f n1 n2.
3196#f;#chunk;#m1;#b;#ofs;#v1;#n1;#m2;#delta;#v2;
3197*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3198#STORE1;#INJb;#Hval_shift;
3199nlapply (store_mapped_inj … ms_inj ?? STORE1 ?);
3200##[ #chunk'; #echunk; napply (load_result_inject … chunk); /2/;
3201##| nwhd in ⊢ (??%?); nrewrite > INJb; (* XXX: // has stopped working *) napply refl
3202##| nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;
3203    nwhd in ⊢ (? → ??%? → ??%? → ?);
3204    nelim (f b1); nelim (f b2);
3205    ##[#_;#e1;nwhd in e1:(??%?);ndestruct;
3206    ##|#z;#_;#e1;nwhd in e1:(??%?);ndestruct;
3207    ##|#z;#_;#_;#e2;nwhd in e2:(??%?);ndestruct;
3208    ##|#delta1';#delta2';#neb;#e1;#e2;
3209       nwhd in e1:(??%?) e2:(??%?);
3210       ndestruct;
3211       @1;@1;@1;//;
3212    ##]
3213##| ##7: //;
3214##| ##4,5,6: ##skip
3215##]
3216*;#n2;*;#STORE;#MINJ;
3217@ n2; @; //; @;
3218##[ (* inj *) //
3219##| (* samedomain *)
3220    nrewrite > (nextblock_store … STORE1);
3221    nrewrite > (nextblock_store … STORE);
3222    //;
3223##| (* domain *)
3224    nrewrite > (nextblock_store … STORE1);
3225    //
3226##| (* range *)
3227    /2/
3228##| #b1;#delta1;#INJb1;
3229    nrewrite > (low_bound_store … STORE b1);
3230    nrewrite > (high_bound_store … STORE b1);
3231    napply ms_range_2;//;
3232##] nqed.
3233
3234nlemma store_outside_shift:
3235  ∀f,chunk,m1,b,ofs,m2,v,m2',delta.
3236  mem_shift f m1 m2 →
3237  f b = Some ? delta →
3238  high_bound m1 b + delta ≤ ofs
3239  ∨ ofs + size_chunk chunk ≤ low_bound m1 b + delta →
3240  store chunk m2 b ofs v = Some ? m2' →
3241  mem_shift f m1 m2'.
3242#f;#chunk;#m1;#b;#ofs;#m2;#v;#m2';#delta;
3243*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3244#INJb;#Hbounds;#STORE;@;
3245##[ (* inj *)
3246    napply (store_outside_inj … STORE); //;
3247    #b';#d'; nwhd in ⊢ (??%? → ?); nlapply (refl ? (f b')); nelim (f b') in ⊢ (???% → %);
3248    ##[ #_; #e; nwhd in e:(??%?); ndestruct;
3249    ##| #d''; #ef; #e; nelim (grumpydestruct2 ?????? e); #eb; #ed;
3250        nrewrite > eb in ef ⊢ %; nrewrite > ed; nrewrite > INJb; #ed';
3251        nrewrite < (grumpydestruct1 ??? ed'); //
3252    ##]
3253##| (* samedomain *) nrewrite > (nextblock_store … STORE); //
3254##| (* domain *) //
3255##| (* range *) /2/
3256##| #b1;#delta1;#INJb1;
3257    nrewrite > (low_bound_store … STORE b1);
3258    nrewrite > (high_bound_store … STORE b1);
3259    napply ms_range_2;//;
3260##] nqed.
3261
3262nlemma storev_shift:
3263  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
3264  mem_shift f m1 m2 →
3265  storev chunk m1 a1 v1 = Some ? n1 →
3266  val_shift f a1 a2 →
3267  val_shift f v1 v2 →
3268  ∃n2.
3269    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_shift f n1 n2.
3270#f;#chunk;#m1;#a1;#v1;#n1;#m2;#a2;#v2;
3271#Hmem_shift;#STOREV;#Hval_shift_a;#Hval_shift_v;
3272ninversion Hval_shift_a;
3273##[ ##1,2,4: #x;#H;nrewrite > H in STOREV;#H';nwhd in H':(??%?); napply False_ind; ndestruct; ##]
3274#b1;#ofs1;#b2;#ofs2;#delta;
3275nwhd in ⊢ (??%? → ?); nlapply (refl ? (f b1)); nelim (f b1) in ⊢ (???% → %);
3276##[#_; #e; nwhd in e:(??%?); ndestruct; ##]
3277#x; #INJb1; #e; nelim (grumpydestruct2 ?????? e); #eb;#ex;
3278nrewrite > ex in INJb1; #INJb1;
3279#OFS; #ea1;#ea2; nrewrite > ea1 in STOREV; #STOREV;
3280nlapply (store_within_shift … Hmem_shift STOREV INJb1 Hval_shift_v);
3281*; #n2; *; #A;#B;
3282@ n2; @; //;
3283nrewrite > OFS; nrewrite > eb in A;
3284nrewrite < (?:signed (add ofs1 (repr delta)) = signed ofs1 + delta);
3285##[ #H; napply H; (* XXX /2/ *)
3286##| napply (address_shift … chunk … Hmem_shift ? INJb1);
3287    napply (store_valid_access_3 … STOREV);
3288##]
3289nqed.
3290
3291(* Relation between shifts and [free]. *)
3292
3293nlemma free_shift:
3294  ∀f,m1,m2,b.
3295  mem_shift f m1 m2 →
3296  mem_shift f (free m1 b) (free m2 b).
3297#f;#m1;#m2;#b;
3298*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2; @;
3299##[ (* inj *)
3300    napply free_right_inj; ##[ napply free_left_inj; //
3301    ##| #b1;#delta; #chunk;#ofs; nwhd in ⊢ (??%? → ?);
3302        nlapply (refl ? (f b1)); nelim (f b1) in ⊢ (???% → %);
3303        ##[ #_; #e; nwhd in e:(??%?); ndestruct;
3304        ##| #delta'; #INJb1; #e; nwhd in e:(??%?); ndestruct;
3305            napply valid_access_free_2
3306        ##]
3307    ##]
3308##| (* samedomain *) nwhd in ⊢ (??%%); //
3309##| (* domain *) nrewrite > (?:nextblock (free m1 b) = nextblock m1); //
3310##| (* range *) /2/
3311##| #b';#delta;#INJb'; ncases (decidable_eq_Z b' b); #eb;
3312    ##[ nrewrite > eb;
3313        nrewrite > (low_bound_free_same ??); nrewrite > (high_bound_free_same ??);
3314        (* arith *) napply daemon
3315    ##| nrewrite > (low_bound_free …); //; nrewrite > (high_bound_free …); /2/;
3316    ##]
3317##] nqed.
3318
3319(* Relation between shifts and allocation. *)
3320
3321ndefinition shift_incr : memshift → memshift → Prop ≝ λf1,f2: memshift.
3322  ∀b. f1 b = f2 b ∨ f1 b = None ?.
3323
3324nremark shift_incr_inject_incr:
3325  ∀f1,f2.
3326  shift_incr f1 f2 → inject_incr (meminj_of_shift f1) (meminj_of_shift f2).
3327#f1;#f2;#Hshift; nwhd in ⊢ (?%%); nwhd; #b;
3328nelim (Hshift b); #INJ; nrewrite > INJ; /2/;
3329nqed.
3330
3331nlemma val_shift_incr:
3332  ∀f1,f2,v1,v2.
3333  shift_incr f1 f2 → val_shift f1 v1 v2 → val_shift f2 v1 v2.
3334#f1;#f2;#v1;#v2;#Hshift_incr; nwhd in ⊢ (% → %);
3335napply val_inject_incr;
3336napply shift_incr_inject_incr; //;
3337nqed.
3338
3339(* *
3340Remark mem_inj_incr:
3341  ∀f1,f2,m1,m2.
3342  inject_incr f1 f2 → mem_inj val_inject f1 m1 m2 → mem_inj val_inject f2 m1 m2.
3343Proof.
3344  intros; red; intros.
3345  destruct (H b1). rewrite <- H3 in H1.
3346  exploit H0; eauto. intros [v2 [A B]].
3347  exists v2; split. auto. apply val_inject_incr with f1; auto.
3348  congruence.
3349***)
3350
3351nlemma alloc_shift:
3352  ∀f,m1,m2,lo1,hi1,m1',b,delta,lo2,hi2.
3353  mem_shift f m1 m2 →
3354  alloc m1 lo1 hi1 = 〈m1', b〉 →
3355  lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 →
3356  min_signed ≤ delta ∧ delta ≤ max_signed →
3357  min_signed ≤ lo2 → hi2 ≤ max_signed →
3358  inj_offset_aligned delta (hi1-lo1) →
3359  ∃f'. ∃m2'.
3360     alloc m2 lo2 hi2 = 〈m2', b〉
3361  ∧ mem_shift f' m1' m2'
3362  ∧ shift_incr f f'
3363  ∧ f' b = Some ? delta.
3364#f;#m1;#m2;#lo1;#hi1;#m1';#b;#delta;#lo2;#hi2;
3365*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3366#ALLOC;#Hlo_delta;#Hhi_delta;#Hdelta_range;#Hlo_range;#Hhi_range;#Hinj_aligned;
3367nlapply (refl ? (alloc m2 lo2 hi2)); nelim (alloc m2 lo2 hi2) in ⊢ (???% → %);
3368#m2';#b';#ALLOC2;
3369ncut (b' = b);
3370##[ nrewrite > (alloc_result … ALLOC); nrewrite > (alloc_result … ALLOC2); // ##]
3371#eb; nrewrite > eb;
3372ncut (f b = None ?);
3373##[ nlapply (ms_domain b); nrewrite > (alloc_result … ALLOC);
3374    nelim (f (nextblock m1)); //;
3375    #z; (* arith *) napply daemon
3376##]
3377#FB;
3378nletin f' ≝ (λb':block. if eqZb b' b then Some ? delta else f b');
3379ncut (shift_incr f f');
3380##[ nwhd; #b0; nwhd in ⊢ (?(???%)?);
3381    napply eqZb_elim; /2/; ##]
3382#Hshift_incr;
3383ncut (f' b = Some ? delta);
3384##[ nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); // ##] #efb';
3385@ f'; @ m2'; @; //; @; //; @; //; @;
3386##[ (* inj *)
3387    ncut (mem_inj val_inject (meminj_of_shift f') m1 m2);
3388    ##[ nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta2; #MINJf'; #LOAD;
3389        ncut (meminj_of_shift f b1 = Some ? 〈b2, delta2〉);
3390        ##[ nrewrite < MINJf'; nwhd in ⊢ (???(?%?)); nwhd in ⊢ (??%%);
3391            napply eqZb_elim; //; #eb;
3392            nrewrite > eb;
3393            ncut (valid_block m1 b);
3394            ##[ napply valid_access_valid_block;
3395              ##[ ##3: napply load_valid_access; // ##]
3396            ##]
3397            ncut (¬valid_block m1 b); ##[ /2/ ##]
3398            #H;#H'; napply False_ind; napply (absurd ? H' H)
3399        ##] #MINJf;
3400        nlapply (ms_inj … MINJf LOAD); *; #v2; *; #A; #B;
3401        @ v2; @; //;
3402        napply (val_inject_incr … B);
3403        napply shift_incr_inject_incr; //
3404    ##] #Hmem_inj;
3405    napply (alloc_parallel_inj … delta Hmem_inj ALLOC ALLOC2 ?); /2/;
3406    nwhd in ⊢ (??%?); nrewrite > efb'; /2/;
3407##| (* samedomain *)
3408    nrewrite > (nextblock_alloc … ALLOC);
3409    nrewrite > (nextblock_alloc … ALLOC2);
3410    //;
3411##| (* domain *)
3412    #b0; (* FIXME: unfold *) nrewrite > (refl ? (f' b0):f' b0 = if eqZb b0 b then Some ? delta else f b0);
3413    nrewrite > (nextblock_alloc … ALLOC);
3414    nrewrite > (alloc_result … ALLOC);
3415    napply eqZb_elim; #eb0;
3416    ##[ nrewrite > eb0; (* arith *) napply daemon
3417    ##| nlapply (ms_domain b0); nelim (f b0);
3418        (* arith *) napply daemon
3419    ##]
3420##| (* range *)
3421    #b0;#delta0; nwhd in ⊢ (??%? → ?);
3422    napply eqZb_elim;
3423    ##[ #_; #e; nrewrite < (grumpydestruct1 ??? e); //
3424    ##| #neb; #e; napply (ms_range_1 … b0); napply e;
3425    ##]
3426##| #b0;#delta0; nwhd in ⊢ (??%? → ?);
3427    nrewrite > (low_bound_alloc … ALLOC2 ?);
3428    nrewrite > (high_bound_alloc … ALLOC2 ?);
3429    napply eqZb_elim; #eb0; nrewrite > eb;
3430    ##[ nrewrite > eb0; #ed; nrewrite < (grumpydestruct1 ??? ed);
3431        nrewrite > (eqZb_z_z ?); /2/;
3432    ##| #edelta0; nrewrite > (eqZb_false … eb0);
3433        napply ms_range_2; nwhd in edelta0:(??%?); //;
3434    ##]
3435##]
3436nqed.
3437*)
3438(* ** Relation between signed and unsigned loads and stores *)
3439
3440(* Target processors do not distinguish between signed and unsigned
3441  stores of 8- and 16-bit quantities.  We show these are equivalent. *)
3442
3443(* Signed 8- and 16-bit stores can be performed like unsigned stores. *)
3444
3445nremark in_bounds_equiv:
3446  ∀chunk1,chunk2,m,b,ofs.∀A:Type.∀a1,a2: A.
3447  size_chunk chunk1 = size_chunk chunk2 →
3448  (match in_bounds m chunk1 b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
3449  (match in_bounds m chunk2 b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
3450#chunk1;#chunk2;#m;#b;#ofs;#A;#a1;#a2;#Hsize;
3451nelim (in_bounds m chunk1 b ofs);
3452##[ #H; nwhd in ⊢ (??%?); nrewrite > (in_bounds_true … A a1 a2 ?); //;
3453    napply valid_access_compat; //;
3454##| #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 b ofs); //;
3455    #H'; napply False_ind; napply (absurd ?? H);
3456    napply valid_access_compat; //;
3457##] nqed.
3458
3459nlemma storev_8_signed_unsigned:
3460  ∀m,a,v.
3461  storev Mint8signed m a v = storev Mint8unsigned m a v.
3462#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
3463#b;#ofs; nwhd in ⊢ (??%%);
3464nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???); //;
3465nqed.
3466
3467nlemma storev_16_signed_unsigned:
3468  ∀m,a,v.
3469  storev Mint16signed m a v = storev Mint16unsigned m a v.
3470#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
3471#b;#ofs; nwhd in ⊢ (??%%);
3472nrewrite > (in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???); //;
3473nqed.
3474
3475(* Likewise, some target processors (e.g. the PowerPC) do not have
3476  a ``load 8-bit signed integer'' instruction. 
3477  We show that it can be synthesized as a ``load 8-bit unsigned integer''
3478  followed by a sign extension. *)
3479
3480nlemma loadv_8_signed_unsigned:
3481  ∀m,a.
3482  loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a).
3483#m;#a; nwhd in ⊢ (??%(????(%))); nelim a; //;
3484#b;#ofs; nwhd in ⊢ (??%(????%));
3485nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???); //;
3486nelim (in_bounds m Mint8unsigned b (signed ofs)); /2/;
3487#H; nwhd in ⊢ (??%%);
3488nelim (getN 0 (signed ofs) (contents (blocks m b))); //;
3489#i; nwhd in ⊢ (??(??%)(??%)); nrewrite > (sign_ext_zero_ext …); //;
3490(* arith *) napply daemon;
3491nqed.
Note: See TracBrowser for help on using the repository browser.