Update the back-end proofs to the new linking framework.

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.