fix sstate_simu

1 files changed, 18 insertions, 31 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 40c28934..98587b66 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -20,21 +20,8 @@ Require Import RTL BTL OptionMonad BTL_SEtheory.
 
 (** * Refinement of data-structures and of the specification of the simulation test *)
 
-Record sis_ok ctx (sis: sistate): Prop := {
-  OK_PRE: (sis.(si_pre) ctx);
-  OK_SMEM: eval_smem ctx sis.(si_smem) <> None;
-  OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None
-}.
 Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core.
-Local Hint Constructors sis_ok: core.
-
-Lemma sem_sok ctx sis rs m:
-  sem_sistate ctx sis rs m ->  sis_ok ctx sis.
-Proof.
-  unfold sem_sistate;
-  econstructor;
-  intuition congruence.
-Qed.
+Local Hint Constructors si_ok: core.
 
 (* NB: refinement of (symbolic) internal state *)
 Record ristate := 
@@ -65,7 +52,7 @@ Local Hint Resolve OK_RMEM OK_RREG: core.
 Local Hint Constructors ris_ok: core.
 
 Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := {
-  OK_EQUIV: sis_ok ctx sis <-> ris_ok ctx ris;
+  OK_EQUIV: si_ok ctx sis <-> ris_ok ctx ris;
   MEM_EQ: ris_ok ctx ris ->  eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem);
   REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r)
 }.
@@ -97,7 +84,7 @@ Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2:
   sistate_simu ctx sis1 sis2.
 Proof.
   intros RIS REF1 REF2 rs m SEM.
-  exploit sem_sok; eauto.
+  exploit sem_si_ok; eauto.
   erewrite OK_EQUIV; eauto.
   intros ROK1.
   exploit ris_simu_ok_preserv; eauto.
@@ -238,7 +225,7 @@ Proof.
   inv REF1; inv REF2; simpl in *; inv SEM1; auto.
   - (* final_simu *) 
     do 2 eexists; intuition; eauto.
-    exploit sem_sok; eauto.
+    exploit sem_si_ok; eauto.
     erewrite OK_EQUIV; eauto.
     intros ROK1.
     exploit ris_simu_ok_preserv; eauto.
@@ -249,8 +236,8 @@ Proof.
     intros SCOND0; rewrite <- SCOND0 in RCOND0.
     erewrite <- SCOND0.
     destruct b; simpl.
-    * exploit IHrst_simu1; eauto.
-    * exploit IHrst_simu2; eauto.
+    * intros; exploit IHrst_simu1; eauto.
+    * intros; exploit IHrst_simu2; eauto.
 Qed.
 
 (** * Refinement of the symbolic execution *)
@@ -321,8 +308,8 @@ Definition rset_smem rm (ris:ristate): ristate :=
   |}.
 
 Lemma ok_set_mem ctx sm sis:
-  sis_ok ctx (set_smem sm sis)
-  <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None).
+  si_ok ctx (set_smem sm sis)
+  <-> (si_ok ctx sis /\ eval_smem ctx sm <> None).
 Proof.
   split; destruct 1; econstructor; simpl in *; eauto.
   intuition eauto.
@@ -374,8 +361,8 @@ Definition rset_sreg r rsv (ris:ristate): ristate :=
   |}.
 
 Lemma ok_set_sreg ctx r sv sis:
-  sis_ok ctx (set_sreg r sv sis)
-  <-> (sis_ok ctx sis /\ eval_sval ctx sv <> None).
+  si_ok ctx (set_sreg r sv sis)
+  <-> (si_ok ctx sis /\ eval_sval ctx sv <> None).
 Proof.
   unfold set_sreg; split.
   + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split.
@@ -493,8 +480,8 @@ Definition transfer_sis (inputs: list reg) (sis:sistate): sistate :=
       si_smem := sis.(si_smem) |}.
 
 Lemma ok_transfer_sis ctx inputs sis:
-  sis_ok ctx (transfer_sis inputs sis)
-  <-> (sis_ok ctx sis).
+  si_ok ctx (transfer_sis inputs sis)
+  <-> (si_ok ctx sis).
 Proof.
   unfold transfer_sis. induction inputs as [|r l]; simpl.
   + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence.
@@ -626,10 +613,10 @@ Qed.
 
 Lemma history_nested ctx ib:
   forall k
-  (CONT: forall sis hsis, (k sis) = Some hsis -> nested (sis_ok ctx sis) (List.map (sis_ok ctx) hsis))
+  (CONT: forall sis hsis, (k sis) = Some hsis -> nested (si_ok ctx sis) (List.map (si_ok ctx) hsis))
   sis hsis 
   (RET: history ctx ib sis k = Some hsis),
-  nested (sis_ok ctx sis) (List.map (sis_ok ctx) hsis).
+  nested (si_ok ctx sis) (List.map (si_ok ctx) hsis).
 Proof.
   induction ib; simpl; intros; try_simplify_someHyps.
   + econstructor; eauto. admit.
@@ -721,7 +708,7 @@ Qed.
 (* TODO:  bof, "historys_spec" un peu lourd pour l'usage qui en est fait ? *)
 Inductive history_spec ctx sis1 sis2: option (list sistate) -> Prop :=
   history_exist hsis 
-    (NESTED: nested (sis_ok ctx sis1) (List.map (sis_ok ctx) hsis))
+    (NESTED: nested (si_ok ctx sis1) (List.map (si_ok ctx) hsis))
     (LAST: is_last sis2 hsis)
     : history_spec ctx sis1 sis2 (Some hsis)
   .
@@ -770,12 +757,12 @@ Local Hint Constructors rst_refines: core.
 
 Lemma rexec_rec_correct ctx ib: 
   forall kok rk k
-  (CONT: forall ris sis hsis st, ris_refines ctx ris sis -> k sis = st -> kok sis = Some hsis -> (forall sis, List.In sis hsis -> sis_ok ctx sis) -> rst_refines ctx (rk ris) (k sis))
+  (CONT: forall ris sis hsis st, ris_refines ctx ris sis -> k sis = st -> kok sis = Some hsis -> (forall sis, List.In sis hsis -> si_ok ctx sis) -> rst_refines ctx (rk ris) (k sis))
   ris sis hsis st
   (REF: ris_refines ctx ris sis)
   (EXEC: sexec_rec (cf ctx) ib sis k = st)
   (OK1: history ctx ib sis kok = Some hsis)
-  (OK2: forall sis, List.In sis hsis -> sis_ok ctx sis)
+  (OK2: forall sis, List.In sis hsis -> si_ok ctx sis)
   , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st.
 Proof.
   induction ib; simpl; try (intros; subst; eauto; fail).
@@ -802,7 +789,7 @@ Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort).
 
 Lemma rexec_correct ctx ib sis sfv:
   run_sem_isstate ctx (sexec (cf ctx) ib) = Some (sout sis sfv) ->
-  (sis_ok ctx sis) ->
+  (si_ok ctx sis) ->
   rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib).
 Proof.
   intros RUN SIS; exploit run_sem_history; eauto.