24 files changed, 2286 insertions, 1377 deletions

diff --git a/configure b/configure
index 933086c7..2d18531d 100755
--- a/configure
+++ b/configure
@@ -805,6 +805,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
     Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
+    Asmblockdeps.v\\
     AbstractBasicBlocksDef.v DepTreeTheory.v ImpDep.v Parallelizability.v\\
     ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v
 EOF
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 99ee41e7..77fae8ee 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -15,7 +15,7 @@
 let prepro_options = ref ([]: string list)
 let linker_options = ref ([]: string list)
 let assembler_options = ref ([]: string list)
-let option_flongdouble = ref false
+let option_flongdouble = ref (Configuration.arch = "mppa_k1c")
 let option_fstruct_passing = ref false
 let option_fbitfields = ref false
 let option_fvararg_calls = ref true
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 7c735bf1..31bc855d 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -103,11 +103,18 @@ Inductive instruction : Type :=
   | Pfnegw  (rd rs: ireg)                           (**r float negate word *)

   | Pfnarrowdw (rd rs: ireg)                        (**r float narrow 64 -> 32 bits *)

   | Pfwidenlwd (rd rs: ireg)                        (**r float widen 32 -> 64 bits *)

-  | Pfloatwrnsz (rd rs: ireg)                       (**r Floating Point Conversion from integer *)

+  | Pfloatwrnsz (rd rs: ireg)                       (**r Floating Point Conversion from integer (32 -> 32) *)

+  | Pfloatuwrnsz (rd rs: ireg)                      (**r Floating Point Conversion from integer (u32 -> 32) *)

   | Pfloatudrnsz (rd rs: ireg)                       (**r Floating Point Conversion from unsigned integer (64 bits) *)

+  | Pfloatudrnsz_i32 (rd rs: ireg)                       (**r Floating Point Conversion from unsigned integer (32 bits) *)

   | Pfloatdrnsz (rd rs: ireg)                       (**r Floating Point Conversion from integer (64 bits) *)

+  | Pfloatdrnsz_i32 (rd rs: ireg)                       (**r Floating Point Conversion from integer (32 bits) *)

   | Pfixedwrzz (rd rs: ireg)                        (**r Integer conversion from floating point *)

-  | Pfixeddrzz (rd rs: ireg)                        (**r Integer conversion from floating point (64 bits) *)

+  | Pfixeduwrzz (rd rs: ireg)                        (**r Integer conversion from floating point (f32 -> 32 bits unsigned *)

+  | Pfixeddrzz (rd rs: ireg)                        (**r Integer conversion from floating point (i64 -> 64 bits) *)

+  | Pfixeddrzz_i32 (rd rs: ireg)                        (**r Integer conversion from floating point (i32 -> f64) *)

+  | Pfixedudrzz (rd rs: ireg)                        (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *)

+  | Pfixedudrzz_i32 (rd rs: ireg)                        (**r unsigned Integer conversion from floating point (u32 -> 64 bits) *)

 

   (** Arith RI32 *)

   | Pmake   (rd: ireg) (imm: int)                   (**r load immediate *)

@@ -124,6 +131,8 @@ Inductive instruction : Type :=
   (** Arith RRR *)

   | Pcompw  (it: itest) (rd rs1 rs2: ireg)          (**r comparison word *)

   | Pcompl  (it: itest) (rd rs1 rs2: ireg)          (**r comparison long *)

+  | Pfcompw (ft: ftest) (rd rs1 rs2: ireg)          (**r comparison float *)

+  | Pfcompl (ft: ftest) (rd rs1 rs2: ireg)          (**r comparison float64 *)

 

   | Paddw               (rd rs1 rs2: ireg)          (**r add word *)

   | Psubw               (rd rs1 rs2: ireg)          (**r sub word *)

@@ -216,11 +225,18 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRR Asmblock.Pfnegw rd rs => Pfnegw rd rs

   | PArithRR Asmblock.Pfnarrowdw rd rs => Pfnarrowdw rd rs

   | PArithRR Asmblock.Pfwidenlwd rd rs => Pfwidenlwd rd rs

+  | PArithRR Asmblock.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs

   | PArithRR Asmblock.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs

   | PArithRR Asmblock.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs

   | PArithRR Asmblock.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs

+  | PArithRR Asmblock.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs

+  | PArithRR Asmblock.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs

   | PArithRR Asmblock.Pfixedwrzz rd rs => Pfixedwrzz rd rs

+  | PArithRR Asmblock.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs

   | PArithRR Asmblock.Pfixeddrzz rd rs => Pfixeddrzz rd rs

+  | PArithRR Asmblock.Pfixedudrzz rd rs => Pfixedudrzz rd rs

+  | PArithRR Asmblock.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs

+  | PArithRR Asmblock.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs

 

   (* RI32 *)

   | PArithRI32 Asmblock.Pmake rd imm  => Pmake rd imm

@@ -237,6 +253,8 @@ Definition basic_to_instruction (b: basic) :=
   (* RRR *)

   | PArithRRR (Asmblock.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2

   | PArithRRR (Asmblock.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2

+  | PArithRRR (Asmblock.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2

+  | PArithRRR (Asmblock.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2

   | PArithRRR Asmblock.Paddw rd rs1 rs2       => Paddw rd rs1 rs2

   | PArithRRR Asmblock.Psubw rd rs1 rs2       => Psubw rd rs1 rs2

   | PArithRRR Asmblock.Pmulw rd rs1 rs2       => Pmulw rd rs1 rs2

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index b9c50517..86c47613 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -126,6 +126,17 @@ Inductive itest: Type :=
   | ITnone                              (**r Not Any Bits Set in Mask *)
   .
 
+Inductive ftest: Type :=
+  | FTone                               (**r Ordered and Not Equal *)
+  | FTueq                               (**r Unordered or Equal *)
+  | FToeq                               (**r Ordered and Equal *)
+  | FTune                               (**r Unordered or Not Equal *)
+  | FTolt                               (**r Ordered and Less Than *)
+  | FTuge                               (**r Unordered or Greater Than or Equal *)
+  | FToge                               (**r Ordered and Greater Than or Equal *)
+  | FTult                               (**r Unordered or Less Than *)
+  .
+
 (** Offsets for load and store instructions.  An offset is either an
   immediate integer or the low part of a symbol. *)
 
@@ -287,11 +298,18 @@ Inductive arith_name_rr : Type :=
   | Pfnegw                                          (**r float negate word *)
   | Pfnarrowdw                                      (**r float narrow 64 -> 32 bits *)
   | Pfwidenlwd                                      (**r Floating Point widen from 32 bits to 64 bits *)
-  | Pfloatwrnsz                                     (**r Floating Point Conversion from integer (int -> single) *)
-  | Pfloatudrnsz                                    (**r Floating Point Conversion from unsigned integer (ulong -> float) *)
+  | Pfloatwrnsz                                     (**r Floating Point conversion from integer (int -> SINGLE) *)
+  | Pfloatuwrnsz                                    (**r Floating Point conversion from integer (unsigned int -> SINGLE) *)
+  | Pfloatudrnsz                                    (**r Floating Point Conversion from integer (unsigned long -> float) *)
+  | Pfloatudrnsz_i32                                (**r Floating Point Conversion from integer (unsigned int -> float) *)
   | Pfloatdrnsz                                     (**r Floating Point Conversion from integer (long -> float) *)
+  | Pfloatdrnsz_i32                                 (**r Floating Point Conversion from integer (int -> float) *)
   | Pfixedwrzz                                      (**r Integer conversion from floating point (single -> int) *)
+  | Pfixeduwrzz                                     (**r Integer conversion from floating point (single -> unsigned int) *)
   | Pfixeddrzz                                      (**r Integer conversion from floating point (float -> long) *)
+  | Pfixedudrzz                                      (**r Integer conversion from floating point (float -> unsigned long) *)
+  | Pfixeddrzz_i32                                  (**r Integer conversion from floating point (float -> int) *)
+  | Pfixedudrzz_i32                                  (**r Integer conversion from floating point (float -> unsigned int) *)
 .
 
 Inductive arith_name_ri32 : Type :=
@@ -313,6 +331,8 @@ Inductive arith_name_rf64 : Type :=
 Inductive arith_name_rrr : Type :=
   | Pcompw  (it: itest)                             (**r comparison word *)
   | Pcompl  (it: itest)                             (**r comparison long *)
+  | Pfcompw (ft: ftest)                             (**r comparison float32 *)
+  | Pfcompl (ft: ftest)                             (**r comparison float64 *)
 
   | Paddw                                           (**r add word *)
   | Psubw                                           (**r sub word *)
@@ -578,6 +598,36 @@ Proof.
   - destruct e; simpl; try omega. contradict H; simpl; auto.
  *)Qed.
 
+
+Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
+Next Obligation.
+  destruct bb; simpl. assumption.
+Defined.
+
+Lemma no_header_size:
+  forall bb, size (no_header bb) = size bb.
+Proof.
+  intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity.
+Qed.
+
+Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.
+Next Obligation.
+  destruct bb; simpl. assumption.
+Defined.
+
+Lemma stick_header_size:
+  forall h bb, size (stick_header h bb) = size bb.
+Proof.
+  intros. destruct bb. unfold stick_header. simpl. reflexivity.
+Qed.
+
+Lemma stick_header_no_header:
+  forall bb, stick_header (header bb) (no_header bb) = bb.
+Proof.
+  intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity.
+Qed.
+
+
 Definition bblocks := list bblock.
 
 Fixpoint size_blocks (l: bblocks): Z :=
@@ -779,6 +829,31 @@ Definition itest_for_cmp (c: comparison) (s: signedness) :=
   | Cgt, Unsigned => ITgtu
   end.
 
+Inductive oporder_ftest :=
+  | Normal (ft: ftest)
+  | Reversed (ft: ftest)
+.
+
+Definition ftest_for_cmp (c: comparison) :=
+  match c with
+  | Ceq => Normal FToeq
+  | Cne => Normal FTune
+  | Clt => Normal FTolt
+  | Cle => Reversed FToge
+  | Cgt => Reversed FTolt
+  | Cge => Normal FToge
+  end.
+
+Definition notftest_for_cmp (c: comparison) :=
+  match c with
+  | Ceq => Normal FTune
+  | Cne => Normal FToeq
+  | Clt => Normal FTuge
+  | Cle => Reversed FTult
+  | Cgt => Reversed FTuge
+  | Cge => Normal FTult
+  end.
+
 (* CoMPare Signed Words to Zero *)
 Definition btest_for_cmpswz (c: comparison) :=
   match c with
@@ -873,6 +948,28 @@ Definition compare_long (t: itest) (v1 v2: val) (m: mem): val :=
   end
   .
 
+Definition compare_single (t: ftest) (v1 v2: val): val :=
+  match t with
+  | FTone | FTueq => Vundef (* unused *)
+  | FToeq => Val.cmpfs Ceq v1 v2
+  | FTune => Val.cmpfs Cne v1 v2
+  | FTolt => Val.cmpfs Clt v1 v2
+  | FTuge => Val.notbool (Val.cmpfs Clt v1 v2)
+  | FToge => Val.cmpfs Cge v1 v2
+  | FTult => Val.notbool (Val.cmpfs Cge v1 v2)
+  end.
+
+Definition compare_float (t: ftest) (v1 v2: val): val :=
+  match t with
+  | FTone | FTueq => Vundef (* unused *)
+  | FToeq => Val.cmpf Ceq v1 v2
+  | FTune => Val.cmpf Cne v1 v2
+  | FTolt => Val.cmpf Clt v1 v2
+  | FTuge => Val.notbool (Val.cmpf Clt v1 v2)
+  | FToge => Val.cmpf Cge v1 v2
+  | FTult => Val.notbool (Val.cmpf Cge v1 v2)
+  end.
+
 (** Execution of arith instructions 
 
 TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma...
@@ -906,10 +1003,17 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
       | Pfnarrowdw => rs#d <- (Val.singleoffloat rs#s)
       | Pfwidenlwd => rs#d <- (Val.floatofsingle rs#s)
       | Pfloatwrnsz => rs#d <- (match Val.singleofint rs#s with Some f => f | _ => Vundef end)
+      | Pfloatuwrnsz => rs#d <- (match Val.singleofintu rs#s with Some f => f | _ => Vundef end)
       | Pfloatudrnsz => rs#d <- (match Val.floatoflongu rs#s with Some f => f | _ => Vundef end)
+      | Pfloatudrnsz_i32 => rs#d <- (match Val.floatofintu rs#s with Some f => f | _ => Vundef end)
       | Pfloatdrnsz => rs#d <- (match Val.floatoflong rs#s with Some f => f | _ => Vundef end)
+      | Pfloatdrnsz_i32 => rs#d <- (match Val.floatofint rs#s with Some f => f | _ => Vundef end)
       | Pfixedwrzz => rs#d <- (match Val.intofsingle rs#s with Some i => i | _ => Vundef end)
+      | Pfixeduwrzz => rs#d <- (match Val.intuofsingle rs#s with Some i => i | _ => Vundef end)
       | Pfixeddrzz => rs#d <- (match Val.longoffloat rs#s with Some i => i | _ => Vundef end)
+      | Pfixeddrzz_i32 => rs#d <- (match Val.intoffloat rs#s with Some i => i | _ => Vundef end)
+      | Pfixedudrzz => rs#d <- (match Val.longuoffloat rs#s with Some i => i | _ => Vundef end)
+      | Pfixedudrzz_i32 => rs#d <- (match Val.intuoffloat rs#s with Some i => i | _ => Vundef end)
       end
 
   | PArithRI32 n d i =>
@@ -936,6 +1040,8 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
       match n with
       | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2 m)
       | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2 m)
+      | Pfcompw c => rs#d <- (compare_single c rs#s1 rs#s2)
+      | Pfcompl c => rs#d <- (compare_float c rs#s1 rs#s2)
       | Paddw  => rs#d <- (Val.add  rs#s1 rs#s2)
       | Psubw  => rs#d <- (Val.sub  rs#s1 rs#s2)
       | Pmulw  => rs#d <- (Val.mul  rs#s1 rs#s2)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 83064762..c2477e66 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -80,9 +80,11 @@ Inductive op_wrap :=
   | 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.
@@ -115,10 +117,17 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
       | Pfnarrowdw => Some (Val (Val.singleoffloat v))
       | Pfwidenlwd => Some (Val (Val.floatofsingle v))
       | Pfloatwrnsz => Some (Val (match Val.singleofint v with Some f => f | _ => Vundef end))
+      | Pfloatuwrnsz => Some (Val (match Val.singleofintu v with Some f => f | _ => Vundef end))
       | Pfloatudrnsz => Some (Val (match Val.floatoflongu v with Some f => f | _ => Vundef end))
       | Pfloatdrnsz => Some (Val (match Val.floatoflong v with Some f => f | _ => Vundef end))
+      | Pfloatudrnsz_i32 => Some (Val (match Val.floatofintu v with Some f => f | _ => Vundef end))
+      | Pfloatdrnsz_i32 => Some (Val (match Val.floatofint v with Some f => f | _ => Vundef end))
       | Pfixedwrzz => Some (Val (match Val.intofsingle v with Some i => i | _ => Vundef end))
+      | Pfixeduwrzz => Some (Val (match Val.intuofsingle v with Some i => i | _ => Vundef end))
       | Pfixeddrzz => Some (Val (match Val.longoffloat v with Some i => i | _ => Vundef end))
+      | Pfixedudrzz => Some (Val (match Val.longuoffloat v with Some i => i | _ => Vundef end))
+      | Pfixeddrzz_i32 => Some (Val (match Val.intoffloat v with Some i => i | _ => Vundef end))
+      | Pfixedudrzz_i32 => Some (Val (match Val.intuoffloat v with Some i => i | _ => Vundef end))
       end
 
   | OArithRI32 n i, [] =>
@@ -150,6 +159,9 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
 
   | OArithRRR n, [Val v1; Val v2] =>
       match n with
+      | Pfcompw c => Some (Val (compare_single c v1 v2))
+      | Pfcompl c => Some (Val (compare_float c v1 v2))
+
       | Paddw  => Some (Val (Val.add  v1 v2))
       | Psubw  => Some (Val (Val.sub  v1 v2))
       | Pmulw  => Some (Val (Val.mul  v1 v2))
@@ -328,6 +340,13 @@ Definition op_eval (o: op) (l: list value) :=
       | 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
@@ -355,6 +374,7 @@ Definition op_eval (o: op) (l: list value) :=
           end
       end
   | Constant v, [] => Some (Val v)
+  | Fail, _ => None
   | _, _ => None
   end.
 
@@ -443,6 +463,7 @@ Definition op_eq (o1 o2: op): ?? bool :=
   | Freeframe sz1 pos1, Freeframe sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2)
   | Freeframe2 sz1 pos1, Freeframe2 sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2)
   | Constant c1, Constant c2 => phys_eq c1 c2
+  | Fail, Fail => RET true
   | _, _ => RET false
   end.
 
@@ -559,9 +580,21 @@ Definition trans_arith (ai: ar_instruction) : macro :=
   | 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)) (Name (#s1) @ Name (#s2) @ Enil))]
-  | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))]
-  | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))]
+  | PArithRRR n d s1 s2 => 
+      match n with
+      | Pcompw _ | Pcompl _ => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Name pmem @ Enil))]
+      | _ => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Enil))]
+      end
+  | PArithRRI32 n d s i =>
+      match n with
+      | Pcompiw _ => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Name pmem @ Enil))]
+      | _ => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))]
+      end
+  | PArithRRI64 n d s i => 
+      match n with
+      | Pcompil _ => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Name pmem @ Enil))]
+      | _ => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))]
+      end
   end.
 
 
