From be2315351761e4fc0430b91ac791d66eec0e0cd7 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 6 Mar 2016 09:59:32 +0100
Subject: Globalenvs: adapt to new linking framework, and revise.

The commutation lemmas between program transformations and Genv operations now take separate compilation into account.  For example:

  Theorem find_funct_ptr_match:
    forall b f,
    find_funct_ptr (globalenv p) b = Some f ->
    exists cunit tf,
       find_funct_ptr (globalenv tp) b = Some tf
    /\ match_fundef cunit f tf
    /\ linkorder cunit ctx.

Note how "f" and "tf" are related wrt a compilation unit "cunit" which is not necessarily "ctx" (the context for the whole program), but can be a sub-unit of the this whole program.

The other changes in Globalenvs are a long-overdue refactoring and cleanup:

- Introduce Senv.equiv (extensional equivalence between two Senv.t) to collect (in one place) the invariance properties relevant to external functions (preservation of names, of public names, and of volatile blocks).

- Revise internal representation of Genv.t: one map ident -> globdef F V instead of two maps ident -> F and ident -> globvar V.

- More precise characterization of initial memory states: "Genv.init_mem_characterization" uniquely characterizes every byte (memval) of the representation of an initialized global variable.

- Necessary and sufficient conditions for the initial memory state to exist.

- Revised proofs about init_mem, especially init_mem_inject.

- Removed some Genv lemmas that were unused.
---
 common/Globalenvs.v | 1875 ++++++++++++++++++++-------------------------------
 1 file changed, 729 insertions(+), 1146 deletions(-)

(limited to 'common/Globalenvs.v')

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 5f78ea6b..a8d0512c 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -3,7 +3,6 @@
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*  with contributions from Andrew Tolmach (Portland State University) *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
@@ -36,14 +35,8 @@
 
 Require Recdef.
 Require Import Zwf.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
+Require Import Axioms Coqlib Errors Maps AST Linking.
+Require Import Integers Floats Values Memory.
 
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
@@ -113,6 +106,11 @@ Proof.
   intros. unfold symbol_address. destruct (find_symbol ge id); auto.
 Qed.
 
+Definition equiv (se1 se2: t) : Prop :=
+     (forall id, find_symbol se2 id = find_symbol se1 id)
+  /\ (forall id, public_symbol se2 id = public_symbol se1 id)
+  /\ (forall b, block_is_volatile se2 b = block_is_volatile se1 b).
+
 End Senv.
 
 Module Genv.
@@ -129,14 +127,10 @@ Variable V: Type.  (**r The type of information attached to variables *)
 Record t: Type := mkgenv {
   genv_public: list ident;              (**r which symbol names are public *)
   genv_symb: PTree.t block;             (**r mapping symbol -> block *)
-  genv_funs: PTree.t F;                 (**r mapping function pointer -> definition *)
-  genv_vars: PTree.t (globvar V);       (**r mapping variable pointer -> info *)
+  genv_defs: PTree.t (globdef F V);     (**r mapping block -> definition *)
   genv_next: block;                     (**r next symbol pointer *)
   genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> Plt b genv_next;
-  genv_funs_range: forall b f, PTree.get b genv_funs = Some f -> Plt b genv_next;
-  genv_vars_range: forall b v, PTree.get b genv_vars = Some v -> Plt b genv_next;
-  genv_funs_vars: forall b1 b2 f v,
-    PTree.get b1 genv_funs = Some f -> PTree.get b2 genv_vars = Some v -> b1 <> b2;
+  genv_defs_range: forall b g, PTree.get b genv_defs = Some g -> Plt b genv_next;
   genv_vars_inj: forall id1 id2 b,
     PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2
 }.
@@ -166,11 +160,16 @@ Definition public_symbol (ge: t) (id: ident) : bool :=
   | Some _ => In_dec ident_eq id ge.(genv_public)
   end.
 
+(** [find_def ge b] returns the global definition associated with the given address. *)
+
+Definition find_def (ge: t) (b: block) : option (globdef F V) :=
+  PTree.get b ge.(genv_defs).
+
 (** [find_funct_ptr ge b] returns the function description associated with
     the given address. *)
 
 Definition find_funct_ptr (ge: t) (b: block) : option F :=
-  PTree.get b ge.(genv_funs).
+  match find_def ge b with Some (Gfun f) => Some f | _ => None end.
 
 (** [find_funct] is similar to [find_funct_ptr], but the function address
     is given as a value, which must be a pointer with offset 0. *)
@@ -192,7 +191,7 @@ Definition invert_symbol (ge: t) (b: block) : option ident :=
    at address [b]. *)
 
 Definition find_var_info (ge: t) (b: block) : option (globvar V) :=
-  PTree.get b ge.(genv_vars).
+  match find_def ge b with Some (Gvar v) => Some v | _ => None end.
 
 (** [block_is_volatile ge b] returns [true] if [b] points to a global variable
   of volatile type, [false] otherwise. *)
@@ -209,16 +208,9 @@ Program Definition add_global (ge: t) (idg: ident * globdef F V) : t :=
   @mkgenv
     ge.(genv_public)
     (PTree.set idg#1 ge.(genv_next) ge.(genv_symb))
-    (match idg#2 with
-     | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs)
-     | Gvar v => ge.(genv_funs)
-     end)
-    (match idg#2 with
-     | Gfun f => ge.(genv_vars)
-     | Gvar v => PTree.set ge.(genv_next) v ge.(genv_vars)
-     end)
+    (PTree.set ge.(genv_next) idg#2 ge.(genv_defs))
     (Psucc ge.(genv_next))
-    _ _ _ _ _.
+    _ _ _.
 Next Obligation.
   destruct ge; simpl in *.
   rewrite PTree.gsspec in H. destruct (peq id i). inv H. apply Plt_succ.
@@ -226,32 +218,10 @@ Next Obligation.
 Qed.
 Next Obligation.
   destruct ge; simpl in *.
-  destruct g.
-  rewrite PTree.gsspec in H.
-  destruct (peq b genv_next0). inv H. apply Plt_succ.
-  apply Plt_trans_succ; eauto.
+  rewrite PTree.gsspec in H. destruct (peq b genv_next0).
+  inv H. apply Plt_succ.
   apply Plt_trans_succ; eauto.
 Qed.
-Next Obligation.
-  destruct ge; simpl in *.
-  destruct g.
-  apply Plt_trans_succ; eauto.
-  rewrite PTree.gsspec in H.
-  destruct (peq b genv_next0). inv H. apply Plt_succ.
-  apply Plt_trans_succ; eauto.
-Qed.
-Next Obligation.
-  destruct ge; simpl in *.
-  destruct g.
-  rewrite PTree.gsspec in H.
-  destruct (peq b1 genv_next0). inv H.
-  apply sym_not_equal; apply Plt_ne; eauto.
-  eauto.
-  rewrite PTree.gsspec in H0.
-  destruct (peq b2 genv_next0). inv H0.
-  apply Plt_ne; eauto.
-  eauto.
-Qed.
 Next Obligation.
   destruct ge; simpl in *.
   rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0.
@@ -269,17 +239,11 @@ Lemma add_globals_app:
   forall gl2 gl1 ge,
   add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2.
 Proof.
-  induction gl1; simpl; intros. auto. rewrite IHgl1; auto.
+  intros. apply fold_left_app. 
 Qed.
 
 Program Definition empty_genv (pub: list ident): t :=
-  @mkgenv pub (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _.
-Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
-Qed.
-Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
-Qed.
+  @mkgenv pub (PTree.empty _) (PTree.empty _) 1%positive _ _ _.
 Next Obligation.
   rewrite PTree.gempty in H. discriminate.
 Qed.
@@ -400,84 +364,62 @@ Proof.
   intros; simpl. apply dec_eq_true.
 Qed.
 
-Theorem find_symbol_exists:
-  forall p id g,
-  In (id, g) (prog_defs p) ->
-  exists b, find_symbol (globalenv p) id = Some b.
+Theorem find_funct_ptr_iff:
+  forall ge b f, find_funct_ptr ge b = Some f <-> find_def ge b = Some (Gfun f).
 Proof.
-  intros. unfold globalenv. eapply add_globals_ensures; eauto.
-(* preserves *)
-  intros. unfold find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id0).
-  econstructor; eauto.
-  auto.
-(* ensures *)
-  intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto.
+  intros. unfold find_funct_ptr. destruct (find_def ge b) as [[f1|v1]|]; intuition congruence.
 Qed.
 
-Theorem find_funct_ptr_exists_2:
-  forall p gl1 id f gl2,
-  prog_defs p = gl1 ++ (id, Gfun f) :: gl2 -> ~In id (map fst gl2) ->
-  exists b,
-     find_symbol (globalenv p) id = Some b
-  /\ find_funct_ptr (globalenv p) b = Some f.
+Theorem find_var_info_iff:
+  forall ge b v, find_var_info ge b = Some v <-> find_def ge b = Some (Gvar v).
 Proof.
-  intros; unfold globalenv. rewrite H. eapply add_globals_unique_ensures; eauto.
-(* preserves *)
-  intros. unfold find_symbol, find_funct_ptr in *; simpl.
-  destruct H1 as [b [A B]]. exists b; split.
-  rewrite PTree.gso; auto.
-  destruct g1 as [f1 | v1]. rewrite PTree.gso. auto.
-  apply Plt_ne. eapply genv_funs_range; eauto.
-  auto.
-(* ensures *)
-  intros. unfold find_symbol, find_funct_ptr in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss.
+  intros. unfold find_var_info. destruct (find_def ge b) as [[f1|v1]|]; intuition congruence.
 Qed.
 
-Corollary find_funct_ptr_exists:
-  forall p id f,
-  list_norepet (prog_defs_names p) ->
-  In (id, Gfun f) (prog_defs p) ->
-  exists b,
-     find_symbol (globalenv p) id = Some b
-  /\ find_funct_ptr (globalenv p) b = Some f.
+Theorem find_def_symbol:
+  forall p id g,
+  (prog_defmap p)!id = Some g <-> exists b, find_symbol (globalenv p) id = Some b /\ find_def (globalenv p) b = Some g.
 Proof.
-  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y).
-  eapply find_funct_ptr_exists_2; eauto.
+  intros.
+  set (P := fun m ge => m!id = Some g <-> exists b, find_symbol ge id = Some b /\ find_def ge b = Some g).
+  assert (REC: forall l m ge,
+            P m ge ->
+            P (fold_left (fun m idg => PTree.set idg#1 idg#2 m) l m)
+              (add_globals ge l)).
+  { induction l as [ | [id1 g1] l]; intros; simpl.
+  - auto.
+  - apply IHl. unfold P, add_global, find_symbol, find_def; simpl.
+    rewrite ! PTree.gsspec. destruct (peq id id1). 
+    + subst id1. split; intros.
+      inv H0. exists (genv_next ge); split; auto. apply PTree.gss.
+      destruct H0 as (b & A & B). inv A. rewrite PTree.gss in B. auto.
+    + red in H; rewrite H. split.
+      intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto. 
+      apply Plt_ne. eapply genv_symb_range; eauto. 
+      intros (b & A & B). rewrite PTree.gso in B. exists b; auto. 
+      apply Plt_ne. eapply genv_symb_range; eauto. 
+  }
+  apply REC. unfold P, find_symbol, find_def; simpl. 
+  rewrite ! PTree.gempty. split.
+  congruence.
+  intros (b & A & B); congruence.
 Qed.
 
-Theorem find_var_exists_2:
-  forall p gl1 id v gl2,
-  prog_defs p = gl1 ++ (id, Gvar v) :: gl2 -> ~In id (map fst gl2) ->
-  exists b,
-     find_symbol (globalenv p) id = Some b
-  /\ find_var_info (globalenv p) b = Some v.
+Theorem find_symbol_exists:
+  forall p id g,
+  In (id, g) (prog_defs p) ->
+  exists b, find_symbol (globalenv p) id = Some b.
 Proof.
-  intros; unfold globalenv. rewrite H. eapply add_globals_unique_ensures; eauto.
+  intros. unfold globalenv. eapply add_globals_ensures; eauto.
 (* preserves *)
-  intros. unfold find_symbol, find_var_info in *; simpl.
-  destruct H1 as [b [A B]]. exists b; split.
-  rewrite PTree.gso; auto.
-  destruct g1 as [f1 | v1]. auto. rewrite PTree.gso. auto.
-  apply Plt_ne. eapply genv_vars_range; eauto.
+  intros. unfold find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id0).
+  econstructor; eauto.
+  auto.
 (* ensures *)
-  intros. unfold find_symbol, find_var_info in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss.
-Qed.
-
-Corollary find_var_exists:
-  forall p id v,
-  list_norepet (prog_defs_names p) ->
-  In (id, Gvar v) (prog_defs p) ->
-  exists b,
-     find_symbol (globalenv p) id = Some b
-  /\ find_var_info (globalenv p) b = Some v.
-Proof.
-  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y).
-  eapply find_var_exists_2; eauto.
+  intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto.
 Qed.
 
