Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3

23 files changed, 117 insertions, 3313 deletions

diff --git a/kvx/InstructionScheduler.ml b/kvx/InstructionScheduler.ml
deleted file mode 100644
index eab0b21a..00000000
--- a/kvx/InstructionScheduler.ml
+++ /dev/null
@@ -1,1263 +0,0 @@
-(* *************************************************************)
-(*                                                             *)
-(*             The Compcert verified compiler                  *)
-(*                                                             *)
-(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
-(*           David Monniaux     CNRS, VERIMAG                  *)
-(*           Cyril Six          Kalray                         *)
-(*                                                             *)
-(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
-(*  This file is distributed under the terms of the INRIA      *)
-(*  Non-Commercial License Agreement.                          *)
-(*                                                             *)
-(* *************************************************************)
-
-let with_destructor dtor stuff f =
-  try let ret = f stuff in
-      dtor stuff;
-      ret
-  with exn -> dtor stuff;
-              raise exn;;
-
-let with_out_channel chan f = with_destructor close_out chan f;;
-let with_in_channel chan f = with_destructor close_in chan f;;
-
-(** Schedule instructions on a synchronized pipeline
-@author David Monniaux, CNRS, VERIMAG *)
-
-type latency_constraint = {
-    instr_from : int;
-    instr_to : int;
-    latency : int };;
-
-type problem = {
-  max_latency : int;
-  resource_bounds : int array;
-  instruction_usages : int array array;
-  latency_constraints : latency_constraint list;
-  };;
-
-let print_problem channel problem =
-  (if problem.max_latency >= 0
-   then Printf.fprintf channel "max makespan: %d\n" problem.max_latency);
-  output_string channel "resource bounds:";
-  (Array.iter (fun b -> Printf.fprintf channel " %d" b) problem.resource_bounds);
-  output_string channel ";\n";
-  (Array.iteri (fun i v ->
-       Printf.fprintf channel "instr%d:" i;
-       (Array.iter (fun b -> Printf.fprintf channel " %d" b) v);
-       output_string channel ";\n") problem.instruction_usages);
-  List.iter (fun instr ->
-      Printf.printf "t%d - t%d >= %d;\n"
-        instr.instr_to instr.instr_from instr.latency)
-    problem.latency_constraints;;
-
-let get_nr_instructions problem = Array.length problem.instruction_usages;;
-let get_nr_resources problem = Array.length problem.resource_bounds;;
-
-type solution = int array
-type scheduler = problem -> solution option
-
-(* DISABLED				    
-(** Schedule the problem optimally by constraint solving using the Gecode solver. *)
-external gecode_scheduler : problem -> solution option =
-  "caml_gecode_schedule_instr";;
- *)
-				     
-let maximum_slot_used times =
-  let maxi = ref (-1) in
-  for i=0 to (Array.length times)-2
-  do
-    maxi := max !maxi times.(i)
-  done;
-  !maxi;;
-
-let check_schedule (problem : problem) (times : solution) =
-  let nr_instructions = get_nr_instructions problem in
-  (if Array.length times <> nr_instructions+1
-   then failwith
-          (Printf.sprintf "check_schedule: %d times expected, got %d"
-            (nr_instructions+1) (Array.length times)));
-  (if problem.max_latency >= 0 && times.(nr_instructions)> problem.max_latency
-   then failwith "check_schedule: max_latency exceeded");
-  (Array.iteri (fun i time ->
-       (if time < 0
-        then failwith (Printf.sprintf "time[%d] < 0" i))) times);
-  let slot_resources = Array.init ((maximum_slot_used times)+1)
-                         (fun _ -> Array.copy problem.resource_bounds) in
-  for i=0 to nr_instructions -1
-  do
-    let remaining_resources = slot_resources.(times.(i))
-    and used_resources = problem.instruction_usages.(i) in
-    for resource=0 to (Array.length used_resources)-1
-    do
-      let after = remaining_resources.(resource) - used_resources.(resource) in
-      (if after < 0
-       then failwith (Printf.sprintf "check_schedule: instruction %d exceeds resource %d at slot %d" i resource times.(i)));
-      remaining_resources.(resource) <- after
-    done
-  done;
-  List.iter (fun ctr ->
-      if times.(ctr.instr_to) - times.(ctr.instr_from) < ctr.latency
-      then failwith (Printf.sprintf "check_schedule: time[%d]=%d - time[%d]=%d < %d"
-                       ctr.instr_to times.(ctr.instr_to)
-                       ctr.instr_from times.(ctr.instr_from)
-                       ctr.latency)
-    ) problem.latency_constraints;;
-
-let bound_max_time problem =
-  let total = ref(Array.length problem.instruction_usages) in
-  List.iter (fun ctr -> total := !total + ctr.latency) problem.latency_constraints;
-  !total;;
-
-let vector_less_equal a b =
-  try
-    Array.iter2 (fun x y ->
-        if x>y
-        then raise Exit) a b;
-    true
-  with Exit -> false;;
-
-let vector_subtract a b =
-  assert ((Array.length a) = (Array.length b));
-  for i=0 to (Array.length a)-1
-  do
-    b.(i) <- b.(i) - a.(i)
-  done;;
-
-(* The version with critical path ordering is much better! *)
-type list_scheduler_order =
-  | INSTRUCTION_ORDER
-  | CRITICAL_PATH_ORDER;;
-
-let int_max (x : int) (y : int) =
-  if x > y then x else y;;
-
-let int_min (x : int) (y : int) =
-  if x < y then x else y;;
-
-let get_predecessors problem =
-  let nr_instructions = get_nr_instructions problem in
-  let predecessors = Array.make (nr_instructions+1) [] in
-  List.iter (fun ctr ->
-      predecessors.(ctr.instr_to) <-
-        (ctr.instr_from, ctr.latency)::predecessors.(ctr.instr_to))
-    problem.latency_constraints;
-  predecessors;;
-
-let get_successors problem =
-  let nr_instructions = get_nr_instructions problem in
-  let successors = Array.make nr_instructions [] in
-  List.iter (fun ctr ->
-      successors.(ctr.instr_from) <-
-             (ctr.instr_to, ctr.latency)::successors.(ctr.instr_from))
-    problem.latency_constraints;
-  successors;;
-
-let critical_paths successors =
-  let nr_instructions = Array.length successors in
-  let path_lengths =  Array.make nr_instructions (-1) in
-  let rec compute i =
-    if i=nr_instructions then 0 else
-      match path_lengths.(i) with
-      | -2 -> failwith "InstructionScheduler: the dependency graph has cycles"
-      | -1 -> path_lengths.(i) <- -2;
-              let x = List.fold_left
-                        (fun cur (j, latency)-> int_max cur (latency+(compute j)))
-                        1 successors.(i)
-              in path_lengths.(i) <- x; x
-      | x -> x
-  in for i = nr_instructions-1 downto 0
-     do
-       ignore (compute i)
-     done;
-     path_lengths;;
-
-let maximum_critical_path problem =
-  let paths = critical_paths (get_successors problem) in
-  Array.fold_left int_max 0 paths;;
-
-let get_earliest_dates predecessors =
-  let nr_instructions = (Array.length predecessors)-1 in
-  let path_lengths =  Array.make (nr_instructions+1) (-1) in
-  let rec compute i =
-    match path_lengths.(i) with
-    | -2 -> failwith "InstructionScheduler: the dependency graph has cycles"
-    | -1 -> path_lengths.(i) <- -2;
-            let x = List.fold_left
-                      (fun cur (j, latency)-> int_max cur (latency+(compute j)))
-                      0 predecessors.(i)
-            in path_lengths.(i) <- x; x
-    | x -> x
-  in for i = 0 to nr_instructions
-     do
-       ignore (compute i)
-     done;
-     for i = 0 to nr_instructions - 1
-     do
-       path_lengths.(nr_instructions) <- int_max
-	 path_lengths.(nr_instructions) (1 + path_lengths.(i))
-     done;
-     path_lengths;;
-
-exception Unschedulable
-        
-let get_latest_dates deadline successors =
-  let nr_instructions = Array.length successors
-  and path_lengths = critical_paths successors in
-  Array.init (nr_instructions + 1)
-	     (fun i ->
-	      if i < nr_instructions then
-		let path_length = path_lengths.(i) in
-		assert (path_length >= 1);
-		(if path_length > deadline
-                 then raise Unschedulable);
-		deadline - path_length
-	      else deadline);;
-  
-let priority_list_scheduler (order : list_scheduler_order)
-      (problem : problem) :
-      solution option =
-  let nr_instructions = get_nr_instructions problem in
-  let successors = get_successors problem
-  and predecessors = get_predecessors problem
-  and times = Array.make (nr_instructions+1) (-1) in
-
-  let priorities = match order with
-    | INSTRUCTION_ORDER -> None
-    | CRITICAL_PATH_ORDER -> Some (critical_paths successors) in
-  
-  let module InstrSet =
-    Set.Make (struct type t=int
-                     let compare = match priorities with
-                       | None -> (fun x y -> x - y)
-                       | Some p -> (fun x y ->
-                         (match p.(y)-p.(x) with
-                          | 0 -> x - y
-                          | z -> z))
-              end) in
-
-  let max_time = bound_max_time problem in
-  let ready = Array.make max_time InstrSet.empty in
-  Array.iteri (fun i preds ->
-      if i<nr_instructions && preds=[]
-      then ready.(0) <- InstrSet.add i ready.(0)) predecessors;
-  
-  let current_time = ref 0
-  and current_resources = Array.copy problem.resource_bounds
-  and earliest_time i =
-    try
-      let time = ref (-1) in
-      List.iter (fun (j, latency) ->
-          if times.(j) < 0
-          then raise Exit
-          else let t = times.(j) + latency in
-               if t > !time
-               then time := t) predecessors.(i);
-      assert(!time >= 0);
-      !time
-    with Exit -> -1
-               
-  in
-  let advance_time() =
-    begin
-      (if !current_time < max_time-1
-      then
-        begin
-          Array.blit problem.resource_bounds 0 current_resources 0
-            (Array.length current_resources);
-          ready.(!current_time + 1) <-
-            InstrSet.union (ready.(!current_time)) (ready.(!current_time + 1));
-          ready.(!current_time) <- InstrSet.empty;
-        end);
-      incr current_time
-    end in
-
-  let attempt_scheduling ready usages =
-    let result = ref (-1) in
-    try
-      InstrSet.iter (fun i ->
-          (* Printf.printf "trying scheduling %d\n" i;
-        pr   int_vector usages.(i);
-        print           _vector current_resources; *)
-          if vector_less_equal usages.(i) current_resources
-          then
-            begin
-              vector_subtract usages.(i) current_resources;
-              result := i;
-              raise Exit
-            end) ready;
-      -1
-    with Exit -> !result in
-  
-  while !current_time < max_time
-  do
-    if (InstrSet.is_empty ready.(!current_time))
-     then advance_time()
-    else
-      match attempt_scheduling ready.(!current_time)
-              problem.instruction_usages with
-    | -1 -> advance_time()
-    | i ->
-       begin
-         assert(times.(i) < 0);
-         times.(i) <- !current_time;
-         ready.(!current_time) <- InstrSet.remove i (ready.(!current_time));
-         List.iter (fun (instr_to, latency) ->
-             if instr_to < nr_instructions then
-               match earliest_time instr_to with
-               | -1 -> ()
-               | to_time ->
-                  ready.(to_time) <- InstrSet.add instr_to ready.(to_time))
-           successors.(i);
-         successors.(i) <- []
-       end
-  done;
-  try
-    let final_time = ref (-1) in
-    for i=0 to nr_instructions-1
-    do
-      (if times.(i) < 0 then raise Exit);
-      (if !final_time < times.(i)+1 then final_time := times.(i)+1)
-    done;
-    List.iter (fun (i, latency) ->
-        let target_time = latency + times.(i) in
-        if target_time > !final_time
-        then final_time := target_time
-      ) predecessors.(nr_instructions);
-    times.(nr_instructions) <- !final_time;
-    Some times
-  with Exit -> None;;
-
-let list_scheduler = priority_list_scheduler CRITICAL_PATH_ORDER;;
-
-(* dummy code for placating ocaml's warnings *)
-let _ = fun x -> priority_list_scheduler INSTRUCTION_ORDER x;;
-
-type bundle = int list;;
-
-let rec extract_deps_to index = function
-  | [] -> []
-  | dep :: deps -> let extracts = extract_deps_to index deps in
-      if (dep.instr_to == index) then 
-        dep :: extracts
-      else
-        extracts
-
-exception InvalidBundle;;
-
-let dependency_check problem bundle index =
-  let index_deps = extract_deps_to index problem.latency_constraints in
-  List.iter (fun i -> 
-    List.iter (fun dep ->
-      if (dep.instr_from == i) then raise InvalidBundle
-    ) index_deps
-  ) bundle;;
-
-let rec make_bundle problem resources bundle index =
-  let resources_copy = Array.copy resources in
-  let nr_instructions = get_nr_instructions problem in
-  if (index >= nr_instructions) then (bundle, index+1) else
-  let inst_usage = problem.instruction_usages.(index) in
-  try match vector_less_equal inst_usage resources with
-  | false -> raise InvalidBundle
-  | true -> (
-      dependency_check problem bundle index;
-      vector_subtract problem.instruction_usages.(index) resources_copy;
-      make_bundle problem resources_copy (index::bundle) (index+1)
-      )
-  with InvalidBundle -> (bundle, index);;
-
-let rec make_bundles problem index : bundle list =
-  if index >= get_nr_instructions problem then
-    []
-  else
-    let (bundle, new_index) = make_bundle problem problem.resource_bounds [] index in
-    bundle :: (make_bundles problem new_index);;
-
-let bundles_to_schedule problem bundles : solution =
-  let nr_instructions = get_nr_instructions problem in
-  let schedule = Array.make (nr_instructions+1) (nr_instructions+4) in
-  let time = ref 0 in
-  List.iter (fun bundle ->
-    begin
-    List.iter (fun i ->
-      schedule.(i) <- !time
-    ) bundle;
-    time := !time + 1
-    end
-  ) bundles; schedule;;
-
-let greedy_scheduler (problem : problem) : solution option =
-  let bundles = make_bundles problem 0 in
-  Some (bundles_to_schedule problem bundles);;
-  
-(* alternate implementation
-let swap_array_elements a i j =
-  let x = a.(i) in
-  a.(i) <- a.(j);
-  a.(j) <- x;;
-
-let array_reverse_slice a first last =
-  let i = ref first and j = ref last in
-  while i < j
-  do
-    swap_array_elements a !i !j;
-    incr i;
-    decr j
-  done;;
-
-let array_reverse a =
-  let a' = Array.copy a in
-  array_reverse_slice a' 0 ((Array.length a)-1);
-  a';;
- *)
-
-(* unneeded
-let array_reverse a =
-  let n=Array.length a in
-  Array.init n (fun i -> a.(n-1-i));;
- *)
-
-let reverse_constraint nr_instructions ctr =
-  { instr_to = nr_instructions -ctr.instr_from;
-    instr_from =  nr_instructions - ctr.instr_to;
-    latency = ctr.latency };;
-
-(* unneeded
-let rec list_map_filter f = function
-  | [] ->  []                                      
-  | h::t ->
-     (match f h with
-      | None ->  list_map_filter f t
-      | Some x -> x :: (list_map_filter f t));;
- *)
-
-let reverse_problem problem =
-  let nr_instructions = get_nr_instructions problem in
-  {
-    max_latency = problem.max_latency;
-    resource_bounds = problem.resource_bounds;
-    instruction_usages = Array.init (nr_instructions + 1)
-      (fun i ->
-        if i=0
-        then Array.map (fun _ -> 0) problem.resource_bounds                             else problem.instruction_usages.(nr_instructions - i));
-    latency_constraints = List.map (reverse_constraint nr_instructions)
-                            problem.latency_constraints
-  };;
-
-let max_scheduled_time solution =
-  let time = ref (-1) in
-  for i = 0 to ((Array.length solution) - 2)
-  do
-    time := max !time solution.(i)
-  done;
-  !time;;
-
-(*
-let recompute_makespan problem solution =
-  let n = (Array.length solution) - 1 and ms = ref 0 in
-  List.iter (fun cstr ->
-      if cstr.instr_to = n
-      then ms := max !ms (solution.(cstr.instr_from) + cstr.latency) 
-    ) problem.latency_constraints;
-  !ms;;
- *)
-
-let schedule_reversed (scheduler : problem -> solution option)
-    (problem : problem) =
-  match scheduler (reverse_problem problem) with
-  | None -> None
-  | Some solution ->
-     let nr_instructions = get_nr_instructions problem in
-     let makespan = max_scheduled_time solution in
-     let ret = Array.init (nr_instructions + 1)
-                 (fun i -> makespan-solution.(nr_instructions-i)) in
-     ret.(nr_instructions) <- max ((max_scheduled_time ret) + 1)
-                                (ret.(nr_instructions));
-     Some ret;;
-
-(** Schedule the problem using a greedy list scheduling algorithm, from the end. *)
-let reverse_list_scheduler = schedule_reversed list_scheduler;;
-
-let check_problem problem =
-  (if (Array.length problem.instruction_usages) < 1
-   then failwith "length(problem.instruction_usages) < 1");;
-
-let validated_scheduler (scheduler : problem -> solution option)
-      (problem : problem) =
-  check_problem problem;
-  match scheduler problem with
-  | None -> None
-  | (Some solution) as ret -> check_schedule problem solution; ret;;
-
-let get_max_latency solution =
-  solution.((Array.length solution)-1);;
-  
-let show_date_ranges problem =
-  let deadline = problem.max_latency in
-  assert(deadline >= 0);
-  let successors = get_successors problem
-  and predecessors = get_predecessors problem in
-  let earliest_dates : int array = get_earliest_dates predecessors
-  and latest_dates : int array = get_latest_dates deadline successors in
-  assert ((Array.length earliest_dates) =
-            (Array.length latest_dates));
-  Array.iteri (fun i early ->
-      let late = latest_dates.(i) in
-      Printf.printf "t[%d] in %d..%d\n" i early late)
-    earliest_dates;;
-
-type pseudo_boolean_problem_type =
-  | SATISFIABILITY
-  | OPTIMIZATION;;
-
-type pseudo_boolean_mapper = {
-  mapper_pb_type : pseudo_boolean_problem_type;
-  mapper_nr_instructions : int;
-  mapper_nr_pb_variables : int;
-  mapper_earliest_dates : int array;
-  mapper_latest_dates : int array;
-  mapper_var_offsets : int array;
-  mapper_final_predecessors : (int * int) list
-};;
-
-(* Latency constraints are:
-  presence of instr-to at each t <= sum of presences of instr-from at compatible times
-  
-  if reverse_encoding
-  presence of instr-from at each t <= sum of presences of instr-to at compatible times *)
-
-(* Experiments show reverse_encoding=true multiplies time by 2 in sat4j
-   without making hard instances easier *)
-let direct_encoding = false
-and reverse_encoding = false
-and delta_encoding = true
-                   
-let pseudo_boolean_print_problem channel problem pb_type =
-  let deadline = problem.max_latency in
-  assert (deadline > 0);
-  let nr_instructions = get_nr_instructions problem
-  and nr_resources = get_nr_resources problem
-  and successors = get_successors problem
-  and predecessors = get_predecessors problem in
-  let earliest_dates = get_earliest_dates predecessors
-  and latest_dates = get_latest_dates deadline successors in
-  let var_offsets = Array.make
-                      (match pb_type with
-                       | OPTIMIZATION -> nr_instructions+1
-                       | SATISFIABILITY -> nr_instructions) 0 in
-  let nr_pb_variables =
-    (let nr = ref 0 in
-     for i=0 to (match pb_type with
-                 | OPTIMIZATION -> nr_instructions
-                 | SATISFIABILITY -> nr_instructions-1)
-     do
-        var_offsets.(i) <- !nr;
-        nr := !nr + latest_dates.(i) - earliest_dates.(i) + 1
-     done;
-     !nr)
-  and nr_pb_constraints =
-    (match pb_type with
-     | OPTIMIZATION -> nr_instructions+1
-     | SATISFIABILITY -> nr_instructions) +
-
-    (let count = ref 0 in
-     for t=0 to deadline-1
-     do
-       for j=0 to nr_resources-1
-       do
-         try
-           for i=0 to nr_instructions-1
-           do
-             let usage = problem.instruction_usages.(i).(j) in
-             if t >= earliest_dates.(i) && t <= latest_dates.(i)
-                && usage > 0 then raise Exit
-           done
-         with Exit -> incr count
-       done
-     done;
-     !count) +
-      
-     (let count=ref 0 in
-      List.iter
-        (fun ctr ->
-          if ctr.instr_to < nr_instructions
-          then count := !count + 1 + latest_dates.(ctr.instr_to)
-                                   - earliest_dates.(ctr.instr_to)
-                    + (if reverse_encoding
-                       then 1 + latest_dates.(ctr.instr_from)
-                -      earliest_dates.(ctr.instr_from)
-                       else 0)
-        )
-        problem.latency_constraints;
-      !count) +
-      
-      (match pb_type with
-       | OPTIMIZATION -> (1 + deadline - earliest_dates.(nr_instructions)) * nr_instructions
-       | SATISFIABILITY -> 0)
-  and measured_nr_constraints = ref 0 in
-
-  let pb_var i t =
-    assert(t >= earliest_dates.(i));
-    assert(t <= latest_dates.(i));
-    let v = 1+var_offsets.(i)+t-earliest_dates.(i) in
-    assert(v <= nr_pb_variables);
-    Printf.sprintf "x%d" v in
-  
-  let end_constraint () =
-    begin
-      output_string channel ";\n";
-      incr measured_nr_constraints
-    end in
-
-  let gen_latency_constraint i_to i_from latency t_to =
-    Printf.fprintf channel "* t[%d] - t[%d] >= %d when t[%d]=%d\n"
-		   i_to i_from latency i_to t_to;
-        for t_from=earliest_dates.(i_from) to
-              int_min latest_dates.(i_from) (t_to - latency)
-        do
-          Printf.fprintf channel "+1 %s " (pb_var i_from t_from)
-        done;
-        Printf.fprintf channel "-1 %s " (pb_var i_to t_to);
-        Printf.fprintf channel ">= 0";
-        end_constraint()
-
-  and gen_dual_latency_constraint i_to i_from latency t_from =
-    Printf.fprintf channel "* t[%d] - t[%d] >= %d when t[%d]=%d\n"
-		   i_to i_from latency i_to t_from;
-        for t_to=int_max earliest_dates.(i_to) (t_from + latency)
-            to latest_dates.(i_to)
-        do
-          Printf.fprintf channel "+1 %s " (pb_var i_to t_to)
-        done;
-        Printf.fprintf channel "-1 %s " (pb_var i_from t_from);
-        Printf.fprintf channel ">= 0";
-        end_constraint()
-  in
-  
-  Printf.fprintf channel "* #variable= %d #constraint= %d\n" nr_pb_variables nr_pb_constraints;
-  Printf.fprintf channel "* nr_instructions=%d deadline=%d\n" nr_instructions deadline;
-  begin
-    match pb_type with
-    | SATISFIABILITY -> ()
-    | OPTIMIZATION ->
-       output_string channel "min:";
-       for t=earliest_dates.(nr_instructions) to deadline
-       do
-         Printf.fprintf channel " %+d %s" t (pb_var nr_instructions t)
-       done;
-       output_string channel ";\n";
-  end;
-  for i=0 to (match pb_type with
-              | OPTIMIZATION -> nr_instructions
-              | SATISFIABILITY -> nr_instructions-1)
-  do
-    let early = earliest_dates.(i) and late= latest_dates.(i) in
-    Printf.fprintf channel "* t[%d] in %d..%d\n" i early late;
-    for t=early to late
-    do
-      Printf.fprintf channel "+1 %s " (pb_var i t)
-    done;
-    Printf.fprintf channel "= 1";
-    end_constraint()
-  done;
-
-  for t=0 to deadline-1
-  do
-    for j=0 to nr_resources-1
-    do
-      let bound = problem.resource_bounds.(j)
-      and coeffs = ref [] in
-      for i=0 to nr_instructions-1
-      do
-        let usage = problem.instruction_usages.(i).(j) in
-        if t >= earliest_dates.(i) && t <= latest_dates.(i)
-           && usage > 0
-        then coeffs := (i, usage) :: !coeffs 
-      done;
-      if !coeffs <> [] then
-        begin
-          Printf.fprintf channel "* resource #%d at t=%d <= %d\n" j t bound;
-          List.iter (fun (i, usage) ->
-              Printf.fprintf channel "%+d %s " (-usage) (pb_var i t)) !coeffs;
-          Printf.fprintf channel ">= %d" (-bound);
-          end_constraint();
-        end
-    done
-  done;
-  
-  List.iter
-    (fun ctr ->
-      if ctr.instr_to < nr_instructions then
-        begin
-          for t_to=earliest_dates.(ctr.instr_to) to latest_dates.(ctr.instr_to)
-          do
-	    gen_latency_constraint ctr.instr_to ctr.instr_from ctr.latency t_to
-          done;
-          if reverse_encoding
-          then
-            for t_from=earliest_dates.(ctr.instr_from) to latest_dates.(ctr.instr_from)
-            do
-	      gen_dual_latency_constraint ctr.instr_to ctr.instr_from ctr.latency t_from
-            done
-        end
-    ) problem.latency_constraints;
-  
-  begin
-    match pb_type with
-    | SATISFIABILITY -> ()
-    | OPTIMIZATION ->
-       let final_latencies = Array.make nr_instructions 1 in
-       List.iter (fun (i, latency) ->
-	   final_latencies.(i) <- int_max final_latencies.(i) latency)
-	 predecessors.(nr_instructions);
-       for t_to=earliest_dates.(nr_instructions) to deadline
-       do
-         for i_from = 0 to nr_instructions -1
-         do
-	   gen_latency_constraint nr_instructions i_from final_latencies.(i_from) t_to
-         done
-       done
-  end;
-  assert (!measured_nr_constraints = nr_pb_constraints);
-  {
-    mapper_pb_type = pb_type;
-    mapper_nr_instructions = nr_instructions;
-    mapper_nr_pb_variables = nr_pb_variables;
-    mapper_earliest_dates = earliest_dates;
-    mapper_latest_dates = latest_dates;
-    mapper_var_offsets = var_offsets;
-    mapper_final_predecessors = predecessors.(nr_instructions)
-  };;
-
-type pb_answer =
-  | Positive
-  | Negative
-  | Unknown
-      
-let line_to_pb_solution sol line nr_pb_variables =
-  let assign s v =
-    begin
-      let i = int_of_string s in
-      sol.(i-1) <- v
-    end in
-  List.iter
-    begin
-      function "" -> ()
-	     | item ->
-		(match String.get item 0 with
-		 | '+' ->
-		    assert ((String.length item) >= 3);
-		    assert ((String.get item 1) = 'x');
-		    assign (String.sub item 2 ((String.length item)-2)) Positive
-		 | '-' ->
-		    assert ((String.length item) >= 3);
-		    assert ((String.get item 1) = 'x');
-		    assign (String.sub item 2 ((String.length item)-2)) Negative
-		 | 'x' ->
-		    assert ((String.length item) >= 2);
-		    assign (String.sub item 1 ((String.length item)-1)) Positive
-                 | _ -> failwith "syntax error in pseudo Boolean solution: epected + - or x" 
-		)
-    end
-    (String.split_on_char ' ' (String.sub line 2 ((String.length line)-2)));;
-
-let pb_solution_to_schedule mapper pb_solution =
-  Array.mapi (fun i offset ->
-	      let first = mapper.mapper_earliest_dates.(i)
-	      and last = mapper.mapper_latest_dates.(i)
-	      and time = ref (-1) in
-	      for t=first to last
-	      do
-		match pb_solution.(t - first + offset) with
-		| Positive ->
-		   (if !time = -1
-		    then time:=t
-		    else failwith "duplicate time in pseudo boolean solution")
-		| Negative -> ()
-		| Unknown -> failwith "unknown value in pseudo boolean solution"
-	      done;
-	      (if !time = -1
-	       then failwith "no time in pseudo boolean solution");
-	      !time
-	    ) mapper.mapper_var_offsets;;
-  
-let pseudo_boolean_read_solution mapper channel =
-  let optimum = ref (-1)
-  and optimum_found = ref false
-  and solution = Array.make mapper.mapper_nr_pb_variables Unknown in
-  try
-    while true do
-      match input_line channel with
-      | "" -> ()
-      | line ->
-	 begin
-	   match String.get line 0 with
-	   | 'c' -> ()
-	   | 'o' ->
-	      assert ((String.length line) >= 2);
-	      assert ((String.get line 1) = ' ');
-	      optimum := int_of_string (String.sub line 2 ((String.length line)-2))
-	   | 's' -> (match line with
-		     | "s OPTIMUM FOUND" -> optimum_found := true
-		     | "s SATISFIABLE" -> ()
-		     | "s UNSATISFIABLE" -> close_in channel;
-		                            raise Unschedulable
-                     | _ -> failwith line)
-	   | 'v' -> line_to_pb_solution solution line mapper.mapper_nr_pb_variables
-	   | x -> Printf.printf "unknown: %s\n" line
-	 end
-    done;
-    assert false
-  with End_of_file ->
-       close_in channel;
-       begin
-	 let sol = pb_solution_to_schedule mapper solution in
-	 sol
-       end;;
-
-let recompute_max_latency mapper solution =
-  let maxi = ref (-1) in
-  for i=0 to (mapper.mapper_nr_instructions-1)
-  do
-    maxi := int_max !maxi (1+solution.(i))
-  done;
-  List.iter (fun (i, latency) ->
-      maxi := int_max !maxi (solution.(i) + latency)) mapper.mapper_final_predecessors;
-  !maxi;;
-  
-let adjust_check_solution mapper solution =
-  match mapper.mapper_pb_type with
-  | OPTIMIZATION ->
-     let max_latency = recompute_max_latency mapper solution in
-     assert (max_latency = solution.(mapper.mapper_nr_instructions));
-     solution
-  | SATISFIABILITY ->
-     let max_latency = recompute_max_latency mapper solution in
-     Array.init (mapper.mapper_nr_instructions+1)
-       (fun i -> if i < mapper.mapper_nr_instructions
-                 then solution.(i)
-                 else max_latency);;
-
-(* let pseudo_boolean_solver = ref "/local/monniaux/progs/naps/naps" *)
-(* let pseudo_boolean_solver = ref "/local/monniaux/packages/sat4j/org.sat4j.pb.jar CuttingPlanes" *)
-
-(* let pseudo_boolean_solver = ref "java -jar /usr/share/java/org.sat4j.pb.jar CuttingPlanes" *)
-(* let pseudo_boolean_solver = ref "java -jar /usr/share/java/org.sat4j.pb.jar" *)
-(* let pseudo_boolean_solver = ref "clasp" *)
-(* let pseudo_boolean_solver = ref "/home/monniaux/progs/CP/open-wbo/open-wbo_static -formula=1" *)
-(* let pseudo_boolean_solver = ref "/home/monniaux/progs/CP/naps/naps" *)
-(* let pseudo_boolean_solver = ref "/home/monniaux/progs/CP/minisatp/build/release/bin/minisatp" *)
-(* let pseudo_boolean_solver = ref "java -jar sat4j-pb.jar CuttingPlanesStar" *)
-let pseudo_boolean_solver = ref "pb_solver"
-
-let pseudo_boolean_scheduler pb_type problem =
-  try
-    let filename_in = "problem.opb" in
-    (* needed only if not using stdout and filename_out = "problem.sol" *)
-    let mapper =
-      with_out_channel (open_out filename_in)
-        (fun opb_problem ->
-          pseudo_boolean_print_problem opb_problem problem pb_type) in
-    Some (with_in_channel
-      (Unix.open_process_in (!pseudo_boolean_solver ^ " " ^ filename_in))
-      (fun opb_solution -> adjust_check_solution mapper (pseudo_boolean_read_solution mapper opb_solution)))
-  with
-  | Unschedulable -> None;;
-				 
-let rec reoptimizing_scheduler (scheduler : scheduler) (previous_solution : solution) (problem : problem) =
-  if (get_max_latency previous_solution)>1 then
-    begin
-      Printf.printf "reoptimizing < %d\n" (get_max_latency previous_solution);
-      flush stdout;
-      match scheduler
-              { problem with max_latency = (get_max_latency previous_solution)-1 }
-      with
-      | None -> previous_solution
-      | Some solution -> reoptimizing_scheduler scheduler solution problem
-    end
-  else previous_solution;;
-
-let smt_var i = Printf.sprintf "t%d" i
-
-let is_resource_used problem j =
-  try
-    Array.iter (fun usages ->
-        if usages.(j) > 0
-        then raise Exit) problem.instruction_usages;
-    false
-  with Exit -> true;;
-
-let smt_use_quantifiers = false
-                        
-let smt_print_problem channel problem =
-  let nr_instructions = get_nr_instructions problem in
-  let gen_smt_resource_constraint time j =
-        output_string channel "(<= (+";
-        Array.iteri
-          (fun i usages ->
-            let usage=usages.(j) in
-            if usage > 0
-            then Printf.fprintf channel " (ite (= %s %s) %d 0)"
-                   time (smt_var i) usage)
-          problem.instruction_usages;
-        Printf.fprintf channel ") %d)" problem.resource_bounds.(j)
-  in
-  output_string channel "(set-option :produce-models true)\n"; 
-  for i=0 to nr_instructions
-  do
-    Printf.fprintf channel "(declare-const %s Int)\n" (smt_var i);
-    Printf.fprintf channel "(assert (>= %s 0))\n" (smt_var i)
-  done;
-  for i=0 to nr_instructions-1
-  do
-    Printf.fprintf channel "(assert (< %s %s))\n"
-      (smt_var i) (smt_var nr_instructions)
-  done;
-  (if problem.max_latency > 0
-   then Printf.fprintf channel "(assert (<= %s %d))\n"
-          (smt_var nr_instructions) problem.max_latency);
-  List.iter (fun ctr ->
-      Printf.fprintf channel "(assert (>= (- %s %s) %d))\n"
-        (smt_var ctr.instr_to)
-        (smt_var ctr.instr_from)
-        ctr.latency) problem.latency_constraints;
-  for j=0 to (Array.length problem.resource_bounds)-1
-  do
-    if is_resource_used problem j
-    then
-      begin
-        if smt_use_quantifiers
-        then
-          begin
-            Printf.fprintf channel
-              "; resource #%d <= %d\n(assert (forall ((t Int)) "
-              j problem.resource_bounds.(j);
-            gen_smt_resource_constraint "t" j;
-            output_string channel "))\n"
-          end
-        else
-          begin
-            (if problem.max_latency < 0
-             then failwith "quantifier explosion needs max latency");
-            for t=0 to problem.max_latency
-            do
-              Printf.fprintf channel
-                "; resource #%d <= %d at t=%d\n(assert "
-                j problem.resource_bounds.(j) t;
-              gen_smt_resource_constraint (string_of_int t) j;
-              output_string channel ")\n"
-            done
-          end
-      end
-  done;
-  output_string channel "(check-sat)(get-model)\n";;
-      
-                  
-let ilp_print_problem channel problem pb_type =
-  let deadline = problem.max_latency in
-  assert (deadline > 0);
-  let nr_instructions = get_nr_instructions problem
-  and nr_resources = get_nr_resources problem
-  and successors = get_successors problem
-  and predecessors = get_predecessors problem in
-  let earliest_dates = get_earliest_dates predecessors
-  and latest_dates = get_latest_dates deadline successors in
-
-  let pb_var i t =
-    Printf.sprintf "x%d_%d" i t in
-
-  let gen_latency_constraint i_to i_from latency t_to =
-    Printf.fprintf channel "\\ t[%d] - t[%d] >= %d when t[%d]=%d\n"
-		   i_to i_from latency i_to t_to;
-    Printf.fprintf channel "c_%d_%d_%d_%d: "
-		   i_to i_from latency t_to;
-        for t_from=earliest_dates.(i_from) to
-              int_min latest_dates.(i_from) (t_to - latency)
-        do
-          Printf.fprintf channel "+1 %s " (pb_var i_from t_from)
-        done;
-        Printf.fprintf channel "-1 %s " (pb_var i_to t_to);
-        output_string channel ">= 0\n"
-
-  and gen_dual_latency_constraint i_to i_from latency t_from =
-    Printf.fprintf channel "\\ t[%d] - t[%d] >= %d when t[%d]=%d\n"
-      i_to i_from latency i_to t_from;
-    Printf.fprintf channel "d_%d_%d_%d_%d: "
-      i_to i_from latency t_from;
-        for t_to=int_max earliest_dates.(i_to) (t_from + latency)
-            to latest_dates.(i_to)
-        do
-          Printf.fprintf channel "+1 %s " (pb_var i_to t_to)
-        done;
-        Printf.fprintf channel "-1 %s " (pb_var i_from t_from);
-        Printf.fprintf channel ">= 0\n"
-
-  and gen_delta_constraint i_from i_to latency =
-    if delta_encoding
-    then  Printf.fprintf channel "l_%d_%d_%d: +1 t%d -1 t%d >= %d\n"
-            i_from i_to latency i_to i_from latency
-
-  in
-  
-  Printf.fprintf channel "\\ nr_instructions=%d deadline=%d\n" nr_instructions deadline;
-  begin
-    match pb_type with
-    | SATISFIABILITY -> output_string channel "Minimize dummy: 0\n"
-    | OPTIMIZATION ->
-       Printf.fprintf channel "Minimize\nmakespan: t%d\n" nr_instructions
-  end;
-  output_string channel "Subject To\n";
-  for i=0 to (match pb_type with
-              | OPTIMIZATION -> nr_instructions
-              | SATISFIABILITY -> nr_instructions-1)
-  do
-    let early = earliest_dates.(i) and late= latest_dates.(i) in
-    Printf.fprintf channel "\\ t[%d] in %d..%d\ntimes%d: " i early late i;
-    for t=early to late
-    do
-      Printf.fprintf channel "+1 %s " (pb_var i t)
-    done;
-    Printf.fprintf channel "= 1\n"
-  done;
-
-  for t=0 to deadline-1
-  do
-    for j=0 to nr_resources-1
-    do
-      let bound = problem.resource_bounds.(j)
-      and coeffs = ref [] in
-      for i=0 to nr_instructions-1
-      do
-        let usage = problem.instruction_usages.(i).(j) in
-        if t >= earliest_dates.(i) && t <= latest_dates.(i)
-           && usage > 0
-        then coeffs := (i, usage) :: !coeffs 
-      done;
-      if !coeffs <> [] then
-        begin
-          Printf.fprintf channel "\\ resource #%d at t=%d <= %d\nr%d_%d: " j t bound j t;
-          List.iter (fun (i, usage) ->
-              Printf.fprintf channel "%+d %s " (-usage) (pb_var i t)) !coeffs;
-          Printf.fprintf channel ">= %d\n" (-bound)
-        end
-    done
-  done;
-  
-  List.iter
-    (fun ctr ->
-      if ctr.instr_to < nr_instructions then
-        begin
-          gen_delta_constraint ctr.instr_from ctr.instr_to ctr.latency;
-          begin
-            if direct_encoding
-            then
-              for t_to=earliest_dates.(ctr.instr_to) to latest_dates.(ctr.instr_to)
-              do
-	        gen_latency_constraint ctr.instr_to ctr.instr_from ctr.latency t_to
-              done
-          end;
-          begin
-            if reverse_encoding
-            then
-              for t_from=earliest_dates.(ctr.instr_from) to latest_dates.(ctr.instr_from)
-              do
-	        gen_dual_latency_constraint ctr.instr_to ctr.instr_from ctr.latency t_from
-              done
-          end
-        end
-    ) problem.latency_constraints;
-  
-  begin
-    match pb_type with
-    | SATISFIABILITY -> ()
-    | OPTIMIZATION ->
-       let final_latencies = Array.make nr_instructions 1 in
-       List.iter (fun (i, latency) ->
-	   final_latencies.(i) <- int_max final_latencies.(i) latency)
-	 predecessors.(nr_instructions);
-       for i_from = 0 to nr_instructions -1
-       do
-	 gen_delta_constraint i_from nr_instructions final_latencies.(i_from)
-       done;
-       for t_to=earliest_dates.(nr_instructions) to deadline
-       do
-         for i_from = 0 to nr_instructions -1
-         do
-	   gen_latency_constraint nr_instructions i_from final_latencies.(i_from) t_to
-         done
-       done
-  end;
-  for i=0 to (match pb_type with
-              | OPTIMIZATION -> nr_instructions
-              | SATISFIABILITY -> nr_instructions-1)
-  do
-    Printf.fprintf channel "ct%d : -1 t%d" i i;
-    let early = earliest_dates.(i) and late= latest_dates.(i) in
-    for t=early to late do
-      Printf.fprintf channel " +%d %s" t (pb_var i t)
-    done;
-    output_string channel " = 0\n"
-  done;
-  output_string channel "Bounds\n";
-  for i=0 to (match pb_type with
-              | OPTIMIZATION -> nr_instructions
-              | SATISFIABILITY -> nr_instructions-1)
-  do
-    let early = earliest_dates.(i) and late= latest_dates.(i) in
-    begin
-      Printf.fprintf channel "%d <= t%d <= %d\n" early i late;
-      if true then
-        for t=early to late do
-          Printf.fprintf channel "0 <= %s <= 1\n" (pb_var i t)
-        done
-    end
-  done;
-  output_string channel "Integer\n";
-  for i=0 to (match pb_type with
-              | OPTIMIZATION -> nr_instructions
-              | SATISFIABILITY -> nr_instructions-1)
-  do
-    Printf.fprintf channel "t%d " i
-  done;
-  output_string channel "\nBinary\n";
-  for i=0 to (match pb_type with
-              | OPTIMIZATION -> nr_instructions
-              | SATISFIABILITY -> nr_instructions-1)
-  do
-    let early = earliest_dates.(i) and late= latest_dates.(i) in
-    for t=early to late do
-      output_string channel (pb_var i t);
-      output_string channel " "
-    done;
-    output_string channel "\n"
-  done;
-  output_string channel "End\n";
-  {
-    mapper_pb_type = pb_type;
-    mapper_nr_instructions = nr_instructions;
-    mapper_nr_pb_variables = 0;
-    mapper_earliest_dates = earliest_dates;
-    mapper_latest_dates = latest_dates;
-    mapper_var_offsets = [| |];
-    mapper_final_predecessors = predecessors.(nr_instructions)
-  };;
-
-(* Guess what? Cplex sometimes outputs 11.000000004 instead of integer 11 *)
-
-let positive_float_round x = truncate (x +. 0.5)
-                           
-let float_round (x : float) : int =
-  if x > 0.0
-  then positive_float_round x
-  else - (positive_float_round (-. x))
-  
-let rounded_int_of_string x =  float_round (float_of_string x)
-                             
-let ilp_read_solution mapper channel =
-  let times = Array.make
-                (match mapper.mapper_pb_type with
-                 | OPTIMIZATION -> 1+mapper.mapper_nr_instructions
-                 | SATISFIABILITY -> mapper.mapper_nr_instructions) (-1) in
-  try
-    while true do
-      let line = input_line channel in
-      ( if (String.length line) < 3
-        then failwith (Printf.sprintf "bad ilp output: length(line) < 3: %s" line));
-      match String.get line 0 with
-      | 'x' -> ()
-      | 't' -> let space =
-                 try String.index line ' '
-                 with Not_found ->
-                   failwith "bad ilp output: no t variable number"
-               in
-               let tnumber =
-                 try int_of_string (String.sub line 1 (space-1))
-                 with Failure _ ->
-                   failwith "bad ilp output: not a variable number"
-               in
-               (if tnumber < 0 || tnumber >= (Array.length times)
-                then failwith (Printf.sprintf "bad ilp output: not a correct variable number: %d (%d)" tnumber (Array.length times)));
-               let value =
-                 let s = String.sub line (space+1) ((String.length line)-space-1) in
-                 try rounded_int_of_string s
-                 with Failure _ ->
-                   failwith (Printf.sprintf "bad ilp output: not a time number (%s)" s)
-               in
-               (if value < 0
-                then failwith "bad ilp output: negative time");
-               times.(tnumber) <- value
-      | '#' -> ()
-      | '0' -> ()
-      | _ -> failwith (Printf.sprintf "bad ilp output: bad variable initial, line = %s" line)
-    done;
-    assert false
-  with End_of_file ->
-    Array.iteri (fun i x ->
-        if i<(Array.length times)-1
-           && x<0 then raise Unschedulable) times;
-    times;;
-
-let ilp_solver = ref "ilp_solver"
-
-let problem_nr = ref 0
-
-let ilp_scheduler pb_type problem =
-  try
-    let filename_in = Printf.sprintf  "problem%05d.lp" !problem_nr
-    and filename_out = Printf.sprintf "problem%05d.sol" !problem_nr in
-    incr problem_nr;
-    let mapper = with_out_channel (open_out filename_in)
-      (fun opb_problem -> ilp_print_problem opb_problem problem pb_type) in
-
-    begin
-      match Unix.system (!ilp_solver ^ " " ^ filename_in ^ " " ^ filename_out) with
-      | Unix.WEXITED 0 ->
-         Some (with_in_channel
-                 (open_in filename_out)
-                 (fun opb_solution ->
-                   adjust_check_solution mapper
-                     (ilp_read_solution mapper opb_solution)))
-      | Unix.WEXITED _ -> failwith "failed to start ilp solver"
-      | _ -> None
-    end
-  with
-  | Unschedulable -> None;;
-
-let current_utime_all () =
-  let t = Unix.times() in
-  t.Unix.tms_cutime +. t.Unix.tms_utime;;
-
-let utime_all_fn fn arg =
-  let utime_start = current_utime_all () in
-  let output = fn arg in
-  let utime_end = current_utime_all () in
-  (output, utime_end -. utime_start);;
-    
-let cascaded_scheduler (problem : problem) =
-  let (some_initial_solution, list_scheduler_time) =
-    utime_all_fn (validated_scheduler list_scheduler) problem in
-  match some_initial_solution with
-  | None -> None
-  | Some initial_solution ->
-     let (solution, reoptimizing_time) = utime_all_fn (reoptimizing_scheduler (validated_scheduler (ilp_scheduler SATISFIABILITY)) initial_solution) problem in
-     begin
-       let latency2 = get_max_latency solution
-       and latency1 = get_max_latency initial_solution in
-       Printf.printf "postpass %s: %d, %d, %d, %g, %g\n"
-		     (if latency2 < latency1 then "REOPTIMIZED" else "unchanged")
-		     (get_nr_instructions problem)
-		     latency1 latency2
-		     list_scheduler_time reoptimizing_time;
-       flush stdout
-     end;
-     Some solution;;
-
-let scheduler_by_name name =
-  match name with
-  | "ilp" -> validated_scheduler cascaded_scheduler
-  | "list" -> validated_scheduler list_scheduler
-  | "revlist" -> validated_scheduler reverse_list_scheduler
-  | "greedy" -> greedy_scheduler
-  | s -> failwith ("unknown scheduler: " ^ s);;
diff --git a/kvx/InstructionScheduler.mli b/kvx/InstructionScheduler.mli
deleted file mode 100644
index 85e2a5c6..00000000
--- a/kvx/InstructionScheduler.mli
+++ /dev/null
@@ -1,113 +0,0 @@
-(** Schedule instructions on a synchronized pipeline
-by David Monniaux, CNRS, VERIMAG *)
-
-(** A latency constraint: instruction number [instr_to] should be scheduled at least [latency] clock ticks before [instr_from].
-
-It is possible to specify [latency]=0, meaning that [instr_to] can be scheduled at the same clock tick as [instr_from], but not before.
-
-[instr_to] can be the special value equal to the number of instructions, meaning that it refers to the final output latency. *)
-type latency_constraint = {
-  instr_from : int;
-  instr_to : int;
-  latency : int;
-  }
-                        
-(** A scheduling problem.
-
-In addition to the latency constraints, the resource constraints should be satisfied: at every clock tick, the sum of vectors of resources used by the instructions scheduled at that tick does not exceed the resource bounds.
-*)
-type problem = {
-    max_latency : int;
-    (** An optional maximal total latency of the problem, after which the problem is deemed not schedulable. -1 means there should be no maximum. *)
-
-    resource_bounds : int array;
-    (** An array of number of units available indexed by the kind of resources to be allocated. It can be empty, in which case the problem is scheduling without resource constraints. *)
-
-    instruction_usages: int array array;
-    (** At index {i i} the vector of resources used by instruction number {i i}. It must be the same length as [resource_bounds] *)
-
-    latency_constraints : latency_constraint list
-    (** The latency constraints that must be satisfied *)
-  };;
-
-(** Print problem for human readability. *)
-val print_problem : out_channel -> problem -> unit;;
-
-(** Scheduling solution. For {i n} instructions to schedule, and 0≤{i i}<{i n}, position {i i} contains the time to which instruction {i i} should be scheduled. Position {i n} contains the final output latency. *)
-type solution = int array
-              
-(** A scheduling algorithm.
-The return value [Some x] is a solution [x].
-[None] means that scheduling failed. *)
-type scheduler = problem -> solution option;;
-
-(* DISABLED
-(** Schedule the problem optimally by constraint solving using the Gecode solver. *)
-external gecode_scheduler : problem -> solution option
-  = "caml_gecode_schedule_instr"
- *)
-  
-(** Get the number the last scheduling time used for an instruction in a solution.
-@return The last clock tick used *)
-val maximum_slot_used : solution -> int
-
-(** Validate that a solution is truly a solution of a scheduling problem.
-@raise Failure if validation fails *)
-val check_schedule : problem -> solution -> unit
-
-(** Schedule the problem using a greedy list scheduling algorithm, from the start.
-The first (according to instruction ordering) instruction that is ready (according to the latency constraints) is scheduled at the current clock tick.
-Once a clock tick is full go to the next.
-
-@return [Some solution] when a solution is found, [None] if not. *)
-val list_scheduler : problem -> solution option
-
-(** Schedule the problem using the order of instructions without any reordering *)
-val greedy_scheduler : problem -> solution option
-
-(** Schedule a problem using a scheduler applied in the opposite direction, e.g. for list scheduling from the end instead of the start. BUGGY *)
-val schedule_reversed : scheduler -> problem -> int array option
-
-(** Schedule a problem from the end using a list scheduler. BUGGY *)
-val reverse_list_scheduler : problem -> int array option
-
-(** Check that a problem is well-formed.
-@raise Failure if validation fails *)
-val check_problem : problem -> unit
-  
-(** Apply a scheduler and validate the result against the input problem.
-@return The solution found
-@raise Failure if validation fails *)
-val validated_scheduler : scheduler -> problem -> solution option;;
-
-(** Get max latency from solution
-@return Max latency *)
-val get_max_latency : solution -> int;;
-
-(** Get the length of a maximal critical path
-@return Max length *)
-val maximum_critical_path : problem -> int;;
-
-(** Apply line scheduler then advanced solver
-@return A solution if found *)
-val cascaded_scheduler : problem -> solution option;;
-
-val show_date_ranges : problem -> unit;;
-
-type pseudo_boolean_problem_type =
-  | SATISFIABILITY
-  | OPTIMIZATION;;
-
-type pseudo_boolean_mapper
-val pseudo_boolean_print_problem : out_channel -> problem -> pseudo_boolean_problem_type -> pseudo_boolean_mapper;;
-val pseudo_boolean_read_solution : pseudo_boolean_mapper -> in_channel -> solution;;
-val pseudo_boolean_scheduler : pseudo_boolean_problem_type -> problem -> solution option;;
-
-val smt_print_problem : out_channel -> problem -> unit;;
-
-val ilp_print_problem : out_channel -> problem -> pseudo_boolean_problem_type -> pseudo_boolean_mapper;;
-
-val ilp_scheduler : pseudo_boolean_problem_type -> problem -> solution option;;
-
-(** Schedule a problem using a scheduler given by a string name *)
-val scheduler_by_name : string -> problem -> int array option;;
diff --git a/kvx/OpWeights.ml b/kvx/OpWeights.ml
new file mode 100644
index 00000000..23c2e5d3
--- /dev/null
+++ b/kvx/OpWeights.ml
@@ -0,0 +1,115 @@
+open Op;;
+open PostpassSchedulingOracle;;
+open PrepassSchedulingOracleDeps;;
+
+module KV3 =
+  struct
+let resource_bounds = PostpassSchedulingOracle.resource_bounds;;
+let nr_non_pipelined_units = 0;;
+
+let rec nlist_rec x l = function
+  | 0 -> l
+  | n when n > 0 -> nlist_rec x (x :: l) (n-1)
+  | _ -> failwith "nlist_rec";;
+let nlist x n = nlist_rec x [] n;;
+
+let bogus_register = Machregs.R0;;
+let bogus_inputs n = nlist bogus_register n;;
+
+let insns_of_op (op : operation) (nargs : int) =
+  match Asmblockgen.transl_op op
+          (bogus_inputs nargs) bogus_register [] with
+  | Errors.Error msg -> failwith "OpWeights.insns_of_op"
+  | Errors.OK insns -> insns;;
+
+let insn_of_op op nargs =
+  match insns_of_op op nargs with
+  | [] -> failwith "OpWeights.insn_of_op"
+  | h::_ -> h;;
+
+let insns_of_cond (cond : condition) (nargs : int) =
+  match Asmblockgen.transl_cond_op cond
+           Asmvliw.GPR0 (bogus_inputs nargs) [] with
+  | Errors.Error msg -> failwith "OpWeights.insns_of_cond"
+  | Errors.OK insns -> insns;;
+
+let insn_of_cond cond nargs =
+  match insns_of_cond cond nargs with
+  | [] -> failwith "OpWeights.insn_of_cond"
+  | h::_ -> h;;
+
+let insns_of_load trap chunk addressing (nargs : int) =
+  match Asmblockgen.transl_load trap chunk addressing
+          (bogus_inputs nargs) bogus_register [] with
+  | Errors.Error msg -> failwith "OpWeights.insns_of_load"
+  | Errors.OK insns -> insns;;
+
+let insn_of_load trap chunk addressing nargs =
+  match insns_of_load trap chunk addressing nargs with
+  | [] -> failwith "OpWeights.insn_of_load"
+  | h::_ -> h;;
+
+let insns_of_store chunk addressing (nargs : int) =
+  match Asmblockgen.transl_store chunk addressing
+          (bogus_inputs nargs) bogus_register [] with
+  | Errors.Error msg -> failwith "OpWeights.insns_of_store"
+  | Errors.OK insns -> insns;;
+
+let insn_of_store chunk addressing nargs =
+  match insns_of_store chunk addressing nargs with
+  | [] -> failwith "OpWeights.insn_of_store"
+  | h::_ -> h;;
+
+let latency_of_op (op : operation) (nargs : int) =
+  let insn = insn_of_op op nargs in
+  let record = basic_rec insn in
+  let latency = real_inst_to_latency record.inst in
+  latency;;
+
+let resources_of_op (op : operation) (nargs : int) =
+  let insn = insn_of_op op nargs in
+  let record = basic_rec insn in
+  rec_to_usage record;;
+  
+let non_pipelined_resources_of_op (op : operation) (nargs : int) = [| |]
+
+let resources_of_cond (cond : condition) (nargs : int) =
+  let insn = insn_of_cond cond nargs in
+  let record = basic_rec insn in
+  rec_to_usage record;;
+
+let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3;;
+let latency_of_call _ _ = 6;;
+
+let resources_of_load trap chunk addressing nargs =
+  let insn = insn_of_load trap chunk addressing nargs in
+  let record = basic_rec insn in
+  rec_to_usage record;;
+
+let resources_of_store chunk addressing nargs =
+  let insn = insn_of_store chunk addressing nargs in
+  let record = basic_rec insn in
+  rec_to_usage record;;
+
+let resources_of_call _ _ = resource_bounds;;
+let resources_of_builtin _ = resource_bounds;;
+  end;;
+
+let get_opweights () : opweights =
+  match !Clflags.option_mtune with
+  | "kv3" | "" ->
+     {
+       pipelined_resource_bounds = KV3.resource_bounds;
+       nr_non_pipelined_units = KV3.nr_non_pipelined_units;
+       latency_of_op = KV3.latency_of_op;
+       resources_of_op = KV3.resources_of_op;
+       non_pipelined_resources_of_op = KV3.non_pipelined_resources_of_op;
+       latency_of_load = KV3.latency_of_load;
+       resources_of_load = KV3.resources_of_load;
+       resources_of_store = KV3.resources_of_store;
+       resources_of_cond = KV3.resources_of_cond;
+       latency_of_call = KV3.latency_of_call;
+       resources_of_call = KV3.resources_of_call;
+       resources_of_builtin = KV3.resources_of_builtin
+     }
+  | xxx -> failwith (Printf.sprintf "unknown -mtune: %s" xxx);;
diff --git a/kvx/PrepassSchedulingOracle.ml b/kvx/PrepassSchedulingOracle.ml
new file mode 120000
index 00000000..912e9ffa
--- /dev/null
+++ b/kvx/PrepassSchedulingOracle.ml
@@ -0,0 +1 @@
+../aarch64/PrepassSchedulingOracle.ml
\ No newline at end of file
diff --git a/kvx/PrepassSchedulingOracleDeps.ml b/kvx/PrepassSchedulingOracleDeps.ml
new file mode 120000
index 00000000..1e955b85
--- /dev/null
+++ b/kvx/PrepassSchedulingOracleDeps.ml
@@ -0,0 +1 @@
+../aarch64/PrepassSchedulingOracleDeps.ml
\ No newline at end of file
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 8c834de5..7a301929 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1199,7 +1199,6 @@ Qed.
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
 Proof.
   red; intros until x. unfold cast8unsigned.
-
   rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate.
 Qed.
 
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v
index 122c9a60..87554258 100644
--- a/kvx/ValueAOp.v
+++ b/kvx/ValueAOp.v
@@ -16,87 +16,6 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op ExtValues ExtFloats RTL ValueDomain.
-
-Definition intoffloat_total (x: aval) :=
-  match x with
-  | F f =>
-      match Float.to_int f with
-      | Some i => I i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition intuoffloat_total (x: aval) :=
-  match x with
-  | F f =>
-      match Float.to_intu f with
-      | Some i => I i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition intofsingle_total (x: aval) :=
-  match x with
-  | FS f =>
-      match Float32.to_int f with
-      | Some i => I i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition intuofsingle_total (x: aval) :=
-  match x with
-  | FS f =>
-      match Float32.to_intu f with
-      | Some i => I i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition longoffloat_total (x: aval) :=
-  match x with
-  | F f =>
-      match Float.to_long f with
-      | Some i => L i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition longuoffloat_total (x: aval) :=
-  match x with
-  | F f =>
-      match Float.to_longu f with
-      | Some i => L i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition longofsingle_total (x: aval) :=
-  match x with
-  | FS f =>
-      match Float32.to_long f with
-      | Some i => L i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition longuofsingle_total (x: aval) :=
-  match x with
-  | FS f =>
-      match Float32.to_longu f with
-      | Some i => L i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
 Definition minf := binop_float ExtFloat.min.
 Definition maxf := binop_float ExtFloat.max.
 Definition minfs := binop_single ExtFloat32.min.
@@ -400,196 +319,6 @@ Hypothesis GENV: genv_match bc ge.
 Variable sp: block.
 Hypothesis STACK: bc sp = BCstack.
 
-Lemma intoffloat_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x).
-Proof.
-  unfold Val.intoffloat, intoffloat_total. intros.
-  inv MATCH; cbn in *; try constructor.
-  all: destruct (Float.to_int f) as [i|] eqn:E; cbn; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve intoffloat_total_sound : va.
-
-Lemma intuoffloat_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x).
-Proof.
-  unfold Val.intoffloat, intoffloat_total. intros.
-  inv MATCH; cbn in *; try constructor.
-  all: destruct (Float.to_intu f) as [i|] eqn:E; cbn; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve intuoffloat_total_sound : va.
-
-Lemma intofsingle_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x).
-Proof.
-  unfold Val.intofsingle, intofsingle_total. intros.
-  inv MATCH; cbn in *; try constructor.
-  all: destruct (Float32.to_int f) as [i|] eqn:E; cbn; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve intofsingle_total_sound : va.
-
-Lemma intuofsingle_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x).
-Proof.
-  unfold Val.intofsingle, intofsingle_total. intros.
-  inv MATCH; cbn in *; try constructor.
-  all: destruct (Float32.to_intu f) as [i|] eqn:E; cbn; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve intuofsingle_total_sound : va.
-
-Lemma singleofint_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x).
-Proof.
-  unfold Val.singleofint, singleofint; intros.
-  inv H; cbn.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve singleofint_total_sound : va.
-
-Lemma singleofintu_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x).
-Proof.
-  unfold Val.singleofintu, singleofintu; intros.
-  inv H; cbn.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve singleofintu_total_sound : va.
-
-Lemma longoffloat_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x).
-Proof.
-  unfold Val.longoffloat, longoffloat_total. intros.
-  inv MATCH; cbn in *; try constructor.
-  all: destruct (Float.to_long f) as [i|] eqn:E; cbn; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve longoffloat_total_sound : va.
-
-Lemma longuoffloat_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x).
-Proof.
-  unfold Val.longoffloat, longoffloat_total. intros.
-  inv MATCH; cbn in *; try constructor.
-  all: destruct (Float.to_longu f) as [i|] eqn:E; cbn; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve longuoffloat_total_sound : va.
-
-Lemma longofsingle_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x).
-Proof.
-  unfold Val.longofsingle, longofsingle_total. intros.
-  inv MATCH; cbn in *; try constructor.
-  all: destruct (Float32.to_long f) as [i|] eqn:E; cbn; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve longofsingle_total_sound : va.
-
-Lemma longuofsingle_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x).
-Proof.
-  unfold Val.longofsingle, longofsingle_total. intros.
-  inv MATCH; cbn in *; try constructor.
-  all: destruct (Float32.to_longu f) as [i|] eqn:E; cbn; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve longuofsingle_total_sound : va.
-
-Lemma singleoflong_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x).
-Proof.
-  unfold Val.singleoflong, singleoflong; intros.
-  inv H; cbn.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve singleoflong_total_sound : va.
-
-Lemma singleoflongu_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x).
-Proof.
-  unfold Val.singleoflongu, singleoflongu; intros.
-  inv H; cbn.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve singleoflongu_total_sound : va.
-
-Lemma floatoflong_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x).
-Proof.
-  unfold Val.floatoflong, floatoflong; intros.
-  inv H; cbn.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve floatoflong_total_sound : va.
-
-Lemma floatoflongu_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x).
-Proof.
-  unfold Val.floatoflongu, floatoflongu; intros.
-  inv H; cbn.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve floatoflongu_total_sound : va.
-
 Lemma minf_sound:
   forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y).
 Proof.
