Merge of the newmem branch:

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


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

5 files changed, 583 insertions, 96 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 87b19ca..50535fb 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -23,23 +23,6 @@ Require Export List.
 Require Export Bool.
 Require Import Wf_nat.
 
-(***
-
-(** * Logical axioms *)
-
-(** We use two logical axioms that are not provable in Coq but consistent
-  with the logic: function extensionality and proof irrelevance.
-  These are used in the memory model to show that two memory states
-  that have identical contents are equal. *)
-
-Axiom extensionality:
-  forall (A B: Type) (f g : A -> B),
-  (forall x, f x = g x) -> f = g.
-
-Axiom proof_irrelevance:
-  forall (P: Prop) (p1 p2: P), p1 = p2.
-***)
-  
 (** * Useful tactics *)
 
 Ltac inv H := inversion H; clear H; subst.
@@ -51,7 +34,7 @@ Ltac caseEq name :=
   generalize (refl_equal name); pattern name at -1 in |- *; case name.
 
 Ltac destructEq name :=
-  generalize (refl_equal name); pattern name at -1 in |- *; destruct name; intro.
+  destruct name as []_eqn.
 
 Ltac decEq :=
   match goal with
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 3625845..235b650 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -10,65 +10,88 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* Bounded and unbounded iterators *)
+(** Bounded and unbounded iterators *)
 
 Require Import Axioms.
 Require Import Coqlib.
-Require Import Classical.
-Require Import Max.
+Require Import Wfsimpl.
 
-Module Type ITER.
-Variable iterate
-     : forall A B : Type, (A -> B + A) -> A -> option B.
-Hypothesis iterate_prop
-     : forall (A B : Type) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop),
-       (forall a : A, P a ->
-           match step a with inl b => Q b | inr a' => P a' end) ->
-       forall (a : A) (b : B), iterate A B step a = Some b -> P a -> Q b.
-End ITER.
+(** This modules defines several Coq encodings of a general "while" loop.
+  The loop is presented in functional style as the iteration
+  of a [step] function of type [A -> B + A]:
+<<
+        let rec iterate step a =
+          match step a with
+          | inl b -> b
+          | inr a' -> iterate step a'
+>>
+  This iteration cannot be defined directly in Coq using [Fixpoint],
+  because Coq is a logic of total functions, and therefore we must
+  guarantee termination of the loop.
+*)
 
-Axiom
-  dependent_description' :
-    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
-      (forall x:A,
-          exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
-       sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).
+(** * Terminating iteration *)
 
-(* A constructive implementation using bounded iteration. *)
+(** We first implement the case where termination is guaranteed because
+  the current state [a] decreases at each iteration. *)
 
-Module PrimIter: ITER.
+Module WfIter.
 
 Section ITERATION.
 
 Variables A B: Type.
 Variable step: A -> B + A.
+Variable ord: A -> A -> Prop.
+Hypothesis ord_wf: well_founded ord.
+Hypothesis step_decr: forall a a', step a = inr _ a' -> ord a' a.
 
