Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):

the new Lineartyping can't keep track of single floats that were spilled.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 661 insertions, 1076 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index f4fcd6e..f830d79 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -368,7 +368,7 @@ End IndexedEqKind.
 
 Module OrderedEqKind := OrderedIndexed(IndexedEqKind).
 
-(** This is an order over equations that is lexicographic on [ereg], then
+(** This is an order over equations that is lexicgraphic on [ereg], then
   [eloc], then [ekind]. *)
 
 Module OrderedEquation <: OrderedType.
@@ -609,6 +609,20 @@ Definition subst_loc (l1 l2: loc) (e: eqs) : option eqs :=
      (EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e))
      (Some e).
 
+(** [loc_type_compat env l e] checks that for all equations [r = l] in [e],
+  the type [env r] of [r] is compatible with the type of [l]. *)
+
+Definition sel_type (k: equation_kind) (ty: typ) : typ :=
+  match k with
+  | Full => ty
+  | Low | High => Tint
+  end.
+
+Definition loc_type_compat (env: regenv) (l: loc) (e: eqs) : bool :=
+  EqSet2.for_all_between
+    (fun q => subtype (sel_type (ekind q) (env (ereg q))) (Loc.type l))
+    (select_loc_l l) (select_loc_h l) (eqs2 e).
+
 (** [add_equations [r1...rN] [m1...mN] e] adds to [e] the [N] equations
     [ri = R mi [Full]].  Return [None] if the two lists have different lengths.
 *)
@@ -759,18 +773,25 @@ Definition destroyed_by_move (src dst: loc) :=
   | _, _ => destroyed_by_op Omove
   end.
 
+Definition well_typed_move (env: regenv) (dst: loc) (e: eqs) : bool :=
+  match dst with
+  | R r => true
+  | S sl ofs ty => loc_type_compat env dst e
+  end.
+
 (** Simulate the effect of a sequence of moves [mv] on a set of
   equations [e].  The set [e] is the equations that must hold
   after the sequence of moves.  Return the set of equations that
   must hold before the sequence of moves.  Return [None] if the
   set of equations [e] cannot hold after the sequence of moves. *)
 
-Fixpoint track_moves (mv: moves) (e: eqs) : option eqs :=
+Fixpoint track_moves (env: regenv) (mv: moves) (e: eqs) : option eqs :=
   match mv with
   | nil => Some e
   | (src, dst) :: mv =>
-      do e1 <- track_moves mv e;
+      do e1 <- track_moves env mv e;
       assertion (can_undef_except dst (destroyed_by_move src dst)) e1;
+      assertion (well_typed_move env dst e1);
       subst_loc dst src e1
   end.
 
@@ -803,89 +824,89 @@ Definition kind_second_word := if Archi.big_endian then Low else High.
   equations that must hold "before" these instructions, or [None] if
   impossible. *)
 
-Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option eqs :=
+Definition transfer_aux (f: RTL.function) (env: regenv) (shape: block_shape) (e: eqs) : option eqs :=
   match shape with
   | BSnop mv s =>
-      track_moves mv e
+      track_moves env mv e
   | BSmove src dst mv s =>
-      track_moves mv (subst_reg dst src e)
+      track_moves env mv (subst_reg dst src e)
   | BSmakelong src1 src2 dst mv s =>
       let e1 := subst_reg_kind dst High src1 Full e in
       let e2 := subst_reg_kind dst Low src2 Full e1 in
       assertion (reg_unconstrained dst e2);
-      track_moves mv e2
+      track_moves env mv e2
   | BSlowlong src dst mv s =>
       let e1 := subst_reg_kind dst Full src Low e in
       assertion (reg_unconstrained dst e1);
-      track_moves mv e1
+      track_moves env mv e1
   | BShighlong src dst mv s =>
       let e1 := subst_reg_kind dst Full src High e in
       assertion (reg_unconstrained dst e1);
-      track_moves mv e1
+      track_moves env mv e1
   | BSop op args res mv1 args' res' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       do e2 <- transfer_use_def args res args' res' (destroyed_by_op op) e1;
-      track_moves mv1 e2
+      track_moves env mv1 e2
   | BSopdead op args res mv s =>
       assertion (reg_unconstrained res e);
-      track_moves mv e
+      track_moves env mv e
   | BSload chunk addr args dst mv1 args' dst' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1;
-      track_moves mv1 e2
+      track_moves env mv1 e2
   | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s =>
