Library semacc_pure

Require Import sem_common.

Open Scope code_scope.

Lemma semacc_new_fundation:
  forall s P a msgq mq a´ msgq´ mq´ n wls i x2 x3 x4 qid b tcbls,
    s |= AEventData a msgq ** P ->
    RLH_ECBData_P msgq mq ->
    R_ECB_ETbl_P qid (a,b) tcbls ->
    a = (V$OS_EVENT_TYPE_SEM :: Vint32 i :: Vint32 n :: x2 :: x3 :: x4 :: nil) ->
    msgq = DSem n ->
    mq = (abssem n, wls) ->
    Int.ltu Int.zero n = true ->
    a´ = (V$OS_EVENT_TYPE_SEM :: Vint32 i :: Vint32 (n-ᵢ$ 1) :: x2 :: x3 :: x4 :: nil) ->
    msgq´ = DSem (n-ᵢ$ 1) ->
    mq´ = (abssem (n-ᵢ$ 1), wls) ->
    s |= AEventData a´ msgq´ **
         [| RLH_ECBData_P msgq´ mq´ |] **
         [| R_ECB_ETbl_P qid (a´,b) tcbls |] ** P.

Lemma semacc_RH_TCBList_ECBList_P_hold:
  forall mqls tcbls ct a n wl,
    RH_TCBList_ECBList_P mqls tcbls ct ->
    EcbMod.get mqls a = Some (abssem n, wl) ->
    Int.ltu Int.zero n = true ->
    RH_TCBList_ECBList_P
      (EcbMod.set mqls a (abssem (Int.sub n Int.one), wl)) tcbls ct.