Translation from Asmvliw to AbstractBB

Require Import AST.
Require Import 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 Parallelizability.
Require Import Asmvliw Permutation.
Require Import Chunks.

Require Import Lia.


Import ListNotations.
Local Open Scope list_scope.

Open Scope impure.


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

Section IMPPARAM.

Definition env := Genv.t fundef unit.

Inductive genv_wrap := Genv (ge: env) (fn: function).
Definition genv := genv_wrap.

Variable Ge: genv.

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

Definition value := value_wrap.

Inductive control_op :=
  | Oj_l (l: label)
  | Ocb (bt: btest) (l: label)
  | Ocbu (bt: btest) (l: label)
  | Odiv
  | Odivu
  | OError
  | OIncremPC (sz: Z)
  | Ojumptable (l: list label)
.

Inductive arith_op :=
  | OArithR (n: arith_name_r)
  | OArithRR (n: arith_name_rr)
  | OArithRI32 (n: arith_name_ri32) (imm: int)
  | OArithRI64 (n: arith_name_ri64) (imm: int64)
  | OArithRF32 (n: arith_name_rf32) (imm: float32)
  | OArithRF64 (n: arith_name_rf64) (imm: float)
  | OArithRRR (n: arith_name_rrr)
  | OArithRRI32 (n: arith_name_rri32) (imm: int)
  | OArithRRI64 (n: arith_name_rri64) (imm: int64)
  | OArithARRR (n: arith_name_arrr)
  | OArithARR (n: arith_name_arr)
  | OArithARRI32 (n: arith_name_arri32) (imm: int)
  | OArithARRI64 (n: arith_name_arri64) (imm: int64)
.

Coercion OArithR: arith_name_r >-> arith_op.
Coercion OArithRR: arith_name_rr >-> arith_op.
Coercion OArithRI32: arith_name_ri32 >-> Funclass.
Coercion OArithRI64: arith_name_ri64 >-> Funclass.
Coercion OArithRF32: arith_name_rf32 >-> Funclass.
Coercion OArithRF64: arith_name_rf64 >-> Funclass.
Coercion OArithRRR: arith_name_rrr >-> arith_op.
Coercion OArithRRI32: arith_name_rri32 >-> Funclass.
Coercion OArithRRI64: arith_name_rri64 >-> Funclass.

Inductive load_op :=
  | OLoadRRO (n: load_name) (trap: trapping_mode) (ofs: offset)
  | OLoadRRR (n: load_name) (trap: trapping_mode)
  | OLoadRRRXS (n: load_name) (trap: trapping_mode)
.

Coercion OLoadRRO: load_name >-> Funclass.

Inductive store_op :=
  | OStoreRRO (n: store_name) (ofs: offset)
  | OStoreRRR (n: store_name)
  | OStoreRRRXS (n: store_name)
.

Coercion OStoreRRO: store_name >-> Funclass.

Inductive op_wrap :=
  | Arith (ao: arith_op)
  | Load (lo: load_op)
  | Store (so: store_op)
  | Control (co: control_op)
  | Allocframe (sz: Z) (pos: ptrofs)
  | Allocframe2 (sz: Z) (pos: ptrofs)
  | Freeframe (sz: Z) (pos: ptrofs)
  | Freeframe2 (sz: Z) (pos: ptrofs)
  | Constant (v: val)
  | Fail
.

Coercion Arith: arith_op >-> op_wrap.
Coercion Load: load_op >-> op_wrap.
Coercion Store: store_op >-> op_wrap.
Coercion Control: control_op >-> op_wrap.

Definition op := op_wrap.

Definition arith_eval (ao: arith_op) (l: list value) :=
  let (ge, fn) := Ge in
  match ao, l with
  | OArithR n, [] => Some (Val (arith_eval_r ge n))

  | OArithRR n, [Val v] => Some (Val (arith_eval_rr n v))

  | OArithRI32 n i, [] => Some (Val (arith_eval_ri32 n i))
  | OArithRI64 n i, [] => Some (Val (arith_eval_ri64 n i))
  | OArithRF32 n i, [] => Some (Val (arith_eval_rf32 n i))
  | OArithRF64 n i, [] => Some (Val (arith_eval_rf64 n i))

  | OArithRRR n, [Val v1; Val v2] => Some (Val (arith_eval_rrr n v1 v2))
  | OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i))
  | OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i))

  | OArithARR n, [Val v1; Val v2] => Some (Val (arith_eval_arr n v1 v2))
  | OArithARRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrr n v1 v2 v3))
  | OArithARRI32 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri32 n v1 v2 i))
  | OArithARRI64 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri64 n v1 v2 i))

  | _, _ => None
  end.

Definition exec_incorrect_load trap :=
  match trap with
  | TRAP => None
  | NOTRAP => Some (Val Vundef)
  end.

Definition exec_load_deps_offset (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) :=
  let (ge, fn) := Ge in
  match (eval_offset ofs) with
  | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with
              | None => exec_incorrect_load trap
              | Some vl => Some (Val vl)
              end
  | _ => None
  end.

Definition exec_load_deps_reg (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) :=
  match Mem.loadv chunk m (Val.addl v vo) with
  | None => exec_incorrect_load trap
  | Some vl => Some (Val vl)
  end.

Definition exec_load_deps_regxs (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) :=
  match Mem.loadv chunk m (Val.addl v (Val.shll vo (scale_of_chunk chunk))) with
  | None => exec_incorrect_load trap
  | Some vl => Some (Val vl)
  end.

