cleaning

1 files changed, 0 insertions, 2245 deletions

diff --git a/aarch64/Asmgenproof_orig_single_label_in_header.v.stash b/aarch64/Asmgenproof_orig_single_label_in_header.v.stash
deleted file mode 100644
index bff18716..00000000
--- a/aarch64/Asmgenproof_orig_single_label_in_header.v.stash
+++ /dev/null
@@ -1,2245 +0,0 @@
-(* *************************************************************)
-(*                                                             *)
-(*             The Compcert verified compiler                  *)
-(*                                                             *)
-(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
-(*           Léo Gourdin        UGA, VERIMAG                   *)
-(*           Justus Fasse       UGA, 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.                          *)
-(*                                                             *)
-(* *************************************************************)
-
-Require Import Coqlib Errors.
-Require Import Integers Floats AST Linking.
-Require Import Values Memory Events Globalenvs Smallstep.
-Require Import Op Locations Machblock Conventions PseudoAsmblock Asm Asmblock.
-Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
-Require Import Asmgen.
-Require Import Axioms.
-Require Import IterList.
-Require Import Ring.
-
-Module Asmblock_PRESERVATION.
-
-Import Asmblock_TRANSF.
-
-Definition match_prog (p: Asmblock.program) (tp: Asm.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.
-
-Section PRESERVATION.
-
-Variable prog: Asmblock.program.
-Variable tprog: Asm.program.
-Hypothesis TRANSF: match_prog prog tprog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}.
-
-Lemma symbols_preserved:
-  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
-
-Lemma symbol_addresses_preserved:
-  forall (s: ident) (ofs: ptrofs),
-  Genv.symbol_address tge s ofs = Genv.symbol_address ge s ofs.
-Proof.
-  intros; unfold Genv.symbol_address; rewrite symbols_preserved; reflexivity.
-Qed.
-
-Lemma senv_preserved:
-  Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
-
-Lemma symbol_high_low: forall (id: ident) (ofs: ptrofs),
-  Val.addl (Asmblock.symbol_high lk id ofs) (Asmblock.symbol_low lk id ofs) = Genv.symbol_address ge id ofs.
-Proof.
-  unfold lk; simpl. intros; rewrite Asm.symbol_high_low; unfold Genv.symbol_address;
-  rewrite symbols_preserved; reflexivity.
-Qed.
-
-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 internal_functions_translated:
-  forall b f,
-  Genv.find_funct_ptr ge b = Some (Internal f) ->
-  exists tf,
-  Genv.find_funct_ptr tge b = Some (Internal tf) /\ transf_function f = OK tf.
-Proof.
-  intros; exploit functions_translated; eauto.
-  intros (x & FIND & TRANSf).
-  apply bind_inversion in TRANSf.
-  destruct TRANSf as (tf & TRANSf & X).
-  inv X.
-  eauto.
-Qed.
-
-Lemma internal_functions_unfold:
-  forall b f,
-  Genv.find_funct_ptr ge b = Some (Internal f) ->
-  exists tc,
-  Genv.find_funct_ptr tge b = Some (Internal (Asm.mkfunction (fn_sig f) tc))
-  /\ unfold (fn_blocks f) = OK tc
-  /\ list_length_z tc <= Ptrofs.max_unsigned.
-Proof.
-  intros.
-  exploit internal_functions_translated; eauto.
-  intros (tf & FINDtf & TRANStf).
-  unfold transf_function in TRANStf.
-  monadInv TRANStf.
-  destruct (zlt _ _); try congruence.
-  inv EQ. inv EQ0.
-  eexists; intuition eauto.
-  omega.
-Qed.
-
-
-Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop :=
-  | is_nth_label l:
-     list_nth_z (header bb) n = Some l ->
-     i = Asm.Plabel l ->
-     is_nth_inst bb n i
-  | is_nth_basic bi:
-     list_nth_z (body bb) (n - list_length_z (header bb)) = Some bi ->
-     basic_to_instruction bi = OK i ->
-     is_nth_inst bb n i
-  | is_nth_ctlflow cfi:
-     (exit bb) = Some cfi ->
-     n = size bb - 1 ->
-     i = control_to_instruction cfi ->
-     is_nth_inst bb n i.
-
-(* Asmblock and Asm share the same definition of state *)
-Definition match_states (s1 s2 : state) := s1 = s2.
-
-Inductive match_internal: forall n, state -> state -> Prop :=
-  | match_internal_intro n rs1 m1 rs2 m2
-    (MEM: m1 = m2)
-    (AG: forall r, r <> PC -> rs1 r = rs2 r)
-    (AGPC: Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC)
-    : match_internal n (State rs1 m1) (State rs2 m2).
-
-Lemma match_internal_set_parallel:
-  forall n rs1 m1 rs2 m2 r val,
-  match_internal n (State rs1 m1) (State rs2 m2) ->
-  r <> PC ->
-  match_internal n (State (rs1#r <- val) m1) (State (rs2#r <- val ) m2).
-Proof.
-  intros n rs1 m1 rs2 m2 r v MI.
-  inversion MI; constructor; auto.
-  - intros r' NOTPC.
-    unfold Pregmap.set; rewrite AG. reflexivity. assumption.
-  - unfold Pregmap.set; destruct (PregEq.eq PC r); congruence.
-Qed.
-
-Lemma agree_match_states:
-  forall rs1 m1 rs2 m2,
-  match_states (State rs1 m1) (State rs2 m2) ->
-  forall r : preg, rs1#r = rs2#r.
-Proof.
-  intros.
-  unfold match_states in *.
-  assert (rs1 = rs2) as EQ. { congruence. }
-  rewrite EQ. reflexivity.
-Qed.
-
-Lemma match_states_set_parallel:
-  forall rs1 m1 rs2 m2 r v,
-  match_states (State rs1 m1) (State rs2 m2) ->
-  match_states (State (rs1#r <- v) m1) (State (rs2#r <- v) m2).
-Proof.
-  intros; unfold match_states in *.
-  assert (rs1 = rs2) as RSEQ. { congruence. }
-  assert (m1 = m2) as MEQ. { congruence. }
-  rewrite RSEQ in *; rewrite MEQ in *; unfold Pregmap.set; reflexivity.
-Qed.
-
-(* match_internal from match_states *)
-Lemma mi_from_ms:
-  forall rs1 m1 rs2 m2 b ofs,
-  match_states (State rs1 m1) (State rs2 m2) ->
-  rs1#PC = Vptr b ofs ->
-  match_internal 0 (State rs1 m1) (State rs2 m2).
-Proof.
-  intros rs1 m1 rs2 m2 b ofs MS PCVAL.
-  inv MS; constructor; auto; unfold Val.offset_ptr;
-  rewrite PCVAL; rewrite Ptrofs.add_zero; reflexivity.
-Qed.
-
-Lemma transf_initial_states:
-  forall s1, Asmblock.initial_state prog s1 ->
-  exists s2, Asm.initial_state tprog s2 /\ match_states s1 s2.
-Proof.
-  intros ? INIT_s1.
-  inversion INIT_s1 as (m, ?, ge0, rs). unfold ge0 in *.
-  econstructor; split.
-  - econstructor.
-    eapply (Genv.init_mem_transf_partial TRANSF); eauto.
-  - rewrite (match_program_main TRANSF); rewrite symbol_addresses_preserved.
-    unfold rs; reflexivity.
-Qed.
-
-Lemma transf_final_states:
-  forall s1 s2 r,
-  match_states s1 s2 -> Asmblock.final_state s1 r -> Asm.final_state s2 r.
-Proof.
-  intros s1 s2 r MATCH FINAL_s1.
-  inv FINAL_s1; inv MATCH; constructor; assumption.
-Qed.
-
-Definition max_pos (f : Asm.function) := list_length_z f.(Asm.fn_code).
-
-Lemma functions_bound_max_pos: forall 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 fb f tf FINDf TRANSf.
-  unfold transf_function in TRANSf.
-  apply bind_inversion in TRANSf.
-  destruct TRANSf as (c & TRANSf).
-  destruct TRANSf as (_ & TRANSf).
-  destruct (zlt _ _).
-  - inversion TRANSf.
-  - unfold max_pos.
-    assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. }
-    rewrite H; omega.
-Qed.
-
-Lemma one_le_max_unsigned:
-  1 <= Ptrofs.max_unsigned.
-Proof.
-  unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize;
-  unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega.
-Qed.
-
-(* NB: does not seem useful anymore, with the [exec_header_simulation] proof below
-Lemma match_internal_exec_label:
-  forall n rs1 m1 rs2 m2 l fb f tf,
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  transf_function f = OK tf ->
-  match_internal n (State rs1 m1) (State rs2 m2) ->
-  n >= 0 ->
-  (* There is no step if n is already max_pos *)
-  n < (max_pos tf) ->
-  exists rs2' m2', Asm.exec_instr tge tf (Asm.Plabel l) rs2 m2 = Next rs2' m2'
-                   /\ match_internal (n+1) (State rs1 m1) (State rs2' m2').
-Proof.
-  intros. (* XXX auto generated names *)
-  unfold Asm.exec_instr.
-  eexists; eexists; split; eauto.
-  inversion H1; constructor; auto.
-  - intros; unfold Asm.nextinstr; unfold Pregmap.set;
-    destruct (PregEq.eq r PC); auto; contradiction.
-  - unfold Asm.nextinstr; rewrite Pregmap.gss; unfold Ptrofs.one.
-    rewrite <- AGPC; rewrite Val.offset_ptr_assoc; unfold Ptrofs.add;
-    rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; trivial.
-    + split.
-      * apply Z.le_0_1.
-      * apply one_le_max_unsigned.
-    + split.
-      * apply Z.ge_le; assumption.
-      * rewrite <- functions_bound_max_pos; eauto; omega.
-Qed.
-*)
-
-Lemma incrPC_agree_but_pc:
-  forall rs r ofs,
-  r <> PC ->
-  (incrPC ofs rs)#r = rs#r.
-Proof.
-  intros rs r ofs NOTPC.
-  unfold incrPC; unfold Pregmap.set; destruct (PregEq.eq r PC).
-  - contradiction.
-  - reflexivity.
-Qed.
-
-Lemma bblock_non_empty bb: body bb <> nil \/ exit bb <> None.
-Proof.
-  destruct bb. simpl.
-  unfold non_empty_bblockb in correct.
-  unfold non_empty_body, non_empty_exit, Is_true in correct.
-  destruct body, exit.
-  - right. discriminate.
-  - contradiction.
-  - right. discriminate.
-  - left. discriminate.
-Qed.
-
-Lemma list_length_z_aux_increase A (l: list A): forall acc,
-  list_length_z_aux l acc >= acc.
-Proof.
-  induction l; simpl; intros.
-  - omega.
-  - generalize (IHl (Z.succ acc)). omega.
-Qed.
-
-Lemma bblock_size_aux_pos bb: list_length_z (body bb) + Z.of_nat (length_opt (exit bb)) >= 1.
-Proof.
-  destruct (bblock_non_empty bb), (body bb) as [|hd tl], (exit bb); simpl;
-  try (congruence || omega);
-  unfold list_length_z; simpl;
-  generalize (list_length_z_aux_increase _ tl 1); omega.
-Qed.
-
-
-Lemma list_length_add_acc A (l : list A) acc:
-  list_length_z_aux l acc = (list_length_z l) + acc.
-Proof.
-    unfold list_length_z, list_length_z_aux. simpl.
-    fold list_length_z_aux.
-    rewrite (list_length_z_aux_shift l acc 0).
-    omega.
-Qed.
-
-Lemma list_length_z_cons A hd (tl : list A):
-  list_length_z (hd :: tl) = list_length_z tl + 1.
-Proof.
-  unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity.
-Qed.
-
-(*Lemma length_agree A (l : list A):*)
-  (*list_length_z l = Z.of_nat (length l).*)
-(*Proof.*)
-  (*induction l as [| ? l IH]; intros.*)
-  (*- unfold list_length_z; reflexivity.*)
-  (*- simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega.*)
-(*Qed.*)
-
-Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)).
-Proof.
-  unfold size.
-  repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). reflexivity.
-Qed.
-
-Lemma header_size_lt_block_size bb:
-  list_length_z (header bb) < size bb.
-Proof.
-  rewrite bblock_size_aux.
-  generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT].
-  - destruct (body bb); try contradiction; rewrite list_length_z_cons;
-    repeat rewrite list_length_z_nat; omega.
-  - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; omega.
-Qed.
-
-Lemma body_size_le_block_size bb:
-  list_length_z (body bb) <= size bb.
-Proof.
-  rewrite bblock_size_aux; repeat rewrite list_length_z_nat; omega.
-Qed.
-
-
-Lemma bblock_size_pos bb: size bb >= 1.
-Proof.
-  rewrite (bblock_size_aux bb).
-  generalize (bblock_size_aux_pos bb).
-  generalize (list_length_z_pos (header bb)).
-  omega.
-Qed.
-
-Lemma unfold_car_cdr bb bbs tc:
-  unfold (bb :: bbs) = OK tc ->
-  exists tbb tc', unfold_bblock bb = OK tbb
-                  /\ unfold bbs = OK tc'
-                  /\ unfold (bb :: bbs) = OK (tbb ++ tc').
-Proof.
-  intros UNFOLD.
-  assert (UF := UNFOLD).
-  unfold unfold in UNFOLD.
-  apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UBB). destruct UBB as (UBB & REST).
-  apply bind_inversion in REST. destruct REST as (? & UNFOLD').
-  fold unfold in UNFOLD'. destruct UNFOLD' as (UNFOLD' & UNFOLD).
-  rewrite <- UNFOLD in UF.
-  eauto.
-Qed.
-
-Lemma unfold_cdr bb bbs tc:
-  unfold (bb :: bbs) = OK tc ->
-  exists tc', unfold bbs = OK tc'.
-Proof.
-  intros; exploit unfold_car_cdr; eauto. intros (_ & ? & _ & ? & _).
-  eexists; eauto.
-Qed.
-
-Lemma unfold_car bb bbs tc:
-  unfold (bb :: bbs) = OK tc ->
-  exists tbb, unfold_bblock bb = OK tbb.
-Proof.
-  intros; exploit unfold_car_cdr; eauto. intros (? & _ & ? & _ & _).
-  eexists; eauto.
-Qed.
-
-Lemma all_blocks_translated:
-  forall bbs tc,
-  unfold bbs = OK tc ->
-  forall bb, In bb bbs ->
-  exists c, unfold_bblock bb = OK c.
-Proof.
-  induction bbs as [| bb bbs IHbbs].
-  - contradiction.
-  - intros ? UNFOLD ? IN.
-    (* unfold proceeds by unfolding the basic block at the head of the list and
-     * then recurring *)
-    exploit unfold_car_cdr; eauto. intros (? & ? & ? & ? & _).
-    (* basic block is either in head or tail *)
-    inversion IN as [EQ | NEQ].
-    + rewrite <- EQ; eexists; eauto.
-    + eapply IHbbs; eauto.
-Qed.
-
-Lemma entire_body_translated:
-  forall lbi tc,
-  unfold_body lbi = OK tc ->
-  forall bi, In bi lbi ->
-  exists bi', basic_to_instruction bi = OK bi'.
-Proof.
-  induction lbi as [| a lbi IHlbi].
-  - intros. contradiction.
-  - intros tc UNFOLD_BODY bi IN.
-    unfold unfold_body in UNFOLD_BODY. apply bind_inversion in UNFOLD_BODY.
-    destruct UNFOLD_BODY as (? & TRANSbi & REST).
-    apply bind_inversion in REST. destruct REST as (? & UNFOLD_BODY' & ?).
-    fold unfold_body in UNFOLD_BODY'.
-
-    inversion IN as [EQ | NEQ].
-    + rewrite <- EQ; eauto.
-    + eapply IHlbi; eauto.
-Qed.
-
-Lemma bblock_in_bblocks bbs bb: forall
-  tc pos
-  (UNFOLD: unfold bbs = OK tc)
-  (FINDBB: find_bblock pos bbs = Some bb),
-  In bb bbs.
-Proof.
-  induction bbs as [| b bbs IH].
-  - intros. inversion FINDBB.
-  - destruct pos.
-    + intros. inversion FINDBB as (EQ). rewrite <- EQ. apply in_eq.
-    + intros.
-      exploit unfold_cdr; eauto. intros (tc' & UNFOLD').
-      unfold find_bblock in FINDBB. simpl in FINDBB.
-      fold find_bblock in FINDBB.
-      apply in_cons. eapply IH; eauto.
-    + intros. inversion FINDBB.
-Qed.
-
-Lemma blocks_translated tc pos bbs bb: forall
-  (UNFOLD: unfold bbs = OK tc)
-  (FINDBB: find_bblock pos bbs = Some bb),
-  exists tbb, unfold_bblock bb = OK tbb.
-Proof.
-  intros; exploit bblock_in_bblocks; eauto; intros;
-  eapply all_blocks_translated; eauto.
-Qed.
-
-Lemma size_header b pos f bb: forall
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock pos (fn_blocks f) = Some bb),
-  list_length_z (header bb) <= 1.
-Proof.
-  intros.
-  exploit internal_functions_unfold; eauto.
-  intros (tc & FINDtf & TRANStf & ?).
-  exploit blocks_translated; eauto. intros TBB.
-
-  unfold unfold_bblock in TBB.
-  destruct (zle (list_length_z (header bb)) 1).
-  - assumption.
-  - destruct TBB as (? & TBB). discriminate TBB.
-Qed.
-
-Lemma list_nth_z_neg A (l: list A): forall n,
-  n < 0 -> list_nth_z l n = None.
-Proof.
-  induction l; simpl; auto.
-  intros n H; destruct (zeq _ _); (try eapply IHl); omega.
-Qed.
-
-Lemma find_bblock_neg bbs: forall pos,
-  pos < 0 -> find_bblock pos bbs = None.
-Proof.
-  induction bbs; simpl; auto.
-  intros. destruct (zlt pos 0). { reflexivity. }
-  destruct (zeq pos 0); contradiction.
-Qed.
-
-Lemma equal_header_size bb:
-  length (header bb) = length (unfold_label (header bb)).
-Proof.
-  induction (header bb); auto.
-  simpl. rewrite IHl. auto.
-Qed.
-
-Lemma equal_body_size:
-  forall bb tb,
-  unfold_body (body bb) = OK tb ->
-  length (body bb) = length tb.
-Proof.
-  intros bb. induction (body bb).
-  - simpl. intros ? H. inversion H. auto.
-  - intros tb H. simpl in H. apply bind_inversion in H. destruct H as (? & BI & TAIL).
-    apply bind_inversion in TAIL. destruct TAIL as (tb' & BODY' & CONS). inv CONS.
-    simpl. specialize (IHl tb' BODY'). rewrite IHl. reflexivity.
-Qed.
-
-Lemma equal_exit_size bb:
-  length_opt (exit bb) = length (unfold_exit (exit bb)).
-Proof.
-  destruct (exit bb); trivial.
-Qed.
-
-Lemma bblock_size_preserved bb tb:
-  unfold_bblock bb = OK tb ->
-  size bb = list_length_z tb.
-Proof.
-  unfold unfold_bblock. intros UNFOLD_BBLOCK.
-  destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. }
-  apply bind_inversion in UNFOLD_BBLOCK. destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & CONS).
-  inversion CONS.
-  unfold size.
-  rewrite equal_header_size, equal_exit_size.
-  erewrite equal_body_size; eauto.
-  rewrite list_length_z_nat.
-  repeat (rewrite app_length).
-  rewrite plus_assoc. auto.
-Qed.
-
-Lemma size_of_blocks_max_pos_aux:
-  forall bbs tbbs pos bb,
-  find_bblock pos bbs = Some bb ->
-  unfold bbs = OK tbbs ->
-  pos + size bb <= list_length_z tbbs.
-Proof.
-  induction bbs as [| bb ? IHbbs].
-  - intros tbbs ? ? FINDBB; inversion FINDBB.
-  - simpl; intros tbbs pos bb' FINDBB UNFOLD.
-    apply bind_inversion in UNFOLD; destruct UNFOLD as (tbb & UNFOLD_BBLOCK & H).
-    apply bind_inversion in H; destruct H as (tbbs' & UNFOLD & CONS).
-    inv CONS.
-    destruct (zlt pos 0). { discriminate FINDBB. }
-    destruct (zeq pos 0).
-    + inv FINDBB.
-      exploit bblock_size_preserved; eauto; intros SIZE; rewrite SIZE.
-      repeat (rewrite list_length_z_nat). rewrite app_length, Nat2Z.inj_add.
-      omega.
-    + generalize (IHbbs tbbs' (pos - size bb) bb' FINDBB UNFOLD). intros IH.
-      exploit bblock_size_preserved; eauto; intros SIZE.
-      repeat (rewrite list_length_z_nat); rewrite app_length.
-      rewrite Nat2Z.inj_add; repeat (rewrite <- list_length_z_nat).
-      omega.
-Qed.
-
-Lemma size_of_blocks_max_pos pos f tf bi:
-  find_bblock pos (fn_blocks f) = Some bi ->
-  transf_function f = OK tf ->
-  pos + size bi <= max_pos tf.
-Proof.
-  unfold transf_function, max_pos.
-  intros FINDBB UNFOLD.
-  apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UNFOLD & H).
-  destruct (zlt Ptrofs.max_unsigned (list_length_z x)). { discriminate H. }
-  inv H. simpl.
-  eapply size_of_blocks_max_pos_aux; eauto.
-Qed.
-
-Lemma unfold_bblock_not_nil bb:
-  unfold_bblock bb = OK nil -> False.
-Proof.
-  intros.
-  exploit bblock_size_preserved; eauto. unfold list_length_z; simpl. intros SIZE.
-  generalize (bblock_size_pos bb). intros SIZE'. omega.
-Qed.
-
-(* same proof as list_nth_z_range (Coqlib) *)
-Lemma find_instr_range:
-  forall c n i,
-  Asm.find_instr n c = Some i -> 0 <= n < list_length_z c.
-Proof.
-  induction c; simpl; intros.
-  discriminate.
-  rewrite list_length_z_cons. destruct (zeq n 0).
-  generalize (list_length_z_pos c); omega.
-  exploit IHc; eauto. omega.
-Qed.
-
-Lemma find_instr_tail:
-  forall tbb pos c i,
-  Asm.find_instr pos c = Some i ->
-  Asm.find_instr (pos + list_length_z tbb) (tbb ++ c) = Some i.
-Proof.
-  induction tbb as [| ? ? IHtbb].
-  - intros. unfold list_length_z; simpl. rewrite Z.add_0_r. assumption.
-  - intros. rewrite list_length_z_cons. simpl.
-    destruct (zeq (pos + (list_length_z tbb + 1)) 0).
-    + exploit find_instr_range; eauto. intros POS_RANGE.
-      generalize (list_length_z_pos tbb). omega.
-    + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega.
-      eapply IHtbb; eauto.
-Qed.
-
-Lemma size_of_blocks_bounds fb pos f bi:
-      Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      find_bblock pos (fn_blocks f) = Some bi ->
-      pos + size bi <= Ptrofs.max_unsigned.
-Proof.
-  intros; exploit internal_functions_translated; eauto.
-  intros (tf & _ & TRANSf).
-  assert (pos + size bi <= max_pos tf). { eapply size_of_blocks_max_pos; eauto. }
-  assert (max_pos tf <= Ptrofs.max_unsigned). { eapply functions_bound_max_pos; eauto. }
-  omega.
-Qed.
-
-Lemma find_instr_bblock_tail:
-  forall tbb bb pos c i,
-  Asm.find_instr pos c = Some i ->
-  unfold_bblock bb = OK tbb ->
-  Asm.find_instr (pos + size bb ) (tbb ++ c) = Some i.
-Proof.
-  induction tbb.
-   - intros. exploit unfold_bblock_not_nil; eauto. intros. contradiction.
-   - intros. simpl.
-     destruct (zeq (pos + size bb) 0).
-     + (* absurd *)
-       exploit find_instr_range; eauto. intros POS_RANGE.
-       generalize (bblock_size_pos bb). intros SIZE. omega.
-     + erewrite bblock_size_preserved; eauto.
-       rewrite list_length_z_cons.
-       replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega.
-       apply find_instr_tail; auto.
-Qed.
-
-Lemma list_nth_z_find_label:
-  forall (ll : list label) il n l,
-  list_nth_z ll n = Some l ->
-  Asm.find_instr n ((unfold_label ll) ++ il) = Some (Asm.Plabel l).
-Proof.
-  induction ll.
-  - intros. inversion H.
-  - intros. simpl.
-    destruct (zeq n 0) as [Z | NZ].
-    + inversion H as (H'). rewrite Z in H'. simpl in H'. inv H'. reflexivity.
-    + simpl in H. destruct (zeq n 0). { contradiction. }
-      apply IHll; auto.
-Qed.
-
-Lemma list_nth_z_find_bi:
-  forall lbi bi tlbi n bi' exit,
-  list_nth_z lbi n = Some bi ->
-  unfold_body lbi = OK tlbi ->
-  basic_to_instruction bi = OK bi' ->
-  Asm.find_instr n (tlbi ++ exit) = Some bi'.
-Proof.
-  induction lbi.
-  - intros. inversion H.
-  - simpl. intros.
-    apply bind_inversion in H0. destruct H0 as (? & ? & ?).
-    apply bind_inversion in H2. destruct H2 as (? & ? & ?).
-    destruct (zeq n 0) as [Z | NZ].
-    + destruct n.
-      * inversion H as (BI). rewrite BI in *.
-        inversion H3. simpl. congruence.
-      * (* absurd *) congruence.
-      * (* absurd *) congruence.
-    + inv H3. simpl. destruct (zeq n 0). { contradiction. }
-      eapply IHlbi; eauto.
-Qed.
-
-Lemma list_nth_z_find_bi_with_header:
-  forall ll lbi bi tlbi n bi' (rest : list Asm.instruction),
-  list_nth_z lbi (n - list_length_z ll) = Some bi ->
-  unfold_body lbi = OK tlbi ->
-  basic_to_instruction bi = OK bi' ->
-  Asm.find_instr n ((unfold_label ll) ++ (tlbi) ++ (rest)) = Some bi'.
-Proof.
-  induction ll.
-  - unfold list_length_z. simpl. intros.
-    replace (n - 0) with n in H by omega. eapply list_nth_z_find_bi; eauto.
-  - intros. simpl. destruct (zeq n 0).
-    + rewrite list_length_z_cons in H. rewrite e in H.
-      replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by omega.
-      generalize (list_length_z_pos ll). intros.
-      rewrite list_nth_z_neg in H; try omega. inversion H.
-    + rewrite list_length_z_cons in H.
-      replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by omega.
-      eapply IHll; eauto.
-Qed.
-
-(* XXX unused *)
-Lemma range_list_nth_z:
-  forall (A: Type) (l: list A) n,
-  0 <= n < list_length_z l ->
-  exists x, list_nth_z l n = Some x.
-Proof.
-  induction l.
-  - intros. unfold list_length_z in H. simpl in H. omega.
-  - intros n. destruct (zeq n 0).
-    + intros. simpl. destruct (zeq n 0). { eauto. } contradiction.
-    + intros H. rewrite list_length_z_cons in H.
-      simpl. destruct (zeq n 0). { contradiction. }
-      replace (Z.pred n) with (n - 1) by omega.
-      eapply IHl; omega.
-Qed.
-
-Lemma list_nth_z_n_too_big:
-  forall (A: Type) (l: list A) n,
-  0 <= n ->
-  list_nth_z l n = None ->
-  n >= list_length_z l.
-Proof.
-  induction l.
-  - intros. unfold list_length_z. simpl. omega.
-  - intros. rewrite list_length_z_cons.
-    simpl in H0.
-    destruct (zeq n 0) as [N | N].
-    + inversion H0.
-    + (* XXX there must be a more elegant way to prove this simple fact *)
-      assert (n > 0). { omega. }
-      assert (0 <= n - 1). { omega. }
-      generalize (IHl (n - 1)). intros IH.
-      assert (n - 1 >= list_length_z l). { auto. }
-      assert (n > list_length_z l); omega.
-Qed.
-
-Lemma find_instr_past_header:
-  forall labels n rest,
-  list_nth_z labels n = None ->
-  Asm.find_instr n (unfold_label labels ++ rest) =
-  Asm.find_instr (n - list_length_z labels) rest.
-Proof.
-  induction labels as [| label labels' IH].
-  - unfold list_length_z; simpl; intros; rewrite Z.sub_0_r; reflexivity.
-  - intros. simpl. destruct (zeq n 0) as [N | N].
-    + rewrite N in H. inversion H.
-    + rewrite list_length_z_cons.
-      replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by omega.
-      simpl in H. destruct (zeq n 0). { contradiction. }
-      replace (Z.pred n) with (n - 1) in H by omega.
-      apply IH; auto.
-Qed.
-
-(* very similar to find_instr_past_header *)
-Lemma find_instr_past_body:
-  forall lbi n tlbi rest,
-  list_nth_z lbi n = None ->
-  unfold_body lbi = OK tlbi ->
-  Asm.find_instr n (tlbi ++ rest) =
-  Asm.find_instr (n - list_length_z lbi) rest.
-Proof.
-  induction lbi.
-  - unfold list_length_z; simpl; intros ? ? ? ? H. inv H; rewrite Z.sub_0_r; reflexivity.
-  - intros n tlib ? NTH UNFOLD_BODY.
-    unfold unfold_body in UNFOLD_BODY. apply bind_inversion in UNFOLD_BODY.
-    destruct UNFOLD_BODY as (? & BI & H).
-    apply bind_inversion in H. destruct H as (? & UNFOLD_BODY' & CONS).
-    fold unfold_body in UNFOLD_BODY'. inv CONS.
-    simpl; destruct (zeq n 0) as [N|N].
-    + rewrite N in NTH; inversion NTH.
-    + rewrite list_length_z_cons.
-      replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by omega.
-      simpl in NTH. destruct (zeq n 0). { contradiction. }
-      replace (Z.pred n) with (n - 1)  in NTH by omega.
-      apply IHlbi; auto.
-Qed.
-
-Lemma n_beyond_body:
-  forall bb n,
-  0 <= n < size bb ->
-  list_nth_z (header bb) n = None ->
-  list_nth_z (body bb) (n - list_length_z (header bb)) = None ->
-  n >= Z.of_nat (length (header bb) + length (body bb)).
-Proof.
-  intros.
-  assert (0 <= n). { omega. }
-  generalize (list_nth_z_n_too_big label (header bb) n H2 H0). intros.
-  generalize (list_nth_z_n_too_big _ (body bb) (n - list_length_z (header bb))). intros.
-  unfold size in H.
-
-  assert (0 <= n - list_length_z (header bb)). { omega. }
-  assert (n - list_length_z (header bb) >= list_length_z (body bb)). { apply H4; auto. }
-
-  assert (n >= list_length_z (header bb) + list_length_z (body bb)). { omega. }
-  rewrite Nat2Z.inj_add.
-  repeat (rewrite <- list_length_z_nat). assumption.
-Qed.
-
-Lemma exec_arith_instr_dont_move_PC ai rs rs': forall
-  (BASIC: exec_arith_instr lk ai rs = rs'),
-  rs PC = rs' PC.
-Proof.
-  destruct ai; simpl; intros;
-  try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate).
-  - destruct i; simpl in BASIC.
-    + unfold compare_long in BASIC; rewrite <- BASIC.
-      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
-    + unfold compare_long in BASIC; rewrite <- BASIC.
-      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
-    + destruct sz;
-      try (unfold compare_single in BASIC || unfold compare_float in BASIC);
-      destruct (rs r1), (rs r2);
-      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
-  - destruct i; simpl in BASIC; destruct is;
-      try (unfold compare_int in BASIC || unfold compare_long in BASIC);
-      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
-  - destruct i; simpl in BASIC; destruct sz;
-    try (unfold compare_single in BASIC || unfold compare_float in BASIC);
-    destruct (rs r1);
-    try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
-  - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
-  - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
-Qed.
-
-Lemma exec_basic_dont_move_PC bi rs m rs' m': forall
-  (BASIC: exec_basic lk ge bi rs m = Next rs' m'),
-  rs PC = rs' PC.
-Proof.
-  destruct bi; simpl; intros.
-  - inv BASIC. exploit exec_arith_instr_dont_move_PC; eauto.
-  - unfold exec_load in BASIC.
-    destruct Mem.loadv. 2: { discriminate BASIC. }
-    inv BASIC. rewrite Pregmap.gso; try discriminate; auto.
-  - unfold exec_store in BASIC.
-    destruct Mem.storev. 2: { discriminate BASIC. }
-    inv BASIC; reflexivity.
-  - destruct Mem.alloc, Mem.store. 2: { discriminate BASIC. }
-    inv BASIC. repeat (rewrite Pregmap.gso; try discriminate). reflexivity.
-  - destruct Mem.loadv. 2: { discriminate BASIC. }
-    destruct rs, Mem.free; try discriminate BASIC.
-    inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-Qed.
-
-Lemma exec_body_dont_move_PC_aux:
-  forall bis rs m rs' m'
-  (BODY: exec_body lk ge bis rs m = Next rs' m'),
-  rs PC = rs' PC.
-Proof.
-  induction bis.
-  - intros; inv BODY; reflexivity.
-  - simpl; intros.
-    remember (exec_basic lk ge a rs m) as bi eqn:BI; destruct bi. 2: { discriminate BODY. }
-    symmetry in BI; destruct s in BODY, BI; simpl in BODY, BI.
-    exploit exec_basic_dont_move_PC; eauto; intros AGPC; rewrite AGPC.
-    eapply IHbis; eauto.
-Qed.
-
-Lemma exec_body_dont_move_PC bb rs m rs' m': forall
-  (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
-  rs PC = rs' PC.
-Proof. apply exec_body_dont_move_PC_aux. Qed.
-
-Lemma find_instr_bblock:
-  forall n lb pos bb tlb
-  (FINDBB: find_bblock pos lb = Some bb)
-  (UNFOLD: unfold lb = OK tlb)
-  (SIZE: 0 <= n < size bb),
-  exists i, is_nth_inst bb n i /\ Asm.find_instr (pos+n) tlb = Some i.
-Proof.
-  induction lb as [| b lb IHlb].
-  - intros. inversion FINDBB.
-  - intros pos bb tlb FINDBB UNFOLD SIZE.
-    destruct pos.
-    + inv FINDBB. simpl.
-      exploit unfold_car_cdr; eauto. intros (tbb & tlb' & UNFOLD_BBLOCK & UNFOLD' & UNFOLD_cons).
-      rewrite UNFOLD in UNFOLD_cons. inversion UNFOLD_cons.
-      unfold unfold_bblock in UNFOLD_BBLOCK.
-      destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. }
-      apply bind_inversion in UNFOLD_BBLOCK.
-      destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & H).
-      inversion H as (UNFOLD_BBLOCK).
-      remember (list_nth_z (header bb) n) as label_opt eqn:LBL. destruct label_opt.
-      * (* nth instruction is a label *)
-        eexists; split. { eapply is_nth_label; eauto. }
-        inversion UNFOLD_cons.
-        symmetry in LBL.
-        rewrite <- app_assoc.
-        apply list_nth_z_find_label; auto.
-      * remember (list_nth_z (body bb) (n - list_length_z (header bb))) as bi_opt eqn:BI.
-        destruct bi_opt.
-        -- (* nth instruction is a basic instruction *)
-           exploit list_nth_z_in; eauto. intros INBB.
-           exploit entire_body_translated; eauto. intros BI'.
-           destruct BI'.
-           eexists; split.
-            ++ eapply is_nth_basic; eauto.
-            ++ repeat (rewrite <- app_assoc). eapply list_nth_z_find_bi_with_header; eauto.
-        -- (* nth instruction is the exit instruction *)
-           generalize n_beyond_body. intros TEMP.
-           assert (n >= Z.of_nat (Datatypes.length (header bb)
-                        + Datatypes.length (body bb))) as NGE. { auto. } clear TEMP.
-           remember (exit bb) as exit_opt eqn:EXIT. destruct exit_opt.
-           ++ rewrite <- app_assoc. rewrite find_instr_past_header; auto.
-              rewrite <- app_assoc. erewrite find_instr_past_body; eauto.
-              assert (SIZE' := SIZE).
-              unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE.
-              destruct SIZE as (LOWER & UPPER).
-              repeat (rewrite Nat2Z.inj_add in UPPER).
-              repeat (rewrite <- list_length_z_nat in UPPER). repeat (rewrite Nat2Z.inj_add in NGE).
-              repeat (rewrite <- list_length_z_nat in NGE). simpl in UPPER.
-              assert (n = list_length_z (header bb) + list_length_z (body bb)). { omega. }
-              assert (n = size bb - 1). {
-                unfold size. rewrite <- EXIT. simpl.
-                repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. omega.
-              }
-              symmetry in EXIT.
-              eexists; split.
-              ** eapply is_nth_ctlflow; eauto.
-              ** simpl.
-                 destruct (zeq (n - list_length_z (header bb) - list_length_z (body bb)) 0). { reflexivity. }
-                 (* absurd *) omega.
-           ++ (* absurd *)
-              unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE.
-              destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. omega.
-    + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB.
-      inversion UNFOLD as (UNFOLD').
-      apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')).
-      apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD' & TLB)).
-      inversion TLB.
-      generalize (IHlb _ _ _ FINDBB UNFOLD'). intros IH.
-      destruct IH as (? & (IH_is_nth & IH_find_instr)); eauto.
-      eexists; split.
-      * apply IH_is_nth.
-      * replace (Z.pos p + n) with (Z.pos p + n - size b + size b) by omega.
-        eapply find_instr_bblock_tail; try assumption.
-        replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by omega.
-        apply IH_find_instr.
-    + (* absurd *)
-      generalize (Pos2Z.neg_is_neg p). intros. exploit (find_bblock_neg (b :: lb)); eauto.
-      rewrite FINDBB. intros CONTRA. inversion CONTRA.
-Qed.
-
-Lemma exec_header_simulation b ofs f bb rs m: forall
-  (ATPC: rs PC = Vptr b ofs)
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb),
-  exists s', star Asm.step tge (State rs m) E0 s'
-             /\ match_internal (list_length_z (header bb)) (State rs m) s'.
-Proof.
-  intros.
-  exploit internal_functions_unfold; eauto.
-  intros (tc & FINDtf & TRANStf & _).
-  assert (BNDhead: list_length_z (header bb) <= 1). { eapply size_header; eauto. }
-  destruct (header bb) as [|l[|]] eqn: EQhead.
-  + (* header nil *)
-    eexists; split.
-    - eapply star_refl.
-    - split; eauto.
-      unfold list_length_z; rewrite !ATPC; simpl.
-      rewrite Ptrofs.add_zero; auto.
-  + (* header one *)
-    assert (Lhead: list_length_z (header bb) = 1). { rewrite EQhead; unfold list_length_z; simpl. auto. }
-    exploit (find_instr_bblock 0); eauto.
-    { generalize (bblock_size_pos bb). omega. }
-    intros (i & NTH & FIND_INSTR).
-    inv NTH.
-    * rewrite EQhead in H; simpl in H. inv H.
-      cutrewrite (Ptrofs.unsigned ofs + 0 = Ptrofs.unsigned ofs) in FIND_INSTR; try omega.
-      eexists. split.
-      - eapply star_one.
-        eapply Asm.exec_step_internal; eauto.
-        simpl; eauto.
-      - unfold list_length_z; simpl. split; eauto.
-        intros r; destruct r; simpl; congruence || auto.
-    * (* absurd case *)
-      erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; omega].
-    * (* absurd case *)
-      rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). omega.
-  + (* absurd case *)
-    unfold list_length_z in BNDhead. simpl in *.
-    generalize (list_length_z_aux_increase _ l1 2); omega.
-Qed.
-
-Lemma eval_addressing_preserved a rs1 rs2:
-  (forall r : preg, r <> PC -> rs1 r = rs2 r) ->
-  eval_addressing lk a rs1 = Asm.eval_addressing tge a rs2.
-Proof.
-  intros EQ.
-  destruct a; simpl; try (rewrite !EQ; congruence). auto.
-Qed.
-
-Ltac next_stuck_cong := try (unfold Next, Stuck in *; congruence).
-
-Ltac inv_ok_eq :=
-  repeat match goal with
-  | [EQ: OK ?x = OK ?y |- _ ]
-      => inversion EQ; clear EQ; subst
-  end.
-
-Ltac reg_rwrt :=
-  match goal with
-  | [e: DR _ = DR _ |- _ ]
-      => rewrite e in *
-  end.
-
-Ltac destruct_reg_inv :=
-  repeat match goal with
-  | [ H : match ?reg with _ => _ end = _ |- _ ]
-      => simpl in *; destruct reg; try congruence; try inv_ok_eq; try reg_rwrt
-  end.
-
-Ltac destruct_ireg_inv :=
-  repeat match goal with
-  | [ H : match ?reg with _ => _ end = _ |- _ ]
-      => destruct reg as [[r|]|]; try congruence; try inv_ok_eq; subst
-  end.
-
-Ltac destruct_reg_size :=
-  simpl in *;
-  match goal with
-  | [ |- context [ match ?reg with _ => _ end ] ]
-      => destruct reg; try congruence
-  end.
-
-Ltac find_rwrt_ag :=
-  simpl in *;
-  match goal with
-  | [ AG: forall r, r <> ?PC -> _ r = _ r |- _ ]
-      => repeat rewrite <- AG; try congruence
-  end.
-
-Ltac inv_matchi :=
-  match goal with
-  | [ MATCHI : match_internal _ _ _ |- _ ]
-      => inversion MATCHI; subst; find_rwrt_ag
-  end.
-
-Ltac destruct_ir0_reg :=
-  match goal with
-  | [ |- context [ ir0 _ _ ?r ] ]
-      => unfold ir0 in *; destruct r; find_rwrt_ag; eauto
-  end.
-
-Ltac pc_not_sp :=
-  match goal with
-  | [ |- ?PC <> ?SP ]
-      => destruct (PregEq.eq SP PC); repeat congruence; discriminate
-  end.
-
-Ltac update_x_access_x :=
-  subst; rewrite !Pregmap.gss; auto.
-
-Ltac update_x_access_r :=
-  rewrite !Pregmap.gso; auto.
-
-Lemma nextinstr_agree_but_pc rs1 rs2: forall
-  (AG: forall r, r <> PC -> rs1 r = rs2 r),
-  forall r, r <> PC -> rs1 r = Asm.nextinstr rs2 r.
-Proof.
-  intros; unfold Asm.nextinstr in *; rewrite Pregmap.gso in *; eauto.
-Qed.
-
-Lemma ptrofs_nextinstr_agree rs1 rs2 n: forall
-  (BOUNDED : 0 <= n <= Ptrofs.max_unsigned)
-  (AGPC : Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC),
-  Val.offset_ptr (rs1 PC) (Ptrofs.repr (n + 1)) = Asm.nextinstr rs2 PC.
-Proof.
-  intros; unfold Asm.nextinstr; rewrite Pregmap.gss.
-  rewrite <- Ptrofs.unsigned_one; rewrite <- (Ptrofs.unsigned_repr n); eauto;
-  rewrite <- Ptrofs.add_unsigned; rewrite <- Val.offset_ptr_assoc; rewrite AGPC; eauto.
-Qed.
-
-Lemma load_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a: forall
-  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
-  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
-  (HLOAD: exec_load lk chk f a rd rs1 m1 = Next rs1' m1'),
-  exists (rs2' : regset) (m2' : mem), Asm.exec_load tge chk f a rd rs2 m2 = Next rs2' m2'
-  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
-Proof.
-  intros.
-  unfold exec_load, Asm.exec_load in *.
-  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
-  rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
-  destruct (Mem.loadv _ _ _).
-  + inversion HLOAD; auto. repeat (econstructor; eauto).
-    * eapply nextinstr_agree_but_pc; intros.
-      destruct (PregEq.eq r rd); try update_x_access_x; try update_x_access_r.
-    * eapply ptrofs_nextinstr_agree; eauto.
-  + next_stuck_cong.
-Qed.
-
-Lemma store_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk a: forall
-  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
-  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
-  (HSTORE: exec_store lk chk a rd rs1 m1 = Next rs1' m1'),
-  exists (rs2' : regset) (m2' : mem), Asm.exec_store tge chk a rd rs2 m2 = Next rs2' m2'
-  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
-Proof.
-  intros.
-  unfold exec_store, Asm.exec_store in *.
-  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
-  rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
-  destruct (Mem.storev _ _ _ _).
-  + inversion HSTORE; auto. repeat (econstructor; eauto).
-    * eapply nextinstr_agree_but_pc; intros.
-      subst. apply EQR. auto.
-    * eapply ptrofs_nextinstr_agree; subst; eauto.
-  + next_stuck_cong.
-Qed.
-
-Lemma next_inst_preserved n rs1 m1 rs1' m1' rs2 m2 (x: dreg) v: forall
-  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
-  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
-  (NEXTI: Next rs1 # x <- v m1 = Next rs1' m1'),
-  exists (rs2' : regset) (m2' : mem),
-  Next (Asm.nextinstr rs2 # x <- v) m2 = Next rs2' m2'
-  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
-Proof.
-  intros.
-  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
-  inversion NEXTI. repeat (econstructor; eauto).
-  * eapply nextinstr_agree_but_pc; intros.
-    destruct (PregEq.eq r x); try update_x_access_x; try update_x_access_r.
-  * eapply ptrofs_nextinstr_agree; eauto.
-Qed.
-
-Lemma match_internal_nextinstr_switch:
-  forall n s rs2 m2 r v,
-  r <> PC ->
-  match_internal n s (State ((Asm.nextinstr rs2)#r <- v) m2) ->
-  match_internal n s (State (Asm.nextinstr (rs2#r <- v)) m2).
-Proof.
-  unfold Asm.nextinstr; intros n s rs2 m2 r v NOTPC1 MI.
-  inversion MI; subst; constructor; auto.
-  - eapply nextinstr_agree_but_pc; intros.
-    rewrite AG; try congruence.
-    destruct (PregEq.eq r r0); try update_x_access_x; try update_x_access_r.
-  - rewrite !Pregmap.gss, !Pregmap.gso; try congruence.
-    rewrite AGPC.
-    rewrite Pregmap.gso, Pregmap.gss; try congruence.
-Qed.
-
-Lemma match_internal_nextinstr_set_parallel:
-  forall n rs1 m1 rs2 m2 r v1 v2,
-  r <> PC ->
-  match_internal n (State rs1 m1) (State (Asm.nextinstr rs2) m2) ->
-  v1 = v2 ->
-  match_internal n (State (rs1#r <- v1) m1) (State (Asm.nextinstr (rs2#r <- v2)) m2).
-Proof.
-  intros; subst; eapply match_internal_nextinstr_switch; eauto.
-  intros; eapply match_internal_set_parallel; eauto.
-Qed.
-
-Lemma exec_basic_simulation:
-  forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi
-  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
-  (BASIC: exec_basic lk ge bi rs1 m1 = Next rs1' m1')
-  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
-  (TRANSBI: basic_to_instruction bi = OK tbi),
-  exists rs2' m2', Asm.exec_instr tge tf tbi
-                                  rs2 m2 = Next rs2' m2'
-                   /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
-Proof.
-  intros.
-  destruct bi.
-  { (* PArith *)
-    simpl in *; destruct i.
-    1,2,3,4,5,6: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *)
-      destruct i;
-      try (destruct sumbool_rec; try congruence);
-      try (monadInv TRANSBI);
-      try (destruct_reg_inv);
-      try (inv_matchi);
-      try (exploit next_inst_preserved; eauto);
-      try (repeat destruct_reg_size);
-      try (destruct_ir0_reg).
-    { (* PArithComparisonPP *)
-      destruct i;
-      try (monadInv TRANSBI);
-      try (inv_matchi);
-      try (destruct_reg_inv);
-      simpl in *.
-      1,2: (* compare_long *)
-        inversion BASIC; clear BASIC; subst;
-        eexists; eexists; split; eauto;
-        unfold compare_long;
-        repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
-        try (econstructor; eauto);
-        try (eapply nextinstr_agree_but_pc; eauto);
-        try (eapply ptrofs_nextinstr_agree; eauto).
-
-      destruct sz.
-      - (* compare_single *)
-        unfold compare_single in BASIC.
-        destruct (rs1 x), (rs1 x0);
-        inversion BASIC;
-        eexists; eexists; split; eauto;
-        repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
-        try (econstructor; eauto);
-        try (eapply nextinstr_agree_but_pc; eauto);
-        try (eapply ptrofs_nextinstr_agree; eauto).
-      - (* compare_float *)
-        unfold compare_float in BASIC.
-        destruct (rs1 x), (rs1 x0);
-        inversion BASIC;
-        eexists; eexists; split; eauto;
-        repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
-        try (econstructor; eauto);
-        try (eapply nextinstr_agree_but_pc; eauto);
-        try (eapply ptrofs_nextinstr_agree; eauto). }
-    1,2: (* PArithComparisonR0R, PArithComparisonP *)
-      destruct i;
-      try (monadInv TRANSBI);
-      try (inv_matchi);
-      try (destruct_reg_inv);
-      try (destruct_reg_size);
-      simpl in *;
-      inversion BASIC; clear BASIC; subst;
-      eexists; eexists; split; eauto;
-      unfold compare_long, compare_int, compare_float, compare_single;
-      try (destruct_reg_size);
-      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
-      try (econstructor; eauto);
-      try (destruct_ir0_reg);
-      try (eapply nextinstr_agree_but_pc; eauto);
-      try (eapply ptrofs_nextinstr_agree; eauto).
-    { (* Pcset *)
-      try (monadInv TRANSBI);
-      try (inv_matchi).
-      try (exploit next_inst_preserved; eauto);
-      try (simpl in *; intros;
-      unfold if_opt_bool_val in *; unfold eval_testcond in *;
-      rewrite <- !AG; try congruence; eauto). }
-    { (* Pfmovi *)
-      try (monadInv TRANSBI);
-      try (inv_matchi);
-      try (destruct_reg_size);
-      try (destruct_ir0_reg);
-      try (exploit next_inst_preserved; eauto). }
-    { (* Pcsel *)
-      try (destruct_reg_inv);
-      try (monadInv TRANSBI);
-      try (destruct_reg_inv);
-      try (inv_matchi);
-      try (exploit next_inst_preserved; eauto);
-      simpl in *; intros;
-      unfold if_opt_bool_val in *; unfold eval_testcond in *;
-      rewrite <- !AG; try congruence; eauto. }
-    { (* Pfnmul *)
-      try (monadInv TRANSBI);
-      try (inv_matchi);
-      try (destruct_reg_size);
-      try (exploit next_inst_preserved; eauto);
-      try (find_rwrt_ag). } }
-  { (* PLoad *)
-    destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_preserved; eauto;
-    intros; simpl in *; destruct sz; eauto. }
-  { (* PStore *)
-    destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto;
-    simpl in *; inv_matchi; find_rwrt_ag. }
-  { (* Pallocframe *)
-    monadInv TRANSBI;
-    inv_matchi; try pc_not_sp;
-    destruct sz eqn:EQSZ;
-    destruct Mem.alloc eqn:EQALLOC;
-    destruct Mem.store eqn:EQSTORE; inversion BASIC; try pc_not_sp;
-    eexists; eexists; split; eauto;
-    repeat (eapply match_internal_nextinstr_set_parallel; [ try (pc_not_sp; congruence) | idtac | try (reflexivity)]);
-    try (econstructor; eauto);
-    try (eapply nextinstr_agree_but_pc; eauto);
-    try (eapply ptrofs_nextinstr_agree; eauto). }
-  { (* Pfreeframe *)
-    monadInv TRANSBI;
-    inv_matchi; try pc_not_sp;
-    destruct sz eqn:EQSZ;
-    destruct Mem.loadv eqn:EQLOAD;
-    destruct (rs1 SP) eqn:EQRS1SP;
-    try (destruct Mem.free eqn:EQFREE);
-    inversion BASIC; try pc_not_sp;
-    eexists; eexists; split; eauto;
-    repeat (eapply match_internal_nextinstr_set_parallel; [ try (pc_not_sp; congruence) | idtac | try (reflexivity)]);
-    try (econstructor; eauto);
-    try (eapply nextinstr_agree_but_pc; eauto);
-    try (eapply ptrofs_nextinstr_agree; eauto). }
-  1,2,3,4: (* Ploadsymbol, Pcvtsw2x, Pcvtuw2x, Pcvtx2w *)
-    try (monadInv TRANSBI);
-    try (inv_matchi);
-    try (exploit next_inst_preserved; eauto);
-    rewrite symbol_addresses_preserved; eauto;
-    try (find_rwrt_ag).
-Qed.
-
-Lemma find_basic_instructions b ofs f bb tc: forall
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (UNFOLD: unfold (fn_blocks f) = OK tc),
-  forall n,
-  (n < length (body bb))%nat ->
-  exists (i : Asm.instruction) (bi : basic),
-     list_nth_z (body bb) (Z.of_nat n) = Some bi
-  /\ basic_to_instruction bi = OK i
-  /\ Asm.find_instr (Ptrofs.unsigned ofs
-                     + (list_length_z (header bb))
-                     + Z.of_nat n) tc
-                     = Some i.
-Proof.
-  intros until n; intros NLT.
-  exploit internal_functions_unfold; eauto.
-  intros (tc' & FINDtf & TRANStf & _).
-  assert (tc' = tc) by congruence; subst.
-    exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto.
-    { unfold size; split.
-      - rewrite list_length_z_nat; omega.
-      - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). omega. }
-    intros (i & NTH & FIND_INSTR).
-    exists i; intros.
-    inv NTH.
-    - (* absurd *) apply list_nth_z_range in H; omega.
-    - exists bi;
-      rewrite Z.add_simpl_l in H;
-      rewrite Z.add_assoc in FIND_INSTR;
-      intuition.
-    - (* absurd *) rewrite bblock_size_aux in H0;
-      rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; omega.
-Qed.
-
-(** "is_tail" auxiliary lemma about is_tail to move in IterList ou Coqlib (déplacer aussi Machblockgenproof.is_tail_app_inv) ? *)
-
-Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1).
-Proof.
-  intros; eapply Machblockgenproof.is_tail_app_inv; econstructor.
-Qed.
-
-Lemma is_tail_app_def A (l1 l2: list A):
-  is_tail l1 l2 -> exists l3, l2 = l3 ++ l1.
-Proof.
-  induction 1 as [|x l1 l2]; simpl.
-  - exists nil; simpl; auto.
-  - destruct IHis_tail as (l3 & EQ); rewrite EQ.
-    exists (x::l3); simpl; auto.
-Qed.
-
-Lemma is_tail_bound A (l1 l2: list A):
-  is_tail l1 l2 -> (length l1 <= length l2)%nat.
-Proof.
-  intros H; destruct (is_tail_app_def _ _ _ H) as (l3 & EQ).
-  subst; rewrite app_length.
-  omega.
-Qed.
-
-Lemma is_tail_list_nth_z A (l1 l2: list A):
-  is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
-Proof.
-  induction 1; simpl.
-  - replace (list_length_z c - list_length_z c) with 0; omega || auto.
-  - assert (X: list_length_z (i :: c2) > list_length_z c1).
-    { rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
-      exploit is_tail_bound; simpl; eauto.
-      omega. }
-    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega.
-    replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
-    rewrite list_length_z_cons.
-    omega.
-Qed.
-
-(* TODO: remplacer find_basic_instructions directement par ce lemme ? *)
-Lemma find_basic_instructions_alt b ofs f bb tc n: forall
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (UNFOLD: unfold (fn_blocks f) = OK tc)
-  (BOUND: 0 <= n < list_length_z (body bb)),
-  exists (i : Asm.instruction) (bi : basic),
-     list_nth_z (body bb) n = Some bi
-  /\ basic_to_instruction bi = OK i
-  /\ Asm.find_instr (Ptrofs.unsigned ofs
-                     + (list_length_z (header bb))
-                     + n) tc
-                     = Some i.
-Proof.
-  intros; assert ((Z.to_nat n) < length (body bb))%nat.
-  { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try omega. }
-  exploit find_basic_instructions; eauto.
-  rewrite Z2Nat.id; try omega. intros (i & bi & X).
-  eexists; eexists; intuition eauto.
-Qed.
-
-Lemma header_body_tail_bound: forall (a: basic) (li: list basic) bb ofs
-  (BOUNDBB : Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
-  (BDYLENPOS : 0 <= list_length_z (body bb) - list_length_z (a :: li) <
-              list_length_z (body bb)),
-0 <= list_length_z (header bb) + list_length_z (body bb) - list_length_z (a :: li) <=
-Ptrofs.max_unsigned.
-Proof.
-  intros.
-  assert (HBBPOS: list_length_z (header bb) >= 0) by eapply list_length_z_pos.
-  assert (HBBSIZE: list_length_z (header bb) < size bb) by eapply header_size_lt_block_size.
-  assert (OFSBOUND: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2.
-  assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by omega.
-  unfold size in BBSIZE.
-  rewrite !Nat2Z.inj_add in BBSIZE.
-  rewrite <- !list_length_z_nat in BBSIZE.
-  omega.
-Qed.
-
-(* A more general version of the exec_body_simulation_plus lemma below.
-   This generalization is necessary for the induction proof inside the body.
-*)
-Lemma exec_body_simulation_plus_gen li: forall b ofs f bb rs m s2 rs' m'
-  (BLI: is_tail li (body bb))
-  (ATPC: rs PC = Vptr b ofs)
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (NEMPTY_BODY: li <> nil)
-  (MATCHI: match_internal ((list_length_z (header bb)) + (list_length_z (body bb)) - (list_length_z li)) (State rs m) s2)
-  (BODY: exec_body lk ge li rs m = Next rs' m'),
-  exists s2', plus Asm.step tge s2 E0 s2'
-             /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'.
-Proof.
-  induction li as [|a li]; simpl; try congruence.
-  intros.
-  assert (BDYLENPOS: 0 <= (list_length_z (body bb) - list_length_z (a::li)) < list_length_z (body bb)). {
-    assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try omega.
-    rewrite !list_length_z_nat; split.
-    - rewrite <- Nat2Z.inj_lt. simpl. omega.
-    - rewrite <- Nat2Z.inj_le; eapply is_tail_bound; eauto.
-  }
-  exploit internal_functions_unfold; eauto.
-  intros (tc & FINDtf & TRANStf & _).
-  exploit find_basic_instructions_alt; eauto.
-  intros (tbi & (bi & (NTHBI & TRANSBI & FIND_INSTR))).
-  exploit is_tail_list_nth_z; eauto.
-  rewrite NTHBI; simpl.
-  intros X; inversion X; subst; clear X NTHBI.
-  destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong.
-  destruct s as (rs1 & m1); simpl in *.
-  destruct s2 as (rs2 & m2); simpl in *.
-  assert (BOUNDBBMAX: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
-  by (eapply size_of_blocks_bounds; eauto).
-  exploit header_body_tail_bound; eauto. intros BDYTAIL.
-  exploit exec_basic_simulation; eauto.
-  intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT).
-  exploit exec_basic_dont_move_PC; eauto. intros AGPC.
-  inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS'].
-  subst A. subst B. subst C. subst D. subst E.
-  rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT.
-
-  inv MATCHI. symmetry in AGPC0.
-  rewrite ATPC in AGPC0.
-  unfold Val.offset_ptr in AGPC0.
-
-  simpl in FIND_INSTR.
-  (* Execute internal step. *)
-  exploit (Asm.exec_step_internal tge b); eauto.
-  {
-    rewrite Ptrofs.add_unsigned.
-    repeat (rewrite Ptrofs.unsigned_repr); try omega.
-    2: {
-      assert (BOUNDOFS: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2.
-      assert (list_length_z (body bb) <= size bb) by eapply body_size_le_block_size.
-      assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. }
-      omega. }
-    try rewrite list_length_z_nat; try split;
-    simpl; rewrite <- !list_length_z_nat;
-    replace (Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb) -
-      list_length_z (a :: li))) with (Ptrofs.unsigned ofs + list_length_z (header bb) +
-      (list_length_z (body bb) - list_length_z (a :: li))) by omega;
-    try assumption; try omega. }
-
-  (* This is our STEP hypothesis. *)
-  intros STEP_NEXT.
-  destruct li as [|a' li]; simpl in *.
-  - (* case of a single instruction in li: this our base case in the induction *)
-    inversion BODY; subst.
-    eexists; split.
-    + apply plus_one. eauto.
-    + constructor; auto.
-      rewrite ATPC_NEXT.
-      apply f_equal.
-      apply f_equal.
-      rewrite bblock_size_aux, list_length_z_cons; simpl.
-      omega.
-  - exploit (IHli b ofs f bb rs1 m_next' (State rs_next' m_next')); congruence || eauto.
-    + exploit is_tail_app_def; eauto.
-      intros (l3 & EQ); rewrite EQ.
-      exploit (is_tail_app_right _ (l3 ++ a::nil)).
-      rewrite <- app_assoc; simpl; eauto.
-    + constructor; auto.
-      rewrite ATPC_NEXT.
-      apply f_equal.
-      apply f_equal.
-      rewrite! list_length_z_cons; simpl.
-      omega.
-    + intros (s2' & LAST_STEPS & LAST_MATCHS).
-      eexists. split; eauto.
-      eapply plus_left'; eauto.
-Qed.
-
-Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall
-  (ATPC: rs PC = Vptr b ofs)
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (NEMPTY_BODY: body bb <> nil)
-  (MATCHI: match_internal (list_length_z (header bb)) (State rs m) s2)
-  (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
-  exists s2', plus Asm.step tge s2 E0 s2'
-             /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'.
-Proof.
-  intros.
-  exploit exec_body_simulation_plus_gen; eauto.
-  - constructor.
-  - replace (list_length_z (header bb) + list_length_z (body bb) - list_length_z (body bb)) with (list_length_z (header bb)); auto.
-    omega.
-Qed.
-
-Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall
-  (ATPC: rs PC = Vptr b ofs)
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (MATCHI: match_internal (list_length_z (header bb)) (State rs m) s2)
-  (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
-  exists s2', star Asm.step tge s2 E0 s2'
-             /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'.
-Proof.
-  intros.
-  destruct (body bb) eqn: Hbb.
-  - simpl in BODY. inv BODY.
-    eexists. split.
-    eapply star_refl; eauto.
-    assert (EQ: (size bb - Z.of_nat (length_opt (exit bb))) = list_length_z (header bb)).
-    {  rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. omega. }
-    rewrite EQ; eauto.
-  - exploit exec_body_simulation_plus; congruence || eauto.
-    { rewrite Hbb; eauto. }
-    intros (s2' & PLUS & MATCHI').
-    eexists; split; eauto.
-    eapply plus_star; eauto.
-Qed.
-
-Lemma list_nth_z_range_exceeded A (l : list A) n:
-  n >= list_length_z l ->
-  list_nth_z l n = None.
-Proof.
-  intros N.
-  remember (list_nth_z l n) as opt eqn:H. symmetry in H.
-  destruct opt; auto.
-  exploit list_nth_z_range; eauto. omega.
-Qed.
-
-Lemma label_in_header_list lbl a:
-  is_label lbl a = true -> list_length_z (header a) <= 1 -> header a = lbl :: nil.
-Proof.
-  intros.
-  eapply is_label_correct_true in H.
-  destruct (header a).
-  - eapply in_nil in H. contradiction.
-  - rewrite list_length_z_cons in H0.
-    assert (list_length_z l0 >= 0) by eapply list_length_z_pos.
-    assert (list_length_z l0 = 0) by omega.
-    rewrite list_length_z_nat in H2.
-    assert (Datatypes.length l0 = 0%nat) by omega.
-    eapply length_zero_iff_nil in H3. subst.
-    unfold In in H. destruct H.
-    + subst; eauto.
-    + destruct H.
-Qed.
-
-Lemma no_label_in_basic_inst: forall a lbl x,
-  basic_to_instruction a = OK x -> Asm.is_label lbl x = false.
-Proof.
-  intros.
-  destruct a; simpl in *;
-  repeat destruct i; simpl in *;
-  try (try destruct_reg_inv; monadInv H; simpl in *; reflexivity).
-Qed.
-
-Lemma label_pos_body bdy: forall c1 c2 z ex lbl
-  (HUNF : unfold_body bdy = OK c2),
-  Asm.label_pos lbl (z + Z.of_nat ((Datatypes.length bdy) + length_opt ex)) c1 = Asm.label_pos lbl (z) ((c2 ++ unfold_exit ex) ++ c1).
-Proof.
-  induction bdy.
-  - intros. inversion HUNF. simpl in *.
-    destruct ex eqn:EQEX.
-    + simpl in *. unfold Asm.is_label. destruct c; simpl; try congruence.
-      destruct i; simpl; try congruence.
-    + simpl in *. ring_simplify (z + 0). auto.
-  - intros. inversion HUNF; clear HUNF. monadInv H0. simpl in *.
-    erewrite no_label_in_basic_inst; eauto. rewrite <- IHbdy; eauto.
-    erewrite Zpos_P_of_succ_nat.
-    apply f_equal2; auto. omega.
-Qed.
-
-Lemma asm_label_pos_header: forall z a x0 x1 lbl
-  (HUNF: unfold_body (body a) = OK x1),
-  Asm.label_pos lbl (z + size a) x0 =
-  Asm.label_pos lbl (z + list_length_z (header a)) ((x1 ++ unfold_exit (exit a)) ++ x0).
-Proof.
-  intros.
-  unfold size.
-  rewrite <- plus_assoc. rewrite Nat2Z.inj_add.
-  rewrite list_length_z_nat.
-  replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by omega.
-  eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto.
-Qed.
-
-Lemma header_size_cons_nil: forall (l0: label) (l1: list label)
-  (HSIZE: list_length_z (l0 :: l1) <= 1),
-  l1 = nil.
-Proof.
-  intros.
-  destruct l1; try congruence. rewrite !list_length_z_cons in HSIZE.
-  assert (list_length_z l1 >= 0) by eapply list_length_z_pos.
-  assert (list_length_z l1 + 1 + 1 >= 2) by omega.
-  assert (2 <= 1) by omega. contradiction H1. omega.
-Qed.
-
-Lemma label_pos_preserved_gen bbs: forall lbl c z
-  (HUNF: unfold bbs = OK c),
-  label_pos lbl z bbs = Asm.label_pos lbl z c.
-Proof.
-  induction bbs.
-  - intros. simpl in *. inversion HUNF. simpl. reflexivity.
-  - intros. simpl in *. monadInv HUNF. unfold unfold_bblock in EQ.
-    destruct (zle _ _); try congruence. monadInv EQ.
-    destruct (is_label _ _) eqn:EQLBL.
-    + erewrite label_in_header_list; eauto.
-      simpl in *. destruct (peq lbl lbl); try congruence.
-    + erewrite IHbbs; eauto.
-      rewrite (asm_label_pos_header z a x0 x1 lbl); auto.
-      unfold is_label in *.
-      destruct (header a).
-      * replace (z + list_length_z (@nil label)) with (z); eauto.
-        unfold list_length_z. simpl. omega.
-      * eapply header_size_cons_nil in l as HL1.
-        subst. simpl in *. destruct (in_dec _ _); try congruence.
-        simpl in *.
-        destruct (peq _ _); try intuition congruence.
-Qed.
-
-Lemma label_pos_preserved f lbl z tf: forall
-  (FINDF: transf_function f = OK tf),
-  label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf).
-Proof.
-  intros.
-  eapply label_pos_preserved_gen.
-  unfold transf_function in FINDF. monadInv FINDF.
-  destruct zlt; try congruence. inversion EQ0. eauto.
-Qed.
-
-Lemma goto_label_preserved bb rs1 m1 rs1' m1' rs2 m2 lbl f tf v: forall
-  (FINDF: transf_function f = OK tf)
-  (BOUNDED: size bb <= Ptrofs.max_unsigned)
-  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2))
-  (HGOTO: goto_label f lbl (incrPC v rs1) m1 = Next rs1' m1'),
-  exists (rs2' : regset) (m2' : mem), Asm.goto_label tf lbl rs2 m2 = Next rs2' m2'
-  /\ match_states (State rs1' m1') (State rs2' m2').
-Proof.
-  intros.
-  unfold goto_label, Asm.goto_label in *.
-  rewrite <- (label_pos_preserved f); auto.
-  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
-  destruct label_pos; next_stuck_cong.
-  destruct (incrPC v rs1 PC) eqn:INCRPC; next_stuck_cong.
-  inversion HGOTO; auto. repeat (econstructor; eauto).
-  rewrite <- EQPC.
-  unfold incrPC in *.
-  rewrite !Pregmap.gss in *.
-  destruct (rs1 PC) eqn:EQRS1; simpl in *; try congruence.
-  replace (rs2 # PC <- (Vptr b0 (Ptrofs.repr z))) with ((rs1 # PC <- (Vptr b0 (Ptrofs.add i0 v))) # PC <- (Vptr b (Ptrofs.repr z))); auto.
-  eapply functional_extensionality. intros.
-  destruct (PregEq.eq x PC); subst.
-  rewrite !Pregmap.gss. congruence.
-  rewrite !Pregmap.gso; auto.
-Qed.
-
-Lemma next_inst_incr_pc_preserved bb rs1 m1 rs1' m1' rs2 m2 f tf: forall
-  (FINDF: transf_function f = OK tf)
-  (BOUNDED: size bb <= Ptrofs.max_unsigned)
-  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2))
-  (NEXT: Next (incrPC (Ptrofs.repr (size bb)) rs1) m2 = Next rs1' m1'),
-  exists (rs2' : regset) (m2' : mem),
-  Next (Asm.nextinstr rs2) m2 = Next rs2' m2'
-  /\ match_states (State rs1' m1') (State rs2' m2').
-Proof.
-  intros; simpl in *; unfold incrPC in NEXT;
-  inv_matchi;
-  assert (size bb >= 1) by eapply bblock_size_pos;
-  assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by omega;
-  inversion NEXT; subst;
-  eexists; eexists; split; eauto.
-  assert (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))) = Asm.nextinstr rs2). {
-    unfold Pregmap.set. apply functional_extensionality.
-    intros x. destruct (PregEq.eq x PC).
-    -- unfold Asm.nextinstr. rewrite <- AGPC.
-       rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned.
-       rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega.
-       rewrite Ptrofs.unsigned_one.
-       replace (size bb - 1 + 1) with (size bb) by omega.
-       rewrite e. rewrite Pregmap.gss.
-       reflexivity.
-    -- eapply nextinstr_agree_but_pc; eauto. }
-       rewrite H1. econstructor.
-Qed.
-
-Lemma pc_reg_overwrite: forall (r: ireg) rs1 m1 rs2 m2 bb
-  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)),
-  rs2 # PC <- (rs2 r) =
-  (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb)))) # PC <-
-  (rs1 r).
-Proof.
-  intros.
-  unfold Pregmap.set; apply functional_extensionality.
-  intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate; inv_matchi.
-Qed.
-
-Lemma exec_cfi_simulation:
-  forall bb f tf rs1 m1 rs1' m1' rs2 m2 cfi
-  (SIZE: size bb <= Ptrofs.max_unsigned)
-  (FINDF: transf_function f = OK tf)
-  (* Warning: Asmblock's PC is assumed to be already pointing on the next instruction ! *)
-  (CFI: exec_cfi ge f cfi (incrPC (Ptrofs.repr (size bb)) rs1) m1 = Next rs1' m1')
-  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)),
-  exists rs2' m2', Asm.exec_instr tge tf (cf_instruction_to_instruction cfi)
-                                  rs2 m2 = Next rs2' m2'
-                   /\ match_states (State rs1' m1') (State rs2' m2').
-Proof.
-  intros.
-  assert (BBPOS: size bb >= 1) by eapply bblock_size_pos.
-  destruct cfi; inv CFI; simpl.
-  - (* Pb *)
-    exploit goto_label_preserved; eauto.
-  - (* Pbc *)
-    inv_matchi.
-    unfold eval_testcond in *. destruct c;
-    erewrite !incrPC_agree_but_pc in H0; try rewrite <- !AG; try congruence.
-    all:
-      destruct_reg_size;
-      try destruct b eqn:EQB.
-      1,4,7,10,13,16,19,22,25,28,31,34:
-        exploit goto_label_preserved; eauto.
-      1,3,5,7,9,11,13,15,17,19,21,23:
-        exploit next_inst_incr_pc_preserved; eauto.
-      all: repeat (econstructor; eauto).
-  - (* Pbl *)
-    eexists; eexists; split; eauto.
-    assert ( ((incrPC (Ptrofs.repr (size bb)) rs1) # X30 <- (incrPC (Ptrofs.repr (size bb)) rs1 PC))
-                                                   # PC <-  (Genv.symbol_address ge id Ptrofs.zero)
-           = (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one))
-                           # PC <- (Genv.symbol_address tge id Ptrofs.zero)
-           ) as EQRS. {
-      unfold incrPC. unfold Pregmap.set. simpl. apply functional_extensionality.
-      intros x. destruct (PregEq.eq x PC).
-      * rewrite symbol_addresses_preserved. reflexivity.
-      * destruct (PregEq.eq x X30).
-        -- inv MATCHI. rewrite <- AGPC. rewrite Val.offset_ptr_assoc.
-           unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try omega.
-           replace (size bb - 1 + 1) with (size bb) by omega. reflexivity.
-        -- inv MATCHI; rewrite AG; try assumption; reflexivity.
-    } rewrite EQRS; inv MATCHI; reflexivity.
-  - (* Pbs *)
-    eexists; eexists; split; eauto.
-    assert ( (incrPC (Ptrofs.repr (size bb)) rs1) # PC <-
-                           (Genv.symbol_address ge id Ptrofs.zero)
-           = rs2 # PC <- (Genv.symbol_address tge id Ptrofs.zero)
-           ) as EQRS. {
-      unfold incrPC, Pregmap.set. rewrite symbol_addresses_preserved. inv MATCHI.
-      apply functional_extensionality. intros x. destruct (PregEq.eq x PC); auto.
-    } rewrite EQRS; inv MATCHI; reflexivity.
-  - (* Pblr *)
-    eexists; eexists; split; eauto.
-    unfold incrPC. rewrite Pregmap.gss. rewrite Pregmap.gso; try discriminate.
-    assert ( (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) # PC <- (rs2 r)
-           = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))))
-                   # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))))
-                   # PC <- (rs1 r)
-           ) as EQRS. {
-      unfold Pregmap.set. apply functional_extensionality.
-      intros x; destruct (PregEq.eq x PC) as [X | X].
-      - inv_matchi; rewrite AG; auto.
-      - destruct (PregEq.eq x X30) as [X' | X'].
-        + inversion MATCHI; subst. rewrite <- AGPC.
-          rewrite Val.offset_ptr_assoc. unfold Ptrofs.one.
-          rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try omega. rewrite Ptrofs.unsigned_repr; try omega.
-          rewrite Z.sub_add; reflexivity.
-        + inv_matchi.
-    } rewrite EQRS. inv_matchi.
-  - (* Pbr *)
-    eexists; eexists; split; eauto.
-    unfold incrPC. rewrite Pregmap.gso; try discriminate.
-    rewrite (pc_reg_overwrite r rs1 m1' rs2 m2 bb); auto.
-    inv_matchi.
-  - (* Pret *)
-    eexists; eexists; split; eauto.
-    unfold incrPC. rewrite Pregmap.gso; try discriminate.
-    rewrite (pc_reg_overwrite r rs1 m1' rs2 m2 bb); auto.
-    inv_matchi.
-  - (* Pcbnz *)
-    inv_matchi.
-    unfold eval_neg_branch in *.
-    erewrite incrPC_agree_but_pc in H0; try congruence.
-    destruct eval_testzero; next_stuck_cong.
-    destruct b.
-    * exploit next_inst_incr_pc_preserved; eauto.
-    * exploit goto_label_preserved; eauto.
-  - (* Pcbz *)
-    inv_matchi.
-    unfold eval_branch in *.
-    erewrite incrPC_agree_but_pc in H0; try congruence.
-    destruct eval_testzero; next_stuck_cong.
-    destruct b.
-    * exploit goto_label_preserved; eauto.
-    * exploit next_inst_incr_pc_preserved; eauto.
-  - (* Ptbnbz *)
-    inv_matchi.
-    unfold eval_branch in *.
-    erewrite incrPC_agree_but_pc in H0; try congruence.
-    destruct eval_testbit; next_stuck_cong.
-    destruct b.
-    * exploit goto_label_preserved; eauto.
-    * exploit next_inst_incr_pc_preserved; eauto.
-  - (* Ptbz *)
-    inv_matchi.
-    unfold eval_neg_branch in *.
-    erewrite incrPC_agree_but_pc in H0; try congruence.
-    destruct eval_testbit; next_stuck_cong.
-    destruct b.
-    * exploit next_inst_incr_pc_preserved; eauto.
-    * exploit goto_label_preserved; eauto.
-  - (* Pbtbl *)
-    assert (rs2 # X16 <- Vundef r1 = (incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef r1)
-    as EQUNDEFX16. {
-      unfold incrPC, Pregmap.set.
-      destruct (PregEq.eq r1 X16) as [X16 | X16]; auto.
-      destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate.
-      inv MATCHI; rewrite AG; auto.
-    } rewrite <- EQUNDEFX16 in H0.
-    destruct_reg_inv; next_stuck_cong.
-    unfold goto_label, Asm.goto_label in *.
-    rewrite <- (label_pos_preserved f); auto.
-    inversion MATCHI; subst.
-    destruct label_pos; next_stuck_cong.
-    destruct (((incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef) # X17 <- Vundef PC) eqn:INCRPC; next_stuck_cong.
-    inversion H0; auto. repeat (econstructor; eauto).
-    rewrite !Pregmap.gso; try congruence.
-    rewrite <- AGPC.
-    unfold incrPC in *.
-    destruct (rs1 PC) eqn:EQRS1; simpl in *; try discriminate.
-    replace (((rs2 # X16 <- Vundef) # X17 <- Vundef) # PC <- (Vptr b0 (Ptrofs.repr z))) with
-      ((((rs1 # PC <- (Vptr b0 (Ptrofs.add i1 (Ptrofs.repr (size bb))))) # X16 <-
-      Vundef) # X17 <- Vundef) # PC <- (Vptr b (Ptrofs.repr z))); auto.
-    eapply functional_extensionality; intros x.
-    destruct (PregEq.eq x PC); subst.
-    + rewrite Pregmap.gso in INCRPC; try congruence.
-      rewrite Pregmap.gso in INCRPC; try congruence.
-      rewrite Pregmap.gss in INCRPC.
-      rewrite !Pregmap.gss in *; congruence.
-    + rewrite Pregmap.gso; auto.
-      rewrite (Pregmap.gso (i := x) (j := PC)); auto.
-      destruct (PregEq.eq x X17); subst.
-      * rewrite !Pregmap.gss; auto.
-      * rewrite !(Pregmap.gso (i := x) (j:= X17)); auto. destruct (PregEq.eq x X16); subst.
-        -- rewrite !Pregmap.gss; auto.
-        -- rewrite !Pregmap.gso; auto.
-Qed.
-
-Lemma last_instruction_cannot_be_label bb:
-  list_nth_z (header bb) (size bb - 1) = None.
-Proof.
-  assert (list_length_z (header bb) <= size bb - 1). {
-    rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). omega.
-  }
-  remember (list_nth_z (header bb) (size bb - 1)) as label_opt; destruct label_opt; auto;
-  exploit list_nth_z_range; eauto; omega.
-Qed.
-
-Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m
-  (ATPC : rs PC = Vptr b ofs)
-  (MATCHI : match_internal (size bb - 1)
-            {| _rs := rs; _m := m |}
-            {| _rs := _rs; _m := _m |}),
-  _rs PC = Vptr b (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))).
-Proof.
-  intros; inv MATCHI. rewrite <- AGPC; rewrite ATPC; unfold Val.offset_ptr; eauto.
-Qed.
-
-Lemma find_instr_ofs_somei: forall ofs bb f tc asmi rs m _rs _m
-  (BOUNDOFS : Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
-  (FIND_INSTR : Asm.find_instr (Ptrofs.unsigned ofs + (size bb - 1)) tc =
-                Some (asmi))
-  (MATCHI : match_internal (size bb - 1)
-            {| _rs := rs; _m := m |}
-            {| _rs := _rs; _m := _m |}),
-  Asm.find_instr (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
-    (Asm.fn_code {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}) =
-  Some (asmi).
-Proof.
-  intros; simpl.
-  replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
-          with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption.
-  generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros.
-  unfold Ptrofs.add.
-  rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega.
-  rewrite Ptrofs.unsigned_repr; omega.
-Qed.
-
-Lemma eval_builtin_arg_match: forall rs _m _rs a1 b1
-  (AG : forall r : preg, r <> PC -> rs r = _rs r)
-  (EVAL : eval_builtin_arg tge (fun r : dreg => rs r) (rs SP) _m a1 b1),
-  eval_builtin_arg tge _rs (_rs SP) _m (map_builtin_arg DR a1) b1.
-Proof.
-  intros; induction EVAL; simpl in *; try rewrite AG; try rewrite AG in EVAL; try discriminate; try congruence; eauto with barg.
-  econstructor. rewrite <- AG; try discriminate; auto.
-Qed.
-
-Lemma eval_builtin_args_match: forall bb rs m _rs _m args vargs
-  (MATCHI : match_internal (size bb - 1)
-            {| _rs := rs; _m := m |}
-            {| _rs := _rs; _m := _m |})
-  (EVAL : eval_builtin_args tge (fun r : dreg => rs r) (rs SP) m args vargs),
-  eval_builtin_args tge _rs (_rs SP) _m (map (map_builtin_arg DR) args) vargs.
-Proof.
-  intros; inv MATCHI.
-  induction EVAL; subst.
-  - econstructor.
-  - econstructor.
-    + eapply eval_builtin_arg_match; eauto.
-    + eauto.
-Qed.
-
-Lemma pc_both_sides: forall (rs _rs: regset) v
-  (AG : forall r : preg, r <> PC -> rs r = _rs r),
-  rs # PC <- v = _rs # PC <- v.
-Proof.
-  intros; unfold Pregmap.set; apply functional_extensionality; intros y.
-  destruct (PregEq.eq y PC); try rewrite AG; eauto.
-Qed.
-
-Lemma set_buitin_res_sym res: forall vres rs _rs r
-  (NPC: r <> PC)
-  (AG : forall r : preg, r <> PC -> rs r = _rs r),
-  set_res res vres rs r = set_res res vres _rs r.
-Proof.
-  induction res; simpl; intros; unfold Pregmap.set; try rewrite AG; eauto.
-Qed.
-
-Lemma set_builtin_res_dont_move_pc_gen res: forall vres rs _rs v1 v2
-  (HV: v1 = v2)
-  (AG : forall r : preg, r <> PC -> rs r = _rs r),
-  (set_res res vres rs) # PC <- v1 =
-  (set_res res vres _rs) # PC <- v2.
-Proof.
-  intros. rewrite HV. generalize res vres rs _rs AG v2.
-  clear res vres rs _rs AG v1 v2 HV.
-  induction res.
-  - simpl; intros. apply pc_both_sides; intros.
-    unfold Pregmap.set; try rewrite AG; eauto.
-  - simpl; intros; apply pc_both_sides; eauto.
-  - simpl; intros.
-    erewrite IHres2; eauto; intros.
-    eapply set_buitin_res_sym; eauto.
-Qed.
-
-Lemma set_builtin_map_not_pc (res: builtin_res dreg): forall vres rs,
-  set_res (map_builtin_res DR res) vres rs PC = rs PC.
-Proof.
-  induction res.
-  - intros; simpl. unfold Pregmap.set. destruct (PregEq.eq PC x); try congruence.
-  - intros; simpl; congruence.
-  - intros; simpl in *. rewrite IHres2. rewrite IHres1. reflexivity.
-Qed.
-
-Lemma undef_reg_preserved (rl: list mreg): forall rs _rs r
-  (NPC: r <> PC)
-  (AG : forall r : preg, r <> PC -> rs r = _rs r),
-  undef_regs (map preg_of rl) rs r = undef_regs (map preg_of rl) _rs r.
-Proof.
-  induction rl.
-  - simpl; auto.
-  - simpl; intros. erewrite IHrl; eauto.
-    intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of a)); try rewrite AG; eauto.
-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.
-
-Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (NEMPTY_EXIT: exit bb <> None)
-  (MATCHI: match_internal (size bb - Z.of_nat (length_opt (exit bb))) (State rs m) s2)
-  (EXIT: exec_exit ge f (Ptrofs.repr (size bb)) rs m (exit bb) t rs' m')
-  (ATPC: rs PC = Vptr b ofs),
-  plus Asm.step tge s2 t (State rs' m').
-Proof.
-  intros.
-  exploit internal_functions_unfold; eauto.
-  intros (tc & FINDtf & TRANStf & _).
-
-  exploit (find_instr_bblock (size bb - 1)); eauto.
-  { generalize (bblock_size_pos bb). omega. }
-  intros (i' & NTH & FIND_INSTR).
-
-  inv NTH.
-  + rewrite last_instruction_cannot_be_label in *. discriminate.
-  + destruct (exit bb) as [ctrl |] eqn:NEMPTY_EXIT'. 2: { contradiction. }
-    rewrite bblock_size_aux in *. rewrite NEMPTY_EXIT' in *. simpl in *.
-    (* XXX: Is there a better way to simplify this expression i.e. automatically? *)
-    replace (list_length_z (header bb) + list_length_z (body bb) + 1 - 1 -
-       list_length_z (header bb)) with (list_length_z (body bb)) in H by omega.
-    rewrite list_nth_z_range_exceeded in H; try omega. discriminate.
-  + assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned). {
-      eapply size_of_blocks_bounds; eauto.
-    }
-    assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); omega. }
-    destruct cfi.
-    * (* control flow instruction *)
-      destruct s2.
-      rewrite H in EXIT. (* exit bb is a cfi *)
-      inv EXIT.
-      rewrite H in MATCHI. simpl in MATCHI.
-      exploit internal_functions_translated; eauto.
-      rewrite FINDtf.
-      intros (tf & FINDtf' & TRANSf). inversion FINDtf'; subst; clear FINDtf'.
-      exploit exec_cfi_simulation; eauto.
-      (* extract exec_cfi_simulation's conclusion as separate hypotheses *)
-      intros (rs2' & m2' & EXECI & MATCHS); rewrite MATCHS.
-      apply plus_one.
-      eapply Asm.exec_step_internal; eauto.
-      - eapply pc_ptr_exec_step; eauto.
-      - eapply find_instr_ofs_somei; eauto.
-    * (* builtin *)
-      destruct s2.
-      rewrite H in EXIT.
-      rewrite H in MATCHI. simpl in MATCHI.
-      simpl in FIND_INSTR.
-      inversion EXIT.
-      apply plus_one.
-      eapply external_call_symbols_preserved in H10; try (apply senv_preserved).
-      eapply eval_builtin_args_preserved in H6; try (apply symbols_preserved).
-      eapply Asm.exec_step_builtin; eauto.
-      - eapply pc_ptr_exec_step; eauto.
-      - eapply find_instr_ofs_somei; eauto.
-      - eapply eval_builtin_args_match; eauto.
-      - inv MATCHI; eauto.
-      - inv MATCHI.
-        unfold Asm.nextinstr, incrPC.
-        assert (HPC: Val.offset_ptr (rs PC) (Ptrofs.repr (size bb))
-                   = Val.offset_ptr (_rs PC) Ptrofs.one).
-        { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr.
-          rewrite Ptrofs.add_assoc. unfold Ptrofs.add.
-          assert (BBPOS: size bb >= 1) by eapply bblock_size_pos.
-          rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega.
-          rewrite Ptrofs.unsigned_one.
-          replace (size bb - 1 + 1) with (size bb) by omega.
-          reflexivity. }
-        apply set_builtin_res_dont_move_pc_gen.
-        -- erewrite !set_builtin_map_not_pc.
-           erewrite !undef_regs_other_2.
-           rewrite HPC; auto. all: rewrite preg_notin_charact; intros; try discriminate.
-        -- intros. eapply undef_reg_preserved; eauto.
-Qed.
-
-Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (MATCHI: match_internal (size bb - Z.of_nat (length_opt (exit bb))) (State rs m) s2)
-  (EXIT: exec_exit ge f (Ptrofs.repr (size bb)) rs m (exit bb) t rs' m')
-  (ATPC: rs PC = Vptr b ofs),
-  star Asm.step tge s2 t (State rs' m').
-Proof.
-  intros.
-  destruct (exit bb) eqn: Hex.
-  - eapply plus_star.
-    eapply exec_exit_simulation_plus; try rewrite Hex; congruence || eauto.
-  - inv MATCHI.
-    inv EXIT.
-    assert (X: rs2 = incrPC (Ptrofs.repr (size bb)) rs). {
-      unfold incrPC. unfold Pregmap.set.
-        apply functional_extensionality. intros x.
-        destruct (PregEq.eq x PC) as [X|].
-        - rewrite X. rewrite <- AGPC. simpl.
-          replace (size bb - 0) with (size bb) by omega. reflexivity.
-        - rewrite AG; try assumption. reflexivity.
-    }
-    destruct X.
-    subst; eapply star_refl; eauto.
-Qed.
-
-Lemma exec_bblock_simulation b ofs f bb t rs m rs' m': forall
-  (ATPC: rs PC = Vptr b ofs)
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (EXECBB: exec_bblock lk ge f bb rs m t rs' m'),
-  plus Asm.step tge (State rs m) t (State rs' m').
-Proof.
-  intros; destruct EXECBB as (rs1 & m1 & BODY & CTL).
-  exploit exec_header_simulation; eauto.
-  intros (s0 & STAR & MATCH0).
-  eapply star_plus_trans; traceEq || eauto.
-  destruct (bblock_non_empty bb).
-  - (* body bb <> nil *)
-     exploit exec_body_simulation_plus; eauto.
-     intros (s1 & PLUS & MATCH1).
-     eapply plus_star_trans; traceEq || eauto.
-     eapply exec_exit_simulation_star; eauto.
-     erewrite <- exec_body_dont_move_PC; eauto.
-  - (* exit bb <> None *)
-     exploit exec_body_simulation_star; eauto.
-     intros (s1 & STAR1 & MATCH1).
-     eapply star_plus_trans; traceEq || eauto.
-     eapply exec_exit_simulation_plus; eauto.
-     erewrite <- exec_body_dont_move_PC; eauto.
-Qed.
-
-Lemma step_simulation s t s':
-  Asmblock.step lk ge s t s' -> plus Asm.step tge s t s'.
-Proof.
-  intros STEP.
-  inv STEP; simpl; exploit functions_translated; eauto;
-  intros (tf0 & FINDtf & TRANSf);
-  monadInv TRANSf.
-  - (* internal step *) eapply exec_bblock_simulation; eauto.
-  - (* external step *)
-    apply plus_one.
-    exploit external_call_symbols_preserved; eauto. apply senv_preserved.
-    intros ?.
-    eapply Asm.exec_step_external; eauto.
-Qed.
-
-Lemma transf_program_correct:
-  forward_simulation (Asmblock.semantics lk prog) (Asm.semantics tprog).
-Proof.
-  eapply forward_simulation_plus.
-  - apply senv_preserved.
-  - eexact transf_initial_states.
-  - eexact transf_final_states.
-  - (* TODO step_simulation *)
-    unfold match_states.
-    simpl; intros; subst; eexists; split; eauto.
-    eapply step_simulation; eauto.
-Qed.
-
-End PRESERVATION.
-
-End Asmblock_PRESERVATION.
-
-
-Local Open Scope linking_scope.
-
-Definition block_passes :=
-      mkpass Machblockgenproof.match_prog
-  ::: mkpass PseudoAsmblockproof.match_prog
-  ::: mkpass Asmblockgenproof.match_prog
-  (*::: mkpass PostpassSchedulingproof.match_prog*)
-  ::: mkpass Asmblock_PRESERVATION.match_prog
-  ::: pass_nil _.
-
-Definition match_prog := pass_match (compose_passes block_passes).
-
-Lemma transf_program_match:
-  forall p tp, Asmgen.transf_program p = OK tp -> match_prog p tp.
-Proof.
-  intros p tp H.
-  unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
-  inversion_clear H. apply bind_inversion in H1. destruct H1.
-  inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
-  unfold match_prog; simpl.
-  exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
-  exists x; split. apply PseudoAsmblockproof.transf_program_match; auto.
-  exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
-  exists tp; split. apply Asmblock_PRESERVATION.transf_program_match; auto. auto.
-Qed.
-
-(** Return Address Offset *)
-
-Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
-  Machblockgenproof.Mach_return_address_offset (PseudoAsmblockproof.rao Asmblockgenproof.next).
-
-Lemma return_address_exists:
-  forall f sg ros c, is_tail (Mach.Mcall sg ros :: c) f.(Mach.fn_code) ->
-  exists ra, return_address_offset f c ra.
-Proof.
-  intros; eapply Machblockgenproof.Mach_return_address_exists; eauto.
-Admitted.
-
-Section PRESERVATION.
-
-Variable prog: Mach.program.
-Variable tprog: Asm.program.
-Hypothesis TRANSF: match_prog prog tprog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-Theorem transf_program_correct:
-  forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
-Proof.
-  unfold match_prog in TRANSF. simpl in TRANSF.
-  inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
-  eapply compose_forward_simulations.
-  { exploit Machblockgenproof.transf_program_correct; eauto. }
-  eapply compose_forward_simulations.
-  + apply PseudoAsmblockproof.transf_program_correct; eauto.
-    - intros; apply Asmblockgenproof.next_progress.
-    - intros; eapply Asmblockgenproof.functions_bound_max_pos; eauto.
-      { intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. }
-  + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
-    { intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. }
-     apply Asmblock_PRESERVATION.transf_program_correct. eauto.
-Qed.
-
-End PRESERVATION.
-
-Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes).
-
-(*******************************************)
-(* Stub actually needed by driver/Compiler *)
-
-Module Asmgenproof0.
-
-Definition return_address_offset := return_address_offset.
-
-End Asmgenproof0.