From 7d66fffc7453a5ec446c7d2c2c7b4f7f5c86ea4f Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 18 Sep 2020 17:42:05 +0200 Subject: More avancement --- kvx/lib/RTLpathSE_impl_junk.v | 32 +++++++++++++++++++++++++++++--- 1 file changed, 29 insertions(+), 3 deletions(-) (limited to 'kvx/lib') diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 0c2af325..ec48c975 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -1986,6 +1986,19 @@ 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 @@ -2010,9 +2023,23 @@ Proof. generalize (REG r0); clear REG. destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). (* Iload *) - - admit. + - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0. + eapply hsist_set_local_correct_dyn; eauto. + + destruct H1 as (A & B & C). + eapply hslocal_set_sreg_correct; eauto. + { eapply refines_okargs. repeat (econstructor; eauto). } + simpl. intro HOK. unfold root_apply. wlp_bind lhsv LHSV. wlp_intro hsv HSV. + eapply hlist_args_correct in LHSV; eauto. + erewrite hSload_correct; eauto. simpl. reflexivity. + + unfold sok_local; simpl; intros (PRE & MEM & REG). + intuition. + generalize (REG r0); clear REG. + destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). (* Istore *) - - admit. + - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0. + eapply hsist_set_local_correct_dyn; eauto. + + admit. (** TODO - port hslocal_set_smem_correct *) + + unfold sok_local; simpl; intuition. (* Icall *) - admit. (* Itailcall *) @@ -2028,7 +2055,6 @@ Proof. Admitted. - (* PROOF from RTLpathSE_impl.v destruct i; simpl; intros STEP1 STEP2; inversion_clear STEP1; inversion_clear STEP2; discriminate || (intro REF; eauto). -- cgit