Merge branch 'master' into cleanup

8 files changed, 2166 insertions, 1966 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 39481bfb..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"
@@ -55,8 +56,8 @@ let rec print_builtin_arg px oc = function
   | BA x -> px oc x
   | BA_int n -> fprintf oc "int %ld" (camlint_of_coqint n)
   | BA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n)
-  | BA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n)
-  | BA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n)
+  | BA_float n -> fprintf oc "float %.15F" (camlfloat_of_coqfloat n)
+  | BA_single n -> fprintf oc "single %.15F" (camlfloat_of_coqfloat32 n)
   | BA_loadstack(chunk, ofs) ->
       fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs)
   | BA_addrstack(ofs) ->
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 :=