Definition load_eval (lo: load_op) (l: list value) :=
  match lo, l with
  | OLoadRRO n trap ofs, [Val v; Memstate m] => exec_load_deps_offset trap (load_chunk n) m v ofs
  | OLoadRRR n trap, [Val v; Val vo; Memstate m] => exec_load_deps_reg trap (load_chunk n) m v vo
  | OLoadRRRXS n trap, [Val v; Val vo; Memstate m] => exec_load_deps_regxs trap (load_chunk n) m v vo
  | _, _ => None
  end.

Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) :=
  let (ge, fn) := Ge in
  match (eval_offset ofs) with
  | OK ptr => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with
              | None => None
              | Some m' => Some (Memstate m')
              end
  | _ => None
  end.

Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) :=
  match Mem.storev chunk m (Val.addl va vo) vs with
  | None => None
  | Some m' => Some (Memstate m')
  end.

Definition exec_store_deps_regxs (chunk: memory_chunk) (m: mem) (vs va vo: val) :=
  match Mem.storev chunk m (Val.addl va (Val.shll vo (scale_of_chunk chunk))) vs with
  | None => None
  | Some m' => Some (Memstate m')
  end.

Definition store_eval (so: store_op) (l: list value) :=
  match so, l with
  | OStoreRRO n ofs, [Val vs; Val va; Memstate m] => exec_store_deps_offset (store_chunk n) m vs va ofs
  | OStoreRRR n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_reg (store_chunk n) m vs va vo
  | OStoreRRRXS n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_regxs (store_chunk n) m vs va vo
  | _, _ => None
  end.

Local Open Scope Z.

Remark size_chunk_positive: forall chunk,
    (size_chunk chunk) > 0.

Remark size_chunk_small: forall chunk,
    (size_chunk chunk) <= 8.

Definition disjoint_chunks
           (ofs1 : offset) (chunk1 : memory_chunk)
           (ofs2 : offset) (chunk2 : memory_chunk) :=
  Intv.disjoint ((Ptrofs.unsigned ofs1),
                 ((Ptrofs.unsigned ofs1) + (size_chunk chunk1)))
                ((Ptrofs.unsigned ofs2),
                 ((Ptrofs.unsigned ofs2) + (size_chunk chunk2))).

Definition small_offset_threshold := 18446744073709551608.

Lemma store_store_disjoint_offsets :
  forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m1 m2 m1' m2',
    (disjoint_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2)) ->
    (Ptrofs.unsigned ofs1) < small_offset_threshold ->
    (Ptrofs.unsigned ofs2) < small_offset_threshold ->
    store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) ->
    store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) ->
    store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0] = Some (Memstate m1') ->
    store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m1'] = Some (Memstate m2') ->
    m2 = m2'.

Lemma load_store_disjoint_offsets :
  forall n1 n2 tm ofs1 ofs2 vs va m0 m1,
    (disjoint_chunks ofs1 (store_chunk n1) ofs2 (load_chunk n2)) ->
    (Ptrofs.unsigned ofs1) < small_offset_threshold ->
    (Ptrofs.unsigned ofs2) < small_offset_threshold ->
    store_eval (OStoreRRO n1 ofs1) [vs; va; Memstate m0] = Some (Memstate m1) ->
    load_eval (OLoadRRO n2 tm ofs2) [va; Memstate m1] =
    load_eval (OLoadRRO n2 tm ofs2) [va; Memstate m0].

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 eval_branch_deps (f: function) (l: label) (vpc: val) (res: option bool) :=
  match res with
    | Some true => goto_label_deps f l vpc
    | Some false => Some (Val vpc)
    | None => None
  end.

