Library asrtLib
Require Import include.
Require Import memory.
Require Import memdata.
Require Import Lists.ListSet.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import lemmasforseplog.
Require Import inferules.
Require Import tacticsforseplog.
Require Import lmachLib.
Require Import contLib.
Require Import joinmemLib.
Require Import loststepLib.
Require Import baseTac.
Ltac trysimplsall := repeat progress (simpl substmo in *;
simpl substaskst in *;
simpl getmem in *;
simpl getabst in *;
simpl substmo in *;
simpl getisr in *;
simpl getis in *;
simpl getie in *;
simpl gettopis in *;
simpl getcs in *;
simpl get_smem in *;
simpl get_mem in *;
simpl gettopis in *;
simpl starinv_isr in *).
Tactic Notation "invertstep" tactic (t) :=
repeat progress
match goal with
| H : (_, _) = (_, _) |- _ => inverts H; tryfalse
| H : estep _ _ _ _ _ _ |- _ => inverts H
| H : loststep _ _ _ _ _ |- _ => inverts H
| H : cstep _ _ _ _ _ |- _ => inverts H
| H : sstep _ _ _ _ _ _ _ |- _ => inverts H
| _ => t
end.
Ltac destru m := (let H := fresh in destruct m as ( H & m)).
Ltac casenot H := apply Classical_Prop.not_and_or in H;
let Hc := fresh "Cs" in ( destruct H as [Hc | H];
[apply Classical_Prop.NNPP in Hc| ]).
Lemma absop_aux : forall s, emposabst s -> s = OSAbstMod.emp.
Lemma absop_aux2 : forall s, empst s -> getabst s =OSAbstMod.emp.
Lemma good_inv_prop :
forall p, GoodInvAsrt p ->
forall ge le M ir ie is cs abst op,
(ge, le, M ,ir, (ie ,is,cs), abst, op) |= p ->
forall le´ op´ ie´ cs´,
(ge,le´, M, ir, (ie´,is,cs´) ,abst, op´) |= p.
Lemma absop_emp_asrt :
forall p ,
AbsOsEmpAsrt p ->
forall o abs op ,
(o, abs, op ) |= p -> abs = OSAbstMod.emp.
Lemma Emp_AbsOs_Asrt_prop :
forall p,
AbsOsEmpAsrt p -> Emp_AbsOs_Asrt p.
Lemma emp_absos_asrt_prop : forall p ,
Emp_AbsOs_Asrt p -> forall o O aop , sat (o,O,aop) p -> O = empabst.
Lemma precise_Astar :
forall P Q,
precise P -> precise Q -> precise (P ** Q).
Definition cjy_and := and.
Qed.
Lemma precise_Apure :
forall P,
precise ([| P |]).
Lemma precise_Aie_Adisj :
forall P Q,
precise P -> precise Q -> precise (Aie true ** P \\// Aie false ** Q).
Lemma precise_starinv_isr :
forall I low n,
precise (starinv_isr I low n).
Lemma inv_precise_prop :
forall I,
precise (INV I).
Lemma inv_precise_imply_eqm :
forall G E M Ms Ms´ I isr aux Os Os´ ab M´ M´´,
(G, E, Ms, isr, aux, Os, ab) |= INV I ->
(G, E, Ms´, isr, aux, Os´, ab) |= INV I ->
MemMod.join M Ms M´´ ->
MemMod.join M´ Ms´ M´´ ->
M = M´ /\ Ms = Ms´.
Lemma inv_precise_imply_eqo :
forall G E Ms Ms´ isr aux Os Os´ ab I O O´ O´´,
(G, E, Ms, isr, aux, Os, ab) |= INV I ->
(G, E, Ms´, isr, aux, Os´, ab) |= INV I ->
OSAbstMod.join O Os O´´ ->
OSAbstMod.join O´ Os´ O´´ ->
O = O´ /\ Os = Os´.
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 inv_noisr_irrev_prop :
forall n low I ge le M ir aux abst op,
(ge, le, M ,ir, aux, abst, op) |= starinv_noisr I low n ->
forall le´ op´,
(ge, le´, M ,ir, aux, abst, op´) |= starinv_noisr I low n.
Lemma INV_irrev_prop :
forall I ge le M ir aux abst op,
(ge, le, M ,ir, aux, abst, op) |= INV I ->
forall le´ op´,
(ge, le´, M ,ir, aux, abst, op´) |= INV I.
Lemma SWPRE_irrev_prop :
forall x ge le M ir aux abst op sd,
(ge, le, M ,ir, aux, abst, op) |= SWPRE sd x ->
forall le´ op´,
(ge, le´, M ,ir, aux, abst, op´) |= SWPRE sd x.
Lemma SWINV_irrev_prop :
forall I ge le M ir aux abst op,
(ge, le, M ,ir, aux, abst, op) |= SWINV I ->
forall le´ op´,
(ge, le´, M ,ir, aux, abst, op´) |= SWINV I.
Lemma RYDINV_irrev_prop :
forall I ge le M ir aux abst op,
(ge, le, M ,ir, aux, abst, op) |= RDYINV I ->
forall le´ op´,
(ge, le´, M ,ir, aux, abst, op´) |= RDYINV I.
Lemma IRINV_irrev_prop :
forall I ge le M ir aux abst op,
(ge, le, M ,ir, aux, abst, op) |= IRINV I ->
forall le´ op´,
(ge, le´, M ,ir, aux, abst, op´) |= IRINV I.
Lemma good_frame_asrt_prop:
forall p, GoodFrame p ->
forall ge le M ir aux abst op,
(ge,le,M , ir, aux,abst, op) |= p ->
abst = empabst /\
forall op´ ge´ le´ ir´ aux´,
(ge´,le´,M ,ir´, aux´,abst, op´) |= p.
Lemma good_fun_asrt_absop:
forall p, GoodFunAsrt p ->
forall ge le M ir aux abst op,
(ge,le,M , ir, aux,abst, op) |= p ->
forall le´,
(ge,le´,M ,ir, aux,abst, op) |= p.
Lemma alloc_inv_prev : forall p vl dl o C o´ ks Ms Os ab I,
losallocstep p (curs (salloc vl dl), (kenil, ks)) o C o´ ->
(substaskst o Ms, Os, ab) |= INV I ->
(substaskst o´ Ms, Os, ab) |= INV I.
Lemma tl_vl_dl: forall tl vl dl, tl_vl_match tl vl = true -> tlmatch tl dl -> dl_vl_match dl vl =true.
Lemma tl_vl_match_leneq: forall tl vl, tl_vl_match tl vl = true -> length vl =length tl.
Lemma tl_vl_match_leneq´: forall tl vl, tl_vl_match (rev tl) vl = true -> length vl =length tl.
Lemma tl_vl_rev_match:
forall tl vl, tl_vl_match tl vl = tl_vl_match (rev tl) (rev vl).
Lemma vl_app_v_h_t : forall {T} vl v, exists (h:T) t, vl ++ v :: nil = h :: t.
Lemma tl_vl_match_true_append : forall tl vl t v, tl_vl_match tl vl = true ->
tl_vl_match (tl ++ t :: nil) (vl ++ v :: nil) = tl_vl_match (t :: nil) (v :: nil).
Lemma tl_vl_match_false_append : forall tl vl t v, tl_vl_match tl vl = false ->
tl_vl_match (tl ++ t :: nil) (vl ++ v :: nil) = false.
Qed.
Lemma rev_tl_vl: forall tl vl, tl_vl_match (rev tl) vl =true -> tl_vl_match tl (rev vl) = true.
Lemma tl_vl_dl´: forall tl vl dl, tl_vl_match (rev tl) vl = true -> tlmatch tl dl -> dl_vl_match dl (rev vl) =true.
Lemma tl_vl_dl´´: forall tl vl dl, tl_vl_match tl vl = true -> tlmatch (rev tl) dl -> dl_vl_match dl (rev vl) =true.
Lemma build_pre_ret_exist : forall f tl tp Spec pre post vl d1 d2 s p0 ll,
tl_vl_match (rev tl) vl = true -> tlmatch tl d1 ->
good_decllist (revlcons d1 d2) = true ->
p0 f = Some (tp, d1, d2, s) ->
Spec f = Some (pre, post, (tp, tl)) ->
(exists p , Some p = BuildPreI p0 f vl ll pre) /\ (exists r , Some r = BuildRetI p0 f vl ll post).
Lemma alloc_notabortm : forall v d ks,notabortm (curs (salloc v d), (kenil, ks)).
Lemma alloc_lemma_aux: forall d1 asrt vl a M1 M2 M ir aux Os p n aop o G E0 ks s f E,
GoodFunAsrt asrt ->
buildp d1 vl = (Some a) ->
MemMod.join M1 M2 M ->
(G, E, M1, ir, aux, Os, aop) |= asrt ->
losallocstepn n p
(curs (salloc vl d1),
(kenil, kcall f s E ks)) (G, E0, M, ir, aux)
(curs (salloc nil dnil), (kenil, kcall f s E ks)) o ->
exists E1 E2 M´,
EnvMod.join E0 E1 E2 /\
joinmem (G, E2, M´, ir, aux) M2 o /\
(G, E2, M´, ir, aux, Os, aop)
|= (a **asrt) /\(
(G, E1, empmem, ir, aux, empabst, aop)
|= A_dom_lenv (getlenvdom d1)//\\ <|aop|>).
Lemma alloc_lemma : forall prespec s ks n p f vl d1 d2 E G M1 M2 M ir aux o Os aop pre tp stmt ll,
Some prespec = BuildPreI p f vl ll pre ->
p f = Some (tp ,d1, d2, stmt) ->
dl_vl_match d1 (rev vl) =true->
MemMod.join M1 M2 M ->
(G, E, M1, ir, aux, Os, aop) |= PRE [pre, rev vl, ll] ->
losallocstepn n p
(curs (salloc vl (revlcons d1 d2)),
(kenil, kcall f s E ks)) (G, empenv, M, ir, aux)
(curs (salloc nil dnil), (kenil, kcall f s E ks)) o ->
exists E´ M´ , joinmem (G, E´,M´, ir ,aux ) M2 o
/\ ((G, E´,M´, ir ,aux ), Os, aop) |= prespec.
Lemma fcall_not : forall c ke ks ks´, ~ IsFcall (c, (ke, ks ## ks´)) -> ~ IsFcall (c, (ke, ks )).
Lemma fcall_kstop : forall c ke ks f s E ks´,
~ IsFcall (c, (ke, ks ## kcall f s E ks´)) ->
~ IsFcall (c, (ke, ks ## kcall f s E kstop)).
Lemma freev_notabortm : forall vl v ke ks, notabortm (curs (sfree vl v),(ke,ks)).
Lemma not_skipend : forall c ke ks f s E ks´,
~IsEnd (c, (ke, ks ## kcall f s E ks´)).
Lemma exint_notabortm :
forall ks f s E ks´,
notabortm (curs (sprim exint), (kenil, ks ## kcall f s E ks´)) ->
notabortm (curs (sprim exint), (kenil, ks ## kcall f s E kstop)).
Lemma swpre_join_prop :
forall o M o´ O aop x sd ,
joinmem o M o´ ->
(o, O, aop) |= SWPRE sd x -> (o´, O, aop) |= SWPRE sd x.
Lemma OsAbst_Merge_eq : forall O Os O´ , OSAbstMod.disj O Os ->
OSAbstMod.disj O´ Os ->
OSAbstMod.merge O Os = OSAbstMod.merge O´ Os ->
O = O´.
Lemma IsFcall_kstop : forall v ks f s E,
~ IsFcall (curs (sfree nil v), (kenil, ks ## kcall f s E kstop)).
Lemma freeb_join_elim :
forall M b i n M´,
freeb M b i n = Some M´ ->
exists M´´, MemMod.join M´ M´´ M.
Lemma free_frame_prop : forall tp b M M´ M1 MM MM´ Ms Mf, free tp b M = Some M´-> free tp b MM = Some MM´ -> MemMod.join M Ms M1 ->
MemMod.join M1 Mf MM -> exists M´´, MemMod.join M´ Ms M´´ /\ MemMod.join M´´ Mf MM´.
Lemma free_locality_pre : forall b i n M´ M Ms Mf M1 M2 , freeb M b i n = Some M´-> MemMod.join M Ms M1 -> MemMod.join M1 Mf M2 -> exists M´´, freeb M2 b i n = Some M´´ .
Lemma free_locality: forall tp b M´ M Ms Mf M1 M2 , free tp b M = Some M´-> MemMod.join M Ms M1 -> MemMod.join M1 Mf M2 -> exists M´´, free tp b M2 = Some M´´ .
Inductive freels : freelist -> mem -> mem -> Prop :=
| freelist_0 : forall M, freels nil M M
| freelist_n : forall b t ls M M´´ M´, free t b M = Some M´´ -> freels ls M´´ M´ ->
freels (cons (b,t) ls) M M´.
Inductive freels´ : freelist -> mem -> mem -> Prop :=
| freelist´_0 : forall M, freels´ nil M M
| freelist´_n : forall b t ls1 ls2 M1 M2 M3 M4, free t b M1 = Some M2 ->
freels´ ls1 M2 M3 ->
freels´ ls2 M3 M4 ->
freels´ (ls1 ++ ( (b, t)) ::ls2) M1 M4.
Lemma get_ptomvallist_less_none :
forall b i n ls M,
(n > 0)%Z ->
ptomvallist (b, (i + n)%Z) ls M ->
MemMod.get M (b, i) = None.
Lemma freeb_join :
forall b i n M1 M12,
freeb M12 b i n = Some M1 ->
exists vl M2, length vl = n /\ ptomvallist (b, i) vl M2 /\ MemMod.join M1 M2 M12.
Lemma freeb_join_rev :
forall b i n vl M1 M2 M12,
MemMod.join M1 M2 M12 ->
ptomvallist (b, i) vl M2 ->
length vl = n ->
freeb M12 b i n = Some M1.
Lemma free_exchange´ :
forall b i ls b´ i´ ls´ M1 M2 M3,
freeb M1 b i ls = Some M2 ->
freeb M2 b´ i´ ls´ = Some M3 ->
exists M, freeb M1 b´ i´ ls´ = Some M /\ freeb M b i ls = Some M3.
Lemma free_exchage :
forall t b M1 t´ b´ M2 M3,
free t b M1 = Some M2 ->
free t´ b´ M2 = Some M3 ->
exists M´, free t´ b´ M1 = Some M´ /\ free t b M´ = Some M3.
Lemma freels_exchange1 :
forall ls1 t b M1 M2 t´ b´ M3 M4,
free t b M1 = Some M2 ->
free t´ b´ M2 = Some M3 ->
freels ls1 M3 M4 ->
exists M´´ M´´´,
free t´ b´ M1 = Some M´´ /\
freels ls1 M´´ M´´´/\
free t b M´´´ = Some M4.
Lemma freels_exchage2 :
forall ls1 t b ls2 M1 M2 M3 M4,
free t b M1 = Some M2 ->
freels ls1 M2 M3 -> freels ls2 M3 M4 ->
exists M´, freels ls1 M1 M´ /\ freels ((b, t) :: ls2) M´ M4.
Lemma freels_merge : forall ls1 ls2 M1 M2 M3, freels ls1 M1 M2 -> freels ls2 M2 M3 ->
freels (ls1 ++ ls2) M1 M3.
Lemma freels_imply_freels´ : forall ls M1 M2, freels´ ls M1 M2 ->
freels ls M1 M2.
Lemma freels´_imply_freels : forall ls M1 M2, freels ls M1 M2 ->
freels´ ls M1 M2.
Lemma freels_split : forall ls1 ls2 M1 M3,
freels (ls1 ++ ls2) M1 M3 ->exists M2, freels ls1 M1 M2 /\ freels ls2 M2 M3.
Lemma freels´_split : forall ls2 ls1 ls M´ M , ls = ls1++ ls2 -> freels´ ls M M´ ->
exists M1, freels´ ls1 M M1 /\ freels´ ls2 M1 M´.
Lemma eqdomenv_nil_enil : forall E , eq_dom_env E nil -> E = empenv.
Definition sub_dom_env (E:env)(d:edom) :=
forall x t, ListSet.set_In (x,t) d ->
exists l, EnvMod.get E x = Some (l, t).
Lemma sub_dom_exists : forall x t d E,
sub_dom_env E (getlenvdom (dcons x t d)) ->
exists l, EnvMod.get E x = Some (l, t).
Lemma envsub_get :
forall E´ E x l t,
EnvMod.sub E´ E -> EnvMod.get E´ x= Some (l, t) ->
EnvMod.get E x = Some (l, t).
Lemma subdomenv_conse:
forall x t E d,
sub_dom_env E (getlenvdom (dcons x t d)) ->
sub_dom_env E (getlenvdom d) /\
exists l, EnvMod.get E x = Some (l,t).
Lemma getaddr_nil_empenv :
forall E, getaddr E = nil -> E = empenv.
Lemma EnvMod_lb_neq :
forall l1 l2 a x v,
EnvMod.lb a (l1 ++ (x, v)::l2) -> identspec.beq x a = false.
Lemma is_orderset_get´_none :
forall l1 l2 x v,
EnvMod.is_orderset (l1 ++ (x, v)::l2) ->
EnvMod.get´ (l1 ++ l2) x = None.
Lemma lb_blt_mid :
forall l1 l2 x a b,
EnvMod.lb x (l1 ++ (a,b)::l2) ->
identspec.blt x a = true.
Lemma lb_sub_r :
forall l1 l2 x,
EnvMod.lb x (l1 ++ l2) ->
EnvMod.lb x l2.
Lemma lb_sub_l :
forall l1 l2 x,
EnvMod.lb x (l1 ++ l2) ->
EnvMod.lb x l1.
Lemma lb_remove_mid :
forall l1 l2 l3 x,
EnvMod.lb x (l1 ++ l2 ++ l3) ->
EnvMod.lb x (l1 ++ l3).
Lemma is_orderset_sub_r :
forall l1 l2,
EnvMod.is_orderset (l1 ++ l2) ->
EnvMod.is_orderset l2.
Lemma is_orderset_sub_l :
forall l1 l2,
EnvMod.is_orderset (l1 ++ l2) ->
EnvMod.is_orderset l1.
Lemma is_orderset_remove_mid :
forall l1 l2 l3,
EnvMod.is_orderset (l1 ++ l2 ++ l3) ->
EnvMod.is_orderset (l1 ++ l3).
Lemma envmod_get´_remove_mid :
forall l1 l2 l3 x,
EnvMod.is_orderset (l1 ++ l2 ++ l3) ->
EnvMod.get´ l2 x = None ->
EnvMod.get´ (l1 ++ l2 ++ l3) x = EnvMod.get´ (l1 ++ l3) x.
Lemma eqdomenv_conse_pre´ :
forall ls x v,
EnvMod.is_orderset ls ->
EnvMod.get´ ls x = Some v ->
exists ls1 ls2 ls´,
ls = ls1 ++ (x,v)::ls2 /\
ls´ = ls1 ++ ls2 /\
EnvMod.is_orderset ls1 /\
EnvMod.is_orderset ls2 /\
EnvMod.is_orderset ls´.
Lemma eqdomenv_conse_pre :
forall E x v,
EnvMod.get E x = Some v ->
exists E1 E2 E´,
EnvMod.join E´ (EnvMod.sig x v) E /\
getaddr E = getaddr E1 ++ v::getaddr E2 /\
getaddr E´ = getaddr E1 ++ getaddr E2.
Lemma ListSet_setIn_in_decllist_true :
forall x t d,
ListSet.set_In (x, t) (getlenvdom d) -> in_decllist x d = true.
Lemma eqdomenv_conse:
forall x t E d,
in_decllist x d = false ->
eq_dom_env E (getlenvdom (dcons x t d)) ->
exists l E1 E2 E´,
getaddr E´ = getaddr E1 ++ getaddr E2 /\
EnvMod.sub E´ E /\
EnvMod.get E x = Some (l,t) /\
getaddr E = (getaddr E1) ++ (l,t) :: getaddr E2 /\
eq_dom_env E´ (getlenvdom d).
Lemma free_locality2´ :
forall M1 M2 M12 b i ls,
MemMod.join M1 M2 M12 ->
ptomvallist (b, i) ls M1 ->
freeb M12 b i (length ls) = Some M2.
Lemma free_locality2 : forall M1 M2 Mc M´ M b t v,
MemMod.join M M1 M2 -> MemMod.join Mc M´ M -> mapstoval (b, 0%Z) t v Mc
-> exists MM, free t b M2 = Some MM /\ MemMod.join M´ M1 MM.
Lemma buidq_intro_e : forall d a G E M isr aux O E´ aop,
EnvMod.sub E´ E ->
Some a = buildq d ->
(G, E, M, isr, aux, O, aop) |= a ->
sub_dom_env E´ (getlenvdom d) ->
(G, E´, M, isr, aux, O, aop) |= a.
Lemma free_intro_aux1 : forall d a G E M isr aux O aop,
Some a = buildq d ->
(G, E, M, isr, aux, O, aop) |= a
-> O = empabst.
Lemma free_intro_aux2: forall d a G E M M1 M2 isr aux O aop,
Some a = buildq d ->
(G, E, M, isr, aux, O, aop) |= a ->
eq_dom_env E (getlenvdom d) ->
MemMod.join M M1 M2 ->
freels´ (getaddr E) M2 M1.
Lemma free_intro: forall a d0 d G E M1 isr aux o1 M2 M3 aop,
Some a = buildq (revlcons d0 d) ->
(G, E, M1, isr, aux, o1, aop) |= a ->
eq_dom_env E (getlenvdom (revlcons d0 d)) ->
MemMod.join M1 M2 M3 ->
o1 = empabst /\ freels (getaddr E) M3 M2.
Lemma getaddr_exist : forall ls, exists al, getaddrlist ls = al.
Lemma get_env_addrlist_ex : forall E, exists al, getaddr E = al.
Lemma nat_exists : forall i j, i < j -> exists k, j = S k.
Lemma sm_nat_exist: forall (i j:nat), (S i < j)%nat -> exists k, j = S (S k).
Lemma beq_nat_false3 : forall i j, beq_nat (S (S (i + j))) (S i) = false.
Open Scope Z_scope.
Lemma Zle_imply_natle : forall n i,0 <= Int.intval i -> Int.intval i < Z.of_nat n -> (Z.to_nat (Int.intval i) < n)%nat.
Lemma beq_nat_false : forall i, beq_nat i (S i) = false.
Lemma beq_nat_false2 : forall i j , beq_nat i (S (S (i+j))) = false.
Lemma OSAbst_join_sub : forall x1 x2 x3 x4 x5,
OSAbstMod.join x1 x2 x3 -> OSAbstMod.join x3 x4 x5 ->
OSAbstMod.sub x1 x5 /\ OSAbstMod.sub x4 x5/\ OSAbstMod.disj x1 x4.
Lemma MemMod_join_sub : forall x1 x2 x3 x4 x5,
MemMod.join x1 x2 x3 -> MemMod.join x3 x4 x5 ->
MemMod.sub x1 x5 /\ MemMod.sub x4 x5/\ MemMod.disj x1 x4.
Lemma eqmem_disj_emp : forall M, MemMod.disj M M -> M = empmem.
Lemma eqabst_disj_emp : forall M, OSAbstMod.disj M M -> M = empabst.
Lemma OSAbst_join_sub´ : forall x1 x2 x3 x4 x5 x6 x7,
OSAbstMod.join x1 x2 x3 -> OSAbstMod.join x4 x3 x5
-> OSAbstMod.join x5 x6 x7 ->
OSAbstMod.sub x1 x7 /\ OSAbstMod.sub x6 x7/\ OSAbstMod.disj x1 x6.
Lemma MemMod_join_sub´ : forall x1 x2 x3 x4 x5 x6 x7,
MemMod.join x1 x2 x3 -> MemMod.join x4 x3 x5 ->
MemMod.join x5 x6 x7 ->
MemMod.sub x1 x7 /\ MemMod.sub x6 x7/\ MemMod.disj x1 x6.
Lemma starinv_prop1: forall j i I,
(starinv_isr I i (S j)) ==>
(starinv_isr I i j) ** (starinv_isr I (S (i+j)) 0)%nat.
Lemma starinv_prop1_rev: forall j i I,
(starinv_isr I i j) ** (starinv_isr I (S (i+j)) 0)%nat ==>
(starinv_isr I i (S j)).
Lemma starinv_prop2: forall i j I,
(starinv_isr I 0 i)%nat **(starinv_isr I (S i) (S j)) ==>
(starinv_isr I 0 (S i))%nat ** (starinv_isr I (S (S i)) j).
Lemma starinv_prop2_rev: forall i j I,
(starinv_isr I 0 (S i))%nat ** (starinv_isr I (S (S i)) j)==>
(starinv_isr I 0 i)%nat **(starinv_isr I (S i) (S j)).
Lemma starinv_isr_prop_intro1 :
forall I i, (starinv_isr I 0 (S i))%nat ==> (starinv_isr I 0 0 )%nat **
(starinv_isr I 1 i)%nat.
Lemma starinv_isr_prop_intro2 : forall I i j, starinv_isr I 0%nat (S j + S i)%nat ==>
starinv_isr I 0%nat (S j) ** starinv_isr I (S (S j)) i.
Lemma starinv_isr_prop_intro3 :
forall I i j, (starinv_isr I 0 (S j + S i))%nat ==> (starinv_isr I 0 j)%nat **
(starinv_isr I (S j) 0)%nat ** (starinv_isr I (S (S j)) i).
Lemma starinv_isr_elim1 : forall j i I,
((starinv_isr I 0 i)%nat ** (starinv_isr I (S i) j))
==> (starinv_isr I 0 (S( i + j)))%nat.
Lemma starinv_isr_prop4 :
forall j i G E M isr aux O aop I,
(G,E,M,isr,aux,O,aop) |= starinv_isr I (S i) j ->
(G,E,M,(isrupd isr i false),aux,O,aop) |= starinv_isr I (S i) j.
Lemma starinv_isr_prop5 :
(forall i j G E M isr aux O aop I,
(G,E,M,isr,aux,O,aop) |= starinv_isr I 0 i ->
(G,E,M,(isrupd isr (S (i + j)) false),aux,O,aop) |= starinv_isr I 0 i)%nat.
Lemma starinv_isr_prop_rev :(forall I i j,
starinv_isr I 0 (S j) ** starinv_isr I (S (S j)) i ==> starinv_isr I 0 (S j + S i))%nat.
Lemma starinv_isr_prop_elim :
forall I i j, (starinv_isr I 0 j)%nat **
(starinv_isr I (S j) 0)%nat ** (starinv_isr I (S (S j)) i) ==> (starinv_isr I 0 (S j + S i))%nat.
Lemma get_env_eq : forall G o M1 o1 M2 o2 o´ M1´ o1´ M2´ o2´,
G = get_genv (get_smem o) ->
joinmem o M1 o1 -> joinmem o1 M2 o2 ->
get_genv (get_smem o2) = get_genv (get_smem o2´) ->
joinmem o´ M1´ o1´ -> joinmem o1´ M2´ o2´ ->
G = get_genv (get_smem o´).
Lemma ltstep_keepG: forall p t C cst o C´ cst´ o´,
ltstep p t C cst o C´ cst´ o´-> get_genv (get_smem o) = get_genv (get_smem o´).
Lemma notabortm_if : forall e s1 s2, notabortm (curs (sif e s1 s2), (kenil, kstop)).
Lemma notabortm_if_v : forall v s1 s2, notabortm (curs(sskip (Some v)),(kenil, kif s1 s2 kstop)).
Lemma OSAbs_disj_eqdom: forall O Os O´, OSAbstMod.disj O Os ->
eqdomO O O´ -> OSAbstMod.disj O´ Os.
Lemma eqdomO_none :
forall O1 O2 x, eqdomO O1 O2 ->
(OSAbstMod.get O1 x = None <-> OSAbstMod.get O2 x = None).
Lemma eqdomO_disj_eqdomO:
forall O O´ Of,
eqdomO O O´ ->
OSAbstMod.disj O Of ->
eqdomO (OSAbstMod.merge O Of) (OSAbstMod.merge O´ Of).
Lemma eqdomO_disj_disj_merge:
forall O O´ Of Os,
eqdomO O O´ ->
OSAbstMod.disj (OSAbstMod.merge O Of) Os ->
OSAbstMod.disj (OSAbstMod.merge O´ Of) Os.
Lemma osabst_disj_join_merge_lpro:
forall Os Of O1 O1´ Os´ O´´,
OSAbstMod.disj O1 Os ->
OSAbstMod.disj Of Os ->
OSAbstMod.join O1 Of O1´ ->
OSAbstMod.disj O1´ Os ->
OSAbstMod.disj O´´ Os´ ->
eqdomO (OSAbstMod.merge O1 Os) (OSAbstMod.merge O´´ Os´) ->
(OSAbstMod.disj Of (OSAbstMod.merge O1 Os)) /\
((OSAbstMod.merge Of (OSAbstMod.merge O1 Os)) = (OSAbstMod.merge O1´ Os)) /\
((OSAbstMod.merge Of (OSAbstMod.merge O´´ Os´)) =
(OSAbstMod.merge (OSAbstMod.merge Of O´´) Os´)) /\
OSAbstMod.disj (OSAbstMod.merge Of O´´) Os´ /\
OSAbstMod.join O´´ Of (OSAbstMod.merge Of O´´).
Lemma joinmem_intro:
forall x4 MM o2´ M Mf,
joinmem x4 MM o2´ ->
MemMod.join M Mf MM ->
exists xc,
joinmem xc Mf o2´ /\ joinmem x4 M xc.
Lemma osabst_disj_eqdom_sym:
forall Of O1 Os x1 x2,
OSAbstMod.disj Of (OSAbstMod.merge O1 Os) ->
eqdomO (OSAbstMod.merge O1 Os) (OSAbstMod.merge x1 x2) ->
OSAbstMod.merge Of (OSAbstMod.merge O1 Os) = OSAbstMod.merge (OSAbstMod.merge O1 Os) Of/\
OSAbstMod.merge Of (OSAbstMod.merge x1 x2) = OSAbstMod.merge (OSAbstMod.merge x1 x2) Of .
Lemma joinmem_prop_in:
forall x3 x5 x4 xc M,
joinmem x3 x5 x4 ->
joinmem x4 M xc -> exists xa, joinmem xa x5 xc /\ joinmem x3 M xa.
Lemma joinmem_get_env_eq :
forall x3 M xa x5 xc Mf o2´ o1 Ms oz MM o2,
joinmem x3 M xa ->
joinmem xa x5 xc ->
joinmem xc Mf o2´ ->
joinmem o1 Ms oz ->
joinmem oz MM o2 ->
get_genv (get_smem o2) = get_genv (get_smem o2´) ->
get_genv (get_smem o1) = get_genv (get_smem x3).
Lemma OSAbstMod_disj_merge_disj:
forall Of O´ Os´ ,
OSAbstMod.disj (OSAbstMod.merge Of O´) Os´ ->
OSAbstMod.disj Of O´ ->
OSAbstMod.disj Of (OSAbstMod.merge O´ Os´).
Lemma absmod_disj_eqdom_merge:
forall O Of O´´ O´,
OSAbstMod.disj O Of ->
OSAbstMod.disj O´´ (OSAbstMod.merge O Of) ->
eqdomO O O´ ->
(OSAbstMod.merge O´´ (OSAbstMod.merge O Of)) =
(OSAbstMod.merge O (OSAbstMod.merge O´´ Of)) /\
(OSAbstMod.merge O´´ (OSAbstMod.merge O´ Of)) =
(OSAbstMod.merge O´ (OSAbstMod.merge O´´ Of)) /\
OSAbstMod.disj O (OSAbstMod.merge O´´ Of) /\
OSAbstMod.disj O´´ (OSAbstMod.merge O´ Of).
Lemma spec_step_eqdomo:
forall O O´ c c´,
spec_step c O c´ O´ -> eqdomO O O´.
Lemma spec_step_disjo:
forall O O´ c c´ Of,
spec_step c O c´ O´ -> OSAbstMod.disj O Of -> OSAbstMod.disj O´ Of.
Lemma hmstestar_disj : forall aop O aop´ O´ Os,
hmstepstar aop O aop´ O´ -> OSAbstMod.disj O Os -> OSAbstMod.disj O´ Os.
Lemma hmstepstar_trans : forall aop O aop´ O´ aop´´ O´´, hmstepstar aop O aop´ O´ -> hmstepstar aop´ O´ aop´´ O´´ ->
hmstepstar aop O aop´´ O´´.
Lemma addstmts_not_eqkstop : forall s ks, AddStmtToKs s ks <> kstop.
Lemma notabort_sseq:forall s1 s2, notabortm (curs (sseq s1 s2), (kenil, kstop)).
Lemma notabort_rete:forall e ,notabortm (nilcont (srete e)).
Lemma store_mapstoval_mono_rev2 :
forall M1 M2 M12 M3 M123 M123´ l t v1 v2,
mapstoval l t v1 M1 ->
MemMod.join M1 M2 M12 ->
MemMod.join M12 M3 M123 ->
store t M123 l v2 = Some M123´ ->
exists M12´, store t M12 l v2 = Some M12´ /\ MemMod.join M12´ M3 M123´.
Lemma assign_loststep_exists : forall p v l t o1 o2 o3 C o3´ Mf Ms aop O P,
loststep p (curs (sskip (Some (Vptr l))),
(kenil,kassignl v t kstop)) o3 C o3´ ->
joinmem o2 Mf o3 ->
joinmem o1 Ms o2 ->
(o1, O, aop) |= P ** (EX v1 : val, (addrval_to_addr l) # t |-> v1) ->
exists o1´ o2´,
loststep p (curs (sskip (Some (Vptr l))), (kenil,kassignl v t kstop)) o1 C o1´/\ joinmem o1´ Ms o2´/\joinmem o2´ Mf o3´.
Lemma assign_loststep_exists´ : forall p v l t o1 o2 o3 C o3´ Mf Ms aop O P v1,
loststep p (curs (sskip (Some (Vptr l))),
(kenil,kassignl v t kstop)) o3 C o3´ ->
joinmem o2 Mf o3 ->
joinmem o1 Ms o2 ->
(o1, O, aop) |= P ** ( (addrval_to_addr l) # t |-> v1) ->
exists o1´ o2´,
loststep p (curs (sskip (Some (Vptr l))), (kenil,kassignl v t kstop)) o1 C o1´/\ joinmem o1´ Ms o2´/\joinmem o2´ Mf o3´.
Lemma evaltype_GE_eq : forall G E M1 M2 e t1 t2, evaltype e (G, E, M1) = Some t1 -> evaltype e (G,E,M2) = Some t2 -> t1 = t2.
Lemma ptomvallist_eqlen_storebytes_exists :
forall b o l1 l2 M,
ptomvallist (b, o) l1 M ->
length l1 = length l2 ->
exists M´, storebytes M (b, o) l2 = Some M´.
Lemma store_exist_join´:
forall l tp x y M1 M2 M3,
mapstoval l tp x M1 ->
MemMod.join M1 M2 M3 ->
exists M´, store tp M3 l y = Some M´.
Lemma store_exist_join:
forall l tp x y M1 M3 M2 M4 M5 M6 M7 M8 M9,
mapstoval l tp x M1 -> MemMod.join M1 M3 M2 -> MemMod.join M4 M2 M5 ->
MemMod.join M5 M6 M7 -> MemMod.join M7 M8 M9 ->
exists M´, store tp M9 l y = Some M´.
Lemma store_asrt_hold : forall G E M M´ e l v isr aux O aop p tp1 tp2 ,
assign_type_match tp1 tp2 ->
(G,E,M, isr,aux,O,aop) |= Rv e@tp2 == v ->
(G,E,M, isr,aux,O,aop) |= p ** (EX v1 : val, l # tp1 |-> v1) ->
store tp1 M l v = Some M´ ->
(G,E,M´, isr,aux,O,aop) |= p ** l # tp1 |-> v.
Lemma store_asrt_hold´ : forall G E M M´ e l v isr aux O aop p tp1 tp2 v1,
assign_type_match tp1 tp2 ->
(G,E,M, isr,aux,O,aop) |= Rv e@tp2 == v ->
(G,E,M, isr,aux,O,aop) |= p ** ( l # tp1 |-> v1) ->
store tp1 M l v = Some M´ ->
(G,E,M´, isr,aux,O,aop) |= p ** l # tp1 |-> v.
Inductive evalexprlist´ : exprlist -> typelist -> vallist -> smem -> Prop :=
| evalexprlist_b : forall m, evalexprlist´ nil nil nil m
| evalexprlist_i : forall e el t tl v vl m, v <> Vundef -> evalval e m = Some v ->
evaltype e m = Some t -> evalexprlist´ el tl vl m ->
evalexprlist´ (cons e el) (cons t tl) (cons v vl) m .
Lemma evalexprlist_imply_evalexprlist´ : forall el tl vl m , evalexprlist el tl vl m ->
evalexprlist´ el tl vl m.
Lemma evalexprlist´_imply_evalexprlist : forall el tl vl m , evalexprlist´ el tl vl m ->
evalexprlist el tl vl m.
Lemma tl_vl_match_rev:forall vl tl,tl_vl_match tl vl =true -> tl_vl_match (rev tl) (rev vl) =true.
Lemma aux_for_tl_vl_match_rev: forall tl vl tl´ vl´, tl_vl_match tl vl =true -> tl_vl_match tl´ vl´ =true -> tl_vl_match (tl++tl´) (vl++vl´)=true.
Qed.
Lemma evalexprlist_imply_eqlen : forall el tl vl m t v,
evalexprlist´ el tl vl m -> length (rev vl ++ v :: nil) =
length (rev tl ++ t :: nil).
Lemma AbsOsEmpAsrt_prop: forall p : asrt,
AbsOsEmpAsrt p ->
forall (ge le : env) (M : mem) (ir : isr) (aux : localst)
(abst : osabst) (op : absop),
(ge, le, M, ir, aux, abst, op) |= p ->
abst = empabst /\
(forall (op´ : absop) (ir´ : isr) (aux´ : localst),
(ge, le, M, ir´, aux´, abst, op´) |= p).
Lemma list_rev_prop : forall (A:Type)(t : A) (tl: list A), t :: tl = rev (rev tl ++ t :: nil).
Lemma store_exists_fcall :
forall tp M0 l v0 M´ M11 M31 M2 Mm1 Mm ge le isr aux O´´ aop
p (vl : vallist) Ms1 Md Mf0 post x O (logicl:list logicvar),
store tp M0 l v0 = Some M´ -> mapstoval l tp x M11 ->
MemMod.join M11 M31 M2 -> MemMod.join Mm1 M2 Mm ->
(ge, le, Mm1, isr, aux, O´´, aop) |= POST [post, rev vl, Some v0, logicl] ->
MemMod.join Mm Ms1 Md ->
MemMod.join Md Mf0 M0 ->
(ge, le, M31, isr, aux, O, aop) |= p ->
exists M11´ M2´ Mm´ Md´,
mapstoval l tp v0 M11´ /\ MemMod.join M11´ M31 M2´/\ MemMod.join Mm1 M2´ Mm´ /\
MemMod.join Mm´ Ms1 Md´ /\ MemMod.join Md´ Mf0 M´.
Lemma evalval_frame_prop: forall o o1 o2 M1 M2 e v, joinmem o M1 o1 -> joinmem o1 M2 o2 ->
evalval e (get_smem o) = Some v ->
evalval e (get_smem o2) = Some v.
Lemma length_tl_3 : forall (tl:typelist), length tl = 3%nat ->
exists t1 t2 t3, tl = t1 :: t2 :: t3 :: nil.
Lemma length_tl_1 : forall (tl:typelist), length tl = 1%nat ->
exists t1, tl = t1 :: nil.
Open Scope nat_scope.
Lemma sat_prop :
forall o O aop isr ie is cs i,
(o,O,aop) |= OS [isr, ie, is, cs] ** ATopis i ** [|i <= INUM|] ->
getisr o = isr /\ getie o = ie /\ getis o = is /\
getcs o = cs /\ gettopis is = i /\ i <= INUM /\ get_mem (get_smem o) = empmem /\ O = empabst.
Lemma inv_simpl : forall G E M isr si cs o aop I,
(G, E, M, isr, (true, si, cs), o, aop)
|= inv_ieon I ->
(G, E, M, isr, (true, si, cs), o, aop)
|= (invlth_isr I 0 INUM).
Lemma starinv_prop : forall I i j, i <= j -> starinv_isr I 0 (S j) ==>
starinv_isr I 0 i ** starinv_isr I (S i) (S j - S i).
Lemma inv_destr :forall i n I, i < n ->
invlth_isr I 0 n ==> ((invlth_isr I 0 i) ** (invlth_isr I (S i) n)).
Lemma inv_isr_prop : forall j i G E M isr ie is cs O aop I ,
(G,E,M,isr,(ie,is,cs),O,aop) |= starinv_isr I i j ->
forall E´ ie´ cs´ aop´,
(G,E´,M,isr,(ie´,is,cs´),O,aop´) |=starinv_isr I i j.
Lemma notabort_expr : forall e, notabortm (cure e, (kenil, kstop)).
Lemma Abs_join_eq : forall Os1 Os, OSAbstMod.join Os1 empabst Os -> Os1 = Os.
Lemma sep_pure : forall o O aop e tp , (o , O,aop) |= EX v : val, Rv e @ tp == v ** [|v <> Vundef|] -> exists v, (o , O,aop) |= Rv e @ tp == v /\ v <> Vundef.