diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-09-30 16:03:14 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-09-30 16:03:14 +0200 |
| commit | d8004bb905cb00e3bffea67c037aa6b162cad9ae (patch) | |
| tree | e1b5f14b321c8074d896b9d230a01a17f848d411 /kvx | |
| parent | 886bd238d849dbd17d9a9770b8da93901b4ed643 (diff) | |
| download | compcert-kvx-d8004bb905cb00e3bffea67c037aa6b162cad9ae.tar.gz compcert-kvx-d8004bb905cb00e3bffea67c037aa6b162cad9ae.zip | |
Proof of hsok_local_set_sreg
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 29 |
1 files changed, 25 insertions, 4 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index a12c939e..86717007 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -2030,6 +2030,13 @@ Proof. rewrite HEVAL. reflexivity. Admitted. +Lemma root_apply_preserves_hok ge sp rs m hst lr rsv: + hsok_local ge sp rs m hst -> + WHEN root_apply rsv lr hst ~> hsv THEN + seval_hsval ge sp hsv rs m <> None. +Proof. +Admitted. + Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr: hok_args ge sp rs0 m0 hst lr -> WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN @@ -2037,10 +2044,24 @@ Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr: <-> (hsok_local ge sp rs0 m0 hst /\ (WHEN root_apply rsv lr hst ~> hsv' THEN seval_hsval ge sp hsv' rs0 m0 <> None)). Proof. -(* unfold hslocal_set_sreg, ok_args, hsok_local; simpl. - destruct may_trap eqn: MAYTRAP; simpl; intuition (subst; eauto). - eapply may_trap_correct; eauto. *) -Admitted. + intros HOK. unfold hslocal_set_sreg. + wlp_bind ok_lhsv. wlp_bind hsv'. wlp_intro hst'. wlp_hret. + constructor. + - intros HOKL. + assert (HOKL': hsok_local ge sp rs0 m0 hst). { + destruct may_trap. + * wlp_hbind hv. wlp_hret. unfold hsok_local. + intros. apply HOKL. simpl. right. assumption. + * wlp_hret. unfold hsok_local. + intros. apply HOKL. simpl. assumption. } + split; [assumption|]. + wlp_intro hsv2. eapply root_apply_preserves_hok; eauto. + - intros (HOKL & RAPP). destruct (may_trap _ _) eqn:MAYT. + + wlp_hbind hv. wlp_hret. unfold hsok_local. simpl. intros. inv H. + * eapply root_apply_preserves_hok; eauto. + * apply HOKL. assumption. + + wlp_hret. apply HOKL. +Qed. Lemma slocal_set_sreg_preserves_sok ge sp rs m st r sv: sok_local ge sp rs m st <-> sok_local ge sp rs m (slocal_set_sreg st r sv). |