Support for 64-bit architectures: generic support

- Introduce Archi.ptr64 parameter.
- Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise).
- Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated.
- Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers.
- Update the memory model accordingly.
- Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly.
- Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers.
- Update the compiler front-end and back-end accordingly.

9 files changed, 1004 insertions, 401 deletions

diff --git a/common/AST.v b/common/AST.v
index ae7178f4..e6fdec3c 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -18,6 +18,7 @@
 
 Require Import String.
 Require Import Coqlib Maps Errors Integers Floats.
+Require Archi.
 
 Set Implicit Arguments.
 
@@ -50,6 +51,8 @@ Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}
 Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
                      := list_eq_dec typ_eq.
 
+Definition Tptr : typ := if Archi.ptr64 then Tlong else Tint.
+
 Definition typesize (ty: typ) : Z :=
   match ty with
   | Tint => 4
@@ -63,6 +66,9 @@ Definition typesize (ty: typ) : Z :=
 Lemma typesize_pos: forall ty, typesize ty > 0.
 Proof. destruct ty; simpl; omega. Qed.
 
+Lemma typesize_Tptr: typesize Tptr = if Archi.ptr64 then 8 else 4.
+Proof. unfold Tptr; destruct Archi.ptr64; auto. Qed.
+
 (** All values of size 32 bits are also of type [Tany32].  All values
   are of type [Tany64].  This corresponds to the following subtyping
   relation over types. *)
@@ -150,6 +156,8 @@ Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}.
 Proof. decide equality. Defined.
 Global Opaque chunk_eq.
 
+Definition Mptr : memory_chunk := if Archi.ptr64 then Mint64 else Mint32.
+
 (** The type (integer/pointer or float) of a chunk. *)
 
 Definition type_of_chunk (c: memory_chunk) : typ :=
@@ -166,6 +174,9 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
   | Many64 => Tany64
   end.
 
+Lemma type_of_Mptr: type_of_chunk Mptr = Tptr.
+Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.
+
 (** The chunk that is appropriate to store and reload a value of
   the given type, without losing information. *)
 
@@ -179,6 +190,9 @@ Definition chunk_of_type (ty: typ) :=
   | Tany64 => Many64
   end.
 
+Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr.
+Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.
+
 (** Initialization data for global variables. *)
 
 Inductive init_data: Type :=
@@ -189,7 +203,7 @@ Inductive init_data: Type :=
   | Init_float32: float32 -> init_data
   | Init_float64: float -> init_data
   | Init_space: Z -> init_data
-  | Init_addrof: ident -> int -> init_data.  (**r address of symbol + offset *)
+  | Init_addrof: ident -> ptrofs -> init_data.  (**r address of symbol + offset *)
 
 Definition init_data_size (i: init_data) : Z :=
   match i with
@@ -199,7 +213,7 @@ Definition init_data_size (i: init_data) : Z :=
   | Init_int64 _ => 8
   | Init_float32 _ => 4
   | Init_float64 _ => 8
-  | Init_addrof _ _ => 4
+  | Init_addrof _ _ => if Archi.ptr64 then 8 else 4
   | Init_space n => Zmax n 0
   end.
 
@@ -212,7 +226,7 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
 Lemma init_data_size_pos:
   forall i, init_data_size i >= 0.
 Proof.
-  destruct i; simpl; xomega.
+  destruct i; simpl; try xomega. destruct Archi.ptr64; omega.
 Qed.
 
 Lemma init_data_list_size_pos:
@@ -463,11 +477,11 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_external name sg => sg
   | EF_builtin name sg => sg
   | EF_runtime name sg => sg
-  | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default
-  | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default
-  | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default
-  | EF_free => mksignature (Tint :: nil) None cc_default
-  | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default
+  | EF_vload chunk => mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default
+  | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default
+  | EF_malloc => mksignature (Tptr :: nil) (Some Tptr) cc_default
+  | EF_free => mksignature (Tptr :: nil) None cc_default
+  | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) None cc_default
   | EF_annot text targs => mksignature targs None cc_default
   | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default
   | EF_inline_asm text sg clob => sg
@@ -609,10 +623,10 @@ Inductive builtin_arg (A: Type) : Type :=
   | BA_long (n: int64)
   | BA_float (f: float)
   | BA_single (f: float32)
-  | BA_loadstack (chunk: memory_chunk) (ofs: int)
-  | BA_addrstack (ofs: int)
-  | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int)
-  | BA_addrglobal (id: ident) (ofs: int)
+  | BA_loadstack (chunk: memory_chunk) (ofs: ptrofs)
+  | BA_addrstack (ofs: ptrofs)
+  | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
+  | BA_addrglobal (id: ident) (ofs: ptrofs)
   | BA_splitlong (hi lo: builtin_arg A).
 
 Inductive builtin_res (A: Type) : Type :=
diff --git a/common/Determinism.v b/common/Determinism.v
index a813dd92..7fa01c2d 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -42,18 +42,18 @@ Require Import Behaviors.
 
 CoInductive world: Type :=
   World (io: string -> list eventval -> option (eventval * world))
-        (vload: memory_chunk -> ident -> int -> option (eventval * world))
-        (vstore: memory_chunk -> ident -> int -> eventval -> option world).
+        (vload: memory_chunk -> ident -> ptrofs -> option (eventval * world))
+        (vstore: memory_chunk -> ident -> ptrofs -> eventval -> option world).
 
 Definition nextworld_io (w: world) (evname: string) (evargs: list eventval) :
                      option (eventval * world) :=
   match w with World io vl vs => io evname evargs end.
 
-Definition nextworld_vload (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) :
+Definition nextworld_vload (w: world) (chunk: memory_chunk) (id: ident) (ofs: ptrofs) :
                      option (eventval * world) :=
   match w with World io vl vs => vl chunk id ofs end.
 
-Definition nextworld_vstore (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) (v: eventval):
+Definition nextworld_vstore (w: world) (chunk: memory_chunk) (id: ident) (ofs: ptrofs) (v: eventval):
                      option world :=
   match w with World io vl vs => vs chunk id ofs v end.
 
diff --git a/common/Events.v b/common/Events.v
index c94d6d35..97d4f072 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -59,12 +59,12 @@ Inductive eventval: Type :=
   | EVlong: int64 -> eventval
   | EVfloat: float -> eventval
   | EVsingle: float32 -> eventval
-  | EVptr_global: ident -> int -> eventval.
+  | EVptr_global: ident -> ptrofs -> eventval.
 
 Inductive event: Type :=
   | Event_syscall: string -> list eventval -> eventval -> event
-  | Event_vload: memory_chunk -> ident -> int -> eventval -> event
-  | Event_vstore: memory_chunk -> ident -> int -> eventval -> event
+  | Event_vload: memory_chunk -> ident -> ptrofs -> eventval -> event
+  | Event_vstore: memory_chunk -> ident -> ptrofs -> eventval -> event
   | Event_annot: string -> list eventval -> event.
 
 (** The dynamic semantics for programs collect traces of events.
@@ -278,7 +278,7 @@ Inductive eventval_match: eventval -> typ -> val -> Prop :=
   | ev_match_ptr: forall id b ofs,
       Senv.public_symbol ge id = true ->
       Senv.find_symbol ge id = Some b ->
-      eventval_match (EVptr_global id ofs) Tint (Vptr b ofs).
+      eventval_match (EVptr_global id ofs) Tptr (Vptr b ofs).
 
 Inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
   | evl_match_nil:
@@ -295,7 +295,7 @@ Lemma eventval_match_type:
   forall ev ty v,
   eventval_match ev ty v -> Val.has_type v ty.
 Proof.
-  intros. inv H; simpl; auto.
+  intros. inv H; simpl; auto. unfold Tptr; destruct Archi.ptr64; auto.
 Qed.
 
 Lemma eventval_list_match_length:
@@ -359,7 +359,7 @@ Definition eventval_type (ev: eventval) : typ :=
   | EVlong _ => Tlong
   | EVfloat _ => Tfloat
   | EVsingle _ => Tsingle
-  | EVptr_global id ofs => Tint
+  | EVptr_global id ofs => Tptr
   end.
 
 Lemma eventval_match_receptive:
@@ -368,15 +368,23 @@ Lemma eventval_match_receptive:
   eventval_valid ev1 -> eventval_valid ev2 -> eventval_type ev1 = eventval_type ev2 ->
   exists v2, eventval_match ev2 ty v2.
 Proof.
-  intros. inv H; destruct ev2; simpl in H2; try discriminate.
+  intros. unfold eventval_type, Tptr in H2. remember Archi.ptr64 as ptr64.
+  inversion H; subst ev1 ty v1; clear H; destruct ev2; simpl in H2; inv H2.
 - exists (Vint i0); constructor.
 - simpl in H1; exploit Senv.public_symbol_exists; eauto. intros [b FS].
-  exists (Vptr b i1); constructor; auto.
+  exists (Vptr b i1); rewrite H3. constructor; auto.
 - exists (Vlong i0); constructor.
+- simpl in H1; exploit Senv.public_symbol_exists; eauto. intros [b FS].
+  exists (Vptr b i1); rewrite H3; constructor; auto.
 - exists (Vfloat f0); constructor.
+- destruct Archi.ptr64; discriminate.
 - exists (Vsingle f0); constructor; auto.
-- exists (Vint i); constructor.
-- simpl in H1. exploit Senv.public_symbol_exists. eexact H1. intros [b' FS].
+- destruct Archi.ptr64; discriminate.
+- exists (Vint i); unfold Tptr; rewrite H5; constructor.
+- exists (Vlong i); unfold Tptr; rewrite H5; constructor.
+- destruct Archi.ptr64; discriminate.
+- destruct Archi.ptr64; discriminate.
+- exploit Senv.public_symbol_exists. eexact H1. intros [b' FS].
   exists (Vptr b' i0); constructor; auto.
 Qed.
 
@@ -458,7 +466,7 @@ Lemma eventval_match_inject:
 Proof.
   intros. inv H; inv H0; try constructor; auto.
   destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ.
-  rewrite Int.add_zero. constructor; auto. rewrite A; auto.
+  rewrite Ptrofs.add_zero. constructor; auto. rewrite A; auto.
 Qed.
 
 Lemma eventval_match_inject_2:
@@ -469,7 +477,7 @@ Proof.
   intros. inv H; try (econstructor; split; eauto; constructor; fail).
   destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]].
   exists (Vptr b2 ofs); split. econstructor; eauto.
-  econstructor; eauto. rewrite Int.add_zero; auto.
+  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
 Qed.
 
 Lemma eventval_list_match_inject:
@@ -546,7 +554,7 @@ Fixpoint output_trace (t: trace) : Prop :=
 (** * Semantics of volatile memory accesses *)
 
 Inductive volatile_load (ge: Senv.t):
-                   memory_chunk -> mem -> block -> int -> trace -> val -> Prop :=
+                   memory_chunk -> mem -> block -> ptrofs -> trace -> val -> Prop :=
   | volatile_load_vol: forall chunk m b ofs id ev v,
       Senv.block_is_volatile ge b = true ->
       Senv.find_symbol ge id = Some b ->
@@ -556,11 +564,11 @@ Inductive volatile_load (ge: Senv.t):
                       (Val.load_result chunk v)
   | volatile_load_nonvol: forall chunk m b ofs v,
       Senv.block_is_volatile ge b = false ->
-      Mem.load chunk m b (Int.unsigned ofs) = Some v ->
+      Mem.load chunk m b (Ptrofs.unsigned ofs) = Some v ->
       volatile_load ge chunk m b ofs E0 v.
 
 Inductive volatile_store (ge: Senv.t):
-                  memory_chunk -> mem -> block -> int -> val -> trace -> mem -> Prop :=
+                  memory_chunk -> mem -> block -> ptrofs -> val -> trace -> mem -> Prop :=
   | volatile_store_vol: forall chunk m b ofs id ev v,
       Senv.block_is_volatile ge b = true ->
       Senv.find_symbol ge id = Some b ->
@@ -570,7 +578,7 @@ Inductive volatile_store (ge: Senv.t):
                       m
   | volatile_store_nonvol: forall chunk m b ofs v m',
       Senv.block_is_volatile ge b = false ->
-      Mem.store chunk m b (Int.unsigned ofs) v = Some m' ->
+      Mem.store chunk m b (Ptrofs.unsigned ofs) v = Some m' ->
       volatile_store ge chunk m b ofs v E0 m'.
 
 (** * Semantics of external functions *)
@@ -737,7 +745,7 @@ Proof.
 - (* volatile load *)
   inv VI. exploit B; eauto. intros [U V]. subst delta.
   exploit eventval_match_inject_2; eauto. intros (v2 & X & Y).
-  rewrite Int.add_zero. exists (Val.load_result chunk v2); split.
+  rewrite Ptrofs.add_zero. exists (Val.load_result chunk v2); split.
   constructor; auto.
   erewrite D; eauto.
   apply Val.load_result_inject. auto.
@@ -762,7 +770,7 @@ Qed.
 Lemma volatile_load_ok:
   forall chunk,
   extcall_properties (volatile_load_sem chunk)
-                     (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default).
+                     (mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -880,7 +888,7 @@ Proof.
   inv VS.
 - (* volatile store *)
   inv AI. exploit Q; eauto. intros [A B]. subst delta.
-  rewrite Int.add_zero. exists m1'; split.
+  rewrite Ptrofs.add_zero. exists m1'; split.
   constructor; auto. erewrite S; eauto.
   eapply eventval_match_inject; eauto. apply Val.load_result_inject. auto.
   intuition auto with mem.
@@ -894,7 +902,7 @@ Proof.
   unfold loc_unmapped; intros. inv AI; congruence.
 + eapply Mem.store_unchanged_on; eauto.
   unfold loc_out_of_reach; intros. red; intros. simpl in A.
-  assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta)
+  assert (EQ: Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta)) = Ptrofs.unsigned ofs + delta)
   by (eapply Mem.address_inject; eauto with mem).
   rewrite EQ in *.
   eelim H3; eauto.
@@ -913,7 +921,7 @@ Qed.
 Lemma volatile_store_ok:
   forall chunk,
   extcall_properties (volatile_store_sem chunk)