@@ -570,13 +603,19 @@ Definition trans_basic (b: basic) : macro :=
   | PArith ai => trans_arith ai
   | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (Name (#a) @ Name pmem @ Enil))]
   | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (Name (#s) @ Name (#a) @ Name pmem @ Enil))]
-  | Pallocframe sz pos => [(pmem, Op (Allocframe sz pos) (Name (#SP) @ Name pmem @ Enil));
-                           (#FP, Name (#SP)); (#SP, Name (#RTMP)); (#RTMP, Op (Constant Vundef) Enil)]
+  | Pallocframe sz pos => [(#FP, Name (#SP)); (#SP, Op (Allocframe2 sz pos) (Name (#SP) @ Name pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil);
+                           (pmem, Op (Allocframe sz pos) (Old (Name (#SP)) @ Name pmem @ Enil))]
   | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (Name (#SP) @ Name pmem @ Enil));
-                          (#SP, Op (Freeframe2 sz pos) (Name (#SP) @ Name pmem @ Enil));
+                          (#SP, Op (Freeframe2 sz pos) (Name (#SP) @ Old (Name pmem) @ Enil));
                           (#RTMP, Op (Constant Vundef) Enil)]
-  | Pget rd ra => [(#rd, Name (#ra))]
-  | Pset ra rd => [(#ra, Name (#rd))]
+  | Pget rd ra => match ra with
+                  | RA => [(#rd, Name (#ra))]
+                  | _ => [(#rd, Op Fail Enil)]
+                  end
+  | Pset ra rd => match ra with
+                  | RA => [(#ra, Name (#rd))]
+                  | _ => [(#rd, Op Fail Enil)]
+                  end
   | Pnop => []
   end.
 
@@ -591,6 +630,16 @@ Definition trans_pcincr (sz: Z) := [(#PC, Op (Control (OIncremPC sz)) (Name (#PC
 Definition trans_block (b: Asmblock.bblock) : L.bblock :=
   trans_body (body b) ++ trans_pcincr (size b) ++ trans_exit (exit b).
 
+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.
+
 Definition state := L.mem.
 Definition exec := L.run.
 
@@ -609,14 +658,53 @@ Definition trans_state (s: Asmblock.state) : state :=
            | None => Val Vundef
            end.
 
-Lemma pos_gpreg_not_3: forall g: gpreg, 3 <> # g.
+Lemma pos_gpreg_not: forall g: gpreg, pmem <> (#g) /\ 2 <> (#g) /\ 3 <> (#g).
+Proof.
+  intros. split; try split. all: destruct g; try discriminate.
+Qed.
+
+Lemma not_3_plus_n:
+  forall n, 3 + n <> pmem /\ 3 + n <> (# RA) /\ 3 + n <> (# PC).
 Proof.
-  destruct g; try discriminate.
+  intros. split; try split.
+  all: destruct n; simpl; try (destruct n; discriminate); try discriminate.
 Qed.
 
-Lemma pos_gpreg_not_2: forall g: gpreg, 2 <> # g.
+Lemma not_eq_add:
+  forall k n n', n <> n' -> k + n <> k + n'.
+Proof.
+Admitted. (* FIXME - help Sylvain ? *)
+
+Lemma not_eq_ireg_to_pos:
+  forall n r r', r' <> r -> n + ireg_to_pos r <> n + ireg_to_pos r'.
 Proof.
-  destruct g; try discriminate.
+  intros. destruct r; destruct r'; try contradiction; apply not_eq_add; discriminate. (* FIXME - quite long to prove *)
+Qed.
+
+Lemma not_eq_ireg_ppos: 
+  forall r r', r <> r' -> (# r') <> (# r).
+Proof.
+  intros. unfold ppos. destruct r.
+  - destruct r'; try discriminate.
+    + apply not_eq_ireg_to_pos; congruence.
+    + destruct g; discriminate.
+    + destruct g; discriminate.
+  - destruct r'; try discriminate; try contradiction.
+    destruct g; discriminate.
+  - destruct r'; try discriminate; try contradiction.
+    destruct g; discriminate.
+Qed.
+
+Lemma not_eq_ireg_to_pos_ppos:
+  forall r r', r' <> r -> 3 + ireg_to_pos r <> # r'.
+Proof.
+  intros. unfold ppos. apply not_eq_ireg_to_pos. assumption.
+Qed.
+
+Lemma not_eq_IR:
+  forall r r', r <> r' -> IR r <> IR r'.
+Proof.
+  intros. congruence.
 Qed.
 
 Ltac Simplif :=
@@ -625,7 +713,7 @@ Ltac Simplif :=
   || (rewrite Pregmap.gss)
   || (rewrite nextblock_pc)
   || (rewrite Pregmap.gso by eauto with asmgen)
-  || (rewrite assign_diff by (try discriminate; try (apply pos_gpreg_not_3); try (apply pos_gpreg_not_2)))
+  || (rewrite assign_diff by (try discriminate; try (apply pos_gpreg_not); try (apply not_3_plus_n); try (apply not_eq_ireg_ppos; apply not_eq_IR; auto); try (apply not_eq_ireg_to_pos_ppos; auto)))
   || (rewrite assign_eq)
   ); auto with asmgen.
 
@@ -641,16 +729,174 @@ Proof.
   destruct g; reflexivity.
 Qed.
 
-Lemma exec_match_app:
+Lemma exec_app_some:
   forall c c' s s' s'',
   exec Ge c s = Some s' ->
   exec Ge c' s' = Some s'' ->
   exec Ge (c ++ c') s = Some s''.
 Proof.
-Admitted.
+  induction c.
+  - simpl. intros. congruence.
+  - intros. simpl in *. destruct (macro_run _ _ _ _); auto. eapply IHc; eauto. discriminate.
+Qed.
+
+Lemma exec_app_none:
+  forall c c' s,
+  exec Ge c s = None ->
+  exec Ge (c ++ c') s = None.
+Proof.
+  induction c.
+  - simpl. discriminate.
+  - intros. simpl. simpl in H. destruct (macro_run _ _ _ _); auto.
+Qed.
+
+Lemma trans_arith_correct:
+  forall ge fn i rs m rs' s,
+  exec_arith_instr ge i rs m = rs' ->
+  match_states (State rs m) s ->
+  exists s',
+     macro_run (Genv ge fn) (trans_arith i) s s = Some s'
+  /\ match_states (State rs' m) s'.
+Proof.
+  intros. unfold exec_arith_instr in H. destruct i.
+(* Ploadsymbol *)
+  - destruct i. inv H. inv H0.
+    eexists; split; try split.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithRR *)
+  - destruct i.
+    all: inv H; inv H0;
+    eexists; split; try split;
+    [ simpl; pose (H1 rs0); simpl in e; rewrite e; reflexivity |
+      Simpl |
+      intros rr; destruct rr; Simpl;
+      destruct (ireg_eq g rd); subst; Simpl ].
+(* PArithRI32 *)
+  - destruct i. inv H. inv H0.
+    eexists; split; try split.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithRI64 *)
+  - destruct i. inv H. inv H0.
+    eexists; split; try split.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithRF32 *)
+  - destruct i. inv H. inv H0.
+    eexists; split; try split.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithRF64 *)
+  - destruct i. inv H. inv H0.
+    eexists; split; try split.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithRRR *)
+  - destruct i.
+    all: inv H; inv H0;
+    eexists; split; try split;
+    [ simpl; pose (H1 rs1); simpl in e; rewrite e; pose (H1 rs2); simpl in e0; rewrite e0; try (rewrite H); reflexivity
+    | Simpl
+    | intros rr; destruct rr; Simpl;
+      destruct (ireg_eq g rd); subst; Simpl ].
+(* PArithRRI32 *)
+  - destruct i.
+    all: inv H; inv H0;
+    eexists; split; try split;
+    [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); reflexivity
+    | Simpl
+    | intros rr; destruct rr; Simpl;
+      destruct (ireg_eq g rd); subst; Simpl ].
+(* PArithRRI64 *)
+  - destruct i.
+    all: inv H; inv H0;
+    eexists; split; try split;
+    [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); reflexivity
+    | Simpl
+    | intros rr; destruct rr; Simpl;
+      destruct (ireg_eq g rd); subst; Simpl ].
+Qed.
+
+Lemma forward_simu_basic:
+  forall ge fn b rs m rs' m' s,
+  exec_basic_instr ge b rs m = Next rs' m' ->
+  match_states (State rs m) s ->
+  exists s',
+     macro_run (Genv ge fn) (trans_basic b) s s = Some s'
+  /\ match_states (State rs' m') s'.
+Proof.
+  intros. destruct b.
+(* Arith *)
+  - simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto.
+(* Load *)
+  - simpl in H. destruct i; destruct i.
+    all: unfold exec_load in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
+    destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
+    eexists; split; try split;
+    [ simpl; rewrite EVALOFF; rewrite H; pose (H1 ra); simpl in e; rewrite e; rewrite MEML; reflexivity|
+     Simpl|
+     intros rr; destruct rr; Simpl;
+      destruct (ireg_eq g rd); [
+       subst; Simpl|
+       Simpl; rewrite assign_diff; pose (H1 g); simpl in e; try assumption; Simpl; unfold ppos; apply not_eq_ireg_to_pos; assumption]].
+(* Store *)
+  - simpl in H. destruct i; destruct i.
+    all: unfold exec_store in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
+    destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
+    eexists; split; try split;
+    [ simpl; rewrite EVALOFF; rewrite H; pose (H1 ra); simpl in e; rewrite e; pose (H1 rs0); simpl in e0; rewrite e0; rewrite MEML; reflexivity
+    | Simpl
+    | intros rr; destruct rr; Simpl].
+(* Allocframe *)
+  - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate.
+    inv H. inv H0. eexists. split; try split.
+    * simpl. Simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite MEMAL. rewrite MEMS. Simpl.
+      rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity.
+    * Simpl.
+    * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]].
+      ** subst. Simpl.
+      ** subst. Simpl.
+      ** subst. Simpl.
+      ** Simpl. repeat (rewrite assign_diff). auto.
+         pose (not_eq_ireg_to_pos_ppos GPR14 g). simpl ireg_to_pos in n2. auto.
+         pose (not_eq_ireg_to_pos_ppos GPR12 g). simpl ireg_to_pos in n2. auto.
+         pose (not_eq_ireg_to_pos_ppos GPR32 g). simpl ireg_to_pos in n2. auto.
+(* Freeframe *)
+  - simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rs GPR12) eqn:SPeq; try discriminate.
+    destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv H0.
+    eexists. split; try split.
+    * simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE.
+      Simpl. rewrite e. rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity.
+    * Simpl.
+    * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]].
+      ** subst. Simpl.
+      ** subst. Simpl.
+      ** subst. Simpl.
+      ** Simpl. repeat (rewrite assign_diff). auto.
+         unfold ppos. pose (not_3_plus_n (ireg_to_pos g)). destruct a as (A & _ & _). auto.
+         pose (not_eq_ireg_to_pos_ppos GPR12 g). simpl ireg_to_pos in n2. auto.
+         pose (not_eq_ireg_to_pos_ppos GPR32 g). simpl ireg_to_pos in n2. auto.
+(* Pget *)
+  - simpl in H. destruct rs0 eqn:rs0eq; try discriminate. inv H. inv H0.
+    eexists. split; try split. Simpl. intros rr; destruct rr; Simpl.
+    destruct (ireg_eq g rd).
+    * subst. Simpl.
+    * Simpl.
+(* Pset *)
+  - simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv H0.
+    eexists. split; try split. Simpl. intros rr; destruct rr; Simpl.
+(* Pnop *)
+  - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption.
+Qed.
 
 Lemma forward_simu_body:
-  forall ge bdy rs m rs' m' fn s,
+  forall bdy ge rs m rs' m' fn s,
   Ge = Genv ge fn ->
   exec_body ge bdy rs m = Next rs' m' ->
   match_states (State rs m) s ->
@@ -658,7 +904,15 @@ Lemma forward_simu_body:
      exec Ge (trans_body bdy) s = Some s'
   /\ match_states (State rs' m') s'.
 Proof.
-Admitted.
+  induction bdy.
+  - intros. inv H1. simpl in *. inv H0. eexists. repeat (split; auto).
+  - intros until s. intros GE EXEB MS. simpl in EXEB. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate.
+    exploit forward_simu_basic; eauto. intros (s' & MRUN & MS'). subst Ge.
+    eapply IHbdy in MS'; eauto. destruct MS' as (s'' & EXECB & MS').
+    eexists. split.
+    * simpl. rewrite MRUN. eassumption.
+    * eassumption.
+Qed.
 
 Lemma forward_simu_control:
   forall ge fn ex b rs m rs2 m2 s,
@@ -753,22 +1007,328 @@ Proof.
     intros. unfold nextblock. destruct r; Simpl.
 Qed. 
 
-Theorem forward_simu:

-  forall rs1 m1 rs2 m2 s1' b ge fn,

-    Ge = Genv ge fn ->

-    exec_bblock ge fn b rs1 m1 = Next rs2 m2 ->

-    match_states (State rs1 m1) s1' ->

-    exists s2',

-       exec Ge (trans_block b) s1' = Some s2'

-    /\ match_states (State rs2 m2) s2'.

-Proof.

-  intros until fn. intros GENV EXECB MS. unfold exec_bblock in EXECB. destruct (exec_body _ _ _) eqn:EXEB; try discriminate.

-  exploit forward_simu_body; eauto. intros (s' & EXETRANSB & MS').

-  exploit forward_simu_control; eauto. intros (s'' & EXETRANSEX & MS'').

-

-  eexists. split.

-  unfold trans_block. eapply exec_match_app. eassumption. eassumption.

-  eassumption.

-Qed.

-

-End SECT.

+Theorem forward_simu:
+  forall rs1 m1 rs2 m2 s1' b ge fn,
+    Ge = Genv ge fn ->
+    exec_bblock ge fn b rs1 m1 = Next rs2 m2 ->
+    match_states (State rs1 m1) s1' ->
+    exists s2',
+       exec Ge (trans_block b) s1' = Some s2'
+    /\ match_states (State rs2 m2) s2'.
+Proof.
+  intros until fn. intros GENV EXECB MS. unfold exec_bblock in EXECB. destruct (exec_body _ _ _) eqn:EXEB; try discriminate.
+  exploit forward_simu_body; eauto. intros (s' & EXETRANSB & MS').
+  exploit forward_simu_control; eauto. intros (s'' & EXETRANSEX & MS'').
+
+  eexists. split.
+  unfold trans_block. eapply exec_app_some. eassumption. eassumption.
+  eassumption.
+Qed.
+
+Lemma exec_bblock_stuck_nec:
+  forall ge fn b rs m,
+     exec_body ge (body b) rs m = Stuck
+  \/ (exists rs' m', exec_body ge (body b) rs m = Next rs' m' /\ exec_control ge fn (exit b) (nextblock b rs') m' = Stuck)
+  <-> exec_bblock ge fn b rs m = Stuck.
+Proof.
+  intros. split.
+  + intros. destruct H.
+    - unfold exec_bblock. rewrite H. reflexivity.
+    - destruct H as (rs' & m' & EXEB & EXEC). unfold exec_bblock. rewrite EXEB. assumption.
+  + intros. unfold exec_bblock in H. destruct (exec_body _ _ _ _) eqn:EXEB.
+    - right. repeat eexists. assumption.
+    - left. reflexivity.
+Qed.
+
+Lemma exec_basic_instr_next_exec:
+  forall ge fn i rs m rs' m' s tc,
+  Ge = Genv ge fn ->
+  exec_basic_instr ge i rs m = Next rs' m' ->
+  match_states (State rs m) s ->
+  exists s',
+     exec Ge (trans_basic i :: tc) s = exec Ge tc s'
+  /\ match_states (State rs' m') s'.
+Proof.
+  intros. exploit forward_simu_basic; eauto.
+  intros (s' & MRUN & MS').
+  simpl exec. exists s'. subst. rewrite MRUN. split; auto.
+Qed.
+
+Lemma exec_body_next_exec:
+  forall c ge fn rs m rs' m' s tc,
+  Ge = Genv ge fn ->
+  exec_body ge c rs m = Next rs' m' ->
+  match_states (State rs m) s ->
+  exists s',
+     exec Ge (trans_body c ++ tc) s = exec Ge tc s'
+  /\ match_states (State rs' m') s'.
+Proof.
+  induction c.
+  - intros. simpl in H0. inv H0. simpl. exists s. split; auto.
+  - intros. simpl in H0. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate.
+    exploit exec_basic_instr_next_exec; eauto. intros (s' & EXEGEBASIC & MS').
+    simpl trans_body. rewrite <- app_comm_cons. rewrite EXEGEBASIC.
+    eapply IHc; eauto.
+Qed.
+
+Lemma exec_trans_pcincr_exec:
+  forall rs m s b,
+  match_states (State rs m) s ->
+  exists s',
+     exec Ge (trans_pcincr (size b) ++ trans_exit (exit b)) s = exec Ge (trans_exit (exit b)) s'
+  /\ match_states (State (nextblock b rs) m) s'.
+Proof.
+  intros. inv H. eexists. split. simpl.
+  unfold control_eval. pose (H1 PC); simpl in e; rewrite e. destruct Ge. reflexivity.
+  simpl. split.
+  - Simpl.
+  - intros rr; destruct rr; Simpl.
+Qed.
+
+Lemma exec_exit_none:
+  forall ge fn rs m s ex,
+  Ge = Genv ge fn ->
+  match_states (State rs m) s ->
+  exec Ge (trans_exit ex) s = None ->
+  exec_control ge fn ex rs m = Stuck.
+Proof.
+  intros. inv H0. destruct ex as [ctl|]; try discriminate.
+  destruct ctl; destruct i; try reflexivity; try discriminate.
+(* Pj_l *)
+  - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e.
+    unfold goto_label_deps in H1. unfold goto_label.
+    destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
+(* Pcb *)
+  - simpl in *. destruct (cmp_for_btest bt). destruct i.
+    + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
+      destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e.
+      unfold eval_branch_deps in H1; unfold eval_branch.
+      destruct (Val.cmp_bool _ _ _); auto. destruct b; try discriminate.
+      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      destruct (rs PC); auto. discriminate.
+    + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
+      destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e.
+      unfold eval_branch_deps in H1; unfold eval_branch.
+      destruct (Val.cmpl_bool _ _ _); auto. destruct b; try discriminate.
+      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      destruct (rs PC); auto. discriminate.
+(* Pcbu *)
+  - simpl in *. destruct (cmpu_for_btest bt). destruct i.
+    + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
+      destruct o; auto. rewrite H2 in H1.
+      pose (H3 r); simpl in e; rewrite e in H1; clear e.
+      unfold eval_branch_deps in H1; unfold eval_branch.
+      destruct (Val.cmpu_bool _ _ _ _); auto. destruct b; try discriminate.
+      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      destruct (rs PC); auto. discriminate.
+    + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
+      destruct o; auto. rewrite H2 in H1.
+      pose (H3 r); simpl in e; rewrite e in H1; clear e.
+      unfold eval_branch_deps in H1; unfold eval_branch.
+      destruct (Val.cmplu_bool _ _ _); auto. destruct b; try discriminate.
+      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      destruct (rs PC); auto. discriminate.
+Qed.
+
+Theorem trans_block_reverse_stuck:
+  forall ge fn b rs m s,
+  Ge = Genv ge fn ->
+  exec Ge (trans_block b) s = None ->
+  match_states (State rs m) s ->
+  exec_bblock ge fn b rs m = Stuck.
+Proof.
+  intros until s. intros Geq EXECBK MS.
+  apply exec_bblock_stuck_nec.
+  destruct (exec_body _ _ _ _) eqn:EXEB.
+  - right. repeat eexists.
+    exploit exec_body_next_exec; eauto.
+    intros (s' & EXECBK' & MS'). unfold trans_block in EXECBK. rewrite EXECBK' in EXECBK. clear EXECBK'. clear EXEB MS.
+    exploit exec_trans_pcincr_exec; eauto. intros (s'' & EXECINCR' & MS''). rewrite EXECINCR' in EXECBK. clear EXECINCR' MS'.
+    eapply exec_exit_none; eauto.
+  - left. reflexivity.
+Qed.
+
+Lemma forward_simu_basic_instr_stuck:
+  forall i ge fn rs m s,
+  Ge = Genv ge fn ->
+  exec_basic_instr ge i rs m = Stuck ->
+  match_states (State rs m) s ->
+  exec Ge [trans_basic i] s = None.
+Proof.
+  intros. inv H1. unfold exec_basic_instr in H0. destruct i; try discriminate.
+(* PLoad *)
+  - destruct i; destruct i.
+    all: simpl; rewrite H2; pose (H3 ra); simpl in e; rewrite e; clear e;
+    unfold exec_load in H0; destruct (eval_offset _ _); auto; destruct (Mem.loadv _ _ _); auto; discriminate.
+(* PStore *)
+  - destruct i; destruct i;
+    simpl; rewrite H2; pose (H3 ra); simpl in e; rewrite e; clear e; pose (H3 rs0); simpl in e; rewrite e; clear e;
+    unfold exec_store in H0; destruct (eval_offset _ _); auto; destruct (Mem.storev _ _ _); auto; discriminate.
+(* Pallocframe *)
+  - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0.
+    destruct (Mem.store _ _ _ _); try discriminate. reflexivity.
+(* Pfreeframe *)
+  - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2.
+    destruct (Mem.loadv _ _ _); auto. destruct (rs GPR12); auto. destruct (Mem.free _ _ _ _); auto.
+    discriminate.
+(* Pget *)
+  - simpl. destruct rs0; subst; try discriminate.
+    all: simpl; auto.
+  - simpl. destruct rd; subst; try discriminate.
+    all: simpl; auto.
+Qed.
+
+Lemma forward_simu_body_stuck:
+  forall bdy ge fn rs m s,
+  Ge = Genv ge fn ->
+  exec_body ge bdy rs m = Stuck ->
+  match_states (State rs m) s ->
+  exec Ge (trans_body bdy) s = None.
+Proof.
+  induction bdy.
+  - simpl. discriminate.
+  - intros. simpl trans_body. simpl in H0.
+    destruct (exec_basic_instr _ _ _ _) eqn:EBI.
+    + exploit exec_basic_instr_next_exec; eauto. intros (s' & EXEGEB & MS'). rewrite EXEGEB. eapply IHbdy; eauto.
+    + cutrewrite (trans_basic a :: trans_body bdy = (trans_basic a :: nil) ++ trans_body bdy); try reflexivity. apply exec_app_none.
+      eapply forward_simu_basic_instr_stuck; eauto.
+Qed.
+
+
+Lemma forward_simu_exit_stuck:
+  forall ex ge fn rs m s,
+  Ge = Genv ge fn ->
+  exec_control ge fn ex rs m = Stuck ->
+  match_states (State rs m) s ->
+  exec Ge (trans_exit ex) s = None.
+Proof.
+  intros. inv H1. destruct ex as [ctl|]; try discriminate.
+  destruct ctl; destruct i; try discriminate; try (simpl; reflexivity).
+(* Pj_l *)
+  - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold goto_label in H0.
+    destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate.
+(* Pcb *)
+  - simpl in *. destruct (cmp_for_btest bt). destruct i.
+    -- destruct o.
+      + unfold eval_branch in H0; unfold eval_branch_deps.
+        pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmp_bool _ _ _); auto.
+        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
+      + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
+    -- destruct o.
+      + unfold eval_branch in H0; unfold eval_branch_deps.
+        pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpl_bool _ _ _); auto.
+        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
+      + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
+(* Pcbu *)
+  - simpl in *. destruct (cmpu_for_btest bt). destruct i.
+    -- destruct o.
+      + rewrite H2. unfold eval_branch in H0; unfold eval_branch_deps.
+        pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpu_bool _ _ _); auto.
+        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
+      + rewrite H2. pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
+    -- destruct o.
+      + rewrite H2. unfold eval_branch in H0; unfold eval_branch_deps.
+        pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmplu_bool _ _ _); auto.
+        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
+      + rewrite H2. pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
+Qed.
+
+
+Theorem forward_simu_stuck:
+  forall rs1 m1 s1' b ge fn,
+    Ge = Genv ge fn ->
+    exec_bblock ge fn b rs1 m1 = Stuck ->
+    match_states (State rs1 m1) s1' ->
+    exec Ge (trans_block b) s1' = None.
+Proof.
+  intros until fn. intros GENV EXECB MS. apply exec_bblock_stuck_nec in EXECB. destruct EXECB.
+  - unfold trans_block. apply exec_app_none. eapply forward_simu_body_stuck; eauto.
+  - destruct H as (rs' & m' & EXEB & EXEC). unfold trans_block. exploit exec_body_next_exec; eauto.
+    intros (s' & EXEGEBODY & MS'). rewrite EXEGEBODY. exploit exec_trans_pcincr_exec; eauto.
+    intros (s'' & EXEGEPC & MS''). rewrite EXEGEPC. eapply forward_simu_exit_stuck; eauto.
+Qed.
+
+
+Lemma state_eq_decomp:
+  forall rs1 m1 rs2 m2, rs1 = rs2 -> m1 = m2 -> State rs1 m1 = State rs2 m2.
+Proof.
+  intros. congruence.
+Qed.
+
+Theorem state_equiv:
+  forall S1 S2 S', match_states S1 S' /\ match_states S2 S' -> S1 = S2.
+Proof.
+  intros. inv H. unfold match_states in H0, H1. destruct S1 as (rs1 & m1). destruct S2 as (rs2 & m2). inv H0. inv H1.
+  apply state_eq_decomp.
+  - apply functional_extensionality. intros. assert (Val (rs1 x) = Val (rs2 x)) by congruence. congruence.
+  - congruence.
+Qed.
+
+
+Axiom bblock_equiv_reduce: 
+  forall p1 p2 ge fn,
+  Ge = Genv ge fn ->
+  L.bblock_equiv Ge (trans_block p1) (trans_block p2) ->
+  Asmblockgenproof0.bblock_equiv ge fn p1 p2. (* FIXME *)
+
+Definition string_of_name (x: P.R.t): ?? pstring := RET (Str ("resname")).
+(*   match x with
+  | xH => RET (Str ("the_mem"))
+  | _ as x => 
+     DO s <~ string_of_Z (Zpos (Pos.pred x)) ;;
+     RET ("R" +; s)
+  end. *)
+
+Definition string_of_op (op: P.op): ?? pstring := RET (Str ("OP")).
+(*   match op with
+  | P.Imm i => 
+     DO s <~ string_of_Z i ;;
+     RET s
+  | P.ARITH ADD => RET (Str "ADD")
+  | P.ARITH SUB => RET (Str "SUB")
+  | P.ARITH MUL => RET (Str "MUL")
+  | P.LOAD => RET (Str "LOAD")
+  | P.STORE => RET (Str "STORE")
+  end. *)
+
+Definition bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool :=
+  if verb then
+    IDT.verb_bblock_eq_test string_of_name string_of_op Ge (trans_block p1) (trans_block p2)
+  else
+    IDT.bblock_eq_test Ge (trans_block p1) (trans_block p2).
+
+Local Hint Resolve IDT.bblock_eq_test_correct bblock_equiv_reduce IDT.verb_bblock_eq_test_correct: wlp.
+
+Theorem bblock_eq_test_correct verb p1 p2 :
+  forall ge fn, Ge = Genv ge fn ->
+  WHEN bblock_eq_test verb p1 p2 ~> b THEN b=true -> Asmblockgenproof0.bblock_equiv ge fn p1 p2.
+Proof.
+  intros ge fn genv_eq.
+  wlp_simplify.
+Admitted. (* FIXME - à voir avec Sylvain *)
+Global Opaque bblock_eq_test.
+Hint Resolve bblock_eq_test_correct: wlp.
+
+Inductive bblock_equiv' (bb bb': L.bblock) :=
+  | bblock_equiv_intro':
+    (forall s, exec Ge bb s = exec Ge bb' s) ->
+    bblock_equiv' bb bb'.
+
+Lemma bblock_equiv'_refl: forall tbb, bblock_equiv' tbb tbb.
+Proof.
+  repeat constructor.
+Qed.
+
+Axiom bblock_equivb: L.bblock -> L.bblock -> bool.
+
+Axiom bblock_equiv'_eq:
+  forall b1 b2,
+  bblock_equivb b1 b2 = true <-> bblock_equiv' b1 b2. (* FIXME - à voir avec Sylvain *)
+
+End SECT.
+
+Extract Constant bblock_equivb => "PostpassSchedulingOracle.bblock_equivb'".
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 6503e5b3..edffd879 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -282,6 +282,30 @@ Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k:
 Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) :=
   Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k.
 
+Definition transl_cond_float32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
+  match ftest_for_cmp cmp with
+  | Normal ft => Pfcompw ft rd r1 r2 ::i k
+  | Reversed ft => Pfcompw ft rd r2 r1 ::i k
+  end.
+
+Definition transl_cond_notfloat32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
+  match notftest_for_cmp cmp with
+  | Normal ft => Pfcompw ft rd r1 r2 ::i k
+  | Reversed ft => Pfcompw ft rd r2 r1 ::i k
+  end.
+
+Definition transl_cond_float64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
+  match ftest_for_cmp cmp with
+  | Normal ft => Pfcompl ft rd r1 r2 ::i k
+  | Reversed ft => Pfcompl ft rd r2 r1 ::i k
+  end.
+
+Definition transl_cond_notfloat64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) :=
+  match notftest_for_cmp cmp with
+  | Normal ft => Pfcompl ft rd r1 r2 ::i k
+  | Reversed ft => Pfcompl ft rd r2 r1 ::i k
+  end.
+
 Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) :=
   match cond, args with
@@ -309,27 +333,19 @@ Definition transl_cond_op
   | Ccompluimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (transl_condimm_int64u c rd r1 n k)
-  | Ccompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompf")
-  | Cnotcompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompf")
-  | Ccompfs _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompfs")
-  | Cnotcompfs _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompfs")
-(*| Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-*)| _, _ =>
+  | Ccompfs c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_float32 c rd r1 r2 k)
+  | Cnotcompfs c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_notfloat32 c rd r1 r2 k)
+  | Ccompf c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_float64 c rd r1 r2 k)
+  | Cnotcompf c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_notfloat64 c rd r1 r2 k)
+  | _, _ =>
       Error(msg "Asmblockgen.transl_cond_op")
 end.
 
@@ -388,13 +404,7 @@ Definition transl_op
       OK (Pmulw rd rs1 rs2 ::i k)
   | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs")
   | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu")
-(*| Omulhs, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhw rd rs1 rs2 :: k)
-  | Omulhu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhuw rd rs1 rs2 :: k)
-*)| Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.")
+  | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.")
       (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pdivw rd rs1 rs2 :: k) *)
   | Odivu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odivu: 32-bits division not supported yet. Please use 64-bits.")
@@ -483,25 +493,7 @@ Definition transl_op
   | Odivlu, _ => Error (msg "Asmblockgen.transl_op: Odivlu")
   | Omodl, _ => Error (msg "Asmblockgen.transl_op: Omodl")
   | Omodlu, _ => Error (msg "Asmblockgen.transl_op: Omodlu")
-(*| Omullhs, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhl rd rs1 rs2 :: k)
-  | Omullhu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhul rd rs1 rs2 :: k)
-  | Odivl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivl rd rs1 rs2 :: k)
-  | Odivlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivul rd rs1 rs2 :: k)
-  | Omodl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Preml rd rs1 rs2 :: k)
-  | Omodlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Premul rd rs1 rs2 :: k)
-*)| Oandl, a1 :: a2 :: nil =>
+  | Oandl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandl rd rs1 rs2 ::i k)
   | Oandlimm n, a1 :: nil =>
@@ -579,18 +571,39 @@ Definition transl_op
   | Osingleofint, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfloatwrnsz rd rs ::i k)
+  | Osingleofintu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfloatuwrnsz rd rs ::i k)
   | Ofloatoflong, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfloatdrnsz rd rs ::i k)
   | Ofloatoflongu, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfloatudrnsz rd rs ::i k)
+  | Ofloatofint, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfloatdrnsz_i32 rd rs ::i k)
+  | Ofloatofintu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfloatudrnsz_i32 rd rs ::i k)
   | Ointofsingle, a1 :: nil =>
       do rd <- ireg_of res; do rs <- freg_of a1;
       OK (Pfixedwrzz rd rs ::i k)
+  | Ointuofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfixeduwrzz rd rs ::i k)
   | Olongoffloat, a1 :: nil =>
       do rd <- ireg_of res; do rs <- freg_of a1;
       OK (Pfixeddrzz rd rs ::i k)
+  | Ointoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfixeddrzz_i32 rd rs ::i k)
+  | Ointuoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfixedudrzz_i32 rd rs ::i k)
+  | Olonguoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfixedudrzz rd rs ::i k)
 
   | Ofloatofsingle, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
