From ca81e74a0fbe21fcdecaa16ddd17f3413ce15e04 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 3 Sep 2020 16:58:58 +0200 Subject: Updates from _impl.v to _impl_junk.v --- kvx/lib/RTLpathSE_impl_junk.v | 157 +++++++++++++++++++++++++++--------------- 1 file changed, 102 insertions(+), 55 deletions(-) (limited to 'kvx') diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 8cb45c55..f5821810 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -527,12 +527,6 @@ Global Opaque PTree_frame_eq_check. (** hsilocal_simu_check and properties *) -(* 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. @@ -808,8 +802,7 @@ Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) := and a "dynamic" part -- that depends on it *) Definition hsiexit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop := - hsi_cond hext = si_cond ext - /\ hsi_ifso hext = si_ifso ext. + hsi_ifso hext = si_ifso ext. Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse). @@ -826,8 +819,9 @@ Qed. 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) - /\ hseval_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) -> + hseval_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 -> @@ -853,32 +847,36 @@ 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; refine (modusponens _ _ (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 <- hseval_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. } refine (modusponens _ _ (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]; [congruence | | ]. - + constructor; [|constructor]; simpl; auto. - + destruct HREF2 as (_ & IFSO). congruence. + simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1) by congruence. + exists path. constructor; [|constructor]; [congruence| |congruence]. + constructor; [|constructor]; simpl; auto. Qed. Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2: @@ -964,9 +962,43 @@ Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop := hsi_pc hst = si_pc st /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st). +Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop := + nsok_nil st: nested_sok ge sp rs0 m0 st nil + | nsok_cons st se lse: + (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) -> + nested_sok ge sp rs0 m0 (si_elocal se) lse -> + nested_sok ge sp rs0 m0 st (se::lse). + +Lemma nested_sok_prop ge sp st sle rs0 m0: + nested_sok ge sp rs0 m0 st sle -> + sok_local ge sp rs0 m0 st -> + forall se, In se sle -> sok_local ge sp rs0 m0 (si_elocal se). +Proof. + induction 1; simpl; intuition (subst; eauto). +Qed. + +Lemma nested_sok_elocal ge sp rs0 m0 st2 exits: + nested_sok ge sp rs0 m0 st2 exits -> + forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) -> + nested_sok ge sp rs0 m0 st1 exits. +Proof. + induction 1; [intros; constructor|]. + intros. constructor; auto. +Qed. + +Lemma nested_sok_tail ge sp rs0 m0 st lx exits: + is_tail lx exits -> + nested_sok ge sp rs0 m0 st exits -> + nested_sok ge sp rs0 m0 st lx. +Proof. + induction 1; [auto|]. + intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto. +Qed. + Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop := hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st) - /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st). + /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st) + /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st). Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2, hsistate_refines_stat hst1 st1 -> @@ -994,22 +1026,25 @@ Remark init_hsistate_correct_dyn ge sp rs0 m0 pc: Proof. unfold init_hsistate. wlp_step_bind hst HST. wlp_simplify. - constructor; simpl; auto. + constructor; simpl; auto; [|constructor]. - apply list_forall2_nil. - apply init_hsistate_local_correct. assumption. + - constructor. Qed. 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: @@ -1029,23 +1064,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 ext1 lx1, + (forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> 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 ext lx1. intros OK H. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction. + - simpl; intros ext lx1 OK 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. apply OK. eassumption. + * 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: @@ -1096,7 +1135,7 @@ Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx: Proof. intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI. destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2). - destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2). + destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _). destruct SIMUC as (PCSIMU & ESIMU & LSIMU). exploit hsiexits_simu_core_correct; eauto. intro HESIMU. unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT. @@ -1104,25 +1143,33 @@ 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. + * eapply nested_sok_prop; eauto. + eapply ssem_local_sok; 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. } - 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. - + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption. - + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ). - destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ). - exists path. repeat (constructor; auto). + exploit siexits_simu_all_fallthrough_upto; eauto. + * destruct ALLFU as (ITAIL & ALLF). + exploit nested_sok_tail; eauto. intros NESTED2. + inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML. + eapply nested_sok_prop; 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. + + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption. + + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ). + destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ). + exists path. repeat (constructor; auto). Qed. Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) := -- cgit