abstractbb: support of removing useless computations

7 files changed, 481 insertions, 299 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.
diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v
index 2e2ad40f..3efe6a36 100644
--- a/mppa_k1c/abstractbb/ImpDep.v
+++ b/mppa_k1c/abstractbb/ImpDep.v
@@ -72,8 +72,6 @@ Hypothesis hC_tree_correct: forall t, WHEN hC_tree t ~> t' THEN pre_data t=data
 Variable hC_list_tree: pre_hashV list_tree -> ?? hashV list_tree.
 Hypothesis hC_list_tree_correct: forall t, WHEN hC_list_tree t ~> t' THEN pre_data t=data t'.
 
-Variable ge: genv.
-
 (* First, we wrap constructors for hashed values !*)
 
 Local Open Scope positive.
@@ -107,19 +105,6 @@ Qed.
 Global Opaque hTop.
 Hint Resolve hTop_correct: wlp.
 
-Definition hTerase (t1 t2: hashV tree) (debug: option pstring): ?? hashV tree :=
-   DO hc <~ hash 3;; 
-   hC_tree {| pre_data:=Terase (data t1) (data t2); 
-              hcodes:=[hc;hid t1; hid t2]; debug_info := debug |}.
-
-Lemma hTerase_correct t1 t2 dbg: 
-  WHEN hTerase t1 t2 dbg ~> t THEN (data t)=(Terase (data t1) (data t2)).
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque hTerase.
-Hint Resolve hTerase_correct: wlp.
-
 Definition hTnil (_: unit): ?? hashV list_tree :=
    hC_list_tree {| pre_data:=Tnil; hcodes := nil; debug_info := None |} .
 
@@ -146,7 +131,9 @@ Hint Resolve hTcons_correct: wlp.
 (* Second, we use these hashed constructors ! *)
 
 
-Definition hdeps:= Dict.t (hashV tree).
+Record hdeps:= {hpre: list (hashV tree); hpost: Dict.t (hashV tree)}.
+
+Coercion hpost: hdeps >-> Dict.t.
 
 (* pseudo deps_get *)
 Definition pdeps_get (d:hdeps) x : tree := 
@@ -169,6 +156,12 @@ Qed.
 Global Opaque hdeps_get.
 Hint Resolve hdeps_get_correct: wlp.
 
+Definition hdeps_valid ge (hd:hdeps) m := forall ht, List.In ht hd.(hpre) -> tree_eval ge (data ht) m <> None.
+
+Definition deps_model ge (d: deps) (hd:hdeps): Prop :=
+     (forall m, hdeps_valid ge hd m <-> pre d ge m)
+  /\ (forall m x, tree_eval ge (pdeps_get hd x) m = deps_eval ge d x m).
+
 Fixpoint hexp_tree (e: exp) (d od: hdeps) (dbg: option pstring) : ?? hashV tree :=
   match e with
   | PReg x => hdeps_get d x dbg
@@ -187,86 +180,95 @@ with hlist_exp_tree (le: list_exp) (d od: hdeps): ?? hashV list_tree :=
   | LOld le => hlist_exp_tree le od od
   end.
 
-Lemma hexp_tree_correct_x e od1 od2:
-  (forall x, pdeps_get od1 x = deps_get od2 x) ->
- forall d1 d2 dbg,
-  (forall x, pdeps_get d1 x = deps_get d2 x) ->
-  WHEN hexp_tree e d1 od1 dbg ~> t THEN data t = exp_tree e d2 od2.
+Lemma hexp_tree_correct_x ge e hod od:
+  deps_model ge od hod ->
+ forall hd d dbg,
+  deps_model ge d hd ->
+  WHEN hexp_tree e hd hod dbg ~> t THEN forall m, tree_eval ge (data t) m  = tree_eval ge (exp_tree e d od) m.
 Proof.
   intro H.
