Added AbstractBasicBlock files to the Coq build process

25 files changed, 4692 insertions, 0 deletions

diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
new file mode 100644
index 00000000..50ce000e
--- /dev/null
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -0,0 +1,214 @@
+(** Syntax and Sequential Semantics of Abstract Basic Blocks.
+*)
+
+
+Module Type ResourceNames.
+
+Parameter t: Type.
+
+Parameter eq_dec: forall (x y: t), { x = y } + { x<>y }.
+
+End ResourceNames.
+
+
+(** * Parameters of the language of Basic Blocks *)
+Module Type LangParam.
+
+Declare Module R: ResourceNames.
+
+Parameter value: Type.
+
+(** Declare the type of operations *)
+
+Parameter op: Type. (* type of operations *)
+
+(* NB: possible generalization
+ - relation after/before.
+*)
+Parameter op_eval: op -> list value -> option value.
+
+End LangParam.
+
+
+
+(** * Syntax and (sequential) semantics of "basic blocks" *)
+Module MkSeqLanguage(P: LangParam).
+
+Export P.
+
+Local Open Scope list.
+
+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.
+
+Inductive exp :=
+  | Name (x:R.t)
+  | Op (o:op) (le: list_exp)
+  | Old (e: exp)
+with list_exp :=
+  | Enil
+  | Econs (e:exp) (le:list_exp)
+  | LOld (le: list_exp)
+  .
+
+Fixpoint exp_eval (e: exp) (m old: mem): option value :=
+  match e with
+  | Name x => Some (m x)
+  | Op o le => 
+     match list_exp_eval le m old with
+     | Some lv => op_eval o lv
+     | _ => None
+     end
+  | Old e => exp_eval e old old
+  end
+with list_exp_eval (le: list_exp) (m old: mem): option (list value) :=
+  match le with
+  | Enil => Some nil
+  | Econs e le' =>
+     match exp_eval e m old, list_exp_eval le' m old with
+     | Some v, Some lv => Some (v::lv)
+     | _, _ => None
+     end
+  | LOld le => list_exp_eval le old old
+  end.
+
+Definition macro := list (R.t * exp). (* = a sequence of assignments *) 
+
+Fixpoint macro_run (i: macro) (m old: mem): option mem :=
+  match i with
+  | nil => Some m
+  | (x, e)::i' =>
+     match exp_eval e m old with
+     | Some v' => macro_run i' (assign m x v') old
+     | None => None
+     end
+  end.
+
+Definition bblock := list macro.
+
+Fixpoint run (p: bblock) (m: mem): option mem :=
+  match p with
+  | nil => Some m
+  | i::p' =>
+     match macro_run i m m with
+     | Some m' => run p' m'
+     | None => None
+     end
+  end.
+
+(* A few useful lemma *)
+Lemma assign_eq m x v:
+  (assign m x v) x = v.
+Proof.
+  unfold assign. destruct (R.eq_dec x x); try congruence.
+Qed.
+
+Lemma assign_diff m x y v:
+  x<>y -> (assign m x v) y = m y.
+Proof.
+  unfold assign. destruct (R.eq_dec x y); try congruence.
+Qed.
+
+Lemma assign_skips m x y:
+  (assign m x (m x)) y = m y.
+Proof.
+  unfold assign. destruct (R.eq_dec x y); try congruence.
+Qed.
+
+Lemma assign_swap m x1 v1 x2 v2 y:
+ x1 <> x2 -> (assign (assign m x1 v1) x2 v2) y = (assign (assign m x2 v2) x1 v1) y.
+Proof.
+  intros; destruct (R.eq_dec x2 y).
+  - subst. rewrite assign_eq, assign_diff; auto. rewrite assign_eq; auto.
+  - rewrite assign_diff; auto. 
+    destruct (R.eq_dec x1 y).
+    + subst; rewrite! assign_eq. auto.
+    + rewrite! assign_diff; auto. 
+Qed.
+
+
+(** A small theory of bblockram equality *)
+
+(* equalities on bblockram outputs *)
+Definition res_eq (om1 om2: option mem): Prop :=
+  match om1 with
+  | Some m1 => exists m2, om2 = Some m2 /\ forall x, m1 x = m2 x 
+  | None => om2 = None
+  end.
+
+Scheme exp_mut := Induction for exp Sort Prop
+with list_exp_mut := Induction for list_exp Sort Prop.
+
+Lemma exp_equiv e old1 old2:
+  (forall x, old1 x = old2 x) ->
+  forall m1 m2, (forall x, m1 x = m2 x) -> 
+   (exp_eval e m1 old1) = (exp_eval e m2 old2).
+Proof.
+  intros H1.
+  induction e using exp_mut with (P0:=fun l =>  forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); simpl; try congruence; auto.
+  - intros; erewrite IHe; eauto.
+  - intros; erewrite IHe, IHe0; auto.
+Qed.
+
+Definition bblock_equiv (p1 p2: bblock): Prop
+  := forall m, res_eq (run p1 m) (run p2 m).
+
+Lemma alt_macro_equiv_refl i old1 old2: 
+  (forall x, old1 x = old2 x) ->
+  forall m1 m2, (forall x, m1 x = m2 x) -> 
+  res_eq (macro_run i m1 old1) (macro_run i m2 old2).
+Proof.
+  intro H; induction i as [ | [x e]]; simpl; eauto.
+  intros m1 m2 H1. erewrite exp_equiv; eauto.
+  destruct (exp_eval e m2 old2); simpl; auto.
+  apply IHi.
+  unfold assign; intro y. destruct (R.eq_dec x y); auto. 
+Qed.
+
+Lemma alt_bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2).
+Proof.
+  induction p as [ | i p']; simpl; eauto.
+  intros m1 m2 H; lapply (alt_macro_equiv_refl i m1 m2); auto.
+  intros X; lapply (X m1 m2); auto; clear X.
+  destruct (macro_run i m1 m1); simpl.
+  - intros [m3 [H1 H2]]; rewrite H1; simpl; auto.
+  - intros H1; rewrite H1; simpl; auto.
+Qed.
+
+Lemma res_eq_sym om1 om2: res_eq om1 om2 -> res_eq om2 om1.
+Proof.
+  destruct om1; simpl.
+  - intros [m2 [H1 H2]]; subst; simpl. eauto.
+  - intros; subst; simpl; eauto.
+Qed.
+
+Lemma res_eq_trans (om1 om2 om3: option mem): 
+  (res_eq om1 om2) -> (res_eq om2 om3) -> (res_eq om1 om3).
+Proof.
+  destruct om1; simpl.
+  - intros [m2 [H1 H2]]; subst; simpl.
+    intros [m3 [H3 H4]]; subst; simpl.
+    eapply ex_intro; intuition eauto. rewrite H2; auto.
+  - intro; subst; simpl; auto.
+Qed.
+
+Lemma bblock_equiv_alt p1 p2: bblock_equiv p1 p2 <-> (forall m1 m2,  (forall x, m1 x = m2 x) -> res_eq (run p1 m1) (run p2 m2)).
+Proof.
+  unfold bblock_equiv; intuition.
+  intros; eapply res_eq_trans. eapply alt_bblock_equiv_refl; eauto.
+  eauto.
+Qed.
+ 
+End MkSeqLanguage.
+
+
+Module Type SeqLanguage.
+
+Declare Module LP: LangParam.
+
+Include MkSeqLanguage LP.
+
+End SeqLanguage.
+
diff --git a/mppa_k1c/abstractbb/DepExample.v b/mppa_k1c/abstractbb/DepExample.v
new file mode 100644
index 00000000..a239e24f
--- /dev/null
+++ b/mppa_k1c/abstractbb/DepExample.v
@@ -0,0 +1,151 @@
+(** Specification of the example illustrating how to use ImpDep. *)
+
+Require Export ZArith.
+
+Require Export ZArith.
+Require Export List.
+Export ListNotations.
+
+(* Syntax *)
+
+Definition reg := positive.
+
+Inductive operand :=
+  | Imm (i:Z)
+  | Reg (r:reg)
+  .
+
+Inductive arith_op := ADD | SUB | MUL.
+
+Inductive inst :=
+  | MOVE (dest: reg) (src: operand)
+  | ARITH (dest: reg) (op: arith_op) (src1 src2: operand)
+  | LOAD (dest base: reg) (offset: operand)
+  | STORE (src base: reg) (offset: operand)
+  | MEMSWAP (r base: reg) (offset: operand)
+  .
+
+Definition bblock := list inst.
+
+(* Semantics *)
+
+Definition value := Z.
+
+Definition addr := positive.
+
+Definition mem := addr -> value.
+
+Definition assign (m: mem) (x:addr) (v: value) :=
+ fun y => if Pos.eq_dec x y then v else (m y).
+
+Definition regmem := reg -> value.
+
+Record state := { sm: mem; rm: regmem }.
+
+Definition operand_eval (x: operand) (rm: regmem): value :=
+  match x with
+  | Imm i => i
+  | Reg r => rm r
+  end.
+
+Definition arith_op_eval (o: arith_op): value -> value -> value :=
+  match o with
+  | ADD => Z.add
+  | SUB => Z.sub
+  | MUL => Z.mul
+  end.
+
+Definition get_addr (base:reg) (offset:operand) (rm: regmem): option addr :=
+  let b := rm base in
+  let ofs := operand_eval offset rm in
+  match Z.add b ofs with
+  | Zpos p => Some p
+  | _ => None
+  end.
+
+(* two-state semantics -- dissociating read from write access.
+   - all read access on [sin] state
+   - all register write access modifies [sout] state
+   - all memory write access modifies [sin] state
+   => useful for parallel semantics
+   NB: in this parallel semantics -- there is at most one STORE by bundle
+   which is non-deterministically chosen...
+*)
+Definition sem_inst (i: inst) (sin sout: state): option state :=
+  match i with
+  | MOVE dest src =>
+      let v := operand_eval src (rm sin) in
+      Some {| sm := sm sout;
+              rm := assign (rm sout) dest v |}
+  | ARITH dest op src1 src2 =>
+      let v1 := operand_eval src1 (rm sin) in
+      let v2 := operand_eval src2 (rm sin) in
+      let v := arith_op_eval op v1 v2 in
+      Some {| sm := sm sout;
+              rm := assign (rm sout) dest v |}
+  | LOAD dest base offset =>
+      match get_addr base offset (rm sin) with
+      | Some srce =>
+          Some {| sm := sm sout;
+                  rm := assign (rm sout) dest (sm sin srce) |}
+      | None => None
+      end
+  | STORE srce base offset =>
+      match get_addr base offset (rm sin) with
+      | Some dest =>
+          Some {| sm := assign (sm sin) dest (rm sin srce);
+                  rm := rm sout |}
+      | None => None
+      end
+  | MEMSWAP x base offset =>
+      match get_addr base offset (rm sin) with
+      | Some ad =>
+          Some {| sm := assign (sm sin) ad (rm sin x);
+                  rm := assign (rm sout) x (sm sin ad) |}
+      | None => None
+      end
+  end.
+
+Local Open Scope list_scope.
+
+(** usual sequential semantics *)
+Fixpoint sem_bblock (p: bblock) (s: state): option state :=
+  match p with
+  | nil => Some s
+  | i::p' =>
+    match sem_inst i s s with
+    | Some s' => sem_bblock p' s'
+    | None => None
+    end
+  end.
+
+Definition state_equiv (s1 s2: state): Prop :=
+  (forall x, sm s1 x = sm s2 x) /\
+  (forall x, rm s1 x = rm s2 x). 
+
+(* equalities on bblockram outputs *)
+Definition res_equiv (os1 os2: option state): Prop :=
+  match os1 with
+  | Some s1 => exists s2, os2 = Some s2 /\ state_equiv s1 s2 
+  | None => os2 = None
+  end.
+
+
+Definition bblock_equiv (p1 p2: bblock): Prop :=
+  forall s, res_equiv (sem_bblock p1 s) (sem_bblock p2 s).
+
+(** parallel semantics with in-order writes *)
+Fixpoint sem_bblock_par_iw (p: bblock) (sin sout: state): option state :=
+  match p with
+  | nil => Some sout
+  | i::p' =>
+    match sem_inst i sin sout with
+    | Some sout' => sem_bblock_par_iw p' sin sout'
+    | None => None
+    end
+  end.
+
+(** parallelism semantics with arbitrary order writes *)
+Require Import Sorting.Permutation.
+
+Definition sem_bblock_par (p: bblock) (sin: state) (sout: option state) := exists p', res_equiv sout (sem_bblock_par_iw p' sin sin) /\ Permutation p p'.
diff --git a/mppa_k1c/abstractbb/DepExampleDemo.v b/mppa_k1c/abstractbb/DepExampleDemo.v
new file mode 100644
index 00000000..c2079b70
--- /dev/null
+++ b/mppa_k1c/abstractbb/DepExampleDemo.v
@@ -0,0 +1,396 @@
+(** Demo of the example illustrating how to use ImpDep. *)
+
+Require Import DepExampleEqTest.
+Require Import Bool.
+
+Open Scope Z_scope.
+
+Module EqTests.
+
+(**** TESTS DRIVER ! ****)
+
+Record test_input := {
+  name: pstring;
+  expected: bool;
+  verbose: bool;
+  p1: bblock;
+  p2: bblock;
+}.
+
+Definition run1 (t: test_input): ?? unit :=
+  print ((name t) +; " =>");;
+  DO result <~ bblock_eq_test (verbose t) (p1 t) (p2 t);;
+  assert_b (eqb result (expected t))  "UNEXPECTED RESULT";;
+  if expected t 
+  then println " SUCCESS" 
+  else RET tt  (* NB: in this case - bblock_eq_test is expected to have print an ERROR mesg *)
+  .
+
+Local Hint Resolve eqb_prop.
+
+Lemma run1_correctness (t: test_input):
+  WHEN run1 t ~> _ THEN (expected t)=true -> bblock_equiv (p1 t) (p2 t).
+Proof.
+  unfold run1; destruct t; simpl; wlp_simplify; subst.
+Qed.
+Global Opaque run1.
+Hint Resolve run1_correctness: wlp.
+
+Fixpoint run_all (l: list test_input): ?? unit :=
+  match l with
+  | nil => RET tt
+  | t::l' =>
+     println "" ;; (* SOME SPACES ! *)
+     run1 t;;
+     run_all l'
+  end.
+
+Lemma run_all_correctness l:
+  WHEN run_all l ~> _ THEN (forall t, List.In t l -> (expected t)=true -> bblock_equiv (p1 t) (p2 t)).
+Proof.
+  induction l; simpl; wlp_simplify; subst; auto.
+Qed.
+Global Opaque run_all.
+
+(**** TESTS ****)
+
+Definition move (dst src: reg) := MOVE dst (Reg src).
+Definition add_imm (dst src: reg) (z:Z) := ARITH dst ADD (Reg src) (Imm z).
+Definition incr (r: reg) (z:Z) := add_imm r r z.
+Definition add (dst src1 src2: reg) := ARITH dst ADD (Reg src1) (Reg src2).
+
+Definition load (dst src:reg) (ofs:Z) := LOAD dst src (Imm ofs).
+Definition store (src dst:reg) (ofs:Z) := STORE src dst (Imm ofs).
+Definition memswap (r base:reg) (ofs:Z) := MEMSWAP r base (Imm ofs).
+
+Definition R1: reg := 1%positive.
+Definition R2: reg := 2%positive.
+Definition R3: reg := 3%positive.
+Definition R4: reg := 4%positive.
+
+
+Definition demo: ?? unit := run_all [
+
+    {| name:="move_ok" ;
+       expected:=true;
+       verbose:=true;
+       p1:=[ move R2 R1; move R3 R1 ];
+       p2:=[ move R3 R1; move R2 R3 ]; 
+    |} ;
+    {| name:="move_ko" ;
+       expected:=false;
+       verbose:=true;
+       p1:=[ move R2 R1; move R3 R1 ];
+       p2:=[ move R3 R1 ]; 
+    |} ;
+
+    {| name:="add_load_RAR_ok" ;
+       expected:=true;
+       verbose:=true;
+       p1:=[ add_imm R1 R2 5; move R4 R2; load R3 R2 2  ];
+       p2:=[ load R3 R2 2; add_imm R1 R2 5; move R4 R2 ]; |} ;
+
+    {| name:="add_load_RAW_ko";
+       expected:=false;
+       verbose:=true;
+       p1:=[ add_imm R1 R2 5; move R4 R2; load R3 R1 2 ];
+       p2:=[ load R3 R1 2; add_imm R1 R2 5; move R4 R2 ]; |} ;
+
+    {| name:="add_load_WAW_ko";
+       expected:=false;
+       verbose:=true;
+       p1:=[ add_imm R3 R2 5; move R4 R2; load R3 R1 2 ];
+       p2:=[ load R3 R1 2; add_imm R3 R2 5; move R4 R2 ]; |} ;
+
+    {| name:="memswap_ok1";
+       expected:=true;
+       verbose:=true;
+       p1:=[ add_imm R1 R2 5; memswap R3 R2 2 ];
+       p2:=[ memswap R3 R2 2; add_imm R1 R2 5 ]; |} ;
+
+    {| name:="memswap_ok2" ;
+       expected:=true;
+       verbose:=true;
+       p1:=[ load R1 R2 2; store R3 R2 2; move R3 R1];
+       p2:=[ memswap R3 R2 2 ; move R1 R3 ];
+     |} ;
+
+    {| name:="memswap_ko" ;
+       expected:=false;
+       verbose:=true;
+       p1:=[ load R3 R2 2; store R3 R2 2];
+       p2:=[ memswap R3 R2 2 ];
+     |}
+].
+
+
+Fixpoint repeat_aux (n:nat) (rev_body next: bblock): bblock :=
+  match n with
+  | O => next
+  | (S n) => repeat_aux n rev_body (List.rev_append rev_body next)
+  end.
+
+Definition repeat n body next := repeat_aux n (List.rev_append body []) next.
+
+
+Definition inst1 := add R1 R1 R2. 
+
+(* NB: returns [inst1^10; next] *)
+Definition dummy1 next:= repeat 10%nat [inst1] next.
+
+Definition main: ?? unit := run_all [
+
+    {| name:="move_never_skips1" ;
+       expected:=false;
+       verbose:=false;
+       p1:=[ move R2 R2 ];
+       p2:=[ ]; 
+    |} ;
+
+    {| name:="move_compress_ok" ;
+       expected:=true;
+       verbose:=false;
+       p1:=[ move R1 R2; move R2 R1; MOVE R1 (Imm 7) ];
+       p2:=[ MOVE R1 (Imm 7); move R2 R2 ]; 
+     |} ;
+
+    {| name:="move_never_skip2" ;
+       expected:=false;
+       verbose:=false;
+       p1:=[ move R1 R2; move R2 R1; MOVE R1 (Imm 7) ];
+       p2:=[ MOVE R1 (Imm 7) ]; 
+     |} ;
+
+    {| name:="R2_RAR_ok1"; 
+       expected:=true; 
+       verbose:=false;
+       p1:=dummy1 [ load R3 R2 2; store R3 R4 7 ];
+       p2:=load R3 R2 2::store R3 R4 7::(dummy1 nil) |} ;
+    {| name:="R2_RAR_ok2"; 
+       expected:=true; 
+       verbose:=false;
+       p1:=dummy1 [ load R3 R2 2; store R3 R4 7 ];
+       p2:=load R3 R2 2::(dummy1 [store R3 R4 7]) |} ;
+    {| name:="R2_RAR_ok3"; 
+       expected:=true; 
+       verbose:=false;
+       p1:=dummy1 [ load R3 R2 2; store R3 R4 7 ];
+       p2:=load R3 R2 2::(repeat 4%nat [inst1;inst1] [store R3 R4 7; inst1; inst1]) |} ;
+    {| name:="bad_register_name_ko"; 
+       expected:=false; 
+       verbose:=false;
+       p1:=dummy1 [ load R3 R2 2 ];
+       p2:=dummy1 [ load R3 R3 2 ] |} ;
+    {| name:="bad_instruction_ko"; 
+       expected:=false; 
+       verbose:=false;
+       p1:=dummy1 [ load R3 R2 2 ];
+       p2:=dummy1 [ store R3 R2 2 ] |} ;
+    {| name:="incompleteness_ko"; 
+       expected:=false; 
+       verbose:=false;
+       p1:=dummy1 [ load R3 R2 2 ];
+       p2:=[inst1; load R3 R2 2] |} ;
+
+
+    {| name:="R2_WAR_ko"; 
+       expected:=false; 
+       verbose:=false;
+       p1:=dummy1 [ load R2 R3 2 ];
+       p2:=load R2 R3 2::(dummy1 nil) |} ;
+    {| name:="bad_register_name_ko2"; 
+       expected:=false; 
+       verbose:=false;
+       p1:=dummy1 [ load R2 R3 2 ];
+       p2:=load R3 R2 2::(dummy1 nil) |} ;
+
+
+    {| name:="load_RAR_ok1";
+       expected:=true;
+       verbose:=false;
+       p1:=[ load R1 R2 2; load R3 R4 5];
+       p2:=[ load R3 R4 5; load R1 R2 2]; |} ;
+    {| name:="load_RAR_ok2";
+       expected:=true;
+       verbose:=false;
+       p1:=[ load R1 R2 2; load R3 R2 5];
+       p2:=[ load R3 R2 5; load R1 R2 2]; |} ;
+    {| name:="load_WAW_ko";
+       expected:=false;
+       verbose:=false;
+       p1:=[ load R1 R2 2; load R1 R4 5];
+       p2:=[ load R1 R4 5; load R1 R2 2]; |} ;
+    {| name:="load_store_WAR_ko";
+       expected:=false;
+       verbose:=false;
+       p1:=[ load R1 R2 2; store R3 R4 5];
+       p2:=[ store R3 R4 5; load R1 R2 2]; |}
+
+  ].
+
+Definition incr_R1_5 := incr R1 5.
+Definition incr_R2_3 := incr R2 3.
+
+Definition big_test (bigN:nat) (name: pstring): ?? unit :=
+    println "";;
+    println("---- Time of bigtest " +; name);;
+    timer(run_all, [
+
+    {| name:="big_test_ok1"; 
+       expected:=true; 
+       verbose:=false;
+       p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3];
+       p2:=repeat bigN [incr_R1_5] (repeat (S bigN) [incr_R2_3] nil) |} ;
+    {| name:="big_test_ok2"; 
+       expected:=true; 
+       verbose:=false;
+       p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3];
+       p2:=repeat bigN [incr_R2_3;incr_R1_5] [incr_R2_3] |} ;
+    {| name:="big_test_ok3"; 
+       expected:=true; 
+       verbose:=false;
+       p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3];
+       p2:=repeat (S bigN) [incr_R2_3] (repeat bigN [incr_R1_5] nil) |} ;
+    {| name:="big_test_ko1"; 
+       expected:=false; 
+       verbose:=false;
+       p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3];
+       p2:=repeat bigN [incr_R1_5] (repeat bigN [incr_R2_3] nil) |} ;
+    {| name:="big_test_ko2"; 
+       expected:=false; 
+       verbose:=false;
+       p1:=repeat bigN [incr_R1_5;incr_R2_3] [incr_R2_3];
+       p2:=repeat (S bigN) [incr_R1_5] (repeat bigN [incr_R2_3] nil) |}
+
+  ]).
+
+Fixpoint big_tests (l:list (nat * string)) :=
+  match l with
+  | nil => RET tt
+  | (x,s)::l' => big_test x s;; big_tests l'
+  end.
+
+Local Open Scope nat_scope.
+Local Open Scope string_scope.
+
+Definition big_runs: ?? unit :=
+  big_tests [(2500, "2500"); (5000, "5000"); (10000, "10000"); (20000, "20000")].
+
+
+End EqTests.
+
+
+Require Import DepExampleParallelTest.
+
+Module ParaTests.
+
+
+(**** TESTS DRIVER ! ****)
+
+Record test_input := {
+  name: pstring;
+  expected: bool;
+  bundle: bblock;
+}.
+
+Definition run1 (t: test_input): ?? unit :=
+  print ((name t) +; " =>");;
+  assert_b (eqb (bblock_is_para (bundle t)) (expected t))  "UNEXPECTED RESULT";;
+  if expected t 
+  then println " SUCCESS" 
+  else println " FAILED (as expected)"
+  .
+
+Local Hint Resolve eqb_prop.
+
+Definition correct_bundle p := forall s os', (sem_bblock_par p s os' <-> res_equiv os' (sem_bblock p s)).
+
+Lemma run1_correctness (t: test_input):
+  WHEN run1 t ~> _ THEN (expected t)=true -> correct_bundle (bundle t).
+Proof.
+  unfold run1; destruct t; simpl; wlp_simplify; subst.
+  - unfold correct_bundle; intros; apply bblock_is_para_correct; auto.
+  - discriminate.
+Qed.
+Global Opaque run1.
+Hint Resolve run1_correctness: wlp.
+
+Fixpoint run_all (l: list test_input): ?? unit :=
+  match l with
+  | nil => RET tt
+  | t::l' =>
+     run1 t;;
+     run_all l'
+  end.
+
+Lemma run_all_correctness l:
+  WHEN run_all l ~> _ THEN (forall t, List.In t l -> (expected t)=true -> correct_bundle (bundle t)).
+Proof.
+  induction l; simpl; wlp_simplify; subst; auto.
+Qed.
+Global Opaque run_all.
+
+(**** TESTS ****)
+
+Definition add_imm (dst src: reg) (z:Z) := ARITH dst ADD (Reg src) (Imm z).
+
+Definition load (dst src:reg) (ofs:Z) := LOAD dst src (Imm ofs).
+Definition store (src dst:reg) (ofs:Z) := STORE src dst (Imm ofs).
+Definition memswap (r base:reg) (ofs:Z) := MEMSWAP r base (Imm ofs).
+
+Definition R1: reg := 1%positive.
+Definition R2: reg := 2%positive.
+Definition R3: reg := 3%positive.
+Definition R4: reg := 4%positive.
+Definition R5: reg := 5%positive.
+Definition R6: reg := 5%positive.
+
+
+Definition main: ?? unit :=
+  println "";;
+  println "-- Parallel Checks --";; 
+  run_all [
+   {| name:="test_war_ok"; 
+      expected:=true; 
+      bundle:=[add_imm R1 R2 2;add_imm R2 R2 3]
+    |};
+   {| name:="test_raw_ko"; 
+      expected:=false; 
+      bundle:=[add_imm R1 R2 2;add_imm R2 R1 3]
+    |};
+   {| name:="test_waw_ko"; 
+      expected:=false; 
+      bundle:=[add_imm R1 R2 2;add_imm R1 R2 3]
+    |};
+   {| name:="test_war_load_store_ok"; 
+      expected:=true; 
+      bundle:=[load R1 R2 2;load R2 R3 3; store R3 R4 4]
+    |};
+   {| name:="test_raw_load_store_ko"; 
+      expected:=false; 
+      bundle:=[load R1 R2 2;store R5 R4 4;load R2 R3 3]
+    |};
+   {| name:="test_waw_load_store_ko"; 
+      expected:=false; 
+      bundle:=[load R1 R2 2;store R3 R2 3;store R5 R4 4]
+    |};
+   {| name:="test_arith_load_store_ok"; 
+      expected:=true; 
+      bundle:=[load R1 R2 2; add_imm R2 R4 3; load R3 R6 3; add_imm R4 R4 3; store R6 R5 4; add_imm R6 R6 7]
+    |}
+  ].
+ 
+End ParaTests.
+
+(*************************)
+(* Extraction directives *)
+
+Require Import ExtrOcamlString.
+Require Import ExtrOcamlBasic.
+
+Import ImpConfig.
+
+Extraction Blacklist List String.
+
+Separate Extraction BinIntDef EqTests ParaTests.
+
diff --git a/mppa_k1c/abstractbb/DepExampleEqTest.v b/mppa_k1c/abstractbb/DepExampleEqTest.v
new file mode 100644
index 00000000..50bfc2f4
--- /dev/null
+++ b/mppa_k1c/abstractbb/DepExampleEqTest.v
@@ -0,0 +1,326 @@
+(** Implementation of the example illustrating how to use ImpDep. *)
+
+Require Export DepExample.
+Require Export Impure.ImpIO.
+Export Notations.
+
+Require Import ImpDep.
+
+Open Scope impure.
+
+Module P<: ImpParam.
+
+Module R := Pos.
+
+Inductive value_wrap :=
+  | Std (v:value)  (* value = DepExample.value *)
+  | Mem (m:mem)
+  .
+
+Inductive op_wrap :=
+  (* constants *)
+  | Imm (i:Z)
+  (* arithmetic operation *)
+  | ARITH (op: arith_op)
+  | LOAD
+  | STORE
+  .
+
+Definition op_eval (op: op_wrap) (l:list value_wrap): option value_wrap :=
+  match op, l with
+  | Imm i, [] => Some (Std i)
+  | ARITH op, [Std v1; Std v2] => Some (Std (arith_op_eval op v1 v2))
+  | LOAD, [Mem m; Std base; Std offset] =>
+     match (Z.add base offset) with
+     | Zpos srce => Some (Std (m srce))
+     | _ => None
+     end
+  | STORE, [Mem m; Std srce; Std base; Std offset] =>
+     match (Z.add base offset) with
+     | Zpos dest => Some (Mem (assign m dest srce))
+     | _ => None
+     end
+  | _, _ => None
+  end.
+
+
+Definition value:=value_wrap.
+Definition op:=op_wrap.
+
+
+Definition op_eq (o1 o2: op_wrap): ?? bool :=
+  match o1, o2 with
+  | Imm i1, Imm i2 => phys_eq i1 i2
+  | ARITH o1, ARITH o2 => phys_eq o1 o2
+  | LOAD, LOAD => RET true
+  | STORE, STORE => RET true
+  | _, _ => RET false
+  end.
+
+Lemma op_eq_correct o1 o2: 
+ WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2.
+Proof.
+  destruct o1, o2; wlp_simplify; congruence.
+Qed.
+
+End P.
+
+
+Module L <: ISeqLanguage with Module LP:=P.
+
+Module LP:=P.
+
+Include MkSeqLanguage P.
+
+End L.
+
+
+Module IDT := ImpDepTree L ImpPosDict.
+
+(** Compilation from DepExample to L *)
+
+Definition the_mem: P.R.t := 1.
+Definition reg_map (r: reg): P.R.t := Pos.succ r.
+
+Coercion L.Name: P.R.t >-> L.exp.
+
+Definition comp_op (o:operand): L.exp :=
+  match o with
+  | Imm i => L.Op (P.Imm i) L.Enil
+  | Reg r => reg_map r
+  end.
+
+Definition comp_inst (i: inst): L.macro :=
+  match i with
+  | MOVE dest src => 
+     [ (reg_map dest, (comp_op src)) ]
+  | ARITH dest op src1 src2 =>
+     [ (reg_map dest, L.Op (P.ARITH op) (L.Econs (comp_op src1) (L.Econs (comp_op src2) L.Enil))) ]
+  | LOAD dest base offset =>
+     [ (reg_map dest, L.Op P.LOAD (L.Econs the_mem (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil)))) ]
+  | STORE srce base offset =>
+     [ (the_mem, L.Op P.STORE (L.Econs the_mem (L.Econs (reg_map srce) (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil))))) ]
+  | MEMSWAP x base offset =>
+     [ (reg_map x, L.Op P.LOAD (L.Econs the_mem (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil))));
+       (the_mem, L.Old (L.Op P.STORE (L.Econs the_mem (L.Econs (reg_map x) (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil)))))) ]
+  end.
+
+Fixpoint comp_bblock (p: bblock): L.bblock :=
+  match p with
+  | nil => nil
+  | i::p' => (comp_inst i)::(comp_bblock p')
+  end.
+
+(** Correctness proof of the compiler *)
+
+Lemma the_mem_separation: forall r, reg_map r <> the_mem.
+Proof.
+  intros r; apply Pos.succ_not_1.
+Qed.
+
+Lemma reg_map_separation: forall r1 r2, r1 <> r2 -> reg_map r1 <> reg_map r2.
+Proof.
+  unfold reg_map; intros r1 r2 H1 H2; lapply (Pos.succ_inj r1 r2); auto.
+Qed.
+
+Local Hint Resolve the_mem_separation reg_map_separation.
+
+Definition match_state (s: state) (m:L.mem): Prop :=
+  m the_mem = P.Mem (sm s)  /\ forall r, m (reg_map r) = P.Std (rm s r).
+
+Definition trans_state (s: state): L.mem :=
+  fun x => 
+  if Pos.eq_dec x the_mem 
+  then P.Mem (sm s)
+  else P.Std (rm s (Pos.pred x)).
+
+Lemma match_trans_state (s:state): match_state s (trans_state s).
+Proof.
+  unfold trans_state; constructor 1.
+  - destruct (Pos.eq_dec the_mem the_mem); try congruence.
+  - intros r; destruct (Pos.eq_dec (reg_map r) the_mem).
+    * generalize the_mem_separation; subst; congruence.
+    * unfold reg_map; rewrite Pos.pred_succ. auto.
+Qed.
+
+Definition match_option_state (os: option state) (om:option L.mem): Prop :=
+  match os with
+  | Some s => exists m, om = Some m /\ match_state s m
+  | None => om = None
+  end.
+
+Lemma comp_op_correct o s m old: match_state s m -> L.exp_eval (comp_op o) m old = Some (P.Std (operand_eval o (rm s))).
+Proof.
+  destruct 1 as [H1 H2]; destruct o; simpl; auto.
+  rewrite H2; auto.
+Qed.
+
+Lemma comp_bblock_correct_aux p: forall s m,  match_state s m -> match_option_state (sem_bblock p s) (L.run (comp_bblock p) m).
+Proof.
+  induction p as [| i p IHp]; simpl; eauto.
+  intros s m H; destruct i; simpl; erewrite !comp_op_correct; eauto; simpl.
+  - (* MOVE *)
+    apply IHp.
+    destruct H as [H1 H2]; constructor 1; simpl.
+    + rewrite L.assign_diff; auto.
+    + unfold assign; intros r; destruct (Pos.eq_dec dest r).
+      * subst; rewrite L.assign_eq; auto.
+      * rewrite L.assign_diff; auto.
+  - (* ARITH *)
+    apply IHp.
+    destruct H as [H1 H2]; constructor 1; simpl.
+    + rewrite L.assign_diff; auto.
+    + unfold assign; intros r; destruct (Pos.eq_dec dest r).
+      * subst; rewrite L.assign_eq; auto.
+      * rewrite L.assign_diff; auto.
+  - (* LOAD *)
+    destruct H as [H1 H2].
+    rewrite H1, H2; simpl.
+    unfold get_addr.
+    destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto.
+    apply IHp.
+    constructor 1; simpl.
+    + rewrite L.assign_diff; auto.
+    + unfold assign; intros r; destruct (Pos.eq_dec dest r).
+      * subst; rewrite L.assign_eq; auto.
+      * rewrite L.assign_diff; auto.
+  - (* STORE *)
+    destruct H as [H1 H2].
+    rewrite H1, !H2; simpl.
+    unfold get_addr.
+    destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto.
+    apply IHp.
+    constructor 1; simpl; auto.
+    + intros r; rewrite L.assign_diff; auto.
+  - (* MEMSWAP *)
+    destruct H as [H1 H2].
+    rewrite H1, !H2; simpl.
+    unfold get_addr.
+    destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto.
+    apply IHp.
+    constructor 1; simpl; auto.
+    intros r0; rewrite L.assign_diff; auto.
+    unfold assign; destruct (Pos.eq_dec r r0).
+    * subst; rewrite L.assign_eq; auto.
+    * rewrite L.assign_diff; auto.
+Qed.
+
+Lemma comp_bblock_correct p s: match_option_state (sem_bblock p s) (L.run (comp_bblock p) (trans_state s)).
+Proof.
+  eapply comp_bblock_correct_aux. apply match_trans_state.
+Qed.
+
+Lemma state_equiv_from_match (s1 s2: state) (m: L.mem) : 
+  (match_state s1 m) -> (match_state s2 m) -> (state_equiv s1 s2).
+Proof.
+  unfold state_equiv, match_state. intuition.
+  - congruence. 
+  - assert (P.Std (rm s1 x) = P.Std (rm s2 x)); congruence.
+Qed.
+
+Definition match_option_stateX (om:option L.mem) (os:option state): Prop :=
+  match om with
+  | Some m => exists s, os = Some s /\ match_state s m
+  | None => os = None
+  end.
+
+Local Hint Resolve state_equiv_from_match.
+
+Lemma res_equiv_from_match (os1 os2: option state) (om: option L.mem): 
+  (match_option_state os1 om) -> (match_option_stateX om os2) -> (res_equiv os1 os2).
+Proof.
+  destruct os1 as [s1|]; simpl.
+  - intros [m [H1 H2]]; subst; simpl.
+    intros [s2 [H3 H4]]; subst; simpl.
+    eapply ex_intro; intuition eauto.
+  - intro; subst; simpl; auto.
+Qed.
+
+
+Lemma match_option_state_intro_X om os: match_option_state os om -> match_option_stateX om os.
+Proof.
+  destruct os as [s | ]; simpl.
+  - intros [m [H1 H2]]. subst; simpl. eapply ex_intro; intuition eauto.
+  - intros; subst; simpl; auto.
+Qed.
+
+
+Lemma match_from_res_eq om1 om2 os: 
+  L.res_eq om2 om1 -> match_option_stateX om1 os ->  match_option_stateX om2 os.
+Proof.
+  destruct om2 as [m2 | ]; simpl.
+  - intros [m [H1 H2]]. subst; simpl.
+    intros [s [H3 H4]]; subst; simpl.
+    eapply ex_intro; intuition eauto.
+    unfold match_state in * |- *.
+    intuition (rewrite H2; auto).
+  - intros; subst; simpl; auto.
+Qed.
+
+Lemma bblock_equiv_reduce p1 p2: L.bblock_equiv (comp_bblock p1) (comp_bblock p2) -> bblock_equiv p1 p2.
+Proof.
+  unfold L.bblock_equiv, bblock_equiv.
+  intros; eapply res_equiv_from_match.
+  apply comp_bblock_correct.
+  eapply match_from_res_eq. eauto.
+  apply match_option_state_intro_X. 
+  apply comp_bblock_correct.
+Qed.
+
+
+
+
+(* NB: pretty-printing functions below only mandatory for IDT.verb_bblock_eq_test *)
+Local Open Scope string_scope.
+
+Definition string_of_name (x: P.R.t): ?? pstring :=
+  match x with
+  | xH => RET (Str ("the_mem"))
+  | _ as x => 
+     DO s <~ string_of_Z (Zpos (Pos.pred x)) ;;
+     RET ("R" +; s)
+  end.
+
+Definition string_of_op (op: P.op): ?? pstring :=
+  match op with
+  | P.Imm i => 
+     DO s <~ string_of_Z i ;;
+     RET s
+  | P.ARITH ADD => RET (Str "ADD")
+  | P.ARITH SUB => RET (Str "SUB")
+  | P.ARITH MUL => RET (Str "MUL")
+  | P.LOAD => RET (Str "LOAD")
+  | P.STORE => RET (Str "STORE")
+  end.
+
+Definition bblock_eq_test (verb: bool) (p1 p2: bblock) : ?? bool :=
+  if verb then
+    IDT.verb_bblock_eq_test string_of_name string_of_op (comp_bblock p1) (comp_bblock p2)
+  else
+    IDT.bblock_eq_test (comp_bblock p1) (comp_bblock p2).
+
+Local Hint Resolve IDT.bblock_eq_test_correct bblock_equiv_reduce IDT.verb_bblock_eq_test_correct: wlp.
+
+
+Theorem bblock_eq_test_correct verb p1 p2 : 
+  WHEN bblock_eq_test verb p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque bblock_eq_test.
+Hint Resolve bblock_eq_test_correct: wlp.
+
+(* TEST: we can coerce this bblock_eq_test into a pure function (even if this is a little unsafe). *)
+(*
+Import UnsafeImpure.
+
+Definition pure_eq_test v (p1 p2: bblock) : bool := unsafe_coerce (bblock_eq_test v p1 p2).
+
+Theorem pure_eq_test_correct v p1 p2 : 
+   pure_eq_test v p1 p2 = true -> bblock_equiv p1 p2.
+Proof.
+   unfold pure_eq_test. intros; eapply bblock_eq_test_correct.
+   - apply unsafe_coerce_not_really_correct; eauto.
+   - eauto.
+Qed.
+*)
\ No newline at end of file
diff --git a/mppa_k1c/abstractbb/DepExampleParallelTest.v b/mppa_k1c/abstractbb/DepExampleParallelTest.v
new file mode 100644
index 00000000..00f33540
--- /dev/null
+++ b/mppa_k1c/abstractbb/DepExampleParallelTest.v
@@ -0,0 +1,161 @@
+Require Import DepExampleEqTest.
+Require Import Parallelizability.
+
+Module PChk := ParallelChecks L PosResourceSet.
+
+Definition bblock_is_para (p: bblock) : bool :=
+  PChk.is_parallelizable (comp_bblock p).
+
+Local Hint Resolve the_mem_separation reg_map_separation.
+
+(* Actually, almost the same proof script than [comp_bblock_correct_aux] !
+   We could definitely factorize the proof through a lemma on compilation to macros.
+*)
+Lemma comp_bblock_correct_para_iw p: forall sin sout min mout,
+  match_state sin min -> 
+  match_state sout mout ->
+  match_option_state (sem_bblock_par_iw p sin sout) (PChk.prun_iw (comp_bblock p) mout min).
+Proof.
+  induction p as [|i p IHp]; simpl; eauto.
+  intros sin sout min mout Hin Hout; destruct i; simpl; erewrite !comp_op_correct; eauto; simpl.
+  - (* MOVE *)
+    apply IHp; auto.
+    destruct Hin as [H1 H2]; destruct Hout as [H3 H4]; constructor 1; simpl; auto.
+    + rewrite L.assign_diff; auto.
+    + unfold assign; intros r; destruct (Pos.eq_dec dest r).
+      * subst; rewrite L.assign_eq; auto.
+      * rewrite L.assign_diff; auto.
+  - (* ARITH *)
+    apply IHp; auto.
+    destruct Hin as [H1 H2]; destruct Hout as [H3 H4]; constructor 1; simpl; auto.
+    + rewrite L.assign_diff; auto.
+    + unfold assign; intros r; destruct (Pos.eq_dec dest r).
+      * subst; rewrite L.assign_eq; auto.
+      * rewrite L.assign_diff; auto.
+  - (* LOAD *)
+    destruct Hin as [H1 H2]; destruct Hout as [H3 H4].
+    rewrite H1, H2; simpl.
+    unfold get_addr.
+    destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto.
+    apply IHp. { constructor 1; auto. }
+    constructor 1; simpl.
+    + rewrite L.assign_diff; auto.
+    + unfold assign; intros r; destruct (Pos.eq_dec dest r).
+      * subst; rewrite L.assign_eq; auto.
+      * rewrite L.assign_diff; auto.
+  - (* STORE *)
+    destruct Hin as [H1 H2]; destruct Hout as [H3 H4].
+    rewrite H1, !H2; simpl.
+    unfold get_addr.
+    destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto.
+    apply IHp. { constructor 1; auto. }
+    constructor 1; simpl; auto.
+    intros r; rewrite L.assign_diff; auto.
+  - (* MEMSWAP *)
+    destruct Hin as [H1 H2]; destruct Hout as [H3 H4].
+    rewrite H1, !H2; simpl.
+    unfold get_addr.
+    destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto.
+    apply IHp. { constructor 1; auto. }
+    constructor 1; simpl; auto.
+    + intros r0; rewrite L.assign_diff; auto.
+      unfold assign; destruct (Pos.eq_dec r r0).
+      * subst; rewrite L.assign_eq; auto.
+      * rewrite L.assign_diff; auto.
+Qed.
+
+Local Hint Resolve match_trans_state.
+
+Definition trans_option_state (os: option state): option L.mem :=
+  match os with
+  | Some s => Some (trans_state s)
+  | None => None
+  end.
+
+Lemma match_trans_option_state os: match_option_state os (trans_option_state os).
+Proof.
+  destruct os; simpl; eauto.
+Qed.
+
+Local Hint Resolve match_trans_option_state comp_bblock_correct match_option_state_intro_X match_from_res_eq res_equiv_from_match.
+
+Lemma is_mem_reg (x: P.R.t): x=the_mem \/ exists r, x=reg_map r.
+Proof.
+  case (Pos.eq_dec x the_mem); auto.
+  unfold the_mem, reg_map; constructor 2.
+  eexists (Pos.pred x). rewrite Pos.succ_pred; auto.
+Qed.
+
+Lemma res_eq_from_match (os: option state) (om1 om2: option L.mem): 
+  (match_option_stateX om1 os) -> (match_option_state os om2) -> (L.res_eq om1 om2).
+Proof.
+  destruct om1 as [m1|]; simpl.
+  - intros (s & H1 & H2 & H3); subst; simpl.
+    intros (m2 & H4 & H5 & H6); subst; simpl.
+    eapply ex_intro; intuition eauto.
+    destruct (is_mem_reg x) as [H|(r & H)]; subst; congruence.
+  - intro; subst; simpl; auto.
+Qed.
+
+(* We use axiom of functional extensionality ! *)
+Require Coq.Logic.FunctionalExtensionality.
+
+Lemma match_from_res_equiv os1 os2 om: 
+  res_equiv os2 os1 -> match_option_state os1 om ->  match_option_state os2 om.
+Proof.
+  destruct os2 as [s2 | ]; simpl.
+  - intros (s & H1 & H2 & H3). subst; simpl.
+    intros (m & H4 & H5 & H6); subst; simpl.
+    eapply ex_intro; intuition eauto.
+    constructor 1.
+    + rewrite H5; apply f_equal; eapply FunctionalExtensionality.functional_extensionality; auto.
+    + congruence.
+  - intros; subst; simpl; auto.
+Qed.
+
+
+Require Import Sorting.Permutation.
+
+Local Hint Constructors Permutation.
+
+Lemma comp_bblock_Permutation p p': Permutation p p' -> Permutation (comp_bblock p) (comp_bblock p').
+Proof.
+ induction 1; simpl; eauto.
+Qed.
+
+Lemma comp_bblock_Permutation_back p1 p1': Permutation p1 p1' -> 
+  forall p, p1=comp_bblock p ->
+  exists p', p1'=comp_bblock p' /\ Permutation p p'.
+Proof.
+ induction 1; simpl; eauto.
+ - destruct p as [|i p]; simpl; intro X; inversion X; subst.
+   destruct (IHPermutation p) as (p' & H1 & H2); subst; auto.
+   eexists (i::p'). simpl; eauto.
+ - destruct p as [|i1 p]; simpl; intro X; inversion X as [(H & H1)]; subst; clear X.
+   destruct p as [|i2 p]; simpl; inversion_clear H1.
+   eexists (i2::i1::p). simpl; eauto.
+ - intros p H1; destruct (IHPermutation1 p) as (p' & H2 & H3); subst; auto.
+   destruct (IHPermutation2 p') as (p'' & H4 & H5); subst; eauto.
+Qed.
+
+Local Hint Resolve comp_bblock_Permutation res_eq_from_match match_from_res_equiv comp_bblock_correct_para_iw.
+
+Lemma bblock_par_iff_prun p s os': 
+ sem_bblock_par p s os' <-> PChk.prun (comp_bblock p) (trans_state s) (trans_option_state os').
+Proof.
+  unfold sem_bblock_par, PChk.prun. constructor 1.
+  - intros (p' & H1 & H2).
+    eexists (comp_bblock p'); intuition eauto.
+  - intros (p' & H1 & H2). 
+    destruct (comp_bblock_Permutation_back _ _ H2 p) as (p0 & H3 & H4); subst; auto.
+    eexists p0; constructor 1; eauto.
+Qed.
+
+Theorem bblock_is_para_correct p:
+  bblock_is_para p = true -> forall s os', (sem_bblock_par p s os' <-> res_equiv os' (sem_bblock p s)).
+Proof.
+  intros H; generalize (PChk.is_parallelizable_correct _ H); clear H.
+  intros H s os'.
+  rewrite bblock_par_iff_prun, H.
+  constructor; eauto.
+Qed.
\ No newline at end of file
diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v
new file mode 100644
index 00000000..3dff22e1
--- /dev/null
+++ b/mppa_k1c/abstractbb/DepTreeTheory.v
@@ -0,0 +1,411 @@
+(** Dependency Trees of Abstract Basic Blocks
+
+with a purely-functional-but-exponential equivalence test.
+
+*)
+
+
+Require Setoid. (* in order to rewrite <-> *)
+Require Export AbstractBasicBlocksDef.
+
+
+Module Type ResourceDictionary.
+
+Declare Module R: ResourceNames.
+
+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 ResourceDictionary.
+
+
+(** * Computations of "bblock" Dependencies and application to the equality test *)
+
+Module DepTree (L: SeqLanguage) (Dict: ResourceDictionary with Module R:=L.LP.R).
+
+Export L.
+Export LP.
+Local Open Scope list.
+
+
+(** 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)
+  | Terase (new old:tree) (* assignment in the resource: [new] replaces [old] *)
+with list_tree :=
+  | Tnil: list_tree
+  | Tcons (t:tree) (l:list_tree):  list_tree
+  .
+
+
+Fixpoint tree_eval (t: tree) (m: mem): option value :=
+  match t with
+  | Tname x => Some (m x)
+  | Top o l =>
+     match list_tree_eval l m with
+     | Some v => op_eval o v
+     | _ => None
+     end
+  | Terase new old =>
+     (* NB: we simply check whether the old computations has aborted *)
+     match tree_eval old m with
+     | Some _ => tree_eval new m
+     | _ => None
+     end
+  end
+with list_tree_eval (l: list_tree) (m: mem) {struct l}: option (list value) :=
+  match l with
+  | Tnil => Some nil
+  | Tcons t l' => 
+    match (tree_eval t m), (list_tree_eval l' m) with
+    | Some v, Some lv => Some (v::lv)
+    | _, _ => None
+    end
+  end.
+
+Definition deps:= Dict.t tree.
+
+Definition deps_get (d:deps) x := 
+   match Dict.get d x with 
+   | None => Tname x
+   | Some t => t
+   end.
+
+Lemma set_spec_eq d x t:
+  deps_get (Dict.set d x t) x = t.
+Proof.
+  unfold deps_get; rewrite Dict.set_spec_eq; simpl; auto.
+Qed.
+
+Lemma set_spec_diff d x y t:
+  x <> y -> deps_get (Dict.set d x t) y = deps_get d y.
+Proof.
+ unfold deps_get; intros; rewrite Dict.set_spec_diff; simpl; auto.
+Qed.
+
+Lemma empty_spec x: deps_get Dict.empty x = Tname x.
+Proof.
+ unfold deps_get; rewrite Dict.empty_spec; simpl; auto.
+Qed.
+
+Hint Rewrite set_spec_eq empty_spec: dict_rw. 
+
+Fixpoint exp_tree (e: exp) (d old: deps): tree :=
+  match e with
+  | Name x => deps_get d x
+  | Op o le => Top o (list_exp_tree le d old)
+  | Old e => exp_tree e old old
+  end
+with list_exp_tree (le: list_exp) (d old: deps): list_tree :=
+  match le with
+  | Enil => Tnil
+  | Econs e le' => Tcons (exp_tree e d old) (list_exp_tree le' d old)
+  | LOld le => list_exp_tree le old old
+  end.
+
+Definition failsafe (t: tree): bool :=
+  match t with
+  | Tname x => true
+  | Top o Tnil => 
+     match op_eval o nil with
+     | Some _ => true
+     | None => false
+     end
+  | _ => false
+  end.
+
+Lemma failsafe_correct (t: tree) m: failsafe t = true -> tree_eval t m <> None.
+Proof.
+  destruct t; simpl; try congruence.
+  destruct l; simpl; try congruence.
+  destruct (op_eval o nil); try congruence.
+Qed.
+
+Fixpoint macro_deps (i: macro) (d old: deps): deps :=
+  match i with
+  | nil => d
+  | (x, e)::i' =>
+     let t0:=deps_get d x in
+     let t1:=exp_tree e d old in
+     let v':=if failsafe t0 then t1 else (Terase t1 t0) in
+     macro_deps i' (Dict.set d x v') old
+  end.
+
+Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps :=
+  match p with
+  | nil => d
+  | i::p' =>
+     let d':=macro_deps i d d in
+     bblock_deps_rec p' d'
+  end.
+
+Definition bblock_deps: bblock -> deps
+ := fun p => bblock_deps_rec p Dict.empty.
+
+(** Main Result: the [bblock_deps_equiv] theorem states that bblocks with the same dependencies are observationaly equals *)
+
+
+Lemma tree_eval_exp e od m0 old:
+  (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
+  forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
+   (tree_eval (exp_tree e d od) m0) = exp_eval e m1 old.
+Proof.
+  intro H.
+  induction e using exp_mut with (P0:=fun l => forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval (list_exp_tree l d od) m0 = list_exp_eval l m1 old); simpl; auto.
+  - intros; erewrite IHe; eauto.
+  - intros; erewrite IHe, IHe0; eauto. 
+Qed.
+
+Lemma tree_eval_macro_abort i m0 x old: forall d,
+    tree_eval (deps_get d x) m0 = None ->
+    tree_eval (deps_get (macro_deps i d old) x) m0 = None.
+Proof.
+  induction i as [|[y e] i IHi]; simpl; auto.
+  intros d H; erewrite IHi; eauto. clear IHi.
+  destruct (R.eq_dec x y).
+  * subst; autorewrite with dict_rw.
+    generalize (failsafe_correct (deps_get d y) m0).
+    destruct (failsafe (deps_get d y)); simpl; intuition try congruence.
+    rewrite H; simpl. auto.
+  * rewrite! set_spec_diff; auto.
+Qed.
+
+Lemma tree_eval_abort p m0 x: forall d,
+    tree_eval (deps_get d x) m0 = None ->
+    tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None.
+Proof.
+  induction p; simpl; auto.
+  intros d H; erewrite IHp; eauto. clear IHp.
+  eapply tree_eval_macro_abort; eauto.
+Qed.
+
+Lemma tree_eval_macro_Some_correct1 i m0 old od: 
+  (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
+  forall (m1 m2: mem) d, 
+  macro_run i m1 old = Some m2 -> 
+  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
+  (forall x, tree_eval (deps_get (macro_deps i d od) x) m0 = Some (m2 x)).
+Proof.
+  intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H.
+  - inversion_clear H; eauto.
+  - intros H0 x0.
+    remember (exp_eval e m1 old) as ov.
+    destruct ov.
+    + refine (IHi _ _ _ _ _ _); eauto.
+      clear x0; intros x0.
+      unfold assign; destruct (R.eq_dec x x0).
+      * subst; autorewrite with dict_rw.
+        destruct (failsafe (deps_get d x0)); simpl; try rewrite H0;
+        erewrite tree_eval_exp; eauto.
+      * rewrite set_spec_diff; auto.
+    + inversion H. 
+Qed.
+
+Local Hint Resolve tree_eval_macro_Some_correct1 tree_eval_abort.
+
+Lemma tree_eval_Some_correct1 p m0: forall (m1 m2: mem) d, 
+ run p m1 = Some m2 -> 
+  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
+    (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)).
+Proof.
+  induction p as [ | i p]; simpl; intros m1 m2 d H.
+  - inversion_clear H; eauto.
+  - intros H0 x0.
+    remember (macro_run i m1 m1) as om.
+    destruct om.
+    + refine (IHp _ _ _ _ _ _); eauto.
+    + inversion H. 
+Qed.
+
+Lemma bblock_deps_Some_correct1 p m0 m1:
+  run p m0 = Some m1
+   -> forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x).
+Proof.
+  intros; eapply tree_eval_Some_correct1;
+  intros; autorewrite with dict_rw; simpl; eauto.
+Qed.
+
+Lemma tree_eval_macro_None_correct i m0 old od: 
+  (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
+  forall m1 d,  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
+  macro_run i m1 old = None <-> exists x, tree_eval (deps_get (macro_deps i d od) x) m0 = None.
+Proof.
+  intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d.
+  - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate].
+  - intros H0.
+    remember (exp_eval e m1 old) as ov.
+    destruct ov.
+    + refine (IHi _ _ _); eauto.
+      intros x0; unfold assign; destruct (R.eq_dec x x0).
+      * subst; autorewrite with dict_rw. 
+        destruct (failsafe (deps_get d x0)); simpl; try rewrite H0;
+        erewrite tree_eval_exp; eauto.
+      * rewrite set_spec_diff; auto.
+    + intuition.
+      constructor 1 with (x:=x); simpl.
+      apply tree_eval_macro_abort.
+      autorewrite with dict_rw.
+      destruct (failsafe (deps_get d x)); simpl; try rewrite H0;
+      erewrite tree_eval_exp; eauto.
+Qed.
+
+
+Lemma tree_eval_None_correct p m0: forall m1 d,
+  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
+  run p m1 = None <-> exists x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None.
+Proof.
+  induction p as [|i p IHp]; simpl; intros m1 d.
+  - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate].
+  - intros H0.
+    remember (macro_run i m1 m1) as om.
+    destruct om.
+    + refine (IHp _ _ _); eauto.
+    + intuition.
+      assert (X: macro_run i m1 m1 = None); auto.
+      rewrite tree_eval_macro_None_correct in X; auto.
+      destruct X as [x H1].
+      constructor 1 with (x:=x); simpl; auto.
+Qed.
+
+Lemma bblock_deps_None_correct p m:
+  run p m = None <-> exists x, tree_eval (deps_get (bblock_deps p) x) m = None.
+Proof.
+  intros; eapply tree_eval_None_correct.
+  intros; autorewrite with dict_rw; simpl; eauto.
+Qed.
+
+Lemma tree_eval_macro_Some_correct2 i m0 old od: 
+  (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
+  forall (m1 m2: mem) d, 
+  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
+    (forall x, tree_eval (deps_get (macro_deps i d od) x) m0 = Some (m2 x)) ->
+    res_eq (Some m2) (macro_run i m1 old).
+Proof.
+  intro X.
+  induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H0.
+  - intros H; eapply ex_intro; intuition eauto.
+    generalize (H0 x); rewrite H.
+    congruence.
+  - intros H.
+    remember (exp_eval e m1 old) as ov.
+    destruct ov.
+    + refine (IHi _ _ _ _ _); eauto.
+      intros x0; unfold assign; destruct (R.eq_dec x x0).
+      * subst; autorewrite with dict_rw.
+        destruct (failsafe (deps_get d x0)); simpl; try rewrite H0;
+        erewrite tree_eval_exp; eauto.
+      * rewrite set_spec_diff; auto.
+    + generalize (H x).
+      rewrite tree_eval_macro_abort; try discriminate.
+      autorewrite with dict_rw. 
+      destruct (failsafe (deps_get d x)); simpl; try rewrite H0;
+      erewrite tree_eval_exp; eauto.
+Qed.
+
+Lemma tree_eval_Some_correct2 p m0: forall (m1 m2: mem) d, 
+  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
+    (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)) ->
+    res_eq (Some m2) (run p m1).
+Proof.
+  induction p as [|i p]; simpl; intros m1 m2 d H0.
+  - intros H; eapply ex_intro; intuition eauto.
+    generalize (H0 x); rewrite H.
+    congruence.
+  - intros H.
+    remember (macro_run i m1 m1) as om.
+    destruct om.
+    + refine (IHp _ _ _ _ _); eauto.
+    + assert (X: macro_run i m1 m1 = None); auto.
+      rewrite tree_eval_macro_None_correct in X; auto.
+      destruct X as [x H1].
+      generalize (H x).
+      rewrite tree_eval_abort; congruence.
+Qed.
+
+Lemma bblock_deps_Some_correct2 p m0 m1:
+  (forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x))
+  -> res_eq (Some m1) (run p m0).
+Proof.
+  intros; eapply tree_eval_Some_correct2; eauto.
+  intros; autorewrite with dict_rw; simpl; eauto.
+Qed.
+
+
+Theorem bblock_deps_equiv p1 p2:
+  (forall x, deps_get (bblock_deps p1) x = deps_get (bblock_deps p2) x)
+   -> bblock_equiv p1 p2.
+Proof.
+  intros H m2.
+  remember (run p1 m2) as om1.
+  destruct om1; simpl.
+  + apply bblock_deps_Some_correct2.
+    intros; rewrite <- H.
+    apply bblock_deps_Some_correct1; auto.
+  + rewrite bblock_deps_None_correct.
+    assert (X: run p1 m2 = None); auto.
+    rewrite bblock_deps_None_correct in X.
+    destruct X as [x Hx].
+    rewrite H in Hx.
+    eauto.
+Qed.
+
+End DepTree.
+
+Require Import PArith.
+Require Import FMapPositive.
+
+Module PosDict <: ResourceDictionary 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
new file mode 100644
index 00000000..65f12b8e
--- /dev/null
+++ b/mppa_k1c/abstractbb/ImpDep.v
@@ -0,0 +1,847 @@
+(** 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 ResourceDictionary.
+
+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 hTerase (t1 t2: hashV tree) (debug: option pstring): ?? hashV tree :=
+   DO hc <~ hash 3;; 
+   hC_tree {| pre_data:=Terase (data t1) (data t2); 
+              hcodes:=[hc;hid t1; hid t2]; debug_info := debug |}.
+
+Lemma hTerase_correct t1 t2 dbg: 
+  WHEN hTerase t1 t2 dbg ~> t THEN (data t)=(Terase (data t1) (data t2)).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hTerase.
+Hint Resolve hTerase_correct: wlp.
+
+Definition hTnil (_: unit): ?? hashV list_tree :=
+   hC_list_tree {| pre_data:=Tnil; hcodes := nil; debug_info := None |} .
+
+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 ! *)
+
+
+Definition hdeps:= Dict.t (hashV tree).
+
+(* pseudo deps_get *)
+Definition pdeps_get (d:hdeps) 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.
+
+Fixpoint hexp_tree (e: exp) (d od: hdeps) (dbg: option pstring) : ?? hashV tree :=
+  match e with
+  | Name 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 e od1 od2:
+  (forall x, pdeps_get od1 x = deps_get od2 x) ->
+ forall d1 d2 dbg,
+  (forall x, pdeps_get d1 x = deps_get d2 x) ->
+  WHEN hexp_tree e d1 od1 dbg ~> t THEN data t = exp_tree e d2 od2.
+Proof.
+  intro H.
+  induction e using exp_mut with (P0:=fun le =>  forall d1 d2,
+     (forall x, pdeps_get d1 x = deps_get d2 x) ->
+     WHEN hlist_exp_tree le d1 od1 ~> lt THEN data lt = list_exp_tree le d2 od2); simpl; wlp_simplify; congruence.
+Qed.
+Global Opaque hexp_tree.
+
+Lemma hexp_tree_correct e d1 od1 dbg:
+  WHEN hexp_tree e d1 od1 dbg ~> t THEN forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) -> (forall x, pdeps_get d1 x = deps_get d2 x) -> data t = exp_tree e d2 od2.
+Proof.
+  intros t H od2 d2 H1 H2; apply (hexp_tree_correct_x e od1 od2 H1 d1 d2 dbg H2 t H). 
+Qed.
+Hint Resolve hexp_tree_correct: wlp.
+
+Variable debug_assign: R.t -> ?? option pstring.
+
+Fixpoint hmacro_deps (i: macro) (d od: hdeps): ?? hdeps :=
+  match i with
+  | nil => RET d
+  | (x, e)::i' =>
+     DO dbg <~ debug_assign x;;
+     DO t0 <~ hdeps_get d x None;;
+     DO v' <~ (if failsafe (data t0) 
+      then 
+        hexp_tree e d od dbg 
+      else
+        DO t1 <~ hexp_tree e d od None;; 
+        hTerase t1 t0 dbg);;
+     hmacro_deps i' (Dict.set d x v') od
+  end.
+
+Lemma pset_spec_eq d x t:
+  pdeps_get (Dict.set d x t) x = (data t).
+Proof.
+  unfold pdeps_get; rewrite Dict.set_spec_eq; simpl; auto.
+Qed.
+
+Lemma pset_spec_diff d x y t:
+  x <> y -> pdeps_get (Dict.set d x t) y = pdeps_get d y.
+Proof.
+ unfold pdeps_get; intros; rewrite Dict.set_spec_diff; simpl; auto.
+Qed.
+
+Lemma pempty_spec x: pdeps_get Dict.empty x = Tname x.
+Proof.
+ unfold pdeps_get; rewrite Dict.empty_spec; simpl; auto.
+Qed.
+
+Hint Rewrite pset_spec_eq pempty_spec: dict_rw.
+
+
+Lemma hmacro_deps_correct i: forall d1 od1,
+  WHEN hmacro_deps i d1 od1 ~> d1' THEN
+    forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) ->
+    (forall x, pdeps_get d1 x = deps_get d2 x) -> 
+    forall x, pdeps_get d1' x = deps_get (macro_deps i d2 od2) x.
+Proof.
+  induction i; simpl; wlp_simplify.
+  + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). 
+    - erewrite H0, H2; simpl; eauto. clear exta2 Hexta2 H2; auto.
+      intros x0; destruct (R.eq_dec a0 x0).
+      * subst; autorewrite with dict_rw. erewrite H1; eauto.
+      * rewrite set_spec_diff, pset_spec_diff; auto.
+    - rewrite H, H4; auto.
+  + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)).
+    - erewrite H0, H3; simpl; eauto. clear exta3 Hexta3 H3; auto.
+      intros x0; destruct (R.eq_dec a0 x0).
+      * subst; autorewrite with dict_rw. rewrite H2.
+        erewrite H, H1; eauto. congruence.
+      * rewrite set_spec_diff, pset_spec_diff; auto.
+   - rewrite H, H5; auto.
+Qed.
+Global Opaque hmacro_deps.
+Hint Resolve hmacro_deps_correct: wlp.
+
+(* logging info: we log the number of macro-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' <~ hmacro_deps i d d;;
+     hbblock_deps_rec p' d'
+  end.
+
+Lemma hbblock_deps_rec_correct p: forall d1,
+  WHEN hbblock_deps_rec p d1 ~> d1' THEN
+    forall d2, (forall x, pdeps_get d1 x = deps_get d2 x) -> forall x, pdeps_get d1' x = deps_get (bblock_deps_rec p d2) x.
+Proof.
+  induction p; simpl; wlp_simplify.
+Qed.
+Global Opaque hbblock_deps_rec.
+Hint Resolve hbblock_deps_rec_correct: wlp.
+
+
+Definition hbblock_deps: bblock -> ?? hdeps
+ := fun p => hbblock_deps_rec p Dict.empty.
+
+Lemma hbblock_deps_correct p:
+  WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps p) x.
+Proof.
+  unfold bblock_deps; wlp_simplify. erewrite H; eauto.
+  intros; autorewrite with dict_rw; auto.
+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
+  | Terase t1a t2a, Terase t1b t2b =>
+      DO b <~ phys_eq t1a t1b ;;
+      if b 
+      then phys_eq t2a t2b
+      else RET false
+  | _,_ => RET false
+  end.
+
+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:
+  (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.
+
+
+(*** A GENERIC EQ_TEST: IN ORDER TO SUPPORT SEVERAL DEBUGGING MODE !!! ***)
+
+Section Prog_Eq_Gen.
+
+Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 macros *)
+Variable dbg2: R.t -> ?? option pstring. (* log of p2 macros *)
+Variable log1: unit -> ?? unit. (* log of p1 macros *)
+Variable log2: unit -> ?? unit. (* log of p2 macros *)
+
+
+
+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.
+
+Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool :=
+  DO r <~ (TRY 
+    DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;;
+    DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;;
+    DO b <~ Dict.eq_test d1 d2 ;;
+    if b then RET true
+    else (
+      print_error_end d1 d2 ;;
+      RET false
+    )
+  CATCH_FAIL s, _ => 
+    print_error s;;
+    RET false
+  ENSURE (fun b => b=true -> bblock_equiv p1 p2));;
+  RET (`r).
+Obligation 1.
+  destruct hco_tree_correct as [X1 X2], hco_list_correct as [Y1 Y2].
+  constructor 1; wlp_simplify; try congruence.
+  apply bblock_deps_equiv; auto.
+  intros; rewrite <- H, <- H0.
+  apply pdeps_get_intro. auto.
+Qed.
+
+Theorem g_bblock_eq_test_correct p1 p2:
+  WHEN g_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2.
+Proof.
+  wlp_simplify.
+  destruct exta; simpl in * |- *; auto.
+Qed.
+Global Opaque g_bblock_eq_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_eq_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 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). 
+
+
+Program Definition bblock_eq_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_eq_test no_dbg no_dbg skip (log_insert log) hco_tree _ hco_list _ print_error_end (print_error log) 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_eq_test_correct.
+
+Theorem bblock_eq_test_correct p1 p2:
+  WHEN bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque bblock_eq_test.
+
+
+
+(** This is only to print info on each bblock_eq_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))
+  | (Terase _ _), [ _ ; t1; t2 ] =>
+    DO st1 <~ string_of_hashcode t1 ;;
+    DO st2 <~ string_of_hashcode t2 ;;
+    println((tree_id st1) +; " erases " +; (tree_id st2))
+  | _, _ => FAILWITH "unexpected hcodes"
+  end.
+
+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 +; ")")
+    | Terase t _, [ _ ; tid; _ ] =>
+      DO pt <~ get_htree tid ;;
+      string_of_tree t pt
+    | _, _ => 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
+  | _ => FAILWITH "No witness info"
+  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_eq_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_eq_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) 
+     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_eq_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) 
+       p2 p1;;
+    if result2 
+    then (
+      println (msg_prefix +; " OOops - symmetry violation in bblock_eq_test  => this is a bug of bblock_eq_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_eq_test_correct p1 p2:
+  WHEN verb_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque verb_bblock_eq_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.
+
+(* 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. 
+
+
+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/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v
new file mode 100644
index 00000000..55931e0f
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ImpConfig.v
@@ -0,0 +1,82 @@
+(** Impure Config for UNTRUSTED backend !!! *)
+
+Require Import ImpMonads.
+Require Extraction.
+(** Pure computations (used for extraction !) 
+
+We keep module [Impure] opaque in order to check that Coq proof do not depend on 
+the implementation of [Impure].
+
+*)
+
+Module Type ImpureView.
+
+ Include MayReturnMonad.
+
+(* WARNING: THIS IS REALLY UNSAFE TO DECOMMENT THE "UnsafeImpure" module !
+
+   unsafe_coerce coerces an impure computation into a pure one !
+
+*)
+
+(*
+ Module UnsafeImpure.
+
+ Parameter unsafe_coerce: forall {A}, t A -> A.
+
+ Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=x -> mayRet k x. 
+
+ End UnsafeImpure.
+*)
+
+End ImpureView.
+
+
+Module Impure: ImpureView.
+
+  Include IdentityMonad.
+
+  Module UnsafeImpure.
+
+  Definition unsafe_coerce {A} (x:t A) := x.
+
+  Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=x -> mayRet k x.
+  Proof.
+    unfold unsafe_coerce, mayRet; auto.
+  Qed.
+
+  End UnsafeImpure.
+
+End Impure.
+
+
+(** Comment the above code and decomment this to test that coq proofs still work with an impure monad !
+
+- this should fail only on extraction or if unsafe_coerce is used !
+
+*)
+(*
+Module Impure: MayReturnMonad := PowerSetMonad.
+*)
+
+Export Impure.
+
+Extraction Inline ret mk_annot.
+
+
+(* WARNING. The following directive is unsound.
+
+  Extraction Inline bind
+
+For example, it may lead to extract the following code as "true" (instead of an error raising code)
+  failwith "foo";;true
+
+*)
+
+Extract Inlined Constant bind => "(|>)".
+
+
+Extract Constant t "" => "". (* This weird directive extracts [t] as "'a" instead of "'a t" *)
+Extraction Inline t.
+
+Global Opaque t.
\ No newline at end of file
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v
new file mode 100644
index 00000000..6eb0c5af
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ImpCore.v
@@ -0,0 +1,187 @@
+(** Impure monad for interface with impure code
+
+*)
+
+Require Export Program.
+Require Export ImpConfig.
+
+(* Theory: bind + embed => dbind 
+
+Program Definition dbind {A B} (k1: t A) (k2: forall (a:A), (mayRet k1 a) -> t B) : t B
+  := bind (mk_annot k1) (fun a => k2 a _).
+
+Lemma mayRet_dbind: forall (A B:Type) k1 k2 (b:B),
+     mayRet (dbind k1 k2) b -> exists a:A, exists H: (mayRet k1 a), mayRet (k2 a H) b.
+Proof.
+  intros A B k1 k2 b H; decompose [ex and] (mayRet_bind _ _ _ _ _ H).
+  eapply ex_intro.
+  eapply ex_intro.
+  eauto.
+Qed.
+
+*)
+
+Definition wlp {A:Type} (k: t A) (P: A -> Prop): Prop
+  := forall a, mayRet k a -> P a.
+
+(* Notations *)
+
+(* Print Grammar constr. *)
+
+Module Notations.
+
+  Bind Scope impure_scope with t.
+  Delimit Scope impure_scope with impure.
+
+  Notation "?? A" := (t A) (at level 0, A at level 95): impure_scope.
+
+  Notation "k '~~>' a" := (mayRet k a) (at level 75, no associativity): impure_scope. 
+
+  Notation "'RET' a" := (ret a) (at level 0): impure_scope.
+
+  Notation "'DO' x '<~' k1 ';;' k2" := (bind k1 (fun x => k2))
+    (at level 55, k1 at level 53, x at level 99, right associativity): impure_scope.
+
+  Notation "k1 ';;'  k2" := (bind k1 (fun _ => k2))
+    (at level 55, right associativity): impure_scope.
+
+  Notation "'WHEN' k '~>' a 'THEN' R" := (wlp k (fun a => R))
+    (at level 73, R at level 100, right associativity): impure_scope.
+
+  Notation "'ASSERT' P" := (ret (A:=P) _) (at level 0, only parsing): impure_scope.
+
+End Notations.
+
+Import Notations.
+Local Open Scope impure.
+
+Goal ((?? list nat * ??nat -> nat) = ((?? ((list nat) * ?? nat) -> nat)))%type.
+Proof.
+  apply refl_equal.
+Qed.
+
+
+(* wlp lemmas for tactics *)
+
+Lemma wlp_unfold A (k:??A)(P: A -> Prop):
+   (forall a, k ~~> a -> P a)
+    -> wlp k P.
+Proof.
+  auto.
+Qed.
+
+Lemma wlp_monotone A (k:?? A) (P1 P2: A -> Prop):
+    wlp k P1
+    -> (forall a, k ~~> a -> P1 a -> P2 a)
+    -> wlp k P2.
+Proof.
+  unfold wlp; eauto.
+Qed.
+
+Lemma wlp_forall A B (k:?? A) (P: B -> A -> Prop):
+   (forall x, wlp k (P x))
+    -> wlp k (fun a => forall x, P x a).
+Proof.
+  unfold wlp; auto.
+Qed.
+
+Lemma wlp_ret A (P: A -> Prop) a:
+   P a -> wlp (ret a) P.
+Proof.
+    unfold wlp.
+    intros H b H0.
+    rewrite <- (mayRet_ret _ a b H0).
+    auto.
+Qed.
+
+Lemma wlp_bind A B (k1:??A) (k2: A -> ??B) (P: B -> Prop):
+  wlp k1 (fun a => wlp (k2 a) P) -> wlp (bind k1 k2) P.
+Proof.
+    unfold wlp.
+    intros H a H0.
+    case (mayRet_bind _ _ _ _ _ H0); clear H0.
+    intuition eauto.
+Qed.
+
+Lemma wlp_ifbool A (cond: bool) (k1 k2: ?? A) (P: A -> Prop):
+ (cond=true -> wlp k1 P) -> (cond=false -> wlp k2 P) -> wlp (if cond then k1 else k2) P.
+Proof.
+  destruct cond; auto.
+Qed.
+
+Lemma wlp_letprod (A B C: Type) (p: A*B) (k: A -> B -> ??C) (P: C -> Prop):
+  (wlp (k (fst p) (snd p)) P)
+    -> (wlp (let (x,y):=p in (k x y)) P).
+Proof.
+  destruct p; simpl; auto.
+Qed.
+
+Lemma wlp_sum (A B C: Type) (x: A+B) (k1: A -> ??C) (k2: B -> ??C)  (P: C -> Prop):
+  (forall a, x=inl a -> wlp (k1 a) P) -> 
+  (forall b, x=inr b -> wlp (k2 b) P) -> 
+     (wlp (match x with inl a => k1 a | inr b => k2 b end) P).
+Proof.
+  destruct x; simpl; auto.
+Qed.
+
+Lemma wlp_sumbool (A B:Prop) (C: Type) (x: {A}+{B}) (k1: A -> ??C) (k2: B -> ??C)  (P: C -> Prop):
+  (forall a, x=left a -> wlp (k1 a) P) -> 
+  (forall b, x=right b -> wlp (k2 b) P) -> 
+     (wlp (match x with left a => k1 a | right b => k2 b end) P).
+Proof.
+  destruct x; simpl; auto.
+Qed.
+
+(* Tactics 
+
+MAIN tactics:  
+  - xtsimplify "base": simplification using from hints in "base" database (in particular "wlp" lemmas).
+  - xtstep "base": only one step of simplification.
+
+For good performance, it is recommanded to have several databases.
+
+*)
+
+Ltac introcomp :=
+  let a:= fresh "exta" in
+  let H:= fresh "Hexta" in
+  intros a H.
+
+(* decompose the current wlp goal using "introduction" rules *)
+Ltac wlp_decompose :=
+    apply wlp_ret
+ || apply wlp_bind
+ || apply wlp_ifbool
+ || apply wlp_letprod
+ || apply wlp_sum
+ || apply wlp_sumbool
+ .
+
+(* this tactic simplifies the current "wlp" goal using any hint found via tactic "hint". *) 
+Ltac apply_wlp_hint hint :=
+    eapply wlp_monotone;
+      [ hint; fail | idtac ] ;
+      simpl; introcomp.
+
+(* one step of wlp_xsimplify 
+*)
+Ltac wlp_step hint :=
+    match goal with
+      | |- (wlp _ _) => 
+        wlp_decompose
+        || apply_wlp_hint hint
+        || (apply wlp_unfold; introcomp)
+    end.
+
+(* main general tactic 
+WARNING: for the good behavior of "wlp_xsimplify", "hint" must at least perform a "eauto".
+
+Example of use:
+  wlp_xsimplify (intuition eauto with base).
+*)
+Ltac wlp_xsimplify hint := 
+    repeat (intros; subst; wlp_step hint; simpl; (tauto || hint)).
+
+Create HintDb wlp discriminated.
+
+Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file
diff --git a/mppa_k1c/abstractbb/Impure/ImpExtern.v b/mppa_k1c/abstractbb/Impure/ImpExtern.v
new file mode 100644
index 00000000..8fb3cf3b
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ImpExtern.v
@@ -0,0 +1,7 @@
+(** Exporting Extern functions
+*)
+
+Require Export ImpPrelude.
+Require Export ImpIO.
+Require Export ImpLoops.
+Require Export ImpHCons.
diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v
new file mode 100644
index 00000000..307eb163
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v
@@ -0,0 +1,48 @@
+Require Export ImpIO.
+
+Import Notations.
+Local Open Scope impure.
+
+(********************************)
+(* (Weak) HConsing              *)
+
+Axiom string_of_hashcode: hashcode -> ?? caml_string.
+Extract Constant string_of_hashcode => "string_of_int".
+
+Axiom hash: forall {A}, A -> ?? hashcode.
+Extract Constant hash => "Hashtbl.hash".
+
+Axiom xhCons: forall {A}, ((A -> A -> ?? bool) * (pre_hashV A -> ?? hashV A)) -> ?? hashConsing A.
+Extract Constant xhCons => "ImpHConsOracles.xhCons".
+
+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) ;;
+  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;
+      |}.
+
+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')).
+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')).
diff --git a/mppa_k1c/abstractbb/Impure/ImpIO.v b/mppa_k1c/abstractbb/Impure/ImpIO.v
new file mode 100644
index 00000000..6c02c395
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ImpIO.v
@@ -0,0 +1,159 @@
+(** Extension of Coq language with some IO and exception-handling operators.
+
+TODO: integration with http://coq.io/ ?
+
+*)
+
+Require Export ImpPrelude.
+
+Import Notations.
+Local Open Scope impure.
+
+(** Printing functions *)
+
+Axiom print: pstring -> ?? unit.
+Extract Constant print => "ImpIOOracles.print".
+
+Axiom println: pstring -> ?? unit.
+Extract Constant println => "ImpIOOracles.println".
+
+Axiom read_line: unit -> ?? pstring.
+Extract Constant read_line => "ImpIOOracles.read_line".
+
+Require Import ZArith.
+Axiom string_of_Z: Z -> ?? pstring.
+Extract Constant string_of_Z => "ImpIOOracles.string_of_Z".
+
+(** timer *)
+
+Axiom timer: forall {A B}, (A -> ?? B)*A -> ?? B.
+Extract Constant timer => "ImpIOOracles.timer".
+
+(** Exception Handling *)
+
+Axiom exit_observer: Type.
+Extract Constant exit_observer => "((unit -> unit) ref)".
+
+Axiom new_exit_observer: (unit -> ??unit) -> ??exit_observer.
+Extract Constant new_exit_observer => "ImpIOOracles.new_exit_observer".
+
+Axiom set_exit_observer: exit_observer * (unit -> ??unit) -> ??unit.
+Extract Constant set_exit_observer => "ImpIOOracles.set_exit_observer".
+
+Axiom exn: Type.
+Extract Inlined Constant exn => "exn".
+
+Axiom raise: forall {A}, exn -> ?? A.
+Extract Constant raise => "raise".
+
+Axiom exn2string: exn -> ?? pstring.
+Extract Constant exn2string => "ImpIOOracles.exn2string".
+
+Axiom fail: forall {A}, pstring -> ?? A.
+Extract Constant fail => "ImpIOOracles.fail".
+
+Axiom try_with_fail: forall {A}, (unit -> ?? A) * (pstring -> exn -> ??A) -> ??A.
+Extract Constant try_with_fail => "ImpIOOracles.try_with_fail".
+
+Axiom try_with_any: forall {A}, (unit -> ?? A) * (exn -> ??A) -> ??A.
+Extract Constant try_with_any => "ImpIOOracles.try_with_any".
+
+Notation "'RAISE' e" := (DO r <~ raise (A:=False) e ;; RET (match r with end)) (at level 0): impure_scope.
+Notation "'FAILWITH' msg" := (DO r <~ fail (A:=False) msg ;; RET (match r with end)) (at level 0): impure_scope.
+
+Definition _FAILWITH {A:Type} msg: ?? A := FAILWITH msg.
+
+Example _FAILWITH_correct A msg (P: A -> Prop):
+  WHEN _FAILWITH msg ~> r THEN P r.
+Proof.
+  wlp_simplify.
+Qed.
+
+Notation "'TRY' k1 'WITH_FAIL' s ',' e '=>' k2" := (try_with_fail (fun _ => k1, fun s e => k2))
+    (at level 55, k1 at level 53, right associativity): impure_scope.
+
+Notation "'TRY' k1 'WITH_ANY' e '=>' k2" := (try_with_any (fun _ => k1, fun e => k2))
+    (at level 55, k1 at level 53, right associativity): impure_scope.
+
+
+Program Definition assert_b (b: bool) (msg: pstring): ?? b=true :=
+  match b with
+  | true => RET _
+  | false => FAILWITH msg
+  end.
+
+Lemma assert_wlp_true msg b: WHEN assert_b b msg ~> _ THEN b=true.
+Proof.
+  wlp_simplify.
+Qed.
+
+Lemma assert_false_wlp msg (P: Prop): WHEN assert_b false msg ~> _ THEN P.
+Proof.
+  simpl; wlp_simplify.
+Qed.
+
+Program Definition try_catch_fail_ensure {A} (k1: unit -> ?? A) (k2: pstring -> exn -> ??A) (P: A -> Prop | wlp (k1 tt) P /\ (forall s e, wlp (k2 s e) P)): ?? { r | P r }
+  := TRY
+        DO r <~ mk_annot (k1 tt);; 
+        RET (exist P r _)
+     WITH_FAIL s, e => 
+        DO r <~ mk_annot (k2 s e);;
+        RET (exist P r _).
+Obligation 2.
+  unfold wlp in * |- *; eauto.
+Qed.
+
+Notation "'TRY' k1 'CATCH_FAIL' s ',' e '=>' k2 'ENSURE' P" := (try_catch_fail_ensure (fun _ => k1) (fun s e => k2) (exist _ P _))
+    (at level 55, k1 at level 53, right associativity): impure_scope.
+
+Definition is_try_post {A} (P: A -> Prop) k1 k2 : Prop := 
+  wlp (k1 ()) P /\ forall (e:exn), wlp (k2 e) P.
+
+Program Definition try_catch_ensure {A} k1 k2 (P:A->Prop|is_try_post P k1 k2): ?? { r | P r }
+  := TRY
+        DO r <~ mk_annot (k1 ());; 
+        RET (exist P r _)
+     WITH_ANY e => 
+        DO r <~ mk_annot (k2 e);;
+        RET (exist P r _).
+Obligation 1.
+  unfold is_try_post, wlp in * |- *; intuition eauto.
+Qed.
+Obligation 2.
+  unfold is_try_post, wlp in * |- *; intuition eauto.
+Qed.
+
+Notation "'TRY' k1 'CATCH' e '=>' k2 'ENSURE' P" := (try_catch_ensure (fun _ => k1) (fun e => k2) (exist _ P _))
+    (at level 55, k1 at level 53, right associativity): impure_scope.
+
+
+Program Example tryex {A} (x y:A) := 
+  TRY (RET x)
+  CATCH _ => (RET y)
+  ENSURE (fun r => r = x \/ r = y).
+Obligation 1.
+  split; wlp_simplify.
+Qed.
+
+Program Example tryex_test {A} (x y:A): 
+  WHEN tryex x y ~> r THEN `r <> x -> `r = y.
+Proof.
+  wlp_simplify. destruct exta as [r [X|X]]; intuition.
+Qed.
+
+
+Program Example try_branch1 {A} (x:A): ?? { r | r = x} := 
+  TRY (RET x)
+  CATCH e => (FAILWITH "!")
+  ENSURE _.
+Obligation 1.
+  split; wlp_simplify.
+Qed.
+
+Program Example try_branch2 {A} (x:A): ?? { r | r = x} := 
+  TRY (FAILWITH "!")
+  CATCH e => (RET x)
+  ENSURE _.
+Obligation 1.
+  split; wlp_simplify.
+Qed.
diff --git a/mppa_k1c/abstractbb/Impure/ImpLoops.v b/mppa_k1c/abstractbb/Impure/ImpLoops.v
new file mode 100644
index 00000000..9e11195e
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ImpLoops.v
@@ -0,0 +1,121 @@
+(** Extension of Coq language with generic loops. *)
+
+Require Export ImpIO.
+
+Import Notations.
+Local Open Scope impure.
+
+
+(** While-loop iterations *)
+
+Axiom loop: forall {A B}, A * (A -> ?? (A+B)) -> ?? B.
+Extract Constant loop => "ImpLoopOracles.loop".
+
+(** A while loop *)
+
+Record while_loop_invariant {S} (cond: S -> bool) (body: S -> ?? S) (s0: S) (I: S -> Prop): Prop :=
+  { while_init: I s0;
+    while_preserv s: I s -> cond s = true -> WHEN (body s) ~> s' THEN I s'
+  }.
+Arguments while_init [S cond body s0 I].
+Arguments while_preserv [S cond body s0 I].
+
+Program Definition while {S} cond body s0 (I: S -> Prop | while_loop_invariant cond body s0 I): ?? {s | I s /\ cond s = false}
+  := loop (A:={s | I s})
+       (s0, 
+          fun s =>
+          match (cond s) with
+          | true => 
+             DO s' <~ mk_annot (body s) ;; 
+             RET (inl (A:={s | I s }) s')
+          | false => 
+             RET (inr (B:={s | I s /\ cond s = false}) s)
+          end).
+Obligation 1.
+  destruct H; auto.
+Qed.
+Obligation 2.
+  eapply (while_preserv H1); eauto.
+Qed.
+Extraction Inline while.
+
+(** A loop until None (useful to demonstrate a UNSAT property) *)
+
+Program Definition loop_until_None {S} (I: S -> Prop) (body: S -> ?? (option S)) 
+  (H:forall s, I s -> WHEN (body s) ~> s' THEN match s' with Some s1 => I s1 | None => False end) (s0:S): ?? ~(I s0)
+  := loop (A:={s | I s0 -> I s})
+       (s0, 
+          fun s =>
+          DO s' <~ mk_annot (body s) ;;
+          match s' with
+          | Some s1 => RET (inl (A:={s | I s0 -> I s }) s1)
+          | None => RET (inr (B:=~(I s0)) _)
+          end).
+Obligation 2.
+  refine (H s _ _ H1). auto.
+Qed.
+Obligation 3.
+  intros X; refine (H s _ _ H0). auto.
+Qed.
+Extraction Inline loop_until_None.
+
+
+(*********************************************)
+(* A generic fixpoint from an equality test  *)
+
+Record answ {A B: Type} {R: A -> B -> Prop} := {
+  input: A ;
+  output: B ;
+  correct: R input output
+}.
+Arguments answ {A B}.
+
+Definition msg: pstring := "wapply fails".
+
+Definition beq_correct {A} (beq: A -> A -> ?? bool) :=
+  forall x y, WHEN beq x y ~> b THEN b=true -> x=y.
+
+Definition wapply {A B} {R: A -> B -> Prop} (beq: A -> A -> ?? bool) (k: A -> ?? answ R) (x:A): ?? B :=
+  DO a <~ k x;;
+  DO b <~ beq x (input 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):
+ beq_correct beq
+ -> WHEN wapply beq k x ~> y THEN R x y.
+Proof.
+  unfold beq_correct; wlp_simplify.
+  destruct exta; simpl; auto.
+Qed.
+Local Hint Resolve wapply_correct: wlp.
+Global Opaque wapply.
+
+Axiom xrec_set_option: recMode -> ?? unit.
+Extract Constant xrec_set_option => "ImpLoopOracles.xrec_set_option".
+
+(* TODO: generalizaton to get beq (and a Hash function ?) in parameters ? *)
+Axiom xrec: forall {A B}, ((A -> ?? B) -> A -> ?? B) -> ?? (A -> ?? B).
+Extract Constant xrec => "ImpLoopOracles.xrec".
+
+Definition rec_preserv {A B} (recF: (A -> ?? B) -> A -> ?? B) (R: A -> B -> Prop) :=
+  forall f x, WHEN recF f x ~> z THEN (forall x', WHEN f x' ~> y THEN R x' y) -> R x z.
+
+
+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 (wapply beq f).
+Obligation 1.
+  eapply H1; eauto. clear H H1.
+  wlp_simplify.
+Qed.
+
+Lemma rec_correct A B beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq): 
+  WHEN rec beq recF R H1 H2 ~> f THEN forall x, WHEN f x ~> y THEN R x y.
+Proof.
+  wlp_simplify.
+Qed.
+Hint Resolve rec_correct: wlp.
+Global Opaque rec.
diff --git a/mppa_k1c/abstractbb/Impure/ImpMonads.v b/mppa_k1c/abstractbb/Impure/ImpMonads.v
new file mode 100644
index 00000000..f01a2755
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ImpMonads.v
@@ -0,0 +1,148 @@
+(** Impure monad for interface with impure code
+*)
+
+
+Require Import Program.
+
+
+Module Type MayReturnMonad.
+
+  Axiom t: Type -> Type.
+
+  Axiom mayRet: forall {A:Type}, t A -> A -> Prop.
+
+  Axiom ret: forall {A}, A -> t A.
+
+  Axiom bind: forall {A B}, (t A) -> (A -> t B) -> t B.
+
+  Axiom mk_annot: forall {A} (k: t A), t { a: A | mayRet k a }.
+
+  Axiom mayRet_ret: forall A (a b:A), 
+     mayRet (ret a) b -> a=b.
+
+  Axiom mayRet_bind: forall A B k1 k2 (b:B),
+     mayRet (bind k1 k2) b -> exists a:A, mayRet k1 a /\ mayRet (k2 a) b.
+
+End MayReturnMonad.
+
+
+
+(** Model of impure computation as predicate *)
+Module PowerSetMonad<: MayReturnMonad.
+ 
+   Definition t (A:Type) := A -> Prop.
+
+   Definition mayRet {A:Type} (k: t A) a: Prop := k a.
+
+   Definition ret {A:Type} (a:A) := eq a.
+
+   Definition bind {A B:Type} (k1: t A) (k2: A -> t B) := 
+     fun b => exists a, k1 a /\ k2 a b.
+
+   Definition mk_annot {A} (k: t A) : t { a | mayRet k a } := fun _ => True.
+
+   Lemma mayRet_ret A (a b:A): mayRet (ret a) b -> a=b.
+   Proof.
+     unfold mayRet, ret. firstorder.
+   Qed.
+
+   Lemma mayRet_bind A B k1 k2 (b:B):
+         mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b.
+   Proof.
+     unfold mayRet, bind. 
+     firstorder.
+   Qed.
+
+End PowerSetMonad.
+
+
+(** The identity interpretation *)
+Module IdentityMonad<: MayReturnMonad.
+
+   Definition t (A:Type) := A.
+
+   (* may-return semantics of computations *)
+   Definition mayRet {A:Type} (a b:A): Prop := a=b.
+
+   Definition ret {A:Type} (a:A) := a.
+
+   Definition bind {A B:Type} (k1: A) (k2: A -> B) := k2 k1.
+
+   Definition mk_annot {A} (k: t A) : t { a: A | mayRet k a } 
+    := exist _ k (eq_refl k) .
+
+   Lemma mayRet_ret (A:Type) (a b:A): mayRet (ret a) b -> a=b.
+   Proof.
+     intuition.
+   Qed.
+
+   Lemma mayRet_bind (A B:Type) (k1:t A) k2 (b:B):
+         mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b.
+   Proof.
+     firstorder.
+   Qed.
+
+End IdentityMonad.
+
+
+(** Model of impure computation as state-transformers *)
+Module StateMonad<: MayReturnMonad.
+ 
+   Parameter St: Type. (* A global state *)
+
+   Definition t (A:Type) := St -> A * St.
+
+   Definition mayRet {A:Type} (k: t A) a: Prop :=
+     exists s, fst (k s)=a.
+
+   Definition ret {A:Type} (a:A) := fun (s:St) => (a,s).
+
+   Definition bind {A B:Type} (k1: t A) (k2: A -> t B) := 
+     fun s0 => let r := k1 s0 in k2 (fst r) (snd r).
+
+   Program Definition mk_annot {A} (k: t A) : t { a | mayRet k a } := 
+     fun s0 => let r := k s0 in (exist _ (fst r) _, snd r).
+   Obligation 1.
+     unfold mayRet; eauto.
+   Qed.
+
+   Lemma mayRet_ret {A:Type} (a b:A): mayRet (ret a) b -> a=b.
+   Proof.
+     unfold mayRet, ret. firstorder.
+   Qed.
+
+   Lemma mayRet_bind {A B:Type} k1 k2 (b:B):
+         mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b.
+   Proof.
+     unfold mayRet, bind. firstorder eauto.
+   Qed. 
+
+End StateMonad.
+
+(** The deferred interpretation *)
+Module DeferredMonad<: MayReturnMonad.
+
+   Definition t (A:Type) := unit -> A.
+
+   (* may-return semantics of computations *)
+   Definition mayRet {A:Type} (a: t A) (b:A): Prop := a tt=b.
+
+   Definition ret {A:Type} (a:A) : t A := fun _ => a.
+
+   Definition bind {A B:Type} (k1: t A) (k2: A -> t B) : t B := fun _ => k2 (k1 tt) tt.
+
+   Definition mk_annot {A} (k: t A) : t { a: A | mayRet k a } 
+    := fun _ => exist _ (k tt) (eq_refl (k tt)).
+
+   Lemma mayRet_ret (A:Type) (a b: A): mayRet (ret a) b -> a=b.
+   Proof.
+     intuition.
+   Qed.
+
+   Lemma mayRet_bind (A B:Type) (k1:t A) k2 (b:B):
+         mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b.
+   Proof.
+     firstorder.
+   Qed.
+
+End DeferredMonad.
diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v
new file mode 100644
index 00000000..cebc7a72
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v
@@ -0,0 +1,163 @@
+Require Export String.
+Require Export List.
+Require Extraction.
+Require Import Ascii.
+Require Import BinNums.
+Require Export ImpCore.
+
+Axiom caml_string: Type.
+Extract Constant caml_string => "string".
+
+(** New line *)
+Definition nl: string := String (ascii_of_pos 10%positive) EmptyString.
+
+Inductive pstring: Type :=
+  | Str: string -> pstring
+  | CamlStr: caml_string -> pstring
+  | Concat: pstring -> pstring -> pstring.
+
+Coercion Str: string >-> pstring.
+Bind Scope string_scope with pstring.
+
+Notation "x +; y" := (Concat x y)
+    (at level 65, left associativity): string_scope.
+
+(** Coq references *)
+
+Import Notations.
+Local Open Scope impure.
+
+Record cref {A} := {
+  set: A -> ?? unit;
+  get: unit -> ?? A
+}.
+Arguments cref: clear implicits.
+
+Axiom make_cref: forall {A}, A -> ?? cref A.
+Extract Constant make_cref => "(fun x -> let r = ref x in { set = (fun y -> r:=y); get = (fun () -> !r) })".
+
+
+(** Data-structure for a logger *)
+
+Record logger {A:Type} := {
+  log_insert: A -> ?? unit;
+  log_info: unit -> ?? pstring;
+}.
+Arguments logger: clear implicits.
+
+Axiom count_logger: unit -> ?? logger unit.
+Extract Constant count_logger => "(fun () -> let count = ref 0 in { log_insert = (fun () -> count := !count + 1); log_info = (fun () -> (CamlStr (string_of_int !count))) })".
+
+
+(** Axioms of Physical equality  *)
+
+Module Type PhysEq.
+
+Axiom phys_eq: forall {A}, A -> A -> ?? bool.
+
+Axiom phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y.
+
+End PhysEq.
+
+
+
+(* We only check here that above axioms are not trivially inconsistent...
+   (but this does not prove the correctness of the extraction directive below).
+ *)
+Module PhysEqModel: PhysEq.
+
+Definition phys_eq {A} (x y: A) := ret false.
+
+Lemma phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y.
+Proof.
+  wlp_simplify. discriminate.
+Qed.
+
+End PhysEqModel.
+
+
+
+Export PhysEqModel.
+
+Extract Constant phys_eq => "(==)".
+Hint Resolve phys_eq_correct: wlp.
+
+
+
+(** Data-structure for generic hash-consing *)
+
+Axiom hashcode: Type.
+Extract Constant hashcode => "int".
+
+Record pre_hashV {A: Type} := {
+  pre_data: A;
+  hcodes: list hashcode;
+  debug_info: option pstring;
+}.
+Arguments pre_hashV: clear implicits.
+
+Record hashV {A:Type}:= {
+  data: A;
+  hid: hashcode
+}.
+Arguments hashV: clear implicits.
+
+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 *)
+}.
+Arguments hashExport: clear implicits.
+
+Record hashConsing {A:Type}:= {
+  hC: pre_hashV A -> ?? hashV A;
+  hC_known: pre_hashV A -> ?? hashV A; (* fails on unknown inputs *)
+  (**** below: debugging functions ****)
+  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.
+
+(** recMode: this is mainly for Tests ! *)
+Inductive recMode:= StdRec | MemoRec | BareRec | BuggyRec.
+
+
+(* This a copy-paste from definitions in CompCert/Lib/CoqLib.v *)
+Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q.
+Proof. auto. Qed.
+
+Ltac exploit x :=
+    refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _) _)
+ || refine (modusponens _ _ (x _ _) _)
+ || refine (modusponens _ _ (x _) _).
diff --git a/mppa_k1c/abstractbb/Impure/LICENSE b/mppa_k1c/abstractbb/Impure/LICENSE
new file mode 100644
index 00000000..65c5ca88
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/LICENSE
@@ -0,0 +1,165 @@
+                   GNU LESSER GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+
+  This version of the GNU Lesser General Public License incorporates
+the terms and conditions of version 3 of the GNU General Public
+License, supplemented by the additional permissions listed below.
+
+  0. Additional Definitions.
+
+  As used herein, "this License" refers to version 3 of the GNU Lesser
+General Public License, and the "GNU GPL" refers to version 3 of the GNU
+General Public License.
+
+  "The Library" refers to a covered work governed by this License,
+other than an Application or a Combined Work as defined below.
+
+  An "Application" is any work that makes use of an interface provided
+by the Library, but which is not otherwise based on the Library.
+Defining a subclass of a class defined by the Library is deemed a mode
+of using an interface provided by the Library.
+
+  A "Combined Work" is a work produced by combining or linking an
+Application with the Library.  The particular version of the Library
+with which the Combined Work was made is also called the "Linked
+Version".
+
+  The "Minimal Corresponding Source" for a Combined Work means the
+Corresponding Source for the Combined Work, excluding any source code
+for portions of the Combined Work that, considered in isolation, are
+based on the Application, and not on the Linked Version.
+
+  The "Corresponding Application Code" for a Combined Work means the
+object code and/or source code for the Application, including any data
+and utility programs needed for reproducing the Combined Work from the
+Application, but excluding the System Libraries of the Combined Work.
+
+  1. Exception to Section 3 of the GNU GPL.
+
+  You may convey a covered work under sections 3 and 4 of this License
+without being bound by section 3 of the GNU GPL.
+
+  2. Conveying Modified Versions.
+
+  If you modify a copy of the Library, and, in your modifications, a
+facility refers to a function or data to be supplied by an Application
+that uses the facility (other than as an argument passed when the
+facility is invoked), then you may convey a copy of the modified
+version:
+
+   a) under this License, provided that you make a good faith effort to
+   ensure that, in the event an Application does not supply the
+   function or data, the facility still operates, and performs
+   whatever part of its purpose remains meaningful, or
+
+   b) under the GNU GPL, with none of the additional permissions of
+   this License applicable to that copy.
+
+  3. Object Code Incorporating Material from Library Header Files.
+
+  The object code form of an Application may incorporate material from
+a header file that is part of the Library.  You may convey such object
+code under terms of your choice, provided that, if the incorporated
+material is not limited to numerical parameters, data structure
+layouts and accessors, or small macros, inline functions and templates
+(ten or fewer lines in length), you do both of the following:
+
+   a) Give prominent notice with each copy of the object code that the
+   Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the object code with a copy of the GNU GPL and this license
+   document.
+
+  4. Combined Works.
+
+  You may convey a Combined Work under terms of your choice that,
+taken together, effectively do not restrict modification of the
+portions of the Library contained in the Combined Work and reverse
+engineering for debugging such modifications, if you also do each of
+the following:
+
+   a) Give prominent notice with each copy of the Combined Work that
+   the Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the Combined Work with a copy of the GNU GPL and this license
+   document.
+
+   c) For a Combined Work that displays copyright notices during
+   execution, include the copyright notice for the Library among
+   these notices, as well as a reference directing the user to the
+   copies of the GNU GPL and this license document.
+
+   d) Do one of the following:
+
+       0) Convey the Minimal Corresponding Source under the terms of this
+       License, and the Corresponding Application Code in a form
+       suitable for, and under terms that permit, the user to
+       recombine or relink the Application with a modified version of
+       the Linked Version to produce a modified Combined Work, in the
+       manner specified by section 6 of the GNU GPL for conveying
+       Corresponding Source.
+
+       1) Use a suitable shared library mechanism for linking with the
+       Library.  A suitable mechanism is one that (a) uses at run time
+       a copy of the Library already present on the user's computer
+       system, and (b) will operate properly with a modified version
+       of the Library that is interface-compatible with the Linked
+       Version.
+
+   e) Provide Installation Information, but only if you would otherwise
+   be required to provide such information under section 6 of the
+   GNU GPL, and only to the extent that such information is
+   necessary to install and execute a modified version of the
+   Combined Work produced by recombining or relinking the
+   Application with a modified version of the Linked Version. (If
+   you use option 4d0, the Installation Information must accompany
+   the Minimal Corresponding Source and Corresponding Application
+   Code. If you use option 4d1, you must provide the Installation
+   Information in the manner specified by section 6 of the GNU GPL
+   for conveying Corresponding Source.)
+
+  5. Combined Libraries.
+
+  You may place library facilities that are a work based on the
+Library side by side in a single library together with other library
+facilities that are not Applications and are not covered by this
+License, and convey such a combined library under terms of your
+choice, if you do both of the following:
+
+   a) Accompany the combined library with a copy of the same work based
+   on the Library, uncombined with any other library facilities,
+   conveyed under the terms of this License.
+
+   b) Give prominent notice with the combined library that part of it
+   is a work based on the Library, and explaining where to find the
+   accompanying uncombined form of the same work.
+
+  6. Revised Versions of the GNU Lesser General Public License.
+
+  The Free Software Foundation may publish revised and/or new versions
+of the GNU Lesser General Public License from time to time. Such new
+versions will be similar in spirit to the present version, but may
+differ in detail to address new problems or concerns.
+
+  Each version is given a distinguishing version number. If the
+Library as you received it specifies that a certain numbered version
+of the GNU Lesser General Public License "or any later version"
+applies to it, you have the option of following the terms and
+conditions either of that published version or of any later version
+published by the Free Software Foundation. If the Library as you
+received it does not specify a version number of the GNU Lesser
+General Public License, you may choose any version of the GNU Lesser
+General Public License ever published by the Free Software Foundation.
+
+  If the Library as you received it specifies that a proxy can decide
+whether future versions of the GNU Lesser General Public License shall
+apply, that proxy's public statement of acceptance of any version is
+permanent authorization for you to choose that version for the
+Library.
diff --git a/mppa_k1c/abstractbb/Impure/README.md b/mppa_k1c/abstractbb/Impure/README.md
new file mode 100644
index 00000000..2b19d14a
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/README.md
@@ -0,0 +1,31 @@
+# `Impure`: importing OCaml functions as non-deterministic ones.
+
+The principle of this library is to encode the type `A -> B` of an
+OCaml function as a type `A -> ?? B` in Coq, where `?? B` is the type
+of an axiomatized monad that can be interpreted as `B -> Prop`.  In
+other word, this encoding abstracts an OCaml function as a function
+returning a postcondition on its possible results (ie a relation between its
+parameter and its result). Side-effects are simply ignored. And
+reasoning on such a function is only possible in partial correctness.
+
+See further explanations and examples on [ImpureDemo](https://github.com/boulme/ImpureDemo).
+
+## Credits
+
+[Sylvain Boulmé](mailto:Sylvain.Boulme@univ-grenoble-alpes.fr).
+
+## Code Overview
+
+- [ImpMonads](ImpMonads.v) axioms of "impure computations" and some Coq models of these axioms.
+
+- [ImpConfig](ImpConfig.v) declares the `Impure` monad and defines its extraction.
+
+- [ImpCore](ImpCore.v) defines notations for the `Impure` monad and a `wlp_simplify` tactic (to reason about `Impure` functions in a Hoare-logic style).
+
+- [ImpPrelude](ImpPrelude.v) declares the data types exchanged with `Impure` oracles.
+
+- [ImpIO](ImpIO.v), [ImpLoops](ImpLoops.v), [ImpHCons](ImpHCons.v) declare `Impure` oracles and define operators from these oracles.
+  [ImpExtern](ImpExtern.v) exports all these impure operators.
+
+- [ocaml/](ocaml/) subdirectory containing the OCaml implementations of `Impure` oracles.
+
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
new file mode 100644
index 00000000..c421ff87
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
@@ -0,0 +1,51 @@
+open ImpPrelude
+
+exception Stop;;
+    
+let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV)) =
+  let module MyHashedType = struct
+    type t = a pre_hashV
+    let equal x y = hash_eq x.pre_data y.pre_data
+    let hash x = Hashtbl.hash x.hcodes 
+  end in
+  let module MyHashtbl = Hashtbl.Make(MyHashedType) in
+  let pick t =
+    let res = ref None in
+    try
+      MyHashtbl.iter (fun k d -> res:=Some (k,d); raise Stop) t;
+      None
+    with
+    | Stop -> !res  
+    in
+  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'
+     | 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);
+   next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs));
+   export = fun () ->
+     match pick t with
+     | None -> { get_hashV = (fun _ -> raise Not_found);  iterall = (fun _ -> ()) } 
+     | Some (k,_) ->
+        (* the state is fully copied at export ! *)
+        let logs = ref (List.rev_append (!logs) []) in
+        let rec step_log i =
+          match !logs with
+          | (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;
+           {
+             get_hashV = (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
new file mode 100644
index 00000000..e81681df
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
@@ -0,0 +1,3 @@
+open ImpPrelude
+
+val xhCons: (('a -> 'a -> bool) * ('a pre_hashV -> 'a hashV)) -> 'a hashConsing
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml
new file mode 100644
index 00000000..e5ec8e87
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml
@@ -0,0 +1,146 @@
+(* Warning 
+
+These oracles assumes the following extraction directives:
+  "Require Import ExtrOcamlString."
+
+*)
+
+open ImpPrelude
+open BinNums
+open Datatypes
+
+(* two auxiliary functions, for efficient mapping of "int" to "BinNums.positive" *)
+exception Overflow
+  
+let aux_add: ('a, 'b) Hashtbl.t -> 'b Queue.t -> 'a -> 'b -> unit
+  = fun t q i p ->
+    if i < 1 then (* protection against wrap around *)
+      raise Overflow;
+    Queue.add p q;
+    Hashtbl.add t i p
+
+let memo_int2pos: int -> int -> BinNums.positive
+  = fun n ->
+    (* init of the Hashtbl *)
+    let n = max n 1 in
+    let t = Hashtbl.create n in
+    let q = Queue.create () in
+    aux_add t q 1 BinNums.Coq_xH ;
+    for i = 1 to (n-1)/2 do
+      let last = Queue.take q in
+      let ni = 2*i in
+      aux_add t q ni (BinNums.Coq_xO last);
+      aux_add t q (ni+1) (BinNums.Coq_xI last)
+    done;
+    if n mod 2 = 0 then (
+      let last = Queue.take q in
+      Hashtbl.add t n (BinNums.Coq_xO last)
+    );
+    (* memoized translation of i *)
+    let rec find i =
+      try
+        (* Printf.printf "-> %d\n" i; *)
+        Hashtbl.find t i
+      with Not_found ->
+        (* Printf.printf "<- %d\n" i; *)
+        if i <= 0 then
+          invalid_arg "non-positive integer"
+        else
+          let p = find (i/2) in
+          let pi = if i mod 2 = 0 then BinNums.Coq_xO p else BinNums.Coq_xI p in
+          Hashtbl.add t i pi;
+          pi
+     in find;;
+           
+  
+let string_coq2caml: char list -> string
+  = fun l ->
+    let buf = Buffer.create (List.length l) in
+    List.iter (fun c -> Buffer.add_char buf c) l;
+    Buffer.contents buf;;
+
+let new_exit_observer: (unit -> unit) -> (unit -> unit) ref
+  = fun f ->
+    let o = ref f in 
+    at_exit (fun () -> !o());
+    o;;
+
+let set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit
+  = fun (r, f) -> r := f
+
+let rec print: pstring -> unit
+  = fun ps ->
+    match ps with
+    | Str l -> List.iter print_char l
+    | CamlStr s -> print_string s
+    | Concat(ps1,ps2) -> (print ps1; print ps2);;
+
+let println: pstring -> unit
+  = fun l -> print l; print_newline()
+
+let read_line () =
+  CamlStr (Pervasives.read_line());;
+    
+exception ImpureFail of pstring;;
+
+let exn2string: exn -> pstring
+  = fun e -> CamlStr (Printexc.to_string e)
+
+let fail: pstring -> 'a
+  = fun s -> raise (ImpureFail s);;
+
+let try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a
+  = fun (k1, k2) ->
+    try
+      k1()
+    with
+    | (ImpureFail s) as e -> k2 s e
+
+let try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a
+  = fun (k1, k2) ->
+    try
+      k1()
+    with
+    | e -> k2 e
+
+(** MISC **)
+
+let rec posTr: BinNums.positive -> int
+= function
+  | BinNums.Coq_xH -> 1
+  | BinNums.Coq_xO p -> (posTr p)*2
+  | BinNums.Coq_xI p -> (posTr p)*2+1;;
+
+let zTr: BinNums.coq_Z -> int
+= function
+  | BinNums.Z0 -> 0
+  | BinNums.Zpos p -> posTr p
+  | BinNums.Zneg p -> - (posTr p)
+
+let ten = BinNums.Zpos (BinNums.Coq_xO (BinNums.Coq_xI (BinNums.Coq_xO BinNums.Coq_xH)))
+
+let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring
+= let (q,r) = BinIntDef.Z.pos_div_eucl p ten in       
+  let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in    
+  match q with
+  | BinNums.Z0 -> acc0
+  | BinNums.Zpos p0 -> string_of_pos p0 acc0
+  | _ -> assert false
+
+let string_of_Z_debug: BinNums.coq_Z -> pstring
+= fun p -> CamlStr (string_of_int (zTr p))
+
+let string_of_Z: BinNums.coq_Z -> pstring
+= function
+  | BinNums.Z0 -> CamlStr "0"
+  | BinNums.Zpos p -> string_of_pos p (CamlStr "")
+  | BinNums.Zneg p -> Concat (CamlStr "-", string_of_pos p (CamlStr ""))
+
+let timer ((f:'a -> 'b), (x:'a)) : 'b =
+  Gc.compact();
+  let itime = (Unix.times()).Unix.tms_utime in
+  let r = f x in
+  let rt = (Unix.times()).Unix.tms_utime -. itime in
+  Printf.printf "time = %f\n" rt;
+  r
+    
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli
new file mode 100644
index 00000000..29db881b
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli
@@ -0,0 +1,34 @@
+open ImpPrelude
+open Datatypes
+
+
+(* 
+Memoized version of translation from int -> BinNums.positive. 
+The first arg is an indicative bound on the max int translated:
+it pre-computes all positives lower or equal to this bound.  
+*)
+val memo_int2pos: int -> int -> BinNums.positive
+
+val read_line: unit -> pstring
+
+val print: pstring -> unit
+
+val println: pstring -> unit
+
+val string_of_Z: BinNums.coq_Z -> pstring
+
+val timer : (('a -> 'b ) * 'a) -> 'b   
+
+val new_exit_observer: (unit -> unit) -> (unit -> unit) ref
+
+val set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit
+
+val exn2string: exn -> pstring
+
+val fail: pstring -> 'a
+
+exception ImpureFail of pstring;;
+
+val try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a
+
+val try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpLoopOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpLoopOracles.ml
new file mode 100644
index 00000000..cb7625e5
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpLoopOracles.ml
@@ -0,0 +1,78 @@
+open ImpPrelude
+open Datatypes
+
+(** GENERIC ITERATIVE LOOP **) 
+
+(* a simple version of loop *)
+let simple_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b
+  = fun (a0, f) ->
+    let rec iter: 'a -> 'b
+      = fun a ->
+        match f a with
+        | Coq_inl a' -> iter a'
+        | Coq_inr b -> b
+    in
+    iter a0;;
+
+(* loop from while *)
+let while_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b
+  = fun (a0, f) ->
+    let s = ref (f a0) in
+    while (match !s with Coq_inl _ -> true | _ -> false) do
+      match !s with
+      | Coq_inl a -> s:=f a
+      | _ -> assert false
+    done;
+    match !s with
+    | Coq_inr b -> b
+    | _ -> assert false;;
+
+let loop = simple_loop
+
+
+(** GENERIC FIXPOINTS **)
+  
+let std_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b =
+  let rec f x = recf f x in
+  f
+
+let memo_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b  =
+  let memo = Hashtbl.create 10 in
+  let rec f x =
+    try
+      Hashtbl.find memo x
+    with
+      Not_found ->
+        let r = recf f x in
+        Hashtbl.replace memo x r;
+        r
+  in f
+
+let bare_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b  =
+  let fix = ref (fun x -> failwith "init") in
+  fix := (fun x -> recf !fix x);
+  !fix;;
+  
+let buggy_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b =
+  let memo = ref None in
+  let rec f x =
+    match !memo with
+    | Some y -> y
+    | None ->
+       let r = recf f x in
+       memo := Some r;
+       r
+  in f
+
+let xrec_mode = ref MemoRec
+
+let xrec_set_option : recMode -> unit
+= fun m -> xrec_mode := m
+
+let xrec : (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b )
+  = fun recf ->
+    match !xrec_mode with
+    | StdRec -> std_rec recf
+    | MemoRec -> memo_rec recf
+    | BareRec -> bare_rec recf
+    | BuggyRec -> buggy_rec recf
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpLoopOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpLoopOracles.mli
new file mode 100644
index 00000000..194696a1
--- /dev/null
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpLoopOracles.mli
@@ -0,0 +1,8 @@
+open ImpPrelude
+open Datatypes
+
+val loop: ('a * ('a -> ('a, 'b) sum)) -> 'b
+
+val xrec_set_option: recMode -> unit 
+
+val xrec: (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b ) 
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v
new file mode 100644
index 00000000..6bfd8770
--- /dev/null
+++ b/mppa_k1c/abstractbb/Parallelizability.v
@@ -0,0 +1,743 @@
+(** Parallel Semantics of Abstract Basic Blocks and parallelizability test.s
+*)
+
+Require Setoid. (* in order to rewrite <-> *)
+Require Export AbstractBasicBlocksDef.
+
+Require Import List.
+Import ListNotations.
+Local Open Scope list_scope.
+
+Require Import Sorting.Permutation.
+Require Import Bool.
+Local Open Scope lazy_bool_scope.
+
+
+Module ParallelSemantics (L: SeqLanguage).
+
+Export L.
+Local Open Scope list.
+
+(* parallel run of a macro *)
+Fixpoint macro_prun (i: macro) (m tmp old: mem): option mem :=
+  match i with
+  | nil => Some m
+  | (x, e)::i' =>
+     match exp_eval e tmp old with
+     | Some v' => macro_prun i' (assign m x v') (assign tmp x v') old
+     | None => None
+     end
+  end.
+
+(* [macro_prun] is generalization of [macro_run] *)   
+Lemma macro_run_prun i: forall m old,
+  macro_run i m old = macro_prun i m m old.
+Proof.
+  induction i as [|[y e] i']; simpl; auto.
+  intros m old; destruct (exp_eval e m old); simpl; auto.
+Qed.
+
+
+(* parallel run of a bblock -- with in-order writes *)
+Fixpoint prun_iw (p: bblock) m old: option mem :=
+  match p with
+  | nil => Some m
+  | i::p' =>
+    match macro_prun i m old old with
+    | Some m1 => prun_iw p' m1 old
+    | None => None
+    end
+  end.
+
+(* non-deterministic parallel run, due to arbitrary writes order *)
+Definition prun (p: bblock) m (om: option mem) := exists p', res_eq om (prun_iw p' m m) /\ Permutation p p'.
+
+
+(* a few lemma on equality *)
+
+Lemma macro_prun_equiv i old: forall m1 m2 tmp,
+  (forall x, m1 x = m2 x) ->
+  res_eq (macro_prun i m1 tmp old) (macro_prun i m2 tmp old).
+Proof.
+  induction i as [|[x e] i']; simpl; eauto.
+  intros m1 m2 tmp H; destruct (exp_eval e tmp old); simpl; auto.
+  eapply IHi'; unfold assign. intros; destruct (R.eq_dec x x0); auto.
+Qed.
+
+Lemma prun_iw_equiv p: forall m1 m2 old, 
+  (forall x, m1 x = m2 x) ->
+  res_eq (prun_iw p m1 old) (prun_iw p m2 old).
+Proof.
+  induction p as [|i p']; simpl; eauto.
+  - intros m1 m2 old H.
+    generalize (macro_prun_equiv i old m1 m2 old H);
+    destruct (macro_prun i m1 old old); simpl.
+    + intros (m3 & H3 & H4); rewrite H3; simpl; eauto.
+    + intros H1; rewrite H1; simpl; auto.
+Qed.
+
+End ParallelSemantics.
+
+
+
+
+
+Fixpoint notIn {A} (x: A) (l:list A): Prop :=
+  match l with
+  | nil => True
+  | a::l' => x <> a /\ notIn x l'
+  end.
+
+Lemma notIn_iff A (x:A) l: (~List.In x l) <-> notIn x l.
+Proof.
+  induction l; simpl; intuition.
+Qed.
+
+Lemma notIn_app A (x:A) l1: forall l2, notIn x (l1++l2) <-> (notIn x l1 /\ notIn x l2).
+Proof.
+  induction l1; simpl.
+  - intuition.
+  - intros; rewrite IHl1. intuition.
+Qed.
+
+
+Lemma In_Permutation A (l1 l2: list A): Permutation l1 l2 -> forall x, In x l1 -> In x l2.
+Proof.
+  induction 1; simpl; intuition.
+Qed.
+
+Lemma Permutation_incl A (l1 l2: list A): Permutation l1 l2 -> incl l1 l2.
+Proof.
+  unfold incl; intros; eapply In_Permutation; eauto.
+Qed.
+
+Lemma notIn_incl A (l1 l2: list A) x: incl l1 l2 -> notIn x l2 -> notIn x l1.
+Proof.
+  unfold incl; rewrite <- ! notIn_iff; intuition.
+Qed.
+
+
+Definition disjoint {A: Type} (l l':list A) : Prop := forall x, In x l -> notIn x l'.
+
+Lemma disjoint_sym_imp A (l1 l2: list A): disjoint l1 l2 -> disjoint l2 l1.
+Proof.
+  unfold disjoint. intros H x H1. generalize (H x). rewrite <- !notIn_iff. intuition.
+Qed.
+
+Lemma disjoint_sym A (l1 l2: list A): disjoint l1 l2 <-> disjoint l2 l1.
+Proof.
+  constructor 1; apply disjoint_sym_imp; auto.
+Qed.
+
+
+Lemma disjoint_cons_l A (x:A) (l1 l2: list A): disjoint (x::l1) l2 <-> (notIn x l2) /\ (disjoint l1 l2).
+Proof.
+  unfold disjoint. simpl; intuition subst; auto. 
+Qed.
+
+Lemma disjoint_cons_r A (x:A) (l1 l2: list A): disjoint l1 (x::l2) <-> (notIn x l1) /\ (disjoint l1 l2).
+Proof.
+  rewrite disjoint_sym, disjoint_cons_l, disjoint_sym; intuition.
+Qed.
+
+Lemma disjoint_app_r A (l l1 l2: list A): disjoint l (l1++l2) <-> (disjoint l l1 /\ disjoint l l2).
+Proof.
+  unfold disjoint. intuition. 
+  - generalize (H x H0). rewrite notIn_app; intuition.
+  - generalize (H x H0). rewrite notIn_app; intuition.
+  - rewrite notIn_app; intuition.
+Qed.
+
+Lemma disjoint_app_l A (l l1 l2: list A): disjoint (l1++l2) l <-> (disjoint l1 l /\ disjoint l2 l).
+Proof.
+  rewrite disjoint_sym,  disjoint_app_r; intuition; rewrite disjoint_sym; auto.
+Qed.
+
+Lemma disjoint_incl_r A (l1 l2: list A): incl l1 l2 -> forall l, disjoint l l2 -> disjoint l l1.
+Proof.
+  unfold disjoint. intros; eapply notIn_incl; eauto.
+Qed.
+
+Lemma disjoint_incl_l A (l1 l2: list A): incl l1 l2 -> forall l, disjoint l2 l -> disjoint l1 l.
+Proof.
+  intros; rewrite disjoint_sym. eapply disjoint_incl_r; eauto. rewrite disjoint_sym; auto.
+Qed.
+
+
+Module ParallelizablityChecking (L: SeqLanguage).
+
+Include ParallelSemantics L.
+
+
+(** * Preliminary notions on frames *)
+
+Lemma notIn_dec (x: R.t) l : { notIn x l } + { In x l }.
+Proof.
+  destruct (In_dec R.eq_dec x l). constructor 2; auto.
+  constructor 1; rewrite <- notIn_iff. auto.
+Qed.
+
+Fixpoint frame_assign m1 (f: list R.t) m2 := 
+  match f with
+  | nil => m1
+  | x::f' => frame_assign (assign m1 x (m2 x)) f' m2  
+  end.
+
+Lemma frame_assign_def f: forall m1 m2 x,
+   frame_assign m1 f m2 x = if notIn_dec x f then m1 x else m2 x.
+Proof.
+  induction f as [|y f] ; simpl; auto.
+  - intros; destruct (notIn_dec x []); simpl in *; tauto.
+  - intros; rewrite IHf; destruct (notIn_dec x (y::f)); simpl in *.
+    + destruct (notIn_dec x f); simpl in *; intuition.
+      rewrite assign_diff; auto.
+      rewrite <- notIn_iff in *; intuition.
+    + destruct (notIn_dec x f); simpl in *; intuition subst.
+      rewrite assign_eq; auto.
+      rewrite <- notIn_iff in *; intuition.
+Qed.
+
+Lemma frame_assign_In m1 f m2 x:
+   In x f -> frame_assign m1 f m2 x = m2 x.
+Proof.
+  intros; rewrite frame_assign_def; destruct (notIn_dec x f); auto.
+  rewrite <- notIn_iff in *; intuition.
+Qed.
+
+Lemma frame_assign_notIn m1 f m2 x:
+   notIn x f -> frame_assign m1 f m2 x = m1 x.
+Proof.
+  intros; rewrite frame_assign_def; destruct (notIn_dec x f); auto.
+  rewrite <- notIn_iff in *; intuition.
+Qed.
+
+Definition frame_eq (frame: R.t -> Prop) (om1 om2: option mem): Prop :=
+  match om1 with
+  | Some m1 => exists m2, om2 = Some m2 /\ forall x, (frame x) -> m1 x = m2 x 
+  | None => om2 = None
+  end.
+
+Lemma frame_eq_list_split f1 (f2: R.t -> Prop) om1 om2:
+ frame_eq (fun x => In x f1) om1 om2 ->
+ (forall m1 m2 x, om1 = Some m1 -> om2 = Some m2 -> f2 x -> notIn x f1 -> m1 x = m2 x) ->
+ frame_eq f2 om1 om2.
+Proof.
+  unfold frame_eq; destruct om1 as [ m1 | ]; simpl; auto.
+  intros (m2 & H0 & H1); subst.
+  intros H.
+  eexists; intuition eauto.
+  destruct (notIn_dec x f1); auto.
+Qed. 
+
+(*
+Lemma frame_eq_res_eq f om1 om2:
+ frame_eq (fun x => In x f) om1 om2 ->
+ (forall m1 m2 x, om1 = Some m1 -> om2 = Some m2 -> notIn x f -> m1 x = m2 x) ->
+ res_eq om1 om2.
+Proof.
+  intros H H0; lapply (frame_eq_list_split f (fun _ => True) om1 om2 H); eauto.
+  clear H H0; unfold frame_eq, res_eq. destruct om1; simpl; firstorder.
+Qed.
+*)
+
+(** * Writing frames *)
+
+Fixpoint macro_wframe(i:macro): list R.t := 
+  match i with
+  | nil => nil
+  | a::i' => (fst a)::(macro_wframe i') 
+  end.
+
+Lemma macro_wframe_correct i m' old: forall m tmp, 
+  macro_prun i m tmp old = Some m' -> 
+  forall x, notIn x (macro_wframe i) -> m' x  = m x.
+Proof.
+  induction i as [|[y e] i']; simpl.
+  - intros m tmp H x H0; inversion_clear H; auto.
+  - intros m tmp H x (H1 & H2); destruct (exp_eval e tmp old); simpl; try congruence.
+    cutrewrite (m x = assign m y v x); eauto.
+    rewrite assign_diff; auto.
+Qed.
+
+Lemma macro_prun_fequiv i old: forall m1 m2 tmp, 
+  frame_eq (fun x => In x (macro_wframe i)) (macro_prun i m1 tmp old) (macro_prun i m2 tmp old).
+Proof.
+  induction i as [|[y e] i']; simpl.
+  - intros m1 m2 tmp; eexists; intuition eauto.
+  - intros m1 m2 tmp. destruct (exp_eval e tmp old); simpl; auto.
+    eapply frame_eq_list_split; eauto. clear IHi'.
+    intros m1' m2' x H1 H2.
+    lapply (macro_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto.
+    lapply (macro_wframe_correct i' m2' old (assign m2 y v) (assign tmp y v)); eauto.
+    intros Xm2 Xm1 H H0. destruct H. 
+    + subst. rewrite Xm1, Xm2; auto. rewrite !assign_eq. auto.
+    + rewrite <- notIn_iff in H0; tauto.
+Qed.
+
+Lemma macro_prun_None i m1 m2 tmp old: 
+  macro_prun i m1 tmp old = None -> 
+  macro_prun i m2 tmp old = None.
+Proof.
+  intros H; generalize (macro_prun_fequiv i old m1 m2 tmp).
+  rewrite H; simpl; auto.
+Qed.
+
+Lemma macro_prun_Some i m1 m2 tmp old m1': 
+  macro_prun i m1 tmp old = Some m1' -> 
+  res_eq (Some (frame_assign m2 (macro_wframe i) m1')) (macro_prun i m2 tmp old).
+Proof.
+  intros H; generalize (macro_prun_fequiv i old m1 m2 tmp).
+  rewrite H; simpl.
+  intros (m2' & H1 & H2).
+  eexists; intuition eauto.
+  rewrite frame_assign_def.
+  lapply (macro_wframe_correct i m2' old m2 tmp); eauto.
+  destruct (notIn_dec x (macro_wframe i)); auto.
+  intros X; rewrite X; auto.
+Qed.
+
+Fixpoint bblock_wframe(p:bblock): list R.t := 
+  match p with
+  | nil => nil
+  | i::p' => (macro_wframe i)++(bblock_wframe p') 
+  end.
+
+Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm.
+
+Lemma bblock_wframe_Permutation p p': 
+ Permutation p p' -> Permutation (bblock_wframe p)  (bblock_wframe p').
+Proof.
+  induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; simpl; auto.
+  - rewrite! app_assoc; auto.
+  - eapply Permutation_trans; eauto.
+Qed.
+
+(*
+Lemma bblock_wframe_correct p m' old: forall m, 
+  prun_iw p m old = Some m' -> 
+  forall x, notIn x (bblock_wframe p) -> m' x = m x.
+Proof.
+  induction p as [|i p']; simpl.
+  - intros m H; inversion_clear H; auto.
+  - intros m H x; rewrite notIn_app; intros (H1 & H2). 
+    remember (macro_prun i m old old) as om.
+    destruct om as [m1|]; simpl.
+    + eapply eq_trans.
+      eapply IHp'; eauto.
+      eapply macro_wframe_correct; eauto.
+    + inversion H.
+Qed.
+
+Lemma prun_iw_fequiv p old: forall m1 m2, 
+  frame_eq (fun x => In x (bblock_wframe p)) (prun_iw p m1 old) (prun_iw p m2 old).
+Proof.
+  induction p as [|i p']; simpl.
+  - intros m1 m2; eexists; intuition eauto.
+  - intros m1 m2; generalize (macro_prun_fequiv i old m1 m2 old).
+    remember (macro_prun i m1 old old) as om.
+    destruct om as [m1'|]; simpl.
+    + intros (m2' & H1 & H2). rewrite H1; simpl.
+    eapply frame_eq_list_split; eauto. clear IHp'.
+    intros m1'' m2'' x H3 H4. rewrite in_app_iff.
+    intros X X2. assert (X1: In x (macro_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. }
+    clear X.
+    lapply (bblock_wframe_correct p' m1'' old m1'); eauto.
+    lapply (bblock_wframe_correct p' m2'' old m2'); eauto.
+    intros Xm2' Xm1'. 
+    rewrite Xm1', Xm2'; auto.
+    + intro H; rewrite H; simpl; auto.
+Qed.
+
+Lemma prun_iw_equiv p m1 m2 old: 
+  (forall x, notIn x (bblock_wframe p) -> m1 x = m2 x) ->
+  res_eq (prun_iw p m1 old) (prun_iw p m2 old).
+Proof.
+  intros; eapply frame_eq_res_eq.
+  eapply prun_iw_fequiv.
+  intros m1' m2' x H1 H2 H0.Require
+  lapply (bblock_wframe_correct p m1' old m1); eauto.
+  lapply (bblock_wframe_correct p m2' old m2); eauto.
+  intros X2 X1; rewrite X1, X2; auto.
+Qed.
+*)
+
+(** * Checking that parallel semantics is deterministic *)
+
+Fixpoint is_det (p: bblock): Prop :=
+  match p with
+  | nil => True
+  | i::p' =>
+       disjoint (macro_wframe i) (bblock_wframe p') (* no WRITE-AFTER-WRITE *)
+    /\ is_det p'
+  end.
+
+Lemma is_det_Permutation p p': 
+ Permutation p p' -> is_det p -> is_det p'.
+Proof.
+  induction 1; simpl; auto.
+  - intros; intuition. eapply disjoint_incl_r. 2: eauto.
+    eapply Permutation_incl. eapply Permutation_sym. 
+    eapply bblock_wframe_Permutation; auto.
+  - rewrite! disjoint_app_r in * |- *. intuition.
+    rewrite disjoint_sym; auto. 
+Qed.
+
+Theorem is_det_correct p p':
+  Permutation p p' -> 
+  is_det p -> 
+  forall m old, res_eq (prun_iw p m old) (prun_iw p' m old).
+Proof.
+  induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; simpl; eauto.
+  - intros [H0 H1] m old.
+    remember (macro_prun i m old old) as om0.
+    destruct om0 as [ m0 | ]; simpl; auto.
+  - rewrite disjoint_app_r.
+    intros ([Z1 Z2] & Z3 & Z4) m old.
+    remember (macro_prun i2 m old old) as om2.
+    destruct om2 as [ m2 | ]; simpl; auto.
+    + remember (macro_prun i1 m old old) as om1.
+      destruct om1 as [ m1 | ]; simpl; auto.
+      * lapply (macro_prun_Some i2 m m1 old old m2); simpl; auto.
+        lapply (macro_prun_Some i1 m m2 old old m1); simpl; auto.
+        intros (m1' & Hm1' & Xm1') (m2' & Hm2' & Xm2').
+        rewrite Hm1', Hm2'; simpl.
+        eapply prun_iw_equiv.
+        intros x; rewrite <- Xm1', <- Xm2'. clear Xm2' Xm1' Hm1' Hm2' m1' m2'.
+        rewrite frame_assign_def.
+        rewrite disjoint_sym in Z1; unfold disjoint in Z1.
+        destruct (notIn_dec x (macro_wframe i1)) as [ X1 | X1 ].
+        { rewrite frame_assign_def; destruct (notIn_dec x (macro_wframe i2)) as [ X2 | X2 ]; auto.
+          erewrite (macro_wframe_correct i2 m2 old m old); eauto.
+          erewrite (macro_wframe_correct i1 m1 old m old); eauto.
+        }
+        rewrite frame_assign_notIn; auto.
+     * erewrite macro_prun_None; eauto. simpl; auto.
+   + remember (macro_prun i1 m old old) as om1.
+     destruct om1 as [ m1 | ]; simpl; auto.
+     erewrite macro_prun_None; eauto.
+  - intros; eapply res_eq_trans.
+    eapply IHPermutation1; eauto.
+    eapply IHPermutation2; eauto.
+    eapply is_det_Permutation; eauto.
+Qed.
+
+(** * Standard Frames *)
+
+Fixpoint exp_frame (e: exp): list R.t :=
+  match e with
+  | Name x => x::nil
+  | Op o le => list_exp_frame le
+  | Old e => exp_frame e
+  end
+with list_exp_frame (le: list_exp): list R.t :=
+  match le with
+  | Enil => nil
+  | Econs e le' => exp_frame e ++ list_exp_frame le'
+  | LOld le => list_exp_frame le
+  end.
+
+Lemma exp_frame_correct e old1 old2: 
+  (forall x, In x (exp_frame e) -> old1 x = old2 x) ->
+  forall m1 m2, (forall x, In x (exp_frame e) -> m1 x = m2 x) ->
+   (exp_eval e m1 old1)=(exp_eval e m2 old2).
+Proof.
+  induction e using exp_mut with (P0:=fun l => (forall x, In x (list_exp_frame l) -> old1 x = old2 x) -> forall m1 m2, (forall x, In x (list_exp_frame l) -> m1 x = m2 x) ->
+   (list_exp_eval l m1 old1)=(list_exp_eval l m2 old2)); simpl; auto.
+  - intros H1 m1 m2 H2; rewrite H2; auto.
+  - intros H1 m1 m2 H2; erewrite IHe; eauto.
+  - intros H1 m1 m2 H2; erewrite IHe, IHe0; eauto; 
+    intros; (eapply H1 || eapply H2); rewrite in_app_iff; auto.
+Qed.
+
+Fixpoint macro_frame (i: macro): list R.t :=
+  match i with
+  | nil => nil
+  | a::i' => (fst a)::(exp_frame (snd a) ++ macro_frame i') 
+  end.
+
+Lemma macro_wframe_frame i x: In x (macro_wframe i) -> In x (macro_frame i).
+Proof.
+  induction i as [ | [y e] i']; simpl; intuition.
+Qed.
+
+
+Lemma macro_frame_correct i wframe old1 old2: forall m tmp1 tmp2,
+  (disjoint (macro_frame i) wframe) ->
+  (forall x, notIn x wframe -> old1 x = old2 x) ->
+  (forall x, notIn x wframe -> tmp1 x = tmp2 x) ->
+  macro_prun i m tmp1 old1 = macro_prun i m tmp2 old2.
+Proof.
+  induction i as [|[x e] i']; simpl; auto.
+  intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l.
+  intros (H1 & H2 & H3) H6 H7.
+  cutrewrite (exp_eval e tmp1 old1 = exp_eval e tmp2 old2).
+  - destruct (exp_eval e tmp2 old2); auto.
+    eapply IHi'; eauto. 
+    simpl; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); simpl; auto. 
+  - unfold disjoint in H2; apply exp_frame_correct.
+    intros;apply H6; auto.
+    intros;apply H7; auto.
+Qed.
+
+(** * Parallelizability *)
+
+Fixpoint pararec (p: bblock) (wframe: list R.t): Prop :=
+  match p with
+  | nil => True
+  | i::p' =>
+       disjoint (macro_frame i) wframe (* no USE-AFTER-WRITE *)
+    /\ pararec p' ((macro_wframe i) ++ wframe)
+  end.
+
+Lemma pararec_disjoint (p: bblock): forall wframe, pararec p wframe -> disjoint (bblock_wframe p) wframe.
+Proof.
+  induction p as [|i p']; simpl.
+  - unfold disjoint; simpl; intuition.
+  - intros wframe [H0 H1]; rewrite disjoint_app_l. 
+    generalize (IHp' _ H1).
+    rewrite disjoint_app_r. intuition. 
+    eapply disjoint_incl_l. 2: eapply H0.
+    unfold incl. eapply macro_wframe_frame; eauto.
+Qed.
+
+Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p.
+Proof.
+  induction p as [|i p']; simpl; auto.
+  intros wframe [H0 H1]. generalize (pararec_disjoint _ _ H1). rewrite disjoint_app_r.
+  intuition. 
+  - apply disjoint_sym; auto.
+  - eapply IHp'. eauto.
+Qed.
+
+Lemma pararec_correct p old: forall wframe m,
+  pararec p wframe -> 
+  (forall x, notIn x wframe -> m x = old x) ->
+  run p m = prun_iw p m old.
+Proof.
+  elim p; clear p; simpl; auto.
+  intros i p' X wframe m [H H0] H1.
+  erewrite macro_run_prun, macro_frame_correct; eauto.
+  remember (macro_prun i m old old) as om0.
+  destruct om0 as [m0 | ]; try congruence.
+  eapply X; eauto.
+  intro x; rewrite notIn_app. intros [H3 H4].
+  rewrite <- H1; auto.
+  eapply macro_wframe_correct; eauto.
+Qed.
+
+Definition parallelizable (p: bblock) := pararec p nil.
+
+Theorem parallelizable_correct p m om':
+  parallelizable p -> (prun p m om' <-> res_eq om' (run p m)).
+Proof.
+  intros H. constructor 1.
+  - intros (p' & H0 & H1). eapply res_eq_trans; eauto.
+    erewrite pararec_correct; eauto.
+    eapply res_eq_sym.
+    eapply is_det_correct; eauto.
+    eapply pararec_det; eauto.
+  - intros; unfold prun. 
+    eexists. constructor 1. 2: apply Permutation_refl. 
+    erewrite pararec_correct in H0; eauto.
+Qed.
+
+End ParallelizablityChecking.
+
+
+Module Type ResourceSet.
+
+Declare Module R: ResourceNames.
+
+(** We assume a datatype [t] refining (list R.t)
+
+This data-refinement is given by an abstract "invariant" match_frame below, 
+preserved by the following operations.
+
+*)
+
+Parameter t: Type.
+Parameter match_frame: t -> (list R.t) -> Prop.
+
+Parameter empty: t.
+Parameter empty_match_frame: match_frame empty nil.
+
+Parameter add: R.t -> t -> t.
+Parameter add_match_frame: forall s x l, match_frame s l -> match_frame (add x s) (x::l).
+
+Parameter union: t -> t -> t.
+Parameter union_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> match_frame (union s1 s2) (l1++l2).
+
+Parameter is_disjoint: t -> t -> bool.
+Parameter is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2. 
+
+End ResourceSet.
+
+
+Lemma lazy_andb_bool_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true.
+Proof.
+  destruct b1, b2; intuition.
+Qed.
+
+
+
+
+Module ParallelChecks (L: SeqLanguage) (S:ResourceSet with Module R:=L.LP.R).
+
+Include ParallelizablityChecking L.
+
+Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame.
+
+(** Now, refinement of each operation toward parallelizable *)
+
+Fixpoint macro_wsframe(i:macro): S.t :=
+  match i with
+  | nil => S.empty
+  | a::i' => S.add (fst a) (macro_wsframe i') 
+  end.
+
+Lemma macro_wsframe_correct i: S.match_frame (macro_wsframe i) (macro_wframe i).
+Proof.
+  induction i; simpl; auto.
+Qed.
+
+Fixpoint exp_sframe (e: exp): S.t :=
+  match e with
+  | Name x => S.add x S.empty
+  | Op o le => list_exp_sframe le
+  | Old e => exp_sframe e
+  end
+with list_exp_sframe (le: list_exp): S.t :=
+  match le with
+  | Enil => S.empty
+  | Econs e le' => S.union (exp_sframe e) (list_exp_sframe le')
+  | LOld le => list_exp_sframe le
+  end.
+
+Lemma exp_sframe_correct e: S.match_frame (exp_sframe e) (exp_frame e).
+Proof.
+  induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); simpl; auto.
+Qed.
+
+Fixpoint macro_sframe (i: macro): S.t :=
+  match i with
+  | nil => S.empty
+  | a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (macro_sframe i'))
+  end.
+
+Local Hint Resolve exp_sframe_correct.
+
+Lemma macro_sframe_correct i: S.match_frame (macro_sframe i) (macro_frame i).
+Proof.
+  induction i as [|[y e] i']; simpl; auto.
+Qed.
+
+Local Hint Resolve macro_wsframe_correct macro_sframe_correct.
+
+Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool :=
+  match p with
+  | nil => true
+  | i::p' =>
+       S.is_disjoint (macro_sframe i) wsframe (* no USE-AFTER-WRITE *)
+    &&& is_pararec p' (S.union (macro_wsframe i) wsframe)
+  end.
+
+Lemma is_pararec_correct (p: bblock): forall s l, S.match_frame s l -> (is_pararec p s)=true -> (pararec p l).
+Proof.
+  induction p; simpl; auto.
+  intros s l H1 H2; rewrite lazy_andb_bool_true in H2. destruct H2 as [H2 H3].
+  constructor 1; eauto.
+Qed.
+
+Definition is_parallelizable (p: bblock) := is_pararec p S.empty.
+
+Lemma is_para_correct_aux p: is_parallelizable p = true -> parallelizable p.
+Proof.
+  unfold is_parallelizable, parallelizable; intros; eapply is_pararec_correct; eauto.
+Qed.
+
+Theorem is_parallelizable_correct p:
+  is_parallelizable p = true -> forall m om', (prun p m om' <-> res_eq om' (run p m)).
+Proof.
+  intros; apply parallelizable_correct.
+  apply is_para_correct_aux. auto.
+Qed.
+
+End ParallelChecks.
+
+
+
+
+Require Import PArith.
+Require Import MSets.MSetPositive.
+
+Module PosResourceSet <: ResourceSet with Module R:=Pos.
+
+Module R:=Pos.
+
+(** We assume a datatype [t] refining (list R.t)
+
+This data-refinement is given by an abstract "invariant" match_frame below, 
+preserved by the following operations.
+
+*)
+
+Definition t:=PositiveSet.t.
+
+Definition match_frame (s:t) (l:list R.t): Prop
+ := forall x, PositiveSet.In x s <-> In x l.
+
+Definition empty:=PositiveSet.empty.
+
+Lemma empty_match_frame: match_frame empty nil.
+Proof.
+  unfold match_frame, empty, PositiveSet.In; simpl; intuition.
+Qed.
+
+Definition add: R.t -> t -> t := PositiveSet.add.
+
+Lemma add_match_frame: forall s x l, match_frame s l -> match_frame (add x s) (x::l).
+Proof.
+  unfold match_frame, add; simpl. 
+  intros s x l H y. rewrite PositiveSet.add_spec, H.
+  intuition. 
+Qed.
+
+Definition union: t -> t -> t := PositiveSet.union.
+Lemma union_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> match_frame (union s1 s2) (l1++l2).
+Proof.
+  unfold match_frame, union. 
+  intros s1 s2 l1 l2 H1 H2 x. rewrite PositiveSet.union_spec, H1, H2.
+  intuition. 
+Qed.
+
+Fixpoint is_disjoint (s s': PositiveSet.t) : bool :=
+  match s with
+  | PositiveSet.Leaf => true
+  | PositiveSet.Node l o r =>
+    match s' with
+    | PositiveSet.Leaf => true
+    | PositiveSet.Node l' o' r' => 
+      if (o &&& o') then false else (is_disjoint l l' &&& is_disjoint r r')
+    end
+  end.
+
+Lemma is_disjoint_spec_true s: forall s', is_disjoint s s' = true -> forall x, PositiveSet.In x s -> PositiveSet.In x s' -> False.
+Proof.
+  unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; simpl; try discriminate.
+  destruct s' as [|l' o' r']; simpl; try discriminate.
+  intros X.
+  assert (H: ~(o = true /\ o'=true) /\ is_disjoint l l' = true /\ is_disjoint r r'=true).
+  { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); simpl in X; intuition. }
+  clear X; destruct H as (H & H1 & H2).
+  destruct x as [i|i|]; simpl; eauto.
+Qed.
+
+Lemma is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2.
+Proof.
+  unfold match_frame, disjoint.
+  intros s1 s2 l1 l2 H1 H2 H3 x.
+  rewrite <- notIn_iff, <- H1, <- H2.
+  intros H4 H5; eapply is_disjoint_spec_true; eauto.
+Qed.
+
+End PosResourceSet.
diff --git a/mppa_k1c/abstractbb/README.md b/mppa_k1c/abstractbb/README.md
new file mode 100644
index 00000000..69e5defc
--- /dev/null
+++ b/mppa_k1c/abstractbb/README.md
@@ -0,0 +1,12 @@
+# Coq sources of AbstractBasicBlocks 
+
+- [AbstractBasicBlocksDef](AbstractBasicBlocksDef.v): syntax and sequential semantics of abstract basic blocks (on which we define our analyzes).
+This syntax and semantics is parametrized in order to adapt the language for different concrete basic block languages.
+
+- [Parallelizability](Parallelizability.v): define the parallel semantics and the 'is_parallelizable' function which tests whether the sequential run of a given abstract basic block is the same than a parallel run.
+
+- [DepTreeTheory](DepTreeTheory.v): defines a theory of dependency trees, such that two basic blocks with the same dependency tree have the same sequential semantics. In practice, permuting the instructions inside a basic block while perserving the dependencies of assignments should not change the dependency tree. The idea is to verify list schedulings, following ideas of [Formal verification of translation validators proposed by Tristan and Leroy](https://hal.inria.fr/inria-00289540/).
+
+- [ImpDep](ImpDep.v): adds a hash-consing mechanism to trees of [DepTreeTheory](DepTreeTheory.v), and thus provides an efficient "equality" test (a true answer ensures that the two basic blocks in input have the same sequential semantics) in order to check the correctness of list schedulings.
+
+- [DepExample](DepExample.v) defines a toy language (syntax and semantics); [DepExampleEqTest](DepExampleEqTest.v) defines a compiler of the toy language into abstract basic blocks and derives an equality test for the toy language; [DepExampleParallelTest](DepExampleParallelTest.v) derives a parallelizability test from the previous compiler; [DepExampleDemo](DepExampleDemo.v) is a test-suite for both tetsts.