Library tst_prop
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 auxdef.
Require Import Classical.
Require Import baseTac.
Require Import contLib.
Require Import asrtLib.
Require Import joinmemLib.
Require Import lmachLib.
Require Import loststepLib.
Require Import etraceref.
Lemma dladd_revlcons_eq: forall d1 d2, dladd d1 d2 = revlcons d1 d2.
Lemma r_lift_rule: forall Spec sd I r´ r p p´ s f ab vl P G,
Some r = BuildRetA P f ab vl G->
Some p = BuildPreA P f ab vl G->
Some r´ = BuildRetA´ P f ab vl ->
Some p´ = BuildPreA´ P f ab vl ->
{|Spec, sd, I, r´, Afalse|}|- {{p´}} s {{Afalse}} ->
{|Spec, sd, I, r, Afalse|}|- {{p}} s {{Afalse}}.
Lemma int_lift_rule: forall Spec sd I r´ r p p´ s i isrreg si ispec G,
p´ = ipreasrt´ i isrreg si ispec I ->
r´ = iretasrt´ i isrreg si I ->
p = ipreasrt i isrreg si ispec I G->
r = iretasrt i isrreg si I G->
{|Spec, sd , I, retfalse, r´|}|- {{p´}} s {{Afalse}} ->
{|Spec, sd , I, retfalse, r|}|- {{p}} s {{Afalse}}.
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 app_cons_length_lt : forall {A : Type} vl vl´ vl´´ (v : A),
vl ++ v :: vl´ = vl´´ ->
(length vl < length vl´´)%nat.
Lemma dl_add_dnil_eq : forall dl,
dl_add dl dnil = dl.
Lemma length_dl_revlcons_add : forall dl1 dl2 dl,
dl = revlcons dl1 dl2 ->
length_dl dl = (length_dl dl1 + length_dl dl2)%nat.
Lemma dl_add_revlcons_length_le : forall dl d1 d2,
dl_add dl dnil = revlcons d1 d2 ->
(length_dl d1 <= length_dl dl)%nat.
Lemma length_length_dl_eq : forall vl dl,
length_eq vl dl -> length vl = length_dl dl.
Lemma ltstep_good_is : forall p t C1 C2 cst1 cst2 tst1 tst2 m1 m2 r1 r2 ie1 ie2 is1 is2 cs1 cs2,
ltstep p t C1 cst1 tst1 C2 cst2 tst2 ->
tst1 = (m1, r1, (ie1, is1, cs1)) ->
tst2 = (m2, r2, (ie2, is2, cs2)) ->
good_is is1 ->
good_is is2.
Lemma Steq_projS_tid_neq_is_eq : forall t´ t S S´ m m´ r r´ ie ie´ is is´ cs cs´,
t´ <> t ->
Steq S S´ t ->
projS S t´ = Some (m, r, (ie, is, cs)) ->
projS S´ t´ = Some (m´, r´, (ie´, is´, cs´)) ->
is = is´.
Lemma projS_t_Snewt_t´ : forall S t t´ tst,
t <> t´ ->
(projS S t = Some tst <-> projS (Snewt S t´) t = Some tst).
Lemma Snewt_t_projS_t´ : forall S t t´ tst tst´,
projS S t = Some tst ->
projS (Snewt S t´) t = Some tst´ ->
t´ <> t ->
tst = tst´.
Lemma sstep_cont_locality : forall po pi c c´ ks ks´ ks´´ m m´,
sstep (pumerge po pi) c ks m c´ ks´ m´ ->
sstep (pumerge po pi) c (ks ## ks´´) m c´ (ks´ ## ks´´) m´.
Lemma cstep_cont_locality : forall po pi c c´ ke ke´ ks ks´ ks´´ m m´,
cstep (pumerge po pi) (c, (ke, ks)) m (c´, (ke´, ks´)) m´ ->
cstep (pumerge po pi) (c, (ke, ks ## ks´´)) m (c´, (ke´, ks´ ## ks´´)) m´.
Lemma fresh_join : forall M x m1 m2,
fresh M x ->
MemMod.join m1 m2 M ->
fresh m1 x.
Lemma minus_set_comm : forall M1 M2 l v,
~ MemMod.indom M2 l->
MemMod.minus (MemMod.set M1 l v) M2 = MemMod.set (MemMod.minus M1 M2) l v.
Lemma allocb_minus : forall len M m1 m2 b i,
fresh M b -> MemMod.join m1 m2 M ->
MemMod.minus (allocb M b i len) m2 = allocb m1 b i len.
Lemma alloc_minus_mem : forall i t le M le´ M´ m1 m2,
alloc i t le M le´ M´ ->
MemMod.join m1 m2 M ->
alloc i t le m1 le´ (MemMod.minus M´ m2).
Lemma join_minus_join_r : forall M m1 m2 m3 m4,
MemMod.sub m3 M ->
MemMod.join m1 m2 (MemMod.minus M m3) ->
MemMod.join m2 m3 m4 ->
MemMod.join m1 m4 M.
Lemma set_minus_comm : forall m m1 l a,
~ MemMod.indom m l -> MemMod.sub m1 m ->
MemMod.set (MemMod.minus m m1) l a = MemMod.minus (MemMod.set m l a) m1.
Lemma storebytes_minus : forall m1 m2 M M´ M´´ i t le le´ b o v,
MemMod.join m1 m2 M ->
alloc i t le M le´ M´ ->
EnvMod.get le´ i = Some (b, t) ->
storebytes M´ (b, o) (encode_val t v) = Some M´´ ->
storebytes (MemMod.minus M´ m1) (b, o) (encode_val t v) = Some (MemMod.minus M´´ m1).
Lemma alloc_minus_le : forall i t le M le´ M´ le1 le2,
alloc i t le M le´ M´ ->
EnvMod.join le1 le2 le ->
alloc i t le1 M (EnvMod.minus le´ le2) M´.
Lemma ptomvallist_loadbytes : forall l vl m, ptomvallist l vl m -> loadbytes m l (length vl) = Some vl.
Lemma type_val_mach_encode_val_decode_val : forall t v, rule_type_val_match t v =true -> decode_val t (encode_val t v) = v.
Lemma mapstoval_loadbytes:
forall b i t v m, rule_type_val_match t v = true -> mapstoval (b,i) t v m ->
exists bls, loadbytes m (b,i) (typelen t) = Some bls /\ (decode_val t bls = v).
Lemma mapstoval_load:
forall l t v m, rule_type_val_match t v = true -> mapstoval l t v m -> load t m l = Some v.
Lemma mapstoval_load_vptr : forall l tp v v´ m, (forall t n,tp<> Tarray t n) -> mapstoval l tp (Vptr v) m -> load tp m l = Some (Vptr v´) -> v = v´.
Lemma mem_join_minus : forall m1 m2 M M´ M´´,
MemMod.join m1 m2 M ->
MemMod.join M M´ M´´ ->
MemMod.join m2 M´ (MemMod.minus M´´ m1).
Lemma loadbytes_minus : forall len M b o o´ l x v,
loadbytes M (b, o) len = Some l ->
(o´ < o)%Z ->
ptomval (b, o´) v x ->
loadbytes (MemMod.minus M x) (b, o) len = Some l.
Lemma loadbytes_join : forall len M m1 m2 b o o´ l v,
(o´ < o)%Z ->
ptomval (b, o´) v m1 ->
MemMod.join m1 m2 M ->
loadbytes m2 (b, o) len = Some l ->
loadbytes M (b, o) len = Some l.
Lemma loadbytes_ptomvallist_memjoin : forall len m m´ M b o l v,
MemMod.join m m´ M ->
loadbytes M (b, o) len = Some l ->
ptomvallist (b, o) (list_repeat len v) m ->
loadbytes m (b, o) len = Some l.
Lemma mem_minus_disj: forall M M´, MemMod.disj (MemMod.minus M M´) M´.
Lemma sub_minus: forall M M1 M2, MemMod.sub M (MemMod.minus M1 M2) -> MemMod.sub M M1.
Lemma sub_minus_merge_eq: forall M´ M,
MemMod.sub M´ M->
MemMod.merge (MemMod.minus M M´) M´ = M.
Lemma minus_sub: forall M1 M M2, MemMod.sub M1 M ->MemMod.disj M1 M2 -> MemMod.sub M1 (MemMod.minus M M2).
Lemma sub_disj: forall M M1 M2, MemMod.disj M1 M2 -> MemMod.sub M M1 -> MemMod.disj M M2.
Lemma sub_minus_disj: forall Ml Ms Mc, MemMod.disj Ml Ms -> MemMod.sub Mc Ml ->
MemMod.disj (MemMod.merge Mc Ms) (MemMod.minus Ml Mc).
Lemma sub_minus_merge: forall Ml Ms Mc, MemMod.disj Ml Ms -> MemMod.sub Mc Ml ->
MemMod.meq (MemMod.merge (MemMod.merge Mc Ms) (MemMod.minus Ml Mc))
(MemMod.merge Ml Ms).
Lemma mem_join_join_disj:forall M1 M2 M3 M4 M5,MemMod.join M1 M2 M3 ->
MemMod.join M3 M4 M5 ->
MemMod.disj M1 M4.
Lemma join_merge_trans:forall M1 M2 M3 M4 M5,MemMod.join M1 M2 M3 -> MemMod.join M3 M4 M5 ->
MemMod.join M1 (MemMod.merge M2 M4) M5.
Lemma mem_disj_merge_minus_disj: forall Ml Mc Ms Ms´ Mc´,
MemMod.disj Mc´ Ms´->
MemMod.merge Mc´ Ms´ = MemMod.merge Mc Ms-> MemMod.disj Ml Ms -> MemMod.sub Mc Ml -> MemMod.disj (MemMod.merge (MemMod.minus Ml Mc) Mc´) Ms´.
Lemma mem_disj_merge_minus_merge: forall Ml Mc Ms Ms´ Mc´,
MemMod.disj Mc´ Ms´->
MemMod.merge Mc´ Ms´ = MemMod.merge Mc Ms-> MemMod.disj Ml Ms -> MemMod.sub Mc Ml -> MemMod.merge (MemMod.merge (MemMod.minus Ml Mc) Mc´) Ms´ = MemMod.merge Ml Ms.
Lemma mem_disj_merge_ass: forall M1 M2 M3 M4, MemMod.join M1 (MemMod.merge M2 M3) M4 ->
MemMod.disj M2 M3 ->
MemMod.join (MemMod.merge M1 M2) M3 M4.
Lemma join_merge_disj: forall M M1 M2 M3, MemMod.join M (MemMod.merge M1 M2) M3 -> MemMod.disj M M1.
Lemma join_disj_merge_join: forall M M1 M2 Mx, MemMod.join M M1 M2 ->
MemMod.disj M2 Mx ->
MemMod.join (MemMod.merge M Mx) M1 (MemMod.merge M2 Mx).
Lemma disj_sub_minus_merge: forall Mc Ml Ms,
MemMod.sub Mc Ml ->
MemMod.disj Ml Ms ->
MemMod.disj (MemMod.minus Ml Mc) (MemMod.merge Mc Ms).
Lemma mem_join_disj_trans: forall M M1 M2 M3 M4, MemMod.join M M1 M2 -> MemMod.join M2 M3 M4 ->
MemMod.disj M M3.
Lemma mem_join_join_join_eqmerge: forall M1 M2 M3 M4 M5 M6 M7,MemMod.join M1 M2 M3 ->
MemMod.join M3 M4 M5 ->
MemMod.join M5 M6 M7 ->
M7 = MemMod.merge (MemMod.merge M1 M4) (MemMod.merge M2 M6).
Lemma mem_join_join_join_disj_merge´: forall M1 M2 M3 M4 M5 M6 M7,MemMod.join M1 M2 M3 ->
MemMod.join M3 M4 M5 ->
MemMod.join M5 M6 M7 ->
MemMod.disj (MemMod.merge M1 M4) (MemMod.merge M2 M6).
Lemma mem_join_join_merge :forall M0 Mc M1 M m,MemMod.join M0 Mc M1 -> MemMod.join M1 M m -> MemMod.join (MemMod.merge M0 M) Mc m.
Lemma projs_ge_eq: forall S o t, projS S t = Some o -> (gets_g S) = (fst (fst (get_smem o))).
Lemma join_mem: forall a b c d e M M´, MemMod.join c M M´-> joinmem (a, b, c, d, e) M (a, b, M´, d, e).
Lemma join_merge_eq: forall o M, MemMod.disj (get_mem (get_smem o)) M -> joinmem o M (substaskst o (MemMod.merge (get_mem (get_smem o)) M)).
Lemma part_sub: forall M T Tm Mc t, partM M T Tm -> TMSpecMod.maps_to Tm t Mc ->
MemMod.sub Mc M.
Lemma projs_repl: forall o S tid, Some o = projS S tid -> substaskst o (snd (fst (fst S))) = o.
Parameter absopx:absop.
Lemma init_rdy_empm: forall o O x I, (forall ab,sat ((o, O),ab) (RDYINV I)) ->
substaskst o MemMod.emp = x->
InitTaskSt (x,OSAbstMod.emp) ->
InitTaskSt (o,O).
Lemma change_tstm_trans: forall o o´ o´´ M M´, substaskst o M = o´ -> substaskst o M´= o´´ ->
substaskst o´ M´ = o´´.
Lemma change_tstm_trans´: forall o M Ms, substaskst (substaskst o M) Ms = substaskst o Ms.
Lemma repl_change_tstm_trans: forall o M Ms, substaskst (substaskst o M) Ms = substaskst o Ms.
Lemma init_tst_oemp: forall o O, InitTaskSt (o,O) -> InitTaskSt (o,empabst).
Lemma join_tst_join: forall o M M´ o´, joinmem o M o´ -> substaskst o M´ = substaskst o´ M´.
Lemma repl_tst_join: forall o M M´ o´, joinmem o M o´ -> substaskst o M´ = substaskst o´ M´.
Lemma part_disjm: forall M T Tm Ms t Mc,
TMSpecMod.maps_to Tm t Mc ->
partM M T Tm -> MemMod.disj M Ms -> MemMod.disj Mc Ms.
Lemma part_merge_m: forall M T Tm M´ t C Mc,
TMSpecMod.maps_to Tm t Mc ->
MemMod.disj M M´ ->
partM M T Tm -> partM (MemMod.merge M M´) (TasksMod.set T t C) (TMSpecMod.put Tm t (MemMod.merge Mc M´)).
Lemma tm_mapsto_put: forall Tm t t´ a a´, t<>t´ -> TMSpecMod.maps_to (TMSpecMod.put Tm t a) t´ a´-> TMSpecMod.maps_to Tm t´ a´.
Lemma tm_mapsto_put´: forall Tm t t´ a a´, t<>t´-> TMSpecMod.maps_to Tm t´ a´ -> TMSpecMod.maps_to (TMSpecMod.put Tm t a) t´ a´.
Lemma sub_eqe: forall o M o´, substaskst o M = o´-> (snd (fst (get_smem o))) =(snd (fst (get_smem o´))).
Lemma init_emple: forall o O, InitTaskSt (o,O) -> (snd (fst (get_smem o))) =EnvMod.emp.
Lemma projs_eqm: forall o Sl t, projS Sl t = Some o -> (snd (fst (fst Sl))) = (snd (fst (fst o))).
Lemma init_empisr: forall o O, InitTaskSt (o,O) -> (snd (fst o))= empisr.
Lemma subs_eq_isr: forall o o´ M, o´ = substaskst o M -> (snd (fst o))= (snd (fst o´)).
Lemma projs_eq_isr: forall S o t, projS S t = Some o -> (snd (fst S)) = (snd (fst o)).
Lemma proj_stneq: forall S S´ t t´ o,
Steq S S´ t -> t´<>t -> projS S t´ = Some o -> fst (fst S) =fst (fst S´) ->
projS S´ t´ = Some ((fst (fst o)), (snd (fst S´)), (snd o)).
Lemma proj_stneq_ex: forall S S´ t t´ or,
Steq S S´ t -> t´<>t -> projS S t´ = Some or ->
projS S´ t´ =
Some
(
((gets_g S´),
(get_env (get_smem or)),
(gets_m S´)),
(snd (fst S´)),
(snd or)
).
Lemma proj_steq_eqdata: forall S S´ t o o´,
Steq S S´ t -> projS S t =Some o ->
projS S´ t = Some o´ -> fst (fst o) = fst (fst o´) ->
fst (fst S) = fst (fst S´).
Lemma join_trans: forall o o´ o´´ M M´, joinmem o M o´-> joinmem o´ M´ o´´ -> joinmem o (MemMod.merge M M´) o´´.
Lemma join_disj: forall o M o´, joinmem o M o´ -> MemMod.disj M (get_mem (get_smem o)).
Lemma join_disj_trans: forall o M o´ M´, joinmem o M o´ -> MemMod.disj M´ (get_mem (get_smem o´))
-> MemMod.disj M´ (get_mem (get_smem o)).
Lemma join_sub: forall o o´ M, joinmem o M o´-> MemMod.sub M (get_mem (get_smem o´)).
Lemma join_trans´: forall o o´ o´´ M M´, joinmem o M o´-> joinmem o´ M´ o´´ -> (exists o1, joinmem o1 M o´´).
Lemma sub_join_trans: forall o o´ o´´ M M´,
joinmem o M o´ ->
joinmem o´ M´ o´´ ->
MemMod.sub (get_mem (get_smem o))
(MemMod.minus (get_mem (get_smem o´´)) M).
Lemma sub_join_trans´: forall o o´ o´´ M M´ m,
joinmem o M o´ ->
joinmem o´ M´ o´´ ->
MemMod.sub m M´ -> MemMod.sub m (MemMod.minus (get_mem (get_smem o´´)) M).
Lemma join_eq_nmst: forall o o´ M, joinmem o M o´ -> substaskst o´ (get_mem (get_smem o))=o.
Lemma new_t_taskm_eq: forall S t, snd (fst (fst (Snewt S t))) = snd (fst (fst S)).
Lemma snewt_neqt: forall S t t´, t<>t´ -> projS (Snewt S t) t´ = projS S t´.
Lemma get_mem_eq: forall o, snd (fst (fst o))=get_mem (get_smem o).
Lemma partm_new: forall M Tl c c´ t t´ Tm Mc, partM M Tl Tm -> TMSpecMod.maps_to Tm t Mc -> partM M (TasksMod.set (TasksMod.set Tl t c) t´ c´) (TMSpecMod.put Tm t´ empmem).
Lemma projs_snew: forall S t, (fst (fst (fst (fst (Snewt S t))))) = InitG -> exists o, projS (Snewt S t) t = Some o /\ InitTaskSt (RdyChange (substaskst o empmem),empabst).
Lemma projs_nc_tst: forall S S´, (exists t a, projS S t= projS S´ t/\ projS S t= Some a /\ Steq S S´ t) -> S = S´.
Lemma partm_merge_disj: forall M T Tm t Mn Mc,
MemMod.disj M Mn->
TMSpecMod.maps_to Tm t Mc ->
partM M T Tm ->
partM (MemMod.merge M Mn) T (TMSpecMod.put Tm t (MemMod.merge Mc Mn)).
Lemma partm_minus_sub: forall M T Tm t Mc Mm,
MemMod.sub Mm Mc->
TMSpecMod.maps_to Tm t Mc ->
partM M T Tm ->
partM (MemMod.minus M Mm) T (TMSpecMod.put Tm t (MemMod.minus Mc Mm)).
Lemma join_subs_merge: forall o Mc Ms, MemMod.disj Mc Ms-> joinmem (substaskst o Mc) Ms
(substaskst (substaskst o Mc) (MemMod.merge Mc Ms)).
Lemma join_subs_merge_minus: forall Mc Ml Ms tst, MemMod.disj Ml Ms->MemMod.sub Mc Ml-> snd (fst (fst tst)) = MemMod.merge Ml Ms -> joinmem (substaskst tst (MemMod.merge Mc Ms)) (MemMod.minus Ml Mc) tst.
Lemma partm_nochange: forall C C´ M Tm T t, partM M T Tm ->
TasksMod.get T t =Some C->
partM M (TasksMod.set T t C´) Tm.
Lemma join_tst_wo_mem_eq: forall o o´ M, joinmem o M o´ -> TStWoMemEq o o´.
Lemma subs_tst_wo_mem_eq: forall o M, TStWoMemEq o (substaskst o M ).
Lemma tst_wo_mem_eq_subs_eq: forall o o´ M, TStWoMemEq o o´ -> substaskst o M = substaskst o´ M.
Lemma tst_wo_mem_eq_subs_trans: forall o o´ M, TStWoMemEq o (substaskst o´ M)-> TStWoMemEq o o´.
Lemma tst_wo_mem_eq_sym: forall o o´,TStWoMemEq o o´ -> TStWoMemEq o´ o.
Lemma tst_wo_mem_eq_trans: forall o o´ o´´, TStWoMemEq o o´ -> TStWoMemEq o´ o´´ ->
TStWoMemEq o o´´.
Lemma tst_wo_mem_eq_isremp_trans: forall o o´, TStWoMemEq o o´ -> (RdyChange o=o)-> (RdyChange o´=o´).
Lemma join_merge_minus: forall o o´ M M´ M´´, joinmem o M (substaskst o´ M´) ->
MemMod.disj M´´ (MemMod.minus M´ M)->
joinmem o M´´ (substaskst o´ (MemMod.merge M´´ (MemMod.minus M´ M))).
Lemma tst_subs_disj_join: forall o M Mc, MemMod.disj Mc M ->
joinmem (substaskst o Mc) M (substaskst o (MemMod.merge Mc M)).
Lemma join_disj_trans´: forall o o1 o2 o3 M1 M2 M3, joinmem o M1 o1 ->
joinmem o1 M2 o2 ->
joinmem o2 M3 o3 ->
MemMod.disj M1 M3.
Lemma join_add_disj:forall o o´ M Ms,
joinmem o M o´ ->
MemMod.disj (get_mem (get_smem o)) Ms ->
joinmem o Ms (substaskst o´ (MemMod.merge (get_mem (get_smem o)) Ms)).
Lemma join_join_disj: forall o o1 o2 M1 M2, joinmem o M1 o1 -> joinmem o1 M2 o2 -> MemMod.disj (get_mem (get_smem o)) M2.
Lemma join_join_join_move: forall oi0 M Ms Mf o o1 o2,
joinmem oi0 M o ->
joinmem o Ms o1 ->
joinmem o1 Mf o2 -> joinmem (substaskst o (MemMod.merge (get_mem (get_smem oi0)) Ms))
(MemMod.merge M Mf) o2.
Lemma tasks_set_get_neq: forall T t t´ a, t<>t´ -> TasksMod.get (TasksMod.set T t a) t´ = TasksMod.get T t´.
Lemma tasks_get_set: forall T t a, TasksMod.get (TasksMod.set T t a) t = Some a.
Lemma join_join: forall ge le M0 M ir ie is cs Mc´ o´ ,
joinmem (ge, le, MemMod.merge M0 M, ir, (ie, is, cs)) Mc´ o´ ->
joinmem (ge, le, M0, ir, (ie, is, cs)) Mc´ (ge, le,MemMod.merge M0 Mc´, ir, (ie, is, cs)).
Lemma disj_join_join:forall ge le M1 M2 ir ie is cs M3 o,
MemMod.disj M1 M2 ->
joinmem (ge, le, MemMod.merge M1 M2, ir, (ie, is, cs)) M3 o ->
joinmem (ge, le, MemMod.merge M1 M3, ir, (ie, is, cs)) M2 o.
Lemma abst_disj_merge_trans´: forall O1 O2 O3,
OSAbstMod.disj O1 (OSAbstMod.merge O2 O3) ->
OSAbstMod.merge (OSAbstMod.merge O2 O1) O3 =OSAbstMod.merge O1 (OSAbstMod.merge O2 O3).
Lemma abst_merge_disj:forall O O´ O´´, OSAbstMod.disj (OSAbstMod.merge O O´) O´´ ->
OSAbstMod.disj O O´´.
Lemma abst_disj_sym: forall O1 O2, OSAbstMod.disj O1 O2 <-> OSAbstMod.disj O2 O1.
Lemma abst_disj_mergel: forall O1 O2 O2´ O2´´, OSAbstMod.disj O1 O2 -> OSAbstMod.merge O2´ O2´´ = O2 -> OSAbstMod.disj O2´ O2´´-> OSAbstMod.disj (OSAbstMod.merge O1 O2´) O2´´.
Lemma abst_merge_com: forall O1 O2, OSAbstMod.disj O1 O2 -> OSAbstMod.merge O1 O2 = OSAbstMod.merge O2 O1.
Lemma abst_merge_ass: forall O1 O2 O3, OSAbstMod.merge O1 ( OSAbstMod.merge O2 O3)= OSAbstMod.merge ( OSAbstMod.merge O1 O2) O3.
Lemma abst_disj_trans:
forall O Oi Os,
OSAbstMod.disj O Oi ->
OSAbstMod.disj (OSAbstMod.merge Oi O) Os ->
OSAbstMod.disj O (OSAbstMod.merge Oi Os).
Lemma abst_merge_move:
forall O Oi Os,
OSAbstMod.disj O Oi ->
OSAbstMod.disj (OSAbstMod.merge Oi O) Os ->
OSAbstMod.merge (OSAbstMod.merge Oi O) Os =
OSAbstMod.merge O (OSAbstMod.merge Oi Os).
Lemma inittasks_good_t_ks:forall T pc cst O osc, InitTasks T pc cst O -> good_t_ks (pc, osc) T.
Fixpoint asrt_add_cell_to_tail (cell p:asrt):=
match p with
| Aemp => (cell ** Aemp)
| p1 ** p2 => (p1 ** (asrt_add_cell_to_tail cell p2))
| _ => p ** cell
end.
Lemma asrt_add_cell_to_tail_pqr: forall p q r, p ** (asrt_add_cell_to_tail q r) = asrt_add_cell_to_tail q (p ** r).
Lemma buildp_add_v: forall dl´ vl´ p i t v, good_decllist (dl_add dl´ (dcons i t dnil))= true -> length_eq vl´ dl´ -> buildp dl´ vl´ = Some p -> buildp (dl_add dl´ (dcons i t dnil)) (vl´++v::nil) =
Some ( asrt_add_cell_to_tail (Alvarmapsto i t v) p).
Lemma buildp_add_nil: forall vl´ p i t v, length_eq vl´ dnil -> buildp dnil vl´ = Some p -> buildp (dl_add dnil (dcons i t dnil)) (vl´++v::nil) =
Some ( Alvarmapsto i t v ** p).
Lemma buildp_add: forall dl´ vlh p i t, good_decllist (dl_add dl´ (dcons i t dnil))=true -> buildp dl´ vlh = Some p -> buildp (dl_add dl´ (dcons i t dnil)) vlh =
Some ( asrt_add_cell_to_tail (EX v : val, Alvarmapsto i t v) p).
Require Import baseTac.
Require Import tacticsforseplog.
Lemma asrt_add_cell_to_tail_sateq_star:
forall p q ge le M i au O ab,
(ge, le, M, i, au, O, ab) |= p ** q ->
(ge, le, M, i, au, O, ab) |= (asrt_add_cell_to_tail p q).
Require Import lmachLib.
Lemma alloc_sat:forall ge le le´ i t M M´ ir au O ab p dl vl, buildp dl vl = Some p -> alloc i t le M le´ M´ -> (ge, le, M, ir, au, O, ab) |= p -> (ge, le´, M´, ir, au, O, ab)
|= (EX v : val, Alvarmapsto i t v) ** p.
Lemma alloc_store_sat:forall ge le le´ i t M M´ M´´ ir au O ab p b v dl vl,buildp dl vl = Some p -> alloc i t le M le´ M´ -> EnvMod.get le´ i = Some (b, t) -> storebytes M´ (b, 0%Z) (encode_val t v) = Some M´´ -> (ge, le, M, ir, au, O, ab) |= p -> (ge, le´, M´´, ir, au, O, ab)
|= (Alvarmapsto i t v) ** p.
Lemma sat_lenv_mono : forall p dl vl ge le M ir au O ab i x t,
(ge, le, M, ir, au, O, ab) |= p ->
~ EnvMod.indom le i ->
buildp dl vl = Some p ->
(ge, EnvMod.set le i (x, t), M, ir, au, O, ab) |= p.
Lemma alloc_le_sat: forall i t le M le´ M´ dl´, eq_dom_env le (getlenvdom dl´) -> alloc i t le M le´ M´ -> eq_dom_env le´ (getlenvdom (dl_add dl´ (dcons i t dnil))).
Lemma mapsto_load_eq:forall m m´ M a tp v v´, (forall t n,tp<>Tarray t n) -> MemMod.join m m´ M -> mapstoval a tp (Vptr v) m -> load tp M a =
Some (Vptr v´) -> v =v´.
Lemma alloc_step_asrt:
forall p ge le le´ M´ M i0 au O ab dl´ i t vl,
buildp dl´ vl = Some p ->
(ge, le, M, i0, au, O, ab)
|= (p ** Aie true ** Ais nil ** Acs nil ** Aisr empisr) **
A_dom_lenv (getlenvdom dl´) ->
alloc i t le M le´ M´ ->
(ge, le´, M´, i0, au, O, ab)
|= ((asrt_add_cell_to_tail (EX v : val, Alvarmapsto i t v) p ) **
Aie true ** Ais nil ** Acs nil ** Aisr empisr )**
A_dom_lenv (getlenvdom (dl_add dl´ (dcons i t dnil))).
Lemma alloc_v_step_asrt´:
forall ge le le´ M´´ b M´ M i0 au O ab p dl´ x t v vl,
buildp dl´ vl = Some p ->
(ge, le, M, i0, au, O, ab)
|= (p ** Aie true ** Ais nil ** Acs nil ** Aisr empisr) **
A_dom_lenv (getlenvdom dl´) ->
alloc x t le M le´ M´ ->
EnvMod.get le´ x = Some (b, t) ->
store t M´ (b, 0%Z) v = Some M´´ ->
(ge, le´, M´´, i0, au, O, ab)
|= (( asrt_add_cell_to_tail (Alvarmapsto x t v) p) **
Aie true ** Ais nil ** Acs nil ** Aisr empisr)**
A_dom_lenv (getlenvdom (dl_add dl´ (dcons x t dnil))).
Lemma good_inv: forall o O ab I, sat ((o,O),ab) (INV I) -> forall ab´, sat ((o,O),ab´) (INV I).
Lemma emple_subs_inv:forall o o´ Ms Os I,TStWoMemEq (emple_tst o´) (emple_tst o) -> (forall ab : absop, (substaskst o Ms, Os, ab) |= INV I) -> (forall ab : absop, (substaskst o´ Ms, Os, ab) |= INV I).
Lemma isrnclear_nordy: forall o O I, (exists ir´ i, snd (fst o) = isrupd ir´ i true) ->
~(forall ab, (o, O, ab) |= RDYINV I).
Lemma tasks_set_eq_set2:
forall T t x y, TasksMod.set T t x = TasksMod.set (TasksMod.set T t y) t x .
Lemma sw_same_t: forall x tst O p cst T t´ l tp O´ Cl t sleft keh ksh ,
GoodSched (snd (snd p)) ->
TasksMod.get T t = Some Cl ->
OSAbstMod.get O curtid = Some (oscurt t) ->
(forall ab : absop, (tst, O, ab) |= SWPRE (snd (snd p)) x) ->
EnvMod.get (get_genv (get_smem tst)) x = Some (l,(Tptr tp)) ->
load (Tptr tp) (get_mem (get_smem tst)) (l,0%Z) = Some (Vptr t´) ->
OSAbstMod.set O curtid (oscurt t´) = O´ ->
hpstep p (TasksMod.set T t (curs (hapi_code (spec_seq sched sleft)), (keh, ksh))) cst O (TasksMod.set T t (curs (hapi_code sleft), (keh, ksh))) cst O´ /\ (forall ab,(tst,O ,ab) |= AHprio (snd (snd p)) t´ ** Atrue).
Lemma OSAbstMod_join_exists_merge :
forall O1 O2 O12 O,
OSAbstMod.join O1 O2 O12 ->
exists O´, OSAbstMod.join O1 O´ (OSAbstMod.merge O12 O).
Lemma swpre_prop: forall o O M O´ x sd,
(forall ab : absop, (substaskst o M, O´, ab) |= SWPRE sd x) -> MemMod.sub M (snd (fst (fst o))) ->
(forall ab : absop, (o, OSAbstMod.merge O´ O, ab) |= SWPRE sd x).
Lemma sw_has_code: forall x tst O T t´ l tp sd,
GoodSched sd ->
(forall ab : absop, (tst, O, ab) |= SWPRE sd x) ->
EnvMod.get (get_genv (get_smem tst)) x = Some (l,tp) ->
load tp (get_mem (get_smem tst)) (l,0%Z) = Some (Vptr t´)->
eqdomTO T O -> (exists C, TasksMod.get T t´ = Some C).
Lemma lpstep_good_is_S : forall p S cst t S´ cst´ t´ T T´,
good_is_S S ->
lpstep p T cst S t T´ cst´ S´ t´ ->
good_is_S S´.
Lemma tls_get_set: forall T t a, TaskLStMod.get (TaskLStMod.set T t a) t = Some a.
Lemma lpstepev_good_is_S : forall p S cst t S´ cst´ t´ T T´ ev,
good_is_S S ->
lpstepev p T cst S t T´ cst´ S´ t´ ev->
good_is_S S´.
Lemma good_inv_prop´:
forall p : asrt,
inv_prop p ->
GoodInvAsrt p ->
forall (ge le : env) (M : mem) aux aux´ (op : absop) abst,
(ge, le, M, empisr, aux, abst, op) |= p ->
forall (le´ : env) (op´ : absop) ,
(ge, le´, M, empisr, aux´, abst, op´) |= p.
Lemma starinv_isr_ncare_aux_ab: forall j i I ge le le´ m aux O ab ab´ aux´,
(ge, le, m , empisr, aux, O, ab)
|= starinv_isr I i j -> (ge, le´, m , empisr, aux´, O, ab´)
|= starinv_isr I i j .
Definition andaux (P Q : Prop):= P /\ Q.
Lemma Mem_join_disj_merge :
forall x x0 M1 M2, MemMod.join x x0 M1 ->
MemMod.disj x0 M2 ->
MemMod.disj x (MemMod.merge x0 M2) -> MemMod.disj M1 M2.
Lemma OSAbst_join_disj_merge :
forall x x0 M1 M2, OSAbstMod.join x x0 M1 ->
OSAbstMod.disj x0 M2 ->
OSAbstMod.disj x (OSAbstMod.merge x0 M2) -> OSAbstMod.disj M1 M2.
Lemma starinv_isr_prop_intro2´ : forall I i j, starinv_isr I 0%nat (j + S i)%nat ==>
starinv_isr I 0%nat j ** starinv_isr I (S j) i.
Lemma inv_isr_irrev_prop´ :
forall n low I ge le M aux aux´ abst op,
(ge, le, M ,empisr, aux, abst, op) |= starinv_isr I low n ->
forall le´ op´,
(ge, le´, M ,empisr, aux´, abst, op´) |= starinv_isr I low n.
Lemma invlth_isr_add:
forall i j ge le le´ le´´ M1 M2 aux aux´ O1 O2 ab ab´ ab´´ I,
MemMod.disj M1 M2 ->
OSAbstMod.disj O1 O2 ->
i< j-> j<= S INUM ->
(ge,le,M1,empisr,aux,O1,ab) |= invlth_isr I 0 i ->
(ge,le´, M2,empisr,aux,O2,ab´) |= invlth_isr I ((i+1)%nat) j ->
(ge,le´´,MemMod.merge M1 M2,empisr,aux´,OSAbstMod.merge O1 O2,ab´´) |= invlth_isr I 0 j.
Lemma invlth_isr_add´:
forall ge le le´ le´´ M1 M2 aux aux´ O1 O2 i j ab ab´ ab´´ I,
MemMod.disj M1 M2 ->
OSAbstMod.disj O1 O2 ->
i< j -> j<= S INUM->
(ge,le,M1,empisr,aux,O1,ab) |= invlth_isr I 0 i ->
(ge,le´, M2,empisr,aux,O2,ab´) |= invlth_isr I ((i+1)%nat) j ->
(ge,le´´,MemMod.merge M2 M1,empisr,aux´,OSAbstMod.merge O2 O1,ab´´) |= invlth_isr I 0 j.
Lemma invlth_add_sinum:
forall i ge le M M´ M´´ ir aux O O´ O´´ ab I,
i<= INUM ->
ir (S INUM) =false ->
MemMod.join M M´ M´´ ->
OSAbstMod.join O O´ O´´ ->
(ge,le,M´,ir,aux,O´,ab) |= invlth_isr I (i%nat) INUM ->
(ge,le,M,ir,aux,O,ab) |= getinv (I (S INUM)) ->
(ge,le,M´´,ir,aux,O´´,ab) |= invlth_isr I (i%nat) (S INUM).
Lemma invlth_divide:
forall i j ge le M ir au O ab I,
i<j ->
j<= S INUM ->
(ge,le,M,ir,au,O,ab) |= invlth_isr I 0 j ->
exists M1 M2 O1 O2,
MemMod.join M1 M2 M /\ OSAbstMod.join O1 O2 O /\
(ge,le,M1,ir,au,O1,ab) |= invlth_isr I 0 i /\ (ge,le,M2,ir,au,O2,ab) |= invlth_isr I (i+1)%nat j.
Lemma starinvnoisr_prop1_rev: forall j i I,
(starinv_noisr I i j) ** (starinv_noisr I (S (i+j)) 0)%nat ==>
(starinv_noisr I i (S j)).
Lemma invisr_imply_noisr : forall j ge le M ir aux O ab I , ( forall i : hid, ir i = false) ->
(ge, le, M, ir, aux, O, ab) |= starinv_isr I 0 j ->
(ge, le, M, ir, aux, O, ab) |= starinv_noisr I 0 j.
Lemma disj_inv_0_sinum_oemp:
forall ge le M ir aux O O´ ab I sd,
GoodI I sd->
(forall i, ir i = false) ->
(ge,le,M,ir,aux,O,ab) |= invlth_isr I 0 (S INUM) ->
OSAbstMod.disj O´ O ->
O´ = empabst.
Lemma invisr_imply_noisr´ : forall j ge le M ir aux O ab I , ( forall i : hid, i <= j -> ir i = false) ->
(ge, le, M, ir, aux, O, ab) |= starinv_isr I 0 j ->
(ge, le, M, ir, aux, O, ab) |= starinv_noisr I 0 j.
Lemma Mem_join_disj_disj_disj :
forall x x0 M1 M2 ,MemMod.join x x0 M2 -> MemMod.disj M1 x0 -> MemMod.disj M1 x -> MemMod.disj M1 M2 .
Lemma OSAbst_join_disj_disj_disj :
forall x x0 M1 M2 ,OSAbstMod.join x x0 M2 -> OSAbstMod.disj M1 x0 -> OSAbstMod.disj M1 x -> OSAbstMod.disj M1 M2 .
Lemma inv_isr_irrev_prop´´ :
forall n low I ge le M ir aux abst op,
(ge, le, M ,ir, aux, abst, op) |= starinv_isr I low n ->
forall le´ op´,
(ge, le´, M ,ir, aux, abst, op´) |= starinv_isr I low n.
Lemma invlth_add_sinum´:
forall i ge le M M´ M´´ ir aux O O´ O´´ ab I,
i<= INUM ->
MemMod.join M M´ M´´ ->
OSAbstMod.join O O´ O´´ ->
(ge,le,M´,ir,aux,O´,ab) |= invlth_isr I (i%nat) INUM ->
(ge,le,M,ir,aux,O,ab) |= getinv (I (S INUM)) ->
(ge,le,M´´,ir,aux,O´´,ab) |= invlth_isr I (i%nat) INUM** getinv (I (S INUM)).
Lemma Mem_disj_join_dis: forall M1 M2 x1 x0 x,MemMod.disj M1 M2 -> MemMod.join x1 x0 (MemMod.merge M1 M2) ->
MemMod.join x x0 M2 ->
MemMod.disj M1 x /\ x1 = MemMod.merge M1 x.
Lemma OSAbst_disj_join_dis: forall M1 M2 x1 x0 x,OSAbstMod.disj M1 M2 -> OSAbstMod.join x1 x0 (OSAbstMod.merge M1 M2) ->
OSAbstMod.join x x0 M2 ->
OSAbstMod.disj M1 x /\ x1 = OSAbstMod.merge M1 x.
Lemma mem_join_join_merge_eq:forall M1 M2 M3 M4 M, MemMod.join M1 M2 M -> MemMod.join M3 M4 M2 -> M = MemMod.merge M3 (MemMod.merge M1 M4).
Lemma abst_join_join_merge_eq´:forall O1 O2 O3 O4 O, OSAbstMod.join O1 O2 O -> OSAbstMod.join O3 O4 O2 -> O = OSAbstMod.merge (OSAbstMod.merge O1 O4) O3.
Lemma loststep_cont_locality: forall c ke ks o o´ c´ ke´ ks´ po pi ks´´, loststep (pumerge po pi) (c,(ke,ks)) o (c´,(ke´,ks´)) o´ -> loststep (pumerge po pi) (c,(ke,ks ## ks´´)) o (c´,(ke´,ks´ ## ks´´)) o´.
Lemma mem_join_disj_disj_join:forall M1 M2 M M´, MemMod.join M1 M2 M -> MemMod.disj M´ M1 -> MemMod.disj M´ M2 ->
MemMod.join M1 (MemMod.merge M2 M´) (MemMod.merge M´ M).
Lemma abst_join_disj_disj_join:forall M1 M2 M M´, OSAbstMod.join M1 M2 M -> OSAbstMod.disj M´ M1 -> OSAbstMod.disj M´ M2 ->
OSAbstMod.join M1 (OSAbstMod.merge M2 M´) (OSAbstMod.merge M´ M).
Lemma mem_disj_join_disjmerge:forall M M´ M1 M2, MemMod.disj M M´ -> MemMod.join M1 M2 M´ -> MemMod.disj (MemMod.merge M2 M) M1.
Lemma mem_disj_join_mergeeq:forall M M´ M1 M2, MemMod.disj M M´ -> MemMod.join M1 M2 M´ -> MemMod.merge (MemMod.merge M2 M) M1 = MemMod.merge M M´.
Lemma abst_disj_join_disjmerge:forall O O´ O1 O2, OSAbstMod.disj O O´ -> OSAbstMod.join O1 O2 O´ -> OSAbstMod.disj (OSAbstMod.merge O2 O) O1.
Lemma abst_disj_join_mergeeq:forall O O´ O1 O2, OSAbstMod.disj O O´ -> OSAbstMod.join O1 O2 O´ -> OSAbstMod.merge (OSAbstMod.merge O2 O) O1 = OSAbstMod.merge O O´.
Lemma mem_disj_join_disjmerge´:
forall M M´ M1 M2 : MemMod.map,
MemMod.disj M M´ ->
MemMod.join M1 M2 M´ -> MemMod.disj (MemMod.merge M M2) M1.
Lemma mem_join_disj_disj:
forall M1 M2 M´ M,
MemMod.join M1 M2 M ->
MemMod.disj M M´ ->
MemMod.disj M1 M´.
Lemma mem_join_join_disj_mergeeq: forall M1 M2 M3 M4 M M´,
MemMod.disj M M´ ->
MemMod.join M1 M2 M´ ->
MemMod.join M3 M4 (MemMod.merge M M2) ->
MemMod.merge M3 (MemMod.merge M4 M1) = MemMod.merge M M´.
Lemma abst_disj_join_disjmerge´:
forall O O´ O1 O2,
OSAbstMod.disj O O´ ->
OSAbstMod.join O1 O2 O´ -> OSAbstMod.disj (OSAbstMod.merge O O2) O1.
Lemma abst_join_disj_disj:
forall O1 O2 O´ O,
OSAbstMod.join O1 O2 O ->
OSAbstMod.disj O O´ ->
OSAbstMod.disj O1 O´.
Lemma abst_join_join_disj_mergeeq: forall O1 O2 O3 O4 O O´,
OSAbstMod.disj O O´ ->
OSAbstMod.join O1 O2 O´ ->
OSAbstMod.join O3 O4 (OSAbstMod.merge O O2) ->
OSAbstMod.merge O3 (OSAbstMod.merge O4 O1) = OSAbstMod.merge O O´.
Lemma mem_join_merge_merge_eq: forall M1 M2 M M´, MemMod.join M1 M2 M -> MemMod.disj M M´ -> MemMod.merge M1 (MemMod.merge M2 M´) = MemMod.merge M M´.
Lemma abst_join_merge_merge_eq: forall O1 O2 O O´, OSAbstMod.join O1 O2 O -> OSAbstMod.disj O O´ -> OSAbstMod.merge O1 (OSAbstMod.merge O2 O´) = OSAbstMod.merge O O´.
Lemma mem_join_disj_join: forall M1 M2 M M´, MemMod.join M1 M2 M -> MemMod.disj M´ M -> MemMod.join M1 (MemMod.merge M´ M2) (MemMod.merge M´ M).
Lemma abst_join_disj_join: forall O1 O2 O O´, OSAbstMod.join O1 O2 O -> OSAbstMod.disj O´ O -> OSAbstMod.join O1 (OSAbstMod.merge O´ O2) (OSAbstMod.merge O´ O).
Lemma mem_disj_join_join_sub:forall Ml Ms M M0 M1 Ms´, MemMod.disj Ml Ms -> MemMod.join M0 Ms´ M1 -> MemMod.join M1 M (MemMod.merge Ml Ms) -> MemMod.sub Ms (MemMod.merge Ml Ms) /\ MemMod.sub Ms´ (MemMod.merge Ml Ms).
Lemma swinv_isr_emp:
forall ge le m isr aux O ab I,
((ge,le,m,isr,aux),O,ab) |= SWINV I -> isr =empisr.
Lemma isr_false_eq : forall ir i , ir i = false -> ir = isrupd (isrupd ir i true) i false.
Lemma isr_false_sat1 : forall ir i ge le M ie is cs O ab ie´ (j : nat) cs´ I,
ir i = false ->
(ge,le,M,isrupd ir i true,(ie,i::is,cs),O,ab) |= getinv (I j) ->
(ge,le,M,ir,(ie´,is,cs´),O,ab) |= getinv (I j).
Lemma le_beq_nat_false : forall i j, i < j -> beq_nat i j = false.
Lemma isr_true_aux :
forall n i j ir I ge le M ie is cs ie´ cs´ abst op,
ir i = false ->
i < j ->
(ge, le, M , isrupd ir i true , (ie,i::is,cs), abst, op) |= starinv_isr I j n ->
(ge, le, M ,ir , (ie´,is,cs´), abst, op) |= starinv_isr I j n.
Lemma isr_true_S_i´:forall I i ge le M ir ie is cs ie´ cs´ ab O j,
i<j->
j<=INUM ->
ir i = false ->
(ge,le,M,isrupd ir i true,(ie,i::is,cs),O,ab) |= invlth_isr I (i+1)%nat j ** getinv (I (S INUM))->
(ge,le,M,ir,(ie´,is,cs´),O,ab) |= invlth_isr I (i+1)%nat j ** getinv (I (S INUM)).
Lemma swi_rdy_inv´: forall o Ol Os Ms Mc I t t´ S o´,
good_is_S S ->
(OSAbstMod.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)->
projS S t= Some o ->
projS S t´=Some o´ ->
(
exists Mc´ Ms´ Ol´ Os´,
MemMod.disj Mc´ Ms´ /\
MemMod.merge Mc´ Ms´ = MemMod.merge Mc Ms/\
OSAbstMod.disj Ol´ Os´/\
OSAbstMod.merge Ol´ Os´=OSAbstMod.merge Ol Os/\
(
((forall ab : absop, (substaskst o´ Ms´, Os´, ab) |= INV I)/\
(forall ab : absop, (substaskst o´ Mc´, Ol´, ab) |= RDYINV I))
)
).
Lemma rdyinv_isremp: forall o O I M, (forall ab, (substaskst o M,O,ab) |= RDYINV I) ->
(forall M´, RdyChange ( substaskst o M´)=(substaskst o M´)).
Lemma swi_rdy_eq_swi: forall o M Mr O Or I, (forall ab, (substaskst o M, O, ab) |= SWINV I)-> (forall ab, (substaskst o Mr, Or, ab) |= RDYINV I) -> (forall ab, (RdyChange (substaskst o Mr), Or, ab) |= SWINV I).
Lemma swinv_isremp: forall o O I,(forall ab, (o,O,ab) |= SWINV I) ->
(RdyChange o =o).
Lemma inv_substask_emple: forall genv lenv M1 ir aux Ms Os I,
( forall ab : absop,
(substaskst (genv, lenv, M1, ir, aux) Ms, Os, ab) |= INV I) ->
forall ab : absop,
(substaskst (genv, EnvMod.emp, M1, ir, aux) Ms, Os, ab) |= INV I.
Lemma InitAemp: forall genv lenv M ir aux O, InitTaskSt (genv,lenv,M,ir,aux,O) ->
forall ab : absop,
(genv, lenv, M, ir, aux, O, ab)
|= (Aemp ** Aie true ** Ais nil ** Acs nil ** Aisr empisr) **
A_dom_lenv (getlenvdom dnil).
Lemma build_api_asrt:
forall po pi ip A d1 d2 vl p´ t s f G,
dl_vl_match d1 (rev vl)=true ->
eqdomOS (po,pi,ip) A ->
po f = Some (t,d1,d2,s) ->
buildp (revlcons d1 d2) vl = Some p´ ->
(exists p r ab ft,(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).
Lemma bp_bpa: forall po pi ip A o O d1 d2 s vl pf t tl f p´ ab G,
eqdomOS (po,pi,ip) A ->
po f = Some (t,d1,d2,s) ->
(fst (fst A)) f = Some (ab, (t,(List.rev tl))) ->
Some pf = BuildPreA po f (ab,(t,(List.rev tl))) vl G->
buildp (revlcons d1 d2) vl = Some p´->
(forall ab : absop,
(o, O, ab)
|= (p´ ** Aie true ** Ais nil ** Acs nil ** Aisr empisr) **
A_dom_lenv (getlenvdom (revlcons d1 d2)))->
get_genv ((get_smem) o) = G ->
(o,O,(ab (List.rev vl)))|= pf.
Lemma inv_ncare_ab: forall o O ab I, (o,O,ab) |= INV I -> (forall ab´,(o,O,ab´)|= INV I).
Lemma joinmem_emple: forall o M o´, joinmem o M o´ -> joinmem (emple_tst o) M (emple_tst o´).
Lemma buildq_empO:forall dl o O ab q, buildq dl = Some q -> (o,O,ab) |= q -> emposabst O.
Lemma buildq_ncare_ab: forall dl x ab ab´ genv lenv m isr l O, buildq dl = Some x -> (genv,lenv,m,isr,l,O,ab) |= x -> (genv,lenv,m,isr,l,O,ab´) |= x.
Lemma retv_spec:
forall o O ab abs R vl po v f G,
Some R = BuildRetA po f ab vl G -> (o,O,abs) |= R (Some v) ->
freels (getaddr (snd (fst (get_smem o)))) (get_mem (get_smem o)) empmem /\
InitTaskSt (emple_tst (substaskst o empmem), O).
Lemma ret_spec:
forall o O ab abs R vl po f G,
Some R = BuildRetA po f ab vl G-> (o,O,abs) |= R None ->
freels (getaddr (snd (fst (get_smem o)))) (get_mem (get_smem o)) empmem /\
InitTaskSt (emple_tst (substaskst o empmem), O).
Lemma swpre_ncare_ab: forall o O ab x sd, (o,O,ab) |= SWPRE sd x -> (forall ab´,(o,O,ab´)|= SWPRE sd x).
Lemma swinv_ncare_ab: forall o O ab I, (o,O,ab) |= SWINV I -> (forall ab´,(o,O,ab´)|= SWINV I).
Require Import Coq.Logic.FunctionalExtensionality.
Lemma higherint_update_eq: forall i ir,higherint ir i -> ir = isrupd ir i false.
Lemma ret_st : forall (ge le : env) (M : mem) (ir : isr) (ei : ie)
(i0 : hid) (si0 : list hid) (ci : cs) (O : osabst)
(isrreg : isr) (i : hid) (si : list hid) (I : Inv) Ch gamma G,
(ge, le, M, ir, (ei, i0 :: si0, ci), O, gamma)
|= Agenv G //\\
<| Ch |> //\\
Aisr (isrupd isrreg i false) ** Ais (i :: si) ** Acs nil ** IRINV I ->
ir = (isrupd isrreg i false) /\ i0 = i /\ si0 = si /\ ci = nil /\ ge = G.
Lemma good_inv_prop_iret
: forall p ir (i:hid) ge le M op abst le´ op´ ie cs is ie´ cs´,
inv_prop p ->
GoodInvAsrt p ->
ir i = false ->
(ge, le, M, ir, (ie, i::is, cs), abst, op) |= p ->
(ge, le´, M, ir, (ie´,is,cs´), abst, op´) |= p.
Lemma starinv_isr_ncare_aux_ab_iret
: forall (j i : hid) (I : Inv) (ge le le´ : env)
(m : mem) (O : osabst) (ab ab´ : absop)
ie is cs ie´ cs´ ir f,
ir f =false ->
(ge, le, m, ir, (ie,f::is,cs), O, ab) |= starinv_isr I i j ->
(ge, le´, m, ir, (ie´,is,cs´), O, ab´) |= starinv_isr I i j.
Lemma xxx: forall ir i, isrupd ir i false i =false.
Lemma starinv_isr_ncare_ab: forall j i I ge isr le le´ m aux O ab ab´,
(ge, le, m , isr, aux, O, ab)
|= starinv_isr I i j -> (ge, le´, m ,isr, aux, O, ab´)
|= starinv_isr I i j .
Lemma invlth_isr_add_iret:
forall ge le le´ le´´ M1 M2 ir ie f is cs ie´ cs´ O1 O2 i j ab ab´ ab´´ I,
ir f = false ->
MemMod.disj M1 M2 /\ OSAbstMod.disj O1 O2 ->
i< j -> j<= S INUM->
(ge,le,M1,ir,(ie, f:: is, cs),O1,ab) |= invlth_isr I 0 i ->
(ge,le´, M2, ir,(ie, f :: is, cs),O2,ab´) |= invlth_isr I ((i+1)%nat) j ->
(ge,le´´,MemMod.merge M2 M1, ir, (ie´,is,cs´),OSAbstMod.merge O2 O1,ab´´) |= invlth_isr I 0 j.
Lemma iret_spec : forall (genv lenv : env) (m : mem) (isrreg : isr)
(ie0 : ie) (is0 : is) (cs0 : cs) (O Os : osabst)
(is´ : list hid) (i : hid) (ab : absop) (Ms : mem)
(I : Inv) ab´ abx G,
MemMod.disj m Ms ->
OSAbstMod.disj O Os ->
(substaskst (genv, lenv, m, isrupd isrreg i false, (ie0, is0, cs0)) Ms, Os, abx)
|= INV I ->
(genv, lenv, m, isrupd isrreg i false, (ie0, is0, cs0), O, ab)
|= Agenv G //\\
<|ab´|> //\\
Aisr (isrupd isrreg i false) ** Ais (i :: is´) ** Acs nil ** IRINV I ->
exists Ms´ Os´,
MemMod.merge m Ms = Ms´ /\
OSAbstMod.merge O Os = Os´ /\
(genv, lenv, Ms´, isrupd isrreg i false, (true, is´, cs0), Os´, ab) |= INV I /\
(genv, lenv, empmem, isrupd isrreg i false, (true, is´, cs0), empabst, ab)
|= Aemp.
Lemma inv_ncare_le:
forall ge le le´ m ir ls O ab I,
((ge, le, m, ir, ls), O,ab) |= INV I ->
((ge, le´, m, ir, ls), O,ab) |= INV I.
Lemma swpre_prop´: forall o O M O´ x ab sd, (substaskst o M, O´, ab) |= SWPRE sd x -> MemMod.sub M (snd (fst (fst o))) ->
( (o, OSAbstMod.merge O´ O, ab) |= SWPRE sd x).
Lemma swpre_locality:
forall ge le M1 M M´ ir ie is cs O O´ x aop sd,
MemMod.join M1 M M´->
(ge, le, M1, ir, (ie, is, cs), O,aop) |= SWPRE sd x ->
(ge, le, M´, ir, (ie, is, cs), OSAbstMod.merge O O´, aop)
|= SWPRE sd x.
Lemma swinv_inv_O: forall ge le M M´ O O´ Os´ ir ie is cs I aop sd,
GoodI I sd->
MemMod.disj M´ M ->
OSAbstMod.disj O´ Os´ ->
OSAbstMod.disj O (OSAbstMod.merge O´ Os´) ->
( (ge, le, M, ir, (ie, is, cs)), Os´, aop)
|= INV I ->
(ge, le, M´, ir, (ie, is, cs), O´, aop) |= SWINV I ->
O = empabst.
Lemma inv_noisr_irrev_prop_enint :
forall n low I ge le M ir i ie is cs abst op,
(ge, le, M ,ir, (ie,is,cs), abst, op) |= starinv_noisr I low n ->
forall le´ op´ ie´ cs´,
(ge, le´, M ,isrupd ir i true, (ie´,i::is,cs´) , abst, op´) |= starinv_noisr I low n.
Lemma isr_false_inv_eq:
forall i ge le M ir ie ie´ is cs cs´ O ab I,
i<INUM ->
higherint ir i ->
(ge,le,M,ir,(ie,is,cs),O,ab) |= invlth_isr I 0 i ->
(ge,le,M, isrupd ir i true, (ie´,i::is,cs´),O,ab) |= invlth_noisr I 0 i.
Lemma starinv_isr_prop4´ :
forall j i G E M isr ie is cs ie´ cs´ O aop I,
(G,E,M,isr,(ie,is,cs),O,aop) |= starinv_isr I (S i) j ->
(G,E,M,(isrupd isr i true),(ie´,i::is,cs´),O,aop) |= starinv_isr I (S i) j.
Lemma inv_isr_irrev_prop_noempisr :
forall n low I ge ir le M ie is cs ie´ cs´ abst op,
(ge, le, M , ir , (ie,is,cs), abst, op) |= starinv_isr I low n ->
forall le´ op´,
(ge, le´, M ,ir , (ie´,is,cs´), abst, op´) |= starinv_isr I low n.
Lemma isr_true_S_i_rev:
forall I i ge le M ir ie is cs ie´ cs´ ab ab´ O j,
i<j ->
(ge,le,M,ir,(ie,is,cs),O,ab) |= invlth_isr I (i+1)%nat j ->
(ge,le,M,isrupd ir i true,(ie´,i::is,cs´),O,ab´) |= invlth_isr I (i+1)%nat j.
Lemma invlth_isr_minus:
forall ge le M1 M2 ir aux O1 O2 i j ab ab´ ab´´ I,
i< j -> j<= S INUM ->
MemMod.disj M1 M2 -> OSAbstMod.disj O1 O2 ->
(ge,le, M2,ir,aux,O2,ab´) |= invlth_isr I ((i+1)%nat) j ->
(ge,le,MemMod.merge M1 M2,ir,aux,OSAbstMod.merge O1 O2,ab´´) |= invlth_isr I 0 j ->
(ge,le,M1,ir,aux,O1,ab) |= invlth_isr I 0 i .
Lemma invlth_isr_minus´:
forall ge le M1 M2 ir aux O1 O2 i j ab ab´ ab´´ I,
i< j -> j<= S INUM ->
MemMod.disj M1 M2 -> OSAbstMod.disj O1 O2 ->
(ge,le, M2,ir,aux,O2,ab´) |= invlth_isr I ((i+1)%nat) j**getinv (I (S INUM)) ->
(ge,le,MemMod.merge M1 M2,ir,aux,OSAbstMod.merge O1 O2,ab´´) |= invlth_isr I 0 j ** getinv (I (S INUM))->
(ge,le,M1,ir,aux,O1,ab) |= invlth_isr I 0 i .
Lemma nat_gt_neq:forall x y,x > y -> beq_nat x y = false.
Lemma en_int_inv:
forall Mi Ms´ ir is Os´ Oi x I i G,
MemMod.disj Mi Ms´ -> OSAbstMod.disj Oi Os´ ->
higherint ir i -> i < INUM ->
(forall ab : absop,
((G,empenv, (MemMod.merge Mi Ms´), ir, (true, is, nil)) ,
OSAbstMod.merge Oi Os´, ab) |= INV I)->
(forall ab : absop,
((G, empenv, Ms´, isrupd ir i true, (false, i :: is, nil)),
Os´, ab) |= INV I) ->
((G, empenv, Mi, isrupd ir i true, (false, i::is, nil)) ,
Oi, (x )) |= ipreasrt i ir is (x ) I G.
Lemma eqMs:forall Ml Ms Sl t tst o o´ Ms´ M O O´ I,
MemMod.disj Ml Ms ->
MemMod.merge Ml Ms = snd (fst (fst Sl)) ->
projS Sl t = Some tst ->
joinmem o´ M tst ->
joinmem o Ms´ o´ ->
(forall ab : absop, (substaskst tst Ms, O, ab) |= INV I) ->
forall ab : absop, (substaskst o Ms´, O´, ab) |= INV I ->
Ms=Ms´.
Lemma aux_le:forall Mc Ml Ms Sl t tst o´ o ,
MemMod.sub Mc Ml ->
MemMod.disj Ml Ms ->
MemMod.merge Ml Ms = snd (fst (fst Sl)) ->
projS Sl t = Some tst ->
joinmem o´ (MemMod.minus Ml Mc) tst ->
joinmem o Ms o´ ->
substaskst tst Mc = o.
Lemma p_lift:forall p a b c d G, Some p = BuildPreA a b c d G-> exists p´, Some p´ = BuildPreA´ a b c d .
Lemma r_lift:forall r a b c d G, Some r = BuildRetA a b c d G-> exists r´, Some r´ = BuildRetA´ a b c d .
Lemma no_os_goodks : forall p ks, no_os p ks -> goodks p ks.
Lemma no_os_goodks´: forall pc po pi ip ks, no_os (pc,(po,pi,ip)) ks -> goodks (pc,(po,pi,ip)) ks.
Lemma fun_goodks: forall pc po pi ip ks1 f s ks, goodks (pc, (po, pi, ip)) (ks1 ## kcall f s empenv ks) -> goodks (pc, (po, pi, ip)) ks.
Lemma tlmatch_dec:forall tl dl (vl:vallist), ~(tlmatch tl dl/\ tl_vl_match (rev tl) vl=true)\/ (tlmatch tl dl /\ tl_vl_match (rev tl) vl=true).
Lemma tlmatch_trans´: forall tl dl tl´, tlmatch tl´ dl -> ~ tlmatch tl dl -> tl<>tl´.
Lemma api_tlmatch: forall po pi ip B C f tp d1 d2 s D, eqdomOS (po,pi,ip) (B,C, D) -> po f = Some (tp, d1, d2, s) ->(exists ab tl tp, B f = Some (ab,(tp,tl))/\tlmatch tl d1).
Lemma pumerge_get: forall po pi f t d1 d2 s, po f= Some (t, d1, d2, s) -> (pumerge po pi) f = Some (t,d1,d2,s).
Lemma dl_add_nil_eq: forall dl, dl_add dl dnil =dl.
Lemma funbody_inos: forall s po pi f ft d1 d2 s´ pc, GoodStmt s (pumerge pc po)-> po f = Some (ft,d1,d2,s´) -> InOS (curs s,(kenil, kcall f s´ empenv kstop)) (pumerge po pi).
Lemma eq_tp: forall po pi ip A f ab t tl ft d1 d2 s, eqdomOS (po,pi,ip) A -> (fst (fst A)) f = Some (ab,(t,tl)) -> po f = Some (ft,d1,d2,s) -> ft= t /\ tlmatch tl d1.
Lemma tlmatch_trans´´: forall t1 t2 d1 , tlmatch t1 d1 -> tlmatch t2 d1 -> t1 =t2.
Lemma tlmatch_trans: forall d1 t1 t2, tlmatch t1 d1 -> tlmatch t2 d1 -> t1 =t2.
Lemma inos_sw_still: forall x ks1 ks f s po pi, InOS (curs (sprim (switch x)), (kenil, ks1 ## kcall f s empenv ks))
(pumerge po pi) -> InOS (SKIP, (kenil, ks1 ## kcall f s empenv ks))
(pumerge po pi).
Lemma int_inos_sw_still: forall x ks1 ks cx kex lenv po pi, InOS (curs (sprim (switch x)), (kenil, ks1 ## kint cx kex lenv ks))
(pumerge po pi) -> InOS (SKIP, (kenil, ks1 ## kint cx kex lenv ks))
(pumerge po pi).
Lemma intcont_local: forall ks´ c ke lenv ks,
intcont ks´ =None ->
callcont ks´=None ->
intcont (ks´ ## kint c ke lenv ks) = Some (kint c ke lenv ks).
Lemma inos_int:forall c ke ks ks´ c´ ke´ po pi lenv, InOS (c, (ke, ks ## kint c´ ke´ lenv ks´)) (pumerge po pi) -> InOS (c, (ke, ks ## kint c´ ke´ lenv kstop)) (pumerge po pi).
Lemma goodks_noinos_noos:
forall pc po pi ip ks f vl tl,
goodks (pc, (po, pi, ip)) ks ->
~ InOS (curs (sfexec f vl tl), (kenil, ks)) (pumerge po pi) ->
no_os (pc,(po,pi,ip)) ks.
Lemma goodks_callcont_still:
forall pc po pi ip ks f s lenv ks´´,
goodks (pc, (po, pi, ip)) ks ->
callcont ks = Some (kcall f s lenv ks´´)->
goodks (pc,(po,pi,ip)) ks´´.
Lemma goodks_intcont_still:
forall pc po pi ip ks c ke lenv ks´´,
goodks (pc, (po, pi, ip)) ks ->
intcont ks = Some (kint c ke lenv ks´´)->
goodks (pc,(po,pi,ip)) ks´´.
Lemma inos_call´: forall po pi f t d1 d2 s c ke ks ks´, po f = Some (t, d1, d2, s) -> InOS (c, (ke, ks ## kcall f s empenv ks´)) (pumerge po pi) -> InOS (c, (ke, ks ## kcall f s empenv kstop)) (pumerge po pi).
Lemma inos_call:forall c ke ks1 f s ks po pi, InOS (c, (ke, ks1 ## kcall f s empenv kstop)) (pumerge po pi) -> InOS (c, (ke, ks1 ## kcall f s empenv ks)) (pumerge po pi).
Lemma ks_add_int_false: forall ks ks´ c ke le, ks<> ks´ ## kint c ke le ks.
Require Import contLib.
Lemma goodks_callcont_os: forall pc po pi ip f s le ks´ ks, callcont ks = Some (kcall f s le ks´) -> goodks (pc,(po,pi,ip)) ks -> ( exists f0 le1 ks´´ t0 d1 d2 s0 s´,
callcont ks´ = Some (kcall f0 s0 le1 ks´´) /\
pumerge po pi f0 = Some (t0, d1, d2, s´)) -> exists a b c d, pumerge po pi f = Some (a,b,c,d).
Lemma goodks_intcont_os: forall pc po pi ip f s le ks´ ks, callcont ks = Some (kcall f s le ks´) -> goodks (pc,(po,pi,ip)) ks ->intcont ks´ <> None -> exists a b c d, pumerge po pi f = Some (a,b,c,d).
Lemma ks_add_call_false: forall ks ks´ f s le, ks<> ks´ ## kcall f s le ks.
Lemma goodks_int_inos´: forall ks´ c ke lenv ks pc po pi ip c´ ke´,goodks (pc, (po, pi, ip)) (ks´ ## kint c ke lenv ks) -> InOS (c´, (ke´, ks´ ## kint c ke lenv ks)) (pumerge po pi).
Lemma goodks_int_int_inos:
forall pc po pi ip c ke lenv ks ks´ x2 c0 ke0 le´,
goodks (pc, (po, pi, ip)) (ks´ ## kint c ke lenv ks) ->
InOS (curs (sprim exint), (kenil, ks´ ## kint c ke lenv ks))
(pumerge po pi) ->
intcont (ks´ ## kint c ke lenv ks) =
Some (kint c0 ke0 le´ x2 ## kint c ke lenv ks) ->
InOS (c0, (ke0, x2 ## kint c ke lenv ks)) (pumerge po pi).
Lemma goodks_int_inos: forall pc po pi ip c ke lenv ks ks´ ks´´ f s le´, goodks (pc, (po, pi, ip)) (ks´ ## kint c ke lenv ks) -> callcont (ks´ ## kint c ke lenv ks) =
Some (kcall f s le´ ks´´ ## kint c ke lenv ks) -> ((exists f0 le0 ks´0 t0 d1 d2 s0 s´,
callcont (ks´ ## kint c ke lenv ks) = Some (kcall f0 s0 le0 ks´0) /\
pumerge po pi f0 = Some (t0, d1, d2, s´)) \/
intcont (ks´ ## kint c ke lenv ks) <> None) -> (
(exists f0 le0 ks´0 t0 d1 d2 s0 s´,
callcont (ks´´ ## kint c ke lenv ks) = Some (kcall f0 s0 le0 ks´0) /\
pumerge po pi f0 = Some (t0, d1, d2, s´)) \/
intcont (ks´´ ## kint c ke lenv ks) <> None).
Lemma goodks_call_inos: forall pc po pi ip lenv ks ks´ ks´´ f s f´ s´ le´ t d1 d2,po f = Some (t,d1 ,d2,s) -> goodks (pc, (po, pi, ip)) (ks´ ## kcall f s lenv ks) -> callcont (ks´ ## kcall f s lenv ks) =
Some (kcall f´ s´ le´ (ks´´ ## kcall f s lenv ks)) -> ((exists f0 le0 ks´0 t0 d1 d2 s0 s´,
callcont (ks´ ## kcall f s lenv ks) = Some (kcall f0 s0 le0 ks´0) /\
pumerge po pi f0 = Some (t0, d1, d2, s´)) \/
intcont (ks´ ## kcall f s lenv ks) <> None) -> (
(exists f0 le0 ks´0 t0 d1 d2 s0 s´,
callcont (ks´´ ## kcall f s lenv ks) = Some (kcall f0 s0 le0 ks´0) /\
pumerge po pi f0 = Some (t0, d1, d2, s´)) \/
intcont (ks´´ ## kcall f s lenv ks) <> None).
Lemma goodks_int_call_inos´: forall pc po pi ip ks1 f c´ ke´ le´ t d1 d2 s ks ks´´,
pumerge po pi f = Some (t,d1,d2,s) ->
goodks (pc, (po, pi, ip)) (ks1 ## kcall f s empenv ks) -> intcont (ks1 ## kcall f s empenv ks) =
Some (kint c´ ke´ le´ ks´´) ->
(exists f0 le ks´ t0 d0 d3 s0 s´,
callcont ks´´= Some (kcall f0 s0 le ks´) /\
pumerge po pi f0 = Some (t0, d0, d3, s´)) \/
intcont ks´´<> None.
Lemma goodks_int_call_inos: forall pc po pi ip ks1 f c´ ke´ le´ ks1´ t d1 d2 s ks,
po f = Some (t,d1,d2,s) ->
goodks (pc, (po, pi, ip)) (ks1 ## kcall f s empenv ks) -> intcont (ks1 ## kcall f s empenv ks) =
Some (kint c´ ke´ le´ (ks1´ ## kcall f s empenv ks)) -> InOS (c´, (ke´, ks1´ ## kcall f s empenv ks)) (pumerge po pi).
Lemma dl_add_move: forall dl´ dl d1 d2 i t, dl_add dl´ (dcons i t dl) = revlcons d1 d2 -> dl_add (dl_add dl´ (dcons i t dnil)) dl = revlcons d1 d2.
Lemma list_move: forall vl´ (v:val) vl, vl´++(v::vl)= (vl´++v::nil)++vl.
Lemma addtail_length_eq: forall vl´ dl´ v x t,length_eq vl´ dl´ -> length_eq (vl´ ++ v :: nil) (dl_add dl´ (dcons x t dnil)).
Lemma tl_rev_eq:forall (tl:typelist) tl´, rev tl = rev tl´ -> tl = tl´.
Lemma rev_cons_n_nil: forall a (l:typelist), ~ nil= rev(a::l).
Qed.
Fixpoint length_eq_td (tl:typelist) (dl:decllist) :=
match tl with
| nil => match dl with
| dnil => True
| _ => False
end
| t::tl´ => match dl with
| dcons a b dl´ => length_eq_td tl´ dl´
| _ => False
end
end.
Lemma tlmatch_lengtheq: forall tl dl, tlmatch tl dl -> length_eq_td tl dl.
Lemma tl_dl_vl_eq:forall tl dl vl, tlmatch (rev tl) dl -> length vl = length tl -> length_eq vl dl.
Lemma sub_len_neq:forall vl´ vlh d1 v vl dl´ d2,length_eq vlh d1 -> vl´ ++ v :: vl = vlh -> dl_add dl´ dnil = revlcons d1 d2 -> ~ (length_eq vl´ dl´).
Lemma good_dl_add: forall d1 d2 dl´ i t dl, good_decllist (revlcons d1 d2) = true -> dl_add dl´ (dcons i t dl) = revlcons d1 d2 -> good_decllist (dl_add dl´ (dcons i t dnil)) =true.
Lemma mem_disj_join2_disj:
forall o1´ Ms o1 M oo Mc ,
MemMod.disj (get_mem (get_smem o1´)) Ms ->
joinmem o1 M o1´ ->
joinmem oo Mc o1 ->
MemMod.disj Mc Ms.