source: src/common/Mem.ma @ 1873

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

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

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