From 0d856574d11ccccab397e007d43437980e07aeac Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 3 Jun 2021 08:31:20 +0200 Subject: progress in BTL_SEsimuref --- scheduling/BTL_SEsimuref.v | 136 +++++++++++++++++++-------------------------- 1 file changed, 58 insertions(+), 78 deletions(-) (limited to 'scheduling/BTL_SEsimuref.v') 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 -- cgit