abstract_bb: few improvements while writing the paper

6 files changed, 294 insertions, 251 deletions

diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v
index 8f6b05b7..ea55b735 100644
--- a/mppa_k1c/abstractbb/ImpSimuTest.v
+++ b/mppa_k1c/abstractbb/ImpSimuTest.v
@@ -44,7 +44,32 @@ End ISeqLanguage.
 
 Module Type ImpDict.
 
-Include PseudoRegDictionary.
+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.
 
@@ -95,9 +120,10 @@ Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuI
 
 Module CoreL:=L.
 
-Module ST := SimuTheory L Dict.
+Module ST := SimuTheory L.
 
 Import ST.
+Import Terms.
 
 Definition term_set_hid (t: term) (hid: hashcode): term :=
   match t with
@@ -212,9 +238,14 @@ Hint Resolve hLTcons_correct: wlp.
 
 (* Second, we use these hashed constructors ! *)
 
-Record hsmem:= {hpre: list term; hpost: Dict.t term}.
+Record hsmem:= {hpre: list term; hpost:> Dict.t term}.
 
-Coercion hpost: hsmem >-> Dict.t.
+(** 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 
@@ -223,9 +254,9 @@ Definition hsmem_get (d:hsmem) x: ?? term :=
    end.
 
 Lemma hsmem_get_correct (d:hsmem) x:
-  WHEN hsmem_get d x ~> t THEN forall ge m, term_eval ge t m = smem_eval ge d x m.
+  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, smem_eval, smem_get; destruct (Dict.get d x); wlp_simplify.
+  unfold hsmem_get, hsmem_post_eval; destruct (Dict.get d x); wlp_simplify.
 Qed.
 Global Opaque hsmem_get.
 Hint Resolve hsmem_get_correct: wlp.
@@ -234,17 +265,17 @@ 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 -> smem_eval ge hd x m = (smem_eval ge d x 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 -> smem_eval ge hd x m <> None.
+ 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 -> smem_eval ge hd x m <> None.
+ 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.
@@ -256,14 +287,14 @@ Definition naive_set (hd:hsmem) x (t:term) :=
 
 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 = term_eval ge t m) ->
+    (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, smem_eval ge d x m <> None). { 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 * |- *; simpl.
     intuition (subst; eauto).
     + eapply smem_valid_set_proof; eauto.
@@ -272,7 +303,7 @@ Proof.
       intros X1; exploit smem_valid_set_decompose_2; eauto.
       rewrite <- EQT; eauto.
     + exploit smem_valid_set_decompose_1; eauto.
-  - clear DM0. unfold smem_eval, smem_eval, smem_get in * |- *; simpl.
+  - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl.
     Local Hint Resolve smem_valid_set_decompose_1.
     intros; case (R.eq_dec x x0).
     + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto.
@@ -282,7 +313,7 @@ Local Hint Resolve naive_set_correct.
 
 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 -> smem_eval ge hd1 x m = smem_eval ge hd2 x 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.
@@ -363,11 +394,9 @@ Global Opaque hterm_append.
 
 Definition smart_set (hd:hsmem) x (ht:term) :=
      match ht with
-     | Input _ _ =>
-       DO ot <~ hsmem_get hd x;;
-       DO b <~ phys_eq ot ht;;
-       if b then
-          RET (hd.(hpost))
+     | 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)
@@ -379,12 +408,12 @@ Definition smart_set (hd:hsmem) x (ht:term) :=
 
 Lemma smart_set_correct hd x ht:
   WHEN smart_set hd x ht ~> d THEN
-    forall ge m y, smem_eval ge d y m = smem_eval ge (Dict.set hd x ht) y m.
+    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 smem_eval at 2; unfold smem_get; simpl; case (R.eq_dec x y).
-  - intros; subst. rewrite Dict.set_spec_eq. congruence.
-  - intros; rewrite Dict.set_spec_diff; auto.
+  unfold hsmem_post_eval; simpl. case (R.eq_dec x0 y).
+  - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. simpl; congruence.
+  - intros; rewrite Dict.set_spec_diff, Dict.rem_spec_diff; auto.
 Qed.
 (*Local Hint Resolve smart_set_correct: wlp.*)
 Global Opaque smart_set.
@@ -400,7 +429,7 @@ Definition hsmem_set (hd:hsmem) x (t:term) :=
 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 = term_eval ge t m) ->