-(** The [step] parameter represents one step of the iteration.  From a 
-  current iteration state [a: A], it either returns a value of type [B],
-  meaning that iteration is over and that this [B] value is the final
-  result of the iteration, or a value [a' : A] which is the next state
-  of the iteration.
+Definition step_info (a: A) : {b | step a = inl _ b} + {a' | step a = inr _ a' & ord a' a}.
+Proof.
+  caseEq (step a); intros. left; exists b; auto. right; exists a0; auto. 
+Qed.
 
-  The naive way to define the iteration is:
-<<
-Fixpoint iterate (a: A) : B :=
-  match step a with
-  | inl b => b
-  | inr a' => iterate a'
+Definition iterate_F (a: A) (rec: forall a', ord a' a -> B) : B :=
+  match step_info a with
+  | inl (exist b P) => b
+  | inr (exist2 a' P Q) => rec a' Q
   end.
->>
-  However, this is a general recursion, not guaranteed to terminate,
-  and therefore not expressible in Coq.  The standard way to work around
-  this difficulty is to use Noetherian recursion (Coq module [Wf]).
-  This requires that we equip the type [A] with a well-founded ordering [<]
-  (no infinite ascending chains) and we demand that [step] satisfies
-  [step a = inr a' -> a < a'].  For the types [A] that are of interest to us
-  in this development, it is however very painful to define adequate
-  well-founded orderings, even though we know our iterations always
-  terminate.
-
-  Instead, we choose to bound the number of iterations by an arbitrary
-  constant.  [iterate] then becomes a function that can fail,
+
+Definition iterate (a: A) : B := Fix ord_wf iterate_F a.
+
+(** We now prove an invariance property [iterate_prop], similar to the Hoare
+  logic rule for "while" loops. *)
+
+Variable P: A -> Prop.
+Variable Q: B -> Prop.
+
+Hypothesis step_prop:
+  forall a : A, P a ->
+  match step a with inl b => Q b | inr a' => P a' end.
+
+Lemma iterate_prop:
+  forall a, P a -> Q (iterate a).
+Proof.
+  intros a0. pattern a0. apply well_founded_ind with (R := ord). auto.
+  intros. unfold iterate; rewrite unroll_Fix. unfold iterate_F. 
+  destruct (step_info x) as [[b U] | [a' U V]]. 
+  exploit step_prop; eauto. rewrite U; auto.
+  apply H. auto. exploit step_prop; eauto. rewrite U; auto. 
+Qed.
+
+End ITERATION.
+
+End WfIter.
+
+(** * Bounded iteration *)
+
+(** The presentation of iteration shown above is predicated on the existence
+  of a well-founded ordering that decreases at each step of the iteration.
+  In several parts of the CompCert development, it is very painful to define
+  such a well-founded ordering and to prove decrease, even though we know our
+  iterations always terminate.
+
+  In the presentation below, we choose instead to bound the number of iterations
+  by an arbitrary constant.  [iterate] then becomes a function that can fail,
   of type [A -> option B].  The [None] result denotes failure to reach
   a result in the number of iterations prescribed, or, in other terms,
   failure to find a solution to the dataflow problem.  The compiler
@@ -82,6 +105,13 @@ Fixpoint iterate (a: A) : B :=
   course our proofs also cover the failure case and show that 
   nothing bad happens in this hypothetical case either.  *)
 
+Module PrimIter.
+
+Section ITERATION.
+
+Variables A B: Type.
+Variable step: A -> B + A.
+
 Definition num_iterations := 1000000000000%positive.
 
 (** The simple definition of bounded iteration is:
@@ -117,19 +147,7 @@ Definition iter_step (x: positive)
       end
   end.
 
-Definition iter: positive -> A -> option B :=
-  Fix Plt_wf (fun _ => A -> option B) iter_step.
-
-(** We then prove the expected unrolling equations for [iter]. *)
-
-Remark unroll_iter:
-  forall x, iter x = iter_step x (fun y _ => iter y).
-Proof.
-  unfold iter; apply (Fix_eq Plt_wf (fun _ => A -> option B) iter_step).
-  intros. unfold iter_step. apply extensionality. intro s. 
-  case (peq x xH); intro. auto. 
-  rewrite H. auto. 
-Qed.
+Definition iter: positive -> A -> option B := Fix Plt_wf iter_step.
 
 (** The [iterate] function is defined as [iter] up to
     [num_iterations] through the loop. *)
@@ -150,11 +168,12 @@ Lemma iter_prop:
 Proof.
   apply (well_founded_ind Plt_wf 
          (fun p => forall a b, P a -> iter p a = Some b -> Q b)).
-  intros until b. intro. rewrite unroll_iter.
-  unfold iter_step. case (peq x 1); intro. congruence.
-  generalize (step_prop a H0).
-  case (step a); intros. congruence. 
-  apply H with (Ppred x) a0. apply Ppred_Plt; auto. auto. auto.
+  intros. unfold iter in H1. rewrite unroll_Fix in H1. unfold iter_step in H1.
+  destruct (peq x 1). discriminate.
+  specialize (step_prop a H0). 
+  destruct (step a) as [b'|a']_eqn.
+  inv H1. auto.
+  apply H with (Ppred x) a'. apply Ppred_Plt; auto. auto. auto.
 Qed.
 
 Lemma iterate_prop:
@@ -167,11 +186,21 @@ End ITERATION.
 
 End PrimIter.
 
+(** * General iteration *)
+
 (* An implementation using classical logic and unbounded iteration,
   in the style of Yves Bertot's paper, "Extending the Calculus
-  of Constructions with Tarski's fix-point theorem". *)
+  of Constructions with Tarski's fix-point theorem".
 
-Module GenIter: ITER.
+  As in the bounded case, the [iterate] function returns an option type.
+  [None] means that iteration does not terminate.
+  [Some b] means that iteration terminates with the result [b]. *)
+
+Require Import Classical.
+Require Import ClassicalDescription.
+Require Import Max.
+
+Module GenIter.
 
 Section ITERATION.
 
@@ -249,30 +278,29 @@ Proof.
 Qed.
 
 Lemma converges_to_exists_uniquely:
-  forall a, exists b, converges_to a b /\ forall b', converges_to a b' -> b = b'.
+  forall a, exists! b, converges_to a b .
 Proof.
   intro. destruct (converges_to_exists a) as [b CT]. 
   exists b. split. assumption. exact (converges_to_unique _ _ CT).
 Qed.
 
-Definition exists_iterate :=
-  dependent_description' A (fun _ => option B)
-     converges_to converges_to_exists_uniquely.
-
-Definition iterate : A -> option B :=
-  match exists_iterate with existT f P => f end.
+Definition iterate (a: A) : option B :=
+  proj1_sig (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)).
 
 Lemma converges_to_iterate:
   forall a b, converges_to a b -> iterate a = b.
 Proof.
-  intros. unfold iterate. destruct exists_iterate as [f P]. 
-  apply converges_to_unique with a. apply P. auto.
+  intros. unfold iterate. 
+  destruct (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)) as [b' P].
+  simpl. apply converges_to_unique with a; auto.
 Qed.
 
 Lemma iterate_converges_to:
   forall a, converges_to a (iterate a).
 Proof.
-  intros. unfold iterate. destruct exists_iterate as [f P]. apply P.
+  intros. unfold iterate. 
+  destruct (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)) as [b' P].
+  simpl; auto.
 Qed.
 
 (** Invariance property. *)
diff --git a/lib/Maps.v b/lib/Maps.v
index f8d1bd5..255ce44 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -77,6 +77,9 @@ Module Type TREE.
   Hypothesis grspec:
     forall (A: Type) (i j: elt) (m: t A),
     get i (remove j m) = if elt_eq i j then None else get i m.
+  Hypothesis set2:
+    forall (A: Type) (i: elt) (m: t A) (v1 v2: A),
+    set i v2 (set i v1 m) = set i v2 m.
 
   (** Extensional equality between trees. *)
   Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
@@ -302,8 +305,15 @@ Module PTree <: TREE.
      rewrite (IHi m1 v H); congruence.
   Qed.
 
-    Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf.
-    Proof. destruct i; simpl; auto. Qed.
+  Theorem set2:
+    forall (A: Type) (i: elt) (m: t A) (v1 v2: A),
+    set i v2 (set i v1 m) = set i v2 m.
+  Proof.
+    induction i; intros; destruct m; simpl; try (rewrite IHi); auto.
+  Qed.
+
+  Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf.
+  Proof. destruct i; simpl; auto. Qed.
 
   Theorem grs:
     forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None.
@@ -1116,6 +1126,13 @@ Module PMap <: MAP.
     unfold option_map. destruct (PTree.get i (snd m)); auto.
   Qed.
 
+  Theorem set2:
+    forall (A: Type) (i: elt) (x y: A) (m: t A),
+    set i y (set i x m) = set i y m.
+  Proof.
+    intros. unfold set. simpl. decEq. apply PTree.set2.
+  Qed.
+
 End PMap.
 
 (** * An implementation of maps over any type that injects into type [positive] *)
@@ -1178,6 +1195,13 @@ Module IMap(X: INDEXED_TYPE).
     intros. unfold map, get. apply PMap.gmap. 
   Qed.
 
+  Lemma set2:
+    forall (A: Type) (i: elt) (x y: A) (m: t A),
+    set i y (set i x m) = set i y m.
+  Proof.
+    intros. unfold set. apply PMap.set2.
+  Qed.
+
 End IMap.
 
 Module ZIndexed.
@@ -1378,6 +1402,76 @@ Qed.
 
 End TREE_FOLD_IND.
 
+(** A nonnegative measure over trees *)
+
+Section MEASURE.
+
+Variable V: Type.
+
+Definition cardinal (x: T.t V) : nat := List.length (T.elements x).
+
+Remark list_incl_length:
+  forall (A: Type) (l1: list A), list_norepet l1 ->
+  forall (l2: list A), List.incl l1 l2 -> (List.length l1 <= List.length l2)%nat.
+Proof.
+  induction 1; simpl; intros.
+  omega.
+  exploit (List.in_split hd l2). auto with coqlib. intros [l3 [l4 EQ]]. subst l2.
+  assert (length tl <= length (l3 ++ l4))%nat.
+    apply IHlist_norepet. red; intros. 
+    exploit (H1 a); auto with coqlib. 
+    repeat rewrite in_app_iff. simpl. intuition. subst. contradiction.
+  repeat rewrite app_length in *. simpl. omega. 
+Qed.
+
+Remark list_length_incl:
+  forall (A: Type) (l1: list A), list_norepet l1 ->
+  forall l2, List.incl l1 l2 -> List.length l1 = List.length l2 -> List.incl l2 l1.
+Proof.
+  induction 1; simpl; intros.
+  destruct l2; simpl in *. auto with coqlib. discriminate.
+  exploit (List.in_split hd l2). auto with coqlib. intros [l3 [l4 EQ]]. subst l2.
+  assert (incl (l3 ++ l4) tl).
+    apply IHlist_norepet. red; intros. 
+    exploit (H1 a); auto with coqlib. 
+    repeat rewrite in_app_iff. simpl. intuition. subst. contradiction.
+    repeat rewrite app_length in *. simpl in H2. omega. 
+  red; simpl; intros. rewrite in_app_iff in H4; simpl in H4. intuition. 
+Qed.
+
+Remark list_strict_incl_length:
+  forall (A: Type) (l1 l2: list A) (x: A),
+  list_norepet l1 -> List.incl l1 l2 -> ~In x l1 -> In x l2 ->
+  (List.length l1 < List.length l2)%nat.
+Proof.
+  intros. exploit list_incl_length; eauto. intros. 
+  assert (length l1 = length l2 \/ length l1 < length l2)%nat by omega.
+  destruct H4; auto. elim H1. eapply list_length_incl; eauto. 
+Qed.
+
+Remark list_norepet_map:
+  forall (A B: Type) (f: A -> B) (l: list A),
+  list_norepet (List.map f l) -> list_norepet l.
+Proof.
+  induction l; simpl; intros.
+  constructor.
+  inv H. constructor; auto. red; intros; elim H2. apply List.in_map; auto.
+Qed.
+
+Theorem cardinal_remove:
+  forall x m y, T.get x m = Some y -> (cardinal (T.remove x m) < cardinal m)%nat.
+Proof.
+  unfold cardinal; intros. apply list_strict_incl_length with (x := (x, y)).
+  apply list_norepet_map with (f := @fst T.elt V). apply T.elements_keys_norepet.
+  red; intros. destruct a as [x' y']. exploit T.elements_complete; eauto. 
+  rewrite T.grspec. destruct (T.elt_eq x' x); intros; try discriminate.
+  apply T.elements_correct; auto.
+  red; intros. exploit T.elements_complete; eauto. rewrite T.grspec. rewrite dec_eq_true. congruence.
+  apply T.elements_correct; auto.
+Qed.
+
+End MEASURE.
+
 End Tree_Properties.
 
 Module PTree_Properties := Tree_Properties(PTree).
@@ -1386,5 +1480,3 @@ Module PTree_Properties := Tree_Properties(PTree).
 
 Notation "a ! b" := (PTree.get b a) (at level 1).
 Notation "a !! b" := (PMap.get b a) (at level 1).
-
-(* $Id: Maps.v,v 1.12.4.4 2006/01/07 11:46:55 xleroy Exp $ *)
diff --git a/lib/Postorder.v b/lib/Postorder.v
new file mode 100644
index 0000000..fe06da7
--- /dev/null
+++ b/lib/Postorder.v
@@ -0,0 +1,316 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Postorder numbering of a directed graph. *)
+
+Require Import Wellfounded.
+Require Import Coqlib.
+Require Import Maps.
+Require Import Iteration.
+
+(** The graph is presented as a finite map from nodes (of type [positive])
+  to the lists of their successors. *)
+
+Definition node: Type := positive.
+
+Definition graph: Type := PTree.t (list node).
+
+(** The traversal is presented as an iteration that modifies the following state. *)
+
+Record state : Type := mkstate {
+  gr: graph;                    (**r current graph, without already-visited nodes *)
+  wrk: list (node * list node); (**r worklist *)
+  map: PTree.t positive;        (**r current mapping node -> postorder number *)
+  next: positive                (**r number to use for next numbering *)
+}.
+
+Definition init_state (g: graph) (root: node) :=
+  match g!root with
+  | Some succs =>
+     {| gr := PTree.remove root g;
+        wrk := (root, succs) :: nil;
+        map := PTree.empty positive;
+        next := 1%positive |}
+  | None =>
+     {| gr := g;
+        wrk := nil;
+        map := PTree.empty positive;
+        next := 1%positive |}
+  end.
+
+Definition transition (s: state) : PTree.t positive + state :=
+  match s.(wrk) with
+  | nil =>
+      inl _ s.(map)
+  | (x, nil) :: l =>
+      inr _ {| gr := s.(gr); wrk := l; map := PTree.set x s.(next) s.(map); next := Psucc s.(next) |}
+  | (x, y :: succs_x) :: l =>
+      match s.(gr)!y with
+      | None =>
+          inr _ {| gr := s.(gr); wrk := (x, succs_x) :: l; map := s.(map); next := s.(next) |}
+      | Some succs_y =>
+          inr _ {| gr := PTree.remove y s.(gr); wrk := (y, succs_y) :: (x, succs_x) :: l; map := s.(map); next := s.(next) |}
+      end
+  end.
+
+Section POSTORDER.
+
+Variable ginit: graph.
+Variable root: node.
+
+Inductive invariant (s: state) : Prop :=
+  Invariant
+    (* current graph is a subset of ginit *)
+    (SUB: forall x y, s.(gr)!x = Some y -> ginit!x = Some y)
+    (* root is not in current graph *)
+    (ROOT: s.(gr)!root = None)
+    (* mapped nodes have their numbers below next *)
+    (BELOW: forall x y, s.(map)!x = Some y -> Plt y s.(next))
+    (* mapping is injective *)
+    (INJ: forall x1 x2 y, s.(map)!x1 = Some y -> s.(map)!x2 = Some y -> x1 = x2)
+    (* nodes not yet visited have no number *)
+    (REM: forall x y, s.(gr)!x = Some y -> s.(map)!x = None)
+    (* black nodes have no white son *)
+    (COLOR: forall x succs n y,
+            ginit!x = Some succs -> s.(map)!x = Some n -> 
+            In y succs -> s.(gr)!y = None)
+    (* worklist is well-formed *)
+    (WKLIST: forall x l, In (x, l) s.(wrk) ->
+             s.(gr)!x = None /\
+             exists l', ginit!x = Some(l' ++ l)
+                    /\  forall y, In y l' -> s.(gr)!y = None)
+    (* all grey nodes are on the worklist *)
+    (GREY: forall x, ginit!x <> None -> s.(gr)!x = None -> s.(map)!x = None ->
+           exists l, In (x,l) s.(wrk)).
+
+Inductive postcondition (map: PTree.t positive) : Prop :=
+  Postcondition
+    (INJ: forall x1 x2 y, map!x1 = Some y -> map!x2 = Some y -> x1 = x2)
+    (ROOT: ginit!root <> None -> map!root <> None)
+    (SUCCS: forall x succs y, ginit!x = Some succs -> map!x <> None -> In y succs -> ginit!y <> None -> map!y <> None).
+
+Lemma transition_spec:
+  forall s, invariant s -> 
+  match transition s with inr s' => invariant s' | inl m => postcondition m end.
+Proof.
+  intros. inv H. unfold transition. destruct (wrk s) as [ | [x succ_x] l]. 
+  (* finished *)
+  constructor; intros.
+  eauto.
+  caseEq (s.(map)!root); intros. congruence. exploit GREY; eauto. intros [? ?]; contradiction.
+  destruct (s.(map)!x) as []_eqn; try congruence. 
+  destruct (s.(map)!y) as []_eqn; try congruence.
+  exploit COLOR; eauto. intros. exploit GREY; eauto. intros [? ?]; contradiction.
+  (* not finished *)
+  destruct succ_x as [ | y succ_x ].
+  (* all children of x were traversed *)
+  constructor; simpl; intros.
+  (* sub *)
+  eauto.
+  (* root *)
+  eauto.
+  (* below *)
+  rewrite PTree.gsspec in H. destruct (peq x0 x). inv H. 
+  apply Plt_succ.
+  apply Plt_trans_succ. eauto.
+  (* inj *)
+  rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. 
+  destruct (peq x1 x); destruct (peq x2 x); subst.
+  auto.
+  inv H. exploit BELOW; eauto. intros. eelim Plt_strict; eauto.  
+  inv H0. exploit BELOW; eauto. intros. eelim Plt_strict; eauto.
+  eauto.
+  (* rem *)
+  intros. rewrite PTree.gso; eauto. red; intros; subst x0. 
+  exploit (WKLIST x nil); auto with coqlib. intros [A B]. congruence.
+  (* color *)
+  rewrite PTree.gsspec in H0. destruct (peq x0 x). 
+  inv H0.  exploit (WKLIST x nil); auto with coqlib. 
+  intros [A [l' [B C]]]. rewrite app_nil_r in B. 
+  assert (l' = succs) by congruence. subst l'. eauto. 
+  eauto.
+  (* wklist *)
+  apply WKLIST. auto with coqlib.
+  (* grey *)
+  rewrite PTree.gsspec in H1. destruct (peq x0 x). inv H1. 
+  exploit GREY; eauto. intros [l' A]. simpl in A; destruct A.
+  congruence.
+  exists l'; auto.
+
+  (* children y needs traversing *)
+  destruct ((gr s)!y) as [ succs_y | ]_eqn.
+  (* y has children *)
+  constructor; simpl; intros. 
+  (* sub *)
+  rewrite PTree.grspec in H. destruct (PTree.elt_eq x0 y); eauto. inv H.
+  (* root *)
+  rewrite PTree.gro. auto. congruence. 
+  (* below *)
+  eauto.
+  (* inj *)
+  eauto.
+  (* rem *)
+  rewrite PTree.grspec in H. destruct (PTree.elt_eq x0 y); eauto. inv H.
+  (* color *)
+  rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); eauto. 
+  (* wklist *)
+  destruct H. 
+  inv H. split. apply PTree.grs. exists (@nil positive); simpl; intuition. 
+  destruct H.
+  inv H. exploit WKLIST; eauto with coqlib. intros [A [l' [B C]]].
+  split. rewrite PTree.grspec. destruct (PTree.elt_eq x0 y); auto. 
+  exists (l' ++ y :: nil); split. rewrite app_ass. auto. 
+  intros. rewrite in_app_iff in H. simpl in H. intuition. 
+  rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto. 
+  subst y0. apply PTree.grs.
+  exploit (WKLIST x0 l0); eauto with coqlib. intros [A [l' [B C]]].
+  split. rewrite PTree.grspec. destruct (PTree.elt_eq x0 y); auto. 
+  exists l'; split; auto. intros. 
+  rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto.
+  (* grey *)
+  rewrite PTree.grspec in H0. destruct (PTree.elt_eq x0 y) in H0. 
+  subst. exists succs_y; auto with coqlib.
+  exploit GREY; eauto. simpl. intros [l1 A]. destruct A. 
+  inv H2. exists succ_x; auto. 
+  exists l1; auto.
+
+  (* y has no children *)
+  constructor; simpl; intros; eauto.
+  (* wklist *)
+  destruct H. inv H. 
+  exploit (WKLIST x0); eauto with coqlib. intros [A [l' [B C]]].
+  split. auto. exists (l' ++ y :: nil); split. rewrite app_ass; auto. 
+  intros. rewrite in_app_iff in H; simpl in H. intuition. congruence. 
+  eapply WKLIST; eauto with coqlib.
+  (* grey *)
+  exploit GREY; eauto. intros [l1 A]. simpl in A. destruct A.
+  inv H2. exists succ_x; auto.
+  exists l1; auto.
+Qed.
+
+Lemma initial_state_spec:
+  invariant (init_state ginit root).
+Proof.
+  unfold init_state. destruct (ginit!root) as [succs|]_eqn.
+  (* root has succs *)
+  constructor; simpl; intros.
+  (* sub *)
+  rewrite PTree.grspec in H. destruct (PTree.elt_eq x root). inv H. auto.
+  (* root *)
+  apply PTree.grs.
+  (* below *)
+  rewrite PTree.gempty in H; inv H.
+  (* inj *)
+  rewrite PTree.gempty in H; inv H.
+  (* rem *)
+  apply PTree.gempty.
+  (* color *)
+  rewrite PTree.gempty in H0; inv H0.
+  (* wklist *)
+  destruct H; inv H. 
+  split. apply PTree.grs. exists (@nil positive); simpl; tauto.
+  (* grey *)
+  rewrite PTree.grspec in H0. destruct (PTree.elt_eq x root).
+  subst. exists succs; auto. 
+  contradiction.
+
+  (* root has no succs *)
+  constructor; simpl; intros.
+  (* sub *)
+  auto.  
+  (* root *)
+  auto.
+  (* below *)
+  rewrite PTree.gempty in H; inv H.
+  (* inj *)
+  rewrite PTree.gempty in H; inv H.
+  (* rem *)
+  apply PTree.gempty.
+  (* color *)
+  rewrite PTree.gempty in H0; inv H0.
+  (* wklist *)
+  contradiction.
+  (* grey *)
+  contradiction.
+
+Qed.
+
+(** Termination criterion. *)
+
+Fixpoint size_worklist (w: list (positive * list positive)) : nat :=
+  match w with
+  | nil => 0%nat
+  | (x, succs) :: w' => (S (List.length succs) + size_worklist w')%nat
+  end.
+
+Definition lt_state (s1 s2: state) : Prop :=
+  lex_ord lt lt (PTree_Properties.cardinal s1.(gr), size_worklist s1.(wrk))
+                (PTree_Properties.cardinal s2.(gr), size_worklist s2.(wrk)).
+
+Lemma lt_state_wf: well_founded lt_state.
+Proof.
+  set (f := fun s => (PTree_Properties.cardinal s.(gr), size_worklist s.(wrk))).
+  change (well_founded (fun s1 s2 => lex_ord lt lt (f s1) (f s2))).
+  apply wf_inverse_image. 
+  apply wf_lex_ord. 
+  apply lt_wf. apply lt_wf.
+Qed.
+
+Lemma transition_decreases: 
+  forall s s', transition s = inr _ s' -> lt_state s' s.
+Proof.
+  unfold transition, lt_state; intros.
+  destruct (wrk s) as [ | [x succs] l].
+  discriminate.
+  destruct succs as [ | y succs ].
+  inv H. simpl. apply lex_ord_right. omega.
+  destruct ((gr s)!y) as [succs'|]_eqn.
+  inv H. simpl. apply lex_ord_left. eapply PTree_Properties.cardinal_remove; eauto.
+  inv H. simpl. apply lex_ord_right. omega.
+Qed.
+
+End POSTORDER.
+
+Definition postorder (g: graph) (root: node) :=
+  WfIter.iterate _ _ transition lt_state lt_state_wf transition_decreases (init_state g root).
+
+Inductive reachable (g: graph) (root: positive) : positive -> Prop :=
+  | reachable_root:
+      reachable g root root
+  | reachable_succ: forall x succs y,
+      reachable g root x -> g!x = Some succs -> In y succs ->
+      reachable g root y.
+
+Theorem postorder_correct:
+  forall g root,
+  let m := postorder g root in
+  (forall x1 x2 y, m!x1 = Some y -> m!x2 = Some y -> x1 = x2)
+  /\ (forall x, reachable g root x -> g!x <> None -> m!x <> None).
+Proof.
+  intros. 
+  assert (postcondition g root m).
+    unfold m. unfold postorder.
+    apply WfIter.iterate_prop with (P := invariant g root).
+    apply transition_spec. 
+    apply initial_state_spec.
+  inv H.
+  split. auto.
+  induction 1; intros.
+  (* root case *)
+  apply ROOT; auto.
+  (* succ case *)
+  eapply SUCCS; eauto. apply IHreachable. congruence.
+Qed.
+
diff --git a/lib/Wfsimpl.v b/lib/Wfsimpl.v
new file mode 100644
index 0000000..1ed6326
--- /dev/null
+++ b/lib/Wfsimpl.v
@@ -0,0 +1,68 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Defining recursive functions by Noetherian induction.  This is a simplified
+  interface to the [Wf] module of Coq's standard library, where the functions
+  to be defined have non-dependent types, and function extensionality is assumed. *)
+
+Require Import Axioms.
+Require Import Wf.
+Require Import Wf_nat.
+
+Set Implicit Arguments.
+
+Section FIX.
+
+Variables A B: Type.
+Variable R: A -> A -> Prop.
+Hypothesis Rwf: well_founded R.
+Variable F: forall (x: A), (forall (y: A), R y x -> B) -> B.
+
+Definition Fix (x: A) : B := Wf.Fix Rwf (fun (x: A) => B) F x.
+
+Theorem unroll_Fix:
+  forall x, Fix x = F (fun (y: A) (P: R y x) => Fix y).
+Proof.
+  unfold Fix; intros. apply Wf.Fix_eq with (P := fun (x: A) => B). 
+  intros. assert (f = g). apply functional_extensionality_dep; intros.
+  apply functional_extensionality; intros. auto. 
+  subst g; auto.
+Qed.
+
+End FIX.
+
+(** Same, with a nonnegative measure instead of a well-founded ordering *)
+
+Section FIXM.
+
+Variables A B: Type.
+Variable measure: A -> nat.
+Variable F: forall (x: A), (forall (y: A), measure y < measure x -> B) -> B.
+
+Definition Fixm (x: A) : B := Wf.Fix (well_founded_ltof A measure) (fun (x: A) => B) F x.
+
+Theorem unroll_Fixm:
+  forall x, Fixm x = F (fun (y: A) (P: measure y < measure x) => Fixm y).
+Proof.
+  unfold Fixm; intros. apply Wf.Fix_eq with (P := fun (x: A) => B). 
+  intros. assert (f = g). apply functional_extensionality_dep; intros.
+  apply functional_extensionality; intros. auto. 
+  subst g; auto.
+Qed.
+
+End FIXM.
+
+
+