diff options
author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-18 18:05:52 +0200 |
---|---|---|
committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-18 18:05:52 +0200 |
commit | 6cd7dce5a15de04ee8ad5746f623191d803f7e77 (patch) | |
tree | b69601ceb48fbc8dbf04691e38dae24a5917bc81 | |
parent | 95d972434bd4d3b6ee0d0f68c688920dafe14afc (diff) | |
download | compcert-kvx-6cd7dce5a15de04ee8ad5746f623191d803f7e77.tar.gz compcert-kvx-6cd7dce5a15de04ee8ad5746f623191d803f7e77.zip |
**Ugly** proof of simu_check_single_correct
-rw-r--r-- | scheduling/RTLpathSE_impl.v | 39 |
1 files changed, 31 insertions, 8 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 40a05739..08a62202 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -1864,14 +1864,37 @@ Lemma simu_check_single_correct dm tf f pc1 pc2: sexec_simu dm f tf pc1 pc2. Proof. unfold sexec_simu; wlp_simplify. - exploit H2; clear H2. 1-3: wlp_simplify. - (* intros (st2 & SEXEC2 & REF2). try_simplify_someHyps. - exploit H3; clear H3. 1-3: wlp_simplify. - intros (st3 & SEXEC3 & REF3). try_simplify_someHyps. - eexists. eexists. split; eauto. split; eauto. - intros ctx. - eapply hsstate_simu_spec_correct; eauto. *) -Admitted. + exploit H3. 1-5: wlp_simplify. + - simpl. + exploit H0; eauto. + wlp_simplify. + + assert (exta7 = true). { destruct exta7; auto. } + subst. + assert (exta8 = true). { destruct exta8; auto. } subst. + unfold hscond_set_hid. + rewrite H8. + assert (lhsv x = lhsv y). { apply H9. reflexivity. } + rewrite H12. + reflexivity. + + discriminate. + - intros (st2 & SEXEC2 & REF2). try_simplify_someHyps. + exploit H4; clear H4. 1-5: wlp_simplify. + + simpl. + exploit H0; eauto. + wlp_simplify. 2: { discriminate. } + assert (exta7 = true). { destruct exta7; auto. } + subst. + assert (exta8 = true). { destruct exta8; auto. } subst. + unfold hscond_set_hid. + rewrite H4. + assert (lhsv x = lhsv y). { apply H5. reflexivity. } + rewrite H9. + reflexivity. + + intros (st3 & SEXEC3 & REF3). try_simplify_someHyps. + eexists. eexists. split; eauto. split; eauto. + intros ctx. + eapply hsstate_simu_spec_correct; eauto. +Qed. Global Opaque simu_check_single. Global Hint Resolve simu_check_single_correct: wlp. |