Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


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

8 files changed, 1321 insertions, 408 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index d99e20f..e057771 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -252,6 +252,11 @@ let camlstring_of_coqstring (s: char list) =
   | c :: s -> r.[pos] <- c; fill (pos + 1) s
   in fill 0 s
 
+let coqstring_of_camlstring s =
+  let rec cstring accu pos =
+    if pos < 0 then accu else cstring (s.[pos] :: accu) (pos - 1)
+  in cstring [] (String.length s - 1)
+
 (* Floats *)
 
 let coqfloat_of_camlfloat f =
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index b936b9b..ce5d94e 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -559,6 +559,16 @@ Proof.
 Defined.
 Global Opaque Zdivide_dec.
 
+Lemma Zdivide_interval:
+  forall a b c,
+  0 < c -> 0 <= a < b -> (c | a) -> (c | b) -> 0 <= a <= b - c.
+Proof.
+  intros. destruct H1 as [x EQ1]. destruct H2 as [y EQ2]. subst. destruct H0.
+  split. omega. exploit Zmult_lt_reg_r; eauto. intros. 
+  replace (y * c - c) with ((y - 1) * c) by ring.
+  apply Zmult_le_compat_r; omega.
+Qed.
+
 (** Conversion from [Z] to [nat]. *)
 
 Definition nat_of_Z: Z -> nat := Z.to_nat.
@@ -1250,6 +1260,17 @@ Proof.
   intros. unfold proj_sumbool. destruct a. auto. contradiction. 
 Qed.
 
+Ltac InvBooleans :=
+  match goal with
+  | [ H: _ && _ = true |- _ ] =>
+      destruct (andb_prop _ _ H); clear H; InvBooleans
+  | [ H: _ || _ = false |- _ ] =>
+      destruct (orb_false_elim _ _ H); clear H; InvBooleans
+  | [ H: proj_sumbool ?x = true |- _ ] =>
+      generalize (proj_sumbool_true _ H); clear H; intro; InvBooleans
+  | _ => idtac
+  end.
+
 Section DECIDABLE_EQUALITY.
 
 Variable A: Type.
