--- a/Co2sobj_prop.thy Tue Aug 27 08:50:53 2013 +0800
+++ b/Co2sobj_prop.thy Wed Aug 28 08:59:12 2013 +0800
@@ -1,6 +1,6 @@
(*<*)
theory Co2sobj_prop
-imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop
+imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop Alive_prop
begin
(*<*)
@@ -222,37 +222,148 @@
| _ \<Rightarrow> None)
else cqm2sms s q' ms)"
apply (frule vt_grant_os, frule vd_cons)
-apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2)
-using cm2smsg_recvmsg1 cm2smsg_recvmsg2
-apply (auto split:if_splits option.splits)
+apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2
+ dest!:current_has_sms')
+apply (case_tac "msgs_of_queue s q", simp)
+apply (frule_tac ms = "tl (msgs_of_queue s q)" in cqm2sms_recvmsg1)
+apply (drule_tac q = q in distinct_queue_msgs, simp+)
+apply (case_tac a, auto simp:cqm2sms.simps split:option.splits if_splits)
+done
+lemma cqm2sms_removemsgq:
+ "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk>
+ \<Longrightarrow> cqm2sms (RemoveMsgq p q # s) q' ms = cqm2sms s q' ms"
+apply (frule vt_grant_os, frule vd_cons)
+apply (induct ms rule:rev_induct)
+apply (auto simp:cqm2sms_simps2 cm2smsg_removemsgq split:option.splits if_splits)
+done
-lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg
+lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg cqm2sms_removemsgq
(********************* cq2smsgq simpset ***********************)
lemma cq2smsgq_other:
- "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m;
+ "\<lbrakk>valid (e # s); \<forall> p q. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m;
\<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk>
\<Longrightarrow> cq2smsgq (e # s) = cq2smsgq s"
+apply (frule cqm2sms_other, simp+)
apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e)
apply (auto simp:cq2smsgq_def sectxt_of_obj_simps
split:t_object.splits option.splits if_splits
- dest:not_deleted_init_msg dest!:current_has_sec')
+ dest:not_deleted_init_msg)
+done
+
+lemma cq2smsg_createmsgq:
+ "valid (CreateMsgq p q # s)
+ \<Longrightarrow> cq2smsgq (CreateMsgq p q # s) = (cq2smsgq s) (q :=
+ case (sectxt_of_obj s (O_proc p)) of
+ Some psec \<Rightarrow> Some (Created, (fst psec, R_object, (snd o snd) psec), [])
+ | None \<Rightarrow> None)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule cqm2sms_createmsgq)
+apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq
+ split:option.splits if_splits dest:not_deleted_init_msgq)
+done
+lemma cq2smsg_sendmsg:
+ "valid (SendMsg p q m # s)
+ \<Longrightarrow> cq2smsgq (SendMsg p q m # s) = (cq2smsgq s) (q :=
+ case (cq2smsgq s q, sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of
+ (Some (qi, sec, sms), Some msec) \<Rightarrow>
+ Some (qi, sec, sms @ [(Created, msec, O_msg q m \<in> tainted (SendMsg p q m # s))])
+ | _ \<Rightarrow> None)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext)
+apply (frule_tac q' = x in cqm2sms_sendmsg, simp)
+apply (auto simp:cq2smsgq_def sectxt_of_obj_simps split:option.splits if_splits
+ dest!:current_has_sms' current_has_sec')
+done
+
+lemma current_has_smsgq:
+ "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sq. cq2smsgq s q = Some sq"
+by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sec' current_has_sms')
+
+lemma current_has_smsgq':
+ "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"
+by (auto dest:current_has_smsgq)
-
-
+lemma cq2smsg_recvmsg:
+ "valid (RecvMsg p q m # s)
+ \<Longrightarrow> cq2smsgq (RecvMsg p q m # s) = (cq2smsgq s) (q :=
+ case (cq2smsgq s q) of
+ Some (qi, sec, sms) \<Rightarrow> Some (qi, sec, tl sms)
+ | _ \<Rightarrow> None)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext, frule_tac q' = x in cqm2sms_recvmsg, simp)
+apply (auto simp add:cq2smsgq_def sectxt_of_obj_simps split:option.splits if_splits
+ dest!:current_has_sec' current_has_sms' current_has_smsgq')
+done
-lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
+lemma cq2smsg_removemsgq:
+ "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk>
+ \<Longrightarrow> cq2smsgq (RemoveMsgq p q # s) q' = cq2smsgq s q'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto simp:cq2smsgq_def sectxt_of_obj_simps cqm2sms_removemsgq split:if_splits option.splits
+ dest!:current_has_sec' current_has_sms' current_has_smsgq')
+done
+
+lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq
+lemma sm_in_sqsms_init_aux:
+ "\<lbrakk>m \<in> set ms; init_cm2smsg q m = Some sm; q \<in> init_msgqs;
+ init_cqm2sms q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
+apply (induct ms arbitrary:m sm sms)
+by (auto split:if_splits option.splits)
+
+lemma sm_in_sqsms_init:
+ "\<lbrakk>m \<in> set (init_msgs_of_queue q); init_cm2smsg q m = Some sm; q \<in> init_msgqs;
+ init_cqm2sms q (init_msgs_of_queue q) = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
+by (simp add:sm_in_sqsms_init_aux)
+
+lemma cqm2sms_prop0:
+ "\<lbrakk>m \<in> set ms; cm2smsg s q m = Some sm; cqm2sms s q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"
+apply (induct ms arbitrary:m sm sms)
+apply (auto simp:cqm2sms.simps split:option.splits)
+done
lemma sm_in_sqsms:
"\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; cq2smsgq s q = Some (qi, qsec, sms);
cm2smsg s q m = Some sm\<rbrakk> \<Longrightarrow> sm \<in> set sms"
-sorry
+proof (induct s arbitrary:m q qi qsec sms sm)
+ case Nil
+ thus ?case
+ by (simp add:cq2smsga_nil_prop cm2smsg_nil_prop init_cq2smsgq_def sm_in_sqsms_init
+ split:option.splits)
+next
+ case (Cons e s)
+ hence p1:"\<And> m q qi qsec sms sm. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s;
+ cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>
+ \<Longrightarrow> sm \<in> set sms" and p2: "m \<in> set (msgs_of_queue (e # s) q)"
+ and p3: "q \<in> current_msgqs (e # s)" and p4: "valid (e # s)"
+ and p5: "cq2smsgq (e # s) q = Some (qi, qsec, sms)"
+ and p6: "cm2smsg (e # s) q m = Some sm" by auto
+ from p4 have os: "os_grant s e" and vd: "valid s" by (auto dest:vd_cons vt_grant_os)
+(*
+ from p1 have p1':
+ "\<And> m q qi qsec sms sm ms. \<lbrakk>m \<in> set ms; set ms \<subseteq> set (msgs_of_queue s q); q \<in> current_msgqs s;
+ valid s; cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>
+ \<Longrightarrow> sm \<in> set "
+*)
+ show ?case using p2 p3 p4 p5 p6 vd os
+ apply (case_tac e)
+ apply (auto simp:cq2smsgq_simps cm2smsg_simps split:if_splits option.splits intro:p1)
+ apply (rule_tac m = m and q = q and qi = qi and qsec = qsec in p1, simp+)
+ apply (case_tac "q = nat2", simp)
+ apply (drule cq2smsg_createmsgq, simp, simp)
+ apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)
+
+ apply (simp add:cq2smsgq_def split:option.splits)
+ apply (rule_tac m = m and sm = sm in cqm2sms_prop0, simp+)
+ apply (simp add:cqm2sms_recvmsg)
+ done
+qed
(****************** cf2sfile path simpset ***************)
@@ -1489,10 +1600,6 @@
lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other
-
-
-
-
end
(*<*)