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.

8 files changed, 2164 insertions, 1964 deletions

diff --git a/common/AST.v b/common/AST.v
index 16673c47..415e90e2 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -17,10 +17,7 @@
   the abstract syntax trees of many of the intermediate languages. *)
 
 Require Import String.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Integers.
-Require Import Floats.
+Require Import Coqlib Maps Errors Integers Floats.
 
 Set Implicit Arguments.
 
@@ -106,6 +103,12 @@ Record calling_convention : Type := mkcallconv {
 Definition cc_default :=
   {| cc_vararg := false; cc_unproto := false; cc_structret := false |}.
 
+Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}.
+Proof.
+  decide equality; apply bool_dec. 
+Defined.
+Global Opaque calling_convention_eq.
+
 Record signature : Type := mksignature {
   sig_args: list typ;
   sig_res: option typ;
@@ -120,8 +123,7 @@ Definition proj_sig_res (s: signature) : typ :=
 
 Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}.
 Proof.
-  generalize opt_typ_eq, list_typ_eq; intros; decide equality.
-  generalize bool_dec; intros. decide equality.
+  generalize opt_typ_eq, list_typ_eq, calling_convention_eq; decide equality.
 Defined.
 Global Opaque signature_eq.
 
@@ -189,6 +191,36 @@ Inductive init_data: Type :=
   | Init_space: Z -> init_data
   | Init_addrof: ident -> int -> init_data.  (**r address of symbol + offset *)
 
+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.
+
+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.
+
+Lemma init_data_size_pos:
+  forall i, init_data_size i >= 0.
+Proof.
+  destruct i; simpl; xomega.
+Qed.
+
+Lemma 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.
+
 (** Information attached to global variables. *)
 
 Record globvar (V: Type) : Type := mkglobvar {
@@ -226,6 +258,49 @@ Record program (F V: Type) : Type := mkprogram {
 Definition prog_defs_names (F V: Type) (p: program F V) : list ident :=
   List.map fst p.(prog_defs).
 
+(** The "definition map" of a program maps names of globals to their definitions.
+  If several definitions have the same name, the one appearing last in [p.(prog_defs)] wins. *)
+
+Definition prog_defmap (F V: Type) (p: program F V) : PTree.t (globdef F V) :=
+  PTree_Properties.of_list p.(prog_defs).
+
+Section DEFMAP.
+
+Variables F V: Type.
+Variable p: program F V.
+
+Lemma in_prog_defmap:
+  forall id g, (prog_defmap p)!id = Some g -> In (id, g) (prog_defs p).
+Proof.
+  apply PTree_Properties.in_of_list.
+Qed.
+
+Lemma prog_defmap_dom:
+  forall id, In id (prog_defs_names p) -> exists g, (prog_defmap p)!id = Some g.
+Proof.
+  apply PTree_Properties.of_list_dom.
+Qed.
+
+Lemma prog_defmap_unique:
+  forall defs1 id g defs2,
+  prog_defs p = defs1 ++ (id, g) :: defs2 ->
+  ~In id (map fst defs2) ->
+  (prog_defmap p)!id = Some g.
+Proof.
+  unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto. 
+Qed.
+
+Lemma prog_defmap_norepet:
+  forall id g,
+  list_norepet (prog_defs_names p) ->
+  In (id, g) (prog_defs p) ->
+  (prog_defmap p)!id = Some g.
+Proof.
+  apply PTree_Properties.of_list_norepet.
+Qed.
+
+End DEFMAP.
+
 (** * Generic transformations over programs *)
 
 (** We now define a general iterator over programs that applies a given
@@ -249,109 +324,44 @@ Definition transform_program (p: program A V) : program B V :=
     p.(prog_public)
     p.(prog_main).
 
-Lemma transform_program_function:
-  forall p i tf,
-  In (i, Gfun tf) (transform_program p).(prog_defs) ->
-  exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf.
-Proof.
-  simpl. unfold transform_program. intros.
-  exploit list_in_map_inv; eauto.
-  intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ.
-  exists f; auto.
-Qed.
-
 End TRANSF_PROGRAM.
 
-(** General iterator over program that applies a given code transfomration
-    function to all function descriptions with their identifers and leaves
-    teh other parts of the program unchanged. *)
-
-Section TRANSF_PROGRAM_IDENT.
-
-Variable A B V: Type.
-Variable transf: ident -> A -> B.
-
-Definition transform_program_globdef_ident (idg: ident * globdef A V) : ident * globdef B V :=
-  match idg with
-  | (id, Gfun f) => (id, Gfun (transf id f))
-  | (id, Gvar v) => (id, Gvar v)
-  end.
-
-Definition transform_program_ident (p: program A V): program B V :=
-  mkprogram
-    (List.map transform_program_globdef_ident p.(prog_defs))
-    p.(prog_public)
-    p.(prog_main).
-
-Lemma tranforma_program_function_ident:
-  forall p i tf,
-  In (i, Gfun tf) (transform_program_ident p).(prog_defs) ->
-  exists f, In (i, Gfun f) p.(prog_defs) /\ transf i f = tf.
-Proof.
-  simpl. unfold transform_program_ident. intros.
-  exploit list_in_map_inv; eauto.
-  intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ.
-  exists f; auto.
-Qed.
-
-End TRANSF_PROGRAM_IDENT.
-
-(** The following is a more general presentation of [transform_program] where
-  global variable information can be transformed, in addition to function
-  definitions.  Moreover, the transformation functions can fail and
-  return an error message. Also the transformation functions are defined
-  for the case the identifier of the function is passed as additional
-  argument *)
+(** The following is a more general presentation of [transform_program]:
+- Global variable information can be transformed, in addition to function
+  definitions.
+- The transformation functions can fail and return an error message.
+- The transformation for function definitions receives a global context
+  (derived from the compilation unit being transformed) as additiona
+  argument.
+- The transformation functions receive the name of the global as
+  additional argument. *)
 
 Local Open Scope error_monad_scope.
 
 Section TRANSF_PROGRAM_GEN.
 
 Variables A B V W: Type.
-Variable transf_fun: A -> res B.
-Variable transf_fun_ident: ident -> A -> res B.
-Variable transf_var: V -> res W.
-Variable transf_var_ident: ident -> V -> res W.
+Variable transf_fun: ident -> A -> res B.
+Variable transf_var: ident -> V -> res W.
 
-Definition transf_globvar (g: globvar V) : res (globvar W) :=
-  do info' <- transf_var g.(gvar_info);
-  OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).
-
-Definition transf_globvar_ident (i: ident) (g: globvar V) : res (globvar W) :=
-  do info' <- transf_var_ident i g.(gvar_info);
+Definition transf_globvar (i: ident) (g: globvar V) : res (globvar W) :=
+  do info' <- transf_var i g.(gvar_info);
   OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).
 
 Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) :=
   match l with
   | nil => OK nil
   | (id, Gfun f) :: l' =>
-      match transf_fun f with
+    match transf_fun id f with
       | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
       | OK tf =>
-          do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl')
-      end
-  | (id, Gvar v) :: l' =>
-      match transf_globvar v with
-      | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg)
-      | OK tv =>
-          do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl')
-      end
-  end.
-
-Fixpoint transf_globdefs_ident (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) :=
-  match l with
-  | nil => OK nil
-  | (id, Gfun f) :: l' =>
-    match transf_fun_ident id f with
-      | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
-      | OK tf =>
-        do tl' <- transf_globdefs_ident l'; OK ((id, Gfun tf) :: tl')
+        do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl')
     end
   | (id, Gvar v) :: l' =>
-    match transf_globvar_ident id v with
+    match transf_globvar id v with
       | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg)
       | OK tv =>
