From 1b196baa866aceb569df4f9f6803c7d3ea18f3d9 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 27 Aug 2020 18:46:22 +0200 Subject: reduction de la preuve de raffinement du exit à ok_allexit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- kvx/lib/RTLpathSE_impl.v | 113 +++++++++++++++++++++++++-------------------- kvx/lib/RTLpathSE_theory.v | 22 +++++++-- 2 files changed, 81 insertions(+), 54 deletions(-) (limited to 'kvx') diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v index 4e159b15..96854123 100644 --- a/kvx/lib/RTLpathSE_impl.v +++ b/kvx/lib/RTLpathSE_impl.v @@ -49,19 +49,6 @@ Proof. unfold hsi_sreg_eval, hsi_sreg_get; destruct (PTree.get r hst); simpl; auto. Qed. -(* negation of sabort_local *) -Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop := - (st.(si_pre) ge sp rs0 m0) - /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None - /\ forall (r: reg), seval_sval ge sp (si_sreg st r) rs0 m0 <> None. - -Lemma ssem_local_sok ge sp rs0 m0 st rs m: - ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st. -Proof. - unfold sok_local, ssem_local. - intuition congruence. -Qed. - Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop := (forall sv, List.In sv (hsi_ok_lsval hst) -> seval_sval ge sp sv rs0 m0 <> None) /\ (seval_smem ge sp hst.(hsi_smem) rs0 m0 <> None). @@ -216,8 +203,8 @@ Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse). Definition hsiexit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop := hsilocal_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext) - /\ seval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0 - = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0. + /\ (hsok_local ge sp rs0 m0 (hsi_elocal hext) -> seval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0 + = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0). Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2, hsiexit_refines_stat hse1 se1 -> @@ -243,26 +230,31 @@ Theorem hsiexit_simu_core_correct dm f hse1 hse2 ctx: Proof. intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2. assert (SEVALC: - seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) - (the_rs0 ctx) (the_m0 ctx) = - seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) - (the_rs0 ctx) (the_m0 ctx)). - { destruct HDYN1 as (_ & SCOND1). rewrite <- SCOND1 by assumption. clear SCOND1. - destruct HDYN2 as (_ & SCOND2). rewrite <- SCOND2 by assumption. clear SCOND2. + sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1) -> + (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) + (the_rs0 ctx) (the_m0 ctx)) = + (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) + (the_rs0 ctx) (the_m0 ctx))). + { destruct HDYN1 as ((OKEQ1 & _) & SCOND1). + rewrite OKEQ1; intro OK1. rewrite <- SCOND1 by assumption. clear SCOND1. + generalize (genv_match ctx). + intro GFS; exploit hsiexit_simu_core_nofail; eauto. + destruct HDYN2 as (_ & SCOND2). intro OK2. rewrite <- SCOND2 by assumption. clear OK1 OK2 SCOND2. destruct SIMUC as ((path & _ & LSIMU) & _ & CONDEQ & ARGSEQ). destruct LSIMU as (_ & _ & MEMEQ). rewrite CONDEQ. rewrite ARGSEQ. rewrite MEMEQ. erewrite <- seval_condition_preserved; eauto. - eapply ctx. } + } constructor; [assumption|]. intros is1 ICONT SSEME. + assert (OK1: sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1)). { + destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok; eauto. } assert (HOK1: hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1). { - unfold hsok_exit. destruct SSEME as (_ & SSEML & _). apply ssem_local_sok in SSEML. - destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. } + unfold hsok_exit. destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. } exploit hsiexit_simu_core_nofail. 2: eapply ctx. all: eauto. intro HOK2. - destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _). + destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _); eauto. destruct HDYN1 as (LREF1 & _). destruct HDYN2 as (LREF2 & _). exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. intros (SSEML & EQREG). eexists (mk_istate (icontinue is1) (si_ifso st2) _ (imem is1)). simpl. constructor. - - constructor; [|constructor]; [congruence | eassumption | reflexivity]. + - constructor; intuition congruence || eauto. - unfold istate_simu. rewrite ICONT. simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1). { destruct HREF1 as (_ & IFSO). congruence. } exists path. constructor; [|constructor]. @@ -329,14 +321,16 @@ Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2, siexits_simu dm f lse1 lse2 ctx -> all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) -> + (forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx). Proof. - induction 1; [unfold all_fallthrough; contradiction|]. - intros X ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU). + induction 1; [unfold all_fallthrough; contradiction|]; simpl. + intros X OK ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU). apply IHlist_forall2 in ALLFU. - destruct H as (CONDSIMU & _). - inv INEXT; [|eauto]. - erewrite <- CONDSIMU; eauto. + - destruct H as (CONDSIMU & _). + inv INEXT; [|eauto]. + erewrite <- CONDSIMU; eauto. + - intros; intuition. Qed. Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2: @@ -356,23 +350,27 @@ Proof. Qed. Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2: - siexits_simu dm f lse1 lse2 ctx -> forall ext1 lx1, + siexits_simu dm f lse1 lse2 ctx -> + (forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> + forall ext1 lx1, all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) -> exists ext2 lx2, all_fallthrough_upto_exit (the_ge2 ctx) (the_sp ctx) ext2 lx2 lse2 (the_rs0 ctx) (the_m0 ctx) /\ length lx1 = length lx2. Proof. induction 1. - - intros. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction. - - intros ext1 lx1 ALLFUE. + - intros OK ext lx1 H. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction. + - simpl; intros OK ext1 lx1 ALLFUE. destruct ALLFUE as (ITAIL & ALLFU). inv ITAIL. + eexists; eexists. constructor; [| eapply list_forall2_length; eauto]. constructor; [econstructor | eapply siexits_simu_all_fallthrough; eauto]. - + exploit IHlist_forall2; [constructor; eauto|]. - intros (ext2 & lx2 & ALLFUE2 & LENEQ). - eexists; eexists. constructor; eauto. - eapply all_fallthrough_upto_exit_cons; eauto. + + exploit IHlist_forall2. + * intuition. + * constructor; eauto. + * intros (ext2 & lx2 & ALLFUE2 & LENEQ). + eexists; eexists. constructor; eauto. + eapply all_fallthrough_upto_exit_cons; eauto. Qed. Lemma list_forall2_nth_error {A} (l1 l2: list A) P: @@ -417,11 +415,20 @@ Proof. rewrite H0; auto. Qed. + +Lemma ok_allexit ge sp st rs m is1: + ssem_internal ge sp st rs m is1 -> + forall se, In se (si_exits st) -> sok_local ge sp rs m (si_elocal se). +Admitted. (* TODO !! *) + + Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx: hsistate_simu_core dm f hst1 hst2 -> hsistate_simu dm f hst1 hst2 ctx. Proof. intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI. + generalize (ok_allexit _ _ _ _ _ _ SEMI). + intros EXOK. destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2). destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2). destruct SIMUC as (PCSIMU & ESIMU & LSIMU). @@ -431,18 +438,20 @@ Proof. exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. intro SSEML2. exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor. + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]]. - eapply siexits_simu_all_fallthrough; eauto. eapply hsiexits_simu_siexits; eauto. + eapply siexits_simu_all_fallthrough; eauto. + eapply hsiexits_simu_siexits; eauto. + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]]. constructor. - destruct SEMI as (ext & lx & SSEME & ALLFU). assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto). - exploit siexits_simu_all_fallthrough_upto; eauto. intros (ext2 & lx2 & ALLFU2 & LENEQ). - assert (EXTSIMU: siexit_simu dm f ctx ext ext2). { - eapply list_forall2_nth_error; eauto. - - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto. - - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL. - assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto). - congruence. } + exploit siexits_simu_all_fallthrough_upto; eauto. + intros (ext2 & lx2 & ALLFU2 & LENEQ). + assert (EXTSIMU: siexit_simu dm f ctx ext ext2). { + eapply list_forall2_nth_error; eauto. + - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto. + - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL. + assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto). + congruence. } destruct EXTSIMU as (CONDEVAL & EXTSIMU). apply EXTSIMU in SSEME; [|assumption]. clear EXTSIMU. destruct SSEME as (is2 & SSEME2 & ISIMU). exists (mk_istate (icontinue is1) (ipc is2) (irs is2) (imem is2)). constructor. @@ -1158,7 +1167,7 @@ Proof. Qed. Lemma seval_condition_refines hst st ge sp cond args rs m: - hsok_local ge sp rs m hst -> + hsok_local ge sp rs m hst -> hsilocal_refines ge sp rs m hst st -> seval_condition ge sp cond args (hsi_smem hst) rs m = seval_condition ge sp cond args (si_smem st) rs m. @@ -1226,9 +1235,13 @@ Proof. erewrite seval_smem_refines; eauto. erewrite seval_sval_refines; eauto. - (* Icond *) - admit. (* TODO *) -Admitted. - + destruct REF as (EXREF & LREF). constructor; simpl; [|assumption]. + constructor; [|assumption]. + constructor; simpl; [assumption|]. + intros; erewrite seval_condition_refines; eauto. + unfold seval_condition. + erewrite seval_list_sval_refines; eauto. +Qed. Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate := match path with diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v index 3ae6e713..4fb6bee3 100644 --- a/kvx/lib/RTLpathSE_theory.v +++ b/kvx/lib/RTLpathSE_theory.v @@ -1865,11 +1865,25 @@ Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) (sl1 sl2: sista exists is2, ssem_local (the_ge2 ctx) (the_sp ctx) sl2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) /\ istate_simu f dm is1 is2. +(* negation of sabort_local *) +Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop := + (st.(si_pre) ge sp rs0 m0) + /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None + /\ forall (r: reg), seval_sval ge sp (si_sreg st r) rs0 m0 <> None. + +Lemma ssem_local_sok ge sp rs0 m0 st rs m: + ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st. +Proof. + unfold sok_local, ssem_local. + intuition congruence. +Qed. + Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof_context f) (se1 se2: sistate_exit) := - (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) - (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) - = (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2) - (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx)) + (sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1) -> + (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) + (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) = + (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2) + (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx))) /\ forall is1, icontinue is1 = false -> ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) -> -- cgit