+    (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.
@@ -414,9 +443,9 @@ Proof.
   - intros m x0 ALLVALID; rewrite SMART.
     destruct (term_eval ge ht m) eqn: Hht.
     * case (R.eq_dec x x0).
-      + intros; subst. unfold smem_eval; unfold smem_get; simpl. rewrite !Dict.set_spec_eq.
+      + intros; subst. unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_eq.
         erewrite LIFT, EFFECT; eauto.
-      + intros; unfold smem_eval; unfold smem_get; simpl. rewrite !Dict.set_spec_diff; auto.
+      + intros; unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_diff; auto.
     * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto.
 Qed.
 Local Hint Resolve hsmem_set_correct: wlp.
@@ -439,53 +468,53 @@ Qed.
 Local Hint Resolve exp_hterm_correct: wlp.
 *)
 
-Fixpoint hexp_term (e: exp) (d od: hsmem): ?? term :=
+Fixpoint exp_hterm (e: exp) (hd hod: hsmem): ?? term :=
   match e with
-  | PReg x => hsmem_get d x
+  | PReg x => hsmem_get hd x
   | Op o le =>
-     DO lt <~ hlist_exp_term le d od;; 
+     DO lt <~ list_exp_hterm le hd hod;; 
      hApp o lt
-  | Old e => hexp_term e od od
+  | Old e => exp_hterm e hod hod
   end
-with hlist_exp_term (le: list_exp) (d od: hsmem): ?? list_term :=
+with list_exp_hterm (le: list_exp) (hd hod: hsmem): ?? list_term :=
   match le with
   | Enil => hLTnil tt
   | Econs e le' => 
-     DO t <~ hexp_term e d od;;
-     DO lt <~ hlist_exp_term le' d od;;
+     DO t <~ exp_hterm e hd hod;;
+     DO lt <~ list_exp_hterm le' hd hod;;
      hLTcons t lt
-  | LOld le => hlist_exp_term le od od
+  | LOld le => list_exp_hterm le hod hod
   end.
 
-Lemma hexp_term_correct_x ge e hod od:
+Lemma exp_hterm_correct_x ge e hod od:
    smem_model ge od hod ->
   forall hd d,
    smem_model ge d hd ->
-  WHEN hexp_term e hd hod ~> t THEN forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = term_eval ge (exp_term e d od) m.
+  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 hlist_exp_term le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = list_term_eval ge (list_exp_term le d od) m); 
-     unfold smem_model, smem_eval in * |- * ; simpl; wlp_simplify.
+     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 * |- * ; simpl; wlp_simplify.
   - rewrite H1, <- H4; auto.
   - rewrite H4, <- H0; simpl; auto.
   - rewrite H5, <- H0, <- H4; simpl; auto.
 Qed.
-Global Opaque hexp_term.
+Global Opaque exp_hterm.
 
-Lemma hexp_term_correct e hd hod:
-  WHEN hexp_term 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 = term_eval ge (exp_term e d od) m.
+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 hexp_term_correct_x; eauto.
+  unfold wlp; intros; eapply exp_hterm_correct_x; eauto.
 Qed.
-Hint Resolve hexp_term_correct: wlp.
+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 <~ hexp_term e hd hod;;
+     DO ht <~ exp_hterm e hd hod;;
      DO nd <~ hsmem_set hd x ht;;
      hinst_smem i' nd hod
   end.
@@ -503,37 +532,41 @@ Local Hint Resolve hinst_smem_correct: wlp.
 (* logging info: we log the number of inst-instructions passed ! *)
 Variable log_new_inst: unit -> ?? unit. 
 
