abstractbb: support of removing useless computations

1 files changed, 186 insertions, 179 deletions

diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v
index bf45d11a..6646d4f5 100644
--- a/mppa_k1c/abstractbb/DepTreeTheory.v
+++ b/mppa_k1c/abstractbb/DepTreeTheory.v
@@ -1,13 +1,13 @@
 (** Dependency Trees of Abstract Basic Blocks
 
-with a purely-functional-but-exponential equivalence test.
+with a purely-functional-but-exponential test.
 
 *)
 
 
 Require Setoid. (* in order to rewrite <-> *)
 Require Export AbstractBasicBlocksDef.
-
+Require Import List.
 
 Module Type PseudoRegDictionary.
 
@@ -39,12 +39,9 @@ Module DepTree (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R
 
 Export L.
 Export LP.
-Local Open Scope list.
 
 Section DEPTREE.
 
-Variable ge: genv.
-
 (** Dependency Trees of these "bblocks" 
 
 NB: each tree represents the successive computations in one given resource
@@ -54,102 +51,90 @@ NB: each tree represents the successive computations in one given resource
 Inductive tree :=
   | Tname (x:R.t)
   | Top (o: op) (l: list_tree)
-  | Terase (new old:tree) (* assignment in the resource: [new] replaces [old] *)
 with list_tree :=
   | Tnil: list_tree
   | Tcons (t:tree) (l:list_tree):  list_tree
   .
 
 
-Fixpoint tree_eval (t: tree) (m: mem): option value :=
+Fixpoint tree_eval (ge: genv) (t: tree) (m: mem): option value :=
   match t with
   | Tname x => Some (m x)
   | Top o l =>
-     match list_tree_eval l m with
+     match list_tree_eval ge l m with
      | Some v => op_eval ge o v
      | _ => None
      end
-  | Terase new old =>
-     (* NB: we simply check whether the old computations has aborted *)
-     match tree_eval old m with
-     | Some _ => tree_eval new m
-     | _ => None
-     end
   end
-with list_tree_eval (l: list_tree) (m: mem) {struct l}: option (list value) :=
+with list_tree_eval ge (l: list_tree) (m: mem) {struct l}: option (list value) :=
   match l with
   | Tnil => Some nil
   | Tcons t l' => 
-    match (tree_eval t m), (list_tree_eval l' m) with
+    match (tree_eval ge t m), (list_tree_eval ge l' m) with
     | Some v, Some lv => Some (v::lv)
     | _, _ => None
     end
   end.
 
-Definition deps:= Dict.t tree.
-
-Definition deps_get (d:deps) x := 
+Definition deps_get (d:Dict.t tree) x := 
    match Dict.get d x with 
    | None => Tname x
    | Some t => t
    end.
 
-Lemma set_spec_eq d x t:
-  deps_get (Dict.set d x t) x = t.
-Proof.
-  unfold deps_get; rewrite Dict.set_spec_eq; simpl; auto.
-Qed.
-
-Lemma set_spec_diff d x y t:
-  x <> y -> deps_get (Dict.set d x t) y = deps_get d y.
-Proof.
- unfold deps_get; intros; rewrite Dict.set_spec_diff; simpl; auto.
-Qed.
-
-Lemma empty_spec x: deps_get Dict.empty x = Tname x.
-Proof.
- unfold deps_get; rewrite Dict.empty_spec; simpl; auto.
-Qed.
-
-Hint Rewrite set_spec_eq empty_spec: dict_rw. 
-
-Fixpoint exp_tree (e: exp) (d old: deps): tree :=
+Fixpoint exp_tree (e: exp) d old: tree :=
   match e with
   | PReg x => deps_get d x
   | Op o le => Top o (list_exp_tree le d old)
   | Old e => exp_tree e old old
   end
-with list_exp_tree (le: list_exp) (d old: deps): list_tree :=
+with list_exp_tree (le: list_exp) d old: list_tree :=
   match le with
   | Enil => Tnil
   | Econs e le' => Tcons (exp_tree e d old) (list_exp_tree le' d old)
   | LOld le => list_exp_tree le old old
   end.
 
-Definition failsafe (t: tree): bool :=
-  match t with
-  | Tname x => true
-  | Top o Tnil => is_constant o
-  | _ => false
-  end.
+Record deps:= {pre: genv -> mem -> Prop; post: Dict.t tree}.
+
+Coercion post: deps >-> Dict.t.
+
+Definition deps_eval ge (d: deps) x (m:mem) :=
+  tree_eval ge (deps_get d x) m.
+
+Definition deps_set (d:deps) x (t:tree) := 
+  {| pre:=(fun ge m => (deps_eval ge d x m) <> None /\ (d.(pre) ge m));
+     post:=Dict.set d x t |}.
+
+Definition deps_empty := {| pre:=fun _ _ => True; post:=Dict.empty |}.
+
+Variable ge: genv.
+
+Lemma set_spec_eq d x t m:
+ deps_eval ge (deps_set d x t) x m = tree_eval ge t m.
+Proof.
+  unfold deps_eval, deps_set, deps_get; simpl; rewrite Dict.set_spec_eq; simpl; auto. 
+Qed.
 
-Local Hint Resolve is_constant_correct.
+Lemma set_spec_diff d x y t m:
+  x <> y -> deps_eval ge (deps_set d x t) y m = deps_eval ge d y m.
+Proof.
+  intros; unfold deps_eval, deps_set, deps_get; simpl; rewrite Dict.set_spec_diff; simpl; auto. 
+Qed.
 
-Lemma failsafe_correct (t: tree) m: failsafe t = true -> tree_eval t m <> None.
+Lemma deps_eval_empty x m: deps_eval ge deps_empty x m = Some (m x).
 Proof.
-  destruct t; simpl; try congruence.
-  destruct l; simpl; try congruence.
-  eauto.
+  unfold deps_eval, deps_get; rewrite Dict.empty_spec; simpl; auto.
 Qed.
 
+Hint Rewrite set_spec_eq deps_eval_empty: dict_rw. 
+
 Fixpoint inst_deps (i: inst) (d old: deps): deps :=
   match i with
   | nil => d
   | (x, e)::i' =>
-     let t0:=deps_get d x in
-     let t1:=exp_tree e d old in
-     let v':=if failsafe t0 then t1 else (Terase t1 t0) in
-     inst_deps i' (Dict.set d x v') old
+     let t:=exp_tree e d old in
+     inst_deps i' (deps_set d x t) old
   end.
 
 Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps :=
@@ -160,214 +145,236 @@ Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps :=
      bblock_deps_rec p' d'
   end.
 
+Local Hint Resolve deps_eval_empty.
+
 Definition bblock_deps: bblock -> deps
- := fun p => bblock_deps_rec p Dict.empty.
+ := fun p => bblock_deps_rec p deps_empty.
+
+Lemma inst_deps_pre_monotonic i old: forall d m,
+  (pre (inst_deps i d old) ge m) -> (pre d ge m).
+Proof.
+  induction i as [|[y e] i IHi]; simpl; auto.
+  intros d a H; generalize (IHi _ _ H); clear H IHi.
+  unfold deps_set; simpl; intuition.
+Qed.
 
-(** Main Result: the [bblock_deps_equiv] theorem states that bblocks with the same dependencies are observationaly equals *)
+Lemma bblock_deps_pre_monotonic p: forall d m,
+  (pre (bblock_deps_rec p d) ge m) -> (pre d ge m).
+Proof.
+  induction p as [|i p' IHp']; simpl; eauto.
+  intros d a H; eapply inst_deps_pre_monotonic; eauto.
+Qed.
 
+Local Hint Resolve inst_deps_pre_monotonic bblock_deps_pre_monotonic.
 
 Lemma tree_eval_exp e od m0 old:
-  (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
-  forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-   (tree_eval (exp_tree e d od) m0) = exp_eval ge e m1 old.
+  (forall x, deps_eval ge od x m0 = Some (old x)) ->
+  forall d m1,
+   (forall x, deps_eval ge d x m0 = Some (m1 x)) ->
+    tree_eval ge (exp_tree e d od) m0 = exp_eval ge e m1 old.
 Proof.
-  intro H.
-  induction e using exp_mut with (P0:=fun l => forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval (list_exp_tree l d od) m0 = list_exp_eval ge l m1 old); simpl; auto.
+  unfold deps_eval in * |- *; intro H.
+  induction e using exp_mut with
+    (P0:=fun l => forall (d:deps) m1, (forall x, tree_eval ge (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval ge (list_exp_tree l d od) m0 = list_exp_eval ge l m1 old);
+  simpl; auto.
   - intros; erewrite IHe; eauto.
-  - intros; erewrite IHe, IHe0; eauto. 
+  - intros. erewrite IHe, IHe0; eauto. 
 Qed.
 
-Lemma tree_eval_inst_abort i m0 x old: forall d,
-    tree_eval (deps_get d x) m0 = None ->
-    tree_eval (deps_get (inst_deps i d old) x) m0 = None.
+Lemma inst_deps_abort i m0 x old: forall d,
+    pre (inst_deps i d old) ge m0 ->
+    deps_eval ge d x m0 = None ->
+    deps_eval ge (inst_deps i d old) x m0 = None.
 Proof.
   induction i as [|[y e] i IHi]; simpl; auto.
-  intros d H; erewrite IHi; eauto. clear IHi.
+  intros d VALID H; erewrite IHi; eauto. clear IHi.
   destruct (R.eq_dec x y).
   * subst; autorewrite with dict_rw.
-    generalize (failsafe_correct (deps_get d y) m0).
-    destruct (failsafe (deps_get d y)); simpl; intuition try congruence.
-    rewrite H; simpl. auto.
-  * rewrite! set_spec_diff; auto.
+    generalize (inst_deps_pre_monotonic _ _ _ _ VALID); clear VALID.
+    unfold deps_set; simpl; intuition congruence.
+  * rewrite set_spec_diff; auto.
 Qed.
 
-Lemma tree_eval_abort p m0 x: forall d,
-    tree_eval (deps_get d x) m0 = None ->
-    tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None.
+Lemma block_deps_rec_abort p m0 x: forall d,
+    pre (bblock_deps_rec p d) ge m0 ->
+    deps_eval ge d x m0 = None ->
+    deps_eval ge (bblock_deps_rec p d) x m0 = None.
 Proof.
   induction p; simpl; auto.
-  intros d H; erewrite IHp; eauto. clear IHp.
-  eapply tree_eval_inst_abort; eauto.
+  intros d VALID H; erewrite IHp; eauto. clear IHp.
+  eapply inst_deps_abort; eauto.
 Qed.
 
-Lemma tree_eval_inst_Some_correct1 i m0 old od: 
-  (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
-  forall (m1 m2: mem) d, 
+Lemma inst_deps_Some_correct1 i m0 old od:
+  (forall x, deps_eval ge od x m0 = Some (old x)) ->
+  forall (m1 m2: mem) (d: deps), 
   inst_run ge i m1 old = Some m2 -> 
-  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-  (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)).
+  (forall x, deps_eval ge d x m0 = Some (m1 x)) ->
+   forall x, deps_eval ge (inst_deps i d od) x m0 = Some (m2 x).
 Proof.
   intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H.
   - inversion_clear H; eauto.
   - intros H0 x0.
-    remember (exp_eval ge e m1 old) as ov.
-    destruct ov.
-    + refine (IHi _ _ _ _ _ _); eauto.
-      clear x0; intros x0.
-      unfold assign; destruct (R.eq_dec x x0).
-      * subst; autorewrite with dict_rw.
-        destruct (failsafe (deps_get d x0)); simpl; try rewrite H0;
-        erewrite tree_eval_exp; eauto.
-      * rewrite set_spec_diff; auto.
-    + inversion H. 
+    destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence.
+    refine (IHi _ _ _ _ _ _); eauto.
+    clear x0; intros x0.
+    unfold assign; destruct (R.eq_dec x x0).
+    * subst; autorewrite with dict_rw.
+      erewrite tree_eval_exp; eauto.
+    * rewrite set_spec_diff; auto.
 Qed.
 
-Local Hint Resolve tree_eval_inst_Some_correct1 tree_eval_abort.
-
-Lemma tree_eval_Some_correct1 p m0: forall (m1 m2: mem) d, 
+Lemma bblocks_deps_rec_Some_correct1 p m0: forall (m1 m2: mem) d, 
  run ge p m1 = Some m2 -> 
-  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-    (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)).
+  (forall x, deps_eval ge d x m0 = Some (m1 x)) ->
+  forall x, deps_eval ge (bblock_deps_rec p d) x m0 = Some (m2 x).
 Proof.
+  Local Hint Resolve inst_deps_Some_correct1.
   induction p as [ | i p]; simpl; intros m1 m2 d H.
   - inversion_clear H; eauto.
   - intros H0 x0.
-    remember (inst_run ge i m1 m1) as om.
-    destruct om.
+    destruct (inst_run ge i m1 m1) eqn: Heqov.
     + refine (IHp _ _ _ _ _ _); eauto.
     + inversion H. 
 Qed.
 
 Lemma bblock_deps_Some_correct1 p m0 m1:
-  run ge p m0 = Some m1
-   -> forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x).
+   run ge p m0 = Some m1
+   -> forall x, deps_eval ge (bblock_deps p) x m0 = Some (m1 x).
 Proof.
-  intros; eapply tree_eval_Some_correct1;
-  intros; autorewrite with dict_rw; simpl; eauto.
+  intros; eapply bblocks_deps_rec_Some_correct1; eauto.
 Qed.
 
-Lemma tree_eval_inst_None_correct i m0 old od: 
-  (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
-  forall m1 d,  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-  inst_run ge i m1 old = None <-> exists x, tree_eval (deps_get (inst_deps i d od) x) m0 = None.
+Lemma inst_deps_None_correct i m0 old od:
+   (forall x, deps_eval ge od x m0 = Some (old x)) ->
+  forall m1 d, pre (inst_deps i d od) ge m0 ->
+   (forall x, deps_eval ge d x m0 = Some (m1 x)) ->
+  inst_run ge i m1 old = None -> exists x, deps_eval ge (inst_deps i d od) x m0 = None.
 Proof.
   intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d.
-  - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate].
-  - intros H0.
-    remember (exp_eval ge e m1 old) as ov.
-    destruct ov.
-    + refine (IHi _ _ _); eauto.
+  - discriminate.
+  - intros VALID H0.
+    destruct (exp_eval ge e m1 old) eqn: Heqov.
+    + refine (IHi _ _ _ _); eauto.
       intros x0; unfold assign; destruct (R.eq_dec x x0).
       * subst; autorewrite with dict_rw. 
-        destruct (failsafe (deps_get d x0)); simpl; try rewrite H0;
         erewrite tree_eval_exp; eauto.
       * rewrite set_spec_diff; auto.
     + intuition.
       constructor 1 with (x:=x); simpl.
-      apply tree_eval_inst_abort.
+      apply inst_deps_abort; auto.
       autorewrite with dict_rw.
-      destruct (failsafe (deps_get d x)); simpl; try rewrite H0;
       erewrite tree_eval_exp; eauto.
 Qed.
 
-
-Lemma tree_eval_None_correct p m0: forall m1 d,
-  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-  run ge p m1 = None <-> exists x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None.
-Proof.
-  induction p as [|i p IHp]; simpl; intros m1 d.
-  - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate].
-  - intros H0.
-    remember (inst_run ge i m1 m1) as om.
-    destruct om.
-    + refine (IHp _ _ _); eauto.
-    + intuition.
-      assert (X: inst_run ge i m1 m1 = None); auto.
-      rewrite tree_eval_inst_None_correct in X; auto.
-      destruct X as [x H1].
-      constructor 1 with (x:=x); simpl; auto.
-Qed.
-
-Lemma bblock_deps_None_correct p m:
-  run ge p m = None <-> exists x, tree_eval (deps_get (bblock_deps p) x) m = None.
-Proof.
-  intros; eapply tree_eval_None_correct.
-  intros; autorewrite with dict_rw; simpl; eauto.
-Qed.
-
-Lemma tree_eval_inst_Some_correct2 i m0 old od: 
-  (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
+Lemma inst_deps_Some_correct2 i m0 old od:
+  (forall x, deps_eval ge od x m0 = Some (old x)) ->
   forall (m1 m2: mem) d, 
-  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-    (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)) ->
-    res_eq (Some m2) (inst_run ge i m1 old).
+  pre (inst_deps i d od) ge m0 ->
+  (forall x, deps_eval ge d x m0 = Some (m1 x)) ->
+  (forall x, deps_eval ge (inst_deps i d od) x m0 = Some (m2 x)) ->
+  res_eq (Some m2) (inst_run ge i m1 old).
 Proof.
   intro X.
-  induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H0.
+  induction i as [|[x e] i IHi]; simpl; intros m1 m2 d VALID H0.
   - intros H; eapply ex_intro; intuition eauto.
     generalize (H0 x); rewrite H.
     congruence.
   - intros H.
-    remember (exp_eval ge e m1 old) as ov.
-    destruct ov.
-    + refine (IHi _ _ _ _ _); eauto.
+    destruct (exp_eval ge e m1 old) eqn: Heqov.
+    + refine (IHi _ _ _ _ _ _); eauto.
       intros x0; unfold assign; destruct (R.eq_dec x x0).
-      * subst; autorewrite with dict_rw.
-        destruct (failsafe (deps_get d x0)); simpl; try rewrite H0;
+      * subst. autorewrite with dict_rw.
         erewrite tree_eval_exp; eauto.
       * rewrite set_spec_diff; auto.
     + generalize (H x).
-      rewrite tree_eval_inst_abort; try discriminate.
+      rewrite inst_deps_abort; discriminate || auto.
       autorewrite with dict_rw. 
-      destruct (failsafe (deps_get d x)); simpl; try rewrite H0;
       erewrite tree_eval_exp; eauto.
 Qed.
 
-Lemma tree_eval_Some_correct2 p m0: forall (m1 m2: mem) d, 
-  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-    (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)) ->
+Lemma bblocks_deps_rec_Some_correct2 p m0: forall (m1 m2: mem) d, 
+  pre (bblock_deps_rec p d) ge m0 ->
+  (forall x, deps_eval ge d x m0 = Some (m1 x)) ->
+  (forall x, deps_eval ge (bblock_deps_rec p d) x m0 = Some (m2 x)) ->
     res_eq (Some m2) (run ge p m1).
 Proof.
-  induction p as [|i p]; simpl; intros m1 m2 d H0.
+  induction p as [|i p]; simpl; intros m1 m2 d VALID H0.
   - intros H; eapply ex_intro; intuition eauto.
     generalize (H0 x); rewrite H.
     congruence.
   - intros H.
-    remember (inst_run ge i m1 m1) as om.
-    destruct om.
-    + refine (IHp _ _ _ _ _); eauto.
-    + assert (X: inst_run ge i m1 m1 = None); auto.
-      rewrite tree_eval_inst_None_correct in X; auto.
+     destruct (inst_run ge i m1 m1) eqn: Heqom.
+    + refine (IHp _ _ _ _ _ _); eauto.
+    + assert (X: exists x, tree_eval ge (deps_get (inst_deps i d d) x) m0 = None).
+      { eapply inst_deps_None_correct; eauto. }
       destruct X as [x H1].
       generalize (H x).
-      rewrite tree_eval_abort; congruence.
+      erewrite block_deps_rec_abort; eauto.
+      congruence.
 Qed.
 
+
 Lemma bblock_deps_Some_correct2 p m0 m1:
-  (forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x))
+  pre (bblock_deps p) ge m0 ->
+  (forall x, deps_eval ge (bblock_deps p) x m0 = Some (m1 x))
   -> res_eq (Some m1) (run ge p m0).
 Proof.
