the current "high-level" specification of the simulation test will not work !

1 files changed, 68 insertions, 26 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index af2159cb..65052310 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -182,8 +182,8 @@ Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core.
 Local Hint Constructors ris_simu: core.
 Local Hint Resolve sge_match: core.
 
-Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context):
-  ris_simu ris1 ris2 -> ris_ok (bctx1 f1 ctx) ris1 -> ris_ok (bctx2 f2 ctx) ris2.
+Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2):
+  ris_simu ris1 ris2 -> ris_ok (bctx1 ctx) ris1 -> ris_ok (bctx2 ctx) ris2.
 Proof.
   intros SIMU OK; econstructor; eauto.
   - erewrite <- SIMU_MEM; eauto.
@@ -191,12 +191,12 @@ Proof.
   - unfold bctx2; intros; erewrite eval_sval_preserved; eauto.
 Qed.
 
-Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context) sis1 sis2 rs m: 
+Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 rs m: 
   ris_simu ris1 ris2 ->
-  ris_refines (bctx1 f1 ctx) ris1 sis1 ->
-  ris_refines (bctx2 f2 ctx) ris2 sis2 ->
-  sem_sistate (bctx1 f1 ctx) sis1 rs m ->
-  sem_sistate (bctx2 f2 ctx) sis2 rs m.
+  ris_refines (bctx1 ctx) ris1 sis1 ->
+  ris_refines (bctx2 ctx) ris2 sis2 ->
+  sem_sistate (bctx1 ctx) sis1 rs m ->
+  sem_sistate (bctx2 ctx) sis2 rs m.
 Proof.
   intros RIS REF1 REF2 SEM.
   (* destruct REF1. destruct REF2. *)
@@ -216,21 +216,59 @@ Proof.
     erewrite REG_EQ; eauto.
 Qed.
 
-Definition rfv_refines ctx (rfv sfv: sfval): Prop :=
-  forall rs m t s, sem_sfval ctx rfv rs m t s <-> sem_sfval ctx sfv rs m t s.
+Definition option_refines ctx (orsv: option sval) (osv: option sval) :=
+  match orsv, osv with
+  | Some rsv, Some sv => eval_sval ctx rsv = eval_sval ctx sv
+  | None, None => True
+  | _, _ => False
+  end.
+
+Definition sum_refines ctx (rsi: sval + ident) (si: sval + ident) :=
+  match rsi, si with
+  | inl rsv, inl sv => eval_sval ctx rsv = eval_sval ctx sv
+  | inr id, inr id' => id = id'
+  | _, _ => False
+  end.
+
+Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop :=
+  eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args.
+
+Inductive rfv_refines ctx: sfval -> sfval -> Prop :=
+  | refines_Sgoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc)
+  | refines_Scall: forall sig rvos ros rargs args r pc
+      (SUM:sum_refines ctx rvos ros)
+      (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
+      ,rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc)
+  | refines_Stailcall: forall sig rvos ros rargs args
+      (SUM:sum_refines ctx rvos ros)
+      (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
+      ,rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args)
+  | refines_Sbuiltin: forall ef lbra lba br pc
+      (BARGS: bargs_refines ctx lbra lba)
+      ,rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc)
+  | refines_Sjumptable: forall rsv sv lpc
+      (VAL: eval_sval ctx rsv = eval_sval ctx sv)
+      ,rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc)
+  | refines_Sreturn: forall orsv osv
+      (OPT:option_refines ctx orsv osv)
+      ,rfv_refines ctx (Sreturn orsv) (Sreturn osv)
+.
 
 Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2.
 
-Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context) sfv1 sfv2 rs m t s: 
+Local Hint Constructors sem_sfval equiv_state: core.
+
+Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2 rs m t s: 
   rfv_simu rfv1 rfv2 ->
-  rfv_refines (bctx1 f1 ctx) rfv1 sfv1 ->
-  rfv_refines (bctx2 f2 ctx) rfv2 sfv2 ->
-  sem_sfval (bctx1 f1 ctx) sfv1 rs m t s ->
-  sem_sfval (bctx2 f2 ctx) sfv2 rs m t s.
+  rfv_refines (bctx1 ctx) rfv1 sfv1 ->
+  rfv_refines (bctx2 ctx) rfv2 sfv2 ->
+  sem_sfval (bctx1 ctx) sfv1 rs m t s ->
+  exists s', sem_sfval (bctx2 ctx) sfv2 rs m t s' /\ equiv_state s s'.
 Proof.
-  unfold rfv_simu, rfv_refines; intros X REF1 REF2 SEM. subst.
-  rewrite <- REF2.
-  assert (sem_sfval (bctx1 f1 ctx) rfv2 rs m t s). { rewrite REF1; auto. }
+  unfold rfv_simu; intros X REF1 REF2 SEM. subst.
+  unfold bctx2; destruct REF1; inv REF2; inv SEM; simpl.
+  - eexists; split; eauto; simpl.
+    (* eapply State_equiv; eauto. NE MARCHE PAS ! *)
 Admitted.
 
 (* refinement of (symbolic) state *)
@@ -277,11 +315,11 @@ Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
 
 Lemma rst_simu_correct rst1 rst2:
    rst_simu rst1 rst2 ->
-   forall f1 f2 ctx st1 st2 (*ok1 ok2*),
-   rst_refines (*ok1*) (bctx1 f1 ctx) rst1 st1 ->
-   rst_refines (*ok2*) (bctx2 f2 ctx) rst2 st2 ->
+   forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*),
+   rst_refines (*ok1*) (bctx1 ctx) rst1 st1 ->
+   rst_refines (*ok2*) (bctx2 ctx) rst2 st2 ->
    (* ok1 -> ok2 -> *)
-   sstate_simu f1 f2 ctx st1 st2.
+   sstate_simu ctx st1 st2.
 Proof.
   induction 1; simpl; auto.
   - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
@@ -293,25 +331,29 @@ Proof.
     intros RIS_OK2. intuition.
     exploit ris_simu_correct; eauto.
     exploit rvf_simu_correct; eauto.
-    simpl.
+    simpl. (*
     eexists; split.
     + econstructor; eauto.
       simpl.
-      admit. (* TODO: condition sur les tr_inputs: à ajouter plutôt dans le simu_proof_context ! *)
+      clear SIS.
+      admit. (* TODO: condition sur les tr_inputs du simu_proof_context ! *)
+      (* TODO: le rfv_refines est trop sémantique ! *)
     + admit.
   - (* cond *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
     inv REF1. inv REF2. inv SEM1.
     destruct b; simpl.
-    + assert (TODO1: rst_refines (bctx1 f1 ctx) rifso1 ifso). admit.
-      assert (TODO2: rst_refines (bctx2 f2 ctx) rifso2 ifso0). admit.
+    + assert (TODO1: rst_refines (bctx1 ctx) rifso1 ifso). admit.
+      assert (TODO2: rst_refines (bctx2 ctx) rifso2 ifso0). admit.
       exploit IHrst_simu1; eauto.
       intros (s2 & X1 & X2).
       exists s2; split; eauto.
       econstructor; eauto.
-      * assert (TODO3: seval_condition (bctx2 f2 ctx) cond args0 sm0 = Some true). admit.
+      * assert (TODO3: seval_condition (bctx2 ctx) cond args0 sm0 = Some true). admit.
         eauto.
       * simpl; eauto.
    + admit.
   - (* abort *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
     inv REF1. inv SEM1.
+*)
+
 Admitted.