delete useless DepExample* files

in order to avoid to keep these files up-to-date here...

4 files changed, 0 insertions, 1051 deletions

diff --git a/mppa_k1c/abstractbb/DepExample.v b/mppa_k1c/abstractbb/DepExample.v
deleted file mode 100644
index a239e24f..00000000
--- a/mppa_k1c/abstractbb/DepExample.v
+++ /dev/null
@@ -1,151 +0,0 @@
-(** 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
deleted file mode 100644
index 74e8f35e..00000000
--- a/mppa_k1c/abstractbb/DepExampleDemo.v
+++ /dev/null
@@ -1,400 +0,0 @@
-(** Demo of the example illustrating how to use ImpDep. *)
-
-Require Import DepExampleEqTest.
-Require Import Bool.
-
-Open Scope Z_scope.
-
-Module EqTests.
-
-Section TESTS.
-
-Variable ge: P.genv.
-
-(**** 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 ge (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
deleted file mode 100644
index a633ee07..00000000
--- a/mppa_k1c/abstractbb/DepExampleEqTest.v
+++ /dev/null
@@ -1,334 +0,0 @@
-(** 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.
-
-Definition genv := unit.
-
-Section IMP.
-
-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 (ge: genv) (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 IMP.
-End P.
-
-
-Module L <: ISeqLanguage with Module LP:=P.
-
-Module LP:=P.
-
-Include MkSeqLanguage P.
-
-End L.
-
-
-Module IDT := ImpDepTree L ImpPosDict.
-
-Section SECT.
-Variable ge: P.genv.
-
-(** 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 ge (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 ge (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 ge (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 ge (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 ge (comp_bblock p1) (comp_bblock p2)
-  else
-    IDT.bblock_eq_test ge (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.
-
-End SECT.
-(* 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
deleted file mode 100644
index 35b44683..00000000
--- a/mppa_k1c/abstractbb/DepExampleParallelTest.v
+++ /dev/null
@@ -1,166 +0,0 @@
-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.
-
-Section SEC.
-Variable ge: P.genv.
-
-(* 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 ge (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 ge (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 ge _ H); clear H.
-  intros H s os'.
-  rewrite bblock_par_iff_prun, H.
-  constructor; eauto.
-Qed.
-
-End SEC.
\ No newline at end of file