theorem rexec_simu_correct

1 files changed, 111 insertions, 25 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index f39da275..852bced0 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -619,7 +619,7 @@ Proof.
   destruct fi; simpl; eauto.
 Qed.
 
-Lemma si_ok_tr_sis_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis.
+Lemma si_ok_tr_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis.
 Admitted.
 
 Lemma si_ok_op_down ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis.
@@ -632,7 +632,26 @@ Lemma si_ok_store_down ctx chunk addr args src sis: si_ok ctx (sexec_store chunk
 Admitted.
 
 (* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *)
-Local Hint Resolve si_ok_tr_sis_down si_ok_op_down si_ok_trap_down si_ok_store_down: core.
+Local Hint Resolve si_ok_tr_down si_ok_op_down si_ok_trap_down si_ok_store_down: core.
+
+Lemma sexec_rec_down ctx ib: 
+  forall k
+  (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
+  sis lsis sfv
+  (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv))
+  (OK: si_ok ctx lsis)
+  ,si_ok ctx sis.
+Proof.
+  induction ib; simpl; try (autodestruct; simpl).
+  1-6: try_simplify_someHyps.
+  - intros. eapply IHib1. 2-3: eauto.
+    eapply IHib2; eauto.
+  - intros k CONT sis lsis sfv.
+    do 2 autodestruct.
+    + intros; eapply IHib1; eauto.
+    + intros; eapply IHib2; eauto.
+Qed.
+
 
 (** RAFFINEMENT EXEC SYMBOLIQUE **)
 
@@ -656,30 +675,15 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate :=
   end
   .
 
+Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort).
+
+
 Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_ris_imp 
   rexec_op_correct rexec_load_correct rexec_store_correct: core.
 
 Local Hint Constructors rst_refines: core.
 
-Lemma sexec_rec_down ctx ib: 
-  forall k
-  (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
-  sis lsis sfv
-  (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv))
-  (OK: si_ok ctx lsis)
-  ,si_ok ctx sis.
-Proof.
-  induction ib; simpl; try (autodestruct; simpl).
-  1-6: try_simplify_someHyps.
-  - intros. eapply IHib1. 2-3: eauto.
-    eapply IHib2; eauto.
-  - intros k CONT sis lsis sfv.
-    do 2 autodestruct.
-    + intros; eapply IHib1; eauto.
-    + intros; eapply IHib2; eauto.
-Qed.
-
-Lemma rexec_rec_correct ctx ib: 
+Lemma rexec_rec_correct1 ctx ib: 
   forall rk k
   (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
   (CONT: forall ris sis lsis sfv st, ris_refines ctx ris sis -> k sis = st -> get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> rst_refines ctx (rk ris) (k sis))
@@ -710,12 +714,94 @@ Proof.
     econstructor; try_simplify_someHyps.
 Qed.
 
-Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort).
-
-Lemma rexec_correct ctx ib sis sfv:
+Lemma rexec_correct1 ctx ib sis sfv:
   get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) ->
   (si_ok ctx sis) ->
   rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib).
 Proof.
-  unfold sexec; intros; eapply rexec_rec_correct; eauto; simpl; congruence.
+  unfold sexec; intros; eapply rexec_rec_correct1; eauto; simpl; congruence.
+Qed.
+
+
+(** COPIER-COLLER ... Y a-t-il moyen de l'eviter ? **)
+
+Lemma ris_ok_tr_down ctx fi ris: ris_ok ctx (tr_ris (cf ctx) fi ris) -> ris_ok ctx ris.
+Admitted.
+
+Lemma ris_ok_op_down ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris.
+Admitted.
+
+Lemma ris_ok_trap_down ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris.
+Admitted.
+
+Lemma ris_ok_store_down ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris.
+Admitted.
+
+(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *)
+Local Hint Resolve ris_ok_tr_down ris_ok_op_down ris_ok_trap_down ris_ok_store_down: core.
+
+Lemma rexec_rec_down ctx ib: 
+  forall k
+  (CONT: forall ris lris rfv, get_routcome ctx (k ris) = Some (rout lris rfv) ->  ris_ok ctx lris -> ris_ok ctx ris)
+  ris lris rfv
+  (ROUT: get_routcome ctx (rexec_rec (cf ctx) ib ris k) = Some (rout lris rfv))
+  (OK: ris_ok ctx lris)
+  ,ris_ok ctx ris.
+Proof.
+  induction ib; simpl; try (autodestruct; simpl).
+  1-6: try_simplify_someHyps.
+  - intros. eapply IHib1. 2-3: eauto.
+    eapply IHib2; eauto.
+  - intros k CONT sis lsis sfv.
+    do 2 autodestruct.
+    + intros; eapply IHib1; eauto.
+    + intros; eapply IHib2; eauto.
+Qed.
+
+Lemma rexec_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.
+  induction ib; simpl; try (intros; subst; eauto; fail).
+  - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto.
+  - (* seq *)
+    intros; subst.
+    eapply IHib1. 3-6: eauto.
+    + simpl. eapply rexec_rec_down; eauto.
+    + intros; subst. eapply IHib2; eauto.
+  - (* cond *)
+    intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst.
+    assert (OK0: ris_ok ctx ris). {
+      eapply rexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
+    }
+    generalize OUT; clear OUT; simpl.
+    autodestruct.
+    intros COND; generalize COND.
+    erewrite seval_condition_refpreserv; eauto.
+    econstructor; try_simplify_someHyps.
+Qed.
+
+Lemma rexec_correct2 ctx ib ris rfv:
+  get_routcome ctx (rexec (cf ctx) ib) = Some (rout ris rfv) ->
+  (ris_ok ctx ris) ->
+  rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib).
+Proof.
+  unfold rexec; intros; eapply rexec_rec_correct2; eauto; simpl; congruence.
+Qed.
+
+Theorem rexec_simu_correct f1 f2 ib1 ib2:
+  rst_simu (rexec f1 ib1) (rexec f2 ib2) ->
+  symbolic_simu f1 f2 ib1 ib2.
+Proof.
+  intros SIMU ctx.
+  eapply rst_simu_correct; eauto.
+  + intros; eapply rexec_correct1; eauto.
+  + intros; eapply rexec_correct2; eauto.
 Qed.