-      do e1 <- track_moves mv3 e;
+      do e1 <- track_moves env mv3 e;
       let e2 := remove_equation (Eq kind_second_word dst (R dst2')) e1 in
       assertion (loc_unconstrained (R dst2') e2);
       assertion (can_undef (destroyed_by_load Mint32 addr') e2);
       do e3 <- add_equations args args2' e2;
-      do e4 <- track_moves mv2 e3;
+      do e4 <- track_moves env mv2 e3;
       let e5 := remove_equation (Eq kind_first_word dst (R dst1')) e4 in
       assertion (loc_unconstrained (R dst1') e5);
       assertion (can_undef (destroyed_by_load Mint32 addr) e5);
       assertion (reg_unconstrained dst e5);
       do e6 <- add_equations args args1' e5;
-      track_moves mv1 e6
+      track_moves env mv1 e6
   | BSload2_1 addr args dst mv1 args' dst' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       let e2 := remove_equation (Eq kind_first_word dst (R dst')) e1 in
       assertion (reg_loc_unconstrained dst (R dst') e2);
       assertion (can_undef (destroyed_by_load Mint32 addr) e2);
       do e3 <- add_equations args args' e2;
-      track_moves mv1 e3
+      track_moves env mv1 e3
   | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       let e2 := remove_equation (Eq kind_second_word dst (R dst')) e1 in
       assertion (reg_loc_unconstrained dst (R dst') e2);
       assertion (can_undef (destroyed_by_load Mint32 addr') e2);
       do e3 <- add_equations args args' e2;
-      track_moves mv1 e3
+      track_moves env mv1 e3
   | BSloaddead chunk addr args dst mv s =>
       assertion (reg_unconstrained dst e);
-      track_moves mv e
+      track_moves env mv e
   | BSstore chunk addr args src mv args' src' s =>
       assertion (can_undef (destroyed_by_store chunk addr) e);
       do e1 <- add_equations (src :: args) (src' :: args') e;
-      track_moves mv e1
+      track_moves env mv e1
   | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s =>
       assertion (can_undef (destroyed_by_store Mint32 addr') e);
       do e1 <- add_equations args args2' 
                   (add_equation (Eq kind_second_word src (R src2')) e);
-      do e2 <- track_moves mv2 e1;
+      do e2 <- track_moves env mv2 e1;
       assertion (can_undef (destroyed_by_store Mint32 addr) e2);
       do e3 <- add_equations args args1' 
                   (add_equation (Eq kind_first_word src (R src1')) e2);
-      track_moves mv1 e3
+      track_moves env mv1 e3
   | BScall sg ros args res mv1 ros' mv2 s =>
       let args' := loc_arguments sg in
       let res' := map R (loc_result sg) in
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       do e2 <- remove_equations_res res (sig_res sg) res' e1;
       assertion (forallb (fun l => reg_loc_unconstrained res l e2) res');
       assertion (no_caller_saves e2);
       do e3 <- add_equation_ros ros ros' e2;
       do e4 <- add_equations_args args (sig_args sg) args' e3;
-      track_moves mv1 e4
+      track_moves env mv1 e4
   | BStailcall sg ros args mv1 ros' =>
       let args' := loc_arguments sg in
       assertion (tailcall_is_possible sg);
@@ -893,9 +914,9 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option
       assertion (ros_compatible_tailcall ros');
       do e1 <- add_equation_ros ros ros' empty_eqs;
       do e2 <- add_equations_args args (sig_args sg) args' e1;
-      track_moves mv1 e2
+      track_moves env mv1 e2
   | BSbuiltin ef args res mv1 args' res' mv2 s =>
-      do e1 <- track_moves mv2 e;
+      do e1 <- track_moves env mv2 e;
       let args' := map R args' in
       let res' := map R res' in
       do e2 <- remove_equations_res res (sig_res (ef_sig ef)) res' e1;
@@ -903,23 +924,23 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option
       assertion (forallb (fun l => loc_unconstrained l e2) res');
       assertion (can_undef (destroyed_by_builtin ef) e2);
       do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2;
-      track_moves mv1 e3
+      track_moves env mv1 e3
   | BSannot txt typ args res mv1 args' s =>
       do e1 <- add_equations_args args (annot_args_typ typ) args' e;
-      track_moves mv1 e1
+      track_moves env mv1 e1
   | BScond cond args mv args' s1 s2 =>
       assertion (can_undef (destroyed_by_cond cond) e);
       do e1 <- add_equations args args' e;
-      track_moves mv e1
+      track_moves env mv e1
   | BSjumptable arg mv arg' tbl =>
       assertion (can_undef destroyed_by_jumptable e);
-      track_moves mv (add_equation (Eq Full arg (R arg')) e)
+      track_moves env mv (add_equation (Eq Full arg (R arg')) e)
   | BSreturn None mv =>
-      track_moves mv empty_eqs
+      track_moves env mv empty_eqs
   | BSreturn (Some arg) mv =>
       let arg' := map R (loc_result (RTL.fn_sig f)) in
       do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs;
-      track_moves mv e1
+      track_moves env mv e1
   end.
 
 (** The main transfer function for the dataflow analysis.  Like [transfer_aux],
@@ -927,7 +948,7 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option
   equations that must hold "after".  It also handles error propagation
   and reporting. *)
 
-Definition transfer (f: RTL.function) (shapes: PTree.t block_shape)
+Definition transfer (f: RTL.function) (env: regenv) (shapes: PTree.t block_shape)
                     (pc: node) (after: res eqs) : res eqs :=
   match after with
   | Error _ => after
@@ -935,7 +956,7 @@ Definition transfer (f: RTL.function) (shapes: PTree.t block_shape)
       match shapes!pc with
       | None => Error(MSG "At PC " :: POS pc :: MSG ": unmatched block" :: nil)
       | Some shape =>
-          match transfer_aux f shape e with
+          match transfer_aux f env shape e with
           | None => Error(MSG "At PC " :: POS pc :: MSG ": invalid register allocation" :: nil)
           | Some e' => OK e'
           end
@@ -1083,8 +1104,8 @@ Definition successors_block_shape (bsh: block_shape) : list node :=
   | BSreturn optarg mv => nil
   end.
 
-Definition analyze (f: RTL.function) (bsh: PTree.t block_shape) :=
-  DS.fixpoint_allnodes bsh successors_block_shape (transfer f bsh).
+Definition analyze (f: RTL.function) (env: regenv) (bsh: PTree.t block_shape) :=
+  DS.fixpoint_allnodes bsh successors_block_shape (transfer f env bsh).
 
 (** * Validating and translating functions and programs *)
 
@@ -1118,9 +1139,9 @@ Function compat_entry (rparams: list reg) (tys: list typ) (lparams: list loc) (e
   and stack size. *)
 
 Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function)
-                                 (e1: eqs) : option unit :=
+                                 (env: regenv) (e1: eqs) : option unit :=
   do mv <- pair_entrypoints rtl ltl;
-  do e2 <- track_moves mv e1;
+  do e2 <- track_moves env mv e1;
   assertion (compat_entry (RTL.fn_params rtl)
                           (sig_args (RTL.fn_sig rtl))
                           (loc_parameters (RTL.fn_sig rtl)) e2);
@@ -1133,10 +1154,10 @@ Local Close Scope option_monad_scope.
 Local Open Scope error_monad_scope.
 
 Definition check_entrypoints (rtl: RTL.function) (ltl: LTL.function)
-                             (bsh: PTree.t block_shape)
+                             (env: regenv) (bsh: PTree.t block_shape)
                              (a: PMap.t LEq.t): res unit :=
-  do e1 <- transfer rtl bsh (RTL.fn_entrypoint rtl) a!!(RTL.fn_entrypoint rtl);
-  match check_entrypoints_aux rtl ltl e1 with
+  do e1 <- transfer rtl env bsh (RTL.fn_entrypoint rtl) a!!(RTL.fn_entrypoint rtl);
+  match check_entrypoints_aux rtl ltl env e1 with
   | None => Error (msg "invalid register allocation at entry point")
   | Some _ => OK tt
   end.
@@ -1145,11 +1166,11 @@ Definition check_entrypoints (rtl: RTL.function) (ltl: LTL.function)
   a source RTL function and an LTL function generated by the external
   register allocator. *)
 
-Definition check_function (rtl: RTL.function) (ltl: LTL.function) : res unit :=
+Definition check_function (rtl: RTL.function) (ltl: LTL.function) (env: regenv) : res unit :=
   let bsh := pair_codes rtl ltl in
-  match analyze rtl bsh with
+  match analyze rtl env bsh with
   | None => Error (msg "allocation analysis diverges")
-  | Some a => check_entrypoints rtl ltl bsh a
+  | Some a => check_entrypoints rtl ltl env bsh a
   end.
 
 (** [regalloc] is the external register allocator.  It is written in OCaml
@@ -1165,7 +1186,7 @@ Definition transf_function (f: RTL.function) : res LTL.function :=
   | OK env =>
       match regalloc f with
       | Error m => Error m
-      | OK tf => do x <- check_function f tf; OK tf
+      | OK tf => do x <- check_function f tf env; OK tf
       end
   end.
 
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 9303878..4c39fee 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -451,7 +451,7 @@ Lemma add_equations_args_lessdef:
   forall rs ls rl tyl ll e e',
   add_equations_args rl tyl ll e = Some e' ->
   satisf rs ls e' ->
-  Val.has_type_list (rs##rl) (normalize_list tyl) ->
+  Val.has_type_list (rs##rl) tyl ->
   Val.lessdef_list (rs##rl) (decode_longs tyl (map ls ll)).
 Proof.
   intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros.
@@ -648,7 +648,7 @@ Lemma loc_unconstrained_satisf:
 Proof.
   intros; red; intros. 
   destruct (OrderedEquation.eq_dec q (Eq k r l)). 
-  subst q; simpl. unfold l; rewrite Locmap.gss. auto.
+  subst q; simpl. unfold l; rewrite Locmap.gss_reg. auto.
   assert (EqSet.In q (remove_equation (Eq k r l) e)).
     simpl. ESD.fsetdec.  
   rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto. 
@@ -674,7 +674,7 @@ Lemma parallel_assignment_satisf:
 Proof.
   intros; red; intros.
   destruct (OrderedEquation.eq_dec q (Eq k r l)).
-  subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss; auto.
+  subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss_reg; auto.
   assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)).
     simpl. ESD.fsetdec.
   exploit reg_loc_unconstrained_sound; eauto. intros [A B].
@@ -702,11 +702,11 @@ Proof.
   rewrite <- H5 in H2. simpl in H2. InvBooleans. simpl.
   destruct (OrderedEquation.eq_dec q (Eq Low res l2)).
   subst q; simpl. rewrite Regmap.gss.
-  destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
+  destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg.
   apply Val.loword_lessdef; auto. 
   destruct (OrderedEquation.eq_dec q (Eq High res l1)).
   subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto.
-  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
+  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg.
   apply Val.hiword_lessdef; auto.
   assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. 
   rewrite Regmap.gso. rewrite ! Locmap.gso. auto. 
@@ -719,7 +719,7 @@ Proof.
   set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *.
   destruct (OrderedEquation.eq_dec q (Eq Full res l1)). 
   subst q; simpl. rewrite Regmap.gss.
-  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
+  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss_reg.
   auto.
   assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec. 
   simpl. rewrite Regmap.gso. rewrite Locmap.gso. auto.
@@ -969,7 +969,6 @@ Proof.
   split. apply eqs_same; auto. auto. 
 Qed.
 
-(*
 Lemma loc_type_compat_charact:
   forall env l e q,
   loc_type_compat env l e = true ->
@@ -1009,8 +1008,7 @@ Proof.
   destruct (rs#r); exact I.
   eelim Loc.diff_not_eq. eexact A. auto.
 Qed.
-*)
-(*
+
 Remark val_lessdef_normalize:
   forall v v' ty,
   Val.has_type v ty -> Val.lessdef v v' ->
@@ -1018,19 +1016,23 @@ Remark val_lessdef_normalize:
 Proof.
   intros. inv H0. rewrite Val.load_result_same; auto. auto. 
 Qed.
-*)
 
 Lemma subst_loc_satisf:
   forall env src dst rs ls e e',
   subst_loc dst src e = Some e' ->
-  (*well_typed_move env dst e = true ->*)
+  well_typed_move env dst e = true ->
   wt_regset env rs ->
   satisf rs ls e' ->
   satisf rs (Locmap.set dst (ls src) ls) e.
 Proof.
   intros; red; intros.
   exploit in_subst_loc; eauto. intros [[A B] | [A B]].
-  subst dst. rewrite Locmap.gss. apply (H1 _ B).
+  subst dst. rewrite Locmap.gss.
+  destruct q as [k r l]; simpl in *.
+  exploit well_typed_move_charact; eauto.
+  destruct l as [mr | sl ofs ty]; intros.
+  apply (H2 _ B). 
+  apply val_lessdef_normalize; auto. apply (H2 _ B). 
   rewrite Locmap.gso; auto.
 Qed.
 
@@ -1077,18 +1079,22 @@ Proof.
 Qed.
 
 Lemma subst_loc_undef_satisf:
-  forall src dst rs ls ml e e',
+  forall env src dst rs ls ml e e',
   subst_loc dst src e = Some e' ->
-  (*well_typed_move env dst e = true ->*)
+  well_typed_move env dst e = true ->
   can_undef_except dst ml e = true ->
-  (*wt_regset env rs ->*)
+  wt_regset env rs ->
   satisf rs ls e' ->
   satisf rs (Locmap.set dst (ls src) (undef_regs ml ls)) e.
 Proof.
   intros; red; intros.
   exploit in_subst_loc; eauto. intros [[A B] | [A B]].
   subst dst. rewrite Locmap.gss.
-  destruct q as [k r l]; simpl in *. apply (H1 _ B). 
+  destruct q as [k r l]; simpl in *.
+  exploit well_typed_move_charact; eauto.
+  destruct l as [mr | sl ofs ty]; intros.
+  apply (H3 _ B). 
+  apply val_lessdef_normalize; auto. apply (H3 _ B). 
   rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto. 
   eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto.
 Qed.
@@ -1330,27 +1336,27 @@ Qed.
 (** * Properties of the dataflow analysis *)
 
 Lemma analyze_successors:
-  forall f bsh an pc bs s e,
-  analyze f bsh = Some an ->
+  forall f env bsh an pc bs s e,
+  analyze f env bsh = Some an ->
   bsh!pc = Some bs ->
   In s (successors_block_shape bs) ->
   an!!pc = OK e ->
-  exists e', transfer f bsh s an!!s = OK e' /\ EqSet.Subset e' e.
+  exists e', transfer f env bsh s an!!s = OK e' /\ EqSet.Subset e' e.
 Proof.
   unfold analyze; intros. exploit DS.fixpoint_allnodes_solution; eauto.
-  rewrite H2. unfold DS.L.ge. destruct (transfer f bsh s an#s); intros.
+  rewrite H2. unfold DS.L.ge. destruct (transfer f env bsh s an#s); intros.
   exists e0; auto. 
   contradiction.
 Qed.
 
 Lemma satisf_successors:
-  forall f bsh an pc bs s e rs ls,
-  analyze f bsh = Some an ->
+  forall f env bsh an pc bs s e rs ls,
+  analyze f env bsh = Some an ->
   bsh!pc = Some bs ->
   In s (successors_block_shape bs) ->
   an!!pc = OK e ->
   satisf rs ls e ->
-  exists e', transfer f bsh s an!!s = OK e' /\ satisf rs ls e'.
+  exists e', transfer f env bsh s an!!s = OK e' /\ satisf rs ls e'.
 Proof.
   intros. exploit analyze_successors; eauto. intros [e' [A B]]. 
   exists e'; split; auto. eapply satisf_incr; eauto.
@@ -1360,12 +1366,13 @@ Qed.
 
 Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop :=
   | transf_function_spec_intro:  
-      forall an mv k e1 e2,
-      analyze f (pair_codes f tf) = Some an ->
+      forall env an mv k e1 e2,
+      wt_function f env ->
+      analyze f env (pair_codes f tf) = Some an ->
       (LTL.fn_code tf)!(LTL.fn_entrypoint tf) = Some(expand_moves mv (Lbranch (RTL.fn_entrypoint f) :: k)) ->
       wf_moves mv ->
-      transfer f (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 ->
-      track_moves mv e1 = Some e2 ->
+      transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 ->
+      track_moves env mv e1 = Some e2 ->
       compat_entry (RTL.fn_params f) (sig_args (RTL.fn_sig f)) (loc_parameters (fn_sig tf)) e2 = true ->
       can_undef destroyed_at_function_entry e2 = true ->
       RTL.fn_stacksize f = LTL.fn_stacksize tf ->
@@ -1380,33 +1387,36 @@ Proof.
   unfold transf_function; intros.
   destruct (type_function f) as [env|] eqn:TY; try discriminate.
   destruct (regalloc f); try discriminate.
-  destruct (check_function f f0) as [] eqn:?; inv H.
+  destruct (check_function f f0 env) as [] eqn:?; inv H.
   unfold check_function in Heqr. 
-  destruct (analyze f (pair_codes f tf)) as [an|] eqn:?; try discriminate.
+  destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate.
   monadInv Heqr. 
-  destruct (check_entrypoints_aux f tf x) as [y|] eqn:?; try discriminate.
+  destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate.
   unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv.
   exploit extract_moves_sound; eauto. intros [A B]. subst b.
   exploit check_succ_sound; eauto. intros [k EQ1]. subst b0.
-  econstructor; eauto. congruence. 
+  econstructor; eauto. eapply type_function_correct; eauto. congruence. 
 Qed.
 
 Lemma invert_code:
-  forall f tf pc i opte e,
+  forall f env tf pc i opte e,
+  wt_function f env ->
   (RTL.fn_code f)!pc = Some i ->
-  transfer f (pair_codes f tf) pc opte = OK e ->
+  transfer f env (pair_codes f tf) pc opte = OK e ->
   exists eafter, exists bsh, exists bb,
   opte = OK eafter /\ 
   (pair_codes f tf)!pc = Some bsh /\
   (LTL.fn_code tf)!pc = Some bb /\
   expand_block_shape bsh i bb /\
-  transfer_aux f bsh eafter = Some e.
+  transfer_aux f env bsh eafter = Some e /\
+  wt_instr f env i.
 Proof.
-  intros. destruct opte as [eafter|]; simpl in H0; try discriminate. exists eafter.
+  intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter.
   destruct (pair_codes f tf)!pc as [bsh|] eqn:?; try discriminate. exists bsh. 
   exploit matching_instr_block; eauto. intros [bb [A B]].
-  destruct (transfer_aux f bsh eafter) as [e1|] eqn:?; inv H0. 
-  exists bb. tauto. 
+  destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H1. 
+  exists bb. exploit wt_instr_at; eauto.
+  tauto. 
 Qed.
 
 (** * Semantic preservation *)
@@ -1480,10 +1490,11 @@ Proof.
 Qed.
 
 Lemma exec_moves:
-  forall mv rs s f sp bb m e e' ls,
-  track_moves mv e = Some e' ->
+  forall mv env rs s f sp bb m e e' ls,
+  track_moves env mv e = Some e' ->
   wf_moves mv ->
   satisf rs ls e' ->
+  wt_regset env rs ->
   exists ls',
     star step tge (Block s f sp (expand_moves mv bb) ls m)
                E0 (Block s f sp bb ls' m)
@@ -1495,7 +1506,7 @@ Opaque destroyed_by_op.
 - unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto.
   (* step *)
 - destruct a as [src dst]. unfold expand_moves. simpl. 
-  destruct (track_moves mv e) as [e1|] eqn:?; MonadInv.
+  destruct (track_moves env mv e) as [e1|] eqn:?; MonadInv.
   assert (wf_moves mv). red; intros. apply H0; auto with coqlib. 
   destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst].
   (* reg-reg *)
@@ -1521,13 +1532,17 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
       sg.(sig_res) = Some Tint ->
       match_stackframes nil nil sg
   | match_stackframes_cons:
-      forall res f sp pc rs s tf bb ls ts sg an e
+      forall res f sp pc rs s tf bb ls ts sg an e env
         (STACKS: match_stackframes s ts (fn_sig tf))
         (FUN: transf_function f = OK tf)
-        (ANL: analyze f (pair_codes f tf) = Some an)
-        (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e)
+        (ANL: analyze f env (pair_codes f tf) = Some an)
+        (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e)
+        (WTF: wt_function f env)
+        (WTRS: wt_regset env rs)
+        (WTRES: subtype (proj_sig_res sg) (env res) = true)
         (STEPS: forall v ls1 m,
            Val.lessdef_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) ->
+           Val.has_type v (env res) ->
            agree_callee_save ls ls1 ->
            exists ls2,
            star LTL.step tge (Block ts tf sp bb ls1 m)
@@ -1540,13 +1555,15 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
 
 Inductive match_states: RTL.state -> LTL.state -> Prop :=
   | match_states_intro:
-      forall s f sp pc rs m ts tf ls m' an e
+      forall s f sp pc rs m ts tf ls m' an e env
         (STACKS: match_stackframes s ts (fn_sig tf))
         (FUN: transf_function f = OK tf)
-        (ANL: analyze f (pair_codes f tf) = Some an)
-        (EQ: transfer f (pair_codes f tf) pc an!!pc = OK e)
+        (ANL: analyze f env (pair_codes f tf) = Some an)
+        (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e)
         (SAT: satisf rs ls e)
-        (MEM: Mem.extends m m'),
+        (MEM: Mem.extends m m')
+        (WTF: wt_function f env)
+        (WTRS: wt_regset env rs),
       match_states (RTL.State s f sp pc rs m)
                    (LTL.State ts tf sp pc ls m')
   | match_states_call:
@@ -1555,7 +1572,8 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
         (FUN: transf_fundef f = OK tf)
         (ARGS: Val.lessdef_list args (decode_longs (sig_args (funsig tf)) (map ls (loc_arguments (funsig tf)))))
         (AG: agree_callee_save (parent_locset ts) ls)
-        (MEM: Mem.extends m m'),
+        (MEM: Mem.extends m m')
+        (WTARGS: Val.has_type_list args (sig_args (funsig tf))),
       match_states (RTL.Callstate s f args m)
                    (LTL.Callstate ts tf ls m')
   | match_states_return:
@@ -1563,7 +1581,8 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
         (STACKS: match_stackframes s ts sg)
         (RES: Val.lessdef_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg))))
         (AG: agree_callee_save (parent_locset ts) ls)
-        (MEM: Mem.extends m m'),
+        (MEM: Mem.extends m m')
+        (WTRES: Val.has_type res (proj_sig_res sg)),
       match_states (RTL.Returnstate s res m)
                    (LTL.Returnstate ts ls m').
 
@@ -1576,13 +1595,14 @@ Proof.
   intros. inv H. 
   constructor. congruence.
   econstructor; eauto.
+  unfold proj_sig_res in *. rewrite H0; auto. 
   intros. unfold loc_result in H; rewrite H0 in H; eauto. 
 Qed.
 
 Ltac UseShape :=
   match goal with
-  | [ CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ = OK _ |- _ ] =>
-      destruct (invert_code _ _ _ _ _ _ CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR); 
+  | [ WT: wt_function _ _, CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ _ = OK _ |- _ ] =>
+      destruct (invert_code _ _ _ _ _ _ _ WT CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI); 
       inv EBS; unfold transfer_aux in TR; MonadInv
   end.
 
@@ -1599,8 +1619,10 @@ Proof.
   { generalize args (type_of_addressing addr) H0 H1 H5.
     induction args0; simpl; intros.
     contradiction.
-    destruct l. discriminate. inv H4. 
-    destruct H2. subst a. apply H3; auto with coqlib. 
+    destruct l. discriminate. InvBooleans. 
+    destruct H2. subst a. 
+    assert (t = Tint) by auto with coqlib. subst t. 
+    destruct (env r); auto || discriminate. 
     eauto with coqlib. 
   }
   red; intros; subst r. rewrite H in H8; discriminate.
@@ -1610,11 +1632,11 @@ Qed.
     "plus" kind. *)
 
 Lemma step_simulation:
-  forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 ->
+  forall S1 t S2, RTL.step ge S1 t S2 ->
   forall S1', match_states S1 S1' ->
   exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'.
 Proof.
-  induction 1; intros WT S1' MS; inv MS; try UseShape.
+  induction 1; intros S1' MS; inv MS; try UseShape.
 
 (* nop *)
   exploit exec_moves; eauto. intros [ls1 [X Y]]. 
@@ -1626,7 +1648,8 @@ Proof.
   econstructor; eauto. 
 
 (* op move *)
-- simpl in H0. inv H0.  
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  simpl in H0. inv H0.  
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1637,7 +1660,8 @@ Proof.
   econstructor; eauto.
 
 (* op makelong *)
-- simpl in H0. inv H0. 
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1649,7 +1673,8 @@ Proof.
   econstructor; eauto.
 
 (* op lowlong *)
-- simpl in H0. inv H0. 
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1661,7 +1686,8 @@ Proof.
   econstructor; eauto.
 
 (* op highlong *)
-- simpl in H0. inv H0. 
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  simpl in H0. inv H0. 
   exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. 
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -1673,7 +1699,8 @@ Proof.
   econstructor; eauto.
 
 (* op regular *)
-- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
+  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   exploit transfer_use_def_satisf; eauto. intros [X Y].
   exploit eval_operation_lessdef; eauto. intros [v' [F G]]. 
   exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]].
@@ -1697,9 +1724,11 @@ Proof.
   eapply reg_unconstrained_satisf; eauto. 
   intros [enext [U V]]. 
   econstructor; eauto.
+  eapply wt_exec_Iop; eauto. 
 
 (* load regular *)
-- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   exploit transfer_use_def_satisf; eauto. intros [X Y].
   exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
   exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. 
@@ -1715,7 +1744,8 @@ Proof.
   econstructor; eauto.
 
 (* load pair *)
-- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+  exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
@@ -1736,8 +1766,7 @@ Proof.
   assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')).
   { replace (rs##args) with ((rs#dst<-v)##args). 
     eapply add_equations_lessdef; eauto. 
-    apply list_map_exten; intros. rewrite Regmap.gso; auto.
-    exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
+    apply list_map_exten; intros. rewrite Regmap.gso; auto. 
     eapply addressing_not_long; eauto. 
   }
   exploit eval_addressing_lessdef. eexact LD3.
@@ -1769,7 +1798,8 @@ Proof.
   econstructor; eauto.
 
 (* load first word of a pair *)
-- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+  exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
@@ -1799,7 +1829,8 @@ Proof.
   econstructor; eauto.
 
 (* load second word of a pair *)
-- exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+  exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
@@ -1839,6 +1870,7 @@ Proof.
   eapply reg_unconstrained_satisf; eauto. 
   intros [enext [U V]]. 
   econstructor; eauto.
+  eapply wt_exec_Iload; eauto.
 
 (* store *)
 - exploit exec_moves; eauto. intros [ls1 [X Y]].
@@ -1918,19 +1950,21 @@ Proof.
   exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]].
   econstructor; eauto.
   econstructor; eauto.
+  inv WTI. rewrite SIG. auto. 
   intros. exploit (exec_moves mv2). eauto. eauto. 
   eapply function_return_satisf with (v := v) (ls_before := ls1) (ls_after := ls0); eauto.
   eapply add_equation_ros_satisf; eauto. 
   eapply add_equations_args_satisf; eauto. 
   congruence.
+  apply wt_regset_assign; auto.
   intros [ls2 [A2 B2]].
   exists ls2; split. 
   eapply star_right. eexact A2. constructor. traceEq.
   apply satisf_incr with eafter; auto. 
   rewrite SIG. eapply add_equations_args_lessdef; eauto.
-  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
-  inv WTI. rewrite <- H7. apply wt_regset_list; auto. 
+  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
   simpl. red; auto.
+  inv WTI. rewrite SIG. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
 
 (* tailcall *)
 - set (sg := RTL.funsig fd) in *.
@@ -1951,16 +1985,16 @@ Proof.
   eapply match_stackframes_change_sig; eauto. rewrite SIG. rewrite e0. decEq.
   destruct (transf_function_inv _ _ FUN); auto.
   rewrite SIG. rewrite return_regs_arg_values; auto. eapply add_equations_args_lessdef; eauto.
-  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
-  inv WTI. rewrite <- H6. apply wt_regset_list; auto. 
+  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
   apply return_regs_agree_callee_save.
+  rewrite SIG. inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
 
 (* builtin *)
-- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
+- assert (WTRS': wt_regset env (rs#res <- v)) by (eapply wt_exec_Ibuiltin; eauto).
+  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. 
   exploit external_call_mem_extends; eauto.
   eapply add_equations_args_lessdef; eauto.
-  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
-  inv WTI. rewrite <- H4. apply wt_regset_list; auto. 
+  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
   intros [v' [m'' [F [G [J K]]]]].
   assert (E: map ls1 (map R args') = reglist ls1 args').
   { unfold reglist. rewrite list_map_compose. auto. }
@@ -1990,8 +2024,7 @@ Proof.
 (* annot *)
 - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. 
   exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto.
-  exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
-  inv WTI. simpl in H4. rewrite <- H4. apply wt_regset_list; auto. 
+  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. 
   intros [v' [m'' [F [G [J K]]]]].
   assert (v = Vundef). red in H0; inv H0. auto.
   econstructor; split.
@@ -2009,6 +2042,7 @@ Proof.
   econstructor; eauto.
   change (destroyed_by_builtin (EF_annot txt typ)) with (@nil mreg). 
   simpl. subst v. assumption.
+  apply wt_regset_assign; auto. subst v. constructor. 
 
 (* cond *)
 - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
@@ -2040,43 +2074,45 @@ Proof.
 
 (* return *)
 - destruct (transf_function_inv _ _ FUN). 
-  exploit Mem.free_parallel_extends; eauto. rewrite H9. intros [m'' [P Q]].
-  destruct or as [r|]; MonadInv.
+  exploit Mem.free_parallel_extends; eauto. rewrite H10. intros [m'' [P Q]].
+  inv WTI; MonadInv.
+  (* without an argument *)
++ exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
+  econstructor; split.
+  eapply plus_left. econstructor; eauto. 
+  eapply star_right. eexact A1.
+  econstructor. eauto. eauto. traceEq.
+  simpl. econstructor; eauto.
+  unfold encode_long, loc_result. rewrite <- H11; rewrite H13. simpl; auto.
+  apply return_regs_agree_callee_save.
+  constructor.
   (* with an argument *)
 + exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
   eapply star_right. eexact A1.
   econstructor. eauto. eauto. traceEq.
-  simpl. econstructor; eauto. rewrite <- H10.
+  simpl. econstructor; eauto. rewrite <- H11.
   replace (map (return_regs (parent_locset ts) ls1) (map R (loc_result (RTL.fn_sig f))))
      with (map ls1 (map R (loc_result (RTL.fn_sig f)))).
   eapply add_equations_res_lessdef; eauto.
   rewrite !list_map_compose. apply list_map_exten; intros.
   unfold return_regs. apply pred_dec_true. eapply loc_result_caller_save; eauto.
   apply return_regs_agree_callee_save.
-
-  (* without an argument *)
-+ assert (SG: f.(RTL.fn_sig).(sig_res) = None).
-  { exploit wt_instr_inv; eauto. intros (env & WTI & WTRS). 
-    inv WTI; auto. }
-  exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
-  econstructor; split.
-  eapply plus_left. econstructor; eauto. 
-  eapply star_right. eexact A1.
-  econstructor. eauto. eauto. traceEq.
-  simpl. econstructor; eauto.
-  unfold encode_long, loc_result. rewrite <- H10. rewrite SG. simpl; auto.
-  apply return_regs_agree_callee_save.
+  unfold proj_sig_res. rewrite <- H11; rewrite H13. 
+  eapply Val.has_subtype; eauto. 
 
 (* internal function *)
 - monadInv FUN. simpl in *.
   destruct (transf_function_inv _ _ EQ). 
-  exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H7; apply Zle_refl. 
+  exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl. 
   intros [m'' [U V]].
+  assert (WTRS: wt_regset env (init_regs args (fn_params f))).
+  { apply wt_init_regs. inv H0. eapply Val.has_subtype_list; eauto. congruence. }
   exploit (exec_moves mv). eauto. eauto.
     eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. 
-    rewrite call_regs_param_values. rewrite H8. eexact ARGS.
+    rewrite call_regs_param_values. rewrite H9. eexact ARGS.
+    exact WTRS.
   intros [ls1 [A B]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
@@ -2108,13 +2144,15 @@ Proof.
   exploit list_in_map_inv; eauto. intros [r [A B]]; subst l'. 
   destruct l; simpl; auto. red; intros; subst r0; elim H0.
   eapply loc_result_caller_save; eauto.
+  simpl. eapply external_call_well_typed; eauto. 
  
 (* return *)
 - inv STACKS.
-  exploit STEPS; eauto. intros [ls2 [A B]].
+  exploit STEPS; eauto. eapply Val.has_subtype; eauto. intros [ls2 [A B]].
   econstructor; split.
   eapply plus_left. constructor. eexact A. traceEq.
   econstructor; eauto.
+  apply wt_regset_assign; auto. eapply Val.has_subtype; eauto. 
 Qed.
 
 Lemma initial_states_simulation:
@@ -2135,6 +2173,7 @@ Proof.
   rewrite SIG; rewrite H3; simpl; auto.
   red; auto.
   apply Mem.extends_refl.
+  rewrite SIG; rewrite H3; simpl; auto.
 Qed.
 
 Lemma final_states_simulation:
@@ -2146,31 +2185,14 @@ Proof.
   unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. inv H3; auto. 
 Qed.
 
-Lemma wt_prog: wt_program prog.
-Proof.
-  red; intros. exploit transform_partial_program_succeeds; eauto. 
-  intros [tfd TF]. destruct f; simpl in *. 
-- monadInv TF. unfold transf_function in EQ.
-  destruct (type_function f) as [env|] eqn:TF; try discriminate.
-  econstructor. eapply type_function_correct; eauto.
-- constructor.
-Qed.
-
 Theorem transf_program_correct:
   forward_simulation (RTL.semantics prog) (LTL.semantics tprog).
 Proof.
-  set (ms := fun s s' => wt_state s /\ match_states s s').
-  eapply forward_simulation_plus with (match_states := ms). 
-- exact symbols_preserved.
-- intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. 
-  exists st2; split; auto. split; auto.
-  apply wt_initial_state with (p := prog); auto. exact wt_prog. 
-- intros. destruct H. eapply final_states_simulation; eauto. 
-- intros. destruct H0. 
-  exploit step_simulation; eauto. intros [s2' [A B]].
-  exists s2'; split. exact A. split.
-  eapply subject_reduction; eauto. eexact wt_prog. eexact H. 
-  auto.
+  eapply forward_simulation_plus.
+  eexact symbols_preserved.
+  eexact initial_states_simulation.
+  eexact final_states_simulation.
+  exact step_simulation. 
 Qed.
 
 End PRESERVATION.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index f1e3d41..73c5453 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -10,26 +10,20 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Type-checking Linear code. *)
+(** Typing rules for Linear. *)
 
-Require Import FSets.
-Require FSetAVL.
 Require Import Coqlib.
-Require Import Ordered.
-Require Import Maps.
-Require Import Iteration.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Events.
 Require Import Op.
-Require Import Machregs.
 Require Import Locations.
 Require Import Conventions.
 Require Import LTL.
 Require Import Linear.
 
-(** The typechecker for Linear enforce several properties useful for
+(** The typing rules for Linear enforce several properties useful for
   the proof of the [Stacking] pass:
 - for each instruction, the type of the result register or slot
   agrees with the type of values produced by the instruction;
@@ -37,120 +31,13 @@ Require Import Linear.
   accessed through [Lgetstack] and [Lsetstack] Linear instructions.
 *)
 
-(** * Tracking the flow of single-precision floats *)
-
-(** At each program point, we infer a set of machine registers
-  that are guaranteed to contain single-precision floats.
-  The inference is a simple forward dataflow analysis, iterating on the 
-  list of instructions until a fixpoint is reached.  The result of
-  the analysis is a map from labels to sets of machine registers
-  containing single-precision floats.  *)
-
-Module OrderedMreg := OrderedIndexed(IndexedMreg).
-Module Regset := FSetAVL.Make(OrderedMreg).
-
-Definition setreg (fs: Regset.t) (r: mreg) (t: typ) :=
-  if typ_eq t Tsingle then Regset.add r fs else Regset.remove r fs.
-
-Fixpoint setregs (fs: Regset.t) (rl: list mreg) (tl: list typ) :=
-  match rl, tl with
-  | nil, nil => fs
-  | r1 :: rs, t1 :: ts => setregs (setreg fs r1 t1) rs ts
-  | _, _ => fs
-  end.
-
-Definition copyreg (fs: Regset.t) (rd rs: mreg) :=
-  if Regset.mem rs fs then Regset.add rd fs else Regset.remove rd fs.
-
-Definition allregs :=
-  List.fold_right Regset.add Regset.empty
-                  (float_caller_save_regs ++ float_callee_save_regs).
-
-Definition destroyed_at_call_regs :=
-  List.fold_right Regset.add Regset.empty destroyed_at_call.
-
-Definition callregs (fs: Regset.t) :=
-  Regset.diff fs destroyed_at_call_regs.
-
-Definition labelmap := PMap.t Regset.t.
-
-Definition update_label (lbl: label) (fs: Regset.t) (lm: labelmap) : Regset.t * labelmap * bool :=
-  let fs1 := PMap.get lbl lm in
-  if Regset.subset fs1 fs
-  then (fs1, lm, false)
-  else let fs2 := Regset.inter fs fs1 in (fs2, PMap.set lbl fs2 lm, true).
-
-Fixpoint update_labels (lbls: list label) (fs: Regset.t) (lm: labelmap): labelmap * bool :=
-  match lbls with
-  | nil => (lm, false)
-  | lbl1 :: lbls =>
-      let '(fs1, lm1, changed1) := update_label lbl1 fs lm in
-      let '(lm2, changed2) := update_labels lbls fs lm1 in
-      (lm2, changed1 || changed2)
-  end.
-
-Fixpoint ana_code (lm: labelmap) (ch: bool) (fs: Regset.t) (c: code) : labelmap * bool :=
-  match c with
-  | nil => (lm, ch)
-  | Lgetstack sl ofs ty rd :: c =>
-      ana_code lm ch (setreg fs rd ty) c
-  | Lsetstack rs sl ofs ty :: c =>
-      ana_code lm ch fs c
-  | Lop op args dst :: c =>
-      match is_move_operation op args with
-      | Some src => ana_code lm ch (copyreg fs dst src) c
-      | None     => ana_code lm ch (setreg fs dst (snd (type_of_operation op))) c
-      end
-  | Lload chunk addr args dst :: c =>
-      ana_code lm ch (setreg fs dst (type_of_chunk chunk)) c
-  | Lstore chunk addr args src :: c =>
-      ana_code lm ch fs c
-  | Lcall sg ros :: c =>
-      ana_code lm ch (callregs fs) c
-  | Ltailcall sg ros :: c =>
-      ana_code lm ch allregs c
-  | Lbuiltin ef args res :: c =>
-      ana_code lm ch (setregs fs res (proj_sig_res' (ef_sig ef))) c
-  | Lannot ef args :: c =>
-      ana_code lm ch fs c
-  | Llabel lbl :: c =>
-      let '(fs1, lm1, ch1) := update_label lbl fs lm in
-      ana_code lm1 (ch || ch1) fs1 c
-  | Lgoto lbl :: c =>
-      let '(fs1, lm1, ch1) := update_label lbl fs lm in
-      ana_code lm1 (ch || ch1) allregs c
-  | Lcond cond args lbl :: c =>
-      let '(fs1, lm1, ch1) := update_label lbl fs lm in
-      ana_code lm1 (ch || ch1) fs c
-  | Ljumptable r lbls :: c =>
-      let '(lm1, ch1) := update_labels lbls fs lm in
-      ana_code lm1 (ch || ch1) allregs c
-  | Lreturn :: c =>
-      ana_code lm ch allregs c
-  end.
-
-Definition ana_iter (c: code) (lm: labelmap) : labelmap + labelmap :=
-  let '(lm1, ch) := ana_code lm false Regset.empty c in
-  if ch then inr _ lm1 else inl _ lm.
-
-Definition ana_function (f: function): option (PMap.t Regset.t) :=
-  PrimIter.iterate _ _ (ana_iter f.(fn_code)) (PMap.init allregs).
-
-(** * The type-checker *)
-
-(** The typing rules are presented as boolean-valued functions so that we
+(** The rules are presented as boolean-valued functions so that we
   get an executable type-checker for free. *)
 
 Section WT_INSTR.
 
 Variable funct: function.
 
-Variable lm: labelmap.
-
-Definition reg_type (fs: Regset.t) (r: mreg) :=
-  let ty := mreg_type r in
-  if typ_eq ty Tfloat && Regset.mem r fs then Tsingle else ty.
-
 Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
   match sl with
   | Local => zle 0 ofs
@@ -176,579 +63,116 @@ Definition loc_valid (l: loc) : bool :=
   | S _ _ _ => false
   end.
 
-Fixpoint wt_code (fs: Regset.t) (c: code) : bool :=
-  match c with
-  | nil => true
-  | Lgetstack sl ofs ty rd :: c =>
-      subtype ty (mreg_type rd) && slot_valid sl ofs ty &&
-      wt_code (setreg fs rd ty) c
-  | Lsetstack rs sl ofs ty :: c =>
-      subtype (reg_type fs rs) ty &&
-      slot_valid sl ofs ty && slot_writable sl &&
-      wt_code fs c
-  | Lop op args dst :: c =>
+Definition wt_instr (i: instruction) : bool :=
+  match i with
+  | Lgetstack sl ofs ty r =>
+      subtype ty (mreg_type r) && slot_valid sl ofs ty
+  | Lsetstack r sl ofs ty =>
+      slot_valid sl ofs ty && slot_writable sl
+  | Lop op args res =>
       match is_move_operation op args with
-      | Some src =>
-          typ_eq (mreg_type src) (mreg_type dst) &&
-          wt_code (copyreg fs dst src) c
-      | None =>
-          let (ty_args, ty_res) := type_of_operation op in
-          subtype ty_res (mreg_type dst) &&
-          wt_code (setreg fs dst ty_res) c
+      | Some arg =>
+          subtype (mreg_type arg) (mreg_type res)
+      | None => 
+          let (targs, tres) := type_of_operation op in
+          subtype tres (mreg_type res)
       end
-  | Lload chunk addr args dst :: c =>
-      subtype (type_of_chunk chunk) (mreg_type dst) &&
-      wt_code (setreg fs dst (type_of_chunk chunk)) c
-  | Lstore chunk addr args src :: c =>
-      wt_code fs c
-  | Lcall sg ros :: c =>
-      wt_code (callregs fs) c
-  | Ltailcall sg ros :: c =>
-      zeq (size_arguments sg) 0 &&
-      wt_code allregs c
-  | Lbuiltin ef args res :: c =>
-      let ty_res := proj_sig_res' (ef_sig ef) in
-      subtype_list ty_res (map mreg_type res) &&
-      wt_code (setregs fs res ty_res) c
-  | Lannot ef args :: c =>
-      forallb loc_valid args &&
-      wt_code fs c
-  | Llabel lbl :: c =>
-      let fs1 := PMap.get lbl lm in
-      Regset.subset fs1 fs && wt_code fs1 c
-  | Lgoto lbl :: c =>
-      let fs1 := PMap.get lbl lm in
-      Regset.subset fs1 fs && wt_code allregs c
-  | Lcond cond args lbl :: c =>
-      let fs1 := PMap.get lbl lm in
-      Regset.subset fs1 fs && wt_code fs c
-  | Ljumptable r lbls :: c =>
-      forallb (fun lbl => Regset.subset (PMap.get lbl lm) fs) lbls &&
-      wt_code allregs c
-  | Lreturn :: c =>
-      wt_code allregs c
+  | Lload chunk addr args dst =>
+      subtype (type_of_chunk chunk) (mreg_type dst)
+  | Ltailcall sg ros =>
+      zeq (size_arguments sg) 0
+  | Lbuiltin ef args res =>
+      subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res) 
+  | Lannot ef args =>
+      forallb loc_valid args
+  | _ =>
+      true
   end.
 
-Remark wt_code_cons:
-  forall fs i c,
-  wt_code fs (i :: c) = true -> exists fs', wt_code fs' c = true.
-Proof.
-  simpl; intros. destruct i; InvBooleans; try (econstructor; eassumption).
-  destruct (is_move_operation o l).
-  InvBooleans; econstructor; eassumption.
-  destruct (type_of_operation o). InvBooleans; econstructor; eassumption.
-Qed.
-
-Lemma wt_find_label:
-  forall lbl c' c fs,
-  find_label lbl c = Some c' ->
-  wt_code fs c = true ->
-  wt_code (PMap.get lbl lm) c' = true.
-Proof.
-  induction c; intros.
-- discriminate.
-- simpl in H. specialize (is_label_correct lbl a). destruct (is_label lbl a); intros IL.
-  + subst a. simpl in H0. inv H. InvBooleans. auto. 
-  + destruct (wt_code_cons _ _ _ H0) as [fs' WT]. eauto. 
-Qed.
-
 End WT_INSTR.
 
-Definition wt_funcode (f: function) (lm: labelmap) : bool :=
-  wt_code f lm Regset.empty f.(fn_code).
+Definition wt_code (f: function) (c: code) : bool :=
+  forallb (wt_instr f) c.
 
 Definition wt_function (f: function) : bool :=
-  match ana_function f with
-  | None => false
-  | Some lm => wt_funcode f lm
-  end.
+  wt_code f f.(fn_code).
 
-(** * Soundness of the type system *)
+(** Typing the run-time state.  These definitions are used in [Stackingproof]. *)
 
 Require Import Values.
-Require Import Globalenvs.
-Require Import Memory.
 
-Module RSF := FSetFacts.Facts(Regset).
-
-(** ** Typing the run-time state *)
-
-Definition loc_type (fs: Regset.t) (l: loc): typ :=
-  match l with
-  | R r => reg_type fs r
-  | S sl ofs ty => ty
-  end.
-
-Definition wt_locset (fs: Regset.t) (ls: locset) : Prop :=
-  forall l, Val.has_type (ls l) (loc_type fs l).
-
-Remark subtype_refl:
-  forall ty, subtype ty ty = true.
-Proof.
-  destruct ty; reflexivity.
-Qed.
-
-Remark reg_type_sub:
-  forall fs r, subtype (reg_type fs r) (mreg_type r) = true.
-Proof.
-  intros. unfold reg_type. destruct (typ_eq (mreg_type r) Tfloat); simpl.
-  rewrite e. destruct (Regset.mem r fs); auto. 
-  apply subtype_refl.
-Qed.
-
-Lemma wt_mreg:
-  forall fs ls r, wt_locset fs ls -> Val.has_type (ls (R r)) (mreg_type r).
-Proof.
-  intros. eapply Val.has_subtype. apply reg_type_sub with (fs := fs). apply H.
-Qed.
-
-Lemma wt_locset_empty:
-  forall ls,
-  (forall l, Val.has_type (ls l) (Loc.type l)) -> 
-  wt_locset Regset.empty ls.
-Proof.
-  intros; red; intros. destruct l; simpl.
-- unfold reg_type. change (Regset.mem r Regset.empty) with false. 
-  rewrite andb_false_r. apply H. 
-- apply H.
-Qed.
-
-Remark reg_type_mon:
-  forall fs1 fs2 r, Regset.Subset fs2 fs1 -> subtype (reg_type fs1 r) (reg_type fs2 r) = true.
-Proof.
-  intros. unfold reg_type. destruct (typ_eq (mreg_type r) Tfloat); simpl.
-  rewrite e. destruct (Regset.mem r fs2) eqn:E. 
-  rewrite Regset.mem_1. auto. apply H. apply Regset.mem_2; auto. 
-  destruct (Regset.mem r fs1); auto. 
-  apply subtype_refl.
-Qed.
-
-Lemma wt_locset_mon:
-  forall fs1 fs2 ls,
-  Regset.Subset fs2 fs1 -> wt_locset fs1 ls -> wt_locset fs2 ls.
-Proof.
-  intros; red; intros. apply Val.has_subtype with (loc_type fs1 l); auto. 
-  unfold loc_type. destruct l. apply reg_type_mon; auto. apply subtype_refl.
-Qed.
+Definition wt_locset (ls: locset) : Prop :=
+  forall l, Val.has_type (ls l) (Loc.type l).
 
 Lemma wt_setreg:
-  forall fs ls r v ty,
-  Val.has_type v ty -> subtype ty (mreg_type r) = true -> wt_locset fs ls ->
-  wt_locset (setreg fs r ty) (Locmap.set (R r) v ls).
+  forall ls r v,
+  Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls).
 Proof.
   intros; red; intros.
-  unfold Locmap.set. destruct (Loc.eq (R r) l).
-- subst l. simpl. unfold reg_type, setreg.
-  destruct (typ_eq (mreg_type r) Tfloat &&
-      Regset.mem r
-        (if typ_eq ty Tsingle then Regset.add r fs else Regset.remove r fs)) eqn:E.
-+ InvBooleans. destruct (typ_eq ty Tsingle).
-  congruence.
-  rewrite RSF.remove_b in H3. unfold RSF.eqb in H3. rewrite dec_eq_true in H3. 
-  simpl in H3. rewrite andb_false_r in H3. discriminate.
-+ eapply Val.has_subtype; eauto.
-- destruct (Loc.diff_dec (R r) l).
-+ replace (loc_type (setreg fs r ty) l) with (loc_type fs l).
-  apply H1. 
-  unfold loc_type, setreg. destruct l; auto. destruct (typ_eq ty Tsingle).
-  unfold reg_type. rewrite RSF.add_neq_b. auto. congruence. 
-  unfold reg_type. rewrite RSF.remove_neq_b. auto. congruence.
-+ red; auto. 
-Qed.
-
-Lemma wt_copyreg:
-  forall fs ls src dst v,
-  mreg_type src = mreg_type dst ->
-  wt_locset fs ls ->
-  Val.has_type v (reg_type fs src) ->
-  wt_locset (copyreg fs dst src) (Locmap.set (R dst) v ls).
-Proof.
-  intros; red; intros.
-  unfold Locmap.set. destruct (Loc.eq (R dst) l). 
-- subst l. simpl. unfold reg_type, copyreg.
-  unfold reg_type in H1. rewrite H in H1. 
-  destruct (Regset.mem src fs) eqn:SRC. 
-  rewrite RSF.add_b. unfold RSF.eqb. rewrite dec_eq_true. simpl. auto.
-  rewrite RSF.remove_b. unfold RSF.eqb. rewrite dec_eq_true. simpl. rewrite ! andb_false_r. 
-  rewrite andb_false_r in H1. auto.
-- destruct (Loc.diff_dec (R dst) l). 
-+ replace (loc_type (copyreg fs dst src) l) with (loc_type fs l).
-  apply H0.
-  unfold loc_type, copyreg. destruct l; auto. destruct (Regset.mem src fs). 
-  unfold reg_type. rewrite RSF.add_neq_b. auto. congruence. 
-  unfold reg_type. rewrite RSF.remove_neq_b. auto. congruence.
-+ red; auto.
+  unfold Locmap.set. 
+  destruct (Loc.eq (R r) l).
+  subst l; auto.
+  destruct (Loc.diff_dec (R r) l). auto. red. auto.
 Qed.
 
 Lemma wt_setstack:
-  forall fs ls sl ofs ty v,
-  Val.has_type v ty -> wt_locset fs ls ->
-  wt_locset fs (Locmap.set (S sl ofs ty) v ls).
+  forall ls sl ofs ty v,
+  wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls).
 Proof.
   intros; red; intros.
   unfold Locmap.set. 
   destruct (Loc.eq (S sl ofs ty) l).
-  subst l. simpl. auto. 
+  subst l. simpl. 
+  generalize (Val.load_result_type (chunk_of_type ty) v). 
+  replace (type_of_chunk (chunk_of_type ty)) with ty. auto.
+  destruct ty; reflexivity.
   destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto.
 Qed.
 
-Lemma wt_undef:
-  forall fs ls l, wt_locset fs ls -> wt_locset fs (Locmap.set l Vundef ls).
-Proof.
-  intros; red; intros. unfold Locmap.set. 
-  destruct (Loc.eq l l0). red; auto. 
-  destruct (Loc.diff_dec l l0); auto. red; auto.
-Qed.
-
 Lemma wt_undef_regs:
-  forall fs rs ls, wt_locset fs ls -> wt_locset fs (undef_regs rs ls).
+  forall rs ls, wt_locset ls -> wt_locset (undef_regs rs ls).
 Proof.
-  induction rs; simpl; intros. auto. apply wt_undef; auto. 
+  induction rs; simpl; intros. auto. apply wt_setreg; auto. red; auto.
 Qed.
 
 Lemma wt_call_regs:
-  forall fs ls, wt_locset fs ls -> wt_locset Regset.empty (call_regs ls).
+  forall ls, wt_locset ls -> wt_locset (call_regs ls).
 Proof.
-  intros; red; intros. unfold call_regs. destruct l.
-  eapply Val.has_subtype; eauto. unfold loc_type. apply reg_type_mon. 
-  red; intros. eelim Regset.empty_1; eauto. 
+  intros; red; intros. unfold call_regs. destruct l. auto.
   destruct sl.
   red; auto.
-  change (loc_type Regset.empty (S Incoming pos ty))
-    with (loc_type fs (S Outgoing pos ty)). auto.
+  change (Loc.type (S Incoming pos ty)) with (Loc.type (S Outgoing pos ty)). auto.
   red; auto.
 Qed.
 
-Remark set_from_list:
-  forall r l, Regset.In r (List.fold_right Regset.add Regset.empty l) <-> In r l.
-Proof.
-  induction l; simpl. 
-- rewrite RSF.empty_iff. tauto.
-- rewrite RSF.add_iff. rewrite IHl. tauto.
-Qed.
-
 Lemma wt_return_regs:
-  forall fs caller callee,
-  wt_locset fs caller -> wt_locset Regset.empty callee ->
-  wt_locset (callregs fs) (return_regs caller callee).
+  forall caller callee,
+  wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee).
 Proof.
   intros; red; intros.
-  unfold return_regs. destruct l.
-- destruct (in_dec mreg_eq r destroyed_at_call). 
-+ unfold loc_type. replace (reg_type (callregs fs) r) with (mreg_type r).
-  eapply Val.has_subtype. eapply reg_type_sub. apply (H0 (R r)).
-  unfold reg_type, callregs. rewrite RSF.diff_b. 
-  rewrite (@Regset.mem_1 destroyed_at_call_regs).
-  rewrite ! andb_false_r. auto.
-  unfold destroyed_at_call_regs; apply set_from_list; auto.
-+ unfold loc_type, reg_type, callregs. rewrite RSF.diff_b. 
-  destruct (Regset.mem r destroyed_at_call_regs) eqn:E. 
-  elim n. apply set_from_list. apply Regset.mem_2; auto. 
-  rewrite andb_true_r. apply H. 
-- unfold loc_type. apply H. 
+  unfold return_regs. destruct l; auto.
+  destruct (in_dec mreg_eq r destroyed_at_call); auto.
 Qed.
 
 Lemma wt_init:
-  forall fs, wt_locset fs (Locmap.init Vundef).
+  wt_locset (Locmap.init Vundef).
 Proof.
   red; intros. unfold Locmap.init. red; auto.
 Qed.
 
-Lemma wt_setregs:
-  forall vl tyl rl fs rs,
-  Val.has_type_list vl tyl ->
-  subtype_list tyl (map mreg_type rl) = true ->
-  wt_locset fs rs ->
-  wt_locset (setregs fs rl tyl) (Locmap.setlist (map R rl) vl rs).
-Proof.
-  induction vl; simpl; intros.
-- destruct tyl; try contradiction. destruct rl; try discriminate. 
-  simpl. auto.
-- destruct tyl as [ | ty tyl]; try contradiction. destruct H.
-  destruct rl as [ | r rl]; simpl in H0; try discriminate. InvBooleans.
-  simpl. eapply IHvl; eauto. eapply wt_setreg; eauto. 
-Qed.
-
-Lemma wt_setregs_result:
-  forall sg fs v rl rs,
+Lemma wt_setlist_result:
+  forall sg v rs,
   Val.has_type v (proj_sig_res sg) ->
-  subtype_list (proj_sig_res' sg) (map mreg_type rl) = true ->
-  wt_locset fs rs ->
-  wt_locset (setregs fs rl (proj_sig_res' sg)) 
-            (Locmap.setlist (map R rl) (encode_long (sig_res sg) v) rs).
-Proof.
-  intros. eapply wt_setregs; eauto. 
-  unfold proj_sig_res in H. unfold encode_long, proj_sig_res'. 
-  destruct (sig_res sg) as [[] | ]; simpl; intuition. 
-  destruct v; simpl; auto.
-  destruct v; simpl; auto.
-Qed.
-
-Remark in_setreg_other:
-  forall fs r ty r',
-  r' <> r -> (Regset.In r' (setreg fs r ty) <-> Regset.In r' fs).
-Proof.
-  intros. unfold setreg. destruct (typ_eq ty Tsingle). 
-  rewrite RSF.add_iff. intuition. 
-  rewrite RSF.remove_iff. intuition.
-Qed.
-
-Remark in_setregs_other:
-  forall r rl fs tyl,
-  ~In r rl -> (Regset.In r (setregs fs rl tyl) <-> Regset.In r fs).
-Proof.
-  induction rl; simpl; intros. 
-- destruct tyl; tauto.
-- destruct tyl. tauto. rewrite IHrl by tauto. apply in_setreg_other. intuition.
-Qed. 
-
-Remark callregs_setregs_result:
-  forall sg fs,
-  Regset.Subset (callregs fs) (setregs fs (loc_result sg) (proj_sig_res' sg)).
-Proof.
-  red; unfold callregs; intros. rewrite RSF.diff_iff in H. destruct H. 
-  apply in_setregs_other; auto. 
-  red; intros; elim H0. apply set_from_list. eapply loc_result_caller_save; eauto.
-Qed.
-
-Definition wt_fundef (fd: fundef) :=
-  match fd with
-  | Internal f => wt_function f = true
-  | External ef => True
-  end.
-
-Inductive wt_callstack: list stackframe -> Regset.t -> Prop :=
-  | wt_callstack_nil: forall fs, 
-      wt_callstack nil fs
-  | wt_callstack_cons: forall f sp rs c s fs lm fs0 fs1
-        (WTSTK: wt_callstack s fs0)
-        (WTF: wt_funcode f lm = true)
-        (WTC: wt_code f lm (callregs fs1) c = true)
-        (WTRS: wt_locset fs rs)
-        (INCL: Regset.Subset (callregs fs1) (callregs fs)),
-      wt_callstack (Stackframe f sp rs c :: s) fs.
-
-Lemma wt_parent_locset:
-  forall s fs, wt_callstack s fs -> wt_locset fs (parent_locset s).
-Proof.
-  induction 1; simpl.
-- apply wt_init.
-- auto.
-Qed.
-
-Lemma wt_callstack_change_fs:
-  forall s fs, wt_callstack s fs -> wt_callstack s (callregs fs).
-Proof.
-  induction 1.
-- constructor.
-- econstructor; eauto. 
-  apply wt_locset_mon with fs; auto. 
-  unfold callregs; red; intros. eapply Regset.diff_1; eauto.
-  red; intros. exploit INCL; eauto. unfold callregs. rewrite ! RSF.diff_iff. 
-  tauto.
-Qed.
-
-Inductive wt_state: state -> Prop :=
-  | wt_regular_state: forall s f sp c rs m lm fs fs0
-        (WTSTK: wt_callstack s fs0)
-        (WTF: wt_funcode f lm = true)
-        (WTC: wt_code f lm fs c = true)
-        (WTRS: wt_locset fs rs),
-      wt_state (State s f sp c rs m)
-  | wt_call_state: forall s fd rs m fs
-        (WTSTK: wt_callstack s fs)
-        (WTFD: wt_fundef fd)
-        (WTRS: wt_locset fs rs),
-      wt_state (Callstate s fd rs m)
-  | wt_return_state: forall s rs m fs
-        (WTSTK: wt_callstack s fs)
-        (WTRS: wt_locset (callregs fs) rs),
-      wt_state (Returnstate s rs m).
-
-(** ** Preservation of state typing by transitions *)
-
-Section SOUNDNESS.
-
-Variable prog: program.
-Let ge := Genv.globalenv prog.
-
-Hypothesis wt_prog:
-  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.
-
-Lemma wt_find_function:
-  forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f.
-Proof.
-  intros. 
-  assert (X: exists i, In (i, Gfun f) prog.(prog_defs)).
-  {
-    destruct ros as [r | s]; simpl in H.
-    eapply Genv.find_funct_inversion; eauto. 
-    destruct (Genv.find_symbol ge s) as [b|]; try discriminate.
-    eapply Genv.find_funct_ptr_inversion; eauto.
-  }
-  destruct X as [i IN]. eapply wt_prog; eauto. 
-Qed.
-
-Theorem step_type_preservation:
-  forall S1 t S2, step ge S1 t S2 -> wt_state S1 -> wt_state S2.
-Proof.
-  induction 1; intros WTS; inv WTS.
-- (* getstack *)
-  simpl in WTC; InvBooleans. 
-  econstructor; eauto.
-  apply wt_setreg; auto. apply (WTRS (S sl ofs ty)). apply wt_undef_regs; auto.
-- (* setstack *)
-  simpl in WTC; InvBooleans. 
-  econstructor; eauto. 
-  apply wt_setstack; auto. eapply Val.has_subtype; eauto. apply WTRS. 
-  apply wt_undef_regs; auto.
-- (* op *)
-  simpl in WTC. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE.
-  + (* move *)
-    InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst. 
-    simpl in H. inv H.
-    econstructor; eauto. 
-    apply wt_copyreg. auto. apply wt_undef_regs; auto. apply WTRS. 
-  + (* other ops *) 
-    destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
-    econstructor; eauto.
-    apply wt_setreg; auto. 
-    change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. 
-    eapply type_of_operation_sound; eauto. 
-    red; intros; subst op. simpl in ISMOVE. 
-    destruct args; try discriminate. destruct args; discriminate. 
-    apply wt_undef_regs; auto.
-- (* load *)
-  simpl in WTC; InvBooleans. 
-  econstructor; eauto.
-  apply wt_setreg. 
-  destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
-  auto. 
-  apply wt_undef_regs; auto.
-- (* store *)
-  simpl in WTC; InvBooleans. 
-  econstructor; eauto.
-  apply wt_undef_regs; auto.
-- (* call *)
-  simpl in WTC; InvBooleans.
-  econstructor; eauto. econstructor; eauto.
-  red; auto.
-  eapply wt_find_function; eauto.
-- (* tailcall *)
-  simpl in WTC; InvBooleans.
-  econstructor. apply wt_callstack_change_fs; eauto. 
-  eapply wt_find_function; eauto.
-  apply wt_return_regs. apply wt_parent_locset; auto. 
-  eapply wt_locset_mon; eauto. red; intros. eelim Regset.empty_1; eauto.
-- (* builtin *)
-  simpl in WTC; InvBooleans. inv H. 
-  econstructor; eauto.
-  apply wt_setregs_result; auto.
-  eapply external_call_well_typed; eauto.
-  apply wt_undef_regs; auto.
-- (* annot *)
-  simpl in WTC; InvBooleans.
-  econstructor; eauto. 
-- (* label *)
-  simpl in WTC; InvBooleans. 
-  econstructor; eauto.
-  eapply wt_locset_mon; eauto. apply Regset.subset_2; auto.
-- (* goto *)
-  simpl in WTC; InvBooleans. 
-  econstructor. eauto. eauto. 
-  eapply wt_find_label; eauto. 
-  eapply wt_locset_mon; eauto. apply Regset.subset_2; auto.
-- (* cond branch, taken *)
-  simpl in WTC; InvBooleans. 
-  econstructor. eauto. eauto. 
-  eapply wt_find_label; eauto. 
-  eapply wt_locset_mon. apply Regset.subset_2; eauto.
-  apply wt_undef_regs; auto.
-- (* cond branch, not taken *)
-  simpl in WTC; InvBooleans. 
-  econstructor. eauto. eauto. eauto. 
-  apply wt_undef_regs; auto.
-- (* jumptable *)
-  simpl in WTC; InvBooleans. 
-  econstructor. eauto. eauto.
-  eapply wt_find_label; eauto. 
-  apply wt_locset_mon with fs.
-  apply Regset.subset_2. rewrite List.forallb_forall in H2. apply H2. 
-  eapply list_nth_z_in; eauto.
-  apply wt_undef_regs; auto.
-- (* return *)
-  econstructor. eauto. 
-  apply wt_return_regs. 
-  apply wt_parent_locset; auto. 
-  apply wt_locset_mon with fs; auto. red; intros. eelim Regset.empty_1; eauto.
-- (* internal function *)
-  simpl in WTFD. unfold wt_function in WTFD. destruct (ana_function f) as [lm|]; try discriminate.
-  econstructor. eauto. eauto. eexact WTFD. 
-  apply wt_undef_regs. eapply wt_call_regs; eauto. 
-- (* external function *)
-  inv H0. 
-  econstructor. eauto. 
-  eapply wt_locset_mon. 2: eapply wt_setregs_result; eauto. 
-  apply callregs_setregs_result. 
-  eapply external_call_well_typed; eauto. 
-  unfold proj_sig_res', loc_result. destruct (sig_res (ef_sig ef) )as [[] | ]; auto.
-- (* return *)
-  inv WTSTK. econstructor; eauto. 
-  apply wt_locset_mon with (callregs fs); auto. 
-Qed.
-
-Theorem wt_initial_state:
-  forall S, initial_state prog S -> wt_state S.
-Proof.
-  induction 1. econstructor. 
-  apply wt_callstack_nil with (fs := Regset.empty).
-  unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto.
-  intros [id IN]. eapply wt_prog; eauto. 
-  apply wt_init.
-Qed.
-
-End SOUNDNESS.
-
-(** Properties of well-typed states that are used in [Stackingproof]. *)
-
-Lemma wt_state_getstack:
-  forall s f sp sl ofs ty rd c rs m,
-  wt_state (State s f sp (Lgetstack sl ofs ty rd :: c) rs m) ->
-  slot_valid f sl ofs ty = true.
-Proof.
-  intros. inv H. simpl in WTC; InvBooleans. auto.
-Qed.
-
-Lemma wt_state_setstack:
-  forall s f sp sl ofs ty r c rs m,
-  wt_state (State s f sp (Lsetstack r sl ofs ty :: c) rs m) ->
-  Val.has_type (rs (R r)) ty /\ slot_valid f sl ofs ty = true /\ slot_writable sl = true.
-Proof.
-  intros. inv H. simpl in WTC; InvBooleans. intuition. 
-  eapply Val.has_subtype; eauto. apply WTRS. 
-Qed.
-
-Lemma wt_state_tailcall:
-  forall s f sp sg ros c rs m,
-  wt_state (State s f sp (Ltailcall sg ros :: c) rs m) ->
-  size_arguments sg = 0.
-Proof.
-  intros. inv H. simpl in WTC; InvBooleans. auto.
-Qed.
-
-Lemma wt_state_annot:
-  forall s f sp ef args c rs m,
-  wt_state (State s f sp (Lannot ef args :: c) rs m) ->
-  forallb (loc_valid f) args = true.
-Proof.
-  intros. inv H. simpl in WTC; InvBooleans. auto. 
-Qed.
-
-Lemma wt_callstate_wt_locset:
-  forall s f rs m,
-  wt_state (Callstate s f rs m) -> wt_locset Regset.empty rs.
-Proof.
-  intros. inv H. apply wt_locset_mon with fs; auto. 
-  red; intros; eelim Regset.empty_1; eauto.
+  wt_locset rs ->
+  wt_locset (Locmap.setlist (map R (loc_result sg)) (encode_long (sig_res sg) v) rs).
+Proof.
+  unfold loc_result, encode_long, proj_sig_res; intros.
+  destruct (sig_res sg) as [[] | ]; simpl.
+- apply wt_setreg; auto.
+- apply wt_setreg; auto.
+- destruct v; simpl in H; try contradiction;
+  simpl; apply wt_setreg; auto; apply wt_setreg; auto.
+- apply wt_setreg; auto. apply Val.has_subtype with Tsingle; auto. 
+- apply wt_setreg; auto.
 Qed.
 
diff --git a/backend/Locations.v b/backend/Locations.v
index 96f1eba..43ce210 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -301,16 +301,29 @@ Module Locmap.
 
   Definition set (l: loc) (v: val) (m: t) : t :=
     fun (p: loc) =>
-      if Loc.eq l p then v
-      else if Loc.diff_dec l p then m p
+      if Loc.eq l p then
+        match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end
+      else if Loc.diff_dec l p then
+        m p
       else Vundef.
 
   Lemma gss: forall l v m,
-    (set l v m) l = v.
+    (set l v m) l = 
+    match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end.
   Proof.
     intros. unfold set. apply dec_eq_true.
   Qed.
 
+  Lemma gss_reg: forall r v m, (set (R r) v m) (R r) = v.
+  Proof.
+    intros. unfold set. rewrite dec_eq_true. auto.
+  Qed.
+
+  Lemma gss_typed: forall l v m, Val.has_type v (Loc.type l) -> (set l v m) l = v.
+  Proof.
+    intros. rewrite gss. destruct l. auto. apply Val.load_result_same; auto. 
+  Qed.
+
   Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p.
   Proof.
     intros. unfold set. destruct (Loc.eq l p).
@@ -336,10 +349,11 @@ Module Locmap.
   Proof.
     assert (P: forall ll l m, m l = Vundef -> (undef ll m) l = Vundef).
       induction ll; simpl; intros. auto. apply IHll. 
-      unfold set. destruct (Loc.eq a l). auto.
+      unfold set. destruct (Loc.eq a l).
+      destruct a. auto. destruct ty; reflexivity. 
       destruct (Loc.diff_dec a l); auto.
     induction ll; simpl; intros. contradiction. 
-    destruct H. apply P. subst a. apply gss.  
+    destruct H. apply P. subst a. apply gss_typed. exact I. 
     auto.
   Qed.
 
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index e8ae7ae..24f8d7b 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -14,7 +14,7 @@
 
 Require Import Coqlib.
 Require Import Errors.
-Require Import Unityping.
+Require Import Subtyping.
 Require Import Maps.
 Require Import AST.
 Require Import Op.
@@ -36,8 +36,7 @@ Require Import Conventions.
   is very simple, consisting of the four types [Tint] (for integers
   and pointers), [Tfloat] (for double-precision floats), [Tlong]
   (for 64-bit integers) and [Tsingle] (for single-precision floats).
-  At the RTL level, we simplify things further by equating [Tsingle]
-  with [Tfloat].
+  The only subtlety is that [Tsingle] is a subtype of [Tfloat].
 
   Additionally, we impose that each pseudo-register has the same type
   throughout the function.  This requirement helps with register allocation,
@@ -57,11 +56,6 @@ Require Import Conventions.
   which can work over both integers and floats.
 *)
 
-Definition normalize (ty: typ) : typ :=
-  match ty with Tsingle => Tfloat | _ => ty end.
-
-Definition normalize_list (tyl: list typ) : list typ := map normalize tyl.
-
 Definition regenv := reg -> typ.
 
 Section WT_INSTR.
@@ -79,57 +73,57 @@ Inductive wt_instr : instruction -> Prop :=
       wt_instr (Inop s)
   | wt_Iopmove:
       forall r1 r s,
-      env r = env r1 ->
+      subtype (env r1) (env r) = true ->
       valid_successor s ->
       wt_instr (Iop Omove (r1 :: nil) r s)
   | wt_Iop:
       forall op args res s,
       op <> Omove ->
-      map env args = fst (type_of_operation op) ->
-      env res = normalize (snd (type_of_operation op)) ->
+      subtype_list (map env args) (fst (type_of_operation op)) = true ->
+      subtype (snd (type_of_operation op)) (env res) = true ->
       valid_successor s ->
       wt_instr (Iop op args res s)
   | wt_Iload:
       forall chunk addr args dst s,
-      map env args = type_of_addressing addr ->
-      env dst = normalize (type_of_chunk chunk) ->
+      subtype_list (map env args) (type_of_addressing addr) = true ->
+      subtype (type_of_chunk chunk) (env dst) = true ->
       valid_successor s ->
       wt_instr (Iload chunk addr args dst s)
   | wt_Istore:
       forall chunk addr args src s,
-      map env args = type_of_addressing addr ->
-      env src = type_of_chunk_use chunk ->
+      subtype_list (map env args) (type_of_addressing addr) = true ->
+      subtype (env src) (type_of_chunk_use chunk) = true ->
       valid_successor s ->
       wt_instr (Istore chunk addr args src s)
   | wt_Icall:
       forall sig ros args res s,
-      match ros with inl r => env r = Tint | inr s => True end ->
-      map env args = normalize_list sig.(sig_args) ->
-      env res = normalize (proj_sig_res sig) ->
+      match ros with inl r => subtype (env r) Tint = true | inr s => True end ->
+      subtype_list (map env args) sig.(sig_args) = true ->
+      subtype (proj_sig_res sig) (env res) = true ->
       valid_successor s ->
       wt_instr (Icall sig ros args res s)
   | wt_Itailcall:
       forall sig ros args,
-      match ros with inl r => env r = Tint | inr s => True end ->
-      map env args = normalize_list sig.(sig_args) ->
+      match ros with inl r => subtype (env r) Tint = true | inr s => True end ->
       sig.(sig_res) = funct.(fn_sig).(sig_res) ->
+      subtype_list (map env args) sig.(sig_args) = true ->
       tailcall_possible sig ->
       wt_instr (Itailcall sig ros args)
   | wt_Ibuiltin:
       forall ef args res s,
-      map env args = normalize_list (ef_sig ef).(sig_args) ->
-      env res = normalize (proj_sig_res (ef_sig ef)) ->
+      subtype_list (map env args) (ef_sig ef).(sig_args) = true ->
+      subtype (proj_sig_res (ef_sig ef)) (env res) = true ->
       valid_successor s ->
       wt_instr (Ibuiltin ef args res s)
   | wt_Icond:
       forall cond args s1 s2,
-      map env args = type_of_condition cond ->
+      subtype_list (map env args) (type_of_condition cond) = true ->
       valid_successor s1 ->
       valid_successor s2 ->
       wt_instr (Icond cond args s1 s2)
   | wt_Ijumptable:
       forall arg tbl,
-      env arg = Tint ->
+      subtype (env arg) Tint = true ->
       (forall s, In s tbl -> valid_successor s) ->
       list_length_z tbl * 4 <= Int.max_unsigned ->
       wt_instr (Ijumptable arg tbl)
@@ -139,7 +133,7 @@ Inductive wt_instr : instruction -> Prop :=
   | wt_Ireturn_some:
       forall arg ty,
       funct.(fn_sig).(sig_res) = Some ty ->
-      env arg = normalize ty ->
+      subtype (env arg) ty = true ->
       wt_instr (Ireturn (Some arg)).
 
 End WT_INSTR.
@@ -152,7 +146,7 @@ End WT_INSTR.
 Record wt_function (f: function) (env: regenv): Prop :=
   mk_wt_function {
     wt_params:
-      map env f.(fn_params) = normalize_list f.(fn_sig).(sig_args);
+      subtype_list f.(fn_sig).(sig_args) (map env f.(fn_params)) = true;
     wt_norepet:
       list_norepet f.(fn_params);
     wt_instrs:
@@ -174,8 +168,8 @@ Definition wt_program (p: program): Prop :=
 
 (** * Type inference *)
 
-(** Type inference reuses the generic solver for unification constraints
-  defined in module [Unityping]. *)
+(** Type inference reuses the generic solver for subtyping constraints
+  defined in module [Subtyping]. *)
 
 Module RTLtypes <: TYPE_ALGEBRA.
 
@@ -183,9 +177,122 @@ Definition t := typ.
 Definition eq := typ_eq.
 Definition default := Tint.
 
+Definition sub (t1 t2: typ): Prop := subtype t1 t2 = true.
+
+Lemma sub_refl: forall ty, sub ty ty.
+Proof. unfold sub; destruct ty; auto. Qed.
+
+Lemma sub_trans: forall ty1 ty2 ty3, sub ty1 ty2 -> sub ty2 ty3 -> sub ty1 ty3.
+Proof.
+  unfold sub; intros. destruct ty1; destruct ty2; try discriminate; destruct ty3; auto; discriminate.
+Qed.
+
+Definition sub_dec: forall ty1 ty2, {sub ty1 ty2} + {~sub ty1 ty2}.
+Proof.
+  unfold sub; intros. destruct (subtype ty1 ty2). left; auto. right; congruence.
+Defined.
+
+Definition lub (ty1 ty2: typ) :=
+  match ty1, ty2 with
+  | Tint, Tint => Tint
+  | Tlong, Tlong => Tlong
+  | Tfloat, Tfloat => Tfloat
+  | Tsingle, Tsingle => Tsingle
+  | Tfloat, Tsingle => Tfloat
+  | Tsingle, Tfloat => Tfloat
+  | _, _ => default
+  end.
+
+Lemma lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y).
+Proof.
+  unfold sub, lub; intros. destruct x; destruct y; auto; destruct z; discriminate.
+Qed.
+
+Lemma lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y).
+Proof.
+  unfold sub, lub; intros. destruct x; destruct y; auto; destruct z; discriminate.
+Qed.
+
+Lemma lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z.
+Proof.
+  unfold sub, lub; intros. destruct x; destruct z; try discriminate; destruct y; auto; discriminate.
+Qed.
+
+Definition glb (ty1 ty2: typ) :=
+  match ty1, ty2 with
+  | Tint, Tint => Tint
+  | Tlong, Tlong => Tlong
+  | Tfloat, Tfloat => Tfloat
+  | Tsingle, Tsingle => Tsingle
+  | Tfloat, Tsingle => Tsingle
+  | Tsingle, Tfloat => Tsingle
+  | _, _ => default
+  end.
+
+Lemma glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x.
+Proof.
+  unfold sub, glb; intros. destruct x; destruct y; auto; destruct z; discriminate.
+Qed.
+
+Lemma glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y.
+Proof.
+  unfold sub, glb; intros. destruct x; destruct y; auto; destruct z; discriminate.
+Qed.
+
+Lemma glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y).
+Proof.
+  unfold sub, glb; intros. destruct x; destruct z; try discriminate; destruct y; auto; discriminate.
+Qed.
+
+Definition low_bound (ty: typ) :=
+  match ty with Tfloat => Tsingle | _ => ty end.
+
+Definition high_bound (ty: typ) :=
+  match ty with Tsingle => Tfloat | _ => ty end.
+
+Lemma low_bound_sub: forall t, sub (low_bound t) t.
+Proof.
+  unfold sub; destruct t0; auto.
+Qed.
+
+Lemma low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x.
+Proof.
+  unfold sub; intros. destruct x; destruct y; auto; discriminate.
+Qed.
+
+Lemma high_bound_sub: forall t, sub t (high_bound t).
+Proof.
+  unfold sub; destruct t0; auto.
+Qed.
+
+Lemma high_bound_majorant: forall x y, sub x y -> sub y (high_bound x).
+Proof.
+  unfold sub; intros. destruct x; destruct y; auto; discriminate.
+Qed.
+
+Definition weight (t: typ) :=
+  match t with Tfloat => 1%nat | _ => 0%nat end.
+
+Definition max_weight := 1%nat.
+
+Lemma weight_range: forall t, (weight t <= max_weight)%nat.
+Proof.
+  unfold max_weight; destruct t0; simpl; omega.
+Qed.
+
+Lemma weight_sub: forall x y, sub x y -> (weight x <= weight y)%nat.
+Proof.
+  unfold sub; intros. destruct x; destruct y; simpl; discriminate || omega.
+Qed.
+
+Lemma weight_sub_strict: forall x y, sub x y -> x <> y -> (weight x < weight y)%nat.
+Proof.
+  unfold sub, subtype; intros. destruct x; destruct y; simpl; congruence || omega.
+Qed.
+
 End RTLtypes.
 
-Module S := UniSolver(RTLtypes).
+Module S := SubSolver(RTLtypes).
 
 Section INFERENCE.
 
@@ -211,7 +318,7 @@ Fixpoint check_successors (sl: list node): res unit :=
 
 Definition type_ros (e: S.typenv) (ros: reg + ident) : res S.typenv :=
   match ros with
-  | inl r => S.set e r Tint
+  | inl r => S.type_use e r Tint
   | inr s => OK e
   end.
 
@@ -226,28 +333,28 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
       do x <- check_successor s;
       if is_move op then
         match args with
-        | arg :: nil => do (changed, e') <- S.move e res arg; OK e'
+        | arg :: nil => do (changed, e') <- S.type_move e arg res; OK e'
         | _ => Error (msg "ill-formed move")
         end
       else
        (let (targs, tres) := type_of_operation op in
-        do e1 <- S.set_list e args targs; S.set e1 res (normalize tres))
+        do e1 <- S.type_uses e args targs; S.type_def e1 res tres)
   | Iload chunk addr args dst s =>
       do x <- check_successor s;
-      do e1 <- S.set_list e args (type_of_addressing addr);
-      S.set e1 dst (normalize (type_of_chunk chunk))
+      do e1 <- S.type_uses e args (type_of_addressing addr);
+      S.type_def e1 dst (type_of_chunk chunk)
   | Istore chunk addr args src s =>
       do x <- check_successor s;
-      do e1 <- S.set_list e args (type_of_addressing addr);
-      S.set e1 src (type_of_chunk_use chunk)
+      do e1 <- S.type_uses e args (type_of_addressing addr);
+      S.type_use e1 src (type_of_chunk_use chunk)
   | Icall sig ros args res s =>
       do x <- check_successor s;
       do e1 <- type_ros e ros;
-      do e2 <- S.set_list e1 args (normalize_list sig.(sig_args));
-      S.set e2 res (normalize (proj_sig_res sig))
+      do e2 <- S.type_uses e1 args sig.(sig_args);
+      S.type_def e2 res (proj_sig_res sig)
   | Itailcall sig ros args =>
       do e1 <- type_ros e ros;
-      do e2 <- S.set_list e1 args (normalize_list sig.(sig_args));
+      do e2 <- S.type_uses e1 args sig.(sig_args);
       if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then
         if tailcall_is_possible sig
         then OK e2
@@ -256,48 +363,45 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
   | Ibuiltin ef args res s =>
       let sig := ef_sig ef in
       do x <- check_successor s;
-      do e1 <- S.set_list e args (normalize_list sig.(sig_args));
-      S.set e1 res (normalize (proj_sig_res sig))
- | Icond cond args s1 s2 =>
+      do e1 <- S.type_uses e args sig.(sig_args);
+      S.type_def e1 res (proj_sig_res sig)
+  | Icond cond args s1 s2 =>
       do x1 <- check_successor s1;
       do x2 <- check_successor s2;
-      S.set_list e args (type_of_condition cond)
- | Ijumptable arg tbl =>
+      S.type_uses e args (type_of_condition cond)
+  | Ijumptable arg tbl =>
       do x <- check_successors tbl;
-      do e1 <- S.set e arg Tint;
-      if zle (list_length_z tbl * 4) Int.max_unsigned
-      then OK e1
-      else Error(msg "jumptable too big")
+      do e1 <- S.type_use e arg Tint;
+      if zle (list_length_z tbl * 4) Int.max_unsigned then OK e1 else Error(msg "jumptable too big")
   | Ireturn optres =>
       match optres, f.(fn_sig).(sig_res) with
       | None, None => OK e
-      | Some r, Some t => S.set e r (normalize t)
+      | Some r, Some t => S.type_use e r t
       | _, _ => Error(msg "bad return")
       end
   end.
 
 Definition type_code (e: S.typenv): res S.typenv :=
-  PTree.fold (fun re pc i =>
-    match re with
-    | Error _ => re
-    | OK e =>
-        match type_instr e i with
-        | Error msg => Error(MSG "At PC " :: POS pc :: MSG ": " :: msg)
-        | OK e' => OK e'
-        end
-    end)
-  f.(fn_code) (OK e).
+  PTree.fold
+    (fun re pc i =>
+       match re with
+       | Error _ => re
+       | OK e =>
+           match type_instr e i with
+           | Error msg => Error(MSG "At PC " :: POS pc :: MSG ": " :: msg)
+           | OK e' => OK e'
+           end
+       end)
+    f.(fn_code) (OK e).
 
 (** Solve remaining constraints *)
 
-Definition check_params_norepet (params: list reg): res unit := 
-  if list_norepet_dec Reg.eq params
-  then OK tt
-  else Error(msg "duplicate parameters").
+Definition check_params_norepet (params: list reg): res unit :=
+  if list_norepet_dec Reg.eq params then OK tt else Error(msg "duplicate parameters").
 
 Definition type_function : res regenv :=
   do e1 <- type_code S.initial;
-  do e2 <- S.set_list e1 f.(fn_params) (normalize_list f.(fn_sig).(sig_args));
+  do e2 <- S.type_defs e1 f.(fn_params) f.(fn_sig).(sig_args);
   do te <- S.solve e2;
   do x1 <- check_params_norepet f.(fn_params);
   do x2 <- check_successor f.(fn_entrypoint);
@@ -315,10 +419,10 @@ Hint Resolve type_ros_incr: ty.
 
 Lemma type_ros_sound:
   forall e ros e' te, type_ros e ros = OK e' -> S.satisf te e' ->
-  match ros with inl r => te r = Tint | inr s => True end.
+  match ros with inl r => subtype (te r) Tint = true | inr s => True end.
 Proof.
   unfold type_ros; intros. destruct ros. 
-  eapply S.set_sound; eauto.
+  eapply S.type_use_sound; eauto.
   auto.
 Qed.
 
@@ -339,6 +443,17 @@ Proof.
   monadInv H. destruct H0. subst a; eauto with ty. eauto. 
 Qed.
 
+Remark subtype_list_charact:
+  forall tyl1 tyl2,
+  subtype_list tyl1 tyl2 = true <-> list_forall2 RTLtypes.sub tyl1 tyl2.
+Proof.
+  unfold RTLtypes.sub; intros; split; intros.
+  revert tyl1 tyl2 H. induction tyl1; destruct tyl2; simpl; intros; try discriminate.
+  constructor.
+  InvBooleans. constructor; auto. 
+  revert tyl1 tyl2 H. induction 1; simpl. auto. rewrite H; rewrite IHlist_forall2; auto.
+Qed.
+
 Lemma type_instr_incr:
   forall e i e' te,
   type_instr e i = OK e' -> S.satisf te e' -> S.satisf te e.
@@ -374,56 +489,56 @@ Proof.
   + assert (o = Omove) by (unfold is_move in ISMOVE; destruct o; congruence).
     subst o.
     destruct l; try discriminate. destruct l; monadInv EQ0.
-    constructor. eapply S.move_sound; eauto. eauto with ty.
+    constructor. eapply S.type_move_sound; eauto. eauto with ty.
   + destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0.
     apply wt_Iop. 
     unfold is_move in ISMOVE; destruct o; congruence.
-    rewrite TYOP. eapply S.set_list_sound; eauto with ty.
-    rewrite TYOP. eapply S.set_sound; eauto with ty.
+    rewrite TYOP. rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty.
+    rewrite TYOP. eapply S.type_def_sound; eauto with ty.
     eauto with ty.
 - (* load *)
   constructor.
-  eapply S.set_list_sound; eauto with ty.
-  eapply S.set_sound; eauto with ty.
+  rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty.
+  eapply S.type_def_sound; eauto with ty.
   eauto with ty.
 - (* store *)
   constructor.
-  eapply S.set_list_sound; eauto with ty.
-  eapply S.set_sound; eauto with ty.
+  rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty.
+  eapply S.type_use_sound; eauto with ty.
   eauto with ty.
 - (* call *)
   constructor. 
   eapply type_ros_sound; eauto with ty.
-  eapply S.set_list_sound; eauto with ty.
-  eapply S.set_sound; eauto with ty.
+  rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty.
+  eapply S.type_def_sound; eauto with ty.
   eauto with ty.
 - (* tailcall *)
   destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
   destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2.
   constructor.
   eapply type_ros_sound; eauto with ty. 
-  eapply S.set_list_sound; eauto with ty.
   auto.
+  rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty.
   apply tailcall_is_possible_correct; auto.
 - (* builtin *)
   constructor.
-  eapply S.set_list_sound; eauto with ty.
-  eapply S.set_sound; eauto with ty.
+  rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty.
+  eapply S.type_def_sound; eauto with ty.
   eauto with ty.
 - (* cond *)
   constructor.
-  eapply S.set_list_sound; eauto with ty.
+  rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty.
   eauto with ty.
   eauto with ty.
 - (* jumptable *)
   destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2.
   constructor.
-  eapply S.set_sound; eauto.
+  eapply S.type_use_sound; eauto.
   eapply check_successors_sound; eauto. 
   auto.
 - (* return *)
   simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate.
-  econstructor. eauto. eapply S.set_sound; eauto with ty.
+  econstructor. eauto. eapply S.type_use_sound; eauto with ty.
   inv H. constructor. auto. 
 Qed.
 
@@ -460,7 +575,7 @@ Proof.
   assert (SAT1: S.satisf env x) by (eauto with ty).
   constructor.
 - (* type of parameters *)
-  eapply S.set_list_sound; eauto.
+  rewrite subtype_list_charact. eapply S.type_defs_sound; eauto.
 - (* parameters are unique *)
   unfold check_params_norepet in EQ2. 
   destruct (list_norepet_dec Reg.eq (fn_params f)); inv EQ2; auto. 
@@ -475,11 +590,11 @@ Qed.
 Lemma type_ros_complete:
   forall te ros e,
   S.satisf te e ->
-  match ros with inl r => te r = Tint | inr s => True end ->
+  match ros with inl r => subtype (te r) Tint = true | inr s => True end ->
   exists e', type_ros e ros = OK e' /\ S.satisf te e'.
 Proof.
   intros; destruct ros; simpl. 
-  eapply S.set_complete; eauto.
+  eapply S.type_use_complete; eauto.
   exists e; auto.
 Qed.
 
@@ -500,60 +615,67 @@ Proof.
 - (* nop *)
   econstructor; split. rewrite check_successor_complete; simpl; eauto. auto.
 - (* move *)
-  exploit S.move_complete; eauto. intros (changed & e' & A & B).
+  exploit S.type_move_complete; eauto. intros (changed & e' & A & B).
   exists e'; split. rewrite check_successor_complete by auto; simpl. rewrite A; auto. auto.
 - (* other op *)
   destruct (type_of_operation op) as [targ tres]. simpl in *.
-  exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]].
-  exploit S.set_complete. eexact B. eauto. intros [e2 [C D]].
+  rewrite subtype_list_charact in H1.
+  exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]].
+  exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]].
   exists e2; split; auto.
   rewrite check_successor_complete by auto; simpl. 
   replace (is_move op) with false. rewrite A; simpl; rewrite C; auto.
   destruct op; reflexivity || congruence.
 - (* load *)
-  exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]].
-  exploit S.set_complete. eexact B. eauto. intros [e2 [C D]].
+  rewrite subtype_list_charact in H0.
+  exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]].
+  exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]].
   exists e2; split; auto.
   rewrite check_successor_complete by auto; simpl. 
   rewrite A; simpl; rewrite C; auto.
 - (* store *)
-  exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]].
-  exploit S.set_complete. eexact B. eauto. intros [e2 [C D]].
+  rewrite subtype_list_charact in H0.
+  exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]].
+  exploit S.type_use_complete. eexact B. eauto. intros [e2 [C D]].
   exists e2; split; auto.
   rewrite check_successor_complete by auto; simpl. 
   rewrite A; simpl; rewrite C; auto.
 - (* call *)
   exploit type_ros_complete. eauto. eauto. intros [e1 [A B]].
-  exploit S.set_list_complete. eauto. eauto. intros [e2 [C D]].
-  exploit S.set_complete. eexact D. eauto. intros [e3 [E F]].
+  rewrite subtype_list_charact in H1.
+  exploit S.type_uses_complete. eauto. eauto. intros [e2 [C D]].
+  exploit S.type_def_complete. eexact D. eauto. intros [e3 [E F]].
   exists e3; split; auto. 
   rewrite check_successor_complete by auto; simpl. 
   rewrite A; simpl; rewrite C; simpl; rewrite E; auto.
 - (* tailcall *)
   exploit type_ros_complete. eauto. eauto. intros [e1 [A B]].
-  exploit S.set_list_complete. eauto. eauto. intros [e2 [C D]].
+  rewrite subtype_list_charact in H2.
+  exploit S.type_uses_complete. eauto. eauto. intros [e2 [C D]].
   exists e2; split; auto. 
   rewrite A; simpl; rewrite C; simpl. 
-  rewrite H2; rewrite dec_eq_true. 
+  rewrite H1; rewrite dec_eq_true. 
   replace (tailcall_is_possible sig) with true; auto. 
   revert H3. unfold tailcall_possible, tailcall_is_possible. generalize (loc_arguments sig). 
   induction l; simpl; intros. auto.
   exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl.
   intros; apply H3; auto. 
 - (* builtin *)
-  exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]].
-  exploit S.set_complete. eexact B. eauto. intros [e2 [C D]].
+  rewrite subtype_list_charact in H0.
+  exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]].
+  exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]].
   exists e2; split; auto.
   rewrite check_successor_complete by auto; simpl. 
   rewrite A; simpl; rewrite C; auto.
 - (* cond *)
-  exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]].
+  rewrite subtype_list_charact in H0.
+  exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]].
   exists e1; split; auto.
   rewrite check_successor_complete by auto; simpl. 
   rewrite check_successor_complete by auto; simpl.
   auto.
 - (* jumptbl *)
-  exploit S.set_complete. eauto. eauto. intros [e1 [A B]].
+  exploit S.type_use_complete. eauto. eauto. intros [e1 [A B]].
   exists e1; split; auto.
   replace (check_successors tbl) with (OK tt). simpl. 
   rewrite A; simpl. apply zle_true; auto. 
@@ -563,7 +685,7 @@ Proof.
 - (* return none *)
   rewrite H0. exists e; auto.
 - (* return some *)
-  rewrite H0. apply S.set_complete; auto.
+  rewrite H0. apply S.type_use_complete; auto.
 Qed.
 
 Lemma type_code_complete:
@@ -597,7 +719,8 @@ Proof.
   intros. destruct H. 
   destruct (type_code_complete te S.initial) as (e1 & A & B).
   auto. apply S.satisf_initial. 
-  destruct (S.set_list_complete te f.(fn_params) (normalize_list f.(fn_sig).(sig_args)) e1) as (e2 & C & D); auto.
+  destruct (S.type_defs_complete te f.(fn_params) f.(fn_sig).(sig_args) e1) as (e2 & C & D); auto.
+  rewrite <- subtype_list_charact; auto.
   destruct (S.solve_complete te e2) as (te' & E); auto.
   exists te'; unfold type_function.
   rewrite A; simpl. rewrite C; simpl. rewrite E; simpl. 
@@ -637,23 +760,6 @@ Proof.
   apply H.
 Qed.
 
-Lemma normalize_subtype:
-  forall ty, subtype ty (normalize ty) = true.
-Proof.
-  intros. destruct ty; reflexivity.
-Qed.
-
-Lemma wt_regset_assign2:
-  forall env rs v r ty,
-  wt_regset env rs ->
-  Val.has_type v ty ->
-  env r = normalize ty ->
-  wt_regset env (rs#r <- v).
-Proof.
-  intros. eapply wt_regset_assign; eauto.
-  rewrite H1. eapply Val.has_subtype; eauto. apply normalize_subtype.
-Qed.
-
 Lemma wt_regset_list:
   forall env rs,
   wt_regset env rs ->
@@ -682,11 +788,11 @@ Lemma wt_exec_Iop:
   wt_regset env (rs#res <- v).
 Proof.
   intros. inv H. 
-  simpl in H0. inv H0. apply wt_regset_assign; auto.
-  rewrite H4; auto.
-  eapply wt_regset_assign2; auto.
+  simpl in H0. inv H0. apply wt_regset_assign; auto. 
+  eapply Val.has_subtype; eauto. 
+  apply wt_regset_assign; auto.
+  eapply Val.has_subtype; eauto.
   eapply type_of_operation_sound; eauto.
-  auto.
 Qed.
 
 Lemma wt_exec_Iload:
@@ -697,7 +803,8 @@ Lemma wt_exec_Iload:
   wt_regset env (rs#dst <- v).
 Proof.
   intros. destruct a; simpl in H0; try discriminate. inv H.
-  eapply wt_regset_assign2; eauto.
+  apply wt_regset_assign; auto. 
+  eapply Val.has_subtype; eauto. 
   eapply Mem.load_type; eauto.
 Qed.
 
@@ -709,7 +816,8 @@ Lemma wt_exec_Ibuiltin:
   wt_regset env (rs#res <- vres).
 Proof.
   intros. inv H. 
-  eapply wt_regset_assign2; eauto. 
+  apply wt_regset_assign; auto. 
+  eapply Val.has_subtype; eauto.
   eapply external_call_well_typed; eauto.
 Qed.
 
@@ -720,46 +828,36 @@ Proof.
   intros. inv H. eauto. 
 Qed.
 
-Inductive wt_stackframes: list stackframe -> signature -> Prop :=
-  | wt_stackframes_nil: forall sg,
-      sg.(sig_res) = Some Tint ->
-      wt_stackframes nil sg
+Inductive wt_stackframes: list stackframe -> option typ -> Prop :=
+  | wt_stackframes_nil:
+      wt_stackframes nil (Some Tint)
   | wt_stackframes_cons:
-      forall s res f sp pc rs env sg,
+      forall s res f sp pc rs env tyres,
       wt_function f env ->
       wt_regset env rs ->
-      env res = normalize (proj_sig_res sg) ->
-      wt_stackframes s (fn_sig f) ->
-      wt_stackframes (Stackframe res f sp pc rs :: s) sg.
+      subtype (match tyres with None => Tint | Some t => t end) (env res) = true ->
+      wt_stackframes s (sig_res (fn_sig f)) ->
+      wt_stackframes (Stackframe res f sp pc rs :: s) tyres.
 
 Inductive wt_state: state -> Prop :=
   | wt_state_intro:
       forall s f sp pc rs m env
-        (WT_STK: wt_stackframes s (fn_sig f))
+        (WT_STK: wt_stackframes s (sig_res (fn_sig f)))
         (WT_FN: wt_function f env)
         (WT_RS: wt_regset env rs),
       wt_state (State s f sp pc rs m)
   | wt_state_call:
       forall s f args m,
-      wt_stackframes s (funsig f) ->
+      wt_stackframes s (sig_res (funsig f)) ->
       wt_fundef f ->
-      Val.has_type_list args (normalize_list (sig_args (funsig f))) ->
+      Val.has_type_list args (sig_args (funsig f)) ->
       wt_state (Callstate s f args m)
   | wt_state_return:
-      forall s v m sg,
-      wt_stackframes s sg ->
-      Val.has_type v (normalize (proj_sig_res sg)) ->
+      forall s v m tyres,
+      wt_stackframes s tyres ->
+      Val.has_type v (match tyres with None => Tint | Some t => t end) ->
       wt_state (Returnstate s v m).
 
-Remark wt_stackframes_change_sig:
-  forall s sg1 sg2,
-  sg1.(sig_res) = sg2.(sig_res) -> wt_stackframes s sg1 -> wt_stackframes s sg2.
-Proof.
-  intros. inv H0. 
-- constructor; congruence.
-- econstructor; eauto. rewrite H3. unfold proj_sig_res. rewrite H. auto. 
-Qed.
-
 Section SUBJECT_REDUCTION.
 
 Variable p: program.
@@ -793,7 +891,7 @@ Proof.
     discriminate.
   econstructor; eauto.
   econstructor; eauto. inv WTI; auto. 
-  inv WTI. rewrite <- H8. apply wt_regset_list. auto.
+  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list. auto.
   (* Itailcall *)
   assert (wt_fundef fd).
     destruct ros; simpl in H0.
@@ -804,8 +902,8 @@ Proof.
     exact wt_p. exact H0.
     discriminate.
   econstructor; eauto.
-  inv WTI. apply wt_stackframes_change_sig with (fn_sig f); auto.
-  inv WTI. rewrite <- H7. apply wt_regset_list. auto.
+  inv WTI. rewrite H7; auto. 
+  inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list. auto.
   (* Ibuiltin *)
   econstructor; eauto. eapply wt_exec_Ibuiltin; eauto.
   (* Icond *)
@@ -814,40 +912,18 @@ Proof.
   econstructor; eauto.
   (* Ireturn *)
   econstructor; eauto. 
-  inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. rewrite <- H3. auto. 
+  inv WTI; simpl. auto. rewrite H2. eapply Val.has_subtype; eauto. 
   (* internal function *)
   simpl in *. inv H5.
   econstructor; eauto.
-  inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto. 
+  inv H1. apply wt_init_regs; auto. eapply Val.has_subtype_list; eauto. 
   (* external function *)
   econstructor; eauto. simpl.  
-  change (Val.has_type res (normalize (proj_sig_res (ef_sig ef)))).
-  eapply Val.has_subtype. apply normalize_subtype. 
+  change (Val.has_type res (proj_sig_res (ef_sig ef))).
   eapply external_call_well_typed; eauto.
   (* return *)
   inv H1. econstructor; eauto.
-  apply wt_regset_assign; auto. rewrite H10; auto. 
-Qed.
-
-Lemma wt_initial_state:
-  forall S, initial_state p S -> wt_state S.
-Proof.
-  intros. inv H. constructor. constructor. rewrite H3; auto. 
-  pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b.
-  exact wt_p. exact H2.
-  rewrite H3. constructor.
-Qed.
-
-Lemma wt_instr_inv:
-  forall s f sp pc rs m i,
-  wt_state (State s f sp pc rs m) ->
-  f.(fn_code)!pc = Some i ->
-  exists env, wt_instr f env i /\ wt_regset env rs.
-Proof.
-  intros. inv H. exists env; split; auto. 
-  inv WT_FN. eauto. 
+  apply wt_regset_assign; auto. eapply Val.has_subtype; eauto. 
 Qed.
 
 End SUBJECT_REDUCTION.
-
-  
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index cea2e0b..9b144cb 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -664,12 +664,17 @@ Record agree_frame (j: meminj) (ls ls0: locset)
 
     (** Permissions on the frame part of the Mach stack block *)
     agree_perm:
-      frame_perm_freeable m' sp'
+      frame_perm_freeable m' sp';
+
+    (** Current locset is well-typed *)
+    agree_wt_ls:
+      wt_locset ls
   }.
 
 Hint Resolve agree_unused_reg agree_locals agree_outgoing agree_incoming
              agree_link agree_retaddr agree_saved_int agree_saved_float
-             agree_valid_linear agree_valid_mach agree_perm: stacking.
+             agree_valid_linear agree_valid_mach agree_perm
+             agree_wt_ls: stacking.
 
 (** Auxiliary predicate used at call points *)
 
@@ -788,16 +793,19 @@ Lemma agree_frame_set_reg:
   forall j ls ls0 m sp m' sp' parent ra r v,
   agree_frame j ls ls0 m sp m' sp' parent ra ->
   mreg_within_bounds b r ->
+   Val.has_type v (Loc.type (R r)) ->
   agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra.
 Proof.
   intros. inv H; constructor; auto; intros.
   rewrite Locmap.gso. auto. red. intuition congruence.
+  apply wt_setreg; auto.
 Qed.
 
 Lemma agree_frame_set_regs:
   forall j ls0 m sp m' sp' parent ra rl vl ls,
   agree_frame j ls ls0 m sp m' sp' parent ra ->
   (forall r, In r rl -> mreg_within_bounds b r) ->
+  Val.has_type_list vl (map Loc.type (map R rl)) ->
   agree_frame j (Locmap.setlist (map R rl) vl ls) ls0 m sp m' sp' parent ra.
 Proof.
   induction rl; destruct vl; simpl; intros; intuition.
@@ -813,7 +821,7 @@ Lemma agree_frame_undef_regs:
 Proof.
   induction regs; simpl; intros.
   auto.
-  apply agree_frame_set_reg; auto.
+  apply agree_frame_set_reg; auto. red; auto.
 Qed.
 
 Lemma caller_save_reg_within_bounds:
@@ -844,18 +852,17 @@ Lemma agree_frame_set_local:
   forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true ->
-  Val.has_type v ty ->
   val_inject j v v' ->
   Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' ->
   agree_frame j (Locmap.set (S Local ofs ty) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
   intros. inv H. 
-  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H4.
+  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3.
   constructor; auto; intros.
 (* local *)
   unfold Locmap.set.
   destruct (Loc.eq (S Local ofs ty) (S Local ofs0 ty0)).
-  inv e. eapply gss_index_contains_inj; eauto with stacking.
+  inv e. eapply gss_index_contains_inj'; eauto with stacking.
   destruct (Loc.diff_dec (S Local ofs ty) (S Local ofs0 ty0)).
   eapply gso_index_contains_inj. eauto. eauto with stacking. eauto. 
   simpl. simpl in d. intuition.
@@ -876,6 +883,8 @@ Proof.
   eauto with mem.
 (* perm *)
   red; intros. eapply Mem.perm_store_1; eauto.
+(* wt *)
+  apply wt_setstack; auto. 
 Qed.
 
 (** Preservation by assignment to outgoing slot *)
@@ -884,20 +893,19 @@ Lemma agree_frame_set_outgoing:
   forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true ->
-  Val.has_type v ty ->
   val_inject j v v' ->
   Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' ->
   agree_frame j (Locmap.set (S Outgoing ofs ty) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
   intros. inv H. 
-  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H4.
+  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3.
   constructor; auto; intros.
 (* local *)
   rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking. red; auto.
   red; left; congruence.
 (* outgoing *)
   unfold Locmap.set. destruct (Loc.eq (S Outgoing ofs ty) (S Outgoing ofs0 ty0)).
-  inv e. eapply gss_index_contains_inj; eauto with stacking.
+  inv e. eapply gss_index_contains_inj'; eauto with stacking.
   destruct (Loc.diff_dec (S Outgoing ofs ty) (S Outgoing ofs0 ty0)).
   eapply gso_index_contains_inj; eauto with stacking.
   red. red in d. intuition. 
@@ -915,6 +923,8 @@ Proof.
   eauto with mem stacking.
 (* perm *)
   red; intros. eapply Mem.perm_store_1; eauto.
+(* wt *)
+  apply wt_setstack; auto. 
 Qed.
 
 (** General invariance property with respect to memory changes. *)
@@ -1041,6 +1051,7 @@ Lemma agree_frame_return:
   forall j ls ls0 m sp m' sp' parent retaddr ls',
   agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   agree_callee_save ls' ls ->
+  wt_locset ls' ->
   agree_frame j ls' ls0 m sp m' sp' parent retaddr.
 Proof.
   intros. red in H0. inv H; constructor; auto; intros.
@@ -1236,7 +1247,7 @@ Hypothesis csregs_typ:
 Hypothesis ls_temp_undef:
   forall r, In r (destroyed_by_setstack ty) -> ls (R r) = Vundef.
 
-Hypothesis wt_ls: wt_locset Regset.empty ls.
+Hypothesis wt_ls: wt_locset ls.
 
 Lemma save_callee_save_regs_correct:
   forall l k rs m,
@@ -1293,8 +1304,7 @@ Proof.
   simpl in H3. destruct (mreg_eq a r). subst r.
   assert (index_contains_inj j m1 sp (mkindex (number a)) (ls (R a))).
     eapply gss_index_contains_inj; eauto.
-    rewrite mkindex_typ. rewrite <- (csregs_typ a). eapply wt_mreg; eauto. 
-    auto with coqlib.
+    rewrite mkindex_typ. rewrite <- (csregs_typ a). apply wt_ls. auto with coqlib.
   destruct H5 as [v' [P Q]].
   exists v'; split; auto. apply C; auto. 
   intros. apply mkindex_inj. apply number_inj; auto with coqlib. 
@@ -1344,7 +1354,7 @@ Qed.
 Lemma save_callee_save_correct:
   forall j ls0 rs sp cs fb k m,
   let ls := LTL.undef_regs destroyed_at_function_entry ls0 in
-  agree_regs j ls rs -> wt_locset Regset.empty ls ->
+  agree_regs j ls rs -> wt_locset ls ->
   frame_perm_freeable m sp ->
   exists rs', exists m',
     star step tge 
@@ -1470,7 +1480,7 @@ Lemma function_prologue_correct:
   forall j ls ls0 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k,
   agree_regs j ls rs ->
   agree_callee_save ls ls0 ->
-  wt_locset Regset.empty ls ->
+  wt_locset ls ->
   ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) ->
   rs1 = undef_regs destroyed_at_function_entry rs ->
   Mem.inject j m1 m1' ->
@@ -1530,7 +1540,7 @@ Proof.
     instantiate (1 := rs1). instantiate (1 := call_regs ls). instantiate (1 := j').
     subst rs1. apply agree_regs_undef_regs. 
     apply agree_regs_call_regs. eapply agree_regs_inject_incr; eauto.
-    apply wt_undef_regs. eapply wt_call_regs. eauto.
+    apply wt_undef_regs. apply wt_call_regs. auto.
     eexact PERM4.
   rewrite <- LS1.
   intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]].
@@ -1612,6 +1622,8 @@ Proof.
     exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto.
     (* perms *)
     auto.
+    (* wt *)
+    rewrite LS1. apply wt_undef_regs. apply wt_call_regs; auto.
   (* incr *)
   split. auto.
   (* separated *)
@@ -1854,6 +1866,7 @@ Inductive match_stacks (j: meminj) (m m': mem):
       match_stacks j m m' nil nil sg bound bound'
   | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf
         (TAIL: is_tail c (Linear.fn_code f))
+        (WTF: wt_function f = true)
         (FINDF: Genv.find_funct_ptr tge fb = Some (Internal trf))
         (TRF: transf_function f = OK trf)
         (TRC: transl_code (make_env (function_bounds f)) c = c')
@@ -2042,6 +2055,16 @@ Qed.
 
 (** Typing properties of [match_stacks]. *)
 
+Lemma match_stacks_wt_locset:
+  forall j m m' cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  wt_locset (parent_locset cs).
+Proof.
+  induction 1; simpl.
+  unfold Locmap.init; red; intros; red; auto.
+  inv FRM; auto.
+Qed.
+
 Lemma match_stacks_type_sp:
   forall j m m' cs cs' sg bound bound',
   match_stacks j m m' cs cs' sg bound bound' ->
@@ -2434,6 +2457,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
         (STACKS: match_stacks j m m' cs cs' f.(Linear.fn_sig) sp sp')
         (TRANSL: transf_function f = OK tf)
         (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf))
+        (WTF: wt_function f = true)
         (AGREGS: agree_regs j ls rs)
         (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs'))
         (TAIL: is_tail c (Linear.fn_code f)),
@@ -2445,6 +2469,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
         (STACKS: match_stacks j m m' cs cs' (Linear.funsig f) (Mem.nextblock m) (Mem.nextblock m'))
         (TRANSL: transf_fundef f = OK tf)
         (FIND: Genv.find_funct_ptr tge fb = Some tf)
+        (WTLS: wt_locset ls)
         (AGREGS: agree_regs j ls rs)
         (AGLOCS: agree_callee_save ls (parent_locset cs)),
       match_states (Linear.Callstate cs f ls m)
@@ -2453,6 +2478,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
       forall cs ls m cs' rs m' j sg 
         (MINJ: Mem.inject j m m')
         (STACKS: match_stacks j m m' cs cs' sg (Mem.nextblock m) (Mem.nextblock m'))
+        (WTLS: wt_locset ls)
         (AGREGS: agree_regs j ls rs)
         (AGLOCS: agree_callee_save ls (parent_locset cs)),
       match_states (Linear.Returnstate cs ls m)
@@ -2460,40 +2486,37 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
 
 Theorem transf_step_correct:
   forall s1 t s2, Linear.step ge s1 t s2 ->
-  forall (WTS: wt_state s1) s1' (MS: match_states s1 s1'),
+  forall s1' (MS: match_states s1 s1'),
   exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.
 Proof.
-(*
   assert (USEWTF: forall f i c,
           wt_function f = true -> is_tail (i :: c) (Linear.fn_code f) ->
           wt_instr f i = true).
     intros. unfold wt_function, wt_code in H. rewrite forallb_forall in H.
     apply H. eapply is_tail_in; eauto. 
-*)
   induction 1; intros;
   try inv MS;
   try rewrite transl_code_eq;
+  try (generalize (USEWTF _ _ _ WTF TAIL); intro WTI; simpl in WTI; InvBooleans);
   try (generalize (function_is_within_bounds f _ (is_tail_in TAIL));
        intro BOUND; simpl in BOUND);
   unfold transl_instr.
 
-- (* Lgetstack *)
-  destruct BOUND.
-  exploit wt_state_getstack; eauto. intros SV.
-  unfold destroyed_by_getstack; destruct sl.
-+ (* Lgetstack, local *)
+  (* Lgetstack *)
+  destruct BOUND. unfold destroyed_by_getstack; destruct sl.
+  (* Lgetstack, local *)
   exploit agree_locals; eauto. intros [v [A B]].
   econstructor; split.
   apply plus_one. apply exec_Mgetstack. 
   eapply index_contains_load_stack; eauto.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg; auto.
-  apply agree_frame_set_reg; auto.
-+ (* Lgetstack, incoming *)
-  unfold slot_valid in SV. InvBooleans.
+  apply agree_frame_set_reg; auto. simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto.
+  (* Lgetstack, incoming *)
+  unfold slot_valid in H0. InvBooleans.
   exploit incoming_slot_in_parameters; eauto. intros IN_ARGS.
   inversion STACKS; clear STACKS.
-  elim (H6 _ IN_ARGS).
+  elim (H7 _ IN_ARGS).
   subst bound bound' s cs'.
   exploit agree_outgoing. eexact FRM. eapply ARGS; eauto.
   exploit loc_arguments_acceptable; eauto. intros [A B].
@@ -2514,7 +2537,8 @@ Proof.
   eapply agree_frame_set_reg; eauto. eapply agree_frame_set_reg; eauto. 
   apply caller_save_reg_within_bounds. 
   apply temp_for_parent_frame_caller_save.
-+ (* Lgetstack, outgoing *)
+  simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto.
+  (* Lgetstack, outgoing *)
   exploit agree_outgoing; eauto. intros [v [A B]].
   econstructor; split.
   apply plus_one. apply exec_Mgetstack. 
@@ -2522,55 +2546,66 @@ Proof.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg; auto.
   apply agree_frame_set_reg; auto.
+  simpl. eapply Val.has_subtype; eauto. eapply agree_wt_ls; eauto.
 
-- (* Lsetstack *)
-  exploit wt_state_setstack; eauto. intros (VTY & SV & SW). 
+  (* Lsetstack *)
   set (idx := match sl with
               | Local => FI_local ofs ty
               | Incoming => FI_link (*dummy*)
               | Outgoing => FI_arg ofs ty
               end).
   assert (index_valid f idx).
-  { unfold idx; destruct sl.
+    unfold idx; destruct sl.
     apply index_local_valid; auto.
     red; auto.
-    apply index_arg_valid; auto. }
+    apply index_arg_valid; auto.
   exploit store_index_succeeds; eauto. eapply agree_perm; eauto.
   instantiate (1 := rs0 src). intros [m1' STORE].
   econstructor; split.
-  apply plus_one. destruct sl; simpl in SW.
+  apply plus_one. destruct sl; simpl in H0.
     econstructor. eapply store_stack_succeeds with (idx := idx); eauto. eauto.
     discriminate.
     econstructor. eapply store_stack_succeeds with (idx := idx); eauto. auto. 
   econstructor. 
   eapply Mem.store_outside_inject; eauto. 
     intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta.
-    rewrite size_type_chunk in H2.
+    rewrite size_type_chunk in H4.
     exploit offset_of_index_disj_stack_data_2; eauto.
     exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. 
     omega.
   apply match_stacks_change_mach_mem with m'; auto.
-  eauto with mem. eauto with mem. intros. rewrite <- H1; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. 
+  eauto with mem. eauto with mem. intros. rewrite <- H3; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. 
   eauto. eauto. auto. 
   apply agree_regs_set_slot. apply agree_regs_undef_regs; auto. 
   destruct sl.
-  + eapply agree_frame_set_local. eapply agree_frame_undef_locs; eauto.
-    apply destroyed_by_setstack_caller_save. auto. auto. auto. apply AGREGS. 
+    eapply agree_frame_set_local. eapply agree_frame_undef_locs; eauto.
+    apply destroyed_by_setstack_caller_save. auto. auto. apply AGREGS. 
+    assumption. 
+    simpl in H0; discriminate.
+    eapply agree_frame_set_outgoing. eapply agree_frame_undef_locs; eauto.
+    apply destroyed_by_setstack_caller_save. auto. auto. apply AGREGS.
     assumption. 
-  + simpl in SW; discriminate.
-  + eapply agree_frame_set_outgoing. eapply agree_frame_undef_locs; eauto.
-    apply destroyed_by_setstack_caller_save. auto. auto. auto. apply AGREGS.
-    assumption.
-  + eauto with coqlib.
+  eauto with coqlib.
 
-- (* Lop *)
+  (* Lop *)
+  assert (Val.has_type v (mreg_type res)).
+    destruct (is_move_operation op args) as [arg|] eqn:?.
+    exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst op args. 
+    eapply Val.has_subtype; eauto. simpl in H; inv H. eapply agree_wt_ls; eauto. 
+    destruct (type_of_operation op) as [targs tres] eqn:TYOP. 
+    eapply Val.has_subtype; eauto. 
+    replace tres with (snd (type_of_operation op)).
+    eapply type_of_operation_sound; eauto.
+    red; intros. subst op. simpl in Heqo.
+    destruct args; simpl in H. discriminate. destruct args. discriminate. simpl in H. discriminate.
+    rewrite TYOP; auto. 
   assert (exists v',
           eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v'
        /\ val_inject j v v').
   eapply eval_operation_inject; eauto.
   eapply match_stacks_preserves_globals; eauto.
   eapply agree_inj; eauto. eapply agree_reglist; eauto.
-  destruct H0 as [v' [A B]].
+  destruct H1 as [v' [A B]].
   econstructor; split. 
   apply plus_one. econstructor. 
   instantiate (1 := v'). rewrite <- A. apply eval_operation_preserved. 
@@ -2581,7 +2616,7 @@ Proof.
   apply agree_frame_set_reg; auto. apply agree_frame_undef_locs; auto.
   apply destroyed_by_op_caller_save.
 
-- (* Lload *)
+  (* Lload *)
   assert (exists a',
           eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
        /\ val_inject j a a').
@@ -2598,8 +2633,9 @@ Proof.
   apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. 
   apply agree_frame_set_reg. apply agree_frame_undef_locs; auto.
   apply destroyed_by_load_caller_save. auto. 
+  simpl. eapply Val.has_subtype; eauto. destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
 
-- (* Lstore *)
+  (* Lstore *)
   assert (exists a',
           eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
        /\ val_inject j a a').
@@ -2620,7 +2656,7 @@ Proof.
   eapply agree_frame_parallel_stores; eauto.
   apply destroyed_by_store_caller_save. 
 
-- (* Lcall *)
+  (* Lcall *)
   exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
   exploit is_tail_transf_function; eauto. intros IST.
   rewrite transl_code_eq in IST. simpl in IST.
@@ -2636,9 +2672,10 @@ Proof.
     apply loc_arguments_bounded; auto.
   eapply agree_valid_linear; eauto.
   eapply agree_valid_mach; eauto.
+  eapply agree_wt_ls; eauto. 
   simpl; red; auto.
 
-- (* Ltailcall *)
+  (* Ltailcall *)
   exploit function_epilogue_correct; eauto.
   intros [rs1 [m1' [P [Q [R [S [T [U V]]]]]]]].
   exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
@@ -2651,13 +2688,14 @@ Proof.
   apply match_stacks_change_mach_mem with m'0.
   auto. 
   eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; apply Plt_ne; auto. 
-  intros. rewrite <- H1. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. 
+  intros. rewrite <- H3. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. 
   eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
   apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
   apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
-  apply zero_size_arguments_tailcall_possible. eapply wt_state_tailcall; eauto. 
+  apply zero_size_arguments_tailcall_possible; auto. 
+  apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
-- (* Lbuiltin *)
+  (* Lbuiltin *)
   exploit external_call_mem_inject'; eauto. 
     eapply match_stacks_preserves_globals; eauto.
     eapply agree_reglist; eauto. 
@@ -2679,9 +2717,12 @@ Proof.
   intros. inv H; eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto.
   eapply external_call_valid_block'; eauto.
   eapply agree_valid_mach; eauto.
+  simpl. rewrite list_map_compose.
+  change (fun x => Loc.type (R x)) with mreg_type.
+  eapply Val.has_subtype_list; eauto. eapply external_call_well_typed'; eauto.
 
-- (* Lannot *)
-  exploit transl_annot_params_correct; eauto. eapply wt_state_annot; eauto.
+  (* Lannot *)
+  exploit transl_annot_params_correct; eauto.
   intros [vargs' [P Q]]. 
   exploit external_call_mem_inject'; eauto. 
     eapply match_stacks_preserves_globals; eauto.
@@ -2702,49 +2743,49 @@ Proof.
   eapply external_call_valid_block'; eauto.
   eapply agree_valid_mach; eauto.
 
-- (* Llabel *)
+  (* Llabel *)
   econstructor; split.
   apply plus_one; apply exec_Mlabel.
   econstructor; eauto with coqlib.
 
-- (* Lgoto *)
+  (* Lgoto *)
   econstructor; split.
   apply plus_one; eapply exec_Mgoto; eauto.
   apply transl_find_label; eauto.
   econstructor; eauto. 
   eapply find_label_tail; eauto.
 
-- (* Lcond, true *)
+  (* Lcond, true *)
   econstructor; split.
   apply plus_one. eapply exec_Mcond_true; eauto.
   eapply eval_condition_inject; eauto. eapply agree_reglist; eauto.
   eapply transl_find_label; eauto.
-  econstructor. eauto. eauto. eauto. eauto.
+  econstructor. eauto. eauto. eauto. eauto. eauto. 
   apply agree_regs_undef_regs; auto. 
   apply agree_frame_undef_locs; auto. apply destroyed_by_cond_caller_save. 
   eapply find_label_tail; eauto.
 
-- (* Lcond, false *)
+  (* Lcond, false *)
   econstructor; split.
   apply plus_one. eapply exec_Mcond_false; eauto.
   eapply eval_condition_inject; eauto. eapply agree_reglist; eauto.
-  econstructor. eauto. eauto. eauto. eauto.
+  econstructor. eauto. eauto. eauto. eauto. eauto. 
   apply agree_regs_undef_regs; auto. 
   apply agree_frame_undef_locs; auto. apply destroyed_by_cond_caller_save. 
   eauto with coqlib.
 
-- (* Ljumptable *)
+  (* Ljumptable *)
   assert (rs0 arg = Vint n).
-  { generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto. }
+    generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto.
   econstructor; split.
   apply plus_one; eapply exec_Mjumptable; eauto. 
   apply transl_find_label; eauto.
-  econstructor. eauto. eauto. eauto. eauto.
+  econstructor. eauto. eauto. eauto. eauto. eauto.
   apply agree_regs_undef_regs; auto.
   apply agree_frame_undef_locs; auto. apply destroyed_by_jumptable_caller_save.
   eapply find_label_tail; eauto.
 
-- (* Lreturn *)
+  (* Lreturn *)
   exploit function_epilogue_correct; eauto.
   intros [rs1 [m1' [P [Q [R [S [T [U V]]]]]]]].
   econstructor; split.
@@ -2760,12 +2801,13 @@ Proof.
   eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
   apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
   apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
+  apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
-- (* internal function *)
+  (* internal function *)
   revert TRANSL. unfold transf_fundef, transf_partial_fundef.
   caseEq (transf_function f); simpl; try congruence.
   intros tfn TRANSL EQ. inversion EQ; clear EQ; subst tf.
-  exploit function_prologue_correct; eauto. eapply wt_callstate_wt_locset; eauto.
+  exploit function_prologue_correct; eauto.
   eapply match_stacks_type_sp; eauto. 
   eapply match_stacks_type_retaddr; eauto.
   intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]].
@@ -2786,9 +2828,10 @@ Proof.
   intros. eapply stores_in_frame_perm; eauto with mem.
   intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto.
   eapply Mem.load_alloc_unchanged; eauto. red. congruence.
+  eapply transf_function_well_typed; eauto.
   auto with coqlib.
 
-- (* external function *)
+  (* external function *)
   simpl in TRANSL. inversion TRANSL; subst tf.
   exploit transl_external_arguments; eauto. intros [vl [ARGS VINJ]].
   exploit external_call_mem_inject'; eauto. 
@@ -2803,10 +2846,11 @@ Proof.
   inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. 
   eapply external_call_nextblock'; eauto.
   eapply external_call_nextblock'; eauto.
+  inv H0. apply wt_setlist_result. eapply external_call_well_typed; eauto. auto.
   apply agree_regs_set_regs; auto. apply agree_regs_inject_incr with j; auto. 
   apply agree_callee_save_set_result; auto. 
 
-- (* return *)
+  (* return *)
   inv STACKS. simpl in AGLOCS.  
   econstructor; split.
   apply plus_one. apply exec_return. 
@@ -2835,6 +2879,7 @@ Proof.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.
   rewrite H3. red; intros. contradiction.
+  apply wt_init.
   unfold Locmap.init. red; intros; auto.
   unfold parent_locset. red; auto.
 Qed.
@@ -2848,31 +2893,14 @@ Proof.
   econstructor; eauto. 
 Qed.
 
-Lemma wt_prog:
-  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.
-Proof.
-  intros. exploit transform_partial_program_succeeds; eauto. 
-  intros [tfd TF]. destruct fd; simpl in *. 
-- monadInv TF. unfold transf_function in EQ.
-  destruct (wt_function f). auto. discriminate.  
-- auto.
-Qed.
-
 Theorem transf_program_correct:
   forward_simulation (Linear.semantics prog) (Mach.semantics return_address_offset tprog).
 Proof.
-  set (ms := fun s s' => wt_state s /\ match_states s s').
-  eapply forward_simulation_plus with (match_states := ms). 
-- exact symbols_preserved.
-- intros. exploit transf_initial_states; eauto. intros [st2 [A B]]. 
-  exists st2; split; auto. split; auto.
-  apply wt_initial_state with (prog := prog); auto. exact wt_prog. 
-- intros. destruct H. eapply transf_final_states; eauto. 
-- intros. destruct H0. 
-  exploit transf_step_correct; eauto. intros [s2' [A B]].
-  exists s2'; split. exact A. split.
-  eapply step_type_preservation; eauto. eexact wt_prog. eexact H. 
-  auto.
+  eapply forward_simulation_plus.
+  eexact symbols_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  eexact transf_step_correct. 
 Qed.
 
 End PRESERVATION.