diff options
-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. |