-  intros; eapply tree_eval_Some_correct2; eauto.
-  intros; autorewrite with dict_rw; simpl; eauto.
+  intros; eapply bblocks_deps_rec_Some_correct2; eauto.
+Qed.
+
+Lemma inst_valid i m0 old od:
+  (forall x, deps_eval ge od x m0 = Some (old x)) ->
+  forall (m1 m2: mem) (d: deps), 
+  pre d ge m0 ->
+  inst_run ge i m1 old = Some m2 ->
+  (forall x, deps_eval ge d x m0 = Some (m1 x)) ->
+   pre (inst_deps i d od) ge m0.
+Proof.
+  induction i as [|[x e] i IHi]; simpl; auto.
+  intros Hold m1 m2 d VALID0 H Hm1.
+  destruct (exp_eval ge e m1 old) eqn: Heq; simpl; try congruence.
+  eapply IHi; eauto.
+  + unfold deps_set in * |- *; simpl. 
+    rewrite Hm1; intuition congruence.
+  + intros x0. unfold assign; destruct (R.eq_dec x x0).
+    * subst; autorewrite with dict_rw.
+      erewrite tree_eval_exp; eauto.
+    * rewrite set_spec_diff; auto.
+Qed.
+
+
+Lemma block_deps_rec_valid p m0: forall (m1 m2: mem) (d:deps), 
+  pre d ge m0 ->
+  run ge p m1 = Some m2 -> 
+  (forall x, deps_eval ge d x m0 = Some (m1 x)) ->
+  pre (bblock_deps_rec p d) ge m0.
+Proof.
+  Local Hint Resolve inst_valid.
+  induction p as [ | i p]; simpl; intros m1 d H; auto.
+  intros H0 H1.
+  destruct (inst_run ge i m1 m1) eqn: Heqov; eauto.
+  congruence.
 Qed.
 
