Library OSEventRemovePure
Require Import ucert.
Require Import mathlib.
Require Export oscore_common.
Fixpoint not_in {A B:Type} (e:B) (l:list A) (f:A -> option B) :=
match l with
| nil => True
| h :: t => (forall e´, f h = Some e´ -> e´ <> e) /\ not_in e t f
end.
Fixpoint distinct´ {A B:Type} (l:list A) (f:A -> option B) :=
match l with
| nil => True
| h :: t => (forall e, f h = Some e -> not_in e t f) /\ distinct´ t f
end.
Definition distinct {A B:Type} (head:B) (l:list A) f := distinct´ l f /\ not_in head l f.
Fixpoint get_last {A B:Type} (l:list A) (f: A->option B) :=
match l with
| nil => None
| e::nil => f e
| h::t => get_last t f
end.
Definition ecb_get_next_ptr (ecb: EventCtr) := let (a, b) := ecb in V_OSEventListPtr a.
Definition ecbls_ptr_distinct (ecbls: list EventCtr):= distinct´ ecbls ecb_get_next_ptr.
Lemma evsllseg_distinct :
forall l1 l2 head s P,
s |= evsllseg head Vnull l1 l2 ** P ->
ecbls_ptr_distinct l1.
Lemma evsllseg_not_in_vnull :
forall l1 l2 head s P,
s |= evsllseg head Vnull l1 l2 ** P ->
not_in head l1 ecb_get_next_ptr.
Lemma AEventNode_vnull_false :
forall s v v0 e0 P,
s |= AEventNode Vnull v v0 e0 ** P ->
False.
Qed.
Lemma evsllseg_not_in_vnull´ :
forall l1 l2 head s,
s |= evsllseg head Vnull l1 l2 ->
not_in head l1 ecb_get_next_ptr.
Qed.
Lemma evsllseg_distinct´ :
forall l1 l2 head s,
s |= evsllseg head Vnull l1 l2 ->
ecbls_ptr_distinct l1.
Lemma evsllseg_ptr_dup_false : forall l1 l2 x a1 a2 s lx ,
s |= evsllseg (Vptr x) Vnull ((a1::l1)++(a2::l2)) lx ->
get_last_ptr (a1::l1) = Some (Vptr x) ->
False.
Lemma get_last_not_in_false : forall {A B:Type} (l1 l2:list A) (e:B) (f:A->option B),
get_last l1 f = Some e -> not_in e (l1 ++ l2) f -> False.
Lemma not_in_get_last_ptr_false : forall l1 l2 x,
not_in x (l1++l2) ecb_get_next_ptr -> get_last_ptr l1 = Some x ->
False.
Qed.
Lemma val_eq_true_eq : forall v1 v2, val_eq v1 v2 = Some (Vint32 Int.one) -> v1 = v2.
Ltac solve_Afalse_in_pre :=
eapply backward_rule1 with (p:=Afalse);
[intros s_1 H_1; destruct_s s_1; simpl in H_1; mytac; tryfalse |
apply pfalse_rule].
Lemma struct_type_vallist_match_os_event : forall v, struct_type_vallist_match OS_EVENT v -> exists v1 v2 v3 v4 v5 v6 tail, v = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: tail.
Lemma evsllseg_list_len_eq´ : forall l1 l2 s p1 p2,
s |= evsllseg p1 p2 l1 l2 -> length l1 = length l2.
Definition val_beq (v1 v2:val) :=
match v1, v2 with
| Vundef, Vundef => true
| Vnull, Vnull => true
| Vint32 i1, Vint32 i2 => Int.eq i1 i2
| Vptr (b1, i1), Vptr (b2, i2) => peq b1 b2 && Int.eq i1 i2
| _, _ => false
end.
Fixpoint ptr_in_ectrls´ (l:list EventCtr) (ptr:val) {struct l}:=
match l with
| nil => false
| (a, b)::t => match t with
| nil => false
| _ :: _ => match V_OSEventListPtr a with
| Some ptr´ => match val_beq ptr ptr´ with
| true => true
| false => ptr_in_ectrls´ t ptr
end
| _ => ptr_in_ectrls´ t ptr
end
end
end.
Definition ptr_in_ectrls (head:val) (l:list EventCtr) (ptr:val) :=
match val_beq head ptr with
| true => true
| false => ptr_in_ectrls´ l ptr
end.
Lemma while_rule´´ : forall Spec I r ri p s e v tp,
p ==> Rv e @ tp == v ->
{|Spec, GetHPrio, I, r, ri|}|-{{p**[|v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef|]}}s{{p}} ->
{|Spec, GetHPrio, I, r, ri|}|-{{p}}swhile e s{{p**[|v = Vint32 Int.zero \/ v = Vnull|]}}.
Lemma evsllseg_vnull_false : forall s h t l,
s |= evsllseg Vnull Vnull (h :: t) l -> False.
Lemma evsllseg_vnull_false_p : forall s h t l P,
s |= evsllseg Vnull Vnull (h :: t) l ** P -> False.
Lemma val_beq_true_eq : forall v1 v2, val_beq v1 v2 = true -> v1 = v2.
Lemma val_beq_true : forall v, val_beq v v = true.
Lemma ptr_in_ectrls_nil_false : forall head ptr,
head <> ptr -> ptr_in_ectrls head nil ptr = false.
Lemma isptr_vundef1 : forall x,
isptr x ->
val_inj (bool_and (val_inj (notint (val_inj (val_eq x Vnull)))) (Vint32 Int.one)) <>Vundef.
Lemma evsllseg_head_isptr´ : forall l1 l2 s p1,
s |= evsllseg p1 Vnull l1 l2 -> isptr p1.
Lemma evsllseg_has_node : forall s x l1 l2,
s |= evsllseg (Vptr x) Vnull l1 l2 ->
exists h1 t1 h2 t2, l1 = h1 :: t1 /\ l2 = h2 :: t2.
Lemma isptr_val_inj_vundef : forall x p,
isptr p -> val_inj (notint (val_inj (val_eq p (Vptr x)))) <> Vundef.
Lemma evsllseg_append1 : forall (v´9:list EventCtr) (v´11:list EventData) v´6 v´13 v´12 x4 (v1:val) x6 v´8 x8 v´10 v0 v1 v´9 v´11 s d i0,
RL_Tbl_Grp_P v0 v´12 -> id_addrval´ (Vptr (v´13, Int.zero)) OSEventTbl OS_EVENT = Some v´10 -> struct_type_vallist_match OS_EVENT
(i0 :: v´12 :: x4 :: v1 :: x6 :: v´8 :: x8) ->
s |= evsllseg v´6 (Vptr (v´13, Int.zero)) v´9 v´11 **
Astruct (v´13, Int.zero) OS_EVENT(i0 :: v´12 :: x4 :: v1 :: x6 :: v´8 :: x8) **
AOSEventTbl v´10 v0 ** AEventData (i0 :: v´12 :: x4 :: v1 :: x6 :: v´8 :: x8) d ->
s |= evsllseg v´6 v´8 (v´9 ++ (i0 :: v´12 :: x4 :: v1 :: x6 :: v´8 :: x8, v0) :: nil) (v´11 ++ d :: nil).
Lemma notbool_one_zero : Int.notbool Int.one = Int.zero.
Lemma notbool_zero_one : Int.notbool Int.zero = Int.one.
Lemma evsllseg_vnull_nil_p : forall {l1 l2 s P},
s |= evsllseg Vnull Vnull l1 l2 ** P -> l1 = nil /\ l2 = nil.
Lemma get_last_ptr_ptr_in_ectrls_true : forall l x head h t,
get_last_ptr l = Some (Vptr x) ->
ptr_in_ectrls head (l ++ h::t) (Vptr x) = true.
Lemma val_beq_sym : forall v1 v2, val_beq v1 v2 = val_beq v2 v1.
Qed.
Lemma evsllseg_get_last_eq_p :
forall (ls1 : list EventCtr) (head tail : val) (ls2 : list EventData)
(s : RstateOP) P,
ls1 <> nil ->
s |= evsllseg head tail ls1 ls2 ** P -> get_last_ptr ls1 = Some tail.
Lemma ptr_in_ectrls_false_append : forall l head p1 p2 e,
ptr_in_ectrls head l p1 = false ->
get_last_ptr l = Some p2 ->
p1 <> p2 ->
ptr_in_ectrls head (l ++ e :: nil) p1 = false.
Lemma val_inj_notint_zero_eq : forall v1 v2,
val_inj (notint (val_inj (val_eq v1 v2))) = Vint32 Int.zero -> v1 = v2.
Lemma int_eq_true_eq : forall i1 i2, Int.eq i1 i2 = true -> i1 = i2.
Qed.
Lemma val_inj_notint_vnull_false : forall x, val_inj (notint x) = Vnull -> False.
Open Scope code_scope.
Lemma aistrue_oand : forall s b1 b2,
s |= Aistrue ( b1 &&ₑ b2) -> s |= Aistrue b1 /\ s |= Aistrue b2.
Lemma evsllseg_ecbls_ptr_distinct:
forall l1 l2 s head p vl P,
s |= evsllseg head (Vptr p) l1 l2 ** Astruct p OS_EVENT vl ** P ->
ecbls_ptr_distinct l1.
Lemma evsllseg_astruct_not_in :
forall l1 l2 v p vl P s,
s |= evsllseg v (Vptr p) l1 l2 ** Astruct p OS_EVENT vl ** P ->
not_in v l1 ecb_get_next_ptr.
Qed.
Lemma ecbls_ptr_distinct_get_last_eq : forall (l1 l2 l1´ l2´: list EventCtr) e,
ecbls_ptr_distinct (l1++l2) -> l1++l2 = l1´++l2´ ->
get_last l1 ecb_get_next_ptr = Some e -> get_last l1´ ecb_get_next_ptr = Some e ->
l1 = l1´.
Lemma get_last_get_last_ptr_eq :
forall l, get_last_ptr l = get_last l ecb_get_next_ptr.
Lemma get_last_app : forall {A B:Type} (l: list A) tail f (x:B),
f tail = Some x ->
get_last (l++tail::nil) f = Some x.
Lemma app_tail_exists_head : forall {A:Type} (l:list A) tail,
exists h t, (l ++ tail::nil) = h::t.
Qed.
Lemma app_length_tail : forall {A:Type} (l:list A) tail,
length (l++tail::nil) = ((length l) + 1)%nat.
Lemma app_length_eq_eq : forall {A:Type} (l1:list A) l2 l1´ l2´,
l1 ++ l2 = l1´ ++ l2´ -> length l1 = length l1´ ->
l1 = l1´.
Lemma upd_last_ectrls_last : forall l v1 v2 v3 v4 v5 v6 v7 etbl x,
upd_last_ectrls (l ++ ((v1::v2::v3::v4::v5::v6::v7), etbl)::nil) x =
l ++ ((v1::v2::v3::v4::v5::x::v7), etbl)::nil.
Lemma cons_ext : forall {A} (h:A) t1 t2, t1 = t2 -> cons h t1 = cons h t2.
Qed.
Lemma evsllseg_merge´ : forall (l1 : list EventCtr) (l1´ : list EventData)
(l2 : list EventCtr) (l2´ : list EventData) (x1 x2 y : val) (s : RstateOP),
s |= evsllseg x1 y l1 l1´ ** evsllseg y x2 l2 l2´ ->
s |= evsllseg x1 x2 (l1 ++ l2) (l1´ ++ l2´).
Require Import mathlib.
Require Export oscore_common.
Fixpoint not_in {A B:Type} (e:B) (l:list A) (f:A -> option B) :=
match l with
| nil => True
| h :: t => (forall e´, f h = Some e´ -> e´ <> e) /\ not_in e t f
end.
Fixpoint distinct´ {A B:Type} (l:list A) (f:A -> option B) :=
match l with
| nil => True
| h :: t => (forall e, f h = Some e -> not_in e t f) /\ distinct´ t f
end.
Definition distinct {A B:Type} (head:B) (l:list A) f := distinct´ l f /\ not_in head l f.
Fixpoint get_last {A B:Type} (l:list A) (f: A->option B) :=
match l with
| nil => None
| e::nil => f e
| h::t => get_last t f
end.
Definition ecb_get_next_ptr (ecb: EventCtr) := let (a, b) := ecb in V_OSEventListPtr a.
Definition ecbls_ptr_distinct (ecbls: list EventCtr):= distinct´ ecbls ecb_get_next_ptr.
Lemma evsllseg_distinct :
forall l1 l2 head s P,
s |= evsllseg head Vnull l1 l2 ** P ->
ecbls_ptr_distinct l1.
Lemma evsllseg_not_in_vnull :
forall l1 l2 head s P,
s |= evsllseg head Vnull l1 l2 ** P ->
not_in head l1 ecb_get_next_ptr.
Lemma AEventNode_vnull_false :
forall s v v0 e0 P,
s |= AEventNode Vnull v v0 e0 ** P ->
False.
Qed.
Lemma evsllseg_not_in_vnull´ :
forall l1 l2 head s,
s |= evsllseg head Vnull l1 l2 ->
not_in head l1 ecb_get_next_ptr.
Qed.
Lemma evsllseg_distinct´ :
forall l1 l2 head s,
s |= evsllseg head Vnull l1 l2 ->
ecbls_ptr_distinct l1.
Lemma evsllseg_ptr_dup_false : forall l1 l2 x a1 a2 s lx ,
s |= evsllseg (Vptr x) Vnull ((a1::l1)++(a2::l2)) lx ->
get_last_ptr (a1::l1) = Some (Vptr x) ->
False.
Lemma get_last_not_in_false : forall {A B:Type} (l1 l2:list A) (e:B) (f:A->option B),
get_last l1 f = Some e -> not_in e (l1 ++ l2) f -> False.
Lemma not_in_get_last_ptr_false : forall l1 l2 x,
not_in x (l1++l2) ecb_get_next_ptr -> get_last_ptr l1 = Some x ->
False.
Qed.
Lemma val_eq_true_eq : forall v1 v2, val_eq v1 v2 = Some (Vint32 Int.one) -> v1 = v2.
Ltac solve_Afalse_in_pre :=
eapply backward_rule1 with (p:=Afalse);
[intros s_1 H_1; destruct_s s_1; simpl in H_1; mytac; tryfalse |
apply pfalse_rule].
Lemma struct_type_vallist_match_os_event : forall v, struct_type_vallist_match OS_EVENT v -> exists v1 v2 v3 v4 v5 v6 tail, v = v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: tail.
Lemma evsllseg_list_len_eq´ : forall l1 l2 s p1 p2,
s |= evsllseg p1 p2 l1 l2 -> length l1 = length l2.
Definition val_beq (v1 v2:val) :=
match v1, v2 with
| Vundef, Vundef => true
| Vnull, Vnull => true
| Vint32 i1, Vint32 i2 => Int.eq i1 i2
| Vptr (b1, i1), Vptr (b2, i2) => peq b1 b2 && Int.eq i1 i2
| _, _ => false
end.
Fixpoint ptr_in_ectrls´ (l:list EventCtr) (ptr:val) {struct l}:=
match l with
| nil => false
| (a, b)::t => match t with
| nil => false
| _ :: _ => match V_OSEventListPtr a with
| Some ptr´ => match val_beq ptr ptr´ with
| true => true
| false => ptr_in_ectrls´ t ptr
end
| _ => ptr_in_ectrls´ t ptr
end
end
end.
Definition ptr_in_ectrls (head:val) (l:list EventCtr) (ptr:val) :=
match val_beq head ptr with
| true => true
| false => ptr_in_ectrls´ l ptr
end.
Lemma while_rule´´ : forall Spec I r ri p s e v tp,
p ==> Rv e @ tp == v ->
{|Spec, GetHPrio, I, r, ri|}|-{{p**[|v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef|]}}s{{p}} ->
{|Spec, GetHPrio, I, r, ri|}|-{{p}}swhile e s{{p**[|v = Vint32 Int.zero \/ v = Vnull|]}}.
Lemma evsllseg_vnull_false : forall s h t l,
s |= evsllseg Vnull Vnull (h :: t) l -> False.
Lemma evsllseg_vnull_false_p : forall s h t l P,
s |= evsllseg Vnull Vnull (h :: t) l ** P -> False.
Lemma val_beq_true_eq : forall v1 v2, val_beq v1 v2 = true -> v1 = v2.
Lemma val_beq_true : forall v, val_beq v v = true.
Lemma ptr_in_ectrls_nil_false : forall head ptr,
head <> ptr -> ptr_in_ectrls head nil ptr = false.
Lemma isptr_vundef1 : forall x,
isptr x ->
val_inj (bool_and (val_inj (notint (val_inj (val_eq x Vnull)))) (Vint32 Int.one)) <>Vundef.
Lemma evsllseg_head_isptr´ : forall l1 l2 s p1,
s |= evsllseg p1 Vnull l1 l2 -> isptr p1.
Lemma evsllseg_has_node : forall s x l1 l2,
s |= evsllseg (Vptr x) Vnull l1 l2 ->
exists h1 t1 h2 t2, l1 = h1 :: t1 /\ l2 = h2 :: t2.
Lemma isptr_val_inj_vundef : forall x p,
isptr p -> val_inj (notint (val_inj (val_eq p (Vptr x)))) <> Vundef.
Lemma evsllseg_append1 : forall (v´9:list EventCtr) (v´11:list EventData) v´6 v´13 v´12 x4 (v1:val) x6 v´8 x8 v´10 v0 v1 v´9 v´11 s d i0,
RL_Tbl_Grp_P v0 v´12 -> id_addrval´ (Vptr (v´13, Int.zero)) OSEventTbl OS_EVENT = Some v´10 -> struct_type_vallist_match OS_EVENT
(i0 :: v´12 :: x4 :: v1 :: x6 :: v´8 :: x8) ->
s |= evsllseg v´6 (Vptr (v´13, Int.zero)) v´9 v´11 **
Astruct (v´13, Int.zero) OS_EVENT(i0 :: v´12 :: x4 :: v1 :: x6 :: v´8 :: x8) **
AOSEventTbl v´10 v0 ** AEventData (i0 :: v´12 :: x4 :: v1 :: x6 :: v´8 :: x8) d ->
s |= evsllseg v´6 v´8 (v´9 ++ (i0 :: v´12 :: x4 :: v1 :: x6 :: v´8 :: x8, v0) :: nil) (v´11 ++ d :: nil).
Lemma notbool_one_zero : Int.notbool Int.one = Int.zero.
Lemma notbool_zero_one : Int.notbool Int.zero = Int.one.
Lemma evsllseg_vnull_nil_p : forall {l1 l2 s P},
s |= evsllseg Vnull Vnull l1 l2 ** P -> l1 = nil /\ l2 = nil.
Lemma get_last_ptr_ptr_in_ectrls_true : forall l x head h t,
get_last_ptr l = Some (Vptr x) ->
ptr_in_ectrls head (l ++ h::t) (Vptr x) = true.
Lemma val_beq_sym : forall v1 v2, val_beq v1 v2 = val_beq v2 v1.
Qed.
Lemma evsllseg_get_last_eq_p :
forall (ls1 : list EventCtr) (head tail : val) (ls2 : list EventData)
(s : RstateOP) P,
ls1 <> nil ->
s |= evsllseg head tail ls1 ls2 ** P -> get_last_ptr ls1 = Some tail.
Lemma ptr_in_ectrls_false_append : forall l head p1 p2 e,
ptr_in_ectrls head l p1 = false ->
get_last_ptr l = Some p2 ->
p1 <> p2 ->
ptr_in_ectrls head (l ++ e :: nil) p1 = false.
Lemma val_inj_notint_zero_eq : forall v1 v2,
val_inj (notint (val_inj (val_eq v1 v2))) = Vint32 Int.zero -> v1 = v2.
Lemma int_eq_true_eq : forall i1 i2, Int.eq i1 i2 = true -> i1 = i2.
Qed.
Lemma val_inj_notint_vnull_false : forall x, val_inj (notint x) = Vnull -> False.
Open Scope code_scope.
Lemma aistrue_oand : forall s b1 b2,
s |= Aistrue ( b1 &&ₑ b2) -> s |= Aistrue b1 /\ s |= Aistrue b2.
Lemma evsllseg_ecbls_ptr_distinct:
forall l1 l2 s head p vl P,
s |= evsllseg head (Vptr p) l1 l2 ** Astruct p OS_EVENT vl ** P ->
ecbls_ptr_distinct l1.
Lemma evsllseg_astruct_not_in :
forall l1 l2 v p vl P s,
s |= evsllseg v (Vptr p) l1 l2 ** Astruct p OS_EVENT vl ** P ->
not_in v l1 ecb_get_next_ptr.
Qed.
Lemma ecbls_ptr_distinct_get_last_eq : forall (l1 l2 l1´ l2´: list EventCtr) e,
ecbls_ptr_distinct (l1++l2) -> l1++l2 = l1´++l2´ ->
get_last l1 ecb_get_next_ptr = Some e -> get_last l1´ ecb_get_next_ptr = Some e ->
l1 = l1´.
Lemma get_last_get_last_ptr_eq :
forall l, get_last_ptr l = get_last l ecb_get_next_ptr.
Lemma get_last_app : forall {A B:Type} (l: list A) tail f (x:B),
f tail = Some x ->
get_last (l++tail::nil) f = Some x.
Lemma app_tail_exists_head : forall {A:Type} (l:list A) tail,
exists h t, (l ++ tail::nil) = h::t.
Qed.
Lemma app_length_tail : forall {A:Type} (l:list A) tail,
length (l++tail::nil) = ((length l) + 1)%nat.
Lemma app_length_eq_eq : forall {A:Type} (l1:list A) l2 l1´ l2´,
l1 ++ l2 = l1´ ++ l2´ -> length l1 = length l1´ ->
l1 = l1´.
Lemma upd_last_ectrls_last : forall l v1 v2 v3 v4 v5 v6 v7 etbl x,
upd_last_ectrls (l ++ ((v1::v2::v3::v4::v5::v6::v7), etbl)::nil) x =
l ++ ((v1::v2::v3::v4::v5::x::v7), etbl)::nil.
Lemma cons_ext : forall {A} (h:A) t1 t2, t1 = t2 -> cons h t1 = cons h t2.
Qed.
Lemma evsllseg_merge´ : forall (l1 : list EventCtr) (l1´ : list EventData)
(l2 : list EventCtr) (l2´ : list EventData) (x1 x2 y : val) (s : RstateOP),
s |= evsllseg x1 y l1 l1´ ** evsllseg y x2 l2 l2´ ->
s |= evsllseg x1 x2 (l1 ++ l2) (l1´ ++ l2´).