-                     (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default).
+                     (mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -951,19 +959,19 @@ Qed.
 
 Inductive extcall_malloc_sem (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_malloc_sem_intro: forall n m m' b m'',
-      Mem.alloc m (-4) (Int.unsigned n) = (m', b) ->
-      Mem.store Mint32 m' b (-4) (Vint n) = Some m'' ->
-      extcall_malloc_sem ge (Vint n :: nil) m E0 (Vptr b Int.zero) m''.
+  | extcall_malloc_sem_intro: forall sz m m' b m'',
+      Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned sz) = (m', b) ->
+      Mem.store Mptr m' b (- size_chunk Mptr) (Vptrofs sz) = Some m'' ->
+      extcall_malloc_sem ge (Vptrofs sz :: nil) m E0 (Vptr b Ptrofs.zero) m''.
 
 Lemma extcall_malloc_ok:
   extcall_properties extcall_malloc_sem
-                     (mksignature (Tint :: nil) (Some Tint) cc_default).
+                     (mksignature (Tptr :: nil) (Some Tptr) cc_default).
 Proof.
   assert (UNCHANGED:
-    forall (P: block -> Z -> Prop) m n m' b m'',
-    Mem.alloc m (-4) (Int.unsigned n) = (m', b) ->
-    Mem.store Mint32 m' b (-4) (Vint n) = Some m'' ->
+    forall (P: block -> Z -> Prop) m lo hi v m' b m'',
+    Mem.alloc m lo hi = (m', b) ->
+    Mem.store Mptr m' b lo v = Some m'' ->
     Mem.unchanged_on P m m'').
   {
     intros.
@@ -975,7 +983,7 @@ Proof.
   }
   constructor; intros.
 (* well typed *)
-- inv H. unfold proj_sig_res; simpl. auto.
+- inv H. unfold proj_sig_res, Tptr; simpl. destruct Archi.ptr64; auto.
 (* symbols preserved *)
 - inv H0; econstructor; eauto.
 (* valid block *)
@@ -987,23 +995,28 @@ Proof.
 (* readonly *)
 - inv H. eapply UNCHANGED; eauto.
 (* mem extends *)
-- inv H. inv H1. inv H5. inv H7.
+- inv H. inv H1. inv H7.
+  assert (SZ: v2 = Vptrofs sz).
+  { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. } 
+  subst v2.
   exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
   intros [m3' [A B]].
-  exploit Mem.store_within_extends. eexact B. eauto.
-  instantiate (1 := Vint n). auto.
+  exploit Mem.store_within_extends. eexact B. eauto. eauto.
   intros [m2' [C D]].
-  exists (Vptr b Int.zero); exists m2'; intuition.
+  exists (Vptr b Ptrofs.zero); exists m2'; intuition.
   econstructor; eauto.
   eapply UNCHANGED; eauto.
 (* mem injects *)
-- inv H0. inv H2. inv H6. inv H8.
+- inv H0. inv H2. inv H8.
+  assert (SZ: v' = Vptrofs sz).
+  { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. } 
+  subst v'.
   exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl.
   intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]].
   exploit Mem.store_mapped_inject. eexact A. eauto. eauto.
-  instantiate (1 := Vint n). auto.
-  intros [m2' [E G]].
-  exists f'; exists (Vptr b' Int.zero); exists m2'; intuition.
+  instantiate (1 := Vptrofs sz). unfold Vptrofs; destruct Archi.ptr64; constructor.
+  rewrite Zplus_0_r. intros [m2' [E G]].
+  exists f'; exists (Vptr b' Ptrofs.zero); exists m2'; intuition auto.
   econstructor; eauto.
   econstructor. eauto. auto.
   eapply UNCHANGED; eauto.
@@ -1017,7 +1030,14 @@ Proof.
 - assert (t1 = t2). inv H; inv H0; auto. subst t2.
   exists vres1; exists m1; auto.
 (* determ *)
-- inv H; inv H0. split. constructor. intuition congruence.
+- inv H. simple inversion H0.
+  assert (EQ2: sz0 = sz).
+  { unfold Vptrofs in H4; destruct Archi.ptr64 eqn:SF.
+    rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
+    rewrite <- (Ptrofs.of_int_to_int SF sz0), <- (Ptrofs.of_int_to_int SF sz). congruence.
+  }
+  subst. 
+  split. constructor. intuition congruence.
 Qed.
 
 (** ** Semantics of dynamic memory deallocation (free) *)
@@ -1025,14 +1045,14 @@ Qed.
 Inductive extcall_free_sem (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_free_sem_intro: forall b lo sz m m',
-      Mem.load Mint32 m b (Int.unsigned lo - 4) = Some (Vint sz) ->
-      Int.unsigned sz > 0 ->
-      Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) = Some m' ->
+      Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) ->
+      Ptrofs.unsigned sz > 0 ->
+      Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' ->
       extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'.
 
 Lemma extcall_free_ok:
   extcall_properties extcall_free_sem
-                     (mksignature (Tint :: nil) None cc_default).
+                     (mksignature (Tptr :: nil) None cc_default).
 Proof.
   constructor; intros.
 (* well typed *)
@@ -1050,7 +1070,10 @@ Proof.
   eapply Mem.free_range_perm; eauto.
 (* mem extends *)
 - inv H. inv H1. inv H8. inv H6.
-  exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B.
+  exploit Mem.load_extends; eauto. intros [v' [A B]].
+  assert (v' = Vptrofs sz).
+  { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
+  subst v'.
   exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]].
   exists Vundef; exists m2'; intuition.
   econstructor; eauto.
@@ -1062,26 +1085,30 @@ Proof.
   tauto.
 (* mem inject *)
 - inv H0. inv H2. inv H7. inv H9.
-  exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B.
-  assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable).
+  exploit Mem.load_inject; eauto. intros [v' [A B]].
+  assert (v' = Vptrofs sz).
+  { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
+  subst v'.
+  assert (P: Mem.range_perm m1 b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) Cur Freeable).
     eapply Mem.free_range_perm; eauto.
   exploit Mem.address_inject; eauto.
     apply Mem.perm_implies with Freeable; auto with mem.
-    apply H0. instantiate (1 := lo). omega.
+    apply P. instantiate (1 := lo). 
+    generalize (size_chunk_pos Mptr); omega.
   intro EQ.
   exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
   exists f, Vundef, m2'; split.
   apply extcall_free_sem_intro with (sz := sz) (m' := m2').
     rewrite EQ. rewrite <- A. f_equal. omega.
-    auto.
+    auto. auto.
     rewrite ! EQ. rewrite <- C. f_equal; omega.
   split. auto.
   split. auto.
   split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence.
   split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach.
-    intros. red; intros. eelim H7; eauto.
+    intros. red; intros. eelim H2; eauto.
     apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-    apply H0. omega.
+    apply P. omega.
   split. auto.
   red; intros. congruence.
 (* trace length *)
@@ -1090,7 +1117,15 @@ Proof.
 - assert (t1 = t2). inv H; inv H0; auto. subst t2.
   exists vres1; exists m1; auto.
 (* determ *)
-- inv H; inv H0. split. constructor. intuition congruence.
+- inv H; inv H0.
+  assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
+  assert (EQ2: sz0 = sz).
+  { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF.
+    rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
+    rewrite <- (Ptrofs.of_int_to_int SF sz0), <- (Ptrofs.of_int_to_int SF sz). congruence.
+  }
+  subst sz0.
+  split. constructor. intuition congruence.
 Qed.
 
 (** ** Semantics of [memcpy] operations. *)
@@ -1099,19 +1134,19 @@ Inductive extcall_memcpy_sem (sz al: Z) (ge: Senv.t):
                         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 \/ al = 8 -> sz >= 0 -> (al | sz) ->
-      (sz > 0 -> (al | Int.unsigned osrc)) ->
-      (sz > 0 -> (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' ->
+      (sz > 0 -> (al | Ptrofs.unsigned osrc)) ->
+      (sz > 0 -> (al | Ptrofs.unsigned odst)) ->
+      bsrc <> bdst \/ Ptrofs.unsigned osrc = Ptrofs.unsigned odst
+                   \/ Ptrofs.unsigned osrc + sz <= Ptrofs.unsigned odst
+                   \/ Ptrofs.unsigned odst + sz <= Ptrofs.unsigned osrc ->
+      Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz = Some bytes ->
+      Mem.storebytes m bdst (Ptrofs.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 cc_default).
+                     (mksignature (Tptr :: Tptr :: nil) None cc_default).
 Proof.
   intros. constructor.
 - (* return type *)
@@ -1147,9 +1182,9 @@ Proof.
   destruct (zeq sz 0).
 + (* special case sz = 0 *)
   assert (bytes = nil).
-  { exploit (Mem.loadbytes_empty m1 bsrc (Int.unsigned osrc) sz). omega. congruence. }
+  { exploit (Mem.loadbytes_empty m1 bsrc (Ptrofs.unsigned osrc) sz). omega. congruence. }
   subst.
-  destruct (Mem.range_perm_storebytes m1' b0 (Int.unsigned (Int.add odst (Int.repr delta0))) nil)
+  destruct (Mem.range_perm_storebytes m1' b0 (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta0))) nil)
   as [m2' SB].
   simpl. red; intros; omegaContradiction.
   exists f, Vundef, m2'.
@@ -1168,15 +1203,15 @@ Proof.
   red; intros; congruence.
 + (* general case sz > 0 *)
   exploit Mem.loadbytes_length; eauto. intros LEN.
-  assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Cur Nonempty).
+  assert (RPSRC: Mem.range_perm m1 bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sz) Cur 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) Cur Nonempty).
+  assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur 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) Cur Nonempty).
+  assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
     apply RPSRC. omega.
-  assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Cur Nonempty).
+  assert (PDST: Mem.perm m1 bdst (Ptrofs.unsigned odst) Cur Nonempty).
     apply RPDST. omega.
   exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
   exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
@@ -1509,10 +1544,10 @@ Inductive eval_builtin_arg: builtin_arg A -> val -> Prop :=
   | eval_BA_single: forall n,
       eval_builtin_arg (BA_single n) (Vsingle n)
   | eval_BA_loadstack: forall chunk ofs v,
-      Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v ->
+      Mem.loadv chunk m (Val.offset_ptr sp ofs) = Some v ->
       eval_builtin_arg (BA_loadstack chunk ofs) v
   | eval_BA_addrstack: forall ofs,
-      eval_builtin_arg (BA_addrstack ofs) (Val.add sp (Vint ofs))
+      eval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr sp ofs)
   | eval_BA_loadglobal: forall chunk id ofs v,
       Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v ->
       eval_builtin_arg (BA_loadglobal chunk id ofs) v
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 2a8d6d97..9affd634 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -93,17 +93,37 @@ Record t: Type := mksenv {
     forall b, block_is_volatile b = true -> Plt b nextblock
 }.
 
-Definition symbol_address (ge: t) (id: ident) (ofs: int) : val :=
+Definition symbol_address (ge: t) (id: ident) (ofs: ptrofs) : val :=
   match find_symbol ge id with
   | Some b => Vptr b ofs
   | None => Vundef
   end.
 
 Theorem shift_symbol_address:
+  forall ge id ofs delta,
+  symbol_address ge id (Ptrofs.add ofs delta) = Val.offset_ptr (symbol_address ge id ofs) delta.
+Proof.
+  intros. unfold symbol_address, Val.offset_ptr. destruct (find_symbol ge id); auto.
+Qed.
+
+Theorem shift_symbol_address_32:
+  forall ge id ofs n,
+  Archi.ptr64 = false ->
+  symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int n)) = Val.add (symbol_address ge id ofs) (Vint n).
+Proof.
+  intros. unfold symbol_address. destruct (find_symbol ge id).
+- unfold Val.add. rewrite H. auto.
+- auto.
+Qed.
+
+Theorem shift_symbol_address_64:
   forall ge id ofs n,
-  symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).
+  Archi.ptr64 = true ->
+  symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int64 n)) = Val.addl (symbol_address ge id ofs) (Vlong n).
 Proof.
-  intros. unfold symbol_address. destruct (find_symbol ge id); auto.
+  intros. unfold symbol_address. destruct (find_symbol ge id).
+- unfold Val.addl. rewrite H. auto.
+- auto.
 Qed.
 
 Definition equiv (se1 se2: t) : Prop :=
@@ -146,7 +166,7 @@ Definition find_symbol (ge: t) (id: ident) : option block :=
   with [id], at byte offset [ofs].  [Vundef] is returned if no block is associated
   to [id]. *)
 
-Definition symbol_address (ge: t) (id: ident) (ofs: int) : val :=
+Definition symbol_address (ge: t) (id: ident) (ofs: ptrofs) : val :=
   match find_symbol ge id with
   | Some b => Vptr b ofs
   | None => Vundef
@@ -176,7 +196,7 @@ Definition find_funct_ptr (ge: t) (b: block) : option F :=
 
 Definition find_funct (ge: t) (v: val) : option F :=
   match v with
-  | Vptr b ofs => if Int.eq_dec ofs Int.zero then find_funct_ptr ge b else None
+  | Vptr b ofs => if Ptrofs.eq_dec ofs Ptrofs.zero then find_funct_ptr ge b else None
   | _ => None
   end.
 
@@ -341,25 +361,45 @@ Proof.
 Qed.
 
 Theorem shift_symbol_address:
+  forall ge id ofs delta,
+  symbol_address ge id (Ptrofs.add ofs delta) = Val.offset_ptr (symbol_address ge id ofs) delta.
+Proof.
+  intros. unfold symbol_address, Val.offset_ptr. destruct (find_symbol ge id); auto.
+Qed.
+
+Theorem shift_symbol_address_32:
   forall ge id ofs n,
-  symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).
+  Archi.ptr64 = false ->
+  symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int n)) = Val.add (symbol_address ge id ofs) (Vint n).
 Proof.
-  intros. unfold symbol_address. destruct (find_symbol ge id); auto.
+  intros. unfold symbol_address. destruct (find_symbol ge id).
+- unfold Val.add. rewrite H. auto.
+- auto.
+Qed.
+
+Theorem shift_symbol_address_64:
+  forall ge id ofs n,
+  Archi.ptr64 = true ->
+  symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int64 n)) = Val.addl (symbol_address ge id ofs) (Vlong n).
+Proof.
+  intros. unfold symbol_address. destruct (find_symbol ge id).
+- unfold Val.addl. rewrite H. auto.
+- auto.
 Qed.
 
 Theorem find_funct_inv:
   forall ge v f,
-  find_funct ge v = Some f -> exists b, v = Vptr b Int.zero.
+  find_funct ge v = Some f -> exists b, v = Vptr b Ptrofs.zero.
 Proof.
   intros until f; unfold find_funct.
   destruct v; try congruence.
-  destruct (Int.eq_dec i Int.zero); try congruence.
+  destruct (Ptrofs.eq_dec i Ptrofs.zero); try congruence.
   intros. exists b; congruence.
 Qed.
 
 Theorem find_funct_find_funct_ptr:
   forall ge b,
-  find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b.
+  find_funct ge (Vptr b Ptrofs.zero) = find_funct_ptr ge b.
 Proof.
   intros; simpl. apply dec_eq_true.
 Qed.
@@ -594,7 +634,7 @@ Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option m
   | Init_addrof symb ofs =>
       match find_symbol ge symb with
       | None => None
-      | Some b' => Mem.store Mint32 m b p (Vptr b' ofs)
+      | Some b' => Mem.store Mptr m b p (Vptr b' ofs)
       end
   | Init_space n => Some m
   end.
@@ -824,7 +864,8 @@ Proof.
   try (eapply Mem.store_unchanged_on; eauto; fail).
   inv H; apply Mem.unchanged_on_refl.
   destruct (find_symbol ge i); try congruence.
-  eapply Mem.store_unchanged_on; eauto. 
+  eapply Mem.store_unchanged_on; eauto;
+  unfold Mptr; destruct Archi.ptr64; eauto.
 Qed.
 
 Remark store_init_data_list_unchanged:
@@ -886,11 +927,17 @@ Definition bytes_of_init_data (i: init_data): list memval :=
   | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero)
   | Init_addrof id ofs =>
       match find_symbol ge id with
-      | Some b => inj_value Q32 (Vptr b ofs)
-      | None   => list_repeat 4%nat Undef
+      | Some b => inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs)
+      | None   => list_repeat (if Archi.ptr64 then 8%nat else 4%nat) Undef
       end
   end.
 
