simplification of Duplicate: remove xfunction

2 files changed, 154 insertions, 187 deletions

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index a591d6e5..3ad37c83 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -13,49 +13,28 @@ Axiom duplicate_aux: function -> code * node * (PTree.t node).
 
 Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux".
 
-Record xfunction : Type := 
- { fn_RTL: function;
-   fn_revmap: PTree.t node;
- }.
-
-Definition xfundef := AST.fundef xfunction.
-Definition xprogram := AST.program xfundef unit.
-Definition xgenv := Genv.t xfundef unit.
-
-Definition fundef_RTL (fu: xfundef) : fundef := 
-  match fu with
-  | Internal f => Internal (fn_RTL f)
-  | External ef => External ef
-  end.
-
 (** * Verification of node duplications *)
 
-Definition verify_mapping_entrypoint (f: function) (xf: xfunction) : res unit :=
-  match ((fn_revmap xf)!(fn_entrypoint (fn_RTL xf))) with
-  | None => Error (msg "verify_mapping: No node in xf revmap for entrypoint")
-  | Some n => match (Pos.compare n (fn_entrypoint f)) with
-              | Eq => OK tt
-              | _ => Error (msg "verify_mapping_entrypoint: xf revmap for entrypoint does not correspond to the entrypoint of f")
-              end
-  end.
-
-Definition verify_is_copy revmap n n' :=
-  match revmap!n' with
+Definition verify_is_copy dupmap n n' :=
+  match dupmap!n' with
   | None => Error(msg "verify_is_copy None")
   | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end
   end.
 
-Fixpoint verify_is_copy_list revmap ln ln' :=
+Fixpoint verify_is_copy_list dupmap ln ln' :=
   match ln with
   | n::ln => match ln' with
-             | n'::ln' => do u <- verify_is_copy revmap n n';
-                          verify_is_copy_list revmap ln ln'
+             | n'::ln' => do u <- verify_is_copy dupmap n n';
+                          verify_is_copy_list dupmap ln ln'
              | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end
   | nil => match ln' with
           | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'")
           | nil => OK tt end
   end.
 
