From c49cec7b43157a65283dec8bbe343293faa7d012 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 10 Jun 2021 08:48:06 +0200
Subject: fix rst_simu_correct

---
 scheduling/BTL_SEsimuref.v | 48 ++++++++++++++++++++--------------------------
 1 file changed, 21 insertions(+), 27 deletions(-)

(limited to 'scheduling/BTL_SEsimuref.v')

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 2ca36b11..f39da275 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -231,9 +231,6 @@ Proof.
   destruct b; simpl; auto.
 Qed.
 
-
-(* Comment prend on en compte le ris en cours d'execution ??? *)
-
 Inductive rst_refines ctx: rstate -> sstate -> Prop :=
   | Reffinal ris sis rfv sfv
       (RIS: ris_refines ctx ris sis)
@@ -274,30 +271,27 @@ Qed.
 
 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,
-   rst_refines (bctx1 ctx) rst1 st1 ->
-   rst_refines (bctx2 ctx) rst2 st2 ->
-   sstate_simu ctx st1 st2.
-Proof.
-  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_si_ok; eauto.
-    erewrite OK_EQUIV; eauto.
-    intros ROK1.
-    exploit ris_simu_ok_preserv; eauto.
-  - (* cond_simu *)
-    destruct (seval_condition (bctx1 ctx) cond args) eqn: SCOND; try congruence.
-    generalize RCOND0.
-    erewrite <- seval_condition_preserved, RCOND by eauto.
-    intros SCOND0; rewrite <- SCOND0 in RCOND0.
-    erewrite <- SCOND0.
-    destruct b; simpl.
-    * intros; exploit IHrst_simu1; eauto.
-    * intros; exploit IHrst_simu2; eauto.
+Lemma rst_simu_correct f1 f2 (ctx: simu_proof_context f1 f2) rst1 rst2 st1 st2
+   (SIMU: rst_simu rst1 rst2) 
+   (REF1: forall sis sfv, get_soutcome (bctx1 ctx) st1 = Some (sout sis sfv) -> si_ok (bctx1 ctx) sis -> rst_refines (bctx1 ctx) rst1 st1)
+   (REF2: forall ris rfv, get_routcome (bctx2 ctx) rst2 = Some (rout ris rfv) -> ris_ok (bctx2 ctx) ris -> rst_refines (bctx2 ctx) rst2 st2)
+   :sstate_simu ctx st1 st2.
+Proof.
+  intros sis1 sfv1 SOUT OK1.
+  exploit REF1; eauto.
+  clear REF1; intros REF1.
+  exploit rst_refines_outcome_down; eauto. clear REF1 SOUT.
+  intros (ris1 & rfv1 & ROUT1 & REFI1 & REFF1).
+  rewrite OK_EQUIV in OK1; eauto. 
+  exploit REFF1; eauto. clear REFF1; intros REFF1.
+  exploit rst_simu_lroutcome; eauto.
+  intros (ris2 & rfv2 & ROUT2 & SIMUI & SIMUF). clear ROUT1.
+  exploit ris_simu_ok_preserv; eauto.
+  clear OK1. intros OK2.
+  exploit REF2; eauto. clear REF2; intros REF2.
+  exploit rst_refines_outcome_up; eauto.
+  intros (sis2 & sfv2 & SOUT & REFI2 & REFF2).
+  do 2 eexists; split; eauto.
 Qed.
 
 (** * Refinement of the symbolic execution *)
-- 
cgit