(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           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.                          *)
(*                                                             *)
(* *************************************************************)

(** * Translation from [Asmblock] to [AbstractBB] *)

(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmblock] into [L].
    [AbstractBB] will then define a sequential semantics for [L].
    We prove a bisimulation between the sequential semantics of [L] and [Asmblock].
    Then, the checker on [Asmblock] is deduced from those of [L].
 *)

Require Import AST.
Require Import Asm Asmblock.
Require Import Asmblockprops.
Require Import Values.
Require Import Globalenvs.
Require Import Memory.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import ZArith.
Require Import Coqlib.
Require Import ImpSimuTest.
Require Import Axioms.
Require Import Permutation.
Require Import Events.

Require Import Lia.

Import ListNotations.
Local Open Scope list_scope.

Open Scope impure.
(** auxiliary treatments of builtins *)

Definition is_builtin(ex: option control): bool :=
 match ex with
 | Some (Pbuiltin _ _ _) => true
 | _ => false
 end.

Definition has_builtin(bb: bblock): bool :=
 is_builtin (exit bb).

Remark builtin_arg_eq_dreg: forall (a b: builtin_arg dreg), {a=b} + {a<>b}.
Proof.
  intros.
  apply (builtin_arg_eq dreg_eq).
Qed.

Remark builtin_res_eq_dreg: forall (a b: builtin_res dreg), {a=b} + {a<>b}.
Proof. 
  intros. 
  apply (builtin_res_eq dreg_eq).
Qed.

Definition assert_same_builtin (bb1 bb2: bblock): ?? unit := 
  match exit bb1 with
  | Some (Pbuiltin ef1 lbar1 brr1) =>
     match exit bb2 with
     | Some (Pbuiltin ef2 lbar2 brr2) => 
        if (external_function_eq ef1 ef2) then
           if (list_eq_dec builtin_arg_eq_dreg lbar1 lbar2) then
              if (builtin_res_eq_dreg brr1 brr2) then RET tt
              else FAILWITH "Different brr in Pbuiltin"
           else FAILWITH "Different lbar in Pbuiltin"
        else FAILWITH "Different ef in Pbuiltin"
     | _ =>  FAILWITH "Expected a builtin: found something else" (* XXX: on peut raffiner le message d'erreur si nécessaire *)
     end
  | _ => match exit bb2 with
         | Some (Pbuiltin ef2 lbar2 brr2) => FAILWITH "Expected a something else: found a builtin"
         | _ => RET tt (* ok *)
         end
  end.

Lemma assert_same_builtin_correct (bb1 bb2: bblock):
  WHEN assert_same_builtin bb1 bb2 ~> _ THEN
    has_builtin bb1 = true \/ has_builtin bb2 = true -> exit bb1 = exit bb2.
Proof.
  unfold assert_same_builtin, has_builtin.
  destruct (exit bb1) as [[]|]; simpl;
  destruct (exit bb2) as [[]|]; wlp_simplify; try congruence.
Qed.
Global Opaque assert_same_builtin.
Local Hint Resolve assert_same_builtin_correct: wlp.

(** Definition of [L] *)

Module P<: ImpParam.
Module R := Pos.

Section IMPPARAM.

Definition env := Genv.t fundef unit.

Record genv_wrap := { _genv: env; _fn: function; _lk: aarch64_linker }.
Definition genv := genv_wrap.

Variable Ge: genv.

Inductive value_wrap :=
  | Val (v: val)
  | Memstate (m: mem)
  | Bool (b: bool)
.

Definition value := value_wrap.

Record CRflags := { _CN: val; _CZ:val; _CC: val; _CV: val }.

Inductive control_op :=
  | Ob (l: label)
  | Obc (c: testcond) (l: label)
  | Obl (id: ident)
  | Obs (id: ident)
  | Ocbnz (sz: isize) (l: label)
  | Ocbz (sz: isize) (l: label)
  | Otbnz (sz: isize) (n: int) (l: label)
  | Otbz (sz: isize) (n: int) (l: label)
  | Obtbl (l: list label)
  | OError
  | OIncremPC (sz: Z)
.

Inductive arith_op :=
  | OArithP (n: arith_p)
  | OArithPP (n: arith_pp)
  | OArithPPP (n: arith_ppp)
  | OArithRR0R (n: arith_rr0r)
  | OArithRR0R_XZR (n: arith_rr0r) (vz: val)
  | OArithRR0 (n: arith_rr0)
  | OArithRR0_XZR (n: arith_rr0) (vz: val)
  | OArithARRRR0 (n: arith_arrrr0)
  | OArithARRRR0_XZR (n: arith_arrrr0) (vz: val)
  | OArithComparisonPP_CN (n: arith_comparison_pp)
  | OArithComparisonPP_CZ (n: arith_comparison_pp)
  | OArithComparisonPP_CC (n: arith_comparison_pp)
  | OArithComparisonPP_CV (n: arith_comparison_pp)
  | OArithComparisonR0R_CN (n: arith_comparison_r0r) (is: isize)
  | OArithComparisonR0R_CZ (n: arith_comparison_r0r) (is: isize)
  | OArithComparisonR0R_CC (n: arith_comparison_r0r) (is: isize)
  | OArithComparisonR0R_CV (n: arith_comparison_r0r) (is: isize)
  | OArithComparisonR0R_CN_XZR (n: arith_comparison_r0r) (is: isize) (vz: val)
  | OArithComparisonR0R_CZ_XZR (n: arith_comparison_r0r) (is: isize) (vz: val)
  | OArithComparisonR0R_CC_XZR (n: arith_comparison_r0r) (is: isize) (vz: val)
  | OArithComparisonR0R_CV_XZR (n: arith_comparison_r0r) (is: isize) (vz: val)
  | OArithComparisonP_CN (n: arith_comparison_p)
  | OArithComparisonP_CZ (n: arith_comparison_p)
  | OArithComparisonP_CC (n: arith_comparison_p)
  | OArithComparisonP_CV (n: arith_comparison_p)
  | Ocset (c: testcond)
  | Ofmovi (fsz: fsize)
  | Ofmovi_XZR (fsz: fsize)
  | Ocsel (c: testcond)
  | Ofnmul (fsz: fsize)
.

Inductive store_op :=
  | Ostore1 (st: store_rs_a) (chunk: memory_chunk) (a: addressing)
  | Ostore2 (st: store_rs_a) (chunk: memory_chunk) (a: addressing)
  | OstoreU (st: store_rs_a) (chunk: memory_chunk) (a: addressing)
.

Inductive load_op :=
  | Oload1 (ld: load_rd_a) (chunk: memory_chunk) (a: addressing)
  | Oload2 (ld: load_rd_a) (chunk: memory_chunk) (a: addressing)
  | OloadU (ld: load_rd_a) (chunk: memory_chunk) (a: addressing)
.

Inductive allocf_op :=
  | OAllocf_SP (sz: Z) (linkofs: ptrofs)
  | OAllocf_Mem (sz: Z) (linkofs: ptrofs)
.

Inductive freef_op :=
  | OFreef_SP (sz: Z) (linkofs: ptrofs)
  | OFreef_Mem (sz: Z) (linkofs: ptrofs)
.

Inductive op_wrap :=
  (* arithmetic operation *)
  | Arith (op: arith_op)
  | Load (ld: load_op)
  | Store (st: store_op)
  | Allocframe (al: allocf_op)
  | Freeframe (fr: freef_op)
  | Loadsymbol (id: ident)
  | Cvtsw2x
  | Cvtuw2x
  | Cvtx2w
  | Control (co: control_op)
  | Constant (v: val)
.

Definition op:=op_wrap.

Coercion Arith: arith_op >-> op_wrap.
Coercion Control: control_op >-> op_wrap.

Definition v_compare_int (v1 v2: val) : CRflags :=
  {| _CN := (Val.negative (Val.sub v1 v2));
     _CZ := (Val.mxcmpu Ceq v1 v2);
     _CC := (Val.mxcmpu Cge v1 v2);
     _CV := (Val.sub_overflow v1 v2) |}.

Definition v_compare_long (v1 v2: val) : CRflags :=
  {| _CN := (Val.negativel (Val.subl v1 v2));
     _CZ := (Val.mxcmplu Ceq v1 v2);
     _CC := (Val.mxcmplu Cge v1 v2);
     _CV := (Val.subl_overflow v1 v2) |}.

Definition v_compare_float (v1 v2: val) : CRflags :=
  match v1, v2 with
  | Vfloat f1, Vfloat f2 =>
      {| _CN := (Val.of_bool (Float.cmp Clt f1 f2));
         _CZ := (Val.of_bool (Float.cmp Ceq f1 f2));
         _CC := (Val.of_bool (negb (Float.cmp Clt f1 f2)));
         _CV := (Val.of_bool (negb (Float.ordered f1 f2))) |}
  | _, _ =>
      {| _CN := Vundef;
         _CZ := Vundef;
         _CC := Vundef;
         _CV := Vundef |}
  end.

Definition v_compare_single (v1 v2: val) : CRflags :=
  match v1, v2 with
  | Vsingle f1, Vsingle f2 =>
      {| _CN := (Val.of_bool (Float32.cmp Clt f1 f2));
         _CZ := (Val.of_bool (Float32.cmp Ceq f1 f2));
         _CC := (Val.of_bool (negb (Float32.cmp Clt f1 f2)));
         _CV := (Val.of_bool (negb (Float32.ordered f1 f2))) |}
  | _, _ =>
      {| _CN := Vundef;
         _CZ := Vundef;
         _CC := Vundef;
         _CV := Vundef |}
  end.

Definition arith_eval_comparison_pp (n: arith_comparison_pp) (v1 v2: val) :=
  let (v1',v2') := arith_prepare_comparison_pp n v1 v2 in
  match n with 
  | Pcmpext _ | Pcmnext _ => v_compare_long v1' v2'
  | Pfcmp S => v_compare_single v1' v2'
  | Pfcmp D => v_compare_float v1' v2'
  end.

Definition arith_eval_comparison_p (n: arith_comparison_p) (v: val) :=
  let (v1',v2') := arith_prepare_comparison_p n v in
  match n with
  | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => v_compare_int v1' v2'
  | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => v_compare_long v1' v2'
  | Pfcmp0 S => v_compare_single v1' v2'
  | Pfcmp0 D => v_compare_float v1' v2'
  end.

Definition arith_eval_comparison_r0r (n: arith_comparison_r0r) (v1 v2: val) (is: isize) :=
  let (v1',v2') := arith_prepare_comparison_r0r n v1 v2 in
  if is then v_compare_int v1' v2' else v_compare_long v1' v2'.

Definition flags_testcond_value (c: testcond) (vCN vCZ vCC vCV: val) :=
  match c with
  | TCeq =>                             (**r equal *)
      match vCZ with
      | Vint n => Some (Int.eq n Int.one)
      | _ => None
      end
  | TCne =>                             (**r not equal *)
      match vCZ with
      | Vint n => Some (Int.eq n Int.zero)
      | _ => None
      end
  | TClo =>                             (**r unsigned less than  *)
      match vCC with
      | Vint n => Some (Int.eq n Int.zero)
      | _ => None
      end
  | TCls =>                             (**r unsigned less or equal *)
      match vCC, vCZ with
      | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one)
      | _, _ => None
      end
  | TChs =>                             (**r unsigned greater or equal *)
      match vCC with
      | Vint n => Some (Int.eq n Int.one)
      | _ => None
      end
  | TChi =>                             (**r unsigned greater *)
      match vCC, vCZ with
      | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero)
      | _, _ => None
      end
  | TClt =>                             (**r signed less than *)
      match vCV, vCN with
      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one)
      | _, _ => None
      end
  | TCle =>                             (**r signed less or equal *)
      match vCV, vCN, vCZ with
      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one)
      | _, _, _ => None
      end
  | TCge =>                             (**r signed greater or equal *)
      match vCV, vCN with
      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero)
      | _, _ => None
      end
  | TCgt =>                             (**r signed greater *)
      match vCV, vCN, vCZ with
      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero)
      | _, _, _ => None
      end
  | TCpl =>                             (**r positive *)
      match vCN with
      | Vint n => Some (Int.eq n Int.zero)
      | _ => None
      end
  | TCmi =>                             (**r negative *)
      match vCN with
      | Vint n => Some (Int.eq n Int.one)
      | _ => None
      end
  end.

(* The is argument is used to identify the source inst and avoid rewriting some code
  0 -> Ocset
  1 -> Ocsel
  2 -> Obc *)
Definition cond_eval_is (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) (is: Z) :=
  let res := flags_testcond_value c vCN vCZ vCC vCV in
  match is, res with
  | 0, res => Some (Val (if_opt_bool_val res (Vint Int.one) (Vint Int.zero)))
  | 1, res => Some (Val (if_opt_bool_val res v1 v2))
  | 2, Some b => Some (Bool (b))
  | _, _ => None
  end.

Definition fmovi_eval (fsz: fsize) (v: val) :=
  match fsz with
  | S => float32_of_bits v
  | D => float64_of_bits v
  end.

Definition fmovi_eval_xzr (fsz: fsize) :=
  match fsz with
  | S => float32_of_bits (Vint Int.zero)
  | D => float64_of_bits (Vlong Int64.zero)
  end.

Definition fnmul_eval (fsz: fsize) (v1 v2: val) :=
  match fsz with
  | S => Val.negfs (Val.mulfs v1 v2)
  | D => Val.negf (Val.mulf v1 v2)
  end.

Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is: Z) :=
  match c, l with
  | TCeq, [Val vCZ] => cond_eval_is TCeq v1 v2 Vundef vCZ Vundef Vundef is
  | TCne, [Val vCZ] => cond_eval_is TCne v1 v2 Vundef vCZ Vundef Vundef is
  | TChs, [Val vCC] => cond_eval_is TChs v1 v2 Vundef Vundef vCC Vundef is
  | TClo, [Val vCC] => cond_eval_is TClo v1 v2 Vundef Vundef vCC Vundef is
  | TCmi, [Val vCN] => cond_eval_is TCmi v1 v2 vCN Vundef Vundef Vundef is
  | TCpl, [Val vCN] => cond_eval_is TCpl v1 v2 vCN Vundef Vundef Vundef is
  | TChi, [Val vCZ; Val vCC] => cond_eval_is TChi v1 v2 Vundef vCZ vCC Vundef is
  | TCls, [Val vCZ; Val vCC] => cond_eval_is TCls v1 v2 Vundef vCZ vCC Vundef is
  | TCge, [Val vCN; Val vCV] => cond_eval_is TCge v1 v2 vCN Vundef Vundef vCV is
  | TClt, [Val vCN; Val vCV] => cond_eval_is TClt v1 v2 vCN Vundef Vundef vCV is
  | TCgt, [Val vCN; Val vCZ; Val vCV] => cond_eval_is TCgt v1 v2 vCN vCZ Vundef vCV is
  | TCle, [Val vCN; Val vCZ; Val vCV] => cond_eval_is TCle v1 v2 vCN vCZ Vundef vCV is
  | _, _ => None
  end.