+Remark init_data_size_addrof:
+  forall id ofs, init_data_size (Init_addrof id ofs) = size_chunk Mptr.
+Proof.
+  intros. unfold Mptr. simpl. destruct Archi.ptr64; auto.
+Qed.
+
 Lemma store_init_data_loadbytes:
   forall m b p i m',
   store_init_data m b p i = Some m' ->
@@ -902,8 +949,10 @@ Proof.
   assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0).
   { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } 
   rewrite <- EQ. apply H0. omega. simpl. omega. 
-- simpl; destruct (find_symbol ge i) as [b'|]; try discriminate.
-  apply (Mem.loadbytes_store_same _ _ _ _ _ _ H).
+- rewrite init_data_size_addrof. simpl.
+  destruct (find_symbol ge i) as [b'|]; try discriminate.
+  rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H).
+  unfold encode_val, Mptr; destruct Archi.ptr64; reflexivity.
 Qed.
 
 Fixpoint bytes_of_init_data_list (il: list init_data): list memval :=
@@ -999,8 +1048,8 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s
       Mem.load Mfloat64 m b p = Some(Vfloat n)
       /\ load_store_init_data m b (p + 8) il'
   | Init_addrof symb ofs :: il' =>
-      (exists b', find_symbol ge symb = Some b' /\ Mem.load Mint32 m b p = Some(Vptr b' ofs))
-      /\ load_store_init_data m b (p + 4) il'
+      (exists b', find_symbol ge symb = Some b' /\ Mem.load Mptr m b p = Some(Vptr b' ofs))
+      /\ load_store_init_data m b (p + size_chunk Mptr) il'
   | Init_space n :: il' =>
       read_as_zero m b p n
       /\ load_store_init_data m b (p + Zmax n 0) il'
@@ -1024,8 +1073,8 @@ Proof.
     eapply Mem.load_store_same; eauto.
   }
   induction il; simpl.
-  auto.
-  intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
+- auto.
+- intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
   exploit IHil; eauto.
   set (P := fun (b': block) ofs' => p + init_data_size a <= ofs').
   apply read_as_zero_unchanged with (m := m) (P := P).
@@ -1034,21 +1083,27 @@ Proof.
   intros; unfold P. omega.
   intros; unfold P. omega.
   intro D.
-  destruct a; simpl in Heqo; intuition.
-  eapply (A Mint8unsigned (Vint i)); eauto.
-  eapply (A Mint16unsigned (Vint i)); eauto.
-  eapply (A Mint32 (Vint i)); eauto.
-  eapply (A Mint64 (Vlong i)); eauto.
-  eapply (A Mfloat32 (Vsingle f)); eauto.
-  eapply (A Mfloat64 (Vfloat f)); eauto.
+  destruct a; simpl in Heqo.
++ split; auto. eapply (A Mint8unsigned (Vint i)); eauto.
++ split; auto. eapply (A Mint16unsigned (Vint i)); eauto.
++ split; auto. eapply (A Mint32 (Vint i)); eauto.
++ split; auto. eapply (A Mint64 (Vlong i)); eauto.
++ split; auto. eapply (A Mfloat32 (Vsingle f)); eauto.
++ split; auto. eapply (A Mfloat64 (Vfloat f)); eauto.
++ split; auto.
   set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)).
   inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P).
   red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega.
   eapply store_init_data_list_unchanged; eauto. 
   intros; unfold P. omega.
   intros; unfold P. simpl; xomega.
-  destruct (find_symbol ge i); try congruence. exists b0; split; auto.
-  eapply (A Mint32 (Vptr b0 i0)); eauto.
++ rewrite init_data_size_addrof in *.
+  split; auto.
+  destruct (find_symbol ge i); try congruence.
+  exists b0; split; auto.
+  transitivity (Some (Val.load_result Mptr (Vptr b0 i0))).
+  eapply (A Mptr (Vptr b0 i0)); eauto.
+  unfold Val.load_result, Mptr; destruct Archi.ptr64; auto.
 Qed.
 
 Remark alloc_global_unchanged:
@@ -1324,7 +1379,7 @@ Proof.
   destruct (find_symbol ge i) as [b'|] eqn:E; try discriminate.
   eapply Mem.store_inject_neutral; eauto.
   econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto. eauto.
-  rewrite Int.add_zero. auto.
+  rewrite Ptrofs.add_zero. auto.
 Qed.
 
 Lemma store_init_data_list_neutral:
@@ -1417,7 +1472,7 @@ Definition init_data_alignment (i: init_data) : Z :=
   | Init_int64 n => 8
   | Init_float32 n => 4
   | Init_float64 n => 4
-  | Init_addrof symb ofs => 4
+  | Init_addrof symb ofs => if Archi.ptr64 then 8 else 4
   | Init_space n => 1
   end.
 
@@ -1444,7 +1499,8 @@ Proof.
   { intros. apply Mem.store_valid_access_3 in H0. destruct H0. congruence. }
   destruct i; simpl in H; eauto.
   simpl. apply Z.divide_1_l.
-  destruct (find_symbol ge i); try discriminate. eauto.
+  destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption. 
+  unfold Mptr, init_data_alignment; destruct Archi.ptr64; auto.
 Qed.
 
 Lemma store_init_data_list_aligned:
@@ -1531,7 +1587,9 @@ Proof.
     exists m'; auto. }
   destruct i; eauto.
   simpl. exists m; auto.
-  simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eauto. 
+  simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL. 
+  unfold init_data_size, Mptr. destruct Archi.ptr64; auto.
+  unfold init_data_alignment, Mptr. destruct Archi.ptr64; auto.
 Qed.
 
 Lemma store_init_data_list_exists:
diff --git a/common/Memdata.v b/common/Memdata.v
index 4ef7836b..87547e1e 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -68,6 +68,11 @@ Proof.
   intros; exists n; auto.
 Qed.
 
+Lemma size_chunk_Mptr: size_chunk Mptr = if Archi.ptr64 then 8 else 4.
+Proof.
+  unfold Mptr; destruct Archi.ptr64; auto.
+Qed.
+
 (** Memory reads and writes must respect alignment constraints:
   the byte offset of the location being addressed should be an exact
   multiple of the natural alignment for the chunk being addressed.
@@ -98,6 +103,11 @@ Proof.
   intro. destruct chunk; simpl; omega.
 Qed.
 
+Lemma align_chunk_Mptr: align_chunk Mptr = if Archi.ptr64 then 8 else 4.
+Proof.
+  unfold Mptr; destruct Archi.ptr64; auto.
+Qed.
+
 Lemma align_size_chunk_divides:
   forall chunk, (align_chunk chunk | size_chunk chunk).
 Proof.
@@ -360,8 +370,9 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
   | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n))
   | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n))
   | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n))
-  | Vptr b ofs, Mint32 => inj_value Q32 v
+  | Vptr b ofs, Mint32 => if Archi.ptr64 then list_repeat 4%nat Undef else inj_value Q32 v
   | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n))
+  | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else list_repeat 8%nat Undef
   | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
   | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
   | _, Many32 => inj_value Q32 v
@@ -386,19 +397,26 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
       end
   | None =>
       match chunk with
-      | Mint32 | Many32 => Val.load_result chunk (proj_value Q32 vl)
+      | Mint32 => if Archi.ptr64 then Vundef else Val.load_result chunk (proj_value Q32 vl)
+      | Many32 => Val.load_result chunk (proj_value Q32 vl)
+      | Mint64 => if Archi.ptr64 then Val.load_result chunk (proj_value Q64 vl) else Vundef
       | Many64 => Val.load_result chunk (proj_value Q64 vl)
       | _ => Vundef
       end
   end.
 
+Ltac solve_encode_val_length :=
+  match goal with
+  | [ |- length (inj_bytes _) = _ ] => rewrite length_inj_bytes; solve_encode_val_length
+  | [ |- length (encode_int _ _) = _ ] => apply encode_int_length
+  | [ |- length (if ?x then _ else _) = _ ] => destruct x eqn:?; solve_encode_val_length
+  | _ => reflexivity
+  end.
+
 Lemma encode_val_length:
   forall chunk v, length(encode_val chunk v) = size_chunk_nat chunk.
 Proof.
-  intros. destruct v; simpl; destruct chunk;
-  solve [ reflexivity
-        | apply length_list_repeat
-        | rewrite length_inj_bytes; apply encode_int_length ].
+  intros. destruct v; simpl; destruct chunk; solve_encode_val_length.
 Qed.
 
 Lemma check_inj_value:
@@ -447,13 +465,15 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) :
   | Vint n, Mint16signed, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
   | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
   | Vint n, Mint32, Mint32 => v2 = Vint n
-  | Vint n, Many32, (Mint32 | Many32) => v2 = Vint n
+  | Vint n, Many32, Many32 => v2 = Vint n
   | Vint n, Mint32, Mfloat32 => v2 = Vsingle(Float32.of_bits n)
   | Vint n, Many64, Many64 => v2 = Vint n
   | Vint n, (Mint64 | Mfloat32 | Mfloat64 | Many64), _ => v2 = Vundef
   | Vint n, _, _ => True (**r nothing meaningful to say about v2 *)
-  | Vptr b ofs, (Mint32 | Many32), (Mint32 | Many32) => v2 = Vptr b ofs
+  | Vptr b ofs, (Mint32 | Many32), (Mint32 | Many32) => v2 = if Archi.ptr64 then Vundef else Vptr b ofs
+  | Vptr b ofs, Mint64, (Mint64 | Many64) => v2 = if Archi.ptr64 then Vptr b ofs else Vundef
   | Vptr b ofs, Many64, Many64 => v2 = Vptr b ofs
+  | Vptr b ofs, Many64, Mint64 => v2 = if Archi.ptr64 then Vptr b ofs else Vundef
   | Vptr b ofs, _, _ => v2 = Vundef
   | Vlong n, Mint64, Mint64 => v2 = Vlong n
   | Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.of_bits n)
@@ -476,7 +496,7 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) :
 Remark decode_val_undef:
   forall bl chunk, decode_val chunk (Undef :: bl) = Vundef.
 Proof.
-  intros. unfold decode_val. simpl. destruct chunk; auto.
+  intros. unfold decode_val. simpl. destruct chunk, Archi.ptr64; auto.
 Qed.
 
 Remark proj_bytes_inj_value:
@@ -485,33 +505,33 @@ Proof.
   intros. destruct q; reflexivity.
 Qed.
 
+Ltac solve_decode_encode_val_general :=
+  exact I || reflexivity ||
+  match goal with
+  | |- context [ if Archi.ptr64 then _ else _ ] => destruct Archi.ptr64 eqn:?
+  | |- context [ proj_bytes (inj_bytes _) ] => rewrite proj_inj_bytes
+  | |- context [ proj_bytes (inj_value _ _) ] => rewrite proj_bytes_inj_value
+  | |- context [ proj_value _ (inj_value _ _) ] => rewrite ?proj_inj_value, ?proj_inj_value_mismatch by congruence
+  | |- context [ Int.repr(decode_int (encode_int 1 (Int.unsigned _))) ] => rewrite decode_encode_int_1
+  | |- context [ Int.repr(decode_int (encode_int 2 (Int.unsigned _))) ] => rewrite decode_encode_int_2
+  | |- context [ Int.repr(decode_int (encode_int 4 (Int.unsigned _))) ] => rewrite decode_encode_int_4
+  | |- context [ Int64.repr(decode_int (encode_int 8 (Int64.unsigned _))) ] => rewrite decode_encode_int_8
+  | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; omega
+  | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; omega
+  | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; omega
+  end.
+
 Lemma decode_encode_val_general:
   forall v chunk1 chunk2,
   decode_encode_val v chunk1 chunk2 (decode_val chunk2 (encode_val chunk1 v)).
 Proof.
 Opaque inj_value.
   intros.
-  destruct v; destruct chunk1 eqn:C1; simpl; try (apply decode_val_undef);
-  destruct chunk2 eqn:C2; unfold decode_val; auto;
-  try (rewrite proj_inj_bytes); try (rewrite proj_bytes_inj_value);
-  try (rewrite proj_inj_value); try (rewrite proj_inj_value_mismatch by congruence);
-  auto.
-  rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega.
-  rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega.
-  rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega.
-  rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega.
-  rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. omega.
-  rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega.
-  rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. omega.
-  rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega.
-  rewrite decode_encode_int_4. auto.
-  rewrite decode_encode_int_4. auto.
-  rewrite decode_encode_int_8. auto.
-  rewrite decode_encode_int_8. auto.
-  rewrite decode_encode_int_8. auto.
-  rewrite decode_encode_int_8. decEq. apply Float.of_to_bits.
-  rewrite decode_encode_int_4. auto.
-  rewrite decode_encode_int_4. decEq. apply Float32.of_to_bits.
+  destruct v; destruct chunk1 eqn:C1; try (apply decode_val_undef);
+  destruct chunk2 eqn:C2; unfold decode_encode_val, decode_val, encode_val, Val.load_result;
+  repeat solve_decode_encode_val_general.
+- rewrite Float.of_to_bits; auto.
+- rewrite Float32.of_to_bits; auto.
 Qed.
 
 Lemma decode_encode_val_similar:
@@ -533,7 +553,9 @@ Proof.
   intros. unfold decode_val.
   destruct (proj_bytes cl).
   destruct chunk; simpl; auto.
-  destruct chunk; exact I || apply Val.load_result_type.
+Local Opaque Val.load_result.
+  destruct chunk; simpl;
+  (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)).
 Qed.
 
 Lemma encode_val_int8_signed_unsigned:
@@ -601,7 +623,7 @@ Definition quantity_chunk (chunk: memory_chunk) :=
 
 Inductive shape_encoding (chunk: memory_chunk) (v: val): list memval -> Prop :=
   | shape_encoding_f: forall q i mvl,