-Lemma find_symbol_inversion : forall p x b,
+Theorem find_symbol_inversion : forall p x b,
   find_symbol (globalenv p) x = Some b ->
   In x (prog_defs_names p).
 Proof.
@@ -490,22 +432,30 @@ Proof.
   unfold find_symbol; simpl; intros. rewrite PTree.gempty in H. discriminate.
 Qed.
 
-Theorem find_funct_ptr_inversion:
-  forall p b f,
-  find_funct_ptr (globalenv p) b = Some f ->
-  exists id, In (id, Gfun f) (prog_defs p).
+Theorem find_def_inversion:
+  forall p b g,
+  find_def (globalenv p) b = Some g ->
+  exists id, In (id, g) (prog_defs p).
 Proof.
-  intros until f. unfold globalenv. apply add_globals_preserves.
+  intros until g. unfold globalenv. apply add_globals_preserves.
 (* preserves *)
-  unfold find_funct_ptr; simpl; intros. destruct g; auto.
+  unfold find_def; simpl; intros.
   rewrite PTree.gsspec in H1. destruct (peq b (genv_next ge)).
   inv H1. exists id; auto.
   auto.
 (* base *)
-  unfold find_funct_ptr; simpl; intros. rewrite PTree.gempty in H. discriminate.
+  unfold find_def; simpl; intros. rewrite PTree.gempty in H. discriminate.
 Qed.
 
-Theorem find_funct_inversion:
+Corollary find_funct_ptr_inversion:
+  forall p b f,
+  find_funct_ptr (globalenv p) b = Some f ->
+  exists id, In (id, Gfun f) (prog_defs p).
+Proof.
+  intros. apply find_def_inversion with b. apply find_funct_ptr_iff; auto.
+Qed.
+
+Corollary find_funct_inversion:
   forall p v f,
   find_funct (globalenv p) v = Some f ->
   exists id, In (id, Gfun f) (prog_defs p).
@@ -533,25 +483,6 @@ Proof.
   intros. exploit find_funct_inversion; eauto. intros [id IN]. eauto.
 Qed.
 
-Theorem find_funct_ptr_symbol_inversion:
-  forall p id b f,
-  find_symbol (globalenv p) id = Some b ->
-  find_funct_ptr (globalenv p) b = Some f ->
-  In (id, Gfun f) p.(prog_defs).
-Proof.
-  intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves.
-(* preserves *)
-  intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0).
-  inv H1. destruct g as [f1|v1]. rewrite PTree.gss in H2. inv H2. auto.
-  eelim Plt_strict. eapply genv_funs_range; eauto.
-  destruct g as [f1|v1]. rewrite PTree.gso in H2. auto.
-  apply Plt_ne. eapply genv_symb_range; eauto.
-  auto.
-(* initial *)
-  intros. simpl in *. rewrite PTree.gempty in H. discriminate.
-Qed.
-
-
 Theorem global_addresses_distinct:
   forall ge id1 id2 b1 b2,
   id1 <> id2 ->
@@ -626,7 +557,7 @@ Theorem block_is_volatile_below:
   forall ge b, block_is_volatile ge b = true ->  Plt b ge.(genv_next).
 Proof.
   unfold block_is_volatile; intros. destruct (find_var_info ge b) as [gv|] eqn:FV.
-  eapply genv_vars_range; eauto.
+  rewrite find_var_info_iff in FV. eapply genv_defs_range; eauto.
   discriminate.
 Qed.
 
@@ -652,24 +583,6 @@ Section INITMEM.
 
 Variable ge: t.
 
-Definition init_data_size (i: init_data) : Z :=
-  match i with
-  | Init_int8 _ => 1
-  | Init_int16 _ => 2
-  | Init_int32 _ => 4
-  | Init_int64 _ => 8
-  | Init_float32 _ => 4
-  | Init_float64 _ => 8
-  | Init_addrof _ _ => 4
-  | Init_space n => Zmax n 0
-  end.
-
-Lemma init_data_size_pos:
-  forall i, init_data_size i >= 0.
-Proof.
-  destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega.
-Qed.
-
 Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem :=
   match id with
   | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n)
@@ -697,12 +610,6 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data)
       end
   end.
 
-Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
-  match il with
-  | nil => 0
-  | i :: il' => init_data_size i + init_data_list_size il'
-  end.
-
 Definition perm_globvar (gv: globvar V) : permission :=
   if gv.(gvar_volatile) then Nonempty
   else if gv.(gvar_readonly) then Readable
@@ -818,22 +725,32 @@ Proof.
   congruence.
 Qed.
 
-Remark store_init_data_list_perm:
-  forall k prm b' q idl b m p m',
-  store_init_data_list m b p idl = Some m' ->
+Remark store_init_data_perm:
+  forall k prm b' q i b m p m',
+  store_init_data m b p i = Some m' ->
   (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
-  induction idl; simpl; intros until m'.
-  intros. inv H. tauto.
-  caseEq (store_init_data m b p a); try congruence. intros.
-  rewrite <- (IHidl _ _ _ _ H0).
+  intros. 
   assert (forall chunk v,
-          Mem.store chunk m b p v = Some m0 ->
-          (Mem.perm m b' q k prm <-> Mem.perm m0 b' q k prm)).
+          Mem.store chunk m b p v = Some m' ->
+          (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm)).
     intros; split; eauto with mem.
-  destruct a; simpl in H; eauto.
+  destruct i; simpl in H; eauto. 
   inv H; tauto.
-  destruct (find_symbol ge i). eauto. discriminate.
+  destruct (find_symbol ge i); try discriminate. eauto.
+Qed.
+
+Remark store_init_data_list_perm:
+  forall k prm b' q idl b m p m',
+  store_init_data_list m b p idl = Some m' ->
+  (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
+Proof.
+  induction idl as [ | i1 idl]; simpl; intros.
+- inv H; tauto.
+- destruct (store_init_data m b p i1) as [m1|] eqn:S1; try discriminate.
+  transitivity (Mem.perm m1 b' q k prm). 
+  eapply store_init_data_perm; eauto.
+  eapply IHidl; eauto.
 Qed.
 
 Remark alloc_global_perm:
@@ -883,36 +800,146 @@ Qed.
 
 (** Data preservation properties *)
 
-Remark store_zeros_load_outside:
-  forall m b p n m',
+Remark store_zeros_unchanged:
+  forall (P: block -> Z -> Prop) m b p n m',
   store_zeros m b p n = Some m' ->
-  forall chunk b' p',
-  b' <> b \/ p' + size_chunk chunk <= p \/ p + n <= p' ->
-  Mem.load chunk m' b' p' = Mem.load chunk m b' p'.
+  (forall i, p <= i < p + n -> ~ P b i) ->
+  Mem.unchanged_on P m m'.
 Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
-  inv H; auto.
-  transitivity (Mem.load chunk m' b' p').
-  apply IHo. auto. intuition omega.
-  eapply Mem.load_store_other; eauto. simpl. intuition omega.
-  discriminate.
+- inv H; apply Mem.unchanged_on_refl.
+- apply Mem.unchanged_on_trans with m'.
++ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. 
++ apply IHo; auto. intros; apply H0; omega. 
+- discriminate.
+Qed.
+
+Remark store_init_data_unchanged:
+  forall (P: block -> Z -> Prop) b i m p m',
+  store_init_data m b p i = Some m' ->
+  (forall ofs, p <= ofs < p + init_data_size i -> ~ P b ofs) ->
+  Mem.unchanged_on P m m'.
+Proof.
+  intros. destruct i; simpl in *;
+  try (eapply Mem.store_unchanged_on; eauto; fail).
+  inv H; apply Mem.unchanged_on_refl.
+  destruct (find_symbol ge i); try congruence.
+  eapply Mem.store_unchanged_on; eauto. 
+Qed.
+
+Remark store_init_data_list_unchanged:
+  forall (P: block -> Z -> Prop) b il m p m',
+  store_init_data_list m b p il = Some m' ->
+  (forall ofs, p <= ofs -> ~ P b ofs) ->
+  Mem.unchanged_on P m m'.
+Proof.
+  induction il; simpl; intros.
+- inv H. apply Mem.unchanged_on_refl.
+- destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
+  apply Mem.unchanged_on_trans with m1.
+  eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. 
+  eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); omega.
 Qed.
 
-Remark store_zeros_loadbytes_outside:
+(** Properties related to [loadbytes] *)
+
+Definition readbytes_as_zero (m: mem) (b: block) (ofs len: Z) : Prop :=
+  forall p n,
+  ofs <= p -> p + Z.of_nat n <= ofs + len ->
+  Mem.loadbytes m b p (Z.of_nat n) = Some (list_repeat n (Byte Byte.zero)).
+
+Lemma store_zeros_loadbytes:
   forall m b p n m',
   store_zeros m b p n = Some m' ->
-  forall b' p' n',
-  b' <> b \/ p' + n' <= p \/ p + n <= p' ->
-  Mem.loadbytes m' b' p' n' = Mem.loadbytes m b' p' n'.
+  readbytes_as_zero m' b p n.
 Proof.
-  intros until n. functional induction (store_zeros m b p n); intros.
-  inv H; auto.
-  transitivity (Mem.loadbytes m' b' p' n').
-  apply IHo. auto. intuition omega.
-  eapply Mem.loadbytes_store_other; eauto. simpl. intuition omega.
-  discriminate.
+  intros until n; functional induction (store_zeros m b p n); red; intros.
+- destruct n0. simpl. apply Mem.loadbytes_empty. omega.
+  rewrite inj_S in H1. omegaContradiction.
+- destruct (zeq p0 p).
+  + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. omega.
+    rewrite inj_S in H1. rewrite inj_S.
+    replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by omega.
+    change (list_repeat (S n0) (Byte Byte.zero))
+      with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)).
+    apply Mem.loadbytes_concat.
+    eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p).
+    eapply store_zeros_unchanged; eauto. intros; omega. 
+    intros; omega.
+    change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero).
+    change 1 with (size_chunk Mint8unsigned).
+    eapply Mem.loadbytes_store_same; eauto.
+    eapply IHo; eauto. omega. omega. omega. omega.
+  + eapply IHo; eauto. omega. omega.
+- discriminate.
 Qed.
 
+Definition bytes_of_init_data (i: init_data): list memval :=
+  match i with
+  | Init_int8 n => inj_bytes (encode_int 1%nat (Int.unsigned n))
+  | Init_int16 n => inj_bytes (encode_int 2%nat (Int.unsigned n))
+  | Init_int32 n => inj_bytes (encode_int 4%nat (Int.unsigned n))
+  | Init_int64 n => inj_bytes (encode_int 8%nat (Int64.unsigned n))
+  | Init_float32 n => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
+  | Init_float64 n => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
+  | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero)
+  | Init_addrof id ofs =>
+      match find_symbol ge id with
+      | Some b => inj_value Q32 (Vptr b ofs)
+      | None   => list_repeat 4%nat Undef
+      end
+  end.
+
+Lemma store_init_data_loadbytes:
+  forall m b p i m',
+  store_init_data m b p i = Some m' ->
+  readbytes_as_zero m b p (init_data_size i) ->
+  Mem.loadbytes m' b p (init_data_size i) = Some (bytes_of_init_data i).
+Proof.
+  intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H).
+- inv H. simpl.
+  assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0).
+  { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } 
+  rewrite <- EQ. apply H0. omega. simpl. omega. 
+- simpl; destruct (find_symbol ge i) as [b'|]; try discriminate.
+  apply (Mem.loadbytes_store_same _ _ _ _ _ _ H).
+Qed.
+
+Fixpoint bytes_of_init_data_list (il: list init_data): list memval :=
+  match il with
+  | nil => nil
+  | i :: il => bytes_of_init_data i ++ bytes_of_init_data_list il
+  end.
+
+Lemma store_init_data_list_loadbytes:
+  forall b il m p m',
+  store_init_data_list m b p il = Some m' ->
+  readbytes_as_zero m b p (init_data_list_size il) ->
+  Mem.loadbytes m' b p (init_data_list_size il) = Some (bytes_of_init_data_list il).
+Proof.
+  induction il as [ | i1 il]; simpl; intros.
+- apply Mem.loadbytes_empty. omega.
+- generalize (init_data_size_pos i1) (init_data_list_size_pos il); intros P1 PL.
+  destruct (store_init_data m b p i1) as [m1|] eqn:S; try discriminate.
+  apply Mem.loadbytes_concat.
+  eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 < p + init_data_size i1).
+  eapply store_init_data_list_unchanged; eauto.
+  intros; omega.
+  intros; omega.
+  eapply store_init_data_loadbytes; eauto. 
+  red; intros; apply H0. omega. omega.
+  apply IHil with m1; auto.
+  red; intros. 
+  eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => p + init_data_size i1 <= ofs1).
+  eapply store_init_data_unchanged; eauto. 
+  intros; omega.
+  intros; omega. 
+  apply H0. omega. omega.
+  auto. auto.
+Qed.
+
+(** Properties related to [load] *)
+
 Definition read_as_zero (m: mem) (b: block) (ofs len: Z) : Prop :=
   forall chunk p,
   ofs <= p -> p + size_chunk chunk <= ofs + len ->
@@ -926,32 +953,16 @@ Definition read_as_zero (m: mem) (b: block) (ofs len: Z) : Prop :=
         | Many32 | Many64 => Vundef
         end).
 
-Remark store_zeros_loadbytes:
-  forall m b p n m',
-  store_zeros m b p n = Some m' ->
-  forall p' n',
-  p <= p' -> p' + Z.of_nat n' <= p + n ->
-  Mem.loadbytes m' b p' (Z.of_nat n') = Some (list_repeat n' (Byte Byte.zero)).
+Remark read_as_zero_unchanged:
+  forall (P: block -> Z -> Prop) m b ofs len m',
+  read_as_zero m b ofs len ->
+  Mem.unchanged_on P m m' ->
+  (forall i, ofs <= i < ofs + len -> P b i) ->
+  read_as_zero m' b ofs len.
 Proof.
