cleaning

2 files changed, 0 insertions, 1440 deletions

diff --git a/scheduling/PseudoAsmblock.v b/scheduling/PseudoAsmblock.v
deleted file mode 100644
index b33ea1bd..00000000
--- a/scheduling/PseudoAsmblock.v
+++ /dev/null
@@ -1,267 +0,0 @@
-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.
-
-Module AsmNotations.
-
-(* 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.
-Open Scope asm.
-
-End AsmNotations.
-
-Import AsmNotations.
-
-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.
-
-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/scheduling/PseudoAsmblockproof.v b/scheduling/PseudoAsmblockproof.v
deleted file mode 100644
index 67308278..00000000
--- a/scheduling/PseudoAsmblockproof.v
+++ /dev/null
@@ -1,1173 +0,0 @@
-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.
-Import PseudoAsmblock.AsmNotations.
-
-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 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.