Definition arith_op_eval (op: arith_op) (l: list value) :=
  match op, l with
  | OArithP n, [] => Some (Val (arith_eval_p Ge.(_lk) n))
  | OArithPP n, [Val v] => Some (Val (arith_eval_pp Ge.(_lk) n v))
  | OArithPPP n, [Val v1; Val v2] => Some (Val (arith_eval_ppp n v1 v2))
  | OArithRR0R n, [Val v1; Val v2] => Some (Val (arith_eval_rr0r n v1 v2))
  | OArithRR0R_XZR n vz, [Val v] => Some (Val (arith_eval_rr0r n vz v))
  | OArithRR0 n, [Val v] => Some (Val (arith_eval_rr0 n v))
  | OArithRR0_XZR n vz, [] => Some (Val (arith_eval_rr0 n vz))
  | OArithARRRR0 n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrrr0 n v1 v2 v3))
  | OArithARRRR0_XZR n vz, [Val v1; Val v2] => Some (Val (arith_eval_arrrr0 n v1 v2 vz))
  | OArithComparisonPP_CN n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CN)))
  | OArithComparisonPP_CZ n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CZ)))
  | OArithComparisonPP_CC n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CC)))
  | OArithComparisonPP_CV n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CV)))
  | OArithComparisonR0R_CN n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CN)))
  | OArithComparisonR0R_CZ n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CZ)))
  | OArithComparisonR0R_CC n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CC)))
  | OArithComparisonR0R_CV n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CV)))
  | OArithComparisonR0R_CN_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CN)))
  | OArithComparisonR0R_CZ_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CZ)))
  | OArithComparisonR0R_CC_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CC)))
  | OArithComparisonR0R_CV_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CV)))
  | OArithComparisonP_CN n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CN)))
  | OArithComparisonP_CZ n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CZ)))
  | OArithComparisonP_CC n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CC)))
  | OArithComparisonP_CV n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CV)))
  | Ocset c, l => cflags_eval c l Vundef Vundef 0
  | Ofmovi fsz, [Val v] => Some (Val (fmovi_eval fsz v))
  | Ofmovi_XZR fsz, [] => Some (Val (fmovi_eval_xzr fsz))
  | Ocsel c, Val v1 :: Val v2 :: l' => cflags_eval c l' v1 v2 1
  | Ofnmul fsz, [Val v1; Val v2] => Some (Val (fnmul_eval fsz v1 v2))
  | _, _ => None
  end.

Definition call_ll_storev (c: memory_chunk) (m: mem) (v: option val) (vs: val) :=
  match v with
  | Some va => match Mem.storev c m va vs with
               | Some m' => Some (Memstate m')
               | None => None
               end
  | None => None (* should never occurs *)
  end.

Definition exec_store1 (n: store_rs_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vr vs: val) :=
  let v :=
    match a with
    | ADimm _ n => Some (Val.addl vs (Vlong n))
    | ADadr _ id ofs => Some (Val.addl vs (symbol_low Ge.(_lk) id ofs))
    | _ => None
    end in
  call_ll_storev chunk m v vr.

Definition exec_store2 (n: store_rs_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vr vs1 vs2: val) :=
  let v :=
    match a with
    | ADreg _ _ => Some (Val.addl vs1 vs2)
    | ADlsl _ _ n => Some (Val.addl vs1 (Val.shll vs2 (Vint n)))
    | ADsxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofint vs2) (Vint n)))
    | ADuxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofintu vs2) (Vint n)))
    | _ => None
    end in
  call_ll_storev chunk m v vr.
  
Definition exec_storeU (n: store_rs_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vr: val) :=
  call_ll_storev chunk m None vr.

Definition goto_label_deps (f: function) (lbl: label) (vpc: val) :=
  match label_pos lbl 0 (fn_blocks f) with
  | None => None
  | Some pos =>
      match vpc with
      | Vptr b ofs => Some (Val (Vptr b (Ptrofs.repr pos)))
      | _          => None
      end
  end.

Definition control_eval (o: control_op) (l: list value) :=
  let (ge, fn, lk) := Ge in
  match o, l with
  | Ob lbl, [Val vpc] => goto_label_deps fn lbl vpc
  | Obc c lbl, Val vpc :: l' => match cflags_eval c l' Vundef Vundef 2 with
                                | Some (Bool true) => goto_label_deps fn lbl vpc
                                | Some (Bool false) => Some (Val vpc)
                                | _ => None
                                end
  | Obl id, [] => Some (Val (Genv.symbol_address Ge.(_genv) id Ptrofs.zero))
  | Obs id, [] => Some (Val (Genv.symbol_address Ge.(_genv) id Ptrofs.zero))
  | Ocbnz sz lbl, [Val v; Val vpc] => match eval_testzero sz v with
                                      | Some (true) => Some (Val vpc)
                                      | Some (false) => goto_label_deps fn lbl vpc
                                      | None => None
                                      end
  | Ocbz sz lbl, [Val v; Val vpc] => match eval_testzero sz v with
                                      | Some (true) => goto_label_deps fn lbl vpc
                                      | Some (false) => Some (Val vpc)
                                      | None => None
                                     end
  | Otbnz sz n lbl, [Val v; Val vpc] => match eval_testbit sz v n with
                                        | Some (true) => goto_label_deps fn lbl vpc
                                        | Some (false) => Some (Val vpc)
                                        | None => None
                                       end
  | Otbz sz n lbl, [Val v; Val vpc] => match eval_testbit sz v n with
                                        | Some (true) => Some (Val vpc)
                                        | Some (false) => goto_label_deps fn lbl vpc
                                        | None => None
                                       end
  | Obtbl tbl, [Val index; Val vpc] => match index with
                                       | Vint n => 
                                         match list_nth_z tbl (Int.unsigned n) with
                                         | None => None
                                         | Some lbl => goto_label_deps fn lbl vpc
                                         end
                                       | _ => None
                                       end
  | OIncremPC sz, [Val vpc] => Some (Val (Val.offset_ptr vpc (Ptrofs.repr sz)))
  | OError, _ => None
  | _, _ => None
  end.

Definition store_eval (o: store_op) (l: list value) :=
  match o, l with
  | Ostore1 st chunk a, [Val vr; Val vs; Memstate m] => exec_store1 st m chunk a vr vs
  | Ostore2 st chunk a, [Val vr; Val vs1; Val vs2; Memstate m] => exec_store2 st m chunk a vr vs1 vs2
  | OstoreU st chunk a, [Val vr; Memstate m] => exec_storeU st m chunk a vr
  | _, _ => None
  end.

Definition call_ll_loadv (c: memory_chunk) (transf: val -> val) (m: mem) (v: option val) :=
  match v with
  | Some va => match Mem.loadv c m va with
               | Some v' => Some (Val (transf v'))
               | None => None
               end
  | None => None (* should never occurs *)
  end.

Definition exec_load1 (ld: load_rd_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vl: val) :=
  let v :=
    match a with
    | ADimm _ n => Some (Val.addl vl (Vlong n))
    | ADadr _ id ofs => Some (Val.addl vl (symbol_low Ge.(_lk) id ofs))
    | _ => None
    end in
  call_ll_loadv chunk (interp_load ld) m v.

Definition exec_load2 (ld: load_rd_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vl1 vl2: val) :=
  let v :=
    match a with
    | ADreg _ _ => Some (Val.addl vl1 vl2)
    | ADlsl _ _ n => Some (Val.addl vl1 (Val.shll vl2 (Vint n)))
    | ADsxt _ _ n => Some (Val.addl vl1 (Val.shll (Val.longofint vl2) (Vint n)))
    | ADuxt _ _ n => Some (Val.addl vl1 (Val.shll (Val.longofintu vl2) (Vint n)))
    | _ => None
    end in
  call_ll_loadv chunk (interp_load ld) m v.
  
Definition exec_loadU (n: load_rd_a) (m: mem) (chunk: memory_chunk) (a: addressing) :=
  call_ll_loadv chunk (interp_load n) m None.

Definition load_eval (o: load_op) (l: list value) :=
  match o, l with
  | Oload1 ld chunk a, [Val vs; Memstate m] => exec_load1 ld m chunk a vs
  | Oload2 ld chunk a, [Val vs1; Val vs2; Memstate m] => exec_load2 ld m chunk a vs1 vs2
  | OloadU st chunk a, [Memstate m] => exec_loadU st m chunk a
  | _, _ => None
  end.

Definition eval_allocf (o: allocf_op) (l: list value) :=
  match o, l with
  | OAllocf_Mem sz linkofs, [Val spv; Memstate m] =>
      let (m1, stk) := Mem.alloc m 0 sz in
      let sp := (Vptr stk Ptrofs.zero) in
      call_ll_storev Mint64 m1 (Some (Val.offset_ptr sp linkofs)) spv
  | OAllocf_SP sz linkofs, [Val spv; Memstate m] =>
      let (m1, stk) := Mem.alloc m 0 sz in
      let sp := (Vptr stk Ptrofs.zero) in
      match call_ll_storev Mint64 m1 (Some (Val.offset_ptr sp linkofs)) spv with
      | None => None
      | Some ms => Some (Val sp)
      end
  | _, _ => None
  end.

Definition eval_freef (o: freef_op) (l: list value) :=
  match o, l with
  | OFreef_Mem sz linkofs, [Val spv; Memstate m] =>
      match call_ll_loadv Mint64 (fun v => v) m (Some (Val.offset_ptr spv linkofs)) with
      | None => None
      | Some v =>
          match spv with
          | Vptr stk ofs =>
              match Mem.free m stk 0 sz with
              | None => None
              | Some m' => Some (Memstate m')
              end
          | _ => None
          end
      end
  | OFreef_SP sz linkofs, [Val spv; Memstate m] =>
      match call_ll_loadv Mint64 (fun v => v) m (Some (Val.offset_ptr spv linkofs)) with
      | None => None
      | Some v =>
          match spv with
          | Vptr stk ofs =>
              match Mem.free m stk 0 sz with
              | None => None
              | Some m' => Some (v)
              end
          | _ => None
          end
      end
  | _, _ => None
  end.

Definition op_eval (op: op) (l:list value) :=
  match op, l with
  | Arith op, l => arith_op_eval op l
  | Load o, l => load_eval o l
  | Store o, l => store_eval o l
  | Allocframe o, l => eval_allocf o l
  | Freeframe o, l => eval_freef o l
  | Loadsymbol id, [] => Some (Val (Genv.symbol_address Ge.(_genv) id Ptrofs.zero))
  | Cvtsw2x, [Val v] => Some (Val (Val.longofint v))
  | Cvtuw2x, [Val v] => Some (Val (Val.longofintu v))
  | Cvtx2w, [Val v] => Some (Val (Val.loword v))
  | Control o, l => control_eval o l
  | Constant v, [] => Some (Val v)
  | _, _ => None
  end.

Definition vz_eq (vz1 vz2: val) : ?? bool :=
  RET (match vz1 with
       | Vint i1 => match vz2 with
                    | Vint i2 => Int.eq i1 i2
                    | _ => false
                    end
       | Vlong l1 => match vz2 with
                     | Vlong l2 => Int64.eq l1 l2
                     | _ => false
                     end
       | _ => false
       end).

Lemma vz_eq_correct vz1 vz2:
  WHEN vz_eq vz1 vz2 ~> b THEN b = true -> vz1 = vz2.
Proof.
  wlp_simplify.
  destruct vz1; destruct vz2; trivial; try discriminate.
  - eapply f_equal; apply Int.same_if_eq; auto.
  - eapply f_equal. apply Int64.same_if_eq; auto.
Qed.
Hint Resolve vz_eq_correct: wlp.

Definition is_eq (is1 is2: isize) : ?? bool :=
  RET (match is1 with
       | W => match is2 with
              | W => true
              | _ => false
              end
       | X => match is2 with
              | X => true
              | _ => false
              end
       end).

Lemma is_eq_correct is1 is2:
  WHEN is_eq is1 is2 ~> b THEN b = true -> is1 = is2.
Proof.
  wlp_simplify; destruct is1; destruct is2; trivial; try discriminate.
Qed.
Hint Resolve is_eq_correct: wlp.

Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
  match o1 with
  | OArithP n1 =>
      match o2 with OArithP n2 => phys_eq n1 n2 | _ => RET false end
  | OArithPP n1 =>
      match o2 with OArithPP n2 => phys_eq n1 n2 | _ => RET false end
  | OArithPPP n1 =>
      match o2 with OArithPPP n2 => phys_eq n1 n2 | _ => RET false end
  | OArithRR0R n1 =>
      match o2 with OArithRR0R n2 => phys_eq n1 n2 | _ => RET false end
  | OArithRR0R_XZR n1 vz1 =>
      match o2 with OArithRR0R_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end
  | OArithRR0 n1 =>
      match o2 with OArithRR0 n2 => phys_eq n1 n2 | _ => RET false end
  | OArithRR0_XZR n1 vz1 =>
      match o2 with OArithRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end
  | OArithARRRR0 n1 =>
      match o2 with OArithARRRR0 n2 => phys_eq n1 n2 | _ => RET false end
  | OArithARRRR0_XZR n1 vz1 =>
      match o2 with OArithARRRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end
  | OArithComparisonPP_CN n1 =>
      match o2 with OArithComparisonPP_CN n2 => phys_eq n1 n2 | _ => RET false end
  | OArithComparisonPP_CZ n1 =>
      match o2 with OArithComparisonPP_CZ n2 => phys_eq n1 n2 | _ => RET false end
  | OArithComparisonPP_CC n1 =>
      match o2 with OArithComparisonPP_CC n2 => phys_eq n1 n2 | _ => RET false end
  | OArithComparisonPP_CV n1 =>
      match o2 with OArithComparisonPP_CV n2 => phys_eq n1 n2 | _ => RET false end
  | OArithComparisonR0R_CN n1 is1 =>
      match o2 with OArithComparisonR0R_CN n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end
  | OArithComparisonR0R_CZ n1 is1 =>
      match o2 with OArithComparisonR0R_CZ n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end
  | OArithComparisonR0R_CC n1 is1 =>
      match o2 with OArithComparisonR0R_CC n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end
  | OArithComparisonR0R_CV n1 is1 =>
      match o2 with OArithComparisonR0R_CV n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end
  | OArithComparisonR0R_CN_XZR n1 is1 vz1 =>
      match o2 with OArithComparisonR0R_CN_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end
  | OArithComparisonR0R_CZ_XZR n1 is1 vz1 =>
      match o2 with OArithComparisonR0R_CZ_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end
  | OArithComparisonR0R_CC_XZR n1 is1 vz1 =>
      match o2 with OArithComparisonR0R_CC_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end
  | OArithComparisonR0R_CV_XZR n1 is1 vz1 =>
      match o2 with OArithComparisonR0R_CV_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end
  | OArithComparisonP_CN n1 =>
      match o2 with OArithComparisonP_CN n2 => phys_eq n1 n2 | _ => RET false end
  | OArithComparisonP_CZ n1 =>
      match o2 with OArithComparisonP_CZ n2 => phys_eq n1 n2 | _ => RET false end
  | OArithComparisonP_CC n1 =>
      match o2 with OArithComparisonP_CC n2 => phys_eq n1 n2 | _ => RET false end
  | OArithComparisonP_CV n1 =>
      match o2 with OArithComparisonP_CV n2 => phys_eq n1 n2 | _ => RET false end
  | Ocset c1 =>
      match o2 with Ocset c2 => struct_eq c1 c2 | _ => RET false end
  | Ofmovi fsz1 =>
      match o2 with Ofmovi fsz2 => phys_eq fsz1 fsz2 | _ => RET false end
  | Ofmovi_XZR fsz1 =>
      match o2 with Ofmovi_XZR fsz2 => phys_eq fsz1 fsz2 | _ => RET false end
  | Ocsel c1 =>
      match o2 with Ocsel c2 => struct_eq c1 c2 | _ => RET false end
  | Ofnmul fsz1 =>
      match o2 with Ofnmul fsz2 => phys_eq fsz1 fsz2 | _ => RET false end
  end.

