fix aarch64 merge?

1 files changed, 2318 insertions, 0 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
new file mode 100644
index 00000000..d27b3f8c
--- /dev/null
+++ b/aarch64/Asmgenproof.v
@@ -0,0 +1,2318 @@
+(* *************************************************************)
+(*                                                             *)
+(*             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 Asm Asmblock.
+Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
+Require Import Asmgen.
+Require Import Axioms.
+Require Import IterList.
+Require Import Ring Lia.
+
+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.
+  lia.
+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; lia.
+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; lia.
+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; lia.
+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.
+  - lia.
+  - generalize (IHl (Z.succ acc)). lia.
+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 || lia);
+  unfold list_length_z; simpl;
+  generalize (list_length_z_aux_increase _ tl 1); lia.
+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).
+    lia.
+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 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; lia.
+  - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; lia.
+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; lia.
+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)).
+  lia.
+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); lia.
+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.
+      lia.
+    + 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).
+      lia.
+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'. lia.
+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); lia.
+  exploit IHc; eauto. lia.
+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). lia.
+    + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia.
+      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. }
+  lia.
+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. lia.
+     + 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 lia.
+       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 lia. 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 lia.
+      generalize (list_length_z_pos ll). intros.
+      rewrite list_nth_z_neg in H; try lia. 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 lia.
+      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. lia.
+  - 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 lia.
+      eapply IHl; lia.
+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. lia.
+  - 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). { lia. }
+      assert (0 <= n - 1). { lia. }
+      generalize (IHl (n - 1)). intros IH.
+      assert (n - 1 >= list_length_z l). { auto. }
+      assert (n > list_length_z l); lia.
+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 lia.
+      simpl in H. destruct (zeq n 0). { contradiction. }
+      replace (Z.pred n) with (n - 1) in H by lia.
+      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 lia.
+      simpl in NTH. destruct (zeq n 0). { contradiction. }
+      replace (Z.pred n) with (n - 1)  in NTH by lia.
+      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). { lia. }
+  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)). { lia. }
+  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)). { lia. }
+  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;
+    try destruct (negb _); rewrite <- BASIC;
+    repeat rewrite Pregmap.gso; try discriminate; reflexivity.
+  - destruct i; simpl in BASIC. 
+    1,2: 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 ld.
+    + unfold exec_load_rd_a in BASIC.
+      destruct Mem.loadv. 2: { discriminate BASIC. }
+      inv BASIC. rewrite Pregmap.gso; try discriminate; auto.
+    + unfold exec_load_double, is_pair_addressing_mode_correct in BASIC.
+      destruct a; try discriminate BASIC.
+      do 2 (destruct Mem.loadv; try discriminate BASIC).
+      inv BASIC. rewrite Pregmap.gso; try discriminate; auto.
+  - unfold exec_store in BASIC.
+    destruct st.
+    + unfold exec_store_rs_a in BASIC.
+      destruct Mem.storev. 2: { discriminate BASIC. }
+      inv BASIC; reflexivity.
+    + unfold exec_store_double in BASIC.
+      destruct a; try discriminate BASIC.
+      do 2 (destruct Mem.storev; try 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.
+  - inv BASIC; 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)). { lia. }
+              assert (n = size bb - 1). {
+                unfold size. rewrite <- EXIT. simpl.
+                repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. lia.
+              }
+              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 *) lia.
+           ++ (* absurd *)
+              unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE.
+              destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. lia.
+    + 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 lia.
+        eapply find_instr_bblock_tail; try assumption.
+        replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by lia.
+        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). lia. }
+    intros (i & NTH & FIND_INSTR).
+    inv NTH.
+    * rewrite EQhead in H; simpl in H. inv H.
+      replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by lia.
+      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; lia].
+    * (* absurd case *)
+      rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). lia.
+  + (* absurd case *)
+    unfold list_length_z in BNDhead. simpl in *.
+    generalize (list_length_z_aux_increase _ l1 2); lia.
+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_rd_a_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_rd_a 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_rd_a, 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 load_double_preserved n rs1 m1 rs1' m1' rs2 m2 rd1 rd2 chk1 chk2 f a: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (HLOAD: exec_load_double lk chk1 chk2 f a rd1 rd2 rs1 m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), Asm.exec_load_double tge chk1 chk2 f a rd1 rd2 rs2 m2 = Next rs2' m2'
+  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  unfold exec_load_double, Asm.exec_load_double in *.
+  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
+  erewrite <- !eval_addressing_preserved; eauto.
+  destruct (is_pair_addressing_mode_correct a); try discriminate.
+  destruct (Mem.loadv _ _ _);
+  destruct (Mem.loadv chk2 m2
+      (eval_addressing lk
+         (get_offset_addr a match chk1 with
+                            | Mint32 | Mfloat32| Many32 => 4
+                            | _ => 8
+                            end) rs1));
+  inversion HLOAD; auto.
+  repeat (econstructor; eauto).
+  * eapply nextinstr_agree_but_pc; intros.
+    destruct (PregEq.eq r rd2); destruct (PregEq.eq r rd1).
+    - try update_x_access_x. 
+    - try update_x_access_x.
+    - subst; repeat rewrite Pregmap.gso, Pregmap.gss; auto.
+    - try update_x_access_r.
+  * eapply ptrofs_nextinstr_agree; eauto.
+Qed.
+
+Lemma store_rs_a_preserved n rs1 m1 rs1' m1' rs2 m2 v chk a: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (HSTORE: exec_store_rs_a lk chk a v rs1 m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), Asm.exec_store tge chk a v rs2 m2 = Next rs2' m2'
+  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  unfold exec_store_rs_a, 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 store_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk1 chk2 a: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (HSTORE: exec_store_double lk chk1 chk2 a v1 v2 rs1 m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), Asm.exec_store_double tge chk1 chk2 a v1 v2 rs2 m2 = Next rs2' m2'
+  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  unfold exec_store_double, Asm.exec_store_double in *.
+  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
+  erewrite <- !eval_addressing_preserved; eauto.
+  destruct (is_pair_addressing_mode_correct a); try discriminate.
+  destruct (Mem.storev _ _ _ _);
+  try destruct (Mem.storev chk2 m
+             (eval_addressing lk
+                (get_offset_addr a
+                   match chk1 with
+                   | Mint32 | Mfloat32 | Many32 => 4
+                   | _ => 8
+                   end) rs1) v2);
+  inversion HSTORE; auto.
+  repeat (econstructor; eauto).
+  * eapply nextinstr_agree_but_pc; intros.
+    subst. apply EQR. auto.
+  * eapply ptrofs_nextinstr_agree; subst; eauto.
+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: {
+      destruct i.
+      1,2,3: 
+        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).
+      1,2: (* Special case for Pfmovimmd / Pfmovimms *)
+        try (monadInv TRANSBI);
+        try (destruct_reg_inv);
+        try (inv_matchi);
+        inversion BASIC; clear BASIC; subst;
+        try (destruct (is_immediate_float64 _));
+        try (destruct (is_immediate_float32 _));
+        eexists; eexists; split; eauto;
+        repeat (eapply match_internal_nextinstr_set_parallel; try congruence);
+        try (econstructor; eauto);
+        try (eapply nextinstr_agree_but_pc; eauto);
+        try (eapply ptrofs_nextinstr_agree; eauto).
+    }
+    1,2,3,4,5: (* 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.
+    - destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_rd_a_preserved; eauto;
+      intros; simpl in *; destruct sz; eauto.
+    - destruct ld; monadInv TRANSBI; destruct rd1 as [[rd1'|]|]; destruct rd2 as [[rd2'|]|];
+      inv EQ; inv EQ1; exploit load_double_preserved; eauto. }
+  { (* PStore *)
+    destruct st.
+    - destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_rs_a_preserved; eauto;
+      simpl in *; inv_matchi; find_rwrt_ag.
+    - destruct st; monadInv TRANSBI; destruct rs0 as [[rs0'|]|]; destruct rs3 as [[rs3'|]|];
+      inv EQ; inv EQ1; exploit store_double_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).
+  { (* Pnop *)
+    monadInv TRANSBI; inv_matchi. 
+    inversion BASIC.
+    repeat (econstructor; eauto).
+    eapply nextinstr_agree_but_pc; intros;
+    try rewrite <- H0, AG; auto.
+    try eapply ptrofs_nextinstr_agree; auto; rewrite <- H0;
+    assumption. }
+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; lia.
+      - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). lia. }
+    intros (i & NTH & FIND_INSTR).
+    exists i; intros.
+    inv NTH.
+    - (* absurd *) apply list_nth_z_range in H; lia.
+    - 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; lia.
+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 lia. }
+  exploit find_basic_instructions; eauto.
+  rewrite Z2Nat.id; try lia. 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 lia.
+  unfold size in BBSIZE.
+  rewrite !Nat2Z.inj_add in BBSIZE.
+  rewrite <- !list_length_z_nat in BBSIZE.
+  lia.
+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 lia.
+    rewrite !list_length_z_nat; split.
+    - rewrite <- Nat2Z.inj_lt. simpl. lia.
+    - 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 lia.
+    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. }
+      lia. }
+    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 lia;
+    try assumption; try lia. }
+
+  (* 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.
+      lia.
+  - 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.
+      lia.
+    + 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.
+    lia.
+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. lia. }
+    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. lia.
+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 lia.
+    rewrite list_length_z_nat in H2.
+    assert (Datatypes.length l0 = 0%nat) by lia.
+    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;
+  repeat destruct ld; repeat destruct st;
+  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. lia.
+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 lia.
+  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 lia.
+  assert (2 <= 1) by lia. contradiction H1. lia.
+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. lia.
+      * 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 lia;
+  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 lia.
+       rewrite Ptrofs.unsigned_one.
+       replace (size bb - 1 + 1) with (size bb) by lia.
+       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 lia.
+           replace (size bb - 1 + 1) with (size bb) by lia. 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 lia. rewrite Ptrofs.unsigned_repr; try lia.
+          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 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) # PC <- (Vptr b0 (Ptrofs.repr z))) with
+      (((rs1 # PC <- (Vptr b0 (Ptrofs.add i1 (Ptrofs.repr (size bb))))) # X16 <-
+      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.gss in INCRPC.
+      rewrite !Pregmap.gss in *; congruence.
+    + rewrite Pregmap.gso; auto.
+      rewrite (Pregmap.gso (i := x) (j := PC)); 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). lia.
+  }
+  remember (list_nth_z (header bb) (size bb - 1)) as label_opt; destruct label_opt; auto;
+  exploit list_nth_z_range; eauto; lia.
+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 lia.
+  rewrite Ptrofs.unsigned_repr; lia.
+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). lia. }
+  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 lia.
+    rewrite list_nth_z_range_exceeded in H; try lia. 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); lia. }
+    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 lia.
+          rewrite Ptrofs.unsigned_one.
+          replace (size bb - 1 + 1) with (size bb) by lia.
+          reflexivity. }
+        apply set_builtin_res_dont_move_pc_gen.
+        -- erewrite !set_builtin_map_not_pc.
+           erewrite !undef_regs_other.
+           rewrite HPC; auto.
+           all: intros; simpl in *; destruct H3 as [HX16 | [HX30 | HDES]]; subst; try discriminate;
+           exploit list_in_map_inv; eauto; intros [mr [A B]]; subst; discriminate.
+        -- intros. eapply undef_reg_preserved; eauto.
+           intros. destruct (PregEq.eq X16 r0); destruct (PregEq.eq X30 r0); subst.
+           rewrite Pregmap.gso, Pregmap.gss; try congruence.
+           do 2 (rewrite Pregmap.gso, Pregmap.gss; try discriminate; auto).
+           rewrite 2Pregmap.gss; auto.
+           rewrite !Pregmap.gso; auto.
+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 lia. 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.
+  - 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 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.
+  unfold Compopts.time in *. remember (Machblockgen.transf_program p) as mbp.
+  unfold match_prog; simpl.
+  exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
+  exists x; split. apply Asmblockgenproof.transf_program_match; auto.
+  exists x0; split. apply PostpassSchedulingproof.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 (Asmblockgenproof.return_address_offset).
+
+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; unfold return_address_offset; eapply Machblockgenproof.Mach_return_address_exists; eauto.
+  intros; eapply Asmblockgenproof.return_address_exists; eauto.
+Qed.
+
+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 Asmblockgenproof.transf_program_correct; eauto.
+    { intros.
+      unfold Genv.symbol_address.
+      erewrite <- PostpassSchedulingproof.symbols_preserved; eauto.
+      erewrite Asmblock_PRESERVATION.symbol_high_low; eauto.
+      reflexivity.
+    }
+  + eapply compose_forward_simulations.
+    - apply PostpassSchedulingproof.transf_program_correct; 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.