(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, 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 Asmblock.
Require Machblockgenproof Asmblockgenproof.
Require Import Asmgen.
Require Import Axioms.


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 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.
  - unfold list_length_z; simpl;
    rewrite list_length_add_acc, 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 length_agree). repeat (rewrite Nat2Z.inj_add). reflexivity.
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 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 length_agree; omega.
  - destruct (exit bb); try contradiction; simpl; repeat rewrite length_agree; omega.
Qed.

Lemma body_size_le_block_size bb:
  list_length_z (body bb) <= size bb.
Proof.
  rewrite bblock_size_aux; repeat rewrite length_agree; 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 length_agree.
  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 length_agree). 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 length_agree); rewrite app_length.
      rewrite Nat2Z.inj_add; repeat (rewrite <- length_agree).
      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 <- length_agree). 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 <- length_agree in UPPER). repeat (rewrite Nat2Z.inj_add in NGE).
              repeat (rewrite <- length_agree 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 <- length_agree). 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 exec_basic_simulation:
  forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi
  (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').
Admitted.

Lemma exec_body_simulation_star': forall
  b ofs f bb tc bis end_of_body rs_start m_start s_start rs_end m_end
  (ATPC: rs_start 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 (end_of_body - list_length_z bis) (State rs_start m_start) s_start)
  (BOUNDED: 0 <= Ptrofs.unsigned ofs + end_of_body <= Ptrofs.max_unsigned
            /\ list_length_z bis <= end_of_body)
  (UNFOLD: unfold (fn_blocks f) = OK tc)
  (FINDBI: forall n : nat, (n < length bis)%nat ->
          exists (i : Asm.instruction) (bi : basic),
             list_nth_z bis (Z.of_nat n) = Some bi
          /\ basic_to_instruction bi = OK i
          /\ Asm.find_instr (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis) + Z.of_nat n) tc = Some i)
  (BODY: exec_body lk ge bis rs_start m_start = Next rs_end m_end),
  exists s_end, star Asm.step tge s_start E0 s_end
             /\ match_internal end_of_body (State rs_end m_end) s_end.