Ltac my_wlp_simplify := wlp_xsimplify ltac:(intros; subst; simpl in * |- *; congruence || intuition eauto with wlp).

Lemma arith_op_eq_correct o1 o2:
  WHEN arith_op_eq o1 o2 ~> b THEN b = true -> o1 = o2.
Proof.
  destruct o1, o2; my_wlp_simplify; try congruence;
  try (destruct vz; destruct vz0); try (destruct is; destruct is0);
  repeat apply f_equal; try congruence;
  try apply Int.same_if_eq; try apply Int64.same_if_eq; try auto.
Qed.
Hint Resolve arith_op_eq_correct: wlp.
Opaque arith_op_eq_correct.

Definition control_op_eq (c1 c2: control_op): ?? bool :=
  match c1 with
  | Ob lbl1 =>
     match c2 with Ob lbl2 => phys_eq lbl1 lbl2 | _ => RET false end
  | Obc c1 lbl1 =>
     match c2 with Obc c2 lbl2 => iandb (struct_eq c1 c2) (phys_eq lbl1 lbl2) | _ => RET false end
  | Obl id1 =>
     match c2 with Obl id2 => phys_eq id1 id2 | _ => RET false end
  | Obs id1 =>
     match c2 with Obs id2 => phys_eq id1 id2 | _ => RET false end
  | Ocbnz sz1 lbl1 =>
     match c2 with Ocbnz sz2 lbl2 => iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2) | _ => RET false end
  | Ocbz sz1 lbl1 =>
     match c2 with Ocbz sz2 lbl2 => iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2) | _ => RET false end
  | Otbnz sz1 n1 lbl1 =>
     match c2 with Otbnz sz2 n2 lbl2 => iandb (RET (Int.eq n1 n2)) (iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2)) | _ => RET false end
  | Otbz sz1 n1 lbl1 =>
     match c2 with Otbz sz2 n2 lbl2 => iandb (RET (Int.eq n1 n2)) (iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2)) | _ => RET false end
  | Obtbl tbl1 =>
     match c2 with Obtbl tbl2 => (phys_eq tbl1 tbl2) | _ => RET false end
  | OIncremPC sz1 =>
      match c2 with OIncremPC sz2 => RET (Z.eqb sz1 sz2) | _ => RET false end
  | OError =>
     match c2 with OError => RET true | _ => RET false end
  end.

Lemma control_op_eq_correct c1 c2:
  WHEN control_op_eq c1 c2 ~> b THEN b = true -> c1 = c2.
Proof.
  destruct c1, c2; wlp_simplify; try rewrite Z.eqb_eq in * |-; try congruence;
  try apply Int.same_if_eq in H; try congruence.
Qed.
Hint Resolve control_op_eq_correct: wlp.
Opaque control_op_eq_correct.

Definition store_op_eq (s1 s2: store_op): ?? bool :=
  match s1 with
  | Ostore1 st1 chk1 a1 =>
      match s2 with Ostore1 st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end
  | Ostore2 st1 chk1 a1 =>
      match s2 with Ostore2 st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end
  | OstoreU st1 chk1 a1 =>
      match s2 with OstoreU st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end
  end.

Lemma store_op_eq_correct s1 s2:
  WHEN store_op_eq s1 s2 ~> b THEN b = true -> s1 = s2.
Proof.
  destruct s1, s2; wlp_simplify; try congruence.
  all: rewrite H1 in H0; rewrite H0, H; reflexivity.
Qed.
Hint Resolve store_op_eq_correct: wlp.
Opaque store_op_eq_correct.

Definition load_op_eq (l1 l2: load_op): ?? bool :=
  match l1 with
  | Oload1 ld1 chk1 a1 =>
      match l2 with Oload1 ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end
  | Oload2 ld1 chk1 a1 =>
      match l2 with Oload2 ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end
  | OloadU ld1 chk1 a1 =>
      match l2 with OloadU ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end
  end.

Lemma load_op_eq_correct l1 l2:
  WHEN load_op_eq l1 l2 ~> b THEN b = true -> l1 = l2.
Proof.
  destruct l1, l2; wlp_simplify; try congruence.
  all: rewrite H1 in H0; rewrite H, H0; reflexivity.
Qed.
Hint Resolve load_op_eq_correct: wlp.
Opaque load_op_eq_correct.

Definition allocf_op_eq (al1 al2: allocf_op): ?? bool :=
  match al1 with
  | OAllocf_SP sz1 linkofs1 =>
      match al2 with OAllocf_SP sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq linkofs1 linkofs2) | _ => RET false end
  | OAllocf_Mem sz1 linkofs1 =>
      match al2 with OAllocf_Mem sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq linkofs1 linkofs2) | _ => RET false end
  end.

Lemma allocf_op_eq_correct al1 al2:
  WHEN allocf_op_eq al1 al2 ~> b THEN b = true -> al1 = al2.
Proof.
  destruct al1, al2; wlp_simplify; try congruence.
  all: rewrite H2; rewrite Z.eqb_eq in H; rewrite H; reflexivity.
Qed.
Hint Resolve allocf_op_eq_correct: wlp.
Opaque allocf_op_eq_correct.

Definition freef_op_eq (fr1 fr2: freef_op): ?? bool :=
  match fr1 with
  | OFreef_SP sz1 linkofs1 =>
      match fr2 with OFreef_SP sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq linkofs1 linkofs2) | _ => RET false end
  | OFreef_Mem sz1 linkofs1 =>
      match fr2 with OFreef_Mem sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq linkofs1 linkofs2) | _ => RET false end
  end.

Lemma freef_op_eq_correct fr1 fr2:
  WHEN freef_op_eq fr1 fr2 ~> b THEN b = true -> fr1 = fr2.
Proof.
  destruct fr1, fr2; wlp_simplify; try congruence.
  all: rewrite H2; rewrite Z.eqb_eq in H; rewrite H; reflexivity.
Qed.
Hint Resolve freef_op_eq_correct: wlp.
Opaque freef_op_eq_correct.

Definition op_eq (o1 o2: op): ?? bool :=
  match o1 with
  | Arith i1 =>
    match o2 with Arith i2 => arith_op_eq i1 i2 | _ => RET false end
  | Control i1 =>
    match o2 with Control i2 => control_op_eq i1 i2 | _ => RET false end
  | Load i1 =>
      match o2 with Load i2 => load_op_eq i1 i2 | _ => RET false end
  | Store i1 =>
      match o2 with Store i2 => store_op_eq i1 i2 | _ => RET false end
  | Allocframe i1 =>
      match o2 with Allocframe i2 => allocf_op_eq i1 i2 | _ => RET false end
  | Freeframe i1 =>
      match o2 with Freeframe i2 => freef_op_eq i1 i2 | _ => RET false end
  | Loadsymbol id1 =>
      match o2 with Loadsymbol id2 => phys_eq id1 id2 | _ => RET false end
  | Cvtsw2x =>
    match o2 with Cvtsw2x => RET true | _ => RET false end
  | Cvtuw2x =>
    match o2 with Cvtuw2x => RET true | _ => RET false end
  | Cvtx2w =>
    match o2 with Cvtx2w => RET true | _ => RET false end
  | Constant c1 =>
    match o2 with Constant c2 => phys_eq c1 c2 | _ => RET false end
  end.

Lemma op_eq_correct o1 o2: 
 WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2.
Proof.
  destruct o1, o2; wlp_simplify; congruence.
Qed.

End IMPPARAM.

End P.

Module L <: ISeqLanguage with Module LP:=P.

Module LP:=P.

Include MkSeqLanguage P.

End L.

Module IST := ImpSimu L ImpPosDict.

Import L.
Import P.

(** Compilation from [Asmblock] to [L] *)

Local Open Scope positive_scope.

Definition pmem : R.t := 1.

Definition ireg_to_pos (ir: ireg) : R.t :=
  match ir with
  | X0 => 8 | X1 => 9 | X2 => 10 | X3 => 11 | X4 => 12 | X5 => 13 | X6 => 14 | X7 => 15
  | X8 => 16 | X9 => 17 | X10 => 18 | X11 => 19 | X12 => 20 | X13 => 21 | X14 => 22 | X15 => 23
  | X16 => 24 | X17 => 25 | X18 => 26 | X19 => 27 | X20 => 28 | X21 => 29 | X22 => 30 | X23 => 31
  | X24 => 32 | X25 => 33 | X26 => 34 | X27 => 35 | X28 => 36 | X29 => 37 | X30 => 38
  end
.

Definition freg_to_pos (fr: freg) : R.t :=
  match fr with
  | D0 => 39 | D1 => 40 | D2 => 41 | D3 => 42 | D4 => 43 | D5 => 44 | D6 => 45 | D7 => 46
  | D8 => 47 | D9 => 48 | D10 => 49 | D11 => 50 | D12 => 51 | D13 => 52 | D14 => 53 | D15 => 54
  | D16 => 55 | D17 => 56 | D18 => 57 | D19 => 58 | D20 => 59 | D21 => 60 | D22 => 61 | D23 => 62
  | D24 => 63 | D25 => 64 | D26 => 65 | D27 => 66 | D28 => 67 | D29 => 68 | D30 => 69 | D31 => 70
  end
.

Lemma ireg_to_pos_discr: forall r r', r <> r' -> ireg_to_pos r <> ireg_to_pos r'.
Proof.
  destruct r; destruct r'; try contradiction; discriminate.
Qed.

Lemma freg_to_pos_discr: forall r r', r <> r' -> freg_to_pos r <> freg_to_pos r'.
Proof.
  destruct r; destruct r'; try contradiction; discriminate.
Qed.

Definition ppos (r: preg) : R.t :=
  match r with
  | CR c => match c with
            | CN => 2
            | CZ => 3
            | CC => 4
            | CV => 5
            end
  | PC => 6
  | DR d => match d with
            | IR i => match i with
                      | XSP => 7
                      | RR1 ir => ireg_to_pos ir
                      end
            | FR fr => freg_to_pos fr
            end
  end
.

Notation "# r" := (ppos r) (at level 100, right associativity). 

Lemma not_eq_add:
  forall k n n', n <> n' -> k + n <> k + n'.
Proof.
  intros k n n' H1 H2. apply H1; clear H1. eapply Pos.add_reg_l; eauto.
Qed.

Lemma ppos_equal: forall r r', r = r' <-> ppos r = ppos r'.
Proof.
  destruct r as [dr|cr|]; destruct r' as [dr'|cr'|];
  try destruct dr as [ir|fr]; try destruct dr' as [ir'|fr'];
  try destruct ir as [irr|]; try destruct ir' as [irr'|].
  all: split; intros; try rewrite H; try discriminate; try contradiction; simpl; eauto;
  try destruct irr; try destruct irr';
  try destruct fr; try destruct fr';
  try destruct cr; try destruct cr';
  simpl; try discriminate; try reflexivity.
Qed.

Lemma ppos_discr: forall r r', r <> r' <-> ppos r <> ppos r'.
Proof.
  split; unfold not; try intros; try apply ppos_equal in H0; try discriminate; try contradiction.
Qed.

Lemma ppos_pmem_discr: forall r, pmem <> ppos r.
Proof.
  intros. destruct r as [dr|cr|].
  - destruct dr as [ir|fr]; try destruct ir as [irr|]; try destruct irr; try destruct fr;
    unfold ppos; unfold pmem; discriminate.
  - unfold ppos; unfold pmem; destruct cr; discriminate.
  - unfold ppos; unfold pmem; discriminate.
Qed.

(** Inversion functions, used for debug traces *)

Definition pos_to_ireg (p: R.t) : option ireg :=
  match p with
  | 8 => Some (X0) | 9 => Some (X1) | 10 => Some (X2) | 11 => Some (X3) | 12 => Some (X4) | 13 => Some (X5) | 14 => Some (X6) | 15 => Some (X7)
  | 16 => Some (X8) | 17 => Some (X9) | 18 => Some (X10) | 19 => Some (X11) | 20 => Some (X12) | 21 => Some (X13) | 22 => Some (X14) | 23 => Some (X15)
  | 24 => Some (X16) | 25 => Some (X17) | 26 => Some (X18) | 27 => Some (X19) | 28 => Some (X20) | 29 => Some (X21) | 30 => Some (X22) | 31 => Some (X23)
  | 32 => Some (X24) | 33 => Some (X25) | 34 => Some (X26) | 35 => Some (X27) | 36 => Some (X28) | 37 => Some (X29) | 38 => Some (X30) | _ => None
  end.

Definition pos_to_freg (p: R.t) : option freg :=
  match p with
  | 39 => Some(D0) | 40 => Some(D1) | 41 => Some(D2) | 42 => Some(D3) | 43 => Some(D4) | 44 => Some(D5) | 45 => Some(D6) | 46 => Some(D7)
  | 47 => Some(D8) | 48 => Some(D9) | 49 => Some(D10) | 50 => Some(D11) | 51 => Some(D12) | 52 => Some(D13) | 53 => Some(D14) | 54 => Some(D15)
  | 55 => Some(D16) | 56 => Some(D17) | 57 => Some(D18) | 58 => Some(D19) | 59 => Some(D20) | 60 => Some(D21) | 61 => Some(D22) | 62 => Some(D23)
  | 63 => Some(D24) | 64 => Some(D25) | 65 => Some(D26) | 66 => Some(D27) | 67 => Some(D28) | 68 => Some(D29) | 69 => Some(D30) | 70 => Some(D31) | _ => None
  end.

Definition inv_ppos (p: R.t) : option preg :=
  match p with
  | 1 => None
  | 2 => Some (CR CN)
  | 3 => Some (CR CZ)
  | 4 => Some (CR CC)
  | 5 => Some (CR CV)
  | 6 => Some (PC)
  | 7 => Some (DR (IR XSP))
  | n => match pos_to_ireg n with
         | None => match pos_to_freg n with
                   | None => None
                   | Some fr => Some (DR (FR fr))
                   end
         | Some ir => Some (DR (IR ir))
         end
  end.

Notation "a @ b" := (Econs a b) (at level 102, right associativity).

(** Translations of instructions *)

