Library progtaskstepLib
Require Import include.
Require Import inferules.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import memdata.
Require Import memory.
Require Import Map.
Require Import simulation.
Require Import auxdef.
Require Import etraceref.
Require Import tst_prop.
Require Import contLib.
Require Import Classical.
Require Import List.
Require Import baseTac.
Require Import asrtLib.
Require Import ruleLib.
Require Import lmachLib.
Lemma spec_step_tidsame:
forall c O c´ O´,
spec_step c O c´ O´ -> tidsame O O´.
Lemma hapistep_tidsame: forall A cd cd´ O O´,hapistep A cd O cd´ O´ -> tidsame O O´.
Lemma htstep_tidsame: forall p c cst c´ cst´ O O´ t,htstep p t c cst O c´ cst´ O´ -> tidsame O O´.
Lemma htstepstar_tidsame: forall p c cst c´ cst´ O O´ t,htstepstar p t c cst O c´ cst´ O´ -> tidsame O O´.
Lemma htstepevstar_tidsame
: forall (p : hprog) (c : code) (cst : clientst)
(c´ : code) (cst´ : clientst) (O O´ : osabst) ev t,
htstepevstar p t c cst O c´ cst´ O´ ev-> tidsame O O´.
Lemma abst_join_join_merge_ex:
forall x1 x2 x3 x4,
OSAbstMod.join x1 x2 x3 ->
exists y, OSAbstMod.join x1 y (OSAbstMod.merge x3 x4).
Lemma hmstep_tidsame: forall c o c´ o´, hmstep c o c´ o´ -> tidsame o o´.
Lemma hmstepstar_tidsame: forall c o c´ o´, hmstepstar c o c´ o´ -> tidsame o o´.
Lemma hmstep_locality:
forall ab´ O O´ O´´ ab,
hmstepstar ab O ab´ O´ ->
OSAbstMod.disj O´´ O ->
hmstepstar ab (OSAbstMod.merge O´´ O) ab´ (OSAbstMod.merge O´´ O´).
Lemma hmstep_locality´:
forall ab´ O O´ O´´ ab,
hmstepstar ab O ab´ O´ ->
OSAbstMod.disj O´´ O ->
hmstepstar ab (OSAbstMod.merge O O´´) ab´ (OSAbstMod.merge O´ O´´).
Lemma callcont_nonone_addcont:
forall ks ks1,
callcont ks <> None -> callcont (ks ## ks1) <> None.
Lemma sstep_AddKsToTail : forall pc c1 c2 ks1 ks2 ks´ ge1 ge2 le1 le2 M1 M2,
sstep pc c1 ks1 (ge1, le1, M1) c2 ks2 (ge2, le2, M2) ->
sstep pc c1 (ks1 ## ks´) (ge1, le1, M1) c2 (ks2 ## ks´) (ge2, le2, M2).
Lemma cstep_AddKsToTail : forall pc c1 c2 ke1 ke2 ks1 ks2 ks´ ge1 ge2 le1 le2 M1 M2,
cstep pc (c1, (ke1, ks1)) (ge1, le1, M1) (c2, (ke2, ks2)) (ge2, le2, M2) ->
cstep pc (c1, (ke1, ks1 ## ks´)) (ge1, le1, M1) (c2, (ke2, ks2 ## ks´)) (ge2, le2, M2).
Lemma hapistep_AddKsToTail : forall B C c1 c2 ke1 ke2 ks1 ks2 ks´ O1 O2,
hapistep (B, C) (c1, (ke1, ks1)) O1 (c2, (ke2, ks2)) O2 ->
hapistep (B, C) (c1, (ke1, ks1 ## ks´)) O1 (c2, (ke2, ks2 ## ks´)) O2.
Lemma htstep_AddKsToTail : forall p c1 c2 ke1 ke2 ks1 ks2 ks´ cst cst´ O1 O2 t,
htstep p t (c1, (ke1, ks1)) cst O1 (c2, (ke2, ks2)) cst´ O2 ->
htstep p t (c1, (ke1, ks1 ## ks´)) cst O1 (c2, (ke2, ks2 ## ks´)) cst´ O2.
Lemma htstep_locality´: forall A c ke cst O c´ ke´ cst´ O´ ks ks´1 ks´2 t,
htstepstar A t (c, (ke, ks´1)) cst O (c´, (ke´, ks´2)) cst´ O´ ->
htstepstar A t (c, (ke, ks´1 ## ks)) cst O (c´, (ke´, ks´2 ## ks)) cst´ O´.
Lemma AddKsToTail_kstop : forall ks, kstop ## ks = ks.
Lemma sstep1_locality : forall pc c (ge : env) le M c´ ge le´ M´ ks, sstep pc c kstop (ge, le, M) c´ kstop (ge, le´, M´) -> sstep pc c ks (ge, le, M) c´ ks (ge, le´, M´).
Lemma cstep1_locality : forall pc c ke ge le M c´ ke´ le´ M´ ks, cstep pc (c, (ke, kstop)) (ge, le, M) (c´, (ke´, kstop)) (ge, le´, M´) -> cstep pc (c, (ke, ks)) (ge, le, M) (c´, (ke´, ks)) (ge, le´, M´).
Lemma hapistep1_locality :
forall B C D c ke O c´ ke´ O´ ks,
hapistep (B, C, D) (c, (ke, kstop)) O (c´, (ke´, kstop)) O´ -> hapistep (B, C, D) (c, (ke, ks)) O (c´, (ke´, ks)) O´.
Lemma nat_n_Sn_neq : forall n, ~ n = S n.
Lemma TStWoMemEq_emple_tst_same : forall o,
TStWoMemEq (emple_tst o) (emple_tst o).
Lemma mem_disj_disj_join_disj : forall m1 m2 m3 mx,
MemMod.disj m1 mx -> MemMod.disj m2 mx -> MemMod.join m1 m2 m3 -> MemMod.disj m3 mx.
Lemma freeb_get : forall len b a x m1 m2 i,
freeb m1 b i len = Some m2 -> MemMod.get m2 a = Some x -> MemMod.get m1 a = Some x.
Lemma free_get : forall t b a x m1 m2,
free t b m1 = Some m2 -> MemMod.get m2 a = Some x -> MemMod.get m1 a = Some x.
Lemma freeb_sub : forall len i b M M´,
freeb M b i len = Some M´ -> MemMod.sub M´ M.
Lemma free_sub : forall t b M M´,
free t b M = Some M´ -> MemMod.sub M´ M.
Lemma mem_sub_get_get : forall m1 m2 a x1 x2,
MemMod.sub m1 m2 -> MemMod.get m1 a = Some x1 -> MemMod.get m2 a = Some x2 -> x1 = x2.
Lemma mem_sub_false : forall m1 m2 a x,
MemMod.sub m1 m2 -> MemMod.get m2 a = None -> MemMod.get m1 a = Some x -> False.
Lemma mem_get_eq : forall m1 m2 a, m1 = m2 -> MemMod.get m1 a = MemMod.get m2 a.
Lemma freeb_consistent : forall len m1 m1´ m2 m2´ x1 x2 x2´ b i a,
freeb m1 b i len = Some m1´ -> freeb m2 b i len = Some m2´ ->
MemMod.get m1 a = Some x1 -> MemMod.get m1´ a = None ->
MemMod.get m2 a = Some x2 -> MemMod.get m2´ a = Some x2´ ->
False.
Lemma freeb_inconsistent : forall len m1 m2 m3 m4 a b i x1,
freeb m1 b i len = Some m2 -> MemMod.get m1 a = Some x1 -> MemMod.get m2 a = None ->
MemMod.get m3 a = None -> freeb m3 b i len = Some m4 ->
False.
Lemma free_consistent : forall t m1 m1´ m2 m2´ x1 x2 x2´ b a,
free t b m1 = Some m1´ -> free t b m2 = Some m2´ ->
MemMod.get m1 a = Some x1 -> MemMod.get m1´ a = None ->
MemMod.get m2 a = Some x2 -> MemMod.get m2´ a = Some x2´ ->
False.
Lemma free_inconsistent : forall t m1 m2 m3 m4 a b x1,
free t b m1 = Some m2 -> MemMod.get m1 a = Some x1 -> MemMod.get m2 a = None ->
MemMod.get m3 a = None -> free t b m3 = Some m4 ->
False.
Lemma freeb_mem_join : forall len M M1 M2 M´ b o,
MemMod.join M M1 M2 ->
freeb M b o len = Some M´ ->
exists M´´, freeb M2 b o len = Some M´´.
Lemma int_mem_trans: forall sd p C o C´ o´ Ms I Os Ml,
GoodI I sd->
lintstep p C o C´ o´ ->
MemMod.disj Ml Ms ->
MemMod.merge Ml Ms = (get_mem (get_smem o)) ->
(forall ab, sat (((substaskst o Ms), Os),ab) (INV I)) ->
(
exists Ms´ Ml´ Os´ Ol, Ms = MemMod.merge Ml´ Ms´ /\
MemMod.disj Ml´ Ms´/\
Os = OSAbstMod.merge Os´ Ol /\
OSAbstMod.disj Ol Os´ /\
(forall ab, sat (((substaskst o´ Ms´), Os´),ab) (INV I))
).
Require Import asrtLib.
Lemma tasks_set_a_set_a : forall T a val1 val2, TasksMod.set (TasksMod.set T a val1) a val2 = TasksMod.set T a val2.
Lemma tasks_set_set: forall T t c c´, TasksMod.set T t c´ = TasksMod.set (TasksMod.set T t c) t c´.
Lemma th_ttop_lift: forall Th C C´ p O O´ cst cst´ t,
OSAbstMod.get O curtid = Some (oscurt t) ->
htstepstar p t C cst O C´ cst´ O´ ->
TasksMod.get Th t = Some C ->
hpstepstar p Th cst O (TasksMod.set Th t C´) cst´ O´.
Lemma th_no_create_lift: forall Th C C´ t p O O´ cst cst´, OSAbstMod.get O curtid = Some (oscurt t) -> htstepstar p t C cst O C´ cst´ O´ -> TasksMod.get Th t = Some C ->
hpstepstar p Th cst O
(TasksMod.set Th t C´) cst´ O´.
Lemma th_free_lift: forall Th C C´ t p O O´ cst cst´, OSAbstMod.get O curtid = Some (oscurt t) -> htstep p t C cst O C´ cst´ O´ -> TasksMod.get Th t = Some C ->
hpstepstar p Th cst O
(TasksMod.set Th t C´) cst´ O´ .
Lemma tcbmod_join_sig_nex: forall tls tls´ t b, TcbMod.join tls´ (TcbMod.sig t b) tls ->
~(exists a,TcbMod.get tls´ t = Some a).
Lemma tcbmod_join_ex: forall tls tls´ tls´´ t0, TcbMod.join tls´ tls´´ tls -> (exists a, TcbMod.get tls´ t0 = Some a) -> exists a, TcbMod.get tls t0 = Some a.
Lemma hpstep_eqdomto: forall T O cst cst´ T´ O´ p , eqdomTO T O -> hpstepstar p T cst O T´ cst´ O´ -> eqdomTO T´ O´.
Lemma hpstep_eqdomO :
forall p T T´ cst cst´ O O´,
eqdomTO T O ->
hpstep p T cst O T´ cst´ O´ ->
eqdomTO T´ O´.
Lemma htstep_eqdomO :
forall p t C C´ cst cst´ O O´,
htstep p t C cst O C´ cst´ O´ -> eqdomO O O´.
Lemma eqdomO_refl :
forall O, eqdomO O O.
Lemma hapistep_eqdomO :
forall A C C´ O O´,
hapistep A C O C´ O´ -> eqdomO O O´.
Qed.
Lemma eqdomO_eqdomTO :
forall O O´ T,
eqdomO O O´ -> eqdomTO T O -> eqdomTO T O´.
Lemma eqdomTO_setT :
forall T T´ t C C´ O,
TasksMod.get T t = Some C -> eqdomTO T O ->
TasksMod.set T t C´ = T´ ->
eqdomTO T´ O.
Lemma htistep_eqdomO :
forall ispec C C´ O O´,
htistep ispec C O C´ O´ -> eqdomO O O´.
Lemma eqdomO_set2 :
forall O t x x´,
OSAbstMod.get O t = Some x ->
t <> abtcblsid ->
eqdomO O (OSAbstMod.set O t x´).
Qed.
Qed.
Lemma abst_set_get_neq: forall id1 id2 y O, id1<>id2 -> OSAbstMod.get (OSAbstMod.set O id2 y) id1 = OSAbstMod.get O id1.
Lemma hpstep_star: forall p T T´ T´´ cst cst´ cst´´ O O´ O´´ , hpstepstar p T cst O T´ cst´ O´ -> hpstep p T´ cst´ O´ T´´ cst´´ O´´ -> hpstepstar p T cst O T´´ cst´´ O´´.
Lemma th_no_create_lift_ev:
forall (Th : tasks) (C C´ : code) (t : tid) (p : hprog)
(O O´ : osabst) (cst cst´ : clientst) ev,
OSAbstMod.get O curtid = Some ( oscurt t)->
TasksMod.get Th t = Some C ->
htstepevstar p t C cst O C´ cst´ O´ ev->
hpstepevstar p Th cst O (TasksMod.set Th t C´) cst´ O´ ev.
Lemma hpstepev_eqdomto: forall (T : tasks) (O : osabst) (cst cst´ : clientst)
(T´ : tasks) (O´ : osabst) (p : hprog)
ev,
eqdomTO T O -> hpstepevstar p T cst O T´ cst´ O´ ev-> eqdomTO T´ O´.
Lemma hpstepev_eqdomTO :
forall p T T´ cst cst´ O O´ ev,
eqdomTO T O -> hpstepev p T cst O T´ cst´ O´ ev ->
eqdomTO T´ O´.
Qed.
Lemma cltstep_eqo: forall t pc po pi ip cst cst´ o o´ c c´, ~InOS c (pumerge po pi) -> ltstep (pc,(po,pi,ip)) t c cst o c´ cst´ o´ -> o=o´.
Lemma good_clt_scont_callcont: forall ks ks´ f s le p, good_clt_scont ks p-> callcont ks = Some (kcall f s le ks´) -> good_clt_scont ks´ p.
Lemma no_inos_pc: forall f vl tl ks0 pc po pi t0 d1 d2 s,~ InOS (curs (sfexec f vl tl), (kenil, ks0)) (pumerge po pi) -> pumerge pc po f = Some (t0, d1, d2, s) -> pc f = Some ( t0, d1 , d2 , s).
Lemma clt_step_good_clt: forall pc po pi ip t c ke ks cst o cst´ o´ C´, ltstep (pc,(po,pi,ip)) t (c,(ke,ks)) cst o C´ cst´ o´->
GoodClient pc po pi->
good_clt (c,(ke,ks)) pi->
~InOS (c,(ke,ks)) (pumerge po pi) ->
good_clt C´ pi.
Lemma Goodstmt_good_clt_stmt: forall s p, GoodStmt s p-> good_clt_stmt s p.
Qed.
Lemma clt_stepev_good_clt: forall pc po pi ip t c ke ks cst o cst´ o´ C´ ev , ltstepev (pc,(po,pi,ip)) t (c,(ke,ks)) cst o C´ cst´ o´ ev->
good_clt (c,(ke,ks)) pi ->
~InOS (c,(ke,ks)) (pumerge po pi) ->
good_clt C´ pi.
Lemma sstep_pumerge : forall pc po pi c c´ ks ks´ m m´, sstep (pumerge pc po) c ks m c´ ks´ m´ -> ~InOS (c, (kenil, ks)) (pumerge po pi) -> sstep pc c ks m c´ ks´ m´.
Lemma sstep_pumerge´ : forall pc po pi c c´ ks ks´ m m´, sstep pc c ks m c´ ks´ m´ -> ~InOS (c, (kenil, ks)) (pumerge po pi) -> sstep (pumerge pc po) c ks m c´ ks´ m´.
Lemma cstep_pumerge : forall pc po pi c c´ m m´, cstep (pumerge pc po) c m c´ m´ -> ~InOS c (pumerge po pi) -> cstep pc c m c´ m´.
Lemma cstep_pumerge´ : forall pc po pi c c´ m m´, cstep pc c m c´ m´ -> ~InOS c (pumerge po pi) -> cstep (pumerge pc po) c m c´ m´.
Lemma cltstep1_eq: forall pc po pi ip cst cst´ o O A c c´ t,
ltstep (pc,(po,pi,ip)) t c cst o c´ cst´ o ->
good_clt c pi->
~(InOS c (pumerge po pi)) ->
htstep (pc,A) t c cst O c´ cst´ O.
Lemma cstep_p_local: forall pc po pi c ge le M le´ M´ c´,
~ InOS c (pumerge po pi) ->
cstep pc c (ge, le, M) c´ (ge, le´, M´) ->
cstep (pumerge pc po) c (ge,le ,M) c´ (ge,le´,M´).
Definition no_api_code (c:code) :=
forall ke ks x, c <> (curs (hapi_code x), (ke,ks)).
Lemma cltstep_eqabt: forall pc po pi ip ge envs m o O t A c ,
~IsEnd c ->
eqdomOS (po,pi,ip) A ->
no_api_code c ->
ltstepabt (pc,(po,pi,ip)) t c (ge,envs,m) o->
~(InOS c (pumerge po pi)) ->
htstepabt (pc,A) t c (ge,envs,m) O.
Lemma step_to_inos_dec: forall c ke ks pc po pi ip t cst cst´ C´ o, good_clt (c,(ke,ks)) pi -> goodks (pc,(po,pi,ip)) ks-> ~InOS (c,(ke,ks)) (pumerge po pi) -> ltstep (pc,(po,pi,ip)) t (c,(ke,ks)) cst o C´ cst´ o -> (exists f a vl tl ks, po f = Some a/\C´=(curs (sfexec f vl tl),(kenil,ks)))\/ ~(InOS C´ (pumerge po pi)).
Lemma stepev_still_inos: forall C pc po pi ip t C´ cst o ev, ~InOS C (pumerge po pi) -> ltstepev (pc,(po,pi,ip)) t C cst o C´ cst o ev -> ~(InOS C´ (pumerge po pi)).
Lemma cltstepev_eq: forall pc po pi ip cst cst´ o O t A c c´ ev,
ltstepev (pc,(po,pi,ip)) t c cst o c´ cst´ o ev->
~(InOS c (pumerge po pi)) ->
htstepev (pc,A) t c cst O c´ cst´ O ev.
Lemma len_eq_rev_eq: forall (vl:vallist) (tl:typelist), length vl = length tl -> length vl = length (rev tl).
Lemma n_tlmatch_abt: forall pc po pi ip f tp d1 d2 s tl vl ks t cst o,
~ (tlmatch (List.rev tl) d1/\ dl_vl_match d1 (rev vl)=true) ->
po f = Some (tp, d1, d2, s) ->
ltstepabt (pc,(po,pi,ip)) t (curs (sfexec f vl tl), (kenil, ks)) cst o.
Lemma hn_tlmatch_abt: forall pc B C ab f tp tl´ tl vl ks ge envs m O sc t,
pc f = None ->
~((List.rev tl)=tl´/\ tl_vl_match tl vl = true) ->
B f = Some (ab,(tp,tl´)) ->
htstepabt (pc,(B,C,sc)) t (curs (sfexec f vl tl), (kenil, ks)) (ge,envs,m) O.
Lemma osapi_lift1´:
forall r O r´ O´ ke ks pc A cst t,
hmstep r O r´ O´ ->
htstep (pc, A) t (curs (hapi_code r),(ke,ks)) cst O (curs (hapi_code r´),(ke,ks)) cst O´.
Lemma osapi_lift´:
forall A gamma O O´ gamma´ pc ke ks cst t,
hmstepstar gamma O gamma´ O´ ->
htstepstar (pc,A) t (curs (hapi_code gamma), (ke, ks)) cst O (curs (hapi_code gamma´),(ke,ks)) cst O´.
Lemma step_fexec_ninos:
forall c ke ks t f vl tl ks´ cst cst´ o o´ pc po pi ip,
~ InOS (c, (ke, ks)) (pumerge po pi) ->
ltstep (pc, (po, pi, ip)) t (c, (ke, ks))
cst o (curs (sfexec f vl tl), (kenil, ks´))
cst´ o´ ->
~ InOS (SKIP, (kenil, ks´)) (pumerge po pi).
Lemma fexec_abt_eq:
forall pc po pi ip A t d1 d2 s tid o O cst cst´ dl vl f ks,
GoodClient pc po pi -> po f = Some (t,d1,d2,s) ->
eqdomOS (po,pi,ip) A ->
ltstepabt (pc,(po,pi,ip)) tid (curs (sfexec f vl dl),(kenil,ks)) cst o ->
htstepabtstar (pc,A) tid (curs (sfexec f vl dl),(kenil,ks)) cst´ O.
Lemma alloc_trans:forall pc po pi ip f ft d1 d2 s vlh tid o o´ O cst cst´ C´ ks vl dl,
po f = Some (ft,d1,d2,s) ->
good_decllist (revlcons d1 d2) =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 : absop, (o, O, ab)
|= (p ** Aie true ** Ais nil ** Acs nil ** Aisr empisr) **
A_dom_lenv (getlenvdom dl´))
)->
ltstep (pc,(po,pi,ip)) tid (curs (salloc vl dl), (kenil, kcall f s empenv ks)) cst o
C´ cst´ o´->
(
cst´=cst/\
exists dl´´ vl´´ p dl´´´ vl´´´,
C´=(curs (salloc vl´´ dl´´), (kenil, kcall f s empenv ks))/\
dl_add dl´´´ dl´´ = revlcons d1 d2 /\
vl´´´ ++ vl´´ = vlh /\
buildp dl´´´ vl´´´ = Some p /\
(vl<>nil -> length_eq vl´´´ dl´´´) /\
~(vl=nil/\dl=dnil)/\
(forall ab : absop, (o´, O, ab)
|= (p ** Aie true ** Ais nil ** Acs nil ** Aisr empisr) **
A_dom_lenv (getlenvdom dl´´´))
) \/
(
cst´=cst/\
exists p,
C´= (curs s,(kenil,kcall f s empenv ks))/\
vl=nil/\
dl=dnil/\
buildp (dladd d1 d2) vlh = Some p /\
(forall ab : absop, (o´, O, ab)
|= (p ** Aie true ** Ais nil ** Acs nil ** Aisr empisr) **
A_dom_lenv (getlenvdom (dladd d1 d2)))
).
Lemma alloc_locality: forall p o Ms o1 Mf o2 tid o´´ vl dl ks cst cst´ C´,
joinmem o Ms o1 ->
joinmem o1 Mf o2 ->
ltstep p tid (curs (salloc vl dl),(kenil,ks))
cst o2 C´ cst´ o´´ ->
(exists o1´ o´, ltstep p tid (curs (salloc vl dl),(kenil,ks))
cst o C´ cst´ o´/\ joinmem o´ Ms o1´/\joinmem o1´ Mf o´´/\TStWoMemEq (emple_tst o´) (emple_tst o)).
Lemma htstep_locality: forall A t c ke cst O c´ ke´ cst´ O´ ks, htstepstar A t (c, (ke, kstop)) cst O (c´, (ke´, kstop)) cst´ O´ -> htstepstar A t (c, (ke, ks)) cst O (c´, (ke´, ks)) cst´ O´.
Lemma good_dl_le_init´: forall dl ge M ir aux, good_decllist dl = true -> good_dl_le dl (ge,empenv,M,ir,aux).
Lemma good_dl_le_step´: forall pc po pi ip f ft d1 d2 s dl dl´ cst o cst´ o´ le ks t vl´ vl,po f = Some (ft, d1, d2, s) -> GoodStmt´ s -> good_dl_le dl o -> ltstep (pc, (po, pi, ip)) t (curs (salloc vl dl),(kenil,kcall f s le ks)) cst o (curs (salloc vl´ dl´),(kenil,kcall f s le ks)) cst´ o´ -> good_dl_le dl´ o´.
Lemma good_dl_le_care: forall o o´ dl,get_lenv (get_smem o) = get_lenv (get_smem o´) -> good_dl_le dl o -> good_dl_le dl o´.
Lemma join_eqe: forall o M o´, joinmem o M o´ -> get_lenv (get_smem o) = get_lenv (get_smem o´) .
Lemma tstep_alloc_nabt: forall p t vl dl ks cst o d1 d2 f s le ft, (vl=nil \/exists i t dl´, dl=dcons i t dl´) -> (fst (fst (snd p))) f = Some (ft, d1, d2, s) -> good_dl_le dl o -> ~(ltstepabt p t (curs (salloc vl dl),(kenil,kcall f s le ks)) cst o).
Lemma htstep1_locality:
forall A t c ke cst O c´ ke´ cst´ O´ ks,
htstep A t (c, (ke, kstop)) cst O (c´, (ke´, kstop)) cst´ O´ ->
htstep A t (c, (ke, ks)) cst O (c´, (ke´, ks)) cst´ O´.
Lemma env_can_get:forall le, exists x, getaddr le = x.
Lemma ndym_cont_red : forall ks f s E ks´,
n_dym_com_int_scont (ks ## kcall f s E ks´) ->
n_dym_com_int_scont ks.
Lemma n_dym_com_int_cd_cont : forall c ke ks1 ks f s E,
n_dym_com_int_cd (c, (ke, ks1 ## kcall f s E ks)) -> n_dym_com_int_cd (c, (ke, ks1)).
Lemma ltstep_inos_loststep : forall pc po pi ip tid c o c´ cst cst´ o´,
ltstep (pc, (po, pi, ip)) tid c cst o c´ cst´ o´ ->
InOS c (pumerge po pi) ->
loststep (pumerge po pi) c o c´ o´.
Lemma ltstep_inos_nupd_clst :
forall pc po pi ip tid c o c´ cst cst´ o´,
ltstep (pc, (po, pi, ip)) tid c cst o c´ cst´ o´ ->
InOS c (pumerge po pi) ->
cst = cst´.
Lemma kassignr_ex : forall e t ks0 ks1 f s E ks,
kassignr e t ks0 = ks1 ## kcall f s E ks ->
exists ks´, ks1 = kassignr e t ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma kassignl_ex : forall e t ks0 ks1 f s E ks,
kassignl e t ks0 = ks1 ## kcall f s E ks ->
exists ks´, ks1 = kassignl e t ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma kfuneval_ex1 : forall ks0 ks1 f0 vl tl e el f s E ks,
kfuneval f0 vl tl (e :: el) ks0 = ks1 ## kcall f s E ks ->
exists ks´, ks1 = kfuneval f0 vl tl (e :: el) ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma intcont_notnone_callcont_none : forall ks1 ks2, intcont ks1 <> None -> callcont (ks1##ks2) = None.
Lemma kfuneval_ex2 : forall ks0 ks1 f0 vl tl f s E ks,
kfuneval f0 vl tl nil ks0 = ks1 ## kcall f s E ks ->
exists ks´, ks1 = kfuneval f0 vl tl nil ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma kret_ex : forall ks0 ks1 f s E ks,
kret ks0 = ks1 ## kcall f s E ks ->
exists ks´, ks1 = kret ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma callcont_not_none_ex : forall ks, callcont ks <> None -> exists f s le ks0,
callcont ks = Some (kcall f s le ks0).
Lemma kif_ex : forall s1 s2 ks0 ks1 f s E ks,
kif s1 s2 ks0 = ks1 ## kcall f s E ks ->
exists ks´, ks1 = kif s1 s2 ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma intcont_kcall_intcont : forall ks f s E ks´ c ke le ks´´,
intcont (ks ## kcall f s E ks´)
= Some (kint c ke le ks´´) -> exists kss, intcont ks = Some (kint c ke le kss).
Lemma kseq_ex : forall s0 ks0 ks1 f s E ks,
kseq s0 ks0 = ks1 ## kcall f s E ks ->
exists ks´, ks1 = kseq s0 ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma kwhile_ex : forall e s0 ks0 ks1 f s E ks,
kwhile e s0 ks0 = ks1 ## kcall f s E ks ->
exists ks´, ks1 = kwhile e s0 ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma kcall_ex : forall f0 s0 E´ ks0 ks1 f s E ks, ks1 <> kstop ->
kcall f0 s0 E´ ks0= ks1 ## kcall f s E ks ->
exists ks´, ks1 = kcall f0 s0 E´ ks´ /\ ks0 = ks´ ## kcall f s E ks.
Lemma loststep_nofree_notabt : forall p c ke ks1 ks o2 Cl´ o´´ s f,
loststep p (c, (ke, ks1 ## kcall f s empenv ks)) o2 Cl´ o´´ ->
(~ ((c, (ke, ks1)) = (curs sret, (kenil, ks1)) /\ callcont ks1 = None/\intcont ks1=None))->
( forall v ksx,
~(
(c, (ke, ks1)) = (curs (sskip (Some v)), (kenil, kret ksx)) /\
callcont ksx = None/\intcont ksx =None)) ->
(forall (vl : vallist) (dl : decllist),
(c, (ke, ks1)) <> (curs (salloc vl dl), (kenil, kstop))) ->
(forall (al : freelist) (v : option val),
~
(c = curs (sfree al v) /\
callcont ks1 = None /\ intcont ks1 = None)) ->
~ loststepabt p (c, (ke, ks1)) o2.
Lemma intcont_ndym: forall ks ks´ s ke E, intcont ks = Some (kint s ke E ks´) ->
~ n_dym_com_int_scont ks.
Lemma loststep_not_alloc: forall p c ke ks c´ ke´ ks´ o o´,
n_dym_com_int_cd (c, (ke, ks)) ->
loststep p (c, (ke, ks)) o (c´,(ke´,ks´)) o´ ->
(forall (vl : vallist) (dl : decllist),
(c, (ke, ks)) <> (curs (salloc vl dl), (kenil, kstop))) ->
(forall (vl : vallist) (dl : decllist),
(c´, (ke´, ks´)) <> (curs (salloc vl dl), (kenil, kstop))).
Lemma loststep_not_free: forall p c ke ks c´ ke´ ks´ o o´,
n_dym_com_int_cd (c, (ke, ks)) ->
loststep p (c, (ke, ks)) o (c´,(ke´,ks´)) o´ ->
(forall (al : freelist) (v : option val),
~
(c = curs (sfree al v) /\
callcont ks = None /\ intcont ks = None)) ->
(forall al v,~ (c´ = curs (sfree al v) /\ callcont ks´ = None/\intcont ks´=None)).
Lemma tstep_to_osstep:
forall pc po pi ip tid c ke ks1 ks cst o2 Cl´ cst´ o´´ s f,
n_dym_com_int_cd (c, (ke, ks1 ## kcall f s empenv ks)) ->
ltstep (pc, (po, pi, ip)) tid (c, (ke, ks1 ## kcall f s empenv ks)) cst o2 Cl´ cst´ o´´ ->
(~ ((c, (ke, ks1)) = (curs sret, (kenil, ks1)) /\ callcont ks1 = None/\intcont ks1=None))->
( ~
(exists v ksx,
(c, (ke, ks1)) = (curs (sskip (Some v)), (kenil, kret ksx)) /\
callcont ksx = None/\intcont ksx =None)) ->
(forall (vl : vallist) (dl : decllist),
(c, (ke, ks1)) <> (curs (salloc vl dl), (kenil, kstop))) ->
(forall (al : freelist) (v : option val),
~
(c = curs (sfree al v) /\
callcont ks1 = None /\ intcont ks1 = None)) ->
InOS (c, (ke, ks1 ## kcall f s empenv kstop)) (pumerge po pi) ->
(exists c´ ke´ ks1´,
cst´ =cst /\ loststep (pumerge po pi) (c, (ke, ks1)) o2 (c´,(ke´,ks1´)) o´´ /\
Cl´=(c´, (ke´, ks1´ ## kcall f s empenv ks))/\
(forall (vl : vallist) (dl : decllist),
(c´, (ke´, ks1´)) <> (curs (salloc vl dl), (kenil, kstop)))/\
(forall al v,~ (c´ = curs (sfree al v) /\ callcont ks1´ = None/\intcont ks1´=None))).
Lemma inos_step_still: forall c ke ks1 f pc po pi ip tid c´ ke´ ks1´ cst cst´ o o´ ks s t d1 d2,
po f = Some (t,d1,d2 ,s) ->
goodks (pc,(po,pi,ip)) (ks1 ## kcall f s empenv ks)-> InOS (c, (ke, ks1 ## kcall f s empenv kstop)) (pumerge po pi) -> ltstep (pc, (po, pi, ip)) tid (c, (ke, ks1 ## kcall f s empenv ks)) cst
o (c´, (ke´, ks1´ ## kcall f s empenv ks)) cst´ o´ -> InOS (c´, (ke´, ks1´ ## kcall f s empenv kstop)) (pumerge po pi).
Lemma retv_step:
forall pc po pi ip tid v ksx f (s:stmts) ks cst o C´ cst´ o´ ft d1 d2,
po f = Some (ft,d1,d2,s) ->
callcont ksx = None ->
intcont ksx= None ->
ltstep (pc,(po,pi,ip)) tid (curs (sskip v), (kenil, kret ksx ## kcall f s empenv ks)) cst o C´ cst´
o´ -> o´ = o /\ cst´= cst /\ C´ = (curs (sfree (getaddr (snd (fst (get_smem o)))) v),(kenil,ksx ## kcall f s empenv ks)).
Lemma ret_step:
forall pc po pi ip tid ks1 f (s:stmts) ks cst o C´ cst´ o´ ft d1 d2,
po f = Some (ft,d1,d2,s) ->
callcont ks1 = None ->
intcont ks1= None ->
ltstep (pc,(po,pi,ip)) tid (curs sret, (kenil, ks1 ## kcall f s empenv ks)) cst o C´ cst´
o´ -> o´ = o /\ cst´= cst /\ C´ = (curs (sfree (getaddr (snd (fst (get_smem o)))) None),(kenil,ks1 ## kcall f s empenv ks)).
Lemma tstepev_osstepabt:
forall pc po pi ip tid c ke ks1 f s empenv ks cst Cl´ o2 ev,
ltstepev (pc, (po, pi, ip)) tid (c, (ke, ks1 ## kcall f s empenv ks))
cst o2 Cl´ cst o2 ev ->
notabort (c, (ke, ks1)) /\ loststepabt pi (c, (ke, ks1)) o2.
Lemma no_call_api_loststep_eq:
forall C C´ tst tst´ po pi ip,
no_call_api_os po pi ip ->
no_call_api C po ->
loststep (pumerge po pi) C tst C´ tst´ ->
loststep pi C tst C´ tst´.
Lemma no_call_api_loststep_still:
forall C C´ tst tst´ po pi ip,
no_call_api_os po pi ip ->
no_call_api C po ->
loststep (pumerge po pi) C tst C´ tst´ ->
no_call_api C´ po.
Lemma no_call_api_os_stmt:forall po pi ip f t d1 d2 s, no_call_api_os po pi ip -> pumerge po pi f = Some (t, d1, d2, s) -> no_call_api_stmt s po.
Lemma no_call_api_os_callcont:
forall ks po f s le ks´,
no_call_api_scont ks po ->
callcont ks = Some (kcall f s le ks´) ->
no_call_api_scont ks´ po.
Lemma no_call_api_os_intcont:
forall ks po c le ks´ ke,
no_call_api_scont ks po ->
intcont ks = Some (kint c ke le ks´) ->
no_call_api_cureval c po /\
no_call_api_scont ks´ po.
Qed.
Lemma cstep_no_api_local:
forall po pi c ke ks c´ ke´ ks´ o o´,
no_call_api (c,(ke,ks)) po ->
cstep pi (c, (ke, ks)) o (c´, (ke´, ks´)) o´ ->
cstep (pumerge po pi) (c, (ke, ks)) o (c´, (ke´, ks´)) o´.
Lemma loststep_no_api_local:
forall po pi c ke ks c´ ke´ ks´ o o´,
no_call_api (c,(ke,ks)) po ->
loststep pi (c, (ke, ks)) o (c´, (ke´, ks´)) o´ ->
loststep (pumerge po pi) (c, (ke, ks)) o (c´, (ke´, ks´)) o´.
Lemma nabt_lift: forall pc po pi ip c ke ks o cst tid ks´ f s,
no_call_api (c,(ke,ks)) po->
InOS (c, (ke, ks ## kcall f s empenv kstop)) (pumerge po pi) ->
~ loststepabt pi (c, (ke, ks)) o ->
~ltstepabt (pc, (po, pi, ip)) tid
(c, (ke, ks ## kcall f s empenv ks´)) cst o.
Lemma int_nabt_lift:
forall pc po pi ip c ke ks o cst tid ks´ cx kex lenv,
no_call_api (c,(ke,ks)) po->
InOS (c, (ke, ks ## kint cx kex lenv kstop)) (pumerge po pi) ->
~ loststepabt pi (c, (ke, ks)) o ->
~ltstepabt (pc, (po, pi, ip)) tid
(c, (ke, ks ## kint cx kex lenv ks´)) cst o.
Lemma inos_int´:forall c ke ks ks´ c´ ke´ po pi lenv, InOS (c, (ke, ks ## kint c´ ke´ lenv kstop)) (pumerge po pi) -> InOS (c, (ke, ks ## kint c´ ke´ lenv ks´)) (pumerge po pi).
Qed.
Lemma evalval_type: forall e m v, evalval e m = Some v -> exists t,evaltype e m = Some t.
Lemma isret_nabt:
forall c ke ks1 pc po pi ip tid f s cst o ks, IsRet (c, (ke, ks1)) -> InOS (c, (ke, ks1 ## kcall f s empenv kstop)) (pumerge po pi) -> ~(ltstepabt (pc,(po,pi,ip)) tid
(c, (ke, ks1 ## kcall f s empenv ks)) cst o).
Lemma isrete_nabt:
forall c ke ks1 pc po pi ip tid f s cst o ks, IsRetE (c, (ke, ks1)) -> InOS (c, (ke, ks1 ## kcall f s empenv kstop)) (pumerge po pi)-> ~(ltstepabt (pc,(po,pi,ip)) tid
(c, (ke, ks1 ## kcall f s empenv ks)) cst o).
Lemma free_local:forall m t b M´´ M M´ Ms Mf x, free t b m = Some M´´ -> free t b M = Some M´ -> MemMod.join m Ms x -> MemMod.join x Mf M -> MemMod.join (MemMod.merge M´´ Ms) Mf M´.
Lemma free_join_disj:forall t b m Ms x M´´,free t b m = Some M´´ -> MemMod.join m Ms x -> MemMod.disj M´´ Ms.
Lemma free_step:
forall pc po pi ip al o O Ms o1 Mf o2 o´´ cst cst´ Cl´ v ks1 ks f s ft d1 d2 tid,
po f = Some (ft,d1,d2,s) ->
callcont ks1 = None ->
intcont ks1 = None ->
freels al (get_mem (get_smem o)) empmem ->
InitTaskSt (emple_tst (substaskst o empmem), O) ->
joinmem o Ms o1 ->
joinmem o1 Mf o2 ->
ltstep (pc,(po,pi,ip)) tid
(curs (sfree al v),
(kenil, ks1 ## (kcall f s empenv ks))) cst o2 Cl´ cst´ o´´ ->
( o´´= emple_tst o2 /\ cst´= cst /\ Cl´ = (curs (sskip v), (kenil,ks))/\freels nil (get_mem (get_smem o)) empmem)\/
(exists o´ o1´ al´, joinmem o1´ Mf o´´ /\ joinmem o´ Ms o1´ /\
cst´=cst /\ Cl´ = (curs (sfree al´ v),
(kenil, ks1 ## (kcall f s empenv ks)))/\freels al´ (get_mem (get_smem o´)) empmem/\
InitTaskSt (emple_tst (substaskst o´ empmem), O)
) .
Lemma free_step_mem_join: forall M M1 M2 M3 M4 M´ t b, MemMod.join M M1 M2 -> MemMod.join M2 M3 M4 -> free t b M = Some M´ -> exists M´´, free t b M4 = Some M´´.
Lemma free_nabt:
forall o o´ o´´ pc po pi ip tid f ft d1 d2 s ks ks1 cst al v Ms Mf,
callcont ks1 = None ->
intcont ks1 = None ->
po f = Some (ft,d1,d2,s) ->
joinmem o Ms o´ ->
joinmem o´ Mf o´´ ->
freels al (get_mem (get_smem o)) empmem ->
~ ltstepabt (pc, (po, pi, ip)) tid
(curs (sfree al v), (kenil, ks1 ## (kcall f s empenv ks)))
cst o´´.
Require Import ruleLib.
Lemma eqdomo_disj: forall O O´ O´´, eqdomO O O´ -> OSAbstMod.disj O´´ O -> OSAbstMod.disj O´´ O´.
Lemma eqdomo_disj_merge: forall O O´ O´´,eqdomO O O´ -> OSAbstMod.disj O´´ O -> eqdomO (OSAbstMod.merge O´´ O) (OSAbstMod.merge O´´ O´).
Lemma abst_disj_get: forall O O´ x y,OSAbstMod.disj O´ O -> OSAbstMod.get O x = Some y -> OSAbstMod.get (OSAbstMod.merge O´ O) x = Some y .
Lemma hmstep1_disj:
forall ab ab´ O O´ O´´,
hmstep ab O ab´ O´ ->
OSAbstMod.disj O´´ O ->
OSAbstMod.disj O´´ O´.
Lemma hmstep_disj:
forall ab ab´ O O´ O´´,
hmstepstar ab O ab´ O´ ->
OSAbstMod.disj O´´ O ->
OSAbstMod.disj O´´ O´.
Lemma ltstep_no_exint:
forall c´ ke´ ks´ c ke lenv ks pc po pi ip cst cst´ Cl´ o2 o´´ t,
InOS (c´, (ke´, ks´ ## kint c ke lenv ks)) (pumerge po pi) ->
ltstep (pc, (po, pi, ip)) t (c´, (ke´, ks´ ## kint c ke lenv ks)) cst
o2 Cl´ cst´ o´´ ->
~ ((c´, (ke´, ks´)) = (curs (sprim exint), (kenil, ks´)) /\
callcont ks´ = None /\ intcont ks´ = None) ->
goodks (pc,(po,pi,ip)) (ks´ ## kint c ke lenv ks) ->
(exists c´´ ke´´ ks´´, Cl´ = (c´´, (ke´´, ks´´ ## kint c ke lenv ks))/\InOS (c´´, (ke´´, ks´´ ## kint c ke lenv ks)) (pumerge po pi)/\cst´=cst/\loststep (pumerge po pi) (c´, (ke´, ks´)) o2 (c´´,(ke´´,ks´´)) o´´).
Lemma callcont_int:forall ks´ c ke lenv ks le´ ks´1 f s, callcont (ks´ ## kint c ke lenv ks) = Some (kcall f s le´ ks´1) -> exists ks´´,callcont (ks´) = Some (kcall f s le´ ks´´).
Lemma callcont_int_nonone:
forall (ks´ : stmtcont) (c : cureval) (ke : exprcont)
(lenv : env) (ks : stmtcont) ,
callcont (ks´ ## kint c ke lenv ks) <> None ->
callcont ks´ <> None.
Lemma callcont_int_local: forall ks´ c ke lenv ks f s le´ ks´´,callcont (ks´ ## kint c ke lenv ks) =
Some (kcall f s le´ ks´´ ## kint c ke lenv ks) -> callcont ks´ = Some (kcall f s le´ ks´´).
Lemma callsome_intnone:forall ks´ c ke lenv ks , callcont ks´<>None -> intcont (ks´ ## kint c ke lenv ks) = None.
Lemma intcont_dec:forall ks, intcont ks <> None -> (exists c ke lenv ks´, intcont ks = Some (kint c ke lenv ks´)).
Qed.
Lemma ltstep_goodks: forall p t c´ ke´ ks´ c´´ ke´´ ks´´ cst o cst´ o´, ltstep p t (c´, (ke´, ks´ )) cst o (c´´, (ke´´, ks´´ )) cst´ o´ -> goodks p ks´ -> goodks p ks´´.
Lemma ltstepev_goodks :forall p t c ke ks c´ ke´ ks´ o o´ cst cst´ ev, goodks p ks ->
ltstepev p t (c,(ke,ks)) cst o (c´,(ke´,ks´)) cst´ o´ ev -> goodks p ks´.
Lemma isiret_nabt:forall pc po pi ip t c´ ke´ ks´ c ke lenv ks cst Ge Ee M M´ ir ls O i isrreg si I ab G,
IsIRet (c´,(ke´,ks´)) ->
(Ge, Ee, M´, ir, ls, O, ab) |= iretasrt i isrreg si I G->
~ ltstepabt (pc, (po, pi, ip)) t (c´, (ke´, ks´ ## kint c ke lenv ks))
cst (Ge, Ee, M, ir, ls) .
Lemma ltstep_eqg:
forall p t T cst S T´ S´ cst´ G,
ltstep p t T cst S T´
cst´ S´ -> fst (fst (fst (fst S))) = G ->fst (fst (fst (fst S´))) = G.
Lemma lpstep_eqg:
forall p S S´ cst cst´ t t´ T T´ G,
lpstep p T cst S t T´
cst´ S´ t´ -> fst (fst (fst (fst S))) = G ->fst (fst (fst (fst S´))) = G.
Lemma lpstep_goodks:
forall p S S´ cst cst´ t t´ T T´,
lpstep p T cst S t T´
cst´ S´ t´ -> good_t_ks p T -> good_t_ks p T´.
Lemma ge_n_change: forall p T cst S t T´ cst´ S´ t´,
lpstep p T cst S t T´ cst´ S´ t´ -> (gets_g S)=(gets_g S´).
Lemma lpstepev_goodks: forall p S S´ cst cst´ t t´ T T´ ev,
lpstepev p T cst S t T´
cst´ S´ t´ ev-> good_t_ks p T -> good_t_ks p T´.