Fusion des modifications faites sur les branches "tailcalls" et "smallstep".

En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC


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

9 files changed, 3426 insertions, 2089 deletions

diff --git a/common/AST.v b/common/AST.v
index 5b8c997..403861d 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -2,11 +2,14 @@
   the abstract syntax trees of many of the intermediate languages. *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Integers.
 Require Import Floats.
 
 Set Implicit Arguments.
 
+(** * Syntactic elements *)
+
 (** Identifiers (names of local variables, of global symbols and functions,
   etc) are represented by the type [positive] of positive integers. *)
 
@@ -14,8 +17,9 @@ Definition ident := positive.
 
 Definition ident_eq := peq.
 
-(** The languages are weakly typed, using only two types: [Tint] for
-  integers and pointers, and [Tfloat] for floating-point numbers. *)
+(** The intermediate languages are weakly typed, using only two types:
+  [Tint] for integers and pointers, and [Tfloat] for floating-point
+  numbers. *)
 
 Inductive typ : Set :=
   | Tint : typ
@@ -24,6 +28,9 @@ Inductive typ : Set :=
 Definition typesize (ty: typ) : Z :=
   match ty with Tint => 4 | Tfloat => 8 end.
 
+Lemma typesize_pos: forall ty, typesize ty > 0.
+Proof. destruct ty; simpl; omega. Qed.
+
 (** Additionally, function definitions and function calls are annotated
   by function signatures indicating the number and types of arguments,
   as well as the type of the returned value if any.  These signatures
@@ -82,6 +89,14 @@ Record program (F V: Set) : Set := mkprogram {
   prog_vars: list (ident * list init_data * V)
 }.
 
+Definition prog_funct_names (F V: Set) (p: program F V) : list ident :=
+  map (@fst ident F) p.(prog_funct).
+
+Definition prog_var_names (F V: Set) (p: program F V) : list ident :=
+  map (fun x: ident * list init_data * V => fst(fst x)) p.(prog_vars).
+
+(** * Generic transformations over programs *)
+
 (** We now define a general iterator over programs that applies a given
   code transformation function to all function descriptions and leaves
   the other parts of the program unchanged. *)
@@ -117,48 +132,63 @@ End TRANSF_PROGRAM.
   code transformation function can fail and therefore returns an
   option type. *)
 
+Open Local Scope error_monad_scope.
+Open Local Scope string_scope.
+
 Section MAP_PARTIAL.
 
 Variable A B C: Set.
-Variable f: B -> option C.
+Variable prefix_errmsg: A -> errmsg.
+Variable f: B -> res C.
 
-Fixpoint map_partial (l: list (A * B)) : option (list (A * C)) :=
+Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
   match l with
-  | nil => Some nil
+  | nil => OK nil
   | (a, b) :: rem =>
       match f b with
-      | None => None
-      | Some c =>
-          match map_partial rem with
-          | None => None
-          | Some res => Some ((a, c) :: res)
-          end
+      | Error msg => Error (prefix_errmsg a ++ msg)%list
+      | OK c =>
+          do rem' <- map_partial rem; 
+          OK ((a, c) :: rem')
       end
   end.
 
 Remark In_map_partial:
   forall l l' a c,
-  map_partial l = Some l' ->
+  map_partial l = OK l' ->
   In (a, c) l' ->
-  exists b, In (a, b) l /\ f b = Some c.
+  exists b, In (a, b) l /\ f b = OK c.
 Proof.
   induction l; simpl.
-  intros. inversion H; subst. elim H0.
-  destruct a as [a1 b1]. intros until c.
+  intros. inv H. elim H0.
+  intros until c. destruct a as [a1 b1].
   caseEq (f b1); try congruence.
-  intros c1 EQ1. caseEq (map_partial l); try congruence.
-  intros res EQ2 EQ3 IN. inversion EQ3; clear EQ3; subst l'.
-  elim IN; intro. inversion H; subst. 
-  exists b1; auto.
+  intro c1; intros. monadInv H0. 
+  elim H1; intro. inv H0. exists b1; auto. 
   exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
 Qed.
 
+Remark map_partial_forall2:
+  forall l l',
+  map_partial l = OK l' ->
+  list_forall2
+    (fun (a_b: A * B) (a_c: A * C) =>
+       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
+    l l'.
+Proof.
+  induction l; simpl.
+  intros. inv H. constructor.
+  intro l'. destruct a as [a b].
+  caseEq (f b). 2: congruence. intro c; intros. monadInv H0.  
+  constructor. simpl. auto. auto. 
+Qed.
+
 End MAP_PARTIAL.
 
 Remark map_partial_total:
-  forall (A B C: Set) (f: B -> C) (l: list (A * B)),
-  map_partial (fun b => Some (f b)) l =
-  Some (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
+  forall (A B C: Set) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
+  map_partial prefix (fun b => OK (f b)) l =
+  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
 Proof.
   induction l; simpl.
   auto.
@@ -166,8 +196,8 @@ Proof.
 Qed.
 
 Remark map_partial_identity:
-  forall (A B: Set) (l: list (A * B)),
-  map_partial (fun b => Some b) l = Some l.
+  forall (A B: Set) (prefix: A -> errmsg) (l: list (A * B)),
+  map_partial prefix (fun b => OK b) l = OK l.
 Proof.
   induction l; simpl.
   auto.
@@ -177,39 +207,39 @@ Qed.
 Section TRANSF_PARTIAL_PROGRAM.
 
 Variable A B V: Set.
-Variable transf_partial: A -> option B.
+Variable transf_partial: A -> res B.
 
-Function transform_partial_program (p: program A V) : option (program B V) :=
-  match map_partial transf_partial p.(prog_funct) with
-  | None => None
-  | Some fl => Some (mkprogram fl p.(prog_main) p.(prog_vars))
-  end.
+Definition prefix_funct_name (id: ident) : errmsg :=
+  MSG "In function " :: CTX id :: MSG ":\n" :: nil.
+
+Definition transform_partial_program (p: program A V) : res (program B V) :=
+  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
+  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
 
 Lemma transform_partial_program_function:
   forall p tp i tf,
-  transform_partial_program p = Some tp ->
+  transform_partial_program p = OK tp ->
   In (i, tf) tp.(prog_funct) ->
-  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = Some tf.
+  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
 Proof.
-  intros. functional inversion H. 
-  apply In_map_partial with fl; auto. 
-  inversion H; subst tp; assumption.
+  intros. monadInv H. simpl in H0.  
+  eapply In_map_partial; eauto.
 Qed.
 
 Lemma transform_partial_program_main:
   forall p tp,
-  transform_partial_program p = Some tp ->
+  transform_partial_program p = OK tp ->
   tp.(prog_main) = p.(prog_main).
 Proof.
-  intros. functional inversion H. reflexivity.
+  intros. monadInv H. reflexivity.
 Qed.
 
 Lemma transform_partial_program_vars:
   forall p tp,
-  transform_partial_program p = Some tp ->
+  transform_partial_program p = OK tp ->
   tp.(prog_vars) = p.(prog_vars).
 Proof.
-  intros. functional inversion H. reflexivity.
+  intros. monadInv H. reflexivity.
 Qed.
 
 End TRANSF_PARTIAL_PROGRAM.
@@ -221,49 +251,104 @@ End TRANSF_PARTIAL_PROGRAM.
 Section TRANSF_PARTIAL_PROGRAM2.
 
 Variable A B V W: Set.
-Variable transf_partial_function: A -> option B.
-Variable transf_partial_variable: V -> option W.
-
-Function transform_partial_program2 (p: program A V) : option (program B W) :=
-  match map_partial transf_partial_function p.(prog_funct) with
-  | None => None
-  | Some fl =>
-      match map_partial transf_partial_variable p.(prog_vars) with
-      | None => None
-      | Some vl => Some (mkprogram fl p.(prog_main) vl)
-      end
-  end.
+Variable transf_partial_function: A -> res B.
+Variable transf_partial_variable: V -> res W.
+
+Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
+  MSG "In global variable " :: CTX (fst id_init) :: MSG ":\n" :: nil.
+
+Definition transform_partial_program2 (p: program A V) : res (program B W) :=
+  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
+  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
+  OK (mkprogram fl p.(prog_main) vl).
 
 Lemma transform_partial_program2_function:
   forall p tp i tf,
-  transform_partial_program2 p = Some tp ->
+  transform_partial_program2 p = OK tp ->
   In (i, tf) tp.(prog_funct) ->
-  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = Some tf.
+  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
 Proof.
-  intros. functional inversion H. 
-  apply In_map_partial with fl. auto. subst tp; assumption.
+  intros. monadInv H.  
+  eapply In_map_partial; eauto. 
 Qed.
 
 Lemma transform_partial_program2_variable:
   forall p tp i tv,
-  transform_partial_program2 p = Some tp ->
+  transform_partial_program2 p = OK tp ->
   In (i, tv) tp.(prog_vars) ->
-  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = Some tv.
+  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
 Proof.
-  intros. functional inversion H. 
-  apply In_map_partial with vl. auto. subst tp; assumption.
+  intros. monadInv H. 
+  eapply In_map_partial; eauto. 
 Qed.
 
 Lemma transform_partial_program2_main:
   forall p tp,
-  transform_partial_program2 p = Some tp ->
+  transform_partial_program2 p = OK tp ->
   tp.(prog_main) = p.(prog_main).
 Proof.
-  intros. functional inversion H. reflexivity.
+  intros. monadInv H. reflexivity.
 Qed.
 
 End TRANSF_PARTIAL_PROGRAM2.
 
+(** The following is a relational presentation of 
+  [transform_program_partial2].  Given relations between function
+  definitions and between variable information, it defines a relation
+  between programs stating that the two programs have the same shape
+  (same global names, etc) and that identically-named function definitions 
+  are variable information are related. *)
+
+Section MATCH_PROGRAM.
+
+Variable A B V W: Set.
+Variable match_fundef: A -> B -> Prop.
+Variable match_varinfo: V -> W -> Prop.
+
+Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
+  match x1, x2 with
+  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
+  end.
+
+Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
+  match x1, x2 with
+  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
+  end.
+
+Definition match_program (p1: program A V) (p2: program B W) : Prop :=
+  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
+  /\ p1.(prog_main) = p2.(prog_main)
+  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
+
+End MATCH_PROGRAM.
+
+Remark transform_partial_program2_match:
+  forall (A B V W: Set)
+         (transf_partial_function: A -> res B)
+         (transf_partial_variable: V -> res W)
+         (p: program A V) (tp: program B W),
+  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
+  match_program 
+    (fun fd tfd => transf_partial_function fd = OK tfd)
+    (fun info tinfo => transf_partial_variable info = OK tinfo)
+    p tp.
+Proof.
+  intros. monadInv H. split.
+  apply list_forall2_imply with
+    (fun (ab: ident * A) (ac: ident * B) =>
+       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
+  eapply map_partial_forall2. eauto. 
+  intros. destruct v1; destruct v2; simpl in *. auto.
+  split. auto.
+  apply list_forall2_imply with
+    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
+       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
+  eapply map_partial_forall2. eauto. 
+  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
+Qed.
+
+(** * External functions *)
+
 (** For most languages, the functions composing the program are either
   internal functions, defined within the language, or external functions
   (a.k.a. system calls) that emit an event when applied.  We define
@@ -296,16 +381,12 @@ End TRANSF_FUNDEF.
 Section TRANSF_PARTIAL_FUNDEF.
 
 Variable A B: Set.
-Variable transf_partial: A -> option B.
+Variable transf_partial: A -> res B.
 
-Definition transf_partial_fundef (fd: fundef A): option (fundef B) :=
+Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
   match fd with
-  | Internal f =>
-      match transf_partial f with
-      | None => None
-      | Some f' => Some (Internal f')
-      end
-  | External ef => Some (External ef)
+  | Internal f => do f' <- transf_partial f; OK (Internal f')
+  | External ef => OK (External ef)
   end.
 
 End TRANSF_PARTIAL_FUNDEF.
diff --git a/common/Errors.v b/common/Errors.v
new file mode 100644
index 0000000..2c1d752
--- /dev/null
+++ b/common/Errors.v
@@ -0,0 +1,167 @@
+(** Error reporting and the error monad. *)
+
+Require Import String.
+Require Import Coqlib.
+
+Close Scope string_scope.
+
+Set Implicit Arguments.
+
+(** * Representation of error messages. *)
+
+(** Compile-time errors produce an error message, represented in Coq
+  as a list of either substrings or positive numbers encoding
+  a source-level identifier (see module AST). *)
+
+Inductive errcode: Set :=
+  | MSG: string -> errcode
+  | CTX: positive -> errcode.
+
+Definition errmsg: Set := list errcode.
+
+Definition msg (s: string) : errmsg := MSG s :: nil.
+
+(** * The error monad *)
+
+(** Compilation functions that can fail have return type [res A].
+  The return value is either [OK res] to indicate success,
+  or [Error msg] to indicate failure. *)
+
+Inductive res (A: Set) : Set :=
+| OK: A -> res A
+| Error: errmsg -> res A.
+
+Implicit Arguments Error [A].
+
+(** To automate the propagation of errors, we use a monadic style
+  with the following [bind] operation. *)
+
+Definition bind (A B: Set) (f: res A) (g: A -> res B) : res B :=
+  match f with
+  | OK x => g x
+  | Error msg => Error msg
+  end.
+
+Definition bind2 (A B C: Set) (f: res (A * B)) (g: A -> B -> res C) : res C :=
+  match f with
+  | OK (x, y) => g x y
+  | Error msg => Error msg
+  end.
+
+(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
+
+Notation "'do' X <- A ; B" := (bind A (fun X => B))
+ (at level 200, X ident, A at level 100, B at level 200)
+ : error_monad_scope.
+
+Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
+ (at level 200, X ident, Y ident, A at level 100, B at level 200)
+ : error_monad_scope.
+
+Remark bind_inversion:
+  forall (A B: Set) (f: res A) (g: A -> res B) (y: B),
+  bind f g = OK y ->
+  exists x, f = OK x /\ g x = OK y.
+Proof.
+  intros until y. destruct f; simpl; intros.
+  exists a; auto.
+  discriminate.
+Qed.
+
+Remark bind2_inversion:
+  forall (A B C: Set) (f: res (A*B)) (g: A -> B -> res C) (z: C),
+  bind2 f g = OK z ->
+  exists x, exists y, f = OK (x, y) /\ g x y = OK z.
+Proof.
+  intros until z. destruct f; simpl.
+  destruct p; simpl; intros. exists a; exists b; auto.
+  intros; discriminate.
+Qed.
+
+Open Local Scope error_monad_scope.
+
+(** This is the familiar monadic map iterator. *)
+
+Fixpoint mmap (A B: Set) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
+  match l with
+  | nil => OK nil
+  | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl')
+  end.
+
+Remark mmap_inversion:
+  forall (A B: Set) (f: A -> res B) (l: list A) (l': list B),
+  mmap f l = OK l' ->
+  list_forall2 (fun x y => f x = OK y) l l'.
+Proof.
+  induction l; simpl; intros.
+  inversion_clear H. constructor.
+  destruct (bind_inversion _ _ H) as [hd' [P Q]].
+  destruct (bind_inversion _ _ Q) as [tl' [R S]].
+  inversion_clear S.
+  constructor. auto. auto. 
+Qed.
+
+(** * Reasoning over monadic computations *)
+
+(** The [monadInv H] tactic below simplifies hypotheses of the form
+<<
+        H: (do x <- a; b) = OK res
+>>
+    By definition of the bind operation, both computations [a] and
+    [b] must succeed for their composition to succeed.  The tactic
+    therefore generates the following hypotheses:
+
+         x: ...
+        H1: a = OK x
+        H2: b x = OK res
+*)
+
+Ltac monadInv1 H :=
+  match type of H with
+  | (OK _ = OK _) =>
+      inversion H; clear H; try subst
+  | (Error _ = OK _) =>
+      discriminate
+  | (bind ?F ?G = OK ?X) =>
+      let x := fresh "x" in (
+      let EQ1 := fresh "EQ" in (
+      let EQ2 := fresh "EQ" in (
+      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
+      clear H;
+      try (monadInv1 EQ2))))
+  | (bind2 ?F ?G = OK ?X) =>
+      let x1 := fresh "x" in (
+      let x2 := fresh "x" in (
+      let EQ1 := fresh "EQ" in (
+      let EQ2 := fresh "EQ" in (
+      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
+      clear H;
+      try (monadInv1 EQ2)))))
+  | (mmap ?F ?L = OK ?M) =>
+      generalize (mmap_inversion F L H); intro
+  end.
+
+Ltac monadInv H :=
+  match type of H with
+  | (OK _ = OK _) => monadInv1 H
+  | (Error _ = OK _) => monadInv1 H
+  | (bind ?F ?G = OK ?X) => monadInv1 H
+  | (bind2 ?F ?G = OK ?X) => monadInv1 H
+  | (?F _ _ _ _ _ _ _ _ = OK _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ _ _ = OK _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ _ = OK _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ = OK _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ = OK _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ = OK _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ = OK _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ = OK _) => 
+      ((progress simpl in H) || unfold F in H); monadInv1 H
+  end.
+
diff --git a/common/Events.v b/common/Events.v
index a0559fd..e1a4729 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1,4 +1,4 @@
-(** Representation of (traces of) observable events. *)
+(** Representation of observable events and execution traces. *)
 
 Require Import Coqlib.
 Require Import AST.
@@ -6,23 +6,77 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 
+(** The observable behaviour of programs is stated in terms of
+  input/output events, which can also be thought of as system calls 
+  to the operating system.  An event is generated each time an
+  external function (see module AST) is invoked.  The event records
+  the name of the external function, the arguments to the function
+  invocation provided by the program, and the return value provided by
+  the outside world (e.g. the operating system).  Arguments and values
+  are either integers or floating-point numbers.  We currently do not
+  allow pointers to be exchanged between the program and the outside
+  world. *)
+
 Inductive eventval: Set :=
   | EVint: int -> eventval
   | EVfloat: float -> eventval.
 
-Parameter trace: Set.
-Parameter E0: trace.
-Parameter Eextcall: ident -> list eventval -> eventval -> trace.
-Parameter Eapp: trace -> trace -> trace.
+Record event : Set := mkevent {
+  ev_name: ident;
+  ev_args: list eventval;
+  ev_res: eventval
+}.
+
+(** The dynamic semantics for programs collect traces of events.
+  Traces are of two kinds: finite (type [trace]) 
+  or infinite (type [traceinf]). *)
+
+Definition trace := list event.
+
+Definition E0 : trace := nil.
+
+Definition Eextcall
+             (name: ident) (args: list eventval) (res: eventval) : trace :=
+  mkevent name args res :: nil.
+
+Definition Eapp (t1 t2: trace) : trace := t1 ++ t2.
+
+CoInductive traceinf : Set :=
+  | Econsinf: event -> traceinf -> traceinf.
+
+Fixpoint Eappinf (t: trace) (T: traceinf) {struct t} : traceinf :=
+  match t with
+  | nil => T
+  | ev :: t' => Econsinf ev (Eappinf t' T)
+  end.
+
+(** Concatenation of traces is written [**] in the finite case
+  or [***] in the infinite case. *)
 
 Infix "**" := Eapp (at level 60, right associativity).
+Infix "***" := Eappinf (at level 60, right associativity).
 
-Axiom E0_left: forall t, E0 ** t = t.
-Axiom E0_right: forall t, t ** E0 = t.
-Axiom Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3).
+Lemma E0_left: forall t, E0 ** t = t.
+Proof. auto. Qed.
+
+Lemma E0_right: forall t, t ** E0 = t.
+Proof. intros. unfold E0, Eapp. rewrite <- app_nil_end. auto. Qed.
+
+Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3).
+Proof. intros. unfold Eapp, trace. apply app_ass. Qed.
+
+Lemma Eappinf_assoc: forall t1 t2 T, (t1 ** t2) *** T = t1 *** (t2 *** T).
+Proof.
+  induction t1; intros; simpl. auto. decEq; auto.
+Qed.
 
 Hint Rewrite E0_left E0_right Eapp_assoc: trace_rewrite.
 
+Opaque trace E0 Eextcall Eapp.
+
+(** The following [traceEq] tactic proves equalities between traces
+  or infinite traces. *)
+
 Ltac substTraceHyp :=
   match goal with
   | [ H: (@eq trace ?x ?y) |- _ ] =>
@@ -40,6 +94,11 @@ Ltac decomposeTraceEq :=
 Ltac traceEq := 
   repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.
 
+(** The predicate [event_match ef vargs t vres] expresses that
+  the event [t] is generated when invoking external function [ef]
+  with arguments [vargs], and obtaining [vres] as a return value
+  from the operating system. *)
+
 Inductive eventval_match: eventval -> typ -> val -> Prop :=
   | ev_match_int:
       forall i, eventval_match (EVint i) Tint (Vint i)
@@ -63,6 +122,10 @@ Inductive event_match:
     eventval_match eres (proj_sig_res ef.(ef_sig)) vres ->
     event_match ef vargs (Eextcall ef.(ef_id) eargs eres) vres.
 
+(** The following section shows that [event_match] is stable under
+  relocation of pointer values, as performed by memory injections
+  (see module [Mem]). *)
+
 Require Import Mem.
 
 Section EVENT_MATCH_INJECT.
@@ -101,3 +164,41 @@ Proof.
 Qed.
 
 End EVENT_MATCH_INJECT.
+
+(** The following section shows that [event_match] is stable under
+  replacement of [Vundef] values by more defined values. *)
+
+Section EVENT_MATCH_LESSDEF.
+
+Remark eventval_match_lessdef:
+  forall ev ty v1,  eventval_match ev ty v1 ->
+  forall v2, Val.lessdef v1 v2 ->
+  eventval_match ev ty v2.
+Proof.
+  induction 1; intros; inv H; constructor.
+Qed.
+
+Remark eventval_list_match_moredef:
+  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
+  forall vl2, Val.lessdef_list vl1 vl2 ->
+  eventval_list_match evl tyl vl2.
+Proof.
+  induction 1; intros.
+  inversion H; constructor. 
+  inversion H1; constructor. 
+  eapply eventval_match_lessdef; eauto.
+  eauto.
+Qed.
+
+Lemma event_match_lessdef:
+  forall ef args1 t res1 args2,
+  event_match ef args1 t res1 ->
+  Val.lessdef_list args1 args2 ->
+  exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2.
+Proof.
+  intros. inversion H; subst. exists res1; split. 
+  constructor. eapply eventval_list_match_moredef; eauto. auto.
+  auto.
+Qed.
+
+End EVENT_MATCH_LESSDEF.
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index ccb7b03..623200f 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -19,6 +19,7 @@
   system. *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
@@ -60,6 +61,34 @@ Module Type GENV.
   Hypothesis find_funct_find_funct_ptr:
     forall (F: Set) (ge: t F) (b: block),
     find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b.    
+
+  Hypothesis find_symbol_exists:
+    forall (F V: Set) (p: program F V)
+           (id: ident) (init: list init_data) (v: V),
+    In (id, init, v) (prog_vars p) ->
+    exists b, find_symbol (globalenv p) id = Some b.
+  Hypothesis find_funct_ptr_exists:
+    forall (F V: Set) (p: program F V) (id: ident) (f: F),
+    list_norepet (prog_funct_names p) ->
+    list_disjoint (prog_funct_names p) (prog_var_names p) ->
+    In (id, f) (prog_funct p) ->
+    exists b, find_symbol (globalenv p) id = Some b
+           /\ find_funct_ptr (globalenv p) b = Some f.
+
+  Hypothesis find_funct_ptr_inversion:
+    forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F),
+    find_funct_ptr (globalenv p) b = Some f ->
+    exists id, In (id, f) (prog_funct p).
+  Hypothesis find_funct_inversion:
+    forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F),
+    find_funct (globalenv p) v = Some f ->
+    exists id, In (id, f) (prog_funct p).
+  Hypothesis find_funct_ptr_symbol_inversion:
+    forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F),
+    find_symbol (globalenv p) id = Some b ->
+    find_funct_ptr (globalenv p) b = Some f ->
+    In (id, f) p.(prog_funct).
+
   Hypothesis find_funct_ptr_prop:
     forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F),
     (forall id f, In (id, f) (prog_funct p) -> P f) ->