Definition get_testcond_rlocs (c: testcond) :=
  match c with
  | TCeq => (PReg(#CZ) @ Enil)
  | TCne => (PReg(#CZ) @ Enil)
  | TChs => (PReg(#CC) @ Enil)
  | TClo => (PReg(#CC) @ Enil)
  | TCmi => (PReg(#CN) @ Enil)
  | TCpl => (PReg(#CN) @ Enil)
  | TChi => (PReg(#CZ) @ PReg(#CC) @ Enil)
  | TCls => (PReg(#CZ) @ PReg(#CC) @ Enil)
  | TCge => (PReg(#CN) @ PReg(#CV) @ Enil)
  | TClt => (PReg(#CN) @ PReg(#CV) @ Enil)
  | TCgt => (PReg(#CN) @ PReg(#CZ) @ PReg(#CV) @ Enil)
  | TCle => (PReg(#CN) @ PReg(#CZ) @ PReg(#CV) @ Enil)
  end.

Definition trans_control (ctl: control) : inst :=
  match ctl with
  | Pb lbl => [(#PC, Op (Control (Ob lbl)) (PReg(#PC) @ Enil))]
  | Pbc c lbl =>
      let lr := get_testcond_rlocs c in
      [(#PC, Op (Control (Obc c lbl)) (PReg(#PC) @ lr))]
  | Pbl id sg => [(#RA, PReg(#PC));
                  (#PC, Op (Control (Obl id)) Enil)]
  | Pbs id sg => [(#PC, Op (Control (Obs id)) Enil)]
  | Pblr r sg => [(#RA, PReg(#PC));
                  (#PC, Old (PReg(#r)))]
  | Pbr r sg => [(#PC, PReg(#r))]
  | Pret r => [(#PC, PReg(#r))]
  | Pcbnz sz r lbl => [(#PC, Op (Control (Ocbnz sz lbl)) (PReg(#r) @ PReg(#PC) @ Enil))]
  | Pcbz sz r lbl => [(#PC, Op (Control (Ocbz sz lbl)) (PReg(#r) @ PReg(#PC) @ Enil))]
  | Ptbnz sz r n lbl => [(#PC, Op (Control (Otbnz sz n lbl)) (PReg(#r) @ PReg(#PC) @ Enil))]
  | Ptbz sz r n lbl => [(#PC, Op (Control (Otbz sz n lbl)) (PReg(#r) @ PReg(#PC) @ Enil))]
  | Pbtbl r tbl => [(#X16, Op (Constant Vundef) Enil);
                    (#PC, Op (Control (Obtbl tbl)) (PReg(#r) @ PReg(#PC) @ Enil));
                    (#X16, Op (Constant Vundef) Enil)]
  | Pbuiltin ef args res => []
  end.

Definition trans_exit (ex: option control) : L.inst :=
  match ex with
  | None => []
  | Some ctl => trans_control ctl
  end
.

Definition trans_arith (ai: ar_instruction) : inst :=
  match ai with
  | PArithP n rd => 
      if destroy_X16 n then [(#rd, Op(Arith (OArithP n)) Enil); (#X16, Op (Constant Vundef) Enil)]
      else [(#rd, Op(Arith (OArithP n)) Enil)]
  | PArithPP n rd r1 => [(#rd, Op(Arith (OArithPP n)) (PReg(#r1) @ Enil))]
  | PArithPPP n rd r1 r2 => [(#rd, Op(Arith (OArithPPP n)) (PReg(#r1) @ PReg(#r2) @ Enil))]
  | PArithRR0R n rd r1 r2 =>
      let lr := match r1 with
                | RR0 r1' => Op(Arith (OArithRR0R n)) (PReg(#r1') @ PReg(#r2) @ Enil)
                | XZR => let vz := if arith_rr0r_isize n then Vint Int.zero else Vlong Int64.zero in
                         Op(Arith (OArithRR0R_XZR n vz)) (PReg(#r2) @ Enil)
                end in
      [(#rd,  lr)]
  | PArithRR0 n rd r1 =>
      let lr := match r1 with
                | RR0 r1' => Op(Arith (OArithRR0 n)) (PReg(#r1') @ Enil)
                | XZR => let vz := if arith_rr0_isize n then Vint Int.zero else Vlong Int64.zero in
                         Op(Arith (OArithRR0_XZR n vz)) (Enil)
                end in
      [(#rd, lr)]
  | PArithARRRR0 n rd r1 r2 r3 =>
      let lr := match r3 with
                | RR0 r3' => Op(Arith (OArithARRRR0 n)) (PReg(#r1) @ PReg (#r2) @ PReg(#r3') @ Enil)
                | XZR => let vz := if arith_arrrr0_isize n then Vint Int.zero else Vlong Int64.zero in
                         Op(Arith (OArithARRRR0_XZR n vz)) (PReg(#r1) @ PReg(#r2) @ Enil)
                end in
      [(#rd, lr)]
  | PArithComparisonPP n r1 r2 =>
      [(#CN, Op(Arith (OArithComparisonPP_CN n)) (PReg(#r1) @ PReg(#r2) @ Enil));
       (#CZ, Op(Arith (OArithComparisonPP_CZ n)) (PReg(#r1) @ PReg(#r2) @ Enil));
       (#CC, Op(Arith (OArithComparisonPP_CC n)) (PReg(#r1) @ PReg(#r2) @ Enil));
       (#CV, Op(Arith (OArithComparisonPP_CV n)) (PReg(#r1) @ PReg(#r2) @ Enil))]
  | PArithComparisonR0R n r1 r2 =>
      let is := arith_comparison_r0r_isize n in
      match r1 with
      | RR0 r1' => [(#CN, Op(Arith (OArithComparisonR0R_CN n is)) (PReg(#r1') @ PReg(#r2) @ Enil));
                    (#CZ, Op(Arith (OArithComparisonR0R_CZ n is)) (PReg(#r1') @ PReg(#r2) @ Enil));
                    (#CC, Op(Arith (OArithComparisonR0R_CC n is)) (PReg(#r1') @ PReg(#r2) @ Enil));
                    (#CV, Op(Arith (OArithComparisonR0R_CV n is)) (PReg(#r1') @ PReg(#r2) @ Enil))]
      | XZR => let vz := if is then Vint Int.zero else Vlong Int64.zero in
          [(#CN, Op(Arith (OArithComparisonR0R_CN_XZR n is vz)) (PReg(#r2) @ Enil));
                (#CZ, Op(Arith (OArithComparisonR0R_CZ_XZR n is vz)) (PReg(#r2) @ Enil));
                (#CC, Op(Arith (OArithComparisonR0R_CC_XZR n is vz)) (PReg(#r2) @ Enil));
                (#CV, Op(Arith (OArithComparisonR0R_CV_XZR n is vz)) (PReg(#r2) @ Enil))]
      end
  | PArithComparisonP n r1 =>
      [(#CN, Op(Arith (OArithComparisonP_CN n)) (PReg(#r1) @ Enil));
       (#CZ, Op(Arith (OArithComparisonP_CZ n)) (PReg(#r1) @ Enil));
       (#CC, Op(Arith (OArithComparisonP_CC n)) (PReg(#r1) @ Enil));
       (#CV, Op(Arith (OArithComparisonP_CV n)) (PReg(#r1) @ Enil))]
  | Pcset rd c =>
      let lr := get_testcond_rlocs c in
      [(#rd, Op(Arith (Ocset c)) lr)]
  | Pfmovi fsz rd r1 =>
      let lr := match r1 with
                | RR0 r1' => Op(Arith (Ofmovi fsz)) (PReg(#r1') @ Enil)
                | XZR => Op(Arith (Ofmovi_XZR fsz)) Enil
                end in
      [(#rd, lr)]
  | Pcsel rd r1 r2 c =>
      let lr := get_testcond_rlocs c in
      [(#rd, Op(Arith (Ocsel c)) (PReg(#r1) @ PReg (#r2) @ lr))]
  | Pfnmul fsz rd r1 r2 => [(#rd, Op(Arith (Ofnmul fsz)) (PReg(#r1) @ PReg(#r2) @ Enil))]
  end.

Definition eval_addressing_rlocs_st (st: store_rs_a) (chunk: memory_chunk) (rs: dreg) (a: addressing) :=
  match a with
  | ADimm base n => Op (Store (Ostore1 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil)
  | ADreg base r => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADlsl base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADsxt base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADuxt base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADadr base id ofs => Op (Store (Ostore1 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil)
  | ADpostincr base n => Op (Store (OstoreU st chunk a)) (PReg (#rs) @ PReg (pmem) @ Enil) (* not modeled yet *)
  end.

Definition eval_addressing_rlocs_ld (ld: load_rd_a) (chunk: memory_chunk) (a: addressing) :=
  match a with
  | ADimm base n => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil)
  | ADreg base r => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADlsl base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADsxt base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADuxt base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADadr base id ofs => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil)
  | ADpostincr base n => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil)
  end.

Definition trans_ldp_chunk (chunk: memory_chunk) (r: dreg): load_rd_a :=
  match chunk with
  | Mint32 => Pldrw
  | Mint64 => Pldrx
  | Mfloat32 => Pldrs
  | Mfloat64 => Pldrd
  | Many32 => Pldrw_a
  | _ => (* This case should always correspond to Many64 *)
    match r with
    | IR _ => Pldrx_a
    | FR _ => Pldrd_a
    end
  end.

Definition trans_stp_chunk (chunk: memory_chunk) (r: dreg): store_rs_a :=
  match chunk with
  | Mint32 => Pstrw
  | Mint64 => Pstrx
  | Mfloat32 => Pstrs
  | Mfloat64 => Pstrd
  | Many32 => Pstrw_a
  | _ => (* This case should always correspond to Many64 *)
    match r with
    | IR _ => Pstrx_a
    | FR _ => Pstrd_a
    end
  end.

Definition trans_load (ldi: ld_instruction) :=
  match ldi with
  | PLd_rd_a ld r a =>
      let lr := eval_addressing_rlocs_ld ld (chunk_load ld) a in [(#r, lr)]
  | Pldp ld r1 r2 chk1 chk2 a =>
      let ldi1 := trans_ldp_chunk chk1 r1 in
      let ldi2 := trans_ldp_chunk chk2 r1 in
      let lr := eval_addressing_rlocs_ld ldi1 chk1 a in
      let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4%Z | _ => 8%Z end in
      match a with
      | ADimm base n =>
        let a' := (get_offset_addr a ofs) in
          [(#r1, lr);
           (#r2, Op (Load (Oload1 ldi2 chk2 a'))
            (Old(PReg (#base)) @ PReg (pmem) @ Enil))]
      | _ => [(#PC, (Op (OError)) Enil)]
      end
  end.

Definition trans_store (sti: st_instruction) :=
  match sti with
  | PSt_rs_a st r a =>
      let lr := eval_addressing_rlocs_st st (chunk_store st) r a in [(pmem, lr)]
  | Pstp st r1 r2 chk1 chk2 a =>
      let sti1 := trans_stp_chunk chk1 r1 in
      let sti2 := trans_stp_chunk chk2 r1 in
      let lr := eval_addressing_rlocs_st sti1 chk1 r1 a in
      let ofs := match chk1 with | Mint32 | Mfloat32| Many32 => 4%Z | _ => 8%Z end in
      match a with
      | ADimm base n =>
        let a' := (get_offset_addr a ofs) in
          [(pmem, lr);
           (pmem, Op (Store (Ostore1 sti2 chk2 a'))
            (PReg (#r2) @ Old(PReg (#base)) @ PReg (pmem) @ Enil))]
      | _ => [(#PC, (Op (OError)) Enil)]
      end
  end.

Definition trans_basic (b: basic) : inst :=
  match b with
  | PArith ai => trans_arith ai
  | PLoad ld => trans_load ld
  | PStore st => trans_store st
  | Pallocframe sz linkofs =>
      [(#X29, PReg(#SP));
       (#SP, Op (Allocframe (OAllocf_SP sz linkofs)) (PReg (#SP) @ PReg pmem @ Enil));
       (#X16, Op (Constant Vundef) Enil);
       (pmem, Op (Allocframe (OAllocf_Mem sz linkofs)) (Old(PReg(#SP)) @ PReg pmem @ Enil))]
  | Pfreeframe sz linkofs =>
      [(pmem, Op (Freeframe (OFreef_Mem sz linkofs)) (PReg (#SP) @ PReg pmem @ Enil));
       (#SP, Op (Freeframe (OFreef_SP sz linkofs)) (PReg (#SP) @ Old (PReg pmem) @ Enil));
       (#X16, Op (Constant Vundef) Enil)]
  | Ploadsymbol rd id => [(#rd, Op (Loadsymbol id) Enil)]
  | Pcvtsw2x rd r1 => [(#rd, Op (Cvtsw2x) (PReg (#r1) @ Enil))]
  | Pcvtuw2x rd r1 => [(#rd, Op (Cvtuw2x) (PReg (#r1) @ Enil))]
  | Pcvtx2w rd => [(#rd, Op (Cvtx2w) (PReg (#rd) @ Enil))]
  | Pnop => []
  end.

Fixpoint trans_body (b: list basic) : list L.inst :=
  match b with
  | nil => nil
  | b :: lb => (trans_basic b) :: (trans_body lb)
  end.

Definition trans_pcincr (sz: Z) (k: L.inst) := (#PC, Op (Control (OIncremPC sz)) (PReg(#PC) @ Enil)) :: k.

Definition trans_block (b: Asmblock.bblock) : L.bblock :=
  trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil).

(*Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb.*)
(*Proof.*)
  (*intros. destruct bb as [hd bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.*)
(*Qed.*)

(*Theorem trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb.*)
(*Proof.*)
  (*intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.*)
(*Qed.*)

(** Lemmas on the translation *)

Definition state := L.mem.
Definition exec := L.run.

Definition match_states (s: Asm.state) (s': state) :=
  let (rs, m) := s in
     s' pmem = Memstate m
  /\ forall r, s' (#r) = Val (rs r).

Definition match_outcome (o:outcome) (s: option state) :=
  match o with
  | Some n => exists s', s=Some s' /\ match_states n s'
  | None => s=None
  end.
 
Notation "a <[ b <- c ]>" := (assign a b c) (at level 102, right associativity).

Definition trans_state (s: Asm.state) : state :=
  let (rs, m) := s in
  fun x => if (Pos.eq_dec x pmem) then Memstate m
           else match (inv_ppos x) with
           | Some r => Val (rs r)
           | None => Val Vundef
           end.

Lemma not_eq_IR:
  forall r r', r <> r' -> IR r <> IR r'.
Proof.
  intros. congruence.
Qed.

Lemma ireg_pos_ppos: forall r,
  ireg_to_pos r = # r.
Proof.
  intros. simpl. reflexivity.
Qed.

Lemma freg_pos_ppos: forall r,
  freg_to_pos r = # r.
Proof.
  intros. simpl. reflexivity.
Qed.

Lemma ireg_not_pc: forall r,
  (#PC) <> ireg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma ireg_not_pmem: forall r,
  ireg_to_pos r <> pmem.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma ireg_not_CN: forall r,
  2 <> ireg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma ireg_not_CZ: forall r,
  3 <> ireg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma ireg_not_CC: forall r,
  4 <> ireg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma ireg_not_CV: forall r,
  5 <> ireg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma freg_not_pmem: forall r,
  freg_to_pos r <> pmem.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma freg_not_CN: forall r,
  2 <> freg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma freg_not_CZ: forall r,
  3 <> freg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma freg_not_CC: forall r,
  4 <> freg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma freg_not_CV: forall r,
  5 <> freg_to_pos r.
Proof.
  intros; destruct r; discriminate.
Qed.

Lemma dreg_not_pmem: forall (r: dreg),
  (# r) <> pmem.
Proof.
  intros; destruct r as [i|f].
  - destruct i. apply ireg_not_pmem. discriminate.
  - apply freg_not_pmem.
Qed.

Ltac DPRM pr :=
  destruct pr as [drDPRF|crDPRF|]; 
      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |]
      | destruct crDPRF|].

Ltac DPRF pr :=
  destruct pr as [drDPRF|crDPRF|]; 
      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|]
      | destruct frDPRF]
      | destruct crDPRF|].

Lemma preg_not_pmem: forall r,
  pmem <> # r.
Proof.
  intros. DPRF r; simpl; discriminate.
Qed.

Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl.

Lemma dreg_not_CN: forall (r: dreg),
  2 <> (#r).
Proof.
  intros; DIRN1 r; [ apply ireg_not_CN | discriminate | apply freg_not_CN].
Qed.

Lemma dreg_not_CZ: forall (r: dreg),
  3 <> (#r).
Proof.
  intros; DIRN1 r; [ apply ireg_not_CZ | discriminate | apply freg_not_CZ].
Qed.

Lemma dreg_not_CC: forall (r: dreg),
  4 <> (#r).
Proof.
  intros; DIRN1 r; [ apply ireg_not_CC | discriminate | apply freg_not_CC].
Qed.

Lemma dreg_not_CV: forall (r: dreg),
  5 <> (#r).
Proof.
  intros; DIRN1 r; [ apply ireg_not_CV | discriminate | apply freg_not_CV].
Qed.

Lemma sr_update_both: forall sr rsr r1 rr v
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  (sr <[ (#r1) <- Val (v) ]>) (#rr) =
  Val (rsr # r1 <- v rr).
Proof.
  intros. unfold assign.
  destruct (R.eq_dec (#r1) (#rr)); subst.
  - apply ppos_equal in e; subst; rewrite Pregmap.gss; reflexivity.
  - rewrite Pregmap.gso; eapply ppos_discr in n; auto.
Qed.

Lemma sr_gss: forall sr pos v,
  (sr <[ pos <- v ]>) pos = v.
Proof.
  intros. unfold assign.
  destruct (R.eq_dec pos pos) eqn:REQ; try reflexivity; try congruence.
Qed.

Lemma sr_update_overwrite: forall sr pos v1 v2,
  (sr <[ pos <- v1 ]>) <[ pos <- v2 ]> = (sr <[ pos <- v2 ]>).
Proof.
  intros.
  unfold assign. apply functional_extensionality; intros x.
  destruct (R.eq_dec pos x); reflexivity.
Qed.

Ltac sr_val_rwrt :=
  repeat match goal with
  | [H: forall r: preg, ?sr (# r) = Val (?rsr r) |- _ ]
      => rewrite H
  end.

Ltac sr_memstate_rwrt :=
  repeat match goal with
  | [H: ?sr pmem = Memstate ?mr |- _ ]
      => rewrite <- H
  end.

Ltac replace_ppos :=
  try erewrite !ireg_pos_ppos;
  try erewrite !freg_pos_ppos;
  try replace (7) with (#XSP) by eauto;
  try replace (24) with (#X16) by auto.

Ltac DDRM dr :=
  destruct dr as [irsDDRF|frDDRF]; 
      [destruct irsDDRF
      | idtac ].

(* Ltac DDRF dr :=
  destruct dr as [irsDDRF|frDDRF]; 
      [destruct irsDDRF as [irsDDRF|]; [destruct irsDDRF|]
      | destruct frDDRF]. *)

(* Ltac DPRI pr :=
  destruct pr as [drDPRI|crDPRI|]; 
      [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|]
      | idtac
      | idtac ]. *)

Ltac discriminate_ppos :=
  try apply ireg_not_pmem;
  try apply ireg_not_pc;
  try apply freg_not_pmem;
  try apply dreg_not_pmem;
  try apply ireg_not_CN;
  try apply ireg_not_CZ;
  try apply ireg_not_CC;
  try apply ireg_not_CV;
  try apply freg_not_CN;
  try apply freg_not_CZ;
  try apply freg_not_CC;
  try apply freg_not_CV;
  try apply dreg_not_CN;
  try apply dreg_not_CZ;
  try apply dreg_not_CC;
  try apply dreg_not_CV;
  try(simpl; discriminate).

Ltac replace_pc := try replace (6) with (#PC) by eauto.

Ltac replace_regs_pos sr :=
  try replace (sr 7) with (sr (ppos XSP)) by eauto;
  try replace (sr 6) with (sr (ppos PC)) by eauto;
  try replace (sr 2) with (sr (ppos CN)) by eauto;
  try replace (sr 3) with (sr (ppos CZ)) by eauto;
  try replace (sr 4) with (sr (ppos CC)) by eauto;
  try replace (sr 5) with (sr (ppos CV)) by eauto.

Ltac Simpl_exists sr :=
  replace_ppos;
  replace_regs_pos sr;
  try sr_val_rwrt;
  try (eexists; split; [| split]); eauto;
  try (sr_memstate_rwrt; rewrite assign_diff;
      try reflexivity;
      discriminate_ppos
  ).

Ltac Simpl_rep sr :=
  replace_ppos;
  replace_regs_pos sr;
  try sr_val_rwrt;
  try (sr_memstate_rwrt; rewrite assign_diff;
      try reflexivity;
      discriminate_ppos
  ).

Ltac Simpl_update :=
  try eapply sr_update_both; eauto.

Ltac Simpl sr := Simpl_exists sr; try (intros rr(* ; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr *)); Simpl_update.

Ltac destruct_res_flag rsr := try (rewrite Pregmap.gso; discriminate_ppos); destruct (rsr _); simpl; try reflexivity.

(* Ltac discriminate_preg_flags := rewrite !assign_diff; try rewrite !Pregmap.gso; discriminate_ppos; sr_val_rwrt; reflexivity. *)

(* Ltac destruct_reg_neq r1 r2 :=
  destruct (PregEq.eq r1 r2); subst;
   [ rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
     rewrite assign_diff; try rewrite Pregmap.gso; fold (ppos r1); try apply ppos_discr; auto]. *)

Lemma reg_update_overwrite: forall rsr sr r rd v1 v2
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((sr <[ # rd <- Val (v1) ]>) <[ # rd <- Val (v2) ]>) (# r) =
  Val ((rsr # rd <- v1) # rd <- v2 r).
Proof.
  intros.
  unfold Pregmap.set; destruct (PregEq.eq r rd).
  - rewrite e; apply sr_gss; reflexivity.
  - rewrite sr_update_overwrite. rewrite assign_diff; eauto.
    unfold not; intros. apply ppos_equal in H. congruence.
Qed.

Ltac replace_regs_cond_force :=
  try replace (5) with (#CV) in * by auto;
  try replace (4) with (#CC) in * by auto;
  try replace (3) with (#CZ) in * by auto;
  try replace (2) with (#CN) in * by auto.
  
Ltac validate_crbit_flags rr v1 v2 :=
  destruct (R.eq_dec 5 (#rr)) as [e0|n0];
  destruct (R.eq_dec 4 (#rr)) as [e1|n1];
  destruct (R.eq_dec 3 (#rr)) as [e2|n2];
  destruct (R.eq_dec 2 (#rr)) as [e3|n3];
  replace_regs_cond_force;
  try apply ppos_equal in e0;
  try apply ppos_equal in e1;
  try apply ppos_equal in e2;
  try apply ppos_equal in e3;
  try apply ppos_discr in n0;
  try apply ppos_discr in n1;
  try apply ppos_discr in n2;
  try apply ppos_discr in n3;
  subst.

Ltac Simpl_flags :=
  try (rewrite Pregmap.gss; reflexivity);
  try (rewrite Pregmap.gso, Pregmap.gss; [reflexivity|]; try auto);
  try (rewrite Pregmap.gso; try auto); 
  try (rewrite !Pregmap.gso; try auto).

Lemma compare_single_res: forall sr mr rsr rr v1 v2
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((((sr <[ 2 <- Val (_CN (v_compare_single v1 v2)) ]>) <[ 3 <-
   Val (_CZ (v_compare_single v1 v2)) ]>) <[ 4 <-
  Val (_CC (v_compare_single v1 v2)) ]>) <[ 5 <-
 Val (_CV (v_compare_single v1 v2)) ]>) (# rr) =
Val
  ((compare_single rsr v1 v2) rr).
Proof.
  intros. unfold v_compare_single, compare_single, assign.
  validate_crbit_flags rr v1 v2.
  all: destruct v1; destruct v2; Simpl_flags.
Qed.

Lemma compare_float_res: forall sr mr rsr rr v1 v2
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((((sr <[ 2 <- Val (_CN (v_compare_float v1 v2)) ]>) <[ 3 <-
   Val (_CZ (v_compare_float v1 v2)) ]>) <[ 4 <-
  Val (_CC (v_compare_float v1 v2)) ]>) <[ 5 <-
 Val (_CV (v_compare_float v1 v2)) ]>) (# rr) =
Val
  ((compare_float rsr v1 v2) rr).
Proof.
  intros. unfold v_compare_float, compare_float, assign.
  validate_crbit_flags rr v1 v2.
  all: destruct v1; destruct v2; Simpl_flags.
Qed.

Lemma compare_long_res: forall sr mr rsr rr v1 v2
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((((sr <[ 2 <- Val (_CN (v_compare_long v1 v2)) ]>) <[ 3 <-
   Val (_CZ (v_compare_long v1 v2)) ]>) <[ 4 <-
  Val (_CC (v_compare_long v1 v2)) ]>) <[ 5 <-
 Val (_CV (v_compare_long v1 v2)) ]>) (# rr) =
Val
  ((compare_long rsr v1 v2) rr).
Proof.
  intros. unfold v_compare_long, compare_long, assign.
  validate_crbit_flags rr v1 v2.
  all: Simpl_flags.
Qed.

Lemma compare_int_res: forall sr mr rsr rr v1 v2
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((((sr <[ 2 <- Val (_CN (v_compare_int v1 v2)) ]>) <[ 3 <-
   Val (_CZ (v_compare_int v1 v2)) ]>) <[ 4 <-
  Val (_CC (v_compare_int v1 v2)) ]>) <[ 5 <-
 Val (_CV (v_compare_int v1 v2)) ]>) (# rr) =
Val
  ((compare_int rsr v1 v2) rr).
Proof.
  intros. unfold v_compare_int, compare_int, assign.
  validate_crbit_flags rr v1 v2.
  all: Simpl_flags.
Qed.

Section SECT_SEQ.

Variable Ge: genv.

Lemma trans_arith_correct rsr mr sr rsw' old i:
  match_states (State rsr mr) sr ->
  exec_arith_instr Ge.(_lk) i rsr = rsw' ->
  exists sw,
     inst_run Ge (trans_arith i) sr old = Some sw
  /\ match_states (State rsw' mr) sw.
Proof.
  induction i.
  all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr.
  - (* PArithP *)
    destruct i.
    1,2,3: DIRN1 rd; Simpl sr.
    (* Special case for Pmovimms/Pmovimmd *)
    all: simpl;
      try(destruct (negb (is_immediate_float32 _)));
      try(destruct (negb (is_immediate_float64 _)));
      DIRN1 rd; Simpl sr;
      try (rewrite assign_diff; discriminate_ppos; reflexivity);
      try (intros rr'; Simpl_update).
  - (* PArithPP *)
    DIRN1 rs; DIRN1 rd; Simpl sr.
  - (* PArithPPP *)
    DIRN1 r1; DIRN1 r2; DIRN1 rd; Simpl sr.
  - (* PArithRR0R *) 
    simpl. destruct r1.
    + (* OArithRR0R *) simpl; Simpl sr.
    + (* OArithRR0R_XZR *) simpl; destruct (arith_rr0r_isize _); Simpl sr.
  - (* PArithRR0 *)
    simpl. destruct r1.
    + (* OArithRR0 *) simpl; Simpl sr.
    + (* OArithRR0_XZR *) simpl; destruct (arith_rr0_isize _); Simpl sr.
  - (* PArithARRRR0 *)
    simpl. destruct r3.
    + (* OArithARRRR0 *) simpl; Simpl sr.
    + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); Simpl sr.
  - (* PArithComparisonPP *)
    simpl; destruct i;
    unfold arith_eval_comparison_pp, arith_prepare_comparison_pp; simpl;
    fold (ppos r2); fold(ppos r1); try rewrite !H0; repeat Simpl_rep sr;
    Simpl sr;
    try destruct sz;
    try (eapply compare_single_res; eauto);
    try (eapply compare_long_res; eauto);
    try (eapply compare_float_res; eauto).
  - (* PArithComparisonR0R *)
    simpl; destruct r1; simpl; destruct i;
    repeat (replace_regs_cond_force; try fold (ppos r); try fold(ppos r2);
    try rewrite !assign_diff; discriminate_ppos; try rewrite !H0);
    Simpl sr; unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize;
    destruct arith_prepare_comparison_r0r; destruct is;
    try (eapply compare_long_res; eauto);
    try (eapply compare_int_res; eauto).
  - (* PArithComparisonP *)
    simpl; destruct i;
    unfold arith_eval_comparison_p, arith_prepare_comparison_p; simpl;
    fold(ppos r1); try rewrite !H0; repeat Simpl_rep sr;
    Simpl sr;
    try destruct sz;
    try (eapply compare_int_res; eauto);
    try (eapply compare_single_res; eauto);
    try (eapply compare_long_res; eauto);
    try (eapply compare_float_res; eauto).
  - (* Pcset *)
    simpl; unfold eval_testcond, get_testcond_rlocs, cflags_eval;
    unfold cond_eval_is; unfold flags_testcond_value, list_exp_eval; destruct c; simpl;
    repeat Simpl_rep sr; Simpl_exists sr;
    destruct_res_flag rsr;
    Simpl sr.
  - (* Pfmovi *)
    simpl; destruct r1; simpl; destruct fsz; Simpl sr.
  - (* Pcsel *)
    destruct c; simpl; DIRN1 rd; fold (ppos r2); fold (ppos r1); Simpl sr.
  - (* Pfnmul *)
    simpl; destruct fsz; Simpl sr.
Qed.

Lemma sp_xsp:
  SP = XSP.
Proof.
  econstructor.
Qed.

Lemma load_chunk_neutral: forall chk v r,
  interp_load (trans_ldp_chunk chk r) v = v.
Proof.
  intros; destruct chk; destruct r; simpl; reflexivity.
Qed.

Theorem bisimu_basic rsr mr sr bi:
  match_states (State rsr mr) sr ->
  match_outcome (exec_basic Ge.(_lk) Ge.(_genv) bi rsr mr) (inst_run Ge (trans_basic bi) sr sr).
Proof.
(* a little tactic to automate reasoning on preg_eq *)
Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core.
Local Ltac preg_eq_discr r rd :=
  destruct (preg_eq r rd); try (subst r; rewrite assign_eq, Pregmap.gss; auto);
  rewrite (assign_diff _ (#rd) (#r) _); auto;
  rewrite Pregmap.gso; auto.

  intros MS; inversion MS as (H & H0).
  destruct bi; simpl.
  (* Loadsymbol / Cvtsw2x / Cvtuw2x / Cvtx2w *) 
  6,7,8,9: Simpl sr.
  - (* Arith *)
    exploit trans_arith_correct; eauto.
  - (* Load *)
    destruct ld.
    + unfold exec_load, exec_load_rd_a, eval_addressing_rlocs_ld, exp_eval;
      destruct ld; destruct a; simpl;
      try fold (ppos base); try fold (ppos r);
      erewrite !H0, H; simpl;
      unfold exec_load1, exec_load2, chunk_load; unfold call_ll_loadv;
      try destruct (Mem.loadv _ _ _); simpl; auto.
      all: try (fold (ppos rd); Simpl_exists sr; auto; intros rr; Simpl_update).
    + 
      unfold exec_load, exec_load_double, eval_addressing_rlocs_ld, exp_eval;
      destruct ld; destruct a; simpl; unfold control_eval; destruct Ge; auto;
      try fold (ppos base);
      try erewrite !H0, H; simpl;
      unfold exec_load1, exec_load2; unfold call_ll_loadv;
      destruct (Mem.loadv _ _ _); simpl; auto;
      fold (ppos rd1); rewrite assign_diff; discriminate_ppos; rewrite H;
      try destruct (Mem.loadv _ _ _); simpl; auto; Simpl_exists sr;
      rewrite !load_chunk_neutral;
      try (rewrite !assign_diff; discriminate_ppos; reflexivity);
      try (destruct rd1 as [ir1|fr1]; try destruct ir1; destruct rd2 as [ir2|fr2]; try destruct ir2;
      destruct base; discriminate_ppos);
      repeat (try fold (ppos r); try fold (ppos r0);
      try fold (ppos fr1); try fold (ppos fr2); intros; Simpl_update).
  - (* Store *)
    destruct st.
    + unfold exec_store, exec_store_rs_a, eval_addressing_rlocs_st, exp_eval;
      destruct st; destruct a; simpl;
      try fold (ppos base); try fold (ppos rs); try fold (ppos r);
      erewrite !H0, H; simpl;
      unfold exec_store1, exec_store2, chunk_store; unfold call_ll_storev;
      try destruct (Mem.storev _ _ _ _); simpl; auto.
      all: eexists; split; [| split]; eauto;
      intros rr; rewrite assign_diff; try rewrite H0; auto; discriminate_ppos.
    + unfold exec_store, exec_store_double, eval_addressing_rlocs_st, exp_eval;
      destruct st; destruct a; simpl; unfold control_eval; destruct Ge; auto;
      try fold (ppos base); try fold (ppos rs1);
      erewrite !H0, H; simpl;
      unfold exec_store1, exec_store2; unfold call_ll_storev;
      try destruct (Mem.storev _ _ _ _); simpl; auto;
      fold (ppos rs2); rewrite assign_diff; try congruence; try rewrite H0; simpl;
      try destruct (Mem.storev _ _ _ _); simpl; auto.
      all: eexists; split; [| split]; eauto;
      repeat (try intros rr; rewrite assign_diff; try rewrite H0; auto; discriminate_ppos).
  - (* Alloc *)
    destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS.
    + eexists; repeat split. 
      * rewrite !assign_diff; try discriminate_ppos; Simpl_exists sr;
        rewrite H; destruct (Mem.alloc _ _ _) eqn:MEMAL2;
        injection MEMAL; intros Hm Hb; try rewrite Hm, Hb;
        rewrite sp_xsp in MEMS; rewrite MEMS.
        rewrite !assign_diff; try discriminate_ppos; Simpl_exists sr; rewrite H;
        destruct (Mem.alloc _ _ _) eqn:MEMAL3;
        injection MEMAL2; intros Hm2 Hb2; try rewrite Hm2, Hb2;
        rewrite Hm, Hb; rewrite MEMS; reflexivity.
      * eauto.
      * intros rr. rewrite assign_diff; try apply preg_not_pmem; try rewrite sp_xsp.
        replace 37 with (#X29) by auto; repeat (Simpl_update; intros).
    + simpl; repeat Simpl_exists sr. erewrite H. destruct (Mem.alloc _ _ _) eqn:HMEMAL2.
        injection MEMAL; intros Hm Hb. 
        try rewrite Hm, Hb; clear Hm Hb.
        try rewrite sp_xsp in MEMS; rewrite MEMS. reflexivity.
  - (* Free *)
    destruct (Mem.loadv _ _ _) eqn:MLOAD; simpl; auto;
    repeat Simpl_exists sr; rewrite H; simpl.
    + destruct (rsr SP) eqn:EQSP; simpl; rewrite <- sp_xsp; rewrite EQSP; rewrite MLOAD; try reflexivity.
      destruct (Mem.free _ _ _) eqn:EQFREE; try reflexivity. rewrite assign_diff; discriminate_ppos.
      replace_regs_pos sr; sr_val_rwrt. rewrite <- sp_xsp; rewrite EQSP; rewrite MLOAD. rewrite EQFREE.
      replace 24 with (#X16) by auto; rewrite sp_xsp; Simpl sr.
      intros rr'; destruct (PregEq.eq XSP rr').
      * rewrite e; rewrite Pregmap.gss, sr_gss; auto.
      * rewrite Pregmap.gso, !assign_diff; auto; apply ppos_discr in n; auto.
    + rewrite <- sp_xsp; rewrite MLOAD; reflexivity.
  - (* Nop *)
    Simpl sr.
Qed.

Theorem bisimu_body:
  forall bdy rsr mr sr,
  match_states (State rsr mr) sr ->
  match_outcome (exec_body Ge.(_lk) Ge.(_genv) bdy rsr mr) (exec Ge (trans_body bdy) sr).
Proof.
  induction bdy as [|i bdy]; simpl; eauto. 
  intros.
  exploit (bisimu_basic rsr mr sr i); eauto.
  destruct (exec_basic _ _ _ _ _); simpl.
  - intros (s' & X1 & X2).
    rewrite X1; simpl; eauto. eapply IHbdy; eauto; simpl.
    unfold match_states in *. destruct s. unfold Asm._m. eauto.
  - intros X; rewrite X; simpl; auto.
Qed.

Theorem bisimu_control ex sz rsr mr sr:
  match_states (State rsr mr) sr ->
  match_outcome (exec_cfi Ge.(_genv) Ge.(_fn) ex (incrPC (Ptrofs.repr sz) rsr) mr) (inst_run Ge (trans_pcincr sz (trans_exit (Some (PCtlFlow ex)))) sr sr).
Proof.
  intros MS.
  simpl in *. inv MS.
  destruct ex.
  (* Obr / Oret *)
  6,7: unfold control_eval, incrPC; simpl; destruct Ge;
       replace_pc; rewrite (H0 PC);
       repeat Simpl_rep sr; Simpl_exists sr;
       intros rr; destruct (preg_eq rr PC); [
       rewrite e; rewrite sr_gss; rewrite Pregmap.gss;
       try rewrite Pregmap.gso; discriminate_ppos; fold (ppos r); auto |
       repeat Simpl_rep sr; try rewrite !Pregmap.gso; auto; apply ppos_discr in n; auto ].
  (* Ocbnz / Ocbz *)
  6,7,8,9: unfold control_eval; destruct Ge; simpl;
           replace_pc; rewrite (H0 PC);
           unfold eval_branch, eval_neg_branch, eval_testzero, eval_testbit,
                  incrPC, goto_label_deps, goto_label;
           destruct (PregEq.eq r PC);
           [ rewrite e; destruct sz0; simpl; Simpl sr |
             destruct sz0; simpl; replace_pc; rewrite Pregmap.gso; auto; repeat Simpl_rep sr; try rewrite H0;
             try (destruct (Val.mxcmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
             try (destruct (Val.mxcmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
             try (destruct (Val.cmp_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
             try (destruct (Val.cmpl_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
             try (simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr);
             destruct (label_pos _ _ _); try reflexivity; rewrite Pregmap.gss;
             destruct Val.offset_ptr; try reflexivity; rewrite sr_update_overwrite; 
             simpl; Simpl sr; (destruct (PregEq.eq rr PC); subst;
                  [ rewrite sr_gss, Pregmap.gss; reflexivity |
                  rewrite !assign_diff, !Pregmap.gso; replace_pc; auto; apply ppos_discr; auto]) ].
  - (* Ob *)
    replace_pc. rewrite (H0 PC). simpl.
    unfold goto_label, control_eval. destruct Ge.
    unfold goto_label_deps. destruct (label_pos _ _ _); auto.
    + unfold incrPC. rewrite Pregmap.gss; eauto. destruct (Val.offset_ptr _ _); auto;
      try (rewrite sr_gss; unfold Stuck; reflexivity).
      simpl. eexists; split; split.
      * rewrite sr_update_overwrite. unfold pmem, assign in *. simpl. rewrite H; reflexivity.
      * intros. rewrite sr_update_overwrite. unfold Pregmap.set, assign.
        destruct r as [dr|cr|]; try destruct dr as [ir|fr]; try destruct ir as [irr|];
        try destruct irr; try destruct fr; try destruct cr; simpl; try rewrite <- H0; eauto.
    + rewrite sr_gss; reflexivity.
  - (* Obc *)
    replace_pc. rewrite (H0 PC). simpl.
    unfold eval_branch, goto_label, control_eval. destruct Ge.
    unfold goto_label_deps, cflags_eval, eval_testcond, list_exp_eval.
    destruct c; simpl; unfold incrPC;
    repeat (replace_ppos; replace_pc; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos).
    1,2,3,4,5,6: destruct_res_flag rsr.
    7,8,9,10: do 2 (destruct_res_flag rsr).
    11,12 : do 3 (destruct_res_flag rsr).
    1,2,3,4,5,6,9,10: destruct (Int.eq _ _); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ];
                      destruct (label_pos _ _ _); [| reflexivity]; replace_pc; 
                      rewrite !Pregmap.gss; destruct Val.offset_ptr;
                      try (unfold Stuck; reflexivity); Simpl_exists sr; intros rr;
                      apply reg_update_overwrite; eauto.
    1,3: destruct (andb); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ];
         destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss;
         destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr;
         intros rr; apply reg_update_overwrite; eauto.
    1,2: destruct (orb); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ];
         destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss;
         destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr;
         intros rr; apply reg_update_overwrite; eauto.
  - (* Obl *)
    replace_pc. rewrite (H0 PC). simpl.
    unfold control_eval. destruct Ge.
    rewrite sr_gss. Simpl sr.
    replace_pc; try replace (38) with (#X30) by eauto; unfold incrPC. Simpl_update.
    repeat (intros; Simpl_update).
  - (* Obs *)
    unfold control_eval. destruct Ge. replace_pc. rewrite (H0 PC). simpl; unfold incrPC.
    replace_pc; Simpl_exists sr; intros rr; apply reg_update_overwrite; eauto.
  - (* Oblr *)
    replace_pc. rewrite (H0 PC).
    unfold control_eval. destruct Ge. simpl. unfold incrPC.
    try (eexists; split; [  | split ]); eauto.
    intros rr; destruct (PregEq.eq PC rr).
    + replace_pc; rewrite e; rewrite !Pregmap.gss, !sr_gss;
      rewrite Pregmap.gso; fold (ppos r); try rewrite H0; auto.
      rewrite <- e; destruct r; discriminate.
    + replace_pc; rewrite Pregmap.gso, assign_diff; auto; apply ppos_discr in n; auto;
      rewrite Pregmap.gss, sr_gss. destruct (PregEq.eq X30 rr); replace 38 with (#X30) by auto.
      * rewrite e; rewrite Pregmap.gss, sr_gss; auto.
      * replace_pc; rewrite !Pregmap.gso, !assign_diff; auto; apply ppos_discr in n0; auto;
        apply ppos_discr; eauto.
  - (* Obtbl *)
    replace_pc; rewrite (H0 PC);
    unfold control_eval; destruct Ge; simpl; unfold incrPC.
    destruct (PregEq.eq X16 r1).
    + fold (ppos r1); rewrite <- e; rewrite Pregmap.gss, sr_gss; reflexivity.
    + rewrite !Pregmap.gso; auto; rewrite ppos_discr in n;
      fold (ppos r1); replace 24 with (#X16) by auto; try rewrite !assign_diff; auto;
      discriminate_ppos; rewrite H0; destruct (rsr r1) eqn:EQR;
      try (try rewrite EQR; reflexivity).
      try destruct (list_nth_z _ _); try reflexivity;
      unfold goto_label, goto_label_deps; destruct (label_pos _ _ _);
      try rewrite 2Pregmap.gso, Pregmap.gss; destruct (Val.offset_ptr (rsr PC) (Ptrofs.repr sz));
      try reflexivity; discriminate_ppos. Simpl sr.
      destruct (PregEq.eq X16 rr); [ subst; Simpl_update |];
      destruct (PregEq.eq PC rr); [ subst; Simpl_update |].
      rewrite !Pregmap.gso; auto;
      apply ppos_discr in n0; apply ppos_discr in n1;
      rewrite !assign_diff; auto.
Qed.

Theorem bisimu_exit ex sz rsr mr sr:
  match_states (State rsr mr) sr ->
  (*is_builtin ex = false ->*)
  match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit ex)) sr sr).
Proof.
  intros MS; unfold estep.
  destruct ex.
  - destruct c.
    + exploit (bisimu_control i sz rsr mr sr); eauto.
    + simpl. inv MS. eexists; split; [| split].
      unfold control_eval; destruct Ge.
      replace_pc; rewrite (H0 PC); eauto.
      rewrite assign_diff; auto.
      intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst.
      * rewrite sr_gss, Pregmap.gss. reflexivity.
      * rewrite assign_diff, Pregmap.gso; try rewrite H0;
        auto; try rewrite ppos_discr in n; auto.
  - simpl. inv MS. eexists; split; [| split].
    + unfold control_eval; destruct Ge.
      replace_pc; rewrite (H0 PC); eauto.
    + rewrite assign_diff; auto.
    + intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst.
      * rewrite sr_gss, Pregmap.gss. reflexivity.
      * rewrite assign_diff, Pregmap.gso; try rewrite H0; auto; try rewrite ppos_discr in n; auto.
Qed.

(* Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). *)

Theorem bisimu rsr mr sr bb:
  match_states (State rsr mr) sr ->
  match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rsr mr) (exec Ge (trans_block bb) sr).
Proof.
  intros MS. unfold bbstep, trans_block.
  exploit (bisimu_body (body bb) rsr mr sr); eauto.
  destruct (exec_body _ _ _ _ _); simpl.
  - unfold match_states in *. intros (s' & X1 & X2). destruct s.
    erewrite run_app_Some; eauto.
    exploit (bisimu_exit (exit bb) (size bb) _rs _m s'); eauto.
    destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).
    replace_pc. erewrite !X3; simpl.
    destruct (inst_run _ _ _ _); simpl; auto.
  - intros X; erewrite run_app_None; eauto.
Qed.

Theorem trans_state_match: forall S, match_states S (trans_state S).
Proof.
  intros. destruct S as (rs & m). simpl.
  split. reflexivity.
  intro. destruct r as [dr|cr|]; try destruct dr as [ir|fr]; try destruct cr;
  try destruct ir as [irr|]; try destruct irr; try destruct fr; try reflexivity.
Qed.

Lemma state_eq_decomp:
  forall rs1 m1 rs2 m2, rs1 = rs2 -> m1 = m2 -> State rs1 m1 = State rs2 m2.
Proof.
  intros. congruence.
Qed.

Theorem state_equiv S1 S2 S': match_states S1 S' -> match_states S2 S' -> S1 = S2.
Proof.
  unfold match_states; intros H0 H1. destruct S1 as (rs1 & m1). destruct S2 as (rs2 & m2). inv H0. inv H1.
  apply state_eq_decomp.
  - apply functional_extensionality. intros. assert (Val (rs1 x) = Val (rs2 x)) by congruence. congruence.
  - congruence.
Qed.

End SECT_SEQ.

Section SECT_BBLOCK_EQUIV.

Variable Ge: genv.

Local Hint Resolve trans_state_match: core.

Lemma bblock_simu_reduce_aux:
  forall p1 p2,
  L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
  Asmblockprops.bblock_simu_aux Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2.
Proof.
  intros p1 p2 H0 rs m EBB.
  generalize (H0 (trans_state (State rs m))); clear H0.
  intro H0.
  exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto.
  exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto.
  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 rs m); try (unfold Stuck in EBB; congruence).
  intros H1 (s2' & exp2 & MS'). unfold exec in exp2, H1. rewrite exp2 in H0.
  destruct H0 as (m2' & H0 & H2). discriminate. rewrite H0 in H1.
  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p2 rs m); simpl in H1.
  * unfold match_states in H1, MS'. destruct s, s0.
    destruct H1 as (s' & H1 & H3 & H4). inv H1. inv MS'.
    replace (_rs0) with (_rs).
    - replace (_m0) with (_m); auto. congruence.
    - apply functional_extensionality. intros r.
      generalize (H1 r). intros Hr. congruence.
  * discriminate.
Qed.

Lemma incrPC_set_res_commut res: forall d vres rs,  
  incrPC d (set_res (map_builtin_res DR res) vres rs) =
  set_res (map_builtin_res DR res) vres (incrPC d rs).
Proof.
  induction res; simpl; auto.
  - intros; apply functional_extensionality.
    unfold incrPC; intros x0.
    destruct (PregEq.eq x0 PC).
    + subst; rewrite! Pregmap.gss; auto.
    + rewrite Pregmap.gso; auto.
      destruct (PregEq.eq x x0).
      * subst; rewrite! Pregmap.gss; auto.
      * rewrite !Pregmap.gso; auto.
  - intros; rewrite IHres2. f_equal. auto.
Qed.

Lemma incrPC_undef_regs_commut l : forall d rs,
  incrPC d (undef_regs l rs) = undef_regs l (incrPC d rs).
Proof.
  induction l; simpl; auto.
  intros. rewrite IHl. unfold incrPC.
  destruct (PregEq.eq a PC).
  - rewrite e. rewrite Pregmap.gss.
    simpl. apply f_equal. unfold Pregmap.set.
    apply functional_extensionality. intros x.
    destruct (PregEq.eq x PC); auto.
  - rewrite Pregmap.gso; auto.
    apply f_equal. unfold Pregmap.set.
    apply functional_extensionality. intros x.
    destruct (PregEq.eq x PC).
    + subst. destruct a; simpl; auto. congruence.
    + auto.
Qed.

Lemma bblock_simu_reduce:
  forall p1 p2,
  L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
  (has_builtin p1 = true \/ has_builtin p2 = true -> exit p1 = exit p2) ->
  Asmblockprops.bblock_simu Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2.
Proof.
  unfold bblock_simu. intros p1 p2 H0 BLT rs m EBB.
  unfold exec_bblock.
  generalize (bblock_simu_reduce_aux p1 p2 H0).
  unfold bblock_simu_aux. clear H0.
  unfold exec_bblock, bbstep. intros H0 m' t0 (rs1 & m1 & H1 & H2).
  assert ((has_builtin p1 = false /\ has_builtin p2 = false) \/ (has_builtin p1 = true \/ has_builtin p2 = true)). { repeat destruct (has_builtin _); simpl; intuition. }
  destruct H as [[X1 X2]|H].
  - (* Not a builtin *)
    exploit (H0); eauto; erewrite H1; simpl; (*gen*)
    unfold estep; unfold has_builtin in *.
    { destruct (exit p1) as [[]|] eqn: EQEX1; try discriminate; simpl in *.
    inversion H2; subst. rewrite H3; discriminate. }
    destruct (exit p1) as [[]|] eqn: EQEX1; try discriminate; simpl in *.
    { inversion H2; subst. rewrite H3.
    destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
    intros H4. eexists; eexists; split; try reflexivity.
    destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto.
    inversion H4. econstructor. }
    { inversion H2; subst.
      destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
intros H4. eexists; eexists; split; try reflexivity.
    destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto.
    inversion H4. rewrite H3. econstructor. }
  - (* Builtin *)
    exploit (BLT); eauto.
    intros EXIT.
    unfold has_builtin in H.
    assert (is_builtin (exit p1) = true). { rewrite <- EXIT in H; intuition. }
    clear H.
    generalize (H0 rs m); eauto; erewrite H1; simpl;
    unfold estep. destruct (exit p1) as [[]|] eqn:EQEX1; try discriminate.
    rewrite <- EXIT.
    intros CONTRA.
    exploit (CONTRA); try discriminate.
    destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
    intros H4. eexists; eexists; split; try reflexivity.
    inversion H2; subst. inversion H4; subst.
    econstructor; eauto.
    + unfold incrPC in H5.
      replace (rs2 SP) with (rs1 SP).
      replace (fun r : dreg => rs2 r) with (fun r : dreg => rs1 r); auto.
      * apply functional_extensionality.
        intros r; destruct (PregEq.eq r PC); try discriminate.
        replace (rs1 r) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) r) by auto.
        rewrite H5; rewrite Pregmap.gso; auto.
      * replace (rs1 SP) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) SP) by auto.
        rewrite H5; rewrite Pregmap.gso; auto; try discriminate.
    + rewrite !incrPC_set_res_commut.
      rewrite !incrPC_undef_regs_commut.
      rewrite H5.
      reflexivity.
Qed.

(** Used for debug traces *)

Definition ireg_name (ir: ireg) : pstring :=
  match ir with
  | X0 => Str ("X0") | X1 => Str ("X1") | X2 => Str ("X2") | X3 => Str ("X3") | X4 => Str ("X4") | X5 => Str ("X5") | X6 => Str ("X6") | X7 => Str ("X7")
  | X8 => Str ("X8") | X9 => Str ("X9") | X10 => Str ("X10") | X11 => Str ("X11") | X12 => Str ("X12") | X13 => Str ("X13") | X14 => Str ("X14") | X15 => Str ("X15")
  | X16 => Str ("X16") | X17 => Str ("X17") | X18 => Str ("X18") | X19 => Str ("X19") | X20 => Str ("X20") | X21 => Str ("X21") | X22 => Str ("X22") | X23 => Str ("X23")
  | X24 => Str ("X24") | X25 => Str ("X25") | X26 => Str ("X26") | X27 => Str ("X27") | X28 => Str ("X28") | X29 => Str ("X29") | X30 => Str ("X30")
  end
.

Definition freg_name (fr: freg) : pstring :=
  match fr with
  | D0 => Str ("D0") | D1 => Str ("D1") | D2 => Str ("D2") | D3 => Str ("D3") | D4 => Str ("D4") | D5 => Str ("D5") | D6 => Str ("D6") | D7 => Str ("D7")
  | D8 => Str ("D8") | D9 => Str ("D9") | D10 => Str ("D10") | D11 => Str ("D11") | D12 => Str ("D12") | D13 => Str ("D13") | D14 => Str ("D14") | D15 => Str ("D15")
  | D16 => Str ("D16") | D17 => Str ("D17") | D18 => Str ("D18") | D19 => Str ("D19") | D20 => Str ("D20") | D21 => Str ("D21") | D22 => Str ("D22") | D23 => Str ("D23")
  | D24 => Str ("D24") | D25 => Str ("D25") | D26 => Str ("D26") | D27 => Str ("D27") | D28 => Str ("D28") | D29 => Str ("D29") | D30 => Str ("D30") | D31 => Str ("D31")
  end
.

Definition iregsp_name (irsp: iregsp) : pstring :=
  match irsp with
  | RR1 ir => ireg_name ir
  | XSP => Str ("XSP")
  end.

Definition dreg_name (dr: dreg) : ?? pstring :=
  match dr with
  | IR ir => match ir with
             | XSP => RET (Str ("XSP"))
             | RR1 irr => RET (ireg_name irr)
             end
  | FR fr => RET (freg_name fr)
  end.

Definition string_of_name (x: P.R.t): ?? pstring := 
  if (Pos.eqb x pmem) then 
    RET (Str "MEM")
  else
    match inv_ppos x with
    | Some (CR cr) => match cr with
                      | CN => RET (Str ("CN"))
                      | CZ => RET (Str ("CZ"))
                      | CC => RET (Str ("CC"))
                      | CV => RET (Str ("CV"))
                      end
    | Some (PC) => RET (Str ("PC"))
    | Some (DR dr) => dreg_name dr
    | _ => RET (Str ("UNDEFINED"))
    end.

Definition string_of_name_ArithP (n: arith_p) : pstring :=
  match n with
  | Padrp _ _ => "Padrp"
  | Pmovz _ _ _ => "Pmov"
  | Pmovn _ _ _ => "Pmov"
  | Pfmovimms _ => "Pfmovimm"
  | Pfmovimmd _ => "Pfmovimm"
  end.

Definition string_of_name_ArithPP (n: arith_pp) : pstring :=
  match n with
  | Pmov => "Pmov"
  | Pmovk _ _ _ => "Pmovk"
  | Paddadr _ _ => "Paddadr"
  | Psbfiz _ _ _ => "Psbfiz"
  | Psbfx _ _ _ => "Psbfx"
  | Pubfiz _ _ _ => "Pubfiz"
  | Pubfx _ _ _ => "Pubfx"
  | Pfmov => "Pfmov"
  | Pfcvtds => "Pfcvtds"
  | Pfcvtsd => "Pfcvtsd"
  | Pfabs _ => "Pfabs"
  | Pfneg _ => "Pfneg"
  | Pscvtf _ _ => "Pscvtf"
  | Pucvtf _ _ => "Pucvtf"
  | Pfcvtzs _ _ => "Pfcvtzs"
  | Pfcvtzu _ _ => "Pfcvtzu"
  | Paddimm _ _ => "Paddimm"
  | Psubimm _ _ => "Psubimm"
  end.

Definition string_of_name_ArithPPP (n: arith_ppp) : pstring :=
  match n with
  | Pasrv _ => "Pasrv"
  | Plslv _ => "Plslv"
  | Plsrv _ => "Plsrv"
  | Prorv _ => "Prorv"
  | Psmulh => "Psmulh"
  | Pumulh => "Pumulh"
  | Psdiv _ => "Psdiv"
  | Pudiv _ => "Pudiv"
  | Paddext _ => "Paddext"
  | Psubext _ => "Psubext"
  | Pfadd _ => "Pfadd"
  | Pfdiv _ => "Pfdiv"
  | Pfmul _ => "Pfmul"
  | Pfsub _ => "Pfsub"
  end.

Definition string_of_name_ArithRR0R (n: arith_rr0r) : pstring :=
  match n with
  | Padd _ _ => "ArithRR0R=>Padd"
  | Psub _ _ => "ArithRR0R=>Psub"
  | Pand _ _ => "ArithRR0R=>Pand"
  | Pbic _ _ => "ArithRR0R=>Pbic"
  | Peon _ _ => "ArithRR0R=>Peon"
  | Peor _ _ => "ArithRR0R=>Peor"
  | Porr _ _ => "ArithRR0R=>Porr"
  | Porn _ _ => "ArithRR0R=>Porn"
  end.

Definition string_of_name_ArithRR0R_XZR (n: arith_rr0r) : pstring :=
  match n with
  | Padd _ _ => "ArithRR0R_XZR=>Padd"
  | Psub _ _ => "ArithRR0R_XZR=>Psub"
  | Pand _ _ => "ArithRR0R_XZR=>Pand"
  | Pbic _ _ => "ArithRR0R_XZR=>Pbic"
  | Peon _ _ => "ArithRR0R_XZR=>Peon"
  | Peor _ _ => "ArithRR0R_XZR=>Peor"
  | Porr _ _ => "ArithRR0R_XZR=>Porr"
  | Porn _ _ => "ArithRR0R_XZR=>Porn"
  end.

Definition string_of_name_ArithRR0 (n: arith_rr0) : pstring :=
  match n with
  | Pandimm _ _ => "ArithRR0=>Pandimm"
  | Peorimm _ _ => "ArithRR0=>Peorimm"
  | Porrimm _ _ => "ArithRR0=>Porrimm"
  end.

Definition string_of_name_ArithRR0_XZR (n: arith_rr0) : pstring :=
match n with
  | Pandimm _ _ => "ArithRR0_XZR=>Pandimm"
  | Peorimm _ _ => "ArithRR0_XZR=>Peorimm"
  | Porrimm _ _ => "ArithRR0_XZR=>Porrimm"
  end.

Definition string_of_name_ArithARRRR0 (n: arith_arrrr0) : pstring :=
  match n with
  | Pmadd _ => "ArithARRRR0=>Pmadd"
  | Pmsub _ => "ArithARRRR0=>Pmsub"
  end.

Definition string_of_name_ArithARRRR0_XZR (n: arith_arrrr0) : pstring :=
  match n with
  | Pmadd _ => "ArithARRRR0_XZR=>Pmadd"
  | Pmsub _ => "ArithARRRR0_XZR=>Pmsub"
  end.

Definition string_of_name_ArithComparisonPP_CN (n: arith_comparison_pp) : pstring :=
  match n with
  | Pcmpext _ => "ArithComparisonPP_CN=>Pcmpext"
  | Pcmnext _ => "ArithComparisonPP_CN=>Pcmnext"
  | Pfcmp _ => "ArithComparisonPP_CN=>Pfcmp"
  end.

Definition string_of_name_ArithComparisonPP_CZ (n: arith_comparison_pp) : pstring :=
  match n with
  | Pcmpext _ => "ArithComparisonPP_CZ=>Pcmpext"
  | Pcmnext _ => "ArithComparisonPP_CZ=>Pcmnext"
  | Pfcmp _ => "ArithComparisonPP_CZ=>Pfcmp"
  end.

Definition string_of_name_ArithComparisonPP_CC (n: arith_comparison_pp) : pstring :=
match n with
  | Pcmpext _ => "ArithComparisonPP_CC=>Pcmpext"
  | Pcmnext _ => "ArithComparisonPP_CC=>Pcmnext"
  | Pfcmp _ => "ArithComparisonPP_CC=>Pfcmp"
  end.

Definition string_of_name_ArithComparisonPP_CV (n: arith_comparison_pp) : pstring :=
match n with
  | Pcmpext _ => "ArithComparisonPP_CV=>Pcmpext"
  | Pcmnext _ => "ArithComparisonPP_CV=>Pcmnext"
  | Pfcmp _ => "ArithComparisonPP_CV=>Pfcmp"
  end.

Definition string_of_name_ArithComparisonR0R_CN (n: arith_comparison_r0r) : pstring :=
  match n with
  | Pcmp _ _ => "ArithComparisonR0R_CN=>Pcmp"
  | Pcmn _ _ => "ArithComparisonR0R_CN=>Pcmn"
  | Ptst _ _ => "ArithComparisonR0R_CN=>Ptst"
  end.

Definition string_of_name_ArithComparisonR0R_CZ (n: arith_comparison_r0r) : pstring :=
  match n with
  | Pcmp _ _ => "ArithComparisonR0R_CZ=>Pcmp"
  | Pcmn _ _ => "ArithComparisonR0R_CZ=>Pcmn"
  | Ptst _ _ => "ArithComparisonR0R_CZ=>Ptst"
  end.

Definition string_of_name_ArithComparisonR0R_CC (n: arith_comparison_r0r) : pstring :=
  match n with
  | Pcmp _ _ => "ArithComparisonR0R_CC=>Pcmp"
  | Pcmn _ _ => "ArithComparisonR0R_CC=>Pcmn"
  | Ptst _ _ => "ArithComparisonR0R_CC=>Ptst"
  end.

Definition string_of_name_ArithComparisonR0R_CV (n: arith_comparison_r0r) : pstring :=
  match n with
  | Pcmp _ _ => "ArithComparisonR0R_CV=>Pcmp"
  | Pcmn _ _ => "ArithComparisonR0R_CV=>Pcmn"
  | Ptst _ _ => "ArithComparisonR0R_CV=>Ptst"
  end.

Definition string_of_name_ArithComparisonR0R_CN_XZR (n: arith_comparison_r0r) : pstring :=
  match n with
  | Pcmp _ _ => "ArithComparisonR0R_CN_XZR=>Pcmp"
  | Pcmn _ _ => "ArithComparisonR0R_CN_XZR=>Pcmn"
  | Ptst _ _ => "ArithComparisonR0R_CN_XZR=>Ptst"
  end.

Definition string_of_name_ArithComparisonR0R_CZ_XZR (n: arith_comparison_r0r) : pstring :=
  match n with
  | Pcmp _ _ => "ArithComparisonR0R_CZ_XZR=>Pcmp"
  | Pcmn _ _ => "ArithComparisonR0R_CZ_XZR=>Pcmn"
  | Ptst _ _ => "ArithComparisonR0R_CZ_XZR=>Ptst"
  end.

Definition string_of_name_ArithComparisonR0R_CC_XZR (n: arith_comparison_r0r) : pstring :=
match n with
  | Pcmp _ _ => "ArithComparisonR0R_CC_XZR=>Pcmp"
  | Pcmn _ _ => "ArithComparisonR0R_CC_XZR=>Pcmn"
  | Ptst _ _ => "ArithComparisonR0R_CC_XZR=>Ptst"
  end.

Definition string_of_name_ArithComparisonR0R_CV_XZR (n: arith_comparison_r0r) : pstring :=
match n with
  | Pcmp _ _ => "ArithComparisonR0R_CV_XZR=>Pcmp"
  | Pcmn _ _ => "ArithComparisonR0R_CV_XZR=>Pcmn"
  | Ptst _ _ => "ArithComparisonR0R_CV_XZR=>Ptst"
  end.

Definition string_of_name_ArithComparisonP_CN (n: arith_comparison_p) : pstring :=
  match n with
  | Pfcmp0 _ => "ArithComparisonP_CN=>Pfcmp0"
  | Pcmpimm _ _ => "ArithComparisonP_CN=>Pcmpimm"
  | Pcmnimm _ _ => "ArithComparisonP_CN=>Pcmnimm"
  | Ptstimm _ _ => "ArithComparisonP_CN=>Ptstimm"
  end.

Definition string_of_name_ArithComparisonP_CZ (n: arith_comparison_p) : pstring :=
  match n with
  | Pfcmp0 _ => "ArithComparisonP_CZ=>Pfcmp0"
  | Pcmpimm _ _ => "ArithComparisonP_CZ=>Pcmpimm"
  | Pcmnimm _ _ => "ArithComparisonP_CZ=>Pcmnimm"
  | Ptstimm _ _ => "ArithComparisonP_CZ=>Ptstimm"
  end.

Definition string_of_name_ArithComparisonP_CC (n: arith_comparison_p) : pstring :=
  match n with
  | Pfcmp0 _ => "ArithComparisonP_CC=>Pfcmp0"
  | Pcmpimm _ _ => "ArithComparisonP_CC=>Pcmpimm"
  | Pcmnimm _ _ => "ArithComparisonP_CC=>Pcmnimm"
  | Ptstimm _ _ => "ArithComparisonP_CC=>Ptstimm"
  end.

Definition string_of_name_ArithComparisonP_CV (n: arith_comparison_p) : pstring :=
  match n with
  | Pfcmp0 _ => "ArithComparisonP_CV=>Pfcmp0"
  | Pcmpimm _ _ => "ArithComparisonP_CV=>Pcmpimm"
  | Pcmnimm _ _ => "ArithComparisonP_CV=>Pcmnimm"
  | Ptstimm _ _ => "ArithComparisonP_CV=>Ptstimm"
  end.

Definition string_of_name_cset (c: testcond) : pstring :=
  match c with
  | TCeq => "Cset=>TCeq"
  | TCne => "Cset=>TCne"
  | TChs => "Cset=>TChs"
  | TClo => "Cset=>TClo"
  | TCmi => "Cset=>TCmi"
  | TCpl => "Cset=>TCpl"
  | TChi => "Cset=>TChi"
  | TCls => "Cset=>TCls"
  | TCge => "Cset=>TCge"
  | TClt => "Cset=>TClt"
  | TCgt => "Cset=>TCgt"
  | TCle => "Cset=>TCle"
  end.

Definition string_of_arith (op: arith_op): pstring :=
  match op with
  | OArithP n => string_of_name_ArithP n
  | OArithPP n => string_of_name_ArithPP n
  | OArithPPP n => string_of_name_ArithPPP n
  | OArithRR0R n => string_of_name_ArithRR0R n
  | OArithRR0R_XZR n _ => string_of_name_ArithRR0R_XZR n
  | OArithRR0 n => string_of_name_ArithRR0 n
  | OArithRR0_XZR n _ => string_of_name_ArithRR0_XZR n
  | OArithARRRR0 n => string_of_name_ArithARRRR0 n
  | OArithARRRR0_XZR n _ => string_of_name_ArithARRRR0_XZR n
  | OArithComparisonPP_CN n => string_of_name_ArithComparisonPP_CN n
  | OArithComparisonPP_CZ n => string_of_name_ArithComparisonPP_CZ n
  | OArithComparisonPP_CC n => string_of_name_ArithComparisonPP_CC n
  | OArithComparisonPP_CV n => string_of_name_ArithComparisonPP_CV n
  | OArithComparisonR0R_CN n _ => string_of_name_ArithComparisonR0R_CN n
  | OArithComparisonR0R_CZ n _ => string_of_name_ArithComparisonR0R_CZ n
  | OArithComparisonR0R_CC n _ => string_of_name_ArithComparisonR0R_CC n
  | OArithComparisonR0R_CV n _ => string_of_name_ArithComparisonR0R_CV n
  | OArithComparisonR0R_CN_XZR n _ _ => string_of_name_ArithComparisonR0R_CN_XZR n
  | OArithComparisonR0R_CZ_XZR n _ _ => string_of_name_ArithComparisonR0R_CZ_XZR n
  | OArithComparisonR0R_CC_XZR n _ _ => string_of_name_ArithComparisonR0R_CC_XZR n
  | OArithComparisonR0R_CV_XZR n _ _ => string_of_name_ArithComparisonR0R_CV_XZR n
  | OArithComparisonP_CN n => string_of_name_ArithComparisonP_CN n
  | OArithComparisonP_CZ n => string_of_name_ArithComparisonP_CZ n
  | OArithComparisonP_CC n => string_of_name_ArithComparisonP_CC n
  | OArithComparisonP_CV n => string_of_name_ArithComparisonP_CV n
  | Ocset c => string_of_name_cset c
  | Ofmovi _ => "Ofmovi"
  | Ofmovi_XZR _ => "Ofmovi_XZR"
  | Ocsel _ => "Ocsel"
  | Ofnmul _ => "Ofnmul"
  end.

Definition string_of_ofs (ofs: ptrofs) : ?? pstring :=
  (string_of_Z (Ptrofs.signed ofs)).

Definition string_of_int (n: int) : ?? pstring :=
  (string_of_Z (Int.signed n)).

Definition string_of_int64 (n: int64) : ?? pstring :=
  (string_of_Z (Int64.signed n)).

Notation "x +; y" := (Concat x y).

Definition string_of_addressing (a: addressing) : ?? pstring :=
  match a with
  | ADimm base n =>
      DO n' <~ string_of_int64 n;;
      RET ((Str "[ADimm ") +; (iregsp_name base) +; " " +; n' +; "]")
  | ADreg base r =>
      RET ((Str "[ADreg ") +; (iregsp_name base) +; " " +; (ireg_name r) +; "]")
  | ADlsl base r n =>
      DO n' <~ string_of_int n;;
      RET ((Str "[ADlsl ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]")
  | ADsxt base r n =>
      DO n' <~ string_of_int n;;
      RET ((Str "[ADsxt ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]")
  | ADuxt base r n =>
      DO n' <~ string_of_int n;;
      RET ((Str "[ADuxt ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]")
  | ADadr base id ofs =>
      DO id' <~ string_of_Z (Zpos id);;
      DO ofs' <~ string_of_ofs ofs;;
      RET ((Str "[ADadr ") +; (iregsp_name base) +; " " +; id' +; " " +; ofs' +; "]")
  | ADpostincr base n =>
      DO n' <~ string_of_int64 n;;
      RET ((Str "[ADpostincr ") +; (iregsp_name base) +; " " +; n' +; "]")
  end.

Definition string_of_ld_rd_a (ld: load_rd_a) : pstring :=
  match ld with
  | Pldrw => Str "Pldrw"
  | Pldrw_a => Str "Pldrw_a"
  | Pldrx => Str "Pldrx"
  | Pldrx_a => Str "Pldrx_a"
  | Pldrb _ => Str "Pldrb"
  | Pldrsb _ => Str "Pldrsb"
  | Pldrh _ => Str "Pldrh"
  | Pldrsh _ => Str "Pldrsh"
  | Pldrzw => Str "Pldrzw"
  | Pldrsw => Str "Pldrsw"
  | Pldrs => Str "Pldrs"
  | Pldrd => Str "Pldrd"
  | Pldrd_a => Str "Pldrd_a"
  end.

Definition string_of_ldi (ldi: ld_instruction) : ?? pstring:=
  match ldi with
  | PLd_rd_a ld rd a =>
      DO a' <~ string_of_addressing a;;
      DO rd' <~ dreg_name rd;;
      RET (Str "PLd_rd_a (" +; (string_of_ld_rd_a ld) +; " " +; rd' +; " " +; a' +; ")")
  | Pldp _ _ _ _ _ a =>
      DO a' <~ string_of_addressing a;;
      RET (Str "Pldp (" +; a' +; ")")
  end.

Definition string_of_load (op: load_op) : ?? pstring :=
  match op with
  | Oload1 ld _ a =>
      DO a' <~ string_of_addressing a;;
      (*DO ld' <~ string_of_ldi ld;;*)
      RET((Str "Oload1 ") +; " " +; string_of_ld_rd_a ld +; " " +; a' +; " ")
  | Oload2 ld _ a =>
      DO a' <~ string_of_addressing a;;
      (*DO ld' <~ string_of_ldi ld;;*)
      RET((Str "Oload2 ") +; " " +; string_of_ld_rd_a ld +; " " +; a' +; " ")
  | OloadU _ _ _ => RET (Str "OloadU")
  end.

Definition string_of_st_rs_a (st: store_rs_a) : pstring :=
  match st with
  | Pstrw => Str "Pstrw"
  | Pstrw_a => Str "Pstrw_a"
  | Pstrx => Str "Pstrx"
  | Pstrx_a => Str "Pstrx_a"
  | Pstrb => Str "Pstrb"
  | Pstrh => Str "Pstrh"
  | Pstrs => Str "Pstrs"
  | Pstrd => Str "Pstrd"
  | Pstrd_a => Str "Pstrd_a"
  end.

Definition string_of_sti (sti: st_instruction) : ?? pstring:=
  match sti with
  | PSt_rs_a st rs a =>
      DO a' <~ string_of_addressing a;;
      DO rs' <~ dreg_name rs;;
      RET (Str "PSt_rs_a (" +; (string_of_st_rs_a st) +; " " +; rs' +; " " +; a' +; ")")
  | Pstp _ _ _ _ _ a =>
      DO a' <~ string_of_addressing a;;
      RET (Str "Pstp (" +; a' +; ")")
  end.

Definition string_of_store (op: store_op) : ?? pstring :=
  match op with
  | Ostore1 st _ a =>
      DO a' <~ string_of_addressing a;;
      (*DO st' <~ string_of_sti st;;*)
      RET((Str "Ostore1 ") +; " " +; string_of_st_rs_a st +; " " +; a' +; " ")
  | Ostore2 st _ a =>
      DO a' <~ string_of_addressing a;;
      (*DO st' <~ string_of_sti st;;*)
      RET((Str "Ostore2 ") +; " " +; string_of_st_rs_a st +; " " +; a' +; " ")
  | OstoreU _ _ _ => RET (Str "OstoreU")
  end.

Definition string_of_control (op: control_op) : pstring :=
  match op with
  | Ob _ => "Ob"
  | Obc _ _ => "Obc"
  | Obl _ => "Obl"
  | Obs _ => "Obs"
  | Ocbnz _ _ => "Ocbnz"
  | Ocbz _ _ => "Ocbz"
  | Otbnz _ _ _ => "Otbnz"
  | Otbz _ _ _ => "Otbz"
  | Obtbl _ => "Obtbl"
  | OIncremPC _ => "OIncremPC"
  | OError => "OError"
  end.

Definition string_of_allocf (op: allocf_op) : pstring :=
  match op with
  | OAllocf_SP _ _ => "OAllocf_SP"
  | OAllocf_Mem _ _ => "OAllocf_Mem"
  end.

Definition string_of_freef (op: freef_op) : pstring :=
  match op with
  | OFreef_SP _ _ => "OFreef_SP"
  | OFreef_Mem _ _ => "OFreef_Mem"
  end.

Definition string_of_op (op: P.op): ?? pstring := 
  match op with
  | Arith op => RET (string_of_arith op)
  | Load op => string_of_load op
  | Store op => string_of_store op
  | Control op => RET (string_of_control op)
  | Allocframe op => RET (string_of_allocf op)
  | Freeframe op => RET (string_of_freef op)
  | Loadsymbol _ => RET (Str "Loadsymbol")
  | Constant _ => RET (Str "Constant")
  | Cvtsw2x => RET (Str "Cvtsw2x")
  | Cvtuw2x => RET (Str "Cvtuw2x")
  | Cvtx2w => RET (Str "Cvtx2w")
  (*| Fail => RET (Str "Fail")*)
  end.
End SECT_BBLOCK_EQUIV.

(** REWRITE RULES *)

Definition is_constant (o: op): bool :=
  match o with
  | OArithP _ | OArithRR0_XZR _ _ | Ofmovi_XZR _ | Loadsymbol _ | Constant _ | Obl _ | Obs _ => true
  | _ => false
  end.

Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None.
Proof.
  destruct o; simpl in * |- *; try congruence.
  destruct op0; simpl in * |- *; try congruence.
  destruct co; simpl in * |- *; try congruence;
  unfold control_eval; destruct ge; simpl in * |- *; try congruence.
Qed.

Definition main_reduce (t: Terms.term):= RET (Terms.nofail is_constant t).

Local Hint Resolve is_constant_correct: wlp.

Lemma main_reduce_correct t:
 WHEN main_reduce t ~> pt THEN Terms.match_pt t pt.
Proof.
  wlp_simplify.
Qed.

Definition reduce := {| Terms.result := main_reduce; Terms.result_correct := main_reduce_correct |}.

Definition bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool :=
  assert_same_builtin p1 p2;;
  if verb then
    IST.verb_bblock_simu_test reduce string_of_name string_of_op (trans_block p1) (trans_block p2)
  else
    IST.bblock_simu_test reduce (trans_block p1) (trans_block p2).

Local Hint Resolve IST.bblock_simu_test_correct IST.verb_bblock_simu_test_correct: wlp.

(** Main simulation (Impure) theorem *) 
Theorem bblock_simu_test_correct verb p1 p2 :
  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn lk, Asmblockprops.bblock_simu lk ge fn p1 p2.
Proof.
  wlp_simplify; eapply bblock_simu_reduce with (Ge:={| _genv := ge; _fn := fn; _lk := lk |}); eauto;
  intros; destruct H; auto.
Qed.

Hint Resolve bblock_simu_test_correct: wlp.

(** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *)

Import UnsafeImpure.

Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock): bool := 
  match unsafe_coerce (bblock_simu_test verb p1 p2) with
  | Some b => b
  | None => false
  end.

Theorem pure_bblock_simu_test_correct verb p1 p2 lk ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu lk ge fn p1 p2.
Proof.
   unfold pure_bblock_simu_test. 
   destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate.
   intros; subst. eapply bblock_simu_test_correct; eauto.
   apply unsafe_coerce_not_really_correct; eauto.
Qed.

Definition bblock_simub: Asmblock.bblock -> Asmblock.bblock -> bool := pure_bblock_simu_test true.

Lemma bblock_simub_correct p1 p2 lk ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu lk ge fn p1 p2.
Proof.
 eapply (pure_bblock_simu_test_correct true).
Qed.