intermediatet commit before builtins

6 files changed, 3292 insertions, 99 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 96e7db4b..e260bd69 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -389,9 +389,9 @@ Definition arith_extended
 Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
   if Int.eq n Int.zero then
     Pmov rd r1 ::bi k
-  else if Int.eq n Int.one then
+(*   else if Int.eq n Int.one then
     Padd W (SOlsr (Int.repr 31)) X16 r1 r1 ::bi
-    Porr W (SOasr n) rd XZR X16 ::bi k
+    Porr W (SOasr n) rd XZR X16 ::bi k *)
   else
     Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi
     Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi
@@ -400,9 +400,9 @@ Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
 Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
   if Int.eq n Int.zero then
     Pmov rd r1 ::bi k
-  else if Int.eq n Int.one then
+(*   else if Int.eq n Int.one then
     Padd X (SOlsr (Int.repr 63)) X16 r1 r1 ::bi
-    Porr X (SOasr n) rd XZR X16 ::bi k
+    Porr X (SOasr n) rd XZR X16 ::bi k *)
   else
     Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi
     Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi
@@ -1141,8 +1141,11 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
       OK (if ep then c else loadptr_bc XSP f.(fn_link_ofs) X29 c)
   | MBop op args res =>
       transl_op op args res k
-  | MBload _ chunk addr args dst =>
-      transl_load chunk addr args dst k
+  | MBload t chunk addr args dst =>
+      match t with
+      | TRAP => transl_load chunk addr args dst k
+      | NOTRAP => Error(msg "Asmgenblock.transl_instr_basic: NOTRAP load not supported in aarch64.")
+      end
   | MBstore chunk addr args src =>
       transl_store chunk addr args src k
   end.
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 33acc110..55f50b7a 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -1,12 +1,24 @@
-(** Correctness proof for aarch64/Asmblock generation: main proof. 
-CURRENTLY A STUB !
-*)
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
 
 Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock IterList.
-Require Import Asmblockgen Asmblockgenproof0.
+Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
 
 Module MB := Machblock.
 Module AB := Asmblock.
@@ -44,13 +56,16 @@ Lemma functions_translated:
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
 Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
-Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
-  Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
-
-(*Lemma functions_bound_max_pos: forall fb f,
+Lemma functions_transl:
+  forall fb f tf,
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  (max_pos next f) <= Ptrofs.max_unsigned.
-Admitted.*)
+  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. unfold transf_function in H0. monadInv H0.
+  destruct zlt; try discriminate. rewrite EQ in EQ0. inv EQ0; inv EQ1; auto.
+Qed.
 
 Lemma transf_function_no_overflow:
   forall f tf,
@@ -60,6 +75,14 @@ Proof.
   omega.
 Qed.
 
+Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
+  Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
+
+(*Lemma functions_bound_max_pos: forall fb f,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  (max_pos next f) <= Ptrofs.max_unsigned.
+Admitted.*)
+
 (** * Proof of semantic preservation *)
 
 (** Semantic preservation is proved using a complex simulation diagram
@@ -118,6 +141,183 @@ Inductive match_states: Machblock.state -> Asm.state -> Prop :=
       match_states (Machblock.Returnstate s ms m)
                    (Asm.State rs m').
 
+Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *)
+
+Lemma cons_bblocks_label:
+  forall hd bdy ex tbb tc,
+  cons_bblocks hd bdy ex = tbb::tc ->
+  header tbb = hd.
+Proof.
+  intros until tc. intros CONSB. unfold cons_bblocks in CONSB.
+  destruct ex; try destruct bdy; try destruct c; try destruct i.
+  all: inv CONSB; simpl; auto.
+Qed.
+
+Lemma cons_bblocks_label2:
+  forall hd bdy ex tbb1 tbb2,
+  cons_bblocks hd bdy ex = tbb1::tbb2::nil ->
+  header tbb2 = nil.
+Proof.
+  intros until tbb2. intros CONSB. unfold cons_bblocks in CONSB.
+  destruct ex; try destruct bdy; try destruct c; try destruct i.
+  all: inv CONSB; simpl; auto.
+Qed.
+
+Remark in_dec_transl:
+  forall lbl hd,
+  (if in_dec lbl hd then true else false) = (if MB.in_dec lbl hd then true else false).
+Proof.
+  intros. destruct (in_dec lbl hd), (MB.in_dec lbl hd). all: tauto.
+Qed.
+
+Lemma transl_is_label:
+  forall lbl bb tbb f ep tc,
+  transl_block f bb ep = OK (tbb::tc) ->
+  is_label lbl tbb = MB.is_label lbl bb.
+Proof.
+  intros until tc. intros TLB.
+  destruct tbb as [thd tbdy tex]; simpl in *.
+  monadInv TLB.
+  unfold is_label. simpl.
+  apply cons_bblocks_label in H0. simpl in H0. subst.
+  rewrite in_dec_transl. auto.
+Qed.
+
+Lemma transl_is_label_false2:
+  forall lbl bb f ep tbb1 tbb2,
+  transl_block f bb ep = OK (tbb1::tbb2::nil) ->
+  is_label lbl tbb2 = false.
+Proof.
+  intros until tbb2. intros TLB.
+  destruct tbb2 as [thd tbdy tex]; simpl in *.
+  monadInv TLB. apply cons_bblocks_label2 in H0. simpl in H0. subst.
+  apply is_label_correct_false. simpl. auto.
+Qed.
+
+(*
+Lemma transl_is_label2:
+  forall f bb ep tbb1 tbb2 lbl,
+  transl_block f bb ep = OK (tbb1::tbb2::nil) ->
+     is_label lbl tbb1 = MB.is_label lbl bb
+  /\ is_label lbl tbb2 = false.
+Proof.
+  intros. split. eapply transl_is_label; eauto. eapply transl_is_label_false2; eauto.
+Qed. *)
+
+Lemma transl_block_nonil:
+  forall f c ep tc,
+  transl_block f c ep = OK tc ->
+  tc <> nil.
+Proof.
+  intros. monadInv H. unfold cons_bblocks.
+  destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i.
+  all: discriminate.
+Qed.
+
+Lemma transl_block_limit: forall f bb ep tbb1 tbb2 tbb3 tc,
+  ~transl_block f bb ep = OK (tbb1 :: tbb2 :: tbb3 :: tc).
+Proof.
+  intros. intro. monadInv H.
+  unfold cons_bblocks in H0.
+  destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i.
+  all: discriminate.
+Qed.
+
+Lemma find_label_transl_false:
+  forall x f lbl bb ep x',
+  transl_block f bb ep = OK x ->
+  MB.is_label lbl bb = false ->
+  find_label lbl (x++x') = find_label lbl x'.
+Proof.
+  intros until x'. intros TLB MBis; simpl; auto.
+  destruct x as [|x0 x1]; simpl; auto.
+  destruct x1 as [|x1 x2]; simpl; auto.
+  - erewrite <- transl_is_label in MBis; eauto. rewrite MBis. auto.
+  - destruct x2 as [|x2 x3]; simpl; auto.
+    + erewrite <- transl_is_label in MBis; eauto. rewrite MBis.
+      erewrite transl_is_label_false2; eauto.
+    + apply transl_block_limit in TLB. destruct TLB.
+Qed.
+
+Lemma transl_blocks_label:
+  forall lbl f c tc ep,
+  transl_blocks f c ep = OK tc ->
+  match MB.find_label lbl c with
+  | None => find_label lbl tc = None
+  | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_blocks f c' false = OK tc'
+  end.
+Proof.
+  induction c; simpl; intros.
+  inv H. auto.
+  monadInv H.
+  destruct (MB.is_label lbl a) eqn:MBis.
+  - destruct x as [|tbb tc]. { apply transl_block_nonil in EQ. contradiction. }
+    simpl find_label. exploit transl_is_label; eauto. intros ABis. rewrite MBis in ABis.
+    rewrite ABis.
+    eexists. eexists. split; eauto. simpl transl_blocks.
+    assert (MB.header a <> nil).
+    { apply MB.is_label_correct_true in MBis.
+      destruct (MB.header a). contradiction. discriminate. }
+    destruct (MB.header a); try contradiction.
+    rewrite EQ. simpl. rewrite EQ1. simpl. auto.
+  - apply IHc in EQ1. destruct (MB.find_label lbl c).
+    + destruct EQ1 as (tc' & FIND & TLBS). exists tc'; eexists; auto.
+      erewrite find_label_transl_false; eauto.
+    + erewrite find_label_transl_false; eauto.
+Qed.
+
+Lemma find_label_nil:
+  forall bb lbl c,
+  header bb = nil ->
+  find_label lbl (bb::c) = find_label lbl c.
+Proof.
+  intros. destruct bb as [hd bdy ex]; simpl in *. subst.
+  assert (is_label lbl {| AB.header := nil; AB.body := bdy; AB.exit := ex; AB.correct := correct |} = false).
+  { erewrite <- is_label_correct_false. simpl. auto. }
+  rewrite H. auto.
+Qed.
+
+Theorem transl_find_label:
+  forall lbl f tf,
+  transf_function f = OK tf ->
+  match MB.find_label lbl f.(MB.fn_code) with
+  | None => find_label lbl tf.(fn_blocks) = None
+  | Some c => exists tc, find_label lbl tf.(fn_blocks) = Some tc /\ transl_blocks f c false = OK tc
+  end.
+Proof.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); inv EQ0. clear g.
+  monadInv EQ. unfold make_prologue. simpl fn_blocks. repeat (rewrite find_label_nil); simpl; auto.
+  eapply transl_blocks_label; eauto.
+Qed.
+
+End TRANSL_LABEL.
+(** A valid branch in a piece of Machblock code translates to a valid ``go to''
+  transition in the generated Asmblock 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 ->
+  MB.find_label lbl f.(MB.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:
@@ -144,11 +344,6 @@ Ltac exploreInst :=
   | [ H : bind _ _ = OK _ |- _ ] => monadInv H
   | [ H : Error _ = OK _ |- _ ] => inversion H
   end.
-  
-Ltac desif :=
-  repeat match goal with
-  | [ |- context[if ?f then _ else _ ] ] => destruct f
-  end.
 
 (** Some translation properties *)
 
@@ -488,6 +683,688 @@ Proof.
   all: simpl; auto.
 Qed.
 
+Lemma exec_straight_body:
+  forall c c' rs1 m1 rs2 m2,
+  exec_straight tge lk c rs1 m1 c' rs2 m2 ->
+  exists l,
+     c = l ++ c'
+  /\ exec_body lk tge l rs1 m1 = Next rs2 m2.
+Proof.
+  induction c; try (intros; inv H; fail).
+  intros until m2. intros EXES. inv EXES.
+  - exists (a :: nil). repeat (split; simpl; auto). rewrite H6. auto.
+  - eapply IHc in H7; eauto. destruct H7 as (l' & Hc & EXECB). subst.
+    exists (a :: l'). repeat (split; simpl; auto).
+    rewrite H1. auto.
+Qed.
+
+Lemma exec_straight_body2:
+  forall c rs1 m1 c' rs2 m2,
+  exec_straight tge lk c rs1 m1 c' rs2 m2 ->
+  exists body,
+     exec_body lk tge body rs1 m1 = Next rs2 m2
+  /\ body ++ c' = c.
+Proof.
+  intros until m2. induction 1.
+  - exists (i1::nil). split; auto. simpl. rewrite H. auto.
+  - destruct IHexec_straight as (bdy & EXEB & BTC).
+    exists (i:: bdy). split; simpl.
+    + rewrite H. auto.
+    + congruence.
+Qed.
+
+Lemma exec_straight_opt_body2:
+  forall c rs1 m1 c' rs2 m2,
+  exec_straight_opt tge lk c rs1 m1 c' rs2 m2 ->
+  exists body,
+     exec_body lk tge body rs1 m1 = Next rs2 m2
+  /\ body ++ c' = c.
+Proof.
+  intros until m2. intros EXES.
+  inv EXES.
+  - exists nil. split; auto.
+  - eapply exec_straight_body2. auto.
+Qed.
+
+Lemma PC_not_data_preg: forall r ,
+  data_preg r = true ->
+  r <> PC.
+Proof.
+  intros. destruct (PregEq.eq r PC); [ rewrite e in H; simpl in H; discriminate | auto ].
+Qed.
+
+Lemma X30_not_data_preg: forall r ,
+  data_preg r = true ->
+  r <> X30.
+Proof.
+  intros. destruct (PregEq.eq r X30); [ 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 ->
+  cur cs2 = tbb ->
+  match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 ->
+  match_asmstate fb cs2 (State rs1 m1) ->
+  exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') t S'' ->
+  (exists rs3 m3 rs4 m4,
+      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.
+  inv ESTEP.
+  - inv MCS. inv MAS. simpl in *.
+    inv Hpstate.
+    destruct ctl.
+    + (* MBcall *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence. subst f0.
+      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
+        eapply transf_function_no_overflow; eauto.
+      destruct s1 as [rf|fid]; simpl in H1.
+      * (* Indirect call *)
+        monadInv H1. monadInv EQ.
+        assert (ms' rf = Vptr f' Ptrofs.zero).
+        { unfold find_function_ptr in H12. destruct (ms' rf); try discriminate.
+          revert H12; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
+        assert (rs2 x = Vptr f' Ptrofs.zero).
+        { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. }
+        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. }
+        assert (f1 = f) by congruence. subst f1.
+        exploit return_address_offset_correct; eauto. intros; subst ra.
+
+        repeat eexists.
+        econstructor; eauto. econstructor.
+          econstructor; eauto. econstructor; eauto.
+          eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros.
+          unfold incrPC; repeat Simpl; auto.
+          simpl. unfold incrPC; rewrite Pregmap.gso; auto; try discriminate.
+          rewrite !Pregmap.gss. rewrite PCeq. rewrite Heqofs'. simpl. auto.
+
+      * (* Direct call *)
+        monadInv H1.
+        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.
+        assert (f1 = f) by congruence. subst f1.
+        exploit return_address_offset_correct; eauto. intros; subst ra.
+        repeat eexists.
+        econstructor; eauto. econstructor.
+          econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros.
+        unfold incrPC; repeat Simpl; auto. unfold Genv.symbol_address. rewrite symbols_preserved. simpl in H12. rewrite H12. auto.
+        unfold incrPC; simpl; rewrite Pregmap.gso; try discriminate. rewrite !Pregmap.gss.
+        subst. unfold Val.offset_ptr. rewrite PCeq. auto.
+    + (* MBtailcall *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence.  subst f0.
+      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
+        eapply transf_function_no_overflow; eauto.
+      exploit Mem.loadv_extends. eauto. eexact H13. auto. simpl. intros [parent' [A B]].
+      destruct s1 as [rf|fid]; simpl in H11. 
+      * monadInv H1. monadInv EQ.
+        assert (ms' rf = Vptr f' Ptrofs.zero).
+          { destruct (ms' rf); try discriminate. revert H11. predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
+        assert (rs2 x = Vptr f' Ptrofs.zero).
+          { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. }
+
+        assert (f = f1) by congruence. subst f1. clear FIND1. clear H12.
+        exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
+        exploit exec_straight_body; eauto.
+        intros (l & MKEPI & EXEB).
+        repeat eexists. rewrite app_nil_r in MKEPI.
+        rewrite <- MKEPI in EXEB.
+        eauto. econstructor. simpl. unfold incrPC.
+        rewrite !Pregmap.gso; try discriminate. eauto.
+        econstructor; eauto.
+          { apply agree_set_other.
+            - econstructor; auto with asmgen.
+              + apply V.
+              + intro r. destruct r; apply V; auto.
+            - eauto with asmgen. }
+        rewrite Pregmap.gss. rewrite Z; auto; try discriminate.
+        eapply ireg_of_not_X30''; eauto.
+        eapply ireg_of_not_X16''; eauto.
+      * monadInv H1. assert (f = f1) by congruence. subst f1. clear FIND1. clear H12.
+        exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
+        exploit exec_straight_body; eauto.
+        intros (l & MKEPI & EXEB).
+        repeat eexists. inv EQ. rewrite app_nil_r in MKEPI.
+        rewrite <- MKEPI in EXEB.
+        eauto. inv EQ. econstructor. simpl. unfold incrPC.
+        eauto.
+        econstructor; eauto.
+        { apply agree_set_other.
+          - econstructor; auto with asmgen.
+            + apply V.
+            + intro r. destruct r; apply V; auto.
+          - 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.
+    + (* MBgoto *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence. subst f0. assert (f1 = f) by congruence. subst f1. clear H9.
+      remember (incrPC (Ptrofs.repr (size tbb)) rs2) as rs2'.
+      exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND'.
+      assert (tf = fn) by congruence. subst tf.
+      exploit find_label_goto_label.
+        eauto. eauto.
+        instantiate (2 := rs2').
+        { subst. unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. eauto. }
+        eauto.
+      intros (tc' & rs' & GOTO & AT2 & INV).
+
+      eexists. eexists. repeat eexists. repeat split.
+      econstructor; eauto.
+        rewrite Heqrs2' in INV. unfold incrPC in INV.
+        rewrite Heqrs2' in GOTO; simpl; eauto.
+        econstructor; eauto.
+        eapply agree_exten; eauto with asmgen.
+        assert (forall r : preg, r <> PC -> rs' r = rs2 r).
+        { intros. rewrite Heqrs2' in INV.
+          rewrite INV; unfold incrPC; try rewrite Pregmap.gso; auto. }
+        eauto with asmgen.
+        congruence.
+    + (* MBcond *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      * (* 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. *) }
+        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.
+        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.
+
+        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. discriminate.
+
+      * (* MBcond false *)
+        assert (f0 = f) by congruence. subst f0.
+        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 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. }
+        rewrite PCeq' in PCeq.
+        exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'.
+        assert (tf = fn) by congruence. subst tf.
+
+        assert (NOOV: size_blocks fn.(fn_blocks) <= Ptrofs.max_unsigned).
+          eapply transf_function_no_overflow; eauto.
+        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.
+
+        econstructor; eauto.
+          unfold nextblock, incrPC. Simpl. 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. 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.
+      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 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.
+      
+      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.
+      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. }
+        discriminate.
+    + (* MBreturn *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence. subst f0.
+      assert (NOOV: size_blocks tf.(fn_blocks) <= 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_body; eauto.
+        simpl. eauto.
+      intros EXEB.
+      assert (f1 = f) by congruence. subst f1.
+      
+      repeat eexists.
+        rewrite H6. simpl extract_basic. eauto.
+        rewrite H7. simpl extract_ctl. simpl. reflexivity.
+      econstructor; eauto.
+        unfold nextblock, 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.
+    simpl. repeat eexists.
+    econstructor. 4: instantiate (3 := false). all:eauto.
+      unfold nextblock, incrPC. Simpl. 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.
+    discriminate.
+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)) ->
+  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 ->
+  match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
+  (exists rs2 m2 l cs2 tbdy',
+       cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := tbdy'; pbody2 := pbody2 cs1;
+                pctl := pctl cs1; ep := it1_is_parent (ep cs1) bi; rem := rem cs1; cur := cur cs1 |}
+    /\ tbdy = l ++ tbdy'
+    /\ 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.
+  simpl in *. inv Hpstate.
+  rewrite Hbody in TBC. monadInv TBC.
+  inv BSTEP.
+
+  - (* MBgetstack *)
+    simpl in EQ0.
+    unfold Mach.load_stack in H.
+    exploit Mem.loadv_extends; eauto. intros [v' [A B]].
+    rewrite (sp_val _ _ _ AG) in A.
+    exploit loadind_correct; eauto with asmgen.
+    intros (rs2 & EXECS & Hrs'1 & Hrs'2).
+    eapply exec_straight_body in EXECS.
+    destruct EXECS as (l & Hlbi & 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. simpl. auto. }
+    subst. simpl in Hheadereq.
+
+    eapply match_codestate_intro; eauto.
+    eapply agree_set_mreg; eauto with asmgen.
+    intro Hep. simpl in Hep. discriminate.
+  - (* MBsetstack *)
+    simpl in EQ0.
+    unfold Mach.store_stack in H.
+    assert (Val.lessdef (ms src) (rs1 (preg_of src))). { eapply preg_val; eauto. }
+    exploit Mem.storev_extends; eauto. intros [m2' [A B]].
+    exploit storeind_correct; eauto with asmgen.
+    rewrite (sp_val _ _ _ AG) in A. eauto. intros [rs' [P Q]].
+
+    eapply exec_straight_body in P.
+    destruct P as (l & ll & EXECB).
+    exists rs', m2', l.
+    eexists. eexists. split. instantiate (1 := x). eauto.
+    repeat (split; auto).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+    subst.
+    eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
+    eapply agree_undef_regs; eauto with asmgen.
+    simpl; intros. rewrite Q; auto with asmgen. rewrite Hheader in DXP. auto.
+  - (* MBgetparam *)
+    simpl in EQ0.
+
+    assert (f0 = f) by congruence; subst f0.
+    unfold Mach.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]].
+
+    monadInv EQ0. rewrite Hheader. rewrite Hheader in DXP.
+    destruct ep0 eqn:EPeq.
+
+  (* X29 contains parent *)
+    + exploit loadind_correct. eexact EQ1.
+      instantiate (2 := rs1). rewrite DXP; eauto. discriminate.
+      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. simpl. auto. }
+      subst.
+      eapply match_codestate_intro; eauto.
+
+      eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
+      simpl; intros. rewrite R; auto with asmgen. unfold preg_of.
+      apply preg_of_not_X29; auto.
+
+  (* X29 does not contain parent *)
+    + rewrite chunk_of_Tptr in A. 
+      exploit loadptr_correct. eexact A. discriminate. intros [rs2 [P [Q R]]].
+      exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto.
+      discriminate.
+      intros [rs3 [S [T U]]].
+
+      exploit exec_straight_trans.
+        eapply P.
+        eapply S.
+      intros EXES.
+
+      eapply exec_straight_body in EXES.
+      destruct EXES as (l & ll & EXECB).
+      exists rs3, 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. }
+      subst.
+      eapply match_codestate_intro; eauto.
+      eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
+      instantiate (1 := rs2#X29 <- (rs3#X29)). intros.
+      rewrite Pregmap.gso; auto with asmgen.
+      congruence.
+      intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
+      simpl; intros. rewrite U; auto with asmgen.
+      apply preg_of_not_X29; auto.
+  - (* MBop *)
+    simpl in EQ0. rewrite Hheader in DXP.
+    
+    assert (eval_operation tge sp op (map ms args) m' = Some v).
+      rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
+    exploit eval_operation_lessdef.
+      eapply preg_vals; eauto.
+      2: eexact H0.
+      all: eauto.
+    intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+    exploit transl_op_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).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+    subst.
+    eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
+    apply agree_set_undef_mreg with rs1; auto. 
+    apply Val.lessdef_trans with v'; auto.
+    simpl; intros. destruct (andb_prop _ _ H1); clear H1.
+    rewrite R; auto. apply preg_of_not_X29; auto.
+Local Transparent destroyed_by_op.
+    destruct op; simpl; auto; try discriminate.
+  - (* MBload *)
+    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 Mem.loadv_extends; eauto. intros [v' [C D]]. destruct trap; try discriminate.
+    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).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+    subst.
+    eapply match_codestate_intro; eauto.
+    eapply agree_set_mreg; eauto with asmgen.
+    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.
+
+    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.
+    assert (Val.lessdef (ms src) (rs1 (preg_of src))). eapply preg_val; eauto.
+    exploit Mem.storev_extends; eauto. intros [m2' [C D]].
+    exploit transl_store_correct; eauto. intros [rs2 [P Q]].
+
+    eapply exec_straight_body in P.
+    destruct P as (l & ll & EXECB).
+    exists rs2, m2', 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. }
+    subst.
+    eapply match_codestate_intro; eauto.
+    eapply agree_undef_regs; eauto with asmgen.
+    intro Hep. simpl in Hep. discriminate.
+Qed.
+
+Lemma exec_body_trans:
+  forall l l' rs0 m0 rs1 m1 rs2 m2,
+  exec_body lk tge l rs0 m0 = Next rs1 m1 ->
+  exec_body lk tge l' rs1 m1 = Next rs2 m2 ->
+  exec_body lk tge (l++l') rs0 m0 = Next rs2 m2.
+Proof.
+  induction l.
+  - simpl. induction l'. intros.
+    + simpl in *. congruence.
+    + intros. inv H. auto.
+  - intros until m2. intros EXEB1 EXEB2.
+    inv EXEB1. destruct (exec_basic _) eqn:EBI; try discriminate.
+    simpl. rewrite EBI. eapply IHl; eauto.
+Qed.
+
+Lemma exec_body_control:
+  forall b t rs1 m1 rs2 m2 rs3 m3 fn,
+  exec_body lk tge (body b) rs1 m1 = Next rs2 m2 ->
+  exec_exit tge fn (Ptrofs.repr (size b)) rs2 m2 (exit b) t rs3 m3 ->
+  exec_bblock lk tge fn b rs1 m1 t rs3 m3.
+Proof.
+  intros until fn. intros EXEB EXECTL.
+  econstructor; eauto.
+Qed.
+
+Inductive exec_header: codestate -> codestate -> Prop :=
+  | exec_header_cons: forall cs1,
+      exec_header cs1 {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1;
+                          pctl := pctl cs1; ep := (if pheader cs1 then ep cs1 else false); rem := rem cs1;
+                          cur := cur cs1 |}.
+
+(* Theorem (A) in the diagram, the easiest of all *)
+Theorem step_simu_header:
+  forall bb s fb sp c ms m rs1 m1 cs1,
+  pstate cs1 = (State rs1 m1) ->
+  match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
+  (exists cs1',
+       exec_header cs1 cs1'
+    /\ match_codestate fb (MB.State s fb sp (mb_remove_header bb::c) ms m) cs1').
+Proof.
+  intros until cs1. intros Hpstate MCS.
+  eexists. split; eauto.
+  econstructor; eauto.
+  inv MCS. simpl in *. inv Hpstate.
+  econstructor; eauto.
+Qed.
+
+(* Theorem (B) in the diagram, using step_simu_basic + induction on the Machblock body *)
+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 ->
+  (exists rs2 m2 cs2 ep,
+       cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := nil; pbody2 := pbody2 cs1;
+                pctl := pctl cs1; ep := ep; rem := rem cs1; cur := cur cs1 |}
+    /\ exec_body lk tge (pbody1 cs1) rs1 m1 = Next rs2 m2
+    /\ 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.
+    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.
+    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.
+    intros (rs3 & m3 & cs3 & ep & Hcs3 & EXEB' & MCS'').
+    exists rs3, m3, cs3, ep.
+    repeat (split; simpl; auto). subst. simpl in *. auto.
+    rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto.
+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':
@@ -543,8 +1420,7 @@ Proof.
     assert (exists rs1 m1, pstate cs1 = State rs1 m1). { inv MAS. simpl. eauto. }
     destruct H as (rs1 & m1 & Hpstate2). subst.
     assert (f = fb). { inv MCS. auto. } subst fb.
-    all: admit.
-    (*exploit step_simu_header.
+    exploit step_simu_header.
       2: eapply MCS.
       all: eauto.
     intros (cs1' & EXEH & MCS2).
@@ -561,15 +1437,11 @@ Proof.
     assert (exists tf, Genv.find_funct_ptr tge f = Some (Internal tf)).
     { exploit functions_translated; eauto. intros (tf & FIND' & TRANSF'). monadInv TRANSF'. eauto. }
     destruct H as (tf & FIND').
-    assert (exists tex, pbody2 cs1 = extract_basic tex /\ pctl cs1 = extract_ctl tex).
-    { inv MAS. simpl in *. eauto. }
-    destruct H as (tex & Hpbody2 & Hpctl).
     inv EXEH. simpl in *.
     subst. exploit step_simu_control.
       9: eapply MCS'. all: simpl.
       10: eapply ESTEP.
       all: simpl; eauto.
-      rewrite Hpbody2. rewrite Hpctl.
       { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto.
         erewrite exec_body_pc; eauto. }
     intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS').
@@ -580,14 +1452,14 @@ Proof.
       eauto.
     intros EXEB2.
     exploit exec_body_control; eauto.
-    rewrite <- Hpbody2 in EXEB2. rewrite <- Hbody in EXEB2. eauto.
-    rewrite Hexit. rewrite Hpctl. eauto.
-    intros EXECB. inv EXECB.
+    rewrite <- Hbody in EXEB2. eauto.
+    rewrite Hexit. eauto.
+    intros EXECB. (* inv EXECB. *)
     exists (State rs4 m4).
     split; auto. eapply plus_one. rewrite Hpstate2.
     assert (exists ofs, rs1 PC = Vptr f ofs).
     { rewrite Hpstate2 in MAS. inv MAS. simpl in *. eauto. }
-    destruct H0 as (ofs & Hrs1pc).
+    destruct H as (ofs & Hrs1pc).
     eapply exec_step_internal; eauto.
 
     (* proving the initial find_bblock *)
@@ -595,10 +1467,10 @@ 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''. rewrite TRANSF0 in EQ. inv EQ.
+    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.
     eapply find_bblock_tail; eauto.
-Qed.*)
-Admitted.
+Qed.
 
 Theorem step_simulation_bblock:
   forall sf f sp bb ms m ms' m' S2 c,
@@ -616,6 +1488,106 @@ 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) ->
+  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'.
+Proof.
+  intros until S2. intros Hbody Hexit ESTEP S1' MS.
+  inv MS. inv AT. monadInv H2. monadInv EQ.
+  rewrite Hbody in EQ. monadInv EQ.
+  rewrite Hexit in EQ0. monadInv EQ0.
+  rewrite Hexit in ESTEP. inv ESTEP. inv H4.
+
+  exploit functions_transl; eauto. intro FN.
+  generalize (transf_function_no_overflow _ _ H1); intro NOOV.
+  exploit builtin_args_match; eauto. intros [vargs' [P Q]].
+  exploit external_call_mem_extends; eauto.
+  intros [vres' [m2' [A [B [C D]]]]].
+  econstructor; split. apply plus_one.
+  simpl in H3.
+  eapply exec_step_internal. eauto. eauto.
+    eapply find_bblock_tail; eauto.
+    simpl. econstructor. eexists. simpl. split; eauto.
+    econstructor.
+    erewrite <- sp_val by eauto.
+    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+    eauto.
+  econstructor; eauto.
+    instantiate (2 := tf); instantiate (1 := x0).
+    unfold incrPC. rewrite Pregmap.gss.
+    rewrite set_res_other. rewrite undef_regs_other_2.
+    rewrite <- H. simpl. econstructor; eauto.
+    eapply code_tail_next_int; 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.
+    congruence.
+Qed.
+
 (* Measure to prove finite stuttering, see the other backends *)
 Definition measure (s: MB.state) : nat :=
   match s with
@@ -631,26 +1603,23 @@ 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.
-  induction 1; intros.
+Proof. Admitted.
+(*  induction 1; intros.
 
 - (* bblock *)
   left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0.
-  all: admit.
-all: admit.
-Admitted.
-  (*all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; 
+  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.
+    * (* 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.
+(*       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.
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 69d6037c..4a35485e 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -6,6 +6,7 @@
 (*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
 (*           David Monniaux     CNRS, VERIMAG                  *)
 (*           Cyril Six          Kalray                         *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
 (*                                                             *)
 (*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
 (*  This file is distributed under the terms of the INRIA      *)
@@ -44,6 +45,52 @@ Module AB:=Asmblock.
 
 (** * Agreement between Mach registers and processor registers *)
 
+Hint Extern 2 (_ <> _) => congruence: asmgen.
+
+Lemma ireg_of_eq:
+  forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
+Proof.
+  unfold ireg_of; intros. destruct (preg_of r) as [[[rr1|]|]|xsp|]; inv H; auto.
+Qed.
+
+Lemma freg_of_eq:
+  forall r r', freg_of r = OK r' -> preg_of r = FR r'.
+Proof.
+  unfold freg_of; intros. destruct (preg_of r) as [[fr|]|xsp|]; inv H; auto.
+Qed.
+
+Lemma ireg_of_eq':
+  forall r r', ireg_of r = OK r' -> dreg_of r = IR r'.
+Proof.
+  unfold ireg_of; intros. destruct r; simpl in *; inv H; auto.
+Qed.
+
+Lemma freg_of_eq':
+  forall r r', freg_of r = OK r' -> dreg_of r = FR r'.
+Proof.
+  unfold freg_of; intros. destruct r; simpl in *; inv H; auto.
+Qed.
+
+Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop :=
+  match rl with
+  | nil => True
+  | r1 :: nil => r <> preg_of r1
+  | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl
+  end.
+
+Remark preg_notin_charact:
+  forall r rl,
+  preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr).
+Proof.
+  induction rl; simpl; intros.
+  tauto.
+  destruct rl.
+  simpl. split. intros. intuition congruence. auto.
+  rewrite IHrl. split.
+  intros [A B]. intros. destruct H. congruence. auto.
+  auto.
+Qed.
+
 Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree {
   agree_sp: rs#SP = sp;
   agree_sp_def: sp <> Vundef;
@@ -67,6 +114,184 @@ Proof.
   intros. destruct H. auto.
 Qed.
 
+Lemma preg_vals:
+  forall ms sp rs, agree ms sp rs ->
+  forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)).
+Proof.
+  induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto.
+Qed.
+
+Lemma preg_of_injective:
+  forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
+Proof.
+  destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
+Qed.
+
+Lemma sp_val:
+  forall ms sp rs, agree ms sp rs -> sp = rs#SP.
+Proof.
+  intros. destruct H; auto.
+Qed.
+
+Lemma ireg_val:
+  forall ms sp rs r r',
+  agree ms sp rs ->
+  ireg_of r = OK r' ->
+  Val.lessdef (ms r) rs#r'.
+Proof.
+  intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto.
+Qed.
+
+Lemma preg_of_not_X29: forall dst,
+  negb (mreg_eq dst R29) = true ->
+  DR (IR X29) <> preg_of dst.
+Proof.
+  intros. destruct dst; try discriminate.
+Qed.
+
+Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
+
+(** Preservation of register agreement under various assignments. *)
+
+Lemma agree_set_mreg:
+  forall ms sp rs r v rs',
+  agree ms sp rs ->
+  Val.lessdef v (rs'#(preg_of r)) ->
+  (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Mach.Regmap.set r v ms) sp rs'.
+Proof.
+  intros. destruct H. split; auto.
+  rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP.
+  intros. unfold Mach.Regmap.set. destruct (Mach.RegEq.eq r0 r). congruence.
+  rewrite H1. auto. apply preg_of_data.
+  red; intros; elim n. eapply preg_of_injective; eauto.
+Qed.
+
+Lemma agree_set_other:
+  forall ms sp rs r v,
+  agree ms sp rs ->
+  data_preg r = false ->
+  agree ms sp (rs#r <- v).
+Proof.
+  intros. apply agree_exten with rs. auto.
+  intros. apply Pregmap.gso. congruence.
+Qed.
+
+Lemma agree_nextblock:
+  forall ms sp rs b,
+  agree ms sp rs -> agree ms sp (incrPC (Ptrofs.repr (size b)) rs).
+Proof.
+  intros. unfold incrPC. apply agree_set_other. auto. auto.
+Qed.
+
+Lemma agree_set_res:
+  forall res ms sp rs v v',
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.set_res res v ms) sp (set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v' rs).
+Proof.
+  induction res; simpl; intros.
+- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto.
+  intros. apply Pregmap.gso; auto.
+- auto.
+- apply IHres2. apply IHres1. auto.
+  apply Val.hiword_lessdef; auto.
+  apply Val.loword_lessdef; auto.
+Qed.
+
+Lemma agree_undef_regs:
+  forall ms sp rl rs rs',
+  agree ms sp rs ->
+  (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') ->
+  agree (Mach.undef_regs rl ms) sp rs'.
+Proof.
+  intros. destruct H. split; auto.
+  rewrite <- agree_sp0. apply H0; auto.
+  rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP.
+  intros. destruct (In_dec mreg_eq r rl).
+  rewrite Mach.undef_regs_same; auto.
+  rewrite Mach.undef_regs_other; auto. rewrite H0; auto.
+  apply preg_of_data.
+  rewrite preg_notin_charact. intros; red; intros. elim n.
+  exploit preg_of_injective; eauto. congruence.
+Qed.
+
+Lemma agree_set_undef_mreg:
+  forall ms sp rs r v rl rs',
+  agree ms sp rs ->
+  Val.lessdef v (rs'#(preg_of r)) ->
+  (forall r', data_preg r' = true -> r' <> preg_of r -> preg_notin r' rl -> rs'#r' = rs#r') ->
+  agree (Mach.Regmap.set r v (Mach.undef_regs rl ms)) sp rs'.
+Proof.
+  intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto.
+  apply agree_undef_regs with rs; auto.
+  intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of r)).
+  congruence. auto.
+  intros. rewrite Pregmap.gso; auto.
+Qed.
+
+Lemma agree_change_sp:
+  forall ms sp rs sp',
+  agree ms sp rs -> sp' <> Vundef ->
+  agree ms sp' (rs#SP <- sp').
+Proof.
+  intros. inv H. split; auto.
+  intros. rewrite Pregmap.gso; auto with asmgen.
+Qed.
+
+Remark builtin_arg_match:
+  forall ge (rs: regset) sp m a v,
+  eval_builtin_arg ge (fun r => rs (dreg_of r)) sp m a v ->
+  eval_builtin_arg ge (fun r => rs (DR r)) sp m (map_builtin_arg dreg_of a) v.
+Proof.
+  induction 1; simpl; eauto with barg. econstructor.
+Qed.
+
+Lemma builtin_args_match:
+  forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall al vl, eval_builtin_args ge ms sp m al vl ->
+  exists vl', eval_builtin_args ge (fun r => rs (DR r)) sp m' (map (map_builtin_arg dreg_of) al) vl'
+           /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; intros; simpl.
+  exists (@nil val); split; constructor.
+  exploit (@eval_builtin_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto.
+  intros; eapply preg_val; eauto.
+  intros (v1' & A & B).
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto.
+Qed.
+
+Lemma set_res_other:
+  forall r res v rs,
+  data_preg r = false ->
+  set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v rs r = rs r.
+Proof.
+  induction res; simpl; intros.
+- apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate.
+- auto.
+- rewrite IHres2, IHres1; auto.
+Qed.
+
+Lemma undef_regs_other:
+  forall r rl rs,
+  (forall r', In r' rl -> r <> r') ->
+  undef_regs rl rs r = rs r.
+Proof.
+  induction rl; simpl; intros. auto.
+  rewrite IHrl by auto. rewrite Pregmap.gso; auto.
+Qed.
+
+Lemma undef_regs_other_2:
+  forall r rl rs,
+  preg_notin r rl ->
+  undef_regs (map preg_of rl) rs r = rs r.
+Proof.
+  intros. apply undef_regs_other. intros.
+  exploit list_in_map_inv; eauto. intros [mr [A B]]. subst.
+  rewrite preg_notin_charact in H. auto.
+Qed.
+
 Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
   | code_tail_0: forall c,
       code_tail 0 c c
@@ -156,6 +381,45 @@ Proof.
   - rewrite Ptrofs.unsigned_repr; omega.
 Qed.
 
+(** The [find_label] function returns the code tail starting at the
+  given label.  A connection with [code_tail] is then established. *)
+
+Fixpoint find_label (lbl: label) (c: bblocks) {struct c} : option bblocks :=
+  match c with
+  | nil => None
+  | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl
+  end.
+
+(* inspired from Mach *)
+
+Lemma find_label_tail:
+  forall lbl c c', MB.find_label lbl c = Some c' -> is_tail c' c.
+Proof.
+  induction c; simpl; intros. discriminate.
+  destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib.
+Qed.
+
+Lemma label_pos_code_tail:
+  forall lbl c pos c',
+  find_label lbl c = Some c' ->
+  exists pos',
+  label_pos lbl pos c = Some pos'
+  /\ code_tail (pos' - pos) c c'
+  /\ pos <= pos' <= pos + size_blocks c.
+Proof.
+  induction c.
+  simpl; intros. discriminate.
+  simpl; intros until c'.
+  case (is_label lbl a).
+  - intros. inv H. exists pos. split; auto. split.
+    replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
+    generalize (size_blocks_pos c). generalize (size_positive a). omega.
+  - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
+  exists pos'. split. auto. split.
+  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
+  constructor. auto. generalize (size_positive a). omega.
+Qed.
+
 (** Predictor for return addresses in generated Asm code.
 
   The [return_address_offset] predicate defined here is used in the
@@ -282,6 +546,129 @@ Proof.
   congruence.
 Qed.
 
+Section STRAIGHTLINE.
+
+Variable ge: genv.
+Variable lk: aarch64_linker.
+Variable fn: function.
+
+(** Straight-line code is composed of processor instructions that execute
+  in sequence (no branches, no function calls and returns).
+  The following inductive predicate relates the machine states
+  before and after executing a straight-line sequence of instructions.
+  Instructions are taken from the first list instead of being fetched
+  from memory. *)
+
+Inductive exec_straight: list basic -> regset -> mem ->
+                         list basic -> regset -> mem -> Prop :=
+  | exec_straight_one:
+      forall i1 c rs1 m1 rs2 m2,
+      exec_basic lk ge i1 rs1 m1 = Next rs2 m2 ->
+      exec_straight (i1 :: c) rs1 m1 c rs2 m2
+  | exec_straight_step:
+      forall i c rs1 m1 rs2 m2 c' rs3 m3,
+      exec_basic lk ge i rs1 m1 = Next rs2 m2 ->
+      exec_straight c rs2 m2 c' rs3 m3 ->
+      exec_straight (i :: c) rs1 m1 c' rs3 m3.
+
+Lemma exec_straight_trans:
+  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
+  exec_straight c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight c1 rs1 m1 c3 rs3 m3.
+Proof.
+  induction 1; intros.
+  apply exec_straight_step with rs2 m2; auto.
+  apply exec_straight_step with rs2 m2; auto.
+Qed.
+
+Lemma exec_straight_two:
+  forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
+  exec_basic lk ge i1 rs1 m1 = Next rs2 m2 ->
+  exec_basic lk ge i2 rs2 m2 = Next rs3 m3 ->
+  exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  apply exec_straight_one; auto.
+Qed.
+
+Lemma exec_straight_three:
+  forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
+  exec_basic lk ge i1 rs1 m1 = Next rs2 m2 ->
+  exec_basic lk ge i2 rs2 m2 = Next rs3 m3 ->
+  exec_basic lk ge i3 rs3 m3 = Next rs4 m4 ->
+  exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  eapply exec_straight_two; eauto.
+Qed.
+
+Inductive exec_straight_opt: list basic -> regset -> mem -> list basic -> regset -> mem -> Prop :=
+  | exec_straight_opt_refl: forall c rs m,
+      exec_straight_opt c rs m c rs m
+  | exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2,
+      exec_straight c1 rs1 m1 c2 rs2 m2 ->
+      exec_straight_opt c1 rs1 m1 c2 rs2 m2.
+
+Remark exec_straight_opt_right:
+  forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2,
+  exec_straight_opt c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight c1 rs1 m1 c3 rs3 m3.
+Proof.
+  destruct 1; intros. auto. eapply exec_straight_trans; eauto. 
+Qed.
+
+Lemma exec_straight_opt_step:
+  forall i c rs1 m1 rs2 m2 c' rs3 m3,
+  exec_basic lk ge i rs1 m1 = Next rs2 m2 ->
+  exec_straight_opt c rs2 m2 c' rs3 m3 ->
+  exec_straight (i :: c) rs1 m1 c' rs3 m3.
+Proof.
+  intros. inv H0.
+- apply exec_straight_one; auto.
+- eapply exec_straight_step; eauto.
+Qed.
+
+Lemma exec_straight_opt_step_opt:
+  forall i c rs1 m1 rs2 m2 c' rs3 m3,
+  exec_basic lk ge i rs1 m1 = Next rs2 m2 ->
+  exec_straight_opt c rs2 m2 c' rs3 m3 ->
+  exec_straight_opt (i :: c) rs1 m1 c' rs3 m3.
+Proof.
+  intros. apply exec_straight_opt_intro. eapply exec_straight_opt_step; eauto.
+Qed.
+
+(** Linking exec_straight with exec_straight_blocks *)
+
+(* Lemma exec_straight_pc:
+  forall c c' rs1 m1 rs2 m2,
+  exec_straight c rs1 m1 c' rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  induction c; intros; try (inv H; fail).
+  inv H.
+  - eapply exec_basic_instr_pc; eauto.
+  - rewrite (IHc c' rs3 m3 rs2 m2); auto.
+    erewrite exec_basic_instr_pc; eauto.
+Qed. *)
+
+Lemma exec_body_pc:
+  forall ge l rs1 m1 rs2 m2,
+  exec_body lk ge l rs1 m1 = Next rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  induction l.
+  - intros. inv H. auto.
+  - intros until m2. intro EXEB.
+    inv EXEB. destruct (exec_basic _ _ _ _ _) eqn:EBI; try discriminate.
+    eapply IHl in H0. rewrite H0.
+    destruct s.
+    erewrite exec_basic_instr_pc; eauto.
+Qed.
+
+End STRAIGHTLINE.
+
 (** * Properties of the Machblock call stack *)
 
 Section MATCH_STACK.
diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v
new file mode 100644
index 00000000..bc4302ca
--- /dev/null
+++ b/aarch64/Asmblockgenproof1.v
@@ -0,0 +1,1834 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** * Proof of correctness for individual instructions *)
+
+Require Import Coqlib Errors Maps Zbits.
+Require Import AST Integers Floats Values Memory Globalenvs Linking.
+Require Import Op Locations Machblock Conventions.
+Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
+
+Module MB := Machblock.
+Module AB := Asmblock.
+
+Section CONSTRUCTORS.
+
+Variable lk: aarch64_linker.
+Variable ge: genv.
+Variable fn: function.
+
+Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
+  Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address ge id ofs.
+
+Ltac Simplif :=
+  ((rewrite Pregmap.gss)
+  || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen.
+
+Ltac Simpl := repeat Simplif.
+
+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).
+  
+Ltac SimplEval H :=
+  match type of H with
+  | Some _ = None _ => discriminate
+  | Some _ = Some _ => inversion H; subst
+  | ?a = Some ?b => let A := fresh in assert (A: Val.maketotal a = b) by (rewrite H; reflexivity)
+end.
+
+Ltac TranslOpSimpl :=
+  econstructor; split;
+  [ apply exec_straight_one; reflexivity
+  | split; [ apply Val.lessdef_same; simpl; Simpl; fail | intros; simpl; Simpl; fail ] ].
+
+Ltac TranslOpSimplN :=
+  econstructor; split;
+  try apply exec_straight_one; try reflexivity; try split; try apply Val.lessdef_same;
+  Simpl; simpl; try destruct negb; Simpl; try intros; Simpl; simpl; try destruct negb; Simpl.
+
+Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC.
+Proof.
+  destruct r; simpl; try discriminate.
+Qed.
+Hint Resolve preg_of_iregsp_not_PC: asmgen.
+
+Lemma preg_of_not_X16: forall r, preg_of r <> X16.
+Proof.
+  destruct r; simpl; try discriminate.
+Qed.
+
+Lemma preg_of_not_X30: forall r, preg_of r <> X30.
+Proof.
+  destruct r; simpl; try discriminate.
+Qed.
+
+Lemma ireg_of_not_X16: forall r x, ireg_of r = OK x -> x <> X16.
+Proof.
+  unfold ireg_of; intros. destruct (preg_of r) eqn:E; inv H.
+  red; intros; subst x. elim (preg_of_not_X16 r); auto.
+  destruct d. destruct i. inv H1; auto.
+  all: discriminate.
+Qed.
+
+Lemma ireg_of_not_X16': forall r x, ireg_of r = OK x -> IR x <> IR X16.
+Proof.
+  intros. apply ireg_of_not_X16 in H. congruence.
+Qed.
+
+Lemma ireg_of_not_X16'': forall r x, ireg_of r = OK x -> DR (IR x) <> DR (IR X16).
+Proof.
+  intros. apply ireg_of_not_X16 in H. congruence.
+Qed.
+
+Lemma ireg_of_not_X30: forall r x, ireg_of r = OK x -> x <> X30.
+Proof.
+  unfold ireg_of; intros. destruct (preg_of r) eqn:E; inv H.
+  red; intros; subst x. elim (preg_of_not_X30 r); auto.
+  destruct d. destruct i. inv H1; auto.
+  all: discriminate.
+Qed.
+
+Lemma ireg_of_not_X30': forall r x, ireg_of r = OK x -> IR x <> IR X30.
+Proof.
+  intros. apply ireg_of_not_X30 in H. congruence.
+Qed.
+
+Lemma ireg_of_not_X30'': forall r x, ireg_of r = OK x -> DR (IR x) <> DR (IR X30).
+Proof.
+  intros. apply ireg_of_not_X30 in H. congruence.
+Qed.
+
+Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16' ireg_of_not_X16'': asmgen.
+Hint Resolve preg_of_not_X30 ireg_of_not_X30 ireg_of_not_X30' ireg_of_not_X30'': asmgen.
+
+Inductive wf_decomposition: list (Z * Z) -> Prop :=
+  | wf_decomp_nil:
+      wf_decomposition nil
+  | wf_decomp_cons: forall m n p l,
+      n = Zzero_ext 16 m -> 0 <= p -> wf_decomposition l ->
+      wf_decomposition ((n, p) :: l).
+
+Lemma decompose_int_wf:
+  forall N n p, 0 <= p -> wf_decomposition (decompose_int N n p).
+Proof.
+Local Opaque Zzero_ext.
+  induction N as [ | N]; simpl; intros.
+- constructor.
+- set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0).
++ apply IHN. omega.
++ econstructor. reflexivity. omega. apply IHN; omega. 
+Qed.
+
+Fixpoint recompose_int (accu: Z) (l: list (Z * Z)) : Z :=
+  match l with
+  | nil => accu
+  | (n, p) :: l => recompose_int (Zinsert accu n p 16) l
+  end.
+
+Lemma decompose_int_correct:
+  forall N n p accu,
+  0 <= p ->
+  (forall i, p <= i -> Z.testbit accu i = false) ->
+  (forall i, 0 <= i < p + Z.of_nat N * 16 ->
+   Z.testbit (recompose_int accu (decompose_int N n p)) i =
+   if zlt i p then Z.testbit accu i else Z.testbit n i).
+Proof.
+  induction N as [ | N]; intros until accu; intros PPOS ABOVE i RANGE.
+- simpl. rewrite zlt_true; auto. xomega.
+- rewrite inj_S in RANGE. simpl.
+  set (frag := Zzero_ext 16 (Z.shiftr n p)).
+  assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)).
+  { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega.
+    rewrite Z.shiftr_spec by omega. f_equal; omega. }
+  destruct (Z.eqb_spec frag 0).
++ rewrite IHN.
+* destruct (zlt i p). rewrite zlt_true by omega. auto.
+  destruct (zlt i (p + 16)); auto.
+  rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto.
+* omega.
+* intros; apply ABOVE; omega.
+* xomega.
++ simpl. rewrite IHN.
+* destruct (zlt i (p + 16)).
+** rewrite Zinsert_spec by omega. unfold proj_sumbool.
+   rewrite zlt_true by omega.
+   destruct (zlt i p).
+   rewrite zle_false by omega. auto.
+   rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega.
+** rewrite Z.ldiff_spec, Z.shiftl_spec by omega.
+   change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega.
+   rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. 
+* omega.
+* intros. rewrite Zinsert_spec by omega. unfold proj_sumbool.
+  rewrite zle_true by omega. rewrite zlt_false by omega. simpl.
+  apply ABOVE. omega.
+* xomega.
+Qed.
+
+Corollary decompose_int_eqmod: forall N n,
+  eqmod (two_power_nat (N * 16)%nat) (recompose_int 0 (decompose_int N n 0)) n.
+Proof.
+  intros; apply eqmod_same_bits; intros.
+  rewrite decompose_int_correct. apply zlt_false; omega. 
+  omega. intros; apply Z.testbit_0_l. xomega.
+Qed.
+
+Corollary decompose_notint_eqmod: forall N n,
+  eqmod (two_power_nat (N * 16)%nat)
+        (Z.lnot (recompose_int 0 (decompose_int N (Z.lnot n) 0))) n.
+Proof.
+  intros; apply eqmod_same_bits; intros.
+  rewrite Z.lnot_spec, decompose_int_correct.
+  rewrite zlt_false by omega. rewrite Z.lnot_spec by omega. apply negb_involutive.
+  omega. intros; apply Z.testbit_0_l. xomega. omega.
+Qed.
+
+Lemma negate_decomposition_wf:
+  forall l, wf_decomposition l -> wf_decomposition (negate_decomposition l).
+Proof.
+  induction 1; simpl; econstructor; auto.
+  instantiate (1 := (Z.lnot m)).
+  apply equal_same_bits; intros.
+  rewrite H. change 65535 with (two_p 16 - 1).
+  rewrite Z.lxor_spec, !Zzero_ext_spec, Z.lnot_spec, Ztestbit_two_p_m1 by omega.
+  destruct (zlt i 16).
+  apply xorb_true_r.
+  auto.
+Qed.
+
+Lemma Zinsert_eqmod:
+  forall n x1 x2 y p l, 0 <= p -> 0 <= l ->
+  eqmod (two_power_nat n) x1 x2 ->
+  eqmod (two_power_nat n) (Zinsert x1 y p l) (Zinsert x2 y p l).
+Proof.
+  intros. apply eqmod_same_bits; intros. rewrite ! Zinsert_spec by omega.
+  destruct (zle p i && zlt i (p + l)); auto.
+  apply same_bits_eqmod with n; auto.
+Qed.
+
+Lemma Zinsert_0_l:
+  forall y p l,
+  0 <= p -> 0 <= l ->
+  Z.shiftl (Zzero_ext l y) p = Zinsert 0 (Zzero_ext l y) p l.
+Proof.
+  intros. apply equal_same_bits; intros.
+  rewrite Zinsert_spec by omega. unfold proj_sumbool.
+  destruct (zlt i p); [rewrite zle_false by omega|rewrite zle_true by omega]; simpl.
+- rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto.
+- rewrite Z.shiftl_spec by omega. 
+  destruct (zlt i (p + l)); auto.
+  rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto.
+Qed.
+
+Lemma recompose_int_negated:
+  forall l, wf_decomposition l ->
+  forall accu, recompose_int (Z.lnot accu) (negate_decomposition l) = Z.lnot (recompose_int accu l).
+Proof.
+  induction 1; intros accu; simpl.
+- auto.
+- rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. 
+  rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega.
+  unfold proj_sumbool.
+  destruct (zle p i); simpl; auto.
+  destruct (zlt i (p + 16)); simpl; auto.
+  change 65535 with (two_p 16 - 1).
+  rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega.
+  apply xorb_true_r. 
+Qed.
+
+Lemma exec_loadimm_k_w:
+  forall (rd: ireg) k m l,
+  wf_decomposition l ->
+  forall (rs: regset) accu,
+  rs#rd = Vint (Int.repr accu) ->
+  exists rs',
+     exec_straight_opt ge lk (loadimm_k W rd l k) rs m k rs' m
+  /\ rs'#rd = Vint (Int.repr (recompose_int accu l))
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  induction 1; intros rs accu ACCU; simpl.
+- exists rs; split. apply exec_straight_opt_refl. auto.
+- destruct (IHwf_decomposition
+                ((rs#rd <- (insert_in_int rs#rd n p 16)))
+                (Zinsert accu n p 16))
+  as (rs' & P & Q & R).
+  Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. 
+  apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+  exists rs'; split.
+  eapply exec_straight_opt_step_opt. simpl. eauto. auto.
+  split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
+Qed.
+
+Lemma exec_loadimm_z_w:
+  forall rd l k rs m,
+  wf_decomposition l ->
+  exists rs',
+     exec_straight ge lk (loadimm_z W rd l k) rs m k rs' m
+  /\ rs'#rd = Vint (Int.repr (recompose_int 0 l))
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold loadimm_z; destruct 1.
+- econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl.
+  intros; Simpl.
+- set (accu0 := Zinsert 0 n p 16).
+  set (rs1 := rs#rd <- (Vint (Int.repr accu0))).
+  destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
+  unfold rs1; Simpl.
+  exists rs2; split.
+  eapply exec_straight_opt_step; eauto.
+  simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
+  split. exact Q. 
+  intros. rewrite R by auto. unfold rs1; Simpl.
+Qed.
+
+Lemma exec_loadimm_n_w:
+  forall rd l k rs m,
+  wf_decomposition l ->
+  exists rs',
+     exec_straight ge lk (loadimm_n W rd l k) rs m k rs' m
+  /\ rs'#rd = Vint (Int.repr (Z.lnot (recompose_int 0 l)))
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold loadimm_n; destruct 1.
+- econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. 
+  intros; Simpl.
+- set (accu0 := Z.lnot (Zinsert 0 n p 16)).
+  set (rs1 := rs#rd <- (Vint (Int.repr accu0))).
+  destruct (exec_loadimm_k_w rd k m (negate_decomposition l) 
+                                    (negate_decomposition_wf l H1)
+                                    rs1 accu0) as (rs2 & P & Q & R).
+  unfold rs1; Simpl.
+  exists rs2; split.
+  eapply exec_straight_opt_step; eauto.
+  simpl. unfold rs1. do 5 f_equal.
+  unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
+  split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
+  intros. rewrite R by auto. unfold rs1; Simpl.
+Qed.
+
+Lemma exec_loadimm32:
+  forall rd n k rs m,
+  exists rs',
+     exec_straight ge lk (loadimm32 rd n k) rs m k rs' m
+  /\ rs'#rd = Vint n
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold loadimm32, loadimm; intros.
+  destruct (is_logical_imm32 n).
+- econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. rewrite Int.repr_unsigned, Int.or_zero_l; auto.
+  intros; Simpl.
+- set (dz := decompose_int 2%nat (Int.unsigned n) 0).
+  set (dn := decompose_int 2%nat (Z.lnot (Int.unsigned n)) 0).
+  assert (A: Int.repr (recompose_int 0 dz) = n).
+  { transitivity (Int.repr (Int.unsigned n)).
+    apply Int.eqm_samerepr. apply decompose_int_eqmod. 
+    apply Int.repr_unsigned. }
+  assert (B: Int.repr (Z.lnot (recompose_int 0 dn)) = n).
+  { transitivity (Int.repr (Int.unsigned n)).
+    apply Int.eqm_samerepr. apply decompose_notint_eqmod. 
+    apply Int.repr_unsigned. }
+  destruct Nat.leb.
++ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega.
++ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega.
+Qed.
+
+Lemma exec_loadimm_k_x:
+  forall (rd: ireg) k m l,
+  wf_decomposition l ->
+  forall (rs: regset) accu,
+  rs#rd = Vlong (Int64.repr accu) ->
+  exists rs',
+     exec_straight_opt ge lk (loadimm_k X rd l k) rs m k rs' m
+  /\ rs'#rd = Vlong (Int64.repr (recompose_int accu l))
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  induction 1; intros rs accu ACCU; simpl.
+- exists rs; split. apply exec_straight_opt_refl. auto.
+- destruct (IHwf_decomposition
+                (rs#rd <- (insert_in_long rs#rd n p 16))
+                (Zinsert accu n p 16))
+  as (rs' & P & Q & R).
+  Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. 
+  apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
+  exists rs'; split.
+  eapply exec_straight_opt_step_opt. simpl; eauto. auto.
+  split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
+Qed.
+
+Lemma exec_loadimm_z_x:
+  forall rd l k rs m,
+  wf_decomposition l ->
+  exists rs',
+     exec_straight ge lk (loadimm_z X rd l k) rs m k rs' m
+  /\ rs'#rd = Vlong (Int64.repr (recompose_int 0 l))
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold loadimm_z; destruct 1.
+- econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl.
+  intros; Simpl.
+- set (accu0 := Zinsert 0 n p 16).
+  set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))).
+  destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
+  unfold rs1; Simpl.
+  exists rs2; split.
+  eapply exec_straight_opt_step; eauto.
+  simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
+  split. exact Q. 
+  intros. rewrite R by auto. unfold rs1; Simpl.
+Qed.
+
+Lemma exec_loadimm_n_x:
+  forall rd l k rs m,
+  wf_decomposition l ->
+  exists rs',
+     exec_straight ge lk (loadimm_n X rd l k) rs m k rs' m
+  /\ rs'#rd = Vlong (Int64.repr (Z.lnot (recompose_int 0 l)))
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold loadimm_n; destruct 1.
+- econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. 
+  intros; Simpl.
+- set (accu0 := Z.lnot (Zinsert 0 n p 16)).
+  set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))).
+  destruct (exec_loadimm_k_x rd k m (negate_decomposition l) 
+                                    (negate_decomposition_wf l H1)
+                                    rs1 accu0) as (rs2 & P & Q & R).
+  unfold rs1; Simpl.
+  exists rs2; split.
+  eapply exec_straight_opt_step; eauto.
+  simpl. unfold rs1. do 5 f_equal.
+  unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
+  split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
+  intros. rewrite R by auto. unfold rs1; Simpl.
+Qed.
+
+Lemma exec_loadimm64:
+  forall rd n k rs m,
+  exists rs',
+     exec_straight ge lk (loadimm64 rd n k) rs m k rs' m
+  /\ rs'#rd = Vlong n
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold loadimm64, loadimm; intros.
+  destruct (is_logical_imm64 n).
+- econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. rewrite Int64.repr_unsigned, Int64.or_zero_l; auto.
+  intros; Simpl.
+- set (dz := decompose_int 4%nat (Int64.unsigned n) 0).
+  set (dn := decompose_int 4%nat (Z.lnot (Int64.unsigned n)) 0).
+  assert (A: Int64.repr (recompose_int 0 dz) = n).
+  { transitivity (Int64.repr (Int64.unsigned n)).
+    apply Int64.eqm_samerepr. apply decompose_int_eqmod. 
+    apply Int64.repr_unsigned. }
+  assert (B: Int64.repr (Z.lnot (recompose_int 0 dn)) = n).
+  { transitivity (Int64.repr (Int64.unsigned n)).
+    apply Int64.eqm_samerepr. apply decompose_notint_eqmod. 
+    apply Int64.repr_unsigned. }
+  destruct Nat.leb.
++ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega.
++ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega.
+Qed.
+
+(** Add immediate *)
+
+Lemma exec_addimm_aux_32:
+  forall (insn: Z -> arith_pp) (sem: val -> val -> val),
+  (forall rd r1 n rs m,
+    exec_basic lk ge (PArith (PArithPP (insn n) rd r1)) rs m =
+      Next (rs#rd <- (sem rs#r1 (Vint (Int.repr n)))) m) ->
+  (forall v n1 n2, sem (sem v (Vint n1)) (Vint n2) = sem v (Vint (Int.add n1 n2))) ->
+  forall rd r1 n k rs m,
+  exists rs',
+     exec_straight ge lk (addimm_aux insn rd r1 (Int.unsigned n) k) rs m k rs' m
+  /\ rs'#rd = sem rs#r1 (Vint n)
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros insn sem SEM ASSOC; intros. unfold addimm_aux.
+  set (nlo := Zzero_ext 12 (Int.unsigned n)). set (nhi := Int.unsigned n - nlo).
+  assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega).
+  rewrite <- (Int.repr_unsigned n).
+  destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
+- econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
+  split. Simpl. do 3 f_equal; omega.
+  intros; Simpl.
+- econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
+  split. Simpl. do 3 f_equal; omega.
+  intros; Simpl.
+- econstructor; split. eapply exec_straight_two.
+  apply SEM. apply SEM. simpl. Simpl.
+  split. Simpl. simpl.  rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr.
+  rewrite E. auto with ints.
+  intros; Simpl.
+Qed.
+
+Lemma exec_addimm32:
+  forall (rd r1: ireg) n k rs m,
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (addimm32 rd r1 n k) rs m k rs' m
+  /\ rs'#rd = Val.add rs#r1 (Vint n)
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros. unfold addimm32. set (nn := Int.neg n).
+  destruct (Int.eq n (Int.zero_ext 24 n)); [| destruct (Int.eq nn (Int.zero_ext 24 nn))].
+- apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. 
+- rewrite <- Val.sub_opp_add.
+  apply exec_addimm_aux_32 with (sem := Val.sub). auto.
+  intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto.
+- destruct (Int.lt n Int.zero).
++ rewrite <- Val.sub_opp_add; fold nn.
+  edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. rewrite B, C; eauto with asmgen.
+  intros; Simpl.
++ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. rewrite B, C; eauto with asmgen.
+  intros; Simpl.
+Qed.
+
+Lemma exec_addimm_aux_64:
+  forall (insn: Z -> arith_pp) (sem: val -> val -> val),
+  (forall rd r1 n rs m,
+    exec_basic lk ge (PArith (PArithPP (insn n) rd r1)) rs m =
+      Next (rs#rd <- (sem rs#r1 (Vlong (Int64.repr n)))) m) ->
+  (forall v n1 n2, sem (sem v (Vlong n1)) (Vlong n2) = sem v (Vlong (Int64.add n1 n2))) ->
+  forall rd r1 n k rs m,
+  exists rs',
+     exec_straight ge lk (addimm_aux insn rd r1 (Int64.unsigned n) k) rs m k rs' m
+  /\ rs'#rd = sem rs#r1 (Vlong n)
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros insn sem SEM ASSOC; intros. unfold addimm_aux.
+  set (nlo := Zzero_ext 12 (Int64.unsigned n)). set (nhi := Int64.unsigned n - nlo).
+  assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; omega).
+  rewrite <- (Int64.repr_unsigned n).
+  destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
+- econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
+  split. Simpl. do 3 f_equal; omega.
+  intros; Simpl.
+- econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
+  split. Simpl. do 3 f_equal; omega.
+  intros; Simpl.
+- econstructor; split. eapply exec_straight_two.
+  apply SEM. apply SEM. Simpl. Simpl.
+  split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr.
+  rewrite E. auto with ints.
+  intros; Simpl.
+Qed.
+
+Lemma exec_addimm64:
+  forall (rd r1: iregsp) n k rs m,
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (addimm64 rd r1 n k) rs m k rs' m
+  /\ rs'#rd = Val.addl rs#r1 (Vlong n)
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros. 
+  unfold addimm64. set (nn := Int64.neg n).
+  destruct (Int64.eq n (Int64.zero_ext 24 n)); [| destruct (Int64.eq nn (Int64.zero_ext 24 nn))].
+- apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. 
+- rewrite <- Val.subl_opp_addl.
+  apply exec_addimm_aux_64 with (sem := Val.subl). auto.
+  intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto.
+- destruct (Int64.lt n Int64.zero).
++ rewrite <- Val.subl_opp_addl; fold nn.
+  edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. 
+  split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
+  intros; Simpl.
++ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. 
+  split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
+  intros; Simpl.
+Qed.
+
+(** Logical immediate *)
+
+Lemma exec_logicalimm32:
+  forall (insn1: Z -> arith_rr0)
+         (insn2: shift_op -> arith_rr0r)
+         (sem: val -> val -> val),
+  (forall rd r1 n rs m,
+    exec_basic lk ge (PArith (PArithRR0 (insn1 n) rd r1)) rs m =
+      Next (rs#rd <- (sem rs##r1 (Vint (Int.repr n)))) m) ->
+  (forall rd r1 r2 s rs m,
+    exec_basic lk ge (PArith (PArithRR0R (insn2 s) rd r1 r2)) rs m =
+      Next (rs#rd <- (sem rs##r1 (eval_shift_op_int rs#r2 s))) m) ->
+  forall rd r1 n k rs m,
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (logicalimm32 insn1 insn2 rd r1 n k) rs m k rs' m
+  /\ rs'#rd = sem rs#r1 (Vint n)
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32.
+  destruct (is_logical_imm32 n).
+- econstructor; split. 
+  apply exec_straight_one. apply SEM1.
+  split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl.
+- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A.  
+  apply exec_straight_one. apply SEM2.
+  split. Simpl. f_equal; auto. apply C; auto with asmgen.
+  intros; Simpl. 
+Qed.
+
+Lemma exec_logicalimm64:
+  forall (insn1: Z -> arith_rr0)
+         (insn2: shift_op -> arith_rr0r)
+         (sem: val -> val -> val),
+  (forall rd r1 n rs m,
+    exec_basic lk ge (PArith (PArithRR0 (insn1 n) rd r1)) rs m =
+      Next (rs#rd <- (sem rs###r1 (Vlong (Int64.repr n)))) m) ->
+  (forall rd r1 r2 s rs m,
+    exec_basic lk ge (PArith (PArithRR0R (insn2 s) rd r1 r2)) rs m =
+      Next (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s))) m) ->
+  forall rd r1 n k rs m,
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (logicalimm64 insn1 insn2 rd r1 n k) rs m k rs' m
+  /\ rs'#rd = sem rs#r1 (Vlong n)
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64.
+  destruct (is_logical_imm64 n).
+- econstructor; split. 
+  apply exec_straight_one. apply SEM1.
+  split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl.
+- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A.  
+  apply exec_straight_one. apply SEM2.
+  split. Simpl. f_equal; auto. apply C; auto with asmgen.
+  intros; Simpl. 
+Qed.
+
+(** Load address of symbol *)
+
+Lemma exec_loadsymbol: forall rd s ofs k rs m,
+  rd <> X16 \/ Archi.pic_code tt = false ->
+  exists rs',
+     exec_straight ge lk (loadsymbol rd s ofs k) rs m k rs' m
+  /\ rs'#rd = Genv.symbol_address ge s ofs
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold loadsymbol; intros. destruct (Archi.pic_code tt).
+- predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero.
++ subst ofs. econstructor; split.
+  apply exec_straight_one. simpl; eauto.
+  split. Simpl. intros; Simpl.
++ exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence.
+  intros (rs1 & A & B & C).
+  econstructor; split.
+  econstructor. simpl; eauto. auto. eexact A. 
+  split. simpl in B; rewrite B. Simpl. 
+  rewrite <- Genv.shift_symbol_address_64 by auto.
+  rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto.
+  intros. rewrite C by auto. Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
+  split. Simpl.
+  intros; Simpl.
+Qed.
+
+(** Shifted operands *)
+
+Remark transl_shift_not_none:
+  forall s a, transl_shift s a <> SOnone.
+Proof.
+  destruct s; intros; simpl; congruence.
+Qed.
+
+Remark or_zero_eval_shift_op_int:
+  forall v s, s <> SOnone -> Val.or (Vint Int.zero) (eval_shift_op_int v s) = eval_shift_op_int v s.
+Proof.
+  intros; destruct s; try congruence; destruct v; auto; simpl;
+  destruct (Int.ltu n Int.iwordsize); auto; rewrite Int.or_zero_l; auto.
+Qed.
+
+Remark or_zero_eval_shift_op_long:
+  forall v s, s <> SOnone -> Val.orl (Vlong Int64.zero) (eval_shift_op_long v s) = eval_shift_op_long v s.
+Proof.
+  intros; destruct s; try congruence; destruct v; auto; simpl;
+  destruct (Int.ltu n Int64.iwordsize'); auto; rewrite Int64.or_zero_l; auto.
+Qed.
+
+Remark add_zero_eval_shift_op_long:
+  forall v s, s <> SOnone -> Val.addl (Vlong Int64.zero) (eval_shift_op_long v s) = eval_shift_op_long v s.
+Proof.
+  intros; destruct s; try congruence; destruct v; auto; simpl;
+  destruct (Int.ltu n Int64.iwordsize'); auto; rewrite Int64.add_zero_l; auto.
+Qed.
+
+Lemma transl_eval_shift: forall s v (a: amount32),
+  eval_shift_op_int v (transl_shift s a) = eval_shift s v a.
+Proof.
+  intros. destruct s; simpl; auto.
+Qed.
+
+Lemma transl_eval_shift': forall s v (a: amount32),
+  Val.or (Vint Int.zero) (eval_shift_op_int v (transl_shift s a)) = eval_shift s v a.
+Proof.
+  intros. rewrite or_zero_eval_shift_op_int by (apply transl_shift_not_none).
+  apply transl_eval_shift.
+Qed.
+
+Lemma transl_eval_shiftl: forall s v (a: amount64),
+  eval_shift_op_long v (transl_shift s a) = eval_shiftl s v a.
+Proof.
+  intros. destruct s; simpl; auto.
+Qed.
+
+Lemma transl_eval_shiftl': forall s v (a: amount64),
+  Val.orl (Vlong Int64.zero) (eval_shift_op_long v (transl_shift s a)) = eval_shiftl s v a.
+Proof.
+  intros. rewrite or_zero_eval_shift_op_long by (apply transl_shift_not_none).
+  apply transl_eval_shiftl.
+Qed.
+
+Lemma transl_eval_shiftl'': forall s v (a: amount64),
+  Val.addl (Vlong Int64.zero) (eval_shift_op_long v (transl_shift s a)) = eval_shiftl s v a.
+Proof.
+  intros. rewrite add_zero_eval_shift_op_long by (apply transl_shift_not_none).
+  apply transl_eval_shiftl.
+Qed.
+
+(** Zero- and Sign- extensions *)
+
+Lemma exec_move_extended_base: forall rd r1 ex k rs m,
+  exists rs',
+     exec_straight ge lk (move_extended_base rd r1 ex k) rs m k rs' m
+  /\ rs' rd = match ex with Xsgn32 => Val.longofint rs#r1 | Xuns32 => Val.longofintu rs#r1 end
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold move_extended_base; destruct ex; econstructor;
+  (split; [apply exec_straight_one; simpl; eauto | split; [Simpl|intros;Simpl]]).
+Qed.
+
+Lemma exec_move_extended: forall rd r1 ex (a: amount64) k rs m,
+  exists rs',
+     exec_straight ge lk (move_extended rd r1 ex a k) rs m k rs' m
+  /\ rs' rd = Op.eval_extend ex rs#r1 a
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold move_extended; intros. predSpec Int.eq Int.eq_spec a Int.zero.
+- exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. unfold Op.eval_extend. rewrite H. rewrite B.
+  destruct ex, (rs r1); simpl; auto; rewrite Int64.shl'_zero; auto.
+  auto.
+- Local Opaque Val.addl.
+  exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  change (SOlsl a) with (transl_shift Slsl a). rewrite transl_eval_shiftl''. eauto. auto.
+  split. Simpl. rewrite B. auto. 
+  intros; Simpl.
+Qed.
+
+Lemma exec_arith_extended:
+  forall (sem: val -> val -> val)
+         (insnX: extend_op -> arith_ppp)
+         (insnS: shift_op -> arith_rr0r),
+  (forall rd r1 r2 x rs m,
+    exec_basic lk ge (PArith (PArithPPP (insnX x) rd r1 r2)) rs m =
+      Next (rs#rd <- (sem rs#r1 (eval_extend rs#r2 x))) m) ->
+  (forall rd r1 r2 s rs m,
+    exec_basic lk ge (PArith (PArithRR0R (insnS s) rd r1 r2)) rs m =
+      Next (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s))) m) ->
+  forall (rd r1 r2: ireg) (ex: extension) (a: amount64) (k: bcode) rs m,
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (arith_extended insnX insnS rd r1 r2 ex a k) rs m k rs' m
+  /\ rs'#rd = sem rs#r1 (Op.eval_extend ex rs#r2 a)
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros sem insnX insnS EX ES; intros. unfold arith_extended. destruct (Int.ltu a (Int.repr 5)).
+- econstructor; split. 
+  apply exec_straight_one. rewrite EX; eauto. auto.
+  split. Simpl. f_equal. destruct ex; auto.
+  intros; Simpl.
+- exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one. 
+  rewrite ES. eauto. auto.
+  split. Simpl. unfold ir0. rewrite C by eauto with asmgen. f_equal. 
+  rewrite B. destruct ex; auto.
+  intros; Simpl.
+Qed. 
+
+(** Extended right shift *)
+
+Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
+  Val.shrx rs#r1 (Vint n) = Some v ->
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (shrx32 rd r1 n k) rs m k rs' m
+  /\ rs'#rd = v
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold shrx32; intros. apply Val.shrx_shr_2 in H.
+  destruct (Int.eq n Int.zero) eqn:E0.
+- econstructor; split. apply exec_straight_one; simpl; eauto. 
+  split. Simpl. subst v; auto. intros; Simpl.
+- econstructor; split. eapply exec_straight_three.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  rewrite or_zero_eval_shift_op_int by congruence. eauto.
+  simpl; eauto.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  rewrite or_zero_eval_shift_op_int by congruence. eauto.
+  split. subst v; Simpl. intros; Simpl.
+Qed.
+
+Lemma exec_shrx32_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m,
+  Val.shrx rs#r1 (Vint n) = None ->
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (shrx32 rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal None) (rs' x)
+  /\ forall r, data_preg r = true -> r <> rd -> preg_notin r (destroyed_by_op (Oshrximm n)) -> rs'#r = rs#r.
+Proof.
+  unfold shrx32; intros.
+  destruct (Int.eq n Int.zero) eqn:E0.
+- econstructor; split. apply exec_straight_one; simpl; eauto. 
+  split. Simpl. auto. intros; Simpl.
+- econstructor; split. eapply exec_straight_three.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  rewrite or_zero_eval_shift_op_int by congruence. eauto.
+  simpl; eauto.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  rewrite or_zero_eval_shift_op_int by congruence. eauto.
+  split. Simpl. intros; Simpl.
+Qed.
+
+Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
+  Val.shrxl rs#r1 (Vint n) = Some v ->
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (shrx64 rd r1 n k) rs m k rs' m
+  /\ rs'#rd = v
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold shrx64; intros. apply Val.shrxl_shrl_2 in H.
+  destruct (Int.eq n Int.zero) eqn:E.
+- econstructor; split. apply exec_straight_one; simpl; eauto. 
+  split. Simpl. subst v; auto. intros; Simpl.
+- econstructor; split. eapply exec_straight_three.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  rewrite or_zero_eval_shift_op_long by congruence. eauto.
+  simpl; eauto.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  rewrite or_zero_eval_shift_op_long by congruence. eauto.
+  split. subst v; Simpl. intros; Simpl.
+Qed.
+
+Lemma exec_shrx64_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m,
+  Val.shrxl rs#r1 (Vint n) = None ->
+  r1 <> X16 ->
+  exists rs',
+     exec_straight ge lk (shrx64 rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal None) (rs' x)
+  /\ forall r, data_preg r = true -> r <> rd -> preg_notin r (destroyed_by_op (Oshrximm n)) -> rs'#r = rs#r.
+Proof.
+  unfold shrx64; intros.
+  destruct (Int.eq n Int.zero) eqn:E.
+- econstructor; split. apply exec_straight_one; simpl; eauto. 
+  split. Simpl. auto. intros; Simpl.
+- econstructor; split. eapply exec_straight_three.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  rewrite or_zero_eval_shift_op_long by congruence. eauto.
+  simpl; eauto.
+  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+  rewrite or_zero_eval_shift_op_long by congruence. eauto.
+  split. Simpl. intros; Simpl.
+Qed.
+
+Ltac TranslOpBase :=
+  econstructor; split;
+  [ apply exec_straight_one; [simpl; eauto ]
+  | split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl; Simpl
+           | intros; Simpl; fail ] ].
+
+(** Condition bits *)
+
+Lemma compare_int_spec: forall rs v1 v2,
+  let rs' := compare_int rs v1 v2 in
+     rs'#CN = (Val.negative (Val.sub v1 v2))
+  /\ rs'#CZ = (Val_cmpu Ceq v1 v2)
+  /\ rs'#CC = (Val_cmpu Cge v1 v2)
+  /\ rs'#CV = (Val.sub_overflow v1 v2).
+Proof.
+  intros; unfold rs'; auto.
+Qed.
+
+Lemma eval_testcond_compare_sint: forall c v1 v2 b rs,
+  Val.cmp_bool c v1 v2 = Some b ->
+  eval_testcond (cond_for_signed_cmp c) (compare_int rs v1 v2) = Some b.
+Proof.
+  intros. generalize (compare_int_spec rs v1 v2). 
+  set (rs' := compare_int rs v1 v2). intros (B & C & D & E).
+  unfold eval_testcond; rewrite B, C, D, E.
+  destruct v1; try discriminate; destruct v2; try discriminate.
+  simpl in H; inv H.
+  unfold Val_cmpu; simpl. destruct c; simpl.
+- destruct (Int.eq i i0); auto.
+- destruct (Int.eq i i0); auto.
+- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
+- rewrite Int.lt_sub_overflow, Int.not_lt.
+  destruct (Int.eq i i0), (Int.lt i i0); auto.
+- rewrite Int.lt_sub_overflow, (Int.lt_not i). 
+  destruct (Int.eq i i0), (Int.lt i i0); auto.
+- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
+Qed.
+
+Lemma eval_testcond_compare_uint: forall c v1 v2 b rs,
+  Val_cmpu_bool c v1 v2 = Some b ->
+  eval_testcond (cond_for_unsigned_cmp c) (compare_int rs v1 v2) = Some b.
+Proof.
+  intros. generalize (compare_int_spec rs v1 v2). 
+  set (rs' := compare_int rs v1 v2). intros (B & C & D & E).
+  unfold eval_testcond; rewrite B, C, D, E.
+  destruct v1; try discriminate; destruct v2; try discriminate.
+  simpl in H; inv H.
+  unfold Val_cmpu; simpl. destruct c; simpl.
+- destruct (Int.eq i i0); auto.
+- destruct (Int.eq i i0); auto.
+- destruct (Int.ltu i i0); auto.
+- rewrite (Int.not_ltu i). destruct (Int.eq i i0), (Int.ltu i i0); auto.
+- rewrite (Int.ltu_not i). destruct (Int.eq i i0), (Int.ltu i i0); auto.
+- destruct (Int.ltu i i0); auto.
+Qed.
+
+Lemma compare_long_spec: forall rs v1 v2,
+  let rs' := compare_long rs v1 v2 in
+     rs'#CN = (Val.negativel (Val.subl v1 v2))
+  /\ rs'#CZ = (Val_cmplu Ceq v1 v2)
+  /\ rs'#CC = (Val_cmplu Cge v1 v2)
+  /\ rs'#CV = (Val.subl_overflow v1 v2).
+Proof.
+  intros; unfold rs'; auto.
+Qed.
+
+Remark int64_sub_overflow:
+  forall x y,
+  Int.xor (Int.repr (Int64.unsigned (Int64.sub_overflow x y Int64.zero)))
+          (Int.repr (Int64.unsigned (Int64.negative (Int64.sub x y)))) =
+  (if Int64.lt x y then Int.one else Int.zero).
+Proof.
+  intros.
+  transitivity (Int.repr (Int64.unsigned (if Int64.lt x y then Int64.one else Int64.zero))).
+  rewrite <- (Int64.lt_sub_overflow x y).
+  unfold Int64.sub_overflow, Int64.negative.
+  set (s := Int64.signed x - Int64.signed y - Int64.signed Int64.zero).
+  destruct (zle Int64.min_signed s && zle s Int64.max_signed);
+  destruct (Int64.lt (Int64.sub x y) Int64.zero);
+  auto.
+  destruct (Int64.lt x y); auto.
+Qed.
+
+Lemma eval_testcond_compare_slong: forall c v1 v2 b rs,
+  Val.cmpl_bool c v1 v2 = Some b ->
+  eval_testcond (cond_for_signed_cmp c) (compare_long rs v1 v2) = Some b.
+Proof.
+  intros. generalize (compare_long_spec rs v1 v2). 
+  set (rs' := compare_long rs v1 v2). intros (B & C & D & E).
+  unfold eval_testcond; rewrite B, C, D, E.
+  destruct v1; try discriminate; destruct v2; try discriminate.
+  simpl in H; inv H.
+  unfold Val_cmplu; simpl. destruct c; simpl.
+- destruct (Int64.eq i i0); auto.
+- destruct (Int64.eq i i0); auto.
+- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
+- rewrite int64_sub_overflow, Int64.not_lt.
+  destruct (Int64.eq i i0), (Int64.lt i i0); auto.
+- rewrite int64_sub_overflow, (Int64.lt_not i). 
+  destruct (Int64.eq i i0), (Int64.lt i i0); auto.
+- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
+Qed.
+
+Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs,
+  Val_cmplu_bool c v1 v2 = Some b ->
+  eval_testcond (cond_for_unsigned_cmp c) (compare_long rs v1 v2) = Some b.
+Proof.
+  intros. generalize (compare_long_spec rs v1 v2). 
+  set (rs' := compare_long rs v1 v2). intros (B & C & D & E).
+  unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu.
+  destruct v1; try discriminate; destruct v2; try discriminate; simpl in H.
+- (* int-int *)
+  inv H. destruct c; simpl.
++ destruct (Int64.eq i i0); auto.
++ destruct (Int64.eq i i0); auto.
++ destruct (Int64.ltu i i0); auto.
++ rewrite (Int64.not_ltu i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto.
++ rewrite (Int64.ltu_not i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto.
++ destruct (Int64.ltu i i0); auto.
+- (* int-ptr *)
+  simpl.
+  destruct (Archi.ptr64); simpl; try discriminate.
+  destruct (Int64.eq i Int64.zero); simpl; try discriminate.
+  destruct c; simpl in H; inv H; reflexivity.
+- (* ptr-int *)
+  simpl.
+  destruct (Archi.ptr64); simpl; try discriminate.
+  destruct (Int64.eq i0 Int64.zero); try discriminate.
+  destruct c; simpl in H; inv H; reflexivity.
+- (* ptr-ptr *)
+  simpl. 
+  destruct (eq_block b0 b1).
+  destruct (Archi.ptr64); simpl; try discriminate.
+  inv H.
+  destruct c; simpl.
+* destruct (Ptrofs.eq i i0); auto.
+* destruct (Ptrofs.eq i i0); auto.
+* destruct (Ptrofs.ltu i i0); auto.
+* rewrite (Ptrofs.not_ltu i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto.
+* rewrite (Ptrofs.ltu_not i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto.
+* destruct (Ptrofs.ltu i i0); auto.
+* destruct c; simpl in H; inv H; reflexivity.
+Qed.
+
+Lemma compare_float_spec: forall rs f1 f2,
+  let rs' := compare_float rs (Vfloat f1) (Vfloat f2) in
+     rs'#CN = (Val.of_bool (Float.cmp Clt f1 f2))
+  /\ rs'#CZ = (Val.of_bool (Float.cmp Ceq f1 f2))
+  /\ rs'#CC = (Val.of_bool (negb (Float.cmp Clt f1 f2)))
+  /\ rs'#CV = (Val.of_bool (negb (Float.ordered f1 f2))).
+Proof.
+  intros; auto.
+Qed.
+
+Lemma eval_testcond_compare_float: forall c v1 v2 b rs,
+  Val.cmpf_bool c v1 v2 = Some b ->
+  eval_testcond (cond_for_float_cmp c) (compare_float rs v1 v2) = Some b.
+Proof.
+  intros. destruct v1; try discriminate; destruct v2; simpl in H; inv H. 
+  generalize (compare_float_spec rs f f0). 
+  set (rs' := compare_float rs (Vfloat f) (Vfloat f0)).
+  intros (B & C & D & E).
+  unfold eval_testcond; rewrite B, C, D, E.
+Local Transparent Float.cmp Float.ordered.
+  unfold Float.cmp, Float.ordered;
+  destruct c; destruct (Float.compare f f0) as [[]|]; reflexivity.
+Qed.
+
+Lemma eval_testcond_compare_not_float: forall c v1 v2 b rs,
+  option_map negb (Val.cmpf_bool c v1 v2) = Some b ->
+  eval_testcond (cond_for_float_not_cmp c) (compare_float rs v1 v2) = Some b.
+Proof.
+  intros. destruct v1; try discriminate; destruct v2; simpl in H; inv H.
+  generalize (compare_float_spec rs f f0). 
+  set (rs' := compare_float rs (Vfloat f) (Vfloat f0)).
+  intros (B & C & D & E).
+  unfold eval_testcond; rewrite B, C, D, E.
+Local Transparent Float.cmp Float.ordered.
+  unfold Float.cmp, Float.ordered;
+  destruct c; destruct (Float.compare f f0) as [[]|]; reflexivity.
+Qed.
+
+Lemma compare_single_spec: forall rs f1 f2,
+  let rs' := compare_single rs (Vsingle f1) (Vsingle f2) in
+     rs'#CN = (Val.of_bool (Float32.cmp Clt f1 f2))
+  /\ rs'#CZ = (Val.of_bool (Float32.cmp Ceq f1 f2))
+  /\ rs'#CC = (Val.of_bool (negb (Float32.cmp Clt f1 f2)))
+  /\ rs'#CV = (Val.of_bool (negb (Float32.ordered f1 f2))).
+Proof.
+  intros; auto.
+Qed.
+
+Lemma eval_testcond_compare_single: forall c v1 v2 b rs,
+  Val.cmpfs_bool c v1 v2 = Some b ->
+  eval_testcond (cond_for_float_cmp c) (compare_single rs v1 v2) = Some b.
+Proof.
+  intros. destruct v1; try discriminate; destruct v2; simpl in H; inv H. 
+  generalize (compare_single_spec rs f f0). 
+  set (rs' := compare_single rs (Vsingle f) (Vsingle f0)).
+  intros (B & C & D & E).
+  unfold eval_testcond; rewrite B, C, D, E.
+Local Transparent Float32.cmp Float32.ordered.
+  unfold Float32.cmp, Float32.ordered;
+  destruct c; destruct (Float32.compare f f0) as [[]|]; reflexivity.
+Qed.
+
+Lemma eval_testcond_compare_not_single: forall c v1 v2 b rs,
+  option_map negb (Val.cmpfs_bool c v1 v2) = Some b ->
+  eval_testcond (cond_for_float_not_cmp c) (compare_single rs v1 v2) = Some b.
+Proof.
+  intros. destruct v1; try discriminate; destruct v2; simpl in H; inv H.
+  generalize (compare_single_spec rs f f0). 
+  set (rs' := compare_single rs (Vsingle f) (Vsingle f0)).
+  intros (B & C & D & E).
+  unfold eval_testcond; rewrite B, C, D, E.
+Local Transparent Float32.cmp Float32.ordered.
+  unfold Float32.cmp, Float32.ordered;
+  destruct c; destruct (Float32.compare f f0) as [[]|]; reflexivity.
+Qed.
+
+Remark compare_float_inv: forall rs v1 v2 r,
+  match r with CR _ => False | _ => True end ->
+  (compare_float rs v1 v2)#r = rs#r.
+Proof.
+  intros; unfold compare_float.
+  destruct r; try contradiction; destruct v1; auto; destruct v2; auto.
+Qed.
+
+Remark compare_single_inv: forall rs v1 v2 r,
+  match r with CR _ => False | _ => True end ->
+  (compare_single rs v1 v2)#r = rs#r.
+Proof.
+  intros; unfold compare_single.
+  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) ->
+  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''
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
+Proof.
+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) ->
+  eval_condition cond (List.map ms args) m = Some true ->
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  exists rs', exists insn,
+     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'
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
+Proof.
+  intros. eapply transl_cbranch_correct_1 with (b := true); eauto.
+Qed.  *)
+
+Lemma transl_cond_correct:
+  forall cond args k c rs m,
+  transl_cond cond args k = OK c ->
+  exists rs',
+     exec_straight ge lk c rs m k rs' m
+  /\ (forall b,
+      eval_condition cond (map rs (map preg_of args)) m = Some b ->
+      eval_testcond (cond_for_cond cond) rs' = Some b)
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
+Proof.
+  intros until m; intros TR. destruct cond; simpl in TR; ArgsInv.
+- (* Ccomp *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_sint; auto. 
+  destruct r; reflexivity || discriminate.
+- (* Ccompu *)
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros. apply eval_testcond_compare_uint; auto. 
+  destruct r; reflexivity || discriminate.
+- (* Ccompimm *)
+  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.
+  split; intros. apply eval_testcond_compare_sint; auto. 
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+- (* Ccompuimm *)
+  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_uint; 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_uint; 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_uint; auto. 
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+- (* Ccompshift *)
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. 
+  destruct r; reflexivity || discriminate.
+- (* Ccompushift *)
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. 
+  destruct r; reflexivity || discriminate.
+- (* Cmaskzero *)
+  destruct (is_logical_imm32 n).
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); 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 Ceq); auto.
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+- (* Cmasknotzero *)
+  destruct (is_logical_imm32 n).
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); 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 Cne); auto.
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+- (* Ccompl *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_slong; auto. 
+  destruct r; reflexivity || discriminate.
+- (* Ccomplu *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_ulong; auto.
+  erewrite Val_cmplu_bool_correct; eauto.
+  destruct r; reflexivity || discriminate.
+- (* Ccomplimm *)
+  destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. 
+  destruct r; reflexivity || discriminate.
++ econstructor; split.
+  apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
+  split; intros. apply eval_testcond_compare_slong; auto. 
+  destruct r; reflexivity || discriminate.
++ exploit (exec_loadimm64 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_slong; auto. 
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+- (* Ccompluimm *)
+  destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto.
+  erewrite Val_cmplu_bool_correct; eauto.
+  destruct r; reflexivity || discriminate.
++ econstructor; split.
+  apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
+  split; intros. apply eval_testcond_compare_ulong; auto.
+  erewrite Val_cmplu_bool_correct; eauto.
+  destruct r; reflexivity || discriminate.
++ exploit (exec_loadimm64 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.
+  split; intros. apply eval_testcond_compare_ulong; auto.
+  erewrite Val_cmplu_bool_correct; eauto. 
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+- (* Ccomplshift *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. 
+  destruct r; reflexivity || discriminate.
+- (* Ccomplushift *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto.
+  erewrite Val_cmplu_bool_correct; eauto. 
+  destruct r; reflexivity || discriminate.
+- (* Cmasklzero *)
+  destruct (is_logical_imm64 n).
++ econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto.
+  destruct r; reflexivity || discriminate.
++ exploit (exec_loadimm64 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.
+  split; intros. apply (eval_testcond_compare_slong Ceq); auto.
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+- (* Cmasknotzero *)
+  destruct (is_logical_imm64 n).
++ econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto.
+  destruct r; reflexivity || discriminate.
++ exploit (exec_loadimm64 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.
+  split; intros. apply (eval_testcond_compare_slong Cne); auto.
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+- (* Ccompf *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_float; auto.
+  destruct r; discriminate || rewrite compare_float_inv; auto.
+- (* Cnotcompf *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_not_float; auto.
+  destruct r; discriminate || rewrite compare_float_inv; auto.
+- (* Ccompfzero *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_float; auto.
+  destruct r; discriminate || rewrite compare_float_inv; auto.
+- (* Cnotcompfzero *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_not_float; auto.
+  destruct r; discriminate || rewrite compare_float_inv; auto.
+- (* Ccompfs *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_single; auto.
+  destruct r; discriminate || rewrite compare_single_inv; auto.
+- (* Cnotcompfs *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_not_single; auto.
+  destruct r; discriminate || rewrite compare_single_inv; auto.
+- (* Ccompfszero *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_single; auto.
+  destruct r; discriminate || rewrite compare_single_inv; auto.
+- (* Cnotcompfszero *)
+  econstructor; split. apply exec_straight_one. simpl; eauto.
+  split; intros. apply eval_testcond_compare_not_single; auto.
+  destruct r; discriminate || rewrite compare_single_inv; auto.
+Qed.
+
+Lemma transl_op_correct:
+  forall op args res k (rs: regset) m v c,
+  transl_op op args res k = OK c ->
+  eval_operation ge (rs#SP) op (map rs (map preg_of args)) m = Some v ->
+  exists rs',
+     exec_straight ge lk c rs m k rs' m
+  /\ Val.lessdef v rs'#(preg_of res)
+  /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.
+Proof.
+  (* assert (SAME: forall v1 v2, v1 = v2 -> Val.lessdef v2 v1). { intros; subst; auto. } *)
+Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize.
+  intros until c; intros TR EV.
+  unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl;
+  try (rewrite <- transl_eval_shift; TranslOpSimpl).
+- (* move *)
+  destruct (preg_of res), (preg_of m0); try destruct d; try destruct d0; inv TR; TranslOpSimpl.
+- (* intconst *)
+  exploit exec_loadimm32. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
+- (* longconst *)
+  exploit exec_loadimm64. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
+- (* floatconst *)
+  destruct (Float.eq_dec n Float.zero).
++ subst n. TranslOpSimpl. 
++ TranslOpSimplN.
+- (* singleconst *)
+  destruct (Float32.eq_dec n Float32.zero).
++ subst n. TranslOpSimpl. 
++ TranslOpSimplN.
+- (* loadsymbol *)
+  exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
+- (* addrstack *)
+  exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)); try discriminate. simpl; eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. replace (DR XSP) with (SP) in B by auto. rewrite B.
+Local Transparent Val.addl.
+  destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
+  auto.
+- (* shift *)
+  rewrite <- transl_eval_shift'. TranslOpSimpl.
+- (* addimm *)
+  exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
+- (* mul *)
+  TranslOpBase.
+Local Transparent Val.add.
+  destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto.
+- (* andimm *)
+  exploit (exec_logicalimm32 (Pandimm W) (Pand W)).
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
+- (* orimm *)
+  exploit (exec_logicalimm32 (Porrimm W) (Porr W)). 
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
+- (* xorimm *)
+  exploit (exec_logicalimm32 (Peorimm W) (Peor W)). 
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
+- (* not *)
+  TranslOpBase.
+  destruct (rs x0); auto. simpl. rewrite Int.or_zero_l; auto. 
+- (* notshift *)
+  TranslOpBase.
+  destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto. 
+- (* shrx *)
+  assert (Val.maketotal (Val.shrx (rs x0) (Vint n)) = Val.maketotal (Val.shrx (rs x0) (Vint n))) by eauto.
+  destruct (Val.shrx) eqn:E.
+  + exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C).
+    econstructor; split. eexact A. split. rewrite B; auto. auto.
+  + exploit (exec_shrx32_none x x0 n); eauto with asmgen.
+- (* zero-ext *)
+  TranslOpBase.
+  destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto.
+- (* sign-ext *)
+  TranslOpBase.
+  destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto.
+- (* shlzext *)
+  TranslOpBase.
+  destruct (rs x0); simpl; auto. rewrite <- Int.shl_zero_ext_min; auto using a32_range.
+- (* shlsext *)
+  TranslOpBase.
+  destruct (rs x0); simpl; auto. rewrite <- Int.shl_sign_ext_min; auto using a32_range.
+- (* zextshr *)
+  TranslOpBase.
+  destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.zero_ext_shru_min; auto using a32_range.
+- (* sextshr *)
+  TranslOpBase.
+  destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.sign_ext_shr_min; auto using a32_range.
+- (* shiftl *)
+  rewrite <- transl_eval_shiftl'. TranslOpSimpl.
+- (* extend *)
+  exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C).
+  econstructor; split. eexact A. 
+  split. rewrite B; auto. eauto with asmgen.
+- (* addlshift *)
+  TranslOpBase.
+- (* addext *)
+  exploit (exec_arith_extended Val.addl Paddext (Padd X)).
+  auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
+  econstructor; split. eexact A. split. rewrite B; auto. auto.
+- (* addlimm *)
+  exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence.
+  intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto.
+- (* neglshift *)
+  TranslOpBase.
+- (* sublshift *)
+  TranslOpBase.
+- (* subext *)
+  exploit (exec_arith_extended Val.subl Psubext (Psub X)).
+  auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
+  econstructor; split. eexact A. split. rewrite B; auto. auto.
+- (* mull *)
+  TranslOpBase.
+  destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto.
+- (* andlshift *)
+  TranslOpBase.
+- (* andlimm *)
+  exploit (exec_logicalimm64 (Pandimm X) (Pand X)). 
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
+- (* orlshift *)
+  TranslOpBase.
+- (* orlimm *)
+  exploit (exec_logicalimm64 (Porrimm X) (Porr X)). 
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
+- (* orlshift *)
+  TranslOpBase.
+- (* xorlimm *)
+  exploit (exec_logicalimm64 (Peorimm X) (Peor X)). 
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
+- (* notl *)
+  TranslOpBase.
+  destruct (rs x0); auto. simpl. rewrite Int64.or_zero_l; auto.
+- (* notlshift *)
+  TranslOpBase.
+  destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto.
+- (* biclshift *)
+  TranslOpBase.
+- (* ornlshift *)
+  TranslOpBase.
+- (* eqvlshift *)
+  TranslOpBase.
+- (* shrx *)
+  assert (Val.maketotal (Val.shrxl (rs x0) (Vint n)) = Val.maketotal (Val.shrxl (rs x0) (Vint n))) by eauto.
+  destruct (Val.shrxl) eqn:E.
+  + exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C).
+    econstructor; split. eexact A. split. rewrite B; auto. auto.
+  + exploit (exec_shrx64_none x x0 n); eauto with asmgen.
+- (* zero-ext-l *)
+  TranslOpBase.
+  destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto.
+- (* sign-ext-l *)
+  TranslOpBase.
+  destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto.
+- (* shllzext *)
+  TranslOpBase.
+  destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_zero_ext_min; auto using a64_range.
+- (* shllsext *)
+  TranslOpBase.
+  destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_sign_ext_min; auto using a64_range.
+- (* zextshrl *)
+  TranslOpBase.
+  destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.zero_ext_shru'_min; auto using a64_range.
+- (* sextshrl *)
+  TranslOpBase.
+  destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range.
+- (* condition *)
+  exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
+  rewrite (B b) by auto. auto. 
+  auto.
+  intros; Simpl.
+- (* select *)
+  destruct (preg_of res) as [[ir|fr]|cr|] eqn:RES; monadInv TR.
+  + (* integer *)
+    generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
+    exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
+    econstructor; split.
+    eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto.
+    split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
+    rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
+    rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
+    auto.
+    intros; Simpl.
+  + (* FP *)
+    generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
+    exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
+    econstructor; split.
+    eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto.
+    split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
+    rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
+    rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
+    auto.
+    intros; Simpl.
+Qed.
+
+(** Translation of addressing modes, loads, stores *)
+
+Lemma transl_addressing_correct:
+  forall sz addr args (insn: Asm.addressing -> basic) k (rs: regset) m c b o,
+  transl_addressing sz addr args insn k = OK c ->
+  Op.eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some (Vptr b o) ->
+  exists ad rs',
+     exec_straight_opt ge lk c rs m (insn ad :: k) rs' m
+  /\ eval_addressing lk ad rs' = Vptr b o
+  /\ forall r, data_preg r = true -> rs' r = rs r.
+Proof.
+  intros until o; intros TR EV.
+  unfold transl_addressing in TR; destruct addr; ArgsInv; SimplEval EV.
+- (* Aindexed *)
+  destruct (offset_representable sz ofs); inv EQ0.
++ econstructor; econstructor; split. apply exec_straight_opt_refl.
+  auto.
++ exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C).
+  econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A.
+  split. simpl. rewrite B, C by eauto with asmgen. auto.
+  eauto with asmgen.
+- (* Aindexed2 *)
+  econstructor; econstructor; split. apply exec_straight_opt_refl.
+  auto.
+- (* Aindexed2shift *)
+  destruct (Int.eq a Int.zero) eqn:E; [|destruct (Int.eq (Int.shl Int.one a) (Int.repr sz))]; inv EQ2.
++ apply Int.same_if_eq in E. rewrite E.
+  econstructor; econstructor; split. apply exec_straight_opt_refl.
+  split; auto. simpl.
+  rewrite Val.addl_commut in H0. destruct (rs x0); try discriminate.
+  unfold Val.shll. rewrite Int64.shl'_zero. auto.
++ econstructor; econstructor; split. apply exec_straight_opt_refl.
+  auto. 
++ econstructor; econstructor; split.
+  apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto.
+  split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto.
+  intros; Simpl.
+- (* Aindexed2ext *)
+  destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2.
++ econstructor; econstructor; split. apply exec_straight_opt_refl.
+  split; auto. destruct x; auto.
++ exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto.
+  instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C).
+  econstructor; exists rs'; split.
+  apply exec_straight_opt_intro. eexact A. 
+  split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal.
+  unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range;
+  simpl; rewrite Int64.add_zero; auto.
+  intros. apply C; eauto with asmgen.
+- (* Aglobal *)
+  destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR.
++ econstructor; econstructor; split.
+  apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto.
+  split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence.
+  intros; Simpl.
++ exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C).
+  econstructor; exists rs'; split.
+  apply exec_straight_opt_intro. eexact A.
+  split. simpl. 
+  rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. 
+  simpl in EV. congruence. 
+  auto with asmgen.
+- (* Ainstrack *)
+  assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o).
+  { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. 
+    rewrite Ptrofs.of_int64_to_int64 by auto. auto. }   
+  destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR.
++ econstructor; econstructor; split. apply exec_straight_opt_refl.
+  auto.
++ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C).
+  econstructor; exists rs'; split.
+  apply exec_straight_opt_intro. eexact A.
+  split. simpl. rewrite B, C by eauto with asmgen. auto.
+  auto with asmgen.
+Qed.
+
+Lemma transl_load_correct:
+  forall chunk addr args dst k c (rs: regset) m vaddr v,
+  transl_load chunk addr args dst k = OK c ->
+  Op.eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some vaddr ->
+  Mem.loadv chunk m vaddr = Some v ->
+  exists rs',
+     exec_straight ge lk c rs m k rs' m
+  /\ rs'#(preg_of dst) = v
+  /\ forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r.
+Proof.
+  intros. destruct vaddr; try discriminate.
+  assert (A: exists sz insn,
+                transl_addressing sz addr args insn k = OK c
+             /\ (forall ad rs', exec_basic lk ge (insn ad) rs' m =
+                              exec_load_rd_a lk chunk (fun v => v) ad (dreg_of dst) rs' m)).
+  {
+    destruct chunk; monadInv H;
+    try rewrite (ireg_of_eq' _ _ EQ); try rewrite (freg_of_eq' _ _ EQ);
+    do 2 econstructor; (split; [eassumption|auto]).
+  }
+  destruct A as (sz & insn & B & C).
+  exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R).
+  assert (X: exec_load_rd_a lk chunk (fun v => v) ad (dreg_of dst) rs' m =
+             Next (rs'#(preg_of dst) <- v) m).
+  { unfold exec_load_rd_a. rewrite Q, H1. auto. }
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact P.
+  apply exec_straight_one. rewrite C, X; eauto. Simpl. 
+  split. auto. intros; Simpl.
+Qed.
+
+Lemma transl_store_correct:
+  forall chunk addr args src k c (rs: regset) m vaddr m',
+  transl_store chunk addr args src k = OK c ->
+  Op.eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some vaddr ->
+  Mem.storev chunk m vaddr rs#(preg_of src) = Some m' ->
+  exists rs',
+     exec_straight ge lk c rs m k rs' m'
+  /\ forall r, data_preg r = true -> rs' r = rs r.
+Proof.
+  intros. destruct vaddr; try discriminate. 
+  set (chunk' := match chunk with Mint8signed => Mint8unsigned
+                                | Mint16signed => Mint16unsigned
+                                | _ => chunk end).
+  assert (A: exists sz insn,
+                transl_addressing sz addr args insn k = OK c
+             /\ (forall ad rs', exec_basic lk ge (insn ad) rs' m =
+                              exec_store_rs_a lk chunk' ad rs'#(preg_of src) rs' m)).
+  {
+    unfold chunk'; destruct chunk; monadInv H;
+    try rewrite (ireg_of_eq _ _ EQ); try rewrite (freg_of_eq _ _ EQ);
+    do 2 econstructor; (split; [eassumption|auto]).
+  }
+  destruct A as (sz & insn & B & C).
+  exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R).
+  assert (X: Mem.storev chunk' m (Vptr b i) rs#(preg_of src) = Some m').
+  { rewrite <- H1. unfold chunk'. destruct chunk; auto; simpl; symmetry.
+    apply Mem.store_signed_unsigned_8.
+    apply Mem.store_signed_unsigned_16. }
+  assert (Y: exec_store_rs_a lk chunk' ad rs'#(preg_of src) rs' m =
+             Next rs' m').
+  { unfold exec_store_rs_a. rewrite Q, R, X by auto with asmgen. auto. }
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact P.
+  apply exec_straight_one. rewrite C, Y; eauto. 
+  intros; Simpl. rewrite R; auto.
+Qed.
+
+(** Memory accesses *)
+
+Lemma indexed_memory_access_correct: forall insn sz (base: iregsp) ofs k (rs: regset) m b i,
+  preg_of_iregsp base <> X16 ->
+  Val.offset_ptr rs#base ofs = Vptr b i ->
+  exists ad rs',
+     exec_straight_opt ge lk (indexed_memory_access_bc insn sz base ofs k) rs m (insn ad :: k) rs' m
+  /\ eval_addressing lk ad rs' = Vptr b i
+  /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r.
+Proof.
+  unfold indexed_memory_access_bc; intros.
+  assert (Val.addl rs#base (Vlong (Ptrofs.to_int64 ofs)) = Vptr b i).
+  { destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. }
+  destruct offset_representable.
+- econstructor; econstructor; split. apply exec_straight_opt_refl. auto. 
+- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C).
+  econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A.
+  split. simpl. rewrite B, C; eauto; try discriminate.
+  unfold preg_of_iregsp in H. destruct base; auto. auto.
+Qed.
+
+Lemma loadptr_correct: forall (base: iregsp) ofs dst k m v (rs: regset),
+  Mem.loadv Mint64 m (Val.offset_ptr rs#base ofs) = Some v ->
+  preg_of_iregsp base <> IR X16 ->
+  exists rs',
+     exec_straight ge lk (loadptr_bc base ofs dst k) rs m k rs' m
+  /\ rs'#dst = v
+  /\ forall r, r <> PC -> r <> X16 -> r <> dst -> 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_load_rd_a. rewrite B, H. eauto.
+  split. Simpl. intros; Simpl.
+Qed.
+
+Lemma loadind_correct:
+  forall (base: iregsp) ofs ty dst k c (rs: regset) m v,
+  loadind base ofs ty dst k = OK c ->
+  Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v ->
+  preg_of_iregsp base <> IR X16 ->
+  exists rs',
+     exec_straight ge lk c rs m k rs' m
+  /\ rs'#(preg_of dst) = v
+  /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
+Proof.
+  intros.
+  destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
+  assert (X: exists sz (insn: addressing -> ld_instruction),
+                c = indexed_memory_access_bc insn sz base ofs k
+             /\ (forall ad rs', exec_basic lk ge (insn ad) rs' m =
+                              exec_load_rd_a lk (chunk_of_type ty) (fun v => v) ad (dreg_of dst) rs' m)).
+  {
+    unfold loadind in H; destruct ty; destruct (dst); inv H;
+    do 2 econstructor; split; eauto.
+  }
+  destruct X as (sz & insn & EQ & SEM). subst c.
+  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. rewrite SEM. unfold exec_load.
+  unfold exec_load_rd_a. rewrite B, H0. eauto. Simpl.
+  split. auto. intros; Simpl.
+Qed.
+
+Lemma storeind_correct: forall (base: iregsp) ofs ty src k c (rs: regset) m m',
+  storeind src base ofs ty k = OK c ->
+  Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' ->
+  preg_of_iregsp base <> IR X16 ->
+  exists rs',
+     exec_straight ge lk c rs m k rs' m'
+  /\ forall r, data_preg r = true -> rs' r = rs r.
+Proof.
+  intros. 
+  destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
+  assert (X: exists sz (insn: addressing -> st_instruction),
+                c = indexed_memory_access_bc insn sz base ofs k
+             /\ (forall ad rs', exec_basic lk ge (insn ad) rs' m =
+                              exec_store_rs_a lk (chunk_of_type ty) ad rs'#(preg_of src) rs' m)).
+  {
+    unfold storeind in H; destruct ty; destruct (preg_of src) as [[ir|fr]|cr|]; inv H; do 2 econstructor; split; eauto.
+  }
+  destruct X as (sz & insn & EQ & SEM). subst c.
+  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. rewrite SEM.
+  unfold exec_store. unfold exec_store_rs_a.
+  rewrite B, C, H0 by eauto with asmgen. eauto.
+  intros; Simpl. unfold data_preg in H2. destruct r as [[[ir|]|fr]|cr|].
+  all: rewrite C; auto; try discriminate;
+       destruct ir; try discriminate.
+Qed.
+
+Lemma make_epilogue_correct:
+  forall ge0 f m stk soff cs m' ms rs tm,
+  Mach.load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
+  Mach.load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) ->
+  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+  agree ms (Vptr stk soff) rs ->
+  Mem.extends m tm ->
+  match_stack ge0 cs ->
+  exists rs', exists tm',
+     exec_straight ge lk (make_epilogue f) rs tm nil rs' tm'
+  /\ agree ms (parent_sp cs) rs'
+  /\ Mem.extends m' tm'
+  /\ rs'#RA = parent_ra cs
+  /\ rs'#SP = parent_sp cs
+  /\ (forall r, r <> PC -> r <> SP -> r <> X30 -> r <> X16 -> rs'#r = rs#r).
+Proof.
+  assert (Archi.ptr64 = true) as SF; auto.
+  intros until tm; intros LP LRA FREE AG MEXT MCS.
+  exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP').
+  exploit Mem.loadv_extends. eauto. eexact LRA. auto. simpl. intros (ra' & LRA' & LDRA').
+  exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'.
+  exploit lessdef_parent_ra; eauto. intros EQ; subst ra'; clear LDRA'.
+  exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
+  unfold make_epilogue.
+  rewrite chunk_of_Tptr in *. unfold Mptr in *. rewrite SF in *.
+
+  exploit (loadptr_correct XSP (fn_retaddr_ofs f)).
+    instantiate (2 := rs). simpl. 
+    replace (rs XSP) with (rs SP) by auto.
+    rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. simpl; discriminate.
+    
+    intros (rs1 & A1 & B1 & C1).
+  econstructor; econstructor; split.
+  eapply exec_straight_trans. eexact A1. apply exec_straight_one. simpl. 
+    simpl; rewrite (C1 SP) by auto with asmgen. rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. 
+    rewrite FREE'. eauto.
+  split. apply agree_set_other; auto.
+  apply agree_change_sp with (Vptr stk soff).
+  apply agree_exten with rs; auto. intros; apply C1; auto with asmgen.
+  eapply parent_sp_def; eauto.
+  split. auto.
+  split. Simpl. 
+  split. Simpl. 
+  intros. Simpl.
+Qed.
+
+End CONSTRUCTORS.
\ No newline at end of file
diff --git a/aarch64/Asmblockprops.v b/aarch64/Asmblockprops.v
index d1015ea9..cef95aad 100644
--- a/aarch64/Asmblockprops.v
+++ b/aarch64/Asmblockprops.v
@@ -39,7 +39,13 @@ Lemma preg_of_data:
 Proof.
   intros. destruct r; reflexivity.
 Qed.
-Hint Resolve preg_of_data: asmgen.
+
+Lemma dreg_of_data:
+  forall r, data_preg (dreg_of r) = true.
+Proof.
+  intros. destruct r; reflexivity.
+Qed.
+Hint Resolve preg_of_data dreg_of_data: asmgen.
 
 Lemma data_diff:
   forall r r',
@@ -55,6 +61,12 @@ Proof.
   intros. apply data_diff; auto with asmgen.
 Qed.
 
+Lemma preg_of_not_SP:
+  forall r, preg_of r <> SP.
+Proof.
+  intros. unfold preg_of; destruct r; simpl; try discriminate.
+Qed.
+
 (*
 Lemma preg_of_not_SP:
   forall r, preg_of r <> SP.
@@ -81,73 +93,61 @@ Lemma nextblock_inv1:
   forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.
 Proof.
   intros. apply nextblock_inv. red; intro; subst; discriminate.
-Qed.
+Qed.*)
+
+Ltac desif :=
+  repeat match goal with
+  | [ |- context[ if ?f then _ else _ ] ] => destruct f
+  end.
+  
+Ltac decomp :=
+  repeat match goal with
+  | [ |- context[ match (?rs ?r) with | _ => _ end ] ] => destruct (rs r)
+  end.
 
 Ltac Simplif :=
-  ((rewrite nextblock_inv by eauto with asmgen)
-  || (rewrite nextblock_inv1 by eauto with asmgen)
+  ((desif)
+  || (try unfold compare_long)
+  || (try unfold compare_int)
+  || (try unfold compare_float)
+  || (try unfold compare_single)
+  || decomp
   || (rewrite Pregmap.gss)
-  || (rewrite nextblock_pc)
   || (rewrite Pregmap.gso by eauto with asmgen)
   ); auto with asmgen.
 
 Ltac Simpl := repeat Simplif.
 
+Section EPC.
+
+Variable lk: aarch64_linker.
+
 (* For Asmblockgenproof0 *)
 
 Theorem exec_basic_instr_pc:
   forall ge b rs1 m1 rs2 m2,
-  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
+  exec_basic lk ge b rs1 m1 = Next rs2 m2 ->
   rs2 PC = rs1 PC.
 Proof.
-  intros. destruct b; try destruct i; try destruct i.
-  all: try (inv H; Simpl).
-  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  { (* PLoadQRRO *)
-    unfold  parexec_load_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  { (* PLoadORRO *)
-    unfold  parexec_load_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
-  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  
-  { (* PStoreQRRO *)
-    unfold  parexec_store_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  { (* PStoreORRO *)
-    unfold  parexec_store_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
-  - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
-    destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
-  - destruct rs; try discriminate. inv H1. Simpl.
-  - destruct rd; try discriminate. inv H1; Simpl.
-  - reflexivity.
+  intros. destruct b; try destruct i; try destruct i; try destruct ld; try destruct ld;
+  try destruct st; try destruct st; try destruct a.
+  all: try (inv H; simpl in *; auto; Simpl).
+  all: try (try unfold exec_load_rd_a in H1; try destruct (Mem.loadv _ _ _); inv H1; Simpl).
+  all: try (try unfold exec_load_double in H0; destruct (Mem.loadv _ _ _); simpl in *;
+            try destruct (Mem.loadv _ _ _); simpl in *; inv H0; Simpl).
+  all: try (try unfold exec_store_rs_a in H0; try destruct (Mem.storev _ _ _); inv H0; auto; Simpl).
+  all: try (try unfold exec_store_double in H1; destruct (Mem.storev _ _ _); simpl in *;
+            try destruct (Mem.storev _ _ _); simpl in *; inv H1; auto; Simpl).
+  - (* alloc *)
+    destruct (Mem.alloc _ _ _); destruct (Mem.store _ _ _); inv H1; auto; Simpl.
+  - (* free *)
+    destruct (rs1 SP); try discriminate; destruct (Mem.free _ _ _ _); inv H1; Simpl.
 Qed.
 
+End EPC.
+
+(*
+
 (* For PostpassSchedulingproof *)
 
 Lemma regset_double_set:
diff --git a/configure b/configure
index ae729e80..a81fe61b 100755
--- a/configure
+++ b/configure
@@ -844,7 +844,7 @@ if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling
 cat >> Makefile.config <<EOF
 ARCHDIRS=$arch
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v \\
-    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof.v Asm.v Asmblockprops.v\\
+    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asm.v Asmblockprops.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
     Asmblockdeps.v\\
     AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\