Merge of the "princeton" branch:

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


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

9 files changed, 312 insertions, 244 deletions

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 2df8b93..d6b99ed 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -204,7 +204,7 @@ Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> P
 
 Record match_env (f: meminj) (cenv: compilenv)
                  (e: Csharpminor.env) (sp: block)
-                 (lo hi: Z) : Prop :=
+                 (lo hi: block) : Prop :=
   mk_match_env {
 
 (** C#minor local variables match sub-blocks of the Cminor stack data block. *)
@@ -213,12 +213,12 @@ Record match_env (f: meminj) (cenv: compilenv)
 
 (** [lo, hi] is a proper interval. *)
     me_low_high:
-      lo <= hi;
+      Ple lo hi;
 
 (** Every block appearing in the C#minor environment [e] must be
   in the range [lo, hi]. *)
     me_bounded:
-      forall id b sz, PTree.get id e = Some(b, sz) -> lo <= b < hi;
+      forall id b sz, PTree.get id e = Some(b, sz) -> Ple lo b /\ Plt b hi;
 
 (** All blocks mapped to sub-blocks of the Cminor stack data must be
     images of variables from the C#minor environment [e] *)
@@ -232,7 +232,7 @@ Record match_env (f: meminj) (cenv: compilenv)
   (i.e. allocated before the stack data for the current Cminor function). *)
     me_incr:
       forall b tb delta,
-      f b = Some(tb, delta) -> b < lo -> tb < sp
+      f b = Some(tb, delta) -> Plt b lo -> Plt tb sp
   }.
 
 Ltac geninv x := 
@@ -243,7 +243,7 @@ Lemma match_env_invariant:
   match_env f1 cenv e sp lo hi ->
   inject_incr f1 f2 ->
   (forall b delta, f2 b = Some(sp, delta) -> f1 b = Some(sp, delta)) ->
-  (forall b, b < lo -> f2 b = f1 b) ->
+  (forall b, Plt b lo -> f2 b = f1 b) ->
   match_env f2 cenv e sp lo hi.
 Proof.
   intros. destruct H. constructor; auto.
@@ -285,12 +285,12 @@ Lemma match_env_external_call:
   match_env f1 cenv e sp lo hi ->
   inject_incr f1 f2 ->
   inject_separated f1 f2 m1 m1' ->
-  hi <= Mem.nextblock m1 -> sp < Mem.nextblock m1' ->
+  Ple hi (Mem.nextblock m1) -> Plt sp (Mem.nextblock m1') ->
   match_env f2 cenv e sp lo hi.
 Proof.
   intros. apply match_env_invariant with f1; auto.
   intros. eapply inject_incr_separated_same'; eauto.
-  intros. eapply inject_incr_separated_same; eauto. red. destruct H. omega. 
+  intros. eapply inject_incr_separated_same; eauto. red. destruct H. xomega. 
 Qed.
 
 (** [match_env] and allocations *)
@@ -320,18 +320,18 @@ Proof.
   constructor; eauto.
   constructor.
 (* low-high *)
-  rewrite NEXTBLOCK; omega.
+  rewrite NEXTBLOCK; xomega.
 (* bounded *)
   intros. rewrite PTree.gsspec in H. destruct (peq id0 id).
-  inv H. rewrite NEXTBLOCK; omega.
-  exploit me_bounded0; eauto. rewrite NEXTBLOCK; omega.
+  inv H. rewrite NEXTBLOCK; xomega.
+  exploit me_bounded0; eauto. rewrite NEXTBLOCK; xomega.
 (* inv *)
-  intros. destruct (zeq b (Mem.nextblock m1)).
+  intros. destruct (eq_block b (Mem.nextblock m1)).
   subst b. rewrite SAME in H; inv H. exists id; exists sz. apply PTree.gss. 
   rewrite OTHER in H; auto. exploit me_inv0; eauto. 
   intros [id1 [sz1 EQ]]. exists id1; exists sz1. rewrite PTree.gso; auto. congruence.
 (* incr *)
-  intros. rewrite OTHER in H. eauto. unfold block in *; omega.
+  intros. rewrite OTHER in H. eauto. unfold block in *; xomega.
 Qed.
 
 (** The sizes of blocks appearing in [e] are respected. *)
@@ -371,7 +371,7 @@ Lemma padding_freeable_invariant:
   padding_freeable f1 e tm1 sp sz ->
   match_env f1 cenv e sp lo hi ->
   (forall ofs, Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
-  (forall b, b < hi -> f2 b = f1 b) ->
+  (forall b, Plt b hi -> f2 b = f1 b) ->
   padding_freeable f2 e tm2 sp sz.
 Proof.
   intros; red; intros.
@@ -424,14 +424,13 @@ Qed.
 (** Global environments match if the memory injection [f] leaves unchanged
   the references to global symbols and functions. *)
 
-Inductive match_globalenvs (f: meminj) (bound: Z): Prop :=
+Inductive match_globalenvs (f: meminj) (bound: block): Prop :=
   | mk_match_globalenvs
-      (POS: bound > 0)
-      (DOMAIN: forall b, b < bound -> f b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+      (DOMAIN: forall b, Plt b bound -> f b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).
 
 Remark inj_preserves_globals:
   forall f hi,
@@ -459,7 +458,7 @@ Inductive frame : Type :=
        (le: Csharpminor.temp_env)
        (te: Cminor.env)
        (sp: block)
-       (lo hi: Z).
+       (lo hi: block).
 
 Definition callstack : Type := list frame.
 
@@ -473,16 +472,16 @@ Definition callstack : Type := list frame.
 *)
 
 Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
-                          callstack -> Z -> Z -> Prop :=
+                          callstack -> block -> block -> Prop :=
   | mcs_nil:
       forall hi bound tbound,
       match_globalenvs f hi ->
-      hi <= bound -> hi <= tbound ->
+      Ple hi bound -> Ple hi tbound ->
       match_callstack f m tm nil bound tbound 
   | mcs_cons:
       forall cenv tf e le te sp lo hi cs bound tbound
-        (BOUND: hi <= bound)
-        (TBOUND: sp < tbound)
+        (BOUND: Ple hi bound)
+        (TBOUND: Plt sp tbound)
         (MTMP: match_temps f le te)
         (MENV: match_env f cenv e sp lo hi)
         (BOUND: match_bounds e m)
@@ -506,44 +505,44 @@ Lemma match_callstack_invariant:
   forall f1 m1 tm1 f2 m2 tm2 cs bound tbound,
   match_callstack f1 m1 tm1 cs bound tbound ->
   inject_incr f1 f2 ->
-  (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  (forall sp ofs, sp < tbound -> Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
-  (forall b, b < bound -> f2 b = f1 b) ->
-  (forall b b' delta, f2 b = Some(b', delta) -> b' < tbound -> f1 b = Some(b', delta)) ->
+  (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
+  (forall sp ofs, Plt sp tbound -> Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
+  (forall b, Plt b bound -> f2 b = f1 b) ->
+  (forall b b' delta, f2 b = Some(b', delta) -> Plt b' tbound -> f1 b = Some(b', delta)) ->
   match_callstack f2 m2 tm2 cs bound tbound.
 Proof.
   induction 1; intros.
   (* base case *)
   econstructor; eauto.
   inv H. constructor; intros; eauto.
-  eapply IMAGE; eauto. eapply H6; eauto. omega.
+  eapply IMAGE; eauto. eapply H6; eauto. xomega.
   (* inductive case *)
-  assert (lo <= hi) by (eapply me_low_high; eauto).
+  assert (Ple lo hi) by (eapply me_low_high; eauto).
   econstructor; eauto.
   eapply match_temps_invariant; eauto.
   eapply match_env_invariant; eauto. 
-    intros. apply H3. omega.
+    intros. apply H3. xomega.
   eapply match_bounds_invariant; eauto.
     intros. eapply H1; eauto. 
-    exploit me_bounded; eauto. omega. 
+    exploit me_bounded; eauto. xomega. 
   eapply padding_freeable_invariant; eauto. 
-    intros. apply H3. omega. 
+    intros. apply H3. xomega. 
   eapply IHmatch_callstack; eauto. 
-    intros. eapply H1; eauto. omega. 
-    intros. eapply H2; eauto. omega. 
-    intros. eapply H3; eauto. omega.
-    intros. eapply H4; eauto. omega.
+    intros. eapply H1; eauto. xomega. 
+    intros. eapply H2; eauto. xomega. 
+    intros. eapply H3; eauto. xomega.
+    intros. eapply H4; eauto. xomega.
 Qed.
 
 Lemma match_callstack_incr_bound:
   forall f m tm cs bound tbound bound' tbound',
   match_callstack f m tm cs bound tbound ->
-  bound <= bound' -> tbound <= tbound' ->
+  Ple bound bound' -> Ple tbound tbound' ->
   match_callstack f m tm cs bound' tbound'.
 Proof.
   intros. inv H.
-  econstructor; eauto. omega. omega. 
-  constructor; auto. omega. omega.
+  econstructor; eauto. xomega. xomega. 
+  constructor; auto. xomega. xomega.
 Qed.
 
 (** Assigning a temporary variable. *)
@@ -610,7 +609,7 @@ Proof.
   apply match_callstack_incr_bound with lo sp; try omega.
   apply match_callstack_invariant with f m tm; auto.
   intros. eapply perm_freelist; eauto.
-  intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega.
+  intros. eapply Mem.perm_free_1; eauto. left; unfold block; xomega. xomega. xomega.
   eapply Mem.free_inject; eauto.
   intros. exploit me_inv0; eauto. intros [id [sz A]]. 
   exists 0; exists sz; split.
@@ -622,52 +621,52 @@ Qed.
 
 Lemma match_callstack_external_call:
   forall f1 f2 m1 m2 m1' m2',
-  mem_unchanged_on (loc_unmapped f1) m1 m2 ->
-  mem_unchanged_on (loc_out_of_reach f1 m1) m1' m2' ->
+  Mem.unchanged_on (loc_unmapped f1) m1 m2 ->
+  Mem.unchanged_on (loc_out_of_reach f1 m1) m1' m2' ->
   inject_incr f1 f2 ->
   inject_separated f1 f2 m1 m1' ->
   (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
   forall cs bound tbound,
   match_callstack f1 m1 m1' cs bound tbound ->
-  bound <= Mem.nextblock m1 -> tbound <= Mem.nextblock m1' ->
+  Ple bound (Mem.nextblock m1) -> Ple tbound (Mem.nextblock m1') ->
   match_callstack f2 m2 m2' cs bound tbound.
 Proof.
   intros until m2'. 
   intros UNMAPPED OUTOFREACH INCR SEPARATED MAXPERMS.
-  destruct OUTOFREACH as [OUTOFREACH1 OUTOFREACH2].
   induction 1; intros.
 (* base case *)
   apply mcs_nil with hi; auto.
   inv H. constructor; auto.
   intros. case_eq (f1 b1). 
   intros [b2' delta'] EQ. rewrite (INCR _ _ _ EQ) in H. inv H. eauto. 
-  intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. omega. 
+  intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega. 
 (* inductive case *)
   constructor. auto. auto. 
   eapply match_temps_invariant; eauto.
   eapply match_env_invariant; eauto. 
   red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|] eqn:?. 
   exploit INCR; eauto. congruence.
-  exploit SEPARATED; eauto. intros [A B]. elim B. red. omega. 
-  intros. assert (lo <= hi) by (eapply me_low_high; eauto).
+  exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega. 
+  intros. assert (Ple lo hi) by (eapply me_low_high; eauto).
   destruct (f1 b) as [[b' delta']|] eqn:?. 
   apply INCR; auto. 
   destruct (f2 b) as [[b' delta']|] eqn:?; auto.
-  exploit SEPARATED; eauto. intros [A B]. elim A. red. omega.
+  exploit SEPARATED; eauto. intros [A B]. elim A. red. xomega.
   eapply match_bounds_invariant; eauto. 
-  intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. omega. 
+  intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. xomega. 
   (* padding-freeable *)
   red; intros.
   destruct (is_reachable_from_env_dec f1 e sp ofs).
   inv H3. right. apply is_reachable_intro with id b sz delta; auto. 
   exploit PERM; eauto. intros [A|A]; try contradiction.
-  left. apply OUTOFREACH1; auto. red; intros.
-  red; intros; elim H3.
+  left. eapply Mem.perm_unchanged_on; eauto.
+  red; intros; red; intros. elim H3.
   exploit me_inv; eauto. intros [id [lv B]].
   exploit BOUND0; eauto. intros C.
   apply is_reachable_intro with id b0 lv delta; auto; omega.
+  eauto with mem.
   (* induction *)
-  eapply IHmatch_callstack; eauto. inv MENV; omega. omega.
+  eapply IHmatch_callstack; eauto. inv MENV; xomega. xomega.
 Qed.
 
 (** [match_callstack] and allocations *)
@@ -687,12 +686,12 @@ Proof.
   exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK.
   exploit Mem.alloc_result; eauto. intros RES.
   constructor.
-  omega.
-  unfold block in *; omega.
+  xomega.
+  unfold block in *; xomega.
   auto.
   constructor; intros.
     rewrite H3. rewrite PTree.gempty. constructor.
-    omega.
+    xomega.
     rewrite PTree.gempty in H4; discriminate.
     eelim Mem.fresh_block_alloc; eauto. eapply Mem.valid_block_inject_2; eauto.
     rewrite RES. change (Mem.valid_block tm tb). eapply Mem.valid_block_inject_2; eauto. 
@@ -721,25 +720,25 @@ Proof.
   intros. inv H. 
   exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK.
   exploit Mem.alloc_result; eauto. intros RES.
-  assert (LO: lo <= Mem.nextblock m1) by (eapply me_low_high; eauto). 
+  assert (LO: Ple lo (Mem.nextblock m1)) by (eapply me_low_high; eauto). 
   constructor.
-  omega.
+  xomega.
   auto.
   eapply match_temps_invariant; eauto.
   eapply match_env_alloc; eauto.
   red; intros. rewrite PTree.gsspec in H. destruct (peq id0 id).
   inversion H. subst b0 sz0 id0. eapply Mem.perm_alloc_3; eauto.
   eapply BOUND0; eauto. eapply Mem.perm_alloc_4; eauto. 
-  exploit me_bounded; eauto. unfold block in *; omega.
+  exploit me_bounded; eauto. unfold block in *; xomega.
   red; intros. exploit PERM; eauto. intros [A|A]. auto. right. 
   inv A. apply is_reachable_intro with id0 b0 sz0 delta; auto.
   rewrite PTree.gso. auto. congruence.
   eapply match_callstack_invariant with (m1 := m1); eauto. 
   intros. eapply Mem.perm_alloc_4; eauto.
-  unfold block in *; omega.
-  intros. apply H4. unfold block in *; omega.
-  intros. destruct (zeq b0 b). 
-  subst b0. rewrite H3 in H. inv H. omegaContradiction. 
+  unfold block in *; xomega.
+  intros. apply H4. unfold block in *; xomega.
+  intros. destruct (eq_block b0 b). 
+  subst b0. rewrite H3 in H. inv H. xomegaContradiction. 
   rewrite H4 in H; auto.
 Qed.
 
@@ -841,7 +840,7 @@ Proof.
   exploit (IHalloc_variables f2); eauto.
     red; intros. eapply COMPAT. auto with coqlib.
     red; intros. eapply SEP1; eauto with coqlib.
-    red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b b1); intros P.
+    red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b b1); intros P.
     subst b. rewrite C in H5; inv H5. 
     exploit SEP1. eapply in_eq. eapply in_cons; eauto. eauto. eauto. 
     red; intros; subst id0. elim H3. change id with (fst (id, sz0)). apply in_map; auto. 
@@ -1553,9 +1552,9 @@ Proof.
     repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
   inv H; inv H0; inv H1; TrivialExists.
     apply Int.sub_add_l.
-    simpl. destruct (zeq b1 b0); auto.
+    simpl. destruct (eq_block b1 b0); auto.
     subst b1. rewrite H in H0; inv H0. 
-    rewrite zeq_true. rewrite Int.sub_shifted. auto.
+    rewrite dec_eq_true. rewrite Int.sub_shifted. auto.
   inv H; inv H0; inv H1; TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
     destruct (Int.eq i0 Int.zero
@@ -2575,7 +2574,7 @@ Proof.
     apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
     eapply match_callstack_external_call; eauto.
     intros. eapply external_call_max_perm; eauto.
-    omega. omega. 
+    xomega. xomega. 
     eapply external_call_nextblock; eauto.
     eapply external_call_nextblock; eauto.
   econstructor; eauto.
@@ -2725,7 +2724,7 @@ Opaque PTree.set.
   apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_callstack_external_call; eauto.
   intros. eapply external_call_max_perm; eauto.
-  omega. omega.
+  xomega. xomega.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
@@ -2743,10 +2742,9 @@ Lemma match_globalenvs_init:
   match_globalenvs (Mem.flat_inj (Mem.nextblock m)) (Mem.nextblock m).
 Proof.
   intros. constructor.
-  apply Mem.nextblock_pos.
-  intros. unfold Mem.flat_inj. apply zlt_true; auto. 
+  intros. unfold Mem.flat_inj. apply pred_dec_true; auto. 
   intros. unfold Mem.flat_inj in H0. 
-  destruct (zlt b1 (Mem.nextblock m)); congruence.
+  destruct (plt b1 (Mem.nextblock m)); congruence.
   intros. eapply Genv.find_symbol_not_fresh; eauto.
   intros. eapply Genv.find_funct_ptr_not_fresh; eauto.
   intros. eapply Genv.find_var_info_not_fresh; eauto. 
@@ -2770,7 +2768,7 @@ Proof.
   eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z).
   auto.
   eapply Genv.initmem_inject; eauto.
-  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. omega. omega.
+  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. xomega. xomega.
   constructor. red; auto.
   constructor. 
 Qed.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index e7ffc89..4932bad 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -604,7 +604,7 @@ Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   | sub_case_pp ty =>          (**r pointer minus pointer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vptr b2 ofs2 =>
-          if zeq b1 b2 then
+          if eq_block b1 b2 then
             if Int.eq (Int.repr (sizeof ty)) Int.zero then None
             else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty))))
           else None
