Library inv_prop
Require Import assertion.
Require Import baseTac.
Require Import OSQInvDef.
Require Import include.
Require Import os_code_defs.
Require Import BaseAsrtDef.
Require Import seplog_tactics.
Require Import lemmasforseplog.
Require Import mathsolver.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Lemma sat_sep_conj_elim1 :
forall e e0 M i l O a P Q,
(e, e0, M, i, l, O, a) |= P ** Q ->
exists M1 M2 O1 O2, memory.MemMod.join M1 M2 M /\ OSAbstMod.join O1 O2 O /\
(e, e0, M1, i, l, O1, a) |= P /\
(e, e0, M2, i, l, O2, a) |= Q.
Ltac elim_sep_conj1 H head_H:= let a := fresh in apply sat_sep_conj_elim1 in H; do 4 destruct H; destruct H as [a H]; let b := fresh in destruct H as [b H]; let c := fresh in destruct H as [head_H H].
Ltac mem_join_sub_solver :=
match goal with
| H: memory.MemMod.join ?m _ ?X |- memory.MemMod.sub ?m ?M =>
apply memory.MemMod.join_sub_l in H; apply memory.MemMod.sub_trans with (m2:=X); auto; mem_join_sub_solver
| H: memory.MemMod.join _ ?m ?X |- memory.MemMod.sub ?m ?M =>
apply memory.MemMod.join_sub_r in H; apply memory.MemMod.sub_trans with (m2:=X); auto; mem_join_sub_solver
end.
Lemma MemMod_eq_join_eq :
forall m1 m1´ m2 m2´ M M´,
memory.MemMod.join m1 m2 M ->
memory.MemMod.join m1´ m2´ M´ ->
m1 = m1´ -> m2 = m2´ ->
M = M´.
Ltac mem_eq_solver´ MM :=
eapply MemMod_eq_join_eq; eauto;[
match goal with
| H: forall M : memory.MemMod.map, memory.MemMod.sub ?m1 M -> memory.MemMod.sub ?m2 M -> ?m1 = ?m2 |- ?m1 = ?m2 => apply H with (M:= MM)
end; mem_join_sub_solver | try (mem_eq_solver´ MM)].
Ltac mem_eq_solver MM := try (mem_eq_solver´ MM);
match goal with
| H: forall M : memory.MemMod.map, memory.MemMod.sub ?m1 M -> memory.MemMod.sub ?m2 M -> ?m1 = ?m2 |- ?m1 = ?m2 => apply H with (M:= MM)
end; mem_join_sub_solver.
Lemma osabst_eq_join_eq :
forall m1 m1´ m2 m2´ M M´,
OSAbstMod.join m1 m2 M ->
OSAbstMod.join m1´ m2´ M´ ->
m1 = m1´ -> m2 = m2´ ->
M = M´.
Ltac osabst_join_sub_solver :=
match goal with
| H: OSAbstMod.join ?m _ ?X |- OSAbstMod.sub ?m ?M =>
apply OSAbstMod.join_sub_l in H; apply OSAbstMod.sub_trans with (m2:=X); auto; osabst_join_sub_solver
| H: OSAbstMod.join _ ?m ?X |- OSAbstMod.sub ?m ?M =>
apply OSAbstMod.join_sub_r in H; apply OSAbstMod.sub_trans with (m2:=X); auto; osabst_join_sub_solver
end.
Ltac osabst_eq_solver´ OO :=
eapply osabst_eq_join_eq; eauto;[
match goal with
| H: forall o0 : OSAbstMod.map, OSAbstMod.sub ?m1 o0 -> OSAbstMod.sub ?m2 o0 -> ?m1 = ?m2 |- ?m1 = ?m2 => apply H with (o0:= OO)
end; osabst_join_sub_solver | try (osabst_eq_solver´ OO)].
Ltac osabst_eq_solver OO := try (osabst_eq_solver´ OO);
match goal with
| H: forall o0 : OSAbstMod.map, OSAbstMod.sub ?m1 o0 -> OSAbstMod.sub ?m2 o0 -> ?m1 = ?m2 |- ?m1 = ?m2 => apply H with (o0:=OO)
end; osabst_join_sub_solver.
Ltac mem_sig_eq_solver M :=
match goal with
| |- memory.MemMod.sig ?l1 ?v1 = memory.MemMod.sig ?l2 ?v2 =>
assert(memory.MemMod.sub (memory.MemMod.sig l1 v1) M) as _H1 by mem_join_sub_solver;
assert(memory.MemMod.sub (memory.MemMod.sig l2 v2) M) as _H2 by mem_join_sub_solver;
assert(memory.MemMod.get (memory.MemMod.sig l1 v1) l1 = Some v1) as _H3 by (rewrite memory.MemMod.get_sig_some; auto);
assert(memory.MemMod.get (memory.MemMod.sig l2 v2) l2 = Some v2) as _H4 by (rewrite memory.MemMod.get_sig_some; auto);
apply _H1 in _H3; apply _H2 in _H4;
unfold memory.MemMod.lookup in _H3, _H4; rewrite _H3 in _H4;
remember v1 as X; remember v2 as Y;
inverts _H4; auto
end.
Ltac mem_eq_solver_1 M :=
eapply MemMod_eq_join_eq; eauto; [mem_sig_eq_solver M |try (mem_eq_solver_1 M)]; mem_sig_eq_solver M.
Lemma a_isr_is: inv_isr_prop A_isr_is_prop.
Ltac mytac_1´ :=
match goal with
| H:exists _, _ |- _ => destruct H; mytac_1´
| H:_ /\ _ |- _ => destruct H; mytac_1´
| H:emposabst _ |- _ => unfold emposabst in H; subst; mytac_1´
| H:memory.MemMod.join empmem _ _
|- _ => apply memory.MemMod.join_emp_eq in H; subst; mytac_1´
| H:memory.MemMod.join _ empmem _
|- _ =>
apply memory.MemMod.join_comm in H;
apply memory.MemMod.join_emp_eq in H; subst; mytac_1´
| |- memory.MemMod.join empmem _ _ => apply memory.MemMod.join_emp; mytac_1´
| |- memory.MemMod.join _ empmem _ =>
apply memory.MemMod.join_comm; apply memory.MemMod.join_emp; mytac_1´
| H:memory.EnvMod.join empenv _ _
|- _ => apply memory.EnvMod.join_emp_eq in H; subst; mytac_1´
| H:memory.EnvMod.join _ empenv _
|- _ =>
apply memory.EnvMod.join_comm in H;
apply memory.EnvMod.join_emp_eq in H; subst; mytac_1´
| |- memory.EnvMod.join empenv _ _ => apply memory.EnvMod.join_emp; mytac_1´
| |- memory.EnvMod.join _ empenv _ =>
apply memory.EnvMod.join_comm; apply memory.EnvMod.join_emp; mytac_1´
| H:OSAbstMod.join empabst _ _
|- _ => apply OSAbstMod.join_emp_eq in H; subst; mytac_1´
| H:OSAbstMod.join _ empabst _
|- _ =>
apply OSAbstMod.join_comm in H; apply OSAbstMod.join_emp_eq in H;
subst; mytac_1´
| |- OSAbstMod.join empabst _ _ => apply OSAbstMod.join_emp; mytac_1´
| |- OSAbstMod.join _ empabst _ =>
apply OSAbstMod.join_comm; apply OSAbstMod.join_emp; mytac_1´
| H:memory.MemMod.join ?a ?b ?ab
|- memory.MemMod.join ?b ?a ?ab => apply memory.MemMod.join_comm; auto
| H:memory.EnvMod.join ?a ?b ?ab
|- memory.EnvMod.join ?b ?a ?ab => apply memory.EnvMod.join_comm; auto
| H:OSAbstMod.join ?a ?b ?ab
|- OSAbstMod.join ?b ?a ?ab => apply OSAbstMod.join_comm; auto
| H:memory.MemMod.join ?a ?b ?ab
|- memory.MemMod.disj ?a ?b =>
apply memory.MemMod.join_disj_meq in H; destruct H; auto
| H:memory.EnvMod.join ?a ?b ?ab
|- memory.EnvMod.disj ?a ?b =>
apply memory.EnvMod.join_disj_meq in H; destruct H; auto
| H:OSAbstMod.join ?a ?b ?ab
|- OSAbstMod.disj ?a ?b =>
apply OSAbstMod.join_disj_meq in H; destruct H; auto
| H:memory.MemMod.join ?a ?b ?ab
|- memory.MemMod.disj ?b ?a => apply memory.MemMod.join_comm; mytac_1´
| H:memory.EnvMod.join ?a ?b ?ab
|- memory.EnvMod.disj ?b ?a => apply memory.EnvMod.join_comm; mytac_1´
| H:OSAbstMod.join ?a ?b ?ab
|- OSAbstMod.disj ?b ?a => apply OSAbstMod.join_comm; mytac_1´
| H:memory.MemMod.meq _ _ |- _ => apply memory.MemMod.meq_eq in H; mytac_1´
| H:memory.EnvMod.meq _ _ |- _ => apply memory.EnvMod.meq_eq in H; mytac_1´
| H:OSAbstMod.meq _ _ |- _ => apply OSAbstMod.meq_eq in H; mytac_1´
| H:(_, _) = (_, _) |- _ => inversion H; clear H; mytac_1´
| H:?x = ?x |- _ => clear H; mytac_1´
| |- ?x = ?x => reflexivity
| |- memory.MemMod.join _ ?a ?a => apply memory.MemMod.join_emp; mytac_1´
| |- memory.MemMod.join ?a _ ?a => apply memory.MemMod.join_comm; mytac_1´
| |- memory.EnvMod.join _ ?a ?a => apply memory.EnvMod.join_emp; mytac_1´
| |- memory.EnvMod.join ?a _ ?a => apply memory.EnvMod.join_comm; mytac_1´
| |- OSAbstMod.join _ ?a ?a => apply OSAbstMod.join_emp; mytac_1´
| |- OSAbstMod.join ?a _ ?a => apply OSAbstMod.join_comm; mytac_1´
| |- empmem = _ => reflexivity; mytac_1´
| |- _ = empmem => reflexivity; mytac_1´
| |- empenv = _ => reflexivity; mytac_1´
| |- _ = empenv => reflexivity; mytac_1´
| |- emposabst _ => unfold emposabst; reflexivity; mytac_1´
| |- empabst = _ => reflexivity; mytac_1´
| |- _ = empabst => reflexivity; mytac_1´
| |- empisr = _ => reflexivity; mytac_1´
| |- _ = empisr => reflexivity; mytac_1´
| H:True |- _ => clear H; mytac_1´
| |- True => auto
| _ => try (progress subst; mytac_1´)
end.
Ltac mytac´ := repeat progress mytac_1´.
Ltac simpl_sat H := unfold sat in H; fold sat in H; simpl substmo in H; simpl getmem in H; simpl getabst in H; simpl empst in H.
Lemma ptomvallist_mem_eq :
forall vl l m m´ M,
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
ptomvallist l vl m -> ptomvallist l vl m´ ->
m = m´.
Lemma mapstoval_rule_type_val_match_eq :
forall l t v v´ m m´ M,
rule_type_val_match t v = true -> rule_type_val_match t v´ = true ->
mapstoval l t v m -> mapstoval l t v´ m´ ->
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
v = v´ /\ m = m´.
Lemma isptr_ecbf_sll :
forall s head eventl t next,
s |= ecbf_sll head eventl t next -> isptr head.
Lemma isptr_ecbf_sllseg :
forall s head eventl t next,
s |= ecbf_sllseg head Vnull eventl t next -> isptr head.
Lemma mapstoval_mem_eq :
forall l t v v´ m m´ M,
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
mapstoval l t v m -> mapstoval l t v´ m´ -> m = m´.
Lemma Astruct´_precise :
forall vl vl´ l d M1 M2 o1 o2 e e0 i lo a,
struct_type_vallist_match´ d vl ->
struct_type_vallist_match´ d vl´ ->
(e, e0, M1, i, lo, o1, a) |= Astruct´ l d vl ->
(e, e0, M2, i, lo, o2, a) |= Astruct´ l d vl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma Astruct_precise :
forall vl vl´ l t M1 M2 o1 o2 e e0 i lo a,
struct_type_vallist_match t vl ->
struct_type_vallist_match t vl´ ->
(e, e0, M1, i, lo, o1, a) |= Astruct l t vl ->
(e, e0, M2, i, lo, o2, a) |= Astruct l t vl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma node_precise :
forall vl vl´ head t M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= node head vl t ->
(e, e0, M2, i, l, o2, a) |= node head vl´ t ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma mapstoval_vptr_eq :
forall l a x x´ m m´ M,
mapstoval l (Tptr a) (Vptr x) m -> mapstoval l (Tptr a) (Vptr x´) m´ ->
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
x = x´ /\ m = m´.
Lemma mapstoval_vptr_eq1 :
forall l a x x´ m m´ M,
mapstoval l (Tptr a) (Vptr x) m -> mapstoval l (Tptr a) (Vptr x´) m´ ->
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
x = x´.
Lemma Aarray´_precise :
forall vl vl´ head n t M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= Aarray´ head n t vl ->
(e, e0, M2, i, l, o2, a) |= Aarray´ head n t vl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma Aarray_precise :
forall vl vl´ head t M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= Aarray head t vl ->
(e, e0, M2, i, l, o2, a) |= Aarray head t vl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Open Scope list_scope.
Fixpoint struct_atom_val_eq´ (vl vl´:vallist) (d:decllist) :=
match vl with
| nil =>
match vl´ with
| nil => True
| _ :: _ => False
end
| v1 :: t1 =>
match vl´ with
| nil => False
| v2 :: t2 =>
match d with
| dnil => False
| dcons id (Tstruct _ _) td => struct_atom_val_eq´ t1 t2 td
| dcons id (Tarray _ _) td => struct_atom_val_eq´ t1 t2 td
| dcons id _ td => v1 = v2 /\ struct_atom_val_eq´ t1 t2 td
end
end
end.
Definition struct_atom_val_eq vl vl´ t :=
match t with
| Tstruct id dl => struct_atom_val_eq´ vl vl´ dl
| _ => False
end.
Lemma Astruct´_vl_eq :
forall vl vl´ d l e e0 M1 M2 M i lo o1 o2 a,
struct_type_vallist_match´ d vl -> struct_type_vallist_match´ d vl´ ->
(e, e0, M1, i, lo, o1, a) |= Astruct´ l d vl ->
(e, e0, M2, i, lo, o2, a) |= Astruct´ l d vl´ ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq´ vl vl´ d.
Lemma node_vl_eq :
forall vl vl´ head t M1 M2 M o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= node head vl t ->
(e, e0, M2, i, l, o2, a) |= node head vl´ t ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq vl vl´ t.
Lemma Astruct´_osabst_emp :
forall vl e e0 M i l o a0 lo d,
(e, e0, M, i, lo, o, a0) |= Astruct´ l d vl ->
o = empabst.
Lemma Astruct_osabst_emp :
forall e e0 M i l o a lo t vl,
(e, e0, M, i, lo, o, a) |= Astruct l t vl ->
o = empabst.
Lemma node_osabst_emp :
forall head a t e e0 M i l o a0,
(e, e0, M, i, l, o, a0) |= node head a t ->
o = empabst.
Lemma Aarray´_osabst_emp :
forall vl l n t e e0 M i lo o a0 ,
(e, e0, M, i, lo, o, a0) |= Aarray´ l n t vl ->
o = empabst.
Lemma Aarray_osabst_emp :
forall vl l t e e0 M i lo o a0 ,
(e, e0, M, i, lo, o, a0) |= Aarray l t vl ->
o = empabst.
Lemma ecbf_sllseg_osabst_emp :
forall eventl e e0 M i l o a head tail t next,
(e, e0, M, i, l, o, a) |= ecbf_sllseg head tail eventl t next ->
o = empabst.
Lemma struct_type_vallist_match_os_event : forall v, struct_type_vallist_match os_ucos_h.OS_EVENT v -> exists v1 v2 v3 v4 v5 v6, v = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: nil.
Lemma ecbf_sll_precise :
forall eventl eventl´ head M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= ecbf_sll head eventl os_ucos_h.OS_EVENT V_OSEventListPtr ->
(e, e0, M2, i, l, o2, a) |= ecbf_sll head eventl´ os_ucos_h.OS_EVENT V_OSEventListPtr ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma ecbf_sll_osabst_emp :
forall eventl e e0 M i l o a head t next,
(e, e0, M, i, l, o, a) |= ecbf_sll head eventl t next ->
o = empabst.
Lemma AOSEventFreeList_precise :
forall eventl eventl´ M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= AOSEventFreeList eventl ->
(e, e0, M2, i, l, o2, a) |= AOSEventFreeList eventl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma sllseg_osabst_emp :
forall osql e e0 M i l o a head tail t next,
(e, e0, M, i, l, o, a) |= sllseg head tail osql t next ->
o = empabst.
Lemma sll_osabst_emp :
forall osql e e0 M i l o a head t next,
(e, e0, M, i, l, o, a) |= OSQInvDef.sll head osql t next ->
o = empabst.
Lemma struct_type_vallist_match_os_q : forall v, struct_type_vallist_match os_ucos_h.OS_Q v -> exists v1 v2 v3 v4 v5 v6 v7 v8, v = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: v7 :: v8 :: nil.
Lemma osq_sll_precise :
forall osql osql´ head e e0 M1 M2 i l o1 o2 a,
(e, e0, M1, i, l, o1, a) |= OSQInvDef.sll head osql os_ucos_h.OS_Q V_OSQPtr ->
(e, e0, M2, i, l, o2, a) |= OSQInvDef.sll head osql´ os_ucos_h.OS_Q V_OSQPtr ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma sll_isptr :
forall vl s head t next,
s |= OSQInvDef.sll head vl t next -> isptr head.
Lemma AOSQFreeList_precise :
forall osql osql´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= AOSQFreeList osql ->
(e, e0, M2, i, l, o2, a) |= AOSQFreeList osql´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma qblkf_sll_isptr :
forall qblkl head t next s,
s |= qblkf_sll head qblkl t next -> isptr head.
Lemma qblkf_sllseg_osabst_emp :
forall eventl e e0 M i l o a head tail t next,
(e, e0, M, i, l, o, a) |= qblkf_sllseg head tail eventl t next ->
o = empabst.
Lemma struct_type_vallist_match_os_q_freeblk : forall v, struct_type_vallist_match os_ucos_h.OS_Q_FREEBLK v -> exists v1 v2, v = v1 :: v2 :: nil.
Lemma qblkf_sll_precise :
forall qblkl qblkl´ head e e0 M1 M2 i l o1 o2 a,
(e, e0, M1, i, l, o1, a) |= qblkf_sll head qblkl os_ucos_h.OS_Q_FREEBLK V_nextblk ->
(e, e0, M2, i, l, o2, a) |= qblkf_sll head qblkl´ os_ucos_h.OS_Q_FREEBLK V_nextblk ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma qblkf_sll_osabst_emp :
forall eventl e e0 M i l o a head t next,
(e, e0, M, i, l, o, a) |= qblkf_sll head eventl t next ->
o = empabst.
Lemma AOSQFreeBlk_precise :
forall qblkl qblkl´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= AOSQFreeBlk qblkl ->
(e, e0, M2, i, l, o2, a) |= AOSQFreeBlk qblkl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSEventTbl_precise :
forall l etbl etbl´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSEventTbl l etbl ->
(e, e0, M2, i, lo, o2, a) |= AOSEventTbl l etbl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma evsllseg_isptr :
forall ectrl head msgql s,
s |= evsllseg head Vnull ectrl msgql -> isptr head.
Lemma AOSEvent_precise :
forall l osevent osevent´ etbl etbl´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSEvent l osevent etbl ->
(e, e0, M2, i, lo, o2, a) |= AOSEvent l osevent´ etbl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSEvent_osevent_eq :
forall osevent osevent´ etbl etbl´ l e e0 M1 M2 M i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSEvent l osevent etbl ->
(e, e0, M2, i, lo, o2, a) |= AOSEvent l osevent´ etbl´ ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq osevent osevent´ os_ucos_h.OS_EVENT.
Lemma AOSQCtr_osq_eq :
forall osq osq´ l e e0 M1 M2 M i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSQCtr l osq ->
(e, e0, M2, i, lo, o2, a) |= AOSQCtr l osq´ ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq osq osq´ os_ucos_h.OS_Q.
Lemma AOSQCtr_precise :
forall l osq osq´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSQCtr l osq ->
(e, e0, M2, i, lo, o2, a) |= AOSQCtr l osq´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSQBlk_precise :
forall l osqblk osqblk´ msgtbl msgtbl´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSQBlk l osqblk msgtbl ->
(e, e0, M2, i, lo, o2, a) |= AOSQBlk l osqblk´ msgtbl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSQCtr_osabst_emp :
forall l osq e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AOSQCtr l osq ->
o = empabst.
Lemma AOSQBlk_osabst_emp :
forall l osqblk msgtbl e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AOSQBlk l osqblk msgtbl ->
o = empabst.
Lemma AMsgData_precise :
forall l osq osq´ osqblk osqblk´ msgtbl msgtbl´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AMsgData l osq osqblk msgtbl ->
(e, e0, M2, i, lo, o2, a) |= AMsgData l osq´ osqblk´ msgtbl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Ltac un_eq_event_type_solver :=
match goal with
| H1: Some _ = Some _ , H2: Some _ = Some _ |- _ =>
rewrite H1 in H2; inverts H2
end.
Lemma AEventData_precise :
forall osevent osevent´ d d´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AEventData osevent d ->
(e, e0, M2, i, lo, o2, a) |= AEventData osevent´ d´ ->
struct_atom_val_eq osevent osevent´ os_ucos_h.OS_EVENT ->
struct_type_vallist_match os_ucos_h.OS_EVENT osevent ->
struct_type_vallist_match os_ucos_h.OS_EVENT osevent´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AEventData_osabst_emp :
forall osevent d e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AEventData osevent d ->
o = empabst.
Lemma AOSEvent_osabst_emp :
forall l osevent etbl e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AOSEvent l osevent etbl ->
o = empabst.
Lemma AEventNode_precise :
forall l osevent osevent´ etbl etbl´ d d´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AEventNode l osevent etbl d ->
(e, e0, M2, i, lo, o2, a) |= AEventNode l osevent´ etbl´ d´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AEventNode_osevent_eq :
forall v osevent osevent´ etbl etbl´ d d´ e e0 M1 M2 M i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AEventNode v osevent etbl d ->
(e, e0, M2, i, lo, o2, a) |= AEventNode v osevent´ etbl´ d´ ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq osevent osevent´ os_ucos_h.OS_EVENT.
Lemma AEventNode_osabst_emp :
forall v osevent etbl d e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AEventNode v osevent etbl d ->
o = empabst.
Lemma evsllseg_osabst_emp :
forall ectrl msgql head tail e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= evsllseg head tail ectrl msgql ->
o = empabst.
Lemma evsllseg_precise :
forall ectrl ectrl´ msgql msgql´ head e e0 M1 M2 i l o1 o2 a,
(e, e0, M1, i, l, o1, a) |= evsllseg head Vnull ectrl msgql ->
(e, e0, M2, i, l, o2, a) |= evsllseg head Vnull ectrl´ msgql´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AECBList_precise :
forall ectrl ectrl´ msgql msgql´ ecbls ecbls´ tcbls tcbls´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= AECBList ectrl msgql ecbls tcbls ->
(e, e0, M2, i, l, o2, a) |= AECBList ectrl´ msgql´ ecbls´ tcbls´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSMapTbl_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSMapTbl ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSMapTbl ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSUnMapTbl_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSUnMapTbl ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSUnMapTbl ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSTCBPrioTbl_precise :
forall ptbl ptbl´ rtbl rtbl´ tcbls tcbls´ vhold vhold´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSTCBPrioTbl ptbl rtbl tcbls vhold ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSTCBPrioTbl ptbl´ rtbl´ tcbls´ vhold´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSIntNesting_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSIntNesting ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSIntNesting ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSTCBList_vptr :
forall s p1 p2 tcbl1 tcbcur tcbl2 rtbl ct tcbls,
s |= OSTCBInvDef.AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls ->
(exists x, p1 = Vptr x).
Lemma tcbdllseg_compose:
forall s P h hp t1 tn1 t2 tn2 l1 l2,
s |= OSTCBInvDef.tcbdllseg h hp t1 tn1 l1 ** OSTCBInvDef.tcbdllseg tn1 t1 t2 tn2 l2 ** P->
s |= OSTCBInvDef.tcbdllseg h hp t2 tn2 (l1++l2) ** P.
Lemma struct_type_vallist_match_os_tcb : forall v, struct_type_vallist_match os_ucos_h.OS_TCB v -> exists v1 v2 v3 v4 v5 v6 v7 v8 v9 v10, exists v11, v = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: v7 :: v8 :: v9 :: v10 :: v11 :: nil.
Lemma dllseg_osabst_emp :
forall l head headprev tail tailnext t prev next e e0 M i lo o a0,
(e, e0, M, i, lo, o, a0) |= dllseg head headprev tail tailnext l t prev next -> o = empabst.
Lemma dllseg_ostcb_precise :
forall l l´ head headprev headprev´ tail tail´ e e0 i lo a M1 M2 o1 o2,
(e, e0, M1, i, lo, o1, a) |= dllseg head headprev tail Vnull l os_ucos_h.OS_TCB OSTCBInvDef.V_OSTCBPrev OSTCBInvDef.V_OSTCBNext ->
(e, e0, M2, i, lo, o2, a) |= dllseg head headprev´ tail´ Vnull l´ os_ucos_h.OS_TCB OSTCBInvDef.V_OSTCBPrev OSTCBInvDef.V_OSTCBNext ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma tcbdllseg_precise :
forall l l´ head headprev headprev´ tail tail´ e e0 i lo a M1 M2 o1 o2,
(e, e0, M1, i, lo, o1, a) |= OSTCBInvDef.tcbdllseg head headprev tail Vnull l ->
(e, e0, M2, i, lo, o2, a) |= OSTCBInvDef.tcbdllseg head headprev´ tail´ Vnull l´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma tcbdllseg_osabst_emp :
forall l head headprev tail tailnext e e0 M i lo o a0,
(e, e0, M, i, lo, o, a0) |= OSTCBInvDef.tcbdllseg head headprev tail tailnext l -> o = empabst.
Lemma AOSTCBList_precise :
forall p1 p1´ p2 p2´ tcbl1 tcbl1´ tcbcur tcbcur´ tcbl2 tcbl2´ rtbl rtbl´ ct ct´ tcbls tcbls´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSTCBList p1´ p2´ tcbl1´ (tcbcur´ :: tcbl2´) rtbl´ ct´ tcbls´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma ostcb_sll_precise :
forall lfree lfree´ head e e0 M1 M2 i l o1 o2 a,
(e, e0, M1, i, l, o1, a) |= sll head lfree os_ucos_h.OS_TCB OSTCBInvDef.V_OSTCBNext ->
(e, e0, M2, i, l, o2, a) |= sll head lfree´ os_ucos_h.OS_TCB OSTCBInvDef.V_OSTCBNext ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSTCBFreeList_precise :
forall ptfree ptfree´ lfree lfree´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSTCBFreeList ptfree lfree ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSTCBFreeList ptfree´ lfree´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSRdyTblGrp_precise :
forall rtbl rtbl´ rgrp rgrp´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSRdyTblGrp rtbl rgrp ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSRdyTblGrp rtbl´ rgrp´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSTime_precise :
forall t t´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSTime (Vint32 t) ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSTime (Vint32 t´) ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma Aabsdata_precise :
forall id absdata absdata´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= Aabsdata id absdata ->
(e, e0, M2, i, l, o2, a) |= Aabsdata id absdata´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AGVars_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AGVars ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AGVars ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma A_isr_is_prop_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= A_isr_is_prop ->
(e, e0, M2, i, l, o2, a) |= A_isr_is_prop ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma OSInv_precise : precise OSInv.
Ltac destr_and_inst H v:= let s := fresh v in (destruct H as [s H]; exists s).
Ltac simpl_sat_goal := unfold sat; fold sat; unfold substmo; unfold substaskst; unfold getmem; unfold getabst; unfold get_smem; unfold get_mem.
Lemma is_isr_irrel_Astruct´ :
forall vl l d a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= Astruct´ l d vl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= Astruct´ l d vl.
Lemma is_isr_irrel_Astruct :
forall vl l t a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= Astruct l t vl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= Astruct l t vl.
Lemma is_isr_irrel_node :
forall vl v t a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= node v vl t ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= node v vl t.
Lemma is_isr_irrel_Aarray´ :
forall vl l n t a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= Aarray´ l n t vl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= Aarray´ l n t vl.
Lemma is_isr_irrel_Aarray :
forall vl l t a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= Aarray l t vl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= Aarray l t vl.
Lemma is_isr_irrel_sllseg :
forall l head tail t next a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= sllseg head tail l t next ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= sllseg head tail l t next.
Lemma is_isr_irrel_sll :
forall l head t next a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= OSQInvDef.sll head l t next ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= OSQInvDef.sll head l t next.
Lemma is_isr_AOSEvent :
forall v osevent etbl a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= AOSEvent v osevent etbl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= AOSEvent v osevent etbl.
Lemma is_isr_AEventData :
forall osevent d a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= AEventData osevent d ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= AEventData osevent d.
Lemma is_isr_AEventNode :
forall v osevent etbl d a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= AEventNode v osevent etbl d ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= AEventNode v osevent etbl d.
Lemma is_isr_qblkf_evsllseg :
forall vl head tail ecbls a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= evsllseg head tail vl ecbls ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= evsllseg head tail vl ecbls.
Ltac cancel_pure H := sep split in H; sep split; auto.
Ltac solve_sat H := simpl_sat H; simpl_sat_goal; mytac; do 6 eexists; repeat(split; eauto); eauto.
Lemma is_isr_dllseg :
forall l head headprev tail tailnext t prev next a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= dllseg head headprev tail tailnext l t prev next->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= dllseg head headprev tail tailnext l t prev next.
Lemma is_isr_tcbdllseg :
forall head headprev tail tailnext l a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= OSTCBInvDef.tcbdllseg head headprev tail tailnext l->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= OSTCBInvDef.tcbdllseg head headprev tail tailnext l.
Ltac get_isr_is_prop H := unfold OSInv in H; mytac; do 20 destruct H; sep remember (20::nil)%nat in H; simpl in H; mytac.
Ltac solve_sat_auto :=
match goal with
| H: _ |= ?P ** ?Q |- _ => sep remember (1::nil)%nat in H; solve_sat H; solve_sat_auto
| _ => idtac
end.
Lemma is_isr_qblkf_sllseg :
forall l head tailnext t next a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= qblkf_sllseg head tailnext l t next ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= qblkf_sllseg head tailnext l t next.
Lemma OSInv_isr_is_irrel :
forall a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= OSInv -> isr_is_prop ir´ si´ ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= OSInv.
Lemma GoodInvAsrt_Astruct´ :
forall vl l d, GoodInvAsrt (Astruct´ l d vl).
Lemma GoodInvAsrt_Astruct :
forall vl l t, GoodInvAsrt (Astruct l t vl).
Lemma GoodInvAsrt_Aarray´ :
forall vl l n t, GoodInvAsrt (Aarray´ l n t vl).
Lemma GoodInvAsrt_Aarray :
forall vl l t, GoodInvAsrt (Aarray l t vl).
Lemma GoodInvAsrt_AEventNode : forall v1 v2 v3 v4, GoodInvAsrt (AEventNode v1 v2 v3 v4).
Lemma GoodInvAsrt_dllseg :
forall vl head headprev tail tailnext t prev next,
GoodInvAsrt (dllseg head headprev tail tailnext vl t prev next).
Lemma invprop: inv_prop OSInv.
Lemma goodinv: GoodInvAsrt OSInv.
Definition aemp_isr_is:= Aemp ** A_isr_is_prop.
Lemma goodinv_aemp :
GoodInvAsrt aemp_isr_is.
Lemma invprop_aemp :
inv_prop aemp_isr_is.
Definition atoy_inv´:=(EX i, GV OSIntToyCount@ (Tint32) |-> Vint32 i) .
Definition atoy_inv:= atoy_inv´** A_isr_is_prop.
Lemma atoy_inv´_precise :
forall e e0 M1 M2 i i0 i1 c o1 o2 a,
(e, e0, M1, i, (i0, i1, c), o1, a) |= atoy_inv´ ->
(e, e0, M2, i, (i0, i1, c), o2, a) |= atoy_inv´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o0 : OSAbstMod.map,
OSAbstMod.sub o1 o0 -> OSAbstMod.sub o2 o0 -> o1 = o2).
Lemma goodinv_atoy :
GoodInvAsrt atoy_inv.
Lemma invprop_atoyinv :
inv_prop atoy_inv.
Definition I (n:hid) :=
match n with
| 0 => mkinvasrt goodinv invprop
| 1 => mkinvasrt goodinv_atoy invprop_atoyinv
| _ => mkinvasrt goodinv_aemp invprop_aemp
end.
Require Import baseTac.
Require Import OSQInvDef.
Require Import include.
Require Import os_code_defs.
Require Import BaseAsrtDef.
Require Import seplog_tactics.
Require Import lemmasforseplog.
Require Import mathsolver.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Lemma sat_sep_conj_elim1 :
forall e e0 M i l O a P Q,
(e, e0, M, i, l, O, a) |= P ** Q ->
exists M1 M2 O1 O2, memory.MemMod.join M1 M2 M /\ OSAbstMod.join O1 O2 O /\
(e, e0, M1, i, l, O1, a) |= P /\
(e, e0, M2, i, l, O2, a) |= Q.
Ltac elim_sep_conj1 H head_H:= let a := fresh in apply sat_sep_conj_elim1 in H; do 4 destruct H; destruct H as [a H]; let b := fresh in destruct H as [b H]; let c := fresh in destruct H as [head_H H].
Ltac mem_join_sub_solver :=
match goal with
| H: memory.MemMod.join ?m _ ?X |- memory.MemMod.sub ?m ?M =>
apply memory.MemMod.join_sub_l in H; apply memory.MemMod.sub_trans with (m2:=X); auto; mem_join_sub_solver
| H: memory.MemMod.join _ ?m ?X |- memory.MemMod.sub ?m ?M =>
apply memory.MemMod.join_sub_r in H; apply memory.MemMod.sub_trans with (m2:=X); auto; mem_join_sub_solver
end.
Lemma MemMod_eq_join_eq :
forall m1 m1´ m2 m2´ M M´,
memory.MemMod.join m1 m2 M ->
memory.MemMod.join m1´ m2´ M´ ->
m1 = m1´ -> m2 = m2´ ->
M = M´.
Ltac mem_eq_solver´ MM :=
eapply MemMod_eq_join_eq; eauto;[
match goal with
| H: forall M : memory.MemMod.map, memory.MemMod.sub ?m1 M -> memory.MemMod.sub ?m2 M -> ?m1 = ?m2 |- ?m1 = ?m2 => apply H with (M:= MM)
end; mem_join_sub_solver | try (mem_eq_solver´ MM)].
Ltac mem_eq_solver MM := try (mem_eq_solver´ MM);
match goal with
| H: forall M : memory.MemMod.map, memory.MemMod.sub ?m1 M -> memory.MemMod.sub ?m2 M -> ?m1 = ?m2 |- ?m1 = ?m2 => apply H with (M:= MM)
end; mem_join_sub_solver.
Lemma osabst_eq_join_eq :
forall m1 m1´ m2 m2´ M M´,
OSAbstMod.join m1 m2 M ->
OSAbstMod.join m1´ m2´ M´ ->
m1 = m1´ -> m2 = m2´ ->
M = M´.
Ltac osabst_join_sub_solver :=
match goal with
| H: OSAbstMod.join ?m _ ?X |- OSAbstMod.sub ?m ?M =>
apply OSAbstMod.join_sub_l in H; apply OSAbstMod.sub_trans with (m2:=X); auto; osabst_join_sub_solver
| H: OSAbstMod.join _ ?m ?X |- OSAbstMod.sub ?m ?M =>
apply OSAbstMod.join_sub_r in H; apply OSAbstMod.sub_trans with (m2:=X); auto; osabst_join_sub_solver
end.
Ltac osabst_eq_solver´ OO :=
eapply osabst_eq_join_eq; eauto;[
match goal with
| H: forall o0 : OSAbstMod.map, OSAbstMod.sub ?m1 o0 -> OSAbstMod.sub ?m2 o0 -> ?m1 = ?m2 |- ?m1 = ?m2 => apply H with (o0:= OO)
end; osabst_join_sub_solver | try (osabst_eq_solver´ OO)].
Ltac osabst_eq_solver OO := try (osabst_eq_solver´ OO);
match goal with
| H: forall o0 : OSAbstMod.map, OSAbstMod.sub ?m1 o0 -> OSAbstMod.sub ?m2 o0 -> ?m1 = ?m2 |- ?m1 = ?m2 => apply H with (o0:=OO)
end; osabst_join_sub_solver.
Ltac mem_sig_eq_solver M :=
match goal with
| |- memory.MemMod.sig ?l1 ?v1 = memory.MemMod.sig ?l2 ?v2 =>
assert(memory.MemMod.sub (memory.MemMod.sig l1 v1) M) as _H1 by mem_join_sub_solver;
assert(memory.MemMod.sub (memory.MemMod.sig l2 v2) M) as _H2 by mem_join_sub_solver;
assert(memory.MemMod.get (memory.MemMod.sig l1 v1) l1 = Some v1) as _H3 by (rewrite memory.MemMod.get_sig_some; auto);
assert(memory.MemMod.get (memory.MemMod.sig l2 v2) l2 = Some v2) as _H4 by (rewrite memory.MemMod.get_sig_some; auto);
apply _H1 in _H3; apply _H2 in _H4;
unfold memory.MemMod.lookup in _H3, _H4; rewrite _H3 in _H4;
remember v1 as X; remember v2 as Y;
inverts _H4; auto
end.
Ltac mem_eq_solver_1 M :=
eapply MemMod_eq_join_eq; eauto; [mem_sig_eq_solver M |try (mem_eq_solver_1 M)]; mem_sig_eq_solver M.
Lemma a_isr_is: inv_isr_prop A_isr_is_prop.
Ltac mytac_1´ :=
match goal with
| H:exists _, _ |- _ => destruct H; mytac_1´
| H:_ /\ _ |- _ => destruct H; mytac_1´
| H:emposabst _ |- _ => unfold emposabst in H; subst; mytac_1´
| H:memory.MemMod.join empmem _ _
|- _ => apply memory.MemMod.join_emp_eq in H; subst; mytac_1´
| H:memory.MemMod.join _ empmem _
|- _ =>
apply memory.MemMod.join_comm in H;
apply memory.MemMod.join_emp_eq in H; subst; mytac_1´
| |- memory.MemMod.join empmem _ _ => apply memory.MemMod.join_emp; mytac_1´
| |- memory.MemMod.join _ empmem _ =>
apply memory.MemMod.join_comm; apply memory.MemMod.join_emp; mytac_1´
| H:memory.EnvMod.join empenv _ _
|- _ => apply memory.EnvMod.join_emp_eq in H; subst; mytac_1´
| H:memory.EnvMod.join _ empenv _
|- _ =>
apply memory.EnvMod.join_comm in H;
apply memory.EnvMod.join_emp_eq in H; subst; mytac_1´
| |- memory.EnvMod.join empenv _ _ => apply memory.EnvMod.join_emp; mytac_1´
| |- memory.EnvMod.join _ empenv _ =>
apply memory.EnvMod.join_comm; apply memory.EnvMod.join_emp; mytac_1´
| H:OSAbstMod.join empabst _ _
|- _ => apply OSAbstMod.join_emp_eq in H; subst; mytac_1´
| H:OSAbstMod.join _ empabst _
|- _ =>
apply OSAbstMod.join_comm in H; apply OSAbstMod.join_emp_eq in H;
subst; mytac_1´
| |- OSAbstMod.join empabst _ _ => apply OSAbstMod.join_emp; mytac_1´
| |- OSAbstMod.join _ empabst _ =>
apply OSAbstMod.join_comm; apply OSAbstMod.join_emp; mytac_1´
| H:memory.MemMod.join ?a ?b ?ab
|- memory.MemMod.join ?b ?a ?ab => apply memory.MemMod.join_comm; auto
| H:memory.EnvMod.join ?a ?b ?ab
|- memory.EnvMod.join ?b ?a ?ab => apply memory.EnvMod.join_comm; auto
| H:OSAbstMod.join ?a ?b ?ab
|- OSAbstMod.join ?b ?a ?ab => apply OSAbstMod.join_comm; auto
| H:memory.MemMod.join ?a ?b ?ab
|- memory.MemMod.disj ?a ?b =>
apply memory.MemMod.join_disj_meq in H; destruct H; auto
| H:memory.EnvMod.join ?a ?b ?ab
|- memory.EnvMod.disj ?a ?b =>
apply memory.EnvMod.join_disj_meq in H; destruct H; auto
| H:OSAbstMod.join ?a ?b ?ab
|- OSAbstMod.disj ?a ?b =>
apply OSAbstMod.join_disj_meq in H; destruct H; auto
| H:memory.MemMod.join ?a ?b ?ab
|- memory.MemMod.disj ?b ?a => apply memory.MemMod.join_comm; mytac_1´
| H:memory.EnvMod.join ?a ?b ?ab
|- memory.EnvMod.disj ?b ?a => apply memory.EnvMod.join_comm; mytac_1´
| H:OSAbstMod.join ?a ?b ?ab
|- OSAbstMod.disj ?b ?a => apply OSAbstMod.join_comm; mytac_1´
| H:memory.MemMod.meq _ _ |- _ => apply memory.MemMod.meq_eq in H; mytac_1´
| H:memory.EnvMod.meq _ _ |- _ => apply memory.EnvMod.meq_eq in H; mytac_1´
| H:OSAbstMod.meq _ _ |- _ => apply OSAbstMod.meq_eq in H; mytac_1´
| H:(_, _) = (_, _) |- _ => inversion H; clear H; mytac_1´
| H:?x = ?x |- _ => clear H; mytac_1´
| |- ?x = ?x => reflexivity
| |- memory.MemMod.join _ ?a ?a => apply memory.MemMod.join_emp; mytac_1´
| |- memory.MemMod.join ?a _ ?a => apply memory.MemMod.join_comm; mytac_1´
| |- memory.EnvMod.join _ ?a ?a => apply memory.EnvMod.join_emp; mytac_1´
| |- memory.EnvMod.join ?a _ ?a => apply memory.EnvMod.join_comm; mytac_1´
| |- OSAbstMod.join _ ?a ?a => apply OSAbstMod.join_emp; mytac_1´
| |- OSAbstMod.join ?a _ ?a => apply OSAbstMod.join_comm; mytac_1´
| |- empmem = _ => reflexivity; mytac_1´
| |- _ = empmem => reflexivity; mytac_1´
| |- empenv = _ => reflexivity; mytac_1´
| |- _ = empenv => reflexivity; mytac_1´
| |- emposabst _ => unfold emposabst; reflexivity; mytac_1´
| |- empabst = _ => reflexivity; mytac_1´
| |- _ = empabst => reflexivity; mytac_1´
| |- empisr = _ => reflexivity; mytac_1´
| |- _ = empisr => reflexivity; mytac_1´
| H:True |- _ => clear H; mytac_1´
| |- True => auto
| _ => try (progress subst; mytac_1´)
end.
Ltac mytac´ := repeat progress mytac_1´.
Ltac simpl_sat H := unfold sat in H; fold sat in H; simpl substmo in H; simpl getmem in H; simpl getabst in H; simpl empst in H.
Lemma ptomvallist_mem_eq :
forall vl l m m´ M,
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
ptomvallist l vl m -> ptomvallist l vl m´ ->
m = m´.
Lemma mapstoval_rule_type_val_match_eq :
forall l t v v´ m m´ M,
rule_type_val_match t v = true -> rule_type_val_match t v´ = true ->
mapstoval l t v m -> mapstoval l t v´ m´ ->
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
v = v´ /\ m = m´.
Lemma isptr_ecbf_sll :
forall s head eventl t next,
s |= ecbf_sll head eventl t next -> isptr head.
Lemma isptr_ecbf_sllseg :
forall s head eventl t next,
s |= ecbf_sllseg head Vnull eventl t next -> isptr head.
Lemma mapstoval_mem_eq :
forall l t v v´ m m´ M,
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
mapstoval l t v m -> mapstoval l t v´ m´ -> m = m´.
Lemma Astruct´_precise :
forall vl vl´ l d M1 M2 o1 o2 e e0 i lo a,
struct_type_vallist_match´ d vl ->
struct_type_vallist_match´ d vl´ ->
(e, e0, M1, i, lo, o1, a) |= Astruct´ l d vl ->
(e, e0, M2, i, lo, o2, a) |= Astruct´ l d vl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma Astruct_precise :
forall vl vl´ l t M1 M2 o1 o2 e e0 i lo a,
struct_type_vallist_match t vl ->
struct_type_vallist_match t vl´ ->
(e, e0, M1, i, lo, o1, a) |= Astruct l t vl ->
(e, e0, M2, i, lo, o2, a) |= Astruct l t vl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma node_precise :
forall vl vl´ head t M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= node head vl t ->
(e, e0, M2, i, l, o2, a) |= node head vl´ t ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma mapstoval_vptr_eq :
forall l a x x´ m m´ M,
mapstoval l (Tptr a) (Vptr x) m -> mapstoval l (Tptr a) (Vptr x´) m´ ->
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
x = x´ /\ m = m´.
Lemma mapstoval_vptr_eq1 :
forall l a x x´ m m´ M,
mapstoval l (Tptr a) (Vptr x) m -> mapstoval l (Tptr a) (Vptr x´) m´ ->
memory.MemMod.sub m M -> memory.MemMod.sub m´ M ->
x = x´.
Lemma Aarray´_precise :
forall vl vl´ head n t M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= Aarray´ head n t vl ->
(e, e0, M2, i, l, o2, a) |= Aarray´ head n t vl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma Aarray_precise :
forall vl vl´ head t M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= Aarray head t vl ->
(e, e0, M2, i, l, o2, a) |= Aarray head t vl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Open Scope list_scope.
Fixpoint struct_atom_val_eq´ (vl vl´:vallist) (d:decllist) :=
match vl with
| nil =>
match vl´ with
| nil => True
| _ :: _ => False
end
| v1 :: t1 =>
match vl´ with
| nil => False
| v2 :: t2 =>
match d with
| dnil => False
| dcons id (Tstruct _ _) td => struct_atom_val_eq´ t1 t2 td
| dcons id (Tarray _ _) td => struct_atom_val_eq´ t1 t2 td
| dcons id _ td => v1 = v2 /\ struct_atom_val_eq´ t1 t2 td
end
end
end.
Definition struct_atom_val_eq vl vl´ t :=
match t with
| Tstruct id dl => struct_atom_val_eq´ vl vl´ dl
| _ => False
end.
Lemma Astruct´_vl_eq :
forall vl vl´ d l e e0 M1 M2 M i lo o1 o2 a,
struct_type_vallist_match´ d vl -> struct_type_vallist_match´ d vl´ ->
(e, e0, M1, i, lo, o1, a) |= Astruct´ l d vl ->
(e, e0, M2, i, lo, o2, a) |= Astruct´ l d vl´ ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq´ vl vl´ d.
Lemma node_vl_eq :
forall vl vl´ head t M1 M2 M o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= node head vl t ->
(e, e0, M2, i, l, o2, a) |= node head vl´ t ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq vl vl´ t.
Lemma Astruct´_osabst_emp :
forall vl e e0 M i l o a0 lo d,
(e, e0, M, i, lo, o, a0) |= Astruct´ l d vl ->
o = empabst.
Lemma Astruct_osabst_emp :
forall e e0 M i l o a lo t vl,
(e, e0, M, i, lo, o, a) |= Astruct l t vl ->
o = empabst.
Lemma node_osabst_emp :
forall head a t e e0 M i l o a0,
(e, e0, M, i, l, o, a0) |= node head a t ->
o = empabst.
Lemma Aarray´_osabst_emp :
forall vl l n t e e0 M i lo o a0 ,
(e, e0, M, i, lo, o, a0) |= Aarray´ l n t vl ->
o = empabst.
Lemma Aarray_osabst_emp :
forall vl l t e e0 M i lo o a0 ,
(e, e0, M, i, lo, o, a0) |= Aarray l t vl ->
o = empabst.
Lemma ecbf_sllseg_osabst_emp :
forall eventl e e0 M i l o a head tail t next,
(e, e0, M, i, l, o, a) |= ecbf_sllseg head tail eventl t next ->
o = empabst.
Lemma struct_type_vallist_match_os_event : forall v, struct_type_vallist_match os_ucos_h.OS_EVENT v -> exists v1 v2 v3 v4 v5 v6, v = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: nil.
Lemma ecbf_sll_precise :
forall eventl eventl´ head M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= ecbf_sll head eventl os_ucos_h.OS_EVENT V_OSEventListPtr ->
(e, e0, M2, i, l, o2, a) |= ecbf_sll head eventl´ os_ucos_h.OS_EVENT V_OSEventListPtr ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma ecbf_sll_osabst_emp :
forall eventl e e0 M i l o a head t next,
(e, e0, M, i, l, o, a) |= ecbf_sll head eventl t next ->
o = empabst.
Lemma AOSEventFreeList_precise :
forall eventl eventl´ M1 M2 o1 o2 e e0 i l a,
(e, e0, M1, i, l, o1, a) |= AOSEventFreeList eventl ->
(e, e0, M2, i, l, o2, a) |= AOSEventFreeList eventl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma sllseg_osabst_emp :
forall osql e e0 M i l o a head tail t next,
(e, e0, M, i, l, o, a) |= sllseg head tail osql t next ->
o = empabst.
Lemma sll_osabst_emp :
forall osql e e0 M i l o a head t next,
(e, e0, M, i, l, o, a) |= OSQInvDef.sll head osql t next ->
o = empabst.
Lemma struct_type_vallist_match_os_q : forall v, struct_type_vallist_match os_ucos_h.OS_Q v -> exists v1 v2 v3 v4 v5 v6 v7 v8, v = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: v7 :: v8 :: nil.
Lemma osq_sll_precise :
forall osql osql´ head e e0 M1 M2 i l o1 o2 a,
(e, e0, M1, i, l, o1, a) |= OSQInvDef.sll head osql os_ucos_h.OS_Q V_OSQPtr ->
(e, e0, M2, i, l, o2, a) |= OSQInvDef.sll head osql´ os_ucos_h.OS_Q V_OSQPtr ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma sll_isptr :
forall vl s head t next,
s |= OSQInvDef.sll head vl t next -> isptr head.
Lemma AOSQFreeList_precise :
forall osql osql´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= AOSQFreeList osql ->
(e, e0, M2, i, l, o2, a) |= AOSQFreeList osql´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma qblkf_sll_isptr :
forall qblkl head t next s,
s |= qblkf_sll head qblkl t next -> isptr head.
Lemma qblkf_sllseg_osabst_emp :
forall eventl e e0 M i l o a head tail t next,
(e, e0, M, i, l, o, a) |= qblkf_sllseg head tail eventl t next ->
o = empabst.
Lemma struct_type_vallist_match_os_q_freeblk : forall v, struct_type_vallist_match os_ucos_h.OS_Q_FREEBLK v -> exists v1 v2, v = v1 :: v2 :: nil.
Lemma qblkf_sll_precise :
forall qblkl qblkl´ head e e0 M1 M2 i l o1 o2 a,
(e, e0, M1, i, l, o1, a) |= qblkf_sll head qblkl os_ucos_h.OS_Q_FREEBLK V_nextblk ->
(e, e0, M2, i, l, o2, a) |= qblkf_sll head qblkl´ os_ucos_h.OS_Q_FREEBLK V_nextblk ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma qblkf_sll_osabst_emp :
forall eventl e e0 M i l o a head t next,
(e, e0, M, i, l, o, a) |= qblkf_sll head eventl t next ->
o = empabst.
Lemma AOSQFreeBlk_precise :
forall qblkl qblkl´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= AOSQFreeBlk qblkl ->
(e, e0, M2, i, l, o2, a) |= AOSQFreeBlk qblkl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSEventTbl_precise :
forall l etbl etbl´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSEventTbl l etbl ->
(e, e0, M2, i, lo, o2, a) |= AOSEventTbl l etbl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma evsllseg_isptr :
forall ectrl head msgql s,
s |= evsllseg head Vnull ectrl msgql -> isptr head.
Lemma AOSEvent_precise :
forall l osevent osevent´ etbl etbl´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSEvent l osevent etbl ->
(e, e0, M2, i, lo, o2, a) |= AOSEvent l osevent´ etbl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSEvent_osevent_eq :
forall osevent osevent´ etbl etbl´ l e e0 M1 M2 M i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSEvent l osevent etbl ->
(e, e0, M2, i, lo, o2, a) |= AOSEvent l osevent´ etbl´ ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq osevent osevent´ os_ucos_h.OS_EVENT.
Lemma AOSQCtr_osq_eq :
forall osq osq´ l e e0 M1 M2 M i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSQCtr l osq ->
(e, e0, M2, i, lo, o2, a) |= AOSQCtr l osq´ ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq osq osq´ os_ucos_h.OS_Q.
Lemma AOSQCtr_precise :
forall l osq osq´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSQCtr l osq ->
(e, e0, M2, i, lo, o2, a) |= AOSQCtr l osq´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSQBlk_precise :
forall l osqblk osqblk´ msgtbl msgtbl´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AOSQBlk l osqblk msgtbl ->
(e, e0, M2, i, lo, o2, a) |= AOSQBlk l osqblk´ msgtbl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSQCtr_osabst_emp :
forall l osq e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AOSQCtr l osq ->
o = empabst.
Lemma AOSQBlk_osabst_emp :
forall l osqblk msgtbl e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AOSQBlk l osqblk msgtbl ->
o = empabst.
Lemma AMsgData_precise :
forall l osq osq´ osqblk osqblk´ msgtbl msgtbl´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AMsgData l osq osqblk msgtbl ->
(e, e0, M2, i, lo, o2, a) |= AMsgData l osq´ osqblk´ msgtbl´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Ltac un_eq_event_type_solver :=
match goal with
| H1: Some _ = Some _ , H2: Some _ = Some _ |- _ =>
rewrite H1 in H2; inverts H2
end.
Lemma AEventData_precise :
forall osevent osevent´ d d´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AEventData osevent d ->
(e, e0, M2, i, lo, o2, a) |= AEventData osevent´ d´ ->
struct_atom_val_eq osevent osevent´ os_ucos_h.OS_EVENT ->
struct_type_vallist_match os_ucos_h.OS_EVENT osevent ->
struct_type_vallist_match os_ucos_h.OS_EVENT osevent´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AEventData_osabst_emp :
forall osevent d e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AEventData osevent d ->
o = empabst.
Lemma AOSEvent_osabst_emp :
forall l osevent etbl e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AOSEvent l osevent etbl ->
o = empabst.
Lemma AEventNode_precise :
forall l osevent osevent´ etbl etbl´ d d´ e e0 M1 M2 i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AEventNode l osevent etbl d ->
(e, e0, M2, i, lo, o2, a) |= AEventNode l osevent´ etbl´ d´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AEventNode_osevent_eq :
forall v osevent osevent´ etbl etbl´ d d´ e e0 M1 M2 M i lo o1 o2 a,
(e, e0, M1, i, lo, o1, a) |= AEventNode v osevent etbl d ->
(e, e0, M2, i, lo, o2, a) |= AEventNode v osevent´ etbl´ d´ ->
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M ->
struct_atom_val_eq osevent osevent´ os_ucos_h.OS_EVENT.
Lemma AEventNode_osabst_emp :
forall v osevent etbl d e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= AEventNode v osevent etbl d ->
o = empabst.
Lemma evsllseg_osabst_emp :
forall ectrl msgql head tail e e0 M i lo o a,
(e, e0, M, i, lo, o, a) |= evsllseg head tail ectrl msgql ->
o = empabst.
Lemma evsllseg_precise :
forall ectrl ectrl´ msgql msgql´ head e e0 M1 M2 i l o1 o2 a,
(e, e0, M1, i, l, o1, a) |= evsllseg head Vnull ectrl msgql ->
(e, e0, M2, i, l, o2, a) |= evsllseg head Vnull ectrl´ msgql´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AECBList_precise :
forall ectrl ectrl´ msgql msgql´ ecbls ecbls´ tcbls tcbls´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= AECBList ectrl msgql ecbls tcbls ->
(e, e0, M2, i, l, o2, a) |= AECBList ectrl´ msgql´ ecbls´ tcbls´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSMapTbl_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSMapTbl ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSMapTbl ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSUnMapTbl_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSUnMapTbl ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSUnMapTbl ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSTCBPrioTbl_precise :
forall ptbl ptbl´ rtbl rtbl´ tcbls tcbls´ vhold vhold´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSTCBPrioTbl ptbl rtbl tcbls vhold ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSTCBPrioTbl ptbl´ rtbl´ tcbls´ vhold´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSIntNesting_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSIntNesting ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSIntNesting ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSTCBList_vptr :
forall s p1 p2 tcbl1 tcbcur tcbl2 rtbl ct tcbls,
s |= OSTCBInvDef.AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls ->
(exists x, p1 = Vptr x).
Lemma tcbdllseg_compose:
forall s P h hp t1 tn1 t2 tn2 l1 l2,
s |= OSTCBInvDef.tcbdllseg h hp t1 tn1 l1 ** OSTCBInvDef.tcbdllseg tn1 t1 t2 tn2 l2 ** P->
s |= OSTCBInvDef.tcbdllseg h hp t2 tn2 (l1++l2) ** P.
Lemma struct_type_vallist_match_os_tcb : forall v, struct_type_vallist_match os_ucos_h.OS_TCB v -> exists v1 v2 v3 v4 v5 v6 v7 v8 v9 v10, exists v11, v = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: v7 :: v8 :: v9 :: v10 :: v11 :: nil.
Lemma dllseg_osabst_emp :
forall l head headprev tail tailnext t prev next e e0 M i lo o a0,
(e, e0, M, i, lo, o, a0) |= dllseg head headprev tail tailnext l t prev next -> o = empabst.
Lemma dllseg_ostcb_precise :
forall l l´ head headprev headprev´ tail tail´ e e0 i lo a M1 M2 o1 o2,
(e, e0, M1, i, lo, o1, a) |= dllseg head headprev tail Vnull l os_ucos_h.OS_TCB OSTCBInvDef.V_OSTCBPrev OSTCBInvDef.V_OSTCBNext ->
(e, e0, M2, i, lo, o2, a) |= dllseg head headprev´ tail´ Vnull l´ os_ucos_h.OS_TCB OSTCBInvDef.V_OSTCBPrev OSTCBInvDef.V_OSTCBNext ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma tcbdllseg_precise :
forall l l´ head headprev headprev´ tail tail´ e e0 i lo a M1 M2 o1 o2,
(e, e0, M1, i, lo, o1, a) |= OSTCBInvDef.tcbdllseg head headprev tail Vnull l ->
(e, e0, M2, i, lo, o2, a) |= OSTCBInvDef.tcbdllseg head headprev´ tail´ Vnull l´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma tcbdllseg_osabst_emp :
forall l head headprev tail tailnext e e0 M i lo o a0,
(e, e0, M, i, lo, o, a0) |= OSTCBInvDef.tcbdllseg head headprev tail tailnext l -> o = empabst.
Lemma AOSTCBList_precise :
forall p1 p1´ p2 p2´ tcbl1 tcbl1´ tcbcur tcbcur´ tcbl2 tcbl2´ rtbl rtbl´ ct ct´ tcbls tcbls´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSTCBList p1´ p2´ tcbl1´ (tcbcur´ :: tcbl2´) rtbl´ ct´ tcbls´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma ostcb_sll_precise :
forall lfree lfree´ head e e0 M1 M2 i l o1 o2 a,
(e, e0, M1, i, l, o1, a) |= sll head lfree os_ucos_h.OS_TCB OSTCBInvDef.V_OSTCBNext ->
(e, e0, M2, i, l, o2, a) |= sll head lfree´ os_ucos_h.OS_TCB OSTCBInvDef.V_OSTCBNext ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSTCBFreeList_precise :
forall ptfree ptfree´ lfree lfree´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSTCBFreeList ptfree lfree ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSTCBFreeList ptfree´ lfree´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSRdyTblGrp_precise :
forall rtbl rtbl´ rgrp rgrp´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSRdyTblGrp rtbl rgrp ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSRdyTblGrp rtbl´ rgrp´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AOSTime_precise :
forall t t´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AOSTime (Vint32 t) ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AOSTime (Vint32 t´) ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma Aabsdata_precise :
forall id absdata absdata´ e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= Aabsdata id absdata ->
(e, e0, M2, i, l, o2, a) |= Aabsdata id absdata´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma AGVars_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= OSTCBInvDef.AGVars ->
(e, e0, M2, i, l, o2, a) |= OSTCBInvDef.AGVars ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma A_isr_is_prop_precise :
forall e e0 i l a M1 M2 o1 o2,
(e, e0, M1, i, l, o1, a) |= A_isr_is_prop ->
(e, e0, M2, i, l, o2, a) |= A_isr_is_prop ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o : OSAbstMod.map,
OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Lemma OSInv_precise : precise OSInv.
Ltac destr_and_inst H v:= let s := fresh v in (destruct H as [s H]; exists s).
Ltac simpl_sat_goal := unfold sat; fold sat; unfold substmo; unfold substaskst; unfold getmem; unfold getabst; unfold get_smem; unfold get_mem.
Lemma is_isr_irrel_Astruct´ :
forall vl l d a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= Astruct´ l d vl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= Astruct´ l d vl.
Lemma is_isr_irrel_Astruct :
forall vl l t a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= Astruct l t vl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= Astruct l t vl.
Lemma is_isr_irrel_node :
forall vl v t a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= node v vl t ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= node v vl t.
Lemma is_isr_irrel_Aarray´ :
forall vl l n t a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= Aarray´ l n t vl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= Aarray´ l n t vl.
Lemma is_isr_irrel_Aarray :
forall vl l t a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= Aarray l t vl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= Aarray l t vl.
Lemma is_isr_irrel_sllseg :
forall l head tail t next a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= sllseg head tail l t next ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= sllseg head tail l t next.
Lemma is_isr_irrel_sll :
forall l head t next a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= OSQInvDef.sll head l t next ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= OSQInvDef.sll head l t next.
Lemma is_isr_AOSEvent :
forall v osevent etbl a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= AOSEvent v osevent etbl ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= AOSEvent v osevent etbl.
Lemma is_isr_AEventData :
forall osevent d a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= AEventData osevent d ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= AEventData osevent d.
Lemma is_isr_AEventNode :
forall v osevent etbl d a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= AEventNode v osevent etbl d ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= AEventNode v osevent etbl d.
Lemma is_isr_qblkf_evsllseg :
forall vl head tail ecbls a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= evsllseg head tail vl ecbls ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= evsllseg head tail vl ecbls.
Ltac cancel_pure H := sep split in H; sep split; auto.
Ltac solve_sat H := simpl_sat H; simpl_sat_goal; mytac; do 6 eexists; repeat(split; eauto); eauto.
Lemma is_isr_dllseg :
forall l head headprev tail tailnext t prev next a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= dllseg head headprev tail tailnext l t prev next->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= dllseg head headprev tail tailnext l t prev next.
Lemma is_isr_tcbdllseg :
forall head headprev tail tailnext l a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= OSTCBInvDef.tcbdllseg head headprev tail tailnext l->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= OSTCBInvDef.tcbdllseg head headprev tail tailnext l.
Ltac get_isr_is_prop H := unfold OSInv in H; mytac; do 20 destruct H; sep remember (20::nil)%nat in H; simpl in H; mytac.
Ltac solve_sat_auto :=
match goal with
| H: _ |= ?P ** ?Q |- _ => sep remember (1::nil)%nat in H; solve_sat H; solve_sat_auto
| _ => idtac
end.
Lemma is_isr_qblkf_sllseg :
forall l head tailnext t next a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= qblkf_sllseg head tailnext l t next ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= qblkf_sllseg head tailnext l t next.
Lemma OSInv_isr_is_irrel :
forall a b c ir ir´ ie0 si si´ cs0 x aop,
(a, b, c, ir, (ie0, si, cs0), x, aop) |= OSInv -> isr_is_prop ir´ si´ ->
(a, b, c, ir´, (ie0, si´, cs0), x, aop) |= OSInv.
Lemma GoodInvAsrt_Astruct´ :
forall vl l d, GoodInvAsrt (Astruct´ l d vl).
Lemma GoodInvAsrt_Astruct :
forall vl l t, GoodInvAsrt (Astruct l t vl).
Lemma GoodInvAsrt_Aarray´ :
forall vl l n t, GoodInvAsrt (Aarray´ l n t vl).
Lemma GoodInvAsrt_Aarray :
forall vl l t, GoodInvAsrt (Aarray l t vl).
Lemma GoodInvAsrt_AEventNode : forall v1 v2 v3 v4, GoodInvAsrt (AEventNode v1 v2 v3 v4).
Lemma GoodInvAsrt_dllseg :
forall vl head headprev tail tailnext t prev next,
GoodInvAsrt (dllseg head headprev tail tailnext vl t prev next).
Lemma invprop: inv_prop OSInv.
Lemma goodinv: GoodInvAsrt OSInv.
Definition aemp_isr_is:= Aemp ** A_isr_is_prop.
Lemma goodinv_aemp :
GoodInvAsrt aemp_isr_is.
Lemma invprop_aemp :
inv_prop aemp_isr_is.
Definition atoy_inv´:=(EX i, GV OSIntToyCount@ (Tint32) |-> Vint32 i) .
Definition atoy_inv:= atoy_inv´** A_isr_is_prop.
Lemma atoy_inv´_precise :
forall e e0 M1 M2 i i0 i1 c o1 o2 a,
(e, e0, M1, i, (i0, i1, c), o1, a) |= atoy_inv´ ->
(e, e0, M2, i, (i0, i1, c), o2, a) |= atoy_inv´ ->
(forall M : memory.MemMod.map,
memory.MemMod.sub M1 M -> memory.MemMod.sub M2 M -> M1 = M2) /\
(forall o0 : OSAbstMod.map,
OSAbstMod.sub o1 o0 -> OSAbstMod.sub o2 o0 -> o1 = o2).
Lemma goodinv_atoy :
GoodInvAsrt atoy_inv.
Lemma invprop_atoyinv :
inv_prop atoy_inv.
Definition I (n:hid) :=
match n with
| 0 => mkinvasrt goodinv invprop
| 1 => mkinvasrt goodinv_atoy invprop_atoyinv
| _ => mkinvasrt goodinv_aemp invprop_aemp
end.