Translation from Asmblock to AbstractBB

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

Require Import Lia.

Import ListNotations.
Local Open Scope list_scope.

Import OptionMonad.
Local Open Scope option_monad_scope.

Open Scope impure.

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

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

Remark builtin_arg_eq_dreg: forall (a b: builtin_arg dreg), {a=b} + {a<>b}.

Remark builtin_res_eq_dreg: forall (a b: builtin_res dreg), {a=b} + {a<>b}.

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"
     end
  | _ => match exit bb2 with
         | Some (Pbuiltin ef2 lbar2 brr2) => FAILWITH "Expected a something else: found a builtin"
         | _ => RET tt
         end
  end.

Lemma assert_same_builtin_correct (bb1 bb2: bblock):
  WHEN assert_same_builtin bb1 bb2 ~> _ THEN
    has_builtin bb1 = true \/ has_builtin bb2 = true -> exit bb1 = exit bb2.
Global Opaque assert_same_builtin.
Local Hint Resolve assert_same_builtin_correct: wlp.


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

Section IMPPARAM.

Definition env := Genv.t fundef unit.

Record genv_wrap := { _genv: env; _fn: function; }.
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)
  | Ocbz (l: label)
  | Ocbnz (l: label)
  | Obsymb (id: qualident)
  | Oblsymb (id: qualident)
  | Obtbl (tbl: list label)
  | OIncremPC (sz: Z)
  | OError.

Inductive shift_val :=
  | Sreg
  | Slsl (n: int)
  | Slsr (n: int)
  | Sasr (n: int)
  | Sror (n: int)
  .

Inductive arith_op :=
  | OArithP (n: arith_p)
  | OArithPP (n: arith_pp)
  | OArithRO0 (n: arith_ro) (i: int)
  | OArithRO1 (n: arith_ro) (s: shift_val)
  | OArithAPP (n: arith_app)
  | OArithPPP (n: arith_ppp)
  | OArithRRO0 (n: arith_rro) (i: int)
  | OArithRRO1 (n: arith_rro) (s: shift_val)
  | OArithAFFF (n: arith_afff)
  | OArithRRRR (n: arith_rrrr)
  | OArithDRRRR1 (n: arith_drrrr)
  | OArithDRRRR2 (n: arith_drrrr)
  | OArithComparisonF_CN (n: arith_comparison_f)
  | OArithComparisonF_CZ (n: arith_comparison_f)
  | OArithComparisonF_CC (n: arith_comparison_f)
  | OArithComparisonF_CV (n: arith_comparison_f)
  | OArithComparisonFF_CN (n: arith_comparison_ff)
  | OArithComparisonFF_CZ (n: arith_comparison_ff)
  | OArithComparisonFF_CC (n: arith_comparison_ff)
  | OArithComparisonFF_CV (n: arith_comparison_ff)
  | OArithComparisonRO0_CN (n: arith_comparison_ro) (i: int)
  | OArithComparisonRO0_CZ (n: arith_comparison_ro) (i: int)
  | OArithComparisonRO0_CC (n: arith_comparison_ro) (i: int)
  | OArithComparisonRO0_CV (n: arith_comparison_ro) (i: int)
  | OArithComparisonRO1_CN (n: arith_comparison_ro) (s: shift_val)
  | OArithComparisonRO1_CZ (n: arith_comparison_ro) (s: shift_val)
  | OArithComparisonRO1_CC (n: arith_comparison_ro) (s: shift_val)
  | OArithComparisonRO1_CV (n: arith_comparison_ro) (s: shift_val)
  | OSbcs0_CN (i: int)
  | OSbcs0_CZ (i: int)
  | OSbcs0_CC (i: int)
  | OSbcs0_CV (i: int)
  | OSbcs0_res (i: int)
  | OSbcs1_CN (s: shift_val)
  | OSbcs1_CZ (s: shift_val)
  | OSbcs1_CC (s: shift_val)
  | OSbcs1_CV (s: shift_val)
  | OSbcs1_res (s: shift_val)
  | Oflid (f: float)
  | Oftosizd
  | Oftouizd
  | Oftosizs
  | Oftouizs
  | Omovite00 (c: testcond) (v1 v2: int)
  | Omovite01 (c: testcond) (v1: int) (sv2: shift_val)
  | Omovite10 (c: testcond) (sv1: shift_val) (v2: int)
  | Omovite11 (c: testcond) (sv1 sv2: shift_val)
  | Ofmovite (c: testcond).

Inductive load_op :=
  | Oload1 (chunk: memory_chunk) (i: int)
  | Oload2 (chunk: memory_chunk) (s: shift_val).

Inductive store_op :=
  | Ostore1 (chunk: memory_chunk) (i: int)
  | Ostore2 (chunk: memory_chunk) (s: shift_val).

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 :=
  | Arith (op: arith_op)
  | Load (ld: load_op)
  | Store (st: store_op)
  | Memcpy (sz: Z) (is id: int)
  | Allocframe (al: allocf_op)
  | Freeframe (fr: freef_op)
  | Loadsymbol (lbl: qualident) (ofs: ptrofs)
  | Control (co: control_op)
  | Constant (v: val)
  | Osdiv
  | Oudiv.

Definition op := op_wrap.

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

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

Definition v_compare_int_test (v1 v2: val) (m: mem): CRflags :=
  let v := Val.and v1 v2 in
  {| _CN := Val.negative v;
     _CZ := Val.cmp Ceq v (Vint Int.zero);
     _CC := Vundef;
     _CV := Vundef |}.

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.cmp Ceq f1 f2 ||
                                    Float.cmp Clt f1 f2 ||
                                    Float.cmp Cgt f1 f2))) |}
  | _, _ =>
      {| _CN := Vundef;
         _CZ := Vundef;
         _CC := Vundef;
         _CV := Vundef |}
  end.

Definition v_compare_float32 (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.cmp Ceq f1 f2 ||
                                    Float32.cmp Clt f1 f2 ||
                                    Float32.cmp Cgt f1 f2))) |}
  | _, _ =>
      {| _CN := Vundef;
         _CZ := Vundef;
         _CC := Vundef;
         _CV := Vundef |}
  end.

Definition arith_eval_comparison_f (n: arith_comparison_f) (v: val) :=
  let (v1',v2') := arith_prepare_comparison_f n v in
  match n with
  | Pfcmpzd => v_compare_float v1' v2'
  | Pfcmpzs => v_compare_float32 v1' v2'
  end.

Definition arith_eval_comparison_ff (n: arith_comparison_ff) (v1 v2: val) :=
  let (v1',v2') := arith_prepare_comparison_ff n v1 v2 in
  match n with
  | Pfcmpd => v_compare_float v1' v2'
  | Pfcmps => v_compare_float32 v1' v2'
  end.

Definition arith_eval_comparison_ro (n: arith_comparison_ro) (v vo: val) :=
  let (v1',v2') := arith_prepare_comparison_ro n v vo in
  match n with
  | Pcmp | Pcmn => v_compare_int v1' v2'
  | Ptst => v_compare_int_test v1' v2'
  end.

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

Definition eval_shift_val (sv: shift_val) (v: val) :=
  match sv with
  | Sreg => v
  | Slsl n => (Val.shl v (Vint n))
  | Slsr n => (Val.shru v (Vint n))
  | Sasr n => (Val.shr v (Vint n))
  | Sror n => (Val.ror v (Vint n))
  end.

Definition cond_eval_is c vCN vCZ vCC vCV ifso ifnot is :=
  match is, flags_testcond_value c vCN vCZ vCC vCV with
  | 0, Some true => Some (Val ifso)
  | 0, Some false => Some (Val ifnot)
  | 0, None => Some (Val Vundef)
  | 1, Some b => Some (Bool b)
  | _, _ => None
  end.

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

Definition arith_op_eval (op: arith_op) (l: list value) :=
  match op, l with
  | OArithP n, [] => Some (Val (arith_eval_p n))
  | OArithPP n, [Val v] => Some (Val (arith_eval_pp n v))
  | OArithRO0 n i, [] => Some (Val (arith_eval_ro n (Vint i)))
  | OArithRO1 n s, [Val v] => Some (Val (arith_eval_ro n (eval_shift_val s v)))
  | OArithAPP n, [Val v] => Some (Val (arith_eval_app n v))
  | OArithPPP n, [Val v1; Val v2] => Some (Val (arith_eval_ppp n v1 v2))
  | OArithRRO0 n i, [Val v1] => Some (Val (arith_eval_rro n v1 (Vint i)))
  | OArithRRO1 n s, [Val v1; Val v2] => Some (Val (arith_eval_rro n v1 (eval_shift_val s v2)))
  | OArithAFFF n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_afff n v1 v2 v3))
  | OArithRRRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_rrrr n v1 v2 v3))
  | OArithDRRRR1 n, [Val v1; Val v2] => Some (Val (arith_eval_drrrr1 n v1 v2))
  | OArithDRRRR2 n, [Val v1; Val v2] => Some (Val (arith_eval_drrrr2 n v1 v2))
  | OArithComparisonF_CN n, [Val v1] => Some (Val ((arith_eval_comparison_f n v1).(_CN)))
  | OArithComparisonF_CZ n, [Val v1] => Some (Val ((arith_eval_comparison_f n v1).(_CZ)))
  | OArithComparisonF_CC n, [Val v1] => Some (Val ((arith_eval_comparison_f n v1).(_CC)))
  | OArithComparisonF_CV n, [Val v1] => Some (Val ((arith_eval_comparison_f n v1).(_CV)))
  | OArithComparisonFF_CN n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_ff n v1 v2).(_CN)))
  | OArithComparisonFF_CZ n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_ff n v1 v2).(_CZ)))
  | OArithComparisonFF_CC n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_ff n v1 v2).(_CC)))
  | OArithComparisonFF_CV n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_ff n v1 v2).(_CV)))
  | OArithComparisonRO0_CN n i, [Val v1; Memstate m] => Some (Val (((arith_eval_comparison_ro n v1 (Vint i)) m).(_CN)))
  | OArithComparisonRO0_CZ n i, [Val v1; Memstate m] => Some (Val (((arith_eval_comparison_ro n v1 (Vint i)) m).(_CZ)))
  | OArithComparisonRO0_CC n i, [Val v1; Memstate m] => Some (Val (((arith_eval_comparison_ro n v1 (Vint i)) m).(_CC)))
  | OArithComparisonRO0_CV n i, [Val v1; Memstate m] => Some (Val (((arith_eval_comparison_ro n v1 (Vint i)) m).(_CV)))
  | OArithComparisonRO1_CN n s, [Val v1; Val v2; Memstate m] =>
      Some (Val (((arith_eval_comparison_ro n v1 (eval_shift_val s v2)) m).(_CN)))
  | OArithComparisonRO1_CZ n s, [Val v1; Val v2; Memstate m] =>
      Some (Val (((arith_eval_comparison_ro n v1 (eval_shift_val s v2)) m).(_CZ)))
  | OArithComparisonRO1_CC n s, [Val v1; Val v2; Memstate m] =>
      Some (Val (((arith_eval_comparison_ro n v1 (eval_shift_val s v2)) m).(_CC)))
  | OArithComparisonRO1_CV n s, [Val v1; Val v2; Memstate m] =>
      Some (Val (((arith_eval_comparison_ro n v1 (eval_shift_val s v2)) m).(_CV)))
  | OSbcs0_CN i, [Val v1; Val cin; Memstate m] =>
      Some (Val (Val.negative (Val.sub (Val.sub v1 (Vint i))
                                       (Val.sub (Vint Int.one) cin))))
  | OSbcs0_CZ i, [Val v1; Val cin; Memstate m] =>
      Some (Val (Val.cmpu (Mem.valid_pointer m) Ceq
                   (Val.sub (Val.sub v1 (Vint i))
                            (Val.sub (Vint Int.one) cin)) (Vint Int.zero)))
  | OSbcs0_CC i, [Val v1; Val cin] =>
      Some (Val (Val.add_carry v1 (Val.notint (Vint i)) cin))
  | OSbcs0_CV i, [Val v1; Val cin] =>
      Some (Val (match v1, (Vint i), Val.sub (Vint Int.one) cin with
                 | Vint x, Vint y, Vint b => Vint (Int.sub_overflow x y b)
                 | _, _, _ => Vundef
                 end))
  | OSbcs0_res i, [Val v1; Val cin] =>
      Some (Val (Val.sub (Val.sub v1 (Vint i)) (Val.sub (Vint Int.one) cin)))
  | OSbcs1_CN s, [Val v1; Val v2; Val cin; Memstate m] =>
      Some (Val (Val.negative (Val.sub (Val.sub v1 (eval_shift_val s v2))
                                       (Val.sub (Vint Int.one) cin))))
  | OSbcs1_CZ s, [Val v1; Val v2; Val cin; Memstate m] =>
      Some (Val (Val.cmpu (Mem.valid_pointer m) Ceq
                   (Val.sub (Val.sub v1 (eval_shift_val s v2))
                            (Val.sub (Vint Int.one) cin)) (Vint Int.zero)))
  | OSbcs1_CC s, [Val v1; Val v2; Val cin] =>
      Some (Val (Val.add_carry v1 (Val.notint (eval_shift_val s v2)) cin))
  | OSbcs1_CV s, [Val v1; Val v2; Val cin] =>
      Some (Val (match v1, eval_shift_val s v2, Val.sub (Vint Int.one) cin with
                 | Vint x, Vint y, Vint b => Vint (Int.sub_overflow x y b)
                 | _, _, _ => Vundef
                 end))
  | OSbcs1_res s, [Val v1; Val v2; Val cin] =>
      Some (Val (Val.sub (Val.sub v1 (eval_shift_val s v2))
                         (Val.sub (Vint Int.one) cin)))
  | Oflid f, [] => Some (Val (Vfloat f))
  | Oftosizd, [Val v] => Some (Val (Val.maketotal (Val.intoffloat v)))
  | Oftouizd, [Val v] => Some (Val (Val.maketotal (Val.intuoffloat v)))
  | Oftosizs, [Val v] => Some (Val (Val.maketotal (Val.intofsingle v)))
  | Oftouizs, [Val v] => Some (Val (Val.maketotal (Val.intuofsingle v)))
  | Omovite00 c ifso ifnot, l' =>
      cflags_eval c l' (Vint ifso) (Vint ifnot) 0
  | Omovite01 c ifso sifnot, Val v :: l' =>
      cflags_eval c l' (Vint ifso) (eval_shift_val sifnot v) 0
  | Omovite10 c sifso ifnot, Val v :: l' =>
      cflags_eval c l' (eval_shift_val sifso v) (Vint ifnot) 0
  | Omovite11 c sifso sifnot, Val v1 :: Val v2 :: l' =>
      cflags_eval c l' (eval_shift_val sifso v1) (eval_shift_val sifnot v2) 0
  | Ofmovite c, Val v1 :: Val v2 :: l' => cflags_eval c l' v1 v2 0
  | _, _ => None
  end.

