k1c -> kvx changes

5 files changed, 2789 insertions, 0 deletions

diff --git a/kvx/lib/Asmblockgenproof0.v b/kvx/lib/Asmblockgenproof0.v
new file mode 100644
index 00000000..1af59238
--- /dev/null
+++ b/kvx/lib/Asmblockgenproof0.v
@@ -0,0 +1,982 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           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.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** * "block" version of Asmgenproof0
+
+    This module is largely adapted from Asmgenproof0.v of the other backends
+    It needs to stand apart because of the block structure, and the distinction control/basic that there isn't in the other backends
+    It has similar definitions than Asmgenproof0, but adapted to this new structure *)
+
+Require Import Coqlib.
+Require Intv.
+Require Import AST.
+Require Import Errors.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Locations.
+Require Import Machblock.
+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] *)
+Require Import Asmblockprops.
+
+Module MB:=Machblock.
+Module AB:=Asmblock.
+
+Lemma ireg_of_eq:
+  forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
+Proof.
+  unfold ireg_of; intros. destruct (preg_of r); inv H; auto.
+Qed.
+
+Lemma freg_of_eq:
+  forall r r', freg_of r = OK r' -> preg_of r = IR r'.
+Proof.
+  unfold freg_of; intros. destruct (preg_of r); inv H; auto.
+Qed.
+
+Lemma preg_of_injective:
+  forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
+Proof.
+  destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
+Qed.
+
+Lemma undef_regs_other:
+  forall r rl rs,
+  (forall r', In r' rl -> r <> r') ->
+  undef_regs rl rs r = rs r.
+Proof.
+  induction rl; simpl; intros. auto.
+  rewrite IHrl by auto. rewrite Pregmap.gso; auto.
+Qed.
+
+Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop :=
+  match rl with
+  | nil => True
+  | r1 :: nil => r <> preg_of r1
+  | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl
+  end.
+
+Remark preg_notin_charact:
+  forall r rl,
+  preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr).
+Proof.
+  induction rl; simpl; intros.
+  tauto.
+  destruct rl.
+  simpl. split. intros. intuition congruence. auto.
+  rewrite IHrl. split.
+  intros [A B]. intros. destruct H. congruence. auto.
+  auto.
+Qed.
+
+Lemma undef_regs_other_2:
+  forall r rl rs,
+  preg_notin r rl ->
+  undef_regs (map preg_of rl) rs r = rs r.
+Proof.
+  intros. apply undef_regs_other. intros.
+  exploit list_in_map_inv; eauto. intros [mr [A B]]. subst.
+  rewrite preg_notin_charact in H. auto.
+Qed.
+
+(** * Agreement between Mach registers and processor registers *)
+
+Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree {
+  agree_sp: rs#SP = sp;
+  agree_sp_def: sp <> Vundef;
+  agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r))
+}.
+
+Lemma preg_val:
+  forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r).
+Proof.
+  intros. destruct H. auto.
+Qed.
+
+Lemma preg_vals:
+  forall ms sp rs, agree ms sp rs ->
+  forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)).
+Proof.
+  induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto.
+Qed.
+
+Lemma sp_val:
+  forall ms sp rs, agree ms sp rs -> sp = rs#SP.
+Proof.
+  intros. destruct H; auto.
+Qed.
+
+Lemma ireg_val:
+  forall ms sp rs r r',
+  agree ms sp rs ->
+  ireg_of r = OK r' ->
+  Val.lessdef (ms r) rs#r'.
+Proof.
+  intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto.
+Qed.
+
+Lemma freg_val:
+  forall ms sp rs r r',
+  agree ms sp rs ->
+  freg_of r = OK r' ->
+  Val.lessdef (ms r) (rs#r').
+Proof.
+  intros. rewrite <- (freg_of_eq _ _ H0). eapply preg_val; eauto.
+Qed.
+
+Lemma agree_exten:
+  forall ms sp rs rs',
+  agree ms sp rs ->
+  (forall r, data_preg r = true -> rs'#r = rs#r) ->
+  agree ms sp rs'.
+Proof.
+  intros. destruct H. split; auto.
+  rewrite H0; auto. auto.
+  intros. rewrite H0; auto. apply preg_of_data.
+Qed.
+
+(** Preservation of register agreement under various assignments. *)
+
+Lemma agree_set_mreg:
+  forall ms sp rs r v rs',
+  agree ms sp rs ->
+  Val.lessdef v (rs'#(preg_of r)) ->
+  (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Mach.Regmap.set r v ms) sp rs'.
+Proof.
+  intros. destruct H. split; auto.
+  rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP.
+  intros. unfold Mach.Regmap.set. destruct (Mach.RegEq.eq r0 r). congruence.
+  rewrite H1. auto. apply preg_of_data.
+  red; intros; elim n. eapply preg_of_injective; eauto.
+Qed.
+
+Corollary agree_set_mreg_parallel:
+  forall ms sp rs r v v',
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs).
+Proof.
+  intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto.
+Qed.
+
+Lemma agree_set_other:
+  forall ms sp rs r v,
+  agree ms sp rs ->
+  data_preg r = false ->
+  agree ms sp (rs#r <- v).
+Proof.
+  intros. apply agree_exten with rs. auto.
+  intros. apply Pregmap.gso. congruence.
+Qed.
+
+Lemma agree_nextblock:
+  forall ms sp rs b,
+  agree ms sp rs -> agree ms sp (nextblock b rs).
+Proof.
+  intros. unfold nextblock. apply agree_set_other. auto. auto.
+Qed.
+
+Lemma agree_set_pair:
+  forall sp p v v' ms rs,
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs).
+Proof.
+  intros. destruct p; simpl.
+- apply agree_set_mreg_parallel; auto.
+- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
+  apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
+Qed.
+
+Lemma agree_undef_nondata_regs:
+  forall ms sp rl rs,
+  agree ms sp rs ->
+  (forall r, In r rl -> data_preg r = false) ->
+  agree ms sp (undef_regs rl rs).
+Proof.
+  induction rl; simpl; intros. auto.
+  apply IHrl. apply agree_exten with rs; auto.
+  intros. apply Pregmap.gso. red; intros; subst.
+  assert (data_preg a = false) by auto. congruence.
+  intros. apply H0; auto.
+Qed.
+
+Lemma agree_undef_regs:
+  forall ms sp rl rs rs',
+  agree ms sp rs ->
+  (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') ->
+  agree (Mach.undef_regs rl ms) sp rs'.
+Proof.
+  intros. destruct H. split; auto.
+  rewrite <- agree_sp0. apply H0; auto.
+  rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP.
+  intros. destruct (In_dec mreg_eq r rl).
+  rewrite Mach.undef_regs_same; auto.
+  rewrite Mach.undef_regs_other; auto. rewrite H0; auto.
+  apply preg_of_data.
+  rewrite preg_notin_charact. intros; red; intros. elim n.
+  exploit preg_of_injective; eauto. congruence.
+Qed.
+
+Lemma agree_set_undef_mreg:
+  forall ms sp rs r v rl rs',
+  agree ms sp rs ->
+  Val.lessdef v (rs'#(preg_of r)) ->
+  (forall r', data_preg r' = true -> r' <> preg_of r -> preg_notin r' rl -> rs'#r' = rs#r') ->
+  agree (Mach.Regmap.set r v (Mach.undef_regs rl ms)) sp rs'.
+Proof.
+  intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto.
+  apply agree_undef_regs with rs; auto.
+  intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of r)).
+  congruence. auto.
+  intros. rewrite Pregmap.gso; auto.
+Qed.
+
+Lemma agree_undef_caller_save_regs:
+  forall ms sp rs,
+  agree ms sp rs ->
+  agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs).
+Proof.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split.
+- unfold proj_sumbool; rewrite dec_eq_true. auto.
+- auto.
+- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
+  destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
++ apply list_in_map_inv in i. destruct i as (mr & A & B). 
+  assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
+  apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
++ destruct (is_callee_save r) eqn:CS; auto.
+  elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
+Qed.
+
+Lemma agree_change_sp:
+  forall ms sp rs sp',
+  agree ms sp rs -> sp' <> Vundef ->
+  agree ms sp' (rs#SP <- sp').
+Proof.
+  intros. inv H. split; auto.
+  intros. rewrite Pregmap.gso; auto with asmgen.
+Qed.
+
+(** Connection between Mach and Asm calling conventions for external
+    functions. *)
+
+Lemma extcall_arg_match:
+  forall ms sp rs m m' l v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Mach.extcall_arg ms m sp l v ->
+  exists v', AB.extcall_arg rs m' l v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1.
+  exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto.
+  unfold Mach.load_stack in H2.
+  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
+  rewrite (sp_val _ _ _ H) in A.
+  exists v'; split; auto.
+  econstructor. eauto. assumption.
+Qed.
+
+Lemma extcall_arg_pair_match:
+  forall ms sp rs m m' p v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Mach.extcall_arg_pair ms m sp p v ->
+  exists v', AB.extcall_arg_pair rs m' p v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1.
+- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto.
+- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1).
+  exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2).
+  exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto.
+Qed.
+
+
+Lemma extcall_args_match:
+  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall ll vl,
+  list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl ->
+  exists vl', list_forall2 (AB.extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; intros.
+  exists (@nil val); split. constructor. constructor.
+  exploit extcall_arg_pair_match; eauto. intros [v1' [A B]].
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
+Qed.
+
+Lemma extcall_arguments_match:
+  forall ms m m' sp rs sg args,
+  agree ms sp rs -> Mem.extends m m' ->
+  Mach.extcall_arguments ms m sp sg args ->
+  exists args', AB.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
+Proof.
+  unfold Mach.extcall_arguments, AB.extcall_arguments; intros.
+  eapply extcall_args_match; eauto.
+Qed.
+
+Remark builtin_arg_match:
+  forall ge (rs: regset) sp m a v,
+  eval_builtin_arg ge (fun r => rs (preg_of r)) sp m a v ->
+  eval_builtin_arg ge rs sp m (map_builtin_arg preg_of a) v.
+Proof.
+  induction 1; simpl; eauto with barg.
+Qed.
+
+Lemma builtin_args_match:
+  forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall al vl, eval_builtin_args ge ms sp m al vl ->
+  exists vl', eval_builtin_args ge rs sp m' (map (map_builtin_arg preg_of) al) vl'
+           /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; intros; simpl.
+  exists (@nil val); split; constructor.
+  exploit (@eval_builtin_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto.
+  intros; eapply preg_val; eauto.
+  intros (v1' & A & B).
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto.
+Qed.
+
+Lemma agree_set_res:
+  forall res ms sp rs v v',
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.set_res res v ms) sp (AB.set_res (map_builtin_res preg_of res) v' rs).
+Proof.
+  induction res; simpl; intros.
+- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto.
+  intros. apply Pregmap.gso; auto.
+- auto.
+- apply IHres2. apply IHres1. auto.
+  apply Val.hiword_lessdef; auto.
+  apply Val.loword_lessdef; auto.
+Qed.
+
+Lemma set_res_other:
+  forall r res v rs,
+  data_preg r = false ->
+  set_res (map_builtin_res preg_of res) v rs r = rs r.
+Proof.
+  induction res; simpl; intros.
+- apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate.
+- auto.
+- rewrite IHres2, IHres1; auto.
+Qed.
+
+(* inspired from Mach *)
+
+Lemma find_label_tail:
+  forall lbl c c', MB.find_label lbl c = Some c' -> is_tail c' c.
+Proof.
+  induction c; simpl; intros. discriminate.
+  destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib.
+Qed.
+
+(* inspired from Asmgenproof0 *)
+
+(* ... skip ... *)
+
+(** The ``code tail'' of an instruction list [c] is the list of instructions
+  starting at PC [pos]. *)
+
+Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
+  | code_tail_0: forall c,
+      code_tail 0 c c
+  | code_tail_S: forall pos bi c1 c2,
+      code_tail pos c1 c2 ->
+      code_tail (pos + (size bi)) (bi :: c1) c2.
+
+Lemma code_tail_pos:
+  forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
+Proof.
+  induction 1. omega. generalize (size_positive bi); intros; omega.
+Qed.
+
+Lemma find_bblock_tail:
+  forall c1 bi c2 pos,
+  code_tail pos c1 (bi :: c2) ->
+  find_bblock pos c1 = Some bi.
+Proof.
+  induction c1; simpl; intros.
+  inversion H.  
+  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
+  destruct (zeq pos 0). subst pos.
+  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
+  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
+  eauto.
+Qed.
+
+
+Local Hint Resolve code_tail_0 code_tail_S: core.
+
+Lemma code_tail_next:
+  forall fn ofs c0,
+  code_tail ofs fn c0 ->
+  forall bi c1, c0 = bi :: c1 -> code_tail (ofs + (size bi)) fn c1.
+Proof.
+  induction 1; intros.
+  - subst; eauto.
+  - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
+    omega.
+Qed.
+
+Lemma size_blocks_pos c: 0 <= size_blocks c.
+Proof.
+  induction c as [| a l ]; simpl; try omega.
+  generalize (size_positive a); omega.
+Qed.
+
+Remark code_tail_positive:
+  forall fn ofs c,
+  code_tail ofs fn c -> 0 <= ofs.
+Proof.
+  induction 1; intros; simpl.
+  - omega.
+  - generalize (size_positive bi). omega.
+Qed.
+
+Remark code_tail_size:
+  forall fn ofs c,
+  code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
+Proof.
+  induction 1; intros; simpl; try omega.
+Qed.
+
+Remark code_tail_bounds fn ofs c:
+  code_tail ofs fn c -> 0 <= ofs <= size_blocks fn.
+Proof.
+  intro H; 
+  exploit code_tail_size; eauto.
+  generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
+  omega.
+Qed.
+
+Local Hint Resolve code_tail_next: core.
+
+Lemma code_tail_next_int:
+  forall fn ofs bi c,
+  size_blocks fn <= Ptrofs.max_unsigned ->
+  code_tail (Ptrofs.unsigned ofs) fn (bi :: c) ->
+  code_tail (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bi)))) fn c.
+Proof.
+  intros. 
+  exploit code_tail_size; eauto.
+  simpl; generalize (code_tail_positive _ _ _ H0), (size_positive bi), (size_blocks_pos c).
+  intros.
+  rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
+  - rewrite Ptrofs.unsigned_repr; eauto.
+    omega.
+  - rewrite Ptrofs.unsigned_repr; omega.
+Qed.
+
+(** Predictor for return addresses in generated Asm code.
+
+  The [return_address_offset] predicate defined here is used in the
+  semantics for Mach to determine the return addresses that are
+  stored in activation records. *)
+
+(** Consider a Mach function [f] and a sequence [c] of Mach instructions
+  representing the Mach code that remains to be executed after a
+  function call returns.  The predicate [return_address_offset f c ofs]
+  holds if [ofs] is the integer offset of the PPC instruction
+  following the call in the Asm code obtained by translating the
+  code of [f]. Graphically:
+<<
+     Mach function f    |--------- Mcall ---------|
+         Mach code c    |                |--------|
+                        |                 \        \
+                        |                  \        \
+                        |                   \        \
+     Asm code           |                    |--------|
+     Asm function       |------------- Pcall ---------|
+
+                        <-------- ofs ------->
+>>
+*)
+
+Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : Prop :=
+  forall tf  tc,
+  transf_function f = OK tf ->
+  transl_blocks f c false = OK tc ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc.
+
+Lemma transl_blocks_tail:
+  forall f c1 c2, is_tail c1 c2 ->
+  forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 ->
+  exists tc1, exists ep1, transl_blocks f c1 ep1 = OK tc1 /\ is_tail tc1 tc2.
+Proof.
+  induction 1; simpl; intros.
+  exists tc2; exists ep2; split; auto with coqlib.
+  monadInv H0. exploit IHis_tail; eauto. intros (tc1 & ep1 & A & B).
+  exists tc1; exists ep1; split. auto.
+  eapply is_tail_trans with x0; eauto with coqlib.
+Qed.
+
+Lemma is_tail_code_tail:
+  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
+Proof.
+  induction 1; eauto.
+  destruct IHis_tail; eauto. 
+Qed.
+
+Section RETADDR_EXISTS.
+
+Hypothesis transf_function_inv:
+  forall f tf, transf_function f = OK tf ->
+  exists tc ep, transl_blocks f (Machblock.fn_code f) ep = OK tc /\ is_tail tc (fn_blocks tf).
+
+Hypothesis transf_function_len:
+  forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned.
+
+
+Lemma return_address_exists:
+  forall b f c, is_tail (b :: c) f.(MB.fn_code) ->
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros. destruct (transf_function f) as [tf|] eqn:TF.
+  + exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1).
+    exploit transl_blocks_tail; eauto. intros (tc2 & ep2 & TR2 & TL2).
+    monadInv TR2.
+    assert (TL3: is_tail x0 (fn_blocks tf)).
+    { apply is_tail_trans with tc1; auto. 
+      apply is_tail_trans with (x++x0); auto. eapply is_tail_app.
+    }
+    exploit is_tail_code_tail. eexact TL3. intros [ofs CT].
+    exists (Ptrofs.repr ofs). red; intros.
+    rewrite Ptrofs.unsigned_repr. congruence.
+    exploit code_tail_bounds; eauto.
+    intros; apply transf_function_len in TF. omega.
+  + exists Ptrofs.zero; red; intros. congruence.
+Qed.
+
+End RETADDR_EXISTS.
+
+(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points
+  within the Asmblock code generated by translating Machblock function [f],
+  and [tc] is the tail of the generated code at the position corresponding
+  to the code pointer [pc]. *)
+
+Inductive transl_code_at_pc (ge: MB.genv):
+    val -> block -> MB.function -> MB.code -> bool -> AB.function -> AB.bblocks -> Prop :=
+  transl_code_at_pc_intro:
+    forall b ofs f c ep tf tc,
+    Genv.find_funct_ptr ge b = Some(Internal f) ->
+    transf_function f = Errors.OK tf ->
+    transl_blocks f c ep = OK tc ->
+    code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc ->
+    transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc.
+
+Remark code_tail_no_bigger:
+  forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
+Proof.
+  induction 1; simpl; omega.
+Qed.
+
+Remark code_tail_unique:
+  forall fn c pos pos',
+  code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
+Proof.
+  induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  f_equal. eauto.
+Qed.
+
+Lemma return_address_offset_correct:
+  forall ge b ofs fb f c tf tc ofs',
+  transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc ->
+  return_address_offset f c ofs' ->
+  ofs' = ofs.
+Proof.
+  intros. inv H. red in H0.
+  exploit code_tail_unique. eexact H12. eapply H0; eauto. intro.
+  rewrite <- (Ptrofs.repr_unsigned ofs).
+  rewrite <- (Ptrofs.repr_unsigned ofs').
+  congruence.
+Qed.
+
+(** The [find_label] function returns the code tail starting at the
+  given label.  A connection with [code_tail] is then established. *)
+
+Fixpoint find_label (lbl: label) (c: bblocks) {struct c} : option bblocks :=
+  match c with
+  | nil => None
+  | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl
+  end.
+
+Lemma label_pos_code_tail:
+  forall lbl c pos c',
+  find_label lbl c = Some c' ->
+  exists pos',
+  label_pos lbl pos c = Some pos'
+  /\ code_tail (pos' - pos) c c'
+  /\ pos <= pos' <= pos + size_blocks c.
+Proof.
+  induction c.
+  simpl; intros. discriminate.
+  simpl; intros until c'.
+  case (is_label lbl a).
+  - intros. inv H. exists pos. split; auto. split.
+    replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
+    generalize (size_blocks_pos c). generalize (size_positive a). omega.
+  - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
+  exists pos'. split. auto. split.
+  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
+  constructor. auto. generalize (size_positive a). omega.
+Qed.
+
+(** Helper lemmas to reason about
+- the "code is tail of" property
+- correct translation of labels. *)
+
+Definition tail_nolabel (k c: bblocks) : Prop :=
+  is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k.
+
+Lemma tail_nolabel_refl:
+  forall c, tail_nolabel c c.
+Proof.
+  intros; split. apply is_tail_refl. auto.
+Qed.
+
+Lemma tail_nolabel_trans:
+  forall c1 c2 c3, tail_nolabel c2 c3 -> tail_nolabel c1 c2 -> tail_nolabel c1 c3.
+Proof.
+  intros. destruct H; destruct H0; split.
+  eapply is_tail_trans; eauto.
+  intros. rewrite H1; auto.
+Qed.
+
+Definition nolabel (b: bblock) :=
+  match (header b) with nil => True | _ => False end.
+
+Hint Extern 1 (nolabel _) => exact I : labels.
+
+Lemma tail_nolabel_cons:
+  forall b c k,
+  nolabel b -> tail_nolabel k c -> tail_nolabel k (b :: c).
+Proof.
+  intros. destruct H0. split.
+  constructor; auto.
+  intros. simpl. rewrite <- H1. destruct b as [hd bdy ex]; simpl in *.
+  destruct hd as [|l hd]; simpl in *.
+  - assert (is_label lbl {| AB.header := nil; AB.body := bdy; AB.exit := ex; AB.correct := correct |} = false).
+    { apply is_label_correct_false. simpl header. apply in_nil. }
+    rewrite H2. auto.
+  - contradiction.
+Qed.
+
+Hint Resolve tail_nolabel_refl: labels.
+
+Ltac TailNoLabel :=
+  eauto with labels;
+  match goal with
+  | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel]
+  | [ H: Error _ = OK _ |- _ ] => discriminate
+  | [ H: assertion_failed = OK _ |- _ ] => discriminate
+  | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel
+  | [ H: bind _ _ = OK _ |- _ ] => monadInv H;  TailNoLabel
+  | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel
+  | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabel
+  | _ => idtac
+  end.
+
+Remark tail_nolabel_find_label:
+  forall lbl k c, tail_nolabel k c -> find_label lbl c = find_label lbl k.
+Proof.
+  intros. destruct H. auto.
+Qed.
+
+Remark tail_nolabel_is_tail:
+  forall k c, tail_nolabel k c -> is_tail k c.
+Proof.
+  intros. destruct H. auto.
+Qed.
+
+Lemma exec_body_pc:
+  forall ge l rs1 m1 rs2 m2,
+  exec_body ge l rs1 m1 = Next rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  induction l.
+  - intros. inv H. auto.
+  - intros until m2. intro EXEB.
+    inv EXEB. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate.
+    eapply IHl in H0. rewrite H0.
+    erewrite exec_basic_instr_pc; eauto.
+Qed.
+
+Section STRAIGHTLINE.
+
+Variable ge: genv.
+Variable fn: function.
+
+(** Straight-line code is composed of processor instructions that execute
+  in sequence (no branches, no function calls and returns).
+  The following inductive predicate relates the machine states
+  before and after executing a straight-line sequence of instructions.
+  Instructions are taken from the first list instead of being fetched
+  from memory. *)
+
+Inductive exec_straight: list instruction -> regset -> mem ->
+                         list instruction -> regset -> mem -> Prop :=
+  | exec_straight_one:
+      forall i1 c rs1 m1 rs2 m2,
+      exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 ->
+      exec_straight ((PBasic i1) ::g c) rs1 m1 c rs2 m2
+  | exec_straight_step:
+      forall i c rs1 m1 rs2 m2 c' rs3 m3,
+      exec_basic_instr ge i rs1 m1 = Next rs2 m2 ->
+      exec_straight c rs2 m2 c' rs3 m3 ->
+      exec_straight ((PBasic i) :: c) rs1 m1 c' rs3 m3.
+
+Inductive exec_control_rel: option control -> bblock -> regset -> mem ->
+                             regset -> mem -> Prop :=
+  | exec_control_rel_intro:
+      forall rs1 m1 b rs1' ctl rs2 m2,
+      rs1' = nextblock b rs1 ->
+      exec_control ge fn ctl rs1' m1 = Next rs2 m2 ->
+      exec_control_rel ctl b rs1 m1 rs2 m2.
+
+Inductive exec_bblock_rel: bblock -> regset -> mem -> regset -> mem -> Prop :=
+  | exec_bblock_rel_intro:
+      forall rs1 m1 b rs2 m2,
+      exec_bblock ge fn b rs1 m1 = Next rs2 m2 ->
+      exec_bblock_rel b rs1 m1 rs2 m2.
+
+Lemma exec_straight_body:
+  forall c l rs1 m1 rs2 m2,
+  exec_straight c rs1 m1 nil rs2 m2 ->
+  code_to_basics c = Some l ->
+  exec_body ge l rs1 m1 = Next rs2 m2.
+Proof.
+  induction c as [|i c].
+  - intros until m2. intros EXES CTB. inv EXES.
+  - intros until m2. intros EXES CTB. inv EXES.
+    + inv CTB. simpl. rewrite H6. auto.
+    + inv CTB. destruct (code_to_basics c); try discriminate. inv H0. eapply IHc in H7; eauto.
+      rewrite <- H7. simpl. rewrite H1. auto.
+Qed.
+
+Lemma exec_straight_body2:
+  forall c rs1 m1 c' rs2 m2,
+  exec_straight c rs1 m1 c' rs2 m2 ->
+  exists body,
+     exec_body ge body rs1 m1 = Next rs2 m2
+  /\ (basics_to_code body) ++g c' = c.
+Proof.
+  intros until m2. induction 1.
+  - exists (i1::nil). split; auto. simpl. rewrite H. auto.
+  - destruct IHexec_straight as (bdy & EXEB & BTC).
+    exists (i:: bdy). split; simpl.
+    + rewrite H. auto.
+    + congruence.
+Qed.
+
+Lemma exec_straight_trans:
+  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
+  exec_straight c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight c1 rs1 m1 c3 rs3 m3.
+Proof.
+  induction 1; intros.
+  apply exec_straight_step with rs2 m2; auto.
+  apply exec_straight_step with rs2 m2; auto.
+Qed.
+
+Lemma exec_straight_two:
+  forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
+  exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 ->
+  exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 ->
+  exec_straight (i1 ::g i2 ::g c) rs1 m1 c rs3 m3.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  apply exec_straight_one; auto.
+Qed.
+
+Lemma exec_straight_three:
+  forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
+  exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 ->
+  exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 ->
+  exec_basic_instr ge i3 rs3 m3 = Next rs4 m4 ->
+  exec_straight (i1 ::g i2 ::g i3 ::g c) rs1 m1 c rs4 m4.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  eapply exec_straight_two; eauto.
+Qed.
+
+(** Like exec_straight predicate, but on blocks *)
+
+Inductive exec_straight_blocks: bblocks -> regset -> mem ->
+                                bblocks -> regset -> mem -> Prop :=
+  | exec_straight_blocks_one:
+      forall b1 c rs1 m1 rs2 m2,
+      exec_bblock ge fn b1 rs1 m1 = Next rs2 m2 ->
+      rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b1)) ->
+      exec_straight_blocks (b1 :: c) rs1 m1 c rs2 m2
+  | exec_straight_blocks_step:
+      forall b c rs1 m1 rs2 m2 c' rs3 m3,
+      exec_bblock ge fn b rs1 m1 = Next rs2 m2 ->
+      rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b)) ->
+      exec_straight_blocks c rs2 m2 c' rs3 m3 ->
+      exec_straight_blocks (b :: c) rs1 m1 c' rs3 m3.
+
+Lemma exec_straight_blocks_trans:
+  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
+  exec_straight_blocks c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight_blocks c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight_blocks c1 rs1 m1 c3 rs3 m3.
+Proof.
+  induction 1; intros.
+  apply exec_straight_blocks_step with rs2 m2; auto.
+  apply exec_straight_blocks_step with rs2 m2; auto.
+Qed.
+
+(** Linking exec_straight with exec_straight_blocks *)
+
+Lemma exec_straight_pc:
+  forall c c' rs1 m1 rs2 m2,
+  exec_straight c rs1 m1 c' rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  induction c; intros; try (inv H; fail).
+  inv H.
+  - eapply exec_basic_instr_pc; eauto.
+  - rewrite (IHc c' rs3 m3 rs2 m2); auto.
+    erewrite exec_basic_instr_pc; eauto.
+Qed.
+
+Lemma regset_same_assign (rs: regset) r:
+  rs # r <- (rs r) = rs.
+Proof.
+  apply functional_extensionality. intros x. destruct (preg_eq x r); subst; Simpl.
+Qed.
+
+Lemma exec_straight_through_singleinst:
+  forall a b rs1 m1 rs2 m2 rs2' m2' lb,
+  bblock_single_inst (PBasic a) = b ->
+  exec_straight (a ::g nil) rs1 m1 nil rs2 m2 ->
+  nextblock b rs2 = rs2' -> m2 = m2' ->
+  exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'.
+Proof.
+  intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto.
+  simpl. rewrite regset_same_assign. auto.
+  simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto.
+Qed.
+
+(** The following lemmas show that straight-line executions
+  (predicate [exec_straight_blocks]) correspond to correct Asm executions. *)
+
+Lemma exec_straight_steps_1:
+  forall c rs m c' rs' m',
+  exec_straight_blocks c rs m c' rs' m' ->
+  size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned ->
+  forall b ofs,
+  rs#PC = Vptr b ofs ->
+  Genv.find_funct_ptr ge b = Some (Internal fn) ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c ->
+  plus step ge (State rs m) E0 (State rs' m').
+Proof.
+  induction 1; intros.
+  apply plus_one.
+  econstructor; eauto.
+  eapply find_bblock_tail. eauto.
+  eapply plus_left'.
+  econstructor; eauto.
+  eapply find_bblock_tail. eauto.
+  apply IHexec_straight_blocks with b0 (Ptrofs.add ofs (Ptrofs.repr (size b))).
+  auto. rewrite H0. rewrite H3. reflexivity.
+  auto.
+  apply code_tail_next_int; auto.
+  traceEq.
+Qed.
+
+Lemma exec_straight_steps_2:
+  forall c rs m c' rs' m',
+  exec_straight_blocks c rs m c' rs' m' ->
+  size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned ->
+  forall b ofs,
+  rs#PC = Vptr b ofs ->
+  Genv.find_funct_ptr ge b = Some (Internal fn) ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c ->
+  exists ofs',
+     rs'#PC = Vptr b ofs'
+  /\ code_tail (Ptrofs.unsigned ofs') (fn_blocks fn) c'.
+Proof.
+  induction 1; intros.
+  exists (Ptrofs.add ofs (Ptrofs.repr (size b1))). split.
+  rewrite H0. rewrite H2. auto.
+  apply code_tail_next_int; auto.
+  apply IHexec_straight_blocks with (Ptrofs.add ofs (Ptrofs.repr (size b))).
+  auto. rewrite H0. rewrite H3. reflexivity. auto.
+  apply code_tail_next_int; auto.
+Qed.
+
+End STRAIGHTLINE.
+
+(** * Properties of the Machblock call stack *)
+
+Section MATCH_STACK.
+
+Variable ge: MB.genv.
+
+Inductive match_stack: list MB.stackframe -> Prop :=
+  | match_stack_nil:
+      match_stack nil
+  | match_stack_cons: forall fb sp ra c s f tf tc,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      transl_code_at_pc ge ra fb f c false tf tc ->
+      sp <> Vundef ->
+      match_stack s ->
+      match_stack (Stackframe fb sp ra c :: s).
+
+Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
+Proof.
+  induction 1; simpl.
+  unfold Vnullptr; destruct Archi.ptr64; congruence.
+  auto.
+Qed.
+
+Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
+Proof.
+  induction 1; simpl.
+  unfold Vnullptr; destruct Archi.ptr64; congruence.
+  inv H0. congruence.
+Qed.
+
+Lemma lessdef_parent_sp:
+  forall s v,
+  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
+Proof.
+  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
+Qed.
+
+Lemma lessdef_parent_ra:
+  forall s v,
+  match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s.
+Proof.
+  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
+Qed.
+
+End MATCH_STACK.
diff --git a/kvx/lib/ForwardSimulationBlock.v b/kvx/lib/ForwardSimulationBlock.v
new file mode 100644
index 00000000..f79814f2
--- /dev/null
+++ b/kvx/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.
+
+
+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; simpl.
+  + intros m k H; assert (X: m=0); try omega.
+    assert (X0: k=0); try omega.
+    subst; repeat (eapply ex_intro); intuition eauto.
+  + intros m; destruct m as [| m']; simpl.
+    - 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; simpl. 
+  + 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.
+  + omega.
+  + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)).
+    - eapply starN_tailstep; eauto.
+    - omega.
+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.
+  + omega.
+  + cutrewrite (dist_end_block head - dist_end_block current = 1).
+    - eapply starN_tailstep; eauto.
+    - omega.
+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]. simpl.
+  destruct ms as [ms|]; unfold head; simpl; auto.
+  constructor 1.
+  omega.
+  cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O).
+  + apply starN_refl; auto.
+  + omega.
+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); simpl; 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. simpl in H2; subst.
+  destruct (discr_dist_end rs2) as [H3 | H3].
+  + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl.
+    intuition.
+  + destruct ms2 as [s|].
+    - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl.
+      intuition.
+    - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl.
+      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 |}); simpl.
+    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; simpl.
+  apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); simpl; 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); simpl; 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].
+        cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega.
+        eapply starN_tailstep; eauto.
+      * unfold head; rewrite H2; simpl. 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/kvx/lib/Machblock.v b/kvx/lib/Machblock.v
new file mode 100644
index 00000000..08e0eba2
--- /dev/null
+++ b/kvx/lib/Machblock.v
@@ -0,0 +1,380 @@
+(* *************************************************************)
+(*                                                             *)
+(*             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.
+
+(** 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
+  .
+
+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.
+  simpl 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]. simpl. unfold size. simpl.
+  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 (simpl in Hh; discriminate); auto.
+  destruct b; try (simpl in Hb; discriminate); auto.
+  destruct e; try (simpl in He; discriminate); auto.
+Qed.
+
+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.
+
+(*** sémantique ***)
+
+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)); simpl; 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)); simpl; 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/kvx/lib/Machblockgen.v b/kvx/lib/Machblockgen.v
new file mode 100644
index 00000000..287e4f7b
--- /dev/null
+++ b/kvx/lib/Machblockgen.v
@@ -0,0 +1,216 @@
+(* *************************************************************)
+(*                                                             *)
+(*             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.
+
+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
+  * Either adding the instruction to the head of the list,
+  * or create 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 *)
+
+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]; 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: 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]; 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: 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/kvx/lib/Machblockgenproof.v b/kvx/lib/Machblockgenproof.v
new file mode 100644
index 00000000..dfb97bfe
--- /dev/null
+++ b/kvx/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; simpl; auto.
+  unfold trans_stackframe. destruct s; simpl; 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; simpl; auto.
+  unfold trans_stackframe. destruct s; simpl; 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. simpl. 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. 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
+  | 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); 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 ->
+  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; 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.
+
+
+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; simpl in H; congruence.
+  + unfold cfi_bblock in H; simpl 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 * |- *); 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):
+  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; simpl 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: simpl; rewrite <- parent_sp_preserved; auto.
+  - eapply exec_MBop; eauto. rewrite <- H. destruct o; simpl; auto. destruct (rs ## l); simpl; auto.
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; 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; 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: 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; simpl.
+  + 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.
+    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 (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; 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 (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; simpl.
+    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; simpl.
+  + (* 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; simpl.
+      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; simpl.
+    - (* 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; simpl.
+    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 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 *)
+  - intros. simpl.
+    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. simpl. destruct H. split with (r := r); auto.
+(* final_states_end_block *)
+  - intros. simpl in H0.
+    inversion H0.
+    inversion H; simpl; 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; 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.