Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


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

8 files changed, 1957 insertions, 1296 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index f48b0ab..ba3a2bf 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -20,9 +20,8 @@ Require Import Maps.
 Require Import Ordered.
 Require Import AST.
 Require Import Integers.
-Require Mem.
+Require Import Memdata.
 Require Import Csharpminor.
-Require Import Op.
 Require Import Cminor.
 
 Open Local Scope string_scope.
@@ -49,14 +48,132 @@ Open Local Scope error_monad_scope.
   of Cminor.
 *)
 
-(** Translation of constants. *)
+(** Compile-time information attached to each Csharpminor
+  variable: global variables, local variables, function parameters.
+  [Var_local] denotes a scalar local variable whose address is not
+  taken; it will be translated to a Cminor local variable of the
+  same name.  [Var_stack_scalar] and [Var_stack_array] denote
+  local variables that are stored as sub-blocks of the Cminor stack
+  data block.  [Var_global_scalar] and [Var_global_array] denote
+  global variables, stored in the global symbols with the same names. *)
 
-Definition transl_constant (cst: Csharpminor.constant): constant :=
-  match cst with
-  | Csharpminor.Ointconst n => Ointconst n
-  | Csharpminor.Ofloatconst n => Ofloatconst n
+Inductive var_info: Type :=
+  | Var_local: memory_chunk -> var_info
+  | Var_stack_scalar: memory_chunk -> Z -> var_info
+  | Var_stack_array: Z -> var_info
+  | Var_global_scalar: memory_chunk -> var_info
+  | Var_global_array: var_info.
+
+Definition compilenv := PMap.t var_info.
+
+(** Infer the type or memory chunk of the result of an expression. *)
+
+Definition chunktype_const (c: Csharpminor.constant) :=
+  match c with
+  | Csharpminor.Ointconst n => Mint32
+  | Csharpminor.Ofloatconst n => Mfloat64
   end.
 
+Definition chunktype_unop (op: unary_operation) :=
+  match op with
+  | Ocast8unsigned => Mint8unsigned
+  | Ocast8signed => Mint8signed
+  | Ocast16unsigned => Mint16unsigned
+  | Ocast16signed => Mint16signed
+  | Onegint => Mint32
+  | Onotbool => Mint32
+  | Onotint => Mint32
+  | Onegf => Mfloat64
+  | Oabsf => Mfloat64
+  | Osingleoffloat => Mfloat32
+  | Ointoffloat => Mint32
+  | Ointuoffloat => Mint32
+  | Ofloatofint => Mfloat64
+  | Ofloatofintu => Mfloat64
+  end.
+
+Definition chunktype_binop (op: binary_operation) :=
+  match op with
+  | Oadd => Mint32
+  | Osub => Mint32
+  | Omul => Mint32
+  | Odiv => Mint32
+  | Odivu => Mint32
+  | Omod => Mint32
+  | Omodu => Mint32
+  | Oand => Mint32
+  | Oor => Mint32
+  | Oxor => Mint32
+  | Oshl => Mint32
+  | Oshr => Mint32
+  | Oshru => Mint32
+  | Oaddf => Mfloat64
+  | Osubf => Mfloat64
+  | Omulf => Mfloat64
+  | Odivf => Mfloat64
+  | Ocmp c => Mint8unsigned
+  | Ocmpu c => Mint8unsigned
+  | Ocmpf c => Mint8unsigned
+  end.
+
+Definition chunktype_compat (src dst: memory_chunk) : bool :=
+  match src, dst with
+  | Mint8unsigned, (Mint8unsigned|Mint16unsigned|Mint16signed|Mint32) => true
+  | Mint8signed, (Mint8signed|Mint16unsigned|Mint16signed|Mint32) => true
+  | Mint16unsigned, (Mint16unsigned|Mint32) => true
+  | Mint16signed, (Mint16signed|Mint32) => true
+  | Mint32, Mint32 => true
+  | Mfloat32, (Mfloat32|Mfloat64) => true
+  | Mfloat64, Mfloat64 => true
+  | _, _ => false
+  end.
+
+Definition chunk_for_type (ty: typ) : memory_chunk :=
+  match ty with Tint => Mint32 | Tfloat => Mfloat64 end.
+
+Definition chunktype_merge (c1 c2: memory_chunk) : res memory_chunk :=
+  if chunktype_compat c1 c2 then
+    OK c2
+  else if chunktype_compat c2 c1 then
+    OK c1
+  else if typ_eq (type_of_chunk c1) (type_of_chunk c2) then
+    OK (chunk_for_type (type_of_chunk c1))
+  else
+    Error(msg "Cminorgen: chunktype_merge").
+
+Fixpoint chunktype_expr (cenv: compilenv) (e: Csharpminor.expr)
+                        {struct e}: res memory_chunk :=
+  match e with
+  | Csharpminor.Evar id =>
+      match cenv!!id with
+      | Var_local chunk => OK chunk
+      | Var_stack_scalar chunk ofs => OK chunk
+      | Var_global_scalar chunk => OK chunk
+      | _ => Error(msg "Cminorgen.chunktype_expr")
+      end
+  | Csharpminor.Eaddrof id =>
+      OK Mint32
+  | Csharpminor.Econst cst =>
+      OK (chunktype_const cst)
+  | Csharpminor.Eunop op e1 =>
+      OK (chunktype_unop op)
+  | Csharpminor.Ebinop op e1 e2 =>
+      OK (chunktype_binop op)
+  | Csharpminor.Eload chunk e =>
+      OK chunk
+  | Csharpminor.Econdition e1 e2 e3 =>
+      do chunk2 <- chunktype_expr cenv e2;
+      do chunk3 <- chunktype_expr cenv e3;
+      chunktype_merge chunk2 chunk3
+  end.
+
+Definition type_expr  (cenv: compilenv) (e: Csharpminor.expr): res typ :=
+  do c <- chunktype_expr cenv e; OK(type_of_chunk c).
+
+Definition type_exprlist (cenv: compilenv) (el: list Csharpminor.expr):
+                                                       res (list typ) :=
+  mmap (type_expr cenv) el.
+
 (** [make_cast chunk e] returns a Cminor expression that normalizes
   the value of Cminor expression [e] as prescribed by the memory chunk
   [chunk].  For instance, 8-bit sign extension is performed if
@@ -74,10 +191,9 @@ Definition make_cast (chunk: memory_chunk) (e: expr): expr :=
   end.
 
 (** When the translation of an expression is stored in memory,
-  the normalization performed by [make_cast] can be redundant
+  a cast at the toplevel of the expression can be redundant
   with that implicitly performed by the memory store.
-  [store_arg] detects this case and strips away the redundant
-  normalization. *)
+  [store_arg] detects this case and strips away the redundant cast. *)
 
 Definition store_arg (chunk: memory_chunk) (e: expr) : expr :=
   match e with
@@ -103,26 +219,7 @@ Definition make_stackaddr (ofs: Z): expr :=
 Definition make_globaladdr (id: ident): expr :=
   Econst (Oaddrsymbol id Int.zero).
 
-(** Compile-time information attached to each Csharpminor
-  variable: global variables, local variables, function parameters.
-  [Var_local] denotes a scalar local variable whose address is not
-  taken; it will be translated to a Cminor local variable of the
-  same name.  [Var_stack_scalar] and [Var_stack_array] denote
-  local variables that are stored as sub-blocks of the Cminor stack
-  data block.  [Var_global_scalar] and [Var_global_array] denote
-  global variables, stored in the global symbols with the same names. *)
-
-Inductive var_info: Type :=
-  | Var_local: memory_chunk -> var_info
-  | Var_stack_scalar: memory_chunk -> Z -> var_info
-  | Var_stack_array: Z -> var_info
-  | Var_global_scalar: memory_chunk -> var_info
-  | Var_global_array: var_info.
-
-Definition compilenv := PMap.t var_info.
-
-(** Generation of Cminor code corresponding to accesses to Csharpminor 
-  local variables: reads, assignments, and taking the address of. *)
+(** Generation of a Cminor expression for reading a Csharpminor variable. *)
 
 Definition var_get (cenv: compilenv) (id: ident): res expr :=
   match PMap.get id cenv with
@@ -136,24 +233,67 @@ Definition var_get (cenv: compilenv) (id: ident): res expr :=
       Error(msg "Cminorgen.var_get")
   end.
 
-Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): res stmt :=
+(** Generation of a Cminor expression for taking the address of
+  a Csharpminor variable. *)
+
+Definition var_addr (cenv: compilenv) (id: ident): res expr :=
+  match PMap.get id cenv with
+  | Var_local chunk => Error(msg "Cminorgen.var_addr")
+  | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs)
+  | Var_stack_array ofs => OK (make_stackaddr ofs)
+  | _ => OK (make_globaladdr id)
+  end.
+
+(** Generation of a Cminor statement performing an assignment to
+  a variable.  [rhs_chunk] is the inferred chunk type for the
+  right-hand side.  If the variable was allocated to a Cminor variable,
+  a cast may need to be inserted to normalize the value of the r.h.s.,
+  as per Csharpminor's semantics. *)
+
+Definition var_set (cenv: compilenv)
+                   (id: ident) (rhs: expr) (rhs_chunk: memory_chunk): res stmt :=
   match PMap.get id cenv with
   | Var_local chunk =>
-      OK(Sassign id (make_cast chunk rhs))
+      if chunktype_compat rhs_chunk chunk then
+        OK(Sassign id rhs)
+      else if typ_eq (type_of_chunk chunk) (type_of_chunk rhs_chunk) then
+        OK(Sassign id (make_cast chunk rhs))
+      else
+        Error(msg "Cminorgen.var_set.1")
   | Var_stack_scalar chunk ofs =>
       OK(make_store chunk (make_stackaddr ofs) rhs)
   | Var_global_scalar chunk =>
       OK(make_store chunk (make_globaladdr id) rhs)
   | _ =>
-      Error(msg "Cminorgen.var_set")
+      Error(msg "Cminorgen.var_set.2")
   end.
 
-Definition var_addr (cenv: compilenv) (id: ident): res expr :=
+(** A variant of [var_set] used for initializing function parameters
+  and storing the return values of function calls.  The value to
+  be stored already resides in the Cminor variable called [id].
+  Moreover, its chunk type is not known, only its int-or-float type. *)
+
+Definition var_set_self (cenv: compilenv) (id: ident) (ty: typ): res stmt :=
   match PMap.get id cenv with
-  | Var_local chunk => Error(msg "Cminorgen.var_addr")
-  | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs)
-  | Var_stack_array ofs => OK (make_stackaddr ofs)
-  | _ => OK (make_globaladdr id)
+  | Var_local chunk =>
+      if typ_eq (type_of_chunk chunk) ty then
+        OK(Sassign id (make_cast chunk (Evar id)))
+      else
+        Error(msg "Cminorgen.var_set_self.1")
+  | Var_stack_scalar chunk ofs =>
+      OK(make_store chunk (make_stackaddr ofs) (Evar id))
+  | Var_global_scalar chunk =>
+      OK(make_store chunk (make_globaladdr id) (Evar id))
+  | _ =>
+      Error(msg "Cminorgen.var_set_self.2")
+  end.
+
+(** Translation of constants. *)
+
+Definition transl_constant (cst: Csharpminor.constant): constant :=
+  match cst with
+  | Csharpminor.Ointconst n => Ointconst n
+  | Csharpminor.Ofloatconst n => Ofloatconst n
   end.
 
 (** Translation of expressions.  All the hard work is done by the
@@ -234,16 +374,27 @@ Fixpoint switch_env (ls: lbl_stmt) (e: exit_env) {struct ls}: exit_env :=
   | LScase _ _ ls' => false :: switch_env ls' e
   end.
 
-(** Translation of statements.  The only nonobvious part is
-  the translation of [switch] statements, outlined above. *)
+(** Translation of statements.  The nonobvious part is
+  the translation of [switch] statements, outlined above. 
+  Also note the additional type checks on arguments to calls and returns.
+  These checks should always succeed for C#minor code generated from
+  well-typed Clight code, but are necessary for the correctness proof
+  to go through.
+*)
+
+Definition typ_of_opttyp (ot: option typ) :=
+  match ot with None => Tint | Some t => t end.
 
-Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
+Fixpoint transl_stmt (ret: option typ) (cenv: compilenv) 
+                     (xenv: exit_env) (s: Csharpminor.stmt)
                      {struct s}: res stmt :=
   match s with
   | Csharpminor.Sskip =>
       OK Sskip
   | Csharpminor.Sassign id e =>
-      do te <- transl_expr cenv e; var_set cenv id te
+      do chunk <- chunktype_expr cenv e;
+      do te <- transl_expr cenv e;
+      var_set cenv id te chunk
   | Csharpminor.Sstore chunk e1 e2 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_expr cenv e2;
@@ -251,26 +402,32 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
   | Csharpminor.Scall None sig e el =>
       do te <- transl_expr cenv e;
       do tel <- transl_exprlist cenv el;
-      OK (Scall None sig te tel)
+      do tyl <- type_exprlist cenv el;
+      if list_eq_dec typ_eq tyl sig.(sig_args)
+      then OK (Scall None sig te tel)
+      else Error(msg "Cminorgen.transl_stmt(call0)")
   | Csharpminor.Scall (Some id) sig e el =>
       do te <- transl_expr cenv e;
       do tel <- transl_exprlist cenv el;
-      do s <- var_set cenv id (Evar id);
-      OK (Sseq (Scall (Some id) sig te tel) s)
+      do tyl <- type_exprlist cenv el;
+      do s <- var_set_self cenv id (proj_sig_res sig);
+      if list_eq_dec typ_eq tyl sig.(sig_args)
+      then OK (Sseq (Scall (Some id) sig te tel) s)
+      else Error(msg "Cminorgen.transl_stmt(call1)")
   | Csharpminor.Sseq s1 s2 =>
-      do ts1 <- transl_stmt cenv xenv s1;
-      do ts2 <- transl_stmt cenv xenv s2;
+      do ts1 <- transl_stmt ret cenv xenv s1;
+      do ts2 <- transl_stmt ret cenv xenv s2;
       OK (Sseq ts1 ts2)
   | Csharpminor.Sifthenelse e s1 s2 =>
       do te <- transl_expr cenv e;
-      do ts1 <- transl_stmt cenv xenv s1;
-      do ts2 <- transl_stmt cenv xenv s2;
+      do ts1 <- transl_stmt ret cenv xenv s1;
+      do ts2 <- transl_stmt ret cenv xenv s2;
       OK (Sifthenelse te ts1 ts2)
   | Csharpminor.Sloop s =>
-      do ts <- transl_stmt cenv xenv s;
+      do ts <- transl_stmt ret cenv xenv s;
       OK (Sloop ts)
   | Csharpminor.Sblock s =>
-      do ts <- transl_stmt cenv (true :: xenv) s;
+      do ts <- transl_stmt ret cenv (true :: xenv) s;
       OK (Sblock ts)
   | Csharpminor.Sexit n =>
       OK (Sexit (shift_exit xenv n))
@@ -278,27 +435,31 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
       let cases := switch_table ls O in
       let default := length cases in
       do te <- transl_expr cenv e;
-      transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te cases default)
+      transl_lblstmt ret cenv (switch_env ls xenv) ls (Sswitch te cases default)
   | Csharpminor.Sreturn None =>
       OK (Sreturn None)
   | Csharpminor.Sreturn (Some e) =>
-      do te <- transl_expr cenv e; OK (Sreturn (Some te))
+      do te <- transl_expr cenv e;
+      do ty <- type_expr cenv e;
+      if typ_eq ty (typ_of_opttyp ret)
+      then OK (Sreturn (Some te))
+      else Error(msg "Cminorgen.transl_stmt(return)")
   | Csharpminor.Slabel lbl s =>
-      do ts <- transl_stmt cenv xenv s; OK (Slabel lbl ts)
+      do ts <- transl_stmt ret cenv xenv s; OK (Slabel lbl ts)
   | Csharpminor.Sgoto lbl =>
       OK (Sgoto lbl)
   end
 
-with transl_lblstmt (cenv: compilenv) (xenv: exit_env)
-                    (ls: Csharpminor.lbl_stmt) (body: stmt)
+with transl_lblstmt (ret: option typ) (cenv: compilenv)
+                    (xenv: exit_env) (ls: Csharpminor.lbl_stmt) (body: stmt)
                     {struct ls}: res stmt :=
   match ls with
   | Csharpminor.LSdefault s =>
-      do ts <- transl_stmt cenv xenv s;
+      do ts <- transl_stmt ret cenv xenv s;
       OK (Sseq (Sblock body) ts)
   | Csharpminor.LScase _ s ls' =>
-      do ts <- transl_stmt cenv xenv s;
-      transl_lblstmt cenv (List.tail xenv) ls' (Sseq (Sblock body) ts)
+      do ts <- transl_stmt ret cenv xenv s;
+      transl_lblstmt ret cenv (List.tail xenv) ls' (Sseq (Sblock body) ts)
   end.
 
 (** Computation of the set of variables whose address is taken in
@@ -379,7 +540,7 @@ Definition assign_variable
       (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz)
   | (id, Vscalar chunk) =>
       if Identset.mem id atk then
-        let sz := Mem.size_chunk chunk in
+        let sz := size_chunk chunk in
         let ofs := align stacksize sz in
         (PMap.set id (Var_stack_scalar chunk ofs) cenv, ofs + sz)
       else
@@ -425,7 +586,7 @@ Fixpoint store_parameters
   match params with
   | nil => OK Sskip
   | (id, chunk) :: rem =>
-      do s1 <- var_set cenv id (Evar id);
+      do s1 <- var_set_self cenv id (type_of_chunk chunk);
       do s2 <- store_parameters cenv rem;
       OK (Sseq s1 s2)
   end.
@@ -471,7 +632,7 @@ Definition make_vars (params: list ident) (vars: list ident)
 
 Definition transl_funbody 
   (cenv: compilenv) (stacksize: Z) (f: Csharpminor.function): res function :=
-    do tbody <- transl_stmt cenv nil f.(Csharpminor.fn_body);
+    do tbody <- transl_stmt f.(fn_return) cenv nil f.(Csharpminor.fn_body);
     do sparams <- store_parameters cenv f.(Csharpminor.fn_params);
        OK (mkfunction
               (Csharpminor.fn_sig f)
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index a472e70..c79555c 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -12,20 +12,23 @@
 
 (** Correctness proof for Cminor generation. *)
 
+Require Import Coq.Program.Equality.
 Require Import FSets.
 Require Import Coqlib.
+Require Intv.
 Require Import Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memdata.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
+Require Import Switch.
 Require Import Csharpminor.
-Require Import Op.
 Require Import Cminor.
 Require Import Cminorgen.
 
@@ -51,20 +54,19 @@ Lemma function_ptr_translated:
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transl_fundef gce f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar TRANSL).
-
+Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).
 
 Lemma functions_translated:
   forall (v: val) (f: Csharpminor.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transl_fundef gce f = OK tf.
-Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL).
+Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).
 
 Lemma sig_preserved_body:
   forall f tf cenv size,
   transl_funbody cenv size f = OK tf -> 
-  tf.(fn_sig) = f.(Csharpminor.fn_sig).
+  tf.(fn_sig) = Csharpminor.fn_sig f.
 Proof.
   intros. monadInv H. reflexivity.
 Qed.
@@ -112,6 +114,193 @@ Proof.
   intro. rewrite PMap.gi. auto.
 Qed.
 
