From a3f8b6fc7931e73ca005644124597ff6656cbce7 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 8 Jun 2021 14:37:02 +0200 Subject: generalize nested --- scheduling/BTL_SEsimuref.v | 145 +++++++++++++++++++++++---------------------- 1 file changed, 74 insertions(+), 71 deletions(-) (limited to 'scheduling/BTL_SEsimuref.v') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 4f472e3e..5098659d 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -660,16 +660,15 @@ Fixpoint history ctx ib sis (k:sistate -> option (list sistate)): option (list s end . -Inductive nested ctx: sistate -> list sistate -> Type := - ns_nil sis: nested ctx sis nil -| ns_cons sis1 sis2 lsis: - (sis_ok ctx sis2 -> sis_ok ctx sis1) -> - nested ctx sis2 lsis -> - nested ctx sis1 (sis2::lsis) +Inductive nested: Prop -> list Prop -> Type := + ns_nil ok: nested ok nil +| ns_cons (ok1 ok2: Prop) loks: + (ok2 -> ok1) -> + nested ok2 loks -> + nested ok1 (ok2::loks) . Local Hint Constructors nested: core. -(* TODO: A REVOIR ! Lemma nested_monotonic ok1 oks: nested ok1 oks -> forall (ok2: Prop), (ok1 -> ok2) -> @@ -680,10 +679,10 @@ Qed. Lemma history_nested ctx ib: forall k - (CONT: forall sis hsis, (k sis) = Some hsis -> nested (sis_ok ctx sis) hsis) + (CONT: forall sis hsis, (k sis) = Some hsis -> nested (sis_ok ctx sis) (List.map (sis_ok ctx) hsis)) sis hsis (RET: history ctx ib sis k = Some hsis), - nested (sis_ok ctx sis) hsis. + nested (sis_ok ctx sis) (List.map (sis_ok ctx) hsis). Proof. induction ib; simpl; intros; try_simplify_someHyps. + econstructor; eauto. admit. @@ -727,75 +726,73 @@ Proof. * eapply nested_last_1; eauto. * eapply IHLAST; eauto. Qed. + Local Hint Constructors is_last: core. -Lemma run_sem_isstate_okcnd_last ctx ib: forall ks kok - (CONT: forall sis1 sis2 sfv, run_sem_isstate ctx (ks sis1) = Some (sout sis2 sfv) -> exists hsis, kok sis1 = Some hsis /\ is_last (sis_ok ctx sis2) hsis) - sis1 sis2 sfv +Lemma is_last_map {A B} (f: A -> B) x l: is_last x l -> is_last (f x) (List.map f l). +Proof. + induction 1; simpl; eauto. +Qed. + +Lemma run_sem_is_last ctx ib: forall ks kok + (CONT: forall sis1 sis2 sfv hsis, run_sem_isstate ctx (ks sis1) = Some (sout sis2 sfv) -> kok sis1 = Some hsis -> is_last sis2 hsis) + sis1 sis2 sfv hsis (RUN: run_sem_isstate ctx (sexec_rec (cf ctx) ib sis1 ks) = Some (sout sis2 sfv)) - ,exists hsis, history ctx ib sis1 kok = Some hsis /\ is_last (sis_ok ctx sis2) hsis. + (HIST: history ctx ib sis1 kok = Some hsis) + ,is_last sis2 hsis. Proof. induction ib; simpl; intros; try_simplify_someHyps. + destruct trap; simpl; try_simplify_someHyps. + (* seq *) - intros; eapply IHib1; eauto. + intros; eapply IHib1. 2-3: eauto. simpl; intros; eapply IHib2; eauto. + (* cond *) - autodestruct. intros; destruct b. - - exploit IHib1; eauto. - intros (hsis & OK & LAST). - rewrite OK; simpl. - eexists; split; eauto. - - exploit IHib2; eauto. - intros (hsis & OK & LAST). - rewrite OK; simpl. - eexists; split; eauto. + autodestruct. + destruct (history _ _ _ _) eqn: HIST; try_simplify_someHyps. + intros; econstructor. + destruct b; eauto. Qed. -*) - -Inductive histOK ctx: list sistate -> sstate -> Prop := - | Final_ok sis sfv - : histOK ctx (sis::nil) (Sfinal sis sfv) - | Cond_ok b sis hsis cond args ifso ifnot - (OK: (sis_ok ctx sis)) - (EVAL: seval_condition ctx cond args sis.(si_smem) = Some b) - (REC: histOK ctx hsis (if b then ifso else ifnot)) - : histOK ctx (sis::hsis) (Scond cond args sis.(si_smem) ifso ifnot) - . -Local Hint Constructors histOK: core. -(* TODO: pour prouver ça, faut généraliser avec nested + is_last en hypothèse ? - -Lemma run_sem_isstate_okentails ctx ib: forall ks kok - (CONT: forall sis st, ks sis = st -> run_sem_isstate ctx st <> None -> exists hsis, kok sis = Some hsis /\ histOK ctx hsis st) - sis st - (EXEC: sexec_rec (cf ctx) ib sis ks = st) - (OK: run_sem_isstate ctx st <> None) - ,exists hsis, history ctx ib sis kok = Some hsis /\ histOK ctx hsis st. +Lemma run_sem_history_None ctx ib: forall ks kok + (CONT: forall sis, kok sis = None -> run_sem_isstate ctx (ks sis) = None) + sis + (HIST: history ctx ib sis kok = None) + ,run_sem_isstate ctx (sexec_rec (cf ctx) ib sis ks) = None. Proof. - induction ib; simpl; intros; subst; try_simplify_someHyps. - + destruct trap; simpl in *; try_simplify_someHyps. congruence. + induction ib; simpl; intros; try_simplify_someHyps. + + destruct trap; simpl in *; try_simplify_someHyps. + (* seq *) - intros; eapply IHib1; eauto. + intros; eapply IHib1. 2: eauto. simpl; intros; eapply IHib2; eauto. + (* cond *) simpl in *. autodestruct. - intros; destruct b. - - exploit IHib1; eauto. - intros (hsis & OK1 & X). - rewrite OK1; simpl. - eexists; split; eauto. - econstructor; eauto. - admit. - - exploit IHib2; eauto. - intros (hsis & OK2 & LAST). - rewrite OK2; simpl. - eexists; split; eauto. - econstructor; eauto. - admit. -Admitted. -*) + destruct (history _ _ _ _) eqn: X; try congruence. + intros; destruct b; eauto. +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)) + (LAST: is_last sis2 hsis) + : history_spec ctx sis1 sis2 (Some hsis) + . +Local Hint Resolve history_exist: core. + +Lemma run_sem_history ctx ib sis svf + (OK: run_sem_isstate ctx (sexec (cf ctx) ib) = Some (sout sis svf)) + :history_spec ctx sis_init sis (history ctx ib sis_init (fun _ => None)). +Proof. + unfold sexec in *; destruct (history _ _ _ _) eqn: HIST. + + econstructor. + * eapply history_nested; eauto. + simpl; try congruence. + * eapply run_sem_is_last. 2-3: eauto. + simpl; try congruence. + + exploit (run_sem_history_None ctx ib (fun _ => Sabort)); eauto. + congruence. +Qed. (** RAFFINEMENT EXEC SYMBOLIQUE **) @@ -826,12 +823,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 -> histOK ctx hsis st -> 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 -> sis_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: histOK ctx hsis st) + (OK2: forall sis, List.In sis hsis -> sis_ok ctx sis) , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st. Proof. induction ib; simpl; try (intros; subst; eauto; fail). @@ -843,13 +840,12 @@ Proof. - (* cond *) intros rk k kok CONT ris sis hsis st REF EXEC. subst. autodestruct. - intros EQb. + intros COND. destruct (history _ _ _ _) eqn: EQl; intros; try_simplify_someHyps; intros. - inv OK2. + exploit (OK2 sis); auto. assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV; eauto. } - try_simplify_someHyps; intros. - generalize EVAL. + generalize COND. erewrite seval_condition_valid_preserv, <- seval_condition_refpreserv; eauto. intros; econstructor; try_simplify_someHyps. @@ -857,11 +853,18 @@ Qed. Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort). -Lemma rexec_correct ctx ib hsis: - history ctx ib sis_init (fun _ : sistate => None) = Some hsis -> - histOK ctx hsis (sexec_rec (cf ctx) ib sis_init (fun _ : sistate => Sabort)) -> +Lemma rexec_correct ctx ib sis sfv: + run_sem_isstate ctx (sexec (cf ctx) ib) = Some (sout sis sfv) -> + (sis_ok ctx sis) -> rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). Proof. + intros RUN SIS; exploit run_sem_history; eauto. + intros HIST; inv HIST. unfold sexec; intros; eapply rexec_rec_correct; eauto. - simpl; congruence. + + simpl; intros; subst; eauto. + + intros; eapply nested_last_all. + - eapply is_last_map; eauto. + - eapply NESTED. + - eapply SIS. + - eapply List.in_map; eauto. Qed. -- cgit