directory postpass_lib

4 files changed, 1819 insertions, 0 deletions

diff --git a/scheduling/postpass_lib/ForwardSimulationBlock.v b/scheduling/postpass_lib/ForwardSimulationBlock.v
new file mode 100644
index 00000000..cc6ecdd8
--- /dev/null
+++ b/scheduling/postpass_lib/ForwardSimulationBlock.v
@@ -0,0 +1,387 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(***
+
+Auxiliary lemmas on starN and forward_simulation 
+in order to prove the forward simulation of Mach -> Machblock. 
+
+***)
+
+Require Import Relations.
+Require Import Wellfounded.
+Require Import Coqlib.
+Require Import Events.
+Require Import Globalenvs.
+Require Import Smallstep.
+Require Import Lia.
+
+Local Open Scope nat_scope.
+
+
+(** Auxiliary lemma on starN *)
+Section starN_lemma.
+
+Variable L: semantics.
+
+Local Hint Resolve starN_refl starN_step Eapp_assoc: core.
+
+Lemma starN_split n s t s':
+  starN (step L) (globalenv L) n s t s' ->
+  forall m k, n=m+k ->
+  exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2.
+Proof.
+  induction 1; cbn.
+  + intros m k H; assert (X: m=0); try lia.
+    assert (X0: k=0); try lia.
+    subst; repeat (eapply ex_intro); intuition eauto.
+  + intros m; destruct m as [| m']; cbn.
+    - intros k H2; subst; repeat (eapply ex_intro); intuition eauto.
+    - intros k H2. inversion H2.
+      exploit (IHstarN m' k); eauto. intro.
+      destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7).
+      repeat (eapply ex_intro).
+      instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0).
+      intuition eauto. subst. auto.
+Qed.
+
+Lemma starN_tailstep n s t1 s': 
+  starN (step L) (globalenv L) n s t1 s' ->
+  forall (t t2:trace) s'',
+     Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''.
+Proof.
+  induction 1; cbn. 
+  + intros t t1 s0; autorewrite with trace_rewrite.
+    intros; subst; eapply starN_step; eauto.
+    autorewrite with trace_rewrite; auto.
+  + intros. eapply  starN_step; eauto.
+    intros; subst; autorewrite with trace_rewrite; auto.
+Qed.
+
+End starN_lemma.
+
+
+
+(** General scheme from a "match_states" relation *)
+
+Section ForwardSimuBlock_REL.
+
+Variable L1 L2: semantics.
+
+
+(** Hypothèses de la preuve *)
+
+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.
+
+Variable match_states: state L1 -> state L2 -> Prop.
+
+Hypothesis match_initial_states:
+  forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2.
+
+Hypothesis match_final_states:
+  forall s1 s2 r, final_state L1 s1 r -> match_states 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' -> match_states s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states s1' s2'.
+
+
+(** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *)
+
+Local Hint Resolve starN_refl starN_step: core.
+
+Definition follows_in_block (head current: state L1): Prop :=
+  dist_end_block head >= dist_end_block current 
+  /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. 
+
+Lemma follows_in_block_step (head previous next: state L1):
+  forall t, follows_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> follows_in_block head next.
+Proof.
+  intros t [H1 H2] H3 H4.
+  destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. 
+  constructor 1.
+  + lia.
+  + replace (dist_end_block head - dist_end_block next) with (S (dist_end_block head - dist_end_block previous)).
+    - eapply starN_tailstep; eauto.
+    - lia.
+Qed.
+
+Lemma follows_in_block_init (head current: state L1):
+  forall t, Step L1 head t current -> (dist_end_block head)<>0 -> follows_in_block head current.
+Proof.
+  intros t H3 H4.
+  destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. 
+  constructor 1.
+  + lia.
+  + replace (dist_end_block head - dist_end_block current) with 1.
+    - eapply starN_tailstep; eauto.
+    - lia.
+Qed.
+
+
+Record memostate := {
+    real: state L1; 
+    memorized: option (state L1);
+    memo_star: forall head, memorized = Some head -> follows_in_block head real;
+    memo_final: forall r, final_state L1 real r -> memorized = None
+}.
+
+Definition head (s: memostate): state L1 :=
+    match memorized s with
+    | None => real s
+    | Some s' => s'
+    end.
+
+Lemma head_followed (s: memostate): follows_in_block (head s) (real s).
+Proof.
+  destruct s as [rs ms Hs]. cbn.
+  destruct ms as [ms|]; unfold head; cbn; auto.
+  constructor 1.
+  lia.
+  replace (dist_end_block rs - dist_end_block rs)%nat with O.
+  + apply starN_refl; auto.
+  + lia.
+Qed.
+
+Inductive is_well_memorized (s s': memostate): Prop :=
+  | StartBloc:
+    dist_end_block (real s) <> O  ->
+    memorized s = None ->
+    memorized s' = Some (real s) ->
+    is_well_memorized s s'
+  | MidBloc:
+    dist_end_block (real s) <> O ->
+    memorized s <> None ->
+    memorized s' = memorized s ->
+    is_well_memorized s s'
+  | ExitBloc:
+    dist_end_block (real s) = O ->
+    memorized s' = None ->
+    is_well_memorized s s'.
+
+Local Hint Resolve StartBloc MidBloc ExitBloc: core.
+
+Definition memoL1 := {| 
+  state := memostate;
+  genvtype := genvtype L1;
+  step := fun ge s t s' => 
+    step L1 ge (real s) t (real s') 
+    /\ is_well_memorized s s' ;
+  initial_state := fun s => initial_state L1 (real s) /\ memorized s = None;
+  final_state := fun s r => final_state L1 (real s) r;
+  globalenv:= globalenv L1;
+  symbolenv:= symbolenv L1
+|}.
+
+
+(** Preuve des 2 forward simulations: L1 -> memoL1  et  memoL1 -> L2 *)
+
+Lemma discr_dist_end s:
+  {dist_end_block s = O} + {dist_end_block s <> O}.
+Proof.
+  destruct (dist_end_block s); cbn; intuition.
+Qed.
+
+Lemma memo_simulation_step:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2').
+Proof.
+  intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. cbn in H2; subst.
+  destruct (discr_dist_end rs2) as [H3 | H3].
+  + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); cbn.
+    intuition.
+  + destruct ms2 as [s|].
+    - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); cbn.
+      intuition.
+    - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); cbn.
+      intuition.
+  Unshelve.
+  * intros; discriminate.
+  * intros; auto.
+  * intros head X; injection X; clear X; intros; subst.
+    eapply follows_in_block_step; eauto.
+  * intros r X; erewrite final_states_end_block in H3; intuition eauto.
+  * intros head X; injection X; clear X; intros; subst.
+    eapply follows_in_block_init; eauto.
+  * intros r X; erewrite final_states_end_block in H3; intuition eauto.
+Qed.
+
+Lemma forward_memo_simulation_1: forward_simulation L1 memoL1.
+Proof.
+  apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto.
+  + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); cbn.
+    intuition.
+  + intros; subst; auto.
+  + intros; exploit memo_simulation_step; eauto.
+  Unshelve.
+  * intros; discriminate.
+  * auto.
+Qed.
+
+Lemma forward_memo_simulation_2: forward_simulation memoL1 L2.
+Proof.
+  unfold memoL1; cbn.
+  apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); cbn; auto.
+  + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0).
+    unfold head; rewrite H1.
+    intuition eauto.
+  + intros s1 s2 r X H0;  unfold head in X. 
+    erewrite memo_final in X; eauto.
+  + intros s1 t s1' [H1 H2] s2 H; subst.
+    destruct H2 as [ H0 H2 H3 | H0 H2 H3 | H0 H2].
+    - (* StartBloc *)
+      constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto.
+      unfold head in * |- *. rewrite H2 in H. rewrite H3. rewrite H4. intuition.
+    - (* MidBloc *)
+      constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto.
+      unfold head in * |- *. rewrite H3. rewrite H4. intuition.
+      destruct (memorized s1); cbn; auto. tauto.
+    - (* EndBloc *)
+      constructor 1.
+      destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto.
+      * destruct (head_followed s1) as [H4 H3].
+        replace (dist_end_block (head s1) - dist_end_block (real s1)) with (dist_end_block (head s1)) in H3; try lia.
+        eapply starN_tailstep; eauto.
+      * unfold head; rewrite H2; cbn. intuition eauto. 
+Qed.
+
+Lemma forward_simulation_block_rel: forward_simulation L1 L2.
+Proof.
+  eapply compose_forward_simulations.
+  eapply forward_memo_simulation_1.
+  apply forward_memo_simulation_2.
+Qed.
+
+
+End ForwardSimuBlock_REL.
+
+
+
+(* An instance of the previous scheme, when there is a translation from L1 states to L2 states 
+
+Here, we do not require that the sequence of S2 states does exactly match the sequence of L1 states by trans_state.
+This is because the exact matching is broken in Machblock on "goto" instruction (due to the find_label).
+
+However, the Machblock state after a goto remains "equivalent" to the trans_state of the Mach state in the sense of "equiv_on_next_step" below...
+
+*)
+
+
+Section ForwardSimuBlock_TRANS.
+
+Variable L1 L2: semantics.
+
+Variable trans_state: state L1 -> state L2.
+
+Definition equiv_on_next_step (P Q: Prop) s2_a s2_b: Prop := 
+  (P -> (forall t s', Step L2 s2_a t s' <-> Step L2 s2_b t s')) /\ (Q -> (forall r, (final_state L2 s2_a r) <-> (final_state L2 s2_b r))).
+
+Definition match_states s1 s2: Prop :=
+  equiv_on_next_step (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 (trans_state s1).
+
+Lemma match_states_trans_state s1: match_states s1 (trans_state s1).
+Proof.
+  unfold match_states, equiv_on_next_step. intuition.
+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 s1 s2 /\ initial_state L2 s2.
+
+Hypothesis match_final_states:
+  forall s1 r, final_state L1 s1 r -> final_state L2 (trans_state s1) 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', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> exists s2', Step L2 (trans_state s1) t s2' /\ match_states s1' s2'.
+
+Lemma forward_simulation_block_trans: forward_simulation L1 L2.
+Proof.
+  eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states); try tauto.
+  + (* final_states *) intros s1 s2 r H1 [H2 H3]. rewrite H3; eauto.
+  + (* simu_end_block *)
+    intros s1 t s1' s2 H1 [H2a H2b]. exploit simu_end_block; eauto.
+    intros (s2' & H3 & H4); econstructor 1; intuition eauto.
+    rewrite H2a; auto.
+    inversion_clear H1. eauto.
+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/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v
new file mode 100644
index 00000000..404c2a96
--- /dev/null
+++ b/scheduling/postpass_lib/Machblock.v
@@ -0,0 +1,387 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** Abstract syntax and semantics of a Mach variant, structured with basic-blocks. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Op.
+Require Import Locations.
+Require Import Conventions.
+Require Stacklayout.
+Require Import Mach.
+Require Import Linking.
+
+(** * Abstract Syntax *)
+
+(** ** basic instructions (ie no control-flow) *)
+Inductive basic_inst: Type :=
+  | MBgetstack: ptrofs -> typ -> mreg -> basic_inst
+  | MBsetstack: mreg -> ptrofs -> typ -> basic_inst
+  | MBgetparam: ptrofs -> typ -> mreg -> basic_inst
+  | MBop: operation -> list mreg -> mreg -> basic_inst
+  | MBload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> basic_inst
+  | MBstore: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst
+  .
+
+Definition bblock_body := list basic_inst.
+
+(** ** control flow instructions *)
+Inductive control_flow_inst: Type :=
+  | MBcall: signature -> mreg + ident -> control_flow_inst
+  | MBtailcall: signature -> mreg + ident -> control_flow_inst
+  | MBbuiltin: external_function -> list (builtin_arg mreg) -> builtin_res mreg -> control_flow_inst
+  | MBgoto: label -> control_flow_inst
+  | MBcond: condition -> list mreg -> label -> control_flow_inst
+  | MBjumptable: mreg -> list label -> control_flow_inst
+  | MBreturn: control_flow_inst
+  .
+
+(** ** basic block *)
+Record bblock := mk_bblock {
+  header: list label;
+  body:   bblock_body;
+  exit:   option control_flow_inst
+}.
+
+Lemma bblock_eq:
+  forall b1 b2,
+  header b1 = header b2 ->
+  body b1 = body b2 ->
+  exit b1 = exit b2 ->
+  b1 = b2.
+Proof.
+  intros. destruct b1. destruct b2.
+  cbn in *. subst. auto.
+Qed.
+
+Definition length_opt {A} (o: option A) : nat :=
+  match o with
+  | Some o => 1
+  | None => 0
+  end.
+
+Definition size (b:bblock): nat := (length (header b))+(length (body b))+(length_opt (exit b)).
+
+Lemma size_null b:
+  size b = 0%nat ->
+  header b = nil /\ body b = nil /\ exit b = None.
+Proof.
+  destruct b as [h b e]. cbn. unfold size. cbn.
+  intros H.
+  assert (length h = 0%nat) as Hh; [ omega |].
+  assert (length b = 0%nat) as Hb; [ omega |].
+  assert (length_opt e = 0%nat) as He; [ omega|].
+  repeat split.
+  destruct h; try (cbn in Hh; discriminate); auto.
+  destruct b; try (cbn in Hb; discriminate); auto.
+  destruct e; try (cbn in He; discriminate); auto.
+Qed.
+
+(** ** programs *)
+
+Definition code := list bblock.
+
+Record function: Type := mkfunction
+  { fn_sig: signature;
+    fn_code: code;
+    fn_stacksize: Z;
+    fn_link_ofs: ptrofs;
+    fn_retaddr_ofs: ptrofs }.
+
+Definition fundef := AST.fundef function.
+
+Definition program := AST.program fundef unit.
+
+Definition genv := Genv.t fundef unit.
+
+(** * Operational (blockstep) semantics ***)
+
+Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
+Proof.
+  apply List.in_dec.
+  apply Pos.eq_dec.
+Qed.
+
+Definition is_label (lbl: label) (bb: bblock) : bool :=
+  if in_dec lbl (header bb) then true else false.
+
+Lemma is_label_correct_true lbl bb:
+  List.In lbl (header bb) <-> is_label lbl bb = true. 
+Proof.
+  unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition.
+Qed.
+
+Lemma is_label_correct_false lbl bb:
+  ~(List.In lbl (header bb)) <-> is_label lbl bb = false. 
+Proof.
+  unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition.
+Qed.
+
+
+Local Open Scope nat_scope.
+
+Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
+  match c with
+  | nil => None
+  | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl
+  end.
+
+Section RELSEM.
+
+Variable rao:function -> code -> ptrofs -> Prop.
+Variable ge:genv.
+
+Definition find_function_ptr
+        (ge: genv) (ros: mreg + ident) (rs: regset) : option block :=
+  match ros with
+  | inl r =>
+      match rs r with
+      | Vptr b ofs => if Ptrofs.eq ofs Ptrofs.zero then Some b else None
+      | _ => None
+      end
+  | inr symb =>
+      Genv.find_symbol ge symb
+  end.
+
+(** ** Machblock execution states. *)
+
+Inductive stackframe: Type :=
+  | Stackframe:
+      forall (f: block)       (**r pointer to calling function *)
+             (sp: val)        (**r stack pointer in calling function *)
+             (retaddr: val)   (**r Asm return address in calling function *)
+             (c: code),       (**r program point in calling function *)
+      stackframe.
+
+Inductive state: Type :=
+  | State:
+      forall (stack: list stackframe)  (**r call stack *)
+             (f: block)                (**r pointer to current function *)
+             (sp: val)                 (**r stack pointer *)
+             (c: code)                 (**r current program point *)
+             (rs: regset)              (**r register state *)
+             (m: mem),                 (**r memory state *)
+      state
+  | Callstate:
+      forall (stack: list stackframe)  (**r call stack *)
+             (f: block)                (**r pointer to function to call *)
+             (rs: regset)              (**r register state *)
+             (m: mem),                 (**r memory state *)
+      state
+  | Returnstate:
+      forall (stack: list stackframe)  (**r call stack *)
+             (rs: regset)              (**r register state *)
+             (m: mem),                 (**r memory state *)
+      state.
+
+Definition parent_sp (s: list stackframe) : val :=
+  match s with
+  | nil => Vnullptr
+  | Stackframe f sp ra c :: s' => sp
+  end.
+
+Definition parent_ra (s: list stackframe) : val :=
+  match s with
+  | nil => Vnullptr
+  | Stackframe f sp ra c :: s' => ra
+  end.
+
+Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop :=
+  | exec_MBgetstack:
+      forall ofs ty dst v,
+      load_stack m sp ty ofs = Some v ->
+      basic_step s fb sp rs m (MBgetstack ofs ty dst) (rs#dst <- v) m
+  | exec_MBsetstack:
+      forall src ofs ty m' rs',
+      store_stack m sp ty ofs (rs src) = Some m' ->
+      rs' = undef_regs (destroyed_by_setstack ty) rs ->
+      basic_step s fb sp rs m (MBsetstack src ofs ty) rs' m'
+  | exec_MBgetparam:
+      forall ofs ty dst v rs' f,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      load_stack m sp Tptr f.(fn_link_ofs) = Some (parent_sp s) ->
+      load_stack m (parent_sp s) ty ofs = Some v ->
+      rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) ->
+      basic_step s fb sp rs m (MBgetparam ofs ty dst) rs' m
+  | exec_MBop:
+      forall op args v rs' res,
+      eval_operation ge sp op rs##args m = Some v ->
+      rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) ->
+      basic_step s fb sp rs m (MBop op args res) rs' m
+  | exec_MBload:
+      forall addr args a v rs' trap chunk dst,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) ->
+      basic_step s fb sp rs m (MBload trap chunk addr args dst) rs' m
+  | exec_MBload_notrap1:
+      forall addr args rs' chunk dst,
+      eval_addressing ge sp addr rs##args = None ->
+      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+      basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m
+  | exec_MBload_notrap2:
+      forall addr args a rs' chunk dst,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.loadv chunk m a = None ->
+      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+      basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m
+  | exec_MBstore:
+      forall chunk addr args src m' a rs',
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.storev chunk m a (rs src) = Some m' ->
+      rs' = undef_regs (destroyed_by_store chunk addr) rs ->
+      basic_step s fb sp rs m (MBstore chunk addr args src) rs' m'
+  .
+
+
+Inductive body_step (s: list stackframe) (f: block) (sp: val): bblock_body -> regset -> mem -> regset -> mem -> Prop :=
+   | exec_nil_body:
+       forall rs m,
+       body_step s f sp nil rs m rs m
+   | exec_cons_body:
+       forall rs m bi p rs' m' rs'' m'',
+       basic_step s f sp rs m bi rs' m' ->
+       body_step s f sp p rs' m' rs'' m'' ->
+       body_step s f sp (bi::p) rs m rs'' m''
+   .
+
+Inductive cfi_step: control_flow_inst -> state -> trace -> state -> Prop :=
+  | exec_MBcall:
+      forall s fb sp sig ros c b rs m f f' ra,
+      find_function_ptr ge ros rs = Some f' ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      rao f c ra ->
+      cfi_step (MBcall sig ros) (State s fb sp (b::c) rs m)
+        E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s)
+                       f' rs m)
+  | exec_MBtailcall:
+      forall s fb stk soff sig ros c rs m f f' m',
+      find_function_ptr ge ros rs = Some f' ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) ->
+      load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      cfi_step (MBtailcall sig ros) (State s fb (Vptr stk soff) c rs m)
+        E0 (Callstate s f' rs m')
+  | exec_MBbuiltin:
+      forall s f sp rs m ef args res b c vargs t vres rs' m',
+      eval_builtin_args ge rs sp m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      rs' = set_res res vres (undef_regs (destroyed_by_builtin ef) rs) ->
+      cfi_step (MBbuiltin ef args res) (State s f sp (b :: c) rs m)
+         t (State s f sp c rs' m')
+  | exec_MBgoto:
+      forall s fb f sp lbl c rs m c',
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      find_label lbl f.(fn_code) = Some c' ->
+      cfi_step (MBgoto lbl) (State s fb sp c rs m)
+        E0 (State s fb sp c' rs m)
+  | exec_MBcond_true:
+      forall s fb f sp cond args lbl c rs m c' rs',
+      eval_condition cond rs##args m = Some true ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      find_label lbl f.(fn_code) = Some c' ->
+      rs' = undef_regs (destroyed_by_cond cond) rs ->
+      cfi_step (MBcond cond args lbl) (State s fb sp c rs m)
+        E0 (State s fb sp c' rs' m)
+  | exec_MBcond_false:
+      forall s f sp cond args lbl b c rs m rs',
+      eval_condition cond rs##args m = Some false ->
+      rs' = undef_regs (destroyed_by_cond cond) rs ->
+      cfi_step (MBcond cond args lbl) (State s f sp (b :: c) rs m)
+        E0 (State s f sp c rs' m)
+  | exec_MBjumptable:
+      forall s fb f sp arg tbl c rs m n lbl c' rs',
+      rs arg = Vint n ->
+      list_nth_z tbl (Int.unsigned n) = Some lbl ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      find_label lbl f.(fn_code) = Some c' ->
+      rs' = undef_regs destroyed_by_jumptable rs ->
+      cfi_step (MBjumptable arg tbl) (State s fb sp c rs m)
+        E0 (State s fb sp c' rs' m)
+  | exec_MBreturn:
+      forall s fb stk soff c rs m f m',
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) ->
+      load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      cfi_step MBreturn (State s fb (Vptr stk soff) c rs m)
+        E0 (Returnstate s rs m')
+  .
+
+Inductive exit_step: option control_flow_inst -> state -> trace -> state -> Prop :=
+  | exec_Some_exit:
+      forall ctl s t s',
+      cfi_step ctl s t s' ->
+      exit_step (Some ctl) s t s'
+  | exec_None_exit:
+      forall stk f sp b lb rs m,
+      exit_step None (State stk f sp (b::lb) rs m) E0 (State stk f sp lb rs m)
+  .
+
+Inductive step: state -> trace -> state -> Prop :=
+  | exec_bblock:
+      forall sf f sp bb c rs m rs' m' t s',
+        body_step sf f sp (body bb) rs m rs' m' ->
+        exit_step (exit bb) (State sf f sp (bb::c) rs' m') t s' ->
+        step (State sf f sp (bb::c) rs m) t s'
+  | exec_function_internal:
+      forall s fb rs m f m1 m2 m3 stk rs',
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
+      let sp := Vptr stk Ptrofs.zero in
+      store_stack m1 sp Tptr f.(fn_link_ofs) (parent_sp s) = Some m2 ->
+      store_stack m2 sp Tptr f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
+      rs' = undef_regs destroyed_at_function_entry rs ->
+      step (Callstate s fb rs m)
+        E0 (State s fb sp f.(fn_code) rs' m3)
+  | exec_function_external:
+      forall s fb rs m t rs' ef args res m',
+      Genv.find_funct_ptr ge fb = Some (External ef) ->
+      extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
+      external_call ef ge args m t res m' ->
+      rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) ->
+      step (Callstate s fb rs m)
+         t (Returnstate s rs' m')
+  | exec_return:
+      forall s f sp ra c rs m,
+      step (Returnstate (Stackframe f sp ra c :: s) rs m)
+        E0 (State s f sp c rs m)
+  .
+
+End RELSEM.
+
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall fb m0,
+      let ge := Genv.globalenv p in
+      Genv.init_mem p = Some m0 ->
+      Genv.find_symbol ge p.(prog_main) = Some fb ->
+      initial_state p (Callstate nil fb (Regmap.init Vundef) m0).
+
+Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall rs m r retcode,
+      loc_result signature_main = One r ->
+      rs r = Vint retcode ->
+      final_state (Returnstate nil rs m) retcode.
+
+Definition semantics (rao: function -> code -> ptrofs -> Prop) (p: program) :=
+  Semantics (step rao) (initial_state p) final_state (Genv.globalenv p).
diff --git a/scheduling/postpass_lib/Machblockgen.v b/scheduling/postpass_lib/Machblockgen.v
new file mode 100644
index 00000000..5a2f2a61
--- /dev/null
+++ b/scheduling/postpass_lib/Machblockgen.v
@@ -0,0 +1,221 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Op.
+Require Import Locations.
+Require Import Conventions.
+Require Stacklayout.
+Require Import Mach.
+Require Import Linking.
+Require Import Machblock.
+
+(** * Tail-recursive (greedy) translation from Mach code to Machblock code *)
+
+Inductive Machblock_inst: Type :=
+| MB_label (lbl: label) 
+| MB_basic (bi: basic_inst)
+| MB_cfi   (cfi: control_flow_inst).
+
+Definition trans_inst (i:Mach.instruction) : Machblock_inst :=
+  match i with
+  | 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 trap chunk addr args dst=> MB_basic (MBload trap chunk addr args dst)
+  | Mstore    chunk addr args src => MB_basic (MBstore    chunk addr args src)
+  | Mlabel l => MB_label l
+  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 add_basic bi bb :={| header := nil; body := bi::(body bb); exit := (exit bb) |}.
+Extraction Inline add_basic.
+
+Definition cfi_bblock cfi:={| header := nil; body := nil; exit := Some cfi |}.
+Extraction Inline cfi_bblock.
+
+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.
+
+(** Adding an instruction to the beginning of a bblock list by
+
+- either adding the instruction to the head of the list,
+
+- or creating a new bblock with the instruction 
+*)
+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 => bl
+  | i::c0 =>
+    trans_code_rev c0 (add_to_code (trans_inst i) bl)
+  end.
+
+Function trans_code (c: Mach.code) : code :=
+  trans_code_rev (List.rev_append c nil) nil.
+
+Definition transf_function (f: Mach.function) : function :=
+  {| fn_sig:=Mach.fn_sig f;
+     fn_code:=trans_code (Mach.fn_code f);
+     fn_stacksize := Mach.fn_stacksize f;
+     fn_link_ofs := Mach.fn_link_ofs f;
+     fn_retaddr_ofs := Mach.fn_retaddr_ofs f
+ |}.
+
+Definition transf_fundef (f: Mach.fundef) : fundef :=
+  transf_fundef transf_function f.
+
+Definition transf_program (src: Mach.program) : program :=
+  transform_program transf_fundef src.
+
+
+(** * Abstracting trans_code with a simpler inductive relation *)
+
+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: core.
+
+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: core.
+
+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]; cbn.
+  - 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; cbn in * |- *; congruence.
+    + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b].
+      * eapply Tr_add_basic; eauto.
+      * replace (add_basic bi empty_bblock) with (add_to_new_bblock (MB_basic bi)); auto.
+        rewrite Heqti; eapply Tr_end_block; eauto.
+        rewrite <- Heqti. eapply End_basic. congruence.
+    + intros.
+      replace (cfi_bblock cfi) with (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: core.
+
+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]; cbn; 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; cbn; auto.
+     * destruct (header bh); congruence.
+     * destruct bl0; cbn; congruence.
+  + (* case Tr_add_basic *) rewrite H3. cbn. 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]; cbn; 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: core.
+
+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/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v
new file mode 100644
index 00000000..fc722887
--- /dev/null
+++ b/scheduling/postpass_lib/Machblockgenproof.v
@@ -0,0 +1,824 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Op.
+Require Import Locations.
+Require Import Conventions.
+Require Stacklayout.
+Require Import Mach.
+Require Import Linking.
+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).
+
+Definition match_prog (p: Mach.program) (tp: Machblock.program) :=
+  match_program (fun _ f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match: forall p tp, transf_program p = tp -> match_prog p tp.
+Proof.
+  intros. rewrite <- H. eapply match_transform_program; eauto.
+Qed.
+
+Definition trans_stackframe (msf: Mach.stackframe) : stackframe :=
+  match msf with
+  | Mach.Stackframe f sp retaddr c => Stackframe f sp retaddr (trans_code c)
+  end.
+
+Fixpoint trans_stack (mst: list Mach.stackframe) : list stackframe :=
+  match mst with
+  | nil => nil
+  | msf :: mst0 => (trans_stackframe msf) :: (trans_stack mst0)
+  end.
+
+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
+  | Mach.Returnstate  s rs m        => Returnstate  (trans_stack s) rs m
+  end.
+
+Section PRESERVATION.
+
+Local Open Scope nat_scope.
+
+Variable prog: Mach.program.
+Variable tprog: Machblock.program.
+Hypothesis TRANSF: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+
+Variable rao: function -> code -> ptrofs -> Prop.
+
+Definition match_states: Mach.state -> state -> Prop 
+  := ForwardSimulationBlock.match_states (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog) trans_state.
+
+Lemma match_states_trans_state s1: match_states s1 (trans_state s1).
+Proof.
+  apply match_states_trans_state.
+Qed.
+
+Local Hint Resolve match_states_trans_state: core.
+
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof (Genv.find_symbol_match TRANSF).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
+
+Lemma init_mem_preserved:
+  forall m,
+  Genv.init_mem prog = Some m ->
+  Genv.init_mem tprog = Some m.
+Proof (Genv.init_mem_transf TRANSF).
+
+Lemma prog_main_preserved:
+  prog_main tprog = prog_main prog.
+Proof (match_program_main TRANSF).
+
+Lemma functions_translated:
+  forall b f,
+  Genv.find_funct_ptr ge b = Some f ->
+  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = tf.
+Proof.
+  intros.
+  exploit (Genv.find_funct_ptr_match TRANSF); eauto. intro.
+  destruct H0 as (cunit & tf & A & B & C).
+  eapply ex_intro. intuition; eauto. subst. eapply A.
+Qed.
+
+Lemma find_function_ptr_same:
+  forall s rs,
+  Mach.find_function_ptr ge s rs = find_function_ptr tge s rs.
+Proof.
+  intros. unfold Mach.find_function_ptr. unfold find_function_ptr.
+  destruct s; auto.
+  rewrite symbols_preserved; auto.
+Qed.
+
+Lemma find_funct_ptr_same:
+  forall f f0,
+  Genv.find_funct_ptr ge f = Some (Internal f0) ->
+  Genv.find_funct_ptr tge f = Some (Internal (transf_function f0)).
+Proof.
+  intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto.
+Qed.
+
+Lemma find_funct_ptr_same_external:
+  forall f f0,
+  Genv.find_funct_ptr ge f = Some (External f0) ->
+  Genv.find_funct_ptr tge f = Some (External f0).
+Proof.
+  intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto.
+Qed.
+
+Lemma parent_sp_preserved:
+  forall s,
+  Mach.parent_sp s = parent_sp (trans_stack s).
+Proof.
+  unfold parent_sp. unfold Mach.parent_sp. destruct s; cbn; auto.
+  unfold trans_stackframe. destruct s; cbn; auto.
+Qed.
+
+Lemma parent_ra_preserved:
+  forall s,
+  Mach.parent_ra s = parent_ra (trans_stack s).
+Proof.
+  unfold parent_ra. unfold Mach.parent_ra. destruct s; cbn; auto.
+  unfold trans_stackframe. destruct s; cbn; auto.
+Qed.
+
+Lemma external_call_preserved:
+  forall ef args m t res m',
+  external_call ef ge args m t res m' ->
+  external_call ef tge args m t res m'.
+Proof.
+  intros. eapply external_call_symbols_preserved; eauto.
+  apply senv_preserved.
+Qed.
+
+Lemma Mach_find_label_split l i c c':
+  Mach.find_label l (i :: c) = Some c' ->
+   (i=Mlabel l /\ c' = c) \/ (i <> Mlabel l /\ Mach.find_label l c = Some c').
+Proof.
+  intros H.
+  destruct i; try (constructor 2; split; auto; discriminate ).
+  destruct (peq l0 l) as [P|P].
+  - constructor. subst l0; split; auto.
+    revert H. unfold Mach.find_label. cbn. rewrite peq_true.
+    intros H; injection H; auto.
+  - constructor 2. split.
+    + intro F. injection F. intros. contradict P; auto.
+    + revert H. unfold Mach.find_label. cbn. 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; cbn in * |- *; try (destruct (in_dec l nil); intuition).
+  inversion H.
+  destruct (in_dec l (l0::nil)) as [H6|H6]; auto.
+  cbn 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; cbn; 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; cbn; auto.
+Qed.
+
+Definition concat (h: list label) (c: code): code :=
+  match c with
+  | nil =>  {| header := h; body := nil; exit := None |}::nil
+  | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c'
+  end.
+
+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. remember (trans_code _) as bl.
+  rewrite <- is_trans_code_inv in * |-.
+  induction Heqbl. 
+  + (* Tr_nil *) 
+    intros; exists (l::nil); cbn 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; cbn; auto.
+      inversion H as [mbi H1 H2| | ].
+      subst.
+      inversion Heqbl.
+      subst.
+      exists (l :: nil); cbn; 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; cbn; eauto.
+      subst_is_trans_code Heqbl.
+      exists (l :: nil); cbn; eauto.
+    - subst; assert (H: l0 <> l); try congruence; clear H0.
+      exploit IHHeqbl; eauto.
+      clear IHHeqbl Heqbl.
+      intros (h & H3 & H4).
+      cbn; unfold is_label, add_label; cbn.
+      destruct (in_dec l (l0::header bh)) as [H5|H5]; cbn in H5.
+      * destruct H5; try congruence.
+        exists (l0::h); cbn; intuition.
+        rewrite find_label_at_begin in H4; auto.
+        apply f_equal. inversion H4 as [H5]. clear H4.
+        destruct (trans_code c'); cbn in * |- *;
+        inversion H5; subst; cbn; 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 ->
+  exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)).
+Proof.
+  intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto.
+  apply find_label_transcode_preserved; auto.
+Qed.
+
+Lemma mem_free_preserved:
+  forall m stk f,
+  Mem.free m stk 0 (Mach.fn_stacksize f) = Mem.free m stk 0 (fn_stacksize (transf_function f)).
+Proof.
+  intros. auto.
+Qed.
+
+Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated
+                   parent_sp_preserved: core.
+
+
+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
+  | Mach.State _ _ _ c _ _ => dist_end_block_code c
+  | _ => 0
+  end.
+
+Local Hint Resolve exec_nil_body exec_cons_body: core.
+Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore: core.
+
+Lemma size_add_label l bh: size (add_label l bh) = size bh + 1.
+Proof.
+  unfold add_label, size; cbn; 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; cbn. omega.
+Qed.
+
+
+Lemma size_add_to_newblock i: size (add_to_new_bblock i) = 1.
+Proof.
+  destruct i; auto.
+Qed.
+
+
+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.
+  unfold dist_end_block_code.
+  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: core.
+
+
+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: core.
+Local Hint Resolve MBbasic_is_not_cfi: core.
+
+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; cbn in H; congruence.
+  + unfold cfi_bblock in H; cbn in H; congruence.
+Qed.
+
+Local Hint Resolve Mlabel_is_not_basic: core.
+
+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 * |- *); cbn in * |- *;
+  try congruence.
+  + (* label at end block *)
+    inversion H1; subst. inversion H0; subst.
+    assert (X:i=Mlabel lbl). { destruct i; cbn 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; cbn; try congruence.
+      * exploit (add_to_new_block_is_label i0); eauto.
+        intros (l & H8); subst; cbn; congruence.
+      * exploit H3; eauto.
+      * exploit (add_to_new_block_is_label i0); eauto.
+        intros (l & H8); subst; cbn; 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; cbn; 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):
+  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.
+  destruct i; cbn in * |-;
+   (discriminate
+    || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)).
+  - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro.
+    destruct H3 as (tf & A & B). subst. eapply A.
+    all: cbn; rewrite <- parent_sp_preserved; auto.
+  - eapply exec_MBop; eauto. rewrite <- H. destruct o; cbn; auto. destruct (rs ## l); cbn; auto.
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBload; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBstore; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+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; cbn.
+  + 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: core.
+Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same: core.
+
+
+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.
+  intros; constructor 1; cbn.
+  + intros (t0 & s1' & H0) t s'. 
+    remember (trans_code _) as bl.
+    destruct bl as [|bh bl]. 
+    { rewrite <- is_trans_code_inv in Heqbl; inversion Heqbl; inversion H0; congruence. } 
+    clear H0.
+    cbn; constructor 1; 
+    intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; cbn in * |- *; 
+    eapply exec_bblock; eauto; cbn;
+    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 (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.
+  destruct i; cbn 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.
+    - cbn; rewrite <- parent_sp_preserved; auto.
+    - cbn; 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 (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.
+  * exploit find_label_transcode_preserved; eauto. intros (h & 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_MBreturn; eauto.
+    rewrite parent_sp_preserved in H0; subst; auto.
+    rewrite parent_ra_preserved in H1; subst; auto. 
+Qed.
+
+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.
+  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; cbn.
+    autorewrite  with trace_rewrite.
+    exists s2.
+    split;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' ->
+  exists s2', step rao tge (trans_state s1) t s2' /\ match_states s1' s2'.
+Proof.
+  destruct s1; cbn.
+  + (* State *)
+    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; cbn.
+      inversion_clear H;
+      inversion_clear H0. 
+    }
+    assert (X: Datatypes.S (dist_end_block_code c) = (size b)).
+    {
+      unfold dist_end_block_code. 
+      subst_is_trans_code Heqtc.
+      lapply (size_nonzero c b bl); auto.
+      omega.
+    }
+    rewrite X in H; unfold size in H.
+    (* 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&s1''&H&H1&H2).
+    subst t3; clear H0.
+    exploit trans_code_decompose; eauto. clear Heqtc.
+    intros (c0&c1&c2&Hc0&Hc1&Hc2&Heqtc).
+    (* header steps *)
+    exploit step_simu_header; eauto.
+    clear H; intros [X1 X2]; subst.
+    (* body steps *)
+    exploit (star_step_simu_body_step); eauto.
+    clear H1; intros (rs'&m'&H0&H1&H2). subst.
+    autorewrite with trace_rewrite.
+    (* exit step *)
+    exploit step_simu_exit_step; eauto.
+    clear H3; intros (s2' & H3 & H4).
+    eapply ex_intro; intuition eauto.
+    eapply exec_bblock; eauto.
+  + (* Callstate *)
+    intros t s1' H; inversion_clear H.
+    eapply ex_intro; constructor 1; eauto.
+    inversion H1; subst; clear H1.
+    inversion_clear H0; cbn.
+    - (* function_internal*)
+      cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto.
+      eapply exec_function_internal; eauto.
+      rewrite <- parent_sp_preserved; eauto.
+      rewrite <- parent_ra_preserved; eauto.
+    - (* function_external *)
+      autorewrite with trace_rewrite.
+      eapply exec_function_external; eauto.
+      apply find_funct_ptr_same_external; auto.
+      rewrite <- parent_sp_preserved; eauto.
+  +  (* Returnstate *)
+    intros t s1' H; inversion_clear H.
+    eapply ex_intro; constructor 1; eauto.
+    inversion H1; subst; clear H1.
+    inversion_clear H0; cbn.
+    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;cbn in H;try(congruence); ( 
+    remember (trans_code _) as bl; 
+    rewrite <- is_trans_code_inv in Heqbl;
+    inversion Heqbl; subst; cbn 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 H2.
+    destruct H1; cbn in * |- *; omega || (intuition auto);
+    destruct H2; eapply cfi_dist_end_block; cbn; eauto.
+(* public_preserved *)
+  - apply senv_preserved.
+(* match_initial_states *)
+  - intros. cbn.
+    eapply ex_intro; constructor 1.
+    eapply match_states_trans_state.
+    destruct H. split.
+    apply init_mem_preserved; auto.
+    rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved.
+(* match_final_states *)
+  - intros. cbn. destruct H. split with (r := r); auto.
+(* final_states_end_block *)
+  - intros. cbn in H0.
+    inversion H0.
+    inversion H; cbn; auto.
+    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; cbn in * |- *; try congruence ).
+    exists nil; cbn; 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(cbn; congruence).
+      cbn in H5; congruence. }
+    all: try(exists nil; cbn; eexists;  eapply  Tr_add_basic; eauto; inversion H; try(eauto || congruence)).
+  - (*i=cfi*)
+    destruct i; try(cbn 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; cbn; 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; cbn; 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; cbn 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'; cbn; eauto with coqlib.
+    * exploit (trans_code_monotonic i c2); eauto.
+      intros (l' & b' & Hl'); rewrite Hl'.
+      cbn; 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.