-  intros until n; functional induction (store_zeros m b p n); intros.
-- destruct n'. simpl. apply Mem.loadbytes_empty. omega.
-  rewrite inj_S in H1. omegaContradiction.
-- destruct (zeq p' p).
-  + subst p'. destruct n'. simpl. apply Mem.loadbytes_empty. omega.
-    rewrite inj_S in H1. rewrite inj_S.
-    replace (Z.succ (Z.of_nat n')) with (1 + Z.of_nat n') by omega.
-    change (list_repeat (S n') (Byte Byte.zero))
-      with ((Byte Byte.zero :: nil) ++ list_repeat n' (Byte Byte.zero)).
-    apply Mem.loadbytes_concat.
-    erewrite store_zeros_loadbytes_outside; eauto.
-    change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero).
-    change 1 with (size_chunk Mint8unsigned).
-    eapply Mem.loadbytes_store_same; eauto.
-    right; omega.
-    eapply IHo; eauto. omega. omega. omega. omega.
-  + eapply IHo; eauto. omega. omega.
-- discriminate.
-Qed.
+  intros; red; intros. eapply Mem.load_unchanged_on; eauto. 
+  intros; apply H1. omega. 
+Qed. 
 
 Lemma store_zeros_read_as_zero:
   forall m b p n m',
@@ -965,35 +976,6 @@ Proof.
   f_equal. destruct chunk; reflexivity.
 Qed.
 
-Remark store_init_data_outside:
-  forall b i m p m',
-  store_init_data m b p i = Some m' ->
-  forall chunk b' q,
-  b' <> b \/ q + size_chunk chunk <= p \/ p + init_data_size i <= q ->
-  Mem.load chunk m' b' q = Mem.load chunk m b' q.
-Proof.
-  intros. destruct i; simpl in *;
-  try (eapply Mem.load_store_other; eauto; fail).
-  inv H; auto.
-  destruct (find_symbol ge i); try congruence.
-  eapply Mem.load_store_other; eauto; intuition.
-Qed.
-
-Remark store_init_data_list_outside:
-  forall b il m p m',
-  store_init_data_list m b p il = Some m' ->
-  forall chunk b' q,
-  b' <> b \/ q + size_chunk chunk <= p ->
-  Mem.load chunk m' b' q = Mem.load chunk m b' q.
-Proof.
-  induction il; simpl.
-  intros; congruence.
-  intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
-  transitivity (Mem.load chunk m1 b' q).
-  eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega.
-  eapply store_init_data_outside; eauto. tauto.
-Qed.
-
 Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop :=
   match il with
   | nil => True
@@ -1023,12 +1005,6 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s
       /\ load_store_init_data m b (p + Zmax n 0) il'
   end.
 
-Remark init_data_list_size_pos:
-  forall il, init_data_list_size il >= 0.
-Proof.
-  induction il; simpl. omega. generalize (init_data_size_pos a); omega.
-Qed.
-
 Lemma store_init_data_list_charact:
   forall b il m p m',
   store_init_data_list m b p il = Some m' ->
@@ -1040,17 +1016,22 @@ Proof.
     store_init_data_list m1 b (p + size_chunk chunk) il = Some m' ->
     Mem.load chunk m' b p = Some(Val.load_result chunk v)).
   {
-    intros. transitivity (Mem.load chunk m1 b p).
-    eapply store_init_data_list_outside; eauto. right. omega.
+    intros.
+    eapply Mem.load_unchanged_on with (P := fun b' ofs' => ofs' < p + size_chunk chunk).
+    eapply store_init_data_list_unchanged; eauto. intros; omega.
+    intros; tauto.
     eapply Mem.load_store_same; eauto.
   }
   induction il; simpl.
   auto.
   intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
   exploit IHil; eauto.
-  red; intros. transitivity (Mem.load chunk m b p0).
-  eapply store_init_data_outside. eauto. auto.
-  apply H0. generalize (init_data_size_pos a); omega. omega. auto.
+  set (P := fun (b': block) ofs' => p + init_data_size a <= ofs').
+  apply read_as_zero_unchanged with (m := m) (P := P).
+  red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. 
+  eapply store_init_data_unchanged with (P := P); eauto.
+  intros; unfold P. omega.
+  intros; unfold P. omega.
   intro D.
   destruct a; simpl in Heqo; intuition.
   eapply (A Mint8unsigned (Vint i)); eauto.
@@ -1059,56 +1040,60 @@ Proof.
   eapply (A Mint64 (Vlong i)); eauto.
   eapply (A Mfloat32 (Vsingle f)); eauto.
   eapply (A Mfloat64 (Vfloat f)); eauto.
-  inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0).
-  eapply store_init_data_list_outside; eauto. right. simpl. xomega.
-  apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega.
+  set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)).
+  inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P).
+  red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega.
+  eapply store_init_data_list_unchanged; eauto. 
+  intros; unfold P. omega.
+  intros; unfold P. simpl; xomega.
   destruct (find_symbol ge i); try congruence. exists b0; split; auto.
   eapply (A Mint32 (Vptr b0 i0)); eauto.
 Qed.
 
-Remark load_alloc_global:
-  forall chunk b p id g m m',
+Remark alloc_global_unchanged:
+  forall (P: block -> Z -> Prop) m id g m',
   alloc_global m (id, g) = Some m' ->
-  Mem.valid_block m b ->
-  Mem.load chunk m' b p = Mem.load chunk m b p.
+  Mem.unchanged_on P m m'.
 Proof.
   intros. destruct g as [f|v]; simpl in H.
-  (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?.
-  assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  transitivity (Mem.load chunk m1 b p).
-  eapply Mem.load_drop; eauto.
-  eapply Mem.load_alloc_unchanged; eauto.
-  (* variable *)
+- (* function *)
+  destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
+  set (Q := fun b' (ofs: Z) => b' <> b).
+  apply Mem.unchanged_on_implies with Q.
+  apply Mem.unchanged_on_trans with m1.
+  eapply Mem.alloc_unchanged_on; eauto.
+  eapply Mem.drop_perm_unchanged_on; eauto. 
+  intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem.
+- (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b'] eqn:?.
-  destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate.
-  destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate.
-  assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  transitivity (Mem.load chunk m3 b p).
-  eapply Mem.load_drop; eauto.
-  transitivity (Mem.load chunk m2 b p).
-  eapply store_init_data_list_outside; eauto.
-  transitivity (Mem.load chunk m1 b p).
-  eapply store_zeros_load_outside; eauto.
-  eapply Mem.load_alloc_unchanged; eauto.
-Qed.
-
-Remark load_alloc_globals:
-  forall chunk b p gl m m',
+  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate.
+  destruct (store_init_data_list m2 b 0 init) as [m3|] eqn:?; try discriminate.
+  set (Q := fun b' (ofs: Z) => b' <> b).
+  apply Mem.unchanged_on_implies with Q.
+  apply Mem.unchanged_on_trans with m1.
+  eapply Mem.alloc_unchanged_on; eauto.
+  apply Mem.unchanged_on_trans with m2.
+  eapply store_zeros_unchanged; eauto.
+  apply Mem.unchanged_on_trans with m3.
+  eapply store_init_data_list_unchanged; eauto. 
+  eapply Mem.drop_perm_unchanged_on; eauto. 
+  intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem.
+Qed.
+
+Remark alloc_globals_unchanged:
+  forall (P: block -> Z -> Prop) gl m m',
   alloc_globals m gl = Some m' ->
-  Mem.valid_block m b ->
-  Mem.load chunk m' b p = Mem.load chunk m b p.
+  Mem.unchanged_on P m m'.
 Proof.
   induction gl; simpl; intros.
-  congruence.
-  destruct (alloc_global m a) as [m''|] eqn:?; try discriminate.
-  transitivity (Mem.load chunk m'' b p).
-  apply IHgl; auto. unfold Mem.valid_block in *.
-  erewrite alloc_global_nextblock; eauto.
-  apply Plt_trans with (Mem.nextblock m); auto. apply Plt_succ.
-  destruct a as [id g]. eapply load_alloc_global; eauto.
+- inv H. apply Mem.unchanged_on_refl.
+- destruct (alloc_global m a) as [m''|] eqn:?; try discriminate.
+  destruct a as [id g].
+  apply Mem.unchanged_on_trans with m''. 
+  eapply alloc_global_unchanged; eauto.
+  apply IHgl; auto.
 Qed.
 
 Remark load_store_init_data_invariant:
@@ -1119,125 +1104,101 @@ Remark load_store_init_data_invariant:
 Proof.
   induction il; intro p; simpl.
   auto.
-  repeat rewrite H. destruct a; intuition. red; intros; rewrite H; auto.
-Qed.
-
-Definition variables_initialized (g: t) (m: mem) :=
-  forall b gv,
-  find_var_info g b = Some gv ->
-  Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Cur (perm_globvar gv)
-  /\ (forall ofs k p, Mem.perm m b ofs k p ->
-        0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p)
-  /\ (gv.(gvar_volatile) = false -> load_store_init_data m b 0 gv.(gvar_init)).
-
-Definition functions_initialized (g: t) (m: mem) :=
-  forall b fd,
-  find_funct_ptr g b = Some fd ->
-  Mem.perm m b 0 Cur Nonempty
-  /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p).
+  rewrite ! H. destruct a; intuition. red; intros; rewrite H; auto.
+Qed.
+
+Definition globals_initialized (g: t) (m: mem) :=
+  forall b gd,
+  find_def g b = Some gd ->
+  match gd with
+  | Gfun f =>
+         Mem.perm m b 0 Cur Nonempty
+      /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ p = Nonempty)
+  | Gvar v =>
+         Mem.range_perm m b 0 (init_data_list_size v.(gvar_init)) Cur (perm_globvar v)
+      /\ (forall ofs k p, Mem.perm m b ofs k p ->
+            0 <= ofs < init_data_list_size v.(gvar_init) /\ perm_order (perm_globvar v) p)
+      /\ (v.(gvar_volatile) = false -> load_store_init_data m b 0 v.(gvar_init))
+      /\ (v.(gvar_volatile) = false -> Mem.loadbytes m b 0 (init_data_list_size v.(gvar_init)) = Some (bytes_of_init_data_list v.(gvar_init)))
+  end.
 
 Lemma alloc_global_initialized:
-  forall ge m id g m',
-  genv_next ge = Mem.nextblock m ->
-  alloc_global m (id, g) = Some m' ->
-  variables_initialized ge m ->
-  functions_initialized ge m ->
-  variables_initialized (add_global ge (id, g)) m'
-  /\ functions_initialized (add_global ge (id, g)) m'
-  /\ genv_next (add_global ge (id, g)) = Mem.nextblock m'.
+  forall g m id gd m',
+  genv_next g = Mem.nextblock m ->
+  alloc_global m (id, gd) = Some m' ->
+  globals_initialized g m ->
+     globals_initialized (add_global g (id, gd)) m'
+  /\ genv_next (add_global g (id, gd)) = Mem.nextblock m'.
 Proof.
   intros.
   exploit alloc_global_nextblock; eauto. intros NB. split.
-(* variables-initialized *)
-  destruct g as [f|v].
-(* function *)
-  red; intros. unfold find_var_info in H3. simpl in H3.
-  exploit H1; eauto. intros [A [B C]].
-  assert (D: Mem.valid_block m b).
-    red. exploit genv_vars_range; eauto. rewrite H; auto.
-  split. red; intros. erewrite <- alloc_global_perm; eauto.
-  split. intros. eapply B. erewrite alloc_global_perm; eauto.
-  intros. apply load_store_init_data_invariant with m; auto.
-  intros. eapply load_alloc_global; eauto.
-(* variable *)
-  red; intros. unfold find_var_info in H3. simpl in H3. rewrite PTree.gsspec in H3.
-  destruct (peq b (genv_next ge0)).
-  (* same *)
-  inv H3. simpl in H0.
-  set (init := gvar_init gv) in *.
+- (* globals-initialized *)
+  red; intros. unfold find_def in H2; simpl in H2.
+  rewrite PTree.gsspec in H2. destruct (peq b (genv_next g)).
++ inv H2. destruct gd0 as [f|v]; simpl in H0.
+* destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC.
+  exploit Mem.alloc_result; eauto. intros RES.
+  rewrite H, <- RES. split.
+  eapply Mem.perm_drop_1; eauto. omega.
+  intros. 
+  assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. }
+  exploit Mem.perm_drop_2; eauto. intros ORD.
+  split. omega. inv ORD; auto.
+* set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b'] eqn:?.
-  destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate.
-  destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate.
+  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate.
+  destruct (store_init_data_list m2 b 0 init) as [m3|] eqn:?; try discriminate.
   exploit Mem.alloc_result; eauto. intro RES.
-  replace (genv_next ge0) with b' by congruence.
+  replace (genv_next g) with b by congruence.
   split. red; intros. eapply Mem.perm_drop_1; eauto.
   split. intros.
   assert (0 <= ofs < sz).
-    eapply Mem.perm_alloc_3; eauto.
-    erewrite store_zeros_perm; [idtac|eauto].
-    erewrite store_init_data_list_perm; [idtac|eauto].
-    eapply Mem.perm_drop_4; eauto.
-  split. auto. eapply Mem.perm_drop_2; eauto.
-  intros. apply load_store_init_data_invariant with m3.
-  intros. eapply Mem.load_drop; eauto.
-  right; right; right. unfold perm_globvar. rewrite H3.
-  destruct (gvar_readonly gv); auto with mem.
-  eapply store_init_data_list_charact; eauto.
+  { eapply Mem.perm_alloc_3; eauto. 
+    erewrite store_zeros_perm by eauto.
+    erewrite store_init_data_list_perm by eauto. 
+    eapply Mem.perm_drop_4; eauto. }
+  split; auto.
+  eapply Mem.perm_drop_2; eauto.
+  split. intros NOTVOL. apply load_store_init_data_invariant with m3.
+  intros. eapply Mem.load_drop; eauto. right; right; right. 
+  unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem.
+  eapply store_init_data_list_charact; eauto. 
   eapply store_zeros_read_as_zero; eauto.
-  (* older var *)
-  exploit H1; eauto. intros [A [B C]].
-  assert (D: Mem.valid_block m b).
-    red. exploit genv_vars_range; eauto. rewrite H; auto.
-  split. red; intros. erewrite <- alloc_global_perm; eauto.
-  split. intros. eapply B. erewrite alloc_global_perm; eauto.
-  intros. apply load_store_init_data_invariant with m; auto.
-  intros. eapply load_alloc_global; eauto.
-(* functions-initialized *)
-  split. destruct g as [f|v].
-(* function *)
-  red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite PTree.gsspec in H3.
-  destruct (peq b (genv_next ge0)).
-  (* same *)
-  inv H3. simpl in H0.
-  destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?.
-  exploit Mem.alloc_result; eauto. intro RES.
-  replace (genv_next ge0) with b' by congruence.
-  split. eapply Mem.perm_drop_1; eauto. omega.
-  intros.
-  assert (0 <= ofs < 1).
-    eapply Mem.perm_alloc_3; eauto.
-    eapply Mem.perm_drop_4; eauto.
-  split. omega. eapply Mem.perm_drop_2; eauto.
-  (* older function *)
-  exploit H2; eauto. intros [A B].
-  assert (D: Mem.valid_block m b).
-    red. exploit genv_funs_range; eauto. rewrite H; auto.
-  split. erewrite <- alloc_global_perm; eauto.
-  intros. eapply B. erewrite alloc_global_perm; eauto.
-(* variables *)
-  red; intros. unfold find_funct_ptr in H3. simpl in H3.
-  exploit H2; eauto. intros [A B].
-  assert (D: Mem.valid_block m b).
-    red. exploit genv_funs_range; eauto. rewrite H; auto.
-  split. erewrite <- alloc_global_perm; eauto.
-  intros. eapply B. erewrite alloc_global_perm; eauto.
-(* nextblock *)
-  rewrite NB. simpl. rewrite H. auto.
+  intros NOTVOL. 
+  transitivity (Mem.loadbytes m3 b 0 sz). 
+  eapply Mem.loadbytes_drop; eauto. right; right; right.
+  unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem.
+  eapply store_init_data_list_loadbytes; eauto.
+  eapply store_zeros_loadbytes; eauto.
++ assert (U: Mem.unchanged_on (fun _ _ => True) m m') by (eapply alloc_global_unchanged; eauto).
+  assert (VALID: Mem.valid_block m b).
+  { red. rewrite <- H. eapply genv_defs_range; eauto. } 
+  exploit H1; eauto.
+  destruct gd0 as [f|v].
+* intros [A B]; split; intros.
+  eapply Mem.perm_unchanged_on; eauto. exact I.
+  eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I.
+* intros (A & B & C & D). split; [| split; [| split]]. 
+  red; intros. eapply Mem.perm_unchanged_on; eauto. exact I.
+  intros. eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I.
+  intros. apply load_store_init_data_invariant with m; auto. 
+  intros. eapply Mem.load_unchanged_on_1; eauto. intros; exact I.
+  intros. eapply Mem.loadbytes_unchanged_on; eauto. intros; exact I.
+- simpl. congruence.
 Qed.
 
 Lemma alloc_globals_initialized:
   forall gl ge m m',
-  genv_next ge = Mem.nextblock m ->
   alloc_globals m gl = Some m' ->
-  variables_initialized ge m ->
-  functions_initialized ge m ->
-  variables_initialized (add_globals ge gl) m' /\ functions_initialized (add_globals ge gl) m'.
+  genv_next ge = Mem.nextblock m ->
+  globals_initialized ge m ->
+  globals_initialized (add_globals ge gl) m'.
 Proof.
   induction gl; simpl; intros.
-  inv H0; auto.
-  destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|] eqn:?; try discriminate.
-  exploit alloc_global_initialized; eauto. intros [P [Q R]].
+- inv H; auto.
+- destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|] eqn:?; try discriminate.
+  exploit alloc_global_initialized; eauto. intros [P Q].
   eapply IHgl; eauto.
 Qed.
 
@@ -1265,13 +1226,21 @@ Proof.
   eapply genv_symb_range; eauto.
 Qed.
 
+Theorem find_def_not_fresh:
+  forall p b g m,
+  init_mem p = Some m ->
+  find_def (globalenv p) b = Some g -> Mem.valid_block m b.
+Proof.
+  intros. red. erewrite <- init_mem_genv_next; eauto.
+  eapply genv_defs_range; eauto.
+Qed.
+
 Theorem find_funct_ptr_not_fresh:
   forall p b f m,
   init_mem p = Some m ->
   find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b.
 Proof.
-  intros. red. erewrite <- init_mem_genv_next; eauto.
-  eapply genv_funs_range; eauto.
+  intros. rewrite find_funct_ptr_iff in H0. eapply find_def_not_fresh; eauto.
 Qed.
 
 Theorem find_var_info_not_fresh:
@@ -1279,8 +1248,18 @@ Theorem find_var_info_not_fresh:
   init_mem p = Some m ->
   find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b.
 Proof.
-  intros. red. erewrite <- init_mem_genv_next; eauto.
-  eapply genv_vars_range; eauto.
+  intros. rewrite find_var_info_iff in H0. eapply find_def_not_fresh; eauto.
+Qed.
+
+Lemma init_mem_characterization_gen:
+  forall p m,
+  init_mem p = Some m ->
+  globals_initialized (globalenv p) (globalenv p) m.
+Proof.
+  intros. apply alloc_globals_initialized with Mem.empty. 
+  auto.
+  rewrite Mem.nextblock_empty. auto.
+  red; intros. unfold find_def in H0; simpl in H0; rewrite PTree.gempty in H0; discriminate.
 Qed.
 
 Theorem init_mem_characterization:
@@ -1290,12 +1269,13 @@ Theorem init_mem_characterization:
   Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Cur (perm_globvar gv)
   /\ (forall ofs k p, Mem.perm m b ofs k p ->
         0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p)
-  /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)).
+  /\ (gv.(gvar_volatile) = false ->
+      load_store_init_data (globalenv p) m b 0 gv.(gvar_init))
+  /\ (gv.(gvar_volatile) = false ->
+      Mem.loadbytes m b 0 (init_data_list_size gv.(gvar_init)) = Some (bytes_of_init_data_list (globalenv p) gv.(gvar_init))).
 Proof.
-  intros. eapply alloc_globals_initialized; eauto.
-  rewrite Mem.nextblock_empty. auto.
-  red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
-  red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
+  intros. rewrite find_var_info_iff in H.
+  exploit init_mem_characterization_gen; eauto.
 Qed.
 
 Theorem init_mem_characterization_2:
@@ -1303,12 +1283,10 @@ Theorem init_mem_characterization_2:
   find_funct_ptr (globalenv p) b = Some fd ->
   init_mem p = Some m ->
   Mem.perm m b 0 Cur Nonempty
-  /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p).
+  /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ p = Nonempty).
 Proof.
