First version of the oracle checker, does not compile yet

1 files changed, 576 insertions, 832 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 1acbdf1e..571e511f 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -5,6 +5,7 @@
 (*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
 (*           David Monniaux     CNRS, VERIMAG                  *)
 (*           Cyril Six          Kalray                         *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
 (*                                                             *)
 (*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
 (*  This file is distributed under the terms of the INRIA      *)
@@ -21,7 +22,6 @@
     Then, the checkers on [Asmblock] and [Asmvliw] are deduced from those of [L].
  *)
 
-   (*
 Require Import AST.
 Require Import Asmblock.
 Require Import Asmblockgenproof0 Asmblockprops.
@@ -35,9 +35,7 @@ Require Import ZArith.
 Require Import Coqlib.
 Require Import ImpSimuTest.
 Require Import Axioms.
-Require Import Parallelizability.
-Require Import Asmvliw Permutation.
-Require Import Chunks.
+Require Import Permutation.
 
 Require Import Lia.
 
@@ -52,7 +50,7 @@ Section IMPPARAM.
 
 Definition env := Genv.t fundef unit.
 
-Inductive genv_wrap := Genv (ge: env) (fn: function).
+Record genv_wrap := { _genv: env; _fn: function; _lk: aarch64_linker }.
 Definition genv := genv_wrap.
 
 Variable Ge: genv.
@@ -65,298 +63,35 @@ Inductive value_wrap :=
 Definition value := value_wrap.
 
 Inductive control_op :=
-  | Oj_l (l: label)
-  | Ocb (bt: btest) (l: label)
-  | Ocbu (bt: btest) (l: label)
-  | Odiv
-  | Odivu
-  | OError
+  (*| Oj_l (l: label)*)
+  | Ob (l: label)
+  (*| Ocb (bt: btest) (l: label)*)
+  (*| Ocbu (bt: btest) (l: label)*)
+  (*| Odiv*)
+  (*| Odivu*)
+  (*| OError*)
   | OIncremPC (sz: Z)
-  | Ojumptable (l: list label)
+  (*| 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)
+  | OArithPPP (n: arith_ppp)
 .
 
-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)
+  (* arithmetic operation *)
+  | Arith (op: arith_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))
+Definition op:=op_wrap.
 
+Definition arith_op_eval (op: arith_op) (l: list value) :=
+  match op, l with
+  | OArithPPP n, [Val v1; Val v2] => Some (Val (arith_eval_ppp n v1 v2))
   | _, _ => None
   end.
 
-Definition exec_incorrect_load trap chunk :=
-  match trap with
-  | TRAP => None
-  | NOTRAP => Some (Val (concrete_default_notrap_load_value chunk))
-  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 chunk
-              | 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 chunk
-  | 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 chunk
-  | 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.
-Proof.
-  destruct chunk; simpl; lia.
-Qed.
-
-Remark size_chunk_small: forall chunk,
-    (size_chunk chunk) <= 8.
-Proof.
-  destruct chunk; simpl; lia.
-Qed.
-
-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'.
-Proof.
-  intros until m2'.
-  intros DISJOINT SMALL1 SMALL2 STORE0 STORE1 STORE0' STORE1'.
-  unfold disjoint_chunks in DISJOINT.
-  destruct vs1 as [v1 | ]; simpl in STORE0, STORE1'; try congruence.
-  destruct vs2 as [v2 | ]; simpl in STORE1, STORE0'; try congruence.
-  destruct va as [base | ]; try congruence.
-  unfold exec_store_deps_offset in *.
-  destruct Ge.
-  unfold eval_offset in *; simpl in *.
-  unfold Mem.storev in *.
-  unfold Val.offset_ptr in *.
-  destruct base as [ | | | | | wblock wpofs] in * ; try congruence.
-  destruct (Mem.store _ _ _ _ _) eqn:E0; try congruence.
-  inv STORE0.
-  destruct (Mem.store (store_chunk n2) _ _ _ _) eqn:E1; try congruence.
-  inv STORE1.
-  destruct (Mem.store (store_chunk n2) m0 _ _ _) eqn:E0'; try congruence.
-  inv STORE0'.
-  destruct (Mem.store _ m1' _ _ _) eqn:E1'; try congruence.
-  inv STORE1'.
-  assert (Some m2 = Some m2').
-  2: congruence.
-  rewrite <- E1.
-  rewrite <- E1'.
-  eapply Mem.store_store_other.
-  2, 3: eassumption.
-
-  right.
-  pose proof (size_chunk_positive (store_chunk n1)).
-  pose proof (size_chunk_positive (store_chunk n2)).
-  pose proof (size_chunk_small (store_chunk n1)).
-  pose proof (size_chunk_small (store_chunk n2)).
-  destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]];
-    unfold Intv.empty in DIS; simpl in DIS.
-  1, 2: lia.
-  pose proof (Ptrofs.unsigned_range ofs1).
-  pose proof (Ptrofs.unsigned_range ofs2).
-  unfold small_offset_threshold in *.
-  destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1;
-    destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2;
-      change Ptrofs.modulus with 18446744073709551616 in *; 
-      lia.
-Qed.
-
-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].
-Proof.
-  intros until m1.
-  intros DISJOINT SMALL1 SMALL2 STORE0.
-  destruct vs as [v | ]; simpl in STORE0; try congruence.
-  destruct va as [base | ]; try congruence.
-  unfold exec_store_deps_offset in *.
-  unfold eval_offset in *; simpl in *.
-  unfold exec_load_deps_offset.
-  unfold Mem.storev, Mem.loadv in *.
-  destruct Ge in *.
-  unfold eval_offset in *.
-  unfold Val.offset_ptr in *.
-  destruct base as [ | | | | | wblock wpofs] in * ; try congruence.
-  destruct (Mem.store _ _ _ _) eqn:E0; try congruence.
-  inv STORE0.
-  assert (
-    (Mem.load (load_chunk n2) m1 wblock
-      (Ptrofs.unsigned (Ptrofs.add wpofs ofs2))) =
-    (Mem.load (load_chunk n2) m0 wblock
-              (Ptrofs.unsigned (Ptrofs.add wpofs ofs2))) ) as LOADS.
-  {
-    eapply Mem.load_store_other.
-    eassumption.
-    right.
-    pose proof (size_chunk_positive (store_chunk n1)).
-    pose proof (size_chunk_positive (load_chunk n2)).
-    pose proof (size_chunk_small (store_chunk n1)).
-    pose proof (size_chunk_small (load_chunk n2)).
-    destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]];
-      unfold Intv.empty in DIS; simpl in DIS.
-    1,2: lia.
-    
-    pose proof (Ptrofs.unsigned_range ofs1).
-    pose proof (Ptrofs.unsigned_range ofs2).
-    unfold small_offset_threshold in *.
-    destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1;
-      destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2;
-        change Ptrofs.modulus with 18446744073709551616 in *; 
-        lia.
-  }
-  destruct (Mem.load _ m1 _ _) in *; destruct (Mem.load _ m0 _ _) in *; congruence.
-Qed.
-
 Definition goto_label_deps (f: function) (lbl: label) (vpc: val) :=
   match label_pos lbl 0 (fn_blocks f) with
   | None => None
