Library OSTimeDlyPure
Require Export mathlib.
Lemma R_PrioTbl_P_hold1:
forall vl tcb tid prio st msg st´ adrv,
R_PrioTbl_P vl tcb adrv ->
TcbMod.get tcb tid = Some (prio, st, msg) ->
R_PrioTbl_P vl (TcbMod.set tcb tid (prio, st´, msg)) adrv.
Lemma RH_TCBList_ECBList_P_hold1:
forall tid ecbls tcbls prio st msg i,
RH_TCBList_ECBList_P ecbls tcbls tid ->
TcbMod.get tcbls tid = Some (prio, st, msg) ->
(st = rdy \/ exists n, st = wait os_stat_time n) ->
RH_TCBList_ECBList_P ecbls (TcbMod.set tcbls tid (prio, wait os_stat_time i, msg)) tid.
Lemma ecb_etbl_prop:
forall st b prio msg x v v0 tcbls i,
st = rdy \/ (exists n, st = wait os_stat_time n) ->
TcbMod.get tcbls (b, Int.zero) = Some (prio, st, msg) ->
R_ECB_ETbl_P x (v, v0) tcbls ->
R_ECB_ETbl_P x (v, v0)
(TcbMod.set tcbls (b, Int.zero)
(prio, wait os_stat_time i, msg)).
Lemma ECBList_P_hold1:
forall l v ecbls mqls tcbls b i prio st msg,
ECBList_P v Vnull l ecbls mqls tcbls ->
TcbMod.get tcbls (b, Int.zero) = Some (prio, st, msg) ->
(st = rdy \/ exists n, st = wait os_stat_time n) ->
Int.unsigned i <= 65535 ->
Int.ltu ($ 0) i = true ->
ECBList_P v Vnull l ecbls mqls (TcbMod.set tcbls (b, Int.zero) (prio, wait os_stat_time i, msg)).
Lemma RH_CurTCB_hold1 :
forall tid tcbls prio st msg i,
RH_CurTCB tid tcbls ->
TcbMod.get tcbls tid = Some (prio, st, msg) ->
RH_CurTCB tid (TcbMod.set tcbls tid (prio, wait os_stat_time i, msg)).
Lemma event_wait_rl_tbl_grp´:
forall x10 x9 x8 x7 i10 i6 i5 i4 i3 i2 i1 i0 v´1 x,
RL_TCBblk_P
(x10
:: x9
:: x8
:: x7
:: Vint32 i10
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3 :: Vint32 i2 :: Vint32 i1 :: nil) ->
array_type_vallist_match Int8u v´1 ->
Int.eq (x&Int.not i2) ($ 0) = true ->
RL_Tbl_Grp_P v´1 (Vint32 i0) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned i3)) v´1 (Vint32 (x&Int.not i2)))
(Vint32 (i0&Int.not i1)).
Lemma event_wait_rl_tbl_grp:
forall x10 x9 x8 x7 i10 i6 i5 i4 i3 i2 v´5 x0 i i1,
RL_TCBblk_P
(x10
:: x9
:: x8
:: x7
:: Vint32 i10
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3 :: Vint32 i2 :: Vint32 i1 :: nil) ->
array_type_vallist_match Int8u v´5 ->
nth_val´ (Z.to_nat (Int.unsigned i3)) v´5 = Vint32 x0 ->
RL_Tbl_Grp_P v´5 (Vint32 i) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned i3)) v´5 (Vint32 (Int.or x0 i2)))
(Vint32 (Int.or i i1)).
Lemma event_wait_rl_tbl_grp´´:
forall x10 x9 x8 x7 i10 i6 i5 i4 i3 i2 i1 i0 v´1 x,
RL_TCBblk_P
(x10
:: x9
:: x8
:: x7
:: Vint32 i10
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3 :: Vint32 i2 :: Vint32 i1 :: nil) ->
array_type_vallist_match Int8u v´1 ->
nth_val´ (Z.to_nat (Int.unsigned i3)) v´1 = Vint32 x ->
Int.eq (x&Int.not i2) ($ 0) = false ->
RL_Tbl_Grp_P v´1 (Vint32 i0) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned i3)) v´1 (Vint32 (x&Int.not i2)))
(Vint32 i0).
Lemma low_stat_rdy_imp_high:
forall a b c d e f g h i j st rtbl p t m,
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
RL_TCBblk_P (a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: Vint32 f
:: g
:: h :: i :: j :: nil)
->
R_TCB_Status_P
(a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: Vint32 f
:: g
:: h :: i :: j :: nil)
rtbl (p, t, m) -> Int.eq st ($ OS_STAT_RDY) = true ->
Int.eq e ($ 0) = true ->
t = rdy .
Lemma low_stat_nordy_imp_high:
forall a b c d e f g h i j st rtbl p t m,
R_TCB_Status_P
(a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: f
:: g
:: h :: i :: j :: nil)
rtbl (p, t, m) -> (Int.eq st ($ OS_STAT_RDY) = false \/ Int.eq e ($ 0) = false) ->
~(t = rdy ).
Lemma RLH_Rdy_prioneq_prop_hold:
forall p prio a rtbl t m grp,
p <> prio ->
0 <= Int.unsigned prio < 64 ->
0 <= Int.unsigned p < 64 ->
V_OSTCBPrio a = Some (Vint32 p) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_RdyI_P a rtbl (p, t, m) ->
RLH_RdyI_P a
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) (p, t, m).
Lemma RHL_Rdy_prioneq_prop_hold:
forall p prio a rtbl t m grp,
p <> prio ->
0 <= Int.unsigned prio < 64 ->
0 <= Int.unsigned p < 64 ->
V_OSTCBPrio a = Some (Vint32 p) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_RdyI_P a rtbl (p, t, m) ->
RHL_RdyI_P a
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) (p, t, m).
Lemma RLH_Wait_prioneq_prop_hold:
forall p prio a rtbl t m grp,
p <> prio ->
0 <= Int.unsigned prio < 64 ->
0 <= Int.unsigned p < 64 ->
V_OSTCBPrio a = Some (Vint32 p) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_TCB_Status_Wait_P a rtbl (p, t, m) ->
RLH_TCB_Status_Wait_P a
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) (p, t, m).
Lemma RHL_Wait_prioneq_prop_hold:
forall p prio a rtbl t m grp,
p <> prio ->
0 <= Int.unsigned prio < 64 ->
0 <= Int.unsigned p < 64 ->
V_OSTCBPrio a = Some (Vint32 p) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_TCB_Status_Wait_P a rtbl (p, t, m) ->
RHL_TCB_Status_Wait_P a
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) (p, t, m).
Lemma update_rtbl_tcblist_hold:
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 a b c , TcbMod.get tcbls tid = Some (a,b,c) -> a <> prio
) ->
TCBList_P vptr vl rtbl tcbls ->
TCBList_P vptr vl
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp &Int.not ($ 1<<(prio &$ 7))))) tcbls.
Lemma TCBList_P_tcb_dly_hold :
forall ptcb v1 v2 v3 v5 v6 v8 v9 v10 v11 rtbl vl
tcbls prio st m time ry,
Int.unsigned time <= 65535 ->
Int.ltu ($ 0) time = true ->
TCBList_P (Vptr ptcb) ((v1::v2::v3::m::v5::(Vint32 v6)::(Vint32 prio)::v8::(Vint32 v9)::(Vint32 v10)::v11::nil)::vl) rtbl tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
st = rdy \/ (exists n, st = wait os_stat_time n) ->
prio_neq_cur tcbls ptcb prio ->
nth_val (nat_of_Z (Int.unsigned v9)) rtbl = Some (Vint32 ry) ->
TCBList_P (Vptr ptcb) ((v1::v2::v3::m::(Vint32 time)::(Vint32 v6)::(Vint32 prio)::v8::(Vint32 v9)::(Vint32 v10)::v11::nil)::vl)
(update_nth_val ∘(Int.unsigned v9) rtbl (Vint32 (Int.and ry (Int.not v10))))
(TcbMod.set tcbls ptcb (prio, wait os_stat_time time, m)).
Lemma TCBList_P_tcb_dly_hold´ :
forall v ptcb rtbl vl y bitx
tcbls prio ry x1 tcs tcs´ t m,
0 <= Int.unsigned prio < 64 ->
TcbMod.join (TcbMod.sig ptcb (prio, t, m)) x1 tcs ->
TcbMod.join tcbls tcs tcs´ ->
TCBList_P v vl rtbl tcbls ->
y = Int.shru prio ($ 3) ->
bitx = ($ 1) << (Int.and prio ($ 7)) ->
prio_neq_cur tcbls ptcb prio ->
nth_val (nat_of_Z (Int.unsigned y)) rtbl = Some (Vint32 ry) ->
TCBList_P v vl (update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (Int.and ry (Int.not bitx)))) tcbls.
Lemma rtbl_remove_RL_RTbl_PrioTbl_P_hold :
forall prio y bitx rtbl ry ptbl vhold,
0 <= Int.unsigned prio < 64 ->
y = Int.shru (prio) ($ 3) ->
bitx = ($ 1) << (Int.and (prio) ($ 7)) ->
nth_val ∘(Int.unsigned y) rtbl = Some (Vint32 ry) ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
RL_RTbl_PrioTbl_P
(update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (ry&Int.not bitx))) ptbl vhold.
Lemma R_PrioTbl_P_hold1:
forall vl tcb tid prio st msg st´ adrv,
R_PrioTbl_P vl tcb adrv ->
TcbMod.get tcb tid = Some (prio, st, msg) ->
R_PrioTbl_P vl (TcbMod.set tcb tid (prio, st´, msg)) adrv.
Lemma RH_TCBList_ECBList_P_hold1:
forall tid ecbls tcbls prio st msg i,
RH_TCBList_ECBList_P ecbls tcbls tid ->
TcbMod.get tcbls tid = Some (prio, st, msg) ->
(st = rdy \/ exists n, st = wait os_stat_time n) ->
RH_TCBList_ECBList_P ecbls (TcbMod.set tcbls tid (prio, wait os_stat_time i, msg)) tid.
Lemma ecb_etbl_prop:
forall st b prio msg x v v0 tcbls i,
st = rdy \/ (exists n, st = wait os_stat_time n) ->
TcbMod.get tcbls (b, Int.zero) = Some (prio, st, msg) ->
R_ECB_ETbl_P x (v, v0) tcbls ->
R_ECB_ETbl_P x (v, v0)
(TcbMod.set tcbls (b, Int.zero)
(prio, wait os_stat_time i, msg)).
Lemma ECBList_P_hold1:
forall l v ecbls mqls tcbls b i prio st msg,
ECBList_P v Vnull l ecbls mqls tcbls ->
TcbMod.get tcbls (b, Int.zero) = Some (prio, st, msg) ->
(st = rdy \/ exists n, st = wait os_stat_time n) ->
Int.unsigned i <= 65535 ->
Int.ltu ($ 0) i = true ->
ECBList_P v Vnull l ecbls mqls (TcbMod.set tcbls (b, Int.zero) (prio, wait os_stat_time i, msg)).
Lemma RH_CurTCB_hold1 :
forall tid tcbls prio st msg i,
RH_CurTCB tid tcbls ->
TcbMod.get tcbls tid = Some (prio, st, msg) ->
RH_CurTCB tid (TcbMod.set tcbls tid (prio, wait os_stat_time i, msg)).
Lemma event_wait_rl_tbl_grp´:
forall x10 x9 x8 x7 i10 i6 i5 i4 i3 i2 i1 i0 v´1 x,
RL_TCBblk_P
(x10
:: x9
:: x8
:: x7
:: Vint32 i10
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3 :: Vint32 i2 :: Vint32 i1 :: nil) ->
array_type_vallist_match Int8u v´1 ->
Int.eq (x&Int.not i2) ($ 0) = true ->
RL_Tbl_Grp_P v´1 (Vint32 i0) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned i3)) v´1 (Vint32 (x&Int.not i2)))
(Vint32 (i0&Int.not i1)).
Lemma event_wait_rl_tbl_grp:
forall x10 x9 x8 x7 i10 i6 i5 i4 i3 i2 v´5 x0 i i1,
RL_TCBblk_P
(x10
:: x9
:: x8
:: x7
:: Vint32 i10
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3 :: Vint32 i2 :: Vint32 i1 :: nil) ->
array_type_vallist_match Int8u v´5 ->
nth_val´ (Z.to_nat (Int.unsigned i3)) v´5 = Vint32 x0 ->
RL_Tbl_Grp_P v´5 (Vint32 i) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned i3)) v´5 (Vint32 (Int.or x0 i2)))
(Vint32 (Int.or i i1)).
Lemma event_wait_rl_tbl_grp´´:
forall x10 x9 x8 x7 i10 i6 i5 i4 i3 i2 i1 i0 v´1 x,
RL_TCBblk_P
(x10
:: x9
:: x8
:: x7
:: Vint32 i10
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3 :: Vint32 i2 :: Vint32 i1 :: nil) ->
array_type_vallist_match Int8u v´1 ->
nth_val´ (Z.to_nat (Int.unsigned i3)) v´1 = Vint32 x ->
Int.eq (x&Int.not i2) ($ 0) = false ->
RL_Tbl_Grp_P v´1 (Vint32 i0) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned i3)) v´1 (Vint32 (x&Int.not i2)))
(Vint32 i0).
Lemma low_stat_rdy_imp_high:
forall a b c d e f g h i j st rtbl p t m,
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
RL_TCBblk_P (a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: Vint32 f
:: g
:: h :: i :: j :: nil)
->
R_TCB_Status_P
(a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: Vint32 f
:: g
:: h :: i :: j :: nil)
rtbl (p, t, m) -> Int.eq st ($ OS_STAT_RDY) = true ->
Int.eq e ($ 0) = true ->
t = rdy .
Lemma low_stat_nordy_imp_high:
forall a b c d e f g h i j st rtbl p t m,
R_TCB_Status_P
(a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: f
:: g
:: h :: i :: j :: nil)
rtbl (p, t, m) -> (Int.eq st ($ OS_STAT_RDY) = false \/ Int.eq e ($ 0) = false) ->
~(t = rdy ).
Lemma RLH_Rdy_prioneq_prop_hold:
forall p prio a rtbl t m grp,
p <> prio ->
0 <= Int.unsigned prio < 64 ->
0 <= Int.unsigned p < 64 ->
V_OSTCBPrio a = Some (Vint32 p) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_RdyI_P a rtbl (p, t, m) ->
RLH_RdyI_P a
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) (p, t, m).
Lemma RHL_Rdy_prioneq_prop_hold:
forall p prio a rtbl t m grp,
p <> prio ->
0 <= Int.unsigned prio < 64 ->
0 <= Int.unsigned p < 64 ->
V_OSTCBPrio a = Some (Vint32 p) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_RdyI_P a rtbl (p, t, m) ->
RHL_RdyI_P a
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) (p, t, m).
Lemma RLH_Wait_prioneq_prop_hold:
forall p prio a rtbl t m grp,
p <> prio ->
0 <= Int.unsigned prio < 64 ->
0 <= Int.unsigned p < 64 ->
V_OSTCBPrio a = Some (Vint32 p) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RLH_TCB_Status_Wait_P a rtbl (p, t, m) ->
RLH_TCB_Status_Wait_P a
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) (p, t, m).
Lemma RHL_Wait_prioneq_prop_hold:
forall p prio a rtbl t m grp,
p <> prio ->
0 <= Int.unsigned prio < 64 ->
0 <= Int.unsigned p < 64 ->
V_OSTCBPrio a = Some (Vint32 p) ->
nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl = Some (Vint32 grp) ->
RHL_TCB_Status_Wait_P a rtbl (p, t, m) ->
RHL_TCB_Status_Wait_P a
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp&Int.not ($ 1<<(prio&$ 7))))) (p, t, m).
Lemma update_rtbl_tcblist_hold:
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 a b c , TcbMod.get tcbls tid = Some (a,b,c) -> a <> prio
) ->
TCBList_P vptr vl rtbl tcbls ->
TCBList_P vptr vl
(update_nth_val ∘(Int.unsigned (Int.shru prio ($ 3))) rtbl
(Vint32 (grp &Int.not ($ 1<<(prio &$ 7))))) tcbls.
Lemma TCBList_P_tcb_dly_hold :
forall ptcb v1 v2 v3 v5 v6 v8 v9 v10 v11 rtbl vl
tcbls prio st m time ry,
Int.unsigned time <= 65535 ->
Int.ltu ($ 0) time = true ->
TCBList_P (Vptr ptcb) ((v1::v2::v3::m::v5::(Vint32 v6)::(Vint32 prio)::v8::(Vint32 v9)::(Vint32 v10)::v11::nil)::vl) rtbl tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
st = rdy \/ (exists n, st = wait os_stat_time n) ->
prio_neq_cur tcbls ptcb prio ->
nth_val (nat_of_Z (Int.unsigned v9)) rtbl = Some (Vint32 ry) ->
TCBList_P (Vptr ptcb) ((v1::v2::v3::m::(Vint32 time)::(Vint32 v6)::(Vint32 prio)::v8::(Vint32 v9)::(Vint32 v10)::v11::nil)::vl)
(update_nth_val ∘(Int.unsigned v9) rtbl (Vint32 (Int.and ry (Int.not v10))))
(TcbMod.set tcbls ptcb (prio, wait os_stat_time time, m)).
Lemma TCBList_P_tcb_dly_hold´ :
forall v ptcb rtbl vl y bitx
tcbls prio ry x1 tcs tcs´ t m,
0 <= Int.unsigned prio < 64 ->
TcbMod.join (TcbMod.sig ptcb (prio, t, m)) x1 tcs ->
TcbMod.join tcbls tcs tcs´ ->
TCBList_P v vl rtbl tcbls ->
y = Int.shru prio ($ 3) ->
bitx = ($ 1) << (Int.and prio ($ 7)) ->
prio_neq_cur tcbls ptcb prio ->
nth_val (nat_of_Z (Int.unsigned y)) rtbl = Some (Vint32 ry) ->
TCBList_P v vl (update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (Int.and ry (Int.not bitx)))) tcbls.
Lemma rtbl_remove_RL_RTbl_PrioTbl_P_hold :
forall prio y bitx rtbl ry ptbl vhold,
0 <= Int.unsigned prio < 64 ->
y = Int.shru (prio) ($ 3) ->
bitx = ($ 1) << (Int.and (prio) ($ 7)) ->
nth_val ∘(Int.unsigned y) rtbl = Some (Vint32 ry) ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
RL_RTbl_PrioTbl_P
(update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (ry&Int.not bitx))) ptbl vhold.