source: src/common/Mem.ma @ 1651

Last change on this file since 1651 was 1599, checked in by sacerdot, 8 years ago

Start of merging of stuff into the standard library of Matita.

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