@@ -1059,8 +1059,8 @@ Proof.
   + inv H0; inv H1; inv H. TrivialInject.
     econstructor. eauto. rewrite Int.sub_add_l. auto.
   + inv H0; inv H1; inv H. TrivialInject.
-    destruct (zeq b1 b0); try discriminate. subst b1. 
-    rewrite H0 in H2; inv H2. rewrite zeq_true. 
+    destruct (eq_block b1 b0); try discriminate. subst b1. 
+    rewrite H0 in H2; inv H2. rewrite dec_eq_true. 
     destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3.
     rewrite Int.sub_shifted. TrivialInject.
   + inv H0; inv H1; inv H. TrivialInject.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 953e690..11f8011 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -437,8 +437,8 @@ Proof.
   destruct (classify_sub tya tyb); inv MAKE.
 - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - destruct va; try discriminate; destruct vb; inv SEM.
-  destruct (zeq b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0.
-  econstructor; eauto with cshm. rewrite zeq_true. simpl. rewrite E; auto. 
+  destruct (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0.
+  econstructor; eauto with cshm. rewrite dec_eq_true. simpl. rewrite E; auto. 
 - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index cb2f132..e7debfc 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -30,7 +30,7 @@ Open Scope error_monad_scope.
 (** To evaluate constant expressions at compile-time, we use the same [value]
   type and the same [sem_*] functions that are used in CompCert C's semantics
   (module [Csem]).  However, we interpret pointer values symbolically:
-  [Vptr (Zpos id) ofs] represents the address of global variable [id]
+  [Vptr id ofs] represents the address of global variable [id]
   plus byte offset [ofs]. *)
 
 (** [constval a] evaluates the constant expression [a].
@@ -111,7 +111,7 @@ Fixpoint constval (a: expr) : res val :=
   | Ecomma r1 r2 ty =>
       do v1 <- constval r1; constval r2
   | Evar x ty =>
-      OK(Vptr (Zpos x) Int.zero)
+      OK(Vptr x Int.zero)
   | Ederef r ty =>
       constval r
   | Efield l f ty =>
@@ -155,9 +155,9 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   | Vlong n, Tlong _ _ => OK(Init_int64 n)
   | Vfloat f, Tfloat F32 _ => OK(Init_float32 f)
   | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
-  | Vptr (Zpos id) ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
-  | Vptr (Zpos id) ofs, Tpointer _ _ => OK(Init_addrof id ofs)
-  | Vptr (Zpos id) ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs)
+  | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
+  | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs)
+  | Vptr id ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs)
   | Vundef, _ => Error(msg "undefined operation in initializer")
   | _, _ => Error (msg "type mismatch in initializer")
   end.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 2f29514..f3de05c 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -334,17 +334,13 @@ Qed.
 (** * Soundness of the compile-time evaluator *)
 
 (** A global environment [ge] induces a memory injection mapping
-  our symbolic pointers [Vptr (Zpos id) ofs] to run-time pointers
+  our symbolic pointers [Vptr id ofs] to run-time pointers
   [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *)
 
 Definition inj (b: block) :=
-  match b with
-  | Zpos id =>
-      match Genv.find_symbol ge id with
-      | Some b' => Some (b', 0)
-      | None => None
-      end
-  | _ => None
+  match Genv.find_symbol ge b with
+  | Some b' => Some (b', 0)
+  | None => None
   end.
 
 Lemma mem_empty_not_valid_pointer:
@@ -512,11 +508,11 @@ Proof.
   destruct ty; try discriminate. 
   destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
   (* pointer *)
-  unfold inj in H. destruct b1; try discriminate.
-  assert (data = Init_addrof p ofs1 /\ chunk = Mint32).
+  unfold inj in H.
+  assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32).
     destruct ty; inv EQ2; inv H2.
     destruct i; inv H5. intuition congruence. auto.
-  destruct H4; subst. destruct (Genv.find_symbol ge p); inv H. 
+  destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H. 
   rewrite Int.add_zero in H3. auto.
   (* undef *)
   discriminate.
@@ -538,7 +534,6 @@ Proof.
   destruct ty; inv EQ2; reflexivity. 
   destruct ty; try discriminate.
   destruct f0; inv EQ2; reflexivity.
-  destruct b; try discriminate.
   destruct ty; try discriminate.
   destruct i0; inv EQ2; reflexivity.
   inv EQ2; reflexivity.
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 8e6bc9f..854d345 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -90,6 +90,14 @@ Definition gensym (ty: type): mon ident :=
         (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g))
         (Ple_succ (gen_next g)).
 
+Definition reset_trail: mon unit :=
+  fun (g: generator) =>
+    Res tt (mkgenerator (gen_next g) nil) (Ple_refl (gen_next g)).
+
+Definition get_trail: mon (list (ident * type)) :=
+  fun (g: generator) =>
+    Res (gen_trail g) g (Ple_refl (gen_next g)).
+
 (** Construct a sequence from a list of statements.  To facilitate the
    proof, the sequence is nested to the left and starts with a [Sskip]. *)
 