-      (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
+      (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) ->
       q = quantity_chunk chunk ->
       S i = size_quantity_nat q ->
       (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) ->
@@ -628,7 +650,7 @@ Proof.
   }
   assert (B: forall q,
              q = quantity_chunk chunk ->
-             (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
+             (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) ->
              shape_encoding chunk v (inj_value q v)).
   {
 Local Transparent inj_value.
@@ -651,12 +673,15 @@ Local Transparent inj_value.
     intros. eapply in_list_repeat; eauto.
   }
   generalize (encode_val_length chunk v). intros LEN.
-  unfold encode_val; unfold encode_val in LEN; destruct v; destruct chunk; (apply B || apply C || apply D); auto; red; auto.
+  unfold encode_val; unfold encode_val in LEN;
+  destruct v; destruct chunk;
+  (apply B || apply C || apply D || (destruct Archi.ptr64; (apply B || apply D)));
+  auto.
 Qed.
 
 Inductive shape_decoding (chunk: memory_chunk): list memval -> val -> Prop :=
   | shape_decoding_f: forall v q i mvl,
-      (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
+      (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) ->
       q = quantity_chunk chunk ->
       S i = size_quantity_nat q ->
       (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) ->
@@ -696,7 +721,7 @@ Proof.
     destruct chunk; auto.
   }
   assert (C: forall q, size_quantity_nat q = size_chunk_nat chunk ->
-             (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
+             (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) ->
              shape_decoding chunk (mv1 :: mvl) (Val.load_result chunk (proj_value q (mv1 :: mvl)))).
   {
     intros. unfold proj_value. destruct mv1; auto.
@@ -706,7 +731,7 @@ Proof.
     destruct (beq_nat sz n) eqn:EQN; auto.
     destruct (check_value sz v q mvl) eqn:CHECK; auto.
     simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto.
-    destruct H0 as [E|[E|E]]; subst chunk; destruct q; auto || discriminate.
+    destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate.
     congruence.
     intros. eapply B; eauto. omega.
   }
@@ -714,7 +739,7 @@ Proof.
   destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB.
   exploit (A mv1); eauto with coqlib. intros [b1 EQ1]; subst mv1.
   destruct chunk; (apply shape_decoding_u || apply shape_decoding_b); eauto with coqlib.
-  destruct chunk; (apply shape_decoding_u || apply C); auto.
+  destruct chunk, Archi.ptr64; (apply shape_decoding_u || apply C); auto.
 Qed.
 
 (** * Compatibility with memory injections *)
@@ -835,7 +860,7 @@ Proof.
     rewrite proj_value_undef. destruct chunk; auto. eapply proj_bytes_not_inject; eauto. congruence.
     apply Val.load_result_inject. apply proj_value_inject; auto.
   }
-  destruct chunk; auto.
+  destruct chunk; destruct Archi.ptr64; auto.
 Qed.
 
 (** Symmetrically, [encode_val], applied to values related by [Val.inject],
@@ -883,10 +908,13 @@ Theorem encode_val_inject:
   Val.inject f v1 v2 ->
   list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2).
 Proof.
+Local Opaque list_repeat.
   intros. inversion H; subst; simpl; destruct chunk;
   auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val.
-  unfold encode_val. destruct v2; apply inj_value_inject; auto.
-  unfold encode_val. destruct v2; apply inj_value_inject; auto.
+- destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self.
+- destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self.
+- unfold encode_val. destruct v2; apply inj_value_inject; auto.
+- unfold encode_val. destruct v2; apply inj_value_inject; auto.
 Qed.
 
 Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id.
@@ -964,20 +992,20 @@ Qed.
 
 Lemma decode_val_int64:
   forall l1 l2,
-  length l1 = 4%nat -> length l2 = 4%nat ->
+  length l1 = 4%nat -> length l2 = 4%nat -> Archi.ptr64 = false ->
   Val.lessdef
     (decode_val Mint64 (l1 ++ l2))
     (Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2))
                      (decode_val Mint32 (if Archi.big_endian then l2 else l1))).
 Proof.
-  intros. unfold decode_val.
+  intros. unfold decode_val. rewrite H1.
   rewrite proj_bytes_append.
   destruct (proj_bytes l1) as [b1|] eqn:B1; destruct (proj_bytes l2) as [b2|] eqn:B2; auto.
   exploit length_proj_bytes. eexact B1. rewrite H; intro L1.
   exploit length_proj_bytes. eexact B2. rewrite H0; intro L2.
   assert (UR: forall l, length l = 4%nat -> Int.unsigned (Int.repr (int_of_bytes l)) = int_of_bytes l).
     intros. apply Int.unsigned_repr.
-    generalize (int_of_bytes_range l). rewrite H1.
+    generalize (int_of_bytes_range l). rewrite H2.
     change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1).
     omega.
   apply Val.lessdef_same.
@@ -1029,11 +1057,13 @@ Qed.
 
 Lemma encode_val_int64:
   forall v,
+  Archi.ptr64 = false ->
   encode_val Mint64 v =
      encode_val Mint32 (if Archi.big_endian then Val.hiword v else Val.loword v)
   ++ encode_val Mint32 (if Archi.big_endian then Val.loword v else Val.hiword v).
 Proof.
-  intros. destruct v; destruct Archi.big_endian eqn:BI; try reflexivity;
+  intros. unfold encode_val. rewrite H. 
+  destruct v; destruct Archi.big_endian eqn:BI; try reflexivity;
   unfold Val.loword, Val.hiword, encode_val.
   unfold inj_bytes. rewrite <- map_app. f_equal.
   unfold encode_int, rev_if_be. rewrite BI. rewrite <- rev_app_distr. f_equal.
diff --git a/common/Memory.v b/common/Memory.v
index 672012be..d0cbe8a0 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -450,7 +450,7 @@ Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val :
 
 Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
   match addr with
-  | Vptr b ofs => load chunk m b (Int.unsigned ofs)
+  | Vptr b ofs => load chunk m b (Ptrofs.unsigned ofs)
   | _ => None
   end.
 
@@ -566,7 +566,7 @@ Qed.
 
 Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   match addr with
-  | Vptr b ofs => store chunk m b (Int.unsigned ofs) v
+  | Vptr b ofs => store chunk m b (Ptrofs.unsigned ofs) v
   | _ => None
   end.
 
@@ -873,7 +873,7 @@ Qed.
 
 Theorem load_int64_split:
   forall m b ofs v,
-  load Mint64 m b ofs = Some v ->
+  load Mint64 m b ofs = Some v -> Archi.ptr64 = false ->
   exists v1 v2,
      load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2)
   /\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1)
@@ -897,29 +897,47 @@ Proof.
   exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)).
   split. destruct Archi.big_endian; auto.
   split. destruct Archi.big_endian; auto.
-  rewrite EQ. rewrite APP. apply decode_val_int64.
+  rewrite EQ. rewrite APP. apply decode_val_int64; auto.
   erewrite loadbytes_length; eauto. reflexivity.
   erewrite loadbytes_length; eauto. reflexivity.
 Qed.
 
+Lemma addressing_int64_split:
+  forall i,
+  Archi.ptr64 = false ->
+  (8 | Ptrofs.unsigned i) ->
+  Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4.
+Proof.
+  intros.
+  rewrite Ptrofs.add_unsigned.
+  replace (Ptrofs.unsigned (Ptrofs.of_int (Int.repr 4))) with (Int.unsigned (Int.repr 4))
+    by (symmetry; apply Ptrofs.agree32_of_int; auto).
+  change (Int.unsigned (Int.repr 4)) with 4. 
+  apply Ptrofs.unsigned_repr.
+  exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8).
+  omega. apply Ptrofs.unsigned_range. auto.
+  exists (two_p (Ptrofs.zwordsize - 3)).
+  unfold Ptrofs.modulus, Ptrofs.zwordsize, Ptrofs.wordsize.
+  unfold Wordsize_Ptrofs.wordsize. destruct Archi.ptr64; reflexivity.
+  unfold Ptrofs.max_unsigned. omega.
+Qed.
+
 Theorem loadv_int64_split:
   forall m a v,
-  loadv Mint64 m a = Some v ->
+  loadv Mint64 m a = Some v -> Archi.ptr64 = false ->
   exists v1 v2,
      loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2)
-  /\ loadv  Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1)
+  /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1)
   /\ Val.lessdef v (Val.longofwords v1 v2).
 Proof.
-  intros. destruct a; simpl in H; try discriminate.
+  intros. destruct a; simpl in H; inv H.
   exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ).
-  assert (NV: Int.unsigned (Int.add i (Int.repr 4)) = Int.unsigned i + 4).
-    rewrite Int.add_unsigned. apply Int.unsigned_repr.
-    exploit load_valid_access. eexact H. intros [P Q]. simpl in Q.
-    exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8).
-    omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity.
-    unfold Int.max_unsigned. omega.
-  exists v1; exists v2.
-Opaque Int.repr.
+  unfold Val.add; rewrite H0.
+  assert (NV: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4).
+  { apply addressing_int64_split; auto. 
+    exploit load_valid_access. eexact H2. intros [P Q]. auto. }
+  exists v1, v2.
+Opaque Ptrofs.repr.
   split. auto.
   split. simpl. rewrite NV. auto.
   auto.
@@ -1205,18 +1223,18 @@ Qed.
 Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop :=
   match chunk1, chunk2 with
   | (Mint32 | Many32), (Mint32 | Many32) => True
-  | Many64, Many64 => True
+  | (Mint64 | Many64), (Mint64 | Many64) => True
   | _, _ => False
   end.
 
 Lemma compat_pointer_chunks_true:
   forall chunk1 chunk2,
-  (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Many64) ->
-  (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Many64) ->
+  (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Mint64 \/ chunk1 = Many64) ->
+  (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Mint64 \/ chunk2 = Many64) ->
   quantity_chunk chunk1 = quantity_chunk chunk2 ->
   compat_pointer_chunks chunk1 chunk2.
 Proof.
-  intros. destruct H as [P|[P|P]]; destruct H0 as [Q|[Q|Q]];
+  intros. destruct H as [P|[P|[P|P]]]; destruct H0 as [Q|[Q|[Q|Q]]];
   subst; red; auto; discriminate.
 Qed.
 
@@ -1237,10 +1255,11 @@ Proof.
   destruct CASES as [(A & B) | [(A & B) | (A & B)]].
 - (* Same offset *)
   subst. inv ENC.
-  assert (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64)
+  assert (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64)
   by (destruct chunk; auto || contradiction).
   left; split. rewrite H3.
-  destruct H4 as [P|[P|P]]; subst chunk'; destruct v0; simpl in H3; congruence.
+  destruct H4 as [P|[P|[P|P]]]; subst chunk'; destruct v0; simpl in H3;
+  try congruence; destruct Archi.ptr64; congruence.
   split. apply compat_pointer_chunks_true; auto.
   auto.
 - (* ofs' > ofs *)
@@ -1612,7 +1631,7 @@ Qed.
 
 Theorem store_int64_split:
   forall m b ofs v m',
-  store Mint64 m b ofs v = Some m' ->
+  store Mint64 m b ofs v = Some m' -> Archi.ptr64 = false ->
   exists m1,
      store Mint32 m b ofs (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1
   /\ store Mint32 m1 b (ofs + 4) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'.
@@ -1620,7 +1639,7 @@ Proof.
   intros.
   exploit store_valid_access_3; eauto. intros [A B]. simpl in *.
   exploit store_storebytes. eexact H. intros SB.
-  rewrite encode_val_int64 in SB.
+  rewrite encode_val_int64 in SB by auto.
   exploit storebytes_split. eexact SB. intros [m1 [SB1 SB2]].
   rewrite encode_val_length in SB2. simpl in SB2.
   exists m1; split.
@@ -1632,20 +1651,18 @@ Qed.
 
 Theorem storev_int64_split:
   forall m a v m',
-  storev Mint64 m a v = Some m' ->
+  storev Mint64 m a v = Some m' -> Archi.ptr64 = false ->
   exists m1,
      storev Mint32 m a (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1
   /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'.
 Proof.
-  intros. destruct a; simpl in H; try discriminate.
+  intros. destruct a; simpl in H; inv H. rewrite H2.
   exploit store_int64_split; eauto. intros [m1 [A B]].
   exists m1; split.
   exact A.
-  unfold storev, Val.add. rewrite Int.add_unsigned. rewrite Int.unsigned_repr. exact B.
-  exploit store_valid_access_3. eexact H. intros [P Q]. simpl in Q.
-  exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8).
-    omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity.
-  change (Int.unsigned (Int.repr 4)) with 4. unfold Int.max_unsigned. omega.
+  unfold storev, Val.add. rewrite H0.
+  rewrite addressing_int64_split; auto.
+  exploit store_valid_access_3. eexact H2. intros [P Q]. exact Q.
 Qed.
 
 (** ** Properties related to [alloc]. *)
@@ -1811,7 +1828,8 @@ Theorem load_alloc_same:
 Proof.
   intros. exploit load_result; eauto. intro. rewrite H0.
   injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1.
-  rewrite PMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity.
+  rewrite PMap.gss. destruct (size_chunk_nat_pos chunk) as [n E]. rewrite E. simpl.
+  rewrite ZMap.gi. apply decode_val_undef. 
 Qed.
 
 Theorem load_alloc_same':
@@ -3142,8 +3160,8 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop :=
     mi_representable:
       forall b b' delta ofs,
       f b = Some(b', delta) ->
-      perm m1 b (Int.unsigned ofs) Max Nonempty \/ perm m1 b (Int.unsigned ofs - 1) Max Nonempty ->
-      delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned;
+      perm m1 b (Ptrofs.unsigned ofs) Max Nonempty \/ perm m1 b (Ptrofs.unsigned ofs - 1) Max Nonempty ->
+      delta >= 0 /\ 0 <= Ptrofs.unsigned ofs + delta <= Ptrofs.max_unsigned;
     mi_perm_inv:
       forall b1 ofs b2 delta k p,
       f b1 = Some(b2, delta) ->
@@ -3246,24 +3264,24 @@ Qed.
 Lemma address_inject:
   forall f m1 m2 b1 ofs1 b2 delta p,
   inject f m1 m2 ->
-  perm m1 b1 (Int.unsigned ofs1) Cur p ->
+  perm m1 b1 (Ptrofs.unsigned ofs1) Cur p ->
   f b1 = Some (b2, delta) ->
-  Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.
 Proof.
   intros.
-  assert (perm m1 b1 (Int.unsigned ofs1) Max Nonempty) by eauto with mem.
+  assert (perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty) by eauto with mem.
   exploit mi_representable; eauto. intros [A B].
-  assert (0 <= delta <= Int.max_unsigned).
-    generalize (Int.unsigned_range ofs1). omega.
-  unfold Int.add. repeat rewrite Int.unsigned_repr; omega.
+  assert (0 <= delta <= Ptrofs.max_unsigned).
+    generalize (Ptrofs.unsigned_range ofs1). omega.
+  unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; omega.
 Qed.
 
 Lemma address_inject':
   forall f m1 m2 chunk b1 ofs1 b2 delta,
   inject f m1 m2 ->
-  valid_access m1 chunk b1 (Int.unsigned ofs1) Nonempty ->
+  valid_access m1 chunk b1 (Ptrofs.unsigned ofs1) Nonempty ->
   f b1 = Some (b2, delta) ->
-  Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.
 Proof.
   intros. destruct H0. eapply address_inject; eauto.
   apply H0. generalize (size_chunk_pos chunk). omega.
@@ -3272,24 +3290,24 @@ Qed.
 Theorem weak_valid_pointer_inject_no_overflow:
   forall f m1 m2 b ofs b' delta,
   inject f m1 m2 ->
-  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
   f b = Some(b', delta) ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 Proof.
   intros. rewrite weak_valid_pointer_spec in H0.
   rewrite ! valid_pointer_nonempty_perm in H0.
   exploit mi_representable; eauto. destruct H0; eauto with mem.
   intros [A B].
-  pose proof (Int.unsigned_range ofs).
-  rewrite Int.unsigned_repr; omega.
+  pose proof (Ptrofs.unsigned_range ofs).
+  rewrite Ptrofs.unsigned_repr; omega.
 Qed.
 
 Theorem valid_pointer_inject_no_overflow:
   forall f m1 m2 b ofs b' delta,
   inject f m1 m2 ->
-  valid_pointer m1 b (Int.unsigned ofs) = true ->
+  valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
   f b = Some(b', delta) ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 Proof.
   eauto using weak_valid_pointer_inject_no_overflow, valid_pointer_implies.
 Qed.
@@ -3297,9 +3315,9 @@ Qed.
 Theorem valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
-  valid_pointer m1 b (Int.unsigned ofs) = true ->
+  valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
   Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
-  valid_pointer m2 b' (Int.unsigned ofs') = true.
+  valid_pointer m2 b' (Ptrofs.unsigned ofs') = true.
 Proof.
   intros. inv H1.
   erewrite address_inject'; eauto.
@@ -3310,9 +3328,9 @@ Qed.
 Theorem weak_valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
-  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
   Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
-  weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
+  weak_valid_pointer m2 b' (Ptrofs.unsigned ofs') = true.
 Proof.
   intros. inv H1.
   exploit weak_valid_pointer_inject; eauto. intros W.
@@ -3320,8 +3338,8 @@ Proof.
   rewrite ! valid_pointer_nonempty_perm in H0.
   exploit mi_representable; eauto. destruct H0; eauto with mem.
   intros [A B].
-  pose proof (Int.unsigned_range ofs).
-  unfold Int.add. repeat rewrite Int.unsigned_repr; auto; omega.
+  pose proof (Ptrofs.unsigned_range ofs).
+  unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; omega.
 Qed.
 
 Theorem inject_no_overlap:
@@ -3341,13 +3359,13 @@ Theorem different_pointers_inject:
   forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
   inject f m m' ->
   b1 <> b2 ->
-  valid_pointer m b1 (Int.unsigned ofs1) = true ->
-  valid_pointer m b2 (Int.unsigned ofs2) = true ->
+  valid_pointer m b1 (Ptrofs.unsigned ofs1) = true ->
+  valid_pointer m b2 (Ptrofs.unsigned ofs2) = true ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
   b1' <> b2' \/
-  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <>
-  Int.unsigned (Int.add ofs2 (Int.repr delta2)).
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <>
+  Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).
 Proof.
   intros.
   rewrite valid_pointer_valid_access in H1.
@@ -3356,8 +3374,8 @@ Proof.
   rewrite (address_inject' _ _ _ _ _ _ _ _ H H2 H4).
   inv H1. simpl in H5. inv H2. simpl in H1.
   eapply mi_no_overlap; eauto.
-  apply perm_cur_max. apply (H5 (Int.unsigned ofs1)). omega.
-  apply perm_cur_max. apply (H1 (Int.unsigned ofs2)). omega.
+  apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). omega.
+  apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). omega.
 Qed.
 
 Require Intv.