@@ -600,34 +613,16 @@ Definition transl_op
       OK (Pfnarrowdw rd rs ::i k)
 
 
-  | Oabsf , _ => Error (msg "Asmblockgen.transl_op: Oabsf")
-  | Oaddf , _ => Error (msg "Asmblockgen.transl_op: Oaddf")
-  | Osubf , _ => Error (msg "Asmblockgen.transl_op: Osubf")
-  | Omulf , _ => Error (msg "Asmblockgen.transl_op: Omulf")
   | Odivf , _ => Error (msg "Asmblockgen.transl_op: Odivf")
-  | Onegfs , _ => Error (msg "Asmblockgen.transl_op: Onegfs")
-  | Oabsfs , _ => Error (msg "Asmblockgen.transl_op: Oabsfs")
-  | Oaddfs , _ => Error (msg "Asmblockgen.transl_op: Oaddfs")
-  | Osubfs , _ => Error (msg "Asmblockgen.transl_op: Osubfs")
-  | Omulfs , _ => Error (msg "Asmblockgen.transl_op: Omulfs")
-  | Odivfs , _ => Error (msg "Asmblockgen.transl_op: Odivfs")
-  | Ofloatoflongu , _ => Error (msg "Asmblockgen.transl_op: Ofloatoflongu")
-  | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong")
-  | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu")
-  | Osingleoffloat , _ => Error (msg "Asmblockgen.transl_op: Osingleoffloat")
-  | Ofloatofsingle , _ => Error (msg "Asmblockgen.transl_op: Ofloatofsingle")
-  | Ointoffloat , _ => Error (msg "Asmblockgen.transl_op: Ointoffloat")
-  | Ointuoffloat , _ => Error (msg "Asmblockgen.transl_op: Ointuoffloat")
-  | Ofloatofint , _ => Error (msg "Asmblockgen.transl_op: Ofloatofint")
-  | Ofloatofintu , _ => Error (msg "Asmblockgen.transl_op: Ofloatofintu")
-  | Ointuofsingle , _ => Error (msg "Asmblockgen.transl_op: Ointuofsingle")
-  | Osingleofintu , _ => Error (msg "Asmblockgen.transl_op: Osingleofintu")
-  | Olonguoffloat , _ => Error (msg "Asmblockgen.transl_op: Olonguoffloat")
-
 
+  (* We use the Splitlong instead for these four conversions *)
+  | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong") 
+  | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu")
   | Olongofsingle , _ => Error (msg "Asmblockgen.transl_op: Olongofsingle")
   | Olonguofsingle , _ => Error (msg "Asmblockgen.transl_op: Olonguofsingle")
 
+
+
   | Ocmp cmp, _ =>
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 9cba8402..1ac9a211 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -950,6 +950,10 @@ Proof.
   - simpl in TIB. monadInv TIB. unfold loadind in EQ. exploreInst; try discriminate.

   - simpl in TIB. unfold transl_op in TIB. exploreInst; try discriminate.

     unfold transl_cond_op in EQ0. exploreInst; try discriminate.

+    unfold transl_cond_float64. exploreInst; try discriminate.

+    unfold transl_cond_notfloat64. exploreInst; try discriminate.

+    unfold transl_cond_float32. exploreInst; try discriminate.

+    unfold transl_cond_notfloat32. exploreInst; try discriminate.

   - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate.

     all: unfold transl_memory_access in EQ0; exploreInst; try discriminate.

   - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate.

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 175eca73..76404257 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -968,6 +968,138 @@ Proof.
   split; intros; Simpl.
 Qed.
 
