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

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

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

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