From 6c0efaa166b1acbabcdcd051c5ec389b9b562fe6 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 10 Jun 2021 08:15:06 +0200 Subject: remove history --- scheduling/BTL_SEsimuref.v | 299 +++++++++++++++++---------------------------- scheduling/BTL_SEtheory.v | 18 +-- 2 files changed, 121 insertions(+), 196 deletions(-) diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 98587b66..2ca36b11 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -8,9 +8,6 @@ on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct". - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement ! - TODO: A REVOIR COMPLETEMENT. - - introduire "fake" hash-consed values (à renommer en "refined" plutôt que "fake"). - *) Require Import Coqlib Maps Floats. @@ -18,6 +15,9 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import Op Registers. Require Import RTL BTL OptionMonad BTL_SEtheory. + +Local Open Scope option_monad_scope. + (** * Refinement of data-structures and of the specification of the simulation test *) Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core. @@ -45,12 +45,20 @@ Definition ris_sreg_get (ris: ristate) r: sval := Coercion ris_sreg_get: ristate >-> Funclass. Record ris_ok ctx (ris: ristate) : Prop := { - OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None; - OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None + OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None; + OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None }. Local Hint Resolve OK_RMEM OK_RREG: core. Local Hint Constructors ris_ok: core. +(* TODO: Is it useful ? +Definition ris_abs (ris: ristate) : sistate := {| + si_pre := fun ctx => ris_ok ctx ris; + si_sreg := ris_sreg_get ris; + si_smem := ris.(ris_smem) +|}. +*) + Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := { OK_EQUIV: si_ok ctx sis <-> ris_ok ctx ris; MEM_EQ: ris_ok ctx ris -> eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem); @@ -178,6 +186,21 @@ Inductive rstate := | Rabort . + +Record routcome := rout { + _ris: ristate; + _rfv: sfval; +}. + +Fixpoint get_routcome ctx (rst:rstate): option routcome := + match rst with + | Rfinal ris rfv => Some (rout ris rfv) + | Rcond cond args ifso ifnot => + SOME b <- seval_condition ctx cond args IN + get_routcome ctx (if b then ifso else ifnot) + | Rabort => None + end. + Inductive rst_simu: rstate -> rstate -> Prop := | Rfinal_simu ris1 ris2 rfv1 rfv2 (RIS: ris_simu ris1 ris2) @@ -196,6 +219,19 @@ Inductive rst_simu: rstate -> rstate -> Prop := *) . +Lemma rst_simu_lroutcome rst1 rst2: + rst_simu rst1 rst2 -> + forall f1 f2 (ctx: simu_proof_context f1 f2) ris1 rfv1, + get_routcome (bctx1 ctx) rst1 = Some (rout ris1 rfv1) -> + exists ris2 rfv2, get_routcome (bctx2 ctx) rst2 = Some (rout ris2 rfv2) /\ ris_simu ris1 ris2 /\ rfv_simu rfv1 rfv2. +Proof. + induction 1; simpl; intros f1 f2 ctx lris1 lrfv1 ROUT; try_simplify_someHyps. + erewrite <- seval_condition_preserved. + autodestruct. + destruct b; simpl; auto. +Qed. + + (* Comment prend on en compte le ris en cours d'execution ??? *) Inductive rst_refines ctx: rstate -> sstate -> Prop := @@ -212,6 +248,30 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop := : rst_refines ctx Rabort Sabort . +Lemma rst_refines_outcome_up ctx rst st: + rst_refines ctx rst st -> + forall ris rfv, + get_routcome ctx rst = Some (rout ris rfv) -> + exists sis sfv, get_soutcome ctx st = Some (sout sis sfv) /\ ris_refines ctx ris sis /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv). +Proof. + induction 1; simpl; intros lris lrfv ROUT; try_simplify_someHyps. + rewrite RCOND. + autodestruct. + destruct b; simpl; auto. +Qed. + +Lemma rst_refines_outcome_down ctx rst st: + rst_refines ctx rst st -> + forall sis sfv, + get_soutcome ctx st = Some (sout sis sfv) -> + exists ris rfv, get_routcome ctx rst = Some (rout ris rfv) /\ ris_refines ctx ris sis /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv). +Proof. + induction 1; simpl; intros lris lrfv ROUT; try_simplify_someHyps. + rewrite RCOND. + autodestruct. + destruct b; simpl; auto. +Qed. + Local Hint Resolve ris_simu_correct rvf_simu_correct: core. Lemma rst_simu_correct rst1 rst2: @@ -248,7 +308,7 @@ Lemma eval_list_sval_refpreserv ctx args ris sis: ris_refines ctx ris sis -> ris_ok ctx ris -> eval_list_sval ctx (list_sval_inj (map ris args)) = - eval_list_sval ctx (list_sval_inj (map sis args)). + eval_list_sval ctx (list_sval_inj (map (si_sreg sis) args)). Proof. intros REF OK. induction args; simpl; eauto. @@ -565,168 +625,20 @@ Proof. 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 IN - SOME oks <- history ctx (if b then ifso else ifnot) sis k IN - Some (sis::oks) - end - . - -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. - -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 (si_ok ctx sis) (List.map (si_ok ctx) hsis)) - sis hsis - (RET: history ctx ib sis k = Some hsis), - nested (si_ok ctx sis) (List.map (si_ok ctx) 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. +Lemma si_ok_tr_sis_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis. 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 si_ok_op_down ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis. +Admitted. -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 si_ok_trap_down ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis. +Admitted. -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)) - (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. 2-3: eauto. - simpl; intros; eapply IHib2; eauto. - + (* cond *) - autodestruct. - destruct (history _ _ _ _) eqn: HIST; try_simplify_someHyps. - intros; econstructor. - destruct b; eauto. -Qed. - -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; try_simplify_someHyps. - + destruct trap; simpl in *; try_simplify_someHyps. - + (* seq *) - intros; eapply IHib1. 2: eauto. - simpl; intros; eapply IHib2; eauto. - + (* cond *) - simpl in *. - autodestruct. - destruct (history _ _ _ _) eqn: X; try congruence. - intros; destruct b; eauto. -Qed. +Lemma si_ok_store_down ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis. +Admitted. -(* 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 (si_ok ctx sis1) (List.map (si_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. +(* 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. (** RAFFINEMENT EXEC SYMBOLIQUE **) @@ -755,50 +667,61 @@ Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_r 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: - forall kok rk k - (CONT: forall ris sis hsis st, ris_refines ctx ris sis -> k sis = st -> kok sis = Some hsis -> (forall sis, List.In sis hsis -> si_ok ctx sis) -> rst_refines ctx (rk ris) (k sis)) - ris sis hsis st + 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)) + ris sis lsis sfv 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: forall sis, List.In sis hsis -> si_ok ctx sis) + (SOUT: get_soutcome ctx st = Some (sout lsis sfv)) + (OK: si_ok ctx lsis) , 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. + eapply IHib1. 3-6: eauto. + + simpl. eapply sexec_rec_down; eauto. + + intros; subst. eapply IHib2; eauto. - (* cond *) - intros rk k kok CONT ris sis hsis st REF EXEC. subst. + intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst. + assert (rOK: ris_ok ctx ris). { + erewrite <- OK_EQUIV. 2: eauto. + eapply sexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + } + generalize OUT; clear OUT; simpl. autodestruct. - intros COND. - destruct (history _ _ _ _) eqn: EQl; - intros; try_simplify_someHyps; intros. - exploit (OK2 sis); auto. - assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV; eauto. } - generalize COND. + intros COND; generalize COND. erewrite <- 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 ib sis sfv: - run_sem_isstate ctx (sexec (cf ctx) ib) = Some (sout 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. - intros RUN SIS; exploit run_sem_history; eauto. - intros HIST; inv HIST. - unfold sexec; intros; eapply rexec_rec_correct; eauto. - + simpl; intros; subst; eauto. - + intros; eapply nested_last_all. - - eapply is_last_map; eauto. - - eapply NESTED. - - eapply SIS. - - eapply List.in_map; eauto. + unfold sexec; intros; eapply rexec_rec_correct; eauto; simpl; congruence. Qed. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 9074b071..5a94b235 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -25,6 +25,8 @@ Record iblock_exec_context := Bctx { (** * Syntax and semantics of symbolic values *) +(* TODO: introduire les hash-code directement ici - avec les "fake" smart constructors qui mettent un unknown_hid ? *) + (* symbolic value *) Inductive sval := | Sundef @@ -717,12 +719,12 @@ Record soutcome := sout { _sfv: sfval; }. -Fixpoint run_sem_isstate ctx (st:sstate): option soutcome := +Fixpoint get_soutcome ctx (st:sstate): option soutcome := match st with | Sfinal sis sfv => Some (sout sis sfv) | Scond cond args ifso ifnot => SOME b <- seval_condition ctx cond args IN - run_sem_isstate ctx (if b then ifso else ifnot) + get_soutcome ctx (if b then ifso else ifnot) | Sabort => None end. @@ -742,7 +744,7 @@ Inductive sem_sstate ctx stk t s: sstate -> Prop := Lemma sem_sstate_run ctx stk st t s: sem_sstate ctx stk t s st -> exists sis sfv rs m, - run_sem_isstate ctx st = Some (sout sis sfv) + get_soutcome ctx st = Some (sout sis sfv) /\ sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m /\ sem_sfval ctx stk sfv rs m t s . @@ -753,7 +755,7 @@ Qed. Local Hint Resolve sem_Sfinal: core. Lemma run_sem_sstate ctx st sis sfv: - run_sem_isstate ctx st = Some (sout sis sfv) -> + get_soutcome ctx st = Some (sout sis sfv) -> forall rs m stk s t, sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m -> sem_sfval ctx stk sfv rs m t s -> @@ -1154,8 +1156,8 @@ Qed. Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop := - forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 -> - exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) + forall sis1 sfv1, get_soutcome (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 -> + exists sis2 sfv2, get_soutcome (bctx2 ctx) st2 = Some (sout sis2 sfv2) /\ sistate_simu ctx sis1 sis2 /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2) . @@ -1261,8 +1263,8 @@ Proof. Qed. (* TODO: useless ? -Lemma run_sem_isstate_preserved sis: - run_sem_isstate (bctx1 ctx) sis = run_sem_isstate (bctx2 ctx) sis. +Lemma get_soutcome_preserved sis: + get_soutcome (bctx1 ctx) sis = get_soutcome (bctx2 ctx) sis. Proof. induction sis; simpl; eauto. erewrite seval_condition_preserved. -- cgit