Merge of the "princeton" branch:

- Define type "block" as "positive" instead of "Z".
- Strengthen mem_unchanged_on so that the permissions are identical,
  instead of possibly increasing.
- Move mem_unchanged_on from Events to Memory.Mem.
- Define it in terms of mem_contents rather than in terms of Mem.load.
- ExportClight: try to name temporaries introduced by SimplExpr
- SimplExpr: avoid reusing temporaries between different functions,
  instead, thread a single generator through all functions.


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

5 files changed, 689 insertions, 613 deletions

diff --git a/common/Events.v b/common/Events.v
index be1915a..3082503 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -582,14 +582,6 @@ Definition extcall_sem : Type :=
 
 (** We now specify the expected properties of this predicate. *)
 
-Definition mem_unchanged_on (P: block -> Z -> Prop) (m_before m_after: mem): Prop :=
-  (forall b ofs k p,
-   P b ofs -> Mem.perm m_before b ofs k p -> Mem.perm m_after b ofs k p)
-/\(forall chunk b ofs v,
-   (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) ->
-   Mem.load chunk m_before b ofs = Some v ->
-   Mem.load chunk m_after b ofs = Some v).
-
 Definition loc_out_of_bounds (m: mem) (b: block) (ofs: Z) : Prop :=
   ~Mem.perm m b ofs Max Nonempty.
 
@@ -663,7 +655,7 @@ Record extcall_properties (sem: extcall_sem)
        sem F V ge vargs' m1' t vres' m2'
     /\ Val.lessdef vres vres'
     /\ Mem.extends m2 m2'
-    /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2';
+    /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2';
 
 (** External calls must commute with memory injections,
   in the following sense. *)
@@ -677,8 +669,8 @@ Record extcall_properties (sem: extcall_sem)
        sem F V ge vargs' m1' t vres' m2'
     /\ val_inject f' vres vres'
     /\ Mem.inject f' m2 m2'
-    /\ mem_unchanged_on (loc_unmapped f) m1 m2
-    /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2'
+    /\ Mem.unchanged_on (loc_unmapped f) m1 m2
+    /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
     /\ inject_incr f f'
     /\ inject_separated f f' m1 m1';
 
@@ -797,12 +789,12 @@ Proof.
 (* mem extends *)
   inv H. inv H1. inv H6. inv H4. 
   exploit volatile_load_extends; eauto. intros [v' [A B]].
-  exists v'; exists m1'; intuition. constructor; auto. red; auto.
+  exists v'; exists m1'; intuition. constructor; auto.
 (* mem injects *)
   inv H0. inv H2. inv H7. inversion H5; subst. 
   exploit volatile_load_inject; eauto. intros [v' [A B]]. 
   exists f; exists v'; exists m1'; intuition. constructor; auto.
-  red; auto. red; auto. red; intros. congruence.
+  red; intros. congruence.
 (* trace length *)
   inv H; inv H0; simpl; omega.
 (* receptive *)
@@ -821,7 +813,6 @@ Proof.
   split. constructor. intuition congruence.
 Qed.
 
-
 Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int)
                                    (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
@@ -861,14 +852,14 @@ Proof.
   inv H; auto.
 (* extends *)
   inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]].
-  exists v'; exists m1'; intuition. econstructor; eauto. red; auto.
+  exists v'; exists m1'; intuition. econstructor; eauto.
 (* inject *)
   inv H0. inv H2.
   assert (val_inject f (Vptr b ofs) (Vptr b ofs)). 
     exploit (proj1 H); eauto. intros EQ. econstructor. eauto. rewrite Int.add_zero; auto.
   exploit volatile_load_inject; eauto. intros [v' [A B]].
   exists f; exists v'; exists m1'; intuition. econstructor; eauto. 
-  red; auto. red; auto. red; intros; congruence. 
+  red; intros; congruence. 
 (* trace length *)
   inv H; inv H1; simpl; omega.
 (* receptive *)
@@ -933,25 +924,20 @@ Lemma volatile_store_extends:
   exists m2', 
      volatile_store ge chunk m1' b ofs v' t m2'
   /\ Mem.extends m2 m2'
-  /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'.
+  /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'.
 Proof.
   intros. inv H.
-  econstructor; split. econstructor; eauto. eapply eventval_match_lessdef; eauto.
-  split. auto. red; auto.
-  exploit Mem.store_within_extends; eauto. intros [m2' [A B]].
-  exists m2'; intuition. econstructor; eauto. 
-  red; split; intros.
-  eapply Mem.perm_store_1; eauto.
-  rewrite <- H4. eapply Mem.load_store_other; eauto.
-  destruct (eq_block b0 b); auto. subst b0; right. 
-  apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
-                              (Int.unsigned ofs, Int.unsigned ofs + size_chunk chunk)).
-  red; intros; red; intros.
-  exploit (H x H5). exploit Mem.store_valid_access_3. eexact H3. intros [E G].
-  apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
-  auto.
-  simpl. generalize (size_chunk_pos chunk0). omega.
-  simpl. generalize (size_chunk_pos chunk). omega.
+- econstructor; split. econstructor; eauto. eapply eventval_match_lessdef; eauto.
+  auto with mem.
+- exploit Mem.store_within_extends; eauto. intros [m2' [A B]].
+  exists m2'; intuition.
++ econstructor; eauto.
++ eapply Mem.store_unchanged_on; eauto. 
+  unfold loc_out_of_bounds; intros.
+  assert (Mem.perm m1 b i Max Nonempty).
+  { apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
+    exploit Mem.store_valid_access_3. eexact H3. intros [P Q]. eauto. }
+  tauto.
 Qed.
 
 Lemma volatile_store_inject:
@@ -964,37 +950,28 @@ Lemma volatile_store_inject:
   exists m2',
        volatile_store ge chunk m1' b' ofs' v' t m2'
     /\ Mem.inject f m2 m2'
-    /\ mem_unchanged_on (loc_unmapped f) m1 m2
-    /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2'.
+    /\ Mem.unchanged_on (loc_unmapped f) m1 m2
+    /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'.
 Proof.
   intros. inv H0.
-  inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ.
-  rewrite Int.add_zero. exists m1'.
-  split. constructor; auto.  eapply eventval_match_inject; eauto.
-  split. auto. split. red; auto. red; auto. 
-  assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto.
+- inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ.
+  rewrite Int.add_zero. exists m1'. intuition. 
+  constructor; auto.  eapply eventval_match_inject; eauto.
+- assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto.
   exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]].
   inv H1. exists m2'; intuition. 
-  constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto.  
-  split; intros. eapply Mem.perm_store_1; eauto.
-  rewrite <- H6. eapply Mem.load_store_other; eauto. 
-  left. exploit (H1 ofs0). generalize (size_chunk_pos chunk0). omega. 
-  unfold loc_unmapped. congruence.
-  split; intros. eapply Mem.perm_store_1; eauto.
-  rewrite <- H6. eapply Mem.load_store_other; eauto.
-  destruct (eq_block b0 b'); auto. subst b0; right.
-  assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta).
-    eapply Mem.address_inject; eauto with mem.
-  unfold Mem.storev in A. rewrite EQ in A. rewrite EQ.
-  apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
-                              (Int.unsigned ofs + delta, Int.unsigned ofs + delta + size_chunk chunk)).
-  red; intros; red; intros. exploit (H1 x H7). eauto.
-  exploit Mem.store_valid_access_3. eexact H0. intros [C D].
-  apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
-  apply C. red in H8; simpl in H8. omega. 
-  auto.
-  simpl. generalize (size_chunk_pos chunk0). omega.
-  simpl. generalize (size_chunk_pos chunk). omega.
++ constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto.  
++ eapply Mem.store_unchanged_on; eauto.
+  unfold loc_unmapped; intros. 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)
+  by (eapply Mem.address_inject; eauto with mem).
+  rewrite EQ in *.
+  eelim H6; eauto. 
+  exploit Mem.store_valid_access_3. eexact H5. intros [P Q]. 
+  apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. 
+  apply P. omega.
 Qed.
 
 Lemma volatile_store_receptive:
@@ -1120,13 +1097,15 @@ Proof.
     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'' ->
-    mem_unchanged_on P m m'').
-  intros; split; intros.
-  eauto with mem.
-  transitivity (Mem.load chunk m' b0 ofs). 
-  eapply Mem.load_store_other; eauto. left. 
-  apply Mem.valid_not_valid_diff with m; eauto with mem.
-  eapply Mem.load_alloc_other; eauto. 
+    Mem.unchanged_on P m m'').
+  {
+    intros; constructor; intros.
+  - split; intros; eauto with mem.
+  - assert (b0 <> b) by (eapply Mem.valid_not_valid_diff; eauto with mem).
+    erewrite Mem.store_mem_contents; eauto. rewrite Maps.PMap.gso by auto.
+    Local Transparent Mem.alloc. unfold Mem.alloc in H. injection H; intros A B.
+    rewrite <- B; simpl. rewrite A. rewrite Maps.PMap.gso by auto. auto.
+  } 
 
   constructor; intros.
 (* well typed *)
@@ -1139,7 +1118,7 @@ Proof.
   inv H. eauto with mem.
 (* perms *)
   inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto.
-  rewrite zeq_false. auto. 
+  rewrite dec_eq_false. auto. 
   apply Mem.valid_not_valid_diff with m1; eauto with mem.
 (* readonly *)
   inv H. transitivity (Mem.load chunk m' b ofs).
@@ -1194,6 +1173,7 @@ Lemma extcall_free_ok:
   extcall_properties extcall_free_sem 
                      (mksignature (Tint :: nil) None).
 Proof.
+(*
   assert (UNCHANGED:
     forall (P: block -> Z -> Prop) m b lo hi m',
     Mem.free m b lo hi = Some m' ->
@@ -1201,13 +1181,16 @@ Proof.
     (forall b' ofs, P b' ofs -> b' <> b \/ ofs < lo \/ hi <= ofs) ->
     mem_unchanged_on P m m').
   intros; split; intros.
+  split; intros.
   eapply Mem.perm_free_1; eauto.
+  eapply Mem.perm_free_3; eauto.
   rewrite <- H3. eapply Mem.load_free; eauto. 
   destruct (eq_block b0 b); auto. right. right. 
   apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) (lo, hi)).
   red; intros. apply Intv.notin_range. simpl. exploit H1; eauto. intuition. 
   simpl; generalize (size_chunk_pos chunk); omega.
   simpl; omega.
+*)
 
   constructor; intros.
 (* well typed *)
@@ -1239,12 +1222,12 @@ Proof.
   exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]].
   exists Vundef; exists m2'; intuition.
   econstructor; eauto.
-  eapply UNCHANGED; eauto. omega. 
-  intros. destruct (eq_block b' b); auto. subst b; right.
-  assert (~(Int.unsigned lo - 4 <= ofs < Int.unsigned lo + Int.unsigned sz)).
-    red; intros; elim H. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-    eapply Mem.free_range_perm. eexact H4. auto. 
-  omega.
+  eapply Mem.free_unchanged_on; eauto. 
+  unfold loc_out_of_bounds; intros. 
+  assert (Mem.perm m1 b i Max Nonempty).
+  { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. 
+    eapply Mem.free_range_perm. eexact H4. eauto. }
+  tauto.
 (* mem inject *)
   inv H0. inv H2. inv H7. inv H9.
   exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. 
@@ -1278,18 +1261,15 @@ Proof.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
   apply H0. omega.
   eapply Mem.perm_max. eauto with mem.
-  unfold block; omega.
+  intuition. 
 
-  eapply UNCHANGED; eauto. omega. intros.  
-  red in H7. left. congruence. 
+  eapply Mem.free_unchanged_on; eauto. 
+  unfold loc_unmapped; intros. congruence.
 
-  eapply UNCHANGED; eauto. omega. intros.
-  destruct (eq_block b' b2); auto. subst b'. right.
-  assert (~(Int.unsigned lo + delta - 4 <= ofs < Int.unsigned lo + delta + Int.unsigned sz)).
-    red; intros. elim (H7 _ _ H6). 
-    apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-    apply H0. omega.
-  omega.
+  eapply Mem.free_unchanged_on; eauto. 
+  unfold loc_out_of_reach; intros. red; intros. eelim H8; eauto. 
+  apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
+  apply H0. omega.
 
   red; intros. congruence.
 (* trace length *)
@@ -1351,21 +1331,12 @@ Proof.
   split. econstructor; eauto.
   split. constructor.
   split. auto.
-  red; split; intros.
-  eauto with mem.  
-  exploit Mem.loadbytes_length. eexact H8. intros.
-  rewrite <- H1. eapply Mem.load_storebytes_other; eauto. 
-  destruct (eq_block b bdst); auto. subst b; right.
-  exploit list_forall2_length; eauto. intros R. 
-  apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk)
-                              (Int.unsigned odst, Int.unsigned odst + Z_of_nat (length bytes2))); simpl.
-  red; unfold Intv.In; simpl; intros; red; intros.
-  eapply (H x H11).
+  eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_bounds; intros. 
+  assert (Mem.perm m1 bdst i Max Nonempty).
   apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
-  eapply Mem.storebytes_range_perm. eexact H9.
-  rewrite R. auto. 
-  generalize (size_chunk_pos chunk). omega.
-  rewrite <- R. rewrite H10. rewrite nat_of_Z_eq. omega. omega.
+  eapply Mem.storebytes_range_perm; eauto. 
+  erewrite list_forall2_length; eauto. 
+  tauto.
 (* injections *)
   intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12.
   exploit Mem.loadbytes_length; eauto. intros LEN.
@@ -1392,20 +1363,13 @@ Proof.
   apply Mem.range_perm_max with Cur; auto.
   split. constructor.
   split. auto.
-  split. red; split; intros. eauto with mem. 
-  rewrite <- H2. eapply Mem.load_storebytes_other; eauto. 
-  destruct (eq_block b bdst); auto. subst b. 
-  assert (loc_unmapped f bdst ofs). apply H0. generalize (size_chunk_pos chunk); omega. 
-  red in H12. congruence.
-  split. red; split; intros. eauto with mem.
-  rewrite <- H2. eapply Mem.load_storebytes_other; eauto. 
-  destruct (eq_block b b0); auto. subst b0; right.
-  rewrite <- (list_forall2_length B). rewrite LEN. rewrite nat_of_Z_eq; try omega.
-  apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk)
-                              (Int.unsigned odst + delta0, Int.unsigned odst + delta0 + sz)); simpl.
-  red; unfold Intv.In; simpl; intros; red; intros.
-  eapply (H0 x H12). eauto. apply Mem.perm_cur_max. apply RPDST. omega. 
-  generalize (size_chunk_pos chunk); omega.
+  split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros.
+  congruence.
+  split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros.
+  eelim H2; eauto. 
+  apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
+  eapply Mem.storebytes_range_perm; eauto. 
+  erewrite list_forall2_length; eauto. 
   omega.
   split. apply inject_incr_refl.
   red; intros; congruence.
@@ -1452,15 +1416,12 @@ Proof.
   exists vres; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_list_match_lessdef; eauto.
-  red; auto.
 (* mem injects *)
   inv H0.
   exists f; exists vres; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_list_match_inject; eauto.
   eapply eventval_match_inject_2; eauto.
-  red; auto.
-  red; auto.
   red; intros; congruence.
 (* trace length *)
   inv H; simpl; omega.
@@ -1518,14 +1479,11 @@ Proof.
   exists Vundef; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_list_match_lessdef; eauto.
-  red; auto.
 (* mem injects *)
   inv H0.
   exists f; exists Vundef; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_list_match_inject; eauto.
-  red; auto.
-  red; auto.
   red; intros; congruence.
 (* trace length *)
   inv H; simpl; omega.
@@ -1567,14 +1525,11 @@ Proof.
   exists v2; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_match_lessdef; eauto.
-  red; auto.
 
   inv H0. inv H2. inv H7.
   exists f; exists v'; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_match_inject; eauto.
-  red; auto.
-  red; auto.
   red; intros; congruence.
 
   inv H; simpl; omega.
@@ -1687,12 +1642,12 @@ Qed.
 Lemma external_call_nextblock:
   forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2,
   external_call ef ge vargs m1 t vres m2 ->
-  Mem.nextblock m1 <= Mem.nextblock m2.
+  Ple (Mem.nextblock m1) (Mem.nextblock m2).
 Proof.
-  intros. 
-  exploit external_call_valid_block; eauto. 
-  instantiate (1 := Mem.nextblock m1 - 1). red; omega.
-  unfold Mem.valid_block. omega.
+  intros. destruct (plt (Mem.nextblock m2) (Mem.nextblock m1)).
+  exploit external_call_valid_block; eauto. intros.
+  eelim Plt_strict; eauto.
+  unfold Plt, Ple in *; zify; omega.
 Qed.
 
 (** Corollaries of [external_call_determ]. *)
