Merge branch 'kvx-work' into PseudoAsmblock

9 files changed, 4358 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/IterList.v b/kvx/lib/IterList.v
new file mode 100644
index 00000000..b9eb5922
--- /dev/null
+++ b/kvx/lib/IterList.v
@@ -0,0 +1,85 @@
+Require Import Coqlib.
+
+(** TODO: are these def and lemma already defined in the standard library ?
+
+In this case, it should be better to reuse those of the standard library !
+
+*)
+
+Fixpoint iter {A} (n:nat) (f: A -> A) (x: A) {struct n}: A :=
+  match n with
+  | O => x
+  | S n0 => iter n0 f (f x)
+  end.
+
+Lemma iter_S A (n:nat) (f: A -> A): forall x, iter (S n) f x = f (iter n f x).
+Proof.
+  induction n; simpl; auto.
+  intros; erewrite <- IHn; simpl; auto.
+Qed.
+
+Lemma iter_plus A (n m:nat) (f: A -> A): forall x, iter (n+m) f x = iter m f (iter n f x).
+Proof.
+  induction n; simpl; auto.
+Qed.
+
+Definition iter_tail {A} (n:nat) (l: list A) := iter n (@tl A) l.
+
+Lemma iter_tail_S {A} (n:nat) (l: list A): iter_tail (S n) l = tl (iter_tail n l).
+Proof.
+  apply iter_S.
+Qed.
+
+Lemma iter_tail_plus A (n m:nat) (l: list A): iter_tail (n+m) l = iter_tail m (iter_tail n l).
+Proof.
+  apply iter_plus.
+Qed.
+
+Lemma iter_tail_length A l1: forall (l2: list A), iter_tail (length l1) (l1 ++ l2) = l2.
+Proof.
+  induction l1; auto.
+Qed.
+
+Lemma iter_tail_nil A n: @iter_tail A n nil = nil.
+Proof.
+  unfold iter_tail; induction n; simpl; auto.
+Qed.
+
+Lemma iter_tail_reach_nil A (l: list A): iter_tail (length l) l = nil.
+Proof.
+  rewrite (app_nil_end l) at 2.
+  rewrite iter_tail_length. 
+  auto.
+Qed.
+
+Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat.
+Proof.
+  unfold iter_tail; induction n; auto.
+  intros l; destruct l. { simpl; omega. }
+  intros; simpl. erewrite IHn; eauto.
+  simpl in *; omega.
+Qed.
+
+Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l).
+Proof.
+  unfold iter_tail; induction n; simpl.
+  - intros l; destruct l; simpl; omega || eauto.
+  - intros l H; destruct (IHn (tl l)) as (x & H1).
+    + destruct l; simpl in *; try omega.
+    + rewrite H1; eauto.
+Qed.
+
+Lemma iter_tail_inject1 {A} (n1 n2:nat) (l: list A): (n1 <= List.length l)%nat -> (n2 <= List.length l)%nat -> iter_tail n1 l = iter_tail n2 l -> n1=n2.
+Proof.
+  intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto.
+  rewrite EQ.
+  rewrite (length_iter_tail n2 l); eauto.
+  omega.
+Qed.
+
+Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat.
+Proof.
+  destruct (le_lt_dec n (List.length l)); try omega.
+  intros; exploit (iter_tail_inject1 n (length l) l); try omega.
+  rewrite iter_tail_reach_nil. auto.
+Qed.
\ No newline at end of file
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.
diff --git a/kvx/lib/OptionMonad.v b/kvx/lib/OptionMonad.v
new file mode 100644
index 00000000..824a9c2f
--- /dev/null
+++ b/kvx/lib/OptionMonad.v
@@ -0,0 +1,49 @@
+(* Declare Scope option_monad_scope. *)
+
+Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
+         (at level 200, X ident, A at level 100, B at level 200)
+         : option_monad_scope.
+
+Notation "'ASSERT' A 'IN' B" := (if A then B else None)
+         (at level 200, A at level 100, B at level 200)
+         : option_monad_scope.
+
+Local Open Scope option_monad_scope.
+
+
+(** Simple tactics for option-monad *)
+
+Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B):
+  (forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)).
+Proof.
+  intros; destruct e; simpl; auto.
+Qed.
+
+Lemma destruct_ASSERT B (P: option B -> Prop) (e: bool) (x: option B):
+  (e = true -> P x) -> (e = false -> P None) -> (P (ASSERT e IN x)).
+Proof.
+  intros; destruct e; simpl; auto.
+Qed.
+
+Ltac inversion_SOME x :=
+  try (eapply destruct_SOME; [ let x := fresh x in intro x | simpl; try congruence ]).
+
+Ltac inversion_ASSERT :=
+  try (eapply destruct_ASSERT; [ idtac | simpl; try congruence ]).
+
+Ltac simplify_someHyp :=
+  match goal with
+  | H: None = Some _ |- _  => inversion H; clear H; subst
+  | H: Some _ = None |- _  => inversion H; clear H; subst
+  | H: ?t = ?t |- _ => clear H
+  | H: Some _ = Some _ |- _  => inversion H; clear H; subst
+  | H: Some _ <> None |- _ => clear H
+  | H: None <> Some _ |- _ => clear H
+  | H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H
+  end.
+
+Ltac simplify_someHyps := 
+  repeat (simplify_someHyp; simpl in * |- *).
+
+Ltac try_simplify_someHyps := 
+  try (intros; simplify_someHyps; eauto).
diff --git a/kvx/lib/PseudoAsmblock.v b/kvx/lib/PseudoAsmblock.v
new file mode 100644
index 00000000..336e315c
--- /dev/null
+++ b/kvx/lib/PseudoAsmblock.v
@@ -0,0 +1,262 @@
+Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep.
+Require Import Op Machregs Locations Stacklayout Conventions.
+Require Import Mach Machblock OptionMonad.
+
+
+(** Registers and States *)
+
+Inductive preg: Type :=
+  | PC: preg (* program counter *)
+  | RA: preg (* return-address *)
+  | SP: preg (* stack-pointer *)
+  | preg_of: mreg -> preg.
+Coercion preg_of: mreg >-> preg.
+
+Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
+Proof.
+ decide equality.
+ apply mreg_eq.
+Defined.
+
+Module PregEq.
+  Definition t := preg.
+  Definition eq := preg_eq.
+End PregEq.
+
+Module Pregmap := EMap(PregEq).
+
+Definition regset := Pregmap.t val.
+
+(* Declare Scope asm. *)
+Notation "a # b" := (a b) (at level 1, only parsing) : asm.
+Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+
+
+Definition to_Machrs (rs: regset): Mach.regset :=
+ fun (r:mreg) => rs r.
+Coercion to_Machrs: regset >-> Mach.regset.
+
+Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset :=
+ fun (r:preg) => 
+   match r with 
+   | preg_of mr => mrs mr
+   | _ => rs r
+   end.
+
+Local Open Scope option_monad_scope.
+Local Open Scope asm.
+
+Record state: Type := State { _rs: regset; _m: mem }.
+Definition outcome := option state.
+Definition Next rs m: outcome := Some (State rs m).
+Definition Stuck: outcome := None.
+
+(* Asm semantic on Mach *)
+
+Section RELSEM.
+
+(** "oracle" stating the successive position (ie offset) of each block in the final assembly function *)
+Variable next: function -> Z -> Z.
+
+Inductive is_pos (f: function): Z -> code -> Prop :=
+  | First_pos: is_pos f 0 (fn_code f)
+  | Next_pos pos b c: is_pos f pos (b::c) -> is_pos f (next f pos) c.
+
+Fixpoint label_pos (f: function) (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
+  match c with
+  | nil => None
+  | b :: c' =>
+    if is_label lbl b then Some pos else label_pos f lbl (next f pos) c'
+  end.
+
+Definition goto_label (f: function) (lbl: label) (rs: regset) : option val :=
+  SOME pos <- label_pos f lbl 0 (fn_code f) IN
+  match rs#PC with
+  | Vptr b _ => Some (Vptr b (Ptrofs.repr pos))
+  | _        => None
+  end.
+
+Definition next_addr (f: function) (rs: regset): option val :=
+  match rs#PC with
+  | Vptr b ofs => Some (Vptr b (Ptrofs.repr (next f (Ptrofs.unsigned ofs))))
+  | _          => None
+  end.
+
+Variable ge:genv.
+
+Inductive basic_step (f: function) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop :=
+  | exec_MBgetstack:
+      forall ofs ty dst v,
+      load_stack m (rs#SP) ty ofs = Some v ->
+      basic_step f rs m (MBgetstack ofs ty dst) (rs#dst <- v) m
+  | exec_MBsetstack:
+      forall (src: mreg) ofs ty m' rs',
+      store_stack m (rs#SP) ty ofs (rs src) = Some m' ->
+      rs' = set_from_Machrs (undef_regs (destroyed_by_setstack ty) rs) rs ->
+      basic_step f rs m (MBsetstack src ofs ty) rs' m'
+  | exec_MBgetparam:
+      forall ofs ty (dst: mreg) v rs' psp,
+      load_stack m (rs#SP) Tptr f.(fn_link_ofs) = Some psp ->
+      load_stack m psp ty ofs = Some v ->
+      rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) ->
+      basic_step f rs m (MBgetparam ofs ty dst) rs' m
+  | exec_MBop:
+      forall op args v rs' (res: mreg),
+      eval_operation ge (rs#SP) op (to_Machrs rs)##args m = Some v ->
+      rs' = (set_from_Machrs (undef_regs (destroyed_by_op op) rs) rs)#res <- v ->
+      basic_step f rs m (MBop op args res) rs' m
+  | exec_MBload:
+      forall addr args a v rs' trap chunk (dst: mreg),
+      eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- v ->
+      basic_step f rs m (MBload trap chunk addr args dst) rs' m
+  | exec_MBload_notrap1:
+      forall addr args rs' chunk (dst: mreg),
+      eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = None ->
+      rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) ->
+      basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m
+  | exec_MBload_notrap2:
+      forall addr args a rs' chunk (dst: mreg),
+      eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
+      Mem.loadv chunk m a = None ->
+      rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) ->
+      basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m
+  | exec_MBstore:
+      forall chunk addr args (src: mreg) m' a rs',
+      eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
+      Mem.storev chunk m a (rs src) = Some m' ->
+      rs' = set_from_Machrs (undef_regs (destroyed_by_store chunk addr) rs) rs ->
+      basic_step f rs m (MBstore chunk addr args src) rs' m'
+  .
+
+
+Inductive body_step (f: function) : bblock_body -> regset -> mem -> regset -> mem -> Prop :=
+   | exec_nil_body rs m:
+       body_step f nil rs m rs m
+   | exec_cons_body rs m bi p rs' m' rs'' m'':
+       basic_step f rs m bi rs' m' ->
+       body_step f p rs' m' rs'' m'' ->
+       body_step f (bi::p) rs m rs'' m''
+   .
+
+
+Definition find_function_ptr (ros: mreg + ident) (rs: regset) : option val :=
+  match ros with
+  | inl r => Some (rs#r)
+  | inr symb =>
+      SOME b <- Genv.find_symbol ge symb IN
+      Some (Vptr b Ptrofs.zero)
+  end.
+
+Definition exec_epilogue (f: function) (rs: regset) (m: mem) : outcome :=
+   SOME sp <- load_stack m rs#SP Tptr f.(fn_link_ofs) IN
+   SOME ra <- load_stack m rs#SP Tptr f.(fn_retaddr_ofs) IN
+   match rs#SP with
+   | Vptr stk ofs =>
+     SOME m' <- Mem.free m stk 0 f.(fn_stacksize) IN
+     Next (rs#SP <- sp #RA <- ra) m'
+   | _ => Stuck
+   end.
+
+Inductive cfi_step (f: function): control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop :=
+  | exec_MBcall sig ros rs m pc:
+      find_function_ptr ros rs = Some pc ->
+      cfi_step f (MBcall sig ros) rs m E0 ((rs#RA <- (rs#PC))#PC <- pc) m
+  | exec_MBtailcall sig ros rs m rs' m' pc:
+      find_function_ptr ros rs = Some pc ->
+      exec_epilogue f rs m = Next rs' m' ->
+      cfi_step f (MBtailcall sig ros) rs m E0 (rs'#PC <- pc) m'
+  | exec_MBreturn rs m rs' m':
+      exec_epilogue f rs m = Next rs' m' ->
+      cfi_step f MBreturn rs m E0 (rs'#PC <- (rs'#RA)) m'
+  | exec_MBgoto lbl rs m pc:
+      goto_label f lbl rs = Some pc ->
+      cfi_step f (MBgoto lbl) rs m E0 (rs#PC <- pc) m
+  | exec_MBcond_true cond args lbl rs m pc rs':
+      eval_condition cond (to_Machrs rs)##args m = Some true ->
+      goto_label f lbl rs = Some pc ->
+      rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs ->
+      cfi_step f (MBcond cond args lbl) rs m E0 (rs'#PC <- pc) m
+  | exec_MBcond_false cond args lbl rs m rs':
+      eval_condition cond (to_Machrs rs)##args m = Some false ->
+      rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs ->
+      cfi_step f (MBcond cond args lbl) rs m E0 rs' m
+  | exec_MBjumptable arg tbl rs m index lbl pc rs':
+      to_Machrs rs arg = Vint index ->
+      list_nth_z tbl (Int.unsigned index) = Some lbl ->
+      goto_label f lbl rs = Some pc ->
+      rs' = set_from_Machrs (undef_regs destroyed_by_jumptable rs) rs ->
+      cfi_step f (MBjumptable arg tbl) rs m E0 (rs'#PC <- pc) m
+  | exec_MBbuiltin rs m ef args res vargs t vres rs' m':
+      eval_builtin_args ge (to_Machrs rs) (rs#SP) m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      rs' = set_from_Machrs (set_res res vres (undef_regs (destroyed_by_builtin ef) rs)) rs ->
+      cfi_step f (MBbuiltin ef args res) rs m t rs' m'
+  .
+
+Inductive exit_step f : option control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop :=
+  | exec_Some_exit ctl rs m t rs' m':
+      cfi_step f ctl rs m t rs' m' ->
+      exit_step f (Some ctl) rs m t rs' m'
+  | exec_None_exit rs m:
+      exit_step f None rs m E0 rs m
+  .
+
+Inductive exec_bblock f: bblock -> regset -> mem -> trace -> regset -> mem -> Prop :=
+  | exec_bblock_all (bb: bblock) rs0 m0 rs1 m1 pc t rs2 m2: 
+       body_step f (body bb) rs0 m0 rs1 m1 ->
+       next_addr f rs1 = Some pc ->
+       exit_step f (exit bb) (rs1#PC <- pc) m1 t rs2 m2 ->
+       exec_bblock f bb rs0 m0 t rs2 m2.
+
+Definition exec_prologue f (pos:Z) (rs: regset) (m:mem) : option state :=
+    if Z.eq_dec pos 0 then
+      let (m1, stk) := Mem.alloc m 0 f.(fn_stacksize) in
+      let sp := Vptr stk Ptrofs.zero in
+      SOME m2 <- store_stack m1 sp Tptr f.(fn_link_ofs) rs#SP IN
+      SOME m3 <- store_stack m2 sp Tptr f.(fn_retaddr_ofs) rs#RA IN
+      Next ((set_from_Machrs (undef_regs destroyed_at_function_entry rs) rs)#SP <- sp) m3
+    else
+      Next rs m.
+
+
+Inductive step: state -> trace -> state -> Prop :=
+  | exec_step_internal b ofs f bb c rs0 m0 rs1 m1 t rs2 m2:
+      rs0 PC = Vptr b ofs ->
+      Genv.find_funct_ptr ge b = Some (Internal f) ->
+      is_pos f (Ptrofs.unsigned ofs) (bb::c) ->
+      exec_prologue f (Ptrofs.unsigned ofs) rs0 m0 = Next rs1 m1 ->
+      exec_bblock f bb rs1 m1 t rs2 m2 ->
+      step (State rs0 m0) t (State rs2 m2)
+  | exec_step_external:
+      forall b ef args res rs m t rs' m',
+      rs PC = Vptr b Ptrofs.zero ->
+      Genv.find_funct_ptr ge b = Some (External ef) ->
+      extcall_arguments (to_Machrs rs) m (rs#SP) (ef_sig ef) args ->
+      external_call ef ge args m t res m' ->
+      rs' = (set_from_Machrs (set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs)) rs) #PC <- (rs RA) ->
+      step (State rs m) t (State rs' m').
+
+End RELSEM.
+
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall m0,
+      let ge := Genv.globalenv p in
+      Genv.init_mem p = Some m0 ->
+      let rs0 :=
+        (Pregmap.init Vundef)
+        # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
+        # SP <- Vnullptr
+        # RA <- Vnullptr in
+      initial_state p (State rs0 m0).
+
+Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall rs m r retcode,
+      loc_result signature_main = One r ->
+      rs PC = Vnullptr ->
+      rs r = Vint retcode ->
+      final_state (State rs m) retcode.
+
+Definition semantics (next: function -> Z -> Z) (p: program) :=
+  Semantics (step next) (initial_state p) final_state (Genv.globalenv p).
diff --git a/kvx/lib/PseudoAsmblockproof.v b/kvx/lib/PseudoAsmblockproof.v
new file mode 100644
index 00000000..3eb80ebb
--- /dev/null
+++ b/kvx/lib/PseudoAsmblockproof.v
@@ -0,0 +1,1173 @@
+Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep.
+Require Import Op Machregs Locations Stacklayout Conventions.
+Require Import Mach Machblock OptionMonad.
+Require Import Errors Datatypes PseudoAsmblock IterList.
+
+(** Tiny translation from Machblock semantics to PseudoAsmblock semantics (needs additional checks) 
+*)
+
+Section TRANSLATION.
+
+(* In the actual Asmblock code, the prologue will be inserted in the first block of the function.
+   But, this block should have an empty header.
+*)
+
+Definition has_header (c: code) : bool :=
+  match c with
+  | nil => false
+  | bb::_ => match header bb with
+             | nil => false
+             | _ => true
+             end
+  end.
+
+Definition insert_implicit_prologue c :=
+ if has_header c then {| header := nil; body := nil; exit := None |}::c else c.
+
+Definition transl_function (f: function) : function :=
+  {| fn_sig:=fn_sig f;
+     fn_code:=insert_implicit_prologue (fn_code f);
+     fn_stacksize := fn_stacksize f;
+     fn_link_ofs := fn_link_ofs f;
+     fn_retaddr_ofs := fn_retaddr_ofs f
+ |}.
+
+Definition transf_function (f: function) : res function :=
+  let tf := transl_function f in
+  (* removed because it is simpler or/and more efficient to perform this test in Asmblockgen !
+  if zlt Ptrofs.max_unsigned (max_pos tf)
+  then Error (msg "code size exceeded")
+  else *) 
+  OK tf.
+
+Definition transf_fundef (f: fundef) : res fundef :=
+  transf_partial_fundef transf_function f.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
+
+End TRANSLATION.
+
+(** Proof of the translation
+*)
+
+Require Import Linking.
+
+Section PRESERVATION.
+
+Definition match_prog (p: program) (tp: program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. eapply match_transform_partial_program; eauto.
+Qed.
+
+Local Open Scope Z_scope.
+Local Open Scope asm.
+Local Open Scope option_monad_scope.
+
+Variable prog: program.
+Variable tprog: program.
+
+Hypothesis TRANSF: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Variable next: function -> Z -> Z.
+
+Hypothesis next_progress: forall (f:function) (pos:Z), (pos < (next f pos))%Z.
+
+Definition max_pos (f:function) := iter (S (length f.(fn_code))) (next f) 0.
+
+(* This hypothesis expresses that Asmgen checks for each tf 
+   that (max_pos tf) represents a valid address
+*)
+Hypothesis functions_bound_max_pos: forall fb tf,
+  Genv.find_funct_ptr tge fb = Some (Internal tf) ->
+  (max_pos tf) <= Ptrofs.max_unsigned.
+
+(** * Agreement between Mach registers and PseudoAsm registers *)
+Record agree (ms: Mach.regset) (sp: val) (rs: regset) : Prop := mkagree {
+  agree_sp: rs#SP = sp;
+  agree_sp_def: sp <> Vundef;
+  agree_mregs: forall r: mreg, (ms r)=(rs#r)
+}.
+
+(** [transl_code_at_pc pc fb f tf c] holds if the code pointer [pc] points
+  within the code generated by Machblock function (originally [f] -- but translated as [tf]),
+  and [c] is the tail of the code at the position corresponding to the code pointer [pc].
+*)
+Inductive transl_code_at_pc (b:block) (f:function) (tf:function) (c:code): val -> Prop :=
+  transl_code_at_pc_intro ofs:
+    Genv.find_funct_ptr ge b = Some (Internal f) ->
+    transf_function f = OK tf ->
+    (* we have passed the first block containing the prologue *)
+    (0 < (Ptrofs.unsigned ofs))%Z -> 
+    (* the code is identical in the two functions *)
+    is_pos next tf (Ptrofs.unsigned ofs) c ->
+    transl_code_at_pc b f tf c (Vptr b ofs).
+
+Inductive match_stack: list stackframe -> Prop :=
+  | match_stack_nil:
+      match_stack nil
+  | match_stack_cons: forall fb sp ra c s f tf,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      transl_code_at_pc fb f tf c ra ->
+      sp <> Vundef ->
+      match_stack s ->
+      match_stack (Stackframe fb sp ra c :: s).
+
+(** Semantic preservation is proved using simulation diagrams
+  of the following form.
+<<
+           s1 ---------------- s2
+            |                   |
+           t|                  *|t
+            |                   |
+            v                   v
+           s1'---------------- s2'
+>>
+  The invariant is the [match_states] predicate below...
+
+*)
+
+Inductive match_states: Machblock.state -> state -> Prop :=
+  | match_states_internal s fb sp c ms m rs f tf
+        (STACKS: match_stack s)
+        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
+        (AT: transl_code_at_pc fb f tf c (rs PC))
+        (AG: agree ms sp rs):
+      match_states (Machblock.State s fb sp c ms m)
+                   (State rs m)
+  | match_states_prologue s sp fb ms rs0 m0 f rs1 m1 
+        (STACKS: match_stack s)
+        (AG: agree ms sp rs1)
+        (ATPC: rs0 PC = Vptr fb Ptrofs.zero)
+        (ATLR: rs0 RA = parent_ra s)
+        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
+        (PROL: exec_prologue f 0 rs0 m0 = Next rs1 m1):
+      match_states (Machblock.State s fb sp (fn_code f) ms m1)
+                   (State rs0 m0)
+  | match_states_call s fb ms m rs
+        (STACKS: match_stack s)
+        (AG: agree ms (parent_sp s) rs)
+        (ATPC: rs PC = Vptr fb Ptrofs.zero)
+        (ATLR: rs RA = parent_ra s):
+      match_states (Machblock.Callstate s fb ms m)
+                   (State rs m)
+  | match_states_return s ms m rs
+        (STACKS: match_stack s)
+        (AG: agree ms (parent_sp s) rs)
+        (ATPC: rs PC = parent_ra s):
+      match_states (Machblock.Returnstate s ms m)
+                   (State rs m).
+
+Definition measure (s: Machblock.state) : nat :=
+  match s with
+  | Machblock.State _ _ _ _ _ _ => 0%nat
+  | Machblock.Callstate _ _ _ _ => 1%nat
+  | Machblock.Returnstate _ _ _ => 1%nat
+  end.
+
+Definition rao (f: function) (c: code) (ofs: ptrofs) : Prop :=
+  forall tf,
+  transf_function f = OK tf ->
+  is_pos next tf (Ptrofs.unsigned ofs) c.
+
+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 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 = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+
+Lemma functions_transl fb f tf:
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  transf_function f = OK tf ->
+  Genv.find_funct_ptr tge fb = Some (Internal tf).
+Proof.
+  intros. exploit functions_translated; eauto. intros [tf' [A B]].
+  monadInv B. inv H0; auto.
+Qed.
+
+Lemma function_bound fb f tf:
+  Genv.find_funct_ptr ge fb = Some (Internal f) -> transf_function f = OK tf -> (max_pos tf) <= Ptrofs.max_unsigned.
+Proof.
+  intros; eapply functions_bound_max_pos; eauto.
+  eapply functions_transl; eauto.
+Qed.
+
+Lemma transf_function_def f tf:
+  transf_function f = OK tf -> tf.(fn_code) = insert_implicit_prologue f.(fn_code).
+Proof.
+  unfold transf_function.
+  intros EQ; inv EQ.
+  auto.
+Qed.
+
+Lemma stackinfo_preserved f tf:
+  transf_function f = OK tf ->
+  tf.(fn_stacksize) = f.(fn_stacksize) 
+  /\ tf.(fn_retaddr_ofs) = f.(fn_retaddr_ofs)
+   /\ tf.(fn_link_ofs) = f.(fn_link_ofs).
+Proof.
+  unfold transf_function.
+  intros EQ0; inv EQ0. simpl; intuition.
+Qed.
+
+Lemma transf_initial_states st1: Machblock.initial_state prog st1 ->
+  exists st2, initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intro H. inversion H. unfold ge0 in *.
+  econstructor; split.
+  - econstructor.
+    eapply (Genv.init_mem_transf_partial TRANSF); eauto.
+  - replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero)
+     with (Vptr fb Ptrofs.zero).
+    + econstructor; eauto.
+      * constructor.
+      * split; auto; simpl; unfold Vnullptr; destruct Archi.ptr64; congruence.
+    + unfold Genv.symbol_address.
+      rewrite (match_program_main TRANSF).
+      rewrite symbols_preserved.
+      unfold ge. simplify_someHyp. auto.
+Qed.
+
+Lemma transf_final_states st1 st2 r:
+  match_states st1 st2 -> Machblock.final_state st1 r -> final_state st2 r.
+Proof.
+  intros H H0. inv H0. inv H.
+  econstructor; eauto.
+  exploit agree_mregs; eauto.
+  erewrite H2. intro H3; inversion H3.
+  auto.
+Qed.
+
+(** Lemma on [is_pos]. *)
+
+Lemma is_pos_alt_def f pos code: is_pos next f pos code -> 
+  exists n, (n <= List.length (fn_code f))%nat /\ pos = (iter n (next f) 0) /\ code = iter_tail n (fn_code f).
+Proof.
+  induction 1.
+  - unfold iter_tail; exists O; simpl; intuition.
+  - destruct IHis_pos as (n & H0 & H1 & H2).
+    exists (S n). repeat split.
+    + rewrite (length_iter_tail n); eauto.
+      rewrite <- H2; simpl; omega.
+    + rewrite iter_S; congruence.
+    + unfold iter_tail in *; rewrite iter_S, <- H2; auto.
+Qed.
+
+Local Hint Resolve First_pos Next_pos: core.
+
+Lemma is_pos_alt_def_recip f n: (n <= List.length (fn_code f))%nat ->
+  is_pos next f (iter n (next f) 0) (iter_tail n (fn_code f)).
+Proof.
+  induction n.
+  - unfold iter_tail; simpl; eauto.
+  - intros H; destruct (iter_tail_S_ex n (fn_code f)) as (x & H1); try omega.
+    rewrite iter_S; lapply IHn; try omega.
+    rewrite H1; eauto.
+Qed.
+
+Lemma is_pos_inject1 f pos1 pos2 code:
+  is_pos next f pos1 code -> is_pos next f pos2 code -> pos1=pos2.
+Proof.
+  intros H1 H2.
+  destruct (is_pos_alt_def f pos1 code) as (n1 & B1 & POS1 & CODE1); eauto.
+  destruct (is_pos_alt_def f pos2 code) as (n2 & B2 & POS2 & CODE2); eauto.
+  clear H1 H2; subst.
+  erewrite (iter_tail_inject1 n1 n2); eauto.
+Qed.
+
+Lemma iter_next_strict_monotonic f n m x: (n < m)%nat -> iter n (next f) x < iter m (next f) x.
+Proof.
+  induction 1; rewrite iter_S; auto.
+  generalize (next_progress f (iter m (next f) x)).
+  omega.
+Qed.
+
+Lemma iter_next_monotonic f n m x: (n <= m)%nat -> iter n (next f) x <= iter m (next f) x.
+Proof.
+  destruct 1.
+  - omega.
+  - generalize (iter_next_strict_monotonic f n (S m) x). omega.
+Qed.
+
+Lemma is_pos_bound_pos f pos code:
+  is_pos next f pos code -> 0 <= pos <= max_pos f.
+Proof.
+  intros H; exploit is_pos_alt_def; eauto.
+  intros (n & H1 & H2 & H3).
+  rewrite H2. unfold max_pos. split.
+  - cutrewrite (0 = iter O (next f) 0); auto.
+    apply iter_next_monotonic; omega.
+  - apply iter_next_monotonic; omega.
+Qed.
+
+Lemma is_pos_unsigned_repr f pos code:
+  is_pos next f pos code -> 
+  max_pos f <= Ptrofs.max_unsigned ->
+  Ptrofs.unsigned (Ptrofs.repr pos) = pos.
+Proof.
+  intros; eapply Ptrofs.unsigned_repr.
+  exploit is_pos_bound_pos; eauto.
+  omega.
+Qed.
+
+Lemma is_pos_simplify f pos code:
+  is_pos next f pos code -> 
+  max_pos f <= Ptrofs.max_unsigned ->
+  is_pos next f (Ptrofs.unsigned (Ptrofs.repr pos)) code.
+Proof.
+  intros; erewrite is_pos_unsigned_repr; eauto.
+Qed.
+
+Lemma find_label_label_pos f lbl c: forall pos c',
+  find_label lbl c = Some c' ->
+  exists n,
+  label_pos next f lbl pos c = Some (iter n (next f) pos)
+  /\ c' = iter_tail n c
+  /\ (n <= List.length c)%nat.
+Proof.
+  induction c.
+  - simpl; intros. discriminate.
+  - simpl; intros pos c'.
+    destruct (is_label lbl a).
+    + intro EQ; injection EQ; intro; subst c'.
+      exists O; simpl; intuition.
+    + intros. generalize (IHc (next f pos) c' H). intros (n' & A & B & C).
+       exists (S n'). intuition.
+Qed.
+
+Lemma find_label_insert_implicit_prologue lbl c:
+  find_label lbl c = find_label lbl (insert_implicit_prologue c).
+Proof.
+  unfold insert_implicit_prologue.
+  destruct (has_header c); simpl; auto.
+  unfold is_label; simpl.
+  destruct (in_dec lbl nil); auto.
+  simpl in *. tauto.
+Qed.
+
+Lemma no_header_insert_implicit_prologue c:
+  has_header (insert_implicit_prologue c) = false.
+Proof.
+  unfold insert_implicit_prologue.
+  destruct (has_header c) eqn: H; simpl; auto.
+Qed.
+
+Lemma find_label_has_header lbl c c':
+  find_label lbl c = Some c' -> 
+  has_header c' = true.
+Proof.
+  induction c; simpl; try congruence.
+  destruct (is_label lbl a) eqn:LAB; auto.
+  intros X; inv X; simpl.
+  unfold is_label in LAB.
+  destruct (in_dec lbl (header a)); try congruence.
+  destruct (header a); try congruence.
+  simpl in *; tauto.
+Qed.
+
+Lemma find_label_label_pos_no_header f lbl c pos c':
+  (has_header c) = false ->
+  find_label lbl c = Some c' ->
+  exists n,
+  label_pos next f lbl pos c = Some (iter (S n) (next f) pos)
+  /\ c' = iter_tail (S n) c
+  /\ ((S n) <= List.length c)%nat.
+Proof.
+  intros H H0; exploit find_label_label_pos; eauto.
+  intros ([|n] & H1 & H2 & H3); try (exists n; intuition eauto).
+  unfold iter_tail in *; simpl in *; subst.
+  erewrite find_label_has_header in H; eauto.
+  congruence.
+Qed.
+
+Hint Resolve is_pos_simplify is_pos_alt_def_recip function_bound: core.
+
+Lemma find_label_goto_label f tf lbl rs c' b ofs:
+  Genv.find_funct_ptr ge b = Some (Internal f) ->
+  transf_function f = OK tf ->
+  Vptr b ofs = rs PC ->
+  find_label lbl f.(fn_code) = Some c' ->
+  exists pc,
+     goto_label next tf lbl rs = Some pc
+  /\ transl_code_at_pc b f tf c' pc.
+Proof.
+  intros FINDF T HPC FINDL.
+  erewrite find_label_insert_implicit_prologue, <- transf_function_def in FINDL; eauto.
+  exploit find_label_label_pos_no_header; eauto.
+  { erewrite transf_function_def; eauto.
+    apply no_header_insert_implicit_prologue.
+  }
+  intros (n & LAB & CODE & BOUND); subst.
+  exists (Vptr b (Ptrofs.repr (iter (S n) (next tf) 0))).
+  unfold goto_label; intuition.
+  - simplify_someHyps; rewrite <- HPC. auto.
+  - econstructor; eauto.
+    erewrite is_pos_unsigned_repr; eauto.
+    generalize (iter_next_strict_monotonic tf O (S n) 0); simpl.
+    omega.
+Qed.
+
+(** Preservation of register agreement under various assignments. *)
+
+Lemma agree_mregs_list ms sp rs:
+  agree ms sp rs ->
+  forall l, (ms##l)=(to_Machrs rs)##l.
+Proof.
+  unfold to_Machrs. intros AG; induction l; simpl; eauto.
+  erewrite agree_mregs; eauto.
+  congruence.
+Qed.
+
+Lemma agree_set_mreg ms sp rs r v rs':
+  agree ms sp rs ->
+  v=(rs'#(preg_of r)) ->
+  (forall r', r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Regmap.set r v ms) sp rs'.
+Proof.
+  intros H H0 H1. destruct H. split; auto.
+  - rewrite H1; auto. destruct r; simpl; congruence.
+  - intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence.
+    rewrite H1; auto. destruct r; simpl; congruence.
+Qed.
+
+Corollary agree_set_mreg_parallel:
+  forall ms sp rs r v,
+  agree ms sp rs ->
+  agree (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.
+
+Corollary agree_set_mreg_parallel2:
+  forall ms sp rs r v ms',
+  agree ms sp (set_from_Machrs ms' rs)->
+  agree (Regmap.set r v ms) sp (set_from_Machrs (Regmap.set r v ms') rs).
+Proof.
+  intros. unfold set_from_Machrs in *. eapply agree_set_mreg; eauto.
+  - rewrite Regmap.gss; auto. 
+  - intros r' X. destruct r'; try congruence. rewrite Regmap.gso; try congruence.
+Qed.
+
+Definition data_preg (r: preg) : bool :=
+  match r with
+  | preg_of _ | SP => true
+  | _ => false
+  end.
+
+Lemma agree_exten ms sp rs rs':
+  agree ms sp rs ->
+  (forall r, data_preg r = true -> rs'#r = rs#r) ->
+  agree ms sp rs'.
+Proof.
+  intros H H0. destruct H. split; intros; try rewrite H0; auto.
+Qed.
+
+Lemma agree_set_from_Machrs ms sp ms' rs:
+  agree ms sp rs ->
+  (forall (r:mreg), (ms' r) = rs#r) ->
+  agree ms sp (set_from_Machrs ms' rs).
+Proof.
+  unfold set_from_Machrs; intros.
+  eapply agree_exten; eauto.
+  intros r; destruct r; simpl; try congruence.
+Qed.
+
+Lemma agree_set_other 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_next_addr f ms sp b pos rs:
+  agree ms sp rs ->
+  agree ms sp (rs#PC <- (Vptr b (Ptrofs.repr (next f pos)))).
+Proof.
+  intros. apply agree_set_other; auto.
+Qed.
+
+Local Hint Resolve agree_set_mreg_parallel2: core.
+
+Lemma agree_set_pair sp p v ms ms' rs:
+  agree ms sp (set_from_Machrs ms' rs) ->
+  agree (set_pair p v ms) sp (set_from_Machrs (set_pair p v ms') rs).
+Proof.
+  intros H; destruct p; simpl; auto.
+Qed.
+
+Lemma agree_undef_caller_save_regs:
+  forall ms sp ms' rs,
+  agree ms sp (set_from_Machrs ms' rs) ->
+  agree (undef_caller_save_regs ms) sp (set_from_Machrs (undef_caller_save_regs ms') rs).
+Proof.
+  intros. destruct H as [H0 H1 H2]. unfold undef_caller_save_regs. split; auto.
+  intros.
+  unfold set_from_Machrs in * |- *.
+  rewrite H2. auto.
+Qed.
+
+Lemma agree_change_sp ms sp rs sp':
+  agree ms sp rs -> sp' <> Vundef ->
+  agree ms sp' (rs#SP <- sp').
+Proof.
+  intros H H0. inv H. split; auto.
+Qed.
+
+Lemma agree_undef_regs ms sp rl ms' rs:
+  agree ms sp (set_from_Machrs ms' rs) ->
+  agree (Mach.undef_regs rl ms) sp (set_from_Machrs (Mach.undef_regs rl ms') rs).
+Proof.
+  unfold set_from_Machrs; intros H. destruct H; subst. split; auto.
+  intros. destruct (In_dec mreg_eq r rl).
+  + rewrite! undef_regs_same; auto.
+  + rewrite! undef_regs_other; auto.
+Qed.
+
+(** Translation of arguments and results to builtins. *)
+
+Remark builtin_arg_match:
+  forall ms rs sp m a v,
+  agree ms sp rs ->
+  eval_builtin_arg ge ms sp m a v ->
+  eval_builtin_arg ge (to_Machrs rs) sp m a v.
+Proof.
+  induction 2; simpl; eauto with barg.
+  unfold to_Machrs; erewrite agree_mregs; eauto.
+  econstructor.
+Qed.
+
+Lemma builtin_args_match: 
+  forall ms sp rs m,
+  agree ms sp rs ->
+  forall al vl, eval_builtin_args ge ms sp m al vl ->
+  eval_builtin_args ge (to_Machrs rs) sp m al vl.
+Proof.
+  induction 2; intros; simpl; try (constructor; auto).
+  eapply eval_builtin_arg_preserved; eauto.
+  eapply builtin_arg_match; eauto.
+Qed.
+
+Lemma agree_set_res res: forall ms sp rs v ms',
+  agree ms sp (set_from_Machrs ms' rs) ->
+  agree (set_res res v ms) sp (set_from_Machrs (set_res res v ms') rs).
+Proof.
+  induction res; simpl; auto.
+Qed.
+
+Lemma find_function_ptr_agree ros ms rs sp b: 
+  agree ms sp rs ->
+  Machblock.find_function_ptr ge ros ms = Some b ->
+  find_function_ptr tge ros rs = Some (Vptr b Ptrofs.zero).
+Proof.
+  intros AG; unfold Mach.find_function_ptr; destruct ros as [r|s]; simpl; auto.
+  - generalize (agree_mregs _ _ _ AG r). destruct (ms r); simpl; try congruence.
+    intros H; inv H; try congruence.
+    inversion_ASSERT. intros H; rewrite (Ptrofs.same_if_eq _ _ H); eauto.
+    try_simplify_someHyps.
+  - intros H; rewrite symbols_preserved, H. auto.
+Qed.
+
+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 extcall_arg_match ms sp rs m l v:
+  agree ms sp rs ->
+  extcall_arg ms m sp l v ->
+  extcall_arg rs m (rs#SP) l v.
+Proof.
+  destruct 2.
+  - erewrite agree_mregs; eauto. constructor.
+  - unfold load_stack in *. econstructor; eauto.
+    erewrite agree_sp; eauto.
+Qed.
+
+Local Hint Resolve extcall_arg_match: core.
+
+Lemma extcall_arg_pair_match:
+  forall ms sp rs m p v,
+  agree ms sp rs ->
+  extcall_arg_pair ms m sp p v ->
+  extcall_arg_pair rs m (rs#SP) p v.
+Proof.
+  destruct 2; constructor; eauto.
+Qed.
+
+Local Hint Resolve extcall_arg_pair_match: core.
+
+Lemma extcall_args_match:
+  forall ms sp rs m, agree ms sp rs ->
+  forall ll vl,
+  list_forall2 (extcall_arg_pair ms m sp) ll vl ->
+  list_forall2 (extcall_arg_pair rs m rs#SP) ll vl.
+Proof.
+  induction 2; constructor; eauto.
+Qed.
+
+Lemma extcall_arguments_match:
+  forall ms m sp rs sg args,
+  agree ms sp rs ->
+  extcall_arguments ms m sp sg args ->
+  extcall_arguments rs m (rs#SP) sg args.
+Proof.
+  unfold extcall_arguments, extcall_arguments; intros.
+  eapply extcall_args_match; eauto.
+Qed.
+
+(** A few tactics *)
+
+Local Hint Resolve functions_transl symbols_preserved
+  agree_next_addr agree_mregs agree_set_mreg_parallel agree_undef_regs agree_set_other agree_change_sp
+  agree_sp_def agree_set_from_Machrs agree_set_pair agree_undef_caller_save_regs agree_set_res f_equal Ptrofs.repr_unsigned parent_sp_def
+  builtin_args_match external_call_symbols_preserved: core.
+
+Ltac simplify_regmap :=
+  repeat (rewrite ?Pregmap.gss; try (rewrite Pregmap.gso; try congruence)).
+
+Ltac simplify_next_addr :=
+  match goal with
+  | [ HPC: Vptr _ _ = _ PC |- _ ] => try (unfold next_addr, Val.offset_ptr); simplify_regmap; try (rewrite <- HPC)
+  end.
+
+Ltac discharge_match_states :=
+   econstructor; eauto; try ( simplify_next_addr; econstructor; eauto ).
+
+
+(** Instruction step simulation lemma: the simulation lemma for stepping one instruction 
+
+<<
+           s1 ---------------- s2
+            |                   |
+           t|                  +|t
+            |                   |
+            v                   v
+           s1'---------------- s2'
+>>
+
+*)
+
+Lemma trivial_exec_prologue:
+  forall tf ofs rs m,
+  0 < Ptrofs.unsigned ofs ->
+  exec_prologue tf (Ptrofs.unsigned ofs) rs m = Next rs m.
+Proof.
+  unfold exec_prologue. intros.
+  destruct (Z.eq_dec); eauto. omega.
+Qed.
+
+Lemma basic_step_simulation: forall ms sp rs s f tf fb ms' bi m m',
+  agree ms sp rs ->
+  match_stack s ->
+  transf_function f = OK tf ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  Machblock.basic_step ge s fb sp ms m bi ms' m' ->
+  exists rs', basic_step tge tf rs m bi rs' m' /\ agree ms' sp rs' /\ rs' PC = rs PC.
+Proof.
+  destruct 5.
+  (* MBgetstack *)
+  - eexists; split.
+    + econstructor; eauto. erewrite agree_sp; eauto.
+    + eauto.
+  (* MBsetstack *)
+  - eexists; split.
+    + econstructor; eauto.
+      erewrite agree_sp; eauto.
+      erewrite <- agree_mregs; eauto.
+    + rewrite H4; split; eauto.
+  (* MBgetparam *)
+  - eexists; split.
+    + econstructor; eauto.
+      erewrite agree_sp; eauto.
+      assert (f = f0). { rewrite H2 in H3. inversion H3. reflexivity. }
+      assert (fn_link_ofs tf = fn_link_ofs f0). {
+        rewrite <- H7.
+        eapply stackinfo_preserved. eauto.
+      }
+      rewrite H8. eauto.
+    + rewrite H6; split; eauto.
+  (* MBop *)
+  - eexists; split.
+    + econstructor; eauto.
+      erewrite agree_sp; eauto.
+      erewrite agree_mregs_list in H3.
+      * erewrite <- H3.
+        eapply eval_operation_preserved; trivial.
+      * eauto.
+    + rewrite H4; split; eauto.
+  (* MBload *)
+  - eexists; split.
+    + econstructor; eauto.
+      erewrite agree_sp; eauto. erewrite <- agree_mregs_list; eauto.
+      erewrite <- H3.
+      eapply eval_addressing_preserved; trivial.
+    + rewrite H5; split; eauto.
+  (* MBload notrap1 *)
+  - eexists; split.
+    + eapply exec_MBload_notrap1; eauto.
+      erewrite agree_sp; eauto.
+      erewrite agree_mregs_list in H3; eauto.
+      * erewrite eval_addressing_preserved; eauto.
+    + rewrite H4; eauto.
+  (* MBload notrap2 *)
+  - eexists; split.
+    + eapply exec_MBload_notrap2; eauto.
+      erewrite agree_sp; eauto.
+      erewrite agree_mregs_list in H3; eauto.
+      * erewrite eval_addressing_preserved; eauto.
+    + rewrite H5; eauto.
+  (* MBstore *)
+  - eexists; split.
+    + econstructor; eauto.
+      * erewrite agree_sp; eauto.
+        erewrite agree_mregs_list in H3.
+        erewrite eval_addressing_preserved; eauto.
+        eauto.
+      * erewrite <- agree_mregs; eauto.
+    + rewrite H5; eauto.
+Qed.
+
+Lemma body_step_simulation: forall ms sp s f tf fb ms' bb m m',
+  match_stack s ->
+  transf_function f = OK tf ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  Machblock.body_step ge s fb sp bb ms m ms' m' ->
+  forall rs, agree ms sp rs ->
+  exists rs', body_step tge tf bb rs m rs' m' /\ agree ms' sp rs' /\ rs' PC = rs PC.
+Proof.
+  induction 4.
+  - repeat (econstructor; eauto).
+  - intros. exploit basic_step_simulation; eauto.
+    intros (rs'0 & BASIC & AG1' & AGPC1).
+    exploit IHbody_step; eauto.
+    intros (rs'1 & BODY & AG2' & AGPC2).
+    repeat (econstructor; eauto).
+    congruence.
+Qed.
+
+Local Hint Resolve trivial_exec_prologue: core.
+
+Lemma exit_step_simulation s fb f sp c t bb ms m s1' tf rs pc
+  (STEP: Machblock.exit_step rao ge (exit bb) (Machblock.State s fb sp (bb :: c) ms m) t s1')
+  (STACKS: match_stack s)
+  (AG: agree ms sp rs)
+  (NXT: next_addr next tf rs = Some pc)
+  (AT: transl_code_at_pc fb f tf c pc):
+  exists rs' m', exit_step next tge tf (exit bb) (rs#PC <- pc) m t rs' m' /\ match_states s1' (State rs' m').
+Proof.
+  inv AT.
+  inv STEP.
+  (* cfi_step currently only defined for exec_MBcall, exec_MBreturn, and exec_MBgoto *)
+  - inversion H4; subst. clear H4. (* inversion_clear H4 does not work so well: it clears an important hypothesis about "sp" in the Mreturn case *)
+    (* MBcall *)
+    + eexists. eexists. split.
+      * apply exec_Some_exit.
+        apply exec_MBcall.
+        eapply find_function_ptr_agree; eauto.
+      * assert (f0 = f). { congruence. } subst.
+        assert (Ptrofs.unsigned ra = Ptrofs.unsigned ofs). {
+          eapply is_pos_inject1; eauto.
+        }
+        assert (ofs = ra). {
+          apply Ptrofs.same_if_eq. unfold Ptrofs.eq.
+          rewrite H4. rewrite zeq_true. reflexivity.
+        }
+        repeat econstructor; eauto.
+        -- unfold rao in *. congruence.
+        -- simpl. simplify_regmap.
+           erewrite agree_sp; eauto.
+        -- simpl. simplify_regmap. auto.
+    (* MBtailcall *)
+    + assert (f0 = f). { congruence. } subst.
+      eexists. eexists. split.
+      * repeat econstructor.
+        -- eapply find_function_ptr_agree; eauto.
+        -- unfold exec_epilogue. erewrite agree_sp; eauto.
+           apply stackinfo_preserved in H0 as ( SS & RA & LO ).
+           rewrite SS, RA, LO.
+           try_simplify_someHyps.
+      * repeat econstructor; eauto.
+        intros r.
+        eapply agree_mregs; eapply agree_set_other; eauto.
+    (* MBbuiltin *)
+    +eexists. eexists. split.
+      * repeat econstructor.
+        -- simplify_regmap. erewrite agree_sp; eauto.
+           eapply eval_builtin_args_preserved; eauto.
+        -- eapply external_call_symbols_preserved; eauto.
+           exact senv_preserved.
+      * repeat econstructor; eauto.
+        -- assert (transl_function f = tf). {
+             unfold transf_function in *. congruence.
+           }
+           erewrite H5. assumption.
+        -- eapply agree_sp. eapply agree_set_res. eapply agree_undef_regs.
+           eapply agree_set_from_Machrs; eauto.
+        -- intros; simpl.
+           eapply agree_set_res. eapply agree_undef_regs.
+           eapply agree_set_from_Machrs; eauto.
+    (* MBgoto *)
+    + simplify_someHyps. intros.
+      assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). {
+        rewrite Pregmap.gss. reflexivity.
+      }
+      eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc
+               /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). {
+        eapply find_label_goto_label; eauto.
+      }
+      eexists. eexists. split.
+      * apply exec_Some_exit.
+        apply exec_MBgoto.
+        rewrite GOTO_LABEL. trivial.
+      * repeat econstructor; eauto.
+        -- simplify_regmap.
+           exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL).
+           assert(pc' = pc). { congruence. } subst. eauto.
+        -- simplify_regmap. erewrite agree_sp; eauto.
+    (* MBcond true *)
+    (* Mostly copy and paste from MBgoto *)
+    + simplify_someHyps. intros.
+      assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). {
+        rewrite Pregmap.gss. reflexivity.
+      }
+      eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc
+               /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). {
+        eapply find_label_goto_label; eauto.
+      }
+      eexists. eexists. split.
+      * apply exec_Some_exit. eapply exec_MBcond_true; eauto.
+        erewrite agree_mregs_list in H14; eauto.
+      * repeat econstructor; eauto.
+        -- simplify_regmap.
+           exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL).
+           assert(pc' = pc). { congruence. } subst. eauto.
+        -- simplify_regmap. erewrite agree_sp; eauto.
+    (* MBcond false *)
+    + inv H0. eexists. eexists. split. 
+      * apply exec_Some_exit. apply exec_MBcond_false.
+        -- erewrite agree_mregs_list in H15; eauto.
+        -- trivial.
+      * repeat econstructor; eauto. erewrite agree_sp; eauto.
+    (* MBjumptable *)
+    + simplify_someHyps. intros.
+      assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). {
+        rewrite Pregmap.gss. reflexivity.
+      }
+      eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc
+               /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). {
+        eapply find_label_goto_label; eauto.
+      }
+      eexists. eexists. split.
+      * repeat econstructor; eauto.
+        rewrite <- H14.
+        symmetry. eapply agree_mregs. eapply agree_set_other; eauto.
+      * repeat econstructor; eauto.
+        (* copy paste from MBgoto *)
+        --  simplify_regmap.
+            exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL).
+            assert(pc' = pc). { congruence. } subst. eauto.
+        -- simplify_regmap. erewrite agree_sp; eauto.
+        -- intros; simplify_regmap. eauto.
+    + (* MBreturn *)
+      try_simplify_someHyps.
+      eexists. eexists. split.
+      * apply exec_Some_exit.
+        apply exec_MBreturn.
+        unfold exec_epilogue.
+        erewrite agree_sp; eauto.
+        apply stackinfo_preserved in H0 as ( SS & RA & LO ).
+        rewrite SS, RA, LO.
+        try_simplify_someHyps.
+      * repeat econstructor; eauto. intros r.
+        simplify_regmap. eapply agree_mregs; eauto.
+  - inv H0; repeat econstructor; eauto.
+    erewrite agree_sp; eauto.
+Qed.
+
+Lemma inst_step_simulation s fb f sp c t ms m s1' tf rs
+  (STEP: Machblock.step rao ge (Machblock.State s fb sp c ms m) t s1')
+  (STACKS: match_stack s)
+  (AT: transl_code_at_pc fb f tf c (rs PC))
+  (AG: agree ms sp rs):
+  exists s2' : state, plus (step next) tge (State rs m) t s2' /\ match_states s1' s2'.
+Proof.
+  inv STEP.
+  inv AT.
+  exploit body_step_simulation; eauto. intros (rs0' & BODY & AG0 & AGPC).
+  assert (NXT: next_addr next tf rs0' = Some (Vptr fb (Ptrofs.repr (next tf (Ptrofs.unsigned ofs))))).
+  { unfold next_addr; rewrite AGPC, <- H; simpl; eauto. }
+  exploit exit_step_simulation; eauto.
+  { econstructor; eauto.
+    erewrite is_pos_unsigned_repr; eauto.
+    generalize (next_progress tf (Ptrofs.unsigned ofs)); omega. }
+  intros (rs2 & m2 & STEP & MS).
+  eexists.
+  split; eauto.
+  eapply plus_one.
+  eapply exec_step_internal; eauto.
+  econstructor; eauto.
+Qed.
+
+Lemma prologue_preserves_pc: forall f rs0 m0 rs1 m1,
+  exec_prologue f 0 rs0 m0 = Next rs1 m1 ->
+  rs1 PC = rs0 PC.
+Proof.
+  unfold exec_prologue; simpl;
+  intros f rs0 m0 rs1 m1 H.
+  destruct (Mem.alloc m0 0 (fn_stacksize f)) in H; unfold Next in H.
+  simplify_someHyps; inversion_SOME ignored; inversion_SOME ignored';
+  intros ? ? H'; inversion H'; trivial.
+Qed.
+
+Lemma is_pos_next_zero bb c fb f
+  (FIND : Genv.find_funct_ptr ge fb = Some (Internal f))
+  (FN_HEAD : bb :: c = fn_code f):
+  is_pos next (transl_function f) (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)) (if has_header (fn_code f) then bb::c else c).
+Proof.
+  exploit (transf_function_def f). unfold transf_function; auto.
+  unfold insert_implicit_prologue.
+  intros fn_code_tf; destruct (has_header (fn_code f));
+  eapply Next_pos; rewrite Ptrofs.unsigned_zero;
+  rewrite FN_HEAD; rewrite <- fn_code_tf; apply First_pos.
+Qed.
+
+Lemma prologue_simulation_no_header_step t s1' s sp fb ms f m1 rs0 m0 rs1
+  (STACKS : match_stack s)
+  (AG : agree ms sp rs1)
+  (ATPC : rs0 PC = Vptr fb Ptrofs.zero)
+  (ATLR : rs0 RA = parent_ra s)
+  (FIND : Genv.find_funct_ptr ge fb = Some (Internal f))
+  (PROL : exec_prologue f 0 rs0 m0 = Next rs1 m1)
+  (STEP : Machblock.step rao ge (Machblock.State s fb sp (fn_code f) ms m1) t s1')
+  (NO_HEADER: has_header (fn_code f) = false):
+  exists s2' : state, step next tge {| _rs := rs0; _m := m0 |} t s2' /\ match_states s1' s2'.
+Proof.
+  inv STEP.
+
+  exploit functions_translated; eauto;
+  intros (tf & FINDtf & TRANSf); monadInv TRANSf.
+  assert (fn_code f = fn_code (transl_function f)) as TF_CODE. {
+    unfold transl_function; simpl; unfold insert_implicit_prologue;
+    rewrite NO_HEADER; trivial.
+  }
+
+  exploit body_step_simulation; eauto; unfold transf_function; auto.
+  intros (rs0' & BODY & AG0 & AGPC).
+
+  exploit prologue_preserves_pc; eauto.
+  intros AGPC'.
+
+  exploit is_pos_next_zero; eauto; rewrite NO_HEADER.
+  intros IS_POS.
+
+  exploit transl_code_at_pc_intro; eauto; unfold transf_function; auto. {
+    rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto.
+  } intros TRANSL_CODE.
+
+  assert (next_addr next (transl_function f) rs0' =
+          Some (Vptr fb (Ptrofs.repr (next (transl_function f)
+                        (Ptrofs.unsigned Ptrofs.zero))))) as NEXT_ADDR. {
+    unfold next_addr; rewrite AGPC; rewrite AGPC'; rewrite ATPC; reflexivity.
+  }
+
+  exploit exit_step_simulation; eauto.
+  intros (? & ? & EXIT_STEP & MATCH_EXIT).
+
+  exploit exec_bblock_all; eauto.
+  intros EXEC_BBLOCK.
+
+  exploit exec_step_internal; eauto.
+  apply is_pos_simplify; eauto. rewrite H3; rewrite TF_CODE; apply First_pos.
+Qed.
+
+Lemma prologue_simulation_header_step t s1' s sp fb ms f m1 rs0 m0 rs1
+  (STACKS : match_stack s)
+  (AG : agree ms sp rs1)
+  (ATPC : rs0 PC = Vptr fb Ptrofs.zero)
+  (ATLR : rs0 RA = parent_ra s)
+  (FIND : Genv.find_funct_ptr ge fb = Some (Internal f))
+  (PROL : exec_prologue f 0 rs0 m0 = Next rs1 m1)
+  (STEP : Machblock.step rao ge (Machblock.State s fb sp (fn_code f) ms m1) t s1')
+  (HEADER: has_header (fn_code f) = true):
+  exists s2' : state, plus (step next) tge {| _rs := rs0; _m := m0 |} t s2' /\ match_states s1' s2'.
+Proof.
+  inv STEP.
+
+  (* FIRST STEP *)
+  exploit functions_translated; eauto;
+  intros (tf & FINDtf & TRANSf); monadInv TRANSf.
+  exploit transf_function_def; eauto; unfold transf_function; auto;
+  unfold insert_implicit_prologue; rewrite HEADER; intros TF_CODE.
+
+  exploit is_pos_next_zero; eauto; rewrite HEADER; rewrite H3;
+  intros IS_POS.
+
+  exploit prologue_preserves_pc; eauto.
+  intros AGPC'.
+
+  assert ( next_addr next (transl_function f) rs1
+         = Some (Vptr fb (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero))))
+         ) as NEXT_ADDR0. { unfold next_addr; rewrite AGPC'; rewrite ATPC; trivial. }
+
+  exploit exec_nil_body; intros BODY0.
+  assert ((body {| header := nil; body := nil; exit := None |}) = nil) as NIL; auto.
+  rewrite <- NIL in BODY0.
+
+  exploit exec_None_exit; intros EXIT0.
+  assert ((exit {| header := nil; body := nil; exit := None |}) = None) as NONE; auto.
+  rewrite <- NONE in EXIT0.
+
+  exploit exec_bblock_all; eauto;
+  intros BBLOCK0.
+
+  exploit exec_step_internal; eauto. rewrite <- TF_CODE; apply First_pos.
+  intros STEP0.
+
+  clear BODY0 BBLOCK0 EXIT0.
+
+  (* SECOND step *)
+
+  exploit (mkagree ms sp
+            (rs1 # PC <- (Vptr fb (Ptrofs.repr (next (transl_function f)
+                         (Ptrofs.unsigned Ptrofs.zero)))))); eauto.
+  apply (agree_sp ms); apply agree_set_other; eauto.
+  intros AG'.
+
+  exploit body_step_simulation; eauto; unfold transf_function; auto.
+  intros (rs1' & BODY1 & AGRS1' & AGPC).
+
+  assert ( next_addr next (transl_function f) rs1'
+         = Some (Vptr fb (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned
+           (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)))))))
+         ) as NEXT_ADDR1. { unfold next_addr; rewrite AGPC; reflexivity. }
+
+  assert (IS_POS' := IS_POS).
+  rewrite <- H3 in IS_POS'; apply Next_pos in IS_POS'.
+  exploit transl_code_at_pc_intro; eauto; unfold transf_function; auto. {
+    rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto.
+    assert (0 < next (transl_function f) 0) as Z0. { apply next_progress. }
+    assert ( next (transl_function f) 0
+           < next (transl_function f) (next (transl_function f) 0)
+           ) as Z1. { apply next_progress. }
+    rewrite <- Z1. exact Z0.
+  } intros TRANSL_CODE1.
+
+  exploit exit_step_simulation; eauto.
+  rewrite Ptrofs.unsigned_repr.
+  2: {
+    assert(max_pos (transl_function f) <= Ptrofs.max_unsigned) as MAX_POS. {
+      eapply functions_bound_max_pos; eauto.
+    }
+    rewrite <- MAX_POS.
+    eapply is_pos_bound_pos; eauto.
+  }
+  exact TRANSL_CODE1.
+  intros (? & ? & EXIT_STEP & MATCH_EXIT).
+
+  exploit (trivial_exec_prologue (transl_function f) (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)))). {
+    rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto.
+  } intros NO_PROL.
+
+  exploit exec_bblock_all; eauto; intros BBLOCK1.
+
+  clear AGPC.
+  rewrite <- H3 in IS_POS.
+  exploit (exec_step_internal next tge fb
+                              (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)))
+                              (transl_function f)
+                              bb c); simplify_regmap; eauto.
+
+  intros STEP1.
+
+  eexists; split.
+  + eapply plus_two.
+    * exact STEP0.
+    * exact STEP1.
+    * trivial.
+  + assumption.
+Qed.
+
+Lemma step_simulation s1 t s1':
+  Machblock.step rao ge s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  (exists s2', plus (step next) tge s2 t s2' /\ match_states s1' s2') \/ ((measure s1' < measure s1)%nat /\ t = E0 /\ match_states s1' s2).
+Proof.
+  intros STEP s2 MATCH; destruct MATCH.
+  - exploit inst_step_simulation; eauto.
+  - left.
+    destruct (has_header (fn_code f)) eqn:NO_HEADER.
+    + eapply prologue_simulation_header_step; eauto.
+    + exploit prologue_simulation_no_header_step; eauto;
+      intros (s2' & NO_HEADER_STEP & MATCH_STATES).
+      eexists; split; eauto.
+      apply plus_one; eauto.
+  - inv STEP; simpl; exploit functions_translated; eauto;
+    intros (tf0 & FINDtf & TRANSf);
+    monadInv TRANSf.
+    * (* internal calls *)
+      right.
+      intuition.
+      econstructor; eauto.
+      -- exploit
+           (mkagree (undef_regs destroyed_at_function_entry ms)
+                    sp
+                    (set_from_Machrs (undef_regs destroyed_at_function_entry rs) rs) # SP <- sp
+           ); eauto.
+      ++ unfold sp; discriminate.
+      ++ intros mr; unfold undef_regs;
+         induction destroyed_at_function_entry as [ | ? ? IH].
+         ** inversion AG as [_ _ AG_MREGS]; apply AG_MREGS.
+         ** fold undef_regs in *;
+            unfold Regmap.set; simpl; rewrite IH; reflexivity.
+      -- unfold exec_prologue;
+         inversion AG as (RS_SP & ?); rewrite RS_SP; fold sp;
+         rewrite H4; fold sp; rewrite H7; rewrite ATLR; rewrite H8; eauto.
+    * (* external calls *)
+      left.
+      exploit extcall_arguments_match; eauto.
+      eexists; split.
+      + eapply plus_one.
+        eapply exec_step_external; eauto.
+        eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+      + econstructor; eauto.
+  - (* Returnstate *)
+   inv STEP; simpl; right.
+   inv STACKS; simpl in *; subst.
+   repeat (econstructor; eauto).
+Qed.
+
+(** * The main simulation theorem *)
+
+Theorem transf_program_correct:
+  forward_simulation (Machblock.semantics rao prog) (semantics next tprog).
+Proof.
+  eapply forward_simulation_star with (measure := measure).
+  apply senv_preserved.
+  - eexact transf_initial_states.
+  - eexact transf_final_states.
+  - eexact step_simulation.
+Qed.
+
+End PRESERVATION.