source: C-semantics/Mem.ma @ 15

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

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

File size: 121.3 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            ##[napply Hl2
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
573(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
574nlet rec in_bounds
575  (m:mem) (chunk:memory_chunk) (b:block) (ofs:Z) on b : 
576    Sum (valid_access m chunk b ofs) (Not (valid_access 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
639nlet rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
640  match addr with
641  [ Vptr b ofs ⇒ load chunk m b (signed ofs)
642  | _ ⇒ None ? ].
643
644(* The memory state [m] after a store of value [v] at offset [ofs]
645   in block [b]. *)
646
647ndefinition unchecked_store : memory_chunk → mem → block → Z → val → mem ≝
648λchunk,m,b,ofs,v.
649  let c ≝ (blocks m b) in
650  mk_mem
651    (update ? b
652        (mk_block_contents (low c) (high c)
653                 (setN (pred_size_chunk chunk) ofs v (contents c)))
654        (blocks m))
655    (nextblock m)
656    (nextblock_pos m).
657
658(* [store chunk m b ofs v] perform a write in memory state [m].
659  Value [v] is stored at address [b] and offset [ofs].
660  Return the updated memory store, or [None] if the address is invalid
661  or the memory access is out of bounds. *)
662
663ndefinition store : memory_chunk → mem → block → Z → val → option mem ≝
664λchunk,m,b,ofs,v.
665  match in_bounds m chunk b ofs with
666  [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v)
667  | inr _ ⇒ None ? ].
668
669nlemma store_inv:
670  ∀chunk,m,b,ofs,v,m'.
671  store chunk m b ofs v = Some ? m' →
672  valid_access m chunk b ofs ∧
673  m' = unchecked_store chunk m b ofs v.
674#chunk;#m;#b;#ofs;#v;#m';nwhd in ⊢ (??%? → ?);
675(*9*)
676ncases (in_bounds m chunk b ofs);#Hv;nwhd in ⊢(??%? → ?);#Heq;
677##[@; ##[//|ndestruct;//]
678##|ndestruct]
679nqed.
680
681(* [storev chunk m addr v] is similar, but the address and offset are given
682  as a single value [addr], which must be a pointer value. *)
683
684ndefinition storev : memory_chunk → mem → val → val → option mem ≝
685λchunk,m,addr,v.
686  match addr with
687  [ Vptr b ofs ⇒ store chunk m b (signed ofs) v
688  | _ ⇒ None ? ].
689
690
691(* Build a block filled with the given initialization data. *)
692ndefinition contents_init_data_step :
693  Z → init_data → (Z → contentmap) → contentmap ≝
694  λpos,data,reccall.
695  match data with
696  [ Init_int8 n ⇒
697      setN 0 pos (Vint n) (reccall (pos + oneZ))
698  | Init_int16 n ⇒
699      setN 1 pos (Vint n) (reccall (pos + oneZ))
700  | Init_int32 n ⇒
701      setN 3 pos (Vint n) (reccall (pos + oneZ))
702  | Init_float32 f ⇒
703      setN 3 pos (Vfloat f) (reccall (pos + oneZ))
704  | Init_float64 f ⇒
705      setN 7 pos (Vfloat f) (reccall (pos + oneZ))
706  | Init_space n ⇒ reccall (pos + Zmax n 0) (*??*)
707  | Init_addrof s n ⇒
708      (* Not handled properly yet *)
709      reccall (pos + 4)
710  | Init_pointer x ⇒
711      (* Not handled properly yet *)
712      reccall (pos + 4)].
713
714nlet rec contents_init_data (pos: Z) (i_data: list init_data) on i_data
715  : contentmap ≝
716  match i_data with
717  [ nil ⇒ (λ_.Undef)
718  | cons data i_data' ⇒
719      contents_init_data_step pos data (λn.contents_init_data n i_data') ].
720
721ndefinition size_init_data : init_data → Z ≝
722 λi_data.match i_data with
723  [ Init_int8 _ ⇒ 1
724  | Init_int16 _ ⇒ 2
725  | Init_int32 _ ⇒ 4
726  | Init_float32 _ ⇒ 4
727  | Init_float64 _ ⇒ 8
728  | Init_space n ⇒ Zmax n 0
729  | Init_addrof _ _ ⇒ 4
730  | Init_pointer _ ⇒ Z_of_nat (*** can't use implicit coercion??? *)4].
731
732ndefinition size_init_data_list : list init_data → Z ≝
733  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
734
735nremark size_init_data_list_pos:
736  ∀i_data. OZ ≤ size_init_data_list i_data.
737#i_data;nelim i_data;//;
738#a;#tl;ncut (OZ ≤ size_init_data a)
739##[ncases a;nnormalize;//;
740   #x;ncases x;nnormalize;//;
741##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
742   ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
743   ##[ncases (size_init_data a) in Hsize IH;
744      ##[##1,2:/3/
745      ##|nnormalize;#n;#Hfalse;nelim Hfalse]
746   ##|#Hdisc;ncases Hdisc
747      ##[#Heq;nrewrite > Heq;//;
748      ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2;
749         (* TODO: arithmetics *) napply daemon]
750   ##]
751##]
752nqed.
753
754ndefinition block_init_data : list init_data → block_contents ≝
755  λi_data.mk_block_contents
756    OZ (size_init_data_list i_data) (contents_init_data OZ i_data).
757
758ndefinition alloc_init_data : mem → list init_data → mem × block ≝
759  λm,i_data.
760  〈mk_mem (update ? (nextblock m)
761                 (block_init_data i_data)
762                 (blocks m))
763         (Zsucc (nextblock m))
764         (succ_nextblock_pos m),
765   (nextblock m)〉.
766
767nremark block_init_data_empty:
768  block_init_data [] = empty_block OZ OZ.
769//;
770nqed.
771
772(* * Properties of the memory operations *)
773
774(* ** Properties related to block validity *)
775
776nlemma valid_not_valid_diff:
777  ∀m,b,b'. valid_block m b →  ¬(valid_block m b') → b ≠ b'.
778#m;#b;#b';#H;#H';napply nmk;#e;nrewrite > e in H;#H;
779napply (absurd ? H H');
780nqed.
781
782nlemma valid_access_valid_block:
783  ∀m,chunk,b,ofs. valid_access m chunk b ofs → valid_block m b.
784#m;#chunk;#b;#ofs;#H;
785nelim H;//;
786nqed.
787
788nlemma valid_access_aligned:
789  ∀m,chunk,b,ofs.
790  valid_access m chunk b ofs → (align_chunk chunk ∣ ofs).
791#m;#chunk;#b;#ofs;#H;
792nelim H;//;
793nqed.
794
795nlemma valid_access_compat:
796  ∀m,chunk1,chunk2,b,ofs.
797  size_chunk chunk1 = size_chunk chunk2 →
798  valid_access m chunk1 b ofs →
799  valid_access m chunk2 b ofs.
800#m;#chunk;#chunk2;#b;#ofs;#H1;#H2;
801nelim H2;#H3;#H4;#H5;#H6;
802nrewrite > H1 in H5;#H5;
803@;//;
804nrewrite < (align_chunk_compat … H1);//;
805nqed.
806
807(* Hint Resolve valid_not_valid_diff valid_access_valid_block valid_access_aligned: mem.*)
808
809(* ** Properties related to [load] *)
810
811ntheorem valid_access_load:
812  ∀m,chunk,b,ofs.
813  valid_access m chunk b ofs →
814  ∃v. load chunk m b ofs = Some ? v.
815#m;#chunk;#b;#ofs;#H;@;
816##[##2:nwhd in ⊢ (??%?);napply in_bounds_true;//;
817##|##skip]
818nqed.
819
820ntheorem load_valid_access:
821  ∀m,chunk,b,ofs,v.
822  load chunk m b ofs = Some ? v →
823  valid_access m chunk b ofs.
824#m;#chunk;#b;#ofs;#v;#H;
825ncases (load_inv … H);//;
826nqed.
827
828(* Hint Resolve load_valid_access valid_access_load.*)
829
830(* ** Properties related to [store] *)
831
832nlemma valid_access_store:
833  ∀m1,chunk,b,ofs,v.
834  valid_access m1 chunk b ofs →
835  ∃m2. store chunk m1 b ofs v = Some ? m2.
836#m1;#chunk;#b;#ofs;#v;#H;
837@;
838##[##2:napply in_bounds_true;//
839##|##skip]
840nqed.
841
842(* section STORE *)
843
844nlemma low_bound_store:
845  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
846  ∀b'.low_bound m2 b' = low_bound m1 b'.
847#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
848#b';ncases (store_inv … STORE);
849#H1;#H2;nrewrite > H2;
850nwhd in ⊢ (??(?%?)?);nwhd in ⊢ (??%?);
851nwhd in ⊢ (??(?%)?);nlapply (eqZb_to_Prop b' b);
852ncases (eqZb b' b);nnormalize;//;
853nqed.
854
855nlemma nextblock_store :
856  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
857  nextblock m2 = nextblock m1.
858#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
859ncases (store_inv … STORE);
860#Hvalid;#Heq;
861nrewrite > Heq;@;
862nqed.
863
864nlemma high_bound_store:
865  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
866  ∀b'. high_bound m2 b' = high_bound m1 b'.
867#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
868#b';ncases (store_inv … STORE);
869#Hvalid;#H;
870nrewrite > H;
871nwhd in ⊢ (??(?%?)?);nwhd in ⊢ (??%?);
872nwhd in ⊢ (??(?%)?);nlapply (eqZb_to_Prop b' b);
873ncases (eqZb b' b);nnormalize;//;
874nqed.
875
876nlemma store_valid_block_1:
877  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
878  ∀b'. valid_block m1 b' → valid_block m2 b'.
879#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
880#b';nwhd in ⊢ (% → %);#Hv;
881nrewrite > (nextblock_store … STORE);//;
882nqed.
883
884nlemma store_valid_block_2:
885  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
886  ∀b'. valid_block m2 b' → valid_block m1 b'.
887#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
888#b';nwhd in ⊢ (%→%);
889nrewrite > (nextblock_store … STORE);//;
890nqed.
891
892(*Hint Resolve store_valid_block_1 store_valid_block_2: mem.*)
893
894nlemma store_valid_access_1:
895  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
896  ∀chunk',b',ofs'.
897  valid_access m1 chunk' b' ofs' → valid_access m2 chunk' b' ofs'.
898#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
899#chunk';#b';#ofs';
900* Hv;
901#Hvb;#Hl;#Hr;#Halign;
902@;//;
903##[napply (store_valid_block_1 … STORE);//
904##|nrewrite > (low_bound_store … STORE …);//
905##|nrewrite > (high_bound_store … STORE …);//]
906nqed.
907
908nlemma store_valid_access_2:
909  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
910  ∀chunk',b',ofs'.
911  valid_access m2 chunk' b' ofs' → valid_access m1 chunk' b' ofs'.
912#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
913#chunk';#b';#ofs';
914* Hv;
915#Hvb;#Hl;#Hr;#Halign;
916@;//;
917##[napply (store_valid_block_2 … STORE);//
918##|nrewrite < (low_bound_store … STORE …);//
919##|nrewrite < (high_bound_store … STORE …);//]
920nqed.
921
922nlemma store_valid_access_3:
923  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
924  valid_access m1 chunk b ofs.
925#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
926ncases (store_inv … STORE);//;
927nqed.
928
929(*Hint Resolve store_valid_access_1 store_valid_access_2
930             store_valid_access_3: mem.*)
931
932ntheorem load_store_similar:
933  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
934  ∀chunk'.
935  size_chunk chunk' = size_chunk chunk →
936  load chunk' m2 b ofs = Some ? (load_result chunk' v).
937#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
938#chunk';#Hsize;ncases (store_inv … STORE);
939#Hv;#Heq;
940nwhd in ⊢ (??%?);
941nrewrite > (in_bounds_true m2 chunk' b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))
942               (None ?) ?);
943##[nrewrite > Heq;
944   nwhd in ⊢ (??(??(? ? (? ? ? (? (? % ?)))))?);
945   nrewrite > (update_s ? b ? (blocks m1)); (* XXX  too many metas for my taste *)
946   nrewrite > (? : pred_size_chunk chunk = pred_size_chunk chunk');
947   ##[//;
948   ##|nrewrite > (size_chunk_pred …) in Hsize;#Hsize;
949      nrewrite > (size_chunk_pred …) in Hsize;#Hsize;
950      napply injective_Z_of_nat;napply (injective_Zplus_r 1);//;##]
951##|napply (store_valid_access_1 ?????? STORE);
952   ncases Hv;#H1;#H2;#H3;#H4;@;//;
953   nrewrite > (align_chunk_compat … Hsize);//]
954nqed.
955
956ntheorem load_store_same:
957  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
958  load chunk m2 b ofs = Some ? (load_result chunk v).
959#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
960napply load_store_similar;//;
961nqed.
962       
963ntheorem load_store_other:
964  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
965  ∀chunk',b',ofs'.
966  b' ≠ b
967  ∨ ofs' + size_chunk chunk' ≤  ofs
968  ∨ ofs + size_chunk chunk ≤ ofs' →
969  load chunk' m2 b' ofs' = load chunk' m1 b' ofs'.
970#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
971#chunk';#b';#ofs';#H;
972ncases (store_inv … STORE);
973#Hvalid;#Heq;nwhd in ⊢ (??%%);
974ncases (in_bounds m1 chunk' b' ofs');
975##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' b' ofs' ? (Some ? ?) ??);
976   ##[nwhd in ⊢ (???%);napply eq_f;napply eq_f;
977      nrewrite > Heq;nwhd in ⊢ (??(???(? (? % ?)))?);
978                     nwhd in ⊢ (??(???(? %))?);
979      nlapply (eqZb_to_Prop b' b);ncases (eqZb b' b);
980      nwhd in ⊢ (% → ?);
981      ##[#Heq1;nrewrite > Heq1;nwhd in ⊢ (??(??? (? %))?);
982         nrewrite > (size_chunk_pred …) in H;
983         nrewrite > (size_chunk_pred …);#H;
984         napply (getN_setN_other …);ncases H
985         ##[*
986            ##[#Hfalse;nelim Hfalse;#H1;nelim (H1 Heq1)
987            ##|#H1;@2;(*H1*)napply daemon ##]
988         ##|#H1;@;(*H1*)napply daemon ##]
989      ##|#Hneq;@ ##]
990   ##|napply (store_valid_access_1 … STORE);//##]
991##|nwhd in ⊢ (? → ???%);nlapply (in_bounds m2 chunk' b' ofs');
992   #H1;ncases H1;
993   ##[#H2;#H3;nlapply (store_valid_access_2 … STORE … H2);#Hfalse;
994      ncases H3;#H4;nelim (H4 Hfalse)
995   ##|#H2;#H3;@]
996##]
997nqed.
998
999
1000ntheorem load_store_overlap:
1001  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
1002  ∀chunk',ofs',v'. load chunk' m2 b ofs' = Some ? v' →
1003  ofs' ≠ ofs →
1004  ofs < ofs' + size_chunk chunk' →
1005  ofs' < ofs + size_chunk chunk →
1006  v' = Vundef.
1007#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
1008#chunk';#ofs';#v';#H;
1009#H1;#H2;#H3;
1010ncases (store_inv … STORE);
1011ncases (load_inv … H);
1012#Hvalid;#Heq;#Hvalid1;#Heq1;nrewrite > Heq;nrewrite > Heq1;
1013nchange in ⊢ (??(??(???(?(?%?))))?) with (mk_mem ???);
1014nrewrite > (update_s block_contents …);
1015nrewrite > (getN_setN_overlap …);
1016##[ncases chunk';//
1017##|nrewrite > (size_chunk_pred …) in H2;(*arith*) napply daemon
1018##|nrewrite > (size_chunk_pred …) in H3;(*arith*) napply daemon
1019##|napply sym_neq;//]
1020nqed.
1021
1022ntheorem load_store_overlap':
1023  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
1024  ∀chunk',ofs'.
1025  valid_access m1 chunk' b ofs' →
1026  ofs' ≠ ofs →
1027  ofs < ofs' + size_chunk chunk' →
1028  ofs' < ofs + size_chunk chunk →
1029  load chunk' m2 b ofs' = Some ? Vundef.
1030#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
1031#chunk';#ofs';#Hvalid;#H;#H1;#H2;
1032ncut (∃v'.load chunk' m2 b ofs' = Some ? v')
1033##[napply valid_access_load;
1034   napply (store_valid_access_1 … STORE);//
1035##|#H3;ncases H3;
1036   #x;#Hx;nrewrite > Hx;napply eq_f;
1037   napply (load_store_overlap … STORE … Hx);//;##]
1038nqed.
1039
1040ntheorem load_store_mismatch:
1041  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
1042  ∀chunk',v'.
1043  load chunk' m2 b ofs = Some ? v' →
1044  size_chunk chunk' ≠ size_chunk chunk →
1045  v' = Vundef.
1046#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
1047#chunk';#v';#H;#H1;
1048ncases (store_inv … STORE);
1049ncases (load_inv … H);
1050#Hvalid;#H2;#Hvalid1;#H3;
1051nrewrite > H2;
1052nchange in H3:(???%) with (mk_mem ???);
1053nrewrite > H3;nrewrite > (update_s block_contents …);
1054nrewrite > (getN_setN_mismatch …);
1055##[ncases chunk';//;
1056##|nrewrite > (size_chunk_pred …) in H1;nrewrite > (size_chunk_pred …);
1057   #H1;napply nmk;#Hfalse;nelim H1;#H4;napply H4;
1058   napply (eq_f ?? (λx.1 + x) ???);//##]
1059nqed.
1060
1061ntheorem load_store_mismatch':
1062  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
1063  ∀chunk'.
1064  valid_access m1 chunk' b ofs →
1065  size_chunk chunk' ≠ size_chunk chunk →
1066  load chunk' m2 b ofs = Some ? Vundef.
1067#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
1068#chunk';#Hvalid;#Hsize;
1069ncut (∃v'.load chunk' m2 b ofs = Some ? v')
1070##[napply (valid_access_load …);
1071   napply (store_valid_access_1 … STORE);//
1072##|*;#x;#Hx;nrewrite > Hx;napply eq_f;
1073   napply (load_store_mismatch … STORE … Hsize);//;##]
1074nqed.
1075
1076ninductive load_store_cases
1077      (chunk1: memory_chunk) (b1: block) (ofs1: Z)
1078      (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type ≝
1079  | lsc_similar:
1080      b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 = size_chunk chunk2 →
1081      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
1082  | lsc_other:
1083      b1 ≠ b2 ∨ ofs2 + size_chunk chunk2 ≤ ofs1 ∨ ofs1 + size_chunk chunk1 ≤ ofs2 →
1084      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
1085  | lsc_overlap:
1086      b1 = b2 -> ofs1 ≠ ofs2 -> ofs1 < ofs2 + size_chunk chunk2 → ofs2 < ofs1 + size_chunk chunk1 ->
1087      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
1088  | lsc_mismatch:
1089      b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 ≠ size_chunk chunk2 ->
1090      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.
1091
1092ndefinition load_store_classification:
1093  ∀chunk1,b1,ofs1,chunk2,b2,ofs2.
1094  load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.
1095#chunk1;#b1;#ofs1;#chunk2;#b2;#ofs2;
1096ncases (decidable_eq_Z_Type b1 b2);#H;
1097##[ncases (decidable_eq_Z_Type ofs1 ofs2);#H1;
1098   ##[ncases (decidable_eq_Z_Type (size_chunk chunk1) (size_chunk chunk2));#H2
1099      ##[napply lsc_similar;//;
1100      ##|napply lsc_mismatch;//;##]
1101   ##|nlapply (Z_compare_to_Prop (ofs2 + size_chunk chunk2) ofs1);
1102      ncases (Z_compare (ofs2+size_chunk chunk2) ofs1);
1103      ##[nchange with (Zlt ? ? → ?);#H2;
1104         napply lsc_other;@;@2;(*trivial Zlt_to_Zle BUT the statement is strange*)
1105         napply daemon
1106      ##|nchange with (? = ? → ?);#H2;
1107         napply lsc_other;@;@2;(*trivial eq_to_Zle not defined *) napply daemon
1108      ##|nchange with (Zlt ? ? → ?);#H2;
1109         nlapply (Z_compare_to_Prop (ofs1 + size_chunk chunk1) ofs2);
1110         ncases (Z_compare (ofs1 + size_chunk chunk1) ofs2);
1111         ##[nchange with (Zlt ? ? → ?);#H3;
1112            napply lsc_other;@2;(*trivial as previously*) napply daemon
1113         ##|nchange with (? = ? → ?);#H3;
1114            napply lsc_other;@2;(*trivial as previously*) napply daemon
1115         ##|nchange with (Zlt ? ? → ?);#H3;
1116            napply lsc_overlap;//;##]
1117      ##]
1118   ##]
1119##|napply lsc_other;@;@; (* XXX // doesn't spot this! *) napply H ##]
1120nqed.
1121
1122ntheorem load_store_characterization:
1123  ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
1124  ∀chunk',b',ofs'.
1125  valid_access m1 chunk' b' ofs' ->
1126  load chunk' m2 b' ofs' =
1127    match load_store_classification chunk b ofs chunk' b' ofs' with
1128    [ lsc_similar _ _ _ => Some ? (load_result chunk' v)
1129    | lsc_other _ => load chunk' m1 b' ofs'
1130    | lsc_overlap _ _ _ _ => Some ? Vundef
1131    | lsc_mismatch _ _ _ => Some ? Vundef ].
1132#chunk;#m1;#b;#ofs;#v;#m2;#STORE;
1133#chunk';#b';#ofs';#Hvalid;
1134ncut (∃v'. load chunk' m2 b' ofs' = Some ? v')
1135##[napply valid_access_load;
1136   napply (store_valid_access_1 … STORE … Hvalid);
1137##|*;#x;#Hx;
1138   ncases (load_store_classification chunk b ofs chunk' b' ofs')
1139   ##[#H1;#H2;#H3;nrewrite > H1;napply load_store_similar;//;
1140   ##|#H1;napply (load_store_other … STORE);
1141      ncases H1
1142      ##[*
1143         ##[#H2;@;@;napply sym_neq;//
1144         ##|#H2;@;@2;//]
1145      ##|#H2;@2;//]
1146   ##|#H1;#H2;#H3;#H4;nrewrite < H1 in Hx;
1147      #Hx;nrewrite > Hx;
1148      napply eq_f;napply (load_store_overlap … STORE … Hx);/2/;
1149   ##|#H1;#H2;#H3;nrewrite < H1 in Hx;
1150      nrewrite < H2;#Hx;nrewrite > Hx;napply eq_f;
1151      napply (load_store_mismatch … STORE … Hx);/2/]
1152##]
1153nqed.
1154
1155(*nlemma d : ∀a,b,c,d:nat.∀e:〈a,b〉 = 〈c,d〉. ∀P:(∀a,b,c,d,e.Prop).
1156           P a b c d e → P a b a b (refl ??).
1157#a;#b;#c;#d;#e;#P;#H1;ndestruct;*)
1158
1159(*
1160Section ALLOC.
1161
1162Variable m1: mem.
1163Variables lo hi: Z.
1164Variable m2: mem.
1165Variable b: block.
1166Hypothesis ALLOC: alloc m1 lo hi = (m2, b).
1167*)
1168
1169ndefinition pairdisc ≝
1170λA,B.λx,y:pair A B.
1171match x with
1172[(mk_pair t0 t1) ⇒
1173match y with
1174[(mk_pair u0 u1) ⇒
1175  ∀P: Type[1].
1176  (∀e0: (eq A (R0 ? t0) u0).
1177   ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].
1178
1179nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
1180#A;#B;#x;#y;#e;nrewrite > e;ncases y;
1181#a;#b;nnormalize;#P;#PH;napply PH;@;
1182nqed.
1183
1184nlemma nextblock_alloc:
1185  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1186  nextblock m2 = Zsucc (nextblock m1).
1187#m1;#lo;#hi;#m2;#b;#ALLOC;
1188nwhd in ALLOC:(??%%); ndestruct; //;
1189nqed.
1190
1191nlemma alloc_result:
1192  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1193  b = nextblock m1.
1194#m1;#lo;#hi;#m2;#b;#ALLOC;
1195nwhd in ALLOC:(??%%); ndestruct; //;
1196nqed.
1197
1198
1199nlemma valid_block_alloc:
1200  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1201  ∀b'. valid_block m1 b' → valid_block m2 b'.
1202#m1;#lo;#hi;#m2;#b;#ALLOC;
1203#b'; nrewrite > (unfold_valid_block m1 b');
1204nrewrite > (unfold_valid_block m2 b');
1205nrewrite > (nextblock_alloc … ALLOC);
1206(* arith *) napply daemon;
1207nqed.
1208
1209nlemma fresh_block_alloc:
1210  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1211  ¬(valid_block m1 b).
1212#m1;#lo;#hi;#m2;#b;#ALLOC;
1213nrewrite > (unfold_valid_block m1 b);
1214nrewrite > (alloc_result … ALLOC);
1215(* arith *) napply daemon;
1216nqed.
1217
1218nlemma valid_new_block:
1219  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1220  valid_block m2 b.
1221#m1;#lo;#hi;#m2;#b;#ALLOC;
1222nrewrite > (unfold_valid_block m2 b);
1223nrewrite > (alloc_result … ALLOC);
1224nrewrite > (nextblock_alloc … ALLOC);
1225(* arith *) napply daemon;
1226nqed.
1227
1228(*
1229Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
1230*)
1231
1232nlemma valid_block_alloc_inv:
1233  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1234  ∀b'. valid_block m2 b' → b' = b ∨ valid_block m1 b'.
1235#m1;#lo;#hi;#m2;#b;#ALLOC;
1236#b';
1237nrewrite > (unfold_valid_block m2 b');
1238nrewrite > (unfold_valid_block m1 b');
1239nrewrite > (nextblock_alloc … ALLOC); #H;
1240nrewrite > (alloc_result … ALLOC);
1241(* arith *) napply daemon;
1242nqed.
1243
1244nlemma low_bound_alloc:
1245  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1246  ∀b'. low_bound m2 b' = if eqZb b' b then lo else low_bound m1 b'.
1247#m1;#lo;#hi;#m2;#b;#ALLOC;
1248nwhd in ALLOC:(??%%); ndestruct; #b';
1249nrewrite > (unfold_update block_contents ????);
1250ncases (eqZb b' (nextblock m1)); //;
1251nqed.
1252
1253nlemma low_bound_alloc_same:
1254  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1255  low_bound m2 b = lo.
1256#m1;#lo;#hi;#m2;#b;#ALLOC;
1257nrewrite > (low_bound_alloc … ALLOC b);
1258nrewrite > (eqZb_z_z …);
1259//;
1260nqed.
1261
1262nlemma low_bound_alloc_other:
1263  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1264  ∀b'. valid_block m1 b' → low_bound m2 b' = low_bound m1 b'.
1265#m1;#lo;#hi;#m2;#b;#ALLOC;
1266#b'; nrewrite > (low_bound_alloc … ALLOC b');
1267napply eqZb_elim; #Hb;
1268##[ nrewrite > Hb; #bad; napply False_ind; napply (absurd ? bad);
1269    napply (fresh_block_alloc … ALLOC)
1270##| //
1271##] nqed.
1272
1273nlemma high_bound_alloc:
1274  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1275  ∀b'. high_bound m2 b' = if eqZb b' b then hi else high_bound m1 b'.
1276#m1;#lo;#hi;#m2;#b;#ALLOC;
1277nwhd in ALLOC:(??%%); ndestruct; #b';
1278nrewrite > (unfold_update block_contents ????);
1279ncases (eqZb b' (nextblock m1)); //;
1280nqed.
1281
1282nlemma high_bound_alloc_same:
1283  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1284  high_bound m2 b = hi.
1285#m1;#lo;#hi;#m2;#b;#ALLOC;
1286nrewrite > (high_bound_alloc … ALLOC b);
1287nrewrite > (eqZb_z_z …);
1288//;
1289nqed.
1290
1291nlemma high_bound_alloc_other:
1292  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1293  ∀b'. valid_block m1 b' → high_bound m2 b' = high_bound m1 b'.
1294#m1;#lo;#hi;#m2;#b;#ALLOC;
1295#b'; nrewrite > (high_bound_alloc … ALLOC b');
1296napply eqZb_elim; #Hb;
1297##[ nrewrite > Hb; #bad; napply False_ind; napply (absurd ? bad);
1298    napply (fresh_block_alloc … ALLOC)
1299##| //
1300##] nqed.
1301
1302nlemma valid_access_alloc_other:
1303  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1304  ∀chunk,b',ofs.
1305  valid_access m1 chunk b' ofs →
1306  valid_access m2 chunk b' ofs.
1307#m1;#lo;#hi;#m2;#b;#ALLOC;
1308#chunk;#b';#ofs;#H;
1309ncases H; #Hvalid; #Hlow; #Hhigh;#Halign;
1310@;
1311##[ napply (valid_block_alloc … ALLOC); //
1312##| nrewrite > (low_bound_alloc_other … ALLOC b' Hvalid); //
1313##| nrewrite > (high_bound_alloc_other … ALLOC b' Hvalid); //
1314##| //
1315##] nqed.
1316
1317nlemma valid_access_alloc_same:
1318  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1319  ∀chunk,ofs.
1320  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
1321  valid_access m2 chunk b ofs.
1322#m1;#lo;#hi;#m2;#b;#ALLOC;
1323#chunk;#ofs; #Hlo; #Hhi; #Halign;
1324@;
1325##[ napply (valid_new_block … ALLOC)
1326##| nrewrite > (low_bound_alloc_same … ALLOC); //
1327##| nrewrite > (high_bound_alloc_same … ALLOC); //
1328##| //
1329##] nqed.
1330
1331(*
1332Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
1333*)
1334
1335nlemma valid_access_alloc_inv:
1336  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1337  ∀chunk,b',ofs.
1338  valid_access m2 chunk b' ofs →
1339  valid_access m1 chunk b' ofs ∨
1340  (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs))).
1341#m1;#lo;#hi;#m2;#b;#ALLOC;
1342#chunk;#b';#ofs;*;#Hblk;#Hlo;#Hhi;#Hal;
1343nelim (valid_block_alloc_inv … ALLOC ? Hblk);#H;
1344##[ nrewrite < H in ALLOC ⊢ %; #ALLOC';
1345    nrewrite > (low_bound_alloc_same … ALLOC') in Hlo; #Hlo';
1346    nrewrite > (high_bound_alloc_same … ALLOC') in Hhi; #Hhi';
1347    @2; /4/
1348##| @1;@;//;
1349  ##[ nrewrite > (low_bound_alloc_other … ALLOC ??) in Hlo; //
1350  ##| nrewrite > (high_bound_alloc_other … ALLOC ??) in Hhi; //
1351  ##]
1352##] nqed.
1353
1354ntheorem load_alloc_unchanged:
1355  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1356  ∀chunk,b',ofs.
1357  valid_block m1 b' →
1358  load chunk m2 b' ofs = load chunk m1 b' ofs.
1359#m1;#lo;#hi;#m2;#b;#ALLOC;
1360#chunk;#b';#ofs;#H;nwhd in ⊢ (??%%);
1361ncases (in_bounds m2 chunk b' ofs); #H';
1362##[ nelim (valid_access_alloc_inv … ALLOC ??? H');
1363  ##[ #H''; (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error
1364  nrewrite > (in_bounds_true ???? ??? H''); *) nrewrite > (in_bounds_true … ? (option val) ?? H'');
1365      nwhd in ⊢ (??%?); (* XXX: if you do this at the point below the proof term is ill-typed. *)
1366       nwhd in ALLOC:(??%%); ndestruct;
1367      nrewrite > (update_o block_contents ?????);
1368      ##[ // ##| napply sym_neq; napply (valid_not_valid_diff … H); napply (fresh_block_alloc … );//; ##]
1369  ##| *;*;#A;#B;#C; nrewrite < A in ALLOC ⊢ %; #ALLOC;
1370      napply False_ind; napply (absurd ? H); napply (fresh_block_alloc … ALLOC)
1371  ##]
1372##| ncases (in_bounds m1 chunk b' ofs); #H''; nwhd in ⊢ (??%%); //;
1373    napply False_ind; napply (absurd ? ? H'); napply (valid_access_alloc_other … ALLOC); //
1374##] nqed.
1375 
1376ntheorem load_alloc_other:
1377  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1378  ∀chunk,b',ofs,v.
1379  load chunk m1 b' ofs = Some ? v →
1380  load chunk m2 b' ofs = Some ? v.
1381#m1;#lo;#hi;#m2;#b;#ALLOC;
1382#chunk;#b';#ofs;#v;#H;
1383nrewrite < H; napply (load_alloc_unchanged … ALLOC ???); /3/;
1384nqed.
1385
1386ntheorem load_alloc_same:
1387  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1388  ∀chunk,ofs,v.
1389  load chunk m2 b ofs = Some ? v →
1390  v = Vundef.
1391#m1;#lo;#hi;#m2;#b;#ALLOC;
1392#chunk;#ofs;#v;#H;
1393nelim (load_inv … H); #H0; #H1; nrewrite > H1;
1394 nwhd in ALLOC:(??%%); (* XXX ndestruct; ??? *) napply (pairdisc_elim … ALLOC);
1395 nwhd in ⊢ (??%% → ?);#e0;nrewrite < e0 in ⊢ (%→?);
1396 nwhd in ⊢ (??%% → ?);#e1;
1397nrewrite < e1; nrewrite < e0; nrewrite > (update_s ? ? (empty_block lo hi) ?);
1398nnormalize; ncases chunk; //;
1399nqed.
1400
1401ntheorem load_alloc_same':
1402  ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
1403  ∀chunk,ofs.
1404  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
1405  load chunk m2 b ofs = Some ? Vundef.
1406#m1;#lo;#hi;#m2;#b;#ALLOC;
1407#chunk;#ofs;#Hlo;#Hhi;#Hal;
1408ncut (∃v. load chunk m2 b ofs = Some ? v);
1409##[ napply valid_access_load; @; /2/;
1410  ##[ nrewrite > (low_bound_alloc_same … ALLOC); //
1411  ##| nrewrite > (high_bound_alloc_same … ALLOC); //
1412  ##]
1413##| *; #v;#LOAD; nrewrite > LOAD; napply eq_f;
1414    napply (load_alloc_same … ALLOC … LOAD);
1415##] nqed.
1416
1417(*
1418End ALLOC.
1419
1420Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
1421Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
1422Hint Resolve load_alloc_unchanged: mem.
1423
1424*)
1425
1426(* ** Properties related to [free]. *)
1427(*
1428Section FREE.
1429
1430Variable m: mem.
1431Variable bf: block.
1432*)
1433
1434nlemma valid_block_free_1:
1435  ∀m,bf,b. valid_block m b → valid_block (free m bf) b.
1436nnormalize;//;
1437nqed.
1438
1439nlemma valid_block_free_2:
1440  ∀m,bf,b. valid_block (free m bf) b → valid_block m b.
1441nnormalize;//;
1442nqed.
1443
1444(*
1445Hint Resolve valid_block_free_1 valid_block_free_2: mem.
1446*)
1447
1448nlemma low_bound_free:
1449  ∀m,bf,b. b ≠ bf -> low_bound (free m bf) b = low_bound m b.
1450#m;#bf;#b;#H;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
1451nrewrite > (update_o block_contents …); //; napply sym_neq; //;
1452nqed.
1453
1454nlemma high_bound_free:
1455  ∀m,bf,b. b ≠ bf → high_bound (free m bf) b = high_bound m b.
1456#m;#bf;#b;#H;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
1457nrewrite > (update_o block_contents …); //; napply sym_neq; //;
1458nqed.
1459
1460nlemma low_bound_free_same:
1461  ∀m,b. low_bound (free m b) b = 0.
1462#m;#b;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
1463nrewrite > (update_s block_contents …); //;
1464nqed.
1465
1466nlemma high_bound_free_same:
1467  ∀m,b. high_bound (free m b) b = 0.
1468#m;#b;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
1469nrewrite > (update_s block_contents …); //;
1470nqed.
1471
1472nlemma valid_access_free_1:
1473  ∀m,bf,chunk,b,ofs.
1474  valid_access m chunk b ofs → b ≠ bf →
1475  valid_access (free m bf) chunk b ofs.
1476#m;#bf;#chunk;#b;#ofs;*;#Hval;#Hlo;#Hhi;#Hal;#Hneq;
1477@; //;
1478##[ napply valid_block_free_1; //
1479##| nrewrite > (low_bound_free … Hneq); //
1480##| nrewrite > (high_bound_free … Hneq); //
1481##] nqed.
1482
1483nlemma valid_access_free_2:
1484  ∀m,bf,chunk,ofs. ¬(valid_access (free m bf) chunk bf ofs).
1485#m;#bf;#chunk;#ofs; napply nmk; *; #Hval;#Hlo;#Hhi;#Hal;
1486nwhd in Hlo:(?%?);nwhd in Hlo:(?(?(?%?))?); nrewrite > (update_s block_contents …) in Hlo;
1487nwhd in Hhi:(??%);nwhd in Hhi:(??(?(?%?))); nrewrite > (update_s block_contents …) in Hhi;
1488nwhd in ⊢ ((??%)→(?%?)→?); (* arith *) napply daemon;
1489nqed.
1490
1491(*
1492Hint Resolve valid_access_free_1 valid_access_free_2: mem.
1493*)
1494
1495nlemma valid_access_free_inv:
1496  ∀m,bf,chunk,b,ofs.
1497  valid_access (free m bf) chunk b ofs →
1498  valid_access m chunk b ofs ∧ b ≠ bf.
1499#m;#bf;#chunk;#b;#ofs; nelim (decidable_eq_Z_Type b bf);
1500##[ #e; nrewrite > e;
1501    #H; napply False_ind; napply (absurd ? H (valid_access_free_2 …));
1502##| #ne; *; nrewrite > (low_bound_free … ne);
1503    nrewrite > (high_bound_free … ne);
1504    #Hval; #Hlo; #Hhi; #Hal;
1505    @; /2/; @; //; napply (valid_block_free_2 … Hval);
1506##] nqed.
1507
1508ntheorem load_free:
1509  ∀m,bf,chunk,b,ofs.
1510  b ≠ bf →
1511  load chunk (free m bf) b ofs = load chunk m b ofs.
1512#m;#bf;#chunk;#b;#ofs;#ne; nwhd in ⊢ (??%%);
1513nelim (in_bounds m chunk b ofs);
1514##[ #Hval; nwhd in ⊢ (???%); nrewrite > (in_bounds_true ???? (option val) ???);
1515  ##[ nwhd in ⊢ (??(??(??(???(?(?%?)))))?); nrewrite > (update_o block_contents …); //;
1516      napply sym_neq; //
1517  ##| napply valid_access_free_1; //; napply ne;
1518  ##]
1519##| nelim (in_bounds (free m bf) chunk b ofs); (* XXX just // used to work *) ##[ ##2: nnormalize; //; ##]
1520    #H;#H'; napply False_ind; napply (absurd ? ? H');
1521    nelim (valid_access_free_inv …H); //;
1522##] nqed.
1523
1524(*
1525End FREE.
1526*)
1527
1528(* ** Properties related to [free_list] *)
1529
1530nlemma valid_block_free_list_1:
1531  ∀bl,m,b. valid_block m b → valid_block (free_list m bl) b.
1532#bl;nelim bl;
1533##[ #m;#b;#H; nwhd in ⊢ (?%?); //
1534##| #h;#t;#IH;#m;#b;#H; nrewrite > (unfold_free_list m h t);
1535    napply valid_block_free_1; napply IH; //
1536##] nqed.
1537
1538nlemma valid_block_free_list_2:
1539  ∀bl,m,b. valid_block (free_list m bl) b → valid_block m b.
1540#bl; nelim bl;
1541##[ #m;#b;#H; nwhd in H:(?%?); //
1542##| #h;#t;#IH;#m;#b; nrewrite > (unfold_free_list m h t);#H;
1543    napply IH; napply valid_block_free_2; //
1544##] nqed.
1545
1546nlemma valid_access_free_list:
1547  ∀chunk,b,ofs,m,bl.
1548  valid_access m chunk b ofs → ¬in_list ? b bl →
1549  valid_access (free_list m bl) chunk b ofs.
1550#chunk; #b; #ofs; #m; #bl; nelim bl;
1551##[ nwhd in ⊢ (?→?→(?%???)); //
1552##| #h;#t;#IH;#H;#notin; nrewrite > (unfold_free_list m h t); napply valid_access_free_1;
1553    ##[ napply IH; //; napply (not_to_not ??? notin); #Ht; napply (in_list_cons … Ht)
1554    ##| napply nmk; #e; napply (absurd ?? notin); nrewrite > e; // ##]
1555##] nqed.
1556
1557nlemma valid_access_free_list_inv:
1558  ∀chunk,b,ofs,m,bl.
1559  valid_access (free_list m bl) chunk b ofs →
1560  ¬in_list ? b bl ∧ valid_access m chunk b ofs.
1561#chunk; #b; #ofs; #m; #bl; nelim bl;
1562##[ nwhd in ⊢ ((?%???)→?); #H; @; //
1563##| #h;#t;#IH; nrewrite > (unfold_free_list m h t); #H;
1564    nelim (valid_access_free_inv … H); #H';#ne;
1565    nelim (IH H'); #notin;#H''; @; //;
1566    napply (not_to_not ??? notin); #Ht;
1567    (* WTF? this is specialised to nat! napply (in_list_tail t b h); *) napply daemon
1568##] nqed.
1569
1570(* ** Properties related to pointer validity *)
1571
1572nlemma valid_pointer_valid_access:
1573  ∀m,b,ofs.
1574  valid_pointer m b ofs = true ↔ valid_access m Mint8unsigned b ofs.
1575#m;#b;#ofs;nwhd in ⊢ (?(??%?)?); @;
1576##[ #H;
1577    nlapply (andb_true_l … H); #H';
1578    nlapply (andb_true_l … H'); #H1;
1579    nlapply (andb_true_r … H'); #H2;
1580    nlapply (andb_true_r … H); #H3;
1581    @;
1582    ##[ nrewrite > (unfold_valid_block m b); napply (Zltb_true_to_Zlt … H1)
1583    ##| napply (Zleb_true_to_Zle … H2)
1584    ##| nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
1585    ##| ncases ofs; /2/;
1586    ##]
1587##| *; #Hval;#Hlo;#Hhi;#Hal;
1588    nrewrite > (Zlt_to_Zltb_true … Hval);
1589    nrewrite > (Zle_to_Zleb_true … Hlo);
1590    nwhd in Hhi:(?(??%)?); nrewrite > (Zlt_to_Zltb_true … ?);
1591    //; (* arith *) napply daemon
1592##] nqed.
1593
1594ntheorem valid_pointer_alloc:
1595  ∀m1,m2: mem. ∀lo,hi: Z. ∀b,b': block. ∀ofs: Z.
1596  alloc m1 lo hi = 〈m2, b'〉 →
1597  valid_pointer m1 b ofs = true →
1598  valid_pointer m2 b ofs = true.
1599#m1;#m2;#lo;#hi;#b;#b';#ofs;#ALLOC;#VALID;
1600nlapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval;
1601napply (proj2 ?? (valid_pointer_valid_access ???));
1602napply (valid_access_alloc_other … ALLOC … Hval);
1603nqed.
1604
1605ntheorem valid_pointer_store:
1606  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
1607  store chunk m1 b' ofs' v = Some ? m2 →
1608  valid_pointer m1 b ofs = true → valid_pointer m2 b ofs = true.
1609#chunk;#m1;#m2;#b;#b';#ofs;#ofs';#v;#STORE;#VALID;
1610nlapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval;
1611napply (proj2 ?? (valid_pointer_valid_access ???));
1612napply (store_valid_access_1 … STORE … Hval);
1613nqed.
1614
1615(* * * Generic injections between memory states. *)
1616
1617(* Section GENERIC_INJECT. *)
1618
1619ndefinition meminj : Type ≝ block → option (block × Z).
1620(*
1621Variable val_inj: meminj -> val -> val -> Prop.
1622
1623Hypothesis val_inj_undef:
1624  ∀mi. val_inj mi Vundef Vundef.
1625*)
1626
1627ndefinition mem_inj ≝ λval_inj.λmi: meminj. λm1,m2: mem.
1628  ∀chunk, b1, ofs, v1, b2, delta.
1629  mi b1 = Some ? 〈b2, delta〉 →
1630  load chunk m1 b1 ofs = Some ? v1 →
1631  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2.
1632
1633(* FIXME: another nunfold hack*)
1634nlemma unfold_mem_inj : ∀val_inj.∀mi: meminj. ∀m1,m2: mem.
1635  (mem_inj val_inj mi m1 m2) =
1636  (∀chunk, b1, ofs, v1, b2, delta.
1637  mi b1 = Some ? 〈b2, delta〉 →
1638  load chunk m1 b1 ofs = Some ? v1 →
1639  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2).
1640//; nqed.
1641
1642nlemma valid_access_inj: ∀val_inj.
1643  ∀mi,m1,m2,chunk,b1,ofs,b2,delta.
1644  mi b1 = Some ? 〈b2, delta〉 →
1645  mem_inj val_inj mi m1 m2 →
1646  valid_access m1 chunk b1 ofs →
1647  valid_access m2 chunk b2 (ofs + delta).
1648#val_inj;
1649#mi;#m1;#m2;#chunk;#b1;#ofs;#b2;#delta;#H;#Hinj;#Hval;
1650ncut (∃v1. load chunk m1 b1 ofs = Some ? v1);
1651##[ /2/;
1652##| *;#v1;#LOAD1;
1653    nelim (Hinj … H LOAD1);#v2;*;#LOAD2;#VCP;
1654    /2/
1655##] nqed.
1656
1657(*Hint Resolve valid_access_inj: mem.*)
1658
1659(* FIXME: can't use ndestruct below *)
1660nlemma grumpydestruct : ∀A,v. None A = Some A v → False.
1661#A;#v;#H;ndestruct;
1662nqed.
1663
1664nlemma store_unmapped_inj: ∀val_inj.
1665  ∀mi,m1,m2,b,ofs,v,chunk,m1'.
1666  mem_inj val_inj mi m1 m2 →
1667  mi b = None ? →
1668  store chunk m1 b ofs v = Some ? m1' →
1669  mem_inj val_inj mi m1' m2.
1670#val_inj;
1671#mi;#m1;#m2;#b;#ofs;#v;#chunk;#m1';#Hinj;#Hmi;#Hstore;
1672nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload;
1673ncut (load chunk0 m1 b1 ofs0 = Some ? v1);
1674##[ nrewrite < Hload; napply sym_eq; napply (load_store_other … Hstore);
1675    @1;@1; napply nmk; #eq; nrewrite > eq in Hmi0; nrewrite > Hmi; #H; ndestruct;
1676##| #Hload'; napply (Hinj … Hmi0 Hload');
1677##] nqed.
1678
1679nlemma store_outside_inj: ∀val_inj.
1680  ∀mi,m1,m2,chunk,b,ofs,v,m2'.
1681  mem_inj val_inj mi m1 m2 →
1682  (∀b',delta.
1683    mi b' = Some ? 〈b, delta〉 →
1684    high_bound m1 b' + delta ≤ ofs
1685    ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) →
1686  store chunk m2 b ofs v = Some ? m2' →
1687  mem_inj val_inj mi m1 m2'.
1688#val_inj;
1689#mi;#m1;#m2;#chunk;#b;#ofs;#v;#m2';#Hinj;#Hbounds;#Hstore;
1690nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload;
1691nlapply (Hinj … Hmi0 Hload);*;#v2;*;#LOAD2;#VINJ;
1692@ v2;@;//;
1693nrewrite < LOAD2; napply (load_store_other … Hstore);
1694nelim (decidable_eq_Z b2 b);
1695##[ #Heq; nrewrite > Heq in Hmi0 LOAD2; #Hmi0;#LOAD2;
1696    nlapply (Hbounds … Hmi0); #Hb;
1697    ncut (valid_access m1 chunk0 b1 ofs0); /2/;
1698    #Hv; nelim Hv; #Hv1; #Hlo1; #Hhi1; #Hal1;
1699    nelim Hb; #Hb; ##[ @1;@2;(* arith *) napply daemon ##| @2;(* arith *) napply daemon ##]
1700##| #ineq; @1; @1; napply ineq;
1701##] nqed.
1702
1703(* XXX: use Or rather than ∨ to bring resource usage under control. *)
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  Or (Or (Or (b1' ≠ b2')
1710             (low_bound m b1 ≥ high_bound m b1))
1711         (low_bound m b2 ≥ high_bound m b2))
1712  (Or (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 ndestruct expands proof state too much;*)
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:(??%%); ndestruct;
1754                napply Hvalinj; //;
1755            ##]
1756         ##| #Hdis; #H; (* disjoint *)
1757             nrewrite > LOAD1 in H; #H;
1758             nlapply (Hinj … CP ?); ##[ napply sym_eq; napply H; ##| ##*: ##]
1759             *;#v2';*;#LOAD2;#VCP;
1760             @ v2'; @; //;
1761             nrewrite < LOAD2; napply (load_store_other … STORE2);
1762             nelim (decidable_eq_Z b1 b1'); #eb1;
1763             ##[ nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
1764                 nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
1765                 nelim Hdis; ##[ #Hdis; nelim Hdis;
1766                               ##[ #eb1'; napply False_ind; napply (absurd ? eb1 eb1');
1767                               ##| #Hdis;@1;@2;(* arith *) napply daemon
1768                               ##] ##| #Hdis;@2;(* arith *) napply daemon ##]
1769             ##| ncut (valid_access m1 chunk b1 ofs); /2/; #Hval';
1770                 nlapply (Hnoover … eb1 Hb1 CP);
1771                 #Ha; nelim Ha; #Ha;
1772                 ##[ nelim Ha; #Ha;
1773                 ##[ nelim Ha; #Ha;
1774                 ##[ @1;@1;/2/
1775                 ##| nelim Hval'; nlapply (size_chunk_pos chunk); (* arith *) napply daemon ##]
1776                 ##| nelim Hval; nlapply (size_chunk_pos chunk'); (* arith *) napply daemon ##]
1777                 ##| nelim Hval'; nelim Hval;  (* arith *) napply daemon ##]
1778             ##]
1779         ##| #eb1;#Hofs1;#Hofs2;#Hofs3;#H; (* overlapping *)
1780             nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
1781             nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
1782             ncut (∃v2'. load chunk' m2' b2 (ofs' + delta) = Some ? v2');
1783             ##[ napply valid_access_load; napply (store_valid_access_1 … STORE2); napply (valid_access_inj … Hinj Hval); nrewrite > eb1; //
1784             ##| *;#v2';#LOAD2';
1785                 ncut (v2' = Vundef); ##[ napply (load_store_overlap … STORE2 … LOAD2'); (* arith *) napply daemon ##| ##]
1786                 #ev2'; @ v2'; @;//;
1787                 nrewrite > LOAD1 in H;#H; nwhd in H:(??%%); nrewrite > (grumpydestruct1 … H);
1788                 nrewrite > ev2';
1789                 napply val_inj_undef; ##]
1790         ##| #eb1;#Hofs;nrewrite < Hofs in Hval LOAD1 ⊢ %;#Hval;#LOAD1;#Hsize;#H; (* overlapping *)
1791             
1792             nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
1793             nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
1794             ncut (∃v2'. load chunk' m2' b2 (ofs + delta) = Some ? v2');
1795             ##[ napply valid_access_load; napply (store_valid_access_1 … STORE2); napply (valid_access_inj … Hinj Hval); nrewrite > eb1; //
1796             ##| *;#v2';#LOAD2';
1797                 ncut (v2' = Vundef); ##[ napply (load_store_mismatch … STORE2 … LOAD2' ?); napply sym_neq;// ##| ##]
1798                 #ev2'; @ v2'; @;//;
1799                 nrewrite > LOAD1 in H;#H; nwhd in H:(??%%); nrewrite > (grumpydestruct1 … H);
1800                 nrewrite > ev2';
1801                 napply val_inj_undef; ##]
1802         ##]
1803     ##]
1804##] nqed.
1805
1806ndefinition inj_offset_aligned ≝ λdelta: Z. λsize: Z.
1807  ∀chunk. size_chunk chunk ≤ size → (align_chunk chunk ∣ delta).
1808
1809nlemma alloc_parallel_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef.
1810  ∀mi,m1,m2,lo1,hi1,m1',b1,lo2,hi2,m2',b2,delta.
1811  mem_inj val_inj mi m1 m2 →
1812  alloc m1 lo1 hi1 = 〈m1', b1〉 →
1813  alloc m2 lo2 hi2 = 〈m2', b2〉 →
1814  mi b1 = Some ? 〈b2, delta〉 →
1815  lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 →
1816  inj_offset_aligned delta (hi1 - lo1) →
1817  mem_inj val_inj mi m1' m2'.
1818#val_inj;#val_inj_undef;
1819#mi;#m1;#m2;#lo1;#hi1;#m1';#b1;#lo2;#hi2;#m2';#b2;#delta;
1820#Hinj;#ALLOC1;#ALLOC2;#Hbinj;#Hlo;#Hhi;#Hal;
1821nwhd; #chunk;#b1';#ofs;#v;#b2';#delta';#Hbinj';#LOAD;
1822nlapply (valid_access_alloc_inv … m1 … ALLOC1 chunk b1' ofs ?); /2/;
1823*;
1824##[ #A;
1825    ncut (load chunk m1 b1' ofs = Some ? v);
1826    ##[ nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC1); /2/; ##]
1827    #LOAD0; nlapply (Hinj … Hbinj' LOAD0); *;#v2;*;#LOAD2;#VINJ;
1828    @ v2; @;
1829    ##[ nrewrite < LOAD2; napply (load_alloc_unchanged … ALLOC2);
1830        napply valid_access_valid_block; ##[ ##3: napply load_valid_access; ##]
1831        //
1832    ##| //
1833    ##]
1834##| *;*;#A;#B;#C;
1835    nrewrite > A in Hbinj' LOAD; #Hbinj';#LOAD;
1836    nrewrite > Hbinj in Hbinj'; #Hbinj'; nelim (grumpydestruct2 ?????? Hbinj');
1837    #eb2;#edelta; nrewrite < eb2; nrewrite < edelta;
1838    ncut (v = Vundef); ##[ napply (load_alloc_same … ALLOC1 … LOAD); ##]
1839    #ev; nrewrite > ev;
1840    ncut (∃v2. load chunk m2' b2 (ofs + delta) = Some ? v2);
1841    ##[ napply valid_access_load;
1842        napply (valid_access_alloc_same … ALLOC2);
1843        ##[ ##1,2: (*arith*) napply daemon;
1844        ##| (* arith using Hal *) napply daemon
1845        ##] ##]
1846    *;#v2;#LOAD2;
1847    ncut (v2 = Vundef); ##[ napply (load_alloc_same … ALLOC2 … LOAD2) ##]
1848    #ev2; nrewrite > ev2;
1849    @ Vundef; @; //;
1850##] nqed.
1851
1852nlemma alloc_right_inj: ∀val_inj.
1853  ∀mi,m1,m2,lo,hi,b2,m2'.
1854  mem_inj val_inj mi m1 m2 →
1855  alloc m2 lo hi = 〈m2', b2〉 →
1856  mem_inj val_inj mi m1 m2'.
1857#val_inj;
1858#mi;#m1;#m2;#lo;#hi;#b2;#m2';
1859#Hinj;#ALLOC;
1860nwhd; #chunk; #b1; #ofs; #v1; #b2'; #delta; #Hbinj; #LOAD;
1861nlapply (Hinj … Hbinj LOAD); *; #v2;*;#LOAD2;#VINJ;
1862@ v2; @; //;
1863ncut (valid_block m2 b2');
1864  ##[ napply (valid_access_valid_block ? chunk ? (ofs + delta)); /2/ ##]
1865#Hval;
1866nrewrite < LOAD2; napply (load_alloc_unchanged … ALLOC … Hval);
1867nqed.
1868
1869(*
1870Hypothesis val_inj_undef_any:
1871  ∀mi,v. val_inj mi Vundef v.
1872*)
1873
1874nlemma alloc_left_unmapped_inj: ∀val_inj.
1875  ∀mi,m1,m2,lo,hi,b1,m1'.
1876  mem_inj val_inj mi m1 m2 →
1877  alloc m1 lo hi = 〈m1', b1〉 →
1878  mi b1 = None ? →
1879  mem_inj val_inj mi m1' m2.
1880#val_inj;
1881#mi;#m1;#m2;#lo;#hi;#b1;#m1';
1882#Hinj;#ALLOC;#Hbinj;
1883nwhd;  #chunk; #b1'; #ofs; #v1; #b2'; #delta; #Hbinj'; #LOAD;
1884nlapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
1885*;
1886##[ #A;
1887  napply (Hinj … Hbinj' );
1888  nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC); /2/;
1889##| *;*;#A;#B;#C;
1890  nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD;
1891  nrewrite > Hbinj in Hbinj'; #bad; ndestruct;
1892##] nqed.
1893
1894nlemma alloc_left_mapped_inj: ∀val_inj.∀val_inj_undef_any:∀mi,v. val_inj mi Vundef v.
1895  ∀mi,m1,m2,lo,hi,b1,m1',b2,delta.
1896  mem_inj val_inj mi m1 m2 →
1897  alloc m1 lo hi = 〈m1', b1〉 →
1898  mi b1 = Some ? 〈b2, delta〉 →
1899  valid_block m2 b2 →
1900  low_bound m2 b2 ≤ lo + delta → hi + delta ≤ high_bound m2 b2 →
1901  inj_offset_aligned delta (hi - lo) →
1902  mem_inj val_inj mi m1' m2.
1903#val_inj;#val_inj_undef_any;
1904#mi;#m1;#m2;#lo;#hi;#b1;#m1';#b2;#delta;
1905#Hinj;#ALLOC;#Hbinj;#Hval;#Hlo;#Hhi;#Hal;
1906nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
1907nlapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
1908*;
1909##[ #A;
1910    napply (Hinj … Hbinj');
1911    nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC); /2/;
1912##| *;*;#A;#B;*;#C;#D;
1913    nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD; nrewrite > Hbinj in Hbinj';
1914    #Hbinj'; (* XXX ndestruct normalizes too much here *) nelim (grumpydestruct2 ?????? Hbinj'); #eb2; #edelta;
1915    nrewrite < eb2; nrewrite < edelta;
1916    ncut (v1 = Vundef); ##[ napply (load_alloc_same … ALLOC … LOAD) ##]
1917    #ev1; nrewrite > ev1;
1918    ncut (∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2);
1919    ##[ napply valid_access_load; @; //;
1920      ##[ (* arith *) napply daemon
1921      ##| (* arith *) napply daemon
1922      ##| (* arith *) napply daemon
1923      ##]
1924    ##]
1925    *;#v2;#LOAD2; @ v2; @; //;
1926##] nqed.
1927
1928nlemma free_parallel_inj: ∀val_inj.
1929  ∀mi,m1,m2,b1,b2,delta.
1930  mem_inj val_inj mi m1 m2 →
1931  mi b1 = Some ? 〈b2, delta〉 →
1932  (∀b,delta'. mi b = Some ? 〈b2, delta'〉 → b = b1) →
1933  mem_inj val_inj mi (free m1 b1) (free m2 b2).
1934#val_inj;
1935#mi;#m1;#m2;#b1;#b2;#delta; #Hinj;#Hb1inj;#Hbinj;
1936nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
1937nlapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A;#B;
1938ncut (load chunk m1 b1' ofs = Some ? v1);
1939##[ nrewrite < LOAD; napply sym_eq; napply load_free; napply B ##] #LOAD';
1940nelim (Hinj … Hbinj' LOAD'); #v2;*;#LOAD2;#INJ;
1941@ v2;@;
1942##[ nrewrite < LOAD2; napply load_free;
1943    napply nmk; #e; napply (absurd ?? B);
1944    nrewrite > e in Hbinj'; #Hbinj'; napply (Hbinj ?? Hbinj');
1945##| //
1946##] nqed.
1947
1948nlemma free_left_inj: ∀val_inj.
1949  ∀mi,m1,m2,b1.
1950  mem_inj val_inj mi m1 m2 →
1951  mem_inj val_inj mi (free m1 b1) m2.
1952#val_inj;#mi;#m1;#m2;#b1;#Hinj;
1953nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
1954nlapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A;#B;
1955napply (Hinj … Hbinj');
1956nrewrite < LOAD; napply sym_eq; napply load_free; napply B;
1957nqed.
1958
1959nlemma free_list_left_inj: ∀val_inj.
1960  ∀mi,bl,m1,m2.
1961  mem_inj val_inj mi m1 m2 →
1962  mem_inj val_inj mi (free_list m1 bl) m2.
1963#val_inj;#mi;#bl;nelim bl;
1964##[ nwhd in ⊢ (?→?→?→???%?); //
1965##| #h;#t;#IH; #m1;#m2;#H; nrewrite > (unfold_free_list m1 h t);
1966    napply free_left_inj; napply IH; //
1967##] nqed.
1968
1969nlemma free_right_inj: ∀val_inj.
1970  ∀mi,m1,m2,b2.
1971  mem_inj val_inj mi m1 m2 →
1972  (∀b1,delta,chunk,ofs.
1973   mi b1 = Some ? 〈b2, delta〉 → ¬(valid_access m1 chunk b1 ofs)) →
1974  mem_inj val_inj mi m1 (free m2 b2).
1975#val_inj;#mi;#m1;#m2;#b2; #Hinj; #Hinval;
1976nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
1977ncut (b2' ≠ b2);
1978##[ napply nmk; #e; nrewrite > e in Hbinj'; #Hbinj';
1979    napply (absurd ?? (Hinval … Hbinj')); napply (load_valid_access … LOAD); ##]
1980#ne; nlapply (Hinj … Hbinj' LOAD); *;#v2;*;#LOAD2;#INJ;
1981@ v2; @; //;
1982nrewrite < LOAD2; napply load_free; napply ne;
1983nqed.
1984
1985nlemma valid_pointer_inj: ∀val_inj.
1986  ∀mi,m1,m2,b1,ofs,b2,delta.
1987  mi b1 = Some ? 〈b2, delta〉 →
1988  mem_inj val_inj mi m1 m2 →
1989  valid_pointer m1 b1 ofs = true →
1990  valid_pointer m2 b2 (ofs + delta) = true.
1991#val_inj;#mi;#m1;#m2;#b1;#ofs;#b2;#delta;#Hbinj;#Hinj;#VALID;
1992nlapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval;
1993napply (proj2 ?? (valid_pointer_valid_access ???));
1994napply (valid_access_inj … Hval); //;
1995nqed.
1996
1997(*
1998End GENERIC_INJECT.
1999*)
2000(* ** Store extensions *)
2001
2002(* A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
2003  by increasing the sizes of the memory blocks of [m1] (decreasing
2004  the low bounds, increasing the high bounds), while still keeping the
2005  same contents for block offsets that are valid in [m1]. *)
2006
2007ndefinition inject_id : meminj ≝ λb. Some ? 〈b, OZ〉.
2008
2009ndefinition val_inj_id ≝ λmi: meminj. λv1,v2: val. v1 = v2.
2010
2011ndefinition extends ≝ λm1,m2: mem.
2012  nextblock m1 = nextblock m2 ∧ mem_inj val_inj_id inject_id m1 m2.
2013
2014ntheorem extends_refl:
2015  ∀m: mem. extends m m.
2016#m;@;//;
2017nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;nnormalize in ⊢ (%→?);#H;
2018(* XXX: ndestruct makes the goal unreadable *) nelim (grumpydestruct2 ?????? H); #eb1;#edelta;#LOAD;
2019@ v1; @;
2020##[ nrewrite < edelta; nrewrite > (Zplus_z_OZ ofs); //;
2021##| //
2022##] nqed.
2023
2024ntheorem alloc_extends:
2025  ∀m1,m2,m1',m2': mem. ∀lo1,hi1,lo2,hi2: Z. ∀b1,b2: block.
2026  extends m1 m2 →
2027  lo2 ≤ lo1 → hi1 ≤ hi2 →
2028  alloc m1 lo1 hi1 = 〈m1', b1〉 →
2029  alloc m2 lo2 hi2 = 〈m2', b2〉 →
2030  b1 = b2 ∧ extends m1' m2'.
2031#m1;#m2;#m1';#m2';#lo1;#hi1;#lo2;#hi2;#b1;#b2;
2032*;#Hnext;#Hinj;#Hlo;#Hhi;#ALLOC1;#ALLOC2;
2033ncut (b1 = b2);
2034##[ napply (transitive_eq … (nextblock m1)); ##[ napply (alloc_result … ALLOC1);
2035    ##| napply sym_eq; nrewrite > Hnext; napply (alloc_result … ALLOC2) ##] ##]
2036#eb; nrewrite < eb in ALLOC2 ⊢ %; #ALLOC2; @; //; @;
2037##[ nrewrite > (nextblock_alloc … ALLOC1);
2038    nrewrite > (nextblock_alloc … ALLOC2);
2039    //;
2040##| napply (alloc_parallel_inj ??????????????? ALLOC1 ALLOC2 ????);
2041  ##[ ##1,4: nnormalize; //;
2042  ##| ##3,5,6: //
2043  ##| ##7: nwhd; #chunk;#Hsize; (* divides 0 *) napply daemon
2044  ##]
2045##] nqed.
2046
2047ntheorem free_extends:
2048  ∀m1,m2: mem. ∀b: block.
2049  extends m1 m2 →
2050  extends (free m1 b) (free m2 b).
2051#m1;#m2;#b;*;#Hnext;#Hinj; @;
2052##[ nnormalize; //;
2053##| napply (free_parallel_inj … Hinj);
2054  ##[ ##2: //;
2055  ##| ##3: nnormalize; #b';#delta;#ee; ndestruct; //
2056  ##]
2057##] nqed.
2058
2059ntheorem load_extends:
2060  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val.
2061  extends m1 m2 →
2062  load chunk m1 b ofs = Some ? v →
2063  load chunk m2 b ofs = Some ? v.
2064#chunk;#m1;#m2;#b;#ofs;#v;
2065*;#Hnext;#Hinj;#LOAD;
2066nlapply (Hinj … LOAD); ##[ nnormalize; // ##| ##2,3: ##]
2067*;#v2;*; nrewrite > (Zplus_z_OZ ofs); #LOAD2;#EQ;nwhd in EQ;
2068//;
2069nqed.
2070
2071ntheorem store_within_extends:
2072  ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val.
2073  extends m1 m2 →
2074  store chunk m1 b ofs v = Some ? m1' →
2075  ∃m2'. store chunk m2 b ofs v = Some ? m2' ∧ extends m1' m2'.
2076#chunk;#m1;#m2;#m1';#b;#ofs;#v;*;#Hnext;#Hinj;#STORE1;
2077nlapply (store_mapped_inj … Hinj ?? STORE1 ?);
2078##[ ##1,2,7: nnormalize; //
2079##| (* TODO: unfolding, etc ought to tidy this up *)
2080    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neb;#Hinj1;#Hinj2;
2081    nnormalize in Hinj1 Hinj2; @1; @1; @1; ndestruct; //
2082##| ##4,5,6: ##skip
2083##]
2084*;#m2';*;#STORE;#MINJ;
2085@ m2'; @; nrewrite > (Zplus_z_OZ ofs) in STORE; #STORE; //;
2086@;
2087##[ nrewrite > (nextblock_store … STORE1);
2088    nrewrite > (nextblock_store … STORE);
2089    //
2090##| //
2091##] nqed.
2092
2093ntheorem store_outside_extends:
2094  ∀chunk: memory_chunk. ∀m1,m2,m2': mem. ∀b: block. ∀ofs: Z. ∀v: val.
2095  extends m1 m2 →
2096  ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs →
2097  store chunk m2 b ofs v = Some ? m2' →
2098  extends m1 m2'.
2099#chunk;#m1;#m2;#m2';#b;#ofs;#v;*;#Hnext;#Hinj;#Houtside;#STORE; @;
2100##[ nrewrite > (nextblock_store … STORE); //
2101##| napply (store_outside_inj … STORE); //;
2102    #b';#delta;#einj;nnormalize in einj; ndestruct;
2103    nelim Houtside;
2104    ##[ #lo;@ 2; nrewrite > (Zplus_z_OZ ?); /2/
2105    ##| #hi;@ 1;  nrewrite > (Zplus_z_OZ ?); /2/
2106    ##]
2107##] nqed.
2108
2109ntheorem valid_pointer_extends:
2110  ∀m1,m2,b,ofs.
2111  extends m1 m2 → valid_pointer m1 b ofs = true →
2112  valid_pointer m2 b ofs = true.
2113#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
2114nrewrite < (Zplus_z_OZ ofs);
2115napply (valid_pointer_inj … Hinj VALID); //;
2116nqed.
2117
2118
2119(* * The ``less defined than'' relation over memory states *)
2120
2121(* A memory state [m1] is less defined than [m2] if, for all addresses,
2122  the value [v1] read in [m1] at this address is less defined than
2123  the value [v2] read in [m2], that is, either [v1 = v2] or [v1 = Vundef]. *)
2124
2125ndefinition val_inj_lessdef ≝ λmi: meminj. λv1,v2: val.
2126  Val_lessdef v1 v2.
2127
2128ndefinition lessdef ≝ λm1,m2: mem.
2129  nextblock m1 = nextblock m2 ∧
2130  mem_inj val_inj_lessdef inject_id m1 m2.
2131
2132nlemma lessdef_refl:
2133  ∀m. lessdef m m.
2134#m; @; //;
2135nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;#H;#LOAD;
2136nwhd in H:(??%?); nelim (grumpydestruct2 ?????? H); #eb1; #edelta;
2137@ v1; @; //;
2138nqed.
2139
2140nlemma load_lessdef:
2141  ∀m1,m2,chunk,b,ofs,v1.
2142  lessdef m1 m2 → load chunk m1 b ofs = Some ? v1 →
2143  ∃v2. load chunk m2 b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
2144#m1;#m2;#chunk;#b;#ofs;#v1;*;#Hnext;#Hinj;#LOAD0;
2145nlapply (Hinj … LOAD0); ##[ nwhd in ⊢ (??%?); // ##| ##2,3:##skip ##]
2146*;#v2;*;#LOAD;#INJ; @ v2; @;//;
2147nqed.
2148
2149nlemma loadv_lessdef:
2150  ∀m1,m2,chunk,addr1,addr2,v1.
2151  lessdef m1 m2 → Val_lessdef addr1 addr2 →
2152  loadv chunk m1 addr1 = Some ? v1 →
2153  ∃v2. loadv chunk m2 addr2 = Some ? v2 ∧ Val_lessdef v1 v2.
2154#m1;#m2;#chunk;#addr1;#addr2;#v1;#H;#H0;#LOAD;
2155ninversion H0;
2156##[ #v; #e1;#e2; nrewrite > e1 in LOAD; ncases v;
2157    ##[ nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
2158    ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
2159    ##| #b';#off; napply load_lessdef; //
2160    ##]
2161##| #v;#e;nrewrite > e in LOAD; #LOAD; nwhd in LOAD:(??%?); ndestruct;
2162##] nqed.
2163
2164nlemma store_lessdef:
2165  ∀m1,m2,chunk,b,ofs,v1,v2,m1'.
2166  lessdef m1 m2 → Val_lessdef v1 v2 →
2167  store chunk m1 b ofs v1 = Some ? m1' →
2168  ∃m2'. store chunk m2 b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
2169#m1;#m2;#chunk;#b;#ofs;#v1;#v2;#m1';
2170*;#Hnext;#Hinj;#Hvless;#STORE0;
2171nlapply (store_mapped_inj … Hinj … STORE0 ?);
2172##[ #chunk';#Hsize;nwhd;napply load_result_lessdef;napply Hvless
2173##| nwhd in ⊢ (??%?); //
2174##| nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neq;
2175    nwhd in ⊢ ((??%?)→(??%?)→?); #e1; #e2; ndestruct;
2176    @;@;@;//
2177##| ##7: #mi; nwhd; //;
2178##| ##8: *;#m2';*;#STORE;#MINJ;
2179         @ m2';@; /2/;
2180         @;
2181         nrewrite > (nextblock_store … STORE0);
2182         nrewrite > (nextblock_store … STORE);
2183         //;
2184##] nqed.
2185
2186nlemma storev_lessdef:
2187  ∀m1,m2,chunk,addr1,v1,addr2,v2,m1'.
2188  lessdef m1 m2 → Val_lessdef addr1 addr2 → Val_lessdef v1 v2 →
2189  storev chunk m1 addr1 v1 = Some ? m1' →
2190  ∃m2'. storev chunk m2 addr2 v2 = Some ? m2' ∧ lessdef m1' m2'.
2191#m1;#m2;#chunk;#addr1;#v1;#addr2;#v2;#m1';
2192#Hmless;#Haless;#Hvless;#STORE;
2193ninversion Haless;
2194##[ #v; #e1;#e2; nrewrite > e1 in STORE; ncases v;
2195    ##[ nwhd in ⊢ ((??%?)→?); #H'; napply False_ind; ndestruct;
2196    ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
2197    ##| #b';#off; napply store_lessdef; //
2198    ##]
2199##| #v;#e;nrewrite > e in STORE; #STORE; nwhd in STORE:(??%?); ndestruct
2200##] nqed.
2201
2202nlemma alloc_lessdef:
2203  ∀m1,m2,lo,hi,b1,m1',b2,m2'.
2204  lessdef m1 m2 → alloc m1 lo hi = 〈m1', b1〉 → alloc m2 lo hi = 〈m2', b2〉 →
2205  b1 = b2 ∧ lessdef m1' m2'.
2206#m1;#m2;#lo;#hi;#b1;#m1';#b2;#m2';
2207*;#Hnext;#Hinj;#ALLOC1;#ALLOC2;
2208ncut (b1 = b2);
2209##[ nrewrite > (alloc_result … ALLOC1); nrewrite > (alloc_result … ALLOC2); //
2210##]
2211#e; nrewrite < e in ALLOC2 ⊢ %; #ALLOC2; @; //;
2212@;
2213##[ nrewrite > (nextblock_alloc … ALLOC1);
2214    nrewrite > (nextblock_alloc … ALLOC2);
2215    //
2216##| napply (alloc_parallel_inj … Hinj ALLOC1 ALLOC2);
2217##[ //
2218##| ##3: nwhd in ⊢ (??%?); //
2219##| ##4,5: //;
2220##| ##6: nwhd; #chunk;#_; ncases chunk;//;
2221##] nqed.
2222
2223nlemma free_lessdef:
2224  ∀m1,m2,b. lessdef m1 m2 → lessdef (free m1 b) (free m2 b).
2225#m1;#m2;#b;*;#Hnext;#Hinj; @;
2226##[ nwhd in ⊢ (??%%); //
2227##| napply (free_parallel_inj … Hinj); //;
2228    #b';#delta;#H; nwhd in H:(??%?); nelim (grumpydestruct2 ?????? H); //
2229##] nqed.
2230
2231nlemma free_left_lessdef:
2232  ∀m1,m2,b.
2233  lessdef m1 m2 → lessdef (free m1 b) m2.
2234#m1;#m2;#b;*;#Hnext;#Hinj;@;
2235nrewrite < Hnext; //;
2236napply free_left_inj; //;
2237nqed.
2238
2239nlemma free_right_lessdef:
2240  ∀m1,m2,b.
2241  lessdef m1 m2 → low_bound m1 b ≥ high_bound m1 b →
2242  lessdef m1 (free m2 b).
2243#m1;#m2;#b;*;#Hnext;#Hinj;#Hbounds;
2244@; nrewrite > Hnext; //;
2245napply free_right_inj; //;
2246#b1;#delta;#chunk;#ofs;#H; nwhd in H:(??%?); ndestruct;
2247napply nmk; *; #H1;#H2;#H3;#H4;
2248(* arith H2 and H3 contradict Hbounds. *) napply daemon;
2249nqed.
2250
2251nlemma valid_block_lessdef:
2252  ∀m1,m2,b. lessdef m1 m2 → valid_block m1 b → valid_block m2 b.
2253#m1;#m2;#b;*;#Hnext;#Hinj;
2254 nrewrite > (unfold_valid_block …); nrewrite > (unfold_valid_block m2 b);
2255 //; nqed.
2256
2257nlemma valid_pointer_lessdef:
2258  ∀m1,m2,b,ofs.
2259  lessdef m1 m2 → valid_pointer m1 b ofs = true → valid_pointer m2 b ofs = true.
2260#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
2261nrewrite < (Zplus_z_OZ ofs); napply (valid_pointer_inj … Hinj VALID); //;
2262nqed.
2263
2264
2265(* ** Memory injections *)
2266
2267(* A memory injection [f] is a function from addresses to either [None]
2268  or [Some] of an address and an offset.  It defines a correspondence
2269  between the blocks of two memory states [m1] and [m2]:
2270- if [f b = None], the block [b] of [m1] has no equivalent in [m2];
2271- if [f b = Some〈b', ofs〉], the block [b] of [m2] corresponds to
2272  a sub-block at offset [ofs] of the block [b'] in [m2].
2273*)
2274
2275(* A memory injection defines a relation between values that is the
2276  identity relation, except for pointer values which are shifted
2277  as prescribed by the memory injection. *)
2278
2279ninductive val_inject (mi: meminj): val → val → Prop :=
2280  | val_inject_int:
2281      ∀i. val_inject mi (Vint i) (Vint i)
2282  | val_inject_float:
2283      ∀f. val_inject mi (Vfloat f) (Vfloat f)
2284  | val_inject_ptr:
2285      ∀b1,ofs1,b2,ofs2,x.
2286      mi b1 = Some ? 〈b2, x〉 →
2287      ofs2 = add ofs1 (repr x) →
2288      val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)
2289  | val_inject_undef: ∀v.
2290      val_inject mi Vundef v.
2291(*
2292Hint Resolve val_inject_int val_inject_float val_inject_ptr
2293             val_inject_undef.
2294*)
2295ninductive val_list_inject (mi: meminj): list val → list val→ Prop:=
2296  | val_nil_inject :
2297      val_list_inject mi (nil ?) (nil ?)
2298  | val_cons_inject : ∀v,v',vl,vl'.
2299      val_inject mi v v' → val_list_inject mi vl vl'→
2300      val_list_inject mi (v :: vl) (v' :: vl'). 
2301(*
2302Hint Resolve val_nil_inject val_cons_inject.
2303*)
2304(* A memory state [m1] injects into another memory state [m2] via the
2305  memory injection [f] if the following conditions hold:
2306- loads in [m1] must have matching loads in [m2] in the sense
2307  of the [mem_inj] predicate;
2308- unallocated blocks in [m1] must be mapped to [None] by [f];
2309- if [f b = Some〈b', delta〉], [b'] must be valid in [m2];
2310- distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2];
2311- the sizes of [m2]'s blocks are representable with signed machine integers;
2312- the offsets [delta] are representable with signed machine integers.
2313*)
2314
2315nrecord mem_inject (f: meminj) (m1,m2: mem) : Prop ≝
2316  {
2317    mi_inj:
2318      mem_inj val_inject f m1 m2;
2319    mi_freeblocks:
2320      ∀b. ¬(valid_block m1 b) → f b = None ?;
2321    mi_mappedblocks:
2322      ∀b,b',delta. f b = Some ? 〈b', delta〉 → valid_block m2 b';
2323    mi_no_overlap:
2324      meminj_no_overlap f m1;
2325    mi_range_1:
2326      ∀b,b',delta.
2327      f b = Some ? 〈b', delta〉 →
2328      min_signed ≤ delta ∧ delta ≤ max_signed;
2329    mi_range_2:
2330      ∀b,b',delta.
2331      f b = Some ? 〈b', delta〉 →
2332      delta = 0 ∨ (min_signed ≤ low_bound m2 b' ∧ high_bound m2 b' ≤ max_signed)
2333  }.
2334
2335
2336(* The following lemmas establish the absence of machine integer overflow
2337  during address computations. *)
2338
2339nlemma address_inject:
2340  ∀f,m1,m2,chunk,b1,ofs1,b2,delta.
2341  mem_inject f m1 m2 →
2342  valid_access m1 chunk b1 (signed ofs1) →
2343  f b1 = Some ? 〈b2, delta〉 →
2344  signed (add ofs1 (repr delta)) = signed ofs1 + delta.
2345#f;#m1;#m2;#chunk;#b1;#ofs1;#b2;#delta;
2346*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2347#Hvalid;#Hb1inj;
2348nelim (mi_range_2 ??? Hb1inj);
2349##[ (* delta = 0 *)
2350    #edelta; nrewrite > edelta;
2351    nrewrite > (?:repr O = zero); ##[ ##2: // ##]
2352    nrewrite > (add_zero ?);
2353    nrewrite > (Zplus_z_OZ …);
2354    //;
2355##| (* delta ≠ 0 *)
2356    #Hrange; nrewrite > (add_signed ??);
2357    nrewrite > (signed_repr delta ?);
2358    ##[ nrewrite > (signed_repr ??);
2359      ##[ //
2360      ##| ncut (valid_access m2 chunk b2 (signed ofs1 + delta));
2361        ##[ napply (valid_access_inj … Hvalid); //;
2362        ##| *; #_; #Hlo; #Hhi; #_; (* arith *) napply daemon
2363        ##]
2364      ##]
2365    ##| /2/
2366    ##]
2367##] nqed.
2368
2369nlemma valid_pointer_inject_no_overflow:
2370  ∀f,m1,m2,b,ofs,b',x.
2371  mem_inject f m1 m2 →
2372  valid_pointer m1 b (signed ofs) = true →
2373  f b = Some ? 〈b', x〉 →
2374  min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed.
2375#f;#m1;#m2;#b;#ofs;#b';#x;
2376*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2377#Hvalid;#Hb1inj;
2378nlapply ((proj1 ?? (valid_pointer_valid_access ???)) Hvalid); #Hvalid';
2379ncut (valid_access m2 Mint8unsigned b' (signed ofs + x));
2380##[ napply (valid_access_inj … Hvalid'); // ##]
2381*; nrewrite > (?:size_chunk Mint8unsigned = 1); ##[ ##2: // ##] #_; #Hlo; #Hhi; #_;
2382nrewrite > (signed_repr ??); ##[ ##2: /2/; ##]
2383nlapply (mi_range_2 … Hb1inj); *;
2384##[ #ex; nrewrite > ex; nrewrite > (Zplus_z_OZ ?); napply signed_range;
2385##| (* arith *) napply daemon
2386##] nqed.
2387
2388(* XXX: should use ndestruct, but reduces large definitions *)
2389nremark vptr_eq: ∀b,b',i,i'. Vptr b i = Vptr b' i' → b = b' ∧ i = i'.
2390#b b' i i' e; ndestruct; /2/; nqed.
2391
2392nlemma valid_pointer_inject:
2393  ∀f,m1,m2,b,ofs,b',ofs'.
2394  mem_inject f m1 m2 →
2395  valid_pointer m1 b (signed ofs) = true →
2396  val_inject f (Vptr b ofs) (Vptr b' ofs') →
2397  valid_pointer m2 b' (signed ofs') = true.
2398#f;#m1;#m2;#b;#ofs;#b';#ofs';
2399#Hinj; #Hvalid; #Hvinj; ninversion Hvinj;
2400##[ ##1,2,4: #x;#H;ndestruct; ##]
2401#b0;#i;#b0';#i';#delta;#Hb;#Hi';#eptr;#eptr';
2402nrewrite < (proj1 … (vptr_eq ???? eptr)) in Hb; nrewrite < (proj1 … (vptr_eq ???? eptr'));
2403nrewrite < (proj2 … (vptr_eq ???? eptr)) in Hi'; nrewrite < (proj2 … (vptr_eq ???? eptr'));
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 very similar *)
2513##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
2514    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
2515    ##[ ##2,4: nwhd in ⊢ (??%%); nrewrite > Hz; @
2516    ##| ##1,3: nwhd in ⊢ (??%%); nrewrite > (sign_ext_equal_if_zero_equal … Hz);
2517        @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
2518    ##]
2519##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
2520    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
2521    ##[ ##2,4: nwhd in ⊢ (??%%); nrewrite > Hz; @
2522    ##| ##1,3: nwhd in ⊢ (??%%); nrewrite > (sign_ext_equal_if_zero_equal … Hz);
2523        @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
2524    ##]
2525
2526##| #f;#f';#float;#echunk;nrewrite > echunk;#_;#_;
2527    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
2528    ##[ @4; ##| nrewrite > float; @2 ##]
2529##] nqed.
2530
2531nlemma store_mapped_inject_1 :
2532  ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2.
2533  mem_inject f m1 m2 →
2534  store chunk m1 b1 ofs v1 = Some ? n1 →
2535  f b1 = Some ? 〈b2, delta〉 →
2536  val_content_inject f chunk v1 v2 →
2537  ∃n2.
2538    store chunk m2 b2 (ofs + delta) v2 = Some ? n2
2539    ∧ mem_inject f n1 n2.
2540#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;#b2;#delta;#v2;
2541*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2542#STORE1; #INJb1; #Hvcinj;
2543nlapply (store_mapped_inj … mi_inj mi_no_overlap INJb1 STORE1 ?); //;
2544##[ #chunk';#Hchunksize;napply (load_result_inject … chunk …);//;
2545##| ##skip ##]
2546*;#n2;*;#STORE;#MINJ;
2547@ n2; @; //; @;
2548##[ (* inj *) //
2549##| (* freeblocks *) #b;#notvalid; napply mi_freeblocks;
2550    napply (not_to_not ??? notvalid); napply (store_valid_block_1 … STORE1);
2551##| (* mappedblocks *) #b;#b';#delta';#INJb';napply (store_valid_block_1 … STORE);
2552    /2/;
2553##| (* no_overlap *) nwhd; #b1';#b1'';#delta1';#b2';#b2'';#delta2';#neqb';
2554    #fb1';#fb2';
2555    nrewrite > (low_bound_store … STORE1 ?);  nrewrite > (low_bound_store … STORE1 ?);
2556    nrewrite > (high_bound_store … STORE1 ?);  nrewrite > (high_bound_store … STORE1 ?);
2557    napply mi_no_overlap; //;
2558##| (* range *) /2/;
2559##| (* range 2 *) #b;#b';#delta';#INJb;
2560    nrewrite > (low_bound_store … STORE ?);
2561    nrewrite > (high_bound_store … STORE ?);
2562    napply mi_range_2; //;
2563##] nqed.
2564
2565nlemma store_mapped_inject:
2566  ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2.
2567  mem_inject f m1 m2 →
2568  store chunk m1 b1 ofs v1 = Some ? n1 →
2569  f b1 = Some ? 〈b2, delta〉 →
2570  val_inject f v1 v2 →
2571  ∃n2.
2572    store chunk m2 b2 (ofs + delta) v2 = Some ? n2
2573    ∧ mem_inject f n1 n2.
2574#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;#b2;#delta;#v2;
2575#MINJ;#STORE;#INJb1;#Hvalinj;napply (store_mapped_inject_1 … STORE);//;
2576napply val_content_inject_base;//;
2577nqed.
2578
2579nlemma store_unmapped_inject:
2580  ∀f,chunk,m1,b1,ofs,v1,n1,m2.
2581  mem_inject f m1 m2 →
2582  store chunk m1 b1 ofs v1 = Some ? n1 →
2583  f b1 = None ? →
2584  mem_inject f n1 m2.
2585#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;
2586*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2587#STORE;#INJb1;@;
2588##[ (* inj *) napply (store_unmapped_inj … STORE); //
2589##| (* freeblocks *) #b;#notvalid; napply mi_freeblocks;
2590    napply (not_to_not ??? notvalid); napply (store_valid_block_1 … STORE);
2591##| (* mappedblocks *) #b;#b';#delta;#INJb; napply mi_mappedblock; //;
2592##| (* no_overlap *) nwhd; #b1';#b1'';#delta1';#b2';#b2'';#delta2';#neqb';
2593    #fb1';#fb2';
2594    nrewrite > (low_bound_store … STORE ?);  nrewrite > (low_bound_store … STORE ?);
2595    nrewrite > (high_bound_store … STORE ?);  nrewrite > (high_bound_store … STORE ?);
2596    napply mi_no_overlap; //;
2597##| (* range *) /2/
2598##| /2/
2599##] nqed.
2600
2601nlemma storev_mapped_inject_1:
2602  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
2603  mem_inject f m1 m2 →
2604  storev chunk m1 a1 v1 = Some ? n1 →
2605  val_inject f a1 a2 →
2606  val_content_inject f chunk v1 v2 →
2607  ∃n2.
2608    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2.
2609#f;#chunk;#m1;#a1;#v1;#n1;#m2;#a2;#v2;
2610#MINJ;#STORE;#Hvinj;#Hvcinj;
2611ninversion Hvinj;
2612##[ ##1,2,4:#x;#ex1;#ex2;nrewrite > ex1 in STORE; nwhd in ⊢ ((??%?)→?); #H;
2613    napply False_ind; ndestruct; ##]
2614#b;#ofs;#b';#ofs';#delta;#INJb;#Hofs;#ea1;#ea2;
2615nrewrite > Hofs; nrewrite > ea1 in STORE; #STORE;
2616nlapply (store_mapped_inject_1 … MINJ STORE … INJb Hvcinj);
2617nrewrite < (?:signed (add ofs (repr delta)) = signed ofs + delta); //;
2618napply (address_inject … chunk … MINJ ? INJb);
2619napply (store_valid_access_3 … STORE);
2620nqed.
2621
2622nlemma storev_mapped_inject:
2623  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
2624  mem_inject f m1 m2 →
2625  storev chunk m1 a1 v1 = Some ? n1 →
2626  val_inject f a1 a2 →
2627  val_inject f v1 v2 →
2628  ∃n2.
2629    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2.
2630#f;#chunk;#m1;#a1;#v1;#n1;#m2;#a2;#v2; #MINJ;#STOREV;#Hvinj;#Hvinj';
2631napply (storev_mapped_inject_1 … STOREV); /2/;
2632nqed.
2633
2634(* Relation between injections and [free] *)
2635
2636nlemma meminj_no_overlap_free:
2637  ∀mi,m,b.
2638  meminj_no_overlap mi m →
2639  meminj_no_overlap mi (free m b).
2640#mi;#m;#b;#H;nwhd;#b1;#b1';#delta1;#b2;#b2';#delta2;#Hne;#mi1;#mi2;
2641ncut (low_bound (free m b) b ≥ high_bound (free m b) b);
2642##[ nrewrite > (low_bound_free_same …); nrewrite > (high_bound_free_same …);// ##]
2643#Hbounds;
2644ncases (decidable_eq_Z b1 b);#e1; ##[ nrewrite > e1 in Hne mi1 ⊢ %;#Hne;#mi1;##]
2645ncases (decidable_eq_Z b2 b);#e2; ##[ ##1,3: nrewrite > e2 in Hne mi2 ⊢ %;#Hne;#mi2;##]
2646##[ napply False_ind; nelim Hne; /2/
2647##| @;@2;//;
2648##| @;@;@2;//
2649##| nrewrite > (low_bound_free …);//; nrewrite > (low_bound_free …);//;
2650    nrewrite > (high_bound_free …);//; nrewrite > (high_bound_free …);//;
2651    /2/;
2652##] nqed.
2653
2654nlemma meminj_no_overlap_free_list:
2655  ∀mi,m,bl.
2656  meminj_no_overlap mi m →
2657  meminj_no_overlap mi (free_list m bl).
2658#mi;#m;#bl; nelim bl;
2659##[ #H; nwhd in ⊢ (??%); //
2660##| #h;#t; #IH; #H; napply meminj_no_overlap_free; napply IH; //
2661##] nqed.
2662
2663nlemma free_inject:
2664  ∀f,m1,m2,l,b.
2665  (∀b1,delta. f b1 = Some ? 〈b, delta〉 → in_list ? b1 l) →
2666  mem_inject f m1 m2 →
2667  mem_inject f (free_list m1 l) (free m2 b).
2668#f;#m1;#m2;#l;#b;#mappedin;
2669*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2670@;
2671##[ (* inj *)
2672    napply free_right_inj; ##[ napply free_list_left_inj; //; ##]
2673    #b1;#delta;#chunk;#ofs;#INJb1; napply nmk; #Hvalid;
2674    nelim (valid_access_free_list_inv … Hvalid); #b1ni; #Haccess;
2675    napply (absurd ? (mappedin ?? INJb1) b1ni);
2676##| (* freeblocks *)
2677    #b';#notvalid; napply mi_freeblocks; napply (not_to_not ??? notvalid);
2678    #H; napply valid_block_free_list_1; //
2679##| (* mappedblocks *)
2680    #b1;#b1';#delta;#INJb1; napply valid_block_free_1; /2/
2681##| (* overlap *)
2682    napply meminj_no_overlap_free_list; //
2683##| (* range *)
2684    /2/
2685##| #b1;#b2;#delta;#INJb1; ncases (decidable_eq_Z b2 b); #eb;
2686    ##[ nrewrite > eb;
2687        nrewrite > (low_bound_free_same ??); nrewrite > (high_bound_free_same ??);
2688        @2; (* arith *) napply daemon
2689    ##| nrewrite > (low_bound_free …); //; nrewrite > (high_bound_free …); /2/;
2690    ##]
2691##] nqed.
2692
2693(* Monotonicity properties of memory injections. *)
2694
2695ndefinition inject_incr : meminj → meminj → Prop ≝ λf1,f2.
2696  ∀b. f1 b = f2 b ∨ f1 b = None ?.
2697
2698nlemma inject_incr_refl :
2699   ∀f. inject_incr f f .
2700#f;nwhd;#b;@;//; nqed.
2701
2702nlemma inject_incr_trans :
2703  ∀f1,f2,f3.
2704  inject_incr f1 f2 → inject_incr f2 f3 → inject_incr f1 f3 .
2705#f1;#f2;#f3;nwhd in ⊢ (%→%→%);#H1;#H2;#b;
2706nelim (H1 b); nelim (H2 b); /2/; nqed.
2707
2708nlemma val_inject_incr:
2709  ∀f1,f2,v,v'.
2710  inject_incr f1 f2 →
2711  val_inject f1 v v' →
2712  val_inject f2 v v'.
2713#f1;#f2;#v;#v';#Hincr;#Hvinj;
2714ninversion Hvinj;
2715##[ ##1,2,4: #x;#_;#_; //;
2716##|#b;#ofs;#b';#ofs';#delta; #INJb; #Hofs; #_;#_;
2717nelim (Hincr b); #H;
2718##[ napply (val_inject_ptr ??????? Hofs); /2/;
2719##| napply False_ind; nrewrite > INJb in H; #H; ndestruct;
2720##] nqed.
2721
2722nlemma val_list_inject_incr:
2723  ∀f1,f2,vl,vl'.
2724  inject_incr f1 f2 → val_list_inject f1 vl vl' →
2725  val_list_inject f2 vl vl'.
2726#f1;#f2;#vl;nelim vl;
2727##[ #vl'; #Hincr; #H; ninversion H; //; #v;#v';#l;#l0;#_;#_;#_; #H; ndestruct;
2728##| #h;#t;#IH;#vl';#Hincr;#H1; ninversion H1;
2729  ##[ #H; ndestruct
2730  ##| #h';#h'';#t';#t''; #Hinj1; #Hintt; #_; #e1; #e2; ndestruct;
2731      @2;/2/; napply IH; //; napply Hincr;
2732  ##]
2733##] nqed.
2734
2735(*
2736Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.
2737*)
2738
2739(* Properties of injections and allocations. *)
2740
2741ndefinition extend_inject ≝
2742       λb: block. λx: option (block × Z). λf: meminj.
2743  λb': block. if eqZb b' b then x else f b'.
2744
2745nlemma extend_inject_incr:
2746  ∀f,b,x.
2747  f b = None ? →
2748  inject_incr f (extend_inject b x f).
2749#f;#b;#x;#INJb;nwhd;#b'; nwhd in ⊢ (?(???%)?);
2750napply (eqZb_elim b' b); #eb; /2/;
2751nqed.
2752
2753nlemma alloc_right_inject:
2754  ∀f,m1,m2,lo,hi,m2',b.
2755  mem_inject f m1 m2 →
2756  alloc m2 lo hi = 〈m2', b〉 →
2757  mem_inject f m1 m2'.
2758#f;#m1;#m2;#lo;#hi;#m2';#b;
2759*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2760#ALLOC; @;
2761##[ napply (alloc_right_inj … ALLOC); //;
2762##| /2/;
2763##| #b1;#b2;#delta;#INJb1; napply (valid_block_alloc … ALLOC); /2/;
2764##| //;
2765##| /2/;
2766##|#b1;#b2;#delta;#INJb1; nrewrite > (?:low_bound m2' b2 = low_bound m2 b2);
2767   ##[ nrewrite > (?:high_bound m2' b2 = high_bound m2 b2); /2/;
2768       napply high_bound_alloc_other; /2/;
2769   ##| napply low_bound_alloc_other; /2/
2770   ##]
2771##] nqed.
2772
2773nlemma alloc_unmapped_inject:
2774  ∀f,m1,m2,lo,hi,m1',b.
2775  mem_inject f m1 m2 →
2776  alloc m1 lo hi = 〈m1', b〉 →
2777  mem_inject (extend_inject b (None ?) f) m1' m2 ∧
2778  inject_incr f (extend_inject b (None ?) f).
2779#f;#m1;#m2;#lo;#hi;#m1';#b;
2780*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2781#ALLOC;
2782ncut (inject_incr f (extend_inject b (None ?) f));
2783##[ napply extend_inject_incr; napply mi_freeblocks; /2/; ##]
2784#Hinject_incr; @; //; @;
2785##[ (* inj *)
2786    napply (alloc_left_unmapped_inj … ALLOC);
2787    ##[ ##2: nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); /2/; ##]
2788    nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;
2789    nwhd in ⊢ ((??%?)→?→?); napply eqZb_elim; #e; nwhd in ⊢ ((??%?)→?→?);
2790    #Hextend;#LOAD;
2791    ##[ ndestruct;
2792    ##| nlapply (mi_inj … Hextend LOAD); *; #v2; *; #LOAD2; #VINJ;
2793    @ v2; @; //;
2794    napply val_inject_incr; //;
2795    ##]
2796##| (* freeblocks *)
2797    #b';#Hinvalid; nwhd in ⊢ (??%?); napply (eqZb_elim b' b); //;
2798    #neb; napply mi_freeblocks; napply (not_to_not ??? Hinvalid);
2799    napply valid_block_alloc; //;
2800##| (* mappedblocks *)
2801    #b1;#b2;#delta; nwhd in ⊢ (??%?→?); napply (eqZb_elim b1 b); #eb;
2802    ##[ #H; ndestruct;
2803    ##| #H; napply (mi_mappedblock … H);
2804    ##]
2805##| (* overlap *)
2806    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2; #neb1; nwhd in ⊢ (??%?→??%?→?);
2807    nrewrite > (low_bound_alloc … ALLOC ?); nrewrite > (low_bound_alloc … ALLOC ?);
2808    nrewrite > (high_bound_alloc … ALLOC ?); nrewrite > (high_bound_alloc … ALLOC ?);
2809    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2810    ##[ ndestruct
2811    ##| nlapply (eqZb_to_Prop b2 b); nelim (eqZb b2 b); #e2; #INJb2;
2812      ##[ ndestruct
2813      ##| napply mi_no_overlap; /2/;
2814      ##]
2815    ##]
2816##| (* range *)
2817    #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
2818    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2819    ##[ ndestruct
2820    ##| napply (mi_range_1 … INJb1);
2821    ##]
2822##| #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
2823    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2824    ##[  ndestruct
2825    ##| napply (mi_range_2 … INJb1);
2826    ##]
2827##] nqed.
2828
2829nlemma alloc_mapped_inject:
2830  ∀f,m1,m2,lo,hi,m1',b,b',ofs.
2831  mem_inject f m1 m2 →
2832  alloc m1 lo hi = 〈m1', b〉 →
2833  valid_block m2 b' →
2834  min_signed ≤ ofs ∧ ofs ≤ max_signed →
2835  min_signed ≤ low_bound m2 b' →
2836  high_bound m2 b' ≤ max_signed →
2837  low_bound m2 b' ≤ lo + ofs →
2838  hi + ofs ≤ high_bound m2 b' →
2839  inj_offset_aligned ofs (hi-lo) →
2840  (∀b0,ofs0.
2841   f b0 = Some ? 〈b', ofs0〉 →
2842   high_bound m1 b0 + ofs0 ≤ lo + ofs ∨
2843   hi + ofs ≤ low_bound m1 b0 + ofs0) →
2844  mem_inject (extend_inject b (Some ? 〈b', ofs〉) f) m1' m2 ∧
2845  inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f).
2846#f;#m1;#m2;#lo;#hi;#m1';#b;#b';#ofs;
2847*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2848#ALLOC;#validb';#rangeofs;#rangelo;#rangehi;#boundlo;#boundhi;#injaligned;#boundmapped;
2849ncut (inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f));
2850##[ napply extend_inject_incr; napply mi_freeblocks; /2/; ##]
2851#Hincr; @; //; @;
2852##[ (* inj *)
2853    napply (alloc_left_mapped_inj … ALLOC … validb' boundlo boundhi); /2/;
2854    ##[ ##2:nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); /2/; ##]
2855    nwhd; #chunk;#b1;#ofs';#v1;#b2;#delta;#Hextend;#LOAD;
2856    nwhd in Hextend:(??%?); nrewrite > (eqZb_false b1 b ?) in Hextend;
2857    ##[ #Hextend; nlapply (mi_inj … Hextend LOAD);
2858        *; #v2; *; #LOAD2; #VINJ;
2859    @ v2; @; //;
2860    napply val_inject_incr; //;
2861    ##| napply (valid_not_valid_diff m1); /2/;
2862        napply (valid_access_valid_block … chunk … ofs'); /2/;
2863    ##]
2864##| (* freeblocks *)
2865    #b';#Hinvalid; nwhd in ⊢ (??%?); nrewrite > (eqZb_false b' b ?);
2866    ##[ napply mi_freeblocks; napply (not_to_not ??? Hinvalid);
2867    napply valid_block_alloc; //;
2868    ##| napply sym_neq; napply (valid_not_valid_diff m1'); //;
2869        napply (valid_new_block … ALLOC);
2870    ##]
2871##| (* mappedblocks *)
2872    #b1;#b2;#delta; nwhd in ⊢ (??%?→?); napply (eqZb_elim b1 b); #eb;#einj;
2873    ##[ ndestruct; //;
2874    ##| napply (mi_mappedblock … einj);
2875    ##]
2876##| (* overlap *)
2877    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2; #neb1; nwhd in ⊢ (??%?→??%?→?);
2878    nrewrite > (low_bound_alloc … ALLOC ?); nrewrite > (low_bound_alloc … ALLOC ?);
2879    nrewrite > (high_bound_alloc … ALLOC ?); nrewrite > (high_bound_alloc … ALLOC ?);
2880    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2881    ##[ nelim (grumpydestruct2 ?????? INJb1); #eb1';#eofs1 ##]
2882    nlapply (eqZb_to_Prop b2 b); nelim (eqZb b2 b); #e2; #INJb2;
2883    ##[ nelim (grumpydestruct2 ?????? INJb2); #eb2';#eofs2 ##]
2884    ##[ napply False_ind; nrewrite > e in neb1; nrewrite > e2; /2/;
2885    ##| nelim (decidable_eq_Z b1' b2'); #e';
2886        ##[ nrewrite < e' in INJb2 ⊢ %; nrewrite < eb1'; nrewrite < eofs1; #INJb2; nlapply (boundmapped … INJb2);
2887            *; #H; @2; ##[ @2 ##| @1 ##] napply H;
2888        ##| @1;@1;@1; napply e'
2889        ##]
2890    ##| nelim (decidable_eq_Z b1' b2'); #e';
2891        ##[ nrewrite < e' in INJb2 ⊢ %; #INJb2; nelim (grumpydestruct2 ?????? INJb2); #eb'; #eofs; nrewrite < eb' in INJb1; nrewrite < eofs; #INJb1; nlapply (boundmapped … INJb1);
2892            *; #H; @2; ##[ @1; /2/ ##| @2; napply H; ##]
2893        ##| @1;@1;@1; napply e'
2894        ##]
2895    ##| napply mi_no_overlap; /2/;
2896    ##]
2897##| (* range *)
2898    #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
2899    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2900    ##[ ndestruct; /2/;
2901    ##| napply (mi_range_1 … INJb1);
2902    ##]
2903##| #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
2904    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
2905    ##[ ndestruct; @2;@;/2/;
2906    ##| napply (mi_range_2 … INJb1);
2907    ##]
2908##] nqed.
2909
2910nlemma alloc_parallel_inject:
2911  ∀f,m1,m2,lo,hi,m1',m2',b1,b2.
2912  mem_inject f m1 m2 →
2913  alloc m1 lo hi = 〈m1', b1〉 →
2914  alloc m2 lo hi = 〈m2', b2〉 →
2915  min_signed ≤ lo → hi ≤ max_signed →
2916  mem_inject (extend_inject b1 (Some ? 〈b2, OZ〉) f) m1' m2' ∧
2917  inject_incr f (extend_inject b1 (Some ? 〈b2, OZ〉) f).
2918#f;#m1;#m2;#lo;#hi;#m1';#m2';#b1;#b2;
2919#Hminj;#ALLOC1;#ALLOC2;#Hlo;#Hhi;
2920napply (alloc_mapped_inject … ALLOC1); /2/;
2921##[ napply (alloc_right_inject … Hminj ALLOC2);
2922##| nrewrite > (low_bound_alloc_same … ALLOC2); //
2923##| nrewrite > (high_bound_alloc_same … ALLOC2); //
2924##| nrewrite > (low_bound_alloc_same … ALLOC2); //
2925##| nrewrite > (high_bound_alloc_same … ALLOC2); //
2926##| nwhd; (* arith *) napply daemon
2927##| #b;#ofs;#INJb0; napply False_ind;
2928    nelim Hminj;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
2929    nlapply (mi_mappedblock … INJb0);
2930    #H; napply (absurd ? H ?); /2/;
2931##] nqed.
2932
2933ndefinition meminj_init ≝ λm: mem.
2934  λb: block. if Zltb b (nextblock m) then Some ? 〈b, OZ〉 else None ?.
2935
2936ndefinition mem_inject_neutral ≝ λm: mem.
2937  ∀f,chunk,b,ofs,v.
2938  load chunk m b ofs = Some ? v → val_inject f v v.
2939
2940nlemma init_inject:
2941  ∀m.
2942  mem_inject_neutral m →
2943  mem_inject (meminj_init m) m m.
2944#m;#neutral;@;
2945##[ (* inj *)
2946    nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta; nwhd in ⊢ (??%?→?→?);
2947    napply Zltb_elim_Type0; #ltb1; ##[
2948    #H; nelim (grumpydestruct2 ?????? H); #eb1; #edelta;
2949    nrewrite < eb1; nrewrite < edelta; #LOAD; @v1; @; //;
2950    napply neutral; //;
2951    ##| #H;nwhd in H:(??%?); ndestruct;
2952    ##]
2953##| (* free blocks *)
2954    #b;nrewrite > (unfold_valid_block …); nwhd in ⊢ (?→??%?); #notvalid;
2955    napply Zltb_elim_Type0; #ltb1;
2956    ##[ napply False_ind; napply (absurd ? ltb1 notvalid)
2957    ##| //
2958    ##]
2959##| (* mapped blocks *)
2960    #b;#b';#delta;nwhd in ⊢ (??%?→?); nrewrite > (unfold_valid_block …);
2961    napply Zltb_elim_Type0; #ltb;
2962    #H; nwhd in H:(??%?); ndestruct; //
2963##| (* overlap *)
2964    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neb1; nwhd in ⊢(??%?→??%?→?);
2965    napply Zltb_elim_Type0; #ltb1;
2966    ##[ #H; nwhd in H:(??%?); ndestruct;
2967        napply Zltb_elim_Type0; #ltb2;
2968        #H2; nwhd in H2:(??%?); ndestruct; @;@;@;/2/;
2969    ##| #H; nwhd in H:(??%?); ndestruct;
2970    ##]
2971##| (* range *)
2972    #b;#b';#delta;nwhd in ⊢ (??%?→?);
2973    napply Zltb_elim_Type0; #ltb;
2974    ##[ #H; nelim (grumpydestruct2 ?????? H); #eb; #edelta; nrewrite < edelta;
2975        (* FIXME: should be in integers.ma *) napply daemon
2976    ##| #H; nwhd in H:(??%?); ndestruct;
2977    ##]
2978##| (* range *)
2979    #b;#b';#delta;nwhd in ⊢ (??%?→?);
2980    napply Zltb_elim_Type0; #ltb;
2981    ##[ #H; nelim (grumpydestruct2 ?????? H); #eb; #edelta; nrewrite < edelta;
2982        (* FIXME: should be in integers.ma *) napply daemon
2983    ##| #H; nwhd in H:(??%?); ndestruct;
2984    ##]
2985##] nqed.
2986
2987nremark getN_setN_inject:
2988  ∀f,m,v,n1,p1,n2,p2.
2989  val_inject f (getN n2 p2 m) (getN n2 p2 m) →
2990  val_inject f v v →
2991  val_inject f (getN n2 p2 (setN n1 p1 v m))
2992               (getN n2 p2 (setN n1 p1 v m)).
2993#f;#m;#v;#n1;#p1;#n2;#p2;#injget;#injv;
2994ncases (getN_setN_characterization m v n1 p1 n2 p2);##[ * ##] #A;
2995nrewrite > A; //;
2996nqed.
2997             
2998nremark getN_contents_init_data_inject:
2999  ∀f,n,ofs,id,pos.
3000  val_inject f (getN n ofs (contents_init_data pos id))
3001               (getN n ofs (contents_init_data pos id)).
3002#f;#n;#ofs;#id;nelim id;
3003##[ #pos; nrewrite > (getN_init …); //
3004##| #h;#t;#IH;#pos; ncases h;
3005##[ ##1,2,3,4,5: #x; napply getN_setN_inject; //
3006##| ##6,8: #x; napply IH ##| #x;#y;napply IH ##] (* XXX // doesn't work? *)
3007nqed.
3008
3009nlemma alloc_init_data_neutral:
3010  ∀m,id,m',b.
3011  mem_inject_neutral m →
3012  alloc_init_data m id = 〈m', b〉 →
3013  mem_inject_neutral m'.
3014#m;#id;#m';#b;#Hneutral;#INIT; nwhd in INIT:(??%?); (* XXX: ndestruct makes a bit of a mess *)
3015napply (pairdisc_elim … INIT);
3016nwhd in ⊢ (??%% → ?);#B;nrewrite < B in ⊢ (??%% → ?);
3017nwhd in ⊢ (??%% → ?);#A;
3018nwhd; #f;#chunk;#b';#ofs;#v; #LOAD;
3019nlapply (load_inv … LOAD); *; #C; #D;
3020nrewrite < B in D; nrewrite > A;
3021nrewrite > (unfold_update block_contents …); napply eqZb_elim;
3022##[ #eb'; #D; nwhd in D:(???(??(???%))); nrewrite > D;
3023    napply (load_result_inject … chunk); //; @;
3024    napply getN_contents_init_data_inject;
3025##| #neb'; #D; napply (Hneutral ? chunk b' ofs ??); nwhd in ⊢ (??%?);
3026    nrewrite > (in_bounds_true m chunk b' ofs (option ?) …);
3027    ##[ nrewrite < D; //
3028    ##| nelim C; #Cval;#Clo;#Chi;#Cal; @;
3029    ##[ nrewrite > (unfold_valid_block …);
3030        nrewrite > (unfold_valid_block …) in Cval; nrewrite < B;
3031        (* arith using neb' *) napply daemon
3032    ##| nrewrite > (?:low_bound m b' = low_bound m' b'); //;
3033        nwhd in ⊢ (??%%); nrewrite < B; nrewrite > A;
3034        nrewrite > (update_o block_contents …); //; napply sym_neq; //;
3035    ##| nrewrite > (?:high_bound m b' = high_bound m' b'); //;
3036        nwhd in ⊢ (??%%); nrewrite < B; nrewrite > A;
3037        nrewrite > (update_o block_contents …); //; napply sym_neq; //;
3038    ##| //;
3039    ##]
3040##] nqed.
3041
3042
3043(* ** Memory shifting *)
3044
3045(* A special case of memory injection where blocks are not coalesced:
3046  each source block injects in a distinct target block. *)
3047
3048ndefinition memshift ≝ block → option Z.
3049
3050ndefinition meminj_of_shift : memshift → meminj ≝ λmi: memshift.
3051  λb. match mi b with [ None ⇒ None ? | Some x ⇒ Some ? 〈b, x〉 ].
3052
3053ndefinition val_shift ≝ λmi: memshift. λv1,v2: val.
3054  val_inject (meminj_of_shift mi) v1 v2.
3055
3056nrecord mem_shift (f: memshift) (m1,m2: mem) : Prop :=
3057  {
3058    ms_inj:
3059      mem_inj val_inject (meminj_of_shift f) m1 m2;
3060    ms_samedomain:
3061      nextblock m1 = nextblock m2;
3062    ms_domain:
3063      ∀b. match f b with [ Some _ ⇒ b < nextblock m1 | None ⇒ b ≥ nextblock m1 ];
3064    ms_range_1:
3065      ∀b,delta.
3066      f b = Some ? delta →
3067      min_signed ≤ delta ∧ delta ≤ max_signed;
3068    ms_range_2:
3069      ∀b,delta.
3070      f b = Some ? delta →
3071      min_signed ≤ low_bound m2 b ∧ high_bound m2 b ≤ max_signed
3072  }.
3073
3074(* * The following lemmas establish the absence of machine integer overflow
3075  during address computations. *)
3076
3077nlemma address_shift:
3078  ∀f,m1,m2,chunk,b,ofs1,delta.
3079  mem_shift f m1 m2 →
3080  valid_access m1 chunk b (signed ofs1) →
3081  f b = Some ? delta →
3082  signed (add ofs1 (repr delta)) = signed ofs1 + delta.
3083#f;#m1;#m2;#chunk;#b;#ofs1;#delta;
3084*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;#Hvalid_access;#INJb;
3085nelim (ms_range_2 … INJb); #Hlo;#Hhi;
3086nrewrite > (add_signed …);
3087nrewrite > (signed_repr …); nrewrite > (signed_repr …); /2/;
3088ncut (valid_access m2 chunk b (signed ofs1 + delta));
3089##[ napply (valid_access_inj ? (meminj_of_shift f) … ms_inj Hvalid_access);
3090    nwhd in ⊢ (??%?); nrewrite > INJb; // ##]
3091*; (* arith *) napply daemon;
3092nqed.
3093
3094nlemma valid_pointer_shift_no_overflow:
3095  ∀f,m1,m2,b,ofs,x.
3096  mem_shift f m1 m2 →
3097  valid_pointer m1 b (signed ofs) = true →
3098  f b = Some ? x →
3099  min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed.
3100#f;#m1;#m2;#b;#ofs;#x;
3101*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3102#VALID;#INJb;
3103nlapply (proj1 ?? (valid_pointer_valid_access …) VALID); #Hvalid_access;
3104ncut (valid_access m2 Mint8unsigned b (signed ofs + x));
3105##[ napply (valid_access_inj … ms_inj Hvalid_access);
3106    nwhd in ⊢ (??%?); nrewrite > INJb; // ##]
3107*;#Hvalid_block;#Hlo;#Hhi;#Hal; nwhd in Hhi:(?(??%)?);
3108nrewrite > (signed_repr …); /2/;
3109nlapply (ms_range_2 … INJb);*;#A;#B;
3110(* arith *) napply daemon;
3111nqed.
3112
3113(* FIXME to get around ndestruct problems *)
3114nlemma vptr_eq_1 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → b = b'.
3115#b;#b';#ofs;#ofs';#H;ndestruct;//;
3116nqed.
3117nlemma vptr_eq_2 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → ofs = ofs'.
3118#b;#b';#ofs;#ofs';#H;ndestruct;//;
3119nqed.
3120
3121nlemma valid_pointer_shift:
3122  ∀f,m1,m2,b,ofs,b',ofs'.
3123  mem_shift f m1 m2 →
3124  valid_pointer m1 b (signed ofs) = true →
3125  val_shift f (Vptr b ofs) (Vptr b' ofs') →
3126  valid_pointer m2 b' (signed ofs') = true.
3127#f;#m1;#m2;#b;#ofs;#b';#ofs';#Hmem_shift;#VALID;#Hval_shift;
3128nwhd in Hval_shift; ninversion Hval_shift;
3129##[ ##1,2,4: #a; #H; ndestruct; ##]
3130#b1;#ofs1;#b2;#ofs2;#delta;#INJb1;#Hofs;#eb1;#eb2;
3131nrewrite < (vptr_eq_1 … eb1) in INJb1; nrewrite < (vptr_eq_1 … eb2); #INJb';
3132nrewrite < (vptr_eq_2 … eb1) in Hofs; nrewrite < (vptr_eq_2 … eb2); #Hofs; nrewrite > Hofs;
3133ncut (f b = Some ? delta);
3134##[ nwhd in INJb':(??%?); ncases (f b) in INJb' ⊢ %;
3135  ##[ #H; napply (False_ind … (grumpydestruct … H)); ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##]
3136##] #INJb;
3137nlapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV;
3138nelim Hmem_shift;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3139nrewrite > (add_signed …); nrewrite > (signed_repr …); //;
3140nrewrite > (signed_repr …); /2/;
3141napply (valid_pointer_inj … VALID); /2/;
3142nqed.
3143
3144(* Relation between shifts and loads. *)
3145
3146nlemma load_shift:
3147  ∀f,m1,m2,chunk,b,ofs,delta,v1.
3148  mem_shift f m1 m2 →
3149  load chunk m1 b ofs = Some ? v1 →
3150  f b = Some ? delta →
3151  ∃v2. load chunk m2 b (ofs + delta) = Some ? v2 ∧ val_shift f v1 v2.
3152#f;#m1;#m2;#chunk;#b;#ofs;#delta;#v1;
3153*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3154#LOAD; #INJb;
3155nwhd in ⊢ (??(λ_.??%)); napply (ms_inj … LOAD);
3156nwhd in ⊢ (??%?); nrewrite > INJb; //;
3157nqed.
3158
3159nlemma loadv_shift:
3160  ∀f,m1,m2,chunk,a1,a2,v1.
3161  mem_shift f m1 m2 →
3162  loadv chunk m1 a1 = Some ? v1 →
3163  val_shift f a1 a2 →
3164  ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_shift f v1 v2.
3165#f;#m1;#m2;#chunk;#a1;#a2;#v1;#Hmem_shift;#LOADV;#Hval_shift;
3166ninversion Hval_shift;
3167##[ ##1,2,4: #x;#H;nrewrite > H in LOADV;#H';nwhd in H':(??%?);napply False_ind; ndestruct; ##]
3168#b1;#ofs1;#b2;#ofs2;#delta;#INJb1;#Hofs;#ea1;#ea2; nrewrite > ea1 in LOADV; #LOADV;
3169nlapply INJb1; nwhd in ⊢ (??%? → ?);
3170nlapply (refl ? (f b1)); ncases (f b1) in ⊢ (???% → %);
3171##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; napply (False_ind … (grumpydestruct … H));
3172##| #delta'; #DELTA; nwhd in ⊢ (??%? → ?); #H; nelim (grumpydestruct2 ?????? H);
3173    #eb;#edelta;
3174##] nlapply (load_shift … Hmem_shift LOADV DELTA); *; #v2; *;#LOAD;#INJ;
3175@ v2; @; //; nrewrite > Hofs; nrewrite > eb in LOAD; nrewrite > edelta;
3176nrewrite < (?:signed (add ofs1 (repr delta)) = signed ofs1 + delta);
3177##[#H'; napply H'; (* XXX // doesn't work *)
3178##| nrewrite < edelta; napply (address_shift … chunk … Hmem_shift … DELTA);
3179    napply (load_valid_access … LOADV);
3180##]
3181nqed.
3182
3183(* Relation between shifts and stores. *)
3184
3185nlemma store_within_shift:
3186  ∀f,chunk,m1,b,ofs,v1,n1,m2,delta,v2.
3187  mem_shift f m1 m2 →
3188  store chunk m1 b ofs v1 = Some ? n1 →
3189  f b = Some ? delta →
3190  val_shift f v1 v2 →
3191  ∃n2.
3192    store chunk m2 b (ofs + delta) v2 = Some ? n2
3193    ∧ mem_shift f n1 n2.
3194#f;#chunk;#m1;#b;#ofs;#v1;#n1;#m2;#delta;#v2;
3195*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3196#STORE1;#INJb;#Hval_shift;
3197nlapply (store_mapped_inj … ms_inj ?? STORE1 ?);
3198##[ #chunk'; #echunk; napply (load_result_inject … chunk); /2/;
3199##| nwhd in ⊢ (??%?); nrewrite > INJb; (* XXX: // has stopped working *) napply refl
3200##| nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;
3201    nwhd in ⊢ (? → ??%? → ??%? → ?);
3202    nelim (f b1); nelim (f b2);
3203    ##[#_;#e1;nwhd in e1:(??%?);ndestruct;
3204    ##|#z;#_;#e1;nwhd in e1:(??%?);ndestruct;
3205    ##|#z;#_;#_;#e2;nwhd in e2:(??%?);ndestruct;
3206    ##|#delta1';#delta2';#neb;#e1;#e2;
3207       nwhd in e1:(??%?) e2:(??%?);
3208       ndestruct;
3209       @1;@1;@1;//;
3210    ##]
3211##| ##7: //;
3212##| ##4,5,6: ##skip
3213##]
3214*;#n2;*;#STORE;#MINJ;
3215@ n2; @; //; @;
3216##[ (* inj *) //
3217##| (* samedomain *)
3218    nrewrite > (nextblock_store … STORE1);
3219    nrewrite > (nextblock_store … STORE);
3220    //;
3221##| (* domain *)
3222    nrewrite > (nextblock_store … STORE1);
3223    //
3224##| (* range *)
3225    /2/
3226##| #b1;#delta1;#INJb1;
3227    nrewrite > (low_bound_store … STORE b1);
3228    nrewrite > (high_bound_store … STORE b1);
3229    napply ms_range_2;//;
3230##] nqed.
3231
3232nlemma store_outside_shift:
3233  ∀f,chunk,m1,b,ofs,m2,v,m2',delta.
3234  mem_shift f m1 m2 →
3235  f b = Some ? delta →
3236  high_bound m1 b + delta ≤ ofs
3237  ∨ ofs + size_chunk chunk ≤ low_bound m1 b + delta →
3238  store chunk m2 b ofs v = Some ? m2' →
3239  mem_shift f m1 m2'.
3240#f;#chunk;#m1;#b;#ofs;#m2;#v;#m2';#delta;
3241*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3242#INJb;#Hbounds;#STORE;@;
3243##[ (* inj *)
3244    napply (store_outside_inj … STORE); //;
3245    #b';#d'; nwhd in ⊢ (??%? → ?); nlapply (refl ? (f b')); nelim (f b') in ⊢ (???% → %);
3246    ##[ #_; #e; nwhd in e:(??%?); ndestruct;
3247    ##| #d''; #ef; #e; nelim (grumpydestruct2 ?????? e); #eb; #ed;
3248        nrewrite > eb in ef ⊢ %; nrewrite > ed; nrewrite > INJb; #ed';
3249        nrewrite < (grumpydestruct1 ??? ed'); //
3250    ##]
3251##| (* samedomain *) nrewrite > (nextblock_store … STORE); //
3252##| (* domain *) //
3253##| (* range *) /2/
3254##| #b1;#delta1;#INJb1;
3255    nrewrite > (low_bound_store … STORE b1);
3256    nrewrite > (high_bound_store … STORE b1);
3257    napply ms_range_2;//;
3258##] nqed.
3259
3260nlemma storev_shift:
3261  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
3262  mem_shift f m1 m2 →
3263  storev chunk m1 a1 v1 = Some ? n1 →
3264  val_shift f a1 a2 →
3265  val_shift f v1 v2 →
3266  ∃n2.
3267    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_shift f n1 n2.
3268#f;#chunk;#m1;#a1;#v1;#n1;#m2;#a2;#v2;
3269#Hmem_shift;#STOREV;#Hval_shift_a;#Hval_shift_v;
3270ninversion Hval_shift_a;
3271##[ ##1,2,4: #x;#H;nrewrite > H in STOREV;#H';nwhd in H':(??%?); napply False_ind; ndestruct; ##]
3272#b1;#ofs1;#b2;#ofs2;#delta;
3273nwhd in ⊢ (??%? → ?); nlapply (refl ? (f b1)); nelim (f b1) in ⊢ (???% → %);
3274##[#_; #e; nwhd in e:(??%?); ndestruct; ##]
3275#x; #INJb1; #e; nelim (grumpydestruct2 ?????? e); #eb;#ex;
3276nrewrite > ex in INJb1; #INJb1;
3277#OFS; #ea1;#ea2; nrewrite > ea1 in STOREV; #STOREV;
3278nlapply (store_within_shift … Hmem_shift STOREV INJb1 Hval_shift_v);
3279*; #n2; *; #A;#B;
3280@ n2; @; //;
3281nrewrite > OFS; nrewrite > eb in A;
3282nrewrite < (?:signed (add ofs1 (repr delta)) = signed ofs1 + delta);
3283##[ #H; napply H; (* XXX /2/ *)
3284##| napply (address_shift … chunk … Hmem_shift ? INJb1);
3285    napply (store_valid_access_3 … STOREV);
3286##]
3287nqed.
3288
3289(* Relation between shifts and [free]. *)
3290
3291nlemma free_shift:
3292  ∀f,m1,m2,b.
3293  mem_shift f m1 m2 →
3294  mem_shift f (free m1 b) (free m2 b).
3295#f;#m1;#m2;#b;
3296*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2; @;
3297##[ (* inj *)
3298    napply free_right_inj; ##[ napply free_left_inj; //
3299    ##| #b1;#delta; #chunk;#ofs; nwhd in ⊢ (??%? → ?);
3300        nlapply (refl ? (f b1)); nelim (f b1) in ⊢ (???% → %);
3301        ##[ #_; #e; nwhd in e:(??%?); ndestruct;
3302        ##| #delta'; #INJb1; #e; nwhd in e:(??%?); ndestruct;
3303            napply valid_access_free_2
3304        ##]
3305    ##]
3306##| (* samedomain *) nwhd in ⊢ (??%%); //
3307##| (* domain *) nrewrite > (?:nextblock (free m1 b) = nextblock m1); //
3308##| (* range *) /2/
3309##| #b';#delta;#INJb'; ncases (decidable_eq_Z b' b); #eb;
3310    ##[ nrewrite > eb;
3311        nrewrite > (low_bound_free_same ??); nrewrite > (high_bound_free_same ??);
3312        (* arith *) napply daemon
3313    ##| nrewrite > (low_bound_free …); //; nrewrite > (high_bound_free …); /2/;
3314    ##]
3315##] nqed.
3316
3317(* Relation between shifts and allocation. *)
3318
3319ndefinition shift_incr : memshift → memshift → Prop ≝ λf1,f2: memshift.
3320  ∀b. f1 b = f2 b ∨ f1 b = None ?.
3321
3322nremark shift_incr_inject_incr:
3323  ∀f1,f2.
3324  shift_incr f1 f2 → inject_incr (meminj_of_shift f1) (meminj_of_shift f2).
3325#f1;#f2;#Hshift; nwhd in ⊢ (?%%); nwhd; #b;
3326nelim (Hshift b); #INJ; nrewrite > INJ; /2/;
3327nqed.
3328
3329nlemma val_shift_incr:
3330  ∀f1,f2,v1,v2.
3331  shift_incr f1 f2 → val_shift f1 v1 v2 → val_shift f2 v1 v2.
3332#f1;#f2;#v1;#v2;#Hshift_incr; nwhd in ⊢ (% → %);
3333napply val_inject_incr;
3334napply shift_incr_inject_incr; //;
3335nqed.
3336
3337(* *
3338Remark mem_inj_incr:
3339  ∀f1,f2,m1,m2.
3340  inject_incr f1 f2 → mem_inj val_inject f1 m1 m2 → mem_inj val_inject f2 m1 m2.
3341Proof.
3342  intros; red; intros.
3343  destruct (H b1). rewrite <- H3 in H1.
3344  exploit H0; eauto. intros [v2 [A B]].
3345  exists v2; split. auto. apply val_inject_incr with f1; auto.
3346  congruence.
3347***)
3348
3349nlemma alloc_shift:
3350  ∀f,m1,m2,lo1,hi1,m1',b,delta,lo2,hi2.
3351  mem_shift f m1 m2 →
3352  alloc m1 lo1 hi1 = 〈m1', b〉 →
3353  lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 →
3354  min_signed ≤ delta ∧ delta ≤ max_signed →
3355  min_signed ≤ lo2 → hi2 ≤ max_signed →
3356  inj_offset_aligned delta (hi1-lo1) →
3357  ∃f'. ∃m2'.
3358     alloc m2 lo2 hi2 = 〈m2', b〉
3359  ∧ mem_shift f' m1' m2'
3360  ∧ shift_incr f f'
3361  ∧ f' b = Some ? delta.
3362#f;#m1;#m2;#lo1;#hi1;#m1';#b;#delta;#lo2;#hi2;
3363*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
3364#ALLOC;#Hlo_delta;#Hhi_delta;#Hdelta_range;#Hlo_range;#Hhi_range;#Hinj_aligned;
3365nlapply (refl ? (alloc m2 lo2 hi2)); nelim (alloc m2 lo2 hi2) in ⊢ (???% → %);
3366#m2';#b';#ALLOC2;
3367ncut (b' = b);
3368##[ nrewrite > (alloc_result … ALLOC); nrewrite > (alloc_result … ALLOC2); // ##]
3369#eb; nrewrite > eb;
3370ncut (f b = None ?);
3371##[ nlapply (ms_domain b); nrewrite > (alloc_result … ALLOC);
3372    nelim (f (nextblock m1)); //;
3373    #z; (* arith *) napply daemon
3374##]
3375#FB;
3376nletin f' ≝ (λb':block. if eqZb b' b then Some ? delta else f b');
3377ncut (shift_incr f f');
3378##[ nwhd; #b0; nwhd in ⊢ (?(???%)?);
3379    napply eqZb_elim; /2/; ##]
3380#Hshift_incr;
3381ncut (f' b = Some ? delta);
3382##[ nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); // ##] #efb';
3383@ f'; @ m2'; @; //; @; //; @; //; @;
3384##[ (* inj *)
3385    ncut (mem_inj val_inject (meminj_of_shift f') m1 m2);
3386    ##[ nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta2; #MINJf'; #LOAD;
3387        ncut (meminj_of_shift f b1 = Some ? 〈b2, delta2〉);
3388        ##[ nrewrite < MINJf'; nwhd in ⊢ (???(?%?)); nwhd in ⊢ (??%%);
3389            napply eqZb_elim; //; #eb;
3390            nrewrite > eb;
3391            ncut (valid_block m1 b);
3392            ##[ napply valid_access_valid_block;
3393              ##[ ##3: napply load_valid_access; // ##]
3394            ##]
3395            ncut (¬valid_block m1 b); ##[ /2/ ##]
3396            #H;#H'; napply False_ind; napply (absurd ? H' H)
3397        ##] #MINJf;
3398        nlapply (ms_inj … MINJf LOAD); *; #v2; *; #A; #B;
3399        @ v2; @; //;
3400        napply (val_inject_incr … B);
3401        napply shift_incr_inject_incr; //
3402    ##] #Hmem_inj;
3403    napply (alloc_parallel_inj … delta Hmem_inj ALLOC ALLOC2 ?); /2/;
3404    nwhd in ⊢ (??%?); nrewrite > efb'; /2/;
3405##| (* samedomain *)
3406    nrewrite > (nextblock_alloc … ALLOC);
3407    nrewrite > (nextblock_alloc … ALLOC2);
3408    //;
3409##| (* domain *)
3410    #b0; (* FIXME: unfold *) nrewrite > (refl ? (f' b0):f' b0 = if eqZb b0 b then Some ? delta else f b0);
3411    nrewrite > (nextblock_alloc … ALLOC);
3412    nrewrite > (alloc_result … ALLOC);
3413    napply eqZb_elim; #eb0;
3414    ##[ nrewrite > eb0; (* arith *) napply daemon
3415    ##| nlapply (ms_domain b0); nelim (f b0);
3416        (* arith *) napply daemon
3417    ##]
3418##| (* range *)
3419    #b0;#delta0; nwhd in ⊢ (??%? → ?);
3420    napply eqZb_elim;
3421    ##[ #_; #e; nrewrite < (grumpydestruct1 ??? e); //
3422    ##| #neb; #e; napply (ms_range_1 … b0); napply e;
3423    ##]
3424##| #b0;#delta0; nwhd in ⊢ (??%? → ?);
3425    nrewrite > (low_bound_alloc … ALLOC2 ?);
3426    nrewrite > (high_bound_alloc … ALLOC2 ?);
3427    napply eqZb_elim; #eb0; nrewrite > eb;
3428    ##[ nrewrite > eb0; #ed; nrewrite < (grumpydestruct1 ??? ed);
3429        nrewrite > (eqZb_z_z ?); /3/;
3430    ##| #edelta0; nrewrite > (eqZb_false … eb0);
3431        napply ms_range_2; nwhd in edelta0:(??%?); //;
3432    ##]
3433##]
3434nqed.
3435
3436(* ** Relation between signed and unsigned loads and stores *)
3437
3438(* Target processors do not distinguish between signed and unsigned
3439  stores of 8- and 16-bit quantities.  We show these are equivalent. *)
3440
3441(* Signed 8- and 16-bit stores can be performed like unsigned stores. *)
3442
3443nremark in_bounds_equiv:
3444  ∀chunk1,chunk2,m,b,ofs.∀A:Type.∀a1,a2: A.
3445  size_chunk chunk1 = size_chunk chunk2 →
3446  (match in_bounds m chunk1 b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
3447  (match in_bounds m chunk2 b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
3448#chunk1;#chunk2;#m;#b;#ofs;#A;#a1;#a2;#Hsize;
3449nelim (in_bounds m chunk1 b ofs);
3450##[ #H; nwhd in ⊢ (??%?); nrewrite > (in_bounds_true … A a1 a2 ?); //;
3451    napply valid_access_compat; //;
3452##| #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 b ofs); //;
3453    #H'; napply False_ind; napply (absurd ?? H);
3454    napply valid_access_compat; //;
3455##] nqed.
3456
3457nlemma storev_8_signed_unsigned:
3458  ∀m,a,v.
3459  storev Mint8signed m a v = storev Mint8unsigned m a v.
3460#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
3461#b;#ofs; nwhd in ⊢ (??%%);
3462nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???); //;
3463nqed.
3464
3465nlemma storev_16_signed_unsigned:
3466  ∀m,a,v.
3467  storev Mint16signed m a v = storev Mint16unsigned m a v.
3468#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
3469#b;#ofs; nwhd in ⊢ (??%%);
3470nrewrite > (in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???); //;
3471nqed.
3472
3473(* Likewise, some target processors (e.g. the PowerPC) do not have
3474  a ``load 8-bit signed integer'' instruction. 
3475  We show that it can be synthesized as a ``load 8-bit unsigned integer''
3476  followed by a sign extension. *)
3477
3478nlemma loadv_8_signed_unsigned:
3479  ∀m,a.
3480  loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a).
3481#m;#a; nwhd in ⊢ (??%(????(%))); nelim a; //;
3482#b;#ofs; nwhd in ⊢ (??%(????%));
3483nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???); //;
3484nelim (in_bounds m Mint8unsigned b (signed ofs)); /2/;
3485#H; nwhd in ⊢ (??%%);
3486nelim (getN 0 (signed ofs) (contents (blocks m b)));
3487##[ ##1,3,4: //;
3488##| #i; nwhd in ⊢ (??(??%)(??%));
3489    nrewrite > (sign_ext_zero_ext ?? i); ##[ napply refl; (* XXX: // ? *)
3490    ##| (* arith *) napply daemon;
3491    ##]
3492##]
3493nqed.
Note: See TracBrowser for help on using the repository browser.