Library OSQAcceptPure
Require Export mathlib.
Lemma rh_tcbls_mqls_p_getmsg_hold:
forall mqls tcbls ct a v vl qmax wl,
RH_TCBList_ECBList_P mqls tcbls ct ->
EcbMod.get mqls a =
Some
(absmsgq (v:: vl) qmax, wl) ->
RH_TCBList_ECBList_P (EcbMod.set mqls a (absmsgq vl qmax, wl)) tcbls ct.
Lemma msgqnode_p_nomsg:
forall qptr qst qend qin qout size qens qblk mblk ml A l,
Int.ltu ($ 0) qens = false ->
RLH_ECBData_P
(
DMsgQ l (qptr
:: qst
:: qend
:: qin
:: qout
:: Vint32 size :: Vint32 qens :: Vptr qblk :: nil)
mblk ml) A ->
exists qmax wl, A = (absmsgq nil qmax,wl).
Lemma msgqnode_p_hold_end:
forall b sti qens outi qend qptr qst qin qsize qblk mblk ml hml hsize wl l,
id_addrval qblk msgqueuetbl OS_Q_FREEBLK = Some (b, sti) ->
Int.ltu ($ 0) qens =true ->
qend = Vptr (b, (outi +ᵢ Int.mul ($ 1) ($ 4))) ->
WellformedOSQ
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: Vint32 qsize :: Vint32 qens :: Vptr qblk :: nil) ->
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: Vint32 qsize :: Vint32 qens :: Vptr qblk :: nil)
mblk ml)
(absmsgq (nth_val´ (Z.to_nat ((Int.unsigned outi - Int.unsigned sti) / 4)) ml
:: hml) hsize, wl) ->
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: qst
:: Vint32 qsize
:: Vint32 (qens -ᵢ $ 1) :: Vptr qblk :: nil)
mblk ml ) (absmsgq hml hsize, wl).
Lemma msgqnode_p_hold_no_end:
forall b sti qens outi qend qptr qst qin qsize qblk mblk ml hml hsize wl l,
id_addrval qblk msgqueuetbl OS_Q_FREEBLK = Some (b, sti) ->
length ml = ∘OS_MAX_Q_SIZE ->
WellformedOSQ
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: Vint32 qsize :: Vint32 qens :: Vptr qblk :: nil) ->
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: Vint32 qsize :: Vint32 qens :: Vptr qblk :: nil)
mblk ml)
(absmsgq (nth_val´ (Z.to_nat ((Int.unsigned outi - Int.unsigned sti) / 4)) ml
:: hml) hsize, wl) ->
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi +ᵢ Int.mul ($ 1) ($ 4))
:: Vint32 qsize
:: Vint32 (qens -ᵢ $ 1) :: Vptr qblk :: nil)
mblk ml ) (absmsgq hml hsize, wl).
Lemma h_has_same_msg:
forall b qptr qst qend qin outi qsize qens qblk sti l qblkm vl hml,
Int.ltu ($ 0) qens = true ->
id_addrval qblk msgqueuetbl OS_Q_FREEBLK = Some (b, sti) ->
length vl = ∘OS_MAX_Q_SIZE ->
WellformedOSQ
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: qsize :: Vint32 qens :: Vptr qblk:: nil) ->
RLH_ECBData_P (DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: qsize :: Vint32 qens :: Vptr qblk:: nil)
qblkm vl) hml ->
exists vl´ max wl, hml = (absmsgq ((nth_val´ (Z.to_nat ((Int.unsigned outi - Int.unsigned sti) / 4)) vl) :: vl´) max , wl).
Lemma get_wellformedosq_end:
forall x qptr st b i qin qout size ens qfr,
ens = Vint32 x ->
Int.ltu Int.zero x = true ->
WellformedOSQ
(qptr
:: st
:: Vptr (b, i +ᵢ Int.mul ($ 1) ($ 4))
:: qin :: qout :: size :: ens :: qfr :: nil) ->
WellformedOSQ
(qptr
:: st
:: Vptr (b, i +ᵢ Int.mul ($ 1) ($ 4))
:: qin
:: st
:: size
:: val_inj (sub ens (Vint32 (Int.repr 1)) Tint16)
:: qfr :: nil).
Lemma get_wellformedosq_end´:
forall x qptr st b i qin size ens qfr qend,
ens = Vint32 x ->
qend <> Vptr (b, i +ᵢ Int.mul ($ 1) ($ 4)) ->
WellformedOSQ
(qptr
:: st
:: qend
:: qin :: Vptr (b, i) :: size :: ens :: qfr :: nil) ->
WellformedOSQ
(qptr
:: st
:: qend
:: qin
:: Vptr (b, i +ᵢ Int.mul ($ 1) ($ 4))
:: size
:: val_inj (sub ens (Vint32 (Int.repr 1)) Tint16)
:: qfr :: nil).
Lemma msgqlist_p_compose:
forall p qid mqls qptrl1 qptrl2 i i1 a x3 p´ v´41
msgqls1 msgqls2 msgq mqls1 mqls2 mq mqls´ tcbls,
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´ mqls ->
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) mqls tcbls.
Lemma osq_same_blk_st_out´
: 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´, qout = Vptr (b, i´).
Lemma wellq_props:
forall x12 x11 x5 x6 v´49 x i2 i1 v´47 x13 x14 v2 v´46,
length v2 = ∘OS_MAX_Q_SIZE ->
Int.ltu ($ 0) i1 = true ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x12
:: x11
:: x5
:: x6
:: Vptr (v´49, x)
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x13 :: x14 :: nil) v2) v´46 ->
WellformedOSQ
(x12
:: x11
:: x5
:: x6
:: Vptr (v´49, x)
:: 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) /\
rule_type_val_match (Void) ∗
(nth_val´
(Z.to_nat
((Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4))
v2) = true.
Require Import lab.
Lemma qacc_absinfer_no_msg:
forall P mqls x qmaxlen wl,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq nil qmaxlen,wl) ->
absinfer
(<|| qacc (Vptr x :: nil) ||> ** HECBList mqls ** P)
(<|| END Some Vnull ||> ** HECBList mqls ** P).
Lemma qacc_absinfer_get_msg:
forall P mqls x qmaxlen wl v vl v1 v3 v4 ,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq (v::vl) qmaxlen,wl) ->
absinfer
(<|| qacc (Vptr x :: nil) ||> **
HECBList mqls ** HTCBList v1 ** HTime v3 ** HCurTCB v4 ** P)
(<|| END Some v ||> ** HECBList (EcbMod.set mqls x (absmsgq vl qmaxlen,wl)) ** HTCBList v1 ** HTime v3 ** HCurTCB v4 ** P).
Lemma qacc_absinfer_null:
forall P, can_change_aop P ->
absinfer (<|| qacc (Vnull :: nil) ||> ** P) (<|| END (Some Vnull) ||> ** P).
Lemma qacc_absinfer_no_q :
forall P mqls x,
can_change_aop P ->
(~ exists a b wl,EcbMod.get mqls x = Some (absmsgq a b,wl)) ->
absinfer (<|| qacc (Vptr x :: nil) ||> ** HECBList mqls ** P)
(<|| END Some Vnull ||> ** HECBList mqls ** P).
Ltac join_get_solver :=
match goal with
| H: OSAbstMod.join (OSAbstMod.sig ?x ?y) _ ?O |- OSAbstMod.get ?O ?x = Some ?y =>
eapply OSAbstMod.join_get_get_l; eauto
| H: OSAbstMod.join ?O1 ?O2 ?O |- OSAbstMod.get ?O ?x = Some ?y =>
eapply OSAbstMod.join_get_get_r; [eauto | join_get_solver]
end.
Lemma absinfer_conseq_pre :
forall p´ p q,
⊢ p ⇒ q -> p´ ==> p -> ⊢ p´ ⇒ q .
Lemma rh_tcbls_mqls_p_getmsg_hold:
forall mqls tcbls ct a v vl qmax wl,
RH_TCBList_ECBList_P mqls tcbls ct ->
EcbMod.get mqls a =
Some
(absmsgq (v:: vl) qmax, wl) ->
RH_TCBList_ECBList_P (EcbMod.set mqls a (absmsgq vl qmax, wl)) tcbls ct.
Lemma msgqnode_p_nomsg:
forall qptr qst qend qin qout size qens qblk mblk ml A l,
Int.ltu ($ 0) qens = false ->
RLH_ECBData_P
(
DMsgQ l (qptr
:: qst
:: qend
:: qin
:: qout
:: Vint32 size :: Vint32 qens :: Vptr qblk :: nil)
mblk ml) A ->
exists qmax wl, A = (absmsgq nil qmax,wl).
Lemma msgqnode_p_hold_end:
forall b sti qens outi qend qptr qst qin qsize qblk mblk ml hml hsize wl l,
id_addrval qblk msgqueuetbl OS_Q_FREEBLK = Some (b, sti) ->
Int.ltu ($ 0) qens =true ->
qend = Vptr (b, (outi +ᵢ Int.mul ($ 1) ($ 4))) ->
WellformedOSQ
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: Vint32 qsize :: Vint32 qens :: Vptr qblk :: nil) ->
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: Vint32 qsize :: Vint32 qens :: Vptr qblk :: nil)
mblk ml)
(absmsgq (nth_val´ (Z.to_nat ((Int.unsigned outi - Int.unsigned sti) / 4)) ml
:: hml) hsize, wl) ->
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: qst
:: Vint32 qsize
:: Vint32 (qens -ᵢ $ 1) :: Vptr qblk :: nil)
mblk ml ) (absmsgq hml hsize, wl).
Lemma msgqnode_p_hold_no_end:
forall b sti qens outi qend qptr qst qin qsize qblk mblk ml hml hsize wl l,
id_addrval qblk msgqueuetbl OS_Q_FREEBLK = Some (b, sti) ->
length ml = ∘OS_MAX_Q_SIZE ->
WellformedOSQ
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: Vint32 qsize :: Vint32 qens :: Vptr qblk :: nil) ->
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: Vint32 qsize :: Vint32 qens :: Vptr qblk :: nil)
mblk ml)
(absmsgq (nth_val´ (Z.to_nat ((Int.unsigned outi - Int.unsigned sti) / 4)) ml
:: hml) hsize, wl) ->
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi +ᵢ Int.mul ($ 1) ($ 4))
:: Vint32 qsize
:: Vint32 (qens -ᵢ $ 1) :: Vptr qblk :: nil)
mblk ml ) (absmsgq hml hsize, wl).
Lemma h_has_same_msg:
forall b qptr qst qend qin outi qsize qens qblk sti l qblkm vl hml,
Int.ltu ($ 0) qens = true ->
id_addrval qblk msgqueuetbl OS_Q_FREEBLK = Some (b, sti) ->
length vl = ∘OS_MAX_Q_SIZE ->
WellformedOSQ
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: qsize :: Vint32 qens :: Vptr qblk:: nil) ->
RLH_ECBData_P (DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: Vptr (b, outi)
:: qsize :: Vint32 qens :: Vptr qblk:: nil)
qblkm vl) hml ->
exists vl´ max wl, hml = (absmsgq ((nth_val´ (Z.to_nat ((Int.unsigned outi - Int.unsigned sti) / 4)) vl) :: vl´) max , wl).
Lemma get_wellformedosq_end:
forall x qptr st b i qin qout size ens qfr,
ens = Vint32 x ->
Int.ltu Int.zero x = true ->
WellformedOSQ
(qptr
:: st
:: Vptr (b, i +ᵢ Int.mul ($ 1) ($ 4))
:: qin :: qout :: size :: ens :: qfr :: nil) ->
WellformedOSQ
(qptr
:: st
:: Vptr (b, i +ᵢ Int.mul ($ 1) ($ 4))
:: qin
:: st
:: size
:: val_inj (sub ens (Vint32 (Int.repr 1)) Tint16)
:: qfr :: nil).
Lemma get_wellformedosq_end´:
forall x qptr st b i qin size ens qfr qend,
ens = Vint32 x ->
qend <> Vptr (b, i +ᵢ Int.mul ($ 1) ($ 4)) ->
WellformedOSQ
(qptr
:: st
:: qend
:: qin :: Vptr (b, i) :: size :: ens :: qfr :: nil) ->
WellformedOSQ
(qptr
:: st
:: qend
:: qin
:: Vptr (b, i +ᵢ Int.mul ($ 1) ($ 4))
:: size
:: val_inj (sub ens (Vint32 (Int.repr 1)) Tint16)
:: qfr :: nil).
Lemma msgqlist_p_compose:
forall p qid mqls qptrl1 qptrl2 i i1 a x3 p´ v´41
msgqls1 msgqls2 msgq mqls1 mqls2 mq mqls´ tcbls,
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´ mqls ->
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) mqls tcbls.
Lemma osq_same_blk_st_out´
: 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´, qout = Vptr (b, i´).
Lemma wellq_props:
forall x12 x11 x5 x6 v´49 x i2 i1 v´47 x13 x14 v2 v´46,
length v2 = ∘OS_MAX_Q_SIZE ->
Int.ltu ($ 0) i1 = true ->
RLH_ECBData_P
(DMsgQ (Vptr (v´47, Int.zero))
(x12
:: x11
:: x5
:: x6
:: Vptr (v´49, x)
:: Vint32 i2
:: Vint32 i1 :: Vptr (v´49, Int.zero) :: nil)
(x13 :: x14 :: nil) v2) v´46 ->
WellformedOSQ
(x12
:: x11
:: x5
:: x6
:: Vptr (v´49, x)
:: 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) /\
rule_type_val_match (Void) ∗
(nth_val´
(Z.to_nat
((Int.unsigned x - Int.unsigned (Int.zero+ᵢ($ 4+ᵢInt.zero))) / 4))
v2) = true.
Require Import lab.
Lemma qacc_absinfer_no_msg:
forall P mqls x qmaxlen wl,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq nil qmaxlen,wl) ->
absinfer
(<|| qacc (Vptr x :: nil) ||> ** HECBList mqls ** P)
(<|| END Some Vnull ||> ** HECBList mqls ** P).
Lemma qacc_absinfer_get_msg:
forall P mqls x qmaxlen wl v vl v1 v3 v4 ,
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq (v::vl) qmaxlen,wl) ->
absinfer
(<|| qacc (Vptr x :: nil) ||> **
HECBList mqls ** HTCBList v1 ** HTime v3 ** HCurTCB v4 ** P)
(<|| END Some v ||> ** HECBList (EcbMod.set mqls x (absmsgq vl qmaxlen,wl)) ** HTCBList v1 ** HTime v3 ** HCurTCB v4 ** P).
Lemma qacc_absinfer_null:
forall P, can_change_aop P ->
absinfer (<|| qacc (Vnull :: nil) ||> ** P) (<|| END (Some Vnull) ||> ** P).
Lemma qacc_absinfer_no_q :
forall P mqls x,
can_change_aop P ->
(~ exists a b wl,EcbMod.get mqls x = Some (absmsgq a b,wl)) ->
absinfer (<|| qacc (Vptr x :: nil) ||> ** HECBList mqls ** P)
(<|| END Some Vnull ||> ** HECBList mqls ** P).
Ltac join_get_solver :=
match goal with
| H: OSAbstMod.join (OSAbstMod.sig ?x ?y) _ ?O |- OSAbstMod.get ?O ?x = Some ?y =>
eapply OSAbstMod.join_get_get_l; eauto
| H: OSAbstMod.join ?O1 ?O2 ?O |- OSAbstMod.get ?O ?x = Some ?y =>
eapply OSAbstMod.join_get_get_r; [eauto | join_get_solver]
end.
Lemma absinfer_conseq_pre :
forall p´ p q,
⊢ p ⇒ q -> p´ ==> p -> ⊢ p´ ⇒ q .