progress in BTL_SEsimuref

1 files changed, 58 insertions, 78 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index e9ae11e0..c322a9a5 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -89,14 +89,13 @@ Proof.
   - intros; erewrite <- eval_sval_preserved; eauto.
 Qed.
 
-Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 rs m: 
+Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2: 
   ris_simu ris1 ris2 ->
   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.
+  sistate_simu ctx sis1 sis2.
 Proof.
-  intros RIS REF1 REF2 SEM.
+  intros RIS REF1 REF2 rs m SEM.
   exploit sem_sok; eauto.
   erewrite OK_EQUIV; eauto.
   intros ROK1.
@@ -113,62 +112,76 @@ Proof.
     erewrite REG_EQ; eauto.
 Qed.
 
-(* TODO:
-
-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.
+Inductive optrsv_refines ctx: (option sval) -> (option sval) -> Prop :=
+  | RefSome rsv sv
+     (REF:eval_sval ctx rsv = eval_sval ctx sv)
+     :optrsv_refines ctx (Some rsv) (Some sv)
+  | RefNone: optrsv_refines ctx None None
+  .
 
-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.
+Inductive rsvident_refines ctx: (sval + ident) -> (sval + ident) -> Prop :=
+  | RefLeft rsv sv
+     (REF:eval_sval ctx rsv = eval_sval ctx sv)
+     :rsvident_refines ctx (inl rsv) (inl sv)
+  | RefRight id1 id2
+     (IDSIMU: id1 = id2)
+     :rsvident_refines ctx (inr id1) (inr id2)
+  .
 
 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)
+  | RefGoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc)
+  | RefCall sig rvos ros rargs args r pc
+      (SV:rsvident_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)
+      :rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc)
+  | RefTailcall sig rvos ros rargs args
+      (SV:rsvident_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
+      :rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args)
+  | RefBuiltin 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
+      :rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc)
+  | RefJumptable 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)
+      :rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc)
+  | RefReturn orsv osv
+      (OPT:optrsv_refines ctx orsv osv)
+      :rfv_refines ctx (Sreturn orsv) (Sreturn osv)
 .
 
 Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2.
 
-Local Hint Constructors sem_sfval equiv_state: core.
+Local Hint Resolve eval_sval_preserved list_sval_eval_preserved smem_eval_preserved eval_list_builtin_sval_preserved: core.
 
-Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2 rs m t s: 
+Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2: 
   rfv_simu rfv1 rfv2 ->
   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'.
+  sfv_simu ctx sfv1 sfv2.
 Proof.
-  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.
+  unfold rfv_simu; intros X REF1 REF2. subst.
+  unfold bctx2; destruct REF1; inv REF2; simpl; econstructor; eauto.
+  - (* call svid *)
+    inv SV; inv SV0; econstructor; eauto.
+    rewrite <- REF, <- REF0; eauto.
+  - (* call args *)
+    rewrite <- LIST, <- LIST0; eauto.
+  - (* taillcall svid *)
+    inv SV; inv SV0; econstructor; eauto.
+    rewrite <- REF, <- REF0; eauto.
+  - (* tailcall args *)
+    rewrite <- LIST, <- LIST0; eauto.
+  - (* builtin args *)
+    unfold bargs_refines, bargs_simu in *.
+    rewrite <- BARGS, <- BARGS0; eauto.
+  - rewrite <- VAL, <- VAL0; eauto.
+  - (* return *)
+    inv OPT; inv OPT0; econstructor; eauto.
+    rewrite <- REF, <- REF0; eauto.
+Qed.
 
 (* refinement of (symbolic) state *)
 Inductive rstate :=
@@ -197,18 +210,18 @@ Inductive rst_simu: rstate -> rstate -> Prop :=
 
 (* Comment prend on en compte le ris en cours d'execution ??? *)
 Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
-  | refines_Sfinal ris sis rfv sfv (*ok: Prop*)
+  | Reffinal ris sis rfv sfv (*ok: Prop*)
       (*OK: ris_ok ctx ris -> ok*)
       (RIS: ris_refines ctx ris sis)
       (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv)
       : rst_refines ctx (*ok*) (Rfinal ris rfv) (Sfinal sis sfv)
-  | refines_Scond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*)
+  | Refcond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*)
       (*OK1: ok2 -> ok1*)
       (RCOND: (* ok2 -> *) seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm)
       (REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx (*ok2*) rifso ifso)
       (REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx (*ok2*) rifnot ifnot)
       : rst_refines ctx (*ok1*) (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot)
-  | refines_Sabort
+  | Refabort
       : rst_refines ctx Rabort Sabort
   .
 
@@ -223,37 +236,4 @@ Proof.
   induction 1; simpl; auto.
   - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
     inv REF1. inv REF2. inv SEM1.
-    exploit sem_sok; eauto.
-    rewrite OK_EQUIV; eauto.
-    intros RIS_OK1.
-    exploit (ris_simu_ok_preserv f1 f2); eauto.
-    intros RIS_OK2. intuition.
-    exploit ris_simu_correct; eauto.
-    exploit rvf_simu_correct; eauto.
-    simpl. (*
-    eexists; split.
-    + econstructor; eauto.
-      simpl.
-      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 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 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.
-*)
\ No newline at end of file
+Admitted.
\ No newline at end of file