+Lemma swap_comparison_cmpfs:
+  forall v1 v2 cmp,
+  Val.lessdef (Val.cmpfs cmp v1 v2) (Val.cmpfs (swap_comparison cmp) v2 v1).
+Proof.
+  intros. unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto.
+  rewrite Float32.cmp_swap. auto.
+Qed.
+
+Lemma transl_cond_float32_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_float32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.cmpfs cmp rs#r1 rs#r2) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpfs.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpfs.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_cond_nofloat32_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_notfloat32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpfs_bool cmp (rs r1) (rs r2)))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float32.cmp_ne_eq. auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float32.cmp_ne_eq. simpl. destruct (Float32.cmp Ceq f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float32.cmp Clt f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float32.cmp_swap.
+  destruct (Float32.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float32.cmp_swap.
+  destruct (Float32.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float32.cmp _ _ _); auto.
+Qed.
+
+Lemma swap_comparison_cmpf:
+  forall v1 v2 cmp,
+  Val.lessdef (Val.cmpf cmp v1 v2) (Val.cmpf (swap_comparison cmp) v2 v1).
+Proof.
+  intros. unfold Val.cmpf. unfold Val.cmpf_bool. destruct v1; destruct v2; auto.
+  rewrite Float.cmp_swap. auto.
+Qed.
+
+Lemma transl_cond_float64_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_float64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.cmpf cmp rs#r1 rs#r2) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpf.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpf.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_cond_nofloat64_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_notfloat64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpf_bool cmp (rs r1) (rs r2)))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros. destruct cmp; simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float.cmp_ne_eq. auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float.cmp_ne_eq. simpl. destruct (Float.cmp Ceq f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float.cmp Clt f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float.cmp_swap.
+  destruct (Float.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float.cmp_swap.
+  destruct (Float.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float.cmp _ _ _); auto.
+Qed.
+
 Lemma transl_cond_op_correct:
   forall cond rd args k c rs m,
   transl_cond_op cond rd args k = OK c ->
@@ -1003,6 +1135,14 @@ Proof.
   exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. 
   intros (rs' & A & B & C).
   exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmpfloat *) 
+  exploit transl_cond_float64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpnosingle *)
+  exploit transl_cond_nofloat64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpsingle *) 
+  exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpnosingle *)
+  exploit transl_cond_nofloat32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
 Qed.
 
 (*
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 1b56d3ab..fa0ebfe6 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -12,6 +12,7 @@
 
 Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
+Require Import Asmblockdeps Asmblockgenproof0.
 
 Local Open Scope error_monad_scope.
 
@@ -21,555 +22,467 @@ Axiom schedule: bblock -> list bblock.
 
 Extract Constant schedule => "PostpassSchedulingOracle.schedule".
 
-(** Specification of the "coming soon" Asmblockdeps.v *)
-Inductive bblock_equiv (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=

-  | bblock_equiv_intro:

-      (forall rs m,

-      exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m) ->

-      bblock_equiv ge f bb bb'.

-

-Axiom state': Type.

-Definition outcome' := option state'.

-

-Axiom bblock': Type.

-Extract Constant bblock' => "PostpassSchedulingOracle.bblock'". (* FIXME *)

-Axiom exec': genv -> function -> bblock' -> state' -> outcome'.

-Axiom match_states: state -> state' -> Prop. 

-Axiom trans_block: bblock -> bblock'.

-Extract Constant trans_block => "PostpassSchedulingOracle.trans_block". (* FIXME *)

-Axiom trans_state: state -> state'.

-

-Axiom trans_state_match: forall S, match_states S (trans_state S).

-

-Inductive bblock_equiv' (ge: Genv.t fundef unit) (f: function) (bb bb': bblock') :=

-  | bblock_equiv_intro':

-      (forall s,

-      exec' ge f bb s = exec' ge f bb' s) ->

-      bblock_equiv' ge f bb bb'.

-

-Lemma bblock_equiv'_refl: forall ge fn tbb, bblock_equiv' ge fn tbb tbb.

-Proof.

-  repeat constructor.

-Qed.

-

-

-

-Definition exec := exec_bblock.

-

-Axiom forward_simu:

-  forall rs1 m1 rs2 m2 s1' b ge fn,

-    exec ge fn b rs1 m1 = Next rs2 m2 ->

-    match_states (State rs1 m1) s1' ->

-    exists s2',

-       exec' ge fn (trans_block b) s1' = Some s2'

-    /\ match_states (State rs2 m2) s2'.

-

-Axiom forward_simu_stuck:

-  forall rs1 m1 s1' b ge fn,

-    exec ge fn b rs1 m1 = Stuck ->

-    match_states (State rs1 m1) s1' ->

-    exec' ge fn (trans_block b) s1' = None.

-

-Axiom trans_block_reverse_stuck:

-  forall ge fn b rs m s',

-  exec' ge fn (trans_block b) s' = None ->

-  match_states (State rs m) s' ->

-  exec ge fn b rs m = Stuck.

-

-Axiom state_equiv:

-  forall S1 S2 S', match_states S1 S' /\ match_states S2 S' -> S1 = S2.

-

-

-(* TODO - replace it by the actual bblock_equivb' *)

-Axiom bblock_equivb': bblock' -> bblock' -> bool.

-Extract Constant bblock_equivb' => "PostpassSchedulingOracle.bblock_equivb'". (* FIXME *)

-

-Axiom bblock_equiv'_eq:

-  forall ge fn b1 b2,

-  bblock_equivb' b1 b2 = true <-> bblock_equiv' ge fn b1 b2.

-

-Lemma bblock_equivb'_refl: forall tbb, bblock_equivb' tbb tbb = true.

-Proof.

-  intros. rewrite bblock_equiv'_eq. apply bblock_equiv'_refl.

-  Unshelve. (* FIXME - problem of Genv and function *)

-Admitted.

-

-

-Lemma trans_equiv_stuck:

-  forall b1 b2 ge fn rs m,

-  bblock_equiv' ge fn (trans_block b1) (trans_block b2) ->

-  (exec ge fn b1 rs m = Stuck <-> exec ge fn b2 rs m = Stuck).

-Proof.

-  intros. inv H.

-  pose (trans_state_match (State rs m)).

-  split.

-  - intros. eapply forward_simu_stuck in H; eauto. rewrite H0 in H. eapply trans_block_reverse_stuck; eassumption.

-  - intros. eapply forward_simu_stuck in H; eauto. rewrite <- H0 in H. eapply trans_block_reverse_stuck; eassumption.

-Qed.

-

-

-

-Lemma bblock_equiv'_comm:

-  forall ge fn b1 b2,

-  bblock_equiv' ge fn b1 b2 <-> bblock_equiv' ge fn b2 b1.

-Proof.

-  intros. repeat constructor. all: inv H; congruence.

-Qed.

-

-Theorem trans_exec:

-  forall b1 b2 ge f, bblock_equiv' ge f (trans_block b1) (trans_block b2) -> bblock_equiv ge f b1 b2.

-Proof.

-  repeat constructor. intros rs1 m1.

-  destruct (exec_bblock _ _ b1 _ _) as [rs2 m2|] eqn:EXEB; destruct (exec_bblock _ _ b2 _ _) as [rs3 m3|] eqn:EXEB2; auto.

-  - pose (trans_state_match (State rs1 m1)).

-    exploit forward_simu.

-      eapply EXEB.

-      eapply m.

-    intros (s2' & EXEB' & MS).

-    exploit forward_simu.

-      eapply EXEB2.

-      eapply m.

-    intros (s3' & EXEB'2 & MS2). inv H.

-    rewrite H0 in EXEB'. rewrite EXEB'2 in EXEB'. inv EXEB'.

-    exploit (state_equiv (State rs2 m2) (State rs3 m3) s2'). eauto.

-    congruence.

-  - rewrite trans_equiv_stuck in EXEB2. 2: eapply bblock_equiv'_comm; eauto. unfold exec in EXEB2. rewrite EXEB2 in EXEB. discriminate.

-  - rewrite trans_equiv_stuck in EXEB; eauto. unfold exec in EXEB. rewrite EXEB in EXEB2. discriminate.

-Qed.

-

-

-

-(* Lemmas necessary for defining concat_all *)

-Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil.

-Proof.

-  intros. destruct l; simpl.

-  - contradiction.

-  - discriminate.

-Qed.

-

-Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil.

-Proof.

-  destruct l.

-  - intros. simpl; auto.

-  - intros. rewrite <- app_comm_cons. discriminate.

-Qed.

-

-

-

-Definition check_size bb :=

-  if zlt Ptrofs.max_unsigned (size bb)

-    then Error (msg "PostpassSchedulingproof.check_size")

-  else OK tt.

-

-Program Definition concat2 (bb bb': bblock) : res bblock :=

-  do ch <- check_size bb;

-  do ch' <- check_size bb';

-  match (exit bb) with

-  | None => 

-      match (header bb') with

-      | nil => 

-          match (exit bb') with 

-          | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone")

-          | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |}

-          end

-      | _ => Error (msg "PostpassSchedulingproof.concat2")

-      end

-  | _ => Error (msg "PostpassSchedulingproof.concat2")

-  end.

-Next Obligation.

-  apply wf_bblock_refl. constructor.

-  - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *.

-    apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF.

-    inversion_clear WF'. inversion_clear WF. clear H1 H3.

-    inversion H2; inversion H0.

-    + left. apply app_nonil. auto.

-    + right. auto.

-    + left. apply app_nonil2. auto.

-    + right. auto.

-  - unfold builtin_alone. intros. rewrite H0 in H.

-    assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))).

-    apply (H ef args res). contradict H1. auto.

-Defined.

-

-Lemma concat2_zlt_size:

-  forall a b bb,

-  concat2 a b = OK bb ->

-     size a <= Ptrofs.max_unsigned

-  /\ size b <= Ptrofs.max_unsigned.

-Proof.

-  intros. monadInv H.

-  split.

-  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.

-  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.

-Qed.

-

-Lemma concat2_noexit:

-  forall a b bb,

-  concat2 a b = OK bb ->

-  exit a = None.

-Proof.

-  intros. destruct a as [hd bdy ex WF]; simpl in *.

-  destruct ex as [e|]; simpl in *; auto.

-  unfold concat2 in H. simpl in H. monadInv H.

-Qed.

-

-Lemma concat2_decomp:

-  forall a b bb,

-  concat2 a b = OK bb ->

-     body bb = body a ++ body b

-  /\ exit bb = exit b.

-Proof.

-  intros. exploit concat2_noexit; eauto. intros.

-  destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *.

-  subst exa.

-  unfold concat2 in H; simpl in H.

-  destruct hdb.

-  - destruct exb.

-    + destruct c.

-      * destruct i. monadInv H.

-      * monadInv H. split; auto.

-    + monadInv H. split; auto.

-  - monadInv H.

-Qed.

-

-Lemma concat2_size:

-  forall a b bb, concat2 a b = OK bb -> size bb = size a + size b.

-Proof.

-  intros. unfold concat2 in H.

-  destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *.

-  destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2).

-  - destruct c.

-    + destruct i; try (monadInv EQ2).

-    + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity.

-  - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity.

-Qed.

-

-Lemma concat2_header:

-  forall bb bb' tbb,

-  concat2 bb bb' = OK tbb -> header bb = header tbb.

-Proof.

-  intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *.

-  unfold concat2 in H. simpl in H. monadInv H.

-  destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'.

-  - destruct c.

-    + destruct i; discriminate.

-    + congruence.

-  - congruence.

-Qed.

-

-Lemma concat2_no_header_in_middle:

-  forall bb bb' tbb,

-  concat2 bb bb' = OK tbb ->

-  header bb' = nil.

-Proof.

-  intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *.

-  unfold concat2 in H. simpl in H. monadInv H.

-  destruct ex; try discriminate. destruct hd'; try discriminate. reflexivity.

-Qed.

-

-

-

-Fixpoint concat_all (lbb: list bblock) : res bblock :=

-  match lbb with

-  | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")

-  | bb::nil => OK bb

-  | bb::lbb =>

-      do bb' <- concat_all lbb;

-      concat2 bb bb'

-  end.

-

-Lemma concat_all_size :

-  forall lbb a bb bb',

-  concat_all (a :: lbb) = OK bb ->

-  concat_all lbb = OK bb' ->

-  size bb = size a + size bb'.

-Proof.

-  intros. unfold concat_all in H. fold concat_all in H.

-  destruct lbb; try discriminate.

-  monadInv H. rewrite H0 in EQ. inv EQ.

-  apply concat2_size. assumption.

-Qed.

-

-Lemma concat_all_header:

-  forall lbb bb tbb,

-  concat_all (bb::lbb) = OK tbb -> header bb = header tbb.

-Proof.

-  destruct lbb.

-  - intros. simpl in H. congruence.

-  - intros. simpl in H. destruct lbb.

-    + inv H. eapply concat2_header; eassumption.

-    + monadInv H. eapply concat2_header; eassumption.

-Qed.

-

-Lemma concat_all_no_header_in_middle:

-  forall lbb tbb,

-  concat_all lbb = OK tbb ->

-  Forall (fun b => header b = nil) (tail lbb).

-Proof.

-  induction lbb; intros; try constructor.

-  simpl. simpl in H. destruct lbb.

-  - constructor.

-  - monadInv H. simpl tl in IHlbb. constructor.

-    + apply concat2_no_header_in_middle in EQ0. apply concat_all_header in EQ. congruence.

-    + apply IHlbb in EQ. assumption.

-Qed.

-

-

-

-Definition verify_schedule (bb bb' : bblock) : res unit :=

-  match (bblock_equivb' (trans_block bb) (trans_block bb')) with

-  | true => OK tt

-  | false => Error (msg "PostpassScheduling.verify_schedule")

-  end.

-

-Lemma verify_schedule_refl:

-  forall bb, verify_schedule bb bb = OK tt.

-Proof.

-  intros. unfold verify_schedule. rewrite bblock_equivb'_refl. reflexivity.

-Qed.

-

-

-

-Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").

-

-Lemma verify_size_size:

-  forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb.

-Proof.

-  intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate.

-  apply Z.eqb_eq. assumption.

-Qed.

-

-

-

-Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.

-Next Obligation.

-  destruct bb; simpl. assumption.

-Defined.

-

-Lemma no_header_size:

-  forall bb, size (no_header bb) = size bb.

-Proof.

-  intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity.

-Qed.

-

-Axiom trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb.

-

-Lemma verify_schedule_no_header:

-  forall bb bb',

-  verify_schedule (no_header bb) bb' = verify_schedule bb bb'.

-Proof.

-  intros. unfold verify_schedule. rewrite trans_block_noheader_inv. reflexivity.

-Qed.

-

-

-

-Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.

-Next Obligation.

-  destruct bb; simpl. assumption.

-Defined.

-

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

-

-Lemma stick_header_size:

-  forall h bb, size (stick_header h bb) = size bb.

-Proof.

-  intros. destruct bb. unfold stick_header. simpl. reflexivity.

-Qed.

-

-Lemma stick_header_no_header:

-  forall bb, stick_header (header bb) (no_header bb) = bb.

-Proof.

-  intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity.

-Qed.

-

-Lemma stick_header_verify_schedule:

-  forall hd bb' hbb' bb,

-  stick_header hd bb' = hbb' ->

-  verify_schedule bb bb' = verify_schedule bb hbb'.

-Proof.

-  intros. unfold verify_schedule. rewrite <- H. rewrite trans_block_header_inv. reflexivity.

-Qed.

-

-Lemma check_size_stick_header:

-  forall bb hd,

-  check_size bb = check_size (stick_header hd bb).

-Proof.

-  intros. unfold check_size. rewrite stick_header_size. reflexivity.

-Qed.

-

-Lemma stick_header_concat2:

-  forall bb bb' hd tbb,

-  concat2 bb bb' = OK tbb ->

-  concat2 (stick_header hd bb) bb' = OK (stick_header hd tbb).

-Proof.

-  intros. monadInv H. erewrite check_size_stick_header in EQ.

-  unfold concat2. rewrite EQ. rewrite EQ1. simpl.

-  destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *.

-  destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'.

-  - destruct c.

-    + destruct i. discriminate.

-    + inv EQ2. unfold stick_header; simpl. reflexivity.

-  - inv EQ2. unfold stick_header; simpl. reflexivity.

-Qed.

-

-Lemma stick_header_concat_all:

-  forall bb c tbb hd,

-  concat_all (bb :: c) = OK tbb ->

-  concat_all (stick_header hd bb :: c) = OK (stick_header hd tbb).

-Proof.

-  intros. simpl in *. destruct c; try congruence.

-  monadInv H. rewrite EQ. simpl.

-  apply stick_header_concat2. assumption.

-Qed.

-

-

-

-Definition stick_header_code (h : list label) (lbb : list bblock) :=

-  match (head lbb) with

-  | None => Error (msg "PostpassScheduling.stick_header: empty schedule")

-  | Some fst => OK ((stick_header h fst) :: tail lbb)

-  end.

-

-Lemma stick_header_code_no_header:

-  forall bb c,

-  stick_header_code (header bb) (no_header bb :: c) = OK (bb :: c).

-Proof.

-  intros. unfold stick_header_code. simpl. rewrite stick_header_no_header. reflexivity.

-Qed.

-

-Lemma hd_tl_size:

-  forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb).

-Proof.

-  destruct lbb.

-  - intros. simpl in H. discriminate.

-  - intros. simpl in H. inv H. simpl. reflexivity.

-Qed.

-

-Lemma stick_header_code_size:

-  forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'.

-Proof.

-  intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate.

-  inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto.

-Qed.

-

-Lemma stick_header_code_no_header_in_middle:

-  forall c h lbb,

-  stick_header_code h c = OK lbb ->

-  Forall (fun b => header b = nil) (tl c) ->

-  Forall (fun b => header b = nil) (tl lbb).

-Proof.

-  destruct c; intros.

-  - unfold stick_header_code in H. simpl in H. discriminate.

-  - unfold stick_header_code in H. simpl in H. inv H. simpl in H0.

-    simpl. assumption.

-Qed.

-

-Lemma stick_header_code_concat_all:

-  forall hd lbb hlbb tbb,

-  stick_header_code hd lbb = OK hlbb ->

-  concat_all lbb = OK tbb ->

-  exists htbb,

-     concat_all hlbb = OK htbb

-  /\ stick_header hd tbb = htbb.

-Proof.

-  intros. exists (stick_header hd tbb). split; auto.

-  destruct lbb.

-  - unfold stick_header_code in H. simpl in H. discriminate.

-  - unfold stick_header_code in H. simpl in H. inv H.

-    apply stick_header_concat_all. assumption.

-Qed.

-

-

-

-Definition do_schedule (bb: bblock) : list bblock :=

-  if (Z.eqb (size bb) 1) then bb::nil else schedule bb.

-

-Definition verified_schedule (bb : bblock) : res (list bblock) :=

-  let bb' := no_header bb in

-  let lbb := do_schedule bb' in

-  do tbb <- concat_all lbb;

-  do sizecheck <- verify_size bb lbb;

-  do schedcheck <- verify_schedule bb' tbb;

-  stick_header_code (header bb) lbb.

-

-Lemma verified_schedule_size:

-  forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.

-Proof.

-  intros. monadInv H. erewrite <- stick_header_code_size; eauto.

-  apply verify_size_size.

-  destruct x0; try discriminate. assumption.

-Qed.

-

-Lemma verified_schedule_single_inst:

-  forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil).

-Proof.

-  intros. unfold verified_schedule.

-  unfold do_schedule. rewrite no_header_size. rewrite H. simpl.

-  unfold verify_size. simpl. rewrite no_header_size. rewrite Z.add_0_r. cutrewrite (size bb =? size bb = true). rewrite verify_schedule_refl. simpl.

-  apply stick_header_code_no_header.

-  rewrite H. reflexivity.

-Qed.

-

-Lemma verified_schedule_no_header_in_middle:

-  forall lbb bb,

-  verified_schedule bb = OK lbb ->

-     Forall (fun b => header b = nil) (tail lbb).

-Proof.

-  intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto.

-  eapply concat_all_no_header_in_middle. eassumption.

-Qed.

-

-Lemma verified_schedule_header:

-  forall bb tbb lbb,

-  verified_schedule bb = OK (tbb :: lbb) ->

-     header bb = header tbb

-  /\ Forall (fun b => header b = nil) lbb.

-Proof.

-  intros. split.

-  - monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3.

-    simpl. reflexivity.

-  - apply verified_schedule_no_header_in_middle in H. assumption.

-Qed.

-

-Theorem verified_schedule_correct:

-  forall ge f bb lbb,

-  verified_schedule bb = OK lbb ->

-  exists tbb, 

-     concat_all lbb = OK tbb

-  /\ bblock_equiv ge f bb tbb.

-Proof.

-  intros. monadInv H.

-  exploit stick_header_code_concat_all; eauto.

-  intros (tbb & CONC & STH).

-  exists tbb. split; auto.

-  rewrite verify_schedule_no_header in EQ0. erewrite stick_header_verify_schedule in EQ0; eauto.

-  apply trans_exec. apply bblock_equiv'_eq. unfold verify_schedule in EQ0.

-  destruct (bblock_equivb' _ _); auto; try discriminate.

-Qed.

-

-

-

-Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=

-  match lbb with

-  | nil => OK nil

-  | (cons bb lbb) =>

-      do tlbb <- transf_blocks lbb;

-      do tbb <- verified_schedule bb;

-      OK (tbb ++ tlbb)

-  end.

-

-Definition transl_function (f: function) : res function :=

-  do lb <- transf_blocks (fn_blocks f); 

-  OK (mkfunction (fn_sig f) lb).

-

-Definition transf_function (f: function) : res function :=

-  do tf <- transl_function f;

-  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))

-  then Error (msg "code size exceeded")

-  else OK tf.

-

-Definition transf_fundef (f: fundef) : res fundef :=

-  transf_partial_fundef transf_function f.

-

-Definition transf_program (p: program) : res program :=

