Library OSEventTaskRdyPure
Require Import ucert.
Require Import mathlib.
Open Scope code_scope.
Lemma z_le_n_lt´:
forall x1,
Int.unsigned x1 <= 7 ->
(Z.to_nat (Int.unsigned x1) < ∘OS_EVENT_TBL_SIZE)%nat.
Lemma pos_to_nat_range_0_7:
forall z, 0<=z -> z<=7 -> (0<=Z.to_nat z<=7)%nat.
Lemma osmapvallist_prop:forall x, (Int.unsigned x <=7) -> exists i, nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 i /\ Int.unsigned i <= 128.
Lemma unsigned_int_and_not_range:
forall x y,
Int.unsigned x <= 255 ->
Int.unsigned y<=255 ->
Int.unsigned (x&Int.not y) <=? 255 = true.
Lemma shl3_add_le_255:
forall x1 x2,
Int.unsigned x1 <= 7 ->
Int.unsigned x2 <= 7 ->
Int.unsigned ((x1<<$ 3)+ᵢx2) <64.
Lemma shl3_add_le_255´:
forall x1 x2,
Int.unsigned x1 <= 7 ->
Int.unsigned x2 <= 7 ->
((Z.to_nat (Int.unsigned ((x1<<$ 3)+ᵢx2))) <64) %nat.
Lemma rl_etbl_ptbl_p:
forall l egrp i4 v´33 x6 v´22 etbl tcbls ptbl etype av,
array_type_vallist_match Int8u etbl ->
length etbl = ∘OS_RDY_TBL_SIZE ->
R_ECB_ETbl_P l
(etype
:: Vint32 egrp
:: Vint32 i4 :: Vptr (v´33, Int.zero)
:: x6 :: v´22 :: nil,
etbl) tcbls ->
RL_Tbl_Grp_P etbl (Vint32 egrp) ->
R_PrioTbl_P ptbl tcbls av->
RL_RTbl_PrioTbl_P etbl ptbl av.
Lemma tcb_join_disj_get:
forall tcbls1 tcbls2 tcbls tid x,
TcbMod.join tcbls1 tcbls2 tcbls ->
TcbMod.get tcbls tid = Some x ->
(TcbMod.get tcbls1 tid = Some x /\ TcbMod.get tcbls2 tid = None)
\/(TcbMod.get tcbls2 tid = Some x /\ TcbMod.get tcbls1 tid = None).
Lemma last_eq:
forall x2 (x4 : vallist),
(last (x2 ++ x4 :: nil) nil) = x4.
Lemma tcbdllseg_isvptr:
forall l s p1 tail1 ct p z,
s |= tcbdllseg p1 z tail1 (Vptr ct) l ** p -> exists x, p1 = Vptr x.
Lemma tcbdllseg_split´:
forall x1 s P v´23 v´32 x2 x3 xx y,
s |= tcbdllseg (Vptr v´23) xx v´32 (Vptr y) (x1 ++ x2 :: x3) ** P ->
s |= EX x v´15,
tcbdllseg (Vptr v´23) xx x (Vptr v´15) x1 **
tcbdllseg (Vptr v´15) x v´32 (Vptr y) (x2 :: x3)** [|x1<>nil /\ nth_val 0 (last x1 nil) = Some (Vptr v´15) \/ x1 = nil /\ Vptr v´15 = Vptr v´23 |] ** P.
Lemma list_app_neq_nil:
forall x2 (x4 : vallist),
(x2 ++ x4 :: nil <> nil).
Lemma join_sig_minus_tcb : forall m a x, TcbMod.get m a = Some x -> TcbMod.join (TcbMod.sig a x) (TcbMod.minus m (TcbMod.sig a x)) m.
Lemma tcb_get_ex_tcbjoin:
forall x tid y,
TcbMod.get x tid = Some y ->
exists a, TcbJoin tid y a x.
Lemma in_ptbl_no_ct_get:
forall s x tid ptbl tcbls tcbls1 tcbls2 p1 l1 rtbl ct curtcb l2 tail1 tail2 P av ,
ct <> tid ->
tid <> av ->
0 <= Int.unsigned x < 64 ->
R_PrioTbl_P ptbl tcbls av->
nth_val´ ∘(Int.unsigned x) ptbl = Vptr tid ->
TcbMod.join tcbls1 tcbls2 tcbls ->
TCBList_P p1 l1 rtbl tcbls1 ->
TCBList_P (Vptr ct) (curtcb :: l2) rtbl tcbls2 ->
s |= tcbdllseg p1 Vnull tail1 (Vptr ct) l1 ** tcbdllseg (Vptr ct) tail1 tail2 Vnull (curtcb :: l2) ** P ->
(
s|= (EX tail1´ l1´ tidtcb l1´´ tcbls1´ tcbls1´´,
tcbdllseg p1 Vnull tail1´ (Vptr tid) l1´ **
tcbdllseg (Vptr tid) tail1´ tail1 (Vptr ct) (tidtcb::l1´´) **
tcbdllseg (Vptr ct) tail1 tail2 Vnull (curtcb :: l2) **
[| TCBList_P p1 l1´ rtbl tcbls1´|] **
[| TCBList_P (Vptr tid) (tidtcb::l1´´) rtbl tcbls1´´ |] **
[| TcbMod.join tcbls1´ tcbls1´´ tcbls1|] **
[| l1 = l1´++(tidtcb::l1´´) |] ** P)
\\//
(EX tail2´ l2´ tidtcb l2´´ tcbls2´ tcbls2´´,
tcbdllseg p1 Vnull tail1 (Vptr ct) l1 **
tcbdllseg (Vptr ct) tail1 tail2´ (Vptr tid) (curtcb :: l2´) **
tcbdllseg (Vptr tid) tail2´ tail2 Vnull (tidtcb::l2´´) **
[| TCBList_P (Vptr ct) (curtcb::l2´) rtbl tcbls2´|] **
[| TCBList_P (Vptr tid) (tidtcb::l2´´) rtbl tcbls2´´|] **
[| TcbMod.join tcbls2´ tcbls2´´ tcbls2|] **
[| l2 = l2´++(tidtcb::l2´´) |] ** P)
).
Lemma tcb_join_join_joinsig:
forall x1 x2 x x1´ x1´´ tid vl x1´´1,
TcbMod.join x1 x2 x ->
TcbMod.join x1´ x1´´ x1 ->
TcbJoin tid vl x1´´1 x1´´ ->
exists x´, TcbJoin tid vl x´ x.
Lemma tcbdllseg_get_last_tcb_ptr:
forall l s P head headpre tail x ,
s |= tcbdllseg head headpre tail x l ** P ->
get_last_tcb_ptr l head = Some x.
Lemma unmap_inrtbl´: forall (x y i i0 : int32) (rtbl : vallist),
i <> Int.zero ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
Int.unsigned i <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
prio_in_tbl ($ Int.unsigned ((x<<$ 3)+ᵢy)) rtbl.
Lemma not_add_os_stat_q:
Int.unsigned ($ OS_STAT_Q&Int.not ($ OS_STAT_Q)) = 0.
Lemma z_le_n_lt:
forall x1, Int.unsigned x1 <= 7 ->
(Z.to_nat (Int.unsigned x1) < ∘OS_RDY_TBL_SIZE)%nat.
Lemma os_stat_q_not_and:
(Int.eq ($ OS_STAT_Q&Int.not ($ OS_STAT_Q)) ($ OS_STAT_RDY) = true).
Lemma tcb_join_join_joinsig´:
forall x1 x2 x x1´ x1´´ tid vl x1´´1,
TcbMod.join x1 x2 x ->
TcbMod.join x1´ x1´´ x2 ->
TcbJoin tid vl x1´´1 x1´´ ->
exists x´, TcbJoin tid vl x´ x.
Close Scope code_scope.
Require Import mathlib.
Open Scope code_scope.
Lemma z_le_n_lt´:
forall x1,
Int.unsigned x1 <= 7 ->
(Z.to_nat (Int.unsigned x1) < ∘OS_EVENT_TBL_SIZE)%nat.
Lemma pos_to_nat_range_0_7:
forall z, 0<=z -> z<=7 -> (0<=Z.to_nat z<=7)%nat.
Lemma osmapvallist_prop:forall x, (Int.unsigned x <=7) -> exists i, nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 i /\ Int.unsigned i <= 128.
Lemma unsigned_int_and_not_range:
forall x y,
Int.unsigned x <= 255 ->
Int.unsigned y<=255 ->
Int.unsigned (x&Int.not y) <=? 255 = true.
Lemma shl3_add_le_255:
forall x1 x2,
Int.unsigned x1 <= 7 ->
Int.unsigned x2 <= 7 ->
Int.unsigned ((x1<<$ 3)+ᵢx2) <64.
Lemma shl3_add_le_255´:
forall x1 x2,
Int.unsigned x1 <= 7 ->
Int.unsigned x2 <= 7 ->
((Z.to_nat (Int.unsigned ((x1<<$ 3)+ᵢx2))) <64) %nat.
Lemma rl_etbl_ptbl_p:
forall l egrp i4 v´33 x6 v´22 etbl tcbls ptbl etype av,
array_type_vallist_match Int8u etbl ->
length etbl = ∘OS_RDY_TBL_SIZE ->
R_ECB_ETbl_P l
(etype
:: Vint32 egrp
:: Vint32 i4 :: Vptr (v´33, Int.zero)
:: x6 :: v´22 :: nil,
etbl) tcbls ->
RL_Tbl_Grp_P etbl (Vint32 egrp) ->
R_PrioTbl_P ptbl tcbls av->
RL_RTbl_PrioTbl_P etbl ptbl av.
Lemma tcb_join_disj_get:
forall tcbls1 tcbls2 tcbls tid x,
TcbMod.join tcbls1 tcbls2 tcbls ->
TcbMod.get tcbls tid = Some x ->
(TcbMod.get tcbls1 tid = Some x /\ TcbMod.get tcbls2 tid = None)
\/(TcbMod.get tcbls2 tid = Some x /\ TcbMod.get tcbls1 tid = None).
Lemma last_eq:
forall x2 (x4 : vallist),
(last (x2 ++ x4 :: nil) nil) = x4.
Lemma tcbdllseg_isvptr:
forall l s p1 tail1 ct p z,
s |= tcbdllseg p1 z tail1 (Vptr ct) l ** p -> exists x, p1 = Vptr x.
Lemma tcbdllseg_split´:
forall x1 s P v´23 v´32 x2 x3 xx y,
s |= tcbdllseg (Vptr v´23) xx v´32 (Vptr y) (x1 ++ x2 :: x3) ** P ->
s |= EX x v´15,
tcbdllseg (Vptr v´23) xx x (Vptr v´15) x1 **
tcbdllseg (Vptr v´15) x v´32 (Vptr y) (x2 :: x3)** [|x1<>nil /\ nth_val 0 (last x1 nil) = Some (Vptr v´15) \/ x1 = nil /\ Vptr v´15 = Vptr v´23 |] ** P.
Lemma list_app_neq_nil:
forall x2 (x4 : vallist),
(x2 ++ x4 :: nil <> nil).
Lemma join_sig_minus_tcb : forall m a x, TcbMod.get m a = Some x -> TcbMod.join (TcbMod.sig a x) (TcbMod.minus m (TcbMod.sig a x)) m.
Lemma tcb_get_ex_tcbjoin:
forall x tid y,
TcbMod.get x tid = Some y ->
exists a, TcbJoin tid y a x.
Lemma in_ptbl_no_ct_get:
forall s x tid ptbl tcbls tcbls1 tcbls2 p1 l1 rtbl ct curtcb l2 tail1 tail2 P av ,
ct <> tid ->
tid <> av ->
0 <= Int.unsigned x < 64 ->
R_PrioTbl_P ptbl tcbls av->
nth_val´ ∘(Int.unsigned x) ptbl = Vptr tid ->
TcbMod.join tcbls1 tcbls2 tcbls ->
TCBList_P p1 l1 rtbl tcbls1 ->
TCBList_P (Vptr ct) (curtcb :: l2) rtbl tcbls2 ->
s |= tcbdllseg p1 Vnull tail1 (Vptr ct) l1 ** tcbdllseg (Vptr ct) tail1 tail2 Vnull (curtcb :: l2) ** P ->
(
s|= (EX tail1´ l1´ tidtcb l1´´ tcbls1´ tcbls1´´,
tcbdllseg p1 Vnull tail1´ (Vptr tid) l1´ **
tcbdllseg (Vptr tid) tail1´ tail1 (Vptr ct) (tidtcb::l1´´) **
tcbdllseg (Vptr ct) tail1 tail2 Vnull (curtcb :: l2) **
[| TCBList_P p1 l1´ rtbl tcbls1´|] **
[| TCBList_P (Vptr tid) (tidtcb::l1´´) rtbl tcbls1´´ |] **
[| TcbMod.join tcbls1´ tcbls1´´ tcbls1|] **
[| l1 = l1´++(tidtcb::l1´´) |] ** P)
\\//
(EX tail2´ l2´ tidtcb l2´´ tcbls2´ tcbls2´´,
tcbdllseg p1 Vnull tail1 (Vptr ct) l1 **
tcbdllseg (Vptr ct) tail1 tail2´ (Vptr tid) (curtcb :: l2´) **
tcbdllseg (Vptr tid) tail2´ tail2 Vnull (tidtcb::l2´´) **
[| TCBList_P (Vptr ct) (curtcb::l2´) rtbl tcbls2´|] **
[| TCBList_P (Vptr tid) (tidtcb::l2´´) rtbl tcbls2´´|] **
[| TcbMod.join tcbls2´ tcbls2´´ tcbls2|] **
[| l2 = l2´++(tidtcb::l2´´) |] ** P)
).
Lemma tcb_join_join_joinsig:
forall x1 x2 x x1´ x1´´ tid vl x1´´1,
TcbMod.join x1 x2 x ->
TcbMod.join x1´ x1´´ x1 ->
TcbJoin tid vl x1´´1 x1´´ ->
exists x´, TcbJoin tid vl x´ x.
Lemma tcbdllseg_get_last_tcb_ptr:
forall l s P head headpre tail x ,
s |= tcbdllseg head headpre tail x l ** P ->
get_last_tcb_ptr l head = Some x.
Lemma unmap_inrtbl´: forall (x y i i0 : int32) (rtbl : vallist),
i <> Int.zero ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
Int.unsigned i <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
prio_in_tbl ($ Int.unsigned ((x<<$ 3)+ᵢy)) rtbl.
Lemma not_add_os_stat_q:
Int.unsigned ($ OS_STAT_Q&Int.not ($ OS_STAT_Q)) = 0.
Lemma z_le_n_lt:
forall x1, Int.unsigned x1 <= 7 ->
(Z.to_nat (Int.unsigned x1) < ∘OS_RDY_TBL_SIZE)%nat.
Lemma os_stat_q_not_and:
(Int.eq ($ OS_STAT_Q&Int.not ($ OS_STAT_Q)) ($ OS_STAT_RDY) = true).
Lemma tcb_join_join_joinsig´:
forall x1 x2 x x1´ x1´´ tid vl x1´´1,
TcbMod.join x1 x2 x ->
TcbMod.join x1´ x1´´ x2 ->
TcbJoin tid vl x1´´1 x1´´ ->
exists x´, TcbJoin tid vl x´ x.
Close Scope code_scope.