-        do tl' <- transf_globdefs_ident l'; OK ((id, Gvar tv) :: tl')
+        do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl')
     end
   end.
 
@@ -359,213 +369,6 @@ Definition transform_partial_program2 (p: program A V) : res (program B W) :=
   do gl' <- transf_globdefs p.(prog_defs);
   OK (mkprogram gl' p.(prog_public) p.(prog_main)).
 
-Definition transform_partial_ident_program2 (p: program A V) : res (program B W) :=
-  do gl' <- transf_globdefs_ident p.(prog_defs);
-  OK (mkprogram gl' p.(prog_public) p.(prog_main)).
-
-Lemma transform_partial_program2_function:
-  forall p tp i tf,
-  transform_partial_program2 p = OK tp ->
-  In (i, Gfun tf) tp.(prog_defs) ->
-  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf.
-Proof.
-  intros. monadInv H. simpl in H0.
-  revert x EQ H0. induction (prog_defs p); simpl; intros.
-  inv EQ. contradiction.
-  destruct a as [id [f|v]].
-  destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H. exists f; auto.
-  exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
-  destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H.
-  exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
-Qed.
-
-Lemma transform_partial_ident_program2_function:
-  forall p tp i tf,
-  transform_partial_ident_program2 p = OK tp ->
-  In (i, Gfun tf) tp.(prog_defs) ->
-  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun_ident i f = OK tf.
-Proof.
-  intros. monadInv H. simpl in H0.
-  revert x EQ H0. induction (prog_defs p); simpl; intros.
-  inv EQ. contradiction.
-  destruct a as [id [f|v]].
-  destruct (transf_fun_ident id f) as [tf1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H. exists f; auto.
-  exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
-  destruct (transf_globvar_ident id v) as [tv1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H.
-  exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
-Qed.
-
-Lemma transform_partial_program2_variable:
-  forall p tp i tv,
-  transform_partial_program2 p = OK tp ->
-  In (i, Gvar tv) tp.(prog_defs) ->
-  exists v,
-     In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs)
-  /\ transf_var v = OK tv.(gvar_info).
-Proof.
-  intros. monadInv H. simpl in H0.
-  revert x EQ H0. induction (prog_defs p); simpl; intros.
-  inv EQ. contradiction.
-  destruct a as [id [f|v]].
-  destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H.
-  exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
-  destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H.
-  monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto.
-  exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
-Qed.
-
-
-Lemma transform_partial_ident_program2_variable:
-  forall p tp i tv,
-  transform_partial_ident_program2 p = OK tp ->
-  In (i, Gvar tv) tp.(prog_defs) ->
-  exists v,
-     In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs)
-  /\ transf_var_ident i v = OK tv.(gvar_info).
-Proof.
-  intros. monadInv H. simpl in H0.
-  revert x EQ H0. induction (prog_defs p); simpl; intros.
-  inv EQ. contradiction.
-  destruct a as [id [f|v]].
-  destruct (transf_fun_ident id f) as [tf1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H.
-  exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
-  destruct (transf_globvar_ident id v) as [tv1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H.
-  monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto.
-  exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
-Qed.
-
-Lemma transform_partial_program2_succeeds:
-  forall p tp i g,
-  transform_partial_program2 p = OK tp ->
-  In (i, g) p.(prog_defs) ->
-  match g with
-  | Gfun fd => exists tfd, transf_fun fd = OK tfd
-  | Gvar gv => exists tv, transf_var gv.(gvar_info) = OK tv
-  end.
-Proof.
-  intros. monadInv H.
-  revert x EQ H0. induction (prog_defs p); simpl; intros.
-  contradiction.
-  destruct a as [id1 g1]. destruct g1.
-  destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ.
-  destruct H0. inv H. econstructor; eauto. eapply IHl; eauto.
-  destruct (transf_globvar v) eqn:TV; try discriminate. monadInv EQ.
-  destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto.
-Qed.
-
-Lemma transform_partial_ident_program2_succeeds:
-  forall p tp i g,
-  transform_partial_ident_program2 p = OK tp ->
-  In (i, g) p.(prog_defs) ->
-  match g with
-  | Gfun fd => exists tfd, transf_fun_ident i fd = OK tfd
-  | Gvar gv => exists tv, transf_var_ident i gv.(gvar_info) = OK tv
-  end.
-Proof.
-  intros. monadInv H.
-  revert x EQ H0. induction (prog_defs p); simpl; intros.
-  contradiction.
-  destruct a as [id1 g1]. destruct g1.
-  destruct (transf_fun_ident id1 f) eqn:TF; try discriminate. monadInv EQ.
-  destruct H0. inv H. econstructor; eauto. eapply IHl; eauto.
-  destruct (transf_globvar_ident id1 v) eqn:TV; try discriminate. monadInv EQ.
-  destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto.
-Qed.
-
-Lemma transform_partial_program2_main:
-  forall p tp,
-  transform_partial_program2 p = OK tp ->
-  tp.(prog_main) = p.(prog_main).
-Proof.
-  intros. monadInv H. reflexivity.
-Qed.
-
-Lemma transform_partial_ident_program2_main:
-  forall p tp,
-  transform_partial_ident_program2 p = OK tp ->
-  tp.(prog_main) = p.(prog_main).
-Proof.
-  intros. monadInv H. reflexivity.
-Qed.
-
-Lemma transform_partial_program2_public:
-  forall p tp,
-  transform_partial_program2 p = OK tp ->
-  tp.(prog_public) = p.(prog_public).
-Proof.
-  intros. monadInv H. reflexivity.
-Qed.
-
-Lemma transform_partial_ident_program2_public:
-  forall p tp,
-  transform_partial_ident_program2 p = OK tp ->
-  tp.(prog_public) = p.(prog_public).
-Proof.
-  intros. monadInv H. reflexivity.
-Qed.
-
-(** Additionally, we can also "augment" the program with new global definitions
-  and a different "main" function. *)
-
-Section AUGMENT.
-
-Variable new_globs: list(ident * globdef B W).
-Variable new_main: ident.
-
-Definition transform_partial_augment_program (p: program A V) : res (program B W) :=
-  do gl' <- transf_globdefs p.(prog_defs);
-  OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main).
-
-Lemma transform_partial_augment_program_main:
-  forall p tp,
-  transform_partial_augment_program p = OK tp ->
-  tp.(prog_main) = new_main.
-Proof.
-  intros. monadInv H. reflexivity.
-Qed.
-
-Definition transform_partial_augment_ident_program (p: program A V) : res (program B W) :=
-  do gl' <- transf_globdefs_ident p.(prog_defs);
-  OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main).
-
-Lemma transform_partial_augment_ident_program_main:
-  forall p tp,
-  transform_partial_augment_ident_program p = OK tp ->
-  tp.(prog_main) = new_main.
-Proof.
-  intros. monadInv H. reflexivity.
-Qed.
-
-End AUGMENT.
-
-Remark transform_partial_program2_augment:
-  forall p,
-  transform_partial_program2 p =
-  transform_partial_augment_program nil p.(prog_main) p.
-Proof.
-  unfold transform_partial_program2, transform_partial_augment_program; intros.
-  destruct (transf_globdefs (prog_defs p)); auto.
-  simpl. f_equal. f_equal. rewrite <- app_nil_end. auto.
-Qed.
-
-Remark transform_partial_ident_program2_augment:
-  forall p,
-  transform_partial_ident_program2 p =
-  transform_partial_augment_ident_program nil p.(prog_main) p.
-Proof.
-  unfold transform_partial_ident_program2, transform_partial_augment_ident_program; intros.
-  destruct (transf_globdefs_ident (prog_defs p)); auto.
-  simpl. f_equal. f_equal. rewrite <- app_nil_end. auto.
-Qed.
-
 End TRANSF_PROGRAM_GEN.
 
 (** The following is a special case of [transform_partial_program2],
@@ -574,178 +377,26 @@ End TRANSF_PROGRAM_GEN.
 Section TRANSF_PARTIAL_PROGRAM.
 
 Variable A B V: Type.
-Variable transf_partial: A -> res B.
-Variable transf_partial_ident: ident -> A -> res B.
+Variable transf_fun: A -> res B.
 
 Definition transform_partial_program (p: program A V) : res (program B V) :=
-  transform_partial_program2 transf_partial (fun v => OK v) p.
-
-Definition transform_partial_ident_program (p: program A V) : res (program B V) :=
-  transform_partial_ident_program2 transf_partial_ident (fun _ v => OK v) p.
-
-Lemma transform_partial_program_main:
-  forall p tp,
-  transform_partial_program p = OK tp ->
-  tp.(prog_main) = p.(prog_main).
-Proof.
-  apply transform_partial_program2_main.
-Qed.
-
-Lemma transform_partial_ident_program_main:
-  forall p tp,
-  transform_partial_ident_program p = OK tp ->
-  tp.(prog_main) = p.(prog_main).
-Proof.
-  apply transform_partial_ident_program2_main.
-Qed.
-
-Lemma transform_partial_program_public:
-  forall p tp,
-  transform_partial_program p = OK tp ->
-  tp.(prog_public) = p.(prog_public).
-Proof.
-  apply transform_partial_program2_public.
-Qed.
-
-Lemma transform_partial_ident_program_public:
-  forall p tp,
-  transform_partial_ident_program p = OK tp ->
-  tp.(prog_public) = p.(prog_public).
-Proof.
-  apply transform_partial_ident_program2_public.
-Qed.
-
-Lemma transform_partial_program_function:
-  forall p tp i tf,
-  transform_partial_program p = OK tp ->
-  In (i, Gfun tf) tp.(prog_defs) ->
-  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf.
-Proof.
-  apply transform_partial_program2_function.
-Qed.
-
-Lemma transform_partial_ident_program_function:
-  forall p tp i tf,
-  transform_partial_ident_program p = OK tp ->
-  In (i, Gfun tf) tp.(prog_defs) ->
-  exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial_ident i f = OK tf.
-Proof.
-  apply transform_partial_ident_program2_function.
-Qed.
-
-Lemma transform_partial_program_succeeds:
-  forall p tp i fd,
-  transform_partial_program p = OK tp ->
-  In (i, Gfun fd) p.(prog_defs) ->
-  exists tfd, transf_partial fd = OK tfd.
-Proof.
-  unfold transform_partial_program; intros.
-  exploit transform_partial_program2_succeeds; eauto.
-Qed.
-
-Lemma transform_partial_ident_program_succeeds:
-  forall p tp i fd,
-  transform_partial_ident_program p = OK tp ->
-  In (i, Gfun fd) p.(prog_defs) ->
-  exists tfd, transf_partial_ident i fd = OK tfd.
-Proof.
-  unfold transform_partial_ident_program; intros.
-  exploit transform_partial_ident_program2_succeeds; eauto.
-Qed.
+  transform_partial_program2 (fun i f => transf_fun f) (fun i v => OK v) p.
 
 End TRANSF_PARTIAL_PROGRAM.
 
 Lemma transform_program_partial_program:
-  forall (A B V: Type) (transf: A -> B) (p: program A V),
-  transform_partial_program (fun f => OK(transf f)) p = OK(transform_program transf p).
-Proof.
-  intros.
-  unfold transform_partial_program, transform_partial_program2, transform_program; intros.
-  replace (transf_globdefs (fun f => OK (transf f)) (fun v => OK v) p.(prog_defs))
-     with (OK (map (transform_program_globdef transf) p.(prog_defs))).
-  auto.
-  induction (prog_defs p); simpl.
-  auto.
-  destruct a as [id [f|v]]; rewrite <- IHl.
-    auto.
-    destruct v; auto.
-Qed.
-
-Lemma transform_program_partial_ident_program:
-  forall (A B V: Type) (transf: ident -> A -> B) (p: program A V),
-  transform_partial_ident_program (fun id f => OK(transf id f)) p = OK(transform_program_ident transf p).
-Proof.
-  intros.
-  unfold transform_partial_ident_program, transform_partial_ident_program2, transform_program; intros.
-  replace (transf_globdefs_ident (fun id f => OK (transf id f)) (fun _  v => OK v) p.(prog_defs))
-     with (OK (map (transform_program_globdef_ident transf) p.(prog_defs))).
-  auto.
-  induction (prog_defs p); simpl.
-  auto.
-  destruct a as [id [f|v]]; rewrite <- IHl.
-    auto.
-    destruct v; auto.
-Qed.
-
-(** The following is a relational presentation of
-  [transform_partial_augment_preogram].  Given relations between function
-  definitions and between variable information, it defines a relation
-  between programs stating that the two programs have appropriately related
-  shapes (global names are preserved and possibly augmented, etc)
-  and that identically-named function definitions
-  and variable information are related. *)
-
-Section MATCH_PROGRAM.
-
-Variable A B V W: Type.
-Variable match_fundef: A -> B -> Prop.
-Variable match_varinfo: V -> W -> Prop.
-
-Inductive match_globdef: ident * globdef A V -> ident * globdef B W -> Prop :=
-  | match_glob_fun: forall id f1 f2,
-      match_fundef f1 f2 ->
-      match_globdef (id, Gfun f1) (id, Gfun f2)
-  | match_glob_var: forall id init ro vo info1 info2,
-      match_varinfo info1 info2 ->
-      match_globdef (id, Gvar (mkglobvar info1 init ro vo)) (id, Gvar (mkglobvar info2 init ro vo)).
-
-Definition match_program (new_globs : list (ident * globdef B W))
-                         (new_main : ident)
-                         (p1: program A V)  (p2: program B W) : Prop :=
-  (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\
-                 p2.(prog_defs) = tglob ++ new_globs) /\
-  p2.(prog_main) = new_main /\
-  p2.(prog_public) = p1.(prog_public).
-
-End MATCH_PROGRAM.
-
-Lemma transform_partial_augment_program_match:
-  forall (A B V W: Type)
-         (transf_fun: A -> res B)
-         (transf_var: V -> res W)
-         (p: program A V)
-         (new_globs : list (ident * globdef B W))
-         (new_main : ident)
-         (tp: program B W),
-  transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp ->
-  match_program
-    (fun fd tfd => transf_fun fd = OK tfd)
-    (fun info tinfo => transf_var info = OK tinfo)
-    new_globs new_main
-    p tp.
+  forall (A B V: Type) (transf_fun: A -> B) (p: program A V),
+  transform_partial_program (fun f => OK (transf_fun f)) p = OK (transform_program transf_fun p).
 Proof.
-  unfold transform_partial_augment_program; intros. monadInv H.
-  red; simpl. split; auto. exists x; split; auto.
-  revert x EQ. generalize (prog_defs p). induction l; simpl; intros.
-  monadInv EQ. constructor.
-  destruct a as [id [f|v]].
-  (* function *)
-  destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ.
-  constructor; auto. constructor; auto.
-  (* variable *)
-  unfold transf_globvar in EQ.
-  destruct (transf_var (gvar_info v)) as [tinfo|?] eqn:?; simpl in EQ; monadInv EQ.
-  constructor; auto. destruct v; simpl in *. constructor; auto.
+  intros. unfold transform_partial_program, transform_partial_program2.
+  assert (EQ: forall l,
+              transf_globdefs (fun i f => OK (transf_fun f)) (fun i (v: V) => OK v) l =
+              OK (List.map (transform_program_globdef transf_fun) l)).
+  { induction l as [ | [id g] l]; simpl.
+  - auto.
+  - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto. 
+  }
+  rewrite EQ; simpl. auto.
 Qed.
 
 (** * External functions *)
@@ -763,6 +414,9 @@ Inductive external_function : Type :=
   | EF_builtin (name: string) (sg: signature)
      (** A compiler built-in function.  Behaves like an external, but
          can be inlined by the compiler. *)
+  | EF_runtime (name: string) (sg: signature)
+     (** A function from the run-time library.  Behaves like an
+         external, but must not be redefined. *)
   | EF_vload (chunk: memory_chunk)
      (** A volatile read operation.  If the adress given as first argument
          points within a volatile global variable, generate an
@@ -808,6 +462,7 @@ Definition ef_sig (ef: external_function): signature :=
   match ef with
   | EF_external name sg => sg
   | EF_builtin name sg => sg
+  | EF_runtime name sg => sg
   | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default
   | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default
   | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default
@@ -825,6 +480,7 @@ Definition ef_inline (ef: external_function) : bool :=
   match ef with
   | EF_external name sg => false
   | EF_builtin name sg => true
+  | EF_runtime name sg => false
   | EF_vload chunk => true
   | EF_vstore chunk => true
   | EF_malloc => false
diff --git a/common/Behaviors.v b/common/Behaviors.v
index 1a6b8bd6..ef99b205 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -281,31 +281,29 @@ End PROGRAM_BEHAVIORS.
 
 Section FORWARD_SIMULATIONS.
 
-Variable L1: semantics.
-Variable L2: semantics.
-Variable S: forward_simulation L1 L2.
+Context L1 L2 index order match_states (S: fsim_properties L1 L2 index order match_states).
 
 Lemma forward_simulation_state_behaves:
   forall i s1 s2 beh1,
-  S i s1 s2 -> state_behaves L1 s1 beh1 ->
+  match_states i s1 s2 -> state_behaves L1 s1 beh1 ->
   exists beh2, state_behaves L2 s2 beh2 /\ behavior_improves beh1 beh2.
 Proof.
   intros. inv H0.
-(* termination *)
+- (* termination *)
   exploit simulation_star; eauto. intros [i' [s2' [A B]]].
   exists (Terminates t r); split.
   econstructor; eauto. eapply fsim_match_final_states; eauto.
   apply behavior_improves_refl.
-(* silent divergence *)
+- (* silent divergence *)
   exploit simulation_star; eauto. intros [i' [s2' [A B]]].
   exists (Diverges t); split.
   econstructor; eauto. eapply simulation_forever_silent; eauto.
   apply behavior_improves_refl.
-(* reactive divergence *)
+- (* reactive divergence *)
   exists (Reacts T); split.
   econstructor. eapply simulation_forever_reactive; eauto.
   apply behavior_improves_refl.
-(* going wrong *)
+- (* going wrong *)
   exploit simulation_star; eauto. intros [i' [s2' [A B]]].
   destruct (state_behaves_exists L2 s2') as [beh' SB].
   exists (behavior_app t beh'); split.
@@ -315,16 +313,19 @@ Proof.
   simpl. decEq. traceEq.
 Qed.
 
+End FORWARD_SIMULATIONS.
+
 Theorem forward_simulation_behavior_improves:
+  forall L1 L2, forward_simulation L1 L2 ->
   forall beh1, program_behaves L1 beh1 ->
   exists beh2, program_behaves L2 beh2 /\ behavior_improves beh1 beh2.
 Proof.
-  intros. inv H.
-(* initial state defined *)
+  intros L1 L2 FS. destruct FS as [init order match_states S]. intros. inv H.
+- (* initial state defined *)
   exploit (fsim_match_initial_states S); eauto. intros [i [s' [INIT MATCH]]].
   exploit forward_simulation_state_behaves; eauto. intros [beh2 [A B]].
   exists beh2; split; auto. econstructor; eauto.
-(* initial state undefined *)
+- (* initial state undefined *)
   destruct (classic (exists s', initial_state L2 s')).
   destruct H as [s' INIT].
   destruct (state_behaves_exists L2 s') as [beh' SB].
@@ -336,6 +337,7 @@ Proof.
 Qed.
 
 Corollary forward_simulation_same_safe_behavior:
+  forall L1 L2, forward_simulation L1 L2 ->
   forall beh,
   program_behaves L1 beh -> not_wrong beh ->
   program_behaves L2 beh.
@@ -343,18 +345,14 @@ Proof.
   intros. exploit forward_simulation_behavior_improves; eauto.
   intros [beh' [A B]]. destruct B.
   congruence.
-  destruct H1 as [t [C D]]. subst. contradiction.
+  destruct H2 as [t [C D]]. subst. contradiction.
 Qed.
 
-End FORWARD_SIMULATIONS.
-
 (** * Backward simulations and program behaviors *)
 
 Section BACKWARD_SIMULATIONS.
 
-Variable L1: semantics.
-Variable L2: semantics.
-Variable S: backward_simulation L1 L2.
+Context L1 L2 index order match_states (S: bsim_properties L1 L2 index order match_states).
 
 Definition safe_along_behavior (s: state L1) (b: program_behavior) : Prop :=
   forall t1 s' b2, Star L1 s t1 s' -> b = behavior_app t1 b2 ->
@@ -402,8 +400,8 @@ Qed.
 
 Lemma backward_simulation_star:
   forall s2 t s2', Star L2 s2 t s2' ->
-  forall i s1 b, S i s1 s2 -> safe_along_behavior s1 (behavior_app t b) ->
-  exists i', exists s1', Star L1 s1 t s1' /\ S i' s1' s2'.
+  forall i s1 b, match_states i s1 s2 -> safe_along_behavior s1 (behavior_app t b) ->
+  exists i', exists s1', Star L1 s1 t s1' /\ match_states i' s1' s2'.
 Proof.
   induction 1; intros.
   exists i; exists s1; split; auto. apply star_refl.
@@ -418,12 +416,12 @@ Qed.
 
 Lemma backward_simulation_forever_silent:
   forall i s1 s2,
-  Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 ->
+  Forever_silent L2 s2 -> match_states i s1 s2 -> safe L1 s1 ->
   Forever_silent L1 s1.
 Proof.
   assert (forall i s1 s2,
-         Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 ->
-         forever_silent_N (step L1) (bsim_order S) (globalenv L1) i s1).
+         Forever_silent L2 s2 -> match_states i s1 s2 -> safe L1 s1 ->
+         forever_silent_N (step L1) order (globalenv L1) i s1).
     cofix COINDHYP; intros.
     inv H.  destruct (bsim_simulation S _ _ _ H2 _ H0 H1) as [i' [s2' [A B]]].
     destruct A as [C | [C D]].
@@ -431,29 +429,29 @@ Proof.
       eapply star_safe; eauto. apply plus_star; auto.
     eapply forever_silent_N_star; eauto. eapply COINDHYP; eauto.
       eapply star_safe; eauto.
-  intros. eapply forever_silent_N_forever; eauto. apply bsim_order_wf.
+  intros. eapply forever_silent_N_forever; eauto. eapply bsim_order_wf; eauto.
 Qed.
 
 Lemma backward_simulation_forever_reactive:
   forall i s1 s2 T,
-  Forever_reactive L2 s2 T -> S i s1 s2 -> safe_along_behavior s1 (Reacts T) ->
+  Forever_reactive L2 s2 T -> match_states i s1 s2 -> safe_along_behavior s1 (Reacts T) ->
   Forever_reactive L1 s1 T.
 Proof.
   cofix COINDHYP; intros. inv H.
-  destruct (backward_simulation_star H2 _ (Reacts T0) H0) as [i' [s1' [A B]]]; eauto.
+  destruct (backward_simulation_star H2 (Reacts T0) H0) as [i' [s1' [A B]]]; eauto.
   econstructor; eauto. eapply COINDHYP; eauto. eapply star_safe_along; eauto.
 Qed.
 
 Lemma backward_simulation_state_behaves:
   forall i s1 s2 beh2,
-  S i s1 s2 -> state_behaves L2 s2 beh2 ->
+  match_states i s1 s2 -> state_behaves L2 s2 beh2 ->
   exists beh1, state_behaves L1 s1 beh1 /\ behavior_improves beh1 beh2.
 Proof.
   intros. destruct (classic (safe_along_behavior s1 beh2)).
-(* 1. Safe along *)
+- (* 1. Safe along *)
   exists beh2; split; [idtac|apply behavior_improves_refl].
   inv H0.
-(* termination *)
++ (* termination *)
   assert (Terminates t r = behavior_app t (Terminates E0 r)).
     simpl. rewrite E0_right; auto.
   rewrite H0 in H1.
@@ -463,7 +461,7 @@ Proof.
     eapply safe_along_safe. eapply star_safe_along; eauto.
   intros [s1'' [C D]].
   econstructor. eapply star_trans; eauto. traceEq. auto.
-(* silent divergence *)
++ (* silent divergence *)
   assert (Diverges t = behavior_app t (Diverges E0)).
     simpl. rewrite E0_right; auto.
   rewrite H0 in H1.
@@ -471,9 +469,9 @@ Proof.
   intros [i' [s1' [A B]]].
   econstructor. eauto. eapply backward_simulation_forever_silent; eauto.
   eapply safe_along_safe. eapply star_safe_along; eauto.
-(* reactive divergence *)
++ (* reactive divergence *)
   econstructor. eapply backward_simulation_forever_reactive; eauto.
-(* goes wrong *)
++ (* goes wrong *)
   assert (Goes_wrong t = behavior_app t (Goes_wrong E0)).
     simpl. rewrite E0_right; auto.
   rewrite H0 in H1.
@@ -484,7 +482,7 @@ Proof.
   elim (H4 _ FIN).
   elim (H3 _ _ STEP2).
 
-(* 2. Not safe along *)
+- (* 2. Not safe along *)
   exploit not_safe_along_behavior; eauto.
   intros [t [s1' [PREF [STEPS [NOSTEP NOFIN]]]]].
   exists (Goes_wrong t); split.
@@ -492,23 +490,26 @@ Proof.
   right. exists t; auto.
 Qed.
 
+End BACKWARD_SIMULATIONS.
+
 Theorem backward_simulation_behavior_improves:
+  forall L1 L2, backward_simulation L1 L2 ->
   forall beh2, program_behaves L2 beh2 ->
   exists beh1, program_behaves L1 beh1 /\ behavior_improves beh1 beh2.
 Proof.
-  intros. inv H.
-(* L2's initial state is defined. *)
+  intros L1 L2 S beh2 H. destruct S as [index order match_states S]. inv H.
+- (* L2's initial state is defined. *)
   destruct (classic (exists s1, initial_state L1 s1)) as [[s1 INIT] | NOINIT].
-(* L1's initial state is defined too. *)
++ (* L1's initial state is defined too. *)
   exploit (bsim_match_initial_states S); eauto. intros [i [s1' [INIT1' MATCH]]].
   exploit backward_simulation_state_behaves; eauto. intros [beh1 [A B]].
   exists beh1; split; auto. econstructor; eauto.
-(* L1 has no initial state *)
++ (* L1 has no initial state *)
   exists (Goes_wrong E0); split.
   apply program_goes_initially_wrong.
   intros; red; intros. elim NOINIT; exists s0; auto.
   apply behavior_improves_bot.
-(* L2 has no initial state *)
+- (* L2 has no initial state *)
   exists (Goes_wrong E0); split.
   apply program_goes_initially_wrong.
   intros; red; intros.
@@ -518,17 +519,16 @@ Proof.
 Qed.
 
 Corollary backward_simulation_same_safe_behavior:
+  forall L1 L2, backward_simulation L1 L2 ->
   (forall beh, program_behaves L1 beh -> not_wrong beh) ->
   (forall beh, program_behaves L2 beh -> program_behaves L1 beh).
 Proof.
   intros. exploit backward_simulation_behavior_improves; eauto.
   intros [beh' [A B]]. destruct B.
   congruence.
-  destruct H1 as [t [C D]]. subst. elim (H (Goes_wrong t)). auto.
+  destruct H2 as [t [C D]]. subst. elim (H0 (Goes_wrong t)). auto.
 Qed.
 
-End BACKWARD_SIMULATIONS.
-
 (** * Program behaviors for the "atomic" construction *)
 
 Section ATOMIC.
@@ -635,7 +635,7 @@ Theorem atomic_behaviors:
   forall beh, program_behaves L beh <-> program_behaves (atomic L) beh.
 Proof.
   intros; split; intros.
-  (* L -> atomic L *)
+- (* L -> atomic L *)
   exploit forward_simulation_behavior_improves. eapply atomic_forward_simulation. eauto.
   intros [beh2 [A B]]. red in B. destruct B as [EQ | [t [C D]]].
   congruence.
@@ -646,23 +646,23 @@ Proof.
   intros; red; intros. simpl in H. destruct H. eelim H4; eauto.
   apply program_goes_initially_wrong.
   intros; red; intros. simpl in H; destruct H. eelim H1; eauto.
-  (* atomic L -> L *)
+- (* atomic L -> L *)
   inv H.
-  (* initial state defined *)
++ (* initial state defined *)
   destruct s as [t s]. simpl in H0. destruct H0; subst t.
   apply program_runs with s; auto.
   inv H1.
-  (* termination *)
+* (* termination *)
   destruct s' as [t' s']. simpl in H2; destruct H2; subst t'.
   econstructor. eapply atomic_star_star; eauto. auto.
-  (* silent divergence *)
+* (* silent divergence *)
   destruct s' as [t' s'].
   assert (t' = E0). inv H2. inv H1; auto. subst t'.
   econstructor. eapply atomic_star_star; eauto.
   change s' with (snd (E0,s')). apply atomic_forever_silent_forever_silent. auto.
-  (* reactive divergence *)
+* (* reactive divergence *)
   econstructor. apply atomic_forever_reactive_forever_reactive. auto.
-  (* going wrong *)
+* (* going wrong *)
   destruct s' as [t' s'].
   assert (t' = E0).
     destruct t'; auto. eelim H2. simpl. apply atomic_step_continue.
@@ -672,7 +672,7 @@ Proof.
   elim (H2 E0 (E0,s'0)). constructor; auto.
   elim (H2 (e::nil) (t0,s'0)). constructor; auto.
   intros; red; intros. elim (H3 r). simpl; auto.
-  (* initial state undefined *)
++ (* initial state undefined *)
   apply program_goes_initially_wrong.
   intros; red; intros. elim (H0 (E0,s)); simpl; auto.
 Qed.
diff --git a/common/Events.v b/common/Events.v
index 7029a984..040029fb 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -619,9 +619,7 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop :=
 (** The semantics is invariant under change of global environment that preserves symbols. *)
   ec_symbols_preserved:
     forall ge1 ge2 vargs m1 t vres m2,
-    (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) ->
-    (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) ->
-    (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) ->
+    Senv.equiv ge1 ge2 ->
     sem ge1 vargs m1 t vres m2 ->
     sem ge2 vargs m1 t vres m2;
 
@@ -704,17 +702,15 @@ Inductive volatile_load_sem (chunk: memory_chunk) (ge: Senv.t):
 
 Lemma volatile_load_preserved:
   forall ge1 ge2 chunk m b ofs t v,
-  (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) ->
-  (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) ->
-  (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) ->
+  Senv.equiv ge1 ge2 ->
   volatile_load ge1 chunk m b ofs t v ->
   volatile_load ge2 chunk m b ofs t v.
 Proof.
-  intros. inv H2; constructor; auto.
-  rewrite H1; auto.
-  rewrite H; auto.
+  intros. destruct H as (A & B & C). inv H0; constructor; auto.
+  rewrite C; auto.
+  rewrite A; auto.
   eapply eventval_match_preserved; eauto.
-  rewrite H1; auto.
+  rewrite C; auto.
 Qed.
 
 Lemma volatile_load_extends:
@@ -773,7 +769,7 @@ Proof.
 - unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type.
   eapply Mem.load_type; eauto.
 (* symbols *)
-- inv H2. constructor. eapply volatile_load_preserved; eauto.
+- inv H0. constructor. eapply volatile_load_preserved; eauto.
 (* valid blocks *)
 - inv H; auto.
 (* max perms *)
@@ -817,17 +813,15 @@ Inductive volatile_store_sem (chunk: memory_chunk) (ge: Senv.t):
 
 Lemma volatile_store_preserved:
   forall ge1 ge2 chunk m1 b ofs v t m2,
-  (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) ->
-  (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) ->
-  (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) ->
+  Senv.equiv ge1 ge2 ->
   volatile_store ge1 chunk m1 b ofs v t m2 ->
   volatile_store ge2 chunk m1 b ofs v t m2.
 Proof.
-  intros. inv H2; constructor; auto.
-  rewrite H1; auto.
-  rewrite H; auto.
+  intros. destruct H as (A & B & C). inv H0; constructor; auto.
+  rewrite C; auto.
+  rewrite A; auto.
   eapply eventval_match_preserved; eauto.
-  rewrite H1; auto.
+  rewrite C; auto.
 Qed.
 
 Lemma volatile_store_readonly:
@@ -925,7 +919,7 @@ Proof.
 (* well typed *)
 - unfold proj_sig_res; simpl. inv H; constructor.
 (* symbols preserved *)
-- inv H2. constructor. eapply volatile_store_preserved; eauto.
+- inv H0. constructor. eapply volatile_store_preserved; eauto.
 (* valid block *)
 - inv H. inv H1. auto. eauto with mem.
 (* perms *)
@@ -972,19 +966,18 @@ Proof.
     Mem.store Mint32 m' b (-4) (Vint n) = Some m'' ->
     Mem.unchanged_on P m m'').
   {
-    intros; constructor; intros.
-  - split; intros; eauto with mem.
-  - assert (b0 <> b) by (eapply Mem.valid_not_valid_diff; eauto with mem).
-    erewrite Mem.store_mem_contents; eauto. rewrite Maps.PMap.gso by auto.
-    Local Transparent Mem.alloc. unfold Mem.alloc in H. injection H; intros A B.
-    rewrite <- B; simpl. rewrite A. rewrite Maps.PMap.gso by auto. auto.
+    intros.
+    apply Mem.unchanged_on_implies with (fun b1 ofs1 => b1 <> b).
+    apply Mem.unchanged_on_trans with m'. 
+    eapply Mem.alloc_unchanged_on; eauto.
+    eapply Mem.store_unchanged_on; eauto.
+    intros. eapply Mem.valid_not_valid_diff; eauto with mem.
   }
-
   constructor; intros.
 (* well typed *)
 - inv H. unfold proj_sig_res; simpl. auto.
 (* symbols preserved *)
-- inv H2; econstructor; eauto.
+- inv H0; econstructor; eauto.
 (* valid block *)
 - inv H. eauto with mem.
 (* perms *)
@@ -1045,7 +1038,7 @@ Proof.
 (* well typed *)
 - inv H. unfold proj_sig_res. simpl. auto.
 (* symbols preserved *)
-- inv H2; econstructor; eauto.
+- inv H0; econstructor; eauto.
 (* valid block *)
 - inv H. eauto with mem.
 (* perms *)
@@ -1124,7 +1117,7 @@ Proof.
 - (* return type *)
   intros. inv H. constructor.
 - (* change of globalenv *)
-  intros. inv H2. econstructor; eauto.
+  intros. inv H0. econstructor; eauto.
 - (* valid blocks *)
   intros. inv H. eauto with mem.
 - (* perms *)
@@ -1235,7 +1228,7 @@ Proof.
 (* well typed *)
 - inv H. simpl. auto.
 (* symbols *)
-- inv H2. econstructor; eauto.
+- destruct H as (A & B & C). inv H0. econstructor; eauto.
   eapply eventval_list_match_preserved; eauto.
 (* valid blocks *)
 - inv H; auto.
@@ -1280,7 +1273,7 @@ Proof.
 (* well typed *)
 - inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto.
 (* symbols *)
-- inv H2. econstructor; eauto.
+- destruct H as (A & B & C). inv H0. econstructor; eauto.
   eapply eventval_match_preserved; eauto.
 (* valid blocks *)
 - inv H; auto.
@@ -1324,7 +1317,7 @@ Proof.
 (* well typed *)
 - inv H. simpl. auto.
 (* symbols *)
-- inv H2. econstructor; eauto.
+- inv H0. econstructor; eauto.
 (* valid blocks *)
 - inv H; auto.
 (* perms *)
@@ -1351,8 +1344,9 @@ Qed.
 
 (** ** Semantics of external functions. *)
 
-(** For functions defined outside the program ([EF_external] and [EF_builtin]),
-  we do not define their semantics, but only assume that it satisfies
+(** For functions defined outside the program ([EF_external],
+  [EF_builtin] and [EF_runtime]), we do not define their
+  semantics, but only assume that it satisfies
   [extcall_properties]. *)
 
 Parameter external_functions_sem: String.string -> signature -> extcall_sem.
@@ -1384,6 +1378,7 @@ Definition external_call (ef: external_function): extcall_sem :=
   match ef with
   | EF_external name sg  => external_functions_sem name sg
   | EF_builtin name sg   => external_functions_sem name sg
+  | EF_runtime name sg   => external_functions_sem name sg
   | EF_vload chunk       => volatile_load_sem chunk
   | EF_vstore chunk      => volatile_store_sem chunk
   | EF_malloc            => extcall_malloc_sem
@@ -1402,6 +1397,7 @@ Proof.
   intros. unfold external_call, ef_sig; destruct ef.
   apply external_functions_properties.
   apply external_functions_properties.
+  apply external_functions_properties.
   apply volatile_load_ok.
   apply volatile_store_ok.
   apply extcall_malloc_ok.
@@ -1414,7 +1410,7 @@ Proof.
 Qed.
 
 Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef).
-Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef).
+Definition external_call_symbols_preserved ef := ec_symbols_preserved (external_call_spec ef).
 Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef).
 Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef).
 Definition external_call_readonly ef := ec_readonly (external_call_spec ef).
@@ -1424,20 +1420,6 @@ Definition external_call_trace_length ef := ec_trace_length (external_call_spec
 Definition external_call_receptive ef := ec_receptive (external_call_spec ef).
 Definition external_call_determ ef := ec_determ (external_call_spec ef).
 
-(** Special cases of [external_call_symbols_preserved_gen]. *)
-
-Lemma external_call_symbols_preserved:
-  forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
-  external_call ef ge1 vargs m1 t vres m2 ->
-  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
-  (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) ->
-  (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) ->
-  external_call ef ge2 vargs m1 t vres m2.
-Proof.
-  intros. apply external_call_symbols_preserved_gen with (ge1 := ge1); auto.
-  intros. simpl. unfold Genv.block_is_volatile. rewrite H2. auto.
-Qed.
-
 (** Corollary of [external_call_valid_block]. *)
 
 Lemma external_call_nextblock:
@@ -1596,9 +1578,7 @@ Qed.
 Lemma external_call_symbols_preserved':
   forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
   external_call' ef ge1 vargs m1 t vres m2 ->
-  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
-  (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) ->
-  (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) ->
+  Senv.equiv ge1 ge2 ->
   external_call' ef ge2 vargs m1 t vres m2.
 Proof.
   intros. inv H. exists v; auto. eapply external_call_symbols_preserved; eauto.
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.
 
diff --git a/common/Linking.v b/common/Linking.v
new file mode 100644
index 00000000..52e774db
--- /dev/null
+++ b/common/Linking.v
@@ -0,0 +1,905 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Separate compilation and syntactic linking *)
+
+Require Import Coqlib Maps Errors AST.
+
+(** This file follows "approach A" from the paper
+       "Lightweight Verification of Separate Compilation"
+    by Kang, Kim, Hur, Dreyer and Vafeiadis, POPL 2016. *)
+
+
+(** * Syntactic linking *)
+
+(** A syntactic element [A] supports syntactic linking if it is equipped with the following:
+- a partial binary operator [link] that produces the result of linking two elements,
+  or fails if they cannot be linked (e.g. two definitions that are incompatible);
+- a preorder [linkorder] with the meaning that [linkorder a1 a2] holds
+  if [a2] can be obtained by linking [a1] with some other syntactic element.
+*)
+
+Class Linker (A: Type) := {
+  link: A -> A -> option A;
+  linkorder: A -> A -> Prop;
+  linkorder_refl: forall x, linkorder x x;
+  linkorder_trans: forall x y z, linkorder x y -> linkorder y z -> linkorder x z;
+  link_linkorder: forall x y z, link x y = Some z -> linkorder x z /\ linkorder y z
+}.
+
+(** Linking function definitions.  External functions of the [EF_external]
+  kind can link with internal function definitions; the result of
+  linking is the internal definition.  Two external functions can link
+  if they are identical. *)
+
+Definition link_fundef {F: Type} (fd1 fd2: fundef F) :=
+  match fd1, fd2 with
+  | Internal _, Internal _ => None
+  | External ef1, External ef2 =>
+      if external_function_eq ef1 ef2 then Some (External ef1) else None
+  | Internal f, External ef =>
+      match ef with EF_external id sg => Some (Internal f) | _ => None end
+  | External ef, Internal f =>
+      match ef with EF_external id sg => Some (Internal f) | _ => None end
+  end.
+
+Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
+  | linkorder_fundef_refl: forall fd, linkorder_fundef fd fd
+  | linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f).
+
+Instance Linker_fundef (F: Type): Linker (fundef F) := {
+  link := link_fundef;
+  linkorder := linkorder_fundef
+}.
+Proof.
+- intros; constructor.
+- intros. inv H; inv H0; constructor.
+- intros x y z EQ. destruct x, y; simpl in EQ.
++ discriminate.
++ destruct e; inv EQ. split; constructor.
++ destruct e; inv EQ. split; constructor.
++ destruct (external_function_eq e e0); inv EQ. split; constructor.
+Defined.
+
+Global Opaque Linker_fundef.
+
+(** Linking variable initializers.  We adopt the following conventions:
+- an "extern" variable has an empty initialization list;
+- a "common" variable has an initialization list of the form [Init_space sz];
+- all other initialization lists correspond to fully defined variables, neither "common" nor "extern".
+*)
+
+Inductive init_class : list init_data -> Type :=
+  | Init_extern: init_class nil
+  | Init_common: forall sz, init_class (Init_space sz :: nil)
+  | Init_definitive: forall il, init_class il.
+
+Definition classify_init (i: list init_data) : init_class i :=
+  match i with
+  | nil => Init_extern
+  | Init_space sz :: nil => Init_common sz
+  | i => Init_definitive i
+  end.
+
+Definition link_varinit (i1 i2: list init_data) :=
+  match classify_init i1, classify_init i2 with
+  | Init_extern, _ => Some i2
+  | _, Init_extern => Some i1
+  | Init_common sz1, _ => if zeq sz1 (init_data_list_size i2) then Some i2 else None
+  | _, Init_common sz2 => if zeq sz2 (init_data_list_size i1) then Some i1 else None
+  | _, _ => None
+  end.
+
+Inductive linkorder_varinit: list init_data -> list init_data -> Prop :=
+  | linkorder_varinit_refl: forall il, linkorder_varinit il il
+  | linkorder_varinit_extern: forall il, linkorder_varinit nil il
+  | linkorder_varinit_common: forall sz il,
+      il <> nil -> init_data_list_size il = sz ->
+      linkorder_varinit (Init_space sz :: nil) il.
+
+Instance Linker_varinit : Linker (list init_data) := {
+  link := link_varinit;
+  linkorder := linkorder_varinit    
+}.
+Proof.
+- intros. constructor.
+- intros. inv H; inv H0; constructor; auto.
+  congruence.
+  simpl. generalize (init_data_list_size_pos z). xomega. 
+- unfold link_varinit; intros until z.
+  destruct (classify_init x) eqn:Cx, (classify_init y) eqn:Cy; intros E; inv E; try (split; constructor; fail).
++ destruct (zeq sz (Z.max sz0 0 + 0)); inv H0.
+  split; constructor. congruence. auto.
++ destruct (zeq sz (init_data_list_size il)); inv H0.
+  split; constructor. red; intros; subst z; discriminate. auto.
++ destruct (zeq sz (init_data_list_size il)); inv H0.
+  split; constructor. red; intros; subst z; discriminate. auto.
+Defined.
+
+Global Opaque Linker_varinit.
+
+(** Linking variable definitions. *)
+
+Definition link_vardef {V: Type} {LV: Linker V} (v1 v2: globvar V) :=
+  match link v1.(gvar_info) v2.(gvar_info) with
+  | None => None
+  | Some info =>
+      match link v1.(gvar_init) v2.(gvar_init) with
+      | None => None
+      | Some init =>
+          if eqb v1.(gvar_readonly) v2.(gvar_readonly)
+          && eqb v1.(gvar_volatile) v2.(gvar_volatile)
+          then Some {| gvar_info := info; gvar_init := init;
+                       gvar_readonly := v1.(gvar_readonly);
+                       gvar_volatile := v1.(gvar_volatile) |}
+          else None
+      end
+  end.
+
+Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> Prop :=
+  | linkorder_vardef_intro: forall info1 info2 i1 i2 ro vo,
+      linkorder info1 info2 ->
+      linkorder i1 i2 ->
+      linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo).
+
+Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
+  link := link_vardef;
+  linkorder := linkorder_vardef
+}.
+Proof.
+- intros. destruct x; constructor; apply linkorder_refl. 
+- intros. inv H; inv H0. constructor; eapply linkorder_trans; eauto.
+- unfold link_vardef; intros until z.
+  destruct x as [f1 i1 r1 v1], y as [f2 i2 r2 v2]; simpl.
+  destruct (link f1 f2) as [f|] eqn:LF; try discriminate.
+  destruct (link i1 i2) as [i|] eqn:LI; try discriminate.
+  destruct (eqb r1 r2) eqn:ER; try discriminate.
+  destruct (eqb v1 v2) eqn:EV; intros EQ; inv EQ.
+  apply eqb_prop in ER; apply eqb_prop in EV; subst r2 v2.
+  apply link_linkorder in LF. apply link_linkorder in LI.
+  split; constructor; tauto.
+Defined.
+
+Global Opaque Linker_vardef.
+
+(** A trivial linker for the trivial var info [unit]. *)
+
+Instance Linker_unit: Linker unit := {
+  link := fun x y => Some tt;
+  linkorder := fun x y => True
+}.
+Proof.
+- auto.
+- auto.
+- auto.
+Defined.
+
+Global Opaque Linker_unit.
+
+(** Linking global definitions *)
+
+Definition link_def {F V: Type} {LF: Linker F} {LV: Linker V} (gd1 gd2: globdef F V) :=
+  match gd1, gd2 with
+  | Gfun f1, Gfun f2 =>
+      match link f1 f2 with Some f => Some (Gfun f) | None => None end
+  | Gvar v1, Gvar v2 =>
+      match link v1 v2 with Some v => Some (Gvar v) | None => None end
+  | _, _ => None
+  end.
+
+Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V -> globdef F V -> Prop :=
+  | linkorder_def_fun: forall fd1 fd2,
+      linkorder fd1 fd2 ->
+      linkorder_def (Gfun fd1) (Gfun fd2)
+  | linkorder_def_var: forall v1 v2,
+      linkorder v1 v2 ->
+      linkorder_def (Gvar v1) (Gvar v2).
+
+Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := {
+  link := link_def;
+  linkorder := linkorder_def
+}.
+Proof.
+- intros. destruct x; constructor; apply linkorder_refl.
+- intros. inv H; inv H0; constructor; eapply linkorder_trans; eauto.
+- unfold link_def; intros.  
+  destruct x as [f1|v1], y as [f2|v2]; try discriminate.
++ destruct (link f1 f2) as [f|] eqn:L; inv H. apply link_linkorder in L.
+  split; constructor; tauto.
++ destruct (link v1 v2) as [v|] eqn:L; inv H. apply link_linkorder in L.
+  split; constructor; tauto.
+Defined.
+
+Global Opaque Linker_def.
+
+(** Linking two compilation units.  Compilation units are represented like
+  whole programs using the type [program F V].  If a name has
+  a global definition in one unit but not in the other, this definition
+  is left unchanged in the result of the link.  If a name has
+  global definitions in both units, and is public (not static) in both,
+  the two definitions are linked as per [Linker_def] above.  
+
+  If one or both definitions are static (not public), we should ideally
+  rename it so that it can be kept unchanged in the result of the link.
+  This would require a general notion of renaming of global identifiers
+  in programs that we do not have yet.  Hence, as a first step, linking
+  is undefined if static definitions with the same name appear in both
+  compilation units. *)
+
+Section LINKER_PROG.
+
+Context {F V: Type} {LF: Linker F} {LV: Linker V} (p1 p2: program F V).
+
+Let dm1 := prog_defmap p1.
+Let dm2 := prog_defmap p2.
+
+Definition link_prog_check (x: ident) (gd1: globdef F V) :=
+  match dm2!x with
+  | None => true
+  | Some gd2 =>
+      In_dec peq x p1.(prog_public)
+      && In_dec peq x p2.(prog_public)
+      && match link gd1 gd2 with Some _ => true | None => false end
+  end.
+
+Definition link_prog_merge (o1 o2: option (globdef F V)) :=
+  match o1, o2 with
+  | None, _ => o2
+  | _, None => o1
+  | Some gd1, Some gd2 => link gd1 gd2
+  end.
+
+Definition link_prog :=
+  if ident_eq p1.(prog_main) p2.(prog_main)
+  && PTree_Properties.for_all dm1 link_prog_check then
+    Some {| prog_main := p1.(prog_main);
+            prog_public := p1.(prog_public) ++ p2.(prog_public);
+            prog_defs := PTree.elements (PTree.combine link_prog_merge dm1 dm2) |}
+  else
+    None.
+
+Lemma link_prog_inv:
+  forall p,
+  link_prog = Some p ->
+      p1.(prog_main) = p2.(prog_main)
+   /\ (forall id gd1 gd2,
+         dm1!id = Some gd1 -> dm2!id = Some gd2 ->
+         In id p1.(prog_public) /\ In id p2.(prog_public) /\ exists gd, link gd1 gd2 = Some gd)
+  /\ p = {| prog_main := p1.(prog_main);
+            prog_public := p1.(prog_public) ++ p2.(prog_public);
+            prog_defs := PTree.elements (PTree.combine link_prog_merge dm1 dm2) |}.
+Proof.
+  unfold link_prog; intros p E.
+  destruct (ident_eq (prog_main p1) (prog_main p2)); try discriminate.
+  destruct (PTree_Properties.for_all dm1 link_prog_check) eqn:C; inv E.
+  rewrite PTree_Properties.for_all_correct in C. 
+  split; auto. split; auto. 
+  intros. exploit C; eauto. unfold link_prog_check. rewrite H0. intros.
+  destruct (in_dec peq id (prog_public p1)); try discriminate.
+  destruct (in_dec peq id (prog_public p2)); try discriminate.
+  destruct (link gd1 gd2) eqn:L; try discriminate.
+  intuition auto. exists g; auto.
+Qed.
+
+Lemma link_prog_succeeds:
+  p1.(prog_main) = p2.(prog_main) ->
+  (forall id gd1 gd2,
+      dm1!id = Some gd1 -> dm2!id = Some gd2 ->
+      In id p1.(prog_public) /\ In id p2.(prog_public) /\ link gd1 gd2 <> None) ->
+  link_prog =
+    Some {| prog_main := p1.(prog_main);
+            prog_public := p1.(prog_public) ++ p2.(prog_public);
+            prog_defs := PTree.elements (PTree.combine link_prog_merge dm1 dm2) |}.
+Proof.
+  intros. unfold link_prog. unfold proj_sumbool. rewrite H, dec_eq_true. simpl. 
+  replace (PTree_Properties.for_all dm1 link_prog_check) with true; auto.
+  symmetry. apply PTree_Properties.for_all_correct; intros. rename a into gd1.
+  unfold link_prog_check. destruct dm2!x as [gd2|] eqn:G2; auto.
+  exploit H0; eauto. intros (P & Q & R). unfold proj_sumbool; rewrite ! pred_dec_true by auto.
+  destruct (link gd1 gd2); auto; discriminate.
+Qed.
+
+Lemma prog_defmap_elements:
+  forall (m: PTree.t (globdef F V)) pub mn x,
+  (prog_defmap {| prog_defs := PTree.elements m; prog_public := pub; prog_main := mn |})!x = m!x.
+Proof.
+  intros. unfold prog_defmap; simpl. apply PTree_Properties.of_list_elements.
+Qed.
+
+End LINKER_PROG.
+
+Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := {
+  link := link_prog;
+  linkorder := fun p1 p2 =>
+     p1.(prog_main) = p2.(prog_main)
+  /\ incl p1.(prog_public) p2.(prog_public)
+  /\ forall id gd1,
+     (prog_defmap p1)!id = Some gd1 ->
+     exists gd2,
+        (prog_defmap p2)!id = Some gd2
+     /\ linkorder gd1 gd2
+     /\ (~In id p2.(prog_public) -> gd2 = gd1)
+}.
+Proof.
+- intros; split; auto. split. apply incl_refl. intros.
+  exists gd1; split; auto. split; auto. apply linkorder_refl. 
+
+- intros x y z (A1 & B1 & C1) (A2 & B2 & C2). 
+  split. congruence. split. red; eauto. 
+  intros. exploit C1; eauto. intros (gd2 & P & Q & R). 
+  exploit C2; eauto. intros (gd3 & U & X & Y). 
+  exists gd3. split; auto. split. eapply linkorder_trans; eauto. 
+  intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto. 
+
+- intros. apply link_prog_inv in H. destruct H as (L1 & L2 & L3).
+  subst z; simpl. intuition auto.
++ red; intros; apply in_app_iff; auto.
++ rewrite prog_defmap_elements, PTree.gcombine, H by auto. 
+  destruct (prog_defmap y)!id as [gd2|] eqn:GD2; simpl.
+* exploit L2; eauto. intros (P & Q & gd & R).
+  exists gd; split. auto. split. apply link_linkorder in R; tauto. 
+  rewrite in_app_iff; tauto.
+* exists gd1; split; auto. split. apply linkorder_refl. auto.
++ red; intros; apply in_app_iff; auto.
++ rewrite prog_defmap_elements, PTree.gcombine, H by auto. 
+  destruct (prog_defmap x)!id as [gd2|] eqn:GD2; simpl.
+* exploit L2; eauto. intros (P & Q & gd & R).
+  exists gd; split. auto. split. apply link_linkorder in R; tauto. 
+  rewrite in_app_iff; tauto.
+* exists gd1; split; auto. split. apply linkorder_refl. auto.
+Defined.
+
+Lemma prog_defmap_linkorder:
+  forall {F V: Type} {LF: Linker F} {LV: Linker V} (p1 p2: program F V) id gd1,
+  linkorder p1 p2 ->
+  (prog_defmap p1)!id = Some gd1 ->
+  exists gd2, (prog_defmap p2)!id = Some gd2 /\ linkorder gd1 gd2.
+Proof.
+  intros. destruct H as (A & B & C).
+  exploit C; eauto. intros (gd2 & P & Q & R). exists gd2; auto.
+Qed.
+
+Global Opaque Linker_prog.
+
+(** * Matching between two programs *)
+
+(** The following is a relational presentation of program transformations,
+  e.g. [transf_partial_program] from module [AST].  *)
+
+(** To capture the possibility of separate compilation, we parameterize
+  the [match_fundef] relation between function definitions with
+  a context, e.g. the compilation unit from which the function definition comes.
+  This unit is characterized as any program that is in the [linkorder]
+  relation with the final, whole program. *)
+
+Section MATCH_PROGRAM_GENERIC.
+
+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.
+
+Inductive match_globvar: globvar V1 -> globvar V2 -> Prop :=
+  | match_globvar_intro: forall i1 i2 init ro vo,
+      match_varinfo i1 i2 ->
+      match_globvar (mkglobvar i1 init ro vo) (mkglobvar i2 init ro vo).
+
+Inductive match_globdef (ctx: C): globdef F1 V1 -> globdef F2 V2 -> Prop :=
+  | match_globdef_fun: forall ctx' f1 f2,
+      linkorder ctx' ctx ->
+      match_fundef ctx' f1 f2 ->
+      match_globdef ctx (Gfun f1) (Gfun f2)
+  | match_globdef_var: forall v1 v2,
+      match_globvar v1 v2 ->
+      match_globdef ctx (Gvar v1) (Gvar v2).
+
+Definition match_ident_globdef
+     (ctx: C) (ig1: ident * globdef F1 V1) (ig2: ident * globdef F2 V2) : Prop :=
+  fst ig1 = fst ig2 /\ match_globdef ctx (snd ig1) (snd ig2).
+
+Definition match_program_gen (ctx: C) (p1: program F1 V1) (p2: program F2 V2) : Prop :=
+  list_forall2 (match_ident_globdef ctx) p1.(prog_defs) p2.(prog_defs)
+  /\ p2.(prog_main) = p1.(prog_main)
+  /\ p2.(prog_public) = p1.(prog_public).
+
+Theorem match_program_defmap:
+  forall ctx p1 p2, match_program_gen ctx p1 p2 ->
+  forall id, option_rel (match_globdef ctx) (prog_defmap p1)!id (prog_defmap p2)!id.
+Proof.
+  intros. apply PTree_Properties.of_list_related. apply H. 
+Qed.
+
+Lemma match_program_gen_main:
+  forall ctx p1 p2, match_program_gen ctx p1 p2 -> p2.(prog_main) = p1.(prog_main).
+Proof.
+  intros. apply H. 
+Qed.
+
+Lemma match_program_public:
+  forall ctx p1 p2, match_program_gen ctx p1 p2 -> p2.(prog_public) = p1.(prog_public).
+Proof.
+  intros. apply H. 
+Qed.
+
+End MATCH_PROGRAM_GENERIC.
+
+(** In many cases, the context for [match_program_gen] is the source program or 
+  source compilation unit itself.  We provide a specialized definition for this case. *)
+
+Definition match_program {F1 V1 F2 V2: Type} {LF: Linker F1} {LV: Linker V1}
+                         (match_fundef: program F1 V1 -> F1 -> F2 -> Prop)
+                         (match_varinfo: V1 -> V2 -> Prop)
+                         (p1: program F1 V1) (p2: program F2 V2) : Prop :=
+  match_program_gen match_fundef match_varinfo p1 p1 p2.
+
+Lemma match_program_main:
+  forall {F1 V1 F2 V2: Type} {LF: Linker F1} {LV: Linker V1}
+         {match_fundef: program F1 V1 -> F1 -> F2 -> Prop}
+         {match_varinfo: V1 -> V2 -> Prop}
+         {p1: program F1 V1} {p2: program F2 V2},
+  match_program match_fundef match_varinfo p1 p2 -> p2.(prog_main) = p1.(prog_main).
+Proof.
+  intros. apply H.
+Qed.
+
+(*
+Lemma match_program_implies:
+  forall (A B V W: Type) (LA: Linker A) (LV: Linker V)
+         (match_fundef1 match_fundef2: program A V -> A -> B -> Prop)
+         (match_varinfo1 match_varinfo2: V -> W -> Prop)
+         p p',
+  match_program match_fundef1 match_varinfo1 p p' ->
+  (forall cu a b, match_fundef1 cu a b -> linkorder cu p -> match_fundef2 cu a b) ->
+  (forall v w, match_varinfo1 v w -> match_varinfo2 v w) ->
+  match_program match_fundef2 match_varinfo2 p p'.
+Proof.
+  intros. destruct H as [P Q]. split; auto. 
+  eapply list_forall2_imply; eauto.
+  intros. inv H3. split; auto. inv H5.
+  econstructor; eauto.
+  constructor. inv H7; constructor; auto.
+Qed.
+*)
+
+(** Relation between the program transformation functions from [AST]
+  and the [match_program] predicate. *)
+
+Theorem match_transform_partial_program2:
+  forall {C F1 V1 F2 V2: Type} {LC: Linker C} {LF: Linker F1} {LV: Linker V1}
+         (match_fundef: C -> F1 -> F2 -> Prop)
+         (match_varinfo: V1 -> V2 -> Prop)
+         (transf_fun: ident -> F1 -> res F2)
+         (transf_var: ident -> V1 -> res V2)
+         (ctx: C) (p: program F1 V1) (tp: program F2 V2),
+  transform_partial_program2 transf_fun transf_var p = OK tp ->
+  (forall i f tf, transf_fun i f = OK tf -> match_fundef ctx f tf) ->
+  (forall i v tv, transf_var i v = OK tv -> match_varinfo v tv) ->
+  match_program_gen match_fundef match_varinfo ctx p tp.
+Proof.
+  unfold transform_partial_program2; intros. monadInv H.
+  red; simpl; split; auto. 
+  revert x EQ. generalize (prog_defs p). 
+  induction l as [ | [i g] l]; simpl; intros.
+- monadInv EQ. constructor.
+- destruct g as [f|v].
++ destruct (transf_fun i f) as [tf|?] eqn:TF; monadInv EQ. 
+  constructor; auto. split; simpl; auto. econstructor. apply linkorder_refl. eauto.
++ destruct (transf_globvar transf_var i v) as [tv|?] eqn:TV; monadInv EQ.
+  constructor; auto. split; simpl; auto. constructor.
+  monadInv TV. destruct v; simpl; constructor. eauto.
+Qed.
+
+Theorem match_transform_partial_program_contextual:
+  forall {A B V: Type} {LA: Linker A} {LV: Linker V}
+         (match_fundef: program A V -> A -> B -> Prop)
+         (transf_fun: A -> res B)
+         (p: program A V) (tp: program B V),
+  transform_partial_program transf_fun p = OK tp ->
+  (forall f tf, transf_fun f = OK tf -> match_fundef p f tf) ->
+  match_program match_fundef eq p tp.
+Proof.
+  intros. 
+  eapply match_transform_partial_program2. eexact H.
+  auto.
+  simpl; intros. congruence.
+Qed.
+
+Theorem match_transform_program_contextual:
+  forall {A B V: Type} {LA: Linker A} {LV: Linker V}
+         (match_fundef: program A V -> A -> B -> Prop)
+         (transf_fun: A -> B)
+         (p: program A V),
+  (forall f, match_fundef p f (transf_fun f)) ->
+  match_program match_fundef eq p (transform_program transf_fun p).
+Proof.
+  intros. 
+  eapply match_transform_partial_program_contextual. 
+  apply transform_program_partial_program with (transf_fun := transf_fun).
+  simpl; intros. inv H0. auto.
+Qed.
+
+(** The following two theorems are simpler versions for the case where the
+  function transformation does not depend on the compilation unit. *)
+
+Theorem match_transform_partial_program:
+  forall {A B V: Type} {LA: Linker A} {LV: Linker V}
+         (transf_fun: A -> res B)
+         (p: program A V) (tp: program B V),
+  transform_partial_program transf_fun p = OK tp ->
+  match_program (fun cu f tf => transf_fun f = OK tf) eq p tp.
+Proof.
+  intros.
+  eapply match_transform_partial_program2. eexact H.
+  auto.
+  simpl; intros. congruence.
+Qed.
+
+Theorem match_transform_program:
+  forall {A B V: Type} {LA: Linker A} {LV: Linker V}
+         (transf: A -> B)
+         (p: program A V),
+  match_program (fun cu f tf => tf = transf f) eq p (transform_program transf p).
+Proof.
+  intros. apply match_transform_program_contextual. auto.
+Qed.
+
+(** * Commutation between linking and program transformations *)
+
+Section LINK_MATCH_PROGRAM.
+
+Context {C F1 V1 F2 V2: Type} {LC: Linker C} {LF1: Linker F1} {LF2: Linker F2} {LV1: Linker V1} {LV2: Linker V2}.
+Variable match_fundef: C -> F1 -> F2 -> Prop.
+Variable match_varinfo: V1 -> V2 -> Prop.
+
+Local Transparent Linker_vardef Linker_def Linker_prog.
+
+Hypothesis link_match_fundef:
+  forall ctx1 ctx2 f1 tf1 f2 tf2 f,
+  link f1 f2 = Some f ->
+  match_fundef ctx1 f1 tf1 -> match_fundef ctx2 f2 tf2 ->
+  exists tf, link tf1 tf2 = Some tf /\ (match_fundef ctx1 f tf \/ match_fundef ctx2 f tf).
+
+Hypothesis link_match_varinfo:
+  forall v1 tv1 v2 tv2 v,
+  link v1 v2 = Some v ->
+  match_varinfo v1 tv1 -> match_varinfo v2 tv2 ->
+  exists tv, link tv1 tv2 = Some tv /\ match_varinfo v tv.
+
+Lemma link_match_globvar:
+  forall v1 tv1 v2 tv2 v,
+  link v1 v2 = Some v ->
+  match_globvar match_varinfo v1 tv1 -> match_globvar match_varinfo v2 tv2 ->
+  exists tv, link tv1 tv2 = Some tv /\ match_globvar match_varinfo v tv.
+Proof.
+  simpl; intros. unfold link_vardef in *. inv H0; inv H1; simpl in *. 
+  destruct (link i1 i0) as [info'|] eqn:LINFO; try discriminate.
+  destruct (link init init0) as [init'|] eqn:LINIT; try discriminate.
+  destruct (eqb ro ro0 && eqb vo vo0); inv H.
+  exploit link_match_varinfo; eauto. intros (tinfo & P & Q). rewrite P. 
+  econstructor; split. eauto. constructor. auto.
+Qed.
+
+Lemma link_match_globdef:
+  forall ctx1 ctx2 ctx g1 tg1 g2 tg2 g,
+  linkorder ctx1 ctx -> linkorder ctx2 ctx ->
+  link g1 g2 = Some g ->
+  match_globdef match_fundef match_varinfo ctx1 g1 tg1 ->
+  match_globdef match_fundef match_varinfo ctx2 g2 tg2 ->
+  exists tg, link tg1 tg2 = Some tg /\ match_globdef match_fundef match_varinfo ctx g tg.
+Proof.
+  simpl link. unfold link_def. intros. inv H2; inv H3; try discriminate.
+- destruct (link f1 f0) as [f|] eqn:LF; inv H1.
+  exploit link_match_fundef; eauto. intros (tf & P & Q).
+  assert (X: exists ctx', linkorder ctx' ctx /\ match_fundef ctx' f tf).
+  { destruct Q as [Q|Q]; econstructor; (split; [|eassumption]).
+    apply linkorder_trans with ctx1; auto. 
+    apply linkorder_trans with ctx2; auto. }
+  destruct X as (cu & X & Y).
+  exists (Gfun tf); split. rewrite P; auto. econstructor; eauto.
+- destruct (link v1 v0) as [v|] eqn:LVAR; inv H1.
+  exploit link_match_globvar; eauto. intros (tv & P & Q).
+  exists (Gvar tv); split. rewrite P; auto. constructor; auto.
+Qed.
+
+Lemma match_globdef_linkorder:
+  forall ctx ctx' g tg,
+  match_globdef match_fundef match_varinfo ctx g tg ->
+  linkorder ctx ctx' ->
+  match_globdef match_fundef match_varinfo ctx' g tg.
+Proof.
+  intros. inv H. 
+- econstructor. eapply linkorder_trans; eauto. auto.
+- constructor; auto.
+Qed.
+
+Theorem link_match_program:
+  forall ctx1 ctx2 ctx p1 p2 tp1 tp2 p,
+  link p1 p2 = Some p ->
+  match_program_gen match_fundef match_varinfo ctx1 p1 tp1 ->
+  match_program_gen match_fundef match_varinfo ctx2 p2 tp2 ->
+  linkorder ctx1 ctx -> linkorder ctx2 ctx ->
+  exists tp, link tp1 tp2 = Some tp /\ match_program_gen match_fundef match_varinfo ctx p tp.
+Proof.
+  intros. destruct (link_prog_inv _ _ _ H) as (P & Q & R).
+  generalize H0; intros (A1 & B1 & C1).
+  generalize H1; intros (A2 & B2 & C2).
+  econstructor; split.
+- apply link_prog_succeeds. 
++ congruence. 
++ intros. 
+  generalize (match_program_defmap _ _ _ _ _ H0 id) (match_program_defmap _ _ _ _ _ H1 id).
+  rewrite H4, H5. intros R1 R2; inv R1; inv R2.
+  exploit Q; eauto. intros (X & Y & gd & Z).
+  exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. 
+  intros (tg & TL & _). intuition congruence.
+- split; [|split].
++ rewrite R. apply PTree.elements_canonical_order'. intros id. 
+  rewrite ! PTree.gcombine by auto.
+  generalize (match_program_defmap _ _ _ _ _ H0 id) (match_program_defmap _ _ _ _ _ H1 id).
+  clear R. intros R1 R2; inv R1; inv R2; unfold link_prog_merge.
+* constructor.
+* constructor. apply match_globdef_linkorder with ctx2; auto. 
+* constructor. apply match_globdef_linkorder with ctx1; auto.
+* exploit Q; eauto. intros (X & Y & gd & Z).
+  exploit link_match_globdef. eexact H2. eexact H3. eauto. eauto. eauto. 
+  intros (tg & TL & MG). rewrite Z, TL. constructor; auto. 
++ rewrite R; simpl; auto.
++ rewrite R; simpl. congruence.
+Qed.
+
+End LINK_MATCH_PROGRAM.
+
+(** We now wrap this commutation diagram into a class, and provide some common instances. *)
+
+Class TransfLink {A B: Type} {LA: Linker A} {LB: Linker B} (transf: A -> B -> Prop) :=
+  transf_link:
+    forall (p1 p2: A) (tp1 tp2: B) (p: A),
+    link p1 p2 = Some p ->
+    transf p1 tp1 -> transf p2 tp2 ->
+    exists tp, link tp1 tp2 = Some tp /\ transf p tp.
+
+Remark link_transf_partial_fundef:
+  forall (A B: Type) (tr1 tr2: A -> res B) (f1 f2: fundef A) (tf1 tf2: fundef B) (f: fundef A),
+  link f1 f2 = Some f ->
+  transf_partial_fundef tr1 f1 = OK tf1 ->
+  transf_partial_fundef tr2 f2 = OK tf2 ->
+  exists tf, 
+      link tf1 tf2 = Some tf
+  /\ (transf_partial_fundef tr1 f = OK tf \/ transf_partial_fundef tr2 f = OK tf).
+Proof.
+Local Transparent Linker_fundef.
+  simpl; intros. destruct f1 as [f1|ef1], f2 as [f2|ef2]; simpl in *; monadInv H0; monadInv H1.
+- discriminate.
+- destruct ef2; inv H. exists (Internal x); split; auto. left; simpl; rewrite EQ; auto.
+- destruct ef1; inv H. exists (Internal x); split; auto. right; simpl; rewrite EQ; auto.
+- destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto. 
+Qed.
+
+Instance TransfPartialContextualLink
+           {A B C V: Type} {LV: Linker V}
+           (tr_fun: C -> A -> res B)
+           (ctx_for: program (fundef A) V -> C):
+  TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) =>
+              match_program
+                (fun cu f tf => AST.transf_partial_fundef (tr_fun (ctx_for cu)) f = OK tf)
+                eq p1 p2).
+Proof.
+  red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
+  eapply link_match_program; eauto.
+- intros. eapply link_transf_partial_fundef; eauto. 
+- intros; subst. exists v; auto. 
+Qed.
+
+Instance TransfPartialLink
+           {A B V: Type} {LV: Linker V}
+           (tr_fun: A -> res B):
+  TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) =>
+              match_program
+                (fun cu f tf => AST.transf_partial_fundef tr_fun f = OK tf)
+                eq p1 p2).
+Proof.
+  red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
+  eapply link_match_program; eauto.
+- intros. eapply link_transf_partial_fundef; eauto. 
+- intros; subst. exists v; auto. 
+Qed.
+
+Instance TransfTotallContextualLink
+           {A B C V: Type} {LV: Linker V}
+           (tr_fun: C -> A -> B)
+           (ctx_for: program (fundef A) V -> C):
+  TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) =>
+              match_program
+                (fun cu f tf => tf = AST.transf_fundef (tr_fun (ctx_for cu)) f)
+                eq p1 p2).
+Proof.
+  red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
+  eapply link_match_program; eauto.
+- intros. subst. destruct f1, f2; simpl in *. 
++ discriminate.
++ destruct e; inv H2. econstructor; eauto. 
++ destruct e; inv H2. econstructor; eauto. 
++ destruct (external_function_eq e e0); inv H2. econstructor; eauto. 
+- intros; subst. exists v; auto. 
+Qed.
+
+Instance TransfTotalLink
+           {A B V: Type} {LV: Linker V}
+           (tr_fun: A -> B):
+  TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) =>
+              match_program
+                (fun cu f tf => tf = AST.transf_fundef tr_fun f)
+                eq p1 p2).
+Proof.
+  red. intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
+  eapply link_match_program; eauto.
+- intros. subst. destruct f1, f2; simpl in *. 
++ discriminate.
++ destruct e; inv H2. econstructor; eauto. 
++ destruct e; inv H2. econstructor; eauto. 
++ destruct (external_function_eq e e0); inv H2. econstructor; eauto. 
+- intros; subst. exists v; auto. 
+Qed.
+
+(** * Linking a set of compilation units *)
+
+(** Here, we take a more general view of linking as taking a nonempty list of compilation units
+  and producing a whole program. *)
+
+Section LINK_LIST.
+
+Context {A: Type} {LA: Linker A}.
+
+Fixpoint link_list (l: nlist A) : option A :=
+  match l with
+  | nbase a => Some a
+  | ncons a l =>
+      match link_list l with None => None | Some b => link a b end
+  end.
+
+Lemma link_list_linkorder:
+  forall a l b, link_list l = Some b -> nIn a l -> linkorder a b.
+Proof.
+  induction l; simpl; intros.
+- inv H. subst. apply linkorder_refl.
+- destruct (link_list l) as [b'|]; try discriminate.
+  apply link_linkorder in H. destruct H0.
++ subst a0. tauto.
++ apply linkorder_trans with b'. auto. tauto.
+Qed.
+
+End LINK_LIST.
+
+(** List linking commutes with program transformations, provided the
+  transformation commutes with simple (binary) linking. *)
+
+Section LINK_LIST_MATCH.
+
+Context {A B: Type} {LA: Linker A} {LB: Linker B} (prog_match: A -> B -> Prop) {TL: TransfLink prog_match}.
+
+Theorem link_list_match:
+  forall al bl, nlist_forall2 prog_match al bl ->
+  forall a, link_list al = Some a ->
+  exists b, link_list bl = Some b /\ prog_match a b.
+Proof.
+  induction 1; simpl; intros a' L.
+- inv L. exists b; auto. 
+- destruct (link_list l) as [a1|] eqn:LL; try discriminate.
+  exploit IHnlist_forall2; eauto. intros (b' & P & Q).
+  red in TL. exploit TL; eauto. intros (b'' & U & V).
+  rewrite P; exists b''; auto.
+Qed.
+
+End LINK_LIST_MATCH.
+
+(** * Linking and composition of compilation passes *)
+
+Set Implicit Arguments.
+
+(** A generic language is a type of programs and a linker. *)
+
+Structure Language := mklang { lang_prog :> Type; lang_link: Linker lang_prog }.
+
+Canonical Structure Language_gen (A: Type) (L: Linker A) : Language := @mklang A L.
+
+(** A compilation pass from language [S] (source) to language [T] (target)
+  is a matching relation between [S] programs and [T] programs,
+  plus two linkers, one for [S] and one for [T],
+  and a property of commutation with linking. *)
+
+Record Pass (S T: Language) := mkpass {
+  pass_match :> lang_prog S -> lang_prog T -> Prop;
+  pass_match_link: @TransfLink (lang_prog S) (lang_prog T) (lang_link S) (lang_link T) pass_match
+}.
+
+Arguments mkpass {S} {T} (pass_match) {pass_match_link}.
+
+Program Definition pass_identity (l: Language): Pass l l :=
+  {| pass_match := fun p1 p2 => p1 = p2;
+     pass_match_link := _ |}.
+Next Obligation.
+  red; intros. subst. exists p; auto. 
+Defined.
+
+Program Definition pass_compose {l1 l2 l3: Language} (pass: Pass l1 l2) (pass': Pass l2 l3) : Pass l1 l3 :=
+  {| pass_match := fun p1 p3 => exists p2, pass_match pass p1 p2 /\ pass_match pass' p2 p3;
+     pass_match_link := _ |}.
+Next Obligation.
+  red; intros.
+  destruct H0 as (p1' & A1 & B1).
+  destruct H1 as (p2' & A2 & B2).
+  edestruct (pass_match_link pass) as (p' & A & B); eauto.
+  edestruct (pass_match_link pass') as (tp & C & D); eauto.
+Defined.
+
+(** A list of compilation passes that can be composed. *)
+
+Inductive Passes: Language -> Language -> Type :=
+  | pass_nil: forall l, Passes l l
+  | pass_cons: forall l1 l2 l3, Pass l1 l2 -> Passes l2 l3 -> Passes l1 l3.
+
+Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope.
+
+(** The pass corresponding to the composition of a list of passes. *)
+
+Fixpoint compose_passes (l l': Language) (passes: Passes l l') : Pass l l' :=
+  match passes in Passes l l' return Pass l l' with
+  | pass_nil l => pass_identity l
+  | pass_cons l1 l2 l3 pass1 passes => pass_compose pass1 (compose_passes passes)
+  end.
+
+(** Some more lemmas about [nlist_forall2]. *)
+
+Lemma nlist_forall2_identity:
+  forall (A: Type) (la lb: nlist A),
+  nlist_forall2 (fun a b => a = b) la lb -> la = lb.
+Proof.
+  induction 1; congruence.
+Qed.
+
+Lemma nlist_forall2_compose_inv:
+  forall (A B C: Type) (R1: A -> B -> Prop) (R2: B -> C -> Prop)
+         (la: nlist A) (lc: nlist C),
+  nlist_forall2 (fun a c => exists b, R1 a b /\ R2 b c) la lc ->
+  exists lb: nlist B, nlist_forall2 R1 la lb /\ nlist_forall2 R2 lb lc.
+Proof.
+  induction 1.
+- rename b into c. destruct H as (b & P & Q). 
+  exists (nbase b); split; constructor; auto.
+- rename b into c. destruct H as (b & P & Q). destruct IHnlist_forall2 as (lb & U & V).
+  exists (ncons b lb); split; constructor; auto.
+Qed.
+
+(** List linking with a composition of compilation passes. *)
+
+Theorem link_list_compose_passes:
+  forall (src tgt: Language) (passes: Passes src tgt)
+         (src_units: nlist src) (tgt_units: nlist tgt),
+  nlist_forall2 (pass_match (compose_passes passes)) src_units tgt_units ->
+  forall src_prog,
+  @link_list _ (lang_link src) src_units = Some src_prog ->
+  exists tgt_prog,
+  @link_list _ (lang_link tgt) tgt_units = Some tgt_prog
+  /\ pass_match (compose_passes passes) src_prog tgt_prog.
+Proof.
+  induction passes; simpl; intros src_units tgt_units F2 src_prog LINK.
+- apply nlist_forall2_identity in F2. subst tgt_units. exists src_prog; auto.
+- apply nlist_forall2_compose_inv in F2. destruct F2 as (interm_units & P & Q).
+  edestruct (@link_list_match _ _ (lang_link l1) (lang_link l2) (pass_match p))
+  as (interm_prog & U & V).
+  apply pass_match_link. eauto. eauto.  
+  exploit IHpasses; eauto. intros (tgt_prog & X & Y).
+  exists tgt_prog; split; auto. exists interm_prog; auto. 
+Qed.
+
diff --git a/common/Memory.v b/common/Memory.v
index 93d0e432..0ea9e3b0 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -4143,6 +4143,8 @@ Section UNCHANGED_ON.
 Variable P: block -> Z -> Prop.
 
 Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
+  unchanged_on_nextblock:
+    Ple (nextblock m_before) (nextblock m_after);
   unchanged_on_perm:
     forall b ofs k p,
     P b ofs -> valid_block m_before b ->
@@ -4157,15 +4159,22 @@ Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
 Lemma unchanged_on_refl:
   forall m, unchanged_on m m.
 Proof.
-  intros; constructor; tauto.
+  intros; constructor. apply Ple_refl. tauto. tauto.
+Qed.
+
+Lemma valid_block_unchanged_on:
+  forall m m' b,
+  unchanged_on m m' -> valid_block m b -> valid_block m' b.
+Proof.
+  unfold valid_block; intros. apply unchanged_on_nextblock in H. xomega.
 Qed.
 
 Lemma perm_unchanged_on:
   forall m m' b ofs k p,
-  unchanged_on m m' -> P b ofs -> valid_block m b ->
+  unchanged_on m m' -> P b ofs ->
   perm m b ofs k p -> perm m' b ofs k p.
 Proof.
-  intros. destruct H. apply unchanged_on_perm0; auto.
+  intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. 
 Qed.
 
 Lemma perm_unchanged_on_2:
@@ -4176,6 +4185,17 @@ Proof.
   intros. destruct H. apply unchanged_on_perm0; auto.
 Qed.
 
+Lemma unchanged_on_trans:
+  forall m1 m2 m3, unchanged_on m1 m2 -> unchanged_on m2 m3 -> unchanged_on m1 m3.
+Proof.
+  intros; constructor.
+- apply Ple_trans with (nextblock m2); apply unchanged_on_nextblock; auto.
+- intros. transitivity (perm m2 b ofs k p); apply unchanged_on_perm; auto.
+  eapply valid_block_unchanged_on; eauto.
+- intros. transitivity (ZMap.get ofs (mem_contents m2)#b); apply unchanged_on_contents; auto.
+  eapply perm_unchanged_on; eauto. 
+Qed.
+
 Lemma loadbytes_unchanged_on_1:
   forall m m' b ofs n,
   unchanged_on m m' ->
@@ -4243,6 +4263,7 @@ Lemma store_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_store _ _ _ _ _ _ H). apply Ple_refl.
 - split; intros; eauto with mem.
 - erewrite store_mem_contents; eauto. rewrite PMap.gsspec.
   destruct (peq b0 b); auto. subst b0. apply setN_outside.
@@ -4259,6 +4280,7 @@ Lemma storebytes_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_storebytes _ _ _ _ _ H). apply Ple_refl.
 - split; intros. eapply perm_storebytes_1; eauto. eapply perm_storebytes_2; eauto.
 - erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec.
   destruct (peq b0 b); auto. subst b0. apply setN_outside.
@@ -4273,6 +4295,7 @@ Lemma alloc_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_alloc _ _ _ _ _ H). apply Ple_succ.
 - split; intros.
   eapply perm_alloc_1; eauto.
   eapply perm_alloc_4; eauto.
@@ -4288,6 +4311,7 @@ Lemma free_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_free _ _ _ _ _ H). apply Ple_refl.
 - split; intros.
   eapply perm_free_1; eauto.
   destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto.
@@ -4297,8 +4321,39 @@ Proof.
   simpl. auto.
 Qed.
 
+Lemma drop_perm_unchanged_on:
+  forall m b lo hi p m',
+  drop_perm m b lo hi p = Some m' ->
+  (forall i, lo <= i < hi -> ~ P b i) ->
+  unchanged_on m m'.
+Proof.
+  intros; constructor; intros.
+- rewrite (nextblock_drop _ _ _ _ _ _ H). apply Ple_refl.
+- split; intros. eapply perm_drop_3; eauto.
+  destruct (eq_block b0 b); auto.
+  subst b0. 
+  assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. }
+  right; omega.
+  eapply perm_drop_4; eauto. 
+- unfold drop_perm in H. 
+  destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto.
+Qed. 
+
 End UNCHANGED_ON.
 
+Lemma unchanged_on_implies:
+  forall (P Q: block -> Z -> Prop) m m',
+  unchanged_on P m m' ->
+  (forall b ofs, Q b ofs -> valid_block m b -> P b ofs) ->
+  unchanged_on Q m m'.
+Proof.
+  intros. destruct H. constructor; intros.
+- auto.
+- apply unchanged_on_perm0; auto. 
+- apply unchanged_on_contents0; auto. 
+  apply H0; auto. eapply perm_valid_block; eauto. 
+Qed.
+
 End Mem.
 
 Notation mem := Mem.mem.
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 4994026a..48172dfd 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -39,6 +39,7 @@ let name_of_chunk = function
 let name_of_external = function
   | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name)
   | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name)
+  | EF_runtime(name, sg) -> sprintf "runtime %S" (camlstring_of_coqstring name)
   | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk)
   | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk)
   | EF_malloc -> "malloc"
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 71cef35f..9c91243a 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -513,43 +513,49 @@ Open Scope smallstep_scope.
 
 (** The general form of a forward simulation. *)
 