-  induction e using exp_mut with (P0:=fun le =>  forall d1 d2,
-     (forall x, pdeps_get d1 x = deps_get d2 x) ->
-     WHEN hlist_exp_tree le d1 od1 ~> lt THEN data lt = list_exp_tree le d2 od2); simpl; wlp_simplify; congruence.
+  induction e using exp_mut with (P0:=fun le =>  forall d hd,
+     deps_model ge d hd ->
+     WHEN hlist_exp_tree le hd hod ~> lt THEN forall m, list_tree_eval ge (data lt) m = list_tree_eval ge (list_exp_tree le d od) m); 
+     unfold deps_model, deps_eval in * |- * ; simpl; wlp_simplify; try congruence.
+  - rewrite H4, <- H0; simpl; reflexivity.
+  - rewrite H1; simpl; reflexivity.
+  - rewrite H5, <- H0, <- H4; simpl; reflexivity.
 Qed.
 Global Opaque hexp_tree.
 
-Lemma hexp_tree_correct e d1 od1 dbg:
-  WHEN hexp_tree e d1 od1 dbg ~> t THEN forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) -> (forall x, pdeps_get d1 x = deps_get d2 x) -> data t = exp_tree e d2 od2.
+Lemma hexp_tree_correct e hd hod dbg:
+  WHEN hexp_tree e hd hod dbg ~> t THEN forall ge od d m, deps_model ge od hod -> deps_model ge d hd -> tree_eval ge (data t) m = tree_eval ge (exp_tree e d od) m.
 Proof.
-  intros t H od2 d2 H1 H2; apply (hexp_tree_correct_x e od1 od2 H1 d1 d2 dbg H2 t H). 
+  unfold wlp; intros; eapply hexp_tree_correct_x; eauto.
 Qed.
 Hint Resolve hexp_tree_correct: wlp.
 
-Variable debug_assign: R.t -> ?? option pstring.
-
-Fixpoint hinst_deps (i: inst) (d od: hdeps): ?? hdeps :=
-  match i with
-  | nil => RET d
-  | (x, e)::i' =>
-     DO dbg <~ debug_assign x;;
-     DO t0 <~ hdeps_get d x None;;
-     DO v' <~ (if failsafe (data t0) 
-      then 
-        hexp_tree e d od dbg 
-      else
-        DO t1 <~ hexp_tree e d od None;; 
-        hTerase t1 t0 dbg);;
-     hinst_deps i' (Dict.set d x v') od
+Definition failsafe (t: tree): bool :=
+  match t with
+  | Tname x => true
+  | Top o Tnil => is_constant o
+  | _ => false
   end.
 
-Lemma pset_spec_eq d x t:
-  pdeps_get (Dict.set d x t) x = (data t).
-Proof.
-  unfold pdeps_get; rewrite Dict.set_spec_eq; simpl; auto.
-Qed.
+Local Hint Resolve is_constant_correct.
 
-Lemma pset_spec_diff d x y t:
-  x <> y -> pdeps_get (Dict.set d x t) y = pdeps_get d y.
+Lemma failsafe_correct ge (t: tree) m: failsafe t = true -> tree_eval ge t m <> None.
 Proof.
- unfold pdeps_get; intros; rewrite Dict.set_spec_diff; simpl; auto.
+  destruct t; simpl; try congruence.
+  destruct l; simpl; try congruence.
+  eauto.
 Qed.
-
-Lemma pempty_spec x: pdeps_get Dict.empty x = Tname x.
+Local Hint Resolve failsafe_correct.
+
+Definition hdeps_set (d:hdeps) x (t:hashV tree) :=
+     DO ot <~ hdeps_get d x None;;
+     RET {| hpre:=if failsafe (data ot) then d.(hpre) else ot::d.(hpre);
+            hpost:=Dict.set d x t |}.
+
+Lemma hdeps_set_correct hd x ht:
+  WHEN hdeps_set hd x ht ~> nhd THEN
+    forall ge d t, deps_model ge d hd ->
+    (forall m, tree_eval ge (data ht) m = tree_eval ge t m) -> (* TODO: condition à revoir, on peut sans doute relâcher ici ! *)
+    deps_model ge (deps_set d x t) nhd.
 Proof.