+(** * Derived properties of memory operations *)
+
+Lemma load_freelist:
+  forall fbl chunk m b ofs m',
+  (forall b' lo hi, In (b', lo, hi) fbl -> b' <> b) -> 
+  Mem.free_list m fbl = Some m' ->
+  Mem.load chunk m' b ofs = Mem.load chunk m b ofs.
+Proof.
+  induction fbl; intros.
+  simpl in H0. congruence.
+  destruct a as [[b' lo] hi].
+  generalize H0. simpl. case_eq (Mem.free m b' lo hi); try congruence.
+  intros m1 FR1 FRL. 
+  transitivity (Mem.load chunk m1 b ofs).
+  eapply IHfbl; eauto. intros. eapply H. eauto with coqlib. 
+  eapply Mem.load_free; eauto. left. apply sym_not_equal. eapply H. auto with coqlib. 
+Qed.
+
+Lemma perm_freelist:
+  forall fbl m m' b ofs p,
+  Mem.free_list m fbl = Some m' ->
+  Mem.perm m' b ofs p ->
+  Mem.perm m b ofs p.
+Proof.
+  induction fbl; simpl; intros until p.
+  congruence.
+  destruct a as [[b' lo] hi]. case_eq (Mem.free m b' lo hi); try congruence.
+  intros. eauto with mem.
+Qed.
+
+Lemma nextblock_freelist:
+  forall fbl m m',
+  Mem.free_list m fbl = Some m' ->
+  Mem.nextblock m' = Mem.nextblock m.
+Proof.
+  induction fbl; intros until m'; simpl.
+  congruence.
+  destruct a as [[b lo] hi]. 
+  case_eq (Mem.free m b lo hi); intros; try congruence.
+  transitivity (Mem.nextblock m0). eauto. eapply Mem.nextblock_free; eauto.
+Qed.
+
+Lemma free_list_freeable:
+  forall l m m',
+  Mem.free_list m l = Some m' ->
+  forall b lo hi,
+  In (b, lo, hi) l -> Mem.range_perm m b lo hi Freeable.
+Proof.
+  induction l; simpl; intros.
+  contradiction.
+  revert H. destruct a as [[b' lo'] hi'].
+  caseEq (Mem.free m b' lo' hi'); try congruence.
+  intros m1 FREE1 FREE2.
+  destruct H0. inv H. 
+  eauto with mem.
+  red; intros. eapply Mem.perm_free_3; eauto. exploit IHl; eauto.
+Qed.
+
+Lemma bounds_freelist:
+  forall b l m m',
+  Mem.free_list m l = Some m' -> Mem.bounds m' b = Mem.bounds m b.
+Proof.
+  induction l; simpl; intros.
+  inv H; auto.
+  revert H. destruct a as [[b' lo'] hi'].
+  caseEq (Mem.free m b' lo' hi'); try congruence.
+  intros m1 FREE1 FREE2.
+  transitivity (Mem.bounds m1 b). eauto. eapply Mem.bounds_free; eauto.
+Qed.
+
+Lemma nextblock_storev:
+  forall chunk m addr v m',
+  Mem.storev chunk m addr v = Some m' -> Mem.nextblock m' = Mem.nextblock m.
+Proof.
+  unfold Mem.storev; intros. destruct addr; try discriminate. 
+  eapply Mem.nextblock_store; eauto.
+Qed.
+
+(** * Normalized values and operations over memory chunks *)
+
+(** A value is normalized with respect to a memory chunk if it is
+  invariant under the cast (truncation, sign extension) corresponding to
+  the chunk. *)
+
+Definition val_normalized (v: val) (chunk: memory_chunk) : Prop :=
+  Val.load_result chunk v = v.
+
+Lemma val_normalized_has_type:
+  forall chunk v, val_normalized v chunk -> Val.has_type v (type_of_chunk chunk).
+Proof.
+  intros until v; unfold val_normalized, Val.load_result.
+  destruct chunk; destruct v; intro EQ; try (inv EQ); simpl; exact I.
+Qed.
+
+Lemma val_has_type_normalized:
+  forall ty v, Val.has_type v ty -> val_normalized v (chunk_for_type ty).
+Proof.
+  unfold Val.has_type, val_normalized; intros; destruct ty; destruct v;
+  contradiction || reflexivity.
+Qed.
+
+Lemma chunktype_const_correct:
+  forall c v,
+  Csharpminor.eval_constant c = Some v ->
+  val_normalized v (chunktype_const c).
+Proof.
+  unfold Csharpminor.eval_constant; intros. 
+  destruct c; inv H; unfold val_normalized; auto.
+Qed.
+
+Lemma chunktype_unop_correct:
+  forall op v1 v,
+  Csharpminor.eval_unop op v1 = Some v ->
+  val_normalized v (chunktype_unop op).
+Proof.
+  intros; destruct op; simpl in *; unfold val_normalized.
+  inv H. destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. compute; auto.
+  inv H. destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto.
+  inv H. destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. compute; auto.
+  inv H. destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto.
+  destruct v1; inv H; auto.
+  destruct v1; inv H. destruct (Int.eq i Int.zero); auto. reflexivity.
+  destruct v1; inv H; auto.
+  destruct v1; inv H; auto.
+  destruct v1; inv H; auto.
+  inv H. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem; auto.
+  destruct v1; inv H; auto.
+  destruct v1; inv H; auto.
+  destruct v1; inv H; auto.
+  destruct v1; inv H; auto.
+Qed.
+
+Lemma chunktype_binop_correct:
+  forall op v1 v2 m v,
+  Csharpminor.eval_binop op v1 v2 m = Some v ->
+  val_normalized v (chunktype_binop op).
+Proof.
+  intros; destruct op; simpl in *; unfold val_normalized;
+  destruct v1; destruct v2; try (inv H; reflexivity).
+  destruct (eq_block b b0); inv H; auto.
+  destruct (Int.eq i0 Int.zero); inv H; auto.
+  destruct (Int.eq i0 Int.zero); inv H; auto.
+  destruct (Int.eq i0 Int.zero); inv H; auto.
+  destruct (Int.eq i0 Int.zero); inv H; auto.
+  destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
+  destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
+  destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
+  inv H; destruct (Int.cmp c i i0); reflexivity.
+  unfold eval_compare_null in H. destruct (Int.eq i Int.zero).
+  destruct c; inv H; auto. inv H.
+  unfold eval_compare_null in H. destruct (Int.eq i0 Int.zero).
+  destruct c; inv H; auto. inv H.
+  destruct (Mem.valid_pointer m b (Int.signed i) &&
+            Mem.valid_pointer m b0 (Int.signed i0)).
+  destruct (eq_block b b0); inv H. destruct (Int.cmp c i i0); auto.
+  destruct c; inv H1; auto. inv H.
+  inv H. destruct (Int.cmpu c i i0); auto.
+  inv H. destruct (Float.cmp c f f0); auto.
+Qed.
+
+Lemma chunktype_compat_correct:
+  forall src dst v,
+  chunktype_compat src dst = true ->
+  val_normalized v src -> val_normalized v dst.
+Proof.
+  unfold val_normalized; intros. rewrite <- H0.
+  destruct src; destruct dst; simpl in H; try discriminate; auto;
+  destruct v; simpl; auto.
+Admitted.
+
+Lemma chunktype_merge_correct:
+  forall c1 c2 c v,
+  chunktype_merge c1 c2 = OK c ->
+  val_normalized v c1 \/ val_normalized v c2 ->
+  val_normalized v c.
+Proof.
+  intros until v. unfold chunktype_merge. 
+  case_eq (chunktype_compat c1 c2).
+  intros. inv H0. destruct H1. eapply chunktype_compat_correct; eauto. auto.
+  case_eq (chunktype_compat c2 c1).
+  intros. inv H1. destruct H2. auto. eapply chunktype_compat_correct; eauto.
+  intros. destruct (typ_eq (type_of_chunk c1) (type_of_chunk c2)); inv H1.
+  apply val_has_type_normalized. destruct H2. 
+  apply val_normalized_has_type. auto.
+  rewrite e. apply val_normalized_has_type. auto.
+Qed.
+
 (** * Correspondence between Csharpminor's and Cminor's environments and memory states *)
 
 (** In Csharpminor, every variable is stored in a separate memory block.
@@ -125,12 +314,12 @@ Qed.
   to a sub-block of Cminor block [b] at offset [ofs].
 
   A memory injection [f] defines a relation [val_inject f] between
-  values and a relation [mem_inject f] between memory states.
-  These relations, defined in file [Memory], will be used intensively
+  values and a relation [Mem.inject f] between memory states.
+  These relations will be used intensively
   in our proof of simulation between Csharpminor and Cminor executions.
 
-  In the remainder of this section, we define relations between
-  Csharpminor and Cminor environments and call stacks. *)
+  In this section, we define the relation between
+  Csharpminor and Cminor environments. *)
 
 (** Matching for a Csharpminor variable [id].
 - If this variable is mapped to a Cminor local variable, the
@@ -187,7 +376,7 @@ Record match_env (f: meminj) (cenv: compilenv)
     me_vars:
       forall id, match_var f id e m te sp (PMap.get id cenv);
 
-(** The range [lo, hi] must not be empty. *)
+(** [lo, hi] is a proper interval. *)
     me_low_high:
       lo <= hi;
 
@@ -215,9 +404,16 @@ Record match_env (f: meminj) (cenv: compilenv)
   (i.e. allocated before the stack data for the current Cminor function). *)
     me_incr:
       forall b tb delta,
-      f b = Some(tb, delta) -> b < lo -> tb < sp
+      f b = Some(tb, delta) -> b < lo -> tb < sp;
+
+(** The sizes of blocks appearing in [e] agree with their types *)
+    me_bounds:
+      forall id b lv,
+      PTree.get id e = Some(b, lv) -> Mem.bounds m b = (0, sizeof lv)
   }.
 
+Hint Resolve me_low_high.
+
 (** Global environments match if the memory injection [f] leaves unchanged
   the references to global symbols and functions. *)
 
@@ -231,72 +427,28 @@ Record match_globalenvs (f: meminj) : Prop :=
       forall b, b < 0 -> f b = Some(b, 0)
   }.
 
-(** Call stacks represent abstractly the execution state of the current
-  Csharpminor and Cminor functions, as well as the states of the
-  calling functions.  A call stack is a list of frames, each frame
-  collecting information on the current execution state of a Csharpminor
-  function and its Cminor translation. *)
-
-Record frame : Type :=
-  mkframe {
-    fr_cenv: compilenv;
-    fr_e: Csharpminor.env;
-    fr_te: env;
-    fr_sp: block;
-    fr_low: Z;
-    fr_high: Z
-  }.
-
-Definition callstack : Type := list frame.
-
-(** Matching of call stacks imply matching of environments for each of
-  the frames, plus matching of the global environments, plus disjointness
-  conditions over the memory blocks allocated for local variables
-  and Cminor stack data. *)
-
-Inductive match_callstack: meminj -> callstack -> Z -> Z -> mem -> Prop :=
-  | mcs_nil:
-      forall f bound tbound m,
-      match_globalenvs f ->
-      match_callstack f nil bound tbound m
-  | mcs_cons:
-      forall f cenv e te sp lo hi cs bound tbound m,
-      hi <= bound ->
-      sp < tbound ->
-      match_env f cenv e m te sp lo hi ->
-      match_callstack f cs lo sp m ->
-      match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m.
-
 (** The remainder of this section is devoted to showing preservation
-  of the [match_callstack] invariant under various assignments and memory
+  of the [match_en] invariant under various assignments and memory
   stores.  First: preservation by memory stores to ``mapped'' blocks
   (block that have a counterpart in the Cminor execution). *)
 
+Ltac geninv x := 
+  let H := fresh in (generalize x; intro H; inv H).
+
 Lemma match_env_store_mapped:
   forall f cenv e m1 m2 te sp lo hi chunk b ofs v,
   f b <> None ->
-  store chunk m1 b ofs v = Some m2 ->
+  Mem.store chunk m1 b ofs v = Some m2 ->
   match_env f cenv e m1 te sp lo hi ->
   match_env f cenv e m2 te sp lo hi.
 Proof.
-  intros. inversion H1. constructor; auto.
+  intros; inv H1; constructor; auto.
   (* vars *)
-  intros. generalize (me_vars0 id); intro. 
-  inversion H2; econstructor; eauto.
-  rewrite <- H5. eapply load_store_other; eauto. 
+  intros. geninv (me_vars0 id); econstructor; eauto.
+  rewrite <- H4. eapply Mem.load_store_other; eauto. 
   left. congruence.
-Qed.
-
-Lemma match_callstack_mapped:
-  forall f cs bound tbound m1,
-  match_callstack f cs bound tbound m1 ->
-  forall chunk b ofs v m2,
-  f b <> None ->
-  store chunk m1 b ofs v = Some m2 ->
-  match_callstack f cs bound tbound m2.
-Proof.
-  induction 1; intros; econstructor; eauto.
-  eapply match_env_store_mapped; eauto.
+  (* bounds *)
+  intros. rewrite (Mem.bounds_store _ _ _ _ _ _ H0). eauto. 
 Qed.
 
 (** Preservation by assignment to a Csharpminor variable that is 
@@ -307,27 +459,28 @@ Qed.
 Lemma match_env_store_local:
   forall f cenv e m1 m2 te sp lo hi id b chunk v tv,
   e!id = Some(b, Vscalar chunk) ->
+  Val.has_type v (type_of_chunk chunk) ->
   val_inject f (Val.load_result chunk v) tv ->
-  store chunk m1 b 0 v = Some m2 ->
+  Mem.store chunk m1 b 0 v = Some m2 ->
   match_env f cenv e m1 te sp lo hi ->
   match_env f cenv e m2 (PTree.set id tv te) sp lo hi.
 Proof.
-  intros. inversion H2. constructor; auto.
-  intros. generalize (me_vars0 id0); intro.
-  inversion H3; subst.
+  intros. inv H3. constructor; auto.
+  (* vars *)
+  intros. geninv (me_vars0 id0).
   (* var_local *)
   case (peq id id0); intro.
     (* the stored variable *)
-    subst id0. 
-    change Csharpminor.var_kind with var_kind in H4. 
-    rewrite H in H5. injection H5; clear H5; intros; subst b0 chunk0.
+    subst id0.
+    assert (b0 = b) by congruence. subst.
+    assert (chunk0 = chunk) by congruence. subst.
     econstructor. eauto. 
-    eapply load_store_same; eauto. auto. 
+    eapply Mem.load_store_same; eauto. auto. 
     rewrite PTree.gss. reflexivity.
     auto.
     (* a different variable *)
     econstructor; eauto.
-    rewrite <- H6. eapply load_store_other; eauto. 
+    rewrite <- H6. eapply Mem.load_store_other; eauto. 
     rewrite PTree.gso; auto.
   (* var_stack_scalar *)
   econstructor; eauto.
@@ -337,49 +490,393 @@ Proof.
   econstructor; eauto.
   (* var_global_array *)
   econstructor; eauto.
+  (* bounds *)
+  intros. rewrite (Mem.bounds_store _ _ _ _ _ _ H2). eauto. 
 Qed.
 
-Lemma match_env_store_above:
-  forall f cenv e m1 m2 te sp lo hi chunk b v,
-  store chunk m1 b 0 v = Some m2 ->
-  hi <= b ->
+(** The [match_env] relation is preserved by any memory operation
+  that preserves sizes and loads from blocks in the [lo, hi] range. *)
+
+Lemma match_env_invariant:
+  forall f cenv e m1 m2 te sp lo hi,
+  (forall b ofs chunk v, 
+     lo <= b < hi -> Mem.load chunk m1 b ofs = Some v ->
+     Mem.load chunk m2 b ofs = Some v) ->
+  (forall b,
+     lo <= b < hi -> Mem.bounds m2 b = Mem.bounds m1 b) ->
   match_env f cenv e m1 te sp lo hi ->
   match_env f cenv e m2 te sp lo hi.
 Proof.
-  intros. inversion H1; constructor; auto.
-  intros. generalize (me_vars0 id); intro.
-  inversion H2; econstructor; eauto.
-  rewrite <- H5. eapply load_store_other; eauto.
-  left. generalize (me_bounded0 _ _ _ H4). unfold block in *. omega.
+  intros. inv H1. constructor; eauto.
+  (* vars *)
+  intros. geninv (me_vars0 id); econstructor; eauto.
+  (* bounds *)
+  intros. rewrite H0. eauto. eauto.
 Qed.
 
-Lemma match_callstack_store_above:
-  forall f cs bound tbound m1,
-  match_callstack f cs bound tbound m1 ->
-  forall chunk b v m2,
-  store chunk m1 b 0 v = Some m2 ->
-  bound <= b ->
-  match_callstack f cs bound tbound m2.
+(** [match_env] is insensitive to the Cminor values of stack-allocated data. *)
+
+Lemma match_env_extensional:
+  forall f cenv e m te1 sp lo hi te2,
+  match_env f cenv e m te1 sp lo hi ->
+  (forall id chunk, cenv!!id = Var_local chunk -> te2!id = te1!id) ->
+  match_env f cenv e m te2 sp lo hi.
 Proof.
-  induction 1; intros; econstructor; eauto.
-  eapply match_env_store_above with (b := b); eauto. omega.
+  intros. inv H; econstructor; eauto.
+  intros. geninv (me_vars0 id); econstructor; eauto.
+  rewrite <- H5. eauto. 
+Qed.
+
+(** [match_env] and allocations *)
+
+Inductive alloc_condition: var_info -> var_kind -> block -> option (block * Z) -> Prop :=
+  | alloc_cond_local: forall chunk sp,
+      alloc_condition (Var_local chunk) (Vscalar chunk) sp None
+  | alloc_cond_stack_scalar: forall chunk pos sp,
+      alloc_condition (Var_stack_scalar chunk pos) (Vscalar chunk) sp (Some(sp, pos))
+  | alloc_cond_stack_array: forall pos sz sp,
+      alloc_condition (Var_stack_array pos) (Varray sz) sp (Some(sp, pos)).
+
+Lemma match_env_alloc_same:
+  forall f1 cenv e m1 te sp lo lv m2 b f2 id info tv,
+  match_env f1 cenv e m1 te sp lo (Mem.nextblock m1) ->
+  Mem.alloc m1 0 (sizeof lv) = (m2, b) ->
+  inject_incr f1 f2 ->
+  alloc_condition info lv sp (f2 b) ->
+  (forall b', b' <> b -> f2 b' = f1 b') ->
+  te!id = Some tv ->
+  e!id = None ->
+  match_env f2 (PMap.set id info cenv) (PTree.set id (b, lv) e) m2 te sp lo (Mem.nextblock m2).
+Proof.
+  intros until tv.
+  intros ME ALLOC INCR ACOND OTHER TE E.
+(*
+  assert (ALLOC_RES: b = Mem.nextblock m1) by eauto with mem.
+  assert (ALLOC_NEXT: Mem.nextblock m2 = Zsucc(Mem.nextblock m1)) by eauto with mem.
+*)
+  inv ME; constructor.
+(* vars *)
+  intros. rewrite PMap.gsspec. destruct (peq id0 id). subst id0.
+  (* the new var *)
+  inv ACOND; econstructor.
+    (* local *)
+  rewrite PTree.gss. reflexivity. 
+  eapply Mem.load_alloc_same'; eauto. omega. simpl; omega. apply Zdivide_0.
+  auto. eauto. constructor. 
+    (* stack scalar *)
+  rewrite PTree.gss; reflexivity. 
+  econstructor; eauto. rewrite Int.add_commut; rewrite Int.add_zero; auto.
+    (* stack array *)
+  rewrite PTree.gss; reflexivity. 
+  econstructor; eauto. rewrite Int.add_commut; rewrite Int.add_zero; auto.
+  (* the other vars *)
+  geninv (me_vars0 id0); econstructor.
+    (* local *)
+  rewrite PTree.gso; eauto. eapply Mem.load_alloc_other; eauto.
+  rewrite OTHER; auto.
+  exploit me_bounded0; eauto. exploit Mem.alloc_result; eauto. unfold block; omega.
+  eauto. eapply val_inject_incr; eauto. 
+    (* stack scalar *)
+  rewrite PTree.gso; eauto. eapply val_inject_incr; eauto.
+    (* stack array *)
+  rewrite PTree.gso; eauto. eapply val_inject_incr; eauto.
+    (* global scalar *)
+  rewrite PTree.gso; auto. auto. 
+    (* global array *)
+  rewrite PTree.gso; auto.
+(* low high *)
+  exploit Mem.nextblock_alloc; eauto. unfold block in *; omega.
+(* bounded *)
+  exploit Mem.alloc_result; eauto. intro RES.
+  exploit Mem.nextblock_alloc; eauto. intro NEXT.
+  intros until lv0. rewrite PTree.gsspec. destruct (peq id0 id); intro EQ.
+  inv EQ. unfold block in *; omega.
+  exploit me_bounded0; eauto. unfold block in *; omega.
+(* inj *)
+  intros until lv2. repeat rewrite PTree.gsspec. 
+  exploit Mem.alloc_result; eauto. intro RES.
+  destruct (peq id1 id); destruct (peq id2 id); subst; intros A1 A2 DIFF.
+  congruence.
+  inv A1. exploit me_bounded0; eauto. unfold block; omega.
+  inv A2. exploit me_bounded0; eauto. unfold block; omega.
+  eauto.
+(* inv *)
+  intros. destruct (zeq b0 b). 
+  subst. exists id; exists lv. apply PTree.gss.
+  exploit me_inv0; eauto. rewrite <- OTHER; eauto.
+  intros [id' [lv' A]]. exists id'; exists lv'.
+  rewrite PTree.gso; auto. congruence.
+(* incr *)
+  intros. eapply me_incr0; eauto. rewrite <- OTHER; eauto.
+  exploit Mem.alloc_result; eauto. unfold block; omega.
+(* bounds *)
+  intros. rewrite PTree.gsspec in H.
+  rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). 
+  destruct (peq id0 id). 
+  inv H. apply dec_eq_true.
+  rewrite dec_eq_false. eauto. 
+  apply Mem.valid_not_valid_diff with m1.
+  exploit me_bounded0; eauto. intros [A B]. auto. 
+  eauto with mem.
+Qed.
+
+Lemma match_env_alloc_other:
+  forall f1 cenv e m1 te sp lo hi sz m2 b f2,
+  match_env f1 cenv e m1 te sp lo hi ->
+  Mem.alloc m1 0 sz = (m2, b) ->
+  inject_incr f1 f2 ->
+  (forall b', b' <> b -> f2 b' = f1 b') ->
+  hi <= b ->
+  match f2 b with None => True | Some(b',ofs) => sp < b' end ->
+  match_env f2 cenv e m2 te sp lo hi.
+Proof.
+  intros until f2; intros ME ALLOC INCR OTHER BOUND TBOUND.
+  inv ME.
+  assert (BELOW: forall id b' lv, e!id = Some(b', lv) -> b' <> b).
+    intros. exploit me_bounded0; eauto. exploit Mem.alloc_result; eauto.
+    unfold block in *; omega.
+  econstructor; eauto.
+(* vars *)
+  intros. geninv (me_vars0 id); econstructor.
+    (* local *)
+  eauto. eapply Mem.load_alloc_other; eauto.
+  rewrite OTHER; eauto. eauto. eapply val_inject_incr; eauto. 
+    (* stack scalar *)
+  eauto. eapply val_inject_incr; eauto. 
+    (* stack array *)
+  eauto. eapply val_inject_incr; eauto. 
+    (* global scalar *)
+  auto. auto. 
+    (* global array *)
+  auto.
+(* inv *)
+  intros. rewrite OTHER in H. eauto. 
+  red; intro; subst b0. rewrite H in TBOUND. omegaContradiction.
+(* incr *)
+  intros. eapply me_incr0; eauto. rewrite <- OTHER; eauto. 
+  exploit Mem.alloc_result; eauto. unfold block in *; omega.
+(* bounds *)
+  intros. rewrite (Mem.bounds_alloc_other _ _ _ _ _ ALLOC). eauto.
+  exploit me_bounded0; eauto.
+Qed.
+
+(** [match_env] and external calls *)
+
+Remark inject_incr_separated_same:
+  forall f1 f2 m1 m1',
+  inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' ->
+  forall b, Mem.valid_block m1 b -> f2 b = f1 b.
+Proof.
+  intros. case_eq (f1 b).
+  intros [b' delta] EQ. apply H; auto. 
+  intros EQ. case_eq (f2 b).
+  intros [b'1 delta1] EQ1. exploit H0; eauto. intros [C D]. contradiction.
+  auto.
+Qed.
+
+Remark inject_incr_separated_same':
+  forall f1 f2 m1 m1',
+  inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' ->
+  forall b b' delta,
+  f2 b = Some(b', delta) -> Mem.valid_block m1' b' -> f1 b = Some(b', delta).
+Proof.
+  intros. case_eq (f1 b).
+  intros [b'1 delta1] EQ. exploit H; eauto. congruence.
+  intros. exploit H0; eauto. intros [C D]. contradiction.
+Qed.
+
+Lemma match_env_external_call:
+  forall f1 cenv e m1 te sp lo hi m2 f2 m1',
+  match_env f1 cenv e m1 te sp lo hi ->
+  mem_unchanged_on (loc_unmapped f1) m1 m2 ->
+  inject_incr f1 f2 ->
+  inject_separated f1 f2 m1 m1' ->
+  (forall b, Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  hi <= Mem.nextblock m1 -> sp < Mem.nextblock m1' ->
+  match_env f2 cenv e m2 te sp lo hi.
+Proof.
+  intros until m1'. intros ME UNCHANGED INCR SEPARATED BOUNDS VALID VALID'.
+  destruct UNCHANGED as [UNCHANGED1 UNCHANGED2].
+  inversion ME. constructor; auto.
+(* vars *)
+  intros. geninv (me_vars0 id); try (econstructor; eauto; fail).
+    (* local *)
+    econstructor.
+    eauto.
+    apply UNCHANGED2; eauto.
+    rewrite <- H3. eapply inject_incr_separated_same; eauto.
+    red. exploit me_bounded0; eauto. omega. 
+    eauto. eauto.
+(* inv *)
+  intros. apply me_inv0 with delta. eapply inject_incr_separated_same'; eauto.
+(* incr *)
+  intros.
+  exploit inject_incr_separated_same; eauto. 
+  instantiate (1 := b). red; omega. intros. 
+  apply me_incr0 with b delta. congruence. auto.
+(* bounds *)
+  intros. rewrite BOUNDS; eauto. 
+  red. exploit me_bounded0; eauto. omega.
+Qed.
+
+(** * Invariant on abstract call stacks  *)
+
+(** Call stacks represent abstractly the execution state of the current
+  Csharpminor and Cminor functions, as well as the states of the
+  calling functions.  A call stack is a list of frames, each frame
+  collecting information on the current execution state of a Csharpminor
+  function and its Cminor translation. *)
+
+Inductive frame : Type :=
+  Frame(cenv: compilenv)
+       (tf: Cminor.function)
+       (e: Csharpminor.env)
+       (te: Cminor.env)
+       (sp: block)
+       (lo hi: Z).
+
+Definition callstack : Type := list frame.
+
+(** Matching of call stacks imply:
+- matching of environments for each of the frames
+- matching of the global environments
+- separation conditions over the memory blocks allocated for C#minor local variables;
+- separation conditions over the memory blocks allocated for Cminor stack data;
+- freeable permissions on the parts of the Cminor stack data blocks
+  that are not images of C#minor local variable blocks.
+*)
+
+Definition padding_freeable (f: meminj) (m: mem) (tm: mem) (sp: block) (sz: Z) : Prop :=
+  forall ofs, 
+  0 <= ofs < sz ->
+  Mem.perm tm sp ofs Freeable
+  \/ exists b, exists delta, 
+       f b = Some(sp, delta) 
+       /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta.
+
+Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
+                          callstack -> Z -> Z -> Prop :=
+  | mcs_nil:
+      forall bound tbound,
+      match_globalenvs f ->
+      match_callstack f m tm nil bound tbound 
+  | mcs_cons:
+      forall cenv tf e te sp lo hi cs bound tbound
+        (BOUND: hi <= bound)
+        (TBOUND: sp < tbound)
+        (MENV: match_env f cenv e m te sp lo hi)
+        (PERM: padding_freeable f m tm sp tf.(fn_stackspace))
+        (MCS: match_callstack f m tm cs lo sp),
+      match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) bound tbound.
+
+(** [match_callstack] implies [match_globalenvs]. *)
+
+Lemma match_callstack_match_globalenvs:
+  forall f m tm cs bound tbound,
+  match_callstack f m tm cs bound tbound ->
+  match_globalenvs f.
+Proof.
+  induction 1; eauto.
+Qed.
+
+(** We now show invariance properties for [match_callstack] that
+    generalize those for [match_env]. *)
+
+Lemma padding_freeable_invariant:
+  forall f1 m1 tm1 sp sz cenv e te lo hi f2 m2 tm2,
+  padding_freeable f1 m1 tm1 sp sz ->
+  match_env f1 cenv e m1 te sp lo hi ->
+  (forall ofs, Mem.perm tm1 sp ofs Freeable -> Mem.perm tm2 sp ofs Freeable) ->
+  (forall b, b < hi -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  (forall b, b < hi -> f2 b = f1 b) ->
+  padding_freeable f2 m2 tm2 sp sz.
+Proof.
+  intros; red; intros.
+  exploit H; eauto. intros [A | [b [delta [A B]]]].
+  left; auto. 
+  exploit me_inv; eauto. intros [id [lv C]]. 
+  exploit me_bounded; eauto. intros [D E]. 
+  right; exists b; exists delta. split.
+  rewrite H3; auto. 
+  rewrite H2; auto.
+Qed.
+
+Lemma match_callstack_store_mapped:
+  forall f m tm chunk b b' delta ofs ofs' v tv m' tm',
+  f b = Some(b', delta) ->
+  Mem.store chunk m b ofs v = Some m' ->
+  Mem.store chunk tm b' ofs' tv = Some tm' ->
+  forall cs lo hi,
+  match_callstack f m tm cs lo hi ->
+  match_callstack f m' tm' cs lo hi.
+Proof.
+  induction 4.
+  constructor; auto.
+  constructor; auto. 
+  eapply match_env_store_mapped; eauto. congruence.
+  eapply padding_freeable_invariant; eauto. 
+  intros; eauto with mem.
+  intros. eapply Mem.bounds_store; eauto.
+Qed.
+
+Lemma match_callstack_storev_mapped:
+  forall f m tm chunk a ta v tv m' tm',
+  val_inject f a ta ->
+  Mem.storev chunk m a v = Some m' ->
+  Mem.storev chunk tm ta tv = Some tm' ->
+  forall cs lo hi,
+  match_callstack f m tm cs lo hi ->
+  match_callstack f m' tm' cs lo hi.
+Proof.
+  intros. destruct a; simpl in H0; try discriminate.
+  inv H. simpl in H1. 
+  eapply match_callstack_store_mapped; eauto. 
+Qed.
+
+Lemma match_callstack_invariant:
+  forall f m tm cs bound tbound,
+  match_callstack f m tm cs bound tbound ->
+  forall m' tm',
+  (forall cenv e te sp lo hi,
+    hi <= bound ->
+    match_env f cenv e m te sp lo hi ->
+    match_env f cenv e m' te sp lo hi) ->
+  (forall b,
+    b < bound -> Mem.bounds m' b = Mem.bounds m b) ->
+  (forall b ofs p,
+    b < tbound -> Mem.perm tm b ofs p -> Mem.perm tm' b ofs p) ->
+  match_callstack f m' tm' cs bound tbound.
+Proof.
+  induction 1; intros.
+  constructor; auto.
+  constructor; auto.
+  eapply padding_freeable_invariant; eauto. 
+  intros. apply H1. omega.
   eapply IHmatch_callstack; eauto. 
-  inversion H1. omega.
+  intros. eapply H0; eauto. inv MENV; omega.
+  intros. apply H1; auto. inv MENV; omega. 
+  intros. apply H2; auto. omega. 
 Qed.
 
 Lemma match_callstack_store_local:
-  forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv,
+  forall f cenv e te sp lo hi cs bound tbound m1 m2 tm tf id b chunk v tv,
   e!id = Some(b, Vscalar chunk) ->
+  Val.has_type v (type_of_chunk chunk) ->
   val_inject f (Val.load_result chunk v) tv ->
-  store chunk m1 b 0 v = Some m2 ->
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 ->
-  match_callstack f (mkframe cenv e (PTree.set id tv te) sp lo hi :: cs) bound tbound m2.
+  Mem.store chunk m1 b 0 v = Some m2 ->
+  match_callstack f m1 tm (Frame cenv tf e te sp lo hi :: cs) bound tbound ->
+  match_callstack f m2 tm (Frame cenv tf e (PTree.set id tv te) sp lo hi :: cs) bound tbound.
 Proof.
-  intros. inversion H2. constructor; auto.
+  intros. inv H3. constructor; auto.
   eapply match_env_store_local; eauto.
-  eapply match_callstack_store_above; eauto.
-  inversion H16. 
-  generalize (me_bounded0 _ _ _ H). omega.
+  eapply padding_freeable_invariant; eauto.
+  intros. eapply Mem.bounds_store; eauto.
+  eapply match_callstack_invariant; eauto.
+  intros. apply match_env_invariant with m1; auto.
+  intros. rewrite <- H6. eapply Mem.load_store_other; eauto. 
+  left. inv MENV. exploit me_bounded0; eauto. unfold block in *; omega. 
+  intros. eapply Mem.bounds_store; eauto.
+  intros. eapply Mem.bounds_store; eauto.
 Qed.
 
 (** A variant of [match_callstack_store_local] where the Cminor environment
@@ -387,436 +884,385 @@ Qed.
   In this case, [match_callstack] is preserved even if no assignment
   takes place on the Cminor side. *)
 
-Lemma match_env_extensional:
-  forall f cenv e m te1 sp lo hi,
-  match_env f cenv e m te1 sp lo hi ->
-  forall te2,
-  (forall id, te2!id = te1!id) ->
-  match_env f cenv e m te2 sp lo hi.
-Proof.
-  induction 1; intros; econstructor; eauto.
-  intros. generalize (me_vars0 id); intro. 
-  inversion H0; econstructor; eauto.
-  rewrite H. auto.
-Qed.
-
 Lemma match_callstack_store_local_unchanged:
-  forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv,
+  forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv tf tm,
   e!id = Some(b, Vscalar chunk) ->
+  Val.has_type v (type_of_chunk chunk) ->
   val_inject f (Val.load_result chunk v) tv ->
-  store chunk m1 b 0 v = Some m2 ->
+  Mem.store chunk m1 b 0 v = Some m2 ->
   te!id = Some tv ->
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 ->
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m2.
+  match_callstack f m1 tm (Frame cenv tf e te sp lo hi :: cs) bound tbound ->
+  match_callstack f m2 tm (Frame cenv tf e te sp lo hi :: cs) bound tbound.
 Proof.
-  intros. inversion H3. constructor; auto.
-  apply match_env_extensional with (PTree.set id tv te).
-  eapply match_env_store_local; eauto.
+  intros. exploit match_callstack_store_local; eauto. intro MCS.
+  inv MCS. constructor; auto. eapply match_env_extensional; eauto. 
   intros. rewrite PTree.gsspec. 
   case (peq id0 id); intros. congruence. auto.
-  eapply match_callstack_store_above; eauto.
-  inversion H17. 
-  generalize (me_bounded0 _ _ _ H). omega.
 Qed.
 
-(** Preservation of [match_callstack] by freeing all blocks allocated
-  for local variables at function entry (on the Csharpminor side). *)
-
 Lemma match_callstack_incr_bound:
-  forall f cs bound tbound m,
-  match_callstack f cs bound tbound m ->
-  forall bound' tbound',
+  forall f m tm cs bound tbound bound' tbound',
+  match_callstack f m tm cs bound tbound ->
   bound <= bound' -> tbound <= tbound' ->
-  match_callstack f cs bound' tbound' m.
+  match_callstack f m tm cs bound' tbound'.
 Proof.
   intros. inversion H; constructor; auto. omega. omega.
 Qed.
 
-Lemma load_freelist:
-  forall fbl chunk m b ofs,
-  (forall b', In b' fbl -> b' <> b) -> 
-  load chunk (free_list m fbl) b ofs = load chunk m b ofs.
-Proof.
-  induction fbl; simpl; intros.
-  auto.
-  rewrite load_free. apply IHfbl. 
-  intros. apply H. tauto.
-  apply sym_not_equal. apply H. tauto.
-Qed.
-
-Lemma match_env_freelist:
-  forall f cenv e m te sp lo hi fbl,
-  match_env f cenv e m te sp lo hi ->
-  (forall b, In b fbl -> hi <= b) ->
-  match_env f cenv e (free_list m fbl) te sp lo hi.
-Proof.
-  intros. inversion H. econstructor; eauto.
-  intros. generalize (me_vars0 id); intro. 
-  inversion H1; econstructor; eauto.
-  rewrite <- H4. apply load_freelist. 
-  intros. generalize (H0 _ H8); intro. 
-  generalize (me_bounded0 _ _ _ H3). unfold block; omega.
-Qed.  
-
-Lemma match_callstack_freelist_rec:
-  forall f cs bound tbound m,
-  match_callstack f cs bound tbound m ->
-  forall fbl,
-  (forall b, In b fbl -> bound <= b) ->
-  match_callstack f cs bound tbound (free_list m fbl).
-Proof.
-  induction 1; intros; constructor; auto.
-  eapply match_env_freelist; eauto. 
-  intros. generalize (H3 _ H4). omega.
-  apply IHmatch_callstack. intros. 
-  generalize (H3 _ H4). inversion H1. omega. 
-Qed.
-
-Lemma blocks_of_env_charact:
-  forall b e,
-  In b (blocks_of_env e) <->
-  exists id, exists lv, e!id = Some(b, lv).
-Proof.
-  unfold blocks_of_env.
-  set (f := fun id_b_lv : positive * (block * var_kind) =>
-      let (_, y) := id_b_lv in let (b0, _) := y in b0).
-  intros; split; intros.
-  exploit list_in_map_inv; eauto. intros [[id [b' lv]] [A B]].
-  simpl in A. subst b'. exists id; exists lv. apply PTree.elements_complete. auto.
-  destruct H as [id [lv EQ]].
-  change b with (f (id, (b, lv))). apply List.in_map.
-  apply PTree.elements_correct. auto.
-Qed.
-
-Lemma match_callstack_freelist:
-  forall f cenv e te sp lo hi cs bound tbound m tm,
-  mem_inject f m tm ->
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m ->
-  match_callstack f cs bound tbound (free_list m (blocks_of_env e))
-  /\ mem_inject f (free_list m (blocks_of_env e)) (free tm sp).
-Proof.
-  intros. inv H0. inv H14. split.
-  apply match_callstack_incr_bound with lo sp.
-  apply match_callstack_freelist_rec. auto.
-  intros. rewrite blocks_of_env_charact in H0. 
-  destruct H0 as [id [lv EQ]]. exploit me_bounded0; eauto. omega.
-  omega. omega.
-  apply Mem.free_inject; auto.
-  intros. rewrite blocks_of_env_charact. eauto.
-Qed.
-
-(** Preservation of [match_callstack] when allocating a block for
-  a local variable on the Csharpminor side.  *)
+(** Preservation of [match_callstack] by freeing all blocks allocated
+  for local variables at function entry (on the Csharpminor side)
+  and simultaneously freeing the Cminor stack data block. *)
 
-Lemma load_from_alloc_is_undef:
-  forall m1 chunk m2 b,
-  alloc m1 0 (size_chunk chunk) = (m2, b) ->
-  load chunk m2 b 0 = Some Vundef.
+Lemma in_blocks_of_env:
+  forall e id b lv,
+  e!id = Some(b, lv) -> In (b, 0, sizeof lv) (blocks_of_env e).
 Proof.
-  intros.
-  assert (exists v, load chunk m2 b 0 = Some v).
-    apply valid_access_load.
-    eapply valid_access_alloc_same; eauto. omega. omega. apply Zdivide_0.
-  destruct H0 as [v LOAD]. rewrite LOAD. decEq. 
-  eapply load_alloc_same; eauto.
+  unfold blocks_of_env; intros. 
+  change (b, 0, sizeof lv) with (block_of_binding (id, (b, lv))).
+  apply List.in_map. apply PTree.elements_correct. auto.
 Qed.
 
-Lemma match_env_alloc_same:
-  forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data tv,
-  alloc m1 0 (sizeof lv) = (m2, b) ->
-  match info with
-    | Var_local chunk => data = None /\ lv = Vscalar chunk
-    | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk
-    | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz
-    | Var_global_scalar chunk => False
-    | Var_global_array => False
-  end ->
-  match_env f1 cenv1 e1 m1 te sp lo m1.(nextblock) ->
-  te!id = Some tv ->
-  e1!id = None ->
-  let f2 := extend_inject b data f1 in
-  let cenv2 := PMap.set id info cenv1 in
-  let e2 := PTree.set id (b, lv) e1 in
-  inject_incr f1 f2 ->
-  match_env f2 cenv2 e2 m2 te sp lo m2.(nextblock).
+Lemma in_blocks_of_env_inv:
+  forall b lo hi e,
+  In (b, lo, hi) (blocks_of_env e) ->
+  exists id, exists lv, e!id = Some(b, lv) /\ lo = 0 /\ hi = sizeof lv.
 Proof.
-  intros. 
-  assert (b = m1.(nextblock)).
-    injection H; intros. auto.
-  assert (m2.(nextblock) = Zsucc m1.(nextblock)).
-    injection H; intros. rewrite <- H7; reflexivity.
-  inversion H1. constructor.
-  (* me_vars *)
-  intros id0. unfold cenv2. rewrite PMap.gsspec. case (peq id0 id); intros.
-    (* same var *)
-    subst id0. destruct info.
-      (* info = Var_local chunk *)
-      elim H0; intros.
-      apply match_var_local with b Vundef tv.
-      unfold e2; rewrite PTree.gss. congruence.
-      eapply load_from_alloc_is_undef; eauto. 
-      rewrite H8 in H. unfold sizeof in H. eauto.
-      unfold f2, extend_inject, eq_block. rewrite zeq_true. auto.
-      auto.
-      constructor.
-      (* info = Var_stack_scalar chunk ofs *)
-      elim H0; intros.
-      apply match_var_stack_scalar with b. 
-      unfold e2; rewrite PTree.gss. congruence.
-      eapply val_inject_ptr. 
-      unfold f2, extend_inject, eq_block. rewrite zeq_true. eauto.
-      rewrite Int.add_commut. rewrite Int.add_zero. auto.
-      (* info = Var_stack_array z *)
-      elim H0; intros A [sz B].
-      apply match_var_stack_array with sz b.
-      unfold e2; rewrite PTree.gss. congruence.
-      eapply val_inject_ptr. 
-      unfold f2, extend_inject, eq_block. rewrite zeq_true. eauto.
-      rewrite Int.add_commut. rewrite Int.add_zero. auto.
-      (* info = Var_global *)
-      contradiction.
-      contradiction.
-    (* other vars *)
-    generalize (me_vars0 id0); intros.
-    inversion H7.
-    eapply match_var_local with (v := v); eauto.
-      unfold e2; rewrite PTree.gso; eauto.
-      eapply load_alloc_other; eauto. 
-      unfold f2, extend_inject, eq_block; rewrite zeq_false; auto.
-      generalize (me_bounded0 _ _ _ H9). unfold block in *; omega.
-    econstructor; eauto.
-      unfold e2; rewrite PTree.gso; eauto.
-    econstructor; eauto. 
-      unfold e2; rewrite PTree.gso; eauto. 
-    econstructor; eauto.
-      unfold e2; rewrite PTree.gso; eauto.
-    econstructor; eauto. 
-      unfold e2; rewrite PTree.gso; eauto. 
-  (* lo <= hi *)
-  unfold block in *; omega.
-  (* me_bounded *)
-  intros until lv0. unfold e2; rewrite PTree.gsspec. 
-  case (peq id0 id); intros.
-  subst id0. inversion H7. subst b0. unfold block in *; omega. 
-  generalize (me_bounded0 _ _ _ H7). rewrite H6. omega.
-  (* me_inj *)
-  intros until lv2. unfold e2; repeat rewrite PTree.gsspec.
-  case (peq id1 id); case (peq id2 id); intros.
-  congruence.
-  inversion H7. subst b1. rewrite H5. 
-    generalize (me_bounded0 _ _ _ H8). unfold block; omega.
-  inversion H8. subst b2. rewrite H5.
-    generalize (me_bounded0 _ _ _ H7). unfold block; omega.
-  eauto.
-  (* me_inv *)
-  intros until delta. unfold f2, extend_inject, eq_block.
-  case (zeq b0 b); intros.
-  subst b0. exists id; exists lv. unfold e2. apply PTree.gss.
-  exploit me_inv0; eauto. intros [id' [lv' EQ]].
-  exists id'; exists lv'. unfold e2. rewrite PTree.gso; auto.
-  congruence.
-  (* me_incr *)
-  intros until delta. unfold f2, extend_inject, eq_block.
-  case (zeq b0 b); intros.
-  subst b0. unfold block in *; omegaContradiction.
-  eauto.
+  unfold blocks_of_env; intros. 
+  exploit list_in_map_inv; eauto. intros [[id [b' lv]] [A B]].
+  unfold block_of_binding in A. inv A. 
+  exists id; exists lv; intuition. apply PTree.elements_complete. auto.
 Qed.
 
-Lemma match_env_alloc_other:
-  forall f1 cenv e m1 m2 te sp lo hi chunk b data,
-  alloc m1 0 (sizeof chunk) = (m2, b) ->
-  match data with None => True | Some (b', delta') => sp < b' end ->
-  hi <= m1.(nextblock) ->
-  match_env f1 cenv e m1 te sp lo hi ->
-  let f2 := extend_inject b data f1 in
-  inject_incr f1 f2 ->
-  match_env f2 cenv e m2 te sp lo hi.
+(*
+Lemma free_list_perm:
+  forall l m m',
+  Mem.free_list m l = Some m' ->
+  forall b ofs p,
+  Mem.perm m' b ofs p -> Mem.perm m b ofs p.
 Proof.
-  intros. 
-  assert (b = m1.(nextblock)). injection H; auto.
-  rewrite <- H4 in H1.
-  inversion H2. constructor; auto.
-  (* me_vars *)
-  intros. generalize (me_vars0 id); intro. 
-  inversion H5.
-  eapply match_var_local with (v := v); eauto.
-    eapply load_alloc_other; eauto.
-    unfold f2, extend_inject, eq_block. rewrite zeq_false. auto.
-    generalize (me_bounded0 _ _ _ H7). unfold block in *; omega.
-  econstructor; eauto.
-  econstructor; eauto.
-  econstructor; eauto.
-  econstructor; eauto.
-  (* me_bounded *)
-  intros until delta. unfold f2, extend_inject, eq_block.
-  case (zeq b0 b); intros. rewrite H5 in H0. omegaContradiction.
-  eauto.
-  (* me_incr *)
-  intros until delta. unfold f2, extend_inject, eq_block.
-  case (zeq b0 b); intros. subst b0. omegaContradiction.
-  eauto.
+  induction l; simpl; intros. 
+  inv H; auto.
+  revert H. destruct a as [[b' lo'] hi'].
+  caseEq (Mem.free m b' lo' hi'); try congruence.
+  intros m1 FREE1 FREE2.
+  eauto with mem. 
 Qed.
+*)
 
-Lemma match_callstack_alloc_other:
-  forall f1 cs bound tbound m1,
-  match_callstack f1 cs bound tbound m1 ->
-  forall lv m2 b data,
-  alloc m1 0 (sizeof lv) = (m2, b) ->
-  match data with None => True | Some (b', delta') => tbound <= b' end ->
-  bound <= m1.(nextblock) ->
-  let f2 := extend_inject b data f1 in
+Lemma match_callstack_freelist:
+  forall f cenv tf e te sp lo hi cs m m' tm,
+  Mem.inject f m tm ->
+  Mem.free_list m (blocks_of_env e) = Some m' ->
+  match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
+  exists tm',
+  Mem.free tm sp 0 tf.(fn_stackspace) = Some tm'
+  /\ match_callstack f m' tm' cs (Mem.nextblock m') (Mem.nextblock tm')
+  /\ Mem.inject f m' tm'.
+Proof.
+  intros until tm; intros INJ FREELIST MCS. inv MCS. inv MENV.
+  assert ({tm' | Mem.free tm sp 0 (fn_stackspace tf) = Some tm'}).
+  apply Mem.range_perm_free.
+  red; intros.
+  exploit PERM; eauto. intros [A | [b [delta [A B]]]].
+  auto.
+  exploit me_inv0; eauto. intros [id [lv C]]. 
+  exploit me_bounds0; eauto. intro D. rewrite D in B; simpl in B.
+  assert (Mem.range_perm m b 0 (sizeof lv) Freeable). 
+  eapply free_list_freeable; eauto. eapply in_blocks_of_env; eauto.
+  replace ofs with ((ofs - delta) + delta) by omega. 
+  eapply Mem.perm_inject; eauto. apply H0. omega. 
+  destruct X as  [tm' FREE].
+  exploit nextblock_freelist; eauto. intro NEXT.
+  exploit Mem.nextblock_free; eauto. intro NEXT'.
+  exists tm'. split. auto. split.
+  rewrite NEXT; rewrite NEXT'.
+  apply match_callstack_incr_bound with lo sp; try omega.
+  apply match_callstack_invariant with m tm; auto.
+  intros. apply match_env_invariant with m; auto.
+  intros. rewrite <- H2. eapply load_freelist; eauto. 
+  intros. exploit in_blocks_of_env_inv; eauto. 
+  intros [id [lv [A [B C]]]]. 
+  exploit me_bounded0; eauto. unfold block; omega.
+  intros. eapply bounds_freelist; eauto.
+  intros. eapply bounds_freelist; eauto.
+  intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega.
+  eapply Mem.free_inject; eauto.
+  intros. exploit me_inv0; eauto. intros [id [lv A]]. 
+  exists 0; exists (sizeof lv); split.
+  eapply in_blocks_of_env; eauto.
+  exploit me_bounds0; eauto. intro B. 
+  exploit Mem.perm_in_bounds; eauto. rewrite B; simpl. auto.
+Qed.
+
+(** Preservation of [match_callstack] by allocations. *)
+
+Lemma match_callstack_alloc_below:
+  forall f1 m1 tm sz m2 b f2,
+  Mem.alloc m1 0 sz = (m2, b) ->
   inject_incr f1 f2 ->
-  match_callstack f2 cs bound tbound m2.
+  (forall b', b' <> b -> f2 b' = f1 b') ->
+  forall cs bound tbound,
+  match_callstack f1 m1 tm cs bound tbound ->
+  bound <= b ->
+  match f2 b with None => True | Some(b',ofs) => tbound <= b' end ->
+  match_callstack f2 m2 tm cs bound tbound.
 Proof.
-  induction 1; intros.
+  induction 4; intros.
   constructor. 
-    inversion H. constructor. 
-    intros. auto.
-    intros. elim (mg_symbols0 _ _ H4); intros.
-    split; auto. elim (H3 b0); intros; congruence.
-    intros. generalize (mg_functions0 _ H4). elim (H3 b0); congruence.
-  constructor. auto. auto. 
-  unfold f2; eapply match_env_alloc_other; eauto. 
-  destruct data; auto. destruct p. omega. omega. 
-  unfold f2; eapply IHmatch_callstack; eauto. 
-  destruct data; auto. destruct p. omega. 
-  inversion H1; omega.
+  inv H2. constructor. 
+  intros. exploit mg_symbols0; eauto. intros [A B]. auto. 
+  intros. rewrite H1; auto. 
+  exploit Mem.alloc_result; eauto. 
+  generalize (Mem.nextblock_pos m1).
+  unfold block; omega.
+  constructor; auto.
+  eapply match_env_alloc_other; eauto. omega. destruct (f2 b); auto. destruct p; omega.
+  eapply padding_freeable_invariant; eauto. 
+  intros. eapply Mem.bounds_alloc_other; eauto. unfold block; omega.
+  intros. apply H1. unfold block; omega.
+  apply IHmatch_callstack. 
+  inv MENV; omega. 
+  destruct (f2 b); auto. destruct p; omega. 
 Qed.
 
 Lemma match_callstack_alloc_left:
-  forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data cs tv tbound,
-  alloc m1 0 (sizeof lv) = (m2, b) ->
-  match info with
-    | Var_local chunk => data = None /\ lv = Vscalar chunk
-    | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk
-    | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz
-    | Var_global_scalar chunk => False
-    | Var_global_array => False
-  end ->
-  match_callstack f1 (mkframe cenv1 e1 te sp lo m1.(nextblock) :: cs) m1.(nextblock) tbound m1 ->
-  te!id = Some tv ->
-  e1!id = None ->
-  let f2 := extend_inject b data f1 in
-  let cenv2 := PMap.set id info cenv1 in
-  let e2 := PTree.set id (b, lv) e1 in
+  forall f1 m1 tm cenv tf e te sp lo cs lv m2 b f2 info id tv,
+  match_callstack f1 m1 tm
+    (Frame cenv tf e te sp lo (Mem.nextblock m1) :: cs)
+    (Mem.nextblock m1) (Mem.nextblock tm) ->
+  Mem.alloc m1 0 (sizeof lv) = (m2, b) ->
   inject_incr f1 f2 ->
-  match_callstack f2 (mkframe cenv2 e2 te sp lo m2.(nextblock) :: cs) m2.(nextblock) tbound m2.
-Proof.
-  intros. inversion H1. constructor. omega. auto.
-  unfold f2, cenv2, e2. eapply match_env_alloc_same; eauto.
-  unfold f2; eapply match_callstack_alloc_other; eauto. 
-  destruct info.
-  elim H0; intros. rewrite H20. auto.
-  elim H0; intros. rewrite H20. omega.
-  elim H0; intros. rewrite H20. omega.
-  contradiction.
-  contradiction.
-  inversion H18; omega. 
+  alloc_condition info lv sp (f2 b) ->
+  (forall b', b' <> b -> f2 b' = f1 b') ->
+  te!id = Some tv ->
+  e!id = None ->
+  match_callstack f2 m2 tm
+    (Frame (PMap.set id info cenv) tf (PTree.set id (b, lv) e) te sp lo (Mem.nextblock m2) :: cs)
+    (Mem.nextblock m2) (Mem.nextblock tm).
+Proof.
+  intros until tv; intros MCS ALLOC INCR ACOND OTHER TE E.
+  inv MCS. 
+  exploit Mem.alloc_result; eauto. intro RESULT.
+  exploit Mem.nextblock_alloc; eauto. intro NEXT.
+  constructor.
+  omega. auto. 
+  eapply match_env_alloc_same; eauto.
+  eapply padding_freeable_invariant; eauto. 
+  intros. eapply Mem.bounds_alloc_other; eauto. unfold block in *; omega.
+  intros. apply OTHER. unfold block in *; omega. 
+  eapply match_callstack_alloc_below; eauto.
+  inv MENV. unfold block in *; omega.
+  inv ACOND. auto. omega. omega.
 Qed.
 
 Lemma match_callstack_alloc_right:
-  forall f cs bound tm1 m tm2 lo hi b,
-  alloc tm1 lo hi = (tm2, b) ->
-  match_callstack f cs bound tm1.(nextblock) m ->
-  match_callstack f cs bound tm2.(nextblock) m.
-Proof.
-  intros. eapply match_callstack_incr_bound; eauto. omega.
-  injection H; intros. rewrite <- H2; simpl. omega.
-Qed.
-
-Lemma match_env_alloc:
-  forall m1 l h m2 b tm1 tm2 tb f1 ce e te sp lo hi,
-  alloc m1 l h = (m2, b) ->
-  alloc tm1 l h = (tm2, tb) ->
-  match_env f1 ce e m1 te sp lo hi ->
-  hi <= m1.(nextblock) ->
-  sp < tm1.(nextblock) ->
-  let f2 := extend_inject b (Some(tb, 0)) f1 in
-  inject_incr f1 f2 ->
-  match_env f2 ce e m2 te sp lo hi.
+  forall f m tm cs tf sp tm' te,
+  match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) ->
+  Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) ->
+  Mem.inject f m tm ->
+  match_callstack f m tm'
+    (Frame gce tf empty_env te sp (Mem.nextblock m) (Mem.nextblock m) :: cs)
+    (Mem.nextblock m) (Mem.nextblock tm').
 Proof.
+  intros.
+  exploit Mem.alloc_result; eauto. intro RES.
+  exploit Mem.nextblock_alloc; eauto. intro NEXT.
+  constructor. omega. unfold block in *; omega.
+(* match env *) 
+  constructor.
+(* vars *)
+  intros. generalize (global_compilenv_charact id); intro. 
+  destruct (gce!!id); try contradiction. 
+  constructor. apply PTree.gempty. auto.
+  constructor. apply PTree.gempty. 
+(* low high *)
+  omega.
+(* bounded *)
+  intros. rewrite PTree.gempty in H2. congruence.
+(* inj *)
+  intros. rewrite PTree.gempty in H2. congruence.
+(* inv *)
   intros. 
-  assert (BEQ: b = m1.(nextblock)). injection H; auto.
-  assert (TBEQ: tb = tm1.(nextblock)). injection H0; auto.
-  inversion H1. constructor; auto.
-  (* me_vars *)
-  intros. generalize (me_vars0 id); intro. inversion H5.
-    (* var_local *)
-    eapply match_var_local with (v := v); eauto.
-    eapply load_alloc_other; eauto. 
-    generalize (me_bounded0 _ _ _ H7). intro. 
-    unfold f2, extend_inject. case (zeq b0 b); intro. 
-    subst b0. rewrite BEQ in H12. omegaContradiction. 
-    auto.
-    (* var_stack_scalar *)
-    econstructor; eauto.
-    (* var_stack_array *)
-    econstructor; eauto.
-    (* var_global_scalar *)
-    econstructor; eauto.
-    (* var_global_array *)
-    econstructor; eauto.
-  (* me_bounded *)
-  intros until delta. unfold f2, extend_inject. case (zeq b0 b); intro.
-  intro. injection H5; clear H5; intros. 
-  rewrite H6 in TBEQ. rewrite TBEQ in H3. omegaContradiction.
-  eauto.
-  (* me_inj *)
-  intros until delta. unfold f2, extend_inject. case (zeq b0 b); intros.
-  injection H5; clear H5; intros; subst b0 tb0 delta.
-  rewrite BEQ in H6. omegaContradiction. 
-  eauto.
-Qed.
-
-Lemma match_callstack_alloc_rec:
-  forall f1 cs bound tbound m1,
-  match_callstack f1 cs bound tbound m1 ->
-  forall l h m2 b tm1 tm2 tb,
-  alloc m1 l h = (m2, b) ->
-  alloc tm1 l h = (tm2, tb) ->
-  bound <= m1.(nextblock) ->
-  tbound <= tm1.(nextblock) ->
-  let f2 := extend_inject b (Some(tb, 0)) f1 in
-  inject_incr f1 f2 ->
-  match_callstack f2 cs bound tbound m2.
+  assert (sp <> sp). apply Mem.valid_not_valid_diff with tm.
+  eapply Mem.valid_block_inject_2; eauto. eauto with mem. 
+  tauto.
+(* incr *)
+  intros. rewrite RES. change (Mem.valid_block tm tb).
+  eapply Mem.valid_block_inject_2; eauto.
+(* bounds *)
+  unfold empty_env; intros. rewrite PTree.gempty in H2. congruence.
+(* padding freeable *)
+  red; intros. left. eapply Mem.perm_alloc_2; eauto. 
+(* previous call stack *)
+  rewrite RES. apply match_callstack_invariant with m tm; auto.
+  intros. eapply Mem.perm_alloc_1; eauto. 
+Qed.
+
+(** Decidability of the predicate "this is not a padding location" *)
+
+Definition is_reachable (f: meminj) (m: mem) (sp: block) (ofs: Z) : Prop :=
+  exists b, exists delta, 
+  f b = Some(sp, delta)
+  /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta.
+
+Lemma is_reachable_dec:
+  forall f cenv e m te sp lo hi ofs,
+  match_env f cenv e m te sp lo hi ->
+  {is_reachable f m sp ofs} + {~is_reachable f m sp ofs}.
 Proof.
-  induction 1; intros.
-  constructor. 
-    inversion H. constructor.
-    intros. elim (mg_symbols0 _ _ H5); intros.
-    split; auto. elim (H4 b0); intros; congruence.
-    intros. generalize (mg_functions0 _ H5). elim (H4 b0); congruence.
-  constructor. auto. auto. 
-  unfold f2. eapply match_env_alloc; eauto. omega. omega. 
-  unfold f2; eapply IHmatch_callstack; eauto.
-  inversion H1; omega.
-  omega.
-Qed.
-
-Lemma match_callstack_alloc:
-  forall f1 cs m1 tm1 l h m2 b tm2 tb,
-  match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1 ->
-  alloc m1 l h = (m2, b) ->
-  alloc tm1 l h = (tm2, tb) ->
-  let f2 := extend_inject b (Some(tb, 0)) f1 in
+  intros.
+  set (P := fun (b: block) =>
+       match f b with
+       | None => False
+       | Some(b', delta) =>
+           b' = sp /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta
+       end).
+  assert ({forall b, Intv.In b (lo, hi) -> ~P b} + {exists b, Intv.In b (lo, hi) /\ P b}).
+  apply Intv.forall_dec. intro b. unfold P. 
+  destruct (f b) as [[b' delta] | ]. 
+  destruct (eq_block b' sp).
+  destruct (zle (Mem.low_bound m b + delta) ofs).
+  destruct (zlt ofs (Mem.high_bound m b + delta)).
+  right; auto.
+  left; intuition.
+  left; intuition.
+  left; intuition.
+  left; intuition.
+  inv H. destruct H0.
+  right; red; intros [b [delta [A [B C]]]].
+  elim (n b). 
+  exploit me_inv0; eauto. intros [id [lv D]]. exploit me_bounded0; eauto. 
+  red. rewrite A. auto. 
+  left. destruct e0 as [b [A B]]. red in B; revert B.
+  case_eq (f b). intros [b' delta] EQ [C [D E]]. subst b'. 
+  exists b; exists delta. auto. 
+  tauto. 
+Qed.
+
+(** Preservation of [match_callstack] by external calls. *)
+
+Lemma match_callstack_external_call:
+  forall f1 f2 m1 m2 m1' m2',
+  mem_unchanged_on (loc_unmapped f1) m1 m2 ->
+  mem_unchanged_on (loc_out_of_reach f1 m1) m1' m2' ->
   inject_incr f1 f2 ->
-  match_callstack f2 cs m2.(nextblock) tm2.(nextblock) m2.
+  inject_separated f1 f2 m1 m1' ->
+  (forall b, Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  forall cs bound tbound,
+  match_callstack f1 m1 m1' cs bound tbound ->
+  bound <= Mem.nextblock m1 -> tbound <= Mem.nextblock m1' ->
+  match_callstack f2 m2 m2' cs bound tbound.
+Proof.
+  intros until m2'. 
+  intros UNMAPPED OUTOFREACH INCR SEPARATED BOUNDS.
+  destruct OUTOFREACH as [OUTOFREACH1 OUTOFREACH2].
+  induction 1; intros; constructor.
+(* base case *)
+  constructor; intros. 
+  exploit mg_symbols; eauto. intros [A B]. auto.
+  replace (f2 b) with (f1 b). eapply mg_functions; eauto.
+  symmetry. eapply inject_incr_separated_same; eauto. 
+  red. generalize (Mem.nextblock_pos m1); omega.
+(* inductive case *)
+  auto. auto. 
+  eapply match_env_external_call; eauto. omega. omega. 
+  (* padding-freeable *)
+  red; intros.
+  destruct (is_reachable_dec _ _ _ _ _ _ _ _ ofs MENV).
+  destruct i as [b [delta [A B]]].
+  right; exists b; exists delta; split.
+  apply INCR; auto. rewrite BOUNDS. auto. 
+  exploit me_inv; eauto. intros [id [lv C]].
+  exploit me_bounded; eauto. intros. red; omega.
+  exploit PERM; eauto. intros [A|A]; try contradiction. left.
+  apply OUTOFREACH1; auto. red; intros. 
+  assert ((ofs < Mem.low_bound m1 b0 + delta \/ ofs >= Mem.high_bound m1 b0 + delta)
+          \/ Mem.low_bound m1 b0 + delta <= ofs < Mem.high_bound m1 b0 + delta)
+  by omega. destruct H4; auto.
+  elim n. exists b0; exists delta; auto.
+  (* induction *)
+  eapply IHmatch_callstack; eauto. inv MENV; omega. omega.
+Qed.
+
+Remark external_call_nextblock_incr:
+  forall ef vargs m1 t vres m2,
+  external_call ef vargs m1 t vres m2 ->
+  Mem.nextblock m1 <= Mem.nextblock m2.
 Proof.
-  intros. unfold f2 in *. 
-  apply match_callstack_incr_bound with m1.(nextblock) tm1.(nextblock).
-  eapply match_callstack_alloc_rec; eauto. omega. omega. 
-  injection H0; intros; subst m2; simpl; omega. 
-  injection H1; intros; subst tm2; simpl; omega. 
+  intros. 
+  generalize (external_call_valid_block _ _ _ _ _ _ (Mem.nextblock m1 - 1) H).
+  unfold Mem.valid_block. omega. 
 Qed.
 
-(** [match_callstack] implies [match_globalenvs]. *)
+(** * Soundness of chunk and type inference. *)
 
-Lemma match_callstack_match_globalenvs:
-  forall f cs bound tbound m,
-  match_callstack f cs bound tbound m ->
-  match_globalenvs f.
+Lemma load_normalized:
+  forall chunk m b ofs v,
+  Mem.load chunk m b ofs = Some v -> val_normalized v chunk.
 Proof.
-  induction 1; eauto.
+  intros. 
+  exploit Mem.load_type; eauto. intro TY.
+  exploit Mem.load_cast; eauto. intro CST.
+  red. destruct chunk; destruct v; simpl in *; auto; contradiction.
+Qed.
+
+Lemma chunktype_expr_correct:
+  forall f m tm cenv tf e te sp lo hi cs bound tbound,
+  match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) bound tbound ->
+  forall a v,
+  Csharpminor.eval_expr gve e m a v ->
+  forall chunk (CTE: chunktype_expr cenv a = OK chunk),
+  val_normalized v chunk.
+Proof.
+  intros until tbound; intro MCS. induction 1; intros; try (monadInv CTE).
+(* var *)
+  assert (chunk0 = chunk).
+    unfold chunktype_expr in CTE. 
+    inv MCS. inv MENV. generalize (me_vars0 id); intro MV.
+    inv MV; rewrite <- H1 in CTE; monadInv CTE; inv H; try congruence.
+    unfold gve in H6. simpl in H6. congruence.
+  subst chunk0.
+  inv H; exploit load_normalized; eauto. unfold val_normalized; auto.
+(* const *)
+  eapply chunktype_const_correct; eauto.
+(* unop *)
+  eapply chunktype_unop_correct; eauto.
+(* binop *)
+  eapply chunktype_binop_correct; eauto.
+(* load *)
+  destruct v1; simpl in H0; try discriminate. 
+  eapply load_normalized; eauto.
+(* cond *)
+  eapply chunktype_merge_correct; eauto. 
+  destruct vb1; eauto.
+Qed.
+
+Lemma type_expr_correct:
+  forall f m tm cenv tf e te sp lo hi cs bound tbound,
+  match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) bound tbound ->
+  forall a v ty,
+  Csharpminor.eval_expr gve e m a v ->
+  type_expr cenv a = OK ty ->
+  Val.has_type v ty.
+Proof.
+  intros. monadInv H1. apply val_normalized_has_type. 
+  eapply chunktype_expr_correct; eauto.
+Qed.
+
+Lemma type_exprlist_correct:
+  forall f m tm cenv tf e te sp lo hi cs bound tbound,
+  match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) bound tbound ->
+  forall al vl tyl,
+  Csharpminor.eval_exprlist gve e m al vl ->
+  type_exprlist cenv al = OK tyl ->
+  Val.has_type_list vl tyl.
+Proof.
+  intros. monadInv H1. 
+  generalize al vl H0 tyl H2. induction 1; intros.
+  inv H3. simpl. auto.
+  inv H5. simpl. split.
+  eapply type_expr_correct; eauto.
+  auto.
 Qed.
 
 (** * Correctness of Cminor construction functions *)
@@ -910,7 +1356,7 @@ Lemma eval_binop_compat:
   Csharpminor.eval_binop op v1 v2 m = Some v ->
   val_inject f v1 tv1 ->
   val_inject f v2 tv2 ->
-  mem_inject f m tm ->
+  Mem.inject f m tm ->
   exists tv,
      Cminor.eval_binop op tv1 tv2 = Some tv
   /\ val_inject f v tv.
@@ -924,8 +1370,8 @@ Proof.
     destruct (eq_block b1 b0); inv H4. 
     assert (b3 = b2) by congruence. subst b3. 
     unfold eq_block; rewrite zeq_true. TrivialOp.
-    replace x0 with x by congruence. decEq. decEq. 
-    apply Int.sub_shifted.
+    replace delta0 with delta by congruence.
+    decEq. decEq. apply Int.sub_shifted.
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
     destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
@@ -952,28 +1398,28 @@ Proof.
     exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
     exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
   (* cmp ptr ptr *)
-  caseEq (valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b0 (Int.signed ofs0)); 
+  caseEq (Mem.valid_pointer m b1 (Int.signed ofs1) && Mem.valid_pointer m b0 (Int.signed ofs0)); 
   intro EQ; rewrite EQ in H4; try discriminate.
   elim (andb_prop _ _ EQ); intros.
   destruct (eq_block b1 b0); inv H4.
   (* same blocks in source *)
   assert (b3 = b2) by congruence. subst b3.
-  assert (x0 = x) by congruence. subst x0.
+  assert (delta0 = delta) by congruence. subst delta0.
   exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split.
   unfold eq_block; rewrite zeq_true; simpl.
   decEq. decEq. rewrite Int.translate_cmp. auto. 
-  eapply valid_pointer_inject_no_overflow; eauto.
-  eapply valid_pointer_inject_no_overflow; eauto.
+  eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  eapply Mem.valid_pointer_inject_no_overflow; eauto.
   apply val_inject_val_of_bool.
   (* different blocks in source *)
   simpl. exists v; split; [idtac | eapply val_inject_eval_compare_mismatch; eauto].
   destruct (eq_block b2 b3); auto.
-  exploit different_pointers_inject; eauto. intros [A|A]. 
+  exploit Mem.different_pointers_inject; eauto. intros [A|A]. 
   congruence.
   decEq. destruct c; simpl in H6; inv H6; unfold Int.cmp.
-  predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr x)) (Int.add ofs0 (Int.repr x0)).
+  predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)).
   congruence. auto.
-  predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr x)) (Int.add ofs0 (Int.repr x0)).
+  predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)).
   congruence. auto.
   (* cmpu *)
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
@@ -1038,6 +1484,29 @@ Qed.
 
 (** Correctness of [make_store]. *)
 
+Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop :=
+  | val_content_inject_8_signed:
+      forall n,
+      val_content_inject f Mint8signed (Vint (Int.sign_ext 8 n)) (Vint n)
+  | val_content_inject_8_unsigned:
+      forall n,
+      val_content_inject f Mint8unsigned (Vint (Int.zero_ext 8 n)) (Vint n)
+  | val_content_inject_16_signed:
+      forall n,
+      val_content_inject f Mint16signed (Vint (Int.sign_ext 16 n)) (Vint n)
+  | val_content_inject_16_unsigned:
+      forall n,
+      val_content_inject f Mint16unsigned (Vint (Int.zero_ext 16 n)) (Vint n)
+  | val_content_inject_32:
+      forall n,
+      val_content_inject f Mfloat32 (Vfloat (Float.singleoffloat n)) (Vfloat n)
+  | val_content_inject_base:
+      forall chunk v1 v2,
+      val_inject f v1 v2 ->
+      val_content_inject f chunk v1 v2.
+
+Hint Resolve val_content_inject_base.
+
 Lemma store_arg_content_inject:
   forall f sp te tm a v va chunk,
   eval_expr tge sp te tm a va ->
@@ -1056,12 +1525,30 @@ Proof.
   destruct chunk; trivial;
   inv H; simpl in H6; inv H6;
   econstructor; (split; [eauto|idtac]);
-  destruct v1; simpl in H0; inv H0; try (constructor; constructor).
-  apply val_content_inject_8. auto. apply Int.zero_ext_idem. compute; auto.
-  apply val_content_inject_8; auto. apply Int.zero_ext_sign_ext. compute; auto.
-  apply val_content_inject_16; auto. apply Int.zero_ext_idem. compute; auto.
-  apply val_content_inject_16; auto. apply Int.zero_ext_sign_ext. compute; auto.
-  apply val_content_inject_32. apply Float.singleoffloat_idem. 
+  destruct v1; simpl in H0; inv H0; constructor; constructor.
+Qed.
+
+Lemma storev_mapped_inject':
+  forall f chunk m1 a1 v1 n1 m2 a2 v2,
+  Mem.inject f m1 m2 ->
+  Mem.storev chunk m1 a1 v1 = Some n1 ->
+  val_inject f a1 a2 ->
+  val_content_inject f chunk v1 v2 ->
+  exists n2,
+    Mem.storev chunk m2 a2 v2 = Some n2 /\ Mem.inject f n1 n2.
+Proof.
+  intros.
+  assert (forall v1',
+    (forall b ofs, Mem.store chunk m1 b ofs v1 = Mem.store chunk m1 b ofs v1') ->
+    Mem.storev chunk m1 a1 v1' = Some n1).
+  intros. rewrite <- H0. destruct a1; simpl; auto. 
+  inv H2; (eapply Mem.storev_mapped_inject; [eauto|idtac|eauto|eauto]);
+  auto; apply H3; intros.
+  apply Mem.store_int8_sign_ext.
+  apply Mem.store_int8_zero_ext.
+  apply Mem.store_int16_sign_ext.
+  apply Mem.store_int16_zero_ext.
+  apply Mem.store_float32_truncate.
 Qed.
 
 Lemma make_store_correct:
@@ -1069,69 +1556,63 @@ Lemma make_store_correct:
   eval_expr tge sp te tm addr tvaddr ->
   eval_expr tge sp te tm rhs tvrhs ->
   Mem.storev chunk m vaddr vrhs = Some m' ->
-  mem_inject f m tm ->
+  Mem.inject f m tm ->
   val_inject f vaddr tvaddr ->
   val_inject f vrhs tvrhs ->
-  exists tm',
+  exists tm', exists tvrhs',
   step tge (State fn (make_store chunk addr rhs) k sp te tm)
         E0 (State fn Sskip k sp te tm')
-  /\ mem_inject f m' tm'
-  /\ nextblock tm' = nextblock tm.
+  /\ Mem.storev chunk tm tvaddr tvrhs' = Some tm'
+  /\ Mem.inject f m' tm'.
 Proof.
   intros. unfold make_store.
   exploit store_arg_content_inject. eexact H0. eauto. 
   intros [tv [EVAL VCINJ]].
-  exploit storev_mapped_inject_1; eauto.
+  exploit storev_mapped_inject'; eauto.
   intros [tm' [STORE MEMINJ]].
-  exists tm'.
-  split. eapply step_store; eauto. 
-  split. auto.
-  unfold storev in STORE; destruct tvaddr; try discriminate.
-  eapply nextblock_store; eauto.
+  exists tm'; exists tv.
+  split. eapply step_store; eauto.
+  auto.
 Qed.
 
 (** Correctness of the variable accessors [var_get], [var_addr],
   and [var_set]. *)
 
 Lemma var_get_correct:
-  forall cenv id a f e te sp lo hi m cs tm b chunk v,
+  forall cenv id a f tf e te sp lo hi m cs tm b chunk v,
   var_get cenv id = OK a ->
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
-  mem_inject f m tm ->
+  match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
+  Mem.inject f m tm ->
   eval_var_ref gve e id b chunk ->
-  load chunk m b 0 = Some v ->
+  Mem.load chunk m b 0 = Some v ->
   exists tv,
     eval_expr tge (Vptr sp Int.zero) te tm a tv /\
     val_inject f v tv.
 Proof.
   unfold var_get; intros.
-  assert (match_var f id e m te sp cenv!!id).
-    inversion H0. inversion H17. auto.
-  inversion H4; subst; rewrite <- H5 in H; inversion H; subst.
+  assert (match_var f id e m te sp cenv!!id). inv H0. inv MENV. auto.
+  inv H4; rewrite <- H5 in H; inv H; inv H2; try congruence.
   (* var_local *)
-  inversion H2; [subst|congruence].
   exists v'; split.
-  apply eval_Evar. auto. 
-  replace v with v0. auto. congruence.
+  apply eval_Evar. auto.
+  congruence.
   (* var_stack_scalar *)
-  inversion H2; [subst|congruence].
   assert (b0 = b). congruence. subst b0.
   assert (chunk0 = chunk). congruence. subst chunk0.
-  exploit loadv_inject; eauto.
-    unfold loadv. eexact H3. 
+  exploit Mem.loadv_inject; eauto.
+    unfold Mem.loadv. eexact H3. 
   intros [tv [LOAD INJ]].
   exists tv; split. 
   eapply eval_Eload; eauto. eapply make_stackaddr_correct; eauto.
   auto.
   (* var_global_scalar *)
-  inversion H2; [congruence|subst]. simpl in H9; simpl in H10. 
+  simpl in *.
   assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inversion H11. destruct (mg_symbols0 _ _ H9) as [A B].
+  inv H2. exploit mg_symbols0; eauto. intros [A B].
   assert (chunk0 = chunk). congruence. subst chunk0.
-  assert (loadv chunk m (Vptr b Int.zero) = Some v). assumption.
   assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)).
-    econstructor; eauto. 
-  generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13).
+    econstructor; eauto.
+  exploit Mem.loadv_inject; eauto. simpl. eauto.   
   intros [tv [LOAD INJ]].
   exists tv; split. 
   eapply eval_Eload; eauto. eapply make_globaladdr_correct; eauto.
@@ -1139,8 +1620,8 @@ Proof.
 Qed.
 
 Lemma var_addr_correct:
-  forall cenv id a f e te sp lo hi m cs tm b,
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
+  forall cenv id a f tf e te sp lo hi m cs tm b,
+  match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
   var_addr cenv id = OK a ->
   eval_var_addr gve e id b ->
   exists tv,
@@ -1149,201 +1630,188 @@ Lemma var_addr_correct:
 Proof.
   unfold var_addr; intros.
   assert (match_var f id e m te sp cenv!!id).
-    inversion H. inversion H15. auto.
-  inversion H2; subst; rewrite <- H3 in H0; inversion H0; subst; clear H0.
+    inv H. inv MENV. auto. 
+  inv H2; rewrite <- H3 in H0; inv H0; inv H1; try congruence.
   (* var_stack_scalar *)
-  inversion H1; [subst|congruence]. 
   exists (Vptr sp (Int.repr ofs)); split.
-  eapply make_stackaddr_correct.
-  replace b with b0. auto. congruence.
+  eapply make_stackaddr_correct. congruence. 
   (* var_stack_array *)
-  inversion H1; [subst|congruence]. 
   exists (Vptr sp (Int.repr ofs)); split.
-  eapply make_stackaddr_correct.
-  replace b with b0. auto. congruence.
+  eapply make_stackaddr_correct. congruence.
   (* var_global_scalar *)
-  inversion H1; [congruence|subst].
   assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inversion H7. destruct (mg_symbols0 _ _ H6) as [A B].
+  inv H1. exploit mg_symbols0; eauto. intros [A B].
   exists (Vptr b Int.zero); split.
   eapply make_globaladdr_correct. eauto.
   econstructor; eauto. 
   (* var_global_array *)
-  inversion H1; [congruence|subst].
   assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inversion H6. destruct (mg_symbols0 _ _ H5) as [A B].
+  inv H1. exploit mg_symbols0; eauto. intros [A B].
   exists (Vptr b Int.zero); split.
   eapply make_globaladdr_correct. eauto.
   econstructor; eauto. 
 Qed.
 
 Lemma var_set_correct:
-  forall cenv id rhs a f e te sp lo hi m cs tm tv v m' fn k,
-  var_set cenv id rhs = OK a ->
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
+  forall cenv id rhs rhs_chunk a f tf e te sp lo hi m cs tm tv v m' fn k,
+  var_set cenv id rhs rhs_chunk = OK a ->
+  match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
   eval_expr tge (Vptr sp Int.zero) te tm rhs tv ->
   val_inject f v tv ->
-  mem_inject f m tm ->
+  Mem.inject f m tm ->
   exec_assign gve e m id v m' ->
+  val_normalized v rhs_chunk ->
   exists te', exists tm',
     step tge (State fn a k (Vptr sp Int.zero) te tm)
           E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\
-    mem_inject f m' tm' /\
-    match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m' /\
+    Mem.inject f m' tm' /\
+    match_callstack f m' tm' (Frame cenv tf e te' sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm') /\
     (forall id', id' <> id -> te'!id' = te!id').
 Proof.
-  unfold var_set; intros.
-  inv H4. 
-  assert (NEXTBLOCK: nextblock m' = nextblock m).
-    eapply nextblock_store; eauto.
-  inversion H0; subst.
-  assert (match_var f id e m te sp cenv!!id). inversion H19; auto.
-  inv H4; rewrite <- H7 in H; inv H.
+  intros until k. 
+  intros VS MCS EVAL VINJ MINJ ASG VNORM.
+  unfold var_set in VS. inv ASG. 
+  assert (NEXTBLOCK: Mem.nextblock m' = Mem.nextblock m).
+    eapply Mem.nextblock_store; eauto.
+  assert (MV: match_var f id e m te sp cenv!!id).
+    inv MCS. inv MENV. auto. 
+  inv MV; rewrite <- H1 in VS; inv VS; inv H; try congruence.
   (* var_local *)
-  inversion H5; [subst|congruence]. 
   assert (b0 = b) by congruence. subst b0.
   assert (chunk0 = chunk) by congruence. subst chunk0.
+  generalize H8; clear H8. case_eq (chunktype_compat rhs_chunk chunk).
+    (* compatible chunks *)
+  intros CCOMPAT EQ; inv EQ.
+  exploit chunktype_compat_correct; eauto. intro VNORM'.
+  exists (PTree.set id tv te); exists tm.
+  split. eapply step_assign. eauto. 
+  split. eapply Mem.store_unmapped_inject; eauto. 
+  split. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto.
+  eapply val_normalized_has_type; eauto. red in VNORM'. congruence. 
+  intros. apply PTree.gso; auto.
+    (* incompatible chunks but same type *)
+  intros. destruct (typ_eq (type_of_chunk chunk) (type_of_chunk rhs_chunk)); inv H8.
   exploit make_cast_correct; eauto.  
-  intros [tv' [EVAL INJ]].
+  intros [tv' [EVAL' INJ']].
   exists (PTree.set id tv' te); exists tm.
   split. eapply step_assign. eauto. 
-  split. eapply store_unmapped_inject; eauto. 
+  split. eapply Mem.store_unmapped_inject; eauto. 
   split. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto.
+  rewrite e0. eapply val_normalized_has_type; eauto. 
   intros. apply PTree.gso; auto.
   (* var_stack_scalar *)
-  inversion H5; [subst|congruence].
   assert (b0 = b) by congruence. subst b0.
   assert (chunk0 = chunk) by congruence. subst chunk0.
-  assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
+  assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
   exploit make_store_correct.
     eapply make_stackaddr_correct.
     eauto. eauto. eauto. eauto. eauto. 
-  intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]].
+  intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]].
   exists te; exists tm'.
   split. eauto. split. auto.  
-  split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
-  eapply match_callstack_mapped; eauto. 
-  inversion H9; congruence.
+  split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). 
+  eapply match_callstack_storev_mapped; eauto.
   auto.
   (* var_global_scalar *)
-  inversion H5; [congruence|subst]. simpl in H4; simpl in H10. 
+  simpl in *.
   assert (chunk0 = chunk) by congruence. subst chunk0.  
-  assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
+  assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
   assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inversion H12. destruct (mg_symbols0 _ _ H4) as [A B].
+  exploit mg_symbols; eauto. intros [A B].
   exploit make_store_correct.
     eapply make_globaladdr_correct; eauto.
-    eauto. eauto. eauto. eauto. eauto. 
-  intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]].
+    eauto. eauto. eauto. eauto. eauto.
+  intros [tm' [tvrhs' [EVAL' [STORE' TNEXTBLOCK]]]].
   exists te; exists tm'.
   split. eauto. split. auto. 
-  split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
-  eapply match_callstack_mapped; eauto. congruence.
+  split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). 
+  eapply match_callstack_store_mapped; eauto.
   auto.
 Qed.
 
-Lemma match_env_extensional':
-  forall f cenv e m te1 sp lo hi,
-  match_env f cenv e m te1 sp lo hi ->
-  forall te2,
-  (forall id, 
-     match cenv!!id with
-     | Var_local _ => te2!id = te1!id
-     | _ => True
-     end) ->
-  match_env f cenv e m te2 sp lo hi.
-Proof.
-  induction 1; intros; econstructor; eauto.
-  intros. generalize (me_vars0 id); intro. 
-  inversion H0; econstructor; eauto.
-  generalize (H id). rewrite <- H1. congruence. 
-Qed.
-
-
 Lemma match_callstack_extensional:
-  forall f cenv e te1 te2 sp lo hi cs bound tbound m,
-  (forall id, 
-     match cenv!!id with
-     | Var_local _ => te2!id = te1!id
-     | _ => True
-     end) ->
-  match_callstack f (mkframe cenv e te1 sp lo hi :: cs) bound tbound m ->
-  match_callstack f (mkframe cenv e te2 sp lo hi :: cs) bound tbound m.
+  forall f cenv tf e te1 te2 sp lo hi cs bound tbound m tm,
+  (forall id chunk, cenv!!id = Var_local chunk -> te2!id = te1!id) ->
+  match_callstack f m tm (Frame cenv tf e te1 sp lo hi :: cs) bound tbound ->
+  match_callstack f m tm (Frame cenv tf e te2 sp lo hi :: cs) bound tbound.
 Proof.
   intros. inv H0. constructor; auto. 
-  apply match_env_extensional' with te1; auto.
+  apply match_env_extensional with te1; auto.
 Qed.
 
 Lemma var_set_self_correct:
-  forall cenv id a f e te sp lo hi m cs tm tv v m' fn k,
-  var_set cenv id (Evar id) = OK a ->
-  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->
+  forall cenv id ty a f tf e te sp lo hi m cs tm tv te' v m' fn k,
+  var_set_self cenv id ty = OK a ->
+  match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
   val_inject f v tv ->
-  mem_inject f m tm ->
+  Mem.inject f m tm ->
   exec_assign gve e m id v m' ->
-  exists te', exists tm',
-    step tge (State fn a k (Vptr sp Int.zero) (PTree.set id tv te) tm)
-          E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\
-    mem_inject f m' tm' /\
-    match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m'.
-Proof.
-  unfold var_set; intros.
-  inv H3. 
-  assert (NEXTBLOCK: nextblock m' = nextblock m).
-    eapply nextblock_store; eauto.
-  inversion H0; subst.
-  assert (EVAR: eval_expr tge (Vptr sp Int.zero) (PTree.set id tv te) tm (Evar id) tv).
-    constructor. apply PTree.gss.
-  assert (match_var f id e m te sp cenv!!id). inversion H18; auto.
-  inv H3; rewrite <- H6 in H; inv H.
+  Val.has_type v ty ->
+  te'!id = Some tv ->
+  (forall i, i <> id -> te'!i = te!i) ->
+  exists te'', exists tm',
+    step tge (State fn a k (Vptr sp Int.zero) te' tm)
+          E0 (State fn Sskip k (Vptr sp Int.zero) te'' tm') /\
+    Mem.inject f m' tm' /\
+    match_callstack f m' tm' (Frame cenv tf e te'' sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm') /\
+    (forall id', id' <> id -> te''!id' = te'!id').
+Proof.
+  intros until k. 
+  intros VS MCS VINJ MINJ ASG VTY VAL OTHERS.
+  unfold var_set_self in VS. inv ASG. 
+  assert (NEXTBLOCK: Mem.nextblock m' = Mem.nextblock m).
+    eapply Mem.nextblock_store; eauto.
+  assert (MV: match_var f id e m te sp cenv!!id).
+    inv MCS. inv MENV. auto.
+  assert (EVAR: eval_expr tge (Vptr sp Int.zero) te' tm (Evar id) tv).
+    constructor. auto.
+  inv MV; rewrite <- H1 in VS; inv VS; inv H; try congruence.
   (* var_local *)
-  inversion H4; [subst|congruence]. 
   assert (b0 = b) by congruence. subst b0.
   assert (chunk0 = chunk) by congruence. subst chunk0.
-  exploit make_cast_correct; eauto. 
-  intros [tv' [EVAL INJ]].
-  exists (PTree.set id tv' (PTree.set id tv te)); exists tm.
+  destruct (typ_eq (type_of_chunk chunk) ty); inv H8.
+  exploit make_cast_correct; eauto.  
+  intros [tv' [EVAL' INJ']].
+  exists (PTree.set id tv' te'); exists tm.
   split. eapply step_assign. eauto. 
-  split. eapply store_unmapped_inject; eauto. 
-  rewrite NEXTBLOCK.
+  split. eapply Mem.store_unmapped_inject; eauto. 
+  split. rewrite NEXTBLOCK. 
   apply match_callstack_extensional with (PTree.set id tv' te).
-  intros. destruct (cenv!!id0); auto. 
-  repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. 
+  intros. repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. 
   eapply match_callstack_store_local; eauto.
+  intros; apply PTree.gso; auto.
   (* var_stack_scalar *)
-  inversion H4; [subst|congruence].
   assert (b0 = b) by congruence. subst b0.
   assert (chunk0 = chunk) by congruence. subst chunk0.
-  assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
+  assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
   exploit make_store_correct.
     eapply make_stackaddr_correct.
     eauto. eauto. eauto. eauto. eauto. 
-  intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]].
-  exists (PTree.set id tv te); exists tm'.
+  intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]].
+  exists te'; exists tm'.
   split. eauto. split. auto.  
-  rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
+  split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). 
   apply match_callstack_extensional with te.
-  intros. caseEq (cenv!!id0); intros; auto.
-  rewrite PTree.gsspec. destruct (peq id0 id). congruence. auto.
-  eapply match_callstack_mapped; eauto. 
-  inversion H8; congruence.
+  intros. apply OTHERS. congruence.
+  eapply match_callstack_storev_mapped; eauto.
+  auto.
   (* var_global_scalar *)
-  inversion H4; [congruence|subst]. simpl in H3; simpl in H9.
+  simpl in *.
   assert (chunk0 = chunk) by congruence. subst chunk0.  
-  assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
+  assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
   assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto.
-  inversion H11. destruct (mg_symbols0 _ _ H3) as [A B].
+  exploit mg_symbols; eauto. intros [A B].
   exploit make_store_correct.
     eapply make_globaladdr_correct; eauto.
-    eauto. eauto. eauto. eauto. eauto. 
-  intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]].
-  exists (PTree.set id tv te); exists tm'.
+    eauto. eauto. eauto. eauto. eauto.
+  intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]].
+  exists te'; exists tm'.
   split. eauto. split. auto. 
-  rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
+  split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). 
   apply match_callstack_extensional with te.
-  intros. caseEq (cenv!!id0); intros; auto.
-  rewrite PTree.gsspec. destruct (peq id0 id). congruence. auto.
-  eapply match_callstack_mapped; eauto. congruence.
+  intros. apply OTHERS. congruence.
+  eapply match_callstack_store_mapped; eauto.
+  auto.
 Qed.
 
 (** * Correctness of stack allocation of local variables *)
@@ -1361,26 +1829,38 @@ Proof.
   destruct (zlt sz 8); omega.
 Qed.
 
-Remark assign_variables_incr:
-  forall atk vars cenv sz cenv' sz',
-  assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'.
+Remark assign_variable_incr:
+  forall atk id lv cenv sz cenv' sz',
+  assign_variable atk (id, lv) (cenv, sz) = (cenv', sz') -> sz <= sz'.
 Proof.
-  induction vars; intros until sz'; simpl.
-  intro. replace sz' with sz. omega. congruence.
-  destruct a. destruct v. case (Identset.mem i atk); intros.
-  generalize (IHvars _ _ _ _ H). 
-  generalize (size_chunk_pos m). intro.
-  generalize (align_le sz (size_chunk m) H0). omega.
-  eauto.
-  intro. generalize (IHvars _ _ _ _ H).
+  intros until sz'; simpl.
+  destruct lv. case (Identset.mem id atk); intros.
+  inv H.  generalize (size_chunk_pos m). intro.
+  generalize (align_le sz (size_chunk m) H). omega.
+  inv H. omega.
+  intros. inv H. 
   generalize (align_le sz (array_alignment z) (array_alignment_pos z)).
   assert (0 <= Zmax 0 z). apply Zmax_bound_l. omega.
   omega.
 Qed.
 
+
+Remark assign_variables_incr:
+  forall atk vars cenv sz cenv' sz',
+  assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'.
+Proof.
+  induction vars; intros until sz'.
+  simpl; intros. replace sz' with sz. omega. congruence.
+Opaque assign_variable.
+  destruct a as [id lv]. simpl. 
+  case_eq (assign_variable atk (id, lv) (cenv, sz)). intros cenv1 sz1 EQ1 EQ2.
+  apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto.
+Transparent assign_variable.
+Qed.
+
 Remark inj_offset_aligned_array:
   forall stacksize sz,
-  inj_offset_aligned (align stacksize (array_alignment sz)) sz.
+  Mem.inj_offset_aligned (align stacksize (array_alignment sz)) sz.
 Proof.
   intros; red; intros.
   apply Zdivides_trans with (array_alignment sz).
@@ -1402,7 +1882,7 @@ Qed.
 
 Remark inj_offset_aligned_array':
   forall stacksize sz,
-  inj_offset_aligned (align stacksize (array_alignment sz)) (Zmax 0 sz).
+  Mem.inj_offset_aligned (align stacksize (array_alignment sz)) (Zmax 0 sz).
 Proof.
   intros. 
   replace (array_alignment sz) with (array_alignment (Zmax 0 sz)).
@@ -1413,7 +1893,7 @@ Qed.
 
 Remark inj_offset_aligned_var:
   forall stacksize chunk,
-  inj_offset_aligned (align stacksize (size_chunk chunk)) (size_chunk chunk).
+  Mem.inj_offset_aligned (align stacksize (size_chunk chunk)) (size_chunk chunk).
 Proof.
   intros.
   replace (align stacksize (size_chunk chunk))
@@ -1422,31 +1902,127 @@ Proof.
   decEq. destruct chunk; reflexivity.
 Qed.
 
+Lemma match_callstack_alloc_variable:
+  forall atk id lv cenv sz cenv' sz' tm sp e tf m m' b te lo cs f tv,
+  assign_variable atk (id, lv) (cenv, sz) = (cenv', sz') ->
+  Mem.valid_block tm sp ->
+  Mem.bounds tm sp = (0, tf.(fn_stackspace)) ->
+  Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable ->
+  tf.(fn_stackspace) <= Int.max_signed ->
+  Mem.alloc m 0 (sizeof lv) = (m', b) ->
+  match_callstack f m tm 
+                  (Frame cenv tf e te sp lo (Mem.nextblock m) :: cs)
+                  (Mem.nextblock m) (Mem.nextblock tm) ->
+  Mem.inject f m tm ->
+  0 <= sz -> sz' <= tf.(fn_stackspace) ->
+  (forall b delta, f b = Some(sp, delta) -> Mem.high_bound m b + delta <= sz) ->
+  e!id = None ->
+  te!id = Some tv ->
+  exists f',
+     inject_incr f f'
+  /\ Mem.inject f' m' tm
+  /\ match_callstack f' m' tm
+                     (Frame cenv' tf (PTree.set id (b, lv) e) te sp lo (Mem.nextblock m') :: cs)
+                     (Mem.nextblock m') (Mem.nextblock tm)
+  /\ (forall b delta,
+      f' b = Some(sp, delta) -> Mem.high_bound m' b + delta <= sz').
+Proof.
+  intros until tv. intros ASV VALID BOUNDS PERMS NOOV ALLOC MCS INJ LO HI RANGE E TE.
+  generalize ASV. unfold assign_variable. 
+  caseEq lv.
+  (* 1. lv = LVscalar chunk *)
+  intros chunk LV. case (Identset.mem id atk).
+  (* 1.1 info = Var_stack_scalar chunk ofs *)
+    set (ofs := align sz (size_chunk chunk)).
+    intro EQ; injection EQ; intros; clear EQ. rewrite <- H0.
+    generalize (size_chunk_pos chunk); intro SIZEPOS.
+    generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS.
+    exploit Mem.alloc_left_mapped_inject.
+      eauto. eauto. eauto. 
+      instantiate (1 := ofs). 
+      generalize Int.min_signed_neg. omega.
+      right; rewrite BOUNDS; simpl. generalize Int.min_signed_neg. omega.
+      intros. apply Mem.perm_implies with Freeable; auto with mem.
+      apply PERMS. rewrite LV in H1. simpl in H1. omega.
+      rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. 
+      apply inj_offset_aligned_var.
+      intros. generalize (RANGE _ _ H1). omega. 
+    intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]].
+    exists f1; split. auto. split. auto. split. 
+    eapply match_callstack_alloc_left; eauto.
+    rewrite <- LV; auto. 
+    rewrite SAME; constructor.
+    intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). 
+    destruct (eq_block b0 b); simpl.
+    subst b0. assert (delta = ofs) by congruence. subst delta.  
+    rewrite LV. simpl. omega.
+    rewrite OTHER in H1; eauto. generalize (RANGE _ _ H1). omega. 
+  (* 1.2 info = Var_local chunk *)
+    intro EQ; injection EQ; intros; clear EQ. subst sz'. rewrite <- H0.
+    exploit Mem.alloc_left_unmapped_inject; eauto.
+    intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]].
+    exists f1; split. auto. split. auto. split.
+    eapply match_callstack_alloc_left; eauto. 
+    rewrite <- LV; auto.
+    rewrite SAME; constructor.
+    intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). 
+    destruct (eq_block b0 b); simpl.
+    subst b0. congruence.
+    rewrite OTHER in H; eauto.
+  (* 2 info = Var_stack_array ofs *)
+  intros dim LV EQ. injection EQ; clear EQ; intros. rewrite <- H0.
+  assert (0 <= Zmax 0 dim). apply Zmax1. 
+  generalize (align_le sz (array_alignment dim) (array_alignment_pos dim)). intro.
+  set (ofs := align sz (array_alignment dim)) in *.
+  exploit Mem.alloc_left_mapped_inject. eauto. eauto. eauto. 
+    instantiate (1 := ofs). 
+    generalize Int.min_signed_neg. omega.
+    right; rewrite BOUNDS; simpl. generalize Int.min_signed_neg. omega.
+    intros. apply Mem.perm_implies with Freeable; auto with mem.
+    apply PERMS. rewrite LV in H3. simpl in H3. omega.
+    rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. 
+    apply inj_offset_aligned_array'.
+    intros. generalize (RANGE _ _ H3). omega. 
+  intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]].
+  exists f1; split. auto. split. auto. split. 
+  eapply match_callstack_alloc_left; eauto.
+  rewrite <- LV; auto. 
+  rewrite SAME; constructor.
+  intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). 
+  destruct (eq_block b0 b); simpl.
+  subst b0. assert (delta = ofs) by congruence. subst delta. 
+  rewrite LV. simpl. omega.
+  rewrite OTHER in H3; eauto. generalize (RANGE _ _ H3). omega. 
+Qed.
+
 Lemma match_callstack_alloc_variables_rec:
-  forall tm sp cenv' sz' te lo cs atk,
-  valid_block tm sp ->
-  low_bound tm sp = 0 ->
-  high_bound tm sp = sz' ->
-  sz' <= Int.max_signed ->
+  forall tm sp cenv' tf te lo cs atk,
+  Mem.valid_block tm sp ->
+  Mem.bounds tm sp = (0, tf.(fn_stackspace)) ->
+  Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable ->
+  tf.(fn_stackspace) <= Int.max_signed ->
   forall e m vars e' m',
   alloc_variables e m vars e' m' ->
   forall f cenv sz,
-  assign_variables atk vars (cenv, sz) = (cenv', sz') ->
-  match_callstack f (mkframe cenv e te sp lo m.(nextblock) :: cs)
-                    m.(nextblock) tm.(nextblock) m ->
-  mem_inject f m tm ->
+  assign_variables atk vars (cenv, sz) = (cenv', tf.(fn_stackspace)) ->
+  match_callstack f m tm 
+                  (Frame cenv tf e te sp lo (Mem.nextblock m) :: cs)
+                  (Mem.nextblock m) (Mem.nextblock tm) ->
+  Mem.inject f m tm ->
   0 <= sz ->
-  (forall b delta, f b = Some(sp, delta) -> high_bound m b + delta <= sz) ->
+  (forall b delta,
+     f b = Some(sp, delta) -> Mem.high_bound m b + delta <= sz) ->
   (forall id lv, In (id, lv) vars -> te!id <> None) ->
   list_norepet (List.map (@fst ident var_kind) vars) ->
   (forall id lv, In (id, lv) vars -> e!id = None) ->
   exists f',
      inject_incr f f'
-  /\ mem_inject f' m' tm
-  /\ match_callstack f' (mkframe cenv' e' te sp lo m'.(nextblock) :: cs)
-                        m'.(nextblock) tm.(nextblock) m'.
+  /\ Mem.inject f' m' tm
+  /\ match_callstack f' m' tm
+                     (Frame cenv' tf e' te sp lo (Mem.nextblock m') :: cs)
+                     (Mem.nextblock m') (Mem.nextblock tm).
 Proof.
-  intros until atk. intros VB LB HB NOOV.
+  intros until atk. intros VALID BOUNDS PERM NOOV.
   induction 1.
   (* base case *)
   intros. simpl in H. inversion H; subst cenv sz.
@@ -1462,81 +2038,18 @@ Proof.
   assert (exists tv, te!id = Some tv).
     assert (te!id <> None). eapply DEFINED. simpl; left; auto.
     destruct (te!id). exists v; auto. congruence.
-  elim H1; intros tv TEID; clear H1.
-  assert (UNDEFINED1: forall (id0 : ident) (lv0 : var_kind),
-            In (id0, lv0) vars ->
-            (PTree.set id (b1, lv) e)!id0 = None).
-    intros. rewrite PTree.gso. eapply UNDEFINED; eauto with coqlib.
-    simpl in NOREPET. inversion NOREPET. red; intro; subst id0.
-    elim H4. change id with (fst (id, lv0)). apply List.in_map. auto.
-  assert (NOREPET1: list_norepet (map (fst (A:=ident) (B:=var_kind)) vars)).
-    inv NOREPET; auto.
-  generalize ASV1. unfold assign_variable.
-  caseEq lv.
-  (* 1. lv = LVscalar chunk *)
-  intros chunk LV. case (Identset.mem id atk).
-  (* 1.1 info = Var_stack_scalar chunk ... *)
-    set (ofs := align sz (size_chunk chunk)).
-    intro EQ; injection EQ; intros; clear EQ.
-    set (f1 := extend_inject b1 (Some (sp, ofs)) f).
-    generalize (size_chunk_pos chunk); intro SIZEPOS.
-    generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS.
-    assert (mem_inject f1 m1 tm /\ inject_incr f f1).
-      assert (Int.min_signed < 0). compute; auto.
-      generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro.
-      unfold f1; eapply alloc_mapped_inject; eauto.
-      omega. omega. omega. omega. unfold sizeof; rewrite LV. omega.
-      rewrite Zminus_0_r. unfold ofs. rewrite LV. simpl. 
-      apply inj_offset_aligned_var. 
-      intros. left. generalize (BOUND _ _ H5). omega. 
-    elim H3; intros MINJ1 INCR1; clear H3.
-    exploit IHalloc_variables; eauto.
-      unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib.
-      rewrite <- H1. omega.
-      intros until delta; unfold f1, extend_inject, eq_block.
-      rewrite (high_bound_alloc _ _ _ _ _ H b).
-      case (zeq b b1); intros. 
-      inversion H3. unfold sizeof; rewrite LV. omega.
-      generalize (BOUND _ _ H3). omega.
-    intros [f' [INCR2 [MINJ2 MATCH2]]].
-    exists f'; intuition. eapply inject_incr_trans; eauto. 
-  (* 1.2 info = Var_local chunk *)
-    intro EQ; injection EQ; intros; clear EQ. subst sz1.
-    exploit alloc_unmapped_inject; eauto.
-    set (f1 := extend_inject b1 None f). intros [MINJ1 INCR1].
-    exploit IHalloc_variables; eauto.
-      unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib.
-      intros until delta; unfold f1, extend_inject, eq_block.
-      rewrite (high_bound_alloc _ _ _ _ _ H b).
-      case (zeq b b1); intros. discriminate.
-      eapply BOUND; eauto.
-    intros [f' [INCR2 [MINJ2 MATCH2]]].
-    exists f'; intuition. eapply inject_incr_trans; eauto. 
-  (* 2. lv = LVarray dim, info = Var_stack_array *)
-  intros dim LV EQ. injection EQ; clear EQ; intros.
-  assert (0 <= Zmax 0 dim). apply Zmax1. 
-  generalize (align_le sz (array_alignment dim) (array_alignment_pos dim)). intro.
-  set (ofs := align sz (array_alignment dim)) in *.
-  set (f1 := extend_inject b1 (Some (sp, ofs)) f).
-  assert (mem_inject f1 m1 tm /\ inject_incr f f1).
-    assert (Int.min_signed < 0). compute; auto.
-    generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro.
-    unfold f1; eapply alloc_mapped_inject; eauto.
-    omega. omega. omega. omega. unfold sizeof; rewrite LV. omega.
-    rewrite Zminus_0_r. unfold ofs. rewrite LV. simpl.
-    apply inj_offset_aligned_array'.
-    intros. left. generalize (BOUND _ _ H7). omega. 
-  destruct H5 as [MINJ1 INCR1].
-  exploit IHalloc_variables; eauto.  
-    unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib.
-    rewrite <- H1. omega.
-    intros until delta; unfold f1, extend_inject, eq_block.
-    rewrite (high_bound_alloc _ _ _ _ _ H b).
-    case (zeq b b1); intros. 
-    inversion H5. unfold sizeof; rewrite LV. omega.
-    generalize (BOUND _ _ H5). omega. 
-    intros [f' [INCR2 [MINJ2 MATCH2]]].
-    exists f'; intuition. eapply inject_incr_trans; eauto. 
+  destruct H1 as [tv TEID].
+  assert (sz1 <= fn_stackspace tf). eapply assign_variables_incr; eauto. 
+  exploit match_callstack_alloc_variable; eauto with coqlib.
+  intros [f1 [INCR1 [INJ1 [MCS1 BOUND1]]]].
+  exploit IHalloc_variables; eauto. 
+  apply Zle_trans with sz; auto. eapply assign_variable_incr; eauto.
+  inv NOREPET; auto.
+  intros. rewrite PTree.gso. eapply UNDEFINED; eauto with coqlib.
+  simpl in NOREPET. inversion NOREPET. red; intro; subst id0.
+  elim H5. change id with (fst (id, lv0)). apply List.in_map. auto.
+  intros [f2 [INCR2 [INJ2 MCS2]]].
+  exists f2; intuition. eapply inject_incr_trans; eauto. 
 Qed.
 
 Lemma set_params_defined:
@@ -1578,56 +2091,32 @@ Qed.
   of Csharpminor local variables and of the Cminor stack data block. *)
 
 Lemma match_callstack_alloc_variables:
-  forall fn cenv sz m e m' tm tm' sp f cs targs body,
-  build_compilenv gce fn = (cenv, sz) ->
-  sz <= Int.max_signed ->
+  forall fn cenv tf m e m' tm tm' sp f cs targs body,
+  build_compilenv gce fn = (cenv, tf.(fn_stackspace)) ->
+  tf.(fn_stackspace) <= Int.max_signed ->
   list_norepet (fn_params_names fn ++ fn_vars_names fn) ->
   alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' ->
-  Mem.alloc tm 0 sz = (tm', sp) ->
-  match_callstack f cs m.(nextblock) tm.(nextblock) m ->
-  mem_inject f m tm ->
+  Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) ->
+  match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) ->
+  Mem.inject f m tm ->
   let tvars := make_vars (fn_params_names fn) (fn_vars_names fn) body in
   let te := set_locals tvars (set_params targs (fn_params_names fn)) in
   exists f',
      inject_incr f f'
-  /\ mem_inject f' m' tm'
-  /\ match_callstack f' (mkframe cenv e te sp m.(nextblock) m'.(nextblock) :: cs)
-                        m'.(nextblock) tm'.(nextblock) m'.
+  /\ Mem.inject f' m' tm'
+  /\ match_callstack f' m' tm'
+                     (Frame cenv tf e te sp (Mem.nextblock m) (Mem.nextblock m') :: cs)
+                     (Mem.nextblock m') (Mem.nextblock tm').
 Proof.
   intros. 
-  assert (SP: sp = nextblock tm). injection H3; auto.
   unfold build_compilenv in H. 
-  eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto with mem.
-  eapply low_bound_alloc_same; eauto.
-  eapply high_bound_alloc_same; eauto.
-  (* match_callstack *)
-  constructor. omega. change (valid_block tm' sp). eapply valid_new_block; eauto.
-  constructor. 
-    (* me_vars *)
-    intros. generalize (global_compilenv_charact id).
-    destruct (gce!!id); intro; try contradiction.
-    constructor.
-      unfold Csharpminor.empty_env. apply PTree.gempty. auto.
-    constructor.
-      unfold Csharpminor.empty_env. apply PTree.gempty. 
-    (* me_low_high *)
-    omega.
-    (* me_bounded *)
-    intros until lv. unfold Csharpminor.empty_env. rewrite PTree.gempty. congruence.
-    (* me_inj *)
-    intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence.
-    (* me_inv *)
-    intros. exploit mi_mappedblocks; eauto. intro A.
-    elim (fresh_block_alloc _ _ _ _ _ H3 A).
-    (* me_incr *)
-    intros. exploit mi_mappedblocks; eauto. intro A.
-    rewrite SP; auto.
-  rewrite SP; auto.
-  eapply alloc_right_inject; eauto.
-  omega.
-  intros. exploit mi_mappedblocks; eauto. unfold valid_block; intro.
-  unfold block in SP; omegaContradiction.
-  (* defined *)
+  eapply match_callstack_alloc_variables_rec; eauto with mem.
+  eapply Mem.bounds_alloc_same; eauto.
+  red; intros; eauto with mem.
+  eapply match_callstack_alloc_right; eauto.
+  eapply Mem.alloc_right_inject; eauto. omega. 
+  intros. elim (Mem.valid_not_valid_diff tm sp sp); eauto with mem.
+  eapply Mem.valid_block_inject_2; eauto.
   intros. unfold te. apply set_locals_params_defined.
   elim (in_app_or _ _ _ H6); intros.
   elim (list_in_map_inv _ _ _ H7). intros x [A B].
@@ -1645,15 +2134,16 @@ Qed.
 (** Correctness of the code generated by [store_parameters]
   to store in memory the values of parameters that are stack-allocated. *)
 
-Inductive vars_vals_match:
-    meminj -> list (ident * memory_chunk) -> list val -> env -> Prop :=
+Inductive vars_vals_match (f:meminj):
+             list (ident * memory_chunk) -> list val -> env -> Prop :=
   | vars_vals_nil:
-      forall f te,
+      forall te,
       vars_vals_match f nil nil te
   | vars_vals_cons:
-      forall f te id chunk vars v vals tv,
+      forall te id chunk vars v vals tv,
       te!id = Some tv ->
       val_inject f v tv ->
+      Val.has_type v (type_of_chunk chunk) ->
       vars_vals_match f vars vals te ->
       vars_vals_match f ((id, chunk) :: vars) (v :: vals) te.
 
@@ -1666,24 +2156,25 @@ Lemma vars_vals_match_extensional:
 Proof.
   induction 1; intros.
   constructor.
-  econstructor; eauto. rewrite <- H. eapply H2. left. reflexivity.
-  apply IHvars_vals_match. intros. eapply H2; eauto. right. eauto.
+  econstructor; eauto. 
+  rewrite <- H. eauto with coqlib. 
+  apply IHvars_vals_match. intros. eapply H3; eauto with coqlib.
 Qed.
 
 Lemma store_parameters_correct:
   forall e m1 params vl m2,
   bind_parameters e m1 params vl m2 ->
-  forall s f te1 cenv sp lo hi cs tm1 fn k,
+  forall s f te1 cenv tf sp lo hi cs tm1 fn k,
   vars_vals_match f params vl te1 ->
-  list_norepet (List.map (@fst ident memory_chunk) params) ->
-  mem_inject f m1 tm1 ->
-  match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 ->
+  list_norepet (List.map param_name params) ->
+  Mem.inject f m1 tm1 ->
+  match_callstack f m1 tm1 (Frame cenv tf e te1 sp lo hi :: cs) (Mem.nextblock m1) (Mem.nextblock tm1) ->
   store_parameters cenv params = OK s ->
   exists te2, exists tm2,
      star step tge (State fn s k (Vptr sp Int.zero) te1 tm1)
                 E0 (State fn Sskip k (Vptr sp Int.zero) te2 tm2)
-  /\ mem_inject f m2 tm2
-  /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2.
+  /\ Mem.inject f m2 tm2
+  /\ match_callstack f m2 tm2 (Frame cenv tf e te2 sp lo hi :: cs) (Mem.nextblock m2) (Mem.nextblock tm2).
 Proof.
   induction 1.
   (* base case *)
@@ -1692,17 +2183,15 @@ Proof.
   (* inductive case *)
   intros until k.  intros VVM NOREPET MINJ MATCH STOREP.
   monadInv STOREP.
-  inversion VVM. subst f0 id0 chunk0 vars v vals te.
-  inversion NOREPET. subst hd tl.
-  exploit var_set_correct; eauto.
-    constructor; auto.
-    econstructor; eauto.
-    econstructor; eauto.
+  inv VVM. 
+  inv NOREPET.
+  exploit var_set_self_correct; eauto.
+    econstructor; eauto. econstructor; eauto.
   intros [te2 [tm2 [EXEC1 [MINJ1 [MATCH1 UNCHANGED1]]]]].
   assert (vars_vals_match f params vl te2).
     apply vars_vals_match_extensional with te1; auto.
     intros. apply UNCHANGED1. red; intro; subst id0.
-    elim H4. change id with (fst (id, lv)). apply List.in_map. auto.
+    elim H4. change id with (param_name (id, lv)). apply List.in_map. auto.
   exploit IHbind_parameters; eauto.
   intros [te3 [tm3 [EXEC2 [MINJ2 MATCH2]]]].
   exists te3; exists tm3.
@@ -1715,50 +2204,42 @@ Qed.
 
 Lemma vars_vals_match_holds_1:
   forall f params args targs,
-  list_norepet (List.map (@fst ident memory_chunk) params) ->
-  List.length params = List.length args ->
+  list_norepet (List.map param_name params) ->
   val_list_inject f args targs ->
+  Val.has_type_list args (List.map type_of_chunk (List.map param_chunk params)) ->
   vars_vals_match f params args
     (set_params targs (List.map (@fst ident memory_chunk) params)).
 Proof.
-  induction params; destruct args; simpl; intros; try discriminate.
+  induction params; simpl; intros.
+  destruct args; simpl in H1; try contradiction. inv H0.
   constructor.
-  inversion H1. subst v0 vl targs. 
-  inversion H. subst hd tl.
-  destruct a as [id chunk]. econstructor. 
-  simpl. rewrite PTree.gss. reflexivity.
-  auto. 
+  destruct args; simpl in H1; try contradiction. destruct H1. inv H0. inv H.
+  destruct a as [id chunk]; simpl in *. econstructor.
+  rewrite PTree.gss. reflexivity. 
+  auto. auto.
   apply vars_vals_match_extensional
-  with (set_params vl' (map (@fst ident memory_chunk) params)).
+  with (set_params vl' (map param_name params)).
   eapply IHparams; eauto. 
   intros. simpl. apply PTree.gso. red; intro; subst id0.
-  elim H5. change (fst (id, chunk)) with (fst (id, lv)). 
-  apply List.in_map; auto.
+  elim H4. change id with (param_name (id, lv)). apply List.in_map; auto.
 Qed.
 
 Lemma vars_vals_match_holds:
   forall f params args targs,
-  List.length params = List.length args ->
+  list_norepet (List.map param_name params) ->
   val_list_inject f args targs ->
+  Val.has_type_list args (List.map type_of_chunk (List.map param_chunk params)) ->
   forall vars,
-  list_norepet (vars ++ List.map (@fst ident memory_chunk) params) ->
+  list_norepet (vars ++ List.map param_name params) ->
   vars_vals_match f params args
-    (set_locals vars (set_params targs (List.map (@fst ident memory_chunk) params))).
+    (set_locals vars (set_params targs (List.map param_name params))).
 Proof.
   induction vars; simpl; intros.
   eapply vars_vals_match_holds_1; eauto.
-  inversion H1. subst hd tl.
+  inv H2.
   eapply vars_vals_match_extensional; eauto.
-  intros. apply PTree.gso. red; intro; subst id; elim H4.
-  apply in_or_app. right. change a with (fst (a, lv)). apply List.in_map; auto.
-Qed.
-
-Lemma bind_parameters_length:
-  forall e m1 params args m2,
-  bind_parameters e m1 params args m2 ->
-  List.length params = List.length args.
-Proof.
-  induction 1; simpl; eauto.
+  intros. apply PTree.gso. red; intro; subst id; elim H5.
+  apply in_or_app. right. change a with (param_name (a, lv)). apply List.in_map; auto.
 Qed.
 
 Remark identset_removelist_charact:
@@ -1815,45 +2296,44 @@ Qed.
   and initialize the blocks corresponding to function parameters). *)
 
 Lemma function_entry_ok:
-  forall fn m e m1 vargs m2 f cs tm cenv sz tm1 sp tvargs body s fn' k,
+  forall fn m e m1 vargs m2 f cs tm cenv tf tm1 sp tvargs body s fn' k,
+  list_norepet (fn_params_names fn ++ fn_vars_names fn) ->
   alloc_variables empty_env m (fn_variables fn) e m1 ->
   bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 ->
-  match_callstack f cs m.(nextblock) tm.(nextblock) m ->
-  build_compilenv gce fn = (cenv, sz) ->
-  sz <= Int.max_signed ->
-  Mem.alloc tm 0 sz = (tm1, sp) ->
+  match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) ->
+  build_compilenv gce fn = (cenv, tf.(fn_stackspace)) ->
+  tf.(fn_stackspace) <= Int.max_signed ->
+  Mem.alloc tm 0 tf.(fn_stackspace) = (tm1, sp) ->
   let vars :=
     make_vars (fn_params_names fn) (fn_vars_names fn) body in
   let te :=
     set_locals vars (set_params tvargs (fn_params_names fn)) in
   val_list_inject f vargs tvargs ->
-  mem_inject f m tm ->
-  list_norepet (fn_params_names fn ++ fn_vars_names fn) ->
+  Val.has_type_list vargs (Csharpminor.fn_sig fn).(sig_args) ->
+  Mem.inject f m tm ->
   store_parameters cenv fn.(Csharpminor.fn_params) = OK s ->
   exists f2, exists te2, exists tm2,
      star step tge (State fn' s k (Vptr sp Int.zero) te tm1)
                 E0 (State fn' Sskip k (Vptr sp Int.zero) te2 tm2)
-  /\ mem_inject f2 m2 tm2
+  /\ Mem.inject f2 m2 tm2
   /\ inject_incr f f2
-  /\ match_callstack f2
-       (mkframe cenv e te2 sp m.(nextblock) m1.(nextblock) :: cs)
-       m2.(nextblock) tm2.(nextblock) m2.
+  /\ match_callstack f2 m2 tm2
+       (Frame cenv tf e te2 sp (Mem.nextblock m) (Mem.nextblock m1) :: cs)
+       (Mem.nextblock m2) (Mem.nextblock tm2).
 Proof.
-  intros. 
-  exploit bind_parameters_length; eauto. intro LEN1.
+  intros.
   exploit match_callstack_alloc_variables; eauto.
   intros [f1 [INCR1 [MINJ1 MATCH1]]].
   exploit vars_vals_match_holds.
-    eauto. apply val_list_inject_incr with f. eauto. eauto.
-    eapply make_vars_norepet. auto. 
+    eapply list_norepet_append_left. eexact H.  
+    apply val_list_inject_incr with f. eauto. eauto.
+    auto. eapply make_vars_norepet. auto. 
   intro VVM.
   exploit store_parameters_correct.
-    eauto. eauto. 
-    unfold fn_params_names in H7. eapply list_norepet_append_left; eauto.
-    eexact MINJ1. fold (fn_params_names fn). eexact MATCH1. eauto. 
+    eauto. eauto. eapply list_norepet_append_left; eauto.
+    eexact MINJ1. fold (fn_params_names fn). eexact MATCH1. eauto.
   intros [te2 [tm2 [EXEC [MINJ2 MATCH2]]]].
-  exists f1; exists te2; exists tm2.
-  split. eauto. auto.
+  exists f1; exists te2; exists tm2. eauto.
 Qed.
 
 (** * Semantic preservation for the translation *)
@@ -1890,11 +2370,11 @@ Proof.
 Qed.
 
 Lemma transl_expr_correct:
-  forall f m tm cenv e te sp lo hi cs
-    (MINJ: mem_inject f m tm)
-    (MATCH: match_callstack f
-             (mkframe cenv e te sp lo hi :: cs)
-             m.(nextblock) tm.(nextblock) m),
+  forall f m tm cenv tf e te sp lo hi cs
+    (MINJ: Mem.inject f m tm)
+    (MATCH: match_callstack f m tm
+             (Frame cenv tf e te sp lo hi :: cs)
+             (Mem.nextblock m) (Mem.nextblock tm)),
   forall a v,
   Csharpminor.eval_expr gve e m a v ->
   forall ta
@@ -1922,7 +2402,7 @@ Proof.
   exists tv; split. econstructor; eauto. auto.
   (* Eload *)
   exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
-  exploit loadv_inject; eauto. intros [tv [LOAD INJ]].
+  exploit Mem.loadv_inject; eauto. intros [tv [LOAD INJ]].
   exists tv; split. econstructor; eauto. auto.
   (* Econdition *)
   exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].
@@ -1935,11 +2415,11 @@ Proof.
 Qed.
 
 Lemma transl_exprlist_correct:
-  forall f m tm cenv e te sp lo hi cs
-    (MINJ: mem_inject f m tm)
-    (MATCH: match_callstack f
-             (mkframe cenv e te sp lo hi :: cs)
-             m.(nextblock) tm.(nextblock) m),
+  forall f m tm cenv tf e te sp lo hi cs
+    (MINJ: Mem.inject f m tm)
+    (MATCH: match_callstack f m tm
+             (Frame cenv tf e te sp lo hi :: cs)
+             (Mem.nextblock m) (Mem.nextblock tm)),
   forall a v,
   Csharpminor.eval_exprlist gve e m a v ->
   forall ta
@@ -1957,86 +2437,84 @@ Qed.
 
 (** ** Semantic preservation for statements and functions *)
 
-Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env -> callstack -> Prop :=
-  | match_Kstop: forall cenv xenv,
-      match_cont Csharpminor.Kstop Kstop cenv xenv nil
-  | match_Kseq: forall s k ts tk cenv xenv cs,
-      transl_stmt cenv xenv s = OK ts ->
-      match_cont k tk cenv xenv cs ->
-      match_cont (Csharpminor.Kseq s k) (Kseq ts tk) cenv xenv cs
-  | match_Kseq2: forall s1 s2 k ts1 tk cenv xenv cs,
-      transl_stmt cenv xenv s1 = OK ts1 ->
-      match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs ->
+Inductive match_cont: Csharpminor.cont -> Cminor.cont -> option typ -> compilenv -> exit_env -> callstack -> Prop :=
+  | match_Kstop: forall ty cenv xenv,
+      match_cont Csharpminor.Kstop Kstop ty cenv xenv nil
+  | match_Kseq: forall s k ts tk ty cenv xenv cs,
+      transl_stmt ty cenv xenv s = OK ts ->
+      match_cont k tk ty cenv xenv cs ->
+      match_cont (Csharpminor.Kseq s k) (Kseq ts tk) ty cenv xenv cs
+  | match_Kseq2: forall s1 s2 k ts1 tk ty cenv xenv cs,
+      transl_stmt ty cenv xenv s1 = OK ts1 ->
+      match_cont (Csharpminor.Kseq s2 k) tk ty cenv xenv cs ->
       match_cont (Csharpminor.Kseq (Csharpminor.Sseq s1 s2) k)
-                 (Kseq ts1 tk) cenv xenv cs
-  | match_Kblock: forall k tk cenv xenv cs,
-      match_cont k tk cenv xenv cs ->
-      match_cont (Csharpminor.Kblock k) (Kblock tk) cenv (true :: xenv) cs
-  | match_Kblock2: forall k tk cenv xenv cs,
-      match_cont k tk cenv xenv cs ->
-      match_cont k (Kblock tk) cenv (false :: xenv) cs
-  | match_Kcall_none: forall fn e k tfn sp te tk cenv xenv lo hi cs sz cenv',
+                 (Kseq ts1 tk) ty cenv xenv cs
+  | match_Kblock: forall k tk ty cenv xenv cs,
+      match_cont k tk ty cenv xenv cs ->
+      match_cont (Csharpminor.Kblock k) (Kblock tk) ty cenv (true :: xenv) cs
+  | match_Kblock2: forall k tk ty cenv xenv cs,
+      match_cont k tk ty cenv xenv cs ->
+      match_cont k (Kblock tk) ty cenv (false :: xenv) cs
+  | match_Kcall_none: forall fn e k tfn sp te tk ty cenv xenv lo hi cs sz cenv',
       transl_funbody cenv sz fn = OK tfn ->
-      match_cont k tk cenv xenv cs ->
+      match_cont k tk fn.(fn_return) cenv xenv cs ->
       match_cont (Csharpminor.Kcall None fn e k)
                  (Kcall None tfn (Vptr sp Int.zero) te tk)
-                 cenv' nil
-                 (mkframe cenv e te sp lo hi :: cs)
-  | match_Kcall_some: forall id fn e k tfn s sp te tk cenv xenv lo hi cs sz cenv',
+                 ty cenv' nil
+                 (Frame cenv tfn e te sp lo hi :: cs)
+  | match_Kcall_some: forall id fn e k tfn s sp te tk ty cenv xenv lo hi cs sz cenv',
       transl_funbody cenv sz fn = OK tfn ->
-      var_set cenv id (Evar id) = OK s ->
-      match_cont k tk cenv xenv cs ->
+      var_set_self cenv id (typ_of_opttyp ty) = OK s ->
+      match_cont k tk fn.(fn_return) cenv xenv cs ->
       match_cont (Csharpminor.Kcall (Some id) fn e k)
                  (Kcall (Some id) tfn (Vptr sp Int.zero) te (Kseq s tk))
-                 cenv' nil
-                 (mkframe cenv e te sp lo hi :: cs).
+                 ty cenv' nil
+                 (Frame cenv tfn e te sp lo hi :: cs).
 
 Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
   | match_state:
       forall fn s k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz
       (TRF: transl_funbody cenv sz fn = OK tfn)
-      (TR: transl_stmt cenv xenv s = OK ts)
-      (MINJ: mem_inject f m tm)
-      (MCS: match_callstack f
-               (mkframe cenv e te sp lo hi :: cs)
-               m.(nextblock) tm.(nextblock) m)
-      (MK: match_cont k tk cenv xenv cs),
+      (TR: transl_stmt fn.(fn_return) cenv xenv s = OK ts)
+      (MINJ: Mem.inject f m tm)
+      (MCS: match_callstack f m tm
+               (Frame cenv tfn e te sp lo hi :: cs)
+               (Mem.nextblock m) (Mem.nextblock tm))
+      (MK: match_cont k tk fn.(fn_return) cenv xenv cs),
       match_states (Csharpminor.State fn s k e m)
                    (State tfn ts tk (Vptr sp Int.zero) te tm)
   | match_state_seq:
       forall fn s1 s2 k e m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz
       (TRF: transl_funbody cenv sz fn = OK tfn)
-      (TR: transl_stmt cenv xenv s1 = OK ts1)
-      (MINJ: mem_inject f m tm)
-      (MCS: match_callstack f
-               (mkframe cenv e te sp lo hi :: cs)
-               m.(nextblock) tm.(nextblock) m)
-      (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs),
+      (TR: transl_stmt fn.(fn_return) cenv xenv s1 = OK ts1)
+      (MINJ: Mem.inject f m tm)
+      (MCS: match_callstack f m tm
+               (Frame cenv tfn e te sp lo hi :: cs)
+               (Mem.nextblock m) (Mem.nextblock tm))
+      (MK: match_cont (Csharpminor.Kseq s2 k) tk fn.(fn_return) cenv xenv cs),
       match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e m)
                    (State tfn ts1 tk (Vptr sp Int.zero) te tm)
   | match_callstate:
       forall fd args k m tfd targs tk tm f cs cenv
       (TR: transl_fundef gce fd = OK tfd)
-      (MINJ: mem_inject f m tm)
-      (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m)
-      (MK: match_cont k tk cenv nil cs)
+      (MINJ: Mem.inject f m tm)
+      (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm))
+      (MK: match_cont k tk (Csharpminor.funsig fd).(sig_res) cenv nil cs)
       (ISCC: Csharpminor.is_call_cont k)
-      (ARGSINJ: val_list_inject f args targs),
+      (ARGSINJ: val_list_inject f args targs)
+      (ARGSTY: Val.has_type_list args (Csharpminor.funsig fd).(sig_args)),
       match_states (Csharpminor.Callstate fd args k m)
                    (Callstate tfd targs tk tm)
   | match_returnstate:
-      forall v k m tv tk tm f cs cenv
-      (MINJ: mem_inject f m tm)
-      (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m)
-      (MK: match_cont k tk cenv nil cs)
-      (RESINJ: val_inject f v tv),
+      forall v k m tv tk tm f cs ty cenv
+      (MINJ: Mem.inject f m tm)
+      (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm))
+      (MK: match_cont k tk ty cenv nil cs)
+      (RESINJ: val_inject f v tv)
+      (RESTY: Val.has_type v (typ_of_opttyp ty)),
       match_states (Csharpminor.Returnstate v k m)
                    (Returnstate tv tk tm).
 
-Remark nextblock_freelist:
-  forall lb m, nextblock (free_list m lb) = nextblock m.
-Proof. induction lb; intros; simpl; auto. Qed. 
-
 Remark val_inject_function_pointer:
   forall v fd f tv,
   Genv.find_funct tge v = Some fd ->
@@ -2052,22 +2530,22 @@ Proof.
 Qed.
 
 Lemma match_call_cont:
-  forall k tk cenv xenv cs,
-  match_cont k tk cenv xenv cs ->
-  match_cont (Csharpminor.call_cont k) (call_cont tk) cenv nil cs.
+  forall k tk ty cenv xenv cs,
+  match_cont k tk ty cenv xenv cs ->
+  match_cont (Csharpminor.call_cont k) (call_cont tk) ty cenv nil cs.
 Proof.
   induction 1; simpl; auto; econstructor; eauto.
 Qed.
 
 Lemma match_is_call_cont:
-  forall tfn te sp tm k tk cenv xenv cs,
-  match_cont k tk cenv xenv cs ->
+  forall tfn te sp tm k tk ty cenv xenv cs,
+  match_cont k tk ty cenv xenv cs ->
   Csharpminor.is_call_cont k ->
   exists tk',
     star step tge (State tfn Sskip tk sp te tm)
                E0 (State tfn Sskip tk' sp te tm)
     /\ is_call_cont tk'
-    /\ match_cont k tk' cenv nil cs.
+    /\ match_cont k tk' ty cenv nil cs.
 Proof.
   induction 1; simpl; intros; try contradiction.
   econstructor; split. apply star_refl. split. exact I. econstructor; eauto.
@@ -2080,8 +2558,6 @@ Qed.
 
 (** Properties of [switch] compilation *)
 
-Require Import Switch.
-
 Remark switch_table_shift:
   forall n sl base dfl,
   switch_target n (S dfl) (switch_table sl (S base)) =
@@ -2097,20 +2573,20 @@ Proof.
   induction sl; intros; simpl. auto. decEq; auto.
 Qed.
 
-Inductive transl_lblstmt_cont (cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop :=
+Inductive transl_lblstmt_cont (ty: option typ) (cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop :=
   | tlsc_default: forall s k ts,
-      transl_stmt cenv (switch_env (LSdefault s) xenv) s = OK ts ->
-      transl_lblstmt_cont cenv xenv (LSdefault s) k (Kblock (Kseq ts k))
+      transl_stmt ty cenv (switch_env (LSdefault s) xenv) s = OK ts ->
+      transl_lblstmt_cont ty cenv xenv (LSdefault s) k (Kblock (Kseq ts k))
   | tlsc_case: forall i s ls k ts k',
-      transl_stmt cenv (switch_env (LScase i s ls) xenv) s = OK ts ->
-      transl_lblstmt_cont cenv xenv ls k k' ->
-      transl_lblstmt_cont cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')).
+      transl_stmt ty cenv (switch_env (LScase i s ls) xenv) s = OK ts ->
+      transl_lblstmt_cont ty cenv xenv ls k k' ->
+      transl_lblstmt_cont ty cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')).
 
 Lemma switch_descent:
-  forall cenv xenv k ls body s,
-  transl_lblstmt cenv (switch_env ls xenv) ls body = OK s ->
+  forall ty cenv xenv k ls body s,
+  transl_lblstmt ty cenv (switch_env ls xenv) ls body = OK s ->
   exists k',
-  transl_lblstmt_cont cenv xenv ls k k'
+  transl_lblstmt_cont ty cenv xenv ls k k'
   /\ (forall f sp e m,
       plus step tge (State f s k sp e m) E0 (State f body k' sp e m)).
 Proof.
@@ -2127,14 +2603,14 @@ Proof.
 Qed.
 
 Lemma switch_ascent:
-  forall f n sp e m cenv xenv k ls k1,
+  forall f n sp e m ty cenv xenv k ls k1,
   let tbl := switch_table ls O in
   let ls' := select_switch n ls in
-  transl_lblstmt_cont cenv xenv ls k k1 ->
+  transl_lblstmt_cont ty cenv xenv ls k k1 ->
   exists k2,
   star step tge (State f (Sexit (switch_target n (length tbl) tbl)) k1 sp e m)
              E0 (State f (Sexit O) k2 sp e m)
-  /\ transl_lblstmt_cont cenv xenv ls' k k2.
+  /\ transl_lblstmt_cont ty cenv xenv ls' k k2.
 Proof.
   induction ls; intros; unfold tbl, ls'; simpl.
   inv H. econstructor; split. apply star_refl. econstructor; eauto.
@@ -2151,10 +2627,10 @@ Proof.
 Qed.
 
 Lemma switch_match_cont:
-  forall cenv xenv k cs tk ls tk',
-  match_cont k tk cenv xenv cs ->
-  transl_lblstmt_cont cenv xenv ls tk tk' ->
-  match_cont (Csharpminor.Kseq (seq_of_lbl_stmt ls) k) tk' cenv (false :: switch_env ls xenv) cs.
+  forall ty cenv xenv k cs tk ls tk',
+  match_cont k tk ty cenv xenv cs ->
+  transl_lblstmt_cont ty cenv xenv ls tk tk' ->
+  match_cont (Csharpminor.Kseq (seq_of_lbl_stmt ls) k) tk' ty cenv (false :: switch_env ls xenv) cs.
 Proof.
   induction ls; intros; simpl.
   inv H0. apply match_Kblock2. econstructor; eauto.
@@ -2162,11 +2638,11 @@ Proof.
 Qed.
 
 Lemma transl_lblstmt_suffix:
-  forall n cenv xenv ls body ts,
-  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->
+  forall n ty cenv xenv ls body ts,
+  transl_lblstmt ty cenv (switch_env ls xenv) ls body = OK ts ->
   let ls' := select_switch n ls in
   exists body', exists ts',
-  transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'.
+  transl_lblstmt ty cenv (switch_env ls' xenv) ls' body' = OK ts'.
 Proof.
   induction ls; simpl; intros. 
   monadInv H.
@@ -2180,13 +2656,13 @@ Qed.
 Lemma switch_match_states:
   forall fn k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz ls body tk'
     (TRF: transl_funbody cenv sz fn = OK tfn)
-    (TR: transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts)
-    (MINJ: mem_inject f m tm)
-    (MCS: match_callstack f
-             (mkframe cenv e te sp lo hi :: cs)
-             m.(nextblock) tm.(nextblock) m)
-    (MK: match_cont k tk cenv xenv cs)
-    (TK: transl_lblstmt_cont cenv xenv ls tk tk'),
+    (TR: transl_lblstmt (fn_return fn) cenv (switch_env ls xenv) ls body = OK ts)
+    (MINJ: Mem.inject f m tm)
+    (MCS: match_callstack f m tm
+               (Frame cenv tfn e te sp lo hi :: cs)
+               (Mem.nextblock m) (Mem.nextblock tm))
+    (MK: match_cont k tk (fn_return fn) cenv xenv cs)
+    (TK: transl_lblstmt_cont (fn_return fn) cenv xenv ls tk tk'),
   exists S,
   plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S
   /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e m) S.
@@ -2206,22 +2682,35 @@ Qed.
 Section FIND_LABEL.
 
 Variable lbl: label.
+Variable ty: option typ.
 Variable cenv: compilenv.
 Variable cs: callstack.
 
 Remark find_label_var_set:
-  forall id e s k,
-  var_set cenv id e = OK s ->
+  forall id e chunk s k,
+  var_set cenv id e chunk = OK s ->
   find_label lbl s k = None.
 Proof.
   intros. unfold var_set in H.
-  destruct (cenv!!id); monadInv H; reflexivity.
+  destruct (cenv!!id); try (monadInv H; reflexivity).
+  destruct (chunktype_compat chunk m). inv H; auto. 
+  destruct (typ_eq (type_of_chunk m) (type_of_chunk chunk)); inv H; auto.
+Qed.
+
+Remark find_label_var_set_self:
+  forall id ty s k,
+  var_set_self cenv id ty = OK s ->
+  find_label lbl s k = None.
+Proof.
+  intros. unfold var_set_self in H.
+  destruct (cenv!!id); try (monadInv H; reflexivity).
+  destruct (typ_eq (type_of_chunk m) ty0); inv H; reflexivity.
 Qed.
 
 Lemma transl_lblstmt_find_label_context:
-  forall cenv xenv ls body ts tk1 tk2 ts' tk',
-  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->
-  transl_lblstmt_cont cenv xenv ls tk1 tk2 ->
+  forall xenv ls body ts tk1 tk2 ts' tk',
+  transl_lblstmt ty cenv (switch_env ls xenv) ls body = OK ts ->
+  transl_lblstmt_cont ty cenv xenv ls tk1 tk2 ->
   find_label lbl body tk2 = Some (ts', tk') ->
   find_label lbl ts tk1 = Some (ts', tk').
 Proof.
@@ -2234,30 +2723,30 @@ Qed.
 
 Lemma transl_find_label:
   forall s k xenv ts tk,
-  transl_stmt cenv xenv s = OK ts ->
-  match_cont k tk cenv xenv cs ->
+  transl_stmt ty cenv xenv s = OK ts ->
+  match_cont k tk ty cenv xenv cs ->
   match Csharpminor.find_label lbl s k with
   | None => find_label lbl ts tk = None
   | Some(s', k') =>
       exists ts', exists tk', exists xenv',
         find_label lbl ts tk = Some(ts', tk')
-     /\ transl_stmt cenv xenv' s' = OK ts'
-     /\ match_cont k' tk' cenv xenv' cs
+     /\ transl_stmt ty cenv xenv' s' = OK ts'
+     /\ match_cont k' tk' ty cenv xenv' cs
   end
 
 with transl_lblstmt_find_label:
   forall ls xenv body k ts tk tk1,
-  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->
-  match_cont k tk cenv xenv cs ->
-  transl_lblstmt_cont cenv xenv ls tk tk1 ->
+  transl_lblstmt ty cenv (switch_env ls xenv) ls body = OK ts ->
+  match_cont k tk ty cenv xenv cs ->
+  transl_lblstmt_cont ty cenv xenv ls tk tk1 ->
   find_label lbl body tk1 = None ->
   match Csharpminor.find_label_ls lbl ls k with
   | None => find_label lbl ts tk = None
   | Some(s', k') =>
       exists ts', exists tk', exists xenv',
         find_label lbl ts tk = Some(ts', tk')
-     /\ transl_stmt cenv xenv' s' = OK ts'
-     /\ match_cont k' tk' cenv xenv' cs
+     /\ transl_stmt ty cenv xenv' s' = OK ts'
+     /\ match_cont k' tk' ty cenv xenv' cs
   end.
 Proof.
   intros. destruct s; try (monadInv H); simpl; auto.
@@ -2265,7 +2754,10 @@ Proof.
   eapply find_label_var_set; eauto.
   (* call *)
   destruct o; monadInv H; simpl; auto.
-  eapply find_label_var_set; eauto.
+  destruct (list_eq_dec typ_eq x1 (sig_args s)); monadInv EQ4.
+  simpl. eapply find_label_var_set_self; eauto.
+  destruct (list_eq_dec typ_eq x1 (sig_args s)); monadInv EQ3.
+  simpl; eauto.
   (* seq *)
   exploit (transl_find_label s1). eauto. eapply match_Kseq. eexact EQ1. eauto.  
   destruct (Csharpminor.find_label lbl s1 (Csharpminor.Kseq s2 k)) as [[s' k'] | ].
@@ -2287,6 +2779,7 @@ Proof.
   eapply transl_lblstmt_find_label. eauto. eauto. eauto. reflexivity.  
   (* return *)
   destruct o; monadInv H; auto.
+  destruct (typ_eq x0 (typ_of_opttyp ty)); monadInv EQ2; auto.
   (* label *)
   destruct (ident_eq lbl l).
   exists x; exists tk; exists xenv; auto.
@@ -2316,7 +2809,7 @@ Proof.
   induction vars; intros.
   monadInv H. auto.
   simpl in H. destruct a as [id lv]. monadInv H.
-  simpl. rewrite (find_label_var_set id (Evar id)); auto.
+  simpl. rewrite (find_label_var_set_self id (type_of_chunk lv)); auto.
 Qed.
 
 End FIND_LABEL.
@@ -2324,12 +2817,12 @@ End FIND_LABEL.
 Lemma transl_find_label_body:
   forall cenv xenv size f tf k tk cs lbl s' k',
   transl_funbody cenv size f = OK tf ->
-  match_cont k tk cenv xenv cs ->
+  match_cont k tk (fn_return f) cenv xenv cs ->
   Csharpminor.find_label lbl f.(Csharpminor.fn_body) (Csharpminor.call_cont k) = Some (s', k') ->
   exists ts', exists tk', exists xenv',
      find_label lbl tf.(fn_body) (call_cont tk) = Some(ts', tk')
-  /\ transl_stmt cenv xenv' s' = OK ts'
-  /\ match_cont k' tk' cenv xenv' cs.
+  /\ transl_stmt (fn_return f) cenv xenv' s' = OK ts'
+  /\ match_cont k' tk' (fn_return f) cenv xenv' cs.
 Proof.
   intros. monadInv H. simpl. 
   rewrite (find_label_store_parameters lbl cenv (Csharpminor.fn_params f)); auto.
@@ -2337,8 +2830,7 @@ Proof.
   instantiate (1 := lbl). rewrite H1. auto.
 Qed.
 
-
-Require Import Coq.Program.Equality.
+(** The simulation diagram. *)
 
 Fixpoint seq_left_depth (s: Csharpminor.stmt) : nat :=
   match s with
@@ -2384,16 +2876,17 @@ Proof.
 (* skip call *)
   monadInv TR. left.
   exploit match_is_call_cont; eauto. intros [tk' [A [B C]]]. 
-  exploit match_callstack_freelist; eauto. intros [P Q].
+  exploit match_callstack_freelist; eauto. intros [tm' [P [Q R]]].
   econstructor; split.
   eapply plus_right. eexact A. apply step_skip_call. auto.
-  rewrite (sig_preserved_body _ _ _ _ TRF). auto. traceEq.
-  econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. 
+  rewrite (sig_preserved_body _ _ _ _ TRF). auto. eauto. traceEq.
+  econstructor; eauto. exact I.
 
 (* assign *)
   monadInv TR. 
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
-  exploit var_set_correct; eauto. intros [te' [tm' [EXEC [MINJ' [MCS' OTHER]]]]].
+  exploit var_set_correct; eauto. eapply chunktype_expr_correct; eauto.
+  intros [te' [tm' [EXEC [MINJ' [MCS' OTHER]]]]].
   left; econstructor; split.
   apply plus_one. eexact EXEC.
   econstructor; eauto. 
@@ -2405,19 +2898,20 @@ Proof.
   exploit transl_expr_correct. eauto. eauto. eexact H0. eauto. 
   intros [tv2 [EVAL2 VINJ2]].
   exploit make_store_correct. eexact EVAL1. eexact EVAL2. eauto. eauto. auto. auto.
-  intros [tm' [EXEC [MINJ' NEXTBLOCK]]].
+  intros [tm' [tv' [EXEC [STORE' MINJ']]]].
   left; econstructor; split.
   apply plus_one. eexact EXEC.
-  unfold storev in H1; destruct vaddr; try discriminate.
   econstructor; eauto.
-  replace (nextblock m') with (nextblock m). rewrite NEXTBLOCK. eauto.
-  eapply match_callstack_mapped; eauto. inv VINJ1. congruence.
-  symmetry. eapply nextblock_store; eauto.
+  eapply match_callstack_storev_mapped. eexact VINJ1. eauto. eauto.
+  rewrite (nextblock_storev _ _ _ _ _ H1).
+  rewrite (nextblock_storev _ _ _ _ _ STORE').
+  eauto. 
 
 (* call *)
   simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]].
   simpl in TR. destruct optid; monadInv TR.
 (* with return value *)
+  destruct (list_eq_dec typ_eq x1 (sig_args (Csharpminor.funsig fd))); monadInv EQ4.
   exploit transl_expr_correct; eauto.
   intros [tvf [EVAL1 VINJ1]].
   assert (tvf = vf).
@@ -2434,7 +2928,10 @@ Proof.
   econstructor; eauto.
   eapply match_Kcall_some with (cenv' := cenv); eauto.
   red; auto.
+  eapply type_exprlist_correct; eauto.
+  
 (* without return value *)
+  destruct (list_eq_dec typ_eq x1 (sig_args (Csharpminor.funsig fd))); monadInv EQ3.
   exploit transl_expr_correct; eauto.
   intros [tvf [EVAL1 VINJ1]].
   assert (tvf = vf).
@@ -2450,6 +2947,7 @@ Proof.
   econstructor; eauto.
   eapply match_Kcall_none with (cenv' := cenv); eauto.
   red; auto.
+  eapply type_exprlist_correct; eauto.
 
 (* seq *)
   monadInv TR. 
@@ -2531,23 +3029,21 @@ Proof.
 
 (* return none *)
   monadInv TR. left.
-  exploit match_callstack_freelist; eauto. intros [A B].
+  exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
   econstructor; split.
-  apply plus_one. apply step_return_0.
-(* 
-  rewrite (sig_preserved_body _ _ _ _ TRF). auto.
-*)
-  econstructor; eauto. rewrite nextblock_freelist. simpl. eauto.
-  eapply match_call_cont; eauto.
+  apply plus_one. eapply step_return_0. eauto.
+  econstructor; eauto. eapply match_call_cont; eauto.
+  simpl; auto.
 
 (* return some *)
-  monadInv TR. left. 
+  monadInv TR. destruct (typ_eq x0 (typ_of_opttyp (fn_return f))); monadInv EQ2.
+  left. 
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
-  exploit match_callstack_freelist; eauto. intros [A B].
+  exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
   econstructor; split.
-  apply plus_one. apply step_return_1. eauto. 
-  econstructor; eauto. rewrite nextblock_freelist. simpl. eauto.
-  eapply match_call_cont; eauto.
+  apply plus_one. eapply step_return_1. eauto. eauto. 
+  econstructor; eauto. eapply match_call_cont; eauto.
+  eapply type_expr_correct; eauto.
 
 (* label *)
   monadInv TR.
@@ -2569,8 +3065,11 @@ Proof.
   destruct (zle sz Int.max_signed); try congruence.
   intro TRBODY.
   generalize TRBODY; intro TMP. monadInv TMP.
-  caseEq (alloc tm 0 sz). intros tm' sp ALLOC'.
-  exploit function_entry_ok; eauto. 
+  set (tf := mkfunction (Csharpminor.fn_sig f) (fn_params_names f)
+              (make_vars (fn_params_names f) (fn_vars_names f) (Sseq x1 x0))
+              sz (Sseq x1 x0)) in *.
+  caseEq (Mem.alloc tm 0 (fn_stackspace tf)). intros tm' sp ALLOC'.
+  exploit function_entry_ok; eauto; simpl; auto.  
   intros [f2 [te2 [tm2 [EXEC [MINJ2 [IINCR MCS2]]]]]].
   left; econstructor; split.
   eapply plus_left. constructor; simpl; eauto. 
@@ -2583,10 +3082,19 @@ Proof.
 
 (* external call *)
   monadInv TR. 
-  exploit event_match_inject; eauto. intros [A B].
+  exploit external_call_mem_inject; eauto. 
+  intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
   econstructor; eauto.
+  apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
+  eapply match_callstack_external_call; eauto.
+  intros. eapply external_call_bounds; eauto.
+  omega. omega.
+  eapply external_call_nextblock_incr; eauto.
+  eapply external_call_nextblock_incr; eauto.
+  simpl. change (Val.has_type vres (proj_sig_res (ef_sig ef))). 
+  eapply external_call_well_typed; eauto.
 
 (* return *)
   inv MK; inv H.
@@ -2595,26 +3103,29 @@ Proof.
   apply plus_one. econstructor; eauto. 
   simpl. econstructor; eauto. 
   (* one argument *)
-  exploit var_set_self_correct; eauto.
-  intros [te' [tm' [A [B C]]]].
+  exploit var_set_self_correct. eauto. eauto. eauto. eauto. eauto. eauto.
+  instantiate (1 := PTree.set id tv te). apply PTree.gss. 
+  intros; apply PTree.gso; auto.
+  intros [te' [tm' [A [B [C D]]]]].
   left; econstructor; split.
   eapply plus_left. econstructor. simpl. eapply star_left. econstructor.
   eapply star_one. eexact A.
   reflexivity. traceEq.
-  econstructor; eauto. 
+  econstructor; eauto.
 Qed.
 
 Lemma match_globalenvs_init:
-  let m := Genv.init_mem prog in
-  match_globalenvs (meminj_init m).
+  forall m,
+  Genv.init_mem prog = Some m ->
+  match_globalenvs (Mem.flat_inj (Mem.nextblock m)).
 Proof.
   intros. constructor.
   intros. split.
-  unfold meminj_init. rewrite zlt_true. auto.
-  unfold m; eapply Genv.find_symbol_not_fresh; eauto.
-  rewrite <- H. apply symbols_preserved.
-  intros. unfold meminj_init. rewrite zlt_true. auto.
-  generalize (nextblock_pos m). omega.
+  unfold Mem.flat_inj. rewrite zlt_true. auto.
+  eapply Genv.find_symbol_not_fresh; eauto.
+  rewrite <- H0. apply symbols_preserved.
+  intros. unfold Mem.flat_inj. rewrite zlt_true. auto.
+  generalize (Mem.nextblock_pos m). omega.
 Qed.
 
 Lemma transl_initial_states:
@@ -2625,21 +3136,19 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor.
+  apply (Genv.init_mem_transf_partial2 _ _ _ TRANSL). eauto. 
   simpl. fold tge. rewrite symbols_preserved.
-  replace (prog_main tprog) with (prog_main prog). eexact H.
+  replace (prog_main tprog) with (prog_main prog). eexact H0.
   symmetry. unfold transl_program in TRANSL.
   eapply transform_partial_program2_main; eauto.
   eexact FIND. 
-  rewrite <- H1. apply sig_preserved; auto.
-  rewrite (Genv.init_mem_transf_partial2 _ _ _ TRANSL). 
-  fold m0.
-  eapply match_callstate with (f := meminj_init m0) (cs := @nil frame).
+  rewrite <- H2. apply sig_preserved; auto.
+  eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame).
   auto.
-  apply init_inject. unfold m0. apply Genv.initmem_inject_neutral.
-  constructor. apply match_globalenvs_init. 
+  eapply Genv.initmem_inject; eauto.
+  constructor. apply match_globalenvs_init. auto.  
   instantiate (1 := gce). constructor.
-  red; auto.
-  constructor.
+  red; auto. constructor. rewrite H2; simpl; auto. 
 Qed.
 
 Lemma transl_final_states:
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index f352df7..bd26b0f 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -22,7 +22,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 Require Import AST.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Csyntax.
@@ -294,8 +294,8 @@ Function sem_cmp (c:comparison)
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2))
       | Vptr b1 ofs1,  Vptr b2 ofs2  =>
-          if valid_pointer m b1 (Int.signed ofs1)
-          && valid_pointer m b2 (Int.signed ofs2) then
+          if Mem.valid_pointer m b1 (Int.signed ofs1)
+          && Mem.valid_pointer m b2 (Int.signed ofs2) then
             if zeq b1 b2
             then Some (Val.of_bool (Int.cmp c ofs1 ofs2))
             else sem_cmp_mismatch c
@@ -412,15 +412,15 @@ Inductive cast : val -> type -> type -> val -> Prop :=
   maps names of functions and global variables to memory block references,
   and function pointers to their definitions.  (See module [Globalenvs].) *)
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef type.
 
 (** The local environment maps local variables to block references.
   The current value of the variable is stored in the associated memory
   block. *)
 
-Definition env := PTree.t block. (* map variable -> location *)
+Definition env := PTree.t (block * type). (* map variable -> location & type *)
 
-Definition empty_env: env := (PTree.empty block).
+Definition empty_env: env := (PTree.empty (block * type)).
 
 (** [load_value_of_type ty m b ofs] computes the value of a datum
   of type [ty] residing in memory [m] at block [b], offset [ofs].
@@ -463,7 +463,7 @@ Inductive alloc_variables: env -> mem ->
   | alloc_variables_cons:
       forall e m id ty vars m1 b1 m2 e2,
       Mem.alloc m 0 (sizeof ty) = (m1, b1) ->
-      alloc_variables (PTree.set id b1 e) m1 vars e2 m2 ->
+      alloc_variables (PTree.set id (b1, ty) e) m1 vars e2 m2 ->
       alloc_variables e m ((id, ty) :: vars) e2 m2.
 
 (** Initialization of local variables that are parameters to a function.
@@ -479,15 +479,18 @@ Inductive bind_parameters: env ->
       bind_parameters e m nil nil m
   | bind_parameters_cons:
       forall e m id ty params v1 vl b m1 m2,
-      PTree.get id e = Some b ->
+      PTree.get id e = Some(b, ty) ->
       store_value_of_type ty m b Int.zero v1 = Some m1 ->
       bind_parameters e m1 params vl m2 ->
       bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2.
 
-(** Return the list of blocks in the codomain of [e]. *)
+(** Return the list of blocks in the codomain of [e], with low and high bounds. *)
 
-Definition blocks_of_env (e: env) : list block :=
-  List.map (@snd ident block) (PTree.elements e).
+Definition block_of_binding (id_b_ty: ident * (block * type)) :=
+  match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ty) end.
+
+Definition blocks_of_env (e: env) : list (block * Z * Z) :=
+  List.map block_of_binding (PTree.elements e).
 
 (** Selection of the appropriate case of a [switch], given the value [n]
   of the selector expression. *)
@@ -586,7 +589,7 @@ Inductive eval_expr: expr -> val -> Prop :=
 
 with eval_lvalue: expr -> block -> int -> Prop :=
   | eval_Evar_local:   forall id l ty,
-      e!id = Some l ->
+      e!id = Some(l, ty) ->
       eval_lvalue (Expr (Evar id) ty) l Int.zero
   | eval_Evar_global: forall id l ty,
       e!id = None ->
@@ -844,20 +847,23 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f Sskip (Kfor3 a2 a3 s k) e m)
         E0 (State f (Sfor Sskip a2 a3 s) k e m)
 
-  | step_return_0: forall f k e m,
+  | step_return_0: forall f k e m m',
       f.(fn_return) = Tvoid ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f (Sreturn None) k e m)
-        E0 (Returnstate Vundef (call_cont k) (Mem.free_list m (blocks_of_env e)))
-  | step_return_1: forall f a k e m v,
+        E0 (Returnstate Vundef (call_cont k) m')
+  | step_return_1: forall f a k e m v m',
       f.(fn_return) <> Tvoid ->
       eval_expr e m a v ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f (Sreturn (Some a)) k e m)
-        E0 (Returnstate v (call_cont k) (Mem.free_list m (blocks_of_env e)))
-  | step_skip_call: forall f k e m,
+        E0 (Returnstate v (call_cont k) m')
+  | step_skip_call: forall f k e m m',
       is_call_cont k ->
       f.(fn_return) = Tvoid ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f Sskip k e m)
-        E0 (Returnstate Vundef k (Mem.free_list m (blocks_of_env e)))
+        E0 (Returnstate Vundef k m')
 
   | step_switch: forall f a sl k e m n,
       eval_expr e m a (Vint n) ->
@@ -886,10 +892,10 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k e m2)
 
-  | step_external_function: forall id targs tres vargs k m vres t,
-      event_match (external_function id targs tres) vargs t vres ->
+  | step_external_function: forall id targs tres vargs k m vres t m',
+      external_call (external_function id targs tres) vargs m t vres m' ->
       step (Callstate (External id targs tres) vargs k m)
-         t (Returnstate vres k m)
+         t (Returnstate vres k m')
 
   | step_returnstate_0: forall v f e k m,
       step (Returnstate v (Kcall None f e k) m)
@@ -1084,15 +1090,16 @@ Inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop
   by the call.  *)
 
 with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
-  | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres,
+  | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres m4,
       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       bind_parameters e m1 f.(fn_params) vargs m2 ->
       exec_stmt e m2 f.(fn_body) t m3 out ->
       outcome_result_value out f.(fn_return) vres ->
-      eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres
-  | eval_funcall_external: forall m id targs tres vargs t vres,
-      event_match (external_function id targs tres) vargs t vres ->
-      eval_funcall m (External id targs tres) vargs t m vres.
+      Mem.free_list m3 (blocks_of_env e) = Some m4 ->
+      eval_funcall m (Internal f) vargs t m4 vres
+  | eval_funcall_external: forall m id targs tres vargs t vres m',
+      external_call (external_function id targs tres) vargs m t vres m' ->
+      eval_funcall m (External id targs tres) vargs t m' vres.
 
 Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
   with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
@@ -1212,9 +1219,9 @@ End SEMANTICS.
   without arguments and with an empty continuation. *)
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       initial_state p (Callstate f nil Kstop m0).
@@ -1236,18 +1243,18 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
 (** Big-step execution of a whole program.  *)
 
 Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
-  | bigstep_program_terminates_intro: forall b f m1 t r,
+  | bigstep_program_terminates_intro: forall b f m0 m1 t r,
       let ge := Genv.globalenv p in 
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       eval_funcall ge m0 f nil t m1 (Vint r) ->
       bigstep_program_terminates p t r.
 
 Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
-  | bigstep_program_diverges_intro: forall b f t,
+  | bigstep_program_diverges_intro: forall b f m0 t,
       let ge := Genv.globalenv p in 
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       evalinf_funcall ge m0 f nil t ->
@@ -1525,16 +1532,16 @@ Proof.
   (* Out_normal *)
   assert (fn_return f = Tvoid /\ vres = Vundef).
     destruct (fn_return f); auto || contradiction.
-  destruct H5. subst vres. apply step_skip_call; auto.
+  destruct H6. subst vres. apply step_skip_call; auto.
   (* Out_return None *)
   assert (fn_return f = Tvoid /\ vres = Vundef).
     destruct (fn_return f); auto || contradiction.
-  destruct H6. subst vres.
-  rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
+  destruct H7. subst vres.
+  rewrite <- (is_call_cont_call_cont k H5). rewrite <- H6.
   apply step_return_0; auto.
   (* Out_return Some *)
   destruct H3. subst vres.
-  rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
+  rewrite <- (is_call_cont_call_cont k H5). rewrite <- H6.
   eapply step_return_1; eauto.
   reflexivity. traceEq.
 
@@ -1697,9 +1704,9 @@ Qed.
 Theorem bigstep_program_terminates_exec:
   forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
 Proof.
-  intros. inv H. unfold ge0, m0 in *. 
+  intros. inv H. 
   econstructor.
-  econstructor. eauto. eauto.
+  econstructor. eauto. eauto. eauto.
   apply eval_funcall_steps. eauto. red; auto. 
   econstructor.
 Qed.
@@ -1717,7 +1724,7 @@ Proof.
     eapply evalinf_funcall_forever; eauto. 
   destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
   as [A | [t [s' [T' [B [C D]]]]]]. 
-  left. econstructor. econstructor. eauto. eauto. auto.
+  left. econstructor. econstructor; eauto. eauto.
   right. exists t. split.
   econstructor. econstructor; eauto. eauto. auto. 
   subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 5cdbd84..2fddc6c 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -18,7 +18,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Cminor.
@@ -89,13 +89,24 @@ Inductive var_kind : Type :=
   | Vscalar: memory_chunk -> var_kind
   | Varray: Z -> var_kind.
 
-(** Functions are composed of a signature, a list of parameter names
+Definition sizeof (lv: var_kind) : Z :=
+  match lv with
+  | Vscalar chunk => size_chunk chunk
+  | Varray sz => Zmax 0 sz
+  end.
+
+(** Functions are composed of a return type, a list of parameter names
   with associated memory chunks (parameters must be scalar), a list of
   local variables with associated [var_kind] description, and a
   statement representing the function body.  *)
 
+Definition param_name (p: ident * memory_chunk) := fst p.
+Definition param_chunk (p: ident * memory_chunk) := snd p.
+Definition variable_name (v: ident * var_kind) := fst v.
+Definition variable_kind (v: ident * var_kind) := snd v.
+
 Record function : Type := mkfunction {
-  fn_sig: signature;
+  fn_return: option typ;
   fn_params: list (ident * memory_chunk);
   fn_vars: list (ident * var_kind);
   fn_body: stmt
@@ -105,12 +116,25 @@ Definition fundef := AST.fundef function.
 
 Definition program : Type := AST.program fundef var_kind.
 
+Definition fn_sig (f: function) :=
+  mksignature (List.map type_of_chunk (List.map param_chunk f.(fn_params)))
+              f.(fn_return).
+
 Definition funsig (fd: fundef) :=
   match fd with
-  | Internal f => f.(fn_sig)
-  | External ef => ef.(ef_sig)
+  | Internal f => fn_sig f
+  | External ef => ef_sig ef
   end.
 
+Definition var_of_param (p: ident * memory_chunk) : ident * var_kind :=
+  (fst p, Vscalar (snd p)).
+
+Definition fn_variables (f: function) :=
+  List.map var_of_param f.(fn_params) ++ f.(fn_vars).
+
+Definition fn_params_names (f: function) := List.map param_name f.(fn_params).
+Definition fn_vars_names (f: function) := List.map variable_name f.(fn_vars).
+
 (** * Operational semantics *)
 
 (** Three kinds of evaluation environments are involved:
@@ -120,28 +144,11 @@ Definition funsig (fd: fundef) :=
     to memory blocks and variable informations.
 *)
 
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef var_kind.
 Definition gvarenv := PTree.t var_kind.
 Definition env := PTree.t (block * var_kind).
 Definition empty_env : env := PTree.empty (block * var_kind).
 
-Definition sizeof (lv: var_kind) : Z :=
-  match lv with
-  | Vscalar chunk => size_chunk chunk
-  | Varray sz => Zmax 0 sz
-  end.
-
-Definition fn_variables (f: function) :=
-  List.map
-    (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) f.(fn_params)
-  ++ f.(fn_vars).
-
-Definition fn_params_names (f: function) :=
-  List.map (@fst ident memory_chunk) f.(fn_params).
-
-Definition fn_vars_names (f: function) :=
-  List.map (@fst ident var_kind) f.(fn_vars).
-
 (** Continuations *)
 
 Inductive cont: Type :=
@@ -256,8 +263,8 @@ Definition eval_binop (op: binary_operation)
                       (arg1 arg2: val) (m: mem): option val :=
   match op, arg1, arg2 with
   | Cminor.Ocmp c, Vptr b1 n1, Vptr b2 n2 =>
-      if valid_pointer m b1 (Int.signed n1)
-      && valid_pointer m b2 (Int.signed n2)
+      if Mem.valid_pointer m b1 (Int.signed n1)
+      && Mem.valid_pointer m b2 (Int.signed n2)
       then Cminor.eval_binop op arg1 arg2
       else None
   | _, _, _ =>
@@ -279,11 +286,13 @@ Inductive alloc_variables: env -> mem ->
       alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 ->
       alloc_variables e m ((id, lv) :: vars) e2 m2.
 
-(** List of blocks mentioned in an environment *)
+(** List of blocks mentioned in an environment, with low and high bounds *)
+
+Definition block_of_binding (id_b_lv: ident * (block * var_kind)) :=
+  match id_b_lv with (id, (b, lv)) => (b, 0, sizeof lv) end.
 
-Definition blocks_of_env (e: env) : list block :=
-  List.map (fun id_b_lv => match id_b_lv with (id, (b, lv)) => b end)
-           (PTree.elements e).
+Definition blocks_of_env (e: env) : list (block * Z * Z) :=
+  List.map block_of_binding (PTree.elements e).
 
 (** Initialization of local variables that are parameters.  The value
   of the corresponding argument is stored into the memory block
@@ -418,11 +427,12 @@ Inductive step: state -> trace -> state -> Prop :=
   | step_skip_block: forall f k e m,
       step (State f Sskip (Kblock k) e m)
         E0 (State f Sskip k e m)
-  | step_skip_call: forall f k e m,
+  | step_skip_call: forall f k e m m',
       is_call_cont k ->
-      f.(fn_sig).(sig_res) = None ->
+      f.(fn_return) = None ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f Sskip k e m)
-        E0 (Returnstate Vundef k (Mem.free_list m (blocks_of_env e)))
+        E0 (Returnstate Vundef k m')
 
   | step_assign: forall f id a k e m m' v,
       eval_expr e m a v ->
@@ -478,18 +488,17 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sswitch a cases) k e m)
         E0 (State f (seq_of_lbl_stmt (select_switch n cases)) k e m)
 
-  | step_return_0: forall f k e m,
-      f.(fn_sig).(sig_res) = None ->
+  | step_return_0: forall f k e m m',
+      f.(fn_return) = None ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f (Sreturn None) k e m)
-        E0 (Returnstate Vundef (call_cont k)
-                               (Mem.free_list m (blocks_of_env e)))
-  | step_return_1: forall f a k e m v,
-      f.(fn_sig).(sig_res) <> None ->
+        E0 (Returnstate Vundef (call_cont k) m')
+  | step_return_1: forall f a k e m v m',
+      f.(fn_return) <> None ->
       eval_expr e m a v ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
       step (State f (Sreturn (Some a)) k e m)
-        E0 (Returnstate v (call_cont k)
-                          (Mem.free_list m (blocks_of_env e)))
-
+        E0 (Returnstate v (call_cont k) m')
   | step_label: forall f lbl s k e m,
       step (State f (Slabel lbl s) k e m)
         E0 (State f s k e m)
@@ -506,10 +515,10 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k e m2)
 
-  | step_external_function: forall ef vargs k m t vres,
-      event_match ef vargs t vres ->
+  | step_external_function: forall ef vargs k m t vres m',
+      external_call ef vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
-         t (Returnstate vres k m)        
+         t (Returnstate vres k m')        
 
   | step_return: forall v optid f e k m m',
       exec_opt_assign e m optid v m' ->
@@ -524,9 +533,9 @@ End RELSEM.
   without arguments and with an empty continuation. *)
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f,
+  | initial_state_intro: forall b f m0,
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
+      Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index b40b94c..548c8df 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -34,11 +34,6 @@ Open Local Scope error_monad_scope.
 
 (** * Operations on C types *)
 
-Definition signature_of_function (f: Csyntax.function) : signature :=
-  mksignature 
-   (typlist_of_typelist (type_of_params (Csyntax.fn_params f)))
-   (opttyp_of_type (Csyntax.fn_return f)).
-
 Definition chunk_of_type (ty: type): res memory_chunk :=
   match access_mode ty with
   | By_value chunk => OK chunk
@@ -615,7 +610,7 @@ Definition transl_function (f: Csyntax.function) : res function :=
   do tparams <- transl_params (Csyntax.fn_params f);
   do tvars <- transl_vars (Csyntax.fn_vars f);
   do tbody <- transl_statement 1%nat 0%nat (Csyntax.fn_body f);
-  OK (mkfunction (signature_of_function f) tparams tvars tbody).
+  OK (mkfunction (opttyp_of_type (Csyntax.fn_return f)) tparams tvars tbody).
 
 Definition transl_fundef (f: Csyntax.fundef) : res fundef :=
   match f with
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index 86ecd2a..ebc188e 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -20,7 +20,7 @@ Require Import Floats.
 Require Import AST.
 Require Import Values.
 Require Import Events.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Csyntax.
 Require Import Csem.
@@ -31,6 +31,29 @@ Require Import Cshmgen.
 
 (** * Properties of operations over types *)
 
+Remark type_of_chunk_of_type:
+  forall ty chunk,
+  chunk_of_type ty = OK chunk ->
+  type_of_chunk chunk = typ_of_type ty.
+Proof.
+  intros. unfold chunk_of_type in H. destruct ty; simpl in H; try monadInv H.
+  destruct i; destruct s; monadInv H; reflexivity.
+  destruct f; monadInv H; reflexivity.
+  reflexivity. reflexivity. 
+Qed.
+
+Remark transl_params_types:
+  forall p tp,
+  transl_params p = OK tp ->
+  map type_of_chunk (map param_chunk tp) = typlist_of_typelist (type_of_params p).
+Proof.
+  induction p; simpl; intros. 
+  inv H. auto.
+  destruct a as [id ty]. generalize H; clear H. case_eq (chunk_of_type ty); intros.
+  monadInv H0. simpl. f_equal; auto. apply type_of_chunk_of_type; auto.
+  inv H0.
+Qed.
+
 Lemma transl_fundef_sig1:
   forall f tf args res,
   transl_fundef f = OK tf ->
@@ -39,9 +62,10 @@ Lemma transl_fundef_sig1:
 Proof.
   intros. destruct f; monadInv H. 
   monadInv EQ. simpl.  
-  simpl in H0. inversion H0. reflexivity. 
-  simpl. 
-  simpl in H0. congruence.
+  simpl in H0. inversion H0.
+  unfold fn_sig; simpl. unfold signature_of_type. f_equal. 
+  apply transl_params_types; auto.
+  simpl. simpl in H0. congruence.
 Qed.
 
 Lemma transl_fundef_sig2:
@@ -109,7 +133,7 @@ Qed.
 Lemma transl_params_names:
   forall vars tvars,
   transl_params vars = OK tvars ->
-  List.map (@fst ident memory_chunk) tvars = Ctyping.var_names vars.
+  List.map param_name tvars = Ctyping.var_names vars.
 Proof.
   exact (map_partial_names _ _ chunk_of_type).
 Qed.
@@ -117,7 +141,7 @@ Qed.
 Lemma transl_vars_names:
   forall vars tvars,
   transl_vars vars = OK tvars ->
-  List.map (@fst ident var_kind) tvars = Ctyping.var_names vars.
+  List.map variable_name tvars = Ctyping.var_names vars.
 Proof.
   exact (map_partial_names _ _ var_kind_of_type).
 Qed.
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 199192c..769aee7 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -20,7 +20,7 @@ Require Import Floats.
 Require Import AST.
 Require Import Values.
 Require Import Events.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Csyntax.
 Require Import Csem.
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 836f1e4..7e3658b 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -20,7 +20,7 @@ Require Import Floats.
 Require Import AST.
 Require Import Values.
 Require Import Events.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Csyntax.
@@ -52,13 +52,13 @@ Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial2 transl_fundef transl_globvar TRANSL).
+Proof (Genv.find_funct_transf_partial2 transl_fundef transl_globvar _ TRANSL).
 
 Lemma function_ptr_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar TRANSL).
+Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar _ TRANSL).
 
 Lemma functions_well_typed:
   forall v f,
@@ -82,41 +82,24 @@ Proof.
   assumption.
 Qed.
 
-Lemma sig_translated:
-  forall fd tfd targs tres,
-  classify_fun (type_of_fundef fd) = fun_case_f targs tres ->
-  transl_fundef fd = OK tfd ->
-  funsig tfd = signature_of_type targs tres.
-Proof.
-  intros. destruct fd; monadInv H0; inv H. 
-  monadInv EQ. simpl. auto. 
-  simpl. auto.
-Qed.
-
 (** * Matching between environments *)
 
 (** In this section, we define a matching relation between
   a Clight local environment and a Csharpminor local environment,
   parameterized by an assignment of types to the Clight variables. *)
 
-Definition match_var_kind (ty: type) (vk: var_kind) : Prop :=
-  match access_mode ty with
-  | By_value chunk => vk = Vscalar chunk
-  | _ => True
-  end.
-
 Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop :=
   mk_match_env {
     me_local:
-      forall id b,
-      e!id = Some b ->
-      exists vk, exists ty,
+      forall id b ty,
+      e!id = Some (b, ty) ->
+      exists vk,
         tyenv!id = Some ty
-        /\ match_var_kind ty vk
+        /\ var_kind_of_type ty = OK vk
         /\ te!id = Some (b, vk);
     me_local_inv:
       forall id b vk,
-      te!id = Some (b, vk) -> e!id = Some b;
+      te!id = Some (b, vk) -> exists ty, e!id = Some(b, ty);
     me_global:
       forall id ty,
       e!id = None -> tyenv!id = Some ty ->
@@ -124,64 +107,44 @@ Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop :=
       (forall chunk, access_mode ty = By_value chunk -> (global_var_env tprog)!id = Some (Vscalar chunk))
   }.
 
-
 Lemma match_env_same_blocks:
   forall tyenv e te,
   match_env tyenv e te ->
-  forall b, In b (Csem.blocks_of_env e) <-> In b (blocks_of_env te).
-Proof.
-  intros. inv H.
-  unfold Csem.blocks_of_env, blocks_of_env.
-  set (f := (fun id_b_lv : positive * (block * var_kind) =>
-                let (_, y) := id_b_lv in let (b0, _) := y in b0)).
-  split; intros.
-  exploit list_in_map_inv; eauto. intros [[id b'] [A B]]. 
-  simpl in A; subst b'.
-  exploit (me_local0 id b). apply PTree.elements_complete; auto. 
-  intros [vk [ty [C [D E]]]].
-  change b with (f (id, (b, vk))). 
-  apply List.in_map. apply PTree.elements_correct. auto.
-  exploit list_in_map_inv; eauto. intros [[id [b' vk]] [A B]]. 
-  simpl in A; subst b'.
-  exploit (me_local_inv0 id b vk). apply PTree.elements_complete; auto. 
-  intro.
-  change b with (snd (id, b)).
-  apply List.in_map. apply PTree.elements_correct. auto.
-Qed.
-
-Remark free_list_charact:
-  forall l m,
-  free_list m l =
-    mkmem (fun b => if In_dec eq_block b l then empty_block 0 0 else m.(blocks) b)
-          m.(nextblock)
-          m.(nextblock_pos).
+  blocks_of_env te = Csem.blocks_of_env e.
 Proof.
-  induction l; intros; simpl.
-  destruct m; simpl. decEq. apply extensionality. auto.
-  rewrite IHl. unfold free; simpl. decEq. apply extensionality; intro b.
-  unfold update. destruct (eq_block a b). 
-  subst b. apply zeq_true.
-  rewrite zeq_false; auto. 
-  destruct (In_dec eq_block b l); auto.
-Qed.
-
-Lemma mem_free_list_same:
-  forall m l1 l2,
-  (forall b, In b l1 <-> In b l2) ->
-  free_list m l1 = free_list m l2.
-Proof.
-  intros. repeat rewrite free_list_charact. decEq. apply extensionality; intro b.
-  destruct (In_dec eq_block b l1); destruct (In_dec eq_block b l2); auto.
-  rewrite H in i. contradiction.
-  rewrite <- H in i. contradiction.
+  intros.
+  set (R := fun (x: (block * type)) (y: (block * var_kind)) =>
+         match x, y with
+         | (b1, ty), (b2, vk) => b2 = b1 /\ var_kind_of_type ty = OK vk
+         end).
+  assert (list_forall2 
+            (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
+            (PTree.elements e) (PTree.elements te)).
+  apply PTree.elements_canonical_order.
+  intros id [b ty] GET. exploit me_local; eauto. intros [vk [A [B C]]].
+  exists (b, vk); split; auto. red. auto.
+  intros id [b vk] GET. 
+  exploit me_local_inv; eauto. intros [ty A]. 
+  exploit me_local; eauto. intros [vk' [B [C D]]]. 
+  assert (vk' = vk) by congruence. subst vk'.
+  exists (b, ty); split; auto. red. auto.
+
+  unfold blocks_of_env, Csem.blocks_of_env.
+  generalize H0. induction 1. auto. 
+  simpl. f_equal; auto.
+  unfold block_of_binding, Csem.block_of_binding. 
+  destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 vk2]].
+  simpl in *. destruct H1 as [A [B C]]. subst blk2 id2. f_equal.
+  apply sizeof_var_kind_of_type. auto. 
 Qed.
 
 Lemma match_env_free_blocks:
-  forall tyenv e te m,
+  forall tyenv e te m m',
   match_env tyenv e te ->
-  Mem.free_list m (Csem.blocks_of_env e) = Mem.free_list m (blocks_of_env te).
+  Mem.free_list m (Csem.blocks_of_env e) = Some m' ->
+  Mem.free_list m (blocks_of_env te) = Some m'.
 Proof.
-  intros. apply mem_free_list_same. intros; eapply match_env_same_blocks; eauto.
+  intros. rewrite (match_env_same_blocks _ _ _ H). auto.
 Qed.
 
 Definition match_globalenv (tyenv: typenv) (gv: gvarenv): Prop :=
@@ -203,14 +166,6 @@ Proof.
   intros. red in H. eauto.
 Qed.
 
-Lemma match_var_kind_of_type:
-  forall ty vk, var_kind_of_type ty = OK vk -> match_var_kind ty vk.
-Proof.
-  intros; red. 
-  caseEq (access_mode ty); auto.
-  intros chunk AM. generalize (var_kind_by_value _ _ AM). congruence.
-Qed.
-
 (** The following lemmas establish the [match_env] invariant at
   the beginning of a function invocation, after allocation of
   local variables and initialization of the parameters. *)
@@ -233,17 +188,16 @@ Proof.
   caseEq (transl_vars vars); simpl; [intros tvrs TVARS | congruence].
   intro EQ; inversion EQ; subst tvars; clear EQ.
   set (te2 := PTree.set id (b1, vk) te1).
-  assert (match_env (add_var tyenv (id, ty)) (PTree.set id b1 e) te2).
+  assert (match_env (add_var tyenv (id, ty)) (PTree.set id (b1, ty) e) te2).
     inversion H1. unfold te2, add_var. constructor.
     (* me_local *)
-    intros until b. simpl. repeat rewrite PTree.gsspec.
+    intros until ty0. simpl. repeat rewrite PTree.gsspec.
     destruct (peq id0 id); intros.
-    inv H3. exists vk; exists ty; intuition.
-    apply match_var_kind_of_type. congruence.
+    inv H3. exists vk; intuition.
     auto.
     (* me_local_inv *)
     intros until vk0. repeat rewrite PTree.gsspec. 
-    destruct (peq id0 id); intros. congruence. eauto. 
+    destruct (peq id0 id); intros. exists ty; congruence. eauto. 
     (* me_global *)
     intros until ty0. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros.
     discriminate.
@@ -276,9 +230,8 @@ Proof.
   unfold store_value_of_type in H0. rewrite H4 in H0.
   apply bind_parameters_cons with b m1. 
   assert (tyenv!id = Some ty). apply H2. apply in_eq.
-  destruct (me_local _ _ _ H3 _ _ H) as [vk [ty' [A [B C]]]]. 
-  assert (ty' = ty) by congruence. subst ty'.
-  red in B; rewrite H4 in B. congruence.
+  destruct (me_local _ _ _ H3 _ _ _ H)  as [vk [A [B C]]].
+  exploit var_kind_by_value; eauto. congruence.
   assumption.
   apply IHbind_parameters with tyenv; auto.
   intros. apply H2. apply in_cons; auto.
@@ -422,9 +375,9 @@ Proof.
   inversion H2; clear H2; subst.
   inversion H; subst; clear H.
     (* local variable *)
-    exploit me_local; eauto. intros [vk [ty' [A [B C]]]].
-    assert (ty' = ty) by congruence. subst ty'.
-    red in B; rewrite ACC in B.
+    exploit me_local; eauto. intros [vk [A [B C]]].
+    assert (vk = Vscalar chunk).
+    exploit var_kind_by_value; eauto. congruence.
     subst vk.
     eapply eval_Evar. 
     eapply eval_var_ref_local. eauto. assumption. 
@@ -440,7 +393,7 @@ Proof.
   inversion H2; clear H2; subst.
   inversion H; subst; clear H.
     (* local variable *)
-    exploit me_local; eauto. intros [vk [ty' [A [B C]]]].
+    exploit me_local; eauto. intros [vk [A [B C]]].
     eapply eval_Eaddrof.
     eapply eval_var_addr_local. eauto. 
     (* global variable *)
@@ -473,9 +426,10 @@ Proof.
   inversion H2; clear H2; subst.
   inversion H; subst; clear H. 
     (* local variable *)
-    exploit me_local; eauto. intros [vk [ty' [A [B C]]]].
-    assert (ty' = ty) by congruence. subst ty'.
-    red in B; rewrite ACC in B; subst vk.
+    exploit me_local; eauto. intros [vk [A [B C]]].
+    assert (vk = Vscalar chunk).
+      exploit var_kind_by_value; eauto. congruence.
+    subst vk.
     eapply step_assign. eauto.
     econstructor. eapply eval_var_ref_local. eauto. assumption. 
     (* global variable *)
@@ -514,10 +468,11 @@ Proof.
 (* local variable *)
   split. auto. 
   subst id0 ty l ofs. exploit me_local; eauto. 
-  intros [vk [ty [A [B C]]]].
-  assert (ty = typeof lhs) by congruence. rewrite <- H3. 
-  generalize B; unfold match_var_kind. destruct (access_mode ty); auto. 
-  intros. subst vk. apply eval_var_ref_local; auto.
+  intros [vk [A [B C]]].
+  case_eq (access_mode (typeof lhs)); intros; auto.
+  assert (vk = Vscalar m0).
+    exploit var_kind_by_value; eauto. congruence.
+  subst vk. apply eval_var_ref_local; auto.
 (* global variable *)
   split. auto.
   subst id0 ty l ofs. exploit me_global; eauto. intros [A B].
@@ -542,7 +497,6 @@ Proof.
   constructor. econstructor. eauto. auto.
 Qed.
 
-
 (** * Proof of semantic preservation *)
 
 (** ** Semantic preservation for expressions *)
@@ -794,12 +748,12 @@ Qed.
 
 Lemma transl_Evar_local_correct:
   forall (id : ident) (l : block) (ty : type),
-  e ! id = Some l ->
+  e ! id = Some(l, ty) ->
   eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero.
 Proof.
   intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
   exploit (me_local _ _ _ MENV); eauto.
-  intros [vk [ty' [A [B C]]]].
+  intros [vk [A [B C]]].
   econstructor. eapply eval_var_addr_local. eauto. 
 Qed.
 
@@ -1296,7 +1250,7 @@ Proof.
   apply plus_one. econstructor; eauto. 
   exploit transl_expr_correct; eauto.
   exploit transl_exprlist_correct; eauto.
-  eapply sig_translated; eauto. congruence.
+  eapply transl_fundef_sig1; eauto. congruence.
   econstructor; eauto. eapply functions_well_typed; eauto. 
   econstructor; eauto. simpl. auto. 
 
@@ -1310,7 +1264,7 @@ Proof.
   apply plus_one. econstructor; eauto. 
   exploit transl_expr_correct; eauto.
   exploit transl_exprlist_correct; eauto.
-  eapply sig_translated; eauto. congruence.
+  eapply transl_fundef_sig1; eauto. congruence.
   econstructor; eauto. eapply functions_well_typed; eauto.
   econstructor; eauto. simpl; auto. 
 
@@ -1521,16 +1475,18 @@ Proof.
   monadInv TR. inv MTR. 
   econstructor; split.
   apply plus_one. constructor. monadInv TRF. simpl. rewrite H. auto.
-  rewrite (match_env_free_blocks _ _ _ m MENV). econstructor; eauto.
+  eapply match_env_free_blocks; eauto. 
+  econstructor; eauto.
   eapply match_cont_call_cont. eauto. 
 
 (* return some *)
-  monadInv TR. inv MTR. inv WT. inv H2. 
+  monadInv TR. inv MTR. inv WT. inv H3. 
   econstructor; split.
   apply plus_one. constructor. monadInv TRF. simpl.
-  unfold opttyp_of_type. destruct (fn_return f); congruence.
-  exploit transl_expr_correct; eauto. 
-  rewrite (match_env_free_blocks _ _ _ m MENV). econstructor; eauto.
+  unfold opttyp_of_type. destruct (Csyntax.fn_return f); congruence.
+  exploit transl_expr_correct; eauto.
+  eapply match_env_free_blocks; eauto.
+  econstructor; eauto.
   eapply match_cont_call_cont. eauto. 
 
 (* skip call *)
@@ -1539,7 +1495,8 @@ Proof.
   econstructor; split.
   apply plus_one. apply step_skip_call. auto.
   monadInv TRF. simpl. rewrite H0. auto.
-  rewrite (match_env_free_blocks _ _ _ m MENV). constructor. eauto.
+  eapply match_env_free_blocks; eauto.
+  constructor. eauto.
 
 (* switch *)
   monadInv TR. inv WT.
@@ -1627,7 +1584,7 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   assert (C: Genv.find_symbol tge (prog_main tprog) = Some b).
     rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog).
-    exact H1. symmetry. unfold transl_program in TRANSL. 
+    exact H2. symmetry. unfold transl_program in TRANSL. 
     eapply transform_partial_program2_main; eauto.
   exploit function_ptr_well_typed. eauto. intro WTF.
   assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)).
@@ -1635,16 +1592,15 @@ Proof.
     eapply Genv.find_funct_ptr_symbol_inversion; eauto.
   destruct H as [targs D].
   assert (targs = Tnil). 
-    inv H0. inv H9. simpl in D. unfold type_of_function in D. rewrite <- H4 in D. 
+    inv H0. inv H10. simpl in D. unfold type_of_function in D. rewrite <- H5 in D. 
     simpl in D. congruence.
-    simpl in D. inv D. inv H8. inv H. 
-    destruct targs; simpl in H5; congruence.
+    simpl in D. inv D.
+    exploit external_call_arity; eauto. destruct targs; simpl; congruence.
   subst targs. 
   assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)).
-    eapply sig_translated; eauto. rewrite D; auto. 
+    eapply transl_fundef_sig2; eauto. 
   econstructor; split.
-  econstructor; eauto.
-  rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL).
+  econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. 
   constructor; auto. constructor. exact I.
 Qed.