-Record forward_simulation (L1 L2: semantics) : Type :=
-  Forward_simulation {
-    fsim_index: Type;
-    fsim_order: fsim_index -> fsim_index -> Prop;
-    fsim_order_wf: well_founded fsim_order;
-    fsim_match_states :> fsim_index -> state L1 -> state L2 -> Prop;
+Record fsim_properties (L1 L2: semantics) (index: Type)
+                       (order: index -> index -> Prop)
+                       (match_states: index -> state L1 -> state L2 -> Prop) : Prop := {
+    fsim_order_wf: well_founded order;
     fsim_match_initial_states:
       forall s1, initial_state L1 s1 ->
-      exists i, exists s2, initial_state L2 s2 /\ fsim_match_states i s1 s2;
+      exists i, exists s2, initial_state L2 s2 /\ match_states i s1 s2;
     fsim_match_final_states:
       forall i s1 s2 r,
-      fsim_match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r;
+      match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r;
     fsim_simulation:
       forall s1 t s1', Step L1 s1 t s1' ->
-      forall i s2, fsim_match_states i s1 s2 ->
+      forall i s2, match_states i s1 s2 ->
       exists i', exists s2',
-         (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ fsim_order i' i))
-      /\ fsim_match_states i' s1' s2';
+         (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ order i' i))
+      /\ match_states i' s1' s2';
     fsim_public_preserved:
       forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id
   }.
 
-Implicit Arguments forward_simulation [].
+Arguments fsim_properties: clear implicits.
+
+Inductive forward_simulation (L1 L2: semantics) : Prop :=
+  Forward_simulation (index: Type)
+                     (order: index -> index -> Prop)
+                     (match_states: index -> state L1 -> state L2 -> Prop)
+                     (props: fsim_properties L1 L2 index order match_states).
+
+Arguments Forward_simulation {L1 L2 index} order match_states props.
 
 (** An alternate form of the simulation diagram *)
 
 Lemma fsim_simulation':
-  forall L1 L2 (S: forward_simulation L1 L2),
+  forall L1 L2 index order match_states, fsim_properties L1 L2 index order match_states ->
   forall i s1 t s1', Step L1 s1 t s1' ->
-  forall s2, S i s1 s2 ->
-  (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2')
-  \/ (exists i', fsim_order S i' i /\ t = E0 /\ S i' s1' s2).
+  forall s2, match_states i s1 s2 ->
+  (exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2')
+  \/ (exists i', order i' i /\ t = E0 /\ match_states i' s1' s2).
 Proof.
   intros. exploit fsim_simulation; eauto.
   intros [i' [s2' [A B]]]. intuition.
   left; exists i'; exists s2'; auto.
-  inv H2.
+  inv H3.
   right; exists i'; auto.
   left; exists i'; exists s2'; split; auto. econstructor; eauto.
 Qed.
@@ -602,15 +608,15 @@ Hypothesis simulation:
 
 Lemma forward_simulation_star_wf: forward_simulation L1 L2.
 Proof.
-  apply Forward_simulation with
-    (fsim_order := order)
-    (fsim_match_states := fun idx s1 s2 => idx = s1 /\ match_states s1 s2);
-  auto.
-  intros. exploit match_initial_states; eauto. intros [s2 [A B]].
+  apply Forward_simulation with order (fun idx s1 s2 => idx = s1 /\ match_states s1 s2);
+  constructor.
+- auto.
+- intros. exploit match_initial_states; eauto. intros [s2 [A B]].
     exists s1; exists s2; auto.
-  intros. destruct H. eapply match_final_states; eauto.
-  intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]].
-  exists s1'; exists s2'; intuition.
+- intros. destruct H. eapply match_final_states; eauto.
+- intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]].
+  exists s1'; exists s2'; intuition auto.
+- auto.
 Qed.
 
 End SIMULATION_STAR_WF.