-  transform_partial_program transf_fundef p.
\ No newline at end of file
+Definition state' := L.mem.
+Definition outcome' := option state'.
+
+Definition bblock' := L.bblock.
+
+Definition exec' := L.run.
+
+Definition exec := exec_bblock.
+
+Definition bblock_equivb' := bblock_equivb.
+
+Lemma bblock_equivb'_refl (ge: Genv.t fundef unit) (fn: function): forall tbb, bblock_equivb' tbb tbb = true.
+Proof.
+  intros. rewrite bblock_equiv'_eq. apply bblock_equiv'_refl.
+  Unshelve. (* FIXME - problem of Genv and function *)
+  constructor; auto.
+Qed.
+
+Lemma trans_equiv_stuck:
+  forall b1 b2 ge fn rs m,
+  bblock_equiv' (P.Genv ge fn) (trans_block b1) (trans_block b2) ->
+  (exec ge fn b1 rs m = Stuck <-> exec ge fn b2 rs m = Stuck).
+Proof.
+  intros. inv H.
+  pose (trans_state_match (State rs m)).
+  split.
+  - intros. eapply forward_simu_stuck in H; eauto. rewrite H0 in H. eapply trans_block_reverse_stuck.
+      reflexivity. eassumption. eassumption.
+  - intros. eapply forward_simu_stuck in H; eauto. rewrite <- H0 in H. eapply trans_block_reverse_stuck.
+      reflexivity. eassumption. eassumption.
+Qed.
+
+
+Lemma bblock_equiv'_comm:
+  forall ge fn b1 b2,
+  bblock_equiv' (P.Genv ge fn) b1 b2 <-> bblock_equiv' (P.Genv ge fn) b2 b1.
+Proof.
+  intros. repeat constructor. all: inv H; congruence.
+Qed.
+
+Theorem trans_exec:
+  forall b1 b2 ge f, bblock_equiv' (P.Genv ge f) (trans_block b1) (trans_block b2) -> bblock_equiv ge f b1 b2.
+Proof.
+  repeat constructor. intros rs1 m1.
+  destruct (exec_bblock _ _ b1 _ _) as [rs2 m2|] eqn:EXEB; destruct (exec_bblock _ _ b2 _ _) as [rs3 m3|] eqn:EXEB2; auto.
+  - pose (trans_state_match (State rs1 m1)).
+    exploit forward_simu.
+      reflexivity.
+      eapply EXEB.
+      eapply m.
+    intros (s2' & EXEB' & MS).
+    exploit forward_simu.
+      reflexivity.
+      eapply EXEB2.
+      eapply m.
+    intros (s3' & EXEB'2 & MS2). inv H.
+    rewrite H0 in EXEB'. rewrite EXEB'2 in EXEB'. inv EXEB'.
+    exploit (state_equiv (State rs2 m2) (State rs3 m3) s2'). eauto.
+    congruence.
+  - rewrite trans_equiv_stuck in EXEB2. 2: eapply bblock_equiv'_comm; eauto. unfold exec in EXEB2. rewrite EXEB2 in EXEB. discriminate.
+  - rewrite trans_equiv_stuck in EXEB; eauto. unfold exec in EXEB. rewrite EXEB in EXEB2. discriminate.
+Qed.
+
+
+
+(* Lemmas necessary for defining concat_all *)
+Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil.
+Proof.
+  intros. destruct l; simpl.
+  - contradiction.
+  - discriminate.
+Qed.
+
+Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil.
+Proof.
+  destruct l.
+  - intros. simpl; auto.
+  - intros. rewrite <- app_comm_cons. discriminate.
+Qed.
+
+
+
+Definition check_size bb :=
+  if zlt Ptrofs.max_unsigned (size bb)
+    then Error (msg "PostpassSchedulingproof.check_size")
+  else OK tt.
+
+Program Definition concat2 (bb bb': bblock) : res bblock :=
+  do ch <- check_size bb;
+  do ch' <- check_size bb';
+  match (exit bb) with
+  | None => 
+      match (header bb') with
+      | nil => 
+          match (exit bb') with 
+          | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone")
+          | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |}
+          end
+      | _ => Error (msg "PostpassSchedulingproof.concat2")
+      end
+  | _ => Error (msg "PostpassSchedulingproof.concat2")
+  end.
+Next Obligation.
+  apply wf_bblock_refl. constructor.
+  - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *.
+    apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF.
+    inversion_clear WF'. inversion_clear WF. clear H1 H3.
+    inversion H2; inversion H0.
+    + left. apply app_nonil. auto.
+    + right. auto.
+    + left. apply app_nonil2. auto.
+    + right. auto.
+  - unfold builtin_alone. intros. rewrite H0 in H.
+    assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))).
+    apply (H ef args res). contradict H1. auto.
+Defined.
+
+Lemma concat2_zlt_size:
+  forall a b bb,
+  concat2 a b = OK bb ->
+     size a <= Ptrofs.max_unsigned
+  /\ size b <= Ptrofs.max_unsigned.
+Proof.
+  intros. monadInv H.
+  split.
+  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.
+  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.
+Qed.
+
+Lemma concat2_noexit:
+  forall a b bb,
+  concat2 a b = OK bb ->
+  exit a = None.
+Proof.
+  intros. destruct a as [hd bdy ex WF]; simpl in *.
+  destruct ex as [e|]; simpl in *; auto.
+  unfold concat2 in H. simpl in H. monadInv H.
+Qed.
+
+Lemma concat2_decomp:
+  forall a b bb,
+  concat2 a b = OK bb ->
+     body bb = body a ++ body b
+  /\ exit bb = exit b.
+Proof.
+  intros. exploit concat2_noexit; eauto. intros.
+  destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *.
+  subst exa.
+  unfold concat2 in H; simpl in H.
+  destruct hdb.
+  - destruct exb.
+    + destruct c.
+      * destruct i. monadInv H.
+      * monadInv H. split; auto.
+    + monadInv H. split; auto.
+  - monadInv H.
+Qed.
+
+Lemma concat2_size:
+  forall a b bb, concat2 a b = OK bb -> size bb = size a + size b.
+Proof.
+  intros. unfold concat2 in H.
+  destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *.
+  destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2).
+  - destruct c.
+    + destruct i; try (monadInv EQ2).
+    + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity.
+  - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity.
+Qed.
+
+Lemma concat2_header:
+  forall bb bb' tbb,
+  concat2 bb bb' = OK tbb -> header bb = header tbb.
+Proof.
+  intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *.
+  unfold concat2 in H. simpl in H. monadInv H.
+  destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'.
+  - destruct c.
+    + destruct i; discriminate.
+    + congruence.
+  - congruence.
+Qed.
+
+Lemma concat2_no_header_in_middle:
+  forall bb bb' tbb,
+  concat2 bb bb' = OK tbb ->
+  header bb' = nil.
+Proof.
+  intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *.
+  unfold concat2 in H. simpl in H. monadInv H.
+  destruct ex; try discriminate. destruct hd'; try discriminate. reflexivity.
+Qed.
+
+
+
+Fixpoint concat_all (lbb: list bblock) : res bblock :=
+  match lbb with
+  | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")
+  | bb::nil => OK bb
+  | bb::lbb =>
+      do bb' <- concat_all lbb;
+      concat2 bb bb'
+  end.
+
+Lemma concat_all_size :
+  forall lbb a bb bb',
+  concat_all (a :: lbb) = OK bb ->
+  concat_all lbb = OK bb' ->
+  size bb = size a + size bb'.
+Proof.
+  intros. unfold concat_all in H. fold concat_all in H.
+  destruct lbb; try discriminate.
+  monadInv H. rewrite H0 in EQ. inv EQ.
+  apply concat2_size. assumption.
+Qed.
+
+Lemma concat_all_header:
+  forall lbb bb tbb,
+  concat_all (bb::lbb) = OK tbb -> header bb = header tbb.
+Proof.
+  destruct lbb.
+  - intros. simpl in H. congruence.
+  - intros. simpl in H. destruct lbb.
+    + inv H. eapply concat2_header; eassumption.
+    + monadInv H. eapply concat2_header; eassumption.
+Qed.
+
+Lemma concat_all_no_header_in_middle:
+  forall lbb tbb,
+  concat_all lbb = OK tbb ->
+  Forall (fun b => header b = nil) (tail lbb).
+Proof.
+  induction lbb; intros; try constructor.
+  simpl. simpl in H. destruct lbb.
+  - constructor.
+  - monadInv H. simpl tl in IHlbb. constructor.
+    + apply concat2_no_header_in_middle in EQ0. apply concat_all_header in EQ. congruence.
+    + apply IHlbb in EQ. assumption.
+Qed.
+
+
+
+Definition verify_schedule (bb bb' : bblock) : res unit :=
+  match (bblock_equivb' (trans_block bb) (trans_block bb')) with
+  | true => OK tt
+  | false => Error (msg "PostpassScheduling.verify_schedule")
+  end.
+
+Lemma verify_schedule_refl (ge: Genv.t fundef unit) (fn: function):
+  forall bb, verify_schedule bb bb = OK tt.
+Proof.
+  intros. unfold verify_schedule. rewrite bblock_equivb'_refl. reflexivity. all: auto.
+Qed.
+
+
+
+Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").
+
+Lemma verify_size_size:
+  forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb.
+Proof.
+  intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate.
+  apply Z.eqb_eq. assumption.
+Qed.
+
+Lemma verify_schedule_no_header:
+  forall bb bb',
+  verify_schedule (no_header bb) bb' = verify_schedule bb bb'.
+Proof.
+  intros. unfold verify_schedule. rewrite trans_block_noheader_inv. reflexivity.
+Qed.
+
+
+Lemma stick_header_verify_schedule:
+  forall hd bb' hbb' bb,
+  stick_header hd bb' = hbb' ->
+  verify_schedule bb bb' = verify_schedule bb hbb'.
+Proof.
+  intros. unfold verify_schedule. rewrite <- H. rewrite trans_block_header_inv. reflexivity.
+Qed.
+
+Lemma check_size_stick_header:
+  forall bb hd,
+  check_size bb = check_size (stick_header hd bb).
+Proof.
+  intros. unfold check_size. rewrite stick_header_size. reflexivity.
+Qed.
+
+Lemma stick_header_concat2:
+  forall bb bb' hd tbb,
+  concat2 bb bb' = OK tbb ->
+  concat2 (stick_header hd bb) bb' = OK (stick_header hd tbb).
+Proof.
+  intros. monadInv H. erewrite check_size_stick_header in EQ.
+  unfold concat2. rewrite EQ. rewrite EQ1. simpl.
+  destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *.
+  destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'.
+  - destruct c.
+    + destruct i. discriminate.
+    + inv EQ2. unfold stick_header; simpl. reflexivity.
+  - inv EQ2. unfold stick_header; simpl. reflexivity.
+Qed.
+
+Lemma stick_header_concat_all:
+  forall bb c tbb hd,
+  concat_all (bb :: c) = OK tbb ->
+  concat_all (stick_header hd bb :: c) = OK (stick_header hd tbb).
+Proof.
+  intros. simpl in *. destruct c; try congruence.
+  monadInv H. rewrite EQ. simpl.
+  apply stick_header_concat2. assumption.
+Qed.
+
+
+
+Definition stick_header_code (h : list label) (lbb : list bblock) :=
+  match (head lbb) with
+  | None => Error (msg "PostpassScheduling.stick_header: empty schedule")
+  | Some fst => OK ((stick_header h fst) :: tail lbb)
+  end.
+
+Lemma stick_header_code_no_header:
+  forall bb c,
+  stick_header_code (header bb) (no_header bb :: c) = OK (bb :: c).
+Proof.
+  intros. unfold stick_header_code. simpl. rewrite stick_header_no_header. reflexivity.
+Qed.
+
+Lemma hd_tl_size:
+  forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb).
+Proof.
+  destruct lbb.
+  - intros. simpl in H. discriminate.
+  - intros. simpl in H. inv H. simpl. reflexivity.
+Qed.
+
+Lemma stick_header_code_size:
+  forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'.
+Proof.
+  intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate.
+  inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto.
+Qed.
+
+Lemma stick_header_code_no_header_in_middle:
+  forall c h lbb,
+  stick_header_code h c = OK lbb ->
+  Forall (fun b => header b = nil) (tl c) ->
+  Forall (fun b => header b = nil) (tl lbb).
+Proof.
+  destruct c; intros.
+  - unfold stick_header_code in H. simpl in H. discriminate.
+  - unfold stick_header_code in H. simpl in H. inv H. simpl in H0.
+    simpl. assumption.
+Qed.
+
+Lemma stick_header_code_concat_all:
+  forall hd lbb hlbb tbb,
+  stick_header_code hd lbb = OK hlbb ->
+  concat_all lbb = OK tbb ->
+  exists htbb,
+     concat_all hlbb = OK htbb
+  /\ stick_header hd tbb = htbb.
+Proof.
+  intros. exists (stick_header hd tbb). split; auto.
+  destruct lbb.
+  - unfold stick_header_code in H. simpl in H. discriminate.
+  - unfold stick_header_code in H. simpl in H. inv H.
+    apply stick_header_concat_all. assumption.
+Qed.
+
+
+
+Definition do_schedule (bb: bblock) : list bblock :=
+  if (Z.eqb (size bb) 1) then bb::nil else schedule bb.
+
+Definition verified_schedule (bb : bblock) : res (list bblock) :=
+  let bb' := no_header bb in
+  let lbb := do_schedule bb' in
+  do tbb <- concat_all lbb;
+  do sizecheck <- verify_size bb lbb;
+  do schedcheck <- verify_schedule bb' tbb;
+  stick_header_code (header bb) lbb.
+
+Lemma verified_schedule_size:
+  forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.
+Proof.
+  intros. monadInv H. erewrite <- stick_header_code_size; eauto.
+  apply verify_size_size.
+  destruct x0; try discriminate. assumption.
+Qed.
+
+Lemma verified_schedule_single_inst (ge: Genv.t fundef unit) (fn: function):
+  forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil).
+Proof.
+  intros. unfold verified_schedule.
+  unfold do_schedule. rewrite no_header_size. rewrite H. simpl.
+  unfold verify_size. simpl. rewrite no_header_size. rewrite Z.add_0_r. cutrewrite (size bb =? size bb = true). rewrite verify_schedule_refl. simpl.
+  apply stick_header_code_no_header. all: auto.
+  rewrite H. reflexivity.
+Qed.
+
+Lemma verified_schedule_no_header_in_middle:
+  forall lbb bb,
+  verified_schedule bb = OK lbb ->
+     Forall (fun b => header b = nil) (tail lbb).
+Proof.
+  intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto.
+  eapply concat_all_no_header_in_middle. eassumption.
+Qed.
+
+Lemma verified_schedule_header:
+  forall bb tbb lbb,
+  verified_schedule bb = OK (tbb :: lbb) ->
+     header bb = header tbb
+  /\ Forall (fun b => header b = nil) lbb.
+Proof.
+  intros. split.
+  - monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3.
+    simpl. reflexivity.
+  - apply verified_schedule_no_header_in_middle in H. assumption.
+Qed.
+
+Theorem verified_schedule_correct:
+  forall ge f bb lbb,
+  verified_schedule bb = OK lbb ->
+  exists tbb, 
+     concat_all lbb = OK tbb
+  /\ bblock_equiv ge f bb tbb.
+Proof.
+  intros. monadInv H.
+  exploit stick_header_code_concat_all; eauto.
+  intros (tbb & CONC & STH).
+  exists tbb. split; auto.
+  rewrite verify_schedule_no_header in EQ0. erewrite stick_header_verify_schedule in EQ0; eauto.
+  apply trans_exec. apply bblock_equiv'_eq. unfold verify_schedule in EQ0. unfold bblock_equivb' in EQ0.
+  destruct (bblock_equivb _ _); auto; try discriminate.
+Qed.
+
+
+
+Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
+  match lbb with
+  | nil => OK nil
+  | (cons bb lbb) =>
+      do tlbb <- transf_blocks lbb;
+      do tbb <- verified_schedule bb;
+      OK (tbb ++ tlbb)
+  end.
+
+Definition transl_function (f: function) : res function :=
+  do lb <- transf_blocks (fn_blocks f); 
+  OK (mkfunction (fn_sig f) lb).
+
+Definition transf_function (f: function) : res function :=
+  do tf <- transl_function f;
+  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
+  then Error (msg "code size exceeded")
+  else OK tf.
+
+Definition transf_fundef (f: fundef) : res fundef :=
+  transf_partial_fundef transf_function f.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 54a27966..db50e3a5 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -40,14 +40,23 @@ let arith_rr_str = function
   | Pfnarrowdw -> "Pfnarrowdw"
   | Pfwidenlwd -> "Pfwidenlwd"
   | Pfloatwrnsz -> "Pfloatwrnsz"
+  | Pfloatuwrnsz -> "Pfloatuwrnsz"
+  | Pfloatudrnsz_i32 -> "Pfloatudrnsz_i32"
   | Pfloatudrnsz -> "Pfloatudrnsz"
   | Pfloatdrnsz -> "Pfloatdrnsz"
+  | Pfloatdrnsz_i32 -> "Pfloatdrnsz_i32"
   | Pfixedwrzz -> "Pfixedwrzz"
+  | Pfixeduwrzz -> "Pfixeduwrzz"
   | Pfixeddrzz -> "Pfixeddrzz"
+  | Pfixedudrzz -> "Pfixedudrzz"
+  | Pfixeddrzz_i32 -> "Pfixeddrzz_i32"
+  | Pfixedudrzz_i32 -> "Pfixedudrzz_i32"
 
 let arith_rrr_str = function
   | Pcompw it -> "Pcompw"
   | Pcompl it -> "Pcompl"
+  | Pfcompw ft -> "Pfcompw"
+  | Pfcompl ft -> "Pfcompl"
   | Paddw -> "Paddw"
   | Psubw -> "Psubw"
   | Pmulw -> "Pmulw"
@@ -298,6 +307,10 @@ let alu_lite : int array = let resmap = fun r -> match r with
   | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 |  _ -> 0 
   in Array.of_list (List.map resmap resource_names)
 
+let alu_lite_x : int array = let resmap = fun r -> match r with 
+  | "ISSUE" -> 2 | "TINY" -> 1 | "LITE" -> 1 |  _ -> 0 
+  in Array.of_list (List.map resmap resource_names)
+
 let alu_full : int array = let resmap = fun r -> match r with
   | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | "ALU" -> 1 | _ -> 0
   in Array.of_list (List.map resmap resource_names)
@@ -365,7 +378,8 @@ type real_instruction =
   (* FPU *)
   | Fabsd | Fabsw | Fnegw | Fnegd
   | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
-  | Fnarrowdw | Fwidenlwd | Floatwz | Floatdz | Floatudz | Fixedwz | Fixeddz
+  | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz
+  | Fcompw | Fcompd
 
 let ab_inst_to_real = function
   | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw
@@ -374,6 +388,8 @@ let ab_inst_to_real = function
   | "Pandl" | "Pandil" -> Andd
   | "Pcompw" | "Pcompiw" -> Compw
   | "Pcompl" | "Pcompil" -> Compd
+  | "Pfcompw" -> Fcompw
+  | "Pfcompl" -> Fcompd
   | "Pmulw" -> Mulw
   | "Pmull" -> Muld
   | "Porw" | "Poriw" -> Orw
@@ -395,10 +411,17 @@ let ab_inst_to_real = function
   | "Pfnarrowdw" -> Fnarrowdw
   | "Pfwidenlwd" -> Fwidenlwd
   | "Pfloatwrnsz" -> Floatwz
+  | "Pfloatuwrnsz" -> Floatuwz
   | "Pfloatdrnsz" -> Floatdz
+  | "Pfloatdrnsz_i32" -> Floatdz
   | "Pfloatudrnsz" -> Floatudz
+  | "Pfloatudrnsz_i32" -> Floatudz
   | "Pfixedwrzz" -> Fixedwz
+  | "Pfixeduwrzz" -> Fixeduwz
   | "Pfixeddrzz" -> Fixeddz
+  | "Pfixedudrzz" -> Fixedudz
+  | "Pfixeddrzz_i32" -> Fixeddz
+  | "Pfixedudrzz_i32" -> Fixedudz
 
   | "Plb" -> Lbs
   | "Plbu" -> Lbz
@@ -456,6 +479,12 @@ let rec_to_usage r =
   | Compd -> (match encoding with None | Some U6 | Some S10 -> alu_tiny
                                 | Some U27L5 | Some U27L10 -> alu_tiny_x
                                 | Some E27U27L10 -> alu_tiny_y)
