source: src/common/Mem.ma @ 1591

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

Use pointer record in front-end.

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