[BROKEN] trying to generalize Sylvain's abstract bb to include a genv.

FIXME - DepExampleDemo.v

7 files changed, 133 insertions, 87 deletions

diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 50ce000e..21e7bd98 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -22,10 +22,12 @@ Parameter value: Type.
 
 Parameter op: Type. (* type of operations *)
 
+Parameter genv: Type. (* environment to be used for evaluating an op *)
+
 (* NB: possible generalization
  - relation after/before.
 *)
-Parameter op_eval: op -> list value -> option value.
+Parameter op_eval: genv -> op -> list value -> option value.
 
 End LangParam.
 
@@ -38,6 +40,10 @@ Export P.
 
 Local Open Scope list.
 
+Section SEQLANG.
+
+Variable ge: genv.
+
 Definition mem := R.t -> value.
 
 Definition assign (m: mem) (x:R.t) (v: value): mem 
@@ -58,7 +64,7 @@ Fixpoint exp_eval (e: exp) (m old: mem): option value :=
   | Name x => Some (m x)
   | Op o le => 
      match list_exp_eval le m old with
-     | Some lv => op_eval o lv
+     | Some lv => op_eval ge o lv
      | _ => None
      end
   | Old e => exp_eval e old old
@@ -201,6 +207,8 @@ Proof.
   eauto.
 Qed.
  
+End SEQLANG.
+
 End MkSeqLanguage.
 
 
diff --git a/mppa_k1c/abstractbb/DepExampleDemo.v b/mppa_k1c/abstractbb/DepExampleDemo.v
index c2079b70..74e8f35e 100644
--- a/mppa_k1c/abstractbb/DepExampleDemo.v
+++ b/mppa_k1c/abstractbb/DepExampleDemo.v
@@ -7,6 +7,10 @@ Open Scope Z_scope.
 
 Module EqTests.
 
+Section TESTS.
+
+Variable ge: P.genv.
+
 (**** TESTS DRIVER ! ****)
 
 Record test_input := {
@@ -19,7 +23,7 @@ Record test_input := {
 
 Definition run1 (t: test_input): ?? unit :=
   print ((name t) +; " =>");;
-  DO result <~ bblock_eq_test (verbose t) (p1 t) (p2 t);;
+  DO result <~ bblock_eq_test ge (verbose t) (p1 t) (p2 t);;
   assert_b (eqb result (expected t))  "UNEXPECTED RESULT";;
   if expected t 
   then println " SUCCESS" 
diff --git a/mppa_k1c/abstractbb/DepExampleEqTest.v b/mppa_k1c/abstractbb/DepExampleEqTest.v
index 50bfc2f4..a633ee07 100644
--- a/mppa_k1c/abstractbb/DepExampleEqTest.v
+++ b/mppa_k1c/abstractbb/DepExampleEqTest.v
@@ -12,6 +12,10 @@ Module P<: ImpParam.
 
 Module R := Pos.
 
+Definition genv := unit.
+
+Section IMP.
+
 Inductive value_wrap :=
   | Std (v:value)  (* value = DepExample.value *)
   | Mem (m:mem)
@@ -26,7 +30,7 @@ Inductive op_wrap :=
   | STORE
   .
 
-Definition op_eval (op: op_wrap) (l:list value_wrap): option value_wrap :=
+Definition op_eval (ge: genv) (op: op_wrap) (l:list value_wrap): option value_wrap :=
   match op, l with
   | Imm i, [] => Some (Std i)
   | ARITH op, [Std v1; Std v2] => Some (Std (arith_op_eval op v1 v2))
@@ -47,7 +51,6 @@ Definition op_eval (op: op_wrap) (l:list value_wrap): option value_wrap :=
 Definition value:=value_wrap.
 Definition op:=op_wrap.
 
-
 Definition op_eq (o1 o2: op_wrap): ?? bool :=
   match o1, o2 with
   | Imm i1, Imm i2 => phys_eq i1 i2
@@ -63,6 +66,7 @@ Proof.
   destruct o1, o2; wlp_simplify; congruence.
 Qed.
 
+End IMP.
 End P.
 
 
@@ -77,6 +81,9 @@ End L.
 
 Module IDT := ImpDepTree L ImpPosDict.
 
+Section SECT.
+Variable ge: P.genv.
+
 (** Compilation from DepExample to L *)
 
 Definition the_mem: P.R.t := 1.
@@ -149,13 +156,13 @@ Definition match_option_state (os: option state) (om:option L.mem): Prop :=
   | None => om = None
   end.
 
-Lemma comp_op_correct o s m old: match_state s m -> L.exp_eval (comp_op o) m old = Some (P.Std (operand_eval o (rm s))).
+Lemma comp_op_correct o s m old: match_state s m -> L.exp_eval ge (comp_op o) m old = Some (P.Std (operand_eval o (rm s))).
 Proof.
   destruct 1 as [H1 H2]; destruct o; simpl; auto.
   rewrite H2; auto.
 Qed.
 
-Lemma comp_bblock_correct_aux p: forall s m,  match_state s m -> match_option_state (sem_bblock p s) (L.run (comp_bblock p) m).
+Lemma comp_bblock_correct_aux p: forall s m,  match_state s m -> match_option_state (sem_bblock p s) (L.run ge (comp_bblock p) m).
 Proof.
   induction p as [| i p IHp]; simpl; eauto.
   intros s m H; destruct i; simpl; erewrite !comp_op_correct; eauto; simpl.
@@ -205,7 +212,7 @@ Proof.
     * rewrite L.assign_diff; auto.
 Qed.
 
-Lemma comp_bblock_correct p s: match_option_state (sem_bblock p s) (L.run (comp_bblock p) (trans_state s)).
+Lemma comp_bblock_correct p s: match_option_state (sem_bblock p s) (L.run ge (comp_bblock p) (trans_state s)).
 Proof.
   eapply comp_bblock_correct_aux. apply match_trans_state.
 Qed.
@@ -257,7 +264,7 @@ Proof.
   - intros; subst; simpl; auto.
 Qed.
 
-Lemma bblock_equiv_reduce p1 p2: L.bblock_equiv (comp_bblock p1) (comp_bblock p2) -> bblock_equiv p1 p2.
+Lemma bblock_equiv_reduce p1 p2: L.bblock_equiv ge (comp_bblock p1) (comp_bblock p2) -> bblock_equiv p1 p2.
 Proof.
   unfold L.bblock_equiv, bblock_equiv.
   intros; eapply res_equiv_from_match.
@@ -295,9 +302,9 @@ Definition string_of_op (op: P.op): ?? pstring :=
 
 Definition bblock_eq_test (verb: bool) (p1 p2: bblock) : ?? bool :=
   if verb then
-    IDT.verb_bblock_eq_test string_of_name string_of_op (comp_bblock p1) (comp_bblock p2)
+    IDT.verb_bblock_eq_test string_of_name string_of_op ge (comp_bblock p1) (comp_bblock p2)
   else
-    IDT.bblock_eq_test (comp_bblock p1) (comp_bblock p2).
+    IDT.bblock_eq_test ge (comp_bblock p1) (comp_bblock p2).
 
 Local Hint Resolve IDT.bblock_eq_test_correct bblock_equiv_reduce IDT.verb_bblock_eq_test_correct: wlp.
 
@@ -310,6 +317,7 @@ Qed.
 Global Opaque bblock_eq_test.
 Hint Resolve bblock_eq_test_correct: wlp.
 
+End SECT.
 (* TEST: we can coerce this bblock_eq_test into a pure function (even if this is a little unsafe). *)
 (*
 Import UnsafeImpure.
diff --git a/mppa_k1c/abstractbb/DepExampleParallelTest.v b/mppa_k1c/abstractbb/DepExampleParallelTest.v
index 00f33540..35b44683 100644
--- a/mppa_k1c/abstractbb/DepExampleParallelTest.v
+++ b/mppa_k1c/abstractbb/DepExampleParallelTest.v
@@ -8,13 +8,16 @@ Definition bblock_is_para (p: bblock) : bool :=
 
 Local Hint Resolve the_mem_separation reg_map_separation.
 
+Section SEC.
+Variable ge: P.genv.
+
 (* Actually, almost the same proof script than [comp_bblock_correct_aux] !
    We could definitely factorize the proof through a lemma on compilation to macros.
 *)
 Lemma comp_bblock_correct_para_iw p: forall sin sout min mout,
   match_state sin min -> 
   match_state sout mout ->
-  match_option_state (sem_bblock_par_iw p sin sout) (PChk.prun_iw (comp_bblock p) mout min).
+  match_option_state (sem_bblock_par_iw p sin sout) (PChk.prun_iw ge (comp_bblock p) mout min).
 Proof.
   induction p as [|i p IHp]; simpl; eauto.
   intros sin sout min mout Hin Hout; destruct i; simpl; erewrite !comp_op_correct; eauto; simpl.
@@ -141,7 +144,7 @@ Qed.
 Local Hint Resolve comp_bblock_Permutation res_eq_from_match match_from_res_equiv comp_bblock_correct_para_iw.
 
 Lemma bblock_par_iff_prun p s os': 
- sem_bblock_par p s os' <-> PChk.prun (comp_bblock p) (trans_state s) (trans_option_state os').
+ sem_bblock_par p s os' <-> PChk.prun ge (comp_bblock p) (trans_state s) (trans_option_state os').
 Proof.
   unfold sem_bblock_par, PChk.prun. constructor 1.
   - intros (p' & H1 & H2).
@@ -154,8 +157,10 @@ Qed.
 Theorem bblock_is_para_correct p:
   bblock_is_para p = true -> forall s os', (sem_bblock_par p s os' <-> res_equiv os' (sem_bblock p s)).
 Proof.
-  intros H; generalize (PChk.is_parallelizable_correct _ H); clear H.
+  intros H; generalize (PChk.is_parallelizable_correct ge _ H); clear H.
   intros H s os'.
   rewrite bblock_par_iff_prun, H.
   constructor; eauto.
-Qed.
\ No newline at end of file
+Qed.
+
+End SEC.
\ No newline at end of file
diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v
index 3dff22e1..6f017378 100644
--- a/mppa_k1c/abstractbb/DepTreeTheory.v
+++ b/mppa_k1c/abstractbb/DepTreeTheory.v
@@ -41,6 +41,9 @@ Export L.
 Export LP.
 Local Open Scope list.
 
+Section DEPTREE.
+
+Variable ge: genv.
 
 (** Dependency Trees of these "bblocks" 
 
@@ -63,7 +66,7 @@ Fixpoint tree_eval (t: tree) (m: mem): option value :=
   | Tname x => Some (m x)
   | Top o l =>
      match list_tree_eval l m with
-     | Some v => op_eval o v
+     | Some v => op_eval ge o v
      | _ => None
      end
   | Terase new old =>
@@ -127,7 +130,7 @@ Definition failsafe (t: tree): bool :=
   match t with
   | Tname x => true
   | Top o Tnil => 
-     match op_eval o nil with
+     match op_eval ge o nil with
      | Some _ => true
      | None => false
      end
@@ -138,7 +141,7 @@ Lemma failsafe_correct (t: tree) m: failsafe t = true -> tree_eval t m <> None.
 Proof.
   destruct t; simpl; try congruence.
   destruct l; simpl; try congruence.
-  destruct (op_eval o nil); try congruence.
+  destruct (op_eval ge o nil); try congruence.
 Qed.
 
 Fixpoint macro_deps (i: macro) (d old: deps): deps :=
@@ -168,10 +171,10 @@ Definition bblock_deps: bblock -> deps
 Lemma tree_eval_exp e od m0 old:
   (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
   forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-   (tree_eval (exp_tree e d od) m0) = exp_eval e m1 old.
+   (tree_eval (exp_tree e d od) m0) = exp_eval ge e m1 old.
 Proof.
   intro H.
-  induction e using exp_mut with (P0:=fun l => forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval (list_exp_tree l d od) m0 = list_exp_eval l m1 old); simpl; auto.
+  induction e using exp_mut with (P0:=fun l => forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval (list_exp_tree l d od) m0 = list_exp_eval ge l m1 old); simpl; auto.
   - intros; erewrite IHe; eauto.
   - intros; erewrite IHe, IHe0; eauto. 
 Qed.
@@ -202,14 +205,14 @@ Qed.
 Lemma tree_eval_macro_Some_correct1 i m0 old od: 
   (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
   forall (m1 m2: mem) d, 
-  macro_run i m1 old = Some m2 -> 
+  macro_run ge i m1 old = Some m2 -> 
   (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
   (forall x, tree_eval (deps_get (macro_deps 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.
   - intros H0 x0.
-    remember (exp_eval e m1 old) as ov.
+    remember (exp_eval ge e m1 old) as ov.
     destruct ov.
     + refine (IHi _ _ _ _ _ _); eauto.
       clear x0; intros x0.
@@ -224,21 +227,21 @@ Qed.
 Local Hint Resolve tree_eval_macro_Some_correct1 tree_eval_abort.
 
 Lemma tree_eval_Some_correct1 p m0: forall (m1 m2: mem) d, 
- run p m1 = Some m2 -> 
+ run ge p m1 = Some m2 -> 
   (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
     (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)).
 Proof.
   induction p as [ | i p]; simpl; intros m1 m2 d H.
   - inversion_clear H; eauto.
   - intros H0 x0.
-    remember (macro_run i m1 m1) as om.
+    remember (macro_run ge i m1 m1) as om.
     destruct om.
     + refine (IHp _ _ _ _ _ _); eauto.
     + inversion H. 
 Qed.
 
 Lemma bblock_deps_Some_correct1 p m0 m1:
-  run p m0 = Some m1
+  run ge p m0 = Some m1
    -> forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x).
 Proof.
   intros; eapply tree_eval_Some_correct1;
@@ -248,12 +251,12 @@ Qed.
 Lemma tree_eval_macro_None_correct i m0 old od: 
   (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
   forall m1 d,  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-  macro_run i m1 old = None <-> exists x, tree_eval (deps_get (macro_deps i d od) x) m0 = None.
+  macro_run ge i m1 old = None <-> exists x, tree_eval (deps_get (macro_deps i d od) x) m0 = None.
 Proof.
   intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d.
   - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate].
   - intros H0.
-    remember (exp_eval e m1 old) as ov.
+    remember (exp_eval ge e m1 old) as ov.
     destruct ov.
     + refine (IHi _ _ _); eauto.
       intros x0; unfold assign; destruct (R.eq_dec x x0).
@@ -272,23 +275,23 @@ Qed.
 
 Lemma tree_eval_None_correct p m0: forall m1 d,
   (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-  run p m1 = None <-> exists x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None.
+  run ge p m1 = None <-> exists x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None.
 Proof.
   induction p as [|i p IHp]; simpl; intros m1 d.
   - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate].
   - intros H0.
-    remember (macro_run i m1 m1) as om.
+    remember (macro_run ge i m1 m1) as om.
     destruct om.
     + refine (IHp _ _ _); eauto.
     + intuition.
-      assert (X: macro_run i m1 m1 = None); auto.
+      assert (X: macro_run ge i m1 m1 = None); auto.
       rewrite tree_eval_macro_None_correct in X; auto.
       destruct X as [x H1].
       constructor 1 with (x:=x); simpl; auto.
 Qed.
 
 Lemma bblock_deps_None_correct p m:
-  run p m = None <-> exists x, tree_eval (deps_get (bblock_deps p) x) m = None.
+  run ge p m = None <-> exists x, tree_eval (deps_get (bblock_deps p) x) m = None.
 Proof.
   intros; eapply tree_eval_None_correct.
   intros; autorewrite with dict_rw; simpl; eauto.
@@ -299,7 +302,7 @@ Lemma tree_eval_macro_Some_correct2 i m0 old od:
   forall (m1 m2: mem) d, 
   (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
     (forall x, tree_eval (deps_get (macro_deps i d od) x) m0 = Some (m2 x)) ->
-    res_eq (Some m2) (macro_run i m1 old).
+    res_eq (Some m2) (macro_run ge i m1 old).
 Proof.
   intro X.
   induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H0.
@@ -307,7 +310,7 @@ Proof.
     generalize (H0 x); rewrite H.
     congruence.
   - intros H.
-    remember (exp_eval e m1 old) as ov.
+    remember (exp_eval ge e m1 old) as ov.
     destruct ov.
     + refine (IHi _ _ _ _ _); eauto.
       intros x0; unfold assign; destruct (R.eq_dec x x0).
@@ -325,17 +328,17 @@ Qed.
 Lemma tree_eval_Some_correct2 p m0: forall (m1 m2: mem) d, 
   (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
     (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)) ->
-    res_eq (Some m2) (run p m1).
+    res_eq (Some m2) (run ge p m1).
 Proof.
   induction p as [|i p]; simpl; intros m1 m2 d H0.
   - intros H; eapply ex_intro; intuition eauto.
     generalize (H0 x); rewrite H.
     congruence.
   - intros H.
-    remember (macro_run i m1 m1) as om.
+    remember (macro_run ge i m1 m1) as om.
     destruct om.
     + refine (IHp _ _ _ _ _); eauto.
-    + assert (X: macro_run i m1 m1 = None); auto.
+    + assert (X: macro_run ge i m1 m1 = None); auto.
       rewrite tree_eval_macro_None_correct in X; auto.
       destruct X as [x H1].
       generalize (H x).
@@ -344,7 +347,7 @@ Qed.
 
 Lemma bblock_deps_Some_correct2 p m0 m1:
   (forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x))
-  -> res_eq (Some m1) (run p m0).
+  -> res_eq (Some m1) (run ge p m0).
 Proof.
   intros; eapply tree_eval_Some_correct2; eauto.
   intros; autorewrite with dict_rw; simpl; eauto.
@@ -353,22 +356,24 @@ Qed.
 
 Theorem bblock_deps_equiv p1 p2:
   (forall x, deps_get (bblock_deps p1) x = deps_get (bblock_deps p2) x)
-   -> bblock_equiv p1 p2.
+   -> bblock_equiv ge p1 p2.
 Proof.
   intros H m2.
-  remember (run p1 m2) as om1.
+  remember (run ge p1 m2) as om1.
   destruct om1; simpl.
   + apply bblock_deps_Some_correct2.
     intros; rewrite <- H.
     apply bblock_deps_Some_correct1; auto.
   + rewrite bblock_deps_None_correct.
-    assert (X: run p1 m2 = None); auto.
+    assert (X: run ge p1 m2 = None); auto.
     rewrite bblock_deps_None_correct in X.
     destruct X as [x Hx].
     rewrite H in Hx.
     eauto.
 Qed.
 
+End DEPTREE.
+
 End DepTree.
 
 Require Import PArith.
diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v
index 65f12b8e..994c8e34 100644
--- a/mppa_k1c/abstractbb/ImpDep.v
+++ b/mppa_k1c/abstractbb/ImpDep.v
@@ -72,6 +72,8 @@ Hypothesis hC_tree_correct: forall t, WHEN hC_tree t ~> t' THEN pre_data t=data
 Variable hC_list_tree: pre_hashV list_tree -> ?? hashV list_tree.
 Hypothesis hC_list_tree_correct: forall t, WHEN hC_list_tree t ~> t' THEN pre_data t=data t'.
 
+Variable ge: genv.
+
 (* First, we wrap constructors for hashed values !*)
 
 Local Open Scope positive.
@@ -213,7 +215,7 @@ Fixpoint hmacro_deps (i: macro) (d od: hdeps): ?? hdeps :=
   | (x, e)::i' =>
      DO dbg <~ debug_assign x;;
      DO t0 <~ hdeps_get d x None;;
-     DO v' <~ (if failsafe (data t0) 
+     DO v' <~ (if failsafe ge (data t0) 
       then 
         hexp_tree e d od dbg 
       else
@@ -246,20 +248,20 @@ Lemma hmacro_deps_correct i: forall d1 od1,
   WHEN hmacro_deps i d1 od1 ~> d1' THEN
     forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) ->
     (forall x, pdeps_get d1 x = deps_get d2 x) -> 
-    forall x, pdeps_get d1' x = deps_get (macro_deps i d2 od2) x.
+    forall x, pdeps_get d1' x = deps_get (macro_deps ge i d2 od2) x.
 Proof.
   induction i; simpl; wlp_simplify.
-  + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). 
+  + cutrewrite (failsafe ge (deps_get d2 a0) = failsafe ge (data exta0)). 
     - erewrite H0, H2; simpl; eauto. clear exta2 Hexta2 H2; auto.
       intros x0; destruct (R.eq_dec a0 x0).
-      * subst; autorewrite with dict_rw. erewrite H1; eauto.
+      * subst. autorewrite with dict_rw. rewrite set_spec_eq. erewrite H1; eauto.
       * rewrite set_spec_diff, pset_spec_diff; auto.
     - rewrite H, H4; auto.
-  + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)).
+  + cutrewrite (failsafe ge (deps_get d2 a0) = failsafe ge (data exta0)).
     - erewrite H0, H3; simpl; eauto. clear exta3 Hexta3 H3; auto.
       intros x0; destruct (R.eq_dec a0 x0).
       * subst; autorewrite with dict_rw. rewrite H2.
-        erewrite H, H1; eauto. congruence.
+        erewrite H, H1; eauto. rewrite set_spec_eq. congruence.
       * rewrite set_spec_diff, pset_spec_diff; auto.
    - rewrite H, H5; auto.
 Qed.
@@ -280,7 +282,7 @@ Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps :=
 
 Lemma hbblock_deps_rec_correct p: forall d1,
   WHEN hbblock_deps_rec p d1 ~> d1' THEN
-    forall d2, (forall x, pdeps_get d1 x = deps_get d2 x) -> forall x, pdeps_get d1' x = deps_get (bblock_deps_rec p d2) x.
+    forall d2, (forall x, pdeps_get d1 x = deps_get d2 x) -> forall x, pdeps_get d1' x = deps_get (bblock_deps_rec ge p d2) x.
 Proof.
   induction p; simpl; wlp_simplify.
 Qed.
@@ -292,10 +294,10 @@ Definition hbblock_deps: bblock -> ?? hdeps
  := fun p => hbblock_deps_rec p Dict.empty.
 
 Lemma hbblock_deps_correct p:
-  WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps p) x.
+  WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps ge p) x.
 Proof.
   unfold bblock_deps; wlp_simplify. erewrite H; eauto.
-  intros; autorewrite with dict_rw; auto.
+  intros; autorewrite with dict_rw; auto. rewrite empty_spec. reflexivity.
 Qed.
 Global Opaque hbblock_deps.
 
@@ -373,7 +375,7 @@ Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 macros *)
 Variable dbg2: R.t -> ?? option pstring. (* log of p2 macros *)
 Variable log1: unit -> ?? unit. (* log of p1 macros *)
 Variable log2: unit -> ?? unit. (* log of p2 macros *)
-
+Variable ge: genv.
 
 
 Variable hco_tree: hashConsing tree.
@@ -386,8 +388,8 @@ Variable print_error: pstring -> ?? unit.
 
 Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool :=
   DO r <~ (TRY 
-    DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;;
-    DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;;
+    DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) ge dbg1 log1 p1 ;;
+    DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) ge dbg2 log2 p2 ;;
     DO b <~ Dict.eq_test d1 d2 ;;
     if b then RET true
     else (
@@ -397,7 +399,7 @@ Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool :=
   CATCH_FAIL s, _ => 
     print_error s;;
     RET false
-  ENSURE (fun b => b=true -> bblock_equiv p1 p2));;
+  ENSURE (fun b => b=true -> bblock_equiv ge p1 p2));;
   RET (`r).
 Obligation 1.
   destruct hco_tree_correct as [X1 X2], hco_list_correct as [Y1 Y2].
@@ -408,7 +410,7 @@ Obligation 1.
 Qed.
 
 Theorem g_bblock_eq_test_correct p1 p2:
-  WHEN g_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2.
+  WHEN g_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2.
 Proof.
   wlp_simplify.
   destruct exta; simpl in * |- *; auto.
@@ -437,11 +439,11 @@ Definition print_error (log: logger unit) (s:pstring): ?? unit
     println (msg_prefix +; msg_number +; n +; " -- " +; s). 
 
 
-Program Definition bblock_eq_test (p1 p2: bblock): ?? bool :=
+Program Definition bblock_eq_test (ge: genv) (p1 p2: bblock): ?? bool :=
   DO log <~ count_logger ();;
   DO hco_tree <~ mk_annot (hCons tree_hash_eq (fun _ => RET msg_unknow_tree));;
   DO hco_list <~ mk_annot (hCons list_tree_hash_eq (fun _ => RET msg_unknow_list_tree));;
-  g_bblock_eq_test no_dbg no_dbg skip (log_insert log) hco_tree _ hco_list _ print_error_end (print_error log) p1 p2.
+  g_bblock_eq_test no_dbg no_dbg skip (log_insert log) ge hco_tree _ hco_list _ print_error_end (print_error log) p1 p2.
 Obligation 1.  
   generalize (hCons_correct _ _ _ _ H0); clear H0.
   constructor 1; wlp_simplify.
@@ -453,8 +455,8 @@ Qed.
 
 Local Hint Resolve g_bblock_eq_test_correct.
 
-Theorem bblock_eq_test_correct p1 p2:
-  WHEN bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2.
+Theorem bblock_eq_test_correct ge p1 p2:
+  WHEN bblock_eq_test ge p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2.
 Proof.
   wlp_simplify.
 Qed.
@@ -688,7 +690,7 @@ Definition hlog (log: logger unit) (hct: hashConsing tree) (hcl: hashConsing lis
       next_log hcl s
     ).
 
-Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool :=
+Program Definition verb_bblock_eq_test (ge: genv) (p1 p2: bblock): ?? bool :=
   DO log1 <~ count_logger ();;
   DO log2 <~ count_logger ();;
   DO cr <~ make_cref Nothing;;
@@ -699,6 +701,7 @@ Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool :=
      simple_debug
      (hlog log1 hco_tree hco_list)
      (log_insert log2) 
+     ge
      hco_tree _ 
      hco_list _ 
      (print_error_end1 hco_tree hco_list)
@@ -717,6 +720,7 @@ Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool :=
        simple_debug
        (hlog log1 hco_tree hco_list)
        (log_insert log2) 
+       ge
        hco_tree _ 
        hco_list _ 
        (print_error_end2 hco_tree hco_list)
@@ -745,8 +749,8 @@ Obligation 4.
   constructor 1; wlp_simplify.
 Qed.
 
-Theorem verb_bblock_eq_test_correct p1 p2:
-  WHEN verb_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2.
+Theorem verb_bblock_eq_test_correct ge p1 p2:
+  WHEN verb_bblock_eq_test ge p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2.
 Proof.
   wlp_simplify.
 Qed.
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v
index 6bfd8770..b6d1f142 100644
--- a/mppa_k1c/abstractbb/Parallelizability.v
+++ b/mppa_k1c/abstractbb/Parallelizability.v
@@ -18,12 +18,15 @@ Module ParallelSemantics (L: SeqLanguage).
 Export L.
 Local Open Scope list.
 
+Section PARALLEL.
+Variable ge: genv.
+
 (* parallel run of a macro *)
 Fixpoint macro_prun (i: macro) (m tmp old: mem): option mem :=
   match i with
   | nil => Some m
   | (x, e)::i' =>
-     match exp_eval e tmp old with
+     match exp_eval ge e tmp old with
      | Some v' => macro_prun i' (assign m x v') (assign tmp x v') old
      | None => None
      end
@@ -31,10 +34,10 @@ Fixpoint macro_prun (i: macro) (m tmp old: mem): option mem :=
 
 (* [macro_prun] is generalization of [macro_run] *)   
 Lemma macro_run_prun i: forall m old,
-  macro_run i m old = macro_prun i m m old.
+  macro_run ge i m old = macro_prun i m m old.
 Proof.
   induction i as [|[y e] i']; simpl; auto.
-  intros m old; destruct (exp_eval e m old); simpl; auto.
+  intros m old; destruct (exp_eval ge e m old); simpl; auto.
 Qed.
 
 
@@ -60,7 +63,7 @@ Lemma macro_prun_equiv i old: forall m1 m2 tmp,
   res_eq (macro_prun i m1 tmp old) (macro_prun i m2 tmp old).
 Proof.
   induction i as [|[x e] i']; simpl; eauto.
-  intros m1 m2 tmp H; destruct (exp_eval e tmp old); simpl; auto.
+  intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); simpl; auto.
   eapply IHi'; unfold assign. intros; destruct (R.eq_dec x x0); auto.
 Qed.
 
@@ -76,6 +79,7 @@ Proof.
     + intros H1; rewrite H1; simpl; auto.
 Qed.
 
+End PARALLEL.
 End ParallelSemantics.
 
 
@@ -168,6 +172,8 @@ Module ParallelizablityChecking (L: SeqLanguage).
 
 Include ParallelSemantics L.
 
+Section PARALLELI.
+Variable ge: genv.
 
 (** * Preliminary notions on frames *)
 
@@ -249,22 +255,22 @@ Fixpoint macro_wframe(i:macro): list R.t :=
   end.
 
 Lemma macro_wframe_correct i m' old: forall m tmp, 
-  macro_prun i m tmp old = Some m' -> 
+  macro_prun ge i m tmp old = Some m' -> 
   forall x, notIn x (macro_wframe i) -> m' x  = m x.
 Proof.
   induction i as [|[y e] i']; simpl.
   - intros m tmp H x H0; inversion_clear H; auto.
-  - intros m tmp H x (H1 & H2); destruct (exp_eval e tmp old); simpl; try congruence.
+  - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); simpl; try congruence.
     cutrewrite (m x = assign m y v x); eauto.
     rewrite assign_diff; auto.
 Qed.
 
 Lemma macro_prun_fequiv i old: forall m1 m2 tmp, 
-  frame_eq (fun x => In x (macro_wframe i)) (macro_prun i m1 tmp old) (macro_prun i m2 tmp old).
+  frame_eq (fun x => In x (macro_wframe i)) (macro_prun ge i m1 tmp old) (macro_prun ge i m2 tmp old).
 Proof.
   induction i as [|[y e] i']; simpl.
   - intros m1 m2 tmp; eexists; intuition eauto.
-  - intros m1 m2 tmp. destruct (exp_eval e tmp old); simpl; auto.
+  - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); simpl; auto.
     eapply frame_eq_list_split; eauto. clear IHi'.
     intros m1' m2' x H1 H2.
     lapply (macro_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto.
@@ -275,16 +281,16 @@ Proof.
 Qed.
 
 Lemma macro_prun_None i m1 m2 tmp old: 
-  macro_prun i m1 tmp old = None -> 
-  macro_prun i m2 tmp old = None.
+  macro_prun ge i m1 tmp old = None -> 
+  macro_prun ge i m2 tmp old = None.
 Proof.
   intros H; generalize (macro_prun_fequiv i old m1 m2 tmp).
   rewrite H; simpl; auto.
 Qed.
 
 Lemma macro_prun_Some i m1 m2 tmp old m1': 
-  macro_prun i m1 tmp old = Some m1' -> 
-  res_eq (Some (frame_assign m2 (macro_wframe i) m1')) (macro_prun i m2 tmp old).
+  macro_prun ge i m1 tmp old = Some m1' -> 
+  res_eq (Some (frame_assign m2 (macro_wframe i) m1')) (macro_prun ge i m2 tmp old).
 Proof.
   intros H; generalize (macro_prun_fequiv i old m1 m2 tmp).
   rewrite H; simpl.
@@ -385,17 +391,17 @@ Qed.
 Theorem is_det_correct p p':
   Permutation p p' -> 
   is_det p -> 
-  forall m old, res_eq (prun_iw p m old) (prun_iw p' m old).
+  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 ]; simpl; eauto.
   - intros [H0 H1] m old.
-    remember (macro_prun i m old old) as om0.
+    remember (macro_prun ge i m old old) as om0.
     destruct om0 as [ m0 | ]; simpl; auto.
   - rewrite disjoint_app_r.
     intros ([Z1 Z2] & Z3 & Z4) m old.
-    remember (macro_prun i2 m old old) as om2.
+    remember (macro_prun ge i2 m old old) as om2.
     destruct om2 as [ m2 | ]; simpl; auto.
-    + remember (macro_prun i1 m old old) as om1.
+    + remember (macro_prun ge i1 m old old) as om1.
       destruct om1 as [ m1 | ]; simpl; auto.
       * lapply (macro_prun_Some i2 m m1 old old m2); simpl; auto.
         lapply (macro_prun_Some i1 m m2 old old m1); simpl; auto.
@@ -412,7 +418,7 @@ Proof.
         }
         rewrite frame_assign_notIn; auto.
      * erewrite macro_prun_None; eauto. simpl; auto.
-   + remember (macro_prun i1 m old old) as om1.
+   + remember (macro_prun ge i1 m old old) as om1.
      destruct om1 as [ m1 | ]; simpl; auto.
      erewrite macro_prun_None; eauto.
   - intros; eapply res_eq_trans.
@@ -439,10 +445,10 @@ with list_exp_frame (le: list_exp): list R.t :=
 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 e m1 old1)=(exp_eval e m2 old2).
+   (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 l m1 old1)=(list_exp_eval l m2 old2)); simpl; auto.
+   (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); simpl; 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; 
@@ -465,13 +471,13 @@ Lemma macro_frame_correct i wframe old1 old2: forall m tmp1 tmp2,
   (disjoint (macro_frame i) wframe) ->
   (forall x, notIn x wframe -> old1 x = old2 x) ->
   (forall x, notIn x wframe -> tmp1 x = tmp2 x) ->
-  macro_prun i m tmp1 old1 = macro_prun i m tmp2 old2.
+  macro_prun ge i m tmp1 old1 = macro_prun ge i m tmp2 old2.
 Proof.
   induction i as [|[x e] i']; simpl; auto.
   intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l.
   intros (H1 & H2 & H3) H6 H7.
-  cutrewrite (exp_eval e tmp1 old1 = exp_eval e tmp2 old2).
-  - destruct (exp_eval e tmp2 old2); auto.
+  cutrewrite (exp_eval ge e tmp1 old1 = exp_eval ge e tmp2 old2).
+  - destruct (exp_eval ge e tmp2 old2); auto.
     eapply IHi'; eauto. 
     simpl; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); simpl; auto. 
   - unfold disjoint in H2; apply exp_frame_correct.
@@ -512,12 +518,12 @@ Qed.
 Lemma pararec_correct p old: forall wframe m,
   pararec p wframe -> 
   (forall x, notIn x wframe -> m x = old x) ->
-  run p m = prun_iw p m old.
+  run ge p m = prun_iw ge p m old.
 Proof.
   elim p; clear p; simpl; auto.
   intros i p' X wframe m [H H0] H1.
   erewrite macro_run_prun, macro_frame_correct; eauto.
-  remember (macro_prun i m old old) as om0.
+  remember (macro_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].
@@ -528,7 +534,7 @@ Qed.
 Definition parallelizable (p: bblock) := pararec p nil.
 
 Theorem parallelizable_correct p m om':
-  parallelizable p -> (prun p m om' <-> res_eq om' (run p m)).
+  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.
@@ -541,6 +547,8 @@ Proof.
     erewrite pararec_correct in H0; eauto.
 Qed.
 
+End PARALLELI.
+
 End ParallelizablityChecking.
 
 
@@ -585,6 +593,9 @@ Module ParallelChecks (L: SeqLanguage) (S:ResourceSet 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.
 
 (** Now, refinement of each operation toward parallelizable *)
@@ -656,12 +667,13 @@ Proof.
 Qed.
 
 Theorem is_parallelizable_correct p:
-  is_parallelizable p = true -> forall m om', (prun p m om' <-> res_eq om' (run p m)).
+  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.