@@ -491,34 +499,43 @@ with transl_lblstmt (ls: Csyntax.labeled_statements) : mon labeled_statements :=
 
 (** Translation of a function *)
 
-Definition transl_function (f: Csyntax.function) : res function :=
-  match transl_stmt f.(Csyntax.fn_body) (initial_generator tt) with
-  | Err msg =>
-      Error msg
-  | Res tbody g i =>
-      OK (mkfunction
+Definition transl_function (f: Csyntax.function) : mon function :=
+  do x <- reset_trail;
+  do tbody <- transl_stmt f.(Csyntax.fn_body);
+  do temps <- get_trail;
+  ret (mkfunction
               f.(Csyntax.fn_return)
               f.(Csyntax.fn_params)
               f.(Csyntax.fn_vars)
-              g.(gen_trail)
-              tbody)
-  end.
+              temps
+              tbody).
 
-Local Open Scope error_monad_scope.
-
-Definition transl_fundef (fd: Csyntax.fundef) : res fundef :=
+Definition transl_fundef (fd: Csyntax.fundef) : mon fundef :=
   match fd with
   | Csyntax.Internal f =>
-      do tf <- transl_function f; OK (Internal tf)
+      do tf <- transl_function f; ret (Internal tf)
   | Csyntax.External ef targs tres =>
-      OK (External ef targs tres)
+      ret (External ef targs tres)
   end.
 
-Definition transl_program (p: Csyntax.program) : res program :=
-  transform_partial_program transl_fundef p.
-
-
-
-      
+Local Open Scope error_monad_scope.
 
+Fixpoint transl_globdefs
+    (l: list (ident * globdef Csyntax.fundef type))
+    (g: generator) : res (list (ident * globdef Clight.fundef type)) :=
+  match l with
+  | nil => OK nil
+  | (id, Gfun f) :: l' =>
+      match transl_fundef f g with
+      | Err msg =>
+          Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
+      | Res tf g' _ =>
+          do tl' <- transl_globdefs l' g'; OK ((id, Gfun tf) :: tl')
+      end
+  | (id, Gvar v) :: l' =>
+      do tl' <- transl_globdefs l' g; OK ((id, Gvar v) :: tl')
+  end.
 
+Definition transl_program (p: Csyntax.program) : res program :=
+  do gl' <- transl_globdefs p.(prog_defs) (initial_generator tt);
+  OK (mkprogram gl' p.(prog_main)).
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index a2b8e61..dfe1c8a 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -44,29 +44,44 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof
-  (Genv.find_symbol_transf_partial transl_fundef _ TRANSL).
+Proof.
+  intros. eapply Genv.find_symbol_match. eapply transl_program_spec; eauto. 
+  simpl. tauto.
+Qed.
 
 Lemma function_ptr_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
-  Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
-Proof
-  (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL).
+  Genv.find_funct_ptr tge b = Some tf /\ tr_fundef f tf.
+Proof.
+  intros. eapply Genv.find_funct_ptr_match.
+  eapply transl_program_spec; eauto.
+  assumption.
+Qed.
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   exists tf,
-  Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
-Proof
-  (Genv.find_funct_transf_partial transl_fundef _ TRANSL).
+  Genv.find_funct tge v = Some tf /\ tr_fundef f tf.
+Proof.
+  intros. eapply Genv.find_funct_match.
+  eapply transl_program_spec; eauto.
+  assumption.
+Qed.
 
 Lemma varinfo_preserved:
   forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof
-  (Genv.find_var_info_transf_partial transl_fundef _ TRANSL).
+Proof.
+  intros. destruct (Genv.find_var_info ge b) as [v|] eqn:V. 
+- exploit Genv.find_var_info_match. eapply transl_program_spec; eauto. eassumption. 
+  intros [tv [A B]]. inv B. assumption.
+- destruct (Genv.find_var_info tge b) as [v'|] eqn:V'; auto.
+  exploit Genv.find_var_info_rev_match. eapply transl_program_spec; eauto. eassumption. 
+  simpl. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); try tauto.
+  intros [v [A B]]. inv B. fold ge in A. congruence.
+Qed.
 
 Lemma block_is_volatile_preserved:
   forall b, block_is_volatile tge b = block_is_volatile ge b.
@@ -75,22 +90,19 @@ Proof.
 Qed.
 
 Lemma type_of_fundef_preserved:
-  forall f tf, transl_fundef f = OK tf ->
+  forall f tf, tr_fundef f tf ->
   type_of_fundef tf = Csyntax.type_of_fundef f.
 Proof.
-  intros. destruct f; monadInv H.
-  exploit transl_function_spec; eauto. intros [A [B [C D]]].
-  simpl. unfold type_of_function, Csyntax.type_of_function. congruence.
+  intros. inv H.
+  inv H0; simpl. unfold type_of_function, Csyntax.type_of_function. congruence.
   auto.
 Qed.
 
 Lemma function_return_preserved:
-  forall f tf, transl_function f = OK tf ->
+  forall f tf, tr_function f tf ->
   fn_return tf = Csyntax.fn_return f.
 Proof.
-  intros. unfold transl_function in H.
-  destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); inv H.
-  auto.
+  intros. inv H; auto. 
 Qed.
 
 Lemma type_of_global_preserved:
@@ -893,7 +905,7 @@ Inductive match_cont : Csem.cont -> cont -> Prop :=
       match_cont k tk ->
       match_cont (Csem.Kswitch2 k) (Kswitch tk)
   | match_Kcall: forall f e C ty k optid tf le sl tk a dest tmps,
-      transl_function f = Errors.OK tf ->
+      tr_function f tf ->
       leftcontext RV RV C ->
       (forall v m, tr_top tge e (set_opttemp optid v le) m dest (C (Csyntax.Eval v ty)) sl a tmps) ->
       match_cont_exp dest a k tk ->
@@ -961,19 +973,19 @@ Qed.
 
 Inductive match_states: Csem.state -> state -> Prop :=
   | match_exprstates: forall f r k e m tf sl tk le dest a tmps,
-      transl_function f = Errors.OK tf ->
+      tr_function f tf ->
       tr_top tge e le m dest r sl a tmps ->
       match_cont_exp dest a k tk ->
       match_states (Csem.ExprState f r k e m)
                    (State tf Sskip (Kseqlist sl tk) e le m)
   | match_regularstates: forall f s k e m tf ts tk le,
-      transl_function f = Errors.OK tf ->
+      tr_function f tf ->
       tr_stmt s ts ->
       match_cont k tk ->
       match_states (Csem.State f s k e m)
                    (State tf ts tk e le m)
   | match_callstates: forall fd args k m tfd tk,
-      transl_fundef fd = Errors.OK tfd ->
+      tr_fundef fd tfd ->
       match_cont k tk ->
       match_states (Csem.Callstate fd args k m)
                    (Callstate tfd args tk m)
@@ -2089,8 +2101,7 @@ Proof.
   inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst.
   econstructor; split.
   left. eapply plus_two. constructor. econstructor. eauto.
-  replace (fn_return tf) with (Csyntax.fn_return f). eauto.
-  exploit transl_function_spec; eauto. intuition congruence. 
+  erewrite function_return_preserved; eauto. 
   eauto. traceEq.
   constructor. apply match_cont_call; auto.
 (* skip return *)
@@ -2133,8 +2144,8 @@ Proof.
 
 (* goto *)
   inv H7.
-  exploit transl_function_spec; eauto. intros [A [B [C D]]].
-  exploit tr_find_label. eexact A. apply match_cont_call. eauto. 
+  inversion H6; subst. 
+  exploit tr_find_label. eauto. apply match_cont_call. eauto. 
   instantiate (1 := lbl). rewrite H. 
   intros [ts' [tk' [P [Q R]]]]. 
   econstructor; split. 