+  | Fcompw -> (match encoding with None -> alu_lite
+                                | Some U6 | Some S10 | Some U27L5 -> alu_lite_x
+                                | _ -> raise InvalidEncoding)
+  | Fcompd -> (match encoding with None -> alu_lite
+                                | Some U6 | Some S10 | Some U27L5 -> alu_lite_x
+                                | _ -> raise InvalidEncoding)
   | Make -> (match encoding with Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x 
                           | Some E27U27L10 -> alu_tiny_y 
@@ -469,7 +498,7 @@ let rec_to_usage r =
   | Nop -> alu_nop
   | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
   | Sxwd | Zxwd -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
-  | Fixedwz | Floatwz | Fixeddz | Floatdz | Floatudz -> mau
+  | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 
       (match encoding with None | Some U6 | Some S10 -> lsu_data 
                           | Some U27L5 | Some U27L10 -> lsu_data_x 
@@ -488,9 +517,9 @@ let real_inst_to_latency = function
   | Nop -> 0 (* Only goes through ID *)
   | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
-  | Sxwd | Zxwd
+  | Sxwd | Zxwd | Fcompw | Fcompd
         -> 1
-  | Floatwz | Fixedwz | Floatdz | Floatudz | Fixeddz -> 4
+  | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
   | Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld
   | Sb | Sh | Sw | Sd 
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 2c3b8454..2ecb494d 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -10,675 +10,675 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import Coqlib Errors.

-Require Import Integers Floats AST Linking.

-Require Import Values Memory Events Globalenvs Smallstep.

-Require Import Op Locations Machblock Conventions Asmblock.

-Require Import Asmblockgenproof0.

-Require Import PostpassScheduling.

-Require Import Asmblockgenproof.

-Require Import Axioms.

-

-Local Open Scope error_monad_scope.

-

-Definition match_prog (p tp: Asmblock.program) :=

-  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.

-

-Lemma transf_program_match:

-  forall p tp, transf_program p = OK tp -> match_prog p tp.

-Proof.

-  intros. eapply match_transform_partial_program; eauto.

-Qed.

-

-Remark builtin_body_nil:

-  forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.

-Proof.

-  intros. destruct bb as [hd bdy ex WF]. simpl in *.

-  apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.

-  eapply H1; eauto.

-Qed.

-

-Lemma verified_schedule_builtin_idem:

-  forall bb ef args res lbb,

-  exit bb = Some (PExpand (Pbuiltin ef args res)) ->

-  verified_schedule bb = OK lbb ->

-  lbb = bb :: nil.

-Proof.

-  intros. exploit builtin_body_nil; eauto. intros.

-  rewrite verified_schedule_single_inst in H0.

-  - inv H0. auto.

-  - unfold size. rewrite H. rewrite H1. simpl. auto.

-Qed.

-

-Lemma exec_body_app:

-  forall l l' ge rs m rs'' m'',

-  exec_body ge (l ++ l') rs m = Next rs'' m'' ->

-  exists rs' m',

-       exec_body ge l rs m = Next rs' m'

-    /\ exec_body ge l' rs' m' = Next rs'' m''.

-Proof.

-  induction l.

-  - intros. simpl in H. repeat eexists. auto.

-  - intros. rewrite <- app_comm_cons in H. simpl in H.

-    destruct (exec_basic_instr ge a rs m) eqn:EXEBI.

-    + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).

-      repeat eexists. simpl. rewrite EXEBI. eauto. auto.

-    + discriminate.

-Qed.

-

-Lemma exec_body_pc:

-  forall l ge rs1 m1 rs2 m2,

-  exec_body ge l rs1 m1 = Next rs2 m2 ->

-  rs2 PC = rs1 PC.

-Proof.

-  induction l.

-  - intros. inv H. auto.

-  - intros until m2. intro EXEB.

-    inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.

-    eapply IHl in H0. rewrite H0.

-    erewrite exec_basic_instr_pc; eauto.

-Qed.

-

-Lemma next_eq {A: Type}:

-  forall (rs rs':A) m m',

-  rs = rs' -> m = m' -> Next rs m = Next rs' m'.

-Proof.

-  intros. congruence.

-Qed.

-

-Lemma regset_double_set:

-  forall r1 r2 (rs: regset) v1 v2,

-  r1 <> r2 ->

-  (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).

-Proof.

-  intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).

-  - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.

-  - destruct (preg_eq r r2).

-    + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.

-    + repeat (rewrite Pregmap.gso; auto).

-Qed.

-

-Lemma regset_double_set_id:

-  forall r (rs: regset) v1 v2,

-  (rs # r <- v1 # r <- v2) = (rs # r <- v2).

-Proof.

-  intros. apply functional_extensionality. intros. destruct (preg_eq r x).

-  - subst r. repeat (rewrite Pregmap.gss; auto).

-  - repeat (rewrite Pregmap.gso); auto.

-Qed.

-

-Lemma exec_load_pc_var:

-  forall ge t rs m rd ra ofs rs' m' v,

-  exec_load ge t rs m rd ra ofs = Next rs' m' ->

-  exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

-Proof.

-  intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.

-  destruct (Mem.loadv _ _ _).

-  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.

-  - discriminate.

-Qed.

-

-Lemma exec_store_pc_var:

-  forall ge t rs m rd ra ofs rs' m' v,

-  exec_store ge t rs m rd ra ofs = Next rs' m' ->

-  exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

-Proof.

-  intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.

-  destruct (Mem.storev _ _ _).

-  - inv H. apply next_eq; auto.

-  - discriminate.

-Qed.

-

-Lemma exec_basic_instr_pc_var:

-  forall ge i rs m rs' m' v,

-  exec_basic_instr ge i rs m = Next rs' m' ->

-  exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.

-Proof.

-  intros. unfold exec_basic_instr in *. destruct i.

-  - unfold exec_arith_instr in *. destruct i; destruct i.

-      all: try (exploreInst; inv H; apply next_eq; auto;

-      apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).

-

-      (* Some cases treated seperately because exploreInst destructs too much *)

-      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).

-  - exploreInst; apply exec_load_pc_var; auto.

-  - exploreInst; apply exec_store_pc_var; auto.

-  - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).

-    destruct (Mem.storev _ _ _ _); try discriminate.

-    inv H. apply next_eq; auto. apply functional_extensionality. intros.

-    rewrite (regset_double_set GPR32 PC); try discriminate.

-    rewrite (regset_double_set GPR12 PC); try discriminate.

-    rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity.

-  - repeat (rewrite Pregmap.gso; try discriminate).

-    destruct (Mem.loadv _ _ _); try discriminate.

-    destruct (rs GPR12); try discriminate.

-    destruct (Mem.free _ _ _ _); try discriminate.

-    inv H. apply next_eq; auto.

-    rewrite (regset_double_set GPR32 PC).

-    rewrite (regset_double_set GPR12 PC). reflexivity.

-    all: discriminate.

-  - destruct rs0; try discriminate. inv H. apply next_eq; auto.

-    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.

-  - destruct rd; try discriminate. inv H. apply next_eq; auto.

-    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.

-  - inv H. apply next_eq; auto.

-Qed.

-

-Lemma exec_body_pc_var:

-  forall l ge rs m rs' m' v,

-  exec_body ge l rs m = Next rs' m' ->

-  exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'.

-Proof.

-  induction l.

-  - intros. simpl. simpl in H. inv H. auto.

-  - intros. simpl in *.

-    destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate.

-    erewrite exec_basic_instr_pc_var; eauto.

-Qed.

-

-Lemma pc_set_add:

-  forall rs v r x y,

-  0 <= x <= Ptrofs.max_unsigned ->

-  0 <= y <= Ptrofs.max_unsigned ->

-  rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)).

-Proof.

-  intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0).

-  - subst. repeat (rewrite Pregmap.gss); auto.

-    destruct v; simpl; auto.

-    rewrite Ptrofs.add_assoc.

-    cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto.

-    unfold Ptrofs.add.

-    cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto.

-    repeat (rewrite Ptrofs.unsigned_repr); auto.

-  - repeat (rewrite Pregmap.gso; auto).

-Qed.

-

-Lemma concat2_straight:

-  forall a b bb rs m rs'' m'' f ge,

-  concat2 a b = OK bb ->

-  exec_bblock ge f bb rs m = Next rs'' m'' ->

-  exists rs' m',

-       exec_bblock ge f a rs m = Next rs' m'

-    /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))

-    /\ exec_bblock ge f b rs' m' = Next rs'' m''.

-Proof.

-  intros until ge. intros CONC2 EXEB.

-  exploit concat2_zlt_size; eauto. intros (LTA & LTB).

-  exploit concat2_noexit; eauto. intros EXA.

-  exploit concat2_decomp; eauto. intros. inv H.

-  unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.

-  rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2).

-  repeat eexists.

-    unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.

-    exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.

-    unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto.

-    rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.

-    assert (size bb = size a + size b).

-    { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.

-      repeat (rewrite Nat2Z.inj_add). omega. }

-    clear EXA H0 H1. rewrite H in EXEB.

-    assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }

-    rewrite H0. rewrite <- pc_set_add; auto.

-    exploit AB.size_positive. instantiate (1 := a). intro. omega.

-    exploit AB.size_positive. instantiate (1 := b). intro. omega.

-Qed.

-

-Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :

-  forall a bb rs m lbb rs'' m'', 

-  lbb <> nil ->

-  concat_all (a :: lbb) = OK bb ->

-  exec_bblock ge f bb rs m = Next rs'' m'' ->

-  exists bb' rs' m',

-       concat_all lbb = OK bb'

-    /\ exec_bblock ge f a rs m = Next rs' m'

-    /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))

-    /\ exec_bblock ge f bb' rs' m' = Next rs'' m''.

-Proof.

-  intros until m''. intros Hnonil CONC EXEB.

-  simpl in CONC.

-  destruct lbb as [|b lbb]; try contradiction. clear Hnonil.

-  monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2).

-  exists x. repeat econstructor. all: eauto.

-Qed.

-

-Lemma ptrofs_add_repr :

-  forall a b,

-  Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)).

-Proof.

-  intros a b.

-  rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq).

-  rewrite <- Zplus_mod. auto.

-Qed.

-

-Section PRESERVATION.

-

-Variables prog tprog: program.

-Hypothesis TRANSL: match_prog prog tprog.

-Let ge := Genv.globalenv prog.

-Let tge := Genv.globalenv tprog.

-

-Lemma transf_function_no_overflow:

-  forall f tf,

-  transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.

-Proof.

-  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.

-  omega.

-Qed.

-

-Lemma symbols_preserved:

-  forall id,

-  Genv.find_symbol tge id = Genv.find_symbol ge id.

-Proof (Genv.find_symbol_match TRANSL).

-

-Lemma senv_preserved:

-  Senv.equiv ge tge.

-Proof (Genv.senv_match TRANSL).

-

-Lemma functions_translated:

-  forall v f,

-  Genv.find_funct ge v = Some f ->

-  exists tf,

-  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.

-Proof (Genv.find_funct_transf_partial TRANSL).

-

-Lemma function_ptr_translated:

-  forall v f,

-  Genv.find_funct_ptr ge v = Some f ->

-  exists tf,

-  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.

-Proof (Genv.find_funct_ptr_transf_partial TRANSL).

-

-Lemma functions_transl:

-  forall fb f tf,

-  Genv.find_funct_ptr ge fb = Some (Internal f) ->

-  transf_function f = OK tf ->

-  Genv.find_funct_ptr tge fb = Some (Internal tf).

-Proof.

-  intros. exploit function_ptr_translated; eauto.

-  intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto.

-Qed.

-

-Inductive match_states: state -> state -> Prop :=

-  | match_states_intro:

-      forall s1 s2, s1 = s2 -> match_states s1 s2.

-

-Lemma prog_main_preserved:

-  prog_main tprog = prog_main prog.

-Proof (match_program_main TRANSL).

-

-Lemma prog_main_address_preserved:

-  (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) =

-  (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero).

-Proof.

-  unfold Genv.symbol_address. rewrite symbols_preserved.

-  rewrite prog_main_preserved. auto.

-Qed.

-

-Lemma transf_initial_states:

-  forall st1, initial_state prog st1 ->

-  exists st2, initial_state tprog st2 /\ match_states st1 st2.

-Proof.

-  intros. inv H.

-  econstructor; split.

-  - eapply initial_state_intro.

-    eapply (Genv.init_mem_transf_partial TRANSL); eauto.

-  - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto.

-Qed.

-

-Lemma transf_final_states:

-  forall st1 st2 r,

-  match_states st1 st2 -> final_state st1 r -> final_state st2 r.

-Proof.

-  intros. inv H0. inv H. econstructor; eauto.

-Qed.

-

-Lemma tail_find_bblock:

-  forall lbb pos bb,

-  find_bblock pos lbb = Some bb ->

-  exists c, code_tail pos lbb (bb::c).

-Proof.

-  induction lbb.

-  - intros. simpl in H. inv H.

-  - intros. simpl in H.

-    destruct (zlt pos 0); try (inv H; fail).

-    destruct (zeq pos 0).

-    + inv H. exists lbb. constructor; auto.

-    + apply IHlbb in H. destruct H as (c & TAIL). exists c.

-      cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto.

-      omega.

-Qed.

-

-Lemma code_tail_head_app:

-  forall l pos c1 c2,

-  code_tail pos c1 c2 ->

-  code_tail (pos + size_blocks l) (l++c1) c2.

-Proof.

-  induction l.

-  - intros. simpl. rewrite Z.add_0_r. auto.

-  - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption.

-Qed.

-

-Lemma transf_blocks_verified:

-  forall c tc pos bb c',

-  transf_blocks c = OK tc ->

-  code_tail pos c (bb::c') ->

-  exists lbb,

-     verified_schedule bb = OK lbb

-  /\ exists tc', code_tail pos tc (lbb ++ tc').

-Proof.

-  induction c; intros.

-  - simpl in H. inv H. inv H0.

-  - inv H0.

-    + monadInv H. exists x0.

-      split; simpl; auto. eexists; eauto. econstructor; eauto.

-    + unfold transf_blocks in H. fold transf_blocks in H. monadInv H.

-      exploit IHc; eauto.

-      intros (lbb & TRANS & tc' & TAIL).

-(*       monadInv TRANS. *)

-      repeat eexists; eauto.

-      erewrite verified_schedule_size; eauto.

-      apply code_tail_head_app.

-      eauto.

-Qed.

-

-Lemma transf_find_bblock:

-  forall ofs f bb tf,

-  find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->

-  transf_function f = OK tf ->

-  exists lbb,

-     verified_schedule bb = OK lbb

-  /\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c).

-Proof.

-  intros.

-  monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.

-  monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL).

-  eapply transf_blocks_verified; eauto.

-Qed.

-

-Lemma symbol_address_preserved:

-  forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs.

-Proof.

-  intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity.

-Qed.

-

-Lemma head_tail {A: Type}:

-  forall (l: list A) hd, hd::l = hd :: (tail (hd::l)).

-Proof.

-  intros. simpl. auto.

-Qed.

-

-Lemma verified_schedule_not_empty:

-  forall bb lbb,

-  verified_schedule bb = OK lbb -> lbb <> nil.

-Proof.

-  intros. apply verified_schedule_size in H.

-  pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.

-  destruct lbb; simpl in *; discriminate.

-Qed.

-

-Lemma header_nil_label_pos_none:

-  forall lbb l p,

-  Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None.

-Proof.

-  induction lbb.

-  - intros. simpl. auto.

-  - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. }

-    auto.

-Qed.

-

-Lemma verified_schedule_label:

-  forall bb tbb lbb l,

-  verified_schedule bb = OK (tbb :: lbb) ->

-     is_label l bb = is_label l tbb

-  /\ label_pos l 0 lbb = None.

-Proof.

-  intros. exploit verified_schedule_header; eauto.

-  intros (HdrEq & HdrNil).

-  split.

-  - unfold is_label. rewrite HdrEq. reflexivity.

-  - apply header_nil_label_pos_none. assumption.

-Qed.

-

-Lemma label_pos_app_none:

-  forall c c' l p p',

-  label_pos l p c = None ->

-  label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c').

-Proof.

-  induction c.

-  - intros. simpl in *. rewrite Z.add_0_r. reflexivity.

-  - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL.

-    + discriminate.

-    + eapply IHc in H. rewrite Z.add_assoc. eauto.

-Qed.

-

-Remark label_pos_pvar_none_add:

-  forall tc l p p' k,

-  label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None.

-Proof.

-  induction tc.

-  - intros. simpl. auto.

-  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.

-    + discriminate.

-    + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto.

-Qed.

-

-Lemma label_pos_pvar_none:

-  forall tc l p p',

-  label_pos l p tc = None -> label_pos l p' tc = None.

-Proof.

-  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.

-  eapply label_pos_pvar_none_add; eauto.

-Qed.

-

-Remark label_pos_pvar_some_add_add:

-  forall tc l p p' k k',

-  label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k).

-Proof.

-  induction tc.

-  - intros. simpl in H. discriminate.

-  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.

-    + inv H. assert (k = k') by omega. subst. reflexivity.

-    + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.

-Qed.

-

-Lemma label_pos_pvar_some_add:

-  forall tc l p p' k,

-  label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k).

-Proof.

-  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.

-  eapply label_pos_pvar_some_add_add; eauto.

-Qed.

-

-Remark label_pos_pvar_add:

-  forall c tc l p p' k,

-  label_pos l (p+k) c = label_pos l p tc ->

-  label_pos l (p'+k) c = label_pos l p' tc.

-Proof.

-  induction c.

-  - intros. simpl in *.

-    exploit label_pos_pvar_none; eauto.

-  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.

-    + exploit label_pos_pvar_some_add; eauto.

-    + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto.

-Qed.

-

-Lemma label_pos_pvar:

-  forall c tc l p p',

-  label_pos l p c = label_pos l p tc ->

-  label_pos l p' c = label_pos l p' tc.

-Proof.

-  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.

-  eapply label_pos_pvar_add; eauto.

-Qed.

-

-Lemma label_pos_head_app:

-  forall c bb lbb l tc p,

-  verified_schedule bb = OK lbb ->

-  label_pos l p c = label_pos l p tc ->

-  label_pos l p (bb :: c) = label_pos l p (lbb ++ tc).

-Proof.

-  intros. simpl. destruct lbb as [|tbb lbb].

-  - apply verified_schedule_not_empty in H. contradiction.

-  - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS).

-    rewrite ISLBL.

-    destruct (is_label l tbb) eqn:ISLBL'; simpl; auto.

-    eapply label_pos_pvar in H0. erewrite H0.

-    erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc.

-    erewrite label_pos_app_none; eauto.

-Qed.

-

-Lemma label_pos_preserved:

-  forall c tc l,

-  transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc.

-Proof.

-  induction c.

-  - intros. simpl in *. inv H. reflexivity.

-  - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ.

-    eapply label_pos_head_app; eauto.

-Qed.

-

-Lemma label_pos_preserved_blocks:

-  forall l f tf,

-  transf_function f = OK tf ->

-  label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf).

-Proof.

-  intros. monadInv H. monadInv EQ.

-  destruct (zlt Ptrofs.max_unsigned _); try discriminate.

-  monadInv EQ0. simpl. eapply label_pos_preserved; eauto.

-Qed.

-

-Lemma transf_exec_control:

-  forall f tf ex rs m,

-  transf_function f = OK tf ->

-  exec_control ge f ex rs m = exec_control tge tf ex rs m.

-Proof.

-  intros. destruct ex; simpl; auto.

-  assert (ge = Genv.globalenv prog). auto.

-  assert (tge = Genv.globalenv tprog). auto.

-  pose symbol_address_preserved.

-  exploreInst; simpl; auto; try congruence.

-  - unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-Qed.

-

-Lemma eval_offset_preserved:

-  forall ofs, eval_offset ge ofs = eval_offset tge ofs.

-Proof.

-  intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto.

-Qed.

-

-Lemma transf_exec_load:

-  forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs.

-Proof.

-  intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity.

-Qed.

-

-Lemma transf_exec_store:

-  forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs.

-Proof.

-  intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity.

-Qed.

-

-Lemma transf_exec_basic_instr:

-  forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m.

-Proof.

-  intros. pose symbol_address_preserved.

-  unfold exec_basic_instr. exploreInst; simpl; auto; try congruence.

-  1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence.

-  1-10: apply transf_exec_load.

-  all: apply transf_exec_store.

-Qed.

-

-Lemma transf_exec_body:

-  forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m.

-Proof.

-  induction bdy; intros.

-  - simpl. reflexivity.

-  - simpl. rewrite transf_exec_basic_instr.

-    destruct (exec_basic_instr _ _ _); auto.

-Qed.

-

-Lemma transf_exec_bblock:

-  forall f tf bb rs m,

-  transf_function f = OK tf ->

-  exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m.

-Proof.

-  intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto.

-  eapply transf_exec_control; eauto.

-Qed.

-

-Lemma transf_step_simu:

-  forall tf b lbb ofs c tbb rs m rs' m',

-  Genv.find_funct_ptr tge b = Some (Internal tf) ->

-  size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned ->

-  rs PC = Vptr b ofs ->

-  code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c) ->

-  concat_all lbb = OK tbb ->

-  exec_bblock tge tf tbb rs m = Next rs' m' ->

-  plus step tge (State rs m) E0 (State rs' m').

-Proof.

-  induction lbb.

-  - intros until m'. simpl. intros. discriminate.

-  - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB.

-    destruct lbb.

-    + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto.

