path: root/backend/PPCgenproof.v

(** Correctness proof for PPC generation: main proof. *)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Mach.
Require Import Machtyping.
Require Import PPC.
Require Import PPCgen.
Require Import PPCgenproof1.

Section PRESERVATION.

Variable prog: Mach.program.
Variable tprog: PPC.program.
Hypothesis TRANSF: transf_program prog = Some tprog.

Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall id, Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof.
  intros. unfold ge, tge. 
  apply Genv.find_symbol_transf_partial with transf_fundef.
  exact TRANSF. 
Qed.

Lemma functions_translated:
  forall f b,
  Genv.find_funct_ptr ge b = Some f ->
  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Some tf.
Proof.
  intros. 
  generalize (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF H).
  case (transf_fundef f). 
  intros f' [A B]. exists f'; split. assumption. auto.
  tauto.
Qed.

Lemma functions_transl:
  forall f b,
  Genv.find_funct_ptr ge b = Some (Internal f) ->
  Genv.find_funct_ptr tge b = Some (Internal (transl_function f)).
Proof.
  intros. 
  destruct (functions_translated _ _ H) as [tf [A B]].
  rewrite A. generalize B. unfold transf_fundef, transf_partial_fundef, transf_function.
  case (zlt Int.max_unsigned (code_size (transl_function f))); intro.
  congruence. auto.
Qed.

Lemma functions_transl_no_overflow:
  forall b f,
  Genv.find_funct_ptr ge b = Some (Internal f) ->
  code_size (transl_function f) <= Int.max_unsigned.
Proof.
  intros. 
  destruct (functions_translated _ _ H) as [tf [A B]].
  generalize B. unfold transf_fundef, transf_partial_fundef, transf_function.
  case (zlt Int.max_unsigned (code_size (transl_function f))); intro.
  congruence. intro; omega.
Qed.

(** * Properties of control flow *)

Lemma find_instr_in:
  forall c pos i,
  find_instr pos c = Some i -> In i c.
Proof.
  induction c; simpl. intros; discriminate.
  intros until i. case (zeq pos 0); intros.
  left; congruence. right; eauto.
Qed.

(** The ``code tail'' of an instruction list [c] is the list of instructions
  starting at PC [pos]. *)

Fixpoint code_tail (pos: Z) (c: code) {struct c} : code :=
  match c with
  | nil => nil
  | i :: il => if zeq pos 0 then c else code_tail (pos - 1) il
  end.

Lemma find_instr_tail:
  forall c pos,
  find_instr pos c =
    match code_tail pos c with nil => None | i1 :: il => Some i1 end.
Proof.
  induction c; simpl; intros.
  auto.
  case (zeq pos 0); auto.
Qed.

Remark code_size_pos:
  forall fn, code_size fn >= 0.
Proof.
  induction fn; simpl; omega.
Qed.

Remark code_tail_bounds:
  forall fn ofs i c,
  code_tail ofs fn = i :: c -> 0 <= ofs < code_size fn.
Proof.
  induction fn; simpl.
  intros; discriminate.
  intros until c. case (zeq ofs 0); intros.
  generalize (code_size_pos fn).  omega.
  generalize (IHfn _ _ _ H). omega.
Qed.

Remark code_tail_unfold:
  forall ofs i c,
  ofs >= 0 ->
  code_tail (ofs + 1) (i :: c) = code_tail ofs c.
Proof.
  intros. simpl. case (zeq (ofs + 1) 0); intros.
  omegaContradiction.
  replace (ofs + 1 - 1) with ofs. auto. omega.
Qed.

Remark code_tail_zero:
  forall fn, code_tail 0 fn = fn.
Proof.
  intros. destruct fn; simpl. auto. auto.
Qed.

Lemma code_tail_next:
  forall fn ofs i c,
  code_tail ofs fn = i :: c ->
  code_tail (ofs + 1) fn = c.
Proof.
  induction fn.
  simpl; intros; discriminate.
  intros until c. case (zeq ofs 0); intro.
  subst ofs. intros. rewrite code_tail_zero in H. injection H.
  intros. subst c. rewrite code_tail_unfold. apply code_tail_zero.
  omega.
  intro; generalize (code_tail_bounds _ _ _ _ H); intros [A B].
  assert (ofs = (ofs - 1) + 1). omega.
  rewrite H0 in H. rewrite code_tail_unfold in H.
  rewrite code_tail_unfold. rewrite H0. eauto.
  omega. omega. 
Qed.

Lemma code_tail_next_int:
  forall fn ofs i c,
  code_size fn <= Int.max_unsigned ->
  code_tail (Int.unsigned ofs) fn = i :: c ->
  code_tail (Int.unsigned (Int.add ofs Int.one)) fn = c.
Proof.
  intros. rewrite Int.add_unsigned. unfold Int.one. 
  repeat rewrite Int.unsigned_repr. apply code_tail_next with i; auto.
  compute; intuition congruence.
  generalize (code_tail_bounds _ _ _ _ H0). omega. 
  compute; intuition congruence.
Qed.

(** [transl_code_at_pc pc fn c] holds if the code pointer [pc] points
  within the PPC code generated by translating Mach function [fn],
  and [c] is the tail of the generated code at the position corresponding
  to the code pointer [pc]. *)

Inductive transl_code_at_pc: val -> Mach.function -> Mach.code -> Prop :=
  transl_code_at_pc_intro:
    forall b ofs f c,
    Genv.find_funct_ptr ge b = Some (Internal f) ->
    code_tail (Int.unsigned ofs) (transl_function f) = transl_code c ->
    transl_code_at_pc (Vptr b ofs) f c.

(** The following lemmas show that straight-line executions
  (predicate [exec_straight]) correspond to correct PPC executions
  (predicate [exec_steps]) under adequate [transl_code_at_pc] hypotheses. *)

Lemma exec_straight_steps_1:
  forall fn c rs m c' rs' m',
  exec_straight tge fn c rs m c' rs' m' ->
  code_size fn <= Int.max_unsigned ->
  forall b ofs,
  rs#PC = Vptr b ofs ->
  Genv.find_funct_ptr tge b = Some (Internal fn) ->
  code_tail (Int.unsigned ofs) fn = c ->
  exec_steps tge rs m E0 rs' m'.
Proof.
  induction 1.
  intros. apply exec_refl. 
  intros. apply exec_trans with E0 rs2 m2 E0.
  apply exec_one; econstructor; eauto. 
  rewrite find_instr_tail. rewrite H5. auto.
  apply IHexec_straight with b (Int.add ofs Int.one). 
  auto. rewrite H0. rewrite H3. reflexivity.
  auto. 
  apply code_tail_next_int with i; auto.
  traceEq.
Qed.
    
