Library OSQCreatePure
Require Export mathlib.
Lemma RL_Tbl_init_prop : RL_Tbl_Grp_P INIT_EVENT_TBL (Vint32 Int.zero).
Lemma WLF_OSQ_prop: forall v´47 v´46 i,
val_inj
(bool_or
(val_inj
(if Int.ltu ($ OS_MAX_Q_SIZE) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(bool_or
(val_inj
(if Int.ltu ($ OS_MAX_Q_SIZE) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull ->
WellformedOSQ
(v´47
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vptr (v´46, (Int.zero+ᵢ($ 4+ᵢInt.zero))+ᵢInt.mul ($ 4) i)
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vint32 i :: V$0 :: Vptr (v´46, Int.zero) :: nil).
Lemma OSQCRT_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 (absmsgq nil i, nil))
v´38 v´40.
Lemma ECBList_OSQCRT_prop :
forall v´41 v´48 v´50 v´22 v´28 v´40
v´47 v´46 i v´37 v´38 v´45 v´43 x0 v´27,
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_Q
:: Vint32 Int.zero
:: V$0 :: Vptr (v´48, Int.zero) :: v´50 :: v´22 :: nil,
INIT_EVENT_TBL) :: v´28)
(DMsgQ (Vptr (v´48, Int.zero))
(v´47
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vptr (v´46, (Int.zero+ᵢ($ 4+ᵢInt.zero))+ᵢInt.mul ($ 4) i)
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vint32 i :: V$0 :: Vptr (v´46, Int.zero) :: nil)
(v´43 :: x0 :: nil) v´45 :: v´27)
(EcbMod.set v´37 (v´41, Int.zero) (absmsgq nil i, nil))
v´38.
Lemma ecblist_star_not_inh :
forall v´28 v´24 eid v´27 v´37 v´38 s vl P,
ECBList_P v´24 Vnull v´28 v´27 v´37 v´38 ->
s |= Astruct eid OS_EVENT vl **
evsllseg v´24 Vnull v´28 v´27 ** P ->
EcbMod.get v´37 eid = None.
Lemma absimp_qcre_err_return :
forall P i,
can_change_aop P ->
(Int.unsigned i <=? 65535 = true) ->
absinfer ( <|| qcre (Vint32 i :: nil)||> ** P) ( <|| END (Some Vnull) ||> ** P).
Lemma absimp_qcre_succ_return:
forall P i qid qls tcbls curtid tm,
can_change_aop P ->
Int.ltu ($ Q_SIZE) i = false ->
EcbMod.get qls qid = None ->
absinfer ( <|| qcre (Vint32 i :: nil) ||>
**HECBList qls ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vptr qid)) ||> **
HECBList (EcbMod.set qls qid (absmsgq (nil:list val)
i,
nil:list tid)) **HTCBList tcbls ** HTime tm **
HCurTCB curtid **P).
Lemma int_ltu_maxq_eq :
forall i,
Int.ltu ($ OS_MAX_Q_SIZE) i = true->
Int.eq i ($0) = false.
Lemma val_inj_boolor_false:
forall i,
val_inj
(bool_or
(val_inj
(if Int.ltu ($ OS_MAX_Q_SIZE) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(bool_or
(val_inj
(if Int.ltu ($ OS_MAX_Q_SIZE) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull ->
Int.ltu ($ Q_SIZE) i = false .
Lemma RL_Tbl_init_prop : RL_Tbl_Grp_P INIT_EVENT_TBL (Vint32 Int.zero).
Lemma WLF_OSQ_prop: forall v´47 v´46 i,
val_inj
(bool_or
(val_inj
(if Int.ltu ($ OS_MAX_Q_SIZE) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(bool_or
(val_inj
(if Int.ltu ($ OS_MAX_Q_SIZE) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull ->
WellformedOSQ
(v´47
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vptr (v´46, (Int.zero+ᵢ($ 4+ᵢInt.zero))+ᵢInt.mul ($ 4) i)
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vint32 i :: V$0 :: Vptr (v´46, Int.zero) :: nil).
Lemma OSQCRT_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 (absmsgq nil i, nil))
v´38 v´40.
Lemma ECBList_OSQCRT_prop :
forall v´41 v´48 v´50 v´22 v´28 v´40
v´47 v´46 i v´37 v´38 v´45 v´43 x0 v´27,
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_Q
:: Vint32 Int.zero
:: V$0 :: Vptr (v´48, Int.zero) :: v´50 :: v´22 :: nil,
INIT_EVENT_TBL) :: v´28)
(DMsgQ (Vptr (v´48, Int.zero))
(v´47
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vptr (v´46, (Int.zero+ᵢ($ 4+ᵢInt.zero))+ᵢInt.mul ($ 4) i)
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vptr (v´46, Int.zero+ᵢ($ 4+ᵢInt.zero))
:: Vint32 i :: V$0 :: Vptr (v´46, Int.zero) :: nil)
(v´43 :: x0 :: nil) v´45 :: v´27)
(EcbMod.set v´37 (v´41, Int.zero) (absmsgq nil i, nil))
v´38.
Lemma ecblist_star_not_inh :
forall v´28 v´24 eid v´27 v´37 v´38 s vl P,
ECBList_P v´24 Vnull v´28 v´27 v´37 v´38 ->
s |= Astruct eid OS_EVENT vl **
evsllseg v´24 Vnull v´28 v´27 ** P ->
EcbMod.get v´37 eid = None.
Lemma absimp_qcre_err_return :
forall P i,
can_change_aop P ->
(Int.unsigned i <=? 65535 = true) ->
absinfer ( <|| qcre (Vint32 i :: nil)||> ** P) ( <|| END (Some Vnull) ||> ** P).
Lemma absimp_qcre_succ_return:
forall P i qid qls tcbls curtid tm,
can_change_aop P ->
Int.ltu ($ Q_SIZE) i = false ->
EcbMod.get qls qid = None ->
absinfer ( <|| qcre (Vint32 i :: nil) ||>
**HECBList qls ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vptr qid)) ||> **
HECBList (EcbMod.set qls qid (absmsgq (nil:list val)
i,
nil:list tid)) **HTCBList tcbls ** HTime tm **
HCurTCB curtid **P).
Lemma int_ltu_maxq_eq :
forall i,
Int.ltu ($ OS_MAX_Q_SIZE) i = true->
Int.eq i ($0) = false.
Lemma val_inj_boolor_false:
forall i,
val_inj
(bool_or
(val_inj
(if Int.ltu ($ OS_MAX_Q_SIZE) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(bool_or
(val_inj
(if Int.ltu ($ OS_MAX_Q_SIZE) i
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))
(val_inj
(if Int.eq i ($ 0)
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull ->
Int.ltu ($ Q_SIZE) i = false .