Merge pull request #93 from AbsInt/separate-compilation

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

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

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

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

1 files changed, 611 insertions, 509 deletions

diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 7c1b60a9..bb40a2d3 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -12,28 +12,67 @@
 
 (** Elimination of unreferenced static definitions *)
 
-Require Import FSets.
-Require Import Coqlib.
-Require Import Ordered.
-Require Import Maps.
-Require Import Iteration.
-Require Import AST.
-Require Import Errors.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import Smallstep.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
+Require Import FSets Coqlib Maps Ordered Iteration Errors.
+Require Import AST Linking.
+Require Import Integers Values Memory Globalenvs Events Smallstep.
+Require Import Op Registers RTL.
 Require Import Unusedglob.
 
 Module ISF := FSetFacts.Facts(IS).
 Module ISP := FSetProperties.Properties(IS).
 
-(** * Properties of the analysis *)
+(** * Relational specification of the transformation *)
+
+(** The transformed program is obtained from the original program
+  by keeping only the global definitions that belong to a given
+  set [u] of names.  *)
+
+Record match_prog_1 (u: IS.t) (p tp: program) : Prop := {
+  match_prog_main:
+    tp.(prog_main) = p.(prog_main);
+  match_prog_public:
+    tp.(prog_public) = p.(prog_public);
+  match_prog_def:
+    forall id,
+       (prog_defmap tp)!id = if IS.mem id u then (prog_defmap p)!id else None;
+  match_prog_unique:
+    list_norepet (prog_defs_names tp)
+}.
+
+(** This set [u] (as "used") must be closed under references, and
+  contain the entry point and the public identifiers of the program. *)
+
+Definition ref_function (f: function) (id: ident) : Prop :=
+  exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i).
+
+Definition ref_fundef (fd: fundef) (id: ident) : Prop :=
+  match fd with Internal f => ref_function f id | External ef => False end.
+
+Definition ref_init (il: list init_data) (id: ident) : Prop :=
+  exists ofs, In (Init_addrof id ofs) il.
+
+Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop :=
+  match gd with
+  | Gfun fd => ref_fundef fd id
+  | Gvar gv => ref_init gv.(gvar_init) id
+  end.
+
+Record valid_used_set (p: program) (u: IS.t) : Prop := {
+  used_closed: forall id gd id',
+    IS.In id u -> (prog_defmap p)!id = Some gd -> ref_def gd id' ->
+    IS.In id' u;
+  used_main:
+    IS.In p.(prog_main) u;
+  used_public: forall id,
+    In id p.(prog_public) -> IS.In id u;
+  used_defined: forall id,
+    IS.In id u -> In id (prog_defs_names p) \/ id = p.(prog_main)
+}.
+
+Definition match_prog (p tp: program) : Prop :=
+  exists u: IS.t, valid_used_set p u /\ match_prog_1 u p tp.
+
+(** * Properties of the static analysis *)
 
 (** Monotonic evolution of the workset. *)
 
@@ -123,7 +162,7 @@ Proof.
   eapply workset_incl_trans. 2: apply add_workset_incl.
   generalize {| w_seen := IS.empty; w_todo := nil |}. induction (prog_public p); simpl; intros.
   apply workset_incl_refl.
-  eapply workset_incl_trans. eapply add_workset_incl. eapply IHl.
+  eapply workset_incl_trans. apply add_workset_incl. apply IHl.
 Qed.
 
 (** Soundness properties for functions that add identifiers to the workset *)
@@ -148,9 +187,6 @@ Proof.
   apply IHl; auto.
 Qed.
 
-Definition ref_function (f: function) (id: ident) : Prop :=
-  exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i).
-
 Lemma seen_add_ref_function:
   forall id f w,
   ref_function f id -> IS.In id (add_ref_function f w).
@@ -164,15 +200,6 @@ Proof.
     apply H1. exists pc, i; auto.
 Qed.
 
-Definition ref_fundef (fd: fundef) (id: ident) : Prop :=
-  match fd with Internal f => ref_function f id | External ef => False end.
-
-Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop :=
-  match gd with
-  | Gfun fd => ref_fundef fd id
-  | Gvar gv => exists ofs, List.In (Init_addrof id ofs) gv.(gvar_init)
-  end.
-
 Lemma seen_add_ref_definition:
   forall pm id gd id' w,
   pm!id = Some gd -> ref_def gd id' -> IS.In id' (add_ref_definition pm id w).
@@ -198,7 +225,7 @@ Qed.
 Lemma seen_main_initial_workset:
   forall p, IS.In p.(prog_main) (initial_workset p).
 Proof.
-  unfold initial_workset; intros. apply seen_add_workset.
+  intros. apply seen_add_workset.
 Qed.
 
 Lemma seen_public_initial_workset:
@@ -217,19 +244,14 @@ Proof.
   apply H0. auto.
 Qed.
 
-(** * Semantic preservation *)
+(** * Correctness of the transformation with respect to the relational specification *)
 
-Section SOUNDNESS.
-Variable p: program.
-Variable tp: program.
-Hypothesis TRANSF: transform_program p = OK tp.
-Let ge := Genv.globalenv p.
-Let tge := Genv.globalenv tp.
-
-Let pm := program_map p.
+(** Correctness of the dependency graph traversal. *)
 
+Section ANALYSIS.
 
-(** Correctness of the dependency graph traversal. *)
+Variable p: program.
+Let pm := prog_defmap p.
 
 Definition workset_invariant (w: workset) : Prop :=
   forall id gd id',
@@ -264,7 +286,7 @@ Proof.
 Qed.
 
 Theorem used_globals_sound:
-  forall u, used_globals p = Some u -> used_set_closed u.
+  forall u, used_globals p pm = Some u -> used_set_closed u.
 Proof.
   unfold used_globals; intros. eapply PrimIter.iterate_prop with (P := workset_invariant); eauto.
 - intros. apply iter_step_invariant; auto.
@@ -275,7 +297,7 @@ Proof.
 Qed.
 
 Theorem used_globals_incl:
-  forall u, used_globals p = Some u -> IS.Subset (initial_workset p) u.
+  forall u, used_globals p pm = Some u -> IS.Subset (initial_workset p) u.
 Proof.
   unfold used_globals; intros.
   eapply PrimIter.iterate_prop with (P := fun (w: workset) => IS.Subset (initial_workset p) w); eauto.
@@ -286,35 +308,34 @@ Proof.
 - red; auto.
 Qed.
 
-Definition used: IS.t :=
-  match used_globals p with Some u => u | None => IS.empty end.
-
-Remark USED_GLOBALS: used_globals p = Some used.
+Corollary used_globals_valid:
+  forall u,
+  used_globals p pm = Some u ->
+  IS.for_all (global_defined p pm) u = true ->
+  valid_used_set p u.
 Proof.
-  unfold used. unfold transform_program in TRANSF. destruct (used_globals p). auto. discriminate.
+  intros. constructor.
+- intros. eapply used_globals_sound; eauto. 
+- eapply used_globals_incl; eauto. apply seen_main_initial_workset.
+- intros. eapply used_globals_incl; eauto. apply seen_public_initial_workset; auto.
+- intros. apply ISF.for_all_iff in H0.
++ red in H0. apply H0 in H1. unfold global_defined in H1. 
+  destruct pm!id as [g|] eqn:E.
+* left. change id with (fst (id,g)). apply in_map. apply in_prog_defmap; auto.
+* InvBooleans; auto.
++ hnf. simpl; intros; congruence.
 Qed.
 
-Definition kept (id: ident) : Prop := IS.In id used.
+End ANALYSIS.
 
-Theorem kept_closed:
-  forall id gd id',
-  kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'.
-Proof.
-  intros. assert (UC: used_set_closed used) by (apply used_globals_sound; apply USED_GLOBALS).
-  eapply UC; eauto.
-Qed.
+(** Properties of the elimination of unused global definitions. *)
 
-Theorem kept_main:
-  kept p.(prog_main).
-Proof.
-  unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_main_initial_workset.
-Qed.
+Section TRANSFORMATION.
 