@@ -367,133 +102,49 @@ Definition goto_label_deps (f: function) (lbl: label) (vpc: val) :=
       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
+  let (ge, fn, lk) := 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_cmpu_bool c v (Vint (Int.repr 0)))
-    | (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_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
+  | Ob lbl, [Val vpc] => goto_label_deps fn lbl vpc
   | 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
+Definition op_eval (op: op) (l:list value) :=
+  match op, l with
+  | Arith op, l => arith_op_eval op 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
+  (*| _, _ => 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
+  | OArithPPP n1 =>
+      match o2 with OArithPPP 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).
@@ -506,104 +157,24 @@ Qed.
 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.
-Proof.
-  wlp_simplify.
-  pose (Ptrofs.eq_spec ofs1 ofs2).
-  rewrite H in *.
-  trivial.
-Qed.
-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.
-Proof.
-  wlp_simplify.
-  destruct t1; destruct t2; trivial; discriminate.
-Qed.
-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.
-Proof.
-  destruct o1, o2; wlp_simplify; try discriminate.
-  { f_equal.
-    destruct trap, trap0; simpl in *; trivial; discriminate.
-    pose (Ptrofs.eq_spec ofs ofs0).
-    rewrite H in *. trivial. }
-  all: destruct trap, trap0; simpl in *; trivial; discriminate.
-Qed.
-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.
-Proof.
-  destruct o1, o2; wlp_simplify; try discriminate.
-  - f_equal. pose (Ptrofs.eq_spec ofs ofs0).
-    rewrite H in *. trivial.
-  - congruence.
-  - congruence.
-Qed.
-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
+  | Ob lbl1 =>
+     match c2 with Ob lbl2 => phys_eq lbl1 lbl2 | _ => 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
+      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:
@@ -618,33 +189,15 @@ 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: 
+Lemma op_eq_correct o1 o2: 
  WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2.
 Proof.
-  destruct o1, o2; wlp_simplify; try rewrite Z.eqb_eq in * |- ; try congruence.
+  destruct o1, o2; wlp_simplify; congruence.
 Qed.
-Hint Resolve op_eq_correct: wlp.
-Global Opaque op_eq_correct.
 
 End IMPPARAM.
 
@@ -671,13 +224,19 @@ 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
+  | X0 => 8 | X1 => 9 | X2 => 10 | X3 => 11 | X4 => 12 | X5 => 13 | X6 => 14 | X7 => 15
+  | X8 => 16 | X9 => 17 | X10 => 18 | X11 => 19 | X12 => 20 | X13 => 21 | X14 => 22 | X15 => 23
+  | X16 => 24 | X17 => 25 | X18 => 26 | X19 => 27 | X20 => 28 | X21 => 29 | X22 => 30 | X23 => 31
+  | X24 => 32 | X25 => 33 | X26 => 34 | X27 => 35 | X28 => 36 | X29 => 37 | X30 => 38
+  end
+.
+
+Definition freg_to_pos (fr: freg) : R.t :=
+  match fr with
+  | D0 => 39 | D1 => 40 | D2 => 41 | D3 => 42 | D4 => 43 | D5 => 44 | D6 => 45 | D7 => 46
+  | D8 => 47 | D9 => 48 | D10 => 49 | D11 => 50 | D12 => 51 | D13 => 52 | D14 => 53 | D15 => 54
+  | D16 => 55 | D17 => 56 | D18 => 57 | D19 => 58 | D20 => 59 | D21 => 60 | D22 => 61 | D23 => 62
+  | D24 => 63 | D25 => 64 | D26 => 65 | D27 => 66 | D28 => 67 | D29 => 68 | D30 => 69 | D31 => 70
   end
 .
 
@@ -686,15 +245,36 @@ Proof.
   destruct r; destruct r'; try contradiction; discriminate.
 Qed.
 
+Lemma freg_to_pos_discr: forall r r', r <> r' -> freg_to_pos r <> freg_to_pos r'.
+Proof.
+  destruct r; destruct r'; try contradiction; discriminate.
+Qed.
+
+(*Lemma creg_to_pos_discr: forall r r', r <> r' -> freg_to_pos r <> freg_to_pos r'.*)
+(*Proof.*)
+  (*destruct r; destruct r'; try contradiction; discriminate.*)
+(*Qed.*)
+
 Definition ppos (r: preg) : R.t :=
   match r with
-  | RA => 2
-  | PC => 3
-  | IR ir => 3 + ireg_to_pos ir
+  | CR c => match c with
+            | CN => 2
+            | CZ => 3
+            | CC => 4
+            | CV => 5
+            end
+  | PC => 6
+  | DR d => match d with
+            | IR i => match i with
+                      | XSP => 7
+                      | RR1 ir => ireg_to_pos ir
+                      end
+            | FR fr => freg_to_pos fr
+            end
   end
 .
 
-Notation "# r" := (ppos r) (at level 100, right associativity).
+Notation "# r" := (ppos r) (at level 100, right associativity). 
 
 Lemma not_eq_add:
   forall k n n', n <> n' -> k + n <> k + n'.
@@ -704,49 +284,64 @@ Qed.
 
 Lemma ppos_discr: forall r r', r <> r' -> ppos r <> ppos r'.
 Proof.
-  destruct r; destruct r'.
+  destruct r as [dr|cr|]; destruct r' as [dr'|cr'|];
+  try destruct dr as [ir|fr]; try destruct dr' as [ir'|fr'];
+  try destruct ir as [irr|]; try destruct ir' as [irr'|].
   all: try discriminate; try contradiction.
-  - intros. apply not_eq_add. apply ireg_to_pos_discr. congruence.
-  - intros. unfold ppos. cutrewrite (3 + ireg_to_pos g = (1 + ireg_to_pos g) + 2). apply Pos.add_no_neutral.
-    apply eq_sym. rewrite Pos.add_comm. rewrite Pos.add_assoc. reflexivity.
-  - intros. unfold ppos. rewrite Pos.add_comm. apply Pos.add_no_neutral.
-  - intros. unfold ppos. apply not_eq_sym.
-    cutrewrite (3 + ireg_to_pos g = (1 + ireg_to_pos g) + 2). apply Pos.add_no_neutral.
-    apply eq_sym. rewrite Pos.add_comm. rewrite Pos.add_assoc. reflexivity.
-  - intros. unfold ppos. apply not_eq_sym. rewrite Pos.add_comm. apply Pos.add_no_neutral.
+  1: intros; unfold ppos; apply ireg_to_pos_discr; congruence.
+  1,2,11,18: intros; unfold ppos; try destruct irr; try destruct irr'; discriminate.
+  1,3: intros; unfold ppos; try destruct irr; try destruct fr; try destruct irr'; try destruct fr'; discriminate.
+  1,2,7,13: intros; unfold ppos; try destruct fr; try destruct fr'; discriminate.
+  1: intros; unfold ppos; apply freg_to_pos_discr; congruence.
+  1,4: intros; unfold ppos; try destruct irr; try destruct irr'; try destruct cr; try destruct cr'; discriminate.
+  2,4: intros; unfold ppos; try destruct fr; try destruct fr'; try destruct cr; try destruct cr'; discriminate.
+  1,2,4,5: intros; unfold ppos; try destruct cr; try destruct cr'; discriminate.
+  1: intros; unfold ppos; try destruct cr; try destruct cr'; congruence.
 Qed.
 
 Lemma ppos_pmem_discr: forall r, pmem <> ppos r.
 Proof.
-  intros. destruct r.
-  - unfold ppos. unfold pmem. apply not_eq_sym. rewrite Pos.add_comm. cutrewrite (3 = 2 + 1). rewrite Pos.add_assoc. apply Pos.add_no_neutral.
-    reflexivity.
-  - unfold ppos. unfold pmem. discriminate.
-  - unfold ppos. unfold pmem. discriminate.
+  intros. destruct r as [dr|cr|].
+  - destruct dr as [ir|fr]; try destruct ir as [irr|]; try destruct irr; try destruct fr;
+    unfold ppos; unfold pmem; discriminate.
+  - unfold ppos; unfold pmem; destruct cr; discriminate.
+  - unfold ppos; unfold pmem; discriminate.
 Qed.
 
 (** Inversion functions, used for debug traces *)
 
-Definition pos_to_ireg (p: R.t) : option gpreg :=
+Definition pos_to_ireg (p: R.t) : option ireg :=
   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
+  | 8 => Some (X0) | 9 => Some (X1) | 10 => Some (X2) | 11 => Some (X3) | 12 => Some (X4) | 13 => Some (X5) | 14 => Some (X6) | 15 => Some (X7)
+  | 16 => Some (X8) | 17 => Some (X9) | 18 => Some (X10) | 19 => Some (X11) | 20 => Some (X12) | 21 => Some (X13) | 22 => Some (X14) | 23 => Some (X15)
+  | 24 => Some (X16) | 25 => Some (X17) | 26 => Some (X18) | 27 => Some (X19) | 28 => Some (X20) | 29 => Some (X21) | 30 => Some (X22) | 31 => Some (X23)
+  | 32 => Some (X24) | 33 => Some (X25) | 34 => Some (X26) | 35 => Some (X27) | 36 => Some (X28) | 37 => Some (X29) | 38 => Some (X30) | _ => None
+  end.
+
+Definition pos_to_freg (p: R.t) : option freg :=
+  match p with
+  | 39 => Some(D0) | 40 => Some(D1) | 41 => Some(D2) | 42 => Some(D3) | 43 => Some(D4) | 44 => Some(D5) | 45 => Some(D6) | 46 => Some(D7)
+  | 47 => Some(D8) | 48 => Some(D9) | 49 => Some(D10) | 50 => Some(D11) | 51 => Some(D12) | 52 => Some(D13) | 53 => Some(D14) | 54 => Some(D15)
+  | 55 => Some(D16) | 56 => Some(D17) | 57 => Some(D18) | 58 => Some(D19) | 59 => Some(D20) | 60 => Some(D21) | 61 => Some(D22) | 62 => Some(D23)
+  | 63 => Some(D24) | 64 => Some(D25) | 65 => Some(D26) | 66 => Some(D27) | 67 => Some(D28) | 68 => Some(D29) | 69 => Some(D30) | 70 => Some(D31) | _ => None
   end.
 
 Definition inv_ppos (p: R.t) : option preg :=
   match p with
   | 1 => None
-  | 2 => Some RA | 3 => Some PC
-  | n => match pos_to_ireg (n-3) with
-       | None => None
-       | Some gpr => Some (IR gpr)
-       end
+  | 2 => Some (CR CN)
+  | 3 => Some (CR CZ)
+  | 4 => Some (CR CC)
+  | 5 => Some (CR CV)
+  | 6 => Some (PC)
+  | 7 => Some (DR (IR XSP))
+  | n => match pos_to_ireg n with
+         | None => match pos_to_freg n with
+                   | None => None
+                   | Some fr => Some (DR (FR fr))
+                   end
+         | Some ir => Some (DR (IR ir))
+         end
   end.
 
 Notation "a @ b" := (Econs a b) (at level 102, right associativity).
@@ -755,18 +350,14 @@ 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)]
+  | Pb lbl => [(#PC, Op (Control (Ob lbl)) (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 :=
@@ -778,69 +369,66 @@ Definition trans_exit (ex: option control) : L.inst :=
 
 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))]
