path: root/aarch64/Asmgenproof.v

(* *************************************************************)
(*                                                             *)
(*             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.

Lemma find_instr_bblock n pos lb tlb bb:
  find_bblock pos lb = Some bb ->
  unfold lb = OK tlb ->
  0 <= n < size bb ->
  exists i, is_nth_inst bb n i /\ Asm.find_instr (pos+n) tlb = Some i.
Admitted.

(* 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 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.
Admitted.

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 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 cf_instruction_simulated:
  forall size_b f tf rs1 m1 rs1' m1' cfi,
  (* there are no emnpty basic blocks *)
  size_b >= 1 ->
  exec_exit ge f (Ptrofs.repr size_b) rs1 m1 (Some (PCtlFlow cfi)) E0 rs1' m1' ->
  forall rs2 m2, match_internal (size_b - 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 size_b f tf rs1 m1 rs1' m1' cfi SIZE_B_GE_1 STEP rs2 m2 MI.
  destruct cfi; inv STEP; simpl in H0.
  - (* Pb *)
    simpl; eexists; eexists; split.
    + rewrite <- H0;
      unfold incrPC, Asm.goto_label, goto_label;
      inv MI; rewrite <- AGPC.
      (* TODO: show that Asm.label_pos and label_pos behave the same *
       *       show that both Val.offset_ptr calculation return Vptr _ _ *)
      admit.
    + constructor.
  - (* Pbc *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      (* TODO see Pb *)
      admit.
    + constructor.
  - (* Pbl *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      rewrite symbol_addresses_preserved.
      unfold incrPC.
      assert ( Val.offset_ptr (rs2 PC) Ptrofs.one
             = Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)
             ) as EQPC. {
        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.
      } rewrite EQPC.
      rewrite Pregmap.gss.
      assert (  (rs2 # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
                     # PC <-  (Genv.symbol_address ge id Ptrofs.zero)
             = ((rs1 # PC  <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
                     # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
                     # PC  <- (Genv.symbol_address ge id Ptrofs.zero)
             ) as EQRS. {
        unfold Pregmap.set.
        apply functional_extensionality.
        intros x. destruct (PregEq.eq x X30) as [X | X].
        - rewrite X. reflexivity.
        - destruct (PregEq.eq x PC) as [X' | X']; auto.
        inv MI. rewrite AG; auto.
      } rewrite EQRS. inv MI. reflexivity.
    + constructor.
  - (* Pbs *)
    simpl; eexists; eexists; split.
    + rewrite <- H0.
      rewrite symbol_addresses_preserved.
      unfold incrPC.
      assert ( (rs2 # PC <- (Genv.symbol_address ge id Ptrofs.zero))
             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
                    # PC <- (Genv.symbol_address ge id Ptrofs.zero)
             ) as EQRS. {
        unfold Pregmap.set; apply functional_extensionality. intros x.
        destruct (PregEq.eq x PC) as [X | X]; auto.
        inv MI; rewrite AG; auto.
      } rewrite EQRS; inv MI; auto.
    + constructor.
  - (* 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 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 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 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.
Admitted.

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 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_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'.
Admitted.

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

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