@@ -709,28 +715,26 @@ End FORWARD_SIMU_DIAGRAMS.
 
 Section SIMULATION_SEQUENCES.
 
-Variable L1: semantics.
-Variable L2: semantics.
-Variable S: forward_simulation L1 L2.
+Context L1 L2 index order match_states (S: fsim_properties L1 L2 index order match_states).
 
 Lemma simulation_star:
   forall s1 t s1', Star L1 s1 t s1' ->
-  forall i s2, S i s1 s2 ->
-  exists i', exists s2', Star L2 s2 t s2' /\ S i' s1' s2'.
+  forall i s2, match_states i s1 s2 ->
+  exists i', exists s2', Star L2 s2 t s2' /\ match_states i' s1' s2'.
 Proof.
   induction 1; intros.
   exists i; exists s2; split; auto. apply star_refl.
   exploit fsim_simulation; eauto. intros [i' [s2' [A B]]].
   exploit IHstar; eauto. intros [i'' [s2'' [C D]]].
   exists i''; exists s2''; split; auto. eapply star_trans; eauto.
-  intuition. apply plus_star; auto.
+  intuition auto. apply plus_star; auto.
 Qed.
 
 Lemma simulation_plus:
   forall s1 t s1', Plus L1 s1 t s1' ->
-  forall i s2, S i s1 s2 ->
-  (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2')
-  \/ (exists i', clos_trans _ (fsim_order S) i' i /\ t = E0 /\ S i' s1' s2).
+  forall i s2, match_states i s1 s2 ->
+  (exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2')
+  \/ (exists i', clos_trans _ order i' i /\ t = E0 /\ match_states i' s1' s2).
 Proof.
   induction 1 using plus_ind2; intros.
 (* base case *)
@@ -744,34 +748,34 @@ Proof.
   left; exists i''; exists s2''; split; auto. eapply plus_star_trans; eauto.
   exploit IHplus; eauto. intros [[i'' [s2'' [P Q]]] | [i'' [P [Q R]]]].
   subst. simpl. left; exists i''; exists s2''; auto.
-  subst. simpl. right; exists i''; intuition.
+  subst. simpl. right; exists i''; intuition auto.
   eapply t_trans; eauto. eapply t_step; eauto.
 Qed.
 
 Lemma simulation_forever_silent:
   forall i s1 s2,
-  Forever_silent L1 s1 -> S i s1 s2 ->
+  Forever_silent L1 s1 -> match_states i s1 s2 ->
   Forever_silent L2 s2.
 Proof.
   assert (forall i s1 s2,
-          Forever_silent L1 s1 -> S i s1 s2 ->
-          forever_silent_N (step L2) (fsim_order S) (globalenv L2) i s2).
+          Forever_silent L1 s1 -> match_states i s1 s2 ->
+          forever_silent_N (step L2) order (globalenv L2) i s2).
     cofix COINDHYP; intros.
     inv H. destruct (fsim_simulation S _ _ _ H1 _ _ H0) as [i' [s2' [A B]]].
     destruct A as [C | [C D]].
     eapply forever_silent_N_plus; eauto.
     eapply forever_silent_N_star; eauto.
