Hybrid 64bit/32bit PowerPC port

This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.

The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.

In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.

5 files changed, 230 insertions, 70 deletions

diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v
index a5b543e1..c9e7bad5 100644
--- a/lib/BoolEqual.v
+++ b/lib/BoolEqual.v
@@ -17,7 +17,7 @@
 
 (** The [decide equality] tactic can generate a term of type
 [forall (x y: A), {x=y} + {x<>y}] if [A] is an inductive type.
-This term is a decidable equality function.  
+This term is a decidable equality function.
 
 Similarly, this module defines a [boolean_equality] tactic that generates
 a term of type [A -> A -> bool].  This term is a Boolean-valued equality
@@ -33,7 +33,7 @@ a decidable equality of type [forall (x y: A), {x=y} + {x<>y}].
 
 The advantage of the present tactics over the standard [decide equality]
 tactic is that the former produce smaller transparent definitions than
-the latter.  
+the latter.
 
 For a type [A] that has N constructors, [decide equality] produces a
 single term of size O(N^3), which must be kept transparent so that
@@ -91,7 +91,7 @@ Ltac bool_eq :=
   end.
 
 Lemma proj_sumbool_is_true:
-  forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A), 
+  forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A),
   proj_sumbool (f x x) = true.
 Proof.
   intros. unfold proj_sumbool. destruct (f x x). auto. elim n; auto.
@@ -119,7 +119,7 @@ Lemma proj_sumbool_true:
   forall (A: Type) (x y: A) (a: {x=y} + {x<>y}),
   proj_sumbool a = true -> x = y.
 Proof.
-  intros. destruct a. auto. discriminate.   
+  intros. destruct a. auto. discriminate.
 Qed.
 
 Ltac bool_eq_sound_case :=
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v
index 3bb6eee7..6383794d 100644
--- a/lib/Decidableplus.v
+++ b/lib/Decidableplus.v
@@ -30,14 +30,14 @@ Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) :=
   Decidable_witness := negb (@Decidable_witness P dP)
 }.
 Next Obligation.
-  rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt. 
+  rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt.
 Qed.
 
 Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
   Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ)
 }.
 Next Obligation.
-  rewrite eqb_true_iff. 
+  rewrite eqb_true_iff.
   split; intros.
   split; intros; eapply Decidable_sound; [rewrite <- H | rewrite H]; eapply Decidable_complete; eauto.
   destruct (@Decidable_witness Q dQ) eqn:D.
@@ -65,7 +65,7 @@ Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable
 Next Obligation.
   split.
 - intros. rewrite Decidable_complete in H by auto. eapply Decidable_sound; eauto.
-- intros. destruct (@Decidable_witness P dP) eqn:WP; auto. 
+- intros. destruct (@Decidable_witness P dP) eqn:WP; auto.
   eapply Decidable_complete. apply H. eapply Decidable_sound; eauto.
 Qed.
 
@@ -75,7 +75,7 @@ Program Definition Decidable_eq {A: Type} (eqdec: forall (x y: A), {x=y} + {x<>y
   Decidable_witness := proj_sumbool (eqdec x y)
 |}.
 Next Obligation.
-  split; intros. InvBooleans. auto. subst y. apply dec_eq_true. 
+  split; intros. InvBooleans. auto. subst y. apply dec_eq_true.
 Qed.
 
 Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
@@ -112,14 +112,14 @@ Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
   Decidable_witness := Z.leb x y
 }.
 Next Obligation.
-  apply Z.leb_le. 
+  apply Z.leb_le.
 Qed.
 
 Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
   Decidable_witness := Z.ltb x y
 }.
 Next Obligation.