-  intros. unfold init_mem in H0. eapply alloc_globals_initialized; eauto.
-  rewrite Mem.nextblock_empty. auto.
-  red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
-  red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
+  intros. rewrite find_funct_ptr_iff in H.
+  exploit init_mem_characterization_gen; eauto.
 Qed.
 
 (** ** Compatibility with memory injections *)
@@ -1426,302 +1404,296 @@ Proof.
   apply Ple_refl.
 Qed.
 
-Section INITMEM_AUGMENT_INJ.
+(** ** Sufficient and necessary conditions for the initial memory to exist. *)
+
+(** Alignment properties *)
+
+Definition init_data_alignment (i: init_data) : Z :=
+  match i with
+  | Init_int8 n => 1
+  | Init_int16 n => 2
+  | Init_int32 n => 4
+  | Init_int64 n => 8
+  | Init_float32 n => 4
+  | Init_float64 n => 4
+  | Init_addrof symb ofs => 4
+  | Init_space n => 1
+  end.
+
+Fixpoint init_data_list_aligned (p: Z) (il: list init_data) {struct il} : Prop :=
+  match il with
+  | nil => True
+  | i1 :: il => (init_data_alignment i1 | p) /\ init_data_list_aligned (p + init_data_size i1) il
+  end.
+
+Section INITMEM_INVERSION.
 
 Variable ge: t.
-Variable thr: block.
 
-Lemma store_zeros_augment:
-  forall m1 m2 b p n m2',
-  Mem.inject (Mem.flat_inj thr) m1 m2 ->
-  Ple thr b ->
-  store_zeros m2 b p n = Some m2' ->
-  Mem.inject (Mem.flat_inj thr) m1 m2'.
+Lemma store_init_data_aligned:
+  forall m b p i m',
+  store_init_data ge m b p i = Some m' ->
+  (init_data_alignment i | p).
 Proof.
-  intros until n. functional induction (store_zeros m2 b p n); intros.
-  inv H1; auto.
-  apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl.
-  intros. exfalso. unfold Mem.flat_inj in H2. destruct (plt b' thr).
-  inv H2. unfold Plt, Ple in *. zify; omega.
-  discriminate.
-  discriminate.
+  intros.
+  assert (DFL: forall chunk v,
+    Mem.store chunk m b p v = Some m' ->
+    align_chunk chunk = init_data_alignment i ->
+    (init_data_alignment i | p)).
+  { intros. apply Mem.store_valid_access_3 in H0. destruct H0. congruence. }
+  destruct i; simpl in H; eauto.
+  simpl. apply Z.divide_1_l.
+  destruct (find_symbol ge i); try discriminate. eauto.
 Qed.
 
-Lemma store_init_data_augment:
-  forall m1 m2 b p id m2',
-  Mem.inject (Mem.flat_inj thr) m1 m2 ->
-  Ple thr b ->
-  store_init_data ge m2 b p id = Some m2' ->
-  Mem.inject (Mem.flat_inj thr) m1 m2'.
-Proof.
-  intros until m2'. intros INJ BND ST.
-  assert (P: forall chunk ofs v m2',
-             Mem.store chunk m2 b ofs v = Some m2' ->
-             Mem.inject (Mem.flat_inj thr) m1 m2').
-    intros. eapply Mem.store_outside_inject; eauto.
-    intros. unfold Mem.flat_inj in H0.
-    destruct (plt b' thr); inv H0. unfold Plt, Ple in *. zify; omega.
-  destruct id; simpl in ST; try (eapply P; eauto; fail).
-  congruence.
-  revert ST.  caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto.
+Lemma store_init_data_list_aligned:
+  forall b il m p m',
+  store_init_data_list ge m b p il = Some m' ->
+  init_data_list_aligned p il.
+Proof.
+  induction il as [ | i1 il]; simpl; intros.
+- auto.
+- destruct (store_init_data ge m b p i1) as [m1|] eqn:S1; try discriminate.
+  split; eauto. eapply store_init_data_aligned; eauto.
 Qed.
 
-Lemma store_init_data_list_augment:
-  forall b idl m1 m2 p m2',
-  Mem.inject (Mem.flat_inj thr) m1 m2 ->
-  Ple thr b ->
-  store_init_data_list ge m2 b p idl = Some m2' ->
-  Mem.inject (Mem.flat_inj thr) m1 m2'.
+Lemma store_init_data_list_free_idents:
+  forall b i o il m p m',
+  store_init_data_list ge m b p il = Some m' ->
+  In (Init_addrof i o) il ->
+  exists b', find_symbol ge i = Some b'.
 Proof.
-  induction idl; simpl.
-  intros; congruence.
-  intros until m2'; intros INJ FB.
-  caseEq (store_init_data ge m2 b p a); try congruence. intros.
-  eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto.
+  induction il as [ | i1 il]; simpl; intros.
+- contradiction.
+- destruct (store_init_data ge m b p i1) as [m1|] eqn:S1; try discriminate.
+  destruct H0.
++ subst i1. simpl in S1. destruct (find_symbol ge i) as [b'|]. exists b'; auto. discriminate.
++ eapply IHil; eauto.
 Qed.
 
-Lemma alloc_global_augment:
-  forall idg m1 m2 m2',
-  alloc_global ge m2 idg = Some m2' ->
-  Mem.inject (Mem.flat_inj thr) m1 m2 ->
-  Ple thr (Mem.nextblock m2) ->
-  Mem.inject (Mem.flat_inj thr) m1 m2'.
-Proof.
-  intros. destruct idg as [id [f|v]]; simpl in H.
-  (* function *)
-  destruct (Mem.alloc m2 0 1) as [m3 b] eqn:?.
-  assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
-  eapply Mem.drop_outside_inject. 2: eauto.
-  eapply Mem.alloc_right_inject; eauto.
-  intros. unfold Mem.flat_inj in H3. destruct (plt b' thr); inv H3.
-  unfold Plt, Ple in *. zify; omega.
-  (* variable *)
-  set (init := gvar_init v) in *.
-  set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m2 0 sz) as [m3 b] eqn:?.
-  destruct (store_zeros m3 b 0 sz) as [m4|] eqn:?; try discriminate.
-  destruct (store_init_data_list ge m4 b 0 init) as [m5|] eqn:?; try discriminate.
-  assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
-  eapply Mem.drop_outside_inject. 2: eauto.
-  eapply store_init_data_list_augment. 3: eauto. 2: eauto.
-  eapply store_zeros_augment. 3: eauto. 2: eauto.
-  eapply Mem.alloc_right_inject; eauto.
-  intros. unfold Mem.flat_inj in H3. destruct (plt b' thr); inv H3.
-  unfold Plt, Ple in *. zify; omega.
-Qed.
-
-Lemma alloc_globals_augment:
-  forall gl m1 m2 m2',
-  alloc_globals ge m2 gl = Some m2' ->
-  Mem.inject (Mem.flat_inj thr) m1 m2 ->
-  Ple thr (Mem.nextblock m2) ->
-  Mem.inject (Mem.flat_inj thr) m1 m2'.
-Proof.
-  induction gl; simpl.
-  intros. congruence.
-  intros until m2'. caseEq (alloc_global ge m2 a); try congruence. intros.
-  eapply IHgl with (m2 := m); eauto.
-    eapply alloc_global_augment; eauto.
-    rewrite (alloc_global_nextblock _ _ _ H).
-    apply Ple_trans with (Mem.nextblock m2); auto. apply Ple_succ.
+End INITMEM_INVERSION.
+
+Theorem init_mem_inversion:
+  forall p m id v,
+  init_mem p = Some m ->
+  In (id, Gvar v) p.(prog_defs) ->
+  init_data_list_aligned 0 v.(gvar_init)
+  /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b.
+Proof.
+  intros until v. unfold init_mem. set (ge := globalenv p). 
+  revert m. generalize Mem.empty. generalize (prog_defs p). 
+  induction l as [ | idg1 defs ]; simpl; intros m m'; intros.
+- contradiction.
+- destruct (alloc_global ge m idg1) as [m''|] eqn:A; try discriminate.
+  destruct H0.
++ subst idg1; simpl in A. 
+  set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *. 
+  destruct (Mem.alloc m 0 sz) as [m1 b].
+  destruct (store_zeros m1 b 0 sz) as [m2|]; try discriminate.
+  destruct (store_init_data_list ge m2 b 0 il) as [m3|] eqn:B; try discriminate.
+  split. eapply store_init_data_list_aligned; eauto. intros; eapply store_init_data_list_free_idents; eauto.
++ eapply IHdefs; eauto.
+Qed.
+
+Section INITMEM_EXISTS.
+
+Variable ge: t.
+
+Lemma store_zeros_exists:
+  forall m b p n,
+  Mem.range_perm m b p (p + n) Cur Writable ->
+  exists m', store_zeros m b p n = Some m'.
+Proof.
+  intros until n. functional induction (store_zeros m b p n); intros PERM.
+- exists m; auto.
+- apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. omega.
+- destruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & STORE).
+  split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. 
+  simpl. apply Z.divide_1_l.
+  congruence.
 Qed.
 
-End INITMEM_AUGMENT_INJ.
+Lemma store_init_data_exists:
+  forall m b p i,
+  Mem.range_perm m b p (p + init_data_size i) Cur Writable ->
+  (init_data_alignment i | p) ->
+  (forall id ofs, i = Init_addrof id ofs -> exists b, find_symbol ge id = Some b) ->
+  exists m', store_init_data ge m b p i = Some m'.
+Proof.
+  intros. 
+  assert (DFL: forall chunk v,
+          init_data_size i = size_chunk chunk ->
+          init_data_alignment i = align_chunk chunk ->
+          exists m', Mem.store chunk m b p v = Some m').
+  { intros. destruct (Mem.valid_access_store m chunk b p v) as (m' & STORE).
+    split. rewrite <- H2; auto. rewrite <- H3; auto. 
+    exists m'; auto. }
+  destruct i; eauto.
+  simpl. exists m; auto.
+  simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eauto. 
+Qed.
+
+Lemma store_init_data_list_exists:
+  forall b il m p,
+  Mem.range_perm m b p (p + init_data_list_size il) Cur Writable ->
+  init_data_list_aligned p il ->
+  (forall id ofs, In (Init_addrof id ofs) il -> exists b, find_symbol ge id = Some b) ->
+  exists m', store_init_data_list ge m b p il = Some m'.
+Proof.
+  induction il as [ | i1 il ]; simpl; intros.
+- exists m; auto.
+- destruct H0. 
+  destruct (@store_init_data_exists m b p i1) as (m1 & S1); eauto.
+  red; intros. apply H. generalize (init_data_list_size_pos il); omega.
+  rewrite S1. 
+  apply IHil; eauto. 
+  red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); omega.
+Qed.
+
+Lemma alloc_global_exists:
+  forall m idg,
+  match idg with
+  | (id, Gfun f) => True
+  | (id, Gvar v) =>
+        init_data_list_aligned 0 v.(gvar_init)
+     /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol ge i = Some b
+  end ->
+  exists m', alloc_global ge m idg = Some m'.
+Proof.
+  intros m [id [f|v]]; intros; simpl.
+- destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC.
+  destruct (Mem.range_perm_drop_2 m1 b 0 1 Nonempty) as [m2 DROP].
+  red; intros; eapply Mem.perm_alloc_2; eauto. 
+  exists m2; auto.
+- destruct H as [P Q].
+  set (sz := init_data_list_size (gvar_init v)).
+  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:ALLOC.
+  assert (P1: Mem.range_perm m1 b 0 sz Cur Freeable) by (red; intros; eapply Mem.perm_alloc_2; eauto).
+  destruct (@store_zeros_exists m1 b 0 sz) as [m2 ZEROS].
+  red; intros. apply Mem.perm_implies with Freeable; auto with mem.
+  rewrite ZEROS.
+  assert (P2: Mem.range_perm m2 b 0 sz Cur Freeable).
+  { red; intros. erewrite <- store_zeros_perm by eauto. eauto. }
+  destruct (@store_init_data_list_exists b (gvar_init v) m2 0) as [m3 STORE]; auto.
+  red; intros. apply Mem.perm_implies with Freeable; auto with mem.
+  rewrite STORE.
+  assert (P3: Mem.range_perm m3 b 0 sz Cur Freeable).
+  { red; intros. erewrite <- store_init_data_list_perm by eauto. eauto. }
+  destruct (Mem.range_perm_drop_2 m3 b 0 sz (perm_globvar v)) as [m4 DROP]; auto.
+  exists m4; auto.
+Qed.
+
+End INITMEM_EXISTS.
+
+Theorem init_mem_exists:
+  forall p,
+  (forall id v, In (id, Gvar v) (prog_defs p) ->
+        init_data_list_aligned 0 v.(gvar_init)
+     /\ forall i o, In (Init_addrof i o) v.(gvar_init) -> exists b, find_symbol (globalenv p) i = Some b) ->
+  exists m, init_mem p = Some m.
+Proof.
+  intros. set (ge := globalenv p) in *. 
+  unfold init_mem. revert H. generalize (prog_defs p) Mem.empty.
+  induction l as [ | idg l]; simpl; intros.
+- exists m; auto.
+- destruct (@alloc_global_exists ge m idg) as [m1 A1].
+  destruct idg as [id [f|v]]; eauto.
+  fold ge. rewrite A1. eapply IHl; eauto. 
+Qed. 
 
 End GENV.
 
 (** * Commutation with program transformations *)
 
-(** ** Commutation with matching between programs. *)
-
-Section MATCH_PROGRAMS.
-
-Variables A B V W: Type.
-Variable match_fun: A -> B -> Prop.
-Variable match_varinfo: V -> W -> Prop.
+Section MATCH_GENVS.
 
-Inductive match_globvar: globvar V -> globvar W -> Prop :=
-  | match_globvar_intro: forall info1 info2 init ro vo,
-      match_varinfo info1 info2 ->
-      match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo).
+Context {A B V W: Type} (R: globdef A V -> globdef B W -> Prop).
 
-Record match_genvs (new_globs : list (ident * globdef B W))
-                   (ge1: t A V) (ge2: t B W): Prop := {
+Record match_genvs (ge1: t A V) (ge2: t B W): Prop := {
   mge_next:
-    genv_next ge2 = advance_next new_globs (genv_next ge1);
+    genv_next ge2 = genv_next ge1;
   mge_symb:
-    forall id, ~ In id (map fst new_globs) ->
-                   PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1);
-  mge_funs:
-    forall b f, PTree.get b (genv_funs ge1) = Some f ->
-    exists tf, PTree.get b (genv_funs ge2) = Some tf /\ match_fun f tf;
-  mge_rev_funs:
-    forall b tf, PTree.get b (genv_funs ge2) = Some tf ->
-    if plt b (genv_next ge1) then
-      exists f, PTree.get b (genv_funs ge1) = Some f /\ match_fun f tf
-    else
-      In (Gfun tf) (map snd new_globs);
-  mge_vars:
-    forall b v, PTree.get b (genv_vars ge1) = Some v ->
-    exists tv, PTree.get b (genv_vars ge2) = Some tv /\ match_globvar v tv;
-  mge_rev_vars:
-    forall b tv, PTree.get b (genv_vars ge2) = Some tv ->
-    if plt b (genv_next ge1) then
-      exists v, PTree.get b (genv_vars ge1) = Some v /\ match_globvar v tv
-    else
-      In (Gvar tv) (map snd new_globs)
+    forall id, PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1);
+  mge_defs:
+    forall b, option_rel R (PTree.get b (genv_defs ge1)) (PTree.get b (genv_defs ge2))
 }.
 
 Lemma add_global_match:
-  forall ge1 ge2 idg1 idg2,
-  match_genvs nil ge1 ge2 ->
-  match_globdef match_fun match_varinfo idg1 idg2 ->
-  match_genvs nil (add_global ge1 idg1) (add_global ge2 idg2).
-Proof.
-  intros. destruct H. simpl in mge_next0.
-  inv H0.
-(* two functions *)
-  constructor; simpl.
-  congruence.
-  intros. rewrite mge_next0.
-    repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
-  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec.
-    destruct (peq b (genv_next ge1)).
-     exists f2; split; congruence.
-     eauto.
-  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec.
-   destruct (peq b (genv_next ge1)).
-    subst b. rewrite pred_dec_true. exists f1; split; congruence. apply Plt_succ.
-    pose proof (mge_rev_funs0 b tf H0).
-    destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
-    contradiction.
-  eauto.
-  intros.
-    pose proof (mge_rev_vars0 b tv H0).
-    destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto.
-    apply Plt_trans with (genv_next ge1); auto. apply Plt_succ.
-    contradiction.
-(* two variables *)
-  constructor; simpl.
-  congruence.
-  intros. rewrite mge_next0.
-    repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
-  eauto.
-  intros.
-    pose proof (mge_rev_funs0 b tf H0).
-    destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
-    contradiction.
-  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec.
-    destruct (peq b (genv_next ge1)).
-    econstructor; split. eauto. inv H0. constructor; auto.
-    eauto.
-  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec.
-   destruct (peq b (genv_next ge1)).
-    subst b. rewrite pred_dec_true.
-    econstructor; split. eauto. inv H0. constructor; auto. apply Plt_succ.
-    pose proof (mge_rev_vars0 b tv H0).
-    destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
-    contradiction.
+  forall ge1 ge2 id g1 g2,
+  match_genvs ge1 ge2 ->
+  R g1 g2 ->
+  match_genvs (add_global ge1 (id, g1)) (add_global ge2 (id, g2)).
+Proof.
+  intros. destruct H. constructor; simpl; intros.
+- congruence.
+- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto. 
+- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)). 
+  constructor; auto.
+  auto.
 Qed.
 
 Lemma add_globals_match:
-  forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 ->
-  forall ge1 ge2, match_genvs nil ge1 ge2 ->
-  match_genvs nil (add_globals ge1 gl1) (add_globals ge2 gl2).
+  forall gl1 gl2,
+  list_forall2 (fun idg1 idg2 => fst idg1 = fst idg2 /\ R (snd idg1) (snd idg2)) gl1 gl2 ->
+  forall ge1 ge2, match_genvs ge1 ge2 ->
+  match_genvs (add_globals ge1 gl1) (add_globals ge2 gl2).
 Proof.
   induction 1; intros; simpl.
   auto.
+  destruct a1 as [id1 g1]; destruct b1 as [id2 g2]; simpl in *; destruct H; subst id2.
   apply IHlist_forall2. apply add_global_match; auto.
 Qed.
 
-Lemma add_global_augment_match:
-  forall new_globs ge1 ge2 idg,
-  match_genvs new_globs ge1 ge2 ->
-  match_genvs (new_globs ++ (idg :: nil)) ge1 (add_global ge2 idg).
-Proof.
-  intros. destruct H.
-  assert (LE: Ple (genv_next ge1) (genv_next ge2)).
-  { rewrite mge_next0; apply advance_next_le. }
-  constructor; simpl.
-  rewrite mge_next0. unfold advance_next. rewrite fold_left_app. simpl. auto.
-  intros. rewrite map_app in H. rewrite in_app in H. simpl in H.
-    destruct (peq id idg#1). subst. intuition. rewrite PTree.gso.
-    apply mge_symb0. intuition. auto.
-  intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
-    rewrite PTree.gso. eauto.
-    exploit genv_funs_range; eauto. intros.
-    unfold Plt, Ple in *; zify; omega.
-  intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
-    rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)).
-    rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence.
-    subst b. unfold Plt, Ple in *; zify; omega.
-    exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto.
-    rewrite in_app. tauto.
-    exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto.
-    rewrite in_app. tauto.
-  intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
-    rewrite PTree.gso. eauto. exploit genv_vars_range; eauto.
-    unfold Plt, Ple in *; zify; omega.
-  intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
-    exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto.
-    rewrite in_app. tauto.
-    rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)).
-    rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence.
-    subst b. unfold Plt, Ple in *; zify; omega.
-    exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto.
-    rewrite in_app. tauto.
-Qed.
-
-Lemma add_globals_augment_match:
-  forall gl new_globs ge1 ge2,
-  match_genvs new_globs ge1 ge2 ->
-  match_genvs (new_globs ++ gl) ge1 (add_globals ge2 gl).
-Proof.
-  induction gl; simpl.
-    intros. rewrite app_nil_r. auto.
-    intros. change (a :: gl) with ((a :: nil) ++ gl). rewrite <- app_ass.
-      apply IHgl. apply add_global_augment_match. auto.
-Qed.
-
-Variable new_globs : list (ident * globdef B W).
-Variable new_main : ident.
-
-Variable p: program A V.
-Variable p': program B W.
-Hypothesis progmatch:
-  match_program match_fun match_varinfo new_globs new_main p p'.
+End MATCH_GENVS.
+
+Section MATCH_PROGRAMS.
+
+Context {C F1 V1 F2 V2: Type} {LC: Linker C} {LF: Linker F1} {LV: Linker V1}.
+Variable match_fundef: C -> F1 -> F2 -> Prop.
+Variable match_varinfo: V1 -> V2 -> Prop.
+Variable ctx: C.
+Variable p: program F1 V1.
+Variable tp: program F2 V2.
+Hypothesis progmatch: match_program_gen match_fundef match_varinfo ctx p tp.
 
 Lemma globalenvs_match:
-  match_genvs new_globs (globalenv p) (globalenv p').
+  match_genvs (match_globdef match_fundef match_varinfo ctx) (globalenv p) (globalenv tp).
+Proof.
+  intros. apply add_globals_match. apply progmatch. 
+  constructor; simpl; intros; auto. rewrite ! PTree.gempty. constructor.
+Qed.
+
+Theorem find_def_match_2:
+  forall b, option_rel (match_globdef match_fundef match_varinfo ctx)
+                       (find_def (globalenv p) b) (find_def (globalenv tp) b).
+Proof (mge_defs globalenvs_match).
+
+Theorem find_def_match:
+  forall b g,
+  find_def (globalenv p) b = Some g ->
+  exists tg,
+  find_def (globalenv tp) b = Some tg /\ match_globdef match_fundef match_varinfo ctx g tg.
 Proof.
-  unfold globalenv. destruct progmatch as [[tglob [P Q]] R].
-  rewrite Q. rewrite add_globals_app.
-  change new_globs with (nil ++ new_globs) at 1.
-  apply add_globals_augment_match.
-  apply add_globals_match; auto.
-  constructor; simpl; auto; intros; rewrite PTree.gempty in H; congruence.
+  intros. generalize (find_def_match_2 b). rewrite H; intros R; inv R.
+  exists y; auto. 
 Qed.
 
 Theorem find_funct_ptr_match:
-  forall (b : block) (f : A),
+  forall b f,
   find_funct_ptr (globalenv p) b = Some f ->
-  exists tf : B,
-  find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf.
-Proof (mge_funs globalenvs_match).
-
-Theorem find_funct_ptr_rev_match:
-  forall (b : block) (tf : B),
-  find_funct_ptr (globalenv p') b = Some tf ->
-  if plt b (genv_next (globalenv p)) then
-      exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf
-  else
-      In (Gfun tf) (map snd new_globs).
-Proof (mge_rev_funs globalenvs_match).
+  exists cunit tf,
+  find_funct_ptr (globalenv tp) b = Some tf /\ match_fundef cunit f tf /\ linkorder cunit ctx.
+Proof.
+  intros. rewrite find_funct_ptr_iff in *. apply find_def_match in H. 
+  destruct H as (tg & P & Q). inv Q. 
+  exists ctx', f2; intuition auto. apply find_funct_ptr_iff; auto.
+Qed.
 
 Theorem find_funct_match:
-  forall (v : val) (f : A),
+  forall v f,
   find_funct (globalenv p) v = Some f ->
-  exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf.
+  exists cunit tf,
+  find_funct (globalenv tp) v = Some tf /\ match_fundef cunit f tf /\ linkorder cunit ctx.
 Proof.
   intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v.
   rewrite find_funct_find_funct_ptr in H.
@@ -1729,569 +1701,180 @@ Proof.
   apply find_funct_ptr_match. auto.
 Qed.
 
-Theorem find_funct_rev_match:
-  forall (v : val) (tf : B),
-  find_funct (globalenv p') v = Some tf ->
-  (exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf)
-  \/ (In (Gfun tf) (map snd new_globs)).
-Proof.
-  intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v.
-  rewrite find_funct_find_funct_ptr in H.
-  rewrite find_funct_find_funct_ptr.
-  apply find_funct_ptr_rev_match in H.
-   destruct (plt b (genv_next (globalenv p))); auto.
-Qed.
-
 Theorem find_var_info_match:
-  forall (b : block) (v : globvar V),
+  forall b v,
   find_var_info (globalenv p) b = Some v ->
   exists tv,
-  find_var_info (globalenv p') b = Some tv /\ match_globvar v tv.
-Proof (mge_vars globalenvs_match).
-
-Theorem find_var_info_rev_match:
-  forall (b : block) (tv : globvar W),
-  find_var_info (globalenv p') b = Some tv ->
-  if plt b (genv_next (globalenv p)) then
-    exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv
-  else
-    In (Gvar tv) (map snd new_globs).
-Proof (mge_rev_vars globalenvs_match).
+  find_var_info (globalenv tp) b = Some tv /\ match_globvar match_varinfo v tv.
+Proof.
+  intros. rewrite find_var_info_iff in *. apply find_def_match in H. 
+  destruct H as (tg & P & Q). inv Q. 
+  exists v2; split; auto. apply find_var_info_iff; auto.
+Qed.
 
 Theorem find_symbol_match:
   forall (s : ident),
-  ~In s (map fst new_globs) ->
-  find_symbol (globalenv p') s = find_symbol (globalenv p) s.
+  find_symbol (globalenv tp) s = find_symbol (globalenv p) s.
 Proof.
-  intros. destruct globalenvs_match. unfold find_symbol.  auto.
+  intros. destruct globalenvs_match. apply mge_symb0.
 Qed.
 
-Theorem public_symbol_match:
-  forall (s : ident),
-  ~In s (map fst new_globs) ->
-  public_symbol (globalenv p') s = public_symbol (globalenv p) s.
+Theorem senv_match:
+  Senv.equiv (to_senv (globalenv p)) (to_senv (globalenv tp)).
 Proof.
-  intros. unfold public_symbol. rewrite find_symbol_match by auto.
-  destruct (find_symbol (globalenv p) s); auto.
-  rewrite ! globalenv_public.
+  red; simpl. repeat split.
+- apply find_symbol_match.
+- intros. unfold public_symbol. rewrite find_symbol_match. 
+  rewrite ! globalenv_public. 
   destruct progmatch as (P & Q & R). rewrite R. auto.
+- intros. unfold block_is_volatile. 
+  destruct globalenvs_match as [P Q R]. specialize (R b).
+  unfold find_var_info, find_def.
+  inv R; auto.
+  inv H1; auto.
+  inv H2; auto.
 Qed.
 
-Hypothesis new_ids_fresh:
-  forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False.
-Hypothesis new_ids_unique:
-  list_norepet (map fst new_globs).
-
 Lemma store_init_data_list_match:
   forall idl m b ofs m',
   store_init_data_list (globalenv p) m b ofs idl = Some m' ->
-  store_init_data_list (globalenv p') m b ofs idl = Some m'.
+  store_init_data_list (globalenv tp) m b ofs idl = Some m'.
 Proof.
   induction idl; simpl; intros.
-  auto.
-  assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' ->
-          store_init_data (globalenv p') m b ofs a = Some m').
-   destruct a; simpl; auto. rewrite find_symbol_match. auto.
-   simpl in H. destruct (find_symbol (globalenv p) i) as [b'|] eqn:?; try discriminate.
-   red; intros. exploit find_symbol_inversion; eauto.
-  case_eq (store_init_data (globalenv p) m b ofs a); intros.
-    rewrite H1 in H.
-    pose proof (H0 _ H1). rewrite H2. auto.
-    rewrite H1 in H. inversion H.
+- auto.
+- destruct (store_init_data (globalenv p) m b ofs a) as [m1|] eqn:S; try discriminate.
+  assert (X: store_init_data (globalenv tp) m b ofs a = Some m1).
+  { destruct a; auto. simpl; rewrite find_symbol_match; auto. }
+  rewrite X. auto.
 Qed.
 
 Lemma alloc_globals_match:
-  forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 ->
+  forall gl1 gl2, list_forall2 (match_ident_globdef match_fundef match_varinfo ctx) gl1 gl2 ->
   forall m m',
   alloc_globals (globalenv p) m gl1 = Some m' ->
-  alloc_globals (globalenv p') m gl2 = Some m'.
+  alloc_globals (globalenv tp) m gl2 = Some m'.
 Proof.
   induction 1; simpl; intros.
-  auto.
-  destruct (alloc_global (globalenv p) m a1) as [m1|] eqn:?; try discriminate.
-  assert (alloc_global (globalenv p') m b1 = Some m1).
-    inv H; simpl in *.
-    auto.
+- auto.
+- destruct (alloc_global (globalenv p) m a1) as [m1|] eqn:?; try discriminate.
+  assert (X: alloc_global (globalenv tp) m b1 = Some m1).
+  { destruct a1 as [id1 g1]; destruct b1 as [id2 g2]; destruct H; simpl in *.
+    subst id2. inv H2.
+  - auto.
+  - inv H; simpl in *. 
     set (sz := init_data_list_size init) in *.
     destruct (Mem.alloc m 0 sz) as [m2 b] eqn:?.
     destruct (store_zeros m2 b 0 sz) as [m3|] eqn:?; try discriminate.
     destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|] eqn:?; try discriminate.
     erewrite store_init_data_list_match; eauto.
-  rewrite H2. eauto.
+  }
+  rewrite X; eauto.
 Qed.
 
 Theorem init_mem_match:
-  forall m, init_mem p = Some m ->
-  init_mem p' = alloc_globals (globalenv p') m new_globs.
+  forall m, init_mem p = Some m -> init_mem tp = Some m.
 Proof.
   unfold init_mem; intros.
-  destruct progmatch as [[tglob [P Q]] R].
-  rewrite Q. erewrite <- alloc_globals_app; eauto.
-  eapply alloc_globals_match; eauto.
-Qed.
-
-Theorem find_new_funct_ptr_match:
-  forall id f, In (id, Gfun f) new_globs ->
-  exists b,
-     find_symbol (globalenv p') id = Some b
-  /\ find_funct_ptr (globalenv p') b = Some f.
-Proof.
-  intros.
-  destruct progmatch as [[tglob [P Q]] R].
-  exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T).
-  rewrite S in Q. rewrite <- app_ass in Q.
-  eapply find_funct_ptr_exists_2; eauto.
-Qed.
-
-Theorem find_new_var_match:
-  forall id v, In (id, Gvar v) new_globs ->
-  exists b,
-     find_symbol (globalenv p') id = Some b
-  /\ find_var_info (globalenv p') b = Some v.
-Proof.
-  intros.
-  destruct progmatch as [[tglob [P Q]] R].
-  exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T).
-  rewrite S in Q. rewrite <- app_ass in Q.
-  eapply find_var_exists_2; eauto.
+  eapply alloc_globals_match; eauto. apply progmatch.
 Qed.
 
 End MATCH_PROGRAMS.
 
-Section TRANSF_PROGRAM_AUGMENT.
-
-Variable A B V W: Type.
-Variable transf_fun: A -> res B.
-Variable transf_var: V -> res W.
+(** Special case for partial transformations that do not depend on the compilation unit *)
 
-Variable new_globs : list (ident * globdef B W).
-Variable new_main : ident.
+Section TRANSFORM_PARTIAL.
 
-Variable p: program A V.
-Variable p': program B W.
-
-Hypothesis transf_OK:
-  transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK p'.
-
-Let prog_match:
-  match_program
-    (fun fd tfd => transf_fun fd = OK tfd)
-    (fun info tinfo => transf_var info = OK tinfo)
-    new_globs new_main
-    p p'.
-Proof.
-  apply transform_partial_augment_program_match; auto.
-Qed.
-
-Theorem find_funct_ptr_transf_augment:
-  forall (b: block) (f: A),
-  find_funct_ptr (globalenv p) b = Some f ->
-  exists f',
-  find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
-Proof.
-  intros.
-  exploit find_funct_ptr_match. eexact prog_match. eauto.
-  intros [tf [X Y]]. exists tf; auto.
-Qed.
-
-Theorem find_funct_ptr_rev_transf_augment:
-  forall (b: block) (tf: B),
-  find_funct_ptr (globalenv p') b = Some tf ->
-  if plt b (genv_next (globalenv p)) then
-   (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf)
-  else
-   In (Gfun tf) (map snd new_globs).
-Proof.
-  intros.
-  exploit find_funct_ptr_rev_match; eauto.
-Qed.
-
-Theorem find_funct_transf_augment:
-  forall (v: val) (f: A),
-  find_funct (globalenv p) v = Some f ->
-  exists f',
-  find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
-Proof.
-  intros.
-  exploit find_funct_match. eexact prog_match. eauto. auto.
-Qed.
-
-Theorem find_funct_rev_transf_augment:
-  forall (v: val) (tf: B),
-  find_funct (globalenv p') v = Some tf ->
-  (exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf) \/
-  In (Gfun tf) (map snd new_globs).
-Proof.
-  intros.
-  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
-Qed.
-
-Theorem find_var_info_transf_augment:
-  forall (b: block) (v: globvar V),
-  find_var_info (globalenv p) b = Some v ->
-  exists v',
-  find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'.
-Proof.
-  intros.
-  exploit find_var_info_match. eexact prog_match. eauto. intros [tv [X Y]].
-  exists tv; split; auto. inv Y. unfold transf_globvar; simpl.
-  rewrite H0; simpl. auto.
-Qed.
-
-Theorem find_var_info_rev_transf_augment:
-  forall (b: block) (v': globvar W),
-  find_var_info (globalenv p') b = Some v' ->
-  if plt b (genv_next (globalenv p)) then
-    (exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v')
-  else
-    (In (Gvar v') (map snd new_globs)).
-Proof.
-  intros.
-  exploit find_var_info_rev_match. eexact prog_match. eauto.
-  destruct (plt b (genv_next (globalenv p))); auto.
-  intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl.
-  rewrite H0; simpl. auto.
-Qed.
-
-Theorem find_symbol_transf_augment:
-  forall (s: ident),
-  ~ In s (map fst new_globs) ->
-  find_symbol (globalenv p') s = find_symbol (globalenv p) s.
-Proof.
-  intros. eapply find_symbol_match. eexact prog_match. auto.
-Qed.
-
-Theorem public_symbol_transf_augment:
-  forall (s: ident),
-  ~ In s (map fst new_globs) ->
-  public_symbol (globalenv p') s = public_symbol (globalenv p) s.
-Proof.
-  intros. eapply public_symbol_match. eexact prog_match. auto.
-Qed.
-
-Hypothesis new_ids_fresh:
-  forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False.
-Hypothesis new_ids_unique:
-  list_norepet (map fst new_globs).
-
-Theorem init_mem_transf_augment:
-   forall m, init_mem p = Some m ->
-   init_mem p' = alloc_globals (globalenv p') m new_globs.
-Proof.
-  intros. eapply init_mem_match. eexact prog_match. auto. auto.
-Qed.
-
-Theorem init_mem_inject_transf_augment:
-  forall m, init_mem p = Some m ->
-  forall m', init_mem p' = Some m' ->
-  Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'.
-Proof.
-  intros.
-  pose proof (initmem_inject p H).
-  erewrite init_mem_transf_augment in H0; eauto.
-  eapply alloc_globals_augment; eauto. apply Ple_refl.
-Qed.
-
-Theorem find_new_funct_ptr_exists:
-  forall id f, In (id, Gfun f) new_globs ->
-  exists b, find_symbol (globalenv p') id = Some b
-         /\ find_funct_ptr (globalenv p') b = Some f.
-Proof.
-  intros. eapply find_new_funct_ptr_match; eauto.
-Qed.
-
-Theorem find_new_var_exists:
-  forall id gv, In (id, Gvar gv) new_globs ->
-  exists b, find_symbol (globalenv p') id = Some b
-         /\ find_var_info (globalenv p') b = Some gv.
-Proof.
-  intros. eapply find_new_var_match; eauto.
-Qed.
-
-End TRANSF_PROGRAM_AUGMENT.
-
-Section TRANSF_PROGRAM_PARTIAL2.
-
-Variable A B V W: Type.
-Variable transf_fun: A -> res B.
-Variable transf_var: V -> res W.
-Variable p: program A V.
-Variable p': program B W.
-Hypothesis transf_OK:
-  transform_partial_program2 transf_fun transf_var p = OK p'.
-
-Remark transf_augment_OK:
-  transform_partial_augment_program transf_fun transf_var nil p.(prog_main) p = OK p'.
-Proof.
-  rewrite <- transf_OK. symmetry. apply transform_partial_program2_augment.
-Qed.
-
-Theorem find_funct_ptr_transf_partial2:
-  forall (b: block) (f: A),
-  find_funct_ptr (globalenv p) b = Some f ->
-  exists f',
-  find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
-Proof.
-  exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-Qed.
-
-Theorem find_funct_ptr_rev_transf_partial2:
-  forall (b: block) (tf: B),
-  find_funct_ptr (globalenv p') b = Some tf ->
-  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.
-Proof.
-  pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  intros.  pose proof (H b tf H0).
-  destruct (plt b (genv_next (globalenv p))).  auto. contradiction.
-Qed.
-
-Theorem find_funct_transf_partial2:
-  forall (v: val) (f: A),
-  find_funct (globalenv p) v = Some f ->
-  exists f',
-  find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
-Proof.
-  exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-Qed.
-
-Theorem find_funct_rev_transf_partial2:
-  forall (v: val) (tf: B),
-  find_funct (globalenv p') v = Some tf ->
-  exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.
-Proof.
-  pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  intros. pose proof (H v tf H0).
-  destruct H1. auto. contradiction.
-Qed.
-
-Theorem find_var_info_transf_partial2:
-  forall (b: block) (v: globvar V),
-  find_var_info (globalenv p) b = Some v ->
-  exists v',
-  find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'.
-Proof.
-  exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-Qed.
-
-Theorem find_var_info_rev_transf_partial2:
-  forall (b: block) (v': globvar W),
-  find_var_info (globalenv p') b = Some v' ->
-  exists v,
-  find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'.
-Proof.
-  pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  intros.  pose proof (H b v' H0).
-  destruct (plt b (genv_next (globalenv p))).  auto. contradiction.
-Qed.
-
-Theorem find_symbol_transf_partial2:
-  forall (s: ident),
-  find_symbol (globalenv p') s = find_symbol (globalenv p) s.
-Proof.
-  pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  auto.
-Qed.
-
-Theorem public_symbol_transf_partial2:
-  forall (s: ident),
-  public_symbol (globalenv p') s = public_symbol (globalenv p) s.
-Proof.
-  pose proof (@public_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  auto.
-Qed.
-
-Theorem block_is_volatile_transf_partial2:
-  forall (b: block),
-  block_is_volatile (globalenv p') b = block_is_volatile (globalenv p) b.
-Proof.
-  unfold block_is_volatile; intros.
-  destruct (find_var_info (globalenv p) b) as [v|] eqn:FV.
-  exploit find_var_info_transf_partial2; eauto. intros (v' & P & Q).
-  rewrite P. monadInv Q. auto.
-  destruct (find_var_info (globalenv p') b) as [v'|] eqn:FV'.
-  exploit find_var_info_rev_transf_partial2; eauto. intros (v & P & Q). congruence.
-  auto.
-Qed.
-
-Theorem init_mem_transf_partial2:
-  forall m, init_mem p = Some m -> init_mem p' = Some m.
-Proof.
-  pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  intros. simpl in H. apply H; auto.
-Qed.
-
-End TRANSF_PROGRAM_PARTIAL2.
-
-Section TRANSF_PROGRAM_PARTIAL.
-
-Variable A B V: Type.
-Variable transf: A -> res B.
-Variable p: program A V.
-Variable p': program B V.
-Hypothesis transf_OK: transform_partial_program transf p = OK p'.
+Context {A B V: Type} {LA: Linker A} {LV: Linker V}.
+Context {transf: A -> res B} {p: program A V} {tp: program B V}.
+Hypothesis progmatch: match_program (fun cu f tf => transf f = OK tf) eq p tp.
 
 Theorem find_funct_ptr_transf_partial:
-  forall (b: block) (f: A),
+  forall b f,
   find_funct_ptr (globalenv p) b = Some f ->
-  exists f',
-  find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'.
-Proof.
-  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
-Qed.
-
-Theorem find_funct_ptr_rev_transf_partial:
-  forall (b: block) (tf: B),
-  find_funct_ptr (globalenv p') b = Some tf ->
-  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf.
+  exists tf,
+  find_funct_ptr (globalenv tp) b = Some tf /\ transf f = OK tf.
 Proof.
-  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
+  intros. exploit (find_funct_ptr_match progmatch); eauto. 
+  intros (cu & tf & P & Q & R); exists tf; auto.
 Qed.
 
 Theorem find_funct_transf_partial:
-  forall (v: val) (f: A),
+  forall v f,
   find_funct (globalenv p) v = Some f ->
-  exists f',
-  find_funct (globalenv p') v = Some f' /\ transf f = OK f'.
-Proof.
-  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
-Qed.
-
-Theorem find_funct_rev_transf_partial:
-  forall (v: val) (tf: B),
-  find_funct (globalenv p') v = Some tf ->
-  exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf.
+  exists tf,
+  find_funct (globalenv tp) v = Some tf /\ transf f = OK tf.
 Proof.
-  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
+  intros. exploit (find_funct_match progmatch); eauto. 
+  intros (cu & tf & P & Q & R); exists tf; auto.
 Qed.
 
 Theorem find_symbol_transf_partial:
-  forall (s: ident),
-  find_symbol (globalenv p') s = find_symbol (globalenv p) s.
-Proof.
-  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
-Qed.
-
-Theorem public_symbol_transf_partial:
-  forall (s: ident),
-  public_symbol (globalenv p') s = public_symbol (globalenv p) s.
-Proof.
-  exact (@public_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
-Qed.
-
-Theorem find_var_info_transf_partial:
-  forall (b: block),
-  find_var_info (globalenv p') b = find_var_info (globalenv p) b.
+  forall (s : ident),
+  find_symbol (globalenv tp) s = find_symbol (globalenv p) s.
 Proof.
-  intros. case_eq (find_var_info (globalenv p) b); intros.
-  exploit find_var_info_transf_partial2. eexact transf_OK. eauto.
-  intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto.
-  case_eq (find_var_info (globalenv p') b); intros.
-  exploit find_var_info_rev_transf_partial2. eexact transf_OK. eauto.
-  intros [v' [P Q]]. monadInv Q. inv EQ. congruence.
-  auto.
+  intros. eapply (find_symbol_match progmatch). 
 Qed.
 
-Theorem block_is_volatile_transf_partial:
-  forall (b: block),
-  block_is_volatile (globalenv p') b = block_is_volatile (globalenv p) b.
+Theorem senv_transf_partial:
+  Senv.equiv (to_senv (globalenv p)) (to_senv (globalenv tp)).
 Proof.
-  exact (@block_is_volatile_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
+  intros. eapply (senv_match progmatch).
 Qed.
 
 Theorem init_mem_transf_partial:
-  forall m, init_mem p = Some m -> init_mem p' = Some m.
+  forall m, init_mem p = Some m -> init_mem tp = Some m.
 Proof.
-  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf_OK).
+  eapply (init_mem_match progmatch).
 Qed.
 
-End TRANSF_PROGRAM_PARTIAL.
+End TRANSFORM_PARTIAL.
 
-Section TRANSF_PROGRAM.
+(** Special case for total transformations that do not depend on the compilation unit *)
 
-Variable A B V: Type.
-Variable transf: A -> B.
-Variable p: program A V.
-Let tp := transform_program transf p.
+Section TRANSFORM_TOTAL.
 
-Remark transf_OK:
-  transform_partial_program (fun x => OK (transf x)) p = OK tp.
-Proof.
-  unfold tp. apply transform_program_partial_program.
-Qed.
+Context {A B V: Type} {LA: Linker A} {LV: Linker V}.
+Context {transf: A -> B} {p: program A V} {tp: program B V}.
+Hypothesis progmatch: match_program (fun cu f tf => tf = transf f) eq p tp.
 
 Theorem find_funct_ptr_transf:
-  forall (b: block) (f: A),
+  forall b f,
   find_funct_ptr (globalenv p) b = Some f ->
   find_funct_ptr (globalenv tp) b = Some (transf f).
 Proof.
-  intros.
-  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK _ _ H)
-  as [f' [X Y]]. congruence.
-Qed.
-
-Theorem find_funct_ptr_rev_transf:
-  forall (b: block) (tf: B),
-  find_funct_ptr (globalenv tp) b = Some tf ->
-  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf.
-Proof.
-  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
-  intros [f [X Y]]. exists f; split. auto. congruence.
+  intros. exploit (find_funct_ptr_match progmatch); eauto. 
+  intros (cu & tf & P & Q & R). congruence.
 Qed.
 
 Theorem find_funct_transf:
-  forall (v: val) (f: A),
+  forall v f,
   find_funct (globalenv p) v = Some f ->
   find_funct (globalenv tp) v = Some (transf f).
 Proof.
-  intros.
-  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK _ _ H)
-  as [f' [X Y]]. congruence.
-Qed.
-
-Theorem find_funct_rev_transf:
-  forall (v: val) (tf: B),
-  find_funct (globalenv tp) v = Some tf ->
-  exists f, find_funct (globalenv p) v = Some f /\ transf f = tf.
-Proof.
-  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
-  intros [f [X Y]]. exists f; split. auto. congruence.
+  intros. exploit (find_funct_match progmatch); eauto. 
+  intros (cu & tf & P & Q & R). congruence.
 Qed.
 
 Theorem find_symbol_transf:
-  forall (s: ident),
+  forall (s : ident),
   find_symbol (globalenv tp) s = find_symbol (globalenv p) s.
 Proof.
-  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
-Qed.
-
-Theorem public_symbol_transf:
-  forall (s: ident),
-  public_symbol (globalenv tp) s = public_symbol (globalenv p) s.
-Proof.
-  exact (@public_symbol_transf_partial _ _ _ _ _ _ transf_OK).
-Qed.
-
-Theorem find_var_info_transf:
-  forall (b: block),
-  find_var_info (globalenv tp) b = find_var_info (globalenv p) b.
-Proof.
-  exact (@find_var_info_transf_partial _ _ _ _ _ _ transf_OK).
+  intros. eapply (find_symbol_match progmatch).
 Qed.
 
-Theorem block_is_volatile_transf:
-  forall (b: block),
-  block_is_volatile (globalenv tp) b = block_is_volatile (globalenv p) b.
+Theorem senv_transf:
+  Senv.equiv (to_senv (globalenv p)) (to_senv (globalenv tp)).
 Proof.
-  exact (@block_is_volatile_transf_partial _ _ _ _ _ _ transf_OK).
+  intros. eapply (senv_match progmatch).
 Qed.
 
 Theorem init_mem_transf:
   forall m, init_mem p = Some m -> init_mem tp = Some m.
 Proof.
-  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
+  eapply (init_mem_match progmatch).
 Qed.
 
-End TRANSF_PROGRAM.
+End TRANSFORM_TOTAL.
 
 End Genv.
 
-- 
cgit