Merge pull request #93 from AbsInt/separate-compilation

This pull request implements "approach A" to separate compilation in CompCert from the paper

Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190

In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.

This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.

1 files changed, 729 insertions, 1146 deletions

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,34 +218,12 @@ 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.
   destruct (peq id1 i); destruct (peq id2 i).
   congruence.
@@ -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.