Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


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

4 files changed, 1182 insertions, 1355 deletions

diff --git a/common/Events.v b/common/Events.v
index 3d082a7..93e1827 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -560,23 +560,22 @@ 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 p,
-   P b ofs -> Mem.perm m_before b ofs p -> Mem.perm m_after b ofs p)
+  (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 :=
-  ofs < Mem.low_bound m b \/ ofs > Mem.high_bound m b.
+  ~Mem.perm m b ofs Max Nonempty.
 
 Definition loc_unmapped (f: meminj) (b: block) (ofs: Z): Prop :=
   f b = None.
 
 Definition loc_out_of_reach (f: meminj) (m: mem) (b: block) (ofs: Z): Prop :=
   forall b0 delta,
-  f b0 = Some(b, delta) ->
-  ofs < Mem.low_bound m b0 + delta \/ ofs >= Mem.high_bound m b0 + delta.
+  f b0 = Some(b, delta) -> ~Mem.perm m b0 (ofs - delta) Max Nonempty.
 
 Definition inject_separated (f f': meminj) (m1 m2: mem): Prop :=
   forall b1 b2 delta,
@@ -613,11 +612,22 @@ Record extcall_properties (sem: extcall_sem)
     sem F V ge vargs m1 t vres m2 ->
     Mem.valid_block m1 b -> Mem.valid_block m2 b;
 
-(** External calls preserve the bounds of valid blocks. *)
-  ec_bounds:
-    forall F V (ge: Genv.t F V) vargs m1 t vres m2 b,
+(** External calls cannot increase the max permissions of a valid block.
+    They can decrease the max permissions, e.g. by freeing. *)
+  ec_max_perm:
+    forall F V (ge: Genv.t F V) vargs m1 t vres m2 b ofs p,
+    sem F V ge vargs m1 t vres m2 ->
+    Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p;
+
+(** External call cannot modify memory unless they have [Max, Writable]
+   permissions. *)
+  ec_readonly:
+    forall F V (ge: Genv.t F V) vargs m1 t vres m2 chunk b ofs,
     sem F V ge vargs m1 t vres m2 ->
-    Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b;
+    Mem.valid_block m1 b ->
+    (forall ofs', ofs <= ofs' < ofs + size_chunk chunk ->
+                          ~(Mem.perm m1 b ofs' Max Writable)) ->
+    Mem.load chunk m2 b ofs = Mem.load chunk m1 b ofs;
 
 (** External calls must commute with memory extensions, in the
   following sense. *)
@@ -759,7 +769,9 @@ Proof.
   inv H1. constructor. eapply volatile_load_preserved; eauto. 
 (* valid blocks *)
   inv H; auto.
-(* bounds *)
+(* max perms *)
+  inv H; auto.
+(* readonly *)
   inv H; auto.
 (* mem extends *)
   inv H. inv H1. inv H6. inv H4. 
@@ -821,7 +833,9 @@ Proof.
   inv H1. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. 
 (* valid blocks *)
   inv H; auto.
-(* bounds *)
+(* max perm *)
+  inv H; auto.
+(* readonly *)
   inv H; auto.
 (* extends *)
   inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]].
@@ -867,6 +881,28 @@ Proof.
   rewrite H0; auto.
 Qed.
 
+Lemma volatile_store_readonly:
+  forall F V (ge: Genv.t F V) chunk1 m1 b1 ofs1 v t m2 chunk ofs b,
+  volatile_store ge chunk1 m1 b1 ofs1 v t m2 ->
+  Mem.valid_block m1 b ->
+  (forall ofs', ofs <= ofs' < ofs + size_chunk chunk ->
+                        ~(Mem.perm m1 b ofs' Max Writable)) ->
+  Mem.load chunk m2 b ofs = Mem.load chunk m1 b ofs.
+Proof.
+  intros. inv H.
+  auto.
+  eapply Mem.load_store_other; eauto.
+  destruct (eq_block b b1); auto. subst b1. right.
+  apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk)
+                              (Int.unsigned ofs1, Int.unsigned ofs1 + size_chunk chunk1)).
+  red; intros; red; intros. 
+  elim (H1 x); auto. 
+  exploit Mem.store_valid_access_3; eauto. intros [A B].
+  apply Mem.perm_cur_max. apply A. auto.
+  simpl. generalize (size_chunk_pos chunk); omega.
+  simpl. generalize (size_chunk_pos chunk1); omega.
+Qed.
+
 Lemma volatile_store_extends:
   forall F V (ge: Genv.t F V) chunk m1 b ofs v t m2 m1' v',
   volatile_store ge chunk m1 b ofs v t m2 ->
@@ -886,15 +922,14 @@ Proof.
   eapply Mem.perm_store_1; eauto.
   rewrite <- H4. eapply Mem.load_store_other; eauto.
   destruct (eq_block b0 b); auto. subst b0; right. 
-  exploit Mem.valid_access_in_bounds. 
-  eapply Mem.store_valid_access_3. eexact H3.
-  intros [C D].
-  generalize (size_chunk_pos chunk0). intro E.
-  generalize (size_chunk_pos chunk). intro G.
   apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
                               (Int.unsigned ofs, Int.unsigned ofs + size_chunk chunk)).
-  red; intros. generalize (H x H5). unfold loc_out_of_bounds, Intv.In; simpl. omega.
-  simpl; omega. simpl; omega.
+  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.
 Qed.
 
 Lemma volatile_store_inject:
@@ -929,15 +964,15 @@ Proof.
   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.
-  exploit Mem.valid_access_in_bounds. 
-  eapply Mem.store_valid_access_3. eexact H0.
-  intros [C D].
-  generalize (size_chunk_pos chunk0). intro E.
-  generalize (size_chunk_pos chunk). intro G.
   apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
                               (Int.unsigned ofs + delta, Int.unsigned ofs + delta + size_chunk chunk)).
-  red; intros. exploit (H1 x H7). eauto. unfold Intv.In; simpl. omega.
-  simpl; omega. simpl; omega.
+  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.
 Qed.
 
 Lemma volatile_store_receptive:
@@ -961,8 +996,10 @@ Proof.
   inv H1. constructor. eapply volatile_store_preserved; eauto. 
 (* valid block *)
   inv H. inv H1. auto. eauto with mem.
-(* bounds *)
-  inv H. inv H1. auto. eapply Mem.bounds_store; eauto.
+(* perms *)
+  inv H. inv H2. auto. eauto with mem. 
+(* readonly *)
+  inv H. eapply volatile_store_readonly; eauto.
 (* mem extends*)
   inv H. inv H1. inv H6. inv H7. inv H4.
   exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. 
@@ -1016,8 +1053,10 @@ Proof.
   inv H1. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. 
 (* valid block *)
   inv H. inv H2. auto. eauto with mem.
-(* bounds *)
-  inv H. inv H2. auto. eapply Mem.bounds_store; eauto.
+(* perms *)
+  inv H. inv H3. auto. eauto with mem. 
+(* readonly *)
+  inv H. eapply volatile_store_readonly; eauto.
 (* mem extends*)
   rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. 
   exploit ec_mem_extends. eapply volatile_store_ok. eexact Q. eauto. eauto. 
@@ -1076,11 +1115,15 @@ Proof.
   inv H1; econstructor; eauto.
 (* valid block *)
   inv H. eauto with mem.
-(* bounds *)
-  inv H. transitivity (Mem.bounds m' b).
-  eapply Mem.bounds_store; eauto.
-  eapply Mem.bounds_alloc_other; eauto.
+(* perms *)
+  inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto.
+  rewrite zeq_false. auto. 
   apply Mem.valid_not_valid_diff with m1; eauto with mem.
+(* readonly *)
+  inv H. transitivity (Mem.load chunk m' b ofs).
+  eapply Mem.load_store_other; eauto. 
+  left. apply Mem.valid_not_valid_diff with m1; eauto with mem.
+  eapply Mem.load_alloc_unchanged; eauto.
 (* mem extends *)
   inv H. inv H1. inv H5. inv H7. 
   exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
@@ -1153,8 +1196,21 @@ Proof.
   inv H1; econstructor; eauto.
 (* valid block *)
   inv H. eauto with mem.
-(* bounds *)
-  inv H. eapply Mem.bounds_free; eauto.
+(* perms *)
+  inv H. eapply Mem.perm_free_3; eauto. 
+(* readonly *)
+  inv H. eapply Mem.load_free; eauto.
+  destruct (eq_block b b0); auto.
+  subst b0. right; right. 
+  apply (Intv.range_disjoint'
+           (ofs, ofs + size_chunk chunk)
+           (Int.unsigned lo - 4, Int.unsigned lo + Int.unsigned sz)).
+  red; intros; red; intros.
+  elim (H1 x). auto. apply Mem.perm_cur_max. 
+  apply Mem.perm_implies with Freeable; auto with mem.
+  exploit Mem.free_range_perm; eauto. 
+  simpl. generalize (size_chunk_pos chunk); omega.
+  simpl. omega.
 (* mem extends *)
   inv H. inv H1. inv H8. inv H6. 
   exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B. 
@@ -1163,19 +1219,20 @@ Proof.
   econstructor; eauto.
   eapply UNCHANGED; eauto. omega. 
   intros. destruct (eq_block b' b); auto. subst b; right.
-  red in H.
-  exploit Mem.range_perm_in_bounds. 
-  eapply Mem.free_range_perm. eexact H4. omega. omega.
+  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.
 (* mem inject *)
   inv H0. inv H2. inv H7. inv H9.
   exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. 
-  assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Freeable).
+  assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable).
     eapply Mem.free_range_perm; eauto.
   exploit Mem.address_inject; eauto. 
-    apply Mem.perm_implies with Freeable; auto with mem.
+    apply Mem.perm_implies with Freeable; auto with mem. apply Mem.perm_cur_max.
     apply H0. instantiate (1 := lo). omega. 
   intro EQ.
-  assert (Mem.range_perm m1' b2 (Int.unsigned lo + delta - 4) (Int.unsigned lo + delta + Int.unsigned sz) Freeable).
+  assert (Mem.range_perm m1' b2 (Int.unsigned lo + delta - 4) (Int.unsigned lo + delta + Int.unsigned sz) Cur Freeable).
     red; intros. 
     replace ofs with ((ofs - delta) + delta) by omega.
     eapply Mem.perm_inject; eauto. apply H0. omega. 
@@ -1194,20 +1251,23 @@ Proof.
   subst b. assert (delta0 = delta) by congruence. subst delta0. 
   exists (Int.unsigned lo - 4); exists (Int.unsigned lo + Int.unsigned sz); split.
   simpl; auto. omega.
-  elimtype False.
-  exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. 
-  instantiate (1 := ofs + delta0 - delta). 
-  apply Mem.perm_implies with Freeable; auto with mem.
-  apply H0. omega. eauto with mem.
+  elimtype False. exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. 
+  instantiate (1 := ofs + delta0 - delta).
+  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.
 
   eapply UNCHANGED; eauto. omega. intros.  
   red in H7. left. congruence. 
 
   eapply UNCHANGED; eauto. omega. intros.
-  destruct (eq_block b' b2); auto. subst b'. right. 
-  red in H7. generalize (H7 _ _ H6). intros. 
-  exploit Mem.range_perm_in_bounds. eexact H0. omega. intros. omega.
+  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.
 
   red; intros. congruence.
 (* trace length *)
@@ -1245,8 +1305,20 @@ Proof.
   intros. inv H1. econstructor; eauto.
 (* valid blocks *)
   intros. inv H. eauto with mem. 
-(* bounds *)
-  intros. inv H. eapply Mem.bounds_storebytes; eauto. 
+(* perms *)
+  intros. inv H. eapply Mem.perm_storebytes_2; eauto. 
+(* readonly *)
+  intros. inv H. eapply Mem.load_storebytes_other; eauto.
+  destruct (eq_block b bdst); auto.   subst b. right.
+  apply (Intv.range_disjoint'
+          (ofs, ofs + size_chunk chunk)
+          (Int.unsigned odst, Int.unsigned odst + Z_of_nat (length bytes))).
+  red; intros; red; intros. elim (H1 x); auto.
+  apply Mem.perm_cur_max. 
+  eapply Mem.storebytes_range_perm; eauto. 
+  simpl. generalize (size_chunk_pos chunk); omega.
+  simpl. rewrite (Mem.loadbytes_length _ _ _ _ _ H8). rewrite nat_of_Z_eq.
+  omega. omega.
 (* extensions *)
   intros. inv H. 
   inv H1. inv H13. inv H14. inv H10. inv H11.
@@ -1262,30 +1334,31 @@ Proof.
   exploit Mem.loadbytes_length. eexact H8. intros.
   rewrite <- H1. eapply Mem.load_storebytes_other; eauto. 
   destruct (eq_block b bdst); auto. subst b; right.
-  exploit Mem.range_perm_in_bounds. eapply Mem.storebytes_range_perm. eexact H9.
-  rewrite H10. rewrite nat_of_Z_eq. omega. omega.
-  intros [P Q].
-  exploit list_forall2_length; eauto. intros R. rewrite R in Q.
+  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; intros. generalize (H x H11). unfold loc_out_of_bounds, Intv.In; simpl. omega.
-  generalize (size_chunk_pos chunk); omega.
-  rewrite <- R; rewrite H10. rewrite nat_of_Z_eq. omega. omega.
+  red; unfold Intv.In; simpl; intros; red; intros.
+  eapply (H x H11).
+  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.
 (* injections *)
   intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12.
   exploit Mem.loadbytes_length; eauto. intros LEN.
-  assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Nonempty).
+  assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Cur Nonempty).
     eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
-  assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Nonempty).
+  assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Cur Nonempty).
     replace sz with (Z_of_nat (length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
     rewrite LEN. apply nat_of_Z_eq. omega.
-  assert (PSRC: Mem.perm m1 bsrc (Int.unsigned osrc) Nonempty).
+  assert (PSRC: Mem.perm m1 bsrc (Int.unsigned osrc) Cur Nonempty).
     apply RPSRC. omega.
-  assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Nonempty).
+  assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Cur Nonempty).
     apply RPDST. omega.
-  exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
-  exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
+  exploit Mem.address_inject.  eauto. apply Mem.perm_cur_max. eexact PSRC. eauto. intros EQ1.
+  exploit Mem.address_inject.  eauto. apply Mem.perm_cur_max. eexact PDST. eauto. intros EQ2.
   exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
   exploit Mem.storebytes_mapped_inject; eauto. intros [m2' [C D]].
   exists f; exists Vundef; exists m2'.
@@ -1293,6 +1366,8 @@ Proof.
   eapply Mem.aligned_area_inject with (m := m1); eauto.
   eapply Mem.aligned_area_inject with (m := m1); eauto.
   eapply Mem.disjoint_or_equal_inject with (m := m1); eauto.
+  apply Mem.range_perm_max with Cur; auto.
+  apply Mem.range_perm_max with Cur; auto.
   split. constructor.
   split. auto.
   split. red; split; intros. eauto with mem. 
@@ -1306,10 +1381,8 @@ Proof.
   rewrite <- (list_forall2_length B). rewrite LEN. rewrite nat_of_Z_eq; try omega.
   apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk)
                               (Int.unsigned odst + delta0, Int.unsigned odst + delta0 + sz)); simpl.
-  red; intros. generalize (H0 x H12). unfold loc_out_of_reach, Intv.In; simpl. 
-  intros. exploit H14; eauto. 
-  exploit Mem.range_perm_in_bounds. eexact RPDST. omega. 
-  omega.
+  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.
   omega.
   split. apply inject_incr_refl.
@@ -1348,7 +1421,9 @@ Proof.
   eapply eventval_match_preserved; eauto. 
 (* valid block *)
   inv H; auto.
-(* bounds *)
+(* perms *)
+  inv H; auto.
+(* readonly *)
   inv H; auto.
 (* mem extends *)
   inv H.
@@ -1403,7 +1478,9 @@ Proof.
   eapply eventval_list_match_preserved; eauto.
 (* valid blocks *)
   inv H; auto.
-(* bounds *)
+(* perms *)
+  inv H; auto.
+(* readonly *)
   inv H; auto.
 (* mem extends *)
   inv H.
@@ -1453,6 +1530,8 @@ Proof.
 
   inv H; auto.
 
+  inv H; auto.
+
   inv H. inv H1. inv H6. 
   exists v2; exists m1'; intuition.
   econstructor; eauto.
@@ -1527,7 +1606,8 @@ Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef).
 Definition external_call_arity ef := ec_arity (external_call_spec ef).
 Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef).
 Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef).
-Definition external_call_bounds ef := ec_bounds (external_call_spec ef).
+Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef).
+Definition external_call_readonly ef := ec_readonly (external_call_spec ef).
 Definition external_call_mem_extends ef := ec_mem_extends (external_call_spec ef).
 Definition external_call_mem_inject ef := ec_mem_inject (external_call_spec ef).
 Definition external_call_trace_length ef := ec_trace_length (external_call_spec ef).
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 539bb77..d7449f9 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -276,6 +276,40 @@ Proof.
   intros. unfold globalenv; eauto. 
 Qed.
 
+Theorem find_var_exists:
+  forall p id gv,
+  list_norepet (prog_var_names p) ->
+  In (id, gv) (prog_vars p) ->
+  exists b,
+     find_symbol (globalenv p) id = Some b
+  /\ find_var_info (globalenv p) b = Some gv.
+Proof.
+  intros until gv.
+  assert (forall vl ge,
+    ~In id (var_names vl) ->
+    (exists b, find_symbol ge id = Some b /\ find_var_info ge b = Some gv) ->
+    (exists b, find_symbol (add_variables ge vl) id = Some b
+           /\  find_var_info (add_variables ge vl) b = Some gv)).
+  induction vl; simpl; intros.
+  auto.
+  apply IHvl. tauto. destruct a as [id1 gv1]. destruct H0 as [b [P Q]].
+  unfold add_variable, find_symbol, find_var_info; simpl. 
+  exists b; split. rewrite PTree.gso. auto. intuition. 
+  rewrite ZMap.gso. auto. exploit genv_vars_range; eauto.
+  unfold ZIndexed.t; omega.
+
+  unfold globalenv, prog_var_names.
+  generalize (prog_vars p) (add_functions empty_genv (prog_funct p)).
+  induction l; simpl; intros.
+  contradiction.
+  destruct a as [id1 gv1]; simpl in *. inv H0.
+  destruct H1. inv H0.
+  apply H; auto.
+  exists (genv_nextvar t0); split.
+  unfold find_symbol, add_variable; simpl. apply PTree.gss.
+  unfold find_var_info, add_variable; simpl. apply ZMap.gss.
+  apply IHl; auto. 
+Qed.  
 
 Remark add_variables_inversion : forall vs e x b,
   find_symbol (add_variables e vs) x = Some b ->
@@ -740,50 +774,63 @@ Qed.
 
 
 Remark store_zeros_perm:
-  forall prm b' q m b n m',
+  forall k prm b' q m b n m',
   store_zeros m b n = Some m' ->
