recreate abstractbb/

4 files changed, 2487 insertions, 0 deletions

diff --git a/scheduling/abstractbb/ImpSimuTest.v b/scheduling/abstractbb/ImpSimuTest.v
new file mode 100644
index 00000000..6b64e1d8
--- /dev/null
+++ b/scheduling/abstractbb/ImpSimuTest.v
@@ -0,0 +1,1286 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** Implementation of a simulation test (ie a "scheduling verifier") for the sequential semantics of Abstract Basic Blocks.
+
+It is based on a symbolic execution procedure of Abstract Basic Blocks with imperative hash-consing and rewriting.
+
+It also provides debugging information when the test fails.
+
+
+*)
+
+Require Export Impure.ImpHCons. (**r Import the Impure library. See https://github.com/boulme/ImpureDemo *)
+Export Notations.
+Import HConsing.
+
+Require Import Coq.Bool.Bool.
+Require Export SeqSimuTheory.
+Require Import PArith.
+
+
+Local Open Scope impure.
+
+Import ListNotations.
+Local Open Scope list_scope.
+
+
+Definition FULL_DEBUG_DUMP : bool := false. (* print debug traces, even if the verifier succeeds. *)
+
+(** * Interface of (impure) equality tests for operators *)
+Module Type ImpParam.
+
+Include LangParam.
+
+Parameter op_eq: op -> op -> ?? bool.
+
+Parameter op_eq_correct: forall o1 o2, 
+ WHEN op_eq o1 o2 ~> b THEN
+  b=true -> o1 = o2.
+
+End ImpParam.
+
+
+Module Type ISeqLanguage.
+
+Declare Module LP: ImpParam.
+
+Include MkSeqLanguage LP.
+
+End ISeqLanguage.
+
+
+(** * A generic dictinary on PseudoRegisters with an impure equality test  *)
+
+Module Type ImpDict.
+
+Declare Module R: PseudoRegisters.
+
+Parameter t: Type -> Type.
+
+Parameter get: forall {A}, t A -> R.t -> option A.
+
+Parameter set: forall {A}, t A -> R.t -> A -> t A.
+
+Parameter set_spec_eq: forall A d x (v: A),
+  get (set d x v) x = Some v.
+
+Parameter set_spec_diff: forall A d x y (v: A),
+  x <> y -> get (set d x v) y = get d y.
+
+Parameter rem: forall {A}, t A -> R.t -> t A.
+
+Parameter rem_spec_eq: forall A (d: t A) x,
+  get (rem d x) x = None.
+
+Parameter rem_spec_diff: forall A (d: t A) x y,
+  x <> y -> get (rem d x) y = get d y.
+
+Parameter empty: forall {A}, t A.
+
+Parameter empty_spec: forall A x,
+  get (empty (A:=A)) x = None.
+
+Parameter eq_test: forall {A}, t A -> t A -> ?? bool.
+
+Parameter eq_test_correct: forall A (d1 d2: t A),
+ WHEN eq_test d1 d2 ~> b THEN
+  b=true -> forall x, get d1 x = get d2 x.
+
+(* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries  *)
+
+(** only for debugging *)
+Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t.
+
+End ImpDict.
+
+
+(** * Specification of the provided tests *)
+Module Type ImpSimuInterface.
+
+Declare Module CoreL: ISeqLanguage.
+Import CoreL.
+Import Terms.
+
+(** the silent test (without debugging informations) *)
+Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool.
+
+Parameter bblock_simu_test_correct: forall reduce (p1 p2 : bblock),
+    WHEN bblock_simu_test reduce p1 p2 ~> b
+    THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.
+
+(** the verbose test extended with debugging informations *)
+Parameter verb_bblock_simu_test
+     : reduction ->
+       (R.t -> ?? pstring) ->
+       (op -> ?? pstring) -> bblock -> bblock -> ?? bool.
+
+Parameter verb_bblock_simu_test_correct: 
+   forall reduce
+          (string_of_name : R.t -> ?? pstring)
+          (string_of_op : op -> ?? pstring) 
+          (p1 p2 : bblock),
+    WHEN verb_bblock_simu_test reduce string_of_name string_of_op p1 p2 ~> b
+    THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.
+
+End ImpSimuInterface.
+
+
+(** * Implementation of the provided tests *)
+
+Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuInterface with Module CoreL := L.
+
+Module CoreL:=L.
+
+Module ST := SimuTheory L.
+
+Import ST.
+Import Terms.
+
+Definition term_set_hid (t: term) (hid: hashcode): term :=
+  match t with
+  | Input x _ => Input x hid
+  | App op l _ => App op l hid
+  end.
+
+Definition list_term_set_hid (l: list_term) (hid: hashcode): list_term :=
+  match l with
+  | LTnil _ => LTnil hid
+  | LTcons t l' _ => LTcons t l' hid
+  end.
+
+Lemma term_eval_set_hid ge t hid m:
+  term_eval ge (term_set_hid t hid) m = term_eval ge t m.
+Proof.
+  destruct t; cbn; auto.
+Qed.
+
+Lemma list_term_eval_set_hid ge l hid m:
+  list_term_eval ge (list_term_set_hid l hid) m = list_term_eval ge l m.
+Proof.
+  destruct l; cbn; auto.
+Qed.
+
+(* Local nickname *)
+Module D:=ImpPrelude.Dict.
+
+Section SimuWithReduce.
+
+Variable reduce: reduction.
+
+Section CanonBuilding. (** Implementation of the symbolic execution (ie a "canonical form" representing the semantics of an abstract basic block) *)
+
+Variable hC_term: hashinfo term -> ?? term.
+Hypothesis hC_term_correct: forall t, WHEN hC_term t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.
+
+Variable hC_list_term: hashinfo list_term -> ?? list_term.
+Hypothesis hC_list_term_correct: forall t, WHEN hC_list_term t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m.
+
+(* First, we wrap constructors for hashed values !*)
+
+Local Open Scope positive.
+Local Open Scope list_scope.
+
+Definition hInput_hcodes (x:R.t) :=
+   DO hc <~ hash 1;;
+   DO hv <~ hash x;;
+   RET [hc;hv].
+Extraction Inline hInput_hcodes.
+
+Definition hInput (x:R.t): ?? term :=
+   DO hv <~ hInput_hcodes x;;
+   hC_term {| hdata:=Input x unknown_hid; hcodes :=hv; |}.
+
+Lemma hInput_correct x:
+  WHEN hInput x ~> t THEN forall ge m, term_eval ge t m = Some (m x).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hInput.
+Hint Resolve hInput_correct: wlp.
+
+Definition hApp_hcodes (o:op) (l: list_term) :=
+   DO hc <~ hash 2;;
+   DO hv <~ hash o;;
+   RET [hc;hv;list_term_get_hid l].
+Extraction Inline hApp_hcodes.
+
+Definition hApp (o:op) (l: list_term) : ?? term :=
+   DO hv <~ hApp_hcodes o l;;
+   hC_term {| hdata:=App o l unknown_hid; hcodes:=hv |}.
+
+Lemma hApp_correct o l:
+  WHEN hApp o l ~> t THEN forall ge m,
+    term_eval ge t m = match list_term_eval ge l m with
+                       | Some v => op_eval ge o v
+                       | None => None
+                       end.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hApp.
+Hint Resolve hApp_correct: wlp.
+
+Definition hLTnil (_: unit): ?? list_term :=
+   hC_list_term {| hdata:=LTnil unknown_hid; hcodes := nil; |} .
+
+Lemma hLTnil_correct x: 
+  WHEN hLTnil x ~> l THEN forall ge m, list_term_eval ge l m = Some nil.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hLTnil.
+Hint Resolve hLTnil_correct: wlp.
+
+
+Definition hLTcons (t: term) (l: list_term): ?? list_term :=
+   hC_list_term {| hdata:=LTcons t l unknown_hid; hcodes := [term_get_hid t; list_term_get_hid l]; |}.
+
+Lemma hLTcons_correct t l:
+  WHEN hLTcons t l ~> l' THEN forall ge m, 
+     list_term_eval ge l' m = match term_eval ge t m, list_term_eval ge l m with
+                              | Some v, Some lv => Some (v::lv)
+                              | _, _ => None
+                              end.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hLTcons.
+Hint Resolve hLTcons_correct: wlp.
+
+(* Second, we use these hashed constructors ! *)
+
+Record hsmem:= {hpre: list term; hpost:> Dict.t term}.
+
+(** evaluation of the post-condition *)
+Definition hsmem_post_eval ge (hd: Dict.t term) x (m:mem) :=
+   match Dict.get hd x with 
+   | None => Some (m x)
+   | Some ht => term_eval ge ht m
+   end.
+
+Definition hsmem_get (d:hsmem) x: ?? term :=
+   match Dict.get d x with 
+   | None => hInput x
+   | Some t => RET t
+   end.
+
+Lemma hsmem_get_correct (d:hsmem) x:
+  WHEN hsmem_get d x ~> t THEN forall ge m, term_eval ge t m = hsmem_post_eval ge d x m.
+Proof.
+  unfold hsmem_get, hsmem_post_eval; destruct (Dict.get d x); wlp_simplify.
+Qed.
+Global Opaque hsmem_get.
+Hint Resolve hsmem_get_correct: wlp.
+
+Local Opaque allvalid.
+
+Definition smem_model ge (d: smem) (hd:hsmem): Prop :=
+  (forall m, allvalid ge hd.(hpre) m <-> smem_valid ge d m) 
+  /\ (forall m x, smem_valid ge d m -> hsmem_post_eval ge hd x m = (ST.term_eval ge (d x) m)).
+
+Lemma smem_model_smem_valid_alt ge d hd: smem_model ge d hd -> 
+ forall m x, smem_valid ge d m -> hsmem_post_eval ge hd x m <> None.
+Proof.
+  intros (H1 & H2) m x H. rewrite H2; auto.
+  unfold smem_valid in H. intuition eauto.
+Qed.
+
+Lemma smem_model_allvalid_alt ge d hd: smem_model ge d hd -> 
+ forall m x, allvalid ge hd.(hpre) m -> hsmem_post_eval ge hd x m <> None.
+Proof.
+  intros (H1 & H2) m x H. eapply smem_model_smem_valid_alt.
+  - split; eauto.
+  - rewrite <- H1; auto.
+Qed.
+
+Definition naive_set (hd:hsmem) x (t:term) := 
+  {| hpre:= t::hd.(hpre); hpost:=Dict.set hd x t |}.
+
+Lemma naive_set_correct hd x ht ge d t:
+    smem_model ge d hd ->
+    (forall m, smem_valid ge d m -> term_eval ge ht m = ST.term_eval ge t m) ->
+    smem_model ge (smem_set d x t) (naive_set hd x ht).
+Proof.
+  unfold naive_set; intros (DM0 & DM1) EQT; split.
+  - intros m.
+    destruct (DM0 m) as (PRE & VALID0); clear DM0.
+    assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. }
+    assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, ST.term_eval ge (d x) m <> None). { unfold smem_valid in PRE; tauto. }
+    rewrite !allvalid_extensionality in * |- *; cbn.
+    intuition (subst; eauto).
+    + eapply smem_valid_set_proof; eauto.
+      erewrite <- EQT; eauto.
+    + exploit smem_valid_set_decompose_1; eauto.
+      intros X1; exploit smem_valid_set_decompose_2; eauto.
+      rewrite <- EQT; eauto.
+    + exploit smem_valid_set_decompose_1; eauto.
+  - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; cbn.
+    Local Hint Resolve smem_valid_set_decompose_1: core.
+    intros; case (R.eq_dec x x0).
+    + intros; subst; rewrite !Dict.set_spec_eq; cbn; eauto.
+    + intros; rewrite !Dict.set_spec_diff; cbn; eauto.
+Qed.
+Local Hint Resolve naive_set_correct: core.
+
+Definition equiv_hsmem ge (hd1 hd2: hsmem) := 
+      (forall m, allvalid ge hd1.(hpre) m <-> allvalid ge hd2.(hpre) m)
+   /\ (forall m x, allvalid ge hd1.(hpre) m -> hsmem_post_eval ge hd1 x m = hsmem_post_eval ge hd2 x m).
+
+Lemma equiv_smem_symmetry ge hd1 hd2:
+  equiv_hsmem ge hd1 hd2 -> equiv_hsmem ge hd2 hd1.
+Proof.
+  intros (V1 & P1); split.
+  - intros; symmetry; auto.
+  - intros; symmetry; eapply P1. rewrite V1; auto.
+Qed.
+
+Lemma equiv_hsmem_models ge hd1 hd2 d: 
+   smem_model ge d hd1 -> equiv_hsmem ge hd1 hd2 -> smem_model ge d hd2.
+Proof.
+  intros (VALID & EQUIV) (HEQUIV & PEQUIV); split.
+  - intros m; rewrite <- VALID; auto. symmetry; auto.
+  - intros m x H. rewrite <- EQUIV; auto. 
+    rewrite PEQUIV; auto.
+    rewrite VALID; auto.
+Qed.
+
+Variable log_assign: R.t -> term -> ?? unit.
+
+Definition lift {A B} hid (x:A) (k: B -> ?? A) (y:B): ?? A :=
+  DO b <~ phys_eq hid unknown_hid;;
+  if b then k y else RET x.
+
+Fixpoint hterm_lift (t: term): ?? term :=
+  match t with
+  | Input x hid => lift hid t hInput x
+  | App o l hid => 
+      lift hid t
+       (fun l => DO lt <~ hlist_term_lift l;;
+        hApp o lt) l
+  end
+with hlist_term_lift (l: list_term) {struct l}: ?? list_term :=
+  match l with
+  | LTnil hid => lift hid l hLTnil ()
+  | LTcons t l' hid => 
+     lift hid l
+        (fun t => DO t <~ hterm_lift t;;
+         DO lt <~ hlist_term_lift l';;
+          hLTcons t lt) t
+  end.
+
+Lemma hterm_lift_correct t:
+  WHEN hterm_lift t ~> ht THEN forall ge m, term_eval ge ht m = term_eval ge t m.
+Proof.
+  induction t using term_mut with (P0:=fun lt =>
+     WHEN hlist_term_lift lt ~> hlt THEN forall ge m, list_term_eval ge hlt m = list_term_eval ge lt m); 
+     wlp_simplify.
+  - rewrite H0, H; auto.
+  - rewrite H1, H0, H; auto.
+Qed.
+Local Hint Resolve hterm_lift_correct: wlp.
+Global Opaque hterm_lift.
+
+Variable log_new_hterm: term -> ?? unit.
+
+Fixpoint hterm_append (l: list term) (lh: list term): ?? list term :=
+  match l with
+  | nil => RET lh
+  | t::l' =>
+     DO ht <~ hterm_lift t;;
+     log_new_hterm ht;;
+     hterm_append l' (ht::lh)
+  end.
+
+Lemma hterm_append_correct l: forall lh,
+  WHEN hterm_append l lh ~> lh' THEN (forall ge m, allvalid ge lh' m <-> (allvalid ge l m /\ allvalid ge lh m)).
+Proof.
+  Local Hint Resolve eq_trans: localhint.
+  induction l as [|t l']; cbn; wlp_xsimplify ltac:(eauto with wlp).
+  - intros; rewrite! allvalid_extensionality; intuition eauto.
+  - intros REC ge m; rewrite REC; clear IHl' REC. rewrite !allvalid_extensionality.
+    cbn; intuition (subst; eauto with wlp localhint).
+Qed.
+(*Local Hint Resolve hterm_append_correct: wlp.*)
+Global Opaque hterm_append.
+
+Definition smart_set (hd:hsmem) x (ht:term) :=
+     match ht with
+     | Input y _ =>
+       if R.eq_dec x y then
+          RET (Dict.rem hd x)
+       else (
+          log_assign x ht;;
+          RET (Dict.set hd x ht)
+       )
+     | _ => 
+       log_assign x ht;;
+       RET (Dict.set hd x ht)
+     end.
+
+Lemma smart_set_correct hd x ht:
+  WHEN smart_set hd x ht ~> d THEN
+    forall ge m y, hsmem_post_eval ge d y m = hsmem_post_eval ge (Dict.set hd x ht) y m.
+Proof.
+  destruct ht; wlp_simplify.
+  unfold hsmem_post_eval; cbn. case (R.eq_dec x0 y).
+  - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. cbn; congruence.
+  - intros; rewrite Dict.set_spec_diff, Dict.rem_spec_diff; auto.
+Qed.
+(*Local Hint Resolve smart_set_correct: wlp.*)
+Global Opaque smart_set.
+
+Definition hsmem_set (hd:hsmem) x (t:term) :=
+  DO pt <~ reduce t;;
+  DO lht <~ hterm_append pt.(mayfail) hd.(hpre);;
+  DO ht <~ hterm_lift pt.(effect);;
+  log_new_hterm ht;;
+  DO nd <~ smart_set hd x ht;;
+  RET {| hpre := lht; hpost := nd |}.
+
+Lemma hsmem_set_correct hd x ht:
+  WHEN hsmem_set hd x ht ~> nhd THEN
+    forall ge d t, smem_model ge d hd ->
+    (forall m, smem_valid ge d m -> term_eval ge ht m = ST.term_eval ge t m) ->
+    smem_model ge (smem_set d x t) nhd.
+Proof.
+  intros; wlp_simplify.
+  generalize (hterm_append_correct _ _ _ Hexta0); intro APPEND.
+  generalize (hterm_lift_correct _ _ Hexta1); intro LIFT.
+  generalize (smart_set_correct _ _ _ _ Hexta3); intro SMART.
+  eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; cbn. 
+  destruct H as (VALID & EFFECT); split.
+  - intros; rewrite APPEND, <- VALID.
+    rewrite !allvalid_extensionality in * |- *; cbn; intuition (subst; eauto).
+  - intros m x0 ALLVALID; rewrite SMART.
+    destruct (term_eval ge ht m) eqn: Hht.
+    * case (R.eq_dec x x0).
+      + intros; subst. unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_eq.
+        erewrite LIFT, EFFECT; eauto.
+      + intros; unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_diff; auto.
+    * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); cbn; auto.
+Qed.
+Local Hint Resolve hsmem_set_correct: wlp.
+Global Opaque hsmem_set.
+
+(* VARIANTE: we do not hash-cons the term from the expression
+Lemma exp_hterm_correct ge e hod od:
+  smem_model ge od hod ->
+ forall hd d,
+  smem_model ge d hd ->
+  forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge (exp_term e hd hod) m = term_eval ge (exp_term e d od) m.
+Proof.
+  intro H.
+  induction e using exp_mut with (P0:=fun le =>  forall d hd,
+     smem_model ge d hd -> forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge (list_exp_term le hd hod) m = list_term_eval ge (list_exp_term le d od) m); 
+     unfold smem_model in * |- * ; cbn; intuition eauto.
+  - erewrite IHe; eauto.
+  - erewrite IHe0, IHe; eauto.
+Qed.
+Local Hint Resolve exp_hterm_correct: wlp.
+*)
+
+Fixpoint exp_hterm (e: exp) (hd hod: hsmem): ?? term :=
+  match e with
+  | PReg x => hsmem_get hd x
+  | Op o le =>
+     DO lt <~ list_exp_hterm le hd hod;; 
+     hApp o lt
+  | Old e => exp_hterm e hod hod
+  end
+with list_exp_hterm (le: list_exp) (hd hod: hsmem): ?? list_term :=
+  match le with
+  | Enil => hLTnil tt
+  | Econs e le' => 
+     DO t <~ exp_hterm e hd hod;;
+     DO lt <~ list_exp_hterm le' hd hod;;
+     hLTcons t lt
+  | LOld le => list_exp_hterm le hod hod
+  end.
+
+Lemma exp_hterm_correct_x ge e hod od:
+   smem_model ge od hod ->
+  forall hd d,
+   smem_model ge d hd ->
+  WHEN exp_hterm e hd hod ~> t THEN forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = ST.term_eval ge (exp_term e d od) m.
+ Proof.
+   intro H.
+   induction e using exp_mut with (P0:=fun le =>  forall d hd,
+     smem_model ge d hd ->
+     WHEN list_exp_hterm le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = ST.list_term_eval ge (list_exp_term le d od) m); 
+     unfold smem_model, hsmem_post_eval in * |- * ; cbn; wlp_simplify.
+  - rewrite H1, <- H4; auto.
+  - rewrite H4, <- H0; cbn; auto.
+  - rewrite H5, <- H0, <- H4; cbn; auto.
+Qed.
+Global Opaque exp_hterm.
+
+Lemma exp_hterm_correct e hd hod:
+  WHEN exp_hterm e hd hod ~> t THEN forall ge od d m, smem_model ge od hod -> smem_model ge d hd -> smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = ST.term_eval ge (exp_term e d od) m.
+Proof.
+  unfold wlp; intros; eapply exp_hterm_correct_x; eauto.
+Qed.
+Hint Resolve exp_hterm_correct: wlp.
+
+Fixpoint hinst_smem (i: inst) (hd hod: hsmem): ?? hsmem :=
+  match i with
+  | nil => RET hd
+  | (x, e)::i' =>
+     DO ht <~ exp_hterm e hd hod;;
+     DO nd <~ hsmem_set hd x ht;;
+     hinst_smem i' nd hod
+  end.
+
+Lemma hinst_smem_correct i: forall hd hod,
+  WHEN hinst_smem i hd hod ~> hd' THEN
+    forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'.
+Proof.
+  Local Hint Resolve smem_valid_set_proof: core.
+  induction i; cbn; wlp_simplify; eauto 15 with wlp.
+Qed.
+Global Opaque hinst_smem.
+Local Hint Resolve hinst_smem_correct: wlp.
+
+(* logging info: we log the number of inst-instructions passed ! *)
+Variable log_new_inst: unit -> ?? unit. 
+
+Fixpoint bblock_hsmem_rec (p: bblock) (d: hsmem): ?? hsmem :=
+  match p with
+  | nil => RET d
+  | i::p' =>
+     log_new_inst tt;;
+     DO d' <~ hinst_smem i d d;;
+     bblock_hsmem_rec p' d'
+  end.
+
+Lemma bblock_hsmem_rec_correct p: forall hd,
+  WHEN bblock_hsmem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'.
+Proof.
+  induction p; cbn; wlp_simplify.
+Qed.
+Global Opaque bblock_hsmem_rec.
+Local Hint Resolve bblock_hsmem_rec_correct: wlp.
+
+Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}.
+
+Lemma hsmem_empty_correct ge: smem_model ge smem_empty hsmem_empty.
+Proof.
+  unfold smem_model, smem_valid, hsmem_post_eval; cbn; intuition try congruence.
+  rewrite !Dict.empty_spec; cbn; auto.
+Qed.
+
+Definition bblock_hsmem: bblock -> ?? hsmem
+ := fun p => bblock_hsmem_rec p hsmem_empty.
+
+Lemma bblock_hsmem_correct p:
+  WHEN bblock_hsmem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd.
+Proof.
+  Local Hint Resolve hsmem_empty_correct: core.
+  wlp_simplify.
+Qed.
+Global Opaque bblock_hsmem.
+
+End CanonBuilding.
+
+(* Now, we build the hash-Cons value from a "hash_eq".
+
+Informal specification: 
+  [hash_eq] must be consistent with the "hashed" constructors defined above.
+
+We expect that hashinfo values in the code of these "hashed" constructors verify:
+
+  (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)    
+
+*)
+
+Definition term_hash_eq (ta tb: term): ?? bool := 
+  match ta, tb with
+  | Input xa _, Input xb _ =>
+     if R.eq_dec xa xb  (* Inefficient in some cases ? *)
+     then RET true
+     else RET false
+  | App oa lta _, App ob ltb _ => 
+     DO b <~ op_eq oa ob ;;
+     if b then phys_eq lta ltb
+     else RET false
+  | _,_ => RET false
+  end.
+
+Lemma term_hash_eq_correct: forall ta tb, WHEN term_hash_eq ta tb ~> b THEN b=true -> term_set_hid ta unknown_hid=term_set_hid tb unknown_hid.
+Proof.
+  Local Hint Resolve op_eq_correct: wlp.
+  destruct ta, tb; wlp_simplify; (discriminate || (subst; auto)).
+Qed.
+Global Opaque term_hash_eq.
+Hint Resolve term_hash_eq_correct: wlp.
+
+Definition list_term_hash_eq (lta ltb: list_term): ?? bool := 
+  match lta, ltb with
+  | LTnil _, LTnil _ => RET true
+  | LTcons ta lta _, LTcons tb ltb _ => 
+      DO b <~ phys_eq ta tb ;;
+     if b then phys_eq lta ltb
+     else RET false
+  | _,_ => RET false
+  end.
+
+Lemma list_term_hash_eq_correct: forall lta ltb, WHEN list_term_hash_eq lta ltb ~> b THEN b=true -> list_term_set_hid lta unknown_hid=list_term_set_hid ltb unknown_hid.
+Proof.
+  destruct lta, ltb; wlp_simplify; (discriminate || (subst; auto)).
+Qed.
+Global Opaque list_term_hash_eq.
+Hint Resolve list_term_hash_eq_correct: wlp.
+
+Lemma hsmem_post_eval_intro (d1 d2: hsmem):
+  (forall x, Dict.get d1 x = Dict.get d2 x) -> (forall ge x m, hsmem_post_eval ge d1 x m = hsmem_post_eval ge d2 x m).
+Proof.
+  unfold hsmem_post_eval; intros H ge x m; rewrite H. destruct (Dict.get d2 x); auto.
+Qed.
+
+Local Hint Resolve bblock_hsmem_correct Dict.eq_test_correct: wlp.
+
+Program Definition mk_hash_params (log: term -> ?? unit): Dict.hash_params term :=
+ {|
+    Dict.test_eq := phys_eq;
+    Dict.hashing := fun (ht: term) => RET (term_get_hid ht);
+    Dict.log := log |}.
+Obligation 1.
+  eauto with wlp.
+Qed.
+
+(*** A GENERIC EQ_TEST: IN ORDER TO SUPPORT SEVERAL DEBUGGING MODE !!! ***)
+Definition no_log_assign (x:R.t) (t:term): ?? unit := RET tt.
+Definition no_log_new_term (t:term): ?? unit := RET tt.
+
+Section Prog_Eq_Gen.
+
+Variable log_assign: R.t -> term -> ?? unit.
+Variable log_new_term: hashConsing term -> hashConsing list_term -> ??(term -> ?? unit).
+Variable log_inst1: unit -> ?? unit. (* log of p1 insts *)
+Variable log_inst2: unit -> ?? unit. (* log of p2 insts *)
+
+Variable hco_term: hashConsing term.
+Hypothesis hco_term_correct: forall t, WHEN hco_term.(hC) t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.
+
+Variable hco_list: hashConsing list_term.
+Hypothesis hco_list_correct: forall t, WHEN hco_list.(hC) t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m.
+
+Variable print_end_error: hsmem -> hsmem -> ?? unit.
+Variable print_dump: (option pstring) -> ?? unit.
+
+Variable check_failpreserv: bool.
+Variable dbg_failpreserv: term -> ?? unit. (* info of additional failure of the output bbloc p2 wrt the input bbloc p1 *) 
+
+Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool :=
+  DO failure_in_failpreserv <~ make_cref false;;
+  DO r <~ (TRY
+    DO d1 <~ bblock_hsmem hco_term.(hC) hco_list.(hC) log_assign no_log_new_term log_inst1 p1;;
+    DO log_new_term <~ log_new_term hco_term hco_list;;
+    DO d2 <~ bblock_hsmem hco_term.(hC) hco_list.(hC) no_log_assign log_new_term log_inst2 p2;;
+    DO b <~ Dict.eq_test d1 d2 ;;
+    if b then (
+      (if check_failpreserv then
+          let hp := mk_hash_params dbg_failpreserv in
+          failure_in_failpreserv.(set)(true);;
+          Sets.assert_list_incl hp d2.(hpre) d1.(hpre)
+      else RET tt);;
+      (if FULL_DEBUG_DUMP then
+        print_dump None (* not an error... *)
+      else RET tt);;
+      RET check_failpreserv
+    ) else (
+      print_end_error d1 d2 ;;
+      RET false
+    )
+  CATCH_FAIL s, _ =>
+    DO b <~ failure_in_failpreserv.(get)();;
+    if b then RET false 
+         else print_dump (Some s);; RET false
+  ENSURE (fun b => b=true -> forall ge, bblock_simu ge p1 p2));;
+  RET (`r).
+Obligation 1.
+  constructor 1; wlp_simplify; try congruence.
+  destruct (H ge) as (EQPRE1&EQPOST1); destruct (H0 ge) as (EQPRE2&EQPOST2); clear H H0.
+  apply bblock_smem_simu; auto. split.
+  + intros m; rewrite <- EQPRE1, <- EQPRE2.
+    rewrite ! allvalid_extensionality.
+    unfold incl in * |- *; intuition eauto.
+  + intros m0 x VALID; rewrite <- EQPOST1, <- EQPOST2; auto.
+    erewrite hsmem_post_eval_intro; eauto.
+    erewrite <- EQPRE2; auto.
+    erewrite <- EQPRE1 in VALID.
+    rewrite ! allvalid_extensionality in * |- *.
+    unfold incl in * |- *; intuition eauto.
+Qed.
+
+Theorem g_bblock_simu_test_correct p1 p2:
+  WHEN g_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
+Proof.
+  wlp_simplify.
+  destruct exta0; cbn in * |- *; auto.
+Qed.
+Global Opaque g_bblock_simu_test.
+
+End Prog_Eq_Gen.
+
+
+
+Definition hpt: hashP term := {| hash_eq := term_hash_eq; get_hid:=term_get_hid; set_hid:=term_set_hid |}. 
+Definition hplt: hashP list_term := {| hash_eq := list_term_hash_eq; get_hid:=list_term_get_hid; set_hid:=list_term_set_hid |}.
+
+Definition recover_hcodes (t:term): ??(hashinfo term) :=
+  match t with
+  | Input x _ => 
+    DO hv <~ hInput_hcodes x ;;
+    RET {| hdata := t; hcodes := hv |}
+  | App o l _ => 
+    DO hv <~ hApp_hcodes o l ;;
+    RET {| hdata := t; hcodes := hv |}
+  end.
+
+
+Definition msg_end_of_bblock: pstring :="--- unknown subterms in the graph".
+
+Definition log_new_term
+    (unknownHash_msg: term -> ?? pstring)
+    (hct:hashConsing term) 
+    (hcl:hashConsing list_term) 
+    : ?? (term -> ?? unit) :=
+  DO clock <~ hct.(next_hid)();;
+  hct.(next_log) msg_end_of_bblock;;
+  hcl.(next_log) msg_end_of_bblock;;
+  RET (fun t =>
+       DO ok <~ hash_older (term_get_hid t) clock;;
+       if ok 
+       then
+          RET tt
+       else 
+          DO ht <~ recover_hcodes t;;
+          hct.(remove) ht;;
+          DO msg <~ unknownHash_msg t;;
+          FAILWITH msg).
+
+Definition skip (_:unit): ?? unit := RET tt.
+
+Definition msg_prefix: pstring := "*** ERROR INFO from bblock_simu_test: ".
+Definition msg_error_on_end: pstring := "mismatch in final assignments !".
+Definition msg_unknow_term: pstring := "unknown term".
+Definition msg_number: pstring := "on 2nd bblock -- on inst num ".
+Definition msg_notfailpreserv: pstring := "a possible failure of 2nd bblock is absent in 1st bblock (INTERNAL ERROR: this error is expected to be detected before!!!)".
+
+Definition print_end_error (_ _: hsmem): ?? unit
+ := println (msg_prefix +; msg_error_on_end).
+
+Definition print_error (log: logger unit) (os: option pstring): ?? unit
+ := match os with
+    | Some s =>
+      DO n <~ log_info log ();;
+      println (msg_prefix +; msg_number +; n +; " -- " +; s)
+    | None => RET tt
+    end.
+
+Definition failpreserv_error (_: term): ?? unit
+  := println (msg_prefix +; msg_notfailpreserv).
+
+Lemma term_eval_set_hid_equiv ge t1 t2 hid1 hid2 m:
+  term_set_hid t1 hid1 = term_set_hid t2 hid2 -> term_eval ge t1 m = term_eval ge t2 m.
+Proof.
+  intro H; erewrite <- term_eval_set_hid; rewrite H. apply term_eval_set_hid.
+Qed.
+
+Lemma list_term_eval_set_hid_equiv ge t1 t2 hid1 hid2 m:
+  list_term_set_hid t1 hid1 = list_term_set_hid t2 hid2 -> list_term_eval ge t1 m = list_term_eval ge t2 m.
+Proof.
+  intro H; erewrite <- list_term_eval_set_hid; rewrite H. apply list_term_eval_set_hid.
+Qed.
+
+Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv: core.
+
+Program Definition bblock_simu_test (p1 p2: bblock): ?? bool :=
+  DO log <~ count_logger ();;
+  DO hco_term <~ mk_annot (hCons hpt);;
+  DO hco_list <~ mk_annot (hCons hplt);;
+  g_bblock_simu_test
+    no_log_assign
+    (log_new_term (fun _ => RET msg_unknow_term))
+    skip
+    (log_insert log)
+    hco_term _
+    hco_list _
+    print_end_error
+    (print_error log)
+    true (* check_failpreserv *)
+    failpreserv_error
+    p1 p2.
+Obligation 1.
+  generalize (hCons_correct _ _ _ H0); clear H0.
+  wlp_simplify.
+Qed.
+Obligation 2.
+  generalize (hCons_correct _ _ _ H); clear H.
+  wlp_simplify.
+Qed.
+
+Local Hint Resolve g_bblock_simu_test_correct: core.
+
+Theorem bblock_simu_test_correct p1 p2:
+  WHEN bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque bblock_simu_test.
+
+(** This is only to print info on each bblock_simu_test run **)
+Section Verbose_version.
+
+Variable string_of_name: R.t -> ?? pstring.
+Variable string_of_op: op -> ?? pstring.
+
+
+Local Open Scope string_scope.
+
+Definition string_term_hid (t: term): ?? pstring := 
+  DO id <~ string_of_hashcode (term_get_hid t);;
+  RET ("E" +; (CamlStr id)).
+
+Definition string_list_hid (lt: list_term): ?? pstring := 
+  DO id <~ string_of_hashcode (list_term_get_hid lt);;
+  RET ("L" +; (CamlStr id)).
+
+Definition print_raw_term (t: term): ?? unit :=
+  match t with
+  | Input x _ => 
+    DO s <~ string_of_name x;;
+    println( "init_access " +; s)
+  | App o (LTnil _) _ => 
+    DO so <~ string_of_op o;;
+    println so
+  | App o l _ =>
+    DO so <~ string_of_op o;;
+    DO sl <~ string_list_hid l;;
+    println (so +; " " +; sl)
+  end.
+
+(*
+Definition print_raw_list(lt: list_term): ?? unit :=
+  match lt with
+  | LTnil _=> println ""
+  | LTcons t l _ =>
+    DO st <~ string_term_hid t;;
+    DO sl <~ string_list_hid l;;
+    println(st +; " " +; sl)
+  end.
+*)
+
+Section PrettryPrint.
+
+Variable get_debug_info: term -> ?? option pstring. 
+
+Fixpoint string_of_term (t: term): ?? pstring :=
+  match t with
+  | Input x _ => string_of_name x
+  | App o (LTnil _) _ => string_of_op o
+  | App o l _ => 
+      DO so <~ string_of_op o;;
+      DO sl <~ string_of_list_term l;;
+      RET (so +; "[" +; sl +; "]")
+  end
+with string_of_list_term (l: list_term): ?? pstring :=
+  match l with
+  | LTnil _ => RET (Str "")
+  | LTcons t (LTnil _) _  => 
+    DO dbg <~ get_debug_info t;;
+    match dbg with
+    | Some x => RET x
+    | None => string_of_term t
+    end
+  | LTcons t l' _ => 
+     DO st <~ (DO dbg <~ get_debug_info t;;
+               match dbg with
+               | Some x => RET x
+               | None => string_of_term t
+               end);;
+     DO sl <~ string_of_list_term l';;
+     RET (st +; ";" +; sl)
+  end.
+
+End PrettryPrint.
+
+
+Definition pretty_term gdi t :=
+  DO r <~ string_of_term gdi t;;
+  println(r).
+
+Fixpoint print_head (head: list pstring): ?? unit :=
+  match head with
+  | i::head' => println (i);; print_head head'
+  | _ => RET tt
+  end.
+
+Definition print_term gdi (head: list pstring) (t: term): ?? unit :=
+  print_head head;;
+  DO s <~ string_term_hid t;;
+  print (s +; ": ");;
+  print_raw_term t;;
+  DO dbg <~ gdi t;;
+  match dbg with
+  | Some x => 
+     print("//  " +; x +; " <- ");;
+     pretty_term gdi t
+  | None => RET tt
+  end.
+
+Definition print_list gdi (head: list pstring) (lt: list_term): ?? unit :=
+  print_head head;;
+  DO s <~ string_list_hid lt ;;
+  print (s +; ": ");;
+  (* print_raw_list lt;; *)
+  DO ps <~ string_of_list_term gdi lt;;
+  println("[" +; ps +; "]").
+
+
+Definition print_tables gdi ext exl: ?? unit :=
+  println "-- term table --" ;;
+  iterall ext (fun head _ pt => print_term gdi head pt.(hdata));;
+  println "-- list table --" ;;
+  iterall exl (fun head _ pl => print_list gdi head pl.(hdata));;
+  println "----------------".
+
+Definition print_final_debug gdi (d1 d2: hsmem): ?? unit
+ := DO b <~ Dict.not_eq_witness d1 d2 ;;
+    match b with
+    | Some x =>
+      DO s <~ string_of_name x;;
+      println("mismatch on: " +; s);;
+      match Dict.get d1 x with 
+      | None => println("=> unassigned in 1st bblock")
+      | Some t1 =>
+         print("=> node expected from 1st bblock: ");;
+         pretty_term gdi t1
+      end;;
+      match Dict.get d2 x with 
+      | None => println("=> unassigned in 2nd bblock")
+      | Some t2 =>
+         print("=> node found from 2nd bblock: ");;
+         pretty_term gdi t2
+      end
+    | None => FAILWITH "bug in Dict.not_eq_witness ?"
+    end.
+
+Definition witness:= option term.
+
+Definition msg_term (cr: cref witness) t :=
+  set cr (Some t);;
+  RET msg_unknow_term.
+
+Definition print_witness gdi cr (*msg*) :=
+  DO wit <~ get cr ();;
+  match wit with
+  | Some t =>
+     println("=> unknown term node: ");;
+     pretty_term gdi t (*;;
+     println("=> encoded on " +; msg +; " graph as: ");;
+     print_raw_term t *)
+  | None => println "Unexpected failure: no witness info (hint: hash-consing bug ?)"
+  end.
+
+Definition print_end_error1 gdi hct hcl (d1 d2:hsmem): ?? unit
+ := println "- GRAPH of 1st bblock";;
+    DO ext <~ export hct ();;
+    DO exl <~ export hcl ();;
+    print_tables gdi ext exl;;
+    print_end_error d1 d2;;
+    print_final_debug gdi d1 d2.
+
+Definition print_dump1 gdi hct hcl cr log os : ?? unit
+ := println "- GRAPH of 1st bblock";;
+    DO ext <~ export hct ();;
+    DO exl <~ export hcl ();;
+    print_tables gdi ext exl;;
+    print_error log os;;
+    match os with
+    | Some _ => print_witness gdi cr (*"1st"*)
+    | None => RET tt
+    end.
+
+Definition xmsg_number: pstring := "on 1st bblock -- on inst num ".
+
+Definition print_end_error2 gdi hct hcl (d1 d2:hsmem): ?? unit
+ := println (msg_prefix +; msg_error_on_end);;
+    println "- GRAPH of 2nd bblock";;
+    DO ext <~ export hct ();;
+    DO exl <~ export hcl ();;
+    print_tables gdi ext exl.
+
+Definition print_dump2 gdi hct hcl cr (log: logger unit) (os:option pstring): ?? unit
+ := DO n <~ log_info log ();;
+    DO ext <~ export hct ();;
+    DO exl <~ export hcl ();;
+    match os with
+    | Some s =>
+      println (msg_prefix +; xmsg_number +; n +; " -- " +; s);;
+      print_witness gdi cr (*"2nd"*)
+    | None => RET tt
+    end;;
+    println "- GRAPH of 2nd bblock";;
+    print_tables gdi ext exl.
+
+(* USELESS
+Definition simple_log_assign (d: D.t term pstring) (x: R.t) (t: term): ?? unit :=
+  DO s <~ string_of_name x;;
+  d.(D.set) (t,s).
+*)
+
+Definition log_assign (d: D.t term pstring) (log: logger unit) (x: R.t) (t: term): ?? unit :=
+  DO i <~ log_info log ();;
+  DO sx <~ string_of_name x;;
+  d.(D.set) (t,(sx +; "@" +; i)).
+
+Definition msg_new_inst : pstring := "--- inst ".
+
+Definition hlog (log: logger unit) (hct: hashConsing term) (hcl: hashConsing list_term): unit -> ?? unit :=
+   (fun _ =>
+      log_insert log tt ;;
+      DO s <~ log_info log tt;;
+      let s:= msg_new_inst +; s in
+      next_log hct s;;
+      next_log hcl s
+    ).
+
+Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
+  DO dict_info <~ make_dict (mk_hash_params (fun _ => RET tt));;
+  DO log1 <~ count_logger ();;
+  DO log2 <~ count_logger ();;
+  DO cr <~ make_cref None;;
+  DO hco_term <~ mk_annot (hCons hpt);;
+  DO hco_list <~ mk_annot (hCons hplt);;
+  (if FULL_DEBUG_DUMP then
+      println("");;
+      println("-- START simu checker --")
+   else RET tt);;
+  DO result1 <~ (g_bblock_simu_test
+     (log_assign dict_info log1)
+     (log_new_term (msg_term cr))
+     (hlog log1 hco_term hco_list)
+     (log_insert log2)
+     hco_term _
+     hco_list _
+     (print_end_error1 dict_info.(D.get) hco_term hco_list)
+     (print_dump1 dict_info.(D.get) hco_term hco_list cr log2)
+     true
+     failpreserv_error
+     p1 p2);;
+   if (if FULL_DEBUG_DUMP then false else result1)
+   then RET true
+   else (
+    DO dict_info <~ make_dict (mk_hash_params (fun _ => RET tt));;
+    DO log1 <~ count_logger ();;
+    DO log2 <~ count_logger ();;
+    DO cr <~ make_cref None;;
+    DO hco_term <~ mk_annot (hCons hpt);;
+    DO hco_list <~ mk_annot (hCons hplt);;
+    DO result2 <~ g_bblock_simu_test
+       (log_assign dict_info log1)
+       (*fun _ _ => RET no_log_new_term*)  (* REM: too weak !! *)
+       (log_new_term (msg_term cr))        (* REM: too strong ?? *)
+       (hlog log1 hco_term hco_list)
+       (log_insert log2)
+       hco_term _
+       hco_list _
+       (print_end_error2 dict_info.(D.get) hco_term hco_list)
+       (print_dump2 dict_info.(D.get) hco_term hco_list cr log2)
+       false
+       (fun _ => RET tt)
+       p2 p1;;
+     if FULL_DEBUG_DUMP then
+        println("-- END simu checker --");;
+        println("");;
+        RET result1
+     else if result2
+     then (
+       println (msg_prefix +; " OOops - symmetry violation in bblock_simu_test  => this is a bug of bblock_simu_test ??");;
+       RET false
+     ) else RET false
+  ).
+Obligation 1.
+  generalize (hCons_correct _ _ _ H1); clear H1.
+  wlp_simplify.
+Qed.
+Obligation 2.
+  generalize (hCons_correct _ _ _ H0); clear H0.
+  wlp_simplify.
+Qed.
+Obligation 3.
+  generalize (hCons_correct _ _ _ H1); clear H1.
+  wlp_simplify.
+Qed.
+Obligation 4.
+  generalize (hCons_correct _ _ _ H0); clear H0.
+  wlp_simplify.
+Qed.
+
+Theorem verb_bblock_simu_test_correct p1 p2:
+  WHEN verb_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque verb_bblock_simu_test.
+
+End Verbose_version.
+
+End SimuWithReduce.
+
+(* TODO: why inlining fails here ? *)
+Transparent hterm_lift.
+Extraction Inline lift.
+
+End ImpSimu.
+
+
+(** * Implementation of the Dictionary (based on PositiveMap) *)
+Require Import FMapPositive.
+Require Import PArith.
+Require Import FMapPositive.
+
+Module ImpPosDict <: ImpDict with Module R:=Pos.
+
+Module R:=Pos.
+
+Definition t:=PositiveMap.t.
+
+Definition get {A} (d:t A) (x:R.t): option A 
+ := PositiveMap.find x d.
+
+Definition set {A} (d:t A) (x:R.t) (v:A): t A
+ := PositiveMap.add x v d.
+
+Local Hint Unfold PositiveMap.E.eq: core.
+
+Lemma set_spec_eq A d x (v: A):
+  get (set d x v) x = Some v.
+Proof.
+  unfold get, set; apply PositiveMap.add_1; auto.
+Qed.
+
+Lemma set_spec_diff A d x y (v: A):
+  x <> y -> get (set d x v) y = get d y.
+Proof.
+  unfold get, set; intros; apply PositiveMap.gso; auto.
+Qed.
+
+Definition rem {A} (d:t A) (x:R.t): t A
+ := PositiveMap.remove x d.
+
+Lemma rem_spec_eq A (d: t A) x:
+  get (rem d x) x = None.
+Proof.
+  unfold get, rem; apply PositiveMap.grs; auto.
+Qed.
+
+Lemma rem_spec_diff A (d: t A) x y:
+  x <> y -> get (rem d x) y = get d y.
+Proof.
+  unfold get, rem; intros; apply PositiveMap.gro; auto.
+Qed.
+
+
+Definition empty {A}: t A := PositiveMap.empty A.
+
+Lemma empty_spec A x:
+  get (empty (A:=A)) x = None.
+Proof.
+  unfold get, empty; apply PositiveMap.gempty; auto.
+Qed.
+
+Import PositiveMap.
+
+Fixpoint eq_test {A} (d1 d2: t A): ?? bool :=
+  match d1, d2 with
+  | Leaf _, Leaf _ => RET true
+  | Node l1 (Some x1) r1, Node l2 (Some x2) r2 =>
+      DO b0 <~ phys_eq x1 x2 ;;
+      if b0 then
+        DO b1 <~ eq_test l1 l2 ;;
+        if b1 then
+          eq_test r1 r2
+        else
+           RET false
+      else
+         RET false
+  | Node l1 None r1, Node l2 None r2 =>
+      DO b1 <~ eq_test l1 l2 ;;
+      if b1 then
+        eq_test r1 r2
+      else
+        RET false
+  | _, _ => RET false
+  end.
+
+Lemma eq_test_correct A d1: forall (d2: t A),
+ WHEN eq_test d1 d2 ~> b THEN
+  b=true -> forall x, get d1 x = get d2 x.
+Proof.
+  unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; cbn; 
+  wlp_simplify; (discriminate || (subst; destruct x; cbn; auto)).
+Qed.
+Global Opaque eq_test.
+
+(** ONLY FOR DEBUGGING INFO: get some key of a non-empty d *)
+Fixpoint pick {A} (d: t A): ?? R.t :=
+  match d with
+  | Leaf _ => FAILWITH "unexpected empty dictionary"
+  | Node _ (Some _) _ => RET xH
+  | Node (Leaf _) None r => 
+    DO p <~ pick r;;
+    RET (xI p)
+  | Node l None _ =>
+    DO p <~ pick l;;
+    RET (xO p)
+  end.
+
+(** ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *)
+Fixpoint not_eq_witness {A} (d1 d2: t A): ?? option R.t :=
+  match d1, d2 with
+  | Leaf _, Leaf _ => RET None
+  | Node l1 (Some x1) r1, Node l2 (Some x2) r2 =>
+      DO b0 <~ phys_eq x1 x2 ;;
+      if b0 then
+        DO b1 <~ not_eq_witness l1 l2;;
+        match b1 with
+        | None => 
+          DO b2 <~ not_eq_witness r1 r2;;
+          match b2 with
+          | None => RET None
+          | Some p => RET (Some (xI p))
+          end
+        | Some p => RET (Some (xO p))
+        end
+      else
+         RET (Some xH)
+  | Node l1 None r1, Node l2 None r2 =>
+        DO b1 <~ not_eq_witness l1 l2;;
+        match b1 with
+        | None => 
+          DO b2 <~ not_eq_witness r1 r2;;
+          match b2 with
+          | None => RET None
+          | Some p => RET (Some (xI p))
+          end
+        | Some p => RET (Some (xO p))
+        end
+  | l, Leaf _ => DO p <~ pick l;; RET (Some p)
+  | Leaf _, r => DO p <~ pick r;; RET (Some p)
+  | _, _ => RET (Some xH)
+  end.
+
+End ImpPosDict.
+
diff --git a/scheduling/abstractbb/Parallelizability.v b/scheduling/abstractbb/Parallelizability.v
new file mode 100644
index 00000000..afa4b9fd
--- /dev/null
+++ b/scheduling/abstractbb/Parallelizability.v
@@ -0,0 +1,792 @@
+(* *************************************************************)
+(*                                                             *)
+(*             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.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** Parallel Semantics of Abstract Basic Blocks and parallelizability test.
+*)
+
+Require Setoid. (* in order to rewrite <-> *)
+Require Export AbstractBasicBlocksDef.
+
+Require Import List.
+Import ListNotations.
+Local Open Scope list_scope.
+
+Require Import Sorting.Permutation.
+Require Import Bool.
+Local Open Scope lazy_bool_scope.
+
+(** * Definition of the parallel semantics *)
+Module ParallelSemantics (L: SeqLanguage).
+
+Export L.
+Local Open Scope list.
+
+Section PARALLEL.
+Variable ge: genv.
+
+(* parallel run of a inst *)
+Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem :=
+  match i with
+  | nil => Some m
+  | (x, e)::i' =>
+     match exp_eval ge e tmp old with
+     | Some v' => inst_prun i' (assign m x v') (assign tmp x v') old
+     | None => None
+     end
+  end.
+
+(* [inst_prun] is generalization of [inst_run] *)
+Lemma inst_run_prun i: forall m old,
+  inst_run ge i m old = inst_prun i m m old.
+Proof.
+  induction i as [|[y e] i']; cbn; auto.
+  intros m old; destruct (exp_eval ge e m old); cbn; auto.
+Qed.
+
+
+(* parallel run of a bblock -- with in-order writes *)
+Fixpoint prun_iw (p: bblock) m old: option mem :=
+  match p with
+  | nil => Some m
+  | i::p' =>
+    match inst_prun i m old old with
+    | Some m1 => prun_iw p' m1 old
+    | None => None
+    end
+  end.
+
+(* non-deterministic parallel run, due to arbitrary writes order *)
+Definition prun (p: bblock) m (om: option mem) := exists p', res_eq om (prun_iw p' m m) /\ Permutation p p'.
+
+
+(* a few lemma on equality *)
+
+Lemma inst_prun_equiv i old: forall m1 m2 tmp,
+  (forall x, m1 x = m2 x) ->
+  res_eq (inst_prun i m1 tmp old) (inst_prun i m2 tmp old).
+Proof.
+  induction i as [|[x e] i']; cbn; eauto.
+  intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); cbn; auto.
+  eapply IHi'; unfold assign. intros; destruct (R.eq_dec x x0); auto.
+Qed.
+
+Lemma prun_iw_equiv p: forall m1 m2 old, 
+  (forall x, m1 x = m2 x) ->
+  res_eq (prun_iw p m1 old) (prun_iw p m2 old).
+Proof.
+  induction p as [|i p']; cbn; eauto.
+  - intros m1 m2 old H.
+    generalize (inst_prun_equiv i old m1 m2 old H);
+    destruct (inst_prun i m1 old old); cbn.
+    + intros (m3 & H3 & H4); rewrite H3; cbn; eauto.
+    + intros H1; rewrite H1; cbn; auto.
+Qed.
+
+
+Lemma prun_iw_app p1: forall m1 old p2,
+   prun_iw (p1++p2) m1 old = 
+     match prun_iw p1 m1 old with 
+     | Some m2 => prun_iw p2 m2 old 
+     | None => None
+     end.
+Proof.
+   induction p1; cbn; try congruence.
+   intros; destruct (inst_prun _ _ _); cbn; auto.
+Qed.
+
+Lemma prun_iw_app_None p1: forall m1 old p2,
+   prun_iw p1 m1 old = None ->
+   prun_iw (p1++p2) m1 old = None.
+Proof.
+   intros m1 old p2 H; rewrite prun_iw_app. rewrite H; auto.
+Qed.
+
+Lemma prun_iw_app_Some p1: forall m1 old m2 p2,
+   prun_iw p1 m1 old = Some m2 ->
+   prun_iw (p1++p2) m1 old = prun_iw p2 m2 old.
+Proof.
+   intros m1 old m2 p2 H; rewrite prun_iw_app. rewrite H; auto.
+Qed.
+
+End PARALLEL.
+End ParallelSemantics.
+
+
+
+Fixpoint notIn {A} (x: A) (l:list A): Prop :=
+  match l with
+  | nil => True
+  | a::l' => x <> a /\ notIn x l'
+  end.
+
+Lemma notIn_iff A (x:A) l: (~List.In x l) <-> notIn x l.
+Proof.
+  induction l; cbn; intuition.
+Qed.
+
+Lemma notIn_app A (x:A) l1: forall l2, notIn x (l1++l2) <-> (notIn x l1 /\ notIn x l2).
+Proof.
+  induction l1; cbn.
+  - intuition.
+  - intros; rewrite IHl1. intuition.
+Qed.
+
+
+Lemma In_Permutation A (l1 l2: list A): Permutation l1 l2 -> forall x, In x l1 -> In x l2.
+Proof.
+  induction 1; cbn; intuition.
+Qed.
+
+Lemma Permutation_incl A (l1 l2: list A): Permutation l1 l2 -> incl l1 l2.
+Proof.
+  unfold incl; intros; eapply In_Permutation; eauto.
+Qed.
+
+Lemma notIn_incl A (l1 l2: list A) x: incl l1 l2 -> notIn x l2 -> notIn x l1.
+Proof.
+  unfold incl; rewrite <- ! notIn_iff; intuition.
+Qed.
+
+
+Definition disjoint {A: Type} (l l':list A) : Prop := forall x, In x l -> notIn x l'.
+
+Lemma disjoint_sym_imp A (l1 l2: list A): disjoint l1 l2 -> disjoint l2 l1.
+Proof.
+  unfold disjoint. intros H x H1. generalize (H x). rewrite <- !notIn_iff. intuition.
+Qed.
+
+Lemma disjoint_sym A (l1 l2: list A): disjoint l1 l2 <-> disjoint l2 l1.
+Proof.
+  constructor 1; apply disjoint_sym_imp; auto.
+Qed.
+
+
+Lemma disjoint_cons_l A (x:A) (l1 l2: list A): disjoint (x::l1) l2 <-> (notIn x l2) /\ (disjoint l1 l2).
+Proof.
+  unfold disjoint. cbn; intuition subst; auto. 
+Qed.
+
+Lemma disjoint_cons_r A (x:A) (l1 l2: list A): disjoint l1 (x::l2) <-> (notIn x l1) /\ (disjoint l1 l2).
+Proof.
+  rewrite disjoint_sym, disjoint_cons_l, disjoint_sym; intuition.
+Qed.
+
+Lemma disjoint_app_r A (l l1 l2: list A): disjoint l (l1++l2) <-> (disjoint l l1 /\ disjoint l l2).
+Proof.
+  unfold disjoint. intuition. 
+  - generalize (H x H0). rewrite notIn_app; intuition.
+  - generalize (H x H0). rewrite notIn_app; intuition.
+  - rewrite notIn_app; intuition.
+Qed.
+
+Lemma disjoint_app_l A (l l1 l2: list A): disjoint (l1++l2) l <-> (disjoint l1 l /\ disjoint l2 l).
+Proof.
+  rewrite disjoint_sym,  disjoint_app_r; intuition; rewrite disjoint_sym; auto.
+Qed.
+
+Lemma disjoint_incl_r A (l1 l2: list A): incl l1 l2 -> forall l, disjoint l l2 -> disjoint l l1.
+Proof.
+  unfold disjoint. intros; eapply notIn_incl; eauto.
+Qed.
+
+Lemma disjoint_incl_l A (l1 l2: list A): incl l1 l2 -> forall l, disjoint l2 l -> disjoint l1 l.
+Proof.
+  intros; rewrite disjoint_sym. eapply disjoint_incl_r; eauto. rewrite disjoint_sym; auto.
+Qed.
+
+
+Module ParallelizablityChecking (L: SeqLanguage).
+
+Include ParallelSemantics L.
+
+Section PARALLELI.
+Variable ge: genv.
+
+(** * Preliminary notions on frames *)
+
+Lemma notIn_dec (x: R.t) l : { notIn x l } + { In x l }.
+Proof.
+  destruct (In_dec R.eq_dec x l). constructor 2; auto.
+  constructor 1; rewrite <- notIn_iff. auto.
+Qed.
+
+Fixpoint frame_assign m1 (f: list R.t) m2 := 
+  match f with
+  | nil => m1
+  | x::f' => frame_assign (assign m1 x (m2 x)) f' m2  
+  end.
+
+Lemma frame_assign_def f: forall m1 m2 x,
+   frame_assign m1 f m2 x = if notIn_dec x f then m1 x else m2 x.
+Proof.
+  induction f as [|y f] ; cbn; auto.
+  - intros; destruct (notIn_dec x []); cbn in *; tauto.
+  - intros; rewrite IHf; destruct (notIn_dec x (y::f)); cbn in *.
+    + destruct (notIn_dec x f); cbn in *; intuition.
+      rewrite assign_diff; auto.
+      rewrite <- notIn_iff in *; intuition.
+    + destruct (notIn_dec x f); cbn in *; intuition subst.
+      rewrite assign_eq; auto.
+      rewrite <- notIn_iff in *; intuition.
+Qed.
+
+Lemma frame_assign_In m1 f m2 x:
+   In x f -> frame_assign m1 f m2 x = m2 x.
+Proof.
+  intros; rewrite frame_assign_def; destruct (notIn_dec x f); auto.
+  rewrite <- notIn_iff in *; intuition.
+Qed.
+
+Lemma frame_assign_notIn m1 f m2 x:
+   notIn x f -> frame_assign m1 f m2 x = m1 x.
+Proof.
+  intros; rewrite frame_assign_def; destruct (notIn_dec x f); auto.
+  rewrite <- notIn_iff in *; intuition.
+Qed.
+
+Definition frame_eq (frame: R.t -> Prop) (om1 om2: option mem): Prop :=
+  match om1 with
+  | Some m1 => exists m2, om2 = Some m2 /\ forall x, (frame x) -> m1 x = m2 x 
+  | None => om2 = None
+  end.
+
+Lemma frame_eq_list_split f1 (f2: R.t -> Prop) om1 om2:
+ frame_eq (fun x => In x f1) om1 om2 ->
+ (forall m1 m2 x, om1 = Some m1 -> om2 = Some m2 -> f2 x -> notIn x f1 -> m1 x = m2 x) ->
+ frame_eq f2 om1 om2.
+Proof.
+  unfold frame_eq; destruct om1 as [ m1 | ]; cbn; auto.
+  intros (m2 & H0 & H1); subst.
+  intros H.
+  eexists; intuition eauto.
+  destruct (notIn_dec x f1); auto.
+Qed. 
+
+(*
+Lemma frame_eq_res_eq f om1 om2:
+ frame_eq (fun x => In x f) om1 om2 ->
+ (forall m1 m2 x, om1 = Some m1 -> om2 = Some m2 -> notIn x f -> m1 x = m2 x) ->
+ res_eq om1 om2.
+Proof.
+  intros H H0; lapply (frame_eq_list_split f (fun _ => True) om1 om2 H); eauto.
+  clear H H0; unfold frame_eq, res_eq. destruct om1; cbn; firstorder.
+Qed.
+*)
+
+(** * Writing frames *)
+
+Fixpoint inst_wframe(i:inst): list R.t := 
+  match i with
+  | nil => nil
+  | a::i' => (fst a)::(inst_wframe i') 
+  end.
+
+Lemma inst_wframe_correct i m' old: forall m tmp, 
+  inst_prun ge i m tmp old = Some m' -> 
+  forall x, notIn x (inst_wframe i) -> m' x  = m x.
+Proof.
+  induction i as [|[y e] i']; cbn.
+  - intros m tmp H x H0; inversion_clear H; auto.
+  - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); cbn; try congruence.
+    replace (m x) with (assign m y v x); eauto.
+    rewrite assign_diff; auto.
+Qed.
+
+Lemma inst_prun_fequiv i old: forall m1 m2 tmp, 
+  frame_eq (fun x => In x (inst_wframe i)) (inst_prun ge i m1 tmp old) (inst_prun ge i m2 tmp old).
+Proof.
+  induction i as [|[y e] i']; cbn.
+  - intros m1 m2 tmp; eexists; intuition eauto.
+  - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); cbn; auto.
+    eapply frame_eq_list_split; eauto. clear IHi'.
+    intros m1' m2' x H1 H2.
+    lapply (inst_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto.
+    lapply (inst_wframe_correct i' m2' old (assign m2 y v) (assign tmp y v)); eauto.
+    intros Xm2 Xm1 H H0. destruct H. 
+    + subst. rewrite Xm1, Xm2; auto. rewrite !assign_eq. auto.
+    + rewrite <- notIn_iff in H0; tauto.
+Qed.
+
+Lemma inst_prun_None i m1 m2 tmp old: 
+  inst_prun ge i m1 tmp old = None -> 
+  inst_prun ge i m2 tmp old = None.
+Proof.
+  intros H; generalize (inst_prun_fequiv i old m1 m2 tmp).
+  rewrite H; cbn; auto.
+Qed.
+
+Lemma inst_prun_Some i m1 m2 tmp old m1': 
+  inst_prun ge i m1 tmp old = Some m1' -> 
+  res_eq (Some (frame_assign m2 (inst_wframe i) m1')) (inst_prun ge i m2 tmp old).
+Proof.
+  intros H; generalize (inst_prun_fequiv i old m1 m2 tmp).
+  rewrite H; cbn.
+  intros (m2' & H1 & H2).
+  eexists; intuition eauto.
+  rewrite frame_assign_def.
+  lapply (inst_wframe_correct i m2' old m2 tmp); eauto.
+  destruct (notIn_dec x (inst_wframe i)); auto.
+  intros X; rewrite X; auto.
+Qed.
+
+Fixpoint bblock_wframe(p:bblock): list R.t := 
+  match p with
+  | nil => nil
+  | i::p' => (inst_wframe i)++(bblock_wframe p') 
+  end.
+
+Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm: core.
+
+Lemma bblock_wframe_Permutation p p': 
+ Permutation p p' -> Permutation (bblock_wframe p)  (bblock_wframe p').
+Proof.
+  induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; cbn; auto.
+  - rewrite! app_assoc; auto.
+  - eapply Permutation_trans; eauto.
+Qed.
+
+(*
+Lemma bblock_wframe_correct p m' old: forall m, 
+  prun_iw p m old = Some m' -> 
+  forall x, notIn x (bblock_wframe p) -> m' x = m x.
+Proof.
+  induction p as [|i p']; cbn.
+  - intros m H; inversion_clear H; auto.
+  - intros m H x; rewrite notIn_app; intros (H1 & H2). 
+    remember (inst_prun i m old old) as om.
+    destruct om as [m1|]; cbn.
+    + eapply eq_trans.
+      eapply IHp'; eauto.
+      eapply inst_wframe_correct; eauto.
+    + inversion H.
+Qed.
+
+Lemma prun_iw_fequiv p old: forall m1 m2, 
+  frame_eq (fun x => In x (bblock_wframe p)) (prun_iw p m1 old) (prun_iw p m2 old).
+Proof.
+  induction p as [|i p']; cbn.
+  - intros m1 m2; eexists; intuition eauto.
+  - intros m1 m2; generalize (inst_prun_fequiv i old m1 m2 old).
+    remember (inst_prun i m1 old old) as om.
+    destruct om as [m1'|]; cbn.
+    + intros (m2' & H1 & H2). rewrite H1; cbn.
+    eapply frame_eq_list_split; eauto. clear IHp'.
+    intros m1'' m2'' x H3 H4. rewrite in_app_iff.
+    intros X X2. assert (X1: In x (inst_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. }
+    clear X.
+    lapply (bblock_wframe_correct p' m1'' old m1'); eauto.
+    lapply (bblock_wframe_correct p' m2'' old m2'); eauto.
+    intros Xm2' Xm1'. 
+    rewrite Xm1', Xm2'; auto.
+    + intro H; rewrite H; cbn; auto.
+Qed.
+
+Lemma prun_iw_equiv p m1 m2 old: 
+  (forall x, notIn x (bblock_wframe p) -> m1 x = m2 x) ->
+  res_eq (prun_iw p m1 old) (prun_iw p m2 old).
+Proof.
+  intros; eapply frame_eq_res_eq.
+  eapply prun_iw_fequiv.
+  intros m1' m2' x H1 H2 H0.Require
+  lapply (bblock_wframe_correct p m1' old m1); eauto.
+  lapply (bblock_wframe_correct p m2' old m2); eauto.
+  intros X2 X1; rewrite X1, X2; auto.
+Qed.
+*)
+
+(** * Checking that parallel semantics is deterministic *)
+
+Fixpoint is_det (p: bblock): Prop :=
+  match p with
+  | nil => True
+  | i::p' =>
+       disjoint (inst_wframe i) (bblock_wframe p') (* no WRITE-AFTER-WRITE *)
+    /\ is_det p'
+  end.
+
+Lemma is_det_Permutation p p': 
+ Permutation p p' -> is_det p -> is_det p'.
+Proof.
+  induction 1; cbn; auto.
+  - intros; intuition. eapply disjoint_incl_r. 2: eauto.
+    eapply Permutation_incl. eapply Permutation_sym. 
+    eapply bblock_wframe_Permutation; auto.
+  - rewrite! disjoint_app_r in * |- *. intuition.
+    rewrite disjoint_sym; auto. 
+Qed.
+
+Theorem is_det_correct p p':
+  Permutation p p' -> 
+  is_det p -> 
+  forall m old, res_eq (prun_iw ge p m old) (prun_iw ge p' m old).
+Proof.
+  induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; cbn; eauto.
+  - intros [H0 H1] m old.
+    remember (inst_prun ge i m old old) as om0.
+    destruct om0 as [ m0 | ]; cbn; auto.
+  - rewrite disjoint_app_r.
+    intros ([Z1 Z2] & Z3 & Z4) m old.
+    remember (inst_prun ge i2 m old old) as om2.
+    destruct om2 as [ m2 | ]; cbn; auto.
+    + remember (inst_prun ge i1 m old old) as om1.
+      destruct om1 as [ m1 | ]; cbn; auto.
+      * lapply (inst_prun_Some i2 m m1 old old m2); cbn; auto.
+        lapply (inst_prun_Some i1 m m2 old old m1); cbn; auto.
+        intros (m1' & Hm1' & Xm1') (m2' & Hm2' & Xm2').
+        rewrite Hm1', Hm2'; cbn.
+        eapply prun_iw_equiv.
+        intros x; rewrite <- Xm1', <- Xm2'. clear Xm2' Xm1' Hm1' Hm2' m1' m2'.
+        rewrite frame_assign_def.
+        rewrite disjoint_sym in Z1; unfold disjoint in Z1.
+        destruct (notIn_dec x (inst_wframe i1)) as [ X1 | X1 ].
+        { rewrite frame_assign_def; destruct (notIn_dec x (inst_wframe i2)) as [ X2 | X2 ]; auto.
+          erewrite (inst_wframe_correct i2 m2 old m old); eauto.
+          erewrite (inst_wframe_correct i1 m1 old m old); eauto.
+        }
+        rewrite frame_assign_notIn; auto.
+     * erewrite inst_prun_None; eauto. cbn; auto.
+   + remember (inst_prun ge i1 m old old) as om1.
+     destruct om1 as [ m1 | ]; cbn; auto.
+     erewrite inst_prun_None; eauto.
+  - intros; eapply res_eq_trans.
+    eapply IHPermutation1; eauto.
+    eapply IHPermutation2; eauto.
+    eapply is_det_Permutation; eauto.
+Qed.
+
+(** * Standard Frames *)
+
+Fixpoint exp_frame (e: exp): list R.t :=
+  match e with
+  | PReg x => x::nil
+  | Op o le => list_exp_frame le
+  | Old e => exp_frame e
+  end
+with list_exp_frame (le: list_exp): list R.t :=
+  match le with
+  | Enil => nil
+  | Econs e le' => exp_frame e ++ list_exp_frame le'
+  | LOld le => list_exp_frame le
+  end.
+
+Lemma exp_frame_correct e old1 old2: 
+  (forall x, In x (exp_frame e) -> old1 x = old2 x) ->
+  forall m1 m2, (forall x, In x (exp_frame e) -> m1 x = m2 x) ->
+   (exp_eval ge e m1 old1)=(exp_eval ge e m2 old2).
+Proof.
+  induction e using exp_mut with (P0:=fun l => (forall x, In x (list_exp_frame l) -> old1 x = old2 x) -> forall m1 m2, (forall x, In x (list_exp_frame l) -> m1 x = m2 x) ->
+   (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); cbn; auto.
+  - intros H1 m1 m2 H2; rewrite H2; auto.
+  - intros H1 m1 m2 H2; erewrite IHe; eauto.
+  - intros H1 m1 m2 H2; erewrite IHe, IHe0; eauto; 
+    intros; (eapply H1 || eapply H2); rewrite in_app_iff; auto.
+Qed.
+
+Fixpoint inst_frame (i: inst): list R.t :=
+  match i with
+  | nil => nil
+  | a::i' => (fst a)::(exp_frame (snd a) ++ inst_frame i') 
+  end.
+
+Lemma inst_wframe_frame i x: In x (inst_wframe i) -> In x (inst_frame i).
+Proof.
+  induction i as [ | [y e] i']; cbn; intuition.
+Qed.
+
+
+Lemma inst_frame_correct i wframe old1 old2: forall m tmp1 tmp2,
+  (disjoint (inst_frame i) wframe) ->
+  (forall x, notIn x wframe -> old1 x = old2 x) ->
+  (forall x, notIn x wframe -> tmp1 x = tmp2 x) ->
+  inst_prun ge i m tmp1 old1 = inst_prun ge i m tmp2 old2.
+Proof.
+  induction i as [|[x e] i']; cbn; auto.
+  intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l.
+  intros (H1 & H2 & H3) H6 H7.
+  replace (exp_eval ge e tmp1 old1) with (exp_eval ge e tmp2 old2).
+  - destruct (exp_eval ge e tmp2 old2); auto.
+    eapply IHi'; eauto. 
+    cbn; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); cbn; auto. 
+  - unfold disjoint in H2; apply exp_frame_correct.
+    intros;rewrite H6; auto.
+    intros;rewrite H7; auto.
+Qed.
+
+(** * Parallelizability *)
+
+Fixpoint pararec (p: bblock) (wframe: list R.t): Prop :=
+  match p with
+  | nil => True
+  | i::p' =>
+       disjoint (inst_frame i) wframe (* no USE-AFTER-WRITE *)
+    /\ pararec p' ((inst_wframe i) ++ wframe)
+  end.
+
+Lemma pararec_disjoint (p: bblock): forall wframe, pararec p wframe -> disjoint (bblock_wframe p) wframe.
+Proof.
+  induction p as [|i p']; cbn.
+  - unfold disjoint; cbn; intuition.
+  - intros wframe [H0 H1]; rewrite disjoint_app_l. 
+    generalize (IHp' _ H1).
+    rewrite disjoint_app_r. intuition. 
+    eapply disjoint_incl_l. 2: eapply H0.
+    unfold incl. eapply inst_wframe_frame; eauto.
+Qed.
+
+Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p.
+Proof.
+  induction p as [|i p']; cbn; auto.
+  intros wframe [H0 H1]. generalize (pararec_disjoint _ _ H1). rewrite disjoint_app_r.
+  intuition. 
+  - apply disjoint_sym; auto.
+  - eapply IHp'. eauto.
+Qed.
+
+Lemma pararec_correct p old: forall wframe m,
+  pararec p wframe -> 
+  (forall x, notIn x wframe -> m x = old x) ->
+  run ge p m = prun_iw ge p m old.
+Proof.
+  elim p; clear p; cbn; auto.
+  intros i p' X wframe m [H H0] H1.
+  erewrite inst_run_prun, inst_frame_correct; eauto.
+  remember (inst_prun ge i m old old) as om0.
+  destruct om0 as [m0 | ]; try congruence.
+  eapply X; eauto.
+  intro x; rewrite notIn_app. intros [H3 H4].
+  rewrite <- H1; auto.
+  eapply inst_wframe_correct; eauto.
+Qed.
+
+Definition parallelizable (p: bblock) := pararec p nil.
+
+Theorem parallelizable_correct p m om':
+  parallelizable p -> (prun ge p m om' <-> res_eq om' (run ge p m)).
+Proof.
+  intros H. constructor 1.
+  - intros (p' & H0 & H1). eapply res_eq_trans; eauto.
+    erewrite pararec_correct; eauto.
+    eapply res_eq_sym.
+    eapply is_det_correct; eauto.
+    eapply pararec_det; eauto.
+  - intros; unfold prun. 
+    eexists. constructor 1. 2: apply Permutation_refl. 
+    erewrite pararec_correct in H0; eauto.
+Qed.
+
+End PARALLELI.
+
+End ParallelizablityChecking.
+
+
+(** * We assume a datatype [PseudoRegSet.t] refining [list R.t] *)
+
+(** 
+This data-refinement is given by an abstract "invariant" match_frame below, 
+preserved by the following operations.
+*)
+
+Module Type PseudoRegSet.
+
+Declare Module R: PseudoRegisters.
+
+Parameter t: Type.
+Parameter match_frame: t -> (list R.t) -> Prop.
+
+Parameter empty: t.
+Parameter empty_match_frame: match_frame empty nil.
+
+Parameter add: R.t -> t -> t.
+Parameter add_match_frame: forall s x l, match_frame s l -> match_frame (add x s) (x::l).
+
+Parameter union: t -> t -> t.
+Parameter union_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> match_frame (union s1 s2) (l1++l2).
+
+Parameter is_disjoint: t -> t -> bool.
+Parameter is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2. 
+
+End PseudoRegSet.
+
+
+Lemma lazy_andb_bool_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true.
+Proof.
+  destruct b1, b2; intuition.
+Qed.
+
+
+
+
+Module ParallelChecks (L: SeqLanguage) (S:PseudoRegSet with Module R:=L.LP.R).
+
+Include ParallelizablityChecking L.
+
+Section PARALLEL2.
+Variable ge: genv.
+
+Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame: core.
+
+(** Now, refinement of each operation toward parallelizable *)
+
+Fixpoint inst_wsframe(i:inst): S.t :=
+  match i with
+  | nil => S.empty
+  | a::i' => S.add (fst a) (inst_wsframe i') 
+  end.
+
+Lemma inst_wsframe_correct i: S.match_frame (inst_wsframe i) (inst_wframe i).
+Proof.
+  induction i; cbn; auto.
+Qed.
+
+Fixpoint exp_sframe (e: exp): S.t :=
+  match e with
+  | PReg x => S.add x S.empty
+  | Op o le => list_exp_sframe le
+  | Old e => exp_sframe e
+  end
+with list_exp_sframe (le: list_exp): S.t :=
+  match le with
+  | Enil => S.empty
+  | Econs e le' => S.union (exp_sframe e) (list_exp_sframe le')
+  | LOld le => list_exp_sframe le
+  end.
+
+Lemma exp_sframe_correct e: S.match_frame (exp_sframe e) (exp_frame e).
+Proof.
+  induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); cbn; auto.
+Qed.
+
+Fixpoint inst_sframe (i: inst): S.t :=
+  match i with
+  | nil => S.empty
+  | a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (inst_sframe i'))
+  end.
+
+Local Hint Resolve exp_sframe_correct: core.
+
+Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i).
+Proof.
+  induction i as [|[y e] i']; cbn; auto.
+Qed.
+
+Local Hint Resolve inst_wsframe_correct inst_sframe_correct: core.
+
+Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool :=
+  match p with
+  | nil => true
+  | i::p' =>
+       S.is_disjoint (inst_sframe i) wsframe (* no USE-AFTER-WRITE *)
+    &&& is_pararec p' (S.union (inst_wsframe i) wsframe)
+  end.
+
+Lemma is_pararec_correct (p: bblock): forall s l, S.match_frame s l -> (is_pararec p s)=true -> (pararec p l).
+Proof.
+  induction p; cbn; auto.
+  intros s l H1 H2; rewrite lazy_andb_bool_true in H2. destruct H2 as [H2 H3].
+  constructor 1; eauto.
+Qed.
+
+Definition is_parallelizable (p: bblock) := is_pararec p S.empty.
+
+Lemma is_para_correct_aux p: is_parallelizable p = true -> parallelizable p.
+Proof.
+  unfold is_parallelizable, parallelizable; intros; eapply is_pararec_correct; eauto.
+Qed.
+
+Theorem is_parallelizable_correct p:
+  is_parallelizable p = true -> forall m om', (prun ge p m om' <-> res_eq om' (run ge p m)).
+Proof.
+  intros; apply parallelizable_correct.
+  apply is_para_correct_aux. auto.
+Qed.
+
+End PARALLEL2.
+End ParallelChecks.
+
+
+
+(** * Implementing the datatype [PosPseudoRegSet.t] refining [list R.t] *)
+
+(* This data-refinement is given by an abstract "invariant" match_frame below, 
+preserved by the following operations.
+*)
+
+Require Import PArith.
+Require Import MSets.MSetPositive.
+
+Module PosPseudoRegSet <: PseudoRegSet with Module R:=Pos.
+
+Module R:=Pos.
+
+
+Definition t:=PositiveSet.t.
+
+Definition match_frame (s:t) (l:list R.t): Prop
+ := forall x, PositiveSet.In x s <-> In x l.
+
+Definition empty:=PositiveSet.empty.
+
+Lemma empty_match_frame: match_frame empty nil.
+Proof.
+  unfold match_frame, empty, PositiveSet.In; cbn; intuition.
+Qed.
+
+Definition add: R.t -> t -> t := PositiveSet.add.
+
+Lemma add_match_frame: forall s x l, match_frame s l -> match_frame (add x s) (x::l).
+Proof.
+  unfold match_frame, add; cbn. 
+  intros s x l H y. rewrite PositiveSet.add_spec, H.
+  intuition. 
+Qed.
+
+Definition union: t -> t -> t := PositiveSet.union.
+Lemma union_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> match_frame (union s1 s2) (l1++l2).
+Proof.
+  unfold match_frame, union. 
+  intros s1 s2 l1 l2 H1 H2 x. rewrite PositiveSet.union_spec, H1, H2.
+  intuition. 
+Qed.
+
+Fixpoint is_disjoint (s s': PositiveSet.t) : bool :=
+  match s with
+  | PositiveSet.Leaf => true
+  | PositiveSet.Node l o r =>
+    match s' with
+    | PositiveSet.Leaf => true
+    | PositiveSet.Node l' o' r' => 
+      if (o &&& o') then false else (is_disjoint l l' &&& is_disjoint r r')
+    end
+  end.
+
+Lemma is_disjoint_spec_true s: forall s', is_disjoint s s' = true -> forall x, PositiveSet.In x s -> PositiveSet.In x s' -> False.
+Proof.
+  unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; cbn; try discriminate.
+  destruct s' as [|l' o' r']; cbn; try discriminate.
+  intros X.
+  assert (H: ~(o = true /\ o'=true) /\ is_disjoint l l' = true /\ is_disjoint r r'=true).
+  { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); cbn in X; intuition. }
+  clear X; destruct H as (H & H1 & H2).
+  destruct x as [i|i|]; cbn; eauto.
+Qed.
+
+Lemma is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2.
+Proof.
+  unfold match_frame, disjoint.
+  intros s1 s2 l1 l2 H1 H2 H3 x.
+  rewrite <- notIn_iff, <- H1, <- H2.
+  intros H4 H5; eapply is_disjoint_spec_true; eauto.
+Qed.
+
+End PosPseudoRegSet.
diff --git a/scheduling/abstractbb/README.md b/scheduling/abstractbb/README.md
new file mode 100644
index 00000000..69e5defc
--- /dev/null
+++ b/scheduling/abstractbb/README.md
@@ -0,0 +1,12 @@
+# Coq sources of AbstractBasicBlocks 
+
+- [AbstractBasicBlocksDef](AbstractBasicBlocksDef.v): syntax and sequential semantics of abstract basic blocks (on which we define our analyzes).
+This syntax and semantics is parametrized in order to adapt the language for different concrete basic block languages.
+
+- [Parallelizability](Parallelizability.v): define the parallel semantics and the 'is_parallelizable' function which tests whether the sequential run of a given abstract basic block is the same than a parallel run.
+
+- [DepTreeTheory](DepTreeTheory.v): defines a theory of dependency trees, such that two basic blocks with the same dependency tree have the same sequential semantics. In practice, permuting the instructions inside a basic block while perserving the dependencies of assignments should not change the dependency tree. The idea is to verify list schedulings, following ideas of [Formal verification of translation validators proposed by Tristan and Leroy](https://hal.inria.fr/inria-00289540/).
+
+- [ImpDep](ImpDep.v): adds a hash-consing mechanism to trees of [DepTreeTheory](DepTreeTheory.v), and thus provides an efficient "equality" test (a true answer ensures that the two basic blocks in input have the same sequential semantics) in order to check the correctness of list schedulings.
+
+- [DepExample](DepExample.v) defines a toy language (syntax and semantics); [DepExampleEqTest](DepExampleEqTest.v) defines a compiler of the toy language into abstract basic blocks and derives an equality test for the toy language; [DepExampleParallelTest](DepExampleParallelTest.v) derives a parallelizability test from the previous compiler; [DepExampleDemo](DepExampleDemo.v) is a test-suite for both tetsts.
diff --git a/scheduling/abstractbb/SeqSimuTheory.v b/scheduling/abstractbb/SeqSimuTheory.v
new file mode 100644
index 00000000..df6b9963
--- /dev/null
+++ b/scheduling/abstractbb/SeqSimuTheory.v
@@ -0,0 +1,397 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** A theory for checking/proving simulation by symbolic execution.
+
+*)
+
+
+Require Coq.Logic.FunctionalExtensionality. (* not really necessary -- see lemma at the end *)
+Require Setoid. (* in order to rewrite <-> *)
+Require Export AbstractBasicBlocksDef.
+Require Import List.
+Require Import ImpPrelude.
+Import HConsingDefs.
+
+
+Module SimuTheory (L: SeqLanguage).
+
+Export L.
+Export LP.
+
+Inductive term :=
+  | Input (x:R.t)
+  | App (o: op) (l: list_term)
+with list_term :=
+  | LTnil
+  | LTcons (t:term) (l:list_term)
+  .
+
+Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value :=
+  match t with
+  | Input x => Some (m x)
+  | App o l =>
+     match list_term_eval ge l m with
+     | Some v => op_eval ge o v
+     | _ => None
+     end
+  end
+with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) :=
+  match l with
+  | LTnil => Some nil
+  | LTcons t l' => 
+    match term_eval ge t m, list_term_eval ge l' m with
+    | Some v, Some lv => Some (v::lv)
+    | _, _ => None
+    end
+  end.
+
+(** The (abstract) symbolic memory state *)
+Record smem :=
+{
+   pre: genv -> mem -> Prop; (**r pre-condition expressing that the computation has not yet abort on a None. *)
+   post:> R.t -> term (**r the output term computed on each pseudo-register *)
+}.
+
+(** Initial symbolic memory state *)
+Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}.
+
+Fixpoint exp_term (e: exp) (d old: smem) : term :=
+  match e with
+  | PReg x => d x
+  | Op o le => App o (list_exp_term le d old)
+  | Old e => exp_term e old old
+  end
+with list_exp_term (le: list_exp) (d old: smem) : list_term :=
+  match le with
+  | Enil => LTnil
+  | Econs e le' => LTcons (exp_term e d old) (list_exp_term le' d old)
+  | LOld le => list_exp_term le old old
+  end.
+
+
+(** assignment of the symbolic memory state *)
+Definition smem_set (d:smem) x (t:term) := 
+  {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m));
+     post:=fun y => if R.eq_dec x y then t else d y |}.
+
+(** Simulation theory: the theorem [bblock_smem_simu] ensures that the simulation between two abstract basic blocks is implied by the simulation between their symbolic execution. *)
+Section SIMU_THEORY.
+
+Variable ge: genv.
+
+Lemma set_spec_eq d x t m:
+ term_eval ge (smem_set d x t x) m = term_eval ge t m.
+Proof.
+  unfold smem_set; cbn; case (R.eq_dec x x); try congruence.
+Qed.
+
+Lemma set_spec_diff d x y t m:
+  x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m.
+Proof.
+  unfold smem_set; cbn; case (R.eq_dec x y); try congruence.
+Qed.
+
+Fixpoint inst_smem (i: inst) (d old: smem): smem :=
+  match i with
+  | nil => d
+  | (x, e)::i' =>
+     let t:=exp_term e d old in
+     inst_smem i' (smem_set d x t) old
+  end.
+
+Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem :=
+  match p with
+  | nil => d
+  | i::p' =>
+     let d':=inst_smem i d d in
+     bblock_smem_rec p' d'
+  end.
+
+Definition bblock_smem: bblock -> smem
+ := fun p => bblock_smem_rec p smem_empty.
+
+Lemma inst_smem_pre_monotonic i old: forall d m,
+  (pre (inst_smem i d old) ge m) -> (pre d ge m).
+Proof.
+  induction i as [|[y e] i IHi]; cbn; auto.
+  intros d a H; generalize (IHi _ _ H); clear H IHi.
+  unfold smem_set; cbn; intuition.
+Qed.
+
+Lemma bblock_smem_pre_monotonic p: forall d m,
+  (pre (bblock_smem_rec p d) ge m) -> (pre d ge m).
+Proof.
+  induction p as [|i p' IHp']; cbn; eauto.
+  intros d a H; eapply inst_smem_pre_monotonic; eauto.
+Qed.
+
+Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic: core.
+
+Lemma term_eval_exp e (od:smem) m0 old:
+  (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall (d:smem) m1,
+   (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+    term_eval ge (exp_term e d od) m0 = exp_eval ge e m1 old.
+Proof.
+  intro H.
+  induction e using exp_mut with
+    (P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old);
+  cbn; auto.
+  - intros; erewrite IHe; eauto.
+  - intros. erewrite IHe, IHe0; eauto. 
+Qed.
+
+Lemma inst_smem_abort i m0 x old: forall (d:smem),
+    pre (inst_smem i d old) ge m0 ->
+    term_eval ge (d x) m0 = None ->
+    term_eval ge (inst_smem i d old x) m0 = None.
+Proof.
+  induction i as [|[y e] i IHi]; cbn; auto.
+  intros d VALID H; erewrite IHi; eauto. clear IHi.
+  unfold smem_set; cbn; destruct (R.eq_dec y x); auto.
+  subst;
+  generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID.
+  unfold smem_set; cbn. intuition congruence.
+Qed.
+
+Lemma block_smem_rec_abort p m0 x: forall d,
+    pre (bblock_smem_rec p d) ge m0 ->
+    term_eval ge (d x) m0 = None ->
+    term_eval ge (bblock_smem_rec p d x) m0 = None.
+Proof.
+  induction p; cbn; auto.
+  intros d VALID H; erewrite IHp; eauto. clear IHp.
+  eapply inst_smem_abort; eauto.
+Qed.
+
+Lemma inst_smem_Some_correct1 i m0 old (od:smem): 
+  (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall (m1 m2: mem) (d: smem), 
+  inst_run ge i m1 old = Some m2 -> 
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+   forall x, term_eval ge (inst_smem i d od x) m0 = Some (m2 x).
+Proof.
+  intro X; induction i as [|[x e] i IHi]; cbn; intros m1 m2 d H.
+  - inversion_clear H; eauto.
+  - intros H0 x0.
+    destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence.
+    refine (IHi _ _ _ _ _ _); eauto.
+    clear x0; intros x0.
+    unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto.
+    subst; erewrite term_eval_exp; eauto.
+Qed.
+
+Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem), 
+ run ge p m1 = Some m2 -> 
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x).
+Proof.
+  Local Hint Resolve inst_smem_Some_correct1: core.
+  induction p as [ | i p]; cbn; intros m1 m2 d H.
+  - inversion_clear H; eauto.
+  - intros H0 x0.
+    destruct (inst_run ge i m1 m1) eqn: Heqov.
+    + refine (IHp _ _ _ _ _ _); eauto.
+    + inversion H. 
+Qed.
+
+Lemma bblock_smem_Some_correct1 p m0 m1:
+   run ge p m0 = Some m1
+   -> forall x, term_eval ge (bblock_smem p x) m0 = Some (m1 x).
+Proof.
+  intros; eapply bblocks_smem_rec_Some_correct1; eauto.
+Qed.
+
+Lemma inst_smem_None_correct i m0 old (od: smem):
+   (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall m1 d, pre (inst_smem i d od) ge m0 ->
+   (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  inst_run ge i m1 old = None -> exists x, term_eval ge (inst_smem i d od x) m0 = None.
+Proof.
+  intro X; induction i as [|[x e] i IHi]; cbn; intros m1 d.
+  - discriminate.
+  - intros VALID H0.
+    destruct (exp_eval ge e m1 old) eqn: Heqov.
+    + refine (IHi _ _ _ _); eauto.
+      intros x0; unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto.
+      subst; erewrite term_eval_exp; eauto.
+    + intuition.
+      constructor 1 with (x:=x); cbn.
+      apply inst_smem_abort; auto.
+      rewrite set_spec_eq. 
+      erewrite term_eval_exp; eauto.
+Qed.
+
+Lemma inst_smem_Some_correct2 i m0 old (od: smem):
+  (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall (m1 m2: mem) d, 
+  pre (inst_smem i d od) ge m0 ->
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  (forall x, term_eval ge (inst_smem i d od x) m0 = Some (m2 x)) ->
+  res_eq (Some m2) (inst_run ge i m1 old).
+Proof.
+  intro X.
+  induction i as [|[x e] i IHi]; cbn; intros m1 m2 d VALID H0.
+  - intros H; eapply ex_intro; intuition eauto.
+    generalize (H0 x); rewrite H.
+    congruence.
+  - intros H.
+    destruct (exp_eval ge e m1 old) eqn: Heqov.
+    + refine (IHi _ _ _ _ _ _); eauto.
+      intros x0; unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto.
+      subst; erewrite term_eval_exp; eauto.
+    + generalize (H x).
+      rewrite inst_smem_abort; discriminate || auto.
+      rewrite set_spec_eq. 
+      erewrite term_eval_exp; eauto.
+Qed.
+
+Lemma bblocks_smem_rec_Some_correct2 p m0: forall (m1 m2: mem) d, 
+  pre (bblock_smem_rec p d) ge m0 ->
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  (forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x)) ->
+    res_eq (Some m2) (run ge p m1).
+Proof.
+  induction p as [|i p]; cbn; intros m1 m2 d VALID H0.
+  - intros H; eapply ex_intro; intuition eauto.
+    generalize (H0 x); rewrite H.
+    congruence.
+  - intros H.
+     destruct (inst_run ge i m1 m1) eqn: Heqom.
+    + refine (IHp _ _ _ _ _ _); eauto.
+    + assert (X: exists x, term_eval ge (inst_smem i d d x) m0 = None).
+      { eapply inst_smem_None_correct; eauto. }
+      destruct X as [x H1].
+      generalize (H x).
+      erewrite block_smem_rec_abort; eauto.
+      congruence.
+Qed.
+
+Lemma bblock_smem_Some_correct2 p m0 m1:
+  pre (bblock_smem p) ge m0 ->
+  (forall x, term_eval ge (bblock_smem p x) m0 = Some (m1 x))
+  -> res_eq (Some m1) (run ge p m0).
+Proof.
+  intros; eapply bblocks_smem_rec_Some_correct2; eauto.
+Qed.
+
+Lemma inst_valid i m0 old (od:smem):
+  (forall x, term_eval ge (od x) m0 = Some (old x)) ->
+  forall (m1 m2: mem) (d: smem), 
+  pre d ge m0 ->
+  inst_run ge i m1 old = Some m2 ->
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+   pre (inst_smem i d od) ge m0.
+Proof.
+  induction i as [|[x e] i IHi]; cbn; auto.
+  intros Hold m1 m2 d VALID0 H Hm1.
+  destruct (exp_eval ge e m1 old) eqn: Heq; cbn; try congruence.
+  eapply IHi; eauto.
+  + unfold smem_set in * |- *; cbn. 
+    rewrite Hm1; intuition congruence.
+  + intros x0. unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto.
+    subst; erewrite term_eval_exp; eauto.
+Qed.
+
+
+Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem), 
+  pre d ge m0 ->
+  run ge p m1 = Some m2 -> 
+  (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
+  pre (bblock_smem_rec p d) ge m0.
+Proof.
+  Local Hint Resolve inst_valid: core.
+  induction p as [ | i p]; cbn; intros m1 d H; auto.
+  intros H0 H1.
+  destruct (inst_run ge i m1 m1) eqn: Heqov; eauto.
+  congruence.
+Qed.
+
+Lemma bblock_smem_valid p m0 m1:
+  run ge p m0 = Some m1 ->
+  pre (bblock_smem p) ge m0.
+Proof.
+  intros; eapply block_smem_rec_valid; eauto.
+  unfold smem_empty; cbn. auto.
+Qed.
+
+Definition smem_valid ge d m := pre d ge m /\ forall x, term_eval ge (d x) m <> None.
+
+Definition smem_simu (d1 d2: smem): Prop :=
+     (forall m, smem_valid ge d1 m -> smem_valid ge d2 m)
+  /\ (forall m0 x, smem_valid ge d1 m0 -> 
+                   term_eval ge (d1 x) m0 = term_eval ge (d2 x) m0).
+
+
+Theorem bblock_smem_simu p1 p2:
+   smem_simu (bblock_smem p1) (bblock_smem p2) ->
+   bblock_simu ge p1 p2.
+Proof.
+  Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core.
+  intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-.
+  destruct (run ge p1 m) as [m1|] eqn: RUN1; cbn; try congruence.
+  assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto.
+  eapply bblock_smem_Some_correct2; eauto.
+  + destruct (INCL m); intuition eauto.
+    congruence.
+  + intro x; erewrite <- EQUIV; intuition eauto.
+    congruence.
+Qed.
+
+Lemma smem_valid_set_decompose_1 d t x m:
+  smem_valid ge (smem_set d x t) m -> smem_valid ge d m.
+Proof.
+  unfold smem_valid; intros ((PRE1 & PRE2) & VALID); split.
+  + intuition.
+  + intros x0 H. case (R.eq_dec x x0).
+    * intuition congruence.
+    * intros DIFF; eapply VALID. erewrite set_spec_diff; eauto.
+Qed.
+
+Lemma smem_valid_set_decompose_2 d t x m:
+  smem_valid ge (smem_set d x t) m -> term_eval ge t m <> None.
+Proof.
+  unfold smem_valid; intros ((PRE1 & PRE2) & VALID) H.
+  generalize (VALID x); rewrite set_spec_eq.
+  tauto.
+Qed.
+
+Lemma smem_valid_set_proof d x t m:
+  smem_valid ge d m -> term_eval ge t m <> None -> smem_valid ge (smem_set d x t) m.
+Proof.
+  unfold smem_valid; intros (PRE & VALID) PREt. split.
+  + split; auto.
+  + intros x0; unfold smem_set; cbn; case (R.eq_dec x x0); intros; subst; auto.
+Qed.
+
+
+End SIMU_THEORY.
+
+(** REMARK: this theorem reformulates the lemma above in a more abstract way (but relies on functional_extensionality axiom).
+*)
+Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:=
+   forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)).
+
+Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m).
+Proof.
+  unfold smem_correct; cbn; intros m'; split.
+  + intros; split.
+    * eapply bblock_smem_valid; eauto.
+    * eapply bblock_smem_Some_correct1; eauto.
+  + intros (H1 & H2).
+    destruct (bblock_smem_Some_correct2 ge p m m') as (m2 & X & Y); eauto.
+    rewrite X. f_equal.
+    apply FunctionalExtensionality.functional_extensionality; auto.
+Qed.
+
+End SimuTheory.