Library MboxCreatePure

Require Import include.
Require Import memory.

Require Import memdata.

Require Import NPeano.
Require Import os_code_defs.
Require Import os_code_notations.
Require Import os_ucos_h.
Require Import ucert.
Require Import OSQCreatePure.
Open Scope code_scope.
Require Import os_code_notations.
Require Import List.

Require Import Mbox_common.

Lemma absimp_mbox_create_err_return : forall P i,
   can_change_aop P -> isptr i ->
absinfer ( <|| mbox_create ( i :: nil) ||> ** P) ( <|| END (Some Vnull) ||> ** P).

Lemma absimp_mbox_create_succ_return :
  forall P i qid qls tcbls curtid tm,
    can_change_aop P ->
    isptr i ->
    EcbMod.get qls qid = None ->
    absinfer ( <|| mbox_create ( i :: nil) ||>
                 **HECBList qls ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
           ( <|| END (Some (Vptr qid)) ||> **
                 HECBList (EcbMod.set qls qid (absmbox i,
                                               nil:list tid)) **HTCBList tcbls ** HTime tm **
                 HCurTCB curtid **P).
Lemma intlemma1 :forall v´19 v´21, id_addrval´ (Vptr (v´21, Int.zero)) OSEventTbl OS_EVENT = Some v´19 -> (v´21, Int.zero+ᵢ($ 4+ᵢ($ 2+ᵢ($ 1+ᵢ($ 1+ᵢInt.zero))))) = v´19.

Lemma ECBList_MBox_Create_prop :
  forall v´41 v´50 v´22 v´28 v´40
          v´37 v´38 v´27 x,
    RH_TCBList_ECBList_P v´37 v´38 v´40 ->
    EcbMod.get v´37 (v´41, Int.zero) = None ->
    ECBList_P v´22 Vnull v´28 v´27 v´37 v´38->
    ECBList_P (Vptr (v´41, Int.zero)) Vnull
              
              ((V$OS_EVENT_TYPE_MBOX :: Vint32 Int.zero :: V$0 :: x :: v´50 :: v´22 :: nil, INIT_EVENT_TBL) :: v´28)
              (DMbox x :: v´27)
              (EcbMod.set v´37 (v´41, Int.zero) (absmbox x, nil))
              v´38.

Lemma MBox_Create_TCB_prop :
  forall v´37 x i v´38 v´40 ,
    EcbMod.get v´37 x = None ->
    RH_TCBList_ECBList_P v´37 v´38 v´40 ->
    RH_TCBList_ECBList_P
      (EcbMod.set v´37 x (absmbox i, nil))
      v´38 v´40.