@@ -3439,8 +3457,8 @@ Proof.
   intros. inv H1; simpl in H0; try discriminate.
   exploit load_inject; eauto. intros [v2 [LOAD INJ]].
   exists v2; split; auto. unfold loadv.
-  replace (Int.unsigned (Int.add ofs1 (Int.repr delta)))
-     with (Int.unsigned ofs1 + delta).
+  replace (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))
+     with (Ptrofs.unsigned ofs1 + delta).
   auto. symmetry. eapply address_inject'; eauto with mem.
 Qed.
 
@@ -3547,8 +3565,8 @@ Theorem storev_mapped_inject:
 Proof.
   intros. inv H1; simpl in H0; try discriminate.
   unfold storev.
-  replace (Int.unsigned (Int.add ofs1 (Int.repr delta)))
-    with (Int.unsigned ofs1 + delta).
+  replace (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))
+    with (Ptrofs.unsigned ofs1 + delta).
   eapply store_mapped_inject; eauto.
   symmetry. eapply address_inject'; eauto with mem.
 Qed.
@@ -3740,8 +3758,8 @@ Theorem alloc_left_mapped_inject:
   inject f m1 m2 ->
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
-  0 <= delta <= Int.max_unsigned ->
-  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) ->
+  0 <= delta <= Ptrofs.max_unsigned ->
+  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Ptrofs.max_unsigned) ->
   (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   inj_offset_aligned delta (hi-lo) ->
   (forall b delta' ofs k p,
@@ -3803,10 +3821,10 @@ Proof.
    subst. injection H9; intros; subst b' delta0. destruct H10.
     exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro.
     exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto.
-    generalize (Int.unsigned_range_2 ofs). omega.
+    generalize (Ptrofs.unsigned_range_2 ofs). omega.
    exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro.
    exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto.
-   generalize (Int.unsigned_range_2 ofs). omega.
+   generalize (Ptrofs.unsigned_range_2 ofs). omega.
   eapply mi_representable0; try eassumption.
   destruct H10; eauto using perm_alloc_4.
 (* perm inv *)
@@ -3843,7 +3861,7 @@ Proof.
   eapply alloc_right_inject; eauto.
   eauto.
   instantiate (1 := b2). eauto with mem.
-  instantiate (1 := 0). unfold Int.max_unsigned. generalize Int.modulus_pos; omega.
+  instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; omega.
   auto.
   intros. apply perm_implies with Freeable; auto with mem.
   eapply perm_alloc_2; eauto. omega.
@@ -4054,13 +4072,13 @@ Proof.
   destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate.
   destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H.
   exploit mi_representable0; eauto. intros [A B].
-  set (ofs' := Int.repr (Int.unsigned ofs + delta1)).
-  assert (Int.unsigned ofs' = Int.unsigned ofs + delta1).
-    unfold ofs'; apply Int.unsigned_repr. auto.
+  set (ofs' := Ptrofs.repr (Ptrofs.unsigned ofs + delta1)).
+  assert (Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs + delta1).
+    unfold ofs'; apply Ptrofs.unsigned_repr. auto.
   exploit mi_representable1. eauto. instantiate (1 := ofs').
   rewrite H.
-  replace (Int.unsigned ofs + delta1 - 1) with
-    ((Int.unsigned ofs - 1) + delta1) by omega.
+  replace (Ptrofs.unsigned ofs + delta1 - 1) with
+    ((Ptrofs.unsigned ofs - 1) + delta1) by omega.
   destruct H0; eauto using perm_inj.
   rewrite H. omega.
 (* perm inv *)
@@ -4185,7 +4203,7 @@ Proof.
   apply flat_inj_no_overlap.
 (* range *)
   unfold flat_inj; intros.
-  destruct (plt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega.
+  destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); omega.
 (* perm inv *)
   unfold flat_inj; intros.
   destruct (plt b1 (nextblock m)); inv H0.
diff --git a/common/Memtype.v b/common/Memtype.v
index 5dbb66dc..b055668c 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -124,13 +124,13 @@ Parameter store: forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: v
 
 Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
   match addr with
-  | Vptr b ofs => load chunk m b (Int.unsigned ofs)
+  | Vptr b ofs => load chunk m b (Ptrofs.unsigned ofs)
   | _ => None
   end.
 
 Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   match addr with
-  | Vptr b ofs => store chunk m b (Int.unsigned ofs) v
+  | Vptr b ofs => store chunk m b (Ptrofs.unsigned ofs) v
   | _ => None
   end.
 
@@ -445,7 +445,7 @@ Axiom load_store_other:
 Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop :=
   match chunk1, chunk2 with
   | (Mint32 | Many32), (Mint32 | Many32) => True
-  | Many64, Many64 => True
+  | (Mint64 | Many64), (Mint64 | Many64) => True
   | _, _ => False
   end.
 
@@ -978,37 +978,37 @@ Axiom weak_valid_pointer_inject:
 Axiom address_inject:
   forall f m1 m2 b1 ofs1 b2 delta p,
   inject f m1 m2 ->
-  perm m1 b1 (Int.unsigned ofs1) Cur p ->
+  perm m1 b1 (Ptrofs.unsigned ofs1) Cur p ->
   f b1 = Some (b2, delta) ->
-  Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.
 
 Axiom valid_pointer_inject_no_overflow:
   forall f m1 m2 b ofs b' delta,
   inject f m1 m2 ->
-  valid_pointer m1 b (Int.unsigned ofs) = true ->
+  valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
   f b = Some(b', delta) ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 
 Axiom weak_valid_pointer_inject_no_overflow:
   forall f m1 m2 b ofs b' delta,
   inject f m1 m2 ->
-  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
   f b = Some(b', delta) ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 
 Axiom valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
-  valid_pointer m1 b (Int.unsigned ofs) = true ->
+  valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
   Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
-  valid_pointer m2 b' (Int.unsigned ofs') = true.
+  valid_pointer m2 b' (Ptrofs.unsigned ofs') = true.
 
 Axiom weak_valid_pointer_inject_val:
   forall f m1 m2 b ofs b' ofs',
   inject f m1 m2 ->
-  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+  weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
   Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
-  weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
+  weak_valid_pointer m2 b' (Ptrofs.unsigned ofs') = true.
 
 Axiom inject_no_overlap:
   forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
@@ -1024,13 +1024,13 @@ Axiom different_pointers_inject:
   forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
   inject f m m' ->
   b1 <> b2 ->
-  valid_pointer m b1 (Int.unsigned ofs1) = true ->
-  valid_pointer m b2 (Int.unsigned ofs2) = true ->
+  valid_pointer m b1 (Ptrofs.unsigned ofs1) = true ->
+  valid_pointer m b2 (Ptrofs.unsigned ofs2) = true ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
   b1' <> b2' \/
-  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <>
-  Int.unsigned (Int.add ofs2 (Int.repr delta2)).
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <>
+  Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).
 
 Axiom load_inject:
   forall f m1 m2 chunk b1 ofs b2 delta v1,
@@ -1141,8 +1141,8 @@ Axiom alloc_left_mapped_inject:
   inject f m1 m2 ->
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
-  0 <= delta <= Int.max_unsigned ->
-  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) ->
+  0 <= delta <= Ptrofs.max_unsigned ->
+  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Ptrofs.max_unsigned) ->
   (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   inj_offset_aligned delta (hi-lo) ->
   (forall b delta' ofs k p,
diff --git a/common/Separation.v b/common/Separation.v
index efcd3281..c0a3c9cf 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -319,7 +319,7 @@ Qed.
 
 Program Definition range (b: block) (lo hi: Z) : massert := {|
   m_pred := fun m =>
-       0 <= lo /\ hi <= Int.modulus
+       0 <= lo /\ hi <= Ptrofs.modulus
     /\ (forall i k p, lo <= i < hi -> Mem.perm m b i k p);
   m_footprint := fun b' ofs' => b' = b /\ lo <= ofs' < hi
 |}.
@@ -333,7 +333,7 @@ Qed.
 Lemma alloc_rule:
   forall m lo hi b m' P,
   Mem.alloc m lo hi = (m', b) ->
-  0 <= lo -> hi <= Int.modulus ->
+  0 <= lo -> hi <= Ptrofs.modulus ->
   m |= P ->
   m' |= range b lo hi ** P.
 Proof.
@@ -413,7 +413,7 @@ Qed.
 
 Program Definition contains (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {|
   m_pred := fun m =>
-       0 <= ofs <= Int.max_unsigned
+       0 <= ofs <= Ptrofs.max_unsigned
     /\ Mem.valid_access m chunk b ofs Freeable
     /\ exists v, Mem.load chunk m b ofs = Some v /\ spec v;
   m_footprint := fun b' ofs' => b' = b /\ ofs <= ofs' < ofs + size_chunk chunk
@@ -431,7 +431,7 @@ Qed.
 Lemma contains_no_overflow:
   forall spec m chunk b ofs,
   m |= contains chunk b ofs spec ->
-  0 <= ofs <= Int.max_unsigned.
+  0 <= ofs <= Ptrofs.max_unsigned.
 Proof.
   intros. simpl in H. tauto.
 Qed.
@@ -448,10 +448,10 @@ Qed.
 Lemma loadv_rule:
   forall spec m chunk b ofs,
   m |= contains chunk b ofs spec ->
-  exists v, Mem.loadv chunk m (Vptr b (Int.repr ofs)) = Some v /\ spec v.
+  exists v, Mem.loadv chunk m (Vptr b (Ptrofs.repr ofs)) = Some v /\ spec v.
 Proof.
   intros. exploit load_rule; eauto. intros (v & A & B). exists v; split; auto.
-  simpl. rewrite Int.unsigned_repr; auto. eapply contains_no_overflow; eauto.
+  simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow; eauto.
 Qed.
 
 Lemma store_rule:
@@ -477,10 +477,10 @@ Lemma storev_rule:
   m |= contains chunk b ofs spec1 ** P ->
   spec (Val.load_result chunk v) ->
   exists m',
-  Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P.
+  Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P.
 Proof.
   intros. exploit store_rule; eauto. intros (m' & A & B). exists m'; split; auto.
-  simpl. rewrite Int.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto.
+  simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto.
 Qed.
 
 Lemma range_contains:
@@ -493,7 +493,7 @@ Proof.
   split; [|split].
 - assert (Mem.valid_access m chunk b ofs Freeable).
   { split; auto. red; auto. }
-  split. generalize (size_chunk_pos chunk). unfold Int.max_unsigned. omega.
+  split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. omega.
   split. auto.
 + destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD].
   eauto with mem.
@@ -530,7 +530,7 @@ Lemma storev_rule':
   forall chunk m b ofs v (spec1: val -> Prop) P,
   m |= contains chunk b ofs spec1 ** P ->
   exists m',
-  Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P.
+  Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P.
 Proof.
   intros. eapply storev_rule; eauto.
 Qed.
@@ -656,9 +656,9 @@ Proof.
   intros. destruct H as (A & B & C). simpl in A.
   exploit Mem.storev_mapped_inject; eauto. intros (m2' & STORE & INJ).
   inv H1; simpl in STORE; try discriminate.
-  assert (VALID: Mem.valid_access m1 chunk b1 (Int.unsigned ofs1) Writable)
+  assert (VALID: Mem.valid_access m1 chunk b1 (Ptrofs.unsigned ofs1) Writable)
     by eauto with mem.
-  assert (EQ: Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta).
+  assert (EQ: Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta).
   { eapply Mem.address_inject'; eauto with mem. }
   exists m2'; split; auto.
   split; [|split].
@@ -681,7 +681,7 @@ Lemma alloc_parallel_rule:
   (8 | delta) ->
   lo = delta ->
   hi = delta + Zmax 0 sz1 ->
-  0 <= sz2 <= Int.max_unsigned ->
+  0 <= sz2 <= Ptrofs.max_unsigned ->
   0 <= delta -> hi <= sz2 ->
   exists j',
      m2' |= range b2 0 lo ** range b2 hi sz2 ** minjection j' m1' ** P
@@ -709,7 +709,7 @@ Proof.
   exists j'; split; auto.
   rewrite <- ! sep_assoc.
   split; [|split].
-+ simpl. intuition auto; try (unfold Int.max_unsigned in *; omega).
++ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; omega).
 * apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.perm_alloc_2; eauto. omega. 
 * apply Mem.perm_implies with Freeable; auto with mem.
@@ -891,7 +891,7 @@ Lemma alloc_parallel_rule_2:
   (8 | delta) ->
   lo = delta ->
   hi = delta + Zmax 0 sz1 ->
-  0 <= sz2 <= Int.max_unsigned ->
+  0 <= sz2 <= Ptrofs.max_unsigned ->
   0 <= delta -> hi <= sz2 ->
   exists j',
      m2' |= range b2 0 lo ** range b2 hi sz2 ** minjection j' m1' ** globalenv_inject ge j' ** P
diff --git a/common/Values.v b/common/Values.v
index 663bddf6..d1058fe8 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -16,6 +16,7 @@
 (** This module defines the type of values that is used in the dynamic
   semantics of all our intermediate languages. *)
 
+Require Archi.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
@@ -39,7 +40,7 @@ Inductive val: Type :=
   | Vlong: int64 -> val
   | Vfloat: float -> val
   | Vsingle: float32 -> val
-  | Vptr: block -> int -> val.
+  | Vptr: block -> ptrofs -> val.
 
 Definition Vzero: val := Vint Int.zero.
 Definition Vone: val := Vint Int.one.
@@ -48,6 +49,12 @@ Definition Vmone: val := Vint Int.mone.
 Definition Vtrue: val := Vint Int.one.
 Definition Vfalse: val := Vint Int.zero.
 
+Definition Vnullptr :=
+  if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero.
+
+Definition Vptrofs (n: ptrofs) :=
+  if Archi.ptr64 then Vlong (Ptrofs.to_int64 n) else Vint (Ptrofs.to_int n).
+
 (** * Operations over values *)
 
 (** The module [Val] defines a number of arithmetic and logical operations
@@ -63,7 +70,7 @@ Proof.
   apply Int64.eq_dec.
   apply Float.eq_dec.
   apply Float32.eq_dec.
-  apply Int.eq_dec.
+  apply Ptrofs.eq_dec.
   apply eq_block.
 Defined.
 Global Opaque eq.
@@ -75,8 +82,10 @@ Definition has_type (v: val) (t: typ) : Prop :=
   | Vlong _, Tlong => True
   | Vfloat _, Tfloat => True
   | Vsingle _, Tsingle => True
-  | Vptr _ _, Tint => True
-  | (Vint _ | Vptr _ _ | Vsingle _), Tany32 => True
+  | Vptr _ _, Tint => Archi.ptr64 = false
+  | Vptr _ _, Tlong => Archi.ptr64 = true
+  | (Vint _ | Vsingle _), Tany32 => True
+  | Vptr _ _, Tany32 => Archi.ptr64 = false
   | _, Tany64 => True
   | _, _ => False
   end.
@@ -94,12 +103,25 @@ Definition has_opttype (v: val) (ot: option typ) : Prop :=
   | Some t => has_type v t
   end.
 
+Lemma Vptr_has_type:
+  forall b ofs, has_type (Vptr b ofs) Tptr.
+Proof.
+  intros. unfold Tptr, has_type; destruct Archi.ptr64; reflexivity.
+Qed.
+
+Lemma Vnullptr_has_type:
+  has_type Vnullptr Tptr.
+Proof.
+  unfold has_type, Vnullptr, Tptr; destruct Archi.ptr64; reflexivity.
+Qed.
+
 Lemma has_subtype:
   forall ty1 ty2 v,
   subtype ty1 ty2 = true -> has_type v ty1 -> has_type v ty2.
 Proof.
-  intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac;
-  unfold has_type in *; destruct v; auto.
+  intros. destruct ty1; destruct ty2; simpl in H;
+  (contradiction || discriminate || assumption || idtac);
+  unfold has_type in *; destruct v; auto; contradiction.
 Qed.
 
 Lemma has_subtype_list:
@@ -257,17 +279,18 @@ Definition floatofsingle (v: val) : val :=
 Definition add (v1 v2: val): val :=
   match v1, v2 with
   | Vint n1, Vint n2 => Vint(Int.add n1 n2)
-  | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.add ofs1 n2)
-  | Vint n1, Vptr b2 ofs2 => Vptr b2 (Int.add ofs2 n1)
+  | Vptr b1 ofs1, Vint n2 => if Archi.ptr64 then Vundef else Vptr b1 (Ptrofs.add ofs1 (Ptrofs.of_int n2))
+  | Vint n1, Vptr b2 ofs2 => if Archi.ptr64 then Vundef else Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int n1))
   | _, _ => Vundef
   end.
 
 Definition sub (v1 v2: val): val :=
   match v1, v2 with
   | Vint n1, Vint n2 => Vint(Int.sub n1 n2)
-  | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.sub ofs1 n2)
+  | Vptr b1 ofs1, Vint n2 => if Archi.ptr64 then Vundef else Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.of_int n2))
   | Vptr b1 ofs1, Vptr b2 ofs2 =>
-      if eq_block b1 b2 then Vint(Int.sub ofs1 ofs2) else Vundef
+      if Archi.ptr64 then Vundef else
+      if eq_block b1 b2 then Vint(Ptrofs.to_int (Ptrofs.sub ofs1 ofs2)) else Vundef
   | _, _ => Vundef
   end.
 
@@ -571,12 +594,19 @@ Definition singleoflongu (v: val) : option val :=
 Definition addl (v1 v2: val): val :=
   match v1, v2 with
   | Vlong n1, Vlong n2 => Vlong(Int64.add n1 n2)
+  | Vptr b1 ofs1, Vlong n2 => if Archi.ptr64 then Vptr b1 (Ptrofs.add ofs1 (Ptrofs.of_int64 n2)) else Vundef
+  | Vlong n1, Vptr b2 ofs2 => if Archi.ptr64 then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n1)) else Vundef
   | _, _ => Vundef
   end.
 
 Definition subl (v1 v2: val): val :=
   match v1, v2 with
   | Vlong n1, Vlong n2 => Vlong(Int64.sub n1 n2)
+  | Vptr b1 ofs1, Vlong n2 =>
+      if Archi.ptr64 then Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.of_int64 n2)) else Vundef
+  | Vptr b1 ofs1, Vptr b2 ofs2 =>
+      if negb Archi.ptr64 then Vundef else
+      if eq_block b1 b2 then Vlong(Ptrofs.to_int64 (Ptrofs.sub ofs1 ofs2)) else Vundef
   | _, _ => Vundef
   end.
 