@@ -70,24 +99,19 @@ Module Type GENV.
     (forall id f, In (id, f) (prog_funct p) -> P f) ->
     find_funct (globalenv p) v = Some f ->
     P f.
-  Hypothesis find_funct_ptr_symbol_inversion:
-    forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F),
-    find_symbol (globalenv p) id = Some b ->
-    find_funct_ptr (globalenv p) b = Some f ->
-    In (id, f) p.(prog_funct).
 
   Hypothesis initmem_nullptr:
     forall (F V: Set) (p: program F V),
     let m := init_mem p in
     valid_block m nullptr /\
     m.(blocks) nullptr = empty_block 0 0.
-  Hypothesis initmem_block_init:
-    forall (F V: Set) (p: program F V) (b: block),
-    exists id, (init_mem p).(blocks) b = block_init_data id.
-  Hypothesis find_funct_ptr_inv:
+  Hypothesis initmem_inject_neutral:
+    forall (F V: Set) (p: program F V),
+    mem_inject_neutral (init_mem p).
+  Hypothesis find_funct_ptr_negative:
     forall (F V: Set) (p: program F V) (b: block) (f: F),
     find_funct_ptr (globalenv p) b = Some f -> b < 0.
-  Hypothesis find_symbol_inv:
+  Hypothesis find_symbol_not_fresh:
     forall (F V: Set) (p: program F V) (id: ident) (b: block),
     find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p).
 
@@ -95,74 +119,162 @@ Module Type GENV.
   and operations over global environments. *)
 
   Hypothesis find_funct_ptr_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V) (b: block) (f: A),
+    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (b: block) (f: A),
     find_funct_ptr (globalenv p) b = Some f ->
     find_funct_ptr (globalenv (transform_program transf p)) b = Some (transf f).
   Hypothesis find_funct_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V) (v: val) (f: A),
+    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (v: val) (f: A),
     find_funct (globalenv p) v = Some f ->
     find_funct (globalenv (transform_program transf p)) v = Some (transf f).
   Hypothesis find_symbol_transf:
-    forall (A B V: Set) (transf: A -> B) (p: program A V) (s: ident),
+    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (s: ident),
     find_symbol (globalenv (transform_program transf p)) s =
     find_symbol (globalenv p) s.
   Hypothesis init_mem_transf:
     forall (A B V: Set) (transf: A -> B) (p: program A V),
     init_mem (transform_program transf p) = init_mem p.
+  Hypothesis find_funct_ptr_rev_transf:
+    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (b : block) (tf : B),
+    find_funct_ptr (globalenv (transform_program transf p)) b = Some tf ->
+    exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf.
+  Hypothesis find_funct_rev_transf:
+    forall (A B V: Set) (transf: A -> B) (p: program A V),
+    forall (v : val) (tf : B),
+    find_funct (globalenv (transform_program transf p)) v = Some tf ->
+    exists f : A, find_funct (globalenv p) v = Some f /\ transf f = tf.
 
 (** Commutation properties between partial program transformations
   and operations over global environments. *)
 
   Hypothesis find_funct_ptr_transf_partial:
-    forall (A B V: Set) (transf: A -> option B)
-           (p: program A V) (p': program B V),
-    transform_partial_program transf p = Some p' ->
+    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    transform_partial_program transf p = OK p' ->
     forall (b: block) (f: A),
     find_funct_ptr (globalenv p) b = Some f ->
-    find_funct_ptr (globalenv p') b = transf f /\ transf f <> None.
+    exists f',
+    find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'.
   Hypothesis find_funct_transf_partial:
-    forall (A B V: Set) (transf: A -> option B)
-           (p: program A V) (p': program B V),
-    transform_partial_program transf p = Some p' ->
+    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    transform_partial_program transf p = OK p' ->
     forall (v: val) (f: A),
     find_funct (globalenv p) v = Some f ->
-    find_funct (globalenv p') v = transf f /\ transf f <> None.
+    exists f',
+    find_funct (globalenv p') v = Some f' /\ transf f = OK f'.
   Hypothesis find_symbol_transf_partial:
-    forall (A B V: Set) (transf: A -> option B)
-           (p: program A V) (p': program B V),
-    transform_partial_program transf p = Some p' ->
+    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    transform_partial_program transf p = OK p' ->
     forall (s: ident),
     find_symbol (globalenv p') s = find_symbol (globalenv p) s.
   Hypothesis init_mem_transf_partial:
-    forall (A B V: Set) (transf: A -> option B)
-           (p: program A V) (p': program B V),
-    transform_partial_program transf p = Some p' ->
+    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    transform_partial_program transf p = OK p' ->
     init_mem p' = init_mem p.
+  Hypothesis find_funct_ptr_rev_transf_partial:
+    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    transform_partial_program transf p = OK p' ->
+    forall (b : block) (tf : B),
+    find_funct_ptr (globalenv p') b = Some tf ->
+    exists f : A,
+      find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf.
+  Hypothesis find_funct_rev_transf_partial:
+    forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V),
+    transform_partial_program transf p = OK p' ->
+    forall (v : val) (tf : B),
+    find_funct (globalenv p') v = Some tf ->
+    exists f : A,
+      find_funct (globalenv p) v = Some f /\ transf f = OK tf.
 
   Hypothesis find_funct_ptr_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W)
+    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
-    transform_partial_program2 transf_fun transf_var p = Some p' ->
+    transform_partial_program2 transf_fun transf_var p = OK p' ->
     forall (b: block) (f: A),
     find_funct_ptr (globalenv p) b = Some f ->
-    find_funct_ptr (globalenv p') b = transf_fun f /\ transf_fun f <> None.
+    exists f',
+    find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
   Hypothesis find_funct_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W)
+    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
-    transform_partial_program2 transf_fun transf_var p = Some p' ->
+    transform_partial_program2 transf_fun transf_var p = OK p' ->
     forall (v: val) (f: A),
     find_funct (globalenv p) v = Some f ->
-    find_funct (globalenv p') v = transf_fun f /\ transf_fun f <> None.
+    exists f',
+    find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
   Hypothesis find_symbol_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W)
+    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
-    transform_partial_program2 transf_fun transf_var p = Some p' ->
+    transform_partial_program2 transf_fun transf_var p = OK p' ->
     forall (s: ident),
     find_symbol (globalenv p') s = find_symbol (globalenv p) s.
   Hypothesis init_mem_transf_partial2:
-    forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W)
+    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
+           (p: program A V) (p': program B W),
+    transform_partial_program2 transf_fun transf_var p = OK p' ->
+    init_mem p' = init_mem p.
+  Hypothesis find_funct_ptr_rev_transf_partial2:
+    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
+           (p: program A V) (p': program B W),
+    transform_partial_program2 transf_fun transf_var p = OK p' ->
+    forall (b : block) (tf : B),
+    find_funct_ptr (globalenv p') b = Some tf ->
+    exists f : A,
+      find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.
+  Hypothesis find_funct_rev_transf_partial2:
+    forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W)
            (p: program A V) (p': program B W),
-    transform_partial_program2 transf_fun transf_var p = Some p' ->
+    transform_partial_program2 transf_fun transf_var p = OK p' ->
+    forall (v : val) (tf : B),
+    find_funct (globalenv p') v = Some tf ->
+    exists f : A,
+      find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.
+
+(** Commutation properties between matching between programs
+  and operations over global environments. *)
+
+  Hypothesis find_funct_ptr_match:
+    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
+    match_program match_fun match_var p p' ->
+    forall (b : block) (f : A),
+    find_funct_ptr (globalenv p) b = Some f ->
+    exists tf : B,
+    find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf.
+  Hypothesis find_funct_ptr_rev_match:
+    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
+    match_program match_fun match_var p p' ->
+    forall (b : block) (tf : B),
+    find_funct_ptr (globalenv p') b = Some tf ->
+    exists f : A,
+    find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf.
+  Hypothesis find_funct_match:
+    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
+    match_program match_fun match_var p p' ->
+    forall (v : val) (f : A),
+    find_funct (globalenv p) v = Some f ->
+    exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf.
+  Hypothesis find_funct_rev_match:
+    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
+    match_program match_fun match_var p p' ->
+    forall (v : val) (tf : B),
+    find_funct (globalenv p') v = Some tf ->
+    exists f : A, find_funct (globalenv p) v = Some f /\ match_fun f tf.
+  Hypothesis find_symbol_match:
+    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
+    match_program match_fun match_var p p' ->
+    forall (s : ident),
+    find_symbol (globalenv p') s = find_symbol (globalenv p) s.
+  Hypothesis init_mem_match:
+    forall (A B V W: Set) (match_fun: A -> B -> Prop)
+           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),
+    match_program match_fun match_var p p' ->
     init_mem p' = init_mem p.
 
 End GENV.
@@ -280,10 +392,10 @@ Lemma initmem_nullptr:
   forall (p: program F V),
   let m := init_mem p in
   valid_block m nullptr /\
-  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0).
+  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
 Proof.
   pose (P := fun m => valid_block m nullptr /\
-        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0)).
+        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
   assert (forall init, P (snd init) -> forall vars, P (snd (add_globals init vars))).
   induction vars; simpl; intros.
   auto.
@@ -297,25 +409,25 @@ Proof.
   red; simpl. split. compute. auto. reflexivity.
 Qed. 
 
-Lemma initmem_block_init:
-  forall (p: program F V) (b: block),
-  exists id, (init_mem p).(blocks) b = block_init_data id.
+Lemma initmem_inject_neutral:
+  forall (p: program F V),
+  mem_inject_neutral (init_mem p).
 Proof.
-  assert (forall g0 vars g1 m b,
+  assert (forall g0 vars g1 m,
       add_globals (g0, Mem.empty) vars = (g1, m) ->
-      exists id, m.(blocks) b = block_init_data id).
-  induction vars; simpl.
-  intros. inversion H. unfold Mem.empty; simpl. 
-  exists (@nil init_data). symmetry. apply Mem.block_init_data_empty.
+      mem_inject_neutral m).
+  Opaque alloc_init_data.
+  induction vars; simpl. 
+  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
+  simpl in H1. rewrite Mem.getN_init in H1. 
+  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
   destruct a as [[id1 init1] info1]. 
-  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. 
-  intros g m b EQ1. injection EQ1; intros EQ2 EQ3; clear EQ1.
-  rewrite <- EQ2; simpl. unfold update.
-  case (zeq b (nextblock m1)); intro.
-  exists init1; auto.
-  eauto.
-  intros. caseEq (globalenv_initmem p). 
-  intros g m EQ. unfold init_mem; rewrite EQ; simpl. 
+  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
+  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
+  intros. inv H. 
+  eapply Mem.alloc_init_data_neutral; eauto.
+  intros. caseEq (globalenv_initmem p). intros g m EQ.
+  unfold init_mem; rewrite EQ; simpl. 
   unfold globalenv_initmem in EQ. eauto.
 Qed.      
 
@@ -325,7 +437,7 @@ Proof.
   induction fns; simpl; intros. omega. unfold Zpred. omega.
 Qed.
 
-Theorem find_funct_ptr_inv:
+Theorem find_funct_ptr_negative:
   forall (p: program F V) (b: block) (f: F),
   find_funct_ptr (globalenv p) b = Some f -> b < 0.
 Proof.
@@ -340,7 +452,7 @@ Proof.
   intros. eauto.
 Qed.
 
-Theorem find_symbol_inv:
+Theorem find_symbol_not_fresh:
   forall (p: program F V) (id: ident) (b: block),
   find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p).
 Proof.
@@ -358,6 +470,7 @@ Proof.
   induction vars; simpl; intros until b.
   intros. inversion H0. subst g m. simpl. 
   generalize (H fns s b H1). omega.
+  Transparent alloc_init_data.
   destruct a as [[id1 init1] info1]. 
   caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
   intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
@@ -373,20 +486,125 @@ Qed.
 End GENV.
 
 (* Invariants on functions *)
+
+Lemma find_symbol_exists:
+  forall (F V: Set) (p: program F V)
+         (id: ident) (init: list init_data) (v: V),
+  In (id, init, v) (prog_vars p) ->
+  exists b, find_symbol (globalenv p) id = Some b.
+Proof.
+  intros until v.
+  assert (forall initm vl, In (id, init, v) vl ->
+           exists b, PTree.get id (@symbols F (fst (add_globals initm vl))) = Some b).
+  induction vl; simpl; intros.
+  elim H.
+  destruct a as [[id0 init0] v0]. 
+  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl. 
+  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
+  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto. 
+  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
+Qed.
+
+Remark find_symbol_above_nextfunction:
+  forall (F: Set) (id: ident) (b: block) (fns: list (ident * F)),
+  let g := add_functs (empty F) fns in
+  PTree.get id g.(symbols) = Some b ->
+  b > g.(nextfunction).
+Proof.
+  induction fns; simpl.
+  rewrite PTree.gempty. congruence.
+  rewrite PTree.gsspec. case (peq id (fst a)); intro.
+  intro EQ. inversion EQ. unfold Zpred. omega.
+  intros. generalize (IHfns H). unfold Zpred; omega.
+Qed.
+
+Remark find_symbol_add_globals:
+  forall (F V: Set) (id: ident) (ge_m: t F * mem) (vars: list (ident * list init_data * V)),
+  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) ->
+  find_symbol (fst (add_globals ge_m vars)) id =
+  find_symbol (fst ge_m) id.
+Proof.
+  unfold find_symbol; induction vars; simpl; intros.
+  auto.
+  destruct a as [[id0 init0] var0]. simpl in *.
+  caseEq (add_globals ge_m vars); intros ge' m' EQ.
+  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars. 
+  apply IHvars. tauto. intuition congruence.
+Qed.
+
+Lemma find_funct_ptr_exists:
+  forall (F V: Set) (p: program F V) (id: ident) (f: F),
+  list_norepet (prog_funct_names p) ->
+  list_disjoint (prog_funct_names p) (prog_var_names p) ->
+  In (id, f) (prog_funct p) ->
+  exists b, find_symbol (globalenv p) id = Some b
+         /\ find_funct_ptr (globalenv p) b = Some f.
+Proof.
+  intros until f.
+  assert (forall (fns: list (ident * F)),
+           list_norepet (map (@fst ident F) fns) ->
+           In (id, f) fns ->
+           exists b, find_symbol (add_functs (empty F) fns) id = Some b
+                   /\ find_funct_ptr (add_functs (empty F) fns) b = Some f).
+  unfold find_symbol, find_funct_ptr. induction fns; intros.
+  elim H0.
+  destruct a as [id0 f0]; simpl in *. inv H. 
+  unfold add_funct; simpl.
+  rewrite PTree.gsspec. destruct (peq id id0). 
+  subst id0. econstructor; split. eauto.
+  replace f0 with f. apply ZMap.gss. 
+  elim H0; intro. congruence. elim H3. 
+  change id with (@fst ident F (id, f)). apply List.in_map. auto.
+  exploit IHfns; eauto. elim H0; intro. congruence. auto.
+  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
+  generalize (find_symbol_above_nextfunction _ _ X).
+  unfold block; unfold ZIndexed.t; intro; omega.
+
+  intros. exploit H; eauto. assumption. intros [b [X Y]].
+  exists b; split.
+  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. 
+  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. 
+  unfold prog_funct_names. change id with (fst (id, f)). 
+  apply List.in_map; auto.
+  unfold find_funct_ptr. rewrite functions_globalenv. 
+  assumption. 
+Qed.
+
+Lemma find_funct_ptr_inversion:
+  forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F),
+  find_funct_ptr (globalenv p) b = Some f ->
+  exists id, In (id, f) (prog_funct p).
+Proof.
+  intros until f.
+  assert (forall fns: list (ident * F),
+    find_funct_ptr (add_functs (empty F) fns) b = Some f ->
+    exists id, In (id, f) fns).
+  unfold find_funct_ptr. induction fns; simpl.
+  rewrite ZMap.gi. congruence.
+  destruct a as [id0 f0]; simpl. 
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs (empty F) fns))).
+  intro. inv H. exists id0; auto.
+  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
+  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
+Qed.
+
 Lemma find_funct_ptr_prop:
   forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F),
   (forall id f, In (id, f) (prog_funct p) -> P f) ->
   find_funct_ptr (globalenv p) b = Some f ->
   P f.
 Proof.
-  intros until f.
-  unfold find_funct_ptr. rewrite functions_globalenv.
-  generalize (prog_funct p). induction l; simpl.
-  rewrite ZMap.gi. intros; discriminate.
-  rewrite ZMap.gsspec.
-  case (ZIndexed.eq b (nextfunction (add_functs (empty F) l))); intros.
-  apply H with (fst a). left. destruct a. simpl in *. congruence.
-  apply IHl. intros. apply H with id. right. auto. auto.
+  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
+Qed.
+
+Lemma find_funct_inversion:
+  forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F),
+  find_funct (globalenv p) v = Some f ->
+  exists id, In (id, f) (prog_funct p).
+Proof.
+  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
+  rewrite find_funct_find_funct_ptr in H. 
+  eapply find_funct_ptr_inversion; eauto.
 Qed.
 
 Lemma find_funct_prop:
@@ -395,10 +613,7 @@ Lemma find_funct_prop:
   find_funct (globalenv p) v = Some f ->
   P f.
 Proof.
-  intros until f. unfold find_funct. 
-  destruct v; try (intros; discriminate).
-  case (Int.eq i Int.zero); [idtac | intros; discriminate].
-  intros. eapply find_funct_ptr_prop; eauto.
+  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
 Qed.
 
 Lemma find_funct_ptr_symbol_inversion:
@@ -411,15 +626,6 @@ Proof.
   assert (forall fns,
            let g := add_functs (empty F) fns in
            PTree.get id g.(symbols) = Some b ->
-           b > g.(nextfunction)).
-    induction fns; simpl.
-    rewrite PTree.gempty. congruence.
-    rewrite PTree.gsspec. case (peq id (fst a)); intro.
-    intro EQ. inversion EQ. unfold Zpred. omega.
-    intros. generalize (IHfns H). unfold Zpred; omega.
-  assert (forall fns,
-           let g := add_functs (empty F) fns in
-           PTree.get id g.(symbols) = Some b ->
            ZMap.get b g.(functions) = Some f ->
            In (id, f) fns).
     induction fns; simpl.
@@ -430,216 +636,336 @@ Proof.
     intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true. 
     intro EQ2. left. destruct a. simpl in *. congruence. 
     intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
-    generalize (H _ H0). fold g. unfold block. omega.
+    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
   assert (forall g0 m0, b < 0 ->
           forall vars g m,
           @add_globals F V (g0, m0) vars = (g, m) ->
           PTree.get id g.(symbols) = Some b ->
           PTree.get id g0.(symbols) = Some b).
     induction vars; simpl.
-    intros. inversion H2. auto.
+    intros. inv H1. auto.
     destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). 
     intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
     unfold add_symbol; intros A B. rewrite <- B. simpl. 
     rewrite PTree.gsspec. case (peq id id1); intros.
-    assert (b > 0). injection H2; intros. rewrite <- H3. apply nextblock_pos. 
+    assert (b > 0). inv H1. apply nextblock_pos. 
     omegaContradiction.
     eauto. 
   intros. 
-  generalize (find_funct_ptr_inv _ _ H3). intro.
+  generalize (find_funct_ptr_negative _ _ H2). intro.
   pose (g := add_functs (empty F) (prog_funct p)). 
-  apply H0.  
-  apply H1 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
+  apply H.  
+  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
   auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
   reflexivity. assumption. rewrite <- functions_globalenv. assumption.
 Qed.
 
 (* Global environments and program transformations. *)
 
-Section TRANSF_PROGRAM_PARTIAL2.
+Section MATCH_PROGRAM.
 
 Variable A B V W: Set.
-Variable transf_fun: A -> option B.
-Variable transf_var: V -> option W.
+Variable match_fun: A -> B -> Prop.
+Variable match_var: V -> W -> Prop.
 Variable p: program A V.
 Variable p': program B W.
-Hypothesis transf_OK:
-  transform_partial_program2 transf_fun transf_var p = Some p'.
+Hypothesis match_prog:
+  match_program match_fun match_var p p'.
 
-Lemma add_functs_transf:
+Lemma add_functs_match:
   forall (fns: list (ident * A)) (tfns: list (ident * B)),
-  map_partial transf_fun fns = Some tfns ->
+  list_forall2 (match_funct_entry match_fun) fns tfns ->
   let r := add_functs (empty A) fns in
   let tr := add_functs (empty B) tfns in
   nextfunction tr = nextfunction r /\
   symbols tr = symbols r /\
   forall (b: block) (f: A),
   ZMap.get b (functions r) = Some f ->
-  ZMap.get b (functions tr) = transf_fun f /\ transf_fun f <> None.
+  exists tf, ZMap.get b (functions tr) = Some tf /\ match_fun f tf.
 Proof.
-  induction fns; simpl.
+  induction 1; simpl.
 
-  intros; injection H; intro; subst tfns.
-  simpl. split. reflexivity. split. reflexivity.
+  split. reflexivity. split. reflexivity.
   intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
 
-  intro tfns. destruct a. caseEq (transf_fun a). intros a' TA. 
-  caseEq (map_partial transf_fun fns). intros l TPP EQ.
-  injection EQ; intro; subst tfns.
-  clear EQ. simpl. 
-  generalize (IHfns l TPP).
-  intros [HR1 [HR2 HR3]].
-  rewrite HR1. rewrite HR2.
-  split. reflexivity.
-  split. reflexivity.
+  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. 
+  simpl. red in H. destruct H. 
+  destruct IHlist_forall2 as [X [Y Z]].
+  rewrite X. rewrite Y.  
+  split. auto.
+  split. congruence.
   intros b f.
-  case (zeq b (nextfunction (add_functs (empty A) fns))); intro.
-  subst b. repeat (rewrite ZMap.gss). 
-  intro EQ; injection EQ; intro; subst f; clear EQ.
-  rewrite TA. split. auto. discriminate.
-  repeat (rewrite ZMap.gso; auto). 
+  repeat (rewrite ZMap.gsspec). 
+  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
+  intro EQ; inv EQ. exists fn2; auto.
+  auto.
+Qed.
 
-  intros; discriminate.
-  intros; discriminate.
+Lemma add_functs_rev_match:
+  forall (fns: list (ident * A)) (tfns: list (ident * B)),
+  list_forall2 (match_funct_entry match_fun) fns tfns ->
+  let r := add_functs (empty A) fns in
+  let tr := add_functs (empty B) tfns in
+  nextfunction tr = nextfunction r /\
+  symbols tr = symbols r /\
+  forall (b: block) (tf: B),
+  ZMap.get b (functions tr) = Some tf ->
+  exists f, ZMap.get b (functions r) = Some f /\ match_fun f tf.
+Proof.
+  induction 1; simpl.
+
+  split. reflexivity. split. reflexivity.
+  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
+
+  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. 
+  simpl. red in H. destruct H. 
+  destruct IHlist_forall2 as [X [Y Z]].
+  rewrite X. rewrite Y.  
+  split. auto.
+  split. congruence.
+  intros b f.
+  repeat (rewrite ZMap.gsspec). 
+  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
+  intro EQ; inv EQ. exists fn1; auto.
+  auto.
 Qed.
 
-Lemma mem_add_globals_transf:
+Lemma mem_add_globals_match:
   forall (g1: genv A) (g2: genv B) (m: mem) 
          (vars: list (ident * list init_data * V))
          (tvars: list (ident * list init_data * W)),
-  map_partial transf_var vars = Some tvars ->
+  list_forall2 (match_var_entry match_var) vars tvars ->
   snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
 Proof.
-  induction vars; simpl.
-  intros. inversion H. reflexivity.
-  intro. destruct a as [[id1 init1] info1]. 
-  caseEq (transf_var info1); try congruence.
-  intros tinfo1 EQ1.
-  caseEq (map_partial transf_var vars); try congruence.
-  intros tvars' EQ2 EQ3. 
-  inversion EQ3. simpl. 
-  generalize (IHvars _ EQ2). 
-  destruct (add_globals (g1, m) vars).
-  destruct (add_globals (g2, m) tvars').
+  induction 1; simpl.
+  auto.
+  destruct a1 as [[id1 init1] info1].
+  destruct b1 as [[id2 init2] info2].
+  red in H. destruct H as [X [Y Z]]. subst id2 init2. 
+  generalize IHlist_forall2. 
+  destruct (add_globals (g1, m) al).
+  destruct (add_globals (g2, m) bl).
   simpl. intro. subst m1. auto.
 Qed.
 
-Lemma symbols_add_globals_transf:
+Lemma symbols_add_globals_match:
   forall (g1: genv A) (g2: genv B) (m: mem),
   symbols g1 = symbols g2 ->
   forall (vars: list (ident * list init_data * V))
          (tvars: list (ident * list init_data * W)),
-  map_partial transf_var vars = Some tvars ->
+  list_forall2 (match_var_entry match_var) vars tvars ->
   symbols (fst (add_globals (g1, m) vars)) =
   symbols (fst (add_globals (g2, m) tvars)).
 Proof.
-  induction vars; simpl.
-  intros. inversion H0. assumption.
-  intro. destruct a as [[id1 init1] info1]. 
-  caseEq (transf_var info1); try congruence. intros tinfo1 EQ1.
-  caseEq (map_partial transf_var vars); try congruence.
-  intros tvars' EQ2 EQ3. inversion EQ3; simpl. 
-  generalize (IHvars _ EQ2). 
-  generalize (mem_add_globals_transf g1 g2 m vars EQ2).
-  destruct (add_globals (g1, m) vars).
-  destruct (add_globals (g2, m) tvars').
+  induction 2; simpl.
+  auto.
+  destruct a1 as [[id1 init1] info1].
+  destruct b1 as [[id2 init2] info2].
+  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2. 
+  generalize IHlist_forall2.
+  generalize (mem_add_globals_match g1 g2 m H1).
+  destruct (add_globals (g1, m) al).
+  destruct (add_globals (g2, m) bl).
   simpl. intros. congruence.
 Qed.
 
-(*
-Lemma prog_funct_transf_OK:
-  transf_partial_program transf p.(prog_funct) = Some p'.(prog_funct).
+Theorem find_funct_ptr_match:
+  forall (b: block) (f: A),
+  find_funct_ptr (globalenv p) b = Some f ->
+  exists tf, find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf.
 Proof.
-  generalize transf_OK; unfold transform_partial_program.
-  case (transf_partial_program transf (prog_funct p)); simpl; intros.
-  injection transf_OK0; intros; subst p'. reflexivity.
-  discriminate.
+  intros until f. destruct match_prog as [X [Y Z]]. 
+  destruct (add_functs_match X) as [P [Q R]]. 
+  unfold find_funct_ptr. repeat rewrite functions_globalenv.
+  auto.
 Qed.
-*)
 
-Theorem find_funct_ptr_transf_partial2:
-  forall (b: block) (f: A),
-  find_funct_ptr (globalenv p) b = Some f ->
-  find_funct_ptr (globalenv p') b = transf_fun f /\ transf_fun f <> None.
+Theorem find_funct_ptr_rev_match:
+  forall (b: block) (tf: B),
+  find_funct_ptr (globalenv p') b = Some tf ->
+  exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf.
 Proof.
-  intros until f. functional inversion transf_OK. 
-  destruct (add_functs_transf _ H0) as [P [Q R]]. 
-  unfold find_funct_ptr. repeat rewrite functions_globalenv. simpl. 
+  intros until tf. destruct match_prog as [X [Y Z]]. 
+  destruct (add_functs_rev_match X) as [P [Q R]]. 
+  unfold find_funct_ptr. repeat rewrite functions_globalenv.
   auto.
 Qed.
 
-Theorem find_funct_transf_partial2:
+Theorem find_funct_match:
   forall (v: val) (f: A),
   find_funct (globalenv p) v = Some f ->
-  find_funct (globalenv p') v = transf_fun f /\ transf_fun f <> None.
+  exists tf, find_funct (globalenv p') v = Some tf /\ match_fun f tf.
 Proof.
   intros until f. unfold find_funct. 
   case v; try (intros; discriminate).
   intros b ofs.
   case (Int.eq ofs Int.zero); try (intros; discriminate).
-  apply find_funct_ptr_transf_partial2. 
+  apply find_funct_ptr_match.
 Qed.
 
-Lemma symbols_init_transf2:
+Theorem find_funct_rev_match:
+  forall (v: val) (tf: B),
+  find_funct (globalenv p') v = Some tf ->
+  exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf.
+Proof.
+  intros until tf. unfold find_funct. 
+  case v; try (intros; discriminate).
+  intros b ofs.
+  case (Int.eq ofs Int.zero); try (intros; discriminate).
+  apply find_funct_ptr_rev_match.
+Qed.
+
+Lemma symbols_init_match:
   symbols (globalenv p') = symbols (globalenv p).
 Proof.
   unfold globalenv. unfold globalenv_initmem.
-  functional inversion transf_OK.
-  destruct (add_functs_transf _ H0) as [P [Q R]]. 
-  simpl. symmetry. apply symbols_add_globals_transf. auto. auto.
+  destruct match_prog as [X [Y Z]].
+  destruct (add_functs_match X) as [P [Q R]]. 
+  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
 Qed.
 
-Theorem find_symbol_transf_partial2:
+Theorem find_symbol_match:
   forall (s: ident),
   find_symbol (globalenv p') s = find_symbol (globalenv p) s.
 Proof.
   intros. unfold find_symbol. 
-  rewrite symbols_init_transf2. auto.
+  rewrite symbols_init_match. auto.
+Qed.
+
+Theorem init_mem_match:
+  init_mem p' = init_mem p.
+Proof.
+  unfold init_mem. unfold globalenv_initmem.
+  destruct match_prog as [X [Y Z]]. 
+  symmetry. apply mem_add_globals_match. auto.
+Qed.
+
+End MATCH_PROGRAM.
+
+Section TRANSF_PROGRAM_PARTIAL2.
+
+Variable A B V W: Set.
+Variable transf_fun: A -> res B.
+Variable transf_var: V -> res W.
+Variable p: program A V.
+Variable p': program B W.
+Hypothesis transf_OK:
+  transform_partial_program2 transf_fun transf_var p = OK p'.
+
+Remark prog_match:
+  match_program
+    (fun fd tfd => transf_fun fd = OK tfd)
+    (fun info tinfo => transf_var info = OK tinfo)
+    p p'.
+Proof.
+  apply transform_partial_program2_match; auto.
+Qed.
+
+Theorem find_funct_ptr_transf_partial2:
+  forall (b: block) (f: A),
+  find_funct_ptr (globalenv p) b = Some f ->
+  exists f',
+  find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
+Proof.
+  intros. 
+  exploit find_funct_ptr_match. eexact prog_match. eauto. 
+  intros [tf [X Y]]. exists tf; auto.
+Qed.
+
+Theorem find_funct_ptr_rev_transf_partial2:
+  forall (b: block) (tf: B),
+  find_funct_ptr (globalenv p') b = Some tf ->
+  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.
+Proof.
+  intros. 
+  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. 
+Qed.
+
+Theorem find_funct_transf_partial2:
+  forall (v: val) (f: A),
+  find_funct (globalenv p) v = Some f ->
+  exists f',
+  find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
+Proof.
+  intros. 
+  exploit find_funct_match. eexact prog_match. eauto. 
+  intros [tf [X Y]]. exists tf; auto.
+Qed.
+
+Theorem find_funct_rev_transf_partial2:
+  forall (v: val) (tf: B),
+  find_funct (globalenv p') v = Some tf ->
+  exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.
+Proof.
+  intros. 
+  exploit find_funct_rev_match. eexact prog_match. eauto. auto. 
+Qed.
+
+Theorem find_symbol_transf_partial2:
+  forall (s: ident),
+  find_symbol (globalenv p') s = find_symbol (globalenv p) s.
+Proof.
+  intros. eapply find_symbol_match. eexact prog_match.
 Qed.
 
 Theorem init_mem_transf_partial2:
   init_mem p' = init_mem p.
 Proof.
-  unfold init_mem. unfold globalenv_initmem. 
-  functional inversion transf_OK.
-  simpl. symmetry. apply mem_add_globals_transf. auto.
+  intros. eapply init_mem_match. eexact prog_match.
 Qed.
 
 End TRANSF_PROGRAM_PARTIAL2.
 
-
 Section TRANSF_PROGRAM_PARTIAL.
 
 Variable A B V: Set.
-Variable transf: A -> option B.
+Variable transf: A -> res B.
 Variable p: program A V.
 Variable p': program B V.
-Hypothesis transf_OK: transform_partial_program transf p = Some p'.
+Hypothesis transf_OK: transform_partial_program transf p = OK p'.
 
 Remark transf2_OK:
-  transform_partial_program2 transf (fun x => Some x) p = Some p'.
+  transform_partial_program2 transf (fun x => OK x) p = OK p'.
 Proof.
   rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
-  destruct (map_partial transf (prog_funct p)); auto.
+  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
   rewrite map_partial_identity; auto. 
 Qed.
 
 Theorem find_funct_ptr_transf_partial:
   forall (b: block) (f: A),
   find_funct_ptr (globalenv p) b = Some f ->
-  find_funct_ptr (globalenv p') b = transf f /\ transf f <> None.
+  exists f',
+  find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'.
 Proof.
   exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
 Qed.
 
+Theorem find_funct_ptr_rev_transf_partial:
+  forall (b: block) (tf: B),
+  find_funct_ptr (globalenv p') b = Some tf ->
+  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf.
+Proof.
+  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+Qed.
+
 Theorem find_funct_transf_partial:
   forall (v: val) (f: A),
   find_funct (globalenv p) v = Some f ->
-  find_funct (globalenv p') v = transf f /\ transf f <> None.
+  exists f',
+  find_funct (globalenv p') v = Some f' /\ transf f = OK f'.
 Proof.
   exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
 Qed.
 
+Theorem find_funct_rev_transf_partial:
+  forall (v: val) (tf: B),
+  find_funct (globalenv p') v = Some tf ->
+  exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf.
+Proof.
+  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+Qed.
+
 Theorem find_symbol_transf_partial:
   forall (s: ident),
   find_symbol (globalenv p') s = find_symbol (globalenv p) s.
@@ -663,7 +989,7 @@ Variable p: program A V.
 Let tp := transform_program transf p.
 
 Remark transf_OK:
-  transform_partial_program (fun x => Some (transf x)) p = Some tp.
+  transform_partial_program (fun x => OK (transf x)) p = OK tp.
 Proof.
   unfold tp, transform_program, transform_partial_program.
   rewrite map_partial_total. reflexivity.
@@ -676,7 +1002,16 @@ Theorem find_funct_ptr_transf:
 Proof.
   intros. 
   destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK _ _ H)
-  as [X Y]. auto.
+  as [f' [X Y]]. congruence.
+Qed.
+
+Theorem find_funct_ptr_rev_transf:
+  forall (b: block) (tf: B),
+  find_funct_ptr (globalenv tp) b = Some tf ->
+  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf.
+Proof.
+  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
+  intros [f [X Y]]. exists f; split. auto. congruence.
 Qed.
 
 Theorem find_funct_transf:
@@ -686,7 +1021,16 @@ Theorem find_funct_transf:
 Proof.
   intros. 
   destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK _ _ H)
-  as [X Y]. auto.
+  as [f' [X Y]]. congruence.
+Qed.
+
+Theorem find_funct_rev_transf:
+  forall (v: val) (tf: B),
+  find_funct (globalenv tp) v = Some tf ->
+  exists f, find_funct (globalenv p) v = Some f /\ transf f = tf.
+Proof.
+  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
+  intros [f [X Y]]. exists f; split. auto. congruence.
 Qed.
 
 Theorem find_symbol_transf:
diff --git a/common/Main.v b/common/Main.v
index f472ec3..33bc783 100644
--- a/common/Main.v
+++ b/common/Main.v
@@ -1,40 +1,48 @@
-(** The compiler back-end and its proof of semantic preservation *)
+(** The whole compiler and its proof of semantic preservation *)
 
 (** Libraries. *)
 Require Import Coqlib.
 Require Import Maps.
+Require Import Errors.
 Require Import AST.
 Require Import Values.
+Require Import Smallstep.
 (** Languages (syntax and semantics). *)
 Require Csyntax.
 Require Csem.
 Require Csharpminor.
 Require Cminor.
+Require CminorSel.
 Require RTL.
 Require LTL.
+Require LTLin.
 Require Linear.
 Require Mach.
 Require PPC.
 (** Translation passes. *)
 Require Cshmgen.
 Require Cminorgen.
+Require Selection.
 Require RTLgen.
 Require Constprop.
 Require CSE.
 Require Allocation.
 Require Tunneling.
 Require Linearize.
+Require Reload.
 Require Stacking.
 Require PPCgen.
 (** Type systems. *)
 Require Ctyping.
 Require RTLtyping.
 Require LTLtyping.
+Require LTLintyping.
 Require Lineartyping.
 Require Machtyping.
 (** Proofs of semantic preservation and typing preservation. *)
 Require Cshmgenproof3.
 Require Cminorgenproof.
+Require Selectionproof.
 Require RTLgenproof.
 Require Constpropproof.
 Require CSEproof.
@@ -44,266 +52,234 @@ Require Tunnelingproof.
 Require Tunnelingtyping.
 Require Linearizeproof.
 Require Linearizetyping.
+Require Reloadproof.
+Require Reloadtyping.
 Require Stackingproof.
 Require Stackingtyping.
-Require Machabstr2mach.
+Require Machabstr2concr.
 Require PPCgenproof.
 
+Open Local Scope string_scope.
+
 (** * Composing the translation passes *)
 
 (** We first define useful monadic composition operators,
     along with funny (but convenient) notations. *)
 
-Definition apply_total (A B: Set) (x: option A) (f: A -> B) : option B :=
-  match x with None => None | Some x1 => Some (f x1) end.
+Definition apply_total (A B: Set) (x: res A) (f: A -> B) : res B :=
+  match x with Error msg => Error msg | OK x1 => OK (f x1) end.
 
 Definition apply_partial (A B: Set)
-                         (x: option A) (f: A -> option B) : option B :=
-  match x with None => None | Some x1 => f x1 end.
+                         (x: res A) (f: A -> res B) : res B :=
+  match x with Error msg => Error msg | OK x1 => f x1 end.
 
 Notation "a @@@ b" :=
    (apply_partial _ _ a b) (at level 50, left associativity).
 Notation "a @@ b" :=
    (apply_total _ _ a b) (at level 50, left associativity).
 
-(** We define two translation functions for whole programs: one starting with
-  a C program, the other with a Cminor program.  Both
-  translations produce PPC programs ready for pretty-printing and
-  assembling.  
+(** We define three translation functions for whole programs: one
+  starting with a C program, one with a Cminor program, one with an
+  RTL program.  The three translations produce PPC programs ready for
+  pretty-printing and assembling.
 
-  There are two ways to compose the compiler passes.  The first translates
-  every function from the Cminor program from Cminor to RTL, then to LTL, etc,
-  all the way to PPC, and iterates this transformation for every function.
-  The second translates the whole Cminor program to a RTL program, then to
-  an LTL program, etc.  We follow the first approach because it has lower
-  memory requirements.
+  There are two ways to compose the compiler passes.  The first
+  translates every function from the Cminor program from Cminor to
+  RTL, then to LTL, etc, all the way to PPC, and iterates this
+  transformation for every function.  The second translates the whole
+  Cminor program to a RTL program, then to an LTL program, etc. 
+  Between Cminor and PPC, we follow the first approach because it has
+  lower memory requirements.  The translation from Clight to PPC
+  follows the second approach.
   
-  The translation of a Cminor function to a PPC function is as follows. *)
+  The translation of an RTL function to a PPC function is as follows. *)
 
-Definition transf_cminor_fundef (f: Cminor.fundef) : option PPC.fundef :=
-  Some f
-  @@@ RTLgen.transl_fundef
+Definition transf_rtl_fundef (f: RTL.fundef) : res PPC.fundef :=
+   OK f
    @@ Constprop.transf_fundef
    @@ CSE.transf_fundef
   @@@ Allocation.transf_fundef
    @@ Tunneling.tunnel_fundef
    @@ Linearize.transf_fundef
+   @@ Reload.transf_fundef
   @@@ Stacking.transf_fundef
   @@@ PPCgen.transf_fundef.
 
+(* Here is the translation of a Cminor function to a PPC function. *)
+
+Definition transf_cminor_fundef (f: Cminor.fundef) : res PPC.fundef :=
+  OK f
+   @@ Selection.sel_fundef
+  @@@ RTLgen.transl_fundef
+  @@@ transf_rtl_fundef.
+
 (** The corresponding translations for whole program follow. *)
 
-Definition transf_cminor_program (p: Cminor.program) : option PPC.program :=
+Definition transf_rtl_program (p: RTL.program) : res PPC.program :=
+  transform_partial_program transf_rtl_fundef p.
+
+Definition transf_cminor_program (p: Cminor.program) : res PPC.program :=
   transform_partial_program transf_cminor_fundef p.
 
-Definition transf_c_program (p: Csyntax.program) : option PPC.program :=
+Definition transf_c_program (p: Csyntax.program) : res PPC.program :=
   match Ctyping.typecheck_program p with
-  | false => None
+  | false =>
+      Error (msg "Ctyping: type error")
   | true =>
-      Some p 
+      OK p 
       @@@ Cshmgen.transl_program
       @@@ Cminorgen.transl_program
       @@@ transf_cminor_program
   end.
 
-(** * Equivalence with whole program transformations *)
-
-(** To prove semantic preservation for the whole compiler, it is easier to reason
-  over the second way to compose the compiler pass: the one that translate
-  whole programs through each compiler pass.  We now define this second translation
-  and prove that it produces the same PPC programs as the first translation. *)
-
-Definition transf_cminor_program2 (p: Cminor.program) : option PPC.program :=
-  Some p
-  @@@ RTLgen.transl_program
-   @@ Constprop.transf_program
-   @@ CSE.transf_program
-  @@@ Allocation.transf_program
-   @@ Tunneling.tunnel_program
-   @@ Linearize.transf_program
-  @@@ Stacking.transf_program
-  @@@ PPCgen.transf_program.
+(** The following lemmas help reason over compositions of passes. *)
 
 Lemma map_partial_compose:
   forall (X A B C: Set)
-         (f1: A -> option B) (f2: B -> option C)
-         (p: list (X * A)),
-  map_partial f1 p @@@ map_partial f2 =
-  map_partial (fun f => f1 f @@@ f2) p.
+         (ctx: X -> errmsg)
+         (f1: A -> res B) (f2: B -> res C)
+         (pa: list (X * A)) (pc: list (X * C)),
+  map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc ->
+  exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc.
 Proof.
-  induction p. simpl. auto.
-  simpl. destruct a. destruct (f1 a). 
-  simpl. simpl in IHp. destruct (map_partial f1 p).
-  simpl. simpl in IHp. destruct (f2 b).
-  destruct (map_partial f2 l). 
-  rewrite <- IHp. auto.
-  rewrite <- IHp. auto.
-  auto.
-  simpl. rewrite <- IHp. simpl. destruct (f2 b); auto.
-  simpl. auto.
+  induction pa; simpl.
+  intros. inv H. econstructor; eauto.
+  intro pc. destruct a as [x a].
+  caseEq (f1 a); simpl; try congruence. intros b F1.
+  caseEq (f2 b); simpl; try congruence. intros c F2 EQ.
+  monadInv EQ. exploit IHpa; eauto. intros [pb [P Q]]. 
+  rewrite P; simpl.
+  exists ((x, b) :: pb); split. auto. simpl. rewrite F2. rewrite Q. auto. 
 Qed.
 
-(*
-Lemma transform_partial_program2_compose:
-  forall (A B C V W X: Set)
-         (f1: A -> option B) (g1: V -> option W)
-         (f2: B -> option C) (g2: W -> option X)
-         (p: program A V),
-  transform_partial_program2 f1 g1 p @@@
-                  (fun p' => transform_partial_program2 f2 g2 p') =
-  transform_partial_program2 (fun x => f1 x @@@ f2) (fun x => g1 x @@@ g2) p.
+Lemma transform_partial_program_compose:
+  forall (A B C V: Set)
+         (f1: A -> res B) (f2: B -> res C)
+         (pa: program A V) (pc: program C V),
+  transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc ->
+  exists pb, transform_partial_program f1 pa = OK pb /\
+             transform_partial_program f2 pb = OK pc.
 Proof.
-  unfold transform_partial_program2; intros.
-  rewrite <- map_partial_compose; simpl.
-  rewrite <- map_partial_compose; simpl.
-  destruct (map_partial f1 (prog_funct p)); simpl; auto.
-  destruct (map_partial g1 (prog_vars p)); simpl; auto.
-  destruct (map_partial f2 l); auto.
+  intros. monadInv H. 
+  exploit map_partial_compose; eauto. intros [xb [P Q]].
+  exists (mkprogram xb (prog_main pa) (prog_vars pa)); split.
+  unfold transform_partial_program. rewrite P; auto. 
+  unfold transform_partial_program. simpl. rewrite Q; auto.
 Qed.
 
-Lemma transform_program_partial2_partial:
-  forall (A B V: Set) (f: A -> option B) (p: program A V),
-  transform_partial_program f p =
-  transform_partial_program2 f (fun x => Some x) p.
+Lemma transform_program_partial_program:
+  forall (A B V: Set) (f: A -> B) (p: program A V) (tp: program B V),
+  transform_partial_program (fun x => OK (f x)) p = OK tp ->
+  transform_program f p = tp.
 Proof.
-  intros. unfold transform_partial_program, transform_partial_program2.
-  rewrite map_partial_identity. auto.
+  intros until tp. unfold transform_partial_program. 
+  rewrite map_partial_total. simpl. intros. inv H. auto. 
 Qed.
 
-Lemma apply_partial_transf_program:
-  forall (A B V: Set) (f: A -> option B) (x: option (program A V)),
-  x @@@ (fun p => transform_partial_program f p) =
-  x @@@ (fun p => transform_partial_program2 f (fun x => Some x) p).
-Proof.
-  intros. unfold apply_partial. 
-  destruct x. apply transform_program_partial2_partial. auto.
-Qed.
-*)
-Lemma transform_partial_program_compose:
+Lemma transform_program_compose:
   forall (A B C V: Set)
-         (f1: A -> option B) (f2: B -> option C)
-         (p: program A V),
-  transform_partial_program f1 p @@@
-                       (fun p' => transform_partial_program f2 p') =
-  transform_partial_program (fun f => f1 f @@@ f2) p.
+         (f1: A -> res B) (f2: B -> C)
+         (pa: program A V) (pc: program C V),
+  transform_partial_program (fun f => f1 f @@ f2) pa = OK pc ->
+  exists pb, transform_partial_program f1 pa = OK pb /\
+             transform_program f2 pb = pc.
 Proof.
-  unfold transform_partial_program; intros.
-  rewrite <- map_partial_compose. simpl. 
-  destruct (map_partial f1 (prog_funct p)); simpl.
-  auto. auto. 
+  intros. 
+  replace (fun f : A => f1 f @@ f2)
+     with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H.
+  exploit transform_partial_program_compose; eauto.
+  intros [pb [X Y]]. exists pb; split. auto. 
+  apply transform_program_partial_program. auto. 
+  apply extensionality; intro. destruct(f1 x); auto. 
 Qed.
 
-Lemma transform_program_partial_total:
-  forall (A B V: Set) (f: A -> B) (p: program A V),
-  Some (transform_program f p) =
-    transform_partial_program (fun x => Some (f x)) p.
+Lemma transform_partial_program_identity:
+  forall (A V: Set) (pa pb: program A V),
+  transform_partial_program (@OK A) pa = OK pb ->
+  pa = pb.
 Proof.
-  intros. unfold transform_program, transform_partial_program.
-  rewrite map_partial_total. auto. 
+  intros until pb. unfold transform_partial_program. 
+  replace (@OK A) with (fun b => @OK A b).
+  rewrite map_partial_identity. simpl. destruct pa; simpl; congruence.
+  apply extensionality; auto. 
 Qed.
 
-Lemma apply_total_transf_program:
-  forall (A B V: Set) (f: A -> B) (x: option (program A V)),
-  x @@ (fun p => transform_program f p) =
-  x @@@ (fun p => transform_partial_program (fun x => Some (f x)) p).
-Proof.
-  intros. unfold apply_total, apply_partial. 
-  destruct x. apply transform_program_partial_total. auto.
-Qed.
+(** * Semantic preservation *)
 
-Lemma transf_cminor_program_equiv:
-  forall p, transf_cminor_program2 p = transf_cminor_program p.
-Proof.
-  intro. unfold transf_cminor_program, transf_cminor_program2, transf_cminor_fundef.
-  simpl. 
-  unfold RTLgen.transl_program,
-         Constprop.transf_program, RTL.program.
-  rewrite apply_total_transf_program.  
-  rewrite transform_partial_program_compose.
-  unfold CSE.transf_program, RTL.program.
-  rewrite apply_total_transf_program.
-  rewrite transform_partial_program_compose.
-  unfold Allocation.transf_program,
-         LTL.program, RTL.program. 
-  rewrite transform_partial_program_compose.
-  unfold Tunneling.tunnel_program, LTL.program.
-  rewrite apply_total_transf_program.
-  rewrite transform_partial_program_compose.
-  unfold Linearize.transf_program, LTL.program, Linear.program.
-  rewrite apply_total_transf_program. 
-  rewrite transform_partial_program_compose.
-  unfold Stacking.transf_program, Linear.program, Mach.program.
-  rewrite transform_partial_program_compose.
-  unfold PPCgen.transf_program, Mach.program, PPC.program.
-  rewrite transform_partial_program_compose.
-  reflexivity.
-Qed.
+(** We prove that the [transf_program] translations preserve semantics.
+  The proof composes the semantic preservation results for each pass.
+  This establishes the correctness of the whole compiler! *)
 
-(*
-Lemma transf_csharpminor_program_equiv:
-  forall p, transf_csharpminor_program2 p = transf_csharpminor_program p.
+Theorem transf_rtl_program_correct:
+  forall p tp beh,
+  transf_rtl_program p = OK tp ->
+  RTL.exec_program p beh ->
+  PPC.exec_program tp beh.
 Proof.
-  intros. 
-  unfold transf_csharpminor_program2, transf_csharpminor_program, transf_csharpminor_fundef.
-  simpl. 
-  replace transf_cminor_program2 with transf_cminor_program.
-  unfold transf_cminor_program, Cminorgen.transl_program, Cminor.program, PPC.program.
-  rewrite apply_partial_transf_program.
-  rewrite transform_partial_program2_compose.
-  reflexivity.
-  symmetry. apply extensionality. exact transf_cminor_program_equiv.
-Qed.
-*)
+  intros. unfold transf_rtl_program, transf_rtl_fundef in H.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p7 [H7 P7]].
+  clear H.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H7) as [p6 [H6 P6]].
+  clear H7.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]].
+  clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]].
+  clear H5. generalize (transform_program_partial_program _ _ _ _ _ _ P4). clear P4. intro P4.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]].
+  clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]].
+  clear H3.
+  destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]].
+  clear H2.
+  destruct (transform_program_compose _ _ _ _ _ _ _ _ H1) as [p0 [H00 P0]].
+  clear H1.
+  generalize (transform_partial_program_identity _ _ _ _ H00). clear H00. intro. subst p0.
 
-(** * Semantic preservation *)
+  assert (WT3 : LTLtyping.wt_program p3).
+    apply Alloctyping.program_typing_preserved with p2. auto.
+  assert (WT4 : LTLtyping.wt_program p4).
+    subst p4. apply Tunnelingtyping.program_typing_preserved. auto.
+  assert (WT5 : LTLintyping.wt_program p5).
+    subst p5. apply Linearizetyping.program_typing_preserved. auto.
+  assert (WT6 : Lineartyping.wt_program p6).
+    subst p6. apply Reloadtyping.program_typing_preserved. auto.
+  assert (WT7: Machtyping.wt_program p7).
+    apply Stackingtyping.program_typing_preserved with p6. auto. auto.
 
-(** We prove that the [transf_program] translations preserve semantics.  The proof
-  composes the semantic preservation results for each pass.
-  This establishes the correctness of the whole compiler! *)
+  apply PPCgenproof.transf_program_correct with p7; auto.
+  apply Machabstr2concr.exec_program_equiv; auto.
+  apply Stackingproof.transf_program_correct with p6; auto.
+  subst p6; apply Reloadproof.transf_program_correct; auto.
+  subst p5; apply Linearizeproof.transf_program_correct; auto.
+  subst p4; apply Tunnelingproof.transf_program_correct. 
+  apply Allocproof.transf_program_correct with p2; auto.
+  subst p2; apply CSEproof.transf_program_correct.
+  subst p1; apply Constpropproof.transf_program_correct. auto.
+Qed.
 
 Theorem transf_cminor_program_correct:
   forall p tp t n,
-  transf_cminor_program p = Some tp ->
+  transf_cminor_program p = OK tp ->
   Cminor.exec_program p t (Vint n) ->
-  PPC.exec_program tp t (Vint n).
+  PPC.exec_program tp (Terminates t n).
 Proof.
-  intros until n.
-  rewrite <- transf_cminor_program_equiv.
-  unfold transf_cminor_program2.
-  simpl. caseEq (RTLgen.transl_program p). intros p1 EQ1. 
-  simpl. set (p2 := CSE.transf_program (Constprop.transf_program p1)).
-  caseEq (Allocation.transf_program p2). intros p3 EQ3.
-  simpl. set (p4 := Tunneling.tunnel_program p3).
-  set (p5 := Linearize.transf_program p4).
-  caseEq (Stacking.transf_program p5). intros p6 EQ6.
-  simpl. intros EQTP EXEC.
-  assert (WT3 : LTLtyping.wt_program p3).
-    apply Alloctyping.program_typing_preserved with p2. auto.
-  assert (WT4 : LTLtyping.wt_program p4).
-    unfold p4. apply Tunnelingtyping.program_typing_preserved. auto.
-  assert (WT5 : Lineartyping.wt_program p5).
-    unfold p5. apply Linearizetyping.program_typing_preserved. auto.
-  assert (WT6: Machtyping.wt_program p6).
-    apply Stackingtyping.program_typing_preserved with p5. auto. auto.
-  apply PPCgenproof.transf_program_correct with p6; auto.
-  apply Machabstr2mach.exec_program_equiv; auto.
-  apply Stackingproof.transl_program_correct with p5; auto.
-  unfold p5; apply Linearizeproof.transf_program_correct. 
-  unfold p4; apply Tunnelingproof.transf_program_correct. 
-  apply Allocproof.transl_program_correct with p2; auto.
-  unfold p2; apply CSEproof.transf_program_correct;
-  apply Constpropproof.transf_program_correct.
-  apply RTLgenproof.transl_program_correct with p; auto.
-  simpl; intros; discriminate.
-  simpl; intros; discriminate.
-  simpl; intros; discriminate.
+  intros. unfold transf_cminor_program, transf_cminor_fundef in H.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [H3 P3]].
+  clear H.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]].
+  clear H3.
+  destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]].
+  generalize (transform_partial_program_identity _ _ _ _ H1). clear H1. intro. subst p1.
+  apply transf_rtl_program_correct with p3. auto.
+  apply RTLgenproof.transl_program_correct with p2; auto.
+  rewrite <- P1. apply Selectionproof.sel_program_correct; auto.
 Qed.
 
 Theorem transf_c_program_correct:
   forall p tp t n,
-  transf_c_program p = Some tp ->
+  transf_c_program p = OK tp ->
   Csem.exec_program p t (Vint n) ->
-  PPC.exec_program tp t (Vint n).
+  PPC.exec_program tp (Terminates t n).
 Proof.
   intros until n; unfold transf_c_program; simpl.
   caseEq (Ctyping.typecheck_program p); try congruence; intro.
diff --git a/common/Mem.v b/common/Mem.v
index 679c41e..6b66d9d 100644
--- a/common/Mem.v
+++ b/common/Mem.v
@@ -1,11 +1,11 @@
 (** This file develops the memory model that is used in the dynamic
-  semantics of all the languages of the compiler back-end.
+  semantics of all the languages used in the compiler.
   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.
+- [store]: store a memory chunk at a given address;
+- [alloc]: allocate a fresh memory block;
+- [free]: invalidate a memory block.
 *)
   
 Require Import Coqlib.
@@ -15,12 +15,6 @@ 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.
 
@@ -40,32 +34,32 @@ Proof.
   intros; unfold update. apply zeq_false; auto.
 Qed.
 
+(** * 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. *)
+
 (** 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],
+  the content [Datum(4, 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. *)
+  that would partially overlap 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 *)
+  | Undef: content                 (**r undefined contents *)
+  | Datum: nat -> val -> content   (**r first byte of a 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. *)
+  plus a mapping from byte offsets to contents.  *)
 
 Record block_contents : Set := mkblock {
   low: Z;
   high: Z;
-  contents: contentmap;
-  undef_outside: forall ofs, ofs < low \/ ofs >= high -> contents ofs = Undef
+  contents: contentmap
 }.
 
 (** A memory state is a mapping from block addresses (represented by [Z]
@@ -82,49 +76,43 @@ Record mem : Set := mkmem {
 
 (** 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
+  The following functions extract the size information from a chunk. *)
+
+Definition size_chunk (chunk: memory_chunk) : Z :=
+  match chunk with
+  | Mint8signed => 1
+  | Mint8unsigned => 1
+  | Mint16signed => 2
+  | Mint16unsigned => 2
+  | Mint32 => 4
+  | Mfloat32 => 4
+  | Mfloat64 => 8
   end.
 
-Definition mem_chunk (chunk: memory_chunk) :=
+Definition pred_size_chunk (chunk: memory_chunk) : nat :=
   match chunk with
-  | Mint8signed => Size8
-  | Mint8unsigned => Size8
-  | Mint16signed => Size16
-  | Mint16unsigned => Size16
-  | Mint32 => Size32
-  | Mfloat32 => Size32
-  | Mfloat64 => Size64
+  | Mint8signed => 0%nat
+  | Mint8unsigned => 0%nat
+  | Mint16signed => 1%nat
+  | Mint16unsigned => 1%nat
+  | Mint32 => 3%nat
+  | Mfloat32 => 3%nat
+  | Mfloat64 => 7%nat
   end.
 
-Definition size_chunk (chunk: memory_chunk) := size_mem (mem_chunk chunk).
+Lemma size_chunk_pred:
+  forall chunk, size_chunk chunk = 1 + Z_of_nat (pred_size_chunk chunk).
+Proof.
+  destruct chunk; auto.
+Qed.
 
 (** 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).
+  mkblock lo hi (fun y => Undef).
 
 Definition empty: mem :=
   mkmem (fun x => empty_block 0 0) 1 one_pos.
@@ -200,8 +188,16 @@ Fixpoint check_cont (n: nat) (p: Z) (m: contentmap) {struct n} : bool :=
       end
   end.
 
-Definition getN (n: nat) (p: Z) (m: contentmap) : content :=
-  if check_cont n (p + 1) m then m p else Undef.
+Definition eq_nat: forall (p q: nat), {p=q} + {p<>q}.
+Proof. decide equality. Defined.
+
+Definition getN (n: nat) (p: Z) (m: contentmap) : val :=
+  match m p with
+  | Datum n' v =>
+      if eq_nat n n' && check_cont n (p + 1) m then v else Vundef
+  | _ =>
+      Vundef
+  end.
 
 Fixpoint set_cont (n: nat) (p: Z) (m: contentmap) {struct n} : contentmap :=
   match n with
@@ -209,54 +205,47 @@ Fixpoint set_cont (n: nat) (p: Z) (m: contentmap) {struct n} : contentmap :=
   | 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).
+Definition setN (n: nat) (p: Z) (v: val) (m: contentmap) : contentmap :=
+  update p (Datum n 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.
+Lemma check_cont_spec:
+  forall n m p,
+  if check_cont n p m
+  then (forall q, p <= q < p + Z_of_nat n -> m q = Cont)
+  else (exists q, p <= q < p + Z_of_nat n /\ m q <> Cont).
 Proof.
   induction n; intros.
-  reflexivity.
-  simpl. rewrite H. apply IHn. 
-  intros. apply H. rewrite inj_S. omega.
-  rewrite inj_S. omega. 
+  simpl. intros; omegaContradiction.
+  simpl check_cont. repeat rewrite inj_S. caseEq (m p); intros.
+  exists p; split. omega. congruence.
+  exists p; split. omega. congruence.
+  generalize (IHn m (p + 1)). case (check_cont n (p + 1) m).
+  intros. assert (p = q \/ p + 1 <= q < p + Zsucc (Z_of_nat n)) by omega.
+  elim H2; intro. congruence. apply H0; omega.
+  intros [q [A B]]. exists q; split. omega. auto.
 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).
+Lemma check_cont_true:
+  forall n m p,
+  (forall q, p <= q < p + Z_of_nat n -> m q = Cont) ->
+  check_cont n p m = true.
 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.
+  intros. generalize (check_cont_spec n m p). 
+  destruct (check_cont n p m). auto. 
+  intros [q [A B]]. elim B; 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 ->
+  forall n m p q,
+  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.
+  intros. generalize (check_cont_spec n m p). 
+  destruct (check_cont n p m).
+  intros. elim H0; auto. 
   auto.
 Qed.
 
-Hint Resolve check_cont_false.
-
 Lemma set_cont_inside:
   forall n p m q,
   p <= q < p + Z_of_nat n ->
@@ -273,8 +262,6 @@ Proof.
   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 ->
@@ -286,160 +273,133 @@ Proof.
   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. unfold getN, setN. rewrite update_s.
+  rewrite check_cont_true. unfold proj_sumbool.
+  rewrite dec_eq_true. auto.
   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.
+  generalize (check_cont_spec n2 m (p2 + 1));
+  destruct (check_cont n2 (p2 + 1) m); intros.
+  rewrite check_cont_true. 
+  rewrite update_o. rewrite set_cont_outside. 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.
+  intros. rewrite update_o. rewrite set_cont_outside. auto.
+  omega. omega.
+  destruct H0 as [q [A B]].
+  rewrite (check_cont_false n2 (update p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) q).
+  rewrite update_o. rewrite set_cont_outside. auto.
+  omega. omega. omega. 
+  rewrite update_o. rewrite set_cont_outside. auto. 
+  omega. omega.
+Qed.
 
 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.
+  getN n2 p2 (setN n1 p1 v m) = Vundef.
+Proof.
+  intros. unfold getN, setN.
+  rewrite update_o; auto. 
+  destruct (zlt p2 p1).
+  (* [p1] belongs to [[p2, p2 + n2 - 1]], 
+     therefore [check_cont n2 (p2 + 1) ...] is false. *)
+  rewrite (check_cont_false n2 (update p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) p1).
+  destruct (set_cont n1 (p1 + 1) m p2); auto.
+  destruct (eq_nat n2 n); auto.
+  omega.
+  rewrite update_s. congruence.
+  (* [p2] belongs to [[p1 + 1, p1 + n1 - 1]],
+     therefore [set_cont n1 (p1 + 1) m p2] is [Cont]. *)
+  rewrite set_cont_inside. auto. omega.
+Qed.
 
 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.
+  n1 <> n2 ->
+  getN n2 p (setN n1 p v m) = Vundef.
 Proof.
-  intros. unfold getN. 
-  caseEq (check_cont n2 (p + 1) (setN n1 p v m)); intro.
-  left. unfold setN. apply update_s.
-  right. auto.
+  intros. unfold getN, setN. rewrite update_s. 
+  unfold proj_sumbool; rewrite dec_eq_false; simpl. auto. auto.
 Qed.
 
-Hint Resolve getN_setN_mismatch.
+Lemma getN_setN_characterization:
+  forall m v n1 p1 n2 p2,
+  getN n2 p2 (setN n1 p1 v m) = v
+  \/ getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m
+  \/ getN n2 p2 (setN n1 p1 v m) = Vundef.
+Proof.
+  intros. destruct (zeq p1 p2). subst p2.
+  destruct (eq_nat n1 n2). subst n2.
+  left; apply getN_setN_same.
+  right; right; apply getN_setN_mismatch; auto.
+  destruct (zlt (p1 + Z_of_nat n1) p2).
+  right; left; apply getN_setN_other; auto.
+  destruct (zlt (p2 + Z_of_nat n2) p1).
+  right; left; apply getN_setN_other; auto.
+  right; right; apply getN_setN_overlap; omega.
+Qed.
 
 Lemma getN_init:
   forall n p,
-  getN n p (fun y => Undef) = Undef.
+  getN n p (fun y => Undef) = Vundef.
 Proof.
-  intros. unfold getN.
-  case (check_cont n (p + 1) (fun y => Undef)); auto.
+  intros. auto.
 Qed.
 
-Hint Resolve getN_init.
+(** [valid_access m chunk b ofs] holds if a memory access (load or store)
+    of the given chunk is possible in [m] at address [b, ofs]. *)
+
+Inductive valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) : Prop :=
+  | valid_access_intro:
+      valid_block m b ->
+      low_bound m b <= ofs ->
+      ofs + size_chunk chunk <= high_bound m b ->
+      valid_access m chunk b ofs.
 
 (** 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.
+Definition in_bounds (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) :
+           {valid_access m chunk b ofs} + {~valid_access m chunk b ofs}.
 Proof.
-  intros. case (in_bounds chunk ofs c); intro.
-  auto.
-  omegaContradiction.
-Qed.
+  intros.
+  destruct (zlt b m.(nextblock)).
+  destruct (zle (low_bound m b) ofs).
+  destruct (zle (ofs + size_chunk chunk) (high_bound m b)).
+  left; constructor; auto.
+  right; red; intro V; inv V; omega.
+  right; red; intro V; inv V; omega.
+  right; red; intro V; inv V; contradiction.
+Defined.
 
-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.
+Lemma in_bounds_true:
+  forall m chunk b ofs (A: Set) (a1 a2: A),
+  valid_access m chunk b ofs ->
+  (if in_bounds m chunk b ofs then a1 else a2) = a1.
 Proof.
-  intros; reflexivity.
+  intros. destruct (in_bounds m chunk b ofs). auto. contradiction.
 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.
+  zlt b m.(nextblock) &&
+  zle (low_bound m b) ofs &&
+  zlt ofs (high_bound m b).
 
 (** [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
@@ -447,15 +407,25 @@ Definition load_contents (sz: memory_size) (c: contentmap) (ofs: Z) : val :=
 
 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)
+  if in_bounds m chunk b ofs then
+    Some (Val.load_result chunk
+           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))))
   else
     None.
 
+Lemma load_inv:
+  forall chunk m b ofs v,
+  load chunk m b ofs = Some v ->
+  valid_access m chunk b ofs /\
+  v = Val.load_result chunk
+           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))).
+Proof.
+  intros until v; unfold load.
+  destruct (in_bounds m chunk b ofs); intros.
+  split. auto. congruence.
+  congruence.
+Qed. 
+
 (** [loadv chunk m addr] is similar, but the address and offset are given
   as a single value [addr], which must be a pointer value. *)
 
