source: src/common/Mem.ma @ 1874

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

First cut at using back-end memory model throughout.
Note the correction to BEValues.

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