diff --git a/lib/FSetAVLplus.v b/lib/FSetAVLplus.v
new file mode 100644
index 0000000..5f5cc51
--- /dev/null
+++ b/lib/FSetAVLplus.v
@@ -0,0 +1,513 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** An extension of [FSetAVL] (finite sets as balanced binary search trees)
+  with extra interval-based operations, more efficient than standard
+  operations. *)
+
+Require Import FSetInterface.
+Require FSetAVL.
+Require Import Coqlib.
+
+Module Make(X: OrderedType).
+
+Include FSetAVL.Make(X).
+
+Module Raw := MSet.Raw.
+
+Section MEM_BETWEEN.
+
+(** [mem_between above below s] is [true] iff there exists an element of [s]
+  that belongs to the interval described by the predicates [above] and [below].
+  Using the monotonicity of [above] and [below], the implementation of
+  [mem_between] avoids traversing the subtrees of [s] that
+  lie entirely outside the interval of interest. *)
+
+Variable above_low_bound: elt -> bool.
+Variable below_high_bound: elt -> bool.
+
+Fixpoint raw_mem_between (m: Raw.tree) : bool :=
+  match m with
+  | Raw.Leaf => false
+  | Raw.Node _ l x r =>
+      if above_low_bound x
+      then if below_high_bound x
+           then true
+           else raw_mem_between l
+      else raw_mem_between r
+  end.
+
+Definition mem_between (m: t) : bool := raw_mem_between m.(MSet.this).
+
+Hypothesis above_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
+Hypothesis below_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.
+
+Lemma raw_mem_between_1:
+  forall m,
+  raw_mem_between m = true ->
+  exists x, Raw.In x m /\ above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  induction m; simpl; intros.
+- discriminate.
+- destruct (above_low_bound t1) eqn: LB; [destruct (below_high_bound t1) eqn: HB | idtac].
+  + (* in interval *)
+    exists t1; split; auto.  apply Raw.IsRoot. auto. 
+  + (* above interval *)
+    exploit IHm1; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InLeft; auto.
+  + (* below interval *)
+    exploit IHm2; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InRight; auto.
+Qed.
+
+Lemma raw_mem_between_2:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
+  raw_mem_between m = true.
+Proof.
+  induction 1; simpl; intros.
+- inv H.
+- rewrite Raw.In_node_iff in H1. 
+  destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac].
+  + (* in interval *)
+    auto.
+  + (* above interval *)
+    assert (X.eq x x0 \/ X.lt x0 x -> False).
+    { intros. exploit below_monotone; eauto. congruence. }
+    intuition.
+  + assert (X.eq x x0 \/ X.lt x x0 -> False).
+    { intros. exploit above_monotone; eauto. congruence. }
+    intuition.
+Qed.
+
+Theorem mem_between_1:
+  forall s,
+  mem_between s = true ->
+  exists x, In x s /\ above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  intros. apply raw_mem_between_1. auto. 
+Qed.
+
+Theorem mem_between_2:
+  forall x s,
+  In x s -> above_low_bound x = true -> below_high_bound x = true ->
+  mem_between s = true.
+Proof.
+  unfold mem_between; intros. apply raw_mem_between_2 with x; auto. apply MSet.is_ok.
+Qed.
+
+End MEM_BETWEEN.
+
+Section ELEMENTS_BETWEEN.
+
+(** [elements_between above below s] returns the set of elements of [s]
+  that belong to the interval [above,below]. *)
+
+Variable above_low_bound: elt -> bool.
+Variable below_high_bound: elt -> bool.
+
+Fixpoint raw_elements_between (m: Raw.tree) : Raw.tree :=
+  match m with
+  | Raw.Leaf => Raw.Leaf
+  | Raw.Node _ l x r =>
+      if above_low_bound x then
+        if below_high_bound x then
+          Raw.join (raw_elements_between l) x (raw_elements_between r)
+        else
+          raw_elements_between l
+      else
+        raw_elements_between r
+  end.
+
+Remark In_raw_elements_between_1:
+  forall x m,
+  Raw.In x (raw_elements_between m) -> Raw.In x m.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- rewrite Raw.In_node_iff. 
+  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.join_spec in H. intuition. 
+  + left; apply IHm1; auto.
+  + right; right; apply IHm2; auto.
+Qed.
+
+Lemma raw_elements_between_ok:
+  forall m, Raw.bst m -> Raw.bst (raw_elements_between m).
+Proof.
+  induction 1; simpl.
+- constructor.
+- destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl.
+  + apply Raw.join_ok; auto.
+    red; intros. apply l0. apply In_raw_elements_between_1; auto.
+    red; intros. apply g. apply In_raw_elements_between_1; auto.
+  + auto.
+  + auto.
+Qed.
+
+Definition elements_between (s: t) : t :=
+  @MSet.Mkt (raw_elements_between s.(MSet.this)) (raw_elements_between_ok s.(MSet.this) s.(MSet.is_ok)).
+
+Hypothesis above_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
+Hypothesis below_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.
+
+Remark In_raw_elements_between_2:
+  forall x m,
+  Raw.In x (raw_elements_between m) -> above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.join_spec in H. intuition.
+    apply above_monotone with t1; auto. 
+    apply below_monotone with t1; auto.
+  + auto.
+  + auto.
+Qed.
+
+Remark In_raw_elements_between_3:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
+  Raw.In x (raw_elements_between m).
+Proof.
+  induction 1; simpl; intros.
+- auto.
+- rewrite Raw.In_node_iff in H1.
+  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac].
+  + rewrite Raw.join_spec. intuition. 
+  + assert (X.eq x x0 \/ X.lt x0 x -> False).
+    { intros. exploit below_monotone; eauto. congruence. }
+    intuition. elim H7. apply g. auto.
+  + assert (X.eq x x0 \/ X.lt x x0 -> False).
+    { intros. exploit above_monotone; eauto. congruence. }
+    intuition. elim H7. apply l0. auto.
+Qed.
+
+Theorem elements_between_iff:
+  forall x s,
+  In x (elements_between s) <-> In x s /\ above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  intros. unfold elements_between, In; simpl. split.
+  intros. split. apply In_raw_elements_between_1; auto. eapply In_raw_elements_between_2; eauto. 
+  intros [A [B C]]. apply In_raw_elements_between_3; auto. apply MSet.is_ok.
+Qed.
+
+End ELEMENTS_BETWEEN.
+
+Section FOR_ALL_BETWEEN.
+
+(** [for_all_between pred above below s] is [true] iff all elements of [s]
+  in a given variation interval satisfy predicate [pred].
+  The variation interval is given by two predicates [above] and [below]
+  which must both hold if the element is part of the interval.
+  Using the monotonicity of [above] and [below], the implementation of
+  [for_all_between] avoids traversing the subtrees of [s] that
+  lie entirely outside the interval of interest. *)
+
+Variable pred: elt -> bool.
+Variable above_low_bound: elt -> bool.
+Variable below_high_bound: elt -> bool.
+
+Fixpoint raw_for_all_between (m: Raw.tree) : bool :=
+  match m with
+  | Raw.Leaf => true
+  | Raw.Node _ l x r =>
+      if above_low_bound x
+      then if below_high_bound x
+           then raw_for_all_between l && pred x && raw_for_all_between r
+           else raw_for_all_between l
+      else raw_for_all_between r
+  end.
+
+Definition for_all_between (m: t) : bool := raw_for_all_between m.(MSet.this).
+
+Hypothesis pred_compat:
+  forall x1 x2, X.eq x1 x2 -> pred x1 = pred x2.
+Hypothesis above_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
+Hypothesis below_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.
+
+Lemma raw_for_all_between_1:
+  forall x m,
+  Raw.bst m ->
+  raw_for_all_between m = true ->
+  Raw.In x m ->
+  above_low_bound x = true ->
+  below_high_bound x = true ->
+  pred x = true.
+Proof.
+  induction 1; simpl; intros.
+- inv H0. 
+- destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac].
+  + (* in interval *)
+    destruct (andb_prop _ _ H1) as [P C]. destruct (andb_prop _ _ P) as [A B]. clear H1 P.
+    inv H2.
+    * erewrite pred_compat; eauto. 
+    * apply IHbst1; auto.
+    * apply IHbst2; auto.
+  + (* above interval *)
+    inv H2.
+    * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). 
+      congruence.
+    * apply IHbst1; auto.
+    * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
+      congruence.
+  + (* below interval *)
+    inv H2.
+    * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). 
+      congruence.
+    * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
+      congruence.
+    * apply IHbst2; auto.
+Qed.
+
+Lemma raw_for_all_between_2:
+  forall m,
+  Raw.bst m ->
+  (forall x, Raw.In x m -> above_low_bound x = true -> below_high_bound x = true -> pred x = true) ->
+  raw_for_all_between m = true.
+Proof.
+  induction 1; intros; simpl.
+- auto.
+- destruct (above_low_bound x) eqn: LB; [destruct (below_high_bound x) eqn: HB | idtac].
+  + (* in interval *)
+    rewrite IHbst1. rewrite (H1 x). rewrite IHbst2. auto.
+    intros. apply H1; auto. apply Raw.InRight; auto.
+    apply Raw.IsRoot. reflexivity. auto. auto. 
+    intros. apply H1; auto. apply Raw.InLeft; auto.
+  + (* above interval *)
+    apply IHbst1. intros. apply H1; auto. apply Raw.InLeft; auto.
+  + (* below interval *)
+    apply IHbst2. intros. apply H1; auto. apply Raw.InRight; auto.
+Qed.
+
+Theorem for_all_between_iff:
+  forall s,
+  for_all_between s = true <-> (forall x, In x s -> above_low_bound x = true -> below_high_bound x = true -> pred x = true).
+Proof.
+  unfold for_all_between; intros; split; intros.
+- eapply raw_for_all_between_1; eauto. apply MSet.is_ok. 
+- apply raw_for_all_between_2; auto. apply MSet.is_ok.
+Qed.
+
+End FOR_ALL_BETWEEN.
+
+Section PARTITION_BETWEEN.
+
+Variable above_low_bound: elt -> bool.
+Variable below_high_bound: elt -> bool.
+
+Fixpoint raw_partition_between (m: Raw.tree) : Raw.tree * Raw.tree :=
+  match m with
+  | Raw.Leaf => (Raw.Leaf, Raw.Leaf)
+  | Raw.Node _ l x r =>
+      if above_low_bound x then
+        if below_high_bound x then
+          (let (l1, l2) := raw_partition_between l in
+           let (r1, r2) := raw_partition_between r in
+           (Raw.join l1 x r1, Raw.concat l2 r2))
+        else
+          (let (l1, l2) := raw_partition_between l in
+           (l1, Raw.join l2 x r))
+      else
+        (let (r1, r2) := raw_partition_between r in
+         (r1, Raw.join l x r2))
+  end.
+
+Remark In_raw_partition_between_1:
+  forall x m,
+  Raw.In x (fst (raw_partition_between m)) -> Raw.In x m.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. 
+  + rewrite Raw.In_node_iff. intuition.
+  + rewrite Raw.In_node_iff. intuition.
+Qed.
+
+Remark In_raw_partition_between_2:
+  forall x m,
+  Raw.In x (snd (raw_partition_between m)) -> Raw.In x m.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.concat_spec in H. rewrite Raw.In_node_iff. intuition. 
+  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
+  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
+Qed.
+
+Lemma raw_partition_between_ok:
+  forall m, Raw.bst m -> Raw.bst (fst (raw_partition_between m)) /\ Raw.bst (snd (raw_partition_between m)).
+Proof.
+  induction 1; simpl.
+- split; constructor.
+- destruct IHbst1 as [L1 L2]. destruct IHbst2 as [R1 R2]. 
+  destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl.
+  + split.
+    apply Raw.join_ok; auto.
+    red; intros. apply l0. apply In_raw_partition_between_1. rewrite LEQ; auto. 
+    red; intros. apply g. apply In_raw_partition_between_1. rewrite REQ; auto.
+    apply Raw.concat_ok; auto.
+    intros. transitivity x. 
+    apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. 
+    apply g. apply In_raw_partition_between_2. rewrite REQ; auto.
+  + split.
+    auto.
+    apply Raw.join_ok; auto.
+    red; intros. apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. 
+  + split.
+    auto.
+    apply Raw.join_ok; auto.
+    red; intros. apply g. apply In_raw_partition_between_2. rewrite REQ; auto.
+Qed.
+
+Hypothesis above_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
+Hypothesis below_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.
+
+Remark In_raw_partition_between_3:
+  forall x m,
+  Raw.In x (fst (raw_partition_between m)) -> above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.join_spec in H. intuition.
+    apply above_monotone with t1; auto. 
+    apply below_monotone with t1; auto.
+  + auto.
+  + auto.
+Qed.
+
+Remark In_raw_partition_between_4:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x (snd (raw_partition_between m)) -> above_low_bound x = false \/ below_high_bound x = false.
+Proof.
+  induction 1; simpl; intros.
+- inv H.
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
+  + simpl in H1. rewrite Raw.concat_spec in H1. intuition. 
+  + assert (forall y, X.eq y x0 \/ X.lt x0 y -> below_high_bound y = false).
+    { intros. destruct (below_high_bound y) eqn:E; auto. 
+      assert (below_high_bound x0 = true) by (apply below_monotone with y; auto).
+      congruence. }
+    simpl in H1. rewrite Raw.join_spec in H1. intuition.
+  + assert (forall y, X.eq y x0 \/ X.lt y x0 -> above_low_bound y = false).
+    { intros. destruct (above_low_bound y) eqn:E; auto. 
+      assert (above_low_bound x0 = true) by (apply above_monotone with y; auto).
+      congruence. }
+    simpl in H1. rewrite Raw.join_spec in H1. intuition.
+Qed.
+
+Remark In_raw_partition_between_5:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
+  Raw.In x (fst (raw_partition_between m)).
+Proof.
+  induction 1; simpl; intros.
+- inv H.
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
+  + simpl. rewrite Raw.join_spec. inv H1. 
+    auto.
+    right; left; apply IHbst1; auto. 
+    right; right; apply IHbst2; auto.
+  + simpl. inv H1. 
+    assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
+    congruence.
+    auto. 
+    assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). 
+    congruence.
+  + simpl. inv H1. 
+    assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
+    congruence.
+    assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). 
+    congruence.
+    eauto.
+Qed.
+
+Remark In_raw_partition_between_6:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x m -> above_low_bound x = false \/ below_high_bound x = false ->
+  Raw.In x (snd (raw_partition_between m)).
+Proof.
+  induction 1; simpl; intros.
+- inv H.
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
+  + simpl. rewrite Raw.concat_spec. inv H1.
+    assert (below_high_bound x = true) by (apply below_monotone with x0; auto; left; symmetry; auto).
+    assert (above_low_bound x = true) by (apply above_monotone with x0; auto; left; symmetry; auto).
+    destruct H2; congruence.
+    left; apply IHbst1; auto.
+    right; apply IHbst2; auto.
+  + simpl. rewrite Raw.join_spec. inv H1. 
+    auto.
+    right; left; apply IHbst1; auto. 
+    auto.
+  + simpl. rewrite Raw.join_spec. inv H1. 
+    auto.
+    auto.
+    right; right; apply IHbst2; auto.
+Qed.
+
+Definition partition_between (s: t) : t * t :=
+  let p := raw_partition_between s.(MSet.this) in
+  (@MSet.Mkt (fst p) (proj1 (raw_partition_between_ok s.(MSet.this) s.(MSet.is_ok))),
+   @MSet.Mkt (snd p) (proj2 (raw_partition_between_ok s.(MSet.this) s.(MSet.is_ok)))).
+
+Theorem partition_between_iff_1:
+  forall x s,
+  In x (fst (partition_between s)) <->
+  In x s /\ above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  intros. unfold partition_between, In; simpl. split. 
+  intros. split. apply In_raw_partition_between_1; auto. eapply In_raw_partition_between_3; eauto.
+  intros [A [B C]]. apply In_raw_partition_between_5; auto. apply MSet.is_ok.
+Qed.
+
+Theorem partition_between_iff_2:
+  forall x s,
+  In x (snd (partition_between s)) <->
+  In x s /\ (above_low_bound x = false \/ below_high_bound x = false).
+Proof.
+  intros. unfold partition_between, In; simpl. split. 
+  intros. split. apply In_raw_partition_between_2; auto. eapply In_raw_partition_between_4; eauto. apply MSet.is_ok.
+  intros [A B]. apply In_raw_partition_between_6; auto. apply MSet.is_ok.
+Qed.
+
+End PARTITION_BETWEEN.
+
+End Make.
diff --git a/lib/Floats.v b/lib/Floats.v
index eb86027..02ff25c 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -121,6 +121,26 @@ Definition intuoffloat (f:float): option int := (**r conversion to unsigned 32-b
     | None => None
   end.
 
+Definition longoffloat (f:float): option int64 := (**r conversion to signed 64-bit int *)
+  match Zoffloat f with
+    | Some n =>
+      if Zle_bool Int64.min_signed n && Zle_bool n Int64.max_signed then
+        Some (Int64.repr n)
+      else
+        None
+    | None => None
+  end.
+
+Definition longuoffloat (f:float): option int64 := (**r conversion to unsigned 64-bit int *)
+  match Zoffloat f with
+    | Some n =>
+      if Zle_bool 0 n && Zle_bool n Int64.max_unsigned then
+        Some (Int64.repr n)
+      else
+        None
+    | None => None
+  end.
+
 (* Functions used to parse floats *)
 Program Definition build_from_parsed
   (prec:Z) (emax:Z) (prec_gt_0 :Prec_gt_0 prec) (Hmax:prec < emax)
@@ -154,6 +174,11 @@ Definition floatofint (n:int): float := (**r conversion from signed 32-bit int *
   binary_normalize64 (Int.signed n) 0 false.
 Definition floatofintu (n:int): float:= (**r conversion from unsigned 32-bit int *)
   binary_normalize64 (Int.unsigned n) 0 false.
+Definition floatoflong (n:int64): float := (**r conversion from signed 64-bit int *)
+  binary_normalize64 (Int64.signed n) 0 false.
+Definition floatoflongu (n:int64): float:= (**r conversion from unsigned 64-bit int *)
+  binary_normalize64 (Int64.unsigned n) 0 false.
+
 Definition add: float -> float -> float := b64_plus mode_NE. (**r addition *)
 Definition sub: float -> float -> float := b64_minus mode_NE. (**r subtraction *)
 Definition mul: float -> float -> float := b64_mult mode_NE. (**r multiplication *)
@@ -217,24 +242,7 @@ Definition double_of_bits (b: int64): float := b64_of_bits (Int64.unsigned b).
 Definition bits_of_single (f: float) : int := Int.repr (bits_of_b32 (binary32offloat f)).
 Definition single_of_bits (b: int): float := floatofbinary32 (b32_of_bits (Int.unsigned b)).
 
-Definition from_words (hi lo: int) : float :=
-  double_of_bits
-    (Int64.or (Int64.shl (Int64.repr (Int.unsigned hi)) (Int64.repr 32))
-              (Int64.repr (Int.unsigned lo))).
-
-Lemma from_words_eq:
-  forall lo hi,
-  from_words hi lo =
-  double_of_bits (Int64.repr (Int.unsigned hi * two_p 32 + Int.unsigned lo)).
-Proof.
-  intros. unfold from_words. decEq.
-  rewrite Int64.shifted_or_is_add.
-  apply Int64.eqm_samerepr. auto with ints.
-  change Int64.zwordsize with 64. omega.
-  generalize (Int.unsigned_range lo). intros [A B]. 
-  rewrite Int64.unsigned_repr. assumption. 
-  assert (Int.modulus < Int64.max_unsigned). compute; auto. omega.
-Qed.
+Definition from_words (hi lo: int) : float := double_of_bits (Int64.ofwords hi lo).
 
 (** Below are the only properties of floating-point arithmetic that we
   rely on in the compiler proof. *)
@@ -747,35 +755,11 @@ Definition ox4330_0000 := Int.repr 1127219200.        (**r [0x4330_0000] *)
 
 Lemma split_bits_or:
   forall x,
-  split_bits 52 11
-  (Int64.unsigned
-    (Int64.or
-      (Int64.shl (Int64.repr (Int.unsigned ox4330_0000)) (Int64.repr 32))
-      (Int64.repr (Int.unsigned x)))) = (false, Int.unsigned x, 1075).
+  split_bits 52 11 (Int64.unsigned (Int64.ofwords ox4330_0000 x)) = (false, Int.unsigned x, 1075).
 Proof.
   intros.
   transitivity (split_bits 52 11 (join_bits 52 11 false (Int.unsigned x) 1075)).
-  - f_equal.
-    assert (Int64.unsigned (Int64.repr (Int.unsigned x)) = Int.unsigned x).
-      apply Int64.unsigned_repr. 
-      generalize (Int.unsigned_range x).
-      compute_this (Int.modulus).
-      compute_this (Int64.max_unsigned). 
-      omega.
-    rewrite Int64.shifted_or_is_add.
-    unfold join_bits.
-    rewrite H. 
-    apply Int64.unsigned_repr.
-    generalize (Int.unsigned_range x). 
-    compute_this ((0 + 1075) * 2 ^ 52).
-    compute_this (Int.modulus).
-    compute_this (Int64.max_unsigned). 
-    omega.
-    compute_this Int64.zwordsize. omega.
-    rewrite H. 
-    generalize (Int.unsigned_range x). 
-    change (two_p 32) with Int.modulus. 
-    omega.
+  - f_equal. rewrite Int64.ofwords_add'. reflexivity. 
   - apply split_join_bits. 
     compute; auto.
     generalize (Int.unsigned_range x). 
diff --git a/lib/Integers.v b/lib/Integers.v
index af9decd..84b82bf 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -16,8 +16,8 @@
 (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *)
 
 Require Import Eqdep_dec.
+Require Import Zquot.
 Require Import Zwf.
-Require Recdef.
 Require Import Coqlib.
 
 (** * Comparisons *)
@@ -1061,36 +1061,7 @@ Proof.
   apply eqm_mult; apply eqm_sym; apply eqm_signed_unsigned.
 Qed.
 
-(** ** Properties of division and Lemma Ztestbit_same_equal:
-  forall x y,
-  (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) ->
-  x = y.
-Proof.
-  assert (forall x, 0 <= x ->
-          forall y,
-           (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) ->
-           x = y).
-  {
-    intros x0 POS0; pattern x0; apply Zdiv2_pos_ind; auto.
-    - intros. symmetry. apply Ztestbit_is_zero. 
-      intros. rewrite <- H; auto. apply Z.testbit_0_l. 
-    - intros. rewrite (Zdecomp x); rewrite (Zdecomp y). f_equal.
-      + exploit (H0 0). omega. rewrite !(Ztestbit_eq 0).
-        rewrite !zeq_true. auto. omega. omega.
-      + intros. apply H; intros.
-        exploit (H0 (Zsucc i)). omega. rewrite !(Ztestbit_eq (Z.succ i)). 
-        rewrite !zeq_false. rewrite !Z.pred_succ. auto. 
-        omega. omega. omega. omega.
-  }
-  intros. destruct (zle 0 x).
-  - apply H; auto.
-  - assert (-x-1 = -y-1). 
-    { apply H. omega. intros. rewrite !Z_one_complement; auto. 
-      rewrite H0; auto. 
-    }
-    omega.
-Qed.
-modulus *)
+(** ** Properties of division and modulus *)
 
 Lemma modu_divu_Euclid:
   forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y).
@@ -1155,8 +1126,6 @@ Proof.
   apply one_not_zero.
 Qed.
 
-Require Import Zquot.
-
 Theorem divs_mone:
   forall x, divs x mone = neg x.
 Proof.
@@ -3707,7 +3676,434 @@ Module Wordsize_64.
   Proof. unfold wordsize; congruence. Qed.
 End Wordsize_64.
 
-Module Int64 := Make(Wordsize_64).
+Module Int64.
+
+Include Make(Wordsize_64).
+
+(** Shifts with amount given as a 32-bit integer *)
+
+Definition iwordsize': Int.int := Int.repr zwordsize.
+
+Definition shl' (x: int) (y: Int.int): int :=
+  repr (Z.shiftl (unsigned x) (Int.unsigned y)).
+Definition shru' (x: int) (y: Int.int): int :=
+  repr (Z.shiftr (unsigned x) (Int.unsigned y)).
+Definition shr' (x: int) (y: Int.int): int :=
+  repr (Z.shiftr (signed x) (Int.unsigned y)).
+
+Lemma bits_shl':
+  forall x y i,
+  0 <= i < zwordsize ->
+  testbit (shl' x y) i =
+  if zlt i (Int.unsigned y) then false else testbit x (i - Int.unsigned y).
+Proof.
+  intros. unfold shl'. rewrite testbit_repr; auto. 
+  destruct (zlt i (Int.unsigned y)). 
+  apply Z.shiftl_spec_low. auto.
+  apply Z.shiftl_spec_high. omega. omega.
+Qed.
+
+Lemma bits_shru':
+  forall x y i,
+  0 <= i < zwordsize ->
+  testbit (shru' x y) i =
+  if zlt (i + Int.unsigned y) zwordsize then testbit x (i + Int.unsigned y) else false.
+Proof.
+  intros. unfold shru'. rewrite testbit_repr; auto. 
+  rewrite Z.shiftr_spec. fold (testbit x (i + Int.unsigned y)).
+  destruct (zlt (i + Int.unsigned y) zwordsize).
+  auto.
+  apply bits_above; auto. 
+  omega.
+Qed.
+
+Lemma bits_shr':
+  forall x y i,
+  0 <= i < zwordsize ->
+  testbit (shr' x y) i =
+  testbit x (if zlt (i + Int.unsigned y) zwordsize then i + Int.unsigned y else zwordsize - 1).
+Proof.
+  intros. unfold shr'. rewrite testbit_repr; auto. 
+  rewrite Z.shiftr_spec. apply bits_signed. 
+  generalize (Int.unsigned_range y); omega.
+  omega.
+Qed.
+
+(** Decomposing 64-bit ints as pairs of 32-bit ints *)
+
+Definition loword (n: int) : Int.int := Int.repr (unsigned n).
+
+Definition hiword (n: int) : Int.int := Int.repr (unsigned (shru n (repr Int.zwordsize))).
+
+Definition ofwords (hi lo: Int.int) : int :=
+  or (shl (repr (Int.unsigned hi)) (repr Int.zwordsize)) (repr (Int.unsigned lo)).
+
+Lemma bits_loword:
+  forall n i, 0 <= i < Int.zwordsize -> Int.testbit (loword n) i = testbit n i.
+Proof.
+  intros. unfold loword. rewrite Int.testbit_repr; auto. 
+Qed.
+
+Lemma bits_hiword:
+  forall n i, 0 <= i < Int.zwordsize -> Int.testbit (hiword n) i = testbit n (i + Int.zwordsize).
+Proof.
+  intros. unfold hiword. rewrite Int.testbit_repr; auto.
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  fold (testbit (shru n (repr Int.zwordsize)) i). rewrite bits_shru.
+  change (unsigned (repr Int.zwordsize)) with Int.zwordsize.
+  apply zlt_true. omega. omega. 
+Qed.
+
+Lemma bits_ofwords:
+  forall hi lo i, 0 <= i < zwordsize ->
+  testbit (ofwords hi lo) i =
+  if zlt i Int.zwordsize then Int.testbit lo i else Int.testbit hi (i - Int.zwordsize).
+Proof.
+  intros. unfold ofwords. rewrite bits_or; auto. rewrite bits_shl; auto. 
+  change (unsigned (repr Int.zwordsize)) with Int.zwordsize. 
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  destruct (zlt i Int.zwordsize).
+  rewrite testbit_repr; auto. 
+  rewrite !testbit_repr; auto.
+  fold (Int.testbit lo i). rewrite Int.bits_above. apply orb_false_r. auto. 
+  omega.
+Qed.
+
+Lemma lo_ofwords:
+  forall hi lo, loword (ofwords hi lo) = lo.
+Proof.
+  intros. apply Int.same_bits_eq; intros. 
+  rewrite bits_loword; auto. rewrite bits_ofwords. apply zlt_true. omega. 
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega.
+Qed.
+
+Lemma hi_ofwords:
+  forall hi lo, hiword (ofwords hi lo) = hi.
+Proof.
+  intros. apply Int.same_bits_eq; intros. 
+  rewrite bits_hiword; auto. rewrite bits_ofwords.
+  rewrite zlt_false. f_equal. omega. omega. 
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega.
+Qed.
+
+Lemma ofwords_recompose:
+  forall n, ofwords (hiword n) (loword n) = n.
+Proof.
+  intros. apply same_bits_eq; intros. rewrite bits_ofwords; auto. 
+  destruct (zlt i Int.zwordsize). 
+  apply bits_loword. omega. 
+  rewrite bits_hiword. f_equal. omega. 
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega.
+Qed.
+
+Lemma ofwords_add:
+  forall lo hi, ofwords hi lo = repr (Int.unsigned hi * two_p 32 + Int.unsigned lo).
+Proof.
+  intros. unfold ofwords. rewrite shifted_or_is_add. 
+  apply eqm_samerepr. apply eqm_add. apply eqm_mult. 
+  apply eqm_sym; apply eqm_unsigned_repr.
+  apply eqm_refl. 
+  apply eqm_sym; apply eqm_unsigned_repr.
+  change Int.zwordsize with 32; change zwordsize with 64; omega.
+  rewrite unsigned_repr. generalize (Int.unsigned_range lo). intros [A B]. exact B. 
+  assert (Int.max_unsigned < max_unsigned) by (compute; auto).
+  generalize (Int.unsigned_range_2 lo); omega.
+Qed.
+
+Lemma ofwords_add':
+  forall lo hi, unsigned (ofwords hi lo) = Int.unsigned hi * two_p 32 + Int.unsigned lo.
+Proof.
+  intros. rewrite ofwords_add. apply unsigned_repr.
+  generalize (Int.unsigned_range hi) (Int.unsigned_range lo). 
+  change (two_p 32) with Int.modulus.
+  change Int.modulus with 4294967296.
+  change max_unsigned with 18446744073709551615.
+  omega.
+Qed.
+
+(** Expressing 64-bit operations in terms of 32-bit operations *)
+
+Lemma decompose_bitwise_binop:
+  forall f f64 f32 xh xl yh yl,
+  (forall x y i, 0 <= i < zwordsize -> testbit (f64 x y) i = f (testbit x i) (testbit y i)) ->
+  (forall x y i, 0 <= i < Int.zwordsize -> Int.testbit (f32 x y) i = f (Int.testbit x i) (Int.testbit y i)) ->
+  f64 (ofwords xh xl) (ofwords yh yl) = ofwords (f32 xh yh) (f32 xl yl).
+Proof.
+  intros. apply Int64.same_bits_eq; intros.
+  rewrite H by auto. rewrite ! bits_ofwords by auto.
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  destruct (zlt i Int.zwordsize); rewrite H0 by omega; auto.
+Qed.
+
+Lemma decompose_and:
+  forall xh xl yh yl,
+  and (ofwords xh xl) (ofwords yh yl) = ofwords (Int.and xh yh) (Int.and xl yl).
+Proof.
+  intros. apply decompose_bitwise_binop with andb.
+  apply bits_and. apply Int.bits_and.
+Qed.
+
+Lemma decompose_or:
+  forall xh xl yh yl,
+  or (ofwords xh xl) (ofwords yh yl) = ofwords (Int.or xh yh) (Int.or xl yl).
+Proof.
+  intros. apply decompose_bitwise_binop with orb.
+  apply bits_or. apply Int.bits_or.
+Qed.
+
+Lemma decompose_xor:
+  forall xh xl yh yl,
+  xor (ofwords xh xl) (ofwords yh yl) = ofwords (Int.xor xh yh) (Int.xor xl yl).
+Proof.
+  intros. apply decompose_bitwise_binop with xorb.
+  apply bits_xor. apply Int.bits_xor.
+Qed.
+
+Lemma decompose_not:
+  forall xh xl,
+  not (ofwords xh xl) = ofwords (Int.not xh) (Int.not xl).
+Proof.
+  intros. unfold not, Int.not. rewrite <- decompose_xor. f_equal. 
+  apply (Int64.eq_spec mone (ofwords Int.mone Int.mone)).
+Qed.
+
+Lemma decompose_shl_1:
+  forall xh xl y,
+  0 <= Int.unsigned y < Int.zwordsize ->
+  shl' (ofwords xh xl) y =
+  ofwords (Int.or (Int.shl xh y) (Int.shru xl (Int.sub Int.iwordsize y)))
+          (Int.shl xl y).
+Proof.
+  intros.
+  assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y).
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+    rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. }
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  apply Int64.same_bits_eq; intros.
+  rewrite bits_shl' by auto. symmetry. rewrite bits_ofwords by auto.
+  destruct (zlt i Int.zwordsize). rewrite Int.bits_shl by omega. 
+  destruct (zlt i (Int.unsigned y)). auto. 
+  rewrite bits_ofwords by omega. rewrite zlt_true by omega. auto.
+  rewrite zlt_false by omega. rewrite bits_ofwords by omega. 
+  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. 
+  rewrite Int.bits_shru by omega. rewrite H0.
+  destruct (zlt (i - Int.unsigned y) (Int.zwordsize)).
+  rewrite zlt_true by omega. rewrite zlt_true by omega.
+  rewrite orb_false_l. f_equal. omega. 
+  rewrite zlt_false by omega. rewrite zlt_false by omega. 
+  rewrite orb_false_r. f_equal. omega.
+Qed.
+
+Lemma decompose_shl_2:
+  forall xh xl y,
+  Int.zwordsize <= Int.unsigned y < zwordsize ->
+  shl' (ofwords xh xl) y =
+  ofwords (Int.shl xl (Int.sub y Int.iwordsize)) Int.zero.
+Proof.
+  intros.
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize).
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+    rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. }
+  apply Int64.same_bits_eq; intros.
+  rewrite bits_shl' by auto. symmetry. rewrite bits_ofwords by auto.
+  destruct (zlt i Int.zwordsize). rewrite zlt_true by omega. apply Int.bits_zero.
+  rewrite Int.bits_shl by omega. 
+  destruct (zlt i (Int.unsigned y)).
+  rewrite zlt_true by omega. auto. 
+  rewrite zlt_false by omega. 
+  rewrite bits_ofwords by omega. rewrite zlt_true by omega. f_equal. omega. 
+Qed.
+
+Lemma decompose_shru_1:
+  forall xh xl y,
+  0 <= Int.unsigned y < Int.zwordsize ->
+  shru' (ofwords xh xl) y =
+  ofwords (Int.shru xh y)
+          (Int.or (Int.shru xl y) (Int.shl xh (Int.sub Int.iwordsize y))).
+Proof.
+  intros.
+  assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y).
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+    rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. }
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  apply Int64.same_bits_eq; intros.
+  rewrite bits_shru' by auto. symmetry. rewrite bits_ofwords by auto.
+  destruct (zlt i Int.zwordsize).
+  rewrite zlt_true by omega. 
+  rewrite bits_ofwords by omega.
+  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. 
+  rewrite Int.bits_shru by omega. rewrite H0.
+  destruct (zlt (i + Int.unsigned y) (Int.zwordsize)).
+  rewrite zlt_true by omega.
+  rewrite orb_false_r. auto.
+  rewrite zlt_false by omega. 
+  rewrite orb_false_l. f_equal. omega.
+  rewrite Int.bits_shru by omega. 
+  destruct (zlt (i + Int.unsigned y) zwordsize).
+  rewrite bits_ofwords by omega. 
+  rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. 
+  rewrite zlt_false by omega. auto.
+Qed.
+
+Lemma decompose_shru_2:
+  forall xh xl y,
+  Int.zwordsize <= Int.unsigned y < zwordsize ->
+  shru' (ofwords xh xl) y =
+  ofwords Int.zero (Int.shru xh (Int.sub y Int.iwordsize)).
+Proof.
+  intros.
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize).
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+    rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. }
+  apply Int64.same_bits_eq; intros.
+  rewrite bits_shru' by auto. symmetry. rewrite bits_ofwords by auto.
+  destruct (zlt i Int.zwordsize).
+  rewrite Int.bits_shru by omega. rewrite H1.
+  destruct (zlt (i + Int.unsigned y) zwordsize).
+  rewrite zlt_true by omega. rewrite bits_ofwords by omega. 
+  rewrite zlt_false by omega. f_equal; omega. 
+  rewrite zlt_false by omega. auto.
+  rewrite zlt_false by omega. apply Int.bits_zero.
+Qed.
+
+Lemma decompose_shr_1:
+  forall xh xl y,
+  0 <= Int.unsigned y < Int.zwordsize ->
+  shr' (ofwords xh xl) y =
+  ofwords (Int.shr xh y)
+          (Int.or (Int.shru xl y) (Int.shl xh (Int.sub Int.iwordsize y))).
+Proof.
+  intros.
+  assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y).
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+    rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. }
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  apply Int64.same_bits_eq; intros.
+  rewrite bits_shr' by auto. symmetry. rewrite bits_ofwords by auto.
+  destruct (zlt i Int.zwordsize).
+  rewrite zlt_true by omega. 
+  rewrite bits_ofwords by omega.
+  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. 
+  rewrite Int.bits_shru by omega. rewrite H0.
+  destruct (zlt (i + Int.unsigned y) (Int.zwordsize)).
+  rewrite zlt_true by omega.
+  rewrite orb_false_r. auto.
+  rewrite zlt_false by omega. 
+  rewrite orb_false_l. f_equal. omega.
+  rewrite Int.bits_shr by omega. 
+  destruct (zlt (i + Int.unsigned y) zwordsize).
+  rewrite bits_ofwords by omega. 
+  rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. 
+  rewrite zlt_false by omega. rewrite bits_ofwords by omega. 
+  rewrite zlt_false by omega. f_equal.
+Qed.
+
+Lemma decompose_shr_2:
+  forall xh xl y,
+  Int.zwordsize <= Int.unsigned y < zwordsize ->
+  shr' (ofwords xh xl) y =
+  ofwords (Int.shr xh (Int.sub Int.iwordsize Int.one))
+          (Int.shr xh (Int.sub y Int.iwordsize)).
+Proof.
+  intros.
+  assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
+  assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize).
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+    rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. }
+  apply Int64.same_bits_eq; intros.
+  rewrite bits_shr' by auto. symmetry. rewrite bits_ofwords by auto.
+  destruct (zlt i Int.zwordsize).
+  rewrite Int.bits_shr by omega. rewrite H1.
+  destruct (zlt (i + Int.unsigned y) zwordsize).
+  rewrite zlt_true by omega. rewrite bits_ofwords by omega. 
+  rewrite zlt_false by omega. f_equal; omega. 
+  rewrite zlt_false by omega. rewrite bits_ofwords by omega. 
+  rewrite zlt_false by omega. auto.
+  rewrite Int.bits_shr by omega. 
+  change (Int.unsigned (Int.sub Int.iwordsize Int.one)) with (Int.zwordsize - 1).
+  destruct (zlt (i + Int.unsigned y) zwordsize);
+  rewrite bits_ofwords by omega.
+  symmetry. rewrite zlt_false by omega. f_equal. 
+  destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega.
+  symmetry. rewrite zlt_false by omega. f_equal. 
+  destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega.
+Qed.
+
+Remark eqm_mul_2p32:
+  forall x y, Int.eqm x y -> eqm (x * two_p 32) (y * two_p 32).
+Proof.
+  intros. destruct H as [k EQ]. exists k. rewrite EQ.
+  change Int.modulus with (two_p 32). 
+  change modulus with (two_p 32 * two_p 32).
+  ring.
+Qed.
+
+Lemma decompose_add:
+  forall xh xl yh yl,
+  add (ofwords xh xl) (ofwords yh yl) =
+  ofwords (Int.add (Int.add xh yh) (Int.add_carry xl yl Int.zero))
+          (Int.add xl yl).
+Proof.
+  intros. symmetry. rewrite ofwords_add. rewrite add_unsigned.
+  apply eqm_samerepr. 
+  rewrite ! ofwords_add'. rewrite (Int.unsigned_add_carry xl yl). 
+  set (cc := Int.add_carry xl yl Int.zero).
+  set (Xl := Int.unsigned xl); set (Xh := Int.unsigned xh);
+  set (Yl := Int.unsigned yl); set (Yh := Int.unsigned yh).
+  change Int.modulus with (two_p 32).
+  replace (Xh * two_p 32 + Xl + (Yh * two_p 32 + Yl))
+     with ((Xh + Yh) * two_p 32 + (Xl + Yl)) by ring.
+  replace (Int.unsigned (Int.add (Int.add xh yh) cc) * two_p 32 +
+              (Xl + Yl - Int.unsigned cc * two_p 32))
+     with ((Int.unsigned (Int.add (Int.add xh yh) cc) - Int.unsigned cc) * two_p 32
+           + (Xl + Yl)) by ring.
+  apply eqm_add. 2: apply eqm_refl. apply eqm_mul_2p32.
+  replace (Xh + Yh) with ((Xh + Yh + Int.unsigned cc) - Int.unsigned cc) by ring.
+  apply Int.eqm_sub. 2: apply Int.eqm_refl.
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. 
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. 
+Qed.
+
+Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y).
+
+Lemma decompose_mul:
+  forall xh xl yh yl,
+  mul (ofwords xh xl) (ofwords yh yl) =
+  ofwords (Int.add (Int.add (hiword (mul' xl yl)) (Int.mul xl yh)) (Int.mul xh yl))
+          (loword (mul' xl yl)).
+Proof.
+  intros. 
+  set (pl := loword (mul' xl yl)); set (ph := hiword (mul' xl yl)).
+  assert (EQ0: unsigned (mul' xl yl) = Int.unsigned ph * two_p 32 + Int.unsigned pl).
+  { rewrite <- (ofwords_recompose (mul' xl yl)). apply ofwords_add'. }
+  symmetry. rewrite ofwords_add. unfold mul. rewrite !ofwords_add'.
+  set (XL := Int.unsigned xl); set (XH := Int.unsigned xh);
+  set (YL := Int.unsigned yl); set (YH := Int.unsigned yh).
+  set (PH := Int.unsigned ph) in *. set (PL := Int.unsigned pl) in *.
+  transitivity (repr (((PH + XL * YH) + XH * YL) * two_p 32 + PL)).
+  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. 
+  apply eqm_mul_2p32.
+  rewrite Int.add_unsigned. apply Int.eqm_unsigned_repr_l. apply Int.eqm_add.
+  rewrite Int.add_unsigned. apply Int.eqm_unsigned_repr_l. apply Int.eqm_add.
+  apply Int.eqm_refl.
+  unfold Int.mul. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
+  unfold Int.mul. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
+  transitivity (repr (unsigned (mul' xl yl) + (XL * YH + XH * YL) * two_p 32)).
+  rewrite EQ0. f_equal. ring.
+  transitivity (repr ((XL * YL + (XL * YH + XH * YL) * two_p 32))).
+  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. 
+  unfold mul'. apply eqm_unsigned_repr_l. apply eqm_refl.
+  transitivity (repr (0 + (XL * YL + (XL * YH + XH * YL) * two_p 32))).
+  rewrite Zplus_0_l; auto. 
+  transitivity (repr (XH * YH * (two_p 32 * two_p 32) + (XL * YL + (XL * YH + XH * YL) * two_p 32))).
+  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. 
+  change (two_p 32 * two_p 32) with modulus. exists (- XH * YH). ring. 
+  f_equal. ring. 
+Qed.
+
+End Int64.
 
 Notation int64 := Int64.int.
 
diff --git a/lib/Lattice.v b/lib/Lattice.v
index c4b55e9..3fc0d4c 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -747,3 +747,103 @@ Lemma ge_lub_right: forall x y, ge (lub x y) y.
 Proof. destruct x; destruct y; compute; tauto. Qed.
 
 End LBoolean.
+
+(** * Option semi-lattice *)
+
+(** This lattice adds a top element (represented by [None]) to a given
+  semi-lattice (whose elements are injected via [Some]). *)
+
+Module LOption(L: SEMILATTICE) <: SEMILATTICE_WITH_TOP.
+
+Definition t: Type := option L.t.
+
+Definition eq (x y: t) : Prop :=
+  match x, y with
+  | None, None => True
+  | Some x1, Some y1 => L.eq x1 y1
+  | _, _ => False
+  end.
+
+Lemma eq_refl: forall x, eq x x.
+Proof.
+  unfold eq; intros; destruct x. apply L.eq_refl. auto.
+Qed.
+
+Lemma eq_sym: forall x y, eq x y -> eq y x.
+Proof.
+  unfold eq; intros; destruct x; destruct y; auto. apply L.eq_sym; auto.
+Qed.
+
+Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
+Proof.
+  unfold eq; intros; destruct x; destruct y; destruct z; auto.
+  eapply L.eq_trans; eauto.
+  contradiction.
+Qed.
+
+Definition beq (x y: t) : bool :=
+  match x, y with
+  | None, None => true
+  | Some x1, Some y1 => L.beq x1 y1
+  | _, _ => false
+  end.
+
+Lemma beq_correct: forall x y, beq x y = true -> eq x y.
+Proof.
+  unfold beq, eq; intros; destruct x; destruct y.
+  apply L.beq_correct; auto.
+  discriminate. discriminate. auto.
+Qed.
+
+Definition ge (x y: t) : Prop :=
+  match x, y with
+  | None, _ => True
+  | _, None => False
+  | Some x1, Some y1 => L.ge x1 y1
+  end.
+
+Lemma ge_refl: forall x y, eq x y -> ge x y.
+Proof.
+  unfold eq, ge; intros; destruct x; destruct y.
+  apply L.ge_refl; auto.
+  auto. elim H. auto.
+Qed.
+
+Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+Proof.
+  unfold ge; intros; destruct x; destruct y; destruct z; auto.
+  eapply L.ge_trans; eauto. contradiction.
+Qed.
+
+Definition bot : t := Some L.bot.
+
+Lemma ge_bot: forall x, ge x bot.
+Proof.
+  unfold ge, bot; intros. destruct x; auto. apply L.ge_bot.
+Qed.
+
+Definition lub (x y: t) : t :=
+  match x, y with
+  | None, _ => None
+  | _, None => None
+  | Some x1, Some y1 => Some (L.lub x1 y1)
+  end.
+
+Lemma ge_lub_left: forall x y, ge (lub x y) x.
+Proof.
+  unfold ge, lub; intros; destruct x; destruct y; auto. apply L.ge_lub_left.
+Qed.
+
+Lemma ge_lub_right: forall x y, ge (lub x y) y.
+Proof.
+  unfold ge, lub; intros; destruct x; destruct y; auto. apply L.ge_lub_right.
+Qed.
+
+Definition top : t := None.
+
+Lemma ge_top: forall x, ge top x.
+Proof.
+  unfold ge, top; intros. auto.
+Qed.
+
+End LOption.
diff --git a/lib/Maps.v b/lib/Maps.v
index f667ea4..ddb0c33 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -377,23 +377,18 @@ Module PTree <: TREE.
       end.
 
     Lemma bempty_correct:
-      forall m, bempty m = true -> forall x, get x m = None.
+      forall m, bempty m = true <-> (forall x, get x m = None).
     Proof.
-      induction m; simpl; intros. 
-      change (@Leaf A) with (empty A). apply gempty.
-      destruct o. congruence. destruct (andb_prop _ _ H). 
+      induction m; simpl.
+      split; intros. apply gleaf. auto.
+      destruct o; split; intros.
+      congruence.
+      generalize (H xH); simpl; congruence.
+      destruct (andb_prop _ _ H). rewrite IHm1 in H0. rewrite IHm2 in H1.
       destruct x; simpl; auto.
-    Qed.
-
-    Lemma bempty_complete:
-      forall m, (forall x, get x m = None) -> bempty m = true.
-    Proof.
-      induction m; simpl; intros.
-      auto.
-      destruct o. generalize (H xH); simpl; congruence.
-      rewrite IHm1. rewrite IHm2. auto. 
-      intros; apply (H (xI x)).
-      intros; apply (H (xO x)).
+      apply andb_true_intro; split. 
+      apply IHm1. intros; apply (H (xO x)).
+      apply IHm2. intros; apply (H (xI x)).
     Qed.
 
     Lemma beq_correct:
@@ -406,38 +401,23 @@ Module PTree <: TREE.
        | _, _ => False
        end).
     Proof.
-      intros; split.
-    - (* beq = true -> exteq *)
-      revert m1 m2. induction m1; destruct m2; simpl.
-      intros; red; intros. change (@Leaf A) with (empty A). 
-      repeat rewrite gempty. auto.
-      destruct o; intro. congruence. 
-      red; intros. change (@Leaf A) with (empty A). rewrite gempty.
-      rewrite bempty_correct. auto. assumption. 
-      destruct o; intro. congruence. 
-      red; intros. change (@Leaf A) with (empty A). rewrite gempty.
-      rewrite bempty_correct. auto. assumption. 
-      destruct o; destruct o0; simpl; intro; try congruence.
-      destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). 
-      destruct x; simpl.
-      apply IHm1_2; auto. apply IHm1_1; auto. auto. 
-      destruct (andb_prop _ _ H).
-      red; intros. destruct x; simpl.
-      apply IHm1_2; auto. apply IHm1_1; auto.
-      auto.
-    - (* exteq -> beq = true *)
-      revert m1 m2. induction m1; destruct m2; simpl; intros. 
-      auto.
-      change (bempty (Node m2_1 o m2_2) = true).
-      apply bempty_complete. intros. generalize (H x). rewrite gleaf.
-      destruct (get x (Node m2_1 o m2_2)); tauto. 
-      change (bempty (Node m1_1 o m1_2) = true).
-      apply bempty_complete. intros. generalize (H x). rewrite gleaf.
-      destruct (get x (Node m1_1 o m1_2)); tauto.
-      apply andb_true_intro. split. apply andb_true_intro. split. 
-      generalize (H xH); simpl. destruct o; destruct o0; auto.
-      apply IHm1_1. intros. apply (H (xO x)). 
-      apply IHm1_2. intros. apply (H (xI x)). 
+      induction m1; intros.
+    - simpl. rewrite bempty_correct. split; intros.
+      rewrite gleaf. rewrite H. auto.
+      generalize (H x). rewrite gleaf. destruct (get x m2); tauto. 
+    - destruct m2.
+      + unfold beq. rewrite bempty_correct. split; intros.
+        rewrite H. rewrite gleaf. auto.
+        generalize (H x). rewrite gleaf. destruct (get x (Node m1_1 o m1_2)); tauto.
+      + simpl. split; intros.
+        * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
+          rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. 
+          destruct x; simpl. apply H1. apply H3.
+          destruct o; destruct o0; auto || congruence.
+        * apply andb_true_intro. split. apply andb_true_intro. split.
+          generalize (H xH); simpl. destruct o; destruct o0; tauto. 
+          apply IHm1_1. intros; apply (H (xO x)).
+          apply IHm1_2. intros; apply (H (xI x)).
     Qed.
 
   End BOOLEAN_EQUALITY.
@@ -559,7 +539,7 @@ Module PTree <: TREE.
 
   Section COMBINE.
 
-  Variable A B C: Type.
+  Variables A B C: Type.
   Variable f: option A -> option B -> option C.
   Hypothesis f_none_none: f None None = None.
 
@@ -646,45 +626,53 @@ Module PTree <: TREE.
      auto. 
   Qed.
 
-    Fixpoint xelements (A : Type) (m : t A) (i : positive) {struct m}
-             : list (positive * A) :=
+    Fixpoint xelements (A : Type) (m : t A) (i : positive) 
+                       (k: list (positive * A)) {struct m}
+                       : list (positive * A) :=
       match m with
-      | Leaf => nil
+      | Leaf => k
       | Node l None r =>
-          (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH)))
+          xelements l (append i (xO xH)) (xelements r (append i (xI xH)) k)
       | Node l (Some x) r =>
-          (xelements l (append i (xO xH)))
-          ++ ((i, x) :: xelements r (append i (xI xH)))
+          xelements l (append i (xO xH))
+            ((i, x) :: xelements r (append i (xI xH)) k)
       end.
 
-  (* Note: function [xelements] above is inefficient.  We should apply
-     deforestation to it, but that makes the proofs even harder. *)
 
-  Definition elements A (m : t A) := xelements m xH.
+  Definition elements (A: Type) (m : t A) := xelements m xH nil.
+
+    Lemma xelements_incl:
+      forall (A: Type) (m: t A) (i : positive) k x,
+      In x k -> In x (xelements m i k).
+    Proof.
+      induction m; intros; simpl.
+      auto.
+      destruct o.
+      apply IHm1. simpl; right; auto.
+      auto.
+    Qed.
 
     Lemma xelements_correct:
-      forall (A: Type) (m: t A) (i j : positive) (v: A),
-      get i m = Some v -> In (append j i, v) (xelements m j).
+      forall (A: Type) (m: t A) (i j : positive) (v: A) k,
+      get i m = Some v -> In (append j i, v) (xelements m j k).
     Proof.
       induction m; intros.
        rewrite (gleaf A i) in H; congruence.
        destruct o; destruct i; simpl; simpl in H.
-        rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
-          apply IHm2; auto.
-        rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
-        rewrite append_neutral_r; apply in_or_app; injection H;
-          intro EQ; rewrite EQ; right; apply in_eq.
-        rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto.
-        rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
-        congruence.
+        rewrite append_assoc_1. apply xelements_incl. right. auto.
+        rewrite append_assoc_0. auto. 
+        inv H. apply xelements_incl. left. rewrite append_neutral_r; auto.
+        rewrite append_assoc_1. apply xelements_incl. auto. 
+        rewrite append_assoc_0. auto. 
+        inv H.
     Qed.
 
   Theorem elements_correct:
     forall (A: Type) (m: t A) (i: positive) (v: A),
     get i m = Some v -> In (i, v) (elements m).
   Proof.
-    intros A m i v H.
-    exact (xelements_correct m i xH H).
+    intros A m i v H. 
+    exact (xelements_correct m i xH nil H).
   Qed.
 
     Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A :=
@@ -695,6 +683,13 @@ Module PTree <: TREE.
       | _, _ => None
       end.
 
+    Lemma xget_diag :
+      forall (A : Type) (i : positive) (m1 m2 : t A) (o : option A),
+      xget i i (Node m1 o m2) = o.
+    Proof.
+      induction i; intros; simpl; auto.
+    Qed.
+
     Lemma xget_left :
       forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
       xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v.
@@ -703,122 +698,26 @@ Module PTree <: TREE.
       destruct i; congruence.
     Qed.
 
-    Lemma xelements_ii :
-      forall (A: Type) (m: t A) (i j : positive) (v: A),
-      In (xI i, v) (xelements m (xI j)) -> In (i, v) (xelements m j).
-    Proof.
-      induction m.
-       simpl; auto.
-       intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H);
-         apply in_or_app.
-        left; apply IHm1; auto.
-        right; destruct (in_inv H0).
-         injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq.
-         apply in_cons; apply IHm2; auto.
-        left; apply IHm1; auto.
-        right; apply IHm2; auto.
-    Qed.
-
-    Lemma xelements_io :
-      forall (A: Type) (m: t A) (i j : positive) (v: A),
-      ~In (xI i, v) (xelements m (xO j)).
-    Proof.
-      induction m.
-       simpl; auto.
-       intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
-        apply (IHm1 _ _ _ H0).
-        destruct (in_inv H0).
-         congruence.
-         apply (IHm2 _ _ _ H1).
-        apply (IHm1 _ _ _ H0).
-        apply (IHm2 _ _ _ H0).
-    Qed.
-
-    Lemma xelements_oo :
-      forall (A: Type) (m: t A) (i j : positive) (v: A),
-      In (xO i, v) (xelements m (xO j)) -> In (i, v) (xelements m j).
-    Proof.
-      induction m.
-       simpl; auto.
-       intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H);
-         apply in_or_app.
-        left; apply IHm1; auto.
-        right; destruct (in_inv H0).
-         injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq.
-         apply in_cons; apply IHm2; auto.
-        left; apply IHm1; auto.
-        right; apply IHm2; auto.
-    Qed.
-
-    Lemma xelements_oi :
-      forall (A: Type) (m: t A) (i j : positive) (v: A),
-      ~In (xO i, v) (xelements m (xI j)).
-    Proof.
-      induction m.
-       simpl; auto.
-       intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
-        apply (IHm1 _ _ _ H0).
-        destruct (in_inv H0).
-         congruence.
-         apply (IHm2 _ _ _ H1).
-        apply (IHm1 _ _ _ H0).
-        apply (IHm2 _ _ _ H0).
-    Qed.
-
-    Lemma xelements_ih :
-      forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A),
-      In (xI i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m2 xH).
-    Proof.
-      destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
-        absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto.
-        destruct (in_inv H0).
-         congruence.
-         apply xelements_ii; auto.
-        absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto.
-        apply xelements_ii; auto.
-    Qed.
-
-    Lemma xelements_oh :
-      forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A),
-      In (xO i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m1 xH).
-    Proof.
-      destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
-        apply xelements_oo; auto.
-        destruct (in_inv H0).
-         congruence.
-         absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto.
-        apply xelements_oo; auto.
-        absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto.
-    Qed.
-
-    Lemma xelements_hi :
-      forall (A: Type) (m: t A) (i : positive) (v: A),
-      ~In (xH, v) (xelements m (xI i)).
+    Lemma xget_right :
+      forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
+      xget i (append j (xI xH)) m2 = Some v -> xget i j (Node m1 o m2) = Some v.
     Proof.
-      induction m; intros.
-       simpl; auto.
-       destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
-        generalize H0; apply IHm1; auto.
-        destruct (in_inv H0).
-         congruence.
-         generalize H1; apply IHm2; auto.
-        generalize H0; apply IHm1; auto.
-        generalize H0; apply IHm2; auto.
+      induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
+      destruct i; congruence.
     Qed.
 
-    Lemma xelements_ho :
-      forall (A: Type) (m: t A) (i : positive) (v: A),
-      ~In (xH, v) (xelements m (xO i)).
+    Lemma xelements_complete:
+      forall (A: Type) (m: t A) (i j : positive) (v: A) k,
+      In (i, v) (xelements m j k) -> xget i j m = Some v \/ In (i, v) k.
     Proof.
-      induction m; intros.
-       simpl; auto.
-       destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
-        generalize H0; apply IHm1; auto.
-        destruct (in_inv H0).
-         congruence.
-         generalize H1; apply IHm2; auto.
-        generalize H0; apply IHm1; auto.
-        generalize H0; apply IHm2; auto.
+      induction m; simpl; intros.
+      auto.
+      destruct o. 
+      edestruct IHm1; eauto. left; apply xget_left; auto.
+      destruct H0. inv H0. left; apply xget_diag. 
+      edestruct IHm2; eauto. left; apply xget_right; auto.
+      edestruct IHm1; eauto. left; apply xget_left; auto.
+      edestruct IHm2; eauto. left; apply xget_right; auto.
     Qed.
 
     Lemma get_xget_h :
@@ -827,89 +726,50 @@ Module PTree <: TREE.
       destruct i; simpl; auto.
     Qed.
 
-    Lemma xelements_complete:
-      forall (A: Type) (i j : positive) (m: t A) (v: A),
-      In (i, v) (xelements m j) -> xget i j m = Some v.
-    Proof.
-      induction i; simpl; intros; destruct j; simpl.
-       apply IHi; apply xelements_ii; auto.
-       absurd (In (xI i, v) (xelements m (xO j))); auto; apply xelements_io.
-       destruct m.
-        simpl in H; tauto.
-        rewrite get_xget_h. apply IHi. apply (xelements_ih _ _ _ _ _ H).
-       absurd (In (xO i, v) (xelements m (xI j))); auto; apply xelements_oi.
-       apply IHi; apply xelements_oo; auto.
-       destruct m.
-        simpl in H; tauto.
-        rewrite get_xget_h. apply IHi. apply (xelements_oh _ _ _ _ _ H).
-       absurd (In (xH, v) (xelements m (xI j))); auto; apply xelements_hi.
-       absurd (In (xH, v) (xelements m (xO j))); auto; apply xelements_ho.
-       destruct m.
-        simpl in H; tauto.
-        destruct o; simpl in H; destruct (in_app_or _ _ _ H).
-         absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho.
-         destruct (in_inv H0).
-          congruence.
-          absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi.
-         absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho.
-         absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi.
-    Qed.
-
   Theorem elements_complete:
     forall (A: Type) (m: t A) (i: positive) (v: A),
     In (i, v) (elements m) -> get i m = Some v.
   Proof.
-    intros A m i v H.
-    unfold elements in H.
-    rewrite get_xget_h.
-    exact (xelements_complete i xH m v H).
+    intros A m i v H. unfold elements in H.
+    edestruct xelements_complete; eauto. 
+    rewrite get_xget_h. auto. 
+    contradiction.
   Qed.
 
   Lemma in_xelements:
-    forall (A: Type) (m: t A) (i k: positive) (v: A),
-    In (k, v) (xelements m i) ->
-    exists j, k = append i j.
+    forall (A: Type) (m: t A) (i k: positive) (v: A) l,
+    In (k, v) (xelements m i l) ->
+    (exists j, k = append i j) \/ In (k, v) l.
   Proof.
     induction m; simpl; intros.
-    tauto.
-    assert (k = i \/ In (k, v) (xelements m1 (append i 2))
-                  \/ In (k, v) (xelements m2 (append i 3))).
-      destruct o.
-      elim (in_app_or _ _ _ H); simpl; intuition.
-      replace k with i. tauto. congruence.
-      elim (in_app_or _ _ _ H); simpl; intuition.
-    elim H0; intro.
-    exists xH. rewrite append_neutral_r. auto.
-    elim H1; intro.
-    elim (IHm1 _ _ _ H2). intros k1 EQ. rewrite EQ.
-    rewrite <- append_assoc_0. exists (xO k1); auto.
-    elim (IHm2 _ _ _ H2). intros k1 EQ. rewrite EQ.
-    rewrite <- append_assoc_1. exists (xI k1); auto.
+    auto.
+    destruct o.
+    edestruct IHm1 as [[j EQ] | IN]; eauto.
+    rewrite <- append_assoc_0 in EQ. left; econstructor; eauto. 
+    destruct IN.
+    inv H0. left; exists xH; symmetry; apply append_neutral_r.
+    edestruct IHm2 as [[j EQ] | IN]; eauto.
+    rewrite <- append_assoc_1 in EQ. left; econstructor; eauto. 
+    edestruct IHm1 as [[j EQ] | IN]; eauto.
+    rewrite <- append_assoc_0 in EQ. left; econstructor; eauto. 
+    edestruct IHm2 as [[j EQ] | IN']; eauto.
+    rewrite <- append_assoc_1 in EQ. left; econstructor; eauto.
   Qed.
 
-  Definition xkeys (A: Type) (m: t A) (i: positive) :=
-    List.map (@fst positive A) (xelements m i).
+  Definition xkeys (A: Type) (m: t A) (i: positive) (l: list (positive * A)) :=
+    List.map (@fst positive A) (xelements m i l).
 
   Lemma in_xkeys:
-    forall (A: Type) (m: t A) (i k: positive),
-    In k (xkeys m i) ->
-    exists j, k = append i j.
+    forall (A: Type) (m: t A) (i k: positive) l,
+    In k (xkeys m i l) ->
+    (exists j, k = append i j) \/ In k (List.map fst l).
   Proof.
-    unfold xkeys; intros. 
-    elim (list_in_map_inv _ _ _ H). intros [k1 v1] [EQ IN].
-    simpl in EQ; subst k1. apply in_xelements with A m v1. auto.
-  Qed.
-
-  Remark list_append_cons_norepet:
-    forall (A: Type) (l1 l2: list A) (x: A),
-    list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
-    ~In x l1 -> ~In x l2 ->
-    list_norepet (l1 ++ x :: l2).
-  Proof.
-    intros. apply list_norepet_append_commut. simpl; constructor.
-    red; intros. elim (in_app_or _ _ _ H4); intro; tauto.
-    apply list_norepet_append; auto. 
-    apply list_disjoint_sym; auto.
+    unfold xkeys; intros.
+    exploit list_in_map_inv; eauto. intros [[k1 v1] [EQ IN]].
+    simpl in EQ; subst k1.
+    exploit in_xelements; eauto. intros [EX | IN'].
+    auto.
+    right. change k with (fst (k, v1)). apply List.in_map; auto.
   Qed.
 
   Lemma append_injective:
@@ -922,44 +782,52 @@ Module PTree <: TREE.
   Qed.
 
   Lemma xelements_keys_norepet:
-    forall (A: Type) (m: t A) (i: positive),
-    list_norepet (xkeys m i).
+    forall (A: Type) (m: t A) (i: positive) l,
+    (forall k v, get k m = Some v -> ~In (append i k) (List.map fst l)) ->
+    list_norepet (List.map fst l) ->
+    list_norepet (xkeys m i l).
   Proof.
-    induction m; unfold xkeys; simpl; fold xkeys; intros.
-    constructor.
-    assert (list_disjoint (xkeys m1 (append i 2)) (xkeys m2 (append i 3))).
-      red; intros; red; intro. subst y. 
-      elim (in_xkeys _ _ _ H); intros j1 EQ1.
-      elim (in_xkeys _ _ _ H0); intros j2 EQ2.
-      rewrite EQ1 in EQ2. 
-      rewrite <- append_assoc_0 in EQ2. 
-      rewrite <- append_assoc_1 in EQ2. 
-      generalize (append_injective _ _ _ EQ2). congruence.
-    assert (forall (m: t A) j,
-            j = 2%positive \/ j = 3%positive ->
-            ~In i (xkeys m (append i j))).
-      intros; red; intros. 
-      elim (in_xkeys _ _ _ H1); intros k EQ.
-      assert (EQ1: append i xH = append (append i j) k).
-        rewrite append_neutral_r. auto.
-      elim H0; intro; subst j;
-      try (rewrite <- append_assoc_0 in EQ1);
-      try (rewrite <- append_assoc_1 in EQ1);
-      generalize (append_injective _ _ _ EQ1); congruence.
-    destruct o; rewrite list_append_map; simpl;
-    change (List.map (@fst positive A) (xelements m1 (append i 2)))
-      with (xkeys m1 (append i 2));
-    change (List.map (@fst positive A) (xelements m2 (append i 3)))
-      with (xkeys m2 (append i 3)).
-    apply list_append_cons_norepet; auto. 
-    apply list_norepet_append; auto.
+    unfold xkeys; induction m; simpl; intros.
+    auto.
+    destruct o.
+    apply IHm1. 
+    intros; red; intros IN. rewrite <- append_assoc_0 in IN. simpl in IN; destruct IN.
+    exploit (append_injective i k~0 xH). rewrite append_neutral_r. auto.
+    congruence.
+    exploit in_xkeys; eauto. intros [[j EQ] | IN]. 
+    rewrite <- append_assoc_1 in EQ. exploit append_injective; eauto. congruence.
+    elim (H (xO k) v); auto.
+    simpl. constructor. 
+    red; intros IN. exploit in_xkeys; eauto. intros [[j EQ] | IN'].
+    rewrite <- append_assoc_1 in EQ. 
+    exploit (append_injective i j~1 xH). rewrite append_neutral_r. auto. congruence.
+    elim (H xH a). auto. rewrite append_neutral_r. auto.
+    apply IHm2; auto. intros. rewrite <- append_assoc_1. eapply H; eauto. 
+    apply IHm1. 
+    intros; red; intros IN. rewrite <- append_assoc_0 in IN.
+    exploit in_xkeys; eauto. intros [[j EQ] | IN']. 
+    rewrite <- append_assoc_1 in EQ. exploit append_injective; eauto. congruence.
+    elim (H (xO k) v); auto.
+    apply IHm2; auto. intros. rewrite <- append_assoc_1. eapply H; eauto. 
   Qed.
 
   Theorem elements_keys_norepet:
     forall (A: Type) (m: t A), 
     list_norepet (List.map (@fst elt A) (elements m)).
   Proof.
-    intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet.
+    intros. change (list_norepet (xkeys m 1 nil)). apply xelements_keys_norepet.
+    intros; red; intros. elim H0. constructor.
+  Qed.
+
+  Remark xelements_empty:
+    forall (A: Type) (m: t A) i l, (forall i, get i m = None) -> xelements m i l = l.
+  Proof.
+    induction m; simpl; intros. 
+    auto.
+    destruct o. generalize (H xH); simpl; congruence. 
+    rewrite IHm1. apply IHm2. 
+    intros. apply (H (xI i0)).
+    intros. apply (H (xO i0)).
   Qed.
 
   Theorem elements_canonical_order:
@@ -971,48 +839,48 @@ Module PTree <: TREE.
       (elements m) (elements n).
   Proof.
     intros until R.
-    assert (forall m n j,
+    assert (forall m n j l1 l2,
     (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
     (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
     list_forall2
       (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
-      (xelements m j) (xelements n j)).
-    induction m; induction n; intros; simpl.
-    constructor.
-    destruct o. exploit (H0 xH). simpl. reflexivity. simpl. intros [x [P Q]]. congruence.
-    change (@nil (positive*A)) with ((@nil (positive * A))++nil).
-    apply list_forall2_app.
-    apply IHn1.
-    intros. rewrite gleaf in H1. congruence.
-    intros. exploit (H0 (xO i)). simpl; eauto. rewrite gleaf. intros [x [P Q]]. congruence.
-    apply IHn2.
-    intros. rewrite gleaf in H1. congruence.
-    intros. exploit (H0 (xI i)). simpl; eauto. rewrite gleaf. intros [x [P Q]]. congruence.
-    destruct o. exploit (H xH). simpl. reflexivity. simpl. intros [x [P Q]]. congruence.
-    change (@nil (positive*B)) with (xelements (@Leaf B) (append j 2) ++ (xelements (@Leaf B) (append j 3))).
-    apply list_forall2_app.
-    apply IHm1.
-    intros. exploit (H (xO i)). simpl; eauto. rewrite gleaf. intros [y [P Q]]. congruence.
-    intros. rewrite gleaf in H1. congruence.
-    apply IHm2.
-    intros. exploit (H (xI i)). simpl; eauto. rewrite gleaf. intros [y [P Q]]. congruence.
-    intros. rewrite gleaf in H1. congruence.
-    exploit (IHm1 n1 (append j 2)). 
-    intros. exploit (H (xO i)). simpl; eauto. simpl. auto.
-    intros. exploit (H0 (xO i)). simpl; eauto. simpl; auto.
-    intro REC1.
-    exploit (IHm2 n2 (append j 3)). 
-    intros. exploit (H (xI i)). simpl; eauto. simpl. auto.
-    intros. exploit (H0 (xI i)). simpl; eauto. simpl; auto.
-    intro REC2.
-    destruct o; destruct o0.
-    apply list_forall2_app; auto. constructor; auto. 
-    simpl; split; auto. exploit (H xH). simpl; eauto. simpl. intros [y [P Q]]. congruence.
-    exploit (H xH). simpl; eauto. simpl. intros [y [P Q]]; congruence.
-    exploit (H0 xH). simpl; eauto. simpl. intros [x [P Q]]; congruence.
-    apply list_forall2_app; auto.
-
-    unfold elements; auto.
+      l1 l2 ->
+    list_forall2
+      (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
+      (xelements m j l1) (xelements n j l2)).
+  {
+    induction m; simpl; intros.
+    rewrite xelements_empty. auto. 
+    intros. destruct (get i n) eqn:E; auto. exploit H0; eauto. 
+    intros [x [P Q]]. rewrite gleaf in P; congruence.
+    destruct o. 
+    destruct n. exploit (H xH a); auto. simpl. intros [y [P Q]]; congruence.
+    exploit (H xH a); auto. intros [y [P Q]]. simpl in P. subst o. 
+    simpl. apply IHm1. 
+    intros i x. exact (H (xO i) x). 
+    intros i x. exact (H0 (xO i) x).
+    constructor. simpl; auto. 
+    apply IHm2. 
+    intros i x. exact (H (xI i) x). 
+    intros i x. exact (H0 (xI i) x).
+    auto.
+    destruct n. simpl. 
+    rewrite ! xelements_empty. auto.
+    intros. destruct (get i m2) eqn:E; auto. exploit (H (xI i)); eauto.
+    rewrite gleaf. intros [y [P Q]]; congruence.
+    intros. destruct (get i m1) eqn:E; auto. exploit (H (xO i)); eauto.
+    rewrite gleaf. intros [y [P Q]]; congruence.
+    destruct o. 
+    exploit (H0 xH); simpl; eauto. intros [y [P Q]]; congruence.
+    simpl. apply IHm1. 
+    intros i x. exact (H (xO i) x). 
+    intros i x. exact (H0 (xO i) x).
+    apply IHm2. 
+    intros i x. exact (H (xI i) x). 
+    intros i x. exact (H0 (xI i) x).
+    auto.
+  }
+    intros. apply H. auto. auto. constructor.
   Qed.
 
   Theorem elements_extensional:
@@ -1045,19 +913,15 @@ Module PTree <: TREE.
     xfold f xH m v.
 
   Lemma xfold_xelements:
-    forall (A B: Type) (f: B -> positive -> A -> B) m i v,
-    xfold f i m v =
-    List.fold_left (fun a p => f a (fst p) (snd p))
-                   (xelements m i)
-                   v.
+    forall (A B: Type) (f: B -> positive -> A -> B) m i v l,
+    List.fold_left (fun a p => f a (fst p) (snd p)) l (xfold f i m v) =
+    List.fold_left (fun a p => f a (fst p) (snd p)) (xelements m i l) v.
   Proof.
     induction m; intros.
     simpl. auto.
-    simpl. destruct o.
-    rewrite fold_left_app. simpl. 
-    rewrite IHm1. apply IHm2. 
-    rewrite fold_left_app. simpl.
-    rewrite IHm1. apply IHm2.
+    destruct o; simpl.
+    rewrite <- IHm1. simpl. rewrite <- IHm2. auto.
+    rewrite <- IHm1. rewrite <- IHm2. auto. 
   Qed.
 
   Theorem fold_spec:
@@ -1065,7 +929,7 @@ Module PTree <: TREE.
     fold f m v =
     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
   Proof.
-    intros. unfold fold, elements. apply xfold_xelements. 
+    intros. unfold fold, elements. rewrite <- xfold_xelements. auto. 
   Qed.
 
 End PTree.
diff --git a/lib/Ordered.v b/lib/Ordered.v
index f52a7ef..026671a 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -48,6 +48,36 @@ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.
 
 End OrderedPositive.
 
+(** The ordered type of integers *)
+
+Module OrderedZ <: OrderedType.
+
+Definition t := Z.
+Definition eq (x y: t) := x = y.
+Definition lt := Zlt.
+
+Lemma eq_refl : forall x : t, eq x x.
+Proof (@refl_equal t). 
+Lemma eq_sym : forall x y : t, eq x y -> eq y x.
+Proof (@sym_equal t).
+Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+Proof (@trans_equal t).
+Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+Proof Zlt_trans.
+Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+Proof. unfold lt, eq, t; intros. omega. Qed. 
+Lemma compare : forall x y : t, Compare lt eq x y.
+Proof.
+  intros. destruct (Z.compare x y) as [] eqn:E.
+  apply EQ. red. apply Z.compare_eq_iff. assumption.
+  apply LT. assumption.
+  apply GT. apply Z.compare_gt_iff. assumption.
+Defined.
+
+Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := zeq.
+
+End OrderedZ.
+
 (** The ordered type of machine integers *)
 
 Module OrderedInt <: OrderedType.