-  apply Z.ltb_lt. 
+  apply Z.ltb_lt.
 Qed.
 
 Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := {
@@ -142,8 +142,8 @@ Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := {
 Next Obligation.
   split.
   intros. apply Z.eqb_eq in H. exists (y / x). auto.
-  intros [k EQ]. apply Z.eqb_eq. 
-  destruct (Z.eq_dec x 0). 
+  intros [k EQ]. apply Z.eqb_eq.
+  destruct (Z.eq_dec x 0).
   subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity.
   assert (k = y / x).
   { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. }
@@ -152,7 +152,7 @@ Qed.
 
 (** Deciding properties over lists *)
 
-Program Instance Decidable_forall_in_list : 
+Program Instance Decidable_forall_in_list :
       forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
       Decidable (forall x:A, In x l -> P x) := {
   Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l
@@ -160,10 +160,10 @@ Program Instance Decidable_forall_in_list :
 Next Obligation.
   rewrite List.forallb_forall. split; intros.
 - eapply Decidable_sound; eauto.
-- eapply Decidable_complete; eauto. 
+- eapply Decidable_complete; eauto.
 Qed.
 
-Program Instance Decidable_exists_in_list : 
+Program Instance Decidable_exists_in_list :
       forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
       Decidable (exists x:A, In x l /\ P x) := {
   Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l
@@ -188,8 +188,8 @@ Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Pro
 }.
 Next Obligation.
   rewrite List.forallb_forall. split; intros.
-- eapply Decidable_sound; eauto. apply H. apply Finite_elements_spec. 
-- eapply Decidable_complete; eauto. 
+- eapply Decidable_sound; eauto. apply H. apply Finite_elements_spec.
+- eapply Decidable_complete; eauto.
 Qed.
 
 Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
@@ -198,7 +198,7 @@ Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Pro
 Next Obligation.
   rewrite List.existsb_exists. split.
 - intros (x & A & B). exists x. eapply Decidable_sound; eauto.
-- intros (x & A). exists x; split. eapply Finite_elements_spec. eapply Decidable_complete; eauto. 
+- intros (x & A). exists x; split. eapply Finite_elements_spec. eapply Decidable_complete; eauto.
 Qed.
 
 (** Some examples of finite types. *)
diff --git a/lib/Floats.v b/lib/Floats.v
index 51b0c415..aa52b197 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -820,6 +820,75 @@ Proof.
 - omega.
 Qed.
 
+(** Conversions to/from 32-bit integers can be implemented by going through 64-bit integers. *)
+
+Remark ZofB_range_widen:
+  forall (f: float) n min1 max1 min2 max2,
+  ZofB_range _ _ f min1 max1 = Some n ->
+  min2 <= min1 -> max1 <= max2 ->
+  ZofB_range _ _ f min2 max2 = Some n.
+Proof.
+  intros. exploit ZofB_range_inversion; eauto. intros (A & B & C).
+  unfold ZofB_range; rewrite C.
+  replace (min2 <=? n) with true. replace (n <=? max2) with true. auto.
+  symmetry; apply Z.leb_le; omega.
+  symmetry; apply Z.leb_le; omega.
+Qed.
+
+Theorem to_int_to_long:
+  forall f n, to_int f = Some n -> to_long f = Some (Int64.repr (Int.signed n)).
+Proof.
+  unfold to_int, to_long; intros.
+  destruct (ZofB_range 53 1024 f Int.min_signed Int.max_signed) as [z|] eqn:Z; inv H.
+  exploit ZofB_range_inversion; eauto. intros (A & B & C).
+  replace (ZofB_range 53 1024 f Int64.min_signed Int64.max_signed) with (Some z).
+  simpl. rewrite Int.signed_repr; auto.
+  symmetry; eapply ZofB_range_widen; eauto. compute; congruence. compute; congruence.
+Qed.
+
+Theorem to_intu_to_longu:
+  forall f n, to_intu f = Some n -> to_longu f = Some (Int64.repr (Int.unsigned n)).
+Proof.
+  unfold to_intu, to_longu; intros.
+  destruct (ZofB_range 53 1024 f 0 Int.max_unsigned) as [z|] eqn:Z; inv H.
+  exploit ZofB_range_inversion; eauto. intros (A & B & C).
+  replace (ZofB_range 53 1024 f 0 Int64.max_unsigned) with (Some z).
+  simpl. rewrite Int.unsigned_repr; auto.
+  symmetry; eapply ZofB_range_widen; eauto. omega. compute; congruence.
+Qed.
+
+Theorem to_intu_to_long:
+  forall f n, to_intu f = Some n -> to_long f = Some (Int64.repr (Int.unsigned n)).
+Proof.
+  unfold to_intu, to_long; intros.
+  destruct (ZofB_range 53 1024 f 0 Int.max_unsigned) as [z|] eqn:Z; inv H.
+  exploit ZofB_range_inversion; eauto. intros (A & B & C).
+  replace (ZofB_range 53 1024 f Int64.min_signed Int64.max_signed) with (Some z).
+  simpl. rewrite Int.unsigned_repr; auto.
+  symmetry; eapply ZofB_range_widen; eauto. compute; congruence. compute; congruence.
+Qed.
+
+Theorem of_int_of_long:
+  forall n, of_int n = of_long (Int64.repr (Int.signed n)).
+Proof.
+  unfold of_int, of_long. intros. f_equal. rewrite Int64.signed_repr. auto.
+  generalize (Int.signed_range n). compute_this Int64.min_signed. compute_this Int64.max_signed. smart_omega.
+Qed.
+
+Theorem of_intu_of_longu:
+  forall n, of_intu n = of_longu (Int64.repr (Int.unsigned n)).
+Proof.
+  unfold of_intu, of_longu. intros. f_equal. rewrite Int64.unsigned_repr. auto.
+  generalize (Int.unsigned_range n). smart_omega.
+Qed.
+
+Theorem of_intu_of_long:
+  forall n, of_intu n = of_long (Int64.repr (Int.unsigned n)).
+Proof.
+  unfold of_intu, of_long. intros. f_equal. rewrite Int64.signed_repr. auto.
+  generalize (Int.unsigned_range n). compute_this Int64.min_signed; compute_this Int64.max_signed; smart_omega.
+Qed.
+
 End Float.
 
 (** * Single-precision FP numbers *)
diff --git a/lib/Integers.v b/lib/Integers.v
index b1fa982d..c44fa55f 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1224,9 +1224,9 @@ Proof.
   { unfold Q, R, Z.div, Z.modulo. destruct (Z.div_eucl N D); auto. }
   rewrite E2. rewrite zle_true. auto.
   assert (unsigned d <> 0).
-  { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. }   
+  { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. }
   assert (0 < D).
-  { unfold D. generalize (unsigned_range d); intros. omega. } 
+  { unfold D. generalize (unsigned_range d); intros. omega. }
   assert (0 <= Q <= max_unsigned).
   { unfold Q. apply Zdiv_interval_2.
     rewrite <- E1; apply unsigned_range_2.
@@ -1262,7 +1262,7 @@ Proof.
   set (Q := Z.quot N D); set (R := Z.rem N D).
   assert (E2: Z.quotrem N D = (Q, R)).
   { unfold Q, R, Z.quot, Z.rem. destruct (Z.quotrem N D); auto. }
-  rewrite E2. 
+  rewrite E2.
   assert (min_signed <= N <= max_signed) by (rewrite H2; apply signed_range).
   assert (min_signed <= Q <= max_signed).
   { unfold Q. destruct (zeq D 1); [ | destruct (zeq D (-1))].
@@ -1284,7 +1284,7 @@ Proof.
       rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega.
       apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. }
     rewrite Z.abs_lt in H4.
-    unfold min_signed, max_signed; omega. 
+    unfold min_signed, max_signed; omega.
   }
   unfold proj_sumbool; rewrite ! zle_true by omega; simpl.
   unfold Q, R; rewrite H2; auto.
@@ -2186,6 +2186,16 @@ Proof.
     + omega.
 Qed.
 
+Theorem sub_ltu:
+  forall x y,
+    ltu x y = true ->
+    0 <= unsigned y - unsigned x <= unsigned y.
+Proof.
+  intros.
+  generalize (ltu_inv x y H). intros .
+  split. omega. omega.
+Qed.
+
 Theorem shru_zero: forall x, shru x zero = x.
 Proof.
   bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega.
@@ -4036,8 +4046,13 @@ Definition shru' (x: int) (y: Int.int): int :=
   repr (Z.shiftr (unsigned x) (Int.unsigned y)).
 Definition shr' (x: int) (y: Int.int): int :=
   repr (Z.shiftr (signed x) (Int.unsigned y)).
+Definition rol' (x: int) (y: Int.int): int :=
+  rol x (repr (Int.unsigned y)).
 Definition shrx' (x: int) (y: Int.int): int :=
   divs x (shl' one y).
+Definition shr_carry' (x: int) (y: Int.int): int :=
+  if lt x zero && negb (eq (and x (sub (shl' one y) one)) zero)
+  then one else zero.
 
 Lemma bits_shl':
   forall x y i,
@@ -4082,7 +4097,7 @@ Lemma shl'_mul_two_p:
   shl' x y = mul x (repr (two_p (Int.unsigned y))).
 Proof.
   intros. unfold shl', mul. apply eqm_samerepr.
-  rewrite Zshiftl_mul_two_p. apply eqm_mult. apply eqm_refl. apply eqm_unsigned_repr. 
+  rewrite Zshiftl_mul_two_p. apply eqm_mult. apply eqm_refl. apply eqm_unsigned_repr.
   generalize (Int.unsigned_range y); omega.
 Qed.
 
@@ -4099,11 +4114,50 @@ Proof.
   intros. rewrite shl'_one_two_p. apply shl'_mul_two_p.
 Qed.
 
+Theorem shl'_zero:
+  forall x, shl' x Int.zero = x.
+Proof.
+  intros. unfold shl'. rewrite Int.unsigned_zero. unfold Z.shiftl.
+  apply repr_unsigned.
+Qed.
+
+Theorem shru'_zero :
+  forall x, shru' x Int.zero = x.
+Proof.
+  intros. unfold shru'. rewrite Int.unsigned_zero. unfold Z.shiftr.
+  apply repr_unsigned.
+Qed.
+
+Theorem shr'_zero :
+  forall x, shr' x Int.zero = x.
+Proof.
+  intros. unfold shr'. rewrite Int.unsigned_zero. unfold Z.shiftr.
+  apply repr_signed.
+Qed.
+
 Theorem shrx'_zero:
   forall x, shrx' x Int.zero = x.
 Proof.
-  intros. change (shrx' x Int.zero) with (shrx x zero). apply shrx_zero. compute; auto. 
-Qed. 
+  intros. change (shrx' x Int.zero) with (shrx x zero). apply shrx_zero. compute; auto.
+Qed.
+
+Theorem shrx'_carry:
+  forall x y,
+  Int.ltu y (Int.repr 63) = true ->
+  shrx' x y = add (shr' x y) (shr_carry' x y).
+Proof.
+  intros. apply Int.ltu_inv in H. change (Int.unsigned (Int.repr 63)) with 63 in H.
+  set (y1 := Int64.repr (Int.unsigned y)).
+  assert (U: unsigned y1 = Int.unsigned y).
+  { apply unsigned_repr. assert (63 < max_unsigned) by reflexivity. omega. }
+  transitivity (shrx x y1).
+- unfold shrx', shrx, shl', shl. rewrite U; auto.
+- rewrite shrx_carry. 
++ f_equal. 
+  unfold shr, shr'. rewrite U; auto.
+  unfold shr_carry, shr_carry', shl, shl'. rewrite U; auto.
++ unfold ltu. apply zlt_true. rewrite U; tauto. 
+Qed.
 
 Theorem shrx'_shr_2:
   forall x y,
@@ -4119,7 +4173,7 @@ Proof.
   { unfold z; apply unsigned_repr; omega. }
   assert (B: unsigned (sub (repr 64) z) = Int.unsigned (Int.sub (Int.repr 64) y)).
   { unfold z. unfold sub, Int.sub.
-    change (unsigned (repr 64)) with 64.  
+    change (unsigned (repr 64)) with 64.
     change (Int.unsigned (Int.repr 64)) with 64.
     rewrite (unsigned_repr (Int.unsigned y)) by omega.
     rewrite unsigned_repr, Int.unsigned_repr by omega.
@@ -4172,7 +4226,7 @@ Proof.
   replace (shl' x y) with (shl x (repr (Int.unsigned y))).
   replace (shru' x z) with (shru x (repr (Int.unsigned z))).
   apply or_ror; auto. rewrite F, H1. reflexivity.
-  unfold shru, shru'; rewrite <- B; auto. 
+  unfold shru, shru'; rewrite <- B; auto.
   unfold shl, shl'; rewrite <- A; auto.
 Qed.
 
@@ -4190,7 +4244,7 @@ Proof.
   replace (shl' x y) with (shl x y').
   replace (shl' (shl x y') z) with (shl (shl x y') z').
   replace (shl' x (Int.add y z)) with (shl x (add y' z')).
-  apply shl_shl; auto. apply zlt_true. rewrite <- E. 
+  apply shl_shl; auto. apply zlt_true. rewrite <- E.
   change (unsigned iwordsize) with zwordsize. tauto.
   unfold shl, shl'. rewrite E; auto.
   unfold shl at 1, shl'. rewrite <- B; auto.
@@ -4211,7 +4265,7 @@ Proof.
   replace (shru' x y) with (shru x y').
   replace (shru' (shru x y') z) with (shru (shru x y') z').
   replace (shru' x (Int.add y z)) with (shru x (add y' z')).
-  apply shru_shru; auto. apply zlt_true. rewrite <- E. 
+  apply shru_shru; auto. apply zlt_true. rewrite <- E.
   change (unsigned iwordsize) with zwordsize. tauto.
   unfold shru, shru'. rewrite E; auto.
   unfold shru at 1, shru'. rewrite <- B; auto.
@@ -4232,7 +4286,7 @@ Proof.
   replace (shr' x y) with (shr x y').
   replace (shr' (shr x y') z) with (shr (shr x y') z').
   replace (shr' x (Int.add y z)) with (shr x (add y' z')).
-  apply shr_shr; auto. apply zlt_true. rewrite <- E. 
+  apply shr_shr; auto. apply zlt_true. rewrite <- E.
   change (unsigned iwordsize) with zwordsize. tauto.
   unfold shr, shr'. rewrite E; auto.
   unfold shr at 1, shr'. rewrite <- B; auto.
@@ -4256,8 +4310,8 @@ Proof.
   intros.
   destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]].
   exploit Z_one_bits_range; eauto. intros R.
-  unfold Int.ltu. rewrite EQ. rewrite Int.unsigned_repr. 
-  change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. omega. 
+  unfold Int.ltu. rewrite EQ. rewrite Int.unsigned_repr.
+  change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. omega.
   assert (zwordsize < Int.max_unsigned) by reflexivity. omega.
 Qed.
 
@@ -4276,13 +4330,13 @@ Proof.
   { induction l; simpl; intros.
   - auto.
   - rewrite IHl by eauto. apply eqm_samerepr; apply eqm_add.
-  + rewrite shl'_one_two_p. rewrite Int.unsigned_repr. apply eqm_sym; apply eqm_unsigned_repr.  
+  + rewrite shl'_one_two_p. rewrite Int.unsigned_repr. apply eqm_sym; apply eqm_unsigned_repr.
     exploit (H a). auto. assert (zwordsize < Int.max_unsigned) by reflexivity. omega.
-  + apply eqm_sym; apply eqm_unsigned_repr. 
+  + apply eqm_sym; apply eqm_unsigned_repr.
   }
-  intros. rewrite <- (repr_unsigned x) at 1. unfold one_bits'. rewrite REC. 
+  intros. rewrite <- (repr_unsigned x) at 1. unfold one_bits'. rewrite REC.
   rewrite <- Z_one_bits_powerserie. auto. apply unsigned_range.
-  apply Z_one_bits_range.    
+  apply Z_one_bits_range.
 Qed.
 
 Lemma is_power2'_rng:
@@ -4290,7 +4344,7 @@ Lemma is_power2'_rng:
   is_power2' n = Some logn ->
   0 <= Int.unsigned logn < zwordsize.
 Proof.
-  unfold is_power2'; intros n logn P2. 
+  unfold is_power2'; intros n logn P2.
   destruct (Z_one_bits wordsize (unsigned n) 0) as [ | i [ | ? ?]] eqn:B; inv P2.
   assert (0 <= i < zwordsize).
   { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. }
@@ -4303,7 +4357,7 @@ Theorem is_power2'_range:
   forall n logn,
   is_power2' n = Some logn -> Int.ltu logn iwordsize' = true.
 Proof.
-  intros. unfold Int.ltu. change (Int.unsigned iwordsize') with zwordsize. 
+  intros. unfold Int.ltu. change (Int.unsigned iwordsize') with zwordsize.
   apply zlt_true. generalize (is_power2'_rng _ _ H). tauto.
 Qed.
 
@@ -4321,13 +4375,13 @@ Proof.
   assert (zwordsize < Int.max_unsigned) by reflexivity.
   omega.
 Qed.
-   
+
 Theorem mul_pow2':
   forall x n logn,
   is_power2' n = Some logn ->
   mul x n = shl' x logn.
 Proof.
-  intros. rewrite shl'_mul. f_equal. rewrite shl'_one_two_p. 
+  intros. rewrite shl'_mul. f_equal. rewrite shl'_one_two_p.
   rewrite <- (repr_unsigned n). f_equal. apply is_power2'_correct; auto.
 Qed.
 
@@ -4855,6 +4909,43 @@ Proof.
   rewrite zlt_true by omega; auto.
 Qed.
 
+(** Utility proofs for mixed 32bit and 64bit arithmetic *)
+
+Remark int_unsigned_range:
+  forall x, 0 <= Int.unsigned x <= max_unsigned.
+Proof.
+  intros.
+  unfold max_unsigned. unfold modulus.
+  generalize (Int.unsigned_range x).
+  unfold Int.modulus in *.
+  change (wordsize) with  64%nat in *.
+  change (Int.wordsize) with 32%nat in *.
+  unfold two_power_nat. simpl.
+  omega.
+Qed.
+
+Remark int_unsigned_repr:
+  forall x, unsigned (repr (Int.unsigned x)) = Int.unsigned x.
+Proof.
+  intros. rewrite unsigned_repr. auto.
+  apply int_unsigned_range.
+Qed.
+
+Lemma int_sub_ltu:
+  forall x y,
+    Int.ltu x y= true ->
+    Int.unsigned (Int.sub y x) = unsigned (sub (repr (Int.unsigned y)) (repr (Int.unsigned x))).
+Proof.
+  intros. generalize (Int.sub_ltu x y H). intros. unfold Int.sub. unfold sub.
+  rewrite Int.unsigned_repr. rewrite unsigned_repr.
+  rewrite unsigned_repr by apply int_unsigned_range. rewrite int_unsigned_repr. reflexivity.
+  rewrite unsigned_repr by apply int_unsigned_range.
+  rewrite int_unsigned_repr. generalize (int_unsigned_range y).
+  omega.
+  generalize (Int.sub_ltu x y H). intros.
+  generalize (Int.unsigned_range_2 y). intros. omega.
+Qed.
+
 End Int64.
 
 Strategy 0 [Wordsize_64.wordsize].
@@ -4899,7 +4990,7 @@ Hypothesis _32: Archi.ptr64 = false.
 
 Lemma modulus_eq32: modulus = Int.modulus.
 Proof.
-  unfold modulus, wordsize. 
+  unfold modulus, wordsize.
   change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat).
   rewrite _32. reflexivity.
 Qed.
@@ -4923,8 +5014,8 @@ Qed.
 Lemma agree32_signed:
   forall a b, agree32 a b -> Ptrofs.signed a = Int.signed b.
 Proof.
-  unfold agree32; intros. unfold signed, Int.signed, half_modulus, Int.half_modulus. 
-  rewrite modulus_eq32. rewrite H. auto. 
+  unfold agree32; intros. unfold signed, Int.signed, half_modulus, Int.half_modulus.
+  rewrite modulus_eq32. rewrite H. auto.
 Qed.
 
 Lemma agree32_of_int:
@@ -4932,7 +5023,7 @@ Lemma agree32_of_int:
 Proof.
   unfold of_int; intros. rewrite <- (Int.repr_unsigned b) at 2. apply agree32_repr.
 Qed.
- 
+
 Lemma agree32_of_ints:
   forall b, agree32 (of_ints b) b.
 Proof.
@@ -4942,7 +5033,7 @@ Qed.
 Lemma agree32_of_int_eq:
   forall a b, agree32 a b -> of_int b = a.
 Proof.
-  unfold agree32, of_int; intros. rewrite <- H. apply repr_unsigned. 
+  unfold agree32, of_int; intros. rewrite <- H. apply repr_unsigned.
 Qed.
 
 Lemma agree32_of_ints_eq:
@@ -4954,7 +5045,7 @@ Qed.
 Lemma agree32_to_int:
   forall a, agree32 a (to_int a).
 Proof.
-  unfold agree32, to_int; intros. rewrite <- (agree32_repr (unsigned a)). 
+  unfold agree32, to_int; intros. rewrite <- (agree32_repr (unsigned a)).
   rewrite repr_unsigned; auto.
 Qed.
 
@@ -4974,21 +5065,21 @@ Lemma agree32_add:
   forall a1 b1 a2 b2,
   agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.add a1 a2) (Int.add b1 b2).
 Proof.
-  unfold agree32, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree32_repr. 
+  unfold agree32, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree32_repr.
 Qed.
 
 Lemma agree32_sub:
   forall a1 b1 a2 b2,
   agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.sub a1 a2) (Int.sub b1 b2).
 Proof.
-  unfold agree32, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree32_repr. 
+  unfold agree32, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree32_repr.
 Qed.
 
 Lemma agree32_mul:
   forall a1 b1 a2 b2,
   agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.mul a1 a2) (Int.mul b1 b2).
 Proof.
-  unfold agree32, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree32_repr. 
+  unfold agree32, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree32_repr.
 Qed.
 
 Lemma agree32_divs:
@@ -5004,7 +5095,7 @@ Lemma of_int_to_int:
 Proof.
   intros; unfold of_int, to_int. apply eqm_repr_eq. rewrite <- eqm32.
   apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
-Qed.   
+Qed.
 
 End AGREE32.
 
@@ -5014,7 +5105,7 @@ Hypothesis _64: Archi.ptr64 = true.
 
 Lemma modulus_eq64: modulus = Int64.modulus.
 Proof.
-  unfold modulus, wordsize. 
+  unfold modulus, wordsize.
   change Wordsize_Ptrofs.wordsize with (if Archi.ptr64 then 64%nat else 32%nat).
   rewrite _64. reflexivity.
 Qed.
@@ -5038,8 +5129,8 @@ Qed.
 Lemma agree64_signed:
   forall a b, agree64 a b -> Ptrofs.signed a = Int64.signed b.
 Proof.
-  unfold agree64; intros. unfold signed, Int64.signed, half_modulus, Int64.half_modulus. 
-  rewrite modulus_eq64. rewrite H. auto. 
+  unfold agree64; intros. unfold signed, Int64.signed, half_modulus, Int64.half_modulus.
+  rewrite modulus_eq64. rewrite H. auto.
 Qed.
 
 Lemma agree64_of_int:
@@ -5051,13 +5142,13 @@ Qed.
 Lemma agree64_of_int_eq:
   forall a b, agree64 a b -> of_int64 b = a.
 Proof.
-  unfold agree64, of_int64; intros. rewrite <- H. apply repr_unsigned. 
+  unfold agree64, of_int64; intros. rewrite <- H. apply repr_unsigned.
 Qed.
 
 Lemma agree64_to_int:
   forall a, agree64 a (to_int64 a).
 Proof.
-  unfold agree64, to_int64; intros. rewrite <- (agree64_repr (unsigned a)). 
+  unfold agree64, to_int64; intros. rewrite <- (agree64_repr (unsigned a)).
   rewrite repr_unsigned; auto.
 Qed.
 
@@ -5077,21 +5168,21 @@ Lemma agree64_add:
   forall a1 b1 a2 b2,
   agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.add a1 a2) (Int64.add b1 b2).
 Proof.
-  unfold agree64, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree64_repr. 
+  unfold agree64, Ptrofs.add, Int.add; intros. rewrite H, H0. apply agree64_repr.
 Qed.
 
 Lemma agree64_sub:
   forall a1 b1 a2 b2,
   agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.sub a1 a2) (Int64.sub b1 b2).
 Proof.
-  unfold agree64, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree64_repr. 
+  unfold agree64, Ptrofs.sub, Int.sub; intros. rewrite H, H0. apply agree64_repr.
 Qed.
 
 Lemma agree64_mul:
   forall a1 b1 a2 b2,
   agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.mul a1 a2) (Int64.mul b1 b2).
 Proof.
-  unfold agree64, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree64_repr. 
+  unfold agree64, Ptrofs.mul, Int.mul; intros. rewrite H, H0. apply agree64_repr.
 Qed.
 
 Lemma agree64_divs:
@@ -5107,16 +5198,16 @@ Lemma of_int64_to_int64:
 Proof.
   intros; unfold of_int64, to_int64. apply eqm_repr_eq. rewrite <- eqm64.
   apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
-Qed.   
+Qed.
 
 End AGREE64.
 
-Hint Resolve 
+Hint Resolve
   agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq
   agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs
   agree64_repr agree64_of_int agree64_of_int_eq
   agree64_to_int agree64_to_int_eq agree64_neg agree64_add agree64_sub agree64_mul agree64_divs : ptrofs.
-              
+
 End Ptrofs.
 
 Strategy 0 [Wordsize_Ptrofs.wordsize].
diff --git a/lib/Maps.v b/lib/Maps.v
index e2d4e965..cfb866ba 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -819,8 +819,8 @@ Module PTree <: TREE.
       (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
       (elements m) (elements n).
   Proof.
-    intros. apply elements_canonical_order'. 
-    intros. destruct (get i m) as [x|] eqn:GM. 
+    intros. apply elements_canonical_order'.
+    intros. destruct (get i m) as [x|] eqn:GM.
     exploit H; eauto. intros (y & P & Q). rewrite P; constructor; auto.
     destruct (get i n) as [y|] eqn:GN.
     exploit H0; eauto. intros (x & P & Q). congruence.
@@ -1265,7 +1265,7 @@ Module ITree(X: INDEXED_TYPE).
      | _, _ => False
     end.
   Proof.
-    unfold beq, get. intros. rewrite PTree.beq_correct in H. apply H. 
+    unfold beq, get. intros. rewrite PTree.beq_correct in H. apply H.
   Qed.
 
   Definition combine: forall (A B C: Type), (option A -> option B -> option C) -> t A -> t B -> t C := PTree.combine.
@@ -1636,8 +1636,8 @@ Proof.
   { induction l as [ | [k1 v1] l]; simpl; intros.
   - tauto.
   - apply IHl in H. unfold f in H. simpl in H. rewrite T.gsspec in H.
-    destruct H; auto. 
-    destruct (T.elt_eq k k1). inv H. auto. auto. 
+    destruct H; auto.
+    destruct (T.elt_eq k k1). inv H. auto. auto.
   }
   intros. apply REC in H. rewrite T.gempty in H. intuition congruence.
 Qed.
@@ -1650,7 +1650,7 @@ Proof.
             exists v, T.get k (fold_left f l m) = Some v).
   { induction l as [ | [k1 v1] l]; simpl; intros.
   - tauto.
-  - apply IHl. unfold f; rewrite T.gsspec. simpl. destruct (T.elt_eq k k1). 
+  - apply IHl. unfold f; rewrite T.gsspec. simpl. destruct (T.elt_eq k k1).
     right; econstructor; eauto.
     intuition congruence.
   }
@@ -1669,7 +1669,7 @@ Lemma of_list_unique:
   forall k v l1 l2,
   ~In k (map fst l2) -> T.get k (of_list (l1 ++ (k, v) :: l2)) = Some v.
 Proof.
-  intros. unfold of_list. rewrite fold_left_app. simpl. 
+  intros. unfold of_list. rewrite fold_left_app. simpl.
   rewrite of_list_unchanged by auto. unfold f; apply T.gss.
 Qed.
 
@@ -1683,8 +1683,8 @@ Proof.
   { induction l as [ | [k1 v1] l]; simpl; intros.
     contradiction.
     inv H. destruct H0.
-    inv H. rewrite of_list_unchanged by auto. apply T.gss. 
-    apply IHl; auto. 
+    inv H. rewrite of_list_unchanged by auto. apply T.gss.
+    apply IHl; auto.
   }
   intros; apply REC; auto.
 Qed.