-Fixpoint hbblock_smem_rec (p: bblock) (d: hsmem): ?? hsmem :=
+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;;
-     hbblock_smem_rec p' d'
+     bblock_hsmem_rec p' d'
   end.
 
-Lemma hbblock_smem_rec_correct p: forall hd,
-  WHEN hbblock_smem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'.
+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; simpl; wlp_simplify.
 Qed.
-Global Opaque hbblock_smem_rec.
-Local Hint Resolve hbblock_smem_rec_correct: wlp.
+Global Opaque bblock_hsmem_rec.
+Local Hint Resolve bblock_hsmem_rec_correct: wlp.
 
+Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}.
 
-Definition hbblock_smem: bblock -> ?? hsmem
- := fun p => hbblock_smem_rec p {| 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; simpl; intuition try congruence.
+  rewrite !Dict.empty_spec; simpl; auto.
+Qed.
 
-Transparent allvalid.
+Definition bblock_hsmem: bblock -> ?? hsmem
+ := fun p => bblock_hsmem_rec p hsmem_empty.
 
-Lemma hbblock_smem_correct p:
-  WHEN hbblock_smem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd.
+Lemma bblock_hsmem_correct p:
+  WHEN bblock_hsmem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd.
 Proof.
-  unfold bblock_smem; wlp_simplify. eapply H. clear H.
-  unfold smem_model, smem_valid, smem_eval, smem_get; simpl; intuition;
-  rewrite !Dict.empty_spec in * |- *; simpl in * |- *; try congruence.
+  Local Hint Resolve hsmem_empty_correct.
+  wlp_simplify.
 Qed.
-Global Opaque hbblock_smem.
+Global Opaque bblock_hsmem.
 
 End CanonBuilding.
 
@@ -586,13 +619,13 @@ Qed.
 Global Opaque list_term_hash_eq.
 Hint Resolve list_term_hash_eq_correct: wlp.
 
-Lemma smem_eval_intro (d1 d2: hsmem):
-  (forall x, Dict.get d1 x = Dict.get d2 x) -> (forall ge x m, smem_eval ge d1 x m = smem_eval ge d2 x m).
+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 smem_eval, smem_get; intros H ge x m; rewrite H. destruct (Dict.get d2 x); auto.
+  unfold hsmem_post_eval; intros H ge x m; rewrite H. destruct (Dict.get d2 x); auto.
 Qed.
 
-Local Hint Resolve hbblock_smem_correct Dict.eq_test_correct: wlp.
+Local Hint Resolve bblock_hsmem_correct Dict.eq_test_correct: wlp.
 
 Program Definition mk_hash_params (log: term -> ?? unit): Dict.hash_params term :=
  {|
@@ -629,9 +662,9 @@ Variable dbg_failpreserv: term -> ?? unit. (* info of additional failure of the
 Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool :=
   DO failure_in_failpreserv <~ make_cref false;;
   DO r <~ (TRY
-    DO d1 <~ hbblock_smem hco_term.(hC) hco_list.(hC) log_assign no_log_new_term log_inst1 p1;;
+    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 <~ hbblock_smem hco_term.(hC) hco_list.(hC) no_log_assign log_new_term log_inst2 p2;;
+    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 (
@@ -653,12 +686,12 @@ Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool :=
 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.
+  apply bblock_smem_simu; auto. split.
   + intros m; rewrite <- EQPRE1, <- EQPRE2.
     rewrite ! allvalid_extensionality.
     unfold incl in * |- *; intuition eauto.
-  + intros m0 x m1 VALID; rewrite <- EQPOST1, <- EQPOST2; auto.
-    erewrite smem_eval_intro; 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 * |- *.
@@ -677,8 +710,8 @@ End Prog_Eq_Gen.
 
 
 
-Definition hht: hashH term := {| hash_eq := term_hash_eq; get_hid:=term_get_hid; set_hid:=term_set_hid |}. 
-Definition hlht: hashH list_term := {| hash_eq := list_term_hash_eq; get_hid:=list_term_get_hid; set_hid:=list_term_set_hid |}.
+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
@@ -746,8 +779,8 @@ Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv.
 
 Program Definition bblock_simu_test (p1 p2: bblock): ?? bool :=
   DO log <~ count_logger ();;
-  DO hco_term <~ mk_annot (hCons hht);;
-  DO hco_list <~ mk_annot (hCons hlht);;
+  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))
@@ -996,8 +1029,8 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
   DO log1 <~ count_logger ();;
   DO log2 <~ count_logger ();;
   DO cr <~ make_cref None;;
-  DO hco_term <~ mk_annot (hCons hht);;
-  DO hco_list <~ mk_annot (hCons hlht);;
+  DO hco_term <~ mk_annot (hCons hpt);;
+  DO hco_list <~ mk_annot (hCons hplt);;
   DO result1 <~ g_bblock_simu_test
      (log_assign dict_info log1)
      (log_new_term (msg_term cr))
@@ -1017,8 +1050,8 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
     DO log1 <~ count_logger ();;
     DO log2 <~ count_logger ();;
     DO cr <~ make_cref None;;
-    DO hco_term <~ mk_annot (hCons hht);;
-    DO hco_list <~ mk_annot (hCons hlht);;
+    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 !! *)
@@ -1074,9 +1107,60 @@ End ImpSimu.
 
 Require Import FMapPositive.
 
+
+Require Import PArith.
+Require Import FMapPositive.
+
 Module ImpPosDict <: ImpDict with Module R:=Pos.
 
-Include PosDict.
+Module R:=Pos.
+
+Definition t:=PositiveMap.t.
+
+Definition get {A} (d:t A) (x:R.t): option A 
+ := PositiveMap.find x d.
+
+Definition set {A} (d:t A) (x:R.t) (v:A): t A
+ := PositiveMap.add x v d.
+
+Local Hint Unfold PositiveMap.E.eq.
+
+Lemma set_spec_eq A d x (v: A):
+  get (set d x v) x = Some v.
+Proof.
+  unfold get, set; apply PositiveMap.add_1; auto.
+Qed.
+
+Lemma set_spec_diff A d x y (v: A):
+  x <> y -> get (set d x v) y = get d y.
+Proof.
+  unfold get, set; intros; apply PositiveMap.gso; auto.
+Qed.
+
+Definition 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 :=
diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v
index 637e8296..d8002375 100644
--- a/mppa_k1c/abstractbb/Impure/ImpHCons.v
+++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v
@@ -110,17 +110,17 @@ Module HConsing.
 Export HConsingDefs.
 
 (* NB: this axiom is NOT intended to be called directly, but only through [hCons...] functions below. *)
-Axiom xhCons: forall {A}, (hashH A) -> ?? hashConsing A.
+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} (hh: hashH A): ?? (hashConsing A) :=
-  DO hco <~ xhCons hh ;;
+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 hh x.(hdata) x' ;;
+         DO b0 <~ hash_eq hp x.(hdata) x' ;;
          assert_b b0 hCons_eq_msg;;
          RET x');
       next_hid := hco.(next_hid);
@@ -130,10 +130,10 @@ Definition hCons {A} (hh: hashH A): ?? (hashConsing A) :=
       |}.
 
 
