source: src/common/Mem.ma @ 1988

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

Abstraction of the memory contents in the memory models is no longer
necessary.

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