Back from Oregon commit.

powerpc/*: better compilation of some comparisons; revised asmgenproof1.
common/*: added Mem.storebytes; used to give semantics to memcpy builtin.



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

13 files changed, 1533 insertions, 598 deletions

diff --git a/common/Events.v b/common/Events.v
index ac6c1a0..2e57922 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -901,16 +901,122 @@ Qed.
 
 (** ** Semantics of [memcpy] operations. *)
 
-(** To be done once [storebytes] is added to the [Memtype] interface. *)
-
-Definition extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop :=
-  fun vargs m1 t vres m2 => False.
+Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop :=
+  | extcall_memcpy_sem_intro: forall bdst odst bsrc osrc m bytes m',
+      al = 1 \/ al = 2 \/ al = 4 -> sz > 0 ->
+      (al | sz) -> (al | Int.unsigned osrc) -> (al | Int.unsigned odst) ->
+      bsrc <> bdst \/ Int.unsigned osrc = Int.unsigned odst
+                   \/ Int.unsigned osrc + sz <= Int.unsigned odst
+                   \/ Int.unsigned odst + sz <= Int.unsigned osrc ->
+      Mem.loadbytes m bsrc (Int.unsigned osrc) sz = Some bytes ->
+      Mem.storebytes m bdst (Int.unsigned odst) bytes = Some m' ->
+      extcall_memcpy_sem sz al ge (Vptr bdst odst :: Vptr bsrc osrc :: nil) m E0 Vundef m'.
 
 Lemma extcall_memcpy_ok:
   forall sz al,
   extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None).
 Proof.
-  intros. unfold extcall_memcpy_sem; constructor; contradiction.
+  intros. constructor.
+(* return type *)
+  intros. inv H. constructor. 
+(* arity *)
+  intros. inv H. auto.
+(* change of globalenv *)
+  intros. inv H1. econstructor; eauto.
+(* valid blocks *)
+  intros. inv H. eauto with mem. 
+(* bounds *)
+  intros. inv H. eapply Mem.bounds_storebytes; eauto. 
+(* extensions *)
+  intros. inv H. 
+  inv H1. inv H13. inv H14. inv H10. inv H11.
+  exploit Mem.loadbytes_length; eauto. intros LEN.
+(*
+  destruct (zle sz 0).
+  (* empty copy *)
+  rewrite nat_of_Z_neg in LEN; auto. 
+  assert (bytes = nil). destruct bytes; simpl in LEN; congruence.
+  subst. rewrite Mem.storebytes_empty in H8. inv H8.
+  exists Vundef; exists m1'.
+  split. econstructor; eauto. rewrite Mem.loadbytes_empty; eauto. 
+  apply Mem.storebytes_empty. 
+  split. constructor. split. auto. red; auto.
+  (* nonempty copy *)
+*)
+  exploit Mem.loadbytes_extends; eauto. intros [bytes2 [A B]].
+  exploit Mem.storebytes_within_extends; eauto. intros [m2' [C D]].
+  exists Vundef; exists m2'.
+  split. econstructor; eauto.
+  split. constructor.
+  split. auto.
+  red; split; intros.
+  eauto with mem.  
+  exploit Mem.loadbytes_length. eexact H8. intros.
+  rewrite <- H1. eapply Mem.load_storebytes_other; eauto. 
+  destruct (eq_block b bdst); auto. subst b; right.
+  exploit Mem.range_perm_in_bounds. eapply Mem.storebytes_range_perm. eexact H9.
+  rewrite H10. rewrite nat_of_Z_eq. omega. omega.
+  intros [P Q].
+  exploit list_forall2_length; eauto. intros R. rewrite R in Q.
+  apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk)
+                              (Int.unsigned odst, Int.unsigned odst + Z_of_nat (length bytes2))); simpl.
+  red; intros. generalize (H x H11). unfold loc_out_of_bounds, Intv.In; simpl. omega.
+  generalize (size_chunk_pos chunk); omega.
+  rewrite <- R; rewrite H10. rewrite nat_of_Z_eq. omega. omega.
+(* injections *)
+  intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12.
+  exploit Mem.loadbytes_length; eauto. intros LEN.
+(*
+  destruct (zle sz 0).
+  (* empty copy *)
+  rewrite nat_of_Z_neg in LEN; auto. 
+  assert (bytes = nil). destruct bytes; simpl in LEN; congruence.
+  subst. rewrite Mem.storebytes_empty in H9. inv H9.
+  exists f; exists Vundef; exists m1'.
+  split. econstructor; eauto. 
+*)
+  assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Nonempty).
+    eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
+  assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Nonempty).
+    replace sz with (Z_of_nat (length bytes)).
+    eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
+    rewrite LEN. apply nat_of_Z_eq. omega.
+  assert (PSRC: Mem.perm m1 bsrc (Int.unsigned osrc) Nonempty).
+    apply RPSRC. omega.
+  assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Nonempty).
+    apply RPDST. omega.
+  exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
+  exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
+  exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
+  exploit Mem.storebytes_mapped_inject; eauto. intros [m2' [C D]].
+  exists f; exists Vundef; exists m2'.
+  split. econstructor; try rewrite EQ1; try rewrite EQ2; eauto. 
+  eapply Mem.aligned_area_inject with (m := m1); eauto.
+  eapply Mem.aligned_area_inject with (m := m1); eauto.
+  eapply Mem.disjoint_or_equal_inject with (m := m1); eauto.
+  split. constructor.
+  split. auto.
+  split. red; split; intros. eauto with mem. 
+  rewrite <- H2. eapply Mem.load_storebytes_other; eauto. 
+  destruct (eq_block b bdst); auto. subst b. 
+  assert (loc_unmapped f bdst ofs). apply H0. generalize (size_chunk_pos chunk); omega. 
+  red in H12. congruence.
+  split. red; split; intros. eauto with mem.
+  rewrite <- H2. eapply Mem.load_storebytes_other; eauto. 
+  destruct (eq_block b b0); auto. subst b0; right.
+  rewrite <- (list_forall2_length B). rewrite LEN. rewrite nat_of_Z_eq; try omega.
+  apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk)
+                              (Int.unsigned odst + delta0, Int.unsigned odst + delta0 + sz)); simpl.
+  red; intros. generalize (H0 x H12). unfold loc_out_of_reach, Intv.In; simpl. 
+  intros. exploit H14; eauto. 
+  exploit Mem.range_perm_in_bounds. eexact RPDST. omega. 
+  omega.
+  generalize (size_chunk_pos chunk); omega.
+  omega.
+  split. apply inject_incr_refl.
+  red; intros; congruence.
+(* determinism *)
+  intros. inv H; inv H0. split. auto. split. auto. congruence.
 Qed.
 
 (** ** Semantics of system calls. *)
diff --git a/common/Memdata.v b/common/Memdata.v
index c0e1f50..16adb23 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -69,10 +69,10 @@ Qed.
   multiple of the natural alignment for the chunk being addressed.
   This natural alignment is defined by the following 
   [align_chunk] function.  Some target architectures
-  (e.g. the PowerPC) have no alignment constraints, which we could
+  (e.g. PowerPC and x86) have no alignment constraints, which we could
   reflect by taking [align_chunk chunk = 1].  However, other architectures
   have stronger alignment requirements.  The following definition is
-  appropriate for PowerPC and ARM. *)
+  appropriate for PowerPC, ARM and x86. *)
 
 Definition align_chunk (chunk: memory_chunk) : Z := 
   match chunk with
@@ -1053,9 +1053,12 @@ Proof.
   constructor.
 Qed.
 
-Lemma memval_inject_id:
-  forall mv, memval_inject inject_id mv mv.
+Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id.
+
+Lemma memval_lessdef_refl:
+  forall mv, memval_lessdef mv mv.
 Proof.
-  destruct mv; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. 
+  red. destruct mv; econstructor.
+  unfold inject_id; reflexivity. rewrite Int.add_zero; auto. 
 Qed.
  
diff --git a/common/Memory.v b/common/Memory.v
index d7d1d7b..b456191 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -562,25 +562,29 @@ Proof.
   intros. apply getN_exten. intros. apply setN_outside. omega. 
 Qed.
 
+Lemma setN_noread_undef:
+  forall m b ofs bytes (RP: range_perm m b ofs (ofs + Z_of_nat (length bytes)) Writable),
+  forall b' ofs',
+  perm m b' ofs' Readable \/
+  update b (setN bytes ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef.
+Proof.
+  intros. unfold update. destruct (zeq b' b). subst b'.
+  assert (ofs <= ofs' < ofs + Z_of_nat (length bytes)
+         \/ ofs' < ofs
+         \/ ofs' >= ofs + Z_of_nat (length bytes)) by omega.
+  destruct H. left. apply perm_implies with Writable; auto with mem. 
+  rewrite setN_outside; auto. apply noread_undef; auto. 
+  apply noread_undef; auto.
+Qed.
+
 Lemma store_noread_undef:
   forall m ch b ofs (VA: valid_access m ch b ofs Writable) v,
-       forall b' ofs', 
-       perm m b' ofs' Readable \/ 
-        update b (setN (encode_val ch v) ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef.
+  forall b' ofs', 
+  perm m b' ofs' Readable \/ 
+  update b (setN (encode_val ch v) ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef.
 Proof.
-  intros.
-  destruct VA as [? _].
-  unfold update.
-  destruct (zeq b' b).
-  subst b'.
-  assert (ofs <= ofs' < ofs + size_chunk ch \/ (ofs' < ofs \/ ofs' >= ofs + size_chunk ch)) by omega.
-  destruct H0.
-  exploit (H ofs'); auto; intro.
-  eauto with mem.
-  rewrite setN_outside.
-  destruct (noread_undef m b ofs'); auto.
-  rewrite encode_val_length. rewrite <- size_chunk_conv; auto.
-  destruct (noread_undef m b' ofs'); auto.
+  intros. destruct VA. apply setN_noread_undef. 
+  rewrite encode_val_length. rewrite <- size_chunk_conv. auto.
 Qed.
 
 (** [store chunk m b ofs v] perform a write in memory state [m].
@@ -612,6 +616,26 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   | _ => None
   end.
 
+(** [storebytes m b ofs bytes] stores the given list of bytes [bytes]
+  starting at location [(b, ofs)].  Returns updated memory state
+  or [None] if the accessed locations are not writable. *)
+
+Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem :=
+  match range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Writable with
+  | left RP =>
+      Some (mkmem
+             (update b (setN bytes ofs (m.(mem_contents) b)) m.(mem_contents))
+             m.(mem_access)
+             m.(bounds)
+             m.(nextblock)
+             m.(nextblock_pos)
+             m.(nextblock_noaccess)
+             m.(bounds_noaccess)
+             (setN_noread_undef m b ofs bytes RP))
+  | right _ =>
+      None
+  end.
+
 (** [drop_perm m b lo hi p] sets the permissions of the byte range
     [(b, lo) ... (b, hi - 1)] to [p].  These bytes must have permissions
     at least [p] in the initial memory state [m].
@@ -754,6 +778,25 @@ Proof.
   rewrite pred_dec_false; auto.
 Qed.
 
+(** ** Properties related to [loadbytes] *)
+
+Theorem range_perm_loadbytes:
+  forall m b ofs len,
+  range_perm m b ofs (ofs + len) Readable ->
+  exists bytes, loadbytes m b ofs len = Some bytes.
+Proof.
+  intros. econstructor. unfold loadbytes. rewrite pred_dec_true; eauto. 
+Qed.
+
+Theorem loadbytes_range_perm:
+  forall m b ofs len bytes,
+  loadbytes m b ofs len = Some bytes ->
+  range_perm m b ofs (ofs + len) Readable.
+Proof.
+  intros until bytes. unfold loadbytes.
+  destruct (range_perm_dec m b ofs (ofs + len) Readable). auto. congruence.
+Qed.
+
 Theorem loadbytes_load:
   forall chunk m b ofs bytes,
   loadbytes m b ofs (size_chunk chunk) = Some bytes ->
@@ -796,6 +839,14 @@ Proof.
   inv H. apply getN_length.
 Qed.
 
+Theorem loadbytes_empty:
+  forall m b ofs n,
+  n <= 0 -> loadbytes m b ofs n = Some nil.
+Proof.
+  intros. unfold loadbytes. rewrite pred_dec_true. rewrite nat_of_Z_neg; auto.
+  red; intros. omegaContradiction.
+Qed.
+  
 Lemma getN_concat:
   forall c n1 n2 p,
   getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z_of_nat n1) c.
@@ -1350,6 +1401,269 @@ Theorem store_float32_truncate:
   store Mfloat32 m b ofs (Vfloat n).
 Proof. intros. apply store_similar_chunks. simpl. decEq. apply encode_float32_cast. Qed.
 
+(** ** Properties related to [storebytes]. *)
+
+Theorem range_perm_storebytes:
+  forall m1 b ofs bytes,
+  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable ->
+  { m2 : mem | storebytes m1 b ofs bytes = Some m2 }.
+Proof.
+  intros. 
+  exists (mkmem
+             (update b (setN bytes ofs (m1.(mem_contents) b)) m1.(mem_contents))
+             m1.(mem_access)
+             m1.(bounds)
+             m1.(nextblock)
+             m1.(nextblock_pos)
+             m1.(nextblock_noaccess)
+             m1.(bounds_noaccess)
+             (setN_noread_undef m1 b ofs bytes H)).
+  unfold storebytes. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable).
+  decEq. decEq. apply proof_irr. 
+  contradiction.
+Qed.
+
+Theorem storebytes_store:
+  forall m1 b ofs chunk v m2,
+  storebytes m1 b ofs (encode_val chunk v) = Some m2 ->
+  (align_chunk chunk | ofs) ->
+  store chunk m1 b ofs v = Some m2.
+Proof.
+  unfold storebytes, store. intros. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Writable); inv H.
+  destruct (valid_access_dec m1 chunk b ofs Writable).
+  decEq. decEq. apply proof_irr. 
+  elim n. constructor; auto. 
+  rewrite encode_val_length in r. rewrite size_chunk_conv. auto.
+Qed.
+
+Theorem store_storebytes:
+  forall m1 b ofs chunk v m2,
+  store chunk m1 b ofs v = Some m2 ->
+  storebytes m1 b ofs (encode_val chunk v) = Some m2.
+Proof.
+  unfold storebytes, store. intros. 
+  destruct (valid_access_dec m1 chunk b ofs Writable); inv H.
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Writable).
+  decEq. decEq. apply proof_irr. 
+  destruct v0.  elim n. 
+  rewrite encode_val_length. rewrite <- size_chunk_conv. auto.
+Qed.
+
+Theorem storebytes_empty:
+  forall m b ofs, storebytes m b ofs nil = Some m.
+Proof.
+  intros. unfold storebytes. simpl. 
+  destruct (range_perm_dec m b ofs (ofs + 0) Writable).
+  decEq. destruct m; simpl; apply mkmem_ext; auto. 
+  apply extensionality. unfold update; intros. destruct (zeq x b); congruence.
+  elim n. red; intros; omegaContradiction.
+Qed.
+  
+Section STOREBYTES.
+Variable m1: mem.
+Variable b: block.
+Variable ofs: Z.
+Variable bytes: list memval.
+Variable m2: mem.
+Hypothesis STORE: storebytes m1 b ofs bytes = Some m2.
+
+Lemma storebytes_access: mem_access m2 = mem_access m1.
+Proof.
+  unfold storebytes in STORE. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  inv STORE.
+  auto.
+Qed.
+
+Lemma storebytes_mem_contents:
+   mem_contents m2 = update b (setN bytes ofs (m1.(mem_contents) b)) m1.(mem_contents).
+Proof.
+  unfold storebytes in STORE. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  inv STORE.
+  auto.
+Qed.
+
+Theorem perm_storebytes_1:
+  forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p.
+Proof.
+  intros. unfold perm in *. rewrite storebytes_access; auto.
+Qed.
+
+Theorem perm_storebytes_2:
+  forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p.
+Proof.
+  intros. unfold perm in *. rewrite storebytes_access in H; auto.
+Qed.
+
+Hint Local Resolve perm_storebytes_1 perm_storebytes_2: mem.
+
+Theorem storebytes_valid_access_1:
+  forall chunk' b' ofs' p,
+  valid_access m1 chunk' b' ofs' p -> valid_access m2 chunk' b' ofs' p.
+Proof.
+  intros. inv H. constructor; try red; auto with mem.
+Qed.
+
+Theorem storebytes_valid_access_2:
+  forall chunk' b' ofs' p,
+  valid_access m2 chunk' b' ofs' p -> valid_access m1 chunk' b' ofs' p.
+Proof.
+  intros. inv H. constructor; try red; auto with mem.
+Qed.
+
+Hint Local Resolve storebytes_valid_access_1 storebytes_valid_access_2: mem.
+
+Theorem nextblock_storebytes:
+  nextblock m2 = nextblock m1.
+Proof.
+  intros.
+  unfold storebytes in STORE. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  inv STORE.
+  auto.
+Qed.
+
+Theorem storebytes_valid_block_1:
+  forall b', valid_block m1 b' -> valid_block m2 b'.
+Proof.
+  unfold valid_block; intros. rewrite nextblock_storebytes; auto.
+Qed.
+
+Theorem storebytes_valid_block_2:
+  forall b', valid_block m2 b' -> valid_block m1 b'.
+Proof.
+  unfold valid_block; intros. rewrite nextblock_storebytes in H; auto.
+Qed.
+
+Hint Local Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem.
+
+Theorem storebytes_range_perm:
+  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable.
+Proof.
+  intros. 
+  unfold storebytes in STORE. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  inv STORE.
+  auto.
+Qed.
+
+Theorem bounds_storebytes:
+  forall b', bounds m2 b' = bounds m1 b'.
+Proof.
+  intros.
+  unfold storebytes in STORE. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  inv STORE.
+  auto.
+Qed.
+
+Theorem loadbytes_storebytes_same:
+  loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.
+Proof.
+  intros. unfold storebytes in STORE. unfold loadbytes. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  try discriminate.
+  rewrite pred_dec_true. 
+  decEq. inv STORE; simpl. rewrite update_s. rewrite nat_of_Z_of_nat. 
+  apply getN_setN_same. 
+  red; eauto with mem. 
+Qed.
+
+Theorem loadbytes_storebytes_other:
+  forall b' ofs' len,
+  len >= 0 ->
+  b' <> b
+  \/ ofs' + len <= ofs
+  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
+  loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len.
+Proof.
+  intros. unfold loadbytes.
+  destruct (range_perm_dec m1 b' ofs' (ofs' + len) Readable).
+  rewrite pred_dec_true. 
+  rewrite storebytes_mem_contents. decEq. 
+  unfold update. destruct (zeq b' b). subst b'. 
+  apply getN_setN_outside. rewrite nat_of_Z_eq; auto. intuition congruence.
+  auto.
+  red; auto with mem.
+  apply pred_dec_false. 
+  red; intros; elim n. red; auto with mem.
+Qed.
+
+Theorem load_storebytes_other:
+  forall chunk b' ofs',
+  b' <> b
+  \/ ofs' + size_chunk chunk <= ofs
+  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
+  load chunk m2 b' ofs' = load chunk m1 b' ofs'.
+Proof.
+  intros. unfold load.
+  destruct (valid_access_dec m1 chunk b' ofs' Readable).
+  rewrite pred_dec_true. 
+  rewrite storebytes_mem_contents. decEq. 
+  unfold update. destruct (zeq b' b). subst b'. 
+  rewrite getN_setN_outside. auto. rewrite <- size_chunk_conv. intuition congruence.
+  auto.
+  destruct v; split; auto. red; auto with mem.
+  apply pred_dec_false. 
+  red; intros; elim n. destruct H0. split; auto. red; auto with mem.
+Qed.
+
+End STOREBYTES.
+
+Lemma setN_concat:
+  forall bytes1 bytes2 ofs c,
+  setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z_of_nat (length bytes1)) (setN bytes1 ofs c).
+Proof.
+  induction bytes1; intros.
+  simpl. decEq. omega.
+  simpl length. rewrite inj_S. simpl. rewrite IHbytes1. decEq. omega.
+Qed.
+
+Theorem storebytes_concat:
+  forall m b ofs bytes1 m1 bytes2 m2,
+  storebytes m b ofs bytes1 = Some m1 ->
+  storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 ->
+  storebytes m b ofs (bytes1 ++ bytes2) = Some m2.
+Proof.
+  intros. generalize H; intro ST1. generalize H0; intro ST2.
+  unfold storebytes; unfold storebytes in ST1; unfold storebytes in ST2.
+  destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Writable); try congruence.
+  destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Writable); try congruence.
+  destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Writable).
+  inv ST1; inv ST2; simpl. decEq. apply mkmem_ext; auto.
+  apply extensionality; intros. unfold update. destruct (zeq x b); auto.
+  subst x. rewrite zeq_true. apply setN_concat.
+  elim n.   
+  rewrite app_length. rewrite inj_plus. red; intros.
+  destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))).
+  apply r. omega. 
+  eapply perm_storebytes_2; eauto. apply r0. omega.
+Qed.
+
+Theorem storebytes_split:
+  forall m b ofs bytes1 bytes2 m2,
+  storebytes m b ofs (bytes1 ++ bytes2) = Some m2 ->
+  exists m1,
+     storebytes m b ofs bytes1 = Some m1
+  /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2.
+Proof.
+  intros. 
+  destruct (range_perm_storebytes m b ofs bytes1) as [m1 ST1].
+  red; intros. exploit storebytes_range_perm; eauto. rewrite app_length. 
+  rewrite inj_plus. omega.
+  destruct (range_perm_storebytes m1 b (ofs + Z_of_nat (length bytes1)) bytes2) as [m2' ST2].
+  red; intros. eapply perm_storebytes_1; eauto. exploit storebytes_range_perm. 
+  eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite inj_plus. omega.
+  auto.
+  assert (Some m2 = Some m2').
+  rewrite <- H. eapply storebytes_concat; eauto.
+  inv H0.
+  exists m1; split; auto. 
+Qed.
+
 (** ** Properties related to [alloc]. *)
 
 Section ALLOC.
@@ -1997,6 +2311,18 @@ Proof.
   apply A. simpl; omega. 
 Qed.
 
+Lemma range_perm_inj:
+  forall f m1 m2 b1 lo hi p b2 delta,
+  mem_inj f m1 m2 ->
+  range_perm m1 b1 lo hi p ->
+  f b1 = Some(b2, delta) ->
+  range_perm m2 b2 (lo + delta) (hi + delta) p.
+Proof.
+  intros; red; intros.
+  replace ofs with ((ofs - delta) + delta) by omega.
+  eapply perm_inj; eauto. apply H0. omega.
+Qed.
+
 (** Preservation of loads. *)
 
 Lemma getN_inj:
@@ -2036,6 +2362,25 @@ Proof.
   rewrite <- size_chunk_conv. exploit load_valid_access; eauto. intros [A B]. auto.
 Qed.
 
+Lemma loadbytes_inj:
+  forall f m1 m2 len b1 ofs b2 delta bytes1,
+  mem_inj f m1 m2 ->
+  loadbytes m1 b1 ofs len = Some bytes1 ->
+  f b1 = Some (b2, delta) ->
+  exists bytes2, loadbytes m2 b2 (ofs + delta) len = Some bytes2
+              /\ list_forall2 (memval_inject f) bytes1 bytes2.
+Proof.
+  intros. unfold loadbytes in *. 
+  destruct (range_perm_dec m1 b1 ofs (ofs + len) Readable); inv H0.
+  exists (getN (nat_of_Z len) (ofs + delta) (m2.(mem_contents) b2)).
+  split. apply pred_dec_true.  
+  replace (ofs + delta + len) with ((ofs + len) + delta) by omega.
+  eapply range_perm_inj; eauto with mem. 
+  apply getN_inj; auto. 
+  destruct (zle 0 len). rewrite nat_of_Z_eq; auto. omega. 
+  rewrite nat_of_Z_neg. simpl. red; intros; omegaContradiction. omega.
+Qed.
+
 (** Preservation of stores. *)
 
 Lemma setN_inj:
@@ -2172,6 +2517,99 @@ Proof.
   eauto with mem.
 Qed.
 
+Lemma storebytes_mapped_inj:
+  forall f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
+  mem_inj f m1 m2 ->
+  storebytes m1 b1 ofs bytes1 = Some n1 ->
+  meminj_no_overlap f m1 ->
+  f b1 = Some (b2, delta) ->
+  list_forall2 (memval_inject f) bytes1 bytes2 ->
+  exists n2,
+    storebytes m2 b2 (ofs + delta) bytes2 = Some n2
+    /\ mem_inj f n1 n2.
+Proof.
+  intros. inversion H. 
+  assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z_of_nat (length bytes2)) Writable).
+    replace (ofs + delta + Z_of_nat (length bytes2))
+       with ((ofs + Z_of_nat (length bytes1)) + delta).
+    eapply range_perm_inj; eauto with mem. 
+    eapply storebytes_range_perm; eauto.
+    rewrite (list_forall2_length H3). omega.
+  destruct (range_perm_storebytes _ _ _ _ H4) as [n2 STORE]. 
+  exists n2; split. eauto.
+  constructor.
+(* access *)
+  intros.
+  eapply storebytes_valid_access_1; [apply STORE |].
+  eapply mi_access0; eauto.
+  eapply storebytes_valid_access_2; [apply H0 |]. auto.
+(* mem_contents *)
+  intros.
+  assert (perm m1 b0 ofs0 Nonempty). eapply perm_storebytes_2; eauto. 
+  rewrite (storebytes_mem_contents _ _ _ _ _ H0).
+  rewrite (storebytes_mem_contents _ _ _ _ _ STORE).
+  unfold update. 
+  destruct (zeq b0 b1). subst b0.
+  (* block = b1, block = b2 *)
+  assert (b3 = b2) by congruence. subst b3.
+  assert (delta0 = delta) by congruence. subst delta0.
+  rewrite zeq_true.
+  apply setN_inj with (access := fun ofs => perm m1 b1 ofs Nonempty); auto.
+  destruct (zeq b3 b2). subst b3.
+  (* block <> b1, block = b2 *)
+  rewrite setN_other. auto.
+  intros.
+  assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta).
+    eapply meminj_no_overlap_perm; eauto. 
+    exploit storebytes_range_perm. eexact H0. 
+    instantiate (1 := r - delta). 
+    rewrite (list_forall2_length H3). omega.
+    eauto with mem.
+  destruct H9. congruence. omega.
+  (* block <> b1, block <> b2 *)
+  eauto.
+Qed.
+
+Lemma storebytes_unmapped_inj:
+  forall f m1 b1 ofs bytes1 n1 m2,
+  mem_inj f m1 m2 ->
+  storebytes m1 b1 ofs bytes1 = Some n1 ->
+  f b1 = None ->
+  mem_inj f n1 m2.
+Proof.
+  intros. inversion H.
+  constructor.
+(* access *)
+  intros. eapply mi_access0; eauto. eapply storebytes_valid_access_2; eauto. 
+(* mem_contents *)
+  intros. 
+  rewrite (storebytes_mem_contents _ _ _ _ _ H0).
+  rewrite update_o. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto.
+  congruence.
+Qed.
+
+Lemma storebytes_outside_inj:
+  forall f m1 m2 b ofs bytes2 m2',
+  mem_inj f m1 m2 ->
+  (forall b' delta ofs',
+    f b' = Some(b, delta) ->
+    perm m1 b' ofs' Nonempty ->
+    ofs' + delta < ofs \/ ofs' + delta >= ofs + Z_of_nat (length bytes2)) ->
+  storebytes m2 b ofs bytes2 = Some m2' ->
+  mem_inj f m1 m2'.
+Proof.
+  intros. inversion H. constructor.
+(* access *)
+  intros. eapply storebytes_valid_access_1; eauto with mem.
+(* mem_contents *)
+  intros. 
+  rewrite (storebytes_mem_contents _ _ _ _ _ H1).
+  unfold update. destruct (zeq b2 b). subst b2.
+  rewrite setN_outside. auto. 
+  eapply H0; eauto. 
+  eauto with mem.
+Qed.
+
 (** Preservation of allocations *)
 
 Lemma alloc_right_inj:
@@ -2414,8 +2852,7 @@ Proof.
   intros. constructor. auto. constructor.
   intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto.
   intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. 
-  apply memval_inject_id.
-(*  intros. omega. *)
+  apply memval_lessdef_refl.
 Qed.
 
 Theorem load_extends:
@@ -2442,6 +2879,17 @@ Proof.
   congruence.
 Qed.
 
+Theorem loadbytes_extends:
+  forall m1 m2 b ofs len bytes1,
+  extends m1 m2 ->
+  loadbytes m1 b ofs len = Some bytes1 ->
+  exists bytes2, loadbytes m2 b ofs len = Some bytes2
+              /\ list_forall2 memval_lessdef bytes1 bytes2.
+Proof.
+  intros. inv H.
+  replace ofs with (ofs + 0) by omega. eapply loadbytes_inj; eauto. 
+Qed.
+
 Theorem store_within_extends:
   forall chunk m1 m2 b ofs v1 m1' v2,
   extends m1 m2 ->
@@ -2504,6 +2952,52 @@ Proof.
   congruence.
 Qed.
 
+Theorem storebytes_within_extends:
+  forall m1 m2 b ofs bytes1 m1' bytes2,
+  extends m1 m2 ->
+  storebytes m1 b ofs bytes1 = Some m1' ->
+  list_forall2 memval_lessdef bytes1 bytes2 ->
+  exists m2',
+     storebytes m2 b ofs bytes2 = Some m2'
+  /\ extends m1' m2'.
+Proof.
+  intros. inversion H.
+  exploit storebytes_mapped_inj; eauto. 
+    unfold inject_id; red; intros. inv H3; inv H4. auto.
+    unfold inject_id; reflexivity.
+  intros [m2' [A B]].
+  exists m2'; split.
+  replace (ofs + 0) with ofs in A by omega. auto.
+  split; auto.
+  rewrite (nextblock_storebytes _ _ _ _ _ H0).
+  rewrite (nextblock_storebytes _ _ _ _ _ A).
+  auto.
+(*
+  intros.
+  rewrite (bounds_store _ _ _ _ _ _ H0).
+  rewrite (bounds_store _ _ _ _ _ _ A).
+  auto.
+*)
+Qed.
+
+Theorem storebytes_outside_extends:
+  forall m1 m2 b ofs bytes2 m2',
+  extends m1 m2 ->
+  storebytes m2 b ofs bytes2 = Some m2' ->
+  ofs + Z_of_nat (length bytes2) <= low_bound m1 b \/ high_bound m1 b <= ofs ->
+  extends m1 m2'.
+Proof.
+  intros. inversion H. constructor.
+  rewrite (nextblock_storebytes _ _ _ _ _ H0). auto.
+  eapply storebytes_outside_inj; eauto.
+  unfold inject_id; intros. inv H2.
+  exploit perm_in_bounds; eauto. omega.
+(* 
+  intros.
+  rewrite (bounds_store _ _ _ _ _ _ H0). auto.
+*)
+Qed.
+
 Theorem alloc_extends:
   forall m1 m2 lo1 hi1 b m1' lo2 hi2,
   extends m1 m2 ->
@@ -2702,6 +3196,15 @@ Proof.
   intros. inv H0. eapply perm_inj; eauto. 
 Qed.
 
+Theorem range_perm_inject:
+  forall f m1 m2 b1 b2 delta lo hi p,
+  f b1 = Some(b2, delta) ->
+  inject f m1 m2 ->
+  range_perm m1 b1 lo hi p -> range_perm m2 b2 (lo + delta) (hi + delta) p.
+Proof.
+  intros. inv H0. eapply range_perm_inj; eauto.
+Qed.
+
 Theorem valid_access_inject:
   forall f m1 m2 chunk b1 ofs b2 delta p,
   f b1 = Some(b2, delta) ->
@@ -2824,6 +3327,53 @@ Proof.
   apply (H1 (Int.unsigned ofs2)). omega.
 Qed.
 
+Theorem disjoint_or_equal_inject:
+  forall f m m' b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 sz,
+  inject f m m' ->
+  f b1 = Some(b1', delta1) ->
+  f b2 = Some(b2', delta2) ->
+  range_perm m b1 ofs1 (ofs1 + sz) Nonempty ->
+  range_perm m b2 ofs2 (ofs2 + sz) Nonempty ->
+  sz > 0 ->
+  b1 <> b2 \/ ofs1 = ofs2 \/ ofs1 + sz <= ofs2 \/ ofs2 + sz <= ofs1 ->
+  b1' <> b2' \/ ofs1 + delta1 = ofs2 + delta2
+             \/ ofs1 + delta1 + sz <= ofs2 + delta2 
+             \/ ofs2 + delta2 + sz <= ofs1 + delta1.
+Proof.
+  intros. 
+  exploit range_perm_in_bounds. eexact H2. omega. intros [LO1 HI1].
+  exploit range_perm_in_bounds. eexact H3. omega. intros [LO2 HI2].
+  destruct (eq_block b1 b2).
+  assert (b1' = b2') by congruence. assert (delta1 = delta2) by congruence. subst.
+  destruct H5. congruence. right. destruct H5. left; congruence. right. omega.
+  exploit mi_no_overlap; eauto. intros [P | P]. auto. right. omega.
+Qed.
+
+Theorem aligned_area_inject:
+  forall f m m' b ofs al sz b' delta,
+  inject f m m' ->
+  al = 1 \/ al = 2 \/ al = 4 -> sz > 0 ->
+  (al | sz) ->
+  range_perm m b ofs (ofs + sz) Nonempty ->
+  (al | ofs) ->
+  f b = Some(b', delta) ->
+  (al | ofs + delta).
+Proof.
+  intros. 
+  assert (P: al > 0) by omega.
+  assert (Q: Zabs al <= Zabs sz). apply Zdivide_bounds; auto. omega.
+  rewrite Zabs_eq in Q; try omega. rewrite Zabs_eq in Q; try omega.
+  assert (R: exists chunk, al = align_chunk chunk /\ al = size_chunk chunk).
+    destruct H0. subst; exists Mint8unsigned; auto.
+    destruct H0. subst; exists Mint16unsigned; auto.
+    subst; exists Mint32; auto.
+  destruct R as [chunk [A B]].
+  assert (valid_access m chunk b ofs Nonempty).
+    split. red; intros; apply H3. omega. congruence.
+  exploit valid_access_inject; eauto. intros [C D]. 
+  congruence.
+Qed.
+
 (** Preservation of loads *)
 
 Theorem load_inject:
@@ -2851,6 +3401,17 @@ Proof.
   auto. symmetry. eapply address_inject'; eauto with mem.
 Qed.
 
+Theorem loadbytes_inject:
+  forall f m1 m2 b1 ofs len b2 delta bytes1,
+  inject f m1 m2 ->
+  loadbytes m1 b1 ofs len = Some bytes1 ->
+  f b1 = Some (b2, delta) ->
+  exists bytes2, loadbytes m2 b2 (ofs + delta) len = Some bytes2
+              /\ list_forall2 (memval_inject f) bytes1 bytes2.
+Proof.
+  intros. inv H. eapply loadbytes_inj; eauto. 
+Qed.
+
 (** Preservation of stores *)
 
 Theorem store_mapped_inject:
@@ -2951,6 +3512,87 @@ Proof.
   symmetry. eapply address_inject'; eauto with mem.
 Qed.
 
+Theorem storebytes_mapped_inject:
+  forall f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
+  inject f m1 m2 ->
+  storebytes m1 b1 ofs bytes1 = Some n1 ->
+  f b1 = Some (b2, delta) ->
+  list_forall2 (memval_inject f) bytes1 bytes2 ->
+  exists n2,
+    storebytes m2 b2 (ofs + delta) bytes2 = Some n2
+    /\ inject f n1 n2.
+Proof.
+  intros. inversion H.
+  exploit storebytes_mapped_inj; eauto. intros [n2 [STORE MI]].
+  exists n2; split. eauto. constructor.
+(* inj *)
+  auto.
+(* freeblocks *)
+  intros. apply mi_freeblocks0. red; intros; elim H3; eapply storebytes_valid_block_1; eauto.
+(* mappedblocks *)
+  intros. eapply storebytes_valid_block_1; eauto. 
+(* no overlap *)
+  red; intros.
+  repeat rewrite (bounds_storebytes _ _ _ _ _ H0).
+  eauto. 
+(* range offset *)
+  eauto.
+(* range blocks *)
+  intros. rewrite (bounds_storebytes _ _ _ _ _ STORE). eauto.
+Qed.
+
+Theorem storebytes_unmapped_inject:
+  forall f m1 b1 ofs bytes1 n1 m2,
+  inject f m1 m2 ->
+  storebytes m1 b1 ofs bytes1 = Some n1 ->
+  f b1 = None ->
+  inject f n1 m2.
+Proof.
+  intros. inversion H.
+  constructor.
+(* inj *)
+  eapply storebytes_unmapped_inj; eauto.
+(* freeblocks *)
+  intros. apply mi_freeblocks0. red; intros; elim H2; eapply storebytes_valid_block_1; eauto.
+(* mappedblocks *)
+  eauto with mem.
+(* no overlap *)
+  red; intros. 
+  repeat rewrite (bounds_storebytes _ _ _ _ _ H0).
+  eauto. 
+(* range offset *)
+  eauto.
+(* range blocks *)
+  auto.
+Qed.
+
+Theorem storebytes_outside_inject:
+  forall f m1 m2 b ofs bytes2 m2',
+  inject f m1 m2 ->
+  (forall b' delta,
+    f b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= ofs
+    \/ ofs + Z_of_nat (length bytes2) <= low_bound m1 b' + delta) ->
+  storebytes m2 b ofs bytes2 = Some m2' ->
+  inject f m1 m2'.
+Proof.
+  intros. inversion H. constructor.
+(* inj *)
+  eapply storebytes_outside_inj; eauto.
+  intros. exploit perm_in_bounds; eauto. intro. 
+  exploit H0; eauto. omega. 
+(* freeblocks *)
+  auto.
+(* mappedblocks *)
+  intros. eapply storebytes_valid_block_1; eauto. 
+(* no overlap *)
+  auto.
+(* range offset *)
+  auto.
+(* range blocks *)
+  intros. rewrite (bounds_storebytes _ _ _ _ _ H1). eauto.
+Qed.
+
 (* Preservation of allocations *)
 
 Theorem alloc_right_inject:
@@ -3328,7 +3970,7 @@ End Mem.
 
 Notation mem := Mem.mem.
 
-Global Opaque Mem.alloc Mem.free Mem.store Mem.load.
+Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes.
 
 Hint Resolve
   Mem.valid_not_valid_diff
@@ -3340,6 +3982,7 @@ Hint Resolve
   Mem.valid_access_perm
   Mem.valid_access_load
   Mem.load_valid_access
+  Mem.loadbytes_range_perm
   Mem.valid_access_store
   Mem.perm_store_1
   Mem.perm_store_2
@@ -3349,6 +3992,14 @@ Hint Resolve
   Mem.store_valid_access_1
   Mem.store_valid_access_2
   Mem.store_valid_access_3
+  Mem.storebytes_range_perm
+  Mem.perm_storebytes_1
+  Mem.perm_storebytes_2
+  Mem.storebytes_valid_access_1
+  Mem.storebytes_valid_access_2
+  Mem.nextblock_storebytes
+  Mem.storebytes_valid_block_1
+  Mem.storebytes_valid_block_2
   Mem.nextblock_alloc
   Mem.alloc_result
   Mem.valid_block_alloc
diff --git a/common/Memtype.v b/common/Memtype.v
index 0973643..40e03a3 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -126,6 +126,11 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   [None] is returned if the accessed addresses are not readable. *)
 Parameter loadbytes: forall (m: mem) (b: block) (ofs n: Z), option (list memval).
 
+(** [storebytes m b ofs bytes] stores the given list of bytes [bytes]
+  starting at location [(b, ofs)].  Returns updated memory state
+  or [None] if the accessed locations are not writable. *)
+Parameter storebytes: forall (m: mem) (b: block) (ofs: Z) (bytes: list memval), option mem.
+
 (** [free_list] frees all the given (block, lo, hi) triples. *)
 Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem :=
   match l with
@@ -305,6 +310,18 @@ Axiom load_int16_signed_unsigned:
 
 (** ** Properties of [loadbytes]. *)
 
+(** [loadbytes] succeeds if and only if we have read permissions on the accessed
+    memory area. *)
+
+Axiom range_perm_loadbytes:
+  forall m b ofs len,
+  range_perm m b ofs (ofs + len) Readable ->
+  exists bytes, loadbytes m b ofs len = Some bytes.
+Axiom loadbytes_range_perm:
+  forall m b ofs len bytes,
+  loadbytes m b ofs len = Some bytes ->
+  range_perm m b ofs (ofs + len) Readable.
+
 (** If [loadbytes] succeeds, the corresponding [load] succeeds and
   returns a value that is determined by the
   bytes read by [loadbytes]. *)
@@ -329,6 +346,10 @@ Axiom loadbytes_length:
   loadbytes m b ofs n = Some bytes ->
   length bytes = nat_of_Z n.
 
+Axiom loadbytes_empty:
+  forall m b ofs n,
+  n <= 0 -> loadbytes m b ofs n = Some nil.
+
 (** Composing or decomposing [loadbytes] operations at adjacent addresses. *)
 Axiom loadbytes_concat:
   forall m b ofs n1 n2 bytes1 bytes2,
@@ -473,6 +494,96 @@ Axiom store_float32_truncate:
   store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) =
   store Mfloat32 m b ofs (Vfloat n).
 
+(** ** Properties of [storebytes]. *)
+
+(** [storebytes] preserves block validity, permissions, access validity, and bounds.
+  Moreover, a [storebytes] succeeds if and only if we have write permissions
+  on the addressed memory area. *)
+
+Axiom range_perm_storebytes:
+  forall m1 b ofs bytes,
+  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable ->
+  { m2 : mem | storebytes m1 b ofs bytes = Some m2 }.
+Axiom storebytes_range_perm:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable.
+Axiom perm_storebytes_1:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p.
+Axiom perm_storebytes_2:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p.
+Axiom storebytes_valid_access_1:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall chunk' b' ofs' p,
+  valid_access m1 chunk' b' ofs' p -> valid_access m2 chunk' b' ofs' p.
+Axiom storebytes_valid_access_2:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall chunk' b' ofs' p,
+  valid_access m2 chunk' b' ofs' p -> valid_access m1 chunk' b' ofs' p.
+Axiom nextblock_storebytes:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  nextblock m2 = nextblock m1.
+Axiom storebytes_valid_block_1:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall b', valid_block m1 b' -> valid_block m2 b'.
+Axiom storebytes_valid_block_2:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall b', valid_block m2 b' -> valid_block m1 b'.
+Axiom bounds_storebytes:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall b', bounds m2 b' = bounds m1 b'.
+
+(** Connections between [store] and [storebytes]. *)
+
+Axiom storebytes_store:
+  forall m1 b ofs chunk v m2,
+  storebytes m1 b ofs (encode_val chunk v) = Some m2 ->
+  (align_chunk chunk | ofs) ->
+  store chunk m1 b ofs v = Some m2.
+
+Axiom store_storebytes:
+  forall m1 b ofs chunk v m2,
+  store chunk m1 b ofs v = Some m2 ->
+  storebytes m1 b ofs (encode_val chunk v) = Some m2.
+
+(** Load-store properties. *)
+
+Axiom loadbytes_storebytes_same:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.
+Axiom loadbytes_storebytes_other:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall b' ofs' len,
+  len >= 0 ->
+  b' <> b
+  \/ ofs' + len <= ofs
+  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
+  loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len.
+Axiom load_storebytes_other:
+  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
+  forall chunk b' ofs',
+  b' <> b
+  \/ ofs' + size_chunk chunk <= ofs
+  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
+  load chunk m2 b' ofs' = load chunk m1 b' ofs'.
+
+(** Composing or decomposing [storebytes] operations at adjacent addresses. *)
+
+Axiom storebytes_concat:
+  forall m b ofs bytes1 m1 bytes2 m2,
+  storebytes m b ofs bytes1 = Some m1 ->
+  storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 ->
+  storebytes m b ofs (bytes1 ++ bytes2) = Some m2.
+Axiom storebytes_split:
+  forall m b ofs bytes1 bytes2 m2,
+  storebytes m b ofs (bytes1 ++ bytes2) = Some m2 ->
+  exists m1,
+     storebytes m b ofs bytes1 = Some m1
+  /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2.
+Axiom storebytes_empty:
+  forall m b ofs, storebytes m b ofs nil = Some m.
+
 (** ** Properties of [alloc]. *)
 
 (** The identifier of the freshly allocated block is the next block
@@ -717,6 +828,13 @@ Axiom loadv_extends:
   Val.lessdef addr1 addr2 ->
   exists v2, loadv chunk m2 addr2 = Some v2 /\ Val.lessdef v1 v2.
 
+Axiom loadbytes_extends:
+  forall m1 m2 b ofs len bytes1,
+  extends m1 m2 ->
+  loadbytes m1 b ofs len = Some bytes1 ->
+  exists bytes2, loadbytes m2 b ofs len = Some bytes2
+              /\ list_forall2 memval_lessdef bytes1 bytes2.
+
 Axiom store_within_extends:
   forall chunk m1 m2 b ofs v1 m1' v2,
   extends m1 m2 ->
@@ -743,6 +861,22 @@ Axiom storev_extends:
      storev chunk m2 addr2 v2 = Some m2'
   /\ extends m1' m2'.
 
+Axiom storebytes_within_extends:
+  forall m1 m2 b ofs bytes1 m1' bytes2,
+  extends m1 m2 ->
+  storebytes m1 b ofs bytes1 = Some m1' ->
+  list_forall2 memval_lessdef bytes1 bytes2 ->
+  exists m2',
+     storebytes m2 b ofs bytes2 = Some m2'
+  /\ extends m1' m2'.
+
+Axiom storebytes_outside_extends:
+  forall m1 m2 b ofs bytes2 m2',
+  extends m1 m2 ->
+  storebytes m2 b ofs bytes2 = Some m2' ->
+  ofs + Z_of_nat (length bytes2) <= low_bound m1 b \/ high_bound m1 b <= ofs ->
+  extends m1 m2'.
+
 Axiom alloc_extends:
   forall m1 m2 lo1 hi1 b m1' lo2 hi2,
   extends m1 m2 ->
@@ -891,6 +1025,14 @@ Axiom loadv_inject:
   val_inject f a1 a2 ->
   exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2.
 
+Axiom loadbytes_inject:
+  forall f m1 m2 b1 ofs len b2 delta bytes1,
+  inject f m1 m2 ->
+  loadbytes m1 b1 ofs len = Some bytes1 ->
+  f b1 = Some (b2, delta) ->
+  exists bytes2, loadbytes m2 b2 (ofs + delta) len = Some bytes2
+              /\ list_forall2 (memval_inject f) bytes1 bytes2.
+
 Axiom store_mapped_inject:
   forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
   inject f m1 m2 ->
@@ -927,6 +1069,33 @@ Axiom storev_mapped_inject:
   exists n2,
     storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2.
 
+Axiom storebytes_mapped_inject:
+  forall f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
+  inject f m1 m2 ->
+  storebytes m1 b1 ofs bytes1 = Some n1 ->
+  f b1 = Some (b2, delta) ->
+  list_forall2 (memval_inject f) bytes1 bytes2 ->
+  exists n2,
+    storebytes m2 b2 (ofs + delta) bytes2 = Some n2
+    /\ inject f n1 n2.
+
+Axiom storebytes_unmapped_inject:
+  forall f m1 b1 ofs bytes1 n1 m2,
+  inject f m1 m2 ->
+  storebytes m1 b1 ofs bytes1 = Some n1 ->
+  f b1 = None ->
+  inject f n1 m2.
+
+Axiom storebytes_outside_inject:
+  forall f m1 m2 b ofs bytes2 m2',
+  inject f m1 m2 ->
+  (forall b' delta,
+    f b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= ofs
+    \/ ofs + Z_of_nat (length bytes2) <= low_bound m1 b' + delta) ->
+  storebytes m2 b ofs bytes2 = Some m2' ->
+  inject f m1 m2'.
+
 Axiom alloc_right_inject:
   forall f m1 m2 lo hi b2 m2',
   inject f m1 m2 ->
diff --git a/common/Values.v b/common/Values.v
index ceff333..4dc74b2 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -227,6 +227,12 @@ Definition modu (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
+Definition add_carry (v1 v2 cin: val): val :=
+  match v1, v2, cin with
+  | Vint n1, Vint n2, Vint c => Vint(Int.add_carry n1 n2 c)
+  | _, _, _ => Vundef
+  end.
+
 Definition and (v1 v2: val): val :=
   match v1, v2 with
   | Vint n1, Vint n2 => Vint(Int.and n1 n2)
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 4fc922b..f4d50e8 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -606,6 +606,13 @@ Definition nat_of_Z (z: Z) : nat :=
   | Zneg p => O
   end.
 
+Lemma nat_of_Z_of_nat:
+  forall n, nat_of_Z (Z_of_nat n) = n.
+Proof.
+  intros. unfold Z_of_nat. destruct n. auto.
+  simpl. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. auto.
+Qed.
+
 Lemma nat_of_Z_max:
   forall z, Z_of_nat (nat_of_Z z) = Zmax z 0.
 Proof.
@@ -1133,6 +1140,13 @@ Proof.
   induction 1; intros; simpl. auto. constructor; auto. 
 Qed.
 
+Lemma list_forall2_length:
+  forall l1 l2,
+  list_forall2 l1 l2 -> length l1 = length l2.
+Proof.
+  induction 1; simpl; congruence.
+Qed.
+
 End FORALL2.
 
 Lemma list_forall2_imply:
diff --git a/lib/Integers.v b/lib/Integers.v
index 30f692a..6e7a6cb 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -167,6 +167,11 @@ Definition divu (x y: int) : int :=
 Definition modu (x y: int) : int :=
   repr (Zmod (unsigned x) (unsigned y)).
 
+Definition add_carry (x y cin: int): int :=
+  if zlt (unsigned x + unsigned y + unsigned cin) modulus
+  then zero
+  else one.
+
 (** For bitwise operations, we need to convert between Coq integers [Z]
   and their bit-level representations.  Bit-level representations are
   represented as characteristic functions, that is, functions [f]
@@ -746,6 +751,11 @@ Proof.
   rewrite Zplus_0_r. apply repr_unsigned.
 Qed.
 
+Theorem add_zero_l: forall x, add zero x = x.
+Proof.
+  intros. rewrite add_commut. apply add_zero.
+Qed.
+
 Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
 Proof.
   intros; unfold add.
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index d876144..7ae5112 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -127,9 +127,11 @@ Definition label := positive.
 
 Inductive instruction : Type :=
   | Padd: ireg -> ireg -> ireg -> instruction                 (**r integer addition *)
+  | Padde: ireg -> ireg -> ireg -> instruction                 (**r integer addition with carry *)
   | Paddi: ireg -> ireg -> constant -> instruction            (**r add immediate *)
+  | Paddic: ireg -> ireg -> constant -> instruction            (**r add immediate and set carry *)
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
-  | Paddze: ireg -> ireg -> instruction                       (**r add Carry bit *)
+  | Paddze: ireg -> ireg -> instruction                       (**r add carry *)
   | Pallocframe: Z -> int -> instruction                      (**r allocate new stack frame *)
   | Pand_: ireg -> ireg -> ireg -> instruction                (**r bitwise and *)
   | Pandc: ireg -> ireg -> ireg -> instruction                (**r bitwise and-complement *)
@@ -211,6 +213,7 @@ Inductive instruction : Type :=
   | Pstw: ireg -> constant -> ireg -> instruction             (**r store 32-bit int *)
   | Pstwx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Psubfc: ireg -> ireg -> ireg -> instruction               (**r reversed integer subtraction *)
+  | Psubfe: ireg -> ireg -> ireg -> instruction               (**r reversed integer subtraction with carry *)
   | Psubfic: ireg -> ireg -> constant -> instruction          (**r integer subtraction from immediate *)
   | Pxor: ireg -> ireg -> ireg -> instruction                 (**r bitwise xor *)
   | Pxori: ireg -> ireg -> constant -> instruction            (**r bitwise xor with immediate *)
@@ -527,12 +530,19 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   match i with
   | Padd rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m
+  | Padde rd r1 r2 =>
+      OK (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY)
+                        #CARRY <- (Val.add_carry rs#r1 rs#r2 rs#CARRY))) m
   | Paddi rd r1 cst =>
       OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m
+  | Paddic rd r1 cst =>
+      OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst))
+                       #CARRY <- (Val.add_carry (gpr_or_zero rs r1) (const_low cst) Vzero))) m
   | Paddis rd r1 cst =>
       OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m
   | Paddze rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY))) m
+      OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY)
+                       #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m
   | Pallocframe sz ofs =>
       let (m1, stk) := Mem.alloc m 0 sz in
       let sp := Vptr stk Int.zero in
@@ -736,9 +746,14 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pstwx rd r1 r2 =>
       store2 Mint32 rd r1 r2 rs m
   | Psubfc rd r1 r2 =>
-      OK (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1) #CARRY <- Vundef)) m
+      OK (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1)
+                       #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) Vone))) m
+  | Psubfe rd r1 r2 =>
+      OK (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY)
+                       #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) rs#CARRY))) m
   | Psubfic rd r1 cst =>
-      OK (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) #CARRY <- Vundef)) m
+      OK (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1)
+                       #CARRY <- (Val.add_carry (const_low cst) (Val.notint rs#r1) Vone))) m
   | Pxor rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m
   | Pxori rd r1 cst =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index cecc13e..790b2b9 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -213,6 +213,10 @@ Definition crbit_for_cond (cond: condition) :=
 (** Recognition of comparisons [>= 0] and [< 0]. *)
 
 Inductive condition_class: condition -> list mreg -> Type :=
+  | condition_eq0:
+      forall n r, n = Int.zero -> condition_class (Ccompimm Ceq n) (r :: nil)
+  | condition_ne0:
+      forall n r, n = Int.zero -> condition_class (Ccompimm Cne n) (r :: nil)
   | condition_ge0:
       forall n r, n = Int.zero -> condition_class (Ccompimm Cge n) (r :: nil)
   | condition_lt0:
@@ -222,6 +226,16 @@ Inductive condition_class: condition -> list mreg -> Type :=
 
 Definition classify_condition (c: condition) (args: list mreg): condition_class c args :=
   match c as z1, args as z2 return condition_class z1 z2 with
+  | Ccompimm Ceq n, r :: nil =>
+      match Int.eq_dec n Int.zero with
+      | left EQ => condition_eq0 n r EQ
+      | right _ => condition_default (Ccompimm Ceq n) (r :: nil)
+      end
+  | Ccompimm Cne n, r :: nil =>
+      match Int.eq_dec n Int.zero with
+      | left EQ => condition_ne0 n r EQ
+      | right _ => condition_default (Ccompimm Cne n) (r :: nil)
+      end
   | Ccompimm Cge n, r :: nil =>
       match Int.eq_dec n Int.zero with
       | left EQ => condition_ge0 n r EQ
@@ -236,6 +250,33 @@ Definition classify_condition (c: condition) (args: list mreg): condition_class
       condition_default x y
   end.
 
+(** Translation of a condition operator.  The generated code sets
+  the [r] target register to 0 or 1 depending on the truth value of the
+  condition. *)
+
+Definition transl_cond_op
+             (cond: condition) (args: list mreg) (r: mreg) (k: code) :=
+  match classify_condition cond args with
+  | condition_eq0 _ a _ =>
+      Psubfic GPR0 (ireg_of a) (Cint Int.zero) ::
+      Padde (ireg_of r) GPR0 (ireg_of a) :: k
+  | condition_ne0 _ a _ =>
+      Paddic GPR0 (ireg_of a) (Cint Int.mone) ::
+      Psubfe (ireg_of r) GPR0 (ireg_of a) :: k
+  | condition_ge0 _ a _ =>
+      Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one ::
+      Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k
+  | condition_lt0 _ a _ =>
+      Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k
+  | condition_default _ _ =>
+      let p := crbit_for_cond cond in
+      transl_cond cond args
+        (Pmfcrbit (ireg_of r) (fst p) ::
+         if snd p
+         then k
+         else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)
+  end.
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -350,20 +391,7 @@ Definition transl_op
   | Ofloatofwords, a1 :: a2 :: nil =>
       Pfmake (freg_of r) (ireg_of a1) (ireg_of a2) :: k
   | Ocmp cmp, _ =>
-      match classify_condition cmp args with
-      | condition_ge0 _ a _ =>
-          Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one ::
-          Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k
-      | condition_lt0 _ a _ =>
-          Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k
-      | condition_default _ _ =>
-          let p := crbit_for_cond cmp in
-          transl_cond cmp args
-            (Pmfcrbit (ireg_of r) (fst p) ::
-             if snd p
-             then k
-             else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)
-      end
+      transl_cond_op cmp args r k
   | _, _ =>
       k (**r never happens for well-typed code *)
   end.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 97b04bb..1d270e5 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -417,28 +417,15 @@ Proof.
 Qed.
 Hint Rewrite transl_cond_label: labels.
 
-Remark transl_op_cmp_label:
+Remark transl_cond_op_label:
   forall c args r k,
-  find_label lbl
-    (match classify_condition c args with
-     | condition_ge0 _ a _ =>
-        Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one
-        :: Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k
-     | condition_lt0 _ a _ =>
-        Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k
-     | condition_default _ _ =>
-        transl_cond c args
-          (Pmfcrbit (ireg_of r) (fst (crbit_for_cond c))
-           :: (if snd (crbit_for_cond c)
-               then k
-               else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k))
-    end) = find_label lbl k.
+  find_label lbl (transl_cond_op c args r k) = find_label lbl k.
 Proof.
-  intros. destruct (classify_condition c args); auto. 
-  autorewrite with labels. 
-  case (snd (crbit_for_cond c)); auto.
+  intros c args.
+  unfold transl_cond_op. destruct (classify_condition c args); intros; auto.
+  autorewrite with labels. destruct (snd (crbit_for_cond c)); auto. 
 Qed.
-Hint Rewrite transl_op_cmp_label: labels.
+Hint Rewrite transl_cond_op_label: labels.
 
 Remark transl_op_label:
   forall op args r k, find_label lbl (transl_op op args r k) = find_label lbl k.
@@ -719,11 +706,7 @@ Proof.
   intros [rs2 [EX [RES OTH]]].
   left; eapply exec_straight_steps; eauto with coqlib.
   simpl. exists rs2; split. auto. 
-  apply agree_exten_2 with (rs#(preg_of dst) <- v').
-  auto with ppcgen. 
-  intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of dst)).
-  subst r0. auto.
-  apply OTH; auto.
+  apply agree_set_mreg with rs; auto with ppcgen. congruence. 
 Qed.
 
 Lemma exec_Msetstack_prop:
@@ -748,7 +731,7 @@ Proof.
   intros [rs2 [EX OTH]].
   left; eapply exec_straight_steps; eauto with coqlib.
   exists rs2; split; auto.
-  apply agree_exten_2 with rs; auto.
+  apply agree_exten with rs; auto with ppcgen.
 Qed.
 
 Lemma exec_Mgetparam_prop:
@@ -782,12 +765,11 @@ Proof.
   simpl. unfold load1. simpl. rewrite gpr_or_zero_not_zero.
   rewrite <- (sp_val _ _ _ AG). rewrite A. auto. congruence. auto. 
   auto.
-  assert (agree (Regmap.set IT1 Vundef ms) sp rs1).
-  unfold rs1. change (IR GPR11) with (preg_of IT1).  auto with ppcgen. 
-  apply agree_exten_2 with (rs1#(preg_of dst) <- v').
-  auto with ppcgen.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of dst)).
-  congruence. auto.
+  apply agree_set_mreg with rs1; auto with ppcgen. 
+  unfold rs1. change (IR GPR11) with (preg_of IT1). 
+  apply agree_nextinstr. apply agree_set_mreg with rs; auto with ppcgen.
+  intros. apply Pregmap.gso; auto with ppcgen.
+  congruence.
 Qed.
 
 Lemma exec_Mop_prop:
@@ -1123,9 +1105,9 @@ Proof.
   rewrite <- H0. simpl. constructor; auto.
   eapply code_tail_next_int; eauto. 
   apply sym_not_equal. auto with ppcgen.
-  apply agree_nextinstr. apply agree_set_mreg; auto. 
-  eapply agree_undef_temps; eauto. 
-  intros. repeat rewrite Pregmap.gso; auto. 
+  apply agree_nextinstr. apply agree_set_mreg_undef_temps with rs; auto. 
+  rewrite Pregmap.gss. auto.
+  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
 Qed.
 
 Lemma exec_Mannot_prop:
@@ -1178,7 +1160,7 @@ Proof.
   simpl; auto.
   econstructor; eauto.
   eapply Mach.find_label_incl; eauto.
-  apply agree_exten_2 with rs; auto. 
+  apply agree_exten with rs; auto with ppcgen.
 Qed.
 
 Lemma exec_Mcond_true_prop:
@@ -1221,7 +1203,7 @@ Proof.
   traceEq.
   econstructor; eauto. 
   eapply Mach.find_label_incl; eauto.
-  apply agree_exten_2 with rs2; auto with ppcgen. 
+  apply agree_undef_temps with rs2; auto with ppcgen.
 Qed.
 
 Lemma exec_Mcond_false_prop:
@@ -1245,7 +1227,7 @@ Proof.
   reflexivity.
   apply exec_straight_one. simpl. rewrite RES. reflexivity.
   reflexivity.
-  auto with ppcgen.
+  apply agree_nextinstr. apply agree_undef_temps with rs2; auto.
 Qed.
 
 Lemma exec_Mjumptable_prop:
@@ -1301,11 +1283,11 @@ Proof.
   change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq.
   econstructor; eauto. 
   eapply Mach.find_label_incl; eauto.
-  apply agree_exten_2 with rs2; auto. 
-  unfold rs2, rs1. apply agree_set_other; auto with ppcgen.
   apply agree_undef_temps with rs0; auto.
-  intros. rewrite Pregmap.gso; auto. rewrite nextinstr_inv; auto.
-  rewrite Pregmap.gso; auto. 
+  intros. rewrite INV3; auto with ppcgen.
+  unfold rs2. repeat rewrite Pregmap.gso; auto with ppcgen.
+  unfold rs1. rewrite nextinstr_inv; auto with ppcgen. 
+  apply Pregmap.gso; auto with ppcgen.
 Qed.
 
 Lemma exec_Mreturn_prop:
@@ -1433,7 +1415,7 @@ Proof.
   eapply exec_straight_steps_1; eauto.
   change (Int.unsigned Int.zero) with 0. constructor.
   (* match states *)
-  econstructor; eauto with coqlib. auto with ppcgen.
+  econstructor; eauto with coqlib. apply agree_undef_temps with rs4; auto.
 Qed.
 
 Lemma exec_function_external_prop:
@@ -1460,7 +1442,11 @@ Proof.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
-  unfold loc_external_result. auto with ppcgen.
+  unfold loc_external_result. 
+  apply agree_set_other; auto with ppcgen.
+  apply agree_set_mreg with rs; auto. 
+  rewrite Pregmap.gss; auto. 
+  intros; apply Pregmap.gso; auto.
 Qed.
 
 Lemma exec_return_prop:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 55a74be..42355ad 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -115,58 +115,90 @@ Qed.
 
 (** Characterization of PPC registers that correspond to Mach registers. *)
 
-Definition is_data_reg (r: preg) : Prop :=
+Definition is_data_reg (r: preg) : bool :=
   match r with
-  | IR GPR0 => False
-  | PC => False    | LR => False    | CTR => False
-  | CR0_0 => False | CR0_1 => False | CR0_2 => False | CR0_3 => False
-  | CARRY => False
-  | _ => True
+  | IR GPR0 => false
+  | PC => false    | LR => false    | CTR => false
+  | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false
+  | CARRY => false
+  | _ => true
   end.
 
 Lemma ireg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (ireg_of r).
+  forall (r: mreg), is_data_reg (ireg_of r) = true.
 Proof.
-  destruct r; exact I.
+  destruct r; reflexivity.
 Qed.
 
 Lemma freg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (ireg_of r).
+  forall (r: mreg), is_data_reg (ireg_of r) = true.
 Proof.
-  destruct r; exact I.
+  destruct r; reflexivity.
 Qed.
 
 Lemma preg_of_is_data_reg:
-  forall (r: mreg), is_data_reg (preg_of r).
+  forall (r: mreg), is_data_reg (preg_of r) = true.
 Proof.
-  destruct r; exact I.
+  destruct r; reflexivity.
 Qed.
 
-Lemma ireg_of_not_GPR1:
-  forall r, ireg_of r <> GPR1.
+Lemma data_reg_diff:
+  forall r r', is_data_reg r = true -> is_data_reg r' = false -> r <> r'.
 Proof.
-  intro. case r; discriminate.
+  intros. congruence.
 Qed.
-Lemma ireg_of_not_GPR0:
-  forall r, ireg_of r <> GPR0.
+
+Lemma ireg_diff:
+  forall r r', r <> r' -> IR r <> IR r'.
 Proof.
-  intro. case r; discriminate.
+  intros. congruence.
+Qed.
+
+Lemma diff_ireg:
+  forall r r', IR r <> IR r' -> r <> r'.
+Proof.
+  intros. congruence.
+Qed.
+
+Hint Resolve ireg_of_is_data_reg freg_of_is_data_reg preg_of_is_data_reg
+             data_reg_diff ireg_diff diff_ireg: ppcgen.
+
+Definition is_nontemp_reg (r: preg) : bool :=
+  match r with
+  | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false
+  | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false
+  | PC => false      | LR => false       | CTR => false
+  | CR0_0 => false   | CR0_1 => false    | CR0_2 => false    | CR0_3 => false
+  | CARRY => false
+  | _ => true
+  end.
+
+Remark is_nontemp_is_data:
+  forall r, is_nontemp_reg r = true -> is_data_reg r = true.
+Proof.
+  destruct r; simpl; try congruence. destruct i; congruence.
+Qed.
+
+Lemma nontemp_reg_diff:
+  forall r r', is_nontemp_reg r = true -> is_nontemp_reg r' = false -> r <> r'.
+Proof.
+  intros. congruence.
 Qed.
-Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR0: ppcgen.
 
-Lemma preg_of_not:
-  forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2.
+Hint Resolve is_nontemp_is_data nontemp_reg_diff: ppcgen.
+
+Lemma ireg_of_not_GPR1:
+  forall r, ireg_of r <> GPR1.
 Proof.
-  intros; red; intro. subst r2. elim H. apply preg_of_is_data_reg.
+  intro. case r; discriminate.
 Qed.
-Hint Resolve preg_of_not: ppcgen.
 
 Lemma preg_of_not_GPR1:
   forall r, preg_of r <> GPR1.
 Proof.
   intro. case r; discriminate.
 Qed.
-Hint Resolve preg_of_not_GPR1: ppcgen.
+Hint Resolve ireg_of_not_GPR1 preg_of_not_GPR1: ppcgen.
 
 Lemma int_temp_for_diff:
   forall r, IR(int_temp_for r) <> preg_of r.
@@ -229,79 +261,63 @@ Proof.
   intros. elim H; auto.
 Qed.
 
-Lemma agree_exten_1:
+Lemma agree_exten:
   forall ms sp rs rs',
   agree ms sp rs ->
-  (forall r, is_data_reg r -> rs'#r = rs#r) ->
+  (forall r, is_data_reg r = true -> rs'#r = rs#r) ->
   agree ms sp rs'.
 Proof.
-  intros. inv H. constructor.
-  apply H0. exact I.
-  auto.
-  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 <> IR GPR0 ->
-     r <> PC -> r <> LR -> r <> CTR ->
-     r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 ->
-     r <> CARRY ->
-     rs'#r = rs#r) ->
-  agree ms sp rs'.
-Proof.
-  intros. apply agree_exten_1 with rs. auto.
-  intros. apply H0; (red; intro; subst r; elim H1).
+  intros. inv H. constructor; auto. 
+  intros. rewrite H0; auto with ppcgen.
 Qed.
 
 (** Preservation of register agreement under various assignments. *)
 
 Lemma agree_set_mreg:
-  forall ms sp rs r v v',
+  forall ms sp rs r v rs',
   agree ms sp rs ->
-  Val.lessdef v v' ->
-  agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v').
+  Val.lessdef v (rs'#(preg_of r)) ->
+  (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Regmap.set r v ms) sp rs'.
 Proof.
-  intros. inv H. constructor.
-  rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1.
-  auto.
-  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.
+  intros. inv H. constructor; auto with ppcgen.
+  intros. unfold Regmap.set. destruct (RegEq.eq r0 r).
+  subst r0. auto.
+  rewrite H1; auto with ppcgen. red; intros; 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) ->
+  forall ms sp rs r v (rs': regset),
+  agree ms sp rs ->
+  Val.lessdef v (rs'#(ireg_of r)) ->
   mreg_type r = Tint ->
-  agree ms sp (rs#(ireg_of r) <- v).
+  (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Regmap.set r v ms) sp rs'.
 Proof.
-  intros. unfold preg_of in H. rewrite H0 in H. auto.
+  intros. eapply agree_set_mreg; eauto.  unfold preg_of; rewrite H1; 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) ->
+  forall ms sp rs r v (rs': regset),
+  agree ms sp rs ->
+  Val.lessdef v (rs'#(freg_of r)) ->
   mreg_type r = Tfloat ->
-  agree ms sp (rs#(freg_of r) <- v).
+  (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Regmap.set r v ms) sp rs'.
 Proof.
-  intros. unfold preg_of in H. rewrite H0 in H. auto.
+  intros. eapply agree_set_mreg; eauto.  unfold preg_of; rewrite H1; 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) ->
+  is_data_reg r = false ->
   agree ms sp (rs#r <- v).
 Proof.
-  intros. apply agree_exten_1 with rs.
-  auto. intros. apply Pregmap.gso. red; intro; subst r0; contradiction.
+  intros. apply agree_exten with rs.
+  auto. intros. apply Pregmap.gso. congruence.
 Qed.
 Hint Resolve agree_set_other: ppcgen.
 
@@ -313,24 +329,49 @@ Proof.
 Qed.
 Hint Resolve agree_nextinstr: ppcgen.
 
-Lemma agree_set_mireg_twice:
-  forall ms sp rs r v v' v1,
+Lemma agree_undef_regs:
+  forall rl ms sp rs rs',
   agree ms sp rs ->
-  mreg_type r = Tint ->
-  Val.lessdef v v' ->
-  agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v1 #(ireg_of r) <- v').
-Proof.
-  intros. replace (IR (ireg_of r)) with (preg_of r). inv H.
-  split. repeat (rewrite Pregmap.gso; auto with ppcgen). auto.
-  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.
+  (forall r, is_data_reg r = true -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) ->
+  agree (undef_regs rl ms) sp rs'.
+Proof.
+  induction rl; simpl; intros.
+  apply agree_exten with rs; auto.
+  apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))).
+  apply agree_set_mreg with rs; auto with ppcgen. 
+  intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of a)).
+  congruence. auto.
+  intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of a)).
+  congruence. apply H0; auto. intuition congruence.
+Qed.
+
+Lemma agree_undef_temps:
+  forall ms sp rs rs',
+  agree ms sp rs ->
+  (forall r, is_nontemp_reg r = true -> rs'#r = rs#r) ->
+  agree (undef_temps ms) sp rs'.
+Proof.
+  unfold undef_temps. intros. apply agree_undef_regs with rs; auto.
+  simpl. unfold preg_of; simpl. intros. intuition.
+  apply H0. destruct r; simpl in *; auto.
+  destruct i; intuition. destruct f; intuition.
+Qed.
+Hint Resolve agree_undef_temps: ppcgen.
+
+Lemma agree_set_mreg_undef_temps:
+  forall ms sp rs r v rs',
+  agree ms sp rs ->
+  Val.lessdef v (rs'#(preg_of r)) ->
+  (forall r', is_nontemp_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  agree (Regmap.set r v (undef_temps ms)) sp rs'.
+Proof.
+  intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))).
+  apply agree_undef_temps with rs; auto.
+  intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). 
+  congruence. apply H1; auto. 
+  auto.
+  intros. rewrite Pregmap.gso; auto. 
 Qed.
-Hint Resolve agree_set_mireg_twice: ppcgen.
 
 Lemma agree_set_twice_mireg:
   forall ms sp rs r v v1 v',
@@ -353,101 +394,6 @@ Proof.
   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 ->
-  Val.lessdef v rs'#(ireg_of r) ->
-  (forall r', 
-     r' <> IR GPR0 ->
-     r' <> PC -> r' <> LR -> r' <> CTR ->
-     r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 ->
-     r' <> CARRY ->
-     r' <> IR (ireg_of r) -> rs'#r' = rs#r') ->
-  agree (Regmap.set r v ms) sp rs'.
-Proof.
-  intros. set (v' := rs'#(ireg_of r)). 
-  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.
-Hint Resolve agree_set_mireg_exten: ppcgen.
-
-Lemma agree_undef_regs:
-  forall rl ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, is_data_reg r -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) ->
-  agree (undef_regs rl ms) sp rs'.
-Proof.
-  induction rl; simpl; intros.
-  apply agree_exten_1 with rs; auto.
-  apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))).
-  apply agree_set_mreg; auto.
-  intros. unfold Pregmap.set.
-  destruct (PregEq.eq r (preg_of a)).
-  congruence.
-  apply H0. auto. intuition congruence.
-Qed.
-
-Lemma agree_undef_temps:
-  forall ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, 
-     r <> IR GPR0 ->
-     r <> PC -> r <> LR -> r <> CTR ->
-     r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 ->
-     r <> CARRY ->
-     r <> IR GPR11 -> r <> IR GPR12 ->
-     r <> FR FPR0 -> r <> FR FPR12 -> r <> FR FPR13 ->
-     rs'#r = rs#r) ->
-  agree (undef_temps ms) sp rs'.
-Proof.
-  unfold undef_temps. intros. apply agree_undef_regs with rs; auto.
-  simpl. unfold preg_of; simpl. intros. 
-  apply H0; (red; intro; subst; simpl in H1; intuition congruence).
-Qed.
-Hint Resolve agree_undef_temps: ppcgen.
-
-Lemma agree_undef_temps_2:
-  forall ms sp rs,
-  agree ms sp rs ->
-  agree (undef_temps ms) sp rs.
-Proof.
-  intros. apply agree_undef_temps with rs; auto. 
-Qed.
-Hint Resolve agree_undef_temps_2: ppcgen.
 
 (** Useful properties of the PC and GPR0 registers. *)
 
@@ -458,15 +404,6 @@ Proof.
 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.
-
 Lemma gpr_or_zero_not_zero:
   forall rs r, r <> GPR0 -> gpr_or_zero rs r = rs#r.
 Proof.
@@ -622,6 +559,19 @@ Qed.
 
 (** * Correctness of PowerPC constructor functions *)
 
+(*
+Ltac SIMP :=
+  match goal with
+  | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
+  | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto
+  | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto
+  | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
+  | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
+  end.
+*)
+Ltac SIMP :=
+  (rewrite nextinstr_inv || rewrite Pregmap.gss || rewrite Pregmap.gso); auto with ppcgen.
+
 (** Properties of comparisons. *)
 
 Lemma compare_float_spec:
@@ -630,15 +580,13 @@ Lemma compare_float_spec:
      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'.
+  /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> 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).
+  intros. unfold compare_float. repeat SIMP.
 Qed.
 
 Lemma compare_sint_spec:
@@ -647,15 +595,13 @@ Lemma compare_sint_spec:
      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'.
+  /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> 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).
+  intros. unfold compare_sint. repeat SIMP.
 Qed.
 
 Lemma compare_uint_spec:
@@ -664,15 +610,13 @@ Lemma compare_uint_spec:
      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'.
+  /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> 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).
+  intros. unfold compare_uint. repeat SIMP.
 Qed.
 
 (** Loading a constant. *)
@@ -689,11 +633,9 @@ Proof.
   (* addi *)
   exists (nextinstr (rs#r <- (Vint n))).
   split. apply exec_straight_one. 
-  simpl. rewrite Int.add_commut. rewrite Int.add_zero. reflexivity.
+  simpl. rewrite Int.add_zero_l. auto.
   reflexivity. 
-  split. rewrite nextinstr_inv; auto with ppcgen.
-   apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  split. repeat SIMP. intros; repeat SIMP. 
   (* addis *)
   generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro.
   exists (nextinstr (rs#r <- (Vint n))).
@@ -701,19 +643,16 @@ Proof.
   simpl. rewrite Int.add_commut. 
   rewrite <- H. rewrite low_high_s. reflexivity.
   reflexivity. 
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  split. repeat SIMP. intros; repeat SIMP. 
   (* addis + ori *)
   pose (rs1 := nextinstr (rs#r <- (Vint (Int.shl (high_u n) (Int.repr 16))))).
   exists (nextinstr (rs1#r <- (Vint n))).
   split. eapply exec_straight_two. 
-  simpl. rewrite Int.add_commut. rewrite Int.add_zero. reflexivity.
+  simpl. rewrite Int.add_zero_l. reflexivity.
   simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
   unfold Val.or. rewrite low_high_u. reflexivity.
   reflexivity. reflexivity.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  unfold rs1. split. repeat SIMP. intros; repeat SIMP. 
 Qed.
 
 (** Add integer immediate. *)
@@ -734,8 +673,7 @@ Proof.
   split. apply exec_straight_one. 
   simpl. rewrite gpr_or_zero_not_zero; auto.
   reflexivity. 
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. 
+  split. repeat SIMP. intros. repeat SIMP.
   (* addis *)
   generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro.
   exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))).
@@ -744,8 +682,7 @@ Proof.
   generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. intro.
   rewrite H2. auto.
   reflexivity.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  split. repeat SIMP. intros; repeat SIMP.
   (* addis + addi *)
   pose (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint (Int.shl (high_s n) (Int.repr 16)))))).
   exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))).
@@ -755,9 +692,7 @@ Proof.
   unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
   rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
   reflexivity. reflexivity. 
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  unfold rs1; split. repeat SIMP. intros; repeat SIMP.
 Qed. 
 
 (** And integer immediate. *)
@@ -770,10 +705,7 @@ Lemma andimm_correct:
      exec_straight (andimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = v
   /\ rs'#CR0_2 = Val.cmp Ceq v Vzero
-  /\ forall r': preg,
-       r' <> r1 -> r' <> GPR0 -> r' <> PC ->
-       r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 ->
-       rs'#r' = rs#r'.
+  /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
 Proof.
   intros. unfold andimm.
   case (Int.eq (high_u n) Int.zero).
@@ -782,9 +714,9 @@ Proof.
   generalize (compare_sint_spec (rs#r1 <- v) v Vzero).
   intros [A [B [C D]]].
   split. apply exec_straight_one. reflexivity. reflexivity.
-  split. rewrite D; try discriminate. apply Pregmap.gss. 
+  split. rewrite D; auto with ppcgen. SIMP. 
   split. auto.
-  intros. rewrite D; auto. apply Pregmap.gso; auto.
+  intros. rewrite D; auto with ppcgen. SIMP.
   (* andis *)
   generalize (Int.eq_spec (low_u n) Int.zero);
   case (Int.eq (low_u n) Int.zero); intro.
@@ -794,9 +726,9 @@ Proof.
   split. apply exec_straight_one. simpl.
   generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. 
   intro. rewrite H1. reflexivity. reflexivity.
-  split. rewrite D; try discriminate. apply Pregmap.gss. 
+  split. rewrite D; auto with ppcgen. SIMP. 
   split. auto.
-  intros. rewrite D; auto. apply Pregmap.gso; auto.
+  intros. rewrite D; auto with ppcgen. SIMP.
   (* loadimm + and *)
   generalize (loadimm_correct GPR0 n (Pand_ r1 r2 GPR0 :: k) rs m).
   intros [rs1 [EX1 [RES1 OTHER1]]].
@@ -807,9 +739,9 @@ Proof.
   apply exec_straight_one. simpl. rewrite RES1. 
   rewrite (OTHER1 r2). reflexivity. congruence. congruence.
   reflexivity. 
-  split. rewrite D; try discriminate. apply Pregmap.gss. 
+  split. rewrite D; auto with ppcgen. SIMP. 
   split. auto.
-  intros. rewrite D; auto. rewrite Pregmap.gso; auto.
+  intros. rewrite D; auto with ppcgen. SIMP.
 Qed.
 
 (** Or integer immediate. *)
@@ -827,8 +759,8 @@ Proof.
   (* ori *)
   exists (nextinstr (rs#r1 <- v)).
   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.
+  split. repeat SIMP.
+  intros. repeat SIMP.
   (* oris *)
   generalize (Int.eq_spec (low_u n) Int.zero);
   case (Int.eq (low_u n) Int.zero); intro.
@@ -836,19 +768,12 @@ Proof.
   split. apply exec_straight_one. simpl.
   generalize (low_high_u n). rewrite H. rewrite Int.or_zero. 
   intro. rewrite H0. reflexivity. reflexivity.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  split. repeat SIMP.
+  intros. repeat SIMP.
   (* oris + ori *)
-  pose (rs1 := nextinstr (rs#r1 <- (Val.or rs#r2 (Vint (Int.shl (high_u n) (Int.repr 16)))))).
-  exists (nextinstr (rs1#r1 <- v)).
-  split. apply exec_straight_two with rs1 m.
-  reflexivity. simpl. unfold rs1 at 1. 
-  rewrite nextinstr_inv; auto with ppcgen.
-  rewrite Pregmap.gss. rewrite Val.or_assoc. simpl. 
-  rewrite low_high_u. reflexivity. reflexivity. reflexivity. 
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  econstructor; split. eapply exec_straight_two; simpl; reflexivity.
+  split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss.   rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. 
+  intros. repeat SIMP.
 Qed.
 
 (** Xor integer immediate. *)
@@ -866,8 +791,7 @@ Proof.
   (* xori *)
   exists (nextinstr (rs#r1 <- v)).
   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.
+  split. repeat SIMP. intros. repeat SIMP.
   (* xoris *)
   generalize (Int.eq_spec (low_u n) Int.zero);
   case (Int.eq (low_u n) Int.zero); intro.
@@ -875,20 +799,12 @@ Proof.
   split. apply exec_straight_one. simpl.
   generalize (low_high_u_xor n). rewrite H. rewrite Int.xor_zero. 
   intro. rewrite H0. reflexivity. reflexivity.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  split. repeat SIMP. intros. repeat SIMP.
   (* xoris + xori *)
-  pose (rs1 := nextinstr (rs#r1 <- (Val.xor rs#r2 (Vint (Int.shl (high_u n) (Int.repr 16)))))).
-  exists (nextinstr (rs1#r1 <- v)).
-  split. apply exec_straight_two with rs1 m.
-  reflexivity. simpl. unfold rs1 at 1. 
-  rewrite nextinstr_inv; try discriminate. 
-  rewrite Pregmap.gss. rewrite Val.xor_assoc. simpl. 
-  rewrite low_high_u_xor. reflexivity. reflexivity. reflexivity. 
-  split. rewrite nextinstr_inv; auto with ppcgen.
-  apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
-  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  econstructor; split. eapply exec_straight_two; simpl; reflexivity.
+  split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss.
+  rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. 
+  intros. repeat SIMP.
 Qed.
 
 (** Indexed memory loads. *)
@@ -906,24 +822,23 @@ Proof.
   intros. unfold loadind. destruct (Int.eq (high_s ofs) Int.zero).
 (* one load *)
   exists (nextinstr (rs#(preg_of dst) <- v)); split.
+  unfold preg_of. rewrite H0.
   destruct ty; apply exec_straight_one; auto with ppcgen; simpl.
   unfold load1. rewrite gpr_or_zero_not_zero; auto.
-  simpl in *. rewrite H. unfold preg_of; rewrite H0. auto.
+  simpl in *. rewrite H. auto.
   unfold load1. rewrite gpr_or_zero_not_zero; auto.
-  simpl in *. rewrite H. unfold preg_of; rewrite H0. auto.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+  simpl in *. rewrite H. auto.
+  split. repeat SIMP. intros. repeat SIMP.
 (* loadimm + one load *)
   exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
   exists (nextinstr (rs'#(preg_of dst) <- v)); split.
   eapply exec_straight_trans. eexact A.
+  unfold preg_of. rewrite H0.
   destruct ty; apply exec_straight_one; auto with ppcgen; simpl.
-  unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. 
-  unfold preg_of; rewrite H0. auto. congruence.
-  unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. 
-  unfold preg_of; rewrite H0. auto. congruence.
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. 
-  intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+  unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto.
+  unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto.
+  split. repeat SIMP.
+  intros. repeat SIMP. 
 Qed.
 
 (** Indexed memory stores. *)
@@ -948,7 +863,7 @@ Proof.
   intros. apply nextinstr_inv; auto.
 (* loadimm + one store *)
   exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. 
-  assert (rs' base = rs base). apply C; auto with ppcgen. congruence.
+  assert (rs' base = rs base). apply C; auto with ppcgen. 
   assert (rs' (preg_of src) = rs (preg_of src)). apply C; auto with ppcgen. 
   exists (nextinstr rs').
   split. eapply exec_straight_trans. eexact A. 
@@ -1035,17 +950,16 @@ Ltac UseTypeInfo :=
 
 (** Translation of conditions. *)
 
-Lemma transl_cond_correct_aux:
-  forall cond args k ms sp rs m,
+Lemma transl_cond_correct_1:
+  forall cond args k rs m,
   map mreg_type args = type_of_condition cond ->
-  agree ms sp rs ->
   exists rs',
      exec_straight (transl_cond cond args k) rs m k rs' m
   /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
        (if snd (crbit_for_cond cond)
         then eval_condition_total cond (map rs (map preg_of args))
         else Val.notbool (eval_condition_total cond (map rs (map preg_of args))))
-  /\ agree ms sp rs'.
+  /\ forall r, is_data_reg r = true -> rs'#r = rs#r.
 Proof.
   intros.
   destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo.
@@ -1056,7 +970,7 @@ Proof.
   apply exec_straight_one. simpl; reflexivity. reflexivity.
   split. 
   case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
-  apply agree_exten_2 with rs; auto.
+  auto with ppcgen.
   (* Ccompu *)
   destruct (compare_uint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)))
   as [A [B [C D]]].
@@ -1064,7 +978,7 @@ Proof.
   apply exec_straight_one. simpl; reflexivity. reflexivity.
   split. 
   case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
-  apply agree_exten_2 with rs; auto.
+  auto with ppcgen.
   (* Ccompimm *)
   case (Int.eq (high_s i) Int.zero).
   destruct (compare_sint_spec rs (rs (ireg_of m0)) (Vint i))
@@ -1073,21 +987,20 @@ Proof.
   apply exec_straight_one. simpl. eauto. reflexivity.
   split. 
   case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
-  apply agree_exten_2 with rs; auto.
+  auto with ppcgen.
   generalize (loadimm_correct GPR0 i (Pcmpw (ireg_of m0) GPR0 :: k) rs m).
   intros [rs1 [EX1 [RES1 OTH1]]].
   destruct (compare_sint_spec rs1 (rs (ireg_of m0)) (Vint i))
   as [A [B [C D]]].
   assert (rs1 (ireg_of m0) = rs (ireg_of m0)).
-    apply OTH1; auto with ppcgen. decEq. auto with ppcgen.
+    apply OTH1; auto with ppcgen. 
   exists (nextinstr (compare_sint rs1 (rs1 (ireg_of m0)) (Vint i))).
   split. eapply exec_straight_trans. eexact EX1.
   apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto.
   reflexivity. 
   split. rewrite H. 
   case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
-  apply agree_exten_2 with rs; auto.
-  intros. rewrite H; rewrite D; auto. 
+  intros. rewrite H; rewrite D; auto with ppcgen.
   (* Ccompuimm *)
   case (Int.eq (high_u i) Int.zero).
   destruct (compare_uint_spec rs (rs (ireg_of m0)) (Vint i))
@@ -1096,27 +1009,25 @@ Proof.
   apply exec_straight_one. simpl. eauto. reflexivity.
   split. 
   case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
-  apply agree_exten_2 with rs; auto.
+  auto with ppcgen.
   generalize (loadimm_correct GPR0 i (Pcmplw (ireg_of m0) GPR0 :: k) rs m).
   intros [rs1 [EX1 [RES1 OTH1]]].
   destruct (compare_uint_spec rs1 (rs (ireg_of m0)) (Vint i))
   as [A [B [C D]]].
-  assert (rs1 (ireg_of m0) = rs (ireg_of m0)).
-    apply OTH1; auto with ppcgen. decEq. auto with ppcgen.
+  assert (rs1 (ireg_of m0) = rs (ireg_of m0)). apply OTH1; auto with ppcgen.
   exists (nextinstr (compare_uint rs1 (rs1 (ireg_of m0)) (Vint i))).
   split. eapply exec_straight_trans. eexact EX1.
   apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto.
   reflexivity. 
   split. rewrite H. 
   case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
-  apply agree_exten_2 with rs; auto.
-  intros. rewrite H; rewrite D; auto. 
+  intros. rewrite H; rewrite D; auto with ppcgen.
   (* Ccompf *)
   destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m)
   as [rs' [EX [RES OTH]]].
   exists rs'. split. auto. 
   split. apply RES. 
-  apply agree_exten_2 with rs; auto.
+  auto with ppcgen.
   (* Cnotcompf *)
   destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m)
   as [rs' [EX [RES OTH]]].
@@ -1126,23 +1037,41 @@ Proof.
     intros v1 v2; unfold Val.cmpf; destruct v1; destruct v2; auto. 
     apply Val.notbool_idem2.
   rewrite H. case (snd (crbit_for_fcmp c)); simpl; auto.
-  apply agree_exten_2 with rs; auto.
+  auto with ppcgen.
   (* Cmaskzero *)
-  destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0))
-  as [rs' [A [B [C D]]]].
+  destruct (andimm_correct GPR0 (ireg_of m0) i k rs m)
+  as [rs' [A [B [C D]]]]. auto with ppcgen.
   exists rs'. split. assumption. 
   split. rewrite C. auto. 
-  apply agree_exten_2 with rs; auto.
+  auto with ppcgen.
   (* Cmasknotzero *)
-  destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0))
-  as [rs' [A [B [C D]]]].
+  destruct (andimm_correct GPR0 (ireg_of m0) i k rs m)
+  as [rs' [A [B [C D]]]]. auto with ppcgen.
   exists rs'. split. assumption. 
   split. rewrite C. rewrite Val.notbool_idem3. reflexivity. 
-  apply agree_exten_2 with rs; auto.
+  auto with ppcgen.
+Qed.
+
+Lemma transl_cond_correct_2:
+  forall cond args k rs m b,
+  map mreg_type args = type_of_condition cond ->
+  eval_condition cond (map rs (map preg_of args)) m = Some b ->
+  exists rs',
+     exec_straight (transl_cond cond args k) rs m k rs' m
+  /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
+       (if snd (crbit_for_cond cond)
+        then Val.of_bool b
+        else Val.notbool (Val.of_bool b))
+  /\ forall r, is_data_reg r = true -> rs'#r = rs#r.
+Proof.
+  intros.
+  assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b).
+    apply eval_condition_weaken with m. auto.
+  rewrite <- H1. eapply transl_cond_correct_1; eauto.
 Qed.
 
 Lemma transl_cond_correct:
-  forall cond args k ms sp rs m m' b,
+  forall cond args k ms sp rs m b m',
   map mreg_type args = type_of_condition cond ->
   agree ms sp rs ->
   eval_condition cond (map ms args) m = Some b ->
@@ -1156,10 +1085,121 @@ Lemma transl_cond_correct:
   /\ agree ms sp rs'.
 Proof.
   intros.
-  assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b).
-    apply eval_condition_weaken with m'. eapply eval_condition_lessdef; eauto. 
-    eapply preg_vals; eauto.
-  rewrite <- H3. eapply transl_cond_correct_aux; eauto.
+  exploit transl_cond_correct_2. eauto. 
+    eapply eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
+  intros [rs' [A [B C]]].
+  exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto.
+Qed.
+
+(** Translation of condition operators *)
+
+Remark add_carry_eq0:
+  forall i,
+  Vint (Int.add (Int.add (Int.sub Int.zero i) i)
+                (Int.add_carry Int.zero (Int.xor i Int.mone) Int.one)) =
+  Val.of_bool (Int.eq i Int.zero).
+Proof.
+  intros. rewrite <- Int.sub_add_l. rewrite Int.add_zero_l.
+  rewrite Int.sub_idem. rewrite Int.add_zero_l. fold (Int.not i).
+  predSpec Int.eq Int.eq_spec i Int.zero. 
+  subst i. reflexivity.
+  unfold Val.of_bool, Vfalse. decEq. 
+  unfold Int.add_carry. rewrite Int.unsigned_zero. rewrite Int.unsigned_one.
+  apply zlt_true.
+  generalize (Int.unsigned_range (Int.not i)); intro. 
+  assert (Int.unsigned (Int.not i) <> Int.modulus - 1).
+    red; intros.
+    assert (Int.repr (Int.unsigned (Int.not i)) = Int.mone).
+      rewrite H1. apply Int.mkint_eq. reflexivity. 
+   rewrite Int.repr_unsigned in H2. 
+   assert (Int.not (Int.not i) = Int.zero).
+   rewrite H2. apply Int.mkint_eq; reflexivity.
+  rewrite Int.not_involutive in H3. 
+  congruence.
+  omega.
+Qed.
+
+Remark add_carry_ne0:
+  forall i,
+  Vint (Int.add (Int.add i (Int.xor (Int.add i Int.mone) Int.mone))
+                (Int.add_carry i Int.mone Int.zero)) =
+  Val.of_bool (negb (Int.eq i Int.zero)).
+Proof.
+  intros. fold (Int.not (Int.add i Int.mone)). rewrite Int.not_neg.
+  rewrite (Int.add_commut  (Int.neg (Int.add i Int.mone))).
+  rewrite <- Int.sub_add_opp. rewrite Int.sub_add_r. rewrite Int.sub_idem. 
+  rewrite Int.add_zero_l. rewrite Int.add_neg_zero. rewrite Int.add_zero_l.
+  unfold Int.add_carry, Int.eq. 
+  rewrite Int.unsigned_zero.  rewrite Int.unsigned_mone.
+  unfold negb, Val.of_bool, Vtrue, Vfalse.
+  destruct (zeq (Int.unsigned i) 0); decEq.
+  apply zlt_true. omega.
+  apply zlt_false. generalize (Int.unsigned_range i). omega.
+Qed.
+
+Lemma transl_cond_op_correct:
+  forall cond args r k rs m b,
+  mreg_type r = Tint ->
+  map mreg_type args = type_of_condition cond ->
+  eval_condition cond (map rs (map preg_of args)) m = Some b ->
+  exists rs',
+     exec_straight (transl_cond_op cond args r k) rs m k rs' m
+  /\ rs'#(ireg_of r) = Val.of_bool b
+  /\ forall r', is_data_reg r' = true -> r' <> ireg_of r -> rs'#r' = rs#r'.
+Proof.
+  intros until args. unfold transl_cond_op.
+  destruct (classify_condition cond args);
+  intros until b; intros TY1 TY2 EV; simpl in TY2.
+(* eq 0 *)
+  inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *.
+  econstructor; split.
+  eapply exec_straight_two; simpl; reflexivity.
+  split. repeat SIMP. destruct (rs (ireg_of r)); inv EV. simpl. 
+  apply add_carry_eq0.
+  intros; repeat SIMP.
+(* ne 0 *)
+  inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *.
+  econstructor; split.
+  eapply exec_straight_two; simpl; reflexivity.
+  split. repeat SIMP. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+  destruct (rs (ireg_of r)); inv EV. simpl. 
+  apply add_carry_ne0.
+  intros; repeat SIMP.
+(* ge 0 *)
+  inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *.
+  econstructor; split.
+  eapply exec_straight_two; simpl; reflexivity.
+  split. repeat SIMP. rewrite Val.rolm_ge_zero. 
+  destruct (rs (ireg_of r)); simpl; congruence. 
+  intros; repeat SIMP.
+(* lt 0 *)
+  inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *.
+  econstructor; split.
+  apply exec_straight_one; simpl; reflexivity.
+  split. repeat SIMP. rewrite Val.rolm_lt_zero. 
+  destruct (rs (ireg_of r)); simpl; congruence. 
+  intros; repeat SIMP.
+(* default *)
+  set (bit := fst (crbit_for_cond c)).
+  set (isset := snd (crbit_for_cond c)).
+  set (k1 :=
+        Pmfcrbit (ireg_of r) bit ::
+        (if isset
+         then k
+         else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)).
+  generalize (transl_cond_correct_2 c rl k1 rs m b TY2 EV).
+  fold bit; fold isset. 
+  intros [rs1 [EX1 [RES1 AG1]]].
+  destruct isset.
+  (* bit set *)
+  econstructor; split.  eapply exec_straight_trans. eexact EX1. 
+  unfold k1. apply exec_straight_one; simpl; reflexivity. 
+  split. repeat SIMP. intros; repeat SIMP.
+  (* bit clear *)
+  econstructor; split.  eapply exec_straight_trans. eexact EX1. 
+  unfold k1. eapply exec_straight_two; simpl; reflexivity. 
+  split. repeat SIMP. rewrite RES1. destruct b; compute; reflexivity.
+  intros; repeat SIMP.
 Qed.
 
 (** Translation of arithmetic operations. *)
@@ -1167,255 +1207,143 @@ Qed.
 Ltac TranslOpSimpl :=
   econstructor; split;
   [ apply exec_straight_one; [simpl; eauto | reflexivity]
-  | auto 7 with ppcgen; fail ].
-(*
-  match goal with
-  | H: (Val.lessdef ?v ?v') |-
-         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; auto; fail
-     | auto with ppcgen ])
-  ||
-    (exists (nextinstr (rs#(freg_of res) <- v'));
-     split; 
-     [ apply exec_straight_one; auto; fail
-     | auto with ppcgen ])
-  end.
-*)
+  | split; intros; (repeat SIMP; fail) ].
 
-Lemma transl_op_correct:
-  forall op args res k ms sp rs m v m',
+Lemma transl_op_correct_aux:
+  forall op args res k (rs: regset) m v,
   wt_instr (Mop op args res) ->
-  agree ms sp rs ->
-  eval_operation ge sp op (map ms args) m = Some v ->
-  Mem.extends m m' ->
+  eval_operation ge (rs#GPR1) op (map rs (map preg_of args)) m = Some v ->
   exists rs',
-    exec_straight (transl_op op args res k) rs m' k rs' m'
-  /\ agree (Regmap.set res v (undef_op op ms)) sp rs'.
+     exec_straight (transl_op op args res k) rs m k rs' m
+  /\ rs'#(preg_of res) = v
+  /\ forall r,
+     match op with Omove => is_data_reg r = true | _ => is_nontemp_reg r = true end ->
+     r <> preg_of res -> rs'#r = rs#r.
 Proof.
   intros.
-  assert (exists v', Val.lessdef v v' /\
-          eval_operation_total ge sp op (map rs (map preg_of args)) = v').
-    exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto.
-    intros [v' [A B]]. exists v'; split; auto.
-    eapply eval_operation_weaken; eauto. 
-  destruct H3 as [v' [LD EQ]]. clear H1 H2.
+  exploit eval_operation_weaken; eauto. intro EV.
   inv H.
   (* Omove *)
   simpl in *. 
   exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))).
   split. unfold preg_of. rewrite <- H2.
   destruct (mreg_type r1); apply exec_straight_one; auto.
-  auto with ppcgen. 
+  split. repeat SIMP. intros; repeat SIMP.
   (* Other instructions *)
   destruct op; simpl; simpl in H5; injection H5; clear H5; intros;
   TypeInv; simpl in *; UseTypeInfo; try (TranslOpSimpl).
   (* Omove again *)
   congruence.
   (* Ointconst *)
-  destruct (loadimm_correct (ireg_of res) i k rs m')
-  as [rs' [A [B C]]]. 
-  exists rs'. split. auto. 
-  rewrite <- B in LD. eauto with ppcgen. 
-  (* Ofloatconst *)
-  exists (nextinstr (rs #GPR12 <- Vundef #(freg_of res) <- (Vfloat f))).
-  split. apply exec_straight_one. reflexivity. reflexivity.
-  apply agree_nextinstr. apply agree_set_mfreg; auto. apply agree_set_mreg; auto.
-  eapply agree_undef_temps; eauto. 
-  intros. apply Pregmap.gso; auto. 
+  destruct (loadimm_correct (ireg_of res) i k rs m) as [rs' [A [B C]]]. 
+  exists rs'. split. auto. split. auto. auto with ppcgen.
   (* Oaddrsymbol *)
-  change (find_symbol_offset ge i i0) with (symbol_offset ge i i0) in LD.
+  change (find_symbol_offset ge i i0) with (symbol_offset ge i i0) in *.
   set (v' := symbol_offset ge i i0) in *.
   caseEq (symbol_is_small_data i i0); intro SD.
   (* small data *)
-  exists (nextinstr (rs#(ireg_of res) <- v')); split.
-  apply exec_straight_one; auto. simpl.
+  econstructor; split. apply exec_straight_one; simpl; reflexivity.
+  split. repeat SIMP.
   rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. 
   destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero; auto. 
-  eauto with ppcgen. 
+  intros; repeat SIMP.
   (* not small data *)
-  pose (rs1 := nextinstr (rs#GPR12 <- (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; auto. apply agree_nextinstr.
-  eapply agree_undef_temps; eauto.
-  intros. apply Pregmap.gso; auto.
+Opaque Val.add.
+  econstructor; split. eapply exec_straight_two; simpl; reflexivity.
+  split. repeat SIMP. rewrite gpr_or_zero_zero.
+  rewrite gpr_or_zero_not_zero; auto with ppcgen. repeat SIMP. 
+  rewrite (Val.add_commut Vzero). rewrite high_half_zero. 
+  rewrite Val.add_commut. rewrite low_high_half. auto.
+  intros; repeat SIMP.
   (* Oaddrstack *)
-  assert (GPR1 <> GPR0). discriminate.
-  generalize (addimm_correct (ireg_of res) GPR1 i k rs m' (ireg_of_not_GPR0 res) H1). 
-  intros [rs' [EX [RES OTH]]].
-  exists rs'. split. auto. 
-  apply agree_set_mireg_exten with rs; auto with ppcgen.
-  rewrite (sp_val ms sp rs) in LD; auto. rewrite RES; auto. 
+  destruct (addimm_correct (ireg_of res) GPR1 i k rs m) as [rs' [EX [RES OTH]]].
+    auto with ppcgen. congruence.
+  exists rs'; auto with ppcgen.
   (* Ocast8unsigned *)
-  econstructor; split.
-  apply exec_straight_one. simpl; reflexivity. reflexivity. 
-  replace (Val.zero_ext 8 (rs (ireg_of m0)))
-      with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 255)) in LD.
-  auto with ppcgen. 
-  unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto.
+  econstructor; split. apply exec_straight_one; simpl; reflexivity.
+  split. repeat SIMP. 
+  destruct (rs (ireg_of m0)); simpl; auto. 
   rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
+  intros; repeat SIMP.
   (* Ocast16unsigned *)
-  econstructor; split.
-  apply exec_straight_one. simpl; reflexivity. reflexivity. 
-  replace (Val.zero_ext 16 (rs (ireg_of m0)))
-      with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 65535)) in LD.
-  auto with ppcgen. 
-  unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto.
+  econstructor; split. apply exec_straight_one; simpl; reflexivity.
+  split. repeat SIMP. 
+  destruct (rs (ireg_of m0)); simpl; auto. 
   rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
+  intros; repeat SIMP.
   (* Oaddimm *)
-  generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m'
-                            (ireg_of_not_GPR0 res) (ireg_of_not_GPR0 m0)).
-  intros [rs' [A [B C]]]. 
-  exists rs'. split. auto.
-  rewrite <- B in LD. eauto with ppcgen.  
+  destruct (addimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen.
+  exists rs'; auto with ppcgen.
   (* Osubimm *)
   case (Int.eq (high_s i) Int.zero).
+  TranslOpSimpl.
+  destruct (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]].
   econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  auto 7 with ppcgen.
-  generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m').
-  intros [rs1 [EX [RES OTH]]].
-  econstructor; split.
-  eapply exec_straight_trans. eexact EX. 
-  apply exec_straight_one. simpl; eauto. auto.
-  rewrite RES. rewrite OTH; auto with ppcgen.
-  assert (agree (undef_temps ms) sp rs1). eauto with ppcgen.  
-  auto with ppcgen. decEq; auto with ppcgen.
+  eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity.
+  split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. 
+  intros; repeat SIMP. 
   (* Omulimm *)
   case (Int.eq (high_s i) Int.zero).
+  TranslOpSimpl.
+  destruct (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]].
   econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto. 
-  auto with ppcgen.
-  generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m').
-  intros [rs1 [EX [RES OTH]]].
-  assert (agree (undef_temps ms) sp rs1). eauto with ppcgen.
-  econstructor; split.
-  eapply exec_straight_trans. eexact EX. 
-  apply exec_straight_one. simpl; eauto. auto.
-  rewrite RES. rewrite OTH; auto with ppcgen. decEq; auto with ppcgen.
+  eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity.
+  split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. 
+  intros; repeat SIMP.
   (* Oand *)
   set (v' := Val.and (rs (ireg_of m0)) (rs (ireg_of m1))) in *.
   pose (rs1 := rs#(ireg_of res) <- v').
   generalize (compare_sint_spec rs1 v' Vzero).
   intros [A [B [C D]]].
-  exists (nextinstr (compare_sint rs1 v' Vzero)).
-  split. apply exec_straight_one. auto. auto. 
-  apply agree_exten_2 with rs1. unfold rs1; auto with ppcgen.
-  auto.
+  econstructor; split. apply exec_straight_one; simpl; reflexivity.
+  split. rewrite D; auto with ppcgen. unfold rs1. SIMP. 
+  intros. rewrite D; auto with ppcgen. unfold rs1. SIMP.
   (* Oandimm *)
-  generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m'
-                             (ireg_of_not_GPR0 m0)).
-  intros [rs' [A [B [C D]]]]. 
-  exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen.
+  destruct (andimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B [C D]]]]; auto with ppcgen.
+  exists rs'; auto with ppcgen.
   (* Oorimm *)
-  generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m').
-  intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. 
+  destruct (orimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. 
+  exists rs'; auto with ppcgen.
   (* Oxorimm *)
-  generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m').
-  intros [rs' [A [B C]]]. 
-  exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen.
-  (* Oxhrximm *)
-  pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (rs (ireg_of m0)) (Vint i)) #CARRY <- (Val.shr_carry (rs (ireg_of m0)) (Vint i)))).
-  exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (rs (ireg_of m0)) (Vint i)))).
-  split. apply exec_straight_two with rs1 m'.
-  auto. simpl. decEq. decEq. decEq. 
-  unfold rs1. repeat (rewrite nextinstr_inv; try discriminate).
-  rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. 
-  apply Val.shrx_carry. auto with ppcgen. auto. auto. 
-  apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. 
-  apply agree_set_commut. auto with ppcgen. 
-  apply agree_set_other. apply agree_set_mireg_twice; auto with ppcgen. 
-  compute; auto. auto with ppcgen.
+  destruct (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. 
+  exists rs'; auto with ppcgen.
+  (* Oshrximm *)
+  econstructor; split.
+  eapply exec_straight_two; simpl; reflexivity. 
+  split. repeat SIMP. apply Val.shrx_carry. 
+  intros; repeat SIMP. 
   (* Oroli *)
   destruct (mreg_eq m0 res). subst m0.
   TranslOpSimpl.
   econstructor; split.
-  eapply exec_straight_three.
-  simpl. reflexivity. 
-  simpl. reflexivity.
-  simpl. reflexivity.
-  auto. auto. auto.
-  set (rs1 := nextinstr (rs # GPR0 <- (rs (ireg_of m0)))).
-  set (rs2 := nextinstr (rs1 # GPR0 <-
-        (Val.or (Val.and (rs1 GPR0) (Vint (Int.not i0)))
-               (Val.rolm (rs1 (ireg_of m1)) i i0)))).
-  apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg. 
-  apply agree_undef_temps with rs. auto. 
-  intros. unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. 
-  unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. 
-  unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. 
-  unfold rs1. repeat rewrite nextinstr_inv; auto with ppcgen. 
-  rewrite Pregmap.gss. rewrite Pregmap.gso; auto with ppcgen. decEq. auto with ppcgen. 
-  (* Ointoffloat *)
-  econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg; auto.
-  apply agree_undef_temps with rs; auto. intros. 
-  repeat rewrite Pregmap.gso; auto. 
+  eapply exec_straight_three; simpl; reflexivity. 
+  split. repeat SIMP. intros; repeat SIMP.
   (* Ocmp *)
-  revert H1 LD; case (classify_condition c args); intros.
-  (* Optimization: compimm Cge 0 *)
-  subst n. simpl in *. inv H1. UseTypeInfo. 
-  set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))).
-  set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.xor (rs1#(ireg_of res)) (Vint Int.one)))).
-  exists rs2.
-  split. apply exec_straight_two with rs1 m'; auto.
-  rewrite <- Val.rolm_ge_zero in LD.
-  unfold rs2. apply agree_nextinstr.
-  unfold rs1. apply agree_nextinstr_commut. fold rs1.
-  replace (rs1 (ireg_of res)) with (Val.rolm (rs (ireg_of r)) Int.one Int.one).
-  apply agree_set_mireg_twice; auto with ppcgen.
-  unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. auto. 
-  auto with ppcgen. auto with ppcgen. 
-  (* Optimization: compimm Clt 0 *)
-  subst n. simpl in *. inv H1. UseTypeInfo. 
-  exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))).
-  split. apply exec_straight_one; auto. 
-  rewrite <- Val.rolm_lt_zero in LD.
-  auto with ppcgen. 
-  (* General case *)
-  set (bit := fst (crbit_for_cond c0)).
-  set (isset := snd (crbit_for_cond c0)).
-  set (k1 :=
-        Pmfcrbit (ireg_of res) bit ::
-        (if isset
-         then k
-         else Pxori (ireg_of res) (ireg_of res) (Cint Int.one) :: k)).
-  generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m' H1 H0).
-  fold bit; fold isset. 
-  intros [rs1 [EX1 [RES1 AG1]]].
-  set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#(reg_of_crbit bit)))).
-  destruct isset.
-  exists rs2.
-  split. apply exec_straight_trans with k1 rs1 m'. assumption.
-  unfold k1. apply exec_straight_one. 
-  reflexivity. reflexivity. 
-  unfold rs2. rewrite RES1. auto with ppcgen. 
-  econstructor. 
-  split. apply exec_straight_trans with k1 rs1 m'. assumption.
-  unfold k1. apply exec_straight_two with rs2 m'.
-  reflexivity. simpl. eauto. auto. auto. 
-  apply agree_nextinstr. 
-  unfold rs2 at 1. rewrite nextinstr_inv. rewrite Pregmap.gss. 
-  rewrite RES1. rewrite <- Val.notbool_xor. 
-  unfold rs2. auto 7 with ppcgen. 
-  apply eval_condition_total_is_bool.
-  auto with ppcgen. 
+  destruct (eval_condition c rs ## (preg_of ## args) m) as [ b | ] _eqn; try discriminate.
+  destruct (transl_cond_op_correct c args res k rs m b) as [rs' [A [B C]]]; auto.
+  exists rs'; intuition auto with ppcgen. 
+  rewrite B. destruct b; inv H0; auto.
+Qed.
+
+Lemma transl_op_correct:
+  forall op args res k ms sp rs m v m',
+  wt_instr (Mop op args res) ->
+  agree ms sp rs ->
+  eval_operation ge sp op (map ms args) m = Some v ->
+  Mem.extends m m' ->
+  exists rs',
+     exec_straight (transl_op op args res k) rs m' k rs' m'
+  /\ agree (Regmap.set res v (undef_op op ms)) sp rs'.
+Proof.
+  intros. 
+  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. 
+  intros [v' [A B]].  rewrite (sp_val _ _ _ H0) in A. 
+  exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]].
+  rewrite <- Q in B.
+  exists rs'; split. eexact P. 
+  unfold undef_op. destruct op;
+  (apply agree_set_mreg_undef_temps with rs || apply agree_set_mreg with rs);
+  auto.
 Qed.
 
 Lemma transl_load_store_correct:
@@ -1452,10 +1380,10 @@ Proof.
   set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
   exploit (H (Cint (low_s i)) temp rs1 k).
     simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto. 
-    unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. 
-    rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
-    discriminate.
-  intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+    unfold rs1; repeat SIMP. rewrite Val.add_assoc.
+Transparent Val.add.
+    simpl. rewrite low_high_s. auto.
+    intros; unfold rs1; repeat SIMP.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
   simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. 
@@ -1552,15 +1480,21 @@ Proof.
 (* mk1 *)
   intros. exists (nextinstr (rs1#(preg_of dst) <- v')). 
   split. apply exec_straight_one. rewrite H.
-  unfold load1. rewrite <- H6. rewrite C. auto.
-  auto with ppcgen.
-  eauto with ppcgen.
+  unfold load1. rewrite <- H6. rewrite C. auto. 
+  unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen.
+  apply agree_set_mreg with rs1. 
+  apply agree_undef_temps with rs; auto with ppcgen.
+  repeat SIMP. 
+  intros; repeat SIMP.
 (* mk2 *)
   intros. exists (nextinstr (rs#(preg_of dst) <- v')). 
   split. apply exec_straight_one. rewrite H0. 
   unfold load2. rewrite <- H6. rewrite C. auto.
-  auto with ppcgen.
-  eauto with ppcgen.
+  unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen.
+  apply agree_set_mreg with rs.
+  apply agree_undef_temps with rs; auto with ppcgen.
+  repeat SIMP. 
+  intros; repeat SIMP.
 (* not GPR0 *)
   congruence.
 Qed.
@@ -1611,9 +1545,9 @@ Proof.
   intros [rs3 [U V]].
   exists rs3; split.
   apply exec_straight_one. auto. rewrite V; auto with ppcgen. 
-  eapply agree_undef_temps; eauto. intros. 
-  rewrite V; auto. rewrite nextinstr_inv; auto. apply H7; auto. 
-  unfold int_temp_for. destruct (mreg_eq src IT2); auto.
+  apply agree_undef_temps with rs. auto. 
+  intros. rewrite V; auto with ppcgen. SIMP. apply H7; auto with ppcgen.
+  unfold int_temp_for. destruct (mreg_eq src IT2); auto with ppcgen.
 (* mk2 *)
   intros.
   exploit (H0 r1 r2 rs (nextinstr rs) m1').
@@ -1622,7 +1556,7 @@ Proof.
   exists rs3; split.
   apply exec_straight_one. auto. rewrite V; auto with ppcgen. 
   eapply agree_undef_temps; eauto. intros. 
-  rewrite V; auto. rewrite nextinstr_inv; auto.
+  rewrite V; auto with ppcgen. 
   unfold int_temp_for. destruct (mreg_eq src IT2); congruence.
 Qed.
 
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v
index 5b1f7d5..adc1529 100644
--- a/powerpc/Asmgenretaddr.v
+++ b/powerpc/Asmgenretaddr.v
@@ -147,11 +147,18 @@ Lemma transl_cond_tail:
 Proof. unfold transl_cond; intros; destruct cond; IsTail. Qed.
 Hint Resolve transl_cond_tail: ppcretaddr.
 
+Lemma transl_cond_op_tail:
+  forall cond args r k, is_tail k (transl_cond_op cond args r k).
+Proof.
+  unfold transl_cond_op; intros.
+  destruct (classify_condition cond args); IsTail.
+Qed.
+Hint Resolve transl_cond_op_tail: ppcretaddr.
+
 Lemma transl_op_tail:
   forall op args r k, is_tail k (transl_op op args r k).
 Proof.
   unfold transl_op; intros; destruct op; IsTail. 
-  destruct (classify_condition c args); IsTail.
 Qed.
 Hint Resolve transl_op_tail: ppcretaddr.
 
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index eacf1dd..efe5b98 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -504,8 +504,12 @@ let jumptables : (int * label list) list ref = ref []
 let print_instruction oc = function
   | Padd(r1, r2, r3) ->
       fprintf oc "	add	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Padde(r1, r2, r3) ->
+      fprintf oc "	adde	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Paddi(r1, r2, c) ->
       fprintf oc "	addi	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
+  | Paddic(r1, r2, c) ->
+      fprintf oc "	addic	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
   | Paddis(r1, r2, c) ->
       fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
   | Paddze(r1, r2) ->
@@ -724,6 +728,8 @@ let print_instruction oc = function
       fprintf oc "	stwx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psubfc(r1, r2, r3) ->
       fprintf oc "	subfc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Psubfe(r1, r2, r3) ->
+      fprintf oc "	subfe	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psubfic(r1, r2, c) ->
       fprintf oc "	subfic	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Pxor(r1, r2, r3) ->