@@ -626,6 +656,18 @@ Definition modlu (v1 v2: val): option val :=
   | _, _ => None
   end.
 
+Definition subl_overflow (v1 v2: val) : val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vint (Int.repr (Int64.unsigned (Int64.sub_overflow n1 n2 Int64.zero)))
+  | _, _ => Vundef
+  end.
+
+Definition negativel (v: val) : val :=
+  match v with
+  | Vlong n => Vint (Int.repr (Int64.unsigned (Int64.negative n)))
+  | _ => Vundef
+  end.
+
 Definition andl (v1 v2: val): val :=
   match v1, v2 with
   | Vlong n1, Vlong n2 => Vlong(Int64.and n1 n2)
@@ -671,6 +713,24 @@ Definition shrlu (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
+Definition roll (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vint n2 => Vlong(Int64.rol n1 (Int64.repr (Int.unsigned n2)))
+  | _, _ => Vundef
+  end.
+
+Definition rorl (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vint n2 => Vlong(Int64.ror n1 (Int64.repr (Int.unsigned n2)))
+  | _, _ => Vundef
+  end.
+
+Definition rolml (v: val) (amount mask: int64): val :=
+  match v with
+  | Vlong n => Vlong(Int64.rolm n amount mask)
+  | _ => Vundef
+  end.
+
 (** Comparisons *)
 
 Section COMPARISONS.
@@ -696,22 +756,25 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
   | Vint n1, Vint n2 =>
       Some (Int.cmpu c n1 n2)
   | Vint n1, Vptr b2 ofs2 =>
-      if Int.eq n1 Int.zero && weak_valid_ptr b2 (Int.unsigned ofs2)
+      if Archi.ptr64 then None else
+      if Int.eq n1 Int.zero && weak_valid_ptr b2 (Ptrofs.unsigned ofs2)
       then cmp_different_blocks c
       else None
   | Vptr b1 ofs1, Vptr b2 ofs2 =>
+      if Archi.ptr64 then None else
       if eq_block b1 b2 then
-        if weak_valid_ptr b1 (Int.unsigned ofs1)
-           && weak_valid_ptr b2 (Int.unsigned ofs2)
-        then Some (Int.cmpu c ofs1 ofs2)
+        if weak_valid_ptr b1 (Ptrofs.unsigned ofs1)
+           && weak_valid_ptr b2 (Ptrofs.unsigned ofs2)
+        then Some (Ptrofs.cmpu c ofs1 ofs2)
         else None
       else
-        if valid_ptr b1 (Int.unsigned ofs1)
-           && valid_ptr b2 (Int.unsigned ofs2)
+        if valid_ptr b1 (Ptrofs.unsigned ofs1)
+           && valid_ptr b2 (Ptrofs.unsigned ofs2)
         then cmp_different_blocks c
         else None
   | Vptr b1 ofs1, Vint n2 =>
-      if Int.eq n2 Int.zero && weak_valid_ptr b1 (Int.unsigned ofs1)
+      if Archi.ptr64 then None else
+      if Int.eq n2 Int.zero && weak_valid_ptr b1 (Ptrofs.unsigned ofs1)
       then cmp_different_blocks c
       else None
   | _, _ => None
@@ -738,6 +801,28 @@ Definition cmpl_bool (c: comparison) (v1 v2: val): option bool :=
 Definition cmplu_bool (c: comparison) (v1 v2: val): option bool :=
   match v1, v2 with
   | Vlong n1, Vlong n2 => Some (Int64.cmpu c n1 n2)
+  | Vlong n1, Vptr b2 ofs2 =>
+      if negb Archi.ptr64 then None else
+      if Int64.eq n1 Int64.zero && weak_valid_ptr b2 (Ptrofs.unsigned ofs2)
+      then cmp_different_blocks c
+      else None
+  | Vptr b1 ofs1, Vptr b2 ofs2 =>
+      if negb Archi.ptr64 then None else
+      if eq_block b1 b2 then
+        if weak_valid_ptr b1 (Ptrofs.unsigned ofs1)
+           && weak_valid_ptr b2 (Ptrofs.unsigned ofs2)
+        then Some (Ptrofs.cmpu c ofs1 ofs2)
+        else None
+      else
+        if valid_ptr b1 (Ptrofs.unsigned ofs1)
+           && valid_ptr b2 (Ptrofs.unsigned ofs2)
+        then cmp_different_blocks c
+        else None
+  | Vptr b1 ofs1, Vlong n2 =>
+      if negb Archi.ptr64 then None else
+      if Int64.eq n2 Int64.zero && weak_valid_ptr b1 (Ptrofs.unsigned ofs1)
+      then cmp_different_blocks c
+      else None
   | _, _ => None
   end.
 
@@ -770,6 +855,14 @@ Definition maskzero_bool (v: val) (mask: int): option bool :=
 
 End COMPARISONS.
 
+(** Add the given offset to the given pointer. *)
+
+Definition offset_ptr (v: val) (delta: ptrofs) : val :=
+  match v with
+  | Vptr b ofs => Vptr b (Ptrofs.add ofs delta)
+  | _ => Vundef
+  end.
+
 (** [load_result] reflects the effect of storing a value with a given
   memory chunk, then reading it back with the same chunk.  Depending
   on the chunk and the type of the value, some normalization occurs.
@@ -786,11 +879,13 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
   | Mint16signed, Vint n => Vint (Int.sign_ext 16 n)
   | Mint16unsigned, Vint n => Vint (Int.zero_ext 16 n)
   | Mint32, Vint n => Vint n
-  | Mint32, Vptr b ofs => Vptr b ofs
+  | Mint32, Vptr b ofs => if Archi.ptr64 then Vundef else Vptr b ofs
   | Mint64, Vlong n => Vlong n
+  | Mint64, Vptr b ofs => if Archi.ptr64 then Vptr b ofs else Vundef
   | Mfloat32, Vsingle f => Vsingle f
   | Mfloat64, Vfloat f => Vfloat f
-  | Many32, (Vint _ | Vptr _ _ | Vsingle _) => v
+  | Many32, (Vint _ | Vsingle _) => v
+  | Many32, Vptr _ _ => if Archi.ptr64 then Vundef else v
   | Many64, _ => v
   | _, _ => Vundef
   end.
@@ -798,13 +893,14 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
 Lemma load_result_type:
   forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk).
 Proof.
-  intros. destruct chunk; destruct v; simpl; auto.
+  intros. unfold has_type; destruct chunk; destruct v; simpl; auto; destruct Archi.ptr64 eqn:SF; simpl; auto.
 Qed.
 
 Lemma load_result_same:
   forall v ty, has_type v ty -> load_result (chunk_of_type ty) v = v.
 Proof.
-  unfold has_type; intros. destruct v; destruct ty; try contradiction; auto.
+  unfold has_type, load_result; intros.
+  destruct v; destruct ty; destruct Archi.ptr64; try contradiction; try discriminate; auto.
 Qed.
 
 (** Theorems on arithmetic operations. *)
@@ -882,13 +978,15 @@ Qed.
 
 Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
 Proof.
-  destruct x; destruct y; destruct z; simpl; auto.
-  rewrite Int.add_assoc; auto.
-  rewrite Int.add_assoc; auto.
-  decEq. decEq. apply Int.add_commut.
-  decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc.
-  decEq. apply Int.add_commut.
-  decEq. rewrite Int.add_assoc. auto.
+  unfold add; intros; destruct Archi.ptr64 eqn:SF, x, y, z; simpl; auto.
+- rewrite Int.add_assoc; auto.
+- rewrite Int.add_assoc; auto.
+- rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
+  rewrite Ptrofs.add_commut. auto with ptrofs.
+- rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
+  apply Ptrofs.add_commut.
+- rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
+  symmetry. auto with ptrofs.
 Qed.
 
 Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
@@ -910,7 +1008,8 @@ Qed.
 
 Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
 Proof.
-  destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr.
+  unfold neg, add; intros; destruct Archi.ptr64 eqn:SF, x, y; simpl; auto;
+  rewrite Int.neg_add_distr; auto.
 Qed.
 
 Theorem sub_zero_r: forall x, sub Vzero x = neg x.
@@ -920,37 +1019,40 @@ Qed.
 
 Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)).
 Proof.
-  destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto.
+  unfold sub, add; intros; destruct Archi.ptr64 eqn:SF, x; auto.
+- rewrite Int.sub_add_opp; auto.
+- rewrite Int.sub_add_opp; auto.
+- rewrite Ptrofs.sub_add_opp. f_equal. f_equal. symmetry. auto with ptrofs.
 Qed.
 
 Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y).
 Proof.
-  intros. unfold sub, add.
-  destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto.
+  intros. rewrite sub_add_opp. rewrite Int.neg_involutive. auto.
 Qed.
 
 Theorem sub_add_l:
   forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i).
 Proof.
-  destruct v1; destruct v2; intros; simpl; auto.
-  rewrite Int.sub_add_l. auto.
-  rewrite Int.sub_add_l. auto.
-  case (eq_block b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.
+  unfold sub, add; intros; destruct Archi.ptr64 eqn:SF, v1, v2; auto.
+- rewrite Int.sub_add_l; auto.
+- rewrite Int.sub_add_l; auto.
+- rewrite Ptrofs.sub_add_l; auto.
+- destruct (eq_block b b0); auto.
+  f_equal. rewrite Ptrofs.sub_add_l. auto with ptrofs.
 Qed.
 
 Theorem sub_add_r:
   forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)).
 Proof.