@@ -2142,18 +2153,17 @@ Proof.
   econstructor; eauto. 
 
 (* internal function *)
-  monadInv H7. 
-  exploit transl_function_spec; eauto. intros [A [B [C D]]].
+  inv H7. inversion H3; subst.
   econstructor; split.
   left; apply plus_one. eapply step_internal_function. econstructor.
-  rewrite C; rewrite D; auto.
-  rewrite C; rewrite D. eapply alloc_variables_preserved; eauto.
-  rewrite C. eapply bind_parameters_preserved; eauto.
+  rewrite H5; rewrite H6; auto.
+  rewrite H5; rewrite H6. eapply alloc_variables_preserved; eauto.
+  rewrite H5. eapply bind_parameters_preserved; eauto.
   eauto. 
   constructor; auto. 
 
 (* external function *)
-  monadInv H5. 
+  inv H5.
   econstructor; split.
   left; apply plus_one. econstructor; eauto.
   eapply external_call_symbols_preserved; eauto. 
@@ -2188,14 +2198,13 @@ Lemma transl_initial_states:
   exists S', Clight.initial_state tprog S' /\ match_states S S'.
 Proof.
   intros. inv H. 
+  exploit transl_program_spec; eauto. intros MP.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor.
-  apply (Genv.init_mem_transf_partial _ _ TRANSL). eauto. 
+  exploit Genv.init_mem_match; eauto.  
   simpl. fold tge. rewrite symbols_preserved.
-  replace (prog_main tprog) with (prog_main prog). eexact H1.
-  symmetry. unfold transl_program in TRANSL.
-  eapply transform_partial_program_main; eauto.
+  destruct MP as [A B]. rewrite B; eexact H1.
   eexact FIND.
   rewrite <- H3. apply type_of_fundef_preserved. auto.
   constructor. auto. constructor.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index d063c4e..a424261 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -1085,17 +1085,67 @@ Opaque transl_expression transl_expr_stmt.
   monadInv TR; constructor; eauto.
 Qed.
 
-Theorem transl_function_spec:
-  forall f tf,
-  transl_function f = OK tf ->
-  tr_stmt f.(Csyntax.fn_body) tf.(fn_body)
-  /\ fn_return tf = Csyntax.fn_return f
-  /\ fn_params tf = Csyntax.fn_params f
-  /\ fn_vars tf = Csyntax.fn_vars f.
+(** Relational presentation for the transformation of functions, fundefs, and variables. *)
+
+Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
+  | tr_function_intro: forall f tf,
+      tr_stmt f.(Csyntax.fn_body) tf.(fn_body) ->
+      fn_return tf = Csyntax.fn_return f ->
+      fn_params tf = Csyntax.fn_params f ->
+      fn_vars tf = Csyntax.fn_vars f ->
+      tr_function f tf.
+
+Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop :=
+  | tr_internal: forall f tf,
+      tr_function f tf ->
+      tr_fundef (Csyntax.Internal f) (Clight.Internal tf)
+  | tr_external: forall ef targs tres,
+      tr_fundef (Csyntax.External ef targs tres) (External ef targs tres).
+
+Lemma transl_function_spec:
+  forall f tf g g' i,
+  transl_function f g = Res tf g' i ->
+  tr_function f tf.
 Proof.