Definition call_ll_loadv (chunk: memory_chunk) (m: mem) (addr: val) :=
  SOME v' <- Mem.loadv chunk m addr IN
  Some (Val v').

Definition call_ll_storev (chunk: memory_chunk) (m: mem) (addr: val) (v: val) :=
  SOME m' <- Mem.storev chunk m addr v IN
  Some (Memstate m').

Definition load_op_eval (ld: load_op) (l: list value) :=
  match ld, l with
  | Oload1 chunk i, [Val a; Memstate m] =>
      call_ll_loadv chunk m (Val.add a (Vint i))
  | Oload2 chunk s, [Val a; Val r; Memstate m] =>
      call_ll_loadv chunk m (Val.add a (eval_shift_val s r))
  | _, _ => None
  end.

Definition store_op_eval (st: store_op) (l: list value) :=
  match st, l with
  | Ostore1 chunk i, [Val v; Val a; Memstate m] =>
      call_ll_storev chunk m (Val.add a (Vint i)) v
  | Ostore2 chunk s, [Val v; Val a; Val r; Memstate m] =>
      call_ll_storev chunk m (Val.add a (eval_shift_val s r)) v
  | _, _ => None
  end.

Definition memcpy_eval (sz: Z) (is id: int) (l: list value) :=
  match l with
  | [Val vs; Val vd; Memstate m] =>
      match Val.add vs (Vint is), Val.add vd (Vint id) with
      | Vptr bsrc osrc, Vptr bdst odst =>
          SOME bytes <- Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz IN
          SOME m' <- Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes IN
          Some (Memstate m')
      | _, _ => None
      end
  | _ => None
  end.

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

Definition control_eval (o: control_op) (l: list value) :=
  let (ge, fn) := 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 1 with
      | Some (Bool true) => goto_label_deps fn lbl vpc
      | Some (Bool false) => Some (Val vpc)
      | _ => None
      end
  | Ocbz lbl, [Val vpc; Val vr] =>
      match eval_testzero vr with
      | Some true => goto_label_deps fn lbl vpc
      | Some false => Some (Val vpc)
      | None => None
      end
  | Ocbnz lbl, [Val vpc; Val vr] =>
      match eval_testzero vr with
      | Some true => Some (Val vpc)
      | Some false => goto_label_deps fn lbl vpc
      | None => None
      end
  | Obsymb id, [] => Some (Val (Genv.symbol_address Ge.(_genv) id Ptrofs.zero))
  | Oblsymb id, [] => Some (Val (Genv.symbol_address Ge.(_genv) id Ptrofs.zero))
  | Obtbl tbl, [Val index; Val vpc] =>
      match index with
      | Vint n =>
          SOME lbl <- list_nth_z tbl (Int.unsigned n) IN
          goto_label_deps fn lbl vpc
      | _ => None
      end
  | OIncremPC sz, [Val vpc] => Some (Val (Val.offset_ptr vpc (Ptrofs.repr sz)))
  | _, _ => 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 8 in
      let sp := (Vptr stk Ptrofs.zero) in
      call_ll_storev Mint32 m1 (Val.offset_ptr sp linkofs) spv
  | OAllocf_SP sz linkofs, [Val spv; Memstate m] =>
      let (m1, stk) := Mem.alloc m 0 sz 8 in
      let sp := (Vptr stk Ptrofs.zero) in
      SOME ms <- call_ll_storev Mint32 m1 (Val.offset_ptr sp linkofs) spv IN
      Some (Val sp)
  | _, _ => None
  end.

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

Definition op_eval (op: op) (l:list value) :=
  match op, l with
  | Arith ai, l => arith_op_eval ai l
  | Load ld, l => load_op_eval ld l
  | Store st, l => store_op_eval st l
  | Memcpy sz is id, l => memcpy_eval sz is id l
  | Allocframe al, l => eval_allocf al l
  | Freeframe o, l => eval_freef o l
  | Loadsymbol lbl pos, [] => Some (Val (Genv.symbol_address Ge.(_genv) lbl pos))
  | Control o, l => control_eval o l
  | Constant v, [] => Some (Val v)
  | Osdiv, [Val v1; Val v2] => SOME v <- Val.divs v1 v2 IN Some (Val v)
  | Oudiv, [Val v1; Val v2] => SOME v <- Val.divu v1 v2 IN Some (Val v)
  | _, _ => None
  end.

Definition vz_eq (vz1 vz2: val): ?? bool :=
  RET (match vz1, vz2 with
       | Vint i1, Vint i2 => Int.eq i1 i2
       | _, _ => false
       end).
Lemma vz_eq_correct vz1 vz2:
  WHEN vz_eq vz1 vz2 ~> b THEN b = true -> vz1 = vz2.
Hint Resolve vz_eq_correct: wlp.

Definition svz_eq (svz1 svz2: shift_val): ?? bool :=
  RET (match svz1, svz2 with
       | Sreg, Sreg => true
       | Slsl n1, Slsl n2 => Int.eq n1 n2
       | Slsr n1, Slsr n2 => Int.eq n1 n2
       | Sasr n1, Sasr n2 => Int.eq n1 n2
       | Sror n1, Sror n2 => Int.eq n1 n2
       | _, _ => false
       end).
Lemma svz_eq_correct svz1 svz2:
  WHEN svz_eq svz1 svz2 ~> b THEN b = true -> svz1 = svz2.
Hint Resolve vz_eq_correct: wlp.

Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
  match o1, o2 with
  | OArithP n1, OArithP n2 => struct_eq n1 n2
  | OArithPP n1, OArithPP n2 => struct_eq n1 n2
  | OArithRO0 n1 i1, OArithRO0 n2 i2 => iandb (struct_eq n1 n2) (vz_eq (Vint i1) (Vint i2))
  | OArithRO1 n1 s1, OArithRO1 n2 s2 => iandb (struct_eq n1 n2) (svz_eq s1 s2)
  | OArithAPP n1, OArithAPP n2 => struct_eq n1 n2
  | OArithPPP n1, OArithPPP n2 => struct_eq n1 n2
  | OArithRRO0 n1 i1, OArithRRO0 n2 i2 => iandb (struct_eq n1 n2) (vz_eq (Vint i1) (Vint i2))
  | OArithRRO1 n1 s1, OArithRRO1 n2 s2 => iandb (struct_eq n1 n2) (svz_eq s1 s2)
  | OArithAFFF n1, OArithAFFF n2 => struct_eq n1 n2
  | OArithRRRR n1, OArithRRRR n2 => struct_eq n1 n2
  | OArithDRRRR1 n1, OArithDRRRR1 n2 => struct_eq n1 n2
  | OArithDRRRR2 n1, OArithDRRRR2 n2 => struct_eq n1 n2
  | OArithComparisonF_CN n1, OArithComparisonF_CN n2 => struct_eq n1 n2
  | OArithComparisonF_CZ n1, OArithComparisonF_CZ n2 => struct_eq n1 n2
  | OArithComparisonF_CC n1, OArithComparisonF_CC n2 => struct_eq n1 n2
  | OArithComparisonF_CV n1, OArithComparisonF_CV n2 => struct_eq n1 n2
  | OArithComparisonFF_CN n1, OArithComparisonFF_CN n2 => struct_eq n1 n2
  | OArithComparisonFF_CZ n1, OArithComparisonFF_CZ n2 => struct_eq n1 n2
  | OArithComparisonFF_CC n1, OArithComparisonFF_CC n2 => struct_eq n1 n2
  | OArithComparisonFF_CV n1, OArithComparisonFF_CV n2 => struct_eq n1 n2
  | OArithComparisonRO0_CN n1 i1, OArithComparisonRO0_CN n2 i2 => iandb (struct_eq n1 n2) (vz_eq (Vint i1) (Vint i2))
  | OArithComparisonRO0_CZ n1 i1, OArithComparisonRO0_CZ n2 i2 => iandb (struct_eq n1 n2) (vz_eq (Vint i1) (Vint i2))
  | OArithComparisonRO0_CC n1 i1, OArithComparisonRO0_CC n2 i2 => iandb (struct_eq n1 n2) (vz_eq (Vint i1) (Vint i2))
  | OArithComparisonRO0_CV n1 i1, OArithComparisonRO0_CV n2 i2 => iandb (struct_eq n1 n2) (vz_eq (Vint i1) (Vint i2))
  | OArithComparisonRO1_CN n1 s1, OArithComparisonRO1_CN n2 s2 => iandb (struct_eq n1 n2) (svz_eq s1 s2)
  | OArithComparisonRO1_CZ n1 s1, OArithComparisonRO1_CZ n2 s2 => iandb (struct_eq n1 n2) (svz_eq s1 s2)
  | OArithComparisonRO1_CC n1 s1, OArithComparisonRO1_CC n2 s2 => iandb (struct_eq n1 n2) (svz_eq s1 s2)
  | OArithComparisonRO1_CV n1 s1, OArithComparisonRO1_CV n2 s2 => iandb (struct_eq n1 n2) (svz_eq s1 s2)
  | OSbcs0_CN i1, OSbcs0_CN i2 => vz_eq (Vint i1) (Vint i2)
  | OSbcs0_CZ i1, OSbcs0_CZ i2 => vz_eq (Vint i1) (Vint i2)
  | OSbcs0_CC i1, OSbcs0_CC i2 => vz_eq (Vint i1) (Vint i2)
  | OSbcs0_CV i1, OSbcs0_CV i2 => vz_eq (Vint i1) (Vint i2)
  | OSbcs0_res i1, OSbcs0_res i2 => vz_eq (Vint i1) (Vint i2)
  | OSbcs1_CN s1, OSbcs1_CN s2 => svz_eq s1 s2
  | OSbcs1_CZ s1, OSbcs1_CZ s2 => svz_eq s1 s2
  | OSbcs1_CC s1, OSbcs1_CC s2 => svz_eq s1 s2
  | OSbcs1_CV s1, OSbcs1_CV s2 => svz_eq s1 s2
  | OSbcs1_res s1, OSbcs1_res s2 => svz_eq s1 s2
  | Oflid f1, Oflid f2 => struct_eq f1 f2
  | Oftosizd, Oftosizd => RET true
  | Oftouizd, Oftouizd => RET true
  | Oftosizs, Oftosizs => RET true
  | Oftouizs, Oftouizs => RET true
  | Omovite00 c1 i1 j1, Omovite00 c2 i2 j2 =>
      iandb (iandb (struct_eq c1 c2) (vz_eq (Vint i1) (Vint i2))) (vz_eq (Vint j1) (Vint j2))
  | Omovite01 c1 i1 s1, Omovite01 c2 i2 s2 =>
      iandb (iandb (struct_eq c1 c2) (vz_eq (Vint i1) (Vint i2))) (svz_eq s1 s2)
  | Omovite10 c1 s1 i1, Omovite10 c2 s2 i2 =>
      iandb (iandb (struct_eq c1 c2) (vz_eq (Vint i1) (Vint i2))) (svz_eq s1 s2)
  | Omovite11 c1 s1 t1, Omovite11 c2 s2 t2 =>
      iandb (iandb (struct_eq c1 c2) (svz_eq s1 s2)) (svz_eq t1 t2)
  | Ofmovite c1, Ofmovite c2 => struct_eq c1 c2
  | _, _ => RET false
  end.

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

Ltac desmatch :=
  match goal with
  | [ |- context [ match ?e with _ => _ end ] ]
    => destruct e
  | [ _: context [ match ?e with _ => _ end ] |- _ ]
    => destruct e
  end.

Lemma arith_op_eq_correct o1 o2:
  WHEN arith_op_eq o1 o2 ~> b THEN b = true -> o1 = o2.
Hint Resolve arith_op_eq_correct: wlp.
Opaque arith_op_eq_correct.

Definition control_op_eq (c1 c2: control_op): ?? bool :=
  match c1, c2 with
  | Ob l1, Ob l2 => struct_eq l1 l2
  | Obc c1 l1, Obc c2 l2 => iandb (struct_eq c1 c2) (struct_eq l1 l2)
  | Ocbz l1, Ocbz l2 => struct_eq l1 l2
  | Ocbnz l1, Ocbnz l2 => struct_eq l1 l2
  | Obsymb id1, Obsymb id2 => struct_eq id1 id2
  | Oblsymb id1, Oblsymb id2 => struct_eq id1 id2
  | Obtbl tbl1, Obtbl tbl2 => struct_eq tbl1 tbl2
  | OIncremPC sz1, OIncremPC sz2 => RET (Z.eqb sz1 sz2)
  | OError, OError => RET true
  | _, _ => RET false
  end.

Lemma control_op_eq_correct c1 c2:
  WHEN control_op_eq c1 c2 ~> b THEN b = true -> c1 = c2.
Hint Resolve control_op_eq_correct: wlp.
Opaque control_op_eq_correct.

Definition load_op_eq (ld1 ld2: load_op): ?? bool :=
  match ld1, ld2 with
  | Oload1 ch1 i1, Oload1 ch2 i2 => iandb (struct_eq ch1 ch2) (vz_eq (Vint i1) (Vint i2))
  | Oload2 ch1 s1, Oload2 ch2 s2 => iandb (struct_eq ch1 ch2) (svz_eq s1 s2)
  | _, _ => RET false
  end.

Lemma load_op_eq_correct ld1 ld2:
  WHEN load_op_eq ld1 ld2 ~> b THEN b = true -> ld1 = ld2.
Hint Resolve load_op_eq_correct: wlp.
Opaque load_op_eq_correct.

Definition store_op_eq (st1 st2: store_op): ?? bool :=
  match st1, st2 with
  | Ostore1 ch1 i1, Ostore1 ch2 i2 => iandb (struct_eq ch1 ch2) (vz_eq (Vint i1) (Vint i2))
  | Ostore2 ch1 s1, Ostore2 ch2 s2 => iandb (struct_eq ch1 ch2) (svz_eq s1 s2)
  | _, _ => RET false
  end.

Lemma store_op_eq_correct st1 st2:
  WHEN store_op_eq st1 st2 ~> b THEN b = true -> st1 = st2.
Hint Resolve store_op_eq_correct: wlp.
Opaque store_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)) (struct_eq linkofs1 linkofs2) | _ => RET false end
  | OAllocf_Mem sz1 linkofs1 =>
      match al2 with OAllocf_Mem sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (struct_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.
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)) (struct_eq linkofs1 linkofs2) | _ => RET false end
  | OFreef_Mem sz1 linkofs1 =>
      match fr2 with OFreef_Mem sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (struct_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.
Hint Resolve freef_op_eq_correct: wlp.
Opaque freef_op_eq_correct.

Definition op_eq (o1 o2: op): ?? bool :=
  match o1, o2 with
  | Arith i1, Arith i2 => arith_op_eq i1 i2
  | Control c1, Control c2 => control_op_eq c1 c2
  | Load ld1, Load ld2 => load_op_eq ld1 ld2
  | Store st1, Store st2 => store_op_eq st1 st2
  | Memcpy sz1 is1 id1, Memcpy sz2 is2 id2 =>
      iandb (struct_eq id1 id2) (iandb (struct_eq sz1 sz2) (struct_eq is1 is2))
  | Allocframe a1, Allocframe a2 => allocf_op_eq a1 a2
  | Freeframe f1, Freeframe f2 => freef_op_eq f1 f2
  | Loadsymbol lbl1 ofs1, Loadsymbol lbl2 ofs2 => iandb (struct_eq lbl1 lbl2) (RET (Ptrofs.eq ofs1 ofs2))
  | Constant c1, Constant c2 => struct_eq c1 c2
  | Osdiv, Osdiv => RET true
  | Oudiv, Oudiv => RET true
  | _, _ => RET false
  end.

Lemma op_eq_correct o1 o2:
 WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2.

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.

Local Open Scope positive_scope.

Definition pmem : R.t := 1.

Definition ireg_to_pos (ir: ireg): R.t :=
  match ir with
  | IR0 => 7 | IR1 => 8 | IR2 => 9 | IR3 => 10
  | IR4 => 11 | IR5 => 12 | IR6 => 13 | IR7 => 14
  | IR8 => 15 | IR9 => 16 | IR10 => 17 | IR11 => 18
  | IR12 => 19 | IR13 => 20 | IR14 => 21
  end.

Definition freg_to_pos (fr: freg): R.t :=
  match fr with
  | FR0 => 22 | FR1 => 23 | FR2 => 24 | FR3 => 25
  | FR4 => 26 | FR5 => 27 | FR6 => 28 | FR7 => 29
  | FR8 => 30 | FR9 => 31 | FR10 => 32 | FR11 => 33
  | FR12 => 34 | FR13 => 35 | FR14 => 36 | FR15 => 37
  end.

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 ir => ireg_to_pos ir
            | FR fr => freg_to_pos fr
            end
  end.
Global Opaque ppos.

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

Lemma ppos_equal: forall r r', r = r' <-> ppos r = ppos r'.

Lemma ppos_discr: forall r r', r <> r' <-> ppos r <> ppos r'.


Definition pos_to_ireg (p: R.t) : option ireg :=
  match p with
  | 7 => Some IR0 | 8 => Some IR1 | 9 => Some IR2 | 10 => Some IR3 | 11 => Some IR4
  | 12 => Some IR5 | 13 => Some IR6 | 14 => Some IR7 | 15 => Some IR8 | 16 => Some IR9
  | 17 => Some IR10 | 18 => Some IR11 | 19 => Some IR12 | 20 => Some IR13 | 21 => Some IR14
  | _ => None
  end.

Definition pos_to_freg (p: R.t) : option freg :=
  match p with
  | 22 => Some FR0 | 23 => Some FR1 | 24 => Some FR2 | 25 => Some FR3 | 26 => Some FR4
  | 27 => Some FR5 | 28 => Some FR6 | 29 => Some FR7 | 30 => Some FR8 | 31 => Some FR9
  | 32 => Some FR10 | 33 => Some FR11 | 34 => Some FR12 | 35 => Some FR13 | 36 => Some FR14
  | 37 => Some FR15
  | _ => 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
  | 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).


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))]
  | Pcbz r lbl =>
      [(#PC, Op (Control (Ocbz lbl)) (PReg (#PC) @ PReg (#r) @ Enil))]
  | Pcbnz r lbl =>
      [(#PC, Op (Control (Ocbnz lbl)) (PReg (#PC) @ PReg (#r) @ Enil))]
  | Pbsymb id _ => [(#PC, Op (Control (Obsymb id)) Enil)]
  | Pblsymb id _ => [(#RA, PReg (#PC));
                     (#PC, Op (Control (Oblsymb id)) Enil)]
  | Pbreg r sg => [(#PC, PReg (#r))]
  | Pblreg r sg => [(#RA, PReg (#PC));
                    (#PC, Old (PReg (#r)))]
  | Pbtbl r tbl => [(#PC, Op (Control (Obtbl tbl)) ((PReg (#r)) @ (PReg (#PC)) @ Enil));
                    (#IR14, 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 shift_op_reg (o: shift_op) :=
  match o with
  | SOimm n => inl n
  | SOreg ir => inr (ir, Sreg)
  | SOlsl ir n => inr (ir, Slsl n)
  | SOlsr ir n => inr (ir, Slsr n)
  | SOasr ir n => inr (ir, Sasr n)
  | SOror ir n => inr (ir, Sror n)
  end.

Definition undef_flags_llist :=
  [(#CN, Op (Constant Vundef) Enil);
   (#CZ, Op (Constant Vundef) Enil);
   (#CC, Op (Constant Vundef) Enil);
   (#CV, Op (Constant Vundef) Enil)].

Definition ai_undef_flags_llist ai :=
  if arith_undef_flags ai
  then undef_flags_llist
  else [].

Definition trans_arith (ai: ar_instruction) : inst :=
  match ai with
  | PArithP n rd => [(#rd, Op (Arith (OArithP n)) Enil)]
  | PArithPP n rd r1 => [(#rd, Op (Arith (OArithPP n)) (PReg (#r1) @ Enil))]
  | PArithRO n rd o =>
      let ll := ai_undef_flags_llist ai in
      match shift_op_reg o with
      | inl i => (#rd, Op (Arith (OArithRO0 n i)) Enil)
      | inr (r, s) => (#rd, Op (Arith (OArithRO1 n s)) (PReg (#r) @ Enil))
      end :: ll
  | PArithAPP n rd r1 => [(#rd, Op (Arith (OArithAPP n)) (PReg (#r1) @ Enil))]
  | PArithPPP n rd r1 r2 =>
      let ll := ai_undef_flags_llist ai in
      (#rd, Op (Arith (OArithPPP n)) (PReg (#r1) @ PReg (#r2) @ Enil)) :: ll
  | PArithRRO n rd r1 o =>
      let ll := ai_undef_flags_llist ai in
      match shift_op_reg o with
      | inl i =>
          (#rd, Op (Arith (OArithRRO0 n i)) (PReg (#r1) @ Enil))
      | inr (r2, s) =>
          (#rd, Op (Arith (OArithRRO1 n s)) (PReg (#r1) @ (PReg (#r2)) @ Enil))
      end :: ll
  | PArithAFFF n rd r1 r2 => [(#rd, Op (Arith (OArithAFFF n)) (PReg (#rd) @ PReg (#r1) @ PReg (#r2) @ Enil))]
  | PArithRRRR n rd r1 r2 r3 => [(#rd, Op (Arith (OArithRRRR n)) (PReg (#r1) @ PReg (#r2) @ PReg (#r3) @ Enil))]
  | PArithDRRRR n rd1 rd2 r1 r2 =>
      [(#rd1, Op (Arith (OArithDRRRR1 n)) (Old (PReg (#r1)) @ (Old (PReg (#r2)) @ Enil)));
       (#rd2, Op (Arith (OArithDRRRR2 n)) (Old (PReg (#r1)) @ (Old (PReg (#r2)) @ Enil)))]
  | PArithComparisonF n r1 =>
      [(#CN, Op (Arith (OArithComparisonF_CN n)) (PReg (#r1) @ Enil));
       (#CZ, Op (Arith (OArithComparisonF_CZ n)) (PReg (#r1) @ Enil));
       (#CC, Op (Arith (OArithComparisonF_CC n)) (PReg (#r1) @ Enil));
       (#CV, Op (Arith (OArithComparisonF_CV n)) (PReg (#r1) @ Enil))]
  | PArithComparisonFF n r1 r2 =>
      [(#CN, Op (Arith (OArithComparisonFF_CN n)) (PReg (#r1) @ PReg (#r2) @ Enil));
       (#CZ, Op (Arith (OArithComparisonFF_CZ n)) (PReg (#r1) @ PReg (#r2) @ Enil));
       (#CC, Op (Arith (OArithComparisonFF_CC n)) (PReg (#r1) @ PReg (#r2) @ Enil));
       (#CV, Op (Arith (OArithComparisonFF_CV n)) (PReg (#r1) @ PReg (#r2) @ Enil))]
  | PArithComparisonRO n r1 o =>
      match shift_op_reg o with
      | inl i =>
        [(#CN, Op (Arith (OArithComparisonRO0_CN n i)) (PReg (#r1) @ (PReg pmem) @ Enil));
         (#CZ, Op (Arith (OArithComparisonRO0_CZ n i)) (PReg (#r1) @ (PReg pmem) @ Enil));
         (#CC, Op (Arith (OArithComparisonRO0_CC n i)) (PReg (#r1) @ (PReg pmem) @ Enil));
         (#CV, Op (Arith (OArithComparisonRO0_CV n i)) (PReg (#r1) @ (PReg pmem) @ Enil))]
      | inr (r2, s) =>
        [(#CN, Op (Arith (OArithComparisonRO1_CN n s)) (PReg (#r1) @ PReg (#r2) @ (PReg pmem) @ Enil));
         (#CZ, Op (Arith (OArithComparisonRO1_CZ n s)) (PReg (#r1) @ PReg (#r2) @ (PReg pmem) @ Enil));
         (#CC, Op (Arith (OArithComparisonRO1_CC n s)) (PReg (#r1) @ PReg (#r2) @ (PReg pmem) @ Enil));
         (#CV, Op (Arith (OArithComparisonRO1_CV n s)) (PReg (#r1) @ PReg (#r2) @ (PReg pmem) @ Enil))]
      end
  | Pflid d f => [(#IR14, Op (Constant Vundef) Enil);
                  (#d, Op (Arith (Oflid f)) Enil)]
  | Pftosizd d s => [(#FR6, Op (Constant Vundef) Enil);
                     (#d, Op (Arith Oftosizd) (Old (PReg (#s)) @ Enil))]
  | Pftouizd d s => [(#FR6, Op (Constant Vundef) Enil);
                     (#d, Op (Arith Oftouizd) (Old (PReg (#s)) @ Enil))]
  | Pftosizs d s => [(#FR6, Op (Constant Vundef) Enil);
                     (#d, Op (Arith Oftosizs) (Old (PReg (#s)) @ Enil))]
  | Pftouizs d s => [(#FR6, Op (Constant Vundef) Enil);
                     (#d, Op (Arith Oftouizs) (Old (PReg (#s)) @ Enil))]
  | Pmovite c d ifso ifnot =>
      let lr := get_testcond_rlocs c in
      match shift_op_reg ifso, shift_op_reg ifnot with
      | inl i1, inl i2 => [(#d, Op (Arith (Omovite00 c i1 i2)) lr)]
      | inl i1, inr (r2, s2) => [(#d, Op (Arith (Omovite01 c i1 s2)) (PReg (#r2) @ lr))]
      | inr (r1, s1), inl i2 => [(#d, Op (Arith (Omovite10 c s1 i2)) (PReg (#r1) @ lr))]
      | inr (r1, s1), inr (r2, s2) => [(#d, Op (Arith (Omovite11 c s1 s2)) (PReg (#r1) @ PReg (#r2) @ lr))]
      end
  | Pfmovite c d ifso ifnot =>
      let lr := get_testcond_rlocs c in
      [(#d, Op (Arith (Ofmovite c)) (PReg (#ifso) @ PReg (#ifnot) @ lr))]
  | Psubs rd r1 o =>
      match shift_op_reg o with
      | inl i =>
          [(#CN, Op (Arith (OArithComparisonRO0_CN Pcmp i)) (PReg (#r1) @ (PReg pmem) @ Enil));
           (#CZ, Op (Arith (OArithComparisonRO0_CZ Pcmp i)) (Old (PReg (#r1)) @ (PReg pmem) @ Enil));
           (#CC, Op (Arith (OArithComparisonRO0_CC Pcmp i)) (Old (PReg (#r1)) @ (PReg pmem) @ Enil));
           (#CV, Op (Arith (OArithComparisonRO0_CV Pcmp i)) (Old (PReg (#r1)) @ (PReg pmem) @ Enil));
           (#rd, Op (Arith (OArithRRO0 Psub i)) (Old (PReg (#r1)) @ Enil))]
      | inr (r2, s) =>
          [(#CN, Op (Arith (OArithComparisonRO1_CN Pcmp s)) (PReg (#r1) @ PReg (#r2) @ (PReg pmem) @ Enil));
           (#CZ, Op (Arith (OArithComparisonRO1_CZ Pcmp s)) (Old (PReg (#r1)) @ Old (PReg (#r2)) @ (PReg pmem) @ Enil));
           (#CC, Op (Arith (OArithComparisonRO1_CC Pcmp s)) (Old (PReg (#r1)) @ Old (PReg (#r2)) @ (PReg pmem) @ Enil));
           (#CV, Op (Arith (OArithComparisonRO1_CV Pcmp s)) (Old (PReg (#r1)) @ Old (PReg (#r2)) @ (PReg pmem) @ Enil));
           (#rd, Op (Arith (OArithRRO1 Psub s)) (Old (PReg (#r1)) @ Old (PReg (#r2)) @ Enil))]
      end
  | Padds rd r1 o =>
      match shift_op_reg o with
      | inl i =>
          [(#CN, Op (Arith (OArithComparisonRO0_CN Pcmn i)) (PReg (#r1) @ (PReg pmem) @ Enil));
           (#CZ, Op (Arith (OArithComparisonRO0_CZ Pcmn i)) (Old (PReg (#r1)) @ (PReg pmem) @ Enil));
           (#CC, Op (Arith (OArithComparisonRO0_CC Pcmn i)) (Old (PReg (#r1)) @ (PReg pmem) @ Enil));
           (#CV, Op (Arith (OArithComparisonRO0_CV Pcmn i)) (Old (PReg (#r1)) @ (PReg pmem) @ Enil));
           (#rd, Op (Arith (OArithRRO0 Padd i)) (Old (PReg (#r1)) @ Enil))]
      | inr (r2, s) =>
          [(#CN, Op (Arith (OArithComparisonRO1_CN Pcmn s)) (PReg (#r1) @ PReg (#r2) @ (PReg pmem) @ Enil));
           (#CZ, Op (Arith (OArithComparisonRO1_CZ Pcmn s)) (Old (PReg (#r1)) @ Old (PReg (#r2)) @ (PReg pmem) @ Enil));
           (#CC, Op (Arith (OArithComparisonRO1_CC Pcmn s)) (Old (PReg (#r1)) @ Old (PReg (#r2)) @ (PReg pmem) @ Enil));
           (#CV, Op (Arith (OArithComparisonRO1_CV Pcmn s)) (Old (PReg (#r1)) @ Old (PReg (#r2)) @ (PReg pmem) @ Enil));
           (#rd, Op (Arith (OArithRRO1 Padd s)) (Old (PReg (#r1)) @ Old (PReg (#r2)) @ Enil))]
      end
  | Psbcs rd r1 o =>
      match shift_op_reg o with
      | inl i =>
          [(#CN, Op (Arith (OSbcs0_CN i))
                    (PReg (#r1) @ PReg (#CC) @ PReg pmem @ Enil));
           (#CZ, Op (Arith (OSbcs0_CZ i))
                    (Old (PReg (#r1)) @ Old (PReg (#CC)) @ PReg pmem @ Enil));
           (#CC, Op (Arith (OSbcs0_CC i))
                    (Old (PReg (#r1)) @ Old (PReg (#CC)) @ Enil));
           (#CV, Op (Arith (OSbcs0_CV i))
                    (Old (PReg (#r1)) @ Old (PReg (#CC)) @ Enil));
           (#rd, Op (Arith (OSbcs0_res i))
                    (Old (PReg (#r1)) @ Old (PReg (#CC)) @ Enil))]
      | inr (r2, s) =>
          [(#CN, Op (Arith (OSbcs1_CN s))
                    (PReg (#r1) @ PReg (#r2) @ PReg (#CC) @ PReg pmem @ Enil));
           (#CZ, Op (Arith (OSbcs1_CZ s))
                    (Old (PReg (#r1)) @ Old (PReg (#r2)) @ Old (PReg (#CC)) @ PReg pmem @ Enil));
           (#CC, Op (Arith (OSbcs1_CC s))
                    (Old (PReg (#r1)) @ Old (PReg (#r2)) @ Old (PReg (#CC)) @ Enil));
           (#CV, Op (Arith (OSbcs1_CV s))
                    (Old (PReg (#r1)) @ Old (PReg (#r2)) @ Old (PReg (#CC)) @ Enil));
           (#rd, Op (Arith (OSbcs1_res s))
                    (Old (PReg (#r1)) @ Old (PReg (#r2)) @ Old (PReg (#CC)) @ Enil))]
      end
  end.


Fixpoint trans_load_multi_i_list (ra: ireg) (ofs: Z)
                                 (l: list (ireg * memory_chunk)) : list (R.t * exp) :=
  match l with
  | nil => nil
  | (r, chk) :: tl =>
      (#r, Op (Load (Oload1 chk (Int.repr ofs))) (Old (PReg (#ra)) @ PReg (pmem) @ Enil)) ::
      trans_load_multi_i_list ra (ofs + size_chunk chk) tl
  end.

Fixpoint trans_load_multi_f_list (ra: ireg) (ofs: Z)
                                 (l: list (freg * memory_chunk)) : list (R.t * exp) :=
  match l with
  | nil => nil
  | (r, chk) :: tl =>
      (#r, Op (Load (Oload1 chk (Int.repr ofs))) (Old (PReg (#ra)) @ PReg (pmem) @ Enil)) ::
      trans_load_multi_f_list ra (ofs + size_chunk chk) tl
  end.

Fixpoint trans_store_multi_i_list (ra: ireg) (ofs: Z)
                                  (l: list (ireg * memory_chunk)) : list (R.t * exp) :=
  match l with
  | nil => nil
  | (r, chk) :: tl =>
      (pmem, Op (Store (Ostore1 chk (Int.repr ofs))) (PReg (#r) @ PReg (#ra) @ PReg (pmem) @ Enil)) ::
      trans_store_multi_i_list ra (ofs + size_chunk chk) tl
  end.

Fixpoint trans_store_multi_f_list (ra: ireg) (ofs: Z)
                                  (l: list (freg * memory_chunk)) : list (R.t * exp) :=
  match l with
  | nil => nil
  | (r, chk) :: tl =>
      (pmem, Op (Store (Ostore1 chk (Int.repr ofs))) (PReg (#r) @ PReg (#ra) @ PReg (pmem) @ Enil)) ::
      trans_store_multi_f_list ra (ofs + size_chunk chk) tl
  end.

Definition trans_stuck : list (R.t * exp) :=
  [(pmem, Op (Constant Vundef) (PReg pmem @ Enil))].

Definition trans_load (ld: ld_instruction) :=
  match ld with
  | Pcldi ldi rd ra o =>
      match shift_op_reg o with
      | inl i =>
          [(#rd, Op (Load (Oload1 (chunk_ldi ldi) i)) (PReg (#ra) @ PReg (pmem) @ Enil))]
      | inr (r, s) =>
          [(#rd, Op (Load (Oload2 (chunk_ldi ldi) s)) (PReg (#ra) @ PReg (#r) @ PReg (pmem) @ Enil))]
      end
  | Pcldipi ldi rd ra o =>
      match shift_op_reg o with
      | inl i =>
          (#ra, Op (Arith (OArithRRO0 Padd i)) (PReg (#ra) @ Enil)) ::
          (#rd, Op (Load (Oload1 (chunk_ldipi ldi) Int.zero)) (Old (PReg (#ra)) @ PReg (pmem) @ Enil)) :: undef_flags_llist
      | inr (r, s) =>
          (#ra, Op (Arith (OArithRRO1 Padd s)) (PReg (#ra) @ PReg (#r) @ Enil)) ::
          (#rd, Op (Load (Oload1 (chunk_ldipi ldi) Int.zero)) (Old (PReg (#ra)) @ PReg (pmem) @ Enil)) :: undef_flags_llist
      end
  | Pcldipd ldi rd ra o =>
      match shift_op_reg o with
      | inl i =>
          (#ra, Op (Arith (OArithRRO0 Psub i)) (PReg (#ra) @ Enil)) ::
          (#rd, Op (Load (Oload1 (chunk_ldipd ldi) Int.zero)) (PReg (#ra) @ PReg (pmem) @ Enil)) :: undef_flags_llist
      | inr (r, s) =>
          (#ra, Op (Arith (OArithRRO1 Psub s)) (PReg (#ra) @ PReg (#r) @ Enil)) ::
          (#rd, Op (Load (Oload1 (chunk_ldipd ldi) Int.zero)) (PReg (#ra) @ PReg (pmem) @ Enil)) :: undef_flags_llist
      end
  | Pclddi rd1 rd2 ra chk1 chk2 i1 i2 =>
      [(#rd1, Op (Load (Oload1 chk1 i1)) (Old (PReg (#ra)) @ PReg (pmem) @ Enil));
       (#rd2, Op (Load (Oload1 chk2 i2)) (Old (PReg (#ra)) @ PReg (pmem) @ Enil))]
  | Pclddi_pi rd1 rd2 ra chk1 chk2 i =>
      (#ra, Op (Arith (OArithRRO0 Padd i)) (PReg (#ra) @ Enil)) ::
      (#rd1, Op (Load (Oload1 chk1 Int.zero)) (Old (PReg (#ra)) @ PReg (pmem) @ Enil)) ::
      (#rd2, Op (Load (Oload1 chk2 (Int.repr 4))) (Old (PReg (#ra)) @ PReg (pmem) @ Enil)) ::
      undef_flags_llist
  | Pcldf ldf rd ra i =>
      [(#rd, Op (Load (Oload1 (chunk_ldf ldf) i)) (Old (PReg (#ra)) @ PReg (pmem) @ Enil))]
  | Pcldm ra l =>
      if ldm_iregs_wf ra l then trans_load_multi_i_list ra 0 l else trans_stuck
  | Pcvldm ra l =>
      if vldm_fregs_wf l then trans_load_multi_f_list ra 0 l else trans_stuck
  end.

Definition trans_store (st: st_instruction) :=
  match st with
  | Pcsti sti rs ra o =>
      match shift_op_reg o with
      | inl i =>
          [(pmem, Op (Store (Ostore1 (chunk_sti sti) i)) (PReg (#rs) @ PReg (#ra) @ PReg (pmem) @ Enil))]
      | inr (r, s) =>
          [(pmem, Op (Store (Ostore2 (chunk_sti sti) s)) (PReg (#rs) @ PReg (#ra) @ PReg (#r) @ PReg (pmem) @ Enil))]
      end
  | Pcstipi sti rd ra o =>
      match shift_op_reg o with
      | inl i =>
          (#ra, Op (Arith (OArithRRO0 Padd i)) (PReg (#ra) @ Enil)) ::
          (pmem, Op (Store (Ostore1 (chunk_stipi sti) Int.zero)) (Old (PReg (#rd)) @ Old (PReg (#ra)) @ PReg (pmem) @ Enil)) :: undef_flags_llist
      | inr (r, s) =>
          (#ra, Op (Arith (OArithRRO1 Padd s)) (PReg (#ra) @ PReg (#r) @ Enil)) ::
          (pmem, Op (Store (Ostore1 (chunk_stipi sti) Int.zero)) (Old (PReg (#rd)) @ Old (PReg (#ra)) @ PReg (pmem) @ Enil)) :: undef_flags_llist
      end
  | Pcstipd sti rd ra o =>
      match shift_op_reg o with
      | inl i =>
          (#ra, Op (Arith (OArithRRO0 Psub i)) (PReg (#ra) @ Enil)) ::
          (pmem, Op (Store (Ostore1 (chunk_stipd sti) Int.zero)) (Old (PReg (#rd)) @ PReg (#ra) @ PReg (pmem) @ Enil)) :: undef_flags_llist
      | inr (r, s) =>
          (#ra, Op (Arith (OArithRRO1 Psub s)) (PReg (#ra) @ PReg (#r) @ Enil)) ::
          (pmem, Op (Store (Ostore1 (chunk_stipd sti) Int.zero)) (Old (PReg (#rd)) @ PReg (#ra) @ PReg (pmem) @ Enil)) :: undef_flags_llist
      end
  | Pcstdi rs1 rs2 ra chk1 chk2 i1 i2 =>
      [(pmem, Op (Store (Ostore1 chk1 i1)) (PReg (#rs1) @ PReg (#ra) @ PReg (pmem) @ Enil));
       (pmem, Op (Store (Ostore1 chk2 i2)) (PReg (#rs2) @ PReg (#ra) @ PReg (pmem) @ Enil))]
  | Pcstdi_pi rs1 rs2 ra chk1 chk2 i =>
      (#ra, Op (Arith (OArithRRO0 Padd i)) (PReg (#ra) @ Enil)) ::
      (pmem, Op (Store (Ostore1 chk1 Int.zero)) (Old (PReg (#rs1)) @ Old (PReg (#ra)) @ PReg (pmem) @ Enil)) ::
      (pmem, Op (Store (Ostore1 chk2 (Int.repr 4))) (Old (PReg (#rs2)) @ Old (PReg (#ra)) @ PReg (pmem) @ Enil)) ::
      undef_flags_llist
  | Pcstf stf rs ra i =>
      [(pmem, Op (Store (Ostore1 (chunk_stf stf) i)) (PReg (#rs) @ PReg (#ra) @ PReg (pmem) @ Enil))]
  | Pcstm ra l =>
      if stm_iregs_wf ra l then trans_store_multi_i_list ra 0 l else trans_stuck
  | Pcvstm ra l =>
      if vstm_fregs_wf l then trans_store_multi_f_list ra 0 l else trans_stuck
  end.

Definition mcpy_rs_ofs_addr (a: mcpy_addr) :=
  match a with
  | Ofs n | PreIncr n => n
  | _ => Int.zero
  end.

Definition mcpy_rs_chg_addr (a: mcpy_addr) :=
  match a with
  | PreIncr n | PostIncr n => Some n
  | _ => None
  end.

Definition trans_memcpy_common (ras rad: ireg) (sz: Z) (mas mad: mcpy_addr) (ow: list (R.t * exp)) :=
  let add_rn := fun x y => (#x, Op (Arith (OArithRRO0 Padd y)) (PReg (#x) @ Enil)) in
  let (pre_list, suf_list) :=
    match mcpy_rs_chg_addr mas, mcpy_rs_chg_addr mad with
    | Some ns, Some nd => ((add_rn ras ns) :: ow ++ (add_rn rad nd) :: nil, undef_flags_llist)
    | Some ns, None => ((add_rn ras ns) :: ow, undef_flags_llist)
    | None, Some nd => (ow ++ (add_rn rad nd) :: nil, undef_flags_llist)
    | None, None => (ow, nil)
    end in
  let ofss := mcpy_rs_ofs_addr mas in
  let ofsd := mcpy_rs_ofs_addr mad in
  pre_list ++ [(pmem, Op (Memcpy sz ofss ofsd) (Old (PReg (#ras)) @ Old (PReg (#rad)) @ PReg (pmem) @ Enil))] ++ suf_list.

Definition trans_memcpy (cp: memcpy_instruction) (ras rad: ireg) (mas mad: mcpy_addr) :=
  match cp with
  | Pmemcpy8 tr =>
      if PregEq.eq rad tr || negb (mcpy_valid_reg ras rad mas mad)
      then [(#PC, Op OError Enil)] else
      trans_memcpy_common ras rad 1 mas mad [(#tr, Op (Constant Vundef) Enil)]
  | Pmemcpy16 tr =>
      if PregEq.eq rad tr || negb (mcpy_valid_reg ras rad mas mad)
      then [(#PC, Op OError Enil)] else
      trans_memcpy_common ras rad 2 mas mad [(#tr, Op (Constant Vundef) Enil)]
  | Pmemcpy32 tr =>
      if PregEq.eq rad tr || negb (mcpy_valid_reg ras rad mas mad)
      then [(#PC, Op OError Enil)] else
      trans_memcpy_common ras rad 4 mas mad [(#tr, Op (Constant Vundef) Enil)]
  | Pmemcpy64 tr1 tr2 =>
      if PregEq.eq rad tr1 || PregEq.eq rad tr2 ||
         negb (mcpy_valid_reg ras rad mas mad) ||
         negb (thumb tt || ls_double_valid_regs tr1 tr2)
      then [(#PC, Op OError Enil)] else
      trans_memcpy_common ras rad 8 mas mad [(#tr1, Op (Constant Vundef) Enil); (#tr2, Op (Constant Vundef) Enil)]
  end.

Definition trans_basic (b: basic): inst :=
  match b with
  | PArith ai => trans_arith ai
  | PLoad ld => trans_load ld
  | PStore st => trans_store st
  | PMemcpy cp ras rad mas mad => trans_memcpy cp ras rad mas mad
  | Pallocframe sz pos =>
      [(#IR12, PReg (#SP));
       (#SP, Op (Allocframe (OAllocf_SP sz pos)) (PReg (#SP) @ PReg pmem @ Enil));
       (pmem, Op (Allocframe (OAllocf_Mem sz pos)) (Old (PReg (#SP)) @ PReg pmem @ Enil))]
  | Pfreeframe sz pos =>
      [(pmem, Op (Freeframe (OFreef_Mem sz pos)) (PReg (#SP) @ PReg pmem @ Enil));
       (#SP, Op (Freeframe (OFreef_SP sz pos)) (PReg (#SP) @ Old (PReg pmem) @ Enil))]
  | Ploadsymbol rd lbl ofs => [(#rd, Op (Loadsymbol lbl ofs) Enil)]
  | Pnop _ | Pcfi_rel_offset _ => []
  | Psdiv rd r1 r2 =>
      let undef_regs :=
        if Archi.hardware_idiv tt then []
        else [(#IR0, Op (Constant Vundef) Enil); (#IR1, Op (Constant Vundef) Enil); (#IR2, Op (Constant Vundef) Enil);
              (#IR3, Op (Constant Vundef) Enil); (#IR12, Op (Constant Vundef) Enil); (#FR0, Op (Constant Vundef) Enil);
              (#FR1, Op (Constant Vundef) Enil); (#FR2, Op (Constant Vundef) Enil); (#FR3, Op (Constant Vundef) Enil);
              (#FR4, Op (Constant Vundef) Enil); (#FR5, Op (Constant Vundef) Enil); (#FR6, Op (Constant Vundef) Enil);
              (#FR7, Op (Constant Vundef) Enil)] in
        undef_regs ++ [(#rd, Op Osdiv (Old (PReg (#r1)) @ Old (PReg (#r2)) @ Enil))]
  | Pudiv rd r1 r2 =>
      let undef_regs :=
        if Archi.hardware_idiv tt then []
        else [(#IR0, Op (Constant Vundef) Enil); (#IR1, Op (Constant Vundef) Enil); (#IR2, Op (Constant Vundef) Enil);
              (#IR3, Op (Constant Vundef) Enil); (#IR12, Op (Constant Vundef) Enil); (#FR0, Op (Constant Vundef) Enil);
              (#FR1, Op (Constant Vundef) Enil); (#FR2, Op (Constant Vundef) Enil); (#FR3, Op (Constant Vundef) Enil);
              (#FR4, Op (Constant Vundef) Enil); (#FR5, Op (Constant Vundef) Enil); (#FR6, Op (Constant Vundef) Enil);
              (#FR7, Op (Constant Vundef) Enil)] in
        undef_regs ++ [(#rd, Op Oudiv (Old (PReg (#r1)) @ Old (PReg (#r2)) @ Enil))]
  | Pmemcpyf64 ras rad tr ofss ofsd =>
      trans_memcpy_common ras rad 8 (Ofs ofss) (Ofs ofsd) [(#tr, Op (Constant Vundef) 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).

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
  | Next rs m => exists s', s = Some s' /\ match_states (State rs m) s'
  | Stuck => 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 ireg_pos_ppos: forall r,
  ireg_to_pos r = #r.

Lemma freg_pos_ppos: forall r,
  freg_to_pos r = #r.

Lemma ireg_not_pc: forall r,
  (#PC) <> ireg_to_pos r.

Lemma ireg_not_pmem: forall r,
  ireg_to_pos r <> pmem.

Lemma ireg_not_CN: forall r,
  2 <> ireg_to_pos r.

Lemma ireg_not_CZ: forall r,
  3 <> ireg_to_pos r.

Lemma ireg_not_CC: forall r,
  4 <> ireg_to_pos r.

Lemma ireg_not_CV: forall r,
  5 <> ireg_to_pos r.

Lemma freg_not_pmem: forall r,
  freg_to_pos r <> pmem.

Lemma freg_not_CN: forall r,
  2 <> freg_to_pos r.

Lemma freg_not_CZ: forall r,
  3 <> freg_to_pos r.

Lemma freg_not_CC: forall r,
  4 <> freg_to_pos r.

Lemma freg_not_CV: forall r,
  5 <> freg_to_pos r.

Lemma dreg_not_pmem: forall (r: dreg),
  (#r) <> pmem.

Lemma preg_not_pmem: forall r,
  pmem <> # r.

Lemma dreg_not_CN: forall (r: dreg),
  2 <> (#r).

Lemma dreg_not_CZ: forall (r: dreg),
  3 <> (#r).

Lemma dreg_not_CC: forall (r: dreg),
  4 <> (#r).

Lemma dreg_not_CV: forall (r: dreg),
  5 <> (#r).

Lemma sr_update_both: forall sr rsr r1 rr v
  (HEQV: forall r : preg, sr (#r) = Val (rsr r)),
  (sr <[ #r1 <- Val v ]>) (#rr) =
  Val (rsr#r1 <- v rr).

Lemma sr_gss: forall sr pos v,
  (sr <[ pos <- v ]>) pos = v.

Lemma sr_gso: forall sr pos pos' v,
  pos <> pos' ->
  (sr <[ pos <- v ]>) pos' = sr pos'.

Lemma sr_update_overwrite: forall sr pos v1 v2,
  (sr <[ pos <- v1 ]>) <[ pos <- v2 ]> = (sr <[ pos <- v2 ]>).

Lemma general_same: forall sr rd v rsr mr
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r: preg, sr (#r) = Val (rsr r)),
  exists sw,
    Some (sr <[ #rd <- Val v ]>) = Some sw /\
    sw pmem = Memstate mr /\
    (forall r: preg, sw (#r) = Val (rsr #rd <- v r)).

Lemma Mem_loadv_add_zero: forall chunk m v,
  Mem.loadv chunk m (Val.add v (Vint Int.zero)) = Mem.loadv chunk m v.

Lemma Mem_storev_add_zero: forall chunk m v w,
  Mem.storev chunk m (Val.add v (Vint Int.zero)) w = Mem.storev chunk m v w.

Lemma undef_flags_same: forall sr (rd: dreg) v rsr mr
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r: preg, sr (#r) = Val (rsr r)),
  exists sw,
    Some (((((sr <[ #rd <- Val v ]>)
                 <[ 2 <- Val Vundef ]>)
                 <[ 3 <- Val Vundef ]>)
                 <[ 4 <- Val Vundef ]>)
                 <[ 5 <- Val Vundef ]>) = Some sw /\
    sw pmem = Memstate mr /\
    (forall r: preg, sw (#r) = Val (undef_flags rsr #rd <- v r)).

Lemma undef_flags_same': forall sr (rd: dreg) v rsr mr
  (HEQV: forall r: preg, sr (#r) = Val (rsr r)),
  exists sw,
    Some ((((((sr <[ #rd <- Val v ]>)
                  <[ pmem <- Memstate mr ]>)
                  <[ 2 <- Val Vundef ]>)
                  <[ 3 <- Val Vundef ]>)
                  <[ 4 <- Val Vundef ]>)
                  <[ 5 <- Val Vundef ]>) = Some sw /\
    sw pmem = Memstate mr /\
    (forall r: preg, sw (#r) = Val (undef_flags rsr #rd <- v r)).

Lemma undef_flags_PC_same: forall sr v rsr mr
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r: preg, sr (#r) = Val (rsr r)),
  exists sw,
    Some (((((sr <[ #PC <- Val v ]>)
                 <[ 2 <- Val Vundef ]>)
                 <[ 3 <- Val Vundef ]>)
                 <[ 4 <- Val Vundef ]>)
                 <[ 5 <- Val Vundef ]>) = Some sw /\
    sw pmem = Memstate mr /\
    (forall r: preg, sw (#r) = Val (undef_flags rsr #PC <- v r)).

Lemma compare_float32_same: forall sr mr rsr v1 v2
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r: preg, sr (#r) = Val (rsr r)),
  exists sw,
    Some ((((sr <[ #CN <- Val (_CN (v_compare_float32 v1 v2)) ]>)
                <[ #CZ <- Val (_CZ (v_compare_float32 v1 v2)) ]>)
                <[ #CC <- Val (_CC (v_compare_float32 v1 v2)) ]>)
                <[ #CV <- Val (_CV (v_compare_float32 v1 v2)) ]>) = Some sw /\
    sw pmem = Memstate mr /\
    (forall r: preg, sw (#r) = Val ((compare_float32 rsr v1 v2) r)).

Lemma compare_float_same: forall sr mr rsr v1 v2
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r: preg, sr (#r) = Val (rsr r)),
  exists sw,
    Some ((((sr <[ #CN <- Val (_CN (v_compare_float v1 v2)) ]>)
                <[ #CZ <- Val (_CZ (v_compare_float v1 v2)) ]>)
                <[ #CC <- Val (_CC (v_compare_float v1 v2)) ]>)
                <[ #CV <- Val (_CV (v_compare_float v1 v2)) ]>) = Some sw /\
    sw pmem = Memstate mr /\
    (forall r: preg, sw (#r) = Val ((compare_float rsr v1 v2) r)).

Lemma compare_int_same: forall sr mr rsr v1 v2
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r: preg, sr (#r) = Val (rsr r)),
  exists sw,
    Some ((((sr <[ #CN <- Val (_CN (v_compare_int v1 v2 mr)) ]>)
                <[ #CZ <- Val (_CZ (v_compare_int v1 v2 mr)) ]>)
                <[ #CC <- Val (_CC (v_compare_int v1 v2 mr)) ]>)
                <[ #CV <- Val (_CV (v_compare_int v1 v2 mr)) ]>) = Some sw /\
    sw pmem = Memstate mr /\
    (forall r: preg, sw (#r) = Val ((compare_int rsr v1 v2 mr) r)).

Lemma compare_int_test_same: forall sr mr rsr v1 v2
  (HMEM: sr pmem = Memstate mr)
  (HEQV: forall r: preg, sr (#r) = Val (rsr r)),
  exists sw,
    Some ((((sr <[ #CN <- Val (_CN (v_compare_int_test v1 v2 mr)) ]>)
                <[ #CZ <- Val (_CZ (v_compare_int_test v1 v2 mr)) ]>)
                <[ #CC <- Val (_CC (v_compare_int_test v1 v2 mr)) ]>)
                <[ #CV <- Val (_CV (v_compare_int_test v1 v2 mr)) ]>) = Some sw /\
    sw pmem = Memstate mr /\
    (forall r: preg, sw (#r) = Val ((compare_int_test rsr v1 v2) r)).

Section SECT_SEQ.

Variable Ge: genv.

Global Opaque ppos.

Ltac elim_destr_ite flag :=
  match goal with
  | [ |- context [ match flag with _ => _ end ] ]
    => destruct flag; try (try apply general_same; auto; fail)
  end.

Lemma trans_arith_correct rsr mr sr rsw' i:
  match_states (State rsr mr) sr ->
  exec_arith_instr i rsr mr = rsw' ->
  exists sw,
     inst_run Ge (trans_arith i) sr sr = Some sw
  /\ match_states (State rsw' mr) sw.

Local Transparent Archi.ptr64.


Lemma trans_load_multi_i_list_correct:
  forall (l: list (ireg * memory_chunk)) (ofs: Z) (ra: ireg) base rsr mr sr_old sr_cur
    (Hbase: sr_old (#ra) = Val base)
    (Hpmem: sr_cur pmem = Memstate mr)
    (HEQV_cur: forall r, sr_cur (#r) = Val (rsr r)),
  match exec_load_multi_i base ofs l rsr mr with
  | Some rs' =>
      exists sr_cur',
        inst_run Ge (trans_load_multi_i_list ra ofs l) sr_cur sr_old = Some sr_cur'
        /\ sr_cur' pmem = Memstate mr
        /\ (forall r, sr_cur' (#r) = Val (rs' r))
  | None =>
      inst_run Ge (trans_load_multi_i_list ra ofs l) sr_cur sr_old = None
  end.

Lemma trans_load_multi_f_list_correct:
  forall (l: list (freg * memory_chunk)) (ofs: Z) (ra: ireg) base rsr mr sr_old sr_cur
    (Hbase: sr_old (#ra) = Val base)
    (Hpmem: sr_cur pmem = Memstate mr)
    (HEQV_cur: forall r, sr_cur (#r) = Val (rsr r)),
  match exec_load_multi_f base ofs l rsr mr with
  | Some rs' =>
      exists sr_cur',
        inst_run Ge (trans_load_multi_f_list ra ofs l) sr_cur sr_old = Some sr_cur'
        /\ sr_cur' pmem = Memstate mr
        /\ (forall r, sr_cur' (#r) = Val (rs' r))
  | None =>
      inst_run Ge (trans_load_multi_f_list ra ofs l) sr_cur sr_old = None
  end.

Lemma trans_store_multi_i_list_correct:
  forall (l: list (ireg * memory_chunk)) (ofs: Z) (ra: ireg) rsr mr sr_old sr_cur
    (Hpmem: sr_cur pmem = Memstate mr)
    (HEQV_cur: forall r, sr_cur (#r) = Val (rsr r)),
  match exec_store_multi_i (rsr ra) ofs l rsr mr with
  | Some mr' =>
      exists sr_cur',
        inst_run Ge (trans_store_multi_i_list ra ofs l) sr_cur sr_old = Some sr_cur'
        /\ sr_cur' pmem = Memstate mr'
        /\ (forall r, sr_cur' (#r) = Val (rsr r))
  | None =>
      inst_run Ge (trans_store_multi_i_list ra ofs l) sr_cur sr_old = None
  end.

Lemma trans_store_multi_f_list_correct:
  forall (l: list (freg * memory_chunk)) (ofs: Z) (ra: ireg) rsr mr sr_old sr_cur
    (Hpmem: sr_cur pmem = Memstate mr)
    (HEQV_cur: forall r, sr_cur (#r) = Val (rsr r)),
  match exec_store_multi_f (rsr ra) ofs l rsr mr with
  | Some mr' =>
      exists sr_cur',
        inst_run Ge (trans_store_multi_f_list ra ofs l) sr_cur sr_old = Some sr_cur'
        /\ sr_cur' pmem = Memstate mr'
        /\ (forall r, sr_cur' (#r) = Val (rsr r))
  | None =>
      inst_run Ge (trans_store_multi_f_list ra ofs l) sr_cur sr_old = None
  end.

Theorem bisimu_basic rsr mr sr bi:
  match_states (State rsr mr) sr ->
  match_outcome (exec_basic Ge.(_genv) bi rsr mr) (inst_run Ge (trans_basic bi) sr sr).

Theorem bisimu_body:
  forall bdy rsr mr sr,
  match_states (State rsr mr) sr ->
  match_outcome (exec_body Ge.(_genv) bdy rsr mr) (exec Ge (trans_body bdy) sr).

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).

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 ex)) sr sr).

Theorem bisimu rsr mr sr bb:
  match_states (State rsr mr) sr ->
  match_outcome (bbstep Ge.(_genv) Ge.(_fn) bb rsr mr) (exec Ge (trans_block bb) sr).

Theorem trans_state_match: forall S, match_states S (trans_state S).

Lemma state_eq_decomp:
  forall rs1 m1 rs2 m2, rs1 = rs2 -> m1 = m2 -> State rs1 m1 = State rs2 m2.

Theorem state_equiv S1 S2 S': match_states S1 S' -> match_states S2 S' -> S1 = S2.

End SECT_SEQ.

Section SECT_BBLOCK_EQUIV.

Variable Ge: genv.

Local Hint Resolve trans_state_match: core.

Lemma bblock_simu_reduce_aux:
  forall p1 p2,
  L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
  Asmblockprops.bblock_simu_aux Ge.(_genv) Ge.(_fn) p1 p2.

Lemma incrPC_set_res_commut res: forall d vres rs,
  incrPC d (set_res (map_builtin_res DR res) vres rs) =
  set_res (map_builtin_res DR res) vres (incrPC d rs).

Lemma incrPC_undef_regs_commut l: forall d rs,
  incrPC d (undef_regs l rs) = undef_regs l (incrPC d rs).

Lemma bblock_simu_reduce:
  forall p1 p2,
  L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
  (has_builtin p1 = true \/ has_builtin p2 = true -> exit p1 = exit p2) ->
  Asmblockprops.bblock_simu Ge.(_genv) Ge.(_fn) p1 p2.


Definition ireg_name (ir: ireg): pstring :=
  match ir with
  | IR0 => Str ("IR0") | IR1 => Str ("IR1") | IR2 => Str ("IR2")
  | IR3 => Str ("IR3") | IR4 => Str ("IR4") | IR5 => Str ("IR5")
  | IR6 => Str ("IR6") | IR7 => Str ("IR7") | IR8 => Str ("IR8")
  | IR9 => Str ("IR9") | IR10 => Str ("IR10") | IR11 => Str ("IR11")
  | IR12 => Str ("IR12") | IR13 => Str ("IR13") | IR14 => Str ("IR14")
  end.

Definition freg_name (fr: freg): pstring :=
  match fr with
  | FR0 => Str ("FR0") | FR1 => Str ("FR1") | FR2 => Str ("FR2")
  | FR3 => Str ("FR3") | FR4 => Str ("FR4") | FR5 => Str ("FR5")
  | FR6 => Str ("FR6") | FR7 => Str ("FR7") | FR8 => Str ("FR8")
  | FR9 => Str ("FR9") | FR10 => Str ("FR10") | FR11 => Str ("FR11")
  | FR12 => Str ("FR12") | FR13 => Str ("FR13") | FR14 => Str ("FR14")
  | FR15 => Str ("FR15")
  end.

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

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

Definition string_of_name_ArithP (n: arith_p): pstring :=
  match n with
  | Pgetcanary => "Pgetcanary"
  | Pflis _ => "Pflis"
  | Pmovw _ => "Pmovw"
  end.

Definition string_of_name_ArithPP (n: arith_pp): pstring :=
  match n with
  | Pubfx _ _ => "Pubfx"
  | Psbfx _ _ => "Psbfx"
  | Puxtb => "Puxtb"
  | Psxtb => "Psxtb"
  | Puxth => "Puxth"
  | Psxth => "Psxth"
  | Pfcpyd => "Pfcpyd"
  | Pfabsd => "Pfabsd"
  | Pfnegd => "Pfnegd"
  | Pfabss => "Pfabss"
  | Pfnegs => "Pfnegs"
  | Pfcvtsd => "Pfcvtsd"
  | Pfcvtds => "Pfcvtds"
  | Pfsitod => "Pfsitod"
  | Pfuitod => "Pfuitod"
  | Pfsitos => "Pfsitos"
  | Pfuitos => "Pfuitos"
  | Pclz => "Pclz"
  | Prbit => "Prbit"
  | Prev => "Prev"
  | Psingle_of_bits => "Psingle_of_bits"
  | Pbits_of_single => "Pbits_of_single"
  | Phibits_of_float => "Phibits_of_float"
  | Pfsqrts => "Pfsqrts"
  | Pfsqrtd => "Pfsqrtd"
  end.

Definition string_of_name_ArithAPP (n: arith_app): pstring :=
  match n with
  | Pmovt _ => "Pmovt"
  | Pbfc _ _ => "Pbfc"
  end.

Definition string_of_name_ArithRO0 (n: arith_ro): pstring :=
  match n with
  | Pmov => "ArithRO0=>Pmov"
  | Pmvn => "ArithRO1=>Pmvn"
  end.

Definition string_of_name_ArithRO1 (n: arith_ro): pstring :=
  match n with
  | Pmov => "ArithRO1=>Pmov"
  | Pmvn => "ArithRO1=>Pmvn"
  end.

Definition string_of_name_ArithPPP (n: arith_ppp): pstring :=
  match n with
  | Pasr => "Pasr"
  | Plsl => "Plsl"
  | Plsr => "Plsr"
  | Pror => "Pror"
  | Pmul => "Pmul"
  | Pfaddd => "Pfaddd"
  | Pfdivd => "Pfdivd"
  | Pfmuld => "Pfmuld"
  | Pfsubd => "Pfsubd"
  | Pfadds => "Pfadds"
  | Pfdivs => "Pfdivs"
  | Pfmuls => "Pfmuls"
  | Pfsubs => "Pfsubs"
  | Pdouble_of_iibits => "Pdouble_of_iibits"
  | Pbfi _ _ => "Pbfi"
  end.

Definition string_of_name_ArithRRO0 (n: arith_rro): pstring :=
  match n with
  | Padd => "ArithRRO0=>Padd"
  | Pand => "ArithRRO0=>Pand"
  | Pbic => "ArithRRO0=>Pbic"
  | Peor => "ArithRRO0=>Peor"
  | Porr => "ArithRRO0=>Porr"
  | Prsb => "ArithRRO0=>Prsb"
  | Psub => "ArithRRO0=>Psub"
  end.

Definition string_of_name_ArithRRO1 (n: arith_rro): pstring :=
  match n with
  | Padd => "ArithRRO1=>Padd"
  | Pand => "ArithRRO1=>Pand"
  | Pbic => "ArithRRO1=>Pbic"
  | Peor => "ArithRRO1=>Peor"
  | Porr => "ArithRRO1=>Porr"
  | Prsb => "ArithRRO1=>Prsb"
  | Psub => "ArithRRO1=>Psub"
  end.

Definition string_of_name_ArithAFFF (n: arith_afff): pstring :=
  match n with
  | Pfmlad => "Pfmlad"
  | Pfmlsd => "Pfmlsd"
  | Pfmlas => "Pfmlas"
  | Pfmlss => "Pfmlss"
  end.

Definition string_of_name_ArithRRRR (n: arith_rrrr): pstring :=
  match n with
  | Pmla => "Pmla"
  | Pmls => "Pmls"
  end.

Definition string_of_name_ArithDRRRR1 (n: arith_drrrr): pstring :=
  match n with
  | Psmull => "ArithDRRRR1=>Psmull"
  | Pumull => "ArithDRRRR1=>Pumull"
  end.

Definition string_of_name_ArithDRRRR2 (n: arith_drrrr): pstring :=
  match n with
  | Psmull => "ArithDRRRR2=>Psmull"
  | Pumull => "ArithDRRRR2=>Pumull"
  end.

Definition string_of_name_ArithComparisonF_CN (n: arith_comparison_f): pstring :=
  match n with
  | Pfcmpzd => "ArithComparisonF_CN=>Pfcmpzd"
  | Pfcmpzs => "ArithComparisonF_CN=>Pfcmpzs"
  end.

Definition string_of_name_ArithComparisonF_CZ (n: arith_comparison_f): pstring :=
  match n with
  | Pfcmpzd => "ArithComparisonF_CZ=>Pfcmpzd"
  | Pfcmpzs => "ArithComparisonF_CZ=>Pfcmpzs"
  end.

Definition string_of_name_ArithComparisonF_CC (n: arith_comparison_f): pstring :=
  match n with
  | Pfcmpzd => "ArithComparisonF_CC=>Pfcmpzd"
  | Pfcmpzs => "ArithComparisonF_CC=>Pfcmpzs"
  end.

Definition string_of_name_ArithComparisonF_CV (n: arith_comparison_f): pstring :=
  match n with
  | Pfcmpzd => "ArithComparisonF_CV=>Pfcmpzd"
  | Pfcmpzs => "ArithComparisonF_CV=>Pfcmpzs"
  end.

Definition string_of_name_ArithComparisonFF_CN (n: arith_comparison_ff): pstring :=
  match n with
  | Pfcmpd => "ArithComparisonFF_CN=>Pfcmpd"
  | Pfcmps => "ArithComparisonFF_CN=>Pfcmps"
  end.

Definition string_of_name_ArithComparisonFF_CZ (n: arith_comparison_ff): pstring :=
  match n with
  | Pfcmpd => "ArithComparisonFF_CZ=>Pfcmpd"
  | Pfcmps => "ArithComparisonFF_CZ=>Pfcmps"
  end.

Definition string_of_name_ArithComparisonFF_CC (n: arith_comparison_ff): pstring :=
  match n with
  | Pfcmpd => "ArithComparisonFF_CC=>Pfcmpd"
  | Pfcmps => "ArithComparisonFF_CC=>Pfcmps"
  end.

Definition string_of_name_ArithComparisonFF_CV (n: arith_comparison_ff): pstring :=
  match n with
  | Pfcmpd => "ArithComparisonFF_CV=>Pfcmpd"
  | Pfcmps => "ArithComparisonFF_CV=>Pfcmps"
  end.

Definition string_of_name_ArithComparisonRO0_CN (n: arith_comparison_ro): pstring :=
  match n with
  | Pcmp => "ArithComparisonRO0_CN=>Pcmp"
  | Pcmn => "ArithComparisonRO0_CN=>Pcmn"
  | Ptst => "ArithComparisonRO0_CN=>Ptst"
  end.

Definition string_of_name_ArithComparisonRO0_CZ (n: arith_comparison_ro): pstring :=
  match n with
  | Pcmp => "ArithComparisonRO0_CZ=>Pcmp"
  | Pcmn => "ArithComparisonRO0_CZ=>Pcmn"
  | Ptst => "ArithComparisonRO0_CZ=>Ptst"
  end.

Definition string_of_name_ArithComparisonRO0_CC (n: arith_comparison_ro): pstring :=
  match n with
  | Pcmp => "ArithComparisonRO0_CC=>Pcmp"
  | Pcmn => "ArithComparisonRO0_CC=>Pcmn"
  | Ptst => "ArithComparisonRO0_CC=>Ptst"
  end.

Definition string_of_name_ArithComparisonRO0_CV (n: arith_comparison_ro): pstring :=
  match n with
  | Pcmp => "ArithComparisonRO0_CV=>Pcmp"
  | Pcmn => "ArithComparisonRO0_CV=>Pcmn"
  | Ptst => "ArithComparisonRO0_CV=>Ptst"
  end.

Definition string_of_name_ArithComparisonRO1_CN (n: arith_comparison_ro): pstring :=
  match n with
  | Pcmp => "ArithComparisonRO1_CN=>Pcmp"
  | Pcmn => "ArithComparisonRO1_CN=>Pcmn"
  | Ptst => "ArithComparisonRO1_CN=>Ptst"
  end.

Definition string_of_name_ArithComparisonRO1_CZ (n: arith_comparison_ro): pstring :=
  match n with
  | Pcmp => "ArithComparisonRO1_CZ=>Pcmp"
  | Pcmn => "ArithComparisonRO1_CZ=>Pcmn"
  | Ptst => "ArithComparisonRO1_CZ=>Ptst"
  end.

Definition string_of_name_ArithComparisonRO1_CC (n: arith_comparison_ro): pstring :=
  match n with
  | Pcmp => "ArithComparisonRO1_CC=>Pcmp"
  | Pcmn => "ArithComparisonRO1_CC=>Pcmn"
  | Ptst => "ArithComparisonRO1_CC=>Ptst"
  end.

Definition string_of_name_ArithComparisonRO1_CV (n: arith_comparison_ro): pstring :=
  match n with
  | Pcmp => "ArithComparisonRO1_CV=>Pcmp"
  | Pcmn => "ArithComparisonRO1_CV=>Pcmn"
  | Ptst => "ArithComparisonRO1_CV=>Ptst"
  end.

Definition string_of_eq_op (c: testcond): pstring :=
  match c with
  | TCeq => "TCeq"
  | TCne => "TCne"
  | TChs => "TChs"
  | TClo => "TClo"
  | TCmi => "TCmi"
  | TCpl => "TCpl"
  | TChi => "TChi"
  | TCls => "TCls"
  | TCge => "TCge"
  | TClt => "TClt"
  | TCgt => "TCgt"
  | TCle => "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
  | OArithRO0 n _ => string_of_name_ArithRO0 n
  | OArithRO1 n _ => string_of_name_ArithRO1 n
  | OArithAPP n => string_of_name_ArithAPP n
  | OArithPPP n => string_of_name_ArithPPP n
  | OArithRRO0 n _ => string_of_name_ArithRRO0 n
  | OArithRRO1 n _ => string_of_name_ArithRRO1 n
  | OArithAFFF n => string_of_name_ArithAFFF n
  | OArithRRRR n => string_of_name_ArithRRRR n
  | OArithDRRRR1 n => string_of_name_ArithDRRRR1 n
  | OArithDRRRR2 n => string_of_name_ArithDRRRR2 n
  | OArithComparisonF_CN n => string_of_name_ArithComparisonF_CN n
  | OArithComparisonF_CZ n => string_of_name_ArithComparisonF_CZ n
  | OArithComparisonF_CC n => string_of_name_ArithComparisonF_CC n
  | OArithComparisonF_CV n => string_of_name_ArithComparisonF_CV n
  | OArithComparisonFF_CN n => string_of_name_ArithComparisonFF_CN n
  | OArithComparisonFF_CZ n => string_of_name_ArithComparisonFF_CZ n
  | OArithComparisonFF_CC n => string_of_name_ArithComparisonFF_CC n
  | OArithComparisonFF_CV n => string_of_name_ArithComparisonFF_CV n
  | OArithComparisonRO0_CN n _ => string_of_name_ArithComparisonRO0_CN n
  | OArithComparisonRO0_CZ n _ => string_of_name_ArithComparisonRO0_CZ n
  | OArithComparisonRO0_CC n _ => string_of_name_ArithComparisonRO0_CC n
  | OArithComparisonRO0_CV n _ => string_of_name_ArithComparisonRO0_CV n
  | OArithComparisonRO1_CZ n _ => string_of_name_ArithComparisonRO1_CZ n
  | OArithComparisonRO1_CN n _ => string_of_name_ArithComparisonRO1_CN n
  | OArithComparisonRO1_CC n _ => string_of_name_ArithComparisonRO1_CC n
  | OArithComparisonRO1_CV n _ => string_of_name_ArithComparisonRO1_CV n
  | OSbcs0_CN _ => "OSbcs0_CN"
  | OSbcs0_CZ _ => "OSbcs0_CZ"
  | OSbcs0_CC _ => "OSbcs0_CC"
  | OSbcs0_CV _ => "OSbcs0_CV"
  | OSbcs0_res _ => "OSbcs0_res"
  | OSbcs1_CN _ => "OSbcs1_CN"
  | OSbcs1_CZ _ => "OSbcs1_CZ"
  | OSbcs1_CC _ => "OSbcs1_CC"
  | OSbcs1_CV _ => "OSbcs1_CV"
  | OSbcs1_res _ => "OSbcs1_res"
  | Oflid _ => "Oflid"
  | Oftosizd => "Oftosizd"
  | Oftouizd => "Oftouizd"
  | Oftosizs => "Oftosizs"
  | Oftouizs => "Oftouizs"
  | Omovite00 c _ _ => "Omovite00(" +; (string_of_eq_op c) +; ")"
  | Omovite01 c _ _ => "Omovite01(" +; (string_of_eq_op c) +; ")"
  | Omovite10 c _ _ => "Omovite10(" +; (string_of_eq_op c) +; ")"
  | Omovite11 c _ _ => "Omovite11(" +; (string_of_eq_op c) +; ")"
  | Ofmovite c => "Ofmovite(1" +; (string_of_eq_op c) +; ")"
  end.

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

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

Definition string_of_shift_val (sv: shift_val): ?? pstring :=
  match sv with
  | Sreg => RET (Str "[Sreg]")
  | Slsl i =>
      DO i' <~ (string_of_int i);;
      RET (Str "[Slsl" +; " " +; i' +; "]")
  | Slsr i =>
      DO i' <~ (string_of_int i);;
      RET (Str "[Slsr" +; " " +; i' +; "]")
  | Sasr i =>
      DO i' <~ (string_of_int i);;
      RET (Str "[Sasr" +; " " +; i' +; "]")
  | Sror i =>
      DO i' <~ (string_of_int i);;
      RET (Str "[Sror" +; " " +; i' +; "]")
  end.

Definition string_of_chunk_ld (c: memory_chunk): pstring :=
  match c with
  | Mint32 => "Pldr"
  | Many32 => "Pldr_a"
  | Mint32al1 => "Pldr_u"
  | Mint8unsigned => "Pldrb"
  | Mint16unsigned => "Pldrh"
  | Mint8signed => "Pldrsb"
  | Mint16signed => "Pldrsh"
  | Mfloat64 => "Pfldd"
  | Many64 => "Pfldd_a"
  | Mfloat32 => "Pflds"
  | _ => "UNDEFINED LOAD"
  end.

Definition string_of_load (op: load_op): ?? pstring :=
  match op with
  | Oload1 c i =>
      DO i' <~ string_of_int i;;
      RET ((Str "Oload1=>") +; (string_of_chunk_ld c) +; " " +; i')
  | Oload2 c sv =>
      DO i' <~ string_of_shift_val sv;;
      RET ((Str "Oload2=>") +; (string_of_chunk_ld c) +; " " +; i')
  end.

Definition string_of_chunk_st (c: memory_chunk): pstring :=
  match c with
  | Mint32 => "Pstr"
  | Many32 => "Pstr_a"
  | Mint32al1 => "Pstr_u"
  | Mint8unsigned => "Pstrb"
  | Mint16unsigned => "Pstrh"
  | Mfloat64 => "Pfstd"
  | Many64 => "Pfstd_a"
  | Mfloat32 => "Pfsts"
  | _ => "UNDEFINED LOAD"
  end.

Definition string_of_store (op: store_op): ?? pstring :=
  match op with
  | Ostore1 c i =>
      DO i' <~ string_of_int i;;
      RET ((Str "Ostore1=>") +; (string_of_chunk_st c) +; " " +; i')
  | Ostore2 c sv =>
      DO i' <~ string_of_shift_val sv;;
      RET ((Str "Ostore2=>") +; (string_of_chunk_st c) +; " " +; i')
  end.

Definition string_of_control (op: control_op) : pstring :=
  match op with
  | Ob _ => "Ob"
  | Obc c _ => "Obc(" +; (string_of_eq_op c) +; ")"
  | Ocbz _ => "Ocbz"
  | Ocbnz _ => "Ocbnz"
  | Obsymb _ => "Obsymb"
  | Oblsymb _ => "Oblsymb"
  | Obtbl _ => "Obtbl"
  | OIncremPC _ => "OIncremPC"
  | OError => "OError"
  end.

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

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

Definition string_of_op (op: P.op): ?? pstring :=
  match op with
  | Arith op => RET (string_of_arith op)
  | Load op => string_of_load op
  | Store op => string_of_store op
  | Memcpy sz is id => RET (Str "Memcpy")
  | Allocframe op => RET (string_of_allocf op)
  | Freeframe op => RET (string_of_freef op)
  | Loadsymbol _ _ => RET (Str "Loadsymbol")
  | Control op => RET (string_of_control op)
  | Constant _ => RET (Str "Constant")
  | Osdiv => RET (Str "Osdiv")
  | Oudiv => RET (Str "Oudiv")
  end.

End SECT_BBLOCK_EQUIV.


Definition is_constant (o: op): bool :=
  match o with
  | OArithP _ | OArithRO0 _ _ | Loadsymbol _ _ | Constant _
  | Obsymb _ | Oblsymb _ | Oflid _ => true
  | _ => false
  end.

Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None.

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.

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

Definition bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? unit :=
  assert_same_builtin p1 p2;;
  DO ok <~ (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));;
  assert_b ok "bblock_simu_test failure";;
  RET tt.

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

Theorem bblock_simu_test_correct verb p1 p2 :
  WHEN bblock_simu_test verb p1 p2 ~> _ THEN forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2.

#[global] Hint Resolve bblock_simu_test_correct: wlp.

Coerce bblock_simu_test into a pure function.

Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock): bool :=
  has_returned (bblock_simu_test verb p1 p2).

Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2.

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

Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2.