Library OSQDelPure
Require Export mathlib.
Lemma ecb_wt_ex_prop :
forall
v´43 v´34 v´38 x v´21 tid
v´23 v´35 i i3 x2 x3 v´42 v´40,
Int.eq i ($ 0) = false ->
Int.unsigned i <= 255 ->
array_type_vallist_match Int8u v´40 ->
length v´40 = ∘OS_EVENT_TBL_SIZE ->
RL_Tbl_Grp_P v´40 (Vint32 i) ->
ECBList_P v´38 (Vptr x) v´21 v´23 v´43 v´35->
R_ECB_ETbl_P x
(V$OS_EVENT_TYPE_Q
:: Vint32 i
:: Vint32 i3 :: x2 :: x3 :: v´42 :: nil,
v´40) v´35 ->
RH_TCBList_ECBList_P v´34 v´35 tid ->
exists t´ tl z y,
EcbMod.get v´34 x = Some (absmsgq z y, t´ :: tl).
Lemma ecblist_pin :
forall v1 x y v1´ v2 v3 v4 z,
ECBList_P x y v1 v2 v3 v4 -> In y (get_eidls x (v1 ++ z :: v1´)).
Lemma ecblist_ecbmod_get_aux :
forall v´61 i6 x4 x8 v´58 v´42
v´63 x20 x19 x9 x10 x15 i5 i4 v´65 x21 x22 v3 v´37 v´35 v´36 v´38,
Int.unsigned i5 <= 65535 ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P (Vptr (v´61, Int.zero)) Vnull
(
((V$OS_EVENT_TYPE_Q
:: V$0 :: Vint32 i6 :: Vptr (v´63, Int.zero) :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(
(DMsgQ (Vptr (v´63, Int.zero))
(x20
:: x19
:: x9
:: x10
:: x15
:: Vint32 i5
:: Vint32 i4 :: Vptr (v´65, Int.zero) :: nil)
(x21 :: x22 :: nil) v3 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmsgq msgls i5, nil)
/\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmsgq msgls i5, nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecblist_ecbmod_get :
forall v´61 i6 x4 x8 v´58 v´42 v´21
v´63 x20 x19 x9 x10 x15 i5 i4 v´65 x21 x22 v3 v´37 v´35 v´36 v´38,
length v´21 = O ->
Int.unsigned i5 <= 65535 ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P (Vptr (v´61, Int.zero)) Vnull
(nil ++
((V$OS_EVENT_TYPE_Q
:: V$0 :: Vint32 i6 :: Vptr (v´63, Int.zero) :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(v´21 ++
(DMsgQ (Vptr (v´63, Int.zero))
(x20
:: x19
:: x9
:: x10
:: x15
:: Vint32 i5
:: Vint32 i4 :: Vptr (v´65, Int.zero) :: nil)
(x21 :: x22 :: nil) v3 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmsgq msgls i5, nil)
/\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmsgq msgls i5, nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecb_del_prop_RHhold:
forall v´35 v´36 v´38 x y absmg,
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
EcbMod.join x (EcbMod.sig y (absmg, nil))
v´35 -> RH_TCBList_ECBList_P x v´36 v´38 .
Require Import Mbox_common.
Lemma get_last_prop:
forall (l : list EventCtr) x v y,
l <> nil ->
(get_last_ptr ((x, v) :: l) = y <->
get_last_ptr l = y).
Lemma ecblist_p_decompose :
forall y1 z1 x y2 z2 t z ,
length y1 = length y2 ->
ECBList_P x Vnull (y1++z1) (y2++z2) t z ->
exists x1 t1 t2,
ECBList_P x x1 y1 y2 t1 z /\ ECBList_P x1 Vnull z1 z2 t2 z /\
EcbMod.join t1 t2 t /\ (get_last_ptr y1 = None \/ get_last_ptr y1 = Some x1).
Lemma ecblist_ecbmod_get´ :
forall v´40 v´52 v´61 i6 x4 x8 v´58 v´42 v´21
v´63 x20 x19 x9 x10 x15 i5 i4 v´65 x21 x22 v3 v´37 v´35 v´36 v´38,
Some (Vptr (v´61, Int.zero)) = get_last_ptr v´40 ->
length v´40 = length v´21 ->
Int.unsigned i5 <= 65535 ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P v´52 Vnull
(v´40 ++
((V$OS_EVENT_TYPE_Q
:: V$0 :: Vint32 i6 :: Vptr (v´63, Int.zero) :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(v´21 ++
(DMsgQ (Vptr (v´63, Int.zero))
(x20
:: x19
:: x9
:: x10
:: x15
:: Vint32 i5
:: Vint32 i4 :: Vptr (v´65, Int.zero) :: nil)
(x21 :: x22 :: nil) v3 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmsgq msgls i5, nil)
/\ exists vg vv vx,
ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 vg v´36 /\
EcbMod.join vg vx v´35/\
EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmsgq msgls i5, nil)) vx/\
ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma upd_last_prop:
forall v g x vl z ,
V_OSEventListPtr v = Some x ->
vl = upd_last_ectrls ((v, g) :: nil) z ->
exists v´, vl = ((v´, g) ::nil) /\ V_OSEventListPtr v´ = Some z.
Lemma nth_val_upd_prop:
forall vl n m v x,
(n<>m)%nat ->
(nth_val n (update_nth val m vl v) = Some x <->
nth_val n vl = Some x).
Lemma R_ECB_upd_hold :
forall x1 v v0 v´36 x8,
R_ECB_ETbl_P x1 (v, v0) v´36 ->
R_ECB_ETbl_P x1 (update_nth val 5 v x8, v0) v´36.
Lemma ecb_list_join_join :
forall v´40 v´52 v´61 v´21 x x2 v´36 x8 v´42 v´37 x0 v´51,
v´40 <> nil ->
ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 x v´36 ->
ECBList_P x8 Vnull v´42 v´37 x0 v´36 ->
v´51 = upd_last_ectrls v´40 x8 ->
EcbMod.join x0 x x2 ->
ECBList_P v´52 Vnull (v´51 ++ v´42) (v´21 ++ v´37) x2 v´36.
Lemma absinfer_qdel_err1_return :
forall P ,
can_change_aop P ->
absinfer (<|| qdel (Vnull :: nil) ||> ** P)
( <|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> ** P).
Lemma absinfer_qdel_err2_return :
forall x a P ,
can_change_aop P ->
~ (exists x0 y wls, EcbMod.get x a = Some (absmsgq x0 y, wls)) ->
absinfer (<|| qdel (Vptr a :: nil) ||> ** HECBList x ** P)
( <|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> ** HECBList x ** P).
Lemma absinfer_qdel_succ_return :
forall ecbls ecbls´ x y a P tid tcbls t,
can_change_aop P ->
EcbMod.get ecbls a = Some (absmsgq x y, nil) ->
EcbMod.join ecbls´ (EcbMod.sig a (absmsgq x y, nil)) ecbls ->
absinfer (<|| qdel (Vptr a :: nil) ||> ** HECBList ecbls **
HTCBList tcbls ** HTime t ** HCurTCB tid ** P) ( <|| END (Some (V$NO_ERR)) ||> **
HECBList ecbls´ ** HTCBList tcbls ** HTime t ** HCurTCB tid ** P).
Lemma absinfer_qdel_err3_return :
forall x a P ,
can_change_aop P ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x y wls, d = (absmsgq x y, wls))) ->
absinfer (<|| qdel (Vptr a :: nil) ||> ** HECBList x **
P) ( <|| END (Some (V$ OS_ERR_EVENT_TYPE)) ||> ** HECBList x ** P).
Lemma absinfer_qdel_err4_return :
forall x a P ,
can_change_aop P ->
(exists t´ tl z y,
EcbMod.get x a = Some (absmsgq z y, t´ :: tl)) ->
absinfer (<|| qdel (Vptr a :: nil) ||> ** HECBList x **
P) ( <|| END (Some (V$ OS_ERR_TASK_WAITING)) ||> ** HECBList x ** P).
Lemma ecb_wt_ex_prop :
forall
v´43 v´34 v´38 x v´21 tid
v´23 v´35 i i3 x2 x3 v´42 v´40,
Int.eq i ($ 0) = false ->
Int.unsigned i <= 255 ->
array_type_vallist_match Int8u v´40 ->
length v´40 = ∘OS_EVENT_TBL_SIZE ->
RL_Tbl_Grp_P v´40 (Vint32 i) ->
ECBList_P v´38 (Vptr x) v´21 v´23 v´43 v´35->
R_ECB_ETbl_P x
(V$OS_EVENT_TYPE_Q
:: Vint32 i
:: Vint32 i3 :: x2 :: x3 :: v´42 :: nil,
v´40) v´35 ->
RH_TCBList_ECBList_P v´34 v´35 tid ->
exists t´ tl z y,
EcbMod.get v´34 x = Some (absmsgq z y, t´ :: tl).
Lemma ecblist_pin :
forall v1 x y v1´ v2 v3 v4 z,
ECBList_P x y v1 v2 v3 v4 -> In y (get_eidls x (v1 ++ z :: v1´)).
Lemma ecblist_ecbmod_get_aux :
forall v´61 i6 x4 x8 v´58 v´42
v´63 x20 x19 x9 x10 x15 i5 i4 v´65 x21 x22 v3 v´37 v´35 v´36 v´38,
Int.unsigned i5 <= 65535 ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P (Vptr (v´61, Int.zero)) Vnull
(
((V$OS_EVENT_TYPE_Q
:: V$0 :: Vint32 i6 :: Vptr (v´63, Int.zero) :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(
(DMsgQ (Vptr (v´63, Int.zero))
(x20
:: x19
:: x9
:: x10
:: x15
:: Vint32 i5
:: Vint32 i4 :: Vptr (v´65, Int.zero) :: nil)
(x21 :: x22 :: nil) v3 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmsgq msgls i5, nil)
/\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmsgq msgls i5, nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecblist_ecbmod_get :
forall v´61 i6 x4 x8 v´58 v´42 v´21
v´63 x20 x19 x9 x10 x15 i5 i4 v´65 x21 x22 v3 v´37 v´35 v´36 v´38,
length v´21 = O ->
Int.unsigned i5 <= 65535 ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P (Vptr (v´61, Int.zero)) Vnull
(nil ++
((V$OS_EVENT_TYPE_Q
:: V$0 :: Vint32 i6 :: Vptr (v´63, Int.zero) :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(v´21 ++
(DMsgQ (Vptr (v´63, Int.zero))
(x20
:: x19
:: x9
:: x10
:: x15
:: Vint32 i5
:: Vint32 i4 :: Vptr (v´65, Int.zero) :: nil)
(x21 :: x22 :: nil) v3 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmsgq msgls i5, nil)
/\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmsgq msgls i5, nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecb_del_prop_RHhold:
forall v´35 v´36 v´38 x y absmg,
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
EcbMod.join x (EcbMod.sig y (absmg, nil))
v´35 -> RH_TCBList_ECBList_P x v´36 v´38 .
Require Import Mbox_common.
Lemma get_last_prop:
forall (l : list EventCtr) x v y,
l <> nil ->
(get_last_ptr ((x, v) :: l) = y <->
get_last_ptr l = y).
Lemma ecblist_p_decompose :
forall y1 z1 x y2 z2 t z ,
length y1 = length y2 ->
ECBList_P x Vnull (y1++z1) (y2++z2) t z ->
exists x1 t1 t2,
ECBList_P x x1 y1 y2 t1 z /\ ECBList_P x1 Vnull z1 z2 t2 z /\
EcbMod.join t1 t2 t /\ (get_last_ptr y1 = None \/ get_last_ptr y1 = Some x1).
Lemma ecblist_ecbmod_get´ :
forall v´40 v´52 v´61 i6 x4 x8 v´58 v´42 v´21
v´63 x20 x19 x9 x10 x15 i5 i4 v´65 x21 x22 v3 v´37 v´35 v´36 v´38,
Some (Vptr (v´61, Int.zero)) = get_last_ptr v´40 ->
length v´40 = length v´21 ->
Int.unsigned i5 <= 65535 ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P v´52 Vnull
(v´40 ++
((V$OS_EVENT_TYPE_Q
:: V$0 :: Vint32 i6 :: Vptr (v´63, Int.zero) :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(v´21 ++
(DMsgQ (Vptr (v´63, Int.zero))
(x20
:: x19
:: x9
:: x10
:: x15
:: Vint32 i5
:: Vint32 i4 :: Vptr (v´65, Int.zero) :: nil)
(x21 :: x22 :: nil) v3 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmsgq msgls i5, nil)
/\ exists vg vv vx,
ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 vg v´36 /\
EcbMod.join vg vx v´35/\
EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmsgq msgls i5, nil)) vx/\
ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma upd_last_prop:
forall v g x vl z ,
V_OSEventListPtr v = Some x ->
vl = upd_last_ectrls ((v, g) :: nil) z ->
exists v´, vl = ((v´, g) ::nil) /\ V_OSEventListPtr v´ = Some z.
Lemma nth_val_upd_prop:
forall vl n m v x,
(n<>m)%nat ->
(nth_val n (update_nth val m vl v) = Some x <->
nth_val n vl = Some x).
Lemma R_ECB_upd_hold :
forall x1 v v0 v´36 x8,
R_ECB_ETbl_P x1 (v, v0) v´36 ->
R_ECB_ETbl_P x1 (update_nth val 5 v x8, v0) v´36.
Lemma ecb_list_join_join :
forall v´40 v´52 v´61 v´21 x x2 v´36 x8 v´42 v´37 x0 v´51,
v´40 <> nil ->
ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 x v´36 ->
ECBList_P x8 Vnull v´42 v´37 x0 v´36 ->
v´51 = upd_last_ectrls v´40 x8 ->
EcbMod.join x0 x x2 ->
ECBList_P v´52 Vnull (v´51 ++ v´42) (v´21 ++ v´37) x2 v´36.
Lemma absinfer_qdel_err1_return :
forall P ,
can_change_aop P ->
absinfer (<|| qdel (Vnull :: nil) ||> ** P)
( <|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> ** P).
Lemma absinfer_qdel_err2_return :
forall x a P ,
can_change_aop P ->
~ (exists x0 y wls, EcbMod.get x a = Some (absmsgq x0 y, wls)) ->
absinfer (<|| qdel (Vptr a :: nil) ||> ** HECBList x ** P)
( <|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> ** HECBList x ** P).
Lemma absinfer_qdel_succ_return :
forall ecbls ecbls´ x y a P tid tcbls t,
can_change_aop P ->
EcbMod.get ecbls a = Some (absmsgq x y, nil) ->
EcbMod.join ecbls´ (EcbMod.sig a (absmsgq x y, nil)) ecbls ->
absinfer (<|| qdel (Vptr a :: nil) ||> ** HECBList ecbls **
HTCBList tcbls ** HTime t ** HCurTCB tid ** P) ( <|| END (Some (V$NO_ERR)) ||> **
HECBList ecbls´ ** HTCBList tcbls ** HTime t ** HCurTCB tid ** P).
Lemma absinfer_qdel_err3_return :
forall x a P ,
can_change_aop P ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x y wls, d = (absmsgq x y, wls))) ->
absinfer (<|| qdel (Vptr a :: nil) ||> ** HECBList x **
P) ( <|| END (Some (V$ OS_ERR_EVENT_TYPE)) ||> ** HECBList x ** P).
Lemma absinfer_qdel_err4_return :
forall x a P ,
can_change_aop P ->
(exists t´ tl z y,
EcbMod.get x a = Some (absmsgq z y, t´ :: tl)) ->
absinfer (<|| qdel (Vptr a :: nil) ||> ** HECBList x **
P) ( <|| END (Some (V$ OS_ERR_TASK_WAITING)) ||> ** HECBList x ** P).