Library OSQPostPure
Require Export mathlib.
Require Import OSTimeDlyPure.
Require Import OSQAcceptPure.
Lemma ecbmod_absmsgq:
forall a x y z b,
RLH_ECBData_P
(DMsgQ a x y z) b -> exists vl n wl, b = (absmsgq vl n, wl).
Lemma post_exwt_succ_pre:
forall v´36 v´13 v´12 v´32 v´15 v´24 v´35 v´0 v´8 v´9 v´11 x x0 x1 v´6 v´10 v´38 v´69 v´39 v´58 a b c v´62 v´7 vhold,
v´12 <> Int.zero ->
R_PrioTbl_P v´36 v´7 vhold ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_Q
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig (v´32, Int.zero) (absmsgq x x0, x1) v´6 v´10 ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
TcbJoin (v´58, Int.zero) (a,b,c) v´62 v´7 ->
x1<>nil /\ GetHWait v´7 x1 (v´58,Int.zero) /\ TcbMod.get v´7 (v´58,Int.zero) = Some (a,b,c).
Lemma prio_set_rdy_in_tbl:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_in_tbl prio0 rtbl ->
prio_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7))))).
Lemma prio_set_rdy_in_tbl_rev:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7))))) ->
prio_in_tbl prio0 rtbl.
Lemma prio_set_rdy_not_in_tbl:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_not_in_tbl prio0 rtbl ->
prio_not_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7))))).
Lemma prio_set_rdy_not_in_tbl_rev:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_not_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7))))) ->
prio_not_in_tbl prio0 rtbl.
Module new_rtbl.
Definition set_rdy p rtbl :=
update_nth_val ∘(Int.unsigned (Int.shru p ($ 3))) rtbl
(val_inj (or (nth_val´ (Z.to_nat (Int.unsigned (Int.shru p ($ 3)))) rtbl)
(Vint32 ($ 1<<(p&$ 7))))).
Lemma trans_lemma_1:
forall p grp rtbl,
nth_val (Z.to_nat (Int.unsigned (Int.shru p ($ 3)))) rtbl = Some (Vint32 grp) ->
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned (Int.shru p ($ 3)))) rtbl)
(Vint32 ($ 1<<(p&$ 7))))) =
(Vint32 (Int.or grp ($ 1<<(p&$ 7)))).
Lemma prio_set_rdy_in_tbl_lemma_1:
forall rtbl p,
0<= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
(exists v, nth_val (Z.to_nat (Int.unsigned (Int.shru p ($ 3)))) rtbl = Some (Vint32 v)).
Lemma prio_set_rdy_in_tbl:
forall p0 p rtbl,
0 <= Int.unsigned p0 < 64 ->
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
p0 <> p ->
prio_in_tbl p0 rtbl ->
prio_in_tbl p0 (set_rdy p rtbl).
Lemma prio_set_rdy_in_tbl_rev:
forall p0 p rtbl,
0 <= Int.unsigned p0 < 64 ->
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
p0 <> p ->
prio_in_tbl p0 (set_rdy p rtbl) ->
prio_in_tbl p0 rtbl.
Lemma prio_set_rdy_not_in_tbl:
forall p0 p rtbl,
0 <= Int.unsigned p0 < 64 ->
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
p0 <> p ->
prio_not_in_tbl p0 rtbl ->
prio_not_in_tbl p0 (set_rdy p rtbl).
Lemma prio_set_rdy_not_in_tbl_rev:
forall p0 p rtbl,
0 <= Int.unsigned p0 < 64 ->
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
p0 <> p ->
prio_not_in_tbl p0 (set_rdy p rtbl) ->
prio_not_in_tbl p0 rtbl.
End new_rtbl.
Lemma RdyTCBblk_rtbl_add:
forall prio0 prio rtbl grp vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RdyTCBblk vl rtbl prio0 ->
RdyTCBblk vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
prio0.
Lemma RLH_RdyI_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_RdyI_P vl rtbl (prio0, stat, msg) ->
RLH_RdyI_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_RdyI_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_RdyI_P vl rtbl (prio0, stat, msg) ->
RHL_RdyI_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma WaitTCBblk_rtbl_add:
forall prio0 prio rtbl grp vl t,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
WaitTCBblk vl rtbl prio0 t->
WaitTCBblk vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
prio0 t.
Lemma WaitTCBblk_rtbl_add_rev:
forall prio0 prio rtbl grp vl t,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
WaitTCBblk vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
prio0 t ->
WaitTCBblk vl rtbl prio0 t.
Lemma RLH_Wait_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_Wait_P vl rtbl (prio0, stat, msg) ->
RLH_Wait_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_WaitS_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_WaitS_P vl rtbl (prio0, stat, msg) ->
RLH_WaitS_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_WaitQ_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_WaitQ_P vl rtbl (prio0, stat, msg) ->
RLH_WaitQ_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_WaitMB_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_WaitMB_P vl rtbl (prio0, stat, msg) ->
RLH_WaitMB_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_WaitMS_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_WaitMS_P vl rtbl (prio0, stat, msg) ->
RLH_WaitMS_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_Wait_all_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_TCB_Status_Wait_P vl rtbl (prio0, stat, msg) ->
RLH_TCB_Status_Wait_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_Wait_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_Wait_P vl rtbl (prio0, stat, msg) ->
RHL_Wait_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_WaitS_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_WaitS_P vl rtbl (prio0, stat, msg) ->
RHL_WaitS_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_WaitQ_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_WaitQ_P vl rtbl (prio0, stat, msg) ->
RHL_WaitQ_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_WaitMB_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_WaitMB_P vl rtbl (prio0, stat, msg) ->
RHL_WaitMB_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_WaitMS_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_WaitMS_P vl rtbl (prio0, stat, msg) ->
RHL_WaitMS_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_Wait_all_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_TCB_Status_Wait_P vl rtbl (prio0, stat, msg) ->
RHL_TCB_Status_Wait_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma R_TCB_Status_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
R_TCB_Status_P vl rtbl (prio0, stat, msg) ->
R_TCB_Status_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma TCBNode_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
TCBNode_P vl rtbl (prio0, stat, msg) ->
TCBNode_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma TCBNode_P_prio:
forall vl rtbl p t m,
TCBNode_P vl rtbl (p, t, m) ->
0 <= Int.unsigned p < 64 /\ V_OSTCBPrio vl = Some (Vint32 p).
Lemma TCBList_P_rtbl_add_simpl_version:
forall vl vptr rtbl tcbls prio grp,
0<= Int.unsigned prio < 64 ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
(forall tid p s m , TcbMod.get tcbls tid = Some (p,s,m) -> p <> prio
) ->
TCBList_P vptr vl rtbl tcbls ->
TCBList_P vptr vl
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio &$ 7)))))
tcbls.
Lemma TCBList_P_rtbl_add_lemma_1a:
forall ma mb mab mc ma´ ma´´ p s m tid,
TcbMod.join ma mb mab ->
TcbMod.join mc ma´ ma ->
TcbJoin tid (p, s, m) ma´´ ma´ ->
TcbMod.get mb tid = None.
Lemma get_get_neq:
forall m tid v1 v2 tid´,
TcbMod.get m tid = v1 ->
TcbMod.get m tid´ = v2 ->
v1 <> v2 ->
tid <> tid´.
Lemma TCBList_P_rtbl_add_lemma_1:
forall ma mb mab´ mab mc ma´ ma´´ prio st msg tid,
TcbMod.join ma mb mab ->
TcbMod.join mc ma´ ma ->
TcbJoin tid (prio, st, msg) ma´´ ma´ ->
TcbJoin tid (prio, st, msg) mab´ mab ->
R_Prio_No_Dup mab ->
(forall tid´ p s m,
TcbMod.get mb tid´ = Some (p, s, m) -> p <> prio).
Lemma TCBList_P_rtbl_add_lemma_2a:
forall ertbl ptbl tcbl tcbl´ tid px py prio bitx st msg mab´ mab vhold,
Int.unsigned py <= 7 ->
Int.unsigned px <= 7 ->
RL_RTbl_PrioTbl_P ertbl ptbl vhold->
nth_val´ (Z.to_nat (Int.unsigned ((py<<$ 3)+ᵢpx))) ptbl = Vptr tid ->
TcbJoin tid (prio, st, msg) tcbl´ tcbl ->
R_PrioTbl_P ptbl mab vhold->
TcbJoin tid (prio, st, msg) mab´ mab ->
nth_val´ (Z.to_nat (Int.unsigned px)) OSMapVallist = Vint32 bitx ->
prio = ((py<<$ 3)+ᵢpx) /\
0 <= Int.unsigned prio < 64 /\
px = prio &$ 7 /\
py = Int.shru prio ($ 3) /\
bitx = $ 1<<px.
Lemma TCBList_P_rtbl_add_lemma_2:
forall prio px py bitx grp rtbl vl vptr tcbls,
0 <= Int.unsigned prio < 64 ->
py = Int.shru prio ($ 3) ->
px = prio &$ 7 ->
bitx = $ 1<<px ->
Int.unsigned py <= 7 ->
Int.unsigned px <= 7 ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
TCBList_P vptr vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio &$ 7)))))
tcbls
->
TCBList_P vptr vl
(update_nth_val (Z.to_nat (Int.unsigned py)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned py)) rtbl) (Vint32 bitx))))
tcbls.
Lemma nth_val´2nth_val:
forall n rtbl x,
nth_val´ n rtbl = Vint32 x ->
nth_val n rtbl = Some (Vint32 x).
Lemma TCBList_P_rtbl_add_lemma_main:
forall px py bitx ertbl (ma mb mab mc ma´ ma´´ mab´:TcbMod.map) ptbl prio st msg tid vptr vl rtbl vhold,
Int.unsigned py <= 7 ->
Int.unsigned px <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned px)) OSMapVallist = Vint32 bitx ->
RL_RTbl_PrioTbl_P ertbl ptbl vhold->
nth_val´ (Z.to_nat (Int.unsigned ((py<<$ 3)+ᵢpx))) ptbl = Vptr tid ->
R_PrioTbl_P ptbl mab vhold->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
TcbMod.join ma mb mab ->
TcbMod.join mc ma´ ma ->
TcbJoin tid (prio, st, msg) ma´´ ma´ ->
TcbJoin tid (prio, st, msg) mab´ mab ->
TCBList_P vptr vl rtbl mb ->
TCBList_P vptr vl
(update_nth_val (Z.to_nat (Int.unsigned py)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned py)) rtbl) (Vint32 bitx))))
mb.
Lemma TCBList_P_rtbl_add:
forall v´47 v´36 v´38 v´39 v´40 v´13 v´44 v´43 v´7 v´8 v´45 v´58 v´59 v´49 v´62 v´37 prio st msg vhold,
Int.unsigned v´38 <= 7 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
prio_in_tbl ((v´38<<$ 3)+ᵢv´39) v´13 ->
RL_RTbl_PrioTbl_P v´13 v´36 vhold->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero) ->
R_PrioTbl_P v´36 v´7 vhold->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
TcbMod.join v´44 v´43 v´7 ->
TcbMod.join v´47 v´49 v´44 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´59 v´49 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
TCBList_P v´8 v´45 v´37 v´43 ->
TCBList_P v´8 v´45
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
v´43.
Lemma rl_tbl_grp_p_set_hold:
forall v´12 v´38 v´13 v´69 v´39 v´36 v´58 v´40 v´41,
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
Int.eq (v´69&Int.not v´40) Int.zero = true ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) (Vint32 (v´12&Int.not v´41)).
Lemma get_last_tcb_ptr_prop:
forall l1 a x1 x z,
V_OSTCBNext a = Some x1 ->
get_last_tcb_ptr l1 x1 = Some x ->
get_last_tcb_ptr (a :: l1) z = Some x.
Lemma TCBList_P_Split:
forall l1 x l2 rtbl tcbls,
TCBList_P x (l1 ++ l2) rtbl tcbls ->
exists y tls1 tls2,
get_last_tcb_ptr l1 x = Some y /\
TcbMod.join tls1 tls2 tcbls /\
TCBList_P x l1 rtbl tls1 /\
TCBList_P y l2 rtbl tls2.
Lemma get_last_tcb_ptr_prop´:
forall l1 a x1 x z,
l1 <> nil ->
V_OSTCBNext a = Some x1 ->
get_last_tcb_ptr (a :: l1) z = Some x->
get_last_tcb_ptr l1 x1 = Some x.
Lemma TCBList_P_Combine:
forall l1 x l2 rtbl y tls1 tls2 tcbls,
get_last_tcb_ptr l1 x = Some y ->
TcbMod.join tls1 tls2 tcbls ->
TCBList_P x l1 rtbl tls1 ->
TCBList_P y l2 rtbl tls2 ->
TCBList_P x (l1 ++ l2) rtbl tcbls.
Lemma prio_in_tbl_orself :
forall prio v´37 vx,
prio_in_tbl prio
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) v´37
(Vint32 (Int.or vx ($ 1<<(prio&$ 7))))).
Lemma prio_notin_tbl_orself :
forall prio v´37 vx,
Int.unsigned prio < 64 ->
nth_val (Z.to_nat(Int.unsigned (Int.shru prio ($ 3)))) v´37 = Some (Vint32 vx) ->
~ prio_not_in_tbl prio
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) v´37
(Vint32 (Int.or vx ($ 1<<(prio&$ 7))))).
Lemma TCBList_P_post_msg:
forall v´42 v´48 v´47 v´60 v´50 v´37 v´59 v´49 v´44 v´63 v´64 v´65 v´51 v´52 v´53 v´54 v´55 v´56 x00 v´58 v´40 v´38 prio st msg v´7 v´62 v´43 v´36 v´39 v´13 vhold,
Int.unsigned v´38 <= 7 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
prio_in_tbl ((v´38<<$ 3)+ᵢv´39) v´13 ->
RL_RTbl_PrioTbl_P v´13 v´36 vhold->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero) ->
R_PrioTbl_P v´36 v´7 vhold->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
TcbMod.join v´44 v´43 v´7 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
get_last_tcb_ptr v´48 v´42 = Some (Vptr (v´58, Int.zero)) ->
TCBList_P v´42 v´48 v´37 v´47 ->
TCBList_P v´60 v´50 v´37 v´59 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´59 v´49 ->
TcbMod.join v´47 v´49 v´44 ->
TCBNode_P
(v´60
:: v´63
:: v´64
:: v´65
:: Vint32 v´51
:: V$OS_STAT_Q
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil) v´37
(prio, st, msg) ->
TCBList_P v´42
(v´48 ++
(v´60
:: v´63
:: Vnull
:: Vptr x00
:: V$0
:: Vint32 ($ OS_STAT_Q&Int.not ($ OS_STAT_Q))
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil) :: v´50)
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
(TcbMod.set v´44 (v´58, Int.zero)
(prio, rdy , Vptr x00)).
Lemma rl_tbl_grp_p_set_hold´:
forall v´12 v´38 v´37 v´57 v´69 v´39 v´36 v´13 v´58 v´40 v´41,
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P v´37 (Vint32 v´57) ->
RL_Tbl_Grp_P (update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
(Vint32 (Int.or v´57 v´41)).
Lemma r_priotbl_p_set_hold:
forall v´7 prio st msg v´36 tid x y vhold,
R_PrioTbl_P v´36 v´7 vhold->
TcbMod.get v´7 tid = Some (prio, st, msg) ->
R_PrioTbl_P v´36
(TcbMod.set v´7 tid
(prio, x, y)) vhold.
Lemma rl_tbl_grp_p_set_hold´´
: forall (v´12 v´38 : int32) (v´13 : vallist)
(v´69 v´39 : int32) (v´36 : list val) (v´58 : block)
(v´40 v´41 : int32),
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
Int.eq (v´69&Int.not v´40) Int.zero = false->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) (Vint32 v´12).
Lemma rl_rtbl_priotbl_p_hold:
forall v´36 v´12 v´13 v´38 v´69 v´39 v´58 v´40 v´41 v´57 v´37 vhold,
(v´58, Int.zero) <> vhold ->
RL_RTbl_PrioTbl_P v´37 v´36 vhold->
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P v´37 (Vint32 v´57) ->
Int.unsigned v´57 <= 255 ->
array_type_vallist_match Tint8 v´37 ->
length v´37 = nat_of_Z OS_RDY_TBL_SIZE ->
RL_RTbl_PrioTbl_P
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
v´36 vhold.
Lemma prio_wt_inq_convert:
forall pri vx,
PrioWaitInQ pri vx <->
PrioWaitInQ (Int.unsigned ($ pri)) vx /\ 0 <= pri < 64.
Lemma prio_wt_inq_tid_neq:
forall prio´ v´13 v´69 prio,
nth_val´ (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) v´13 = Vint32 v´69 ->
Int.unsigned prio < 64 ->
(PrioWaitInQ (Int.unsigned prio´)
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) v´13
(Vint32 (v´69&Int.not ($ 1<< (prio & $7))))) <->
PrioWaitInQ (Int.unsigned prio´) v´13 /\ prio´ <> prio).
Lemma wtset_notnil_msgls_nil:
forall x1 x0 x ,
x1 <> nil ->
RH_ECB_P (absmsgq x x0, x1) -> x = nil.
Lemma rl_tbl_grp_neq_zero:
forall v´12 px v´13 v´69,
Int.unsigned px < 8 ->
Int.unsigned v´12 <= 255 ->
v´12 <> $ 0 ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 px ->
nth_val´ (Z.to_nat (Int.unsigned px)) v´13 = Vint32 v´69 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
v´69 <> $ 0.
Lemma ECBList_P_Set_Rdy_hold:
forall a tcbls tid prio msg msg´ x y b c eid nl,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_q eid) nl, msg) ->
EcbMod.get c eid = None ->
ECBList_P x y a b c tcbls ->
ECBList_P x y a b c (TcbMod.set tcbls tid (prio,rdy,msg´)).
Lemma ecblist_p_post_exwt_hold:
forall v´36 v´12 v´13 v´38 v´69 v´39 v´58 v´40 v´32 v´15 v´24 v´35 v´16
v´18 v´19 v´20 v´34 v´21 v´22 v´23 v´25 v´26 v´27 x x0 x1 v´0 v´1
v´5 v´6 v´7 x00 v´11 v´31 v´30 v´29 v´10 v´9 prio v´62 st msg y vhold,
RL_RTbl_PrioTbl_P v´13 v´36 vhold->
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_Q
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DMsgQ (Vptr (v´24, Int.zero))
(v´16
:: v´18
:: v´19
:: v´20
:: v´34
:: Vint32 v´21
:: Vint32 v´22 :: Vptr (v´23, Int.zero) :: nil)
(v´26 :: v´25 :: nil) v´27) (absmsgq x x0, x1)->
ECBList_P v´0 Vnull v´1 v´5 v´6 v´7 ->
ECBList_P v´29 (Vptr (v´32, Int.zero)) v´30 v´31 v´9 v´7 ->
EcbMod.joinsig (v´32, Int.zero) (absmsgq x x0, x1) v´6 v´10 ->
EcbMod.join v´9 v´10 v´11 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
R_PrioTbl_P v´36 v´7 vhold ->
x1 <> nil ->
ECBList_P v´29 Vnull
(v´30 ++
((V$OS_EVENT_TYPE_Q
:: Vint32 y
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) :: nil) ++ v´1)
(v´31 ++
(DMsgQ (Vptr (v´24, Int.zero))
(v´16
:: v´18
:: v´19
:: v´20
:: v´34
:: Vint32 v´21
:: Vint32 v´22 :: Vptr (v´23, Int.zero) :: nil)
(v´26 :: v´25 :: nil) v´27 :: nil) ++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(absmsgq nil x0, remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero)
(prio, rdy , Vptr x00))
.
Lemma ecblist_p_post_exwt_hold´:
forall (v´36 : vallist) (v´12 : int32) (v´13 : vallist)
(v´38 v´69 v´39 : int32) (v´58 : block) (v´40 v´41 : int32)
(v´32 : block) (v´15 : int32) (v´24 : block)
(v´35 v´16 v´18 v´19 v´20 v´34 : val) (v´21 v´22 : int32)
(v´23 : block) (v´25 v´26 : val) (v´27 : vallist)
(x : list msg) (x0 : maxlen) (x1 : waitset)
(v´0 : val) (v´1 : list EventCtr) (v´5 : list EventData)
(v´6 : EcbMod.map) (v´7 : TcbMod.map) (x00 : addrval)
(v´11 : EcbMod.map) (v´31 : list EventData)
(v´30 : list EventCtr) (v´29 : val) (v´10 v´9 : EcbMod.map)
(prio : priority) v´62 st msg vhold,
RL_RTbl_PrioTbl_P v´13 v´36 vhold->
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_Q
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DMsgQ (Vptr (v´24, Int.zero))
(v´16
:: v´18
:: v´19
:: v´20
:: v´34
:: Vint32 v´21
:: Vint32 v´22 :: Vptr (v´23, Int.zero) :: nil)
(v´26 :: v´25 :: nil) v´27) (absmsgq x x0, x1)->
ECBList_P v´0 Vnull v´1 v´5 v´6 v´7 ->
ECBList_P v´29 (Vptr (v´32, Int.zero)) v´30 v´31 v´9 v´7 ->
EcbMod.joinsig (v´32, Int.zero) (absmsgq x x0, x1) v´6 v´10 ->
EcbMod.join v´9 v´10 v´11 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
R_PrioTbl_P v´36 v´7 vhold->
x1 <> nil ->
ECBList_P v´29 Vnull
(v´30 ++
((V$OS_EVENT_TYPE_Q
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) :: nil) ++ v´1)
(v´31 ++
(DMsgQ (Vptr (v´24, Int.zero))
(v´16
:: v´18
:: v´19
:: v´20
:: v´34
:: Vint32 v´21
:: Vint32 v´22 :: Vptr (v´23, Int.zero) :: nil)
(v´26 :: v´25 :: nil) v´27 :: nil) ++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(absmsgq nil x0, remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero)
(prio, rdy , Vptr x00)).
Lemma rh_curtcb_set_nct:
forall v´8 v´7 x tid ,
RH_CurTCB v´8 v´7 ->
v´8 <> tid ->
RH_CurTCB v´8
(TcbMod.set v´7 tid
x).
Lemma tidneq_inwt_in:
forall x1 tid tid0,
tid <> tid0 ->
(In tid0 (remove_tid tid x1) <->
In tid0 x1).
Lemma tid_in_rmwt_in :
forall x1 tid,
In tid (remove_tid tid x1) ->
In tid x1.
Lemma in_wtset_rm_notin:
forall x1 tid,
In tid x1 ->
~ In tid (remove_tid tid x1).
Lemma rh_tcblist_ecblist_p_post_exwt:
forall v´8 tid v´11 v´7 v´9 v´10 eid x x0 x1 v´6 prio msg x00 xl,
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmsgq x x0, x1) v´6 v´10 ->
In tid x1 ->
TcbMod.get v´7 tid = Some (prio, wait (os_stat_q eid) xl, msg) ->
RH_TCBList_ECBList_P
(EcbMod.set v´11 eid
(absmsgq nil x0, remove_tid tid x1))
(TcbMod.set v´7 tid
(prio, rdy , Vptr x00)) v´8.
Lemma qpost_ovf_prop:
forall i2 i1 x13 x12 x6 x7 x8 v´49 v´47 x14 x15 x x1 x2 v2,
true = Int.ltu i2 i1 ->
WellformedOSQ
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x x1, x2) ->
Z.ge (Z_of_nat (length x)) (Int.unsigned x1).
Lemma qpost_ovf_prop´:
forall i2 i1 x13 x12 x6 x7 x8 v´49 v´47 x14 x15 x x1 x2 v2,
true = Int.eq i1 i2 ->
WellformedOSQ
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x x1, x2) ->
Z.ge (Z_of_nat (length x)) (Int.unsigned x1).
Lemma osq_same_blk_st_in´:
forall (qptr qst qend qin qout qsz qen : val) (b : block) (i : int32),
WellformedOSQ
(qptr :: qst :: qend :: qin :: qout :: qsz :: qen :: Vptr (b, i) :: nil) ->
exists i´, qin = Vptr (b, i´).
Lemma wellq_in_props:
forall (x12 x11 x5 x6 : val) (v´49 : block) (x i2 i1 : int32)
(v´47 : block) (x13 x14 : val) (v2 : list val)
(v´46 : absecb.B),
length v2 = ∘OS_MAX_Q_SIZE ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x12
:: x11
:: x5
:: Vptr (v´49, x)
:: x6
:: Vint32 i2 :: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x13 :: x14 :: nil) v2) v´46 ->
WellformedOSQ
(x12
:: x11
:: x5
:: Vptr (v´49, x)
:: x6
:: Vint32 i2 :: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero)) <= Int.unsigned x /\
4 * ((Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4) =
Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero)) /\
(Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4 < 20 /\
(Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4 <
Z.of_nat (length v2).
Lemma wellformedosq_size_add_1:
forall x13 x12 x6 v´49 x x8 i2 i1,
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) -> Int.unsigned (i2+ᵢ$ 1) <= Int16.max_unsigned.
Lemma wellformedosq_ens_add_1:
forall x13 x12 x6 v´49 x x8 i2 i1 x10 x11 v´46 v2 v´36,
length v2 = ∘OS_MAX_Q_SIZE ->
RLH_ECBData_P
(DMsgQ (Vptr (v´36, Int.zero))
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x10 :: x11 :: nil) v2) v´46 ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) -> Int.unsigned (i1+ᵢ$ 1) <= Int16.max_unsigned.
Lemma rlh_ecb_nowait_prop:
forall v´25 i i3 v´47 x4 v´42 v´40 v´35 v´34 x1 x2 x3 v´37,
RL_Tbl_Grp_P v´40 (Vint32 i)->
R_ECB_ETbl_P (v´25, Int.zero)
(V$OS_EVENT_TYPE_Q
:: Vint32 i
:: Vint32 i3 :: Vptr (v´47, Int.zero) :: x4 :: v´42 :: nil,
v´40) v´35 ->
EcbMod.get v´34 (v´25, Int.zero) = Some (absmsgq x1 x2, x3) ->
RH_TCBList_ECBList_P v´34 v´35 v´37 ->
Int.eq i ($ 0) = true ->
x3 = nil.
Lemma qpost_no_wait_prop´:
forall i2 i1 x13 x12 x6 x7 x8 v´49 v´47 x14 x15 x x1 x2 v2,
Int.ltu i1 i2 = true ->
WellformedOSQ
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x x1, x2) ->
Z.of_nat (length x) < (Int.unsigned x1) .
Lemma get_wellformedosq_in_setst:
forall i1 i2 x13 x12 x6 v´49 x x8,
Int.ltu i1 i2 = true ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
val_inj
match x6 with
| Vundef => None
| Vnull => Some (Vint32 Int.zero)
| Vint32 _ => None
| Vptr (b2, ofs2) =>
if peq v´49 b2
then
if Int.eq (x+ᵢInt.mul ($ 1) ($ 4)) ofs2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
else Some (Vint32 Int.zero)
end <> Vint32 Int.zero ->
WellformedOSQ
(x13
:: x12
:: x6
:: x12
:: x8
:: Vint32 i2
:: Vint32 (i1+ᵢ$ 1) :: Vptr (v´49, Int.zero) :: nil).
Lemma msgqlist_p_compose´
: forall (p : val) (qid : addrval) (mqls : EcbMod.map)
(qptrl1 qptrl2 : list EventCtr) (i i1 : int32)
(a : addrval) (x3 p´ : val) (v´41 : vallist)
(msgqls1 msgqls2 : list EventData) (msgq : EventData)
(mqls1 mqls2 : EcbMod.map) (mq : absecb.B)
(mqls´ : EcbMod.map) (tcbls : TcbMod.map),
R_ECB_ETbl_P qid
(V$OS_EVENT_TYPE_Q
:: Vint32 i :: Vint32 i1 :: Vptr a :: x3 :: p´ :: nil, v´41) tcbls ->
ECBList_P p (Vptr qid) qptrl1 msgqls1 mqls1 tcbls ->
ECBList_P p´ Vnull qptrl2 msgqls2 mqls2 tcbls ->
RLH_ECBData_P msgq mq ->
EcbMod.joinsig qid mq mqls2 mqls´ ->
EcbMod.join mqls1 mqls´ (EcbMod.set mqls qid mq) ->
ECBList_P p Vnull
(qptrl1 ++
((V$OS_EVENT_TYPE_Q
:: Vint32 i :: Vint32 i1 :: Vptr a :: x3 :: p´ :: nil, v´41)
:: nil) ++ qptrl2) (msgqls1 ++ (msgq :: nil) ++ msgqls2) (EcbMod.set mqls qid mq)
tcbls.
Lemma rlh_ecbdata_in_end:
forall i1 i2 x13 x12 v´49 x x8 v´47 x14 x15 v2 x1 x2 x0,
Int.ltu i1 i2 = true ->
length v2 = ∘OS_MAX_Q_SIZE ->
WellformedOSQ
(x13
:: x12
:: Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4)) )
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4)) )
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x1 x2, nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: Vptr (v´49, x+ᵢInt.mul ($ 1) ($ 4))
:: x12
:: x8
:: Vint32 i2
:: Vint32 (i1+ᵢ$ 1) :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil)
(update_nth_val
(Z.to_nat
((Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) /
4)) v2 (Vptr x0))) (absmsgq (x1 ++ (Vptr x0::nil)) x2, nil).
Lemma rh_tcbls_mqls_p_setmsg_hold:
forall (mqls : EcbMod.map) (tcbls : TcbMod.map) (ct : tid)
(a : tidspec.A) (v : msg) (vl : list msg) (qmax : maxlen)
(wl : waitset),
RH_TCBList_ECBList_P mqls tcbls ct ->
EcbMod.get mqls a = Some (absmsgq vl qmax, wl) ->
RH_TCBList_ECBList_P (EcbMod.set mqls a (absmsgq (vl++v::nil) qmax, wl)) tcbls ct.
Lemma get_wellformedosq_in_setst´:
forall i1 i2 x13 x12 x6 v´49 x x8,
x6 <> Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4))) ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x+ᵢInt.mul ($ 1) ($ 4))
:: x8
:: Vint32 i2
:: Vint32 (i1+ᵢ$ 1) :: Vptr (v´49, Int.zero) :: nil).
Lemma rlh_ecbdata_in_noend:
forall i1 i2 x13 x12 v´49 x x8 v´47 x14 x15 v2 x1 x2 x0 x6,
x6 <> Vptr (v´49, x+ᵢInt.mul ($ 1) ($ 4)) ->
Int.ltu i1 i2 = true ->
length v2 = ∘OS_MAX_Q_SIZE ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x1 x2, nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: Vptr (v´49, x+ᵢInt.mul ($ 1) ($ 4))
:: x8
:: Vint32 i2
:: Vint32 (i1+ᵢ$ 1) :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil)
(update_nth_val
(Z.to_nat
((Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) /
4)) v2 (Vptr x0))) (absmsgq (x1++ (Vptr x0 :: nil)) x2, nil).
Lemma prio_in_rtbl_hold:
forall rtbl x y prio,
Int.unsigned prio < 64 ->
Int.unsigned x <= 7 ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u rtbl ->
prio_in_tbl prio rtbl ->
prio_in_tbl prio
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 y)))).
Lemma idle_in_rtbl_hold´:
forall rtbl x y,
Int.unsigned x <= 7 ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u rtbl ->
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
prio_in_tbl ($ OS_IDLE_PRIO)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 y)))).
Lemma get_tcb_stat:
forall p etbl ptbl tid tcbls abstcb tcbls´ vl rtbl qid vle vhold,
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u etbl ->
length etbl = ∘OS_EVENT_TBL_SIZE ->
prio_in_tbl p etbl ->
nth_val´ (Z.to_nat (Int.unsigned p)) ptbl = Vptr tid ->
R_PrioTbl_P ptbl tcbls vhold ->
TcbJoin tid abstcb tcbls´ tcbls ->
TCBNode_P vl rtbl abstcb ->
R_ECB_ETbl_P qid
(V$OS_EVENT_TYPE_Q
::vle,
etbl) tcbls ->
V_OSTCBStat vl = Some (Vint32 (Int.repr OS_STAT_Q)).
Lemma rh_tcblist_ecblist_p_post_exwt_aux:
forall (v´8 tid0 : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) (x : list msg)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
st,
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmsgq x x0, x1) v´6 v´10 ->
In tid0 x1 ->
TcbMod.get v´7 tid0 = Some (prio, st, msg0) ->
exists xl, st = wait (os_stat_q eid) xl.
Lemma statq_and_not_statq_eq_rdy:
Int.eq ($ OS_STAT_Q&Int.not ($ OS_STAT_Q)) ($ OS_STAT_RDY) = true.
Require Import lab.
Lemma qpost_absinfer_null:
forall P vl,
can_change_aop P ->
absinfer
( <|| qpost (Vnull :: vl) ||> **
P) (<|| END Some (V$OS_ERR_PEVENT_NULL) ||> **
P).
Lemma qpost_absinfer_msg_null:
forall P v,
can_change_aop P ->
absinfer
( <|| qpost (v :: Vnull ::nil) ||> **
P) (<|| END Some (Vint32 (Int.repr OS_ERR_POST_NULL_PTR)) ||> **
P).
Lemma qpost_absinfer_no_q:
forall P mqls x v,
can_change_aop P ->
(~ exists a b wl,EcbMod.get mqls x = Some (absmsgq a b,wl)) ->
absinfer
( <|| qpost (Vptr x :: v :: nil) ||> **
HECBList mqls ** P)
(<|| END Some (Vint32 (Int.repr MSGQ_NULL_ERR)) ||> ** HECBList mqls ** P).
Lemma qpost_absinfer_ovf:
forall P mqls x v a b wl,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq a b,wl) ->
Z.ge (Z_of_nat (length a)) (Int.unsigned b) ->
absinfer
( <|| qpost (Vptr x :: v :: nil) ||> **
HECBList mqls ** P)
(<|| END Some (Vint32 (Int.repr MSGQ_OVF_ERR)) ||> ** HECBList mqls ** P).
Lemma qpost_absinfer_nowt_succ:
forall P mqls x v a b tcbls t ct,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq a b,nil) ->
Z.lt (Z_of_nat (length a)) (Int.unsigned b) ->
absinfer
( <|| qpost (Vptr x :: v :: nil) ||> **
HECBList mqls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END Some (Vint32 (Int.repr NO_ERR)) ||> ** HECBList (EcbMod.set mqls x (absmsgq (a++(v::nil)) b,nil))** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma qpost_absinfer_exwt_succ:
forall P mqls x v n wl tls t ct p st m t´ vl,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq vl n,wl) ->
~ wl=nil ->
GetHWait tls wl t´ ->
TcbMod.get tls t´ = Some (p,st,m) ->
absinfer
( <|| qpost (Vptr x :: v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| isched ;; END Some (Vint32 (Int.repr NO_ERR)) ||> ** HECBList (EcbMod.set mqls x (absmsgq nil n,(remove_tid t´ wl))) ** HTCBList (TcbMod.set tls t´ (p,rdy ,v) ) ** HTime t ** HCurTCB ct ** P).
Open Scope code_scope.
Lemma Astruct_OSTCB_PV_ptr_neq :
forall s b p2 v1 l v2 P,
s |= Astruct (b, Int.zero) OS_TCB (v1::l) ** PV p2 @ Int8u |-> v2 ** P ->
(b, Int.zero) <> p2.
Lemma event_type_n_match´:
forall s P i1 i0 i2 x2 x3 v´42 i10,
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil)
(DMbox i10) ** P ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = true ->
False.
Lemma event_type_n_match´´:
forall s P i1 i0 i2 x2 x3 v´42 i10 x,
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil)
(DMutex i10 x) ** P ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = true ->
False.
Lemma event_type_n_match:
forall s P i1 i0 i2 x2 x3 v´42 i10,
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil)
(DSem i10) ** P ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = true ->
False.
Lemma isptr_zh :
forall x, isptr x ->
match x with
| Vundef => false
| Vnull => true
| Vint32 _ => false
| Vptr _ => true
end = true.
Require Import OSTimeDlyPure.
Require Import OSQAcceptPure.
Lemma ecbmod_absmsgq:
forall a x y z b,
RLH_ECBData_P
(DMsgQ a x y z) b -> exists vl n wl, b = (absmsgq vl n, wl).
Lemma post_exwt_succ_pre:
forall v´36 v´13 v´12 v´32 v´15 v´24 v´35 v´0 v´8 v´9 v´11 x x0 x1 v´6 v´10 v´38 v´69 v´39 v´58 a b c v´62 v´7 vhold,
v´12 <> Int.zero ->
R_PrioTbl_P v´36 v´7 vhold ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_Q
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig (v´32, Int.zero) (absmsgq x x0, x1) v´6 v´10 ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
TcbJoin (v´58, Int.zero) (a,b,c) v´62 v´7 ->
x1<>nil /\ GetHWait v´7 x1 (v´58,Int.zero) /\ TcbMod.get v´7 (v´58,Int.zero) = Some (a,b,c).
Lemma prio_set_rdy_in_tbl:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_in_tbl prio0 rtbl ->
prio_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7))))).
Lemma prio_set_rdy_in_tbl_rev:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7))))) ->
prio_in_tbl prio0 rtbl.
Lemma prio_set_rdy_not_in_tbl:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_not_in_tbl prio0 rtbl ->
prio_not_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7))))).
Lemma prio_set_rdy_not_in_tbl_rev:
forall prio0 prio rtbl grp,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
prio_not_in_tbl prio0
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7))))) ->
prio_not_in_tbl prio0 rtbl.
Module new_rtbl.
Definition set_rdy p rtbl :=
update_nth_val ∘(Int.unsigned (Int.shru p ($ 3))) rtbl
(val_inj (or (nth_val´ (Z.to_nat (Int.unsigned (Int.shru p ($ 3)))) rtbl)
(Vint32 ($ 1<<(p&$ 7))))).
Lemma trans_lemma_1:
forall p grp rtbl,
nth_val (Z.to_nat (Int.unsigned (Int.shru p ($ 3)))) rtbl = Some (Vint32 grp) ->
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned (Int.shru p ($ 3)))) rtbl)
(Vint32 ($ 1<<(p&$ 7))))) =
(Vint32 (Int.or grp ($ 1<<(p&$ 7)))).
Lemma prio_set_rdy_in_tbl_lemma_1:
forall rtbl p,
0<= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
(exists v, nth_val (Z.to_nat (Int.unsigned (Int.shru p ($ 3)))) rtbl = Some (Vint32 v)).
Lemma prio_set_rdy_in_tbl:
forall p0 p rtbl,
0 <= Int.unsigned p0 < 64 ->
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
p0 <> p ->
prio_in_tbl p0 rtbl ->
prio_in_tbl p0 (set_rdy p rtbl).
Lemma prio_set_rdy_in_tbl_rev:
forall p0 p rtbl,
0 <= Int.unsigned p0 < 64 ->
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
p0 <> p ->
prio_in_tbl p0 (set_rdy p rtbl) ->
prio_in_tbl p0 rtbl.
Lemma prio_set_rdy_not_in_tbl:
forall p0 p rtbl,
0 <= Int.unsigned p0 < 64 ->
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
p0 <> p ->
prio_not_in_tbl p0 rtbl ->
prio_not_in_tbl p0 (set_rdy p rtbl).
Lemma prio_set_rdy_not_in_tbl_rev:
forall p0 p rtbl,
0 <= Int.unsigned p0 < 64 ->
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
p0 <> p ->
prio_not_in_tbl p0 (set_rdy p rtbl) ->
prio_not_in_tbl p0 rtbl.
End new_rtbl.
Lemma RdyTCBblk_rtbl_add:
forall prio0 prio rtbl grp vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RdyTCBblk vl rtbl prio0 ->
RdyTCBblk vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
prio0.
Lemma RLH_RdyI_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_RdyI_P vl rtbl (prio0, stat, msg) ->
RLH_RdyI_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_RdyI_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_RdyI_P vl rtbl (prio0, stat, msg) ->
RHL_RdyI_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma WaitTCBblk_rtbl_add:
forall prio0 prio rtbl grp vl t,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
WaitTCBblk vl rtbl prio0 t->
WaitTCBblk vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
prio0 t.
Lemma WaitTCBblk_rtbl_add_rev:
forall prio0 prio rtbl grp vl t,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
WaitTCBblk vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
prio0 t ->
WaitTCBblk vl rtbl prio0 t.
Lemma RLH_Wait_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_Wait_P vl rtbl (prio0, stat, msg) ->
RLH_Wait_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_WaitS_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_WaitS_P vl rtbl (prio0, stat, msg) ->
RLH_WaitS_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_WaitQ_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_WaitQ_P vl rtbl (prio0, stat, msg) ->
RLH_WaitQ_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_WaitMB_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_WaitMB_P vl rtbl (prio0, stat, msg) ->
RLH_WaitMB_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_WaitMS_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_WaitMS_P vl rtbl (prio0, stat, msg) ->
RLH_WaitMS_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RLH_Wait_all_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_TCB_Status_Wait_P vl rtbl (prio0, stat, msg) ->
RLH_TCB_Status_Wait_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_Wait_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_Wait_P vl rtbl (prio0, stat, msg) ->
RHL_Wait_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_WaitS_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_WaitS_P vl rtbl (prio0, stat, msg) ->
RHL_WaitS_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_WaitQ_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_WaitQ_P vl rtbl (prio0, stat, msg) ->
RHL_WaitQ_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_WaitMB_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_WaitMB_P vl rtbl (prio0, stat, msg) ->
RHL_WaitMB_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_WaitMS_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_WaitMS_P vl rtbl (prio0, stat, msg) ->
RHL_WaitMS_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma RHL_Wait_all_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_TCB_Status_Wait_P vl rtbl (prio0, stat, msg) ->
RHL_TCB_Status_Wait_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma R_TCB_Status_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
R_TCB_Status_P vl rtbl (prio0, stat, msg) ->
R_TCB_Status_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma TCBNode_P_rtbl_add:
forall prio0 prio rtbl grp stat msg vl,
0 <= Int.unsigned prio0 < 64 ->
0 <= Int.unsigned prio < 64 ->
prio0 <> prio ->
V_OSTCBPrio vl = Some (Vint32 prio0) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
TCBNode_P vl rtbl (prio0, stat, msg) ->
TCBNode_P vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio&$ 7)))))
(prio0, stat, msg).
Lemma TCBNode_P_prio:
forall vl rtbl p t m,
TCBNode_P vl rtbl (p, t, m) ->
0 <= Int.unsigned p < 64 /\ V_OSTCBPrio vl = Some (Vint32 p).
Lemma TCBList_P_rtbl_add_simpl_version:
forall vl vptr rtbl tcbls prio grp,
0<= Int.unsigned prio < 64 ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
(forall tid p s m , TcbMod.get tcbls tid = Some (p,s,m) -> p <> prio
) ->
TCBList_P vptr vl rtbl tcbls ->
TCBList_P vptr vl
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio &$ 7)))))
tcbls.
Lemma TCBList_P_rtbl_add_lemma_1a:
forall ma mb mab mc ma´ ma´´ p s m tid,
TcbMod.join ma mb mab ->
TcbMod.join mc ma´ ma ->
TcbJoin tid (p, s, m) ma´´ ma´ ->
TcbMod.get mb tid = None.
Lemma get_get_neq:
forall m tid v1 v2 tid´,
TcbMod.get m tid = v1 ->
TcbMod.get m tid´ = v2 ->
v1 <> v2 ->
tid <> tid´.
Lemma TCBList_P_rtbl_add_lemma_1:
forall ma mb mab´ mab mc ma´ ma´´ prio st msg tid,
TcbMod.join ma mb mab ->
TcbMod.join mc ma´ ma ->
TcbJoin tid (prio, st, msg) ma´´ ma´ ->
TcbJoin tid (prio, st, msg) mab´ mab ->
R_Prio_No_Dup mab ->
(forall tid´ p s m,
TcbMod.get mb tid´ = Some (p, s, m) -> p <> prio).
Lemma TCBList_P_rtbl_add_lemma_2a:
forall ertbl ptbl tcbl tcbl´ tid px py prio bitx st msg mab´ mab vhold,
Int.unsigned py <= 7 ->
Int.unsigned px <= 7 ->
RL_RTbl_PrioTbl_P ertbl ptbl vhold->
nth_val´ (Z.to_nat (Int.unsigned ((py<<$ 3)+ᵢpx))) ptbl = Vptr tid ->
TcbJoin tid (prio, st, msg) tcbl´ tcbl ->
R_PrioTbl_P ptbl mab vhold->
TcbJoin tid (prio, st, msg) mab´ mab ->
nth_val´ (Z.to_nat (Int.unsigned px)) OSMapVallist = Vint32 bitx ->
prio = ((py<<$ 3)+ᵢpx) /\
0 <= Int.unsigned prio < 64 /\
px = prio &$ 7 /\
py = Int.shru prio ($ 3) /\
bitx = $ 1<<px.
Lemma TCBList_P_rtbl_add_lemma_2:
forall prio px py bitx grp rtbl vl vptr tcbls,
0 <= Int.unsigned prio < 64 ->
py = Int.shru prio ($ 3) ->
px = prio &$ 7 ->
bitx = $ 1<<px ->
Int.unsigned py <= 7 ->
Int.unsigned px <= 7 ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
TCBList_P vptr vl
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) rtbl
(Vint32 (Int.or grp ($ 1<<(prio &$ 7)))))
tcbls
->
TCBList_P vptr vl
(update_nth_val (Z.to_nat (Int.unsigned py)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned py)) rtbl) (Vint32 bitx))))
tcbls.
Lemma nth_val´2nth_val:
forall n rtbl x,
nth_val´ n rtbl = Vint32 x ->
nth_val n rtbl = Some (Vint32 x).
Lemma TCBList_P_rtbl_add_lemma_main:
forall px py bitx ertbl (ma mb mab mc ma´ ma´´ mab´:TcbMod.map) ptbl prio st msg tid vptr vl rtbl vhold,
Int.unsigned py <= 7 ->
Int.unsigned px <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned px)) OSMapVallist = Vint32 bitx ->
RL_RTbl_PrioTbl_P ertbl ptbl vhold->
nth_val´ (Z.to_nat (Int.unsigned ((py<<$ 3)+ᵢpx))) ptbl = Vptr tid ->
R_PrioTbl_P ptbl mab vhold->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
TcbMod.join ma mb mab ->
TcbMod.join mc ma´ ma ->
TcbJoin tid (prio, st, msg) ma´´ ma´ ->
TcbJoin tid (prio, st, msg) mab´ mab ->
TCBList_P vptr vl rtbl mb ->
TCBList_P vptr vl
(update_nth_val (Z.to_nat (Int.unsigned py)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned py)) rtbl) (Vint32 bitx))))
mb.
Lemma TCBList_P_rtbl_add:
forall v´47 v´36 v´38 v´39 v´40 v´13 v´44 v´43 v´7 v´8 v´45 v´58 v´59 v´49 v´62 v´37 prio st msg vhold,
Int.unsigned v´38 <= 7 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
prio_in_tbl ((v´38<<$ 3)+ᵢv´39) v´13 ->
RL_RTbl_PrioTbl_P v´13 v´36 vhold->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero) ->
R_PrioTbl_P v´36 v´7 vhold->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
TcbMod.join v´44 v´43 v´7 ->
TcbMod.join v´47 v´49 v´44 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´59 v´49 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
TCBList_P v´8 v´45 v´37 v´43 ->
TCBList_P v´8 v´45
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
v´43.
Lemma rl_tbl_grp_p_set_hold:
forall v´12 v´38 v´13 v´69 v´39 v´36 v´58 v´40 v´41,
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
Int.eq (v´69&Int.not v´40) Int.zero = true ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) (Vint32 (v´12&Int.not v´41)).
Lemma get_last_tcb_ptr_prop:
forall l1 a x1 x z,
V_OSTCBNext a = Some x1 ->
get_last_tcb_ptr l1 x1 = Some x ->
get_last_tcb_ptr (a :: l1) z = Some x.
Lemma TCBList_P_Split:
forall l1 x l2 rtbl tcbls,
TCBList_P x (l1 ++ l2) rtbl tcbls ->
exists y tls1 tls2,
get_last_tcb_ptr l1 x = Some y /\
TcbMod.join tls1 tls2 tcbls /\
TCBList_P x l1 rtbl tls1 /\
TCBList_P y l2 rtbl tls2.
Lemma get_last_tcb_ptr_prop´:
forall l1 a x1 x z,
l1 <> nil ->
V_OSTCBNext a = Some x1 ->
get_last_tcb_ptr (a :: l1) z = Some x->
get_last_tcb_ptr l1 x1 = Some x.
Lemma TCBList_P_Combine:
forall l1 x l2 rtbl y tls1 tls2 tcbls,
get_last_tcb_ptr l1 x = Some y ->
TcbMod.join tls1 tls2 tcbls ->
TCBList_P x l1 rtbl tls1 ->
TCBList_P y l2 rtbl tls2 ->
TCBList_P x (l1 ++ l2) rtbl tcbls.
Lemma prio_in_tbl_orself :
forall prio v´37 vx,
prio_in_tbl prio
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) v´37
(Vint32 (Int.or vx ($ 1<<(prio&$ 7))))).
Lemma prio_notin_tbl_orself :
forall prio v´37 vx,
Int.unsigned prio < 64 ->
nth_val (Z.to_nat(Int.unsigned (Int.shru prio ($ 3)))) v´37 = Some (Vint32 vx) ->
~ prio_not_in_tbl prio
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) v´37
(Vint32 (Int.or vx ($ 1<<(prio&$ 7))))).
Lemma TCBList_P_post_msg:
forall v´42 v´48 v´47 v´60 v´50 v´37 v´59 v´49 v´44 v´63 v´64 v´65 v´51 v´52 v´53 v´54 v´55 v´56 x00 v´58 v´40 v´38 prio st msg v´7 v´62 v´43 v´36 v´39 v´13 vhold,
Int.unsigned v´38 <= 7 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
prio_in_tbl ((v´38<<$ 3)+ᵢv´39) v´13 ->
RL_RTbl_PrioTbl_P v´13 v´36 vhold->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero) ->
R_PrioTbl_P v´36 v´7 vhold->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
TcbMod.join v´44 v´43 v´7 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
get_last_tcb_ptr v´48 v´42 = Some (Vptr (v´58, Int.zero)) ->
TCBList_P v´42 v´48 v´37 v´47 ->
TCBList_P v´60 v´50 v´37 v´59 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´59 v´49 ->
TcbMod.join v´47 v´49 v´44 ->
TCBNode_P
(v´60
:: v´63
:: v´64
:: v´65
:: Vint32 v´51
:: V$OS_STAT_Q
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil) v´37
(prio, st, msg) ->
TCBList_P v´42
(v´48 ++
(v´60
:: v´63
:: Vnull
:: Vptr x00
:: V$0
:: Vint32 ($ OS_STAT_Q&Int.not ($ OS_STAT_Q))
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil) :: v´50)
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
(TcbMod.set v´44 (v´58, Int.zero)
(prio, rdy , Vptr x00)).
Lemma rl_tbl_grp_p_set_hold´:
forall v´12 v´38 v´37 v´57 v´69 v´39 v´36 v´13 v´58 v´40 v´41,
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P v´37 (Vint32 v´57) ->
RL_Tbl_Grp_P (update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
(Vint32 (Int.or v´57 v´41)).
Lemma r_priotbl_p_set_hold:
forall v´7 prio st msg v´36 tid x y vhold,
R_PrioTbl_P v´36 v´7 vhold->
TcbMod.get v´7 tid = Some (prio, st, msg) ->
R_PrioTbl_P v´36
(TcbMod.set v´7 tid
(prio, x, y)) vhold.
Lemma rl_tbl_grp_p_set_hold´´
: forall (v´12 v´38 : int32) (v´13 : vallist)
(v´69 v´39 : int32) (v´36 : list val) (v´58 : block)
(v´40 v´41 : int32),
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
Int.eq (v´69&Int.not v´40) Int.zero = false->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) (Vint32 v´12).
Lemma rl_rtbl_priotbl_p_hold:
forall v´36 v´12 v´13 v´38 v´69 v´39 v´58 v´40 v´41 v´57 v´37 vhold,
(v´58, Int.zero) <> vhold ->
RL_RTbl_PrioTbl_P v´37 v´36 vhold->
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P v´37 (Vint32 v´57) ->
Int.unsigned v´57 <= 255 ->
array_type_vallist_match Tint8 v´37 ->
length v´37 = nat_of_Z OS_RDY_TBL_SIZE ->
RL_RTbl_PrioTbl_P
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
v´36 vhold.
Lemma prio_wt_inq_convert:
forall pri vx,
PrioWaitInQ pri vx <->
PrioWaitInQ (Int.unsigned ($ pri)) vx /\ 0 <= pri < 64.
Lemma prio_wt_inq_tid_neq:
forall prio´ v´13 v´69 prio,
nth_val´ (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) v´13 = Vint32 v´69 ->
Int.unsigned prio < 64 ->
(PrioWaitInQ (Int.unsigned prio´)
(update_nth_val (Z.to_nat (Int.unsigned (Int.shru prio ($ 3)))) v´13
(Vint32 (v´69&Int.not ($ 1<< (prio & $7))))) <->
PrioWaitInQ (Int.unsigned prio´) v´13 /\ prio´ <> prio).
Lemma wtset_notnil_msgls_nil:
forall x1 x0 x ,
x1 <> nil ->
RH_ECB_P (absmsgq x x0, x1) -> x = nil.
Lemma rl_tbl_grp_neq_zero:
forall v´12 px v´13 v´69,
Int.unsigned px < 8 ->
Int.unsigned v´12 <= 255 ->
v´12 <> $ 0 ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 px ->
nth_val´ (Z.to_nat (Int.unsigned px)) v´13 = Vint32 v´69 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
v´69 <> $ 0.
Lemma ECBList_P_Set_Rdy_hold:
forall a tcbls tid prio msg msg´ x y b c eid nl,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_q eid) nl, msg) ->
EcbMod.get c eid = None ->
ECBList_P x y a b c tcbls ->
ECBList_P x y a b c (TcbMod.set tcbls tid (prio,rdy,msg´)).
Lemma ecblist_p_post_exwt_hold:
forall v´36 v´12 v´13 v´38 v´69 v´39 v´58 v´40 v´32 v´15 v´24 v´35 v´16
v´18 v´19 v´20 v´34 v´21 v´22 v´23 v´25 v´26 v´27 x x0 x1 v´0 v´1
v´5 v´6 v´7 x00 v´11 v´31 v´30 v´29 v´10 v´9 prio v´62 st msg y vhold,
RL_RTbl_PrioTbl_P v´13 v´36 vhold->
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_Q
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DMsgQ (Vptr (v´24, Int.zero))
(v´16
:: v´18
:: v´19
:: v´20
:: v´34
:: Vint32 v´21
:: Vint32 v´22 :: Vptr (v´23, Int.zero) :: nil)
(v´26 :: v´25 :: nil) v´27) (absmsgq x x0, x1)->
ECBList_P v´0 Vnull v´1 v´5 v´6 v´7 ->
ECBList_P v´29 (Vptr (v´32, Int.zero)) v´30 v´31 v´9 v´7 ->
EcbMod.joinsig (v´32, Int.zero) (absmsgq x x0, x1) v´6 v´10 ->
EcbMod.join v´9 v´10 v´11 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
R_PrioTbl_P v´36 v´7 vhold ->
x1 <> nil ->
ECBList_P v´29 Vnull
(v´30 ++
((V$OS_EVENT_TYPE_Q
:: Vint32 y
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) :: nil) ++ v´1)
(v´31 ++
(DMsgQ (Vptr (v´24, Int.zero))
(v´16
:: v´18
:: v´19
:: v´20
:: v´34
:: Vint32 v´21
:: Vint32 v´22 :: Vptr (v´23, Int.zero) :: nil)
(v´26 :: v´25 :: nil) v´27 :: nil) ++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(absmsgq nil x0, remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero)
(prio, rdy , Vptr x00))
.
Lemma ecblist_p_post_exwt_hold´:
forall (v´36 : vallist) (v´12 : int32) (v´13 : vallist)
(v´38 v´69 v´39 : int32) (v´58 : block) (v´40 v´41 : int32)
(v´32 : block) (v´15 : int32) (v´24 : block)
(v´35 v´16 v´18 v´19 v´20 v´34 : val) (v´21 v´22 : int32)
(v´23 : block) (v´25 v´26 : val) (v´27 : vallist)
(x : list msg) (x0 : maxlen) (x1 : waitset)
(v´0 : val) (v´1 : list EventCtr) (v´5 : list EventData)
(v´6 : EcbMod.map) (v´7 : TcbMod.map) (x00 : addrval)
(v´11 : EcbMod.map) (v´31 : list EventData)
(v´30 : list EventCtr) (v´29 : val) (v´10 v´9 : EcbMod.map)
(prio : priority) v´62 st msg vhold,
RL_RTbl_PrioTbl_P v´13 v´36 vhold->
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 = Vptr (v´58, Int.zero)->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_Q
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DMsgQ (Vptr (v´24, Int.zero))
(v´16
:: v´18
:: v´19
:: v´20
:: v´34
:: Vint32 v´21
:: Vint32 v´22 :: Vptr (v´23, Int.zero) :: nil)
(v´26 :: v´25 :: nil) v´27) (absmsgq x x0, x1)->
ECBList_P v´0 Vnull v´1 v´5 v´6 v´7 ->
ECBList_P v´29 (Vptr (v´32, Int.zero)) v´30 v´31 v´9 v´7 ->
EcbMod.joinsig (v´32, Int.zero) (absmsgq x x0, x1) v´6 v´10 ->
EcbMod.join v´9 v´10 v´11 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
R_PrioTbl_P v´36 v´7 vhold->
x1 <> nil ->
ECBList_P v´29 Vnull
(v´30 ++
((V$OS_EVENT_TYPE_Q
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) :: nil) ++ v´1)
(v´31 ++
(DMsgQ (Vptr (v´24, Int.zero))
(v´16
:: v´18
:: v´19
:: v´20
:: v´34
:: Vint32 v´21
:: Vint32 v´22 :: Vptr (v´23, Int.zero) :: nil)
(v´26 :: v´25 :: nil) v´27 :: nil) ++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(absmsgq nil x0, remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero)
(prio, rdy , Vptr x00)).
Lemma rh_curtcb_set_nct:
forall v´8 v´7 x tid ,
RH_CurTCB v´8 v´7 ->
v´8 <> tid ->
RH_CurTCB v´8
(TcbMod.set v´7 tid
x).
Lemma tidneq_inwt_in:
forall x1 tid tid0,
tid <> tid0 ->
(In tid0 (remove_tid tid x1) <->
In tid0 x1).
Lemma tid_in_rmwt_in :
forall x1 tid,
In tid (remove_tid tid x1) ->
In tid x1.
Lemma in_wtset_rm_notin:
forall x1 tid,
In tid x1 ->
~ In tid (remove_tid tid x1).
Lemma rh_tcblist_ecblist_p_post_exwt:
forall v´8 tid v´11 v´7 v´9 v´10 eid x x0 x1 v´6 prio msg x00 xl,
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmsgq x x0, x1) v´6 v´10 ->
In tid x1 ->
TcbMod.get v´7 tid = Some (prio, wait (os_stat_q eid) xl, msg) ->
RH_TCBList_ECBList_P
(EcbMod.set v´11 eid
(absmsgq nil x0, remove_tid tid x1))
(TcbMod.set v´7 tid
(prio, rdy , Vptr x00)) v´8.
Lemma qpost_ovf_prop:
forall i2 i1 x13 x12 x6 x7 x8 v´49 v´47 x14 x15 x x1 x2 v2,
true = Int.ltu i2 i1 ->
WellformedOSQ
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x x1, x2) ->
Z.ge (Z_of_nat (length x)) (Int.unsigned x1).
Lemma qpost_ovf_prop´:
forall i2 i1 x13 x12 x6 x7 x8 v´49 v´47 x14 x15 x x1 x2 v2,
true = Int.eq i1 i2 ->
WellformedOSQ
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x x1, x2) ->
Z.ge (Z_of_nat (length x)) (Int.unsigned x1).
Lemma osq_same_blk_st_in´:
forall (qptr qst qend qin qout qsz qen : val) (b : block) (i : int32),
WellformedOSQ
(qptr :: qst :: qend :: qin :: qout :: qsz :: qen :: Vptr (b, i) :: nil) ->
exists i´, qin = Vptr (b, i´).
Lemma wellq_in_props:
forall (x12 x11 x5 x6 : val) (v´49 : block) (x i2 i1 : int32)
(v´47 : block) (x13 x14 : val) (v2 : list val)
(v´46 : absecb.B),
length v2 = ∘OS_MAX_Q_SIZE ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x12
:: x11
:: x5
:: Vptr (v´49, x)
:: x6
:: Vint32 i2 :: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x13 :: x14 :: nil) v2) v´46 ->
WellformedOSQ
(x12
:: x11
:: x5
:: Vptr (v´49, x)
:: x6
:: Vint32 i2 :: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero)) <= Int.unsigned x /\
4 * ((Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4) =
Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero)) /\
(Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4 < 20 /\
(Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4 <
Z.of_nat (length v2).
Lemma wellformedosq_size_add_1:
forall x13 x12 x6 v´49 x x8 i2 i1,
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) -> Int.unsigned (i2+ᵢ$ 1) <= Int16.max_unsigned.
Lemma wellformedosq_ens_add_1:
forall x13 x12 x6 v´49 x x8 i2 i1 x10 x11 v´46 v2 v´36,
length v2 = ∘OS_MAX_Q_SIZE ->
RLH_ECBData_P
(DMsgQ (Vptr (v´36, Int.zero))
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x10 :: x11 :: nil) v2) v´46 ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) -> Int.unsigned (i1+ᵢ$ 1) <= Int16.max_unsigned.
Lemma rlh_ecb_nowait_prop:
forall v´25 i i3 v´47 x4 v´42 v´40 v´35 v´34 x1 x2 x3 v´37,
RL_Tbl_Grp_P v´40 (Vint32 i)->
R_ECB_ETbl_P (v´25, Int.zero)
(V$OS_EVENT_TYPE_Q
:: Vint32 i
:: Vint32 i3 :: Vptr (v´47, Int.zero) :: x4 :: v´42 :: nil,
v´40) v´35 ->
EcbMod.get v´34 (v´25, Int.zero) = Some (absmsgq x1 x2, x3) ->
RH_TCBList_ECBList_P v´34 v´35 v´37 ->
Int.eq i ($ 0) = true ->
x3 = nil.
Lemma qpost_no_wait_prop´:
forall i2 i1 x13 x12 x6 x7 x8 v´49 v´47 x14 x15 x x1 x2 v2,
Int.ltu i1 i2 = true ->
WellformedOSQ
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: x7
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x x1, x2) ->
Z.of_nat (length x) < (Int.unsigned x1) .
Lemma get_wellformedosq_in_setst:
forall i1 i2 x13 x12 x6 v´49 x x8,
Int.ltu i1 i2 = true ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
val_inj
match x6 with
| Vundef => None
| Vnull => Some (Vint32 Int.zero)
| Vint32 _ => None
| Vptr (b2, ofs2) =>
if peq v´49 b2
then
if Int.eq (x+ᵢInt.mul ($ 1) ($ 4)) ofs2
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)
else Some (Vint32 Int.zero)
end <> Vint32 Int.zero ->
WellformedOSQ
(x13
:: x12
:: x6
:: x12
:: x8
:: Vint32 i2
:: Vint32 (i1+ᵢ$ 1) :: Vptr (v´49, Int.zero) :: nil).
Lemma msgqlist_p_compose´
: forall (p : val) (qid : addrval) (mqls : EcbMod.map)
(qptrl1 qptrl2 : list EventCtr) (i i1 : int32)
(a : addrval) (x3 p´ : val) (v´41 : vallist)
(msgqls1 msgqls2 : list EventData) (msgq : EventData)
(mqls1 mqls2 : EcbMod.map) (mq : absecb.B)
(mqls´ : EcbMod.map) (tcbls : TcbMod.map),
R_ECB_ETbl_P qid
(V$OS_EVENT_TYPE_Q
:: Vint32 i :: Vint32 i1 :: Vptr a :: x3 :: p´ :: nil, v´41) tcbls ->
ECBList_P p (Vptr qid) qptrl1 msgqls1 mqls1 tcbls ->
ECBList_P p´ Vnull qptrl2 msgqls2 mqls2 tcbls ->
RLH_ECBData_P msgq mq ->
EcbMod.joinsig qid mq mqls2 mqls´ ->
EcbMod.join mqls1 mqls´ (EcbMod.set mqls qid mq) ->
ECBList_P p Vnull
(qptrl1 ++
((V$OS_EVENT_TYPE_Q
:: Vint32 i :: Vint32 i1 :: Vptr a :: x3 :: p´ :: nil, v´41)
:: nil) ++ qptrl2) (msgqls1 ++ (msgq :: nil) ++ msgqls2) (EcbMod.set mqls qid mq)
tcbls.
Lemma rlh_ecbdata_in_end:
forall i1 i2 x13 x12 v´49 x x8 v´47 x14 x15 v2 x1 x2 x0,
Int.ltu i1 i2 = true ->
length v2 = ∘OS_MAX_Q_SIZE ->
WellformedOSQ
(x13
:: x12
:: Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4)) )
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4)) )
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x1 x2, nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: Vptr (v´49, x+ᵢInt.mul ($ 1) ($ 4))
:: x12
:: x8
:: Vint32 i2
:: Vint32 (i1+ᵢ$ 1) :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil)
(update_nth_val
(Z.to_nat
((Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) /
4)) v2 (Vptr x0))) (absmsgq (x1 ++ (Vptr x0::nil)) x2, nil).
Lemma rh_tcbls_mqls_p_setmsg_hold:
forall (mqls : EcbMod.map) (tcbls : TcbMod.map) (ct : tid)
(a : tidspec.A) (v : msg) (vl : list msg) (qmax : maxlen)
(wl : waitset),
RH_TCBList_ECBList_P mqls tcbls ct ->
EcbMod.get mqls a = Some (absmsgq vl qmax, wl) ->
RH_TCBList_ECBList_P (EcbMod.set mqls a (absmsgq (vl++v::nil) qmax, wl)) tcbls ct.
Lemma get_wellformedosq_in_setst´:
forall i1 i2 x13 x12 x6 v´49 x x8,
x6 <> Vptr (v´49, (x+ᵢInt.mul ($ 1) ($ 4))) ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x+ᵢInt.mul ($ 1) ($ 4))
:: x8
:: Vint32 i2
:: Vint32 (i1+ᵢ$ 1) :: Vptr (v´49, Int.zero) :: nil).
Lemma rlh_ecbdata_in_noend:
forall i1 i2 x13 x12 v´49 x x8 v´47 x14 x15 v2 x1 x2 x0 x6,
x6 <> Vptr (v´49, x+ᵢInt.mul ($ 1) ($ 4)) ->
Int.ltu i1 i2 = true ->
length v2 = ∘OS_MAX_Q_SIZE ->
WellformedOSQ
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: Vptr (v´49, x)
:: x8
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil) v2) (absmsgq x1 x2, nil) ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x13
:: x12
:: x6
:: Vptr (v´49, x+ᵢInt.mul ($ 1) ($ 4))
:: x8
:: Vint32 i2
:: Vint32 (i1+ᵢ$ 1) :: Vptr (v´49, Int.zero) :: nil)
(x14 :: x15 :: nil)
(update_nth_val
(Z.to_nat
((Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) /
4)) v2 (Vptr x0))) (absmsgq (x1++ (Vptr x0 :: nil)) x2, nil).
Lemma prio_in_rtbl_hold:
forall rtbl x y prio,
Int.unsigned prio < 64 ->
Int.unsigned x <= 7 ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u rtbl ->
prio_in_tbl prio rtbl ->
prio_in_tbl prio
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 y)))).
Lemma idle_in_rtbl_hold´:
forall rtbl x y,
Int.unsigned x <= 7 ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u rtbl ->
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
prio_in_tbl ($ OS_IDLE_PRIO)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 y)))).
Lemma get_tcb_stat:
forall p etbl ptbl tid tcbls abstcb tcbls´ vl rtbl qid vle vhold,
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u etbl ->
length etbl = ∘OS_EVENT_TBL_SIZE ->
prio_in_tbl p etbl ->
nth_val´ (Z.to_nat (Int.unsigned p)) ptbl = Vptr tid ->
R_PrioTbl_P ptbl tcbls vhold ->
TcbJoin tid abstcb tcbls´ tcbls ->
TCBNode_P vl rtbl abstcb ->
R_ECB_ETbl_P qid
(V$OS_EVENT_TYPE_Q
::vle,
etbl) tcbls ->
V_OSTCBStat vl = Some (Vint32 (Int.repr OS_STAT_Q)).
Lemma rh_tcblist_ecblist_p_post_exwt_aux:
forall (v´8 tid0 : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) (x : list msg)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
st,
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmsgq x x0, x1) v´6 v´10 ->
In tid0 x1 ->
TcbMod.get v´7 tid0 = Some (prio, st, msg0) ->
exists xl, st = wait (os_stat_q eid) xl.
Lemma statq_and_not_statq_eq_rdy:
Int.eq ($ OS_STAT_Q&Int.not ($ OS_STAT_Q)) ($ OS_STAT_RDY) = true.
Require Import lab.
Lemma qpost_absinfer_null:
forall P vl,
can_change_aop P ->
absinfer
( <|| qpost (Vnull :: vl) ||> **
P) (<|| END Some (V$OS_ERR_PEVENT_NULL) ||> **
P).
Lemma qpost_absinfer_msg_null:
forall P v,
can_change_aop P ->
absinfer
( <|| qpost (v :: Vnull ::nil) ||> **
P) (<|| END Some (Vint32 (Int.repr OS_ERR_POST_NULL_PTR)) ||> **
P).
Lemma qpost_absinfer_no_q:
forall P mqls x v,
can_change_aop P ->
(~ exists a b wl,EcbMod.get mqls x = Some (absmsgq a b,wl)) ->
absinfer
( <|| qpost (Vptr x :: v :: nil) ||> **
HECBList mqls ** P)
(<|| END Some (Vint32 (Int.repr MSGQ_NULL_ERR)) ||> ** HECBList mqls ** P).
Lemma qpost_absinfer_ovf:
forall P mqls x v a b wl,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq a b,wl) ->
Z.ge (Z_of_nat (length a)) (Int.unsigned b) ->
absinfer
( <|| qpost (Vptr x :: v :: nil) ||> **
HECBList mqls ** P)
(<|| END Some (Vint32 (Int.repr MSGQ_OVF_ERR)) ||> ** HECBList mqls ** P).
Lemma qpost_absinfer_nowt_succ:
forall P mqls x v a b tcbls t ct,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq a b,nil) ->
Z.lt (Z_of_nat (length a)) (Int.unsigned b) ->
absinfer
( <|| qpost (Vptr x :: v :: nil) ||> **
HECBList mqls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END Some (Vint32 (Int.repr NO_ERR)) ||> ** HECBList (EcbMod.set mqls x (absmsgq (a++(v::nil)) b,nil))** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma qpost_absinfer_exwt_succ:
forall P mqls x v n wl tls t ct p st m t´ vl,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq vl n,wl) ->
~ wl=nil ->
GetHWait tls wl t´ ->
TcbMod.get tls t´ = Some (p,st,m) ->
absinfer
( <|| qpost (Vptr x :: v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| isched ;; END Some (Vint32 (Int.repr NO_ERR)) ||> ** HECBList (EcbMod.set mqls x (absmsgq nil n,(remove_tid t´ wl))) ** HTCBList (TcbMod.set tls t´ (p,rdy ,v) ) ** HTime t ** HCurTCB ct ** P).
Open Scope code_scope.
Lemma Astruct_OSTCB_PV_ptr_neq :
forall s b p2 v1 l v2 P,
s |= Astruct (b, Int.zero) OS_TCB (v1::l) ** PV p2 @ Int8u |-> v2 ** P ->
(b, Int.zero) <> p2.
Lemma event_type_n_match´:
forall s P i1 i0 i2 x2 x3 v´42 i10,
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil)
(DMbox i10) ** P ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = true ->
False.
Lemma event_type_n_match´´:
forall s P i1 i0 i2 x2 x3 v´42 i10 x,
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil)
(DMutex i10 x) ** P ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = true ->
False.
Lemma event_type_n_match:
forall s P i1 i0 i2 x2 x3 v´42 i10,
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil)
(DSem i10) ** P ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = true ->
False.
Lemma isptr_zh :
forall x, isptr x ->
match x with
| Vundef => false
| Vnull => true
| Vint32 _ => false
| Vptr _ => true
end = true.