From 4c5caa3002ac2a7688395f18e43d216431cd5cc7 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 28 Sep 2020 15:26:31 +0200 Subject: Proof of simplify_correct --- kvx/lib/RTLpathSE_impl_junk.v | 146 +++++++++++++++++++++++++++++------------- 1 file changed, 101 insertions(+), 45 deletions(-) diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 91937ffb..de67185b 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -556,13 +556,6 @@ Global Opaque PTree_frame_eq_check. (** hsilocal_simu_check and properties *) -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 seval_hsval ge sp hsv rs0 m0 := seval_sval ge sp (hsval_proj hsv) rs0 m0. Definition seval_hsmem ge sp hsm rs0 m0 := seval_smem ge sp (hsmem_proj hsm) rs0 m0. @@ -593,6 +586,13 @@ Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_loca /\ (hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0) /\ (forall r sv, hst ! r = Some sv -> In sv (hsi_ok_lsval hst)). +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. + Lemma ssem_local_refines_hok ge sp rs0 m0 hst st rs m: ssem_local ge sp st rs0 m0 rs m -> hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst. Proof. @@ -1936,6 +1936,100 @@ Proof. eapply may_trap_correct; eauto. Qed. *) +Lemma seval_list_sval_proj ge sp rs0 m0: forall lhsv lsv, + list_refines ge sp rs0 m0 lhsv lsv -> + seval_list_sval ge sp (hsval_list_proj lhsv) rs0 m0 = seval_list_sval ge sp lsv rs0 m0. +Proof. + induction lhsv. + - destruct lsv; simpl; intros H; [reflexivity | inv H]. + - destruct lsv; [intro H; inv H|]. + intros. inv H. simpl. erewrite IHlhsv; eauto. + rewrite H6. reflexivity. +Qed. + +Lemma hSop_correct ge sp rs0 m0 op lhsv lsv hst st: + WHEN hSop op lhsv (hsi_smem hst) ~> hsv THEN + hsok_local ge sp rs0 m0 hst -> + list_refines ge sp rs0 m0 lhsv lsv -> + hsilocal_refines ge sp rs0 m0 hst st -> + seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv (si_smem st)) rs0 m0. +Proof. + wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval. + rewrite <- Hexta1. simpl. clear Hexta1. + erewrite seval_list_sval_proj; eauto. clear H0. + destruct H1 as (A & B & C & D). rewrite <- B; eauto. +Qed. + +(** Version of hSop_correct with weaker hypothesis *) +Lemma hSop_correct_mem ge sp rs0 m0 op lhsv lsv hsm sm: + WHEN hSop op lhsv hsm ~> hsv THEN + seval_hsmem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0 -> + list_refines ge sp rs0 m0 lhsv lsv -> + seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv sm) rs0 m0. +Proof. + wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval. + rewrite <- Hexta1. simpl. clear Hexta1. + erewrite seval_list_sval_proj; eauto. clear H0. + rewrite <- H. eauto. +Qed. + +Lemma hSload_correct ge sp rs0 m0 lhsv lsv hst st trap addr chunk: + WHEN hSload (hsi_smem hst) trap chunk addr lhsv ~> hsv THEN + hsok_local ge sp rs0 m0 hst -> + list_refines ge sp rs0 m0 lhsv lsv -> + hsilocal_refines ge sp rs0 m0 hst st -> + seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sload (si_smem st) trap chunk addr lsv) rs0 m0. +Proof. + wlp_simplify. apply hC_hsval_correct in Hexta3. simpl in *. unfold seval_hsval. + rewrite <- Hexta3. simpl. clear Hexta3. + erewrite seval_list_sval_proj; eauto. clear H0. + destruct H1 as (A & B & C & D). rewrite <- B; eauto. +Qed. + +Lemma hsinit_sinit ge sp rs0 m0: + WHEN hSinit () ~> init THEN + seval_hsmem ge sp init rs0 m0 = seval_smem ge sp Sinit rs0 m0. +Proof. + wlp_intro init. eapply hsinit_seval_hsmem in Hinit; eauto. +Qed. + +Lemma simplify_correct (rsv: root_sval) lr (ge: RTL.genv) (sp: val) rs0 m0 v hst st: + WHEN root_apply rsv lr hst ~> hsv THEN + hsok_local ge sp rs0 m0 hst -> + hsilocal_refines ge sp rs0 m0 hst st -> + seval_hsval ge sp hsv rs0 m0 = Some v -> + WHEN simplify rsv lr hst ~> hsv' THEN + seval_hsval ge sp hsv' rs0 m0 = Some v. +Proof. + wlp_bind lhsv. wlp_intro hsv. intros HOK HREF HEVAL. + eapply hlist_args_correct in Hlhsv; eauto. + destruct rsv; simpl. + (* Rop *) + - exploit hSop_correct; eauto. intros EVALMOV. clear Hlhsv. clear Hhsv. + destruct (is_move_operation _ _) eqn:IMOVE. + + apply is_move_operation_correct in IMOVE. inv IMOVE. + rewrite <- HEVAL. rewrite EVALMOV. wlp_intro hsv'. + simpl. destruct HREF as (A & B & C & D). rewrite <- C; eauto. + rewrite hsi_sreg_eval_correct; eauto. + destruct (seval_hsval ge sp hsv' rs0 m0); [|reflexivity]. + apply A in HOK. destruct HOK as (_ & MOK & _). + destruct (seval_smem _ _ _ _ _); [reflexivity|contradiction]. + + clear IMOVE. wlp_bind hsm. wlp_bind lhsv'. wlp_intro hsv'. + eapply hlist_args_correct in Hlhsv'; eauto. + rewrite hSop_correct_mem; eauto; [|eapply hsinit_sinit; eauto]. + clear Hlhsv'. clear Hhsv'. rewrite <- HEVAL. rewrite EVALMOV. + admit. (** Voir avec Sylvain - je ne sais plus où on en est sur les dépendances mémoires avec les op *) + (* Rload *) + - exploit hSload_correct; eauto. intros EVALLOAD. + wlp_bind lhsv'. wlp_intro hsv'. eapply hlist_args_correct in Hlhsv'; eauto. + rewrite hSload_correct; eauto. rewrite EVALLOAD in HEVAL. + destruct trap; simpl; auto. simpl in HEVAL. + destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence. + destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence. + destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. + rewrite HEVAL. reflexivity. +Admitted. + (** TODO - express some lemma about root_apply_correct and simplify_correct * Figure out how to prove this stuff *) Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lr sv': @@ -1969,31 +2063,6 @@ Proof. rewrite <- RVAL, hsi_sreg_eval_correct; auto. *) Admitted. - -Lemma seval_list_sval_proj ge sp rs0 m0: forall lhsv lsv, - list_refines ge sp rs0 m0 lhsv lsv -> - seval_list_sval ge sp (hsval_list_proj lhsv) rs0 m0 = seval_list_sval ge sp lsv rs0 m0. -Proof. - induction lhsv. - - destruct lsv; simpl; intros H; [reflexivity | inv H]. - - destruct lsv; [intro H; inv H|]. - intros. inv H. simpl. erewrite IHlhsv; eauto. - rewrite H6. reflexivity. -Qed. - -Lemma hSop_correct ge sp rs0 m0 op lhsv lsv hst st: - WHEN hSop op lhsv (hsi_smem hst) ~> hsv THEN - hsok_local ge sp rs0 m0 hst -> - list_refines ge sp rs0 m0 lhsv lsv -> - hsilocal_refines ge sp rs0 m0 hst st -> - seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv (si_smem st)) rs0 m0. -Proof. - wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval. - rewrite <- Hexta1. simpl. clear Hexta1. - erewrite seval_list_sval_proj; eauto. clear H0. - destruct H1 as (A & B & C & D). rewrite <- B; eauto. -Qed. - Lemma seval_list_hsval_refines ge sp rs0 m0 hst st lr: hsok_local ge sp rs0 m0 hst -> hsilocal_refines ge sp rs0 m0 hst st -> @@ -2033,19 +2102,6 @@ Proof. apply seval_list_sval_none. assumption. Qed. -Lemma hSload_correct ge sp rs0 m0 lhsv lsv hst st trap addr chunk: - WHEN hSload (hsi_smem hst) trap chunk addr lhsv ~> hsv THEN - hsok_local ge sp rs0 m0 hst -> - list_refines ge sp rs0 m0 lhsv lsv -> - hsilocal_refines ge sp rs0 m0 hst st -> - seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sload (si_smem st) trap chunk addr lsv) rs0 m0. -Proof. - wlp_simplify. apply hC_hsval_correct in Hexta3. simpl in *. unfold seval_hsval. - rewrite <- Hexta3. simpl. clear Hexta3. - erewrite seval_list_sval_proj; eauto. clear H0. - destruct H1 as (A & B & C & D). rewrite <- B; eauto. -Qed. - (* Local Hint Resolve refines_okargs: core. *) Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st': WHEN hsiexec_inst i hst ~> ohst' THEN -- cgit