source: src/common/Mem.ma @ 1516

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

Ported to syntax of Matita 0.99.1.

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