Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

15 files changed, 2093 insertions, 1539 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 265c4e84..b11a77ff 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -9,7 +9,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import ZArith.
 Require Import Coqlib.
-Require Import ImpDep.
+Require Import ImpSimuTest.
 Require Import Axioms.
 Require Import Parallelizability.
 Require Import Asmvliw Permutation.
@@ -302,30 +302,6 @@ Definition op_eval (o: op) (l: list value) :=
   end.
 
 
- (** Function [is_constant] is used for a small optimization inside the scheduling verifier.
-    It is good that it answers [true] as much as possible while satisfying [is_constant_correct] below.
-
-   BE CAREFUL that, [is_constant] must not depend on [ge].
-   Otherwise, we would have an easy implementation: [match op_eval o nil with Some _ => true | _ => false end]
-
-   => REM: when [is_constant] is not complete w.r.t [is_constant_correct], this should have only a very little impact
-      on the performance of the scheduling verifier...
-  *)
-
-Definition is_constant (o: op): bool :=
-  match o with
-  | Constant _ | OArithR _ | OArithRI32 _ _ | OArithRI64 _ _ | OArithRF32 _ _ | OArithRF64 _ _ => true
-  | _ => false
-  end.
-
-Lemma is_constant_correct o: is_constant o = true -> op_eval o nil <> None.
-Proof.
-  destruct o; simpl; try congruence.
-  destruct ao; simpl; try congruence;
-  destruct n; simpl; try congruence;
-  unfold arith_eval; destruct Ge; simpl; try congruence.
-Qed.
-
 Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   match o1 with
   | OArithR n1 =>
@@ -507,7 +483,7 @@ Include MkSeqLanguage P.
 
 End L.
 
-Module IDT := ImpDepTree L ImpPosDict.
+Module IST := ImpSimu L ImpPosDict.
 
 Import L.
 Import P.
@@ -1609,16 +1585,46 @@ Definition string_of_op (op: P.op): ?? pstring :=
   | Fail => RET (Str "Fail")
   end.
 
+End SECT_BBLOCK_EQUIV.
+
+(** REWRITE RULES *)
+
+Definition is_constant (o: op): bool :=
+  match o with
+  | Constant _ | OArithR _ | OArithRI32 _ _ | OArithRI64 _ _ | OArithRF32 _ _ | OArithRF64 _ _ => true
+  | _ => false
+  end.
+
+Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None.
+Proof.
+  destruct o; simpl in * |- *; try congruence.
+  destruct ao; simpl in * |- *; try congruence;
+  destruct n; simpl in * |- *; try congruence;
+  unfold arith_eval; destruct ge; simpl in * |- *; try congruence.
+Qed.
+
+Definition main_reduce (t: Terms.term):= RET (Terms.nofail is_constant t).
+
+Local Hint Resolve is_constant_correct: wlp.
+
+Lemma main_reduce_correct t:
+ WHEN main_reduce t ~> pt THEN Terms.match_pt t pt.
+Proof.
+  wlp_simplify.
+Qed.
+
+Definition reduce := {| Terms.result := main_reduce; Terms.result_correct := main_reduce_correct |}.
+
 Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool :=
   if verb then
-    IDT.verb_bblock_simu_test string_of_name string_of_op (trans_block p1) (trans_block p2)
+    IST.verb_bblock_simu_test reduce string_of_name string_of_op (trans_block p1) (trans_block p2)
   else
-    IDT.bblock_simu_test (trans_block p1) (trans_block p2).
+    IST.bblock_simu_test reduce (trans_block p1) (trans_block p2).
 
-Local Hint Resolve IDT.bblock_simu_test_correct bblock_simu_reduce IDT.verb_bblock_simu_test_correct: wlp.
+Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp.
 
 Theorem bblock_simu_test_correct verb p1 p2 :
-  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Ge = Genv ge fn -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
+  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockgenproof0.bblock_simu ge fn p1 p2.
 Proof.
   wlp_simplify.
 Qed.
@@ -1630,7 +1636,7 @@ Import UnsafeImpure.
 
 Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_simu_test verb p1 p2).
 
-Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: Ge = Genv ge fn -> pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
+Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
 Proof.
    intros; unfold pure_bblock_simu_test. intros; eapply bblock_simu_test_correct; eauto.
    apply unsafe_coerce_not_really_correct; eauto.
@@ -1638,9 +1644,7 @@ Qed.
 
 Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_simu_test true.
 
-Lemma bblock_simub_correct p1 p2 ge fn: Ge = Genv ge fn -> bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
+Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
 Proof.
  eapply (pure_bblock_simu_test_correct true).
-Qed.
-
-End SECT_BBLOCK_EQUIV.
+Qed.
\ No newline at end of file
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 8e6aa028..3370fae3 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -424,7 +424,7 @@ Qed.
 (*
 Lemma signed_0_eqb :
   forall x, (Z.eqb (Int.signed x) 0) = Int.eq x Int.zero.
-Admitted.
+Qed.
  *)
 
 Lemma Z_quot_le: forall a b,
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 2fc561ee..462e9cd0 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -699,20 +699,96 @@ let instruction_usages bb =
  * Latency constraints building
  *)
 
-type access = { inst: int; loc: location }
+(* type access = { inst: int; loc: location } *)
 
-let rec get_accesses llocs laccs =
-  let accesses loc laccs = List.filter (fun acc -> acc.loc = loc) laccs
-  in match llocs with
-  | [] -> []
-  | loc :: llocs -> (accesses loc laccs) @ (get_accesses llocs laccs)
+let preg2int pr = Camlcoq.P.to_int @@ Asmblockdeps.ppos pr
+
+let loc2int = function
+  | Mem -> 1
+  | Reg pr -> preg2int pr
+
+(* module HashedLoc = struct
+  type t = { loc: location; key: int }
+  let equal l1 l2 = (l1.key = l2.key)
+  let hash l = l.key
+  let create (l:location) : t = { loc=l; key = loc2int l }
+end *)
+
+(* module LocHash = Hashtbl.Make(HashedLoc) *)
+module LocHash = Hashtbl
+
+(* Hash table : location => list of instruction ids *)
 
 let rec intlist n =
   if n < 0 then failwith "intlist: n < 0"
   else if n = 0 then []
   else (n-1) :: (intlist (n-1))
 
-let latency_constraints bb = (* failwith "latency_constraints: not implemented" *)
+let find_in_hash hashloc loc =
+  match LocHash.find_opt hashloc loc with
+  | Some idl -> idl
+  | None -> []
+
+(* Returns a list of instruction ids *)
+let rec get_accesses hashloc (ll: location list) = match ll with
+  | [] -> []
+  | loc :: llocs -> (find_in_hash hashloc loc) @ (get_accesses hashloc llocs)
+
+let latency_constraints bb =
+  let written = LocHash.create 70
+  and read = LocHash.create 70
+  and count = ref 0
+  and constraints = ref []
+  and instr_infos = instruction_infos bb
+  in let step (i: inst_info) =
+    let raw = get_accesses written i.read_locs
+    and waw = get_accesses written i.write_locs
+    and war = get_accesses read i.write_locs
+    in begin
+      List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) raw;
+      List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) waw;
+      List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = 0} :: !constraints) war;
+      if i.is_control then List.iter (fun n -> constraints := {instr_from = n; instr_to = !count; latency = 0} :: !constraints) (intlist !count);
+      (* Updating "read" and "written" hashmaps *)
+      List.iter (fun loc ->
+                  begin 
+                    LocHash.replace written loc [!count];
+                    LocHash.replace read loc []; (* Clearing all the entries of "read" hashmap when a register is written *)
+                  end) i.write_locs;
+      List.iter (fun loc -> LocHash.replace read loc ((!count) :: (find_in_hash read loc))) i.read_locs;
+      count := !count + 1
+    end
+  in (List.iter step instr_infos; !constraints)
+
+(*
+let rec list2locmap v = function
+  | [] -> LocMap.empty
+  | loc :: l -> LocMap.add loc v (list2locmap v l)
+
+  let written = ref (LocHash.create 0)
+  and read = ref LocMap.empty
+  and count = ref 0
+  and constraints = ref []
+  and instr_infos = instruction_infos bb
+  in let step (i: inst_info) =
+    let write_accesses = list2locmap !count i.write_locs
+    and read_accesses = list2locmap !count i.read_locs
+    in let raw = get_accesses i.read_locs !written
+    and waw = get_accesses i.write_locs !written
+    and war = get_accesses i.write_locs !read
+    in begin
+      LocMap.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) raw;
+      LocMap.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) waw;
+      LocMap.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = 0} :: !constraints) war;
+      if i.is_control then List.iter (fun n -> constraints := {instr_from = n; instr_to = !count; latency = 0} :: !constraints) (intlist !count);
+      written := LocMap.union (fun _ i1 i2 -> if i1 < i2 then Some i2 else Some i1) !written write_accesses;
+      read := LocMap.union (fun _ i1 i2 -> if i1 < i2 then Some i2 else Some i1) !read read_accesses;
+      count := !count + 1
+    end
+  in (List.iter step instr_infos; !constraints)
+  *)
+
+(* let latency_constraints bb = (* failwith "latency_constraints: not implemented" *)
   let written = ref []
   and read = ref []
   and count = ref 0
@@ -734,6 +810,7 @@ let latency_constraints bb = (* failwith "latency_constraints: not implemented"
       count := !count + 1
     end
   in (List.iter step instr_infos; !constraints)
+*)
 
 (**
  * Using the InstructionScheduler
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 618f3ebe..5c94d435 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -1,6 +1,7 @@
 (** Syntax and Sequential Semantics of Abstract Basic Blocks.
 *)
-
+Require Import Setoid.
+Require Import ImpPrelude.
 
 Module Type PseudoRegisters.
 
@@ -24,16 +25,8 @@ Parameter op: Type. (* type of operations *)
 
 Parameter genv: Type. (* environment to be used for evaluating an op *)
 
-(* NB: possible generalization
- - relation after/before.
-*)
 Parameter op_eval: genv -> op -> list value -> option value.
 
-Parameter is_constant: op -> bool.
-
-Parameter is_constant_correct: 
-  forall ge o, is_constant o = true -> op_eval ge o nil <> None.
-
 End LangParam.
 
 
@@ -54,6 +47,9 @@ Definition mem := R.t -> value.
 Definition assign (m: mem) (x:R.t) (v: value): mem 
   := fun y => if R.eq_dec x y then v else m y.
 
+
+(** expressions *)
+
 Inductive exp :=
   | PReg (x:R.t)
   | Op (o:op) (le: list_exp)
@@ -140,7 +136,7 @@ Proof.
 Qed.
 
 
-(** A small theory of bblock equality *)
+(** A small theory of bblock simulation *)
 
 (* equalities on bblock outputs *)
 Definition res_eq (om1 om2: option mem): Prop :=
@@ -240,6 +236,195 @@ Qed.
 
 End SEQLANG.
 
+Module Terms.
+
+(** terms in the symbolic evaluation 
+NB: such a term represents the successive computations in one given pseudo-register
+*)
+
+Inductive term :=
+  | Input (x:R.t) (hid:hashcode)
+  | App (o: op) (l: list_term) (hid:hashcode)
+with list_term :=
+  | LTnil (hid:hashcode)
+  | LTcons (t:term) (l:list_term) (hid:hashcode)
+  .
+
+Scheme term_mut := Induction for term Sort Prop
+with list_term_mut := Induction for list_term Sort Prop.
+
+Bind Scope pattern_scope with term.
+Delimit Scope term_scope with term.
+Delimit Scope pattern_scope with pattern.
+
+Notation "[ ]" := (LTnil _) (format "[ ]"): pattern_scope.
+Notation "[ x ]" := (LTcons x [] _): pattern_scope.
+Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil _) _) .. _) _): pattern_scope.
+Notation "o @ l" := (App o l _) (at level 50, no associativity): pattern_scope.
+
+Import HConsingDefs.
+
+Notation "[ ]" := (LTnil unknown_hid) (format "[ ]"): term_scope.
+Notation "[ x ]" := (LTcons x [] unknown_hid): term_scope.
+Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil unknown_hid) unknown_hid) .. unknown_hid) unknown_hid): term_scope.
+Notation "o @ l" := (App o l unknown_hid) (at level 50, no associativity): term_scope.
+
+Local Open Scope pattern_scope.
+
+Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value :=
+  match t with
+  | Input x _ => Some (m x)
+  | o @ l =>
+     match list_term_eval ge l m with
+     | Some v => op_eval ge o v
+     | _ => None
+     end
+  end
+with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) :=
+  match l with
+  | [] => Some nil
+  | LTcons t l' _ => 
+    match term_eval ge t m, list_term_eval ge l' m with
+    | Some v, Some lv => Some (v::lv)
+    | _, _ => None
+    end
+  end.
+
+
+Definition term_get_hid (t: term): hashcode :=
+  match t with
+  | Input _ hid => hid
+  | App _ _ hid => hid
+  end.
+
+Definition list_term_get_hid (l: list_term): hashcode :=
+  match l with
+  | LTnil hid => hid
+  | LTcons _ _ hid => hid
+  end.
+
+
+Fixpoint allvalid ge (l: list term) m : Prop :=
+  match l with
+  | nil => True
+  | t::nil => term_eval ge t m <> None
+  | t::l' => term_eval ge t m <> None /\ allvalid ge l' m
+  end. 
+
+Lemma allvalid_extensionality ge (l: list term) m:
+  allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None).
+Proof.
+  induction l as [|t l]; simpl; try (tauto).
+  destruct l.
+  - intuition (congruence || eauto).
+  - rewrite IHl; clear IHl. intuition (congruence || eauto).
+Qed.
+
+Record pseudo_term: Type := intro_fail {
+  mayfail: list term;
+  effect: term
+}.
+
+Lemma inf_option_equivalence (A:Type) (o1 o2: option A):
+  (o1 <> None -> o1 = o2) <-> (forall m1, o1 = Some m1 -> o2 = Some m1).
+Proof.
+  destruct o1; intuition (congruence || eauto).
+  symmetry; eauto.
+Qed.
+
+Definition match_pt (t: term) (pt: pseudo_term) :=
+      (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m)
+   /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1).
+
+Lemma intro_fail_correct (l: list term) (t: term) :
+   (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t).
+Proof.
+  unfold match_pt; simpl; intros; intuition congruence.
+Qed.
+Hint Resolve intro_fail_correct: wlp.
+
+Definition identity_fail (t: term):= intro_fail [t] t.
+
+Lemma identity_fail_correct (t: term): match_pt t (identity_fail t).
+Proof.
+  eapply intro_fail_correct; simpl; tauto.
+Qed.
+Global Opaque identity_fail.
+Hint Resolve identity_fail_correct: wlp.
+
+Definition nofail (is_constant: op -> bool) (t: term):=
+    match t with
+    | Input x _ => intro_fail ([])%list t
+    | o @ [] => if is_constant o then (intro_fail ([])%list t) else (identity_fail t)
+    | _ => identity_fail t
+    end.
+
+Lemma nofail_correct (is_constant: op -> bool) t:
+ (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t).
+Proof.
+  destruct t; simpl.
+  + intros; eapply intro_fail_correct; simpl; intuition congruence.
+  + intros; destruct l; simpl; auto with wlp.
+    destruct (is_constant o) eqn:Heqo; simpl; intuition eauto with wlp.
+     eapply intro_fail_correct; simpl; intuition eauto with wlp.
+Qed.
+Global Opaque nofail.
+Hint Resolve nofail_correct: wlp.
+
+Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m.
+
+Global Instance term_equiv_Equivalence : Equivalence term_equiv.
+Proof.
+  split; intro x; unfold term_equiv; intros; eauto.
+  eapply eq_trans; eauto.
+Qed.
+
+Lemma match_pt_term_equiv t1 t2 pt: term_equiv t1 t2 -> match_pt t1 pt -> match_pt t2 pt.
+Proof.
+  unfold match_pt, term_equiv.
+  intros H. intuition; try (erewrite <- H1 in * |- *; congruence).
+  erewrite <- H2; eauto; congruence.
+Qed.
+Hint Resolve match_pt_term_equiv: wlp.
+
+Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term :=
+  {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}.
+
+Lemma app_fail_allvalid_correct l pt t1 t2: forall
+  (V1: forall (ge : genv) (m : mem), term_eval ge t1 m <> None <-> allvalid ge (mayfail pt) m)
+  (V2: forall (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail {| mayfail := t1 :: l; effect := t1 |}) m)
+  (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail (app_fail l pt)) m.
+Proof.
+  intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; simpl. clear V1 V2.
+  intuition subst.
+  + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto.
+  + eapply H3; eauto.
+    intros. intuition subst.
+    * eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto.
+    * intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto.
+Qed.
+Local Hint Resolve app_fail_allvalid_correct.
+
+Lemma app_fail_correct l pt t1 t2: 
+  match_pt t1 pt -> 
+  match_pt t2 {| mayfail:=t1::l; effect:=t1 |} ->
+  match_pt t2 (app_fail l pt).
+Proof.
+  unfold match_pt in * |- *; intros (V1 & E1) (V2 & E2); split; intros ge m; try (eauto; fail).
+Qed.
+Extraction Inline app_fail.
+
+Import ImpCore.Notations.
+Local Open Scope impure_scope.
+
+Record reduction:= {
+  result:> term -> ?? pseudo_term;
+  result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt;
+}.
+Hint Resolve result_correct: wlp.
+
+End Terms.
+
 End MkSeqLanguage.
 
 
diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v
deleted file mode 100644
index c7bed8bf..00000000
--- a/mppa_k1c/abstractbb/DepTreeTheory.v
+++ /dev/null
@@ -1,456 +0,0 @@
-(** Dependency Trees of Abstract Basic Blocks
-
-with a purely-functional-but-exponential test.
-
-*)
-
-
-Require Setoid. (* in order to rewrite <-> *)
-Require Export AbstractBasicBlocksDef.
-Require Import List.
-
-Module Type PseudoRegDictionary.
-
-Declare Module R: PseudoRegisters.
-
-Parameter t: Type -> Type.
-
-Parameter get: forall {A}, t A -> R.t -> option A.
-
-Parameter set: forall {A}, t A -> R.t -> A -> t A.
-
-Parameter set_spec_eq: forall A d x (v: A),
-  get (set d x v) x = Some v.
-
-Parameter set_spec_diff: forall A d x y (v: A),
-  x <> y -> get (set d x v) y = get d y.
-
-Parameter empty: forall {A}, t A.
-
-Parameter empty_spec: forall A x,
-  get (empty (A:=A)) x = None.
-
-End PseudoRegDictionary.
-
-
-(** * Computations of "bblock" Dependencies and application to the equality test *)
-
-Module DepTree (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R).
-
-Export L.
-Export LP.
-
-Section DEPTREE.
-
-(** Dependency Trees of these "bblocks" 
-
-NB: each tree represents the successive computations in one given resource
-
-*)
-
-Inductive tree :=
-  | Tname (x:R.t)
-  | Top (o: op) (l: list_tree)
-with list_tree :=
-  | Tnil: list_tree
-  | Tcons (t:tree) (l:list_tree):  list_tree
-  .
-
-
-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 ge l m with
-     | Some v => op_eval ge o v
-     | _ => None
-     end
-  end
-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 ge t m), (list_tree_eval ge l' m) with
-    | Some v, Some lv => Some (v::lv)
-    | _, _ => None
-    end
-  end.
-
-Definition deps_get (d:Dict.t tree) x := 
-   match Dict.get d x with 
-   | None => Tname x
-   | Some t => t
-   end.
-
-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: 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.
-
-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.
-
-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 deps_eval_empty x m: deps_eval ge deps_empty x m = Some (m x).
-Proof.
-  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 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 :=
-  match p with
-  | nil => d
-  | i::p' =>
-     let d':=inst_deps i d d in
-     bblock_deps_rec p' d'
-  end.
-
-Local Hint Resolve deps_eval_empty.
-
-Definition bblock_deps: bblock -> deps
- := 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.
-
-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, 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.
-  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. 
-Qed.
-
-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 VALID H; erewrite IHi; eauto. clear IHi.
-  destruct (R.eq_dec x y).
-  * subst; autorewrite with dict_rw.
-    generalize (inst_deps_pre_monotonic _ _ _ _ VALID); clear VALID.
-    unfold deps_set; simpl; intuition congruence.
-  * rewrite set_spec_diff; auto.
-Qed.
-
-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 VALID H; erewrite IHp; eauto. clear IHp.
-  eapply inst_deps_abort; eauto.
-Qed.
-
-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, 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.
-    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.
-
-Lemma bblocks_deps_rec_Some_correct1 p m0: forall (m1 m2: mem) d, 
- run ge p m1 = Some m2 -> 
-  (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.
-    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, deps_eval ge (bblock_deps p) x m0 = Some (m1 x).
-Proof.
-  intros; eapply bblocks_deps_rec_Some_correct1; eauto.
-Qed.
-
-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.
-  - 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. 
-        erewrite tree_eval_exp; eauto.
-      * rewrite set_spec_diff; auto.
-    + intuition.
-      constructor 1 with (x:=x); simpl.
-      apply inst_deps_abort; auto.
-      autorewrite with dict_rw.
-      erewrite tree_eval_exp; eauto.
-Qed.
-
-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, 
-  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 VALID H0.
-  - intros H; eapply ex_intro; intuition eauto.
-    generalize (H0 x); rewrite H.
-    congruence.
-  - intros H.
-    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.
-        erewrite tree_eval_exp; eauto.
-      * rewrite set_spec_diff; auto.
-    + generalize (H x).
-      rewrite inst_deps_abort; discriminate || auto.
-      autorewrite with dict_rw. 
-      erewrite tree_eval_exp; eauto.
-Qed.
-
-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 VALID H0.
-  - intros H; eapply ex_intro; intuition eauto.
-    generalize (H0 x); rewrite H.
-    congruence.
-  - intros H.
-     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).
-      erewrite block_deps_rec_abort; eauto.
-      congruence.
-Qed.
-
-
-Lemma bblock_deps_Some_correct2 p m0 m1:
-  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 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.
-
-Definition valid ge d m := pre d ge m /\ forall x, deps_eval ge d x m <> None.
-
-Theorem bblock_deps_simu p1 p2:
-  (forall m, valid ge (bblock_deps p1) m -> valid ge (bblock_deps p2) m) ->
-  (forall m0 x m1, valid ge (bblock_deps p1) 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.
-  Local Hint Resolve bblock_deps_valid bblock_deps_Some_correct1.
-  unfold valid; intros INCL EQUIV m DONTFAIL.
-  destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence.
-  assert (X: forall x, deps_eval ge (bblock_deps p1) x m = Some (m1 x)); eauto.
-  eapply bblock_deps_Some_correct2; eauto.
-  + destruct (INCL m); intuition eauto.
-    congruence.
-  + intro x; apply EQUIV; intuition eauto.
-    congruence.
-Qed.
-
-Lemma valid_set_decompose_1 d t x m:
-  valid ge (deps_set d x t) m -> valid ge d m.
-Proof.
-  unfold valid; intros ((PRE1 & PRE2) & VALID); split.
-  + intuition.
-  + intros x0 H. case (R.eq_dec x x0).
-    * intuition congruence.
-    * intros DIFF; eapply VALID. erewrite set_spec_diff; eauto.
-Qed.
-
-Lemma valid_set_decompose_2 d t x m:
-  valid ge (deps_set d x t) m -> tree_eval ge t m <> None.
-Proof.
-  unfold valid; intros ((PRE1 & PRE2) & VALID) H.
-  generalize (VALID x); autorewrite with dict_rw.
-  tauto.
-Qed.
-
-Lemma valid_set_proof d x t m:
-  valid ge d m -> tree_eval ge t m <> None -> valid ge (deps_set d x t) m.
-Proof.
-  unfold valid; intros (PRE & VALID) PREt. split.
-  + split; auto.
-  + intros x0; case (R.eq_dec x x0).
-    - intros; subst; autorewrite with dict_rw. auto.
-    - intros. rewrite set_spec_diff; auto. 
-Qed.
-
-End DEPTREE.
-
-End DepTree.
-
-Require Import PArith.
-Require Import FMapPositive.
-
-Module PosDict <: PseudoRegDictionary with Module R:=Pos.
-
-Module R:=Pos.
-
-Definition t:=PositiveMap.t.
-
-Definition get {A} (d:t A) (x:R.t): option A 
- := PositiveMap.find x d.
-
-Definition set {A} (d:t A) (x:R.t) (v:A): t A
- := PositiveMap.add x v d.
-
-Local Hint Unfold PositiveMap.E.eq.
-
-Lemma set_spec_eq A d x (v: A):
-  get (set d x v) x = Some v.
-Proof.
-  unfold get, set; apply PositiveMap.add_1; auto.
-Qed.
-
-Lemma set_spec_diff A d x y (v: A):
-  x <> y -> get (set d x v) y = get d y.
-Proof.
-  unfold get, set; intros; apply PositiveMap.gso; auto.
-Qed.
-
-Definition empty {A}: t A := PositiveMap.empty A.
-
-Lemma empty_spec A x:
-  get (empty (A:=A)) x = None.
-Proof.
-  unfold get, empty; apply PositiveMap.gempty; auto.
-Qed.
-
-End PosDict.
\ No newline at end of file
diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v
deleted file mode 100644
index eebf396d..00000000
--- a/mppa_k1c/abstractbb/ImpDep.v
+++ /dev/null
@@ -1,960 +0,0 @@
-(** Dependency Graph of Abstract Basic Blocks
-
-using imperative hash-consing technique in order to get a linear equivalence test.
-
-*)
-
-Require Export Impure.ImpHCons.
-Export Notations.
-
-Require Export DepTreeTheory.
-
-Require Import PArith.
-
-
-Local Open Scope impure.
-
-Import ListNotations.
-Local Open Scope list_scope.
-
-
-Module Type ImpParam.
-
-Include LangParam.
-
-Parameter op_eq: op -> op -> ?? bool.
-
-Parameter op_eq_correct: forall o1 o2, 
- WHEN op_eq o1 o2 ~> b THEN
-  b=true -> o1 = o2.
-
-End ImpParam.
-
-
-Module Type ISeqLanguage.
-
-Declare Module LP: ImpParam.
-
-Include MkSeqLanguage LP.
-
-End ISeqLanguage.
-
-
-Module Type ImpDict.
-
-Include PseudoRegDictionary.
-
-Parameter eq_test: forall {A}, t A -> t A -> ?? bool.
-
-Parameter eq_test_correct: forall A (d1 d2: t A),
- WHEN eq_test d1 d2 ~> b THEN
-  b=true -> forall x, get d1 x = get d2 x.
-
-(* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries  *)
-
-
-(* only for debugging *)
-Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t.
-
-End ImpDict.
-
-Module ImpDepTree (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R).
-
-Module DT := DepTree L Dict.
-
-Import DT.
-
-Section CanonBuilding.
-
-Variable hC_tree: pre_hashV tree -> ?? hashV tree.
-Hypothesis hC_tree_correct: forall t, WHEN hC_tree t ~> t' THEN pre_data t=data t'.
-
-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'.
-
-(* First, we wrap constructors for hashed values !*)
-
-Local Open Scope positive.
-Local Open Scope list_scope.
-
-Definition hTname (x:R.t) (debug: option pstring): ?? hashV tree :=
-   DO hc <~ hash 1;;
-   DO hv <~ hash x;;
-   hC_tree {| pre_data:=Tname x; hcodes :=[hc;hv]; debug_info := debug |}.
-
-Lemma hTname_correct x dbg: 
-  WHEN hTname x dbg ~> t THEN (data t)=(Tname x).
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque hTname.
-Hint Resolve hTname_correct: wlp.
-
-Definition hTop (o:op) (l: hashV list_tree) (debug: option pstring) : ?? hashV tree :=
-   DO hc <~ hash 2;; 
-   DO hv <~ hash o;;
-   hC_tree {| pre_data:=Top o (data l); 
-              hcodes:=[hc;hv;hid l]; 
-              debug_info := debug  |}.
-
-Lemma hTop_correct o l dbg : 
-  WHEN hTop o l dbg ~> t THEN (data t)=(Top o (data l)).
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque hTop.
-Hint Resolve hTop_correct: wlp.
-
-Definition hTnil (_: unit): ?? hashV list_tree :=
-   hC_list_tree {| pre_data:=Tnil; hcodes := nil; debug_info := None |} .
-
-Lemma hTnil_correct x: 
-  WHEN hTnil x ~> l THEN (data l)=Tnil.
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque hTnil.
-Hint Resolve hTnil_correct: wlp.
-
-
-Definition hTcons (t: hashV tree) (l: hashV list_tree): ?? hashV list_tree :=
-   hC_list_tree {| pre_data:=Tcons (data t) (data l); hcodes := [hid t; hid l]; debug_info := None |}.
-
-Lemma hTcons_correct t l: 
-  WHEN hTcons t l ~> l' THEN (data l')=Tcons (data t) (data l).
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque hTcons.
-Hint Resolve hTcons_correct: wlp.
-
-(* Second, we use these hashed constructors ! *)
-
-
-Record hdeps:= {hpre: list (hashV tree); hpost: Dict.t (hashV tree)}.
-
-Coercion hpost: hdeps >-> Dict.t.
-
-(* pseudo deps_get *)
-Definition pdeps_get (d:Dict.t (hashV tree)) x : tree := 
-   match Dict.get d x with 
-   | None => Tname x
-   | Some t => (data t)
-   end.
-
-Definition hdeps_get (d:hdeps) x dbg : ?? hashV tree := 
-   match Dict.get d x with 
-   | None => hTname x dbg
-   | Some t => RET t
-   end.
-
-Lemma hdeps_get_correct (d:hdeps) x dbg:
-  WHEN hdeps_get d x dbg ~> t THEN (data t) = pdeps_get d x.
-Proof.
-  unfold hdeps_get, pdeps_get; destruct (Dict.get d x); wlp_simplify.
-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 <-> valid ge d m) 
-  /\ (forall m x, valid ge d m -> tree_eval ge (pdeps_get hd x) m = (deps_eval ge d x m)).
-
-Lemma deps_model_valid_alt ge d hd: deps_model ge d hd -> 
- forall m x, valid ge d m -> tree_eval ge (pdeps_get hd x) m <> None.
-Proof.
-  intros (H1 & H2) m x H. rewrite H2; auto.
-  unfold valid in H. intuition eauto.
-Qed.
-
-Lemma deps_model_hdeps_valid_alt ge d hd: deps_model ge d hd -> 
- forall m x, hdeps_valid ge hd m -> tree_eval ge (pdeps_get hd x) m <> None.
-Proof.
-  intros (H1 & H2) m x H. eapply deps_model_valid_alt.
-  - split; eauto.
-  - rewrite <- H1; auto.
-Qed.
-
-Fixpoint hexp_tree (e: exp) (d od: hdeps) (dbg: option pstring) : ?? hashV tree :=
-  match e with
-  | PReg x => hdeps_get d x dbg
-  | Op o le =>
-     DO lt <~ hlist_exp_tree le d od;; 
-     hTop o lt dbg
-  | Old e => hexp_tree e od od dbg
-  end
-with hlist_exp_tree (le: list_exp) (d od: hdeps): ?? hashV list_tree :=
-  match le with
-  | Enil => hTnil tt
-  | Econs e le' => 
-     DO t <~ hexp_tree e d od None;;
-     DO lt <~ hlist_exp_tree le' d od;;
-     hTcons t lt
-  | LOld le => hlist_exp_tree le od od
-  end.
-
-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, valid ge d m -> valid ge od 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 d hd,
-     deps_model ge d hd ->
-     WHEN hlist_exp_tree le hd hod ~> lt THEN forall m, valid ge d m -> valid ge od 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.
-  - rewrite H1, H4; auto.
-  - rewrite H4, <- H0; simpl; auto.
-  - rewrite H1; simpl; auto.
-  - rewrite H5, <- H0, <- H4; simpl; auto.
-Qed.
-Global Opaque hexp_tree.
-
-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 -> valid ge d m -> valid ge od m -> tree_eval ge (data t) m = tree_eval ge (exp_tree e d od) m.
-Proof.
-  unfold wlp; intros; eapply hexp_tree_correct_x; eauto.
-Qed.
-Hint Resolve hexp_tree_correct: wlp.
-
-Definition failsafe (t: tree): bool :=
-  match t with
-  | Tname x => true
-  | Top o Tnil => is_constant o
-  | _ => false
-  end.
-
-Local Hint Resolve is_constant_correct.
-
-Lemma failsafe_correct ge (t: tree) m: failsafe t = true -> tree_eval ge t m <> None.
-Proof.
-  destruct t; simpl; try congruence.
-  destruct l; simpl; try congruence.
-  eauto.
-Qed.
-Local Hint Resolve failsafe_correct.
-
-Definition naive_set (hd:hdeps) x (t:hashV tree) := 
-  {| hpre:= t::hd.(hpre); hpost:=Dict.set hd x t |}.
-
-Lemma naive_set_correct hd x ht ge d t:
-    deps_model ge d hd ->
-    (forall m, valid ge d m -> tree_eval ge (data ht) m = tree_eval ge t m) ->
-    deps_model ge (deps_set d x t) (naive_set hd x ht).
-Proof.
-  unfold naive_set; intros (DM0 & DM1) EQT; split.
-  - intros m.
-    destruct (DM0 m) as (PRE & VALID0); clear DM0.
-    assert (VALID1: hdeps_valid ge hd m -> pre d ge m). { unfold valid in PRE; tauto. }
-    assert (VALID2: hdeps_valid ge hd m -> forall x : Dict.R.t, deps_eval ge d x m <> None). { unfold valid in PRE; tauto. }
-    unfold hdeps_valid in * |- *; simpl.
-    intuition (subst; eauto).
-    + eapply valid_set_proof; eauto.
-      erewrite <- EQT; eauto.
-    + exploit valid_set_decompose_1; eauto.
-      intros X1; exploit valid_set_decompose_2; eauto.
-      rewrite <- EQT; eauto.
-    + exploit valid_set_decompose_1; eauto.
-  - clear DM0. unfold deps_eval, pdeps_get, deps_get in * |- *; simpl.
-    Local Hint Resolve valid_set_decompose_1.
-    intros; case (R.eq_dec x x0).
-    + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto.
-    + intros; rewrite !Dict.set_spec_diff; simpl; eauto.
-Qed.
-Local Hint Resolve naive_set_correct.
-
-Definition equiv_hdeps ge (hd1 hd2: hdeps) := 
-      (forall m, hdeps_valid ge hd1 m <-> hdeps_valid ge hd2 m)
-   /\ (forall m x, hdeps_valid ge hd1 m -> tree_eval ge (pdeps_get hd1 x) m = tree_eval ge (pdeps_get hd2 x) m).
-
-Lemma equiv_deps_symmetry ge hd1 hd2:
-  equiv_hdeps ge hd1 hd2 -> equiv_hdeps ge hd2 hd1.
-Proof.
-  intros (V1 & P1); split.
-  - intros; symmetry; auto.
-  - intros; symmetry; eapply P1. rewrite V1; auto.
-Qed.
-
-Lemma equiv_hdeps_models ge hd1 hd2 d: 
-   deps_model ge d hd1 -> equiv_hdeps ge hd1 hd2 -> deps_model ge d hd2.
-Proof.
-  intros (VALID & EQUIV) (HEQUIV & PEQUIV); split.
-  - intros m; rewrite <- VALID; auto. symmetry; auto.
-  - intros m x H. rewrite <- EQUIV; auto. 
-    rewrite PEQUIV; auto.
-    rewrite VALID; auto.
-Qed.
-
-Definition hdeps_set (hd:hdeps) x (t:hashV tree) :=
-     DO ot <~ hdeps_get hd x None;;
-     DO b <~ phys_eq ot t;;
-     if b then
-        RET hd
-     else
-        RET {| hpre:= if failsafe (data t) then hd.(hpre) else t::hd.(hpre);
-               hpost:=Dict.set hd 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, valid ge d m -> tree_eval ge (data ht) m = tree_eval ge t m) ->
-    deps_model ge (deps_set d x t) nhd.
-Proof.
-  intros; wlp_simplify; eapply equiv_hdeps_models; eauto; unfold equiv_hdeps, hdeps_valid; simpl.
-  + split; eauto.
-    * intros m; split.
-      - intros X1 ht0 X2; apply X1; auto.
-      - intros X1 ht0 [Y1 | Y1]. subst.
-        rewrite H; eapply deps_model_hdeps_valid_alt; eauto.
-        eauto.
-    * intros m x0 X1. case (R.eq_dec x x0).
-      - intros; subst. unfold pdeps_get at 1. rewrite Dict.set_spec_eq. congruence.
-      - intros; unfold pdeps_get; rewrite Dict.set_spec_diff; auto.
-  + split; eauto. intros m.
-    generalize (failsafe_correct ge (data ht) m); intros FAILSAFE.
-    destruct (failsafe _); simpl; intuition (subst; eauto).
-Qed.
-Local Hint Resolve hdeps_set_correct: wlp.
-Global Opaque hdeps_set.
-
-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 hd hod,
-  WHEN hinst_deps i hd hod ~> hd' THEN
-    forall ge od d, deps_model ge od hod -> deps_model ge d hd -> (forall m, valid ge d m -> valid ge od m) -> deps_model ge (inst_deps i d od) hd'.
-Proof.
-  Local Hint Resolve valid_set_proof.
-  induction i; simpl; wlp_simplify; eauto 20.
-Qed.
-Global Opaque hinst_deps.
-Local Hint Resolve hinst_deps_correct: wlp.
-
-(* logging info: we log the number of inst-instructions passed ! *)
-Variable log: unit -> ?? unit. 
-
-Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps :=
-  match p with
-  | nil => RET d
-  | i::p' =>
-     log tt;;
-     DO d' <~ hinst_deps i d d;;
-     hbblock_deps_rec p' d'
-  end.
-
-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.
-Local Hint Resolve hbblock_deps_rec_correct: wlp.
-
-
-Definition hbblock_deps: bblock -> ?? hdeps
- := fun p => hbblock_deps_rec p {| hpre:= nil ; hpost := Dict.empty |}.
-
-Lemma hbblock_deps_correct p:
-  WHEN hbblock_deps p ~> hd THEN forall ge, deps_model ge (bblock_deps p) hd.
-Proof.
-  unfold bblock_deps; wlp_simplify. eapply H. clear H.
-  unfold deps_model, valid, pdeps_get, hdeps_valid, deps_eval, deps_get; simpl; intuition;
-  rewrite !Dict.empty_spec in * |- *; simpl in * |- *; try congruence.
-Qed.
-Global Opaque hbblock_deps.
-
-End CanonBuilding.
-
-(* Now, we build the hash-Cons value from a "hash_eq".
-
-Informal specification: 
-  [hash_eq] must be consistent with the "hashed" constructors defined above.
-
-We expect that pre_hashV values in the code of these "hashed" constructors verify:
-
-  (hash_eq (pre_data x) (pre_data y) ~> true) <-> (hcodes x)=(hcodes y)    
-
-*)
-
-Definition tree_hash_eq (ta tb: tree): ?? bool := 
-  match ta, tb with
-  | Tname xa, Tname xb =>
-     if R.eq_dec xa xb  (* Inefficient in some cases ? *)
-     then RET true
-     else RET false
-  | Top oa lta, Top ob ltb => 
-     DO b <~ op_eq oa ob ;;
-     if b then phys_eq lta ltb
-     else RET false
-  | _,_ => RET false
-  end.
-
-Local Hint Resolve op_eq_correct: wlp.
-
-Lemma tree_hash_eq_correct: forall ta tb, WHEN tree_hash_eq ta tb ~> b THEN b=true -> ta=tb.
-Proof.
-  destruct ta, tb; wlp_simplify; (discriminate || (subst; auto)).
-Qed.
-Global Opaque tree_hash_eq.
-Hint Resolve tree_hash_eq_correct: wlp.
-
-Definition list_tree_hash_eq (lta ltb: list_tree): ?? bool := 
-  match lta, ltb with
-  | Tnil, Tnil => RET true
-  | Tcons ta lta, Tcons tb ltb => 
-      DO b <~ phys_eq ta tb ;;
-     if b then phys_eq lta ltb
-     else RET false
-  | _,_ => RET false
-  end.
-
-Lemma list_tree_hash_eq_correct: forall lta ltb, WHEN list_tree_hash_eq lta ltb ~> b THEN b=true -> lta=ltb.
-Proof.
-  destruct lta, ltb; wlp_simplify; (discriminate || (subst; auto)).
-Qed.
-Global Opaque list_tree_hash_eq.
-Hint Resolve list_tree_hash_eq_correct: wlp.
-
-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.
-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 !!! ***)
-
-Section Prog_Eq_Gen.
-
-Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 insts *)
-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.
-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 (
-      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, _ =>
-    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 [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 m; rewrite <- EQPRE1, <- EQPRE2.
-    unfold incl, hdeps_valid in * |- *; intuition eauto.
-  + intros m0 x m1 VALID; rewrite <- EQPOST1, <- EQPOST2; auto.
-    erewrite pdeps_get_intro; auto.
-    auto.
-    erewrite <- EQPRE2; auto.
-    erewrite <- EQPRE1 in VALID.
-    unfold incl, hdeps_valid in * |- *; intuition eauto.
-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 exta0; simpl in * |- *; auto.
-Qed.
-Global Opaque g_bblock_simu_test.
-
-End Prog_Eq_Gen.
-
-
-
-Definition skip (_:unit): ?? unit := RET tt.
-Definition no_dbg (_:R.t): ?? option pstring := RET None.
-
-
-Definition msg_prefix: pstring := "*** ERROR INFO from bblock_simu_test: ".
-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).
-
-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)
-    true (* check_failpreserv *)
-    failpreserv_error
-    p1 p2.
-Obligation 1.
-  generalize (hCons_correct _ _ _ _ H0); clear H0.
-  constructor 1; wlp_simplify.
-Qed.
-Obligation 2.
-  generalize (hCons_correct _ _ _ _ H); clear H.
-  constructor 1; wlp_simplify.
-Qed.
-
-Local Hint Resolve g_bblock_simu_test_correct.
-
-Theorem bblock_simu_test_correct p1 p2:
-  WHEN bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque bblock_simu_test.
-
-
-
-(** This is only to print info on each bblock_simu_test run **)
-Section Verbose_version.
-
-Variable string_of_name: R.t -> ?? pstring.
-Variable string_of_op: op -> ?? pstring.
-
-Definition tree_id (id: caml_string): pstring := "E" +; (CamlStr id).
-Definition list_id (id: caml_string): pstring := "L" +; (CamlStr id).
-
-Local Open Scope string_scope.
-
-Definition print_raw_htree (td: pre_hashV tree): ?? unit :=
-  match pre_data td, hcodes td with
-  | (Tname x), _ => 
-    DO s <~ string_of_name x;;
-    println( "init_access " +; s)
-  | (Top o Tnil), _ => 
-    DO so <~ string_of_op o;;
-    println so
-  | (Top o _), [ _; _; lid ] =>
-    DO so <~ string_of_op o;;
-    DO sl <~ string_of_hashcode lid;;
-    println (so +; " " +; (list_id sl))
-  | _, _ => FAILWITH "unexpected hcodes"
-  end.
-
-Definition print_raw_hlist(ld: pre_hashV list_tree): ?? unit :=
-  match pre_data ld, hcodes ld with
-  | Tnil, _ => println ""
-  | (Tcons _ _), [ t ; l ] =>
-    DO st <~ string_of_hashcode t ;;
-    DO sl <~ string_of_hashcode l ;;
-    println((tree_id st) +; " " +; (list_id sl))
-  | _, _ => FAILWITH "unexpected hcodes"
-  end.
-
-Section PrettryPrint.
-
-Variable get_htree: hashcode -> ?? pre_hashV tree. 
-Variable get_hlist: hashcode -> ?? pre_hashV list_tree.
-
-(* NB: requires [t = pre_data pt] *)
-Fixpoint string_of_tree (t: tree) (pt: pre_hashV tree) : ?? pstring :=
-  match debug_info pt with
-  | Some x => RET x
-  | None => 
-    match t, hcodes pt with
-    | Tname x, _ => string_of_name x
-    | Top o Tnil, _ => string_of_op o
-    | Top o (_ as l), [ _; _; lid ] => 
-      DO so <~ string_of_op o;;
-      DO pl <~ get_hlist lid;;
-      DO sl <~ string_of_list_tree l pl;;
-      RET (so +; "(" +; sl +; ")")
-    | _, _ => FAILWITH "unexpected hcodes"
-    end
-  end
-(* NB: requires [l = pre_data pl] *)
-with string_of_list_tree (l: list_tree) (lt: pre_hashV list_tree): ?? pstring :=
-  match l, hcodes lt with
-  | Tnil, _ => RET (Str "")
-  | Tcons t Tnil, [ tid ; l ] => 
-     DO pt <~ get_htree tid;;
-     string_of_tree t pt
-  | Tcons t l', [ tid ; lid' ] => 
-     DO pt <~ get_htree tid;;
-     DO st <~ string_of_tree t pt;;
-     DO pl' <~ get_hlist lid';;
-     DO sl <~ string_of_list_tree l' pl';;
-     RET (st +; "," +; sl)
-    | _, _ => FAILWITH "unexpected hcodes"
-  end.
-
-
-End PrettryPrint.
-
-
-Definition pretty_tree ext exl pt :=
-  DO r <~ string_of_tree (get_hashV ext) (get_hashV exl) (pre_data pt) pt;;
-  println(r).
-
-Fixpoint print_head (head: list pstring): ?? unit :=
-  match head with
-  | i::head' => println ("--- inst " +; i);; print_head head'
-  | _ => RET tt
-  end.
-
-Definition print_htree ext exl (head: list pstring) (hid: hashcode) (td: pre_hashV tree): ?? unit :=
-  print_head head;;
-  DO s <~ string_of_hashcode hid ;;
-  print ((tree_id s) +; ": ");;
-  print_raw_htree td;;
-  match debug_info td with
-  | Some x => 
-     print("//  " +; x +; " <- ");;
-     pretty_tree ext exl {| pre_data:=(pre_data td); hcodes:=(hcodes td); debug_info:=None |}
-  | None => RET tt
-  end.
-
-Definition print_hlist (head: list pstring) (hid: hashcode) (ld: pre_hashV list_tree): ?? unit :=
-  print_head head;;
-  DO s <~ string_of_hashcode hid ;;
-  print ((list_id s) +; ": ");;
-  print_raw_hlist ld.
-
-Definition print_tables ext exl: ?? unit :=
-  println "-- tree table --" ;;
-  iterall ext (print_htree ext exl);;
-  println "-- list table --" ;;
-  iterall exl print_hlist;;
-  println "----------------".
-
-Definition print_final_debug ext exl (d1 d2: hdeps): ?? unit 
- := DO b <~ Dict.not_eq_witness d1 d2 ;;
-    match b with
-    | Some x =>
-      DO s <~ string_of_name x;;
-      println("mismatch on: " +; s);;
-      match Dict.get d1 x with 
-      | None => println("=> unassigned in 1st bblock")
-      | Some ht1 =>
-         print("=> node expected from 1st bblock: ");;
-         DO pt1 <~ get_hashV ext (hid ht1);;
-         pretty_tree ext exl pt1
-      end;;
-      match Dict.get d2 x with 
-      | None => println("=> unassigned in 2nd bblock")
-      | Some ht2 =>
-         print("=> node found from 2nd bblock: ");;
-         DO pt2 <~ get_hashV ext (hid ht2);;
-         pretty_tree ext exl pt2
-      end
-    | None => FAILWITH "bug in Dict.not_eq_witness ?"
-    end.
-
-Inductive witness:=
-  | Htree (pt: pre_hashV tree)
-  | Hlist (pl: pre_hashV list_tree)
-  | Nothing
-  .
-
-Definition msg_tree (cr: cref witness) td :=
-  set cr (Htree td);;
-  RET msg_unknow_tree.
-
-Definition msg_list (cr: cref witness) tl := 
-  set cr (Hlist tl);;
-  RET msg_unknow_list_tree.
-
-Definition print_witness ext exl cr msg :=
-  DO wit <~ get cr ();;
-  match wit with
-  | Htree pt =>
-     println("=> unknown tree node: ");;
-     pretty_tree ext exl {| pre_data:=(pre_data pt); hcodes:=(hcodes pt); debug_info:=None |};;
-     println("=> encoded on " +; msg +; " graph as: ");;
-     print_raw_htree pt
-  | Hlist pl =>
-     println("=> unknown list node: ");;
-     DO r <~ string_of_list_tree (get_hashV ext) (get_hashV exl) (pre_data pl) pl;;
-     println(r);;
-     println("=> encoded on " +; msg +; " graph as: ");;
-     print_raw_hlist pl
-  | _ => println "Unexpected failure: no witness info (hint: hash-consing bug ?)"
-  end.
-
-
-Definition print_error_end1 hct hcl (d1 d2:hdeps): ?? unit
- := println "- GRAPH of 1st bblock";;
-    DO ext <~ export hct ();;
-    DO exl <~ export hcl ();;
-    print_tables ext exl;;
-    print_error_end d1 d2;;
-    print_final_debug ext exl d1 d2.
-
-Definition print_error1  hct hcl cr log s : ?? unit
- := println "- GRAPH of 1st bblock";;
-    DO ext <~ export hct ();;
-    DO exl <~ export hcl ();;
-    print_tables ext exl;;
-    print_error log s;;
-    print_witness ext exl cr "1st".
-
-
-Definition xmsg_number: pstring := "on 1st bblock -- on inst num ".
-
-Definition print_error_end2 hct hcl (d1 d2:hdeps): ?? unit
- := println (msg_prefix +; msg_error_on_end);;
-    println "- GRAPH of 2nd bblock";;
-    DO ext <~ export hct ();;
-    DO exl <~ export hcl ();;
-    print_tables ext exl.
-
-Definition print_error2 hct hcl cr (log: logger unit) (s:pstring): ?? unit
- := DO n <~ log_info log ();;
-    DO ext <~ export hct ();;
-    DO exl <~ export hcl ();;
-    println (msg_prefix +; xmsg_number +; n +; " -- " +; s);;
-    print_witness ext exl cr "2nd";;
-    println "- GRAPH of 2nd bblock";;
-    print_tables ext exl.
-
-Definition simple_debug (x: R.t): ?? option pstring :=
-  DO s <~ string_of_name x;;
-  RET (Some s).
-
-Definition log_debug (log: logger unit) (x: R.t): ?? option pstring :=
-  DO i <~ log_info log ();;
-  DO sx <~ string_of_name x;;
-  RET (Some (sx +; "@" +; i)).
-
-Definition hlog (log: logger unit) (hct: hashConsing tree) (hcl: hashConsing list_tree): unit -> ?? unit :=
-   (fun _ =>
-      log_insert log tt ;;
-      DO s <~ log_info log tt;;
-      next_log hct s;;
-      next_log hcl s
-    ).
-
-Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
-  DO log1 <~ count_logger ();;
-  DO log2 <~ count_logger ();;
-  DO cr <~ make_cref Nothing;;
-  DO hco_tree <~ mk_annot (hCons tree_hash_eq (msg_tree cr));;
-  DO hco_list <~ mk_annot (hCons list_tree_hash_eq (msg_list cr));;
-  DO result1 <~ g_bblock_simu_test
-     (log_debug log1)
-     simple_debug
-     (hlog log1 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)
-     true
-     failpreserv_error (* TODO: debug info *)
-     p1 p2;;
-  if result1 
-  then RET true
-  else
-    DO log1 <~ count_logger ();;
-    DO log2 <~ count_logger ();;
-    DO cr <~ make_cref Nothing;;
-    DO hco_tree <~ mk_annot (hCons tree_hash_eq (msg_tree cr));;
-    DO hco_list <~ mk_annot (hCons list_tree_hash_eq (msg_list cr));;
-    DO result2 <~ g_bblock_simu_test 
-       (log_debug log1)
-       simple_debug
-       (hlog log1 hco_tree hco_list)
-       (log_insert log2)
-       hco_tree _
-       hco_list _
-       (print_error_end2 hco_tree hco_list)
-       (print_error2 hco_tree hco_list cr log2)
-       false
-       (fun _ => RET tt)
-       p2 p1;;
-    if result2 
-    then (
-      println (msg_prefix +; " OOops - symmetry violation in bblock_simu_test  => this is a bug of bblock_simu_test ??");;
-      RET false
-    ) else RET false
-   .
-Obligation 1.  
-  generalize (hCons_correct _ _ _ _ H0); clear H0.
-  constructor 1; wlp_simplify.
-Qed.
-Obligation 2.  
-  generalize (hCons_correct _ _ _ _ H); clear H.
-  constructor 1; wlp_simplify.
-Qed.
-Obligation 3.  
-  generalize (hCons_correct _ _ _ _ H0); clear H0.
-  constructor 1; wlp_simplify.
-Qed.
-Obligation 4.  
-  generalize (hCons_correct _ _ _ _ H); clear H.
-  constructor 1; wlp_simplify.
-Qed.
-
-Theorem verb_bblock_simu_test_correct p1 p2:
-  WHEN verb_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque verb_bblock_simu_test.
-
-End Verbose_version.
-
-
-End ImpDepTree.
-
-Require Import FMapPositive.
-
-Module ImpPosDict <: ImpDict with Module R:=Pos.
-
-Include PosDict.
-Import PositiveMap.
-
-Fixpoint eq_test {A} (d1 d2: t A): ?? bool :=
-  match d1, d2 with
-  | Leaf _, Leaf _ => RET true
-  | Node l1 (Some x1) r1, Node l2 (Some x2) r2 =>
-      DO b0 <~ phys_eq x1 x2 ;;
-      if b0 then
-        DO b1 <~ eq_test l1 l2 ;;
-        if b1 then
-          eq_test r1 r2
-        else
-           RET false
-      else
-         RET false
-  | Node l1 None r1, Node l2 None r2 =>
-      DO b1 <~ eq_test l1 l2 ;;
-      if b1 then
-        eq_test r1 r2
-      else
-        RET false
-  | _, _ => RET false
-  end.
-
-Lemma eq_test_correct A d1: forall (d2: t A),
- WHEN eq_test d1 d2 ~> b THEN
-  b=true -> forall x, get d1 x = get d2 x.
-Proof.
-  unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; simpl; 
-  wlp_simplify; (discriminate || (subst; destruct x; simpl; auto)).
-Qed.
-Global Opaque eq_test.
-
-(* 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"
-  | Node _ (Some _) _ => RET xH
-  | Node (Leaf _) None r => 
-    DO p <~ pick r;;
-    RET (xI p)
-  | Node l None _ =>
-    DO p <~ pick l;;
-    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
-  | Node l1 (Some x1) r1, Node l2 (Some x2) r2 =>
-      DO b0 <~ phys_eq x1 x2 ;;
-      if b0 then
-        DO b1 <~ not_eq_witness l1 l2;;
-        match b1 with
-        | None => 
-          DO b2 <~ not_eq_witness r1 r2;;
-          match b2 with
-          | None => RET None
-          | Some p => RET (Some (xI p))
-          end
-        | Some p => RET (Some (xO p))
-        end
-      else
-         RET (Some xH)
-  | Node l1 None r1, Node l2 None r2 =>
-        DO b1 <~ not_eq_witness l1 l2;;
-        match b1 with
-        | None => 
-          DO b2 <~ not_eq_witness r1 r2;;
-          match b2 with
-          | None => RET None
-          | Some p => RET (Some (xI p))
-          end
-        | Some p => RET (Some (xO p))
-        end
-  | l, Leaf _ => DO p <~ pick l;; RET (Some p)
-  | Leaf _, r => DO p <~ pick r;; RET (Some p)
-  | _, _ => RET (Some xH)
-  end.
-
-End ImpPosDict.
-
diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v
new file mode 100644
index 00000000..ea55b735
--- /dev/null
+++ b/mppa_k1c/abstractbb/ImpSimuTest.v
@@ -0,0 +1,1246 @@
+(** Implementation of a symbolic execution of sequential semantics of Abstract Basic Blocks
+
+with imperative hash-consing, and rewriting.
+
+*)
+
+Require Export Impure.ImpHCons.
+Export Notations.
+Import HConsing.
+
+
+Require Export SeqSimuTheory.
+
+Require Import PArith.
+
+
+Local Open Scope impure.
+
+Import ListNotations.
+Local Open Scope list_scope.
+
+
+Module Type ImpParam.
+
+Include LangParam.
+
+Parameter op_eq: op -> op -> ?? bool.
+
+Parameter op_eq_correct: forall o1 o2, 
+ WHEN op_eq o1 o2 ~> b THEN
+  b=true -> o1 = o2.
+
+End ImpParam.
+
+
+Module Type ISeqLanguage.
+
+Declare Module LP: ImpParam.
+
+Include MkSeqLanguage LP.
+
+End ISeqLanguage.
+
+
+Module Type ImpDict.
+
+Declare Module R: PseudoRegisters.
+
+Parameter t: Type -> Type.
+
+Parameter get: forall {A}, t A -> R.t -> option A.
+
+Parameter set: forall {A}, t A -> R.t -> A -> t A.
+
+Parameter set_spec_eq: forall A d x (v: A),
+  get (set d x v) x = Some v.
+
+Parameter set_spec_diff: forall A d x y (v: A),
+  x <> y -> get (set d x v) y = get d y.
+
+Parameter rem: forall {A}, t A -> R.t -> t A.
+
+Parameter rem_spec_eq: forall A (d: t A) x,
+  get (rem d x) x = None.
+
+Parameter rem_spec_diff: forall A (d: t A) x y,
+  x <> y -> get (rem d x) y = get d y.
+
+Parameter empty: forall {A}, t A.
+
+Parameter empty_spec: forall A x,
+  get (empty (A:=A)) x = None.
+
+Parameter eq_test: forall {A}, t A -> t A -> ?? bool.
+
+Parameter eq_test_correct: forall A (d1 d2: t A),
+ WHEN eq_test d1 d2 ~> b THEN
+  b=true -> forall x, get d1 x = get d2 x.
+
+(* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries  *)
+
+
+(* only for debugging *)
+Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t.
+
+End ImpDict.
+
+
+Module Type ImpSimuInterface.
+
+Declare Module CoreL: ISeqLanguage.
+Import CoreL.
+Import Terms.
+
+Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool.
+
+Parameter bblock_simu_test_correct: forall reduce (p1 p2 : bblock),
+    WHEN bblock_simu_test reduce p1 p2 ~> b
+    THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.
+
+
+Parameter verb_bblock_simu_test
+     : reduction ->
+       (R.t -> ?? pstring) ->
+       (op -> ?? pstring) -> bblock -> bblock -> ?? bool.
+
+Parameter verb_bblock_simu_test_correct: 
+   forall reduce
+          (string_of_name : R.t -> ?? pstring)
+          (string_of_op : op -> ?? pstring) 
+          (p1 p2 : bblock),
+    WHEN verb_bblock_simu_test reduce string_of_name string_of_op p1 p2 ~> b
+    THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.
+
+End ImpSimuInterface.
+
+
+
+Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuInterface with Module CoreL := L.
+
+Module CoreL:=L.
+
+Module ST := SimuTheory L.
+
+Import ST.
+Import Terms.
+
+Definition term_set_hid (t: term) (hid: hashcode): term :=
+  match t with
+  | Input x _ => Input x hid
+  | App op l _ => App op l hid
+  end.
+
+Definition list_term_set_hid (l: list_term) (hid: hashcode): list_term :=
+  match l with
+  | LTnil _ => LTnil hid
+  | LTcons t l' _ => LTcons t l' hid
+  end.
+
+Lemma term_eval_set_hid ge t hid m:
+  term_eval ge (term_set_hid t hid) m = term_eval ge t m.
+Proof.
+  destruct t; simpl; auto.
+Qed.
+
+Lemma list_term_eval_set_hid ge l hid m:
+  list_term_eval ge (list_term_set_hid l hid) m = list_term_eval ge l m.
+Proof.
+  destruct l; simpl; auto.
+Qed.
+
+(* Local nickname *)
+Module D:=ImpPrelude.Dict.
+
+Section SimuWithReduce.
+
+Variable reduce: reduction.
+
+Section CanonBuilding.
+
+Variable hC_term: hashinfo term -> ?? term.
+Hypothesis hC_term_correct: forall t, WHEN hC_term t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.
+
+Variable hC_list_term: hashinfo list_term -> ?? list_term.
+Hypothesis hC_list_term_correct: forall t, WHEN hC_list_term t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m.
+
+(* First, we wrap constructors for hashed values !*)
+
+Local Open Scope positive.
+Local Open Scope list_scope.
+
+Definition hInput_hcodes (x:R.t) :=
+   DO hc <~ hash 1;;
+   DO hv <~ hash x;;
+   RET [hc;hv].
+Extraction Inline hInput_hcodes.
+
+Definition hInput (x:R.t): ?? term :=
+   DO hv <~ hInput_hcodes x;;
+   hC_term {| hdata:=Input x unknown_hid; hcodes :=hv; |}.
+
+Lemma hInput_correct x:
+  WHEN hInput x ~> t THEN forall ge m, term_eval ge t m = Some (m x).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hInput.
+Hint Resolve hInput_correct: wlp.
+
+Definition hApp_hcodes (o:op) (l: list_term) :=
+   DO hc <~ hash 2;;
+   DO hv <~ hash o;;
+   RET [hc;hv;list_term_get_hid l].
+Extraction Inline hApp_hcodes.
+
+Definition hApp (o:op) (l: list_term) : ?? term :=
+   DO hv <~ hApp_hcodes o l;;
+   hC_term {| hdata:=App o l unknown_hid; hcodes:=hv |}.
+
+Lemma hApp_correct o l:
+  WHEN hApp o l ~> t THEN forall ge m,
+    term_eval ge t m = match list_term_eval ge l m with
+                       | Some v => op_eval ge o v
+                       | None => None
+                       end.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hApp.
+Hint Resolve hApp_correct: wlp.
+
+Definition hLTnil (_: unit): ?? list_term :=
+   hC_list_term {| hdata:=LTnil unknown_hid; hcodes := nil; |} .
+
+Lemma hLTnil_correct x: 
+  WHEN hLTnil x ~> l THEN forall ge m, list_term_eval ge l m = Some nil.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hLTnil.
+Hint Resolve hLTnil_correct: wlp.
+
+
+Definition hLTcons (t: term) (l: list_term): ?? list_term :=
+   hC_list_term {| hdata:=LTcons t l unknown_hid; hcodes := [term_get_hid t; list_term_get_hid l]; |}.
+
+Lemma hLTcons_correct t l:
+  WHEN hLTcons t l ~> l' THEN forall ge m, 
+     list_term_eval ge l' m = match term_eval ge t m, list_term_eval ge l m with
+                              | Some v, Some lv => Some (v::lv)
+                              | _, _ => None
+                              end.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hLTcons.
+Hint Resolve hLTcons_correct: wlp.
+
+(* Second, we use these hashed constructors ! *)
+
+Record hsmem:= {hpre: list term; hpost:> Dict.t term}.
+
+(** evaluation of the post-condition *)
+Definition hsmem_post_eval ge (hd: Dict.t term) x (m:mem) :=
+   match Dict.get hd x with 
+   | None => Some (m x)
+   | Some ht => term_eval ge ht m
+   end.
+
+Definition hsmem_get (d:hsmem) x: ?? term :=
+   match Dict.get d x with 
+   | None => hInput x
+   | Some t => RET t
+   end.
+
+Lemma hsmem_get_correct (d:hsmem) x:
+  WHEN hsmem_get d x ~> t THEN forall ge m, term_eval ge t m = hsmem_post_eval ge d x m.
+Proof.
+  unfold hsmem_get, hsmem_post_eval; destruct (Dict.get d x); wlp_simplify.
+Qed.
+Global Opaque hsmem_get.
+Hint Resolve hsmem_get_correct: wlp.
+
+Local Opaque allvalid.
+
+Definition smem_model ge (d: smem) (hd:hsmem): Prop :=
+  (forall m, allvalid ge hd.(hpre) m <-> smem_valid ge d m) 
+  /\ (forall m x, smem_valid ge d m -> hsmem_post_eval ge hd x m = (ST.term_eval ge (d x) m)).
+
+Lemma smem_model_smem_valid_alt ge d hd: smem_model ge d hd -> 
+ forall m x, smem_valid ge d m -> hsmem_post_eval ge hd x m <> None.
+Proof.
+  intros (H1 & H2) m x H. rewrite H2; auto.
+  unfold smem_valid in H. intuition eauto.
+Qed.
+
+Lemma smem_model_allvalid_alt ge d hd: smem_model ge d hd -> 
+ forall m x, allvalid ge hd.(hpre) m -> hsmem_post_eval ge hd x m <> None.
+Proof.
+  intros (H1 & H2) m x H. eapply smem_model_smem_valid_alt.
+  - split; eauto.
+  - rewrite <- H1; auto.
+Qed.
+
+Definition naive_set (hd:hsmem) x (t:term) := 
+  {| hpre:= t::hd.(hpre); hpost:=Dict.set hd x t |}.
+
+Lemma naive_set_correct hd x ht ge d t:
+    smem_model ge d hd ->
+    (forall m, smem_valid ge d m -> term_eval ge ht m = ST.term_eval ge t m) ->
+    smem_model ge (smem_set d x t) (naive_set hd x ht).
+Proof.
+  unfold naive_set; intros (DM0 & DM1) EQT; split.
+  - intros m.
+    destruct (DM0 m) as (PRE & VALID0); clear DM0.
+    assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. }
+    assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, ST.term_eval ge (d x) m <> None). { unfold smem_valid in PRE; tauto. }
+    rewrite !allvalid_extensionality in * |- *; simpl.
+    intuition (subst; eauto).
+    + eapply smem_valid_set_proof; eauto.
+      erewrite <- EQT; eauto.
+    + exploit smem_valid_set_decompose_1; eauto.
+      intros X1; exploit smem_valid_set_decompose_2; eauto.
+      rewrite <- EQT; eauto.
+    + exploit smem_valid_set_decompose_1; eauto.
+  - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl.
+    Local Hint Resolve smem_valid_set_decompose_1.
+    intros; case (R.eq_dec x x0).
+    + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto.
+    + intros; rewrite !Dict.set_spec_diff; simpl; eauto.
+Qed.
+Local Hint Resolve naive_set_correct.
+
+Definition equiv_hsmem ge (hd1 hd2: hsmem) := 
+      (forall m, allvalid ge hd1.(hpre) m <-> allvalid ge hd2.(hpre) m)
+   /\ (forall m x, allvalid ge hd1.(hpre) m -> hsmem_post_eval ge hd1 x m = hsmem_post_eval ge hd2 x m).
+
+Lemma equiv_smem_symmetry ge hd1 hd2:
+  equiv_hsmem ge hd1 hd2 -> equiv_hsmem ge hd2 hd1.
+Proof.
+  intros (V1 & P1); split.
+  - intros; symmetry; auto.
+  - intros; symmetry; eapply P1. rewrite V1; auto.
+Qed.
+
+Lemma equiv_hsmem_models ge hd1 hd2 d: 
+   smem_model ge d hd1 -> equiv_hsmem ge hd1 hd2 -> smem_model ge d hd2.
+Proof.
+  intros (VALID & EQUIV) (HEQUIV & PEQUIV); split.
+  - intros m; rewrite <- VALID; auto. symmetry; auto.
+  - intros m x H. rewrite <- EQUIV; auto. 
+    rewrite PEQUIV; auto.
+    rewrite VALID; auto.
+Qed.
+
+Variable log_assign: R.t -> term -> ?? unit.
+
+Definition lift {A B} hid (x:A) (k: B -> ?? A) (y:B): ?? A :=
+  DO b <~ phys_eq hid unknown_hid;;
+  if b then k y else RET x.
+
+Fixpoint hterm_lift (t: term): ?? term :=
+  match t with
+  | Input x hid => lift hid t hInput x
+  | App o l hid => 
+      lift hid t
+       (fun l => DO lt <~ hlist_term_lift l;;
+        hApp o lt) l
+  end
+with hlist_term_lift (l: list_term) {struct l}: ?? list_term :=
+  match l with
+  | LTnil hid => lift hid l hLTnil ()
+  | LTcons t l' hid => 
+     lift hid l
+        (fun t => DO t <~ hterm_lift t;;
+         DO lt <~ hlist_term_lift l';;
+          hLTcons t lt) t
+  end.
+
+Lemma hterm_lift_correct t:
+  WHEN hterm_lift t ~> ht THEN forall ge m, term_eval ge ht m = term_eval ge t m.
+Proof.
+  induction t using term_mut with (P0:=fun lt =>
+     WHEN hlist_term_lift lt ~> hlt THEN forall ge m, list_term_eval ge hlt m = list_term_eval ge lt m); 
+     wlp_simplify.
+  - rewrite H0, H; auto.
+  - rewrite H1, H0, H; auto.
+Qed.
+Local Hint Resolve hterm_lift_correct: wlp.
+Global Opaque hterm_lift.
+
+Variable log_new_hterm: term -> ?? unit.
+
+Fixpoint hterm_append (l: list term) (lh: list term): ?? list term :=
+  match l with
+  | nil => RET lh
+  | t::l' =>
+     DO ht <~ hterm_lift t;;
+     log_new_hterm ht;;
+     hterm_append l' (ht::lh)
+  end.
+
+Lemma hterm_append_correct l: forall lh,
+  WHEN hterm_append l lh ~> lh' THEN (forall ge m, allvalid ge lh' m <-> (allvalid ge l m /\ allvalid ge lh m)).
+Proof.
+  Local Hint Resolve eq_trans: localhint.
+  induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp).
+  - intros; rewrite! allvalid_extensionality; intuition eauto.
+  - intros REC ge m; rewrite REC; clear IHl' REC. rewrite !allvalid_extensionality.
+    simpl; intuition (subst; eauto with wlp localhint).
+Qed.
+(*Local Hint Resolve hterm_append_correct: wlp.*)
+Global Opaque hterm_append.
+
+Definition smart_set (hd:hsmem) x (ht:term) :=
+     match ht with
+     | Input y _ =>
+       if R.eq_dec x y then
+          RET (Dict.rem hd x)
+       else (
+          log_assign x ht;;
+          RET (Dict.set hd x ht)
+       )
+     | _ => 
+       log_assign x ht;;
+       RET (Dict.set hd x ht)
+     end.
+
+Lemma smart_set_correct hd x ht:
+  WHEN smart_set hd x ht ~> d THEN
+    forall ge m y, hsmem_post_eval ge d y m = hsmem_post_eval ge (Dict.set hd x ht) y m.
+Proof.
+  destruct ht; wlp_simplify.
+  unfold hsmem_post_eval; simpl. case (R.eq_dec x0 y).
+  - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. simpl; congruence.
+  - intros; rewrite Dict.set_spec_diff, Dict.rem_spec_diff; auto.
+Qed.
+(*Local Hint Resolve smart_set_correct: wlp.*)
+Global Opaque smart_set.
+
+Definition hsmem_set (hd:hsmem) x (t:term) :=
+  DO pt <~ reduce t;;
+  DO lht <~ hterm_append pt.(mayfail) hd.(hpre);;
+  DO ht <~ hterm_lift pt.(effect);;
+  log_new_hterm ht;;
+  DO nd <~ smart_set hd x ht;;
+  RET {| hpre := lht; hpost := nd |}.
+
+Lemma hsmem_set_correct hd x ht:
+  WHEN hsmem_set hd x ht ~> nhd THEN
+    forall ge d t, smem_model ge d hd ->
+    (forall m, smem_valid ge d m -> term_eval ge ht m = ST.term_eval ge t m) ->
+    smem_model ge (smem_set d x t) nhd.
+Proof.
+  intros; wlp_simplify.
+  generalize (hterm_append_correct _ _ _ Hexta0); intro APPEND.
+  generalize (hterm_lift_correct _ _ Hexta1); intro LIFT.
+  generalize (smart_set_correct _ _ _ _ Hexta3); intro SMART.
+  eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; simpl. 
+  destruct H as (VALID & EFFECT); split.
+  - intros; rewrite APPEND, <- VALID.
+    rewrite !allvalid_extensionality in * |- *; simpl; intuition (subst; eauto).
+  - intros m x0 ALLVALID; rewrite SMART.
+    destruct (term_eval ge ht m) eqn: Hht.
+    * case (R.eq_dec x x0).
+      + intros; subst. unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_eq.
+        erewrite LIFT, EFFECT; eauto.
+      + intros; unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_diff; auto.
+    * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto.
+Qed.
+Local Hint Resolve hsmem_set_correct: wlp.
+Global Opaque hsmem_set.
+
+(* VARIANTE: we do not hash-cons the term from the expression
+Lemma exp_hterm_correct ge e hod od:
+  smem_model ge od hod ->
+ forall hd d,
+  smem_model ge d hd ->
+  forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge (exp_term e hd hod) m = term_eval ge (exp_term e d od) m.
+Proof.
+  intro H.
+  induction e using exp_mut with (P0:=fun le =>  forall d hd,
+     smem_model ge d hd -> forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge (list_exp_term le hd hod) m = list_term_eval ge (list_exp_term le d od) m); 
+     unfold smem_model in * |- * ; simpl; intuition eauto.
+  - erewrite IHe; eauto.
+  - erewrite IHe0, IHe; eauto.
+Qed.
+Local Hint Resolve exp_hterm_correct: wlp.
+*)
+
+Fixpoint exp_hterm (e: exp) (hd hod: hsmem): ?? term :=
+  match e with
+  | PReg x => hsmem_get hd x
+  | Op o le =>
+     DO lt <~ list_exp_hterm le hd hod;; 
+     hApp o lt
+  | Old e => exp_hterm e hod hod
+  end
+with list_exp_hterm (le: list_exp) (hd hod: hsmem): ?? list_term :=
+  match le with
+  | Enil => hLTnil tt
+  | Econs e le' => 
+     DO t <~ exp_hterm e hd hod;;
+     DO lt <~ list_exp_hterm le' hd hod;;
+     hLTcons t lt
+  | LOld le => list_exp_hterm le hod hod
+  end.
+
+Lemma exp_hterm_correct_x ge e hod od:
+   smem_model ge od hod ->
+  forall hd d,
+   smem_model ge d hd ->
+  WHEN exp_hterm e hd hod ~> t THEN forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = ST.term_eval ge (exp_term e d od) m.
+ Proof.
+   intro H.
+   induction e using exp_mut with (P0:=fun le =>  forall d hd,
+     smem_model ge d hd ->
+     WHEN list_exp_hterm le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = ST.list_term_eval ge (list_exp_term le d od) m); 
+     unfold smem_model, hsmem_post_eval in * |- * ; simpl; wlp_simplify.
+  - rewrite H1, <- H4; auto.
+  - rewrite H4, <- H0; simpl; auto.
+  - rewrite H5, <- H0, <- H4; simpl; auto.
+Qed.
+Global Opaque exp_hterm.
+
+Lemma exp_hterm_correct e hd hod:
+  WHEN exp_hterm e hd hod ~> t THEN forall ge od d m, smem_model ge od hod -> smem_model ge d hd -> smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = ST.term_eval ge (exp_term e d od) m.
+Proof.
+  unfold wlp; intros; eapply exp_hterm_correct_x; eauto.
+Qed.
+Hint Resolve exp_hterm_correct: wlp.
+
+Fixpoint hinst_smem (i: inst) (hd hod: hsmem): ?? hsmem :=
+  match i with
+  | nil => RET hd
+  | (x, e)::i' =>
+     DO ht <~ exp_hterm e hd hod;;
+     DO nd <~ hsmem_set hd x ht;;
+     hinst_smem i' nd hod
+  end.
+
+Lemma hinst_smem_correct i: forall hd hod,
+  WHEN hinst_smem i hd hod ~> hd' THEN
+    forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'.
+Proof.
+  Local Hint Resolve smem_valid_set_proof.
+  induction i; simpl; wlp_simplify; eauto 15 with wlp.
+Qed.
+Global Opaque hinst_smem.
+Local Hint Resolve hinst_smem_correct: wlp.
+
+(* logging info: we log the number of inst-instructions passed ! *)
+Variable log_new_inst: unit -> ?? unit. 
+
+Fixpoint bblock_hsmem_rec (p: bblock) (d: hsmem): ?? hsmem :=
+  match p with
+  | nil => RET d
+  | i::p' =>
+     log_new_inst tt;;
+     DO d' <~ hinst_smem i d d;;
+     bblock_hsmem_rec p' d'
+  end.
+
+Lemma bblock_hsmem_rec_correct p: forall hd,
+  WHEN bblock_hsmem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'.
+Proof.
+  induction p; simpl; wlp_simplify.
+Qed.
+Global Opaque bblock_hsmem_rec.
+Local Hint Resolve bblock_hsmem_rec_correct: wlp.
+
+Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}.
+
+Lemma hsmem_empty_correct ge: smem_model ge smem_empty hsmem_empty.
+Proof.
+  unfold smem_model, smem_valid, hsmem_post_eval; simpl; intuition try congruence.
+  rewrite !Dict.empty_spec; simpl; auto.
+Qed.
+
+Definition bblock_hsmem: bblock -> ?? hsmem
+ := fun p => bblock_hsmem_rec p hsmem_empty.
+
+Lemma bblock_hsmem_correct p:
+  WHEN bblock_hsmem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd.
+Proof.
+  Local Hint Resolve hsmem_empty_correct.
+  wlp_simplify.
+Qed.
+Global Opaque bblock_hsmem.
+
+End CanonBuilding.
+
+(* Now, we build the hash-Cons value from a "hash_eq".
+
+Informal specification: 
+  [hash_eq] must be consistent with the "hashed" constructors defined above.
+
+We expect that hashinfo values in the code of these "hashed" constructors verify:
+
+  (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)    
+
+*)
+
+Definition term_hash_eq (ta tb: term): ?? bool := 
+  match ta, tb with
+  | Input xa _, Input xb _ =>
+     if R.eq_dec xa xb  (* Inefficient in some cases ? *)
+     then RET true
+     else RET false
+  | App oa lta _, App ob ltb _ => 
+     DO b <~ op_eq oa ob ;;
+     if b then phys_eq lta ltb
+     else RET false
+  | _,_ => RET false
+  end.
+
+Lemma term_hash_eq_correct: forall ta tb, WHEN term_hash_eq ta tb ~> b THEN b=true -> term_set_hid ta unknown_hid=term_set_hid tb unknown_hid.
+Proof.
+  Local Hint Resolve op_eq_correct: wlp.
+  destruct ta, tb; wlp_simplify; (discriminate || (subst; auto)).
+Qed.
+Global Opaque term_hash_eq.
+Hint Resolve term_hash_eq_correct: wlp.
+
+Definition list_term_hash_eq (lta ltb: list_term): ?? bool := 
+  match lta, ltb with
+  | LTnil _, LTnil _ => RET true
+  | LTcons ta lta _, LTcons tb ltb _ => 
+      DO b <~ phys_eq ta tb ;;
+     if b then phys_eq lta ltb
+     else RET false
+  | _,_ => RET false
+  end.
+
+Lemma list_term_hash_eq_correct: forall lta ltb, WHEN list_term_hash_eq lta ltb ~> b THEN b=true -> list_term_set_hid lta unknown_hid=list_term_set_hid ltb unknown_hid.
+Proof.
+  destruct lta, ltb; wlp_simplify; (discriminate || (subst; auto)).
+Qed.
+Global Opaque list_term_hash_eq.
+Hint Resolve list_term_hash_eq_correct: wlp.
+
+Lemma hsmem_post_eval_intro (d1 d2: hsmem):
+  (forall x, Dict.get d1 x = Dict.get d2 x) -> (forall ge x m, hsmem_post_eval ge d1 x m = hsmem_post_eval ge d2 x m).
+Proof.
+  unfold hsmem_post_eval; intros H ge x m; rewrite H. destruct (Dict.get d2 x); auto.
+Qed.
+
+Local Hint Resolve bblock_hsmem_correct Dict.eq_test_correct: wlp.
+
+Program Definition mk_hash_params (log: term -> ?? unit): Dict.hash_params term :=
+ {|
+    Dict.test_eq := phys_eq;
+    Dict.hashing := fun (ht: term) => RET (term_get_hid ht);
+    Dict.log := log |}.
+Obligation 1.
+  eauto with wlp.
+Qed.
+
+(*** A GENERIC EQ_TEST: IN ORDER TO SUPPORT SEVERAL DEBUGGING MODE !!! ***)
+Definition no_log_assign (x:R.t) (t:term): ?? unit := RET tt.
+Definition no_log_new_term (t:term): ?? unit := RET tt.
+
+Section Prog_Eq_Gen.
+
+Variable log_assign: R.t -> term -> ?? unit.
+Variable log_new_term: hashConsing term -> hashConsing list_term -> ??(term -> ?? unit).
+Variable log_inst1: unit -> ?? unit. (* log of p1 insts *)
+Variable log_inst2: unit -> ?? unit. (* log of p2 insts *)
+
+Variable hco_term: hashConsing term.
+Hypothesis hco_term_correct: forall t, WHEN hco_term.(hC) t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.
+
+Variable hco_list: hashConsing list_term.
+Hypothesis hco_list_correct: forall t, WHEN hco_list.(hC) t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m.
+
+Variable print_error_end: hsmem -> hsmem -> ?? unit.
+Variable print_error: pstring -> ?? unit.
+
+Variable check_failpreserv: bool.
+Variable dbg_failpreserv: term -> ?? 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 <~ bblock_hsmem hco_term.(hC) hco_list.(hC) log_assign no_log_new_term log_inst1 p1;;
+    DO log_new_term <~ log_new_term hco_term hco_list;;
+    DO d2 <~ bblock_hsmem hco_term.(hC) hco_list.(hC) no_log_assign log_new_term log_inst2 p2;;
+    DO b <~ Dict.eq_test d1 d2 ;;
+    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, _ =>
+    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.
+  constructor 1; wlp_simplify; try congruence.
+  destruct (H ge) as (EQPRE1&EQPOST1); destruct (H0 ge) as (EQPRE2&EQPOST2); clear H H0.
+  apply bblock_smem_simu; auto. split.
+  + intros m; rewrite <- EQPRE1, <- EQPRE2.
+    rewrite ! allvalid_extensionality.
+    unfold incl in * |- *; intuition eauto.
+  + intros m0 x VALID; rewrite <- EQPOST1, <- EQPOST2; auto.
+    erewrite hsmem_post_eval_intro; eauto.
+    erewrite <- EQPRE2; auto.
+    erewrite <- EQPRE1 in VALID.
+    rewrite ! allvalid_extensionality in * |- *.
+    unfold incl in * |- *; intuition eauto.
+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 exta0; simpl in * |- *; auto.
+Qed.
+Global Opaque g_bblock_simu_test.
+
+End Prog_Eq_Gen.
+
+
+
+Definition hpt: hashP term := {| hash_eq := term_hash_eq; get_hid:=term_get_hid; set_hid:=term_set_hid |}. 
+Definition hplt: hashP list_term := {| hash_eq := list_term_hash_eq; get_hid:=list_term_get_hid; set_hid:=list_term_set_hid |}.
+
+Definition recover_hcodes (t:term): ??(hashinfo term) :=
+  match t with
+  | Input x _ => 
+    DO hv <~ hInput_hcodes x ;;
+    RET {| hdata := t; hcodes := hv |}
+  | App o l _ => 
+    DO hv <~ hApp_hcodes o l ;;
+    RET {| hdata := t; hcodes := hv |}
+  end.
+
+
+Definition msg_end_of_bblock: pstring :="--- unknown subterms in the graph".
+
+Definition log_new_term
+    (unknownHash_msg: term -> ?? pstring)
+    (hct:hashConsing term) 
+    (hcl:hashConsing list_term) 
+    : ?? (term -> ?? unit) :=
+  DO clock <~ hct.(next_hid)();;
+  hct.(next_log) msg_end_of_bblock;;
+  hcl.(next_log) msg_end_of_bblock;;
+  RET (fun t =>
+       DO ok <~ hash_older (term_get_hid t) clock;;
+       if ok 
+       then
+          RET tt
+       else 
+          DO ht <~ recover_hcodes t;;
+          hct.(remove) ht;;
+          DO msg <~ unknownHash_msg t;;
+          FAILWITH msg).
+
+Definition skip (_:unit): ?? unit := RET tt.
+
+Definition msg_prefix: pstring := "*** ERROR INFO from bblock_simu_test: ".
+Definition msg_error_on_end: pstring := "mismatch in final assignments !".
+Definition msg_unknow_term: pstring := "unknown term".
+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 (INTERNAL ERROR: this error is expected to be detected before!!!)".
+
+Definition print_error_end (_ _: hsmem): ?? unit
+ := println (msg_prefix +; msg_error_on_end).
+
+Definition print_error (log: logger unit) (s:pstring): ?? unit
+ := DO n <~ log_info log ();;
+    println (msg_prefix +; msg_number +; n +; " -- " +; s). 
+
+Definition failpreserv_error (_: term): ?? unit
+  := println (msg_prefix +; msg_notfailpreserv).
+
+Lemma term_eval_set_hid_equiv ge t1 t2 hid1 hid2 m:
+  term_set_hid t1 hid1 = term_set_hid t2 hid2 -> term_eval ge t1 m = term_eval ge t2 m.
+Proof.
+  intro H; erewrite <- term_eval_set_hid; rewrite H. apply term_eval_set_hid.
+Qed.
+
+Lemma list_term_eval_set_hid_equiv ge t1 t2 hid1 hid2 m:
+  list_term_set_hid t1 hid1 = list_term_set_hid t2 hid2 -> list_term_eval ge t1 m = list_term_eval ge t2 m.
+Proof.
+  intro H; erewrite <- list_term_eval_set_hid; rewrite H. apply list_term_eval_set_hid.
+Qed.
+
+Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv.
+
+Program Definition bblock_simu_test (p1 p2: bblock): ?? bool :=
+  DO log <~ count_logger ();;
+  DO hco_term <~ mk_annot (hCons hpt);;
+  DO hco_list <~ mk_annot (hCons hplt);;
+  g_bblock_simu_test
+    no_log_assign
+    (log_new_term (fun _ => RET msg_unknow_term))
+    skip
+    (log_insert log)
+    hco_term _
+    hco_list _
+    print_error_end
+    (print_error log)
+    true (* check_failpreserv *)
+    failpreserv_error
+    p1 p2.
+Obligation 1.
+  generalize (hCons_correct _ _ _ H0); clear H0.
+  wlp_simplify.
+Qed.
+Obligation 2.
+  generalize (hCons_correct _ _ _ H); clear H.
+  wlp_simplify.
+Qed.
+
+Local Hint Resolve g_bblock_simu_test_correct.
+
+Theorem bblock_simu_test_correct p1 p2:
+  WHEN bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque bblock_simu_test.
+
+(** This is only to print info on each bblock_simu_test run **)
+Section Verbose_version.
+
+Variable string_of_name: R.t -> ?? pstring.
+Variable string_of_op: op -> ?? pstring.
+
+
+Local Open Scope string_scope.
+
+Definition string_term_hid (t: term): ?? pstring := 
+  DO id <~ string_of_hashcode (term_get_hid t);;
+  RET ("E" +; (CamlStr id)).
+
+Definition string_list_hid (lt: list_term): ?? pstring := 
+  DO id <~ string_of_hashcode (list_term_get_hid lt);;
+  RET ("L" +; (CamlStr id)).
+
+Definition print_raw_term (t: term): ?? unit :=
+  match t with
+  | Input x _ => 
+    DO s <~ string_of_name x;;
+    println( "init_access " +; s)
+  | App o (LTnil _) _ => 
+    DO so <~ string_of_op o;;
+    println so
+  | App o l _ =>
+    DO so <~ string_of_op o;;
+    DO sl <~ string_list_hid l;;
+    println (so +; " " +; sl)
+  end.
+
+(*
+Definition print_raw_list(lt: list_term): ?? unit :=
+  match lt with
+  | LTnil _=> println ""
+  | LTcons t l _ =>
+    DO st <~ string_term_hid t;;
+    DO sl <~ string_list_hid l;;
+    println(st +; " " +; sl)
+  end.
+*)
+
+Section PrettryPrint.
+
+Variable get_debug_info: term -> ?? option pstring. 
+
+Fixpoint string_of_term (t: term): ?? pstring :=
+  match t with
+  | Input x _ => string_of_name x
+  | App o (LTnil _) _ => string_of_op o
+  | App o l _ => 
+      DO so <~ string_of_op o;;
+      DO sl <~ string_of_list_term l;;
+      RET (so +; "[" +; sl +; "]")
+  end
+with string_of_list_term (l: list_term): ?? pstring :=
+  match l with
+  | LTnil _ => RET (Str "")
+  | LTcons t (LTnil _) _  => 
+    DO dbg <~ get_debug_info t;;
+    match dbg with
+    | Some x => RET x
+    | None => string_of_term t
+    end
+  | LTcons t l' _ => 
+     DO st <~ (DO dbg <~ get_debug_info t;;
+               match dbg with
+               | Some x => RET x
+               | None => string_of_term t
+               end);;
+     DO sl <~ string_of_list_term l';;
+     RET (st +; ";" +; sl)
+  end.
+
+
+End PrettryPrint.
+
+
+Definition pretty_term gdi t :=
+  DO r <~ string_of_term gdi t;;
+  println(r).
+
+Fixpoint print_head (head: list pstring): ?? unit :=
+  match head with
+  | i::head' => println (i);; print_head head'
+  | _ => RET tt
+  end.
+
+Definition print_term gdi (head: list pstring) (t: term): ?? unit :=
+  print_head head;;
+  DO s <~ string_term_hid t;;
+  print (s +; ": ");;
+  print_raw_term t;;
+  DO dbg <~ gdi t;;
+  match dbg with
+  | Some x => 
+     print("//  " +; x +; " <- ");;
+     pretty_term gdi t
+  | None => RET tt
+  end.
+
+Definition print_list gdi (head: list pstring) (lt: list_term): ?? unit :=
+  print_head head;;
+  DO s <~ string_list_hid lt ;;
+  print (s +; ": ");;
+  (* print_raw_list lt;; *)
+  DO ps <~ string_of_list_term gdi lt;;
+  println("[" +; ps +; "]").
+
+
+Definition print_tables gdi ext exl: ?? unit :=
+  println "-- term table --" ;;
+  iterall ext (fun head _ pt => print_term gdi head pt.(hdata));;
+  println "-- list table --" ;;
+  iterall exl (fun head _ pl => print_list gdi head pl.(hdata));;
+  println "----------------".
+
+Definition print_final_debug gdi (d1 d2: hsmem): ?? unit 
+ := DO b <~ Dict.not_eq_witness d1 d2 ;;
+    match b with
+    | Some x =>
+      DO s <~ string_of_name x;;
+      println("mismatch on: " +; s);;
+      match Dict.get d1 x with 
+      | None => println("=> unassigned in 1st bblock")
+      | Some t1 =>
+         print("=> node expected from 1st bblock: ");;
+         pretty_term gdi t1
+      end;;
+      match Dict.get d2 x with 
+      | None => println("=> unassigned in 2nd bblock")
+      | Some t2 =>
+         print("=> node found from 2nd bblock: ");;
+         pretty_term gdi t2
+      end
+    | None => FAILWITH "bug in Dict.not_eq_witness ?"
+    end.
+
+Definition witness:= option term.
+
+Definition msg_term (cr: cref witness) t :=
+  set cr (Some t);;
+  RET msg_unknow_term.
+
+Definition print_witness gdi cr (*msg*) :=
+  DO wit <~ get cr ();;
+  match wit with
+  | Some t =>
+     println("=> unknown term node: ");;
+     pretty_term gdi t (*;;
+     println("=> encoded on " +; msg +; " graph as: ");;
+     print_raw_term t *)
+  | None => println "Unexpected failure: no witness info (hint: hash-consing bug ?)"
+  end.
+
+
+Definition print_error_end1 gdi hct hcl (d1 d2:hsmem): ?? unit
+ := println "- GRAPH of 1st bblock";;
+    DO ext <~ export hct ();;
+    DO exl <~ export hcl ();;
+    print_tables gdi ext exl;;
+    print_error_end d1 d2;;
+    print_final_debug gdi d1 d2.
+
+Definition print_error1 gdi hct hcl cr log s : ?? unit
+ := println "- GRAPH of 1st bblock";;
+    DO ext <~ export hct ();;
+    DO exl <~ export hcl ();;
+    print_tables gdi ext exl;;
+    print_error log s;;
+    print_witness gdi cr (*"1st"*).
+
+
+Definition xmsg_number: pstring := "on 1st bblock -- on inst num ".
+
+Definition print_error_end2 gdi hct hcl (d1 d2:hsmem): ?? unit
+ := println (msg_prefix +; msg_error_on_end);;
+    println "- GRAPH of 2nd bblock";;
+    DO ext <~ export hct ();;
+    DO exl <~ export hcl ();;
+    print_tables gdi ext exl.
+
+Definition print_error2 gdi hct hcl cr (log: logger unit) (s:pstring): ?? unit
+ := DO n <~ log_info log ();;
+    DO ext <~ export hct ();;
+    DO exl <~ export hcl ();;
+    println (msg_prefix +; xmsg_number +; n +; " -- " +; s);;
+    print_witness gdi cr (*"2nd"*);;
+    println "- GRAPH of 2nd bblock";;
+    print_tables gdi ext exl.
+
+(* USELESS
+Definition simple_log_assign (d: D.t term pstring) (x: R.t) (t: term): ?? unit :=
+  DO s <~ string_of_name x;;
+  d.(D.set) (t,s).
+*)
+
+Definition log_assign (d: D.t term pstring) (log: logger unit) (x: R.t) (t: term): ?? unit :=
+  DO i <~ log_info log ();;
+  DO sx <~ string_of_name x;;
+  d.(D.set) (t,(sx +; "@" +; i)).
+
+Definition msg_new_inst : pstring := "--- inst ".
+
+Definition hlog (log: logger unit) (hct: hashConsing term) (hcl: hashConsing list_term): unit -> ?? unit :=
+   (fun _ =>
+      log_insert log tt ;;
+      DO s <~ log_info log tt;;
+      let s:= msg_new_inst +; s in
+      next_log hct s;;
+      next_log hcl s
+    ).
+
+Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
+  DO dict_info <~ make_dict (mk_hash_params (fun _ => RET tt));;
+  DO log1 <~ count_logger ();;
+  DO log2 <~ count_logger ();;
+  DO cr <~ make_cref None;;
+  DO hco_term <~ mk_annot (hCons hpt);;
+  DO hco_list <~ mk_annot (hCons hplt);;
+  DO result1 <~ g_bblock_simu_test
+     (log_assign dict_info log1)
+     (log_new_term (msg_term cr))
+     (hlog log1 hco_term hco_list)
+     (log_insert log2)
+     hco_term _
+     hco_list _
+     (print_error_end1 dict_info.(D.get) hco_term hco_list)
+     (print_error1 dict_info.(D.get) hco_term hco_list cr log2)
+     true
+     failpreserv_error
+     p1 p2;;
+  if result1 
+  then RET true
+  else
+    DO dict_info <~ make_dict (mk_hash_params (fun _ => RET tt));;
+    DO log1 <~ count_logger ();;
+    DO log2 <~ count_logger ();;
+    DO cr <~ make_cref None;;
+    DO hco_term <~ mk_annot (hCons hpt);;
+    DO hco_list <~ mk_annot (hCons hplt);;
+    DO result2 <~ g_bblock_simu_test
+       (log_assign dict_info log1)
+       (*fun _ _ => RET no_log_new_term*)  (* REM: too weak !! *)
+       (log_new_term (msg_term cr))        (* REM: too strong ?? *)
+       (hlog log1 hco_term hco_list)
+       (log_insert log2)
+       hco_term _
+       hco_list _
+       (print_error_end2 dict_info.(D.get) hco_term hco_list)
+       (print_error2 dict_info.(D.get) hco_term hco_list cr log2)
+       false
+       (fun _ => RET tt)
+       p2 p1;;
+    if result2 
+    then (
+      println (msg_prefix +; " OOops - symmetry violation in bblock_simu_test  => this is a bug of bblock_simu_test ??");;
+      RET false
+    ) else RET false
+   .
+Obligation 1.
+  generalize (hCons_correct _ _ _ H0); clear H0.
+  wlp_simplify.
+Qed.
+Obligation 2.
+  generalize (hCons_correct _ _ _ H); clear H.
+  wlp_simplify.
+Qed.
+Obligation 3.
+  generalize (hCons_correct _ _ _ H0); clear H0.
+  wlp_simplify.
+Qed.
+Obligation 4.
+  generalize (hCons_correct _ _ _ H); clear H.
+  wlp_simplify.
+Qed.
+
+Theorem verb_bblock_simu_test_correct p1 p2:
+  WHEN verb_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque verb_bblock_simu_test.
+
+End Verbose_version.
+
+End SimuWithReduce.
+
+(* TODO: why inlining fails here ? *)
+Transparent hterm_lift.
+Extraction Inline lift.
+
+End ImpSimu.
+
+Require Import FMapPositive.
+
+
+Require Import PArith.
+Require Import FMapPositive.
+
+Module ImpPosDict <: ImpDict with Module R:=Pos.
+
+Module R:=Pos.
+
+Definition t:=PositiveMap.t.
+
+Definition get {A} (d:t A) (x:R.t): option A 
+ := PositiveMap.find x d.
+
+Definition set {A} (d:t A) (x:R.t) (v:A): t A
+ := PositiveMap.add x v d.
+
+Local Hint Unfold PositiveMap.E.eq.
+
+Lemma set_spec_eq A d x (v: A):
+  get (set d x v) x = Some v.
+Proof.
+  unfold get, set; apply PositiveMap.add_1; auto.
+Qed.
+
+Lemma set_spec_diff A d x y (v: A):
+  x <> y -> get (set d x v) y = get d y.
+Proof.
+  unfold get, set; intros; apply PositiveMap.gso; auto.
+Qed.
+
+Definition rem {A} (d:t A) (x:R.t): t A
+ := PositiveMap.remove x d.
+
+Lemma rem_spec_eq A (d: t A) x:
+  get (rem d x) x = None.
+Proof.
+  unfold get, rem; apply PositiveMap.grs; auto.
+Qed.
+
+Lemma rem_spec_diff A (d: t A) x y:
+  x <> y -> get (rem d x) y = get d y.
+Proof.
+  unfold get, rem; intros; apply PositiveMap.gro; auto.
+Qed.
+
+
+Definition empty {A}: t A := PositiveMap.empty A.
+
+Lemma empty_spec A x:
+  get (empty (A:=A)) x = None.
+Proof.
+  unfold get, empty; apply PositiveMap.gempty; auto.
+Qed.
+
+Import PositiveMap.
+
+Fixpoint eq_test {A} (d1 d2: t A): ?? bool :=
+  match d1, d2 with
+  | Leaf _, Leaf _ => RET true
+  | Node l1 (Some x1) r1, Node l2 (Some x2) r2 =>
+      DO b0 <~ phys_eq x1 x2 ;;
+      if b0 then
+        DO b1 <~ eq_test l1 l2 ;;
+        if b1 then
+          eq_test r1 r2
+        else
+           RET false
+      else
+         RET false
+  | Node l1 None r1, Node l2 None r2 =>
+      DO b1 <~ eq_test l1 l2 ;;
+      if b1 then
+        eq_test r1 r2
+      else
+        RET false
+  | _, _ => RET false
+  end.
+
+Lemma eq_test_correct A d1: forall (d2: t A),
+ WHEN eq_test d1 d2 ~> b THEN
+  b=true -> forall x, get d1 x = get d2 x.
+Proof.
+  unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; simpl; 
+  wlp_simplify; (discriminate || (subst; destruct x; simpl; auto)).
+Qed.
+Global Opaque eq_test.
+
+(* 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"
+  | Node _ (Some _) _ => RET xH
+  | Node (Leaf _) None r => 
+    DO p <~ pick r;;
+    RET (xI p)
+  | Node l None _ =>
+    DO p <~ pick l;;
+    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
+  | Node l1 (Some x1) r1, Node l2 (Some x2) r2 =>
+      DO b0 <~ phys_eq x1 x2 ;;
+      if b0 then
+        DO b1 <~ not_eq_witness l1 l2;;
+        match b1 with
+        | None => 
+          DO b2 <~ not_eq_witness r1 r2;;
+          match b2 with
+          | None => RET None
+          | Some p => RET (Some (xI p))
+          end
+        | Some p => RET (Some (xO p))
+        end
+      else
+         RET (Some xH)
+  | Node l1 None r1, Node l2 None r2 =>
+        DO b1 <~ not_eq_witness l1 l2;;
+        match b1 with
+        | None => 
+          DO b2 <~ not_eq_witness r1 r2;;
+          match b2 with
+          | None => RET None
+          | Some p => RET (Some (xI p))
+          end
+        | Some p => RET (Some (xO p))
+        end
+  | l, Leaf _ => DO p <~ pick l;; RET (Some p)
+  | Leaf _, r => DO p <~ pick r;; RET (Some p)
+  | _, _ => RET (Some xH)
+  end.
+
+End ImpPosDict.
+
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v
index 7925f62d..f1abaf7a 100644
--- a/mppa_k1c/abstractbb/Impure/ImpCore.v
+++ b/mppa_k1c/abstractbb/Impure/ImpCore.v
@@ -193,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 dd615628..d8002375 100644
--- a/mppa_k1c/abstractbb/Impure/ImpHCons.v
+++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v
@@ -99,41 +99,101 @@ Hint Resolve assert_list_incl_correct.
 
 End Sets.
 
+
+
+
 (********************************)
 (* (Weak) HConsing              *)
 
+Module HConsing.
 
-Axiom xhCons: forall {A}, ((A -> A -> ?? bool) * (pre_hashV A -> ?? hashV A)) -> ?? hashConsing A.
+Export HConsingDefs.
+
+(* NB: this axiom is NOT intended to be called directly, but only through [hCons...] functions below. *)
+Axiom xhCons: forall {A}, (hashP A) -> ?? hashConsing A.
 Extract Constant xhCons => "ImpHConsOracles.xhCons".
 
-Definition hCons_eq_msg: pstring := "xhCons: hash_eq differs".
+Definition hCons_eq_msg: pstring := "xhCons: hash eq differs".
 
-Definition hCons {A} (hash_eq: A -> A -> ?? bool) (unknownHash_msg: pre_hashV A -> ?? pstring): ?? (hashConsing A) :=
-  DO hco <~ xhCons (hash_eq, fun v => DO s <~ unknownHash_msg v ;; FAILWITH s) ;;
+Definition hCons {A} (hp: hashP A): ?? (hashConsing A) :=
+  DO hco <~ xhCons hp ;;
   RET {|
-      hC := fun x => 
-       DO x' <~ hC hco x ;;
-       DO b0 <~ hash_eq (pre_data x) (data x') ;;
-       assert_b b0 hCons_eq_msg;;
-       RET x';
-      hC_known := fun x => 
-       DO x' <~ hC_known hco x ;;
-       DO b0 <~ hash_eq (pre_data x) (data x') ;;
-       assert_b b0 hCons_eq_msg;;
-       RET x';
-      next_log := next_log hco;
-      export := export hco;
+      hC := (fun x =>
+         DO x' <~ hC hco x ;;
+         DO b0 <~ hash_eq hp x.(hdata) x' ;;
+         assert_b b0 hCons_eq_msg;;
+         RET x');
+      next_hid := hco.(next_hid);
+      next_log := hco.(next_log);
+      export := hco.(export);
+      remove := hco.(remove)
       |}.
 
-Lemma hCons_correct: forall A (hash_eq: A -> A -> ?? bool) msg,
-  WHEN hCons hash_eq msg ~> hco THEN
-    ((forall x y, WHEN hash_eq x y ~> b THEN b=true -> x=y) -> forall x, WHEN hC hco x ~> x' THEN (pre_data x)=(data x'))
- /\ ((forall x y, WHEN hash_eq x y ~> b THEN b=true -> x=y) -> forall x, WHEN hC_known hco x ~> x' THEN (pre_data x)=(data x')).
+
+Lemma hCons_correct A (hp: hashP A):
+  WHEN hCons hp ~> hco THEN
+    (forall x y, WHEN hp.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hp x)=(ignore_hid hp y)) ->
+    forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hp x.(hdata)=ignore_hid hp x'.
 Proof.
   wlp_simplify.
 Qed.
 Global Opaque hCons.
 Hint Resolve hCons_correct: wlp.
 
-Definition hCons_spec {A} (hco: hashConsing A) :=
-  (forall x, WHEN hC hco x ~> x' THEN (pre_data x)=(data x')) /\ (forall x, WHEN hC_known hco x ~> x' THEN (pre_data x)=(data x')).
+
+
+(* hashV: extending a given type with hash-consing *)
+Record hashV {A:Type}:= {
+  data: A;
+  hid: hashcode
+}.
+Arguments hashV: clear implicits.
+
+Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashP (hashV A) := {|
+  hash_eq := fun v1 v2 => test_eq v1.(data) v2.(data);
+  get_hid := hid;
+  set_hid := fun v id => {| data := v.(data); hid := id |}
+|}.
+
+Definition liftHV (x:nat) := {| data := x; hid := unknown_hid |}.
+
+Definition hConsV {A} (hasheq: A -> A -> ?? bool): ?? (hashConsing (hashV A)) :=
+  hCons (hashV_C hasheq).
+
+Lemma hConsV_correct A (hasheq: A -> A -> ?? bool):
+  WHEN hConsV hasheq ~> hco THEN
+    (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> 
+    forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data).
+Proof.
+  Local Hint Resolve f_equal2.
+  wlp_simplify.
+  exploit H; eauto.
+  + wlp_simplify.
+  + intros; congruence.
+Qed.
+Global Opaque hConsV.
+Hint Resolve hConsV_correct: wlp.
+
+Definition hC_known {A} (hco:hashConsing (hashV A)) (unknownHash_msg: hashinfo (hashV A) -> ?? pstring) (x:hashinfo (hashV A)): ?? hashV A :=
+  DO clock <~ hco.(next_hid)();;
+  DO x' <~ hco.(hC) x;;
+  DO ok <~ hash_older x'.(hid) clock;;
+  if ok 
+  then RET x'
+  else
+    hco.(remove) x;; 
+    DO msg <~ unknownHash_msg x;;
+    FAILWITH msg.
+
+Lemma hC_known_correct A (hco:hashConsing (hashV A)) msg x:
+  WHEN hC_known hco msg x ~> x' THEN
+    (forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data)) ->
+    x.(hdata).(data)=x'.(data).
+Proof.
+  wlp_simplify.
+  unfold wlp in * |- ; eauto.
+Qed.
+Global Opaque hC_known.
+Hint Resolve hC_known_correct: wlp.
+
+End HConsing.
diff --git a/mppa_k1c/abstractbb/Impure/ImpLoops.v b/mppa_k1c/abstractbb/Impure/ImpLoops.v
index dc8b2627..33376c19 100644
--- a/mppa_k1c/abstractbb/Impure/ImpLoops.v
+++ b/mppa_k1c/abstractbb/Impure/ImpLoops.v
@@ -17,7 +17,7 @@ Section While_Loop.
 (** Local Definition of "while-loop-invariant" *)
 Let wli {S} cond body (I: S -> Prop) := forall s, I s -> cond s = true -> WHEN (body s) ~> s' THEN I s'.
 
-Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | I s0 -> I s /\ cond s = false}
+Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | (I s0 -> I s) /\ cond s = false}
   := loop (A:={s | I s0 -> I s})
        (s0, 
           fun s =>
@@ -26,7 +26,7 @@ Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {
              DO s' <~ mk_annot (body s) ;; 
              RET (inl (A:={s | I s0 -> I s }) s')
           | false => 
-             RET (inr (B:={s | I s0 -> I s /\ cond s = false}) s)
+             RET (inr (B:={s | (I s0 -> I s) /\ cond s = false}) s)
           end).
 Obligation 2.
   unfold wli, wlp in * |-; eauto.
@@ -83,7 +83,7 @@ Definition wapply {A B} {R: A -> B -> Prop} (beq: A -> A -> ?? bool) (k: A -> ??
   assert_b b msg;;
   RET (output a).
 
-Lemma wapply_correct A B (R: A -> B -> Prop) (beq: A -> A -> ?? bool)x (k: A -> ?? answ R):
+Lemma wapply_correct A B (R: A -> B -> Prop) (beq: A -> A -> ?? bool) (k: A -> ?? answ R) x:
  beq_correct beq
  -> WHEN wapply beq k x ~> y THEN R x y.
 Proof.
@@ -107,7 +107,7 @@ Definition rec_preserv {A B} (recF: (A -> ?? B) -> A -> ?? B) (R: A -> B -> Prop
 Program Definition rec {A B} beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq): ?? (A -> ?? B) :=
   DO f <~ xrec (B:=answ R) (fun f x =>
          DO y <~ mk_annot (recF (wapply beq f) x) ;;
-         RET {| input := x; output := proj1_sig y |});;
+         RET {| input := x; output := `y |});;
   RET (wapply beq f).
 Obligation 1.
   eapply H1; eauto. clear H H1.
diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v
index 1a84eb3b..de4c7973 100644
--- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v
+++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v
@@ -91,11 +91,17 @@ Extract Inlined Constant struct_eq => "(=)".
 Hint Resolve struct_eq_correct: wlp.
 
 
-(** Data-structure for generic hash-consing, hash-set *)
+(** Data-structure for generic hash-consing *)
 
 Axiom hashcode: Type.
 Extract Constant hashcode => "int".
 
+(* 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 => "(<)".
+
 Module Dict.
 
 Record hash_params {A:Type} := {
@@ -115,42 +121,45 @@ Arguments t: clear implicits.
 
 End Dict.
 
+Module HConsingDefs.
 
-(* 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;
+Record hashinfo {A: Type} := {
+  hdata: A;
   hcodes: list hashcode;
-  debug_info: option pstring;
 }.
-Arguments pre_hashV: clear implicits.
+Arguments hashinfo: clear implicits.
 
-Record hashV {A:Type}:= {
-  data: A;
-  hid: hashcode
+(* for inductive types with intrinsic hash-consing *)
+Record hashP {A:Type}:= {
+  hash_eq: A -> A -> ?? bool;
+  get_hid: A -> hashcode;
+  set_hid: A -> hashcode -> A; (* WARNING: should only be used by hash-consing machinery *)
 }.
-Arguments hashV: clear implicits.
+Arguments hashP: clear implicits.
+
+Axiom unknown_hid: hashcode.
+Extract Constant unknown_hid => "-1".
+
+Definition ignore_hid {A} (hp: hashP A) (hv:A) := set_hid hp hv unknown_hid.
 
 Record hashExport {A:Type}:= {
-  get_hashV: hashcode -> ?? pre_hashV A;
-  iterall: ((list pstring) -> hashcode -> pre_hashV A -> ?? unit) -> ?? unit; (* iter on all elements in the hashtbl, by order of creation *)
+  get_info: hashcode -> ?? hashinfo A;
+  iterall: ((list pstring) -> hashcode -> hashinfo A -> ?? unit) -> ?? unit; (* iter on all elements in the hashtbl, by order of creation *)
 }.
 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 ****)
+  hC: hashinfo A -> ?? A;
+  (**** below: debugging or internal functions ****)
+  next_hid: unit -> ?? hashcode; (* should be strictly less old than ignore_hid *)
+  remove: hashinfo A -> ??unit; (* SHOULD NOT BE USED ! *)
   next_log: pstring -> ?? unit; (* insert a log info (for the next introduced element) -- regiven by [iterall export] below *)
   export: unit -> ?? hashExport A ; 
 }.
 Arguments hashConsing: clear implicits.
 
+End HConsingDefs.
+
 (** recMode: this is mainly for Tests ! *)
 Inductive recMode:= StdRec | MemoRec | BareRec | BuggyRec.
 
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
index b7a80679..2b66899b 100644
--- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
@@ -1,6 +1,5 @@
 open ImpPrelude
-
-exception Stop;;
+open HConsingDefs
 
 let make_dict (type key) (p: key Dict.hash_params) =
   let module MyHashedType = struct
@@ -16,10 +15,15 @@ let make_dict (type key) (p: key Dict.hash_params) =
   }
 
 
-let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV)) =
+exception Stop;;
+
+let xhCons (type a) (hp:a hashP) =
+  (* We use a hash-table, but a hash-set would be sufficient !                    *)
+  (* Thus, we could use a weak hash-set, but prefer avoid it for easier debugging *)
+  (* Ideally, a parameter would allow to select between the weak or full version  *)
   let module MyHashedType = struct
-    type t = a pre_hashV
-    let equal x y = hash_eq x.pre_data y.pre_data
+    type t = a hashinfo
+    let equal x y = hp.hash_eq x.hdata y.hdata
     let hash x = Hashtbl.hash x.hcodes 
   end in
   let module MyHashtbl = Hashtbl.Make(MyHashedType) in
@@ -34,21 +38,18 @@ let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV))
   let t = MyHashtbl.create 1000 in
   let logs = ref [] in
   {
-   hC = (fun (x:a pre_hashV) ->
-     match MyHashtbl.find_opt t x with
-     | Some x' -> x'
+   hC = (fun (k:a hashinfo) ->
+     match MyHashtbl.find_opt t k with
+     | Some d -> d
      | None -> (*print_string "+";*)
-        let x' = { data = x.pre_data ;
-                   hid = MyHashtbl.length t }
-        in MyHashtbl.add t x x'; x');
-   hC_known = (fun (x:a pre_hashV) ->
-     match MyHashtbl.find_opt t x with
-     | Some x' -> x'
-     | None -> error x);
+        let d = hp.set_hid k.hdata (MyHashtbl.length t) in
+        MyHashtbl.add t {k with hdata = d } d; d);
    next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs));
+   next_hid = (fun () -> MyHashtbl.length t);
+   remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x);
    export = fun () ->
      match pick t with
-     | None -> { get_hashV = (fun _ -> raise Not_found);  iterall = (fun _ -> ()) } 
+     | None -> { get_info = (fun _ -> raise Not_found);  iterall = (fun _ -> ()) } 
      | Some (k,_) ->
         (* the state is fully copied at export ! *)
         let logs = ref (List.rev_append (!logs) []) in
@@ -57,9 +58,9 @@ let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV))
           | (j, info)::l' when i>=j -> logs:=l'; info::(step_log i)
           | _ -> []
         in let a = Array.make (MyHashtbl.length t) k in
-           MyHashtbl.iter (fun k d -> a.(d.hid) <- k) t;
+           MyHashtbl.iter (fun k d -> a.(hp.get_hid d) <- k) t;
            {
-             get_hashV = (fun i -> a.(i));
+             get_info = (fun i -> a.(i));
              iterall = (fun iter_node -> Array.iteri (fun i k -> iter_node (step_log i) i k) a)
            }    
   }
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
index a74c721a..5075d176 100644
--- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
@@ -1,4 +1,5 @@
 open ImpPrelude
+open HConsingDefs
 
-val make_dict : 'a1 Dict.hash_params -> ('a1, 'a2) Dict.t
-val xhCons: (('a -> 'a -> bool) * ('a pre_hashV -> 'a hashV)) -> 'a hashConsing
+val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t
+val xhCons: 'a hashP -> 'a hashConsing
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v
index d1971e57..22809095 100644
--- a/mppa_k1c/abstractbb/Parallelizability.v
+++ b/mppa_k1c/abstractbb/Parallelizability.v
@@ -1,4 +1,4 @@
-(** Parallel Semantics of Abstract Basic Blocks and parallelizability test.s
+(** Parallel Semantics of Abstract Basic Blocks and parallelizability test.
 *)
 
 Require Setoid. (* in order to rewrite <-> *)
@@ -32,7 +32,7 @@ Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem :=
      end
   end.
 
-(* [inst_prun] is generalization of [inst_run] *)   
+(* [inst_prun] is generalization of [inst_run] *)
 Lemma inst_run_prun i: forall m old,
   inst_run ge i m old = inst_prun i m m old.
 Proof.
diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v
new file mode 100644
index 00000000..649dd083
--- /dev/null
+++ b/mppa_k1c/abstractbb/SeqSimuTheory.v
@@ -0,0 +1,387 @@
+(** A theory for checking/proving simulation by symbolic execution.
+
+*)
+
+
+Require Coq.Logic.FunctionalExtensionality. (* not really necessary -- see lemma at the end *)
+Require Setoid. (* in order to rewrite <-> *)
+Require Export AbstractBasicBlocksDef.
+Require Import List.
+Require Import ImpPrelude.
+Import HConsingDefs.
+
+
+Module SimuTheory (L: SeqLanguage).
+
+Export L.
+Export LP.
+
+Inductive term :=
+  | Input (x:R.t)
+  | App (o: op) (l: list_term)
+with list_term :=
+  | LTnil
+  | LTcons (t:term) (l:list_term)
+  .
+
+Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value :=
+  match t with
+  | Input x => Some (m x)
+  | App o l =>
+     match list_term_eval ge l m with
+     | Some v => op_eval ge o v
+     | _ => None
+     end
+  end
+with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) :=
+  match l with
+  | LTnil => Some nil
+  | LTcons t l' => 
+    match term_eval ge t m, list_term_eval ge l' m with
+    | Some v, Some lv => Some (v::lv)
+    | _, _ => None
+    end
+  end.
+
+(* the symbolic memory:
+  - pre: pre-condition expressing that the computation has not yet abort on a None.
+  - post: the post-condition for each pseudo-register 
+*)
+Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}.
+
+(** initial symbolic memory *)
+Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}.
+
+Fixpoint exp_term (e: exp) (d old: smem) : term :=
+  match e with
+  | PReg x => d x
+  | Op o le => App o (list_exp_term le d old)
+  | Old e => exp_term e old old
+  end
+with list_exp_term (le: list_exp) (d old: smem) : list_term :=
+  match le with
+  | Enil => LTnil
+  | Econs e le' => LTcons (exp_term e d old) (list_exp_term le' d old)
+  | LOld le => list_exp_term le old old
+  end.
+
+
+(** assignment of the symbolic memory *)
+Definition smem_set (d:smem) x (t:term) := 
+  {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m));
+     post:=fun y => if R.eq_dec x y then t else d y |}.
+
+Section SIMU_THEORY.
+
+Variable ge: genv.
+
+Lemma set_spec_eq d x t m:
+ term_eval ge (smem_set d x t x) m = term_eval ge t m.
+Proof.
+  unfold smem_set; simpl; case (R.eq_dec x x); try congruence.
+Qed.
+
+Lemma set_spec_diff d x y t m:
+  x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m.
+Proof.
+  unfold smem_set; simpl; case (R.eq_dec x y); try congruence.
+Qed.
+
+Fixpoint inst_smem (i: inst) (d old: smem): smem :=
+  match i with
+  | nil => d
+  | (x, e)::i' =>
+     let t:=exp_term e d old in
+     inst_smem i' (smem_set d x t) old
+  end.
+
+Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem :=
+  match p with
+  | nil => d
+  | i::p' =>
+     let d':=inst_smem i d d in
+     bblock_smem_rec p' d'
+  end.
+(*
+Local Hint Resolve smem_eval_empty.
+*)
+
+Definition bblock_smem: bblock -> smem
+ := fun p => bblock_smem_rec p smem_empty.
+
+Lemma inst_smem_pre_monotonic i old: forall d m,
+  (pre (inst_smem 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 smem_set; simpl; intuition.
+Qed.
+
+Lemma bblock_smem_pre_monotonic p: forall d m,
+  (pre (bblock_smem_rec p d) ge m) -> (pre d ge m).
+Proof.
+  induction p as [|i p' IHp']; simpl; eauto.
+  intros d a H; eapply inst_smem_pre_monotonic; eauto.
+Qed.
+
+Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic.
+
+Lemma term_eval_exp e (od:smem) m0 old:
+  (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall (d:smem) m1,
+   (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+    term_eval ge (exp_term e d od) m0 = exp_eval ge e m1 old.
+Proof.
+  intro H.
+  induction e using exp_mut with
+    (P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old);
+  simpl; auto.
+  - intros; erewrite IHe; eauto.
+  - intros. erewrite IHe, IHe0; eauto. 
+Qed.
+
+Lemma inst_smem_abort i m0 x old: forall (d:smem),
+    pre (inst_smem i d old) ge m0 ->
+    term_eval ge (d x) m0 = None ->
+    term_eval ge (inst_smem i d old x) m0 = None.
+Proof.
+  induction i as [|[y e] i IHi]; simpl; auto.
+  intros d VALID H; erewrite IHi; eauto. clear IHi.
+  unfold smem_set; simpl; destruct (R.eq_dec y x); auto.
+  subst;
+  generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID.
+  unfold smem_set; simpl. intuition congruence.
+Qed.
+
+Lemma block_smem_rec_abort p m0 x: forall d,
+    pre (bblock_smem_rec p d) ge m0 ->
+    term_eval ge (d x) m0 = None ->
+    term_eval ge (bblock_smem_rec p d x) m0 = None.
+Proof.
+  induction p; simpl; auto.
+  intros d VALID H; erewrite IHp; eauto. clear IHp.
+  eapply inst_smem_abort; eauto.
+Qed.
+
+Lemma inst_smem_Some_correct1 i m0 old (od:smem): 
+  (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall (m1 m2: mem) (d: smem), 
+  inst_run ge i m1 old = Some m2 -> 
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+   forall x, term_eval ge (inst_smem 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.
+    destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence.
+    refine (IHi _ _ _ _ _ _); eauto.
+    clear x0; intros x0.
+    unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto.
+    subst; erewrite term_eval_exp; eauto.
+Qed.
+
+Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem), 
+ run ge p m1 = Some m2 -> 
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x).
+Proof.
+  Local Hint Resolve inst_smem_Some_correct1.
+  induction p as [ | i p]; simpl; intros m1 m2 d H.
+  - inversion_clear H; eauto.
+  - intros H0 x0.
+    destruct (inst_run ge i m1 m1) eqn: Heqov.
+    + refine (IHp _ _ _ _ _ _); eauto.
+    + inversion H. 
+Qed.
+
+Lemma bblock_smem_Some_correct1 p m0 m1:
+   run ge p m0 = Some m1
+   -> forall x, term_eval ge (bblock_smem p x) m0 = Some (m1 x).
+Proof.
+  intros; eapply bblocks_smem_rec_Some_correct1; eauto.
+Qed.
+
+Lemma inst_smem_None_correct i m0 old (od: smem):
+   (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall m1 d, pre (inst_smem i d od) ge m0 ->
+   (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  inst_run ge i m1 old = None -> exists x, term_eval ge (inst_smem i d od x) m0 = None.
+Proof.
+  intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d.
+  - discriminate.
+  - intros VALID H0.
+    destruct (exp_eval ge e m1 old) eqn: Heqov.
+    + refine (IHi _ _ _ _); eauto.
+      intros x0; unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto.
+      subst; erewrite term_eval_exp; eauto.
+    + intuition.
+      constructor 1 with (x:=x); simpl.
+      apply inst_smem_abort; auto.
+      rewrite set_spec_eq. 
+      erewrite term_eval_exp; eauto.
+Qed.
+
+Lemma inst_smem_Some_correct2 i m0 old (od: smem):
+  (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall (m1 m2: mem) d, 
+  pre (inst_smem i d od) ge m0 ->
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  (forall x, term_eval ge (inst_smem 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 VALID H0.
+  - intros H; eapply ex_intro; intuition eauto.
+    generalize (H0 x); rewrite H.
+    congruence.
+  - intros H.
+    destruct (exp_eval ge e m1 old) eqn: Heqov.
+    + refine (IHi _ _ _ _ _ _); eauto.
+      intros x0; unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto.
+      subst; erewrite term_eval_exp; eauto.
+    + generalize (H x).
+      rewrite inst_smem_abort; discriminate || auto.
+      rewrite set_spec_eq. 
+      erewrite term_eval_exp; eauto.
+Qed.
+
+Lemma bblocks_smem_rec_Some_correct2 p m0: forall (m1 m2: mem) d, 
+  pre (bblock_smem_rec p d) ge m0 ->
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  (forall x, term_eval ge (bblock_smem_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 VALID H0.
+  - intros H; eapply ex_intro; intuition eauto.
+    generalize (H0 x); rewrite H.
+    congruence.
+  - intros H.
+     destruct (inst_run ge i m1 m1) eqn: Heqom.
+    + refine (IHp _ _ _ _ _ _); eauto.
+    + assert (X: exists x, term_eval ge (inst_smem i d d x) m0 = None).
+      { eapply inst_smem_None_correct; eauto. }
+      destruct X as [x H1].
+      generalize (H x).
+      erewrite block_smem_rec_abort; eauto.
+      congruence.
+Qed.
+
+Lemma bblock_smem_Some_correct2 p m0 m1:
+  pre (bblock_smem p) ge m0 ->
+  (forall x, term_eval ge (bblock_smem p x) m0 = Some (m1 x))
+  -> res_eq (Some m1) (run ge p m0).
+Proof.
+  intros; eapply bblocks_smem_rec_Some_correct2; eauto.
+Qed.
+
+Lemma inst_valid i m0 old (od:smem):
+  (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall (m1 m2: mem) (d: smem), 
+  pre d ge m0 ->
+  inst_run ge i m1 old = Some m2 ->
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+   pre (inst_smem 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 smem_set in * |- *; simpl. 
+    rewrite Hm1; intuition congruence.
+  + intros x0. unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto.
+    subst; erewrite term_eval_exp; eauto.
+Qed.
+
+
+Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem), 
+  pre d ge m0 ->
+  run ge p m1 = Some m2 -> 
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  pre (bblock_smem_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_smem_valid p m0 m1:
+  run ge p m0 = Some m1 ->
+  pre (bblock_smem p) ge m0.
+Proof.
+  intros; eapply block_smem_rec_valid; eauto.
+  unfold smem_empty; simpl. auto.
+Qed.
+
+Definition smem_valid ge d m := pre d ge m /\ forall x, term_eval ge (d x) m <> None.
+
+Definition smem_simu (d1 d2: smem): Prop :=
+     (forall m, smem_valid ge d1 m -> smem_valid ge d2 m)
+  /\ (forall m0 x, smem_valid ge d1 m0 -> 
+                   term_eval ge (d1 x) m0 = term_eval ge (d2 x) m0).
+
+
+Theorem bblock_smem_simu p1 p2:
+   smem_simu (bblock_smem p1) (bblock_smem p2) ->
+   bblock_simu ge p1 p2.
+Proof.
+  Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1.
+  intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-.
+  destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence.
+  assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto.
+  eapply bblock_smem_Some_correct2; eauto.
+  + destruct (INCL m); intuition eauto.
+    congruence.
+  + intro x; erewrite <- EQUIV; intuition eauto.
+    congruence.
+Qed.
+
+Lemma smem_valid_set_decompose_1 d t x m:
+  smem_valid ge (smem_set d x t) m -> smem_valid ge d m.
+Proof.
+  unfold smem_valid; intros ((PRE1 & PRE2) & VALID); split.
+  + intuition.
+  + intros x0 H. case (R.eq_dec x x0).
+    * intuition congruence.
+    * intros DIFF; eapply VALID. erewrite set_spec_diff; eauto.
+Qed.
+
+Lemma smem_valid_set_decompose_2 d t x m:
+  smem_valid ge (smem_set d x t) m -> term_eval ge t m <> None.
+Proof.
+  unfold smem_valid; intros ((PRE1 & PRE2) & VALID) H.
+  generalize (VALID x); rewrite set_spec_eq.
+  tauto.
+Qed.
+
+Lemma smem_valid_set_proof d x t m:
+  smem_valid ge d m -> term_eval ge t m <> None -> smem_valid ge (smem_set d x t) m.
+Proof.
+  unfold smem_valid; intros (PRE & VALID) PREt. split.
+  + split; auto.
+  + intros x0; unfold smem_set; simpl; case (R.eq_dec x x0); intros; subst; auto.
+Qed.
+
+
+End SIMU_THEORY.
+
+(** REMARKS: more abstract formulation of the proof... 
+    but relying on functional_extensionality.
+*)
+Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:=
+   forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)).
+
+Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m).
+Proof.
+  unfold smem_correct; simpl; intros m'; split.
+  + intros; split.
+    * eapply bblock_smem_valid; eauto.
+    * eapply bblock_smem_Some_correct1; eauto.
+  + intros (H1 & H2).
+    destruct (bblock_smem_Some_correct2 ge p m m') as (m2 & X & Y); eauto.
+    rewrite X. f_equal.
+    apply FunctionalExtensionality.functional_extensionality; auto.
+Qed.
+
+End SimuTheory.