Finish implem proof, need to adapt scheduler proof

3 files changed, 371 insertions, 113 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index b04c17fb..34f8eb1f 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -77,6 +77,30 @@ Definition smem_set_hid (sm: smem) (hid: hashcode): smem :=
   | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid
   end.
 
+Lemma sval_set_hid_correct ctx x y:
+  sval_set_hid x unknown_hid = sval_set_hid y unknown_hid ->
+  sval_refines ctx x y.
+Proof.
+  destruct x, y; intro H; inversion H; subst; simpl; auto.
+Qed.
+Local Hint Resolve sval_set_hid_correct: core.
+
+Lemma list_sval_set_hid_correct ctx x y:
+  list_sval_set_hid x unknown_hid = list_sval_set_hid y unknown_hid ->
+  list_sval_refines ctx x y.
+Proof.
+  destruct x, y; intro H; inversion H; subst; simpl; auto.
+Qed.
+Local Hint Resolve list_sval_set_hid_correct: core.
+
+Lemma smem_set_hid_correct ctx x y:
+  smem_set_hid x unknown_hid = smem_set_hid y unknown_hid ->
+  smem_refines ctx x y.
+Proof.
+  destruct x, y; intro H; inversion H; subst; simpl; auto.
+Qed.
+Local Hint Resolve smem_set_hid_correct: core.
+
 (** Now, we build the hash-Cons value from a "hash_eq".
 
   Informal specification: 
@@ -474,7 +498,6 @@ Proof.
   - intros X; inversion REF.
     erewrite H1; eauto.
 Qed.
-Global Opaque hrexec_store.
 Local Hint Resolve hrexec_store_correct: wlp.
 
 (** ** Assignment of registers *)
@@ -788,7 +811,34 @@ Proof.
       rewrite ris_sreg_set_access.
       erewrite red_PTree_set_refines; intuition eauto.
 Qed.
-Global Opaque hrs_sreg_set.
+
+Lemma hrs_ok_op_okpreserv ctx op args dest hrs:
+  WHEN hrs_sreg_set dest args (Rop op) hrs ~> rst THEN
+  ris_ok ctx rst -> ris_ok ctx hrs.
+Proof.
+  wlp_simplify; inv H2 || inv H1;
+  simpl in *; econstructor; eauto.
+Qed.
+
+Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs:
+  WHEN hrs_sreg_set dest args (Rload TRAP chunk addr) hrs ~> rst THEN
+  ris_ok ctx rst -> ris_ok ctx hrs.
+Proof.
+  wlp_simplify; inv H1;
+  simpl in *; econstructor; eauto.
+Qed.
+
+Lemma hrs_ok_store_okpreserv ctx chunk addr args src hrs:
+  WHEN hrexec_store chunk addr args src hrs ~> rst THEN
+  ris_ok ctx rst -> ris_ok ctx hrs.
+Proof.
+  unfold hrexec_store; wlp_simplify.
+  generalize H2. erewrite ok_rset_mem; intuition.
+  specialize H1 with (sm2 := hrs).
+  erewrite H1; eauto. rewrite H3. repeat autodestruct.
+Qed.
+
+Global Opaque hrs_sreg_set hrexec_store.
 Local Hint Resolve hrs_sreg_set_correct: wlp.
 
 (* transfer *)
@@ -800,6 +850,7 @@ Proof.
    split; destruct 1; econstructor; simpl in *; eauto.
 Qed.
 
+(* TODO useless?
 Lemma hrset_red_reg_correct ctx r rsv sv hrs sis:
   ris_refines ctx hrs sis ->
   (ris_ok ctx hrs -> eval_sval ctx rsv <> None) ->
@@ -814,50 +865,62 @@ Proof.
     erewrite red_PTree_set_refines; eauto.
     econstructor; eauto.
 Qed.
+ *)
 
-Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ristate :=
+Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ?? ristate :=
   match inputs with
-  | nil =>   {| ris_smem := hrs.(ris_smem);
-                ris_input_init := false;
-                ok_rsval := hrs.(ok_rsval);
-                ris_sreg:= PTree.empty _
-             |}
+  | nil => RET {| ris_smem := hrs.(ris_smem);
+                  ris_input_init := false;
+                  ok_rsval := hrs.(ok_rsval);
+                  ris_sreg:= PTree.empty _
+               |}
   | r::l =>
-      let hrs' := transfer_hrs l hrs in
-      ris_sreg_set hrs' (red_PTree_set r (ris_sreg_get hrs r) hrs')
+      DO hrs' <~ transfer_hrs l hrs;;
+      DO sv <~ hrs_sreg_get hrs r;;
+      RET (ris_sreg_set hrs' (red_PTree_set r sv hrs'))
   end.
 
 Lemma ok_transfer_hrs ctx inputs hrs:
-  ris_ok ctx (transfer_hrs inputs hrs)
+  WHEN transfer_hrs inputs hrs ~> hrs' THEN
+  ris_ok ctx hrs'
   <-> (ris_ok ctx hrs).
 Proof.
-  induction inputs as [|r l]; simpl.
-  + split; destruct 1; econstructor; simpl in *; intuition eauto.
-  + rewrite ok_hrset_red_sreg. auto.
+  induction inputs as [|r l]; simpl; wlp_simplify;
+  try (inv H; econstructor; eauto; fail).
+  + apply H0; rewrite <- ok_hrset_red_sreg; eauto.
+  + rewrite ok_hrset_red_sreg; auto.
 Qed.
+Local Hint Resolve ok_transfer_hrs: wlp.
 
 Lemma transfer_hrs_correct ctx inputs hrs sis:
+  WHEN transfer_hrs inputs hrs ~> hrs' THEN
   ris_refines ctx hrs sis ->
-  ris_refines ctx (transfer_hrs inputs hrs) (transfer_sis inputs sis).
+  ris_refines ctx hrs' (transfer_sis inputs sis).
 Proof.
-  destruct 1; intros.
-  induction inputs as [|r l].
-  + econstructor; eauto.
-    * erewrite ok_transfer_sis, ok_transfer_hrs; eauto.
-    * erewrite ok_transfer_hrs; eauto.
-    * erewrite ok_transfer_hrs; simpl; unfold ris_sreg_get; simpl; eauto.
-      intros; rewrite PTree.gempty. simpl; auto.
-  + econstructor; eauto.
-    * erewrite ok_transfer_sis, ok_transfer_hrs; eauto.
-    * erewrite ok_transfer_hrs; simpl.
-      intros; inversion IHl. erewrite MEM_EQ0.
-      - unfold transfer_sis; simpl; eauto.
-      - rewrite ok_transfer_hrs; simpl; eauto.
-    * erewrite ok_transfer_hrs; simpl.
-      intros H r0; inversion IHl.
+  unfold transfer_hrs;
+  induction inputs as [|r l]; wlp_simplify.
+  inversion H.
+  + constructor.
+    * erewrite ok_transfer_sis; split; intros X.
+      - constructor; simpl; rewrite OK_EQUIV in X; inv X; assumption.
+      - rewrite OK_EQUIV; constructor; inv X; assumption.
+    * intros X; inv X; simpl; apply MEM_EQ; constructor; auto.
+    * simpl. unfold ris_sreg_get.
+      intros;rewrite PTree.gempty. simpl; auto.
+  + constructor.
+    * erewrite ok_hrset_red_sreg; eauto.
+      inv H2. rewrite <- OK_EQUIV.
+      erewrite !ok_transfer_sis; reflexivity.
+    * intros X; inversion X; simpl in *.
+      rewrite ok_hrset_red_sreg in X.
+      inv H2; rewrite MEM_EQ; auto.
+    * simpl; intros X r0. inversion H2.
+      rewrite ok_hrset_red_sreg in X.
       erewrite red_PTree_set_refines; eauto.
-      - destruct (Pos.eq_dec); eauto.
-      - rewrite ok_transfer_hrs. auto.
+      destruct (Pos.eq_dec); auto.
+      inv H1. rewrite ok_transfer_sis in OK_EQUIV.
+      rewrite <- OK_EQUIV, OK_EQUIV0 in X.
+      erewrite H0; eauto.
 Qed.
 
 Definition tr_hrs := poly_tr (fun f tbl or => transfer_hrs (Regset.elements (pre_inputs f tbl or))).
@@ -866,28 +929,140 @@ Local Hint Resolve transfer_hrs_correct ok_transfer_hrs: core.
 Local Opaque transfer_hrs.
 
 Lemma ok_tr_hrs ctx fi hrs:
-  ris_ok ctx (tr_hrs (cf ctx) fi hrs)
+  WHEN tr_hrs (cf ctx) fi hrs ~> hrs' THEN
+  ris_ok ctx hrs'
   <-> (ris_ok ctx hrs).
 Proof.
    destruct fi; simpl; eauto.
 Qed.
 
-Lemma hrs_ok_tr_okpreserv ctx fi hrs: ris_ok ctx (tr_hrs (cf ctx) fi hrs) -> ris_ok ctx hrs.
+Lemma tr_hrs_correct ctx fi hrs sis:
+  WHEN tr_hrs (cf ctx) fi hrs ~> hrs' THEN
+  ris_refines ctx hrs sis ->
+  ris_refines ctx hrs' (tr_sis (cf ctx) fi sis).
 Proof.
-  rewrite ok_tr_hrs; auto.
+  unfold tr_hrs, poly_tr; destruct fi; wlp_simplify;
+  exploit transfer_hrs_correct; eauto.
+  Unshelve. all: auto.
 Qed.
 
-Lemma tr_hrs_correct ctx fi hrs sis:
-  ris_refines ctx hrs sis ->
-  ris_refines ctx (tr_hrs (cf ctx) fi hrs) (tr_sis (cf ctx) fi sis).
+Fixpoint hbuiltin_arg (hrs: ristate) (arg : builtin_arg reg): ?? builtin_arg sval := 
+  match arg with
+  | BA r => 
+         DO v <~ hrs_sreg_get hrs r;;
+         RET (BA v)
+  | BA_int n => RET (BA_int n)
+  | BA_long n => RET (BA_long n)
+  | BA_float f0 => RET (BA_float f0)
+  | BA_single s => RET (BA_single s)
+  | BA_loadstack chunk ptr => RET (BA_loadstack chunk ptr)
+  | BA_addrstack ptr => RET (BA_addrstack ptr)
+  | BA_loadglobal chunk id ptr => RET (BA_loadglobal chunk id ptr)
+  | BA_addrglobal id ptr => RET (BA_addrglobal id ptr)
+  | BA_splitlong ba1 ba2 => 
+    DO v1 <~ hbuiltin_arg hrs ba1;;
+    DO v2 <~ hbuiltin_arg hrs ba2;;
+    RET (BA_splitlong v1 v2)
+  | BA_addptr ba1 ba2 => 
+    DO v1 <~ hbuiltin_arg hrs ba1;;
+    DO v2 <~ hbuiltin_arg hrs ba2;;
+    RET (BA_addptr v1 v2)
+  end.
+
+Lemma hbuiltin_arg_correct hrs arg:
+  WHEN hbuiltin_arg hrs arg ~> hargs THEN forall ctx (f: reg -> sval)
+    (RR: forall r, sval_refines ctx (hrs r) (f r)),
+    eval_builtin_sval ctx hargs = eval_builtin_sval ctx (builtin_arg_map f arg).
 Proof.
-  intros REF. rewrite <- tr_sis_alt_def.
-  destruct fi; simpl; eauto.
+  induction arg; wlp_simplify.
+  + erewrite H; eauto.
+  + erewrite H; eauto.
+    erewrite H0; eauto.
+  + erewrite H; eauto.
+    erewrite H0; eauto.
+Qed.
+Global Opaque hbuiltin_arg.
+Local Hint Resolve hbuiltin_arg_correct: wlp.
+
+Fixpoint hbuiltin_args hrs (args: list (builtin_arg reg)): ?? list (builtin_arg sval) :=
+  match args with
+  | nil => RET nil
+  | a::l =>
+    DO ha <~ hbuiltin_arg hrs a;;
+    DO hl <~ hbuiltin_args hrs l;;
+    RET (ha::hl)
+    end.
+
+Lemma hbuiltin_args_correct hrs args:
+  WHEN hbuiltin_args hrs args ~> hargs THEN forall ctx (f: reg -> sval)
+    (RR: forall r, sval_refines ctx (hrs r) (f r)),
+    bargs_refines ctx hargs (List.map (builtin_arg_map f) args).
+Proof.
+  unfold bargs_refines; induction args; wlp_simplify.
+  erewrite H; eauto.
+  erewrite H0; eauto.
+Qed.
+Global Opaque hbuiltin_args.
+Local Hint Resolve hbuiltin_args_correct: wlp.
+
+Definition hsum_left hrs (ros: reg + ident): ?? (sval + ident) :=
+  match ros with
+  | inl r => DO hr <~ hrs_sreg_get hrs r;; RET (inl hr) 
+  | inr s => RET (inr s)
+  end.
+
+Lemma hsum_left_correct hrs ros:
+  WHEN hsum_left hrs ros ~> hsi THEN forall ctx (f: reg -> sval)
+    (RR: forall r, sval_refines ctx (hrs r) (f r)),
+    rsvident_refines ctx hsi (sum_left_map f ros).
+Proof.
+  destruct ros; wlp_simplify;
+  econstructor; eauto.
+Qed.
+Global Opaque hsum_left.
+Local Hint Resolve hsum_left_correct: wlp.
+
+(** * Symbolic execution of final step *)
+Definition hrexec_final_sfv (i: final) hrs: ?? sfval := 
+  match i with
+  | Bgoto pc => RET (Sgoto pc)
+  | Bcall sig ros args res pc => 
+      DO svos <~ hsum_left hrs ros;;
+      DO sargs <~ hlist_args hrs args;;
+      RET (Scall sig svos sargs res pc)
+  | Btailcall sig ros args =>
+      DO svos <~ hsum_left hrs ros;;
+      DO sargs <~ hlist_args hrs args;;
+      RET (Stailcall sig svos sargs)
+  | Bbuiltin ef args res pc =>
+      DO sargs <~ hbuiltin_args hrs args;;
+      RET (Sbuiltin ef sargs res pc)
+  | Breturn or => 
+      match or with
+      | Some r => DO hr <~ hrs_sreg_get hrs r;; RET (Sreturn (Some hr))
+      | None => RET (Sreturn None)
+      end
+  | Bjumptable reg tbl =>
+      DO sv <~ hrs_sreg_get hrs reg;;
+      RET (Sjumptable sv tbl)
+  end.
+
+Lemma hrexec_final_sfv_correct ctx fi hrs sis:
+  WHEN hrexec_final_sfv fi hrs ~> hrs' THEN forall
+  (REF: ris_refines ctx hrs sis)
+  (OK: ris_ok ctx hrs),
+  rfv_refines ctx hrs' (sexec_final_sfv fi sis).
+Proof.
+  destruct fi; simpl; wlp_simplify; repeat econstructor;
+  try inversion REF; try erewrite H; eauto.
 Qed.
 
 Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := 
   match ib with
-  | BF fin _ => RET (Rfinal (tr_hrs f fin hrs) (sexec_final_sfv fin hrs))
+  | BF fin _ =>
+      DO sfv <~ hrexec_final_sfv fin hrs;;
+      DO hrs' <~ tr_hrs f fin hrs;;
+      RET (Rfinal hrs' sfv)
   (* basic instructions *)
   | Bnop _ => k hrs
   | Bop op args dst _ =>
@@ -916,7 +1091,7 @@ Definition hrexec f ib :=
   DO init <~ hrs_init;;
   hrexec_rec f ib init (fun _ => RET Rabort).
 
-Local Hint Resolve exec_final_refpreserv tr_hrs_correct hrs_ok_tr_okpreserv: core.
+Local Hint Resolve exec_final_refpreserv ok_tr_hrs: core.
 Local Hint Constructors rst_refines: core.
 
 Lemma hrexec_rec_correct1 ctx ib: 
@@ -938,13 +1113,18 @@ Lemma hrexec_rec_correct1 ctx ib:
   rst_refines ctx rst st.
 Proof.
   induction ib; try (wlp_simplify; fail).
+  - (* BF *)
+    wlp_simplify; exploit tr_hrs_correct; eauto.
+    intros; constructor; auto.
+    intros X; apply H0 in X.
+    exploit hrexec_final_sfv_correct; eauto.
   - (* Bnop *) wlp_simplify; eapply CONT; eauto.
   - (* Bload *) destruct trap; wlp_simplify.
   - (* Bseq *)
     wlp_simplify.
     eapply IHib1. 3-7: eauto.
     + simpl. eapply sexec_rec_okpreserv; eauto.
-    + intros; subst. eapply IHib2; eauto.
+    + intros; eapply IHib2; eauto.
   - (* Bcond *)
     simpl; intros; wlp_simplify.
     assert (rOK: ris_ok ctx hrs). {
@@ -954,9 +1134,11 @@ Proof.
     exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
               (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
     exploit H; eauto; intros (SEVAL & EQC); subst; auto.
-    all: simpl in SOUT; generalize SOUT; inversion_SOME b0; try_simplify_someHyps.
-    * intros; eapply IHib1; eauto.
-    * intros; eapply IHib2; eauto.
+    all:
+      simpl in SOUT; generalize SOUT; clear SOUT;
+      inversion_SOME b0; try_simplify_someHyps.
+    + intros; eapply IHib1; eauto.
+    + intros; eapply IHib2; eauto.
 Qed.
 
 Lemma hrexec_correct1 ctx ib sis sfv:
@@ -969,23 +1151,80 @@ Proof.
   eapply hrexec_rec_correct1; eauto; simpl; congruence.
 Qed.
 
-(*Lemma hrexec_rec_correct2 ctx ib: 
+Lemma hrexec_rec_okpreserv ctx ib: 
+  forall k
+  (CONT: forall hrs lhrs rfv,
+    WHEN k hrs ~> rst THEN
+    get_routcome ctx rst = Some (rout lhrs rfv) ->
+    ris_ok ctx lhrs ->
+    ris_ok ctx hrs)
+  hrs lhrs rfv,
+  WHEN hrexec_rec (cf ctx) ib hrs k ~> rst THEN
+  get_routcome ctx rst = Some (rout lhrs rfv) ->
+  ris_ok ctx lhrs ->
+  ris_ok ctx hrs.
+Proof.
+  induction ib; simpl; try (wlp_simplify; try_simplify_someHyps; fail).
+  - (* Bop *)
+    wlp_simplify; exploit hrs_ok_op_okpreserv; eauto.
+  - (* Bload *)
+    destruct trap; wlp_simplify; try_simplify_someHyps.
+    exploit hrs_ok_load_okpreserv; eauto.
+  - (* Bstore *)
+    wlp_simplify; exploit hrs_ok_store_okpreserv; eauto.
+  - (* Bcond *)
+    wlp_simplify; generalize H2; clear H2; inversion_SOME b; destruct b; try_simplify_someHyps.
+Qed.
+Local Hint Resolve hrexec_rec_okpreserv: wlp.
+
+Lemma hrexec_rec_correct2 ctx ib: 
   forall rk k
-  (CONTh: forall ris lris rfv, get_routcome ctx (rk ris) = Some (rout lris rfv) ->  ris_ok ctx lris -> ris_ok ctx ris)
-  (CONT: forall ris sis lris rfv st,
-    ris_refines ctx ris sis ->
-    rk ris = st ->
-    get_routcome ctx (rk ris) = Some (rout lris rfv) ->
-    ris_ok ctx lris ->
-    rst_refines ctx (rk ris) (k sis))
-  ris sis lris rfv st
-  (REF: ris_refines ctx ris sis)
-  (EXEC: rexec_rec (cf ctx) ib ris rk = st)
-  (SOUT: get_routcome ctx st = Some (rout lris rfv))
-  (OK: ris_ok ctx lris)
-  , rst_refines ctx st (sexec_rec (cf ctx) ib sis k).
+  (CONTh: forall hrs lhrs rfv,
+    WHEN rk hrs ~> rst THEN
+    get_routcome ctx rst = Some (rout lhrs rfv) ->
+    ris_ok ctx lhrs ->
+    ris_ok ctx hrs)
+  (CONT: forall hrs sis lhrs rfv,
+    ris_refines ctx hrs sis ->
+    WHEN rk hrs ~> rst THEN
+    get_routcome ctx rst = Some (rout lhrs rfv) ->
+    ris_ok ctx lhrs ->
+    rst_refines ctx rst (k sis))
+  hrs sis lhrs rfv
+  (REF: ris_refines ctx hrs sis),
+  WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN
+  get_routcome ctx rst = Some (rout lhrs rfv) ->
+  ris_ok ctx lhrs ->
+  rst_refines ctx rst (sexec_rec (cf ctx) ib sis k).
 Proof.
-   Admitted.*)
+  induction ib; try (wlp_simplify; fail).
+  - (* BF *)
+    wlp_simplify; exploit tr_hrs_correct; eauto.
+    intros; constructor; auto.
+    intros X; apply H0 in X.
+    exploit hrexec_final_sfv_correct; eauto.
+  - (* Bnop *) wlp_simplify; eapply CONT; eauto.
+  - (* Bload *) destruct trap; wlp_simplify.
+  - (* Bseq *)
+    wlp_simplify.
+    eapply IHib1. 3-6: eauto.
+    + simpl; eapply hrexec_rec_okpreserv; eauto.
+    + intros; eapply IHib2; eauto.
+  - (* Bcond *)
+    simpl; intros; wlp_simplify.
+    assert (rOK: ris_ok ctx hrs). {
+      simpl in H2; generalize H2; inversion_SOME b0; destruct b0; try_simplify_someHyps.
+    }
+    exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
+              (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
+    exploit H; eauto; intros (SEVAL & EQC); subst; auto.
+    all:
+      simpl in H2; generalize H2; clear H2;
+      inversion_SOME b0; try_simplify_someHyps.
+    + intros; eapply IHib1; eauto.
+    + intros; eapply IHib2; eauto.
+    Unshelve. all: auto.
+Qed.
 
 Lemma hrexec_correct2 ctx ib hrs rfv:
   WHEN hrexec (cf ctx) ib ~> rst THEN
@@ -993,44 +1232,15 @@ Lemma hrexec_correct2 ctx ib hrs rfv:
   (ris_ok ctx hrs) ->
   rst_refines ctx rst (sexec (cf ctx) ib).
 Proof.
-Admitted.
-
-Lemma hrexec_correct_aux ctx ib:
-  WHEN hrexec (cf ctx) ib ~> rst THEN
-  exists st, sexec (cf ctx) ib = st /\ rst_refines ctx rst st.
-Proof.
-  unfold hrexec; wlp_simplify.
-  repeat eexists.
-Admitted.
+  unfold hrexec; intros; wlp_simplify.
+  eapply hrexec_rec_correct2; eauto; simpl;
+  wlp_simplify; congruence.
+Qed.
 
 Global Opaque hrexec.
 
 End CanonBuilding.
 
-(** Correction of concrete symbolic execution wrt abstract symbolic execution *)
-Theorem hrexec_correct
-  (hC_hsval : hashinfo sval -> ?? sval)
-  (hC_list_hsval : hashinfo list_sval -> ?? list_sval)
-  (hC_hsmem : hashinfo smem -> ?? smem)
-  (ctx: iblock_exec_context) 
-  (ib: iblock):
-       WHEN hrexec hC_hsval hC_list_hsval hC_hsmem (cf ctx) ib ~> hrs THEN forall
-        (hC_hsval_correct: forall hs,
-            WHEN hC_hsval hs ~> hs' THEN forall ctx,
-                sval_refines ctx (hdata hs) hs')
-        (hC_list_hsval_correct: forall lh,
-            WHEN hC_list_hsval lh ~> lh' THEN forall ctx,
-              list_sval_refines ctx (hdata lh) lh')
-         (hC_hsmem_correct: forall hm,
-            WHEN hC_hsmem hm ~> hm' THEN forall ctx,
-              smem_refines ctx (hdata hm) hm'),
-         exists st : sstate, sexec (cf ctx) ib = st /\ rst_refines ctx hrs st.
-Proof.
-  wlp_simplify.
-  eapply hrexec_correct_aux; eauto.
-Qed.
-Local Hint Resolve hrexec_correct: wlp.
-
 (** * Implementing the simulation test with concrete hash-consed symbolic execution *)
 
 Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
@@ -1267,34 +1477,30 @@ Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock):
   symbolic_simu f1 f2 ib1 ib2.
 Proof. (* TODO *)
   unfold symbolic_simu; wlp_simplify.
-    exploit hrexec_correct; eauto.
   eapply rst_simu_correct; eauto.
-  + intros; eapply hrexec_correct1; eauto.
-    1-3: wlp_simplify. intuition eauto.
-    simpl. eauto.
-    intuition eauto.
-    admit.
-Admitted.
+  + intros; eapply hrexec_correct1; eauto; wlp_simplify.
+  + intros; eapply hrexec_correct2; eauto; wlp_simplify.
+Qed.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.
 
-Program Definition aux_simu_check (f1 f2: function) (ib1 ib2: iblock): ?? bool :=
+Program Definition aux_simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): ?? bool :=
    DO r <~ 
      (TRY 
-       simu_check_single f1 f2 ib1 ib2;; 
+       simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);; 
        RET true
       CATCH_FAIL s, _ =>
        println ("simu_check_failure:" +; s);;
        RET false
-       ENSURE (fun b => b=true -> symbolic_simu f1 f2 ib1 ib2));;
+       ENSURE (fun b => b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));;
    RET (`r).
 Obligation 1.
   split; wlp_simplify. discriminate.
 Qed.
 
-Lemma aux_simu_check_correct (f1 f2: function) (ib1 ib2: iblock):
-  WHEN aux_simu_check f1 f2 ib1 ib2 ~> b THEN
-  b=true -> symbolic_simu f1 f2 ib1 ib2.
+Lemma aux_simu_check_correct (f1 f2: function) (ibf1 ibf2: iblock_info):
+  WHEN aux_simu_check f1 f2 ibf1 ibf2 ~> b THEN
+  b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry).
 Proof.
   unfold aux_simu_check; wlp_simplify.
   destruct exta; simpl; auto.
@@ -1304,8 +1510,8 @@ Qed.
 
 Import UnsafeImpure.
 
-Definition simu_check (f1 f2: function) (ib1 ib2: iblock): res unit := 
-  match unsafe_coerce (aux_simu_check f1 f2 ib1 ib2) with
+Definition simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): res unit := 
+  match unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2) with
   | Some true => OK tt
   | _ => Error (msg "simu_check has failed")
   end.
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index 12840f62..63114125 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -2,7 +2,7 @@ Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad BTL.
 
-Require Import Errors Linking BTL_SEtheory.
+Require Import Errors Linking BTL_SEtheory BTL_SEimpl.
 
 (** External oracle *)
 Axiom scheduler: BTL.function -> BTL.code.
@@ -48,18 +48,69 @@ Record match_function (f1 f2: BTL.function): Prop := {
 
 Local Open Scope error_monad_scope.
 
-Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO: fixme *)
+Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit :=
+  match lpc with
+  | nil => OK tt
+  | pc :: lpc' =>
+      match (fn_code f1)!pc, (fn_code f2)!pc with
+      | Some ibf1, Some ibf2 =>
+          do _ <- simu_check f1 f2 ibf1 ibf2;
+          check_symbolic_simu_rec f1 f2 lpc'
+      | _, _ => Error (msg "check_symbolic_simu_rec: code tree mismatch")
+      end
+  end.
+
+Definition check_symbolic_simu (f1 f2: BTL.function): res unit :=
+  check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))).
+
+Lemma check_symbolic_simu_rec_input_equiv lpc: forall f1 f2 x,
+  check_symbolic_simu_rec f1 f2 lpc = OK x ->
+  lpc = (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))) ->
+  equiv_input_regs f1 f2.
+Proof.
+Admitted.
+(*
+  unfold equiv_input_regs; induction lpc; simpl; intros f1 f2 x X EQL1.
+  - destruct (map _ _) eqn:EQL2; inv X; intuition;
+    symmetry in EQL1; apply map_eq_nil in EQL1; apply map_eq_nil in EQL2.
+    + destruct (fn_code f1), (fn_code f2); simpl in *; auto.
+      inv EQL2.
+      unfold PTree.elements in EQL1.
+    + admit.
+    + 
+  destruct ((fn_code f1) ! a), ((fn_code f2) ! a); monadInv X.
+  eapply IHlpc; eauto.
+Qed.
+ *)
 
 Lemma check_symbolic_simu_input_equiv x f1 f2:
   check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2.
 Proof.
+  unfold check_symbolic_simu; simpl; intros X.
+  eapply check_symbolic_simu_rec_input_equiv; eauto.
+Qed.
+
+Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x,
+  check_symbolic_simu_rec f1 f2 lpc = OK x ->
+  forall pc ib1, (fn_code f1)!pc = Some ib1 ->
+       exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
+Proof.
 Admitted.
+  (*
+  induction lpc; simpl; intros f1 f2 x X pc ib1 PC; try (inv X; fail).
+  destruct ((fn_code f1) ! pc), ((fn_code f2) ! pc); inv X.
+  eapply IHlpc; eauto.
+Qed.
+   *)
 
 Lemma check_symbolic_simu_correct x f1 f2:
   check_symbolic_simu f1 f2 = OK x ->
   forall pc ib1, (fn_code f1)!pc = Some ib1 ->
        exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
-Admitted.
+Proof.
+  unfold check_symbolic_simu; intros X pc ib1 PC.
+  eapply check_symbolic_simu_rec_correct; eauto.
+Qed.
 
 Definition transf_function (f: BTL.function) :=
   let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 95363194..91e650e8 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -105,11 +105,12 @@ Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
 Proof.
   intros TRANSF; destruct f; simpl; inv TRANSF.
+Admitted. (*
   + exploit transf_function_correct; eauto.
     econstructor. intros MATCH_F.
     eapply match_Internal; eauto.
   + eapply match_External.
-Qed.
+             Qed.*)
 
 Lemma function_ptr_preserved:
   forall v f,