@@ -815,16 +544,6 @@ Proof.
     inv H1; cbn; try constructor.
     all: destruct Int.ltu; [cbn | constructor; fail].
     all: auto with va.
-  - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
-    | Vlong n2 => Vlong (Int64.add n n2)
-    | Vptr b2 ofs2 =>
-        if Archi.ptr64
-        then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n))
-        else Vundef
-    | _ => Vundef
-             end) with (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
-    + eauto with va.
-    + destruct a1; destruct shift; reflexivity.
   - inv H1; constructor.
   - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
     | Vlong n2 => Vlong (Int64.sub n n2)
@@ -832,10 +551,6 @@ Proof.
              end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
     + eauto with va.
     + destruct a1; destruct shift; reflexivity.
-  - (* shrxl *)
-    inv H1; cbn; try constructor.
-    all: destruct Int.ltu; [cbn | constructor; fail].
-    all: auto with va.
   - apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
 
   (* extfz *)
diff --git a/kvx/abstractbb/Impure/ImpConfig.v b/kvx/abstractbb/Impure/ImpConfig.v
deleted file mode 100644
index dd9785b5..00000000
--- a/kvx/abstractbb/Impure/ImpConfig.v
+++ /dev/null
@@ -1,85 +0,0 @@
-(** 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 !
-
-*)
-
-(* START COMMENT *)
- Module UnsafeImpure.
-
- Parameter unsafe_coerce: forall {A}, t A -> option A.
-
- Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=Some x -> mayRet k x.
-
- Extraction Inline unsafe_coerce.
-
- End UnsafeImpure.
-(* END COMMENT *)
-
-
-End ImpureView.
-
-
-Module Impure: ImpureView.
-
-  Include IdentityMonad.
-
-  Module UnsafeImpure.
-
-  Definition unsafe_coerce {A} (x:t A) := Some x.
-
-  Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=Some x -> mayRet k x.
-  Proof.
-    unfold unsafe_coerce, mayRet; congruence.
-  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.
diff --git a/kvx/abstractbb/Impure/ImpCore.v b/kvx/abstractbb/Impure/ImpCore.v
deleted file mode 100644
index 508b3f19..00000000
--- a/kvx/abstractbb/Impure/ImpCore.v
+++ /dev/null
@@ -1,196 +0,0 @@
-(** 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.
-
-Lemma wlp_option (A B: Type) (x: option A) (k1: A -> ??B) (k2: ??B)  (P: B -> Prop):
-  (forall a, x=Some a -> wlp (k1 a) P) -> 
-  (x=None -> wlp k2 P) -> 
-     (wlp (match x with Some a => k1 a | None => k2 end) P).
-Proof.
-  destruct x; simpl; auto.
-Qed.
-
-(* Tactics 
-
-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
- || apply wlp_option
- .
-
-(* 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).
diff --git a/kvx/abstractbb/Impure/ImpExtern.v b/kvx/abstractbb/Impure/ImpExtern.v
deleted file mode 100644
index 8fb3cf3b..00000000
--- a/kvx/abstractbb/Impure/ImpExtern.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(** Exporting Extern functions
-*)
-
-Require Export ImpPrelude.
-Require Export ImpIO.
-Require Export ImpLoops.
-Require Export ImpHCons.
diff --git a/kvx/abstractbb/Impure/ImpHCons.v b/kvx/abstractbb/Impure/ImpHCons.v
deleted file mode 100644
index 637116cc..00000000
--- a/kvx/abstractbb/Impure/ImpHCons.v
+++ /dev/null
@@ -1,199 +0,0 @@
-Require Export ImpIO.
-
-Import Notations.
-Local Open Scope impure.
-
-
-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".
-
-(**************************)
-(* (Weak) Sets            *)
-
-
-Import Dict.
-
-Axiom make_dict: forall {A B}, (hash_params A) -> ?? Dict.t A B.
-Extract Constant make_dict => "ImpHConsOracles.make_dict".
-
-
-Module Sets.
-
-Definition t {A} (mod: A -> Prop) := Dict.t A {x | mod x}.
-
-Definition empty {A} (hp: hash_params A) {mod:A -> Prop}: ?? t mod :=
-  make_dict hp.
-
-Program Fixpoint add {A} (l: list A) {mod: A -> Prop} (d: t mod): forall {H:forall x, List.In x l -> mod x}, ?? unit :=
-  match l with
-  | nil => fun H => RET ()
-  | x::l' => fun H =>
-    d.(set)(x,x);;
-    add l' d
-  end.
-
-Program Definition create {A} (hp: hash_params A) (l:list A): ?? t (fun x => List.In x l) :=
-  DO d <~ empty hp (mod:=fun x => List.In x l);;
-  add l (mod:=fun x => List.In x l) d (H:=_);;
-  RET d.
-Global Opaque create.
-
-Definition is_present {A} (hp: hash_params A) (x:A) {mod} (d:t mod): ?? bool :=
-  DO oy <~ (d.(get)) x;;
-  match oy with
-  | Some y => hp.(test_eq) x (`y)
-  | None => RET false
-  end.
-
-Local Hint Resolve test_eq_correct: wlp.
-
-Lemma is_present_correct A (hp: hash_params A) x mod (d:t mod):
- WHEN is_present hp x d ~> b THEN b=true -> mod x.
-Proof.
-  wlp_simplify; subst; eauto.
-  - apply proj2_sig.
-  - discriminate. 
-Qed.
-Hint Resolve is_present_correct: wlp.
-Global Opaque is_present.
-
-Definition msg_assert_incl: pstring := "Sets.assert_incl".
-
-Fixpoint assert_incl {A} (hp: hash_params A) (l: list A) {mod} (d:t mod): ?? unit :=
-  match l with
-  | nil => RET ()
-  | x::l' =>
-    DO b <~ is_present hp x d;;
-    if b then
-      assert_incl hp l' d
-    else (
-      hp.(log) x;;
-      FAILWITH msg_assert_incl
-    )
-  end.
-
-Lemma assert_incl_correct A (hp: hash_params A) l mod (d:t mod):
- WHEN assert_incl hp l d ~> _ THEN forall x, List.In x l -> mod x.
-Proof.
-  induction l; wlp_simplify; subst; eauto.
-Qed.
-Hint Resolve assert_incl_correct: wlp.
-Global Opaque assert_incl.
-
-Definition assert_list_incl {A} (hp: hash_params A) (l1 l2: list A): ?? unit :=
-  (* println "";;print("dict_create ");;*)
-  DO d <~ create hp l2;;
-  (*print("assert_incl ");;*)
-  assert_incl hp l1 d.
-
-Lemma assert_list_incl_correct A (hp: hash_params A) l1 l2:
- WHEN assert_list_incl hp l1 l2 ~> _ THEN List.incl l1 l2.
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque assert_list_incl.
-Hint Resolve assert_list_incl_correct: wlp.
-
-End Sets.
-
-
-
-
-(********************************)
-(* (Weak) HConsing              *)
-
-Module HConsing.
-
-Export HConsingDefs.
-
-(* NB: this axiom is NOT intended to be called directly, but only through [hCons...] functions below. *)
-Axiom xhCons: forall {A}, (hashP A) -> ?? hashConsing A.
-Extract Constant xhCons => "ImpHConsOracles.xhCons".
-
-Definition hCons_eq_msg: pstring := "xhCons: hash eq differs".
-
-Definition hCons {A} (hp: hashP A): ?? (hashConsing A) :=
-  DO hco <~ xhCons hp ;;
-  RET {|
-      hC := (fun x =>
-         DO x' <~ hC hco x ;;
-         DO b0 <~ hash_eq hp x.(hdata) x' ;;
-         assert_b b0 hCons_eq_msg;;
-         RET x');
-      next_hid := hco.(next_hid);
-      next_log := hco.(next_log);
-      export := hco.(export);
-      remove := hco.(remove)
-      |}.
-
-
-Lemma hCons_correct A (hp: hashP A):
-  WHEN hCons hp ~> hco THEN
-    (forall x y, WHEN hp.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hp x)=(ignore_hid hp y)) ->
-    forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hp x.(hdata)=ignore_hid hp x'.
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque hCons.
-Hint Resolve hCons_correct: wlp.
-
-
-
-(* hashV: extending a given type with hash-consing *)
-Record hashV {A:Type}:= {
-  data: A;
-  hid: hashcode
-}.
-Arguments hashV: clear implicits.
-
-Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashP (hashV A) := {|
-  hash_eq := fun v1 v2 => test_eq v1.(data) v2.(data);
-  get_hid := hid;
-  set_hid := fun v id => {| data := v.(data); hid := id |}
-|}.
-
-Definition liftHV (x:nat) := {| data := x; hid := unknown_hid |}.
-
-Definition hConsV {A} (hasheq: A -> A -> ?? bool): ?? (hashConsing (hashV A)) :=
-  hCons (hashV_C hasheq).
-
-Lemma hConsV_correct A (hasheq: A -> A -> ?? bool):
-  WHEN hConsV hasheq ~> hco THEN
-    (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> 
-    forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data).
-Proof.
-  Local Hint Resolve f_equal2: core.
-  wlp_simplify.
-  exploit H; eauto.
-  + wlp_simplify.
-  + intros; congruence.
-Qed.
-Global Opaque hConsV.
-Hint Resolve hConsV_correct: wlp.
-
-Definition hC_known {A} (hco:hashConsing (hashV A)) (unknownHash_msg: hashinfo (hashV A) -> ?? pstring) (x:hashinfo (hashV A)): ?? hashV A :=
-  DO clock <~ hco.(next_hid)();;
-  DO x' <~ hco.(hC) x;;
-  DO ok <~ hash_older x'.(hid) clock;;
-  if ok 
-  then RET x'
-  else
-    hco.(remove) x;; 
-    DO msg <~ unknownHash_msg x;;
-    FAILWITH msg.
-
-Lemma hC_known_correct A (hco:hashConsing (hashV A)) msg x:
-  WHEN hC_known hco msg x ~> x' THEN
-    (forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data)) ->
-    x.(hdata).(data)=x'.(data).
-Proof.
-  wlp_simplify.
-  unfold wlp in * |- ; eauto.
-Qed.
-Global Opaque hC_known.
-Hint Resolve hC_known_correct: wlp.
-
-End HConsing.
diff --git a/kvx/abstractbb/Impure/ImpIO.v b/kvx/abstractbb/Impure/ImpIO.v
deleted file mode 100644
index 6c02c395..00000000
--- a/kvx/abstractbb/Impure/ImpIO.v
+++ /dev/null
@@ -1,159 +0,0 @@
-(** 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/kvx/abstractbb/Impure/ImpLoops.v b/kvx/abstractbb/Impure/ImpLoops.v
deleted file mode 100644
index 33376c19..00000000
--- a/kvx/abstractbb/Impure/ImpLoops.v
+++ /dev/null
@@ -1,123 +0,0 @@
-(** 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".
-
-
-Section While_Loop.
-
-(** Local Definition of "while-loop-invariant" *)
-Let wli {S} cond body (I: S -> Prop) := forall s, I s -> cond s = true -> WHEN (body s) ~> s' THEN I s'.
-
-Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | (I s0 -> I s) /\ cond s = false}
-  := loop (A:={s | I s0 -> I s})
-       (s0, 
-          fun s =>
-          match (cond s) with
-          | true => 
-             DO s' <~ mk_annot (body s) ;; 
-             RET (inl (A:={s | I s0 -> I s }) s')
-          | false => 
-             RET (inr (B:={s | (I s0 -> I s) /\ cond s = false}) s)
-          end).
-Obligation 2.
-  unfold wli, wlp in * |-; eauto.
-Qed.
-Extraction Inline while.
-
-End While_Loop.
-
-
-Section Loop_Until_None.
-(** useful to demonstrate a UNSAT property *)
-
-(** Local Definition of "loop-until-None-invariant" *)
-Let luni {S} (body: S -> ?? (option S)) (I: S -> Prop) := forall s, I s -> WHEN (body s) ~> s' THEN match s' with Some s1 => I s1 | None => False end.
-
-Program Definition loop_until_None {S} body (I: S -> Prop | luni body I) s0: ?? ~(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 (H2 s _ _ H0). auto.
-Qed.
-Obligation 3.
-  intros X; refine (H1 s _ _ H). auto.
-Qed.
-Extraction Inline loop_until_None.
-
-End 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) (k: A -> ?? answ R) x:
- 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 := `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/kvx/abstractbb/Impure/ImpMonads.v b/kvx/abstractbb/Impure/ImpMonads.v
deleted file mode 100644
index f01a2755..00000000
--- a/kvx/abstractbb/Impure/ImpMonads.v
+++ /dev/null
@@ -1,148 +0,0 @@
-(** 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/kvx/abstractbb/Impure/ImpPrelude.v b/kvx/abstractbb/Impure/ImpPrelude.v
deleted file mode 100644
index de4c7973..00000000
--- a/kvx/abstractbb/Impure/ImpPrelude.v
+++ /dev/null
@@ -1,206 +0,0 @@
-Require Export String.
-Require Export List.
-Require Extraction.
-Require Import Ascii.
-Require Import BinNums.
-Require Export ImpCore.
-Require Export PArith.
-
-
-Import Notations.
-Local Open Scope impure.
-
-(** Impure lazy andb of booleans *)
-Definition iandb (k1 k2: ??bool): ?? bool :=
-  DO r1 <~ k1 ;;
-  if r1 then k2 else RET false.
-
-Extraction Inline iandb. (* Juste pour l'efficacité à l'extraction ! *)
-
-(** Strings for pretty-printing *)
-
-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 *)
-
-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  *)
-
-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.
-
-
-(* 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.
-
-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.
-
-Extract Inlined Constant phys_eq => "(==)".
-Hint Resolve phys_eq_correct: wlp.
-
-
-Axiom struct_eq: forall {A}, A -> A -> ?? bool.
-Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN if b then x=y else x<>y.
-Extract Inlined Constant struct_eq => "(=)".
-Hint Resolve struct_eq_correct: wlp.
-
-
-(** Data-structure for generic hash-consing *)
-
-Axiom hashcode: Type.
-Extract Constant hashcode => "int".
-
-(* NB: hashConsing is assumed to generate hash-code in ascending order.
-   This gives a way to check that a hash-consed value is older than an other one.
-*)
-Axiom hash_older: hashcode -> hashcode -> ?? bool.
-Extract Inlined Constant hash_older => "(<)".
-
-Module Dict.
-
-Record hash_params {A:Type} := {
-  test_eq: A -> A -> ??bool;
-  test_eq_correct: forall x y, WHEN test_eq x y ~> r THEN r=true -> x=y;
-  hashing: A -> ??hashcode;
-  log: A -> ??unit (* for debugging only *)
-}.
-Arguments hash_params: clear implicits.
-
-
-Record t {A B:Type} := {
-  set: A * B -> ?? unit;
-  get: A -> ?? option B
-}.
-Arguments t: clear implicits.
-
-End Dict.
-
-Module HConsingDefs.
-
-Record hashinfo {A: Type} := {
-  hdata: A;
-  hcodes: list hashcode;
-}.
-Arguments hashinfo: clear implicits.
-
-(* for inductive types with intrinsic hash-consing *)
-Record hashP {A:Type}:= {
-  hash_eq: A -> A -> ?? bool;
-  get_hid: A -> hashcode;
-  set_hid: A -> hashcode -> A; (* WARNING: should only be used by hash-consing machinery *)
-}.
-Arguments hashP: clear implicits.
-
-Axiom unknown_hid: hashcode.
-Extract Constant unknown_hid => "-1".
-
-Definition ignore_hid {A} (hp: hashP A) (hv:A) := set_hid hp hv unknown_hid.
-
-Record hashExport {A:Type}:= {
-  get_info: hashcode -> ?? hashinfo A;
-  iterall: ((list pstring) -> hashcode -> hashinfo A -> ?? unit) -> ?? unit; (* iter on all elements in the hashtbl, by order of creation *)
-}.
-Arguments hashExport: clear implicits.
-
-Record hashConsing {A:Type}:= {
-  hC: hashinfo A -> ?? A;
-  (**** below: debugging or internal functions ****)
-  next_hid: unit -> ?? hashcode; (* should be strictly less old than ignore_hid *)
-  remove: hashinfo A -> ??unit; (* SHOULD NOT BE USED ! *)
-  next_log: pstring -> ?? unit; (* insert a log info (for the next introduced element) -- regiven by [iterall export] below *)
-  export: unit -> ?? hashExport A ; 
-}.
-Arguments hashConsing: clear implicits.
-
-End HConsingDefs.
-
-(** recMode: this is mainly for Tests ! *)
-Inductive recMode:= StdRec | MemoRec | BareRec | BuggyRec.
-
-
-(* 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/kvx/abstractbb/Impure/LICENSE b/kvx/abstractbb/Impure/LICENSE
deleted file mode 100644
index 65c5ca88..00000000
--- a/kvx/abstractbb/Impure/LICENSE
+++ /dev/null
@@ -1,165 +0,0 @@
-                   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/kvx/abstractbb/Impure/README.md b/kvx/abstractbb/Impure/README.md
deleted file mode 100644
index 2b19d14a..00000000
--- a/kvx/abstractbb/Impure/README.md
+++ /dev/null
@@ -1,31 +0,0 @@
-# `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/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml
deleted file mode 100644
index 2b66899b..00000000
--- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml
+++ /dev/null
@@ -1,66 +0,0 @@
-open ImpPrelude
-open HConsingDefs
-
-let make_dict (type key) (p: key Dict.hash_params) =
-  let module MyHashedType = struct
-    type t = key
-    let equal = p.Dict.test_eq 
-    let hash = p.Dict.hashing 
-  end in
-  let module MyHashtbl = Hashtbl.Make(MyHashedType) in
-  let dict = MyHashtbl.create 1000 in
-  {
-    Dict.set = (fun (k,d) -> MyHashtbl.replace dict k d);
-    Dict.get = (fun k -> MyHashtbl.find_opt dict k)
-  }
-
-
-exception Stop;;
-
-let xhCons (type a) (hp:a hashP) =
-  (* We use a hash-table, but a hash-set would be sufficient !                    *)
-  (* Thus, we could use a weak hash-set, but prefer avoid it for easier debugging *)
-  (* Ideally, a parameter would allow to select between the weak or full version  *)
-  let module MyHashedType = struct
-    type t = a hashinfo
-    let equal x y = hp.hash_eq x.hdata y.hdata
-    let hash x = Hashtbl.hash x.hcodes 
-  end in
-  let module MyHashtbl = Hashtbl.Make(MyHashedType) in
-  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 (k:a hashinfo) ->
-     match MyHashtbl.find_opt t k with
-     | Some d -> d
-     | None -> (*print_string "+";*)
-        let d = hp.set_hid k.hdata (MyHashtbl.length t) in
-        MyHashtbl.add t {k with hdata = d } d; d);
-   next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs));
-   next_hid = (fun () -> MyHashtbl.length t);
-   remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x);
-   export = fun () ->
-     match pick t with
-     | None -> { get_info = (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.(hp.get_hid d) <- k) t;
-           {
-             get_info = (fun i -> a.(i));
-             iterall = (fun iter_node -> Array.iteri (fun i k -> iter_node (step_log i) i k) a)
-           }    
-  }
diff --git a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli
deleted file mode 100644
index 5075d176..00000000
--- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli
+++ /dev/null
@@ -1,5 +0,0 @@
-open ImpPrelude
-open HConsingDefs
-
-val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t
-val xhCons: 'a hashP -> 'a hashConsing
diff --git a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml
deleted file mode 100644
index 9e63c12d..00000000
--- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml
+++ /dev/null
@@ -1,142 +0,0 @@
-(* 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 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 (Stdlib.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) = BinInt.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/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli
deleted file mode 100644
index 6064286a..00000000
--- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-open ImpPrelude
-
-
-(* 
-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/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml
deleted file mode 100644
index cb7625e5..00000000
--- a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-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/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli
deleted file mode 100644
index 194696a1..00000000
--- a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli
+++ /dev/null
@@ -1,8 +0,0 @@
-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 )