-Theorem kept_public:
-  forall id, In id p.(prog_public) -> kept id.
-Proof.
-  intros. unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_public_initial_workset; auto.
-Qed.
+Variable p: program.
+Variable used: IS.t.
+
+Let add_def (m: prog_map) idg := PTree.set (fst idg) (snd idg) m.
 
 Remark filter_globdefs_accu:
   forall defs accu1 accu2 u,
@@ -333,98 +354,154 @@ Proof.
   intros. rewrite <- filter_globdefs_accu. auto.
 Qed.
 
-Theorem transform_program_charact:
-  forall id, (program_map tp)!id = if IS.mem id used then pm!id else None.
+Lemma filter_globdefs_map_1:
+  forall id l u m1,
+  IS.mem id u = false ->
+  m1!id = None ->
+  (fold_left add_def (filter_globdefs u nil l) m1)!id = None.
 Proof.
-  intros.
-  assert (X: forall l u m1 m2,
-             IS.In id u ->
-             m1!id = m2!id ->
-             (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id =
-             (fold_left add_def_prog_map (List.rev l) m2)!id).
-  {
-    induction l; simpl; intros.
-    auto.
-    destruct a as [id1 gd1]. rewrite fold_left_app. simpl.
-    destruct (IS.mem id1 u) eqn:MEM.
-    rewrite filter_globdefs_nil. rewrite fold_left_app. simpl.
-    unfold add_def_prog_map at 1 3. simpl.
-    rewrite ! PTree.gsspec. destruct (peq id id1). auto.
-    apply IHl; auto. apply IS.remove_2; auto.
-    unfold add_def_prog_map at 2. simpl. rewrite PTree.gso. apply IHl; auto.
-    red; intros; subst id1.
-    assert (IS.mem id u = true) by (apply IS.mem_1; auto). congruence.
-  }
-  assert (Y: forall l u m1,
-             IS.mem id u = false ->
-             m1!id = None ->
-             (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id = None).
-  {
-    induction l; simpl; intros.
-    auto.
-    destruct a as [id1 gd1].
-    destruct (IS.mem id1 u) eqn:MEM.
-    rewrite filter_globdefs_nil. rewrite fold_left_app. simpl.
-    unfold add_def_prog_map at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto.
-    rewrite ISF.remove_b. rewrite H; auto.
-    eapply IHl; eauto.
-  }
-  unfold pm, program_map.
-  unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF. inversion TRANSF.
-  simpl. destruct (IS.mem id used) eqn: MEM.
-  erewrite X. rewrite List.rev_involutive. eauto. apply IS.mem_2; auto. auto.
-  apply Y. auto. apply PTree.gempty.
-Qed.
-
-(** Program map and Genv operations *)
-
-Definition genv_progmap_match (ge: genv) (pm: prog_map) : Prop :=
-  forall id,
-  match Genv.find_symbol ge id with
-  | None => pm!id = None
-  | Some b =>
-      match pm!id with
-      | None => False
-      | Some (Gfun fd) => Genv.find_funct_ptr ge b = Some fd
-      | Some (Gvar gv) => Genv.find_var_info ge b = Some gv
-      end
-  end.
+  induction l as [ | [id1 gd1] l]; simpl; intros.
+- auto.
+- destruct (IS.mem id1 u) eqn:MEM.
++ rewrite filter_globdefs_nil. rewrite fold_left_app. simpl.
+  unfold add_def at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto.
+  rewrite ISF.remove_b. rewrite H; auto.
++ eapply IHl; eauto.
+Qed.
 
-Lemma genv_program_map:
-  forall p, genv_progmap_match (Genv.globalenv p) (program_map p).
+Lemma filter_globdefs_map_2:
+  forall id l u m1 m2,
+  IS.mem id u = true ->
+  m1!id = m2!id ->
+  (fold_left add_def (filter_globdefs u nil l) m1)!id = (fold_left add_def (List.rev l) m2)!id.
 Proof.
-  intros. unfold Genv.globalenv, program_map.
-  assert (REC: forall defs g m,
-               genv_progmap_match g m ->
-               genv_progmap_match (Genv.add_globals g defs) (fold_left add_def_prog_map defs m)).
-  {
-    induction defs; simpl; intros.
-    auto.
-    apply IHdefs. red; intros. specialize (H id).
-    destruct a as [id1 [fd|gv]];
-    unfold Genv.add_global, Genv.find_symbol, Genv.find_funct_ptr, Genv.find_var_info, add_def_prog_map in *;
-    simpl.
-  - rewrite PTree.gsspec. destruct (peq id id1); subst.
-    + rewrite ! PTree.gss. auto.
-    + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto.
-      * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto.
-      * auto.
-  - rewrite PTree.gsspec. destruct (peq id id1); subst.
-    + rewrite ! PTree.gss. auto.
-    + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto.
-      * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto.
-      * auto.
-  }
-  apply REC. red; intros. unfold Genv.find_symbol, Genv.empty_genv; simpl. rewrite ! PTree.gempty; auto.
+  induction l as [ | [id1 gd1] l]; simpl; intros.
+- auto.
+- rewrite fold_left_app. simpl.
+  destruct (IS.mem id1 u) eqn:MEM.
++ rewrite filter_globdefs_nil. rewrite fold_left_app. simpl.
+  unfold add_def at 1 3. simpl.
+  rewrite ! PTree.gsspec. destruct (peq id id1). auto.
+  apply IHl; auto.
+  apply IS.mem_1. apply IS.remove_2; auto. apply IS.mem_2; auto.
++ unfold add_def at 2. simpl. rewrite PTree.gso by congruence. apply IHl; auto.
 Qed.
 
-Lemma transform_program_kept:
-  forall id b, Genv.find_symbol tge id = Some b -> kept id.
+Lemma filter_globdefs_map:
+  forall id u defs,
+  (PTree_Properties.of_list (filter_globdefs u nil (List.rev defs)))! id =
+  if IS.mem id u then (PTree_Properties.of_list defs)!id else None.
 Proof.
-  intros. generalize (genv_program_map tp id). fold tge; rewrite H.
-  rewrite transform_program_charact. intros. destruct (IS.mem id used) eqn:U.
-  unfold kept; apply IS.mem_2; auto.
-  contradiction.
+  intros. unfold PTree_Properties.of_list. fold prog_map. unfold PTree.elt. fold add_def.
+  destruct (IS.mem id u) eqn:MEM.
+- erewrite filter_globdefs_map_2. rewrite List.rev_involutive. reflexivity. 
+  auto. auto.
+- apply filter_globdefs_map_1. auto. apply PTree.gempty.
+Qed.
+
+Lemma filter_globdefs_domain:
+  forall id l u,
+  In id (map fst (filter_globdefs u nil l)) -> IS.In id u /\ In id (map fst l).
+Proof.
+  induction l as [ | [id1 gd1] l]; simpl; intros.
+- tauto.
+- destruct (IS.mem id1 u) eqn:MEM.
++ rewrite filter_globdefs_nil, map_app, in_app_iff in H. destruct H.
+  apply IHl in H. rewrite ISF.remove_iff in H. tauto.
+  simpl in H. destruct H; try tauto. subst id1. split; auto. apply IS.mem_2; auto.
++ apply IHl in H. tauto.
+Qed.
+
+Lemma filter_globdefs_unique_names:
+  forall l u, list_norepet (map fst (filter_globdefs u nil l)).
+Proof.
+  induction l as [ | [id1 gd1] l]; simpl; intros.
+- constructor.
+- destruct (IS.mem id1 u) eqn:MEM; auto.
+  rewrite filter_globdefs_nil, map_app. simpl.
+  apply list_norepet_append; auto. 
+  constructor. simpl; tauto. constructor.
+  red; simpl; intros. destruct H0; try tauto. subst y.
+  apply filter_globdefs_domain in H. rewrite ISF.remove_iff in H. intuition.
+Qed.
+
+End TRANSFORMATION.
+
+Theorem transf_program_match:
+  forall p tp, transform_program p = OK tp -> match_prog p tp.
+Proof.
+  unfold transform_program; intros p tp TR. set (pm := prog_defmap p) in *.
+  destruct (used_globals p pm) as [u|] eqn:U; try discriminate.
+  destruct (IS.for_all (global_defined p pm) u) eqn:DEF; inv TR.
+  exists u; split. 
+  apply used_globals_valid; auto.
+  constructor; simpl; auto.
+  intros. unfold prog_defmap; simpl. apply filter_globdefs_map.
+  apply filter_globdefs_unique_names. 
+Qed.
+
+(** * Semantic preservation *)
+
+Section SOUNDNESS.
+
+Variable p: program.
+Variable tp: program.
+Variable used: IS.t.
+Hypothesis USED_VALID: valid_used_set p used.
+Hypothesis TRANSF: match_prog_1 used p tp.
+Let ge := Genv.globalenv p.
+Let tge := Genv.globalenv tp.
+Let pm := prog_defmap p.
+
+Definition kept (id: ident) : Prop := IS.In id used.
+
+Lemma kept_closed:
+  forall id gd id',
+  kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'.
+Proof.
+  intros. eapply used_closed; eauto.
+Qed.
+
+Lemma kept_main:
+  kept p.(prog_main).
+Proof.
+  eapply used_main; eauto.
+Qed.
+
+Lemma kept_public:
+  forall id, In id p.(prog_public) -> kept id.
+Proof.
+  intros. eapply used_public; eauto.
+Qed.
+
+(** Relating [Genv.find_symbol] operations in the original and transformed program *)
+
+Lemma transform_find_symbol_1:
+  forall id b,
+  Genv.find_symbol ge id = Some b -> kept id -> exists b', Genv.find_symbol tge id = Some b'.
+Proof.
+  intros. 
+  assert (A: exists g, (prog_defmap p)!id = Some g).
+  { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. }
+  destruct A as (g & P).
+  apply Genv.find_symbol_exists with g.
+  apply in_prog_defmap.
+  erewrite match_prog_def by eauto. rewrite IS.mem_1 by auto. auto.
+Qed.
+
+Lemma transform_find_symbol_2:
+  forall id b,
+  Genv.find_symbol tge id = Some b -> kept id /\ exists b', Genv.find_symbol ge id = Some b'.
+Proof.
+  intros. 
+  assert (A: exists g, (prog_defmap tp)!id = Some g).
+  { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. }
+  destruct A as (g & P).
+  erewrite match_prog_def in P by eauto. 
+  destruct (IS.mem id used) eqn:U; try discriminate.
+  split. apply IS.mem_2; auto. 
+  apply Genv.find_symbol_exists with g.
+  apply in_prog_defmap. auto.
 Qed.
 
 (** Injections that preserve used globals. *)
@@ -439,16 +516,13 @@ Record meminj_preserves_globals (f: meminj) : Prop := {
   symbols_inject_3: forall id b',
     Genv.find_symbol tge id = Some b' ->
     exists b, Genv.find_symbol ge id = Some b /\ f b = Some(b', 0);
-  funct_ptr_inject: forall b b' delta fd,
-    f b = Some(b', delta) -> Genv.find_funct_ptr ge b = Some fd ->
-    Genv.find_funct_ptr tge b' = Some fd /\ delta = 0 /\
-    (forall id, ref_fundef fd id -> kept id);
-  var_info_inject: forall b b' delta gv,
-    f b = Some(b', delta) -> Genv.find_var_info ge b = Some gv ->
-    Genv.find_var_info tge b' = Some gv /\ delta = 0;
-  var_info_rev_inject: forall b b' delta gv,
-    f b = Some(b', delta) -> Genv.find_var_info tge b' = Some gv ->
-    Genv.find_var_info ge b = Some gv /\ delta = 0
+  defs_inject: forall b b' delta gd,
+    f b = Some(b', delta) -> Genv.find_def ge b = Some gd ->
+    Genv.find_def tge b' = Some gd /\ delta = 0 /\
+    (forall id, ref_def gd id -> kept id);
+  defs_rev_inject: forall b b' delta gd,
+    f b = Some(b', delta) -> Genv.find_def tge b' = Some gd ->
+    Genv.find_def ge b = Some gd /\ delta = 0
 }.
 
 Definition init_meminj : meminj :=
@@ -462,6 +536,14 @@ Definition init_meminj : meminj :=
     | None => None
     end.
 
+Remark init_meminj_eq:
+  forall id b b',
+  Genv.find_symbol ge id = Some b -> Genv.find_symbol tge id = Some b' ->
+  init_meminj b = Some(b', 0).
+Proof.
+  intros. unfold init_meminj. erewrite Genv.find_invert_symbol by eauto. rewrite H0. auto.
+Qed.
+
 Remark init_meminj_invert:
   forall b b' delta,
   init_meminj b = Some(b', delta) ->
@@ -480,44 +562,26 @@ Proof.
 - exploit init_meminj_invert; eauto. intros (A & id1 & B & C).
   assert (id1 = id) by (eapply (Genv.genv_vars_inj ge); eauto). subst id1.
   auto.
-- unfold init_meminj. erewrite Genv.find_invert_symbol by eauto. apply IS.mem_1 in H.
-  generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
-  rewrite transform_program_charact. rewrite H, H0.
-  destruct (Genv.find_symbol tge id) as [b'|]; intros.
-  exists b'; auto. rewrite H2 in H1; contradiction.
-- generalize (genv_program_map tp id). fold tge. rewrite H. intros.
-  destruct (program_map tp)!id as [gd|] eqn:PM; try contradiction.
-  generalize (transform_program_charact id). rewrite PM.
-  destruct (IS.mem id used) eqn:USED; intros; try discriminate.
-  generalize (genv_program_map p id). fold ge; fold pm.
-  destruct (Genv.find_symbol ge id) as [b|] eqn:FS; intros; try congruence.
-  exists b; split; auto. unfold init_meminj.
-  erewrite Genv.find_invert_symbol by eauto. rewrite H. auto.
+- exploit transform_find_symbol_1; eauto. intros (b' & F). exists b'; split; auto.
+  eapply init_meminj_eq; eauto.
+- exploit transform_find_symbol_2; eauto. intros (K & b & F). 
+  exists b; split; auto. eapply init_meminj_eq; eauto.
+- exploit init_meminj_invert; eauto. intros (A & id & B & C).
+  assert (kept id) by (eapply transform_find_symbol_2; eauto).
+  assert (pm!id = Some gd).
+  { unfold pm; rewrite Genv.find_def_symbol. exists b; auto. }
+  assert ((prog_defmap tp)!id = Some gd).
+  { erewrite match_prog_def by eauto. rewrite IS.mem_1 by auto. auto. }
+  rewrite Genv.find_def_symbol in H3. destruct H3 as (b1 & P & Q).
+  fold tge in P. replace b' with b1 by congruence. split; auto. split; auto. 
+  intros. eapply kept_closed; eauto.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C).
-  generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
-  rewrite transform_program_charact. rewrite B, C. intros.
-  destruct (IS.mem id used) eqn:KEPT; try contradiction.
-  destruct (pm!id) as [gd|] eqn:PM; try contradiction.
-  destruct gd as [fd'|gv'].
-  + assert (fd' = fd) by congruence. subst fd'. split. auto. split. auto.
-    intros. eapply kept_closed; eauto. red; apply IS.mem_2; auto.
-  + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence.
-- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto.
-  generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
-  rewrite transform_program_charact. rewrite B, C. intros.
-  destruct (IS.mem id used); try contradiction.
-  destruct (pm!id) as [gd|]; try contradiction.
-  destruct gd as [fd'|gv'].
-  + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence.
-  + congruence.
-- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto.
-  generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
-  rewrite transform_program_charact. rewrite B, C. intros.
-  destruct (IS.mem id used); try contradiction.
-  destruct (pm!id) as [gd|]; try contradiction.
-  destruct gd as [fd'|gv'].
-  + assert (b' <> b') by (eapply Genv.genv_funs_vars; eassumption). congruence.
-  + congruence.
+  assert ((prog_defmap tp)!id = Some gd).
+  { rewrite Genv.find_def_symbol. exists b'; auto. }
+  erewrite match_prog_def in H1 by eauto.
+  destruct (IS.mem id used); try discriminate.
+  rewrite Genv.find_def_symbol in H1. destruct H1 as (b1 & P & Q).
+  fold ge in P. replace b with b1 by congruence. auto.
 Qed.
 
 Lemma globals_symbols_inject:
@@ -527,28 +591,33 @@ Proof.
   assert (E1: Genv.genv_public ge = p.(prog_public)).
   { apply Genv.globalenv_public. }
   assert (E2: Genv.genv_public tge = p.(prog_public)).
-  { unfold tge; rewrite Genv.globalenv_public.
-    unfold transform_program in TRANSF. rewrite USED_GLOBALS in TRANSF. inversion TRANSF. auto. }
+  { unfold tge; rewrite Genv.globalenv_public. eapply match_prog_public; eauto. }
   split; [|split;[|split]]; intros.
   + simpl; unfold Genv.public_symbol; rewrite E1, E2.
     destruct (Genv.find_symbol tge id) as [b'|] eqn:TFS.
     exploit symbols_inject_3; eauto. intros (b & FS & INJ). rewrite FS. auto.
     destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
     destruct (in_dec ident_eq id (prog_public p)); simpl; auto.
-    exploit symbols_inject_2; eauto. apply kept_public; auto.
+    exploit symbols_inject_2; eauto.
+    eapply kept_public; eauto.
     intros (b' & TFS' & INJ). congruence.
   + eapply symbols_inject_1; eauto.
   + simpl in *; unfold Genv.public_symbol in H0.
     destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
     rewrite E1 in H0.
     destruct (in_dec ident_eq id (prog_public p)); try discriminate. inv H1.
-    exploit symbols_inject_2; eauto. apply kept_public; auto.
+    exploit symbols_inject_2; eauto.
+    eapply kept_public; eauto.
     intros (b' & A & B); exists b'; auto.
   + simpl. unfold Genv.block_is_volatile.
     destruct (Genv.find_var_info ge b1) as [gv|] eqn:V1.
-    exploit var_info_inject; eauto. intros [A B]. rewrite A. auto.
+    rewrite Genv.find_var_info_iff in V1.
+    exploit defs_inject; eauto. intros (A & B & C).
+    rewrite <- Genv.find_var_info_iff in A. rewrite A; auto.
     destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto.
-    exploit var_info_rev_inject; eauto. intros [A B]. congruence.
+    rewrite Genv.find_var_info_iff in V2.
+    exploit defs_rev_inject; eauto. intros (A & B). 
+    rewrite <- Genv.find_var_info_iff in A. congruence.
 Qed.
 
 Lemma symbol_address_inject:
@@ -661,12 +730,10 @@ Proof.
     exists b'; auto.
   + exploit symbols_inject_3; eauto. intros (b & A & B).
     exists b; auto.
-  + eapply funct_ptr_inject; eauto. apply SAME; auto.
-    eapply Genv.genv_funs_range; eauto.
-  + eapply var_info_inject; eauto. apply SAME; auto.
-    eapply Genv.genv_vars_range; eauto.
-  + eapply var_info_rev_inject; eauto. apply SAME'; auto.
-    eapply Genv.genv_vars_range; eauto.
+  + eapply defs_inject; eauto. apply SAME; auto.
+    eapply Genv.genv_defs_range; eauto.
+  + eapply defs_rev_inject; eauto. apply SAME'; auto.
+    eapply Genv.genv_defs_range; eauto.
 - econstructor; eauto.
   apply IHmatch_stacks.
   intros. exploit H1; eauto. intros [A B]. split; eapply Ple_trans; eauto.
@@ -738,11 +805,15 @@ Proof.
 - exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0.
   rewrite Genv.find_funct_find_funct_ptr in H0.
   specialize (H1 r). rewrite R in H1. inv H1.
-  exploit funct_ptr_inject; eauto. intros (A & B & C).
+  rewrite Genv.find_funct_ptr_iff in H0.  
+  exploit defs_inject; eauto. intros (A & B & C).
+  rewrite <- Genv.find_funct_ptr_iff in A. 
   rewrite B; auto.
 - destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
   exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P.
-  exploit funct_ptr_inject; eauto. intros (A & B & C).
+  rewrite Genv.find_funct_ptr_iff in H0.  
+  exploit defs_inject; eauto. intros (A & B & C).
+  rewrite <- Genv.find_funct_ptr_iff in A. 
   auto.
 Qed.
 
@@ -973,285 +1044,159 @@ Qed.
 
 (** Relating initial memory states *)
 
-Remark init_meminj_no_overlap:
-  forall m, Mem.meminj_no_overlap init_meminj m.
+(*
+Remark genv_find_def_exists:
+  forall (F V: Type) (p: AST.program F V) b,
+  Plt b (Genv.genv_next (Genv.globalenv p)) ->
+  exists gd, Genv.find_def (Genv.globalenv p) b = Some gd.
 Proof.
-  intros; red; intros.
-  exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1).
-  exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2).
-  left; red; intros; subst b2'.
-  assert (id1 = id2) by (eapply Genv.genv_vars_inj; eauto).
-  congruence.
+  intros until b.
+  set (P := fun (g: Genv.t F V) =>
+        Plt b (Genv.genv_next g) -> exists gd, (Genv.genv_defs g)!b = Some gd).
+  assert (forall l g, P g -> P (Genv.add_globals g l)).
+  { induction l as [ | [id1 g1] l]; simpl; intros.
+  - auto.
+  - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT.
+  + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto. 
+  + rewrite H0. rewrite PTree.gss. exists g1; auto. }
+  apply H. red; simpl; intros. exfalso; xomega.
 Qed.
+*)
 
-Lemma store_zeros_unmapped_inj:
-  forall m1 b1 i n m1',
-  store_zeros m1 b1 i n = Some m1' ->
-  forall m2,
-  Mem.mem_inj init_meminj m1 m2 ->
-  init_meminj b1 = None ->
-  Mem.mem_inj init_meminj m1' m2.
-Proof.
-  intros until m1'. functional induction (store_zeros m1 b1 i n); intros.
-  inv H. auto.
-  eapply IHo; eauto. eapply Mem.store_unmapped_inj; eauto.
-  discriminate.
-Qed.
-
-Lemma store_zeros_mapped_inj:
-  forall m1 b1 i n m1',
-  store_zeros m1 b1 i n = Some m1' ->
-  forall m2 b2,
-  Mem.mem_inj init_meminj m1 m2 ->
-  init_meminj b1 = Some(b2, 0) ->
-  exists m2', store_zeros m2 b2 i n = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
-Proof.
-  intros until m1'. functional induction (store_zeros m1 b1 i n); intros.
-  inv H. exists m2; split; auto. rewrite store_zeros_equation, e; auto.
-  exploit Mem.store_mapped_inj; eauto. apply init_meminj_no_overlap. instantiate (1 := Vzero); constructor.
-  intros (m2' & A & B). rewrite Zplus_0_r in A.
-  exploit IHo; eauto. intros (m3' & C & D).
-  exists m3'; split; auto. rewrite store_zeros_equation, e, A, C; auto.
-  discriminate.
-Qed.
-
-Lemma store_init_data_unmapped_inj:
-  forall m1 b1 i id m1' m2,
-  Genv.store_init_data ge m1 b1 i id = Some m1' ->
-  Mem.mem_inj init_meminj m1 m2 ->
-  init_meminj b1 = None ->
-  Mem.mem_inj init_meminj m1' m2.
-Proof.
-  intros. destruct id; simpl in H; try (eapply Mem.store_unmapped_inj; now eauto).
-  inv H; auto.
-  destruct (Genv.find_symbol ge i0); try discriminate. eapply Mem.store_unmapped_inj; now eauto.
-Qed.
-
-Lemma store_init_data_mapped_inj:
-  forall m1 b1 i init m1' b2 m2,
-  Genv.store_init_data ge m1 b1 i init = Some m1' ->
-  Mem.mem_inj init_meminj m1 m2 ->
-  init_meminj b1 = Some(b2, 0) ->
-  (forall id ofs, init = Init_addrof id ofs -> kept id) ->
-  exists m2', Genv.store_init_data tge m2 b2 i init = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
-Proof.
-  intros. replace i with (i + 0) by omega. pose proof (init_meminj_no_overlap m1).
-  destruct init; simpl in *; try (eapply Mem.store_mapped_inj; now eauto).
-  inv H. exists m2; auto.
-  destruct (Genv.find_symbol ge i0) as [bi|] eqn:FS1; try discriminate.
-  exploit symbols_inject_2. eapply init_meminj_preserves_globals. eapply H2; eauto. eauto.
-  intros (bi' & A & B). rewrite A. eapply Mem.store_mapped_inj; eauto.
-  econstructor; eauto. rewrite Int.add_zero; auto.
+Lemma init_meminj_invert_strong:
+  forall b b' delta,
+  init_meminj b = Some(b', delta) ->
+  delta = 0 /\
+  exists id gd,
+     Genv.find_symbol ge id = Some b
+  /\ Genv.find_symbol tge id = Some b'
+  /\ Genv.find_def ge b = Some gd
+  /\ Genv.find_def tge b' = Some gd
+  /\ (forall i, ref_def gd i -> kept i).
+Proof.
+  intros. exploit init_meminj_invert; eauto. intros (A & id & B & C). 
+  assert (exists gd, (prog_defmap p)!id = Some gd).
+  { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. }
+  destruct H0 as [gd DM]. rewrite Genv.find_def_symbol in DM.
+  destruct DM as (b'' & P & Q). fold ge in P. rewrite P in B; inv B.
+  fold ge in Q. exploit defs_inject. apply init_meminj_preserves_globals.
+  eauto. eauto. intros (X & _ & Y). 
+  split. auto. exists id, gd; auto. 
 Qed.
 
- Lemma store_init_data_list_unmapped_inj:
-  forall initlist m1 b1 i m1' m2,
-  Genv.store_init_data_list ge m1 b1 i initlist = Some m1' ->
-  Mem.mem_inj init_meminj m1 m2 ->
-  init_meminj b1 = None ->
-  Mem.mem_inj init_meminj m1' m2.
-Proof.
-  induction initlist; simpl; intros.
-- inv H; auto.
-- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate.
-  eapply IHinitlist; eauto. eapply store_init_data_unmapped_inj; eauto.
-Qed.
-
-Lemma store_init_data_list_mapped_inj:
-  forall initlist m1 b1 i m1' b2 m2,
-  Genv.store_init_data_list ge m1 b1 i initlist = Some m1' ->
-  Mem.mem_inj init_meminj m1 m2 ->
-  init_meminj b1 = Some(b2, 0) ->
-  (forall id ofs, In (Init_addrof id ofs) initlist -> kept id) ->
-  exists m2', Genv.store_init_data_list tge m2 b2 i initlist = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
-Proof.
-  induction initlist; simpl; intros.
-- inv H. exists m2; auto.
-- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate.
-  exploit store_init_data_mapped_inj; eauto. intros (m2'' & A & B).
-  exploit IHinitlist; eauto. intros (m2' & C & D).
-  exists m2'; split; auto. rewrite A; auto.
-Qed.
-
-Lemma alloc_global_unmapped_inj:
-  forall m1 id g m1' m2,
-  Genv.alloc_global ge m1 (id, g) = Some m1' ->
-  Mem.mem_inj init_meminj m1 m2 ->
-  init_meminj (Mem.nextblock m1) = None ->
-  Mem.mem_inj init_meminj m1' m2.
-Proof.
-  unfold Genv.alloc_global; intros. destruct g as [fd|gv].
-- destruct (Mem.alloc m1 0 1) as (m1a, b) eqn:ALLOC.
-  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1.
-  eapply Mem.drop_unmapped_inj with (m1 := m1a); eauto.
-  eapply Mem.alloc_left_unmapped_inj; eauto.
-- set (sz := Genv.init_data_list_size (gvar_init gv)) in *.
-  destruct (Mem.alloc m1 0 sz) as (m1a, b) eqn:ALLOC.
-  destruct (store_zeros m1a b 0 sz) as [m1b|] eqn: STZ; try discriminate.
-  destruct (Genv.store_init_data_list ge m1b b 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate.
-  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1.
-  eapply Mem.drop_unmapped_inj with (m1 := m1c); eauto.
-  eapply store_init_data_list_unmapped_inj with (m1 := m1b); eauto.
-  eapply store_zeros_unmapped_inj with (m1 := m1a); eauto.
-  eapply Mem.alloc_left_unmapped_inj; eauto.
-Qed.
-
-Lemma alloc_global_mapped_inj:
-  forall m1 id g m1' m2,
-  Genv.alloc_global ge m1 (id, g) = Some m1' ->
-  Mem.mem_inj init_meminj m1 m2 ->
-  init_meminj (Mem.nextblock m1) = Some(Mem.nextblock m2, 0) ->
-  (forall id, ref_def g id -> kept id) ->
-  exists m2',
-    Genv.alloc_global tge m2 (id, g) = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
-Proof.
-  unfold Genv.alloc_global; intros. destruct g as [fd|gv].
-- destruct (Mem.alloc m1 0 1) as (m1a, b1) eqn:ALLOC.
-  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1.
-  destruct (Mem.alloc m2 0 1) as (m2a, b2) eqn:ALLOC2.
-  exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1.
-  assert (Mem.mem_inj init_meminj m1a m2a).
-  { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0).
-    eapply Mem.alloc_right_inj; eauto.
-    eauto.
-    eauto with mem.
-    red; intros; apply Z.divide_0_r.
-    intros. apply Mem.perm_implies with Freeable; auto with mem.
-    eapply Mem.perm_alloc_2; eauto. omega.
-    auto.
-  }
-  exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap.
-- set (sz := Genv.init_data_list_size (gvar_init gv)) in *.
-  destruct (Mem.alloc m1 0 sz) as (m1a, b1) eqn:ALLOC.
-  destruct (store_zeros m1a b1 0 sz) as [m1b|] eqn: STZ; try discriminate.
-  destruct (Genv.store_init_data_list ge m1b b1 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate.
-  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1.
-  destruct (Mem.alloc m2 0 sz) as (m2a, b2) eqn:ALLOC2.
-  exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1.
-  assert (Mem.mem_inj init_meminj m1a m2a).
-  { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0).
-    eapply Mem.alloc_right_inj; eauto.
-    eauto.
-    eauto with mem.
-    red; intros; apply Z.divide_0_r.
-    intros. apply Mem.perm_implies with Freeable; auto with mem.
-    eapply Mem.perm_alloc_2; eauto. omega.
-    auto.
-  }
-  exploit store_zeros_mapped_inj; eauto. intros (m2b & A & B).
-  exploit store_init_data_list_mapped_inj; eauto.
-  intros. apply H2. red. exists ofs; auto. intros (m2c & C & D).
-  exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. intros (m2' & E & F).
-  exists m2'; split; auto. rewrite ! Zplus_0_r in E. rewrite A, C, E. auto.
-Qed.
-
-Lemma alloc_globals_app:
-  forall F V (g: Genv.t F V) defs1 m defs2,
-  Genv.alloc_globals g m (defs1 ++ defs2) =
-  match Genv.alloc_globals g m defs1 with
-  | None => None
-  | Some m1 => Genv.alloc_globals g m1 defs2
-  end.
+Section INIT_MEM.
+
+Variables m tm: mem.
+Hypothesis IM: Genv.init_mem p = Some m.
+Hypothesis TIM: Genv.init_mem tp = Some tm.
+
+Lemma bytes_of_init_inject:
+  forall il,
+  (forall id, ref_init il id -> kept id) ->
+  list_forall2 (memval_inject init_meminj) (Genv.bytes_of_init_data_list ge il) (Genv.bytes_of_init_data_list tge il).
 Proof.
-  induction defs1; simpl; intros. auto.
-  destruct (Genv.alloc_global g m a); auto.
+  induction il as [ | i1 il]; simpl; intros.
+- constructor.
+- apply list_forall2_app.
++ destruct i1; simpl; try (apply inj_bytes_inject). 
+  induction (Z.to_nat z); simpl; constructor. constructor. auto.
+  destruct (Genv.find_symbol ge i) as [b|] eqn:FS.
+  assert (kept i). { apply H. red. exists i0; auto with coqlib. }
+  exploit symbols_inject_2. apply init_meminj_preserves_globals. eauto. eauto. 
+  intros (b' & A & B). rewrite A. apply inj_value_inject.
+  econstructor; eauto. symmetry; apply Int.add_zero.
+  destruct (Genv.find_symbol tge i) as [b'|] eqn:FS'.
+  exploit symbols_inject_3. apply init_meminj_preserves_globals. eauto.
+  intros (b & A & B). congruence.
+  apply repeat_Undef_inject_self with (n := 4%nat). 
++ apply IHil. intros id [ofs IN]. apply H. exists ofs; auto with coqlib.
 Qed.
 
-Lemma alloc_globals_snoc:
-  forall F V (g: Genv.t F V) m defs1 id_def,
-  Genv.alloc_globals g m (defs1 ++ id_def :: nil) =
-  match Genv.alloc_globals g m defs1 with
-  | None => None
-  | Some m1 => Genv.alloc_global g m1 id_def
-  end.
+Lemma Mem_getN_forall2:
+  forall (P: memval -> memval -> Prop) c1 c2 i n p,
+  list_forall2 P (Mem.getN n p c1) (Mem.getN n p c2) ->
+  p <= i -> i < p + Z.of_nat n ->
+  P (ZMap.get i c1) (ZMap.get i c2).
 Proof.
-  intros. rewrite alloc_globals_app.
-  destruct (Genv.alloc_globals g m defs1); auto. unfold Genv.alloc_globals.
-  destruct (Genv.alloc_global g m0 id_def); auto.
-Qed.
-
-Lemma alloc_globals_inj:
-  forall pubs defs m1 u g1 g2,
-  Genv.alloc_globals ge Mem.empty (List.rev defs) = Some m1 ->
-  g1 = Genv.add_globals (Genv.empty_genv _ _ pubs) (List.rev defs) ->
-  g2 = Genv.add_globals (Genv.empty_genv _ _ pubs) (filter_globdefs u nil defs) ->
-  Mem.nextblock m1 = Genv.genv_next g1 ->
-  (forall id, IS.In id u -> Genv.find_symbol g1 id = Genv.find_symbol ge id) ->
-  (forall id, IS.In id u -> Genv.find_symbol g2 id = Genv.find_symbol tge id) ->
-  (forall b id, Genv.find_symbol ge id = Some b -> Plt b (Mem.nextblock m1) -> kept id -> IS.In id u) ->
-  (forall id, IS.In id u -> (fold_left add_def_prog_map (List.rev defs) (PTree.empty _))!id = pm!id) ->
-  exists m2,
-     Genv.alloc_globals tge Mem.empty (filter_globdefs u nil defs) = Some m2
-  /\ Mem.nextblock m2 = Genv.genv_next g2
-  /\ Mem.mem_inj init_meminj m1 m2.
-Proof.
-  induction defs; simpl; intros until g2; intros ALLOC GE1 GE2 NEXT1 SYMB1 SYMB2 SYMB3 PROGMAP.
-- inv ALLOC. exists Mem.empty. intuition auto. constructor; intros.
-  eelim Mem.perm_empty; eauto.
-  exploit init_meminj_invert; eauto. intros [A B]. subst delta. apply Z.divide_0_r.
-  eelim Mem.perm_empty; eauto.
-- rewrite Genv.add_globals_app in GE1. simpl in GE1.
-  set (g1' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (rev defs)) in *.
-  rewrite alloc_globals_snoc in ALLOC.
-  destruct (Genv.alloc_globals ge Mem.empty (rev defs)) as [m1'|] eqn:ALLOC1'; try discriminate.
-  exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK1.
-  assert (NEXTGE1: Genv.genv_next g1 = Pos.succ (Genv.genv_next g1')) by (rewrite GE1; reflexivity).
-  assert (NEXT1': Mem.nextblock m1' = Genv.genv_next g1') by (unfold block in *; xomega).
-  rewrite fold_left_app in PROGMAP. simpl in PROGMAP.
-  destruct a as [id gd]. unfold add_def_prog_map at 1 in PROGMAP. simpl in PROGMAP.
-  destruct (IS.mem id u) eqn:MEM.
-  + rewrite filter_globdefs_nil in *. rewrite alloc_globals_snoc.
-    rewrite Genv.add_globals_app in GE2. simpl in GE2.
-    set (g2' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (filter_globdefs (IS.remove id u) nil defs)) in *.
-    assert (NEXTGE2: Genv.genv_next g2 = Pos.succ (Genv.genv_next g2')) by (rewrite GE2; reflexivity).
-    assert (FS1: Genv.find_symbol ge id = Some (Mem.nextblock m1')).
-    { rewrite <- SYMB1 by (apply IS.mem_2; auto).
-      rewrite GE1. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. }
-    exploit (IHdefs m1' (IS.remove id u) g1' g2'); eauto.
-      intros. rewrite ISF.remove_iff in H; destruct H.
-      rewrite <- SYMB1 by auto. rewrite GE1. unfold Genv.find_symbol; simpl.
-      rewrite PTree.gso; auto.
-      intros. rewrite ISF.remove_iff in H; destruct H.
-      rewrite <- SYMB2 by auto. rewrite GE2. unfold Genv.find_symbol; simpl.
-      rewrite PTree.gso; auto.
-      intros. rewrite ISF.remove_iff. destruct (ident_eq id id0).
-      subst id0. rewrite FS1 in H. inv H. eelim Plt_strict; eauto.
-      exploit SYMB3. eexact H. unfold block in *; xomega. auto. tauto.
-      intros. rewrite ISF.remove_iff in H; destruct H.
-      rewrite <- PROGMAP by auto. rewrite PTree.gso by auto. auto.
-    intros (m2' & A & B & C). fold g2' in B.
-    assert (FS2: Genv.find_symbol tge id = Some (Mem.nextblock m2')).
-    { rewrite <- SYMB2 by (apply IS.mem_2; auto).
-      rewrite GE2. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. }
-    assert (INJ: init_meminj (Mem.nextblock m1') = Some (Mem.nextblock m2', 0)).
-    { apply Genv.find_invert_symbol in FS1. unfold init_meminj. rewrite FS1, FS2. auto. }
-    exploit alloc_global_mapped_inj. eexact ALLOC. eexact C. exact INJ.
-    intros. apply kept_closed with id gd. eapply transform_program_kept; eauto.
-    rewrite <- PROGMAP by (apply IS.mem_2; auto). apply PTree.gss. auto.
-    intros (m2 & D & E).
-    exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK2.
-    exists m2; split. rewrite A, D. auto.
-    split. unfold block in *; xomega.
-    auto.
-  + exploit (IHdefs m1' u g1' g2); auto.
-    intros. rewrite <- SYMB1 by auto. rewrite GE1.
-    unfold Genv.find_symbol; simpl. rewrite PTree.gso; auto.
-    red; intros; subst id0. apply IS.mem_1 in H. congruence.
-    intros. eapply SYMB3; eauto. unfold block in *; xomega.
-    intros. rewrite <- PROGMAP by auto. rewrite PTree.gso; auto.
-    apply IS.mem_1 in H. congruence.
-    intros (m2 & A & B & C).
-    assert (NOTINJ: init_meminj (Mem.nextblock m1') = None).
-    { destruct (init_meminj (Mem.nextblock m1')) as [[b' delta]|] eqn:J; auto.
-      exploit init_meminj_invert; eauto. intros (U & id1 & V & W).
-      exploit SYMB3; eauto. unfold block in *; xomega.
-      eapply transform_program_kept; eauto.
-      intros P.
-      revert V. rewrite <- SYMB1, GE1 by auto. unfold Genv.find_symbol; simpl.
-      rewrite PTree.gsspec. rewrite NEXT1'. destruct (peq id1 id); intros Q.
-      subst id1. apply IS.mem_1 in P. congruence.
-      eelim Plt_strict. eapply Genv.genv_symb_range; eauto. }
-    exists m2; intuition auto. eapply alloc_global_unmapped_inj; eauto.
+  induction n; simpl Mem.getN; intros.
+- simpl in H1. omegaContradiction.
+- inv H. rewrite inj_S in H1. destruct (zeq i p0).
++ congruence.
++ apply IHn with (p0 + 1); auto. omega. omega.
+Qed. 
+
+Lemma init_mem_inj_1:
+  Mem.mem_inj init_meminj m tm.
+Proof.
+  intros; constructor; intros.
+- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F).
+  exploit (Genv.init_mem_characterization_gen p); eauto.
+  exploit (Genv.init_mem_characterization_gen tp); eauto.
+  destruct gd as [f|v].
++ intros (P2 & Q2) (P1 & Q1).
+  apply Q1 in H0. destruct H0. subst.
+  apply Mem.perm_cur. auto.
++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1).
+  apply Q1 in H0. destruct H0. subst.
+  apply Mem.perm_cur. eapply Mem.perm_implies; eauto. 
+  apply P2. omega.
+- exploit init_meminj_invert; eauto. intros (A & id & B & C). 
+  subst delta. apply Zdivide_0.
+- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F).
+  exploit (Genv.init_mem_characterization_gen p); eauto.
+  exploit (Genv.init_mem_characterization_gen tp); eauto.
+  destruct gd as [f|v].
++ intros (P2 & Q2) (P1 & Q1).
+  apply Q1 in H0. destruct H0; discriminate.
++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1).
+  apply Q1 in H0. destruct H0.
+  assert (NO: gvar_volatile v = false).
+  { unfold Genv.perm_globvar in H1. destruct (gvar_volatile v); auto. inv H1. }
+Local Transparent Mem.loadbytes.
+  generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1.
+  generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2.
+  rewrite Zplus_0_r.
+  apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))).
+  rewrite H3, H4. apply bytes_of_init_inject. auto. 
+  omega. 
+  rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega. 
+Qed.
+
+Lemma init_mem_inj_2:
+  Mem.inject init_meminj m tm.
+Proof.
+  constructor; intros.
+- apply init_mem_inj_1.
+- destruct (init_meminj b) as [[b' delta]|] eqn:INJ; auto.
+  elim H. exploit init_meminj_invert; eauto. intros (A & id & B & C). 
+  eapply Genv.find_symbol_not_fresh; eauto.
+- exploit init_meminj_invert; eauto. intros (A & id & B & C). 
+  eapply Genv.find_symbol_not_fresh; eauto.
+- red; intros.
+  exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1).
+  exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2).
+  destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto.
+- exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta.
+  split. omega. generalize (Int.unsigned_range_2 ofs). omega.
+Qed.
+
+End INIT_MEM.
+
+Lemma init_mem_exists:
+  forall m, Genv.init_mem p = Some m ->
+  exists tm, Genv.init_mem tp = Some tm.
+Proof.
+  intros. apply Genv.init_mem_exists.
+  intros. 
+  assert (P: (prog_defmap tp)!id = Some (Gvar v)).
+  { eapply prog_defmap_norepet; eauto. eapply match_prog_unique; eauto. }
+  rewrite (match_prog_def _ _ _ TRANSF) in P. destruct (IS.mem id used) eqn:U; try discriminate.
+  exploit Genv.init_mem_inversion; eauto. apply in_prog_defmap; eauto. intros [AL FV].
+  split. auto.
+  intros. exploit FV; eauto. intros (b & FS).
+  apply transform_find_symbol_1 with b; auto.
+  apply kept_closed with id (Gvar v). 
+  apply IS.mem_2; auto. auto. red. red. exists o; auto.
 Qed.
 
 Theorem init_mem_inject:
@@ -1260,40 +1205,25 @@ Theorem init_mem_inject:
   exists f tm, Genv.init_mem tp = Some tm /\ Mem.inject f m tm /\ meminj_preserves_globals f.
 Proof.
   intros.
-  unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; injection TRANSF. intros EQ.
-  destruct (alloc_globals_inj (prog_public p) (List.rev (prog_defs p)) m used ge tge) as (tm & A & B & C).
-  rewrite rev_involutive; auto.
-  rewrite rev_involutive; auto.
-  unfold tge; rewrite <- EQ; auto.
-  symmetry. apply Genv.init_mem_genv_next; auto.
-  auto. auto. auto.
-  intros. rewrite rev_involutive. auto.
-  assert (D: Genv.init_mem tp = Some tm).
-  { unfold Genv.init_mem. fold tge. rewrite <- EQ. exact A. }
-  pose proof (init_meminj_preserves_globals).
-  exists init_meminj, tm; intuition auto.
-  constructor; intros.
-  + auto.
-  + destruct (init_meminj b) as [[b1 delta1]|] eqn:INJ; auto.
-    exploit init_meminj_invert; eauto. intros (P & id & Q & R).
-    elim H1. eapply Genv.find_symbol_not_fresh; eauto.
-  + exploit init_meminj_invert; eauto. intros (P & id & Q & R).
-    eapply Genv.find_symbol_not_fresh; eauto.
-  + apply init_meminj_no_overlap.
-  + exploit init_meminj_invert; eauto. intros (P & id & Q & R).
-    split. omega. generalize (Int.unsigned_range_2 ofs). omega.
+  exploit init_mem_exists; eauto. intros [tm INIT].
+  exists init_meminj, tm.
+  split. auto. 
+  split. eapply init_mem_inj_2; eauto. 
+  apply init_meminj_preserves_globals. 
 Qed.
 
 Lemma transf_initial_states:
   forall S1, initial_state p S1 -> exists S2, initial_state tp S2 /\ match_states S1 S2.
 Proof.
   intros. inv H. exploit init_mem_inject; eauto. intros (j & tm & A & B & C).
-  exploit symbols_inject_2. eauto. apply kept_main. eexact H1. intros (tb & P & Q).
-  exploit funct_ptr_inject. eauto. eexact Q. exact H2.
+  exploit symbols_inject_2. eauto. eapply kept_main. eexact H1. intros (tb & P & Q).
+  rewrite Genv.find_funct_ptr_iff in H2. 
+  exploit defs_inject. eauto. eexact Q. exact H2.
   intros (R & S & T).
+  rewrite <- Genv.find_funct_ptr_iff in R.
   exists (Callstate nil f nil tm); split.
   econstructor; eauto.
-    fold tge. unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; inversion TRANSF; auto.
+  fold tge. erewrite match_prog_main by eauto. auto.
   econstructor; eauto.
   constructor. auto.
   erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl.
@@ -1307,7 +1237,7 @@ Proof.
   intros. inv H0. inv H. inv STACKS. inv RESINJ. constructor.
 Qed.
 
-Theorem transf_program_correct:
+Lemma transf_program_correct_1:
   forward_simulation (semantics p) (semantics tp).
 Proof.
   intros.
@@ -1319,3 +1249,175 @@ Proof.
 Qed.
 
 End SOUNDNESS.
+
+Theorem transf_program_correct:
+  forall p tp, match_prog p tp -> forward_simulation (semantics p) (semantics tp).
+Proof.
+  intros p tp (used & A & B).  apply transf_program_correct_1 with used; auto.
+Qed.
+
+(** * Commutation with linking *)
+
+Remark link_def_either:
+  forall (gd1 gd2 gd: globdef fundef unit),
+  link_def gd1 gd2 = Some gd -> gd = gd1 \/ gd = gd2.
+Proof with (try discriminate).
+  intros until gd.
+Local Transparent Linker_def Linker_fundef Linker_varinit Linker_vardef Linker_unit.
+  destruct gd1 as [f1|v1], gd2 as [f2|v2]...
+(* Two fundefs *)
+  destruct f1 as [f1|ef1], f2 as [f2|ef2]; simpl...
+  destruct ef2; intuition congruence.
+  destruct ef1; intuition congruence.
+  destruct (external_function_eq ef1 ef2); intuition congruence.
+(* Two vardefs *)
+  simpl. unfold link_vardef. destruct v1 as [info1 init1 ro1 vo1], v2 as [info2 init2 ro2 vo2]; simpl.
+  destruct (link_varinit init1 init2) as [init|] eqn:LI...
+  destruct (eqb ro1 ro2) eqn:RO...
+  destruct (eqb vo1 vo2) eqn:VO...
+  simpl. 
+  destruct info1, info2.
+  assert (EITHER: init = init1 \/ init = init2).
+  { revert LI. unfold link_varinit. 
+    destruct (classify_init init1), (classify_init init2); intro EQ; inv EQ; auto.
+    destruct (zeq sz (Z.max sz0 0 + 0)); inv H0; auto.
+    destruct (zeq sz (init_data_list_size il)); inv H0; auto.
+    destruct (zeq sz (init_data_list_size il)); inv H0; auto. }
+  apply eqb_prop in RO. apply eqb_prop in VO. 
+  intro EQ; inv EQ. destruct EITHER; subst init; auto.
+Qed.
+
+Remark used_not_defined:
+  forall p used id,
+  valid_used_set p used ->
+  (prog_defmap p)!id = None ->
+  IS.mem id used = false \/ id = prog_main p.
+Proof.
+  intros. destruct (IS.mem id used) eqn:M; auto.
+  exploit used_defined; eauto using IS.mem_2. intros [A|A]; auto.
+  apply prog_defmap_dom in A. destruct A as [g E]; congruence.
+Qed.
+
+Remark used_not_defined_2:
+  forall p used id,
+  valid_used_set p used ->
+  id <> prog_main p ->
+  (prog_defmap p)!id = None ->
+  ~IS.In id used.
+Proof.
+  intros. exploit used_not_defined; eauto. intros [A|A].
+  red; intros; apply IS.mem_1 in H2; congruence.
+  congruence.
+Qed.
+
+Lemma link_valid_used_set:
+  forall p1 p2 p used1 used2,
+  link p1 p2 = Some p ->
+  valid_used_set p1 used1 ->
+  valid_used_set p2 used2 ->
+  valid_used_set p (IS.union used1 used2).
+Proof.
+  intros until used2; intros L V1 V2.
+  destruct (link_prog_inv _ _ _ L) as (X & Y & Z).
+  rewrite Z; clear Z; constructor.
+- intros. rewrite ISF.union_iff in H. rewrite ISF.union_iff.
+  rewrite prog_defmap_elements, PTree.gcombine in H0.
+  destruct (prog_defmap p1)!id as [gd1|] eqn:GD1;
+  destruct (prog_defmap p2)!id as [gd2|] eqn:GD2;
+  simpl in H0; try discriminate.
++ (* common definition *)
+  exploit Y; eauto. intros (PUB1 & PUB2 & _).
+  exploit link_def_either; eauto. intros [EQ|EQ]; subst gd.
+* left. eapply used_closed. eexact V1. eapply used_public. eexact V1. eauto. eauto. auto. 
+* right. eapply used_closed. eexact V2. eapply used_public. eexact V2. eauto. eauto. auto.
++ (* left definition *)
+  inv H0. destruct (ISP.In_dec id used1).
+* left; eapply used_closed; eauto.
+* assert (IS.In id used2) by tauto.
+  exploit used_defined. eexact V2. eauto. intros [A|A].
+  exploit prog_defmap_dom; eauto. intros [g E]; congruence.
+  elim n. rewrite A, <- X. eapply used_main; eauto.
++ (* right definition *)
+  inv H0. destruct (ISP.In_dec id used2).
+* right; eapply used_closed; eauto.
+* assert (IS.In id used1) by tauto.
+  exploit used_defined. eexact V1. eauto. intros [A|A].
+  exploit prog_defmap_dom; eauto. intros [g E]; congruence.
+  elim n. rewrite A, X. eapply used_main; eauto.
++ (* no definition *)
+  auto.
+- simpl. rewrite ISF.union_iff; left; eapply used_main; eauto.
+- simpl. intros id. rewrite in_app_iff, ISF.union_iff. 
+  intros [A|A]; [left|right]; eapply used_public; eauto.
+- intros. rewrite ISF.union_iff in H.
+  destruct (ident_eq id (prog_main p1)).
++ right; assumption.
++ assert (E: exists g, link_prog_merge (prog_defmap p1)!id (prog_defmap p2)!id = Some g).
+  { destruct (prog_defmap p1)!id as [gd1|] eqn:GD1;
+    destruct (prog_defmap p2)!id as [gd2|] eqn:GD2; simpl.
+  * apply Y with id; auto.
+  * exists gd1; auto.
+  * exists gd2; auto.
+  * eapply used_not_defined_2 in GD1; eauto. eapply used_not_defined_2 in GD2; eauto.
+    tauto.
+    congruence.
+  }
+  destruct E as [g LD].
+  left. unfold prog_defs_names; simpl.
+  change id with (fst (id, g)). apply in_map. apply PTree.elements_correct.
+  rewrite PTree.gcombine; auto.
+Qed.
+
+Theorem link_match_program:
+  forall p1 p2 tp1 tp2 p,
+  link p1 p2 = Some p ->
+  match_prog p1 tp1 -> match_prog p2 tp2 ->
+  exists tp, link tp1 tp2 = Some tp /\ match_prog p tp.
+Proof.
+  intros. destruct H0 as (used1 & A1 & B1). destruct H1 as (used2 & A2 & B2).
+  destruct (link_prog_inv _ _ _ H) as (U & V & W).
+  econstructor; split. 
+- apply link_prog_succeeds.
++ rewrite (match_prog_main _ _ _ B1), (match_prog_main _ _ _ B2). auto.
++ intros. 
+  rewrite (match_prog_def _ _ _ B1) in H0.
+  rewrite (match_prog_def _ _ _ B2) in H1.
+  destruct (IS.mem id used1) eqn:U1; try discriminate.
+  destruct (IS.mem id used2) eqn:U2; try discriminate.
+  edestruct V as (X & Y & gd & Z); eauto.
+  split. rewrite (match_prog_public _ _ _ B1); auto. 
+  split. rewrite (match_prog_public _ _ _ B2); auto.
+  congruence.
+- exists (IS.union used1 used2); split.
++ eapply link_valid_used_set; eauto.
++ rewrite W. constructor; simpl; intros.
+* eapply match_prog_main; eauto.
+* rewrite (match_prog_public _ _ _ B1), (match_prog_public _ _ _ B2). auto.
+* rewrite ! prog_defmap_elements, !PTree.gcombine by auto.
+  rewrite (match_prog_def _ _ _ B1 id), (match_prog_def _ _ _ B2 id).
+  rewrite ISF.union_b.
+{
+  destruct (prog_defmap p1)!id as [gd1|] eqn:GD1;
+  destruct (prog_defmap p2)!id as [gd2|] eqn:GD2.
+- (* both defined *)
+  exploit V; eauto. intros (PUB1 & PUB2 & _). 
+  assert (EQ1: IS.mem id used1 = true) by (apply IS.mem_1; eapply used_public; eauto).
+  assert (EQ2: IS.mem id used2 = true) by (apply IS.mem_1; eapply used_public; eauto).
+  rewrite EQ1, EQ2; auto.
+- (* left defined *)
+  exploit used_not_defined; eauto. intros [A|A].
+  rewrite A, orb_false_r. destruct (IS.mem id used1); auto.
+  replace (IS.mem id used1) with true. destruct (IS.mem id used2); auto.
+  symmetry. apply IS.mem_1. rewrite A, <- U. eapply used_main; eauto.
+- (* right defined *)
+  exploit used_not_defined. eexact A1. eauto. intros [A|A].
+  rewrite A, orb_false_l. destruct (IS.mem id used2); auto.
+  replace (IS.mem id used2) with true. destruct (IS.mem id used1); auto.
+  symmetry. apply IS.mem_1. rewrite A, U. eapply used_main; eauto.
+- (* none defined *)
+  destruct (IS.mem id used1), (IS.mem id used2); auto.
+}
+* intros. apply PTree.elements_keys_norepet. 
+Qed.
+
+Instance TransfSelectionLink : TransfLink match_prog := link_match_program.