-  intros. eapply forever_silent_N_forever; eauto. apply fsim_order_wf.
+  intros. eapply forever_silent_N_forever; eauto. eapply fsim_order_wf; eauto.
 Qed.
 
 Lemma simulation_forever_reactive:
   forall i s1 s2 T,
-  Forever_reactive L1 s1 T -> S i s1 s2 ->
+  Forever_reactive L1 s1 T -> match_states i s1 s2 ->
   Forever_reactive L2 s2 T.
 Proof.
   cofix COINDHYP; intros.
   inv H.
-  destruct (simulation_star H1 i _ H0) as [i' [st2' [A B]]].
+  edestruct simulation_star as [i' [st2' [A B]]]; eauto.
   econstructor; eauto.
 Qed.
 
@@ -779,56 +783,48 @@ End SIMULATION_SEQUENCES.
 
 (** ** Composing two forward simulations *)
 
-Section COMPOSE_SIMULATIONS.
-
-Variable L1: semantics.
-Variable L2: semantics.
-Variable L3: semantics.
-Variable S12: forward_simulation L1 L2.
-Variable S23: forward_simulation L2 L3.
-
-Let ff_index : Type := (fsim_index S23 * fsim_index S12)%type.
-
-Let ff_order : ff_index -> ff_index -> Prop :=
-  lex_ord (clos_trans _ (fsim_order S23)) (fsim_order S12).
-
-Let ff_match_states (i: ff_index) (s1: state L1) (s3: state L3) : Prop :=
-  exists s2, S12 (snd i) s1 s2 /\ S23 (fst i) s2 s3.
-
-Lemma compose_forward_simulation: forward_simulation L1 L3.
-Proof.
-  apply Forward_simulation with (fsim_order := ff_order) (fsim_match_states := ff_match_states).
-(* well founded *)
-  unfold ff_order. apply wf_lex_ord. apply wf_clos_trans. apply fsim_order_wf. apply fsim_order_wf.
-(* initial states *)
-  intros. exploit (fsim_match_initial_states S12); eauto. intros [i [s2 [A B]]].
-  exploit (fsim_match_initial_states S23); eauto. intros [i' [s3 [C D]]].
+Lemma compose_forward_simulations:
+  forall L1 L2 L3, forward_simulation L1 L2 -> forward_simulation L2 L3 -> forward_simulation L1 L3.
+Proof.
+  intros L1 L2 L3 S12 S23. 
+  destruct S12 as [index order match_states props].
+  destruct S23 as [index' order' match_states' props'].
+
+  set (ff_index := (index' * index)%type).
+  set (ff_order := lex_ord (clos_trans _ order') order).
+  set (ff_match_states := fun (i: ff_index) (s1: state L1) (s3: state L3) =>
+                             exists s2, match_states (snd i) s1 s2 /\ match_states' (fst i) s2 s3).
+  apply Forward_simulation with ff_order ff_match_states; constructor.
+- (* well founded *)
+  unfold ff_order. apply wf_lex_ord. apply wf_clos_trans.
+  eapply fsim_order_wf; eauto. eapply fsim_order_wf; eauto.
+- (* initial states *)
+  intros. exploit (fsim_match_initial_states props); eauto. intros [i [s2 [A B]]].
+  exploit (fsim_match_initial_states props'); eauto. intros [i' [s3 [C D]]].
   exists (i', i); exists s3; split; auto. exists s2; auto.
-(* final states *)
+- (* final states *)
   intros. destruct H as [s3 [A B]].
-  eapply (fsim_match_final_states S23); eauto.
-  eapply (fsim_match_final_states S12); eauto.
-(* simulation *)
+  eapply (fsim_match_final_states props'); eauto.
+  eapply (fsim_match_final_states props); eauto.
+- (* simulation *)
   intros. destruct H0 as [s3 [A B]]. destruct i as [i2 i1]; simpl in *.
-  exploit (fsim_simulation' S12); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]].
-  (* L2 makes one or several steps. *)
+  exploit (fsim_simulation' props); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]].
++ (* L2 makes one or several steps. *)
   exploit simulation_plus; eauto. intros [[i2' [s2' [P Q]]] | [i2' [P [Q R]]]].
-  (* L3 makes one or several steps *)
+* (* L3 makes one or several steps *)
   exists (i2', i1'); exists s2'; split. auto. exists s3'; auto.
-  (* L3 makes no step *)
+* (* L3 makes no step *)
   exists (i2', i1'); exists s2; split.
   right; split. subst t; apply star_refl. red. left. auto.
   exists s3'; auto.
-  (* L2 makes no step *)
++ (* L2 makes no step *)
   exists (i2, i1'); exists s2; split.
   right; split. subst t; apply star_refl. red. right. auto.
   exists s3; auto.
-(* symbols *)
-  intros. transitivity (Senv.public_symbol (symbolenv L2) id); apply fsim_public_preserved; auto.
+- (* symbols *)
+  intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply fsim_public_preserved; eauto.
 Qed.
 
-End COMPOSE_SIMULATIONS.
-
 (** * Receptiveness and determinacy *)
 
 Definition single_events (L: semantics) : Prop :=
@@ -916,49 +912,57 @@ Qed.
 
 (** The general form of a backward simulation. *)
 
-Record backward_simulation (L1 L2: semantics) : Type :=
-  Backward_simulation {
-    bsim_index: Type;
-    bsim_order: bsim_index -> bsim_index -> Prop;
-    bsim_order_wf: well_founded bsim_order;
-    bsim_match_states :> bsim_index -> state L1 -> state L2 -> Prop;
+Record bsim_properties (L1 L2: semantics) (index: Type)
+                       (order: index -> index -> Prop)
+                       (match_states: index -> state L1 -> state L2 -> Prop) : Prop := {
+    bsim_order_wf: well_founded order;
     bsim_initial_states_exist:
       forall s1, initial_state L1 s1 -> exists s2, initial_state L2 s2;
     bsim_match_initial_states:
       forall s1 s2, initial_state L1 s1 -> initial_state L2 s2 ->
-      exists i, exists s1', initial_state L1 s1' /\ bsim_match_states i s1' s2;
+      exists i, exists s1', initial_state L1 s1' /\ match_states i s1' s2;
     bsim_match_final_states:
       forall i s1 s2 r,
-      bsim_match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r ->
+      match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r ->
       exists s1', Star L1 s1 E0 s1' /\ final_state L1 s1' r;
     bsim_progress:
       forall i s1 s2,
-      bsim_match_states i s1 s2 -> safe L1 s1 ->
+      match_states i s1 s2 -> safe L1 s1 ->
       (exists r, final_state L2 s2 r) \/
       (exists t, exists s2', Step L2 s2 t s2');
     bsim_simulation:
       forall s2 t s2', Step L2 s2 t s2' ->
-      forall i s1, bsim_match_states i s1 s2 -> safe L1 s1 ->
+      forall i s1, match_states i s1 s2 -> safe L1 s1 ->
       exists i', exists s1',
-         (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i))
-      /\ bsim_match_states i' s1' s2';
+         (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ order i' i))
+      /\ match_states i' s1' s2';
     bsim_public_preserved:
       forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id
   }.
 
+Arguments bsim_properties: clear implicits.
+
+Inductive backward_simulation (L1 L2: semantics) : Prop :=
+  Backward_simulation (index: Type)
+                      (order: index -> index -> Prop)
+                      (match_states: index -> state L1 -> state L2 -> Prop)
+                      (props: bsim_properties L1 L2 index order match_states).
+
+Arguments Backward_simulation {L1 L2 index} order match_states props.
+
 (** An alternate form of the simulation diagram *)
 
 Lemma bsim_simulation':
-  forall L1 L2 (S: backward_simulation L1 L2),
+  forall L1 L2 index order match_states, bsim_properties L1 L2 index order match_states ->
   forall i s2 t s2', Step L2 s2 t s2' ->
-  forall s1, S i s1 s2 -> safe L1 s1 ->
-  (exists i', exists s1', Plus L1 s1 t s1' /\ S i' s1' s2')
-  \/ (exists i', bsim_order S i' i /\ t = E0 /\ S i' s1 s2').
+  forall s1, match_states i s1 s2 -> safe L1 s1 ->
+  (exists i', exists s1', Plus L1 s1 t s1' /\ match_states i' s1' s2')
+  \/ (exists i', order i' i /\ t = E0 /\ match_states i' s1 s2').
 Proof.
   intros. exploit bsim_simulation; eauto.
   intros [i' [s1' [A B]]]. intuition.
   left; exists i'; exists s1'; auto.
-  inv H3.
+  inv H4.
   right; exists i'; auto.
   left; exists i'; exists s1'; split; auto. econstructor; eauto.
 Qed.
@@ -1004,13 +1008,13 @@ Hypothesis simulation:
 Lemma backward_simulation_plus: backward_simulation L1 L2.
 Proof.
   apply Backward_simulation with
-    (bsim_order := fun (x y: unit) => False)
-    (bsim_match_states := fun (i: unit) s1 s2 => match_states s1 s2);
-  auto.
-  red; intros; constructor; intros. contradiction.
-  intros. exists tt; eauto.
-  intros. exists s1; split. apply star_refl. eauto.
-  intros. exploit simulation; eauto. intros [s1' [A B]].
+    (fun (x y: unit) => False)
+    (fun (i: unit) s1 s2 => match_states s1 s2);
+  constructor; auto.
+- red; intros; constructor; intros. contradiction.
+- intros. exists tt; eauto.
+- intros. exists s1; split. apply star_refl. eauto.
+- intros. exploit simulation; eauto. intros [s1' [A B]].
   exists tt; exists s1'; auto.
 Qed.
 
@@ -1022,19 +1026,17 @@ End BACKWARD_SIMU_DIAGRAMS.
 
 Section BACKWARD_SIMULATION_SEQUENCES.
 
-Variable L1: semantics.
-Variable L2: semantics.
-Variable S: backward_simulation L1 L2.
+Context L1 L2 index order match_states (S: bsim_properties L1 L2 index order match_states).
 
 Lemma bsim_E0_star:
   forall s2 s2', Star L2 s2 E0 s2' ->
-  forall i s1, S i s1 s2 -> safe L1 s1 ->
-  exists i', exists s1', Star L1 s1 E0 s1' /\ S i' s1' s2'.
+  forall i s1, match_states i s1 s2 -> safe L1 s1 ->
+  exists i', exists s1', Star L1 s1 E0 s1' /\ match_states i' s1' s2'.
 Proof.
   intros s20 s20' STAR0. pattern s20, s20'. eapply star_E0_ind; eauto.
-(* base case *)
+- (* base case *)
   intros. exists i; exists s1; split; auto. apply star_refl.
-(* inductive case *)
+- (* inductive case *)
   intros. exploit bsim_simulation; eauto. intros [i' [s1' [A B]]].
   assert (Star L1 s0 E0 s1'). intuition. apply plus_star; auto.
   exploit H0. eauto. eapply star_safe; eauto. intros [i'' [s1'' [C D]]].
@@ -1043,7 +1045,7 @@ Qed.
 
 Lemma bsim_safe:
   forall i s1 s2,
-  S i s1 s2 -> safe L1 s1 -> safe L2 s2.
+  match_states i s1 s2 -> safe L1 s1 -> safe L2 s2.
 Proof.
   intros; red; intros.
   exploit bsim_E0_star; eauto. intros [i' [s1' [A B]]].
@@ -1052,22 +1054,22 @@ Qed.
 
 Lemma bsim_E0_plus:
   forall s2 t s2', Plus L2 s2 t s2' -> t = E0 ->
-  forall i s1, S i s1 s2 -> safe L1 s1 ->
-     (exists i', exists s1', Plus L1 s1 E0 s1' /\ S i' s1' s2')
-  \/ (exists i', clos_trans _ (bsim_order S) i' i /\ S i' s1 s2').
+  forall i s1, match_states i s1 s2 -> safe L1 s1 ->
+     (exists i', exists s1', Plus L1 s1 E0 s1' /\ match_states i' s1' s2')
+  \/ (exists i', clos_trans _ order i' i /\ match_states i' s1 s2').
 Proof.
   induction 1 using plus_ind2; intros; subst t.
-(* base case *)
+- (* base case *)
   exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]].
-  left; exists i'; exists s1'; auto.
-  right; exists i'; intuition.
-(* inductive case *)
++ left; exists i'; exists s1'; auto.
++ right; exists i'; intuition.
+- (* inductive case *)
   exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst.
   exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]].
-  exploit bsim_E0_star. apply plus_star; eauto. eauto. eapply star_safe; eauto. apply plus_star; auto.
++ exploit bsim_E0_star. apply plus_star; eauto. eauto. eapply star_safe; eauto. apply plus_star; auto.
   intros [i'' [s1'' [P Q]]].
   left; exists i''; exists s1''; intuition. eapply plus_star_trans; eauto.
-  exploit IHplus; eauto. intros [P | [i'' [P Q]]].
++ exploit IHplus; eauto. intros [P | [i'' [P Q]]].
   left; auto.
   right; exists i''; intuition. eapply t_trans; eauto. apply t_step; auto.
 Qed.
@@ -1098,21 +1100,20 @@ Variable L1: semantics.
 Variable L2: semantics.
 Variable L3: semantics.
 Hypothesis L3_single_events: single_events L3.
-Variable S12: backward_simulation L1 L2.
-Variable S23: backward_simulation L2 L3.
+Context index order match_states (S12: bsim_properties L1 L2 index order match_states).
+Context index' order' match_states' (S23: bsim_properties L2 L3 index' order' match_states').
 
-Let bb_index : Type := (bsim_index S12 * bsim_index S23)%type.
+Let bb_index : Type := (index * index')%type.
 
-Let bb_order : bb_index -> bb_index -> Prop :=
-  lex_ord (clos_trans _ (bsim_order S12)) (bsim_order S23).
+Definition bb_order : bb_index -> bb_index -> Prop := lex_ord (clos_trans _ order) order'.
 
 Inductive bb_match_states: bb_index -> state L1 -> state L3 -> Prop :=
   | bb_match_later: forall i1 i2 s1 s3 s2x s2y,
-      S12 i1 s1 s2x -> Star L2 s2x E0 s2y -> S23 i2 s2y s3 ->
+      match_states i1 s1 s2x -> Star L2 s2x E0 s2y -> match_states' i2 s2y s3 ->
       bb_match_states (i1, i2) s1 s3.
 
 Lemma bb_match_at: forall i1 i2 s1 s3 s2,
-  S12 i1 s1 s2 -> S23 i2 s2 s3 ->
+  match_states i1 s1 s2 -> match_states' i2 s2 s3 ->
   bb_match_states (i1, i2) s1 s3.
 Proof.
   intros. econstructor; eauto. apply star_refl.
@@ -1120,7 +1121,7 @@ Qed.
 
 Lemma bb_simulation_base:
   forall s3 t s3', Step L3 s3 t s3' ->
-  forall i1 s1 i2 s2, S12 i1 s1 s2 -> S23 i2 s2 s3 -> safe L1 s1 ->
+  forall i1 s1 i2 s2, match_states i1 s1 s2 -> match_states' i2 s2 s3 -> safe L1 s1 ->
   exists i', exists s1',
     (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bb_order i' (i1, i2)))
     /\ bb_match_states i' s1' s3'.
@@ -1128,29 +1129,29 @@ Proof.
   intros.
   exploit (bsim_simulation' S23); eauto. eapply bsim_safe; eauto.
   intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]].
-  (* 1 L2 makes one or several transitions *)
+- (* 1 L2 makes one or several transitions *)
   assert (EITHER: t = E0 \/ (length t = 1)%nat).
-    exploit L3_single_events; eauto.
-    destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction.
+  { exploit L3_single_events; eauto.
+    destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. }
   destruct EITHER.
-  (* 1.1 these are silent transitions *)
-  subst t. exploit bsim_E0_plus; eauto.
++ (* 1.1 these are silent transitions *)
+  subst t. exploit (bsim_E0_plus S12); eauto.
   intros [ [i1' [s1' [PLUS1 MATCH1]]] | [i1' [ORD1 MATCH1]]].
-  (* 1.1.1 L1 makes one or several transitions *)
+* (* 1.1.1 L1 makes one or several transitions *)
   exists (i1', i2'); exists s1'; split. auto. eapply bb_match_at; eauto.
-  (* 1.1.2 L1 makes no transitions *)
+* (* 1.1.2 L1 makes no transitions *)
   exists (i1', i2'); exists s1; split.
   right; split. apply star_refl. left; auto.
   eapply bb_match_at; eauto.
-  (* 1.2 non-silent transitions *)
++ (* 1.2 non-silent transitions *)
   exploit star_non_E0_split. apply plus_star; eauto. auto.
   intros [s2x [s2y [P [Q R]]]].
-  exploit bsim_E0_star. eexact P. eauto. auto. intros [i1' [s1x [X Y]]].
-  exploit bsim_simulation'. eexact Q. eauto. eapply star_safe; eauto.
+  exploit (bsim_E0_star S12). eexact P. eauto. auto. intros [i1' [s1x [X Y]]].
+  exploit (bsim_simulation' S12). eexact Q. eauto. eapply star_safe; eauto.
   intros [[i1'' [s1y [U V]]] | [i1'' [U [V W]]]]; try (subst t; discriminate).
   exists (i1'', i2'); exists s1y; split.
   left. eapply star_plus_trans; eauto. eapply bb_match_later; eauto.
-  (* 2. L2 makes no transitions *)
+- (* 2. L2 makes no transitions *)
   subst. exists (i1, i2'); exists s1; split.
   right; split. apply star_refl. right; auto.
   eapply bb_match_at; eauto.
@@ -1165,12 +1166,12 @@ Lemma bb_simulation:
 Proof.
   intros. inv H0.
   exploit star_inv; eauto. intros [[EQ1 EQ2] | PLUS].
-  (* 1. match at *)
+- (* 1. match at *)
   subst. eapply bb_simulation_base; eauto.
-  (* 2. match later *)
-  exploit bsim_E0_plus; eauto.
+- (* 2. match later *)
+  exploit (bsim_E0_plus S12); eauto.
   intros [[i1' [s1' [A B]]] | [i1' [A B]]].
-  (* 2.1 one or several silent transitions *)
++ (* 2.1 one or several silent transitions *)
   exploit bb_simulation_base. eauto. auto. eexact B. eauto.
     eapply star_safe; eauto. eapply plus_star; eauto.
   intros [i'' [s1'' [C D]]].
@@ -1178,7 +1179,7 @@ Proof.
   left. eapply plus_star_trans; eauto.
   destruct C as [P | [P Q]]. apply plus_star; eauto. eauto.
   traceEq.
-  (* 2.2 no silent transition *)
++ (* 2.2 no silent transition *)
   exploit bb_simulation_base. eauto. auto. eexact B. eauto. auto.
   intros [i'' [s1'' [C D]]].
   exists i''; exists s1''; split; auto.
@@ -1186,48 +1187,53 @@ Proof.
   inv H6. left. eapply t_trans; eauto. left; auto.
 Qed.
 
-Lemma compose_backward_simulation: backward_simulation L1 L3.
-Proof.
-  apply Backward_simulation with (bsim_order := bb_order) (bsim_match_states := bb_match_states).
-(* well founded *)
-  unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. apply bsim_order_wf. apply bsim_order_wf.
-(* initial states exist *)
-  intros. exploit (bsim_initial_states_exist S12); eauto. intros [s2 A].
-  eapply (bsim_initial_states_exist S23); eauto.
-(* match initial states *)
+End COMPOSE_BACKWARD_SIMULATIONS.
+
+Lemma compose_backward_simulation:
+  forall L1 L2 L3,
+  single_events L3 -> backward_simulation L1 L2 -> backward_simulation L2 L3 ->
+  backward_simulation L1 L3.
+Proof.
+  intros L1 L2 L3 L3single S12 S23.
+  destruct S12 as [index order match_states props].
+  destruct S23 as [index' order' match_states' props'].
+  apply Backward_simulation with (bb_order order order') (bb_match_states L1 L2 L3 match_states match_states');
+  constructor.
+- (* well founded *)
+  unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. eapply bsim_order_wf; eauto. eapply bsim_order_wf; eauto.
+- (* initial states exist *)
+  intros. exploit (bsim_initial_states_exist props); eauto. intros [s2 A].
+  eapply (bsim_initial_states_exist props'); eauto.
+- (* match initial states *)
   intros s1 s3 INIT1 INIT3.
-  exploit (bsim_initial_states_exist S12); eauto. intros [s2 INIT2].
-  exploit (bsim_match_initial_states S23); eauto. intros [i2 [s2' [INIT2' M2]]].
-  exploit (bsim_match_initial_states S12); eauto. intros [i1 [s1' [INIT1' M1]]].
-  exists (i1, i2); exists s1'; intuition. eapply bb_match_at; eauto.
-(* match final states *)
+  exploit (bsim_initial_states_exist props); eauto. intros [s2 INIT2].
+  exploit (bsim_match_initial_states props'); eauto. intros [i2 [s2' [INIT2' M2]]].
+  exploit (bsim_match_initial_states props); eauto. intros [i1 [s1' [INIT1' M1]]].
+  exists (i1, i2); exists s1'; intuition auto. eapply bb_match_at; eauto.
+- (* match final states *)
   intros i s1 s3 r MS SAFE FIN. inv MS.
-  exploit (bsim_match_final_states S23); eauto.
+  exploit (bsim_match_final_states props'); eauto.
     eapply star_safe; eauto. eapply bsim_safe; eauto.
   intros [s2' [A B]].
-  exploit bsim_E0_star. eapply star_trans. eexact H0. eexact A. auto. eauto. auto.
+  exploit (bsim_E0_star props). eapply star_trans. eexact H0. eexact A. auto. eauto. auto.
   intros [i1' [s1' [C D]]].
-  exploit (bsim_match_final_states S12); eauto. eapply star_safe; eauto.
+  exploit (bsim_match_final_states props); eauto. eapply star_safe; eauto.
   intros [s1'' [P Q]].
   exists s1''; split; auto. eapply star_trans; eauto.
-(* progress *)
+- (* progress *)
   intros i s1 s3 MS SAFE. inv MS.
-  eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto.
-(* simulation *)
-  exact bb_simulation.
-(* symbols *)
-  intros. transitivity (Senv.public_symbol (symbolenv L2) id); apply bsim_public_preserved; auto.
+  eapply (bsim_progress props'). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto.
+- (* simulation *)
+  apply bb_simulation; auto.
+- (* symbols *)
+  intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply bsim_public_preserved; eauto.
 Qed.
 
-End COMPOSE_BACKWARD_SIMULATIONS.
-
 (** ** Converting a forward simulation to a backward simulation *)
 
 Section FORWARD_TO_BACKWARD.
 
-Variable L1: semantics.
-Variable L2: semantics.
-Variable FS: forward_simulation L1 L2.
+Context L1 L2 index order match_states (FS: fsim_properties L1 L2 index order match_states).
 Hypothesis L1_receptive: receptive L1.
 Hypothesis L2_determinate: determinate L2.
 
@@ -1243,38 +1249,38 @@ Inductive f2b_transitions: state L1 -> state L2 -> Prop :=
       Star L1 s1 E0 s1' ->
       Step L1 s1' t s1'' ->
       Plus L2 s2 t s2' ->
-      FS i' s1' s2 ->
-      FS i'' s1'' s2' ->
+      match_states i' s1' s2 ->
+      match_states i'' s1'' s2' ->
       f2b_transitions s1 s2.
 
 Lemma f2b_progress:
-  forall i s1 s2, FS i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2.
+  forall i s1 s2, match_states i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2.
 Proof.
-  intros i0; pattern i0. apply well_founded_ind with (R := fsim_order FS).
-  apply fsim_order_wf.
+  intros i0; pattern i0. apply well_founded_ind with (R := order).
+  eapply fsim_order_wf; eauto.
   intros i REC s1 s2 MATCH SAFE.
   destruct (SAFE s1) as [[r FINAL] | [t [s1' STEP1]]]. apply star_refl.
-  (* final state reached *)
+- (* final state reached *)
   eapply f2b_trans_final; eauto.
   apply star_refl.
   eapply fsim_match_final_states; eauto.
-  (* L1 can make one step *)
+- (* L1 can make one step *)
   exploit (fsim_simulation FS); eauto. intros [i' [s2' [A MATCH']]].
-  assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ fsim_order FS i' i)).
-    intuition.
-    destruct (star_inv H0); intuition.
+  assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ order i' i)).
+    intuition auto.
+    destruct (star_inv H0); intuition auto.
   clear A. destruct B as [PLUS2 | [EQ1 [EQ2 ORDER]]].
-  eapply f2b_trans_step; eauto. apply star_refl.
-  subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto.
++ eapply f2b_trans_step; eauto. apply star_refl.
++ subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto.
   intros TRANS; inv TRANS.
-  eapply f2b_trans_final; eauto. eapply star_left; eauto.
-  eapply f2b_trans_step; eauto. eapply star_left; eauto.
+* eapply f2b_trans_final; eauto. eapply star_left; eauto.
+* eapply f2b_trans_step; eauto. eapply star_left; eauto.
 Qed.
 
 Lemma fsim_simulation_not_E0:
   forall s1 t s1', Step L1 s1 t s1' -> t <> E0 ->
-  forall i s2, FS i s1 s2 ->
-  exists i', exists s2', Plus L2 s2 t s2' /\ FS i' s1' s2'.
+  forall i s2, match_states i s1 s2 ->
+  exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2'.
 Proof.
   intros. exploit (fsim_simulation FS); eauto. intros [i' [s2' [A B]]].
   exists i'; exists s2'; split; auto.
@@ -1363,23 +1369,23 @@ Qed.
 
 Inductive f2b_match_states: f2b_index -> state L1 -> state L2 -> Prop :=
   | f2b_match_at: forall i s1 s2,
-      FS i s1 s2 ->
+      match_states i s1 s2 ->
       f2b_match_states (F2BI_after O) s1 s2
   | f2b_match_before: forall s1 t s1' s2b s2 n s2a i,
       Step L1 s1 t s1' ->  t <> E0 ->
       Star L2 s2b E0 s2 ->
       starN (step L2) (globalenv L2) n s2 t s2a ->
-      FS i s1 s2b ->
+      match_states i s1 s2b ->
       f2b_match_states (F2BI_before n) s1 s2
   | f2b_match_after: forall n s2 s2a s1 i,
       starN (step L2) (globalenv L2) (S n) s2 E0 s2a ->
-      FS i s1 s2a ->
+      match_states i s1 s2a ->
       f2b_match_states (F2BI_after (S n)) s1 s2.
 
 Remark f2b_match_after':
   forall n s2 s2a s1 i,
   starN (step L2) (globalenv L2) n s2 E0 s2a ->
-  FS i s1 s2a ->
+  match_states i s1 s2a ->
   f2b_match_states (F2BI_after n) s1 s2.
 Proof.
   intros. inv H.
@@ -1398,15 +1404,15 @@ Lemma f2b_simulation_step:
 Proof.
   intros s2 t s2' STEP2 i s1 MATCH SAFE.
   inv MATCH.
-(* 1. At matching states *)
+- (* 1. At matching states *)
   exploit f2b_progress; eauto. intros TRANS; inv TRANS.
-  (* 1.1  L1 can reach final state and L2 is at final state: impossible! *)
++ (* 1.1  L1 can reach final state and L2 is at final state: impossible! *)
   exploit (sd_final_nostep L2_determinate); eauto. contradiction.
-  (* 1.2  L1 can make 0 or several steps; L2 can make 1 or several matching steps. *)
++ (* 1.2  L1 can make 0 or several steps; L2 can make 1 or several matching steps. *)
   inv H2.
   exploit f2b_determinacy_inv. eexact H5. eexact STEP2.
   intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
-  (* 1.2.1  L2 makes a silent transition *)
+* (* 1.2.1  L2 makes a silent transition *)
   destruct (silent_or_not_silent t2).
   (* 1.2.1.1  L1 makes a silent transition too: perform transition now and go to "after" state *)
   subst. simpl in *. destruct (star_starN H6) as [n STEPS2].
@@ -1418,7 +1424,7 @@ Proof.
   exists (F2BI_before n); exists s1'; split.
   right; split. auto. constructor.
   econstructor. eauto. auto. apply star_one; eauto. eauto. eauto.
-  (* 1.2.2 L2 makes a non-silent transition, and so does L1 *)
+* (* 1.2.2 L2 makes a non-silent transition, and so does L1 *)
   exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
   congruence.
   subst t2. rewrite E0_right in H1.
@@ -1437,15 +1443,15 @@ Proof.
   left. eapply plus_right; eauto.
   eapply f2b_match_after'; eauto.
 
-(* 2. Before *)
+- (* 2. Before *)
   inv H2. congruence.
   exploit f2b_determinacy_inv. eexact H4. eexact STEP2.
   intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
-  (* 2.1 L2 makes a silent transition: remain in "before" state *)
++ (* 2.1 L2 makes a silent transition: remain in "before" state *)
   subst. simpl in *. exists (F2BI_before n0); exists s1; split.
   right; split. apply star_refl. constructor. omega.
   econstructor; eauto. eapply star_right; eauto.
-  (* 2.2 L2 make a non-silent transition *)
++ (* 2.2 L2 make a non-silent transition *)
   exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
   congruence.
   subst. rewrite E0_right in *.
@@ -1466,7 +1472,7 @@ Proof.
   left. apply plus_one; auto.
   eapply f2b_match_after'; eauto.
 
-(* 3. After *)
+- (* 3. After *)
   inv H. exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst.
   exploit f2b_determinacy_inv. eexact H2. eexact STEP2.
   intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
@@ -1476,20 +1482,28 @@ Proof.
   congruence.
 Qed.
 
+End FORWARD_TO_BACKWARD.
+
 (** The backward simulation *)
 
-Lemma forward_to_backward_simulation: backward_simulation L1 L2.
+Lemma forward_to_backward_simulation:
+  forall L1 L2,
+  forward_simulation L1 L2 -> receptive L1 -> determinate L2 ->
+  backward_simulation L1 L2.
 Proof.
-  apply Backward_simulation with (bsim_order := f2b_order) (bsim_match_states := f2b_match_states).
+  intros L1 L2 FS L1_receptive L2_determinate.
+  destruct FS as [index order match_states FS].
+  apply Backward_simulation with f2b_order (f2b_match_states L1 L2 match_states); constructor.
+- (* well founded *)
   apply wf_f2b_order.
-(* initial states exist *)
+- (* initial states exist *)
   intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2 [A B]]].
   exists s2; auto.
-(* initial states *)
+- (* initial states *)
   intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2' [A B]]].
   assert (s2 = s2') by (eapply sd_initial_determ; eauto). subst s2'.
   exists (F2BI_after O); exists s1; split; auto. econstructor; eauto.
-(* final states *)
+- (* final states *)
   intros. inv H.
   exploit f2b_progress; eauto. intros TRANS; inv TRANS.
   assert (r0 = r) by (eapply (sd_final_determ L2_determinate); eauto). subst r0.
@@ -1497,21 +1511,19 @@ Proof.
   inv H4. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
   inv H5. congruence. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
   inv H2. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
-(* progress *)
+- (* progress *)
   intros. inv H.
   exploit f2b_progress; eauto. intros TRANS; inv TRANS.
   left; exists r; auto.
   inv H3. right; econstructor; econstructor; eauto.
   inv H4. congruence. right; econstructor; econstructor; eauto.
   inv H1. right; econstructor; econstructor; eauto.
-(* simulation *)
-  exact f2b_simulation_step.
-(* symbols preserved *)
+- (* simulation *)
+  eapply f2b_simulation_step; eauto.
+- (* symbols preserved *)
   exact (fsim_public_preserved FS).
 Qed.
 
-End FORWARD_TO_BACKWARD.
-
 (** * Transforming a semantics into a single-event, equivalent semantics *)
 
 Definition well_behaved_traces (L: semantics) : Prop :=
@@ -1554,15 +1566,15 @@ Section FACTOR_FORWARD_SIMULATION.
 
 Variable L1: semantics.
 Variable L2: semantics.
-Variable sim: forward_simulation L1 L2.
+Context index order match_states (sim: fsim_properties L1 L2 index order match_states).
 Hypothesis L2single: single_events L2.
 
-Inductive ffs_match: fsim_index sim -> (trace * state L1) -> state L2 -> Prop :=
+Inductive ffs_match: index -> (trace * state L1) -> state L2 -> Prop :=
   | ffs_match_at: forall i s1 s2,
-      sim i s1 s2 ->
+      match_states i s1 s2 ->
       ffs_match i (E0, s1) s2
   | ffs_match_buffer: forall i ev t s1 s2 s2',
-      Star L2 s2 (ev :: t) s2' -> sim i s1 s2' ->
+      Star L2 s2 (ev :: t) s2' -> match_states i s1 s2' ->
       ffs_match i (ev :: t, s1) s2.
 
 Lemma star_non_E0_split':
@@ -1585,27 +1597,27 @@ Lemma ffs_simulation:
   forall s1 t s1', Step (atomic L1) s1 t s1' ->
   forall i s2, ffs_match i s1 s2 ->
   exists i', exists s2',
-     (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ fsim_order sim i' i)
+     (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ order i' i)
   /\ ffs_match i' s1' s2'.
 Proof.
   induction 1; intros.
-(* silent step *)
+- (* silent step *)
   inv H0.
   exploit (fsim_simulation sim); eauto.
   intros [i' [s2' [A B]]].
   exists i'; exists s2'; split. auto. constructor; auto.
-(* start step *)
+- (* start step *)
   inv H0.
   exploit (fsim_simulation sim); eauto.
   intros [i' [s2' [A B]]].
   destruct t as [ | ev' t].
-  (* single event *)
++ (* single event *)
   exists i'; exists s2'; split. auto. constructor; auto.
-  (* multiple events *)
++ (* multiple events *)
   assert (C: Star L2 s2 (ev :: ev' :: t) s2'). intuition. apply plus_star; auto.
   exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]].
   exists i'; exists s2x; split. auto. econstructor; eauto.
-(* continue step *)
+- (* continue step *)
   inv H0.
   exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]].
   destruct t.
@@ -1613,27 +1625,31 @@ Proof.
   exists i; exists s2x; split. auto. econstructor; eauto.
 Qed.
 
+End FACTOR_FORWARD_SIMULATION.
+
 Theorem factor_forward_simulation:
+  forall L1 L2,
+  forward_simulation L1 L2 -> single_events L2 ->
   forward_simulation (atomic L1) L2.
 Proof.
-  apply Forward_simulation with (fsim_match_states := ffs_match) (fsim_order := fsim_order sim).
-(* wf *)
-  apply fsim_order_wf.
-(* initial states *)
+  intros L1 L2 FS L2single. 
+  destruct FS as [index order match_states sim].
+  apply Forward_simulation with order (ffs_match L1 L2 match_states); constructor.
+- (* wf *)
+  eapply fsim_order_wf; eauto.
+- (* initial states *)
   intros. destruct s1 as [t1 s1]. simpl in H. destruct H. subst.
   exploit (fsim_match_initial_states sim); eauto. intros [i [s2 [A B]]].
   exists i; exists s2; split; auto. constructor; auto.
-(* final states *)
+- (* final states *)
   intros. destruct s1 as [t1 s1]. simpl in H0; destruct H0; subst. inv H.
   eapply (fsim_match_final_states sim); eauto.
-(* simulation *)
-  exact ffs_simulation.
-(* symbols preserved *)
+- (* simulation *)
+  eapply ffs_simulation; eauto.
+- (* symbols preserved *)
   simpl. exact (fsim_public_preserved sim).
 Qed.
 
-End FACTOR_FORWARD_SIMULATION.
-
 (** Likewise, a backward simulation from a single-event semantics [L1] to a semantics [L2]
   can be "factored" as a backward simulation from [L1] to [atomic L2]. *)
 
@@ -1641,13 +1657,13 @@ Section FACTOR_BACKWARD_SIMULATION.
 
 Variable L1: semantics.
 Variable L2: semantics.
-Variable sim: backward_simulation L1 L2.
+Context index order match_states (sim: bsim_properties L1 L2 index order match_states).
 Hypothesis L1single: single_events L1.
 Hypothesis L2wb: well_behaved_traces L2.
 
-Inductive fbs_match: bsim_index sim -> state L1 -> (trace * state L2) -> Prop :=
+Inductive fbs_match: index -> state L1 -> (trace * state L2) -> Prop :=
   | fbs_match_intro: forall i s1 t s2 s1',
-      Star L1 s1 t s1' -> sim i s1' s2 ->
+      Star L1 s1 t s1' -> match_states i s1' s2 ->
       t = E0 \/ output_trace t ->
       fbs_match i s1 (t, s2).
 
@@ -1655,18 +1671,18 @@ Lemma fbs_simulation:
   forall s2 t s2', Step (atomic L2) s2 t s2' ->
   forall i s1, fbs_match i s1 s2 -> safe L1 s1 ->
   exists i', exists s1',
-     (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order sim i' i))
+     (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ order i' i))
      /\ fbs_match i' s1' s2'.
 Proof.
   induction 1; intros.
-(* silent step *)
+- (* silent step *)
   inv H0.
   exploit (bsim_simulation sim); eauto. eapply star_safe; eauto.
   intros [i' [s1'' [A B]]].
   exists i'; exists s1''; split.
   destruct A as [P | [P Q]]. left. eapply star_plus_trans; eauto. right; split; auto. eapply star_trans; eauto.
   econstructor. apply star_refl. auto. auto.
-(* start step *)
+- (* start step *)
   inv H0.
   exploit (bsim_simulation sim); eauto. eapply star_safe; eauto.
   intros [i' [s1'' [A B]]].
@@ -1677,7 +1693,7 @@ Proof.
   left; auto.
   econstructor; eauto.
   exploit L2wb; eauto.
-(* continue step *)
+- (* continue step *)
   inv H0. unfold E0 in H8; destruct H8; try congruence.
   exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]].
   exists i; exists s1x; split. left; auto. econstructor; eauto. simpl in H0; tauto.
@@ -1690,47 +1706,51 @@ Lemma fbs_progress:
   (exists t, exists s2', Step (atomic L2) s2 t s2').
 Proof.
   intros. inv H. destruct t.
-(* 1. no buffered events *)
+- (* 1. no buffered events *)
   exploit (bsim_progress sim); eauto. eapply star_safe; eauto.
   intros [[r A] | [t [s2' A]]].
-(* final state *)
++ (* final state *)
   left; exists r; simpl; auto.
-(* L2 can step *)
++ (* L2 can step *)
   destruct t.
   right; exists E0; exists (nil, s2'). constructor. auto.
   right; exists (e :: nil); exists (t, s2'). constructor. auto.
-(* 2. some buffered events *)
+- (* 2. some buffered events *)
   unfold E0 in H3; destruct H3. congruence.
   right; exists (e :: nil); exists (t, s3). constructor. auto.
 Qed.
 
+End FACTOR_BACKWARD_SIMULATION.
+
 Theorem factor_backward_simulation:
+  forall L1 L2,
+  backward_simulation L1 L2 -> single_events L1 -> well_behaved_traces L2 ->
   backward_simulation L1 (atomic L2).
 Proof.
-  apply Backward_simulation with (bsim_match_states := fbs_match) (bsim_order := bsim_order sim).
-(* wf *)
-  apply bsim_order_wf.
-(* initial states exist *)
+  intros L1 L2 BS L1single L2wb. 
+  destruct BS as [index order match_states sim].
+  apply Backward_simulation with order (fbs_match L1 L2 match_states); constructor.
+- (* wf *)
+  eapply bsim_order_wf; eauto.
+- (* initial states exist *)
   intros. exploit (bsim_initial_states_exist sim); eauto. intros [s2 A].
   exists (E0, s2). simpl; auto.
-(* initial states match *)
+- (* initial states match *)
   intros. destruct s2 as [t s2]; simpl in H0; destruct H0; subst.
   exploit (bsim_match_initial_states sim); eauto. intros [i [s1' [A B]]].
   exists i; exists s1'; split. auto. econstructor. apply star_refl. auto. auto.
-(* final states match *)
+- (* final states match *)
   intros. destruct s2 as [t s2]; simpl in H1; destruct H1; subst.
   inv H. exploit (bsim_match_final_states sim); eauto. eapply star_safe; eauto.
   intros [s1'' [A B]]. exists s1''; split; auto. eapply star_trans; eauto.
-(* progress *)
-  exact fbs_progress.
-(* simulation *)
-  exact fbs_simulation.
-(* symbols *)
+- (* progress *)
+  eapply fbs_progress; eauto.
+- (* simulation *)
+  eapply fbs_simulation; eauto.
+- (* symbols *)
   simpl. exact (bsim_public_preserved sim).
 Qed.
 
-End FACTOR_BACKWARD_SIMULATION.
-
 (** Receptiveness of [atomic L]. *)
 
 Record strongly_receptive (L: semantics) : Prop :=