@@ -465,90 +435,17 @@ Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
   | _ => 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.
+(* The memory state [m] after a store of value [v] at offset [ofs]
+   in block [b]. *)
 
 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 :=
+     (ofs: Z) (v: val) : 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)))
+                 (setN (pred_size_chunk chunk) ofs v c.(contents)))
         m.(blocks))
     m.(nextblock)
     m.(nextblock_pos).
@@ -560,13 +457,21 @@ Definition unchecked_store
 
 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.
+  if in_bounds m chunk b ofs
+  then Some(unchecked_store chunk m b ofs v)
+  else None.
+
+Lemma store_inv:
+  forall chunk m b ofs v m',
+  store chunk m b ofs v = Some m' ->
+  valid_access m chunk b ofs /\
+  m' = unchecked_store chunk m b ofs v.
+Proof.
+  intros until m'; unfold store.
+  destruct (in_bounds m chunk b ofs); intros.
+  split. auto. congruence.
+  congruence.
+Qed.
 
 (** [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. *)
@@ -577,63 +482,21 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   | _ => 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)
+      setN 0%nat pos (Vint n) (contents_init_data (pos + 1) id')
   | Init_int16 n :: id' =>
-      store_contents Size16 (contents_init_data (pos + 2) id') pos (Vint n)
+      setN 1%nat pos (Vint n) (contents_init_data (pos + 1) id')
   | Init_int32 n :: id' =>
-      store_contents Size32 (contents_init_data (pos + 4) id') pos (Vint n)
+      setN 3%nat pos (Vint n) (contents_init_data (pos + 1) id')
   | Init_float32 f :: id' =>
-      store_contents Size32 (contents_init_data (pos + 4) id') pos (Vfloat f)
+      setN 3%nat pos (Vfloat f) (contents_init_data (pos + 1) id')
   | Init_float64 f :: id' =>
-      store_contents Size64 (contents_init_data (pos + 8) id') pos (Vfloat f)
+      setN 7%nat pos (Vfloat f) (contents_init_data (pos + 1) id')
   | Init_space n :: id' =>
       contents_init_data (pos + Zmax n 0) id'
   | Init_pointer x :: id' =>
@@ -664,32 +527,8 @@ Proof.
   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. 
-  apply IHid. 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).
+  mkblock 0 (size_init_data_list id) (contents_init_data 0 id).
 
 Definition alloc_init_data (m: mem) (id: list init_data) : mem * block :=
   (mkmem (update m.(nextblock)
@@ -702,8 +541,7 @@ Definition alloc_init_data (m: mem) (id: list init_data) : mem * block :=
 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. 
+  auto.
 Qed.
 
 (** * Properties of the memory operations *)
@@ -716,573 +554,961 @@ 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).
+Lemma valid_access_valid_block:
+  forall m chunk b ofs,
+  valid_access m chunk b ofs -> valid_block m b.
 Proof.
-  intros. injection H; intros; subst b. 
-  unfold valid_block. omega.
+  intros. inv H; auto.
 Qed.
 
-Theorem valid_new_block:
-  forall (m1 m2: mem) (lo hi: Z) (b: block), 
-  alloc m1 lo hi = (m2, b) -> valid_block m2 b.
+Hint Resolve valid_not_valid_diff valid_access_valid_block: mem.
+
+(** ** Properties related to [load] *)
+
+Theorem valid_access_load:
+  forall m chunk b ofs,
+  valid_access m chunk b ofs ->
+  exists v, load chunk m b ofs = Some v.
 Proof.
-  unfold alloc, valid_block; intros.
-  injection H; intros. subst b; subst m2; simpl. omega.
+  intros. econstructor. unfold load. rewrite in_bounds_true; auto.
 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.
+Theorem load_valid_access:
+  forall m chunk b ofs v,
+  load chunk m b ofs = Some v ->
+  valid_access m chunk b ofs.
 Proof.
-  unfold alloc, valid_block; intros.
-  injection H; intros. subst m2; simpl. omega.
+  intros. generalize (load_inv _ _ _ _ _ H). tauto.
 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.
+Hint Resolve load_valid_access valid_access_load.
+
+(** ** Properties related to [store] *)
+
+Lemma valid_access_store:
+  forall m1 chunk b ofs v,
+  valid_access m1 chunk b ofs ->
+  exists m2, store chunk m1 b ofs v = Some m2.
 Proof.
-  intros. generalize (store_inv _ _ _ _ _ _ H). 
-  intros [A [B [C [D [P E]]]]].
-  red. rewrite D. exact H0.
+  intros. econstructor. unfold store. rewrite in_bounds_true; auto. 
 Qed.
 
-Theorem valid_block_free:
-  forall (m: mem) (b b': block), 
-  valid_block m b -> valid_block (free m b') b.
+Hint Resolve valid_access_store: mem.
+
+Section STORE.
+Variable chunk: memory_chunk.
+Variable m1: mem.
+Variable b: block.
+Variable ofs: Z.
+Variable v: val.
+Variable m2: mem.
+Hypothesis STORE: store chunk m1 b ofs v = Some m2.
+
+Lemma low_bound_store:
+  forall b', low_bound m2 b' = low_bound m1 b'.
 Proof.
-  unfold valid_block, free; intros.
-  simpl. auto.
+  intro. elim (store_inv _ _ _ _ _ _ STORE); intros. 
+  subst m2. unfold low_bound, unchecked_store; simpl.
+  unfold update. destruct (zeq b' b); auto. subst b'; auto.
+Qed.
+
+Lemma high_bound_store:
+  forall b', high_bound m2 b' = high_bound m1 b'.
+Proof.
+  intro. elim (store_inv _ _ _ _ _ _ STORE); intros. 
+  subst m2. unfold high_bound, unchecked_store; simpl.
+  unfold update. destruct (zeq b' b); auto. subst b'; auto.
 Qed.
 
-(** ** Properties related to [alloc] *)
+Lemma nextblock_store:
+  nextblock m2 = nextblock m1.
+Proof.
+ intros. elim (store_inv _ _ _ _ _ _ STORE); intros. 
+  subst m2; reflexivity.
+Qed.
 
-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.
+Lemma store_valid_block_1:
+  forall b', valid_block m1 b' -> valid_block m2 b'.
 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.
+  unfold valid_block; intros. rewrite nextblock_store; auto.
 Qed.
 
-Lemma load_contents_init:
-  forall (sz: memory_size) (ofs: Z),
-  load_contents sz (fun y => Undef) ofs = Vundef.
+Lemma store_valid_block_2:
+  forall b', valid_block m2 b' -> valid_block m1 b'.
 Proof.
-  intros. destruct sz; reflexivity.
+  unfold valid_block; intros. rewrite nextblock_store in H; auto.
 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.
+Hint Resolve store_valid_block_1 store_valid_block_2: mem.
+
+Lemma store_valid_access_1:
+  forall chunk' b' ofs',
+  valid_access m1 chunk' b' ofs' -> valid_access m2 chunk' b' ofs'.
 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.  
+  intros. inv H. constructor. auto with mem. 
+  rewrite low_bound_store; auto.
+  rewrite high_bound_store; auto.
+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.
+Lemma store_valid_access_2:
+  forall chunk' b' ofs',
+  valid_access m2 chunk' b' ofs' -> valid_access m1 chunk' b' ofs'.
 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.
+  intros. inv H. constructor. auto with mem. 
+  rewrite low_bound_store in H1; auto.
+  rewrite high_bound_store in H2; auto.
 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.
+Lemma store_valid_access_3:
+  valid_access m1 chunk b ofs.
 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.
+  elim (store_inv _ _ _ _ _ _ STORE); intros. auto.
 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'.
+Hint Resolve store_valid_access_1 store_valid_access_2
+             store_valid_access_3: mem.
+
+Theorem load_store_similar:
+  forall chunk',
+  size_chunk chunk' = size_chunk chunk ->
+  load chunk' m2 b ofs = Some (Val.load_result chunk' v).
 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).
+  intros. destruct (store_inv _ _ _ _ _ _ STORE).
+  unfold load. rewrite in_bounds_true.
+  decEq. decEq. rewrite H1. unfold unchecked_store; simpl.
+  rewrite update_s. simpl.
+  replace (pred_size_chunk chunk) with (pred_size_chunk chunk').
+  apply getN_setN_same.
+  repeat rewrite size_chunk_pred in H. omega.
+  apply store_valid_access_1.
+  inv H0. constructor; auto. congruence.
 Qed.
 
-Hint Resolve store_alloc high_bound_alloc low_bound_alloc load_alloc_same
-load_contents_init load_alloc_other.
+Theorem load_store_same:
+  load chunk m2 b ofs = Some (Val.load_result chunk v).
+Proof.
+  eapply load_store_similar; eauto.
+Qed.
+        
+Theorem load_store_other:
+  forall chunk' b' ofs',
+  b' <> b
+  \/ ofs' + size_chunk chunk' <= ofs
+  \/ ofs + size_chunk chunk <= ofs' ->
+  load chunk' m2 b' ofs' = load chunk' m1 b' ofs'.
+Proof.
+  intros. destruct (store_inv _ _ _ _ _ _ STORE).
+  unfold load. destruct (in_bounds m1 chunk' b' ofs').
+  rewrite in_bounds_true. decEq. decEq. 
+  rewrite H1; unfold unchecked_store; simpl.
+  unfold update. destruct (zeq b' b). subst b'.
+  simpl. repeat rewrite size_chunk_pred in H.
+  apply getN_setN_other. elim H; intro. congruence. omega.
+  auto.
+  eauto with mem.
+  destruct (in_bounds m2 chunk' b' ofs'); auto.
+  elim n. eauto with mem.
+Qed.
+
+Theorem load_store_overlap:
+  forall chunk' ofs' v',
+  load chunk' m2 b ofs' = Some v' ->
+  ofs' <> ofs ->
+  ofs' + size_chunk chunk' > ofs ->
+  ofs + size_chunk chunk > ofs' ->
+  v' = Vundef.
+Proof.
+  intros. destruct (store_inv _ _ _ _ _ _ STORE).
+  destruct (load_inv _ _ _ _ _ H). rewrite H6. 
+  rewrite H4. unfold unchecked_store. simpl. rewrite update_s.
+  simpl. rewrite getN_setN_overlap. 
+  destruct chunk'; reflexivity.
+  auto. rewrite size_chunk_pred in H2. omega.
+  rewrite size_chunk_pred in H1. omega.
+Qed.
+
+Theorem load_store_overlap':
+  forall chunk' ofs',
+  valid_access m1 chunk' b ofs' ->
+  ofs' <> ofs ->
+  ofs' + size_chunk chunk' > ofs ->
+  ofs + size_chunk chunk > ofs' ->
+  load chunk' m2 b ofs' = Some Vundef.
+Proof.
+  intros.
+  assert (exists v', load chunk' m2 b ofs' = Some v').
+    eauto with mem.
+  destruct H3 as [v' LOAD]. rewrite LOAD. decEq.
+  eapply load_store_overlap; eauto.
+Qed.
 
-(** ** Properties related to [free] *)
+Theorem load_store_mismatch:
+  forall chunk' v',
+  load chunk' m2 b ofs = Some v' ->
+  size_chunk chunk' <> size_chunk chunk ->
+  v' = Vundef.
+Proof.
+  intros. destruct (store_inv _ _ _ _ _ _ STORE).
+  destruct (load_inv _ _ _ _ _ H). rewrite H4. 
+  rewrite H2. unfold unchecked_store. simpl. rewrite update_s.
+  simpl. rewrite getN_setN_mismatch.
+  destruct chunk'; reflexivity.
+  repeat rewrite size_chunk_pred in H0; omega.
+Qed.
 
-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.
+Theorem load_store_mismatch':
+  forall chunk',
+  valid_access m1 chunk' b ofs ->
+  size_chunk chunk' <> size_chunk chunk ->
+  load chunk' m2 b ofs = Some Vundef.
 Proof.
-  intros. unfold free, load; simpl.
-  case (zlt b (nextblock m)).
-  repeat (rewrite update_o; auto).
-  reflexivity.
+  intros.
+  assert (exists v', load chunk' m2 b ofs = Some v').
+    eauto with mem.
+  destruct H1 as [v' LOAD]. rewrite LOAD. decEq.
+  eapply load_store_mismatch; eauto.
+Qed.
+
+Inductive load_store_cases 
+      (chunk1: memory_chunk) (b1: block) (ofs1: Z)
+      (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Set :=
+  | lsc_similar:
+      b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 = size_chunk chunk2 ->
+      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
+  | lsc_other:
+      b1 <> b2 \/ ofs2 + size_chunk chunk2 <= ofs1 \/ ofs1 + size_chunk chunk1 <= ofs2 ->
+      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
+  | lsc_overlap:
+      b1 = b2 -> ofs1 <> ofs2 -> ofs2 + size_chunk chunk2 > ofs1 -> ofs1 + size_chunk chunk1 > ofs2 ->
+      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
+  | lsc_mismatch:
+      b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 <> size_chunk chunk2 ->
+      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.
+
+Remark size_chunk_pos:
+  forall chunk1, size_chunk chunk1 > 0.
+Proof.
+  destruct chunk1; simpl; omega.
+Qed.
+
+Definition load_store_classification:
+  forall (chunk1: memory_chunk) (b1: block) (ofs1: Z)
+         (chunk2: memory_chunk) (b2: block) (ofs2: Z),
+  load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.
+Proof.
+  intros. destruct (eq_block b1 b2).
+  destruct (zeq ofs1 ofs2).
+  destruct (zeq (size_chunk chunk1) (size_chunk chunk2)).
+  apply lsc_similar; auto.
+  apply lsc_mismatch; auto.
+  destruct (zle (ofs2 + size_chunk chunk2) ofs1).
+  apply lsc_other. tauto.
+  destruct (zle (ofs1 + size_chunk chunk1) ofs2).
+  apply lsc_other. tauto.
+  apply lsc_overlap; auto.
+  apply lsc_other; tauto.
+Qed.
+
+Theorem load_store_characterization:
+  forall chunk' b' ofs',
+  valid_access m1 chunk' b' ofs' ->
+  load chunk' m2 b' ofs' =
+    match load_store_classification chunk b ofs chunk' b' ofs' with
+    | lsc_similar _ _ _ => Some (Val.load_result chunk' v)
+    | lsc_other _ => load chunk' m1 b' ofs'
+    | lsc_overlap _ _ _ _ => Some Vundef
+    | lsc_mismatch _ _ _ => Some Vundef
+    end.
+Proof.
+  intros. 
+  assert (exists v', load chunk' m2 b' ofs' = Some v') by eauto with mem.
+  destruct H0 as [v' LOAD].
+  destruct (load_store_classification chunk b ofs chunk' b' ofs').
+  subst b' ofs'. apply load_store_similar; auto.
+  apply load_store_other; intuition.
+  subst b'. rewrite LOAD. decEq.
+  eapply load_store_overlap; eauto. 
+  subst b' ofs'. rewrite LOAD. decEq.
+  eapply load_store_mismatch; eauto.
 Qed.
 
-Theorem low_bound_free:
-  forall (m: mem) (b bf: block),
-  b <> bf ->
-  low_bound (free m bf) b = low_bound m b.
+End STORE.
+
+Hint Resolve store_valid_block_1 store_valid_block_2: mem.
+Hint Resolve store_valid_access_1 store_valid_access_2
+             store_valid_access_3: mem.
+
+(** ** Properties related to [alloc]. *)
+
+Section ALLOC.
+
+Variable m1: mem.
+Variables lo hi: Z.
+Variable m2: mem.
+Variable b: block.
+Hypothesis ALLOC: alloc m1 lo hi = (m2, b).
+
+Lemma nextblock_alloc:
+  nextblock m2 = Zsucc (nextblock m1).
 Proof.
-  intros. unfold free, low_bound; simpl.
-  rewrite update_o; auto.
+  injection ALLOC; intros. rewrite <- H0; auto.
 Qed.
 
-Theorem high_bound_free:
-  forall (m: mem) (b bf: block),
-  b <> bf ->
-  high_bound (free m bf) b = high_bound m b.
+Lemma alloc_result:
+  b = nextblock m1.
 Proof.
-  intros. unfold free, high_bound; simpl.
-  rewrite update_o; auto.
+  injection ALLOC; auto.
 Qed.
-Hint Resolve load_free low_bound_free high_bound_free.
 
-(** ** Properties related to [store] *)
+Lemma valid_block_alloc:
+  forall b', valid_block m1 b' -> valid_block m2 b'.
+Proof.
+  unfold valid_block; intros. rewrite nextblock_alloc. omega.
+Qed.
 
-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.
+Lemma fresh_block_alloc:
+  ~(valid_block m1 b).
 Proof.
-  intros. generalize (store_inv _ _ _ _ _ _ H).
-  intros [A [B [C [P D]]]].
-  unfold low_bound, high_bound. tauto.
+  unfold valid_block. rewrite alloc_result. omega.
 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.
+Lemma valid_new_block:
+  valid_block m2 b.
 Proof.
-  intros until v.
-  unfold load_contents, store_contents in |- *; case sz;
-    rewrite getN_setN_same; reflexivity.
+  unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. omega.
 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).
+
+Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
+
+Lemma valid_block_alloc_inv:
+  forall b', valid_block m2 b' -> b' = b \/ valid_block m1 b'.
 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]).
+  unfold valid_block; intros. 
+  rewrite nextblock_alloc in H. rewrite alloc_result. 
+  unfold block; 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.
+Lemma low_bound_alloc:
+  forall b', low_bound m2 b' = if zeq b' b then lo else low_bound m1 b'.
 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.
+  intros. injection ALLOC; intros. rewrite <- H0; unfold low_bound; simpl.
+  unfold update. rewrite H. destruct (zeq b' b); auto.
+Qed.
 
-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.
+Lemma low_bound_alloc_same:
+  low_bound m2 b = lo.
 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.
+  rewrite low_bound_alloc. apply zeq_true. 
+Qed.
 
-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.
+Lemma low_bound_alloc_other:
+  forall b', valid_block m1 b' -> low_bound m2 b' = low_bound m1 b'.
 Proof.
-  intros.
-  destruct sz1; destruct sz2; simpl; LSCM.
-Qed.  
+  intros; rewrite low_bound_alloc.
+  apply zeq_false. eauto with mem. 
+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'.
+Lemma high_bound_alloc:
+  forall b', high_bound m2 b' = if zeq b' b then hi else high_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.
+  intros. injection ALLOC; intros. rewrite <- H0; unfold high_bound; simpl.
+  unfold update. rewrite H. destruct (zeq b' b); auto.
 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'.
+Lemma high_bound_alloc_same:
+  high_bound m2 b = hi.
 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. 
+  rewrite high_bound_alloc. apply zeq_true. 
 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.
+Lemma high_bound_alloc_other:
+  forall b', valid_block m1 b' -> high_bound m2 b' = high_bound m1 b'.
+Proof.
+  intros; rewrite high_bound_alloc.
+  apply zeq_false. eauto with mem. 
+Qed.
 
-(** * Agreement between memory blocks. *)
+Lemma valid_access_alloc_other:
+  forall chunk b' ofs,
+  valid_access m1 chunk b' ofs ->
+  valid_access m2 chunk b' ofs.
+Proof.
+  intros. inv H. constructor. auto with mem. 
+  rewrite low_bound_alloc_other; auto. 
+  rewrite high_bound_alloc_other; auto.
+Qed.
 
-(** 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). *)
+Lemma valid_access_alloc_same:
+  forall chunk ofs,
+  lo <= ofs -> ofs + size_chunk chunk <= hi ->
+  valid_access m2 chunk b ofs.
+Proof.
+  intros. constructor. auto with mem.
+  rewrite low_bound_alloc_same; auto.
+  rewrite high_bound_alloc_same; auto.
+Qed.
+
+Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
+
+Lemma valid_access_alloc_inv:
+  forall chunk b' ofs,
+  valid_access m2 chunk b' ofs ->
+  valid_access m1 chunk b' ofs \/
+  (b' = b /\ lo <= ofs /\ ofs + size_chunk chunk <= hi).
+Proof.
+  intros. inv H. 
+  elim (valid_block_alloc_inv _ H0); intro.
+  subst b'. rewrite low_bound_alloc_same in H1.
+  rewrite high_bound_alloc_same in H2. 
+  right. tauto.
+  left. constructor. auto. 
+  rewrite low_bound_alloc_other in H1; auto.
+  rewrite high_bound_alloc_other in H2; auto.
+Qed.
+
+Theorem load_alloc_unchanged:
+  forall chunk b' ofs,
+  valid_block m1 b' ->
+  load chunk m2 b' ofs = load chunk m1 b' ofs.
+Proof.
+  intros. unfold load.
+  destruct (in_bounds m2 chunk b' ofs). 
+  elim (valid_access_alloc_inv _ _ _ v). intro.
+  rewrite in_bounds_true; auto. 
+  injection ALLOC; intros. rewrite <- H2; simpl.
+  rewrite update_o. auto. rewrite H1. apply sym_not_equal. eauto with mem.
+  intros [A [B C]]. subst b'. elimtype False. eauto with mem. 
+  destruct (in_bounds m1 chunk b' ofs).
+  elim n; eauto with mem.
+  auto.
+Qed.
 
-Definition contentmap_agree (lo hi: Z) (c1 c2: contentmap) :=
-  forall (ofs: Z),
-    lo <= ofs < hi -> c1 ofs = c2 ofs.
+Theorem load_alloc_other:
+  forall chunk b' ofs v,
+  load chunk m1 b' ofs = Some v ->
+  load chunk m2 b' ofs = Some v.
+Proof.
+  intros. rewrite <- H. apply load_alloc_unchanged. eauto with mem.
+Qed.
 
-Definition block_contents_agree (lo hi: Z) (c1 c2: block_contents) :=
-  contentmap_agree lo hi c1.(contents) c2.(contents).
+Theorem load_alloc_same:
+  forall chunk ofs v,
+  load chunk m2 b ofs = Some v ->
+  v = Vundef.
+Proof.
+  intros. destruct (load_inv _ _ _ _ _ H). rewrite H1.
+  injection ALLOC; intros. rewrite <- H3; simpl. 
+  rewrite <- H2. rewrite update_s. 
+  simpl. rewrite getN_init. destruct chunk; auto.
+Qed.
+
+Theorem load_alloc_same':
+  forall chunk ofs,
+  lo <= ofs -> ofs + size_chunk chunk <= hi ->
+  load chunk m2 b ofs = Some Vundef.
+Proof.
+  intros. assert (exists v, load chunk m2 b ofs = Some v).
+    apply valid_access_load. constructor; eauto with mem.
+    rewrite low_bound_alloc_same. auto.
+    rewrite high_bound_alloc_same. auto.
+  destruct H1 as [v LOAD]. rewrite LOAD. decEq.
+  eapply load_alloc_same; eauto.
+Qed.
+
+End ALLOC.
+
+Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
+Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
+Hint Resolve load_alloc_unchanged: mem.
+
+(** ** Properties related to [free]. *)
 
-Definition block_agree (b: block) (lo hi: Z) (m1 m2: mem) :=
-  block_contents_agree lo hi
-     (m1.(blocks) b) (m2.(blocks) b).
+Section FREE.
 
-Theorem block_agree_refl:
-  forall (m: mem) (b: block) (lo hi: Z),
-  block_agree b lo hi m m.
+Variable m: mem.
+Variable bf: block.
+
+Lemma valid_block_free_1:
+  forall b, valid_block m b -> valid_block (free m bf) b.
 Proof.
-  intros. hnf. auto.
+  unfold valid_block, free; intros; simpl; 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.
+Lemma valid_block_free_2:
+  forall b, valid_block (free m bf) b -> valid_block m b.
 Proof.
-  intros. hnf. intros. symmetry. apply H. auto.
+  unfold valid_block, free; intros; simpl in *; 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.
+Hint Resolve valid_block_free_1 valid_block_free_2: mem.
+
+Lemma low_bound_free:
+  forall b, b <> bf -> low_bound (free m bf) b = low_bound m b.
 Proof.
-  intros. hnf. intros. 
-  transitivity (contents (blocks m2 b) ofs).
-  apply H; auto. apply H0; auto.
+  intros. unfold low_bound, free; simpl.
+  rewrite update_o; 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.
+Lemma high_bound_free:
+  forall b, b <> bf -> high_bound (free m bf) b = high_bound m b.
 Proof.
-  induction n; intros; simpl.
-  auto.
-  rewrite inj_S in H1.
-  rewrite H. case (c2 ofs); intros; auto. 
-  apply IHn; omega.
-  omega.
+  intros. unfold high_bound, free; simpl.
+  rewrite update_o; auto.
 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.
+Lemma low_bound_free_same:
+  forall m b, low_bound (free m b) b = 0.
 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.
+  intros. unfold low_bound; simpl. rewrite update_s. simpl; 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.
+Lemma high_bound_free_same:
+  forall m b, high_bound (free m b) b = 0.
 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.
+  intros. unfold high_bound; simpl. rewrite update_s. simpl; 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).
+Lemma valid_access_free_1:
+  forall chunk b ofs,
+  valid_access m chunk b ofs -> b <> bf ->
+  valid_access (free m bf) chunk b ofs.
 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.
+  intros. inv H. constructor. auto with mem. 
+  rewrite low_bound_free; auto. rewrite high_bound_free; 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).
+Lemma valid_access_free_2:
+  forall chunk ofs, ~(valid_access (free m bf) chunk bf ofs).
 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).  
+  intros; red; intros. inv H. 
+  unfold free, low_bound in H1; simpl in H1. rewrite update_s in H1. simpl in H1.
+  unfold free, high_bound in H2; simpl in H2. rewrite update_s in H2. simpl in H2.
+  generalize (size_chunk_pos chunk). omega.
 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).
+Hint Resolve valid_access_free_1 valid_access_free_2: mem.
+
+Lemma valid_access_free_inv:
+  forall chunk b ofs,
+  valid_access (free m bf) chunk b ofs ->
+  valid_access m chunk b ofs /\ b <> bf.
 Proof.
-  intros. unfold store_contents; case sz; apply setN_agree; auto.
+  intros. destruct (eq_block b bf). subst b.
+  elim (valid_access_free_2 _ _ H). 
+  inv H. rewrite low_bound_free in H1; auto. 
+  rewrite high_bound_free in H2; auto.
+  split; auto. constructor; auto with mem.
 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).
+Theorem load_free:
+  forall chunk b ofs,
+  b <> bf ->
+  load chunk (free m bf) b ofs = load chunk m b ofs.
 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. 
+  intros. unfold load.
+  destruct (in_bounds m chunk b ofs).
+  rewrite in_bounds_true; auto with mem. 
+  unfold free; simpl. rewrite update_o; auto. 
+  destruct (in_bounds (free m bf) chunk b ofs); auto.
+  elim n. elim (valid_access_free_inv _ _ _ v); auto.
+Qed.
+
+End FREE.
+
+(** ** Properties related to [free_list] *)
+
+Lemma valid_block_free_list_1:
+  forall bl m b, valid_block m b -> valid_block (free_list m bl) b.
+Proof.
+  induction bl; simpl; intros. auto. 
+  apply valid_block_free_1; 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).
+Lemma valid_block_free_list_2:
+  forall bl m b, valid_block (free_list m bl) b -> valid_block m b.
 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.
+  induction bl; simpl; intros. auto.
+  apply IHbl. apply valid_block_free_2 with a; 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).
+Lemma valid_access_free_list:
+  forall chunk b ofs m bl,
+  valid_access m chunk b ofs -> ~In b bl ->
+  valid_access (free_list m bl) chunk b ofs.
 Proof.
-  intros until v.
-  unfold store_contents; case sz; simpl; intros;
-  apply setN_outside_agree; auto; simpl Z_of_nat; omega.
+  induction bl; simpl; intros. auto. 
+  apply valid_access_free_1. apply IHbl. auto. intuition. intuition congruence.
 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.
+Lemma valid_access_free_list_inv:
+  forall chunk b ofs m bl,
+  valid_access (free_list m bl) chunk b ofs ->
+  ~In b bl /\ valid_access m chunk b ofs.
+Proof.
+  induction bl; simpl; intros.
+  tauto.
+  elim (valid_access_free_inv _ _ _ _ _ H); intros.
+  elim (IHbl H0); intros.
+  intuition congruence.
+Qed.
+
+(** ** Properties related to pointer validity *)
+
+Lemma valid_pointer_valid_access:
+  forall m b ofs,
+  valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs.
+Proof.
+  unfold valid_pointer; intros; split; intros.
+  destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
+  constructor. red. eapply proj_sumbool_true; eauto.
+  eapply proj_sumbool_true; eauto.
+  change (size_chunk Mint8unsigned) with 1. 
+  generalize (proj_sumbool_true _ H1). omega.
+  inv H. unfold proj_sumbool. 
+  rewrite zlt_true; auto. rewrite zle_true; auto.
+  change (size_chunk Mint8unsigned) with 1 in H2. 
+  rewrite zlt_true. auto. omega.
+Qed.
+
+Theorem valid_pointer_alloc:
+  forall (m1 m2: mem) (lo hi: Z) (b b': block) (ofs: Z), 
+  alloc m1 lo hi = (m2, b') ->
+  valid_pointer m1 b ofs = true ->
+  valid_pointer m2 b ofs = true.
+Proof.
+  intros. rewrite valid_pointer_valid_access in H0.
+  rewrite valid_pointer_valid_access.
+  eauto with mem.
+Qed.
+
+Theorem valid_pointer_store:
+  forall (chunk: memory_chunk) (m1 m2: mem) (b b': block) (ofs ofs': Z) (v: val),
+  store chunk m1 b' ofs' v = Some m2 ->
+  valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.
+Proof.
+  intros. rewrite valid_pointer_valid_access in H0.
+  rewrite valid_pointer_valid_access.
+  eauto with mem.
+Qed.
+
+(** * Generic injections between memory states. *)
+
+Section GENERIC_INJECT.
+
+Definition meminj : Set := block -> option (block * Z).
+
+Variable val_inj: meminj -> val -> val -> Prop.
+
+(*
+Hypothesis val_inj_ptr:
+  forall mi b1 ofs1 b2 ofs2,
+  val_inj mi (Vptr b1 ofs1) (Vptr b2 ofs2) <->
+  exists delta, mi b1 = Some(b2, delta) /\ ofs2 = Int.repr (Int.signed ofs1 + delta).
+*)
+
+Hypothesis val_inj_undef:
+  forall mi, val_inj mi Vundef Vundef.
+
+Definition mem_inj (mi: meminj) (m1 m2: mem) :=
+  forall chunk b1 ofs v1 b2 delta,
+  mi b1 = Some(b2, delta) ->
+  load chunk m1 b1 ofs = Some v1 ->
+  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inj mi v1 v2.
+
+Lemma valid_access_inj:
+  forall mi m1 m2 chunk b1 ofs b2 delta,
+  mi b1 = Some(b2, delta) ->
+  mem_inj mi m1 m2 ->
+  valid_access m1 chunk b1 ofs ->
+  valid_access m2 chunk b2 (ofs + delta).
 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'.
+  assert (exists v1, load chunk m1 b1 ofs = Some v1) by eauto with mem.
+  destruct H2 as [v1 LOAD1].
+  destruct (H0 _ _ _ _ _ _ H LOAD1) as [v2 [LOAD2 VCP]].
+  eauto with mem.
+Qed.
+
+Hint Resolve valid_access_inj: mem.
+
+Lemma store_unmapped_inj:
+  forall mi m1 m2 b ofs v chunk m1',
+  mem_inj mi m1 m2 ->
+  mi b = None ->
+  store chunk m1 b ofs v = Some m1' ->
+  mem_inj mi m1' m2.
+Proof.
+  intros; red; intros.
+  assert (load chunk0 m1 b1 ofs0 = Some v1).
+    rewrite <- H3; symmetry. eapply load_store_other; eauto.
+    left. congruence.
+  eapply H; eauto.
+Qed.
+
+Lemma store_outside_inj:
+  forall mi m1 m2 chunk b ofs v m2',
+  mem_inj mi m1 m2 ->
+  (forall b' delta,
+    mi b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= ofs
+    \/ ofs + size_chunk chunk <= low_bound m1 b' + delta) ->
+  store chunk m2 b ofs v = Some m2' ->
+  mem_inj mi m1 m2'.
+Proof.
+  intros; red; intros.
+  exploit H; eauto. intros [v2 [LOAD2 VINJ]].
+  exists v2; split; auto.
+  rewrite <- LOAD2. eapply load_store_other; eauto.
+  destruct (eq_block b2 b). subst b2.
+  right. generalize (H0 _ _ H2); intro.
+  assert (valid_access m1 chunk0 b1 ofs0) by eauto with mem.
+  inv H5. omega. auto.
+Qed. 
+
+Definition meminj_no_overlap (mi: meminj) (m: mem) : Prop :=
+  forall b1 b1' delta1 b2 b2' delta2,
+  b1 <> b2 ->
+  mi b1 = Some (b1', delta1) ->
+  mi b2 = Some (b2', delta2) ->
+  b1' <> b2' 
+  \/ low_bound m b1 >= high_bound m b1
+  \/ low_bound m b2 >= high_bound m b2
+  \/ high_bound m b1 + delta1 <= low_bound m b2 + delta2 
+  \/ high_bound m b2 + delta2 <= low_bound m b1 + delta1.
+
+Lemma store_mapped_inj:
+  forall mi m1 m2 b1 ofs b2 delta v1 v2 chunk m1',
+  mem_inj mi m1 m2 ->
+  meminj_no_overlap mi m1 ->
+  mi b1 = Some(b2, delta) ->
+  store chunk m1 b1 ofs v1 = Some m1' ->
+  (forall chunk', size_chunk chunk' = size_chunk chunk ->
+    val_inj mi (Val.load_result chunk' v1) (Val.load_result chunk' v2)) ->
+  exists m2',
+  store chunk m2 b2 (ofs + delta) v2 = Some m2' /\ mem_inj mi 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'.
+  intros. 
+  assert (exists m2', store chunk m2 b2 (ofs + delta) v2 = Some m2') by eauto with mem.
+  destruct H4 as [m2' STORE2].
+  exists m2'; split. auto.
+  red. intros chunk' b1' ofs' v b2' delta' CP LOAD1.
+  assert (valid_access m1 chunk' b1' ofs') by eauto with mem.
+  generalize (load_store_characterization _ _ _ _ _ _ H2 _ _ _ H4).
+  destruct (load_store_classification chunk b1 ofs chunk' b1' ofs');
+  intro.
+  (* similar *)
+  subst b1' ofs'.
+  rewrite CP in H1. inv H1.
+  rewrite LOAD1 in H5. inv H5.
+  exists (Val.load_result chunk' v2). split. 
+  eapply load_store_similar; eauto.
+  auto.
+  (* disjoint *)
+  rewrite LOAD1 in H5. 
+  destruct (H _ _ _ _ _ _ CP (sym_equal H5)) as [v2' [LOAD2 VCP]].
+  exists v2'. split; auto.
+  rewrite <- LOAD2. eapply load_store_other; eauto.
+  destruct (eq_block b1 b1'). subst b1'.
+  rewrite CP in H1; inv H1. 
+  right. elim o; [congruence | omega].
+  assert (valid_access m1 chunk b1 ofs) by eauto with mem.
+  generalize (H0 _ _ _ _ _ _ n H1 CP). intros [A | [A | [A | A]]].
+  auto.
+  inv H6. generalize (size_chunk_pos chunk). intro. omegaContradiction.
+  inv H4. generalize (size_chunk_pos chunk'). intro. omegaContradiction.
+  right. inv H4. inv H6. omega. 
+  (* overlapping *)
+  subst b1'. rewrite CP in H1; inv H1. 
+  assert (exists v2', load chunk' m2' b2 (ofs' + delta) = Some v2') by eauto with mem.
+  destruct H1 as [v2' LOAD2'].
+  assert (v2' = Vundef). eapply load_store_overlap; eauto. 
+    omega. omega. omega.
+  exists v2'; split. auto. 
+  replace v with Vundef by congruence. subst v2'. apply val_inj_undef.
+  (* mismatch *)
+  subst b1' ofs'. rewrite CP in H1; inv H1. 
+  assert (exists v2', load chunk' m2' b2 (ofs + delta) = Some v2') by eauto with mem.
+  destruct H1 as [v2' LOAD2'].
+  assert (v2' = Vundef). eapply load_store_mismatch; eauto. 
+  exists v2'; split. auto. 
+  replace v with Vundef by congruence. subst v2'. apply val_inj_undef.
+Qed.
+
+Lemma alloc_parallel_inj:
+  forall mi m1 m2 lo1 hi1 m1' b1 lo2 hi2 m2' b2 delta,
+  mem_inj mi m1 m2 ->
+  alloc m1 lo1 hi1 = (m1', b1) ->
+  alloc m2 lo2 hi2 = (m2', b2) ->
+  mi b1 = Some(b2, delta) ->
+  lo2 <= lo1 + delta -> hi1 + delta <= hi2 ->
+  mem_inj mi m1' m2'.
+Proof.
+  intros; red; intros.
+  exploit (valid_access_alloc_inv m1); eauto with mem.
+  intros [A | [A [B C]]].
+  assert (load chunk m1 b0 ofs = Some v1).
+    rewrite <- H6. symmetry. eapply load_alloc_unchanged; eauto with mem.
+  exploit H; eauto. intros [v2 [LOAD2 VINJ]]. 
+  exists v2; split.
+    rewrite <- LOAD2. eapply load_alloc_unchanged; eauto with mem.
+  auto.
+  subst b0. rewrite H2 in H5. inversion H5. subst b3 delta0.
+  assert (v1 = Vundef). eapply load_alloc_same with (m1 := m1); eauto.
+  subst v1.
+  assert (exists v2, load chunk m2' b2 (ofs + delta) = Some v2).
+    apply valid_access_load.
+    eapply valid_access_alloc_same; eauto. omega. omega. 
+  destruct H7 as [v2 LOAD2]. 
+  assert (v2 = Vundef). eapply load_alloc_same with (m1 := m2); eauto.
+  subst v2.
+  exists Vundef; split. auto. apply val_inj_undef.
+Qed.
+
+Lemma alloc_right_inj:
+  forall mi m1 m2 lo hi b2 m2',
+  mem_inj mi m1 m2 ->
+  alloc m2 lo hi = (m2', b2) ->
+  mem_inj mi 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.
+  intros; red; intros.
+  exploit H; eauto. intros [v2 [LOAD2 VINJ]].
+  exists v2; split; auto.
+  assert (valid_block m2 b0).
+    apply valid_access_valid_block with chunk (ofs + delta). 
+    eauto with mem. 
+  rewrite <- LOAD2. eapply load_alloc_unchanged; eauto.
+Qed.
+
+Hypothesis val_inj_undef_any:
+  forall mi v, val_inj mi Vundef v.
+
+Lemma alloc_left_unmapped_inj:
+  forall mi m1 m2 lo hi b1 m1',
+  mem_inj mi m1 m2 ->
+  alloc m1 lo hi = (m1', b1) ->
+  mi b1 = None ->
+  mem_inj mi m1' m2.
+Proof.
+  intros; red; intros.
+  exploit (valid_access_alloc_inv m1); eauto with mem.
+  intros [A | [A [B C]]].
+  eapply H; eauto. 
+  rewrite <- H3. symmetry. eapply load_alloc_unchanged; eauto with mem.
+  subst b0. congruence.
+Qed.
+
+Lemma alloc_left_mapped_inj:
+  forall mi m1 m2 lo hi b1 m1' b2 delta,
+  mem_inj mi m1 m2 ->
+  alloc m1 lo hi = (m1', b1) ->
+  mi b1 = Some(b2, delta) ->
+  valid_block m2 b2 ->
+  low_bound m2 b2 <= lo + delta -> hi + delta <= high_bound m2 b2 ->
+  mem_inj mi m1' m2.
+Proof.
+  intros; red; intros.
+  exploit (valid_access_alloc_inv m1); eauto with mem.
+  intros [A | [A [B C]]].
+  eapply H; eauto. 
+  rewrite <- H6. symmetry. eapply load_alloc_unchanged; eauto with mem.
+  subst b0. rewrite H1 in H5. inversion H5. subst b3 delta0.
+  assert (v1 = Vundef). eapply load_alloc_same with (m1 := m1); eauto.
+  subst v1.
+  assert (exists v2, load chunk m2 b2 (ofs + delta) = Some v2).
+    apply valid_access_load. constructor. auto. omega. omega.
+  destruct H7 as [v2 LOAD2]. exists v2; split. auto.
+  apply val_inj_undef_any.
+Qed.
+
+Lemma free_parallel_inj:
+  forall mi m1 m2 b1 b2 delta,
+  mem_inj mi m1 m2 ->
+  mi b1 = Some(b2, delta) ->
+  (forall b delta', mi b = Some(b2, delta') -> b = b1) ->
+  mem_inj mi (free m1 b1) (free m2 b2).
+Proof.
+  intros; red; intros.
+  exploit valid_access_free_inv; eauto with mem. intros [A B].
+  assert (load chunk m1 b0 ofs = Some v1).
+    rewrite <- H3. symmetry. apply load_free. auto.
+  exploit H; eauto. intros [v2 [LOAD2 INJ]].
+  exists v2; split. 
+    rewrite <- LOAD2. apply load_free.
+    red; intro; subst b3. elim B. eauto. 
+  auto.
 Qed.
 
-(** * Store extensions *)
+Lemma free_left_inj:
+  forall mi m1 m2 b1,
+  mem_inj mi m1 m2 ->
+  mem_inj mi (free m1 b1) m2.
+Proof.
+  intros; red; intros.
+  exploit valid_access_free_inv; eauto with mem. intros [A B].
+  eapply H; eauto with mem. 
+  rewrite <- H1; symmetry; eapply load_free; eauto.
+Qed.
+
+Lemma free_list_left_inj:
+  forall mi bl m1 m2,
+  mem_inj mi m1 m2 ->
+  mem_inj mi (free_list m1 bl) m2.
+Proof.
+  induction bl; intros; simpl.
+  auto.
+  apply free_left_inj. auto.
+Qed.
+
+Lemma free_right_inj:
+  forall mi m1 m2 b2,
+  mem_inj mi m1 m2 ->
+  (forall b1 delta chunk ofs, 
+   mi b1 = Some(b2, delta) -> ~(valid_access m1 chunk b1 ofs)) ->
+  mem_inj mi m1 (free m2 b2).
+Proof.
+  intros; red; intros.
+  assert (b0 <> b2).
+    red; intro; subst b0. elim (H0 b1 delta chunk ofs H1).
+    eauto with mem.
+  exploit H; eauto. intros [v2 [LOAD2 INJ]].
+  exists v2; split; auto. 
+  rewrite <- LOAD2. apply load_free. auto.
+Qed.
+
+Lemma valid_pointer_inj:
+  forall mi m1 m2 b1 ofs b2 delta,
+  mi b1 = Some(b2, delta) ->
+  mem_inj mi m1 m2 ->
+  valid_pointer m1 b1 ofs = true ->
+  valid_pointer m2 b2 (ofs + delta) = true.
+Proof.
+  intros. rewrite valid_pointer_valid_access in H1.
+  rewrite valid_pointer_valid_access. eauto with mem.
+Qed.
+
+End GENERIC_INJECT.
+
+(** ** 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]. *)
+  same contents for block offsets that are valid in [m1]. *)
 
-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 inject_id : meminj := fun b => Some(b, 0).
+
+Definition val_inj_id (mi: meminj) (v1 v2: val) : Prop := v1 = v2.
 
 Definition extends (m1 m2: mem) :=
-  m1.(nextblock) = m2.(nextblock) /\
-  forall (b: block),
-  b < m1.(nextblock) ->
-  block_contents_extends (m1.(blocks) b) (m2.(blocks) b).
+  nextblock m1 = nextblock m2 /\ mem_inj val_inj_id inject_id m1 m2.
 
 Theorem extends_refl:
   forall (m: mem), extends m m.
 Proof.
-  intro. red. split.
-  reflexivity.
-  intros. red. 
-  split. omega. split. omega. 
-  red. intros. reflexivity.
+  intros; split. auto. 
+  red; unfold inject_id; intros. inv H.
+  exists v1; split. replace (ofs + 0) with ofs by omega. auto.
+  unfold val_inj_id; auto.
 Qed.
 
 Theorem alloc_extends:
@@ -1293,16 +1519,18 @@ Theorem alloc_extends:
   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.
+  intros. destruct H.
+  assert (b1 = b2).
+    transitivity (nextblock m1). eapply alloc_result; eauto.
+    symmetry. rewrite H. eapply alloc_result; eauto.
+  subst b2. split. auto. split. 
+  rewrite (nextblock_alloc _ _ _ _ _ H2). 
+  rewrite (nextblock_alloc _ _ _ _ _ H3).
+  congruence.
+  eapply alloc_parallel_inj; eauto. 
+    unfold val_inj_id; auto.
+    unfold inject_id; eauto.
+    omega. omega.
 Qed.
 
 Theorem free_extends:
@@ -1310,16 +1538,11 @@ Theorem free_extends:
   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.  
+  intros. destruct H. split. 
+  simpl; auto.
+  eapply free_parallel_inj; eauto. 
+  unfold inject_id. eauto.
+  unfold inject_id; intros. congruence.
 Qed.
 
 Theorem load_extends:
@@ -1328,18 +1551,10 @@ Theorem load_extends:
   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. 
+  intros. destruct H. 
+  exploit H1; eauto. unfold inject_id. eauto. 
+  unfold val_inj_id. intros [v2 [LOAD EQ]].
+  replace (ofs + 0) with ofs in LOAD by omega. congruence.
 Qed.
 
 Theorem store_within_extends:
@@ -1348,24 +1563,21 @@ Theorem store_within_extends:
   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.
+  intros. destruct H. 
+  exploit store_mapped_inj; eauto. 
+  unfold val_inj_id; eauto.
+  unfold meminj_no_overlap, inject_id; intros.
+    inv H3. inv H4. auto.
+  unfold inject_id; eauto.
+  unfold val_inj_id; intros. eauto.
+  intros [m2' [STORE MINJ]].
+  exists m2'; split.
+  replace (ofs + 0) with ofs in STORE by omega. 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.
+  rewrite (nextblock_store _ _ _ _ _ _ H0).
+  rewrite (nextblock_store _ _ _ _ _ _ STORE).
+  auto.
+  auto.
 Qed.
 
 Theorem store_outside_extends:
@@ -1375,59 +1587,147 @@ Theorem store_outside_extends:
   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. 
+  intros. destruct H. split. 
+  rewrite (nextblock_store _ _ _ _ _ _ H1). auto.
+  eapply store_outside_inj; eauto. 
+  unfold inject_id; intros. inv H3. omega.
+Qed.
+
+Theorem valid_pointer_extends:
+  forall m1 m2 b ofs,
+  extends m1 m2 -> valid_pointer m1 b ofs = true ->
+  valid_pointer m2 b ofs = true.
+Proof.
+  intros. destruct H. 
+  replace ofs with (ofs + 0) by omega.
+  apply valid_pointer_inj with val_inj_id inject_id m1 b; auto.
+Qed.
+
+(** * The ``less defined than'' relation over memory states *)
+
+(** A memory state [m1] is less defined than [m2] if, for all addresses,
+  the value [v1] read in [m1] at this address is less defined than
+  the value [v2] read in [m2], that is, either [v1 = v2] or [v1 = Vundef]. *)
+
+Definition val_inj_lessdef (mi: meminj) (v1 v2: val) : Prop :=
+  Val.lessdef v1 v2.
+
+Definition lessdef (m1 m2: mem) : Prop :=
+  nextblock m1 = nextblock m2 /\
+  mem_inj val_inj_lessdef inject_id m1 m2.
+
+Lemma lessdef_refl:
+  forall m, lessdef m m.
+Proof.
+  intros; split. auto.
+  red; intros. unfold inject_id in H. inv H. 
+  exists v1; split. replace (ofs + 0) with ofs by omega. auto.
+  red. constructor.
+Qed.
+
+Lemma load_lessdef:
+  forall m1 m2 chunk b ofs v1,
+  lessdef m1 m2 -> load chunk m1 b ofs = Some v1 ->
+  exists v2, load chunk m2 b ofs = Some v2 /\ Val.lessdef v1 v2.
+Proof.
+  intros. destruct H.
+  exploit H1; eauto. unfold inject_id. eauto.
+  intros [v2 [LOAD INJ]]. exists v2; split.
+  replace ofs with (ofs + 0) by omega. auto.
+  auto.
+Qed.
+
+Lemma loadv_lessdef:
+  forall m1 m2 chunk addr1 addr2 v1,
+  lessdef m1 m2 -> Val.lessdef addr1 addr2 ->
+  loadv chunk m1 addr1 = Some v1 ->
+  exists v2, loadv chunk m2 addr2 = Some v2 /\ Val.lessdef v1 v2.
+Proof.
+  intros. inv H0.  
+  destruct addr2; simpl in *; try discriminate.
+  eapply load_lessdef; eauto.
+  simpl in H1; discriminate.
+Qed.
+
+Lemma store_lessdef:
+  forall m1 m2 chunk b ofs v1 v2 m1',
+  lessdef m1 m2 -> Val.lessdef v1 v2 ->
+  store chunk m1 b ofs v1 = Some m1' ->
+  exists m2', store chunk m2 b ofs v2 = Some m2' /\ lessdef m1' m2'.
+Proof.
+  intros. destruct H. 
+  exploit store_mapped_inj; eauto.
+    unfold val_inj_lessdef; intros; constructor.
+    red; unfold inject_id; intros. inv H4. inv H5. auto.
+    unfold inject_id; eauto.
+    unfold val_inj_lessdef; intros.
+    apply Val.load_result_lessdef. eexact H0.
+  intros [m2' [STORE MINJ]].
+  exists m2'; split. replace ofs with (ofs + 0) by omega. auto.
+  split. 
+  rewrite (nextblock_store _ _ _ _ _ _ H1).
+  rewrite (nextblock_store _ _ _ _ _ _ STORE).
+  auto.
+  auto.
+Qed.
+
+Lemma storev_lessdef:
+  forall m1 m2 chunk addr1 v1 addr2 v2 m1',
+  lessdef m1 m2 -> Val.lessdef addr1 addr2 -> Val.lessdef v1 v2 ->
+  storev chunk m1 addr1 v1 = Some m1' ->
+  exists m2', storev chunk m2 addr2 v2 = Some m2' /\ lessdef m1' m2'.
+Proof.
+  intros. inv H0.  
+  destruct addr2; simpl in H2; try discriminate.
+  simpl. eapply store_lessdef; eauto.
+  discriminate.
+Qed. 
+
+Lemma alloc_lessdef:
+  forall m1 m2 lo hi b1 m1' b2 m2',
+  lessdef m1 m2 -> alloc m1 lo hi = (m1', b1) -> alloc m2 lo hi = (m2', b2) ->
+  b1 = b2 /\ lessdef m1' m2'.
+Proof.
+  intros. destruct H.
+  assert (b1 = b2).
+    transitivity (nextblock m1). eapply alloc_result; eauto.
+    symmetry. rewrite H. eapply alloc_result; eauto.
+  subst b2. split. auto. split. 
+  rewrite (nextblock_alloc _ _ _ _ _ H0). 
+  rewrite (nextblock_alloc _ _ _ _ _ H1).
   congruence.
+  eapply alloc_parallel_inj; eauto. 
+    unfold val_inj_lessdef; auto.
+    unfold inject_id; eauto.
+    omega. omega.
 Qed.
 
-(** * Store injections *)
+Lemma free_lessdef:
+  forall m1 m2 b, lessdef m1 m2 -> lessdef (free m1 b) (free m2 b).
+Proof.
+  intros. destruct H. split.
+  simpl; auto.
+  eapply free_parallel_inj; eauto.
+  unfold inject_id. eauto.
+  unfold inject_id; intros. congruence.
+Qed.
+
+Lemma valid_block_lessdef:
+  forall m1 m2 b, lessdef m1 m2 -> valid_block m1 b -> valid_block m2 b.
+Proof.
+  unfold valid_block. intros. destruct H. rewrite <- H; auto.
+Qed.
+
+Lemma valid_pointer_lessdef:
+  forall m1 m2 b ofs,
+  lessdef m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.
+Proof.
+  intros. destruct H.
+  replace ofs with (ofs + 0) by omega.
+  apply valid_pointer_inj with val_inj_lessdef inject_id m1 b; auto.
+Qed.
+
+(** ** Memory 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
@@ -1437,718 +1737,358 @@ Qed.
   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 :=
+Inductive val_inject (mi: meminj): val -> val -> Prop :=
   | val_inject_int:
-      forall i, val_inject (Vint i) (Vint i)
+      forall i, val_inject mi (Vint i) (Vint i)
   | val_inject_float:
-      forall f, val_inject (Vfloat f) (Vfloat f)
+      forall f, val_inject mi (Vfloat f) (Vfloat f)
   | val_inject_ptr:
       forall b1 ofs1 b2 ofs2 x,
-      f b1 = Some (b2, x) ->
+      mi b1 = Some (b2, x) ->
       ofs2 = Int.add ofs1 (Int.repr x) ->
-      val_inject (Vptr b1 ofs1) (Vptr b2 ofs2)
+      val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)
   | val_inject_undef: forall v,
-      val_inject Vundef v.
+      val_inject mi Vundef v.
 
 Hint Resolve val_inject_int val_inject_float val_inject_ptr 
-val_inject_undef.
+             val_inject_undef.
 
-Inductive val_list_inject: list val -> list val-> Prop:= 
+Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= 
   | val_nil_inject :
-      val_list_inject nil nil
+      val_list_inject mi 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).
+      val_inject mi v v' -> val_list_inject mi vl vl'->
+      val_list_inject mi (v :: vl) (v' :: vl').  
 
-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
-  }.
+Hint Resolve val_nil_inject val_cons_inject.
 
 (** A memory state [m1] injects into another memory state [m2] via the
   memory injection [f] if the following conditions hold:
+- loads in [m1] must have matching loads in [m2] in the sense
+  of the [mem_inj] predicate;
 - 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].
+- if [f b = Some(b', delta)], [b'] must be valid in [m2];
+- distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2];
+- the sizes of [m2]'s blocks are representable with signed machine integers;
+- the offsets [delta] are representable with signed machine integers.
 *)
 
-Record mem_inject (m1 m2: mem) : Prop :=
+Record mem_inject (f: meminj) (m1 m2: mem) : Prop :=
   mk_mem_inject {
+    mi_inj:
+      mem_inj val_inject f m1 m2;
     mi_freeblocks:
-      forall b, b >= m1.(nextblock) -> f b = None;
+      forall b, ~(valid_block m1 b) -> f b = None;
     mi_mappedblocks:
+      forall b b' delta, f b = Some(b', delta) -> valid_block m2 b';
+    mi_no_overlap:
+      meminj_no_overlap f m1;
+    mi_range_1:
       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)
- }.
+      Int.min_signed <= delta <= Int.max_signed;
+    mi_range_2:
+      forall b b' delta,
+      f b = Some(b', delta) ->
+      delta = 0 \/ (Int.min_signed <= low_bound m2 b' /\ high_bound m2 b' <= Int.max_signed)
+  }.
+
 
 (** 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.
+  forall f m1 m2 chunk b1 ofs1 b2 delta,
+  mem_inject f m1 m2 ->
+  valid_access m1 chunk b1 (Int.signed ofs1) ->
+  f b1 = Some (b2, delta) ->
+  Int.signed (Int.add ofs1 (Int.repr delta)) = Int.signed ofs1 + delta.
 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.
+  intros. inversion H.
+  elim (mi_range_4 _ _ _ H1); intro.
+  (* delta = 0 *)
+  subst delta. change (Int.repr 0) with Int.zero.
+  rewrite Int.add_zero. omega.
+  (* delta <> 0 *)
+  rewrite Int.add_signed.
+  repeat rewrite Int.signed_repr. auto.
+  eauto.
+  assert (valid_access m2 chunk b2 (Int.signed ofs1 + delta)).
+    eapply valid_access_inj; eauto.
+  inv H3. generalize (size_chunk_pos chunk); omega.
+  eauto.
 Qed.
 
 Lemma valid_pointer_inject_no_overflow:
-  forall m1 m2 b ofs b' x,
-  mem_inject m1 m2 ->
+  forall f m1 m2 b ofs b' x,
+  mem_inject f 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. 
+  intros. inv H. rewrite valid_pointer_valid_access in H0.
+  assert (valid_access m2 Mint8unsigned b' (Int.signed ofs + x)).
+    eapply valid_access_inj; eauto.
+  inv H. change (size_chunk Mint8unsigned) with 1 in H4.
+  rewrite Int.signed_repr; eauto.
+  exploit mi_range_4; eauto. intros [A | [A B]].
+  subst x. rewrite Zplus_0_r. apply Int.signed_range.
   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).
+Lemma valid_pointer_inject:
+  forall f m1 m2 b ofs b' ofs',
+  mem_inject f m1 m2 ->
+  valid_pointer m1 b (Int.signed ofs) = true ->
+  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  valid_pointer m2 b' (Int.signed ofs') = true.
 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. 
+  intros. inv H1. 
+  exploit valid_pointer_inject_no_overflow; eauto. intro NOOV.
+  inv H. rewrite Int.add_signed. rewrite Int.signed_repr; auto.
+  rewrite Int.signed_repr; eauto.
+  eapply valid_pointer_inj; eauto.
 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.
+(** Relation between injections and loads. *)
 
 Lemma load_inject:
-  forall m1 m2 chunk b1 ofs b2 delta v1,
-  mem_inject m1 m2 ->
+  forall f m1 m2 chunk b1 ofs b2 delta v1,
+  mem_inject f 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.
+  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f 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.
+  intros. inversion H.
+  eapply mi_inj0; eauto. 
 Qed.
 
 Lemma loadv_inject:
-  forall m1 m2 chunk a1 a2 v1,
-  mem_inject m1 m2 ->
+  forall f m1 m2 chunk a1 a2 v1,
+  mem_inject f m1 m2 ->
   loadv chunk m1 a1 = Some v1 ->
-  val_inject a1 a2 ->
-  exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject v1 v2.
+  val_inject f a1 a2 ->
+  exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f 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.
+  intros. inv H1; simpl in H0; try discriminate.
+  exploit load_inject; eauto. intros [v2 [LOAD INJ]].
+  exists v2; split; auto. simpl.
+  replace (Int.signed (Int.add ofs1 (Int.repr x)))
+     with (Int.signed ofs1 + x).
+  auto. symmetry. eapply address_inject; eauto with mem.
 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.
+Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop :=
+  | val_content_inject_base:
+      forall chunk v1 v2,
+      val_inject f v1 v2 ->
+      val_content_inject f chunk v1 v2
+  | val_content_inject_8:
+      forall chunk n1 n2,
+      chunk = Mint8unsigned \/ chunk = Mint8signed ->
+      Int.cast8unsigned n1 = Int.cast8unsigned n2 ->
+      val_content_inject f chunk (Vint n1) (Vint n2)
+  | val_content_inject_16:
+      forall chunk n1 n2,
+      chunk = Mint16unsigned \/ chunk = Mint16signed ->
+      Int.cast16unsigned n1 = Int.cast16unsigned n2 ->
+      val_content_inject f chunk (Vint n1) (Vint n2)
+  | val_content_inject_32:
+      forall f1 f2,
+      Float.singleoffloat f1 = Float.singleoffloat f2 ->
+      val_content_inject f Mfloat32 (Vfloat f1) (Vfloat f2).
 
-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.
+Hint Resolve val_content_inject_base.
 
-Lemma store_mapped_inject_1:
-  forall chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
-  mem_inject m1 m2 ->
+Lemma load_result_inject:
+  forall f chunk v1 v2 chunk',
+  val_content_inject f chunk v1 v2 ->
+  size_chunk chunk = size_chunk chunk' ->
+  val_inject f (Val.load_result chunk' v1) (Val.load_result chunk' v2).
+Proof.
+  intros. inv H; simpl.
+  inv H1; destruct chunk'; simpl; econstructor; eauto.
+
+  elim H1; intro; subst chunk;
+  destruct chunk'; simpl in H0; try discriminate; simpl.
+  replace (Int.cast8signed n1) with (Int.cast8signed n2).
+  constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto.
+  rewrite H2. constructor.
+  replace (Int.cast8signed n1) with (Int.cast8signed n2).
+  constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto.
+  rewrite H2. constructor.
+
+  elim H1; intro; subst chunk;
+  destruct chunk'; simpl in H0; try discriminate; simpl.
+  replace (Int.cast16signed n1) with (Int.cast16signed n2).
+  constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto.
+  rewrite H2. constructor.
+  replace (Int.cast16signed n1) with (Int.cast16signed n2).
+  constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto.
+  rewrite H2. constructor.
+
+  destruct chunk'; simpl in H0; try discriminate; simpl.
+  constructor. rewrite H1; constructor.
+Qed.
+
+Lemma store_mapped_inject_1 :
+  forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
+  mem_inject f m1 m2 ->
   store chunk m1 b1 ofs v1 = Some n1 ->
   f b1 = Some (b2, delta) ->
-  val_content_inject (mem_chunk chunk) v1 v2 ->
+  val_content_inject f 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.
+    /\ mem_inject f n1 n2.
+Proof.
+  intros. inversion H. 
+  exploit store_mapped_inj; eauto.
+  intros; constructor.
+  intros. apply load_result_inject with chunk; eauto.
+  intros [n2 [STORE MINJ]].
+  exists n2; split. auto. constructor.
+  (* inj *)
+  auto.
+  (* freeblocks *)
+  intros. apply mi_freeblocks0. red; intro. elim H3. eauto with mem.
+  (* mappedblocks *)
+  intros. eauto with mem.
+  (* no_overlap *)
+  red; intros.
+  repeat rewrite (low_bound_store _ _ _ _ _ _ H0).
+  repeat rewrite (high_bound_store _ _ _ _ _ _ H0).
+  eapply mi_no_overlap0; eauto.
+  (* range *)
+  auto.
+  intros. 
+  repeat rewrite (low_bound_store _ _ _ _ _ _ STORE).
+  repeat rewrite (high_bound_store _ _ _ _ _ _ STORE).
+  eapply mi_range_4; eauto.
 Qed.
 
 Lemma store_mapped_inject:
-  forall chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
-  mem_inject m1 m2 ->
+  forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
+  mem_inject f m1 m2 ->
   store chunk m1 b1 ofs v1 = Some n1 ->
   f b1 = Some (b2, delta) ->
-  val_inject v1 v2 ->
+  val_inject f v1 v2 ->
   exists n2,
     store chunk m2 b2 (ofs + delta) v2 = Some n2
-    /\ mem_inject n1 n2.
+    /\ mem_inject f 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 ->
+  forall f chunk m1 b1 ofs v1 n1 m2,
+  mem_inject f 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.
+  mem_inject f n1 m2.
+Proof.
+  intros. inversion H.
+  constructor.
+  (* inj *)
+  eapply store_unmapped_inj; eauto.
+  (* freeblocks *)
+  intros. apply mi_freeblocks0. red; intros; elim H2; eauto with mem.
+  (* mappedblocks *)
+  intros. eapply mi_mappedblocks0; eauto with mem.
+  (* no_overlap *)
+  red; intros.
+  repeat rewrite (low_bound_store _ _ _ _ _ _ H0).
+  repeat rewrite (high_bound_store _ _ _ _ _ _ H0).
+  eapply mi_no_overlap0; eauto.
+  (* range *)
+  auto. auto.
 Qed.
 
 Lemma storev_mapped_inject_1:
-  forall chunk m1 a1 v1 n1 m2 a2 v2,
-  mem_inject m1 m2 ->
+  forall f chunk m1 a1 v1 n1 m2 a2 v2,
+  mem_inject f m1 m2 ->
   storev chunk m1 a1 v1 = Some n1 ->
-  val_inject a1 a2 ->
-  val_content_inject (mem_chunk chunk) v1 v2 ->
+  val_inject f a1 a2 ->
+  val_content_inject f chunk v1 v2 ->
   exists n2,
-    storev chunk m2 a2 v2 = Some n2 /\ mem_inject n1 n2.
+    storev chunk m2 a2 v2 = Some n2 /\ mem_inject f 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).
+  intros. inv H1; simpl in H0; try discriminate.
+  simpl. replace (Int.signed (Int.add ofs1 (Int.repr x)))
+            with (Int.signed ofs1 + 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.
+  symmetry. eapply address_inject; eauto with mem.
 Qed.
 
 Lemma storev_mapped_inject:
-  forall chunk m1 a1 v1 n1 m2 a2 v2,
-  mem_inject m1 m2 ->
+  forall f chunk m1 a1 v1 n1 m2 a2 v2,
+  mem_inject f m1 m2 ->
   storev chunk m1 a1 v1 = Some n1 ->
-  val_inject a1 a2 ->
-  val_inject v1 v2 ->
+  val_inject f a1 a2 ->
+  val_inject f v1 v2 ->
   exists n2,
-    storev chunk m2 a2 v2 = Some n2 /\ mem_inject n1 n2.
+    storev chunk m2 a2 v2 = Some n2 /\ mem_inject f 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.
+Lemma meminj_no_overlap_free:
+  forall mi m b,
+  meminj_no_overlap mi m ->
+  meminj_no_overlap mi (free m b).
 Proof.
-  intros.  unfold free in H.
-  rewrite<- H . unfold low_bound , high_bound .
-  simpl . rewrite update_s. simpl.  omega.  
+  intros; red; intros.
+  assert (low_bound (free m b) b >= high_bound (free m b) b).
+    rewrite low_bound_free_same; rewrite high_bound_free_same; auto.
+    omega.
+  destruct (eq_block b1 b); destruct (eq_block b2 b); subst; auto.
+  repeat (rewrite low_bound_free; auto). 
+  repeat (rewrite high_bound_free; auto).
 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).
+Lemma meminj_no_overlap_free_list:
+  forall mi m bl,
+  meminj_no_overlap mi m ->
+  meminj_no_overlap mi (free_list m bl).
 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.       
+  induction bl; simpl; intros. auto.
+  apply meminj_no_overlap_free. auto.
+Qed.
 
 Lemma free_inject:
-  forall m1 m2 l b,
+  forall f 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 IHid. omega. simpl size_init_data 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.
+  mem_inject f m1 m2 ->
+  mem_inject f (free_list m1 l) (free m2 b).
+Proof.
+  intros. inversion H0. constructor.
+  (* inj *)
+  apply free_right_inj. apply free_list_left_inj. auto.
+  intros; red; intros. 
+  elim (valid_access_free_list_inv _ _ _ _ _ H2); intros.
+  elim H3; eauto.
+  (* freeblocks *)
+  intros. apply mi_freeblocks0. red; intro; elim H1.
+  apply valid_block_free_list_1; auto.
+  (* mappedblocks *)
+  intros. apply valid_block_free_1. eauto. 
+  (* overlap *)
+  apply meminj_no_overlap_free_list; auto.
+  (* range *)
+  auto.
+  intros. destruct (eq_block b' b). subst b'.
+  rewrite low_bound_free_same; rewrite high_bound_free_same. 
+  right; compute; intuition congruence.
+  rewrite low_bound_free; auto. rewrite high_bound_free; auto.
+  eauto.
+Qed.
 
 (** Monotonicity properties of memory injections. *)
 
@@ -2160,16 +2100,11 @@ Lemma inject_incr_refl :
 Proof. unfold inject_incr . intros. left . auto . Qed.
 
 Lemma inject_incr_trans :
-  forall f1 f2 f3  , 
+  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 .
+  unfold inject_incr; intros.
+  generalize (H b); generalize (H0 b); intuition congruence.
 Qed.
 
 Lemma val_inject_incr:
@@ -2192,61 +2127,17 @@ Lemma val_list_inject_incr:
   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.
+  induction vl; intros; inv H0. auto.
+  constructor. eapply val_inject_incr; eauto. 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.
+Hint Resolve inject_incr_refl val_inject_incr val_list_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'.
+  fun (b': block) => if zeq b' b then x else f b'.
 
 Lemma extend_inject_incr:
   forall f b x,
@@ -2254,7 +2145,7 @@ Lemma extend_inject_incr:
   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.
+  destruct (zeq b0 b). subst b0; auto. auto.
 Qed.
 
 Lemma alloc_right_inject:
@@ -2263,14 +2154,17 @@ Lemma alloc_right_inject:
   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.
+  intros. inversion H. constructor.
+  eapply alloc_right_inj; eauto.
+  auto.
+  intros. eauto with mem. 
+  auto.
+  auto.
+  intros. replace (low_bound m2' b') with (low_bound m2 b').
+  replace (high_bound m2' b') with (high_bound m2 b').
+  eauto. 
+  symmetry. eapply high_bound_alloc_other; eauto. 
+  symmetry. eapply low_bound_alloc_other; eauto.
 Qed.
 
 Lemma alloc_unmapped_inject:
@@ -2280,26 +2174,36 @@ Lemma alloc_unmapped_inject:
   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.
+  intros. 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).
+  apply extend_inject_incr. apply mi_freeblocks0. eauto with mem.
+  split; auto. constructor.
+  (* inj *)
+  eapply alloc_left_unmapped_inj; eauto.
+  red; intros. unfold extend_inject in H2.
+  destruct (zeq b1 b). congruence.
+  exploit mi_inj0; eauto. intros [v2 [LOAD VINJ]].
+  exists v2; split. auto. 
+  apply val_inject_incr with f; auto.
+  unfold extend_inject. apply zeq_true.
+  (* freeblocks *)
+  intros. unfold extend_inject. destruct (zeq b0 b). auto.
+  apply mi_freeblocks0; red; intro. elim H2. eauto with mem.
+  (* mappedblocks *)
+  intros. unfold extend_inject in H2. destruct (zeq b0 b).
+  discriminate. eauto.
+  (* overlap *)
+  red; unfold extend_inject, update; intros.
+  repeat rewrite (low_bound_alloc _ _ _ _ _ H0).
+  repeat rewrite (high_bound_alloc _ _ _ _ _ H0).
+  destruct (zeq b1 b); try discriminate.
+  destruct (zeq b2 b); try discriminate.
+  eauto.
+  (* range *)
+  unfold extend_inject; intros.
+  destruct (zeq b0 b). discriminate. eauto.
+  unfold extend_inject; intros.
+  destruct (zeq b0 b). discriminate. eauto.
 Qed.
 
 Lemma alloc_mapped_inject:
@@ -2319,50 +2223,41 @@ Lemma alloc_mapped_inject:
   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 *)
+  intros. inversion H.
   assert (inject_incr f (extend_inject b (Some (b', ofs)) f)).
-  apply extend_inject_incr. apply mi_freeblocks0. rewrite A. omega. 
+  apply extend_inject_incr. apply mi_freeblocks0. eauto with mem.
   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.
+  (* inj *)
+  eapply alloc_left_mapped_inj; eauto.
+  red; intros. unfold extend_inject in H9.
+  rewrite zeq_false in H9.
+  exploit mi_inj0; eauto. intros [v2 [LOAD VINJ]].
+  exists v2; split. auto. eapply val_inject_incr; eauto.
+  eauto with mem. 
+  unfold extend_inject. apply zeq_true.
+  (* freeblocks *)
+  intros. unfold extend_inject. rewrite zeq_false.
+  apply mi_freeblocks0. red; intro. elim H9; eauto with mem.
+  apply sym_not_equal; eauto with mem.
+  (* mappedblocks *)
+  unfold extend_inject; intros.
+  destruct (zeq b0 b). inv H9. auto. eauto.
+  (* overlap *)
+  red; unfold extend_inject, update; intros.
+  repeat rewrite (low_bound_alloc _ _ _ _ _ H0).
+  repeat rewrite (high_bound_alloc _ _ _ _ _ H0).
+  destruct (zeq b1 b); [inv H10|idtac];
+  (destruct (zeq b2 b); [inv H11|idtac]).
+  congruence. 
+  destruct (zeq b1' b2'). subst b2'. generalize (H7 _ _ H11). tauto. auto.
+  destruct (zeq b1' b2'). subst b2'. generalize (H7 _ _ H10). tauto. auto.
+  eauto.
+  (* range *)
+  unfold extend_inject; intros. 
+  destruct (zeq b0 b). inv H9. auto. eauto.
+  unfold extend_inject; intros. 
+  destruct (zeq b0 b). inv H9. auto. eauto.
 Qed.
 
 Lemma alloc_parallel_inject:
@@ -2371,20 +2266,104 @@ Lemma alloc_parallel_inject:
   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).
+  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.
+  eauto with mem.
+  compute; intuition congruence.
+  rewrite (low_bound_alloc_same _ _ _ _ _ H1). auto.
+  rewrite (high_bound_alloc_same _ _ _ _ _ H1). auto.
+  rewrite (low_bound_alloc_same _ _ _ _ _ H1). omega.
+  rewrite (high_bound_alloc_same _ _ _ _ _ H1). omega.
+  intros. elimtype False. inv H. 
+  exploit mi_mappedblocks0; eauto.
+  change (~ valid_block m2 b2). eauto with mem.
+Qed.
+
+Definition meminj_init (m: mem) : meminj :=
+  fun (b: block) => if zlt b m.(nextblock) then Some(b, 0) else None.
+
+Definition mem_inject_neutral (m: mem) : Prop :=
+  forall f chunk b ofs v,
+  load chunk m b ofs = Some v -> val_inject f v v.
+
+Lemma init_inject:
+  forall m,
+  mem_inject_neutral m ->
+  mem_inject (meminj_init m) m m.
+Proof.
+  intros; constructor.
+  (* inj *)
+  red; intros. unfold meminj_init in H0. 
+  destruct (zlt b1 (nextblock m)); inversion H0.
+  subst b2 delta. exists v1; split.
+  rewrite Zplus_0_r. auto. eapply H; eauto.
+  (* free blocks *)
+  unfold valid_block, meminj_init; intros.
+  apply zlt_false. omega.
+  (* mapped blocks *)
+  unfold valid_block, meminj_init; intros.
+  destruct (zlt b (nextblock m)); inversion H0. subst b'; auto.
+  (* overlap *)
+  red; unfold meminj_init; intros.
+  destruct (zlt b1 (nextblock m)); inversion H1.
+  destruct (zlt b2 (nextblock m)); inversion H2.
+  left; congruence.
+  (* range *)
+  unfold meminj_init; intros.
+  destruct (zlt b (nextblock m)); inversion H0. subst delta.
+  compute; intuition congruence.
+  unfold meminj_init; intros.
+  destruct (zlt b (nextblock m)); inversion H0. subst delta.
+  auto.
+Qed.
+
+Remark getN_setN_inject:
+  forall f m v n1 p1 n2 p2,
+  val_inject f (getN n2 p2 m) (getN n2 p2 m) ->
+  val_inject f v v ->
+  val_inject f (getN n2 p2 (setN n1 p1 v m))
+               (getN n2 p2 (setN n1 p1 v m)).
+Proof.
+  intros. 
+  destruct (getN_setN_characterization m v n1 p1 n2 p2)
+  as [A | [A | A]]; rewrite A; auto.
+Qed.
+             
+Remark getN_contents_init_data_inject:
+  forall f n ofs id pos,
+  val_inject f (getN n ofs (contents_init_data pos id))
+               (getN n ofs (contents_init_data pos id)).
+Proof.
+  induction id; simpl; intros.
+  repeat rewrite getN_init. constructor.
+  destruct a; auto; apply getN_setN_inject; auto.
+Qed.
+
+Lemma alloc_init_data_neutral:
+  forall m id m' b,
+  mem_inject_neutral m ->
+  alloc_init_data m id = (m', b) ->
+  mem_inject_neutral m'.
+Proof.
+  intros. injection H0; intros A B.
+  red; intros. 
+  exploit load_inv; eauto. intros [C D].
+  rewrite <- B in D; simpl in D. rewrite A in D. 
+  unfold update in D. destruct (zeq b0 b).
+  subst b0. rewrite D. simpl. 
+  apply load_result_inject with chunk. constructor.
+  apply getN_contents_init_data_inject. auto.
+  apply H with chunk b0 ofs. unfold load.
+  rewrite in_bounds_true. congruence. 
+  inversion C. constructor.
+  generalize H2. unfold valid_block. rewrite <- B; simpl.
+  rewrite A. unfold block in n; intros. omega.
+  replace (low_bound m b0) with (low_bound m' b0). auto.
+  unfold low_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto.
+  replace (high_bound m b0) with (high_bound m' b0). auto.
+  unfold high_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto.
 Qed.
diff --git a/common/Smallstep.v b/common/Smallstep.v
new file mode 100644
index 0000000..7f6c776
--- /dev/null
+++ b/common/Smallstep.v
@@ -0,0 +1,460 @@
+(** Tools for small-step operational semantics *)
+
+(** This module defines generic operations and theorems over
+  the one-step transition relations that are used to specify
+  operational semantics in small-step style. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Events.
+Require Import Globalenvs.
+Require Import Integers.
+
+Set Implicit Arguments.
+
+(** * Closures of transitions relations *)
+
+Section CLOSURES.
+
+Variable genv: Set.
+Variable state: Set.
+
+(** A one-step transition relation has the following signature.
+  It is parameterized by a global environment, which does not
+  change during the transition.  It relates the initial state
+  of the transition with its final state.  The [trace] parameter
+  captures the observable events possibly generated during the
+  transition. *)
+
+Variable step: genv -> state -> trace -> state -> Prop.
+
+(** Zero, one or several transitions.  Also known as Kleene closure,
+    or reflexive transitive closure. *)
+
+Inductive star (ge: genv): state -> trace -> state -> Prop :=
+  | star_refl: forall s,
+      star ge s E0 s
+  | star_step: forall s1 t1 s2 t2 s3 t,
+      step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 ->
+      star ge s1 t s3.
+
+Lemma star_one:
+  forall ge s1 t s2, step ge s1 t s2 -> star ge s1 t s2.
+Proof.
+  intros. eapply star_step; eauto. apply star_refl. traceEq. 
+Qed.
+
+Lemma star_trans:
+  forall ge s1 t1 s2, star ge s1 t1 s2 ->
+  forall t2 s3 t, star ge s2 t2 s3 -> t = t1 ** t2 -> star ge s1 t s3.
+Proof.
+  induction 1; intros.
+  rewrite H0. simpl. auto.
+  eapply star_step; eauto. traceEq.
+Qed.
+
+Lemma star_left:
+  forall ge s1 t1 s2 t2 s3 t,
+  step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 ->
+  star ge s1 t s3.
+Proof star_step.
+
+Lemma star_right:
+  forall ge s1 t1 s2 t2 s3 t,
+  star ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
+  star ge s1 t s3.
+Proof.
+  intros. eapply star_trans. eauto. apply star_one. eauto. auto.
+Qed.
+
+(** One or several transitions.  Also known as the transitive closure. *)
+
+Inductive plus (ge: genv): state -> trace -> state -> Prop :=
+  | plus_left: forall s1 t1 s2 t2 s3 t,
+      step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 ->
+      plus ge s1 t s3.
+
+Lemma plus_one:
+  forall ge s1 t s2,
+  step ge s1 t s2 -> plus ge s1 t s2.
+Proof.
+  intros. econstructor; eauto. apply star_refl. traceEq.
+Qed.
+
+Lemma plus_star:
+  forall ge s1 t s2, plus ge s1 t s2 -> star ge s1 t s2.
+Proof.
+  intros. inversion H; subst.
+  eapply star_step; eauto. 
+Qed.
+
+Lemma plus_right:
+  forall ge s1 t1 s2 t2 s3 t,
+  star ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
+  plus ge s1 t s3.
+Proof.
+  intros. inversion H; subst. simpl. apply plus_one. auto.
+  rewrite Eapp_assoc. eapply plus_left; eauto.
+  eapply star_right; eauto. 
+Qed.
+
+Lemma plus_left':
+  forall ge s1 t1 s2 t2 s3 t,
+  step ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 ->
+  plus ge s1 t s3.
+Proof.
+  intros. eapply plus_left; eauto. apply plus_star; auto.
+Qed.
+
+Lemma plus_right':
+  forall ge s1 t1 s2 t2 s3 t,
+  plus ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
+  plus ge s1 t s3.
+Proof.
+  intros. eapply plus_right; eauto. apply plus_star; auto.
+Qed.
+
+Lemma plus_star_trans:
+  forall ge s1 t1 s2 t2 s3 t,
+  plus ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
+Proof.
+  intros. inversion H; subst. 
+  econstructor; eauto. eapply star_trans; eauto.
+  traceEq.
+Qed.
+
+Lemma star_plus_trans:
+  forall ge s1 t1 s2 t2 s3 t,
+  star ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
+Proof.
+  intros. inversion H; subst.
+  simpl; auto.
+  rewrite Eapp_assoc. 
+  econstructor. eauto. eapply star_trans. eauto. 
+  apply plus_star. eauto. eauto. auto.
+Qed.
+
+Lemma plus_trans:
+  forall ge s1 t1 s2 t2 s3 t,
+  plus ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
+Proof.
+  intros. eapply plus_star_trans. eauto. apply plus_star. eauto. auto.
+Qed.
+
+Lemma plus_inv:
+  forall ge s1 t s2,  plus ge s1 t s2 ->
+  step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2.
+Proof.
+  intros. inversion H; subst. inversion H1; subst.
+  left. rewrite E0_right. auto.
+  right. exists s3; exists t1; exists (t0 ** t3); split. auto.
+  split. econstructor; eauto. auto.
+Qed.
+
+(** Infinitely many transitions *)
+
+CoInductive forever (ge: genv): state -> traceinf -> Prop :=
+  | forever_intro: forall s1 t s2 T,
+      step ge s1 t s2 -> forever ge s2 T ->
+      forever ge s1 (t *** T).
+
+(** An alternate, equivalent definition of [forever] that is useful
+    for coinductive reasoning. *)
+
+CoInductive forever_N (ge: genv): nat -> state -> traceinf -> Prop :=
+  | forever_N_star: forall s1 t s2 p q T,
+      star ge s1 t s2 -> (p < q)%nat -> forever_N ge p s2 T ->
+      forever_N ge q s1 (t *** T)
+  | forever_N_plus: forall s1 t s2 p q T,
+      plus ge s1 t s2 -> forever_N ge p s2 T ->
+      forever_N ge q s1 (t *** T).
+
+Remark Peano_induction:
+  forall (P: nat -> Prop),
+  (forall p, (forall q, (q < p)%nat -> P q) -> P p) ->
+  forall p, P p.
+Proof.
+  intros P IH.
+  assert (forall p, forall q, (q < p)%nat -> P q).
+  induction p; intros. elimtype False; omega.
+  apply IH. intros. apply IHp. omega.
+  intro. apply H with (S p). omega.
+Qed.
+
+Lemma forever_N_inv:
+  forall ge p s T,
+  forever_N ge p s T ->
+  exists t, exists s', exists q, exists T',
+  step ge s t s' /\ forever_N ge q s' T' /\ T = t *** T'.
+Proof.
+  intros ge p. pattern p. apply Peano_induction; intros.
+  inv H0.
+  (* star case *)
+  inv H1.
+  (* no transition *)
+  change (E0 *** T0) with T0. apply H with p1. auto. auto. 
+  (* at least one transition *)
+  exists t1; exists s0; exists p0; exists (t2 *** T0).
+  split. auto. split. eapply forever_N_star; eauto.
+  apply Eappinf_assoc.
+  (* plus case *)
+  inv H1.
+  exists t1; exists s0; exists (S p1); exists (t2 *** T0).
+  split. auto. split. eapply forever_N_star; eauto. 
+  apply Eappinf_assoc.
+Qed.
+
+Lemma forever_N_forever:
+  forall ge p s T, forever_N ge p s T -> forever ge s T.
+Proof.
+  cofix COINDHYP; intros.
+  destruct (forever_N_inv H) as [t [s' [q [T' [A [B C]]]]]].
+  rewrite C. apply forever_intro with s'. auto. 
+  apply COINDHYP with q; auto.
+Qed.
+
+(** * Outcomes for program executions *)
+
+(** The two valid outcomes for the execution of a program:
+- Termination, with a finite trace of observable events
+  and an integer value that stands for the process exit code
+  (the return value of the main function).
+- Divergence with an infinite trace of observable events.
+  (The actual events generated by the execution can be a
+   finite prefix of this trace, or the whole trace.)
+*)
+
+Inductive program_behavior: Set :=
+  | Terminates: trace -> int -> program_behavior
+  | Diverges: traceinf -> program_behavior.
+
+(** Given a characterization of initial states and final states,
+  [program_behaves] relates a program behaviour with the 
+  sequences of transitions that can be taken from an initial state
+  to a final state. *)
+
+Variable initial_state: state -> Prop.
+Variable final_state: state -> int -> Prop.
+
+Inductive program_behaves (ge: genv): program_behavior -> Prop :=
+  | program_terminates: forall s t s' r,
+      initial_state s ->
+      star ge s t s' ->
+      final_state s' r ->
+      program_behaves ge (Terminates t r)
+  | program_diverges: forall s T,
+      initial_state s ->
+      forever ge s T ->
+      program_behaves ge (Diverges T).
+
+End CLOSURES.
+
+(** * Simulations between two small-step semantics. *)
+
+(** In this section, we show that if two transition relations 
+  satisfy certain simulation diagrams, then every program behaviour
+  generated by the first transition relation can also occur
+  with the second transition relation. *)
+
+Section SIMULATION.
+
+(** The first small-step semantics is axiomatized as follows. *)
+
+Variable genv1: Set.
+Variable state1: Set.
+Variable step1: genv1 -> state1 -> trace -> state1 -> Prop.
+Variable initial_state1: state1 -> Prop.
+Variable final_state1: state1 -> int -> Prop.
+Variable ge1: genv1.
+
+(** The second small-step semantics is also axiomatized. *)
+
+Variable genv2: Set.
+Variable state2: Set.
+Variable step2: genv2 -> state2 -> trace -> state2 -> Prop.
+Variable initial_state2: state2 -> Prop.
+Variable final_state2: state2 -> int -> Prop.
+Variable ge2: genv2.
+
+(** We assume given a matching relation between states of both semantics.
+  This matching relation must be compatible with initial states
+  and with final states. *)
+
+
+Variable match_states: state1 -> state2 -> Prop.
+
+Hypothesis match_initial_states:
+  forall st1, initial_state1 st1 ->
+  exists st2, initial_state2 st2 /\ match_states st1 st2.
+
+Hypothesis match_final_states:
+  forall st1 st2 r,
+  match_states st1 st2 ->
+  final_state1 st1 r ->
+  final_state2 st2 r.
+
+(** Simulation when one transition in the first program
+    corresponds to zero, one or several transitions in the second program.
+    However, there is no stuttering: infinitely many transitions
+    in the source program must correspond to infinitely many
+    transitions in the second program. *)
+
+Section SIMULATION_STAR.
+
+(** [measure] is a nonnegative integer associated with states
+  of the first semantics.  It must decrease when we take 
+  a stuttering step. *)
+
+Variable measure: state1 -> nat.
+
+Hypothesis simulation:
+  forall st1 t st1', step1 ge1 st1 t st1' ->
+  forall st2, match_states st1 st2 ->
+  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
+  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat.
+
+Lemma simulation_star_star:
+  forall st1 t st1', star step1 ge1 st1 t st1' ->
+  forall st2, match_states st1 st2 ->
+  exists st2', star step2 ge2 st2 t st2' /\ match_states st1' st2'.
+Proof.
+  induction 1; intros.
+  exists st2; split. apply star_refl. auto.
+  elim (simulation H H2).
+  intros [st2' [A B]]. 
+  destruct (IHstar _ B) as [st3' [C D]].
+  exists st3'; split. apply star_trans with t1 st2' t2.
+  apply plus_star; auto. auto. auto. auto.
+  intros [A [B C]]. rewrite H1. rewrite B. simpl. apply IHstar; auto.
+Qed.
+
+Lemma simulation_star_forever:
+  forall st1 st2 T,
+  forever step1 ge1 st1 T -> match_states st1 st2 ->
+  forever step2 ge2 st2 T.
+Proof.
+  assert (forall st1 st2 T,
+    forever step1 ge1 st1 T -> match_states st1 st2 ->
+    forever_N step2 ge2 (measure st1) st2 T).
+  cofix COINDHYP; intros.
+  inversion H; subst. elim (simulation H1 H0).
+  intros [st2' [A B]]. apply forever_N_plus with st2' (measure s2).
+  auto. apply COINDHYP. assumption. assumption.
+  intros [A [B C]].
+  apply forever_N_star with st2 (measure s2).
+  rewrite B. apply star_refl. auto.
+  apply COINDHYP. assumption. auto.
+  intros. eapply forever_N_forever; eauto.
+Qed.
+
+Lemma simulation_star_preservation:
+  forall beh,
+  program_behaves step1 initial_state1 final_state1 ge1 beh ->
+  program_behaves step2 initial_state2 final_state2 ge2 beh.
+Proof.
+  intros. inversion H; subst.
+  destruct (match_initial_states H0) as [s2 [A B]].
+  destruct (simulation_star_star H1 B) as [s2' [C D]].
+  econstructor; eauto.
+  destruct (match_initial_states H0) as [s2 [A B]].
+  econstructor; eauto.
+  eapply simulation_star_forever; eauto.
+Qed.
+
+End SIMULATION_STAR.
+
+(** Lock-step simulation: each transition in the first semantics
+    corresponds to exactly one transition in the second semantics. *)
+
+Section SIMULATION_STEP.
+
+Hypothesis simulation:
+  forall st1 t st1', step1 ge1 st1 t st1' ->
+  forall st2, match_states st1 st2 ->
+  exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2'.
+
+Lemma simulation_step_preservation:
+  forall beh,
+  program_behaves step1 initial_state1 final_state1 ge1 beh ->
+  program_behaves step2 initial_state2 final_state2 ge2 beh.
+Proof.
+  intros.
+  pose (measure := fun (st: state1) => 0%nat).
+  assert (simulation':
+  forall st1 t st1', step1 ge1 st1 t st1' ->
+  forall st2, match_states st1 st2 ->
+  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
+  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
+  intros. destruct (simulation H0 H1) as [st2' [A B]].
+  left; exists st2'; split. apply plus_one; auto. auto.
+  eapply simulation_star_preservation; eauto.
+Qed.
+
+End SIMULATION_STEP.
+
+(** Simulation when one transition in the first program corresponds
+    to one or several transitions in the second program. *)
+
+Section SIMULATION_PLUS.
+
+Hypothesis simulation:
+  forall st1 t st1', step1 ge1 st1 t st1' ->
+  forall st2, match_states st1 st2 ->
+  exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2'.
+
+Lemma simulation_plus_preservation:
+  forall beh,
+  program_behaves step1 initial_state1 final_state1 ge1 beh ->
+  program_behaves step2 initial_state2 final_state2 ge2 beh.
+Proof.
+  intros.
+  pose (measure := fun (st: state1) => 0%nat).
+  assert (simulation':
+  forall st1 t st1', step1 ge1 st1 t st1' ->
+  forall st2, match_states st1 st2 ->
+  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
+  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
+  intros. destruct (simulation H0 H1) as [st2' [A B]].
+  left; exists st2'; auto.
+  eapply simulation_star_preservation; eauto.
+Qed.
+
+End SIMULATION_PLUS.
+
+(** Simulation when one transition in the first program
+    corresponds to zero or one transitions in the second program.
+    However, there is no stuttering: infinitely many transitions
+    in the source program must correspond to infinitely many
+    transitions in the second program. *)
+
+Section SIMULATION_OPT.
+
+Variable measure: state1 -> nat.
+
+Hypothesis simulation:
+  forall st1 t st1', step1 ge1 st1 t st1' ->
+  forall st2, match_states st1 st2 ->
+  (exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2')
+  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat.
+
+Lemma simulation_opt_preservation:
+  forall beh,
+  program_behaves step1 initial_state1 final_state1 ge1 beh ->
+  program_behaves step2 initial_state2 final_state2 ge2 beh.
+Proof.
+  assert (simulation':
+    forall st1 t st1', step1 ge1 st1 t st1' ->
+    forall st2, match_states st1 st2 ->
+    (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
+    \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
+  intros. elim (simulation H H0). 
+  intros [st2' [A B]]. left. exists st2'; split. apply plus_one; auto. auto.
+  intros [A [B C]]. right. intuition.
+  intros. eapply simulation_star_preservation; eauto.
+Qed.
+
+End SIMULATION_OPT.
+
+End SIMULATION.
+
+
diff --git a/common/Switch.v b/common/Switch.v
new file mode 100644
index 0000000..e8b3967
--- /dev/null
+++ b/common/Switch.v
@@ -0,0 +1,165 @@
+(** Multi-way branches (``[switch]'') and their compilation
+    to 2-way comparison trees. *)
+
+Require Import EqNat.
+Require Import Coqlib.
+Require Import Integers.
+
+(** A multi-way branch is composed of a list of (key, action) pairs,
+  plus a default action.  *)
+
+Definition table : Set := list (int * nat).
+
+Fixpoint switch_target (n: int) (dfl: nat) (cases: table)
+                       {struct cases} : nat :=
+  match cases with
+  | nil => dfl
+  | (key, action) :: rem =>
+      if Int.eq n key then action else switch_target n dfl rem
+  end.
+
+(** Multi-way branches are translated to a 2-way comparison tree.
+    Each node of the tree performs an equality test or a less-than
+    test against one of the keys. *)
+
+Inductive comptree : Set :=
+  | CTaction: nat -> comptree
+  | CTifeq: int -> nat -> comptree -> comptree
+  | CTiflt: int -> comptree -> comptree -> comptree.
+
+Fixpoint comptree_match (n: int) (t: comptree) {struct t}: nat :=
+  match t with
+  | CTaction act => act
+  | CTifeq key act t' =>
+      if Int.eq n key then act else comptree_match n t'
+  | CTiflt key t1 t2 =>
+      if Int.ltu n key then comptree_match n t1 else comptree_match n t2
+  end.
+
+(** The translation from a table to a comparison tree is performed
+  by untrusted Caml code (function [compile_switch] in
+  file [RTLgenaux.ml]).  In Coq, we validate a posteriori the
+  result of this function.  In other terms, we now develop
+  and prove correct Coq functions that take a table and a comparison
+  tree, and check that their semantics are equivalent. *)
+
+Fixpoint split_lt (pivot: int) (cases: table)
+                  {struct cases} : table * table :=
+  match cases with
+  | nil => (nil, nil)
+  | (key, act) :: rem =>
+      let (l, r) := split_lt pivot rem in
+      if Int.ltu key pivot
+      then ((key, act) :: l, r)
+      else (l, (key, act) :: r)
+  end.
+
+Fixpoint split_eq (pivot: int) (cases: table)
+                  {struct cases} : option nat * table :=
+  match cases with
+  | nil => (None, nil)
+  | (key, act) :: rem =>
+      let (same, others) := split_eq pivot rem in
+      if Int.eq key pivot
+      then (Some act, others)
+      else (same, (key, act) :: others)
+  end.
+
+Fixpoint validate_switch (default: nat) (cases: table) (t: comptree)
+                  {struct t} : bool :=
+  match t with
+  | CTaction act =>
+      match cases with
+      | nil => beq_nat act default
+      | _ => false
+      end
+  | CTifeq pivot act t' =>
+      match split_eq pivot cases with
+      | (None, _) => false
+      | (Some act', others) => beq_nat act act' && validate_switch default others t'
+      end
+  | CTiflt pivot t1 t2 =>
+      match split_lt pivot cases with
+      | (lcases, rcases) =>
+          validate_switch default lcases t1 && validate_switch default rcases t2
+      end
+  end.
+
+(** Correctness proof for validation. *)
+
+Lemma split_eq_prop:
+  forall v default n cases optact cases',
+  split_eq n cases = (optact, cases') ->
+  switch_target v default cases =
+   (if Int.eq v n
+    then match optact with Some act => act | None => default end
+    else switch_target v default cases').
+Proof.
+  induction cases; simpl; intros until cases'.
+  intros. inversion H; subst. simpl. 
+  destruct (Int.eq v n); auto.
+  destruct a as [key act]. 
+  case_eq (split_eq n cases). intros same other SEQ.
+  rewrite (IHcases _ _ SEQ).
+  predSpec Int.eq Int.eq_spec key n; intro EQ; inversion EQ; simpl.
+  subst n. destruct (Int.eq v key). auto. auto.
+  predSpec Int.eq Int.eq_spec v key. 
+  subst v. predSpec Int.eq Int.eq_spec key n. congruence. auto.
+  auto.
+Qed.
+
+Lemma split_lt_prop:
+  forall v default n cases lcases rcases,
+  split_lt n cases = (lcases, rcases) ->
+  switch_target v default cases =
+    (if Int.ltu v n
+     then switch_target v default lcases
+     else switch_target v default rcases).
+Proof.
+  induction cases; intros until rcases; simpl.
+  intro. inversion H; subst. simpl.
+  destruct (Int.ltu v n); auto.
+  destruct a as [key act]. 
+  case_eq (split_lt n cases). intros lc rc SEQ.
+  rewrite (IHcases _ _ SEQ).
+  case_eq (Int.ltu key n); intros; inv H0; simpl.
+  predSpec Int.eq Int.eq_spec v key. 
+  subst v. rewrite H. auto.
+  auto.
+  predSpec Int.eq Int.eq_spec v key. 
+  subst v. rewrite H. auto.
+  auto.
+Qed.
+
+Definition table_tree_agree
+    (default: nat) (cases: table) (t: comptree) : Prop :=
+  forall v, switch_target v default cases = comptree_match v t.
+
+Lemma validate_switch_correct:
+  forall default t cases,
+  validate_switch default cases t = true ->
+  table_tree_agree default cases t.
+Proof.
+  induction t; simpl; intros until cases.
+  (* base case *)
+  destruct cases. 2: congruence.
+  intro. replace n with default. 
+  red; intros; simpl; auto.
+  symmetry. apply beq_nat_eq. auto. 
+  (* eq node *)
+  case_eq (split_eq i cases). intros optact cases' EQ. 
+  destruct optact as [ act | ]. 2: congruence.
+  intros. destruct (andb_prop _ _ H). 
+  replace n with act. 
+  generalize (IHt _ H1); intro.  
+  red; intros. simpl. rewrite <- H2.
+  change act with (match Some act with Some act => act | None => default end).
+  eapply split_eq_prop; eauto.
+  symmetry. apply beq_nat_eq. auto. 
+  (* lt node *)
+  case_eq (split_lt i cases). intros lcases rcases EQ V.
+  destruct (andb_prop _ _ V). 
+  red; intros. simpl. 
+  rewrite <- (IHt1 _ H). rewrite <- (IHt2 _ H0). 
+  eapply split_lt_prop; eauto.
+Qed.
diff --git a/common/Values.v b/common/Values.v
index aa59e04..e5b4971 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -885,4 +885,68 @@ Proof.
   elim H0; intro; subst v; reflexivity.
 Qed.
 
+(** The ``is less defined'' relation between values. 
+    A value is less defined than itself, and [Vundef] is
+    less defined than any value. *)
+
+Inductive lessdef: val -> val -> Prop :=
+  | lessdef_refl: forall v, lessdef v v
+  | lessdef_undef: forall v, lessdef Vundef v.
+
+Inductive lessdef_list: list val -> list val -> Prop :=
+  | lessdef_list_nil:
+      lessdef_list nil nil
+  | lessdef_list_cons:
+      forall v1 v2 vl1 vl2,
+      lessdef v1 v2 -> lessdef_list vl1 vl2 ->
+      lessdef_list (v1 :: vl1) (v2 :: vl2).
+
+Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.
+
+Lemma lessdef_list_inv:
+  forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1.
+Proof.
+  induction 1; simpl.
+  tauto.
+  inv H. destruct IHlessdef_list. 
+  left; congruence. tauto. tauto.
+Qed.
+
+Lemma load_result_lessdef:
+  forall chunk v1 v2,
+  lessdef v1 v2 -> lessdef (load_result chunk v1) (load_result chunk v2).
+Proof.
+  intros. inv H. auto. destruct chunk; simpl; auto.
+Qed.
+
+Lemma cast8signed_lessdef:
+  forall v1 v2, lessdef v1 v2 -> lessdef (cast8signed v1) (cast8signed v2).
+Proof.
+  intros; inv H; simpl; auto.
+Qed.
+
+Lemma cast8unsigned_lessdef:
+  forall v1 v2, lessdef v1 v2 -> lessdef (cast8unsigned v1) (cast8unsigned v2).
+Proof.
+  intros; inv H; simpl; auto.
+Qed.
+
+Lemma cast16signed_lessdef:
+  forall v1 v2, lessdef v1 v2 -> lessdef (cast16signed v1) (cast16signed v2).
+Proof.
+  intros; inv H; simpl; auto.
+Qed.
+
+Lemma cast16unsigned_lessdef:
+  forall v1 v2, lessdef v1 v2 -> lessdef (cast16unsigned v1) (cast16unsigned v2).
+Proof.
+  intros; inv H; simpl; auto.
+Qed.
+
+Lemma singleoffloat_lessdef:
+  forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2).
+Proof.
+  intros; inv H; simpl; auto.
+Qed.
+
 End Val.