path: root/aarch64/Asmblockdeps.v

(* *************************************************************)
(*                                                             *)
(*             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 Asmblockgenproof0 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.

Open Scope impure.

(** auxiliary treatments of builtins *)

Definition has_builtin(bb: bblock): bool :=
 match exit bb with
 | Some (Pbuiltin _ _ _) => true
 | _ => false
 end.

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
  | _ => RET tt (* ok *)
  end.

Lemma assert_same_builtin_correct (bb1 bb2: bblock):
  WHEN assert_same_builtin bb1 bb2 ~> _ THEN
    has_builtin bb1 = true -> exit bb1 = exit bb2.
Proof.
  unfold assert_same_builtin, has_builtin.
  destruct (exit bb1) as [[]|]; simpl; try (wlp_simplify; congruence).
  destruct (exit bb2) as [[]|]; wlp_simplify.
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) (a: addressing)
  | Ostore2 (st: store_rs_a) (a: addressing)
  | OstoreU (st: store_rs_a) (a: addressing)
.

Inductive load_op :=
  | Oload1 (ld: load_rd_a) (a: addressing)
  | Oload2 (ld: load_rd_a) (a: addressing)
  | OloadU (ld: load_rd_a) (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.

Definition v_compare_int (v1 v2: val) : CRflags :=
  {| _CN := (Val.negative (Val.sub v1 v2));
     _CZ := (Val_cmpu Ceq v1 v2);
     _CC := (Val_cmpu 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_cmplu Ceq v1 v2);
     _CC := (Val_cmplu 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) (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_store_rs_a n) m v vr.

Definition exec_store2 (n: store_rs_a) (m: mem) (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_store_rs_a n) m v vr.
  
Definition exec_storeU (n: store_rs_a) (m: mem) (a: addressing) (vr: val) :=
  call_ll_storev (chunk_store_rs_a n) 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 a, [Val vr; Val vs; Memstate m] => exec_store1 st m a vr vs
  | Ostore2 st a, [Val vr; Val vs1; Val vs2; Memstate m] => exec_store2 st m a vr vs1 vs2
  | OstoreU st a, [Val vr; Memstate m] => exec_storeU st m 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 (n: load_rd_a) (m: mem) (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_load_rd_a n) (interp_load_rd_a n) m v.

Definition exec_load2 (n: load_rd_a) (m: mem) (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_load_rd_a n) (interp_load_rd_a n) m v.
  
Definition exec_loadU (n: load_rd_a) (m: mem) (a: addressing) :=
  call_ll_loadv (chunk_load_rd_a n) (interp_load_rd_a n) m None.

Definition load_eval (o: load_op) (l: list value) :=
  match o, l with
  | Oload1 st a, [Val vs; Memstate m] => exec_load1 st m a vs
  | Oload2 st a, [Val vs1; Val vs2; Memstate m] => exec_load2 st m a vs1 vs2
  | OloadU st a, [Memstate m] => exec_loadU st m 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 a1 =>
      match s2 with Ostore1 st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
  | Ostore2 st1 a1 =>
      match s2 with Ostore2 st2 a2 => iandb (phys_eq st1 st2) (struct_eq a1 a2) | _ => RET false end
  | OstoreU st1 a1 =>
      match s2 with OstoreU st2 a2 => iandb (phys_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 H0 in H; rewrite 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 a1 =>
      match l2 with Oload1 ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
  | Oload2 ld1 a1 =>
      match l2 with Oload2 ld2 a2 => iandb (phys_eq ld1 ld2) (struct_eq a1 a2) | _ => RET false end
  | OloadU ld1 a1 =>
      match l2 with OloadU ld2 a2 => iandb (phys_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 H0 in H; rewrite H; 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.
  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: try discriminate; try contradiction.
  1: intros; unfold ppos; apply ireg_to_pos_discr; congruence.
  1,2,11,18: intros; unfold ppos; try destruct irr; try destruct irr'; discriminate.
  1,3: intros; unfold ppos; try destruct irr; try destruct fr; try destruct irr'; try destruct fr'; discriminate.
  1,2,7,13: intros; unfold ppos; try destruct fr; try destruct fr'; discriminate.
  1: intros; unfold ppos; apply freg_to_pos_discr; congruence.
  1,4: intros; unfold ppos; try destruct irr; try destruct irr'; try destruct cr; try destruct cr'; discriminate.
  2,4: intros; unfold ppos; try destruct fr; try destruct fr'; try destruct cr; try destruct cr'; discriminate.
  1,2,4,5: intros; unfold ppos; try destruct cr; try destruct cr'; discriminate.
  1: intros; unfold ppos; try destruct cr; try destruct cr'; congruence.
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);
                    (#X17, 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) (rs: dreg) (a: addressing) :=
  match a with
  | ADimm base n => Op (Store (Ostore1 st a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil)
  | ADreg base r => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADlsl base r n => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADsxt base r n => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADuxt base r n => Op (Store (Ostore2 st a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil)
  | ADadr base id ofs => Op (Store (Ostore1 st a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil)
  | ADpostincr base n => Op (Store (OstoreU st a)) (PReg (#rs) @ PReg (pmem) @ Enil) (* not modeled yet *)
  end.

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

Definition trans_basic (b: basic) : inst :=
  match b with
  | PArith ai => trans_arith ai
  | PLoad ld r a => 
      let lr := eval_addressing_rlocs_ld ld a in [(#r, lr)]
  | PStore st r a => 
      let lr := eval_addressing_rlocs_st st r a in [(pmem, lr)]
  | 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))]
  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 (sr: state) r,
  sr (ireg_to_pos r) = sr (# r).
Proof.
  intros. simpl. reflexivity.
Qed.

Lemma freg_pos_ppos: forall (sr: state) r,
  sr (freg_to_pos r) = sr (# 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 sr_ireg_update_both: forall sr rsr r1 rr v
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  (sr <[ ireg_to_pos r1 <- Val (v) ]>) (#rr) =
  Val (rsr # r1 <- v rr).
Proof.
  intros. unfold assign.
  destruct (PregEq.eq r1 rr); subst.
  - rewrite Pregmap.gss. simpl. destruct r1; simpl; reflexivity.
  - rewrite Pregmap.gso; eauto.
    destruct rr; try congruence.
    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; destruct r1; simpl; try congruence.
    + destruct c; destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
    + destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
Qed.

Lemma sr_freg_update_both: forall sr rsr r1 rr v
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  (sr <[ freg_to_pos r1 <- Val (v) ]>) (#rr) =
  Val (rsr # r1 <- v rr).
Proof.
  intros. unfold assign.
  destruct (PregEq.eq r1 rr); subst.
  - rewrite Pregmap.gss. simpl. destruct r1; simpl; reflexivity.
  - rewrite Pregmap.gso; eauto.
    destruct rr; try congruence.
    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; destruct r1; simpl; try congruence.
    + destruct c; destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
    + destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
Qed.

Lemma sr_xsp_update_both: forall sr rsr rr v
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  (sr <[ #XSP <- Val (v) ]>) (#rr) =
  Val (rsr # XSP <- v rr).
Proof.
  intros. unfold assign.
  destruct (PregEq.eq XSP rr); subst.
  - rewrite Pregmap.gss. simpl. reflexivity.
  - rewrite Pregmap.gso; eauto.
    destruct rr; try congruence.
    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence.
    + destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
    + simpl; try rewrite <- HEQV; unfold ppos; try congruence.
Qed.

Lemma sr_pc_update_both: forall sr rsr rr v
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  (sr <[ #PC <- Val (v) ]>) (#rr) =
  Val (rsr # PC <- v rr).
Proof.
  intros. unfold assign.
  destruct (PregEq.eq PC rr); subst.
  - rewrite Pregmap.gss. simpl. reflexivity.
  - rewrite Pregmap.gso; eauto.
    destruct rr; try congruence.
    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence.
    + destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
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.

Ltac DI0N0 ir0 := destruct ir0; subst; simpl.

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

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 DPRF pr :=
  destruct pr as [drDPRF|crDPRF|]; 
      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|]
      | destruct frDPRF]
      | destruct crDPRF|].

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

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 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(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_ireg_update_both; eauto;
  try eapply sr_freg_update_both; eauto;
  try eapply sr_xsp_update_both; eauto;
  try eapply sr_pc_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 validate_crbit_flags c :=
  destruct c;
  [
    do 3 (rewrite assign_diff; discriminate_ppos);
    do 3 (rewrite Pregmap.gso; try discriminate);
    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
    do 2 (rewrite assign_diff; discriminate_ppos);
    do 2 (rewrite Pregmap.gso; try discriminate);
    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
    do 1 (rewrite assign_diff; discriminate_ppos);
    do 1 (rewrite Pregmap.gso; try discriminate);
    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
    rewrite sr_gss; rewrite Pregmap.gss; 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.

Lemma compare_single_res_aux: forall sr mr rsr rr
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((((sr <[ 2 <- Val (_CN (v_compare_single Vundef Vundef)) ]>) <[ 3 <-
   Val (_CZ (v_compare_single Vundef Vundef)) ]>) <[ 4 <-
  Val (_CC (v_compare_single Vundef Vundef)) ]>) <[ 5 <-
 Val (_CV (v_compare_single Vundef Vundef)) ]>) (# rr) =
Val
  ((compare_single rsr Vundef Vundef) rr).
Proof.
  intros. unfold v_compare_single, compare_single.
  (destruct rr;
    [ DDRF d; discriminate_preg_flags |
      validate_crbit_flags c |
      discriminate_preg_flags ]).
Qed.

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.
  destruct v1; destruct v2;
  try eapply compare_single_res_aux; eauto.
  unfold v_compare_single, compare_single.
  (destruct rr;
    [ DDRF d; discriminate_preg_flags |
      validate_crbit_flags c |
      discriminate_preg_flags ]).
Qed.

Lemma compare_float_res_aux: forall sr mr rsr rr
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((((sr <[ 2 <- Val (_CN (v_compare_float Vundef Vundef)) ]>) <[ 3 <-
   Val (_CZ (v_compare_float Vundef Vundef)) ]>) <[ 4 <-
  Val (_CC (v_compare_float Vundef Vundef)) ]>) <[ 5 <-
 Val (_CV (v_compare_float Vundef Vundef)) ]>) (# rr) =
Val
  ((compare_float rsr Vundef Vundef) rr).
Proof.
  intros. unfold v_compare_float, compare_float.
  (destruct rr;
    [ DDRF d; discriminate_preg_flags |
      validate_crbit_flags c |
      discriminate_preg_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.
  destruct v1; destruct v2;
  try eapply compare_float_res_aux; eauto.
  unfold v_compare_float, compare_float.
  (destruct rr;
    [ DDRF d; discriminate_preg_flags |
      validate_crbit_flags c |
      discriminate_preg_flags ]).
Qed.

Lemma compare_long_res_aux: forall sr mr rsr rr
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((((sr <[ 2 <- Val (_CN (v_compare_long Vundef Vundef)) ]>) <[ 3 <-
   Val (_CZ (v_compare_long Vundef Vundef)) ]>) <[ 4 <-
  Val (_CC (v_compare_long Vundef Vundef)) ]>) <[ 5 <-
 Val (_CV (v_compare_long Vundef Vundef)) ]>) (# rr) =
Val
  ((compare_long rsr Vundef Vundef) rr).
Proof.
  intros. unfold v_compare_long, compare_long.
  (destruct rr;
    [ DDRF d; discriminate_preg_flags |
      validate_crbit_flags c |
      discriminate_preg_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.
  destruct v1; destruct v2;
  try eapply compare_long_res_aux; eauto;
  unfold v_compare_long, compare_long;
  (destruct rr;
    [ DDRF d; discriminate_preg_flags |
      validate_crbit_flags c |
      discriminate_preg_flags ]).
Qed.

Lemma compare_int_res_aux: forall sr mr rsr rr
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
  ((((sr <[ 2 <- Val (_CN (v_compare_int Vundef Vundef)) ]>) <[ 3 <-
   Val (_CZ (v_compare_int Vundef Vundef)) ]>) <[ 4 <-
  Val (_CC (v_compare_int Vundef Vundef)) ]>) <[ 5 <-
 Val (_CV (v_compare_int Vundef Vundef)) ]>) (# rr) =
Val
  ((compare_int rsr Vundef Vundef) rr).
Proof.
  intros. unfold v_compare_int, compare_int.
  (destruct rr;
    [ DDRF d; discriminate_preg_flags |
      validate_crbit_flags c |
      discriminate_preg_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.
  destruct v1; destruct v2;
  try eapply compare_int_res_aux; eauto;
  unfold v_compare_int, compare_int;
  (destruct rr;
    [ DDRF d; discriminate_preg_flags |
      validate_crbit_flags c |
      discriminate_preg_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: DIRN1 rd; Simpl sr;
         try (rewrite assign_diff; discriminate_ppos; reflexivity);
         try replace 24 with (#X16) by auto;
         try replace 7 with (#XSP) by auto;
         try (Simpl_update; intros rr; destruct_reg_neq r rr);
         try (Simpl_update; intros rr; destruct_reg_neq XSP rr);
         try (Simpl_update; intros rr; destruct_reg_neq f0 rr).
  - (* 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 *)
    DIRN1 r2; DIRN1 r1; destruct i;
    repeat Simpl_rep sr; Simpl_exists sr;
    unfold arith_eval_comparison_pp; destruct arith_prepare_comparison_pp;
    simpl; intros rr; 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 Simpl_rep sr; Simpl_exists sr;
      unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize; destruct arith_prepare_comparison_r0r; destruct is;
      simpl; intros rr; try destruct sz;
      try (eapply compare_long_res; eauto);
      try (eapply compare_int_res; eauto)).
  - (* PArithComparisonP *)
    DIRN1 r1; destruct i;
    repeat Simpl_rep sr; Simpl_exists sr;
    unfold arith_eval_comparison_p; destruct arith_prepare_comparison_p;
    simpl; try intros rr; try destruct sz;
    try (eapply compare_single_res; eauto);
    try (eapply compare_long_res; eauto);
    try (eapply compare_int_res; eauto);
    try (eapply compare_float_res; eauto).
  - (* Pcset *)
    simpl; (*DI0N0 rd.*) 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 *)
    simpl.
    unfold eval_testcond, cflags_eval. DIRN1 r1; DIRN1 r2; destruct c; simpl;
    repeat Simpl_rep sr;
    (eexists; split; [| split]; [reflexivity | DDRM rd; Simpl_exists sr | idtac]).
    all: intros rr; destruct (PregEq.eq rr rd);
    [ subst; erewrite Pregmap.gss; erewrite sr_gss; reflexivity |
    try erewrite Pregmap.gso; try erewrite assign_diff; try rewrite H0; try fold (ppos rd); try eapply ppos_discr; eauto ].
  - (* Pfnmul *)
    simpl; destruct fsz; Simpl sr.
Qed.

Lemma sp_xsp:
  SP = XSP.
Proof.
  econstructor.
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 *)
    unfold exec_load, eval_addressing_rlocs_ld, exp_eval;
    destruct a; simpl; try destruct base; Simpl_exists sr; erewrite H;
    unfold exec_load1, exec_load2, exec_loadU; unfold call_ll_loadv;
    try destruct (Mem.loadv _ _ _); simpl; auto.
    all: eexists; split; [| split]; [ eauto | DDRF rd; eauto | idtac ];
    intros rr; destruct (PregEq.eq rr rd); subst; [ rewrite Pregmap.gss; rewrite sr_gss; reflexivity |
    rewrite assign_diff; try rewrite Pregmap.gso;
    try rewrite H0; try (fold (ppos rd); eapply ppos_discr); auto].
  - (* Store *)
    unfold exec_store, eval_addressing_rlocs_st, exp_eval;
    destruct a; simpl; DIRN1 r; try destruct base; Simpl_exists sr; erewrite H;
    unfold exec_store1, exec_store2, exec_storeU; unfold call_ll_storev;
    try destruct (Mem.storev _ _ _ _); simpl; auto.
    all: eexists; split; [| split]; [ eauto | eauto |
    intros rr; rewrite assign_diff; [ rewrite H0; auto | apply ppos_pmem_discr ]].
  - (* 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; DPRF rr; repeat Simpl_exists sr.
    + 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.
      Simpl_exists sr. intros rr; DPRF rr; repeat Simpl_exists sr.
    + rewrite <- sp_xsp; rewrite MLOAD; reflexivity.
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_cmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
             try (destruct (Val_cmplu_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_exists sr; intros rr; destruct (PregEq.eq rr PC); subst;
                  [ rewrite sr_gss, Pregmap.gss; reflexivity | rewrite !assign_diff, Pregmap.gso; auto ]);
             try (destruct (label_pos _ _ _); try reflexivity; rewrite Pregmap.gss;
                  destruct Val.offset_ptr; try reflexivity; Simpl_exists sr;
                  intros rr; destruct (PregEq.eq rr PC); subst;
                  [ rewrite sr_gss, Pregmap.gss; reflexivity | rewrite !assign_diff, Pregmap.gso; auto ];
                  rewrite Pregmap.gso; 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 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 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 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.
    repeat Simpl_rep sr. Simpl_exists sr.
    Simpl sr.
    all: repeat (intros; replace_regs_pos sr; try replace (38) with (#X30) by eauto; unfold incrPC; 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; DPRF rr; Simpl_update.
    68: rewrite sr_gss, Pregmap.gss;
        try rewrite Pregmap.gso; discriminate_ppos; fold (ppos r); rewrite H0; auto.
    all: repeat Simpl_rep sr; rewrite !Pregmap.gso; discriminate_ppos; auto.
  - (* Obtbl *)
    replace_pc. rewrite (H0 PC).
    unfold control_eval. destruct Ge. simpl. unfold incrPC.
    destruct r1.
    17: rewrite Pregmap.gss, sr_gss; try reflexivity.
    all: rewrite !Pregmap.gso, !assign_diff; discriminate_ppos;
    rewrite ireg_pos_ppos; try erewrite H0; destruct (rsr _);
    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; Simpl_exists sr;
    intros rr;
    destruct (PregEq.eq X16 rr); [ subst; Simpl_update |];
    destruct (PregEq.eq X17 rr); [ subst; Simpl_update |];
    destruct (PregEq.eq PC rr); [ subst; Simpl_update |];
    rewrite !Pregmap.gso; auto; apply ppos_discr in n; apply ppos_discr in n0; apply ppos_discr in n1;
    simpl in *;repeat Simpl_rep sr; auto.
Qed.

Theorem bisimu_exit ex sz rsr mr sr:
  match_states (State rsr mr) sr ->
  match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit (Some (PCtlFlow ex)))) sr sr).
Proof.
  intros; unfold estep.
  exploit (bisimu_control ex sz rsr mr sr); eauto.
Qed.

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

Theorem bisimu rsr mr sr bdy ex sz:
  match_states (State rsr mr) sr ->
  match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy rsr mr) (run Ge (trans_block_aux bdy sz (Some (PCtlFlow ex))) sr).
Proof.
  intros MS. unfold bbstep, trans_block_aux.
  exploit (bisimu_body bdy 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 ex sz _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.

(* TODO We should use this version, but our current definitions
does not match
Theorem bisimu rsr mr b sr ex sz:
    match_states (State rsr mr) sr -> 
    match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) (body b) rsr mr) (exec Ge (trans_block b) sr).
Proof.

  intros MS. unfold bbstep.
  exploit (bisimu_body (body b) rsr mr sr); eauto.
  unfold exec, trans_block; simpl.
  destruct (exec_body _ _ _ _); simpl.
  - unfold match_states in *. intros (s' & X1 & X2). destruct s.
    erewrite run_app_Some; eauto.
    exploit (bisimu_exit ex sz _rs _m s' s'); eauto.
    destruct Ge; simpl. destruct X2 as (X2 & X3). destruct MS as (Y1 & Y2).
    replace (6) with (#PC) by auto. erewrite X3; simpl.
    unfold trans_exit.
    destruct (inst_run _ _ _); simpl; auto.
  - intros X; erewrite run_app_None; eauto.

  intros MS. unfold bbstep, trans_block.
  exploit (bisimu_body (body b) 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 ex sz _rs _m s' s'); eauto.
    destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).
    replace (6) with (#PC) by auto. erewrite !X3; simpl.
    destruct (inst_run _ _ _ _); simpl; auto.
  - intros X; erewrite run_app_None; eauto.
Qed.*)

(*Theorem bisimu_bblock rsr mr sr bdy1 bdy2 ex sz:*)
  (*match_states (State rsr mr) sr ->*)
  (*match_outcome *)
   (*match bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy1 rsr mr with*)
   (*| Some (State rs' m') => exec_body Ge.(_lk) Ge.(_genv) bdy2 rs' m'*)
   (*| Stuck => Stuck*)
   (*end*)
   (*(run Ge ((trans_block_aux bdy1 sz (Some (PCtlFlow (ex))))++(trans_body bdy2)) sr).*)
(*Proof.*)
  (*intros.*)
  (*exploit (bisimu rsr mr sr bdy1 ex sz); eauto.*)
  (*destruct (bbstep _ _ _ _ _ _); simpl.*)
  (*- intros (s' & X1 & X2).*)
    (*erewrite run_app_Some; eauto. destruct s.*)
    (*eapply bisimu_body; eauto.*)
  (*- intros; erewrite run_app_None; eauto.*)
(*Qed.*)

(*Lemma trans_body_perserves_permutation bdy1 bdy2:*)
  (*Permutation bdy1 bdy2 ->*)
  (*Permutation (trans_body bdy1) (trans_body bdy2).*)
(*Proof.*)
  (*induction 1; simpl; econstructor; eauto.*)
(*Qed.*)
(*
Lemma trans_body_app bdy1: forall bdy2,
   trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2).
Proof.
  induction bdy1; simpl; congruence.
Qed.
*)
(*Theorem trans_block_perserves_permutation bdy1 bdy2 b:*)
  (*Permutation (bdy1 ++ bdy2) (body b) ->*)
  (*Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)).*)
(*Proof.*)
  (*intro H; unfold trans_block, trans_block_aux.*)
  (*eapply perm_trans.*)
  (*- eapply Permutation_app_tail. *)
    (*apply trans_body_perserves_permutation.*)
    (*apply Permutation_sym; eapply H.*)
  (*- rewrite trans_body_app. rewrite <-! app_assoc.*)
    (*apply Permutation_app_head.*)
    (*apply Permutation_app_comm.*)
(*Qed.*)

(*Theorem bisimu_par rs1 m1 s1' b ge fn o2:*)
    (*Ge = Genv ge fn ->*)
    (*match_states (State rs1 m1) s1' -> *)
    (*parexec_bblock ge fn b rs1 m1 o2 ->*)
  (*exists o2',*)
     (*prun Ge (trans_block b) s1' o2'*)
  (*/\ match_outcome o2 o2'.*)
(*Proof.*)
  (*intros GENV MS PAREXEC.*)
  (*inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO).*)
  (*exploit trans_block_perserves_permutation; eauto.*)
  (*intros Perm.*)
  (*exploit (bisimu_par_wio_bblock ge fn rs1 m1 s1' bdy1 bdy2 (exit b) (size b)); eauto.*)
  (*rewrite <- WIO. clear WIO.*)
  (*intros H; eexists; split. 2: eapply H.*)
  (*unfold prun; eexists; split; eauto. *)
  (*destruct (prun_iw _ _ _ _); simpl; eauto.*)
(*Qed.*)

(** sequential execution *)
(*Theorem bisimu_basic ge fn bi rs m s:*)
  (*Ge = Genv ge fn ->*)
  (*match_states (State rs m) s ->*)
  (*match_outcome (exec_basic_instr ge bi rs m) (inst_run Ge (trans_basic bi) s s).*)
(*Proof.*)
  (*intros; unfold exec_basic_instr. rewrite inst_run_prun.*)
  (*eapply bisimu_par_wio_basic; eauto.*)
(*Qed.*)

(*Lemma bisimu_body:*)
  (*forall bdy ge fn rs m s,*)
  (*Ge = Genv ge fn ->*)
  (*match_states (State rs m) s ->*)
  (*match_outcome (exec_body ge bdy rs m) (exec Ge (trans_body bdy) s).*)
(*Proof.*)
  (*induction bdy as [|i bdy]; simpl; eauto. *)
  (*intros.*)
  (*exploit (bisimu_basic ge fn i rs m s); eauto.*)
  (*destruct (exec_basic_instr _ _ _ _); simpl.*)
  (*- intros (s' & X1 & X2). rewrite X1; simpl; eauto.*)
  (*- intros X; rewrite X; simpl; auto.*)
(*Qed.*)

(*Theorem bisimu_exit ge fn b rs m s:*)
  (*Ge = Genv ge fn ->*)
  (*match_states (State rs m) s ->*)
  (*match_outcome (exec_control ge fn (exit b) (nextblock b rs) m) (inst_run Ge (trans_pcincr (size b) (trans_exit (exit b))) s s).*)
(*Proof.*)
  (*intros; unfold exec_control, nextblock. rewrite inst_run_prun. *)
  (*apply (bisimu_par_control (exit b) (size b) (Val.offset_ptr (rs PC) (Ptrofs.repr (size b))) ge fn rs rs m m s s); auto.*)
(*Qed.*)

(*Lemma bbstep_is_exec_bblock: forall bb (cfi: cf_instruction) size_bb bdy rs m rs' m' t,*)
  (*(body bb) = bdy ->*)
  (*(exit bb) = Some (PCtlFlow cfi) ->*)
  (*Ptrofs.repr (size bb) = size_bb ->*)
  (*exec_bblock Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rs m t rs' m'*)
  (*<-> (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) (cfi) size_bb bdy rs m = Next rs' m' /\ t = E0).*)
(*Proof.*)
  (*intros.*)
(*Admitted.*)

(* TODO This is the lemma we should use if we want to modelize
builtins in our scheduling process.
If we do not modelize builtins, we could use a simpler definition (trace E0) *)
(*
Theorem bisimu' rs m rs' m' bb s:
    match_states (State rs m) s -> 
    (exists t, exec_bblock Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rs m t rs' m')
    <-> (exists s', (exec Ge (trans_block bb) s) = Some s' /\ match_states (State rs' m') s').
Proof.
  intros MS.
  destruct (exit bb) eqn:EQEXIT.
  destruct c eqn:EQC.
  - split.
    + intros (t & H).
  rewrite bbstep_is_exec_bblock in H; eauto.
  eexists; split. destruct H as [H0 H1].
  generalize (bisimu )
  unfold exec_bblock.
  exploit (bisimu_body (body b) ge fn rs m s); eauto.
  unfold exec, trans_block; simpl.
  destruct (exec_body _ _ _ _); simpl.
  - intros (s' & X1 & X2).
    erewrite run_app_Some; eauto.
    exploit (bisimu_exit ge fn b rs0 m0 s'); eauto.
    subst Ge; simpl. destruct X2 as (Y1 & Y2). erewrite Y2; 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:
  forall p1 p2,
  L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
  (has_builtin p1 = true -> exit p1 = exit p2) ->
  Asmblockprops.bblock_simu Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2.
Proof.
  unfold bblock_simu. intros p1 p2 H BLT rs m rs' m' t EBB.
  generalize (H (trans_state (State rs m))); clear H.
  intro H. (* TODO How to define this correctly ?
  exploit (bisimu rs m (body p1) (trans_state (State rs m))); eauto.
  exploit (bisimu Ge rs m p2 ge fn (trans_state (State rs m))); eauto.
  destruct (exec_bblock ge fn p1 rs m); try congruence.
  intros H3 (s2' & exp2 & MS'). unfold exec in exp2, H3. rewrite exp2 in H2.
  destruct H2 as (m2' & H2 & H4). discriminate. rewrite H2 in H3.
  destruct (exec_bblock ge fn p2 rs m); simpl in H3.
  * destruct H3 as (s' & H3 & H5 & H6). inv H3. inv MS'.
    cutrewrite (rs0=rs1).
    - cutrewrite (m0=m1); auto. congruence.
    - apply functional_extensionality. intros r.
      generalize (H0 r). intros Hr. congruence.
  * discriminate.
Qed.*)
Admitted.

(** 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 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) => 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
    | _ => 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_store (op: store_op) : pstring :=
  match op with
  | Ostore1 _ _ => "Ostore1"
  | Ostore2 _ _ => "Ostore2"
  | OstoreU _ _ => "OstoreU"
  end.

Definition string_of_load (op: load_op) : pstring :=
  match op with
  | Oload1 _ _ => "Oload1"
  | Oload2 _ _ => "Oload2"
  | OloadU _ _ => "OloadU"
  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 => RET (string_of_load op)
  | Store op => RET (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 (* TODO *)
  | OArithP _ | OArithRR0_XZR _ _ | Ofmovi_XZR _ => 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 n; simpl in * |- *; try congruence;
  unfold arith_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.
Qed.
(*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.