-  destruct v1; destruct v2; intros; simpl; auto.
-  rewrite Int.sub_add_r. auto.
-  repeat rewrite Int.sub_add_opp. decEq.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  decEq. repeat rewrite Int.sub_add_opp.
-  rewrite Int.add_assoc. decEq. apply Int.neg_add_distr.
-  case (eq_block b b0); intro. simpl. decEq.
-  repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq.
-  apply Int.neg_add_distr.
-  reflexivity.
+  unfold sub, add; intros; destruct Archi.ptr64 eqn:SF, v1, v2; auto.
+- rewrite Int.add_commut. rewrite Int.sub_add_r. auto.
+- rewrite Int.add_commut. rewrite Int.sub_add_r. auto.
+- f_equal. replace (Ptrofs.of_int (Int.add i1 i)) with (Ptrofs.add (Ptrofs.of_int i) (Ptrofs.of_int i1)).
+  rewrite Ptrofs.sub_add_r. f_equal.
+  symmetry. auto with ptrofs.
+  symmetry. rewrite Int.add_commut. auto with ptrofs.
+- destruct (eq_block b b0); auto.
+  f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. 
 Qed.
 
 Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -967,16 +1069,15 @@ Qed.
 Theorem mul_add_distr_l:
   forall x y z, mul (add x y) z = add (mul x z) (mul y z).
 Proof.
-  destruct x; destruct y; destruct z; simpl; auto.
-  decEq. apply Int.mul_add_distr_l.
+  unfold mul, add; intros; destruct Archi.ptr64 eqn:SF, x, y, z; simpl; auto;
+  rewrite Int.mul_add_distr_l; auto.
 Qed.
 
-
 Theorem mul_add_distr_r:
   forall x y z, mul x (add y z) = add (mul x y) (mul x z).
 Proof.
-  destruct x; destruct y; destruct z; simpl; auto.
-  decEq. apply Int.mul_add_distr_r.
+  unfold mul, add; intros; destruct Archi.ptr64 eqn:SF, x, y, z; simpl; auto;
+  rewrite Int.mul_add_distr_r; auto.
 Qed.
 
 Theorem mul_pow2:
@@ -1165,6 +1266,144 @@ Proof.
   intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero.
 Qed.
 
+Theorem addl_commut: forall x y, addl x y = addl y x.
+Proof.
+  destruct x; destruct y; simpl; auto.
+  decEq. apply Int64.add_commut.
+Qed.
+
+Theorem addl_assoc: forall x y z, addl (addl x y) z = addl x (addl y z).
+Proof.
+  unfold addl; intros; destruct Archi.ptr64 eqn:SF, x, y, z; simpl; auto.
+- rewrite Int64.add_assoc; auto.
+- rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
+  rewrite Ptrofs.add_commut. auto with ptrofs.
+- rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
+  apply Ptrofs.add_commut.
+- rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
+  symmetry. auto with ptrofs.
+- rewrite Int64.add_assoc; auto.
+Qed.
+
+Theorem addl_permut: forall x y z, addl x (addl y z) = addl y (addl x z).
+Proof.
+  intros. rewrite (addl_commut y z). rewrite <- addl_assoc. apply addl_commut.
+Qed.
+
+Theorem addl_permut_4:
+  forall x y z t, addl (addl x y) (addl z t) = addl (addl x z) (addl y t).
+Proof.
+  intros. rewrite addl_permut. rewrite addl_assoc.
+  rewrite addl_permut. symmetry. apply addl_assoc.
+Qed.
+
+Theorem negl_addl_distr: forall x y, negl(addl x y) = addl (negl x) (negl y).
+Proof.
+  unfold negl, addl; intros; destruct Archi.ptr64 eqn:SF; destruct x; destruct y; simpl; auto;
+  decEq; apply Int64.neg_add_distr.
+Qed.
+
+Theorem subl_addl_opp: forall x y, subl x (Vlong y) = addl x (Vlong (Int64.neg y)).
+Proof.
+  unfold subl, addl; intros; destruct Archi.ptr64 eqn:SF, x; auto.
+- rewrite Int64.sub_add_opp; auto.
+- rewrite Ptrofs.sub_add_opp. f_equal. f_equal. symmetry. auto with ptrofs.
+- rewrite Int64.sub_add_opp; auto.
+Qed.
+
+Theorem subl_opp_addl: forall x y, subl x (Vlong (Int64.neg y)) = addl x (Vlong y).
+Proof.
+  intros. rewrite subl_addl_opp. rewrite Int64.neg_involutive. auto.
+Qed.
+
+Theorem subl_addl_l:
+  forall v1 v2 i, subl (addl v1 (Vlong i)) v2 = addl (subl v1 v2) (Vlong i).
+Proof.
+  unfold subl, addl; intros; destruct Archi.ptr64 eqn:SF, v1, v2; auto.
+- rewrite Int64.sub_add_l; auto.
+- rewrite Ptrofs.sub_add_l; auto.
+- destruct (eq_block b b0); auto.
+  simpl. f_equal. rewrite Ptrofs.sub_add_l. auto with ptrofs.
+- rewrite Int64.sub_add_l; auto.
+Qed.
+
+Theorem subl_addl_r:
+  forall v1 v2 i, subl v1 (addl v2 (Vlong i)) = addl (subl v1 v2) (Vlong (Int64.neg i)).
+Proof.
+  unfold subl, addl; intros; destruct Archi.ptr64 eqn:SF, v1, v2; auto.
+- rewrite Int64.add_commut. rewrite Int64.sub_add_r. auto.
+- f_equal. replace (Ptrofs.of_int64 (Int64.add i1 i)) with (Ptrofs.add (Ptrofs.of_int64 i) (Ptrofs.of_int64 i1)).
+  rewrite Ptrofs.sub_add_r. f_equal.
+  symmetry. auto with ptrofs.
+  symmetry. rewrite Int64.add_commut. auto with ptrofs.
+- destruct (eq_block b b0); auto.
+  simpl; f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. 
+- rewrite Int64.add_commut. rewrite Int64.sub_add_r. auto.
+Qed.
+
+Theorem mull_commut: forall x y, mull x y = mull y x.
+Proof.
+  destruct x; destruct y; simpl; auto. decEq. apply Int64.mul_commut.
+Qed.
+
+Theorem mull_assoc: forall x y z, mull (mull x y) z = mull x (mull y z).
+Proof.
+  destruct x; destruct y; destruct z; simpl; auto.
+  decEq. apply Int64.mul_assoc.
+Qed.
+
+Theorem mull_addl_distr_l:
+  forall x y z, mull (addl x y) z = addl (mull x z) (mull y z).
+Proof.
+  unfold mull, addl; intros; destruct Archi.ptr64 eqn:SF; destruct x; destruct y; destruct z; simpl; auto;
+  decEq; apply Int64.mul_add_distr_l.
+Qed.
+
+Theorem mull_addl_distr_r:
+  forall x y z, mull x (addl y z) = addl (mull x y) (mull x z).
+Proof.
+  unfold mull, addl; intros; destruct Archi.ptr64 eqn:SF; destruct x; destruct y; destruct z; simpl; auto;
+  decEq; apply Int64.mul_add_distr_r.
+Qed.
+
+Theorem andl_commut: forall x y, andl x y = andl y x.
+Proof.
+  destruct x; destruct y; simpl; auto. decEq. apply Int64.and_commut.
+Qed.
+
+Theorem andl_assoc: forall x y z, andl (andl x y) z = andl x (andl y z).
+Proof.
+  destruct x; destruct y; destruct z; simpl; auto.
+  decEq. apply Int64.and_assoc.
+Qed.
+
+Theorem orl_commut: forall x y, orl x y = orl y x.
+Proof.
+  destruct x; destruct y; simpl; auto. decEq. apply Int64.or_commut.
+Qed.
+
+Theorem orl_assoc: forall x y z, orl (orl x y) z = orl x (orl y z).
+Proof.
+  destruct x; destruct y; destruct z; simpl; auto.
+  decEq. apply Int64.or_assoc.
+Qed.
+
+Theorem xorl_commut: forall x y, xorl x y = xorl y x.
+Proof.
+  destruct x; destruct y; simpl; auto. decEq. apply Int64.xor_commut.
+Qed.
+
+Theorem xorl_assoc: forall x y z, xorl (xorl x y) z = xorl x (xorl y z).
+Proof.
+  destruct x; destruct y; destruct z; simpl; auto.
+  decEq. apply Int64.xor_assoc.
+Qed.
+
+Theorem notl_xorl: forall x, notl x = xorl x (Vlong Int64.mone).
+Proof.
+  destruct x; simpl; auto.
+Qed.
+
 Theorem negate_cmp_bool:
   forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y).
 Proof.
@@ -1177,17 +1416,44 @@ Theorem negate_cmpu_bool:
 Proof.
   assert (forall c,
     cmp_different_blocks (negate_comparison c) = option_map negb (cmp_different_blocks c)).
-  destruct c; auto.
-  destruct x; destruct y; simpl; auto.
-  rewrite Int.negate_cmpu. auto.
-  destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto.
-  destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto.
-  destruct (eq_block b b0).
-  destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) &&
-            (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))).
-  rewrite Int.negate_cmpu. auto.
+  { destruct c; auto. }
+  unfold cmpu_bool; intros; destruct Archi.ptr64 eqn:SF, x, y; auto.
+- rewrite Int.negate_cmpu. auto.
+- rewrite Int.negate_cmpu. auto.
+- destruct (Int.eq i Int.zero && (valid_ptr b (Ptrofs.unsigned i0) || valid_ptr b (Ptrofs.unsigned i0 - 1))); auto.
+- destruct (Int.eq i0 Int.zero && (valid_ptr b (Ptrofs.unsigned i) || valid_ptr b (Ptrofs.unsigned i - 1))); auto.
+- destruct (eq_block b b0).
+  destruct ((valid_ptr b (Ptrofs.unsigned i) || valid_ptr b (Ptrofs.unsigned i - 1)) &&
+            (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1))).
+  rewrite Ptrofs.negate_cmpu. auto.
   auto.
-  destruct (valid_ptr b (Int.unsigned i) && valid_ptr b0 (Int.unsigned i0)); auto.
+  destruct (valid_ptr b (Ptrofs.unsigned i) && valid_ptr b0 (Ptrofs.unsigned i0)); auto.
+Qed.
+
+Theorem negate_cmpl_bool:
+  forall c x y, cmpl_bool (negate_comparison c) x y = option_map negb (cmpl_bool c x y).
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Int64.negate_cmp. auto.
+Qed.
+
+Theorem negate_cmplu_bool:
+  forall valid_ptr c x y,
+  cmplu_bool valid_ptr (negate_comparison c) x y = option_map negb (cmplu_bool valid_ptr c x y).
+Proof.
+  assert (forall c,
+    cmp_different_blocks (negate_comparison c) = option_map negb (cmp_different_blocks c)).
+  { destruct c; auto. }
+  unfold cmplu_bool; intros; destruct Archi.ptr64 eqn:SF, x, y; auto.
+- rewrite Int64.negate_cmpu. auto.
+- simpl. destruct (Int64.eq i Int64.zero && (valid_ptr b (Ptrofs.unsigned i0) || valid_ptr b (Ptrofs.unsigned i0 - 1))); auto.
+- simpl. destruct (Int64.eq i0 Int64.zero && (valid_ptr b (Ptrofs.unsigned i) || valid_ptr b (Ptrofs.unsigned i - 1))); auto.
+- simpl. destruct (eq_block b b0).
+  destruct ((valid_ptr b (Ptrofs.unsigned i) || valid_ptr b (Ptrofs.unsigned i - 1)) &&
+            (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1))).
+  rewrite Ptrofs.negate_cmpu. auto.
+  auto.
+  destruct (valid_ptr b (Ptrofs.unsigned i) && valid_ptr b0 (Ptrofs.unsigned i0)); auto.
+- rewrite Int64.negate_cmpu. auto.
 Qed.
 
 Lemma not_of_optbool:
@@ -1223,21 +1489,47 @@ Theorem swap_cmpu_bool:
   cmpu_bool valid_ptr (swap_comparison c) x y =
     cmpu_bool valid_ptr c y x.
 Proof.
-  assert (forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
-    destruct c; auto.
-  destruct x; destruct y; simpl; auto.
-  rewrite Int.swap_cmpu. auto.
-  destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto.
-  destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto.
-  destruct (eq_block b b0); subst.
+  assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
+  { destruct c; auto. }
+  intros; unfold cmpu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.  
+- rewrite Int.swap_cmpu. auto.
+- rewrite Int.swap_cmpu. auto.
+- destruct (eq_block b b0); subst.
+  rewrite dec_eq_true.
+  destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1));
+  destruct (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1));
+  simpl; auto.
+  rewrite Ptrofs.swap_cmpu. auto.
+  rewrite dec_eq_false by auto.
+  destruct (valid_ptr b (Ptrofs.unsigned i));
+    destruct (valid_ptr b0 (Ptrofs.unsigned i0)); simpl; auto.
+Qed.
+
+Theorem swap_cmpl_bool:
+  forall c x y,
+  cmpl_bool (swap_comparison c) x y = cmpl_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Int64.swap_cmp. auto.
+Qed.
+
+Theorem swap_cmplu_bool:
+  forall valid_ptr c x y,
+  cmplu_bool valid_ptr (swap_comparison c) x y = cmplu_bool valid_ptr c y x.
+Proof.
+  assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
+  { destruct c; auto. }
+  intros; unfold cmplu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.  
+- rewrite Int64.swap_cmpu. auto.
+- destruct (eq_block b b0); subst.
   rewrite dec_eq_true.
-  destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1));
-  destruct (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1));
+  destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1));
+  destruct (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1));
   simpl; auto.
-  rewrite Int.swap_cmpu. auto.
+  rewrite Ptrofs.swap_cmpu. auto.
   rewrite dec_eq_false by auto.
-  destruct (valid_ptr b (Int.unsigned i));
-    destruct (valid_ptr b0 (Int.unsigned i0)); simpl; auto.
+  destruct (valid_ptr b (Ptrofs.unsigned i));
+    destruct (valid_ptr b0 (Ptrofs.unsigned i0)); simpl; auto.
+- rewrite Int64.swap_cmpu. auto.
 Qed.
 
 Theorem negate_cmpf_eq:
@@ -1426,6 +1718,13 @@ Proof.
   intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto.
 Qed.
 
