intermediatet commit before builtins

1 files changed, 1834 insertions, 0 deletions

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