- unfold pdeps_get; rewrite Dict.empty_spec; simpl; auto.
+  intros; wlp_simplify.
+  unfold deps_model, deps_set; simpl. destruct H0 as (DM0 & DM1); split.
+  - intros m; unfold hdeps_valid in DM0 |- *; simpl.
+    generalize (failsafe_correct ge (data exta) m); intros FAILSAFE.
+    destruct (DM0 m) as (H2 & H3); clear DM0. unfold deps_eval in * |- *.
+    destruct (failsafe _); simpl.
+    * rewrite !H, !DM1 in * |- *; intuition (subst; eauto).
+    * clear FAILSAFE. rewrite <- DM1, <- H. intuition (subst; eauto).
+  - clear H DM0. unfold deps_eval, pdeps_get, deps_get in * |- *; simpl.
+    intros; case (R.eq_dec x x0).
+    + intros; subst; rewrite !Dict.set_spec_eq; simpl; auto.
+    + intros; rewrite !Dict.set_spec_diff; simpl; auto.
 Qed.
+Local Hint Resolve hdeps_set_correct: wlp.
+Global Opaque hdeps_set.
 
-Hint Rewrite pset_spec_eq pempty_spec: dict_rw.
+Variable debug_assign: R.t -> ?? option pstring.
+
+Fixpoint hinst_deps (i: inst) (d od: hdeps): ?? hdeps :=
+  match i with
+  | nil => RET d
+  | (x, e)::i' =>
+     DO dbg <~ debug_assign x;;
+     DO ht <~ hexp_tree e d od dbg;;
+     DO nd <~ hdeps_set d x ht;;
+     hinst_deps i' nd od
+  end.
 
 
-Lemma hinst_deps_correct i: forall d1 od1,
-  WHEN hinst_deps i d1 od1 ~> d1' THEN
-    forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) ->
-    (forall x, pdeps_get d1 x = deps_get d2 x) -> 
-    forall x, pdeps_get d1' x = deps_get (inst_deps i d2 od2) x.
+Lemma hinst_deps_correct i: forall hd hod,
+  WHEN hinst_deps i hd hod ~> hd' THEN
+    forall ge od d, deps_model ge od hod -> deps_model ge d hd -> deps_model ge (inst_deps i d od) hd'.
 Proof.
   induction i; simpl; wlp_simplify.
-  + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). 
-    - erewrite H0, H2; simpl; eauto. clear exta2 Hexta2 H2; auto.
-      intros x0; destruct (R.eq_dec a0 x0).
-      * subst. autorewrite with dict_rw. rewrite set_spec_eq. erewrite H1; eauto.
-      * rewrite set_spec_diff, pset_spec_diff; auto.
-    - rewrite H, H4; auto.
-  + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)).
-    - erewrite H0, H3; simpl; eauto. clear exta3 Hexta3 H3; auto.
-      intros x0; destruct (R.eq_dec a0 x0).
-      * subst; autorewrite with dict_rw. rewrite H2.
-        erewrite H, H1; eauto. rewrite set_spec_eq. congruence.
-      * rewrite set_spec_diff, pset_spec_diff; auto.
-   - rewrite H, H5; auto.
 Qed.
 Global Opaque hinst_deps.
-Hint Resolve hinst_deps_correct: wlp.
+Local Hint Resolve hinst_deps_correct: wlp.
 
 (* logging info: we log the number of inst-instructions passed ! *)
 Variable log: unit -> ?? unit. 
@@ -280,24 +282,24 @@ Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps :=
      hbblock_deps_rec p' d'
   end.
 
-Lemma hbblock_deps_rec_correct p: forall d1,
-  WHEN hbblock_deps_rec p d1 ~> d1' THEN
-    forall d2, (forall x, pdeps_get d1 x = deps_get d2 x) -> forall x, pdeps_get d1' x = deps_get (bblock_deps_rec p d2) x.
+Lemma hbblock_deps_rec_correct p: forall hd,
+  WHEN hbblock_deps_rec p hd ~> hd' THEN forall ge d, deps_model ge d hd -> deps_model ge (bblock_deps_rec p d) hd'.
 Proof.
   induction p; simpl; wlp_simplify.
 Qed.
 Global Opaque hbblock_deps_rec.