@@ -1822,6 +1777,14 @@ Proof.
   intros. inv H. eapply external_call_valid_block; eauto.
 Qed.
 
+Lemma external_call_nextblock':
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2,
+  external_call' ef ge vargs m1 t vres m2 ->
+  Ple (Mem.nextblock m1) (Mem.nextblock m2).
+Proof.
+  intros. inv H. eapply external_call_nextblock; eauto.
+Qed.
+
 Lemma external_call_mem_extends':
   forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2 m1' vargs',
   external_call' ef ge vargs m1 t vres m2 ->
@@ -1831,7 +1794,7 @@ Lemma external_call_mem_extends':
      external_call' ef ge vargs' m1' t vres' m2'
   /\ Val.lessdef_list vres vres'
   /\ Mem.extends m2 m2'
-  /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'.
+  /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'.
 Proof.
   intros. inv H. 
   exploit external_call_mem_extends; eauto.
@@ -1852,8 +1815,8 @@ Lemma external_call_mem_inject':
      external_call' ef ge vargs' m1' t vres' m2'
   /\ val_list_inject f' vres vres'
   /\ Mem.inject f' m2 m2'
-  /\ mem_unchanged_on (loc_unmapped f) m1 m2
-  /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2'
+  /\ Mem.unchanged_on (loc_unmapped f) m1 m2
+  /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
   /\ inject_incr f f'
   /\ inject_separated f f' m1 m1'.
 Proof.
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index a082819..4e155e3 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -83,15 +83,14 @@ Variable V: Type.  (**r The type of information attached to variables *)
 
 Record t: Type := mkgenv {
   genv_symb: PTree.t block;             (**r mapping symbol -> block *)
-  genv_funs: ZMap.t (option F);         (**r mapping function pointer -> definition *)
-  genv_vars: ZMap.t (option (globvar V)); (**r mapping variable pointer -> info *)
+  genv_funs: PTree.t F;                 (**r mapping function pointer -> definition *)
+  genv_vars: PTree.t (globvar V);       (**r mapping variable pointer -> info *)
   genv_next: block;                     (**r next symbol pointer *)
-  genv_next_pos: genv_next > 0;
-  genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> 0 < b < genv_next;
-  genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> 0 < b < genv_next;
-  genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_next;
+  genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> Plt b genv_next;
+  genv_funs_range: forall b f, PTree.get b genv_funs = Some f -> Plt b genv_next;
+  genv_vars_range: forall b v, PTree.get b genv_vars = Some v -> Plt b genv_next;
   genv_funs_vars: forall b1 b2 f v,
-    ZMap.get b1 genv_funs = Some f -> ZMap.get b2 genv_vars = Some v -> b1 <> b2;
+    PTree.get b1 genv_funs = Some f -> PTree.get b2 genv_vars = Some v -> b1 <> b2;
   genv_vars_inj: forall id1 id2 b, 
     PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2
 }.
@@ -107,7 +106,7 @@ Definition find_symbol (ge: t) (id: ident) : option block :=
     the given address. *)
 
 Definition find_funct_ptr (ge: t) (b: block) : option F :=
-  ZMap.get b ge.(genv_funs).
+  PTree.get b ge.(genv_funs).
 
 (** [find_funct] is similar to [find_funct_ptr], but the function address
     is given as a value, which must be a pointer with offset 0. *)
@@ -129,7 +128,7 @@ Definition invert_symbol (ge: t) (b: block) : option ident :=
    at address [b]. *)
 
 Definition find_var_info (ge: t) (b: block) : option (globvar V) :=
-  ZMap.get b ge.(genv_vars).
+  PTree.get b ge.(genv_vars).
 
 (** ** Constructing the global environment *)
 
@@ -137,48 +136,46 @@ Program Definition add_global (ge: t) (idg: ident * globdef F V) : t :=
   @mkgenv
     (PTree.set idg#1 ge.(genv_next) ge.(genv_symb))
     (match idg#2 with
-     | Gfun f => ZMap.set ge.(genv_next) (Some f) ge.(genv_funs)
+     | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs)
      | Gvar v => ge.(genv_funs)
      end)
     (match idg#2 with
      | Gfun f => ge.(genv_vars)
-     | Gvar v => ZMap.set ge.(genv_next) (Some v) ge.(genv_vars)
+     | Gvar v => PTree.set ge.(genv_next) v ge.(genv_vars)
      end)
-    (ge.(genv_next) + 1)
-    _ _ _ _ _ _.
-Next Obligation.
-  destruct ge; simpl; omega.
-Qed.
+    (Psucc ge.(genv_next))
+    _ _ _ _ _.
 Next Obligation.
   destruct ge; simpl in *.
-  rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega.
-  exploit genv_symb_range0; eauto. unfold block; omega.
+  rewrite PTree.gsspec in H. destruct (peq id i). inv H. apply Plt_succ.
+  apply Plt_trans_succ; eauto.
 Qed.
 Next Obligation.
   destruct ge; simpl in *. 
   destruct g. 
-  rewrite ZMap.gsspec in H. 
-  destruct (ZIndexed.eq b genv_next0). subst; omega. 
-  exploit genv_funs_range0; eauto. omega.
-  exploit genv_funs_range0; eauto. omega.
+  rewrite PTree.gsspec in H. 
+  destruct (peq b genv_next0). inv H. apply Plt_succ.
+  apply Plt_trans_succ; eauto.
+  apply Plt_trans_succ; eauto.
 Qed.
 Next Obligation.
   destruct ge; simpl in *. 
-  destruct g. 
-  exploit genv_vars_range0; eauto. omega.
-  rewrite ZMap.gsspec in H. 
-  destruct (ZIndexed.eq b genv_next0). subst; omega. 
-  exploit genv_vars_range0; eauto. omega.
+  destruct g.
+  apply Plt_trans_succ; eauto.
+  rewrite PTree.gsspec in H. 
+  destruct (peq b genv_next0). inv H. apply Plt_succ.
+  apply Plt_trans_succ; eauto.
 Qed.
 Next Obligation.
-  destruct ge; simpl in *. destruct g.
-  rewrite ZMap.gsspec in H.
-  destruct (ZIndexed.eq b1 genv_next0). inv H. 
-  exploit genv_vars_range0; eauto. unfold ZIndexed.t; omega.
+  destruct ge; simpl in *.
+  destruct g.
+  rewrite PTree.gsspec in H.
+  destruct (peq b1 genv_next0). inv H.
+  apply sym_not_equal; apply Plt_ne; eauto.
   eauto.
-  rewrite ZMap.gsspec in H0.
-  destruct (ZIndexed.eq b2 genv_next0). inv H. 
-  exploit genv_funs_range0; eauto. unfold ZIndexed.t; omega.
+  rewrite PTree.gsspec in H0.
+  destruct (peq b2 genv_next0). inv H0.
+  apply Plt_ne; eauto.
   eauto.
 Qed.
 Next Obligation.
@@ -186,8 +183,8 @@ Next Obligation.
   rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. 
   destruct (peq id1 i); destruct (peq id2 i).
   congruence.
-  exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction.
-  exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction.
+  inv H. eelim Plt_strict. eapply genv_symb_range0; eauto.
+  inv H0. eelim Plt_strict. eapply genv_symb_range0; eauto.
   eauto.
 Qed.
 
@@ -202,21 +199,18 @@ Proof.
 Qed.
 
 Program Definition empty_genv : t :=
-  @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) 1 _ _ _ _ _ _.
-Next Obligation.
-  omega.
-Qed.
+  @mkgenv (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _.
 Next Obligation.
   rewrite PTree.gempty in H. discriminate.
 Qed.
 Next Obligation.
-  rewrite ZMap.gi in H. discriminate.
+  rewrite PTree.gempty in H. discriminate.
 Qed.
 Next Obligation.
-  rewrite ZMap.gi in H. discriminate.
+  rewrite PTree.gempty in H. discriminate.
 Qed.
 Next Obligation.
-  rewrite ZMap.gi in H. discriminate.
+  rewrite PTree.gempty in H. discriminate.
 Qed.
 Next Obligation.
   rewrite PTree.gempty in H. discriminate.
@@ -317,12 +311,12 @@ Proof.
   intros. unfold find_symbol, find_funct_ptr in *; simpl.
   destruct H1 as [b [A B]]. exists b; split.
   rewrite PTree.gso; auto.
-  destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. 
-  exploit genv_funs_range; eauto. unfold ZIndexed.t; omega.
+  destruct g1 as [f1 | v1]. rewrite PTree.gso. auto.
+  apply Plt_ne. eapply genv_funs_range; eauto.
   auto. 
 (* ensures *)
   intros. unfold find_symbol, find_funct_ptr in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. 
+  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss.
 Qed.
 
 Theorem find_var_exists:
@@ -338,11 +332,11 @@ Proof.
   intros. unfold find_symbol, find_var_info in *; simpl.
   destruct H1 as [b [A B]]. exists b; split.
   rewrite PTree.gso; auto.
-  destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. 
-  exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
+  destruct g1 as [f1 | v1]. auto. rewrite PTree.gso. auto.
+  apply Plt_ne. eapply genv_vars_range; eauto.
 (* ensures *)
   intros. unfold find_symbol, find_var_info in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. 
+  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. 
 Qed.
 
 Lemma find_symbol_inversion : forall p x b,
@@ -366,11 +360,11 @@ Proof.
   intros until f. unfold globalenv. apply add_globals_preserves. 
 (* preserves *)
   unfold find_funct_ptr; simpl; intros. destruct g; auto. 
-  rewrite ZMap.gsspec in H1. destruct (ZIndexed.eq b (genv_next ge)).
+  rewrite PTree.gsspec in H1. destruct (peq b (genv_next ge)).
   inv H1. exists id; auto.
   auto.
 (* base *)
-  unfold find_funct_ptr; simpl; intros. rewrite ZMap.gi in H. discriminate.
+  unfold find_funct_ptr; simpl; intros. rewrite PTree.gempty in H. discriminate.
 Qed.
 
 Theorem find_funct_inversion:
@@ -410,22 +404,15 @@ Proof.
   intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves. 
 (* preserves *)
   intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0). 
-  inv H1. destruct g as [f1|v1]. rewrite ZMap.gss in H2. inv H2. auto. 
-  exploit genv_funs_range; eauto. intros. omegaContradiction.
-  destruct g as [f1|v1]. rewrite ZMap.gso in H2. auto. 
-  exploit genv_symb_range; eauto. unfold ZIndexed.t; omega. 
+  inv H1. destruct g as [f1|v1]. rewrite PTree.gss in H2. inv H2. auto.
+  eelim Plt_strict. eapply genv_funs_range; eauto.
+  destruct g as [f1|v1]. rewrite PTree.gso in H2. auto.
+  apply Plt_ne. eapply genv_symb_range; eauto.
   auto.
 (* initial *)
   intros. simpl in *. rewrite PTree.gempty in H. discriminate.
 Qed.
 
-Theorem find_symbol_not_nullptr:
-  forall p id b,
-  find_symbol (globalenv p) id = Some b -> b <> Mem.nullptr.
-Proof.
-  intros until b. unfold find_symbol. destruct (globalenv p); simpl. 
-  intros. exploit genv_symb_range0; eauto. unfold Mem.nullptr, block. omega. 
-Qed.
 
 Theorem global_addresses_distinct:
   forall ge id1 id2 b1 b2,
@@ -470,14 +457,16 @@ Proof.
   congruence.
 Qed.
 
+Definition advance_next (gl: list (ident * globdef F V)) (x: positive) :=
+  List.fold_left (fun n g => Psucc n) gl x.
+
 Remark genv_next_add_globals:
   forall gl ge,
-  genv_next (add_globals ge gl) = genv_next ge + Z_of_nat (length gl).
+  genv_next (add_globals ge gl) = advance_next gl (genv_next ge).
 Proof.
-  induction gl; intros.
-  simpl. unfold block; omega.
-  simpl add_globals; simpl length; rewrite inj_S. 
-  rewrite IHgl. simpl. unfold block; omega.
+  induction gl; simpl; intros.
+  auto.
+  rewrite IHgl. auto. 
 Qed.
 
 (** * Construction of the initial memory state *)
@@ -609,7 +598,7 @@ Qed.
 Remark alloc_global_nextblock:
   forall g m m',
   alloc_global m g = Some m' ->
-  Mem.nextblock m' = Zsucc(Mem.nextblock m).
+  Mem.nextblock m' = Psucc(Mem.nextblock m).
 Proof.
   unfold alloc_global. intros.
   destruct g as [id [f|v]]. 
@@ -631,13 +620,12 @@ Qed.
 Remark alloc_globals_nextblock:
   forall gl m m',
   alloc_globals m gl = Some m' ->
-  Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length gl).
+  Mem.nextblock m' = advance_next gl (Mem.nextblock m).
 Proof.
-  induction gl.
-  simpl; intros. inv H; unfold block; omega.
-  simpl length; rewrite inj_S; simpl; intros.
+  induction gl; simpl; intros.
+  congruence.
   destruct (alloc_global m a) as [m1|] eqn:?; try discriminate.
-  erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. unfold block; omega.
+  erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto.
 Qed.
 
 (** Permissions *)
@@ -712,7 +700,8 @@ Proof.
   simpl; intros. inv H. tauto.
   simpl; intros. destruct (alloc_global m a) as [m1|] eqn:?; try discriminate.
   erewrite alloc_global_perm; eauto. eapply IHgl; eauto. 
-  unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega. 
+  unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto.
+  apply Plt_trans_succ; auto.
 Qed.
 
 (** Data preservation properties *)
@@ -727,8 +716,8 @@ Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
   inv H; auto.
   transitivity (Mem.load chunk m' b' p'). 
-  apply IHo. auto. unfold block in *; omega. 
-  eapply Mem.load_store_other; eauto. simpl. unfold block in *; omega.
+  apply IHo. auto. intuition omega. 
+  eapply Mem.load_store_other; eauto. simpl. intuition omega. 
   discriminate.
 Qed.
 
@@ -847,7 +836,8 @@ Proof.
   destruct (alloc_global m a) as [m''|] eqn:?; try discriminate.
   transitivity (Mem.load chunk m'' b p). 
   apply IHgl; auto. unfold Mem.valid_block in *. 
-  erewrite alloc_global_nextblock; eauto. omega.
+  erewrite alloc_global_nextblock; eauto. 
+  apply Plt_trans with (Mem.nextblock m); auto. apply Plt_succ.
   destruct a as [id g]. eapply load_alloc_global; eauto. 
 Qed.
 
@@ -894,14 +884,14 @@ Proof.
   red; intros. unfold find_var_info in H3. simpl in H3. 
   exploit H1; eauto. intros [A [B C]].
   assert (D: Mem.valid_block m b). 
-    red. exploit genv_vars_range; eauto. rewrite H; omega. 
+    red. exploit genv_vars_range; eauto. rewrite H; auto.
   split. red; intros. erewrite <- alloc_global_perm; eauto. 
   split. intros. eapply B. erewrite alloc_global_perm; eauto. 
   intros. apply load_store_init_data_invariant with m; auto. 
   intros. eapply load_alloc_global; eauto. 
 (* variable *)
-  red; intros. unfold find_var_info in H3. simpl in H3. rewrite ZMap.gsspec in H3.
-  destruct (ZIndexed.eq b (genv_next ge0)).
+  red; intros. unfold find_var_info in H3. simpl in H3. rewrite PTree.gsspec in H3.
+  destruct (peq b (genv_next ge0)).
   (* same *)
   inv H3. simpl in H0.
   set (init := gvar_init gv) in *.
@@ -927,7 +917,7 @@ Proof.
   (* older var *)
   exploit H1; eauto. intros [A [B C]].
   assert (D: Mem.valid_block m b). 
-    red. exploit genv_vars_range; eauto. rewrite H; omega. 
+    red. exploit genv_vars_range; eauto. rewrite H; auto. 
   split. red; intros. erewrite <- alloc_global_perm; eauto. 
   split. intros. eapply B. erewrite alloc_global_perm; eauto. 
   intros. apply load_store_init_data_invariant with m; auto. 
@@ -935,8 +925,8 @@ Proof.
 (* functions-initialized *)
   split. destruct g as [f|v].
 (* function *)
-  red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite ZMap.gsspec in H3.
-  destruct (ZIndexed.eq b (genv_next ge0)).
+  red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite PTree.gsspec in H3.
+  destruct (peq b (genv_next ge0)).
   (* same *)
   inv H3. simpl in H0. 
   destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. 
@@ -951,18 +941,18 @@ Proof.
   (* older function *)
   exploit H2; eauto. intros [A B].
   assert (D: Mem.valid_block m b). 
-    red. exploit genv_funs_range; eauto. rewrite H; omega. 
+    red. exploit genv_funs_range; eauto. rewrite H; auto.
   split. erewrite <- alloc_global_perm; eauto. 
   intros. eapply B. erewrite alloc_global_perm; eauto.
 (* variables *)
   red; intros. unfold find_funct_ptr in H3. simpl in H3. 
   exploit H2; eauto. intros [A B].
   assert (D: Mem.valid_block m b). 
-    red. exploit genv_funs_range; eauto. rewrite H; omega. 
+    red. exploit genv_funs_range; eauto. rewrite H; auto.
   split. erewrite <- alloc_global_perm; eauto. 
   intros. eapply B. erewrite alloc_global_perm; eauto.
 (* nextblock *)
-  rewrite NB. simpl. rewrite H. unfold block; omega. 
+  rewrite NB. simpl. rewrite H. auto.
 Qed.
 
 Lemma alloc_globals_initialized:
@@ -1001,7 +991,7 @@ Theorem find_symbol_not_fresh:
   find_symbol (globalenv p) id = Some b -> Mem.valid_block m b.
 Proof.
   intros. red. erewrite <- init_mem_genv_next; eauto. 
-  exploit genv_symb_range; eauto. omega.
+  eapply genv_symb_range; eauto.
 Qed.
 
 Theorem find_funct_ptr_not_fresh:
@@ -1010,7 +1000,7 @@ Theorem find_funct_ptr_not_fresh:
   find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b.
 Proof.
   intros. red. erewrite <- init_mem_genv_next; eauto. 
-  exploit genv_funs_range; eauto. omega.
+  eapply genv_funs_range; eauto.
 Qed.
 
 Theorem find_var_info_not_fresh:
@@ -1019,7 +1009,7 @@ Theorem find_var_info_not_fresh:
   find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b.
 Proof.
   intros. red. erewrite <- init_mem_genv_next; eauto. 
-  exploit genv_vars_range; eauto. omega.
+  eapply genv_vars_range; eauto.
 Qed.
 
 Theorem init_mem_characterization:
@@ -1033,8 +1023,8 @@ Theorem init_mem_characterization:
 Proof.
   intros. eapply alloc_globals_initialized; eauto.
   rewrite Mem.nextblock_empty. auto. 
-  red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction.
-  red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction.
+  red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
+  red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
 Qed.
 
 Theorem init_mem_characterization_2:
@@ -1045,9 +1035,9 @@ Theorem init_mem_characterization_2:
   /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p).
 Proof.
   intros. unfold init_mem in H0. eapply alloc_globals_initialized; eauto.