Lemma exec_straight_steps_2:
  forall fn c rs m c' rs' m',
  exec_straight tge fn c rs m c' rs' m' ->
  code_size fn <= Int.max_unsigned ->
  forall b ofs,
  rs#PC = Vptr b ofs ->
  Genv.find_funct_ptr tge b = Some (Internal fn) ->
  code_tail (Int.unsigned ofs) fn = c ->
  exists ofs',
     rs'#PC = Vptr b ofs'
  /\ code_tail (Int.unsigned ofs') fn = c'.
Proof.
  induction 1; intros.
  exists ofs. split. auto. auto.
  apply IHexec_straight with (Int.add ofs Int.one).
  auto. rewrite H0. rewrite H3. reflexivity. auto. 
  apply code_tail_next_int with i; auto.
Qed.

Lemma exec_straight_steps:
  forall f c c' rs m rs' m',
  transl_code_at_pc (rs PC) f c ->
  exec_straight tge (transl_function f)
                (transl_code c) rs m (transl_code c') rs' m' ->
  exec_steps tge rs m E0 rs' m' /\ transl_code_at_pc (rs' PC) f c'.
Proof.
  intros. inversion H.
  generalize (functions_transl_no_overflow _ _ H2). intro.
  generalize (functions_transl _ _ H2). intro.
  split. eapply exec_straight_steps_1; eauto. 
  generalize (exec_straight_steps_2 _ _ _ _ _ _ _
                H0 H6 _ _ (sym_equal H1) H7 H3).
  intros [ofs' [PC' CT']].
  rewrite PC'. constructor; auto.
Qed.

(** The [find_label] function returns the code tail starting at the
  given label.  A connection with [code_tail] is then established. *)

Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
  match c with
  | nil => None
  | instr :: c' =>
      if is_label lbl instr then Some c' else find_label lbl c'
  end.

Lemma label_pos_code_tail:
  forall lbl c pos c',
  find_label lbl c = Some c' ->
  exists pos',
  label_pos lbl pos c = Some pos' 
  /\ code_tail (pos' - pos) c = c'
  /\ pos < pos' <= pos + code_size c.
Proof.
  induction c. 
  simpl; intros. discriminate.
  simpl; intros until c'.
  case (is_label lbl a).
  intro EQ; injection EQ; intro; subst c'.
  exists (pos + 1). split. auto. split.
  rewrite zeq_false. replace (pos + 1 - pos - 1) with 0.
  apply code_tail_zero. omega. omega.
  generalize (code_size_pos c). omega. 
  intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
  exists pos'. split. auto. split.
  rewrite zeq_false. replace (pos' - pos - 1) with (pos' - (pos + 1)).
  auto. omega. omega. omega.
Qed.

(** The following lemmas show that the translation from Mach to PPC
  preserves labels, in the sense that the following diagram commutes:
<<
                          translation
        Mach code ------------------------ PPC instr sequence
            |                                          |
            | Mach.find_label lbl       find_label lbl |
            |                                          |
            v                                          v
        Mach code tail ------------------- PPC instr seq tail
                          translation
>>
  The proof demands many boring lemmas showing that PPC constructor
  functions do not introduce new labels.
*)

Section TRANSL_LABEL.

Variable lbl: label.

Remark loadimm_label:
  forall r n k, find_label lbl (loadimm r n k) = find_label lbl k.
Proof.
  intros. unfold loadimm. 
  case (Int.eq (high_s n) Int.zero). reflexivity. 
  case (Int.eq (low_s n) Int.zero). reflexivity.
  reflexivity.
Qed.
Hint Rewrite loadimm_label: labels.

Remark addimm_1_label:
  forall r1 r2 n k, find_label lbl (addimm_1 r1 r2 n k) = find_label lbl k.
Proof.
  intros; unfold addimm_1. 
  case (Int.eq (high_s n) Int.zero). reflexivity.
  case (Int.eq (low_s n) Int.zero). reflexivity. reflexivity.
Qed.
Remark addimm_2_label:
  forall r1 r2 n k, find_label lbl (addimm_2 r1 r2 n k) = find_label lbl k.
Proof.
  intros; unfold addimm_2. autorewrite with labels. reflexivity.
Qed.
Remark addimm_label:
  forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k.
Proof.
  intros; unfold addimm. 
  case (ireg_eq r1 GPR0); intro. apply addimm_2_label.
  case (ireg_eq r2 GPR0); intro. apply addimm_2_label.
  apply addimm_1_label.
Qed.
Hint Rewrite addimm_label: labels.

Remark andimm_label:
  forall r1 r2 n k, find_label lbl (andimm r1 r2 n k) = find_label lbl k.
Proof.
  intros; unfold andimm. 
  case (Int.eq (high_u n) Int.zero). reflexivity.
  case (Int.eq (low_u n) Int.zero). reflexivity.
  autorewrite with labels. reflexivity.
Qed.
Hint Rewrite andimm_label: labels.

Remark orimm_label:
  forall r1 r2 n k, find_label lbl (orimm r1 r2 n k) = find_label lbl k.
Proof.
  intros; unfold orimm. 
  case (Int.eq (high_u n) Int.zero). reflexivity.
  case (Int.eq (low_u n) Int.zero). reflexivity. reflexivity.
Qed.
Hint Rewrite orimm_label: labels.

Remark xorimm_label:
  forall r1 r2 n k, find_label lbl (xorimm r1 r2 n k) = find_label lbl k.
Proof.
  intros; unfold xorimm. 
  case (Int.eq (high_u n) Int.zero). reflexivity.
  case (Int.eq (low_u n) Int.zero). reflexivity. reflexivity.
Qed.
Hint Rewrite xorimm_label: labels.

Remark loadind_aux_label:
  forall base ofs ty dst k, find_label lbl (loadind_aux base ofs ty dst :: k) = find_label lbl k.
Proof.
  intros; unfold loadind_aux.
  case ty; reflexivity.
Qed.
Remark loadind_label:
  forall base ofs ty dst k, find_label lbl (loadind base ofs ty dst k) = find_label lbl k.
Proof.
  intros; unfold loadind. 
  case (Int.eq (high_s ofs) Int.zero). apply loadind_aux_label.
  transitivity (find_label lbl (loadind_aux GPR2 (low_s ofs) ty dst :: k)).
  reflexivity. apply loadind_aux_label.
Qed.
Hint Rewrite loadind_label: labels.
Remark storeind_aux_label:
  forall base ofs ty dst k, find_label lbl (storeind_aux base ofs ty dst :: k) = find_label lbl k.
Proof.
  intros; unfold storeind_aux.
  case dst; reflexivity.
Qed.
Remark storeind_label:
  forall base ofs ty src k, find_label lbl (storeind base src ofs ty k) = find_label lbl k.
Proof.
  intros; unfold storeind. 
  case (Int.eq (high_s ofs) Int.zero). apply storeind_aux_label.
  transitivity (find_label lbl (storeind_aux base GPR2 (low_s ofs) ty :: k)).
  reflexivity. apply storeind_aux_label.
Qed.
Hint Rewrite storeind_label: labels.
Remark floatcomp_label:
  forall cmp r1 r2 k, find_label lbl (floatcomp cmp r1 r2 k) = find_label lbl k.
Proof.
  intros; unfold floatcomp. destruct cmp; reflexivity.
Qed.

Remark transl_cond_label:
  forall cond args k, find_label lbl (transl_cond cond args k) = find_label lbl k.
Proof.
  intros; unfold transl_cond.
  destruct cond; (destruct args; 
  [try reflexivity | destruct args;
  [try reflexivity | destruct args; try reflexivity]]).
  case (Int.eq (high_s i) Int.zero). reflexivity. 
  autorewrite with labels; reflexivity.
  case (Int.eq (high_u i) Int.zero). reflexivity. 
  autorewrite with labels; reflexivity.
  apply floatcomp_label. apply floatcomp_label.
  apply andimm_label. apply andimm_label.
Qed.
Hint Rewrite transl_cond_label: labels.
Remark transl_op_label:
  forall op args r k, find_label lbl (transl_op op args r k) = find_label lbl k.
Proof.
  intros; unfold transl_op;
  destruct op; destruct args; try (destruct args); try (destruct args); try (destruct args);
  try reflexivity; autorewrite with labels; try reflexivity.
  case (mreg_type m); reflexivity.
  case (mreg_type r); reflexivity.
  case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity.
  case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity.
  case (snd (crbit_for_cond c)); reflexivity.
  case (snd (crbit_for_cond c)); reflexivity.
  case (snd (crbit_for_cond c)); reflexivity.
  case (snd (crbit_for_cond c)); reflexivity.
  case (snd (crbit_for_cond c)); reflexivity.
Qed.
Hint Rewrite transl_op_label: labels.

Remark transl_load_store_label:
  forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
         addr args k,
  (forall c r, is_label lbl (mk1 c r) = false) ->
  (forall r1 r2, is_label lbl (mk2 r1 r2) = false) ->
  find_label lbl (transl_load_store mk1 mk2 addr args k) = find_label lbl k.
Proof.
  intros; unfold transl_load_store.
  destruct addr; destruct args; try (destruct args); try (destruct args);
  try reflexivity.
  case (ireg_eq (ireg_of m) GPR0); intro.
  simpl. rewrite H. auto. 
  case (Int.eq (high_s i) Int.zero). simpl; rewrite H; auto.
  simpl; rewrite H; auto.
  simpl; rewrite H0; auto.
  simpl; rewrite H; auto.
  case (ireg_eq (ireg_of m) GPR0); intro; simpl; rewrite H; auto. 
  case (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto.
Qed.
Hint Rewrite transl_load_store_label: labels.

Lemma transl_instr_label:
  forall i k,
  find_label lbl (transl_instr i k) = 
    if Mach.is_label lbl i then Some k else find_label lbl k.
Proof.
  intros. generalize (Mach.is_label_correct lbl i). 
  case (Mach.is_label lbl i); intro.
  subst i. simpl. rewrite peq_true. auto.
  destruct i; simpl; autorewrite with labels; try reflexivity.
  destruct m; rewrite transl_load_store_label; intros; reflexivity. 
  destruct m; rewrite transl_load_store_label; intros; reflexivity. 
  destruct s0; reflexivity.
  rewrite peq_false. auto. congruence.
  case (snd (crbit_for_cond c)); reflexivity.
Qed.

Lemma transl_code_label:
  forall c,
  find_label lbl (transl_code c) = 
    option_map transl_code (Mach.find_label lbl c).
Proof.
  induction c; simpl; intros.
  auto. rewrite transl_instr_label.
  case (Mach.is_label lbl a). reflexivity.
  auto.
Qed.

Lemma transl_find_label:
  forall f,
  find_label lbl (transl_function f) = 
    option_map transl_code (Mach.find_label lbl f.(fn_code)).
Proof.
  intros. unfold transl_function. simpl. apply transl_code_label.
Qed.

End TRANSL_LABEL.

(** A valid branch in a piece of Mach code translates to a valid ``go to''
  transition in the generated PPC code. *)

Lemma find_label_goto_label:
  forall f lbl rs m c' b ofs,
  Genv.find_funct_ptr ge b = Some (Internal f) ->
  rs PC = Vptr b ofs ->
  Mach.find_label lbl f.(fn_code) = Some c' ->
  exists rs',
    goto_label (transl_function f) lbl rs m = OK rs' m  
  /\ transl_code_at_pc (rs' PC) f c'
  /\ forall r, r <> PC -> rs'#r = rs#r.
Proof.
  intros. 
  generalize (transl_find_label lbl f).
  rewrite H1; simpl. intro.
  generalize (label_pos_code_tail lbl (transl_function f) 0 
                 (transl_code c') H2).
  intros [pos' [A [B C]]].
  exists (rs#PC <- (Vptr b (Int.repr pos'))).
  split. unfold goto_label. rewrite A. rewrite H0. auto.
  split. rewrite Pregmap.gss. constructor. auto. 
  rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in B.
  auto. omega. 
  generalize (functions_transl_no_overflow _ _ H). 
  omega.
  intros. apply Pregmap.gso; auto.
Qed.  

(** * Memory properties *)

(** The PowerPC has no instruction for ``load 8-bit signed integer''.
  We show that it can be synthesized as a ``load 8-bit unsigned integer''
  followed by a sign extension. *)

Lemma loadv_8_signed_unsigned:
  forall m a,
  Mem.loadv Mint8signed m a = 
    option_map Val.cast8signed (Mem.loadv Mint8unsigned m a).
Proof.
  intros. unfold Mem.loadv. destruct a; try reflexivity.
  unfold load. case (zlt b (nextblock m)); intro.
  change  (in_bounds Mint8unsigned (Int.signed i) (blocks m b))
     with (in_bounds Mint8signed (Int.signed i) (blocks m b)).
  case (in_bounds Mint8signed (Int.signed i) (blocks m b)).
  change (mem_chunk Mint8unsigned) with (mem_chunk Mint8signed).
  set (v := (load_contents (mem_chunk Mint8signed)
             (contents (blocks m b)) (Int.signed i))).
  unfold Val.load_result. destruct v; try reflexivity. 
  simpl. rewrite Int.cast8_signed_unsigned. auto.
  reflexivity. reflexivity.
Qed.

(** Similarly, we show that signed 8- and 16-bit stores can be performed
  like unsigned stores. *)

Lemma storev_8_signed_unsigned:
  forall m a v,
  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
Proof.
  intros. reflexivity.
Qed.

Lemma storev_16_signed_unsigned:
  forall m a v,
  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
  intros. reflexivity.
Qed.

(** * Proof of semantic preservation *)

(** The invariants for the inductive proof of simulation are as follows.
  The simulation diagrams are of the form:
<<
      c1, ms1, m1 --------------------- rs1, m1
           |                              |
           |                              |
           v                              v
      c2, ms2, m2 --------------------- rs2, m2
>>
  Left: execution of one Mach instruction.  Right: execution of zero, one
  or several instructions.  Precondition (top): agreement between
  the Mach register set [ms1] and the PPC register set [rs1]; moreover,
  [rs1 PC] points to the translation of code [c1].  Postcondition (bottom):
  similar.
*)

Definition exec_instr_prop
            (f: Mach.function) (sp: val) 
            (c1: Mach.code) (ms1: Mach.regset) (m1: mem) (t: trace)
            (c2: Mach.code) (ms2: Mach.regset) (m2: mem) :=
  forall rs1
    (WTF: wt_function f)
    (INCL: incl c1 f.(fn_code))
    (AT: transl_code_at_pc (rs1 PC) f c1)
    (AG: agree ms1 sp rs1),
  exists rs2,
    agree ms2 sp rs2
  /\ exec_steps tge rs1 m1 t rs2 m2
  /\ transl_code_at_pc (rs2 PC) f c2.

Definition exec_function_body_prop
            (f: Mach.function) (parent: val) (ra: val)
            (ms1: Mach.regset) (m1: mem) (t: trace)
            (ms2: Mach.regset) (m2: mem) :=
  forall rs1
    (WTRA: Val.has_type ra Tint)
    (RALR: rs1 LR = ra)
    (WTF: wt_function f)
    (AT: Genv.find_funct ge (rs1 PC) = Some (Internal f))
    (AG: agree ms1 parent rs1),
  exists rs2,
     agree ms2 parent rs2
  /\ exec_steps tge rs1 m1 t rs2 m2
  /\ rs2 PC = rs1 LR.

Definition exec_function_prop
            (f: Mach.fundef) (parent: val) 
            (ms1: Mach.regset) (m1: mem) (t: trace)
            (ms2: Mach.regset) (m2: mem) :=
  forall rs1
    (WTF: wt_fundef f)
    (AT: Genv.find_funct ge (rs1 PC) = Some f)
    (AG: agree ms1 parent rs1)
    (WTRA: Val.has_type (rs1 LR) Tint),
  exists rs2,
     agree ms2 parent rs2
  /\ exec_steps tge rs1 m1 t rs2 m2
  /\ rs2 PC = rs1 LR.
           
(** We show each case of the inductive proof of simulation as a separate
  lemma. *)

Lemma exec_Mlabel_prop:
  forall (f : function) (sp : val) (lbl : Mach.label)
     (c : list Mach.instruction) (rs : Mach.regset) (m : mem),
   exec_instr_prop f sp (Mlabel lbl :: c) rs m E0 c rs m.
Proof.
  intros; red; intros.
  assert (exec_straight tge (transl_function f)
                        (transl_code (Mlabel lbl :: c)) rs1 m
                        (transl_code c) (nextinstr rs1) m).
  simpl. apply exec_straight_one. reflexivity. reflexivity.
  exists (nextinstr rs1). split. apply agree_nextinstr; auto.
  eapply exec_straight_steps; eauto.
Qed.

Lemma exec_Mgetstack_prop:
  forall (f : function) (sp : val) (ofs : int) (ty : typ) (dst : mreg)
     (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (v : val),
   load_stack m sp ty ofs = Some v ->
   exec_instr_prop f sp (Mgetstack ofs ty dst :: c) ms m E0 c (Regmap.set dst v ms) m.
Proof.
  intros; red; intros.
  unfold load_stack in H. 
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI. inversion WTI.
  rewrite (sp_val _ _ _ AG) in H.
  assert (NOTE: GPR1 <> GPR0). congruence.
  generalize (loadind_correct tge (transl_function f) GPR1 ofs ty
                dst (transl_code c) rs1 m v H H1 NOTE).
  intros [rs2 [EX [RES OTH]]].
  exists rs2. split.
  apply agree_exten_2 with (rs1#(preg_of dst) <- v).
  auto with ppcgen. 
  intros. case (preg_eq r0 (preg_of dst)); intro.
  subst r0. rewrite Pregmap.gss. auto. 
  rewrite Pregmap.gso; auto. 
  eapply exec_straight_steps; eauto.
Qed.

Lemma exec_Msetstack_prop:
  forall (f : function) (sp : val) (src : mreg) (ofs : int) (ty : typ)
     (c : list Mach.instruction) (ms : mreg -> val) (m m' : mem),
   store_stack m sp ty ofs (ms src) = Some m' ->
   exec_instr_prop f sp (Msetstack src ofs ty :: c) ms m E0 c ms m'.
Proof.
  intros; red; intros.
  unfold store_stack in H. 
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI. inversion WTI.
  rewrite (sp_val _ _ _ AG) in H.
  rewrite (preg_val ms sp rs1) in H; auto.
  assert (NOTE: GPR1 <> GPR0). congruence.
  generalize (storeind_correct tge (transl_function f) GPR1 ofs ty
                src (transl_code c) rs1 m m' H H2 NOTE).
  intros [rs2 [EX OTH]].
  exists rs2. split.
  apply agree_exten_2 with rs1; auto.
  eapply exec_straight_steps; eauto.
Qed.

Lemma exec_Mgetparam_prop:
  forall (f : function) (sp parent : val) (ofs : int) (ty : typ)
     (dst : mreg) (c : list Mach.instruction) (ms : Mach.regset)
     (m : mem) (v : val),
   load_stack m sp Tint (Int.repr 0) = Some parent ->
   load_stack m parent ty ofs = Some v ->
   exec_instr_prop f sp (Mgetparam ofs ty dst :: c) ms m E0 c (Regmap.set dst v ms) m.
Proof.
  intros; red; intros.
  set (rs2 := nextinstr (rs1#GPR2 <- parent)).
  assert (EX1: exec_straight tge (transl_function f)
                 (transl_code (Mgetparam ofs ty dst :: c)) rs1 m
                 (loadind GPR2 ofs ty dst (transl_code c)) rs2 m).
  simpl. apply exec_straight_one.
  simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen.
  unfold const_low. rewrite <- (sp_val ms sp rs1); auto.
  unfold load_stack in H. simpl chunk_of_type in H. 
  rewrite H. reflexivity. reflexivity.
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI. inversion WTI.
  unfold load_stack in H0. change parent with rs2#GPR2 in H0.
  assert (NOTE: GPR2 <> GPR0). congruence.
  generalize (loadind_correct tge (transl_function f) GPR2 ofs ty
                dst (transl_code c) rs2 m v H0 H2 NOTE).
  intros [rs3 [EX2 [RES OTH]]].
  exists rs3. split.
  apply agree_exten_2 with (rs2#(preg_of dst) <- v).
  unfold rs2; auto with ppcgen.
  intros. case (preg_eq r0 (preg_of dst)); intro.
  subst r0. rewrite Pregmap.gss. auto. 
  rewrite Pregmap.gso; auto. 
  eapply exec_straight_steps; eauto. 
  eapply exec_straight_trans; eauto.
Qed.

Lemma exec_straight_exec_prop:
  forall f sp c1 rs1 m1 c2 m2 ms',
  transl_code_at_pc (rs1 PC) f c1 ->
  (exists rs2, 
      exec_straight tge (transl_function f)
                    (transl_code c1) rs1 m1
                    (transl_code c2) rs2 m2 
   /\ agree ms' sp rs2) ->
  (exists rs2,
      agree ms' sp rs2
   /\ exec_steps tge rs1 m1 E0 rs2 m2
  /\ transl_code_at_pc (rs2 PC) f c2).
Proof.
  intros until ms'. intros TRANS1 [rs2 [EX AG]].
  exists rs2. split. assumption. 
  eapply exec_straight_steps; eauto.
Qed.

Lemma exec_Mop_prop:
  forall (f : function) (sp : val) (op : operation) (args : list mreg)
     (res : mreg) (c : list Mach.instruction) (ms: Mach.regset)
     (m : mem) (v: val),
   eval_operation ge sp op ms ## args = Some v ->
   exec_instr_prop f sp (Mop op args res :: c) ms m E0 c (Regmap.set res v ms) m.
Proof.
  intros; red; intros.
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI. 
  eapply exec_straight_exec_prop; eauto.
  simpl. eapply transl_op_correct; auto.
  rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
Qed.

Lemma exec_Mload_prop:
   forall (f : function) (sp : val) (chunk : memory_chunk)
     (addr : addressing) (args : list mreg) (dst : mreg)
     (c : list Mach.instruction) (ms: Mach.regset) (m : mem) 
     (a v : val),
   eval_addressing ge sp addr ms ## args = Some a ->
   loadv chunk m a = Some v ->
   exec_instr_prop f sp (Mload chunk addr args dst :: c) ms m E0 c (Regmap.set dst v ms) m.
Proof.
  intros; red; intros.
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI; inversion WTI.
  assert (eval_addressing tge sp addr ms##args = Some a).
    rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
  eapply exec_straight_exec_prop; eauto.
  destruct chunk; simpl; simpl in H6;
  (* all cases but Mint8signed *)
  try (eapply transl_load_correct; eauto;
       intros; simpl; unfold preg_of; rewrite H6; auto).
  (* Mint8signed *)
  generalize (loadv_8_signed_unsigned m a).
  rewrite H0. 
  caseEq (loadv Mint8unsigned m a);
  [idtac | simpl;intros;discriminate].
  intros v' LOAD' EQ. simpl in EQ. injection EQ. intro EQ1. clear EQ.
  assert (X1: forall (cst : constant) (r1 : ireg) (rs1 : regset),
    exec_instr tge (transl_function f) (Plbz (ireg_of dst) cst r1) rs1 m =
    load1 tge Mint8unsigned (preg_of dst) cst r1 rs1 m).
    intros. unfold preg_of; rewrite H6. reflexivity. 
  assert (X2: forall (r1 r2 : ireg) (rs1 : regset),
    exec_instr tge (transl_function f) (Plbzx (ireg_of dst) r1 r2) rs1 m =
    load2 Mint8unsigned (preg_of dst) r1 r2 rs1 m).
    intros. unfold preg_of; rewrite H6. reflexivity. 
  generalize (transl_load_correct tge (transl_function f)
                (Plbz (ireg_of dst)) (Plbzx (ireg_of dst))
                Mint8unsigned addr args 
                (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code c) 
                ms sp rs1 m dst a v'
                X1 X2 AG H3 H7 LOAD').
  intros [rs2 [EX1 AG1]].
  exists (nextinstr (rs2#(ireg_of dst) <- v)).
  split. eapply exec_straight_trans. eexact EX1.
  apply exec_straight_one. simpl. 
  rewrite <- (ireg_val _ _ _ dst AG1);auto. rewrite Regmap.gss. 
  rewrite EQ1. reflexivity. reflexivity. 
  eauto with ppcgen.
Qed.

Lemma exec_Mstore_prop:
   forall (f : function) (sp : val) (chunk : memory_chunk)
     (addr : addressing) (args : list mreg) (src : mreg)
     (c : list Mach.instruction) (ms: Mach.regset) (m m' : mem)
     (a : val),
   eval_addressing ge sp addr ms ## args = Some a ->
   storev chunk m a (ms src) = Some m' ->
   exec_instr_prop f sp (Mstore chunk addr args src :: c) ms m E0 c ms m'.
Proof.
  intros; red; intros.
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI; inversion WTI.
  rewrite <- (eval_addressing_preserved symbols_preserved) in H.
  eapply exec_straight_exec_prop; eauto.
  destruct chunk; simpl; simpl in H6;
  try (rewrite storev_8_signed_unsigned in H);
  try (rewrite storev_16_signed_unsigned in H);
  simpl; eapply transl_store_correct; eauto;
  intros; unfold preg_of; rewrite H6; reflexivity.
Qed.

Hypothesis wt_prog: wt_program prog.

Lemma exec_Mcall_prop:
   forall (f : function) (sp : val) (sig : signature)
     (mos : mreg + ident) (c : list Mach.instruction) (ms : Mach.regset)
     (m : mem) (f' : Mach.fundef) (t: trace) (ms' : Mach.regset) (m' : mem),
   find_function ge mos ms = Some f' ->
   exec_function ge f' sp ms m t ms' m' ->
   exec_function_prop f' sp ms m t ms' m' ->
   exec_instr_prop f sp (Mcall sig mos :: c) ms m t c ms' m'.
Proof.
  intros; red; intros.
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI. inversion WTI.
  inversion AT.
  assert (WTF': wt_fundef f').
    destruct mos; simpl in H.
    apply (Genv.find_funct_prop wt_fundef wt_prog H).
    destruct (Genv.find_symbol ge i); try discriminate.
    apply (Genv.find_funct_ptr_prop wt_fundef wt_prog H).
  assert (NOOV: code_size (transl_function f) <= Int.max_unsigned).
    eapply functions_transl_no_overflow; eauto.
  destruct mos; simpl in H; simpl transl_code in H7.
  (* Indirect call *)
  generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
  generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2.
  set (rs2 := nextinstr (rs1#CTR <- (ms m0))).
  set (rs3 := rs2 #LR <- (Val.add rs2#PC Vone) #PC <- (ms m0)).
  assert (TFIND: Genv.find_funct ge (rs3#PC) = Some f').
    unfold rs3. rewrite Pregmap.gss. auto.
  assert (AG3: agree ms sp rs3). 
    unfold rs3, rs2; auto 8 with ppcgen.
  assert (WTRA: Val.has_type rs3#LR Tint).
    change rs3#LR with (Val.add (Val.add rs1#PC Vone) Vone).
    rewrite <- H5. exact I.
  generalize (H1 rs3 WTF' TFIND AG3 WTRA).
  intros [rs4 [AG4 [EXF' PC4]]].
  exists rs4. split. auto. split.
  apply exec_trans with E0 rs2 m t. apply exec_one. econstructor. 
    eauto. apply functions_transl. eexact H6. 
    rewrite find_instr_tail. rewrite H7. reflexivity.
    simpl. rewrite <- (ireg_val ms sp rs1); auto. 
  apply exec_trans with E0 rs3 m t. apply exec_one. econstructor.
    unfold rs2, nextinstr. rewrite Pregmap.gss. 
    rewrite Pregmap.gso. rewrite <- H5. simpl. reflexivity.
    discriminate. apply functions_transl. eexact H6.
    rewrite find_instr_tail. rewrite CT1. reflexivity.
    simpl. replace (rs2 CTR) with (ms m0). reflexivity.
    unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss. 
    auto. discriminate.
  exact EXF'. traceEq. traceEq. 
  rewrite PC4. unfold rs3. rewrite Pregmap.gso. rewrite Pregmap.gss.
  unfold rs2, nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. 
  rewrite <- H5. simpl. constructor. auto. auto. 
  discriminate. discriminate.
  (* Direct call *)
  caseEq (Genv.find_symbol ge i). intros fblock FINDS.
  rewrite FINDS in H.
  generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
  set (rs2 := rs1 #LR <- (Val.add rs1#PC Vone) #PC <- (symbol_offset tge i Int.zero)).
  assert (TFIND: Genv.find_funct ge (rs2#PC) = Some f').
    unfold rs2. rewrite Pregmap.gss. 
    unfold symbol_offset. rewrite symbols_preserved. 
    rewrite FINDS.     
    rewrite Genv.find_funct_find_funct_ptr. assumption.
  assert (AG2: agree ms sp rs2). 
    unfold rs2; auto 8 with ppcgen.
  assert (WTRA: Val.has_type rs2#LR Tint).
    change rs2#LR with (Val.add rs1#PC Vone).
    rewrite <- H5. exact I.
  generalize (H1 rs2 WTF' TFIND AG2 WTRA).
  intros [rs3 [AG3 [EXF' PC3]]].
  exists rs3. split. auto. split.
  apply exec_trans with E0 rs2 m t. apply exec_one. econstructor. 
    eauto. apply functions_transl. eexact H6. 
    rewrite find_instr_tail. rewrite H7. reflexivity.
    simpl. reflexivity. 
  exact EXF'. traceEq.
  rewrite PC3. unfold rs2. rewrite Pregmap.gso. rewrite Pregmap.gss.
  rewrite <- H5. simpl. constructor. auto. auto. 
  discriminate. 
  intro FINDS. rewrite FINDS in H. discriminate.
Qed.

Lemma exec_Malloc_prop:
  forall (f : function) (sp : val) (c : list Mach.instruction)
         (ms : Mach.regset) (m : mem) (sz : int) (m' : mem) (blk : block),
  ms Conventions.loc_alloc_argument = Vint sz ->
  Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
  exec_instr_prop f sp (Malloc :: c) ms m E0 c
    (Regmap.set Conventions.loc_alloc_result (Vptr blk Int.zero) ms) m'.
Proof.
  intros; red; intros.
  eapply exec_straight_exec_prop; eauto.
  simpl. eapply transl_alloc_correct; eauto. 
Qed.

Lemma exec_Mgoto_prop:
   forall (f : function) (sp : val) (lbl : Mach.label)
     (c : list Mach.instruction) (ms : Mach.regset) (m : mem)
     (c' : Mach.code),
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop f sp (Mgoto lbl :: c) ms m E0 c' ms m.
Proof.
  intros; red; intros.
  inversion AT.
  generalize (find_label_goto_label f lbl rs1 m _ _ _ H1 (sym_equal H0) H).
  intros [rs2 [GOTO [AT2 INV]]].
  exists rs2. split. apply agree_exten_2 with rs1; auto. 
  split. inversion AT. apply exec_one. econstructor; eauto.
  apply functions_transl; eauto. 
  rewrite find_instr_tail. rewrite H7. simpl. reflexivity.
  simpl. rewrite GOTO. auto. auto.
Qed.

Lemma exec_Mcond_true_prop:
   forall (f : function) (sp : val) (cond : condition)
     (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction)
     (ms: Mach.regset) (m : mem) (c' : Mach.code),
   eval_condition cond ms ## args = Some true ->
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop f sp (Mcond cond args lbl :: c) ms m E0 c' ms m.
Proof.
  intros; red; intros.
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI. inversion WTI.
  pose (k1 := 
         if snd (crbit_for_cond cond)
         then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code c
         else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code c).
  generalize (transl_cond_correct tge (transl_function f)
                cond args k1 ms sp rs1 m true H2 AG H).
  simpl. intros [rs2 [EX [RES AG2]]].
  inversion AT.
  generalize (functions_transl _ _ H6); intro FN.
  generalize (functions_transl_no_overflow _ _ H6); intro NOOV.
  simpl in H7.
  generalize (exec_straight_steps_2 _ _ _ _ _ _ _ EX 
               NOOV _ _ (sym_equal H5) FN H7).
  intros [ofs' [PC2 CT2]].
  generalize (find_label_goto_label f lbl rs2 m _ _ _ H6 PC2 H0).
  intros [rs3 [GOTO [AT3 INV3]]].
  exists rs3. split.
  apply agree_exten_2 with rs2; auto.
  split. eapply exec_trans. 
  eapply exec_straight_steps_1; eauto.
  caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES.
  apply exec_one. econstructor; eauto.
  rewrite find_instr_tail. rewrite CT2. unfold k1. rewrite ISSET. reflexivity.
  simpl. rewrite RES. simpl. auto.
  apply exec_one. econstructor; eauto.
  rewrite find_instr_tail. rewrite CT2. unfold k1. rewrite ISSET. reflexivity.
  simpl. rewrite RES. simpl. auto.
  traceEq. auto. 
Qed.

Lemma exec_Mcond_false_prop:
   forall (f : function) (sp : val) (cond : condition)
     (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction)
     (ms : Mach.regset) (m : mem),
   eval_condition cond ms ## args = Some false ->
   exec_instr_prop f sp (Mcond cond args lbl :: c) ms m E0 c ms m.
Proof.
  intros; red; intros.
  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
  intro WTI. inversion WTI.
  pose (k1 := 
         if snd (crbit_for_cond cond)
         then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code c
         else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code c).
  generalize (transl_cond_correct tge (transl_function f)
                cond args k1 ms sp rs1 m false H1 AG H).
  simpl. intros [rs2 [EX [RES AG2]]].
  exists (nextinstr rs2).
  split. auto with ppcgen. 
  eapply exec_straight_steps; eauto.
  eapply exec_straight_trans. eexact EX. 
  caseEq (snd (crbit_for_cond cond)); intro ISSET; rewrite ISSET in RES.
  unfold k1; rewrite ISSET; apply exec_straight_one. 
  simpl. rewrite RES. reflexivity.
  reflexivity.
  unfold k1; rewrite ISSET; apply exec_straight_one. 
  simpl. rewrite RES. reflexivity.
  reflexivity.
Qed.

Lemma exec_instr_incl:
  forall f sp c rs m t c' rs' m',
  Mach.exec_instr ge f sp c rs m t c' rs' m' ->
  incl c f.(fn_code) -> incl c' f.(fn_code).
Proof.
  induction 1; intros; eauto with coqlib.
  eapply incl_find_label; eauto.
  eapply incl_find_label; eauto.
Qed.

Lemma exec_instrs_incl:
  forall f sp c rs m t c' rs' m',
  Mach.exec_instrs ge f sp c rs m t c' rs' m' ->
  incl c f.(fn_code) -> incl c' f.(fn_code).
Proof.
  induction 1; intros. 
  auto.
  eapply exec_instr_incl; eauto.
  eauto.
Qed.

Lemma exec_refl_prop:
   forall (f : function) (sp : val) (c : Mach.code) (ms : Mach.regset)
     (m : mem), exec_instr_prop f sp c ms m E0 c ms m.
Proof.
  intros; red; intros.
  exists rs1. split. auto. split. apply exec_refl. auto.
Qed.

Lemma exec_one_prop:
   forall (f : function) (sp : val) (c : Mach.code) (ms : Mach.regset)
     (m : mem) (t: trace) (c' : Mach.code) (ms' : Mach.regset) (m' : mem),
   Mach.exec_instr ge f sp c ms m t c' ms' m' ->
   exec_instr_prop f sp c ms m t c' ms' m' ->
   exec_instr_prop f sp c ms m t c' ms' m'.
Proof.
  auto.
Qed.

Lemma exec_trans_prop:
   forall (f : function) (sp : val) (c1 : Mach.code) (ms1 : Mach.regset)
     (m1 : mem) (t1: trace) (c2 : Mach.code) (ms2 : Mach.regset) (m2 : mem)
     (t2: trace) (c3 : Mach.code) (ms3 : Mach.regset) (m3 : mem) (t3: trace),
   exec_instrs ge f sp c1 ms1 m1 t1 c2 ms2 m2 ->
   exec_instr_prop f sp c1 ms1 m1 t1 c2 ms2 m2 ->
   exec_instrs ge f sp c2 ms2 m2 t2 c3 ms3 m3 ->
   exec_instr_prop f sp c2 ms2 m2 t2 c3 ms3 m3 -> 
   t3 = t1 ** t2 ->
   exec_instr_prop f sp c1 ms1 m1 t3 c3 ms3 m3.
Proof.
  intros; red; intros.
  generalize (H0 rs1 WTF INCL AT AG).
  intros [rs2 [AG2 [EX2 AT2]]].
  generalize (exec_instrs_incl _ _ _ _ _ _ _ _ _ H INCL). intro INCL2.
  generalize (H2 rs2 WTF INCL2 AT2 AG2).
  intros [rs3 [AG3 [EX3 AT3]]].
  exists rs3. split. auto. split. eapply exec_trans; eauto. auto.
Qed.

Lemma exec_function_body_prop_:
   forall (f : function) (parent ra : val) (ms : Mach.regset) (m : mem)
     (t: trace) (ms' : Mach.regset) (m1 m2 m3 m4 : mem) (stk : block)
     (c : list Mach.instruction),
   alloc m (- fn_framesize f)
      (align_16_top (- fn_framesize f) (fn_stacksize f)) = (m1, stk) ->
   let sp := Vptr stk (Int.repr (- fn_framesize f)) in
   store_stack m1 sp Tint (Int.repr 0) parent = Some m2 ->
   store_stack m2 sp Tint (Int.repr 12) ra = Some m3 ->
   exec_instrs ge f sp (fn_code f) ms m3 t (Mreturn :: c) ms' m4 ->
   exec_instr_prop f sp (fn_code f) ms m3 t (Mreturn :: c) ms' m4 ->
   load_stack m4 sp Tint (Int.repr 0) = Some parent ->
   load_stack m4 sp Tint (Int.repr 12) = Some ra ->
   exec_function_body_prop f parent ra ms m t ms' (free m4 stk).
Proof.
  intros; red; intros.
  generalize (Genv.find_funct_inv AT). intros [b EQPC].
  generalize AT. rewrite EQPC. rewrite Genv.find_funct_find_funct_ptr. intro FN.
  generalize (functions_transl_no_overflow _ _ FN); intro NOOV.
  set (rs2 := nextinstr (rs1#GPR1 <- sp #GPR2 <- Vundef)).
  set (rs3 := nextinstr (rs2#GPR2 <- ra)).
  set (rs4 := nextinstr rs3).
  assert (exec_straight tge (transl_function f)
            (transl_function f) rs1 m 
            (transl_code (fn_code f)) rs4 m3).
  unfold transl_function at 2. 
  apply exec_straight_three with rs2 m2 rs3 m2.
  unfold exec_instr. rewrite H. fold sp. 
  generalize H0. unfold store_stack. change (Vint (Int.repr 0)) with Vzero.
  replace (Val.add sp Vzero) with sp. simpl chunk_of_type. 
  rewrite (sp_val _ _ _ AG). intro. rewrite H6. clear H6.
  reflexivity. unfold sp. simpl. rewrite Int.add_zero. reflexivity.
  simpl. replace (rs2 LR) with ra. reflexivity.
  simpl. unfold store1. rewrite gpr_or_zero_not_zero. 
  unfold const_low. replace (rs3 GPR1) with sp. replace (rs3 GPR2) with ra.
  unfold store_stack in H1. simpl chunk_of_type in H1. rewrite H1. reflexivity.
  reflexivity. reflexivity. discriminate. 
  reflexivity. reflexivity. reflexivity.
  assert (AT2: transl_code_at_pc rs4#PC f f.(fn_code)).
    change (rs4 PC) with (Val.add (Val.add (Val.add (rs1 PC) Vone) Vone) Vone).
    rewrite EQPC. simpl. constructor. auto.
    eapply code_tail_next_int; auto.
    eapply code_tail_next_int; auto.
    eapply code_tail_next_int; auto.
    unfold Int.zero. rewrite Int.unsigned_repr. 
    rewrite code_tail_zero. unfold transl_function. reflexivity.
    compute. intuition congruence.
  assert (AG2: agree ms sp rs2).
    split. reflexivity. 
    intros. unfold rs2. rewrite nextinstr_inv. 
    repeat (rewrite Pregmap.gso). elim AG; auto.
    auto with ppcgen. auto with ppcgen. auto with ppcgen.
  assert (AG4: agree ms sp rs4).
    unfold rs4, rs3; auto with ppcgen.
  generalize (H3 rs4 WTF (incl_refl _) AT2 AG4).
  intros [rs5 [AG5 [EXB AT5]]].
  set (rs6 := nextinstr (rs5#GPR2 <- ra)).
  set (rs7 := nextinstr (rs6#LR <- ra)).
  set (rs8 := nextinstr (rs7#GPR1 <- parent)).
  set (rs9 := rs8#PC <- ra).
  assert (exec_straight tge (transl_function f)
            (transl_code (Mreturn :: c)) rs5 m4 
            (Pblr :: transl_code c) rs8 (free m4 stk)).
  simpl. apply exec_straight_three with rs6 m4 rs7 m4.
  simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
  unfold load_stack in H5. simpl in H5. 
  rewrite <- (sp_val _ _ _ AG5). simpl. rewrite H5.
  reflexivity. discriminate.
  unfold rs7. change ra with rs6#GPR2. reflexivity. 
  unfold exec_instr. generalize H4. unfold load_stack. 
  replace (Val.add sp (Vint (Int.repr 0))) with sp.
  simpl chunk_of_type. intro. change rs7#GPR1 with rs5#GPR1.
  rewrite <- (sp_val _ _ _ AG5). rewrite H7.
  unfold sp. reflexivity.
  unfold sp. simpl. rewrite Int.add_zero. reflexivity.
  reflexivity. reflexivity. reflexivity.
  exists rs9. split.
  (* agreement *)
  assert (AG7: agree ms' sp rs7). 
    unfold rs7, rs6; auto 10 with ppcgen.
  assert (AG8: agree ms' parent rs8).
    split. reflexivity. intros. unfold rs8. 
    rewrite nextinstr_inv. rewrite Pregmap.gso.
    elim AG7; auto. auto with ppcgen. auto with ppcgen.
  unfold rs9; auto with ppcgen.
  (* execution *)
  split. apply exec_trans with E0 rs4 m3 t.
  eapply exec_straight_steps_1; eauto. 
  apply functions_transl; auto. 
  apply exec_trans with t rs5 m4 E0. assumption.
  inversion AT5.
  apply exec_trans with E0 rs8 (free m4 stk) E0.
  eapply exec_straight_steps_1; eauto.
  apply functions_transl; auto.
  apply exec_one. econstructor. 
  change rs8#PC with (Val.add (Val.add (Val.add rs5#PC Vone) Vone) Vone).
  rewrite <- H8. simpl. reflexivity.
  apply functions_transl; eauto.
  assert (code_tail (Int.unsigned (Int.add (Int.add (Int.add ofs Int.one) Int.one) Int.one))
                    (transl_function f) = Pblr :: transl_code c).
  eapply code_tail_next_int; auto.
  eapply code_tail_next_int; auto.
  eapply code_tail_next_int; auto.
  rewrite H10. simpl. reflexivity.
  rewrite find_instr_tail. rewrite H13.
  reflexivity.
  reflexivity.
  traceEq. traceEq. traceEq. 
  (* LR preservation *)
  change rs9#PC with ra. auto.
Qed.

Lemma exec_function_internal_prop:
   forall (f : function) (parent : val) (ms : Mach.regset) (m : mem)
          (t: trace) (ms' : Mach.regset) (m' : mem),
   (forall ra : val,
      Val.has_type ra Tint ->
      exec_function_body ge f parent ra ms m t ms' m') ->
   (forall ra : val, Val.has_type ra Tint -> 
      exec_function_body_prop f parent ra ms m t ms' m') ->
   exec_function_prop (Internal f) parent ms m t ms' m'.
Proof.
  intros; red; intros.
  inversion WTF. subst f0. 
  apply (H0 rs1#LR WTRA rs1 WTRA (refl_equal _) H2 AT AG).
Qed.

Lemma exec_function_external_prop:
  forall (ef : external_function) (parent : val) (args : list val)
         (res : val) (ms1 ms2: Mach.regset) (m : mem)
         (t : trace),
  event_match ef args t res ->
  Mach.extcall_arguments ms1 m parent ef.(ef_sig) args ->
  ms2 = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms1 ->
  exec_function_prop (External ef) parent ms1 m t ms2 m.
Proof.
  intros; red; intros.
  destruct (Genv.find_funct_inv AT) as [b EQ].
  rewrite EQ in AT. rewrite Genv.find_funct_find_funct_ptr in AT.
  exists (rs1#(loc_external_result (ef_sig ef)) <- res #PC <- (rs1 LR)).
  split. rewrite loc_external_result_match. rewrite H1. auto with ppcgen.
  split. apply exec_one. eapply exec_step_external; eauto.
  destruct (functions_translated _ _ AT) as [tf [A B]].
  simpl in B. congruence.
  eapply extcall_arguments_match; eauto.
  reflexivity. 
Qed.

(** We then conclude by induction on the structure of the Mach
execution derivation. *)

Theorem transf_function_correct:
  forall f parent ms m t ms' m',
  Mach.exec_function ge f parent ms m t ms' m' ->
  exec_function_prop f parent ms m t ms' m'.
Proof 
  (Mach.exec_function_ind4 ge
           exec_instr_prop
           exec_instr_prop
           exec_function_body_prop
           exec_function_prop

           exec_Mlabel_prop
           exec_Mgetstack_prop
           exec_Msetstack_prop
           exec_Mgetparam_prop
           exec_Mop_prop
           exec_Mload_prop
           exec_Mstore_prop
           exec_Mcall_prop
           exec_Malloc_prop
           exec_Mgoto_prop
           exec_Mcond_true_prop
           exec_Mcond_false_prop
           exec_refl_prop
           exec_one_prop
           exec_trans_prop
           exec_function_body_prop_
           exec_function_internal_prop
           exec_function_external_prop).

End PRESERVATION.

Theorem transf_program_correct:
  forall (p: Mach.program) (tp: PPC.program) (t: trace) (r: val),
  wt_program p ->
  transf_program p = Some tp ->
  Mach.exec_program p t r ->
  PPC.exec_program tp t r.
Proof.
  intros. 
  destruct H1 as [fptr [f [ms [m [FINDS [FINDF [EX RES]]]]]]].
  assert (WTF: wt_fundef f).
    apply (Genv.find_funct_ptr_prop wt_fundef H FINDF).
  set (ge := Genv.globalenv p) in *.
  set (ms0 := Regmap.init Vundef) in *.
  set (tge := Genv.globalenv tp).
  set (rs0 := 
    (Pregmap.init Vundef) # PC <- (symbol_offset tge tp.(prog_main) Int.zero)
                          # LR <- Vzero
                          # GPR1 <- (Vptr Mem.nullptr Int.zero)).
  assert (AT: Genv.find_funct ge (rs0 PC) = Some f).
    change (rs0 PC) with (symbol_offset tge tp.(prog_main) Int.zero).
    rewrite (transform_partial_program_main _ _ H0).
    unfold symbol_offset. rewrite (symbols_preserved p tp H0). 
    fold ge. rewrite FINDS. 
    rewrite Genv.find_funct_find_funct_ptr. exact FINDF.
  assert (AG: agree ms0 (Vptr Mem.nullptr Int.zero) rs0).
    split. reflexivity. intros. unfold rs0. 
    repeat (rewrite Pregmap.gso; auto with ppcgen). 
  assert (WTRA: Val.has_type (rs0 LR) Tint).
    exact I.
  generalize (transf_function_correct p tp H0 H
                 _ _ _ _ _ _ _ EX rs0 WTF AT AG WTRA).
  intros [rs [AG' [EX' RPC]]].
  red. exists rs; exists m.
  split. rewrite (Genv.init_mem_transf_partial _ _ H0). exact EX'.
  split. rewrite RPC. reflexivity. rewrite <- RES. 
  change (IR GPR3) with (preg_of R3). elim AG'; auto.
Qed.