+  | PArithPPP n rd r1 r2 => [(#rd, Op(Arith (OArithPPP n)) (PReg(#r1) @ PReg(#r2) @ Enil))]
+  | _ => []
+  (*| 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))]*)
   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 => []
+  | _ => []
+  (*| 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 :=
@@ -851,38 +439,38 @@ Fixpoint trans_body (b: list basic) : list L.inst :=
 
 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 :=
+Definition trans_block (b: Asmblock.bblock) : L.bblock :=
   trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil).
 
-Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb.
-Proof.
-  intros. destruct bb as [hd bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.
-Qed.
+(*Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb.*)
+(*Proof.*)
+  (*intros. destruct bb as [hd bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.*)
+(*Qed.*)
 
-Theorem trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb.
-Proof.
-  intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.
-Qed.
+(*Theorem trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb.*)
+(*Proof.*)
+  (*intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.*)
+(*Qed.*)
 
 (** Lemmas on the translation *)
 
 Definition state := L.mem.
 Definition exec := L.run.
 
-Definition match_states (s: Asmvliw.state) (s': state) :=
+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
+  | Some n => exists s', s=Some s' /\ match_states n s'
+  | None => s=None
   end.
  
 Notation "a <[ b <- c ]>" := (assign a b c) (at level 102, right associativity).
 
-Definition trans_state (s: Asmvliw.state) : state :=
+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
@@ -896,22 +484,114 @@ Proof.
   intros. congruence.
 Qed.
 
+(*Lemma inv_ppos_from_ireg: forall (ir: ireg),*)
+  (*exists x,*)
+  (*inv_ppos (x) = Some (DR (IR ir)).*)
+(*Proof.*)
+  (*intros. unfold inv_ppos.*)
+  (*eexists (ireg_to_pos ir). destruct ir; simpl; reflexivity.*)
+(*Qed.*)
+
+Lemma ireg_pos_ppos: forall (sr: state) r,
+  sr (ireg_to_pos r) = sr (# r).
+Proof.
+  intros. simpl. reflexivity.
+Qed.
+
+Lemma freg_pos_ppos: forall (sr: state) r,
+  sr (freg_to_pos r) = sr (# r).
+Proof.
+  intros. simpl. reflexivity.
+Qed.
+
+Lemma ireg_not_pmem: forall r,
+  ireg_to_pos r <> pmem.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
+Lemma freg_not_pmem: forall r,
+  freg_to_pos r <> pmem.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
+Lemma sr_ireg_update_both: forall sr rsr r1 rr v
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  (sr <[ ireg_to_pos r1 <- Val (v) ]>) (#rr) =
+  Val (rsr # r1 <- v rr).
+Proof.
+  intros. unfold assign.
+  destruct (PregEq.eq r1 rr); subst.
+  - rewrite Pregmap.gss. simpl. destruct r1; simpl; reflexivity.
+  - rewrite Pregmap.gso; eauto.
+    destruct rr; try congruence.
+    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; destruct r1; simpl; try congruence.
+    + destruct c; destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
+    + destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
+Qed.
+
+Lemma sr_freg_update_both: forall sr rsr r1 rr v
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  (sr <[ freg_to_pos r1 <- Val (v) ]>) (#rr) =
+  Val (rsr # r1 <- v rr).
+Proof.
+  intros. unfold assign.
+  destruct (PregEq.eq r1 rr); subst.
+  - rewrite Pregmap.gss. simpl. destruct r1; simpl; reflexivity.
+  - rewrite Pregmap.gso; eauto.
+    destruct rr; try congruence.
+    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; destruct r1; simpl; try congruence.
+    + destruct c; destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
+    + destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
+Qed.
+
+Lemma sr_xsp_update_both: forall sr rsr rr v
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  (sr <[ #XSP <- Val (v) ]>) (#rr) =
+  Val (rsr # XSP <- v rr).
+Proof.
+  intros. unfold assign.
+  destruct (PregEq.eq XSP rr); subst.
+  - rewrite Pregmap.gss. simpl. reflexivity.
+  - rewrite Pregmap.gso; eauto.
+    destruct rr; try congruence.
+    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence.
+    + destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
+    + simpl; try rewrite <- HEQV; unfold ppos; try congruence.
+Qed.
+
+Lemma sr_update_overwrite: forall sr pos v1 v2,
+  (sr <[ pos <- v1 ]>) <[ pos <- v2 ]> = (sr <[ pos <- v2 ]>).
+Proof.
+  intros.
+  unfold assign. apply functional_extensionality; intros x.
+  destruct (R.eq_dec pos x); reflexivity.
+Qed.
+
+Lemma sr_gss: forall sr pos v,
+  (sr <[ pos <- v ]>) pos = v.
+Proof.
+  intros. unfold assign.
+  destruct (R.eq_dec pos pos) eqn:REQ; try reflexivity; try congruence.
+Qed.
+
 (** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *)
 
-Module PChk := ParallelChecks L PosPseudoRegSet.
+(*Module PChk := ParallelChecks L PosPseudoRegSet.*)
 
-Definition bblock_para_check (p: Asmvliw.bblock) : bool :=
-  PChk.is_parallelizable (trans_block p).
+(*Definition bblock_para_check (p: Asmvliw.bblock) : bool :=*)
+  (*PChk.is_parallelizable (trans_block p).*)
 
-Section SECT_PAR.
+(*Section SECT_PAR.*)
 
-Import PChk.
+(*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 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))
@@ -920,22 +600,48 @@ Ltac Simplif :=
 
 Ltac Simpl := repeat Simplif.
 
-Arguments Pos.add: simpl never.
-Arguments ppos: simpl never.
+(*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 ->
+(*Lemma trans_arith_par_correct o rs m m' old:*)
+Lemma trans_arith_correct rsr mr sr rsw' old i:
+  (*Ge = Genv ge fn ->*)
+  (*match_states (State rs m) m' ->*)
+  (*exists em,*)
+  (*L.inst_run Ge (trans_arith o) m' old = Some em /\ match_states .*)
   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'.
+  (*match_states (State rsw mw) sw ->*)
+  exec_arith_instr Ge.(_lk) i rsr = rsw' ->
+  exists sw,
+     inst_run Ge (trans_arith i) sr old = Some sw
+  /\ match_states (State rsw' mr) sw.
 Proof.
-  intros GENV MSR MSW PARARITH. subst. inv MSR. inv MSW.
-  unfold parexec_arith_instr. destruct i.
+  induction i.
+  3: { intros MS EARITH. subst. inv MS.
+       unfold exec_arith_instr.
+       (*eexists; split; [| split]. *)
+       - simpl. destruct r1 eqn:EQR1; subst; try destruct i0; simpl;
+         destruct r2 eqn:EQR2; subst; try destruct i0; simpl;
+         (*destruct (sr 8).*) destruct rd eqn:EQRD; subst; try destruct i0; simpl;
+         try erewrite !ireg_pos_ppos;
+         try erewrite !freg_pos_ppos;
+         try replace (7) with (ppos XSP) by eauto;
+         try rewrite !H0;
+         try (eexists; split; [| split]); eauto;
+         try (rewrite <- H; rewrite assign_diff;
+              try reflexivity; try apply ireg_not_pmem;
+              try apply freg_not_pmem).
+         all: intros rr; destruct rr as [dr|cr|]; try destruct dr as [ir|fr]; try destruct ir as [irr|];
+         try destruct irr; try destruct fr;
+         try eapply sr_ireg_update_both; eauto;
+         try eapply sr_freg_update_both; eauto;
+         try eapply sr_xsp_update_both; eauto.
+         }
+  all:admit.
+
+  (*
 (* Ploadsymbol *)
   - destruct i. eexists; split; [| split].
     * simpl. reflexivity.
@@ -1013,16 +719,12 @@ Proof.
     * simpl. rewrite (H0 rd).  rewrite (H0 rs). reflexivity.
     * Simpl.
     * intros rr; destruct rr; Simpl.
-      destruct (ireg_eq g rd); subst; Simpl.
-Qed.
-
+      destruct (ireg_eq g rd); subst; Simpl.*)
+Admitted.
 
-
-Theorem bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw bi:
-  Ge = Genv ge fn ->
+Theorem bisimu_basic rsr mr sr bi:
   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).
+  match_outcome (exec_basic Ge.(_lk) Ge.(_genv) bi rsr mr) (inst_run Ge (trans_basic bi) sr sr).
 Proof.
 
 (* a little tactic to automate reasoning on preg_eq *)
@@ -1032,10 +734,11 @@ Local Ltac preg_eq_discr r rd :=
   rewrite (assign_diff _ (#rd) (#r) _); auto;
   rewrite Pregmap.gso; auto.
 
-  intros GENV MSR MSW; inversion MSR as (H & H0); inversion MSW as (H1 & H2).
+  intros MS; inversion MS as (H & H0).
   destruct bi; simpl.
 (* Arith *)
-  - exploit trans_arith_par_correct. 5: eauto. all: eauto.
+  exploit trans_arith_correct; eauto.
+    all: admit. (*
 (* Load *)
   - destruct i.
     (* Load Offset *)
@@ -1166,35 +869,48 @@ Local Ltac preg_eq_discr r rd :=
   - destruct rd eqn:rdeq; simpl; auto.
     eexists. repeat split. Simpl. intros rr; destruct rr; Simpl.
 (* Pnop *)
-  - eexists. repeat split; assumption.
-Qed.
-
+  - eexists. repeat split; assumption.*)
+Admitted.
 
-Theorem bisimu_par_body:
-  forall bdy ge fn rsr mr sr rsw mw sw,
-  Ge = Genv ge fn ->
+Theorem bisimu_body:
+  forall bdy rsr mr sr,
   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).
+  match_outcome (exec_body Ge.(_lk) Ge.(_genv) bdy rsr mr) (exec Ge (trans_body bdy) sr).
 Proof.
   induction bdy as [|i bdy]; simpl; eauto. 
   intros.
-  exploit (bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw i); eauto.
-  destruct (bstep _ _ _ _ _ _); simpl.
-  - intros (s' & X1 & X2). rewrite X1; simpl; eauto.
+  exploit (bisimu_basic rsr mr sr i); eauto.
+  destruct (exec_basic _ _ _ _ _); simpl.
+  - intros (s' & X1 & X2).
+    rewrite X1; simpl; eauto. eapply IHbdy; eauto; simpl.
+    unfold match_states in *. destruct s. unfold Asm._m. eauto.
   - intros X; rewrite X; simpl; auto.
 Qed.
 
-Theorem bisimu_par_control ex sz aux ge fn rsr rsw mr mw sr sw:
-  Ge = Genv ge fn ->
+Theorem bisimu_control ex sz rsr mr sr old:
   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).
+  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 old).
 Proof.
-  intros GENV MSR MSW; unfold estep.
-  simpl in *. inv MSR. inv MSW.
+  intros MS.
+  simpl in *. inv MS.
   destruct ex.
-  - destruct c; destruct i; try discriminate; simpl.
+  1: { replace (6) with (#PC) by auto. rewrite (H0 PC). simpl.
+    unfold goto_label, control_eval. destruct Ge.
+    unfold goto_label_deps. destruct (label_pos _ _ _); auto.
+    + unfold incrPC. rewrite Pregmap.gss; eauto. destruct (Val.offset_ptr _ _); auto;
+      try (rewrite sr_gss; unfold Stuck; reflexivity).
+      simpl. eexists; split; split.
+      * rewrite sr_update_overwrite. unfold pmem, assign in *. simpl. rewrite H; reflexivity.
+      * intros. rewrite sr_update_overwrite. unfold Pregmap.set, assign.
+        destruct r as [dr|cr|]; try destruct dr as [ir|fr]; try destruct ir as [irr|];
+        try destruct irr; try destruct fr; try destruct cr; simpl; try rewrite <- H0; eauto.
+    + rewrite sr_gss; reflexivity. }
+  all: admit.
+
+
+
+
+  (*    destruct c; destruct i; try discriminate; simpl.
     all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold incrPC; Simpl).
 
     (* Pjumptable *)
@@ -1241,55 +957,84 @@ Proof.
 
   - simpl in *. rewrite (H0 PC). eexists; split; try split; Simpl.
     intros rr; destruct rr; unfold incrPC; Simpl.
-Qed.
+Qed.*)
+Admitted.
 
-Theorem bisimu_par_exit ex sz ge fn rsr rsw mr mw sr sw:
-  Ge = Genv ge fn ->
+Theorem bisimu_exit ex sz rsr mr sr old:
   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).
+  match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit (Some (PCtlFlow ex)))) sr old).
 Proof.
   intros; unfold estep.
-  exploit (bisimu_par_control ex sz rsw#PC ge fn rsr rsw mr mw sr sw); eauto.
-  cutrewrite (rsw # PC <- (rsw PC) = rsw); auto.
-  apply extensionality. intros; destruct x; simpl; auto.
+  exploit (bisimu_control ex sz rsr mr sr sr); eauto.
+  intros. destruct ex; simpl; auto.
 Qed.
 
 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 ->
+Theorem bisimu rsr mr sr bdy ex sz:
   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).
+  match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy rsr mr) (run Ge (trans_block_aux bdy sz (Some (PCtlFlow ex))) sr).
 Proof.
-  intros GENV MSR. unfold parexec_wio, trans_block_aux.
-  exploit (bisimu_par_body bdy ge fn rsr mr sr rsr mr sr); eauto.
-  destruct (parexec_wio_body _ _ _ _ _ _); simpl.
-  - intros (s' & X1 & X2).
-    erewrite prun_iw_app_Some; eauto.
-    exploit (bisimu_par_exit ex sz ge fn rsr rs mr m sr s'); eauto.
-    subst Ge; simpl. destruct MSR as (Y1 & Y2). erewrite Y2; simpl.
-    destruct (inst_prun _ _ _ _ _); simpl; auto.
-  - intros X; erewrite prun_iw_app_None; eauto.
+  intros MS. unfold bbstep, trans_block_aux.
+  exploit (bisimu_body bdy rsr mr sr); eauto.
+  destruct (exec_body _ _ _ _ _); simpl.
+  - unfold match_states in *. intros (s' & X1 & X2). destruct s.
+    erewrite run_app_Some; eauto.
+    exploit (bisimu_exit ex sz _rs _m s' s'); eauto.
+    destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).
+    replace (6) with (#PC) by auto. erewrite !X3; simpl.
+    destruct (inst_run _ _ _ _); simpl; auto.
+  - intros X; erewrite run_app_None; eauto.
 Qed.
 
-Theorem bisimu_par_wio_bblock ge fn rsr mr sr bdy1 bdy2 ex sz:
-  Ge = Genv ge fn ->
+(* TODO We should use this version, but our current definitions
+does not match
+Theorem bisimu rsr mr b sr ex sz:
+    match_states (State rsr mr) sr -> 
+    match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) (body b) rsr mr) (exec Ge (trans_block b) sr).
+Proof.
+
+  intros MS. unfold bbstep.
+  exploit (bisimu_body (body b) rsr mr sr); eauto.
+  unfold exec, trans_block; simpl.
+  destruct (exec_body _ _ _ _); simpl.
+  - unfold match_states in *. intros (s' & X1 & X2). destruct s.
+    erewrite run_app_Some; eauto.
+    exploit (bisimu_exit ex sz _rs _m s' s'); eauto.
+    destruct Ge; simpl. destruct X2 as (X2 & X3). destruct MS as (Y1 & Y2).
+    replace (6) with (#PC) by auto. erewrite X3; simpl.
+    unfold trans_exit.
+    destruct (inst_run _ _ _); simpl; auto.
+  - intros X; erewrite run_app_None; eauto.
+
+  intros MS. unfold bbstep, trans_block.
+  exploit (bisimu_body (body b) rsr mr sr); eauto.
+  destruct (exec_body _ _ _ _ _); simpl.
+  - unfold match_states in *. intros (s' & X1 & X2). destruct s.
+    erewrite run_app_Some; eauto.
+    exploit (bisimu_exit ex sz _rs _m s' s'); eauto.
+    destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).
+    replace (6) with (#PC) by auto. erewrite !X3; simpl.
+    destruct (inst_run _ _ _ _); simpl; auto.
+  - intros X; erewrite run_app_None; eauto.
+Qed.*)
+
+Theorem bisimu_bblock rsr mr sr bdy1 bdy2 ex sz:
   match_states (State rsr mr) sr ->
   match_outcome 
-   match parexec_wio ge fn bdy1 ex (Ptrofs.repr sz) rsr mr with
-   | Next rs' m' => parexec_wio_body ge bdy2 rsr rs' mr m'
+   match bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy1 rsr mr with
+   | Some (State rs' m') => exec_body Ge.(_lk) Ge.(_genv) bdy2 rs' m'
    | Stuck => Stuck
    end
-   (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr).
+   (run Ge ((trans_block_aux bdy1 sz (Some (PCtlFlow (ex))))++(trans_body bdy2)) sr).
 Proof.
   intros.
-  exploit (bisimu_par_wio ge fn rsr mr sr bdy1 ex sz); eauto.
-  destruct (parexec_wio _ _ _ _ _ _); simpl.
+  exploit (bisimu rsr mr sr bdy1 ex sz); eauto.
+  destruct (bbstep _ _ _ _ _ _); simpl.
   - intros (s' & X1 & X2).
-    erewrite prun_iw_app_Some; eauto.
-    eapply bisimu_par_body; eauto.
-  - intros; erewrite prun_iw_app_None; eauto.
+    erewrite run_app_Some; eauto. destruct s.
+    eapply bisimu_body; eauto.
+  - intros; erewrite run_app_None; eauto.
 Qed.
 
 Lemma trans_body_perserves_permutation bdy1 bdy2:
@@ -1319,85 +1064,83 @@ Proof.
     apply Permutation_app_comm.
 Qed.
 
-Theorem bisimu_par rs1 m1 s1' b ge fn o2:
-    Ge = Genv ge fn ->
-    match_states (State rs1 m1) s1' -> 
-    parexec_bblock ge fn b rs1 m1 o2 ->
-  exists o2',
-     prun Ge (trans_block b) s1' o2'
-  /\ match_outcome o2 o2'.
-Proof.
-  intros GENV MS PAREXEC.
-  inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO).
-  exploit trans_block_perserves_permutation; eauto.
-  intros Perm.
-  exploit (bisimu_par_wio_bblock ge fn rs1 m1 s1' bdy1 bdy2 (exit b) (size b)); eauto.
-  rewrite <- WIO. clear WIO.
-  intros H; eexists; split. 2: eapply H.
-  unfold prun; eexists; split; eauto. 
-  destruct (prun_iw _ _ _ _); simpl; eauto.
-Qed.
+(*Theorem bisimu_par rs1 m1 s1' b ge fn o2:*)
+    (*Ge = Genv ge fn ->*)
+    (*match_states (State rs1 m1) s1' -> *)
+    (*parexec_bblock ge fn b rs1 m1 o2 ->*)
+  (*exists o2',*)
+     (*prun Ge (trans_block b) s1' o2'*)
+  (*/\ match_outcome o2 o2'.*)
+(*Proof.*)
+  (*intros GENV MS PAREXEC.*)
+  (*inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO).*)
+  (*exploit trans_block_perserves_permutation; eauto.*)
+  (*intros Perm.*)
+  (*exploit (bisimu_par_wio_bblock ge fn rs1 m1 s1' bdy1 bdy2 (exit b) (size b)); eauto.*)
+  (*rewrite <- WIO. clear WIO.*)
+  (*intros H; eexists; split. 2: eapply H.*)
+  (*unfold prun; eexists; split; eauto. *)
+  (*destruct (prun_iw _ _ _ _); simpl; eauto.*)
+(*Qed.*)
 
 (** sequential execution *)
-Theorem bisimu_basic ge fn bi rs m s:
-  Ge = Genv ge fn ->
-  match_states (State rs m) s ->
-  match_outcome (exec_basic_instr ge bi rs m) (inst_run Ge (trans_basic bi) s s).
-Proof.
-  intros; unfold exec_basic_instr. rewrite inst_run_prun.
-  eapply bisimu_par_wio_basic; eauto.
-Qed.
-
-Lemma bisimu_body:
-  forall bdy ge fn rs m s,
-  Ge = Genv ge fn ->
-  match_states (State rs m) s ->
-  match_outcome (exec_body ge bdy rs m) (exec Ge (trans_body bdy) s).
-Proof.
-  induction bdy as [|i bdy]; simpl; eauto. 
-  intros.
-  exploit (bisimu_basic ge fn i rs m s); eauto.
-  destruct (exec_basic_instr _ _ _ _); simpl.
-  - intros (s' & X1 & X2). rewrite X1; simpl; eauto.
-  - intros X; rewrite X; simpl; auto.
-Qed.
-
-Theorem bisimu_exit ge fn b rs m s:
-  Ge = Genv ge fn ->
-  match_states (State rs m) s ->
-  match_outcome (exec_control ge fn (exit b) (nextblock b rs) m) (inst_run Ge (trans_pcincr (size b) (trans_exit (exit b))) s s).
-Proof.
-  intros; unfold exec_control, nextblock. rewrite inst_run_prun. 
-  apply (bisimu_par_control (exit b) (size b) (Val.offset_ptr (rs PC) (Ptrofs.repr (size b))) ge fn rs rs m m s s); auto.
-Qed.
-
-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).
-Proof.
-  intros GENV MS. unfold exec_bblock.
-  exploit (bisimu_body (body b) ge fn rs m s); eauto.
-  unfold exec, trans_block; simpl.
-  destruct (exec_body _ _ _ _); simpl.
-  - intros (s' & X1 & X2).
-    erewrite run_app_Some; eauto.
-    exploit (bisimu_exit ge fn b rs0 m0 s'); eauto.
-    subst Ge; simpl. destruct X2 as (Y1 & Y2). erewrite Y2; simpl.
-    destruct (inst_run _ _ _); simpl; auto.
-  - intros X; erewrite run_app_None; eauto.
-Qed.
-
+(*Theorem bisimu_basic ge fn bi rs m s:*)
+  (*Ge = Genv ge fn ->*)
+  (*match_states (State rs m) s ->*)
+  (*match_outcome (exec_basic_instr ge bi rs m) (inst_run Ge (trans_basic bi) s s).*)
+(*Proof.*)
+  (*intros; unfold exec_basic_instr. rewrite inst_run_prun.*)
+  (*eapply bisimu_par_wio_basic; eauto.*)
+(*Qed.*)
+
+(*Lemma bisimu_body:*)
+  (*forall bdy ge fn rs m s,*)
+  (*Ge = Genv ge fn ->*)
+  (*match_states (State rs m) s ->*)
+  (*match_outcome (exec_body ge bdy rs m) (exec Ge (trans_body bdy) s).*)
+(*Proof.*)
+  (*induction bdy as [|i bdy]; simpl; eauto. *)
+  (*intros.*)
+  (*exploit (bisimu_basic ge fn i rs m s); eauto.*)
+  (*destruct (exec_basic_instr _ _ _ _); simpl.*)
+  (*- intros (s' & X1 & X2). rewrite X1; simpl; eauto.*)
+  (*- intros X; rewrite X; simpl; auto.*)
+(*Qed.*)
+
+(*Theorem bisimu_exit ge fn b rs m s:*)
+  (*Ge = Genv ge fn ->*)
+  (*match_states (State rs m) s ->*)
+  (*match_outcome (exec_control ge fn (exit b) (nextblock b rs) m) (inst_run Ge (trans_pcincr (size b) (trans_exit (exit b))) s s).*)
+(*Proof.*)
+  (*intros; unfold exec_control, nextblock. rewrite inst_run_prun. *)
+  (*apply (bisimu_par_control (exit b) (size b) (Val.offset_ptr (rs PC) (Ptrofs.repr (size b))) ge fn rs rs m m s s); auto.*)
+(*Qed.*)
+
+(*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).*)
+(*Proof.*)
+  (*intros GENV MS. unfold exec_bblock.*)
+  (*exploit (bisimu_body (body b) ge fn rs m s); eauto.*)
+  (*unfold exec, trans_block; simpl.*)
+  (*destruct (exec_body _ _ _ _); simpl.*)
+  (*- intros (s' & X1 & X2).*)
+    (*erewrite run_app_Some; eauto.*)
+    (*exploit (bisimu_exit ge fn b rs0 m0 s'); eauto.*)
+    (*subst Ge; simpl. destruct X2 as (Y1 & Y2). erewrite Y2; simpl.*)
+    (*destruct (inst_run _ _ _); simpl; auto.*)
+  (*- intros X; erewrite run_app_None; eauto.*)
+(*Qed.*)
 
 Theorem trans_state_match: forall S, match_states S (trans_state S).
 Proof.
   intros. destruct S as (rs & m). simpl.
   split. reflexivity.
-  intro. destruct r; try reflexivity.
-  destruct g; reflexivity.
+  intro. destruct r as [dr|cr|]; try destruct dr as [ir|fr]; try destruct cr;
+  try destruct ir as [irr|]; try destruct irr; try destruct fr; try reflexivity.
 Qed.
 
-
 Lemma state_eq_decomp:
   forall rs1 m1 rs2 m2, rs1 = rs2 -> m1 = m2 -> State rs1 m1 = State rs2 m2.
 Proof.
@@ -1412,33 +1155,33 @@ Proof.
   - congruence.
 Qed.
 
-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'.
-Proof.
-  intros H H0 H1 o H2. unfold bblock_para_check in H1.
-  exploit (bisimu rs m bb ge fn); eauto. eapply trans_state_match.
-  rewrite H0; simpl.
-  intros (s2' & EXEC & MS).
-  exploit bisimu_par. 2: apply (trans_state_match (State rs m)). all: eauto.
-  intros (o2' & PRUN & MO).
-  exploit parallelizable_correct. apply is_para_correct_aux. eassumption.
-  intro. eapply H3 in PRUN. clear H3. destruct o2'.
-  - inv PRUN. inv H3. unfold exec in EXEC; unfold trans_state in H.
-    assert (x = s2') by congruence. subst. clear H.
-    assert (m0 = s2') by (apply functional_extensionality; auto). subst. clear H4.
-    destruct o; try discriminate. inv MO. inv H. assert (s2' = x) by congruence. subst.
-    exploit (state_equiv (State rs' m') (State rs0 m0)).
-    2: eapply H4. eapply MS. intro H. inv H. reflexivity.
-  - unfold match_outcome in MO. destruct o.
-    + inv MO. inv H3. discriminate.
-    + clear MO. unfold exec in EXEC.
-      unfold trans_state in PRUN; rewrite EXEC in PRUN. discriminate.
-Qed.
-
-End SECT_PAR.
+(*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'.*)
+(*Proof.*)
+  (*intros H H0 H1 o H2. unfold bblock_para_check in H1.*)
+  (*exploit (bisimu rs m bb ge fn); eauto. eapply trans_state_match.*)
+  (*rewrite H0; simpl.*)
+  (*intros (s2' & EXEC & MS).*)
+  (*exploit bisimu_par. 2: apply (trans_state_match (State rs m)). all: eauto.*)
+  (*intros (o2' & PRUN & MO).*)
+  (*exploit parallelizable_correct. apply is_para_correct_aux. eassumption.*)
+  (*intro. eapply H3 in PRUN. clear H3. destruct o2'.*)
+  (*- inv PRUN. inv H3. unfold exec in EXEC; unfold trans_state in H.*)
+    (*assert (x = s2') by congruence. subst. clear H.*)
+    (*assert (m0 = s2') by (apply functional_extensionality; auto). subst. clear H4.*)
+    (*destruct o; try discriminate. inv MO. inv H. assert (s2' = x) by congruence. subst.*)
+    (*exploit (state_equiv (State rs' m') (State rs0 m0)).*)
+    (*2: eapply H4. eapply MS. intro H. inv H. reflexivity.*)
+  (*- unfold match_outcome in MO. destruct o.*)
+    (*+ inv MO. inv H3. discriminate.*)
+    (*+ clear MO. unfold exec in EXEC.*)
+      (*unfold trans_state in PRUN; rewrite EXEC in PRUN. discriminate.*)
+(*Qed.*)
+
+(*End SECT_PAR.*)
 
 Section SECT_BBLOCK_EQUIV.
 
@@ -1447,15 +1190,14 @@ Variable Ge: genv.
 Local Hint Resolve trans_state_match: core.
 
 Lemma bblock_simu_reduce:
-  forall p1 p2 ge fn,
-  Ge = Genv ge fn ->
+  forall p1 p2,
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
-  Asmblockprops.bblock_simu ge fn p1 p2.
+  Asmblockprops.bblock_simu Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2.
 Proof.
-  unfold bblock_simu, res_eq; intros p1 p2 ge fn H1 H2 rs m DONTSTUCK.
-  generalize (H2 (trans_state (State rs m))); clear H2.
-  intro H2. 
-  exploit (bisimu Ge rs m p1 ge fn (trans_state (State rs m))); eauto.
+  unfold bblock_simu. intros p1 p2 H rs m rs' m' t EBB.
+  generalize (H (trans_state (State rs m))); clear H.
+  intro H. (* TODO How to define this correctly ?
+  exploit (bisimu rs m (body p1) (trans_state (State rs m))); eauto.
   exploit (bisimu Ge rs m p2 ge fn (trans_state (State rs m))); eauto.
   destruct (exec_bblock ge fn p1 rs m); try congruence.
   intros H3 (s2' & exp2 & MS'). unfold exec in exp2, H3. rewrite exp2 in H2.
@@ -1467,10 +1209,12 @@ Proof.
     - apply functional_extensionality. intros r.
       generalize (H0 r). intros Hr. congruence.
   * discriminate.
-Qed.
+Qed.*)
+Admitted.
 
 (** Used for debug traces *)
 
+(*
 Definition gpreg_name (gpr: gpreg) :=
   match gpr with
   | GPR0 => Str ("GPR0") | GPR1 => Str ("GPR1") | GPR2 => Str ("GPR2") | GPR3 => Str ("GPR3") | GPR4 => Str ("GPR4")
@@ -1768,24 +1512,24 @@ Definition string_of_op (op: P.op): ?? pstring :=
   | Constant _ => RET (Str "Constant")
   | Fail => RET (Str "Fail")
   end.
-
+  *)
 End SECT_BBLOCK_EQUIV.
 
 (** REWRITE RULES *)
 
-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.
-Proof.
-  destruct o; simpl in * |- *; try congruence.
-  destruct ao; simpl in * |- *; try congruence;
-  destruct n; simpl in * |- *; try congruence;
-  unfold arith_eval; destruct ge; simpl in * |- *; try congruence.
-Qed.
+(*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.*)
+(*Proof.*)
+  (*destruct o; simpl in * |- *; try congruence.*)
+  (*destruct ao; simpl in * |- *; try congruence;*)
+  (*destruct n; simpl in * |- *; try congruence;*)
+  (*unfold arith_eval; destruct ge; simpl in * |- *; try congruence.*)
+(*Qed.*)
 
 Definition main_reduce (t: Terms.term):= RET (Terms.nofail is_constant t).