Some progress in Asmblockgenproof

4 files changed, 566 insertions, 1494 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index e260bd69..325f238c 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -579,47 +579,47 @@ Definition cond_for_cond (cond: condition) :=
   without setting then testing condition flags.  *)
 
 Definition transl_cond_branch_default
-  (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*control) :=
+  (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) :=
   do ccode <- transl_cond c args k;
-  OK(ccode, PCtlFlow (Pbc (cond_for_cond c) lbl)).
+  OK(ccode, Pbc (cond_for_cond c) lbl).
  
 Definition transl_cond_branch
-  (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*control) :=
+  (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) :=
   match args, c with
   | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) =>
       if Int.eq n Int.zero
-      then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbnz W r1 lbl)))
+      then (do r1 <- ireg_of a1; OK (k, Pcbnz W r1 lbl))
       else transl_cond_branch_default c args lbl k
   | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) =>
       if Int.eq n Int.zero
-      then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbz W r1 lbl)))
+      then (do r1 <- ireg_of a1; OK (k, Pcbz W r1 lbl))
       else transl_cond_branch_default c args lbl k
   | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) =>
       if Int64.eq n Int64.zero
-      then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbnz X r1 lbl)))
+      then (do r1 <- ireg_of a1; OK (k, Pcbnz X r1 lbl))
       else transl_cond_branch_default c args lbl k
   | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) =>
       if Int64.eq n Int64.zero
-      then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbz X r1 lbl)))
+      then (do r1 <- ireg_of a1; OK (k, Pcbz X r1 lbl))
       else transl_cond_branch_default c args lbl k
   | a1 :: nil, Cmaskzero n =>
       match Int.is_power2 n with
-      | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbz W r1 bit lbl))
+      | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz W r1 bit lbl)
       | None => transl_cond_branch_default c args lbl k
       end
   | a1 :: nil, Cmasknotzero n =>
       match Int.is_power2 n with
-      | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbnz W r1 bit lbl))
+      | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz W r1 bit lbl)
       | None => transl_cond_branch_default c args lbl k
       end
   | a1 :: nil, Cmasklzero n =>
       match Int64.is_power2' n with
-      | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbz X r1 bit lbl))
+      | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz X r1 bit lbl)
       | None => transl_cond_branch_default c args lbl k
       end
   | a1 :: nil, Cmasklnotzero n =>
       match Int64.is_power2' n with
-      | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbnz X r1 bit lbl))
+      | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz X r1 bit lbl)
       | None => transl_cond_branch_default c args lbl k
       end
   | _, _ =>
@@ -1234,7 +1234,7 @@ Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res
       OK (make_epilogue f, PCtlFlow (Pbr r1 sig))
   | MBbuiltin ef args res => OK (nil, Pbuiltin ef (List.map (map_builtin_arg dreg_of) args) (map_builtin_res dreg_of res))
   | MBgoto lbl => OK (nil, PCtlFlow (Pb lbl))
-  | MBcond cond args lbl => transl_cond_branch cond args lbl nil
+  | MBcond cond args lbl => do (bc, c) <- transl_cond_branch cond args lbl nil; OK (bc, PCtlFlow c)
   | MBreturn => OK (make_epilogue f, PCtlFlow (Pret RA))
   | MBjumptable arg tbl => do r <- ireg_of arg;
       OK (nil, PCtlFlow (Pbtbl r tbl))
@@ -1272,7 +1272,8 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep:
 
 Program Definition make_prologue (f:  Machblock.function) (k:bblocks) :=
   {| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi
-      storeptr_bc RA XSP f.(fn_retaddr_ofs) nil;
+(*       storeptr_bc RA XSP f.(fn_retaddr_ofs) nil; *)
+      ((PSt_rs_a Pstrx RA) (ADimm XSP (Ptrofs.to_int64 (f.(fn_retaddr_ofs))))) ::bi nil;
       exit := None |} :: k.
   
 (*    Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
@@ -1290,7 +1291,7 @@ Definition transf_function (f: Machblock.function) : res Asmblock.function :=
   else OK tf.
 
 Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
-  transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *)
+  transf_partial_fundef transf_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *)
 
 Definition transf_program (p: Machblock.program) : res Asmblock.program :=
   transform_partial_program transf_fundef p.
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 55f50b7a..586286bd 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -63,8 +63,7 @@ Lemma functions_transl:
   Genv.find_funct_ptr tge fb = Some (Internal tf).
 Proof.
   intros. exploit functions_translated; eauto. intros [tf' [A B]].
-  monadInv B. unfold transf_function in H0. monadInv H0.
-  destruct zlt; try discriminate. rewrite EQ in EQ0. inv EQ0; inv EQ1; auto.
+  monadInv B. rewrite H0 in EQ; inv EQ; auto.
 Qed.
 
 Lemma transf_function_no_overflow:
@@ -347,67 +346,34 @@ Ltac exploreInst :=
 
 (** Some translation properties *)
 
-Lemma no_builtin_preserved:
-  forall f ex x1 x2,
-  (forall ef args res, ex <> Some (MBbuiltin ef args res)) ->
-  transl_exit f ex = OK(x1, x2) ->
-  (exists i, x2 = Some (PCtlFlow i))
-    \/ x2 = None.
-Proof.
-  intros until x2. intros Hbuiltin TIC.
-  destruct ex.
-  - destruct c.
-    (* MBcall *)
-    + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto.
-    (* MBtailcall *)
-    + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto.
-    (* MBbuiltin *)
-    + assert (H: Some (MBbuiltin e l b) <>  Some (MBbuiltin e l b)).
-        apply Hbuiltin. contradict H; auto.
-    (* MBgoto *)
-    + simpl in TIC. exploreInst; simpl; eauto.
-    (* MBcond *)
-    + simpl in TIC. unfold transl_cond_branch, transl_cond_branch_default in TIC.
-      monadInv TIC; exploreInst; simpl; eauto.
-    (* MBjumptable *)
-    + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto.
-    (* MBreturn *)
-    + simpl in TIC. monadInv TIC. simpl. eauto.
-  - monadInv TIC. simpl; auto.
-Qed.
-
 Lemma transl_blocks_distrib:
   forall c f bb tbb tc ep,
   transl_blocks f (bb::c) ep = OK (tbb::tc)
-  -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res))
   -> transl_block f bb (if MB.header bb then ep else false) = OK (tbb :: nil)
   /\ transl_blocks f c false = OK tc.
 Proof.
-  intros until ep. intros TLBS Hbuiltin.
+  intros until ep. intros TLBS.
   destruct bb as [hd bdy ex].
   monadInv TLBS. monadInv EQ.
-  exploit no_builtin_preserved; eauto. intros Hectl. destruct Hectl.
-  - destruct H as [i Hectl].
-    unfold cons_bblocks in H0. rewrite Hectl in H0.
-    destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ0;
-    simpl in *; unfold transl_block; simpl; rewrite H0; simpl;
-    rewrite EQ; simpl; rewrite CBDY; auto.
-  - unfold cons_bblocks in H0. rewrite H in H0.
-    destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ0;
-    simpl in *; unfold transl_block; simpl; rewrite H0; simpl;
-    rewrite EQ; simpl; rewrite CBDY; auto.
+  unfold transl_block.
+  rewrite EQ0; simpl.
+  simpl in EQ; rewrite EQ; simpl.
+  unfold cons_bblocks in *. simpl in EQ0.
+  destruct ex.
+  - simpl in *. monadInv EQ0.
+    destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ1; auto.
+  - simpl in *. inv EQ0. destruct (x3 @@ nil) eqn: CBDY; inv H0; inv EQ1; auto.
 Qed.
 
-Lemma cons_bblocks_nobuiltin:
+Lemma cons_bblocks_decomp:
   forall thd tbdy tex tbb,
   (tbdy <> nil \/ tex <> None) ->
-  (forall ef args res, tex <> Some (Pbuiltin ef args res)) ->
   cons_bblocks thd tbdy tex = tbb :: nil ->
      header tbb = thd
   /\ body tbb = tbdy
   /\ exit tbb = tex.
 Proof.
-  intros until tbb. intros Hnonil Hnobuiltin CONSB. unfold cons_bblocks in CONSB.
+  intros until tbb. intros Hnonil CONSB. unfold cons_bblocks in CONSB.
   destruct (tex) eqn:ECTL.
   - destruct tbdy; inv CONSB; simpl; auto.
   - inversion Hnonil.
@@ -622,21 +588,6 @@ Proof.
   - contradict Hnonil; auto.
 Qed.
 
-Lemma transl_exit_nobuiltin:
-  forall f ex bdy x,
-  (forall ef args res, ex <> Some (MBbuiltin ef args res)) ->
-  transl_exit f ex = OK (bdy, x) ->
-  (forall ef args res, x <> Some (Pbuiltin ef args res)).
-Proof.
-  intros until x. intros Hnobuiltin TIC. intros until res.
-  unfold transl_exit, transl_control in TIC. exploreInst. monadInv TIC.
-  exploreInst.
-  all: try discriminate.
-  - assert False. eapply Hnobuiltin; eauto. destruct H.
-  - unfold transl_cond_branch, transl_cond_branch_default in EQ. exploreInst.
-    all: try discriminate.
-Qed.
-
 Theorem app_nonil: forall A (l1 l2: list A),
   l1 <> nil ->
   l1 @@ l2 <> nil.
@@ -650,7 +601,6 @@ Qed.
 
 Theorem match_state_codestate:
   forall mbs abs s fb sp bb c ms m,