-  Mem.perm m b' q prm -> Mem.perm m' b' q prm.
+  (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
   intros until n. functional induction (store_zeros m b n); intros.
-  inv H; auto.
-  eauto with mem.
+  inv H; tauto.
+  destruct (IHo _ H); intros. split; eauto with mem.
   congruence.
 Qed.
 
 Remark store_init_data_list_perm:
-  forall prm b' q idl b m p m',
+  forall k prm b' q idl b m p m',
   store_init_data_list m b p idl = Some m' ->
-  Mem.perm m b' q prm -> Mem.perm m' b' q prm.
+  (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
   induction idl; simpl; intros until m'.
-  intros. congruence.
-  caseEq (store_init_data m b p a); try congruence. intros. 
-  eapply IHidl; eauto. 
-  destruct a; simpl in H; eauto with mem.
-  congruence.
+  intros. inv H. tauto. 
+  caseEq (store_init_data m b p a); try congruence. intros.
+  rewrite <- (IHidl _ _ _ _ H0).
+  destruct a; simpl in H; split; eauto with mem.
+  inv H; auto. inv H; auto. 
+  destruct (find_symbol ge i); try congruence. eauto with mem.
   destruct (find_symbol ge i); try congruence. eauto with mem.
 Qed.
 
 Remark alloc_variables_perm:
-  forall prm b' q vl m m',
+  forall k prm b' q vl m m',
   alloc_variables m vl = Some m' ->
-  Mem.perm m b' q prm -> Mem.perm m' b' q prm.
+  Mem.valid_block m b' ->
+  (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
   induction vl.
-  simpl; intros. congruence.
+  simpl; intros. inv H. tauto. 
   intros until m'. simpl. unfold alloc_variable. 
   set (init := gvar_init a#2).
   set (sz := init_data_list_size init).
   caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
   caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
   caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
-  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC PERM.
+  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID.
   assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  eapply IHvl; eauto.
-  eapply Mem.perm_drop_3; eauto. 
-  eapply store_init_data_list_perm; eauto.
-  eapply store_zeros_perm; eauto.
+  assert (VALID': Mem.valid_block m4 b').
+    unfold Mem.valid_block. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
+    rewrite (store_init_data_list_nextblock _ _ _ _ STORE).  
+    rewrite (store_zeros_nextblock _ _ _ STZ).  
+    change (Mem.valid_block m1 b'). eauto with mem.
+  rewrite <- (IHvl _ _ REC VALID').
+  split; intros.
+  eapply Mem.perm_drop_3; eauto.
+  rewrite <- store_init_data_list_perm; [idtac|eauto].
+  rewrite <- store_zeros_perm; [idtac|eauto].
   eauto with mem.
+  assert (Mem.perm m1 b' q k prm).
+    rewrite store_zeros_perm; [idtac|eauto].
+    rewrite store_init_data_list_perm; [idtac|eauto].
+    eapply Mem.perm_drop_4; eauto.
+  exploit Mem.perm_alloc_inv; eauto. rewrite zeq_false; auto.
 Qed.
 
 Remark store_zeros_outside:
@@ -913,56 +960,93 @@ Proof.
   repeat rewrite H. destruct a; intuition. 
 Qed.
 
-Lemma alloc_variables_charact:
-  forall id gv vl g m m',
+Definition variables_initialized (g: t) (m: mem) :=
+  forall b gv,
+  find_var_info g b = Some gv ->
+  Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Cur (perm_globvar gv)
+  /\ (forall ofs k p, Mem.perm m b ofs k p ->
+        0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p)
+  /\ (gv.(gvar_volatile) = false -> load_store_init_data m b 0 gv.(gvar_init)).
+
+Lemma alloc_variable_initialized:
+  forall g m id v m',
   genv_nextvar g = Mem.nextblock m ->
-  alloc_variables m vl = Some m' ->
-  list_norepet (map (@fst ident (globvar V)) vl) ->
-  In (id, gv) vl ->
-  exists b, find_symbol (add_variables g vl) id = Some b 
-         /\ find_var_info (add_variables g vl) b = Some gv
-         /\ Mem.range_perm m' b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv)
-         /\ (gv.(gvar_volatile) = false -> load_store_init_data m' b 0 gv.(gvar_init)).
-Proof.
-  induction vl; simpl.
-  contradiction.
-  intros until m'; intro NEXT.
-  unfold alloc_variable. destruct a as [id' gv']. simpl.
-  set (init := gvar_init gv').
-  set (sz := init_data_list_size init).
-  caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC.
-  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
-  caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
-  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar gv')); try congruence.
-  intros m4 DROP REC NOREPET IN. inv NOREPET.
-  exploit Mem.alloc_result; eauto. intro BEQ. 
-  destruct IN. inversion H; subst id gv.
-  exists (Mem.nextblock m); split. 
-  rewrite add_variables_same_symb; auto. unfold find_symbol; simpl. 
-  rewrite PTree.gss. congruence. 
-  split. rewrite add_variables_same_address. unfold find_var_info; simpl.
-  rewrite NEXT. apply ZMap.gss.
-  simpl. rewrite <- NEXT; omega.
-  split. red; intros.
-  rewrite <- BEQ. eapply alloc_variables_perm; eauto. eapply Mem.perm_drop_1; eauto. 
-  intros NOVOL. 
+  alloc_variable m (id, v) = Some m' ->
+  variables_initialized g m ->
+  variables_initialized (add_variable g (id, v)) m'
+  /\ genv_nextvar (add_variable g (id,v)) = Mem.nextblock m'.
+Proof.
+  intros. revert H0. unfold alloc_variable. simpl. 
+  set (il := gvar_init v).
+  set (sz := init_data_list_size il).
+  caseEq (Mem.alloc m 0 sz).   intros m1 b1 ALLOC.
+  caseEq (store_zeros m1 b1 sz); try congruence. intros m2 ZEROS.
+  caseEq (store_init_data_list m2 b1 0 il); try congruence. intros m3 INIT DROP.
+  exploit Mem.nextblock_alloc; eauto.  intros NB1.
+  assert (Mem.nextblock m' = Mem.nextblock m1).
+    rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
+    rewrite (store_init_data_list_nextblock _ _ _ _ INIT).
+    eapply store_zeros_nextblock; eauto.
+  exploit Mem.alloc_result; eauto. intro RES.
+  split.
+  (* var-init *)
+  red; intros. revert H2.
+  unfold add_variable, find_var_info; simpl.
+  rewrite H; rewrite <- RES.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b b1); intros VI.
+  (* new var *)
+  injection VI; intro EQ. subst b gv. clear VI.
+  fold il. fold sz.
+  split. red; intros. eapply Mem.perm_drop_1; eauto.
+  split. intros. 
+    assert (0 <= ofs < sz).
+      eapply Mem.perm_alloc_3; eauto. 
+      rewrite store_zeros_perm; [idtac|eauto].
+      rewrite store_init_data_list_perm; [idtac|eauto].
+      eapply Mem.perm_drop_4; eauto.
+  split; auto. eapply Mem.perm_drop_2; eauto.
+  intros. 
   apply load_store_init_data_invariant with m3.
-  intros. transitivity (Mem.load chunk m4 (Mem.nextblock m) ofs).
-  eapply load_alloc_variables; eauto. 
-  red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
-  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
-  rewrite (store_zeros_nextblock _ _ _ STZ).
-  change (Mem.valid_block m1 (Mem.nextblock m)). rewrite <- BEQ. eauto with mem.
-  eapply Mem.load_drop; eauto. repeat right. 
-  unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv'); auto with mem.
-  rewrite <- BEQ. eapply store_init_data_list_charact; eauto. 
+  intros. eapply Mem.load_drop; eauto. right; right; right.
+  unfold perm_globvar. destruct (gvar_volatile v); try discriminate.
+  destruct (gvar_readonly v); auto with mem.
+  eapply store_init_data_list_charact; eauto.
+  (* older vars *)
+  exploit H1; eauto. intros [A [B C]].
+  split. red; intros. eapply Mem.perm_drop_3; eauto. 
+  rewrite <- store_init_data_list_perm; [idtac|eauto].
+  rewrite <- store_zeros_perm; [idtac|eauto].
+  eapply Mem.perm_alloc_1; eauto.
+  split. intros. eapply B. 
+  eapply Mem.perm_alloc_4; eauto.   
+  rewrite store_zeros_perm; [idtac|eauto].
+  rewrite store_init_data_list_perm; [idtac|eauto].
+  eapply Mem.perm_drop_4; eauto.
+  intros. apply load_store_init_data_invariant with m; auto.
+  intros. transitivity (Mem.load chunk m3 b ofs). 
+  eapply Mem.load_drop; eauto. 
+  transitivity (Mem.load chunk m2 b ofs). 
+  eapply store_init_data_list_outside; eauto.
+  transitivity (Mem.load chunk m1 b ofs). 
+  eapply store_zeros_outside; eauto.
+  eapply Mem.load_alloc_unchanged; eauto.
+  red. exploit genv_vars_range; eauto. rewrite <- H. omega.
+  rewrite H0; rewrite NB1; rewrite H; auto.
+Qed.
 
-  apply IHvl with m4; auto.
-  simpl.
-  rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
-  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
-  rewrite (store_zeros_nextblock _ _ _ STZ).
-  rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega.
+Lemma alloc_variables_initialized:
+  forall vl g m m',
+  genv_nextvar g = Mem.nextblock m ->
+  alloc_variables m vl = Some m' ->
+  variables_initialized g m ->
+  variables_initialized (add_variables g vl) m'.
+Proof.
+  induction vl; simpl; intros.
+  inv H0; auto.
+  destruct (alloc_variable m a) as [m1|]_eqn; try discriminate.
+  destruct a as [id gv].
+  exploit alloc_variable_initialized; eauto. intros [P Q].
+  eapply IHvl; eauto. 
 Qed.
 
 End INITMEM.
@@ -1007,19 +1091,19 @@ Proof.
   red. rewrite H1. rewrite <- H3. intuition.
 Qed.
 
-Theorem find_var_exists:
-  forall p id gv m,
-  list_norepet (prog_var_names p) ->
-  In (id, gv) (prog_vars p) ->
+Theorem init_mem_characterization:
+  forall p b gv m,
+  find_var_info (globalenv p) b = Some gv ->
   init_mem p = Some m ->
-  exists b, find_symbol (globalenv p) id = Some b
-         /\ find_var_info (globalenv p) b = Some gv
-         /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv)
-         /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)).
+  Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Cur (perm_globvar gv)
+  /\ (forall ofs k p, Mem.perm m b ofs k p ->
+        0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p)
+  /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)).
 Proof.
-  intros. exploit alloc_variables_charact; eauto. 
-  instantiate (1 := Mem.empty). rewrite add_functions_nextvar. rewrite Mem.nextblock_empty; auto.
-  assumption.
+  intros. eapply alloc_variables_initialized; eauto. 
+  rewrite add_functions_nextvar; auto. 
+  red; intros. exploit genv_vars_range; eauto. rewrite add_functions_nextvar. 
+  simpl. intros. omegaContradiction.
 Qed.
 
 (** ** Compatibility with memory injections *)
@@ -1142,8 +1226,8 @@ Proof.
              Mem.store chunk m2 b ofs v = Some m2' -> 
              Mem.inject (Mem.flat_inj thr) m1 m2'). 
     intros. eapply Mem.store_outside_inject; eauto. 
-        intros b' ? INJ'. unfold Mem.flat_inj in INJ'. 
-         destruct (zlt b' thr); inversion INJ'; subst. omega. 
+    intros. unfold Mem.flat_inj in H0.
+    destruct (zlt b' thr); inversion H0; subst. omega. 
   destruct id; simpl in ST; try (eapply P; eauto; fail).
   inv ST; auto. 
   revert ST.  caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. 
@@ -1687,31 +1771,40 @@ Proof.
   rewrite H0; simpl. auto.
 Qed.
 
-
-(* This may not yet be in the ideal form for easy use .*)
-Theorem find_new_var_exists: 
-  list_norepet (prog_var_names p ++ var_names new_vars) -> 
-  forall id gv m, In (id, gv) new_vars -> 
-  init_mem p' = Some m -> 
-  exists b, find_symbol (globalenv p') id = Some b
-         /\ find_var_info (globalenv p') b = Some gv
-         /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv)
-         /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p') m b 0 gv.(gvar_init)).
+Theorem find_new_var_exists:
+  forall id gv,
+  list_norepet (var_names new_vars) ->
+  In (id, gv) new_vars ->
+  exists b, find_symbol (globalenv p') id = Some b /\ find_var_info (globalenv p') b = Some gv.
 Proof.
   intros. 
-  destruct p. 
+  assert (P: forall b vars (ge: t B W),
+          ~In id (var_names vars) ->
+          find_symbol ge id = Some b
+          /\ find_var_info ge b = Some gv ->
+          find_symbol (add_variables ge vars) id = Some b
+          /\ find_var_info (add_variables ge vars) b = Some gv).
+  induction vars; simpl; intros. auto. apply IHvars. tauto.
+  destruct a as [id1 gv1]; unfold add_variable, find_symbol, find_var_info; simpl in *.
+  destruct H2; split. rewrite PTree.gso. auto. intuition. 
+  rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. unfold ZIndexed.t; omega.
+
+  assert (Q: forall vars (ge: t B W),
+          list_norepet (var_names vars) ->
+          In (id, gv) vars ->
+          exists b, find_symbol (add_variables ge vars) id = Some b
+                 /\ find_var_info (add_variables ge vars) b = Some gv).
+    induction vars; simpl; intros.
+    contradiction.
+    destruct a as [id1 gv1]; simpl in *. inv H1. destruct H2. inv H1. 
+    exists (genv_nextvar ge). apply P; auto. 
+    unfold add_variable, find_symbol, find_var_info; simpl in *.
+    split. apply PTree.gss. apply ZMap.gss. 
+    apply IHvars; auto. 
+
   unfold transform_partial_augment_program in transf_OK. 
   monadInv transf_OK. rename x into prog_funct'.  rename x0 into prog_vars'. simpl in *.
-  assert (var_names prog_vars = var_names prog_vars').
-   clear - EQ1.  generalize dependent prog_vars'. induction prog_vars; intros.
-      simpl in EQ1. inversion EQ1; subst; auto.
-      simpl in EQ1. destruct a. destruct (transf_globvar transf_var g); try discriminate. monadInv EQ1.
-      simpl; f_equal; auto.
-  apply find_var_exists. 
-  unfold prog_var_names in *; simpl in *.  
-  rewrite var_names_app. rewrite <- H2. auto.
-  simpl. intuition.
-  auto.
+  unfold globalenv; simpl. repeat rewrite add_variables_app. apply Q; auto.
 Qed.
 
 Theorem find_var_info_rev_transf_augment:
diff --git a/common/Memory.v b/common/Memory.v
index 059a27e..0fc663f 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -25,9 +25,10 @@
 - [alloc]: allocate a fresh memory block;
 - [free]: invalidate a memory block.
 *)
-  
+
 Require Import Axioms.
 Require Import Coqlib.
+Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -35,24 +36,7 @@ Require Import Values.
 Require Export Memdata.
 Require Export Memtype.
 
-Definition update (A: Type) (x: Z) (v: A) (f: Z -> A) : Z -> A :=
-  fun y => if zeq y x then v else f y.
-
-Implicit Arguments update [A].
-
-Lemma update_s:
-  forall (A: Type) (x: Z) (v: A) (f: Z -> A),
-  update x v f x = v.
-Proof.
-  intros; unfold update. apply zeq_true.
-Qed.
-
-Lemma update_o:
-  forall (A: Type) (x: Z) (v: A) (f: Z -> A) (y: Z),
-  x <> y -> update x v f y = f y.
-Proof.
-  intros; unfold update. apply zeq_false; auto.
-Qed.
+Local Notation "a # b" := (ZMap.get b a) (at level 1).
 
 Module Mem <: MEM.
 
@@ -62,25 +46,31 @@ Definition perm_order' (po: option permission) (p: permission) :=
   | None => False
  end.
 
+Definition perm_order'' (po1 po2: option permission) := 
+  match po1, po2 with
+  | Some p1, Some p2 => perm_order p1 p2
+  | _, None => True
+  | None, Some _ => False
+ end.
+
 Record mem' : Type := mkmem {
-  mem_contents: block -> Z -> memval;
-  mem_access: block -> Z -> option permission;
-  bounds: block -> Z * Z;
+  mem_contents: ZMap.t (ZMap.t memval);  (**r [block -> offset -> memval] *)
+  mem_access: ZMap.t (Z -> perm_kind -> option permission);
+                                         (**r [block -> offset -> kind -> option permission] *)
   nextblock: block;
   nextblock_pos: nextblock > 0;
-  nextblock_noaccess: forall b, 0 < b < nextblock \/ bounds b = (0,0) ;
-  bounds_noaccess: forall b ofs, ofs < fst(bounds b) \/ ofs >= snd(bounds b) -> mem_access b ofs = None;
-  noread_undef: forall b ofs,  perm_order' (mem_access b ofs) Readable \/ mem_contents b ofs = Undef
+  access_max: 
+    forall b ofs, perm_order'' (mem_access#b ofs Max) (mem_access#b ofs Cur);
+  nextblock_noaccess:
+    forall b ofs k, b <= 0 \/ b >= nextblock -> mem_access#b ofs k = None
 }.
 
 Definition mem := mem'.
 
 Lemma mkmem_ext:
- forall cont1 cont2 acc1 acc2 bound1 bound2 next1 next2 
-          a1 a2 b1 b2 c1 c2 d1 d2,
-  cont1=cont2 -> acc1=acc2 -> bound1=bound2 -> next1=next2 ->
-  mkmem cont1 acc1 bound1 next1 a1 b1 c1 d1 =
-  mkmem cont2 acc2 bound2 next2 a2 b2 c2 d2.
+ forall cont1 cont2 acc1 acc2 next1 next2 a1 a2 b1 b2 c1 c2,
+  cont1=cont2 -> acc1=acc2 -> next1=next2 ->
+  mkmem cont1 acc1 next1 a1 b1 c1 = mkmem cont2 acc2 next2 a2 b2 c2.
 Proof.
   intros. subst. f_equal; apply proof_irr.
 Qed.
@@ -103,29 +93,54 @@ Hint Local Resolve valid_not_valid_diff: mem.
 
 (** Permissions *)
 
-Definition perm (m: mem) (b: block) (ofs: Z) (p: permission) : Prop :=
-   perm_order' (mem_access m b ofs) p.
+Definition perm (m: mem) (b: block) (ofs: Z) (k: perm_kind) (p: permission) : Prop :=
+   perm_order' (m.(mem_access)#b ofs k) p.
 
 Theorem perm_implies:
-  forall m b ofs p1 p2, perm m b ofs p1 -> perm_order p1 p2 -> perm m b ofs p2.
+  forall m b ofs k p1 p2, perm m b ofs k p1 -> perm_order p1 p2 -> perm m b ofs k p2.
 Proof.
   unfold perm, perm_order'; intros.
-  destruct (mem_access m b ofs); auto.
+  destruct (m.(mem_access)#b ofs k); auto.
   eapply perm_order_trans; eauto.
 Qed.
 
 Hint Local Resolve perm_implies: mem.
 
+Theorem perm_cur_max:
+  forall m b ofs p, perm m b ofs Cur p -> perm m b ofs Max p.
+Proof.
+  assert (forall po1 po2 p,
+          perm_order' po2 p -> perm_order'' po1 po2 -> perm_order' po1 p).
+  unfold perm_order', perm_order''. intros. 
+  destruct po2; try contradiction.
+  destruct po1; try contradiction. 
+  eapply perm_order_trans; eauto.
+  unfold perm; intros.
+  generalize (access_max m b ofs). eauto. 
+Qed.
+
+Theorem perm_cur:
+  forall m b ofs k p, perm m b ofs Cur p -> perm m b ofs k p.
+Proof.
+  intros. destruct k; auto. apply perm_cur_max. auto.
+Qed.
+
+Theorem perm_max:
+  forall m b ofs k p, perm m b ofs k p -> perm m b ofs Max p.
+Proof.
+  intros. destruct k; auto. apply perm_cur_max. auto.
+Qed.
+
+Hint Local Resolve perm_cur perm_max: mem.
+
 Theorem perm_valid_block:
-  forall m b ofs p, perm m b ofs p -> valid_block m b.
+  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)).
   auto.
-  assert (mem_access m b ofs = None). 
-  destruct (nextblock_noaccess m b).
-  elimtype False; omega.
-  apply bounds_noaccess. rewrite H0; simpl; omega.
+  assert (m.(mem_access)#b ofs k = None).
+  eapply nextblock_noaccess; eauto. 
   rewrite H0 in H.
   contradiction.
 Qed.
@@ -147,34 +162,48 @@ Proof.
 Qed.
 
 Theorem perm_dec:
-  forall m b ofs p, {perm m b ofs p} + {~ perm m b ofs p}.
+  forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}.
 Proof.
   unfold perm; intros.
   apply perm_order'_dec.
 Qed.
- 
-Definition range_perm (m: mem) (b: block) (lo hi: Z) (p: permission) : Prop :=
-  forall ofs, lo <= ofs < hi -> perm m b ofs p.
+
+Definition range_perm (m: mem) (b: block) (lo hi: Z) (k: perm_kind) (p: permission) : Prop :=
+  forall ofs, lo <= ofs < hi -> perm m b ofs k p.
 
 Theorem range_perm_implies:
-  forall m b lo hi p1 p2,
-  range_perm m b lo hi p1 -> perm_order p1 p2 -> range_perm m b lo hi p2.
+  forall m b lo hi k p1 p2,
+  range_perm m b lo hi k p1 -> perm_order p1 p2 -> range_perm m b lo hi k p2.
 Proof.
   unfold range_perm; intros; eauto with mem.
 Qed.
 
-Hint Local Resolve range_perm_implies: mem.
+Theorem range_perm_cur:
+  forall m b lo hi k p,
+  range_perm m b lo hi Cur p -> range_perm m b lo hi k p.
+Proof.
+  unfold range_perm; intros; eauto with mem.
+Qed.
+
+Theorem range_perm_max:
+  forall m b lo hi k p,
+  range_perm m b lo hi k p -> range_perm m b lo hi Max p.
+Proof.
+  unfold range_perm; intros; eauto with mem.
+Qed.
+
+Hint Local Resolve range_perm_implies range_perm_cur range_perm_max: mem.
 
 Lemma range_perm_dec:
-  forall m b lo hi p, {range_perm m b lo hi p} + {~ range_perm m b lo hi p}.
+  forall m b lo hi k p, {range_perm m b lo hi k p} + {~ range_perm m b lo hi k p}.
 Proof.
   intros. 
   assert (forall n, 0 <= n ->
-          {range_perm m b lo (lo + n) p} + {~ range_perm m b lo (lo + n) p}).
+          {range_perm m b lo (lo + n) k p} + {~ range_perm m b lo (lo + n) k p}).
     apply natlike_rec2.
     left. red; intros. omegaContradiction.
     intros. destruct H0. 
-    destruct (perm_dec m b (lo + z) p). 
+    destruct (perm_dec m b (lo + z) k p). 
     left. red; intros. destruct (zeq ofs (lo + z)). congruence. apply r. omega. 
     right; red; intro. elim n. apply H0. omega. 
     right; red; intro. elim n. red; intros. apply H0. omega. 
@@ -185,14 +214,14 @@ Qed.
 
 (** [valid_access m chunk b ofs p] holds if a memory access
     of the given chunk is possible in [m] at address [b, ofs]
-    with permissions [p].
+    with current permissions [p].
     This means:
-- The range of bytes accessed all have permission [p].
+- The range of bytes accessed all have current permission [p].
 - The offset [ofs] is aligned.
 *)
 
 Definition valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) (p: permission): Prop :=
-  range_perm m b ofs (ofs + size_chunk chunk) p
+  range_perm m b ofs (ofs + size_chunk chunk) Cur p
   /\ (align_chunk chunk | ofs).
 
 Theorem valid_access_implies:
@@ -220,7 +249,7 @@ Theorem valid_access_valid_block:
   valid_block m b.
 Proof.
   intros. destruct H.
-  assert (perm m b ofs Nonempty).
+  assert (perm m b ofs Cur Nonempty).
     apply H. generalize (size_chunk_pos chunk). omega.
   eauto with mem.
 Qed.
@@ -228,11 +257,11 @@ Qed.
 Hint Local Resolve valid_access_valid_block: mem.
 
 Lemma valid_access_perm:
-  forall m chunk b ofs p,
+  forall m chunk b ofs k p,
   valid_access m chunk b ofs p ->
-  perm m b ofs p.
+  perm m b ofs k p.
 Proof.
-  intros. destruct H. apply H. generalize (size_chunk_pos chunk). omega.
+  intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). omega.
 Qed.
 
 Lemma valid_access_compat:
@@ -250,7 +279,7 @@ Lemma valid_access_dec:
   {valid_access m chunk b ofs p} + {~ valid_access m chunk b ofs p}.
 Proof.
   intros. 
-  destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) p).
+  destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur p).
   destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)).
   left; constructor; auto.
   right; red; intro V; inv V; contradiction.
@@ -261,14 +290,14 @@ Qed.
     the byte at the given location is nonempty. *)
 
 Definition valid_pointer (m: mem) (b: block) (ofs: Z): bool :=
-  perm_dec m b ofs Nonempty.
+  perm_dec m b ofs Cur Nonempty.
 
 Theorem valid_pointer_nonempty_perm:
   forall m b ofs,
-  valid_pointer m b ofs = true <-> perm m b ofs Nonempty.
+  valid_pointer m b ofs = true <-> perm m b ofs Cur Nonempty.
 Proof.
   intros. unfold valid_pointer. 
-  destruct (perm_dec m b ofs Nonempty); simpl;
+  destruct (perm_dec m b ofs Cur Nonempty); simpl;
   intuition congruence.
 Qed.
 
@@ -283,62 +312,23 @@ Proof.
   destruct H. apply H. simpl. omega.
 Qed.
 
-(** Bounds *)
-
-(** Each block has a low bound and a high bound, determined at allocation time
-    and invariant afterward.  The crucial properties of bounds is
-    that any offset below the low bound or above the high bound is
-    empty. *)
-
-Notation low_bound m b := (fst(bounds m b)).
-Notation high_bound m b := (snd(bounds m b)).
-
-Theorem perm_in_bounds:
-  forall m b ofs p, perm m b ofs p -> low_bound m b <= ofs < high_bound m b.
-Proof.
-  unfold perm. intros.
-  destruct (zlt ofs (fst (bounds m b))).
-  exploit bounds_noaccess. left; eauto.
-  intros.
-  rewrite H0 in H. contradiction.
-  destruct (zlt ofs (snd (bounds m b))).
-  omega. 
-  exploit bounds_noaccess. right; eauto.
-  intro; rewrite H0 in H. contradiction.
-Qed.
-
-Theorem range_perm_in_bounds:
-  forall m b lo hi p, 
-  range_perm m b lo hi p -> lo < hi -> low_bound m b <= lo /\ hi <= high_bound m b.
-Proof.
-  intros. split. 
-  exploit (perm_in_bounds m b lo p). apply H. omega. omega.
-  exploit (perm_in_bounds m b (hi-1) p). apply H. omega. omega.
-Qed.
-
-Theorem valid_access_in_bounds:
-  forall m chunk b ofs p,
-  valid_access m chunk b ofs p ->
-  low_bound m b <= ofs /\ ofs + size_chunk chunk <= high_bound m b.
-Proof.
-  intros. inv H. apply range_perm_in_bounds with p; auto.
-  generalize (size_chunk_pos chunk). omega.
-Qed.
-
-Hint Local Resolve perm_in_bounds range_perm_in_bounds valid_access_in_bounds.
-
-(** * Store operations *)
+(** * Operations over memory stores *)
 
 (** The initial store *)
 
 Program Definition empty: mem :=