+Lemma addl_lessdef:
+  forall v1 v1' v2 v2',
+  lessdef v1 v1' -> lessdef v2 v2' -> lessdef (addl v1 v2) (addl v1' v2').
+Proof.
+  intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto.
+Qed.
+
 Lemma cmpu_bool_lessdef:
   forall valid_ptr valid_ptr' c v1 v1' v2 v2' b,
   (forall b ofs, valid_ptr b ofs = true -> valid_ptr' b ofs = true) ->
@@ -1434,23 +1733,60 @@ Lemma cmpu_bool_lessdef:
   cmpu_bool valid_ptr' c v1' v2' = Some b.
 Proof.
   intros.
-  assert (A: forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true ->
-                           valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true).
-  { intros until ofs. rewrite ! orb_true_iff. intuition. }
-  destruct v1; simpl in H2; try discriminate;
-  destruct v2; simpl in H2; try discriminate;
-  inv H0; inv H1; simpl; auto.
-  destruct (Int.eq i Int.zero && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))) eqn:E; try discriminate.
-  InvBooleans. rewrite H0, A by auto. auto.
-  destruct (Int.eq i0 Int.zero && (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1))) eqn:E; try discriminate.
-  InvBooleans. rewrite H0, A by auto. auto.
-  destruct (eq_block b0 b1).
-  destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate.
-  destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate.
-  erewrite ! A by eauto. auto.
-  destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate.
-  destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate.
-  erewrite ! H by eauto. auto.
+  assert (X: forall b ofs,
+             valid_ptr b ofs || valid_ptr b (ofs - 1) = true ->
+             valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true).
+  { intros. apply orb_true_intro. destruct (orb_prop _ _ H3).
+    rewrite (H b0 ofs); auto.
+    rewrite (H b0 (ofs - 1)); auto. }
+  inv H0; [ | discriminate].
+  inv H1; [ | destruct v1'; discriminate ].
+  unfold cmpu_bool in *. remember Archi.ptr64 as ptr64.
+  destruct v1'; auto; destruct v2'; auto; destruct ptr64; auto.
+- destruct (Int.eq i Int.zero); auto.
+  destruct (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1)) eqn:A; inv H2.
+  rewrite X; auto.
+- destruct (Int.eq i0 Int.zero); auto.
+  destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)) eqn:A; inv H2.
+  rewrite X; auto.
+- destruct (eq_block b0 b1).
++ destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)) eqn:A; inv H2.
+  destruct (valid_ptr b1 (Ptrofs.unsigned i0) || valid_ptr b1 (Ptrofs.unsigned i0 - 1)) eqn:B; inv H1.
+  rewrite ! X; auto.
++ destruct (valid_ptr b0 (Ptrofs.unsigned i) && valid_ptr b1 (Ptrofs.unsigned i0)) eqn:A; inv H2.
+  InvBooleans. rewrite ! H; auto.
+Qed.
+
+Lemma cmplu_bool_lessdef:
+  forall valid_ptr valid_ptr' c v1 v1' v2 v2' b,
+  (forall b ofs, valid_ptr b ofs = true -> valid_ptr' b ofs = true) ->
+  lessdef v1 v1' -> lessdef v2 v2' ->
+  cmplu_bool valid_ptr c v1 v2 = Some b ->
+  cmplu_bool valid_ptr' c v1' v2' = Some b.
+Proof.
+  intros.
+  assert (X: forall b ofs,
+             valid_ptr b ofs || valid_ptr b (ofs - 1) = true ->
+             valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true).
+  { intros. apply orb_true_intro. destruct (orb_prop _ _ H3).
+    rewrite (H b0 ofs); auto.
+    rewrite (H b0 (ofs - 1)); auto. }
+  inv H0; [ | discriminate].
+  inv H1; [ | destruct v1'; discriminate ].
+  unfold cmplu_bool in *. remember Archi.ptr64 as ptr64.
+  destruct v1'; auto; destruct v2'; auto; destruct ptr64; auto.
+- destruct (Int64.eq i Int64.zero); auto.
+  destruct (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1)) eqn:A; inv H2.
+  rewrite X; auto.
+- destruct (Int64.eq i0 Int64.zero); auto.
+  destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)) eqn:A; inv H2.
+  rewrite X; auto.
+- destruct (eq_block b0 b1).
++ destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)) eqn:A; inv H2.
+  destruct (valid_ptr b1 (Ptrofs.unsigned i0) || valid_ptr b1 (Ptrofs.unsigned i0 - 1)) eqn:B; inv H1.
+  rewrite ! X; auto.
++ destruct (valid_ptr b0 (Ptrofs.unsigned i) && valid_ptr b1 (Ptrofs.unsigned i0)) eqn:A; inv H2.
+  InvBooleans. rewrite ! H; auto.
 Qed.
 
 Lemma of_optbool_lessdef:
@@ -1480,6 +1816,18 @@ Proof.
   intros. inv H; auto.
 Qed.
 
+Lemma offset_ptr_zero:
+  forall v, lessdef (offset_ptr v Ptrofs.zero) v.
+Proof.
+  intros. destruct v; simpl; auto. rewrite Ptrofs.add_zero; auto.
+Qed.
+
+Lemma offset_ptr_assoc:
+  forall v d1 d2, offset_ptr (offset_ptr v d1) d2 = offset_ptr v (Ptrofs.add d1 d2).
+Proof.
+  intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc. 
+Qed.
+
 (** * Values and memory injections *)
 
 (** A memory injection [f] is a function from addresses to either [None]
@@ -1509,7 +1857,7 @@ Inductive inject (mi: meminj): val -> val -> Prop :=
   | inject_ptr:
       forall b1 ofs1 b2 ofs2 delta,
       mi b1 = Some (b2, delta) ->
-      ofs2 = Int.add ofs1 (Int.repr delta) ->
+      ofs2 = Ptrofs.add ofs1 (Ptrofs.repr delta) ->
       inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)
   | val_inject_undef: forall v,
       inject mi Vundef v.
@@ -1525,6 +1873,14 @@ Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
 
 Hint Resolve inject_list_nil inject_list_cons.
 
+Lemma inject_ptrofs:
+  forall mi i, inject mi (Vptrofs i) (Vptrofs i).
+Proof.
+  unfold Vptrofs; intros. destruct Archi.ptr64; auto. 
+Qed.
+
+Hint Resolve inject_ptrofs.
+
 Section VAL_INJ_OPS.
 
 Variable f: meminj.
@@ -1534,7 +1890,7 @@ Lemma load_result_inject:
   inject f v1 v2 ->
   inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
 Proof.
-  intros. inv H; destruct chunk; simpl; econstructor; eauto.
+  intros. inv H; destruct chunk; simpl; try constructor; destruct Archi.ptr64; econstructor; eauto. 
 Qed.
 
 Remark add_inject:
@@ -1543,9 +1899,13 @@ Remark add_inject:
   inject f v2 v2' ->
   inject f (Val.add v1 v2) (Val.add v1' v2').
 Proof.
-  intros. inv H; inv H0; simpl; econstructor; eauto.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  intros. unfold Val.add. destruct Archi.ptr64 eqn:SF.
+- inv H; inv H0; constructor. 
+- inv H; inv H0; simpl; auto.
++ econstructor; eauto. 
+  rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
++ econstructor; eauto. 
+  rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
 Qed.
 
 Remark sub_inject:
@@ -1554,10 +1914,52 @@ Remark sub_inject:
   inject f v2 v2' ->
   inject f (Val.sub v1 v2) (Val.sub v1' v2').
 Proof.
-  intros. inv H; inv H0; simpl; auto.
-  econstructor; eauto. rewrite Int.sub_add_l. auto.
-  destruct (eq_block b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite dec_eq_true.
-  rewrite Int.sub_shifted. auto.
+  intros. unfold Val.sub. destruct Archi.ptr64 eqn:SF.
+- inv H; inv H0; constructor.
+- inv H; inv H0; simpl; auto.
++ econstructor; eauto. 
+  rewrite Ptrofs.sub_add_l. auto.
++ destruct (eq_block b1 b0); auto.
+  subst. rewrite H1 in H. inv H. rewrite dec_eq_true.
+  rewrite Ptrofs.sub_shifted. auto.
+Qed.
+
+Remark addl_inject:
+  forall v1 v1' v2 v2',
+  inject f v1 v1' ->
+  inject f v2 v2' ->
+  inject f (Val.addl v1 v2) (Val.addl v1' v2').
+Proof.
+  intros. unfold Val.addl. destruct Archi.ptr64 eqn:SF.
+- inv H; inv H0; simpl; auto.
++ econstructor; eauto. 
+  rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
++ econstructor; eauto. 
+  rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
+- inv H; inv H0; constructor. 
+Qed.
+
+Remark subl_inject:
+  forall v1 v1' v2 v2',
+  inject f v1 v1' ->
+  inject f v2 v2' ->
+  inject f (Val.subl v1 v2) (Val.subl v1' v2').
+Proof.
+  intros. unfold Val.subl. destruct Archi.ptr64 eqn:SF.
+- inv H; inv H0; simpl; auto.
++ econstructor; eauto. 
+  rewrite Ptrofs.sub_add_l. auto.
++ destruct (eq_block b1 b0); auto.
+  subst. rewrite H1 in H. inv H. rewrite dec_eq_true.
+  rewrite Ptrofs.sub_shifted. auto.
+- inv H; inv H0; constructor.
+Qed.
+
+Lemma offset_ptr_inject:
+  forall v v' ofs, inject f v v' -> inject f (offset_ptr v ofs) (offset_ptr v' ofs).
+Proof.
+  intros. inv H; simpl; econstructor; eauto.
+  rewrite ! Ptrofs.add_assoc. f_equal. apply Ptrofs.add_commut.
 Qed.
 
 Lemma cmp_bool_inject:
@@ -1578,30 +1980,30 @@ Let weak_valid_ptr2 b ofs := valid_ptr2 b ofs || valid_ptr2 b (ofs - 1).
 Hypothesis valid_ptr_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  valid_ptr1 b1 (Int.unsigned ofs) = true ->
-  valid_ptr2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+  valid_ptr1 b1 (Ptrofs.unsigned ofs) = true ->
+  valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
 
 Hypothesis weak_valid_ptr_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  weak_valid_ptr1 b1 (Int.unsigned ofs) = true ->
-  weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+  weak_valid_ptr1 b1 (Ptrofs.unsigned ofs) = true ->
+  weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
 
 Hypothesis weak_valid_ptr_no_overflow:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  weak_valid_ptr1 b1 (Int.unsigned ofs) = true ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+  weak_valid_ptr1 b1 (Ptrofs.unsigned ofs) = true ->
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 
 Hypothesis valid_different_ptrs_inj:
   forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
   b1 <> b2 ->
-  valid_ptr1 b1 (Int.unsigned ofs1) = true ->
-  valid_ptr1 b2 (Int.unsigned ofs2) = true ->
+  valid_ptr1 b1 (Ptrofs.unsigned ofs1) = true ->
+  valid_ptr1 b2 (Ptrofs.unsigned ofs2) = true ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
   b1' <> b2' \/
-  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).
 
 Lemma cmpu_bool_inject:
   forall c v1 v2 v1' v2' b,
@@ -1610,38 +2012,84 @@ Lemma cmpu_bool_inject:
   Val.cmpu_bool valid_ptr1 c v1 v2 = Some b ->
   Val.cmpu_bool valid_ptr2 c v1' v2' = Some b.
 Proof.
-  Local Opaque Int.add.
-  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
-  fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+  Local Opaque Int.add Ptrofs.add.
+  intros.
+  unfold cmpu_bool in *; destruct Archi.ptr64; 
+  inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
+- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))).
   destruct (Int.eq i Int.zero); auto.
-  destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate.
+  destruct (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:E; try discriminate.
   erewrite weak_valid_ptr_inj by eauto. auto.
-- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
-  fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))).
   destruct (Int.eq i Int.zero); auto.
-  destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate.
+  destruct (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:E; try discriminate.
+  erewrite weak_valid_ptr_inj by eauto. auto.
+- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs0)) in H1.
+  fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))).
+  fold (weak_valid_ptr2 b3 (Ptrofs.unsigned (Ptrofs.add ofs0 (Ptrofs.repr delta0)))).
+  destruct (eq_block b1 b0); subst.
+  rewrite H in H2. inv H2. rewrite dec_eq_true.
+  destruct (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs0)) eqn:?; try discriminate.
+  erewrite !weak_valid_ptr_inj by eauto. simpl.
+  rewrite <-H1. simpl. decEq. apply Ptrofs.translate_cmpu; eauto.
+  destruct (valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (valid_ptr1 b0 (Ptrofs.unsigned ofs0)) eqn:?; try discriminate.
+  destruct (eq_block b2 b3); subst.
+  assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true).
+    intros. unfold weak_valid_ptr1. rewrite H0; auto.
+  erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl.
+  exploit valid_different_ptrs_inj; eauto. intros [?|?]; [congruence |].
+  destruct c; simpl in H1; inv H1.
+  simpl; decEq. rewrite Ptrofs.eq_false; auto. congruence.
+  simpl; decEq. rewrite Ptrofs.eq_false; auto. congruence.
+  now erewrite !valid_ptr_inj by eauto.
+Qed.
+
+Lemma cmplu_bool_inject:
+  forall c v1 v2 v1' v2' b,
+  inject f v1 v1' ->
+  inject f v2 v2' ->
+  Val.cmplu_bool valid_ptr1 c v1 v2 = Some b ->
+  Val.cmplu_bool valid_ptr2 c v1' v2' = Some b.
+Proof.
+  Local Opaque Int64.add Ptrofs.add.
+  intros.
+  unfold cmplu_bool in *; destruct Archi.ptr64;
+  inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
+- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))).
+  destruct (Int64.eq i Int64.zero); auto.
+  destruct (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:E; try discriminate.
+  erewrite weak_valid_ptr_inj by eauto. auto.
+- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))).
+  destruct (Int64.eq i Int64.zero); auto.
+  destruct (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:E; try discriminate.
   erewrite weak_valid_ptr_inj by eauto. auto.
-- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
-  fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1.
-  fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
-  fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))).
+- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs0)) in H1.
+  fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))).
+  fold (weak_valid_ptr2 b3 (Ptrofs.unsigned (Ptrofs.add ofs0 (Ptrofs.repr delta0)))).
   destruct (eq_block b1 b0); subst.
   rewrite H in H2. inv H2. rewrite dec_eq_true.
-  destruct (weak_valid_ptr1 b0 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (weak_valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+  destruct (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs0)) eqn:?; try discriminate.
   erewrite !weak_valid_ptr_inj by eauto. simpl.
-  rewrite <-H1. simpl. decEq. apply Int.translate_cmpu; eauto.
-  destruct (valid_ptr1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+  rewrite <-H1. simpl. decEq. apply Ptrofs.translate_cmpu; eauto.
+  destruct (valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (valid_ptr1 b0 (Ptrofs.unsigned ofs0)) eqn:?; try discriminate.
   destruct (eq_block b2 b3); subst.
   assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true).
     intros. unfold weak_valid_ptr1. rewrite H0; auto.
   erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl.
   exploit valid_different_ptrs_inj; eauto. intros [?|?]; [congruence |].
   destruct c; simpl in H1; inv H1.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
+  simpl; decEq. rewrite Ptrofs.eq_false; auto. congruence.
+  simpl; decEq. rewrite Ptrofs.eq_false; auto. congruence.
   now erewrite !valid_ptr_inj by eauto.
 Qed.
 
@@ -1710,8 +2158,8 @@ Lemma val_inject_lessdef:
   forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2.
 Proof.
   intros; split; intros.
-  inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto.
-  inv H; auto. inv H0. rewrite Int.add_zero; auto.
+  inv H; auto. destruct v2; econstructor; eauto. rewrite Ptrofs.add_zero; auto.
+  inv H; auto. inv H0. rewrite Ptrofs.add_zero; auto.
 Qed.
 
 Lemma val_inject_list_lessdef:
@@ -1732,8 +2180,8 @@ Lemma val_inject_id:
 Proof.
   intros; split; intros.
   inv H; auto.
-  unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor.
-  inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto.
+  unfold inject_id in H0. inv H0. rewrite Ptrofs.add_zero. constructor.
+  inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Ptrofs.add_zero; auto.
   constructor.
 Qed.
 
@@ -1757,5 +2205,5 @@ Lemma val_inject_compose:
 Proof.
   intros. inv H; auto; inv H0; auto. econstructor.
   unfold compose_meminj; rewrite H1; rewrite H3; eauto.
-  rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints.
+  rewrite Ptrofs.add_assoc. decEq. unfold Ptrofs.add. apply Ptrofs.eqm_samerepr. auto with ints.
 Qed.