Revu la repartition des sources Coq en sous-repertoires

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 0 insertions, 2385 deletions

diff --git a/backend/Mem.v b/backend/Mem.v
deleted file mode 100644
index 7af696e1..00000000
--- a/backend/Mem.v
+++ /dev/null
@@ -1,2385 +0,0 @@
-(** This file develops the memory model that is used in the dynamic
-  semantics of all the languages of the compiler back-end.
-  It defines a type [mem] of memory states, the following 4 basic
-  operations over memory states, and their properties:
-- [alloc]: allocate a fresh memory block;
-- [free]: invalidate a memory block;
-- [load]: read a memory chunk at a given address;
-- [store]: store a memory chunk at a given address.
-*)
-  
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-
-(** * Structure of memory states *)
-
-(** A memory state is organized in several disjoint blocks.  Each block
-  has a low and a high bound that defines its size.  Each block map
-  byte offsets to the contents of this byte. *)
-
-Definition update (A: Set) (x: Z) (v: A) (f: Z -> A) : Z -> A :=
-  fun y => if zeq y x then v else f y.
-
-Implicit Arguments update [A].
-
-Lemma update_s:
-  forall (A: Set) (x: Z) (v: A) (f: Z -> A),
-  update x v f x = v.
-Proof.
-  intros; unfold update. apply zeq_true.
-Qed.
-
-Lemma update_o:
-  forall (A: Set) (x: Z) (v: A) (f: Z -> A) (y: Z),
-  x <> y -> update x v f y = f y.
-Proof.
-  intros; unfold update. apply zeq_false; auto.
-Qed.
-
-(** The possible contents of a byte-sized memory cell.  To give intuitions,
-  a 4-byte value [v] stored at offset [d] will be represented by
-  the content [Datum32 v] at offset [d] and [Cont] at offsets [d+1],
-  [d+2] and [d+3].  The [Cont] contents enable detecting future writes
-  that would overlap partially the 4-byte value. *)
-
-Inductive content : Set :=
-  | Undef: content              (**r undefined contents *)
-  | Datum8: val -> content      (**r a value that fits in 1 byte *)
-  | Datum16: val -> content     (**r first byte of a 2-byte value *)
-  | Datum32: val -> content     (**r first byte of a 4-byte value *)
-  | Datum64: val -> content     (**r first byte of a 8-byte value *)
-  | Cont: content.            (**r continuation bytes for a multi-byte value *)
-
-Definition contentmap : Set := Z -> content.
-
-(** A memory block comprises the dimensions of the block (low and high bounds)
-  plus a mapping from byte offsets to contents.  For technical reasons,
-  we also carry around a proof that the mapping is equal to [Undef]
-  outside the range of allowed byte offsets. *)
-
-Record block_contents : Set := mkblock {
-  low: Z;
-  high: Z;
-  contents: contentmap;
-  undef_outside: forall ofs, ofs < low \/ ofs >= high -> contents ofs = Undef
-}.
-
-(** A memory state is a mapping from block addresses (represented by [Z]
-  integers) to blocks.  We also maintain the address of the next 
-  unallocated block, and a proof that this address is positive. *)
-
-Record mem : Set := mkmem {
-  blocks: Z -> block_contents;
-  nextblock: block;
-  nextblock_pos: nextblock > 0
-}.
-
-(** * Operations on memory stores *)
-
-(** Memory reads and writes are performed by quantities called memory chunks,
-  encoding the type, size and signedness of the chunk being addressed.
-  It is useful to extract only the size information as given by the
-  following [memory_size] type. *)
-
-Inductive memory_size : Set :=
-  | Size8: memory_size
-  | Size16: memory_size
-  | Size32: memory_size
-  | Size64: memory_size.
-
-Definition size_mem (sz: memory_size) :=
-  match sz with
-  | Size8 => 1
-  | Size16 => 2
-  | Size32 => 4
-  | Size64 => 8
-  end.
-
-Definition mem_chunk (chunk: memory_chunk) :=
-  match chunk with
-  | Mint8signed => Size8
-  | Mint8unsigned => Size8
-  | Mint16signed => Size16
-  | Mint16unsigned => Size16
-  | Mint32 => Size32
-  | Mfloat32 => Size32
-  | Mfloat64 => Size64
-  end.
-
-Definition size_chunk (chunk: memory_chunk) := size_mem (mem_chunk chunk).
-
-(** The initial store. *)
-
-Remark one_pos: 1 > 0.
-Proof. omega. Qed.
-
-Remark undef_undef_outside:
-  forall lo hi ofs, ofs < lo \/ ofs >= hi -> (fun y => Undef) ofs = Undef.
-Proof.
-  auto.
-Qed.
-
-Definition empty_block (lo hi: Z) : block_contents :=
-  mkblock lo hi (fun y => Undef) (undef_undef_outside lo hi).
-
-Definition empty: mem :=
-  mkmem (fun x => empty_block 0 0) 1 one_pos.
-
-Definition nullptr: block := 0.
-
-(** Allocation of a fresh block with the given bounds.  Return an updated
-  memory state and the address of the fresh block, which initially contains
-  undefined cells.  Note that allocation never fails: we model an
-  infinite memory. *)
-
-Remark succ_nextblock_pos:
-  forall m, Zsucc m.(nextblock) > 0.
-Proof. intro. generalize (nextblock_pos m). omega. Qed.
-
-Definition alloc (m: mem) (lo hi: Z) :=
-  (mkmem (update m.(nextblock) 
-                 (empty_block lo hi)
-                 m.(blocks))
-         (Zsucc m.(nextblock))
-         (succ_nextblock_pos m),
-   m.(nextblock)).
-
-(** Freeing a block.  Return the updated memory state where the given
-  block address has been invalidated: future reads and writes to this
-  address will fail.  Note that we make no attempt to return the block
-  to an allocation pool: the given block address will never be allocated
-  later. *)
-
-Definition free (m: mem) (b: block) :=
-  mkmem (update b 
-                (empty_block 0 0)
-                m.(blocks))
-        m.(nextblock)
-        m.(nextblock_pos).
-
-(** Freeing of a list of blocks. *)
-
-Definition free_list (m:mem) (l:list block) :=
-  List.fold_right (fun b m => free m b) m l.
-
-(** Return the low and high bounds for the given block address.
-   Those bounds are 0 for freed or not yet allocated address. *)
-
-Definition low_bound (m: mem) (b: block) :=
-  low (m.(blocks) b).
-Definition high_bound (m: mem) (b: block) :=
-  high (m.(blocks) b).
-
-(** A block address is valid if it was previously allocated. It remains valid
-  even after being freed. *)
-
-Definition valid_block (m: mem) (b: block) :=
-  b < m.(nextblock).
-
-(** Reading and writing [N] adjacent locations in a [contentmap].
-
-  We define two functions and prove some of their properties:
-  - [getN n ofs m] returns the datum at offset [ofs] in block contents [m]
-    after checking that the contents of offsets [ofs+1] to [ofs+n+1]
-    are [Cont].
-  - [setN n ofs v m] updates the block contents [m], storing the content [v]
-    at offset [ofs] and the content [Cont] at offsets [ofs+1] to [ofs+n+1].
- *)
-
-Fixpoint check_cont (n: nat) (p: Z) (m: contentmap) {struct n} : bool :=
-  match n with
-  | O => true
-  | S n1 =>
-      match m p with
-      | Cont => check_cont n1 (p + 1) m
-      | _ => false
-      end
-  end.
-
-Definition getN (n: nat) (p: Z) (m: contentmap) : content :=
-  if check_cont n (p + 1) m then m p else Undef.
-
-Fixpoint set_cont (n: nat) (p: Z) (m: contentmap) {struct n} : contentmap :=
-  match n with
-  | O => m
-  | S n1 => update p Cont (set_cont n1 (p + 1) m)
-  end.
-
-Definition setN (n: nat) (p: Z) (v: content) (m: contentmap) : contentmap :=
-  update p v (set_cont n (p + 1) m).
-
-Lemma check_cont_true:
-  forall n p m,
-  (forall q, p <= q < p + Z_of_nat n -> m q = Cont) ->
-  check_cont n p m = true.
-Proof.
-  induction n; intros.
-  reflexivity.
-  simpl. rewrite H. apply IHn. 
-  intros. apply H. rewrite inj_S. omega.
-  rewrite inj_S. omega. 
-Qed.
-
-Hint Resolve check_cont_true.
-
-Lemma check_cont_inv:
-  forall n p m,
-  check_cont n p m = true ->
-  (forall q, p <= q < p + Z_of_nat n -> m q = Cont).
-Proof.
-  induction n; intros until m.
-  unfold Z_of_nat. intros. omegaContradiction.
-  unfold check_cont; fold check_cont. 
-  caseEq (m p); intros; try discriminate.
-  assert (p = q \/ p + 1 <= q < (p + 1) + Z_of_nat n).
-    rewrite inj_S in H1. omega. 
-  elim H2; intro.
-  subst q. auto.
-  apply IHn with (p + 1); auto.
-Qed.
-
-Hint Resolve check_cont_inv.
-
-Lemma check_cont_false:
-  forall n p q m,
-  p <= q < p + Z_of_nat n ->
-  m q <> Cont ->
-  check_cont n p m = false.
-Proof.
-  intros. caseEq (check_cont n p m); intro.
-  generalize (check_cont_inv _ _ _ H1 q H). intro. contradiction.
-  auto.
-Qed.
-
-Hint Resolve check_cont_false.
-
-Lemma set_cont_inside:
-  forall n p m q,
-  p <= q < p + Z_of_nat n ->
-  (set_cont n p m) q = Cont.
-Proof.
-  induction n; intros.
-  unfold Z_of_nat in H. omegaContradiction.
-  simpl. 
-  assert (p = q \/ p + 1 <= q < (p + 1) + Z_of_nat n).
-    rewrite inj_S in H. omega. 
-  elim H0; intro.
-  subst q. apply update_s.
-  rewrite update_o. apply IHn. auto. 
-  red; intro; subst q. omega. 
-Qed.
-
-Hint Resolve set_cont_inside.
-
-Lemma set_cont_outside:
-  forall n p m q,
-  q < p \/ p + Z_of_nat n <= q ->
-  (set_cont n p m) q = m q.
-Proof.
-  induction n; intros.
-  simpl. auto.
-  simpl. rewrite inj_S in H. 
-  rewrite update_o. apply IHn. omega. omega.
-Qed.
-
-Hint Resolve set_cont_outside.
-
-Lemma getN_setN_same:
-  forall n p v m,
-  getN n p (setN n p v m) = v.
-Proof.
-  intros. unfold getN, setN.
-  rewrite check_cont_true. apply update_s.
-  intros. rewrite update_o. apply set_cont_inside. auto.
-  omega. 
-Qed.
-
-Hint Resolve getN_setN_same.
-
-Lemma getN_setN_other:
-  forall n1 n2 p1 p2 v m,
-  p1 + Z_of_nat n1 < p2 \/ p2 + Z_of_nat n2 < p1 ->
-  getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m.
-Proof.
-  intros. unfold getN, setN.
-  caseEq (check_cont n2 (p2 + 1) m); intro.
-  rewrite check_cont_true. rewrite update_o.
-  apply set_cont_outside. omega. omega.
-  intros. rewrite update_o. rewrite set_cont_outside.
-  eapply check_cont_inv. eauto. auto.
-  omega. omega. 
-  caseEq (check_cont n2 (p2 + 1) (update p1 v (set_cont n1 (p1 + 1) m))); intros.
-  assert (check_cont n2 (p2 + 1) m = true).
-  apply check_cont_true. intros. 
-  generalize (check_cont_inv _ _ _ H1 q H2).
-  rewrite update_o. rewrite set_cont_outside. auto. omega. omega.
-  rewrite H0 in H2; discriminate.
-  auto.
-Qed. 
-
-Hint Resolve getN_setN_other.
-
-Lemma getN_setN_overlap:
-  forall n1 n2 p1 p2 v m,
-  p1 <> p2 ->
-  p1 + Z_of_nat n1 >= p2 -> p2 + Z_of_nat n2 >= p1 ->
-  v <> Cont ->
-  getN n2 p2 (setN n1 p1 v m) = Cont \/
-  getN n2 p2 (setN n1 p1 v m) = Undef.
-Proof.
-  intros. unfold getN.
-  caseEq (check_cont n2 (p2 + 1) (setN n1 p1 v m)); intro.
-  case (zlt p2 p1); intro.
-  assert (p2 + 1 <= p1 < p2 + 1 + Z_of_nat n2). omega.
-  generalize (check_cont_inv _ _ _ H3 p1 H4). 
-  unfold setN. rewrite update_s. intro. contradiction.
-  left. unfold setN. rewrite update_o.
-  apply set_cont_inside. omega. auto.
-  right; auto.
-Qed. 
-
-Hint Resolve getN_setN_overlap.
-
-Lemma getN_setN_mismatch:
-  forall n1 n2 p v m,
-  getN n2 p (setN n1 p v m) = v \/ getN n2 p (setN n1 p v m) = Undef.
-Proof.
-  intros. unfold getN. 
-  caseEq (check_cont n2 (p + 1) (setN n1 p v m)); intro.
-  left. unfold setN. apply update_s.
-  right. auto.
-Qed.
-
-Hint Resolve getN_setN_mismatch.
-
-Lemma getN_init:
-  forall n p,
-  getN n p (fun y => Undef) = Undef.
-Proof.
-  intros. unfold getN.
-  case (check_cont n (p + 1) (fun y => Undef)); auto.
-Qed.
-
-Hint Resolve getN_init.
-
-(** The following function checks whether accessing the given memory chunk
-  at the given offset in the given block respects the bounds of the block. *)
-
-Definition in_bounds (chunk: memory_chunk) (ofs: Z) (c: block_contents) : 
-        {c.(low) <= ofs /\ ofs + size_chunk chunk <= c.(high)}
-      + {c.(low) > ofs \/ ofs + size_chunk chunk > c.(high)} :=
-  match zle c.(low) ofs, zle (ofs + size_chunk chunk) c.(high) with
-  | left P1, left P2 => left _ (conj P1 P2)
-  | left P1, right P2 => right _ (or_intror _ P2)
-  | right P1, _ => right _ (or_introl _ P1)
-  end.
-
-Lemma in_bounds_holds:
-  forall (chunk: memory_chunk) (ofs: Z) (c: block_contents)
-         (A: Set) (a b: A),
-  c.(low) <= ofs -> ofs + size_chunk chunk <= c.(high) ->
-  (if in_bounds chunk ofs c then a else b) = a.
-Proof.
-  intros. case (in_bounds chunk ofs c); intro.
-  auto.
-  omegaContradiction.
-Qed.
-
-Lemma in_bounds_exten:
-  forall (chunk: memory_chunk) (ofs: Z) (c: block_contents) (x: contentmap) P,
-  in_bounds chunk ofs (mkblock (low c) (high c) x P) =
-  in_bounds chunk ofs c.
-Proof.
-  intros; reflexivity.
-Qed.
-
-Hint Resolve in_bounds_holds in_bounds_exten.
-
-(** [valid_pointer] holds if the given block address is valid and the
-  given offset falls within the bounds of the corresponding block. *)
-
-Definition valid_pointer (m: mem) (b: block) (ofs: Z) : bool :=
-  if zlt b m.(nextblock) then
-    (let c := m.(blocks) b in
-     if zle c.(low) ofs then if zlt ofs c.(high) then true else false
-                        else false)
-  else false.
-
-(** Read a quantity of size [sz] at offset [ofs] in block contents [c].
-  Return [Vundef] if the requested size does not match that of the
-  current contents, or if the following offsets do not contain [Cont].
-  The first check captures a size mismatch between the read and the
-  latest write at this offset.  The second check captures partial overwriting
-  of the latest write at this offset by a more recent write at a nearby
-  offset. *)
-
-Definition load_contents (sz: memory_size) (c: contentmap) (ofs: Z) : val :=
-  match sz with
-  | Size8 =>
-      match getN 0%nat ofs c with
-      | Datum8 n => n
-      | _ => Vundef
-      end
-  | Size16 =>
-      match getN 1%nat ofs c with
-      | Datum16 n => n
-      | _ => Vundef
-      end
-  | Size32 =>
-      match getN 3%nat ofs c with
-      | Datum32 n => n
-      | _ => Vundef
-      end
-  | Size64 =>
-      match getN 7%nat ofs c with
-      | Datum64 n => n
-      | _ => Vundef
-      end
-  end.
-
-(** [load chunk m b ofs] perform a read in memory state [m], at address
-  [b] and offset [ofs].  [None] is returned if the address is invalid
-  or the memory access is out of bounds. *)
-
-Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z)
-                : option val :=
-  if zlt b m.(nextblock) then
-    (let c := m.(blocks) b in
-     if in_bounds chunk ofs c
-     then Some (Val.load_result chunk
-                    (load_contents (mem_chunk chunk) c.(contents) ofs))
-     else None)
-  else
-    None.
-
-(** [loadv chunk m addr] is similar, but the address and offset are given
-  as a single value [addr], which must be a pointer value. *)
-
-Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
-  match addr with
-  | Vptr b ofs => load chunk m b (Int.signed ofs)
-  | _ => None
-  end.
-
-Theorem load_in_bounds:
-  forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z),
-  valid_block m b ->
-  low_bound m b <= ofs ->
-  ofs + size_chunk chunk <= high_bound m b ->
-  exists v, load chunk m b ofs = Some v.
-Proof.
-  intros. unfold load. rewrite zlt_true; auto.
-  rewrite in_bounds_holds. 
-  exists (Val.load_result chunk
-            (load_contents (mem_chunk chunk)
-                           (contents (m.(blocks) b))
-                           ofs)).
-  auto.
-  exact H0. exact H1.
-Qed.
-
-Lemma load_inv:
-  forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val),
-  load chunk m b ofs = Some v ->
-  let c := m.(blocks) b in
-  b < m.(nextblock) /\
-  c.(low) <= ofs /\
-  ofs + size_chunk chunk <= c.(high) /\
-  Val.load_result chunk (load_contents (mem_chunk chunk)  c.(contents) ofs) = v.
-Proof.
-  intros until v; unfold load.
-  case (zlt b (nextblock m)); intro.
-  set (c := m.(blocks) b).
-  case (in_bounds chunk ofs c).
-  intuition congruence.
-  intros; discriminate.
-  intros; discriminate.
-Qed.
-Hint Resolve load_in_bounds load_inv.
-
-(* Write the value [v] with size [sz] at offset [ofs] in block contents [c].
-   Return updated block contents.  [Cont] contents are stored at the following
-   offsets. *)
-
-Definition store_contents (sz: memory_size) (c: contentmap)
-                          (ofs: Z) (v: val) : contentmap :=
-  match sz with
-  | Size8 =>
-      setN 0%nat ofs (Datum8 v) c
-  | Size16 =>
-      setN 1%nat ofs (Datum16 v) c
-  | Size32 =>
-      setN 3%nat ofs (Datum32 v) c
-  | Size64 =>
-      setN 7%nat ofs (Datum64 v) c
-  end.
-
-Remark store_contents_undef_outside:
-  forall sz c ofs v lo hi,
-  lo <= ofs /\ ofs + size_mem sz <= hi ->
-  (forall x, x < lo \/ x >= hi -> c x = Undef) ->
-  (forall x, x < lo \/ x >= hi ->
-     store_contents sz c ofs v x = Undef).
-Proof.
-  intros until hi; intros [LO HI] UO.
-  assert (forall n d x, 
-            ofs + (1 + Z_of_nat n) <= hi ->
-            x < lo \/ x >= hi ->
-            setN n ofs d c x = Undef).
-    intros. unfold setN. rewrite update_o.
-    transitivity (c x). apply set_cont_outside. omega. 
-    apply UO. omega. omega.
-  unfold store_contents; destruct sz; unfold size_mem in HI;
-  intros; apply H; auto; simpl Z_of_nat; auto.
-Qed.
-
-Definition unchecked_store
-     (chunk: memory_chunk) (m: mem) (b: block)
-     (ofs: Z) (v: val)
-     (P: (m.(blocks) b).(low) <= ofs /\
-         ofs + size_chunk chunk <= (m.(blocks) b).(high)) : mem :=
-  let c := m.(blocks) b in
-  mkmem
-    (update b
-        (mkblock c.(low) c.(high)
-                 (store_contents (mem_chunk chunk) c.(contents) ofs v)
-                 (store_contents_undef_outside (mem_chunk chunk) c.(contents)
-                      ofs v _ _ P c.(undef_outside)))
-        m.(blocks))
-    m.(nextblock)
-    m.(nextblock_pos).
-
-(** [store chunk m b ofs v] perform a write in memory state [m].
-  Value [v] is stored at address [b] and offset [ofs].
-  Return the updated memory store, or [None] if the address is invalid
-  or the memory access is out of bounds. *)
-
-Definition store (chunk: memory_chunk) (m: mem) (b: block)
-                 (ofs: Z) (v: val) : option mem :=
-  if zlt b m.(nextblock) then
-    match in_bounds chunk ofs (m.(blocks) b) with
-    | left P => Some(unchecked_store chunk m b ofs v P)
-    | right _ => None
-    end
-  else
-    None.
-
-(** [storev chunk m addr v] is similar, but the address and offset are given
-  as a single value [addr], which must be a pointer value. *)
-
-Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
-  match addr with
-  | Vptr b ofs => store chunk m b (Int.signed ofs) v
-  | _ => None
-  end.
-
-Theorem store_in_bounds:
-  forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val),
-  valid_block m b ->
-  low_bound m b <= ofs ->
-  ofs + size_chunk chunk <= high_bound m b ->
-  exists m', store chunk m b ofs v = Some m'.
-Proof.
-  intros. unfold store.
-  rewrite zlt_true; auto. 
-  case (in_bounds chunk ofs (blocks m b)); intro P.
-  exists (unchecked_store chunk m b ofs v P). reflexivity.
-  unfold low_bound in H0. unfold high_bound in H1. omegaContradiction.
-Qed.
-
-Lemma store_inv:
-  forall (chunk: memory_chunk) (m m': mem) (b: block) (ofs: Z) (v: val),
-  store chunk m b ofs v = Some m' ->
-  let c := m.(blocks) b in
-  b < m.(nextblock) /\
-  c.(low) <= ofs /\
-  ofs + size_chunk chunk <= c.(high) /\
-  m'.(nextblock) = m.(nextblock) /\
-  exists P, m'.(blocks) =
-    update b (mkblock c.(low) c.(high)
-                        (store_contents (mem_chunk chunk) c.(contents) ofs v) P)
-                        m.(blocks).
-Proof.
-  intros until v; unfold store.
-  case (zlt b (nextblock m)); intro.
-  set (c := m.(blocks) b).
-  case (in_bounds chunk ofs c).
-  intros; injection H; intro; subst m'. simpl.
-  intuition. fold c. 
-  exists (store_contents_undef_outside (mem_chunk chunk) 
-            (contents c) ofs v (low c) (high c) a (undef_outside c)).
-  auto.
-  intros; discriminate.
-  intros; discriminate.
-Qed.
-
-Hint Resolve store_in_bounds store_inv.
-
-(** Build a block filled with the given initialization data. *)
-
-Fixpoint contents_init_data (pos: Z) (id: list init_data) {struct id}: contentmap :=
-  match id with
-  | nil => (fun y => Undef)
-  | Init_int8 n :: id' =>
-      store_contents Size8 (contents_init_data (pos + 1) id') pos (Vint n)
-  | Init_int16 n :: id' =>
-      store_contents Size16 (contents_init_data (pos + 2) id') pos (Vint n)
-  | Init_int32 n :: id' =>
-      store_contents Size32 (contents_init_data (pos + 4) id') pos (Vint n)
-  | Init_float32 f :: id' =>
-      store_contents Size32 (contents_init_data (pos + 4) id') pos (Vfloat f)
-  | Init_float64 f :: id' =>
-      store_contents Size64 (contents_init_data (pos + 8) id') pos (Vfloat f)
-  | Init_space n :: id' =>
-      contents_init_data (pos + Zmax n 0) id'
-  end.
-
-Definition size_init_data (id: init_data) : Z :=
-  match id with
-  | Init_int8 _ => 1
-  | Init_int16 _ => 2
-  | Init_int32 _ => 4
-  | Init_float32 _ => 4
-  | Init_float64 _ => 8
-  | Init_space n => Zmax n 0
-  end.
-
-Definition size_init_data_list (id: list init_data): Z :=
-  List.fold_right (fun id sz => size_init_data id + sz) 0 id.
-
-Remark size_init_data_list_pos:
-  forall id, size_init_data_list id >= 0.
-Proof.
-  induction id; simpl.
-  omega.
-  assert (size_init_data a >= 0). destruct a; simpl; try omega. 
-  generalize (Zmax2 z 0). omega. omega.
-Qed.
-
-Remark contents_init_data_undef_outside:
-  forall id pos x,
-  x < pos \/ x >= pos + size_init_data_list id ->
-  contents_init_data pos id x = Undef.
-Proof.
-  induction id; simpl; intros.
-  auto.
-  generalize (size_init_data_list_pos id); intro.
-  assert (forall n delta dt,
-    delta = 1 + Z_of_nat n ->
-    x < pos \/ x >= pos + (delta + size_init_data_list id) ->
-    setN n pos dt (contents_init_data (pos + delta) id) x = Undef).
-  intros. unfold setN. rewrite update_o. 
-  transitivity (contents_init_data (pos + delta) id x).
-  apply set_cont_outside.  omega. 
-  apply IHid. omega. omega.
-  unfold size_init_data in H; destruct a;
-  try (apply H1; [reflexivity|assumption]).
-  apply IHid. generalize (Zmax2 z 0). omega. 
-Qed.
-
-Definition block_init_data (id: list init_data) : block_contents :=
-  mkblock 0 (size_init_data_list id) 
-          (contents_init_data 0 id)
-          (contents_init_data_undef_outside id 0).
-
-Definition alloc_init_data (m: mem) (id: list init_data) : mem * block :=
-  (mkmem (update m.(nextblock)
-                 (block_init_data id)
-                 m.(blocks))
-         (Zsucc m.(nextblock))
-         (succ_nextblock_pos m),
-   m.(nextblock)).
-
-Remark block_init_data_empty:
-  block_init_data nil = empty_block 0 0.
-Proof.
-  unfold block_init_data, empty_block. simpl. 
-  decEq. apply proof_irrelevance. 
-Qed.
-
-(** * Properties of the memory operations *)
-
-(** ** Properties related to block validity *)
-
-Lemma valid_not_valid_diff:
-  forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
-Proof.
-  intros; red; intros. subst b'. contradiction.
-Qed.
-
-Theorem fresh_block_alloc:
-  forall (m1 m2: mem) (lo hi: Z) (b: block), 
-  alloc m1 lo hi = (m2, b) -> ~(valid_block m1 b).
-Proof.
-  intros. injection H; intros; subst b. 
-  unfold valid_block. omega.
-Qed.
-
-Theorem valid_new_block:
-  forall (m1 m2: mem) (lo hi: Z) (b: block), 
-  alloc m1 lo hi = (m2, b) -> valid_block m2 b.
-Proof.
-  unfold alloc, valid_block; intros.
-  injection H; intros. subst b; subst m2; simpl. omega.
-Qed.
-
-Theorem valid_block_alloc:
-  forall (m1 m2: mem) (lo hi: Z) (b b': block), 
-  alloc m1 lo hi = (m2, b') ->
-  valid_block m1 b -> valid_block m2 b.
-Proof.
-  unfold alloc, valid_block; intros.
-  injection H; intros. subst m2; simpl. omega.
-Qed.
-
-Theorem valid_block_store:
-  forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs: Z) (v: val),
-  store chunk m1 b' ofs v = Some m2 ->
-  valid_block m1 b -> valid_block m2 b.
-Proof.
-  intros. generalize (store_inv _ _ _ _ _ _ H). 
-  intros [A [B [C [D [P E]]]]].
-  red. rewrite D. exact H0.
-Qed.
-
-Theorem valid_block_free:
-  forall (m: mem) (b b': block), 
-  valid_block m b -> valid_block (free m b') b.
-Proof.
-  unfold valid_block, free; intros.
-  simpl. auto.
-Qed.
-
-(** ** Properties related to [alloc] *)
-
-Theorem load_alloc_other:
-  forall (chunk: memory_chunk) (m1 m2: mem)
-         (b b': block) (ofs lo hi: Z) (v: val),
-  alloc m1 lo hi = (m2, b') ->
-  load chunk m1 b ofs = Some v ->
-  load chunk m2 b ofs = Some v.
-Proof.
-  unfold alloc; intros.
-  injection H; intros; subst m2; clear H.
-  generalize (load_inv _ _ _ _ _ H0).
-  intros (A, (B, (C, D))).
-  unfold load; simpl.
-  rewrite zlt_true.
-  repeat (rewrite update_o).
-  rewrite in_bounds_holds. congruence. auto. auto.
-  omega. omega.
-Qed.
-
-Lemma load_contents_init:
-  forall (sz: memory_size) (ofs: Z),
-  load_contents sz (fun y => Undef) ofs = Vundef.
-Proof.
-  intros. destruct sz; reflexivity.
-Qed.
-
-Theorem load_alloc_same:
-  forall (chunk: memory_chunk) (m1 m2: mem)
-         (b b': block) (ofs lo hi: Z) (v: val),
-  alloc m1 lo hi = (m2, b') ->
-  load chunk m2 b' ofs = Some v ->
-  v = Vundef.
-Proof.
-  unfold alloc; intros.
-  injection H; intros; subst m2; clear H.
-  generalize (load_inv _ _ _ _ _ H0).
-  simpl. rewrite H1. rewrite update_s. simpl. intros (A, (B, (C, D))).
-  rewrite <- D. rewrite load_contents_init. 
-  destruct chunk; reflexivity.
-Qed.  
-
-Theorem low_bound_alloc:
-  forall (m1 m2: mem) (b b': block) (lo hi: Z),
-  alloc m1 lo hi = (m2, b') ->
-  low_bound m2 b = if zeq b b' then lo else low_bound m1 b.
-Proof.
-  unfold alloc; intros. 
-  injection H; intros; subst m2; clear H.
-  unfold low_bound; simpl. 
-  unfold update.
-  subst b'.
-  case (zeq b (nextblock m1)); reflexivity.
-Qed.
-
-Theorem high_bound_alloc:
-  forall (m1 m2: mem) (b b': block) (lo hi: Z),
-  alloc m1 lo hi = (m2, b') ->
-  high_bound m2 b = if zeq b b' then hi else high_bound m1 b.
-Proof.
-  unfold alloc; intros. 
-  injection H; intros; subst m2; clear H.
-  unfold high_bound; simpl. 
-  unfold update.
-  subst b'.
-  case (zeq b (nextblock m1)); reflexivity.
-Qed.
-
-Theorem store_alloc:
-  forall (chunk: memory_chunk) (m1 m2: mem) (b: block) (ofs lo hi: Z) (v: val),
-  alloc m1 lo hi = (m2, b) ->
-  lo <= ofs -> ofs + size_chunk chunk <= hi ->
-  exists m2', store chunk m2 b ofs v = Some m2'.
-Proof.
-  unfold alloc; intros.
-  injection H; intros.
-  assert (A: b < m2.(nextblock)).
-  subst m2; subst b; simpl; omega.
-  assert (B: low_bound m2 b <= ofs).
-  subst m2; subst b. unfold low_bound; simpl. rewrite update_s.
-  simpl. assumption.
-  assert (C: ofs + size_chunk chunk <= high_bound m2 b).
-  subst m2; subst b. unfold high_bound; simpl. rewrite update_s.
-  simpl. assumption.
-  exact (store_in_bounds chunk m2 b ofs v A B C).
-Qed.
-
-Hint Resolve store_alloc high_bound_alloc low_bound_alloc load_alloc_same
-load_contents_init load_alloc_other.
-
-(** ** Properties related to [free] *)
-
-Theorem load_free:
-  forall (chunk: memory_chunk) (m: mem) (b bf: block) (ofs: Z),
-  b <> bf ->
-  load chunk (free m bf) b ofs = load chunk m b ofs.
-Proof.
-  intros. unfold free, load; simpl.
-  case (zlt b (nextblock m)).
-  repeat (rewrite update_o; auto).
-  reflexivity.
-Qed.
-
-Theorem low_bound_free:
-  forall (m: mem) (b bf: block),
-  b <> bf ->
-  low_bound (free m bf) b = low_bound m b.
-Proof.
-  intros. unfold free, low_bound; simpl.
-  rewrite update_o; auto.
-Qed.
-
-Theorem high_bound_free:
-  forall (m: mem) (b bf: block),
-  b <> bf ->
-  high_bound (free m bf) b = high_bound m b.
-Proof.
-  intros. unfold free, high_bound; simpl.
-  rewrite update_o; auto.
-Qed.
-Hint Resolve load_free low_bound_free high_bound_free.
-
-(** ** Properties related to [store] *)
-
-Lemma store_is_in_bounds:
-  forall chunk m1 b ofs v m2,
-  store chunk m1 b ofs v = Some m2 ->
-  low_bound m1 b <= ofs /\ ofs + size_chunk chunk <= high_bound m1 b.
-Proof.
-  intros. generalize (store_inv _ _ _ _ _ _ H).
-  intros [A [B [C [P D]]]].
-  unfold low_bound, high_bound. tauto.
-Qed.
-
-Lemma load_store_contents_same:
-  forall (sz: memory_size) (c: contentmap) (ofs: Z) (v: val),
-  load_contents sz (store_contents sz c ofs v) ofs = v.
-Proof.
-  intros until v.
-  unfold load_contents, store_contents in |- *; case sz;
-    rewrite getN_setN_same; reflexivity.
-Qed.
-  
-Theorem load_store_same:
-  forall (chunk: memory_chunk) (m1 m2: mem) (b: block) (ofs: Z) (v: val),
-  store chunk m1 b ofs v = Some m2 ->
-  load chunk m2 b ofs = Some (Val.load_result chunk v).
-Proof.
-  intros.
-  generalize (store_inv _ _ _ _ _ _ H).
-  intros (A, (B, (C, (D, (P, E))))).
-  unfold load. rewrite D. 
-  rewrite zlt_true; auto. rewrite E. 
-  repeat (rewrite update_s). simpl.
-  rewrite in_bounds_exten. rewrite in_bounds_holds; auto.
-  rewrite load_store_contents_same; auto.
-Qed.
-           
-Lemma load_store_contents_other:
-  forall (sz1 sz2: memory_size) (c: contentmap) 
-         (ofs1 ofs2: Z) (v: val),
-  ofs2 + size_mem sz2 <= ofs1 \/ ofs1 + size_mem sz1 <= ofs2 ->
-  load_contents sz2 (store_contents sz1 c ofs1 v) ofs2 =
-  load_contents sz2 c ofs2.
-Proof.
-  intros until v.
-  unfold size_mem, store_contents, load_contents;
-  case sz1; case sz2; intros;
-  (rewrite getN_setN_other; 
-   [reflexivity | simpl Z_of_nat; omega]).
-Qed.
-
-Theorem load_store_other:
-  forall (chunk1 chunk2: memory_chunk) (m1 m2: mem)
-         (b1 b2: block) (ofs1 ofs2: Z) (v: val),
-  store chunk1 m1 b1 ofs1 v = Some m2 ->
-  b1 <> b2
-  \/ ofs2 + size_chunk chunk2 <= ofs1
-  \/ ofs1 + size_chunk chunk1 <= ofs2 ->
-  load chunk2 m2 b2 ofs2 = load chunk2 m1 b2 ofs2.
-Proof.
-  intros.
-  generalize (store_inv _ _ _ _ _ _ H).
-  intros (A, (B, (C, (D, (P, E))))).
-  unfold load. rewrite D.
-  case (zlt b2 (nextblock m1)); intro.
-  rewrite E; unfold update; case (zeq b2 b1); intro; simpl.
-  subst b2. rewrite in_bounds_exten. 
-  rewrite load_store_contents_other. auto.
-  tauto.
-  reflexivity. 
-  reflexivity.
-Qed.
-
-Ltac LSCO :=
-  match goal with
-  | |- (match getN ?sz2 ?ofs2 (setN ?sz1 ?ofs1 ?v ?c) with
-        | Undef => _
-        | Datum8 _ => _
-        | Datum16 _ => _
-        | Datum32 _ => _
-        | Datum64 _ => _
-        | Cont => _ 
-        end = _) =>
-    elim (getN_setN_overlap sz1 sz2 ofs1 ofs2 v c);
-    [ let H := fresh in (intro H; rewrite H; reflexivity)
-    | let H := fresh in (intro H; rewrite H; reflexivity)
-    | assumption
-    | simpl Z_of_nat; omega
-    | simpl Z_of_nat; omega
-    | discriminate ]
-  end.
-
-Lemma load_store_contents_overlap:
-  forall (sz1 sz2: memory_size) (c: contentmap) 
-         (ofs1 ofs2: Z) (v: val),
-  ofs1 <> ofs2 ->
-  ofs2 + size_mem sz2 > ofs1 -> ofs1 + size_mem sz1 > ofs2 ->
-  load_contents sz2 (store_contents sz1 c ofs1 v) ofs2 = Vundef.
-Proof.
-  intros.
-  destruct sz1; destruct sz2; simpl in H0; simpl in H1; simpl; LSCO.
-Qed.
-
-Ltac LSCM :=
-  match goal with
-  | H:(?x <> ?x) |- _ =>
-    elim H; reflexivity
-  | |- (match getN ?sz2 ?ofs (setN ?sz1 ?ofs ?v ?c) with
-        | Undef => _
-        | Datum8 _ => _
-        | Datum16 _ => _
-        | Datum32 _ => _
-        | Datum64 _ => _
-        | Cont => _ 
-        end = _) =>
-    elim (getN_setN_mismatch sz1 sz2 ofs v c);
-    [ let H := fresh in (intro H; rewrite H; reflexivity)
-    | let H := fresh in (intro H; rewrite H; reflexivity) ]
-  end.
-
-Lemma load_store_contents_mismatch:
-  forall (sz1 sz2: memory_size) (c: contentmap) 
-         (ofs: Z) (v: val),
-  sz1 <> sz2 ->
-  load_contents sz2 (store_contents sz1 c ofs v) ofs = Vundef.
-Proof.
-  intros.
-  destruct sz1; destruct sz2; simpl; LSCM.
-Qed.  
-
-Theorem low_bound_store:
-  forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs: Z) (v: val),
-  store chunk m1 b ofs v = Some m2 ->
-  low_bound m2 b' = low_bound m1 b'.
-Proof.
-  intros.
-  generalize (store_inv _ _ _ _ _ _ H).
-  intros (A, (B, (C, (D, (P, E))))).
-  unfold low_bound. rewrite E; unfold update.
-  case (zeq b' b); intro.
-  subst b'. reflexivity.
-  reflexivity.
-Qed.
-
-Theorem high_bound_store:
-  forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs: Z) (v: val),
-  store chunk m1 b ofs v = Some m2 ->
-  high_bound m2 b' = high_bound m1 b'.
-Proof.
-  intros.
-  generalize (store_inv _ _ _ _ _ _ H).
-  intros (A, (B, (C, (D, (P, E))))).
-  unfold high_bound. rewrite E; unfold update.
-  case (zeq b' b); intro.
-  subst b'. reflexivity.
-  reflexivity. 
-Qed.
-
-Hint Resolve high_bound_store low_bound_store load_store_contents_mismatch
-  load_store_contents_overlap load_store_other store_is_in_bounds  
-  load_store_contents_same  load_store_same load_store_contents_other.
-
-(** * Agreement between memory blocks. *)
-
-(** Two memory blocks [c1] and [c2] agree on a range [lo] to [hi]
-  if they associate the same contents to byte offsets in the range
-  [lo] (included) to [hi] (excluded). *)
-
-Definition contentmap_agree (lo hi: Z) (c1 c2: contentmap) :=
-  forall (ofs: Z),
-    lo <= ofs < hi -> c1 ofs = c2 ofs.
-
-Definition block_contents_agree (lo hi: Z) (c1 c2: block_contents) :=
-  contentmap_agree lo hi c1.(contents) c2.(contents).
-
-Definition block_agree (b: block) (lo hi: Z) (m1 m2: mem) :=
-  block_contents_agree lo hi
-     (m1.(blocks) b) (m2.(blocks) b).
-
-Theorem block_agree_refl:
-  forall (m: mem) (b: block) (lo hi: Z),
-  block_agree b lo hi m m.
-Proof.
-  intros. hnf. auto.
-Qed.
-
-Theorem block_agree_sym:
-  forall (m1 m2: mem) (b: block) (lo hi: Z),
-  block_agree b lo hi m1 m2 ->
-  block_agree b lo hi m2 m1.
-Proof.
-  intros. hnf. intros. symmetry. apply H. auto.
-Qed.
-
-Theorem block_agree_trans:
-  forall (m1 m2 m3: mem) (b: block) (lo hi: Z),
-  block_agree b lo hi m1 m2 ->
-  block_agree b lo hi m2 m3 ->
-  block_agree b lo hi m1 m3.
-Proof.
-  intros. hnf. intros. 
-  transitivity (contents (blocks m2 b) ofs).
-  apply H; auto. apply H0; auto.
-Qed.
-
-Lemma check_cont_agree:
-  forall (c1 c2: contentmap) (lo hi: Z),
-  contentmap_agree lo hi c1 c2 ->
-  forall (n: nat) (ofs: Z),
-  lo <= ofs -> ofs + Z_of_nat n <= hi ->
-  check_cont n ofs c2 = check_cont n ofs c1.
-Proof.
-  induction n; intros; simpl.
-  auto.
-  rewrite inj_S in H1.
-  rewrite H. case (c2 ofs); intros; auto. 
-  apply IHn; omega.
-  omega.
-Qed.
-
-Lemma getN_agree:
-  forall (c1 c2: contentmap) (lo hi: Z),
-  contentmap_agree lo hi c1 c2 ->
-  forall (n: nat) (ofs: Z),
-  lo <= ofs -> ofs + Z_of_nat n < hi ->
-  getN n ofs c2 = getN n ofs c1.
-Proof.
-  intros. unfold getN. 
-  rewrite (check_cont_agree c1 c2 lo hi H n (ofs + 1)).
-  case (check_cont n (ofs + 1) c1).
-  symmetry. apply H. omega. auto.
-  omega. omega.
-Qed.
-
-Lemma load_contentmap_agree:
-  forall (sz: memory_size) (c1 c2: contentmap) (lo hi ofs: Z),
-  contentmap_agree lo hi c1 c2 ->
-  lo <= ofs -> ofs + size_mem sz <= hi ->
-  load_contents sz c2 ofs = load_contents sz c1 ofs.
-Proof.
-  intros sz c1 c2 lo hi ofs EX LO.
-  unfold load_contents, size_mem; case sz; intro HI;
-  rewrite (getN_agree c1 c2 lo hi EX); auto; simpl Z_of_nat; omega.
-Qed.
-
-Lemma set_cont_agree:
-  forall (lo hi: Z) (n: nat) (c1 c2: contentmap) (ofs: Z),
-  contentmap_agree lo hi c1 c2 ->
-  contentmap_agree lo hi (set_cont n ofs c1) (set_cont n ofs c2).
-Proof.
-  induction n; simpl; intros.
-  auto.
-  red. intros p B. 
-  case (zeq p ofs); intro.
-  subst p. repeat (rewrite update_s). reflexivity.
-  repeat (rewrite update_o). apply IHn. assumption.
-  assumption. auto. auto.
-Qed.
-
-Lemma setN_agree:
-  forall (lo hi: Z) (n: nat) (c1 c2: contentmap) (ofs: Z) (v: content),
-  contentmap_agree lo hi c1 c2 ->
-  contentmap_agree lo hi (setN n ofs v c1) (setN n ofs v c2).
-Proof.
-  intros. unfold setN. red; intros p B.
-  case (zeq p ofs); intro.
-  subst p. repeat (rewrite update_s). reflexivity.
-  repeat (rewrite update_o; auto). 
-  exact (set_cont_agree lo hi n c1 c2 (ofs + 1) H p B).  
-Qed.
-
-Lemma store_contentmap_agree:
-  forall (sz: memory_size) (c1 c2: contentmap) (lo hi ofs: Z) (v: val),
-  contentmap_agree lo hi c1 c2 ->
-  contentmap_agree lo hi
-       (store_contents sz c1 ofs v) (store_contents sz c2 ofs v).
-Proof.
-  intros. unfold store_contents; case sz; apply setN_agree; auto.
-Qed.
-
-Lemma set_cont_outside_agree:
-  forall (lo hi: Z) (n: nat) (c1 c2: contentmap) (ofs: Z),
-  contentmap_agree lo hi c1 c2 ->
-  ofs + Z_of_nat n <= lo \/ hi <= ofs ->
-  contentmap_agree lo hi c1 (set_cont n ofs c2).
-Proof.
-  induction n; intros; simpl.
-  auto.
-  red; intros p R. rewrite inj_S in H0.
-  unfold update. case (zeq p ofs); intro.
-  subst p. omegaContradiction.
-  apply IHn. auto. omega. auto. 
-Qed.
-
-Lemma setN_outside_agree:
-  forall (lo hi: Z) (n: nat) (c1 c2: contentmap) (ofs: Z) (v: content),
-  contentmap_agree lo hi c1 c2 ->
-  ofs + Z_of_nat n < lo \/ hi <= ofs ->
-  contentmap_agree lo hi c1 (setN n ofs v c2).
-Proof.
-  intros. unfold setN. red; intros p R.
-  unfold update. case (zeq p ofs); intro.
-  omegaContradiction.
-  apply (set_cont_outside_agree lo hi n c1 c2 (ofs + 1) H).
-  omega. auto.
-Qed.
-
-Lemma store_contentmap_outside_agree:
-  forall (sz: memory_size) (c1 c2: contentmap) (lo hi ofs: Z) (v: val),
-  contentmap_agree lo hi c1 c2 ->
-  ofs + size_mem sz <= lo \/ hi <= ofs ->
-  contentmap_agree lo hi c1 (store_contents sz c2 ofs v).
-Proof.
-  intros until v.
-  unfold store_contents; case sz; simpl; intros;
-  apply setN_outside_agree; auto; simpl Z_of_nat; omega.
-Qed.
-
-Theorem load_agree:
-  forall (chunk: memory_chunk) (m1 m2: mem) 
-         (b: block) (lo hi: Z) (ofs: Z) (v1 v2: val),
-  block_agree b lo hi m1 m2 ->
-  lo <= ofs -> ofs + size_chunk chunk <= hi ->
-  load chunk m1 b ofs = Some v1 ->
-  load chunk m2 b ofs = Some v2 ->
-  v1 = v2.
-Proof.
-  intros. 
-  generalize (load_inv _ _ _ _ _ H2). intros [K [L [M N]]].
-  generalize (load_inv _ _ _ _ _ H3). intros [P [Q [R S]]].
-  subst v1; subst v2. symmetry.
-  decEq. eapply load_contentmap_agree. 
-  apply H. auto. auto. 
-Qed.
-
-Theorem store_agree:
-  forall (chunk: memory_chunk) (m1 m2 m1' m2': mem)
-         (b: block) (lo hi: Z)
-         (b': block) (ofs: Z) (v: val),
-  block_agree b lo hi m1 m2 ->
-  store chunk m1 b' ofs v = Some m1' ->
-  store chunk m2 b' ofs v = Some m2' ->
-  block_agree b lo hi m1' m2'.
-Proof.
-  intros.
-  generalize (store_inv _ _ _ _ _ _ H0).
-  intros [I [J [K [L [x M]]]]].
-  generalize (store_inv _ _ _ _ _ _ H1).
-  intros [P [Q [R [S [y T]]]]].
-  red. red. 
-  rewrite M; rewrite T; unfold update.
-  case (zeq b b'); intro; simpl.
-  subst b'. apply store_contentmap_agree. assumption.
-  apply H. 
-Qed.
-
-Theorem store_outside_agree:
-  forall (chunk: memory_chunk) (m1 m2 m2': mem)
-         (b: block) (lo hi: Z)
-         (b': block) (ofs: Z) (v: val),
-  block_agree b lo hi m1 m2 ->
-  b <> b' \/ ofs + size_chunk chunk <= lo \/ hi <= ofs ->
-  store chunk m2 b' ofs v = Some m2' ->
-  block_agree b lo hi m1 m2'.
-Proof.
-  intros.
-  generalize (store_inv _ _ _ _ _ _ H1).
-  intros [I [J [K [L [x M]]]]].
-  red. red. rewrite M; unfold update;
-  case (zeq b b'); intro; simpl. 
-  subst b'. apply store_contentmap_outside_agree.
-  assumption. 
-  elim H0; intro. tauto. exact H2.
-  apply H.
-Qed.
-
-(** * Store extensions *)
-
-(** A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
-  by increasing the sizes of the memory blocks of [m1] (decreasing
-  the low bounds, increasing the high bounds), while still keeping the
-  same contents for block offsets that are valid in [m1]. 
-  This notion is used in the proof of semantic equivalence in 
-  module [Machenv]. *)
-
-Definition block_contents_extends (c1 c2: block_contents) :=
-  c2.(low) <= c1.(low) /\ c1.(high) <= c2.(high) /\
-  contentmap_agree c1.(low) c1.(high) c1.(contents) c2.(contents).
-
-Definition extends (m1 m2: mem) :=
-  m1.(nextblock) = m2.(nextblock) /\
-  forall (b: block),
-  b < m1.(nextblock) ->
-  block_contents_extends (m1.(blocks) b) (m2.(blocks) b).
-
-Theorem extends_refl:
-  forall (m: mem), extends m m.
-Proof.
-  intro. red. split.
-  reflexivity.
-  intros. red. 
-  split. omega. split. omega. 
-  red. intros. reflexivity.
-Qed.
-
-Theorem alloc_extends:
-  forall (m1 m2 m1' m2': mem) (lo1 hi1 lo2 hi2: Z) (b1 b2: block),
-  extends m1 m2 ->
-  lo2 <= lo1 -> hi1 <= hi2 ->
-  alloc m1 lo1 hi1 = (m1', b1) ->
-  alloc m2 lo2 hi2 = (m2', b2) ->
-  b1 = b2 /\ extends m1' m2'.
-Proof.
-  unfold extends, alloc; intros.
-  injection H2; intros; subst m1'; subst b1.
-  injection H3; intros; subst m2'; subst b2.
-  simpl. intuition.
-  rewrite <- H4. case (zeq b (nextblock m1)); intro.
-  subst b. repeat rewrite update_s.
-  red; simpl. intuition. 
-  red; intros; reflexivity.
-  repeat rewrite update_o.  apply H5.  omega.
-  auto. auto.
-Qed.
-
-Theorem free_extends:
-  forall (m1 m2: mem) (b: block),
-  extends m1 m2 ->
-  extends (free m1 b) (free m2 b).
-Proof.
-  unfold extends, free; intros.
-  simpl. intuition. 
-  red; intros; simpl. 
-  case (zeq b0 b); intro.
-  subst b0; repeat (rewrite update_s). 
-  simpl. split. omega. split. omega. 
-  red. intros. omegaContradiction. 
-  repeat (rewrite update_o). 
-  exact (H1 b0 H).
-  auto. auto.  
-Qed.
-
-Theorem load_extends:
-  forall (chunk: memory_chunk) (m1 m2: mem) (b: block) (ofs: Z) (v: val),
-  extends m1 m2 ->
-  load chunk m1 b ofs = Some v ->
-  load chunk m2 b ofs = Some v.
-Proof.
-  intros sz m1 m2 b ofs v (X, Y) L.
-  generalize (load_inv _ _ _ _ _ L).
-  intros (A, (B, (C, D))).
-  unfold load. rewrite <- X. rewrite zlt_true; auto.
-  generalize (Y b A); intros [M [P Q]].
-  rewrite in_bounds_holds.
-  rewrite <- D. 
-  decEq. decEq.
-  apply load_contentmap_agree with
-    (lo := low((blocks m1) b))
-    (hi := high((blocks m1) b)); auto.
-  omega. omega. 
-Qed.
-
-Theorem store_within_extends:
-  forall (chunk: memory_chunk) (m1 m2 m1': mem) (b: block) (ofs: Z) (v: val),
-  extends m1 m2 ->
-  store chunk m1 b ofs v = Some m1' ->
-  exists m2', store chunk m2 b ofs v = Some m2' /\ extends m1' m2'.
-Proof.
-  intros sz m1 m2 m1' b ofs v (X, Y) STORE.
-  generalize (store_inv _ _ _ _ _ _ STORE).
-  intros (A, (B, (C, (D, (x, E))))).
-  generalize (Y b A); intros [M [P Q]].
-  unfold store. rewrite <- X. rewrite zlt_true; auto.
-  case (in_bounds sz ofs (blocks m2 b)); intro.
-  exists (unchecked_store sz m2 b ofs v a).
-  split. auto.
-  split. 
-  unfold unchecked_store; simpl. congruence.
-  intros b' LT. 
-  unfold block_contents_extends, unchecked_store, block_contents_agree.
-  rewrite E; unfold update; simpl.
-  case (zeq b' b); intro; simpl.
-  subst b'. split. omega. split. omega. 
-  apply store_contentmap_agree. auto.
-  apply Y. rewrite <- D. auto.
-  omegaContradiction.
-Qed.
-
-Theorem store_outside_extends:
-  forall (chunk: memory_chunk) (m1 m2 m2': mem) (b: block) (ofs: Z) (v: val),
-  extends m1 m2 ->
-  ofs + size_chunk chunk <= low_bound m1 b \/ high_bound m1 b <= ofs ->
-  store chunk m2 b ofs v = Some m2' ->
-  extends m1 m2'.
-Proof.
-  intros sz m1 m2 m2' b ofs v (X, Y) BOUNDS STORE.
-  generalize (store_inv _ _ _ _ _ _ STORE).
-  intros (A, (B, (C, (D, (x, E))))).
-  split.
-  congruence.
-  intros b' LT.
-  rewrite E; unfold update; case (zeq b' b); intro.
-  subst b'. generalize (Y b LT). intros [M [P Q]].
-  red; simpl. split. omega. split. omega. 
-  apply store_contentmap_outside_agree.
-  assumption. exact BOUNDS. 
-  auto. 
-Qed.
-
-(** * Memory extensionality properties *)
-
-Lemma block_contents_exten:
-  forall (c1 c2: block_contents),
-  c1.(low) = c2.(low) ->
-  c1.(high) = c2.(high) ->
-  block_contents_agree c1.(low) c1.(high) c1 c2 ->
-  c1 = c2.
-Proof.
-  intros. caseEq c1; intros lo1 hi1 m1 UO1 EQ1. subst c1.
-  caseEq c2; intros lo2 hi2 m2 UO2 EQ2. subst c2.
-  simpl in *. subst lo2 hi2. 
-  assert (m1 = m2). 
-    unfold contentmap. apply extensionality. intro.
-    case (zlt x lo1); intro.
-    rewrite UO1. rewrite UO2. auto. tauto. tauto.
-    case (zlt x hi1); intro.
-    apply H1. omega.
-    rewrite UO1. rewrite UO2. auto. tauto. tauto.
-  subst m2. 
-  assert (UO1 = UO2).
-    apply proof_irrelevance.
-  subst UO2. reflexivity.
-Qed.
-
-Theorem mem_exten:
-  forall m1 m2,
-  m1.(nextblock) = m2.(nextblock) ->
-  (forall b, m1.(blocks) b = m2.(blocks) b) ->
-  m1 = m2.
-Proof.
-  intros. destruct m1 as [map1 nb1 nextpos1]. destruct m2 as [map2 nb2 nextpos2].
-  simpl in *. subst nb2. 
-  assert (map1 = map2). apply extensionality. assumption.
-  assert (nextpos1 = nextpos2). apply proof_irrelevance. 
-  congruence.
-Qed.
-
-(** * Store injections *)
-
-(** A memory injection [f] is a function from addresses to either [None]
-  or [Some] of an address and an offset.  It defines a correspondence
-  between the blocks of two memory states [m1] and [m2]:
-- if [f b = None], the block [b] of [m1] has no equivalent in [m2];
-- if [f b = Some(b', ofs)], the block [b] of [m2] corresponds to
-  a sub-block at offset [ofs] of the block [b'] in [m2].
-*)
-
-Definition meminj := (block -> option (block * Z))%type.
-
-Section MEM_INJECT.
-
-Variable f: meminj.
-
-(** A memory injection defines a relation between values that is the
-  identity relation, except for pointer values which are shifted
-  as prescribed by the memory injection. *)
-
-Inductive val_inject: val -> val -> Prop :=
-  | val_inject_int:
-      forall i, val_inject (Vint i) (Vint i)
-  | val_inject_float:
-      forall f, val_inject (Vfloat f) (Vfloat f)
-  | val_inject_ptr:
-      forall b1 ofs1 b2 ofs2 x,
-      f b1 = Some (b2, x) ->
-      ofs2 = Int.add ofs1 (Int.repr x) ->
-      val_inject (Vptr b1 ofs1) (Vptr b2 ofs2)
-  | val_inject_undef: forall v,
-      val_inject Vundef v.
-
-Hint Resolve val_inject_int val_inject_float val_inject_ptr 
-val_inject_undef.
-
-Inductive val_list_inject: list val -> list val-> Prop:= 
-  | val_nil_inject :
-      val_list_inject nil nil
-  | val_cons_inject : forall v v' vl vl' , 
-      val_inject v v' -> val_list_inject vl vl'->
-      val_list_inject (v::vl) (v':: vl').  
-
-Inductive val_content_inject: memory_size -> val -> val -> Prop :=
-  | val_content_inject_base:
-      forall sz v1 v2,
-      val_inject v1 v2 ->
-      val_content_inject sz v1 v2
-  | val_content_inject_8:
-      forall n1 n2,
-      Int.cast8unsigned n1 = Int.cast8unsigned n2 ->
-      val_content_inject Size8 (Vint n1) (Vint n2)
-  | val_content_inject_16:
-      forall n1 n2,
-      Int.cast16unsigned n1 = Int.cast16unsigned n2 ->
-      val_content_inject Size16 (Vint n1) (Vint n2)
-  | val_content_inject_32:
-      forall f1 f2,
-      Float.singleoffloat f1 = Float.singleoffloat f2 ->
-      val_content_inject Size32 (Vfloat f1) (Vfloat f2).
-
-Hint Resolve val_content_inject_base.
-
-Inductive content_inject: content -> content -> Prop :=
-  | content_inject_undef: 
-      forall c,
-      content_inject Undef c
-  | content_inject_datum8:
-      forall v1 v2,
-      val_content_inject Size8 v1 v2 ->
-      content_inject (Datum8 v1) (Datum8 v2)
-  | content_inject_datum16:
-      forall v1 v2,
-      val_content_inject Size16 v1 v2 ->
-      content_inject (Datum16 v1) (Datum16 v2)
-  | content_inject_datum32:
-      forall v1 v2,
-      val_content_inject Size32 v1 v2 ->
-      content_inject (Datum32 v1) (Datum32 v2)
-  | content_inject_datum64:
-      forall v1 v2,
-      val_content_inject Size64 v1 v2 ->
-      content_inject (Datum64 v1) (Datum64 v2)
-  | content_inject_cont:
-      content_inject Cont Cont.
-
-Hint Resolve content_inject_undef content_inject_datum8 
-content_inject_datum16 content_inject_datum32 content_inject_datum64
-content_inject_cont.
-
-Definition contentmap_inject (c1 c2: contentmap) (lo hi delta: Z) : Prop :=
-  forall x, lo <= x < hi ->
-    content_inject (c1 x) (c2 (x + delta)).
-
-(** A block contents [c1] injects into another block content [c2] at
-  offset [delta] if the contents of [c1] at all valid offsets
-  correspond to the contents of [c2] at the same offsets shifted by [delta].
-  Some additional conditions are imposed to guard against arithmetic
-  overflow in address computations. *)
-
-Record block_contents_inject (c1 c2: block_contents) (delta: Z) : Prop :=
-  mk_block_contents_inject {
-    bci_range1: Int.min_signed <= delta <= Int.max_signed;
-    bci_range2: delta = 0 \/
-                (Int.min_signed <= c2.(low) /\ c2.(high) <= Int.max_signed);
-    bci_lowhigh:forall x, c1.(low) <= x < c1.(high) ->
-                          c2.(low) <= x+delta < c2.(high) ;
-    bci_contents: 
-      contentmap_inject c1.(contents) c2.(contents) c1.(low) c1.(high) delta
-  }.
-
-(** A memory state [m1] injects into another memory state [m2] via the
-  memory injection [f] if the following conditions hold:
-- unallocated blocks in [m1] must be mapped to [None] by [f];
-- if [f b = Some(b', delta)], [b'] must be valid in [m2] and
-  the contents of [b] in [m1] must inject into the contents of [b'] in [m2]
-  with offset [delta];
-- distinct blocks in [m1] cannot be mapped to overlapping sub-blocks in [m2].
-*)
-
-Record mem_inject (m1 m2: mem) : Prop :=
-  mk_mem_inject {
-    mi_freeblocks:
-      forall b, b >= m1.(nextblock) -> f b = None;
-    mi_mappedblocks:
-      forall b b' delta,
-      f b = Some(b', delta) ->
-      b' < m2.(nextblock) /\
-      block_contents_inject (m1.(blocks) b) 
-                            (m2.(blocks) b') 
-                            delta;
-    mi_no_overlap:
-      forall b1 b2 b1' b2' delta1 delta2,
-      b1 <> b2 ->
-      f b1 = Some (b1', delta1) ->
-      f b2 = Some (b2', delta2) ->
-      b1' <> b2' 
-      \/ (forall x1 x2, low_bound m1 b1 <= x1 < high_bound m1 b1 ->
-                              low_bound m1 b2 <= x2 < high_bound m1 b2 ->
-                              x1+delta1 <> x2+delta2)
- }.
-
-(** The following lemmas establish the absence of machine integer overflow
-  during address computations. *)
-
-Lemma size_mem_pos: forall sz, size_mem sz > 0.
-Proof.  destruct sz; simpl; omega. Qed.
-
-Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0.
-Proof. intros. unfold size_chunk. apply size_mem_pos. Qed.
-
-Lemma address_inject:
-  forall m1 m2 chunk b1 ofs1 b2 ofs2 x,
-  mem_inject m1 m2 ->
-  (m1.(blocks) b1).(low) <= Int.signed ofs1 ->
-  Int.signed ofs1 + size_chunk chunk <= (m1.(blocks) b1).(high) ->
-  f b1 = Some (b2, x) ->
-  ofs2 = Int.add ofs1 (Int.repr x) ->
-  Int.signed ofs2 = Int.signed ofs1 + x.
-Proof.
-  intros. 
-  generalize (size_chunk_pos chunk). intro.
-  generalize (mi_mappedblocks m1 m2 H _ _ _ H2). intros [C D].
-  inversion D. 
-  elim  bci_range4 ; intro. 
-  (**x=0**)
-  subst x .  rewrite Zplus_0_r.  rewrite Int.add_zero in H3. 
-  subst ofs2 ; auto . 
-  (**x<>0**)
-  rewrite H3. rewrite Int.add_signed. repeat rewrite Int.signed_repr.
-  auto.  auto.
-  assert (low (blocks m1 b1) <= Int.signed ofs1 < high (blocks m1 b1)).
-  omega.
-  generalize (bci_lowhigh0 (Int.signed ofs1) H6). omega.
-  auto.
-Qed.
-
-Lemma valid_pointer_inject_no_overflow:
-  forall m1 m2 b ofs b' x,
-  mem_inject m1 m2 ->
-  valid_pointer m1 b (Int.signed ofs) = true ->
-  f b = Some(b', x) ->
-  Int.min_signed <= Int.signed ofs + Int.signed (Int.repr x) <= Int.max_signed.
-Proof.
-  intros. unfold valid_pointer in H0.
-  destruct (zlt b (nextblock m1)); try discriminate.
-  destruct (zle (low (blocks m1 b)) (Int.signed ofs)); try discriminate.
-  destruct (zlt (Int.signed ofs) (high (blocks m1 b))); try discriminate.
-  inversion H. generalize (mi_mappedblocks0 _ _ _ H1).
-  intros [A B]. inversion B. 
-  elim  bci_range4 ; intro. 
-  (**x=0**)
-  rewrite Int.signed_repr ; auto.  
-  subst x .  rewrite Zplus_0_r.  apply Int.signed_range . 
-  (**x<>0**)
-  generalize (bci_lowhigh0 _ (conj z0 z1)). intro.
-  rewrite Int.signed_repr. omega. auto.
-Qed.
-
-(** Relation between injections and loads. *)
-
-Lemma check_cont_inject:
-  forall c1 c2 lo hi delta,
-  contentmap_inject c1 c2 lo hi delta ->
-  forall n p,
-  lo <= p -> p + Z_of_nat n <= hi ->
-  check_cont n p c1 = true ->
-  check_cont n (p + delta) c2 = true.
-Proof.
-  induction n.
-  intros. simpl. reflexivity.
-  simpl check_cont. rewrite inj_S. intros p H0 H1.
-  assert (lo <= p < hi). omega.  
-  generalize (H p H2). intro. inversion H3; intros; try discriminate.
-  replace (p + delta + 1) with ((p + 1) + delta). 
-  apply IHn. omega. omega. auto. 
-  omega.
-Qed.
-
-Hint Resolve check_cont_inject.
-
-Lemma getN_inject:
-  forall c1 c2 lo hi delta,
-  contentmap_inject c1 c2 lo hi delta ->
-  forall n p,
-  lo <= p -> p + Z_of_nat n < hi ->
-  content_inject (getN n p c1) (getN n (p + delta) c2).
-Proof.
-  intros. simpl in H1.
-  assert (lo <= p < hi). omega.
-  unfold getN.
-  caseEq (check_cont n (p + 1) c1); intro.
-  replace (check_cont n (p + delta + 1) c2) with true.
-  apply H. assumption. 
-  symmetry. replace (p + delta + 1) with ((p + 1) + delta).
-  eapply check_cont_inject; eauto.
-  omega. omega. omega.
-  constructor. 
-Qed.
-
-Hint Resolve getN_inject.
-
-Definition ztonat (z:Z): nat:=
-match z with
-| Z0 => O
-| Zpos p =>  (nat_of_P p)
-| Zneg p =>O 
-end.
-
-Lemma load_contents_inject:
-  forall sz c1 c2 lo hi delta p,
-  contentmap_inject c1 c2 lo hi delta ->
-  lo <= p -> p + size_mem sz <= hi ->
-  val_content_inject sz (load_contents sz c1 p) (load_contents sz c2 (p + delta)).
-Proof.
-intros.
-assert (content_inject (getN (ztonat (size_mem sz)-1) p c1) 
-(getN (ztonat(size_mem sz)-1) (p + delta) c2)).
-induction sz; assert (lo<= p< hi); simpl in H1; try omega;
-apply getN_inject with lo hi; try assumption; simpl ; try omega. 
-induction sz ; simpl; inversion H2; auto.
-Qed.
-
-Hint Resolve load_contents_inject.
-
-Lemma load_result_inject:
-  forall chunk v1 v2,
-  val_content_inject (mem_chunk chunk) v1 v2 ->
-  val_inject (Val.load_result chunk v1) (Val.load_result chunk v2).
-Proof.
-intros.
-destruct chunk; simpl in H; inversion H; simpl; auto;
-try (inversion H0; simpl; auto; fail).
-replace (Int.cast8signed n2) with (Int.cast8signed n1). constructor. 
-apply Int.cast8_signed_equal_if_unsigned_equal; auto.
-rewrite H0; constructor.
-replace (Int.cast16signed n2) with (Int.cast16signed n1). constructor. 
-apply Int.cast16_signed_equal_if_unsigned_equal; auto.
-rewrite H0; constructor.
-inversion H0; simpl; auto. 
-apply val_inject_ptr with x; auto.
-Qed.
-
-Lemma in_bounds_inject:
-  forall chunk c1 c2 delta p,
-  block_contents_inject c1 c2 delta ->
-  c1.(low) <= p /\ p + size_chunk chunk <= c1.(high) ->
-  c2.(low) <= p + delta /\ (p + delta) + size_chunk chunk <= c2.(high).
-Proof.
-  intros.
-  inversion H. 
-  generalize (size_chunk_pos chunk); intro.
-  assert (low c1 <= p + size_chunk chunk - 1 < high c1).
-  omega.
-  generalize (bci_lowhigh0 _ H2). intro.
-  assert (low c1 <= p < high c1).
-  omega.
-  generalize (bci_lowhigh0 _ H4). intro.
-  omega. 
-Qed.
-
-Lemma block_cont_val:
-forall c1 c2 delta p sz,
-block_contents_inject c1 c2 delta ->
-c1.(low) <= p -> p + size_mem sz <= c1.(high) ->
-  val_content_inject sz (load_contents sz c1.(contents) p) 
-    (load_contents sz c2.(contents) (p + delta)).
-Proof.
-intros.
-inversion H .
-apply load_contents_inject with c1.(low) c1.(high) ;assumption. 
-Qed.
-
-Lemma load_inject:
-  forall m1 m2 chunk b1 ofs b2 delta v1,
-  mem_inject m1 m2 ->
-  load chunk m1 b1 ofs = Some v1 ->
-  f b1 = Some (b2, delta) ->
-  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject v1 v2.
-Proof.
-  intros.
-  generalize (load_inv _ _ _ _ _ H0).  intros [A [B [C D]]].
-  inversion H.
-  generalize (mi_mappedblocks0 _ _ _ H1). intros [U V].
-  inversion V.
-  exists (Val.load_result chunk (load_contents (mem_chunk chunk)
-           (m2.(blocks) b2).(contents) (ofs+delta))). 
-  split.
-  unfold load. 
-  generalize (size_chunk_pos chunk); intro. 
-  rewrite zlt_true. rewrite in_bounds_holds. auto.
-  assert (low (blocks m1 b1) <= ofs < high (blocks m1 b1)).
-    omega.
-  generalize (bci_lowhigh0 _ H3). tauto.
-  assert (low (blocks m1 b1) <= ofs + size_chunk chunk - 1 < high(blocks m1 b1)).
-    omega.
-  generalize (bci_lowhigh0 _ H3). omega.
-  assumption.
-  rewrite <- D. apply load_result_inject. 
-  eapply load_contents_inject; eauto.
-Qed.
-
-Lemma loadv_inject:
-  forall m1 m2 chunk a1 a2 v1,
-  mem_inject m1 m2 ->
-  loadv chunk m1 a1 = Some v1 ->
-  val_inject a1 a2 ->
-  exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject v1 v2.
-Proof.
-  intros.
-  induction H1 ; simpl in H0 ; try discriminate H0.
-  simpl. 
-  replace (Int.signed ofs2) with (Int.signed ofs1 + x).
-  apply load_inject with m1 b1 ; assumption.
-  symmetry. generalize (load_inv _ _ _ _ _ H0). intros [A [B [C D]]].
-  apply address_inject with m1 m2 chunk b1 b2; auto.
-Qed.
-
-(** Relation between injections and stores. *)
-
-Lemma set_cont_inject:
-  forall c1 c2 lo hi delta,
-  contentmap_inject c1 c2 lo hi delta ->
-  forall n p,
-  lo <= p -> p + Z_of_nat n <= hi ->
-  contentmap_inject (set_cont n p c1) (set_cont n (p + delta) c2) lo hi delta.
-Proof.
-induction n. intros. simpl. assumption.
-intros. simpl. unfold contentmap_inject.
-intros p2 Hp2. unfold update.
-case (zeq p2 p); intro.
-subst p2. rewrite zeq_true. constructor.
-rewrite zeq_false. replace (p + delta + 1) with ((p + 1) + delta).
-apply IHn. omega. rewrite inj_S in H1. omega. assumption.
-omega. omega.
-Qed.
-
-Lemma setN_inject:
-  forall c1 c2 lo hi delta n p v1 v2,
-  contentmap_inject c1 c2 lo hi delta ->
-  content_inject v1 v2 ->
-  lo <= p -> p + Z_of_nat n < hi ->
-  contentmap_inject (setN n p v1 c1) (setN n (p + delta) v2 c2)
-                    lo hi delta.
-Proof.
-  intros. unfold setN. red; intros.
-  unfold update. 
-  case (zeq x p); intro. 
-  subst p. rewrite zeq_true. assumption.
-  rewrite zeq_false. 
-  replace (p + delta + 1) with ((p + 1) + delta).
-  apply set_cont_inject with lo hi. 
-  assumption. omega. omega. assumption. omega.
-  omega.
-Qed.
-
-Lemma store_contents_inject:
-  forall c1 c2 lo hi delta sz p v1 v2,
-  contentmap_inject c1 c2 lo hi delta ->
-  val_content_inject sz v1 v2 ->
-  lo <= p -> p + size_mem sz <= hi ->
-  contentmap_inject (store_contents sz c1 p v1) 
-                    (store_contents sz c2 (p + delta) v2)
-                    lo hi delta.
-Proof.
-  intros.
-  destruct sz; simpl in *; apply setN_inject; auto; simpl; omega.
-Qed.
-
-Lemma set_cont_outside1 :
-  forall n  p m q ,
-  (forall x , p <= x < p + Z_of_nat n -> x <> q) ->
-  (set_cont n p m) q = m q.
-Proof.
-  induction n; intros; simpl.
-  auto.
-  rewrite inj_S in H. rewrite update_o. apply IHn.
-  intros. apply H.  omega. 
-  apply H. omega.
-Qed.
-
-Lemma set_cont_outside_inject:
-  forall c1 c2 lo hi delta,
-  contentmap_inject c1 c2 lo hi delta ->
-  forall n p,
-  (forall x1 x2, p <= x1 < p + Z_of_nat n ->
-                 lo <= x2 < hi -> 
-                 x1 <> x2 + delta) ->
-  contentmap_inject c1 (set_cont n p c2) lo hi delta.
-Proof.
-  unfold contentmap_inject. intros.  
-  rewrite set_cont_outside1. apply H. assumption. 
-  intros. apply H0. auto. auto.
-Qed.
-
-Lemma setN_outside_inject:
-  forall n c1 c2 lo hi delta  p v,
-  contentmap_inject c1 c2 lo hi delta ->
-  (forall x1 x2, p <= x1 < p + Z_of_nat (S n) ->
-                 lo <= x2 < hi ->
-                 x1 <> x2 + delta) ->
-  contentmap_inject c1 (setN n p v c2) lo hi delta.
-Proof.
-  intros. unfold setN. red; intros. rewrite update_o.
-  apply set_cont_outside_inject with lo hi. auto.
-  intros. apply H0. rewrite inj_S. omega. auto. auto. 
-  apply H0. rewrite inj_S. omega. auto.
-Qed.
-
-Lemma store_contents_outside_inject:
-  forall c1 c2 lo hi delta sz p v,
-  contentmap_inject c1 c2 lo hi delta ->
-  (forall x1 x2, p <= x1 < p + size_mem sz ->
-                 lo <= x2 < hi ->
-                 x1 <> x2 + delta)->
-  contentmap_inject c1 (store_contents sz c2 p v) lo hi delta.
-Proof.
-  intros c1 c2 lo hi delta sz. generalize (size_mem_pos sz) . intro . 
-  induction sz ;intros ;simpl ; apply setN_outside_inject ; assumption . 
-Qed.
-
-Lemma store_mapped_inject_1:
-  forall chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
-  mem_inject m1 m2 ->
-  store chunk m1 b1 ofs v1 = Some n1 ->
-  f b1 = Some (b2, delta) ->
-  val_content_inject (mem_chunk chunk) v1 v2 ->
-  exists n2,
-    store chunk m2 b2 (ofs + delta) v2 = Some n2
-    /\ mem_inject n1 n2.
-Proof.
-intros. 
-generalize (size_chunk_pos chunk); intro SIZEPOS.
-generalize (store_inv _ _ _ _ _ _ H0).
-intros [A [B [C [D [P E]]]]].
-inversion H.
-generalize (mi_mappedblocks0 _ _ _ H1). intros [U V].
-inversion V.
-generalize (in_bounds_inject _ _ _ _ _ V (conj B C)). intro BND.
-exists  (unchecked_store chunk m2 b2 (ofs+delta) v2 BND).
-split. unfold store.
-rewrite zlt_true; auto.
-case (in_bounds chunk (ofs + delta) (blocks m2 b2)); intro.
-assert (a = BND). apply proof_irrelevance. congruence.
-omegaContradiction.
-constructor.
-intros. apply mi_freeblocks0. rewrite <- D. assumption.
-intros. generalize (mi_mappedblocks0 b b' delta0 H3).
-intros [W Y]. split. simpl. auto.
-rewrite E; simpl. unfold update.
-(* Cas 1: memes blocs b = b1  b'= b2 *)
-case (zeq b b1); intro.
-subst b. assert (b'= b2). congruence. subst b'. 
-assert (delta0 = delta). congruence. subst delta0.
-rewrite zeq_true. inversion Y. constructor; simpl; auto.
-apply store_contents_inject; auto.
-(* Cas 2: blocs differents dans m1 mais mappes sur le meme bloc de m2 *)
-case (zeq b' b2); intro.
-subst b'.  
-inversion Y. constructor; simpl; auto.
-generalize (store_contents_outside_inject _ _ _ _ _ (mem_chunk chunk) 
-  (ofs+delta) v2 bci_contents1).
-intros.
-apply H4. 
-elim (mi_no_overlap0 b b1 b2 b2 delta0 delta n H3 H1).
-tauto.
-unfold high_bound, low_bound. intros. 
-apply sym_not_equal. replace x1 with ((x1 - delta) + delta).
-apply H5. assumption. unfold size_chunk in C. omega. omega. 
-(* Cas 3: blocs differents dans m1 et dans m2 *)
-auto.
-
-unfold high_bound, low_bound. 
-rewrite E; simpl; intros.
-unfold high_bound, low_bound in mi_no_overlap0. 
-unfold update.
-case (zeq b0 b1).
-intro. subst b1. simpl.
-rewrite zeq_false; auto.
-intro. case (zeq b3 b1); intro.
-subst b3. simpl. auto.
-auto.
-Qed.
-
-Lemma store_mapped_inject:
-  forall chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
-  mem_inject m1 m2 ->
-  store chunk m1 b1 ofs v1 = Some n1 ->
-  f b1 = Some (b2, delta) ->
-  val_inject v1 v2 ->
-  exists n2,
-    store chunk m2 b2 (ofs + delta) v2 = Some n2
-    /\ mem_inject n1 n2.
-Proof.
-  intros. eapply store_mapped_inject_1; eauto.
-Qed.
-
-Lemma store_unmapped_inject:
-  forall chunk m1 b1 ofs v1 n1 m2,
-  mem_inject m1 m2 ->
-  store chunk m1 b1 ofs v1 = Some n1 ->
-  f b1 = None ->
-  mem_inject n1 m2.
-Proof.
-intros.
-inversion H.
-generalize (store_inv _ _ _ _ _ _ H0).
-intros [A [B [C [D [P E]]]]].
-constructor.
-rewrite D. assumption.
-intros. elim (mi_mappedblocks0 _ _ _ H2); intros.
-split. auto. 
-rewrite E; unfold update.
-rewrite zeq_false. assumption.
-congruence.
-intros. 
-assert (forall b, low_bound n1 b = low_bound m1 b).
-  intros. unfold low_bound; rewrite E; unfold update.
-  case (zeq b b1); intros. subst b1; reflexivity. reflexivity.
-assert (forall b, high_bound n1 b = high_bound m1 b).
-  intros. unfold high_bound; rewrite E; unfold update.
-  case (zeq b b1); intros. subst b1; reflexivity. reflexivity.
-repeat rewrite H5. repeat rewrite H6. auto.
-Qed.
-
-Lemma storev_mapped_inject_1:
-  forall chunk m1 a1 v1 n1 m2 a2 v2,
-  mem_inject m1 m2 ->
-  storev chunk m1 a1 v1 = Some n1 ->
-  val_inject a1 a2 ->
-  val_content_inject (mem_chunk chunk) v1 v2 ->
-  exists n2,
-    storev chunk m2 a2 v2 = Some n2 /\ mem_inject n1 n2.
-Proof.
-  intros. destruct a1; simpl in H0; try discriminate.
-  inversion H1. subst b.
-  simpl. replace (Int.signed ofs2) with (Int.signed i + x).
-  eapply store_mapped_inject_1; eauto.
-  symmetry. generalize (store_inv _ _ _ _ _ _ H0). intros [A [B [C [D [P E]]]]].
-  apply address_inject with m1 m2 chunk b1 b2; auto.
-Qed.
-
-Lemma storev_mapped_inject:
-  forall chunk m1 a1 v1 n1 m2 a2 v2,
-  mem_inject m1 m2 ->
-  storev chunk m1 a1 v1 = Some n1 ->
-  val_inject a1 a2 ->
-  val_inject v1 v2 ->
-  exists n2,
-    storev chunk m2 a2 v2 = Some n2 /\ mem_inject n1 n2.
-Proof.
-  intros. eapply storev_mapped_inject_1; eauto.
-Qed.
-
-(** Relation between injections and [free] *)
-
-Lemma free_first_inject :
-  forall m1 m2 b,
-  mem_inject m1 m2 ->
-  mem_inject (free m1 b) m2.
-Proof.
-  intros.  inversion H.  constructor . auto.
-  simpl. intros. 
-  generalize (mi_mappedblocks0 b0 b' delta H0).
-  intros [A B] . split. assumption . unfold update.
-  case (zeq b0 b); intro.  inversion B. constructor; simpl; auto.
-  intros.  omega.
-  unfold contentmap_inject.
-  intros. omegaContradiction.
-  auto.  intros. 
-  unfold free . unfold low_bound , high_bound.  simpl. unfold update.
-  case (zeq b1 b);intro.  simpl.
-  right. intros. omegaContradiction.
-  case (zeq b2 b);intro.  simpl.
-  right . intros. omegaContradiction. 
-  unfold low_bound, high_bound in mi_no_overlap0. auto.
-Qed.  
-
-Lemma free_first_list_inject :
-  forall l m1 m2,
-  mem_inject m1 m2 ->
-  mem_inject (free_list m1 l) m2.
-Proof.
-  induction l; simpl; intros.
-  auto.
-  apply free_first_inject. auto.
-Qed.
-
-Lemma free_snd_inject:
-  forall m1 m2 b,
-  (forall b1 delta, f b1 = Some(b, delta) -> 
-                    low_bound m1 b1 >= high_bound m1 b1) ->
-  mem_inject m1 m2 ->
-  mem_inject m1 (free m2 b).
-Proof.
-  intros. inversion H0. constructor. auto.
-  simpl. intros. 
-  generalize (mi_mappedblocks0 b0 b' delta H1).
-  intros [A B] . split. assumption . 
-  inversion B. unfold update.
-  case (zeq b' b); intro.
-  subst b'. generalize (H _ _ H1). unfold low_bound, high_bound; intro.
-  constructor. auto.  elim bci_range4 ; intro.
-  (**delta=0**)
-  left ; auto .  
-  (** delta<>0**)
-  right . 
-  simpl. compute. split; intro; congruence. 
- intros. omegaContradiction.
-  red; intros. omegaContradiction.
-  auto.
-  auto.
-Qed.
-
-Lemma bounds_free_block: 
-  forall m1 b m1' , free m1 b = m1' ->
-  low_bound m1' b >= high_bound m1' b.
-Proof.
-  intros.  unfold free in H.
-  rewrite<- H . unfold low_bound , high_bound .
-  simpl . rewrite update_s. simpl.  omega.  
-Qed.
-
-Lemma free_empty_bounds:
-  forall l m1 ,
-  let m1' := free_list m1 l in
-  (forall b, In b l -> low_bound m1' b >= high_bound m1' b).
-Proof.
-  induction l . intros .  inversion H.  
-  intros.
-  generalize (in_inv H).
-  intro . elim H0.   intro .  subst b.  simpl in m1' .  
-  generalize ( bounds_free_block  
-  (fold_right (fun (b : block) (m : mem) => free m b) m1 l) a m1') . 
-  intros.  apply H1. auto .  intros.  simpl in m1'. unfold m1' . 
-  unfold low_bound , high_bound .  simpl . 
-  unfold update; case (zeq b a); intro; simpl.
-  omega . 
-  unfold low_bound , high_bound in IHl . auto.
-Qed.       
-
-Lemma free_inject:
-  forall m1 m2 l b,
-  (forall b1 delta, f b1 = Some(b, delta) -> In b1 l) ->
-  mem_inject m1 m2 ->
-  mem_inject (free_list m1 l) (free m2 b).
-Proof.
-   intros. apply free_snd_inject. 
-   intros. apply free_empty_bounds. apply H with delta. auto. 
-   apply free_first_list_inject. auto.
-Qed. 
-
-Lemma contents_init_data_inject:
-  forall id, contentmap_inject (contents_init_data 0 id) (contents_init_data 0 id) 0 (size_init_data_list id) 0.
-Proof.
-  intro id0. 
-  set (sz0 := size_init_data_list id0).
-  assert (forall id pos,
-    0 <= pos -> pos + size_init_data_list id <= sz0 ->
-    contentmap_inject (contents_init_data pos id) (contents_init_data pos id) 0 sz0 0).
-  induction id; simpl; intros.
-  red; intros; constructor.
-  assert (forall n dt,
-    size_init_data a = 1 + Z_of_nat n ->
-    content_inject dt dt ->
-    contentmap_inject (setN n pos dt (contents_init_data (pos + size_init_data a) id))
-                      (setN n pos dt (contents_init_data (pos + size_init_data a) id))
-                      0 sz0 0).
-  intros. set (pos' := pos) in |- * at 3. replace pos' with (pos + 0).
-  apply setN_inject. apply IHid. omega. omega. auto. auto. 
-  generalize (size_init_data_list_pos id). omega. unfold pos'; omega.
-  destruct a;
-  try (apply H1; [reflexivity|repeat constructor]).
-  apply IHid. generalize (Zmax2 z 0). omega. simpl in H0; omega.
-
-  apply H. omega. unfold sz0. omega.
-Qed.
-
-End MEM_INJECT.
-
-Hint Resolve val_inject_int val_inject_float val_inject_ptr val_inject_undef.
-Hint Resolve val_nil_inject val_cons_inject.
-
-(** Monotonicity properties of memory injections. *)
-
-Definition inject_incr (f1 f2: meminj) : Prop :=
-  forall b, f1 b = f2 b \/ f1 b = None.
-
-Lemma inject_incr_refl :
-   forall f , inject_incr f f .
-Proof. unfold inject_incr . intros. left . auto . Qed.
-
-Lemma inject_incr_trans :
-  forall f1 f2 f3  , 
-  inject_incr f1 f2 -> inject_incr f2 f3 -> inject_incr f1 f3 .
-Proof .
-  unfold inject_incr . intros . 
-  generalize (H b) . intro . generalize (H0 b) . intro . 
-  elim H1 ; elim H2 ; intros.  
-  rewrite H3 in H4 . left . auto .
-  rewrite H3 in H4 . right . auto .
-  right ; auto . 
-  right ; auto .
-Qed.
-
-Lemma val_inject_incr:
-  forall f1 f2 v v',
-  inject_incr f1 f2 ->
-  val_inject f1 v v' ->
-  val_inject f2 v v'.
-Proof.
-  intros. inversion H0.
-  constructor.
-  constructor.
-  elim (H b1); intro. 
-    apply val_inject_ptr with x. congruence. auto. 
-    congruence.
-  constructor.
-Qed.
-
-Lemma val_list_inject_incr:
-  forall f1 f2 vl vl' ,
-  inject_incr f1 f2 -> val_list_inject f1 vl vl' ->
-  val_list_inject f2 vl vl'.
-Proof.
-  induction vl ;  intros;  inversion H0. auto . 
-  subst a . generalize (val_inject_incr f1 f2 v v' H H3) .  
-  intro .  auto .
-Qed.       
-
-Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.
-
-Section MEM_INJECT_INCR.
-
-Variable f1 f2: meminj.
-Hypothesis INCR: inject_incr f1 f2.
-
-Lemma val_content_inject_incr:
-  forall chunk v v',
-  val_content_inject f1 chunk v v' ->
-  val_content_inject f2 chunk v v'.
-Proof.
-  intros. inversion H.
-  apply val_content_inject_base. eapply val_inject_incr; eauto.
-  apply val_content_inject_8; auto.
-  apply val_content_inject_16; auto.
-  apply val_content_inject_32; auto.
-Qed.
-
-Lemma content_inject_incr:
-  forall c c', content_inject f1 c c' -> content_inject f2 c c'.
-Proof.
-  induction 1; constructor; eapply val_content_inject_incr; eauto.
-Qed.
-
-Lemma contentmap_inject_incr:
-  forall c c' lo hi delta,
-  contentmap_inject f1 c c' lo hi delta -> 
-  contentmap_inject f2 c c' lo hi delta.
-Proof.
-  unfold contentmap_inject; intros.
-  apply content_inject_incr. auto.
-Qed.
-
-Lemma block_contents_inject_incr:
-  forall c c' delta,
-  block_contents_inject f1 c c' delta ->
-  block_contents_inject f2 c c' delta.
-Proof.
-  intros. inversion H. constructor; auto.
-  apply contentmap_inject_incr; auto.
-Qed.
-
-End MEM_INJECT_INCR.
-
-(** Properties of injections and allocations. *)
-
-Definition extend_inject
-       (b: block) (x: option (block * Z)) (f: meminj) : meminj :=
-  fun b' => if eq_block b' b then x else f b'.
-
-Lemma extend_inject_incr:
-  forall f b x,
-  f b = None ->
-  inject_incr f (extend_inject b x f).
-Proof.
-  intros; red; intros. unfold extend_inject. 
-  case (eq_block b0 b); intro. subst b0. right; auto. left; auto.
-Qed.
-
-Lemma alloc_right_inject:
-  forall f m1 m2 lo hi m2' b,
-  mem_inject f m1 m2 ->
-  alloc m2 lo hi = (m2', b) ->
-  mem_inject f m1 m2'.
-Proof.
-  intros. unfold alloc in H0. injection H0; intros A B; clear H0.
-  inversion H.
-  constructor.
-  assumption.
-  intros. generalize (mi_mappedblocks0 _ _ _ H0). intros [C D].
-  rewrite <- B; simpl. split. omega. 
-  rewrite update_o. auto. omega.
-  assumption.
-Qed.
-
-Lemma alloc_unmapped_inject:
-  forall f m1 m2 lo hi m1' b,
-  mem_inject f m1 m2 ->
-  alloc m1 lo hi = (m1', b) ->
-  mem_inject (extend_inject b None f) m1' m2 /\
-  inject_incr f (extend_inject b None f).
-Proof.
-  intros. unfold alloc in H0. injection H0; intros; clear H0.
-  inversion H.
-  assert (inject_incr f (extend_inject b None f)).
-  apply extend_inject_incr. apply mi_freeblocks0. rewrite H1. omega. 
-  split; auto.
-  constructor. 
-  rewrite <- H2; simpl; intros. unfold extend_inject.
-  case (eq_block b0 b); intro. auto. apply mi_freeblocks0. omega.
-  intros until delta. unfold extend_inject at 1. case (eq_block b0 b); intro.
-  intros; discriminate.
-  intros. rewrite <- H2; simpl. rewrite H1. 
-  rewrite update_o; auto. 
-  elim (mi_mappedblocks0 _ _ _ H3). intros A B.
-  split. auto. apply block_contents_inject_incr with f. auto. auto.
-  intros until delta2. unfold extend_inject.
-  case (eq_block b1 b); intro. congruence.
-  case (eq_block b2 b); intro. congruence.
-  rewrite <- H2. unfold low_bound, high_bound; simpl. rewrite H1.
-  repeat rewrite update_o; auto.
-  exact (mi_no_overlap0 b1 b2 b1' b2' delta1 delta2).
-Qed.
-
-Lemma alloc_mapped_inject:
-  forall f m1 m2 lo hi m1' b b' ofs,
-  mem_inject f m1 m2 ->
-  alloc m1 lo hi = (m1', b) ->
-  valid_block m2 b' ->
-  Int.min_signed <= ofs <= Int.max_signed ->
-  Int.min_signed <= low_bound m2 b' ->
-  high_bound m2 b' <= Int.max_signed ->
-  low_bound m2 b' <= lo + ofs ->
-  hi + ofs <= high_bound m2 b' ->
-  (forall b0 ofs0, 
-   f b0 = Some (b', ofs0) -> 
-   high_bound m1 b0 + ofs0 <= lo + ofs \/
-   hi + ofs <= low_bound m1 b0 + ofs0) ->
-  mem_inject (extend_inject b (Some (b', ofs)) f) m1' m2 /\
-  inject_incr f (extend_inject b (Some (b', ofs)) f).
-Proof.
-  intros. 
-  generalize (fun b' => low_bound_alloc _ _ b' _ _ _ H0).
-  intro LOW.
-  generalize (fun b' => high_bound_alloc _ _ b' _ _ _ H0).
-  intro HIGH.
-  unfold alloc in H0. injection H0; intros A B; clear H0.
-  inversion H.
-  (* inject_incr *)
-  assert (inject_incr f (extend_inject b (Some (b', ofs)) f)).
-  apply extend_inject_incr. apply mi_freeblocks0. rewrite A. omega. 
-  split; auto.
-  constructor. 
-  (* mi_freeblocks *)
-  rewrite <- B; simpl; intros. unfold extend_inject.
-  case (eq_block b0 b); intro. unfold block in *. omegaContradiction.
-  apply mi_freeblocks0. omega.
-  (* mi_mappedblocks *)
-  intros until delta. unfold extend_inject at 1. 
-  case (eq_block b0 b); intro.
-  intros. subst b0. inversion H8. subst b'0; subst delta. 
-  split. assumption. 
-  rewrite <- B; simpl. rewrite A. rewrite update_s.
-  constructor; auto.
-  unfold empty_block. simpl. intros. unfold low_bound in H5. unfold high_bound in H6. omega.
-  simpl. red; intros. constructor.
-  intros. 
-  generalize (mi_mappedblocks0 _ _ _ H8). intros [C D].
-  split. auto. 
-  rewrite <- B; simpl; rewrite A; rewrite update_o; auto.
-  apply block_contents_inject_incr with f; auto.
-  (* no overlap *)
-  intros until delta2. unfold extend_inject.
-  repeat rewrite LOW. repeat rewrite HIGH. unfold eq_block.
-  case (zeq b1 b); case (zeq b2 b); intros.
-  congruence.
-  inversion H9. subst b1'; subst delta1.
-  case (eq_block b' b2'); intro.
-  subst b2'. generalize (H7 _ _ H10). intro. 
-  right. intros. omega. left. auto.
-  inversion H10. subst b2'; subst delta2.
-  case (eq_block b' b1'); intro.
-  subst b1'. generalize (H7 _ _ H9). intro.
-  right. intros. omega. left. auto.
-  apply mi_no_overlap0; auto.
-Qed.
-
-Lemma alloc_parallel_inject:
-  forall f m1 m2 lo hi m1' m2' b1 b2,
-  mem_inject f m1 m2 ->
-  alloc m1 lo hi = (m1', b1) ->
-  alloc m2 lo hi = (m2', b2) ->
-  Int.min_signed <= lo -> hi <= Int.max_signed ->
-  mem_inject (extend_inject b1 (Some(b2,0)) f) m1' m2' /\
-  inject_incr f (extend_inject b1 (Some(b2,0)) f).
-Proof.
-  intros. 
-  generalize (low_bound_alloc _ _ b2 _ _ _ H1). rewrite zeq_true; intro LOW.
-  generalize (high_bound_alloc _ _ b2 _ _ _ H1). rewrite zeq_true; intro HIGH.
-  eapply alloc_mapped_inject; eauto.
-  eapply alloc_right_inject; eauto.
-  eapply valid_new_block; eauto.
-  compute. intuition congruence.
-  rewrite LOW; auto.
-  rewrite HIGH; auto.
-  rewrite LOW; omega.
-  rewrite HIGH; omega.
-  intros. elim (mi_mappedblocks _ _ _ H _ _ _ H4); intros.
-  injection H1; intros. rewrite H7 in H5. omegaContradiction.
-Qed.