-Hint Resolve hbblock_deps_rec_correct: wlp.
+Local Hint Resolve hbblock_deps_rec_correct: wlp.
 
 
 Definition hbblock_deps: bblock -> ?? hdeps
- := fun p => hbblock_deps_rec p Dict.empty.
+ := fun p => hbblock_deps_rec p {| hpre:= nil ; hpost := Dict.empty |}.
 
 Lemma hbblock_deps_correct p:
-  WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps p) x.
+  WHEN hbblock_deps p ~> hd THEN forall ge, deps_model ge (bblock_deps p) hd.
 Proof.
-  unfold bblock_deps; wlp_simplify. erewrite H; eauto.
-  intros; autorewrite with dict_rw; auto. rewrite empty_spec. reflexivity.
+  unfold bblock_deps; wlp_simplify. eapply H. clear H.
+  unfold deps_model, pdeps_get, hdeps_valid, deps_eval, deps_get; simpl.
+  intuition; rewrite !Dict.empty_spec; simpl; auto.
 Qed.
 Global Opaque hbblock_deps.
 
@@ -324,11 +326,6 @@ Definition tree_hash_eq (ta tb: tree): ?? bool :=
      DO b <~ op_eq oa ob ;;
      if b then phys_eq lta ltb
      else RET false
-  | Terase t1a t2a, Terase t1b t2b =>
-      DO b <~ phys_eq t1a t1b ;;
-      if b 
-      then phys_eq t2a t2b
-      else RET false
   | _,_ => RET false
   end.
 
@@ -358,7 +355,7 @@ Qed.
 Global Opaque list_tree_hash_eq.
 Hint Resolve list_tree_hash_eq_correct: wlp.
 
-Lemma pdeps_get_intro d1 d2:
+Lemma pdeps_get_intro (d1 d2: hdeps):
   (forall x, Dict.get d1 x = Dict.get d2 x) -> (forall x, pdeps_get d1 x = pdeps_get d2 x).
 Proof.
   unfold pdeps_get; intros H x; rewrite H. destruct (Dict.get d2 x); auto.
@@ -366,6 +363,19 @@ Qed.
 
 Local Hint Resolve hbblock_deps_correct Dict.eq_test_correct: wlp.
 
+(* TODO: 
+  A REVOIR pour que Dict.test_eq qui soit insensible aux infos de debug !
+  (cf. definition ci-dessous).
+  Il faut pour généraliser hash_params sur des Setoid (et les Dict aussi, avec ListSetoid, etc)... 
+ *)
+Program Definition mk_hash_params (log: hashV tree -> ?? unit): Dict.hash_params (hashV tree) :=
+ {| (* Dict.test_eq := fun (ht1 ht2: hashV tree) => phys_eq (data ht1) (data ht2); *)
+    Dict.test_eq := phys_eq;
+    Dict.hashing := fun (ht: hashV tree) => RET (hid ht);
+    Dict.log := log |}.
+Obligation 1.
+  eauto with wlp.
+Qed.
 
 (*** A GENERIC EQ_TEST: IN ORDER TO SUPPORT SEVERAL DEBUGGING MODE !!! ***)
 
@@ -376,7 +386,6 @@ Variable dbg2: R.t -> ?? option pstring. (* log of p2 insts *)
 Variable log1: unit -> ?? unit. (* log of p1 insts *)
 Variable log2: unit -> ?? unit. (* log of p2 insts *)
 
-
 Variable hco_tree: hashConsing tree.
 Hypothesis hco_tree_correct: hCons_spec hco_tree.
 Variable hco_list: hashConsing list_tree.
