From a7bb27d5125fd2232fa38fe9605c31766a96fa2e Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 8 Jun 2021 02:23:24 +0200 Subject: preuve de rexec_rec_correct via les notions history/histOK --- scheduling/BTL_SEsimuref.v | 292 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 251 insertions(+), 41 deletions(-) (limited to 'scheduling/BTL_SEsimuref.v') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index fdefe205..4f472e3e 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -212,18 +212,17 @@ 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 := - | Reffinal ris sis rfv sfv (*ok: Prop*) - (*OK: ris_ok ctx ris -> ok*) + +Inductive rst_refines ctx: rstate -> sstate -> Prop := + | Reffinal ris sis rfv sfv (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) - | 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) + : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv) + | Refcond cond rargs args sm rifso rifnot ifso ifnot + (RCOND: seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm) + (REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx rifso ifso) + (REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx rifnot ifnot) + : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot) | Refabort : rst_refines ctx Rabort Sabort . @@ -232,10 +231,9 @@ Local Hint Resolve ris_simu_correct rvf_simu_correct: core. Lemma rst_simu_correct rst1 rst2: rst_simu rst1 rst2 -> - 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 -> *) + forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2, + rst_refines (bctx1 ctx) rst1 st1 -> + rst_refines (bctx2 ctx) rst2 st2 -> sstate_simu ctx st1 st2. Proof. induction 1; simpl; intros f1 f2 ctx st1 st2 REF1 REF2 sis1 svf1 SEM1; @@ -257,6 +255,34 @@ Proof. * exploit IHrst_simu2; eauto. Qed. + +(* TODO: useless ? +Record routcome := rout { + r_sis: ristate; + r_sfv: sfval; +}. + +Local Open Scope option_monad_scope. + +Fixpoint run_sem_irstate ctx (rst:rstate): option routcome := + match rst with + | Rfinal ris sfv => Some (rout ris sfv) + | Rcond cond args ifso ifnot => + SOME b <- seval_condition ctx cond args Sinit IN + run_sem_irstate ctx (if b then ifso else ifnot) + | Rabort => None + end. + +(* Non: pas assez de "matching" syntaxique entre rst et st pour rst_simu_correct +Definition rst_refines ctx rst st:= + (run_sem_isstate ctx st=None <-> run_sem_irstate ctx rst=None) + /\ (forall ris rfv sis sfv, run_sem_irstate ctx rst = Some (rout ris rfv) -> run_sem_isstate ctx st = Some (sout sis sfv) -> + (ris_refines ctx ris sis) /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv)). + +*) +*) + + (** * Refinement of the symbolic execution *) Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core. @@ -582,29 +608,197 @@ Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre Local Hint Resolve transfer_ris_correct ok_transfer_ris: core. Local Opaque transfer_ris. -Lemma ok_tr_ris ctx f fi ris: - ris_ok ctx (tr_ris f fi ris) +Lemma ok_tr_ris ctx fi ris: + ris_ok ctx (tr_ris (cf ctx) fi ris) <-> (ris_ok ctx ris). Proof. destruct fi; simpl; eauto. Qed. -Lemma ok_tr_ris_imp ctx f fi ris: - ris_ok ctx (tr_ris f fi ris) +Lemma ok_tr_ris_imp ctx fi ris: + ris_ok ctx (tr_ris (cf ctx) fi ris) -> (ris_ok ctx ris). Proof. rewrite ok_tr_ris; auto. Qed. -Lemma tr_ris_correct ctx f fi ris sis: +Lemma tr_ris_correct ctx fi ris sis: ris_refines ctx ris sis -> - ris_refines ctx (tr_ris f fi ris) (tr_sis f fi sis). + ris_refines ctx (tr_ris (cf ctx) fi ris) (tr_sis (cf ctx) fi sis). Proof. intros REF. rewrite <- tr_sis_alt_def. destruct fi; simpl; eauto. Qed. +(** TODO: CHANTIER **) + +Local Open Scope option_monad_scope. + +(* TODO: est-ce qu'un type inductif serait plus simple ? Pas sûr à cause des raisonnements par continuation ? + +Un avantage du fixpoint, c'est que ça pourrait permettre de prouver les propriétés de history de façon plus incrémentale/modulaire. +*) + +Fixpoint history ctx ib sis (k:sistate -> option (list sistate)): option (list sistate) := + match ib with + | BF fin _ => Some (tr_sis (cf ctx) fin sis::nil) + (* basic instructions *) + | Bnop _ => k sis + | Bop op args res _ => k (sexec_op op args res sis) + | Bload TRAP chunk addr args dst _ => k (sexec_load TRAP chunk addr args dst sis) + | Bload NOTRAP chunk addr args dst _ => None + | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis) + (* composed instructions *) + | Bseq ib1 ib2 => + history ctx ib1 sis (fun sis2 => history ctx ib2 sis2 k) + | Bcond cond args ifso ifnot _ => + let args := list_sval_inj (List.map sis args) in + SOME b <- seval_condition ctx cond args sis.(si_smem) IN + SOME oks <- history ctx (if b then ifso else ifnot) sis k IN + Some (sis::oks) + 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) + . +Local Hint Constructors nested: core. + +(* TODO: A REVOIR ! +Lemma nested_monotonic ok1 oks: + nested ok1 oks -> + forall (ok2: Prop), (ok1 -> ok2) -> + nested ok2 oks. +Proof. + induction 1; simpl; eauto. +Qed. + +Lemma history_nested ctx ib: + forall k + (CONT: forall sis hsis, (k sis) = Some hsis -> nested (sis_ok ctx sis) hsis) + sis hsis + (RET: history ctx ib sis k = Some hsis), + nested (sis_ok ctx sis) hsis. +Proof. + induction ib; simpl; intros; try_simplify_someHyps. + + econstructor; eauto. admit. + + intros; eapply nested_monotonic; eauto. + admit. + + destruct trap; try_simplify_someHyps. + intros; eapply nested_monotonic; eauto. + admit. + + intros; eapply nested_monotonic; eauto. + admit. + + intros; eapply nested_monotonic. 2: eauto. + eapply IHib1. 2: eauto. + simpl; intros; eapply nested_monotonic; eauto. + + repeat autodestruct; intros; try_simplify_someHyps. +Admitted. + +Inductive is_last {A} (x:A): list A -> Prop := + is_last_refl: is_last x (x::nil) + | is_last_cons a l (NXT: is_last x l): is_last x (a::l) + . + +Lemma nested_last_1 P oks (LAST: is_last P oks): forall ok + (N: nested ok oks), + P -> ok. +Proof. + induction LAST; simpl; intros. + + inv N; auto. + + inv N; eauto. + eapply IHLAST; eauto. + eapply nested_monotonic; eauto. +Qed. + +Lemma nested_last_all P oks (LAST: is_last P oks): forall ok + (N: nested ok oks), + P -> forall Q, List.In Q oks -> Q. +Proof. + induction LAST; simpl; intros. + + intuition subst. inv N; auto. + + inv N. + intuition subst. + * 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 + (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. +Proof. + induction ib; simpl; intros; try_simplify_someHyps. + + destruct trap; simpl; try_simplify_someHyps. + + (* seq *) + intros; eapply IHib1; 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. +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. +Proof. + induction ib; simpl; intros; subst; try_simplify_someHyps. + + destruct trap; simpl in *; try_simplify_someHyps. congruence. + + (* seq *) + intros; eapply IHib1; 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. +*) + +(** RAFFINEMENT EXEC SYMBOLIQUE **) + Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := match ib with | BF fin _ => Rfinal (tr_ris f fin ris) (sexec_final_sfv fin ris) @@ -625,33 +819,49 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := end . -Local Hint Constructors rst_refines: core. 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. -Lemma rexec_rec_correct ctx f ib: - forall ris sis rk k - (CONT: forall rs ss, ris_refines ctx rs ss -> rst_refines ctx (rk rs) (k ss)) +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)) + ris sis hsis st (REF: ris_refines ctx ris sis) - (*OK: ris_ok ctx ris*) - , rst_refines ctx (rexec_rec f ib ris rk) (sexec_rec f ib sis k). -Proof. - induction ib; simpl; eauto. - - (* load *) autodestruct; eauto. - - intros. - econstructor; eauto. - symmetry. - erewrite seval_condition_valid_preserv; eauto. -Admitted. + (EXEC: sexec_rec (cf ctx) ib sis k = st) + (OK1: history ctx ib sis kok = Some hsis) + (OK2: histOK ctx hsis st) + , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st. +Proof. + induction ib; simpl; try (intros; subst; eauto; fail). + - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. + - (* seq *) + intros; subst. + eapply IHib1; eauto. + simpl. intros; subst. eapply IHib2; eauto. + - (* cond *) + intros rk k kok CONT ris sis hsis st REF EXEC. subst. + autodestruct. + intros EQb. + destruct (history _ _ _ _) eqn: EQl; + intros; try_simplify_someHyps; intros. + inv OK2. + assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV; eauto. } + try_simplify_someHyps; intros. + generalize EVAL. + erewrite seval_condition_valid_preserv, <- seval_condition_refpreserv; eauto. + intros; + econstructor; try_simplify_someHyps. +Qed. Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort). -Lemma rexec_correct ctx f ib: - rst_refines ctx (rexec f ib) (sexec f ib). +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)) -> + rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). Proof. - eapply rexec_rec_correct; eauto. - (* econstructor; simpl; auto. congruence. *) + unfold sexec; intros; eapply rexec_rec_correct; eauto. + simpl; congruence. Qed. - - - -- cgit