Library common
Require Export include.
Require Export memory.
Require Export memdata.
Require Export assertion.
Require Export absop.
Require Export simulation.
Require Export language.
Require Export opsem.
Require Export os_program.
Require Export os_spec.
Require Export inferules.
Require Export os_code_notations.
Require Export os_code_defs.
Require Export os_ucos_h.
Require Export os_time.
Require Export baseTac.
Require Export auxdef.
Require Export seplog_lemmas.
Require Export seplog_tactics.
Require Export derivedrules.
Require Export hoare_conseq.
Require Export symbolic_execution.
Require Export hoare_assign.
Require Export hoare_lemmas.
Require Export BaseAsrtDef.
Require Export inv_prop.
Require Export InternalFunSpec.
Require Export IntLib.
Require Export List.
Require Export can_change_aop_proof.
Require Export cancel_absdata.
Require Export hoare_tactics.
Require Export type_val_match.
Require Export init_spec.
Require Export sep_pure.
Require Export mathsolver.
Require Export absop_rules.
Require Import Coq.Logic.FunctionalExtensionality.
Set Implicit Arguments.
Close Scope nat_scope.
Open Scope Z_scope.
Open Scope code_scope.
Lemma isr_is_prop_emp:
forall i ir, isr_is_prop (isrupd ir i false) (i :: nil) -> (isrupd ir i false) = empisr.
Lemma a_isr_is_prop_split:
forall s P isr is, s |= Aisr isr ** Ais is ** A_isr_is_prop ** P -> s |= Aisr isr ** Ais is ** P ** [| isr_is_prop isr is |].
Lemma retpost_osev : retpost OS_EventSearchPost.
Definition prio_neq_cur tcbls curtid curprio :=
forall tid prio st m,
tid <> curtid ->
TcbMod.get tcbls tid = Some (prio, st, m) ->
prio <> curprio.
Lemma abst_disj_merge_set_eqq
: forall (x y : absdatastru.B) (id : absdataidspec.A)
(O Of : OSAbstMod.map),
OSAbstMod.disj O Of ->
OSAbstMod.get O id = Some x ->
OSAbstMod.merge Of (OSAbstMod.set O id y) =
OSAbstMod.set (OSAbstMod.merge Of O) id y.
Definition array_struct t :=
(exists t1 n, t = Tarray t1 n) \/ (exists id dl, t = Tstruct id dl) \/ ( t = Tvoid).
Lemma tarray_tvoid :
forall t , ~array_struct t -> typelen t <> 0%nat.
Lemma type_encode_nnil :
forall t v, ~array_struct t -> encode_val t v <> nil.
Lemma join_sub_sub_sig_neq:
forall x1 x2 m a b m1 m2,
MemMod.join x1 x2 m ->
MemMod.sub (MemMod.sig a m1) x1 ->
MemMod.sub (MemMod.sig b m2) x2 ->
a <> b.
Ltac eq_case x a := let H0 := fresh in let H0´ := fresh in remember (Classical_Prop.classic (x=a)) as H0 eqn: H0´; clear H0´; destruct H0.
Lemma ptomval_nnil_neq:
forall v1 v2 x y x1 x2 m,
v1 <> nil ->
v2 <> nil ->
MemMod.join x1 x2 m ->
ptomvallist x v1 x1 ->
ptomvallist y v2 x2 ->
x <> y.
Lemma pv_false :
forall s x y t1 t2 v1 v2 P,
~array_struct t1 ->
~ array_struct t2 ->
s |= PV x @ t1 |-> v1 ** PV y @ t2 |-> v2 ** P-> x <> y.
Lemma astruct_neq_ptr : forall s x id1 t1 d1 id2 t2 d2 v1 y v2 P a b,
~array_struct t1 ->
~ array_struct t2 ->
s |= Astruct x (STRUCT id1 { dcons a t1 d1 }) v1
** Astruct y (STRUCT id2 { dcons b t2 d2 }) v2 ** P -> x <> y .
Lemma ecbf_sllseg_isptr : forall s P v1 v2 t f, s |= ecbf_sllseg v1 Vnull
v2 t f ** P -> isptr v1.
Lemma evsllseg_get_last_eq :
forall ls1 head tail ls2 s, ls1 <> nil ->
s |= evsllseg head tail ls1 ls2 -> get_last_ptr ls1 = Some tail.
Lemma evsllseg_merge :
forall l1 l1´ l2 l2´ x1 x2 y s P,
length l1 = length l1´ ->
length l2 = length l2´ ->
s |= evsllseg x1 y l1 l1´ ** evsllseg y x2 l2 l2´ ** P->
s |= evsllseg x1 x2 (l1++l2) (l1´++l2´) **P.
Lemma Aarray_vl_len_eq:
forall vl s n t P l,
s |= Aarray l (Tarray t n) vl ** P -> length vl = n.
Lemma Aarray_vl_len_eq´:
forall vl s n t P l,
s |= Aarray l (Tarray t n) vl ** P -> s|= Aarray l (Tarray t n) vl ** P **[|length vl = n|].
Lemma sep_pure_split:forall s P A, s|=[|P|]**A -> (P /\ s|=A).
Lemma sep_pure_get:forall s P A, s|=[|P|]**A -> (P /\ s|= [|P|] ** A).
Lemma absimp_pre_compose: forall p1 p2 q,
absinfer p1 q -> absinfer p2 q -> absinfer (p1\\//p2) q.
Lemma absimp_conseq_pre: forall p q p´, absinfer p q -> p´==>p -> absinfer p´ q.
Lemma absimp_conseq_post: forall p q q´, absinfer p q -> q ==> q´ -> absinfer p q´.
Lemma absimp_pre_post_compose: forall p1 p2 q1 q2,
absinfer p1 q1 -> absinfer p2 q2 -> absinfer (p1\\//p2) (q1\\//q2).
Lemma absimp_ex_intro:
forall (tp:Type) (p:tp->asrt) q, (forall x,absinfer (p x) q) -> absinfer (EX x:tp,p x) q.
Lemma evsllseg_add_head: forall head tailnext vl ecbl s P tl l x msgq, V_OSEventListPtr l = Some head -> s|= AEventNode tl l x msgq ** evsllseg head tailnext vl ecbl ** P -> s|= evsllseg tl tailnext ((l, x) :: vl) (msgq ::ecbl) ** P.
Lemma evsllseg_app: forall head mid vl0 ecbl0 tail vl1 ecbl1 P s, s|= evsllseg head mid vl0 ecbl0 ** evsllseg mid tail vl1 ecbl1 ** P -> s|= evsllseg head tail (vl0++vl1) (ecbl0++ecbl1) ** P.
Lemma evsllseg_compose:
forall s P (qptrl:list EventCtr) l x p msgqls tail vn qptrl1 qptrl2 msgqls1 msgqls2 tl msgq,
V_OSEventListPtr l = Some vn ->
qptrl = qptrl1 ++ ((l,x)::nil) ++ qptrl2 ->
msgqls = msgqls1 ++ (msgq::nil) ++msgqls2 ->
s |= AEventNode tl l x msgq **
evsllseg p tl qptrl1 msgqls1 **
evsllseg vn tail qptrl2 msgqls2 ** P ->
s |= evsllseg p tail qptrl msgqls ** P.
Lemma elim_a_isr_is_prop:
forall P, Aisr empisr ** Ais nil ** A_isr_is_prop ** P ==> Aisr empisr ** Ais nil ** P.
Lemma add_a_isr_is_prop:
forall P, Aisr empisr ** Ais nil ** P ==> Aisr empisr ** Ais nil ** A_isr_is_prop ** P.
Lemma tcbdllseg_compose:
forall s P h hp t1 tn1 t2 tn2 l1 l2,
s |= tcbdllseg h hp t1 tn1 l1 ** tcbdllseg tn1 t1 t2 tn2 l2 ** P->
s |= tcbdllseg h hp t2 tn2 (l1++l2) ** P.
Lemma evsllseg_isptr : forall {p1 l1 l2 s P},
s |= evsllseg p1 Vnull l1 l2 ** P -> isptr p1.
Lemma sep_ptr_neq_OS_EVENT : forall p1 vl1 p2 vl2 s P,
s |= Astruct p1 OS_EVENT vl1 ** Astruct p2 OS_EVENT vl2 ** P ->
p1 <> p2.
Lemma evsllseg_list_len_eq : forall l1 l2 p1 p2 s P,
s |= evsllseg p1 p2 l1 l2 ** P -> length l1 = length l2.
Lemma disj_conj_distrib_pre : forall (P Q R S: asrt) s a b c d sc,
{|a, b, c, d, sc|} |- {{(P//\\R)\\//(Q//\\R)}} s {{S}} ->
{|a, b, c, d, sc|} |- {{(P\\//Q)//\\R}} s {{S}}.
Lemma topis_0_imp:
forall s x si P,
s|=ATopis x ** Ais (0%nat::si) ** P ->
x =0%nat.
Lemma isrclr_imp :
forall P,
isrclr ** P ==> Aisr empisr ** P.
Lemma imp_isrclr:
forall P,
Aisr empisr ** P ==> isrclr ** P.
Lemma topis_nil:forall s x P ,s |= ATopis x ** Ais nil ** P -> x = INUM.
Lemma atopis_pure:forall s P x, s|= ATopis x ** P -> s|= P.
Lemma tcbblk_prio_range:
forall a p,
RL_TCBblk_P a ->
V_OSTCBPrio a = Some (Vint32 p) ->
0<= Int.unsigned p < 64.
Fixpoint get_eid_list´ (vll:list EventCtr):=
match vll with
| nil => nil
| (vl,x)::vll´ => (nth_val´ 5%nat vl) :: (get_eid_list´ vll´)
end.
Definition get_eid_list (head:val) (vll:list EventCtr):=
head:: (List.removelast (get_eid_list´ vll)).
Definition vl_elem_neq (l:vallist):= forall n m vn vm,nth_val n l = Some vn -> nth_val m l = Some vm -> n <> m -> vn <> vm.
Lemma nth_val_nth_val´_some_eq : forall n vl x,
nth_val n vl = Some x -> nth_val´ n vl = x.
Import MemMod.
Lemma join_merge : forall {m1 m2 m3}, join m1 m2 m3 -> m3 = merge m1 m2.
Lemma disj_join_disj : forall m1 m2 m3 m4 m5 m6,
join m1 m2 m3 -> join m4 m5 m6 -> disj m3 m6 ->
disj m1 m4.
Lemma length_encode_val : forall t v, (typelen t > 0)%nat -> (length (encode_val t v) > 0)%nat.
Lemma length_exists: forall {A:Type} (l: list A), (length l > 0)%nat -> exists h t, l = h :: t.
Lemma mapstoval_disj_false : forall a t v1 v2 m1 m2,
(typelen t > 0)%nat -> mapstoval a t v1 m1 -> mapstoval a t v2 m2 -> MemMod.disj m1 m2 ->
False.
Lemma Astruct_osevent_dup_false :
forall p v1 v1´ s,
s |= Astruct p OS_EVENT v1 ** Astruct p OS_EVENT v1´ -> False.
Lemma Astruct_osevent_dup_false´ :
forall p v1 v1´ s P,
s |= Astruct p OS_EVENT v1 ** Astruct p OS_EVENT v1´ ** P -> False.
Lemma AEventNode_dup_false :
forall p v1 v2 v3 v4 e1 e2 P s,
s |= AEventNode p v1 v2 e1 ** AEventNode p v3 v4 e2 ** P ->
False.
Lemma aeventnode_evsllseg_get_neq : forall ectrl edatal head head´ n v v0 e x tail s P,
s |= AEventNode head v v0 e ** evsllseg head´ tail ectrl edatal ** P-> ectrl <> nil ->
nth_val n (get_eid_list head´ ectrl) = Some x -> head <> x.
Lemma aeventnode_evsllseg_get_neq´ : forall ectrl edatal head head´ n v v0 e x tail s,
s |= AEventNode head v v0 e ** evsllseg head´ tail ectrl edatal -> ectrl <> nil ->
nth_val n (get_eid_list head´ ectrl) = Some x -> head <> x.
Lemma evsllseg_eid_neq:
forall ectrl edatal head tail s P, s |= evsllseg head tail ectrl edatal ** P -> vl_elem_neq (get_eid_list head ectrl).
Lemma ecb_joinsig_ex_split:
forall x x0 x1 ecbls x3 x4,
EcbMod.joinsig x x0 x1 ecbls ->
EcbMod.join x3 x4 x1 ->
exists y, EcbMod.joinsig x x0 x3 y /\ EcbMod.join y x4 ecbls.
Lemma ecblist_p_decompose:
forall l1 ll1 l2 ll2 head ecbls tcbls,
length l1 = length ll1 ->
ECBList_P head Vnull
(l1++
l2) (ll1 ++ ll2) ecbls tcbls ->
exists ecbls1 ecbls2 x,
ECBList_P head x l1 ll1 ecbls1 tcbls /\
ECBList_P x Vnull l2 ll2 ecbls2 tcbls /\
EcbMod.join ecbls1 ecbls2 ecbls.
Lemma ecb_sub_eq:
forall h ecbls h´ x x4 x5 x1 x2,
EcbMod.sub h ecbls ->
EcbMod.sub h´ ecbls ->
EcbMod.joinsig x x4 x5 h ->
EcbMod.joinsig x x1 x2 h´->
x5 = x2 ->
h = h´.
Lemma ecblist_p_eqh:
forall l h h´ ecbls head tail1 tail2 ll tcbls,
EcbMod.sub h ecbls ->
EcbMod.sub h´ ecbls ->
ECBList_P head tail1 l ll h tcbls ->
ECBList_P head tail2 l ll h´ tcbls ->
tail1 = tail2 /\ h = h´.
Lemma eventtype_neq_q:
forall v´38 v´21 i1 i0 i2 x2 x3 v´42 v´40 v´22 v´23 v´41 v´24 v´34 v´35 v´49 s P v´43 v´45 v´44 v´46,
length v´21 = length v´23->
ECBList_P v´38 Vnull
(v´21 ++
((Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil,
v´40) :: nil) ++ v´22) (v´23 ++ (v´41 :: nil) ++ v´24) v´34 v´35 ->
ECBList_P v´38 (Vptr (v´49, Int.zero)) v´21 v´23 v´43 v´35 ->
EcbMod.join v´43 v´45 v´34 ->
EcbMod.joinsig (v´49, Int.zero) v´46 v´44 v´45 ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = false ->
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 ** P ->
s |= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 **
[|~ exists x y z, EcbMod.get v´34 (v´49,Int.zero) = Some (absmsgq x y, z) |] ** P.
Fixpoint RL_PrioTbl_P (ptbl : vallist) (tcbls : list vallist) (vhold:addrval) {struct tcbls}:=
match tcbls with
| nil => True
| l::tcbls´ =>
match
V_OSTCBPrio l with
| Some (Vint32 prio) =>
(exists x,nth_val (nat_of_Z (Int.unsigned prio)) ptbl = Some (Vptr x) /\ x <> vhold ) /\ RL_PrioTbl_P ptbl tcbls´ vhold
| _ => False
end
end.
Fixpoint RL_TCBListblk_P l :=
match l with
| nil => True
| a::l´ => RL_TCBblk_P a /\ RL_TCBListblk_P l´
end.
Lemma imp_rl_priotbl_p:
forall ltls ptbl htls p rtbl vhold,
R_PrioTbl_P ptbl htls vhold->
TCBList_P p ltls rtbl htls ->
RL_PrioTbl_P ptbl ltls vhold.
Lemma tcbdllseg_split:
forall x1 s P v´23 v´32 x2 x3 xx,
s |= tcbdllseg (Vptr v´23) xx v´32 Vnull (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 Vnull (x2 :: x3)** [|x1<>nil /\ nth_val 0 (last x1 nil) = Some (Vptr v´15) \/ x1 = nil /\ Vptr v´15 = Vptr v´23 |] ** P.
Require Export memory.
Require Export memdata.
Require Export assertion.
Require Export absop.
Require Export simulation.
Require Export language.
Require Export opsem.
Require Export os_program.
Require Export os_spec.
Require Export inferules.
Require Export os_code_notations.
Require Export os_code_defs.
Require Export os_ucos_h.
Require Export os_time.
Require Export baseTac.
Require Export auxdef.
Require Export seplog_lemmas.
Require Export seplog_tactics.
Require Export derivedrules.
Require Export hoare_conseq.
Require Export symbolic_execution.
Require Export hoare_assign.
Require Export hoare_lemmas.
Require Export BaseAsrtDef.
Require Export inv_prop.
Require Export InternalFunSpec.
Require Export IntLib.
Require Export List.
Require Export can_change_aop_proof.
Require Export cancel_absdata.
Require Export hoare_tactics.
Require Export type_val_match.
Require Export init_spec.
Require Export sep_pure.
Require Export mathsolver.
Require Export absop_rules.
Require Import Coq.Logic.FunctionalExtensionality.
Set Implicit Arguments.
Close Scope nat_scope.
Open Scope Z_scope.
Open Scope code_scope.
Lemma isr_is_prop_emp:
forall i ir, isr_is_prop (isrupd ir i false) (i :: nil) -> (isrupd ir i false) = empisr.
Lemma a_isr_is_prop_split:
forall s P isr is, s |= Aisr isr ** Ais is ** A_isr_is_prop ** P -> s |= Aisr isr ** Ais is ** P ** [| isr_is_prop isr is |].
Lemma retpost_osev : retpost OS_EventSearchPost.
Definition prio_neq_cur tcbls curtid curprio :=
forall tid prio st m,
tid <> curtid ->
TcbMod.get tcbls tid = Some (prio, st, m) ->
prio <> curprio.
Lemma abst_disj_merge_set_eqq
: forall (x y : absdatastru.B) (id : absdataidspec.A)
(O Of : OSAbstMod.map),
OSAbstMod.disj O Of ->
OSAbstMod.get O id = Some x ->
OSAbstMod.merge Of (OSAbstMod.set O id y) =
OSAbstMod.set (OSAbstMod.merge Of O) id y.
Definition array_struct t :=
(exists t1 n, t = Tarray t1 n) \/ (exists id dl, t = Tstruct id dl) \/ ( t = Tvoid).
Lemma tarray_tvoid :
forall t , ~array_struct t -> typelen t <> 0%nat.
Lemma type_encode_nnil :
forall t v, ~array_struct t -> encode_val t v <> nil.
Lemma join_sub_sub_sig_neq:
forall x1 x2 m a b m1 m2,
MemMod.join x1 x2 m ->
MemMod.sub (MemMod.sig a m1) x1 ->
MemMod.sub (MemMod.sig b m2) x2 ->
a <> b.
Ltac eq_case x a := let H0 := fresh in let H0´ := fresh in remember (Classical_Prop.classic (x=a)) as H0 eqn: H0´; clear H0´; destruct H0.
Lemma ptomval_nnil_neq:
forall v1 v2 x y x1 x2 m,
v1 <> nil ->
v2 <> nil ->
MemMod.join x1 x2 m ->
ptomvallist x v1 x1 ->
ptomvallist y v2 x2 ->
x <> y.
Lemma pv_false :
forall s x y t1 t2 v1 v2 P,
~array_struct t1 ->
~ array_struct t2 ->
s |= PV x @ t1 |-> v1 ** PV y @ t2 |-> v2 ** P-> x <> y.
Lemma astruct_neq_ptr : forall s x id1 t1 d1 id2 t2 d2 v1 y v2 P a b,
~array_struct t1 ->
~ array_struct t2 ->
s |= Astruct x (STRUCT id1 { dcons a t1 d1 }) v1
** Astruct y (STRUCT id2 { dcons b t2 d2 }) v2 ** P -> x <> y .
Lemma ecbf_sllseg_isptr : forall s P v1 v2 t f, s |= ecbf_sllseg v1 Vnull
v2 t f ** P -> isptr v1.
Lemma evsllseg_get_last_eq :
forall ls1 head tail ls2 s, ls1 <> nil ->
s |= evsllseg head tail ls1 ls2 -> get_last_ptr ls1 = Some tail.
Lemma evsllseg_merge :
forall l1 l1´ l2 l2´ x1 x2 y s P,
length l1 = length l1´ ->
length l2 = length l2´ ->
s |= evsllseg x1 y l1 l1´ ** evsllseg y x2 l2 l2´ ** P->
s |= evsllseg x1 x2 (l1++l2) (l1´++l2´) **P.
Lemma Aarray_vl_len_eq:
forall vl s n t P l,
s |= Aarray l (Tarray t n) vl ** P -> length vl = n.
Lemma Aarray_vl_len_eq´:
forall vl s n t P l,
s |= Aarray l (Tarray t n) vl ** P -> s|= Aarray l (Tarray t n) vl ** P **[|length vl = n|].
Lemma sep_pure_split:forall s P A, s|=[|P|]**A -> (P /\ s|=A).
Lemma sep_pure_get:forall s P A, s|=[|P|]**A -> (P /\ s|= [|P|] ** A).
Lemma absimp_pre_compose: forall p1 p2 q,
absinfer p1 q -> absinfer p2 q -> absinfer (p1\\//p2) q.
Lemma absimp_conseq_pre: forall p q p´, absinfer p q -> p´==>p -> absinfer p´ q.
Lemma absimp_conseq_post: forall p q q´, absinfer p q -> q ==> q´ -> absinfer p q´.
Lemma absimp_pre_post_compose: forall p1 p2 q1 q2,
absinfer p1 q1 -> absinfer p2 q2 -> absinfer (p1\\//p2) (q1\\//q2).
Lemma absimp_ex_intro:
forall (tp:Type) (p:tp->asrt) q, (forall x,absinfer (p x) q) -> absinfer (EX x:tp,p x) q.
Lemma evsllseg_add_head: forall head tailnext vl ecbl s P tl l x msgq, V_OSEventListPtr l = Some head -> s|= AEventNode tl l x msgq ** evsllseg head tailnext vl ecbl ** P -> s|= evsllseg tl tailnext ((l, x) :: vl) (msgq ::ecbl) ** P.
Lemma evsllseg_app: forall head mid vl0 ecbl0 tail vl1 ecbl1 P s, s|= evsllseg head mid vl0 ecbl0 ** evsllseg mid tail vl1 ecbl1 ** P -> s|= evsllseg head tail (vl0++vl1) (ecbl0++ecbl1) ** P.
Lemma evsllseg_compose:
forall s P (qptrl:list EventCtr) l x p msgqls tail vn qptrl1 qptrl2 msgqls1 msgqls2 tl msgq,
V_OSEventListPtr l = Some vn ->
qptrl = qptrl1 ++ ((l,x)::nil) ++ qptrl2 ->
msgqls = msgqls1 ++ (msgq::nil) ++msgqls2 ->
s |= AEventNode tl l x msgq **
evsllseg p tl qptrl1 msgqls1 **
evsllseg vn tail qptrl2 msgqls2 ** P ->
s |= evsllseg p tail qptrl msgqls ** P.
Lemma elim_a_isr_is_prop:
forall P, Aisr empisr ** Ais nil ** A_isr_is_prop ** P ==> Aisr empisr ** Ais nil ** P.
Lemma add_a_isr_is_prop:
forall P, Aisr empisr ** Ais nil ** P ==> Aisr empisr ** Ais nil ** A_isr_is_prop ** P.
Lemma tcbdllseg_compose:
forall s P h hp t1 tn1 t2 tn2 l1 l2,
s |= tcbdllseg h hp t1 tn1 l1 ** tcbdllseg tn1 t1 t2 tn2 l2 ** P->
s |= tcbdllseg h hp t2 tn2 (l1++l2) ** P.
Lemma evsllseg_isptr : forall {p1 l1 l2 s P},
s |= evsllseg p1 Vnull l1 l2 ** P -> isptr p1.
Lemma sep_ptr_neq_OS_EVENT : forall p1 vl1 p2 vl2 s P,
s |= Astruct p1 OS_EVENT vl1 ** Astruct p2 OS_EVENT vl2 ** P ->
p1 <> p2.
Lemma evsllseg_list_len_eq : forall l1 l2 p1 p2 s P,
s |= evsllseg p1 p2 l1 l2 ** P -> length l1 = length l2.
Lemma disj_conj_distrib_pre : forall (P Q R S: asrt) s a b c d sc,
{|a, b, c, d, sc|} |- {{(P//\\R)\\//(Q//\\R)}} s {{S}} ->
{|a, b, c, d, sc|} |- {{(P\\//Q)//\\R}} s {{S}}.
Lemma topis_0_imp:
forall s x si P,
s|=ATopis x ** Ais (0%nat::si) ** P ->
x =0%nat.
Lemma isrclr_imp :
forall P,
isrclr ** P ==> Aisr empisr ** P.
Lemma imp_isrclr:
forall P,
Aisr empisr ** P ==> isrclr ** P.
Lemma topis_nil:forall s x P ,s |= ATopis x ** Ais nil ** P -> x = INUM.
Lemma atopis_pure:forall s P x, s|= ATopis x ** P -> s|= P.
Lemma tcbblk_prio_range:
forall a p,
RL_TCBblk_P a ->
V_OSTCBPrio a = Some (Vint32 p) ->
0<= Int.unsigned p < 64.
Fixpoint get_eid_list´ (vll:list EventCtr):=
match vll with
| nil => nil
| (vl,x)::vll´ => (nth_val´ 5%nat vl) :: (get_eid_list´ vll´)
end.
Definition get_eid_list (head:val) (vll:list EventCtr):=
head:: (List.removelast (get_eid_list´ vll)).
Definition vl_elem_neq (l:vallist):= forall n m vn vm,nth_val n l = Some vn -> nth_val m l = Some vm -> n <> m -> vn <> vm.
Lemma nth_val_nth_val´_some_eq : forall n vl x,
nth_val n vl = Some x -> nth_val´ n vl = x.
Import MemMod.
Lemma join_merge : forall {m1 m2 m3}, join m1 m2 m3 -> m3 = merge m1 m2.
Lemma disj_join_disj : forall m1 m2 m3 m4 m5 m6,
join m1 m2 m3 -> join m4 m5 m6 -> disj m3 m6 ->
disj m1 m4.
Lemma length_encode_val : forall t v, (typelen t > 0)%nat -> (length (encode_val t v) > 0)%nat.
Lemma length_exists: forall {A:Type} (l: list A), (length l > 0)%nat -> exists h t, l = h :: t.
Lemma mapstoval_disj_false : forall a t v1 v2 m1 m2,
(typelen t > 0)%nat -> mapstoval a t v1 m1 -> mapstoval a t v2 m2 -> MemMod.disj m1 m2 ->
False.
Lemma Astruct_osevent_dup_false :
forall p v1 v1´ s,
s |= Astruct p OS_EVENT v1 ** Astruct p OS_EVENT v1´ -> False.
Lemma Astruct_osevent_dup_false´ :
forall p v1 v1´ s P,
s |= Astruct p OS_EVENT v1 ** Astruct p OS_EVENT v1´ ** P -> False.
Lemma AEventNode_dup_false :
forall p v1 v2 v3 v4 e1 e2 P s,
s |= AEventNode p v1 v2 e1 ** AEventNode p v3 v4 e2 ** P ->
False.
Lemma aeventnode_evsllseg_get_neq : forall ectrl edatal head head´ n v v0 e x tail s P,
s |= AEventNode head v v0 e ** evsllseg head´ tail ectrl edatal ** P-> ectrl <> nil ->
nth_val n (get_eid_list head´ ectrl) = Some x -> head <> x.
Lemma aeventnode_evsllseg_get_neq´ : forall ectrl edatal head head´ n v v0 e x tail s,
s |= AEventNode head v v0 e ** evsllseg head´ tail ectrl edatal -> ectrl <> nil ->
nth_val n (get_eid_list head´ ectrl) = Some x -> head <> x.
Lemma evsllseg_eid_neq:
forall ectrl edatal head tail s P, s |= evsllseg head tail ectrl edatal ** P -> vl_elem_neq (get_eid_list head ectrl).
Lemma ecb_joinsig_ex_split:
forall x x0 x1 ecbls x3 x4,
EcbMod.joinsig x x0 x1 ecbls ->
EcbMod.join x3 x4 x1 ->
exists y, EcbMod.joinsig x x0 x3 y /\ EcbMod.join y x4 ecbls.
Lemma ecblist_p_decompose:
forall l1 ll1 l2 ll2 head ecbls tcbls,
length l1 = length ll1 ->
ECBList_P head Vnull
(l1++
l2) (ll1 ++ ll2) ecbls tcbls ->
exists ecbls1 ecbls2 x,
ECBList_P head x l1 ll1 ecbls1 tcbls /\
ECBList_P x Vnull l2 ll2 ecbls2 tcbls /\
EcbMod.join ecbls1 ecbls2 ecbls.
Lemma ecb_sub_eq:
forall h ecbls h´ x x4 x5 x1 x2,
EcbMod.sub h ecbls ->
EcbMod.sub h´ ecbls ->
EcbMod.joinsig x x4 x5 h ->
EcbMod.joinsig x x1 x2 h´->
x5 = x2 ->
h = h´.
Lemma ecblist_p_eqh:
forall l h h´ ecbls head tail1 tail2 ll tcbls,
EcbMod.sub h ecbls ->
EcbMod.sub h´ ecbls ->
ECBList_P head tail1 l ll h tcbls ->
ECBList_P head tail2 l ll h´ tcbls ->
tail1 = tail2 /\ h = h´.
Lemma eventtype_neq_q:
forall v´38 v´21 i1 i0 i2 x2 x3 v´42 v´40 v´22 v´23 v´41 v´24 v´34 v´35 v´49 s P v´43 v´45 v´44 v´46,
length v´21 = length v´23->
ECBList_P v´38 Vnull
(v´21 ++
((Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil,
v´40) :: nil) ++ v´22) (v´23 ++ (v´41 :: nil) ++ v´24) v´34 v´35 ->
ECBList_P v´38 (Vptr (v´49, Int.zero)) v´21 v´23 v´43 v´35 ->
EcbMod.join v´43 v´45 v´34 ->
EcbMod.joinsig (v´49, Int.zero) v´46 v´44 v´45 ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = false ->
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 ** P ->
s |= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 **
[|~ exists x y z, EcbMod.get v´34 (v´49,Int.zero) = Some (absmsgq x y, z) |] ** P.
Fixpoint RL_PrioTbl_P (ptbl : vallist) (tcbls : list vallist) (vhold:addrval) {struct tcbls}:=
match tcbls with
| nil => True
| l::tcbls´ =>
match
V_OSTCBPrio l with
| Some (Vint32 prio) =>
(exists x,nth_val (nat_of_Z (Int.unsigned prio)) ptbl = Some (Vptr x) /\ x <> vhold ) /\ RL_PrioTbl_P ptbl tcbls´ vhold
| _ => False
end
end.
Fixpoint RL_TCBListblk_P l :=
match l with
| nil => True
| a::l´ => RL_TCBblk_P a /\ RL_TCBListblk_P l´
end.
Lemma imp_rl_priotbl_p:
forall ltls ptbl htls p rtbl vhold,
R_PrioTbl_P ptbl htls vhold->
TCBList_P p ltls rtbl htls ->
RL_PrioTbl_P ptbl ltls vhold.
Lemma tcbdllseg_split:
forall x1 s P v´23 v´32 x2 x3 xx,
s |= tcbdllseg (Vptr v´23) xx v´32 Vnull (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 Vnull (x2 :: x3)** [|x1<>nil /\ nth_val 0 (last x1 nil) = Some (Vptr v´15) \/ x1 = nil /\ Vptr v´15 = Vptr v´23 |] ** P.