Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass

18 files changed, 1802 insertions, 0 deletions

diff --git a/lib/Impure/ImpConfig.v b/lib/Impure/ImpConfig.v
new file mode 100644
index 00000000..dd9785b5
--- /dev/null
+++ b/lib/Impure/ImpConfig.v
@@ -0,0 +1,85 @@
+(** 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/lib/Impure/ImpCore.v b/lib/Impure/ImpCore.v
new file mode 100644
index 00000000..508b3f19
--- /dev/null
+++ b/lib/Impure/ImpCore.v
@@ -0,0 +1,196 @@
+(** 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/lib/Impure/ImpExtern.v b/lib/Impure/ImpExtern.v
new file mode 100644
index 00000000..8fb3cf3b
--- /dev/null
+++ b/lib/Impure/ImpExtern.v
@@ -0,0 +1,7 @@
+(** Exporting Extern functions
+*)
+
+Require Export ImpPrelude.
+Require Export ImpIO.
+Require Export ImpLoops.
+Require Export ImpHCons.
diff --git a/lib/Impure/ImpHCons.v b/lib/Impure/ImpHCons.v
new file mode 100644
index 00000000..637116cc
--- /dev/null
+++ b/lib/Impure/ImpHCons.v
@@ -0,0 +1,199 @@
+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/lib/Impure/ImpIO.v b/lib/Impure/ImpIO.v
new file mode 100644
index 00000000..6c02c395
--- /dev/null
+++ b/lib/Impure/ImpIO.v
@@ -0,0 +1,159 @@
+(** Extension of Coq language with some IO and exception-handling operators.
+
+TODO: integration with http://coq.io/ ?
+
+*)
+
+Require Export ImpPrelude.
+
+Import Notations.
+Local Open Scope impure.
+
+(** Printing functions *)
+
+Axiom print: pstring -> ?? unit.
+Extract Constant print => "ImpIOOracles.print".
+
+Axiom println: pstring -> ?? unit.
+Extract Constant println => "ImpIOOracles.println".
+
+Axiom read_line: unit -> ?? pstring.
+Extract Constant read_line => "ImpIOOracles.read_line".
+
+Require Import ZArith.
+Axiom string_of_Z: Z -> ?? pstring.
+Extract Constant string_of_Z => "ImpIOOracles.string_of_Z".
+
+(** timer *)
+
+Axiom timer: forall {A B}, (A -> ?? B)*A -> ?? B.
+Extract Constant timer => "ImpIOOracles.timer".
+
+(** Exception Handling *)
+
+Axiom exit_observer: Type.
+Extract Constant exit_observer => "((unit -> unit) ref)".
+
+Axiom new_exit_observer: (unit -> ??unit) -> ??exit_observer.
+Extract Constant new_exit_observer => "ImpIOOracles.new_exit_observer".
+
+Axiom set_exit_observer: exit_observer * (unit -> ??unit) -> ??unit.
+Extract Constant set_exit_observer => "ImpIOOracles.set_exit_observer".
+
+Axiom exn: Type.
+Extract Inlined Constant exn => "exn".
+
+Axiom raise: forall {A}, exn -> ?? A.
+Extract Constant raise => "raise".
+
+Axiom exn2string: exn -> ?? pstring.
+Extract Constant exn2string => "ImpIOOracles.exn2string".
+
+Axiom fail: forall {A}, pstring -> ?? A.
+Extract Constant fail => "ImpIOOracles.fail".
+
+Axiom try_with_fail: forall {A}, (unit -> ?? A) * (pstring -> exn -> ??A) -> ??A.
+Extract Constant try_with_fail => "ImpIOOracles.try_with_fail".
+
+Axiom try_with_any: forall {A}, (unit -> ?? A) * (exn -> ??A) -> ??A.
+Extract Constant try_with_any => "ImpIOOracles.try_with_any".
+
+Notation "'RAISE' e" := (DO r <~ raise (A:=False) e ;; RET (match r with end)) (at level 0): impure_scope.
+Notation "'FAILWITH' msg" := (DO r <~ fail (A:=False) msg ;; RET (match r with end)) (at level 0): impure_scope.
+
+Definition _FAILWITH {A:Type} msg: ?? A := FAILWITH msg.
+
+Example _FAILWITH_correct A msg (P: A -> Prop):
+  WHEN _FAILWITH msg ~> r THEN P r.
+Proof.
+  wlp_simplify.
+Qed.
+
+Notation "'TRY' k1 'WITH_FAIL' s ',' e '=>' k2" := (try_with_fail (fun _ => k1, fun s e => k2))
+    (at level 55, k1 at level 53, right associativity): impure_scope.
+
+Notation "'TRY' k1 'WITH_ANY' e '=>' k2" := (try_with_any (fun _ => k1, fun e => k2))
+    (at level 55, k1 at level 53, right associativity): impure_scope.
+
+
+Program Definition assert_b (b: bool) (msg: pstring): ?? b=true :=
+  match b with
+  | true => RET _
+  | false => FAILWITH msg
+  end.
+
+Lemma assert_wlp_true msg b: WHEN assert_b b msg ~> _ THEN b=true.
+Proof.
+  wlp_simplify.
+Qed.
+
+Lemma assert_false_wlp msg (P: Prop): WHEN assert_b false msg ~> _ THEN P.
+Proof.
+  simpl; wlp_simplify.
+Qed.
+
+Program Definition try_catch_fail_ensure {A} (k1: unit -> ?? A) (k2: pstring -> exn -> ??A) (P: A -> Prop | wlp (k1 tt) P /\ (forall s e, wlp (k2 s e) P)): ?? { r | P r }
+  := TRY
+        DO r <~ mk_annot (k1 tt);; 
+        RET (exist P r _)
+     WITH_FAIL s, e => 
+        DO r <~ mk_annot (k2 s e);;
+        RET (exist P r _).
+Obligation 2.
+  unfold wlp in * |- *; eauto.
+Qed.
+
+Notation "'TRY' k1 'CATCH_FAIL' s ',' e '=>' k2 'ENSURE' P" := (try_catch_fail_ensure (fun _ => k1) (fun s e => k2) (exist _ P _))
+    (at level 55, k1 at level 53, right associativity): impure_scope.
+
+Definition is_try_post {A} (P: A -> Prop) k1 k2 : Prop := 
+  wlp (k1 ()) P /\ forall (e:exn), wlp (k2 e) P.
+
+Program Definition try_catch_ensure {A} k1 k2 (P:A->Prop|is_try_post P k1 k2): ?? { r | P r }
+  := TRY
+        DO r <~ mk_annot (k1 ());; 
+        RET (exist P r _)
+     WITH_ANY e => 
+        DO r <~ mk_annot (k2 e);;
+        RET (exist P r _).
+Obligation 1.
+  unfold is_try_post, wlp in * |- *; intuition eauto.
+Qed.
+Obligation 2.
+  unfold is_try_post, wlp in * |- *; intuition eauto.
+Qed.
+
+Notation "'TRY' k1 'CATCH' e '=>' k2 'ENSURE' P" := (try_catch_ensure (fun _ => k1) (fun e => k2) (exist _ P _))
+    (at level 55, k1 at level 53, right associativity): impure_scope.
+
+
+Program Example tryex {A} (x y:A) := 
+  TRY (RET x)
+  CATCH _ => (RET y)
+  ENSURE (fun r => r = x \/ r = y).
+Obligation 1.
+  split; wlp_simplify.
+Qed.
+
+Program Example tryex_test {A} (x y:A): 
+  WHEN tryex x y ~> r THEN `r <> x -> `r = y.
+Proof.
+  wlp_simplify. destruct exta as [r [X|X]]; intuition.
+Qed.
+
+
+Program Example try_branch1 {A} (x:A): ?? { r | r = x} := 
+  TRY (RET x)
+  CATCH e => (FAILWITH "!")
+  ENSURE _.
+Obligation 1.
+  split; wlp_simplify.
+Qed.
+
+Program Example try_branch2 {A} (x:A): ?? { r | r = x} := 
+  TRY (FAILWITH "!")
+  CATCH e => (RET x)
+  ENSURE _.
+Obligation 1.
+  split; wlp_simplify.
+Qed.
diff --git a/lib/Impure/ImpLoops.v b/lib/Impure/ImpLoops.v
new file mode 100644
index 00000000..33376c19
--- /dev/null
+++ b/lib/Impure/ImpLoops.v
@@ -0,0 +1,123 @@
+(** 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/lib/Impure/ImpMonads.v b/lib/Impure/ImpMonads.v
new file mode 100644
index 00000000..f01a2755
--- /dev/null
+++ b/lib/Impure/ImpMonads.v
@@ -0,0 +1,148 @@
+(** Impure monad for interface with impure code
+*)
+
+
+Require Import Program.
+
+
+Module Type MayReturnMonad.
+
+  Axiom t: Type -> Type.
+
+  Axiom mayRet: forall {A:Type}, t A -> A -> Prop.
+
+  Axiom ret: forall {A}, A -> t A.
+
+  Axiom bind: forall {A B}, (t A) -> (A -> t B) -> t B.
+
+  Axiom mk_annot: forall {A} (k: t A), t { a: A | mayRet k a }.
+
+  Axiom mayRet_ret: forall A (a b:A), 
+     mayRet (ret a) b -> a=b.
+
+  Axiom mayRet_bind: forall A B k1 k2 (b:B),
+     mayRet (bind k1 k2) b -> exists a:A, mayRet k1 a /\ mayRet (k2 a) b.
+
+End MayReturnMonad.
+
+
+
+(** Model of impure computation as predicate *)
+Module PowerSetMonad<: MayReturnMonad.
+ 
+   Definition t (A:Type) := A -> Prop.
+
+   Definition mayRet {A:Type} (k: t A) a: Prop := k a.
+
+   Definition ret {A:Type} (a:A) := eq a.
+
+   Definition bind {A B:Type} (k1: t A) (k2: A -> t B) := 
+     fun b => exists a, k1 a /\ k2 a b.
+
+   Definition mk_annot {A} (k: t A) : t { a | mayRet k a } := fun _ => True.
+
+   Lemma mayRet_ret A (a b:A): mayRet (ret a) b -> a=b.
+   Proof.
+     unfold mayRet, ret. firstorder.
+   Qed.
+
+   Lemma mayRet_bind A B k1 k2 (b:B):
+         mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b.
+   Proof.
+     unfold mayRet, bind. 
+     firstorder.
+   Qed.
+
+End PowerSetMonad.
+
+
+(** The identity interpretation *)
+Module IdentityMonad<: MayReturnMonad.
+
+   Definition t (A:Type) := A.
+
+   (* may-return semantics of computations *)
+   Definition mayRet {A:Type} (a b:A): Prop := a=b.
+
+   Definition ret {A:Type} (a:A) := a.
+
+   Definition bind {A B:Type} (k1: A) (k2: A -> B) := k2 k1.
+
+   Definition mk_annot {A} (k: t A) : t { a: A | mayRet k a } 
+    := exist _ k (eq_refl k) .
+
+   Lemma mayRet_ret (A:Type) (a b:A): mayRet (ret a) b -> a=b.
+   Proof.
+     intuition.
+   Qed.
+
+   Lemma mayRet_bind (A B:Type) (k1:t A) k2 (b:B):
+         mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b.
+   Proof.
+     firstorder.
+   Qed.
+
+End IdentityMonad.
+
+
+(** Model of impure computation as state-transformers *)
+Module StateMonad<: MayReturnMonad.
+ 
+   Parameter St: Type. (* A global state *)
+
+   Definition t (A:Type) := St -> A * St.
+
+   Definition mayRet {A:Type} (k: t A) a: Prop :=
+     exists s, fst (k s)=a.
+
+   Definition ret {A:Type} (a:A) := fun (s:St) => (a,s).
+
+   Definition bind {A B:Type} (k1: t A) (k2: A -> t B) := 
+     fun s0 => let r := k1 s0 in k2 (fst r) (snd r).
+
+   Program Definition mk_annot {A} (k: t A) : t { a | mayRet k a } := 
+     fun s0 => let r := k s0 in (exist _ (fst r) _, snd r).
+   Obligation 1.
+     unfold mayRet; eauto.
+   Qed.
+
+   Lemma mayRet_ret {A:Type} (a b:A): mayRet (ret a) b -> a=b.
+   Proof.
+     unfold mayRet, ret. firstorder.
+   Qed.
+
+   Lemma mayRet_bind {A B:Type} k1 k2 (b:B):
+         mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b.
+   Proof.
+     unfold mayRet, bind. firstorder eauto.
+   Qed. 
+
+End StateMonad.
+
+(** The deferred interpretation *)
+Module DeferredMonad<: MayReturnMonad.
+
+   Definition t (A:Type) := unit -> A.
+
+   (* may-return semantics of computations *)
+   Definition mayRet {A:Type} (a: t A) (b:A): Prop := a tt=b.
+
+   Definition ret {A:Type} (a:A) : t A := fun _ => a.
+
+   Definition bind {A B:Type} (k1: t A) (k2: A -> t B) : t B := fun _ => k2 (k1 tt) tt.
+
+   Definition mk_annot {A} (k: t A) : t { a: A | mayRet k a } 
+    := fun _ => exist _ (k tt) (eq_refl (k tt)).
+
+   Lemma mayRet_ret (A:Type) (a b: A): mayRet (ret a) b -> a=b.
+   Proof.
+     intuition.
+   Qed.
+
+   Lemma mayRet_bind (A B:Type) (k1:t A) k2 (b:B):
+         mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b.
+   Proof.
+     firstorder.
+   Qed.
+
+End DeferredMonad.
diff --git a/lib/Impure/ImpPrelude.v b/lib/Impure/ImpPrelude.v
new file mode 100644
index 00000000..de4c7973
--- /dev/null
+++ b/lib/Impure/ImpPrelude.v
@@ -0,0 +1,206 @@
+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/lib/Impure/LICENSE b/lib/Impure/LICENSE
new file mode 100644
index 00000000..65c5ca88
--- /dev/null
+++ b/lib/Impure/LICENSE
@@ -0,0 +1,165 @@
+                   GNU LESSER GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+
+  This version of the GNU Lesser General Public License incorporates
+the terms and conditions of version 3 of the GNU General Public
+License, supplemented by the additional permissions listed below.
+
+  0. Additional Definitions.
+
+  As used herein, "this License" refers to version 3 of the GNU Lesser
+General Public License, and the "GNU GPL" refers to version 3 of the GNU
+General Public License.
+
+  "The Library" refers to a covered work governed by this License,
+other than an Application or a Combined Work as defined below.
+
+  An "Application" is any work that makes use of an interface provided
+by the Library, but which is not otherwise based on the Library.
+Defining a subclass of a class defined by the Library is deemed a mode
+of using an interface provided by the Library.
+
+  A "Combined Work" is a work produced by combining or linking an
+Application with the Library.  The particular version of the Library
+with which the Combined Work was made is also called the "Linked
+Version".
+
+  The "Minimal Corresponding Source" for a Combined Work means the
+Corresponding Source for the Combined Work, excluding any source code
+for portions of the Combined Work that, considered in isolation, are
+based on the Application, and not on the Linked Version.
+
+  The "Corresponding Application Code" for a Combined Work means the
+object code and/or source code for the Application, including any data
+and utility programs needed for reproducing the Combined Work from the
+Application, but excluding the System Libraries of the Combined Work.
+
+  1. Exception to Section 3 of the GNU GPL.
+
+  You may convey a covered work under sections 3 and 4 of this License
+without being bound by section 3 of the GNU GPL.
+
+  2. Conveying Modified Versions.
+
+  If you modify a copy of the Library, and, in your modifications, a
+facility refers to a function or data to be supplied by an Application
+that uses the facility (other than as an argument passed when the
+facility is invoked), then you may convey a copy of the modified
+version:
+
+   a) under this License, provided that you make a good faith effort to
+   ensure that, in the event an Application does not supply the
+   function or data, the facility still operates, and performs
+   whatever part of its purpose remains meaningful, or
+
+   b) under the GNU GPL, with none of the additional permissions of
+   this License applicable to that copy.
+
+  3. Object Code Incorporating Material from Library Header Files.
+
+  The object code form of an Application may incorporate material from
+a header file that is part of the Library.  You may convey such object
+code under terms of your choice, provided that, if the incorporated
+material is not limited to numerical parameters, data structure
+layouts and accessors, or small macros, inline functions and templates
+(ten or fewer lines in length), you do both of the following:
+
+   a) Give prominent notice with each copy of the object code that the
+   Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the object code with a copy of the GNU GPL and this license
+   document.
+
+  4. Combined Works.
+
+  You may convey a Combined Work under terms of your choice that,
+taken together, effectively do not restrict modification of the
+portions of the Library contained in the Combined Work and reverse
+engineering for debugging such modifications, if you also do each of
+the following:
+
+   a) Give prominent notice with each copy of the Combined Work that
+   the Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the Combined Work with a copy of the GNU GPL and this license
+   document.
+
+   c) For a Combined Work that displays copyright notices during
+   execution, include the copyright notice for the Library among
+   these notices, as well as a reference directing the user to the
+   copies of the GNU GPL and this license document.
+
+   d) Do one of the following:
+
+       0) Convey the Minimal Corresponding Source under the terms of this
+       License, and the Corresponding Application Code in a form
+       suitable for, and under terms that permit, the user to
+       recombine or relink the Application with a modified version of
+       the Linked Version to produce a modified Combined Work, in the
+       manner specified by section 6 of the GNU GPL for conveying
+       Corresponding Source.
+
+       1) Use a suitable shared library mechanism for linking with the
+       Library.  A suitable mechanism is one that (a) uses at run time
+       a copy of the Library already present on the user's computer
+       system, and (b) will operate properly with a modified version
+       of the Library that is interface-compatible with the Linked
+       Version.
+
+   e) Provide Installation Information, but only if you would otherwise
+   be required to provide such information under section 6 of the
+   GNU GPL, and only to the extent that such information is
+   necessary to install and execute a modified version of the
+   Combined Work produced by recombining or relinking the
+   Application with a modified version of the Linked Version. (If
+   you use option 4d0, the Installation Information must accompany
+   the Minimal Corresponding Source and Corresponding Application
+   Code. If you use option 4d1, you must provide the Installation
+   Information in the manner specified by section 6 of the GNU GPL
+   for conveying Corresponding Source.)
+
+  5. Combined Libraries.
+
+  You may place library facilities that are a work based on the
+Library side by side in a single library together with other library
+facilities that are not Applications and are not covered by this
+License, and convey such a combined library under terms of your
+choice, if you do both of the following:
+
+   a) Accompany the combined library with a copy of the same work based
+   on the Library, uncombined with any other library facilities,
+   conveyed under the terms of this License.
+
+   b) Give prominent notice with the combined library that part of it
+   is a work based on the Library, and explaining where to find the
+   accompanying uncombined form of the same work.
+
+  6. Revised Versions of the GNU Lesser General Public License.
+
+  The Free Software Foundation may publish revised and/or new versions
+of the GNU Lesser General Public License from time to time. Such new
+versions will be similar in spirit to the present version, but may
+differ in detail to address new problems or concerns.
+
+  Each version is given a distinguishing version number. If the
+Library as you received it specifies that a certain numbered version
+of the GNU Lesser General Public License "or any later version"
+applies to it, you have the option of following the terms and
+conditions either of that published version or of any later version
+published by the Free Software Foundation. If the Library as you
+received it does not specify a version number of the GNU Lesser
+General Public License, you may choose any version of the GNU Lesser
+General Public License ever published by the Free Software Foundation.
+
+  If the Library as you received it specifies that a proxy can decide
+whether future versions of the GNU Lesser General Public License shall
+apply, that proxy's public statement of acceptance of any version is
+permanent authorization for you to choose that version for the
+Library.
diff --git a/lib/Impure/README.md b/lib/Impure/README.md
new file mode 100644
index 00000000..2b19d14a
--- /dev/null
+++ b/lib/Impure/README.md
@@ -0,0 +1,31 @@
+# `Impure`: importing OCaml functions as non-deterministic ones.
+
+The principle of this library is to encode the type `A -> B` of an
+OCaml function as a type `A -> ?? B` in Coq, where `?? B` is the type
+of an axiomatized monad that can be interpreted as `B -> Prop`.  In
+other word, this encoding abstracts an OCaml function as a function
+returning a postcondition on its possible results (ie a relation between its
+parameter and its result). Side-effects are simply ignored. And
+reasoning on such a function is only possible in partial correctness.
+
+See further explanations and examples on [ImpureDemo](https://github.com/boulme/ImpureDemo).
+
+## Credits
+
+[Sylvain Boulmé](mailto:Sylvain.Boulme@univ-grenoble-alpes.fr).
+
+## Code Overview
+
+- [ImpMonads](ImpMonads.v) axioms of "impure computations" and some Coq models of these axioms.
+
+- [ImpConfig](ImpConfig.v) declares the `Impure` monad and defines its extraction.
+
+- [ImpCore](ImpCore.v) defines notations for the `Impure` monad and a `wlp_simplify` tactic (to reason about `Impure` functions in a Hoare-logic style).
+
+- [ImpPrelude](ImpPrelude.v) declares the data types exchanged with `Impure` oracles.
+
+- [ImpIO](ImpIO.v), [ImpLoops](ImpLoops.v), [ImpHCons](ImpHCons.v) declare `Impure` oracles and define operators from these oracles.
+  [ImpExtern](ImpExtern.v) exports all these impure operators.
+
+- [ocaml/](ocaml/) subdirectory containing the OCaml implementations of `Impure` oracles.
+
diff --git a/lib/Impure/ocaml/ImpHConsOracles.ml b/lib/Impure/ocaml/ImpHConsOracles.ml
new file mode 100644
index 00000000..68a33a91
--- /dev/null
+++ b/lib/Impure/ocaml/ImpHConsOracles.ml
@@ -0,0 +1,72 @@
+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) ->
+     (* DEBUG:
+     Printf.printf "*in %d -- look for hcodes= " (Obj.magic t);
+     List.iter (fun i -> Printf.printf "%d " i) k.hcodes;
+     print_newline();
+     *)
+     match MyHashtbl.find_opt t k with
+     | Some d -> d
+     | None ->
+         (* DEBUG: Printf.printf "*in %d -- new hid:%d" (Obj.magic t) (MyHashtbl.length t); print_newline(); *)
+         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/lib/Impure/ocaml/ImpHConsOracles.mli b/lib/Impure/ocaml/ImpHConsOracles.mli
new file mode 100644
index 00000000..5075d176
--- /dev/null
+++ b/lib/Impure/ocaml/ImpHConsOracles.mli
@@ -0,0 +1,5 @@
+open ImpPrelude
+open HConsingDefs
+
+val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t
+val xhCons: 'a hashP -> 'a hashConsing
diff --git a/lib/Impure/ocaml/ImpIOOracles.ml b/lib/Impure/ocaml/ImpIOOracles.ml
new file mode 100644
index 00000000..9e63c12d
--- /dev/null
+++ b/lib/Impure/ocaml/ImpIOOracles.ml
@@ -0,0 +1,142 @@
+(* 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/lib/Impure/ocaml/ImpIOOracles.mli b/lib/Impure/ocaml/ImpIOOracles.mli
new file mode 100644
index 00000000..6064286a
--- /dev/null
+++ b/lib/Impure/ocaml/ImpIOOracles.mli
@@ -0,0 +1,33 @@
+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/lib/Impure/ocaml/ImpLoopOracles.ml b/lib/Impure/ocaml/ImpLoopOracles.ml
new file mode 100644
index 00000000..cb7625e5
--- /dev/null
+++ b/lib/Impure/ocaml/ImpLoopOracles.ml
@@ -0,0 +1,78 @@
+open ImpPrelude
+open Datatypes
+
+(** GENERIC ITERATIVE LOOP **) 
+
+(* a simple version of loop *)
+let simple_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b
+  = fun (a0, f) ->
+    let rec iter: 'a -> 'b
+      = fun a ->
+        match f a with
+        | Coq_inl a' -> iter a'
+        | Coq_inr b -> b
+    in
+    iter a0;;
+
+(* loop from while *)
+let while_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b
+  = fun (a0, f) ->
+    let s = ref (f a0) in
+    while (match !s with Coq_inl _ -> true | _ -> false) do
+      match !s with
+      | Coq_inl a -> s:=f a
+      | _ -> assert false
+    done;
+    match !s with
+    | Coq_inr b -> b
+    | _ -> assert false;;
+
+let loop = simple_loop
+
+
+(** GENERIC FIXPOINTS **)
+  
+let std_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b =
+  let rec f x = recf f x in
+  f
+
+let memo_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b  =
+  let memo = Hashtbl.create 10 in
+  let rec f x =
+    try
+      Hashtbl.find memo x
+    with
+      Not_found ->
+        let r = recf f x in
+        Hashtbl.replace memo x r;
+        r
+  in f
+
+let bare_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b  =
+  let fix = ref (fun x -> failwith "init") in
+  fix := (fun x -> recf !fix x);
+  !fix;;
+  
+let buggy_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b =
+  let memo = ref None in
+  let rec f x =
+    match !memo with
+    | Some y -> y
+    | None ->
+       let r = recf f x in
+       memo := Some r;
+       r
+  in f
+
+let xrec_mode = ref MemoRec
+
+let xrec_set_option : recMode -> unit
+= fun m -> xrec_mode := m
+
+let xrec : (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b )
+  = fun recf ->
+    match !xrec_mode with
+    | StdRec -> std_rec recf
+    | MemoRec -> memo_rec recf
+    | BareRec -> bare_rec recf
+    | BuggyRec -> buggy_rec recf
diff --git a/lib/Impure/ocaml/ImpLoopOracles.mli b/lib/Impure/ocaml/ImpLoopOracles.mli
new file mode 100644
index 00000000..194696a1
--- /dev/null
+++ b/lib/Impure/ocaml/ImpLoopOracles.mli
@@ -0,0 +1,8 @@
+open ImpPrelude
+open Datatypes
+
+val loop: ('a * ('a -> ('a, 'b) sum)) -> 'b
+
+val xrec_set_option: recMode -> unit 
+
+val xrec: (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b ) 
diff --git a/lib/IterList.v b/lib/IterList.v
new file mode 100644
index 00000000..49beb1c5
--- /dev/null
+++ b/lib/IterList.v
@@ -0,0 +1,96 @@
+Require Import Coqlib.
+
+(** TODO: are these def and lemma already defined in the standard library ?
+
+In this case, it should be better to reuse those of the standard library !
+
+*)
+
+Fixpoint iter {A} (n:nat) (f: A -> A) (x: A) {struct n}: A :=
+  match n with
+  | O => x
+  | S n0 => iter n0 f (f x)
+  end.
+
+Lemma iter_S A (n:nat) (f: A -> A): forall x, iter (S n) f x = f (iter n f x).
+Proof.
+  induction n; simpl; auto.
+  intros; erewrite <- IHn; simpl; auto.
+Qed.
+
+Lemma iter_plus A (n m:nat) (f: A -> A): forall x, iter (n+m) f x = iter m f (iter n f x).
+Proof.
+  induction n; simpl; auto.
+Qed.
+
+Definition iter_tail {A} (n:nat) (l: list A) := iter n (@tl A) l.
+
+Lemma iter_tail_S {A} (n:nat) (l: list A): iter_tail (S n) l = tl (iter_tail n l).
+Proof.
+  apply iter_S.
+Qed.
+
+Lemma iter_tail_plus A (n m:nat) (l: list A): iter_tail (n+m) l = iter_tail m (iter_tail n l).
+Proof.
+  apply iter_plus.
+Qed.
+
+Lemma iter_tail_length A l1: forall (l2: list A), iter_tail (length l1) (l1 ++ l2) = l2.
+Proof.
+  induction l1; auto.
+Qed.
+
+Lemma iter_tail_nil A n: @iter_tail A n nil = nil.
+Proof.
+  unfold iter_tail; induction n; simpl; auto.
+Qed.
+
+Lemma iter_tail_reach_nil A (l: list A): iter_tail (length l) l = nil.
+Proof.
+  rewrite (app_nil_end l) at 2.
+  rewrite iter_tail_length. 
+  auto.
+Qed.
+
+Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat.
+Proof.
+  unfold iter_tail; induction n; auto.
+  intros l; destruct l. { simpl; omega. }
+  intros; simpl. erewrite IHn; eauto.
+  simpl in *; omega.
+Qed.
+
+Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l).
+Proof.
+  unfold iter_tail; induction n; simpl.
+  - intros l; destruct l; simpl; omega || eauto.
+  - intros l H; destruct (IHn (tl l)) as (x & H1).
+    + destruct l; simpl in *; try omega.
+    + rewrite H1; eauto.
+Qed.
+
+Lemma iter_tail_inject1 {A} (n1 n2:nat) (l: list A): (n1 <= List.length l)%nat -> (n2 <= List.length l)%nat -> iter_tail n1 l = iter_tail n2 l -> n1=n2.
+Proof.
+  intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto.
+  rewrite EQ.
+  rewrite (length_iter_tail n2 l); eauto.
+  omega.
+Qed.
+
+Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat.
+Proof.
+  destruct (le_lt_dec n (List.length l)); try omega.
+  intros; exploit (iter_tail_inject1 n (length l) l); try omega.
+  rewrite iter_tail_reach_nil. auto.
+Qed.
+
+Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l).
+Proof.
+  induction l; auto.
+  rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. omega.
+Qed.
+
+Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l).
+Proof.
+  intros; rewrite list_length_z_nat, Nat2Z.id. auto.
+Qed.
diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v
new file mode 100644
index 00000000..824a9c2f
--- /dev/null
+++ b/lib/OptionMonad.v
@@ -0,0 +1,49 @@
+(* Declare Scope option_monad_scope. *)
+
+Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
+         (at level 200, X ident, A at level 100, B at level 200)
+         : option_monad_scope.
+
+Notation "'ASSERT' A 'IN' B" := (if A then B else None)
+         (at level 200, A at level 100, B at level 200)
+         : option_monad_scope.
+
+Local Open Scope option_monad_scope.
+
+
+(** Simple tactics for option-monad *)
+
+Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B):
+  (forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)).
+Proof.
+  intros; destruct e; simpl; auto.
+Qed.
+
+Lemma destruct_ASSERT B (P: option B -> Prop) (e: bool) (x: option B):
+  (e = true -> P x) -> (e = false -> P None) -> (P (ASSERT e IN x)).
+Proof.
+  intros; destruct e; simpl; auto.
+Qed.
+
+Ltac inversion_SOME x :=
+  try (eapply destruct_SOME; [ let x := fresh x in intro x | simpl; try congruence ]).
+
+Ltac inversion_ASSERT :=
+  try (eapply destruct_ASSERT; [ idtac | simpl; try congruence ]).
+
+Ltac simplify_someHyp :=
+  match goal with
+  | H: None = Some _ |- _  => inversion H; clear H; subst
+  | H: Some _ = None |- _  => inversion H; clear H; subst
+  | H: ?t = ?t |- _ => clear H
+  | H: Some _ = Some _ |- _  => inversion H; clear H; subst
+  | H: Some _ <> None |- _ => clear H
+  | H: None <> Some _ |- _ => clear H
+  | H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H
+  end.
+
+Ltac simplify_someHyps := 
+  repeat (simplify_someHyp; simpl in * |- *).
+
+Ltac try_simplify_someHyps := 
+  try (intros; simplify_someHyps; eauto).