From 492a71c60c0dbc810f50b75bdf820c2acfc88d7d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 9 Jun 2021 18:45:26 +0200 Subject: fix sstate_simu --- scheduling/BTL_SEsimuref.v | 49 +++++++++++++++++----------------------------- scheduling/BTL_SEtheory.v | 18 ++++++++++++++++- 2 files changed, 35 insertions(+), 32 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 40c28934..98587b66 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -20,21 +20,8 @@ Require Import RTL BTL OptionMonad BTL_SEtheory. (** * Refinement of data-structures and of the specification of the simulation test *) -Record sis_ok ctx (sis: sistate): Prop := { - OK_PRE: (sis.(si_pre) ctx); - OK_SMEM: eval_smem ctx sis.(si_smem) <> None; - OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None -}. Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core. -Local Hint Constructors sis_ok: core. - -Lemma sem_sok ctx sis rs m: - sem_sistate ctx sis rs m -> sis_ok ctx sis. -Proof. - unfold sem_sistate; - econstructor; - intuition congruence. -Qed. +Local Hint Constructors si_ok: core. (* NB: refinement of (symbolic) internal state *) Record ristate := @@ -65,7 +52,7 @@ Local Hint Resolve OK_RMEM OK_RREG: core. Local Hint Constructors ris_ok: core. Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := { - OK_EQUIV: sis_ok ctx sis <-> ris_ok ctx ris; + 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); REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r) }. @@ -97,7 +84,7 @@ Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2: sistate_simu ctx sis1 sis2. Proof. intros RIS REF1 REF2 rs m SEM. - exploit sem_sok; eauto. + exploit sem_si_ok; eauto. erewrite OK_EQUIV; eauto. intros ROK1. exploit ris_simu_ok_preserv; eauto. @@ -238,7 +225,7 @@ Proof. inv REF1; inv REF2; simpl in *; inv SEM1; auto. - (* final_simu *) do 2 eexists; intuition; eauto. - exploit sem_sok; eauto. + exploit sem_si_ok; eauto. erewrite OK_EQUIV; eauto. intros ROK1. exploit ris_simu_ok_preserv; eauto. @@ -249,8 +236,8 @@ Proof. intros SCOND0; rewrite <- SCOND0 in RCOND0. erewrite <- SCOND0. destruct b; simpl. - * exploit IHrst_simu1; eauto. - * exploit IHrst_simu2; eauto. + * intros; exploit IHrst_simu1; eauto. + * intros; exploit IHrst_simu2; eauto. Qed. (** * Refinement of the symbolic execution *) @@ -321,8 +308,8 @@ Definition rset_smem rm (ris:ristate): ristate := |}. Lemma ok_set_mem ctx sm sis: - sis_ok ctx (set_smem sm sis) - <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None). + si_ok ctx (set_smem sm sis) + <-> (si_ok ctx sis /\ eval_smem ctx sm <> None). Proof. split; destruct 1; econstructor; simpl in *; eauto. intuition eauto. @@ -374,8 +361,8 @@ Definition rset_sreg r rsv (ris:ristate): ristate := |}. Lemma ok_set_sreg ctx r sv sis: - sis_ok ctx (set_sreg r sv sis) - <-> (sis_ok ctx sis /\ eval_sval ctx sv <> None). + si_ok ctx (set_sreg r sv sis) + <-> (si_ok ctx sis /\ eval_sval ctx sv <> None). Proof. unfold set_sreg; split. + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split. @@ -493,8 +480,8 @@ Definition transfer_sis (inputs: list reg) (sis:sistate): sistate := si_smem := sis.(si_smem) |}. Lemma ok_transfer_sis ctx inputs sis: - sis_ok ctx (transfer_sis inputs sis) - <-> (sis_ok ctx sis). + si_ok ctx (transfer_sis inputs sis) + <-> (si_ok ctx sis). Proof. unfold transfer_sis. induction inputs as [|r l]; simpl. + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence. @@ -626,10 +613,10 @@ Qed. Lemma history_nested ctx ib: forall k - (CONT: forall sis hsis, (k sis) = Some hsis -> nested (sis_ok ctx sis) (List.map (sis_ok ctx) hsis)) + (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 (sis_ok ctx sis) (List.map (sis_ok ctx) hsis). + nested (si_ok ctx sis) (List.map (si_ok ctx) hsis). Proof. induction ib; simpl; intros; try_simplify_someHyps. + econstructor; eauto. admit. @@ -721,7 +708,7 @@ 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)) + (NESTED: nested (si_ok ctx sis1) (List.map (si_ok ctx) hsis)) (LAST: is_last sis2 hsis) : history_spec ctx sis1 sis2 (Some hsis) . @@ -770,12 +757,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 -> (forall sis, List.In sis hsis -> sis_ok ctx sis) -> 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 -> si_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: forall sis, List.In sis hsis -> sis_ok ctx sis) + (OK2: forall sis, List.In sis hsis -> si_ok ctx sis) , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st. Proof. induction ib; simpl; try (intros; subst; eauto; fail). @@ -802,7 +789,7 @@ 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) -> - (sis_ok ctx sis) -> + (si_ok ctx sis) -> rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). Proof. intros RUN SIS; exploit run_sem_history; eauto. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 97dc7fc8..9074b071 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1137,8 +1137,24 @@ Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Pr Definition sistate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (sis1 sis2:sistate): Prop := forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sem_sistate (bctx2 ctx) sis2 rs m. + +Record si_ok ctx (sis: sistate): Prop := { + OK_PRE: (sis.(si_pre) ctx); + OK_SMEM: eval_smem ctx sis.(si_smem) <> None; + OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None +}. + +Lemma sem_si_ok ctx sis rs m: + sem_sistate ctx sis rs m -> si_ok ctx sis. +Proof. + unfold sem_sistate; + econstructor; + intuition congruence. +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) -> + 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) /\ sistate_simu ctx sis1 sis2 /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2) -- cgit