-  mkmem (fun b ofs => Undef)
-        (fun b ofs => None)
-        (fun b => (0,0))
-        1 _ _ _ _.
+  mkmem (ZMap.init (ZMap.init Undef))
+        (ZMap.init (fun ofs k => None))
+        1 _ _ _.
 Next Obligation.
   omega.
 Qed.
+Next Obligation.
+  repeat rewrite ZMap.gi. red; auto.
+Qed.
+Next Obligation.
+  rewrite ZMap.gi. auto.
+Qed.
 
 Definition nullptr: block := 0.
 
@@ -348,108 +338,56 @@ Definition nullptr: block := 0.
   infinite memory. *)
 
 Program Definition alloc (m: mem) (lo hi: Z) :=
-  (mkmem (update m.(nextblock) 
-                 (fun ofs => Undef)
-                 m.(mem_contents))
-         (update m.(nextblock)
-                 (fun ofs => if zle lo ofs && zlt ofs hi then Some Freeable else None)
-                 m.(mem_access))
-         (update m.(nextblock) (lo, hi) m.(bounds))
+  (mkmem (ZMap.set m.(nextblock) 
+                   (ZMap.init Undef)
+                   m.(mem_contents))
+         (ZMap.set m.(nextblock)
+                   (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None)
+                   m.(mem_access))
          (Zsucc m.(nextblock))
-         _ _ _ _,
+         _ _ _,
    m.(nextblock)).
 Next Obligation.
   generalize (nextblock_pos m). omega. 
 Qed.
 Next Obligation.
-  assert (0 < b < Zsucc (nextblock m) \/ b <= 0 \/ b > nextblock m) by omega.
-  destruct H as [?|[?|?]]. left; omega.
-  right.
-  rewrite update_o.
-  destruct (nextblock_noaccess m b); auto. elimtype False; omega.
-  generalize (nextblock_pos m); omega.
-(*  generalize (bounds_noaccess m b 0).*)
-  destruct (nextblock_noaccess m b); auto. left; omega.
-  rewrite update_o. right; auto. omega.
-Qed.
-Next Obligation.
-  unfold update in *. destruct (zeq b (nextblock m)). 
-  simpl in H. destruct H. 
-  unfold proj_sumbool. rewrite zle_false. auto. omega.
-  unfold proj_sumbool. rewrite zlt_false; auto. rewrite andb_false_r. auto.
-  apply bounds_noaccess. auto.
+  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextblock m)). 
+  subst b. destruct (zle lo ofs && zlt ofs hi); red; auto with mem. 
+  apply access_max. 
 Qed.
 Next Obligation.
-unfold update.
-destruct (zeq b (nextblock m)); auto.
-apply noread_undef.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextblock m)). 
+  subst b. generalize (nextblock_pos m). intros. omegaContradiction.
+  apply nextblock_noaccess. omega.
 Qed.
 
-
 (** Freeing a block between the given bounds.
   Return the updated memory state where the given range of the given block
   has been invalidated: future reads and writes to this
-  range will fail.  Requires write permission on the given range. *)
-
-Definition clearN (m: block -> Z -> memval) (b: block) (lo hi: Z) : 
-    block -> Z -> memval :=
-   fun b' ofs => if zeq b' b 
-                         then if zle lo ofs && zlt ofs hi then Undef else m b' ofs
-                         else m b' ofs.
-
-Lemma clearN_in:
-   forall m b lo hi ofs, lo <= ofs < hi -> clearN m b lo hi b ofs = Undef.
-Proof.
-intros. unfold clearN. rewrite zeq_true.
-destruct H; unfold andb, proj_sumbool.
-rewrite zle_true; auto. rewrite zlt_true; auto.
-Qed.
-
-Lemma clearN_out:
-  forall m b lo hi b' ofs, (b<>b' \/ ofs < lo \/ hi <= ofs) -> clearN m b lo hi b' ofs = m b' ofs.
-Proof.
-intros. unfold clearN. destruct (zeq b' b); auto.
-subst b'.
-destruct H. contradiction H; auto.
-destruct (zle lo ofs); auto.
-destruct (zlt ofs hi); auto.
-elimtype False; omega.
-Qed.
-
+  range will fail.  Requires freeable permission on the given range. *)
 
 Program Definition unchecked_free (m: mem) (b: block) (lo hi: Z): mem :=
-  mkmem (clearN m.(mem_contents) b lo hi)
-        (update b 
-                (fun ofs => if zle lo ofs && zlt ofs hi then None else m.(mem_access) b ofs)
+  mkmem m.(mem_contents)
+        (ZMap.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.(bounds)
-        m.(nextblock) _ _ _ _.
+        m.(nextblock) _ _ _.
 Next Obligation.
   apply nextblock_pos. 
 Qed.
 Next Obligation.
-apply (nextblock_noaccess m b0).
+  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b).
+  destruct (zle lo ofs && zlt ofs hi). red; auto. apply access_max. 
+  apply access_max.
 Qed.
 Next Obligation.
-  unfold update. destruct (zeq b0 b). subst b0. 
-  destruct (zle lo ofs); simpl; auto.
-  destruct (zlt ofs hi); simpl; auto.
-  apply bounds_noaccess; auto.
-  apply bounds_noaccess; auto.
-  apply bounds_noaccess; auto.
-Qed.
-Next Obligation.
-  unfold clearN, update.
-  destruct (zeq b0 b). subst b0. 
-  destruct (zle lo ofs); simpl; auto.
-  destruct (zlt ofs hi); simpl; auto.
-  apply noread_undef.
-  apply noread_undef.
-  apply noread_undef.
+  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst.
+  destruct (zle lo ofs && zlt ofs hi). auto. apply nextblock_noaccess; auto.
+  apply nextblock_noaccess; auto.
 Qed.
 
 Definition free (m: mem) (b: block) (lo hi: Z): option mem :=
-  if range_perm_dec m b lo hi Freeable 
+  if range_perm_dec m b lo hi Cur Freeable 
   then Some(unchecked_free m b lo hi)
   else None.
 
@@ -467,10 +405,10 @@ Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem :=
 
 (** Reading N adjacent bytes in a block content. *)
 
-Fixpoint getN (n: nat) (p: Z) (c: Z -> memval) {struct n}: list memval :=
+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' => c#p :: getN n' (p + 1) c
   end.
 
 (** [load chunk m b ofs] perform a read in memory state [m], at address
@@ -480,7 +418,7 @@ Fixpoint getN (n: nat) (p: Z) (c: Z -> memval) {struct n}: list memval :=
 
 Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val :=
   if valid_access_dec m chunk b ofs Readable
-  then Some(decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents) b)))
+  then Some(decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents)#b)))
   else None.
 
 (** [loadv chunk m addr] is similar, but the address and offset are given
@@ -497,38 +435,37 @@ Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
   not readable. *)
 
 Definition loadbytes (m: mem) (b: block) (ofs n: Z): option (list memval) :=
