Library OSQGetMsgPure

Require Export mathlib.

Lemma R_PrioTbl_P_msg : forall v´6 v´15 x p t m m´ av,
  TcbMod.get v´15 x = Some (p, t, m) ->
  R_PrioTbl_P v´6 v´15 av -> R_PrioTbl_P v´6 (TcbMod.set v´15 x (p, t, m´)) av.

Lemma TCBNode_P_msg : forall x0 v´19 x7 m m´ i5 i4 i3 i2 i1 i0 i p t v´12,
 TCBNode_P
         (x0
          :: v´19
             :: x7
                :: m
                   :: Vint32 i5
                      :: Vint32 i4
                         :: Vint32 i3
                            :: Vint32 i2
                               :: Vint32 i1 :: Vint32 i0 :: Vint32 i :: nil)
         v´12 (p, t, m) ->
 TCBNode_P
         (x0
          :: v´19
             :: x7
                :: m´
                   :: Vint32 i5
                      :: Vint32 i4
                         :: Vint32 i3
                            :: Vint32 i2
                               :: Vint32 i1 :: Vint32 i0 :: Vint32 i :: nil)
         v´12 (p, t, m´).

Lemma RH_TCBList_ECBList_P_msg :
  forall v´14 v´15 x p t m m´,
    TcbMod.get v´15 x = Some (p, t, m) ->
    RH_TCBList_ECBList_P v´14 v´15 x ->
    RH_TCBList_ECBList_P v´14 (TcbMod.set v´15 x (p, t, m´)) x.

Lemma RHL_ECB_ETbl_P_msg : forall x0 x v v´14 p t m m´,
  RHL_ECB_ETbl_P x0 v v´14 ->
  TcbMod.get v´14 x = Some (p, t, m) ->
  RHL_ECB_ETbl_P x0 v (TcbMod.set v´14 x (p, t, m´)).

Lemma RLH_ECB_ETbl_P_msg : forall x0 v v´14 x p t m m´,
  RLH_ECB_ETbl_P x0 v v´14 ->
  TcbMod.get v´14 x = Some (p, t, m) ->
  RLH_ECB_ETbl_P x0 v (TcbMod.set v´14 x (p, t, m´)).

Lemma R_ECB_ETbl_P_msg : forall x0 v v´14 x p t m m´,
  R_ECB_ETbl_P x0 v v´14 ->
  TcbMod.get v´14 x = Some (p, t, m) ->
R_ECB_ETbl_P x0 v (TcbMod.set v´14 x (p, t, m´)).

Lemma ECBList_P_msg : forall v´4 v x6 x t m m´ v´3 v´13 v´14 p,
  ECBList_P x6 v v´4 v´3 v´13 v´14 ->
  TcbMod.get v´14 x = Some (p, t, m) ->
  ECBList_P x6 v v´4 v´3 v´13 (TcbMod.set v´14 x (p, t, m´)).

Lemma RH_CurTCB_Prop : forall x y p t m m´,
                         TcbMod.get y x = Some (p, t, m) ->
                         RH_CurTCB x y ->
                         RH_CurTCB x
                                   (TcbMod.set y x (p,t,m´)).


Lemma OSQGetMsg_high_level_step : forall P prio state msg hecbls htcbls htime hcurtcb,
  TcbMod.get htcbls hcurtcb = Some (prio, state, msg) ->
  can_change_aop P ->
  absinfer
     (<|| getmsg nil ||> **
      HECBList hecbls **
      HTCBList htcbls **
      HTime htime ** HCurTCB hcurtcb ** P)
     ( <|| END (Some msg) ||> **
      HECBList hecbls **
      HTCBList (TcbMod.set htcbls hcurtcb (prio, state, Vnull))
      ** HTime htime ** HCurTCB hcurtcb ** P).
  Ltac join_get_solver :=
    match goal with
      | H: OSAbstMod.join (OSAbstMod.sig ?x ?y) _ ?O |- OSAbstMod.get ?O ?x = Some ?y =>
        eapply OSAbstMod.join_get_get_l; eauto
      | H: OSAbstMod.join ?O1 ?O2 ?O |- OSAbstMod.get ?O ?x = Some ?y =>
        eapply OSAbstMod.join_get_get_r; [eauto | join_get_solver]
    end.