Library OSMutexPendProof



Require Import sem_common.
Require Import sempend_pure.
Require Import os_mutex.
Require Import OSMutex_common.
Require Import OSMutexPendPart5.
Require Import OSMutexPendPart1.
Require Import OSMutexPendPart2.
Require Import OSQPostPure.
Require Import gen_lemmas.
Open Scope code_scope.

Lemma mutex_pend_part_0: gen_mutex_pend_part_0.
the unfold of transform_pre: eapply backward_rule1. intros. eapply mutex_pend_inv_update1; eauto. sep cancel AEventData. exact_s.
*************** infer the high level cur_stat is rdy

cancel AECBList

AOSTCBList

rename TcbList_P part

info: tcbls_sub_l ++ ptcb_node ++ tcbls_sub_r = tcbls_l
info: tcbls_sub_l ++ ptcb_node ++ tcbls_sub_r = tcbls_r'

Theorem OSMutexPendProof:
  forall vl p r,
    Some p =
    BuildPreA´ os_api OSMutexPend
               mutexpendapi vl ->
    Some r =
    BuildRetA´ os_api OSMutexPend
               mutexpendapi vl ->
    exists t d1 d2 s,
      os_api OSMutexPend = Some (t, d1, d2, s) /\
      {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.
PS: 由于os_eventsearch(pevent)可能找到，也可能找不到，所以，这里就天然的要分成两种情况