-Lemma hCons_correct A (hh: hashH A):
-  WHEN hCons hh ~> hco THEN
-    (forall x y, WHEN hh.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hh x)=(ignore_hid hh y)) ->
-    forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hh x.(hdata)=ignore_hid hh x'.
+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.
@@ -149,7 +149,7 @@ Record hashV {A:Type}:= {
 }.
 Arguments hashV: clear implicits.
 
-Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashH (hashV A) := {|
+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 |}
diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v
index 477be65c..de4c7973 100644
--- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v
+++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v
@@ -130,17 +130,17 @@ Record hashinfo {A: Type} := {
 Arguments hashinfo: clear implicits.
 
 (* for inductive types with intrinsic hash-consing *)
-Record hashH {A:Type}:= {
+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 hashH: clear implicits.
+Arguments hashP: clear implicits.
 
 Axiom unknown_hid: hashcode.
 Extract Constant unknown_hid => "-1".
 
-Definition ignore_hid {A} (hh: hashH A) (hv:A) := set_hid hh hv unknown_hid.
+Definition ignore_hid {A} (hp: hashP A) (hv:A) := set_hid hp hv unknown_hid.
 
 Record hashExport {A:Type}:= {
   get_info: hashcode -> ?? hashinfo A;
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
index 3994cae6..2b66899b 100644
--- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml
@@ -17,13 +17,13 @@ let make_dict (type key) (p: key Dict.hash_params) =
 
 exception Stop;;
 
-let xhCons (type a) (hh:a hashH) =
+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 = hh.hash_eq x.hdata y.hdata
+    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
@@ -42,7 +42,7 @@ let xhCons (type a) (hh:a hashH) =
      match MyHashtbl.find_opt t k with
      | Some d -> d
      | None -> (*print_string "+";*)
-        let d = hh.set_hid k.hdata (MyHashtbl.length t) in
+        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);
@@ -58,7 +58,7 @@ let xhCons (type a) (hh:a hashH) =
           | (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.(hh.get_hid d) <- k) t;
+           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/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
index 9f5eca89..5075d176 100644
--- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli
@@ -2,4 +2,4 @@ open ImpPrelude
 open HConsingDefs
 
 val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t
-val xhCons: 'a hashH -> 'a hashConsing
+val xhCons: 'a hashP -> 'a hashConsing
diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v
index 8b6a372a..649dd083 100644
--- a/mppa_k1c/abstractbb/SeqSimuTheory.v
+++ b/mppa_k1c/abstractbb/SeqSimuTheory.v
@@ -3,104 +3,90 @@
 *)
 
 
+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 Type PseudoRegDictionary.
 
-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 empty: forall {A}, t A.
-
-Parameter empty_spec: forall A x,
-  get (empty (A:=A)) x = None.
-
-End PseudoRegDictionary.
-
-
-Module SimuTheory (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R).
+Module SimuTheory (L: SeqLanguage).
 
 Export L.
 Export LP.
-Export Terms.
+
+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 symbolic memory:
   - pre: pre-condition expressing that the computation has not yet abort on a None.
   - post: the post-condition for each pseudo-register 
 *)
-Record smem:= {pre: genv -> mem -> Prop; post: Dict.t term}.
-
-Coercion post: smem >-> Dict.t.
+Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}.
 
 (** initial symbolic memory *)
-Definition smem_empty := {| pre:=fun _ _ => True; post:=Dict.empty |}.
+Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}.
 
-Definition smem_get (d:Dict.t term) x := 
-   match Dict.get d x with 
-   | None => Input x unknown_hid
-   | Some t => t
-   end.
-
-Fixpoint exp_term (e: exp) (d old: Dict.t term): term :=
+Fixpoint exp_term (e: exp) (d old: smem) : term :=
   match e with
-  | PReg x => smem_get d x
-  | Op o le => App o (list_exp_term le d old) unknown_hid
+  | 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: Dict.t term) : list_term :=
+with list_exp_term (le: list_exp) (d old: smem) : list_term :=
   match le with
-  | Enil => LTnil unknown_hid
-  | Econs e le' => LTcons (exp_term e d old) (list_exp_term le' d old) unknown_hid
+  | 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.
 
-(** evaluation of the post-condition *)
-Definition smem_eval ge (d: Dict.t term) x (m:mem) :=
-  term_eval ge (smem_get d x) m.
 
 (** assignment of the symbolic memory *)
 Definition smem_set (d:smem) x (t:term) := 
-  {| pre:=(fun ge m => (smem_eval ge d x m) <> None /\ (d.(pre) ge m));
-     post:=Dict.set d x t |}.
+  {| 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 |}.
 
 Section SIMU_THEORY.
 
 Variable ge: genv.
 
 Lemma set_spec_eq d x t m:
- smem_eval ge (smem_set d x t) x m = term_eval ge t m.
+ term_eval ge (smem_set d x t x) m = term_eval ge t m.
 Proof.
-  unfold smem_eval, smem_set, smem_get; simpl; rewrite Dict.set_spec_eq; simpl; auto. 
+  unfold smem_set; simpl; case (R.eq_dec x x); try congruence.
 Qed.
 
 Lemma set_spec_diff d x y t m:
-  x <> y -> smem_eval ge (smem_set d x t) y m = smem_eval ge d y m.
+  x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m.
 Proof.
-  intros; unfold smem_eval, smem_set, smem_get; simpl; rewrite Dict.set_spec_diff; simpl; auto. 
+  unfold smem_set; simpl; case (R.eq_dec x y); try congruence.
 Qed.
 
-Lemma smem_eval_empty x m: smem_eval ge smem_empty x m = Some (m x).
-Proof.
-  unfold smem_eval, smem_get; rewrite Dict.empty_spec; simpl; auto.
-Qed.
-
-Hint Rewrite set_spec_eq smem_eval_empty: dict_rw. 
-
 Fixpoint inst_smem (i: inst) (d old: smem): smem :=
   match i with
   | nil => d
@@ -116,8 +102,9 @@ Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem :=
      let d':=inst_smem i d d in
      bblock_smem_rec p' d'
   end.
-
+(*
 Local Hint Resolve smem_eval_empty.
+*)
 
 Definition bblock_smem: bblock -> smem
  := fun p => bblock_smem_rec p smem_empty.
@@ -140,37 +127,36 @@ Qed.
 Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic.
 
 Lemma term_eval_exp e (od:smem) m0 old:
-  (forall x, smem_eval ge od x m0 = Some (old x)) ->
-  forall d m1,
-   (forall x, smem_eval ge (d:smem) x m0 = Some (m1 x)) ->
+  (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.
-  unfold smem_eval in * |- *; intro H.
+  intro H.
   induction e using exp_mut with
-    (P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (smem_get d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old);
+    (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);
   simpl; auto.
   - intros; erewrite IHe; eauto.
   - intros. erewrite IHe, IHe0; eauto. 
 Qed.
 
-Lemma inst_smem_abort i m0 x old: forall d,
+Lemma inst_smem_abort i m0 x old: forall (d:smem),
     pre (inst_smem i d old) ge m0 ->
-    smem_eval ge d x m0 = None ->
-    smem_eval ge (inst_smem i d old) x m0 = None.
+    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]; simpl; auto.
   intros d VALID H; erewrite IHi; eauto. clear IHi.
-  destruct (R.eq_dec x y).
-  * subst; autorewrite with dict_rw.
-    generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID.
-    unfold smem_set; simpl; intuition congruence.
-  * rewrite set_spec_diff; auto.
+  unfold smem_set; simpl; destruct (R.eq_dec y x); auto.
+  subst;
+  generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID.
+  unfold smem_set; simpl. intuition congruence.
 Qed.
 
 Lemma block_smem_rec_abort p m0 x: forall d,
     pre (bblock_smem_rec p d) ge m0 ->
-    smem_eval ge d x m0 = None ->
-    smem_eval ge (bblock_smem_rec p d) x m0 = None.
+    term_eval ge (d x) m0 = None ->
+    term_eval ge (bblock_smem_rec p d x) m0 = None.
 Proof.
   induction p; simpl; auto.
   intros d VALID H; erewrite IHp; eauto. clear IHp.
@@ -178,11 +164,11 @@ Proof.
 Qed.
 
 Lemma inst_smem_Some_correct1 i m0 old (od:smem): 
-  (forall x, smem_eval ge od x m0 = Some (old x)) ->
+  (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, smem_eval ge d x m0 = Some (m1 x)) ->
-   forall x, smem_eval ge (inst_smem i d od) x m0 = Some (m2 x).
+  (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]; simpl; intros m1 m2 d H.
   - inversion_clear H; eauto.
@@ -190,16 +176,14 @@ Proof.
     destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence.
     refine (IHi _ _ _ _ _ _); eauto.
     clear x0; intros x0.
-    unfold assign; destruct (R.eq_dec x x0).
-    * subst; autorewrite with dict_rw.
-      erewrite term_eval_exp; eauto.
-    * rewrite set_spec_diff; auto.
+    unfold assign, smem_set; simpl. 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, smem_eval ge d x m0 = Some (m1 x)) ->
-  forall x, smem_eval ge (bblock_smem_rec p d) x m0 = Some (m2 x).
+  (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.
   induction p as [ | i p]; simpl; intros m1 m2 d H.
@@ -212,39 +196,37 @@ Qed.
 
 Lemma bblock_smem_Some_correct1 p m0 m1:
    run ge p m0 = Some m1
-   -> forall x, smem_eval ge (bblock_smem p) x m0 = Some (m1 x).
+   -> 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, smem_eval ge od x m0 = Some (old x)) ->
+   (forall x, term_eval ge (od x) m0 = Some (old x)) ->
   forall m1 d, pre (inst_smem i d od) ge m0 ->
-   (forall x, smem_eval ge d x m0 = Some (m1 x)) ->
-  inst_run ge i m1 old = None -> exists x, smem_eval ge (inst_smem i d od) x m0 = None.
+   (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]; simpl; intros m1 d.
   - discriminate.
   - intros VALID H0.
     destruct (exp_eval ge e m1 old) eqn: Heqov.
     + refine (IHi _ _ _ _); eauto.
-      intros x0; unfold assign; destruct (R.eq_dec x x0).
-      * subst; autorewrite with dict_rw. 
-        erewrite term_eval_exp; eauto.
-      * rewrite set_spec_diff; auto.
+      intros x0; unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto.
+      subst; erewrite term_eval_exp; eauto.
     + intuition.
       constructor 1 with (x:=x); simpl.
       apply inst_smem_abort; auto.
-      autorewrite with dict_rw.
+      rewrite set_spec_eq. 
       erewrite term_eval_exp; eauto.
 Qed.
 
 Lemma inst_smem_Some_correct2 i m0 old (od: smem):
-  (forall x, smem_eval ge od x m0 = Some (old x)) ->
+  (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, smem_eval ge d x m0 = Some (m1 x)) ->
-  (forall x, smem_eval ge (inst_smem i d od) x m0 = Some (m2 x)) ->
+  (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.
@@ -255,20 +237,18 @@ Proof.
   - intros H.
     destruct (exp_eval ge e m1 old) eqn: Heqov.
     + refine (IHi _ _ _ _ _ _); eauto.
-      intros x0; unfold assign; destruct (R.eq_dec x x0).
-      * subst. autorewrite with dict_rw.
-        erewrite term_eval_exp; eauto.
-      * rewrite set_spec_diff; auto.
+      intros x0; unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto.
+      subst; erewrite term_eval_exp; eauto.
     + generalize (H x).
       rewrite inst_smem_abort; discriminate || auto.
-      autorewrite with dict_rw. 
+      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, smem_eval ge d x m0 = Some (m1 x)) ->
-  (forall x, smem_eval ge (bblock_smem_rec p d) x m0 = Some (m2 x)) ->
+  (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]; simpl; intros m1 m2 d VALID H0.
@@ -278,7 +258,7 @@ Proof.
   - intros H.
      destruct (inst_run ge i m1 m1) eqn: Heqom.
     + refine (IHp _ _ _ _ _ _); eauto.
-    + assert (X: exists x, term_eval ge (smem_get (inst_smem i d d) x) m0 = None).
+    + 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).
@@ -286,21 +266,20 @@ Proof.
       congruence.
 Qed.
 
-
 Lemma bblock_smem_Some_correct2 p m0 m1:
   pre (bblock_smem p) ge m0 ->
-  (forall x, smem_eval ge (bblock_smem p) x m0 = Some (m1 x))
+  (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, smem_eval ge od x m0 = Some (old x)) ->
+  (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, smem_eval ge d x m0 = Some (m1 x)) ->
+  (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]; simpl; auto.
@@ -309,17 +288,15 @@ Proof.
   eapply IHi; eauto.
   + unfold smem_set in * |- *; simpl. 
     rewrite Hm1; intuition congruence.
-  + intros x0. unfold assign; destruct (R.eq_dec x x0).
-    * subst; autorewrite with dict_rw.
-      erewrite term_eval_exp; eauto.
-    * rewrite set_spec_diff; auto.
+  + intros x0. unfold assign, smem_set; simpl; 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, smem_eval ge d x m0 = Some (m1 x)) ->
+  (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.
@@ -337,22 +314,26 @@ Proof.
   unfold smem_empty; simpl. auto.
 Qed.
 
-Definition smem_valid ge d m := pre d ge m /\ forall x, smem_eval ge d x m <> None.
+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:
-  (forall m, smem_valid ge (bblock_smem p1) m -> smem_valid ge (bblock_smem p2) m) ->
-  (forall m0 x m1, smem_valid ge (bblock_smem p1) m0 -> smem_eval ge (bblock_smem p1) x m0 = Some m1 ->
-                   smem_eval ge (bblock_smem p2) x m0 = Some m1) ->
+   smem_simu (bblock_smem p1) (bblock_smem p2) ->
    bblock_simu ge p1 p2.
 Proof.
   Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1.
-  unfold smem_valid; intros INCL EQUIV m DONTFAIL.
+  intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-.
   destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence.
-  assert (X: forall x, smem_eval ge (bblock_smem p1) x m = Some (m1 x)); eauto.
+  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; apply EQUIV; intuition eauto.
+  + intro x; erewrite <- EQUIV; intuition eauto.
     congruence.
 Qed.
 
@@ -370,7 +351,7 @@ 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); autorewrite with dict_rw.
+  generalize (VALID x); rewrite set_spec_eq.
   tauto.
 Qed.
 
@@ -379,50 +360,28 @@ Lemma smem_valid_set_proof d x t m:
 Proof.
   unfold smem_valid; intros (PRE & VALID) PREt. split.
   + split; auto.
-  + intros x0; case (R.eq_dec x x0).
-    - intros; subst; autorewrite with dict_rw. auto.
-    - intros. rewrite set_spec_diff; auto. 
+  + intros x0; unfold smem_set; simpl; case (R.eq_dec x x0); intros; subst; auto.
 Qed.
 
-End SIMU_THEORY.
-
-End SimuTheory.
-
-Require Import PArith.
-Require Import FMapPositive.
-
-Module PosDict <: PseudoRegDictionary with Module R:=Pos.
-
-Module R:=Pos.
-
-Definition t:=PositiveMap.t.
 
-Definition get {A} (d:t A) (x:R.t): option A 
- := PositiveMap.find x d.
-
-Definition set {A} (d:t A) (x:R.t) (v:A): t A
- := PositiveMap.add x v d.
-
-Local Hint Unfold PositiveMap.E.eq.
-
-Lemma set_spec_eq A d x (v: A):
-  get (set d x v) x = Some v.
-Proof.
-  unfold get, set; apply PositiveMap.add_1; auto.
-Qed.
-
-Lemma set_spec_diff A d x y (v: A):
-  x <> y -> get (set d x v) y = get d y.
-Proof.
-  unfold get, set; intros; apply PositiveMap.gso; auto.
-Qed.
+End SIMU_THEORY.
 
-Definition empty {A}: t A := PositiveMap.empty A.
+(** REMARKS: more abstract formulation of the proof... 
+    but relying on functional_extensionality.
+*)
+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 empty_spec A x:
-  get (empty (A:=A)) x = None.
+Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m).
 Proof.
-  unfold get, empty; apply PositiveMap.gempty; auto.
+  unfold smem_correct; simpl; 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 PosDict.
\ No newline at end of file
+End SimuTheory.