-  intros until tf. unfold transl_function.
-  case_eq (transl_stmt (Csyntax.fn_body f) (initial_generator tt)); intros; inv H0.
-  simpl. intuition. eapply transl_stmt_meets_spec; eauto.
+  unfold transl_function; intros. monadInv H.
+  constructor; auto. simpl. eapply transl_stmt_meets_spec; eauto. 
+Qed.
+
+Lemma transl_fundef_spec:
+  forall fd tfd g g' i,
+  transl_fundef fd g = Res tfd g' i ->
+  tr_fundef fd tfd.
+Proof.
+  unfold transl_fundef; intros.
+  destruct fd; monadInv H.
++ constructor. eapply transl_function_spec; eauto. 
++ constructor.
+Qed.
+
+Lemma transl_globdefs_spec:
+  forall l g l',
+  transl_globdefs l g = OK l' ->
+  list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'.
+Proof.
+  induction l; simpl; intros.
+- inv H. constructor.
+- destruct a as [id gd]. destruct gd.
+  + destruct (transl_fundef f g) as [? | tf g' ?] eqn:E1; try discriminate.
+    destruct (transl_globdefs l g') eqn:E2; simpl in H; inv H.
+    constructor; eauto. constructor. eapply transl_fundef_spec; eauto.
+  + destruct (transl_globdefs l g) eqn:E2; simpl in H; inv H.
+    constructor; eauto. destruct v; constructor; auto.
+Qed.
+
+Theorem transl_program_spec:
+  forall p tp,
+  transl_program p = OK tp ->
+  match_program tr_fundef (fun v1 v2 => v1 = v2) nil p.(prog_main) p tp.
+Proof.
+  unfold transl_program; intros. 
+  destruct (transl_globdefs (prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H.
+  split; auto. exists l; split. eapply transl_globdefs_spec; eauto. 
+  rewrite <- app_nil_end; auto.
 Qed.
 
 End SPEC.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 38660c6..515049a 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -114,8 +114,8 @@ Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (t
       match_var f cenv e m te tle id.
 
 Record match_envs (f: meminj) (cenv: compilenv)
-                  (e: env) (le: temp_env) (m: mem) (lo hi: Z)
-                  (te: env) (tle: temp_env) (tlo thi: Z) : Prop :=
+                  (e: env) (le: temp_env) (m: mem) (lo hi: block)
+                  (te: env) (tle: temp_env) (tlo thi: block) : Prop :=
   mk_match_envs {
     me_vars:
       forall id, match_var f cenv e m te tle id;
@@ -127,9 +127,9 @@ Record match_envs (f: meminj) (cenv: compilenv)
     me_inj:
       forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2;
     me_range:
-      forall id b ty, e!id = Some(b, ty) -> lo <= b < hi;
+      forall id b ty, e!id = Some(b, ty) -> Ple lo b /\ Plt b hi;
     me_trange:
-      forall id b ty, te!id = Some(b, ty) -> tlo <= b < thi;
+      forall id b ty, te!id = Some(b, ty) -> Ple tlo b /\ Plt b thi;
     me_mapped:
       forall id b' ty,
       te!id = Some(b', ty) -> exists b, f b = Some(b', 0) /\ e!id = Some(b, ty);
@@ -137,9 +137,9 @@ Record match_envs (f: meminj) (cenv: compilenv)
       forall id b' ty b delta,
       te!id = Some(b', ty) -> f b = Some(b', delta) -> e!id = Some(b, ty) /\ delta = 0;
     me_incr:
-      lo <= hi;
+      Ple lo hi;
     me_tincr:
-      tlo <= thi
+      Ple tlo thi
   }.
 
 (** Invariance by change of memory and injection *)
@@ -148,10 +148,10 @@ Lemma match_envs_invariant:
   forall f cenv e le m lo hi te tle tlo thi f' m',
   match_envs f cenv e le m lo hi te tle tlo thi ->
   (forall b chunk v,
-    f b = None -> lo <= b < hi -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
+    f b = None -> Ple lo b /\ Plt b hi -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
   inject_incr f f' ->
-  (forall b, lo <= b < hi -> f' b = f b) ->
-  (forall b b' delta, f' b = Some(b', delta) -> tlo <= b' < thi -> f' b = f b) ->
+  (forall b, Ple lo b /\ Plt b hi -> f' b = f b) ->
+  (forall b b' delta, f' b = Some(b', delta) -> Ple tlo b' /\ Plt b' thi -> f' b = f b) ->
   match_envs f' cenv e le m' lo hi te tle tlo thi.
 Proof.
   intros until m'; intros ME LD INCR INV1 INV2. 
@@ -175,22 +175,22 @@ Qed.
 Lemma match_envs_extcall:
   forall f cenv e le m lo hi te tle tlo thi tm f' m',
   match_envs f cenv e le m lo hi te tle tlo thi ->
-  mem_unchanged_on (loc_unmapped f) m m' ->
+  Mem.unchanged_on (loc_unmapped f) m m' ->
   inject_incr f f' ->
   inject_separated f f' m tm ->
-  hi <= Mem.nextblock m -> thi <= Mem.nextblock tm ->
+  Ple hi (Mem.nextblock m) -> Ple thi (Mem.nextblock tm) ->
   match_envs f' cenv e le m' lo hi te tle tlo thi.
 Proof.
   intros. eapply match_envs_invariant; eauto. 
-  intros. destruct H0.  eapply H8. intros; red. auto. auto. 
+  intros. eapply Mem.load_unchanged_on; eauto. 
   red in H2. intros. destruct (f b) as [[b' delta]|] eqn:?. 
   eapply H1; eauto.
   destruct (f' b) as [[b' delta]|] eqn:?; auto. 
   exploit H2; eauto. unfold Mem.valid_block. intros [A B].
-  omegaContradiction.
+  xomegaContradiction.
   intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto. 
   exploit H2; eauto. unfold Mem.valid_block. intros [A B].
-  omegaContradiction.
+  xomegaContradiction.
 Qed.
 
 (** Properties of values obtained by casting to a given type. *)
@@ -591,33 +591,34 @@ Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty: compat.
 
 Lemma alloc_variables_nextblock:
   forall e m vars e' m',
-  alloc_variables e m vars e' m' -> Mem.nextblock m <= Mem.nextblock m'.
+  alloc_variables e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m').
 Proof.
   induction 1.
-  omega.
-  exploit Mem.nextblock_alloc; eauto. unfold block. omega.
+  apply Ple_refl.
+  eapply Ple_trans; eauto. exploit Mem.nextblock_alloc; eauto. intros EQ; rewrite EQ. apply Ple_succ. 
 Qed.
 
 Lemma alloc_variables_range:
   forall id b ty e m vars e' m',
   alloc_variables e m vars e' m' ->
-  e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Mem.nextblock m <= b < Mem.nextblock m'.
+  e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Ple (Mem.nextblock m) b /\ Plt b (Mem.nextblock m').
 Proof.
   induction 1; intros.
   auto.
   exploit IHalloc_variables; eauto. rewrite PTree.gsspec. intros [A|A].
   destruct (peq id id0). inv A. 
-  right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block.
-  generalize (alloc_variables_nextblock _ _ _ _ _ H0). omega.
+  right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto.
+  generalize (alloc_variables_nextblock _ _ _ _ _ H0). intros A B C. 
+  subst b. split. apply Ple_refl. eapply Plt_le_trans; eauto. rewrite B. apply Plt_succ. 
   auto.
-  right. exploit Mem.nextblock_alloc; eauto. unfold block. omega.
+  right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega. 
 Qed.
 
 Lemma alloc_variables_injective:
   forall id1 b1 ty1 id2 b2 ty2 e m vars e' m',
   alloc_variables e m vars e' m' ->
   (e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2) ->
-  (forall id b ty, e!id = Some(b, ty) -> b < Mem.nextblock m) ->
+  (forall id b ty, e!id = Some(b, ty) -> Plt b (Mem.nextblock m)) ->
   (e'!id1 = Some(b1, ty1) -> e'!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2).
 Proof.
   induction 1; intros. 
@@ -626,12 +627,12 @@ Proof.
   repeat rewrite PTree.gsspec; intros.
   destruct (peq id1 id); destruct (peq id2 id).
   congruence.
-  inv H6. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; omega.
-  inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; omega.
+  inv H6. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; xomega.
+  inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; xomega.
   eauto.
   intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). inv H6.
-  exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; omega.
-  exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; omega.
+  exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; xomega.
+  exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; xomega.
 Qed.
 
 Lemma match_alloc_variables:
@@ -714,16 +715,16 @@ Proof.
     destruct (eq_block b b1); auto. subst. 
     assert (j' b1 = j1 b1). apply M. eapply Mem.valid_new_block; eauto.
     rewrite H4 in H1. rewrite D in H1. inv H1. eelim Mem.fresh_block_alloc; eauto.
-  split. intros. destruct (zeq b' tb1). 
+  split. intros. destruct (eq_block b' tb1). 
     subst b'. rewrite (N _ _ _ H1) in H1.
-    destruct (zeq b b1). subst b. rewrite D in H1; inv H1. 
+    destruct (eq_block b b1). subst b. rewrite D in H1; inv H1. 
     exploit (P id); auto. intros [X Y]. exists id; exists ty.
     rewrite X; rewrite Y. repeat rewrite PTree.gss. auto.
     rewrite E in H1; auto. elim H3. eapply Mem.mi_mappedblocks; eauto. 
     eapply Mem.valid_new_block; eauto.
     eapply Q; eauto. unfold Mem.valid_block in *.
     exploit Mem.nextblock_alloc. eexact A. exploit Mem.alloc_result. eexact A. 
-    unfold block; omega.
+    unfold block; xomega.
   split. intros. destruct (ident_eq id0 id).
     (* same var *)
     subst id0.
@@ -983,7 +984,7 @@ Proof.
   (* flat *)
   exploit alloc_variables_range. eexact A. eauto. 
   rewrite PTree.gempty. intros [P|P]. congruence. 
-  exploit K; eauto. unfold Mem.valid_block. omega. 
+  exploit K; eauto. unfold Mem.valid_block. xomega. 
   intros [id0 [ty0 [U [V W]]]]. split; auto. 
   destruct (ident_eq id id0). congruence.
   assert (b' <> b').
@@ -1262,7 +1263,7 @@ Proof.
     eapply Mem.range_perm_inject; eauto. 
     eapply free_blocks_of_env_perm_2; eauto.
     (* no repetitions *)
-    set (F := fun id => match te!id with Some(b, ty) => b | None => 0 end).
+    set (F := fun id => match te!id with Some(b, ty) => b | None => xH end).
     replace (map (fun b_lo_hi : block * Z * Z => fst (fst b_lo_hi)) (blocks_of_env te))
        with (map F (map (fun x => fst x) (PTree.elements te))).
     apply list_map_norepet. apply PTree.elements_keys_norepet. 
@@ -1297,14 +1298,13 @@ Qed.
 
 (** Matching global environments *)
 
-Inductive match_globalenvs (f: meminj) (bound: Z): Prop :=
+Inductive match_globalenvs (f: meminj) (bound: block): Prop :=
   | mk_match_globalenvs
-      (POS: bound > 0)
-      (DOMAIN: forall b, b < bound -> f b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+      (DOMAIN: forall b, Plt b bound -> f b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).
 
 Lemma match_globalenvs_preserves_globals:
   forall f,
@@ -1324,7 +1324,7 @@ Variables le tle: temp_env.
 Variables m tm: mem.
 Variable f: meminj.
 Variable cenv: compilenv.
-Variables lo hi tlo thi: Z.
+Variables lo hi tlo thi: block.
 Hypothesis MATCH: match_envs f cenv e le m lo hi te tle tlo thi.
 Hypothesis MEMINJ: Mem.inject f m tm.
 Hypothesis GLOB: exists bound, match_globalenvs f bound.
@@ -1472,9 +1472,9 @@ End EVAL_EXPR.
 
 (** Matching continuations *)
 
-Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> Z -> Z -> Prop :=
+Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> block -> block -> Prop :=
   | match_Kstop: forall cenv m bound tbound hi,
-      match_globalenvs f hi -> hi <= bound -> hi <= tbound ->
+      match_globalenvs f hi -> Ple hi bound -> Ple hi tbound ->
       match_cont f cenv Kstop Kstop m bound tbound
   | match_Kseq: forall cenv s k ts tk m bound tbound,
       simpl_stmt cenv s = OK ts ->
@@ -1501,7 +1501,7 @@ Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> Z -> Z ->
       match_envs f (cenv_for fn) e le m lo hi te tle tlo thi ->
       match_cont f (cenv_for fn) k tk m lo tlo ->
       check_opttemp (cenv_for fn) optid = OK x ->
-      hi <= bound -> thi <= tbound ->
+      Ple hi bound -> Ple thi tbound ->
       match_cont f cenv (Kcall optid fn e le k)
                         (Kcall optid tfn te tle tk) m bound tbound.
 
@@ -1511,26 +1511,26 @@ Lemma match_cont_invariant:
   forall f' m' f cenv k tk m bound tbound,
   match_cont f cenv k tk m bound tbound ->
   (forall b chunk v,
-    f b = None -> b < bound -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
+    f b = None -> Plt b bound -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
   inject_incr f f' ->
-  (forall b, b < bound -> f' b = f b) ->
-  (forall b b' delta, f' b = Some(b', delta) -> b' < tbound -> f' b = f b) ->
+  (forall b, Plt b bound -> f' b = f b) ->
+  (forall b b' delta, f' b = Some(b', delta) -> Plt b' tbound -> f' b = f b) ->
   match_cont f' cenv k tk m' bound tbound.
 Proof.
   induction 1; intros LOAD INCR INJ1 INJ2; econstructor; eauto.
 (* globalenvs *)
   inv H. constructor; intros; eauto.
-  assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. omega.
+  assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. xomega.
   eapply IMAGE; eauto.
 (* call *)
   eapply match_envs_invariant; eauto. 
-  intros. apply LOAD; auto. omega.
-  intros. apply INJ1; auto; omega.
-  intros. eapply INJ2; eauto; omega.
+  intros. apply LOAD; auto. xomega.
+  intros. apply INJ1; auto; xomega.
+  intros. eapply INJ2; eauto; xomega.
   eapply IHmatch_cont; eauto. 
-  intros; apply LOAD; auto. inv H0; omega.
-  intros; apply INJ1. inv H0; omega.
-  intros; eapply INJ2; eauto. inv H0; omega.
+  intros; apply LOAD; auto. inv H0; xomega.
+  intros; apply INJ1. inv H0; xomega.
+  intros; eapply INJ2; eauto. inv H0; xomega.
 Qed.
 
 (** Invariance by assignment to location "above" *)
@@ -1539,15 +1539,15 @@ Lemma match_cont_assign_loc:
   forall f cenv k tk m bound tbound ty loc ofs v m',
   match_cont f cenv k tk m bound tbound ->
   assign_loc ty m loc ofs v m' ->
-  bound <= loc ->
+  Ple bound loc ->
   match_cont f cenv k tk m' bound tbound.
 Proof.
   intros. eapply match_cont_invariant; eauto.
   intros. rewrite <- H4. inv H0.
   (* scalar *)
-  simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; omega. 
+  simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; xomega. 
   (* block copy *)
-  eapply Mem.load_storebytes_other; eauto. left. unfold block; omega.
+  eapply Mem.load_storebytes_other; eauto. left. unfold block; xomega.
 Qed.
 
 (** Invariance by external calls *)
@@ -1555,19 +1555,19 @@ Qed.
 Lemma match_cont_extcall:
   forall f cenv k tk m bound tbound tm f' m',
   match_cont f cenv k tk m bound tbound ->
-  mem_unchanged_on (loc_unmapped f) m m' ->
+  Mem.unchanged_on (loc_unmapped f) m m' ->
   inject_incr f f' ->
   inject_separated f f' m tm ->
-  bound <= Mem.nextblock m -> tbound <= Mem.nextblock tm ->
+  Ple bound (Mem.nextblock m) -> Ple tbound (Mem.nextblock tm) ->
   match_cont f' cenv k tk m' bound tbound.
 Proof.
   intros. eapply match_cont_invariant; eauto. 
-  destruct H0. intros. eapply H5; eauto. 
+  intros. eapply Mem.load_unchanged_on; eauto. 
   red in H2. intros. destruct (f b) as [[b' delta] | ] eqn:?. auto. 
   destruct (f' b) as [[b' delta] | ] eqn:?; auto. 
-  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction.
+  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. xomegaContradiction.
   red in H2. intros. destruct (f b) as [[b'' delta''] | ] eqn:?. auto. 
-  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction.
+  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. xomegaContradiction.
 Qed.
 
 (** Invariance by change of bounds *)
@@ -1576,10 +1576,10 @@ Lemma match_cont_incr_bounds:
   forall f cenv k tk m bound tbound,
   match_cont f cenv k tk m bound tbound ->
   forall bound' tbound',
-  bound <= bound' -> tbound <= tbound' ->
+  Ple bound bound' -> Ple tbound tbound' ->
   match_cont f cenv k tk m bound' tbound'.
 Proof.
-  induction 1; intros; econstructor; eauto; omega.
+  induction 1; intros; econstructor; eauto; xomega.
 Qed.
 
 (** [match_cont] and call continuations. *)
@@ -1626,22 +1626,22 @@ Qed.
 Remark free_list_load:
   forall chunk b' l m m',
   Mem.free_list m l = Some m' ->
-  (forall b lo hi, In (b, lo, hi) l -> b' < b) ->
+  (forall b lo hi, In (b, lo, hi) l -> Plt b' b) ->
   Mem.load chunk m' b' 0 = Mem.load chunk m b' 0.
 Proof.
   induction l; simpl; intros.
   inv H; auto.
   destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate.
   transitivity (Mem.load chunk m1 b' 0). eauto. 
-  eapply Mem.load_free. eauto. left. assert (b' < b) by eauto. unfold block; omega.
+  eapply Mem.load_free. eauto. left. assert (Plt b' b) by eauto. unfold block; xomega.
 Qed.
 
 Lemma match_cont_free_env:
   forall f cenv e le m lo hi te tle tm tlo thi k tk m' tm',
   match_envs f cenv e le m lo hi te tle tlo thi ->
   match_cont f cenv k tk m lo tlo ->
-  hi <= Mem.nextblock m ->
-  thi <= Mem.nextblock tm ->
+  Ple hi (Mem.nextblock m) ->
+  Ple thi (Mem.nextblock tm) ->
   Mem.free_list m (blocks_of_env e) = Some m' ->
   Mem.free_list tm (blocks_of_env te) = Some tm' ->
   match_cont f cenv k tk m' (Mem.nextblock m') (Mem.nextblock tm').
@@ -1651,9 +1651,9 @@ Proof.
   intros. rewrite <- H7. eapply free_list_load; eauto. 
   unfold blocks_of_env; intros. exploit list_in_map_inv; eauto. 
   intros [[id [b1 ty]] [P Q]]. simpl in P. inv P. 
-  exploit me_range; eauto. eapply PTree.elements_complete; eauto. omega.
-  rewrite (free_list_nextblock _ _ _ H3). inv H; omega.
-  rewrite (free_list_nextblock _ _ _ H4). inv H; omega.
+  exploit me_range; eauto. eapply PTree.elements_complete; eauto. xomega.
+  rewrite (free_list_nextblock _ _ _ H3). inv H; xomega.
+  rewrite (free_list_nextblock _ _ _ H4). inv H; xomega.
 Qed.
 
 (** Matching of global environments *)
@@ -1695,8 +1695,8 @@ Inductive match_states: state -> state -> Prop :=
         (MCONT: match_cont j (cenv_for f) k tk m lo tlo)
         (MINJ: Mem.inject j m tm)
         (COMPAT: compat_cenv (addr_taken_stmt s) (cenv_for f))
-        (BOUND: hi <= Mem.nextblock m)
-        (TBOUND: thi <= Mem.nextblock tm),
+        (BOUND: Ple hi (Mem.nextblock m))
+        (TBOUND: Ple thi (Mem.nextblock tm)),
       match_states (State f s k e le m)
                    (State tf ts tk te tle tm)
   | match_call_state:
@@ -1900,7 +1900,7 @@ Proof.
   apply plus_one. econstructor. eapply make_cast_correct. eexact A. rewrite typeof_simpl_expr. eexact C.
   econstructor; eauto with compat. 
   eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto.
-  eapply match_cont_assign_loc; eauto. exploit me_range; eauto. omega.
+  eapply match_cont_assign_loc; eauto. exploit me_range; eauto. xomega.
   inv MV; try congruence. inv H2; try congruence. unfold Mem.storev in H3.
   eapply Mem.store_unmapped_inject; eauto. congruence. 
   erewrite assign_loc_nextblock; eauto.
@@ -1951,9 +1951,9 @@ Proof.
   eapply match_envs_set_opttemp; eauto. 
   eapply match_envs_extcall; eauto. 
   eapply match_cont_extcall; eauto.
-  inv MENV; omega. inv MENV; omega. 
-  eapply Zle_trans; eauto. eapply external_call_nextblock; eauto.
-  eapply Zle_trans; eauto. eapply external_call_nextblock; eauto.
+  inv MENV; xomega. inv MENV; xomega. 
+  eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
+  eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
 
 (* sequence *)
   econstructor; split. apply plus_one. econstructor.
@@ -2085,11 +2085,11 @@ Proof.
   eapply bind_parameters_load; eauto. intros. 
   exploit alloc_variables_range. eexact H1. eauto. 
   unfold empty_env. rewrite PTree.gempty. intros [?|?]. congruence. 
-  red; intros; subst b'. omega. 
+  red; intros; subst b'. xomega. 
   eapply alloc_variables_load; eauto.
   apply compat_cenv_for. 
-  rewrite (bind_parameters_nextblock _ _ _ _ _ H2). omega.
-  rewrite T; omega.
+  rewrite (bind_parameters_nextblock _ _ _ _ _ H2). xomega.
+  rewrite T; xomega.
 
 (* external function *)
   monadInv TRFD. inv FUNTY. 
@@ -2101,7 +2101,7 @@ Proof.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
   intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm).
-  eapply match_cont_extcall; eauto. omega. omega.
+  eapply match_cont_extcall; eauto. xomega. xomega.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
@@ -2130,13 +2130,12 @@ Proof.
   intros. instantiate (1 := Mem.flat_inj (Mem.nextblock m0)). 
   econstructor. instantiate (1 := Mem.nextblock m0). 
   constructor; intros. 
-  apply Mem.nextblock_pos.
-  unfold Mem.flat_inj. apply zlt_true; auto. 
-  unfold Mem.flat_inj in H. destruct (zlt b1 (Mem.nextblock m0)); inv H. auto.
+  unfold Mem.flat_inj. apply pred_dec_true; auto. 
+  unfold Mem.flat_inj in H. destruct (plt b1 (Mem.nextblock m0)); inv H. auto.
   eapply Genv.find_symbol_not_fresh; eauto.
   eapply Genv.find_funct_ptr_not_fresh; eauto.
   eapply Genv.find_var_info_not_fresh; eauto.
-  omega. omega.
+  xomega. xomega.
   eapply Genv.initmem_inject; eauto.
   constructor.
 Qed.