-    + exploit concat_all_exec_bblock; eauto; try discriminate.

-    intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1).

-    eapply plus_left.

-    econstructor.

-      3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto.

-      all: eauto.

-    eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto.

-    eapply code_tail_next_int; eauto.

-Qed.

-

-Theorem transf_step_correct:

-  forall s1 t s2, step ge s1 t s2 ->

-  forall s1' (MS: match_states s1 s1'),

-  (exists s2', plus step tge s1' t s2' /\ match_states s2 s2').

-Proof.

-  induction 1; intros; inv MS.

-  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.

-    exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).

-    exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ).

-    assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).

-      eapply transf_function_no_overflow; eauto. 

-

-    erewrite transf_exec_bblock in H2; eauto.

-    inv BBEQ. rewrite H3 in H2.

-    exists (State rs' m'). split; try (constructor; auto).

-    eapply transf_step_simu; eauto.

-

-  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.

-    exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).

-    exploit verified_schedule_builtin_idem; eauto. intros. subst lbb.

-

-    remember (State (nextblock _ _) _) as s'. exists s'.

-    split; try constructor; auto.

-    eapply plus_one. subst s'.

-    eapply exec_step_builtin.

-      3: eapply find_bblock_tail. simpl in TAIL. 3: eauto.

-      all: eauto.

-    eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto.

-    eapply external_call_symbols_preserved; eauto. apply senv_preserved.

-

-  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.

-    remember (State _ m') as s'. exists s'. split; try constructor; auto.

-    subst s'. eapply plus_one. eapply exec_step_external; eauto.

-    eapply external_call_symbols_preserved; eauto. apply senv_preserved.

-Qed.

-

-Theorem transf_program_correct:

-  forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).

-Proof.

-  eapply forward_simulation_plus.

-  - apply senv_preserved.

-  - apply transf_initial_states.

-  - apply transf_final_states.

-  - apply transf_step_correct.

-Qed.

-

-End PRESERVATION.

+Require Import Coqlib Errors.
+Require Import Integers Floats AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations Machblock Conventions Asmblock.
+Require Import Asmblockgenproof0.
+Require Import PostpassScheduling.
+Require Import Asmblockgenproof.
+Require Import Axioms.
+
+Local Open Scope error_monad_scope.
+
+Definition match_prog (p tp: Asmblock.program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. eapply match_transform_partial_program; eauto.
+Qed.
+
+Remark builtin_body_nil:
+  forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
+Proof.
+  intros. destruct bb as [hd bdy ex WF]. simpl in *.
+  apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
+  eapply H1; eauto.
+Qed.
+
+Lemma verified_schedule_builtin_idem  (ge: Genv.t fundef unit) (fn: function):
+  forall bb ef args res lbb,
+  exit bb = Some (PExpand (Pbuiltin ef args res)) ->
+  verified_schedule bb = OK lbb ->
+  lbb = bb :: nil.
+Proof.
+  intros. exploit builtin_body_nil; eauto. intros.
+  rewrite verified_schedule_single_inst in H0; auto.
+  - inv H0. auto.
+  - unfold size. rewrite H. rewrite H1. simpl. auto.
+Qed.
+
+Lemma exec_body_app:
+  forall l l' ge rs m rs'' m'',
+  exec_body ge (l ++ l') rs m = Next rs'' m'' ->
+  exists rs' m',
+       exec_body ge l rs m = Next rs' m'
+    /\ exec_body ge l' rs' m' = Next rs'' m''.
+Proof.
+  induction l.
+  - intros. simpl in H. repeat eexists. auto.
+  - intros. rewrite <- app_comm_cons in H. simpl in H.
+    destruct (exec_basic_instr ge a rs m) eqn:EXEBI.
+    + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
+      repeat eexists. simpl. rewrite EXEBI. eauto. auto.
+    + discriminate.
+Qed.
+
+Lemma exec_body_pc:
+  forall l ge rs1 m1 rs2 m2,
+  exec_body ge l rs1 m1 = Next rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  induction l.
+  - intros. inv H. auto.
+  - intros until m2. intro EXEB.
+    inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
+    eapply IHl in H0. rewrite H0.
+    erewrite exec_basic_instr_pc; eauto.
+Qed.
+
+Lemma next_eq {A: Type}:
+  forall (rs rs':A) m m',
+  rs = rs' -> m = m' -> Next rs m = Next rs' m'.
+Proof.
+  intros. congruence.
+Qed.
+
+Lemma regset_double_set:
+  forall r1 r2 (rs: regset) v1 v2,
+  r1 <> r2 ->
+  (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).
+Proof.
+  intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).
+  - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.
+  - destruct (preg_eq r r2).
+    + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.
+    + repeat (rewrite Pregmap.gso; auto).
+Qed.
+
+Lemma regset_double_set_id:
+  forall r (rs: regset) v1 v2,
+  (rs # r <- v1 # r <- v2) = (rs # r <- v2).
+Proof.
+  intros. apply functional_extensionality. intros. destruct (preg_eq r x).
+  - subst r. repeat (rewrite Pregmap.gss; auto).
+  - repeat (rewrite Pregmap.gso); auto.
+Qed.
+
+Lemma exec_load_pc_var:
+  forall ge t rs m rd ra ofs rs' m' v,
+  exec_load ge t rs m rd ra ofs = Next rs' m' ->
+  exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
+  destruct (Mem.loadv _ _ _).
+  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+  - discriminate.
+Qed.
+
+Lemma exec_store_pc_var:
+  forall ge t rs m rd ra ofs rs' m' v,
+  exec_store ge t rs m rd ra ofs = Next rs' m' ->
+  exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
+  destruct (Mem.storev _ _ _).
+  - inv H. apply next_eq; auto.
+  - discriminate.
+Qed.
+
+Lemma exec_basic_instr_pc_var:
+  forall ge i rs m rs' m' v,
+  exec_basic_instr ge i rs m = Next rs' m' ->
+  exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
+Proof.
+  intros. unfold exec_basic_instr in *. destruct i.
+  - unfold exec_arith_instr in *. destruct i; destruct i.
+      all: try (exploreInst; inv H; apply next_eq; auto;
+      apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
+
+      (* Some cases treated seperately because exploreInst destructs too much *)
+      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
+  - exploreInst; apply exec_load_pc_var; auto.
+  - exploreInst; apply exec_store_pc_var; auto.
+  - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
+    destruct (Mem.storev _ _ _ _); try discriminate.
+    inv H. apply next_eq; auto. apply functional_extensionality. intros.
+    rewrite (regset_double_set GPR32 PC); try discriminate.
+    rewrite (regset_double_set GPR12 PC); try discriminate.
+    rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity.
+  - repeat (rewrite Pregmap.gso; try discriminate).
+    destruct (Mem.loadv _ _ _); try discriminate.
+    destruct (rs GPR12); try discriminate.
+    destruct (Mem.free _ _ _ _); try discriminate.
+    inv H. apply next_eq; auto.
+    rewrite (regset_double_set GPR32 PC).
+    rewrite (regset_double_set GPR12 PC). reflexivity.
+    all: discriminate.
+  - destruct rs0; try discriminate. inv H. apply next_eq; auto.
+    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
+  - destruct rd; try discriminate. inv H. apply next_eq; auto.
+    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
+  - inv H. apply next_eq; auto.
+Qed.
+
+Lemma exec_body_pc_var:
+  forall l ge rs m rs' m' v,
+  exec_body ge l rs m = Next rs' m' ->
+  exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'.
+Proof.
+  induction l.
+  - intros. simpl. simpl in H. inv H. auto.
+  - intros. simpl in *.
+    destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate.
+    erewrite exec_basic_instr_pc_var; eauto.
+Qed.
+
+Lemma pc_set_add:
+  forall rs v r x y,
+  0 <= x <= Ptrofs.max_unsigned ->
+  0 <= y <= Ptrofs.max_unsigned ->
+  rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)).
+Proof.
+  intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0).
+  - subst. repeat (rewrite Pregmap.gss); auto.
+    destruct v; simpl; auto.
+    rewrite Ptrofs.add_assoc.
+    cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto.
+    unfold Ptrofs.add.
+    cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto.
+    repeat (rewrite Ptrofs.unsigned_repr); auto.
+  - repeat (rewrite Pregmap.gso; auto).
+Qed.
+
+Lemma concat2_straight:
+  forall a b bb rs m rs'' m'' f ge,
+  concat2 a b = OK bb ->
+  exec_bblock ge f bb rs m = Next rs'' m'' ->
+  exists rs' m',
+       exec_bblock ge f a rs m = Next rs' m'
+    /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
+    /\ exec_bblock ge f b rs' m' = Next rs'' m''.
+Proof.
+  intros until ge. intros CONC2 EXEB.
+  exploit concat2_zlt_size; eauto. intros (LTA & LTB).
+  exploit concat2_noexit; eauto. intros EXA.
+  exploit concat2_decomp; eauto. intros. inv H.
+  unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.
+  rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2).
+  repeat eexists.
+    unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
+    exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
+    unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto.
+    rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
+    assert (size bb = size a + size b).
+    { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
+      repeat (rewrite Nat2Z.inj_add). omega. }
+    clear EXA H0 H1. rewrite H in EXEB.
+    assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
+    rewrite H0. rewrite <- pc_set_add; auto.
+    exploit AB.size_positive. instantiate (1 := a). intro. omega.
+    exploit AB.size_positive. instantiate (1 := b). intro. omega.
+Qed.
+
+Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
+  forall a bb rs m lbb rs'' m'', 
+  lbb <> nil ->
+  concat_all (a :: lbb) = OK bb ->
+  exec_bblock ge f bb rs m = Next rs'' m'' ->
+  exists bb' rs' m',
+       concat_all lbb = OK bb'
+    /\ exec_bblock ge f a rs m = Next rs' m'
+    /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
+    /\ exec_bblock ge f bb' rs' m' = Next rs'' m''.
+Proof.
+  intros until m''. intros Hnonil CONC EXEB.
+  simpl in CONC.
+  destruct lbb as [|b lbb]; try contradiction. clear Hnonil.
+  monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2).
+  exists x. repeat econstructor. all: eauto.
+Qed.
+
+Lemma ptrofs_add_repr :
+  forall a b,
+  Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)).
+Proof.
+  intros a b.
+  rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq).
+  rewrite <- Zplus_mod. auto.
+Qed.
+
+Section PRESERVATION.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma transf_function_no_overflow:
+  forall f tf,
+  transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
+Proof.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
+  omega.
+Qed.
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (Genv.find_symbol_match TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSL).
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  exists tf,
+  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_transf_partial TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial TRANSL).
+
+Lemma functions_transl:
+  forall fb f tf,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  transf_function f = OK tf ->
+  Genv.find_funct_ptr tge fb = Some (Internal tf).
+Proof.
+  intros. exploit function_ptr_translated; eauto.
+  intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto.
+Qed.
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro:
+      forall s1 s2, s1 = s2 -> match_states s1 s2.
+
+Lemma prog_main_preserved:
+  prog_main tprog = prog_main prog.
+Proof (match_program_main TRANSL).
+
+Lemma prog_main_address_preserved:
+  (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) =
+  (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero).
+Proof.
+  unfold Genv.symbol_address. rewrite symbols_preserved.
+  rewrite prog_main_preserved. auto.
+Qed.
+
+Lemma transf_initial_states:
+  forall st1, initial_state prog st1 ->
+  exists st2, initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inv H.
+  econstructor; split.
+  - eapply initial_state_intro.
+    eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+  - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto.
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r,
+  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
+Proof.
+  intros. inv H0. inv H. econstructor; eauto.
+Qed.
+
+Lemma tail_find_bblock:
+  forall lbb pos bb,
+  find_bblock pos lbb = Some bb ->
+  exists c, code_tail pos lbb (bb::c).
+Proof.
+  induction lbb.
+  - intros. simpl in H. inv H.
+  - intros. simpl in H.
+    destruct (zlt pos 0); try (inv H; fail).
+    destruct (zeq pos 0).
+    + inv H. exists lbb. constructor; auto.
+    + apply IHlbb in H. destruct H as (c & TAIL). exists c.
+      cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto.
+      omega.
+Qed.
+
+Lemma code_tail_head_app:
+  forall l pos c1 c2,
+  code_tail pos c1 c2 ->
+  code_tail (pos + size_blocks l) (l++c1) c2.
+Proof.
+  induction l.
+  - intros. simpl. rewrite Z.add_0_r. auto.
+  - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption.
+Qed.
+
+Lemma transf_blocks_verified:
+  forall c tc pos bb c',
+  transf_blocks c = OK tc ->
+  code_tail pos c (bb::c') ->
+  exists lbb,
+     verified_schedule bb = OK lbb
+  /\ exists tc', code_tail pos tc (lbb ++ tc').
+Proof.
+  induction c; intros.
+  - simpl in H. inv H. inv H0.
+  - inv H0.
+    + monadInv H. exists x0.
+      split; simpl; auto. eexists; eauto. econstructor; eauto.
+    + unfold transf_blocks in H. fold transf_blocks in H. monadInv H.
+      exploit IHc; eauto.
+      intros (lbb & TRANS & tc' & TAIL).
+(*       monadInv TRANS. *)
+      repeat eexists; eauto.
+      erewrite verified_schedule_size; eauto.
+      apply code_tail_head_app.
+      eauto.
+Qed.
+
+Lemma transf_find_bblock:
+  forall ofs f bb tf,
+  find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
+  transf_function f = OK tf ->
+  exists lbb,
+     verified_schedule bb = OK lbb
+  /\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c).
+Proof.
+  intros.
+  monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.
+  monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL).
+  eapply transf_blocks_verified; eauto.
+Qed.
+
+Lemma symbol_address_preserved:
+  forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs.
+Proof.
+  intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity.
+Qed.
+
+Lemma head_tail {A: Type}:
+  forall (l: list A) hd, hd::l = hd :: (tail (hd::l)).
+Proof.
+  intros. simpl. auto.
+Qed.
+
+Lemma verified_schedule_not_empty:
+  forall bb lbb,
+  verified_schedule bb = OK lbb -> lbb <> nil.
+Proof.
+  intros. apply verified_schedule_size in H.
+  pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.
+  destruct lbb; simpl in *; discriminate.
+Qed.
+
+Lemma header_nil_label_pos_none:
+  forall lbb l p,
+  Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None.
+Proof.
+  induction lbb.
+  - intros. simpl. auto.
+  - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. }
+    auto.
+Qed.
+
+Lemma verified_schedule_label:
+  forall bb tbb lbb l,
+  verified_schedule bb = OK (tbb :: lbb) ->
+     is_label l bb = is_label l tbb
+  /\ label_pos l 0 lbb = None.
+Proof.
+  intros. exploit verified_schedule_header; eauto.
+  intros (HdrEq & HdrNil).
+  split.
+  - unfold is_label. rewrite HdrEq. reflexivity.
+  - apply header_nil_label_pos_none. assumption.
+Qed.
+
+Lemma label_pos_app_none:
+  forall c c' l p p',
+  label_pos l p c = None ->
+  label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c').
+Proof.
+  induction c.
+  - intros. simpl in *. rewrite Z.add_0_r. reflexivity.
+  - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL.
+    + discriminate.
+    + eapply IHc in H. rewrite Z.add_assoc. eauto.
+Qed.
+
+Remark label_pos_pvar_none_add:
+  forall tc l p p' k,
+  label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None.
+Proof.
+  induction tc.
+  - intros. simpl. auto.
+  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
+    + discriminate.
+    + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto.
+Qed.
+
+Lemma label_pos_pvar_none:
+  forall tc l p p',
+  label_pos l p tc = None -> label_pos l p' tc = None.
+Proof.
+  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
+  eapply label_pos_pvar_none_add; eauto.
+Qed.
+
+Remark label_pos_pvar_some_add_add:
+  forall tc l p p' k k',
+  label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k).
+Proof.
+  induction tc.
+  - intros. simpl in H. discriminate.
+  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
+    + inv H. assert (k = k') by omega. subst. reflexivity.
+    + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
+Qed.
+
+Lemma label_pos_pvar_some_add:
+  forall tc l p p' k,
+  label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k).
+Proof.
+  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
+  eapply label_pos_pvar_some_add_add; eauto.
+Qed.
+
+Remark label_pos_pvar_add:
+  forall c tc l p p' k,
+  label_pos l (p+k) c = label_pos l p tc ->
+  label_pos l (p'+k) c = label_pos l p' tc.
+Proof.
+  induction c.
+  - intros. simpl in *.
+    exploit label_pos_pvar_none; eauto.
+  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
+    + exploit label_pos_pvar_some_add; eauto.
+    + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto.
+Qed.
+
+Lemma label_pos_pvar:
+  forall c tc l p p',
+  label_pos l p c = label_pos l p tc ->
+  label_pos l p' c = label_pos l p' tc.
+Proof.
+  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
+  eapply label_pos_pvar_add; eauto.
+Qed.
+
+Lemma label_pos_head_app:
+  forall c bb lbb l tc p,
+  verified_schedule bb = OK lbb ->
+  label_pos l p c = label_pos l p tc ->
+  label_pos l p (bb :: c) = label_pos l p (lbb ++ tc).
+Proof.
+  intros. simpl. destruct lbb as [|tbb lbb].
+  - apply verified_schedule_not_empty in H. contradiction.
+  - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS).
+    rewrite ISLBL.
+    destruct (is_label l tbb) eqn:ISLBL'; simpl; auto.
+    eapply label_pos_pvar in H0. erewrite H0.
+    erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc.
+    erewrite label_pos_app_none; eauto.
+Qed.
+
+Lemma label_pos_preserved:
+  forall c tc l,
+  transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc.
+Proof.
+  induction c.
+  - intros. simpl in *. inv H. reflexivity.
+  - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ.
+    eapply label_pos_head_app; eauto.
+Qed.
+
+Lemma label_pos_preserved_blocks:
+  forall l f tf,
+  transf_function f = OK tf ->
+  label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf).
+Proof.
+  intros. monadInv H. monadInv EQ.
+  destruct (zlt Ptrofs.max_unsigned _); try discriminate.
+  monadInv EQ0. simpl. eapply label_pos_preserved; eauto.
+Qed.
+
+Lemma transf_exec_control:
+  forall f tf ex rs m,
+  transf_function f = OK tf ->
+  exec_control ge f ex rs m = exec_control tge tf ex rs m.
+Proof.
+  intros. destruct ex; simpl; auto.
+  assert (ge = Genv.globalenv prog). auto.
+  assert (tge = Genv.globalenv tprog). auto.
+  pose symbol_address_preserved.
+  exploreInst; simpl; auto; try congruence.
+  - unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+Qed.
+
+Lemma eval_offset_preserved:
+  forall ofs, eval_offset ge ofs = eval_offset tge ofs.
+Proof.
+  intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto.
+Qed.
+
+Lemma transf_exec_load:
+  forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs.
+Proof.
+  intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity.
+Qed.
+
+Lemma transf_exec_store:
+  forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs.
+Proof.
+  intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity.
+Qed.
+
+Lemma transf_exec_basic_instr:
+  forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m.
+Proof.
+  intros. pose symbol_address_preserved.
+  unfold exec_basic_instr. exploreInst; simpl; auto; try congruence.
+  1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence.
+  1-10: apply transf_exec_load.
+  all: apply transf_exec_store.
+Qed.
+
+Lemma transf_exec_body:
+  forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m.
+Proof.
+  induction bdy; intros.
+  - simpl. reflexivity.
+  - simpl. rewrite transf_exec_basic_instr.
+    destruct (exec_basic_instr _ _ _); auto.
+Qed.
+
+Lemma transf_exec_bblock:
+  forall f tf bb rs m,
+  transf_function f = OK tf ->
+  exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m.
+Proof.
+  intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto.
+  eapply transf_exec_control; eauto.
+Qed.
+
+Lemma transf_step_simu:
+  forall tf b lbb ofs c tbb rs m rs' m',
+  Genv.find_funct_ptr tge b = Some (Internal tf) ->
+  size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned ->
+  rs PC = Vptr b ofs ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c) ->
+  concat_all lbb = OK tbb ->
+  exec_bblock tge tf tbb rs m = Next rs' m' ->
+  plus step tge (State rs m) E0 (State rs' m').
+Proof.
+  induction lbb.
+  - intros until m'. simpl. intros. discriminate.
+  - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB.
+    destruct lbb.
+    + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto.
+    + exploit concat_all_exec_bblock; eauto; try discriminate.
+    intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1).
+    eapply plus_left.
+    econstructor.
+      3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto.
+      all: eauto.
+    eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto.
+    eapply code_tail_next_int; eauto.
+Qed.
+
+Theorem transf_step_correct:
+  forall s1 t s2, step ge s1 t s2 ->
+  forall s1' (MS: match_states s1 s1'),
+  (exists s2', plus step tge s1' t s2' /\ match_states s2 s2').
+Proof.
+  induction 1; intros; inv MS.
+  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
+    exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
+    exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ).
+    assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).
+      eapply transf_function_no_overflow; eauto. 
+
+    erewrite transf_exec_bblock in H2; eauto.
+    inv BBEQ. rewrite H3 in H2.
+    exists (State rs' m'). split; try (constructor; auto).
+    eapply transf_step_simu; eauto.
+
+  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
+    exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
+    exploit verified_schedule_builtin_idem; eauto. intros. subst lbb.
+
+    remember (State (nextblock _ _) _) as s'. exists s'.
+    split; try constructor; auto.
+    eapply plus_one. subst s'.
+    eapply exec_step_builtin.
+      3: eapply find_bblock_tail. simpl in TAIL. 3: eauto.
+      all: eauto.
+    eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+
+  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
+    remember (State _ m') as s'. exists s'. split; try constructor; auto.
+    subst s'. eapply plus_one. eapply exec_step_external; eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).
+Proof.
+  eapply forward_simulation_plus.
+  - apply senv_preserved.
+  - apply transf_initial_states.
+  - apply transf_final_states.
+  - apply transf_step_correct.
+Qed.
+
+End PRESERVATION.
diff --git a/mppa_k1c/SelectLong.v b/mppa_k1c/SelectLong.v
index f2aa6be2..ea42b9c3 100644
--- a/mppa_k1c/SelectLong.v
+++ b/mppa_k1c/SelectLong.v
@@ -755,20 +755,29 @@ Definition floatoflongu (e: expr) :=
   if Archi.splitlong then SplitLong.floatoflongu e else 
   Eop Ofloatoflongu (e:::Enil).
 
-Definition longofsingle (e: expr) := 
+(* FIXME - normally we can have it natively, but in practice it requires proving that we can do Fwidenlwd + fixedd.rz.. To do later *)
+Definition longofsingle (e: expr) := SplitLong.longofsingle e.
+(*
   if Archi.splitlong then SplitLong.longofsingle e else 
   Eop Olongofsingle (e:::Enil).
+*)
 
-Definition longuofsingle (e: expr) := 
+Definition longuofsingle (e: expr) := SplitLong.longuofsingle e.
+(*
   if Archi.splitlong then SplitLong.longuofsingle e else 
   Eop Olonguofsingle (e:::Enil).
+*)
 
-Definition singleoflong (e: expr) := 
+Definition singleoflong (e: expr) := SplitLong.singleoflong e.
+(*
   if Archi.splitlong then SplitLong.singleoflong e else 
   Eop Osingleoflong (e:::Enil).
+*)
 
-Definition singleoflongu (e: expr) := 
+Definition singleoflongu (e: expr) := SplitLong.singleoflongu e.
+(*
   if Archi.splitlong then SplitLong.singleoflongu e else 
   Eop Osingleoflongu (e:::Enil).
+*)
 
 End SELECT.
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 26735c99..a3aefb15 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -341,20 +341,29 @@ Definition floatoflongu (e: expr) :=
   if Archi.splitlong then SplitLong.floatoflongu e else 
   Eop Ofloatoflongu (e:::Enil).
 
-Definition longofsingle (e: expr) := 
+(* FIXME - normally we can have it natively, but in practice it requires proving that we can do Fwidenlwd + fixedd.rz.. To do later *)
+Definition longofsingle (e: expr) := SplitLong.longofsingle e.
+(*
   if Archi.splitlong then SplitLong.longofsingle e else 
   Eop Olongofsingle (e:::Enil).
+*)
 
-Definition longuofsingle (e: expr) := 
+Definition longuofsingle (e: expr) := SplitLong.longuofsingle e.
+(*
   if Archi.splitlong then SplitLong.longuofsingle e else 
   Eop Olonguofsingle (e:::Enil).
+*)
 
-Definition singleoflong (e: expr) := 
+Definition singleoflong (e: expr) := SplitLong.singleoflong e.
+(*
   if Archi.splitlong then SplitLong.singleoflong e else 
   Eop Osingleoflong (e:::Enil).
+*)
 
-Definition singleoflongu (e: expr) := 
+Definition singleoflongu (e: expr) := SplitLong.singleoflongu e.
+(*
   if Archi.splitlong then SplitLong.singleoflongu e else 
   Eop Osingleoflongu (e:::Enil).
+*)
 
 End SELECT.
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index d12fb9ae..44846a6f 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -582,30 +582,30 @@ Qed.
 
 Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
 Proof.
-  unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL.
+  unfold longofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *)
   eapply SplitLongproof.eval_longofsingle; eauto.