+Definition verify_mapping_entrypoint dupmap (f f': function): res unit :=
+  verify_is_copy dupmap (fn_entrypoint f) (fn_entrypoint f').
+
 Lemma product_eq {A B: Type} :
   (forall (a b: A), {a=b} + {a<>b}) ->
   (forall (c d: B), {c=d} + {c<>d}) ->
@@ -77,13 +56,13 @@ Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}.
 Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed.
 Global Opaque builtin_res_eq_pos.
 
-Definition verify_match_inst revmap inst tinst :=
+Definition verify_match_inst dupmap inst tinst :=
   match inst with
-  | Inop n => match tinst with Inop n' => do u <- verify_is_copy revmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end
+  | Inop n => match tinst with Inop n' => do u <- verify_is_copy dupmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end
 
   | Iop op lr r n => match tinst with
       Iop op' lr' r' n' =>
-          do u <- verify_is_copy revmap n n';
+          do u <- verify_is_copy dupmap n n';
           if (eq_operation op op') then
             if (list_eq_dec Pos.eq_dec lr lr') then
               if (Pos.eq_dec r r') then
@@ -95,7 +74,7 @@ Definition verify_match_inst revmap inst tinst :=
 
   | Iload m a lr r n => match tinst with
       | Iload m' a' lr' r' n' =>
-          do u <- verify_is_copy revmap n n';
+          do u <- verify_is_copy dupmap n n';
           if (chunk_eq m m') then
             if (eq_addressing a a') then
               if (list_eq_dec Pos.eq_dec lr lr') then
@@ -108,7 +87,7 @@ Definition verify_match_inst revmap inst tinst :=
 
   | Istore m a lr r n => match tinst with
       | Istore m' a' lr' r' n' =>
-          do u <- verify_is_copy revmap n n';
+          do u <- verify_is_copy dupmap n n';
           if (chunk_eq m m') then
             if (eq_addressing a a') then
               if (list_eq_dec Pos.eq_dec lr lr') then
@@ -121,7 +100,7 @@ Definition verify_match_inst revmap inst tinst :=
 
   | Icall s ri lr r n => match tinst with
       | Icall s' ri' lr' r' n' =>
-          do u <- verify_is_copy revmap n n';
+          do u <- verify_is_copy dupmap n n';
           if (signature_eq s s') then
             if (product_eq Pos.eq_dec ident_eq ri ri') then
               if (list_eq_dec Pos.eq_dec lr lr') then
@@ -144,7 +123,7 @@ Definition verify_match_inst revmap inst tinst :=
 
   | Ibuiltin ef lbar brr n => match tinst with
       | Ibuiltin ef' lbar' brr' n' =>
-          do u <- verify_is_copy revmap n n';
+          do u <- verify_is_copy dupmap n n';
           if (external_function_eq ef ef') then
             if (list_eq_dec builtin_arg_eq_pos lbar lbar') then
               if (builtin_res_eq_pos brr brr') then OK tt
@@ -155,8 +134,8 @@ Definition verify_match_inst revmap inst tinst :=
 
   | Icond cond lr n1 n2 => match tinst with
       | Icond cond' lr' n1' n2' =>
-          do u1 <- verify_is_copy revmap n1 n1';
-          do u2 <- verify_is_copy revmap n2 n2';
+          do u1 <- verify_is_copy dupmap n1 n1';
+          do u2 <- verify_is_copy dupmap n2 n2';
           if (eq_condition cond cond') then
             if (list_eq_dec Pos.eq_dec lr lr') then OK tt
             else Error (msg "Different lr in Icond")
@@ -165,7 +144,7 @@ Definition verify_match_inst revmap inst tinst :=
 
   | Ijumptable r ln => match tinst with
       | Ijumptable r' ln' =>
-          do u <- verify_is_copy_list revmap ln ln';
+          do u <- verify_is_copy_list dupmap ln ln';
           if (Pos.eq_dec r r') then OK tt
           else Error (msg "Different r in Ijumptable")
       | _ => Error (msg "verify_match_inst Ijumptable") end
@@ -177,54 +156,40 @@ Definition verify_match_inst revmap inst tinst :=
       | _ => Error (msg "verify_match_inst Ireturn") end
   end.
 
-Definition verify_mapping_mn f xf (m: positive*positive) :=
+Definition verify_mapping_mn dupmap f f' (m: positive*positive) :=
   let (tn, n) := m in
   match (fn_code f)!n with
   | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code f)!n")
-  | Some inst => match (fn_code (fn_RTL xf))!tn with
+  | Some inst => match (fn_code f')!tn with
                  | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code xf)!tn")
-                 | Some tinst => verify_match_inst (fn_revmap xf) inst tinst
+                 | Some tinst => verify_match_inst dupmap inst tinst
                  end
   end.
 
-Fixpoint verify_mapping_mn_rec f xf lm :=
+Fixpoint verify_mapping_mn_rec dupmap f f' lm :=
   match lm with
   | nil => OK tt
-  | m :: lm => do u <- verify_mapping_mn f xf m;
-               do u2 <- verify_mapping_mn_rec f xf lm;
+  | m :: lm => do u <- verify_mapping_mn dupmap f f' m;
+               do u2 <- verify_mapping_mn_rec dupmap f f' lm;
                OK tt
   end.
 
-Definition verify_mapping_match_nodes (f: function) (xf: xfunction) : res unit :=
-  verify_mapping_mn_rec f xf (PTree.elements (fn_revmap xf)).
+Definition verify_mapping_match_nodes dupmap (f f': function): res unit :=
+  verify_mapping_mn_rec dupmap f f' (PTree.elements dupmap).
 
-(** Verifies that the [fn_revmap] of the translated function [xf] is giving correct information in regards to [f] *)
-Definition verify_mapping (f: function) (xf: xfunction) : res unit :=
-  do u <- verify_mapping_entrypoint f xf;
-  do v <- verify_mapping_match_nodes f xf; OK tt.
-(* TODO - verify the other axiom *)
+(** Verifies that the [dupmap] of the translated function [f'] is giving correct information in regards to [f] *)
+Definition verify_mapping dupmap (f f': function) : res unit :=
+  do u <- verify_mapping_entrypoint dupmap f f';
+  do v <- verify_mapping_match_nodes dupmap f f'; OK tt.
 
 (** * Entry points *)
 
-Definition transf_function_aux (f: function) : res xfunction :=
-  let (tcte, mp) := duplicate_aux f in
-  let (tc, te) := tcte in
-  let xf := {| fn_RTL := (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te); fn_revmap := mp |} in
-  do u <- verify_mapping f xf;
-  OK xf.
-
-Theorem transf_function_aux_preserves:
-  forall f xf,
-  transf_function_aux f = OK xf ->
-     fn_sig f = fn_sig (fn_RTL xf) /\ fn_params f = fn_params (fn_RTL xf) /\ fn_stacksize f = fn_stacksize (fn_RTL xf).
-Proof.
-  intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H.
-  repeat (split; try reflexivity).
-Qed.
-
 Definition transf_function (f: function) : res function :=
-  do xf <- transf_function_aux f;
-  OK (fn_RTL xf).
+  let (tcte, dupmap) := duplicate_aux f in
+  let (tc, te) := tcte in
+  let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in
+  do u <- verify_mapping dupmap f f';
+  OK f'.
 
 Definition transf_fundef (f: fundef) : res fundef :=
   transf_partial_fundef transf_function f.
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 04936eeb..9d56e86f 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -7,58 +7,57 @@ Local Open Scope positive_scope.
 
 (** * Definition of [match_states] (independently of the translation) *)
 
-(* est-ce plus simple de prendre is_copy: node -> node, avec un noeud hors CFG à la place de None ? *)
-Inductive match_inst (is_copy: node -> option node): instruction -> instruction -> Prop :=
+(* est-ce plus simple de prendre dupmap: node -> node, avec un noeud hors CFG à la place de None ? *)
+Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop :=
   | match_inst_nop: forall n n',
-      is_copy n' = (Some n) -> match_inst is_copy (Inop n) (Inop n')
+      dupmap!n' = (Some n) -> match_inst dupmap (Inop n) (Inop n')
   | match_inst_op: forall n n' op lr r,
-      is_copy n' = (Some n) -> match_inst is_copy (Iop op lr r n) (Iop op lr r n')
+      dupmap!n' = (Some n) -> match_inst dupmap (Iop op lr r n) (Iop op lr r n')
   | match_inst_load: forall n n' m a lr r,
-      is_copy n' = (Some n) -> match_inst is_copy (Iload m a lr r n) (Iload m a lr r n')
+      dupmap!n' = (Some n) -> match_inst dupmap (Iload m a lr r n) (Iload m a lr r n')
   | match_inst_store: forall n n' m a lr r,
-      is_copy n' = (Some n) -> match_inst is_copy (Istore m a lr r n) (Istore m a lr r n')
+      dupmap!n' = (Some n) -> match_inst dupmap (Istore m a lr r n) (Istore m a lr r n')
   | match_inst_call: forall n n' s ri lr r,
-      is_copy n' = (Some n) -> match_inst is_copy (Icall s ri lr r n) (Icall s ri lr r n')
+      dupmap!n' = (Some n) -> match_inst dupmap (Icall s ri lr r n) (Icall s ri lr r n')
   | match_inst_tailcall: forall s ri lr,
-      match_inst is_copy (Itailcall s ri lr) (Itailcall s ri lr)
+      match_inst dupmap (Itailcall s ri lr) (Itailcall s ri lr)
   | match_inst_builtin: forall n n' ef la br,
-      is_copy n' = (Some n) -> match_inst is_copy (Ibuiltin ef la br n) (Ibuiltin ef la br n')
+      dupmap!n' = (Some n) -> match_inst dupmap (Ibuiltin ef la br n) (Ibuiltin ef la br n')
   | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr,
-      is_copy ifso' = (Some ifso) -> is_copy ifnot' = (Some ifnot) ->
-      match_inst is_copy (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot')
+      dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) ->
+      match_inst dupmap (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot')
   | match_inst_jumptable: forall ln ln' r,
-      list_forall2 (fun n n' => (is_copy n' = (Some n))) ln ln' ->
-      match_inst is_copy (Ijumptable r ln) (Ijumptable r ln')
-  | match_inst_return: forall or, match_inst is_copy (Ireturn or) (Ireturn or).
-
-Record match_function f xf: Prop := {
-  revmap_correct: forall n n', (fn_revmap xf)!n' = Some n ->
-    (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n' => (fn_revmap xf)!n') i i');
-  revmap_entrypoint: (fn_revmap xf)!(fn_entrypoint (fn_RTL xf)) = Some (fn_entrypoint f);
-  preserv_fnsig: fn_sig f = fn_sig (fn_RTL xf);
-  preserv_fnparams: fn_params f = fn_params (fn_RTL xf);
-  preserv_fnstacksize: fn_stacksize f = fn_stacksize (fn_RTL xf)
+      list_forall2 (fun n n' => (dupmap!n' = (Some n))) ln ln' ->
+      match_inst dupmap (Ijumptable r ln) (Ijumptable r ln')
+  | match_inst_return: forall or, match_inst dupmap (Ireturn or) (Ireturn or).
+
+Record match_function dupmap f f': Prop := {
+  dupmap_correct: forall n n', dupmap!n' = Some n ->
+    (forall i, (fn_code f)!n = Some i -> exists i', (fn_code f')!n' = Some i' /\ match_inst dupmap i i');
+  dupmap_entrypoint: dupmap!(fn_entrypoint f') = Some (fn_entrypoint f);
+  preserv_fnsig: fn_sig f = fn_sig f';
+  preserv_fnparams: fn_params f = fn_params f';
+  preserv_fnstacksize: fn_stacksize f = fn_stacksize f'
 }.
 
 Inductive match_fundef: RTL.fundef -> RTL.fundef -> Prop :=
-  | match_Internal f xf: match_function f xf -> match_fundef (Internal f) (Internal (fn_RTL xf))
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
   | match_External ef: match_fundef (External ef) (External ef).
 
-
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
-  | match_stackframe_intro:
-    forall res f sp pc rs xf pc'
-      (TRANSF: match_function f xf)
-      (DUPLIC: (fn_revmap xf)!pc' = Some pc),
-      match_stackframes (Stackframe res f sp pc rs) (Stackframe res (fn_RTL xf) sp pc' rs).
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc):
+      match_stackframes (Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).
 
 Inductive match_states: state -> state -> Prop :=
-  | match_states_intro:
-    forall st f sp pc rs m st' xf pc'
+  | match_states_intro 
+      dupmap st f sp pc rs m st' f' pc'
       (STACKS: list_forall2 match_stackframes st st')
-      (TRANSF: match_function f xf)
-      (DUPLIC: (fn_revmap xf)!pc' = Some pc),
-      match_states (State st f sp pc rs m) (State st' (fn_RTL xf) sp pc' rs m)
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc):
+      match_states (State st f sp pc rs m) (State st' f' sp pc' rs m)
   | match_states_call:
     forall st st' f f' args m
       (STACKS: list_forall2 match_stackframes st st')
@@ -71,11 +70,22 @@ Inductive match_states: state -> state -> Prop :=
 
 (** * Auxiliary properties *)
 
+
+Theorem transf_function_preserves:
+  forall f f',
+  transf_function f = OK f' ->
+     fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'.
+Proof.
+  intros. unfold transf_function in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H.
+  repeat (split; try reflexivity).
+Qed.
+
+
 Lemma verify_mapping_mn_rec_step:
-  forall lb b f xf,
+  forall dupmap lb b f f',
   In b lb ->
-  verify_mapping_mn_rec f xf lb = OK tt ->
-  verify_mapping_mn f xf b = OK tt.
+  verify_mapping_mn_rec dupmap f f' lb = OK tt ->
+  verify_mapping_mn dupmap f f' b = OK tt.
 Proof.
   induction lb; intros.
   - monadInv H0. inversion H.
@@ -85,20 +95,20 @@ Proof.
 Qed.
 
 Lemma verify_is_copy_correct:
-  forall xf n n',
-  verify_is_copy (fn_revmap xf) n n' = OK tt ->
-  (fn_revmap xf) ! n' = Some n.
+  forall dupmap n n',
+  verify_is_copy dupmap n n' = OK tt ->
+  dupmap ! n' = Some n.
 Proof.
   intros. unfold verify_is_copy in H. destruct (_ ! n') eqn:REVM; [|inversion H].
-  destruct (n ?= n0) eqn:NP; try (inversion H; fail).
+  destruct (n ?= p) eqn:NP; try (inversion H; fail).
   eapply Pos.compare_eq in NP. subst.
   reflexivity.
 Qed.
 
 Lemma verify_is_copy_list_correct:
-  forall xf ln ln',
-  verify_is_copy_list (fn_revmap xf) ln ln' = OK tt ->
-  list_forall2 (fun n n' => (fn_revmap xf) ! n' = Some n) ln ln'.
+  forall dupmap ln ln',
+  verify_is_copy_list dupmap ln ln' = OK tt ->
+  list_forall2 (fun n n' => dupmap ! n' = Some n) ln ln'.
 Proof.
   induction ln.
   - intros. destruct ln'; monadInv H. constructor.
@@ -107,9 +117,9 @@ Proof.
 Qed.
 
 Lemma verify_match_inst_correct:
-  forall xf i i',
-  verify_match_inst (fn_revmap xf) i i' = OK tt ->
-  match_inst (fun nn => (fn_revmap xf) ! nn) i i'.
+  forall dupmap i i',
+  verify_match_inst dupmap i i' = OK tt ->
+  match_inst dupmap i i'.
 Proof.
   intros. unfold verify_match_inst in H.
   destruct i; try (inversion H; fail).
@@ -180,64 +190,64 @@ Proof.
 Qed.
 
 
-Lemma verify_mapping_mn_correct:
-  forall mp n n' i f xf tc,
+Lemma verify_mapping_mn_correct mp n n' i f f' tc:
   mp ! n' = Some n ->
   (fn_code f) ! n = Some i ->
-  (fn_code (fn_RTL xf)) = tc ->
-  fn_revmap xf = mp ->
-  verify_mapping_mn f xf (n', n) = OK tt ->
+  (fn_code f') = tc ->
+  verify_mapping_mn mp f f' (n', n) = OK tt ->
   exists i',
      tc ! n' = Some i'
-  /\ match_inst (fun nn => mp ! nn) i i'.
+  /\ match_inst mp i i'.
 Proof.
-  intros. unfold verify_mapping_mn in H3. rewrite H0 in H3. clear H0. rewrite H1 in H3. clear H1.
-  destruct (tc ! n') eqn:TCN; [| inversion H3].
-  exists i0. split; auto. rewrite <- H2.
+  unfold verify_mapping_mn; intros H H0 H1 H2. rewrite H0 in H2. clear H0. rewrite H1 in H2. clear H1.
+  destruct (tc ! n') eqn:TCN; [| inversion H2].
+  exists i0. split; auto.
   eapply verify_match_inst_correct. assumption.
 Qed.
 
 
 Lemma verify_mapping_mn_rec_correct:
-  forall mp n n' i f xf tc,
+  forall mp n n' i f f' tc,
   mp ! n' = Some n ->
   (fn_code f) ! n = Some i ->
-  (fn_code (fn_RTL xf)) = tc ->
-  fn_revmap xf = mp ->
-  verify_mapping_mn_rec f xf (PTree.elements mp) = OK tt ->
+  (fn_code f') = tc ->
+  verify_mapping_mn_rec mp f f' (PTree.elements mp) = OK tt ->
   exists i',
      tc ! n' = Some i'
-  /\ match_inst (fun nn => mp ! nn) i i'.
+  /\ match_inst mp i i'.
 Proof.
   intros. exploit PTree.elements_correct. eapply H. intros IN.
-  eapply verify_mapping_mn_rec_step in H3; eauto.
+  eapply verify_mapping_mn_rec_step in H2; eauto.
   eapply verify_mapping_mn_correct; eauto.
 Qed.
 
-Theorem transf_function_correct f xf:
-    transf_function_aux f = OK xf -> match_function f xf.
+Theorem transf_function_correct f f':
+    transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
 Proof.
-  intros TRANSF ; constructor 1; try (apply transf_function_aux_preserves; auto). 
+  unfold transf_function.
+  intros TRANSF.
+  destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te).
+  monadInv TRANSF.
+  unfold verify_mapping in EQ. monadInv EQ.
+  exists mp; constructor 1; simpl; auto.
   + (* correct *) 
   intros until n'. intros REVM i FNC.
-  unfold transf_function_aux in TRANSF. destruct (duplicate_aux f) as (tcte & mp). destruct tcte as (tc & te). monadInv TRANSF.
-  simpl in *. monadInv EQ. clear EQ0.
   unfold verify_mapping_match_nodes in EQ. simpl in EQ. destruct x1.
-  eapply verify_mapping_mn_rec_correct. 5: eapply EQ. all: eauto.
+  eapply verify_mapping_mn_rec_correct; eauto.
+  simpl; eauto.
   + (* entrypoint *)
-  intros. unfold transf_function_aux in TRANSF. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te).
-  monadInv TRANSF. simpl. monadInv EQ. unfold verify_mapping_entrypoint in EQ0. simpl in EQ0.
-  destruct (mp ! te) eqn:PT; try discriminate.
-  destruct (n ?= fn_entrypoint f) eqn:EQQ; try discriminate. inv EQ0.
-  apply Pos.compare_eq in EQQ. congruence.
+  intros. unfold verify_mapping_entrypoint in EQ0. simpl in EQ0.
+  eapply verify_is_copy_correct; eauto.
+  destruct x0; auto.
 Qed.
 
 Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
 Proof.
   intros TRANSF; destruct f; simpl; monadInv TRANSF.
-  + monadInv EQ.
-    eapply match_Internal; eapply transf_function_correct; eauto.
+  + exploit transf_function_correct; eauto.
+    intros (dupmap & MATCH_F).
+    eapply match_Internal; eauto.
   + eapply match_External.
 Qed.
 
@@ -267,10 +277,12 @@ Proof.
   rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
 Qed.
 
+(* UNUSED LEMMA ?
 Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z.
 Proof.
   unfold Senv.equiv. intuition congruence.
 Qed.
+*)
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
@@ -304,27 +316,17 @@ Lemma function_sig_translated:
   forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f.
 Proof.
   intros. destruct f.
-  - simpl in H. monadInv H. simpl. symmetry. monadInv EQ. apply transf_function_aux_preserves. assumption.
-  - simpl in H. monadInv H. (* monadInv EQ. *) reflexivity.
+  - simpl in H. monadInv H. simpl. symmetry. apply transf_function_preserves. assumption.
+  - simpl in H. monadInv H. reflexivity.
 Qed.
 
-Lemma sig_preserved:
-  forall f tf,
-  transf_fundef f = OK tf ->
-  funsig tf = funsig f.
-Proof.
-  unfold transf_fundef, transf_partial_fundef; intros.
-  destruct f. monadInv H. simpl. symmetry. monadInv EQ. apply transf_function_aux_preserves. assumption.
-  inv H. reflexivity.
-Qed.
-
-Lemma list_nth_z_revmap:
-  forall ln f ln' (pc pc': node) val,
+Lemma list_nth_z_dupmap:
+  forall dupmap ln ln' (pc pc': node) val,
   list_nth_z ln val = Some pc ->
-  list_forall2 (fun n n' => (fn_revmap f)!n' = Some n) ln ln' ->
+  list_forall2 (fun n n' => dupmap!n' = Some n) ln ln' ->
   exists pc',
      list_nth_z ln' val = Some pc'
-  /\ (fn_revmap f)!pc' = Some pc.
+  /\ dupmap!pc' = Some pc.
 Proof.
   induction ln; intros until val; intros LNZ LFA.
   - inv LNZ.
@@ -348,8 +350,8 @@ Proof.
       symmetry. eapply match_program_main. eauto.
     + exploit function_ptr_translated; eauto.
     + destruct f.
-      * monadInv TRANSF. monadInv EQ. rewrite <- H3. symmetry; eapply transf_function_aux_preserves. assumption.
-      * monadInv TRANSF. (* monadInv EQ. *) assumption.
+      * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption.
+      * monadInv TRANSF. assumption.
   - constructor; eauto. constructor. apply transf_fundef_correct; auto.
 Qed.
 
@@ -370,35 +372,35 @@ Proof.
   Local Hint Resolve transf_fundef_correct.
   induction 1; intros; inv MS.
 (* Inop *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3).
     inv H3.
     eexists. split.
     + eapply exec_Inop; eauto.
-    + constructor; eauto.
+    + econstructor; eauto.
 (* Iop *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
     + eapply exec_Iop; eauto. erewrite eval_operation_preserved; eauto.
-    + constructor; eauto.
+    + econstructor; eauto.
 (* Iload *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
     + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto.
-    + constructor; auto.
+    + econstructor; eauto.
 (* Istore *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
     + eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto.
-    + constructor; auto.
+    + econstructor; eauto.
 (* Icall *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     destruct ros.
@@ -407,15 +409,15 @@ Proof.
       eexists. split.
       + eapply exec_Icall. eassumption. simpl. eassumption.
         apply function_sig_translated. assumption.
-      + repeat (constructor; auto).
+      + repeat (econstructor; eauto).
     * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
       apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF).
       eexists. split.
       + eapply exec_Icall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS.
         eassumption. apply function_sig_translated. assumption.
-      + repeat (constructor; auto).
+      + repeat (econstructor; eauto).
 (* Itailcall *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H10 & H11). inv H11.
     pose symbols_preserved as SYMPRES.
     destruct ros.
@@ -434,40 +436,40 @@ Proof.
         erewrite <- preserv_fnstacksize; eauto.
       + repeat (constructor; auto).
 (* Ibuiltin *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
     + eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto.
       eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
-    + constructor; auto.
+    + econstructor; eauto.
 (* Icond *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
     + eapply exec_Icond; eauto.
-    + constructor; auto. destruct b; auto.
+    + econstructor; eauto. destruct b; auto.
 (* Ijumptable *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
-    exploit list_nth_z_revmap; eauto. intros (pc'1 & LNZ & REVM).
+    exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM).
     eexists. split.
     + eapply exec_Ijumptable; eauto.
-    + constructor; auto.
+    + econstructor; eauto.
 (* Ireturn *)
-  - eapply revmap_correct in DUPLIC; eauto.
+  - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
     + eapply exec_Ireturn; eauto. erewrite <- preserv_fnstacksize; eauto.
-    + constructor; auto.
+    + econstructor; eauto.
 (* exec_function_internal *)
-  - inversion TRANSF as [f0 xf MATCHF|]; subst. eexists. split.
+  - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split.
     + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto.
     + erewrite preserv_fnparams; eauto.
-      econstructor; eauto. apply revmap_entrypoint. assumption.
+      econstructor; eauto. apply dupmap_entrypoint. assumption.
 (* exec_function_external *)
   - inversion TRANSF as [|]; subst. eexists. split.
     + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
@@ -475,7 +477,7 @@ Proof.
 (* exec_return *)
   - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split.
     + constructor.
-    + inv H1. constructor; assumption.
+    + inv H1. econstructor; eauto.
 Qed.
 
 Theorem transf_program_correct: