Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div

7 files changed, 712 insertions, 949 deletions

diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 588019a2..e7e21a18 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -45,96 +45,15 @@ Qed.
 
 (** Return Address Offset *)
 
-Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop :=
-  Asmblockgenproof.return_address_offset (Machblockgen.transf_function f) (Machblockgen.trans_code c) ofs.
-
-
-(* TODO: put this proof in Machblocgen ? (it is specific to Machblocgen) *) 
-Lemma trans_code_monotonic c i b l:
-   trans_code c = b::l ->
-   exists l', exists b', trans_code (i::c) = l' ++ (b'::l).
-Proof.
-  destruct c as [|i' c]. { rewrite trans_code_equation; intros; congruence. }
-  destruct (get_code_nature (i :: i':: c)) eqn:GCNIC.
-  - apply get_code_nature_empty in GCNIC. discriminate.
-  - (* i=label *) 
-    destruct i; try discriminate.
-    rewrite! trans_code_equation;
-    remember (to_bblock (Mlabel l0 :: i' :: c)) as b0.
-    destruct b0 as [b0 c0].
-    exploit to_bblock_label; eauto.
-    intros (H1 & H2). rewrite H2; simpl; clear H2.
-    intros H2; inversion H2; subst.
-    exists nil; simpl; eauto.
-  - (*i=basic *) 
-    rewrite! trans_code_equation; destruct (to_basic_inst i) eqn:TBI; [| destruct i; discriminate].
-    destruct (cn_eqdec (get_code_nature (i':: c)) IsLabel).
-    + (* i'=label *) remember (to_bblock (i :: i' :: c)) as b1.
-      destruct b1 as [b1 c1].
-      assert (X: c1 = i'::c).
-      {  generalize Heqb1; clear Heqb1. 
-         unfold to_bblock.
-         erewrite to_bblock_header_noLabel; try congruence.
-         destruct i'; try discriminate.
-         destruct i; try discriminate; simpl;
-         intro X; inversion X; auto.
-      }
-      subst c1.
-      rewrite !trans_code_equation. intro H1; rewrite H1.
-      exists (b1 :: nil). simpl; eauto.
-    + (* i'<>label *) remember (to_bblock (i :: i' :: c)) as b1.
-      destruct b1 as [b1 c1].
-      remember (to_bblock (i' :: c)) as b2.
-      destruct b2 as [b2 c2].
-      intro H1; assert (X: c1=c2).
-      {  generalize Heqb1, Heqb2; clear Heqb1 Heqb2. 
-         unfold to_bblock.
-         erewrite to_bblock_header_noLabel; try congruence.
-         destruct i'; simpl in * |- ; try congruence;
-         destruct i; try discriminate; simpl;
-          try (destruct (to_bblock_body c) as [xx yy], (to_bblock_exit yy);
-              intros X1 X2; inversion X1; inversion X2; auto).
-      }
-      subst; inversion H1.
-      exists nil; simpl; eauto.
- - (* i=cfi *)
-   remember (to_cfi i) as cfi.
-   intros H. destruct cfi.
-   + erewrite trans_code_cfi; eauto.
-     rewrite H.
-     refine (ex_intro _ (_::nil) _). simpl; eauto.
-   + destruct i; simpl in * |-; try congruence.
-Qed.
-
-Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> 
-  exists b, (* Machblock.exit b = Some (Machblock.MBcall sg ros) /\ *) 
-     is_tail (b :: trans_code c) (trans_code c2).
-Proof.
-  intro H; induction 1. 
-  - intros; subst.
-    rewrite (trans_code_equation (Mcall sg ros :: c)).
-    simpl.
-    eapply ex_intro; eauto with coqlib.
-  - intros; exploit IHis_tail; eauto. clear IHis_tail.
-    intros (b & Hb).
-    + inversion Hb; clear Hb.
-      * exploit (trans_code_monotonic c2 i); eauto.
-        intros (l' & b' & Hl'); rewrite Hl'.
-        simpl; eauto with coqlib.
-      * exploit (trans_code_monotonic c2 i); eauto.
-        intros (l' & b' & Hl'); rewrite Hl'.
-        simpl; eapply ex_intro.
-        eapply is_tail_trans; eauto with coqlib.
-Qed.
+Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
+  Mach_return_address_offset Asmblockgenproof.return_address_offset.
 
 Lemma return_address_exists:
   forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
   exists ra, return_address_offset f c ra.
 Proof.
-  intros.
-  exploit Mach_Machblock_tail; eauto.
-  destruct 1.
-  eapply Asmblockgenproof.return_address_exists; eauto.
+  intros; unfold return_address_offset; eapply Mach_return_address_exists; eauto.
+  intros; eapply Asmblockgenproof.return_address_exists; eauto.
 Qed.
 
 
@@ -154,7 +73,6 @@ Proof.
   eapply compose_forward_simulations. 
   exploit Machblockgenproof.transf_program_correct; eauto.
   unfold Machblockgenproof.inv_trans_rao. 
-  intros X; apply X.
   eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
   eapply compose_forward_simulations. apply PostpassSchedulingproof.transf_program_correct; eauto.
   apply Asm.transf_program_correct. eauto.
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v
index 1d5555df..4dfc309e 100644
--- a/mppa_k1c/Machblockgen.v
+++ b/mppa_k1c/Machblockgen.v
@@ -15,552 +15,77 @@ Require Import Mach.
 Require Import Linking.
 Require Import Machblock.
 
+Inductive Machblock_inst: Type :=
+| MB_label (lbl: label) 
+| MB_basic (bi: basic_inst)
+| MB_cfi   (cfi: control_flow_inst).
 
-Fixpoint to_bblock_header (c: Mach.code): list label * Mach.code :=
-  match c with
-  | (Mlabel l)::c' => 
-      let (h, c'') := to_bblock_header c' in
-      (l::h, c'')
-  | _ => (nil, c)
-  end.
-
-Definition to_basic_inst(i: Mach.instruction): option basic_inst :=
+Definition trans_inst (i:Mach.instruction) : Machblock_inst :=
   match i with
-  | Mgetstack ofs ty dst          => Some (MBgetstack ofs ty dst)
-  | Msetstack src ofs ty          => Some (MBsetstack src ofs ty)
-  | Mgetparam ofs ty dst          => Some (MBgetparam ofs ty dst)
-  | Mop       op args res         => Some (MBop       op args res)
-  | Mload     chunk addr args dst => Some (MBload     chunk addr args dst)
-  | Mstore    chunk addr args src => Some (MBstore    chunk addr args src)
-  | _ => None
+  | Mcall sig ros         => MB_cfi (MBcall sig ros)
+  | Mtailcall sig ros     => MB_cfi (MBtailcall sig ros)
+  | Mbuiltin ef args res  => MB_cfi (MBbuiltin ef args res)
+  | Mgoto lbl             => MB_cfi (MBgoto lbl)
+  | Mcond cond args lbl   => MB_cfi (MBcond cond args lbl)
+  | Mjumptable arg tbl    => MB_cfi (MBjumptable arg tbl)
+  | Mreturn               => MB_cfi (MBreturn)
+  | Mgetstack ofs ty dst          => MB_basic (MBgetstack ofs ty dst)
+  | Msetstack src ofs ty          => MB_basic (MBsetstack src ofs ty)
+  | Mgetparam ofs ty dst          => MB_basic (MBgetparam ofs ty dst)
+  | Mop       op args res         => MB_basic (MBop       op args res)
+  | Mload     chunk addr args dst => MB_basic (MBload     chunk addr args dst)
+  | Mstore    chunk addr args src => MB_basic (MBstore    chunk addr args src)
+  | Mlabel l => MB_label l
   end.
 
-Fixpoint to_bblock_body(c: Mach.code): bblock_body * Mach.code :=
-  match c with
-  | nil => (nil,nil)
-  | i::c' =>
-    match to_basic_inst i with
-    | Some bi =>
-       let (p,c'') := to_bblock_body c' in
-       (bi::p, c'')
-    | None => (nil, c)
-    end
-  end.
+Definition empty_bblock:={| header := nil; body := nil; exit := None |}.
+Extraction Inline empty_bblock.
 
+Definition add_label l bb:={| header := l::(header bb); body := (body bb); exit := (exit bb) |}. 
+Extraction Inline add_label.
 
-Definition to_cfi (i: Mach.instruction): option control_flow_inst :=
-  match i with
-  | Mcall sig ros         => Some (MBcall sig ros)
-  | Mtailcall sig ros     => Some (MBtailcall sig ros)
-  | Mbuiltin ef args res  => Some (MBbuiltin ef args res)
-  | Mgoto lbl             => Some (MBgoto lbl)
-  | Mcond cond args lbl   => Some (MBcond cond args lbl)
-  | Mjumptable arg tbl    => Some (MBjumptable arg tbl)
-  | Mreturn               => Some (MBreturn)
-  | _ => None
-  end.
+Definition add_basic bi bb :={| header := nil; body := bi::(body bb); exit := (exit bb) |}.
+Extraction Inline add_basic.
 
-Definition to_bblock_exit (c: Mach.code): option control_flow_inst * Mach.code :=
-  match c with
-  | nil => (None,nil)
-  | i::c' =>
-    match to_cfi i with
-    | Some bi as o => (o, c')
-    | None => (None, c)
-    end
-  end.
-
-Inductive code_nature: Set := IsEmpty | IsLabel | IsBasicInst | IsCFI.
+Definition cfi_bblock cfi:={| header := nil; body := nil; exit := Some cfi |}.
+Extraction Inline cfi_bblock.
 
-Definition get_code_nature (c: Mach.code): code_nature :=
-  match c with
-  | nil => IsEmpty
-  | (Mlabel _)::_ => IsLabel
-  | i::_ => match to_basic_inst i with
-         | Some _ => IsBasicInst
-         | None => IsCFI
-         end
+Definition add_to_new_bblock (i:Machblock_inst) : bblock :=
+  match i with
+  | MB_label l => add_label l empty_bblock
+  | MB_basic i => add_basic i empty_bblock
+  | MB_cfi i => cfi_bblock i
   end.
 
-Lemma cn_eqdec (cn1 cn2: code_nature): { cn1=cn2 } + {cn1 <> cn2}.
-Proof.
-  decide equality.
-Qed.
-
-Lemma get_code_nature_nil c: c<>nil -> get_code_nature c <> IsEmpty.
-Proof.
-  intros H. unfold get_code_nature.
-  destruct c; try (contradict H; auto; fail).
-  destruct i; discriminate.
-Qed.
-
-Lemma get_code_nature_empty c: get_code_nature c = IsEmpty -> c = nil.
-Proof.
-  intros H. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto.
-  intro F. contradict F.
-Qed.
-
-Lemma to_bblock_header_noLabel c:
-  get_code_nature c <> IsLabel ->
-  to_bblock_header c = (nil, c).
-Proof.
-  intros H. destruct c as [|i c]; auto.
-  destruct i; simpl; auto.
-  contradict H; simpl; auto.
-Qed.
-
-Lemma to_bblock_header_wfe c:
-  forall h c0,
-  to_bblock_header c = (h, c0) ->
-  (length c >= length c0)%nat.
-Proof.
-  induction c as [ |i c]; simpl; intros h c' H.
-  - inversion H; subst; clear H; simpl; auto.
-  - destruct i; try (inversion H; subst; simpl; auto; fail).
-    remember (to_bblock_header c) as bhc; destruct bhc as [h0 c0].
-    inversion H; subst.
-    lapply (IHc h0 c'); auto.
-Qed.
-
-Lemma to_bblock_header_wf c b c0:
-  get_code_nature c = IsLabel ->
-  to_bblock_header c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intros H1 H2; destruct c; [ contradict H1; simpl; discriminate | ].
-  destruct i; try discriminate.
-  simpl in H2.
-  remember (to_bblock_header c) as bh; destruct bh as [h c''].
-  inversion H2; subst.
-  exploit to_bblock_header_wfe; eauto.
-  simpl; omega.
-Qed.
-
-Lemma to_bblock_body_noBasic c:
-  get_code_nature c <> IsBasicInst ->
-  to_bblock_body c = (nil, c).
-Proof.
-  intros H. destruct c as [|i c]; simpl; auto.
-  destruct i; simpl; auto.
-  all: contradict H; simpl; auto.
-Qed.
-
-Lemma to_bblock_body_wfe c b c0:
-  to_bblock_body c = (b, c0) ->
-  (length c >= length c0)%nat.
-Proof.
-  generalize b c0; clear b c0.
-  induction c as [|i c].
-  - intros b c0 H. simpl in H. inversion H; subst; auto.
-  - intros b c0 H. simpl in H. destruct (to_basic_inst i).
-    + remember (to_bblock_body c) as tbbc; destruct tbbc as [p c''].
-      exploit (IHc p c''); auto. inversion H; subst; simpl; omega.
-    + inversion H; subst; auto.
-Qed.
-
-(** Attempt to eliminate cons_to_bblock_body *)
-(*
-Lemma to_bblock_body_basic c:
-  get_code_nature c = IsBasicInst ->
-  exists i bi b c',
-     to_basic_inst i = Some bi
-  /\ c = i :: c'
-  /\ to_bblock_body c = (bi::b, snd (to_bblock_body c')).
-Proof.
-  intros H.
-  destruct c as [|i c]; try (contradict H; simpl; discriminate).
-  destruct i eqn:I; try (contradict H; simpl; discriminate).
-  all: simpl; destruct (to_bblock_body c)  as [p c''] eqn:TBBC; repeat (eapply ex_intro); (repeat split);
-    simpl; eauto; rewrite TBBC; simpl; eauto.
-Qed.
-
-Lemma to_bblock_body_wf c b c0:
-  get_code_nature c = IsBasicInst ->
-  to_bblock_body c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intros H1 H2; exploit to_bblock_body_basic; eauto.
-  intros X. destruct X as (i & bi & b' & c' & X1 & X2 & X3).
-  exploit to_bblock_body_wfe. eauto. subst. simpl.
-  rewrite X3 in H2. inversion H2; clear H2; subst.
-  simpl; omega.
-Qed.
-*)
-
-Inductive cons_to_bblock_body c0: Mach.code -> bblock_body -> Prop :=
-  Cons_to_bbloc_body i bi c' b':
-    to_basic_inst i = Some bi
-    -> to_bblock_body c' = (b', c0)
-    -> cons_to_bblock_body c0 (i::c') (bi::b').
-
-Lemma to_bblock_body_IsBasicInst c b c0:
-  get_code_nature c = IsBasicInst ->
-  to_bblock_body c = (b, c0) ->
-  cons_to_bblock_body c0 c b.
-Proof.
-  intros H1 H2. destruct c; [ contradict H1; simpl; discriminate | ].
-  remember (to_basic_inst i) as tbii. destruct tbii.
-  - simpl in H2. rewrite <- Heqtbii in H2.
-    remember (to_bblock_body c) as tbbc. destruct tbbc as [p1 c1].
-    inversion H2. subst. eapply Cons_to_bbloc_body; eauto.
-  - destruct i; try discriminate.
-Qed.
-
-Lemma to_bblock_body_wf c b c0:
-  get_code_nature c = IsBasicInst ->
-  to_bblock_body c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intros H1 H2; exploit to_bblock_body_IsBasicInst; eauto.
-  intros X. destruct X.
-  exploit to_bblock_body_wfe; eauto. subst. simpl.
-  simpl; omega.
-Qed.
-
-Lemma to_bblock_exit_noCFI c:
-  get_code_nature c <> IsCFI ->
-  to_bblock_exit c = (None, c).
-Proof.
-  intros H. destruct c as [|i c]; simpl; auto.
-  destruct i; simpl; auto.
-  all: contradict H; simpl; auto.
-Qed.
-
-Lemma to_bblock_exit_wf c b c0:
-  get_code_nature c = IsCFI ->
-  to_bblock_exit c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intros H1 H2. destruct c as [|i c]; try discriminate.
-  destruct i; try discriminate;
-  unfold to_bblock_header in H2; inversion H2; auto.
-Qed.
-
-Lemma to_bblock_exit_wfe c b c0:
-  to_bblock_exit c = (b, c0) ->
-  (length c >= length c0)%nat.
-Proof.
-  intros H. destruct c as [|i c].
-  - simpl in H. inversion H; subst; clear H; auto.
-  - destruct i; try ( simpl in H; inversion H; subst; clear H; auto ).
-    all: simpl; auto.
-Qed.
-
-Definition to_bblock(c: Mach.code): bblock * Mach.code :=
-  let (h,c0) := to_bblock_header c in
-  let (bdy, c1) := to_bblock_body c0 in
-  let (ext, c2) := to_bblock_exit c1 in
-  ({| header := h; body := bdy; exit := ext |}, c2)
-  .
-
-Lemma to_bblock_acc_label c l b c':
-  to_bblock c = (b, c') ->
-  to_bblock (Mlabel l :: c) = ({| header := l::(header b); body := (body b); exit := (exit b) |}, c').
-Proof.
-  unfold to_bblock; simpl.
-  remember (to_bblock_header c) as bhc; destruct bhc as [h c0].
-  remember (to_bblock_body c0) as bbc; destruct bbc as [bdy c1].
-  remember (to_bblock_exit c1) as bbc; destruct bbc as [ext c2].
-  intros H; inversion H; subst; clear H; simpl; auto.
-Qed.
-
-Lemma to_bblock_basic_then_label i c bi:
-  get_code_nature (i::c) = IsBasicInst ->
-  get_code_nature c = IsLabel ->
-  to_basic_inst i = Some bi ->
-  fst (to_bblock (i::c)) = {| header := nil; body := bi::nil; exit := None |}.
-Proof.
-  intros H1 H2 H3.
-  destruct c as [|i' c]; try (contradict H1; simpl; discriminate).
-  destruct i'; try (contradict H1; simpl; discriminate).
-  destruct i; simpl in *; inversion H3; subst; auto.
-Qed.
-
-Lemma to_bblock_CFI i c cfi:
-  get_code_nature (i::c) = IsCFI ->
-  to_cfi i = Some cfi ->
-  fst (to_bblock (i::c)) = {| header := nil; body := nil; exit := Some cfi |}.
-Proof.
-  intros H1 H2.
-  destruct i; try discriminate.
-  all: subst; rewrite <- H2; simpl; auto.
-Qed.
-
-Lemma to_bblock_noLabel c:
-  get_code_nature c <> IsLabel ->
-  fst (to_bblock c) = {|
-    header := nil;
-    body := body (fst (to_bblock c));
-    exit := exit (fst (to_bblock c))
-  |}.
-Proof.
-  intros H.
-  destruct c as [|i c]; simpl; auto.
-  apply bblock_eq; simpl;
-  destruct i; (
-      try (
-        remember (to_bblock _) as bb;
-        unfold to_bblock in *;
-        remember (to_bblock_header _) as tbh;
-        destruct tbh;
-        destruct (to_bblock_body _);
-        destruct (to_bblock_exit _);
-        subst; simpl; inversion Heqtbh; auto; fail
-      )
-    || contradict H; simpl; auto ).
-Qed.
-
-Lemma to_bblock_body_nil c c':
-  to_bblock_body c = (nil, c') ->
-  c = c'.
-Proof.
-  intros H.
-  destruct c as [|i c]; [ simpl in *; inversion H; auto |].
-  destruct i; try ( simpl in *; remember (to_bblock_body c) as tbc; destruct tbc as [p c'']; inversion H ).
-  all: auto.
-Qed.
-
-Lemma to_bblock_exit_nil c c':
-  to_bblock_exit c = (None, c') ->
-  c = c'.
-Proof.
-  intros H.
-  destruct c as [|i c]; [ simpl in *; inversion H; auto |].
-  destruct i; try ( simpl in *; remember (to_bblock_exit c) as tbe; destruct tbe as [p c'']; inversion H ).
-  all: auto.
-Qed.
-
-Lemma to_bblock_label b l c c':
-  to_bblock (Mlabel l :: c) = (b, c') ->
-  (header b) = l::(tail (header b)) /\ to_bblock c = ({| header:=tail (header b); body := body b; exit := exit b |}, c').
-Proof.
-  unfold to_bblock; simpl.
-  remember (to_bblock_header c) as bhc; destruct bhc as [h c0].
-  remember (to_bblock_body c0) as bbc; destruct bbc as [bdy c1].
-  remember (to_bblock_exit c1) as bbc; destruct bbc as [ext c2].
-  intros H; inversion H; subst; clear H; simpl; auto.
-Qed.
-
-Lemma to_bblock_basic c i bi:
-  get_code_nature (i::c) = IsBasicInst ->
-  to_basic_inst i = Some bi ->
-  get_code_nature c <> IsLabel ->
-  fst (to_bblock (i::c)) = {|
-    header := nil;
-    body := bi :: body (fst (to_bblock c));
-    exit := exit (fst (to_bblock c))
-  |}.
-Proof.
-  intros.
-  destruct c; try (destruct i; inversion H0; subst; simpl; auto; fail).
-  apply bblock_eq; simpl.
-(* header *)
-  + destruct i; simpl; auto; (
-      exploit to_bblock_noLabel; [rewrite H; discriminate | intro; rewrite H2; simpl; auto]).
-(* body *)
-(* FIXME - the proof takes some time to prove.. N² complexity :( *)
-  + unfold to_bblock.
-    remember (to_bblock_header _) as tbh; destruct tbh.
-    remember (to_bblock_body _) as tbb; destruct tbb.
-    remember (to_bblock_exit _) as tbe; destruct tbe.
-    simpl.
-    destruct i; destruct i0.
-    all: try (simpl in H1; contradiction).
-    all: try discriminate.
-    all: try (
-    simpl in Heqtbh; inversion Heqtbh; clear Heqtbh; subst;
-    simpl in Heqtbb; remember (to_bblock_body c) as tbbc; destruct tbbc;
-    inversion Heqtbb; clear Heqtbb; subst; simpl in *; clear H H1;
-    inversion H0; clear H0; subst; destruct (to_bblock_body c);
-    inversion Heqtbbc; clear Heqtbbc; subst;
-    destruct (to_bblock_exit c1); simpl; auto; fail).
-(* exit *)
-  + unfold to_bblock.
-    remember (to_bblock_header _) as tbh; destruct tbh.
-    remember (to_bblock_body _) as tbb; destruct tbb.
-    remember (to_bblock_exit _) as tbe; destruct tbe.
-    simpl.
-    destruct i; destruct i0.
-    all: try (simpl in H1; contradiction).
-    all: try discriminate.
-    all: try (
-    simpl in Heqtbh; inversion Heqtbh; clear Heqtbh; subst;
-    simpl in Heqtbb; remember (to_bblock_body c) as tbbc; destruct tbbc; 
-    inversion Heqtbb; clear Heqtbb; subst; simpl in *; clear H H1;
-    inversion H0; clear H0; subst; destruct (to_bblock_body c) eqn:TBBC;
-    inversion Heqtbbc; clear Heqtbbc; subst;
-    destruct (to_bblock_exit c1) eqn:TBBE; simpl;
-    inversion Heqtbe; clear Heqtbe; subst; auto; fail).
-Qed.
-
-Lemma to_bblock_size_single_label c i:
-  get_code_nature (i::c) = IsLabel ->
-  size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))).
-Proof.
-  intros H.
-  destruct i; try discriminate.
-  remember (to_bblock c) as bl. destruct bl as [b c'].
-  erewrite to_bblock_acc_label; eauto.
-  unfold size; simpl.
-  auto.
-Qed.
-
-Lemma to_bblock_size_label_neqz c:
-  get_code_nature c = IsLabel ->
-  size (fst (to_bblock c)) <> 0%nat.
-Proof.
-  destruct c as [ |i c]; try discriminate.
-  intros; rewrite to_bblock_size_single_label; auto.
-Qed.
-
-Lemma to_bblock_size_basic_neqz c:
-  get_code_nature c = IsBasicInst ->
-  size (fst (to_bblock c)) <> 0%nat.
-Proof.
-  intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate).
-  destruct i; try (contradict H; simpl; discriminate);
-  (
-    destruct (get_code_nature c) eqn:gcnc;
-    (* Case gcnc is not IsLabel *)
-    try (erewrite to_bblock_basic; eauto; [
-        unfold size; simpl; auto
-      | simpl; auto
-      | rewrite gcnc; discriminate
-    ]);
-    erewrite to_bblock_basic_then_label; eauto; [
-        unfold size; simpl; auto
-      | simpl; auto
-    ]
-  ).
-Qed.
-
-Lemma to_bblock_size_cfi_neqz c:
-  get_code_nature c = IsCFI ->
-  size (fst (to_bblock c)) <> 0%nat.
-Proof.
-  intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate).
-  destruct i; discriminate.
-Qed.
-
-Lemma to_bblock_size_single_basic c i:
-  get_code_nature (i::c) = IsBasicInst ->
-  get_code_nature c <> IsLabel ->
-  size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))).
-Proof.
-  intros.
-  destruct i; try (contradict H; simpl; discriminate); try (
-    (exploit to_bblock_basic; eauto);
-      [remember (to_basic_inst _) as tbi; destruct tbi; eauto |];
-    intro; rewrite H1; unfold size; simpl;
-    assert ((length (header (fst (to_bblock c)))) = 0%nat);
-      exploit to_bblock_noLabel; eauto; intro; rewrite H2; simpl; auto;
-    rewrite H2; auto
-  ).
-Qed.
-
-Lemma to_bblock_wf c b c0:
-  c <> nil ->
-  to_bblock c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intro H; lapply (get_code_nature_nil c); eauto.
-  intro H'; remember (get_code_nature c) as gcn.
-  unfold to_bblock.
-  remember (to_bblock_header c) as p1; eauto.
-  destruct p1 as [h c1].
-  intro H0.
-  destruct gcn.
-  - contradict H'; auto.
-  - exploit to_bblock_header_wf; eauto.
-    remember (to_bblock_body c1) as p2; eauto.
-    destruct p2 as [h2 c2].
-    exploit to_bblock_body_wfe; eauto.
-    remember (to_bblock_exit c2) as p3; eauto.
-    destruct p3 as [h3 c3].
-    exploit to_bblock_exit_wfe; eauto.
-    inversion H0. omega.
-  - exploit to_bblock_header_noLabel; eauto. rewrite <- Heqgcn. discriminate.
-    intro. rewrite H1 in Heqp1. inversion Heqp1. clear Heqp1. subst.
-    remember (to_bblock_body c) as p2; eauto.
-    destruct p2 as [h2 c2].
-    exploit to_bblock_body_wf; eauto.
-    remember (to_bblock_exit c2) as p3; eauto.
-    destruct p3 as [h3 c3].
-    exploit to_bblock_exit_wfe; eauto.
-    inversion H0. omega.
-  - exploit to_bblock_header_noLabel; eauto. rewrite <- Heqgcn. discriminate.
-    intro. rewrite H1 in Heqp1. inversion Heqp1; clear Heqp1; subst.
-    remember (to_bblock_body c) as p2; eauto.
-    destruct p2 as [h2 c2].
-    exploit (to_bblock_body_noBasic c); eauto. rewrite <- Heqgcn. discriminate.
-    intros H2; rewrite H2 in Heqp2; inversion Heqp2; clear Heqp2; subst.
-    remember (to_bblock_exit c) as p3; eauto.
-    destruct p3 as [h3 c3].
-    exploit (to_bblock_exit_wf c h3 c3); eauto.
-    inversion H0. omega.
-Qed.
-
-Lemma to_bblock_nonil i c0:
-  size (fst (to_bblock (i :: c0))) <> 0%nat.
-Proof.
-  intros H. remember (i::c0) as c. remember (get_code_nature c) as gcnc. destruct gcnc.
-  - contradict Heqgcnc. subst. simpl. destruct i; discriminate.
-  - eapply to_bblock_size_label_neqz; eauto.
-  - eapply to_bblock_size_basic_neqz; eauto.
-  - eapply to_bblock_size_cfi_neqz; eauto.
-Qed.
-
-Function trans_code (c: Mach.code) { measure length c }: code :=
+(* ajout d'une instruction en début d'une liste de blocks *)
+(* Soit /1\ ajout en tête de block, soit /2\ ajout dans un nouveau block*)
+(* bl est vide -> /2\ *)
+(* cfi -> /2\ (ajout dans exit)*)
+(* basic -> /1\ si header vide, /2\ si a un header *)
+(* label -> /1\ (dans header)*)
+Definition add_to_code (i:Machblock_inst) (bl:code) : code :=
+  match bl with
+  | bh::bl0 => match i with
+              | MB_label l => add_label l bh::bl0
+              | MB_cfi i0 => cfi_bblock i0::bl
+              | MB_basic i0 => match header bh with
+                               |_::_ => add_basic i0 empty_bblock::bl
+                               | nil => add_basic i0 bh::bl0
+                               end
+              end
+  | _ => add_to_new_bblock i::nil
+  end.
+  
+Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code := 
   match c with
-  | nil => nil
-  | _ =>
-     let (b, c0) := to_bblock c in
-     b::(trans_code c0)
+  | nil => bl
+  | i::c0 =>
+    trans_code_rev c0 (add_to_code (trans_inst i) bl)
   end.
-Proof.
-  intros; eapply to_bblock_wf; eauto. discriminate.
-Qed.
-
-Lemma trans_code_nonil c:
-  c <> nil -> trans_code c <> nil.
-Proof.
-  intros H.
-  induction c, (trans_code c) using trans_code_ind; simpl; auto. discriminate.
-Qed.
 
-Lemma trans_code_step c b lb0 hb c1 bb c2 eb c3:
-  trans_code c = b :: lb0 ->
-  to_bblock_header c = (hb, c1) ->
-  to_bblock_body c1 = (bb, c2) ->
-  to_bblock_exit c2 = (eb, c3) ->
-  hb = header b /\ bb = body b /\ eb = exit b /\ trans_code c3 = lb0.
-Proof.
-  intros.
-  induction c, (trans_code c) using trans_code_ind. discriminate. clear IHc0.
-  subst. destruct _x as [|i c]; try (contradict y; auto; fail).
-  inversion H; subst. clear H. unfold to_bblock in e0.
-  remember (to_bblock_header (i::c)) as hd. destruct hd as [hb' c1'].
-  remember (to_bblock_body c1') as bd. destruct bd as [bb' c2'].
-  remember (to_bblock_exit c2') as be. destruct be as [eb' c3'].
-  inversion e0. simpl.
-  inversion H0. subst.
-  rewrite <- Heqbd in H1. inversion H1. subst.
-  rewrite <- Heqbe in H2. inversion H2. subst.
-  auto.
-Qed.
+Function trans_code (c: Mach.code) : code :=
+  trans_code_rev (List.rev_append c nil) nil.
 
-Lemma trans_code_cfi i c cfi:
-  to_cfi i = Some cfi ->
-  trans_code (i :: c) = {| header := nil ; body := nil ; exit := Some cfi |} :: trans_code c.
-Proof.
-  intros. rewrite trans_code_equation. remember (to_bblock _) as tb; destruct tb as [b c0].
-  destruct i; try (contradict H; discriminate).
-  all: unfold to_bblock in Heqtb; remember (to_bblock_header _) as tbh; destruct tbh as [h c0'];
-      remember (to_bblock_body c0') as tbb; destruct tbb as [bdy c1'];
-      remember (to_bblock_exit c1') as tbe; destruct tbe as [ext c2]; simpl in *;
-      inversion Heqtbh; subst; inversion Heqtbb; subst; inversion Heqtbe; subst;
-      inversion Heqtb; subst; rewrite H; auto.
-Qed.
 
 (* à finir pour passer des Mach.function au function, etc. *)
 Definition transf_function (f: Mach.function) : function :=
@@ -576,3 +101,107 @@ Definition transf_fundef (f: Mach.fundef) : fundef :=
 
 Definition transf_program (src: Mach.program) : program :=
   transform_program transf_fundef src.
+
+
+(** Abstraction de trans_code *)
+
+Inductive is_end_block: Machblock_inst -> code -> Prop :=
+  | End_empty mbi: is_end_block mbi nil
+  | End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl)
+  | End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl. 
+
+Local Hint Resolve End_empty End_basic End_cfi.
+
+Inductive is_trans_code: Mach.code -> code -> Prop :=
+  | Tr_nil: is_trans_code nil nil
+  | Tr_end_block i c bl:
+      is_trans_code c bl ->
+      is_end_block (trans_inst i) bl ->
+      is_trans_code (i::c) (add_to_new_bblock (trans_inst i)::bl)
+  | Tr_add_label i l bh c bl:
+      is_trans_code c (bh::bl) ->
+      i = Mlabel l ->
+      is_trans_code (i::c) (add_label l bh::bl)
+  | Tr_add_basic i bi bh c bl:
+      is_trans_code c (bh::bl) ->
+      trans_inst i = MB_basic bi ->
+      header bh = nil ->
+      is_trans_code (i::c) (add_basic bi bh::bl).
+
+Local Hint Resolve Tr_nil Tr_end_block.
+
+Lemma add_to_code_is_trans_code i c bl:
+  is_trans_code c bl ->
+  is_trans_code (i::c) (add_to_code (trans_inst i) bl).
+Proof.
+  destruct bl as [|bh0 bl]; simpl.
+  - intro H. inversion H. subst. eauto.
+  - remember (trans_inst i) as ti.
+    destruct ti as [l|bi|cfi].
+    + intros; eapply Tr_add_label; eauto. destruct i; simpl in * |- *; congruence.
+    + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b].
+      * eapply Tr_add_basic; eauto.
+      * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto.
+        rewrite Heqti; eapply Tr_end_block; eauto.
+        rewrite <- Heqti. eapply End_basic. congruence.
+    + intros.
+      cutrewrite (cfi_bblock cfi = add_to_new_bblock (MB_cfi cfi)); auto.
+      rewrite Heqti. eapply Tr_end_block; eauto.
+      rewrite <- Heqti. eapply End_cfi. congruence.
+Qed.
+
+Local Hint Resolve add_to_code_is_trans_code.
+
+Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, 
+  is_trans_code c2 mbi ->
+  is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi).
+Proof.
+  induction c1 as [| i c1]; simpl; auto.
+Qed.
+
+Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c).
+Proof.
+  unfold trans_code.
+  rewrite <- rev_alt.
+  rewrite <- (rev_involutive c) at 1.
+  rewrite rev_alt at 1.
+  apply trans_code_is_trans_code_rev; auto.
+Qed.
+
+Lemma add_to_code_is_trans_code_inv i c bl:
+  is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0.
+Proof.
+  intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto.
+  + (* case Tr_end_block *) inversion H3; subst; simpl; auto.
+     * destruct (header bh); congruence.
+     * destruct bl0; simpl; congruence.
+  + (* case Tr_add_basic *) rewrite H3. simpl. destruct (header bh); congruence.
+Qed. 
+
+Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi, 
+  is_trans_code (rev_append c1 c2) mbi ->
+  exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0.
+Proof.
+  induction c1 as [| i c1]; simpl; eauto.
+  intros; exploit IHc1; eauto.
+  intros (mbi0 & H1 & H2); subst.
+  exploit add_to_code_is_trans_code_inv; eauto.
+  intros. destruct H0 as [mbi1 [H2 H3]].
+  exists mbi1. split; congruence.
+Qed.
+
+Local Hint Resolve trans_code_is_trans_code.
+
+Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c).
+Proof.
+  constructor; intros; subst; auto.
+  unfold trans_code.
+  exploit (trans_code_is_trans_code_rev_inv (rev_append c nil) nil bl); eauto.
+  * rewrite <- rev_alt.
+    rewrite <- rev_alt.
+    rewrite (rev_involutive c).
+    apply H.
+  * intros.
+    destruct H0 as [mbi [H0 H1]].
+    inversion H0. subst. reflexivity.
+Qed.
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v
index 62c1e0ed..9186e54a 100644
--- a/mppa_k1c/Machblockgenproof.v
+++ b/mppa_k1c/Machblockgenproof.v
@@ -17,6 +17,11 @@ Require Import Machblock.
 Require Import Machblockgen.
 Require Import ForwardSimulationBlock.
 
+Ltac subst_is_trans_code H :=
+  rewrite is_trans_code_inv in H;
+  rewrite <- H in * |- *;
+  rewrite <- is_trans_code_inv in H.
+
 Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.function) (c: Mach.code) :=
   rao (transf_function f) (trans_code c).
 
@@ -39,7 +44,7 @@ Fixpoint trans_stack (mst: list Mach.stackframe) : list stackframe :=
   | msf :: mst0 => (trans_stackframe msf) :: (trans_stack mst0)
   end.
 
-Definition trans_state (ms: Mach.state) : state :=
+Definition trans_state (ms: Mach.state): state :=
   match ms with
   | Mach.State        s f sp c rs m => State        (trans_stack s) f sp (trans_code c) rs m
   | Mach.Callstate    s f rs m      => Callstate    (trans_stack s) f rs m
@@ -163,6 +168,35 @@ Proof.
     + revert H. unfold Mach.find_label. simpl. rewrite peq_false; auto.
 Qed.
 
+Lemma find_label_is_end_block_not_label i l c bl:
+      is_end_block (trans_inst i) bl ->
+      is_trans_code c bl ->
+      i <> Mlabel l -> find_label l (add_to_new_bblock (trans_inst i) :: bl) = find_label l bl.  
+Proof.
+  intros H H0 H1.
+  unfold find_label.
+  remember (is_label l _) as b.
+  cutrewrite (b = false); auto.
+  subst; unfold is_label.
+  destruct i; simpl in * |- *; try (destruct (in_dec l nil); intuition).
+  inversion H.
+  destruct (in_dec l (l0::nil)) as [H6|H6]; auto.
+  simpl in H6; intuition try congruence.
+Qed.
+
+Lemma find_label_at_begin l bh bl:
+  In l (header bh)
+  -> find_label l (bh :: bl) = Some (bh::bl).
+Proof.
+  unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; simpl; auto.
+Qed.
+
+Lemma find_label_add_label_diff l bh bl:
+      ~(In l (header bh)) -> 
+      find_label l (bh::bl) = find_label l bl.
+Proof.
+  unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; simpl; auto.
+Qed.
 
 Definition concat (h: list label) (c: code): code :=
   match c with
@@ -170,128 +204,69 @@ Definition concat (h: list label) (c: code): code :=
   | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c'
   end.
 
-Lemma to_bblock_start_label i c l b c0: 
-  (b, c0) = to_bblock (i :: c)
-  -> In l (header b)
-  -> i <> Mlabel l
-  -> exists l2, i=Mlabel l2.
-Proof.
-   unfold to_bblock.
-   remember (to_bblock_header _) as bh; destruct bh as [h c1].
-   remember (to_bblock_body _) as bb; destruct bb as [bdy c2].
-   remember (to_bblock_exit _) as be; destruct be as [ext c3].
-   intros H; inversion H; subst; clear H; simpl.
-   destruct i; try (simpl in Heqbh; inversion Heqbh; subst; clear Heqbh; simpl; intuition eauto).
-Qed.
-
-Lemma find_label_stop c:
- forall l b c0 c',
-   (b, c0) = to_bblock c
- -> Mach.find_label l c = Some c'
- -> In l (header b)
- -> exists h, In l h /\ Some (b :: trans_code c0) = Some (concat h (trans_code c')).
-Proof.
-  induction c as [ |i c].
-  - simpl; intros; discriminate.
-  - intros l b c0 c' H H1 H2.
-    exploit Mach_find_label_split; eauto; clear H1.
-    intros [(X1 & X2) | (X1 & X2)].
-    * subst. exploit to_bblock_label; eauto. clear H.
-      intros (H3 & H4). constructor 1 with (x:=l::nil); simpl; intuition auto.
-      symmetry.
-      rewrite trans_code_equation.
-      destruct c as [ |i c].
-      + unfold to_bblock in H4; simpl in H4.
-        injection H4. clear H4; intros H4 H H0 H1; subst. simpl.
-        rewrite trans_code_equation; simpl.
-        rewrite <- H1 in H3; clear H1.
-        destruct b as [h b e]; simpl in * |- *; subst; auto.
-      + rewrite H4; clear H4; simpl. rewrite <- H3; clear H3.
-        destruct b; simpl; auto.
-    * exploit to_bblock_start_label; eauto.
-      intros (l' & H'). subst.
-      assert (X: l' <> l). { intro Z; subst; destruct X1; auto. }
-      clear X1.
-      exploit to_bblock_label; eauto. clear H.
-      intros (H3 & H4).
-      exploit IHc; eauto. { simpl. rewrite H3 in H2; simpl in H2. destruct H2; subst; tauto. }
-      intros (h' & H5 & H6).
-      constructor 1 with (x:=l'::h'); simpl; intuition auto.
-      destruct b as [h b e]; simpl in * |- *; subst.
-      remember (tl h) as th. subst h.
-      remember (trans_code c') as tcc'.
-      rewrite trans_code_equation in Heqtcc'.
-      destruct c'; subst; simpl in * |- *. 
-      + inversion H6; subst; auto.
-      + destruct (to_bblock (i :: c')) as [b1 c1]. simpl in * |- *.
-        inversion H6; subst; auto.
-Qed.
-
-Lemma to_bblock_header_find_label c l: forall c1 h c',
-  to_bblock_header c = (h, c1)
-  -> Mach.find_label l c = Some c'
-  -> ~ In l h
-  -> Mach.find_label l c = Mach.find_label l c1.
-Proof.
-  induction c as [|i  c]; simpl; auto.
-  - intros; discriminate.
-  - destruct i;
-    try (simpl; intros c1 h c' H1 H2; inversion H1; subst; clear H1; intros; apply refl_equal).
-    remember (to_bblock_header c) as tbhc. destruct tbhc as [h2 c2].
-    intros h c1 c' H1; inversion H1; subst; clear H1.
-    simpl. destruct (peq _ _).
-    + subst; tauto.
-    + intros H1 H2; erewrite IHc; eauto.
-Qed.
-
-Lemma to_bblock_body_find_label c1 l: forall c2 bdy,
-  (bdy, c2) = to_bblock_body c1 ->
-  Mach.find_label l c1 = Mach.find_label l c2.
-Proof.
-  induction c1 as [|i c1].
-  - intros bdy0 c0 H. simpl in H. inversion H; subst; clear H. auto.
-  - intros bdy' c2' H. simpl in H. destruct i; try (
-      simpl in H; remember (to_bblock_body c1) as tbb; destruct tbb as [p c''];
-      inversion H; subst; clear H; simpl; erewrite IHc1; eauto; fail).
-Qed.
-
-Lemma to_bblock_exit_find_label c1 l c2 ext:
- (ext, c2) = to_bblock_exit c1
- -> Mach.find_label l c1 = Mach.find_label l c2.
-Proof.
-  intros H. destruct c1 as [|i c1].
-  - simpl in H. inversion H; subst; clear H. auto.
-  - destruct i; try (
-      simpl in H; inversion H; subst; clear H; auto; fail).
-Qed.
-
 Lemma find_label_transcode_preserved:
   forall l c c',
   Mach.find_label l c = Some c' ->
   exists h, In l h /\ find_label l (trans_code c) = Some (concat h (trans_code c')).
 Proof.
-  intros l c; induction c, (trans_code c) using trans_code_ind.
-  - intros c' H; inversion H.
-  - intros c' H. subst _x. destruct c as [| i c]; try tauto.
-   unfold to_bblock in * |-.
-   remember (to_bblock_header _) as bh; destruct bh as [h c1].
-   remember (to_bblock_body _) as bb; destruct bb as [bdy c2].
-   remember (to_bblock_exit _) as be; destruct be as [ext c3].
-   simpl; injection e0; intros; subst; clear e0.
-   unfold is_label; simpl; destruct (in_dec l h) as [Y|Y].
-   + clear IHc0.
-     eapply find_label_stop; eauto.
-     unfold to_bblock.
-     rewrite <- Heqbh, <- Heqbb, <- Heqbe. 
-     auto.
-   + exploit IHc0; eauto. clear IHc0.
-     rewrite <- H.
-     erewrite (to_bblock_header_find_label (i::c) l c1); eauto.
-     erewrite (to_bblock_body_find_label c1 l c2); eauto.
-     erewrite (to_bblock_exit_find_label c2 l c0); eauto.
+  intros l c. remember (trans_code _) as bl.
+  rewrite <- is_trans_code_inv in * |-.
+  induction Heqbl. 
+  + (* Tr_nil *) 
+    intros; exists (l::nil); simpl in * |- *; intuition.
+    discriminate.
+  + (* Tr_end_block *)
+    intros.
+    exploit Mach_find_label_split; eauto.
+    clear H0; destruct 1 as [(H0&H2)|(H0&H2)].
+    - subst. rewrite find_label_at_begin; simpl; auto.
+      inversion H as [mbi H1 H2| | ].
+      subst.
+      inversion Heqbl.
+      subst.
+      exists (l :: nil); simpl; eauto.
+    - exploit IHHeqbl; eauto.
+      destruct 1 as (h & H3 & H4).
+      exists h.
+      split; auto.
+      erewrite find_label_is_end_block_not_label;eauto.
+  + (* Tr_add_label *)
+    intros.
+    exploit Mach_find_label_split; eauto.
+    clear H0; destruct 1 as [(H0&H2)|(H0&H2)].
+    - subst.
+      inversion H0 as [H1].
+      clear H0.
+      erewrite find_label_at_begin; simpl; eauto.
+      subst_is_trans_code Heqbl.
+      exists (l :: nil); simpl; eauto.
+    - subst; assert (H: l0 <> l); try congruence; clear H0.
+      exploit IHHeqbl; eauto.
+      clear IHHeqbl Heqbl.
+      intros (h & H3 & H4).
+      simpl; unfold is_label, add_label; simpl.
+      destruct (in_dec l (l0::header bh)) as [H5|H5]; simpl in H5.
+      * destruct H5; try congruence.
+        exists (l0::h); simpl; intuition.
+        rewrite find_label_at_begin in H4; auto.
+        apply f_equal. inversion H4 as [H5]. clear H4.
+        destruct (trans_code c'); simpl in * |- *;
+        inversion H5; subst; simpl; auto.
+      * exists h. intuition.
+        erewrite <- find_label_add_label_diff; eauto.
+  + (* Tr_add_basic *)
+    intros.
+    exploit Mach_find_label_split; eauto.
+    destruct 1 as [(H2&H3)|(H2&H3)].
+    rewrite H2 in H. unfold trans_inst in H. congruence.
+    exploit IHHeqbl; eauto.
+    clear IHHeqbl Heqbl.
+    intros (h & H4 & H5).
+    rewrite find_label_add_label_diff; auto.
+    rewrite find_label_add_label_diff in H5; eauto.
+    rewrite H0; auto.
 Qed.
 
-
 Lemma find_label_preserved:
   forall l f c,
   Mach.find_label l (Mach.fn_code f) = Some c ->
@@ -311,8 +286,12 @@ Qed.
 Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated
                    parent_sp_preserved.
 
-Definition dist_end_block_code (c: Mach.code) := (size (fst (to_bblock c))-1)%nat.
 
+Definition dist_end_block_code (c: Mach.code) := 
+ match trans_code c with
+ | nil => 0
+ | bh::_ => (size bh-1)%nat
+ end.
 
 Definition dist_end_block (s: Mach.state): nat :=
   match s with
@@ -323,65 +302,174 @@ Definition dist_end_block (s: Mach.state): nat :=
 Local Hint Resolve exec_nil_body exec_cons_body.
 Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore.
 
-Ltac ExploitDistEndBlockCode :=
-  match goal with
-  | [ H : dist_end_block_code (Mlabel ?l :: ?c) <> 0%nat |- _ ] =>
-      exploit (to_bblock_size_single_label c (Mlabel l)); eauto
-  | [ H : dist_end_block_code (?i0 :: ?c) <> 0%nat |- _ ] =>
-      exploit (to_bblock_size_single_basic c i0); eauto
-  | _ => idtac
-  end.
+Lemma size_add_label l bh: size (add_label l bh) = size bh + 1.
+Proof.
+  unfold add_label, size; simpl; omega.
+Qed.
+
+Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1.
+Proof.
+  intro H. unfold add_basic, size; rewrite H; simpl. omega.
+Qed.
+
+
+Lemma size_add_to_newblock i: size (add_to_new_bblock i) = 1.
+Proof.
+  destruct i; auto.
+Qed.
 
-Ltac totologize H :=
-  match type of H with
-  | ( ?id = _ ) =>
-    let Hassert := fresh "Htoto" in (
-    assert (id = id) as Hassert; auto; rewrite H in Hassert at 2; simpl in Hassert; rewrite H in Hassert)
-  end.
 
 Lemma dist_end_block_code_simu_mid_block i c:
   dist_end_block_code (i::c) <> 0 ->
   (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c)).
 Proof.
-  intros H.
   unfold dist_end_block_code.
-  destruct (get_code_nature (i::c)) eqn:GCNIC.
-  - apply get_code_nature_empty in GCNIC. discriminate.
-  - rewrite to_bblock_size_single_label; auto.
-    destruct c as [|i' c].
-    + contradict H. destruct i; simpl; auto.
-    + assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil. omega. 
-  - destruct (get_code_nature c) eqn:GCNC.
-    + apply get_code_nature_empty in GCNC. subst. contradict H. destruct i; simpl; auto.
-    + contradict H. destruct c as [|i' c]; try discriminate.
-      destruct i'; try discriminate.
-      destruct i; try discriminate. all: simpl; auto.
-    + destruct (to_basic_inst i) eqn:TBI; [| destruct i; discriminate].
-      erewrite to_bblock_basic; eauto; [| rewrite GCNC; discriminate ].
-      simpl. destruct c as [|i' c]; try discriminate.
-      assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil.
-      cutrewrite (Datatypes.S (size (fst (to_bblock (i'::c))) - 1) = size (fst (to_bblock (i'::c)))).
-      unfold size. cutrewrite (length (header (fst (to_bblock (i' :: c)))) = 0). simpl. omega.
-      rewrite to_bblock_noLabel. simpl; auto.
-      rewrite GCNC. discriminate.
-      omega.
-    + destruct (to_basic_inst i) eqn:TBI; [| destruct i; discriminate].
-      erewrite to_bblock_basic; eauto; [| rewrite GCNC; discriminate ].
-      simpl. destruct c as [|i' c]; try discriminate.
-      assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil.
-      cutrewrite (Datatypes.S (size (fst (to_bblock (i'::c))) - 1) = size (fst (to_bblock (i'::c)))).
-      unfold size. cutrewrite (length (header (fst (to_bblock (i' :: c)))) = 0). simpl. omega.
-      rewrite to_bblock_noLabel. simpl; auto.
-      rewrite GCNC. discriminate.
-      omega.
-  - contradict H. destruct i; try discriminate.
-    all: unfold dist_end_block_code; erewrite to_bblock_CFI; eauto; simpl; eauto.
+  remember (trans_code (i::c)) as bl.
+  rewrite <- is_trans_code_inv in Heqbl.
+  inversion Heqbl as [|bl0 H| |]; subst; clear Heqbl.
+  - rewrite size_add_to_newblock; omega.
+  - rewrite size_add_label;
+    subst_is_trans_code H.
+    omega.
+  - rewrite size_add_basic; auto.
+    subst_is_trans_code H. 
+    omega.
 Qed.
 
 Local Hint Resolve dist_end_block_code_simu_mid_block.
 
+
+Lemma size_nonzero c b bl:
+  is_trans_code c (b :: bl) -> size b <> 0.
+Proof.
+   intros H; inversion H; subst.
+   - rewrite size_add_to_newblock; omega.
+   - rewrite size_add_label; omega.
+   - rewrite size_add_basic; auto; omega.
+Qed.
+
+Inductive is_header: list label -> Mach.code -> Mach.code -> Prop :=
+  | header_empty : is_header nil nil nil
+  | header_not_label i c: (forall l, i <> Mlabel l) -> is_header nil (i::c) (i::c)
+  | header_is_label l h c c0: is_header h c c0 -> is_header (l::h) ((Mlabel l)::c) c0
+ .
+
+Inductive is_body: list basic_inst -> Mach.code -> Mach.code -> Prop :=
+  | body_empty : is_body nil nil nil
+  | body_not_bi i c: (forall bi, (trans_inst i) <> (MB_basic bi)) -> is_body nil (i::c) (i::c)
+  | body_is_bi i lbi c0 c1 bi: (trans_inst i) = MB_basic bi -> is_body lbi c0 c1 -> is_body (bi::lbi) (i::c0) c1
+ .
+
+Inductive is_exit: option control_flow_inst -> Mach.code -> Mach.code -> Prop :=
+  | exit_empty: is_exit None nil nil
+  | exit_not_cfi i c: (forall cfi, (trans_inst i) <> MB_cfi cfi) -> is_exit None (i::c) (i::c)
+  | exit_is_cfi i c cfi: (trans_inst i) = MB_cfi cfi -> is_exit (Some cfi) (i::c) c
+ .
+
+Lemma Mlabel_is_not_basic i:
+  forall bi, trans_inst i = MB_basic bi -> forall l, i <> Mlabel l.
+Proof.
+intros.
+unfold trans_inst in H. 
+destruct i; congruence. 
+Qed.
+
+Lemma Mlabel_is_not_cfi i:
+  forall cfi, trans_inst i = MB_cfi cfi -> forall l, i <> Mlabel l.
+Proof.
+intros.
+unfold trans_inst in H. 
+destruct i; congruence. 
+Qed.
+
+Lemma MBbasic_is_not_cfi i:
+  forall cfi, trans_inst i = MB_cfi cfi -> forall bi, trans_inst i <> MB_basic bi.
+Proof.
+intros.
+unfold trans_inst in H.
+unfold trans_inst. 
+destruct i; congruence. 
+Qed.
+
+
+Local Hint Resolve Mlabel_is_not_cfi.
+Local Hint Resolve MBbasic_is_not_cfi.
+
+Lemma add_to_new_block_is_label i:
+  header (add_to_new_bblock (trans_inst i)) <> nil -> exists l, i = Mlabel l.
+Proof.
+  intros.
+  unfold add_to_new_bblock in H.
+  destruct (trans_inst i) eqn : H1. 
+  + exists lbl. 
+    unfold trans_inst in H1. 
+    destruct i; congruence.
+  + unfold add_basic in H; simpl in H; congruence.
+  + unfold cfi_bblock in H; simpl in H; congruence.
+Qed.
+
+Local Hint Resolve Mlabel_is_not_basic.
+
+Lemma trans_code_decompose c: forall b bl,
+  is_trans_code c (b::bl) ->
+  exists c0 c1 c2, is_header (header b) c c0 /\ is_body (body b) c0 c1 /\ is_exit (exit b) c1 c2 /\ is_trans_code c2 bl.
+Proof.
+  induction c as [|i c].
+  { (* nil => absurd *) intros b bl H; inversion H. }
+  intros b bl H; remember (trans_inst i) as ti.
+  destruct ti as [lbl|bi|cfi];
+  inversion H as [|d0 d1 d2 H0 H1| |]; subst;
+  try (rewrite <- Heqti in * |- *); simpl in * |- *;
+  try congruence.
+  + (* label at end block *)
+    inversion H1; subst. inversion H0; subst.
+    assert (X:i=Mlabel lbl). { destruct i; simpl in Heqti; congruence. }
+    subst. repeat econstructor; eauto.
+  + (* label at mid block *)
+    exploit IHc; eauto.
+    intros (c0 & c1 & c2 & H1 & H2 & H3 & H4).
+    repeat econstructor; eauto.
+  + (* basic at end block *)
+    inversion H1; subst.
+    lapply (Mlabel_is_not_basic i bi); auto.
+    intro H2.
+    - inversion H0; subst.
+      assert (X:(trans_inst i) = MB_basic bi ). { repeat econstructor; congruence. }
+      repeat econstructor; congruence.
+    - exists (i::c), c, c.
+      repeat econstructor; eauto; inversion H0; subst; repeat econstructor; simpl; try congruence.
+      * exploit (add_to_new_block_is_label i0); eauto.
+        intros (l & H8); subst; simpl; congruence.
+      * exploit H3; eauto.
+      * exploit (add_to_new_block_is_label i0); eauto.
+        intros (l & H8); subst; simpl; congruence.
+  + (* basic at mid block *)
+    inversion H1; subst.
+    exploit IHc; eauto.
+    intros (c0 & c1 & c2 & H3 & H4 & H5 & H6).
+    exists (i::c0), c1, c2.
+    repeat econstructor; eauto.
+    rewrite H2 in H3.
+    inversion H3; econstructor; eauto.
+  + (* cfi at end block *)
+    inversion H1; subst;
+    repeat econstructor; eauto.
+Qed.
+
+
+Lemma step_simu_header st f sp rs m s c h c' t: 
+ is_header h c c' ->
+ starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> 
+ s = Mach.State st f sp c' rs m /\ t = E0.
+Proof.
+  induction 1; simpl; intros hs; try (inversion hs; tauto).
+  inversion hs as [|n1 s1 t1 t2 s2 t3 s3 H1]. inversion H1. subst. auto. 
+Qed.
+
+
+
 Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) s f sp rs m (t:trace) (s':Mach.state):
-  to_basic_inst i = Some bi ->
+  trans_inst i = MB_basic bi ->
   Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' ->
   exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'.
 Proof.
@@ -400,80 +488,71 @@ Proof.
 Qed.
 
 
-Lemma star_step_simu_body_step s f sp c:
- forall (p:bblock_body) c' rs m t s',
-  to_bblock_body c = (p, c') ->
-  starN (Mach.step (inv_trans_rao rao)) ge (length p) (Mach.State s f sp c rs m) t s' ->
-  exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp p rs m rs' m'.
-Proof.
-  induction c as [ | i0 c0 Hc0]; simpl; intros p c' rs m t s' H.
-  * (* nil *)
-    inversion_clear H; simpl; intros X; inversion_clear X.
-    eapply ex_intro; eapply ex_intro; intuition eauto.
-  * (* cons *)
-    remember (to_basic_inst i0) as o eqn:Ho.
-    destruct o as [bi |].
-    + (* to_basic_inst i0 = Some bi *)
-      remember (to_bblock_body c0) as r eqn:Hr.
-      destruct r as [p1 c1]; inversion H; simpl; subst; clear H.
-      intros X; inversion_clear X.
-      exploit step_simu_basic_step; eauto.
-      intros [rs' [m' [H2 [H3 H4]]]]; subst.
-      exploit Hc0; eauto.
-      intros [rs'' [m'' [H5 [H6 H7]]]]; subst.
-      refine (ex_intro _ rs'' (ex_intro _ m'' _)); intuition eauto.
-   + (* to_basic_inst i0 = None *)
-     inversion_clear H; simpl.
-     intros X; inversion_clear X. intuition eauto.
-Qed.
+Lemma star_step_simu_body_step s f sp c bdy c':
+  is_body bdy c c' -> forall rs m t s',
+  starN (Mach.step (inv_trans_rao rao)) ge (length bdy) (Mach.State s f sp c rs m) t s' ->
+  exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp bdy rs m rs' m'.
+Proof.
+  induction 1; simpl.
+  + intros. inversion H. exists rs. exists m. auto.
+  + intros. inversion H0. exists rs. exists m. auto.
+  + intros. inversion H1; subst. 
+    exploit (step_simu_basic_step ); eauto. 
+    destruct 1 as [ rs1 [ m1 Hs]].
+    destruct Hs as [Hs1 [Hs2 Hs3]].
+    destruct (IHis_body rs1 m1 t2 s') as [rs2 Hb]. rewrite <- Hs1; eauto.
+    destruct Hb as [m2 [Hb1 [Hb2 Hb3]]].
+    exists rs2, m2.
+    rewrite Hs2, Hb2; eauto.
+    Qed. 
 
 Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit.
 Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same.
 
+
 Lemma match_states_concat_trans_code st f sp c rs m h: 
   match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m).
 Proof.
-  constructor 1; simpl.
+  intros; constructor 1; simpl.
   + intros (t0 & s1' & H0) t s'. 
-    rewrite! trans_code_equation.
-    destruct c as [| i c]. { inversion H0. }
-    remember (to_bblock (i :: c)) as bic. destruct bic as [b c0].
-    simpl.
-    constructor 1; intros H; inversion H; subst; simpl in * |- *;
-    eapply exec_bblock; eauto.
-    - inversion H11; subst; eauto.
-      inversion H2; subst; eauto.
-    - inversion H11; subst; simpl; eauto.
-      inversion H2; subst; simpl; eauto.
+    remember (trans_code _) as bl.
+    destruct bl as [|bh bl]. 
+    { rewrite <- is_trans_code_inv in Heqbl; inversion Heqbl; inversion H0; congruence. } 
+    clear H0.
+    simpl; constructor 1; 
+    intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; simpl in * |- *; 
+    eapply exec_bblock; eauto; simpl;
+    inversion X2 as [cfi d1 d2 d3 H1|]; subst; eauto;
+    inversion H1; subst; eauto.
   + intros H r; constructor 1; intro X; inversion X.
 Qed.
 
-Lemma step_simu_cfi_step:
-  forall c e c' stk f sp rs m t s' b lb',
-  to_bblock_exit c = (Some e, c') ->
-  trans_code c' = lb' ->
-  Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp c rs m) t s' ->
-  exists s2, cfi_step rao tge e (State (trans_stack stk) f sp (b::lb') rs m) t s2 /\ match_states s' s2.
+Lemma step_simu_cfi_step (i: Mach.instruction) (cfi: control_flow_inst) (c: Mach.code) (blc:code) stk f sp rs m (t:trace) (s':Mach.state) b:
+  trans_inst i = MB_cfi cfi ->
+  is_trans_code c blc ->
+  Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp (i::c) rs m) t s' ->
+  exists s2, cfi_step rao tge cfi (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s' s2.
 Proof.
-  intros c e c' stk f sp rs m t s' b lb'.
-  intros Hexit Htc Hstep.
-  destruct c as [|ei c]; try (contradict Hexit; discriminate).
-  destruct ei; (contradict Hexit; discriminate) || (
-    inversion Hexit; subst; inversion Hstep; subst; simpl
-  ).
-  * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto.
-    apply exec_MBcall with (f := (transf_function f0)); auto.
-    rewrite find_function_ptr_same in H9; auto.
-  * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto.
-    apply exec_MBtailcall with (f := (transf_function f0)); auto.
-    rewrite find_function_ptr_same in H9; auto.
-    rewrite parent_sp_preserved in H11; subst; auto.
-    rewrite parent_ra_preserved in H12; subst; auto.
-  * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto.
-    eapply exec_MBbuiltin; eauto.
-  * exploit find_label_transcode_preserved; eauto. intros (h & X1 & X2).
+  destruct i; simpl in * |-;
+  (intro H; intro Htc;apply is_trans_code_inv in Htc;rewrite Htc;inversion_clear H;intro X; inversion_clear X).
+  * eapply ex_intro.
+    intuition auto.
+    eapply exec_MBcall;eauto. 
+    rewrite <-H; exploit (find_function_ptr_same); eauto.
+  * eapply ex_intro.
+    intuition auto.
+    eapply exec_MBtailcall;eauto. 
+    - rewrite <-H; exploit (find_function_ptr_same); eauto.
+    - simpl; rewrite <- parent_sp_preserved; auto.
+    - simpl; rewrite <- parent_ra_preserved; auto.
+  * eapply ex_intro.
+    intuition auto.
+    eapply exec_MBbuiltin ;eauto.
+  * exploit find_label_transcode_preserved; eauto.
+    intros (x & X1 & X2).
     eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto.
-  * exploit find_label_transcode_preserved; eauto. intros (h & X1 & X2).
+  * exploit find_label_transcode_preserved; eauto.
+    intros (x & X1 & X2).
     eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto.
   * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto.
     eapply exec_MBcond_false; eauto.
@@ -481,42 +560,39 @@ Proof.
     eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto.
   * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto.
     eapply exec_MBreturn; eauto.
-    rewrite parent_sp_preserved in H8; subst; auto.
-    rewrite parent_ra_preserved in H9; subst; auto.
+    rewrite parent_sp_preserved in H0; subst; auto.
+    rewrite parent_ra_preserved in H1; subst; auto. 
 Qed.
 
-
-
-Lemma step_simu_exit_step c e c' stk f sp rs m t s' b:
-  to_bblock_exit c = (e, c') ->
-  starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length_opt e) (Mach.State stk f sp c rs m) t s' ->
-  exists s2, exit_step rao tge e (State (trans_stack stk) f sp (b::trans_code c') rs m) t s2 /\ match_states s' s2.
+Lemma step_simu_exit_step stk f sp rs m t s1 e c c' b blc:
+  is_exit e c c' -> is_trans_code c' blc ->
+  starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length_opt e) (Mach.State stk f sp c rs m) t s1 ->
+  exists s2, exit_step rao tge e (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s1 s2.
 Proof.
-  intros H1 H2; destruct e as [ e |]; inversion_clear H2. 
-  + (* Some *) inversion H0; clear H0; subst. autorewrite with trace_rewrite.
-    exploit step_simu_cfi_step; eauto.
-    intros (s2' & H2 & H3); eapply ex_intro; intuition eauto.
-  + (* None *) 
-     destruct c as [ |i c]; simpl in H1; inversion H1.
-     - eapply ex_intro; intuition eauto; try eapply match_states_trans_state.
-     - remember to_cfi as o. destruct o; try discriminate.
-       inversion_clear H1.
-       eapply ex_intro; intuition eauto; try eapply match_states_trans_state.
+  destruct 1.
+  - (* None *)
+    intros H0 H1. inversion H1. exists (State (trans_stack stk) f sp blc rs m).
+    split; eauto.
+    apply is_trans_code_inv in H0. 
+    rewrite H0.
+    apply match_states_trans_state.
+  - (* None *)
+    intros H0 H1. inversion H1. exists (State (trans_stack stk) f sp blc rs m).
+    split; eauto.
+    apply is_trans_code_inv in H0. 
+    rewrite H0.
+    apply match_states_trans_state.
+  - (* Some *)
+    intros H0 H1.
+    inversion H1; subst. 
+    exploit (step_simu_cfi_step); eauto.
+    intros [s2 [Hcfi1 Hcfi3]].
+    inversion H4. subst; simpl.
+    autorewrite  with trace_rewrite.
+    exists s2.
+    split;eauto.
 Qed.
 
-Lemma step_simu_header st f sp rs m s c: forall h c' t, 
- (h, c') = to_bblock_header c ->
- starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> s = Mach.State st f sp c' rs m /\ t = E0.
-Proof.
-   induction c as [ | i c]; simpl; intros h c' t H.
-   - inversion_clear H. simpl; intros H; inversion H; auto.
-   - destruct i; try (injection H; clear H; intros H H2; subst; simpl; intros H; inversion H; subst; auto).
-     remember (to_bblock_header c) as bhc. destruct bhc as [h0 c0].
-     injection H; clear H; intros H H2; subst; simpl; intros H; inversion H; subst.
-     inversion H1; clear H1; subst; auto. autorewrite with trace_rewrite.
-     exploit IHc; eauto.
-Qed. 
-
 Lemma simu_end_block:
   forall s1 t s1',
   starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' ->
@@ -524,56 +600,41 @@ Lemma simu_end_block:
 Proof.
   destruct s1; simpl.
   + (* State *)
-    (* c cannot be nil *)
-    destruct c as [|i c]; simpl; try ( (* nil => absurd *)
-      unfold dist_end_block_code; simpl;
-      intros t s1' H; inversion_clear H;
-      inversion_clear H0; fail
-    ).
-
-    intros t s1' H.
-    remember (_::_) as c0. remember (trans_code c0) as tc0.
-
-    (* tc0 cannot be nil *)
-    destruct tc0; try
-    ( exploit (trans_code_nonil c0); subst; auto; try discriminate; intro H0; contradict H0 ).
-
-    assert (X: Datatypes.S (dist_end_block_code c0) = (size (fst (to_bblock c0)))).
+    remember (trans_code _) as tc.
+    rewrite <- is_trans_code_inv in Heqtc.
+    intros t s1 H.
+    destruct tc as [|b bl].
+    { (* nil => absurd *) 
+      inversion Heqtc. subst. 
+      unfold dist_end_block_code; simpl.
+      inversion_clear H;
+      inversion_clear H0. 
+    }
+    assert (X: Datatypes.S (dist_end_block_code c) = (size b)).
     {
-      unfold dist_end_block_code. remember (size _) as siz.
-      assert (siz <> 0%nat). rewrite Heqsiz; subst; apply to_bblock_nonil with (c0 := c) (i := i); auto.
+      unfold dist_end_block_code. 
+      subst_is_trans_code Heqtc.
+      lapply (size_nonzero c b bl); auto.
       omega.
     }
-
-    (* decomposition of starN in 3 parts: header + body + exit *)
     rewrite X in H; unfold size in H.
-    destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H _ _ refl_equal) as [t3 [t4 [s1 [H0 [H3 H4]]]]].
+    (* decomposition of starN in 3 parts: header + body + exit *)
+    destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H _ _ refl_equal) as (t3&t4&s1'&H0&H3&H4).
     subst t; clear X H.
-    destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H0 _ _ refl_equal) as [t1 [t2 [s0 [H [H1 H2]]]]].
+    destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H0 _ _ refl_equal) as (t1&t2&s1''&H&H1&H2).
     subst t3; clear H0.
-
-    unfold to_bblock in * |- *.
-    (* naming parts of block "b" *)
-    remember (to_bblock_header c0) as hd. destruct hd as [hb c1].
-    remember (to_bblock_body c1) as bb. destruct bb as [bb c2].
-    remember (to_bblock_exit c2) as exb. destruct exb as [exb c3].
-    simpl in * |- *.
-
-    exploit trans_code_step; eauto. intro EQ. destruct EQ as (EQH & EQB & EQE & EQTB0).
-    subst hb bb exb.
-
-    (* header opt step *)
+    exploit trans_code_decompose; eauto. clear Heqtc.
+    intros (c0&c1&c2&Hc0&Hc1&Hc2&Heqtc).
+    (* header steps *)
     exploit step_simu_header; eauto.
-    intros [X1 X2]; subst s0 t1.
-    autorewrite with trace_rewrite.
+    clear H; intros [X1 X2]; subst.
     (* body steps *)
     exploit (star_step_simu_body_step); eauto.
-    clear H1; intros [rs' [m' [H0 [H1 H2]]]].
-    subst s1 t2. autorewrite with trace_rewrite.
+    clear H1; intros (rs'&m'&H0&H1&H2). subst.
+    autorewrite with trace_rewrite.
     (* exit step *)
-    subst tc0.
-    exploit step_simu_exit_step; eauto. clear H3.
-    intros (s2' & H3 & H4).
+    exploit step_simu_exit_step; eauto.
+    clear H3; intros (s2' & H3 & H4).
     eapply ex_intro; intuition eauto.
     eapply exec_bblock; eauto.
   + (* Callstate *)
@@ -599,13 +660,27 @@ Proof.
     eapply exec_return.
 Qed.
 
+
+Lemma cfi_dist_end_block i c:
+(exists cfi, trans_inst i = MB_cfi cfi) ->
+dist_end_block_code (i :: c) = 0.
+Proof.
+  unfold dist_end_block_code.
+  intro H. destruct H as [cfi H].
+  destruct i;simpl in H;try(congruence); ( 
+    remember (trans_code _) as bl; 
+    rewrite <- is_trans_code_inv in Heqbl;
+    inversion Heqbl; subst; simpl in * |- *; try (congruence)).
+Qed.
+
 Theorem transf_program_correct: 
     forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog).
 Proof.
   apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state).
 (* simu_mid_block *)
-  - intros s1 t s1' H1.
-    destruct H1; simpl; omega || (intuition auto).
+  - intros s1 t s1' H1 H2.
+    destruct H1; simpl in * |- *; omega || (intuition auto);
+    destruct H2; eapply cfi_dist_end_block; simpl; eauto.
 (* public_preserved *)
   - apply senv_preserved.
 (* match_initial_states *)
@@ -618,12 +693,114 @@ Proof.
 (* match_final_states *)
   - intros. simpl. destruct H. split with (r := r); auto.
 (* final_states_end_block *)
-  - intros. simpl in H0. inversion H0.
+  - intros. simpl in H0.
+    inversion H0.
     inversion H; simpl; auto.
-    (* the remaining instructions cannot lead to a Returnstate *)
-    all: subst; discriminate.
+    all: try (subst; discriminate).
+    apply cfi_dist_end_block; exists MBreturn; eauto.
 (* simu_end_block *)
   - apply simu_end_block.
 Qed.
 
 End PRESERVATION.
+
+(** Auxiliary lemmas used to prove existence of a Mach return adress from a Machblock return address. *)
+
+
+
+Lemma is_trans_code_monotonic i c b l:
+   is_trans_code c (b::l) ->
+   exists l' b', is_trans_code (i::c) (l' ++ (b'::l)).
+Proof.
+  intro H; destruct c as [|i' c]. { inversion H. }
+  remember (trans_inst i) as ti.
+  destruct ti as [lbl|bi|cfi].
+  - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2:{ destruct i; simpl in * |- *; try congruence. }
+    exists nil; simpl; eexists. eapply Tr_add_label; eauto.
+  - (*i=basic*)
+    destruct i'.
+    10: {exists (add_to_new_bblock (MB_basic bi)::nil).  exists b. 
+      cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto.
+      rewrite Heqti.        
+      eapply  Tr_end_block; eauto.
+      rewrite <-Heqti.
+      eapply End_basic. inversion H; try(simpl; congruence).
+      simpl in H5; congruence. }
+    all: try(exists nil; simpl; eexists;  eapply  Tr_add_basic; eauto; inversion H; try(eauto || congruence)).
+  - (*i=cfi*)
+    destruct i; try(simpl in Heqti; congruence).
+    all: exists (add_to_new_bblock (MB_cfi cfi)::nil);  exists b; 
+        cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto;
+        rewrite Heqti;        
+        eapply  Tr_end_block; eauto;
+        rewrite <-Heqti;
+        eapply End_cfi; congruence.
+Qed.
+
+Lemma trans_code_monotonic i c b l:
+   (b::l) = trans_code c ->
+   exists l' b', trans_code (i::c) = (l' ++ (b'::l)).
+Proof.
+    intro H; rewrite <- is_trans_code_inv in H.
+    destruct (is_trans_code_monotonic i c b l H) as (l' & b' & H0).
+    subst_is_trans_code H0.
+    eauto.
+Qed.
+
+(* FIXME: these two lemma should go into [Coqlib.v] *) 
+Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
+Proof.
+  induction l1; simpl; auto with coqlib.
+Qed.
+Hint Resolve is_tail_app: coqlib.
+
+Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
+Proof.
+  induction l1; simpl; auto with coqlib.
+  intros l2 l3 H; inversion H; eauto with coqlib.
+Qed.
+Hint Resolve is_tail_app_inv: coqlib.
+
+
+Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> 
+  exists b, is_tail (b :: trans_code c) (trans_code c2).
+Proof.
+  intros H; induction 1.
+  - intros; subst.
+    remember (trans_code (Mcall _ _::c)) as tc2.
+    rewrite <- is_trans_code_inv in Heqtc2.
+    inversion Heqtc2; simpl in * |- *; subst; try congruence.
+    subst_is_trans_code H1.
+    eapply ex_intro; eauto with coqlib.
+  - intros; exploit IHis_tail; eauto. clear IHis_tail.
+    intros (b & Hb). inversion Hb; clear Hb.
+    * exploit (trans_code_monotonic i c2); eauto.
+      intros (l' & b' & Hl'); rewrite Hl'.
+      exists b'; simpl; eauto with coqlib.
+    * exploit (trans_code_monotonic i c2); eauto.
+      intros (l' & b' & Hl'); rewrite Hl'.
+      simpl; eapply ex_intro.
+      eapply is_tail_trans; eauto with coqlib.
+Qed.
+
+Section Mach_Return_Address.
+
+Variable return_address_offset: function -> code -> ptrofs -> Prop.
+
+Hypothesis ra_exists: forall (b: bblock) (f: function) (c : list bblock),
+       is_tail (b :: c) (fn_code f) -> exists ra : ptrofs, return_address_offset f c ra.
+
+Definition Mach_return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop :=
+ return_address_offset (transf_function f) (trans_code c) ofs.
+
+Lemma Mach_return_address_exists:
+  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
+  exists ra, Mach_return_address_offset f c ra.
+Proof.
+  intros.
+  exploit Mach_Machblock_tail; eauto.
+  destruct 1.
+  eapply ra_exists; eauto.
+Qed.
+
+End Mach_Return_Address.
\ No newline at end of file
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index e0780b9d..89d41017 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -15,6 +15,7 @@ Require Import Asmblock.
 Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
+Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
 
 Module MB:=Machblock.
 Module AB:=Asmvliw.
@@ -577,21 +578,6 @@ Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : P
   transl_blocks f c false = OK tc ->
   code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc.
 
-(* NB: these two lemma should go into [Coqlib.v] *) 
-Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
-Proof.
-  induction l1; simpl; auto with coqlib.
-Qed.
-Hint Resolve is_tail_app: coqlib.
-
-Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
-Proof.
-  induction l1; simpl; auto with coqlib.
-  intros l2 l3 H; inversion H; eauto with coqlib.
-Qed.
-Hint Resolve is_tail_app_inv: coqlib.
-
-
 Lemma transl_blocks_tail:
   forall f c1 c2, is_tail c1 c2 ->
   forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 ->
diff --git a/mppa_k1c/lib/ForwardSimulationBlock.v b/mppa_k1c/lib/ForwardSimulationBlock.v
index dc8beb29..39dd2234 100644
--- a/mppa_k1c/lib/ForwardSimulationBlock.v
+++ b/mppa_k1c/lib/ForwardSimulationBlock.v
@@ -271,6 +271,7 @@ However, the Machblock state after a goto remains "equivalent" to the trans_stat
 
 *)
 
+
 Section ForwardSimuBlock_TRANS.
 
 Variable L1 L2: semantics.
@@ -320,3 +321,53 @@ Proof.
 Qed.
 
 End ForwardSimuBlock_TRANS.
+
+
+(* another version with a relation [trans_state_R] instead of a function [trans_state] *)
+Section ForwardSimuBlock_TRANS_R.
+
+Variable L1 L2: semantics.
+
+Variable trans_state_R: state L1 -> state L2 -> Prop.
+
+Definition match_states_R s1 s2: Prop :=
+  exists s2', trans_state_R s1 s2' /\ equiv_on_next_step _ (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 s2'.
+
+Lemma match_states_trans_state_R s1 s2: trans_state_R s1 s2 -> match_states_R s1 s2.
+Proof.
+  unfold match_states, equiv_on_next_step. firstorder.
+Qed.
+
+Variable dist_end_block: state L1 -> nat.
+
+Hypothesis simu_mid_block:
+  forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1').
+
+Hypothesis public_preserved:
+  forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
+
+Hypothesis match_initial_states:
+  forall s1, initial_state L1 s1 -> exists s2, match_states_R s1 s2 /\ initial_state L2 s2.
+
+Hypothesis match_final_states:
+  forall s1 s2 r, final_state L1 s1 r -> trans_state_R s1 s2 -> final_state L2 s2 r.
+
+Hypothesis final_states_end_block:
+  forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0.
+
+Hypothesis simu_end_block:
+  forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> trans_state_R s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states_R s1' s2'.
+
+Lemma forward_simulation_block_trans_R: forward_simulation L1 L2.
+Proof.
+  eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states_R); try tauto.
+  + (* final_states *) intros s1 s2 r H1 (s2' & H2 & H3 & H4). rewrite H4; eauto.
+  + (* simu_end_block *)
+    intros s1 t s1' s2 H1 (s2' & H2 & H2a & H2b). exploit simu_end_block; eauto.
+    intros (x & Hx & (y & H3 & H4 & H5)). repeat (econstructor; eauto).
+    rewrite H2a; eauto.
+    inversion_clear H1. eauto.
+Qed.
+
+End ForwardSimuBlock_TRANS_R.
+
diff --git a/test/monniaux/gengraphs.py b/test/monniaux/gengraphs.py
index 2455c285..fd8098b7 100755
--- a/test/monniaux/gengraphs.py
+++ b/test/monniaux/gengraphs.py
@@ -1,9 +1,10 @@
 #!/usr/bin/python3.6
 
-import numpy as np
-import matplotlib.pyplot as plt
-import pandas as pd
+import numpy as np              # type: ignore
+import matplotlib.pyplot as plt # type: ignore
+import pandas as pd             # type: ignore
 import sys
+from typing import *
 
 ##
 # Reading data
@@ -28,7 +29,7 @@ colors = ["forestgreen", "darkorange", "cornflowerblue", "darkorchid", "darksalm
 # Generating PDF
 ##
 
-def extract_envs(keys):
+def extract_envs(keys: List[str]) -> List[str]:
   envs = []
   for key in keys:
     words = key.split()[:-1]
@@ -36,11 +37,11 @@ def extract_envs(keys):
   return envs
 
 
-def subdivide_interv(inf, sup, n):
+def subdivide_interv(inf: float, sup: float, n: int) -> List[float]:
   return [inf + k*(sup-inf)/n for k in range(n)]
 
 
-def generate_file(f, cols):
+def generate_file(f: str, cols: List[str]) -> None:
   ind = np.arange(len(df[cols[0]]))
 
   width = 0.35  # the width of the bars
@@ -63,7 +64,7 @@ def generate_file(f, cols):
   ax.set_xticklabels(benches)
   ax.legend()
 
-  def autolabel(rects, xpos='center'):
+  def autolabel(rects: List[Any], xpos='center') -> None:
       """
       Attach a text label above each bar in *rects*, displaying its height.
 
diff --git a/test/monniaux/genmake.py b/test/monniaux/genmake.py
index ad460b14..d04ba70c 100755
--- a/test/monniaux/genmake.py
+++ b/test/monniaux/genmake.py
@@ -8,6 +8,7 @@ See the source for more info.
 """
 
 from collections import namedtuple
+from typing import *
 import sys
 import yaml
 
@@ -36,7 +37,7 @@ if len(sys.argv) != 2:
 yaml_file = sys.argv[1]
 
 with open(yaml_file, "r") as f:
-  settings = yaml.load(f.read(), Loader=yaml.FullLoader)
+  settings = yaml.load(f.read(), Loader=yaml.SafeLoader)
 
 basename = settings["target"]
 objdeps = settings["objdeps"] if "objdeps" in settings else []
@@ -56,22 +57,22 @@ for objdep in objdeps:
 # Printing the rules
 ##
 
-def make_product(env, optim):
+def make_product(env: Env, optim: Optim) -> str:
   return basename + "." + env.compiler.short + (("." + optim.short) if optim.short != "" else "") + "." + env.target
 
-def make_obj(name, env, compiler_short):
+def make_obj(name: str, env: Env, compiler_short: str) -> str:
   return name + "." + compiler_short + "." + env.target + ".o"
 
-def make_clock(env, optim):
+def make_clock(env: Env, optim: Optim) -> str:
   return "clock.gcc." + env.target
 
-def make_sources(env, optim):
+def make_sources(env: Env, optim: Optim) -> str:
   if sources:
     return "$(src:.c=." + env.compiler.short + (("." + optim.short) if optim.short != "" else "") + "." + env.target + ".o)"
   else:
     return "{product}.o".format(product = make_product(env, optim))
 
-def print_rule(env, optim):
+def print_rule(env: Env, optim: Optim) -> None:
   print("{product}: {sources} ../{clock}.o "
         .format(product = make_product(env, optim),
           sources = make_sources(env, optim), clock = make_clock(env, optim))
@@ -79,12 +80,12 @@ def print_rule(env, optim):
   print("	{compiler} {flags} $+ -o $@"
         .format(compiler = env.compiler.full, flags = optim.full))
 
-def make_env_list(envs):
+def make_env_list(envs: List[Env]) -> str:
   return ",".join([(env.compiler.short + ((" " + optim.short) if optim.short != "" else "") + " " + env.target)
                     for env in environments
                     for optim in env.optimizations])
 
-def print_measure_rule(environments, measures):
+def print_measure_rule(environments: List[Env], measures: List[Union[List[str], str]]) -> None:
   print("measures.csv: $(PRODUCTS_OUT)")
   print('	echo "benches, {}" > $@'.format(make_env_list(environments)))
   for measure in measures: