hrexec1

1 files changed, 81 insertions, 27 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 94d7375d..c32001d4 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -670,15 +670,15 @@ Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
   | None => FAILWITH msg
   end.
 
-Definition hris_init: ?? ristate
+Definition hrs_init: ?? ristate
   := DO hm <~ hSinit ();;
      RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.
 
-Lemma ris_init_correct:
-  WHEN hris_init ~> hris THEN
-  forall ctx, ris_refines ctx hris sis_init.
+Lemma hrs_init_correct:
+  WHEN hrs_init ~> hrs THEN
+  forall ctx, ris_refines ctx hrs sis_init.
 Proof.
-  unfold hris_init, sis_init; wlp_simplify.
+  unfold hrs_init, sis_init; wlp_simplify.
   econstructor; simpl in *; eauto.
   + split; destruct 1; econstructor; simpl in *;
     try rewrite H; try congruence; trivial.
@@ -686,7 +686,7 @@ Proof.
     intros; rewrite PTree.gempty; eauto.
 Qed.
 
-Definition hrset_sreg r lr rsv (hrs: ristate): ?? ristate :=
+Definition hrs_sreg_set r lr rsv (hrs: ristate): ?? ristate :=
   DO ok_lsv <~
     (if may_trap rsv lr
      then DO sv <~ root_happly rsv lr hrs;;
@@ -730,8 +730,8 @@ Proof.
     + intros. exploit (ALLR a); simpl; eauto.
 Qed.
 
-Lemma hrset_sreg_correct r lr rsv hrs:
-  WHEN hrset_sreg r lr rsv hrs ~> hrs' THEN forall ctx sis
+Lemma hrs_sreg_set_correct r lr rsv hrs:
+  WHEN hrs_sreg_set r lr rsv hrs ~> hrs' THEN forall ctx sis
   (REF: ris_refines ctx hrs sis),
   ris_refines ctx hrs' (set_sreg r (rsv lr sis) sis).
 Proof.
@@ -783,6 +783,8 @@ Proof.
       rewrite ris_sreg_set_access.
       erewrite red_PTree_set_refines; intuition eauto.
 Qed.
+Global Opaque hrs_sreg_set.
+Local Hint Resolve hrs_sreg_set_correct: wlp.
 
 Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := 
   match ib with
@@ -790,10 +792,10 @@ Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate :=
   (* basic instructions *)
   | Bnop _ => k hrs
   | Bop op args dst _ =>
-      DO next <~ hrset_sreg dst args (Rop op) hrs;;
+      DO next <~ hrs_sreg_set dst args (Rop op) hrs;;
       k next
   | Bload TRAP chunk addr args dst _ =>
-      DO next <~ hrset_sreg dst args (Rload TRAP chunk addr) hrs;;
+      DO next <~ hrs_sreg_set dst args (Rload TRAP chunk addr) hrs;;
       k next
   | Bload NOTRAP chunk addr args dst _ => RET Rabort
   | Bstore chunk addr args src _ =>
@@ -812,7 +814,7 @@ Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate :=
   .
 
 Definition hrexec f ib :=
-  DO init <~ hris_init;;
+  DO init <~ hrs_init;;
   hrexec_rec f ib init (fun _ => RET Rabort).
 
 Lemma hrexec_rec_correct1 ctx ib: 
@@ -823,28 +825,25 @@ Lemma hrexec_rec_correct1 ctx ib:
     k sis = st ->
     get_soutcome ctx (k sis) = Some (sout lsis sfv) ->
     si_ok ctx lsis ->
-    WHEN rk hrs ~> ris' THEN
-    rst_refines ctx ris' (k sis))
+    WHEN rk hrs ~> rst THEN
+    rst_refines ctx rst (k sis))
   hrs sis lsis sfv st
   (REF: ris_refines ctx hrs sis)
   (EXEC: sexec_rec (cf ctx) ib sis k = st)
   (SOUT: get_soutcome ctx st = Some (sout lsis sfv))
   (OK: si_ok ctx lsis),
-  WHEN hrexec_rec (cf ctx) ib hrs rk ~> hrs THEN
-  rst_refines ctx hrs st.
+  WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN
+  rst_refines ctx rst st.
 Proof.
-  (*
   induction ib; wlp_simplify.
   - admit.
   - eapply CONT; eauto.
-  - try_simplify_someHyps. intros OUT.
+  - autodestruct; try_simplify_someHyps; try congruence; intros; subst.
+(*
+    unfold sexec_load.
+    exploit hrs_sreg_set_correct; eauto.
     eapply CONT; eauto.
-    intuition eauto.
-    econstructor; intuition eauto.
-    inv REF. inv H2.
-    intuition eauto.
-
-
+    destruct next.
   - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto.
   - (* seq *)
     intros; subst.
@@ -865,8 +864,56 @@ Proof.
      Qed.*)
 Admitted.
 
-Definition hsexec (f: function) ib: ?? rstate :=
-  hrexec f ib.
+Lemma hrexec_correct1 ctx ib sis sfv:
+  get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) ->
+  (si_ok ctx sis) ->
+  WHEN hrexec (cf ctx) ib ~> rst THEN
+  rst_refines ctx rst (sexec (cf ctx) ib).
+Proof.
+  unfold sexec; intros; wlp_simplify.
+  eapply hrexec_rec_correct1; eauto; simpl; try congruence; split.
+  - intuition eauto.
+    + inv H2; constructor; auto; simpl; congruence.
+    + inv H2; split; simpl in *; try congruence; trivial.
+  - intros X; simpl in *; auto.
+  - intros X r; inv X; simpl in *.
+    unfold ris_sreg_get; simpl; rewrite PTree.gempty; simpl.
+    reflexivity.
+Qed.
+
+(*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).
+Proof.
+   Admitted.*)
+
+Lemma hrexec_correct2 ctx ib hrs rfv:
+  WHEN hrexec (cf ctx) ib ~> rst THEN
+  get_routcome ctx rst = Some (rout hrs rfv) ->
+  (ris_ok ctx hrs) ->
+  rst_refines ctx rst (sexec (cf ctx) ib).
+Proof.
+Admitted.
+
+Lemma hrexec_simu_correct 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.
 
 End CanonBuilding.
 
@@ -1094,7 +1141,7 @@ Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit :=
   DO hC_sval <~ hCons hSVAL;;
   DO hC_list_hsval <~ hCons hLSVAL;;
   DO hC_hsmem <~ hCons hSMEM;;
-  let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
+  let hsexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
   (* performing the hash-consed executions *)
   DO hst1 <~ hsexec f1 ib1;;
   DO hst2 <~ hsexec f2 ib2;;
@@ -1104,8 +1151,15 @@ Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit :=
 Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock):
   WHEN simu_check_single f1 f2 ib1 ib2 ~> _ THEN
   symbolic_simu f1 f2 ib1 ib2.
-Proof.
+Proof. (* TODO *)
   unfold symbolic_simu; wlp_simplify.
+  eapply rst_simu_correct; eauto.
+  + intros; eapply hrexec_correct1; eauto.
+    1-3: wlp_simplify. unfold hrexec.
+    simpl. eauto.
+    intuition eauto.
+  + intros; eapply rexec_correct2; eauto.
+  intros ctxz.
 Admitted.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.