diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-09-29 16:29:46 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-09-29 16:29:46 +0200 |
| commit | 886bd238d849dbd17d9a9770b8da93901b4ed643 (patch) | |
| tree | 69a94cee735ca1b8fa9412f247935e7d9024cb86 /kvx/lib/RTLpathSE_impl_junk.v | |
| parent | 5c0a6851aabd24da546ab36dc33bae2eaf3cb1f8 (diff) | |
| download | compcert-kvx-886bd238d849dbd17d9a9770b8da93901b4ed643.tar.gz compcert-kvx-886bd238d849dbd17d9a9770b8da93901b4ed643.zip | |
Some more progress
Diffstat (limited to 'kvx/lib/RTLpathSE_impl_junk.v')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 35 |
1 files changed, 33 insertions, 2 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index d156d43c..a12c939e 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -2054,6 +2054,29 @@ Lemma root_apply_none ge sp rsv rs m hst lr: Proof. Admitted. +Lemma hslocal_set_sreg_preserves_smem ge sp hst rs0 m0 r rsv lr: + WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN + seval_hsmem ge sp hst' rs0 m0 = seval_hsmem ge sp hst rs0 m0. +Proof. +Admitted. + +Lemma hslocal_set_sreg_preserves_hsok ge sp rs m hst r rsv lr: + WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN + hsok_local ge sp rs m hst <-> hsok_local ge sp rs m hst'. +Proof. +Admitted. + +Lemma red_PTree_set_correct (r r0:reg) (hsv: hsval) (hst: PTree.t hsval) ge sp rs0 m0: + hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = hsi_sreg_eval ge sp (PTree.set r hsv hst) r0 rs0 m0. +Proof. + destruct hsv; simpl; auto. + destruct (Pos.eq_dec r r1); auto. + subst; unfold hsi_sreg_eval. + destruct (Pos.eq_dec r0 r1); auto. + - subst; rewrite PTree.grs, PTree.gss; simpl; auto. + - rewrite PTree.gro, PTree.gso; simpl; auto. +Qed. + (** 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': @@ -2075,8 +2098,15 @@ Proof. destruct HREF as (A & _). apply A in SOKL. split; [assumption|]. eapply root_apply_none; eauto. - + admit. - + admit. + + intros HOKL. simpl. rewrite hslocal_set_sreg_preserves_smem; eauto. + destruct HREF as (_ & A & _). rewrite A; auto. + eapply hslocal_set_sreg_preserves_hsok; eauto. + + intros HOKL. simpl. intro r0. unfold hslocal_set_sreg in Hhst'. + wlp_hbind ok_lhsv. wlp_hbind hsv'. wlp_hret. simpl. + rewrite red_PTree_set_correct. unfold hsi_sreg_eval. + destruct (Pos.eq_dec r r0). + * subst. rewrite PTree.gss. (* Something about simplify_correct ? *) admit. + * admit. + admit. (* intros (ROK & RMEM & RVAL) OKA RSV. @@ -2097,6 +2127,7 @@ Admitted. + 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 -> |