diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-09-18 17:42:05 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-09-18 17:42:05 +0200 |
| commit | 7d66fffc7453a5ec446c7d2c2c7b4f7f5c86ea4f (patch) | |
| tree | a90918c2fe232c18ae9221cc58298b7738cfebf2 /kvx | |
| parent | 90b813d550061709f60303cc0d926e580118b05c (diff) | |
| download | compcert-kvx-7d66fffc7453a5ec446c7d2c2c7b4f7f5c86ea4f.tar.gz compcert-kvx-7d66fffc7453a5ec446c7d2c2c7b4f7f5c86ea4f.zip | |
More avancement
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 32 |
1 files changed, 29 insertions, 3 deletions
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). |