-  rewrite Mem.nextblock_empty. auto. 
-  red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction.
-  red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction.
+  rewrite Mem.nextblock_empty. auto.
+  red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
+  red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
 Qed.
 
 (** ** Compatibility with memory injections *)
@@ -1056,12 +1046,12 @@ Section INITMEM_INJ.
 
 Variable ge: t.
 Variable thr: block.
-Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> b < thr.
+Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> Plt b thr.
 
 Lemma store_zeros_neutral:
   forall m b p n m',
   Mem.inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   store_zeros m b p n = Some m' ->
   Mem.inject_neutral thr m'.
 Proof.
@@ -1074,30 +1064,29 @@ Qed.
 Lemma store_init_data_neutral:
   forall m b p id m',
   Mem.inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   store_init_data ge m b p id = Some m' ->
   Mem.inject_neutral thr m'.
 Proof.
   intros.
   destruct id; simpl in H1; try (eapply Mem.store_inject_neutral; eauto; fail).
   congruence.
-  revert H1. caseEq (find_symbol ge i); try congruence. intros b' FS ST. 
+  destruct (find_symbol ge i) as [b'|] eqn:E; try discriminate.
   eapply Mem.store_inject_neutral; eauto. 
-  econstructor. unfold Mem.flat_inj. apply zlt_true; eauto. 
+  econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto. eauto.  
   rewrite Int.add_zero. auto. 
 Qed.
 
 Lemma store_init_data_list_neutral:
   forall b idl m p m',
   Mem.inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   store_init_data_list ge m b p idl = Some m' ->
   Mem.inject_neutral thr m'.
 Proof.
-  induction idl; simpl.
-  intros; congruence.
-  intros until m'; intros INJ FB.
-  caseEq (store_init_data ge m b p a); try congruence. intros. 
+  induction idl; simpl; intros.
+  congruence.
+  destruct (store_init_data ge m b p a) as [m1|] eqn:E; try discriminate.
   eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. 
 Qed.
 
@@ -1105,13 +1094,13 @@ Lemma alloc_global_neutral:
   forall idg m m',
   alloc_global ge m idg = Some m' ->
   Mem.inject_neutral thr m ->
-  Mem.nextblock m < thr ->
+  Plt (Mem.nextblock m) thr ->
   Mem.inject_neutral thr m'.
 Proof.
   intros. destruct idg as [id [f|v]]; simpl in H.
   (* function *)
   destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
-  assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+  assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   eapply Mem.drop_inject_neutral; eauto. 
   eapply Mem.alloc_inject_neutral; eauto.
   (* variable *)
@@ -1120,27 +1109,35 @@ Proof.
   destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
   destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate.
   destruct (store_init_data_list ge m2 b 0 init) as [m3|] eqn:?; try discriminate.
-  assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+  assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   eapply Mem.drop_inject_neutral; eauto. 
   eapply store_init_data_list_neutral with (m := m2) (b := b); eauto.
   eapply store_zeros_neutral with (m := m1); eauto. 
   eapply Mem.alloc_inject_neutral; eauto.
 Qed.
 
+Remark advance_next_le: forall gl x, Ple x (advance_next gl x).
+Proof.
+  induction gl; simpl; intros.
+  apply Ple_refl.
+  apply Ple_trans with (Psucc x). apply Ple_succ. eauto.
+Qed.
+
 Lemma alloc_globals_neutral:
   forall gl m m',
   alloc_globals ge m gl = Some m' ->
   Mem.inject_neutral thr m ->
-  Mem.nextblock m' <= thr ->
+  Ple (Mem.nextblock m') thr ->
   Mem.inject_neutral thr m'.
 Proof.
-  induction gl; simpl.
-  intros. congruence.
-  intros until m'. caseEq (alloc_global ge m a); try congruence. intros.
-  assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: gl))).
-  eapply alloc_globals_nextblock with ge. simpl. rewrite H. auto. 
-  simpl length in H3. rewrite inj_S in H3. 
-  exploit alloc_global_neutral; eauto. unfold block in *; omega.
+  induction gl; intros.
+  simpl in *. congruence.
+  exploit alloc_globals_nextblock; eauto. intros EQ. 
+  simpl in *. destruct (alloc_global ge m a) as [m1|] eqn:E; try discriminate.
+  exploit alloc_global_neutral; eauto.
+  assert (Ple (Psucc (Mem.nextblock m)) (Mem.nextblock m')).
+  { rewrite EQ. apply advance_next_le. }
+  unfold Plt, Ple in *; zify; omega.
 Qed.
 
 End INITMEM_INJ.
@@ -1155,7 +1152,7 @@ Proof.
   eapply alloc_globals_neutral; eauto. 
   intros. exploit find_symbol_not_fresh; eauto.
   apply Mem.empty_inject_neutral.
-  omega.
+  apply Ple_refl.
 Qed.
 
 Section INITMEM_AUGMENT_INJ. 
@@ -1166,23 +1163,23 @@ Variable thr: block.
 Lemma store_zeros_augment:
   forall m1 m2 b p n m2',
   Mem.inject (Mem.flat_inj thr) m1 m2 ->
-  b >= thr ->
+  Ple thr b ->
   store_zeros m2 b p n = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2'.
 Proof.
   intros until n. functional induction (store_zeros m2 b p n); intros.
   inv H1; auto.
   apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. 
-  intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr). 
-    inversion H2; subst; omega.  
-    discriminate.
-  inv H1.
+  intros. exfalso. unfold Mem.flat_inj in H2. destruct (plt b' thr). 
+  inv H2. unfold Plt, Ple in *. zify; omega.
+  discriminate.
+  discriminate.
 Qed.
 
 Lemma store_init_data_augment: 
   forall m1 m2 b p id m2', 
   Mem.inject (Mem.flat_inj thr) m1 m2 -> 
-  b >= thr -> 
+  Ple thr b -> 
   store_init_data ge m2 b p id = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2'.
 Proof. 
@@ -1192,7 +1189,7 @@ Proof.
              Mem.inject (Mem.flat_inj thr) m1 m2'). 
     intros. eapply Mem.store_outside_inject; eauto. 
     intros. unfold Mem.flat_inj in H0.
-    destruct (zlt b' thr); inversion H0; subst. omega. 
+    destruct (plt b' thr); inv H0. unfold Plt, Ple in *. zify; omega.
   destruct id; simpl in ST; try (eapply P; eauto; fail).
   congruence.
   revert ST.  caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. 
@@ -1201,7 +1198,7 @@ Qed.
 Lemma store_init_data_list_augment:
   forall b idl m1 m2 p m2', 
   Mem.inject (Mem.flat_inj thr) m1 m2 -> 
-  b >= thr -> 
+  Ple thr b -> 
   store_init_data_list ge m2 b p idl = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2'.
 Proof. 
@@ -1216,37 +1213,37 @@ Lemma alloc_global_augment:
   forall idg m1 m2 m2',
   alloc_global ge m2 idg = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2 -> 
-  Mem.nextblock m2 >= thr -> 
+  Ple thr (Mem.nextblock m2) -> 
   Mem.inject (Mem.flat_inj thr) m1 m2'.
 Proof.
   intros. destruct idg as [id [f|v]]; simpl in H.
   (* function *)
   destruct (Mem.alloc m2 0 1) as [m3 b] eqn:?.
-  assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+  assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   eapply Mem.drop_outside_inject. 2: eauto. 
   eapply Mem.alloc_right_inject; eauto.
-  intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. 
-     subst; exfalso; omega.
+  intros. unfold Mem.flat_inj in H3. destruct (plt b' thr); inv H3.
+  unfold Plt, Ple in *. zify; omega.
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
   destruct (Mem.alloc m2 0 sz) as [m3 b] eqn:?.
   destruct (store_zeros m3 b 0 sz) as [m4|] eqn:?; try discriminate.
   destruct (store_init_data_list ge m4 b 0 init) as [m5|] eqn:?; try discriminate.
-  assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+  assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
   eapply Mem.drop_outside_inject. 2: eauto. 
   eapply store_init_data_list_augment. 3: eauto. 2: eauto.
   eapply store_zeros_augment. 3: eauto. 2: eauto.
   eapply Mem.alloc_right_inject; eauto.
-  intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. 
-     subst; exfalso; omega.
+  intros. unfold Mem.flat_inj in H3. destruct (plt b' thr); inv H3.
+  unfold Plt, Ple in *. zify; omega.
 Qed.
 
 Lemma alloc_globals_augment:
   forall gl m1 m2 m2',
   alloc_globals ge m2 gl = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2 ->
-  Mem.nextblock m2 >= thr ->
+  Ple thr (Mem.nextblock m2) ->
   Mem.inject (Mem.flat_inj thr) m1 m2'.
 Proof.
   induction gl; simpl.
@@ -1255,7 +1252,7 @@ Proof.
   eapply IHgl with (m2 := m); eauto.  
     eapply alloc_global_augment; eauto. 
     rewrite (alloc_global_nextblock _ _ _ H). 
-    unfold block in *; omega. 
+    apply Ple_trans with (Mem.nextblock m2); auto. apply Ple_succ.
 Qed.
 
 End INITMEM_AUGMENT_INJ. 
@@ -1280,26 +1277,26 @@ Inductive match_globvar: globvar V -> globvar W -> Prop :=
 Record match_genvs (new_globs : list (ident * globdef B W)) 
                    (ge1: t A V) (ge2: t B W): Prop := {
   mge_next:
-    genv_next ge2 = genv_next ge1 + Z_of_nat(length new_globs);
+    genv_next ge2 = advance_next new_globs (genv_next ge1);
   mge_symb:
     forall id, ~ In id (map fst new_globs) ->
                    PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1);
   mge_funs:
-    forall b f, ZMap.get b (genv_funs ge1) = Some f ->
-    exists tf, ZMap.get b (genv_funs ge2) = Some tf /\ match_fun f tf;
+    forall b f, PTree.get b (genv_funs ge1) = Some f ->
+    exists tf, PTree.get b (genv_funs ge2) = Some tf /\ match_fun f tf;
   mge_rev_funs:
-    forall b tf, ZMap.get b (genv_funs ge2) = Some tf ->
-    if zlt b (genv_next ge1) then 
-      exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf
+    forall b tf, PTree.get b (genv_funs ge2) = Some tf ->
+    if plt b (genv_next ge1) then 
+      exists f, PTree.get b (genv_funs ge1) = Some f /\ match_fun f tf
     else 
       In (Gfun tf) (map snd new_globs);
   mge_vars:
-    forall b v, ZMap.get b (genv_vars ge1) = Some v ->
-    exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv;
+    forall b v, PTree.get b (genv_vars ge1) = Some v ->
+    exists tv, PTree.get b (genv_vars ge2) = Some tv /\ match_globvar v tv;
   mge_rev_vars:
-    forall b tv, ZMap.get b (genv_vars ge2) = Some tv ->
-    if zlt b (genv_next ge1) then
-      exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv
+    forall b tv, PTree.get b (genv_vars ge2) = Some tv ->
+    if plt b (genv_next ge1) then
+      exists v, PTree.get b (genv_vars ge1) = Some v /\ match_globvar v tv
     else
       In (Gvar tv) (map snd new_globs)
 }.
@@ -1310,50 +1307,49 @@ Lemma add_global_match:
   match_globdef match_fun match_varinfo idg1 idg2 ->
   match_genvs nil (add_global ge1 idg1) (add_global ge2 idg2).
 Proof.
-  intros. destruct H. 
-     simpl in mge_next0. rewrite Zplus_0_r in mge_next0.
+  intros. destruct H. simpl in mge_next0.
   inv H0.
 (* two functions *)
   constructor; simpl.
-  rewrite Zplus_0_r. congruence.
+  congruence.
   intros. rewrite mge_next0. 
     repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
-  rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. 
-    destruct (ZIndexed.eq b (genv_next ge1)). 
+  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. 
+    destruct (peq b (genv_next ge1)). 
      exists f2; split; congruence.
      eauto.
-  rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. 
-   destruct (ZIndexed.eq b (genv_next ge1)). 
-    subst b. rewrite zlt_true. exists f1; split; congruence. omega.
+  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. 
+   destruct (peq b (genv_next ge1)). 
+    subst b. rewrite pred_dec_true. exists f1; split; congruence. apply Plt_succ.
     pose proof (mge_rev_funs0 b tf H0). 
-    destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. 
+    destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
     contradiction.
   eauto.
   intros.
     pose proof (mge_rev_vars0 b tv H0). 
-    destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. 
+    destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto.
+    apply Plt_trans with (genv_next ge1); auto. apply Plt_succ.
     contradiction.
 (* two variables *)
   constructor; simpl.
-  rewrite Zplus_0_r. congruence.
+  congruence.
   intros. rewrite mge_next0. 
     repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
   eauto.
   intros.
     pose proof (mge_rev_funs0 b tf H0). 
-    destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. 
+    destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
     contradiction.
-  rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. 
-    destruct (ZIndexed.eq b (genv_next ge1)).
+  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. 
+    destruct (peq b (genv_next ge1)).
     econstructor; split. eauto. inv H0. constructor; auto. 
     eauto.
-  rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. 
-   destruct (ZIndexed.eq b (genv_next ge1)). 
-    subst b. rewrite zlt_true.
-    econstructor; split. eauto. inv H0. constructor; auto.
-    omega.
+  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. 
+   destruct (peq b (genv_next ge1)). 
+    subst b. rewrite pred_dec_true.
+    econstructor; split. eauto. inv H0. constructor; auto. apply Plt_succ.
     pose proof (mge_rev_vars0 b tv H0). 
-    destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. 
+    destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
     contradiction.
 Qed.
 
@@ -1372,31 +1368,36 @@ Lemma add_global_augment_match:
   match_genvs new_globs ge1 ge2 ->
   match_genvs (new_globs ++ (idg :: nil)) ge1 (add_global ge2 idg).
 Proof.
-  intros. destruct H. constructor; simpl. 
-  rewrite mge_next0. rewrite app_length. 
-    simpl. rewrite inj_plus. change (Z_of_nat 1) with 1. unfold block; omega.
+  intros. destruct H. 
+  assert (LE: Ple (genv_next ge1) (genv_next ge2)).
+  { rewrite mge_next0; apply advance_next_le. }
+  constructor; simpl.
+  rewrite mge_next0. unfold advance_next. rewrite fold_left_app. simpl. auto.
   intros. rewrite map_app in H. rewrite in_app in H. simpl in H. 
     destruct (peq id idg#1). subst. intuition. rewrite PTree.gso. 
     apply mge_symb0. intuition. auto. 
   intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
-    rewrite ZMap.gso. eauto. exploit genv_funs_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. 
+    rewrite PTree.gso. eauto.
+    exploit genv_funs_range; eauto. intros.
+    unfold Plt, Ple in *; zify; omega.
   intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
-    rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). 
-    rewrite zlt_false. rewrite in_app. simpl; right; left. congruence.
-    subst b. rewrite mge_next0. omega.
-    exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. 
+    rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). 
+    rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence.
+    subst b. unfold Plt, Ple in *; zify; omega.
+    exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. 
     rewrite in_app. tauto.
-    exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. 
+    exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. 
     rewrite in_app. tauto.
   intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
-    rewrite ZMap.gso. eauto. exploit genv_vars_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. 
+    rewrite PTree.gso. eauto. exploit genv_vars_range; eauto. 
+    unfold Plt, Ple in *; zify; omega.
   intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
-    exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. 
+    exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. 
     rewrite in_app. tauto.
-    rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). 
-    rewrite zlt_false. rewrite in_app. simpl; right; left. congruence.
-    subst b. rewrite mge_next0. omega.
-    exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. 
+    rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). 
+    rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence.
+    subst b. unfold Plt, Ple in *; zify; omega.
+    exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. 
     rewrite in_app. tauto.
 Qed.
 
@@ -1427,7 +1428,7 @@ Proof.
   change new_globs with (nil ++ new_globs) at 1. 
   apply add_globals_augment_match.
   apply add_globals_match; auto.
-  constructor; simpl; auto; intros; rewrite ZMap.gi in H; congruence.
+  constructor; simpl; auto; intros; rewrite PTree.gempty in H; congruence.
 Qed.
 
 Theorem find_funct_ptr_match:
@@ -1440,7 +1441,7 @@ Proof (mge_funs globalenvs_match).
 Theorem find_funct_ptr_rev_match:
   forall (b : block) (tf : B),
   find_funct_ptr (globalenv p') b = Some tf ->
-  if zlt b (genv_next (globalenv p)) then 
+  if plt b (genv_next (globalenv p)) then 
       exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf
   else 
       In (Gfun tf) (map snd new_globs).
@@ -1467,7 +1468,7 @@ Proof.
   rewrite find_funct_find_funct_ptr in H. 
   rewrite find_funct_find_funct_ptr.
   apply find_funct_ptr_rev_match in H. 
-   destruct (zlt b (genv_next (globalenv p))); auto.
+   destruct (plt b (genv_next (globalenv p))); auto.
 Qed.
 
 Theorem find_var_info_match:
@@ -1480,7 +1481,7 @@ Proof (mge_vars globalenvs_match).
 Theorem find_var_info_rev_match:
   forall (b : block) (tv : globvar W),
   find_var_info (globalenv p') b = Some tv ->
-  if zlt b (genv_next (globalenv p)) then 
+  if plt b (genv_next (globalenv p)) then 
     exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv
   else
     In (Gvar tv) (map snd new_globs).
@@ -1597,18 +1598,18 @@ Proof.
   intros. unfold find_symbol, find_funct_ptr in *; simpl.
   destruct H1 as [b [X Y]]. exists b; split.
   rewrite PTree.gso; auto.
-  destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. 
-  exploit genv_funs_range; eauto. unfold ZIndexed.t; omega.
+  destruct g1 as [f1 | v1]. rewrite PTree.gso. auto.
+  apply Plt_ne. eapply genv_funs_range; eauto.
   auto. 
 (* ensures *)
   intros. unfold find_symbol, find_funct_ptr in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. 
+  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. 
 Qed.
 
 Theorem find_funct_ptr_rev_transf_augment:
   forall (b: block) (tf: B),
   find_funct_ptr (globalenv p') b = Some tf ->
-  if zlt b (genv_next (globalenv p)) then
+  if plt b (genv_next (globalenv p)) then
    (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf)
   else 
    In (Gfun tf) (map snd new_globs).
@@ -1662,24 +1663,24 @@ Proof.
   intros. unfold find_symbol, find_var_info in *; simpl.
   destruct H1 as [b [X Y]]. exists b; split.
   rewrite PTree.gso; auto.
-  destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. 
-  exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
+  destruct g1 as [f1 | v1]. auto. rewrite PTree.gso. auto.
+  red; intros; subst b. eelim Plt_strict. eapply genv_vars_range; eauto.
 (* ensures *)
   intros. unfold find_symbol, find_var_info in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. 
+  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. 
 Qed.
 
 Theorem find_var_info_rev_transf_augment:
   forall (b: block) (v': globvar W),
   find_var_info (globalenv p') b = Some v' ->
-  if zlt b (genv_next (globalenv p)) then
+  if plt b (genv_next (globalenv p)) then
     (exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v')
   else
     (In (Gvar v') (map snd new_globs)).
 Proof.
   intros. 
   exploit find_var_info_rev_match. eexact prog_match. eauto.
-  destruct (zlt b (genv_next (globalenv p))); auto.
+  destruct (plt b (genv_next (globalenv p))); auto.
   intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. 
   rewrite H0; simpl. auto.
 Qed.
@@ -1711,7 +1712,7 @@ Proof.
   intros. 
   pose proof (initmem_inject p H0). 
   erewrite init_mem_transf_augment in H1; eauto. 
-  eapply alloc_globals_augment; eauto. omega.
+  eapply alloc_globals_augment; eauto. apply Ple_refl. 
 Qed.
 
 End TRANSF_PROGRAM_AUGMENT.
@@ -1748,7 +1749,7 @@ Theorem find_funct_ptr_rev_transf_partial2:
 Proof.
   pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
   intros.  pose proof (H b tf H0). 
-  destruct (zlt b (genv_next (globalenv p))).  auto. contradiction.
+  destruct (plt b (genv_next (globalenv p))).  auto. contradiction.
 Qed.
 
 Theorem find_funct_transf_partial2:
@@ -1787,7 +1788,7 @@ Theorem find_var_info_rev_transf_partial2:
 Proof.
   pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
   intros.  pose proof (H b v' H0). 
-  destruct (zlt b (genv_next (globalenv p))).  auto. contradiction.
+  destruct (plt b (genv_next (globalenv p))).  auto. contradiction.
 Qed.
 
 Theorem find_symbol_transf_partial2:
diff --git a/common/Memory.v b/common/Memory.v
index 54d50f7..ca8b490 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -41,7 +41,7 @@ Require Export Memtype.
 Local Unset Elimination Schemes.
 Local Unset Case Analysis Schemes.
 
-Local Notation "a # b" := (ZMap.get b a) (at level 1).
+Local Notation "a # b" := (PMap.get b a) (at level 1).
 
 Module Mem <: MEM.
 
@@ -59,15 +59,16 @@ Definition perm_order'' (po1 po2: option permission) :=
  end.
 
 Record mem' : Type := mkmem {
-  mem_contents: ZMap.t (ZMap.t memval);  (**r [block -> offset -> memval] *)
-  mem_access: ZMap.t (Z -> perm_kind -> option permission);
+  mem_contents: PMap.t (ZMap.t memval);  (**r [block -> offset -> memval] *)
+  mem_access: PMap.t (Z -> perm_kind -> option permission);
                                          (**r [block -> offset -> kind -> option permission] *)
   nextblock: block;
-  nextblock_pos: nextblock > 0;
   access_max: 
     forall b ofs, perm_order'' (mem_access#b ofs Max) (mem_access#b ofs Cur);
   nextblock_noaccess:
-    forall b ofs k, b >= nextblock -> mem_access#b ofs k = None
+    forall b ofs k, ~(Plt b nextblock) -> mem_access#b ofs k = None;
+  contents_default:
+    forall b, fst mem_contents#b = Undef
 }.
 
 Definition mem := mem'.
@@ -85,8 +86,7 @@ Qed.
 (** A block address is valid if it was previously allocated. It remains valid
   even after being freed. *)
 
-Definition valid_block (m: mem) (b: block) :=
-  b < nextblock m.
+Definition valid_block (m: mem) (b: block) := Plt b (nextblock m).
 
 Theorem valid_not_valid_diff:
   forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
@@ -142,7 +142,7 @@ Theorem perm_valid_block:
   forall m b ofs k p, perm m b ofs k p -> valid_block m b.
 Proof.
   unfold perm; intros. 
-  destruct (zlt b m.(nextblock)).
+  destruct (plt b m.(nextblock)).
   auto.
   assert (m.(mem_access)#b ofs k = None).
   eapply nextblock_noaccess; eauto. 
@@ -340,48 +340,47 @@ Qed.
 (** The initial store *)
 
 Program Definition empty: mem :=
-  mkmem (ZMap.init (ZMap.init Undef))
-        (ZMap.init (fun ofs k => None))
-        1 _ _ _.
+  mkmem (PMap.init (ZMap.init Undef))
+        (PMap.init (fun ofs k => None))
+        1%positive _ _ _.
 Next Obligation.
-  omega.
+  repeat rewrite PMap.gi. red; auto.
 Qed.
 Next Obligation.
-  repeat rewrite ZMap.gi. red; auto.
+  rewrite PMap.gi. auto.
 Qed.
 Next Obligation.
-  rewrite ZMap.gi. auto.
+  rewrite PMap.gi. auto.
 Qed.
 
-Definition nullptr: block := 0.
-
 (** Allocation of a fresh block with the given bounds.  Return an updated
   memory state and the address of the fresh block, which initially contains
   undefined cells.  Note that allocation never fails: we model an
   infinite memory. *)
 
 Program Definition alloc (m: mem) (lo hi: Z) :=
-  (mkmem (ZMap.set m.(nextblock) 
+  (mkmem (PMap.set m.(nextblock) 
                    (ZMap.init Undef)
                    m.(mem_contents))
-         (ZMap.set m.(nextblock)
+         (PMap.set m.(nextblock)
                    (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None)
                    m.(mem_access))
-         (Zsucc m.(nextblock))
+         (Psucc m.(nextblock))
          _ _ _,
    m.(nextblock)).
 Next Obligation.
-  generalize (nextblock_pos m). omega. 
-Qed.
-Next Obligation.
-  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextblock m)). 
+  repeat rewrite PMap.gsspec. destruct (peq b (nextblock m)). 
   subst b. destruct (zle lo ofs && zlt ofs hi); red; auto with mem. 
   apply access_max. 
 Qed.
 Next Obligation.
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextblock m)). 
-  subst b. generalize (nextblock_pos m). intros. omegaContradiction.
-  apply nextblock_noaccess. omega.
+  rewrite PMap.gsspec. destruct (peq b (nextblock m)). 
+  subst b. elim H. apply Plt_succ. 
+  apply nextblock_noaccess. red; intros; elim H. 
+  apply Plt_trans_succ; auto.
+Qed.
+Next Obligation.
+  rewrite PMap.gsspec. destruct (peq b (nextblock m)). auto. apply contents_default. 
 Qed.
 
 (** Freeing a block between the given bounds.
@@ -391,23 +390,23 @@ Qed.
 
 Program Definition unchecked_free (m: mem) (b: block) (lo hi: Z): mem :=
   mkmem m.(mem_contents)
-        (ZMap.set b 
+        (PMap.set b 
                 (fun ofs k => if zle lo ofs && zlt ofs hi then None else m.(mem_access)#b ofs k)
                 m.(mem_access))
         m.(nextblock) _ _ _.
 Next Obligation.
-  apply nextblock_pos. 
-Qed.
-Next Obligation.
-  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b).
+  repeat rewrite PMap.gsspec. destruct (peq b0 b).
   destruct (zle lo ofs && zlt ofs hi). red; auto. apply access_max. 
   apply access_max.
 Qed.
 Next Obligation.
-  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst.
+  repeat rewrite PMap.gsspec. destruct (peq b0 b). subst.
   destruct (zle lo ofs && zlt ofs hi). auto. apply nextblock_noaccess; auto.
   apply nextblock_noaccess; auto.
 Qed.
+Next Obligation.
+  apply contents_default.
+Qed.
 
 Definition free (m: mem) (b: block) (lo hi: Z): option mem :=
   if range_perm_dec m b lo hi Cur Freeable 
@@ -431,7 +430,7 @@ Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem :=
 Fixpoint getN (n: nat) (p: Z) (c: ZMap.t memval) {struct n}: list memval :=
   match n with
   | O => nil
-  | S n' => c#p :: getN n' (p + 1) c
+  | S n' => ZMap.get p c :: getN n' (p + 1) c
   end.
 
 (** [load chunk m b ofs] perform a read in memory state [m], at address
@@ -475,12 +474,12 @@ Fixpoint setN (vl: list memval) (p: Z) (c: ZMap.t memval) {struct vl}: ZMap.t me
 Remark setN_other:
   forall vl c p q,
   (forall r, p <= r < p + Z_of_nat (length vl) -> r <> q) ->
-  (setN vl p c)#q = c#q.
+  ZMap.get q (setN vl p c) = ZMap.get q c.
 Proof.
   induction vl; intros; simpl.
   auto. 
   simpl length in H. rewrite inj_S in H.
-  transitivity ((ZMap.set p a c)#q).
+  transitivity (ZMap.get q (ZMap.set p a c)).
   apply IHvl. intros. apply H. omega.
   apply ZMap.gso. apply not_eq_sym. apply H. omega. 
 Qed.
@@ -488,7 +487,7 @@ Qed.
 Remark setN_outside:
   forall vl c p q,
   q < p \/ q >= p + Z_of_nat (length vl) ->
-  (setN vl p c)#q = c#q.
+  ZMap.get q (setN vl p c) = ZMap.get q c.
 Proof.
   intros. apply setN_other. 
   intros. omega. 
@@ -507,7 +506,7 @@ Qed.
 
 Remark getN_exten:
   forall c1 c2 n p,
-  (forall i, p <= i < p + Z_of_nat n -> c1#i = c2#i) ->
+  (forall i, p <= i < p + Z_of_nat n -> ZMap.get i c1 = ZMap.get i c2) ->
   getN n p c1 = getN n p c2.
 Proof.
   induction n; intros. auto. rewrite inj_S in H. simpl. decEq. 
@@ -522,23 +521,34 @@ Proof.
   intros. apply getN_exten. intros. apply setN_outside. omega. 
 Qed.
 
+Remark setN_default:
+  forall vl q c, fst (setN vl q c) = fst c.
+Proof.
+  induction vl; simpl; intros. auto. rewrite IHvl. auto. 
+Qed.
+
 (** [store chunk m b ofs v] perform a write in memory state [m].
   Value [v] is stored at address [b] and offset [ofs].
   Return the updated memory store, or [None] if the accessed bytes
   are not writable. *)
 
-Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem :=
+Program Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem :=
   if valid_access_dec m chunk b ofs Writable then
-    Some (mkmem (ZMap.set b 
+    Some (mkmem (PMap.set b 
                           (setN (encode_val chunk v) ofs (m.(mem_contents)#b))
                           m.(mem_contents))
                 m.(mem_access)
                 m.(nextblock)
-                m.(nextblock_pos)
-                m.(access_max)
-                m.(nextblock_noaccess))
+                _ _ _)
   else
     None.
+Next Obligation. apply access_max. Qed.
+Next Obligation. apply nextblock_noaccess; auto. Qed.
+Next Obligation. 
+  rewrite PMap.gsspec. destruct (peq b0 b).
+  rewrite setN_default. apply contents_default. 
+  apply contents_default.
+Qed.
 
 (** [storev chunk m addr v] is similar, but the address and offset are given
   as a single value [addr], which must be a pointer value. *)
@@ -553,17 +563,22 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   starting at location [(b, ofs)].  Returns updated memory state
   or [None] if the accessed locations are not writable. *)
 
-Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem :=
+Program Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem :=
   if range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Cur Writable then
     Some (mkmem
-             (ZMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents))
+             (PMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents))
              m.(mem_access)
              m.(nextblock)
-             m.(nextblock_pos)
-             m.(access_max)
-             m.(nextblock_noaccess))
+             _ _ _)
   else
     None.
+Next Obligation. apply access_max. Qed.
+Next Obligation. apply nextblock_noaccess; auto. Qed.
+Next Obligation. 
+  rewrite PMap.gsspec. destruct (peq b0 b).
+  rewrite setN_default. apply contents_default. 
+  apply contents_default.
+Qed.
 
 (** [drop_perm m b lo hi p] sets the max permissions of the byte range
     [(b, lo) ... (b, hi - 1)] to [p].  These bytes must have current permissions
@@ -573,38 +588,38 @@ Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option
 Program Definition drop_perm (m: mem) (b: block) (lo hi: Z) (p: permission): option mem :=
   if range_perm_dec m b lo hi Cur Freeable then
     Some (mkmem m.(mem_contents)
-                (ZMap.set b
+                (PMap.set b
                         (fun ofs k => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access)#b ofs k)
                         m.(mem_access))
                 m.(nextblock) _ _ _)
   else None.
 Next Obligation.
-  apply nextblock_pos.
-Qed.
-Next Obligation.
-  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst b0.
+  repeat rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
   destruct (zle lo ofs && zlt ofs hi). red; auto with mem. apply access_max. 
   apply access_max.
 Qed.
 Next Obligation.
   specialize (nextblock_noaccess m b0 ofs k H0). intros. 
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst b0.
+  rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
   destruct (zle lo ofs). destruct (zlt ofs hi).
   assert (perm m b ofs k Freeable). apply perm_cur. apply H; auto. 
   unfold perm in H2. rewrite H1 in H2. contradiction.
   auto. auto. auto. 
 Qed.
+Next Obligation.
+  apply contents_default.
+Qed.
 
 (** * Properties of the memory operations *)
 
 (** Properties of the empty store. *)
 
-Theorem nextblock_empty: nextblock empty = 1.
+Theorem nextblock_empty: nextblock empty = 1%positive.
 Proof. reflexivity. Qed.
 
 Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p.
 Proof. 
-  intros. unfold perm, empty; simpl. rewrite ZMap.gi. simpl. tauto. 
+  intros. unfold perm, empty; simpl. rewrite PMap.gi. simpl. tauto. 
 Qed.
 
 Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p.
@@ -838,7 +853,7 @@ Qed.
 
 Theorem load_rep:
  forall ch m1 m2 b ofs v1 v2, 
-  (forall z, 0 <= z < size_chunk ch -> m1.(mem_contents)#b#(ofs+z) = m2.(mem_contents)#b#(ofs+z)) ->
+  (forall z, 0 <= z < size_chunk ch -> ZMap.get (ofs + z) m1.(mem_contents)#b = ZMap.get (ofs + z) m2.(mem_contents)#b) ->
   load ch m1 b ofs = Some v1 ->
   load ch m2 b ofs = Some v2 ->
   v1 = v2.
@@ -948,9 +963,9 @@ Proof.
 Qed.
 
 Lemma store_mem_contents: 
-  mem_contents m2 = ZMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents).
+  mem_contents m2 = PMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents).
 Proof.
-  unfold store in STORE. destruct ( valid_access_dec m1 chunk b ofs Writable); inv STORE.
+  unfold store in STORE. destruct (valid_access_dec m1 chunk b ofs Writable); inv STORE.
   auto.
 Qed.
 
@@ -1028,7 +1043,7 @@ Proof.
   exists v'; split; auto.
   exploit load_result; eauto. intros B. 
   rewrite B. rewrite store_mem_contents; simpl. 
-  rewrite ZMap.gss.
+  rewrite PMap.gss.
   replace (size_chunk_nat chunk') with (length (encode_val chunk v)).
   rewrite getN_setN_same. apply decode_encode_val_general. 
   rewrite encode_val_length. repeat rewrite size_chunk_conv in H. 
@@ -1063,7 +1078,7 @@ Proof.
   destruct (valid_access_dec m1 chunk' b' ofs' Readable).
   rewrite pred_dec_true. 
   decEq. decEq. rewrite store_mem_contents; simpl.
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'.
+  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
   apply getN_setN_outside. rewrite encode_val_length. repeat rewrite <- size_chunk_conv.
   intuition.
   auto.
@@ -1078,7 +1093,7 @@ Proof.
   intros.
   assert (valid_access m2 chunk b ofs Readable) by eauto with mem.
   unfold loadbytes. rewrite pred_dec_true. rewrite store_mem_contents; simpl. 
-  rewrite ZMap.gss.
+  rewrite PMap.gss.
   replace (nat_of_Z (size_chunk chunk)) with (length (encode_val chunk v)).
   rewrite getN_setN_same. auto.
   rewrite encode_val_length. auto.
@@ -1097,7 +1112,7 @@ Proof.
   destruct (range_perm_dec m1 b' ofs' (ofs' + n) Cur Readable).
   rewrite pred_dec_true. 
   decEq. rewrite store_mem_contents; simpl.
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'.
+  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
   destruct H. congruence.
   destruct (zle n 0) as [z | n0].
   rewrite (nat_of_Z_neg _ z). auto.
@@ -1114,7 +1129,7 @@ Lemma setN_property:
   forall (P: memval -> Prop) vl p q c,
   (forall v, In v vl -> P v) ->
   p <= q < p + Z_of_nat (length vl) ->
-  P((setN vl p c)#q).
+  P(ZMap.get q (setN vl p c)).
 Proof.
   induction vl; intros.
   simpl in H0. omegaContradiction.
@@ -1127,7 +1142,7 @@ Qed.
 Lemma getN_in:
   forall c q n p,
   p <= q < p + Z_of_nat n ->
-  In (c#q) (getN n p c).
+  In (ZMap.get q c) (getN n p c).
 Proof.
   induction n; intros.
   simpl in H; omegaContradiction.
@@ -1143,7 +1158,7 @@ Theorem load_pointer_store:
   \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs').
 Proof.
   intros. exploit load_result; eauto. rewrite store_mem_contents; simpl. 
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b); auto. subst b'. intro DEC.
+  rewrite PMap.gsspec. destruct (peq b' b); auto. subst b'. intro DEC.
   destruct (zle (ofs' + size_chunk chunk') ofs); auto.
   destruct (zle (ofs + size_chunk chunk) ofs'); auto.
   destruct (size_chunk_nat_pos chunk) as [sz SZ].
@@ -1176,9 +1191,9 @@ Proof.
    For the read to return a pointer, it must satisfy ~memval_valid_cont. 
 *)
   elimtype False.
-  assert (~memval_valid_cont (c'#ofs')).
+  assert (~memval_valid_cont (ZMap.get ofs' c')).
     rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. auto.
-  assert (memval_valid_cont (c'#ofs')).
+  assert (memval_valid_cont (ZMap.get ofs' c')).
     inv VSHAPE. unfold c'. rewrite <- H1. simpl. 
     apply setN_property. auto.
     assert (length mvl = sz). 
@@ -1197,10 +1212,10 @@ Proof.
    For the read to return a pointer, it must satisfy ~memval_valid_first.
 *)
   elimtype False.
-  assert (memval_valid_first (c'#ofs)).
+  assert (memval_valid_first (ZMap.get ofs c')).
     inv VSHAPE. unfold c'. rewrite <- H0. simpl. 
     rewrite setN_outside. rewrite ZMap.gss. auto. omega.
-  assert (~memval_valid_first (c'#ofs)).
+  assert (~memval_valid_first (ZMap.get ofs c')).
     rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. 
     apply H4. apply getN_in. rewrite size_chunk_conv in *.
     rewrite SZ' in *. rewrite inj_S in *. omega.
@@ -1229,7 +1244,7 @@ Proof.
   rewrite LD; clear LD.
 Opaque encode_val.
   rewrite ST; simpl.
-  rewrite ZMap.gss.
+  rewrite PMap.gss.
   set (c := m1.(mem_contents)#b).
   set (c' := setN (encode_val chunk (Vptr v_b v_o)) ofs c).
   destruct (decode_val_shape chunk' (getN (size_chunk_nat chunk') ofs' c'))
@@ -1257,9 +1272,9 @@ Opaque encode_val.
    The byte at ofs' is Undef or not memval_valid_first (because write of pointer).
    The byte at ofs' must be memval_valid_first and not Undef (otherwise load returns Vundef).
 *)
-  assert (memval_valid_first (c'#ofs') /\ c'#ofs' <> Undef).
+  assert (memval_valid_first (ZMap.get ofs' c') /\ ZMap.get ofs' c' <> Undef).
     rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. auto.
-  assert (~memval_valid_first (c'#ofs') \/ c'#ofs' = Undef).
+  assert (~memval_valid_first (ZMap.get ofs' c') \/ ZMap.get ofs' c' = Undef).
     unfold c'. destruct ENC.
     right. apply setN_property. rewrite H5. intros. eapply in_list_repeat; eauto.
     rewrite encode_val_length. rewrite <- size_chunk_conv. omega.
@@ -1277,11 +1292,11 @@ Opaque encode_val.
    The byte at ofs is Undef or not memval_valid_cont (because write of pointer).
    The byte at ofs must be memval_valid_cont and not Undef (otherwise load returns Vundef).
 *)
-  assert (memval_valid_cont (c'#ofs) /\ c'#ofs <> Undef).
+  assert (memval_valid_cont (ZMap.get ofs c') /\ ZMap.get ofs c' <> Undef).
     rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. 
     apply H8. apply getN_in. rewrite size_chunk_conv in H2. 
     rewrite SZ' in H2. rewrite inj_S in H2. omega. 
-  assert (~memval_valid_cont (c'#ofs) \/ c'#ofs = Undef).
+  assert (~memval_valid_cont (ZMap.get ofs c') \/ ZMap.get ofs c' = Undef).
     elim ENC. 
     rewrite <- GET. rewrite SZ. simpl. intros. right; congruence.
     rewrite <- GET. rewrite SZ. simpl. intros. inv H5. auto.
@@ -1301,7 +1316,7 @@ Proof.
   rewrite LD; clear LD.
 Opaque encode_val.
   rewrite ST; simpl.
-  rewrite ZMap.gss. 
+  rewrite PMap.gss. 
   set (c1 := m1.(mem_contents)#b).
   set (e := encode_val chunk (Vptr v_b v_o)).
   destruct (size_chunk_nat_pos chunk) as [sz SZ].
@@ -1334,11 +1349,10 @@ Proof.
     rewrite <- (encode_val_length chunk2 v2).
     congruence.
   unfold store.
-  destruct (valid_access_dec m chunk1 b ofs Writable).
-  rewrite pred_dec_true. 
-  f_equal. apply mkmem_ext; auto. congruence.
-  apply valid_access_compat with chunk1; auto. omega.
+  destruct (valid_access_dec m chunk1 b ofs Writable);
   destruct (valid_access_dec m chunk2 b ofs Writable); auto.
+  f_equal. apply mkmem_ext; auto. congruence.
+  elim n. apply valid_access_compat with chunk1; auto. omega.
   elim n. apply valid_access_compat with chunk2; auto. omega.
 Qed.
 
@@ -1392,8 +1406,9 @@ Theorem store_float64al32:
 Proof.
   unfold store; intros. 
   destruct (valid_access_dec m Mfloat64 b ofs Writable); try discriminate.
-  rewrite pred_dec_true. rewrite <- H. auto. 
-  apply valid_access_compat with Mfloat64; auto. simpl; omega.
+  destruct (valid_access_dec m Mfloat64al32 b ofs Writable).
+  rewrite <- H. f_equal. apply mkmem_ext; auto.
+  elim n. apply valid_access_compat with Mfloat64; auto. simpl; omega.
 Qed.
 
 Theorem storev_float64al32:
@@ -1410,9 +1425,9 @@ Theorem range_perm_storebytes:
   range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable ->
   { m2 : mem | storebytes m1 b ofs bytes = Some m2 }.
 Proof.
-  intros. econstructor. unfold storebytes.
+  intros. unfold storebytes.
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable).
-  reflexivity. 
+  econstructor; reflexivity. 
   contradiction.
 Defined.
 
@@ -1425,7 +1440,7 @@ Proof.
   unfold storebytes, store. intros. 
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable); inv H.
   destruct (valid_access_dec m1 chunk b ofs Writable).
-  auto.
+  f_equal. apply mkmem_ext; auto.
   elim n. constructor; auto. 
   rewrite encode_val_length in r. rewrite size_chunk_conv. auto.
 Qed.
@@ -1438,7 +1453,7 @@ Proof.
   unfold storebytes, store. intros. 
   destruct (valid_access_dec m1 chunk b ofs Writable); inv H.
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable).
-  auto.
+  f_equal. apply mkmem_ext; auto.
   destruct v0.  elim n. 
   rewrite encode_val_length. rewrite <- size_chunk_conv. auto.
 Qed.
@@ -1460,7 +1475,7 @@ Proof.
 Qed.
 
 Lemma storebytes_mem_contents:
-   mem_contents m2 = ZMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents).
+   mem_contents m2 = PMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents).
 Proof.
   unfold storebytes in STORE. 
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
@@ -1539,7 +1554,7 @@ Proof.
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
   try discriminate.
   rewrite pred_dec_true. 
-  decEq. inv STORE; simpl. rewrite ZMap.gss. rewrite nat_of_Z_of_nat. 
+  decEq. inv STORE; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat. 
   apply getN_setN_same. 
   red; eauto with mem. 
 Qed.
@@ -1556,7 +1571,7 @@ Proof.
   destruct (range_perm_dec m1 b' ofs' (ofs' + len) Cur Readable).
   rewrite pred_dec_true. 
   rewrite storebytes_mem_contents. decEq. 
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. 
+  rewrite PMap.gsspec. destruct (peq b' b). subst b'. 
   apply getN_setN_outside. rewrite nat_of_Z_eq; auto. intuition congruence.
   auto.
   red; auto with mem.
@@ -1575,7 +1590,7 @@ Proof.
   destruct (valid_access_dec m1 chunk b' ofs' Readable).
   rewrite pred_dec_true. 
   rewrite storebytes_mem_contents. decEq.
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'.
+  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
   rewrite getN_setN_outside. auto. rewrite <- size_chunk_conv. intuition congruence.
   auto.
   destruct v; split; auto. red; auto with mem.
@@ -1606,7 +1621,7 @@ Proof.
   destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Cur Writable); try congruence.
   destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Cur Writable).
   inv ST1; inv ST2; simpl. decEq. apply mkmem_ext; auto.
-  rewrite ZMap.gss.  rewrite setN_concat. symmetry. apply ZMap.set2.
+  rewrite PMap.gss.  rewrite setN_concat. symmetry. apply PMap.set2.
   elim n.   
   rewrite app_length. rewrite inj_plus. red; intros.
   destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))).
@@ -1684,7 +1699,7 @@ Variable b: block.
 Hypothesis ALLOC: alloc m1 lo hi = (m2, b).
 
 Theorem nextblock_alloc:
-  nextblock m2 = Zsucc (nextblock m1).
+  nextblock m2 = Psucc (nextblock m1).
 Proof.
   injection ALLOC; intros. rewrite <- H0; auto.
 Qed.
@@ -1698,19 +1713,20 @@ Qed.
 Theorem valid_block_alloc:
   forall b', valid_block m1 b' -> valid_block m2 b'.
 Proof.
-  unfold valid_block; intros. rewrite nextblock_alloc. omega.
+  unfold valid_block; intros. rewrite nextblock_alloc. 
+  apply Plt_trans_succ; auto.
 Qed.
 
 Theorem fresh_block_alloc:
   ~(valid_block m1 b).
 Proof.
-  unfold valid_block. rewrite alloc_result. omega.
+  unfold valid_block. rewrite alloc_result. apply Plt_strict. 
 Qed.
 
 Theorem valid_new_block:
   valid_block m2 b.
 Proof.
-  unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. omega.
+  unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. apply Plt_succ.
 Qed.
 
 Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
@@ -1720,32 +1736,32 @@ Theorem valid_block_alloc_inv:
 Proof.
   unfold valid_block; intros. 
   rewrite nextblock_alloc in H. rewrite alloc_result. 
-  unfold block; omega.
+  exploit Plt_succ_inv; eauto. tauto.
 Qed.
 
 Theorem perm_alloc_1:
   forall b' ofs k p, perm m1 b' ofs k p -> perm m2 b' ofs k p.
 Proof.
   unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl.
-  subst b. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' (nextblock m1)); auto.
-  rewrite nextblock_noaccess in H. contradiction. omega. 
+  subst b. rewrite PMap.gsspec. destruct (peq b' (nextblock m1)); auto.
+  rewrite nextblock_noaccess in H. contradiction. subst b'. apply Plt_strict. 
 Qed.
 
 Theorem perm_alloc_2:
   forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable.
 Proof.
   unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl.
-  subst b. rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true.
+  subst b. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true.
   rewrite zlt_true. simpl. auto with mem. omega. omega.
 Qed.
 
 Theorem perm_alloc_inv:
   forall b' ofs k p, 
   perm m2 b' ofs k p ->
-  if zeq b' b then lo <= ofs < hi else perm m1 b' ofs k p.
+  if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p.
 Proof.
   intros until p; unfold perm. inv ALLOC. simpl. 
-  rewrite ZMap.gsspec. unfold ZIndexed.eq. destruct (zeq b' (nextblock m1)); intros.
+  rewrite PMap.gsspec. unfold eq_block. destruct (peq b' (nextblock m1)); intros.
   destruct (zle lo ofs); try contradiction. destruct (zlt ofs hi); try contradiction.
   split; auto. 
   auto.
@@ -1754,13 +1770,13 @@ Qed.
 Theorem perm_alloc_3:
   forall ofs k p, perm m2 b ofs k p -> lo <= ofs < hi.
 Proof.
-  intros. exploit perm_alloc_inv; eauto. rewrite zeq_true; auto.
+  intros. exploit perm_alloc_inv; eauto. rewrite dec_eq_true; auto. 
 Qed.
 
 Theorem perm_alloc_4:
   forall b' ofs k p, perm m2 b' ofs k p -> b' <> b -> perm m1 b' ofs k p.
 Proof.
-  intros. exploit perm_alloc_inv; eauto. rewrite zeq_false; auto.
+  intros. exploit perm_alloc_inv; eauto. rewrite dec_eq_false; auto.
 Qed.
 
 Local Hint Resolve perm_alloc_1 perm_alloc_2 perm_alloc_3 perm_alloc_4: mem.
@@ -1794,14 +1810,14 @@ Theorem valid_access_alloc_inv:
 Proof.
   intros. inv H.
   generalize (size_chunk_pos chunk); intro.
-  unfold eq_block. destruct (zeq b' b). subst b'.
+  destruct (eq_block b' b). subst b'.
   assert (perm m2 b ofs Cur p). apply H0. omega. 
   assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. omega. 
-  exploit perm_alloc_inv. eexact H2. rewrite zeq_true. intro.
-  exploit perm_alloc_inv. eexact H3. rewrite zeq_true. intro. 
+  exploit perm_alloc_inv. eexact H2. rewrite dec_eq_true. intro.
+  exploit perm_alloc_inv. eexact H3. rewrite dec_eq_true. intro. 
   intuition omega. 
   split; auto. red; intros. 
-  exploit perm_alloc_inv. apply H0. eauto. rewrite zeq_false; auto. 
+  exploit perm_alloc_inv. apply H0. eauto. rewrite dec_eq_false; auto. 
 Qed.
 
 Theorem load_alloc_unchanged:
@@ -1815,7 +1831,7 @@ Proof.
   subst b'. elimtype False. eauto with mem.
   rewrite pred_dec_true; auto.
   injection ALLOC; intros. rewrite <- H2; simpl.
-  rewrite ZMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem.
+  rewrite PMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem.
   rewrite pred_dec_false. auto.
   eauto with mem.
 Qed.
@@ -1835,7 +1851,7 @@ Theorem load_alloc_same:
 Proof.
   intros. exploit load_result; eauto. intro. rewrite H0. 
   injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1.
-  rewrite ZMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity.
+  rewrite PMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity.
 Qed.
 
 Theorem load_alloc_same':
@@ -1914,7 +1930,7 @@ Theorem perm_free_1:
   perm m2 b ofs k p.
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b.
+  rewrite PMap.gsspec. destruct (peq b bf). subst b.
   destruct (zle lo ofs); simpl. 
   destruct (zlt ofs hi); simpl.
   elimtype False; intuition.
@@ -1926,7 +1942,7 @@ Theorem perm_free_2:
   forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p.
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. 
+  rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. 
   simpl. tauto. omega. omega.
 Qed.
 
@@ -1935,7 +1951,7 @@ Theorem perm_free_3:
   perm m2 b ofs k p -> perm m1 b ofs k p.
 Proof.
   intros until p. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b.
+  rewrite PMap.gsspec. destruct (peq b bf). subst b.
   destruct (zle lo ofs); simpl. 
   destruct (zlt ofs hi); simpl. tauto. 
   auto. auto. auto. 
@@ -1947,7 +1963,7 @@ Theorem perm_free_inv:
   (b = bf /\ lo <= ofs < hi) \/ perm m2 b ofs k p.
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf); auto. subst b.
+  rewrite PMap.gsspec. destruct (peq b bf); auto. subst b.
   destruct (zle lo ofs); simpl; auto.
   destruct (zlt ofs hi); simpl; auto.
 Qed.
@@ -1985,7 +2001,7 @@ Proof.
   intros. destruct H. split; auto. 
   red; intros. generalize (H ofs0 H1). 
   rewrite free_result. unfold perm, unchecked_free; simpl. 
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b.
+  rewrite PMap.gsspec. destruct (peq b bf). subst b.
   destruct (zle lo ofs0); simpl.
   destruct (zlt ofs0 hi); simpl.
   tauto. auto. auto. auto. 
@@ -2072,7 +2088,7 @@ Theorem perm_drop_1:
 Proof.
   intros.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
-  unfold perm. simpl. rewrite ZMap.gss. unfold proj_sumbool. 
+  unfold perm. simpl. rewrite PMap.gss. unfold proj_sumbool. 
   rewrite zle_true. rewrite zlt_true. simpl. constructor.
   omega. omega. 
 Qed.
@@ -2082,7 +2098,7 @@ Theorem perm_drop_2:
 Proof.
   intros.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
-  revert H0. unfold perm; simpl. rewrite ZMap.gss. unfold proj_sumbool. 
+  revert H0. unfold perm; simpl. rewrite PMap.gss. unfold proj_sumbool. 
   rewrite zle_true. rewrite zlt_true. simpl. auto. 
   omega. omega. 
 Qed.
@@ -2092,7 +2108,7 @@ Theorem perm_drop_3:
 Proof.
   intros.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
-  unfold perm; simpl. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. 
+  unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b). subst b'. 
   unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). 
   byContradiction. intuition omega.
   auto. auto. auto.
@@ -2103,7 +2119,7 @@ Theorem perm_drop_4:
 Proof.
   intros.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
-  revert H. unfold perm; simpl. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b).
+  revert H. unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b).
   subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi).
   simpl. intros. apply perm_implies with p. apply perm_implies with Freeable. apply perm_cur.
   apply r. tauto. auto with mem. auto.
@@ -2117,7 +2133,7 @@ Lemma valid_access_drop_1:
 Proof.
   intros. destruct H0. split; auto. 
   red; intros.
-  destruct (zeq b' b). subst b'.
+  destruct (eq_block b' b). subst b'.
   destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. 
   destruct (zle hi ofs0). eapply perm_drop_3; eauto.
   apply perm_implies with p. eapply perm_drop_1; eauto. omega. 
@@ -2133,20 +2149,6 @@ Proof.
   red; intros. eapply perm_drop_4; eauto. 
 Qed.
 
-(*
-Lemma valid_access_drop_3:
-  forall chunk b' ofs p',
-  valid_access m' chunk b' ofs p' ->
-  b' <> b \/ Intv.disjoint (lo, hi) (ofs, ofs + size_chunk chunk) \/ perm_order p p'.
-Proof.
-  intros. destruct H. 
-  destruct (zeq b' b); auto. subst b'.
-  destruct (Intv.disjoint_dec (lo, hi) (ofs, ofs + size_chunk chunk)); auto. 
-  exploit intv_not_disjoint; eauto. intros [x [A B]]. 
-  right; right. apply perm_drop_2 with x. auto. apply H. auto. 
-Qed.
-*)
-
 Theorem load_drop:
   forall chunk b' ofs, 
   b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p Readable ->
@@ -2190,7 +2192,7 @@ Record mem_inj (f: meminj) (m1 m2: mem) : Prop :=
       forall b1 ofs b2 delta,
       f b1 = Some(b2, delta) ->
       perm m1 b1 ofs Cur Readable ->
-      memval_inject f (m1.(mem_contents)#b1#ofs) (m2.(mem_contents)#b2#(ofs + delta))
+      memval_inject f (ZMap.get ofs m1.(mem_contents)#b1) (ZMap.get (ofs+delta) m2.(mem_contents)#b2)
   }.
 
 (** Preservation of permissions *)
@@ -2280,9 +2282,9 @@ Lemma setN_inj:
   forall (access: Z -> Prop) delta f vl1 vl2,
   list_forall2 (memval_inject f) vl1 vl2 ->
   forall p c1 c2,
-  (forall q, access q -> memval_inject f (c1#q) (c2#(q + delta))) ->
-  (forall q, access q -> memval_inject f ((setN vl1 p c1)#q) 
-                                         ((setN vl2 (p + delta) c2)#(q + delta))).
+  (forall q, access q -> memval_inject f (ZMap.get q c1) (ZMap.get (q + delta) c2)) ->
+  (forall q, access q -> memval_inject f (ZMap.get q (setN vl1 p c1)) 
+                                         (ZMap.get (q + delta) (setN vl2 (p + delta) c2))).
 Proof.
   induction 1; intros; simpl. 
   auto.
@@ -2331,15 +2333,15 @@ Proof.
   intros.
   rewrite (store_mem_contents _ _ _ _ _ _ H0).
   rewrite (store_mem_contents _ _ _ _ _ _ STORE).
-  repeat rewrite ZMap.gsspec. 
-  destruct (ZIndexed.eq b0 b1). subst b0.
+  rewrite ! PMap.gsspec. 
+  destruct (peq b0 b1). subst b0.
   (* block = b1, block = b2 *)
   assert (b3 = b2) by congruence. subst b3.
   assert (delta0 = delta) by congruence. subst delta0.
-  rewrite zeq_true.
+  rewrite peq_true.
   apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable).
   apply encode_val_inject; auto. intros. eapply mi_memval; eauto. eauto with mem. 
-  destruct (ZIndexed.eq b3 b2). subst b3.
+  destruct (peq b3 b2). subst b3.
   (* block <> b1, block = b2 *)
   rewrite setN_other. eapply mi_memval; eauto. eauto with mem. 
   rewrite encode_val_length. rewrite <- size_chunk_conv. intros. 
@@ -2367,7 +2369,7 @@ Proof.
 (* mem_contents *)
   intros. 
   rewrite (store_mem_contents _ _ _ _ _ _ H0).
-  rewrite ZMap.gso. eapply mi_memval; eauto with mem. 
+  rewrite PMap.gso. eapply mi_memval; eauto with mem. 
   congruence.
 Qed.
 
@@ -2389,7 +2391,7 @@ Proof.
 (* mem_contents *)
   intros. 
   rewrite (store_mem_contents _ _ _ _ _ _ H1).
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b2 b). subst b2. 
+  rewrite PMap.gsspec. destruct (peq b2 b). subst b2. 
   rewrite setN_outside. auto. 
   rewrite encode_val_length. rewrite <- size_chunk_conv. 
   destruct (zlt (ofs0 + delta) ofs); auto.
@@ -2434,13 +2436,13 @@ Proof.
   assert (perm m1 b0 ofs0 Cur Readable). eapply perm_storebytes_2; eauto. 
   rewrite (storebytes_mem_contents _ _ _ _ _ H0).
   rewrite (storebytes_mem_contents _ _ _ _ _ STORE).
-  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b1). subst b0.
+  rewrite ! PMap.gsspec. destruct (peq b0 b1). subst b0.
   (* block = b1, block = b2 *)
   assert (b3 = b2) by congruence. subst b3.
   assert (delta0 = delta) by congruence. subst delta0.
-  rewrite zeq_true.
+  rewrite peq_true.
   apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable); auto.
-  destruct (ZIndexed.eq b3 b2). subst b3.
+  destruct (peq b3 b2). subst b3.
   (* block <> b1, block = b2 *)
   rewrite setN_other. auto.
   intros.
@@ -2471,7 +2473,7 @@ Proof.
 (* mem_contents *)
   intros. 
   rewrite (storebytes_mem_contents _ _ _ _ _ H0).
-  rewrite ZMap.gso. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto.
+  rewrite PMap.gso. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto.
   congruence.
 Qed.
 
@@ -2493,7 +2495,7 @@ Proof.
 (* mem_contents *)
   intros. 
   rewrite (storebytes_mem_contents _ _ _ _ _ H1).
-  rewrite ZMap.gsspec. destruct (ZIndexed.eq b2 b). subst b2.
+  rewrite PMap.gsspec. destruct (peq b2 b). subst b2.
   rewrite setN_outside. auto. 
   destruct (zlt (ofs0 + delta) ofs); auto.
   destruct (zle (ofs + Z_of_nat (length bytes2)) (ofs0 + delta)). omega. 
@@ -2520,7 +2522,7 @@ Proof.
   assert (perm m2 b0 (ofs + delta) Cur Readable). 
     eapply mi_perm0; eauto.
   assert (valid_block m2 b0) by eauto with mem.
-  rewrite <- MEM; simpl. rewrite ZMap.gso. eauto with mem.
+  rewrite <- MEM; simpl. rewrite PMap.gso. eauto with mem.
   rewrite NEXT. eauto with mem. 
 Qed.
 
@@ -2534,15 +2536,15 @@ Proof.
   intros. inversion H. constructor.
 (* perm *)
   intros. exploit perm_alloc_inv; eauto. intros. 
-  destruct (zeq b0 b1). congruence. eauto. 
+  destruct (eq_block b0 b1). congruence. eauto. 
 (* access *)
-  intros. exploit valid_access_alloc_inv; eauto. unfold eq_block. intros. 
-  destruct (zeq b0 b1). congruence. eauto.
+  intros. exploit valid_access_alloc_inv; eauto. intros. 
+  destruct (eq_block b0 b1). congruence. eauto.
 (* mem_contents *)
   injection H0; intros NEXT MEM. intros. 
   rewrite <- MEM; simpl. rewrite NEXT.
   exploit perm_alloc_inv; eauto. intros.
-  rewrite ZMap.gsspec. unfold ZIndexed.eq. destruct (zeq b0 b1). 
+  rewrite PMap.gsspec. unfold eq_block in H4. destruct (peq b0 b1).
   rewrite ZMap.gi. constructor. eauto. 
 Qed.
 
@@ -2562,12 +2564,12 @@ Proof.
   intros. inversion H. constructor.
 (* perm *)
   intros. 
-  exploit perm_alloc_inv; eauto. intros. destruct (zeq b0 b1). subst b0.
+  exploit perm_alloc_inv; eauto. intros. destruct (eq_block b0 b1). subst b0.
   rewrite H4 in H5; inv H5. eauto. eauto. 
 (* access *)
   intros. 
-  exploit valid_access_alloc_inv; eauto. unfold eq_block. intros.
-  destruct (zeq b0 b1). subst b0. rewrite H4 in H5. inv H5. 
+  exploit valid_access_alloc_inv; eauto. intros.
+  destruct (eq_block b0 b1). subst b0. rewrite H4 in H5. inv H5. 
   split. red; intros. 
   replace ofs0 with ((ofs0 - delta0) + delta0) by omega. 
   apply H3. omega. 
@@ -2577,8 +2579,8 @@ Proof.
   injection H0; intros NEXT MEM. 
   intros. rewrite <- MEM; simpl. rewrite NEXT.
   exploit perm_alloc_inv; eauto. intros.
-  rewrite ZMap.gsspec. unfold ZIndexed.eq. 
-  destruct (zeq b0 b1). rewrite ZMap.gi. constructor. eauto.
+  rewrite PMap.gsspec. unfold eq_block in H7. 
+  destruct (peq b0 b1). rewrite ZMap.gi. constructor. eauto.
 Qed.
 
 Lemma free_left_inj:
@@ -2612,7 +2614,7 @@ Proof.
     perm m1 b1 ofs k p -> perm m2' b2 (ofs + delta) k p).
   intros. 
   intros. eapply perm_free_1; eauto. 
-  destruct (zeq b2 b); auto. subst b. right. 
+  destruct (eq_block b2 b); auto. subst b. right. 
   assert (~ (lo <= ofs + delta < hi)). red; intros; eapply H1; eauto. 
   omega.
   constructor.
@@ -2643,7 +2645,7 @@ Proof.
   eapply valid_access_drop_2; eauto.
 (* contents *)
   intros.
-  replace (m1'.(mem_contents)#b1#ofs) with (m1.(mem_contents)#b1#ofs).
+  replace (ZMap.get ofs m1'.(mem_contents)#b1) with (ZMap.get ofs m1.(mem_contents)#b1).
   apply mi_memval0; auto. eapply perm_drop_4; eauto. 
   unfold drop_perm in H0; destruct (range_perm_dec m1 b lo hi Cur Freeable); inv H0; auto.
 Qed.
@@ -2668,10 +2670,11 @@ Proof.
   assert (PERM: forall b0 b3 delta0 ofs k p0,
                 f b0 = Some (b3, delta0) ->
                 perm m1' b0 ofs k p0 -> perm m2' b3 (ofs + delta0) k p0).
+  {
     intros.
     assert (perm m2 b3 (ofs + delta0) k p0).
       eapply mi_perm0; eauto. eapply perm_drop_4; eauto. 
-    destruct (zeq b1 b0).
+    destruct (eq_block b1 b0).
     (* b1 = b0 *)
     subst b0. rewrite H2 in H; inv H.
     destruct (zlt (ofs + delta0) (lo + delta0)). eapply perm_drop_3; eauto.
@@ -2682,7 +2685,7 @@ Proof.
     eapply perm_drop_1. eauto. omega.
     (* b1 <> b0 *)
     eapply perm_drop_3; eauto.
-    destruct (zeq b3 b2); auto.
+    destruct (eq_block b3 b2); auto.
     destruct (zlt (ofs + delta0) (lo + delta)); auto.
     destruct (zle (hi + delta) (ofs + delta0)); auto.
     exploit H1; eauto.
@@ -2691,7 +2694,8 @@ Proof.
     eapply range_perm_drop_1; eauto. omega. auto with mem. 
     eapply perm_drop_4; eauto. eapply perm_max. apply perm_implies with p0. eauto.  
     eauto with mem.
-    unfold block. omega.
+    intuition.
+  }
   constructor.
 (* perm *)
   auto.
@@ -2723,7 +2727,7 @@ Proof.
                 f b0 = Some (b3, delta0) ->
                 perm m1 b0 ofs k p0 -> perm m2' b3 (ofs + delta0) k p0).
     intros. eapply perm_drop_3; eauto. 
-    destruct (zeq b3 b); auto. subst b3. right. 
+    destruct (eq_block b3 b); auto. subst b3. right. 
     destruct (zlt (ofs + delta0) lo); auto.
     destruct (zle hi (ofs + delta0)); auto.
     byContradiction. exploit H1; eauto. omega.
@@ -2973,7 +2977,7 @@ Theorem valid_block_extends:
   extends m1 m2 ->
   (valid_block m1 b <-> valid_block m2 b).
 Proof.
-  intros. inv H. unfold valid_block. rewrite mext_next0. omega. 
+  intros. inv H. unfold valid_block. rewrite mext_next0. tauto. 
 Qed.
 
 Theorem perm_extends:
@@ -3039,7 +3043,7 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop :=
     mi_representable:
       forall b b' delta ofs,
       f b = Some(b', delta) ->
-      weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+      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
   }.
 Definition inject := inject'.
@@ -3054,7 +3058,7 @@ Theorem valid_block_inject_1:
   inject f m1 m2 ->
   valid_block m1 b1.
 Proof.
-  intros. inv H. destruct (zlt b1 (nextblock m1)). auto. 
+  intros. inv H. destruct (plt b1 (nextblock m1)). auto. 
   assert (f b1 = None). eapply mi_freeblocks; eauto. congruence.
 Qed.
 
@@ -3125,21 +3129,6 @@ Qed.
 (** The following lemmas establish the absence of machine integer overflow
   during address computations. *)
 
-(*
-Lemma address_no_overflow:
-  forall f m1 m2 b1 b2 delta ofs1 k p,
-  inject f m1 m2 ->
-  perm m1 b1 (Int.unsigned ofs1) k p ->
-  f b1 = Some (b2, delta) ->
-  0 <= Int.unsigned ofs1 + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
-Proof.
-  intros. exploit mi_representable; eauto. intros [A | [A B]].
-  subst delta. change (Int.unsigned (Int.repr 0)) with 0. 
-  rewrite Zplus_0_r. apply Int.unsigned_range_2.
-  rewrite Int.unsigned_repr; auto. 
-Qed.
-*)
-
 Lemma address_inject:
   forall f m1 m2 b1 ofs1 b2 delta p,
   inject f m1 m2 ->
@@ -3147,9 +3136,8 @@ Lemma address_inject:
   f b1 = Some (b2, delta) ->
   Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 Proof.
-  intros. apply (perm_implies _ _ _ _ _ Nonempty) in H0; [| constructor].
-  rewrite <-valid_pointer_nonempty_perm in H0.
-  apply valid_pointer_implies in H0.
+  intros.
+  assert (perm m1 b1 (Int.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.
@@ -3174,7 +3162,10 @@ Theorem weak_valid_pointer_inject_no_overflow:
   f b = Some(b', delta) ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 Proof.
-  intros. exploit mi_representable; eauto. intros.
+  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.
 Qed.
@@ -3209,9 +3200,13 @@ Theorem weak_valid_pointer_inject_val:
   val_inject f (Vptr b ofs) (Vptr b' ofs') ->
   weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
 Proof.
-  intros. inv H1. exploit mi_representable; try eassumption. intros.
+  intros. inv H1.
+  exploit weak_valid_pointer_inject; eauto. intros W.
+  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).
-  exploit weak_valid_pointer_inject; eauto.
   unfold Int.add. repeat rewrite Int.unsigned_repr; auto; omega.
 Qed.
 
@@ -3279,7 +3274,7 @@ Proof.
   exploit mi_no_overlap; eauto. 
   instantiate (1 := x - delta1). apply H2. omega.
   instantiate (1 := x - delta2). apply H3. omega.
-  unfold block; omega. 
+  intuition. 
 Qed.
 
 Theorem aligned_area_inject:
@@ -3371,8 +3366,6 @@ Proof.
   red; intros. eauto with mem.
 (* representable *)
   intros. eapply mi_representable; try eassumption.
-  rewrite weak_valid_pointer_spec in *.
-  rewrite !valid_pointer_nonempty_perm in H4 |- *.
   destruct H4; eauto with mem.
 Qed.
 
@@ -3395,8 +3388,6 @@ Proof.
   red; intros. eauto with mem.
 (* representable *)
   intros. eapply mi_representable; try eassumption.
-  rewrite weak_valid_pointer_spec in *.
-  rewrite !valid_pointer_nonempty_perm in H3 |- *.
   destruct H3; eauto with mem.
 Qed.
 
@@ -3463,8 +3454,6 @@ Proof.
   red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. 
 (* representable *)
   intros. eapply mi_representable0; eauto.
-  rewrite weak_valid_pointer_spec in *.
-  rewrite !valid_pointer_nonempty_perm in H4 |- *.
   destruct H4; eauto using perm_storebytes_2. 
 Qed.
 
@@ -3487,8 +3476,6 @@ Proof.
   red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. 
 (* representable *)
   intros. eapply mi_representable0; eauto.
-  rewrite weak_valid_pointer_spec in *.
-  rewrite !valid_pointer_nonempty_perm in H3 |- *.
   destruct H3; eauto using perm_storebytes_2.
 Qed.
 
@@ -3548,44 +3535,42 @@ Theorem alloc_left_unmapped_inject:
   /\ (forall b, b <> b1 -> f' b = f b).
 Proof.
   intros. inversion H.
-  set (f' := fun b => if zeq b b1 then None else f b).
+  set (f' := fun b => if eq_block b b1 then None else f b).
   assert (inject_incr f f').
-    red; unfold f'; intros. destruct (zeq b b1). subst b.
+    red; unfold f'; intros. destruct (eq_block b b1). subst b.
     assert (f b1 = None). eauto with mem. congruence.
     auto.
   assert (mem_inj f' m1 m2).
     inversion mi_inj0; constructor; eauto with mem.
-    unfold f'; intros. destruct (zeq b0 b1). congruence. eauto.
-    unfold f'; intros. destruct (zeq b0 b1). congruence. eauto.
-    unfold f'; intros. destruct (zeq b0 b1). congruence. 
+    unfold f'; intros. destruct (eq_block b0 b1). congruence. eauto.
+    unfold f'; intros. destruct (eq_block b0 b1). congruence. eauto.
+    unfold f'; intros. destruct (eq_block b0 b1). congruence. 
     apply memval_inject_incr with f; auto. 
   exists f'; split. constructor.
 (* inj *)
-  eapply alloc_left_unmapped_inj; eauto. unfold f'; apply zeq_true. 
+  eapply alloc_left_unmapped_inj; eauto. unfold f'; apply dec_eq_true. 
 (* freeblocks *)
-  intros. unfold f'. destruct (zeq b b1). auto. 
+  intros. unfold f'. destruct (eq_block b b1). auto. 
   apply mi_freeblocks0. red; intro; elim H3. eauto with mem. 
 (* mappedblocks *)
-  unfold f'; intros. destruct (zeq b b1). congruence. eauto. 
+  unfold f'; intros. destruct (eq_block b b1). congruence. eauto. 
 (* no overlap *)
   unfold f'; red; intros.
-  destruct (zeq b0 b1); destruct (zeq b2 b1); try congruence.
+  destruct (eq_block b0 b1); destruct (eq_block b2 b1); try congruence.
   eapply mi_no_overlap0. eexact H3. eauto. eauto.
-  exploit perm_alloc_inv. eauto. eexact H6. rewrite zeq_false; auto. 
-  exploit perm_alloc_inv. eauto. eexact H7. rewrite zeq_false; auto. 
+  exploit perm_alloc_inv. eauto. eexact H6. rewrite dec_eq_false; auto.  
+  exploit perm_alloc_inv. eauto. eexact H7. rewrite dec_eq_false; auto. 
 (* representable *)
   unfold f'; intros.
-  destruct (zeq b b1); try discriminate.
+  destruct (eq_block b b1); try discriminate.
   eapply mi_representable0; try eassumption.
-  rewrite weak_valid_pointer_spec in *.
-  rewrite !valid_pointer_nonempty_perm in H4 |- *.
   destruct H4; eauto using perm_alloc_4.
 (* incr *)
   split. auto. 
 (* image *)
-  split. unfold f'; apply zeq_true. 
+  split. unfold f'; apply dec_eq_true. 
 (* incr *)
-  intros; unfold f'; apply zeq_false; auto.
+  intros; unfold f'; apply dec_eq_false; auto.
 Qed.
 
 Theorem alloc_left_mapped_inject:
@@ -3608,68 +3593,65 @@ Theorem alloc_left_mapped_inject:
   /\ (forall b, b <> b1 -> f' b = f b).
 Proof.
   intros. inversion H.
-  set (f' := fun b => if zeq b b1 then Some(b2, delta) else f b).
+  set (f' := fun b => if eq_block b b1 then Some(b2, delta) else f b).
   assert (inject_incr f f').
-    red; unfold f'; intros. destruct (zeq b b1). subst b.
+    red; unfold f'; intros. destruct (eq_block b b1). subst b.
     assert (f b1 = None). eauto with mem. congruence.
     auto.
   assert (mem_inj f' m1 m2).
     inversion mi_inj0; constructor; eauto with mem.
-    unfold f'; intros. destruct (zeq b0 b1).
+    unfold f'; intros. destruct (eq_block b0 b1).
       inversion H8. subst b0 b3 delta0. 
       elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem.
       eauto.
-    unfold f'; intros. destruct (zeq b0 b1).
+    unfold f'; intros. destruct (eq_block b0 b1).
       inversion H8. subst b0 b3 delta0. 
       elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem.
       eauto.
-    unfold f'; intros. destruct (zeq b0 b1).
+    unfold f'; intros. destruct (eq_block b0 b1).
       inversion H8. subst b0 b3 delta0. 
       elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem.
       apply memval_inject_incr with f; auto. 
   exists f'. split. constructor.
 (* inj *)
-  eapply alloc_left_mapped_inj; eauto. unfold f'; apply zeq_true. 
+  eapply alloc_left_mapped_inj; eauto. unfold f'; apply dec_eq_true. 
 (* freeblocks *)
-  unfold f'; intros. destruct (zeq b b1). subst b. 
+  unfold f'; intros. destruct (eq_block b b1). subst b. 
   elim H9. eauto with mem.
   eauto with mem.
 (* mappedblocks *)
-  unfold f'; intros. destruct (zeq b b1). congruence. eauto.
+  unfold f'; intros. destruct (eq_block b b1). congruence. eauto.
 (* overlap *)
   unfold f'; red; intros.
   exploit perm_alloc_inv. eauto. eexact H12. intros P1.
   exploit perm_alloc_inv. eauto. eexact H13. intros P2.
-  destruct (zeq b0 b1); destruct (zeq b3 b1).
+  destruct (eq_block b0 b1); destruct (eq_block b3 b1).
   congruence.
   inversion H10; subst b0 b1' delta1. 
-    destruct (zeq b2 b2'); auto. subst b2'. right; red; intros.
+    destruct (eq_block b2 b2'); auto. subst b2'. right; red; intros.
     eapply H6; eauto. omega.
   inversion H11; subst b3 b2' delta2. 
-    destruct (zeq b1' b2); auto. subst b1'. right; red; intros.
+    destruct (eq_block b1' b2); auto. subst b1'. right; red; intros.
     eapply H6; eauto. omega.
   eauto.
 (* representable *)
   unfold f'; intros.
-  rewrite weak_valid_pointer_spec in *.
-  rewrite !valid_pointer_nonempty_perm in H10.
-  destruct (zeq b b1).
+  destruct (eq_block b b1).
    subst. injection H9; intros; subst b' delta0. destruct H10.
-    exploit perm_alloc_inv; eauto; rewrite zeq_true; intro.
-    exploit H3. apply H4 with (k := Cur) (p := Nonempty); eauto.
+    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.
-   exploit perm_alloc_inv; eauto; rewrite zeq_true; intro.
-   exploit H3. apply H4 with (k := Cur) (p := Nonempty); eauto.
+   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.
   eapply mi_representable0; try eassumption.
-  rewrite !weak_valid_pointer_spec, !valid_pointer_nonempty_perm.
   destruct H10; eauto using perm_alloc_4.
 (* incr *)
   split. auto.
 (* image of b1 *)
-  split. unfold f'; apply zeq_true. 
+  split. unfold f'; apply dec_eq_true. 
 (* image of others *)
-  intros. unfold f'; apply zeq_false; auto. 
+  intros. unfold f'; apply dec_eq_false; auto. 
 Qed.
 
 Theorem alloc_parallel_inject:
@@ -3719,8 +3701,6 @@ Proof.
   red; intros. eauto with mem. 
 (* representable *)
   intros. eapply mi_representable0; try eassumption.
-  rewrite weak_valid_pointer_spec in *.
-  rewrite !valid_pointer_nonempty_perm in H2 |- *.
   destruct H2; eauto with mem.
 Qed.
 
@@ -3732,9 +3712,9 @@ Lemma free_list_left_inject:
 Proof.
   induction l; simpl; intros. 
   inv H0. auto.
-  destruct a as [[b lo] hi]. generalize H0. case_eq (free m1 b lo hi); intros.
-  apply IHl with m; auto. eapply free_left_inject; eauto.
-  congruence.
+  destruct a as [[b lo] hi].
+  destruct (free m1 b lo hi) as [m11|] eqn:E; try discriminate.
+  apply IHl with m11; auto. eapply free_left_inject; eauto.
 Qed.
 
 Lemma free_right_inject:
@@ -3766,14 +3746,14 @@ Lemma perm_free_list:
   perm m b ofs k p /\ 
   (forall lo hi, In (b, lo, hi) l -> lo <= ofs < hi -> False).
 Proof.
-  induction l; intros until p; simpl.
-  intros. inv H. split; auto. 
+  induction l; simpl; intros.
+  inv H. auto. 
   destruct a as [[b1 lo1] hi1].
-  case_eq (free m b1 lo1 hi1); intros; try congruence.
+  destruct (free m b1 lo1 hi1) as [m1|] eqn:E; try discriminate.
   exploit IHl; eauto. intros [A B].
   split. eauto with mem.
-  intros. destruct H2. inv H2.
-  elim (perm_free_2 _ _ _ _ _ H ofs k p). auto. auto.
+  intros. destruct H1. inv H1.
+  elim (perm_free_2 _ _ _ _ _ E ofs k p). auto. auto.
   eauto.
 Qed.
 
@@ -3861,7 +3841,7 @@ Proof.
   exploit mi_no_overlap1. eauto. eauto. eauto.
     eapply perm_inj. eauto. eexact H2. eauto. 
     eapply perm_inj. eauto. eexact H3. eauto. 
-  unfold block; omega.
+  intuition omega.
 (* representable *)
   intros. 
   destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate.
@@ -3872,7 +3852,6 @@ Proof.
     unfold ofs'; apply Int.unsigned_repr. auto.
   exploit mi_representable1. eauto. instantiate (1 := ofs').
   rewrite H.
-  rewrite weak_valid_pointer_spec, !valid_pointer_nonempty_perm in *.
   replace (Int.unsigned ofs + delta1 - 1) with
     ((Int.unsigned ofs - 1) + delta1) by omega.
   destruct H0; eauto using perm_inj.
@@ -3910,7 +3889,6 @@ Proof.
   red; intros. eapply mi_no_overlap0; eauto; eapply perm_extends; eauto.
 (* representable *)
   eapply mi_representable0; eauto.
-  rewrite weak_valid_pointer_spec, !valid_pointer_nonempty_perm in *.
   destruct H1; eauto using perm_extends.
 Qed.
 
@@ -3949,7 +3927,7 @@ Qed.
 (** Injecting a memory into itself. *)
 
 Definition flat_inj (thr: block) : meminj :=
-  fun (b: block) => if zlt b thr then Some(b, 0) else None.
+  fun (b: block) => if plt b thr then Some(b, 0) else None.
 
 Definition inject_neutral (thr: block) (m: mem) :=
   mem_inj (flat_inj thr) m m.
@@ -3958,8 +3936,8 @@ Remark flat_inj_no_overlap:
   forall thr m, meminj_no_overlap (flat_inj thr) m.
 Proof.
   unfold flat_inj; intros; red; intros.
-  destruct (zlt b1 thr); inversion H0; subst.
-  destruct (zlt b2 thr); inversion H1; subst.
+  destruct (plt b1 thr); inversion H0; subst.
+  destruct (plt b2 thr); inversion H1; subst.
   auto.
 Qed.
 
@@ -3971,15 +3949,15 @@ Proof.
   auto.
 (* freeblocks *)
   unfold flat_inj, valid_block; intros.
-  apply zlt_false. omega.
+  apply pred_dec_false. auto. 
 (* mappedblocks *)
   unfold flat_inj, valid_block; intros. 
-  destruct (zlt b (nextblock m)); inversion H0; subst. auto.
+  destruct (plt b (nextblock m)); inversion H0; subst. auto.
 (* no overlap *)
   apply flat_inj_no_overlap.
 (* range *)
   unfold flat_inj; intros.
-  destruct (zlt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega.
+  destruct (plt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega.
 Qed.
 
 Theorem empty_inject_neutral:
@@ -3987,20 +3965,20 @@ Theorem empty_inject_neutral:
 Proof.
   intros; red; constructor.
 (* perm *)
-  unfold flat_inj; intros. destruct (zlt b1 thr); inv H.
+  unfold flat_inj; intros. destruct (plt b1 thr); inv H.
   replace (ofs + 0) with ofs by omega; auto.
 (* access *)
-  unfold flat_inj; intros. destruct (zlt b1 thr); inv H.
+  unfold flat_inj; intros. destruct (plt b1 thr); inv H.
   replace (ofs + 0) with ofs by omega; auto.
 (* mem_contents *)
-  intros; simpl. repeat rewrite ZMap.gi. constructor.
+  intros; simpl. rewrite ! PMap.gi. rewrite ! ZMap.gi. constructor.
 Qed.
 
 Theorem alloc_inject_neutral:
   forall thr m lo hi b m',
   alloc m lo hi = (m', b) ->
   inject_neutral thr m ->
-  nextblock m < thr ->
+  Plt (nextblock m) thr ->
   inject_neutral thr m'.
 Proof.
   intros; red. 
@@ -4010,7 +3988,7 @@ Proof.
   intros.
   apply perm_implies with Freeable; auto with mem.
   eapply perm_alloc_2; eauto. omega. 
-  unfold flat_inj. apply zlt_true. 
+  unfold flat_inj. apply pred_dec_true.  
   rewrite (alloc_result _ _ _ _ _ H). auto.
 Qed.
 
@@ -4018,13 +3996,13 @@ Theorem store_inject_neutral:
   forall chunk m b ofs v m' thr,
   store chunk m b ofs v = Some m' ->
   inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   val_inject (flat_inj thr) v v ->
   inject_neutral thr m'.
 Proof.
   intros; red.
   exploit store_mapped_inj. eauto. eauto. apply flat_inj_no_overlap. 
-  unfold flat_inj. apply zlt_true; auto. eauto.
+  unfold flat_inj. apply pred_dec_true; auto. eauto.
   replace (ofs + 0) with ofs by omega.  
   intros [m'' [A B]]. congruence.
 Qed. 
@@ -4033,15 +4011,152 @@ Theorem drop_inject_neutral:
   forall m b lo hi p m' thr,
   drop_perm m b lo hi p = Some m' ->
   inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   inject_neutral thr m'.
 Proof.
   unfold inject_neutral; intros.
   exploit drop_mapped_inj; eauto. apply flat_inj_no_overlap. 
-  unfold flat_inj. apply zlt_true; eauto. 
+  unfold flat_inj. apply pred_dec_true; eauto. 
   repeat rewrite Zplus_0_r. intros [m'' [A B]]. congruence.
 Qed.
 
+(** * Invariance properties between two memory states *)
+
+Section UNCHANGED_ON.
+
+Variable P: block -> Z -> Prop.
+
+Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
+  unchanged_on_perm:
+    forall b ofs k p,
+    P b ofs -> valid_block m_before b ->
+    (perm m_before b ofs k p <-> perm m_after b ofs k p);
+  unchanged_on_contents:
+    forall b ofs,
+    P b ofs -> perm m_before b ofs Cur Readable ->
+    ZMap.get ofs (PMap.get b m_after.(mem_contents)) =
+    ZMap.get ofs (PMap.get b m_before.(mem_contents))
+}.
+
+Lemma unchanged_on_refl:
+  forall m, unchanged_on m m.
+Proof.
+  intros; constructor; tauto.
+Qed.
+
+Lemma perm_unchanged_on:
+  forall m m' b ofs k p,
+  unchanged_on m m' -> P b ofs -> valid_block m b ->
+  perm m b ofs k p -> perm m' b ofs k p.
+Proof.
+  intros. destruct H. apply unchanged_on_perm0; auto. 
+Qed.
+
+Lemma perm_unchanged_on_2:
+  forall m m' b ofs k p,
+  unchanged_on m m' -> P b ofs -> valid_block m b ->
+  perm m' b ofs k p -> perm m b ofs k p.
+Proof.
+  intros. destruct H. apply unchanged_on_perm0; auto. 
+Qed.
+
+Lemma loadbytes_unchanged_on:
+  forall m m' b ofs n bytes,
+  unchanged_on m m' ->
+  (forall i, ofs <= i < ofs + n -> P b i) ->
+  loadbytes m b ofs n = Some bytes ->
+  loadbytes m' b ofs n = Some bytes.
+Proof.
+  intros. 
+  destruct (zle n 0).
++ erewrite loadbytes_empty in * by assumption. auto.
++ unfold loadbytes in *. destruct H.
+  destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); inv H1.
+  assert (valid_block m b). 
+  { eapply perm_valid_block. apply (r ofs). omega. } 
+  assert (range_perm m' b ofs (ofs + n) Cur Readable).
+  { red; intros. apply unchanged_on_perm0; auto. } 
+  rewrite pred_dec_true by assumption. f_equal.
+  apply getN_exten. intros. rewrite nat_of_Z_eq in H2 by omega.
+  apply unchanged_on_contents0; auto.
+Qed.
+
+Lemma load_unchanged_on:
+  forall m m' chunk b ofs v,
+  unchanged_on m m' ->
+  (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) ->
+  load chunk m b ofs = Some v ->
+  load chunk m' b ofs = Some v.
+Proof.
+  intros. 
+  exploit load_valid_access; eauto. intros [A B].
+  exploit load_loadbytes; eauto. intros [bytes [C D]].
+  subst v. apply loadbytes_load; auto. eapply loadbytes_unchanged_on; eauto.
+Qed.
+
+Lemma store_unchanged_on:
+  forall chunk m b ofs v m',
+  store chunk m b ofs v = Some m' ->
+  (forall i, ofs <= i < ofs + size_chunk chunk -> ~ P b i) ->
+  unchanged_on m m'.
+Proof.
+  intros; constructor; intros.
+- split; intros; eauto with mem.
+- erewrite store_mem_contents; eauto. rewrite PMap.gsspec. 
+  destruct (peq b0 b); auto. subst b0. apply setN_outside. 
+  rewrite encode_val_length. rewrite <- size_chunk_conv. 
+  destruct (zlt ofs0 ofs); auto. 
+  destruct (zlt ofs0 (ofs + size_chunk chunk)); auto.
+  elim (H0 ofs0). omega. auto.
+Qed.
+
+Lemma storebytes_unchanged_on:
+  forall m b ofs bytes m',
+  storebytes m b ofs bytes = Some m' ->
+  (forall i, ofs <= i < ofs + Z_of_nat (length bytes) -> ~ P b i) ->
+  unchanged_on m m'.
+Proof.
+  intros; constructor; intros.
+- split; intros. eapply perm_storebytes_1; eauto. eapply perm_storebytes_2; eauto. 
+- erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec. 
+  destruct (peq b0 b); auto. subst b0. apply setN_outside. 
+  destruct (zlt ofs0 ofs); auto. 
+  destruct (zlt ofs0 (ofs + Z_of_nat (length bytes))); auto.
+  elim (H0 ofs0). omega. auto.
+Qed.
+
+Lemma alloc_unchanged_on:
+  forall m lo hi m' b, 
+  alloc m lo hi = (m', b) ->
+  unchanged_on m m'.
+Proof.
+  intros; constructor; intros.
+- split; intros.
+  eapply perm_alloc_1; eauto.
+  eapply perm_alloc_4; eauto. 
+  eapply valid_not_valid_diff; eauto with mem.
+- injection H; intros A B. rewrite <- B; simpl.
+  rewrite PMap.gso; auto. rewrite A.  eapply valid_not_valid_diff; eauto with mem.
+Qed.
+
+Lemma free_unchanged_on:
+  forall m b lo hi m',
+  free m b lo hi = Some m' ->
+  (forall i, lo <= i < hi -> ~ P b i) ->
+  unchanged_on m m'.
+Proof.
+  intros; constructor; intros.
+- split; intros. 
+  eapply perm_free_1; eauto. 
+  destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto. 
+  subst b0. elim (H0 ofs). omega. auto.
+  eapply perm_free_3; eauto.
+- unfold free in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H.
+  simpl. auto.
+Qed.
+
+End UNCHANGED_ON.
+
 End Mem.
 
 Notation mem := Mem.mem.
@@ -4105,4 +4220,5 @@ Hint Resolve
   Mem.valid_access_free_2
   Mem.valid_access_free_inv_1
   Mem.valid_access_free_inv_2
+  Mem.unchanged_on_refl
 : mem.
diff --git a/common/Memtype.v b/common/Memtype.v
index 59dc7a3..37ab33c 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -88,8 +88,6 @@ Module Type MEM.
 (** The abstract type of memory states. *)
 Parameter mem: Type.
 
-Definition nullptr: block := 0.
-
 (** * Operations on memory states *)
 
 (** [empty] is the initial memory state. *)
@@ -176,11 +174,9 @@ Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), opti
   block. *)
 
 Parameter nextblock: mem -> block.
-Axiom nextblock_pos:
-  forall m, nextblock m > 0.
 
-Definition valid_block (m: mem) (b: block) :=
-  b < nextblock m.
+Definition valid_block (m: mem) (b: block) := Plt b (nextblock m).
+
 Axiom valid_not_valid_diff:
   forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
 
@@ -279,7 +275,7 @@ Axiom valid_pointer_implies:
 
 (** ** Properties of the initial memory state. *)
 
-Axiom nextblock_empty: nextblock empty = 1.
+Axiom nextblock_empty: nextblock empty = 1%positive.
 Axiom perm_empty: forall b ofs k p, ~perm empty b ofs k p.
 Axiom valid_access_empty:
   forall chunk b ofs p, ~valid_access empty chunk b ofs p.
@@ -607,7 +603,7 @@ Axiom alloc_result:
 
 Axiom nextblock_alloc:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  nextblock m2 = Zsucc (nextblock m1).
+  nextblock m2 = Psucc (nextblock m1).
 
 Axiom valid_block_alloc:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
@@ -640,7 +636,7 @@ Axiom perm_alloc_inv:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
   forall b' ofs k p, 
   perm m2 b' ofs k p ->
-  if zeq b' b then lo <= ofs < hi else perm m1 b' ofs k p.
+  if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p.
 
 (** Effect of [alloc] on access validity. *)
 
@@ -1191,7 +1187,7 @@ Axiom drop_outside_inject:
 (** Memory states that inject into themselves. *)
 
 Definition flat_inj (thr: block) : meminj :=
-  fun (b: block) => if zlt b thr then Some(b, 0) else None.
+  fun (b: block) => if plt b thr then Some(b, 0) else None.
 
 Parameter inject_neutral: forall (thr: block) (m: mem), Prop.
 
@@ -1206,14 +1202,14 @@ Axiom alloc_inject_neutral:
   forall thr m lo hi b m',
   alloc m lo hi = (m', b) ->
   inject_neutral thr m ->
-  nextblock m < thr ->
+  Plt (nextblock m) thr ->
   inject_neutral thr m'.
 
 Axiom store_inject_neutral:
   forall chunk m b ofs v m' thr,
   store chunk m b ofs v = Some m' ->
   inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   val_inject (flat_inj thr) v v ->
   inject_neutral thr m'.
 
@@ -1221,7 +1217,7 @@ Axiom drop_inject_neutral:
   forall m b lo hi p m' thr,
   drop_perm m b lo hi p = Some m' ->
   inject_neutral thr m ->
-  b < thr ->
+  Plt b thr ->
   inject_neutral thr m'.
 
 End MEM.
diff --git a/common/Values.v b/common/Values.v
index bb97cdc..7caf551 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -21,8 +21,8 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 
-Definition block : Type := Z.
-Definition eq_block := zeq.
+Definition block : Type := positive.
+Definition eq_block := peq.
 
 (** A value is either:
 - a machine integer;
@@ -212,7 +212,7 @@ Definition sub (v1 v2: val): val :=
   | Vint n1, Vint n2 => Vint(Int.sub n1 n2)
   | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.sub ofs1 n2)
   | Vptr b1 ofs1, Vptr b2 ofs2 =>
-      if zeq b1 b2 then Vint(Int.sub ofs1 ofs2) else Vundef
+      if eq_block b1 b2 then Vint(Int.sub ofs1 ofs2) else Vundef
   | _, _ => Vundef
   end.
 
@@ -568,7 +568,7 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
   | Vint n1, Vptr b2 ofs2 =>
       if Int.eq n1 Int.zero then cmp_different_blocks c else None
   | Vptr b1 ofs1, Vptr b2 ofs2 =>
-      if zeq b1 b2 then
+      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)
@@ -785,7 +785,7 @@ Proof.
   destruct v1; destruct v2; intros; simpl; auto.
   rewrite Int.sub_add_l. auto.
   rewrite Int.sub_add_l. auto.
-  case (zeq b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.
+  case (eq_block b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.
 Qed.
 
 Theorem sub_add_r:
@@ -797,7 +797,7 @@ Proof.
   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 (zeq b b0); intro. simpl. decEq. 
+  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.
@@ -1037,7 +1037,7 @@ Proof.
   rewrite Int.negate_cmpu. auto.
   destruct (Int.eq i Int.zero); auto. 
   destruct (Int.eq i0 Int.zero); auto.
-  destruct (zeq b b0).
+  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.
@@ -1084,13 +1084,13 @@ Proof.
   rewrite Int.swap_cmpu. auto.
   case (Int.eq i Int.zero); auto.
   case (Int.eq i0 Int.zero); auto.
-  destruct (zeq b b0); subst.
-  rewrite zeq_true.
+  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));
   simpl; auto.
   rewrite Int.swap_cmpu. auto.
-  rewrite zeq_false by auto.
+  rewrite dec_eq_false by auto.
   destruct (valid_ptr b (Int.unsigned i));
     destruct (valid_ptr b0 (Int.unsigned i0)); simpl; auto.
 Qed.
@@ -1286,7 +1286,7 @@ Proof.
   destruct v1; simpl in H2; try discriminate;
   destruct v2; simpl in H2; try discriminate;
   inv H0; inv H1; simpl; auto.
-  destruct (zeq b0 b1).
+  destruct (eq_block b0 b1).
   assert (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. 
@@ -1401,7 +1401,7 @@ Remark val_sub_inject:
 Proof.
   intros. inv H; inv H0; simpl; auto.
   econstructor; eauto. rewrite Int.sub_add_l. auto.
-  destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true.
+  destruct (eq_block b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite dec_eq_true. 
   rewrite Int.sub_shifted. auto.
 Qed.
 
@@ -1461,15 +1461,15 @@ Proof.
   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)))). 
-  destruct (zeq b1 b0); subst.
-  rewrite H in H2. inv H2. rewrite zeq_true.
+  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.
   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.
-  destruct (zeq b2 b3); subst.
+  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.