progress in BTL_SEsimuref

1 files changed, 44 insertions, 12 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index c322a9a5..a4da4291 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -191,14 +191,14 @@ Inductive rstate :=
   .
 
 Inductive rst_simu: rstate -> rstate -> Prop :=
-  | Rfinal_simu ris1 ris2 rfv1 rfv2:
-      ris_simu ris1 ris2 ->
-      rfv_simu rfv1 rfv2 ->
-      rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
-  | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2:
-      rst_simu rifso1 rifso2 ->
-      rst_simu rifnot1 rifnot2 ->
-      rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2)
+  | Rfinal_simu ris1 ris2 rfv1 rfv2
+      (RIS: ris_simu ris1 ris2)
+      (RFV: rfv_simu rfv1 rfv2)
+      : rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
+  | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2
+      (IFSO: rst_simu rifso1 rifso2)
+      (IFNOT: rst_simu rifnot1 rifnot2)
+      : rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2)
   | Rabort_simu: rst_simu Rabort Rabort
 (* TODO: extension à voir dans un second temps !
   | Rcond_skip cond rargs rifso1 rifnot1 rst:
@@ -225,6 +225,8 @@ Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
       : rst_refines ctx Rabort Sabort
   .
 
+Local Hint Resolve ris_simu_correct rvf_simu_correct: core.
+
 Lemma rst_simu_correct rst1 rst2:
    rst_simu rst1 rst2 ->
    forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*),
@@ -233,7 +235,37 @@ Lemma rst_simu_correct rst1 rst2:
    (* ok1 -> ok2 -> *)
    sstate_simu ctx st1 st2.
 Proof.
-  induction 1; simpl; auto.
-  - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
-    inv REF1. inv REF2. inv SEM1.
-Admitted.
\ No newline at end of file
+  induction 1; simpl; intros f1 f2 ctx st1 st2 REF1 REF2 sis1 svf1 SEM1;
+  inv REF1; inv REF2; simpl in *; inv SEM1; auto.
+  - (* final_simu *) 
+    do 2 eexists; intuition; eauto.
+    exploit sem_sok; eauto.
+    erewrite OK_EQUIV; eauto.
+    intros ROK1.
+    exploit ris_simu_ok_preserv; eauto.
+  - (* cond_simu *)
+    destruct (seval_condition (bctx1 ctx) cond args sm) eqn: SCOND; try congruence.
+    generalize RCOND0.
+    erewrite <- seval_condition_preserved, RCOND by eauto.
+    intros SCOND0; rewrite <- SCOND0 in RCOND0.
+    erewrite <- SCOND0.
+    destruct b; simpl.
+    * exploit IHrst_simu1; eauto.
+    * exploit IHrst_simu2; eauto.
+Qed.
+
+
+(** TODO: could be useful ?
+Lemma seval_condition_valid_preserv ctx cond args sm b
+  (VALID_PRESERV: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs)
+  :seval_condition ctx cond args sm = Some b ->
+   seval_condition ctx cond args Sinit = Some b.
+Proof.
+  unfold seval_condition; autodestruct; simpl; try congruence.
+  intros EVAL_LIST.
+  autodestruct; try congruence.
+  intros MEM COND. rewrite <- COND.
+  eapply cond_valid_pointer_eq; intros.
+  exploit VALID_PRESERV; eauto.
+Qed.
+*)
\ No newline at end of file