Reorganized the development, modularizing away machine-dependent parts.

Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1507 insertions, 0 deletions

diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
new file mode 100644
index 0000000..32fedf3
--- /dev/null
+++ b/arm/Asmgenproof1.v
@@ -0,0 +1,1507 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness proof for ARM code generation: auxiliary results. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Locations.
+Require Import Mach.
+Require Import Machconcr.
+Require Import Machtyping.
+Require Import Asm.
+Require Import Asmgen.
+Require Conventions.
+
+(** * Correspondence between Mach registers and PPC registers *)
+
+Hint Extern 2 (_ <> _) => discriminate: ppcgen.
+
+(** Mapping from Mach registers to PPC registers. *)
+
+Lemma preg_of_injective:
+  forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
+Proof.
+  destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
+Qed.
+
+(** Characterization of PPC registers that correspond to Mach registers. *)
+
+Definition is_data_reg (r: preg) : Prop :=
+  match r with
+  | IR IR14 => False
+  | CR _ => False
+  | PC => False
+  | _ => True
+  end.
+
+Lemma ireg_of_is_data_reg:
+  forall (r: mreg), is_data_reg (ireg_of r).
+Proof.
+  destruct r; exact I.
+Qed.
+
+Lemma freg_of_is_data_reg:
+  forall (r: mreg), is_data_reg (ireg_of r).
+Proof.
+  destruct r; exact I.
+Qed.
+
+Lemma preg_of_is_data_reg:
+  forall (r: mreg), is_data_reg (preg_of r).
+Proof.
+  destruct r; exact I.
+Qed.
+
+Lemma ireg_of_not_IR13:
+  forall r, ireg_of r <> IR13.
+Proof.
+  intro. case r; discriminate.
+Qed.
+Lemma ireg_of_not_IR14:
+  forall r, ireg_of r <> IR14.
+Proof.
+  intro. case r; discriminate.
+Qed.
+
+Hint Resolve ireg_of_not_IR13 ireg_of_not_IR14: ppcgen.
+
+Lemma preg_of_not:
+  forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2.
+Proof.
+  intros; red; intro. subst r2. elim H. apply preg_of_is_data_reg.
+Qed.
+Hint Resolve preg_of_not: ppcgen.
+
+Lemma preg_of_not_IR13:
+  forall r, preg_of r <> IR13.
+Proof.
+  intro. case r; discriminate.
+Qed.
+Hint Resolve preg_of_not_IR13: ppcgen.
+
+(** Agreement between Mach register sets and PPC register sets. *)
+
+Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) :=
+  rs#IR13 = sp /\ forall r: mreg, ms r = rs#(preg_of r).
+
+Lemma preg_val:
+  forall ms sp rs r,
+  agree ms sp rs -> ms r = rs#(preg_of r).
+Proof.
+  intros. elim H. auto.
+Qed.
+  
+Lemma ireg_val:
+  forall ms sp rs r,
+  agree ms sp rs ->
+  mreg_type r = Tint ->
+  ms r = rs#(ireg_of r).
+Proof.
+  intros. elim H; intros.
+  generalize (H2 r). unfold preg_of. rewrite H0. auto.
+Qed.
+
+Lemma freg_val:
+  forall ms sp rs r,
+  agree ms sp rs ->
+  mreg_type r = Tfloat ->
+  ms r = rs#(freg_of r).
+Proof.
+  intros. elim H; intros.
+  generalize (H2 r). unfold preg_of. rewrite H0. auto.
+Qed.
+
+Lemma sp_val:
+  forall ms sp rs,
+  agree ms sp rs ->
+  sp = rs#IR13.
+Proof.
+  intros. elim H; auto.
+Qed.
+
+Lemma agree_exten_1:
+  forall ms sp rs rs',
+  agree ms sp rs ->
+  (forall r, is_data_reg r -> rs'#r = rs#r) ->
+  agree ms sp rs'.
+Proof.
+  unfold agree; intros. elim H; intros.
+  split. rewrite H0. auto. exact I. 
+  intros. rewrite H0. auto. apply preg_of_is_data_reg.
+Qed.
+
+Lemma agree_exten_2:
+  forall ms sp rs rs',
+  agree ms sp rs ->
+  (forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r) ->
+  agree ms sp rs'.
+Proof.
+  intros. eapply agree_exten_1; eauto. 
+  intros. apply H0; red; intro; subst r; elim H1.
+Qed.
+
+(** Preservation of register agreement under various assignments. *)
+
+Lemma agree_set_mreg:
+  forall ms sp rs r v,
+  agree ms sp rs ->
+  agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v).
+Proof.
+  unfold agree; intros. elim H; intros; clear H.
+  split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_IR13.
+  intros. unfold Regmap.set. case (RegEq.eq r0 r); intro.
+  subst r0. rewrite Pregmap.gss. auto.
+  rewrite Pregmap.gso. auto. red; intro. 
+  elim n. apply preg_of_injective; auto.
+Qed.
+Hint Resolve agree_set_mreg: ppcgen.
+
+Lemma agree_set_mireg:
+  forall ms sp rs r v,
+  agree ms sp (rs#(preg_of r) <- v) ->
+  mreg_type r = Tint ->
+  agree ms sp (rs#(ireg_of r) <- v).
+Proof.
+  intros. unfold preg_of in H. rewrite H0 in H. auto.
+Qed.
+Hint Resolve agree_set_mireg: ppcgen.
+
+Lemma agree_set_mfreg:
+  forall ms sp rs r v,
+  agree ms sp (rs#(preg_of r) <- v) ->
+  mreg_type r = Tfloat ->
+  agree ms sp (rs#(freg_of r) <- v).
+Proof.
+  intros. unfold preg_of in H. rewrite H0 in H. auto.
+Qed.
+Hint Resolve agree_set_mfreg: ppcgen.
+
+Lemma agree_set_other:
+  forall ms sp rs r v,
+  agree ms sp rs ->
+  ~(is_data_reg r) ->
+  agree ms sp (rs#r <- v).
+Proof.
+  intros. apply agree_exten_1 with rs.
+  auto. intros. apply Pregmap.gso. red; intro; subst r0; contradiction.
+Qed.
+Hint Resolve agree_set_other: ppcgen.
+
+Lemma agree_nextinstr:
+  forall ms sp rs,
+  agree ms sp rs -> agree ms sp (nextinstr rs).
+Proof.
+  intros. unfold nextinstr. apply agree_set_other. auto. auto.
+Qed.
+Hint Resolve agree_nextinstr: ppcgen.
+
+Lemma agree_set_mireg_twice:
+  forall ms sp rs r v v',
+  agree ms sp rs ->
+  mreg_type r = Tint ->
+  agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v).
+Proof.
+  intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros.
+  split. repeat (rewrite Pregmap.gso; auto with ppcgen).
+  intros. case (mreg_eq r r0); intro.
+  subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto.
+  assert (preg_of r <> preg_of r0). 
+    red; intro. elim n. apply preg_of_injective. auto.
+  rewrite Regmap.gso; auto.
+  repeat (rewrite Pregmap.gso; auto).
+  unfold preg_of. rewrite H0. auto.
+Qed.
+Hint Resolve agree_set_mireg_twice: ppcgen.
+
+Lemma agree_set_twice_mireg:
+  forall ms sp rs r v v',
+  agree (Regmap.set r v' ms) sp rs ->
+  mreg_type r = Tint ->
+  agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v).
+Proof.
+  intros. elim H; intros.
+  split. rewrite Pregmap.gso. auto. 
+  generalize (ireg_of_not_IR13 r); congruence.
+  intros. generalize (H2 r0). 
+  case (mreg_eq r0 r); intro.
+  subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0.
+  rewrite Pregmap.gss. auto.
+  repeat rewrite Regmap.gso; auto.
+  rewrite Pregmap.gso. auto. 
+  replace (IR (ireg_of r)) with (preg_of r).
+  red; intros. elim n. apply preg_of_injective; auto.
+  unfold preg_of. rewrite H0. auto.
+Qed.
+Hint Resolve agree_set_twice_mireg: ppcgen.
+
+Lemma agree_set_commut:
+  forall ms sp rs r1 r2 v1 v2,
+  r1 <> r2 ->
+  agree ms sp ((rs#r2 <- v2)#r1 <- v1) ->
+  agree ms sp ((rs#r1 <- v1)#r2 <- v2).
+Proof.
+  intros. apply agree_exten_1 with ((rs#r2 <- v2)#r1 <- v1). auto.
+  intros. 
+  case (preg_eq r r1); intro.
+  subst r1. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss.
+  auto. auto.
+  case (preg_eq r r2); intro.
+  subst r2. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss.
+  auto. auto.
+  repeat (rewrite Pregmap.gso; auto). 
+Qed. 
+Hint Resolve agree_set_commut: ppcgen.
+
+Lemma agree_nextinstr_commut:
+  forall ms sp rs r v,
+  agree ms sp (rs#r <- v) ->
+  r <> PC ->
+  agree ms sp ((nextinstr rs)#r <- v).
+Proof.
+  intros. unfold nextinstr. apply agree_set_commut. auto. 
+  apply agree_set_other. auto. auto. 
+Qed.
+Hint Resolve agree_nextinstr_commut: ppcgen.
+
+Lemma agree_set_mireg_exten:
+  forall ms sp rs r v (rs': regset),
+  agree ms sp rs ->
+  mreg_type r = Tint ->
+  rs'#(ireg_of r) = v ->
+  (forall r', r' <> PC -> r' <> ireg_of r -> r' <> IR14 -> rs'#r' = rs#r') ->
+  agree (Regmap.set r v ms) sp rs'.
+Proof.
+  intros. apply agree_exten_2 with (rs#(ireg_of r) <- v).
+  auto with ppcgen.
+  intros. unfold Pregmap.set. case (PregEq.eq r0 (ireg_of r)); intro.
+  subst r0. auto. apply H2; auto.
+Qed.
+
+(** Useful properties of the PC and GPR0 registers. *)
+
+Lemma nextinstr_inv:
+  forall r rs, r <> PC -> (nextinstr rs)#r = rs#r.
+Proof.
+  intros. unfold nextinstr. apply Pregmap.gso. auto.
+Qed.
+Hint Resolve nextinstr_inv: ppcgen.
+
+Lemma nextinstr_set_preg:
+  forall rs m v,
+  (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone.
+Proof.
+  intros. unfold nextinstr. rewrite Pregmap.gss. 
+  rewrite Pregmap.gso. auto. apply sym_not_eq. auto with ppcgen.
+Qed.
+Hint Resolve nextinstr_set_preg: ppcgen.
+
+(** Connection between Mach and Asm calling conventions for external
+    functions. *)
+
+Lemma extcall_arg_match:
+  forall ms sp rs m l v,
+  agree ms sp rs ->
+  Machconcr.extcall_arg ms m sp l v ->
+  Asm.extcall_arg rs m l v.
+Proof.
+  intros. inv H0. 
+  rewrite (preg_val _ _ _ r H). constructor.
+  rewrite (sp_val _ _ _ H) in H1.
+  destruct ty; unfold load_stack in H1.
+  econstructor. reflexivity. assumption.
+  econstructor. reflexivity. assumption.
+Qed.
+
+Lemma extcall_args_match:
+  forall ms sp rs m, agree ms sp rs ->
+  forall ll vl,
+  Machconcr.extcall_args ms m sp ll vl ->
+  Asm.extcall_args rs m ll vl.
+Proof.
+  induction 2; constructor; auto. eapply extcall_arg_match; eauto.
+Qed.
+
+Lemma extcall_arguments_match:
+  forall ms m sp rs sg args,
+  agree ms sp rs ->
+  Machconcr.extcall_arguments ms m sp sg args ->
+  Asm.extcall_arguments rs m sg args.
+Proof.
+  unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros.
+  eapply extcall_args_match; eauto.
+Qed.
+
+(** * Execution of straight-line code *)
+
+Section STRAIGHTLINE.
+
+Variable ge: genv.
+Variable fn: code.
+
+(** Straight-line code is composed of PPC instructions that execute
+  in sequence (no branches, no function calls and returns).
+  The following inductive predicate relates the machine states
+  before and after executing a straight-line sequence of instructions.
+  Instructions are taken from the first list instead of being fetched
+  from memory. *)
+
+Inductive exec_straight: code -> regset -> mem -> 
+                         code -> regset -> mem -> Prop :=
+  | exec_straight_one:
+      forall i1 c rs1 m1 rs2 m2,
+      exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
+      rs2#PC = Val.add rs1#PC Vone ->
+      exec_straight (i1 :: c) rs1 m1 c rs2 m2
+  | exec_straight_step:
+      forall i c rs1 m1 rs2 m2 c' rs3 m3,
+      exec_instr ge fn i rs1 m1 = OK rs2 m2 ->
+      rs2#PC = Val.add rs1#PC Vone ->
+      exec_straight c rs2 m2 c' rs3 m3 ->
+      exec_straight (i :: c) rs1 m1 c' rs3 m3.
+
+Lemma exec_straight_trans:
+  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
+  exec_straight c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight c1 rs1 m1 c3 rs3 m3.
+Proof.
+  induction 1; intros.
+  apply exec_straight_step with rs2 m2; auto.
+  apply exec_straight_step with rs2 m2; auto.
+Qed.
+
+Lemma exec_straight_two:
+  forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
+  exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
+  exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
+  rs2#PC = Val.add rs1#PC Vone ->
+  rs3#PC = Val.add rs2#PC Vone ->
+  exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  apply exec_straight_one; auto.
+Qed.
+
+Lemma exec_straight_three:
+  forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
+  exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
+  exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
+  exec_instr ge fn i3 rs3 m3 = OK rs4 m4 ->
+  rs2#PC = Val.add rs1#PC Vone ->
+  rs3#PC = Val.add rs2#PC Vone ->
+  rs4#PC = Val.add rs3#PC Vone ->
+  exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  eapply exec_straight_two; eauto.
+Qed.
+
+Lemma exec_straight_four:
+  forall i1 i2 i3 i4 c rs1 m1 rs2 m2 rs3 m3 rs4 m4 rs5 m5,
+  exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
+  exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
+  exec_instr ge fn i3 rs3 m3 = OK rs4 m4 ->
+  exec_instr ge fn i4 rs4 m4 = OK rs5 m5 ->
+  rs2#PC = Val.add rs1#PC Vone ->
+  rs3#PC = Val.add rs2#PC Vone ->
+  rs4#PC = Val.add rs3#PC Vone ->
+  rs5#PC = Val.add rs4#PC Vone ->
+  exec_straight (i1 :: i2 :: i3 :: i4 :: c) rs1 m1 c rs5 m5.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  eapply exec_straight_three; eauto.
+Qed.
+
+(** * Correctness of ARM constructor functions *)
+
+(** Properties of comparisons. *)
+(*
+Lemma compare_float_spec:
+  forall rs v1 v2,
+  let rs1 := nextinstr (compare_float rs v1 v2) in
+     rs1#CR0_0 = Val.cmpf Clt v1 v2
+  /\ rs1#CR0_1 = Val.cmpf Cgt v1 v2
+  /\ rs1#CR0_2 = Val.cmpf Ceq v1 v2
+  /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
+       r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
+Proof.
+  intros. unfold rs1.
+  split. reflexivity.
+  split. reflexivity.
+  split. reflexivity.
+  intros. rewrite nextinstr_inv; auto.
+  unfold compare_float. repeat (rewrite Pregmap.gso; auto).
+Qed.
+
+Lemma compare_sint_spec:
+  forall rs v1 v2,
+  let rs1 := nextinstr (compare_sint rs v1 v2) in
+     rs1#CR0_0 = Val.cmp Clt v1 v2
+  /\ rs1#CR0_1 = Val.cmp Cgt v1 v2
+  /\ rs1#CR0_2 = Val.cmp Ceq v1 v2
+  /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
+       r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
+Proof.
+  intros. unfold rs1.
+  split. reflexivity.
+  split. reflexivity.
+  split. reflexivity.
+  intros. rewrite nextinstr_inv; auto.
+  unfold compare_sint. repeat (rewrite Pregmap.gso; auto).
+Qed.
+
+Lemma compare_uint_spec:
+  forall rs v1 v2,
+  let rs1 := nextinstr (compare_uint rs v1 v2) in
+     rs1#CR0_0 = Val.cmpu Clt v1 v2
+  /\ rs1#CR0_1 = Val.cmpu Cgt v1 v2
+  /\ rs1#CR0_2 = Val.cmpu Ceq v1 v2
+  /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
+       r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
+Proof.
+  intros. unfold rs1.
+  split. reflexivity.
+  split. reflexivity.
+  split. reflexivity.
+  intros. rewrite nextinstr_inv; auto.
+  unfold compare_uint. repeat (rewrite Pregmap.gso; auto).
+Qed.
+*)
+
+(** Loading a constant. *)
+
+Lemma loadimm_correct:
+  forall r n k rs m,
+  exists rs',
+     exec_straight (loadimm r n k) rs m  k rs' m
+  /\ rs'#r = Vint n
+  /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+  intros. unfold loadimm.
+  case (is_immed_arith n).
+  (* single move *)
+  exists (nextinstr (rs#r <- (Vint n))).
+  split. apply exec_straight_one. reflexivity. reflexivity.  
+  split. rewrite nextinstr_inv; auto with ppcgen.
+   apply Pregmap.gss. 
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  case (is_immed_arith (Int.not n)).
+  (* single move-complement *)
+  exists (nextinstr (rs#r <- (Vint n))).
+  split. apply exec_straight_one.
+  simpl. change (Int.xor (Int.not n) Int.mone) with (Int.not (Int.not n)).
+  rewrite Int.not_involutive. auto.
+  reflexivity.
+  split. rewrite nextinstr_inv; auto with ppcgen.
+   apply Pregmap.gss. 
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  (* mov - or - or - or *)
+  set (n1 := Int.and n (Int.repr 255)).
+  set (n2 := Int.and n (Int.repr 65280)).
+  set (n3 := Int.and n (Int.repr 16711680)).
+  set (n4 := Int.and n (Int.repr 4278190080)).
+  set (rs1 := nextinstr (rs#r <- (Vint n1))).
+  set (rs2 := nextinstr (rs1#r <- (Val.or rs1#r (Vint n2)))).
+  set (rs3 := nextinstr (rs2#r <- (Val.or rs2#r (Vint n3)))).
+  set (rs4 := nextinstr (rs3#r <- (Val.or rs3#r (Vint n4)))).
+  exists rs4.
+  split. apply exec_straight_four with rs1 m rs2 m rs3 m; auto. 
+  split. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  unfold rs3. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
+  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
+  repeat rewrite Val.or_assoc. simpl. decEq. 
+  unfold n4, n3, n2, n1. repeat rewrite <- Int.and_or_distrib. 
+  change (Int.and n Int.mone = n). apply Int.and_mone.
+  intros. 
+  unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  unfold rs3. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+Qed.
+
+(** Add integer immediate. *)
+
+Lemma addimm_correct:
+  forall r1 r2 n k rs m,
+  exists rs',
+     exec_straight (addimm r1 r2 n k) rs m  k rs' m
+  /\ rs'#r1 = Val.add rs#r2 (Vint n)
+  /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+  intros. unfold addimm.
+  (* addi *)
+  case (is_immed_arith n).
+  exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))).
+  split. apply exec_straight_one; auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  (* subi *)
+  case (is_immed_arith (Int.neg n)).
+  exists (nextinstr (rs#r1 <- (Val.sub rs#r2 (Vint (Int.neg n))))).
+  split. apply exec_straight_one; auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
+    apply Val.sub_opp_add.
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  (* general *)
+  set (n1 := Int.and n (Int.repr 255)).
+  set (n2 := Int.and n (Int.repr 65280)).
+  set (n3 := Int.and n (Int.repr 16711680)).
+  set (n4 := Int.and n (Int.repr 4278190080)).
+  set (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n1)))).
+  set (rs2 := nextinstr (rs1#r1 <- (Val.add rs1#r1 (Vint n2)))).
+  set (rs3 := nextinstr (rs2#r1 <- (Val.add rs2#r1 (Vint n3)))).
+  set (rs4 := nextinstr (rs3#r1 <- (Val.add rs3#r1 (Vint n4)))).
+  exists rs4.
+  split. apply exec_straight_four with rs1 m rs2 m rs3 m; auto. 
+  simpl. 
+  split. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  unfold rs3. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
+  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
+  repeat rewrite Val.add_assoc. simpl. decEq. decEq. 
+  unfold n4, n3, n2, n1. repeat rewrite Int.add_and.
+  change (Int.and n Int.mone = n). apply Int.and_mone.
+  vm_compute; auto.
+  vm_compute; auto.
+  vm_compute; auto.
+  intros.
+  unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  unfold rs3. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+Qed.
+
+(* And integer immediate *)
+
+Lemma andimm_correct:
+  forall r1 r2 n k rs m,
+  r2 <> IR14 ->
+  exists rs',
+     exec_straight (andimm r1 r2 n k) rs m  k rs' m
+  /\ rs'#r1 = Val.and rs#r2 (Vint n)
+  /\ forall r': preg, r' <> r1 -> r' <> IR14 -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+  intros. unfold andimm.
+  (* andi *)
+  case (is_immed_arith n).
+  exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))).
+  split. apply exec_straight_one; auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  (* bici *)
+  case (is_immed_arith (Int.not n)).
+  exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))).
+  split. apply exec_straight_one; auto. simpl.
+    change (Int.xor (Int.not n) Int.mone) with (Int.not (Int.not n)).
+    rewrite Int.not_involutive. auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  (* general *)
+  exploit loadimm_correct. intros [rs' [A [B C]]].
+  exists (nextinstr (rs'#r1 <- (Val.and rs#r2 (Vint n)))).
+  split. eapply exec_straight_trans. eauto. apply exec_straight_one.
+  simpl. rewrite B. rewrite C; auto with ppcgen. congruence.
+  auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
+  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+Qed.
+
+(** Other integer immediate *)
+
+Lemma makeimm_correct:
+  forall (instr: ireg -> ireg -> shift_op -> instruction)
+         (sem: val -> val -> val)
+         r1 (r2: ireg) n k (rs : regset) m,
+  (forall c r1 r2 so rs m,
+   exec_instr ge c (instr r1 r2 so) rs m 
+   = OK (nextinstr rs#r1 <- (sem rs#r2 (eval_shift_op so rs))) m) ->
+   r2 <> IR14 ->
+  exists rs',
+     exec_straight (makeimm instr r1 r2 n k) rs m  k rs' m
+  /\ rs'#r1 = sem rs#r2 (Vint n)
+  /\ forall r': preg, r' <> r1 -> r' <> PC -> r' <> IR14 -> rs'#r' = rs#r'.
+Proof.
+  intros. unfold makeimm.
+  case (is_immed_arith n).
+  (* one immed instr *)
+  exists (nextinstr (rs#r1 <- (sem rs#r2 (Vint n)))).
+  split. apply exec_straight_one. 
+    change (Vint n) with (eval_shift_op (SOimm n) rs). auto.
+    auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  (* general case *)
+  exploit loadimm_correct. intros [rs' [A [B C]]].
+  exists (nextinstr (rs'#r1 <- (sem rs#r2 (Vint n)))).
+  split. eapply exec_straight_trans. eauto. apply exec_straight_one. 
+    rewrite <- B. rewrite <- (C r2). 
+    change (rs' IR14) with (eval_shift_op (SOreg IR14) rs'). auto.
+    congruence. auto with ppcgen. auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
+  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto with ppcgen.
+Qed.
+
+(** Indexed memory loads. *)
+
+Lemma loadind_int_correct:
+  forall (base: ireg) ofs dst (rs: regset) m v k,
+  Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v ->
+  exists rs',
+     exec_straight (loadind_int base ofs dst k) rs m k rs' m
+  /\ rs'#dst = v
+  /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r.
+Proof.
+  intros; unfold loadind_int. destruct (is_immed_mem_word ofs).
+  exists (nextinstr (rs#dst <- v)).
+  split. apply exec_straight_one. simpl. 
+    unfold exec_load. rewrite H. auto. auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  exploit addimm_correct. intros [rs' [A [B C]]].
+  exists (nextinstr (rs'#dst <- v)).
+  split. eapply exec_straight_trans. eauto. apply exec_straight_one.
+    simpl. unfold exec_load. rewrite B.
+    rewrite Val.add_assoc. simpl. rewrite Int.add_zero.
+    rewrite H. auto.
+    auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
+  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+Qed.
+
+Lemma loadind_float_correct:
+  forall (base: ireg) ofs dst (rs: regset) m v k,
+  Mem.loadv Mfloat64 m (Val.add rs#base (Vint ofs)) = Some v ->
+  exists rs',
+     exec_straight (loadind_float base ofs dst k) rs m k rs' m
+  /\ rs'#dst = v
+  /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r.
+Proof.
+  intros; unfold loadind_float. destruct (is_immed_mem_float ofs).
+  exists (nextinstr (rs#dst <- v)).
+  split. apply exec_straight_one. simpl. 
+    unfold exec_load. rewrite H. auto. auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
+  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  exploit addimm_correct. eauto. intros [rs' [A [B C]]].
+  exists (nextinstr (rs'#dst <- v)).
+  split. eapply exec_straight_trans. eauto. apply exec_straight_one.
+    simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl. 
+    rewrite Int.add_zero. rewrite H. auto. auto.
+  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
+  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+Qed.
+
+Lemma loadind_correct:
+  forall (base: ireg) ofs ty dst k (rs: regset) m v,
+  Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
+  mreg_type dst = ty ->
+  exists rs',
+     exec_straight (loadind base ofs ty dst k) rs m k rs' m
+  /\ rs'#(preg_of dst) = v
+  /\ forall r, r <> PC -> r <> IR14 -> r <> preg_of dst -> rs'#r = rs#r.
+Proof.
+  intros. unfold loadind. 
+  assert (preg_of dst <> PC).
+    unfold preg_of. case (mreg_type dst); discriminate.
+  unfold preg_of. rewrite H0. destruct ty.
+  apply loadind_int_correct; auto.
+  apply loadind_float_correct; auto.
+Qed.
+
+(** Indexed memory stores. *)
+
+Lemma storeind_int_correct:
+  forall (base: ireg) ofs (src: ireg) (rs: regset) m m' k,
+  Mem.storev Mint32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' ->
+  src <> IR14 ->
+  exists rs',
+     exec_straight (storeind_int src base ofs k) rs m k rs' m'
+  /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r.
+Proof.
+  intros; unfold storeind_int. destruct (is_immed_mem_word ofs).
+  exists (nextinstr rs).
+  split. apply exec_straight_one. simpl. 
+    unfold exec_store. rewrite H. auto. auto.
+  intros. rewrite nextinstr_inv; auto.
+  exploit addimm_correct. eauto. intros [rs' [A [B C]]].
+  exists (nextinstr rs').
+  split. eapply exec_straight_trans. eauto. apply exec_straight_one.
+    simpl. unfold exec_store. rewrite B. rewrite C.
+    rewrite Val.add_assoc. simpl. rewrite Int.add_zero. 
+    rewrite H. auto. 
+    congruence. auto with ppcgen. auto.
+  intros. rewrite nextinstr_inv; auto.
+Qed.
+
+Lemma storeind_float_correct:
+  forall (base: ireg) ofs (src: freg) (rs: regset) m m' k,
+  Mem.storev Mfloat64 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' ->
+  base <> IR14 ->
+  exists rs',
+     exec_straight (storeind_float src base ofs k) rs m k rs' m'
+  /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r.
+Proof.
+  intros; unfold storeind_float. destruct (is_immed_mem_float ofs).
+  exists (nextinstr rs).
+  split. apply exec_straight_one. simpl. 
+    unfold exec_store. rewrite H. auto. auto.
+  intros. rewrite nextinstr_inv; auto.
+  exploit addimm_correct. eauto. intros [rs' [A [B C]]].
+  exists (nextinstr rs').
+  split. eapply exec_straight_trans. eauto. apply exec_straight_one.
+    simpl. unfold exec_store. rewrite B. rewrite C.
+    rewrite Val.add_assoc. simpl. rewrite Int.add_zero. 
+    rewrite H. auto.
+    congruence. congruence. auto with ppcgen. auto.
+  intros. rewrite nextinstr_inv; auto.
+Qed.
+
+Lemma storeind_correct:
+  forall (base: ireg) ofs ty src k (rs: regset) m m',
+  Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
+  mreg_type src = ty ->
+  base <> IR14 ->
+  exists rs',
+     exec_straight (storeind src base ofs ty k) rs m k rs' m'
+  /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r.
+Proof.
+  intros. unfold storeind. unfold preg_of in H. rewrite H0 in H. destruct ty.
+  apply storeind_int_correct. auto. auto. auto with ppcgen.
+  apply storeind_float_correct. auto. auto.
+Qed.
+
+(** Translation of shift immediates *)
+
+Lemma transl_shift_correct:
+  forall s (r: ireg) (rs: regset),
+  eval_shift_op (transl_shift s r) rs = eval_shift_total s (rs#r).
+Proof.
+  intros. destruct s; simpl;
+  unfold eval_shift_total, eval_shift, Val.shl, Val.shr, Val.shru, Val.ror;
+  rewrite (s_amount_ltu s); auto.
+Qed.
+
+Lemma transl_shift_addr_correct:
+  forall s (r: ireg) (rs: regset),
+  eval_shift_addr (transl_shift_addr s r) rs = eval_shift_total s (rs#r).
+Proof.
+  intros. destruct s; simpl;
+  unfold eval_shift_total, eval_shift, Val.shl, Val.shr, Val.shru, Val.ror;
+  rewrite (s_amount_ltu s); auto.
+Qed.
+
+(** Translation of conditions *)
+
+Ltac TypeInv :=
+  match goal with
+  | H: (List.map ?f ?x = nil) |- _ =>
+      destruct x; [clear H | simpl in H; discriminate]
+  | H: (List.map ?f ?x = ?hd :: ?tl) |- _ =>
+      destruct x; simpl in H;
+      [ discriminate |
+        injection H; clear H; let T := fresh "T" in (
+          intros H T; TypeInv) ]
+  | _ => idtac
+  end.
+
+(** Translation of conditions. *)
+
+Lemma compare_int_spec:
+  forall rs v1 v2,
+  let rs1 := nextinstr (compare_int rs v1 v2) in
+     rs1#CReq = (Val.cmp Ceq v1 v2)
+  /\ rs1#CRne = (Val.cmp Cne v1 v2)
+  /\ rs1#CRhs = (Val.cmpu Cge v1 v2)
+  /\ rs1#CRlo = (Val.cmpu Clt v1 v2)
+  /\ rs1#CRhi = (Val.cmpu Cgt v1 v2)
+  /\ rs1#CRls = (Val.cmpu Cle v1 v2)
+  /\ rs1#CRge = (Val.cmp Cge v1 v2)
+  /\ rs1#CRlt = (Val.cmp Clt v1 v2)
+  /\ rs1#CRgt = (Val.cmp Cgt v1 v2)
+  /\ rs1#CRle = (Val.cmp Cle v1 v2)
+  /\ forall r', is_data_reg r' -> rs1#r' = rs#r'.
+Proof.
+  intros. unfold rs1. intuition; try reflexivity. 
+  rewrite nextinstr_inv; [unfold compare_int; repeat rewrite Pregmap.gso; auto | idtac];
+  red; intro; subst r'; elim H.
+Qed.
+
+Lemma compare_float_spec:
+  forall rs v1 v2,
+  let rs' := nextinstr (compare_float rs v1 v2) in
+     rs'#CReq = (Val.cmpf Ceq v1 v2)
+  /\ rs'#CRne = (Val.cmpf Cne v1 v2)
+  /\ rs'#CRmi = (Val.cmpf Clt v1 v2)              
+  /\ rs'#CRpl = (Val.notbool (Val.cmpf Clt v1 v2))
+  /\ rs'#CRhi = (Val.notbool (Val.cmpf Cle v1 v2))
+  /\ rs'#CRls = (Val.cmpf Cle v1 v2)              
+  /\ rs'#CRge = (Val.cmpf Cge v1 v2)              
+  /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2))
+  /\ rs'#CRgt = (Val.cmpf Cgt v1 v2)               
+  /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2))
+  /\ forall r', is_data_reg r' -> rs'#r' = rs#r'.
+Proof.
+  intros. unfold rs'. intuition; try reflexivity. 
+  rewrite nextinstr_inv; [unfold compare_float; repeat rewrite Pregmap.gso; auto | idtac];
+  red; intro; subst r'; elim H.
+Qed.
+
+Lemma transl_cond_correct:
+  forall cond args k ms sp rs m b,
+  map mreg_type args = type_of_condition cond ->
+  agree ms sp rs ->
+  eval_condition cond (map ms args) m = Some b ->
+  exists rs',
+     exec_straight (transl_cond cond args k) rs m k rs' m
+  /\ rs'#(CR (crbit_for_cond cond)) = Val.of_bool b
+  /\ agree ms sp rs'.
+Proof.
+  intros.
+  rewrite <- (eval_condition_weaken _ _ _ H1). clear H1. 
+  destruct cond; simpl in H; TypeInv; simpl.
+  (* Ccomp *)
+  generalize (compare_int_spec rs ms#m0 ms#m1).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_int rs ms#m0 ms#m1)).
+  split. apply exec_straight_one. simpl. 
+  repeat rewrite <- (ireg_val ms sp rs); trivial. 
+  reflexivity.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs; auto.
+  (* Ccompu *)
+  generalize (compare_int_spec rs ms#m0 ms#m1).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_int rs ms#m0 ms#m1)).
+  split. apply exec_straight_one. simpl. 
+  repeat rewrite <- (ireg_val ms sp rs); trivial. 
+  reflexivity.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs; auto.
+  (* Ccompshift *)
+  generalize (compare_int_spec rs ms#m0 (eval_shift_total s ms#m1)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_int rs ms#m0 (eval_shift_total s ms#m1))).
+  split. apply exec_straight_one. simpl.
+  rewrite transl_shift_correct. 
+  repeat rewrite <- (ireg_val ms sp rs); trivial.
+  reflexivity.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs; auto.
+  (* Ccompushift *)
+  generalize (compare_int_spec rs ms#m0 (eval_shift_total s ms#m1)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_int rs ms#m0 (eval_shift_total s ms#m1))).
+  split. apply exec_straight_one. simpl.
+  rewrite transl_shift_correct. 
+  repeat rewrite <- (ireg_val ms sp rs); trivial.
+  reflexivity.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs; auto.
+  (* Ccompimm *)
+  destruct (is_immed_arith i).
+  generalize (compare_int_spec rs ms#m0 (Vint i)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_int rs ms#m0 (Vint i))).
+  split. apply exec_straight_one. simpl. 
+  rewrite <- (ireg_val ms sp rs); trivial. auto.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs; auto.
+  exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
+  assert (AG: agree ms sp rs'). apply agree_exten_2 with rs; auto. 
+  generalize (compare_int_spec rs' ms#m0 (Vint i)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_int rs' ms#m0 (Vint i))).
+  split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
+  rewrite Q. rewrite <- (ireg_val ms sp rs'); trivial. auto.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs'; auto.
+  (* Ccompuimm *)
+  destruct (is_immed_arith i).
+  generalize (compare_int_spec rs ms#m0 (Vint i)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_int rs ms#m0 (Vint i))).
+  split. apply exec_straight_one. simpl. 
+  rewrite <- (ireg_val ms sp rs); trivial. auto.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs; auto.
+  exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
+  assert (AG: agree ms sp rs'). apply agree_exten_2 with rs; auto. 
+  generalize (compare_int_spec rs' ms#m0 (Vint i)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_int rs' ms#m0 (Vint i))).
+  split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
+  rewrite Q. rewrite <- (ireg_val ms sp rs'); trivial. auto.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs'; auto.
+  (* Ccompf *)
+  generalize (compare_float_spec rs ms#m0 ms#m1).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_float rs ms#m0 ms#m1)).
+  split. apply exec_straight_one. simpl. 
+  repeat rewrite <- (freg_val ms sp rs); trivial. auto.
+  split. 
+  case c; simpl; auto.
+  apply agree_exten_1 with rs; auto.
+  (* Cnotcompf *)
+  generalize (compare_float_spec rs ms#m0 ms#m1).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  exists (nextinstr (compare_float rs ms#m0 ms#m1)).
+  split. apply exec_straight_one. simpl. 
+  repeat rewrite <- (freg_val ms sp rs); trivial. auto.
+  split. 
+  case c; simpl; auto.
+    rewrite Val.negate_cmpf_ne. auto.
+    rewrite Val.negate_cmpf_eq. auto.
+  apply agree_exten_1 with rs; auto.
+Qed.
+
+(** Translation of arithmetic operations. *)
+
+Ltac TranslOpSimpl :=
+  match goal with
+  | |- exists rs' : regset,
+         exec_straight ?c ?rs ?m ?k rs' ?m /\
+         agree (Regmap.set ?res ?v ?ms) ?sp rs'  =>
+    (exists (nextinstr (rs#(ireg_of res) <- v));
+     split; 
+     [ apply exec_straight_one;
+       [ repeat (rewrite (ireg_val ms sp rs); auto);
+         simpl; try rewrite transl_shift_correct; reflexivity
+       | reflexivity ]
+     | auto with ppcgen ])
+  ||
+    (exists (nextinstr (rs#(freg_of res) <- v));
+     split; 
+     [ apply exec_straight_one;
+       [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity
+       | reflexivity ]
+     | auto with ppcgen ])
+  end.
+
+Lemma transl_op_correct:
+  forall op args res k ms sp rs m v,
+  wt_instr (Mop op args res) ->
+  agree ms sp rs ->
+  eval_operation ge sp op (map ms args) m = Some v ->
+  exists rs',
+     exec_straight (transl_op op args res k) rs m k rs' m
+  /\ agree (Regmap.set res v ms) sp rs'.
+Proof.
+  intros. rewrite <- (eval_operation_weaken _ _ _ _ _ H1). (*clear H1; clear v.*)
+  inversion H.
+  (* Omove *)
+  simpl. exists (nextinstr (rs#(preg_of res) <- (ms r1))).
+  split. caseEq (mreg_type r1); intro.
+  apply exec_straight_one. simpl. rewrite (ireg_val ms sp rs); auto.
+  simpl. unfold preg_of. rewrite <- H3. rewrite H6. reflexivity.
+  auto with ppcgen.
+  apply exec_straight_one. simpl. rewrite (freg_val ms sp rs); auto.
+  simpl. unfold preg_of. rewrite <- H3. rewrite H6. reflexivity.
+  auto with ppcgen.
+  auto with ppcgen.
+  (* Other instructions *)
+  clear H2 H3 H5. 
+  destruct op; simpl in H6; injection H6; clear H6; intros;
+  TypeInv; simpl; try (TranslOpSimpl).
+  (* Omove again *)
+  congruence.
+  (* Ointconst *)
+  generalize (loadimm_correct (ireg_of res) i k rs m).
+  intros [rs' [A [B C]]]. 
+  exists rs'. split. auto. 
+  apply agree_set_mireg_exten with rs; auto. 
+(*
+  (* Ofloatconst *)
+  exists (nextinstr (rs#(freg_of res) <- (Vfloat f))).
+  split. apply exec_straight_one. reflexivity. reflexivity.
+  auto with ppcgen.
+  (* Oaddrsymbol *)
+  change (find_symbol_offset ge i i0) with (symbol_offset ge i i0).
+  set (v := symbol_offset ge i i0).
+  pose (rs1 := nextinstr (rs#GPR2 <- (high_half v))).
+  exists (nextinstr (rs1#(ireg_of res) <- v)).
+  split. apply exec_straight_two with rs1 m.
+  unfold exec_instr. rewrite gpr_or_zero_zero.
+  unfold const_high. rewrite Val.add_commut. 
+  rewrite high_half_zero. reflexivity. 
+  simpl. rewrite gpr_or_zero_not_zero. 2: congruence. 
+  unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen.
+  rewrite Pregmap.gss. 
+  fold v. rewrite Val.add_commut. unfold v. rewrite low_high_half.
+  reflexivity. reflexivity. reflexivity. 
+  unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto.
+  apply agree_set_mreg. apply agree_nextinstr.
+  apply agree_set_other. auto. simpl. tauto.
+*)
+  (* Oaddrstack *)
+  generalize (addimm_correct (ireg_of res) IR13 i k rs m). 
+  intros [rs' [EX [RES OTH]]].
+  exists rs'. split. auto. 
+  apply agree_set_mireg_exten with rs; auto.
+  rewrite (sp_val ms sp rs). auto. auto.
+  (* Ocast8signed *)
+  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 24))))).
+  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 24))))).
+  exists rs2. split.
+  apply exec_straight_two with rs1 m; auto.
+  simpl. rewrite <- (ireg_val ms sp rs); auto.
+  unfold rs2. 
+  replace (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 24))) with (Val.sign_ext 8 (ms m0)).
+  apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut.
+  apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. 
+  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  destruct (ms m0); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
+  vm_compute; auto. 
+  (* Ocast8unsigned *)
+  exists (nextinstr (rs#(ireg_of res) <- (Val.and (ms m0) (Vint (Int.repr 255))))).
+  split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
+  replace (Val.zero_ext 8 (ms m0))
+      with (Val.and (ms m0) (Vint (Int.repr 255))).
+  auto with ppcgen. 
+  destruct (ms m0); simpl; auto. rewrite Int.zero_ext_and. reflexivity. 
+  vm_compute; auto.
+  (* Ocast16signed *)
+  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 16))))).
+  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 16))))).
+  exists rs2. split.
+  apply exec_straight_two with rs1 m; auto.
+  simpl. rewrite <- (ireg_val ms sp rs); auto. 
+  unfold rs2. 
+  replace (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 16))) with (Val.sign_ext 16 (ms m0)).
+  apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut.
+  apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. 
+  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  destruct (ms m0); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
+  vm_compute; auto. 
+  (* Ocast16unsigned *)
+  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 16))))).
+  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shru (rs1 (ireg_of res)) (Vint (Int.repr 16))))).
+  exists rs2. split.
+  apply exec_straight_two with rs1 m; auto.
+  simpl. rewrite <- (ireg_val ms sp rs); auto. 
+  unfold rs2. 
+  replace (Val.shru (rs1 (ireg_of res)) (Vint (Int.repr 16))) with (Val.zero_ext 16 (ms m0)).
+  apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut.
+  apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. 
+  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  destruct (ms m0); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity.
+  vm_compute; auto. 
+  (* Oaddimm *)
+  generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m).
+  intros [rs' [A [B C]]]. 
+  exists rs'. split. auto.
+  apply agree_set_mireg_exten with rs; auto.
+  rewrite (ireg_val ms sp rs); auto. 
+  (* Orsbimm *)
+  exploit (makeimm_correct Prsb (fun v1 v2 => Val.sub v2 v1) (ireg_of res) (ireg_of m0));
+  auto with ppcgen.
+  intros [rs' [A [B C]]].
+  exists rs'.
+  split. eauto.
+  apply agree_set_mireg_exten with rs; auto. rewrite B. 
+  rewrite <- (ireg_val ms sp rs); auto. 
+  (* Omul *)
+  destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)).
+  set (rs1 := nextinstr (rs#IR14 <- (Val.mul (ms m0) (ms m1)))).
+  set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#IR14))).
+  exists rs2; split.
+  apply exec_straight_two with rs1 m; auto.
+  simpl. repeat rewrite <- (ireg_val ms sp rs); auto.
+  unfold rs2. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. 
+  apply agree_nextinstr. apply agree_nextinstr_commut. 
+  apply agree_set_mireg; auto.  apply agree_set_mreg. apply agree_set_other. auto.
+  simpl; auto. auto with ppcgen. discriminate.
+  TranslOpSimpl.
+  (* Oandimm *)
+  generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m
+                            (ireg_of_not_IR14 m0)).
+  intros [rs' [A [B C]]]. 
+  exists rs'. split. auto.
+  apply agree_set_mireg_exten with rs; auto.
+  rewrite (ireg_val ms sp rs); auto. 
+  (* Oorimm *)
+  exploit (makeimm_correct Porr Val.or (ireg_of res) (ireg_of m0));
+  auto with ppcgen.
+  intros [rs' [A [B C]]].
+  exists rs'.
+  split. eauto.
+  apply agree_set_mireg_exten with rs; auto. rewrite B. 
+  rewrite <- (ireg_val ms sp rs); auto. 
+  (* Oxorimm *)
+  exploit (makeimm_correct Peor Val.xor (ireg_of res) (ireg_of m0));
+  auto with ppcgen.
+  intros [rs' [A [B C]]].
+  exists rs'.
+  split. eauto.
+  apply agree_set_mireg_exten with rs; auto. rewrite B. 
+  rewrite <- (ireg_val ms sp rs); auto.
+  (* Oshrximm *)
+  assert (exists n, ms m0 = Vint n /\ Int.ltu i (Int.repr 31) = true).
+    simpl in H1. destruct (ms m0); try discriminate.
+    exists i0; split; auto. destruct (Int.ltu i (Int.repr 31)); discriminate || auto.
+  destruct H3 as [n [ARG1 LTU]].
+  assert (LTU': Int.ltu i (Int.repr 32) = true).
+    exploit Int.ltu_inv. eexact LTU. intro.
+    unfold Int.ltu. apply zlt_true.
+    assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto.
+    omega.
+  assert (RSm0: rs (ireg_of m0) = Vint n).
+    rewrite <- ARG1. symmetry. eapply ireg_val; eauto. 
+  set (islt := Int.lt n Int.zero).
+  set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero))).
+  assert (OTH1: forall r', is_data_reg r' -> rs1#r' = rs#r').
+    generalize (compare_int_spec rs (Vint n) (Vint Int.zero)).
+    fold rs1. intros [A B]. intuition.
+  exploit (addimm_correct IR14 (ireg_of m0) (Int.sub (Int.shl Int.one i) Int.one)).
+  intros [rs2 [EXEC2 [RES2 OTH2]]].
+  set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))).
+  set (rs4 := nextinstr (rs3#(ireg_of res) <- (Val.shr rs3#IR14 (Vint i)))).
+  exists rs4; split.
+  apply exec_straight_step with rs1 m.
+  simpl. rewrite RSm0. auto. auto.
+  eapply exec_straight_trans. eexact EXEC2.
+  apply exec_straight_two with rs3 m.
+  simpl. rewrite OTH2. change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)).
+    unfold Val.cmp. change (Int.cmp Cge n Int.zero) with (negb islt).
+    rewrite OTH2. rewrite OTH1. rewrite RSm0. 
+    unfold rs3. case islt; reflexivity.
+    apply ireg_of_is_data_reg. decEq; auto with ppcgen. auto with ppcgen. congruence. congruence.
+  simpl. auto. 
+  auto. unfold rs3. case islt; auto. auto.
+  (* agreement *)
+  assert (RES4: rs4#(ireg_of res) = Vint(Int.shrx n i)).
+    unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gss.
+    rewrite Int.shrx_shr. fold islt. unfold rs3.
+    repeat rewrite nextinstr_inv; auto. 
+    case islt. rewrite RES2. rewrite OTH1. rewrite RSm0. 
+    simpl. rewrite LTU'. auto.
+    apply ireg_of_is_data_reg. 
+    rewrite Pregmap.gss. simpl. rewrite LTU'. auto. congruence.
+    exact LTU. auto with ppcgen. 
+  assert (OTH4: forall r, is_data_reg r -> r <> ireg_of res -> rs4#r = rs#r).
+    intros. 
+    assert (r <> PC). red; intro; subst r; elim H3.
+    assert (r <> IR14). red; intro; subst r; elim H3.
+    unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+    unfold rs3. rewrite nextinstr_inv; auto.
+    transitivity (rs2 r).
+    case islt. auto. apply Pregmap.gso; auto.
+    rewrite OTH2; auto. 
+  apply agree_exten_1 with (rs#(ireg_of res) <- (Val.shrx (ms m0) (Vint i))).
+  auto with ppcgen.
+  intros. unfold Pregmap.set. destruct (PregEq.eq r (ireg_of res)).
+  subst r. rewrite ARG1. simpl. rewrite LTU'. auto.
+  auto.
+  (* Ointoffloat *)
+  exists (nextinstr (rs#(ireg_of res) <- (Val.intoffloat (ms m0)))).
+  split. apply exec_straight_one. 
+  repeat (rewrite (freg_val ms sp rs); auto).
+  reflexivity. auto with ppcgen.
+  (* Ointuoffloat *)
+  exists (nextinstr (rs#(ireg_of res) <- (Val.intuoffloat (ms m0)))).
+  split. apply exec_straight_one. 
+  repeat (rewrite (freg_val ms sp rs); auto).
+  reflexivity. auto with ppcgen.
+  (* Ofloatofint *)
+  exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)))).
+  split. apply exec_straight_one. 
+  repeat (rewrite (ireg_val ms sp rs); auto).
+  reflexivity. auto 10 with ppcgen.
+  (* Ofloatofintu *)
+  exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)))).
+  split. apply exec_straight_one. 
+  repeat (rewrite (ireg_val ms sp rs); auto).
+  reflexivity. auto 10 with ppcgen.
+  (* Ocmp *)
+  assert (exists b, eval_condition c ms##args m = Some b /\ v = Val.of_bool b).
+    simpl in H1. destruct (eval_condition c ms##args m). 
+    destruct b; inv H1. exists true; auto. exists false; auto.
+    discriminate.
+  destruct H5 as [b [EVC EQ]].
+  exploit transl_cond_correct; eauto. intros [rs' [A [B C]]].
+  rewrite (eval_condition_weaken _ _ _ EVC).
+  set (rs1 := nextinstr (rs'#(ireg_of res) <- (Vint Int.zero))).
+  set (rs2 := nextinstr (if b then (rs1#(ireg_of res) <- Vtrue) else rs1)).
+  exists rs2; split.
+  eapply exec_straight_trans. eauto. 
+  apply exec_straight_two with rs1 m; auto.
+  simpl. replace (rs1 (crbit_for_cond c)) with (Val.of_bool b).
+  unfold rs2. destruct b; auto. 
+  unfold rs2. destruct b; auto.
+  apply agree_set_mireg_exten with rs'; auto.
+  unfold rs2. rewrite nextinstr_inv; auto with ppcgen. 
+  destruct b. apply Pregmap.gss.
+  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
+  intros. unfold rs2. rewrite nextinstr_inv; auto. 
+  transitivity (rs1 r'). destruct b; auto. rewrite Pregmap.gso; auto.
+  unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+Qed.
+
+Remark val_add_add_zero:
+  forall v1 v2, Val.add v1 v2 = Val.add (Val.add v1 v2) (Vint Int.zero).
+Proof.
+  intros. destruct v1; destruct v2; simpl; auto; rewrite Int.add_zero; auto.
+Qed.
+ 
+Lemma transl_load_store_correct:
+  forall (mk_instr_imm: ireg -> int -> instruction)
+         (mk_instr_gen: option (ireg -> shift_addr -> instruction))
+         (is_immed: int -> bool)
+         addr args k ms sp rs m ms' m',
+  (forall (r1: ireg) (rs1: regset) n k,
+    eval_addressing_total sp addr (map ms args) = Val.add rs1#r1 (Vint n) ->
+    agree ms sp rs1 ->
+    exists rs',
+    exec_straight (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\
+    agree ms' sp rs') ->
+  match mk_instr_gen with
+  | None => True
+  | Some mk =>
+      (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k,
+      eval_addressing_total sp addr (map ms args) = Val.add rs1#r1 (eval_shift_addr sa rs1) ->
+      agree ms sp rs1 ->
+      exists rs',
+      exec_straight (mk r1 sa :: k) rs1 m k rs' m' /\
+      agree ms' sp rs')
+  end ->
+  agree ms sp rs ->
+  map mreg_type args = type_of_addressing addr ->
+  exists rs',
+    exec_straight (transl_load_store mk_instr_imm mk_instr_gen is_immed addr args k) rs m
+                        k rs' m'
+  /\ agree ms' sp rs'.
+Proof.
+  intros. destruct addr; simpl in H2; TypeInv; simpl.
+  (* Aindexed *)
+  case (is_immed i).
+  (* Aindexed, small displacement *)
+  apply H; eauto. simpl. rewrite (ireg_val ms sp rs); auto.
+  (* Aindexed, large displacement *)
+  exploit (addimm_correct IR14 (ireg_of t)); eauto with ppcgen. 
+  intros [rs' [A [B C]]].
+  exploit (H IR14 rs' Int.zero); eauto.
+  simpl. rewrite (ireg_val ms sp rs); auto. rewrite B.
+  rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity.
+  apply agree_exten_2 with rs; auto. 
+  intros [rs'' [D E]].
+  exists rs''; split.
+  eapply exec_straight_trans. eexact A. eexact D. auto.
+  (* Aindexed2 *)
+  destruct mk_instr_gen as [mk | ]. 
+  (* binary form available *)
+  apply H0; auto. simpl. repeat rewrite (ireg_val ms sp rs); auto. 
+  (* binary form not available *)
+  set (rs' := nextinstr (rs#IR14 <- (Val.add (ms t) (ms t0)))).
+  exploit (H IR14 rs' Int.zero); eauto.
+  simpl. repeat rewrite (ireg_val ms sp rs); auto.
+  unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  repeat rewrite (ireg_val ms sp rs); auto. apply val_add_add_zero. 
+  unfold rs'; auto with ppcgen.
+  intros [rs'' [A B]].
+  exists rs''; split.
+  eapply exec_straight_step with (rs2 := rs'); eauto.
+  simpl. repeat rewrite <- (ireg_val ms sp rs); auto.
+  auto.
+  (* Aindexed2shift *)
+  destruct mk_instr_gen as [mk | ]. 
+  (* binary form available *)
+  apply H0; auto. simpl. repeat rewrite (ireg_val ms sp rs); auto.
+  rewrite transl_shift_addr_correct. auto.
+  (* binary form not available *)
+  set (rs' := nextinstr (rs#IR14 <- (Val.add (ms t) (eval_shift_total s (ms t0))))).
+  exploit (H IR14 rs' Int.zero); eauto.
+  simpl. repeat rewrite (ireg_val ms sp rs); auto.
+  unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
+  repeat rewrite (ireg_val ms sp rs); auto. apply val_add_add_zero. 
+  unfold rs'; auto with ppcgen.
+  intros [rs'' [A B]].
+  exists rs''; split.
+  eapply exec_straight_step with (rs2 := rs'); eauto.
+  simpl. rewrite transl_shift_correct. 
+  repeat rewrite <- (ireg_val ms sp rs); auto.
+  auto.
+  (* Ainstack *)
+  destruct (is_immed i).
+  (* Ainstack, short displacement *)
+  apply H. simpl.  rewrite (sp_val ms sp rs); auto. auto. 
+  (* Ainstack, large displacement *)
+  exploit (addimm_correct IR14 IR13); eauto with ppcgen. 
+  intros [rs' [A [B C]]].
+  exploit (H IR14 rs' Int.zero); eauto.
+  simpl. rewrite (sp_val ms sp rs); auto. rewrite B.
+  rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity.
+  apply agree_exten_2 with rs; auto. 
+  intros [rs'' [D E]].
+  exists rs''; split.
+  eapply exec_straight_trans. eexact A. eexact D. auto.
+Qed.
+
+Lemma transl_load_int_correct:
+  forall (mk_instr: ireg -> ireg -> shift_addr -> instruction)
+         (is_immed: int -> bool)
+         (rd: mreg) addr args k ms sp rs m chunk a v,
+  (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset),
+    exec_instr ge c (mk_instr r1 r2 sa) rs1 m =
+    exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) ->
+  agree ms sp rs ->
+  map mreg_type args = type_of_addressing addr ->
+  mreg_type rd = Tint ->
+  eval_addressing ge sp addr (map ms args) = Some a ->
+  Mem.loadv chunk m a = Some v ->
+  exists rs',
+    exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m
+                        k rs' m
+  /\ agree (Regmap.set rd v ms) sp rs'.
+Proof.
+  intros. unfold transl_load_store_int.
+  exploit eval_addressing_weaken. eauto. intros. 
+  apply transl_load_store_correct with ms; auto.
+  intros. exists (nextinstr (rs1#(ireg_of rd) <- v)); split.
+  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. 
+  unfold exec_load. rewrite H4. auto. auto.
+  auto with ppcgen.
+  intros. exists (nextinstr (rs1#(ireg_of rd) <- v)); split.
+  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. 
+  unfold exec_load. rewrite H4. auto. auto.
+  auto with ppcgen.
+Qed.
+
+Lemma transl_load_float_correct:
+  forall (mk_instr: freg -> ireg -> int -> instruction)
+         (is_immed: int -> bool)
+         (rd: mreg) addr args k ms sp rs m chunk a v,
+  (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset),
+    exec_instr ge c (mk_instr r1 r2 n) rs1 m =
+    exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) ->
+  agree ms sp rs ->
+  map mreg_type args = type_of_addressing addr ->
+  mreg_type rd = Tfloat ->
+  eval_addressing ge sp addr (map ms args) = Some a ->
+  Mem.loadv chunk m a = Some v ->
+  exists rs',
+    exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m
+                        k rs' m
+  /\ agree (Regmap.set rd v ms) sp rs'.
+Proof.
+  intros. unfold transl_load_store_float.
+  exploit eval_addressing_weaken. eauto. intros. 
+  apply transl_load_store_correct with ms; auto.
+  intros. exists (nextinstr (rs1#(freg_of rd) <- v)); split.
+  apply exec_straight_one. rewrite H. rewrite <- H6. rewrite H5. 
+  unfold exec_load. rewrite H4. auto. auto.
+  auto with ppcgen.
+Qed.
+
+Lemma transl_store_int_correct:
+  forall (mk_instr: ireg -> ireg -> shift_addr -> instruction)
+         (is_immed: int -> bool)
+         (rd: mreg) addr args k ms sp rs m chunk a m',
+  (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset),
+    exec_instr ge c (mk_instr r1 r2 sa) rs1 m =
+    exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) ->
+  agree ms sp rs ->
+  map mreg_type args = type_of_addressing addr ->
+  mreg_type rd = Tint ->
+  eval_addressing ge sp addr (map ms args) = Some a ->
+  Mem.storev chunk m a (ms rd) = Some m' ->
+  exists rs',
+    exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m
+                        k rs' m'
+  /\ agree ms sp rs'.
+Proof.
+  intros. unfold transl_load_store_int.
+  exploit eval_addressing_weaken. eauto. intros. 
+  apply transl_load_store_correct with ms; auto.
+  intros. exists (nextinstr rs1); split.
+  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5.
+  unfold exec_store. rewrite <- (ireg_val ms sp rs1); auto.
+  rewrite H4. auto. auto.
+  auto with ppcgen.
+  intros. exists (nextinstr rs1); split.
+  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5.
+  unfold exec_store. rewrite <- (ireg_val ms sp rs1); auto.
+  rewrite H4. auto. auto.
+  auto with ppcgen.
+Qed.
+
+Lemma transl_store_float_correct:
+  forall (mk_instr: freg -> ireg -> int -> instruction)
+         (is_immed: int -> bool)
+         (rd: mreg) addr args k ms sp rs m chunk a m',
+  (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset),
+    exec_instr ge c (mk_instr r1 r2 n) rs1 m =
+    exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) ->
+  agree ms sp rs ->
+  map mreg_type args = type_of_addressing addr ->
+  mreg_type rd = Tfloat ->
+  eval_addressing ge sp addr (map ms args) = Some a ->
+  Mem.storev chunk m a (ms rd) = Some m' ->
+  exists rs',
+    exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m
+                        k rs' m'
+  /\ agree ms sp rs'.
+Proof.
+  intros. unfold transl_load_store_float.
+  exploit eval_addressing_weaken. eauto. intros. 
+  apply transl_load_store_correct with ms; auto.
+  intros. exists (nextinstr rs1); split.
+  apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5.
+  unfold exec_store. rewrite <- (freg_val ms sp rs1); auto.
+  rewrite H4. auto. auto.
+  auto with ppcgen.
+Qed.
+
+(** Translation of allocations *)
+
+Lemma transl_alloc_correct:
+  forall ms sp rs sz m m' blk k,
+  agree ms sp rs ->
+  ms Conventions.loc_alloc_argument = Vint sz ->
+  Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
+  let ms' := Regmap.set Conventions.loc_alloc_result (Vptr blk Int.zero) ms in
+  exists rs',
+    exec_straight (Pallocblock :: k) rs m k rs' m'
+  /\ agree ms' sp rs'.
+Proof.
+  intros. 
+  pose (rs' := nextinstr (rs#IR0 <- (Vptr blk Int.zero) #IR14 <- (Val.add rs#PC Vone))).
+  exists rs'; split.
+  apply exec_straight_one. unfold exec_instr. 
+  generalize (preg_val _ _ _ Conventions.loc_alloc_argument H).
+  unfold preg_of; intro. simpl in H2. rewrite <- H2. rewrite H0.
+  rewrite H1. reflexivity.
+  reflexivity. 
+  unfold ms', rs'. apply agree_nextinstr. apply agree_set_other. 
+  change (IR IR0) with (preg_of Conventions.loc_alloc_result).
+  apply agree_set_mreg. auto.
+  simpl. tauto.
+Qed.
+
+End STRAIGHTLINE.
+