+Lemma bblock_deps_valid p m0 m1:
+  run ge p m0 = Some m1 ->
+  pre (bblock_deps p) ge m0.
+Proof.
+  intros; eapply block_deps_rec_valid; eauto.
+  unfold deps_empty; simpl. auto.
+Qed.
 
 Theorem bblock_deps_simu p1 p2:
-  (forall x, deps_get (bblock_deps p1) x = deps_get (bblock_deps p2) x)
-   -> bblock_simu ge p1 p2.
+  (forall m, pre (bblock_deps p1) ge m -> pre (bblock_deps p2) ge m) ->
+  (forall m0 x m1, pre (bblock_deps p1) ge m0 -> deps_eval ge (bblock_deps p1) x m0 = Some m1 ->
+                   deps_eval ge (bblock_deps p2) x m0 = Some m1) ->
+   bblock_simu ge p1 p2.
 Proof.
-  intros H m2 DONTFAIL.
-  remember (run ge p1 m2) as om1.
-  destruct om1; simpl.
-  + apply bblock_deps_Some_correct2.
-    intros; rewrite <- H.
-    apply bblock_deps_Some_correct1; auto.
-  + rewrite bblock_deps_None_correct.
-    assert (X: run ge p1 m2 = None); auto.
-    rewrite bblock_deps_None_correct in X.
-    destruct X as [x Hx].
-    rewrite H in Hx.
-    eauto.
+  Local Hint Resolve bblock_deps_valid bblock_deps_Some_correct1.
+  intros INCL EQUIV m DONTFAIL.
+  destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence.
+  eapply bblock_deps_Some_correct2; eauto.
 Qed.
 
 End DEPTREE.