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

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

pointer_compat is a little more natural if it takes that block rather than
the block's region.

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