Library semdel_pure
Require Import sem_common.
Require Import sem_lab.
Open Scope code_scope.
Lemma sem_ecb_wt_ex_prop :
forall grp etbl v x v´21 v´23 mqls tcbls cnt x2 x3 v´42 ecbls tid,
Int.eq grp ($ 0) = false ->
Int.unsigned grp <= 255 ->
array_type_vallist_match Int8u etbl ->
length etbl = ∘OS_EVENT_TBL_SIZE ->
RL_Tbl_Grp_P etbl (Vint32 grp) ->
ECBList_P v (Vptr x) v´21 v´23 mqls tcbls->
R_ECB_ETbl_P x
(V$OS_EVENT_TYPE_SEM
:: Vint32 grp
:: Vint32 cnt :: x2 :: x3 :: v´42 :: nil,
etbl) tcbls ->
RH_TCBList_ECBList_P ecbls tcbls tid ->
exists cnt´ t´ tl,
EcbMod.get ecbls x = Some (abssem cnt´, t´ :: tl).
Lemma semdel_ecblist_ecbmod_get :
forall v´53 v´33 v´34 v´36 v´57 i2 x5 x6 x7 v´45 v´38,
Int.unsigned i2 <= 65535 ->
array_type_vallist_match Int8u v´53 ->
RH_CurTCB v´36 v´34 ->
length v´53 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´33 v´34 v´36 ->
RL_Tbl_Grp_P v´53 (V$0) ->
ECBList_P (Vptr (v´57, Int.zero)) Vnull
(nil ++
((V$OS_EVENT_TYPE_SEM :: V$0 :: Vint32 i2 :: x5 :: x6 :: x7 :: nil,
v´53) :: nil) ++ v´45) (nil ++ (DSem i2 :: nil) ++ v´38) v´33 v´34 ->
EcbMod.get v´33 (v´57, Int.zero) = Some (abssem i2, nil) /\
exists vv, EcbMod.join vv (EcbMod.sig (v´57, Int.zero) (abssem i2, nil)) v´33 /\
ECBList_P x7 Vnull v´45 v´38 vv v´34.
Lemma semdel_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 .
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 semdel_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 semdel_ecblist_ecbmod_get´ :
forall v´57 v´40 v´35 v´53 v´33 v´34 v´36 v´47 i2 x5 x6 x7 v´45 v´38,
Some (Vptr (v´57, Int.zero)) = get_last_ptr v´40 ->
length v´40 = length v´35 ->
Int.unsigned i2 <= 65535 ->
array_type_vallist_match Int8u v´53 ->
RH_CurTCB v´36 v´34 ->
length v´53 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´33 v´34 v´36 ->
RL_Tbl_Grp_P v´53 (V$0) ->
ECBList_P v´47 Vnull
(v´40 ++
((V$OS_EVENT_TYPE_SEM :: V$0 :: Vint32 i2 :: x5 :: x6 :: x7 :: nil,
v´53) :: nil) ++ v´45) (v´35 ++ (DSem i2 :: nil) ++ v´38) v´33
v´34 ->
EcbMod.get v´33 (v´57, Int.zero) = Some (abssem i2, nil) /\
exists vg vv vx,
ECBList_P v´47 (Vptr (v´57, Int.zero)) v´40 v´35 vg v´34 /\
EcbMod.join vg vx v´33 /\
EcbMod.join vv (EcbMod.sig (v´57, Int.zero) (abssem i2, nil)) vx /\
ECBList_P x7 Vnull v´45 v´38 vv v´34.
Lemma semdel_ecbjoin_sig_join:
forall x x1 v´35 x0 v´61 i2,
EcbMod.join x x1 v´35 ->
EcbMod.join x0 (EcbMod.sig (v´61, Int.zero) (abssem i2, nil)) x1 ->
exists y,
EcbMod.join x0 x y /\
EcbMod.join y (EcbMod.sig (v´61, Int.zero) (abssem i2, nil)) v´35.
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 semdel_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.
Require Import sem_lab.
Open Scope code_scope.
Lemma sem_ecb_wt_ex_prop :
forall grp etbl v x v´21 v´23 mqls tcbls cnt x2 x3 v´42 ecbls tid,
Int.eq grp ($ 0) = false ->
Int.unsigned grp <= 255 ->
array_type_vallist_match Int8u etbl ->
length etbl = ∘OS_EVENT_TBL_SIZE ->
RL_Tbl_Grp_P etbl (Vint32 grp) ->
ECBList_P v (Vptr x) v´21 v´23 mqls tcbls->
R_ECB_ETbl_P x
(V$OS_EVENT_TYPE_SEM
:: Vint32 grp
:: Vint32 cnt :: x2 :: x3 :: v´42 :: nil,
etbl) tcbls ->
RH_TCBList_ECBList_P ecbls tcbls tid ->
exists cnt´ t´ tl,
EcbMod.get ecbls x = Some (abssem cnt´, t´ :: tl).
Lemma semdel_ecblist_ecbmod_get :
forall v´53 v´33 v´34 v´36 v´57 i2 x5 x6 x7 v´45 v´38,
Int.unsigned i2 <= 65535 ->
array_type_vallist_match Int8u v´53 ->
RH_CurTCB v´36 v´34 ->
length v´53 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´33 v´34 v´36 ->
RL_Tbl_Grp_P v´53 (V$0) ->
ECBList_P (Vptr (v´57, Int.zero)) Vnull
(nil ++
((V$OS_EVENT_TYPE_SEM :: V$0 :: Vint32 i2 :: x5 :: x6 :: x7 :: nil,
v´53) :: nil) ++ v´45) (nil ++ (DSem i2 :: nil) ++ v´38) v´33 v´34 ->
EcbMod.get v´33 (v´57, Int.zero) = Some (abssem i2, nil) /\
exists vv, EcbMod.join vv (EcbMod.sig (v´57, Int.zero) (abssem i2, nil)) v´33 /\
ECBList_P x7 Vnull v´45 v´38 vv v´34.
Lemma semdel_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 .
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 semdel_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 semdel_ecblist_ecbmod_get´ :
forall v´57 v´40 v´35 v´53 v´33 v´34 v´36 v´47 i2 x5 x6 x7 v´45 v´38,
Some (Vptr (v´57, Int.zero)) = get_last_ptr v´40 ->
length v´40 = length v´35 ->
Int.unsigned i2 <= 65535 ->
array_type_vallist_match Int8u v´53 ->
RH_CurTCB v´36 v´34 ->
length v´53 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´33 v´34 v´36 ->
RL_Tbl_Grp_P v´53 (V$0) ->
ECBList_P v´47 Vnull
(v´40 ++
((V$OS_EVENT_TYPE_SEM :: V$0 :: Vint32 i2 :: x5 :: x6 :: x7 :: nil,
v´53) :: nil) ++ v´45) (v´35 ++ (DSem i2 :: nil) ++ v´38) v´33
v´34 ->
EcbMod.get v´33 (v´57, Int.zero) = Some (abssem i2, nil) /\
exists vg vv vx,
ECBList_P v´47 (Vptr (v´57, Int.zero)) v´40 v´35 vg v´34 /\
EcbMod.join vg vx v´33 /\
EcbMod.join vv (EcbMod.sig (v´57, Int.zero) (abssem i2, nil)) vx /\
ECBList_P x7 Vnull v´45 v´38 vv v´34.
Lemma semdel_ecbjoin_sig_join:
forall x x1 v´35 x0 v´61 i2,
EcbMod.join x x1 v´35 ->
EcbMod.join x0 (EcbMod.sig (v´61, Int.zero) (abssem i2, nil)) x1 ->
exists y,
EcbMod.join x0 x y /\
EcbMod.join y (EcbMod.sig (v´61, Int.zero) (abssem i2, nil)) v´35.
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 semdel_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.