Definition control_eval (o: control_op) (l: list value) :=
  let (ge, fn) := Ge in
  match o, l with
  | (Ojumptable 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
  | Oj_l l, [Val vpc] => goto_label_deps fn l vpc
  | Ocb bt l, [Val v; Val vpc] =>
    match cmp_for_btest bt with
    | (Some c, Int) => eval_branch_deps fn l vpc (Val.cmp_bool c v (Vint (Int.repr 0)))
    | (Some c, Long) => eval_branch_deps fn l vpc (Val.cmpl_bool c v (Vlong (Int64.repr 0)))
    | (None, _) => None
    end
  | Ocbu bt l, [Val v; Val vpc] =>
    match cmpu_for_btest bt with
    | (Some c, Int) => eval_branch_deps fn l vpc (Val.mxcmpu_bool c v (Vint (Int.repr 0)))
    | (Some c, Long) => eval_branch_deps fn l vpc (Val.mxcmplu_bool c v (Vlong (Int64.repr 0)))
    | (None, _) => None
    end
  | Odiv, [Val v1; Val v2] =>
    match Val.divs v1 v2 with
    | Some v => Some (Val v)
    | None => None
    end
  | Odivu, [Val v1; Val v2] =>
    match Val.divu v1 v2 with
    | Some v => Some (Val v)
    | None => None
    end
  | OIncremPC sz, [Val vpc] => Some (Val (Val.offset_ptr vpc (Ptrofs.repr sz)))
  | OError, _ => None
  | _, _ => None
  end.

Definition op_eval (o: op) (l: list value) :=
  match o, l with
  | Arith o, l => arith_eval o l
  | Load o, l => load_eval o l
  | Store o, l => store_eval o l
  | Control o, l => control_eval o l
  | Allocframe sz pos, [Val spv; Memstate m] =>
      let (m1, stk) := Mem.alloc m 0 sz in
      let sp := (Vptr stk Ptrofs.zero) in
      match Mem.storev Mptr m1 (Val.offset_ptr sp pos) spv with
      | None => None
      | Some m => Some (Memstate m)
      end
  | Allocframe2 sz pos, [Val spv; Memstate m] =>
      let (m1, stk) := Mem.alloc m 0 sz in
      let sp := (Vptr stk Ptrofs.zero) in
      match Mem.storev Mptr m1 (Val.offset_ptr sp pos) spv with
      | None => None
      | Some m => Some (Val sp)
      end
  | Freeframe sz pos, [Val spv; Memstate m] =>
      match Mem.loadv Mptr m (Val.offset_ptr spv pos) 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
  | Freeframe2 sz pos, [Val spv; Memstate m] =>
      match Mem.loadv Mptr m (Val.offset_ptr spv pos) with
      | None => None
      | Some v =>
          match spv with
          | Vptr stk ofs =>
              match Mem.free m stk 0 sz with
              | None => None
              | Some m' => Some (Val v)
              end
          | _ => None
          end
      end
  | Constant v, [] => Some (Val v)
  | Fail, _ => None
  | _, _ => None
  end.


Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
  match o1 with
  | OArithR n1 =>
     match o2 with OArithR n2 => struct_eq n1 n2 | _ => RET false end
  | OArithRR n1 =>
     match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end
  | OArithRI32 n1 i1 =>
     match o2 with OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
  | OArithRI64 n1 i1 =>
     match o2 with OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
  | OArithRF32 n1 i1 =>
     match o2 with OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
  | OArithRF64 n1 i1 =>
     match o2 with OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
  | OArithRRR n1 =>
     match o2 with OArithRRR n2 => phys_eq n1 n2 | _ => RET false end
  | OArithRRI32 n1 i1 =>
     match o2 with OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
  | OArithRRI64 n1 i1 =>
     match o2 with OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
  | OArithARRR n1 =>
     match o2 with OArithARRR n2 => phys_eq n1 n2 | _ => RET false end
  | OArithARR n1 =>
     match o2 with OArithARR n2 => phys_eq n1 n2 | _ => RET false end
  | OArithARRI32 n1 i1 =>
     match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
  | OArithARRI64 n1 i1 =>
     match o2 with OArithARRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => 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.
Hint Resolve arith_op_eq_correct: wlp.
Opaque arith_op_eq_correct.

Definition offset_eq (ofs1 ofs2 : offset): ?? bool :=
  RET (Ptrofs.eq ofs1 ofs2).

Lemma offset_eq_correct ofs1 ofs2:
  WHEN offset_eq ofs1 ofs2 ~> b THEN b = true -> ofs1 = ofs2.
Hint Resolve offset_eq_correct: wlp.

Definition trapping_mode_eq trap1 trap2 :=
  RET (match trap1, trap2 with
       | TRAP, TRAP | NOTRAP, NOTRAP => true
       | TRAP, NOTRAP | NOTRAP, TRAP => false
      end).
Lemma trapping_mode_eq_correct t1 t2:
  WHEN trapping_mode_eq t1 t2 ~> b THEN b = true -> t1 = t2.
Hint Resolve trapping_mode_eq_correct: wlp.

Definition load_op_eq (o1 o2: load_op): ?? bool :=
  match o1 with
  | OLoadRRO n1 trap ofs1 =>
    match o2 with
    | OLoadRRO n2 trap2 ofs2 => iandb (phys_eq n1 n2) (iandb (offset_eq ofs1 ofs2) (trapping_mode_eq trap trap2))
    | _ => RET false
    end
  | OLoadRRR n1 trap =>
    match o2 with
    | OLoadRRR n2 trap2 => iandb (phys_eq n1 n2) (trapping_mode_eq trap trap2)
    | _ => RET false
    end
  | OLoadRRRXS n1 trap =>
    match o2 with
    | OLoadRRRXS n2 trap2 => iandb (phys_eq n1 n2) (trapping_mode_eq trap trap2)
    | _ => RET false
    end
  end.

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

Definition store_op_eq (o1 o2: store_op): ?? bool :=
  match o1 with
  | OStoreRRO n1 ofs1 =>
     match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (offset_eq ofs1 ofs2) | _ => RET false end
  | OStoreRRR n1 =>
     match o2 with OStoreRRR n2 => phys_eq n1 n2 | _ => RET false end
  | OStoreRRRXS n1 =>
     match o2 with OStoreRRRXS n2 => phys_eq n1 n2 | _ => RET false end
  end.

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

Definition control_op_eq (c1 c2: control_op): ?? bool :=
  match c1 with
  | Oj_l l1 =>
     match c2 with Oj_l l2 => phys_eq l1 l2 | _ => RET false end
  | Ocb bt1 l1 =>
     match c2 with Ocb bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => RET false end
  | Ocbu bt1 l1 =>
     match c2 with Ocbu bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => RET false end
  | Ojumptable tbl1 =>
     match c2 with Ojumptable tbl2 => phys_eq tbl1 tbl2 | _ => RET false end
  | Odiv =>
     match c2 with Odiv => RET true | _ => RET false end
  | Odivu =>
     match c2 with Odivu => RET true | _ => 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.
Hint Resolve control_op_eq_correct: wlp.
Opaque control_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
  | 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
  | Control i1 =>
    match o2 with Control i2 => control_op_eq i1 i2 | _ => RET false end
  | Allocframe sz1 pos1 =>
    match o2 with Allocframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end
  | Allocframe2 sz1 pos1 =>
    match o2 with Allocframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end
  | Freeframe sz1 pos1 =>
    match o2 with Freeframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end
  | Freeframe2 sz1 pos1 =>
    match o2 with Freeframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end
  | Constant c1 =>
    match o2 with Constant c2 => phys_eq c1 c2 | _ => RET false end
  | Fail =>
    match o2 with Fail => RET true | _ => RET false end
  end.

Theorem op_eq_correct o1 o2:
 WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2.
Hint Resolve op_eq_correct: wlp.
Global Opaque op_eq_correct.

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
  | GPR0 => 1 | GPR1 => 2 | GPR2 => 3 | GPR3 => 4 | GPR4 => 5 | GPR5 => 6 | GPR6 => 7 | GPR7 => 8 | GPR8 => 9 | GPR9 => 10
  | GPR10 => 11 | GPR11 => 12 | GPR12 => 13 | GPR13 => 14 | GPR14 => 15 | GPR15 => 16 | GPR16 => 17 | GPR17 => 18 | GPR18 => 19 | GPR19 => 20
  | GPR20 => 21 | GPR21 => 22 | GPR22 => 23 | GPR23 => 24 | GPR24 => 25 | GPR25 => 26 | GPR26 => 27 | GPR27 => 28 | GPR28 => 29 | GPR29 => 30
  | GPR30 => 31 | GPR31 => 32 | GPR32 => 33 | GPR33 => 34 | GPR34 => 35 | GPR35 => 36 | GPR36 => 37 | GPR37 => 38 | GPR38 => 39 | GPR39 => 40
  | GPR40 => 41 | GPR41 => 42 | GPR42 => 43 | GPR43 => 44 | GPR44 => 45 | GPR45 => 46 | GPR46 => 47 | GPR47 => 48 | GPR48 => 49 | GPR49 => 50
  | GPR50 => 51 | GPR51 => 52 | GPR52 => 53 | GPR53 => 54 | GPR54 => 55 | GPR55 => 56 | GPR56 => 57 | GPR57 => 58 | GPR58 => 59 | GPR59 => 60
  | GPR60 => 61 | GPR61 => 62 | GPR62 => 63 | GPR63 => 64
  end
.

Lemma ireg_to_pos_discr: forall r r', r <> r' -> ireg_to_pos r <> ireg_to_pos r'.

Definition ppos (r: preg) : R.t :=
  match r with
  | RA => 2
  | PC => 3
  | IR ir => 3 + ireg_to_pos ir
  end
.

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

Lemma not_eq_add:
  forall k n n', n <> n' -> k + n <> k + n'.

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

Lemma ppos_pmem_discr: forall r, pmem <> ppos r.


Definition pos_to_ireg (p: R.t) : option gpreg :=
  match p with
  | 1 => Some GPR0 | 2 => Some GPR1 | 3 => Some GPR2 | 4 => Some GPR3 | 5 => Some GPR4 | 6 => Some GPR5 | 7 => Some GPR6 | 8 => Some GPR7 | 9 => Some GPR8 | 10 => Some GPR9
  | 11 => Some GPR10 | 12 => Some GPR11 | 13 => Some GPR12 | 14 => Some GPR13 | 15 => Some GPR14 | 16 => Some GPR15 | 17 => Some GPR16 | 18 => Some GPR17 | 19 => Some GPR18 | 20 => Some GPR19
  | 21 => Some GPR20 | 22 => Some GPR21 | 23 => Some GPR22 | 24 => Some GPR23 | 25 => Some GPR24 | 26 => Some GPR25 | 27 => Some GPR26 | 28 => Some GPR27 | 29 => Some GPR28 | 30 => Some GPR29
  | 31 => Some GPR30 | 32 => Some GPR31 | 33 => Some GPR32 | 34 => Some GPR33 | 35 => Some GPR34 | 36 => Some GPR35 | 37 => Some GPR36 | 38 => Some GPR37 | 39 => Some GPR38 | 40 => Some GPR39
  | 41 => Some GPR40 | 42 => Some GPR41 | 43 => Some GPR42 | 44 => Some GPR43 | 45 => Some GPR44 | 46 => Some GPR45 | 47 => Some GPR46 | 48 => Some GPR47 | 49 => Some GPR48 | 50 => Some GPR49
  | 51 => Some GPR50 | 52 => Some GPR51 | 53 => Some GPR52 | 54 => Some GPR53 | 55 => Some GPR54 | 56 => Some GPR55 | 57 => Some GPR56 | 58 => Some GPR57 | 59 => Some GPR58 | 60 => Some GPR59
  | 61 => Some GPR60 | 62 => Some GPR61 | 63 => Some GPR62 | 64 => Some GPR63
  | _ => None
  end.

Definition inv_ppos (p: R.t) : option preg :=
  match p with
  | 1 => None
  | 2 => Some RA | 3 => Some PC
  | n => match pos_to_ireg (n-3) with
       | None => None
       | Some gpr => Some (IR gpr)
       end
  end.

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


Definition trans_control (ctl: control) : inst :=
  match ctl with
  | Pret => [(#PC, PReg(#RA))]
  | Pcall s => [(#RA, PReg(#PC)); (#PC, Op (Arith (OArithR (Ploadsymbol s Ptrofs.zero))) Enil)]
  | Picall r => [(#RA, PReg(#PC)); (#PC, PReg(#r))]
  | Pgoto s => [(#PC, Op (Arith (OArithR (Ploadsymbol s Ptrofs.zero))) Enil)]
  | Pigoto r => [(#PC, PReg(#r))]
  | Pj_l l => [(#PC, Op (Control (Oj_l l)) (PReg(#PC) @ Enil))]
  | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (PReg(#r) @ PReg(#PC) @ Enil))]
  | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (PReg(#r) @ PReg(#PC) @ Enil))]
  | Pjumptable r labels => [(#PC, Op (Control (Ojumptable labels)) (PReg(#r) @ PReg(#PC) @ Enil));
                            (#GPR62, Op (Constant Vundef) Enil);
                            (#GPR63, Op (Constant Vundef) Enil) ]
  | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]
  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
  | PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)]
  | PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (PReg(#s) @ Enil))]
  | PArithRI32 n d i => [(#d, Op (Arith (OArithRI32 n i)) Enil)]
  | PArithRI64 n d i => [(#d, Op (Arith (OArithRI64 n i)) Enil)]
  | PArithRF32 n d i => [(#d, Op (Arith (OArithRF32 n i)) Enil)]
  | PArithRF64 n d i => [(#d, Op (Arith (OArithRF64 n i)) Enil)]
  | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (PReg(#s1) @ PReg(#s2) @ Enil))]
  | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (PReg(#s) @ Enil))]
  | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (PReg(#s) @ Enil))]
  | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (PReg(#d) @ PReg(#s1) @ PReg(#s2) @ Enil))]
  | PArithARR n d s => [(#d, Op (Arith (OArithARR n)) (PReg(#d) @ PReg(#s) @ Enil))]
  | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (PReg(#d) @ PReg(#s) @ Enil))]
  | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (PReg(#d) @ PReg(#s) @ Enil))]
  end.


Definition trans_basic (b: basic) : inst :=
  match b with
  | PArith ai => trans_arith ai
  | PLoadRRO trap n d a ofs => [(#d, Op (Load (OLoadRRO n trap ofs)) (PReg (#a) @ PReg pmem @ Enil))]
  | PLoadRRR trap n d a ro => [(#d, Op (Load (OLoadRRR n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
  | PLoadRRRXS trap n d a ro => [(#d, Op (Load (OLoadRRRXS n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
  | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))]
  | PLoadQRRO qd a ofs =>
    let (d0, d1) := gpreg_q_expand qd in
      [(#d0, Op (Load (OLoadRRO Pld_a TRAP ofs)) (PReg (#a) @ PReg pmem @ Enil));
       (#d1, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil))]
  | PLoadORRO od a ofs =>
    match gpreg_o_expand od with
    | (d0, d1, d2, d3) =>
        [(#d0, Op (Load (OLoadRRO Pld_a TRAP ofs)) (PReg (#a) @ PReg pmem @ Enil));
         (#d1, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil));
         (#d2, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 16)))) (Old(PReg (#a)) @ PReg pmem @ Enil));
         (#d3, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 24)))) (Old(PReg (#a)) @ PReg pmem @ Enil))]
    end
  | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
  | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
  | PStoreQRRO qs a ofs =>
    let (s0, s1) := gpreg_q_expand qs in
    [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil));
     (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil))]
  | PStoreORRO os a ofs =>
    match gpreg_o_expand os with
    | (s0, s1, s2, s3) =>
      [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil));
       (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil));
       (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (PReg (#s2) @ PReg (#a) @ PReg pmem @ Enil));
       (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (PReg (#s3) @ PReg (#a) @ PReg pmem @ Enil))]
    end
  | Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil);
                           (pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))]
  | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil));
                          (#SP, Op (Freeframe2 sz pos) (PReg (#SP) @ Old (PReg pmem) @ Enil));
                          (#RTMP, Op (Constant Vundef) Enil)]
  | Pget rd ra => match ra with
                  | RA => [(#rd, PReg(#ra))]
                  | _ => [(#rd, Op Fail Enil)]
                  end
  | Pset ra rd => match ra with
                  | RA => [(#ra, PReg(#rd))]
                  | _ => [(#rd, Op Fail Enil)]
                  end
  | Pnop => []
  end.

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

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

Definition trans_block (b: Asmvliw.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.

Theorem trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb.


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

Definition match_states (s: Asmvliw.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: Asmvliw.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'.


Module PChk := ParallelChecks L PosPseudoRegSet.

Definition bblock_para_check (p: Asmvliw.bblock) : bool :=
  PChk.is_parallelizable (trans_block p).

Section SECT_PAR.

Import PChk.

Ltac Simplif :=
  ((rewrite nextblock_inv by eauto with asmgen)
  || (rewrite nextblock_inv1 by eauto with asmgen)
  || (rewrite Pregmap.gss)
  || (rewrite nextblock_pc)
  || (rewrite Pregmap.gso by eauto with asmgen)
  || (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr);
                                    try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto))
  || (rewrite assign_eq)
  ); auto with asmgen.

Ltac Simpl := repeat Simplif.

Arguments Pos.add: simpl never.
Arguments ppos: simpl never.

Variable Ge: genv.

Lemma trans_arith_par_correct ge fn rsr mr sr rsw mw sw rsw' i:
  Ge = Genv ge fn ->
  match_states (State rsr mr) sr ->
  match_states (State rsw mw) sw ->
  parexec_arith_instr ge i rsr rsw = rsw' ->
  exists sw',
     inst_prun Ge (trans_arith i) sw sr sr = Some sw'
  /\ match_states (State rsw' mw) sw'.



Theorem bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw bi:
  Ge = Genv ge fn ->
  match_states (State rsr mr) sr ->
  match_states (State rsw mw) sw ->
  match_outcome (bstep ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr).


Theorem bisimu_par_body:
  forall bdy ge fn rsr mr sr rsw mw sw,
  Ge = Genv ge fn ->
  match_states (State rsr mr) sr ->
  match_states (State rsw mw) sw ->
  match_outcome (parexec_wio_body ge bdy rsr rsw mr mw) (prun_iw Ge (trans_body bdy) sw sr).

Theorem bisimu_par_control ex sz aux ge fn rsr rsw mr mw sr sw:
  Ge = Genv ge fn ->
  match_states (State rsr mr) sr ->
  match_states (State rsw mw) sw ->
  match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) (rsw#PC <- aux) mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr).

Theorem bisimu_par_exit ex sz ge fn rsr rsw mr mw sr sw:
  Ge = Genv ge fn ->
  match_states (State rsr mr) sr ->
  match_states (State rsw mw) sw ->
  match_outcome (estep ge fn ex (Ptrofs.repr sz) rsr rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr).

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

Theorem bisimu_par_wio ge fn rsr mr sr bdy ex sz:
  Ge = Genv ge fn ->
  match_states (State rsr mr) sr ->
  match_outcome (parexec_wio ge fn bdy ex (Ptrofs.repr sz) rsr mr) (prun_iw Ge (trans_block_aux bdy sz ex) sr sr).

Theorem bisimu_par_wio_bblock ge fn rsr mr sr bdy1 bdy2 ex sz:
  Ge = Genv ge fn ->
  match_states (State rsr mr) sr ->
  match_outcome
   match parexec_wio ge fn bdy1 ex (Ptrofs.repr sz) rsr mr with
   | Next rs' m' => parexec_wio_body ge bdy2 rsr rs' mr m'
   | Stuck => Stuck
   end
   (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr).

Lemma trans_body_perserves_permutation bdy1 bdy2:
  Permutation bdy1 bdy2 ->
  Permutation (trans_body bdy1) (trans_body bdy2).

Lemma trans_body_app bdy1: forall bdy2,
   trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2).

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

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

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

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

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

Theorem bisimu rs m b ge fn s:
    Ge = Genv ge fn ->
    match_states (State rs m) s ->
    match_outcome (exec_bblock ge fn b rs m) (exec Ge (trans_block b) s).


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.

Lemma bblock_para_check_correct ge fn bb rs m rs' m':
  Ge = Genv ge fn ->
  exec_bblock ge fn bb rs m = Next rs' m' ->
  bblock_para_check bb = true ->
  det_parexec ge fn bb rs m rs' m'.

End SECT_PAR.

Section SECT_BBLOCK_EQUIV.

Variable Ge: genv.

Local Hint Resolve trans_state_match: core.

Lemma bblock_simu_reduce:
  forall p1 p2 ge fn,
  Ge = Genv ge fn ->
  L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
  Asmblockprops.bblock_simu ge fn p1 p2.


Definition gpreg_name (gpr: gpreg) :=
  match gpr with
  | GPR0 => Str ("GPR0") | GPR1 => Str ("GPR1") | GPR2 => Str ("GPR2") | GPR3 => Str ("GPR3") | GPR4 => Str ("GPR4")
  | GPR5 => Str ("GPR5") | GPR6 => Str ("GPR6") | GPR7 => Str ("GPR7") | GPR8 => Str ("GPR8") | GPR9 => Str ("GPR9")
  | GPR10 => Str ("GPR10") | GPR11 => Str ("GPR11") | GPR12 => Str ("GPR12") | GPR13 => Str ("GPR13") | GPR14 => Str ("GPR14")
  | GPR15 => Str ("GPR15") | GPR16 => Str ("GPR16") | GPR17 => Str ("GPR17") | GPR18 => Str ("GPR18") | GPR19 => Str ("GPR19")
  | GPR20 => Str ("GPR20") | GPR21 => Str ("GPR21") | GPR22 => Str ("GPR22") | GPR23 => Str ("GPR23") | GPR24 => Str ("GPR24")
  | GPR25 => Str ("GPR25") | GPR26 => Str ("GPR26") | GPR27 => Str ("GPR27") | GPR28 => Str ("GPR28") | GPR29 => Str ("GPR29")
  | GPR30 => Str ("GPR30") | GPR31 => Str ("GPR31") | GPR32 => Str ("GPR32") | GPR33 => Str ("GPR33") | GPR34 => Str ("GPR34")
  | GPR35 => Str ("GPR35") | GPR36 => Str ("GPR36") | GPR37 => Str ("GPR37") | GPR38 => Str ("GPR38") | GPR39 => Str ("GPR39")
  | GPR40 => Str ("GPR40") | GPR41 => Str ("GPR41") | GPR42 => Str ("GPR42") | GPR43 => Str ("GPR43") | GPR44 => Str ("GPR44")
  | GPR45 => Str ("GPR45") | GPR46 => Str ("GPR46") | GPR47 => Str ("GPR47") | GPR48 => Str ("GPR48") | GPR49 => Str ("GPR49")
  | GPR50 => Str ("GPR50") | GPR51 => Str ("GPR51") | GPR52 => Str ("GPR52") | GPR53 => Str ("GPR53") | GPR54 => Str ("GPR54")
  | GPR55 => Str ("GPR55") | GPR56 => Str ("GPR56") | GPR57 => Str ("GPR57") | GPR58 => Str ("GPR58") | GPR59 => Str ("GPR59")
  | GPR60 => Str ("GPR60") | GPR61 => Str ("GPR61") | GPR62 => Str ("GPR62") | GPR63 => Str ("GPR63")
  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 RA => RET (Str ("RA"))
         | Some PC => RET (Str ("PC"))
         | Some (IR gpr) => RET (gpreg_name gpr)
         | _ => RET (Str ("UNDEFINED"))
    end.

Definition string_of_name_r (n: arith_name_r): pstring :=
  match n with
  | Ploadsymbol _ _ => "Ploadsymbol"
  end.

Definition string_of_name_rr (n: arith_name_rr): pstring :=
  match n with
    Pmv => "Pmv"
  | Pnegw => "Pnegw"
  | Pnegl => "Pnegl"
  | Pcvtl2w => "Pcvtl2w"
  | Psxwd => "Psxwd"
  | Pzxwd => "Pzxwd"
  | Pextfz _ _ => "Pextfz"
  | Pextfs _ _ => "Pextfs"
  | Pextfzl _ _ => "Pextfzl"
  | Pextfsl _ _ => "Pextfsl"
  | Pfabsd => "Pfabsd"
  | Pfabsw => "Pfabsw"
  | Pfnegd => "Pfnegd"
  | Pfnegw => "Pfnegw"
  | Pfinvw => "Pfinvw"
  | Pfnarrowdw => "Pfnarrowdw"
  | Pfwidenlwd => "Pfwidenlwd"
  | Pfloatwrnsz => "Pfloatwrnsz"
  | Pfloatuwrnsz => "Pfloatuwrnsz"
  | Pfloatudrnsz => "Pfloatudrnsz"
  | Pfloatdrnsz => "Pfloatdrnsz"
  | Pfixedwrzz => "Pfixedwrzz"
  | Pfixeduwrzz => "Pfixeduwrzz"
  | Pfixeddrzz => "Pfixeddrzz"
  | Pfixedudrzz => "Pfixedudrzz"
  | Pfixeddrzz_i32 => "Pfixeddrzz_i32"
  | Pfixedudrzz_i32 => "Pfixedudrzz_i32"
  | Pfixedwrne => "Pfixedwrne"
  | Pfixeduwrne => "Pfixeduwrne"
  | Pfixeddrne => "Pfixeddrne"
  | Pfixedudrne => "Pfixedudrne"
  end.

Definition string_of_name_ri32 (n: arith_name_ri32): pstring :=
  match n with
  | Pmake => "Pmake"
  end.

Definition string_of_name_ri64 (n: arith_name_ri64): pstring :=
  match n with
  | Pmakel => "Pmakel"
  end.

Definition string_of_name_rf32 (n: arith_name_rf32): pstring :=
  match n with
  | Pmakefs => "Pmakefs"
  end.

Definition string_of_name_rf64 (n: arith_name_rf64): pstring :=
  match n with
  | Pmakef => "Pmakef"
  end.

Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
  match n with
  | Pcompw _ => "Pcompw"
  | Pcompl _ => "Pcompl"
  | Pfcompw _ => "Pfcompw"
  | Pfcompl _ => "Pfcompl"
  | Paddw => "Paddw"
  | Paddxw _ => "Paddxw"
  | Psubw => "Psubw"
  | Prevsubxw _ => "Prevsubxw"
  | Pmulw => "Pmulw"
  | Pandw => "Pandw"
  | Pnandw => "Pnandw"
  | Porw => "Porw"
  | Pnorw => "Pnorw"
  | Pxorw => "Pxorw"
  | Pnxorw => "Pnxorw"
  | Pandnw => "Pandnw"
  | Pornw => "Pornw"
  | Psraw => "Psraw"
  | Psrlw => "Psrlw"
  | Psrxw => "Psrxw"
  | Psllw => "Psllw"
  | Paddl => "Paddl"
  | Paddxl _ => "Paddxl"
  | Psubl => "Psubl"
  | Prevsubxl _ => "Prevsubxl"
  | Pandl => "Pandl"
  | Pnandl => "Pnandl"
  | Porl => "Porl"
  | Pnorl => "Pnorl"
  | Pxorl => "Pxorl"
  | Pnxorl => "Pnxorl"
  | Pandnl => "Pandnl"
  | Pornl => "Pornl"
  | Pmull => "Pmull"
  | Pslll => "Pslll"
  | Psrll => "Psrll"
  | Psrxl => "Psrxl"
  | Psral => "Psral"
  | Pfaddd => "Pfaddd"
  | Pfaddw => "Pfaddw"
  | Pfsbfd => "Pfsbfd"
  | Pfsbfw => "Pfsbfw"
  | Pfmuld => "Pfmuld"
  | Pfmulw => "Pfmulw"
  | Pfmind => "Pfmind"
  | Pfminw => "Pfminw"
  | Pfmaxd => "Pfmaxd"
  | Pfmaxw => "Pfmaxw"
  | Pabdw => "Pabdw"
  | Pabdl => "Pabdl"
  end.

Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
  match n with
    Pcompiw _ => "Pcompiw"
  | Paddiw => "Paddiw"
  | Paddxiw _ => "Paddxiw"
  | Prevsubiw => "Prevsubiw"
  | Prevsubxiw _ => "Prevsubxiw"
  | Pmuliw => "Pmuliw"
  | Pandiw => "Pandiw"
  | Pnandiw => "Pnandiw"
  | Poriw => "Poriw"
  | Pnoriw => "Pnoriw"
  | Pxoriw => "Pxoriw"
  | Pnxoriw => "Pnxoriw"
  | Pandniw => "Pandniw"
  | Porniw => "Porniw"
  | Psraiw => "Psraiw"
  | Psrliw => "Psrliw"
  | Psrxiw => "Psrxiw"
  | Pslliw => "Pslliw"
  | Proriw => "Proriw"
  | Psllil => "Psllil"
  | Psrlil => "Psrlil"
  | Psrail => "Psrail"
  | Psrxil => "Psrxil"
  | Pabdiw => "Pabdiw"
  end.

Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
  match n with
    Pcompil _ => "Pcompil"
  | Paddil => "Paddil"
  | Prevsubil => "Prevsubil"
  | Paddxil _ => "Paddxil"
  | Prevsubxil _ => "Prevsubxil"
  | Pmulil => "Pmulil"
  | Pandil => "Pandil"
  | Pnandil => "Pnandil"
  | Poril => "Poril"
  | Pnoril => "Pnoril"
  | Pxoril => "Pxoril"
  | Pnxoril => "Pnxoril"
  | Pandnil => "Pandnil"
  | Pornil => "Pornil"
  | Pabdil => "Pabdil"
  end.

Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
  match n with
  | Pmaddw => "Pmaddw"
  | Pmaddl => "Pmaddl"
  | Pmsubw => "Pmsubw"
  | Pmsubl => "Pmsubl"
  | Pcmove _ => "Pcmove"
  | Pcmoveu _ => "Pcmoveu"
  | Pfmaddfw => "Pfmaddfw"
  | Pfmaddfl => "Pfmaddfl"
  | Pfmsubfw => "Pfmsubfw"
  | Pfmsubfl => "Pfmsubfl"
  end.

Definition string_of_name_arr (n: arith_name_arr): pstring :=
  match n with
  | Pinsf _ _ => "Pinsf"
  | Pinsfl _ _ => "Pinsfl"
  end.

Definition string_of_name_arri32 (n: arith_name_arri32): pstring :=
  match n with
  | Pmaddiw => "Pmaddw"
  | Pcmoveiw _ => "Pcmoveiw"
  | Pcmoveuiw _ => "Pcmoveuiw"
  end.

Definition string_of_name_arri64 (n: arith_name_arri64): pstring :=
  match n with
  | Pmaddil => "Pmaddl"
  | Pcmoveil _ => "Pcmoveil"
  | Pcmoveuil _ => "Pcmoveuil"
  end.

Definition string_of_arith (op: arith_op): pstring :=
  match op with
  | OArithR n => string_of_name_r n
  | OArithRR n => string_of_name_rr n
  | OArithRI32 n _ => string_of_name_ri32 n
  | OArithRI64 n _ => string_of_name_ri64 n
  | OArithRF32 n _ => string_of_name_rf32 n
  | OArithRF64 n _ => string_of_name_rf64 n
  | OArithRRR n => string_of_name_rrr n
  | OArithRRI32 n _ => string_of_name_rri32 n
  | OArithRRI64 n _ => string_of_name_rri64 n
  | OArithARRR n => string_of_name_arrr n
  | OArithARR n => string_of_name_arr n
  | OArithARRI32 n _ => string_of_name_arri32 n
  | OArithARRI64 n _ => string_of_name_arri64 n
  end.

Definition string_of_load_name (n: load_name) : pstring :=
  match n with
    Plb => "Plb"
  | Plbu => "Plbu"
  | Plh => "Plh"
  | Plhu => "Plhu"
  | Plw => "Plw"
  | Plw_a => "Plw_a"
  | Pld => "Pld"
  | Pld_a => "Pld_a"
  | Pfls => "Pfls"
  | Pfld => "Pfld"
  end.

Definition string_of_load (op: load_op): pstring :=
  match op with
  | OLoadRRO n _ _ => string_of_load_name n
  | OLoadRRR n _ => string_of_load_name n
  | OLoadRRRXS n _ => string_of_load_name n
  end.

Definition string_of_store_name (n: store_name) : pstring :=
  match n with
    Psb => "Psb"
  | Psh => "Psh"
  | Psw => "Psw"
  | Psw_a => "Psw_a"
  | Psd => "Psd"
  | Psd_a => "Psd_a"
  | Pfss => "Pfss"
  | Pfsd => "Pfsd"
  end.

Definition string_of_store (op: store_op) : pstring :=
  match op with
  | OStoreRRO n _ => string_of_store_name n
  | OStoreRRR n => string_of_store_name n
  | OStoreRRRXS n => string_of_store_name n
  end.

Definition string_of_control (op: control_op) : pstring :=
  match op with
  | Oj_l _ => "Oj_l"
  | Ocb _ _ => "Ocb"
  | Ocbu _ _ => "Ocbu"
  | Odiv => "Odiv"
  | Odivu => "Odivu"
  | Ojumptable _ => "Ojumptable"
  | OError => "OError"
  | OIncremPC _ => "OIncremPC"
  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 _ _ => RET (Str "Allocframe")
  | Allocframe2 _ _ => RET (Str "Allocframe2")
  | Freeframe _ _ => RET (Str "Freeframe")
  | Freeframe2 _ _ => RET (Str "Freeframe2")
  | Constant _ => RET (Str "Constant")
  | Fail => RET (Str "Fail")
  end.

End SECT_BBLOCK_EQUIV.


Definition is_constant (o: op): bool :=
  match o with
  | Constant _ | OArithR _ | OArithRI32 _ _ | OArithRI64 _ _ | OArithRF32 _ _ | OArithRF64 _ _ => 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: Asmvliw.bblock) : ?? bool :=
  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 bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp.

Theorem bblock_simu_test_correct verb p1 p2 :
  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2.
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: Asmvliw.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 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2.

Definition bblock_simub: Asmvliw.bblock -> Asmvliw.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.