(* *************************************************************)
(*                                                             *)
(*             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 Lia.
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. lia.
    + econstructor. reflexivity. lia. apply IHN; lia. 
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. lia.
  - 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 lia. rewrite zlt_true by lia.
      rewrite Z.shiftr_spec by lia. f_equal; lia. }
    destruct (Z.eqb_spec frag 0).
    + rewrite IHN.
      * destruct (zlt i p). rewrite zlt_true by lia. auto.
        destruct (zlt i (p + 16)); auto.
        rewrite ABOVE by lia. rewrite FRAG by lia. rewrite e, Z.testbit_0_l. auto.
      * lia.
      * intros; apply ABOVE; lia.
      * lia.
    + simpl. rewrite IHN.
      * destruct (zlt i (p + 16)).
        ** rewrite Zinsert_spec by lia. unfold proj_sumbool.
           rewrite zlt_true by lia.
           destruct (zlt i p).
           rewrite zle_false by lia. auto.
           rewrite zle_true by lia. simpl. symmetry; apply FRAG; lia.
        ** rewrite Z.ldiff_spec, Z.shiftl_spec by lia.
           change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by lia.
           rewrite zlt_false by lia. rewrite zlt_false by lia. apply andb_true_r. 
      * lia.
      * intros. rewrite Zinsert_spec by lia. unfold proj_sumbool.
        rewrite zle_true by lia. rewrite zlt_false by lia. simpl.
        apply ABOVE. lia.
      * lia.
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; lia. 
  lia. intros; apply Z.testbit_0_l. lia.
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 lia. rewrite Z.lnot_spec by lia. apply negb_involutive.
  lia. intros; apply Z.testbit_0_l. lia. lia.
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 lia.
  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 lia.
  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 lia. unfold proj_sumbool.
  destruct (zlt i p); [rewrite zle_false by lia|rewrite zle_true by lia]; simpl.
  - rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto.
  - rewrite Z.shiftl_spec by lia. 
    destruct (zlt i (p + l)); auto.
    rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by lia. 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 lia.
    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 lia. rewrite zlt_true by lia.
    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. lia. 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; lia.
    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; lia.
    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; lia.
    + rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; lia.
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. lia. 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; lia.
    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; lia.
    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; lia.
    + rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; lia.
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; lia).
  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; lia.
    intros; Simpl.
  - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
    split. Simpl. do 3 f_equal; lia.
    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; lia).
  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; lia.
    intros; Simpl.
  - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
    split. Simpl. do 3 f_equal; lia.
    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.mxcmpu Ceq v1 v2)
  /\ rs'#CC = (Val.mxcmpu 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.mxcmpu; 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.mxcmpu_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.mxcmpu; 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.mxcmplu Ceq v1 v2)
  /\ rs'#CC = (Val.mxcmplu 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.mxcmplu; 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.mxcmplu_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.mxcmplu.
  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_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.mxcmplu_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.mxcmplu_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.mxcmplu_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.mxcmplu_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.mxcmplu_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_cond_correct':
  forall cond args k c tbb 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) (incrPC (Ptrofs.repr (size tbb)) rs') = Some b)
  /\ forall r, data_preg r = true -> rs'#r = rs#r.
Proof.
  intros until m; intros TR.
  eapply transl_cond_correct; eauto.
Qed.
  
Lemma transl_cbranch_correct_1:
  forall cond args lbl c k b m rs tbb bdy,
  transl_cond_branch cond args lbl k = OK (bdy,c) ->
  eval_condition cond (map rs (map preg_of args)) m = Some b ->
  exists rs',
     exec_straight_opt ge lk bdy rs m k rs' m
  /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m =
        (if b then goto_label fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m else
        Next (incrPC (Ptrofs.repr (size tbb)) rs') m)
  /\ forall r, data_preg r = true -> rs'#r = rs#r.
Proof.
intros until bdy; intros TR EV.
  assert (Archi.ptr64 = true) as SF; auto.
  assert (DFL:
    transl_cond_branch_default cond args lbl k = OK (bdy,c) ->
    exists rs',
       exec_straight_opt ge lk bdy rs m k rs' m
    /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m = eval_branch fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m (Some b)
    /\ forall r, data_preg r = true -> rs'#r = rs#r).
  {
    unfold transl_cond_branch_default; intros. monadInv H.
    exploit transl_cond_correct'; eauto. intros (rs' & A & B & C).
    eexists; split.
    apply exec_straight_opt_intro. eexact A.
    split; auto. simpl. rewrite (B b) by auto. auto. 
  }
Local Opaque transl_cond transl_cond_branch_default.
  destruct args as [ | a1 args]; simpl in TR; auto.
  destruct args as [ | a2 args]; simpl in TR; auto.
  destruct cond; simpl in TR; auto.
  - (* Ccompimm *)
    destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; 
    apply Int.same_if_eq in N0; subst n; ArgsInv.
    + (* Ccompimm Cne 0 *)
      econstructor; split. econstructor.
      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV.
      unfold incrPC. Simpl. rewrite EQRSX. simpl. auto.
    + (* Ccompimm Ceq 0 *)
      econstructor; split. econstructor.
      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
      unfold incrPC. Simpl. rewrite EQRSX. simpl.
      destruct (Int.eq i Int.zero); auto.
  - (* Ccompuimm *)
    destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto.
    apply Int.same_if_eq in N0; subst n; ArgsInv.
    + (* Ccompuimm Cne 0 *)
      econstructor; split. econstructor.
      split; auto. simpl. apply Val.mxcmpu_bool_correct in EV.
      unfold incrPC. Simpl. rewrite EV. auto.
    + (* Ccompuimm Ceq 0 *)
      monadInv TR. ArgsInv. simpl in *.
      econstructor; split. econstructor.
      split; auto. simpl. unfold incrPC. Simpl.
      apply Int.same_if_eq in N0; subst.
      rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV.
      destruct b; auto.
  - (* Cmaskzero *)
    destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv.
    econstructor; split. econstructor.
    split; auto. simpl.
    erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto.
    unfold incrPC. Simpl.
    rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto.
  - (* Cmasknotzero *)
    destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv.
    econstructor; split. econstructor.
    split; auto. simpl.
    erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto.
    unfold incrPC. Simpl.
    rewrite EV. auto.
  - (* Ccomplimm *)
    destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; 
    apply Int64.same_if_eq in N0; subst n; ArgsInv.
    + (* Ccomplimm Cne 0 *)
      econstructor; split. econstructor.
      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV.
      unfold incrPC. Simpl. rewrite EQRSX. simpl. auto.
    + (* Ccomplimm Ceq 0 *)
      econstructor; split. econstructor.
      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
      unfold incrPC. Simpl. rewrite EQRSX. simpl.
      destruct (Int64.eq i Int64.zero); auto.
  - (* Ccompluimm *)
    destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto;
    apply Int64.same_if_eq in N0; subst n; ArgsInv.
    + (* Ccompluimm Cne 0 *)
      econstructor; split. econstructor.
      split; auto. simpl. apply Val.mxcmplu_bool_correct in EV.
      unfold incrPC. Simpl. rewrite EV. auto.
    + (* Ccompluimm Ceq 0 *)
      econstructor; split. econstructor.
      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
      unfold incrPC. Simpl. rewrite EQRSX. simpl.
      destruct (Int64.eq i Int64.zero); auto.
      unfold incrPC. Simpl. rewrite EQRSX. simpl.
      rewrite SF in *; simpl in *.
      rewrite Int64.eq_true in *.
      destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *.
      assert (b = true). { destruct b; try congruence. }
      rewrite H; auto. discriminate.
  - (* Cmasklzero *)
    destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv.
    econstructor; split. econstructor.
    split; auto.
    erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto.
    unfold incrPC. Simpl.
    rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto.
  - (* Cmasklnotzero *)
    destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv.
    econstructor; split. econstructor.
    split; auto.
    erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto.
    unfold incrPC. Simpl.
    rewrite EV. 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 storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset),
  Mem.storev Mint64 m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
  preg_of_iregsp base <> IR X16 ->
  (DR (IR (RR1 src))) <> (DR (IR (RR1 X16))) ->
  exists rs',
     exec_straight ge lk (storeptr_bc src base ofs k) rs m k rs' m'
  /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r.
Proof.
  intros. 
  destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
  exploit indexed_memory_access_correct; eauto. intros (ad & rs' & A & B & C). 
  econstructor; split.
  eapply exec_straight_opt_right. eexact A.
  apply exec_straight_one. simpl. unfold exec_store_rs_a. rewrite B, C, H. eauto.
  discriminate. auto.
  intros; Simpl. rewrite C; auto.
Qed.

Lemma loadind_correct:
  forall (base: iregsp) ofs ty dst k c (rs: regset) m v,
  loadind base ofs ty dst k = OK c ->
  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.