-  TrivialExists.
+(*   TrivialExists. *)
 Qed.
 
 Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle.
 Proof.
-  unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL.
+  unfold longuofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *)
   eapply SplitLongproof.eval_longuofsingle; eauto.
-  TrivialExists.
+(*   TrivialExists. *)
 Qed.
 
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
 Proof.
-  unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL.
+  unfold singleoflong; red; intros. (* destruct Archi.splitlong eqn:SL. *)
   eapply SplitLongproof.eval_singleoflong; eauto.
-  TrivialExists.
+(*   TrivialExists. *)
 Qed.
 
 Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu.
 Proof.
-  unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL.
+  unfold singleoflongu; red; intros. (* destruct Archi.splitlong eqn:SL. *)
   eapply SplitLongproof.eval_singleoflongu; eauto.
-  TrivialExists.
+(*   TrivialExists. *)
 Qed.
 
 End CMCONSTR.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index bbb608de..5d59e7d2 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -173,6 +173,18 @@ module Target (*: TARGET*) =
       | ITnone -> "none"
 
     let icond oc c = fprintf oc "%s" (icond_name c)
+
+    let fcond_name = let open Asmblock in function
+      | FTone -> "one"
+      | FTueq -> "ueq"
+      | FToeq -> "oeq"
+      | FTune -> "une"
+      | FTolt -> "olt"
+      | FTuge -> "uge"
+      | FToge -> "oge"
+      | FTult -> "ult"
+
+    let fcond oc c = fprintf oc "%s" (fcond_name c)
   
     let bcond_name = let open Asmblock in function
       | BTwnez -> "wnez"
@@ -295,23 +307,29 @@ module Target (*: TARGET*) =
       | Pfabsw(rd, rs) ->
          fprintf oc "	fabsw	%a = %a\n" ireg rd ireg rs
       | Pfnegd(rd, rs) ->
-         fprintf oc "	fnegd	%a = %a\n" ireg rs ireg rd
+         fprintf oc "	fnegd	%a = %a\n" ireg rd ireg rs
       | Pfnegw(rd, rs) ->
-         fprintf oc "	fnegw	%a = %a\n" ireg rs ireg rd
+         fprintf oc "	fnegw	%a = %a\n" ireg rd ireg rs
       | Pfnarrowdw(rd, rs) ->
-         fprintf oc "	fnarrowdw	%a = %a\n" ireg rs ireg rd
+         fprintf oc "	fnarrowdw	%a = %a\n" ireg rd ireg rs
       | Pfwidenlwd(rd, rs) ->
-         fprintf oc "	fwidenlwd	%a = %a\n" ireg rs ireg rd
+         fprintf oc "	fwidenlwd	%a = %a\n" ireg rd ireg rs
+      | Pfloatuwrnsz(rd, rs) ->
+         fprintf oc "	floatuw.rn.s	%a = %a, 0\n" ireg rd ireg rs
       | Pfloatwrnsz(rd, rs) ->
          fprintf oc "	floatw.rn.s	%a = %a, 0\n" ireg rd ireg rs
-      | Pfloatudrnsz(rd, rs) ->
+      | Pfloatudrnsz(rd, rs) | Pfloatudrnsz_i32(rd, rs) ->
          fprintf oc "	floatud.rn.s	%a = %a, 0\n" ireg rd ireg rs
-      | Pfloatdrnsz(rd, rs) ->
+      | Pfloatdrnsz(rd, rs) | Pfloatdrnsz_i32(rd, rs) ->
          fprintf oc "	floatd.rn.s	%a = %a, 0\n" ireg rd ireg rs
       | Pfixedwrzz(rd, rs) ->
          fprintf oc "	fixedw.rz	%a = %a, 0\n" ireg rd ireg rs
-      | Pfixeddrzz(rd, rs) ->
+      | Pfixeduwrzz(rd, rs) ->
+         fprintf oc "	fixeduw.rz	%a = %a, 0\n" ireg rd ireg rs
+      | Pfixeddrzz(rd, rs) | Pfixeddrzz_i32(rd, rs) ->
          fprintf oc "	fixedd.rz	%a = %a, 0\n" ireg rd ireg rs
+      | Pfixedudrzz(rd, rs) | Pfixedudrzz_i32(rd, rs) ->
+         fprintf oc "	fixedud.rz	%a = %a, 0\n" ireg rd ireg rs
 
       (* Arith RI32 instructions *)
       | Pmake (rd, imm) ->
@@ -339,6 +357,11 @@ module Target (*: TARGET*) =
       | Pcompl (it, rd, rs1, rs2) ->
          fprintf oc "	compd.%a	%a = %a, %a\n" icond it ireg rd ireg rs1 ireg rs2
 
+      | Pfcompw (ft, rd, rs1, rs2) ->
+         fprintf oc "	fcompw.%a	%a = %a, %a\n" fcond ft ireg rd ireg rs1 ireg rs2
+      | Pfcompl (ft, rd, rs1, rs2) ->
+         fprintf oc "	fcompd.%a	%a = %a, %a\n" fcond ft ireg rd ireg rs1 ireg rs2
+
       | Paddw (rd, rs1, rs2) ->
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Psubw (rd, rs1, rs2) ->
@@ -382,9 +405,9 @@ module Target (*: TARGET*) =
       | Pfaddw (rd, rs1, rs2) ->
          fprintf oc "	faddw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pfsbfd (rd, rs1, rs2) ->
-         fprintf oc "	fsbfd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	fsbfd	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
       | Pfsbfw (rd, rs1, rs2) ->
-         fprintf oc "	fsbfw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	fsbfw	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
       | Pfmuld (rd, rs1, rs2) ->
          fprintf oc "	fmuld	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pfmulw (rd, rs1, rs2) ->
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 8c299f88..69234938 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -20,6 +20,12 @@ Module AB:=Asmblock.
 
 Hint Extern 2 (_ <> _) => congruence: asmgen.
 
+Inductive bblock_equiv (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
+  | bblock_equiv_intro:
+      (forall rs m,
+      exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m) ->
+      bblock_equiv ge f bb bb'.
+
 Lemma ireg_of_eq:
   forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
 Proof.
@@ -1096,4 +1102,4 @@ Proof.
   intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
 Qed.
 
-End MATCH_STACK.
\ No newline at end of file
+End MATCH_STACK.
diff --git a/runtime/Makefile b/runtime/Makefile
index 66ec6fec..f58d4b6a 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -23,7 +23,9 @@ OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o
 else ifeq ($(ARCH),powerpc64)
 OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o
 else ifeq ($(ARCH),mppa_k1c)
-OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o
+OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o\
+		 i64_dtos.o i64_dtou.o i64_utod.o i64_utof.o i64_stod.o i64_stof.o
+# Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o
 DOMAKE:=$(shell (cd mppa_k1c && make))
 else
 OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
@@ -66,7 +68,7 @@ $(LIB): $(OBJS)
 	../ccomp -O2 -S -o $*.s -I./c c/$*.c
 	sed -i -e 's/i64_/__compcert_i64_/g' $*.s
 	$(CASMRUNTIME) -o $*.o $*.s
-	@rm -f $*.s
+	@rm $*.s
 
 clean::
 	rm -f *.o $(LIB) *.tmp?.s
diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile
index b4abb6a4..ea86114c 100644
--- a/test/mppa/instr/Makefile
+++ b/test/mppa/instr/Makefile
@@ -5,6 +5,7 @@ OPTIM ?= -O2
 CFLAGS ?= $(OPTIM)
 SIMU ?= k1-mppa
 TIMEOUT ?= --signal=SIGTERM 120s
+DIFF ?= python2.7 floatcmp.py -reltol .00001
 
 DIR=./
 SRCDIR=$(DIR)
@@ -50,7 +51,7 @@ test: $(X86_GCC_OUT) $(GCC_OUT)
 	@for test in $(TESTNAMES); do\
 		x86out=$(OUTDIR)/$$test.x86-gcc.out;\
 		gccout=$(OUTDIR)/$$test.gcc.out;\
-		if diff -q $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
+		if $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
 			>&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\
 		else\
 			printf "$(GREEN)GOOD: $$x86out and $$gccout concur$(NC)\n";\
@@ -63,7 +64,7 @@ check: $(GCC_OUT) $(CCOMP_OUT)
 	@for test in $(TESTNAMES); do\
 		gccout=$(OUTDIR)/$$test.gcc.out;\
 		ccompout=$(OUTDIR)/$$test.ccomp.out;\
-		if diff -q $$ccompout $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
+		if $(DIFF) $$ccompout $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\
 			>&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\
 		else\
 			printf "$(GREEN)GOOD: $$ccompout and $$gccout concur$(NC)\n";\
diff --git a/test/mppa/instr/faddw.c b/test/mppa/instr/faddw.c
index a00e9afe..e0e635ae 100644
--- a/test/mppa/instr/faddw.c
+++ b/test/mppa/instr/faddw.c
@@ -1,5 +1,5 @@
 #include "framework.h"
 
-BEGIN_TEST(double)
+BEGIN_TEST(float)
     c = ((float)a + (float)b);
-END_TESTF64()
+END_TESTF32()
diff --git a/test/mppa/instr/floatcmp.py b/test/mppa/instr/floatcmp.py
new file mode 100755
index 00000000..49f1bc13
--- /dev/null
+++ b/test/mppa/instr/floatcmp.py
@@ -0,0 +1,93 @@
+#!/usr/bin/python2.7
+
+import argparse as ap
+import sys
+
+parser = ap.ArgumentParser()
+parser.add_argument("file1", help="First file to compare")
+parser.add_argument("file2", help="Second file to compare")
+parser.add_argument("-reltol", help="Relative error")
+parser.add_argument("-abstol", help="Absolute error")
+parser.add_argument("-s", help="Silent output", action="store_true")
+args = parser.parse_args()
+
+reltol = float(args.reltol) if args.reltol else None
+abstol = float(args.abstol) if args.abstol else None
+silent = args.s
+
+if silent:
+    sys.stdout = open("/dev/null", "w")
+
+import re
+from math import fabs
+
+def floatcmp(f1, f2):
+    if abstol:
+        if fabs(f1 - f2) > abstol:
+            return False
+    if reltol:
+        if f2 != 0. and fabs((f1 - f2) / f2) > reltol:
+            return False
+    return True
+
+class Parsed(list):
+    def __eq__(self, other):
+        if len(self) != len(other):
+            return False
+        comps = zip(self, other)
+        for comp in comps:
+            if all(isinstance(compElt, str) for compElt in comp):
+                if comp[0] != comp[1]:
+                    return False
+            elif all (isinstance(compElt, float) for compElt in comp):
+                if not floatcmp(comp[0], comp[1]):
+                    return False
+            else:
+                return False
+        return True
+    
+    def __ne__(self, other):
+        return not self.__eq__(other)
+
+parseLine = re.compile(r"\s*(\S+)")
+def readline(line):
+    words = parseLine.findall(line)
+    parsed = Parsed([])
+    for word in words:
+        try:
+            parse = float(word)
+            parsed.append(parse)
+        except ValueError:
+            parsed.append(word)
+    return parsed
+
+def readfile(filename):
+    L = []
+    try:
+        with open(filename) as f:
+            for line in f:
+                L.append(readline(line))
+    except IOError:
+        print "Unable to read {}".format(filename)
+        sys.exit(2)
+    return L
+
+L1 = readfile(args.file1)
+L2 = readfile(args.file2)
+
+if len(L1) != len(L2):
+    print "The files have different amount of lines"
+    print "\t{}: {} lines".format(args.file1, len(L1))
+    print "\t{}: {} lines".format(args.file2, len(L2))
+    sys.exit(1)
+
+cmpL = zip(L1, L2)
+for i, cmpElt in enumerate(cmpL):
+    if cmpElt[0] != cmpElt[1]:
+        print "The files differ at line {}".format(i)
+        print "\t{}: {}".format(args.file1, cmpElt[0])
+        print "\t{}: {}".format(args.file2, cmpElt[1])
+        sys.exit(1)
+
+print "Comparison succeeded"
+sys.exit(0)
diff --git a/test/mppa/instr/fmulw.c b/test/mppa/instr/fmulw.c
index 030a6d9c..f85eba64 100644
--- a/test/mppa/instr/fmulw.c
+++ b/test/mppa/instr/fmulw.c
@@ -1,7 +1,7 @@
 #include "framework.h"
 
-BEGIN_TEST(double)
+BEGIN_TEST(float)
 {
     c = ((float)a * (float)b);
 }
-END_TESTF64()
+END_TESTF32()
diff --git a/test/mppa/instr/fnegw.c b/test/mppa/instr/fnegw.c
index acbabf68..fbeaab8e 100644
--- a/test/mppa/instr/fnegw.c
+++ b/test/mppa/instr/fnegw.c
@@ -1,6 +1,6 @@
 #include "framework.h"
 
-BEGIN_TEST(double)
+BEGIN_TEST(float)
 {
     c = (-(float)a);
 }
diff --git a/test/mppa/instr/framework.h b/test/mppa/instr/framework.h
index d4f36f6b..3bbfa271 100644
--- a/test/mppa/instr/framework.h
+++ b/test/mppa/instr/framework.h
@@ -46,7 +46,7 @@
     /* END END_TEST32 */
 
 #define END_TESTF32()\
-            printf("%f\t%f\t%f\n", a, b, c);\
+            printf("%e\t%e\t%e\n", a, b, c);\
             S += c;\
         }\
         return 0;\
@@ -54,7 +54,7 @@
     /* END END_TESTF32 */
 
 #define END_TESTF64()\
-            printf("%lf\t%lf\t%lf\n", a, b, c);\
+            printf("%e\t%e\t%e\n", a, b, c);\
             S += c;\
         }\
         return 0;\
diff --git a/test/mppa/instr/fsbfw.c b/test/mppa/instr/fsbfw.c
index 835963d5..067c40b5 100644
--- a/test/mppa/instr/fsbfw.c
+++ b/test/mppa/instr/fsbfw.c
@@ -1,6 +1,6 @@
 #include "framework.h"
 
-BEGIN_TEST(double)
+BEGIN_TEST(float)
 {
     c = ((float)a - (float)b);
 }