From 485a4c0dd450e65745c83e59acdb40b42058e556 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 10 Jun 2021 13:43:14 +0200 Subject: theorem rexec_simu_correct --- scheduling/BTL_SEsimuref.v | 136 ++++++++++++++++++++++++++++++++++++--------- 1 file changed, 111 insertions(+), 25 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index f39da275..852bced0 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -619,7 +619,7 @@ Proof. destruct fi; simpl; eauto. Qed. -Lemma si_ok_tr_sis_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis. +Lemma si_ok_tr_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis. Admitted. Lemma si_ok_op_down ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis. @@ -632,7 +632,26 @@ Lemma si_ok_store_down ctx chunk addr args src sis: si_ok ctx (sexec_store chunk Admitted. (* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *) -Local Hint Resolve si_ok_tr_sis_down si_ok_op_down si_ok_trap_down si_ok_store_down: core. +Local Hint Resolve si_ok_tr_down si_ok_op_down si_ok_trap_down si_ok_store_down: core. + +Lemma sexec_rec_down ctx ib: + forall k + (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) + sis lsis sfv + (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv)) + (OK: si_ok ctx lsis) + ,si_ok ctx sis. +Proof. + induction ib; simpl; try (autodestruct; simpl). + 1-6: try_simplify_someHyps. + - intros. eapply IHib1. 2-3: eauto. + eapply IHib2; eauto. + - intros k CONT sis lsis sfv. + do 2 autodestruct. + + intros; eapply IHib1; eauto. + + intros; eapply IHib2; eauto. +Qed. + (** RAFFINEMENT EXEC SYMBOLIQUE **) @@ -656,30 +675,15 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := end . +Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort). + + Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_ris_imp rexec_op_correct rexec_load_correct rexec_store_correct: core. Local Hint Constructors rst_refines: core. -Lemma sexec_rec_down ctx ib: - forall k - (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) - sis lsis sfv - (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv)) - (OK: si_ok ctx lsis) - ,si_ok ctx sis. -Proof. - induction ib; simpl; try (autodestruct; simpl). - 1-6: try_simplify_someHyps. - - intros. eapply IHib1. 2-3: eauto. - eapply IHib2; eauto. - - intros k CONT sis lsis sfv. - do 2 autodestruct. - + intros; eapply IHib1; eauto. - + intros; eapply IHib2; eauto. -Qed. - -Lemma rexec_rec_correct ctx ib: +Lemma rexec_rec_correct1 ctx ib: forall rk k (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) (CONT: forall ris sis lsis sfv st, ris_refines ctx ris sis -> k sis = st -> get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> rst_refines ctx (rk ris) (k sis)) @@ -710,12 +714,94 @@ Proof. econstructor; try_simplify_someHyps. Qed. -Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort). - -Lemma rexec_correct ctx ib sis sfv: +Lemma rexec_correct1 ctx ib sis sfv: get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) -> (si_ok ctx sis) -> rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). Proof. - unfold sexec; intros; eapply rexec_rec_correct; eauto; simpl; congruence. + unfold sexec; intros; eapply rexec_rec_correct1; eauto; simpl; congruence. +Qed. + + +(** COPIER-COLLER ... Y a-t-il moyen de l'eviter ? **) + +Lemma ris_ok_tr_down ctx fi ris: ris_ok ctx (tr_ris (cf ctx) fi ris) -> ris_ok ctx ris. +Admitted. + +Lemma ris_ok_op_down ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris. +Admitted. + +Lemma ris_ok_trap_down ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris. +Admitted. + +Lemma ris_ok_store_down ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris. +Admitted. + +(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *) +Local Hint Resolve ris_ok_tr_down ris_ok_op_down ris_ok_trap_down ris_ok_store_down: core. + +Lemma rexec_rec_down ctx ib: + forall k + (CONT: forall ris lris rfv, get_routcome ctx (k ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) + ris lris rfv + (ROUT: get_routcome ctx (rexec_rec (cf ctx) ib ris k) = Some (rout lris rfv)) + (OK: ris_ok ctx lris) + ,ris_ok ctx ris. +Proof. + induction ib; simpl; try (autodestruct; simpl). + 1-6: try_simplify_someHyps. + - intros. eapply IHib1. 2-3: eauto. + eapply IHib2; eauto. + - intros k CONT sis lsis sfv. + do 2 autodestruct. + + intros; eapply IHib1; eauto. + + intros; eapply IHib2; eauto. +Qed. + +Lemma rexec_rec_correct2 ctx ib: + forall rk k + (CONTh: forall ris lris rfv, get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) + (CONT: forall ris sis lris rfv st, ris_refines ctx ris sis -> rk ris = st -> get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> rst_refines ctx (rk ris) (k sis)) + ris sis lris rfv st + (REF: ris_refines ctx ris sis) + (EXEC: rexec_rec (cf ctx) ib ris rk = st) + (SOUT: get_routcome ctx st = Some (rout lris rfv)) + (OK: ris_ok ctx lris) + , rst_refines ctx st (sexec_rec (cf ctx) ib sis k). +Proof. + induction ib; simpl; try (intros; subst; eauto; fail). + - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. + - (* seq *) + intros; subst. + eapply IHib1. 3-6: eauto. + + simpl. eapply rexec_rec_down; eauto. + + intros; subst. eapply IHib2; eauto. + - (* cond *) + intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst. + assert (OK0: ris_ok ctx ris). { + eapply rexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + } + generalize OUT; clear OUT; simpl. + autodestruct. + intros COND; generalize COND. + erewrite seval_condition_refpreserv; eauto. + econstructor; try_simplify_someHyps. +Qed. + +Lemma rexec_correct2 ctx ib ris rfv: + get_routcome ctx (rexec (cf ctx) ib) = Some (rout ris rfv) -> + (ris_ok ctx ris) -> + rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). +Proof. + unfold rexec; intros; eapply rexec_rec_correct2; eauto; simpl; congruence. +Qed. + +Theorem rexec_simu_correct f1 f2 ib1 ib2: + rst_simu (rexec f1 ib1) (rexec f2 ib2) -> + symbolic_simu f1 f2 ib1 ib2. +Proof. + intros SIMU ctx. + eapply rst_simu_correct; eauto. + + intros; eapply rexec_correct1; eauto. + + intros; eapply rexec_correct2; eauto. Qed. -- cgit