-  if range_perm_dec m b ofs (ofs + n) Readable
-  then Some (getN (nat_of_Z n) ofs (m.(mem_contents) b))
+  if range_perm_dec m b ofs (ofs + n) Cur Readable
+  then Some (getN (nat_of_Z n) ofs (m.(mem_contents)#b))
   else None.
 
 (** Memory stores. *)
 
 (** Writing N adjacent bytes in a block content. *)
 
-Fixpoint setN (vl: list memval) (p: Z) (c: Z -> memval) {struct vl}: Z -> memval :=
+Fixpoint setN (vl: list memval) (p: Z) (c: ZMap.t memval) {struct vl}: ZMap.t memval :=
   match vl with
   | nil => c
-  | v :: vl' => setN vl' (p + 1) (update p v c)
+  | v :: vl' => setN vl' (p + 1) (ZMap.set p v c)
   end.
 
-
 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.
+  (setN vl p c)#q = c#q.
 Proof.
   induction vl; intros; simpl.
   auto. 
   simpl length in H. rewrite inj_S in H.
-  transitivity (update p a c q).
-  apply IHvl. intros. apply H. omega. 
-  apply update_o. apply H. omega. 
+  transitivity ((ZMap.set p a c)#q).
+  apply IHvl. intros. apply H. omega.
+  apply ZMap.gso. apply not_eq_sym. apply H. omega. 
 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.
+  (setN vl p c)#q = c#q.
 Proof.
   intros. apply setN_other. 
   intros. omega. 
@@ -541,13 +478,13 @@ Proof.
   induction vl; intros; simpl.
   auto.
   decEq. 
-  rewrite setN_outside. apply update_s. omega. 
+  rewrite setN_outside. apply ZMap.gss. omega. 
   apply IHvl. 
 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 -> c1#i = c2#i) ->
   getN n p c1 = getN n p c2.
 Proof.
   induction n; intros. auto. rewrite inj_S in H. simpl. decEq. 
@@ -562,50 +499,23 @@ Proof.
   intros. apply getN_exten. intros. apply setN_outside. omega. 
 Qed.
 
-Lemma setN_noread_undef:
-  forall m b ofs bytes (RP: range_perm m b ofs (ofs + Z_of_nat (length bytes)) Writable),
-  forall b' ofs',
-  perm m b' ofs' Readable \/
-  update b (setN bytes ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef.
-Proof.
-  intros. unfold update. destruct (zeq b' b). subst b'.
-  assert (ofs <= ofs' < ofs + Z_of_nat (length bytes)
-         \/ ofs' < ofs
-         \/ ofs' >= ofs + Z_of_nat (length bytes)) by omega.
-  destruct H. left. apply perm_implies with Writable; auto with mem. 
-  rewrite setN_outside; auto. apply noread_undef; auto. 
-  apply noread_undef; auto.
-Qed.
-
-Lemma store_noread_undef:
-  forall m ch b ofs (VA: valid_access m ch b ofs Writable) v,
-  forall b' ofs', 
-  perm m b' ofs' Readable \/ 
-  update b (setN (encode_val ch v) ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef.
-Proof.
-  intros. destruct VA. apply setN_noread_undef. 
-  rewrite encode_val_length. rewrite <- size_chunk_conv. auto.
-Qed.
-
 (** [store chunk m b ofs v] perform a write in memory state [m].
   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 :=
- match valid_access_dec m chunk b ofs Writable with
- | left VA => Some (mkmem (update b 
-                                  (setN (encode_val chunk v) ofs (m.(mem_contents) b))
-                                  m.(mem_contents))
-                    m.(mem_access)
-                    m.(bounds)
-                    m.(nextblock)
-                    m.(nextblock_pos)
-                    m.(nextblock_noaccess)
-                    m.(bounds_noaccess)
-                    (store_noread_undef m chunk b ofs VA v))
- | right _ => None
- end.
+  if valid_access_dec m chunk b ofs Writable then
+    Some (mkmem (ZMap.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.
 
 (** [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. *)
@@ -621,57 +531,45 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   or [None] if the accessed locations are not writable. *)
 
 Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem :=
-  match range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Writable with
-  | left RP =>
-      Some (mkmem
-             (update b (setN bytes ofs (m.(mem_contents) b)) m.(mem_contents))
+  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))
              m.(mem_access)
-             m.(bounds)
              m.(nextblock)
              m.(nextblock_pos)
-             m.(nextblock_noaccess)
-             m.(bounds_noaccess)
-             (setN_noread_undef m b ofs bytes RP))
-  | right _ =>
-      None
-  end.
-
-(** [drop_perm m b lo hi p] sets the permissions of the byte range
-    [(b, lo) ... (b, hi - 1)] to [p].  These bytes must have permissions
-    at least [p] in the initial memory state [m].
+             m.(access_max)
+             m.(nextblock_noaccess))
+  else
+    None.
+
+(** [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
+    [Freeable] in the initial memory state [m].
     Returns updated memory state, or [None] if insufficient permissions. *)
 
 Program Definition drop_perm (m: mem) (b: block) (lo hi: Z) (p: permission): option mem :=
-  if range_perm_dec m b lo hi p then
-    Some (mkmem (update b 
-                        (fun ofs => if zle lo ofs && zlt ofs hi && negb (perm_order_dec p Readable)
-                                    then Undef else m.(mem_contents) b ofs)
-                        m.(mem_contents))
-                (update b
-                        (fun ofs => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access) b ofs)
+  if range_perm_dec m b lo hi Cur Freeable then
+    Some (mkmem m.(mem_contents)
+                (ZMap.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.(bounds) m.(nextblock) _ _ _ _)
+                m.(nextblock) _ _ _)
   else None.
 Next Obligation.
-  destruct m; auto.
+  apply nextblock_pos.
 Qed.
 Next Obligation.
-  destruct m; auto.
+  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst b0.
+  destruct (zle lo ofs && zlt ofs hi). red; auto with mem. apply access_max. 
+  apply access_max.
 Qed.
 Next Obligation.
-  unfold update. destruct (zeq b0 b). subst b0.
+  specialize (nextblock_noaccess m b0 ofs k H0). intros. 
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst b0.
   destruct (zle lo ofs). destruct (zlt ofs hi).
-  exploit range_perm_in_bounds; eauto. omega. intros. omegaContradiction. 
-  simpl. eapply bounds_noaccess; eauto. 
-  simpl. eapply bounds_noaccess; eauto.
-  eapply bounds_noaccess; eauto. 
-Qed.
-Next Obligation.
-  unfold update. destruct (zeq b0 b). subst b0. 
-  destruct (zle lo ofs && zlt ofs hi). 
-  destruct (perm_order_dec p Readable); simpl; auto.
-  eapply noread_undef; eauto.
-  eapply noread_undef; eauto.
+  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.
 
 (** * Properties of the memory operations *)
@@ -681,14 +579,14 @@ Qed.
 Theorem nextblock_empty: nextblock empty = 1.
 Proof. reflexivity. Qed.
 
-Theorem perm_empty: forall b ofs p, ~perm empty b ofs p.
+Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p.
 Proof. 
-  intros. unfold perm, empty; simpl. congruence.
+  intros. unfold perm, empty; simpl. rewrite ZMap.gi. simpl. tauto. 
 Qed.
 
 Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p.
 Proof.
-  intros. red; intros. elim (perm_empty b ofs p). apply H. 
+  intros. red; intros. elim (perm_empty b ofs Cur p). apply H. 
   generalize (size_chunk_pos chunk); omega.
 Qed.
 
@@ -716,7 +614,7 @@ Qed.
 Lemma load_result:
   forall chunk m b ofs v,
   load chunk m b ofs = Some v ->
-  v = decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents) b)).
+  v = decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents)#b)).
 Proof.
   intros until v. unfold load. 
   destruct (valid_access_dec m chunk b ofs Readable); intros.
@@ -748,7 +646,7 @@ Theorem load_cast:
   end.
 Proof.
   intros. exploit load_result; eauto.
-  set (l := getN (size_chunk_nat chunk) ofs (mem_contents m b)).
+  set (l := getN (size_chunk_nat chunk) ofs m.(mem_contents)#b).
   intros. subst v. apply decode_val_cast. 
 Qed.
 
@@ -758,7 +656,7 @@ Theorem load_int8_signed_unsigned:
 Proof.
   intros. unfold load.
   change (size_chunk_nat Mint8signed) with (size_chunk_nat Mint8unsigned).
-  set (cl := getN (size_chunk_nat Mint8unsigned) ofs (mem_contents m b)).
+  set (cl := getN (size_chunk_nat Mint8unsigned) ofs m.(mem_contents)#b).
   destruct (valid_access_dec m Mint8signed b ofs Readable).
   rewrite pred_dec_true; auto. unfold decode_val. 
   destruct (proj_bytes cl); auto. rewrite decode_int8_signed_unsigned. auto.
@@ -771,7 +669,7 @@ Theorem load_int16_signed_unsigned:
 Proof.
   intros. unfold load.
   change (size_chunk_nat Mint16signed) with (size_chunk_nat Mint16unsigned).
-  set (cl := getN (size_chunk_nat Mint16unsigned) ofs (mem_contents m b)).
+  set (cl := getN (size_chunk_nat Mint16unsigned) ofs m.(mem_contents)#b).
   destruct (valid_access_dec m Mint16signed b ofs Readable).
   rewrite pred_dec_true; auto. unfold decode_val. 
   destruct (proj_bytes cl); auto. rewrite decode_int16_signed_unsigned. auto.
@@ -782,7 +680,7 @@ Qed.
 
 Theorem range_perm_loadbytes:
   forall m b ofs len,
-  range_perm m b ofs (ofs + len) Readable ->
+  range_perm m b ofs (ofs + len) Cur Readable ->
   exists bytes, loadbytes m b ofs len = Some bytes.
 Proof.
   intros. econstructor. unfold loadbytes. rewrite pred_dec_true; eauto. 
@@ -791,10 +689,10 @@ Qed.
 Theorem loadbytes_range_perm:
   forall m b ofs len bytes,
   loadbytes m b ofs len = Some bytes ->
-  range_perm m b ofs (ofs + len) Readable.
+  range_perm m b ofs (ofs + len) Cur Readable.
 Proof.
   intros until bytes. unfold loadbytes.
-  destruct (range_perm_dec m b ofs (ofs + len) Readable). auto. congruence.
+  destruct (range_perm_dec m b ofs (ofs + len) Cur Readable). auto. congruence.
 Qed.
 
 Theorem loadbytes_load:
@@ -804,7 +702,7 @@ Theorem loadbytes_load:
   load chunk m b ofs = Some(decode_val chunk bytes).
 Proof.
   unfold loadbytes, load; intros. 
-  destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Readable);
+  destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur Readable);
   try congruence.
   inv H. rewrite pred_dec_true. auto. 
   split; auto.
@@ -818,7 +716,7 @@ Theorem load_loadbytes:
 Proof.
   intros. exploit load_valid_access; eauto. intros [A B].
   exploit load_result; eauto. intros. 
-  exists (getN (size_chunk_nat chunk) ofs (mem_contents m b)); split.
+  exists (getN (size_chunk_nat chunk) ofs m.(mem_contents)#b); split.
   unfold loadbytes. rewrite pred_dec_true; auto. 
   auto.
 Qed.
@@ -835,7 +733,7 @@ Theorem loadbytes_length:
   length bytes = nat_of_Z n.
 Proof.
   unfold loadbytes; intros.
-  destruct (range_perm_dec m b ofs (ofs + n) Readable); try congruence.
+  destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); try congruence.
   inv H. apply getN_length.
 Qed.
 
@@ -866,8 +764,8 @@ Theorem loadbytes_concat:
   loadbytes m b ofs (n1 + n2) = Some(bytes1 ++ bytes2).
 Proof.
   unfold loadbytes; intros.
-  destruct (range_perm_dec m b ofs (ofs + n1) Readable); try congruence.
-  destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Readable); try congruence.
+  destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence.
+  destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence.
   rewrite pred_dec_true. rewrite nat_of_Z_plus; auto.
   rewrite getN_concat. rewrite nat_of_Z_eq; auto.
   congruence.
@@ -886,7 +784,7 @@ Theorem loadbytes_split:
   /\ bytes = bytes1 ++ bytes2.
 Proof.
   unfold loadbytes; intros. 
-  destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Readable);
+  destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable);
   try congruence.
   rewrite nat_of_Z_plus in H; auto. rewrite getN_concat in H.
   rewrite nat_of_Z_eq in H; auto. 
@@ -899,28 +797,28 @@ Qed.
 
 Theorem load_rep:
  forall ch m1 m2 b ofs v1 v2, 
-  (forall z, 0 <= z < size_chunk ch -> mem_contents m1 b (ofs+z) = mem_contents m2 b (ofs+z)) ->
+  (forall z, 0 <= z < size_chunk ch -> m1.(mem_contents)#b#(ofs+z) = m2.(mem_contents)#b#(ofs+z)) ->
   load ch m1 b ofs = Some v1 ->
   load ch m2 b ofs = Some v2 ->
   v1 = v2.
 Proof.
-intros.
-apply load_result in H0.
-apply load_result in H1.
-subst.
-f_equal.
-rewrite size_chunk_conv in H.
-remember (size_chunk_nat ch) as n; clear Heqn.
-revert ofs H; induction n; intros; simpl; auto.
-f_equal.
-rewrite inj_S in H.
-replace ofs with (ofs+0) by omega.
-apply H; omega.
-apply IHn.
-intros.
-rewrite <- Zplus_assoc.
-apply H.
-rewrite inj_S. omega.
+  intros.
+  apply load_result in H0.
+  apply load_result in H1.
+  subst.
+  f_equal.
+  rewrite size_chunk_conv in H.
+  remember (size_chunk_nat ch) as n; clear Heqn.
+  revert ofs H; induction n; intros; simpl; auto.
+  f_equal.
+  rewrite inj_S in H.
+  replace ofs with (ofs+0) by omega.
+  apply H; omega.
+  apply IHn.
+  intros.
+  rewrite <- Zplus_assoc.
+  apply H.
+  rewrite inj_S. omega.
 Qed.
 
 (** ** Properties related to [store] *)
@@ -954,27 +852,27 @@ Proof.
   auto.
 Qed.
 
-Lemma store_mem_contents: mem_contents m2 = 
-                                       update b (setN (encode_val chunk v) ofs (m1.(mem_contents) b)) m1.(mem_contents).
+Lemma store_mem_contents: 
+  mem_contents m2 = ZMap.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.
   auto.
 Qed.
 
 Theorem perm_store_1:
-  forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p.
+  forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.
 Proof.
   intros. 
  unfold perm in *. rewrite store_access; auto.
 Qed.
 
 Theorem perm_store_2:
-  forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p.
+  forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p.
 Proof.
   intros. unfold perm in *.  rewrite store_access in H; auto.
 Qed.
 
-Hint Local Resolve perm_store_1 perm_store_2: mem.
+Local Hint Resolve perm_store_1 perm_store_2: mem.
 
 Theorem nextblock_store:
   nextblock m2 = nextblock m1.
@@ -996,7 +894,7 @@ Proof.
   unfold valid_block; intros. rewrite nextblock_store in H; auto.
 Qed.
 
-Hint Local Resolve store_valid_block_1 store_valid_block_2: mem.
+Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.
 
 Theorem store_valid_access_1:
   forall chunk' b' ofs' p,
@@ -1020,16 +918,7 @@ Proof.
   congruence.
 Qed.
 
-Hint Local Resolve store_valid_access_1 store_valid_access_2
-             store_valid_access_3: mem.
-
-Theorem bounds_store:
-  forall b', bounds m2 b' = bounds m1 b'.
-Proof.
-  intros.
-  unfold store in STORE.
-  destruct ( valid_access_dec m1 chunk b ofs Writable); inv STORE. simpl. auto.
-Qed.
+Local Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3: mem.
 
 Theorem load_store_similar:
   forall chunk',
@@ -1043,7 +932,7 @@ Proof.
   exists v'; split; auto.
   exploit load_result; eauto. intros B. 
   rewrite B. rewrite store_mem_contents; simpl. 
-  rewrite update_s.
+  rewrite ZMap.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. 
@@ -1070,7 +959,7 @@ Proof.
   destruct (valid_access_dec m1 chunk' b' ofs' Readable).
   rewrite pred_dec_true. 
   decEq. decEq. rewrite store_mem_contents; simpl.
-  unfold update. destruct (zeq b' b). subst b'.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'.
   apply getN_setN_outside. rewrite encode_val_length. repeat rewrite <- size_chunk_conv.
   intuition.
   auto.
@@ -1085,9 +974,8 @@ 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 update_s. 
-  replace (nat_of_Z (size_chunk chunk))
-     with (length (encode_val chunk v)).
+  rewrite ZMap.gss.
+  replace (nat_of_Z (size_chunk chunk)) with (length (encode_val chunk v)).
   rewrite getN_setN_same. auto.
   rewrite encode_val_length. auto.
   apply H. 
@@ -1102,10 +990,10 @@ Theorem loadbytes_store_other:
   loadbytes m2 b' ofs' n = loadbytes m1 b' ofs' n.
 Proof.
   intros. unfold loadbytes. 
-  destruct (range_perm_dec m1 b' ofs' (ofs' + n) Readable).
+  destruct (range_perm_dec m1 b' ofs' (ofs' + n) Cur Readable).
   rewrite pred_dec_true. 
   decEq. rewrite store_mem_contents; simpl.
-  unfold update. destruct (zeq b' b). subst b'.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'.
   destruct H. congruence.
   destruct (zle n 0). 
   rewrite (nat_of_Z_neg _ z). auto.
@@ -1122,12 +1010,12 @@ 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((setN vl p c)#q).
 Proof.
   induction vl; intros.
   simpl in H0. omegaContradiction.
   simpl length in H0. rewrite inj_S in H0. simpl. 
-  destruct (zeq p q). subst q. rewrite setN_outside. rewrite update_s. 
+  destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss. 
   auto with coqlib. omega.
   apply IHvl. auto with coqlib. omega.
 Qed.
@@ -1135,7 +1023,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 (c#q) (getN n p c).
 Proof.
   induction n; intros.
   simpl in H; omegaContradiction.
@@ -1151,14 +1039,14 @@ 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. 
-  unfold update. destruct (zeq b' b); auto. subst b'. intro DEC.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq 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].
   destruct (size_chunk_nat_pos chunk') as [sz' SZ'].
   exploit decode_pointer_shape; eauto. intros [CHUNK' PSHAPE]. clear CHUNK'.
   generalize (encode_val_shape chunk v). intro VSHAPE.  
-  set (c := mem_contents m1 b) in *.
+  set (c := m1.(mem_contents)#b) in *.
   set (c' := setN (encode_val chunk v) ofs c) in *.
   destruct (zeq ofs ofs').
 
@@ -1167,7 +1055,7 @@ Proof.
   exploit decode_val_pointer_inv; eauto. intros [A B].
   subst chunk'. simpl in B. inv B.
   generalize H4. unfold c'. rewrite <- H0. simpl. 
-  rewrite setN_outside; try omega. rewrite update_s. intros.
+  rewrite setN_outside; try omega. rewrite ZMap.gss. intros.
   exploit (encode_val_pointer_inv chunk v v_b v_o). 
   rewrite <- H0. subst mv1. eauto. intros [C [D E]].
   left; auto.
@@ -1184,9 +1072,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 (c'#ofs')).
     rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. auto.
-  assert (memval_valid_cont (c' ofs')).
+  assert (memval_valid_cont (c'#ofs')).
     inv VSHAPE. unfold c'. rewrite <- H1. simpl. 
     apply setN_property. auto.
     assert (length mvl = sz). 
@@ -1205,10 +1093,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 (c'#ofs)).
     inv VSHAPE. unfold c'. rewrite <- H0. simpl. 
-    rewrite setN_outside. rewrite update_s. auto. omega.
-  assert (~memval_valid_first (c' ofs)).
+    rewrite setN_outside. rewrite ZMap.gss. auto. omega.
+  assert (~memval_valid_first (c'#ofs)).
     rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. 
     apply H4. apply getN_in. rewrite size_chunk_conv in z. 
     rewrite SZ' in z. rewrite inj_S in z. omega. 
@@ -1217,9 +1105,9 @@ Qed.
 
 End STORE.
 
-Hint Local Resolve perm_store_1 perm_store_2: mem.
-Hint Local Resolve store_valid_block_1 store_valid_block_2: mem.
-Hint Local Resolve store_valid_access_1 store_valid_access_2
+Local Hint Resolve perm_store_1 perm_store_2: mem.
+Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.
+Local Hint Resolve store_valid_access_1 store_valid_access_2
              store_valid_access_3: mem.
 
 Theorem load_store_pointer_overlap:
@@ -1237,8 +1125,8 @@ Proof.
   rewrite LD; clear LD.
 Opaque encode_val.
   rewrite ST; simpl.
-  rewrite update_s.
-  set (c := mem_contents m1 b).
+  rewrite ZMap.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'))
   as [OK | VSHAPE].
@@ -1265,9 +1153,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 (c'#ofs') /\ c'#ofs' <> Undef).
     rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. auto.
-  assert (~memval_valid_first (c' ofs') \/ c' ofs' = Undef).
+  assert (~memval_valid_first (c'#ofs') \/ c'#ofs' = 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.
@@ -1285,11 +1173,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 (c'#ofs) /\ c'#ofs <> 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 (c'#ofs) \/ c'#ofs = Undef).
     elim ENC. 
     rewrite <- GET. rewrite SZ. simpl. intros. right; congruence.
     rewrite <- GET. rewrite SZ. simpl. intros. inv H5. auto.
@@ -1309,8 +1197,8 @@ Proof.
   rewrite LD; clear LD.
 Opaque encode_val.
   rewrite ST; simpl.
-  rewrite update_s.
-  set (c1 := mem_contents m1 b).
+  rewrite ZMap.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].
   destruct (size_chunk_nat_pos chunk') as [sz' SZ'].
@@ -1322,7 +1210,7 @@ Opaque encode_val.
 Transparent encode_val.
   unfold e, encode_val. rewrite SZ. destruct chunk; simpl; auto.
   destruct e as [ | e1 el]. contradiction.
-  rewrite SZ'. simpl. rewrite setN_outside. rewrite update_s. 
+  rewrite SZ'. simpl. rewrite setN_outside. rewrite ZMap.gss. 
   destruct e1; try contradiction. 
   destruct chunk'; auto. 
   destruct chunk'; auto. intuition.
@@ -1350,7 +1238,6 @@ Proof.
   destruct chunk1; destruct chunk2;  inv H0; unfold valid_access, align_chunk in *; try contradiction.
 Qed.
 
-
 Theorem store_signed_unsigned_8:
   forall m b ofs v,
   store Mint8signed m b ofs v = store Mint8unsigned m b ofs v.
@@ -1395,22 +1282,12 @@ Proof. intros. apply store_similar_chunks. simpl. decEq. apply encode_float32_ca
 
 Theorem range_perm_storebytes:
   forall m1 b ofs bytes,
-  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable ->
+  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable ->
   { m2 : mem | storebytes m1 b ofs bytes = Some m2 }.
 Proof.
-  intros. 
-  exists (mkmem
-             (update b (setN bytes ofs (m1.(mem_contents) b)) m1.(mem_contents))
-             m1.(mem_access)
-             m1.(bounds)
-             m1.(nextblock)
-             m1.(nextblock_pos)
-             m1.(nextblock_noaccess)
-             m1.(bounds_noaccess)
-             (setN_noread_undef m1 b ofs bytes H)).
-  unfold storebytes. 
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable).
-  decEq. decEq. apply proof_irr. 
+  intros. econstructor. unfold storebytes.
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable).
+  reflexivity. 
   contradiction.
 Qed.
 
@@ -1421,9 +1298,9 @@ Theorem storebytes_store:
   store chunk m1 b ofs v = Some m2.
 Proof.
   unfold storebytes, store. intros. 
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Writable); inv H.
+  destruct (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).
-  decEq. decEq. apply proof_irr. 
+  auto.
   elim n. constructor; auto. 
   rewrite encode_val_length in r. rewrite size_chunk_conv. auto.
 Qed.
@@ -1435,21 +1312,11 @@ Theorem store_storebytes:
 Proof.
   unfold storebytes, store. intros. 
   destruct (valid_access_dec m1 chunk b ofs Writable); inv H.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Writable).
-  decEq. decEq. apply proof_irr. 
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable).
+  auto.
   destruct v0.  elim n. 
   rewrite encode_val_length. rewrite <- size_chunk_conv. auto.
 Qed.
-
-Theorem storebytes_empty:
-  forall m b ofs, storebytes m b ofs nil = Some m.
-Proof.
-  intros. unfold storebytes. simpl. 
-  destruct (range_perm_dec m b ofs (ofs + 0) Writable).
-  decEq. destruct m; simpl; apply mkmem_ext; auto. 
-  apply extensionality. unfold update; intros. destruct (zeq x b); congruence.
-  elim n. red; intros; omegaContradiction.
-Qed.
   
 Section STOREBYTES.
 Variable m1: mem.
@@ -1462,33 +1329,33 @@ Hypothesis STORE: storebytes m1 b ofs bytes = Some m2.
 Lemma storebytes_access: mem_access m2 = mem_access m1.
 Proof.
   unfold storebytes in STORE. 
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
   inv STORE.
   auto.
 Qed.
 
 Lemma storebytes_mem_contents:
-   mem_contents m2 = update b (setN bytes ofs (m1.(mem_contents) b)) m1.(mem_contents).
+   mem_contents m2 = ZMap.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)) Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
   inv STORE.
   auto.
 Qed.
 
 Theorem perm_storebytes_1:
-  forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p.
+  forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.
 Proof.
   intros. unfold perm in *. rewrite storebytes_access; auto.
 Qed.
 
 Theorem perm_storebytes_2:
-  forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p.
+  forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p.
 Proof.
   intros. unfold perm in *. rewrite storebytes_access in H; auto.
 Qed.
 
-Hint Local Resolve perm_storebytes_1 perm_storebytes_2: mem.
+Local Hint Resolve perm_storebytes_1 perm_storebytes_2: mem.
 
 Theorem storebytes_valid_access_1:
   forall chunk' b' ofs' p,
@@ -1504,14 +1371,14 @@ Proof.
   intros. inv H. constructor; try red; auto with mem.
 Qed.
 
-Hint Local Resolve storebytes_valid_access_1 storebytes_valid_access_2: mem.
+Local Hint Resolve storebytes_valid_access_1 storebytes_valid_access_2: mem.
 
 Theorem nextblock_storebytes:
   nextblock m2 = nextblock m1.
 Proof.
   intros.
   unfold storebytes in STORE. 
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
   inv STORE.
   auto.
 Qed.
@@ -1528,24 +1395,14 @@ Proof.
   unfold valid_block; intros. rewrite nextblock_storebytes in H; auto.
 Qed.
 
-Hint Local Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem.
+Local Hint Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem.
 
 Theorem storebytes_range_perm:
-  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable.
+  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable.
 Proof.
   intros. 
   unfold storebytes in STORE. 
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
-  inv STORE.
-  auto.
-Qed.
-
-Theorem bounds_storebytes:
-  forall b', bounds m2 b' = bounds m1 b'.
-Proof.
-  intros.
-  unfold storebytes in STORE. 
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
   inv STORE.
   auto.
 Qed.
@@ -1554,10 +1411,10 @@ Theorem loadbytes_storebytes_same:
   loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.
 Proof.
   intros. unfold storebytes in STORE. unfold loadbytes. 
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable);
+  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 update_s. rewrite nat_of_Z_of_nat. 
+  decEq. inv STORE; simpl. rewrite ZMap.gss. rewrite nat_of_Z_of_nat. 
   apply getN_setN_same. 
   red; eauto with mem. 
 Qed.
@@ -1571,10 +1428,10 @@ Theorem loadbytes_storebytes_other:
   loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len.
 Proof.
   intros. unfold loadbytes.
-  destruct (range_perm_dec m1 b' ofs' (ofs' + len) Readable).
+  destruct (range_perm_dec m1 b' ofs' (ofs' + len) Cur Readable).
   rewrite pred_dec_true. 
   rewrite storebytes_mem_contents. decEq. 
-  unfold update. destruct (zeq b' b). subst b'. 
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. 
   apply getN_setN_outside. rewrite nat_of_Z_eq; auto. intuition congruence.
   auto.
   red; auto with mem.
@@ -1592,8 +1449,8 @@ Proof.
   intros. unfold load.
   destruct (valid_access_dec m1 chunk b' ofs' Readable).
   rewrite pred_dec_true. 
-  rewrite storebytes_mem_contents. decEq. 
-  unfold update. destruct (zeq b' b). subst b'. 
+  rewrite storebytes_mem_contents. decEq.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'.
   rewrite getN_setN_outside. auto. rewrite <- size_chunk_conv. intuition congruence.
   auto.
   destruct v; split; auto. red; auto with mem.
@@ -1620,12 +1477,11 @@ Theorem storebytes_concat:
 Proof.
   intros. generalize H; intro ST1. generalize H0; intro ST2.
   unfold storebytes; unfold storebytes in ST1; unfold storebytes in ST2.
-  destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Writable); try congruence.
-  destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Writable); try congruence.
-  destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Writable).
+  destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Cur Writable); try congruence.
+  destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) 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.
-  apply extensionality; intros. unfold update. destruct (zeq x b); auto.
-  subst x. rewrite zeq_true. apply setN_concat.
+  rewrite ZMap.gss.  rewrite setN_concat. symmetry. apply ZMap.set2.
   elim n.   
   rewrite app_length. rewrite inj_plus. red; intros.
   destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))).
@@ -1694,7 +1550,7 @@ Proof.
   unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. omega.
 Qed.
 
-Hint Local Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
+Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
 
 Theorem valid_block_alloc_inv:
   forall b', valid_block m2 b' -> b' = b \/ valid_block m1 b'.
@@ -1705,49 +1561,47 @@ Proof.
 Qed.
 
 Theorem perm_alloc_1:
-  forall b' ofs p, perm m1 b' ofs p -> perm m2 b' ofs p.
+  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. unfold update. destruct (zeq b' (nextblock m1)); auto.
-  elimtype False.
-  destruct (nextblock_noaccess m1 b').
-  omega.
-  rewrite bounds_noaccess in H. contradiction. rewrite H0.  simpl; omega.
+  subst b. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' (nextblock m1)); auto.
+  rewrite nextblock_noaccess in H. contradiction. omega. 
 Qed.
 
 Theorem perm_alloc_2:
-  forall ofs, lo <= ofs < hi -> perm m2 b ofs Freeable.
+  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 update_s. unfold proj_sumbool. rewrite zle_true.
+  subst b. rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true.
   rewrite zlt_true. simpl. auto with mem. omega. omega.
 Qed.
 
-Theorem perm_alloc_3:
-  forall ofs p, ofs < lo \/ hi <= ofs -> ~perm m2 b ofs p.
-Proof.
-  unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl.
-  subst b. rewrite update_s. unfold proj_sumbool.
-  destruct H. rewrite zle_false. simpl. congruence. omega.
-  rewrite zlt_false. rewrite andb_false_r.
-  intro; contradiction.
-  omega.
-Qed.
-
-Hint Local Resolve perm_alloc_1 perm_alloc_2 perm_alloc_3: mem.
-
 Theorem perm_alloc_inv:
-  forall b' ofs p, 
-  perm m2 b' ofs p ->
-  if zeq b' b then lo <= ofs < hi else perm m1 b' ofs p.
+  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.
 Proof.
   intros until p; unfold perm. inv ALLOC. simpl. 
-  unfold update. destruct (zeq b' (nextblock m1)); intros.
+  rewrite ZMap.gsspec. unfold ZIndexed.eq. destruct (zeq b' (nextblock m1)); intros.
   destruct (zle lo ofs); try contradiction. destruct (zlt ofs hi); try contradiction.
   split; auto. 
   auto.
 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.
+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.
+Qed.
+
+Local Hint Resolve perm_alloc_1 perm_alloc_2 perm_alloc_3 perm_alloc_4: mem.
+
 Theorem valid_access_alloc_other:
   forall chunk b' ofs p,
   valid_access m1 chunk b' ofs p ->
@@ -1766,7 +1620,7 @@ Proof.
   red; intros. apply perm_alloc_2. omega. 
 Qed.
 
-Hint Local Resolve valid_access_alloc_other valid_access_alloc_same: mem.
+Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
 
 Theorem valid_access_alloc_inv:
   forall chunk b' ofs p,
@@ -1778,8 +1632,8 @@ Proof.
   intros. inv H.
   generalize (size_chunk_pos chunk); intro.
   unfold eq_block. destruct (zeq b' b). subst b'.
-  assert (perm m2 b ofs p). apply H0. omega. 
-  assert (perm m2 b (ofs + size_chunk chunk - 1) p). apply H0. omega. 
+  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. 
   intuition omega. 
@@ -1787,25 +1641,6 @@ Proof.
   exploit perm_alloc_inv. apply H0. eauto. rewrite zeq_false; auto. 
 Qed.
 
-Theorem bounds_alloc:
-  forall b', bounds m2 b' = if eq_block b' b then (lo, hi) else bounds m1 b'.
-Proof.
-  injection ALLOC; intros. rewrite <- H; rewrite <- H0; simpl. 
-  unfold update. auto. 
-Qed.
-
-Theorem bounds_alloc_same:
-  bounds m2 b = (lo, hi).
-Proof.
-  rewrite bounds_alloc. apply dec_eq_true. 
-Qed. 
-
-Theorem bounds_alloc_other:
-  forall b', b' <> b -> bounds m2 b' = bounds m1 b'.
-Proof.
-  intros. rewrite bounds_alloc. apply dec_eq_false. auto.
-Qed.
-
 Theorem load_alloc_unchanged:
   forall chunk b' ofs,
   valid_block m1 b' ->
@@ -1817,7 +1652,7 @@ Proof.
   subst b'. elimtype False. eauto with mem.
   rewrite pred_dec_true; auto.
   injection ALLOC; intros. rewrite <- H2; simpl.
-  rewrite update_o. auto. rewrite H1. apply sym_not_equal; eauto with mem.
+  rewrite ZMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem.
   rewrite pred_dec_false. auto.
   eauto with mem.
 Qed.
@@ -1837,7 +1672,7 @@ Theorem load_alloc_same:
 Proof.
   intros. exploit load_result; eauto. intro. rewrite H0. 
   injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1.
-  rewrite update_s. destruct chunk; reflexivity. 
+  rewrite ZMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity.
 Qed.
 
 Theorem load_alloc_same':
@@ -1854,14 +1689,14 @@ Qed.
 
 End ALLOC.
 
-Hint Local Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
-Hint Local Resolve valid_access_alloc_other valid_access_alloc_same: mem.
+Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
+Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
 
 (** ** Properties related to [free]. *)
 
 Theorem range_perm_free:
   forall m1 b lo hi,
-  range_perm m1 b lo hi Freeable ->
+  range_perm m1 b lo hi Cur Freeable ->
   { m2: mem | free m1 b lo hi = Some m2 }.
 Proof.
   intros; unfold free. rewrite pred_dec_true; auto. econstructor; eauto.
@@ -1876,16 +1711,16 @@ Variable m2: mem.
 Hypothesis FREE: free m1 bf lo hi = Some m2.
 
 Theorem free_range_perm:
-  range_perm m1 bf lo hi Freeable.
+  range_perm m1 bf lo hi Cur Freeable.
 Proof.
-  unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Freeable); auto.
+  unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Cur Freeable); auto.
   congruence.
 Qed.
 
 Lemma free_result:
   m2 = unchecked_free m1 bf lo hi.
 Proof.
-  unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Freeable).
+  unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Cur Freeable).
   congruence. congruence.
 Qed.
 
@@ -1907,16 +1742,16 @@ Proof.
   intros. rewrite free_result in H. assumption.
 Qed.
 
-Hint Local Resolve valid_block_free_1 valid_block_free_2: mem.
+Local Hint Resolve valid_block_free_1 valid_block_free_2: mem.
 
 Theorem perm_free_1:
-  forall b ofs p,
+  forall b ofs k p,
   b <> bf \/ ofs < lo \/ hi <= ofs ->
-  perm m1 b ofs p ->
-  perm m2 b ofs p.
+  perm m1 b ofs k p ->
+  perm m2 b ofs k p.
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
-  unfold update. destruct (zeq b bf). subst b.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b.
   destruct (zle lo ofs); simpl. 
   destruct (zlt ofs hi); simpl.
   elimtype False; intuition.
@@ -1925,22 +1760,33 @@ Proof.
 Qed.
 
 Theorem perm_free_2:
-  forall ofs p, lo <= ofs < hi -> ~ perm m2 bf ofs p.
+  forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p.
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite update_s. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. 
-  simpl. congruence. omega. omega.
+  rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. 
+  simpl. tauto. omega. omega.
 Qed.
 
 Theorem perm_free_3:
-  forall b ofs p,
-  perm m2 b ofs p -> perm m1 b ofs p.
+  forall b ofs k p,
+  perm m2 b ofs k p -> perm m1 b ofs k p.
 Proof.
   intros until p. rewrite free_result. unfold perm, unchecked_free; simpl.
-  unfold update. destruct (zeq b bf). subst b. 
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b.
   destruct (zle lo ofs); simpl. 
-  destruct (zlt ofs hi); simpl. intro; contradiction.
-  congruence. auto. auto.
+  destruct (zlt ofs hi); simpl. tauto. 
+  auto. auto. auto. 
+Qed.
+
+Theorem perm_free_inv:
+  forall b ofs k p,
+  perm m1 b ofs k p ->
+  (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.
+  destruct (zle lo ofs); simpl; auto.
+  destruct (zlt ofs hi); simpl; auto.
 Qed.
 
 Theorem valid_access_free_1:
@@ -1962,9 +1808,9 @@ Proof.
   intros; red; intros. inv H2. 
   generalize (size_chunk_pos chunk); intros.
   destruct (zlt ofs lo).
-  elim (perm_free_2 lo p).
+  elim (perm_free_2 lo Cur p).
   omega. apply H3. omega. 
-  elim (perm_free_2 ofs p).
+  elim (perm_free_2 ofs Cur p).
   omega. apply H3. omega. 
 Qed.
 
@@ -1976,10 +1822,10 @@ Proof.
   intros. destruct H. split; auto. 
   red; intros. generalize (H ofs0 H1). 
   rewrite free_result. unfold perm, unchecked_free; simpl. 
-  unfold update. destruct (zeq b bf). subst b. 
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b.
   destruct (zle lo ofs0); simpl.
-  destruct (zlt ofs0 hi); simpl. 
-  intro; contradiction. congruence. auto. auto.
+  destruct (zlt ofs0 hi); simpl.
+  tauto. auto. auto. auto. 
 Qed.
 
 Theorem valid_access_free_inv_2:
@@ -1994,12 +1840,6 @@ Proof.
   elim (valid_access_free_2 chunk ofs p); auto. omega.
 Qed.
 
-Theorem bounds_free:
-  forall b, bounds m2 b = bounds m1 b.
-Proof.
-  intros. rewrite free_result; simpl. auto.
-Qed.
-
 Theorem load_free:
   forall chunk b ofs,
   b <> bf \/ lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs ->
@@ -2009,51 +1849,32 @@ Proof.
   destruct (valid_access_dec m2 chunk b ofs Readable).
   rewrite pred_dec_true. 
   rewrite free_result; auto.
-  simpl. f_equal. f_equal.
-  unfold clearN.
-  rewrite size_chunk_conv in H.
-  remember (size_chunk_nat chunk) as n; clear Heqn.
-  clear v FREE.
-  revert lo hi ofs H; induction n; intros; simpl; auto.
-  f_equal.
-  destruct (zeq b bf); auto. subst bf.
-  destruct (zle lo ofs); auto. destruct (zlt ofs hi); auto.
-  elimtype False.
-  destruct H as [? | [? | [? | ?]]]; try omega.
-  contradict H; auto.
-  rewrite inj_S in H; omega.
-  apply IHn.
-  rewrite inj_S in H.
-  destruct H as [? | [? | [? | ?]]]; auto.
-  unfold block in *; omega.
-  unfold block in *; omega.
-
-  apply valid_access_free_inv_1; auto. 
+  eapply valid_access_free_inv_1; eauto. 
   rewrite pred_dec_false; auto.
   red; intro; elim n. eapply valid_access_free_1; eauto. 
 Qed.
 
 End FREE.
 
-Hint Local Resolve valid_block_free_1 valid_block_free_2
+Local Hint Resolve valid_block_free_1 valid_block_free_2
              perm_free_1 perm_free_2 perm_free_3 
              valid_access_free_1 valid_access_free_inv_1: mem.
 
 (** ** Properties related to [drop_perm] *)
 
 Theorem range_perm_drop_1:
-  forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> range_perm m b lo hi p.
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> range_perm m b lo hi Cur Freeable.
 Proof.
   unfold drop_perm; intros. 
-  destruct (range_perm_dec m b lo hi p). auto. discriminate.
+  destruct (range_perm_dec m b lo hi Cur Freeable). auto. discriminate.
 Qed.
 
 Theorem range_perm_drop_2:
   forall m b lo hi p,
-  range_perm m b lo hi p -> {m' | drop_perm m b lo hi p = Some m' }.
+  range_perm m b lo hi Cur Freeable -> {m' | drop_perm m b lo hi p = Some m' }.
 Proof.
   unfold drop_perm; intros. 
-  destruct (range_perm_dec m b lo hi p). econstructor. eauto. contradiction.
+  destruct (range_perm_dec m b lo hi Cur Freeable). econstructor. eauto. contradiction.
 Qed.
 
 Section DROP.
@@ -2068,59 +1889,64 @@ Hypothesis DROP: drop_perm m b lo hi p = Some m'.
 Theorem nextblock_drop:
   nextblock m' = nextblock m.
 Proof.
-  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP; auto.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP; auto.
+Qed.
+
+Theorem drop_perm_valid_block_1:
+  forall b', valid_block m b' -> valid_block m' b'.
+Proof.
+  unfold valid_block; rewrite nextblock_drop; auto.
+Qed.
+
+Theorem drop_perm_valid_block_2:
+  forall b', valid_block m' b' -> valid_block m b'.
+Proof.
+  unfold valid_block; rewrite nextblock_drop; auto.
 Qed.
 
 Theorem perm_drop_1:
-  forall ofs, lo <= ofs < hi -> perm m' b ofs p.
+  forall ofs k, lo <= ofs < hi -> perm m' b ofs k p.
 Proof.
   intros.
-  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
-  unfold perm. simpl. rewrite update_s. unfold proj_sumbool. 
+  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. 
   rewrite zle_true. rewrite zlt_true. simpl. constructor.
   omega. omega. 
 Qed.
   
 Theorem perm_drop_2:
-  forall ofs p', lo <= ofs < hi -> perm m' b ofs p' -> perm_order p p'.
+  forall ofs k p', lo <= ofs < hi -> perm m' b ofs k p' -> perm_order p p'.
 Proof.
   intros.
-  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
-  revert H0. unfold perm; simpl. rewrite update_s. unfold proj_sumbool. 
+  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. 
   rewrite zle_true. rewrite zlt_true. simpl. auto. 
   omega. omega. 
 Qed.
 
 Theorem perm_drop_3:
-  forall b' ofs p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs p' -> perm m' b' ofs p'.
+  forall b' ofs k p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs k p' -> perm m' b' ofs k p'.
 Proof.
   intros.
-  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
-  unfold perm; simpl. unfold update. destruct (zeq b' b). subst b'. 
+  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 proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). 
   byContradiction. intuition omega.
   auto. auto. auto.
 Qed.
 
 Theorem perm_drop_4:
-  forall b' ofs p', perm m' b' ofs p' -> perm m b' ofs p'.
+  forall b' ofs k p', perm m' b' ofs k p' -> perm m b' ofs k p'.
 Proof.
   intros.
-  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
-  revert H. unfold perm; simpl. unfold update. destruct (zeq b' b). 
+  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).
   subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi).
-  simpl. intros. apply perm_implies with p. apply r. tauto. auto.
+  simpl. intros. apply perm_implies with p. apply perm_implies with Freeable. apply perm_cur.
+  apply r. tauto. auto with mem. auto.
   auto. auto. auto.
 Qed.
 
-Theorem bounds_drop:
-  forall b', bounds m' b' = bounds m b'.
-Proof.
-  intros.
-  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP.
-  unfold bounds; simpl. auto.
-Qed.
-
 Lemma valid_access_drop_1:
   forall chunk b' ofs p', 
   b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p p' ->
@@ -2167,13 +1993,7 @@ Proof.
   unfold load.
   destruct (valid_access_dec m chunk b' ofs Readable).
   rewrite pred_dec_true.
-  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP. simpl.
-  unfold update. destruct (zeq b' b). subst b'. decEq. decEq. 
-  apply getN_exten. rewrite <- size_chunk_conv. intros.
-  unfold proj_sumbool. destruct (zle lo i). destruct (zlt i hi). destruct (perm_order_dec p Readable).
-  auto.
-  elimtype False. intuition.
-  auto. auto. auto.
+  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. simpl. auto.
   eapply valid_access_drop_1; eauto. 
   rewrite pred_dec_false. auto.
   red; intros; elim n. eapply valid_access_drop_2; eauto.
@@ -2181,85 +2001,6 @@ Qed.
 
 End DROP.
 
-(** * Extensionality properties *)
-
-Lemma mem_access_ext:
-  forall m1 m2, perm m1 = perm m2 -> mem_access m1 = mem_access m2.
-Proof.
-  intros.
-  apply extensionality; intro b.
-  apply extensionality; intro ofs.
-  case_eq (mem_access m1 b ofs); case_eq (mem_access m2 b ofs); intros; auto.
-  assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
-  assert (perm m1 b ofs p0 <-> perm m2 b ofs p0) by (rewrite H; intuition).
-  unfold perm, perm_order' in H2,H3.
-  rewrite H0 in H2,H3; rewrite H1 in H2,H3.
-  f_equal.
-  assert (perm_order p p0 -> perm_order p0 p -> p0=p) by
-    (clear; intros; inv H; inv H0; auto).
-  intuition.
-  assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
-  unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2.
-  assert (perm_order p p) by auto with mem.
-  intuition.
-  assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
-  unfold perm, perm_order'  in H2; rewrite H0 in H2; rewrite H1 in H2.
-  assert (perm_order p p) by auto with mem.
-  intuition.
-Qed.
-
-Lemma mem_ext': 
-  forall m1 m2, 
-  mem_access m1 = mem_access m2 ->
-  nextblock m1 = nextblock m2 ->
-  (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) ->
-  (forall b ofs, perm_order' (mem_access m1 b ofs) Readable -> 
-                          mem_contents m1 b ofs = mem_contents m2 b ofs) ->
-  m1 = m2.
-Proof.
-  intros.
-  destruct m1; destruct m2; simpl in *.
-  destruct H; subst.
-  apply mkmem_ext; auto.
-  apply extensionality; intro b.
-  apply extensionality; intro ofs.
-  destruct (perm_order'_dec (mem_access0 b ofs) Readable).
-  auto.
-  destruct (noread_undef0 b ofs); try contradiction.
-  destruct (noread_undef1 b ofs); try contradiction.
-  congruence.
-  apply extensionality; intro b.
-  destruct (nextblock_noaccess0 b); auto.
-  destruct (nextblock_noaccess1 b); auto.
-  congruence.
-Qed.
-
-Theorem mem_ext:
-  forall m1 m2, 
-  perm m1 = perm m2 ->
-  nextblock m1 = nextblock m2 ->
-  (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) ->
-  (forall b ofs, loadbytes m1 b ofs 1 = loadbytes m2 b ofs 1) ->
-  m1 = m2.
-Proof.
-  intros.
-  generalize (mem_access_ext _ _ H); clear H; intro.
-  apply mem_ext'; auto.
-  intros.
-  specialize (H2 b ofs).
-  unfold loadbytes in H2; simpl in H2.
-  destruct (range_perm_dec m1 b ofs (ofs+1)).
-  destruct (range_perm_dec m2 b ofs (ofs+1)).
-  inv H2; auto.
-  contradict n.
-  intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'.
-  unfold perm, perm_order'.
-    rewrite <- H; destruct (mem_access m1 b ofs); try destruct p; intuition.
-  contradict n.
-  intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'.
-  unfold perm. destruct (mem_access m1 b ofs); try destruct p; intuition.
-Qed.
-
 (** * Generic injections *)
 
 (** A memory state [m1] generically injects into another memory state [m2] via the
@@ -2272,6 +2013,11 @@ Qed.
 
 Record mem_inj (f: meminj) (m1 m2: mem) : Prop :=
   mk_mem_inj {
+    mi_perm:
+      forall b1 b2 delta ofs k p,
+      f b1 = Some(b2, delta) ->
+      perm m1 b1 ofs k p ->
+      perm m2 b2 (ofs + delta) k p;
     mi_access:
       forall b1 b2 delta chunk ofs p,
       f b1 = Some(b2, delta) ->
@@ -2280,33 +2026,28 @@ Record mem_inj (f: meminj) (m1 m2: mem) : Prop :=
     mi_memval:
       forall b1 ofs b2 delta,
       f b1 = Some(b2, delta) ->
-      perm m1 b1 ofs Nonempty ->
-      memval_inject f (m1.(mem_contents) b1 ofs) (m2.(mem_contents) b2 (ofs + delta))
+      perm m1 b1 ofs Cur Readable ->
+      memval_inject f (m1.(mem_contents)#b1#ofs) (m2.(mem_contents)#b2#(ofs + delta))
   }.
 
 (** Preservation of permissions *)
 
 Lemma perm_inj:
-  forall f m1 m2 b1 ofs p b2 delta,
+  forall f m1 m2 b1 ofs k p b2 delta,
   mem_inj f m1 m2 ->
-  perm m1 b1 ofs p ->
+  perm m1 b1 ofs k p ->
   f b1 = Some(b2, delta) ->
-  perm m2 b2 (ofs + delta) p.
+  perm m2 b2 (ofs + delta) k p.
 Proof.
-  intros. 
-  assert (valid_access m1 Mint8unsigned b1 ofs p).
-    split. red; intros. simpl in H2. replace ofs0 with ofs by omega. auto.
-    simpl. apply Zone_divide.
-  exploit mi_access; eauto. intros [A B].
-  apply A. simpl; omega. 
+  intros. eapply mi_perm; eauto. 
 Qed.
 
 Lemma range_perm_inj:
-  forall f m1 m2 b1 lo hi p b2 delta,
+  forall f m1 m2 b1 lo hi k p b2 delta,
   mem_inj f m1 m2 ->
-  range_perm m1 b1 lo hi p ->
+  range_perm m1 b1 lo hi k p ->
   f b1 = Some(b2, delta) ->
-  range_perm m2 b2 (lo + delta) (hi + delta) p.
+  range_perm m2 b2 (lo + delta) (hi + delta) k p.
 Proof.
   intros; red; intros.
   replace ofs with ((ofs - delta) + delta) by omega.
@@ -2320,18 +2061,17 @@ Lemma getN_inj:
   mem_inj f m1 m2 ->
   f b1 = Some(b2, delta) ->
   forall n ofs,
-  range_perm m1 b1 ofs (ofs + Z_of_nat n) Readable ->
+  range_perm m1 b1 ofs (ofs + Z_of_nat n) Cur Readable ->
   list_forall2 (memval_inject f) 
-               (getN n ofs (m1.(mem_contents) b1))
-               (getN n (ofs + delta) (m2.(mem_contents) b2)).
+               (getN n ofs (m1.(mem_contents)#b1))
+               (getN n (ofs + delta) (m2.(mem_contents)#b2)).
 Proof.
   induction n; intros; simpl.
   constructor.
   rewrite inj_S in H1. 
   constructor. 
   eapply mi_memval; eauto.
-  apply perm_implies with Readable.
-  apply H1. omega. constructor. 
+  apply H1. omega.  
   replace (ofs + delta + 1) with ((ofs + 1) + delta) by omega.
   apply IHn. red; intros; apply H1; omega. 
 Qed.
@@ -2344,7 +2084,7 @@ Lemma load_inj:
   exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2.
 Proof.
   intros.
-  exists (decode_val chunk (getN (size_chunk_nat chunk) (ofs + delta) (m2.(mem_contents) b2))).
+  exists (decode_val chunk (getN (size_chunk_nat chunk) (ofs + delta) (m2.(mem_contents)#b2))).
   split. unfold load. apply pred_dec_true.  
   eapply mi_access; eauto with mem. 
   exploit load_result; eauto. intro. rewrite H2. 
@@ -2361,8 +2101,8 @@ Lemma loadbytes_inj:
               /\ list_forall2 (memval_inject f) bytes1 bytes2.
 Proof.
   intros. unfold loadbytes in *. 
-  destruct (range_perm_dec m1 b1 ofs (ofs + len) Readable); inv H0.
-  exists (getN (nat_of_Z len) (ofs + delta) (m2.(mem_contents) b2)).
+  destruct (range_perm_dec m1 b1 ofs (ofs + len) Cur Readable); inv H0.
+  exists (getN (nat_of_Z len) (ofs + delta) (m2.(mem_contents)#b2)).
   split. apply pred_dec_true.  
   replace (ofs + delta + len) with ((ofs + len) + delta) by omega.
   eapply range_perm_inj; eauto with mem. 
@@ -2377,46 +2117,27 @@ 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 (c1#q) (c2#(q + delta))) ->
+  (forall q, access q -> memval_inject f ((setN vl1 p c1)#q) 
+                                         ((setN vl2 (p + delta) c2)#(q + delta))).
 Proof.
   induction 1; intros; simpl. 
   auto.
   replace (p + delta + 1) with ((p + 1) + delta) by omega.
   apply IHlist_forall2; auto. 
-  intros. unfold update at 1. destruct (zeq q0 p). subst q0.
-  rewrite update_s. auto.
-  rewrite update_o. auto. omega.
+  intros. rewrite ZMap.gsspec at 1. destruct (ZIndexed.eq q0 p). subst q0.
+  rewrite ZMap.gss. auto. 
+  rewrite ZMap.gso. auto. unfold ZIndexed.t in *. omega.
 Qed.
 
 Definition meminj_no_overlap (f: meminj) (m: mem) : Prop :=
-  forall b1 b1' delta1 b2 b2' delta2,
-  b1 <> b2 ->
-  f b1 = Some (b1', delta1) ->
-  f b2 = Some (b2', delta2) ->
-  b1' <> b2' 
-(*
-  \/ low_bound m b1 >= high_bound m b1
-  \/ low_bound m b2 >= high_bound m b2 *)
-  \/ high_bound m b1 + delta1 <= low_bound m b2 + delta2 
-  \/ high_bound m b2 + delta2 <= low_bound m b1 + delta1.
-
-Lemma meminj_no_overlap_perm:
-  forall f m b1 b1' delta1 b2 b2' delta2 ofs1 ofs2,
-  meminj_no_overlap f m ->
+  forall b1 b1' delta1 b2 b2' delta2 ofs1 ofs2,
   b1 <> b2 ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
-  perm m b1 ofs1 Nonempty ->
-  perm m b2 ofs2 Nonempty ->
+  perm m b1 ofs1 Max Nonempty ->
+  perm m b2 ofs2 Max Nonempty ->
   b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2.
-Proof.
-  intros. exploit H; eauto. intro. 
-  exploit perm_in_bounds. eexact H3. intro. 
-  exploit perm_in_bounds. eexact H4. intro.
-  destruct H5. auto. right. omega. 
-Qed.
 
 Lemma store_mapped_inj:
   forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
@@ -2429,41 +2150,43 @@ Lemma store_mapped_inj:
     store chunk m2 b2 (ofs + delta) v2 = Some n2
     /\ mem_inj f n1 n2.
 Proof.
-  intros. inversion H. 
+  intros.
   assert (valid_access m2 chunk b2 (ofs + delta) Writable).
-    eapply mi_access0; eauto with mem.
+    eapply mi_access; eauto with mem.
   destruct (valid_access_store _ _ _ _ v2 H4) as [n2 STORE]. 
-  exists n2; split. eauto.
+  exists n2; split. auto.
   constructor.
+(* perm *)
+  intros. eapply perm_store_1; [eexact STORE|].
+  eapply mi_perm; eauto.
+  eapply perm_store_2; eauto. 
 (* access *)
-  intros.
-  eapply store_valid_access_1; [apply STORE |].
-  eapply mi_access0; eauto.
-  eapply store_valid_access_2; [apply H0 |]. auto.
+  intros. eapply store_valid_access_1; [apply STORE |].
+  eapply mi_access; eauto.
+  eapply store_valid_access_2; eauto.
 (* mem_contents *)
   intros.
-  assert (perm m1 b0 ofs0 Nonempty). eapply perm_store_2; eauto. 
   rewrite (store_mem_contents _ _ _ _ _ _ H0).
   rewrite (store_mem_contents _ _ _ _ _ _ STORE).
-  unfold update. 
-  destruct (zeq b0 b1). subst b0.
+  repeat rewrite ZMap.gsspec. 
+  destruct (ZIndexed.eq b0 b1). subst b0.
   (* block = b1, block = b2 *)
   assert (b3 = b2) by congruence. subst b3.
   assert (delta0 = delta) by congruence. subst delta0.
   rewrite zeq_true.
-  apply setN_inj with (access := fun ofs => perm m1 b1 ofs Nonempty).
-  apply encode_val_inject; auto. auto. auto. 
-  destruct (zeq b3 b2). subst b3.
+  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.
   (* block <> b1, block = b2 *)
-  rewrite setN_other. auto.
+  rewrite setN_other. eapply mi_memval; eauto. eauto with mem. 
   rewrite encode_val_length. rewrite <- size_chunk_conv. intros. 
   assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta).
-    eapply meminj_no_overlap_perm; eauto. 
+    eapply H1; eauto. eauto 6 with mem.
     exploit store_valid_access_3. eexact H0. intros [A B].
-    eapply perm_implies. apply A. omega. auto with mem.
-  destruct H9. congruence. omega.
+    eapply perm_implies. apply perm_cur_max. apply A. omega. auto with mem.
+  destruct H8. congruence. omega.
   (* block <> b1, block <> b2 *)
-  eauto.
+  eapply mi_memval; eauto. eauto with mem. 
 Qed.
 
 Lemma store_unmapped_inj:
@@ -2473,14 +2196,15 @@ Lemma store_unmapped_inj:
   f b1 = None ->
   mem_inj f n1 m2.
 Proof.
-  intros. inversion H.
-  constructor.
+  intros. constructor.
+(* perm *)
+  intros. eapply mi_perm; eauto with mem.
 (* access *)
-  eauto with mem.
+  intros. eapply mi_access; eauto with mem.
 (* mem_contents *)
   intros. 
   rewrite (store_mem_contents _ _ _ _ _ _ H0).
-  rewrite update_o. eauto with mem. 
+  rewrite ZMap.gso. eapply mi_memval; eauto with mem. 
   congruence.
 Qed.
 
@@ -2489,21 +2213,25 @@ Lemma store_outside_inj:
   mem_inj f m1 m2 ->
   (forall b' delta ofs',
     f b' = Some(b, delta) ->
-    perm m1 b' ofs' Nonempty ->
-    ofs' + delta < ofs \/ ofs' + delta >= ofs + size_chunk chunk) ->
+    perm m1 b' ofs' Cur Readable -> 
+    ofs <= ofs' + delta < ofs + size_chunk chunk -> False) ->
   store chunk m2 b ofs v = Some m2' ->
   mem_inj f m1 m2'.
 Proof.
-  intros. inversion H. constructor.
+  intros. inv H. constructor.
+(* perm *)
+  eauto with mem.
 (* access *)
   eauto with mem.
 (* mem_contents *)
   intros. 
   rewrite (store_mem_contents _ _ _ _ _ _ H1).
-  unfold update. destruct (zeq b2 b). subst b2.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b2 b). subst b2. 
   rewrite setN_outside. auto. 
   rewrite encode_val_length. rewrite <- size_chunk_conv. 
-  eapply H0; eauto. 
+  destruct (zlt (ofs0 + delta) ofs); auto.
+  destruct (zle (ofs + size_chunk chunk) (ofs0 + delta)). omega. 
+  byContradiction. eapply H0; eauto. omega. 
   eauto with mem.
 Qed.
 
@@ -2519,7 +2247,7 @@ Lemma storebytes_mapped_inj:
     /\ mem_inj f n1 n2.
 Proof.
   intros. inversion H. 
-  assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z_of_nat (length bytes2)) Writable).
+  assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z_of_nat (length bytes2)) Cur Writable).
     replace (ofs + delta + Z_of_nat (length bytes2))
        with ((ofs + Z_of_nat (length bytes1)) + delta).
     eapply range_perm_inj; eauto with mem. 
@@ -2528,33 +2256,37 @@ Proof.
   destruct (range_perm_storebytes _ _ _ _ H4) as [n2 STORE]. 
   exists n2; split. eauto.
   constructor.
+(* perm *)
+  intros.
+  eapply perm_storebytes_1; [apply STORE |].
+  eapply mi_perm0; eauto.
+  eapply perm_storebytes_2; eauto.
 (* access *)
   intros.
   eapply storebytes_valid_access_1; [apply STORE |].
   eapply mi_access0; eauto.
-  eapply storebytes_valid_access_2; [apply H0 |]. auto.
+  eapply storebytes_valid_access_2; eauto.
 (* mem_contents *)
   intros.
-  assert (perm m1 b0 ofs0 Nonempty). eapply perm_storebytes_2; eauto. 
+  assert (perm m1 b0 ofs0 Cur Readable). eapply perm_storebytes_2; eauto. 
   rewrite (storebytes_mem_contents _ _ _ _ _ H0).
   rewrite (storebytes_mem_contents _ _ _ _ _ STORE).
-  unfold update. 
-  destruct (zeq b0 b1). subst b0.
+  repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b1). subst b0.
   (* block = b1, block = b2 *)
   assert (b3 = b2) by congruence. subst b3.
   assert (delta0 = delta) by congruence. subst delta0.
   rewrite zeq_true.
-  apply setN_inj with (access := fun ofs => perm m1 b1 ofs Nonempty); auto.
-  destruct (zeq b3 b2). subst b3.
+  apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable); auto.
+  destruct (ZIndexed.eq b3 b2). subst b3.
   (* block <> b1, block = b2 *)
   rewrite setN_other. auto.
   intros.
   assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta).
-    eapply meminj_no_overlap_perm; eauto. 
+    eapply H1; eauto 6 with mem.
     exploit storebytes_range_perm. eexact H0. 
     instantiate (1 := r - delta). 
     rewrite (list_forall2_length H3). omega.
-    eauto with mem.
+    eauto 6 with mem.
   destruct H9. congruence. omega.
   (* block <> b1, block <> b2 *)
   eauto.
@@ -2569,12 +2301,14 @@ Lemma storebytes_unmapped_inj:
 Proof.
   intros. inversion H.
   constructor.
+(* perm *)
+  intros. eapply mi_perm0; eauto. eapply perm_storebytes_2; eauto. 
 (* access *)
   intros. eapply mi_access0; eauto. eapply storebytes_valid_access_2; eauto. 
 (* mem_contents *)
   intros. 
   rewrite (storebytes_mem_contents _ _ _ _ _ H0).
-  rewrite update_o. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto.
+  rewrite ZMap.gso. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto.
   congruence.
 Qed.
 
@@ -2583,20 +2317,24 @@ Lemma storebytes_outside_inj:
   mem_inj f m1 m2 ->
   (forall b' delta ofs',
     f b' = Some(b, delta) ->
-    perm m1 b' ofs' Nonempty ->
-    ofs' + delta < ofs \/ ofs' + delta >= ofs + Z_of_nat (length bytes2)) ->
+    perm m1 b' ofs' Cur Readable -> 
+    ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) ->
   storebytes m2 b ofs bytes2 = Some m2' ->
   mem_inj f m1 m2'.
 Proof.
   intros. inversion H. constructor.
+(* perm *)
+  intros. eapply perm_storebytes_1; eauto with mem.
 (* access *)
   intros. eapply storebytes_valid_access_1; eauto with mem.
 (* mem_contents *)
   intros. 
   rewrite (storebytes_mem_contents _ _ _ _ _ H1).
-  unfold update. destruct (zeq b2 b). subst b2.
+  rewrite ZMap.gsspec. destruct (ZIndexed.eq b2 b). subst b2.
   rewrite setN_outside. auto. 
-  eapply H0; eauto. 
+  destruct (zlt (ofs0 + delta) ofs); auto.
+  destruct (zle (ofs + Z_of_nat (length bytes2)) (ofs0 + delta)). omega. 
+  byContradiction. eapply H0; eauto. omega. 
   eauto with mem.
 Qed.
 
@@ -2610,17 +2348,17 @@ Lemma alloc_right_inj:
 Proof.
   intros. injection H0. intros NEXT MEM.
   inversion H. constructor.
+(* perm *)
+  intros. eapply perm_alloc_1; eauto. 
 (* access *)
-  intros. eauto with mem. 
+  intros. eapply valid_access_alloc_other; eauto. 
 (* mem_contents *)
   intros.
-  assert (valid_access m2 Mint8unsigned b0 (ofs + delta) Nonempty).
-    eapply mi_access0; eauto.
-    split. simpl. red; intros. assert (ofs0 = ofs) by omega. congruence.
-    simpl. apply Zone_divide. 
+  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 update_o. eauto with mem.
-  rewrite NEXT. apply sym_not_equal. eauto with mem. 
+  rewrite <- MEM; simpl. rewrite ZMap.gso. eauto with mem.
+  rewrite NEXT. eauto with mem. 
 Qed.
 
 Lemma alloc_left_unmapped_inj:
@@ -2631,15 +2369,18 @@ Lemma alloc_left_unmapped_inj:
   mem_inj f m1' m2.
 Proof.
   intros. inversion H. constructor.
+(* perm *)
+  intros. exploit perm_alloc_inv; eauto. intros. 
+  destruct (zeq b0 b1). congruence. eauto. 
 (* access *)
-  unfold update; intros.
-  exploit valid_access_alloc_inv; eauto. unfold eq_block. intros. 
+  intros. exploit valid_access_alloc_inv; eauto. unfold eq_block. intros. 
   destruct (zeq b0 b1). congruence. eauto.
 (* mem_contents *)
   injection H0; intros NEXT MEM. intros. 
-  rewrite <- MEM; simpl. rewrite NEXT. unfold update.
-  exploit perm_alloc_inv; eauto. intros. 
-  destruct (zeq b0 b1). constructor. eauto.
+  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. 
 Qed.
 
 Definition inj_offset_aligned (delta: Z) (size: Z) : Prop :=
@@ -2651,25 +2392,30 @@ Lemma alloc_left_mapped_inj:
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
   inj_offset_aligned delta (hi-lo) ->
-  (forall ofs p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) p) ->
+  (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   f b1 = Some(b2, delta) ->
   mem_inj f m1' m2.
 Proof.
   intros. inversion H. constructor.
+(* perm *)
+  intros. 
+  exploit perm_alloc_inv; eauto. intros. destruct (zeq 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. inversion H5; clear H5; subst b3 delta0.
+  destruct (zeq b0 b1). subst b0. rewrite H4 in H5. inv H5. 
   split. red; intros. 
-  replace ofs0 with ((ofs0 - delta) + delta) by omega. 
+  replace ofs0 with ((ofs0 - delta0) + delta0) by omega. 
   apply H3. omega. 
   destruct H6. apply Zdivide_plus_r. auto. apply H2. omega.
   eauto.
 (* mem_contents *)
   injection H0; intros NEXT MEM. 
-  intros. rewrite <- MEM; simpl. rewrite NEXT. unfold update.
-  exploit perm_alloc_inv; eauto. intros. 
-  destruct (zeq b0 b1). constructor. eauto.
+  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.
 Qed.
 
 Lemma free_left_inj:
@@ -2679,45 +2425,42 @@ Lemma free_left_inj:
   mem_inj f m1' m2.
 Proof.
   intros. exploit free_result; eauto. intro FREE. inversion H. constructor.
+(* perm *)
+  intros. eauto with mem.
 (* access *)
   intros. eauto with mem. 
 (* mem_contents *)
-  intros. rewrite FREE; simpl.
-  assert (b=b1 /\ lo <= ofs < hi \/ (b<>b1 \/ ofs<lo \/ hi <= ofs)) by (unfold block; omega).
-  destruct H3.
-  destruct H3. subst b1.
-  rewrite (clearN_in _ _ _ _ _ H4); auto.
-  constructor.
-  rewrite (clearN_out _ _ _ _ _ _ H3).
-  apply mi_memval0; auto.
-  eapply perm_free_3; eauto.
+  intros. rewrite FREE; simpl. eauto with mem.
 Qed.
 
-
 Lemma free_right_inj:
   forall f m1 m2 b lo hi m2',
   mem_inj f m1 m2 ->
   free m2 b lo hi = Some m2' ->
-  (forall b1 delta ofs p,
-    f b1 = Some(b, delta) -> perm m1 b1 ofs p ->
-    lo <= ofs + delta < hi -> False) ->
+  (forall b' delta ofs k p,
+    f b' = Some(b, delta) ->
+    perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) ->
   mem_inj f m1 m2'.
 Proof.
-  intros. exploit free_result; eauto. intro FREE. inversion H. constructor.
+  intros. exploit free_result; eauto. intro FREE. inversion H.
+  assert (PERM:
+    forall b1 b2 delta ofs k p,
+    f b1 = Some (b2, delta) ->
+    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. 
+  assert (~ (lo <= ofs + delta < hi)). red; intros; eapply H1; eauto. 
+  omega.
+  constructor.
+(* perm *)
+  auto.
 (* access *)
   intros. exploit mi_access0; eauto. intros [RG AL]. split; auto.
-  red; intros. eapply perm_free_1; eauto. 
-  destruct (zeq b2 b); auto. subst b. right.
-  destruct (zlt ofs0 lo); auto. destruct (zle hi ofs0); auto.
-  elimtype False. eapply H1 with (ofs := ofs0 - delta). eauto. 
-  apply H3. omega. omega.
+  red; intros. replace ofs0 with ((ofs0 - delta) + delta) by omega. 
+  eapply PERM. eauto. apply H3. omega. 
 (* mem_contents *)
-  intros. rewrite FREE; simpl.
-  specialize (mi_memval0 _ _ _ _ H2 H3).
-  assert (b=b2 /\ lo <= ofs+delta < hi \/ (b<>b2 \/ ofs+delta<lo \/ hi <= ofs+delta)) by (unfold block; omega).
-  destruct H4. destruct H4. subst b2.
-  specialize (H1 _ _ _ _ H2 H3). elimtype False; auto.
-  rewrite (clearN_out _ _ _ _ _ _ H4); auto.
+  intros. rewrite FREE; simpl. eauto. 
 Qed.
 
 (** Preservation of [drop_perm] operations. *)
@@ -2730,13 +2473,16 @@ Lemma drop_unmapped_inj:
   mem_inj f m1' m2.
 Proof.
   intros. inv H. constructor. 
+(* perm *)
+  intros. eapply mi_perm0; eauto. eapply perm_drop_4; eauto. 
+(* access *)
   intros. eapply mi_access0. eauto.
-  eapply valid_access_drop_2; eauto. 
-  intros. replace (mem_contents m1' b1 ofs) with (mem_contents m1 b1 ofs). 
-  apply mi_memval0; auto. 
-  eapply perm_drop_4; eauto. 
-  unfold drop_perm in H0. destruct (range_perm_dec m1 b lo hi p); inv H0. 
-  simpl. rewrite update_o; auto. congruence.
+  eapply valid_access_drop_2; eauto.
+(* contents *)
+  intros.
+  replace (m1'.(mem_contents)#b1#ofs) with (m1.(mem_contents)#b1#ofs).
+  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.
 
 Lemma drop_mapped_inj:
@@ -2755,103 +2501,84 @@ Proof.
   replace ofs with ((ofs - delta) + delta) by omega.
   eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. omega. 
   destruct X as [m2' DROP]. exists m2'; split; auto.
-  inv H. constructor; intros.
+  inv H.
+  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).
+    (* b1 = b0 *)
+    subst b0. rewrite H2 in H; inv H.
+    destruct (zlt (ofs + delta0) (lo + delta0)). eapply perm_drop_3; eauto.
+    destruct (zle (hi + delta0) (ofs + delta0)). eapply perm_drop_3; eauto.
+    assert (perm_order p p0).
+      eapply perm_drop_2.  eexact H0. instantiate (1 := ofs). omega. eauto. 
+    apply perm_implies with p; auto. 
+    eapply perm_drop_1. eauto. omega.
+    (* b1 <> b0 *)
+    eapply perm_drop_3; eauto.
+    destruct (zeq b3 b2); auto.
+    destruct (zlt (ofs + delta0) (lo + delta)); auto.
+    destruct (zle (hi + delta) (ofs + delta0)); auto.
+    exploit H1; eauto.
+    instantiate (1 := ofs + delta0 - delta). 
+    apply perm_cur_max. apply perm_implies with Freeable.
+    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.
+  constructor.
+(* perm *)
+  auto.
 (* access *)
-  exploit mi_access0; eauto. eapply valid_access_drop_2; eauto.
+  intros. exploit mi_access0; eauto. eapply valid_access_drop_2; eauto.
   intros [A B]. split; auto. red; intros.
-  destruct (eq_block b1 b0). subst b0. rewrite H2 in H; inv H.
-  (* b1 = b0 *)
-  destruct (zlt ofs0 (lo + delta0)). eapply perm_drop_3; eauto. 
-  destruct (zle (hi + delta0) ofs0). eapply perm_drop_3; eauto.
-  destruct H3 as [C D].
-  assert (perm_order p p0).
-    eapply perm_drop_2. eexact H0. instantiate (1 := ofs0 - delta0). omega. 
-    apply C. omega. 
-  apply perm_implies with p; auto.
-  eapply perm_drop_1. eauto. omega.
-  (* b1 <> b0 *)
-  eapply perm_drop_3; eauto.
-  exploit H1; eauto. intros [P | P]. auto. right. 
-  destruct (zlt lo hi). 
-  exploit range_perm_in_bounds. eapply range_perm_drop_1. eexact H0. auto. 
-  intros [U V].
-  exploit valid_access_drop_2. eexact H0. eauto.
-  intros [C D].
-  exploit range_perm_in_bounds. eexact C. generalize (size_chunk_pos chunk); omega. 
-  intros [X Y].
-  generalize (size_chunk_pos chunk). omega.
-  omega.
+  replace ofs0 with ((ofs0 - delta0) + delta0) by omega.
+  eapply PERM; eauto. apply H3. omega. 
 (* memval *)
-  assert (A: perm m1 b0 ofs Nonempty). eapply perm_drop_4; eauto.
-  exploit mi_memval0; eauto. intros B.
-  unfold drop_perm in *. 
-  destruct (range_perm_dec m1 b1 lo hi p); inversion H0; clear H0. clear H5.
-  destruct (range_perm_dec m2 b2 (lo + delta) (hi + delta) p); inversion DROP; clear DROP. clear H4.
-  simpl. unfold update. destruct (zeq b0 b1). 
-  (* b1 = b0 *)
-  subst b0. rewrite H2 in H; inv H. rewrite zeq_true. unfold proj_sumbool. 
-  destruct (zle lo ofs).
-  rewrite zle_true. 
-  destruct (zlt ofs hi).
-  rewrite zlt_true.
-  destruct (perm_order_dec p Readable).
-  simpl. auto.
-  simpl. constructor.
-  omega.
-  rewrite zlt_false. simpl. auto. omega. 
-  omega.
-  rewrite zle_false. simpl. auto. omega.
-  (* b1 <> b0 *)
-  destruct (zeq b3 b2).
-  (* b2 = b3 *)
-  subst b3. exploit H1. eauto. eauto. eauto. intros [P | P]. congruence.
-  exploit perm_in_bounds; eauto. intros X.
-  destruct (zle (lo + delta) (ofs + delta0)).
-  destruct (zlt (ofs + delta0) (hi + delta)).
-  destruct (zlt lo hi). 
-  exploit range_perm_in_bounds. eexact r. auto. intros [Y Z].
-  omegaContradiction.
-  omegaContradiction.
-  simpl. auto.
-  simpl. auto.
-  auto.
+  intros.
+  replace (m1'.(mem_contents)#b0) with (m1.(mem_contents)#b0).
+  replace (m2'.(mem_contents)#b3) with (m2.(mem_contents)#b3).
+  apply mi_memval0; auto. eapply perm_drop_4; eauto. 
+  unfold drop_perm in DROP; destruct (range_perm_dec m2 b2 (lo + delta) (hi + delta) Cur Freeable); inv DROP; auto.
+  unfold drop_perm in H0; destruct (range_perm_dec m1 b1 lo hi Cur Freeable); inv H0; auto.
 Qed.
 
 Lemma drop_outside_inj: forall f m1 m2 b lo hi p m2',
   mem_inj f m1 m2 -> 
   drop_perm m2 b lo hi p = Some m2' -> 
-  (forall b' delta,
+  (forall b' delta ofs' k p,
     f b' = Some(b, delta) ->
-    high_bound m1 b' + delta <= lo 
-    \/ hi <= low_bound m1 b' + delta) ->
+    perm m1 b' ofs' k p -> 
+    lo <= ofs' + delta < hi -> False) ->
   mem_inj f m1 m2'.
-Proof. 
-  intros. destruct H. constructor; intros.
-
+Proof.
+  intros. inv H. 
+  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. eapply perm_drop_3; eauto. 
+    destruct (zeq b3 b); auto. subst b3. right. 
+    destruct (zlt (ofs + delta0) lo); auto.
+    destruct (zle hi (ofs + delta0)); auto.
+    byContradiction. exploit H1; eauto. omega.
+  constructor.
+  (* perm *)
+  auto.
   (* access *)
-  inversion H2.
-  destruct (range_perm_in_bounds _ _ _ _ _ H3). 
-    pose proof (size_chunk_pos chunk). omega.
-  pose proof (mi_access0 b1 b2 delta chunk ofs p0 H H2). clear mi_access0 H2 H3. 
-  unfold valid_access in *.  intuition. clear H3. 
-  unfold range_perm in *. intros. 
-  eapply perm_drop_3; eauto.  
-  destruct (eq_block b2 b); subst; try (intuition; fail).  
-    destruct (H1 b1 delta H); intuition omega. 
-
-  (* memval *)
-  pose proof (mi_memval0 _ _ _ _  H H2). clear mi_memval0. 
-  unfold Mem.drop_perm in H0. 
-  destruct (Mem.range_perm_dec m2 b lo hi p); inversion H0; subst; clear H0. 
-  simpl.  unfold update.  destruct (zeq b2 b); subst; auto. 
-    pose proof (perm_in_bounds _ _ _ _ H2). 
-    destruct (H1 b1 delta H). 
-       destruct (zle lo (ofs + delta)); simpl; auto. exfalso; omega. 
-       destruct (zle lo (ofs + delta)); destruct (zlt (ofs + delta) hi); simpl; auto. 
-           exfalso; omega. 
+  intros. exploit mi_access0; eauto. intros [A B]. split; auto.
+  red; intros.
+  replace ofs0 with ((ofs0 - delta) + delta) by omega.
+  eapply PERM; eauto. apply H2. omega.
+  (* contents *)
+  intros. 
+  replace (m2'.(mem_contents)#b2) with (m2.(mem_contents)#b2).
+  apply mi_memval0; auto.
+  unfold drop_perm in H0; destruct (range_perm_dec m2 b lo hi Cur Freeable); inv H0; auto.
 Qed.
 
-
 (** * Memory extensions *)
 
 (**  A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
@@ -2864,9 +2591,6 @@ Record extends' (m1 m2: mem) : Prop :=
   mk_extends {
     mext_next: nextblock m1 = nextblock m2;
     mext_inj:  mem_inj inject_id m1 m2
-(*
-    mext_bounds: forall b, low_bound m2 b <= low_bound m1 b /\ high_bound m1 b <= high_bound m2 b
-*)
   }.
 
 Definition extends := extends'.
@@ -2876,6 +2600,7 @@ Theorem extends_refl:
 Proof.
   intros. constructor. auto. constructor.
   intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto.
+  intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto.
   intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. 
   apply memval_lessdef_refl.
 Qed.
@@ -2936,30 +2661,19 @@ Proof.
   rewrite (nextblock_store _ _ _ _ _ _ H0).
   rewrite (nextblock_store _ _ _ _ _ _ A).
   auto.
-(*
-  intros.
-  rewrite (bounds_store _ _ _ _ _ _ H0).
-  rewrite (bounds_store _ _ _ _ _ _ A).
-  auto.
-*)
 Qed.
 
 Theorem store_outside_extends:
   forall chunk m1 m2 b ofs v m2',
   extends m1 m2 ->
   store chunk m2 b ofs v = Some m2' ->
-  ofs + size_chunk chunk <= low_bound m1 b \/ high_bound m1 b <= ofs ->
+  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + size_chunk chunk -> False) ->
   extends m1 m2'.
 Proof.
   intros. inversion H. constructor.
   rewrite (nextblock_store _ _ _ _ _ _ H0). auto.
   eapply store_outside_inj; eauto.
-  unfold inject_id; intros. inv H2.
-  exploit perm_in_bounds; eauto. omega.
-(* 
-  intros.
-  rewrite (bounds_store _ _ _ _ _ _ H0). auto.
-*)
+  unfold inject_id; intros. inv H2. eapply H1; eauto. omega. 
 Qed.
 
 Theorem storev_extends:
@@ -2997,30 +2711,19 @@ Proof.
   rewrite (nextblock_storebytes _ _ _ _ _ H0).
   rewrite (nextblock_storebytes _ _ _ _ _ A).
   auto.
-(*
-  intros.
-  rewrite (bounds_store _ _ _ _ _ _ H0).
-  rewrite (bounds_store _ _ _ _ _ _ A).
-  auto.
-*)
 Qed.
 
 Theorem storebytes_outside_extends:
   forall m1 m2 b ofs bytes2 m2',
   extends m1 m2 ->
   storebytes m2 b ofs bytes2 = Some m2' ->
-  ofs + Z_of_nat (length bytes2) <= low_bound m1 b \/ high_bound m1 b <= ofs ->
+  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) ->
   extends m1 m2'.
 Proof.
   intros. inversion H. constructor.
   rewrite (nextblock_storebytes _ _ _ _ _ H0). auto.
   eapply storebytes_outside_inj; eauto.
-  unfold inject_id; intros. inv H2.
-  exploit perm_in_bounds; eauto. omega.
-(* 
-  intros.
-  rewrite (bounds_store _ _ _ _ _ _ H0). auto.
-*)
+  unfold inject_id; intros. inv H2. eapply H1; eauto. omega. 
 Qed.
 
 Theorem alloc_extends:
@@ -3063,26 +2766,19 @@ Proof.
   intros. inv H. constructor.
   rewrite (nextblock_free _ _ _ _ _ H0). auto.
   eapply free_left_inj; eauto.
-(*
-  intros. rewrite (bounds_free _ _ _ _ _ H0). auto.
-*)
 Qed.
 
 Theorem free_right_extends:
   forall m1 m2 b lo hi m2',
   extends m1 m2 ->
   free m2 b lo hi = Some m2' ->
-  (forall ofs p, lo <= ofs < hi -> ~perm m1 b ofs p) ->
+  (forall ofs k p, perm m1 b ofs k p -> lo <= ofs < hi -> False) ->
   extends m1 m2'.
 Proof.
   intros. inv H. constructor.
   rewrite (nextblock_free _ _ _ _ _ H0). auto.
   eapply free_right_inj; eauto.
-  unfold inject_id; intros. inv H.
-  elim (H1 ofs p); auto. omega.
-(* 
-  intros. rewrite (bounds_free _ _ _ _ _ H0). auto.
-*)
+  unfold inject_id; intros. inv H. eapply H1; eauto. omega.
 Qed. 
 
 Theorem free_parallel_extends:
@@ -3105,15 +2801,8 @@ Proof.
   rewrite (nextblock_free _ _ _ _ _ FREE). auto.
   eapply free_right_inj with (m1 := m1'); eauto. 
   eapply free_left_inj; eauto. 
-  unfold inject_id; intros. inv H. 
-  assert (~perm m1' b ofs p). eapply perm_free_2; eauto. omega. 
-  contradiction.
-(*
-  intros.
-  rewrite (bounds_free _ _ _ _ _ H0).
-  rewrite (bounds_free _ _ _ _ _ FREE).
-  auto.
-*)
+  unfold inject_id; intros. inv H.
+  eapply perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. 
 Qed.
 
 Theorem valid_block_extends:
@@ -3125,8 +2814,8 @@ Proof.
 Qed.
 
 Theorem perm_extends:
-  forall m1 m2 b ofs p,
-  extends m1 m2 -> perm m1 b ofs p -> perm m2 b ofs p.
+  forall m1 m2 b ofs k p,
+  extends m1 m2 -> perm m1 b ofs k p -> perm m2 b ofs k p.
 Proof.
   intros. inv H. replace ofs with (ofs + 0) by omega. 
   eapply perm_inj; eauto. 
@@ -3149,15 +2838,6 @@ Proof.
   eapply valid_access_extends; eauto.
 Qed.
 
-(*
-Theorem bounds_extends:
-  forall m1 m2 b,
-  extends m1 m2 -> low_bound m2 b <= low_bound m1 b /\ high_bound m1 b <= high_bound m2 b.
-Proof.
-  intros. inv H. auto.
-Qed.
-*)
-
 (** * Memory injections *)
 
 (** A memory state [m1] injects into another memory state [m2] via the
@@ -3188,15 +2868,15 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop :=
       f b = Some(b', delta) ->
       0 <= delta <= Int.max_unsigned;
     mi_range_block:
-      forall b b' delta,
+      forall b b' delta ofs k p,
       f b = Some(b', delta) ->
-      delta = 0 \/ 
-      (0 <= low_bound m2 b' /\ high_bound m2 b' <= Int.max_unsigned)
+      perm m2 b' ofs k p ->
+      delta = 0 \/ 0 <= ofs <= Int.max_unsigned
   }.
 
 Definition inject := inject'.
 
-Hint Local Resolve mi_mappedblocks mi_range_offset: mem.
+Local Hint Resolve mi_mappedblocks mi_range_offset: mem.
 
 (** Preservation of access validity and pointer validity *)
 
@@ -3219,22 +2899,22 @@ Proof.
   intros. eapply mi_mappedblocks; eauto. 
 Qed.
 
-Hint Local Resolve valid_block_inject_1 valid_block_inject_2: mem.
+Local Hint Resolve valid_block_inject_1 valid_block_inject_2: mem.
 
 Theorem perm_inject:
-  forall f m1 m2 b1 b2 delta ofs p,
+  forall f m1 m2 b1 b2 delta ofs k p,
   f b1 = Some(b2, delta) ->
   inject f m1 m2 ->
-  perm m1 b1 ofs p -> perm m2 b2 (ofs + delta) p.
+  perm m1 b1 ofs k p -> perm m2 b2 (ofs + delta) k p.
 Proof.
   intros. inv H0. eapply perm_inj; eauto. 
 Qed.
 
 Theorem range_perm_inject:
-  forall f m1 m2 b1 b2 delta lo hi p,
+  forall f m1 m2 b1 b2 delta lo hi k p,
   f b1 = Some(b2, delta) ->
   inject f m1 m2 ->
-  range_perm m1 b1 lo hi p -> range_perm m2 b2 (lo + delta) (hi + delta) p.
+  range_perm m1 b1 lo hi k p -> range_perm m2 b2 (lo + delta) (hi + delta) k p.
 Proof.
   intros. inv H0. eapply range_perm_inj; eauto.
 Qed.
@@ -3268,19 +2948,18 @@ Qed.
 Lemma address_inject:
   forall f m1 m2 b1 ofs1 b2 delta,
   inject f m1 m2 ->
-  perm m1 b1 (Int.unsigned ofs1) Nonempty ->
+  perm m1 b1 (Int.unsigned ofs1) Max Nonempty ->
   f b1 = Some (b2, delta) ->
   Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 Proof.
   intros.
   exploit perm_inject; eauto. intro A.
-  exploit perm_in_bounds. eexact A. intros [B C]. 
-  exploit mi_range_block; eauto. intros [D | [E F]].
+  exploit mi_range_block; eauto. intros [D | E].
   subst delta. rewrite Int.add_zero. omega.
   unfold Int.add.
   repeat rewrite Int.unsigned_repr. auto.
   eapply mi_range_offset; eauto.
-  omega. 
+  auto.
   eapply mi_range_offset; eauto.
 Qed.
 
@@ -3292,7 +2971,7 @@ Lemma address_inject':
   Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 Proof.
   intros. destruct H0. eapply address_inject; eauto. 
-  apply H0. generalize (size_chunk_pos chunk). omega. 
+  apply perm_cur_max. apply H0. generalize (size_chunk_pos chunk). omega. 
 Qed.
 
 Theorem valid_pointer_inject_no_overflow:
@@ -3330,11 +3009,11 @@ Theorem inject_no_overlap:
   b1 <> b2 ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
-  perm m1 b1 ofs1 Nonempty ->
-  perm m1 b2 ofs2 Nonempty ->
+  perm m1 b1 ofs1 Max Nonempty ->
+  perm m1 b2 ofs2 Max Nonempty ->
   b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2.
 Proof.
-  intros. inv H. eapply meminj_no_overlap_perm; eauto.
+  intros. inv H. eapply mi_no_overlap0; eauto.
 Qed.
 
 Theorem different_pointers_inject:
@@ -3355,19 +3034,20 @@ Proof.
   rewrite (address_inject' _ _ _ _ _ _ _ _ H H1 H3). 
   rewrite (address_inject' _ _ _ _ _ _ _ _ H H2 H4). 
   inv H1. simpl in H5. inv H2. simpl in H1.
-  eapply meminj_no_overlap_perm. 
-  eapply mi_no_overlap; eauto. eauto. eauto. eauto. 
-  apply (H5 (Int.unsigned ofs1)). omega.
-  apply (H1 (Int.unsigned ofs2)). omega.
+  eapply mi_no_overlap; eauto.
+  apply perm_cur_max. apply (H5 (Int.unsigned ofs1)). omega.
+  apply perm_cur_max. apply (H1 (Int.unsigned ofs2)). omega.
 Qed.
 
+Require Intv.
+
 Theorem disjoint_or_equal_inject:
   forall f m m' b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 sz,
   inject f m m' ->
   f b1 = Some(b1', delta1) ->
   f b2 = Some(b2', delta2) ->
-  range_perm m b1 ofs1 (ofs1 + sz) Nonempty ->
-  range_perm m b2 ofs2 (ofs2 + sz) Nonempty ->
+  range_perm m b1 ofs1 (ofs1 + sz) Max Nonempty ->
+  range_perm m b2 ofs2 (ofs2 + sz) Max Nonempty ->
   sz > 0 ->
   b1 <> b2 \/ ofs1 = ofs2 \/ ofs1 + sz <= ofs2 \/ ofs2 + sz <= ofs1 ->
   b1' <> b2' \/ ofs1 + delta1 = ofs2 + delta2
@@ -3375,12 +3055,19 @@ Theorem disjoint_or_equal_inject:
              \/ ofs2 + delta2 + sz <= ofs1 + delta1.
 Proof.
   intros. 
-  exploit range_perm_in_bounds. eexact H2. omega. intros [LO1 HI1].
-  exploit range_perm_in_bounds. eexact H3. omega. intros [LO2 HI2].
   destruct (eq_block b1 b2).
   assert (b1' = b2') by congruence. assert (delta1 = delta2) by congruence. subst.
   destruct H5. congruence. right. destruct H5. left; congruence. right. omega.
-  exploit mi_no_overlap; eauto. intros [P | P]. auto. right. omega.
+  destruct (eq_block b1' b2'); auto. subst. right. right. 
+  set (i1 := (ofs1 + delta1, ofs1 + delta1 + sz)).
+  set (i2 := (ofs2 + delta2, ofs2 + delta2 + sz)).
+  change (snd i1 <= fst i2 \/ snd i2 <= fst i1).
+  apply Intv.range_disjoint'; simpl; try omega.
+  unfold Intv.disjoint, Intv.In; simpl; intros. red; intros. 
+  exploit mi_no_overlap; eauto. 
+  instantiate (1 := x - delta1). apply H2. omega.
+  instantiate (1 := x - delta2). apply H3. omega.
+  unfold block; omega. 
 Qed.
 
 Theorem aligned_area_inject:
@@ -3388,7 +3075,7 @@ Theorem aligned_area_inject:
   inject f m m' ->
   al = 1 \/ al = 2 \/ al = 4 -> sz > 0 ->
   (al | sz) ->
-  range_perm m b ofs (ofs + sz) Nonempty ->
+  range_perm m b ofs (ofs + sz) Cur Nonempty ->
   (al | ofs) ->
   f b = Some(b', delta) ->
   (al | ofs + delta).
@@ -3468,13 +3155,11 @@ Proof.
 (* mappedblocks *)
   eauto with mem.
 (* no overlap *)
-  red; intros.
-  repeat rewrite (bounds_store _ _ _ _ _ _ H0).
-  eauto. 
+  red; intros. eauto with mem.
 (* range offset *)
   eauto.
 (* range blocks *)
-  intros. rewrite (bounds_store _ _ _ _ _ _ STORE). eauto.
+  eauto with mem. 
 Qed.
 
 Theorem store_unmapped_inject:
@@ -3493,9 +3178,7 @@ Proof.
 (* mappedblocks *)
   eauto with mem.
 (* no overlap *)
-  red; intros. 
-  repeat rewrite (bounds_store _ _ _ _ _ _ H0).
-  eauto. 
+  red; intros. eauto with mem.
 (* range offset *)
   eauto.
 (* range blocks *)
@@ -3505,18 +3188,16 @@ Qed.
 Theorem store_outside_inject:
   forall f m1 m2 chunk b ofs v m2',
   inject f m1 m2 ->
-  (forall b' delta,
+  (forall b' delta ofs',
     f b' = Some(b, delta) ->
-    high_bound m1 b' + delta <= ofs
-    \/ ofs + size_chunk chunk <= low_bound m1 b' + delta) ->
+    perm m1 b' ofs' Cur Readable ->
+    ofs <= ofs' + delta < ofs + size_chunk chunk -> False) ->
   store chunk m2 b ofs v = Some m2' ->
   inject f m1 m2'.
 Proof.
   intros. inversion H. constructor.
 (* inj *)
   eapply store_outside_inj; eauto.
-  intros. exploit perm_in_bounds; eauto. intro. 
-  exploit H0; eauto. intro. omega. 
 (* freeblocks *)
   auto.
 (* mappedblocks *)
@@ -3525,8 +3206,8 @@ Proof.
   auto.
 (* range offset *)
   auto.
-(* rang blocks *)
-  intros. rewrite (bounds_store _ _ _ _ _ _ H1). eauto.
+(* range blocks *)
+  intros. eauto with mem. 
 Qed.
 
 Theorem storev_mapped_inject:
@@ -3566,13 +3247,11 @@ Proof.
 (* mappedblocks *)
   intros. eapply storebytes_valid_block_1; eauto. 
 (* no overlap *)
-  red; intros.
-  repeat rewrite (bounds_storebytes _ _ _ _ _ H0).
-  eauto. 
+  red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. 
 (* range offset *)
   eauto.
 (* range blocks *)
-  intros. rewrite (bounds_storebytes _ _ _ _ _ STORE). eauto.
+  intros. eapply mi_range_block0; eauto. eapply perm_storebytes_2; eauto. 
 Qed.
 
 Theorem storebytes_unmapped_inject:
@@ -3591,30 +3270,26 @@ Proof.
 (* mappedblocks *)
   eauto with mem.
 (* no overlap *)
-  red; intros. 
-  repeat rewrite (bounds_storebytes _ _ _ _ _ H0).
-  eauto. 
+  red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. 
 (* range offset *)
   eauto.
 (* range blocks *)
-  auto.
+  eauto.
 Qed.
 
 Theorem storebytes_outside_inject:
   forall f m1 m2 b ofs bytes2 m2',
   inject f m1 m2 ->
-  (forall b' delta,
+  (forall b' delta ofs',
     f b' = Some(b, delta) ->
-    high_bound m1 b' + delta <= ofs
-    \/ ofs + Z_of_nat (length bytes2) <= low_bound m1 b' + delta) ->
+    perm m1 b' ofs' Cur Readable ->
+    ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) ->
   storebytes m2 b ofs bytes2 = Some m2' ->
   inject f m1 m2'.
 Proof.
   intros. inversion H. constructor.
 (* inj *)
   eapply storebytes_outside_inj; eauto.
-  intros. exploit perm_in_bounds; eauto. intro. 
-  exploit H0; eauto. omega. 
 (* freeblocks *)
   auto.
 (* mappedblocks *)
@@ -3624,7 +3299,7 @@ Proof.
 (* range offset *)
   auto.
 (* range blocks *)
-  intros. rewrite (bounds_storebytes _ _ _ _ _ H1). eauto.
+  intros. eapply mi_range_block0; eauto. eapply perm_storebytes_2; eauto. 
 Qed.
 
 (* Preservation of allocations *)
@@ -3648,7 +3323,7 @@ Proof.
 (* range offset *)
   auto.
 (* range block *)
-  intros. rewrite (bounds_alloc_other _ _ _ _ _ H0). eauto. 
+  intros. exploit perm_alloc_inv; eauto. rewrite zeq_false. eauto. 
   eapply valid_not_valid_diff; eauto with mem.
 Qed.
 
@@ -3663,39 +3338,43 @@ Theorem alloc_left_unmapped_inject:
   /\ (forall b, b <> b1 -> f' b = f b).
 Proof.
   intros. inversion H.
-  assert (inject_incr f (update b1 None f)).
-    red; unfold update; intros. destruct (zeq b b1). subst b.
+  set (f' := fun b => if zeq b b1 then None else f b).
+  assert (inject_incr f f').
+    red; unfold f'; intros. destruct (zeq b b1). subst b.
     assert (f b1 = None). eauto with mem. congruence.
     auto.
-  assert (mem_inj (update b1 None f) m1 m2).
+  assert (mem_inj f' m1 m2).
     inversion mi_inj0; constructor; eauto with mem.
-    unfold update; intros. destruct (zeq b0 b1). congruence. eauto. 
-    unfold update; intros. destruct (zeq b0 b1). congruence. 
+    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. 
     apply memval_inject_incr with f; auto. 
-  exists (update b1 None f); split. constructor.
+  exists f'; split. constructor.
 (* inj *)
-  eapply alloc_left_unmapped_inj; eauto. apply update_s. 
+  eapply alloc_left_unmapped_inj; eauto. unfold f'; apply zeq_true. 
 (* freeblocks *)
-  intros. unfold update. destruct (zeq b b1). auto. 
+  intros. unfold f'. destruct (zeq b b1). auto. 
   apply mi_freeblocks0. red; intro; elim H3. eauto with mem. 
 (* mappedblocks *)
-  unfold update; intros. destruct (zeq b b1). congruence. eauto. 
+  unfold f'; intros. destruct (zeq b b1). congruence. eauto. 
 (* no overlap *)
-  unfold update; red; intros.
+  unfold f'; red; intros.
   destruct (zeq b0 b1); destruct (zeq b2 b1); try congruence.
-  repeat rewrite (bounds_alloc_other _ _ _ _ _ H0); eauto.
+  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. 
 (* range offset *)
-  unfold update; intros.
+  unfold f'; intros.
   destruct (zeq b b1). congruence. eauto.
 (* range block *)
-  unfold update; intros.
+  unfold f'; intros.
   destruct (zeq b b1). congruence. eauto.
 (* incr *)
   split. auto. 
 (* image *)
-  split. apply update_s.
+  split. unfold f'; apply zeq_true. 
 (* incr *)
-  intros; apply update_o; auto.
+  intros; unfold f'; apply zeq_false; auto.
 Qed.
 
 Theorem alloc_left_mapped_inject:
@@ -3704,13 +3383,13 @@ Theorem alloc_left_mapped_inject:
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
   0 <= delta <= Int.max_unsigned ->
-  delta = 0 \/ 0 <= low_bound m2 b2 /\ high_bound m2 b2 <= Int.max_unsigned ->
-  (forall ofs p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) p) ->
+  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) ->
+  (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   inj_offset_aligned delta (hi-lo) ->
-  (forall b ofs, 
-   f b = Some (b2, ofs) -> 
-   high_bound m1 b + ofs <= lo + delta \/
-   hi + delta <= low_bound m1 b + ofs) ->
+  (forall b delta' ofs k p,
+   f b = Some (b2, delta') -> 
+   perm m1 b ofs k p ->
+   lo + delta <= ofs + delta' < hi + delta -> False) ->
   exists f',
      inject f' m1' m2
   /\ inject_incr f f'
@@ -3718,48 +3397,57 @@ Theorem alloc_left_mapped_inject:
   /\ (forall b, b <> b1 -> f' b = f b).
 Proof.
   intros. inversion H.
-  assert (inject_incr f (update b1 (Some(b2, delta)) f)).
-    red; unfold update; intros. destruct (zeq b b1). subst b.
+  set (f' := fun b => if zeq b b1 then Some(b2, delta) else f b).
+  assert (inject_incr f f').
+    red; unfold f'; intros. destruct (zeq b b1). subst b.
     assert (f b1 = None). eauto with mem. congruence.
     auto.
-  assert (mem_inj (update b1 (Some(b2, delta)) f) m1 m2).
+  assert (mem_inj f' m1 m2).
     inversion mi_inj0; constructor; eauto with mem.
-    unfold update; intros. destruct (zeq b0 b1).
-      inv H8. elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem.
+    unfold f'; intros. destruct (zeq b0 b1).
+      inversion H8. subst b0 b3 delta0. 
+      elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem.
+      eauto.
+    unfold f'; intros. destruct (zeq b0 b1).
+      inversion H8. subst b0 b3 delta0. 
+      elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem.
       eauto.
-    unfold update; intros. destruct (zeq b0 b1).
-      inv H8. elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. 
+    unfold f'; intros. destruct (zeq b0 b1).
+      inversion H8. subst b0 b3 delta0. 
+      elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem.
       apply memval_inject_incr with f; auto. 
-  exists (update b1 (Some(b2, delta)) f). split. constructor.
+  exists f'. split. constructor.
 (* inj *)
-  eapply alloc_left_mapped_inj; eauto. apply update_s.
+  eapply alloc_left_mapped_inj; eauto. unfold f'; apply zeq_true. 
 (* freeblocks *)
-  unfold update; intros. destruct (zeq b b1). subst b. 
+  unfold f'; intros. destruct (zeq b b1). subst b. 
   elim H9. eauto with mem.
   eauto with mem.
 (* mappedblocks *)
-  unfold update; intros. destruct (zeq b b1). inv H9. auto.
-  eauto.
+  unfold f'; intros. destruct (zeq b b1). congruence. eauto.
 (* overlap *)
-  unfold update; red; intros.
-  repeat rewrite (bounds_alloc _ _ _ _ _ H0). unfold eq_block. 
-  destruct (zeq b0 b1); destruct (zeq b3 b1); simpl.
-  inv H10; inv H11. congruence.
-  inv H10. destruct (zeq b1' b2'); auto. subst b2'. 
-  right. generalize (H6 _ _ H11). tauto. 
-  inv H11. destruct (zeq b1' b2'); auto. subst b2'. 
-  right. eapply H6; eauto. 
+  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).
+  congruence.
+  inversion H10; subst b0 b1' delta1. 
+    destruct (zeq 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.
+    eapply H6; eauto. omega.
   eauto.
 (* range offset *)
-  unfold update; intros. destruct (zeq b b1). inv H9. auto. eauto.
+  unfold f'; intros. destruct (zeq b b1). congruence. eauto. 
 (* range block *)
-  unfold update; intros. destruct (zeq b b1). inv H9. auto. eauto.
+  unfold f'; intros. destruct (zeq b b1). inversion H9; subst b b' delta0. eauto. eauto. 
 (* incr *)
   split. auto.
 (* image of b1 *)
-  split. apply update_s.
+  split. unfold f'; apply zeq_true. 
 (* image of others *)
-  intros. apply update_o; auto.
+  intros. unfold f'; apply zeq_false; auto. 
 Qed.
 
 Theorem alloc_parallel_inject:
@@ -3782,11 +3470,10 @@ Proof.
   instantiate (1 := b2). eauto with mem.
   instantiate (1 := 0). unfold Int.max_unsigned. generalize Int.modulus_pos; omega.
   auto.
-  intros.
-  apply perm_implies with Freeable; auto with mem.
+  intros. apply perm_implies with Freeable; auto with mem.
   eapply perm_alloc_2; eauto. omega.
   red; intros. apply Zdivide_0.
-  intros. elimtype False. apply (valid_not_valid_diff m2 b2 b2); eauto with mem.
+  intros. apply (valid_not_valid_diff m2 b2 b2); eauto with mem.
   intros [f' [A [B [C D]]]].
   exists f'; exists m2'; exists b2; auto.
 Qed.
@@ -3807,7 +3494,7 @@ Proof.
 (* mappedblocks *)
   auto.
 (* no overlap *)
-  red; intros. repeat rewrite (bounds_free _ _ _ _ _ H0). eauto. 
+  red; intros. eauto with mem. 
 (* range offset *)
   auto.
 (* range block *)
@@ -3831,8 +3518,8 @@ Lemma free_right_inject:
   forall f m1 m2 b lo hi m2',
   inject f m1 m2 ->
   free m2 b lo hi = Some m2' ->
-  (forall b1 delta ofs p,
-    f b1 = Some(b, delta) -> perm m1 b1 ofs p ->
+  (forall b1 delta ofs k p,
+    f b1 = Some(b, delta) -> perm m1 b1 ofs k p ->
     lo <= ofs + delta < hi -> False) ->
   inject f m1 m2'.
 Proof.
@@ -3848,14 +3535,14 @@ Proof.
 (* range offset *)
   auto.
 (* range blocks *)
-  intros. rewrite (bounds_free _ _ _ _ _ H0). eauto.
+  intros. eauto with mem. 
 Qed.
 
 Lemma perm_free_list:
-  forall l m m' b ofs p,
+  forall l m m' b ofs k p,
   free_list m l = Some m' ->
-  perm m' b ofs p ->
-  perm m b ofs p /\ 
+  perm m' b ofs k p ->
+  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.
@@ -3865,7 +3552,7 @@ Proof.
   exploit IHl; eauto. intros [A B].
   split. eauto with mem.
   intros. destruct H2. inv H2.
-  elim (perm_free_2 _ _ _ _ _ H ofs p). auto. auto.
+  elim (perm_free_2 _ _ _ _ _ H ofs k p). auto. auto.
   eauto.
 Qed.
 
@@ -3874,9 +3561,9 @@ Theorem free_inject:
   inject f m1 m2 ->
   free_list m1 l = Some m1' ->
   free m2 b lo hi = Some m2' ->
-  (forall b1 delta ofs p,
+  (forall b1 delta ofs k p,
     f b1 = Some(b, delta) -> 
-    perm m1 b1 ofs p -> lo <= ofs + delta < hi ->
+    perm m1 b1 ofs k p -> lo <= ofs + delta < hi ->
     exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) ->
   inject f m1' m2'.
 Proof.
@@ -3887,37 +3574,18 @@ Proof.
   exploit H2; eauto. intros [lo1 [hi1 [C D]]]. eauto.
 Qed.
 
-(*
-Theorem free_inject':
-  forall f m1 l m1' m2 b lo hi m2',
-  inject f m1 m2 ->
-  free_list m1 l = Some m1' ->
-  free m2 b lo hi = Some m2' ->
-  (forall b1 delta,
-    f b1 = Some(b, delta) -> In (b1, low_bound m1 b1, high_bound m1 b1) l) ->
-  inject f m1' m2'.
-Proof.
-  intros. eapply free_inject; eauto.
-  intros. exists (low_bound m1 b1); exists (high_bound m1 b1).
-  split. eauto. apply perm_in_bounds with p. auto.
-Qed.
-*)
-
 Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2',
   inject f m1 m2 -> 
   drop_perm m2 b lo hi p = Some m2' -> 
-  (forall b' delta,
+  (forall b' delta ofs k p,
     f b' = Some(b, delta) ->
-    high_bound m1 b' + delta <= lo 
-    \/ hi <= low_bound m1 b' + delta) ->
+    perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) ->
   inject f m1 m2'.
 Proof.
   intros. destruct H. constructor; eauto.
   eapply drop_outside_inj; eauto.
-
-  intros.  unfold valid_block in *. erewrite nextblock_drop; eauto. 
-
-  intros.  erewrite bounds_drop; eauto. 
+  intros. unfold valid_block in *. erewrite nextblock_drop; eauto. 
+  intros. eapply mi_range_block0; eauto. eapply perm_drop_4; eauto. 
 Qed.
 
 (** Injecting a memory into itself. *)
@@ -3964,11 +3632,14 @@ Theorem empty_inject_neutral:
   forall thr, inject_neutral thr empty.
 Proof.
   intros; red; constructor.
+(* perm *)
+  unfold flat_inj; intros. destruct (zlt b1 thr); inv H.
+  replace (ofs + 0) with ofs by omega; auto.
 (* access *)
   unfold flat_inj; intros. destruct (zlt b1 thr); inv H.
   replace (ofs + 0) with ofs by omega; auto.
 (* mem_contents *)
-  intros; simpl; constructor.
+  intros; simpl. repeat rewrite ZMap.gi. constructor.
 Qed.
 
 Theorem alloc_inject_neutral:
@@ -4026,8 +3697,12 @@ Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes
 Hint Resolve
   Mem.valid_not_valid_diff
   Mem.perm_implies
+  Mem.perm_cur
+  Mem.perm_max
   Mem.perm_valid_block
   Mem.range_perm_implies
+  Mem.range_perm_cur
+  Mem.range_perm_max
   Mem.valid_access_implies
   Mem.valid_access_valid_block
   Mem.valid_access_perm
@@ -4059,6 +3734,7 @@ Hint Resolve
   Mem.perm_alloc_1
   Mem.perm_alloc_2
   Mem.perm_alloc_3
+  Mem.perm_alloc_4
   Mem.perm_alloc_inv
   Mem.valid_access_alloc_other
   Mem.valid_access_alloc_same
diff --git a/common/Memtype.v b/common/Memtype.v
index 2e44331..a13e861 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -32,7 +32,8 @@ Require Import Memdata.
 
 (** Memory states are accessed by addresses [b, ofs]: pairs of a block
   identifier [b] and a byte offset [ofs] within that block.
-  Each address is in one of the following five states:
+  Each address is associated to permissions, also known as access rights.
+  The following permissions are expressible:
 - Freeable (exclusive access): all operations permitted
 - Writable: load, store and pointer comparison operations are permitted,
   but freeing is not.
@@ -67,6 +68,21 @@ Proof.
   intros. inv H; inv H0; constructor.
 Qed.
 
+(** Each address has not one, but two permissions associated
+  with it.  The first is the current permission.  It governs whether
+  operations (load, store, free, etc) over this address succeed or
+  not.  The other is the maximal permission.  It is always at least as
+  strong as the current permission.  Once a block is allocated, the
+  maximal permission of an address within this block can only
+  decrease, as a result of [free] or [drop_perm] operations, or of
+  external calls.  In contrast, the current permission of an address
+  can be temporarily lowered by an external call, then raised again by
+  another external call. *)
+
+Inductive perm_kind: Type :=
+  | Max: perm_kind
+  | Cur: perm_kind.
+
 Module Type MEM.
 
 (** The abstract type of memory states. *)
@@ -143,8 +159,8 @@ Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem :=
   end.
 
 (** [drop_perm m b lo hi p] sets the permissions of the byte range
-    [(b, lo) ... (b, hi - 1)] to [p].  These bytes must have permissions
-    at least [p] in the initial memory state [m].
+    [(b, lo) ... (b, hi - 1)] to [p].  These bytes must have [Freeable] permissions
+    in the initial memory state [m].
     Returns updated memory state, or [None] if insufficient permissions. *)
 
 Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), option mem.
@@ -168,41 +184,52 @@ Definition valid_block (m: mem) (b: block) :=
 Axiom valid_not_valid_diff:
   forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
 
-(** [perm m b ofs p] holds if the address [b, ofs] in memory state [m]
-  has permission [p]: one of writable, readable, and nonempty.
-  If the address is empty, [perm m b ofs p] is false for all values of [p]. *)
-Parameter perm: forall (m: mem) (b: block) (ofs: Z) (p: permission), Prop.
+(** [perm m b ofs k p] holds if the address [b, ofs] in memory state [m]
+  has permission [p]: one of freeable, writable, readable, and nonempty.
+  If the address is empty, [perm m b ofs p] is false for all values of [p].
+  [k] is the kind of permission we are interested in: either the current
+  permissions or the maximal permissions. *)
+Parameter perm: forall (m: mem) (b: block) (ofs: Z) (k: perm_kind) (p: permission), Prop.
 
 (** Logical implications between permissions *)
 
 Axiom perm_implies:
-  forall m b ofs p1 p2, perm m b ofs p1 -> perm_order p1 p2 -> perm m b ofs p2.
+  forall m b ofs k p1 p2, perm m b ofs k p1 -> perm_order p1 p2 -> perm m b ofs k p2.
+
+(** The current permission is always less than or equal to the maximal permission. *)
+
+Axiom perm_cur_max:
+  forall m b ofs p, perm m b ofs Cur p -> perm m b ofs Max p.
+Axiom perm_cur:
+  forall m b ofs k p, perm m b ofs Cur p -> perm m b ofs k p.
+Axiom perm_max:
+  forall m b ofs k p, perm m b ofs k p -> perm m b ofs Max p.
 
 (** Having a (nonempty) permission implies that the block is valid.
   In other words, invalid blocks, not yet allocated, are all empty. *)
 Axiom perm_valid_block:
-  forall m b ofs p, perm m b ofs p -> valid_block m b.
+  forall m b ofs k p, perm m b ofs k p -> valid_block m b.
 
 (* Unused?
 (** The [Mem.perm] predicate is decidable. *)
 Axiom perm_dec:
-  forall m b ofs p, {perm m b ofs p} + {~ perm m b ofs p}.
+  forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}.
 *)
 
 (** [range_perm m b lo hi p] holds iff the addresses [b, lo] to [b, hi-1]
-  all have permission [p]. *)
-Definition range_perm (m: mem) (b: block) (lo hi: Z) (p: permission) : Prop :=
-  forall ofs, lo <= ofs < hi -> perm m b ofs p.
+  all have permission [p] of kind [k]. *)
+Definition range_perm (m: mem) (b: block) (lo hi: Z) (k: perm_kind) (p: permission) : Prop :=
+  forall ofs, lo <= ofs < hi -> perm m b ofs k p.
 
 Axiom range_perm_implies:
-  forall m b lo hi p1 p2,
-  range_perm m b lo hi p1 -> perm_order p1 p2 -> range_perm m b lo hi p2.
+  forall m b lo hi k p1 p2,
+  range_perm m b lo hi k p1 -> perm_order p1 p2 -> range_perm m b lo hi k p2.
 
 (** An access to a memory quantity [chunk] at address [b, ofs] with
   permission [p] is valid in [m] if the accessed addresses all have
-  permission [p] and moreover the offset is properly aligned. *)
+  current permission [p] and moreover the offset is properly aligned. *)
 Definition valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) (p: permission): Prop :=
-  range_perm m b ofs (ofs + size_chunk chunk) p
+  range_perm m b ofs (ofs + size_chunk chunk) Cur p
   /\ (align_chunk chunk | ofs).
 
 Axiom valid_access_implies:
@@ -216,9 +243,9 @@ Axiom valid_access_valid_block:
   valid_block m b.
 
 Axiom valid_access_perm:
-  forall m chunk b ofs p,
+  forall m chunk b ofs k p,
   valid_access m chunk b ofs p ->
-  perm m b ofs p.
+  perm m b ofs k p.
 
 (** [valid_pointer m b ofs] returns [true] if the address [b, ofs]
   is nonempty in [m] and [false] if it is empty. *)
@@ -227,41 +254,17 @@ Parameter valid_pointer: forall (m: mem) (b: block) (ofs: Z), bool.
 
 Axiom valid_pointer_nonempty_perm:
   forall m b ofs,
-  valid_pointer m b ofs = true <-> perm m b ofs Nonempty.
+  valid_pointer m b ofs = true <-> perm m b ofs Cur Nonempty.
 Axiom valid_pointer_valid_access:
   forall m b ofs,
   valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs Nonempty.
 
-(** Each block has associated low and high bounds.  These are the bounds 
-    that were given when the block was allocated.  *)
-
-Parameter bounds: forall (m: mem) (b: block), Z*Z.
-
-Notation low_bound m b := (fst(bounds m b)).
-Notation high_bound m b := (snd(bounds m b)).
-
-(** The crucial properties of bounds is that any offset below the low
-    bound or above the high bound is empty. *)
-
-Axiom perm_in_bounds:
-  forall m b ofs p, perm m b ofs p -> low_bound m b <= ofs < high_bound m b.
-
-Axiom range_perm_in_bounds:
-  forall m b lo hi p, 
-  range_perm m b lo hi p -> lo < hi ->
-  low_bound m b <= lo /\ hi <= high_bound m b.
-
-Axiom valid_access_in_bounds:
-  forall m chunk b ofs p,
-  valid_access m chunk b ofs p ->
-  low_bound m b <= ofs /\ ofs + size_chunk chunk <= high_bound m b.
-
 (** * Properties of the memory operations *)
 
 (** ** Properties of the initial memory state. *)
 
 Axiom nextblock_empty: nextblock empty = 1.
-Axiom perm_empty: forall b ofs p, ~perm empty b ofs p.
+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.
 
@@ -315,12 +318,12 @@ Axiom load_int16_signed_unsigned:
 
 Axiom range_perm_loadbytes:
   forall m b ofs len,
-  range_perm m b ofs (ofs + len) Readable ->
+  range_perm m b ofs (ofs + len) Cur Readable ->
   exists bytes, loadbytes m b ofs len = Some bytes.
 Axiom loadbytes_range_perm:
   forall m b ofs len bytes,
   loadbytes m b ofs len = Some bytes ->
-  range_perm m b ofs (ofs + len) Readable.
+  range_perm m b ofs (ofs + len) Cur Readable.
 
 (** If [loadbytes] succeeds, the corresponding [load] succeeds and
   returns a value that is determined by the
@@ -384,10 +387,10 @@ Axiom store_valid_block_2:
 
 Axiom perm_store_1:
   forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 ->
-  forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p.
+  forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.
 Axiom perm_store_2:
   forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 ->
-  forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p.
+  forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p.
 
 Axiom valid_access_store:
   forall m1 chunk b ofs v,
@@ -405,10 +408,6 @@ Axiom store_valid_access_3:
   forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 ->
   valid_access m1 chunk b ofs Writable.
 
-Axiom bounds_store:
-  forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 ->
-  forall b', bounds m2 b' = bounds m1 b'.
-
 (** Load-store properties. *)
 
 Axiom load_store_similar:
@@ -502,17 +501,17 @@ Axiom store_float32_truncate:
 
 Axiom range_perm_storebytes:
   forall m1 b ofs bytes,
-  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable ->
+  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable ->
   { m2 : mem | storebytes m1 b ofs bytes = Some m2 }.
 Axiom storebytes_range_perm:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
-  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable.
+  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable.
 Axiom perm_storebytes_1:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
-  forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p.
+  forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.
 Axiom perm_storebytes_2:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
-  forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p.
+  forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p.
 Axiom storebytes_valid_access_1:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
   forall chunk' b' ofs' p,
@@ -530,9 +529,6 @@ Axiom storebytes_valid_block_1:
 Axiom storebytes_valid_block_2:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
   forall b', valid_block m2 b' -> valid_block m1 b'.
-Axiom bounds_storebytes:
-  forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
-  forall b', bounds m2 b' = bounds m1 b'.
 
 (** Connections between [store] and [storebytes]. *)
 
@@ -581,8 +577,6 @@ Axiom storebytes_split:
   exists m1,
      storebytes m b ofs bytes1 = Some m1
   /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2.
-Axiom storebytes_empty:
-  forall m b ofs, storebytes m b ofs nil = Some m.
 
 (** ** Properties of [alloc]. *)
 
@@ -616,18 +610,21 @@ Axiom valid_block_alloc_inv:
 
 Axiom perm_alloc_1:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  forall b' ofs p, perm m1 b' ofs p -> perm m2 b' ofs p.
+  forall b' ofs k p, perm m1 b' ofs k p -> perm m2 b' ofs k p.
 Axiom perm_alloc_2:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  forall ofs, lo <= ofs < hi -> perm m2 b ofs Freeable.
+  forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable.
 Axiom perm_alloc_3:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  forall ofs p, ofs < lo \/ hi <= ofs -> ~perm m2 b ofs p.
+  forall ofs k p, perm m2 b ofs k p -> lo <= ofs < hi.
+Axiom perm_alloc_4:
+  forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
+  forall b' ofs k p, perm m2 b' ofs k p -> b' <> b -> perm m1 b' ofs k p.
 Axiom perm_alloc_inv:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  forall b' ofs p, 
-  perm m2 b' ofs p ->
-  if zeq b' b then lo <= ofs < hi else perm m1 b' ofs p.
+  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.
 
 (** Effect of [alloc] on access validity. *)
 
@@ -649,20 +646,6 @@ Axiom valid_access_alloc_inv:
   then lo <= ofs /\ ofs + size_chunk chunk <= hi /\ (align_chunk chunk | ofs)
   else valid_access m1 chunk b' ofs p.
 
-(** Effect of [alloc] on bounds. *)
-
-Axiom bounds_alloc:
-  forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  forall b', bounds m2 b' = if eq_block b' b then (lo, hi) else bounds m1 b'.
-
-Axiom bounds_alloc_same:
-  forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  bounds m2 b = (lo, hi).
-
-Axiom bounds_alloc_other:
-  forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  forall b', b' <> b -> bounds m2 b' = bounds m1 b'.
-
 (** Load-alloc properties. *)
 
 Axiom load_alloc_unchanged:
@@ -689,15 +672,15 @@ Axiom load_alloc_same':
 (** ** Properties of [free]. *)
 
 (** [free] succeeds if and only if the correspond range of addresses
-  has [Freeable] permission. *)
+  has [Freeable] current permission. *)
 
 Axiom range_perm_free:
   forall m1 b lo hi,
-  range_perm m1 b lo hi Freeable ->
+  range_perm m1 b lo hi Cur Freeable ->
   { m2: mem | free m1 b lo hi = Some m2 }.
 Axiom free_range_perm:
   forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 ->
-  range_perm m1 bf lo hi Freeable.
+  range_perm m1 bf lo hi Cur Freeable.
 
 (** Block validity is preserved by [free]. *)
 
@@ -715,17 +698,17 @@ Axiom valid_block_free_2:
 
 Axiom perm_free_1:
   forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 ->
-  forall b ofs p,
+  forall b ofs k p,
   b <> bf \/ ofs < lo \/ hi <= ofs ->
-  perm m1 b ofs p ->
-  perm m2 b ofs p.
+  perm m1 b ofs k p ->
+  perm m2 b ofs k p.
 Axiom perm_free_2:
   forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 ->
-  forall ofs p, lo <= ofs < hi -> ~ perm m2 bf ofs p.
+  forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p.
 Axiom perm_free_3:
   forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 ->
-  forall b ofs p,
-  perm m2 b ofs p -> perm m1 b ofs p.
+  forall b ofs k p,
+  perm m2 b ofs k p -> perm m1 b ofs k p.
 
 (** Effect of [free] on access validity. *)
 
@@ -751,12 +734,6 @@ Axiom valid_access_free_inv_2:
   valid_access m2 chunk bf ofs p ->
   lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs.
 
-(** [free] preserves bounds. *)
-
-Axiom bounds_free:
-  forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 ->
-  forall b, bounds m2 b = bounds m1 b.
-
 (** Load-free properties *)
 
 Axiom load_free:
@@ -770,30 +747,32 @@ Axiom load_free:
 Axiom nextblock_drop:
   forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
   nextblock m' = nextblock m.
+Axiom drop_perm_valid_block_1:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  forall b', valid_block m b' -> valid_block m' b'.
+Axiom drop_perm_valid_block_2:
+  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
+  forall b', valid_block m' b' -> valid_block m b'.
 
 Axiom range_perm_drop_1:
   forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
-  range_perm m b lo hi p.
+  range_perm m b lo hi Cur Freeable.
 Axiom range_perm_drop_2:
   forall m b lo hi p,
-  range_perm m b lo hi p -> { m' | drop_perm m b lo hi p = Some m' }.
+  range_perm m b lo hi Cur Freeable -> { m' | drop_perm m b lo hi p = Some m' }.
 
 Axiom perm_drop_1:
   forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
-  forall ofs, lo <= ofs < hi -> perm m' b ofs p.
+  forall ofs k, lo <= ofs < hi -> perm m' b ofs k p.
 Axiom perm_drop_2:
   forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
-  forall ofs p', lo <= ofs < hi -> perm m' b ofs p' -> perm_order p p'.
+  forall ofs k p', lo <= ofs < hi -> perm m' b ofs k p' -> perm_order p p'.
 Axiom perm_drop_3:
   forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
-  forall b' ofs p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs p' -> perm m' b' ofs p'.
+  forall b' ofs k p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs k p' -> perm m' b' ofs k p'.
 Axiom perm_drop_4:
   forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
-  forall b' ofs p', perm m' b' ofs p' -> perm m b' ofs p'.
-
-Axiom bounds_drop:
-  forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
-  forall b', bounds m' b' = bounds m b'.
+  forall b' ofs k p', perm m' b' ofs k p' -> perm m b' ofs k p'.
 
 Axiom load_drop:
   forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
@@ -848,7 +827,7 @@ Axiom store_outside_extends:
   forall chunk m1 m2 b ofs v m2',
   extends m1 m2 ->
   store chunk m2 b ofs v = Some m2' ->
-  ofs + size_chunk chunk <= low_bound m1 b \/ high_bound m1 b <= ofs ->
+  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + size_chunk chunk -> False) ->
   extends m1 m2'.
 
 Axiom storev_extends:
@@ -874,7 +853,7 @@ Axiom storebytes_outside_extends:
   forall m1 m2 b ofs bytes2 m2',
   extends m1 m2 ->
   storebytes m2 b ofs bytes2 = Some m2' ->
-  ofs + Z_of_nat (length bytes2) <= low_bound m1 b \/ high_bound m1 b <= ofs ->
+  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) ->
   extends m1 m2'.
 
 Axiom alloc_extends:
@@ -896,7 +875,7 @@ Axiom free_right_extends:
   forall m1 m2 b lo hi m2',
   extends m1 m2 ->
   free m2 b lo hi = Some m2' ->
-  (forall ofs p, lo <= ofs < hi -> ~perm m1 b ofs p) ->
+  (forall ofs k p, perm m1 b ofs k p -> lo <= ofs < hi -> False) ->
   extends m1 m2'.
 
 Axiom free_parallel_extends:
@@ -912,8 +891,8 @@ Axiom valid_block_extends:
   extends m1 m2 ->
   (valid_block m1 b <-> valid_block m2 b).
 Axiom perm_extends:
-  forall m1 m2 b ofs p,
-  extends m1 m2 -> perm m1 b ofs p -> perm m2 b ofs p.
+  forall m1 m2 b ofs k p,
+  extends m1 m2 -> perm m1 b ofs k p -> perm m2 b ofs k p.
 Axiom valid_access_extends:
   forall m1 m2 chunk b ofs p,
   extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p.
@@ -952,10 +931,10 @@ Axiom valid_block_inject_2:
   valid_block m2 b2.
 
 Axiom perm_inject:
-  forall f m1 m2 b1 b2 delta ofs p,
+  forall f m1 m2 b1 b2 delta ofs k p,
   f b1 = Some(b2, delta) ->
   inject f m1 m2 ->
-  perm m1 b1 ofs p -> perm m2 b2 (ofs + delta) p.
+  perm m1 b1 ofs k p -> perm m2 b2 (ofs + delta) k p.
 
 Axiom valid_access_inject:
   forall f m1 m2 chunk b1 ofs b2 delta p,
@@ -974,7 +953,7 @@ Axiom valid_pointer_inject:
 Axiom address_inject:
   forall f m1 m2 b1 ofs1 b2 delta,
   inject f m1 m2 ->
-  perm m1 b1 (Int.unsigned ofs1) Nonempty ->
+  perm m1 b1 (Int.unsigned ofs1) Max Nonempty ->
   f b1 = Some (b2, delta) ->
   Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
 
@@ -998,8 +977,8 @@ Axiom inject_no_overlap:
   b1 <> b2 ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
-  perm m1 b1 ofs1 Nonempty ->
-  perm m1 b2 ofs2 Nonempty ->
+  perm m1 b1 ofs1 Max Nonempty ->
+  perm m1 b2 ofs2 Max Nonempty ->
   b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2.
 
 Axiom different_pointers_inject:
@@ -1056,10 +1035,10 @@ Axiom store_unmapped_inject:
 Axiom store_outside_inject:
   forall f m1 m2 chunk b ofs v m2',
   inject f m1 m2 ->
-  (forall b' delta,
+  (forall b' delta ofs',
     f b' = Some(b, delta) ->
-    high_bound m1 b' + delta <= ofs
-    \/ ofs + size_chunk chunk <= low_bound m1 b' + delta) ->
+    perm m1 b' ofs' Cur Readable ->
+    ofs <= ofs' + delta < ofs + size_chunk chunk -> False) ->
   store chunk m2 b ofs v = Some m2' ->
   inject f m1 m2'.
 
@@ -1092,10 +1071,10 @@ Axiom storebytes_unmapped_inject:
 Axiom storebytes_outside_inject:
   forall f m1 m2 b ofs bytes2 m2',
   inject f m1 m2 ->
-  (forall b' delta,
+  (forall b' delta ofs',
     f b' = Some(b, delta) ->
-    high_bound m1 b' + delta <= ofs
-    \/ ofs + Z_of_nat (length bytes2) <= low_bound m1 b' + delta) ->
+    perm m1 b' ofs' Cur Readable ->
+    ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) ->
   storebytes m2 b ofs bytes2 = Some m2' ->
   inject f m1 m2'.
 
@@ -1124,13 +1103,13 @@ Axiom alloc_left_mapped_inject:
   alloc m1 lo hi = (m1', b1) ->
   valid_block m2 b2 ->
   0 <= delta <= Int.max_unsigned ->
-  delta = 0 \/ 0 <= low_bound m2 b2 /\ high_bound m2 b2 <= Int.max_unsigned ->
-  (forall ofs p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) p) ->
+  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) ->
+  (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   inj_offset_aligned delta (hi-lo) ->
-  (forall b ofs, 
-   f b = Some (b2, ofs) -> 
-   high_bound m1 b + ofs <= lo + delta \/
-   hi + delta <= low_bound m1 b + ofs) ->
+  (forall b delta' ofs k p,
+   f b = Some (b2, delta') -> 
+   perm m1 b ofs k p ->
+   lo + delta <= ofs + delta' < hi + delta -> False) ->
   exists f',
      inject f' m1' m2
   /\ inject_incr f f'
@@ -1154,8 +1133,8 @@ Axiom free_inject:
   inject f m1 m2 ->
   free_list m1 l = Some m1' ->
   free m2 b lo hi = Some m2' ->
-  (forall b1 delta ofs p,
-    f b1 = Some(b, delta) -> perm m1 b1 ofs p -> lo <= ofs + delta < hi ->
+  (forall b1 delta ofs k p,
+    f b1 = Some(b, delta) -> perm m1 b1 ofs k p -> lo <= ofs + delta < hi ->
     exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) ->
   inject f m1' m2'.
 
@@ -1163,10 +1142,9 @@ Axiom drop_outside_inject:
   forall f m1 m2 b lo hi p m2',
   inject f m1 m2 -> 
   drop_perm m2 b lo hi p = Some m2' -> 
-  (forall b' delta,
+  (forall b' delta ofs k p,
     f b' = Some(b, delta) ->
-    high_bound m1 b' + delta <= lo 
-    \/ hi <= low_bound m1 b' + delta) ->
+    perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) ->
   inject f m1 m2'.
 
 (** Memory states that inject into themselves. *)