Library lemmasfortoptheo
Require Import include.
Require Import inferules.
Require Import language.
Require Import opsem.
Require Import etraceref.
Require Import assertion.
Require Import memdata.
Require Import memory.
Require Import Map.
Require Import simulation.
Require Import Omega.
Require Import includeLib.
Require Import soundness.
Require Import auxdef.
Require Import Classical.
Require Import progtaskstepLib.
Require Import tacticsforseplog.
Require Import baseTac.
Import OSAbstMod.
Lemma projs_eqg:forall (o : env * EnvSpec.B * mem * isr * LocalStSpec.B)
(Sl : osstate) (t : tid),
projS Sl t = Some o -> fst (fst (fst (fst Sl))) = fst (fst (fst (fst o))).
Import OSAbstMod.
Lemma join_storebytes_storebytes : forall vl b i M1 M1´ M2 M,
MemMod.join M1 M2 M ->
storebytes M1 (b, i) vl = Some M1´ ->
exists M´, storebytes M (b, i) vl = Some M´.
Lemma join_store_general : forall Mc Mc´ Ml M tp l v,
MemMod.join Ml Mc M ->
store tp Mc l v = Some Mc´ ->
exists M´, store tp M l v = Some M´.
Lemma join_store:forall Mc Mc´ Ml M tp b t,
MemMod.join Ml Mc M ->
store tp Mc (b,0%Z) (Vptr t) = Some Mc´ ->
exists M´,
store tp M (b,0%Z) (Vptr t) = Some M´.
Lemma part_storebytes_part : forall vl Tm Tl Ml Mc b o t Mc´, partM Ml Tl Tm -> TMSpecMod.maps_to Tm t Mc -> storebytes Mc (b, o) vl = Some Mc´ ->
exists Ml´, storebytes Ml (b, o) vl = Some Ml´ /\ partM Ml´ Tl (TMSpecMod.put Tm t Mc´).
Lemma part_store_part: forall Tm Tl Ml Mc l v t tp Mc´, partM Ml Tl Tm -> TMSpecMod.maps_to Tm t Mc -> store tp Mc l v = Some Mc´ -> exists Ml´,store tp Ml l v = Some Ml´ /\ partM Ml´ Tl (TMSpecMod.put Tm t Mc´).
Lemma disj_storebytes_disj : forall vl M1 M2 M1´ b o, MemMod.disj M1 M2 -> storebytes M1 (b, o) vl = Some M1´ -> MemMod.disj M1´ M2.
Lemma disj_store_disj:forall M1 M2 M1´ t l v ,MemMod.disj M1 M2 -> store t M1 l v = Some M1´ -> MemMod.disj M1´ M2.
Lemma merge_store_merge:forall M1 M2 m t l v M1´ m´,MemMod.merge M1 M2 = m -> store t M1 l v = Some M1´ -> store t m l v = Some m´ -> MemMod.merge M1´ M2 = m´.
Lemma join_store_join:forall Ml Mc M t l v Mc´ M´, MemMod.join Ml Mc M -> store t Mc l v = Some Mc´ -> store t M l v = Some M´ -> MemMod.join Ml Mc´ M´.
Lemma disj_get_eq:forall O Os a x x´, OSAbstMod.disj O Os -> OSAbstMod.get O a = Some x -> OSAbstMod.get (OSAbstMod.merge O Os) a = Some x´ -> x = x´.
Require Import lmachLib.
Lemma storebytes_set : forall l M M´ b o o´ a, storebytes M (b, o) l = Some M´ -> (o´ < o)%Z -> storebytes (MemMod.set M (b, o´) a) (b, o) l = Some (MemMod.set M´ (b, o´) a).
Lemma mem_disj_merge_minus_disj´
: forall Ml Mc´ Ms Ms´ Mc´0 Mcc tp l v ,
store tp Mc´ l v = Some Mcc ->
MemMod.disj Mc´0 Ms´ ->
MemMod.merge Mc´0 Ms´ = MemMod.merge Mcc Ms ->
MemMod.disj Ml Ms ->
MemMod.sub Mc´ Ml ->
MemMod.disj (MemMod.merge (MemMod.minus Ml Mc´) Mc´0) Ms´.
Lemma mem_disj_merge_minus_merge´
: forall Ml Mc Ms Ms´ Mc´ m Mcc m´ v l tp,
store tp Mc l v = Some Mcc ->
store tp m l v= Some m´ ->
MemMod.disj Mc´ Ms´ ->
MemMod.merge Mc´ Ms´ = MemMod.merge Mcc Ms ->
MemMod.disj Ml Ms ->
MemMod.sub Mc Ml ->
MemMod.merge Ml Ms =m ->
MemMod.merge (MemMod.merge (MemMod.minus Ml Mc) Mc´) Ms´ = m´.
Lemma store_sub_minus_eq:forall Ml M Ml´ tp l v, MemMod.sub Ml M -> store tp Ml l v = Some Ml´ -> MemMod.minus M Ml = MemMod.minus M Ml´.
Lemma sub_disj_disj:forall M1 M2 Ms Ml, MemMod.disj Ml Ms -> MemMod.sub M2 Ml -> MemMod.sub M1 (MemMod.merge M2 Ms) -> MemMod.disj (MemMod.minus Ml M2) M1.
Lemma store_disj_merge:forall M M1 Ms M2 tp l v, MemMod.disj M (MemMod.merge M1 Ms) -> store tp M1 l v = Some M2 -> MemMod.disj M (MemMod.merge M2 Ms).
Lemma store_sub_disj_disj:
forall M1 M2 Ms Ml M2´ tp l v,
store tp M2 l v = Some M2´ ->
MemMod.disj Ml Ms ->
MemMod.sub M2 Ml ->
MemMod.sub M1 (MemMod.merge M2´ Ms) ->
MemMod.disj (MemMod.minus Ml M2´) M1.
Lemma merge_set_eq:forall O O´ x y, merge (set O x y) O´ = set (merge O O´) x y.
Lemma disj_indom_set_disj: forall O O´ x y, indom O x -> disj O O´ ->
disj (set O x y) O´.
Lemma swpre_store:forall ge le Mc ir au O ab x tp b t sc,
((ge, le, Mc, ir, au), O, ab) |= SWPRE x sc->
EnvMod.get ge OSTCBCur = Some (b, tp) ->
exists Mc´,
store tp Mc (b,0%Z) (Vptr t) = Some Mc´.
Lemma store_join_store : forall t v l M1 M2 M3, (exists M1´, store t M1 l v = Some M1´) ->
MemMod.join M1 M2 M3 ->
exists M3´, store t M3 l v = Some M3´.
Qed.
Lemma GoodI_SWINV_indom_curt:
forall I o O sc, GoodI I sc ->
(forall ab, (o, O, ab) |= SWINV I) ->
OSAbstMod.indom O curtid.
Lemma goodI_swinv_samet:
forall ge le M ir au O ab I tid sc,
GoodI I sc->
(ge, le, M, ir, au, O, ab) |= SWINV I ->
(ge, le, M, ir, au, O, ab) |= AHprio sc tid ** Atrue ->
(exists b tp v tid, EnvMod.get ge OSTCBCur = Some (b,(Tptr tp)) /\
load (Tptr tp) M (b,0%Z) = Some v /\ OSAbstMod.get O curtid = Some (oscurt tid)) /\
( forall b tp M´, OSAbstMod.get O curtid = Some (oscurt tid) -> EnvMod.get ge OSTCBCur = Some (b,(Tptr tp)) -> store (Tptr tp) M (b,0%Z) (Vptr tid) = Some M´ -> (ge, le, M´, ir, au, O, ab) |= SWINV I).
Lemma swi_rdy_inv´´´:forall (o : taskst) (Ol Os : map) (Ms Mc : MemMod.map)
(I : Inv) (t t´ : tid) (S : osstate)
(o´ : env * EnvSpec.B * mem * isr * LocalStSpec.B) b tp Mcc sc,
good_is_S S ->
GoodI I sc->
disj Ol Os ->
MemMod.disj Mc Ms ->
(forall ab : absop, (substaskst o Ms, Os, ab) |= INV I) ->
(forall ab : absop, (substaskst o Mc, Ol, ab) |= SWINV I) ->
(forall ab : absop, (substaskst o Mc, Ol, ab) |= AHprio sc t´ ** Atrue) ->
projS S t = Some o ->
projS S t´ = Some o´ ->
EnvMod.get (get_genv (get_smem o)) OSTCBCur = Some (b,(Tptr tp)) ->
store (Tptr tp) Mc (b,0%Z) (Vptr t´) = Some Mcc ->
exists Mc´ Ms´ Ol´ Os´,
MemMod.disj Mc´ Ms´ /\
MemMod.merge Mc´ Ms´ = MemMod.merge Mcc Ms /\
disj Ol´ Os´ /\
merge Ol´ Os´ = set (merge Ol Os) curtid (oscurt t´) /\
(forall ab : absop, (substaskst o´ Ms´, Os´, ab) |= INV I) /\
(forall ab : absop, (substaskst o´ Mc´, Ol´, ab) |= RDYINV I).
Lemma p_eq: forall (pc po pi pc0 po0 pi0:progunit) (ip ip0:intunit), (pc, (po, pi, ip)) = (pc0, (po0, pi0, ip0)) -> pc = pc0/\ po=po0/\pi=pi0/\ip=ip0.
Lemma code_eq_dec: forall (c c´:code), c=c´\/c<>c´.
Lemma stmts_dec: forall (s:stmts) s´, s= s´ \/ s<>s´.
Lemma ret_dec:forall c ke ks,~ ((c, (ke, ks)) = (curs sret, (kenil, ks)) /\ callcont ks = None/\intcont ks=None)\/((c, (ke, ks)) = (curs sret, (kenil, ks)) /\ callcont ks = None/\intcont ks=None).
Lemma retv_dec: forall c ke ks, ~(exists v ksx, (c,(ke,ks))= (curs (sskip (Some v)),(kenil,kret ksx))/\callcont ksx = None/\intcont ksx=None) \/ (exists v ksx, (c,(ke,ks))= (curs (sskip (Some v)),(kenil,kret ksx))/\callcont ksx = None/\intcont ksx=None).
Lemma exint_dec: forall c ke ks, ((c,(ke,ks)) = (curs (sprim exint),(kenil,ks))/\callcont ks=None/\intcont ks=None)\/ ~((c,(ke,ks)) = (curs (sprim exint),(kenil,ks))/\callcont ks=None/\intcont ks=None).
Lemma IntSeq´´:
forall pc (po:progunit) pi ip A p c ke ks t I r
lenv si isrreg (oi:taskst) o O Oi M ab absi c´ ke´ ks´ i ch keh ksh ge,
no_call_api_os po pi ip ->
no_call_api (c´,(ke´,ks´)) po->
GoodI I (snd A)->
OSAbstMod.disj O Oi ->
joinmem oi M o ->
r = iretasrt i isrreg si I ge ->
(snd (fst A)) i = Some absi ->
TaskSim (pc,(po,pi,ip)) (c,(ke,ks)) ((ge,lenv,M),(isrupd isrreg i false),(true,si,nil)) (pc,A) (ch,(keh,ksh)) O t I p ->
goodks (pc,(po,pi,ip)) (ks´##kint c ke lenv ks) ->
MethSim pi (snd A) (c´,(ke´,ks´)) oi ab Oi I retfalse r retfalse ->
InOS (c´,(ke´, ks´## kint c ke lenv ks)) (pumerge po pi) ->
TaskSim (pc,(po,pi,ip)) (c´,(ke´, ks´## kint c ke lenv ks)) o (pc,A) (curs (hapi_code ab),(kenil,kevent ch keh ksh)) (OSAbstMod.merge Oi O) t I p.
Inductive lintstep´ : hid -> intunit -> code -> taskst -> code -> taskst -> Prop :=
li_step : forall (C : code) (c : cureval) (ke : exprcont)
(ks : stmtcont) (ir : isr) (si : is)
(i : hid),
forall (s : stmts) (theta : intunit) (ge le : env) (m : mem),
C = (c, (ke, ks)) ->
higherint ir i ->
i < INUM ->
theta i = Some s ->
lintstep´ i theta C (ge, le, m, ir, (true, si, nil))
(curs s, (kenil, kint c ke le ks))
(ge, empenv, m, isrupd ir i true, (false, i :: si, nil)).
Lemma IntSeq´: forall pc po pi ip (A:osspec) o´ O Oi Mi I ch keh ksh c ke ks Mc t s Ms Os Ms´ Os´ p lenv ge le m ir ie is cs sh i,
ip i = Some s ->
(snd (fst A)) i = Some sh->
no_call_api_os po pi ip ->
GoodI I (snd A)->
TaskSim (pc,(po,pi,ip)) ( c, (ke, ks)) (substaskst ((ge,le,m),ir,(ie,is,cs)) Mc) (pc,A) (ch,(keh,ksh)) O t I p ->
fst (fst (get_smem ((ge,le,m),ir,(ie,is,cs)))) = ge ->
lintstep´ i ip (c ,(ke, ks)) ((ge,le,m),ir,(ie,is,cs)) ((curs s), (kenil, (kint c ke lenv ks))) o´ ->
(forall ab, sat (((substaskst ((ge,le,m),ir,(ie,is,cs)) Ms),Os),ab) (INV I)) ->
(forall ab, sat (((substaskst o´ Ms´),Os´),ab) (INV I)) ->
Os = OSAbstMod.merge Oi Os´->
OSAbstMod.disj Oi Os´ ->
OSAbstMod.disj O Os ->
MemMod.disj Mi Ms´->
MemMod.disj Mc Ms ->
Ms = MemMod.merge Mi Ms´ ->
(
forall (i:hid) ispec isrreg si G ,
(snd (fst A)) i = Some ispec ->
(
exists (s:stmts) p r,
ip i = Some s /\
p = ipreasrt i isrreg si ispec I G/\
r = iretasrt i isrreg si I G/\
MethSimAsrt pi (snd A) I retfalse r p s Afalse
)
)->
eqdomOS (po,pi,ip) A ->
goodks (pc,(po,pi,ip)) ks->
TaskSim (pc,(po,pi,ip)) ((curs s), (kenil, (kint c ke lenv ks)))
(substaskst o´ (MemMod.merge Mc Mi)) (pc,A) ((curs (hapi_code sh)), (kenil, kevent ch keh ksh)) (OSAbstMod.merge O Oi) t I p.
Lemma inos_lift: forall v ks po pi,
~ InOS (SKIP, (kenil, ks)) (pumerge po pi) ->
~ InOS (curs (sskip v), (kenil, ks)) (pumerge po pi).
Lemma GoodStmt_to_GoodStmt´: forall s p, GoodStmt s p ->GoodStmt´ s.
Lemma goodstmt´_n_dym_com_s: forall s, GoodStmt´ s -> n_dym_com_s s.
Lemma n_dym_ks_call: forall ks´ ks f s, n_dym_com_int_scont (ks´##kcall f s empenv ks) -> n_dym_com_int_scont ks.
Lemma goodstmt_n_dym_com_s: forall s p , GoodStmt s p-> n_dym_com_s s.
Lemma pumerge_get_ex:forall p p´ f t d1 d2 s, (pumerge p p´) f= Some (t,d1,d2,s) -> p f =Some (t,d1,d2,s)\/ p´ f = Some (t,d1,d2,s).
Lemma callcont_ndymint:forall ks f s le ks´, callcont ks = Some (kcall f s le ks´) -> n_dym_com_int_scont ks -> n_dym_com_int_scont ks´.
Lemma ltstep_n_dym_com_int_cd:
forall pc po pi ip t c´ ke´ ks´ c´´ ke´´ ks´´ cst o cst´ o´,
(forall f t d1 d2 s, po f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
(forall f t d1 d2 s, pi f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
GoodClient pc po pi ->
ltstep (pc,(po,pi,ip)) t (c´, (ke´, ks´ )) cst o (c´´, (ke´´, ks´´ )) cst´ o´ -> n_dym_com_int_cd (c´, (ke´, ks´ )) -> n_dym_com_int_cd (c´´, (ke´´, ks´´ )).
Lemma int_ndymint_false:forall ks c ke le ks´, intcont ks = Some (kint c ke le ks´) -> ~(n_dym_com_int_scont ks).
Qed.
Lemma ltstepev_n_dym_com_int_cd:
forall pc po pi ip t c´ ke´ ks´ c´´ ke´´ ks´´ cst o cst´ o´ ev,
(forall f t d1 d2 s, po f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
(forall f t d1 d2 s, pi f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
GoodClient pc po pi ->
ltstepev (pc,(po,pi,ip)) t (c´, (ke´, ks´ )) cst o (c´´, (ke´´, ks´´ )) cst´ o´ ev-> n_dym_com_int_cd (c´, (ke´, ks´ )) -> n_dym_com_int_cd (c´´, (ke´´, ks´´ )).
Definition no_fun_same (p1 p2:progunit):=
(forall f, p1 f <> None -> p2 f = None) /\ forall f, (p2 f <> None -> p1 f = None).
Lemma tlmatch_dec´:forall tl dl (vl:vallist), ~(tlmatch tl dl/\ dl_vl_match dl (rev vl)=true)\/ (tlmatch tl dl /\ dl_vl_match dl (rev vl)=true).
Lemma funbody´_inos: forall s po pi f ft d1 d2 s´, GoodStmt´ s-> po f = Some (ft,d1,d2,s´) -> InOS (curs s,(kenil, kcall f s´ empenv kstop)) (pumerge po pi).
Lemma cstep_no_api_elim:
forall po pi c ke ks c´ ke´ ks´ o o´,
no_call_api (c,(ke,ks)) po ->
cstep (pumerge po pi) (c, (ke, ks)) o (c´, (ke´, ks´)) o´ ->
cstep pi (c, (ke, ks)) o (c´, (ke´, ks´)) o´.
Lemma loststep_no_api_elim:
forall po pi c ke ks c´ ke´ ks´ o o´,
no_call_api (c,(ke,ks)) po ->
loststep (pumerge po pi) (c, (ke, ks)) o (c´, (ke´, ks´)) o´ ->
loststep pi (c, (ke, ks)) o (c´, (ke´, ks´)) o´.
Lemma XXXX: forall ksx f s kstop ks, ksx ## (kcall f s empenv kstop ## ks) = ksx ## kcall f s empenv kstop ## ks.
Lemma SmCTaskSim´:
forall (pc po pi:progunit) (ip:intunit) (A:osspec) I o O (tid:tid) c ke ks1 ks2 ks ch keh,
no_fun_same po pi ->
no_call_api_os po pi ip ->
True ->
(forall f t d1 d2 s, po f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
(forall f t d1 d2 s, pi f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
(
forall (f:fid) ab vl p r ft G,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA po f (ab,ft) vl G->
Some r = BuildRetA po f (ab,ft) vl G->
(
exists t d1 d2 s,
po f = Some (t, d1, d2, s)/\
GoodStmt´ s /\
MethSimAsrt pi (snd A) I r Afalse p s Afalse
)
) ->
(eqdomOS (po,pi,ip) A /\GoodClient pc po pi/\ goodks (pc,(po,pi,ip)) (ks1##(ks2##ks))/\n_dym_com_int_cd (c,(ke,ks1##(ks2##ks)))/\ good_clt (SKIP, (kenil,ks)) pi/\ True)->
(
(~InOS (c,(ke,ks)) (pumerge po pi) /\
(c=ch/\ke=keh/\ks1=kstop/\ks2=kstop)) \/
(exists f vl tl s d1 d2 ft,
po f = Some (ft,d1,d2,s)/\ c = curs (sfexec f vl tl)/\ ke=kenil/\ ch =c /\keh=kenil/\
ks1=kstop/\ks2=kstop/\~InOS (SKIP,(kenil,ks)) (pumerge po pi))\/
(exists f vl , exists dl vlh s d1 d2 ft tl,
po f = Some (ft,d1,d2,s) /\ c =curs (salloc vl dl)/\ke=kenil/\
ch = curs (sfexec f vlh tl)/\keh=kenil/\
ks1=kstop/\ks2=kcall f s EnvMod.emp kstop/\
~InOS (SKIP,(kenil,ks)) (pumerge po pi))\/
(exists f s d1 d2 ft,
po f = Some (ft,d1,d2,s)/\ keh=kenil/\ks2=kcall f s EnvMod.emp kstop/\
(forall vl dl,(c,(ke,ks1))<>(curs (salloc vl dl),(kenil,kstop)))/\
(forall al v, ~ (c=curs (sfree al v) /\ callcont ks1 = None/\intcont ks1=None))/\
~InOS (SKIP,(kenil,ks)) (pumerge po pi))\/
(exists (al:freelist) f s d1 d2 ft v,
po f = Some (ft,d1,d2,s)/\ keh=kenil/\ks2=kcall f s EnvMod.emp kstop/\ ke=kenil/\
c=curs (sfree al v)/\ callcont ks1 = None /\ intcont ks1 =None/\
~InOS (SKIP,(kenil,ks)) (pumerge po pi))
)->
(
~InOS (c,(ke,ks)) (pumerge po pi) ->
c=ch-> ke=keh -> ks1=kstop -> ks2=kstop ->
InitTaskSt (pair o O) /\ good_clt (c,(ke,ks)) pi
) ->
(
forall f vl tl s d1 d2 ft,
po f = Some (ft,d1,d2,s)-> c = curs (sfexec f vl tl) -> ke=kenil -> ch =c -> keh=kenil->
ks1=kstop -> ks2=kstop -> ~InOS (SKIP,(kenil,ks)) (pumerge po pi) ->
InitTaskSt (pair o O)
) ->
(
(forall f vl dl vlh s d1 d2 ft tl,
po f = Some (ft,d1,d2,s)-> c =curs (salloc vl dl)->ke=kenil->
ch = curs (sfexec f vlh tl)->
ks1=kstop -> ks2=kcall f s EnvMod.emp kstop ->
~InOS (SKIP,(kenil,ks)) (pumerge po pi) ->
(
tlmatch (List.rev tl) d1 /\ tl_vl_match tl vlh =true /\ good_dl_le dl o /\ True /\
exists dl´ vl´ p,
(vl<>nil -> length_eq vl´ dl´) /\
dl_add dl´ dl=revlcons d1 d2/\ vl´ ++ vl = vlh/\buildp dl´ vl´=Some p /\
(forall ab,sat ((o,O),ab) ((p ** (Aie true) ** (Ais nil)** (Acs nil) ** (Aisr empisr))** A_dom_lenv (getlenvdom dl´)))))
) ->
(
forall f s d1 d2 ft ab tt,
po f = Some (ft,d1,d2,s) -> keh=kenil -> ks2=kcall f s EnvMod.emp kstop ->
(forall vl dl,(c,(ke,ks1))<>(curs (salloc vl dl),(kenil,kstop)))->
(forall al v, ~ (c=curs (sfree al v) /\ callcont ks1 = None/\intcont ks1=None))->
~InOS (SKIP,(kenil,ks)) (pumerge po pi) ->
(fst (fst A)) f = Some (ab,tt) ->
(exists R vlh AC, InOS (c,(ke,ks1##kcall f s EnvMod.emp kstop)) (pumerge po pi)/\ch = curs (hapi_code AC) /\Some R = BuildRetA po f (ab,tt) vlh (get_genv (get_smem o)) /\ no_call_api (c,(ke,ks1)) po /\
{{[ pi, (snd A), I, R, Afalse, retfalse]}} ||-
((c,(ke,ks1)), o) <_msim (AC, O) )
)->
(
forall (al:freelist) f s d1 d2 ft v,
po f = Some (ft,d1,d2,s) -> keh=kenil -> ks2=kcall f s EnvMod.emp kstop -> ke=kenil ->
c=curs (sfree al v) -> callcont ks1 = None -> intcont ks1 = None->
~InOS (SKIP,(kenil,ks)) (pumerge po pi) ->
(freels al (get_mem (get_smem o)) MemMod.emp /\
InitTaskSt (emple_tst (substaskst o MemMod.emp),O)/\ ch=curs (sskip v)/\keh=kenil)
)
->
TaskSim (pc, (po,pi,ip)) (c,(ke,ks1##(ks2##ks))) o (pc, A) (ch,(keh,ks)) O tid I InitTaskSt.
Lemma hret_spec:
forall (o : taskst) (O : osabst) (ab : osapi) (abs : absop)
(R : retasrt) (vl : vallist) (po : progunit) v
(f : fid) G,
Some R = BuildRetA po f ab vl G->
(o, O, abs) |= R v ->
abs = spec_done v.
Qed.
Definition get_lint (os:oscode):= snd os.
Definition get_ifun (os:oscode):= snd (fst os).
Definition get_afun (os:oscode):= fst (fst os).
Lemma SmCTaskSim: forall pc OS1 (A:osspec) I o O t C,
no_fun_same (get_afun OS1) (get_ifun OS1) ->
no_call_api_os (get_afun OS1) (get_ifun OS1) (get_lint OS1) ->
(forall f t d1 d2 s, (fst (fst OS1)) f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
(forall f t d1 d2 s, (snd (fst OS1)) f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
(
forall (f:fid) ab vl p r ft G,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA (fst (fst OS1)) f (ab,ft) vl G->
Some r = BuildRetA (fst (fst OS1)) f (ab,ft) vl G->
(
exists t d1 d2 s,
(fst (fst OS1)) f = Some (t, d1, d2, s)/\ GoodStmt´ s/\
MethSimAsrt (snd (fst OS1)) (snd A) I r Afalse p s Afalse
)
) ->
(GoodClient pc (fst (fst OS1)) (snd (fst OS1))/\eqdomOS OS1 A) ->
InitTaskSt (pair o O) ->
(exists s, C= nilcont s /\ GoodStmt s (snd (fst OS1)) /\ True ) ->
TaskSim (pc, OS1) C o ( pc, A) C O t I InitTaskSt.
Lemma GoodP_to_S: forall p po pi f a b c s, GoodClient p po pi-> p f = Some (a,b,c,s)-> GoodStmt s pi.
Lemma projs_steq_projs:
forall Sl S´ t´ t´0 or ge le ir m ir´ i si,
t´0 <> t´ ->
projS Sl t´ = Some (ge, le, m, ir, (true, si, nil)) ->
projS S´ t´ = Some (ge, empenv, m, ir´, (false, i :: si, nil)) ->
Steq Sl S´ t´ ->
projS Sl t´0 = Some or -> projS S´ t´0 = Some (fst (fst or), snd (fst S´), snd or).
Definition eqevntls (env: CltEnvMod.map) (tls:TcbMod.map) :=
forall (t:tid), CltEnvMod.indom env t <-> TcbMod.indom tls t.
Definition eqisttls (lst:ltaskstset) (tls:TcbMod.map) :=
forall (t:tid), TaskLStMod.indom lst t <-> TcbMod.indom tls t.
Definition eqdomSO (S : osstate) (O:OSAbstMod.map) :=
match S with
| (G,pi,M,isr,lst) =>
match OSAbstMod.get O abtcblsid with
| Some (abstcblist tls) => eqevntls pi tls /\ eqisttls lst tls
| _ => False
end
end.
Lemma tsimtopsim:
forall pl Tl Sl ph Th O cst t,
OSAbstMod.get O curtid = Some (oscurt t)->
(
exists (pc:progunit) (A:osspec) po pi ip Tm Ol Os Ms Ml I,
no_fun_same po pi/\
True /\
no_call_api_os po pi ip /\
(forall f t d1 d2 s, po f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) /\ (forall f t d1 d2 s, pi f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) /\
pl = (pc, ( po, pi, ip)) /\ ph = (pc, A) /\ (GoodClient pc po pi/\ True /\ good_t_ks pl Tl /\ good_is_S Sl/\GoodI I (snd A) )
/\
MemMod.disj Ml Ms /\ MemMod.merge Ml Ms = (snd (fst (fst Sl)))
/\
partM Ml Tl Tm
/\
OSAbstMod.disj Ol Os /\ O = OSAbstMod.merge Ol Os
/\
(exists o o´, projS Sl t = Some o /\ substaskst o Ms = o´ /\(forall ab, sat ((pair o´ Os),ab) (INV I) ))
/\
(exists o o´ Mc Cl Ch, TMSpecMod.maps_to Tm t Mc /\
projS Sl t = Some o /\ substaskst o Mc = o´ /\
TasksMod.get Th t = Some Ch /\ TasksMod.get Tl t = Some Cl/\
TaskSim pl Cl o´ ph Ch Ol t I InitTaskSt)
/\
(
forall t´ Ch, ~(t´=t) -> TasksMod.get Th t´ = Some Ch ->
(
exists o M´ Cl,
TMSpecMod.maps_to Tm t´ M´ /\
projS Sl t´ = Some o /\
TasksMod.get Tl t´ = Some Cl/\
(
forall Mr Or,
(forall ab, sat ((pair (RdyChange (substaskst o Mr)) Or),ab) (RDYINV I))/\
MemMod.disj Mr M´ ->
(
exists M´´, M´´=MemMod.merge Mr M´ /\
TaskSim pl Cl (RdyChange (substaskst o M´´)) ph Ch Or t´ I InitTaskSt
)
)
)
)
/\ eqdomTO Th O /\ eqdomOS (po, pi, ip) A
/\
(
forall (f:fid) ab vl p r ft G,
(fst (fst A)) f = Some (ab,ft )->
Some p = BuildPreA po f (ab,ft) vl G->
Some r = BuildRetA po f (ab,ft) vl G->
(
exists t d1 d2 s,
po f = Some (t, d1, d2, s)/\ GoodStmt´ s /\
MethSimAsrt pi (snd A) I r Afalse p s Afalse
)
)
/\
(
forall (i:hid) ispec isrreg si G,
(snd (fst A)) i = Some ispec ->
(
exists (s:stmts) p r,
ip i = Some s /\
p = ipreasrt i isrreg si (ispec ) I G/\
r = iretasrt i isrreg si I G/\
MethSimAsrt pi (snd A) I retfalse r p s Afalse
)
)
)
->
ProgSim pl Tl Sl ph Th O cst t.
Lemma lemma_trans_temp:forall o o´ O O´ x t´ sc, GoodSched sc -> (forall ab : absop, (o, O, ab) |= SWPRE sc x) -> (forall ab : absop, (o´, merge O O´, ab) |= AHprio sc t´ ** Atrue) -> (forall ab : absop, (o, O, ab) |= AHprio sc t´ ** Atrue).
Lemma abst_get_set: forall O id x, get (set O id x) id = Some x.
Lemma abst_set_get_neq: forall id1 id2 y O, id1<>id2 -> OSAbstMod.get (OSAbstMod.set O id2 y) id1 = OSAbstMod.get O id1.
Qed.
Lemma ApiMethSim:
forall (OS1:oscode) (A:osspec) Spec I,
GoodI I (snd A)->
(
WFFuncsSim (snd (fst OS1)) Spec (snd A) I
) ->
(
forall (f:fid) ab vl p r ft G,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA (fst (fst OS1)) f (ab,ft) vl G->
Some r = BuildRetA (fst (fst OS1)) f (ab,ft) vl G->
(
exists t d1 d2 s,
(fst (fst OS1)) f = Some (t, d1, d2, s)/\ GoodStmt´ s /\
InfRules Spec (snd A) I r Afalse p s Afalse
)
)
->
(
forall (f:fid) ab vl p r ft G,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA (fst (fst OS1)) f (ab,ft) vl G->
Some r = BuildRetA (fst (fst OS1)) f (ab,ft) vl G->
(
exists t d1 d2 s,
(fst (fst OS1)) f = Some (t, d1, d2, s)/\ GoodStmt´ s /\
MethSimAsrt (snd (fst OS1)) (snd A) I r Afalse p s Afalse
)
).
Lemma IntMethSim:
forall (OS1:oscode) (A:osspec) Spec I,
GoodI I (snd A) ->
(
WFFuncsSim (snd (fst OS1)) Spec (snd A) I
) ->
(
forall (i:hid) ispec isrreg si G,
(snd (fst A)) i = Some ispec ->
(
exists (s:stmts) p r,
(snd OS1) i = Some s /\
p = ipreasrt i isrreg si (ispec ) I G/\
r = iretasrt i isrreg si I G/\
InfRules Spec (snd A) I retfalse r p s Afalse
)
)
->
(
forall (i:hid) ispec isrreg si G,
(snd (fst A)) i = Some ispec ->
(
exists (s:stmts) p r,
(snd OS1) i = Some s /\
p = ipreasrt i isrreg si (ispec) I G/\
r = iretasrt i isrreg si I G/\
MethSimAsrt (snd (fst OS1)) (snd A) I retfalse r p s Afalse
)
).
Definition side_condition´ I schedmethod init:=
(
GoodI I schedmethod /\
(forall tid S O, init S O ->
(forall o, (projS S tid) = Some o ->
exists o´,
o´ = substaskstm o MemMod.emp /\
(InitTaskSt (pair o´ OSAbstMod.emp)) /\
(forall ab,sat ((pair o O),ab) (INV I)) ) /\ eqdomSO S O)
).
Lemma bpr´_to_bpr: forall osc (A:osspec) I Spec,
(
forall (f:fid) ab vl p r ft,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA´ (get_afun osc) f (ab,ft) vl ->
Some r = BuildRetA´ (get_afun osc) f (ab,ft) vl ->
(
exists t d1 d2 s,
(get_afun osc) f = Some (t, d1, d2, s)/\ GoodStmt´ s /\
InfRules Spec (snd A) I r Afalse p s Afalse
)
) ->
(
forall (f:fid) ab vl p r ft G,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA (get_afun osc) f (ab,ft) vl G->
Some r = BuildRetA (get_afun osc) f (ab,ft) vl G->
(
exists t d1 d2 s,
(get_afun osc) f = Some (t, d1, d2, s)/\ GoodStmt´ s /\
InfRules Spec (snd A) I r Afalse p s Afalse
)
).
Lemma int_bpr´_to_bpr : forall osc (A:osspec) I Spec,
(
forall (i:hid) ispec isrreg si,
(snd (fst A)) i = Some ispec ->
(
exists (s:stmts) p r,
(get_lint osc) i = Some s /\
p = ipreasrt´ i isrreg si (ispec) I /\
r = iretasrt´ i isrreg si I /\
InfRules Spec (snd A) I retfalse r p s Afalse
)
)->
(
forall (i:hid) ispec isrreg si G,
(snd (fst A)) i = Some ispec ->
(
exists (s:stmts) p r,
(get_lint osc) i = Some s /\
p = ipreasrt i isrreg si (ispec ) I G/\
r = iretasrt i isrreg si I G/\
InfRules Spec (snd A) I retfalse r p s Afalse
)
).
Definition oscorrect_aux (Os:oscode) (A:osspec) (init:InitAsrt):=
forall (t:tid) pc Wl Wh (T:tasks) S cst O,
OSAbstMod.get O curtid = Some (oscurt t) ->
InitTasks T pc cst O -> init S O -> (WellClient pc (fst (fst Os)) (snd (fst Os)))-> TasksMod.indom T t ->
Wl = ((pc, Os), T , cst, S, t) ->
Wh = ((pc, A), T, cst, O) ->
etrace_subset Wl Wh.
Theorem toptheorem´: forall (osc:oscode) (A:osspec) (init:InitAsrt) (I:Inv) (Spec:funspec),
no_fun_same (get_afun osc) (get_ifun osc)->
True ->
True ->
no_call_api_os (get_afun osc) (get_ifun osc) (get_lint osc) ->
(forall f t d1 d2 s, (fst (fst osc)) f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
(forall f t d1 d2 s, (snd (fst osc)) f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
GoodI I (snd A)->
(
forall (i:hid) ispec isrreg si,
(snd (fst A)) i = Some ispec ->
(
exists (s:stmts) p r,
(get_lint osc) i = Some s /\
p = ipreasrt´ i isrreg si (ispec) I /\
r = iretasrt´ i isrreg si I /\
InfRules Spec (snd A) I retfalse r p s Afalse
)
)->
(
forall (f:fid) ab vl p r ft,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA´ (get_afun osc) f (ab,ft) vl ->
Some r = BuildRetA´ (get_afun osc) f (ab,ft) vl ->
(
exists t d1 d2 s,
(get_afun osc) f = Some (t, d1, d2, s)/\ GoodStmt´ s /\
InfRules Spec (snd A) I r Afalse p s Afalse
)
)->
WFFunEnv (get_ifun osc) Spec (snd A) I->
(
eqdomOS osc A /\
(forall tid S O, init S O ->
(forall o, (projS S tid) = Some o ->
exists o´,
o´ = substaskstm o MemMod.emp /\
(InitTaskSt (pair o´ OSAbstMod.emp)) /\
(forall ab,sat ((pair o O),ab) (INV I)) ) /\ eqdomSO S O)
)->
oscorrect_aux osc A init.
Lemma eqdomsot_get_exproj:
forall t S O T,
TasksMod.indom T t ->
eqdomTO T O ->
eqdomSO S O ->
exists o, projS S t = Some o.
Lemma init_goodis:
forall S O I,
(
forall o t,
projS S t = Some o ->
exists o´,
o´ = substaskstm o empmem /\
InitTaskSt (o´, empabst) /\ (forall ab : absop, (o, O, ab) |= INV I)) ->
good_is_S S.
Lemma eqdomto_indom_get:
forall T t O x,
TasksMod.indom T t -> eqdomTO T O -> get O abtcblsid = Some (abstcblist x) -> exists a, TcbMod.get x t = Some a.
Lemma eqdomsot_get_exproj´:
forall t S O T Ch,
TasksMod.get T t = Some Ch ->
eqdomTO T O ->
eqdomSO S O ->
exists o, projS S t = Some o.
Qed.
Theorem toptheorem´´: forall osc A (init:InitAsrt) (I:Inv) (Spec:funspec),
no_fun_same (get_afun osc) (get_ifun osc)->
no_call_api_os (get_afun osc) (get_ifun osc) (get_lint osc) ->
(forall f t d1 d2 s, (fst (fst osc)) f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
(forall f t d1 d2 s, (snd (fst osc)) f = Some (t,d1,d2,s) -> good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
GoodI I (snd A)->
(
forall (i:hid) ispec isrreg si,
(snd (fst A)) i = Some ispec ->
(
exists (s:stmts) p r,
(get_lint osc) i = Some s /\
p = ipreasrt´ i isrreg si (ispec) I /\
r = iretasrt´ i isrreg si I /\
InfRules Spec (snd A) I retfalse r p s Afalse
)
)->
(
forall (f:fid) ab vl p r ft,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA´ (get_afun osc) f (ab,ft) vl ->
Some r = BuildRetA´ (get_afun osc) f (ab,ft) vl ->
(
exists t d1 d2 s,
(get_afun osc) f = Some (t, d1, d2, s) /\
InfRules Spec (snd A) I r Afalse p s Afalse
)
)->
WFFunEnv (get_ifun osc) Spec (snd A) I->
(
eqdomOS osc A /\
(forall tid S O, init S O -> (forall o, (projS S tid) = Some o ->
exists o´,
o´ = substaskstm o MemMod.emp /\
(InitTaskSt (pair o´ OSAbstMod.emp)) /\
(forall ab,sat ((pair o O),ab) (INV I)) ) /\ eqdomSO S O)
)
->
oscorrect_aux osc A init.
Theorem toptheorem:
forall osc A (init:InitAsrt) (I:Inv) (Spec:funspec),
no_fun_same (get_afun osc) (get_ifun osc)->
no_call_api_os (get_afun osc) (get_ifun osc) (get_lint osc) ->
(forall f t d1 d2 s, (fst (fst osc)) f = Some (t,d1,d2,s) ->
good_decllist (revlcons d1 d2) = true /\ GoodStmt´ s) ->
(forall f t d1 d2 s, (snd (fst osc)) f = Some (t,d1,d2,s) ->
good_decllist (revlcons d1 d2) = true/\GoodStmt´ s) ->
GoodI I (snd A)->
(
forall i isrreg si p r,
Some p = BuildintPre i (snd (fst A)) isrreg si I ->
Some r = BuildintRet i (snd (fst A)) isrreg si I ->
exists s,
(get_lint osc) i = Some s /\
{|Spec , (snd A), I, retfalse, r|}|- {{p}}s {{Afalse}}
)->
(
forall (f:fid) ab vl p r ft,
(fst (fst A)) f = Some (ab,ft) ->
Some p = BuildPreA´ (get_afun osc) f (ab,ft) vl ->
Some r = BuildRetA´ (get_afun osc) f (ab,ft) vl ->
(
exists t d1 d2 s,
(get_afun osc) f = Some (t, d1, d2, s) /\
InfRules Spec (snd A) I r Afalse p s Afalse
)
)->
WFFunEnv (get_ifun osc) Spec (snd A) I->
(
eqdomOS osc A /\
(forall tid S O, init S O ->
(forall o, (projS S tid) = Some o ->
exists o´,
o´ = substaskstm o MemMod.emp /\
(InitTaskSt (pair o´ OSAbstMod.emp)) /\
(forall ab,sat ((pair o O),ab) (INV I)) ) /\ eqdomSO S O)
)
->
oscorrect_aux osc A init.