3 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

     3 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

   225 apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2)

   225 apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2 

   226 using cm2smsg_recvmsg1 cm2smsg_recvmsg2

   226      dest!:current_has_sms')

   227 apply (auto split:if_splits option.splits)

   227 apply (case_tac "msgs_of_queue s q", simp)

   228 

   228 apply (frule_tac ms = "tl (msgs_of_queue s q)" in cqm2sms_recvmsg1)

   229 apply (drule_tac q = q in distinct_queue_msgs, simp+)

   230 apply (case_tac a, auto simp:cqm2sms.simps split:option.splits if_splits)

   231 done

   232 

   233 lemma cqm2sms_removemsgq:

   234   "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk> 

   235    \<Longrightarrow> cqm2sms (RemoveMsgq p q # s) q' ms = cqm2sms s q' ms"

   236 apply (frule vt_grant_os, frule vd_cons)

   237 apply (induct ms rule:rev_induct)

   238 apply (auto simp:cqm2sms_simps2 cm2smsg_removemsgq split:option.splits if_splits)

   239 done

   230 lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg

   241 lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg cqm2sms_removemsgq

   235   "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 

   246   "\<lbrakk>valid (e # s); \<forall> p q. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 

   241             dest:not_deleted_init_msg  dest!:current_has_sec') 

   253             dest:not_deleted_init_msg) 

   242 

   254 done

   243 

   255 

   244   

   256 lemma cq2smsg_createmsgq:

   245 

   257   "valid (CreateMsgq p q # s)

   246 

   258    \<Longrightarrow> cq2smsgq (CreateMsgq p q # s) = (cq2smsgq s) (q := 

   247 lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other 

   259      case (sectxt_of_obj s (O_proc p)) of

   248 

   260        Some psec \<Rightarrow> Some (Created, (fst psec, R_object, (snd o snd) psec), [])

   261      | None     \<Rightarrow> None)"

   262 apply (frule vd_cons, frule vt_grant_os)

   263 apply (frule cqm2sms_createmsgq)

   264 apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq 

   265   split:option.splits if_splits dest:not_deleted_init_msgq)

   266 done

   267 

   268 lemma cq2smsg_sendmsg:

   269   "valid (SendMsg p q m # s) 

   270    \<Longrightarrow> cq2smsgq (SendMsg p q m # s) = (cq2smsgq s) (q := 

   271      case (cq2smsgq s q, sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of 

   272        (Some (qi, sec, sms), Some msec) \<Rightarrow> 

   273           Some (qi, sec, sms @ [(Created, msec, O_msg q m \<in> tainted (SendMsg p q m # s))])

   274      | _ \<Rightarrow> None)"

   275 apply (frule vd_cons, frule vt_grant_os)

   276 apply (rule ext)

   277 apply (frule_tac q' = x in cqm2sms_sendmsg, simp)

   278 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps  split:option.splits if_splits

   279   dest!:current_has_sms' current_has_sec')

   280 done

   281 

   282 lemma current_has_smsgq:

   283   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sq. cq2smsgq s q = Some sq"

   284 by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sec' current_has_sms')

   285 

   286 lemma current_has_smsgq':

   287   "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"

   288 by (auto dest:current_has_smsgq)

   289 

   290 lemma cq2smsg_recvmsg:

   291   "valid (RecvMsg p q m # s) 

   292    \<Longrightarrow> cq2smsgq (RecvMsg p q m # s) = (cq2smsgq s) (q := 

   293     case (cq2smsgq s q) of

   294       Some (qi, sec, sms) \<Rightarrow> Some (qi, sec, tl sms)

   295     | _ \<Rightarrow> None)"

   296 apply (frule vd_cons, frule vt_grant_os)

   297 apply (rule ext, frule_tac q' = x in cqm2sms_recvmsg, simp)

   298 apply (auto simp add:cq2smsgq_def sectxt_of_obj_simps split:option.splits if_splits 

   299   dest!:current_has_sec' current_has_sms' current_has_smsgq')

   300 done

   301 

   302 lemma cq2smsg_removemsgq:

   303   "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk>

   304    \<Longrightarrow> cq2smsgq (RemoveMsgq p q # s) q' = cq2smsgq s q'"

   305 apply (frule vd_cons, frule vt_grant_os)

   306 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps cqm2sms_removemsgq split:if_splits option.splits 

   307   dest!:current_has_sec' current_has_sms' current_has_smsgq')

   308 done

   309 

   310 lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq

   311 

   312 lemma sm_in_sqsms_init_aux:

   313   "\<lbrakk>m \<in> set ms; init_cm2smsg q m = Some sm; q \<in> init_msgqs; 

   314     init_cqm2sms q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   315 apply (induct ms arbitrary:m sm sms)

   316 by (auto split:if_splits option.splits)

   317 

   318 lemma sm_in_sqsms_init:

   319   "\<lbrakk>m \<in> set (init_msgs_of_queue q); init_cm2smsg q m = Some sm; q \<in> init_msgqs; 

   320     init_cqm2sms q (init_msgs_of_queue q) = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   321 by (simp add:sm_in_sqsms_init_aux)

   322 

   323 lemma cqm2sms_prop0:

   324   "\<lbrakk>m \<in> set ms; cm2smsg s q m = Some sm; cqm2sms s q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   325 apply (induct ms arbitrary:m sm sms)

   326 apply (auto simp:cqm2sms.simps split:option.splits)

   327 done

   253 sorry

   332 proof (induct s arbitrary:m q qi qsec sms sm)

   254 

   333   case Nil

   255 

   334   thus ?case 

   335     by (simp add:cq2smsga_nil_prop cm2smsg_nil_prop init_cq2smsgq_def sm_in_sqsms_init 

   336            split:option.splits)

   337 next

   338   case (Cons e s)

   339   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; 

   340     cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>

   341     \<Longrightarrow> sm \<in> set sms" and p2: "m \<in> set (msgs_of_queue (e # s) q)" 

   342     and p3: "q \<in> current_msgqs (e # s)" and p4: "valid (e # s)"

   343     and p5: "cq2smsgq (e # s) q = Some (qi, qsec, sms)"

   344     and p6: "cm2smsg (e # s) q m = Some sm" by auto

   345   from p4 have os: "os_grant s e" and vd: "valid s" by (auto dest:vd_cons vt_grant_os)

   346 (*

   347   from p1 have p1':

   348     "\<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;

   349     valid s; cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>

   350     \<Longrightarrow> sm \<in> set "

   351 *)

   352   show ?case using p2 p3 p4 p5 p6 vd os

   353     apply (case_tac e)

   354     apply (auto simp:cq2smsgq_simps cm2smsg_simps split:if_splits option.splits intro:p1)

   355 

   356     apply (rule_tac m = m and q = q and qi = qi and qsec = qsec in p1, simp+)

   357     apply (case_tac "q = nat2", simp)

   358     apply (drule cq2smsg_createmsgq, simp, simp)

   359 

   360     apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)

   361 

   362     apply (simp add:cq2smsgq_def split:option.splits)

   363     apply (rule_tac m = m and sm = sm in cqm2sms_prop0, simp+)

   364     apply (simp add:cqm2sms_recvmsg)

   365     done

   366 qed