-  (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
   (MB.body bb <> nil \/ MB.exit bb <> None) ->
   mbs = (Machblock.State s fb sp (bb::c) ms m) ->
   match_states mbs abs ->
@@ -663,16 +613,15 @@ Theorem match_state_codestate:
     /\ cur cs = tbb /\ rem cs = tc
     /\ pstate cs = abs.
 Proof.
-  intros until m. intros Hnobuiltin Hnotempty Hmbs MS. subst. inv MS.
+  intros until m. intros Hnotempty Hmbs MS. subst. inv MS.
   inv AT. clear H0. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst.
   exploit transl_blocks_distrib; eauto. intros (TLB & TLBS). clear H2.
-  monadInv TLB. exploit cons_bblocks_nobuiltin; eauto.
+  monadInv TLB. exploit cons_bblocks_decomp; eauto.
     { inversion Hnotempty.
       - destruct (MB.body bb) as [|bi bdy]; try (contradict H0; simpl; auto; fail).
         left. apply app_nonil. eapply transl_basic_code_nonil; eauto.
       - destruct (MB.exit bb) as [ei|]; try (contradict H0; simpl; auto; fail).
         right. eapply transl_exit_nonil; eauto. }
-    eapply transl_exit_nobuiltin; eauto.
   intros (Hth & Htbdy & Htexit).
   exists {| pstate := (State rs m'); pheader := (Machblock.header bb); pbody1 := x1; pbody2 := x;
             pctl := x0; ep := ep0; rem := tc'; cur := tbb |}, fb, f, tbb, tc', ep0.
@@ -740,30 +689,22 @@ Proof.
   intros. destruct (PregEq.eq r X30); [ rewrite e in H; simpl in H; discriminate | auto ].
 Qed.
 
+Lemma X16_not_data_preg: forall r ,
+  data_preg r = true ->
+  r <> X16.
+Proof.
+  intros. destruct (PregEq.eq r X16); [ rewrite e in H; simpl in H; discriminate | auto ].
+Qed.
+
 Ltac Simpl :=
   rewrite Pregmap.gso; try apply PC_not_data_preg; try apply X30_not_data_preg.
   
-Ltac ArgsInv :=
-  repeat (match goal with
-  | [ H: Error _ = OK _ |- _ ] => discriminate
-  | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args
-  | [ H: bind _ _ = OK _ |- _ ] => monadInv H
-  | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
-  | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
-  end);
-  subst;
-  repeat (match goal with
-  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *
-  | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
-  end).
-  
 (* See (C) in the diagram. The proofs are mostly adapted from the previous Mach->Asm proofs, but are
    unfortunately quite cumbersome. To reproduce them, it's best to have a Coq IDE with you and see by
    yourself the steps *)
 Theorem step_simu_control:
   forall bb' fb fn s sp c ms' m' rs2 m2 t S'' rs1 m1 tbb tbdy2 tex cs2,
   MB.body bb' = nil ->
-  (forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) ->
   Genv.find_funct_ptr tge fb = Some (Internal fn) ->
   pstate cs2 = (State rs2 m2) ->
   pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex ->
@@ -775,8 +716,8 @@ Theorem step_simu_control:
       exec_body lk tge tbdy2 rs2 m2 = Next rs3 m3
   /\  exec_exit tge fn (Ptrofs.repr (size tbb)) rs3 m3 tex t rs4 m4
   /\  match_states S'' (State rs4 m4)).
-Proof. Admitted. (*
-  intros until cs2. intros Hbody Hbuiltin FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP.
+Proof.
+  intros until cs2. intros Hbody FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP.
   inv ESTEP.
   - inv MCS. inv MAS. simpl in *.
     inv Hpstate.
@@ -873,8 +814,37 @@ Proof. Admitted. (*
           - eauto with asmgen. }
         { rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H11. auto. }
     + (* MBbuiltin (contradiction) *)
-      assert (MB.exit bb' <> Some (MBbuiltin e l b)) by (apply Hbuiltin).
-      rewrite <- H in H1. contradict H1; auto.
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      
+      assert (f0 = f) by congruence. subst f0.
+      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
+        eapply transf_function_no_overflow; eauto.
+        generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
+        remember (Ptrofs.add _ _) as ofs'.
+  assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
+          econstructor; eauto.
+ (*        exploit return_address_offset_correct; eauto. intros; subst ra.
+        repeat eexists.
+        econstructor; eauto. econstructor. *)
+      
+      monadInv TBC. monadInv TIC. inv H0.
+      
+      
+exploit builtin_args_match; eauto. intros [vargs' [P Q]].
+  exploit external_call_mem_extends; eauto.
+  intros [vres' [m2' [A [B [C D]]]]].
+  
+  
+  repeat eexists. econstructor. erewrite <- sp_val by eauto.
+  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto.
+  econstructor; eauto.
+  unfold incrPC. rewrite Pregmap.gss.
+  rewrite set_res_other. rewrite undef_regs_other_2. unfold Val.offset_ptr. rewrite PCeq.
+  eauto. rewrite preg_notin_charact. intros. auto with asmgen.
+  auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto.
+  eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
+  intros. discriminate.
     + (* MBgoto *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
       inv TBC. inv TIC. inv H0.
@@ -903,71 +873,46 @@ Proof. Admitted. (*
         congruence.
     + (* MBcond *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
-      inv TBC. inv TIC. inv H0.
+      inv TBC. inv TIC. inv H0. monadInv H1. monadInv EQ.
 
       * (* MBcond true *)
         assert (f0 = f) by congruence. subst f0.
         exploit eval_condition_lessdef.
           eapply preg_vals; eauto.
           all: eauto.
-        intros EC. monadInv H1.
-        unfold transl_cond_branch in EQ. ArgsInv.
-        { unfold transl_cond_branch_default in EQ. monadInv EQ. unfold transl_cond in EQ0.
-          destruct c0; try discriminate. }
-        { destruct c0; ArgsInv;
-          try (unfold transl_cond_branch_default, transl_cond in EQ; try monadInv EQ; discriminate).
-          - destruct c0.
-            3:{ unfold transl_cond_branch_default, transl_cond in EQ. monadInv EQ. monadInv EQ0.
-            repeat eexists. destruct is_arith_imm32.
-            - simpl. eauto.
-            - destruct is_arith_imm32; simpl; eauto.
-            
-            discriminate.
-          destruct c0; ArgsInv. unfold transl_cond_branch_default in EQ; try monadInv EQ; try unfold transl_cond in EQ0;
-          try discriminate.
-        { destruct c0; try discriminate. }
-        
-        
-        { monadInv EQ. unfold transl_cond in EQ0. destruct c0; try discriminate. }
-        { apply IHl. discriminate.
-          { destruct l, c0; simpl in *; try congruence.
-        destruct c0; simpl. simpl in EQ. monadInv EQ.
-        
-        exploit (transl_cbranch_correct); eauto. intros (rsX & mX & rsY & mY & A & B & C).
-        
-        exists rsX. exists mX. exists rsY. exists mY. split. eauto. eauto.
-
-        assert (PCeq': rs2 PC = rs' PC). { admit. (* inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. *) }
+        intros EC.
+        exploit transl_cbranch_correct_true; eauto. intros (rs', H).
+        destruct H as [ES [ECFI]].
+        exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC).
+        assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. }
         rewrite PCeq' in PCeq.
         assert (f1 = f) by congruence. subst f1.
         exploit find_label_goto_label.
-          4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs')). unfold incrPC.
-          rewrite Pregmap.gss.
-          unfold Val.offset_ptr. rewrite PCeq. eauto.
+          4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs')).
+          unfold incrPC, Val.offset_ptr. rewrite PCeq. rewrite Pregmap.gss. eauto.
         intros (tc' & rs3 & GOTOL & TLPC & Hrs3).
         exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'.
         assert (tf = fn) by congruence. subst tf.
 
         repeat eexists.
           rewrite <- BTC. simpl. rewrite app_nil_r. eauto.
-          eapply (cfi_step tge fn (Ptrofs.repr (size tbb)) rs' m2 (Some x0) E0 _ _). rewrite <- BTC. simpl. econstructor. rewrite B. eauto.
+          rewrite <- BTC. simpl. econstructor. rewrite ECFI. eauto.
 
         econstructor; eauto.
           eapply agree_exten with rs2; eauto with asmgen.
-          { intros. destruct r; try destruct g; try discriminate.
-            all: rewrite Hrs3; try discriminate; unfold nextblock, incrPC; Simpl. }
+          { intros. rewrite Hrs3; unfold incrPC. Simpl. rewrite H. all: auto. apply PC_not_data_preg; auto. }
         intros. discriminate.
-
       * (* MBcond false *)
-        assert (f0 = f) by congruence. subst f0.
+        assert (f0 = f) by congruence. subst f0. monadInv H1. monadInv EQ.
         exploit eval_condition_lessdef.
           eapply preg_vals; eauto.
           all: eauto.
         intros EC.
 
-        exploit transl_cbranch_correct_false; eauto. intros (rs' & jmp & A & B & C).
+        exploit transl_cbranch_correct_false; eauto. intros (rs', H).
+        destruct H as [ES [ECFI]].
         exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC).
-        assert (PCeq': rs2 PC = rs' PC). { inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. }
+        assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. }
         rewrite PCeq' in PCeq.
         exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'.
         assert (tf = fn) by congruence. subst tf.
@@ -977,39 +922,38 @@ Proof. Admitted. (*
         generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
 
         repeat eexists.
-          rewrite H6. rewrite <- BTC. rewrite extract_basics_to_code. simpl. rewrite app_nil_r. eauto.
-          rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto.
+          rewrite <- BTC. simpl. rewrite app_nil_r. eauto.
+          rewrite <- BTC. simpl. econstructor. rewrite ECFI. eauto.
 
         econstructor; eauto.
-          unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.
+          unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.
           eapply agree_exten with rs2; eauto with asmgen.
-          { intros. destruct r; try destruct g; try discriminate.
-            all: rewrite <- C; try discriminate; unfold nextblock, incrPC; Simpl. }
+          { intros. unfold incrPC. Simpl. rewrite H. all: auto. }
         intros. discriminate.
     + (* MBjumptable *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
       inv TBC. inv TIC. inv H0.
 
       assert (f0 = f) by congruence. subst f0.
-      monadInv H1.
+      monadInv H1. monadInv EQ.
       generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.
       assert (f1 = f) by congruence. subst f1.
-      exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef).
-        unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.
+      exploit find_label_goto_label. 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs2) # X16 <- Vundef # X17 <- Vundef).
+        unfold incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. discriminate.
       exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.
 
       intros [tc' [rs' [A [B C]]]].
-      exploit ireg_val; eauto. rewrite H13. intros LD; inv LD.
+      exploit ireg_val; eauto. rewrite H11. intros LD; inv LD.
       
-      repeat eexists.
-        rewrite H6. simpl extract_basic. simpl. eauto.
-        rewrite H7. simpl extract_ctl. simpl. Simpl. rewrite <- H1. unfold Mach.label in H14. unfold label. rewrite H14. eapply A.
+      repeat eexists. econstructor. simpl. Simpl. 2: { eapply ireg_of_not_X16''; eauto. }
+        unfold incrPC. rewrite Pregmap.gso; try discriminate. rewrite <- H1.
+        simpl. unfold Mach.label in H12. unfold label. rewrite H12. eapply A.
       econstructor; eauto.
         eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen.
-        { assert (destroyed_by_jumptable = R62 :: R63 :: nil) by auto. rewrite H2 in H0. simpl in H0. inv H0.
-          destruct (preg_eq r' GPR63). subst. contradiction.
-          destruct (preg_eq r' GPR62). subst. contradiction.
-          destruct r'; Simpl. }
+        { unfold incrPC. repeat Simpl; auto. assert (destroyed_by_jumptable = R17 :: nil) by auto.
+          rewrite H2 in H0. simpl in H0. destruct r'; try discriminate.
+          destruct d; try discriminate. destruct i; try discriminate.
+          destruct r; try discriminate. }
         discriminate.
     + (* MBreturn *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
@@ -1021,33 +965,33 @@ Proof. Admitted. (*
       exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
       exploit exec_straight_body; eauto.
         simpl. eauto.
-      intros EXEB.
+      intros EXEB. destruct EXEB as [l [MKEPI EXEB]].
       assert (f1 = f) by congruence. subst f1.
       
       repeat eexists.
-        rewrite H6. simpl extract_basic. eauto.
-        rewrite H7. simpl extract_ctl. simpl. reflexivity.
+        rewrite app_nil_r in MKEPI. rewrite <- MKEPI in EXEB. eauto.
+        econstructor. simpl. reflexivity.
       econstructor; eauto.
-        unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen.
+        unfold incrPC. repeat apply agree_set_other; auto with asmgen.
 
   - inv MCS. inv MAS. simpl in *. subst. inv Hpstate.
     destruct bb' as [hd' bdy' ex']; simpl in *. subst.
-    monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6.
+    monadInv TBC. monadInv TIC. simpl in *.
     simpl. repeat eexists.
-    econstructor. 4: instantiate (3 := false). all:eauto.
-      unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq.
+    econstructor. econstructor. 4: instantiate (3 := false). all:eauto.
+      unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq.
       assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
         eapply transf_function_no_overflow; eauto.
       assert (f = f0) by congruence. subst f0. econstructor; eauto.
       generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. eauto.
-    eapply agree_exten; eauto. intros. Simpl.
+    eapply agree_exten; eauto. intros. unfold incrPC; Simpl; auto.
     discriminate.
-Qed.*)
+Qed.
 
 (* Handling the individual instructions of theorem (B) in the above diagram. A bit less cumbersome, but still tough *)
 Theorem step_simu_basic:
   forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy,
-  MB.header bb = nil -> MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
+  MB.header bb = nil -> MB.body bb = bi::(bdy) ->
   bb' = {| MB.header := nil; MB.body := bdy; MB.exit := MB.exit bb |} ->
   basic_step ge s fb sp ms m bi ms' m' ->
   pstate cs1 = (State rs1 m1) -> pbody1 cs1 = tbdy ->
@@ -1059,7 +1003,7 @@ Theorem step_simu_basic:
     /\ exec_body lk tge l rs1 m1 = Next rs2 m2
     /\ match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2).
 Proof.
-  intros until bdy. intros Hheader Hbody Hnobuiltin (* Hnotempty *) Hbb' BSTEP Hpstate Hpbody1 MCS. inv MCS.
+  intros until bdy. intros Hheader Hbody (* Hnotempty *) Hbb' BSTEP Hpstate Hpbody1 MCS. inv MCS.
   simpl in *. inv Hpstate.
   rewrite Hbody in TBC. monadInv TBC.
   inv BSTEP.
@@ -1212,56 +1156,8 @@ Local Transparent destroyed_by_op.
     intro Hep. simpl in Hep. discriminate.
   - (* MBload notrap1 *)
     simpl in EQ0. unfold transl_load in EQ0. discriminate.
-    (*destruct addr; simpl in H; destruct chunk; monadInv EQ0.
-    all:
-    destruct args as [|h0 t0]; try discriminate;
-    destruct t0 as [|h1 t1]; try discriminate;
-    destruct t1 as [|h2 t2]; try discriminate.*)
-    
   - (* MBload notrap2 *)
     simpl in EQ0. unfold transl_load in EQ0. discriminate.
-    (*simpl in EQ0. rewrite Hheader in DXP.
-
-    assert (Op.eval_addressing tge sp addr (map ms args) = Some a).
-      rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
-    exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
-    intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-    exploit transl_load_correct; eauto.
-    intros [rs2 [P [Q R]]].
-    
-    destruct (Mem.loadv chunk m1 a') as [v' | ] eqn:Hload.
-    {
-    exploit transl_load_correct; eauto.
-    intros [rs2 [P [Q R]]].
-
-    eapply exec_straight_body in P.
-    destruct P as (l & ll & EXECB).
-    exists rs2, m1, l.
-    eexists. eexists. split. instantiate (1 := x). eauto.
-    repeat (split; auto).
-    eapply match_codestate_intro; eauto.
-
-    eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
-
-    simpl in *. discriminate.
-    }
-    {
-    exploit transl_load_correct_notrap2; eauto.
-    intros [rs2 [P [Q R]]].
-
-    eapply exec_straight_body in P.
-    destruct P as (l & ll & EXECB).
-    exists rs2, m1, l.
-    eexists. eexists. split. instantiate (1 := x). eauto.
-    repeat (split; auto).
-    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
-(*     assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
-    rewrite <- Hheadereq. *) subst.
-    eapply match_codestate_intro; eauto.
-
-    eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
-    simpl in *. discriminate.
-    }*)
   - (* MBstore *)
     simpl in EQ0. rewrite Hheader in DXP.
 
@@ -1337,7 +1233,6 @@ Qed.
 Theorem step_simu_body:
   forall bb s fb sp c ms m rs1 m1 ms' cs1 m',
   MB.header bb = nil ->
-  (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
   body_step ge s fb sp (MB.body bb) ms m ms' m' ->
   pstate cs1 = (State rs1 m1) ->
   match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
@@ -1348,17 +1243,17 @@ Theorem step_simu_body:
     /\ match_codestate fb (MB.State s fb sp ({| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |}::c) ms' m') cs2).
 Proof.
   intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy].
-  - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS.
+  - intros until m'. intros Hheader BSTEP Hpstate MCS.
     inv BSTEP.
     exists rs1, m1, cs1, (ep cs1).
     inv MCS. inv Hpstate. simpl in *. monadInv TBC. repeat (split; simpl; auto).
     econstructor; eauto.
-  - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS. inv BSTEP.
+  - intros until m'. intros Hheader BSTEP Hpstate MCS. inv BSTEP.
     rename ms' into ms''. rename m' into m''. rename rs' into ms'. rename m'0 into m'.
     exploit (step_simu_basic); eauto. simpl. eauto. simpl; auto. simpl; auto.
     intros (rs2 & m2 & l & cs2 & tbdy' & Hcs2 & Happ & EXEB & MCS').
     simpl in *.
-    exploit IHbdy. auto. 2: eapply H6. 3: eapply MCS'. all: eauto. subst; eauto. simpl; auto.
+    exploit IHbdy. auto. eapply H6. 2: eapply MCS'. all: eauto. subst; eauto. simpl; auto.
     intros (rs3 & m3 & cs3 & ep & Hcs3 & EXEB' & MCS'').
     exists rs3, m3, cs3, ep.
     repeat (split; simpl; auto). subst. simpl in *. auto.
@@ -1368,16 +1263,15 @@ Qed.
 (* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *)
 (* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *)
 Lemma step_simulation_bblock':
-  forall sf f sp bb bb' bb'' rs m rs' m' s'' c S1,
+  forall t sf f sp bb bb' bb'' rs m rs' m' s'' c S1,
   bb' = mb_remove_header bb ->
   body_step ge sf f sp (Machblock.body bb') rs m rs' m' ->
   bb'' = mb_remove_body bb' ->
-  (forall ef args res, MB.exit bb'' <> Some (MBbuiltin ef args res)) ->
-  exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') E0 s'' ->
+  exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') t s'' ->
   match_states (Machblock.State sf f sp (bb :: c) rs m) S1 ->
-  exists S2 : state, plus (step lk) tge S1 E0 S2 /\ match_states s'' S2.
+  exists S2 : state, plus (step lk) tge S1 t S2 /\ match_states s'' S2.
 Proof.
-  intros until S1. intros Hbb' BSTEP Hbb'' Hbuiltin ESTEP MS.
+  intros until S1. intros Hbb' BSTEP Hbb'' ESTEP MS.
   destruct (mbsize bb) eqn:SIZE.
   - apply mbsize_eqz in SIZE. destruct SIZE as (Hbody & Hexit).
     destruct bb as [hd bdy ex]; simpl in *; subst.
@@ -1386,9 +1280,7 @@ Proof.
     eexists. split.
     + eapply plus_one.
       exploit functions_translated; eauto. intros (tf0 & FIND' & TRANSF'). monadInv TRANSF'.
-      assert (x = tf). { unfold transf_function in H1. monadInv H1.
-      destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try congruence. }
-      subst x.
+      assert (x = tf) by congruence. subst x.
       eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto.
       unfold exec_bblock. simpl.
       eexists; eexists; split; eauto.
@@ -1412,7 +1304,7 @@ Proof.
 
     (* initial setting *)
     exploit match_state_codestate.
-      2: eapply Hnotempty.
+      eapply Hnotempty.
       all: eauto.
     intros (cs1 & fb & f0 & tbb & tc & ep & MCS & MAS & FIND & TLBS & Hbody & Hexit & Hcur & Hrem & Hpstate).
 
@@ -1428,8 +1320,8 @@ Proof.
     (* step_simu_body part *)
     assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. }
     exploit step_simu_body.
-      3: eapply BSTEP.
-      4: eapply MCS2.
+      2: eapply BSTEP.
+      3: eapply MCS2.
       all: eauto. rewrite Hpstate'. eauto.
     intros (rs2 & m2 & cs2 & ep' & Hcs2 & EXEB & MCS').
 
@@ -1439,8 +1331,8 @@ Proof.
     destruct H as (tf & FIND').
     inv EXEH. simpl in *.
     subst. exploit step_simu_control.
-      9: eapply MCS'. all: simpl.
-      10: eapply ESTEP.
+      8: eapply MCS'. all: simpl.
+      9: eapply ESTEP.
       all: simpl; eauto.
       { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto.
         erewrite exec_body_pc; eauto. }
@@ -1467,20 +1359,18 @@ Proof.
     assert (f1 = f0) by congruence. subst f0.
     rewrite PCeq in Hrs1pc. inv Hrs1pc.
     exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''.
-    inv FIND''. monadInv TRANS''. unfold transf_function in TRANSF0. monadInv TRANSF0.
-    destruct (zlt _ _) in EQ1; try discriminate. rewrite EQ in EQ0. inv EQ0. inv EQ1.
+    inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ.
     eapply find_bblock_tail; eauto.
 Qed.
 
 Theorem step_simulation_bblock:
-  forall sf f sp bb ms m ms' m' S2 c,
+  forall t sf f sp bb ms m ms' m' S2 c,
   body_step ge sf f sp (Machblock.body bb) ms m ms' m' ->
-  (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
-  exit_step return_address_offset ge (Machblock.exit bb) (Machblock.State sf f sp (bb :: c) ms' m') E0 S2 ->
+  exit_step return_address_offset ge (Machblock.exit bb) (Machblock.State sf f sp (bb :: c) ms' m') t S2 ->
   forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' ->
-  exists S2' : state, plus (step lk) tge S1' E0 S2' /\ match_states S2 S2'.
+  exists S2' : state, plus (step lk) tge S1' t S2' /\ match_states S2 S2'.
 Proof.
-  intros until c. intros BSTEP Hbuiltin ESTEP S1' MS.
+  intros until c. intros BSTEP ESTEP S1' MS.
   eapply step_simulation_bblock'; eauto.
   all: destruct bb as [hd bdy ex]; simpl in *; eauto.
   inv ESTEP.
@@ -1488,76 +1378,19 @@ Proof.
   - econstructor.
 Qed.
 
-(* Definition split (c: MB.code) :=
-  match c with
-  | nil => nil
-  | bb::c => {| MB.header := MB.header bb; MB.body := MB.body bb; MB.exit := None |}
-              :: {| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |} :: c
-  end.
-  
-Lemma cons_ok_eq3 {A: Type} :
-  forall (x:A) y z x' y' z',
-  x = x' -> y = y' -> z = z' ->
-  OK (x::y::z) = OK (x'::y'::z').
-Proof.
-  intros. subst. auto.
-Qed.
-
-Lemma transl_blocks_split_builtin:
-  forall bb c ep f ef args res,
-  MB.exit bb = Some (MBbuiltin ef args res) -> MB.body bb <> nil ->
-  transl_blocks f (split (bb::c)) ep = transl_blocks f (bb::c) ep.
-Proof.
-  intros until res. intros Hexit Hbody. simpl split.
-  unfold transl_blocks. fold transl_blocks. unfold transl_block.
-  simpl. remember (transl_basic_code _ _ _) as tbc. remember (transl_exit _ _) as tbi.
-  remember (transl_blocks _ _ _) as tlbs.
-  destruct tbc; destruct tbi; destruct tlbs.
-  - unfold cons_bblocks; try destruct p; try simpl; rewrite app_nil_r. 
-  destruct l; destruct o; destruct b; simpl. auto.
-  
-  auto.
-  all: unfold cons_bblocks; try destruct p; try simpl; auto.
-  - simpl. rewrite Hexit in Heqtbi. simpl in Heqtbi. monadInv Heqtbi. simpl.
-    unfold cons_bblocks. simpl. destruct l.
-    + exploit transl_basic_code_nonil; eauto. intro. destruct H.
-    + simpl. rewrite app_nil_r. simpl. apply cons_ok_eq3. all: try eapply bblock_equality. all: simpl; auto.
-Qed.
-
-Lemma transl_code_at_pc_split_builtin:
-  forall rs f f0 bb c ep tf tc ef args res,
-  MB.body bb <> nil -> MB.exit bb = Some (MBbuiltin ef args res) ->
-  transl_code_at_pc ge (rs PC) f f0 (bb :: c) ep tf tc ->
-  transl_code_at_pc ge (rs PC) f f0 (split (bb :: c)) ep tf tc.
-Proof.
-  intros until res. intros Hbody Hexit AT. inv AT.
-  econstructor; eauto. erewrite transl_blocks_split_builtin; eauto.
-Qed.
-
-
-Theorem match_states_split_builtin:
-  forall sf f sp bb c rs m ef args res S1,
-  MB.body bb <> nil -> MB.exit bb = Some (MBbuiltin ef args res) ->
+(* Theorem step_simulation_builtin:
+  forall t sf f sp bb bb' bb'' rs m rs' m' s'' c ef args res S1,
+  bb' = mb_remove_header bb ->
+  body_step ge sf f sp (Machblock.body bb') rs m rs' m' ->
+  bb'' = mb_remove_body bb' ->
+  MB.exit bb = Some (MBbuiltin ef args res) ->
+  exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') t s'' ->
   match_states (Machblock.State sf f sp (bb :: c) rs m) S1 ->
-  match_states (Machblock.State sf f sp (split (bb::c)) rs m) S1.
-Proof.
-  intros until S1. intros Hbody Hexit MS.
-  inv MS.
-  econstructor; eauto.
-  eapply transl_code_at_pc_split_builtin; eauto.
-Qed. *)
-
-Theorem step_simulation_builtin:
-  forall ef args res bb sf f sp c ms m t S2,
-  MB.body bb = nil -> MB.exit bb = Some (MBbuiltin ef args res) ->
-  exit_step return_address_offset ge (MB.exit bb) (Machblock.State sf f sp (bb :: c) ms m) t S2 ->
-  forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' ->
-  exists S2' : state, plus (step lk) tge S1' t S2' /\ match_states S2 S2'.
+  exists S2 : state, plus (step lk) tge S1 E0 S2 /\ match_states s'' S2.
 Proof.
-  intros until S2. intros Hbody Hexit ESTEP S1' MS.
+  intros until S1. intros Hbb' BSTEP Hbb'' Hexit ESTEP MS.
   inv MS. inv AT. monadInv H2. monadInv EQ.
-  rewrite Hbody in EQ. monadInv EQ.
-  rewrite Hexit in EQ0. monadInv EQ0.
+  rewrite Hexit in EQ0. monadInv EQ0. simpl in ESTEP.
   rewrite Hexit in ESTEP. inv ESTEP. inv H4.
 
   exploit functions_transl; eauto. intro FN.
@@ -1569,7 +1402,10 @@ Proof.
   simpl in H3.
   eapply exec_step_internal. eauto. eauto.
     eapply find_bblock_tail; eauto.
-    simpl. econstructor. eexists. simpl. split; eauto.
+    destruct (x3 @@ nil).
+    - eauto.
+    - eauto.
+    simpl. eauto. eexists. simpl. split; eauto.
     econstructor.
     erewrite <- sp_val by eauto.
     eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eauto.
@@ -1586,7 +1422,7 @@ Proof.
     apply agree_nextblock. eapply agree_set_res; auto.
     eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
     congruence.
-Qed.
+Qed. *)
 
 (* Measure to prove finite stuttering, see the other backends *)
 Definition measure (s: MB.state) : nat :=
@@ -1596,6 +1432,12 @@ Definition measure (s: MB.state) : nat :=
   | MB.Returnstate _ _ _ => 1%nat
   end.
 
+Lemma next_sep:
+  forall rs m rs' m', rs = rs' -> m = m' -> Next rs m = Next rs' m'.
+Proof.
+  congruence.
+Qed.
+
 (* The actual MB.step/AB.step simulation, using the above theorems, plus extra proofs
    for the internal and external function cases *)
 Theorem step_simulation:
@@ -1603,41 +1445,14 @@ Theorem step_simulation:
   forall S1' (MS: match_states S1 S1'),
   (exists S2', plus (step lk) tge S1' t S2' /\ match_states S2 S2')
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
-Proof. Admitted.
-(*  induction 1; intros.
+Proof.
+  induction 1; intros.
 
 - (* bblock *)
   left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0.
   all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; 
-            try (rewrite MBE; try discriminate); eauto).
-  + (* MBbuiltin *)
-    destruct (MB.body bb) eqn:MBB.
-    * inv H. eapply step_simulation_builtin; eauto. rewrite MBE. eauto.
-    * (* eapply match_states_split_builtin in MS; eauto.
-        2: rewrite MBB; discriminate. *)
-      (* simpl split in MS. *)
-      rewrite <- MBB in H.
-(*       remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb1. *)
-(*       assert (MB.body bb = MB.body bb1). { subst. simpl. auto. } *)
-(*       rewrite H1 in H. subst. *)
-      exploit step_simulation_bblock. eapply H.
-        discriminate.
-        simpl. constructor.
-        eauto.
-      intros (S2' & PLUS1 & MS').
-      rewrite MBE in MS'.
-      assert (exit_step return_address_offset ge (Some (MBbuiltin e l b)) 
-              (MB.State sf f sp ({| MB.header := nil; MB.body := nil; MB.exit := Some (MBbuiltin e l b) |}::c) 
-                rs' m') t s').
-      { inv H0. inv H3. econstructor. econstructor; eauto. }
-      exploit step_simulation_builtin.
-        4: eapply MS'.
-        all: simpl; eauto.
-      intros (S3' & PLUS'' & MS'').
-      exists S3'. split; eauto.
-      eapply plus_trans. eapply PLUS1. eapply PLUS''. eauto.
+            try (rewrite MBE; try discriminate); eauto). 
   + inversion H0. subst. eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto.
-
 - (* internal function *)
   inv MS.
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
@@ -1655,42 +1470,43 @@ Proof. Admitted.
   monadInv EQ0.
   set (tfbody := make_prologue f x0) in *.
   set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.
-  set (rs2 := rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef).
-  exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto.
-  intros (rs' & U' & V').
-  exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2').
+  set (rs2 := rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef).
+  exploit (storeptr_correct lk tge XSP (fn_retaddr_ofs f) RA nil m2' m3' rs2).
   { rewrite chunk_of_Tptr in P.
-    assert (rs' GPRA = rs0 RA). { apply V'. }
-    assert (rs' SP = rs2 SP). { apply V'; discriminate. }
-    rewrite H4. rewrite H3.
+    assert (rs0 X30 = rs2 RA) by auto.
+    rewrite <- H3.
     rewrite ATLR.
-    change (rs2 SP) with sp. eexact P. }
+    change (rs2 XSP) with sp. eexact P. }
+  1-2: discriminate.
   intros (rs3 & U & V).
   assert (EXEC_PROLOGUE: exists rs3',
-            exec_straight_blocks tge tf
+            exec_straight_blocks tge lk tf
               tf.(fn_blocks) rs0 m'
               x0 rs3' m3'
-          /\ forall r, r <> PC -> rs3' r = rs3 r).
+          /\ forall r, r <> PC -> r <> X16 -> rs3' r = rs3 r).
   { eexists. split.
     - change (fn_blocks tf) with tfbody; unfold tfbody.
-      econstructor; eauto. unfold exec_bblock. simpl exec_body.
-      rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F.
-      Simpl. unfold parexec_store_offset. rewrite Ptrofs.of_int64_to_int64. unfold eval_offset.
-      rewrite chunk_of_Tptr in P. Simpl. rewrite ATLR. unfold Mptr in P. assert (Archi.ptr64 = true) by auto. 2: auto. rewrite H3 in P. rewrite P.
-      simpl. apply next_sep; eauto. reflexivity.
-    - intros. destruct V' as (V'' & V'). destruct r.
-      + Simpl.
-        destruct (gpreg_eq g0 GPR16). { subst. Simpl. rewrite V; try discriminate. rewrite V''. subst rs2. Simpl. }
-        destruct (gpreg_eq g0 GPR32). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }
-        destruct (gpreg_eq g0 GPR12). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }
-        destruct (gpreg_eq g0 GPR17). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }
-        Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. { destruct g0; try discriminate. contradiction. }
-      + Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl.
-      + contradiction.
+      econstructor; eauto.
+      assert (Archi.ptr64 = true) as SF; auto.
+      + unfold exec_bblock. simpl exec_body.
+        rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F.
+        assert (Mptr = Mint64) by auto. rewrite H3 in F. simpl in F. rewrite F. simpl.
+        unfold exec_store_rs_a. repeat Simpl; try discriminate.
+        exists rs2. exists m3'. split.
+        * unfold eval_addressing. Simpl; try discriminate. rewrite Pregmap.gss.
+          rewrite chunk_of_Tptr in P. rewrite H3 in P.
+          unfold Val.addl. unfold Val.offset_ptr in P.
+          destruct sp; simpl; try discriminate. rewrite SF; simpl.
+          rewrite Ptrofs.of_int64_to_int64. unfold Mem.storev in P. rewrite ATLR.
+          rewrite P. simpl. apply next_sep; eauto. apply SF.
+        * econstructor.
+      + eauto.
+    - intros. unfold incrPC.
+      rewrite Pregmap.gso; auto. rewrite V; auto.
   } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
   exploit exec_straight_steps_2; eauto using functions_transl.
   simpl fn_blocks. simpl fn_blocks in g. omega. constructor.
-  intros (ofs' & X & Y).                    
+  intros (ofs' & X & Y).
   left; exists (State rs3' m3'); split.
   eapply exec_straight_steps_1; eauto.
   simpl fn_blocks. simpl fn_blocks in g. omega.
@@ -1703,22 +1519,15 @@ Proof. Admitted.
   apply agree_change_sp with (parent_sp s). 
   apply agree_undef_regs with rs0. auto.
 Local Transparent destroyed_at_function_entry.
-  simpl; intros; Simpl.
+  simpl; intros; Simpl. auto.
+  assert (r' <> X29). { contradict H3; rewrite H3; unfold data_preg; auto. } auto.
   unfold sp; congruence.
 
   intros.
-  assert (r <> RTMP). { contradict H3; rewrite H3; unfold data_preg; auto. }
-  rewrite Heqrs3'. Simpl. rewrite V. inversion V'. rewrite H6. auto.
-  assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. }
-  assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }
-  contradict H3; rewrite H3; unfold data_preg; auto.
-  contradict H3; rewrite H3; unfold data_preg; auto.
-  contradict H3; rewrite H3; unfold data_preg; auto.
-  contradict H3; rewrite H3; unfold data_preg; auto.
-  intros. rewrite Heqrs3'. rewrite V by auto with asmgen.
-  assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }
-  rewrite H4 by auto with asmgen. reflexivity. discriminate.
 
+  rewrite Heqrs3'. rewrite V. 2-5: try apply X16_not_data_preg; try apply PC_not_data_preg; auto.
+  auto.
+  intros. rewrite Heqrs3'; try discriminate. rewrite V by auto with asmgen. reflexivity.
 - (* external function *)
   inv MS.
   exploit functions_translated; eauto.
@@ -1742,7 +1551,7 @@ Local Transparent destroyed_at_function_entry.
   right. split. omega. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
-Qed.*)
+Qed.
 
 Lemma transf_initial_states:
   forall st1, MB.initial_state prog st1 ->
@@ -1785,1112 +1594,6 @@ Proof.
   - eexact transf_initial_states.
   - eexact transf_final_states.
   - exact step_simulation.
-Admitted.
-
-End PRESERVATION.
-
-
-(* ORIGINAL aarch64/Asmgenproof file that needs to be adapted
-
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*         Xavier Leroy, Collège de France and INRIA Paris             *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Correctness proof for AArch64 code generation. *)
-
-Require Import Coqlib Errors.
-Require Import Integers Floats AST Linking.
-Require Import Values Memory Events Globalenvs Smallstep.
-Require Import Op Locations Mach Conventions Asm.
-Require Import Asmgen Asmgenproof0 Asmgenproof1.
-
-Definition match_prog (p: Mach.program) (tp: Asm.program) :=
-  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
-
-Lemma transf_program_match:
-  forall p tp, transf_program p = OK tp -> match_prog p tp.
-Proof.
-  intros. eapply match_transform_partial_program; eauto.
-Qed.
-
-Section PRESERVATION.
-
-Variable prog: Mach.program.
-Variable tprog: Asm.program.
-Hypothesis TRANSF: match_prog prog tprog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-Lemma symbols_preserved:
-  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
-
-Lemma senv_preserved:
-  Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
-
-Lemma functions_translated:
-  forall b f,
-  Genv.find_funct_ptr ge b = Some f ->
-  exists tf,
-  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
-
-Lemma functions_transl:
-  forall fb f tf,
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  transf_function f = OK tf ->
-  Genv.find_funct_ptr tge fb = Some (Internal tf).
-Proof.
-  intros. exploit functions_translated; eauto. intros [tf' [A B]].
-  monadInv B. rewrite H0 in EQ; inv EQ; auto.
-Qed.
-
-(** * Properties of control flow *)
-
-Lemma transf_function_no_overflow:
-  forall f tf,
-  transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned.
-Proof.
-  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
-  omega.
-Qed.
-
-Lemma exec_straight_exec:
-  forall fb f c ep tf tc c' rs m rs' m',
-  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
-  exec_straight tge tf tc rs m c' rs' m' ->
-  plus step tge (State rs m) E0 (State rs' m').
-Proof.
-  intros. inv H.
-  eapply exec_straight_steps_1; eauto.
-  eapply transf_function_no_overflow; eauto.
-  eapply functions_transl; eauto.
-Qed.
-
-Lemma exec_straight_at:
-  forall fb f c ep tf tc c' ep' tc' rs m rs' m',
-  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
-  transl_code f c' ep' = OK tc' ->
-  exec_straight tge tf tc rs m tc' rs' m' ->
-  transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.
-Proof.
-  intros. inv H.
-  exploit exec_straight_steps_2; eauto.
-  eapply transf_function_no_overflow; eauto.
-  eapply functions_transl; eauto.
-  intros [ofs' [PC' CT']].
-  rewrite PC'. constructor; auto.
-Qed.
-
-(** The following lemmas show that the translation from Mach to Asm
-  preserves labels, in the sense that the following diagram commutes:
-<<
-                          translation
-        Mach code ------------------------ Asm instr sequence
-            |                                          |
-            | Mach.find_label lbl       find_label lbl |
-            |                                          |
-            v                                          v
-        Mach code tail ------------------- Asm instr seq tail
-                          translation
->>
-  The proof demands many boring lemmas showing that Asm constructor
-  functions do not introduce new labels.
-*)
-
-Section TRANSL_LABEL.
-
-Remark loadimm_z_label: forall sz rd l k, tail_nolabel k (loadimm_z sz rd l k).
-Proof. 
-  intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel.
-  induction l as [ | [n p] l]; simpl; TailNoLabel.
-Qed.
-
-Remark loadimm_n_label: forall sz rd l k, tail_nolabel k (loadimm_n sz rd l k).
-Proof. 
-  intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel.
-  induction l as [ | [n p] l]; simpl; TailNoLabel.
-Qed.
-
-Remark loadimm_label: forall sz rd n k, tail_nolabel k (loadimm sz rd n k).
-Proof.
-  unfold loadimm; intros. destruct Nat.leb; [apply loadimm_z_label|apply loadimm_n_label].
-Qed.
-Hint Resolve loadimm_label: labels.
-
-Remark loadimm32_label: forall r n k, tail_nolabel k (loadimm32 r n k).
-Proof.
-  unfold loadimm32; intros. destruct (is_logical_imm32 n); TailNoLabel.
-Qed.
-Hint Resolve loadimm32_label: labels.
-
-Remark loadimm64_label: forall r n k, tail_nolabel k (loadimm64 r n k).
-Proof.
-  unfold loadimm64; intros. destruct (is_logical_imm64 n); TailNoLabel.
-Qed.
-Hint Resolve loadimm64_label: labels.
-
-Remark addimm_aux: forall insn rd r1 n k,
-  (forall rd r1 n, nolabel (insn rd r1 n)) ->
-  tail_nolabel k (addimm_aux insn rd r1 n k).
-Proof.
-  unfold addimm_aux; intros. 
-  destruct Z.eqb. TailNoLabel. destruct Z.eqb; TailNoLabel.
-Qed.
-
-Remark addimm32_label: forall rd r1 n k, tail_nolabel k (addimm32 rd r1 n k).
-Proof.
-  unfold addimm32; intros. 
-  destruct Int.eq. apply addimm_aux; intros; red; auto.
-  destruct Int.eq. apply addimm_aux; intros; red; auto.
-  destruct Int.lt; eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-Hint Resolve addimm32_label: labels.
-
-Remark addimm64_label: forall rd r1 n k, tail_nolabel k (addimm64 rd r1 n k).
-Proof.
-  unfold addimm64; intros. 
-  destruct Int64.eq. apply addimm_aux; intros; red; auto.
-  destruct Int64.eq. apply addimm_aux; intros; red; auto.
-  destruct Int64.lt; eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-Hint Resolve addimm64_label: labels.
-
-Remark logicalimm32_label: forall insn1 insn2 rd r1 n k,
-  (forall rd r1 n, nolabel (insn1 rd r1 n)) ->
-  (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) ->
-  tail_nolabel k (logicalimm32 insn1 insn2 rd r1 n k).
-Proof.
-  unfold logicalimm32; intros.
-  destruct (is_logical_imm32 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-
-Remark logicalimm64_label: forall insn1 insn2 rd r1 n k,
-  (forall rd r1 n, nolabel (insn1 rd r1 n)) ->
-  (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) ->
-  tail_nolabel k (logicalimm64 insn1 insn2 rd r1 n k).
-Proof.
-  unfold logicalimm64; intros.
-  destruct (is_logical_imm64 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-
-Remark move_extended_label: forall rd r1 ex a k, tail_nolabel k (move_extended rd r1 ex a k).
-Proof.
-  unfold move_extended, move_extended_base; intros. destruct Int.eq, ex; TailNoLabel.
-Qed.
-Hint Resolve move_extended_label: labels.
-
-Remark arith_extended_label: forall insnX insnS rd r1 r2 ex a k,
-  (forall rd r1 r2 x, nolabel (insnX rd r1 r2 x)) ->
-  (forall rd r1 r2 s, nolabel (insnS rd r1 r2 s)) ->
-  tail_nolabel k (arith_extended insnX insnS rd r1 r2 ex a k).
-Proof.
-  unfold arith_extended; intros. destruct Int.ltu.
-  TailNoLabel.
-  destruct ex; simpl; TailNoLabel.
-Qed.
-
-Remark loadsymbol_label: forall r id ofs k, tail_nolabel k (loadsymbol r id ofs k).
-Proof.
-  intros; unfold loadsymbol.
-  destruct (Archi.pic_code tt); TailNoLabel. destruct Ptrofs.eq; TailNoLabel.
-Qed. 
-Hint Resolve loadsymbol_label: labels.
-
-Remark transl_cond_label: forall cond args k c,
-  transl_cond cond args k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_cond; intros; destruct cond; TailNoLabel.
-- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-
-Remark transl_cond_branch_default_label: forall cond args lbl k c,
-  transl_cond_branch_default cond args lbl k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_cond_branch_default; intros. 
-  eapply tail_nolabel_trans; [eapply transl_cond_label;eauto|TailNoLabel].
-Qed.
-Hint Resolve transl_cond_branch_default_label: labels.
-
-Remark transl_cond_branch_label: forall cond args lbl k c,
-  transl_cond_branch cond args lbl k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_cond_branch; intros; destruct args; TailNoLabel; destruct cond; TailNoLabel.
-- destruct c0; TailNoLabel.
-- destruct c0; TailNoLabel.
-- destruct (Int.is_power2 n); TailNoLabel.
-- destruct (Int.is_power2 n); TailNoLabel.
-- destruct c0; TailNoLabel.
-- destruct c0; TailNoLabel.
-- destruct (Int64.is_power2' n); TailNoLabel.
-- destruct (Int64.is_power2' n); TailNoLabel.
-Qed.
-
-Remark transl_op_label:
-  forall op args r k c,
-  transl_op op args r k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_op; intros; destruct op; TailNoLabel.
-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-- destruct (Float.eq_dec n Float.zero); TailNoLabel.
-- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
-- apply logicalimm32_label; unfold nolabel; auto.
-- apply logicalimm32_label; unfold nolabel; auto.
-- apply logicalimm32_label; unfold nolabel; auto.
-- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel.
-- apply arith_extended_label; unfold nolabel; auto.
-- apply arith_extended_label; unfold nolabel; auto.
-- apply logicalimm64_label; unfold nolabel; auto.
-- apply logicalimm64_label; unfold nolabel; auto.
-- apply logicalimm64_label; unfold nolabel; auto.
-- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel.
-- eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel.
-- destruct (preg_of r); try discriminate; TailNoLabel;
-  (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]).
-Qed.
-
-Remark transl_addressing_label:
-  forall sz addr args insn k c,
-  transl_addressing sz addr args insn k = OK c ->
-  (forall ad, nolabel (insn ad)) ->
-  tail_nolabel k c.
-Proof.
-  unfold transl_addressing; intros; destruct addr; TailNoLabel;
-  eapply tail_nolabel_trans; TailNoLabel.
-  eapply tail_nolabel_trans. apply arith_extended_label; unfold nolabel; auto. TailNoLabel.
-Qed.
-
-Remark transl_load_label:
-  forall trap chunk addr args dst k c,
-  transl_load trap chunk addr args dst k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_load; intros; destruct trap; try discriminate; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto.
-Qed.
-
-Remark transl_store_label:
-  forall chunk addr args src k c,
-  transl_store chunk addr args src k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_store; intros; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto.
-Qed.
-
-Remark indexed_memory_access_label:
-  forall insn sz base ofs k,
-  (forall ad, nolabel (insn ad)) ->
-  tail_nolabel k (indexed_memory_access insn sz base ofs k).
-Proof.
-  unfold indexed_memory_access; intros. destruct offset_representable.
-  TailNoLabel.
-  eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-
-Remark loadind_label:
-  forall base ofs ty dst k c,
-  loadind base ofs ty dst k = OK c -> tail_nolabel k c.
-Proof.
-  unfold loadind; intros.
-  destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I.
-Qed.
-
-Remark storeind_label:
-  forall src base ofs ty k c,
-  storeind src base ofs ty k = OK c -> tail_nolabel k c.
-Proof.
-  unfold storeind; intros.
-  destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I.
-Qed.
-
-Remark loadptr_label:
-  forall base ofs dst k, tail_nolabel k (loadptr base ofs dst k).
-Proof.
-  intros. apply indexed_memory_access_label. unfold nolabel; auto.
-Qed.
-
-Remark storeptr_label:
-  forall src base ofs k, tail_nolabel k (storeptr src base ofs k).
-Proof.
-  intros. apply indexed_memory_access_label. unfold nolabel; auto.
-Qed.
-
-Remark make_epilogue_label:
-  forall f k, tail_nolabel k (make_epilogue f k).
-Proof.
-  unfold make_epilogue; intros.
-  (* FIXME destruct is_leaf_function.
-  { TailNoLabel. } *)
-  eapply tail_nolabel_trans.
-  apply loadptr_label.
-  TailNoLabel.
-Qed.
-
-Lemma transl_instr_label:
-  forall f i ep k c,
-  transl_instr f i ep k = OK c ->
-  match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end.
-Proof.
-  unfold transl_instr; intros; destruct i; TailNoLabel.
-- eapply loadind_label; eauto.
-- eapply storeind_label; eauto.
-- destruct ep. eapply loadind_label; eauto.
-  eapply tail_nolabel_trans. apply loadptr_label. eapply loadind_label; eauto. 
-- eapply transl_op_label; eauto.
-- eapply transl_load_label; eauto. 
-- eapply transl_store_label; eauto.
-- destruct s0; monadInv H; TailNoLabel.
-- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).
-- eapply transl_cond_branch_label; eauto.
-- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
-Qed.
-
-Lemma transl_instr_label':
-  forall lbl f i ep k c,
-  transl_instr f i ep k = OK c ->
-  find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.
-Proof.
-  intros. exploit transl_instr_label; eauto.
-  destruct i; try (intros [A B]; apply B).
-  intros. subst c. simpl. auto.
-Qed.
-
-Lemma transl_code_label:
-  forall lbl f c ep tc,
-  transl_code f c ep = OK tc ->
-  match Mach.find_label lbl c with
-  | None => find_label lbl tc = None
-  | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc'
-  end.
-Proof.
-  induction c; simpl; intros.
-  inv H. auto.
-  monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0).
-  generalize (Mach.is_label_correct lbl a).
-  destruct (Mach.is_label lbl a); intros.
-  subst a. simpl in EQ. exists x; auto.
-  eapply IHc; eauto.
-Qed.
-
-Lemma transl_find_label:
-  forall lbl f tf,
-  transf_function f = OK tf ->
-  match Mach.find_label lbl f.(Mach.fn_code) with
-  | None => find_label lbl tf.(fn_code) = None
-  | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc
-  end.
-Proof.
-  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
-  monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. 
-  simpl. destruct (storeptr_label X30 XSP (fn_retaddr_ofs f) x) as [A B]; rewrite B. 
-  eapply transl_code_label; eauto.
-Qed.
-
-End TRANSL_LABEL.
-
-(** A valid branch in a piece of Mach code translates to a valid ``go to''
-  transition in the generated Asm code. *)
-
-Lemma find_label_goto_label:
-  forall f tf lbl rs m c' b ofs,
-  Genv.find_funct_ptr ge b = Some (Internal f) ->
-  transf_function f = OK tf ->
-  rs PC = Vptr b ofs ->
-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
-  exists tc', exists rs',
-     goto_label tf lbl rs m = Next rs' m
-  /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc'
-  /\ forall r, r <> PC -> rs'#r = rs#r.
-Proof.
-  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2.
-  intros [tc [A B]].
-  exploit label_pos_code_tail; eauto. instantiate (1 := 0).
-  intros [pos' [P [Q R]]].
-  exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
-  split. unfold goto_label. rewrite P. rewrite H1. auto.
-  split. rewrite Pregmap.gss. constructor; auto.
-  rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
-  auto. omega.
-  generalize (transf_function_no_overflow _ _ H0). omega.
-  intros. apply Pregmap.gso; auto.
-Qed.
-
-(** Existence of return addresses *)
-
-Lemma return_address_exists:
-  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
-  exists ra, return_address_offset f c ra.
-Proof.
-  intros. eapply Asmgenproof0.return_address_exists; eauto.
-- intros. exploit transl_instr_label; eauto.
-  destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
-- intros. monadInv H0.
-  destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ.
-  rewrite transl_code'_transl_code in EQ0.
-  exists x; exists true; split; auto. unfold fn_code.
-  constructor. apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) x).
-- exact transf_function_no_overflow.
-Qed.
-
-(** * Proof of semantic preservation *)
-
-(** Semantic preservation is proved using simulation diagrams
-  of the following form.
-<<
-           st1 --------------- st2
-            |                   |
-           t|                  *|t
-            |                   |
-            v                   v
-           st1'--------------- st2'
->>
-  The invariant is the [match_states] predicate below, which includes:
-- The Asm code pointed by the PC register is the translation of
-  the current Mach code sequence.
-- Mach register values and Asm register values agree.
-*)
-
-Inductive match_states: Mach.state -> Asm.state -> Prop :=
-  | match_states_intro:
-      forall s fb sp c ep ms m m' rs f tf tc
-        (STACKS: match_stack ge s)
-        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
-        (MEXT: Mem.extends m m')
-        (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
-        (AG: agree ms sp rs)
-        (DXP: ep = true -> rs#X29 = parent_sp s)
-        (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s),
-      match_states (Mach.State s fb sp c ms m)
-                   (Asm.State rs m')
-  | match_states_call:
-      forall s fb ms m m' rs
-        (STACKS: match_stack ge s)
-        (MEXT: Mem.extends m m')
-        (AG: agree ms (parent_sp s) rs)
-        (ATPC: rs PC = Vptr fb Ptrofs.zero)
-        (ATLR: rs RA = parent_ra s),
-      match_states (Mach.Callstate s fb ms m)
-                   (Asm.State rs m')
-  | match_states_return:
-      forall s ms m m' rs
-        (STACKS: match_stack ge s)
-        (MEXT: Mem.extends m m')
-        (AG: agree ms (parent_sp s) rs)
-        (ATPC: rs PC = parent_ra s),
-      match_states (Mach.Returnstate s ms m)
-                   (Asm.State rs m').
-
-Lemma exec_straight_steps:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2,
-  match_stack ge s ->
-  Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
-  (forall k c (TR: transl_instr f i ep k = OK c),
-   exists rs2,
-       exec_straight tge tf c rs1 m1' k rs2 m2'
-    /\ agree ms2 sp rs2
-    /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s)
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
-  exists st',
-  plus step tge (State rs1 m1') E0 st' /\
-  match_states (Mach.State s fb sp c ms2 m2) st'.
-Proof.
-  intros. inversion H2. subst. monadInv H7.
-  exploit H3; eauto. intros [rs2 [A [B [C D]]]].
-  exists (State rs2 m2'); split.
-  - eapply exec_straight_exec; eauto.
-  - econstructor; eauto. eapply exec_straight_at; eauto.
-Qed.
-
-Lemma exec_straight_steps_goto:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
-  match_stack ge s ->
-  Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
-  it1_is_parent ep i = false ->
-  (forall k c (TR: transl_instr f i ep k = OK c),
-   exists jmp, exists k', exists rs2,
-       exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
-    /\ agree ms2 sp rs2
-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
-  exists st',
-  plus step tge (State rs1 m1') E0 st' /\
-  match_states (Mach.State s fb sp c' ms2 m2) st'.
-Proof.
-  intros. inversion H3. subst. monadInv H9.
-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
-  generalize (functions_transl _ _ _ H7 H8); intro FN.
-  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
-  exploit exec_straight_steps_2; eauto.
-  intros [ofs' [PC2 CT2]].
-  exploit find_label_goto_label; eauto.
-  intros [tc' [rs3 [GOTO [AT' OTH]]]].
-  exists (State rs3 m2'); split.
-  eapply plus_right'.
-  eapply exec_straight_steps_1; eauto.
-  econstructor; eauto.
-  eapply find_instr_tail. eauto.
-  rewrite C. eexact GOTO.
-  traceEq.
-  econstructor; eauto.
-  apply agree_exten with rs2; auto with asmgen.
-  congruence.
-  rewrite OTH by congruence; auto.
-Qed.
-
-Lemma exec_straight_opt_steps_goto:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
-  match_stack ge s ->
-  Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
-  it1_is_parent ep i = false ->
-  (forall k c (TR: transl_instr f i ep k = OK c),
-   exists jmp, exists k', exists rs2,
-       exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2'
-    /\ agree ms2 sp rs2
-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
-  exists st',
-  plus step tge (State rs1 m1') E0 st' /\
-  match_states (Mach.State s fb sp c' ms2 m2) st'.
-Proof.
-  intros. inversion H3. subst. monadInv H9.
-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
-  generalize (functions_transl _ _ _ H7 H8); intro FN.
-  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
-  inv A.
-- exploit find_label_goto_label; eauto.
-  intros [tc' [rs3 [GOTO [AT' OTH]]]].
-  exists (State rs3 m2'); split.
-  apply plus_one. econstructor; eauto.
-  eapply find_instr_tail. eauto.
-  rewrite C. eexact GOTO.
-  econstructor; eauto.
-  apply agree_exten with rs2; auto with asmgen.
-  congruence.
-  rewrite OTH by congruence; auto.
-- exploit exec_straight_steps_2; eauto.
-  intros [ofs' [PC2 CT2]].
-  exploit find_label_goto_label; eauto.
-  intros [tc' [rs3 [GOTO [AT' OTH]]]].
-  exists (State rs3 m2'); split.
-  eapply plus_right'.
-  eapply exec_straight_steps_1; eauto.
-  econstructor; eauto.
-  eapply find_instr_tail. eauto.
-  rewrite C. eexact GOTO.
-  traceEq.
-  econstructor; eauto.
-  apply agree_exten with rs2; auto with asmgen.
-  congruence.
-  rewrite OTH by congruence; auto.
-Qed.
-
-(** We need to show that, in the simulation diagram, we cannot
-  take infinitely many Mach transitions that correspond to zero
-  transitions on the Asm side.  Actually, all Mach transitions
-  correspond to at least one Asm transition, except the
-  transition from [Machsem.Returnstate] to [Machsem.State].
-  So, the following integer measure will suffice to rule out
-  the unwanted behaviour. *)
-
-Definition measure (s: Mach.state) : nat :=
-  match s with
-  | Mach.State _ _ _ _ _ _ => 0%nat
-  | Mach.Callstate _ _ _ _ => 0%nat
-  | Mach.Returnstate _ _ _ => 1%nat
-  end.
-
-Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r.
-Proof.
-  intros. change (IR X29) with (preg_of R29). red; intros.
-  exploit preg_of_injective; eauto. intros; subst r; discriminate.
-Qed.
-
-Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP.
-Proof.
-  intros. eapply sp_val; eauto. 
-Qed. 
-
-(** This is the simulation diagram.  We prove it by case analysis on the Mach transition. *)
-
-Theorem step_simulation:
-  forall S1 t S2, Mach.step return_address_offset ge S1 t S2 ->
-  forall S1' (MS: match_states S1 S1')  (WF: wf_state ge S1),
-  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
-  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
-Proof.
-  induction 1; intros; inv MS.
-
-- (* Mlabel *)
-  left; eapply exec_straight_steps; eauto; intros.
-  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. { apply agree_nextinstr; auto. }
-  split. { simpl; congruence. }
-  rewrite nextinstr_inv by congruence; assumption.
-
-- (* Mgetstack *)
-  unfold load_stack in H.
-  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
-  rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
-  exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]].
-  exists rs'; split. eauto.
-  split. { eapply agree_set_mreg; eauto with asmgen. congruence. }
-  split. { simpl; congruence. }
-  rewrite S. assumption.
-
-- (* Msetstack *)
-  unfold store_stack in H.
-  assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
-  exploit Mem.storev_extends; eauto. intros [m2' [A B]].
-  left; eapply exec_straight_steps; eauto.
-  rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
-  exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
-  exists rs'; split. eauto.
-  split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; intros.
-  split. rewrite Q; auto with asmgen.
-  rewrite R. assumption.
-
-- (* Mgetparam *)
-  assert (f0 = f) by congruence; subst f0.
-  unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H0. auto.
-  intros [parent' [A B]]. rewrite (sp_val' _ _ _ AG) in A.
-  exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto.
-  intros [v' [C D]].
-Opaque loadind.
-  left; eapply exec_straight_steps; eauto; intros. monadInv TR. 
-  destruct ep.
-(* X30 contains parent *)
-  exploit loadind_correct. eexact EQ.
-  instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence.
-  intros [rs1 [P [Q [R S]]]].
-  exists rs1; split. eauto.
-  split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
-  simpl; split; intros.
-  { rewrite R; auto with asmgen.
-    apply preg_of_not_X29; auto.
-  }
-  { rewrite S; auto. }
-    
-(* X30 does not contain parent *)
-  exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]].
-  exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence.
-  intros [rs2 [S [T [U V]]]].
-  exists rs2; split. eapply exec_straight_trans; eauto.
-  split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
-  instantiate (1 := rs1#X29 <- (rs2#X29)). intros.
-  rewrite Pregmap.gso; auto with asmgen.
-  congruence.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
-  split; simpl; intros. rewrite U; auto with asmgen.
-  apply preg_of_not_X29; auto.
-  rewrite V. rewrite R by congruence. auto.
-  
-- (* Mop *)
-  assert (eval_operation tge sp op (map rs args) m = Some v).
-  { rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. }
-  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
-  intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
-  exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]].
-  exists rs2; split. eauto. split.
-  apply agree_set_undef_mreg with rs0; auto. 
-  apply Val.lessdef_trans with v'; auto.
-  split; simpl; intros. InvBooleans. 
-  rewrite R; auto. apply preg_of_not_X29; auto.
-Local Transparent destroyed_by_op.
-  destruct op; try exact I; simpl; congruence.
-  rewrite S.
-  auto.
-- (* Mload *)
-  destruct trap.
-  {
-  assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
-  { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
-  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
-  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
-  exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]].
-  exists rs2; split. eauto.
-  split. eapply agree_set_undef_mreg; eauto. congruence.
-  split. simpl; congruence.
-  rewrite S. assumption.
-  }
-  
-  (* Mload notrap1 *)
-  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
-
-- (* Mload notrap *)
-  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
-
-- (* Mload notrap *)
-  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
-
-- (* Mstore *)
-  assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
-  { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
-  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
-  exploit Mem.storev_extends; eauto. intros [m2' [C D]].
-  left; eapply exec_straight_steps; eauto.
-  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]].
-  exists rs2; split. eauto.
-  split. eapply agree_undef_regs; eauto with asmgen.
-  split. simpl; congruence.
-  rewrite R. assumption.
-
-- (* Mcall *)
-  assert (f0 = f) by congruence.  subst f0.
-  inv AT.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-  { eapply transf_function_no_overflow; eauto. }
-  destruct ros as [rf|fid]; simpl in H; monadInv H5.
-+ (* Indirect call *)
-  assert (rs rf = Vptr f' Ptrofs.zero).
-  { destruct (rs rf); try discriminate.
-    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
-  assert (rs0 x0 = Vptr f' Ptrofs.zero).
-  { exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. }
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
-  {  econstructor; eauto. }
-  exploit return_address_offset_correct; eauto. intros; subst ra.
-  left; econstructor; split.
-  apply plus_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
-  simpl. eauto.
-  econstructor; eauto.
-  econstructor; eauto.
-  eapply agree_sp_def; eauto.
-  simpl. eapply agree_exten; eauto. intros. Simpl.
-  Simpl. rewrite <- H2. auto.
-+ (* Direct call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
-    econstructor; eauto.
-  exploit return_address_offset_correct; eauto. intros; subst ra.
-  left; econstructor; split.
-  apply plus_one. eapply exec_step_internal. eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
-  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
-  econstructor; eauto.
-  econstructor; eauto.
-  eapply agree_sp_def; eauto.
-  simpl. eapply agree_exten; eauto. intros. Simpl.
-  Simpl. rewrite <- H2. auto.
-
-- (* Mtailcall *)
-  assert (f0 = f) by congruence.  subst f0.
-  inversion AT; subst.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-  { eapply transf_function_no_overflow; eauto. }
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]].
-  destruct ros as [rf|fid]; simpl in H; monadInv H7.
-+ (* Indirect call *)
-  assert (rs rf = Vptr f' Ptrofs.zero).
-  { destruct (rs rf); try discriminate.
-    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
-  assert (rs0 x0 = Vptr f' Ptrofs.zero).
-  { exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. }
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-  Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. 
-+ (* Direct call *)
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-  Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto.
-
-- (* Mbuiltin *)
-  inv AT. monadInv H4.
-  exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H3); intro NOOV.
-  exploit builtin_args_match; eauto. intros [vargs' [P Q]].
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2' [A [B [C D]]]]].
-  left. econstructor; split. apply plus_one.
-  eapply exec_step_builtin. eauto. eauto.
-  eapply find_instr_tail; eauto.
-  erewrite <- sp_val by eauto.
-  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  eauto.
-  econstructor; eauto.
-  instantiate (2 := tf); instantiate (1 := x).
-  unfold nextinstr. rewrite Pregmap.gss.
-  rewrite set_res_other. rewrite undef_regs_other_2.
-  rewrite <- H1. simpl. econstructor; eauto.
-  eapply code_tail_next_int; eauto.
-  rewrite preg_notin_charact. intros. auto with asmgen.
-  auto with asmgen.
-  apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
-  congruence.
-
-  Simpl.
-  rewrite set_res_other by trivial.
-  rewrite undef_regs_other.
-  assumption.
-  intro.
-  rewrite in_map_iff.
-  intros (x0 & PREG & IN).
-  subst r'.
-  intro.
-  apply (preg_of_not_RA x0).
-  congruence.
-  
-- (* Mgoto *)
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H4.
-  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
-  left; exists (State rs' m'); split.
-  apply plus_one. econstructor; eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail; eauto.
-  simpl; eauto.
-  econstructor; eauto.
-  eapply agree_exten; eauto with asmgen.
-  congruence.
-
-  rewrite INV by congruence.
-  assumption.
-  
-- (* Mcond true *)
-  assert (f0 = f) by congruence. subst f0.
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_opt_steps_goto; eauto.
-  intros. simpl in TR.
-  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
-  exists jmp; exists k; exists rs'.
-  split. eexact A. 
-  split. apply agree_exten with rs0; auto with asmgen.
-  split.
-  exact B.
-  rewrite D. exact LEAF.
-
-- (* Mcond false *)
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
-  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
-  econstructor; split.
-  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto.
-  split. apply agree_exten with rs0; auto. intros. Simpl.
-  split.
-  simpl; congruence.
-  Simpl. rewrite D.
-  exact LEAF.
-
-- (* Mjumptable *)
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H6.
-  exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H5); intro NOOV.
-  exploit find_label_goto_label. eauto. eauto.
-  instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef).
-  Simpl. eauto.
-  eauto.
-  intros [tc' [rs' [A [B C]]]].
-  exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
-  left; econstructor; split.
-  apply plus_one. econstructor; eauto.
-  eapply find_instr_tail; eauto.
-  simpl. Simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
-  econstructor; eauto.
-  eapply agree_undef_regs; eauto.
-  simpl. intros. rewrite C; auto with asmgen. Simpl.
-  congruence.
-
-  rewrite C by congruence.
-  repeat rewrite Pregmap.gso by congruence.
-  assumption.
-  
-- (* Mreturn *)
-  assert (f0 = f) by congruence. subst f0.
-  inversion AT; subst. simpl in H6; monadInv H6.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-    eapply transf_function_no_overflow; eauto.
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-
-- (* internal function *)
-
-  exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
-  generalize EQ; intros EQ'. monadInv EQ'.
-  destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0.
-  unfold store_stack in *.
-  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
-  intros [m1' [C D]].
-  exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto.
-  intros [m2' [F G]].
-  simpl chunk_of_type in F.
-  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
-  intros [m3' [P Q]].
-  change (chunk_of_type Tptr) with Mint64 in *.
-  (* Execution of function prologue *)
-  monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
-  set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::
-                 storeptr RA XSP (fn_retaddr_ofs f) x0) in *.
-  set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
-  set (rs2 := nextinstr (rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef)).
-  exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2).
-    simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. 
-    change (rs2 X2) with sp. eexact P. 
-    simpl; congruence. congruence.
-  intros (rs3 & U & V & W).
-  assert (EXEC_PROLOGUE:
-            exec_straight tge tf
-              tf.(fn_code) rs0 m'
-              x0 rs3 m3').
-  { change (fn_code tf) with tfbody; unfold tfbody.
-    apply exec_straight_step with rs2 m2'.
-    unfold exec_instr. rewrite C. fold sp.
-    rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity.
-    reflexivity. 
-    eexact U. }
-  exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
-  intros (ofs' & X & Y).                    
-  left; exists (State rs3 m3'); split.
-  eapply exec_straight_steps_1; eauto. omega. constructor.
-  econstructor; eauto.
-  rewrite X; econstructor; eauto. 
-  apply agree_exten with rs2; eauto with asmgen.
-  unfold rs2. 
-  apply agree_nextinstr. apply agree_set_other; auto with asmgen.
-  apply agree_change_sp with (parent_sp s). 
-  apply agree_undef_regs with rs0. auto.
-Local Transparent destroyed_at_function_entry. simpl.
-  simpl; intros; Simpl.
-  unfold sp; congruence.
-  intros. rewrite V by auto with asmgen. reflexivity.
-
-  rewrite W.
-  unfold rs2.
-  Simpl.
-  
-- (* external function *)
-  exploit functions_translated; eauto.
-  intros [tf [A B]]. simpl in B. inv B.
-  exploit extcall_arguments_match; eauto.
-  intros [args' [C D]].
-  exploit external_call_mem_extends; eauto.
-  intros [res' [m2' [P [Q [R S]]]]].
-  left; econstructor; split.
-  apply plus_one. eapply exec_step_external; eauto.
-  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  econstructor; eauto.
-  unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto.
-  apply agree_undef_caller_save_regs; auto. 
-
-- (* return *)
-  inv STACKS. simpl in *.
-  right. split. omega. split. auto.
-  rewrite <- ATPC in H5.
-  econstructor; eauto. congruence.
-  inv WF.
-  inv STACK.
-  inv H1.
-  congruence.
-Qed.
-
-Lemma transf_initial_states:
-  forall st1, Mach.initial_state prog st1 ->
-  exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2.
-Proof.
-  intros. inversion H. unfold ge0 in *.
-  econstructor; split.
-  econstructor.
-  eapply (Genv.init_mem_transf_partial TRANSF); eauto.
-  replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero)
-     with (Vptr fb Ptrofs.zero).
-  econstructor; eauto.
-  constructor.
-  apply Mem.extends_refl.
-  split. auto. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence.
-  intros. rewrite Regmap.gi. auto.
-  unfold Genv.symbol_address.
-  rewrite (match_program_main TRANSF).
-  rewrite symbols_preserved.
-  unfold ge; rewrite H1. auto.
-Qed.
-
-Lemma transf_final_states:
-  forall st1 st2 r,
-  match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r.
-Proof.
-  intros. inv H0. inv H. constructor. assumption.
-  compute in H1. inv H1.
-  generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto.
-Qed.
-
-Theorem transf_program_correct:
-  forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
-Proof.
-  eapply forward_simulation_star with (measure := measure)
-         (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1).
-  - apply senv_preserved.
-  - simpl; intros. exploit transf_initial_states; eauto.
-    intros (s2 & A & B).
-    exists s2; intuition auto. apply wf_initial; auto.
-  - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto.
-  - simpl; intros. destruct H0 as [MS WF]. 
-    exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ].
-    + left; exists s2'; intuition auto. eapply wf_step; eauto. 
-    + right; intuition auto. eapply wf_step; eauto.
 Qed.
 
-End PRESERVATION.
-*)
\ No newline at end of file
+End PRESERVATION.
\ No newline at end of file
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 4a35485e..a47654b8 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -167,6 +167,15 @@ Proof.
   red; intros; elim n. eapply preg_of_injective; eauto.
 Qed.
 
+Corollary agree_set_mreg_parallel:
+  forall ms sp rs r v v',
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs).
+Proof.
+  intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto.
+Qed.
+
 Lemma agree_set_other:
   forall ms sp rs r v,
   agree ms sp rs ->
@@ -184,6 +193,18 @@ Proof.
   intros. unfold incrPC. apply agree_set_other. auto. auto.
 Qed.
 
+Lemma agree_set_pair:
+  forall sp p v v' ms rs,
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs).
+Proof.
+  intros. destruct p; simpl.
+- apply agree_set_mreg_parallel; auto.
+- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
+  apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
+Qed.
+
 Lemma agree_set_res:
   forall res ms sp rs v v',
   agree ms sp rs ->
@@ -230,6 +251,23 @@ Proof.
   intros. rewrite Pregmap.gso; auto.
 Qed.
 
+Lemma agree_undef_caller_save_regs:
+  forall ms sp rs,
+  agree ms sp rs ->
+  agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs).
+Proof.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split.
+- unfold proj_sumbool; rewrite dec_eq_true. auto.
+- auto.
+- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
+  destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
++ apply list_in_map_inv in i. destruct i as (mr & A & B). 
+  assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
+  apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
++ destruct (is_callee_save r) eqn:CS; auto.
+  elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
+Qed.
+
 Lemma agree_change_sp:
   forall ms sp rs sp',
   agree ms sp rs -> sp' <> Vundef ->
@@ -262,6 +300,62 @@ Proof.
   exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto.
 Qed.
 
+(** Connection between Mach and Asm calling conventions for external
+    functions. *)
+
+Lemma extcall_arg_match:
+  forall ms sp rs m m' l v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Mach.extcall_arg ms m sp l v ->
+  exists v', extcall_arg rs m' l v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1.
+  exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto.
+  unfold Mach.load_stack in H2.
+  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
+  rewrite (sp_val _ _ _ H) in A.
+  exists v'; split; auto.
+  econstructor. eauto. assumption.
+Qed.
+
+Lemma extcall_arg_pair_match:
+  forall ms sp rs m m' p v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Mach.extcall_arg_pair ms m sp p v ->
+  exists v', extcall_arg_pair rs m' p v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1.
+- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto.
+- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1).
+  exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2).
+  exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto.
+Qed.
+
+Lemma extcall_args_match:
+  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall ll vl,
+  list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl ->
+  exists vl', list_forall2 (extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; intros.
+  exists (@nil val); split. constructor. constructor.
+  exploit extcall_arg_pair_match; eauto. intros [v1' [A B]].
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
+Qed.
+
+Lemma extcall_arguments_match:
+  forall ms m m' sp rs sg args,
+  agree ms sp rs -> Mem.extends m m' ->
+  Mach.extcall_arguments ms m sp sg args ->
+  exists args', extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
+Proof.
+  unfold Mach.extcall_arguments, extcall_arguments; intros.
+  eapply extcall_args_match; eauto.
+Qed.
+
 Lemma set_res_other:
   forall r res v rs,
   data_preg r = false ->
@@ -639,9 +733,36 @@ Proof.
   intros. apply exec_straight_opt_intro. eapply exec_straight_opt_step; eauto.
 Qed.
 
+(** Like exec_straight predicate, but on blocks *)
+
+Inductive exec_straight_blocks: bblocks -> regset -> mem ->
+                                bblocks -> regset -> mem -> Prop :=
+  | exec_straight_blocks_one:
+      forall b1 c rs1 m1 rs2 m2,
+      exec_bblock lk ge fn b1 rs1 m1 E0 rs2 m2 ->
+      rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b1)) ->
+      exec_straight_blocks (b1 :: c) rs1 m1 c rs2 m2
+  | exec_straight_blocks_step:
+      forall b c rs1 m1 rs2 m2 c' rs3 m3,
+      exec_bblock lk ge fn b rs1 m1 E0 rs2 m2 ->
+      rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b)) ->
+      exec_straight_blocks c rs2 m2 c' rs3 m3 ->
+      exec_straight_blocks (b :: c) rs1 m1 c' rs3 m3.
+
+Lemma exec_straight_blocks_trans:
+  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
+  exec_straight_blocks c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight_blocks c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight_blocks c1 rs1 m1 c3 rs3 m3.
+Proof.
+  induction 1; intros.
+  eapply exec_straight_blocks_step; eauto.
+  eapply exec_straight_blocks_step; eauto.
+Qed.
+
 (** Linking exec_straight with exec_straight_blocks *)
 
-(* Lemma exec_straight_pc:
+Lemma exec_straight_pc:
   forall c c' rs1 m1 rs2 m2,
   exec_straight c rs1 m1 c' rs2 m2 ->
   rs2 PC = rs1 PC.
@@ -651,7 +772,7 @@ Proof.
   - eapply exec_basic_instr_pc; eauto.
   - rewrite (IHc c' rs3 m3 rs2 m2); auto.
     erewrite exec_basic_instr_pc; eauto.
-Qed. *)
+Qed.
 
 Lemma exec_body_pc:
   forall ge l rs1 m1 rs2 m2,
@@ -667,6 +788,54 @@ Proof.
     erewrite exec_basic_instr_pc; eauto.
 Qed.
 
+(** The following lemmas show that straight-line executions
+  (predicate [exec_straight_blocks]) correspond to correct Asm executions. *)
+
+Lemma exec_straight_steps_1:
+  forall c rs m c' rs' m',
+  exec_straight_blocks c rs m c' rs' m' ->
+  size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned ->
+  forall b ofs,
+  rs#PC = Vptr b ofs ->
+  Genv.find_funct_ptr ge b = Some (Internal fn) ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c ->
+  plus (step lk) ge (State rs m) E0 (State rs' m').
+Proof.
+  induction 1; intros.
+  apply plus_one.
+  econstructor; eauto.
+  eapply find_bblock_tail. eauto.
+  eapply plus_left'.
+  econstructor; eauto.
+  eapply find_bblock_tail. eauto.
+  apply IHexec_straight_blocks with b0 (Ptrofs.add ofs (Ptrofs.repr (size b))).
+  auto. rewrite H0. rewrite H3. reflexivity.
+  auto.
+  apply code_tail_next_int; auto.
+  traceEq.
+Qed.
+
+Lemma exec_straight_steps_2:
+  forall c rs m c' rs' m',
+  exec_straight_blocks c rs m c' rs' m' ->
+  size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned ->
+  forall b ofs,
+  rs#PC = Vptr b ofs ->
+  Genv.find_funct_ptr ge b = Some (Internal fn) ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c ->
+  exists ofs',
+     rs'#PC = Vptr b ofs'
+  /\ code_tail (Ptrofs.unsigned ofs') (fn_blocks fn) c'.
+Proof.
+  induction 1; intros.
+  exists (Ptrofs.add ofs (Ptrofs.repr (size b1))). split.
+  rewrite H0. rewrite H2. auto.
+  apply code_tail_next_int; auto.
+  apply IHexec_straight_blocks with (Ptrofs.add ofs (Ptrofs.repr (size b))).
+  auto. rewrite H0. rewrite H3. reflexivity. auto.
+  apply code_tail_next_int; auto.
+Qed.
+
 End STRAIGHTLINE.
 
 (** * Properties of the Machblock call stack *)
diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v
index bc4302ca..870211b8 100644
--- a/aarch64/Asmblockgenproof1.v
+++ b/aarch64/Asmblockgenproof1.v
@@ -1121,32 +1121,213 @@ Proof.
   destruct r; try contradiction; destruct v1; auto; destruct v2; auto.
 Qed.
 
-Lemma transl_cbranch_correct:
-  forall cond args lbl k c m ms b sp rs m' bdy t ofs,
-  transl_cond_branch cond args lbl k = OK (bdy, c) ->
+Lemma cmpu_bool_some_b: forall n x rs m0 b tbb,
+  Int.eq n Int.zero = true ->
+  Val.cmp_bool Ceq (rs (preg_of m0)) (Vint n) = Some b ->
+  ireg_of m0 = OK x ->
+  Val_cmpu_bool Ceq (incrPC (Ptrofs.repr (size tbb)) rs x) (Vint Int.zero) = Some b.
+Proof.
+  intros.
+  replace (Vint Int.zero) with (Vint n).
+  2: { apply f_equal. apply Int.same_if_eq; auto. }
+  unfold incrPC. Simpl. replace (rs (preg_of m0)) with (rs x) in H0. auto.
+  apply f_equal. symmetry. apply ireg_of_eq; auto.
+Qed.
+
+Lemma transl_cbranch_correct_1:
+  forall cond args lbl c k b m ms sp rs m' tbb bdy,
+  transl_cond_branch cond args lbl k = OK (bdy,c) ->
   eval_condition cond (List.map ms args) m = Some b ->
   agree ms sp rs ->
   Mem.extends m m' ->
-  exists rs' m' rs'' m'',
-     exec_body lk ge bdy rs m = Next rs' m'
-  /\ exec_exit ge fn ofs rs' m' (Some c) t rs'' m''
+  exists rs',
+     exec_straight_opt ge lk bdy rs m' k rs' m'
+  /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = eval_branch fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m' (Some b)
   /\ forall r, data_preg r = true -> rs'#r = rs#r.
 Proof.
+  intros until bdy; intros TR EC AG MEMX.
+  set (vl' := map rs (map preg_of args)).
+  assert (EVAL': eval_condition cond vl' m' = Some b).
+  { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
+  destruct cond; unfold transl_cond_branch in TR;
+  try unfold transl_cond_branch_default in TR;
+  simpl in TR; destruct args; ArgsInv.
+- (* Ccomp *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_signed_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_sint; auto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+- (* Ccompu *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_uint; auto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+- (* Ccompimm *)
+admit.
+(*   destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))];
+  destruct c0; try destruct (Int.eq n Int.zero) eqn:IEQ;
+  monadInv TR; try monadInv EQ; econstructor; split;
+  try (econstructor; try apply exec_straight_one);
+  simpl in *; eauto; try (split; intros; auto).
+  all: try (erewrite (cmpu_bool_some_b n x rs m0 b tbb); eauto; assumption).
+  unfold incrPC; Simpl.
+  try (rewrite (cmpu_bool_some_b n x rs m0 b tbb); auto).
+  + monadInv TR; try monadInv EQ. econstructor; split. econstructor; apply exec_straight_one. simpl in *; eauto.
+    split; intros; auto. unfold compare_int, incrPC. Simpl. auto.
+    assert (Val_cmpu_bool Ceq (incrPC (Ptrofs.repr (size tbb)) rs x) (Vint Int.zero) = Some b).
+    { replace (Vint Int.zero) with (Vint n).
+      2: { apply f_equal. apply Int.same_if_eq; auto. }
+      unfold incrPC. Simpl. replace (rs (preg_of m0)) with (rs x) in EVAL'. auto.
+      apply f_equal. symmetry. apply ireg_of_eq; auto. }
+     rewrite H; auto.
+    inv EQ.
+    split; intros; auto. assert (eval_testcond (cond_for_unsigned_cmp c0)
+       (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_uint; auto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+  
+  destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. 
+  destruct r; reflexivity || discriminate.
++ econstructor; split.
+  apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
+  split; intros. apply eval_testcond_compare_sint; auto. 
+  destruct r; reflexivity || discriminate.
++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one.
+  simpl. rewrite B, C by eauto with asmgen. eauto. auto.
+  split; intros. apply eval_testcond_compare_sint; auto. 
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. *)
+- (* Ccompuimm *)
+  admit.
+- (* Ccompshift *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_signed_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb))
+        (compare_int rs (rs x) (eval_shift_op_int (rs x0) (transl_shift s a)))) = Some b).
+  { apply eval_testcond_compare_sint; auto. rewrite transl_eval_shift; auto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+- (* Ccompushift *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb))
+        (compare_int rs (rs x) (eval_shift_op_int (rs x0) (transl_shift s a)))) = Some b).
+  { apply eval_testcond_compare_uint; auto. rewrite transl_eval_shift; auto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+- (* Cmaskzero *) admit.
+- (* Cmasknotzero *) admit.
+- (* Ccompl *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_signed_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_long rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_slong; auto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+- (* Ccomplu *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_long rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_ulong; auto. eapply Val_cmplu_bool_correct; eauto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+- (* Ccomplimm *) admit.
+- (* Ccompluimm *) admit.
+- (* Ccomplshift *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_signed_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb))
+        (compare_long rs (rs x) (eval_shift_op_long (rs x0) (transl_shift s a)))) = Some b).
+  { apply eval_testcond_compare_slong; auto. rewrite transl_eval_shiftl; auto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+- (* Ccomplushift *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb))
+        (compare_long rs (rs x) (eval_shift_op_long (rs x0) (transl_shift s a)))) = Some b).
+  { apply eval_testcond_compare_ulong; auto. rewrite transl_eval_shiftl; auto.
+    eapply Val_cmplu_bool_correct; eauto. } rewrite H. auto.
+  destruct r; reflexivity || discriminate.
+- (* Cmasklzero *) admit.
+- (* Cmasknotzero *) admit.
+- (* Ccompf *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_float_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_float; auto. } rewrite H. auto.
+  destruct r; discriminate || rewrite compare_float_inv; auto.
+- (* Cnotcompf *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_float_not_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_not_float; auto. } rewrite H. auto.
+  destruct r; discriminate || rewrite compare_float_inv; auto.
+- (* Ccompfzero *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_float_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (Vfloat Float.zero))) = Some b).
+  { apply eval_testcond_compare_float; auto. } rewrite H. auto.
+  destruct r; discriminate || rewrite compare_float_inv; auto.
+- (* Cnotcompfzero *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_float_not_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (Vfloat Float.zero))) = Some b).
+  { apply eval_testcond_compare_not_float; auto. } rewrite H. auto.
+  destruct r; discriminate || rewrite compare_float_inv; auto.
+- (* Ccompfs *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_float_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_single; auto. } rewrite H. auto.
+  destruct r; discriminate || rewrite compare_single_inv; auto.
+- (* Cnotcompfs *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_float_not_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (rs x0))) = Some b).
+  { apply eval_testcond_compare_not_single; auto. } rewrite H. auto.
+  destruct r; discriminate || rewrite compare_single_inv; auto.
+- (* Ccompfszero *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_float_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (Vsingle Float32.zero))) = Some b).
+  { apply eval_testcond_compare_single; auto. } rewrite H. auto.
+  destruct r; discriminate || rewrite compare_single_inv; auto.
+- (* Cnotcompfszero *)
+  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
+  split; intros. assert (eval_testcond (cond_for_float_not_cmp c0)
+     (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (Vsingle Float32.zero))) = Some b).
+  { apply eval_testcond_compare_not_single; auto. } rewrite H. auto.
+  destruct r; discriminate || rewrite compare_single_inv; auto.
 Admitted.
 
-(* Lemma transl_cbranch_correct_true:
-  forall cond args lbl k c m ms sp rs m' bdy,
-  transl_cond_branch cond args lbl k = OK (bdy, c) ->
+Lemma transl_cbranch_correct_true:
+  forall cond args lbl k c m ms sp rs m' tbb bdy,
+  transl_cond_branch cond args lbl k = OK (bdy,c) ->
   eval_condition cond (List.map ms args) m = Some true ->
   agree ms sp rs ->
   Mem.extends m m' ->
-  exists rs', exists insn,
+  exists rs',
      exec_straight_opt ge lk bdy rs m' k rs' m'
-  /\ exec_cfi ge fn insn (nextinstr rs') m' = goto_label fn lbl (nextinstr rs') m'
+  /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = goto_label fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m'
   /\ forall r, data_preg r = true -> rs'#r = rs#r.
 Proof.
   intros. eapply transl_cbranch_correct_1 with (b := true); eauto.
-Qed.  *)
+Qed.
+
+Lemma transl_cbranch_correct_false:
+  forall cond args lbl k c m ms sp rs m' tbb bdy,
+  transl_cond_branch cond args lbl k = OK (bdy,c) ->
+  eval_condition cond (List.map ms args) m = Some false ->
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  exists rs',
+     exec_straight_opt ge lk bdy rs m' k rs' m'
+  /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = Next (incrPC (Ptrofs.repr (size tbb)) rs') m'
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
+Proof.
+  intros. exploit transl_cbranch_correct_1. all: eauto.
+Qed.
 
 Lemma transl_cond_correct:
   forall cond args k c rs m,
@@ -1727,6 +1908,24 @@ Proof.
   split. Simpl. intros; Simpl.
 Qed.
 
+Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset),
+  Mem.storev Mint64 m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
+  preg_of_iregsp base <> IR X16 ->
+  (DR (IR (RR1 src))) <> (DR (IR (RR1 X16))) ->
+  exists rs',
+     exec_straight ge lk (storeptr_bc src base ofs k) rs m k rs' m'
+  /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r.
+Proof.
+  intros. 
+  destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
+  exploit indexed_memory_access_correct; eauto. intros (ad & rs' & A & B & C). 
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A.
+  apply exec_straight_one. simpl. unfold exec_store_rs_a. rewrite B, C, H. eauto.
+  discriminate. auto.
+  intros; Simpl. rewrite C; auto.
+Qed.
+
 Lemma loadind_correct:
   forall (base: iregsp) ofs ty dst k c (rs: regset) m v,
   loadind base ofs ty dst k = OK c ->