Proof.
  induction bis as [| bi_next bis IH].
  - intros; eexists; split.
    + apply star_refl.
    + inv BODY;
      unfold list_length_z in MATCHI; simpl in MATCHI; rewrite Z.sub_0_r in MATCHI;
      assumption.
  - intros.
    exploit internal_functions_unfold; eauto.
    intros (x & FINDtf & TRANStf & _).
    assert (x = tc) by congruence; subst x.

    assert (FINDBI' := FINDBI).
    specialize (FINDBI' 0%nat).
    destruct FINDBI' as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))); try (simpl; omega).
    inversion NTHBI; subst bi_next'.
    simpl in BODY; destruct exec_basic as [s_next|] eqn:BASIC; try discriminate.

    destruct s_next as (rs_next & m_next); simpl in BODY.
    destruct s_start as (rs_start' & m_start').
    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 [? ? ? ? ? M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT OFS_NEXT RS RS']; subst.
    rewrite ATPC in AGPC; symmetry in AGPC, ATPC_NEXT.

    inversion MATCHI as [? ? ? ? ? M_AGREE RS_AGREE ATPC' OFS RS RS']; subst.
    symmetry in ATPC'. unfold list_length_z in ATPC'.
    simpl in ATPC'. rewrite list_length_add_acc in ATPC'.
    rewrite ATPC in ATPC'.
    unfold Val.offset_ptr in ATPC'.
    simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
    unfold list_length_z in FIND_INSTR; simpl in FIND_INSTR.
    rewrite list_length_add_acc in FIND_INSTR.

    destruct BOUNDED as [(? & LT_MAX) LT_END_OF_BODY].
    assert (list_length_z bis < end_of_body).
    { unfold list_length_z in LT_END_OF_BODY; simpl in LT_END_OF_BODY;
      rewrite list_length_add_acc in LT_END_OF_BODY; omega. }
    generalize (Ptrofs.unsigned_range_2 ofs); intros.
    exploit (Asm.exec_step_internal tge b
             (Ptrofs.add ofs (Ptrofs.repr (end_of_body - (list_length_z bis + 1))))
             {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}
             i_next rs_start' m_start'); eauto.
    { unfold Ptrofs.add; repeat (rewrite Ptrofs.unsigned_repr);
      try (split; try omega; rewrite length_agree; omega).
      rewrite Z.add_sub_assoc; assumption. }
    intros STEP_NEXT.

    unfold list_length_z in MI_NEXT; simpl in MI_NEXT.
    rewrite list_length_add_acc in MI_NEXT.
    (* XXX use better tactics *)
    replace (end_of_body - (list_length_z bis + 1) + 1)
       with (end_of_body - list_length_z bis) in MI_NEXT by omega.
    assert (0 <= Ptrofs.unsigned ofs + end_of_body <= Ptrofs.max_unsigned
            /\ list_length_z bis <= end_of_body). { split; omega. }
    exploit IH; eauto.
    { (* XXX *)
      intros n NLT.
      assert (NLT': (n + 1 < length (bi_next :: bis))%nat). { simpl; omega. }
      specialize (FINDBI (n + 1)%nat NLT').
      unfold list_length_z in FINDBI. simpl in FINDBI. rewrite list_length_add_acc in FINDBI.
      destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e. simpl in e. omega. }
      unfold list_length_z in FINDBI. simpl in FINDBI. rewrite list_length_add_acc in FINDBI.
      rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI. rewrite Z.add_0_r in FINDBI.
      replace (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis + 1) + (Z.of_nat n + 1))
         with (Ptrofs.unsigned ofs + end_of_body - list_length_z bis + Z.of_nat n) in FINDBI by omega.
      replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega.
      assumption. }
    intros IH'.
    destruct IH' as (? & STEP_REST & MATCH_REST).

    eexists; split.
    + eapply star_step; eauto.
    + info_auto.
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 length_agree; omega.
      - repeat (rewrite length_agree). 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 length_agree in H0; omega.
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 internal_functions_unfold; eauto.
  intros (tc & FINDtf & TRANStf & _).

  (* Prove an Asm.step given that body bb is not empty *)

  destruct (body bb) as [| bi bis] eqn:BDY; try contradiction.
  assert (H: (0 < length (body bb))%nat). { rewrite BDY; simpl; omega. }
  exploit find_basic_instructions; eauto. clear H. rewrite BDY; intros FINDBI.
  destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))).
  inversion NTHBI; subst bi_next'.
  simpl in BODY. destruct exec_basic as [s_next|] eqn:BASIC; try discriminate.

  destruct s_next as (rs_next & m_next); simpl in BODY.
  destruct s2 as (rs_start' & m_start').
  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.
  unfold list_length_z in AGPC0.
  simpl in AGPC0. rewrite list_length_add_acc in AGPC0.
  rewrite ATPC in AGPC0.
  unfold Val.offset_ptr in AGPC0.
  simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
  unfold list_length_z in FIND_INSTR; simpl in FIND_INSTR.
  rewrite list_length_add_acc in FIND_INSTR.
  rewrite Z.add_0_r in FIND_INSTR.
  rewrite Z.add_0_r in AGPC0.

  assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
    by (eapply size_of_blocks_bounds; eauto).
  generalize (header_size_lt_block_size bb). rewrite length_agree; intros HEADER_LT.
  generalize (Ptrofs.unsigned_range_2 ofs). intros (A & B).
  exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb)))))
           {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}
           i_next rs_start' m_start'); eauto.
  { unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr);
    try rewrite length_agree; try split; try omega.
    simpl; rewrite <- length_agree; assumption. }
  intros STEP_NEXT.

  (* Now, use exec_body_simulation_star' to go the rest of the way 0+ steps *)
  rewrite AGPC in ATPC_NEXT.
  unfold Val.offset_ptr in ATPC_NEXT.
  unfold Ptrofs.add in ATPC_NEXT.
  rewrite Ptrofs.unsigned_repr in ATPC_NEXT. 2: { rewrite length_agree; split; omega. }

  (* give omega more facts to work with *)
  assert (list_length_z (header bb) + list_length_z (body bb) <= size bb). {
    rewrite bblock_size_aux. omega. }
  generalize (body_size_le_block_size bb). rewrite length_agree. intros.
  assert (0 <= Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb))
            <= Ptrofs.max_unsigned
            /\ list_length_z bis <= list_length_z (header bb) + list_length_z (body bb)).
  { split; try omega. split; try omega.
    - rewrite length_agree in H0; repeat (rewrite length_agree); omega.
    - rewrite BDY. rewrite list_length_z_cons; repeat rewrite length_agree; omega. }

  exploit (exec_body_simulation_star' b ofs
           f bb tc bis (list_length_z (header bb) + list_length_z (body bb))); eauto.
  - rewrite BDY. unfold list_length_z. simpl.
    repeat (rewrite list_length_add_acc). repeat (rewrite Z.add_0_r).
    rewrite Z.add_assoc. rewrite Z.add_sub_swap. rewrite Z.add_simpl_r.
    apply MI_NEXT.
  - rewrite Z.add_assoc.
    intros n NBOUNDS.
    rewrite BDY.
    assert (NBOUNDS': (n + 1 < length (body bb))%nat). { rewrite BDY; simpl; omega. }
    exploit find_basic_instructions; eauto. rewrite BDY; intros FINDBI.
    simpl in FINDBI. destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e; simpl in e; omega. }
    rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI.
    replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega.
    rewrite list_length_z_cons, Z.add_assoc, Z.add_sub_swap, Z.add_simpl_r.
    replace (Ptrofs.unsigned ofs + list_length_z (header bb) + (Z.of_nat n + 1))
       with (Ptrofs.unsigned ofs + list_length_z (header bb) + 1 + Z.of_nat n) in FINDBI by omega.
    assumption.
  - intros (s_end & STAR_STEP & MI_STAR).
    eexists s_end; split.
    + eapply plus_left; eauto.
    + rewrite bblock_size_aux, Z.add_simpl_r. assumption.
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 exec_cfi_simulation:
  forall bb f tf rs1 m1 rs1' m1' rs2 m2 cfi
  (SIZE: size bb <= Ptrofs.max_unsigned)
  (* 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.
  destruct cfi; inv CFI; simpl.
  - (* Pb *) admit.
  - (* Pbc *) admit.
  - (* 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).
             ++ replace (size bb - 1 + 1) with (size bb) by omega. reflexivity.
             ++ split; try omega. apply one_le_max_unsigned.
             ++ generalize (bblock_size_pos bb); omega.
          -- 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 *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      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_b)))
                     # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
                     # PC <- (rs1 r)
             ) as EQRS. {
        unfold Pregmap.set. apply functional_extensionality.
        intros x; destruct (PregEq.eq x PC) as [X | X].
        - inv MI; rewrite AG; auto. discriminate.
        - destruct (PregEq.eq x X30) as [X' | X'].
          + inv MI. rewrite <- AGPC.
            rewrite Val.offset_ptr_assoc. unfold Ptrofs.one.
            rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
            rewrite Z.sub_add; reflexivity.
            * split; try omega. apply one_le_max_unsigned.
            * split; try omega.
              (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
          + inv MI; rewrite AG; auto.
      } rewrite EQRS. inv MI; auto.
    + constructor.
  - (* Pbr *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      unfold incrPC. rewrite Pregmap.gso; try discriminate.
      assert (  rs2 # PC <- (rs2 r)
             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
                    # PC <- (rs1 r)
             ) as EQRS. {
        unfold Pregmap.set; apply functional_extensionality.
        intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
        - inv MI; rewrite AG; try discriminate. reflexivity.
        - inv MI; rewrite AG; auto.
      } rewrite EQRS; inv MI; auto.
    + constructor.
  - (* Pret *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      unfold incrPC. rewrite Pregmap.gso; try discriminate.
      assert (  rs2 # PC <- (rs2 r)
             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) # PC <- (rs1 r)
             ) as EQRS. {
        unfold Pregmap.set; apply functional_extensionality.
        intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
        - inv MI; rewrite AG; try discriminate. reflexivity.
        - inv MI; rewrite AG; auto.
      } rewrite EQRS; inv MI; auto.
    + constructor.
  - (* Pcbnz *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      unfold eval_neg_branch. destruct sz.
      * simpl. inv MI. rewrite <- AG; try discriminate.
        replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs1 r). 2: {
          symmetry. rewrite incrPC_agree_but_pc; try discriminate; auto.
        }
        assert (Asm.nextinstr rs2 = (incrPC (Ptrofs.repr size_b) rs1)) as EQTrue. {
          unfold incrPC, Asm.nextinstr, Ptrofs.one. rewrite <- AGPC.
          rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned.
          rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
          - rewrite Z.sub_add; unfold Pregmap.set; apply functional_extensionality.
            intros x; destruct (PregEq.eq x PC) as [ X | X ]; auto. rewrite AG; trivial.
          - split; try omega. apply one_le_max_unsigned.
          - split; try omega.
            (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
        } rewrite EQTrue. fold Stuck.
          (* TODO show that Asm.goto_label and goto_label behave the same *) admit.
      * (* TODO see/merge above case *) admit.
    + constructor.
  - (* Pcbz *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      unfold eval_branch. (* TODO, will be very similar to Pcbnz *) admit.
    + constructor.
  - (* Pcbz *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      unfold eval_branch.
      replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs2 r). 2: {
          symmetry; rewrite incrPC_agree_but_pc; try discriminate; auto;
          inv MI; rewrite AG; try discriminate; auto.
      } (* TODO, cf. Pcbnz *) admit.
    + constructor.
  - (* Ptbz *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      (* TODO, cf. Pcbz *) admit.
    + constructor.
  - (* Pbtbl *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      assert (  rs2 # X16 <- Vundef r1
             = (incrPC (Ptrofs.repr size_b) 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 MI; rewrite AG; auto.
      } rewrite <- EQUNDEFX16.
      (* TODO Asm.goto_label and goto_label *) admit.
    + constructor.
*)
Admitted.

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 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 exec_cfi_simulation; eauto; intros.
      (* extract exec_cfi_simulation's conclusion as separate hypotheses *)
      destruct H3. destruct H3. destruct H3. rewrite H5.
      inversion MATCHI.
      apply plus_one.
      eapply Asm.exec_step_internal; eauto.
      - rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto.
      - 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.
    * (* 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.
      - inv MATCHI. rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto.
      - (* XXX copy-paste from case above *)
        simpl. replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
                  with (Ptrofs.unsigned ofs + (size bb - 1)); eauto.
        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.
      - simpl. (* TODO something like eval_builtin_args_match *) admit.
      - inv MATCHI; eauto.
      - rewrite H11. (* TODO lemmas for set_res, undef_regs ... *) admit.
Admitted.

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 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.