@@ -385,34 +394,48 @@ Hypothesis hco_list_correct: hCons_spec hco_list.
 Variable print_error_end: hdeps -> hdeps -> ?? unit.
 Variable print_error: pstring -> ?? unit.
 
+Variable check_failpreserv: bool.
+Variable dbg_failpreserv: hashV tree -> ?? unit. (* info of additional failure of the output bbloc p2 wrt the input bbloc p1 *) 
+
 Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool :=
+  DO failure_in_failpreserv <~ make_cref false;;
   DO r <~ (TRY
     DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;;
     DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;;
     DO b <~ Dict.eq_test d1 d2 ;;
-    if b then RET true
-    else (
+    if b then (
+      if check_failpreserv then (
+          let hp := mk_hash_params dbg_failpreserv in
+          failure_in_failpreserv.(set)(true);;
+          Sets.assert_list_incl hp d2.(hpre) d1.(hpre);;
+          RET true
+      ) else RET false
+    ) else (
       print_error_end d1 d2 ;;
       RET false
     )
   CATCH_FAIL s, _ =>
-    print_error s;;
-    RET false
+    DO b <~ failure_in_failpreserv.(get)();;
+    if b then RET false 
+         else print_error s;; RET false
   ENSURE (fun b => b=true -> forall ge, bblock_simu ge p1 p2));;
   RET (`r).
 Obligation 1.
-  destruct hco_tree_correct as [X1 X2], hco_list_correct as [Y1 Y2].
+  destruct hco_tree_correct as [TEQ1 TEQ2], hco_list_correct as [LEQ1 LEQ2].
   constructor 1; wlp_simplify; try congruence.
+  destruct (H ge) as (EQPRE1&EQPOST1); destruct (H0 ge) as (EQPRE2&EQPOST2); clear H H0.
   apply bblock_deps_simu; auto.
-  intros; rewrite <- H, <- H0.
-  apply pdeps_get_intro. auto.
+  + intros m; rewrite <- EQPRE1, <- EQPRE2.
+    unfold incl, hdeps_valid in * |- *; intuition eauto.
+  + intros m0 x m1 VALID; rewrite <- EQPOST1, <- EQPOST2.
+    erewrite pdeps_get_intro; auto. auto.
 Qed.
 
 Theorem g_bblock_simu_test_correct p1 p2:
   WHEN g_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
 Proof.
   wlp_simplify.
-  destruct exta; simpl in * |- *; auto.
+  destruct exta0; simpl in * |- *; auto.
 Qed.
 Global Opaque g_bblock_simu_test.
 
@@ -429,6 +452,7 @@ Definition msg_error_on_end: pstring := "mismatch in final assignments !".
 Definition msg_unknow_tree: pstring := "unknown tree node".
 Definition msg_unknow_list_tree: pstring := "unknown list node".
 Definition msg_number: pstring := "on 2nd bblock -- on inst num ".
+Definition msg_notfailpreserv: pstring := "a possible failure of 2nd bblock is absent in 1st bblock".
 
 Definition print_error_end (_ _: hdeps): ?? unit
  := println (msg_prefix +; msg_error_on_end).
@@ -437,17 +461,30 @@ Definition print_error (log: logger unit) (s:pstring): ?? unit
  := DO n <~ log_info log ();;
     println (msg_prefix +; msg_number +; n +; " -- " +; s). 
 
+Definition failpreserv_error (_: hashV tree): ?? unit
+  := println (msg_prefix +; msg_notfailpreserv).
 
 Program Definition bblock_simu_test (p1 p2: bblock): ?? bool :=
   DO log <~ count_logger ();;
   DO hco_tree <~ mk_annot (hCons tree_hash_eq (fun _ => RET msg_unknow_tree));;
   DO hco_list <~ mk_annot (hCons list_tree_hash_eq (fun _ => RET msg_unknow_list_tree));;
-  g_bblock_simu_test no_dbg no_dbg skip (log_insert log) hco_tree _ hco_list _ print_error_end (print_error log) p1 p2.
-Obligation 1.  
+  g_bblock_simu_test
+    no_dbg
+    no_dbg
+    skip
+    (log_insert log)
+    hco_tree _
+    hco_list _
+    print_error_end
+    (print_error log)
+    true (* check_failpreserv *)
+    failpreserv_error
+    p1 p2.
+Obligation 1.
   generalize (hCons_correct _ _ _ _ H0); clear H0.
   constructor 1; wlp_simplify.
 Qed.
-Obligation 2.  
+Obligation 2.
   generalize (hCons_correct _ _ _ _ H); clear H.
   constructor 1; wlp_simplify.
 Qed.
@@ -486,10 +523,6 @@ Definition print_raw_htree (td: pre_hashV tree): ?? unit :=
     DO so <~ string_of_op o;;
     DO sl <~ string_of_hashcode lid;;
     println (so +; " " +; (list_id sl))
-  | (Terase _ _), [ _ ; t1; t2 ] =>
-    DO st1 <~ string_of_hashcode t1 ;;
-    DO st2 <~ string_of_hashcode t2 ;;
-    println((tree_id st1) +; " erases " +; (tree_id st2))
   | _, _ => FAILWITH "unexpected hcodes"
   end.
 
@@ -521,9 +554,6 @@ Fixpoint string_of_tree (t: tree) (pt: pre_hashV tree) : ?? pstring :=
       DO pl <~ get_hlist lid;;
       DO sl <~ string_of_list_tree l pl;;
       RET (so +; "(" +; sl +; ")")
-    | Terase t _, [ _ ; tid; _ ] =>
-      DO pt <~ get_htree tid ;;
-      string_of_tree t pt
     | _, _ => FAILWITH "unexpected hcodes"
     end
   end
@@ -699,11 +729,13 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
      (log_debug log1)
      simple_debug
      (hlog log1 hco_tree hco_list)
-     (log_insert log2) 
-     hco_tree _ 
-     hco_list _ 
+     (log_insert log2)
+     hco_tree _
+     hco_list _
      (print_error_end1 hco_tree hco_list)
-     (print_error1 hco_tree hco_list cr log2) 
+     (print_error1 hco_tree hco_list cr log2)
+     true
+     failpreserv_error (* TODO: debug info *)
      p1 p2;;
   if result1 
   then RET true
@@ -718,10 +750,12 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
        simple_debug
        (hlog log1 hco_tree hco_list)
        (log_insert log2)
-       hco_tree _ 
-       hco_list _ 
+       hco_tree _
+       hco_list _
        (print_error_end2 hco_tree hco_list)
-       (print_error2 hco_tree hco_list cr log2) 
+       (print_error2 hco_tree hco_list cr log2)
+       false
+       (fun _ => RET tt)
        p2 p1;;
     if result2 
     then (
@@ -796,7 +830,7 @@ Proof.
 Qed.
 Global Opaque eq_test.
 
-(* get some key of a non-empty d *)
+(* ONLY FOR DEBUGGING INFO: get some key of a non-empty d *)
 Fixpoint pick {A} (d: t A): ?? R.t :=
   match d with
   | Leaf _ => FAILWITH "unexpected empty dictionary"
@@ -809,7 +843,7 @@ Fixpoint pick {A} (d: t A): ?? R.t :=
     RET (xO p)
   end. 
 
-
+(* ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *)
 Fixpoint not_eq_witness {A} (d1 d2: t A): ?? option R.t :=
   match d1, d2 with
   | Leaf _, Leaf _ => RET None
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v
index 55e67608..7925f62d 100644
--- a/mppa_k1c/abstractbb/Impure/ImpCore.v
+++ b/mppa_k1c/abstractbb/Impure/ImpCore.v
@@ -132,6 +132,13 @@ Proof.
   destruct x; simpl; auto.
 Qed.
 
+Lemma wlp_option (A B: Type) (x: option A) (k1: A -> ??B) (k2: ??B)  (P: B -> Prop):
+  (forall a, x=Some a -> wlp (k1 a) P) -> 
+  (x=None -> wlp k2 P) -> 
+     (wlp (match x with Some a => k1 a | None => k2 end) P).
+Proof.
+  destruct x; simpl; auto.
+Qed.
 
 (* Tactics 
 
@@ -156,6 +163,7 @@ Ltac wlp_decompose :=
  || apply wlp_letprod
  || apply wlp_sum
  || apply wlp_sumbool
+ || apply wlp_option
  .
 
 (* this tactic simplifies the current "wlp" goal using any hint found via tactic "hint". *) 
@@ -185,4 +193,4 @@ Ltac wlp_xsimplify hint :=
 
 Create HintDb wlp discriminated.
 
-Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file
+Ltac wlp_simplify := wlp_xsimplify ltac:(intuition (eauto with wlp)).
\ No newline at end of file
diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v
index 307eb163..dd615628 100644
--- a/mppa_k1c/abstractbb/Impure/ImpHCons.v
+++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v
@@ -3,8 +3,6 @@ Require Export ImpIO.
 Import Notations.
 Local Open Scope impure.
 
-(********************************)
-(* (Weak) HConsing              *)
 
 Axiom string_of_hashcode: hashcode -> ?? caml_string.
 Extract Constant string_of_hashcode => "string_of_int".
@@ -12,6 +10,99 @@ Extract Constant string_of_hashcode => "string_of_int".
 Axiom hash: forall {A}, A -> ?? hashcode.
 Extract Constant hash => "Hashtbl.hash".
 
+(**************************)
+(* (Weak) Sets            *)
+
+
+Import Dict.
+
+Axiom make_dict: forall {A B}, (hash_params A) -> ?? Dict.t A B.
+Extract Constant make_dict => "ImpHConsOracles.make_dict".
+
+
+Module Sets.
+
+Definition t {A} (mod: A -> Prop) := Dict.t A {x | mod x}.
+
+Definition empty {A} (hp: hash_params A) {mod:A -> Prop}: ?? t mod :=
+  make_dict hp.
+
+Program Fixpoint add {A} (l: list A) {mod: A -> Prop} (d: t mod): forall {H:forall x, List.In x l -> mod x}, ?? unit :=
+  match l with
+  | nil => fun H => RET ()
+  | x::l' => fun H =>
+    d.(set)(x,x);;
+    add l' d
+  end.
+
+Program Definition create {A} (hp: hash_params A) (l:list A): ?? t (fun x => List.In x l) :=
+  DO d <~ empty hp (mod:=fun x => List.In x l);;
+  add l (mod:=fun x => List.In x l) d (H:=_);;
+  RET d.
+Global Opaque create.
+
+Definition is_present {A} (hp: hash_params A) (x:A) {mod} (d:t mod): ?? bool :=
+  DO oy <~ (d.(get)) x;;
+  match oy with
+  | Some y => hp.(test_eq) x (`y)
+  | None => RET false
+  end.
+
+Local Hint Resolve test_eq_correct: wlp.
+
+Lemma is_present_correct A (hp: hash_params A) x mod (d:t mod):
+ WHEN is_present hp x d ~> b THEN b=true -> mod x.
+Proof.
+  wlp_simplify; subst; eauto.
+  - apply proj2_sig.
+  - discriminate. 
+Qed.
+Hint Resolve is_present_correct: wlp.
+Global Opaque is_present.
+
+Definition msg_assert_incl: pstring := "Sets.assert_incl".
+
+Fixpoint assert_incl {A} (hp: hash_params A) (l: list A) {mod} (d:t mod): ?? unit :=
+  match l with
+  | nil => RET ()
+  | x::l' =>
+    DO b <~ is_present hp x d;;
+    if b then
+      assert_incl hp l' d
+    else (
+      hp.(log) x;;
+      FAILWITH msg_assert_incl
+    )
+  end.
+
+Lemma assert_incl_correct A (hp: hash_params A) l mod (d:t mod):
+ WHEN assert_incl hp l d ~> _ THEN forall x, List.In x l -> mod x.
+Proof.
+  induction l; wlp_simplify; subst; eauto.
+Qed.
+Hint Resolve assert_incl_correct: wlp.
+Global Opaque assert_incl.
+
+Definition assert_list_incl {A} (hp: hash_params A) (l1 l2: list A): ?? unit :=
+  (* println "";;print("dict_create ");;*)
+  DO d <~ create hp l2;;
+  (*print("assert_incl ");;*)
+  assert_incl hp l1 d.
+
+Lemma assert_list_incl_correct A (hp: hash_params A) l1 l2:
+ WHEN assert_list_incl hp l1 l2 ~> _ THEN List.incl l1 l2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque assert_list_incl.
+Hint Resolve assert_list_incl_correct.
+
+End Sets.
+
+(********************************)
+(* (Weak) HConsing              *)
+
+
 Axiom xhCons: forall {A}, ((A -> A -> ?? bool) * (pre_hashV A -> ?? hashV A)) -> ?? hashConsing A.
 Extract Constant xhCons => "ImpHConsOracles.xhCons".
 
diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v
index 0efa042c..1a84eb3b 100644
--- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v
+++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v
@@ -91,11 +91,37 @@ Extract Inlined Constant struct_eq => "(=)".
 Hint Resolve struct_eq_correct: wlp.
 
 
-(** Data-structure for generic hash-consing *)
+(** Data-structure for generic hash-consing, hash-set *)
 
 Axiom hashcode: Type.
 Extract Constant hashcode => "int".
 
+Module Dict.
+
+Record hash_params {A:Type} := {
+  test_eq: A -> A -> ??bool;
+  test_eq_correct: forall x y, WHEN test_eq x y ~> r THEN r=true -> x=y;
+  hashing: A -> ??hashcode;
+  log: A -> ??unit (* for debugging only *)
+}.
+Arguments hash_params: clear implicits.
+
+
+Record t {A B:Type} := {
+  set: A * B -> ?? unit;
+  get: A -> ?? option B
+}.
+Arguments t: clear implicits.
+
+End Dict.
+
+
+(* NB: hashConsing is assumed to generate hash-code in ascending order.
+   This gives a way to check that a hash-consed value is older than an other one.
+*)
+Axiom hash_older: hashcode -> hashcode -> ?? bool.
+Extract Inlined Constant hash_older => "(<=)".
+
 Record pre_hashV {A: Type} := {
   pre_data: A;
   hcodes: list hashcode;
@@ -116,6 +142,7 @@ Record hashExport {A:Type}:= {
 Arguments hashExport: clear implicits.
 
 Record hashConsing {A:Type}:= {
+  (* TODO next_hashcode: unit -> ?? hashcode *) 
   hC: pre_hashV A -> ?? hashV A;
   hC_known: pre_hashV A -> ?? hashV A; (* fails on unknown inputs *)
   (**** below: debugging functions ****)
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
index c421ff87..b7a80679 100644
--- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
@@ -1,7 +1,21 @@
 open ImpPrelude
 
 exception Stop;;
-    
+
+let make_dict (type key) (p: key Dict.hash_params) =
+  let module MyHashedType = struct
+    type t = key
+    let equal = p.Dict.test_eq 
+    let hash = p.Dict.hashing 
+  end in
+  let module MyHashtbl = Hashtbl.Make(MyHashedType) in
+  let dict = MyHashtbl.create 1000 in
+  {
+    Dict.set = (fun (k,d) -> MyHashtbl.replace dict k d);
+    Dict.get = (fun k -> MyHashtbl.find_opt dict k)
+  }
+
+
 let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV)) =
   let module MyHashedType = struct
     type t = a pre_hashV
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
index e81681df..a74c721a 100644
--- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
@@ -1,3 +1,4 @@
 open ImpPrelude
 
+val make_dict : 'a1 Dict.hash_params -> ('a1, 'a2) Dict.t
 val xhCons: (('a -> 'a -> bool) * ('a pre_hashV -> 'a hashV)) -> 'a hashConsing