theory Enrichimports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 Tempbegin(* enriched objects, closely related to static objects, so are only 3 kinds *)datatype t_enrich_obj = E_proc "t_process" "t_msgq" "t_msgq"| E_file "t_file" "nat" | E_file_link "t_file"| E_msgq "t_msgq"(* objects that need dynamic indexing, all nature-numbers *)datatype t_index_obj = I_proc "t_process" | I_file "t_file"| I_fd "t_process" "t_fd"| I_inum "nat"| I_msgq "t_msgq"| I_msg "t_msgq" "t_msg"context tainting_s beginfun no_del_event:: "t_event list \<Rightarrow> bool"where "no_del_event [] = True"| "no_del_event (Kill p p' # \<tau>) = False"| "no_del_event (Exit p # s) = False"| "no_del_event (CloseFd p fd # \<tau>) = False"| "no_del_event (UnLink p f # \<tau>) = False"| "no_del_event (Rmdir p f # \<tau>) = False"(*| "no_del_event (Rename p f f' # \<tau>) = False"*)| "no_del_event (RemoveMsgq p q # \<tau>) = False"(*| "no_del_event (RecvMsg p q m # \<tau>) = False"*)| "no_del_event (_ # \<tau>) = no_del_event \<tau>"(*fun all_inums :: "t_state \<Rightarrow> t_inode_num set"where "all_inums [] = current_inode_nums []"| "all_inums (Open p f flags fd opt # s) = ( case opt of None \<Rightarrow> all_inums s | Some i \<Rightarrow> all_inums s \<union> {i} )"| "all_inums (Mkdir p f i # s) = (all_inums s \<union> {i})"| "all_inums (CreateSock p af st fd i # s) = (all_inums s \<union> {i})"| "all_inums (Accept p fd addr lport fd' i # s) = (all_inums s \<union> {i})"| "all_inums (_ # s) = all_inums s"fun all_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"where "all_fds [] = init_fds_of_proc"| "all_fds (Open p f flags fd ipt # s) = (all_fds s) (p := all_fds s p \<union> {fd})"| "all_fds (CreateSock p sf st fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})"| "all_fds (Accept p fd' raddr port fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})"| "all_fds (Clone p p' fds # s) = (all_fds s) (p' := fds)"| "all_fds (_ # s) = all_fds s"fun all_msgqs:: "t_state \<Rightarrow> t_msgq set"where "all_msgqs [] = {}"| "all_msgqs (CreateMsgq p q # s) = all_msgqs s \<union> {q}"| "all_msgqs (e # s) = all_msgqs s"*)fun all_msgs:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg set"where "all_msgs [] q = {}"| "all_msgs (CreateMsgq p q # s) q' = (if q' = q then {} else all_msgs s q')"| "all_msgs (SendMsg p q m # s) q' = (if q' = q then all_msgs s q \<union> {m} else all_msgs s q')"| "all_msgs (_ # s) q' = all_msgs s q'"fun all_files:: "t_state \<Rightarrow> t_file set"where "all_files [] = init_files "| "all_files (Open p f flags fd opt # s) = (if opt = None then all_files s else (all_files s \<union> {f}))"| "all_files (Mkdir p f inum # s) = all_files s \<union> {f}"| "all_files (LinkHard p f f' # s) = all_files s \<union> {f'}"| "all_files (e # s) = all_files s"(*fun notin_all:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool"where "notin_all s (E_proc p) = (p \<notin> all_procs s)"| "notin_all s (E_file f) = (f \<notin> all_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf))"| "notin_all s (E_fd p fd) = (fd \<notin> all_fds s p)"| "notin_all s (E_inum i) = (i \<notin> all_inums s)"| "notin_all s (E_msgq q) = (q \<notin> all_msgqs s)"| "notin_all s (E_msg q m) = (m \<notin> all_msgs s q)"*)fun nums_of_recvmsg:: "t_state \<Rightarrow> t_process \<Rightarrow> nat"where "nums_of_recvmsg [] p' = 0"| "nums_of_recvmsg (RecvMsg p q m # s) p' = (if p' = p then Suc (nums_of_recvmsg s p) else nums_of_recvmsg s p')"| "nums_of_recvmsg (e # s) p' = nums_of_recvmsg s p'"lemma nums_of_recv_0: "\<lbrakk>p \<notin> current_procs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> nums_of_recvmsg s p = 0"apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply (auto)donelemma new_msgq_1: "\<lbrakk>new_msgq s \<le> q; q \<le> new_msgq s - Suc 0\<rbrakk> \<Longrightarrow> False"apply (subgoal_tac "new_msgq s \<noteq> 0")apply (simp, simp add:new_msgq_def next_nat_def)donefun notin_cur:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool"where "notin_cur s (E_proc p qmin qmax) = (p \<notin> current_procs s \<and> qmin = new_msgq s \<and> qmax = new_msgq s + (nums_of_recvmsg s p) - 1)"| "notin_cur s (E_file f inum) = (f \<notin> current_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf) \<and> inum \<notin> current_inode_nums s)"| "notin_cur s (E_file_link f) = (f \<notin> current_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf))"| "notin_cur s (E_msgq q) = (q \<notin> current_msgqs s)"(*lemma not_all_procs_cons: "p \<notin> all_procs (e # s) \<Longrightarrow> p \<notin> all_procs s"by (case_tac e, auto)lemma not_all_procs_prop: "\<lbrakk>p' \<notin> all_procs s; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<noteq> p"apply (induct s, rule notI, simp)apply (frule vt_grant_os, frule vd_cons, frule not_all_procs_cons, simp, rule notI)apply (case_tac a, auto)donelemma not_all_procs_prop2: "p' \<notin> all_procs s \<Longrightarrow> p' \<notin> init_procs"apply (induct s, simp)by (case_tac a, auto)lemma not_all_procs_prop3: "p' \<notin> all_procs s \<Longrightarrow> p' \<notin> current_procs s"apply (induct s, simp)by (case_tac a, auto)*)(*lemma not_all_msgqs_cons: "p \<notin> all_msgqs (e # s) \<Longrightarrow> p \<notin> all_msgqs s"apply (case_tac e, auto)lemma not_all_msgqs_prop: "\<lbrakk>p' \<notin> all_msgqs s; p \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> p' \<noteq> p"apply (induct s, rule notI, simp)apply (frule vt_grant_os, frule vd_cons, frule not_all_msgqs_cons, simp, rule notI)apply (case_tac a, auto)donelemma not_all_msgqs_prop3: "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s"apply (induct s, simp)by (case_tac a, auto) *)fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_index_obj \<Rightarrow> bool"where "enrich_not_alive s obj (I_file f) = (f \<notin> current_files s \<and> (\<forall> inum. obj \<noteq> E_file f inum) \<and> obj \<noteq> E_file_link f)"| "enrich_not_alive s obj (I_proc p) = (p \<notin> current_procs s \<and> (\<forall> qmin qmax. obj \<noteq> E_proc p qmin qmax))"| "enrich_not_alive s obj (I_fd p fd) = ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> (\<forall> qmin qmax. obj \<noteq> E_proc p qmin qmax))"| "enrich_not_alive s obj (I_msgq q) = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q \<and> (case obj of E_proc p qmin qmax \<Rightarrow> \<not> (q \<ge> qmin \<and> q \<le> qmax) | _ \<Rightarrow> True) )"| "enrich_not_alive s obj (I_inum i) = (i \<notin> current_inode_nums s \<and> (\<forall> f. obj \<noteq> E_file f i))"| "enrich_not_alive s obj (I_msg q m) = ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msgq q \<and> (case obj of E_proc p qmin qmax \<Rightarrow> \<not> (q \<ge> qmin \<and> q \<le> qmax) | _ \<Rightarrow> True) )"lemma file_has_parent: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> pf. is_dir s pf \<and> parent f = Some pf"apply (case_tac f)apply (simp, drule root_is_dir', simp+)apply (simp add:parentf_is_dir_prop2)donelemma enrich_search_check: assumes grant: "search_check s (up, rp, tp) f" and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" and vd: "valid s" and f_in: "is_file s f" and f_in': "is_file s' f" and sec: "sectxt_of_obj s' (O_file f) = sectxt_of_obj s (O_file f)" shows "search_check s' (up, rp, tp) f"proof (cases f) case Nil with f_in vd have "False" by (auto dest:root_is_dir') thus ?thesis by simpnext case (Cons n pf) from vd f_in obtain sf where sf: "cf2sfile s f = Some sf" apply (drule_tac is_file_in_current, drule_tac current_file_has_sfile, simp) apply (erule exE, simp) done then obtain psfs where psfs: "get_parentfs_ctxts s pf = Some psfs" using Cons by (auto simp:cf2sfile_def split:option.splits if_splits) from sf cf2sf f_in have sf': "cf2sfile s' f = Some sf" by (auto dest:is_file_in_current) then obtain psfs' where psfs': "get_parentfs_ctxts s' pf = Some psfs'"using Cons by (auto simp:cf2sfile_def split:option.splits if_splits) with sf sf' psfs have psfs_eq: "set psfs' = set psfs" using Cons f_in f_in' apply (simp add:cf2sfile_def split:option.splits) apply (case_tac sf, simp) done show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec apply (simp add:Cons split:option.splits) by (case_tac a, simp)qedlemma enrich_search_check': assumes grant: "search_check s (up, rp, tp) f" and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" and vd: "valid s" and vd': "valid s'" and f_in: "is_dir s f" and f_in': "is_dir s' f" and sec: "sectxt_of_obj s' (O_dir f) = sectxt_of_obj s (O_dir f)" shows "search_check s' (up, rp, tp) f"proof (cases f) case Nil have "sectxt_of_obj s' (O_dir []) = sectxt_of_obj s (O_dir [])" using cf2sf apply (erule_tac x = "[]" in allE) by (auto simp:cf2sfile_def root_sec_remains vd vd') thus ?thesis using grant Nil by autonext case (Cons n pf) from vd f_in obtain sf where sf: "cf2sfile s f = Some sf" apply (drule_tac is_dir_in_current, drule_tac current_file_has_sfile, simp) apply (erule exE, simp) done then obtain psfs where psfs: "get_parentfs_ctxts s pf = Some psfs" using Cons by (auto simp:cf2sfile_def split:option.splits if_splits) from sf cf2sf f_in have sf': "cf2sfile s' f = Some sf" by (auto dest:is_dir_in_current) then obtain psfs' where psfs': "get_parentfs_ctxts s' pf = Some psfs'"using Cons by (auto simp:cf2sfile_def split:option.splits if_splits) with sf sf' psfs have psfs_eq: "set psfs' = set psfs" using Cons f_in f_in' apply (drule_tac is_dir_not_file) apply (drule is_dir_not_file) apply (simp add:cf2sfile_def split:option.splits) apply (case_tac sf, simp) done show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec apply (drule_tac is_dir_not_file) apply (drule_tac is_dir_not_file) apply (simp add:Cons split:option.splits) by (case_tac a, simp)qedlemma proc_filefd_has_sfd: "\<lbrakk>fd \<in> proc_file_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> sfd. cfd2sfd s p fd = Some sfd"apply (simp add:proc_file_fds_def)apply (auto dest: current_filefd_has_sfd)donelemma enrich_inherit_fds_check: assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" and cfd2sfd: "\<forall> p fd. fd \<in> proc_file_fds s p\<longrightarrow> cfd2sfd s' p fd = cfd2sfd s p fd" and fd_in: "fds \<subseteq> proc_file_fds s p" and fd_in': "fds \<subseteq> proc_file_fds s' p" shows "inherit_fds_check s' (up, nr, nt) p fds"proof- have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" proof- fix fd assume fd_in_fds: "fd \<in> fds" hence fd_in_cfds: "fd \<in> proc_file_fds s p" and fd_in_cfds': "fd \<in> proc_file_fds s' p" using fd_in fd_in' by auto with cfd2sfd have cfd_eq: "cfd2sfd s' p fd = cfd2sfd s p fd" by auto from fd_in_cfds obtain f where ffd: "file_of_proc_fd s p fd = Some f" by (auto simp:proc_file_fds_def) moreover have "flags_of_proc_fd s p fd \<noteq> None" using ffd vd by (auto dest:current_filefd_has_flags) moreover have "sectxt_of_obj s (O_fd p fd) \<noteq> None" using fd_in_cfds vd apply (rule_tac notI) by (auto dest!:current_has_sec' file_fds_subset_pfds[where p = p] intro:vd) moreover have "cf2sfile s f \<noteq> None" apply (rule notI) apply (drule current_file_has_sfile') using ffd by (auto simp:vd is_file_in_current dest:file_of_pfd_is_file) ultimately show "sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" using cfd_eq by (auto simp:cfd2sfd_def split:option.splits) qed hence "sectxts_of_fds s' p fds = sectxts_of_fds s p fds" by (simp add:sectxts_of_fds_def) thus ?thesis using grant by (simp add:inherit_fds_check_def)qedlemma enrich_inherit_fds_check_dup: assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" and cfd2sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd s' p' fd = cfd2sfd s p fd" and fd_in: "fds' \<subseteq> fds \<inter> proc_file_fds s p" shows "inherit_fds_check s' (up, nr, nt) p' fds'"proof- have "sectxts_of_fds s' p' fds' \<subseteq> sectxts_of_fds s p fds" proof- have "\<And> fd sfd. \<lbrakk>fd \<in> fds'; sectxt_of_obj s' (O_fd p' fd) = Some sfd\<rbrakk> \<Longrightarrow> \<exists> fd \<in> fds. sectxt_of_obj s (O_fd p fd) = Some sfd" proof- fix fd sfd assume fd_in_fds': "fd \<in> fds'" and sec: "sectxt_of_obj s' (O_fd p' fd) = Some sfd" from fd_in_fds' fd_in have fd_in_fds: "fd \<in> fds" and fd_in_cfds: "fd \<in> proc_file_fds s p" by auto from fd_in_cfds obtain f where ffd: "file_of_proc_fd s p fd = Some f" by (auto simp:proc_file_fds_def) moreover have "flags_of_proc_fd s p fd \<noteq> None" using ffd vd by (auto dest:current_filefd_has_flags) moreover have "cf2sfile s f \<noteq> None" apply (rule notI) apply (drule current_file_has_sfile') using ffd by (auto simp:vd is_file_in_current dest:file_of_pfd_is_file) moreover have "sectxt_of_obj s (O_fd p fd) \<noteq> None" using fd_in_cfds vd apply (rule_tac notI) by (auto dest!:current_has_sec' file_fds_subset_pfds[where p = p] intro:vd) ultimately have "sectxt_of_obj s (O_fd p fd) = Some sfd" using fd_in_cfds cfd2sfd sec apply (erule_tac x = fd in allE) apply (auto simp:cfd2sfd_def split:option.splits) done thus "\<exists> fd \<in> fds. sectxt_of_obj s (O_fd p fd) = Some sfd" using fd_in_fds by (rule_tac x = fd in bexI, auto) qed thus ?thesis by (auto simp:sectxts_of_fds_def) qed thus ?thesis using grant by (auto simp:inherit_fds_check_def inherit_fds_check_ctxt_def)qedlemma enrich_valid_intro_cons: assumes vs': "valid s'" and vd': "valid (e # s)" and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj" and alive': "\<forall> obj. enrich_not_alive s obj' obj \<longrightarrow> enrich_not_alive s' obj' obj" and hungs: "files_hung_by_del s' = files_hung_by_del s" and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" and cq2sq: "\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq s' q = cq2smsgq s q" and ffd_remain: "\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> file_of_proc_fd s' p fd = Some f" and fflags_remain: "\<forall> p fd flags. flags_of_proc_fd s p fd = Some flags \<longrightarrow> flags_of_proc_fd s' p fd = Some flags" and sms_remain: "\<forall> q. q \<in> current_msgqs s \<longrightarrow> msgs_of_queue s' q = msgs_of_queue s q" (* and empty_remain: "\<forall> f. dir_is_empty s f \<longrightarrow> dir_is_empty s' f" *) and cfd2sfd: "\<forall> p fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd s' p fd = cfd2sfd s p fd" and nodel: "no_del_event (e # s)" and notin_cur: "notin_cur (e # s) obj'" shows "valid (e # s')"proof- from vd' have os: "os_grant s e" and grant: "grant s e" and vd: "valid s" by (auto dest:vt_grant_os vt_grant vd_cons) show ?thesis proof (cases e) case (Execve p f fds) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Execve) have f_in: "is_file s' f" using os alive apply (erule_tac x = "O_file f" in allE) by (auto simp:Execve) have fd_in: "fds \<subseteq> proc_file_fds s' p" using os alive ffd_remain by (auto simp:Execve proc_file_fds_def) have "os_grant s' e" using p_in f_in fd_in by (simp add:Execve) moreover have "grant s' e" proof- from grant obtain up rp tp uf rf tf where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" by (simp add:Execve split:option.splits, blast) with grant obtain pu nr nt where p3: "npctxt_execve (up, rp, tp) (uf, rf, tf) = Some (pu, nr, nt)" by (simp add:Execve split:option.splits del:npctxt_execve.simps, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits) from os have f_in': "is_file s f" by (simp add:Execve) from vd os have "\<exists> sf. cf2sfile s f = Some sf" by (auto dest!:is_file_in_current current_file_has_sfile simp:Execve) hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf apply (erule_tac x = f in allE) apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) apply (case_tac f, simp) apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) done have "inherit_fds_check s' (pu, nr, nt) p fds" proof- have "fds \<subseteq> proc_file_fds s' p" using os ffd_remain Execve by (auto simp:proc_file_fds_def) thus ?thesis using Execve grant vd cfd2sfd p1 p2 p3 os apply (rule_tac s = s in enrich_inherit_fds_check) by (simp_all split:option.splits) qed moreover have "search_check s' (pu, rp, tp) f" using p1 p2 p2' vd cf2sf f_in' grant Execve p3 f_in apply (rule_tac s = s in enrich_search_check) by (simp_all split:option.splits) ultimately show ?thesis using p1' p2' p3 apply (simp add:Execve split:option.splits) using grant Execve p1 p2 by (simp add:Execve grant p1 p2) qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Clone p p' fds) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Clone) have p'_not_in: "p' \<notin> current_procs s'" using alive' notin_cur os Clone apply (erule_tac x = "I_proc p'" in allE) apply (auto simp del:nums_of_recvmsg.simps) done have fd_in: "fds \<subseteq> proc_file_fds s' p" using os alive ffd_remain by (auto simp:Clone proc_file_fds_def) have "os_grant s' e" using p_in p'_not_in fd_in by (simp add:Clone) moreover have "grant s' e" proof- from grant obtain up rp tp where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" apply (simp add:Clone split:option.splits) by (case_tac a, auto) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Clone co2sobj.simps cp2sproc_def split:option.splits) have p2: "inherit_fds_check s' (up, rp, tp) p fds" proof- have "fds \<subseteq> proc_file_fds s' p" using os ffd_remain Clone by (auto simp:proc_file_fds_def) thus ?thesis using Clone grant vd cfd2sfd p1 os apply (rule_tac s = s in enrich_inherit_fds_check) by (simp_all split:option.splits) qed show ?thesis using p1 p2 p1' grant by (simp add:Clone) qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Kill p p') have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Kill) have p'_in: "p' \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p'" in allE) by (auto simp:Kill) have "os_grant s' e" using p_in p'_in by (simp add:Kill) moreover have "grant s' e" proof- from grant obtain up rp tp up' rp' tp' where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p'1: "sectxt_of_obj s (O_proc p') = Some (up', rp', tp')" apply (simp add:Kill split:option.splits) by (case_tac a, case_tac aa, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Kill co2sobj.simps cp2sproc_def split:option.splits) from p'1 have p'1': "sectxt_of_obj s' (O_proc p') = Some (up', rp', tp')" using os cp2sp apply (erule_tac x = p' in allE) by (auto simp:Kill co2sobj.simps cp2sproc_def split:option.splits) show ?thesis using p1 p'1 p1' p'1' grant by (simp add:Kill) qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Ptrace p p') have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Ptrace) have p'_in: "p' \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p'" in allE) by (auto simp:Ptrace) have "os_grant s' e" using p_in p'_in by (simp add:Ptrace) moreover have "grant s' e" proof- from grant obtain up rp tp up' rp' tp' where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p'1: "sectxt_of_obj s (O_proc p') = Some (up', rp', tp')" apply (simp add:Ptrace split:option.splits) by (case_tac a, case_tac aa, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Ptrace co2sobj.simps cp2sproc_def split:option.splits) from p'1 have p'1': "sectxt_of_obj s' (O_proc p') = Some (up', rp', tp')" using os cp2sp apply (erule_tac x = p' in allE) by (auto simp:Ptrace co2sobj.simps cp2sproc_def split:option.splits) show ?thesis using p1 p'1 p1' p'1' grant by (simp add:Ptrace) qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Exit p) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Exit) have "os_grant s' e" using p_in by (simp add:Exit) moreover have "grant s' e" by (simp add:Exit) ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Open p f flags fd opt) show ?thesis proof (cases opt) case None have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Open None) have f_in: "is_file s' f" using os alive apply (erule_tac x = "O_file f" in allE) by (auto simp:Open None) have fd_not_in: "fd \<notin> current_proc_fds s' p" using os alive' p_in notin_cur Open None apply (erule_tac x = "I_fd p fd" in allE) apply (case_tac obj', auto) done have "os_grant s' e" using p_in f_in fd_not_in os by (simp add:Open None) moreover have "grant s' e" proof- from grant obtain up rp tp uf rf tf where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" apply (simp add:Open None split:option.splits) by (case_tac a, case_tac aa, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Open None co2sobj.simps cp2sproc_def split:option.splits) from os have f_in': "is_file s f" by (simp add:Open None) from vd os have "\<exists> sf. cf2sfile s f = Some sf" by (auto dest!:is_file_in_current current_file_has_sfile simp:Open None) hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf apply (erule_tac x = f in allE) apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) apply (case_tac f, simp) apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) done have "search_check s' (up, rp, tp) f" using p1 p2 p2' vd cf2sf f_in' grant Open None f_in apply (rule_tac s = s in enrich_search_check) by (simp_all split:option.splits) thus ?thesis using p1' p2' apply (simp add:Open None split:option.splits) using grant Open None p1 p2 by simp qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Some inum) from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f = Some pf" by (auto simp:Open Some) have pf_in: "is_dir s' pf" using pf_in_s alive apply (erule_tac x = "O_dir pf" in allE) by simp have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Open Some) have f_not_in: "f \<notin> current_files s'" using os alive' Open Some notin_cur nodel apply (erule_tac x = "I_file f" in allE) by (case_tac obj', auto simp:current_files_simps) have fd_not_in: "fd \<notin> current_proc_fds s' p" using os alive' p_in Open Some notin_cur apply (erule_tac x = "I_fd p fd" in allE) apply (case_tac obj', auto) done have inum_not_in: "inum \<notin> current_inode_nums s'" using os alive' Open Some notin_cur nodel apply (erule_tac x = "I_inum inum" in allE) apply (case_tac obj', auto) apply (auto simp add:current_inode_nums_def current_file_inums_def split:if_splits) done have "os_grant s' e" using p_in pf_in parent f_not_in fd_not_in inum_not_in os by (simp add:Open Some hungs) moreover have "grant s' e" proof- from grant parent obtain up rp tp uf rf tf where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_dir pf) = Some (uf, rf, tf)" apply (simp add:Open Some split:option.splits) by (case_tac a, case_tac aa, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Open Some co2sobj.simps cp2sproc_def split:option.splits) from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf" by (auto dest!:is_dir_in_current current_file_has_sfile simp:Open Some) hence p2': "sectxt_of_obj s' (O_dir pf) = Some (uf, rf, tf)" using p2 cf2sf pf_in pf_in_s apply (erule_tac x = pf in allE) apply (erule exE, frule_tac s = s in is_dir_in_current, simp) apply (drule is_dir_not_file, drule is_dir_not_file) apply (auto simp:cf2sfile_def split:option.splits) apply (case_tac pf, simp_all) by (simp add:sroot_def root_sec_remains vd vs') have "search_check s' (up, rp, tp) pf" using p1 p2 p2' vd cf2sf pf_in grant Open Some pf_in_s parent vs' apply (rule_tac s = s in enrich_search_check') by (simp_all split:option.splits) thus ?thesis using p1' p2' parent apply (simp add:Open Some split:option.splits) using grant Open Some p1 p2 by simp qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) qed next case (ReadFile p fd) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:ReadFile) have fd_in: "fd \<in> current_proc_fds s' p" using os alive apply (erule_tac x = "O_fd p fd" in allE) by (auto simp:ReadFile) obtain f where ffd: "file_of_proc_fd s p fd = Some f" using os ReadFile by auto hence f_in_s: "is_file s f" using vd by (auto intro:file_of_pfd_is_file) obtain flags where fflag: "flags_of_proc_fd s p fd = Some flags" using os ReadFile by auto have ffd_in: "file_of_proc_fd s' p fd = Some f" using ffd_remain ffd by auto hence f_in: "is_file s' f" using vs' by (auto intro:file_of_pfd_is_file) have flags_in: "flags_of_proc_fd s' p fd = Some flags" using fflags_remain fflag by auto have "os_grant s' e" using p_in fd_in ffd_in flags_in fflag os f_in by (auto simp add:ReadFile is_file_in_current) moreover have "grant s' e" proof- from grant ffd obtain up rp tp uf rf tf ufd rfd tfd where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" and p3: "sectxt_of_obj s (O_fd p fd) = Some (ufd, rfd, tfd)" apply (simp add:ReadFile split:option.splits) by (case_tac a, case_tac aa, case_tac ab, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:ReadFile co2sobj.simps cp2sproc_def split:option.splits) from vd f_in_s have "\<exists> sf. cf2sfile s f = Some sf" by (auto dest!:is_file_in_current current_file_has_sfile) hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in_s p2 cf2sf apply (erule_tac x = f in allE) apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) apply (case_tac f, simp) apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) done have p3': "sectxt_of_obj s' (O_fd p fd) = Some (ufd, rfd, tfd)" using cfd2sfd ffd_in ffd p3 f_in f_in_s vd apply (erule_tac x = p in allE) apply (erule_tac x = fd in allE) apply (simp add:proc_file_fds_def) apply (auto simp:cfd2sfd_def fflag flags_in p3 split:option.splits dest!:current_file_has_sfile' simp:is_file_in_current) done show ?thesis using p1' p2' p3' ffd_in ffd apply (simp add:ReadFile split:option.splits) using grant p1 p2 p3 ReadFile by simp qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (WriteFile p fd) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:WriteFile) have fd_in: "fd \<in> current_proc_fds s' p" using os alive apply (erule_tac x = "O_fd p fd" in allE) by (auto simp:WriteFile) obtain f where ffd: "file_of_proc_fd s p fd = Some f" using os WriteFile by auto hence f_in_s: "is_file s f" using vd by (auto intro:file_of_pfd_is_file) obtain flags where fflag: "flags_of_proc_fd s p fd = Some flags" using os WriteFile by auto have ffd_in: "file_of_proc_fd s' p fd = Some f" using ffd_remain ffd by auto hence f_in: "is_file s' f" using vs' by (auto intro:file_of_pfd_is_file) have flags_in: "flags_of_proc_fd s' p fd = Some flags" using fflags_remain fflag by auto have "os_grant s' e" using p_in fd_in ffd_in flags_in fflag os f_in by (auto simp add:WriteFile is_file_in_current) moreover have "grant s' e" proof- from grant ffd obtain up rp tp uf rf tf ufd rfd tfd where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" and p3: "sectxt_of_obj s (O_fd p fd) = Some (ufd, rfd, tfd)" apply (simp add:WriteFile split:option.splits) by (case_tac a, case_tac aa, case_tac ab, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:WriteFile co2sobj.simps cp2sproc_def split:option.splits) from vd f_in_s have "\<exists> sf. cf2sfile s f = Some sf" by (auto dest!:is_file_in_current current_file_has_sfile) hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in_s p2 cf2sf apply (erule_tac x = f in allE) apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) apply (case_tac f, simp) apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) done have p3': "sectxt_of_obj s' (O_fd p fd) = Some (ufd, rfd, tfd)" using cfd2sfd ffd_in ffd p3 f_in f_in_s vd apply (erule_tac x = p in allE) apply (erule_tac x = fd in allE) apply (simp add:proc_file_fds_def) apply (auto simp:cfd2sfd_def fflag flags_in p3 split:option.splits dest!:current_file_has_sfile' simp:is_file_in_current) done show ?thesis using p1' p2' p3' ffd_in ffd apply (simp add:WriteFile split:option.splits) using grant p1 p2 p3 WriteFile by simp qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (CloseFd p fd) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:CloseFd) have fd_in: "fd \<in> current_proc_fds s' p" using os alive apply (erule_tac x = "O_fd p fd" in allE) by (auto simp:CloseFd) have "os_grant s' e" using p_in fd_in by (auto simp add:CloseFd) moreover have "grant s' e" by(simp add:CloseFd) ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (UnLink p f) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:UnLink) have f_in: "is_file s' f" using os alive apply (erule_tac x = "O_file f" in allE) by (auto simp:UnLink) from os vd obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f = Some pf" by (auto simp:UnLink dest!:file_has_parent) from pf_in_s alive have pf_in: "is_dir s' pf" apply (erule_tac x = "O_dir pf" in allE) by (auto simp:UnLink) have "os_grant s' e" using p_in f_in os by (simp add:UnLink hungs) moreover have "grant s' e" proof- from grant parent obtain up rp tp uf rf tf upf rpf tpf where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" apply (simp add:UnLink split:option.splits) by (case_tac a, case_tac aa, case_tac ab, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:UnLink co2sobj.simps cp2sproc_def split:option.splits) from vd os pf_in_s have "\<exists> sf. cf2sfile s f = Some sf" by (auto dest!:is_file_in_current current_file_has_sfile simp:UnLink) hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using p2 cf2sf f_in os parent apply (erule_tac x = f in allE) apply (erule exE, clarsimp simp:UnLink) apply (frule_tac s = s in is_file_in_current, simp) by (auto simp:cf2sfile_def split:option.splits) from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf" by (auto dest!:is_dir_in_current current_file_has_sfile simp:UnLink) hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s apply (erule_tac x = pf in allE) apply (erule exE, frule_tac s = s in is_dir_in_current, simp) apply (drule is_dir_not_file, drule is_dir_not_file) apply (auto simp:cf2sfile_def split:option.splits) apply (case_tac pf, simp_all) by (simp add:sroot_def root_sec_remains vd vs') have "search_check s' (up, rp, tp) f" using p1 p2 p2' vd cf2sf f_in grant UnLink os parent vs' apply (rule_tac s = s in enrich_search_check) by (simp_all split:option.splits) thus ?thesis using p1' p2' p3' parent apply (simp add:UnLink split:option.splits) using grant UnLink p1 p2 p3 by simp qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Rmdir p f) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Rmdir) have f_in: "is_dir s' f" using os alive apply (erule_tac x = "O_dir f" in allE) by (auto simp:Rmdir dir_is_empty_def) have not_root: "f \<noteq> []" using os by (auto simp:Rmdir) from os vd obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f = Some pf" apply (auto simp:Rmdir dir_is_empty_def) apply (case_tac f, simp+) apply (drule parentf_is_dir_prop1, auto) done from pf_in_s alive have pf_in: "is_dir s' pf" apply (erule_tac x = "O_dir pf" in allE) by (auto simp:Rmdir) have empty_in: "dir_is_empty s' f" using os Rmdir notin_cur apply (clarsimp simp add:dir_is_empty_def f_in) using alive' apply (erule_tac x = "I_file f'" in allE) apply simp apply (erule disjE) apply (erule_tac x = f' in allE, simp) apply (case_tac obj', simp_all) apply (clarsimp) apply (drule_tac f' = f in parent_ancen) apply (simp, rule notI, simp add:noJ_Anc) apply (case_tac "f = pf") using vd' Rmdir apply (simp_all add:is_dir_rmdir) apply (erule_tac x = pf in allE) apply (drule_tac f = pf in is_dir_in_current) apply (simp add:noJ_Anc) apply (clarsimp) apply (drule_tac f' = f in parent_ancen) apply (simp, rule notI, simp add:noJ_Anc) apply (case_tac "f = pf") using vd' Rmdir apply (simp_all add:is_dir_rmdir) apply (erule_tac x = pf in allE) apply (drule_tac f = pf in is_dir_in_current) apply (simp add:noJ_Anc) done have "os_grant s' e" using p_in f_in os empty_in by (simp add:Rmdir hungs) moreover have "grant s' e" proof- from grant parent obtain up rp tp uf rf tf upf rpf tpf where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_dir f) = Some (uf, rf, tf)" and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" apply (simp add:Rmdir split:option.splits) by (case_tac a, case_tac aa, case_tac ab, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Rmdir co2sobj.simps cp2sproc_def split:option.splits) from vd os pf_in_s have "\<exists> sf. cf2sfile s f = Some sf" by (auto dest!:is_dir_in_current current_file_has_sfile simp:dir_is_empty_def Rmdir) hence p2': "sectxt_of_obj s' (O_dir f) = Some (uf, rf, tf)" using p2 cf2sf f_in os parent apply (erule_tac x = f in allE) apply (erule exE, clarsimp simp:Rmdir dir_is_empty_def) apply (frule_tac s = s in is_dir_in_current, simp) apply (drule is_dir_not_file, drule is_dir_not_file) by (auto simp:cf2sfile_def split:option.splits) from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf" by (auto dest!:is_dir_in_current current_file_has_sfile simp:Rmdir) hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s apply (erule_tac x = pf in allE) apply (erule exE, frule_tac s = s in is_dir_in_current, simp) apply (drule is_dir_not_file, drule is_dir_not_file) apply (auto simp:cf2sfile_def split:option.splits) apply (case_tac pf, simp_all) by (simp add:sroot_def root_sec_remains vd vs') have "search_check s' (up, rp, tp) f" using p1 p2 p2' vd cf2sf f_in grant Rmdir os parent vs' apply (rule_tac s = s in enrich_search_check') by (simp_all add:dir_is_empty_def split:option.splits) thus ?thesis using p1' p2' p3' parent apply (simp add:Rmdir split:option.splits) using grant Rmdir p1 p2 p3 by simp qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Mkdir p f inum) from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f = Some pf" by (auto simp:Mkdir) have pf_in: "is_dir s' pf" using pf_in_s alive apply (erule_tac x = "O_dir pf" in allE) by simp have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Mkdir) have f_not_in: "f \<notin> current_files s'" using os alive' Mkdir notin_cur apply (erule_tac x = "I_file f" in allE) by (auto simp:current_files_simps) have inum_not_in: "inum \<notin> current_inode_nums s'" using os alive' Mkdir notin_cur apply (erule_tac x = "I_inum inum" in allE) apply (auto simp:current_inode_nums_def current_file_inums_def split:if_splits) done have "os_grant s' e" using p_in pf_in parent f_not_in os inum_not_in by (simp add:Mkdir hungs) moreover have "grant s' e" proof- from grant parent obtain up rp tp uf rf tf where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_dir pf) = Some (uf, rf, tf)" apply (simp add:Mkdir split:option.splits) by (case_tac a, case_tac aa, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Mkdir co2sobj.simps cp2sproc_def split:option.splits) from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf" by (auto dest!:is_dir_in_current current_file_has_sfile simp:Mkdir) hence p2': "sectxt_of_obj s' (O_dir pf) = Some (uf, rf, tf)" using p2 cf2sf pf_in pf_in_s apply (erule_tac x = pf in allE) apply (erule exE, frule_tac s = s in is_dir_in_current, simp) apply (drule is_dir_not_file, drule is_dir_not_file) apply (auto simp:cf2sfile_def split:option.splits) apply (case_tac pf, simp_all) by (simp add:sroot_def root_sec_remains vd vs') have "search_check s' (up, rp, tp) pf" using p1 p2 p2' vd cf2sf pf_in grant Mkdir pf_in_s parent vs' apply (rule_tac s = s in enrich_search_check') apply (simp_all split:option.splits) done thus ?thesis using p1' p2' parent apply (simp add:Mkdir split:option.splits) using grant Mkdir p1 p2 apply simp done qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (LinkHard p f f') from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f' = Some pf" by (auto simp:LinkHard) have pf_in: "is_dir s' pf" using pf_in_s alive apply (erule_tac x = "O_dir pf" in allE) by simp have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:LinkHard) have f'_not_in: "f' \<notin> current_files s'" using os alive' LinkHard notin_cur vd' apply (erule_tac x = "I_file f'" in allE) apply (auto simp:LinkHard current_files_simps) done have f_in: "is_file s' f" using os alive apply (erule_tac x = "O_file f" in allE) by (auto simp:LinkHard) have "os_grant s' e" using p_in pf_in parent os f_in f'_not_in by (simp add:LinkHard hungs) moreover have "grant s' e" proof- from grant parent obtain up rp tp uf rf tf upf rpf tpf where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" apply (simp add:LinkHard split:option.splits) by (case_tac a, case_tac aa, case_tac ab, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:LinkHard co2sobj.simps cp2sproc_def split:option.splits) from vd os pf_in_s have "\<exists> sf. cf2sfile s f = Some sf" by (auto dest!:is_file_in_current current_file_has_sfile simp:LinkHard) hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using p2 cf2sf f_in os parent apply (erule_tac x = f in allE) apply (erule exE, clarsimp simp:LinkHard) apply (frule_tac s = s in is_file_in_current, simp) apply (auto simp:cf2sfile_def split:option.splits) apply (case_tac f, simp) by (drule_tac s = s in root_is_dir', simp add:vd, simp+) from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf" by (auto dest!:is_dir_in_current current_file_has_sfile simp:LinkHard) hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s apply (erule_tac x = pf in allE) apply (erule exE, frule_tac s = s in is_dir_in_current, simp) apply (drule is_dir_not_file, drule is_dir_not_file) apply (auto simp:cf2sfile_def split:option.splits) apply (case_tac pf, simp_all) by (simp add:sroot_def root_sec_remains vd vs') have "search_check s' (up, rp, tp) f" using p1 p2 p2' vd cf2sf f_in grant LinkHard os parent vs' apply (rule_tac s = s in enrich_search_check) by (simp_all split:option.splits) moreover have "search_check s' (up, rp, tp) pf" using p1 p3 p3' vd cf2sf pf_in grant LinkHard os parent vs' apply (rule_tac s = s in enrich_search_check') apply (simp_all split:option.splits) done ultimately show ?thesis using p1' p2' p3' parent apply (simp add:LinkHard split:option.splits) using grant LinkHard p1 p2 p3 apply simp done qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (Truncate p f len) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Truncate) have f_in: "is_file s' f" using os alive apply (erule_tac x = "O_file f" in allE) by (auto simp:Truncate) have "os_grant s' e" using p_in f_in by (simp add:Truncate) moreover have "grant s' e" proof- from grant obtain up rp tp uf rf tf where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" apply (simp add:Truncate split:option.splits) by (case_tac a, case_tac aa, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Truncate co2sobj.simps cp2sproc_def split:option.splits) from os have f_in': "is_file s f" by (simp add:Truncate) from vd os have "\<exists> sf. cf2sfile s f = Some sf" by (auto dest!:is_file_in_current current_file_has_sfile simp:Truncate) hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf apply (erule_tac x = f in allE) apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) apply (case_tac f, simp) apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) done have "search_check s' (up, rp, tp) f" using p1 p2 p2' vd cf2sf f_in' grant Truncate f_in apply (rule_tac s = s in enrich_search_check) by (simp_all split:option.splits) thus ?thesis using p1' p2' apply (simp add:Truncate split:option.splits) using grant Truncate p1 p2 by (simp add:Truncate grant p1 p2) qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (CreateMsgq p q) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:CreateMsgq) have q_not_in: "q \<notin> current_msgqs s'" using os alive' CreateMsgq notin_cur nodel vd apply (erule_tac x = "I_msgq q" in allE) apply (auto split:t_enrich_obj.splits) apply (drule nums_of_recv_0, simp+) apply (drule new_msgq_1, simp+) done have "os_grant s' e" using p_in q_not_in by (simp add:CreateMsgq) moreover have "grant s' e" proof- from grant obtain up rp tp where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" apply (simp add:CreateMsgq split:option.splits) by (case_tac a, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:CreateMsgq co2sobj.simps cp2sproc_def split:option.splits) show ?thesis using p1' apply (simp add:CreateMsgq split:option.splits) using grant CreateMsgq p1 by simp qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (RemoveMsgq p q) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:RemoveMsgq) have q_in: "q \<in> current_msgqs s'" using os alive apply (erule_tac x = "O_msgq q" in allE) by (simp add:RemoveMsgq) have "os_grant s' e" using p_in q_in by (simp add:RemoveMsgq) moreover have "grant s' e" proof- from grant obtain up rp tp uq rq tq where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)" apply (simp add:RemoveMsgq split:option.splits) by (case_tac a, case_tac aa, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:RemoveMsgq co2sobj.simps cp2sproc_def split:option.splits) from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)" using os cq2sq vd apply (erule_tac x = q in allE) by (auto simp:RemoveMsgq co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits) show ?thesis using p1' p2' grant p1 p2 by (simp add:RemoveMsgq) qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (SendMsg p q m) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:SendMsg) have q_in: "q \<in> current_msgqs s'" using os alive apply (erule_tac x = "O_msgq q" in allE) by (simp add:SendMsg) have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_cur SendMsg q_in nodel vd apply (erule_tac x = "I_msg q m" in allE) apply (case_tac obj', auto) apply (drule nums_of_recv_0, simp+) apply (drule new_msgq_1, simp+) done have "os_grant s' e" using p_in q_in m_not_in sms_remain os by (simp add:SendMsg) moreover have "grant s' e" proof- from grant obtain up rp tp uq rq tq where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)" apply (simp add:SendMsg split:option.splits) by (case_tac a, case_tac aa, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:SendMsg co2sobj.simps cp2sproc_def split:option.splits) from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)" using os cq2sq vd apply (erule_tac x = q in allE) by (auto simp:SendMsg co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits) show ?thesis using p1' p2' grant p1 p2 by (simp add:SendMsg) qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (RecvMsg p q m) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:RecvMsg) have q_in: "q \<in> current_msgqs s'" using os alive apply (erule_tac x = "O_msgq q" in allE) by (simp add:RecvMsg) have m_in: "m = hd (msgs_of_queue s' q)" and sms_not_empty: "msgs_of_queue s' q \<noteq> []" using os sms_remain by (auto simp:RecvMsg) have "os_grant s' e" using p_in q_in m_in sms_not_empty os by (simp add:RecvMsg) moreover have "grant s' e" proof- from grant obtain up rp tp uq rq tq um rm tm where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)" and p3: "sectxt_of_obj s (O_msg q m) = Some (um, rm, tm)" apply (simp add:RecvMsg split:option.splits) by (case_tac a, case_tac aa, case_tac ab, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:RecvMsg co2sobj.simps cp2sproc_def split:option.splits) from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)" using os cq2sq vd apply (erule_tac x = q in allE) by (auto simp:RecvMsg co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits) from p3 have p3': "sectxt_of_obj s' (O_msg q m) = Some (um, rm, tm)" using sms_remain cq2sq vd os p2 p2' p3 apply (erule_tac x = q in allE) apply (erule_tac x = q in allE) apply (clarsimp simp:RecvMsg) apply (simp add:cq2smsgq_def split:option.splits if_splits) apply (drule current_has_sms', simp, simp) apply (case_tac "msgs_of_queue s q", simp) apply (simp add:cqm2sms.simps split:option.splits) apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1] done show ?thesis using p1' p2' p3' grant p1 p2 p3 by (simp add:RecvMsg) qed ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next case (CreateSock p af st fd inum) show ?thesis using grant by (simp add:CreateSock) next case (Bind p fd addr) show ?thesis using grant by (simp add:Bind) next case (Connect p fd addr) show ?thesis using grant by (simp add:Connect) next case (Listen p fd) show ?thesis using grant by (simp add:Listen) next case (Accept p fd addr port fd' inum) show ?thesis using grant by (simp add:Accept) next case (SendSock p fd) show ?thesis using grant by (simp add:SendSock) next case (RecvSock p fd) show ?thesis using grant by (simp add:RecvSock) next case (Shutdown p fd how) show ?thesis using grant by (simp add:Shutdown) qed qedlemma current_proc_fds_in_curp: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"apply (induct s)apply (simp add:init_fds_of_proc_prop1)apply (frule vt_grant_os, frule vd_cons)apply (case_tac a, auto split:if_splits option.splits)donelemma get_parentfs_ctxts_prop: "\<lbrakk>get_parentfs_ctxts s (a # f) = Some ctxts; sectxt_of_obj s (O_dir f) = Some ctxt; valid s\<rbrakk> \<Longrightarrow> ctxt \<in> set (ctxts)"apply (induct f)apply (auto split:option.splits)donelemma search_check_allp_intro: "\<lbrakk>search_check s sp pf; get_parentfs_ctxts s pf = Some ctxts; valid s; is_dir s pf\<rbrakk> \<Longrightarrow> search_check_allp sp (set ctxts)"apply (case_tac pf)apply (simp split:option.splits if_splits add:search_check_allp_def)apply (rule ballI)apply (auto simp:search_check_ctxt_def search_check_dir_def split:if_splits option.splits)apply (auto simp:search_check_allp_def search_check_file_def)apply (frule is_dir_not_file, simp)donelemma search_check_leveling_f: "\<lbrakk>search_check s sp pf; parent f = Some pf; is_file s f; valid s; sectxt_of_obj s (O_file f) = Some fctxt; search_check_file sp fctxt\<rbrakk> \<Longrightarrow> search_check s sp f"apply (case_tac f, simp+)apply (auto split:option.splits simp:search_check_ctxt_def)apply (frule parentf_is_dir_prop2, simp)apply (erule get_pfs_secs_prop, simp)apply (erule_tac search_check_allp_intro, simp_all)apply (simp add:parentf_is_dir_prop2)donelemma current_fflag_in_fds: "\<lbrakk>flags_of_proc_fd s p fd = Some flag; valid s\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p"apply (induct s arbitrary:p)apply (simp add:flags_of_proc_fd.simps file_of_proc_fd.simps init_oflags_prop2) apply (frule vd_cons, frule vt_grant_os, case_tac a)apply (auto split:if_splits option.splits dest:proc_fd_in_fds)donelemma current_fflag_has_ffd: "\<lbrakk>flags_of_proc_fd s p fd = Some flag; valid s\<rbrakk> \<Longrightarrow> \<exists> f. file_of_proc_fd s p fd = Some f"apply (induct s arbitrary:p)apply (simp add: file_of_proc_fd.simps init_fileflag_valid) apply (frule vd_cons, frule vt_grant_os, case_tac a)apply (auto split:if_splits option.splits dest:proc_fd_in_fds)donelemma oflags_check_remove_create: "oflags_check flags sp sf \<Longrightarrow> oflags_check (remove_create_flag flags) sp sf"apply (case_tac flags)apply (auto simp:oflags_check_def perms_of_flags_def perm_of_oflag_def split:bool.splits)donefun enrich_msgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msgq \<Rightarrow> t_state"where "enrich_msgq [] tq dq = []"| "enrich_msgq (CreateMsgq p q # s) tq dq = (if (tq = q) then (CreateMsgq p dq # CreateMsgq p q # s) else CreateMsgq p q # (enrich_msgq s tq dq))"| "enrich_msgq (SendMsg p q m # s) tq dq = (if (tq = q) then (SendMsg p dq m # SendMsg p q m # (enrich_msgq s tq dq)) else SendMsg p q m # (enrich_msgq s tq dq))"| "enrich_msgq (RecvMsg p q m # s) tq dq = (if (tq = q) then (RecvMsg p dq m # RecvMsg p q m # (enrich_msgq s tq dq)) else RecvMsg p q m # (enrich_msgq s tq dq))"| "enrich_msgq (e # s) tq dq = e # (enrich_msgq s tq dq)"lemma enrich_msgq_duq_in: "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> q' \<in> current_msgqs (enrich_msgq s q q')"apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply autodonelemma enrich_msgq_duq_sms: "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') q' = msgs_of_queue s q"apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply autodonelemma enrich_msgq_cur_inof: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"apply (induct s arbitrary:f, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply (auto split:option.splits)donelemma enrich_msgq_cur_inos: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"apply (rule ext)apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply (auto split:option.splits)donelemma enrich_msgq_cur_inos': "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"apply (simp add:enrich_msgq_cur_inos)donelemma enrich_msgq_cur_inums: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"apply (auto simp:current_inode_nums_def current_file_inums_def current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)donelemma enrich_msgq_cur_itag: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"apply (rule ext)apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply (auto split:option.splits t_socket_type.splits)donelemma enrich_msgq_cur_tcps: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"apply (rule ext)apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos split:option.splits t_inode_tag.splits)donelemma enrich_msgq_cur_udps: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"apply (rule ext)apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos split:option.splits t_inode_tag.splits)donelemma enrich_msgq_cur_msgqs: "\<lbrakk>q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons)apply (case_tac a, auto)donelemma enrich_msgq_cur_msgs: "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') = (msgs_of_queue s) (q' := msgs_of_queue s q)" apply (rule ext, simp, rule conjI, rule impI)apply (simp add:enrich_msgq_duq_sms)apply (rule impI) apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons)apply (case_tac a, auto)donelemma enrich_msgq_cur_procs: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons)apply (case_tac a, auto)donelemma enrich_msgq_cur_files: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"apply (auto simp:current_files_def)apply (simp add:enrich_msgq_cur_inof)+donelemma enrich_msgq_cur_fds: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply autodonelemma enrich_msgq_filefd: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"apply (rule ext, rule ext)apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply autodonelemma enrich_msgq_flagfd: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"apply (rule ext, rule ext)apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply autodonelemma enrich_msgq_proc_fds: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"apply (auto simp:proc_file_fds_def enrich_msgq_filefd)donelemma enrich_msgq_hungs: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> files_hung_by_del (enrich_msgq s q q') = files_hung_by_del s"apply (induct s, simp)apply (frule vt_grant_os, frule vd_cons, case_tac a)apply (auto simp:files_hung_by_del.simps)donelemma enrich_msgq_is_file: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"apply (rule ext)apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof split:option.splits t_inode_tag.splits)donelemma enrich_msgq_is_dir: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"apply (rule ext)apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof split:option.splits t_inode_tag.splits)donelemma enrich_msgq_sameinode: "\<lbrakk>no_del_event s; valid s\<rbrakk> \<Longrightarrow> (f \<in> same_inode_files (enrich_msgq s q q') f') = (f \<in> same_inode_files s f')"apply (induct s, simp)apply (simp add:same_inode_files_def)apply (auto simp:enrich_msgq_is_file enrich_msgq_cur_inof)donelemma enrich_msgq_tainted_aux1: "\<lbrakk>no_del_event s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}) \<subseteq> tainted (enrich_msgq s q q')"apply (induct s, simp) apply (frule vt_grant_os, frule vd_cons)apply (case_tac a)apply (auto split:option.splits if_splits dest:tainted_in_current simp:enrich_msgq_filefd enrich_msgq_sameinode)donelemma enrich_msgq_tainted_aux2: "\<lbrakk>no_del_event s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; valid s; valid (enrich_msgq s q q')\<rbrakk> \<Longrightarrow> tainted (enrich_msgq s q q') \<subseteq> (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s})"apply (induct s, simp) apply (frule vt_grant_os, frule vd_cons)apply (case_tac a)apply (auto split:option.splits if_splits simp:enrich_msgq_filefd enrich_msgq_sameinode dest:tainted_in_current vd_cons)apply (drule_tac vd_cons)+apply (simp)apply (drule set_mp)apply simpapply simpapply (drule_tac s = s in tainted_in_current)apply simp+donelemma enrich_msgq_alive: "\<lbrakk>alive s obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> alive (enrich_msgq s q q') obj"apply (case_tac obj)apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds enrich_msgq_cur_tcps enrich_msgq_cur_udps)apply (rule impI, simp)donelemma enrich_msgq_alive': "\<lbrakk>alive (enrich_msgq s q q') obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> alive s obj \<or> obj = O_msgq q' \<or> (\<exists> m. obj = O_msg q' m \<and> alive s (O_msg q m))"apply (case_tac obj)apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds enrich_msgq_cur_tcps enrich_msgq_cur_udps)apply (auto split:if_splits)donelemma enrich_msgq_not_alive: "\<lbrakk>enrich_not_alive s (E_msgq q') obj; q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> enrich_not_alive (enrich_msgq s q q') (E_msgq q') obj"apply (case_tac obj)apply (auto simp:enrich_msgq_cur_fds enrich_msgq_cur_files enrich_msgq_cur_procs enrich_msgq_cur_inums enrich_msgq_cur_msgqs enrich_msgq_cur_msgs)donelemma enrich_msgq_nodel: "no_del_event (enrich_msgq s q q') = no_del_event s"apply (induct s, simp)by (case_tac a, auto)lemma enrich_msgq_died_proc: "died (O_proc p) (enrich_msgq s q q') = died (O_proc p) s"apply (induct s, simp)by (case_tac a, auto)lemma cf2sfile_execve: "\<lbrakk>ff \<in> current_files (Execve p f fds # s); valid (Execve p f fds # s)\<rbrakk> \<Longrightarrow> cf2sfile (Execve p f fds # s) ff= cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemma cf2sfile_clone: "\<lbrakk>ff \<in> current_files (Clone p p' fds # s); valid (Clone p p' fds # s)\<rbrakk> \<Longrightarrow> cf2sfile (Clone p p' fds # s) ff= cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemma cf2sfile_ptrace: "\<lbrakk>ff \<in> current_files (Ptrace p p' # s); valid (Ptrace p p' # s)\<rbrakk> \<Longrightarrow> cf2sfile (Ptrace p p' # s) ff= cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemma cf2sfile_readfile: "\<lbrakk>ff \<in> current_files (ReadFile p fd # s); valid (ReadFile p fd # s)\<rbrakk> \<Longrightarrow> cf2sfile (ReadFile p fd # s) ff= cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemma cf2sfile_writefile: "\<lbrakk>ff \<in> current_files (WriteFile p fd # s); valid (WriteFile p fd # s)\<rbrakk> \<Longrightarrow> cf2sfile (WriteFile p fd # s) ff= cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemma cf2sfile_truncate: "\<lbrakk>ff \<in> current_files (Truncate p f len # s); valid (Truncate p f len # s)\<rbrakk> \<Longrightarrow> cf2sfile (Truncate p f len # s) ff= cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemma cf2sfile_createmsgq: "\<lbrakk>ff \<in> current_files (CreateMsgq p q # s); valid (CreateMsgq p q # s)\<rbrakk> \<Longrightarrow> cf2sfile (CreateMsgq p q # s) ff= cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemma cf2sfile_sendmsg: "\<lbrakk>ff \<in> current_files (SendMsg p q m # s); valid (SendMsg p q m # s)\<rbrakk> \<Longrightarrow> cf2sfile (SendMsg p q m # s) ff = cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemma cf2sfile_recvmsg: "\<lbrakk>ff \<in> current_files (RecvMsg p q m # s); valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cf2sfile (RecvMsg p q m # s) ff = cf2sfile s ff"by (auto dest:cf2sfile_other' simp:current_files_simps)lemmas cf2sfile_other'' = cf2sfile_recvmsg cf2sfile_sendmsg cf2sfile_createmsgq cf2sfile_truncate cf2sfile_writefile cf2sfile_readfile cf2sfile_ptrace cf2sfile_clone cf2sfile_execvelemma enrich_msgq_prop: "\<lbrakk>valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> valid (enrich_msgq s q q') \<and> (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \<and> (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and> (\<forall> tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and> (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and> (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q) \<and> (tainted (enrich_msgq s q q') = (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}))"proof (induct s) case Nil thus ?case by (auto)next case (Cons e s) hence vd_cons': "valid (e # s)" and curq_cons: "q \<in> current_msgqs (e # s)" and curq'_cons: "q' \<notin> current_msgqs (e # s)" and nodel_cons: "no_del_event (e # s)" and os: "os_grant s e" and grant: "grant s e" and vd: "valid s" by (auto dest:vd_cons vt_grant_os vt_grant) from curq'_cons nodel_cons have curq': "q' \<notin> current_msgqs s" by (case_tac e, auto) from nodel_cons have nodel: "no_del_event s" by (case_tac e, auto) from nodel curq' vd Cons have pre: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q') \<and> (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \<and> (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and> (\<forall>tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and> (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and> (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q) \<and> (tainted (enrich_msgq s q q') = (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}))" by auto from pre have pre_vd: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q')" by simp from pre have pre_sp: "\<And> tp. \<lbrakk>tp \<in> current_procs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp" by auto from pre have pre_sf: "\<And> f. \<lbrakk>f \<in> current_files s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" by auto from pre have pre_sq: "\<And> tq. \<lbrakk>tq \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq" by auto from pre have pre_sfd: "\<And> tp fd. \<lbrakk>fd \<in> proc_file_fds s tp; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by auto hence pre_sfd': "\<And> tp fd f. \<lbrakk>file_of_proc_fd s tp fd = Some f; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def) from pre have pre_duq: "q \<in> current_msgqs s \<Longrightarrow> cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q" by auto have vd_enrich:"q \<in> current_msgqs s \<Longrightarrow> valid (e # enrich_msgq s q q')" apply (frule pre_vd) apply (erule_tac s = s and obj' = "E_msgq q'" in enrich_valid_intro_cons) apply (simp_all add:pre nodel nodel_cons curq_cons vd_cons' vd enrich_msgq_hungs) apply (clarsimp simp:nodel vd curq' enrich_msgq_alive) apply (rule allI, rule impI, erule enrich_msgq_not_alive) apply (simp_all add:curq' curq'_cons nodel vd enrich_msgq_cur_msgs enrich_msgq_filefd enrich_msgq_flagfd) done have q_neq_q': "q' \<noteq> q" using curq'_cons curq_cons by auto have vd_enrich_cons: "valid (enrich_msgq (e # s) q q')" proof- have "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow> valid (enrich_msgq (e # s) q q')" proof- fix p q'' assume ev: "e = CreateMsgq p q''" show "valid (enrich_msgq (e # s) q q')" proof (cases "q'' = q") case False with ev vd_enrich curq_cons show ?thesis by simp next case True have "os_grant (CreateMsgq p q # s) (CreateMsgq p q')" using os ev by (simp add:q_neq_q' curq') moreover have "grant (CreateMsgq p q # s) (CreateMsgq p q')" using grant ev by (auto simp add:sectxt_of_obj_def split:option.splits) ultimately show ?thesis using ev vd_cons' True by (auto intro: valid.intros(2)) qed qed moreover have "\<And> p q'' m. \<lbrakk>e = SendMsg p q'' m; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> valid (enrich_msgq (e # s) q q')" proof- fix p q'' m assume ev: "e = SendMsg p q'' m" and q_in: "q \<in> current_msgqs s" show "valid (enrich_msgq (e # s) q q')" proof (cases "q'' = q") case False with ev vd_enrich q_in show ?thesis by simp next case True from grant os ev True obtain psec qsec where psec: "sectxt_of_obj s (O_proc p) = Some psec" and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec" by (auto split:option.splits) from psec q_in os ev have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec" by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits) from qsec q_in pre_duq vd have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec" by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd curq' psec psec' qsec qsec' grant os q_neq_q' apply (simp, erule_tac valid.intros(2)) apply (auto simp:q_neq_q' enrich_msgq_cur_msgqs enrich_msgq_cur_procs enrich_msgq_cur_msgs sectxt_of_obj_simps) done qed qed moreover have "\<And> p q'' m. \<lbrakk>e = RecvMsg p q'' m; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> valid (enrich_msgq (e # s) q q')" proof- fix p q'' m assume ev: "e = RecvMsg p q'' m" and q_in: "q \<in> current_msgqs s" show "valid (enrich_msgq (e # s) q q')" proof (cases "q'' = q") case False with ev vd_enrich q_in show ?thesis by simp next case True from grant os ev True obtain psec qsec msec where psec: "sectxt_of_obj s (O_proc p) = Some psec" and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec" and msec: "sectxt_of_obj s (O_msg q (hd (msgs_of_queue s q))) = Some msec" by (auto split:option.splits) from psec q_in os ev have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec" by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits) from qsec q_in pre_duq vd have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec" by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') from qsec q_in vd have qsec'': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q) = Some qsec" apply (frule_tac pre_sq, simp_all) by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') from msec q_in pre_duq vd qsec qsec' qsec'' curq' nodel have msec': "sectxt_of_obj (enrich_msgq s q q') (O_msg q' (hd (msgs_of_queue s q))) = Some msec" apply (auto simp:cq2smsgq_def enrich_msgq_cur_msgs split:option.splits dest!:current_has_sms') apply (case_tac "msgs_of_queue s q") using os ev True apply simp apply (simp add:cqm2sms.simps split:option.splits) apply (auto simp:cm2smsg_def split:option.splits) done show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd curq' grant os q_neq_q' psec psec' msec msec' qsec qsec' apply (simp, erule_tac valid.intros(2)) apply (auto simp:enrich_msgq_cur_msgqs enrich_msgq_cur_procs enrich_msgq_cur_msgs sectxt_of_obj_simps) done qed qed ultimately show ?thesis using vd_enrich curq_cons vd_cons' apply (case_tac e) apply (auto simp del:enrich_msgq.simps) apply (auto split:if_splits ) done qed have curpsec: "\<And> tp. \<lbrakk>tp \<in> current_procs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> sectxt_of_obj (enrich_msgq s q q') (O_proc tp) = sectxt_of_obj s (O_proc tp)" using pre_vd vd apply (frule_tac pre_sp, simp) by (auto simp:cp2sproc_def split:option.splits if_splits dest!:current_has_sec') have curfsec: "\<And> f. \<lbrakk>is_file s f; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)" proof- fix f assume a1: "is_file s f" and a2: "q \<in> current_msgqs s" from a2 pre_sf pre_vd have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" and vd_enrich: "valid (enrich_msgq s q q')" by auto hence csf: "cf2sfile (enrich_msgq s q q') f = cf2sfile s f" using a1 by (auto simp:is_file_in_current) from a1 obtain sf where csf_some: "cf2sfile s f = Some sf" apply (case_tac "cf2sfile s f") apply (drule current_file_has_sfile') apply (simp add:vd, simp add:is_file_in_current, simp) done from a1 have a1': "is_file (enrich_msgq s q q') f" using vd nodel by (simp add:enrich_msgq_is_file) show "sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)" using csf csf_some vd_enrich vd a1 a1' apply (auto simp:cf2sfile_def split:option.splits if_splits) apply (case_tac f, simp_all) apply (drule root_is_dir', simp+) done qed have curdsec: "\<And> tf. \<lbrakk>is_dir s tf; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)" proof- fix tf assume a1: "is_dir s tf" and a2: "q \<in> current_msgqs s" from a2 pre_sf pre_vd have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" and vd_enrich: "valid (enrich_msgq s q q')" by auto hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf" using a1 by (auto simp:is_dir_in_current) from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf" apply (case_tac "cf2sfile s tf") apply (drule current_file_has_sfile') apply (simp add:vd, simp add:is_dir_in_current, simp) done from a1 have a1': "is_dir (enrich_msgq s q q') tf" using enrich_msgq_is_dir vd nodel by simp from a1 have a3: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file) from a1' vd have a3': "\<not> is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file) show "sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)" using csf csf_some a3 a3' vd_enrich vd apply (auto simp:cf2sfile_def split:option.splits) apply (case_tac tf) apply (simp add:root_sec_remains, simp) done qed have curpsecs: "\<And> tf ctxts'. \<lbrakk>is_dir s tf; q \<in> current_msgqs s; get_parentfs_ctxts s tf = Some ctxts'\<rbrakk> \<Longrightarrow> \<exists> ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \<and> set ctxts = set ctxts'" proof- fix tf ctxts' assume a1: "is_dir s tf" and a2: "q \<in> current_msgqs s" and a4: "get_parentfs_ctxts s tf = Some ctxts'" from a2 pre have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" and vd_enrich': "valid (enrich_msgq s q q')" by auto hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf" using a1 by (auto simp:is_dir_in_current) from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf" apply (case_tac "cf2sfile s tf") apply (drule current_file_has_sfile') apply (simp add:vd, simp add:is_dir_in_current, simp) done from a1 have a1': "is_dir (enrich_msgq s q q') tf" using enrich_msgq_is_dir vd nodel by simp from a1 have a5: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file) from a1' vd have a5': "\<not> is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file) from a1' pre_vd a2 obtain ctxts where a3: "get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts" apply (case_tac "get_parentfs_ctxts (enrich_msgq s q q') tf") apply (drule get_pfs_secs_prop', simp+) done moreover have "set ctxts = set ctxts'" proof (cases tf) case Nil with a3 a4 vd vd_enrich' show ?thesis by (simp add:get_parentfs_ctxts.simps root_sec_remains split:option.splits) next case (Cons a ff) with csf csf_some a5 a5' vd_enrich' vd a3 a4 show ?thesis apply (auto simp:cf2sfile_def split:option.splits if_splits) done qed ultimately show "\<exists> ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \<and> set ctxts = set ctxts'" by auto qed have psec_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> sectxt_of_obj (enrich_msgq (e # s) q q') (O_proc tp) = sectxt_of_obj (e # s) (O_proc tp)" using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd apply (case_tac e) apply (auto intro:curpsec simp:sectxt_of_obj_simps) apply (frule curpsec, simp, frule curfsec, simp) apply (auto split:option.splits)[1] apply (frule vd_cons) defer apply (frule vd_cons) apply (auto intro:curpsec simp:sectxt_of_obj_simps) done have sf_cons: "\<And> f. f \<in> current_files (e # s) \<Longrightarrow> cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" proof- fix f assume a1: "f \<in> current_files (e # s)" hence a1': "f \<in> current_files (enrich_msgq (e # s) q q')" using nodel_cons os vd vd_cons' vd_enrich_cons apply (case_tac e) apply (auto simp:current_files_simps enrich_msgq_cur_files dest:is_file_in_current split:option.splits) done have b1: "\<And> p f' flags fd opt. e = Open p f' flags fd opt \<Longrightarrow> cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" proof- fix p f' flags fd opt assume ev: "e = Open p f' flags fd opt" show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" proof (cases opt) case None with a1 a1' ev vd_cons' vd_enrich_cons curq_cons show ?thesis apply (simp add:cf2sfile_open_none) apply (simp add:pre_sf current_files_simps) done next case (Some inum) show ?thesis proof (cases "f = f'") case False with a1 a1' ev vd_cons' vd_enrich_cons curq_cons Some show ?thesis apply (simp add:cf2sfile_open) apply (simp add:pre_sf current_files_simps) done next case True with vd_cons' ev os Some obtain pf where pf: "parent f = Some pf" by auto then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" using os vd ev Some True apply (case_tac "get_parentfs_ctxts s pf") apply (drule get_pfs_secs_prop', simp, simp) apply auto done have "sectxt_of_obj (Open p f' flags fd (Some inum) # enrich_msgq s q q') (O_file f') = sectxt_of_obj (Open p f' flags fd (Some inum) # s) (O_file f')" using Some vd_enrich_cons vd_cons' ev pf True os curq_cons by (simp add:sectxt_of_obj_simps curpsec curdsec) moreover have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" using curq_cons ev pf Some True os by (simp add:curdsec) moreover have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts" using curq_cons ev pf Some True os vd psecs apply (case_tac "get_parentfs_ctxts s pf") apply (drule get_pfs_secs_prop', simp+) apply (rule curpsecs, simp+) done then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" and psecs_eq: "set ctxts' = set ctxts" by auto ultimately show ?thesis using a1 a1' ev vd_cons' vd_enrich_cons Some True pf psecs by (simp add:cf2sfile_open split:option.splits) qed qed qed have b2: "\<And> p f' inum. e = Mkdir p f' inum \<Longrightarrow> cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" proof- fix p f' inum assume ev: "e = Mkdir p f' inum" show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" proof (cases "f' = f") case False with a1 a1' ev vd_cons' vd_enrich_cons curq_cons show ?thesis apply (simp add:cf2sfile_mkdir) apply (simp add:pre_sf current_files_simps) done next case True with vd_cons' ev os obtain pf where pf: "parent f = Some pf" by auto then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" using os vd ev True apply (case_tac "get_parentfs_ctxts s pf") apply (drule get_pfs_secs_prop', simp, simp) apply auto done have "sectxt_of_obj (Mkdir p f' inum # enrich_msgq s q q') (O_dir f') = sectxt_of_obj (Mkdir p f' inum # s) (O_dir f')" using vd_enrich_cons vd_cons' ev pf True os curq_cons by (simp add:sectxt_of_obj_simps curpsec curdsec) moreover have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" using curq_cons ev pf True os by (simp add:curdsec) moreover have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts" using curq_cons ev pf True os vd psecs apply (case_tac "get_parentfs_ctxts s pf") apply (drule get_pfs_secs_prop', simp+) apply (rule curpsecs, simp+) done then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" and psecs_eq: "set ctxts' = set ctxts" by auto ultimately show ?thesis using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs apply (simp add:cf2sfile_mkdir split:option.splits) done qed qed have b3: "\<And> p f' f''. e = LinkHard p f' f'' \<Longrightarrow> cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" proof- fix p f' f'' assume ev: "e = LinkHard p f' f''" show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" proof (cases "f'' = f") case False with a1 a1' ev vd_cons' vd_enrich_cons curq_cons show ?thesis apply (simp add:cf2sfile_linkhard) apply (simp add:pre_sf current_files_simps) done next case True with vd_cons' ev os obtain pf where pf: "parent f = Some pf" by auto then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" using os vd ev True apply (case_tac "get_parentfs_ctxts s pf") apply (drule get_pfs_secs_prop', simp, simp) apply auto done have "sectxt_of_obj (LinkHard p f' f'' # enrich_msgq s q q') (O_file f) = sectxt_of_obj (LinkHard p f' f'' # s) (O_file f)" using vd_enrich_cons vd_cons' ev pf True os curq_cons by (simp add:sectxt_of_obj_simps curpsec curdsec) moreover have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" using curq_cons ev pf True os by (simp add:curdsec) moreover have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts" using curq_cons ev pf True os vd psecs apply (case_tac "get_parentfs_ctxts s pf") apply (drule get_pfs_secs_prop', simp+) apply (rule curpsecs, simp+) done then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" and psecs_eq: "set ctxts' = set ctxts" by auto ultimately show ?thesis using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs apply (simp add:cf2sfile_linkhard split:option.splits) done qed qed show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" apply (case_tac e) prefer 6 apply (erule b1) prefer 11 apply (erule b2) prefer 11 apply (erule b3) apply (simp_all only:b1 b2 b3) using a1' a1 vd_enrich_cons vd_cons' curq_cons nodel_cons apply (simp_all add:cf2sfile_other'' cf2sfile_simps enrich_msgq.simps no_del_event.simps split:if_splits) apply (simp_all add:pre_sf cf2sfile_other' current_files_simps split:if_splits) apply (drule vd_cons, simp add:cf2sfile_other', drule pre_sf, simp+)+ done qed have sfd_cons:"\<And> tp fd f. file_of_proc_fd (e # s) tp fd = Some f \<Longrightarrow> cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" proof- fix tp fd f assume a1: "file_of_proc_fd (e # s) tp fd = Some f" hence a1': "file_of_proc_fd (enrich_msgq (e # s) q q') tp fd = Some f" using nodel_cons vd_enrich os vd_cons' apply (case_tac e, auto simp:enrich_msgq_filefd simp del:enrich_msgq.simps) done have b1: "\<And> p f' flags fd' opt. e = Open p f' flags fd' opt \<Longrightarrow> cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" proof- fix p f' flags fd' opt assume ev: "e = Open p f' flags fd' opt" have c1': "file_of_proc_fd (Open p f' flags fd' opt # s) tp fd = Some f" using a1' ev a1 by (simp split:if_splits) show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" thm cfd2sfd_open proof (cases "tp = p \<and> fd = fd'") case False show ?thesis using ev vd_enrich_cons vd_cons' a1' a1 False curq_cons apply (simp add:cfd2sfd_open split:if_splits del:file_of_proc_fd.simps) apply (rule conjI, rule impI, simp) apply (rule conjI, rule impI, simp) apply (auto simp: False intro!:pre_sfd' split:if_splits) done next case True have "f' \<in> current_files (Open p f' flags fd' opt # s)" using ev vd_cons' os by (auto simp:current_files_simps is_file_in_current split:option.splits) hence "cf2sfile (Open p f' flags fd' opt # enrich_msgq s q q') f' = cf2sfile (Open p f' flags fd' opt # s) f'" using sf_cons ev by auto moreover have "sectxt_of_obj (enrich_msgq s q q') (O_proc p) = sectxt_of_obj s (O_proc p)" apply (rule curpsec) using os ev curq_cons by (auto split:option.splits) ultimately show ?thesis using ev True a1 a1' vd_enrich_cons vd_cons' apply (simp add:cfd2sfd_open sectxt_of_obj_simps del:file_of_proc_fd.simps) done qed qed show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" apply (case_tac e) prefer 6 apply (erule b1) using a1' a1 vd_enrich_cons vd_cons' curq_cons apply (simp_all only:cfd2sfd_simps enrich_msgq.simps) apply (auto simp:cfd2sfd_simps pre_sfd' dest:vd_cons cfd2sfd_other split:if_splits) done qed have pfds_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> cpfd2sfds (enrich_msgq (e # s) q q') tp = cpfd2sfds (e # s) tp" apply (auto simp add:cpfd2sfds_def proc_file_fds_def) apply (rule_tac x = fd in exI, rule conjI, rule_tac x = f in exI) prefer 3 apply (rule_tac x = fd in exI, rule conjI, rule_tac x = f in exI) apply (auto simp:sfd_cons enrich_msgq_filefd nodel_cons vd_cons') done have tainted_cons: "tainted (enrich_msgq (e # s) q q') = (tainted (e # s) \<union> {O_msg q' m | m. O_msg q m \<in> tainted (e # s)})" apply (rule equalityI) using nodel_cons curq_cons curq'_cons vd_cons' vd_enrich_cons apply (rule enrich_msgq_tainted_aux2) using nodel_cons curq_cons curq'_cons vd_cons' apply (rule enrich_msgq_tainted_aux1) done have pre_tainted: "q \<in> current_msgqs s \<Longrightarrow> tainted (enrich_msgq s q q') = (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s})" by (simp add:pre) have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" by (auto simp:proc_file_fds_def elim!:sfd_cons) moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_msgq (e # s) q q') tp = cp2sproc (e # s) tp" by (auto simp:cp2sproc_def pfds_cons psec_cons enrich_msgq_died_proc split:option.splits) moreover have "\<forall>tq. tq \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq" proof clarify fix tq assume a1: "tq \<in> current_msgqs (e # s)" have curqsec: "\<And> tq. \<lbrakk>tq \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> sectxt_of_obj (enrich_msgq s q q') (O_msgq tq) = sectxt_of_obj s (O_msgq tq)" using pre_vd vd apply (frule_tac pre_sq, simp) by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms') have cursms: "\<And> q''. \<lbrakk>q'' \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> cqm2sms (enrich_msgq s q q') q'' (msgs_of_queue (enrich_msgq s q q') q'') = cqm2sms s q'' (msgs_of_queue s q'')" using pre_vd vd apply (frule_tac pre_sq, simp) by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms') have qsec_cons: "sectxt_of_obj (enrich_msgq (e # s) q q') (O_msgq tq) = sectxt_of_obj (e # s) (O_msgq tq)" using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons curq_cons a1 apply (case_tac e) apply (auto intro:curqsec simp:sectxt_of_obj_simps curpsec split:option.splits dest!:current_has_sec') apply (frule vd_cons) defer apply (frule vd_cons) apply (auto intro:curqsec simp:sectxt_of_obj_simps) done have sms_cons: "cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" proof- have b1: "\<And> p q'' m. e = SendMsg p q'' m \<Longrightarrow> cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" apply (case_tac e) using a1 curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms pre_tainted split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*}) apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms pre_tainted split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) done have b2: "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow> cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" using a1 curq_cons curq'_cons vd_enrich_cons vd_cons' apply (auto simp:cqm2sms_simps intro:cursms) apply (auto simp:cqm2sms.simps) done have b3: "\<And> p q'' m. e = RecvMsg p q'' m \<Longrightarrow> cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" using a1 curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) apply (frule vd_cons) defer apply (frule vd_cons) apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) done show "cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" apply (case_tac e) prefer 15 apply (erule b2) prefer 15 apply (erule b1) prefer 15 apply (erule b3) using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons a1 apply (auto intro:cursms simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) done qed show "cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq" using a1 curq_cons apply (simp add:cq2smsgq_def qsec_cons sms_cons) done qed moreover have "cq2smsgq (enrich_msgq (e # s) q q') q' = cq2smsgq (e # s) q" proof- have duqsec: "q \<in> current_msgqs s \<Longrightarrow> sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = sectxt_of_obj s (O_msgq q)" apply (frule pre_duq) using vd by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms') have duqsms: "q \<in> current_msgqs s \<Longrightarrow> cqm2sms (enrich_msgq s q q') q' (msgs_of_queue (enrich_msgq s q q') q') = cqm2sms s q (msgs_of_queue s q)" apply (frule pre_duq) using vd by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms') have qsec_cons: "sectxt_of_obj (enrich_msgq (e # s) q q') (O_msgq q') = sectxt_of_obj (e # s) (O_msgq q)" using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons curq_cons apply (case_tac e) apply (auto simp:duqsec sectxt_of_obj_simps curpsec split:option.splits dest!:current_has_sec') apply (frule vd_cons) defer apply (frule vd_cons) apply (auto intro:duqsec simp:sectxt_of_obj_simps) done have sms_cons: "cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') = cqm2sms (e # s) q (msgs_of_queue (e # s) q)" proof- have b1: "\<And> p q'' m. e = SendMsg p q'' m \<Longrightarrow> cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') = cqm2sms (e # s) q (msgs_of_queue (e # s) q)" apply (case_tac e) using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted enrich_msgq_cur_procs enrich_msgq_cur_msgqs split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*}) apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted enrich_msgq_cur_procs enrich_msgq_cur_msgqs dest:tainted_in_current split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) done have b2: "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow> cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') = cqm2sms (e # s) q (msgs_of_queue (e # s) q)" using curq_cons curq'_cons vd_enrich_cons vd_cons' apply (auto simp:cqm2sms_simps intro:duqsms) apply (auto simp:cqm2sms.simps) done have b3: "\<And> p q'' m. e = RecvMsg p q'' m \<Longrightarrow> cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') = cqm2sms (e # s) q (msgs_of_queue (e # s) q)" using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted enrich_msgq_cur_procs enrich_msgq_cur_msgqs split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*}) apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted enrich_msgq_cur_procs enrich_msgq_cur_msgqs dest:tainted_in_current split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) done show ?thesis apply (case_tac e) prefer 15 apply (erule b2) prefer 15 apply (erule b1) prefer 15 apply (erule b3) using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons apply (auto intro:duqsms simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsms split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) done qed show ?thesis using curq_cons apply (simp add:cq2smsgq_def qsec_cons sms_cons) done qed ultimately show ?case using vd_enrich_cons sf_cons tainted_cons by autoqedlemma enrich_msgq_vd: "\<lbrakk>q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> valid (enrich_msgq s q q')"by (auto dest:enrich_msgq_prop)lemma enrich_msgq_sp: "\<lbrakk>tp \<in> current_procs s; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp"by (auto dest:enrich_msgq_prop)lemma enrich_msgq_sf: "\<lbrakk>f \<in> current_files s; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f"by (auto dest:enrich_msgq_prop)lemma enrich_msgq_sfs: "\<lbrakk>is_file s f; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> cf2sfiles (enrich_msgq s q q') f = cf2sfiles s f"apply (auto simp add:cf2sfiles_def)apply (rule_tac x = f' in bexI) deferapply (simp add:enrich_msgq_sameinode)apply (rule_tac x = f' in bexI) deferapply (simp add:enrich_msgq_sameinode)+apply (drule same_inode_files_prop11, drule_tac f = f' in is_file_in_current)apply (simp add:enrich_msgq_sf)apply (drule same_inode_files_prop11, drule_tac f = f' in is_file_in_current)apply (simp add:enrich_msgq_sf)donelemma enrich_msgq_sq: "\<lbrakk>tq \<in> current_msgqs s; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq"by (auto dest:enrich_msgq_prop)lemma enrich_msgq_sfd': "\<lbrakk>fd \<in> proc_file_fds s tp; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd"by (auto dest:enrich_msgq_prop)lemma enrich_msgq_sfd: "\<lbrakk>file_of_proc_fd s tp fd = Some f; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd"by (auto intro:enrich_msgq_sfd' simp:proc_file_fds_def)lemma enrich_msgq_duq: "\<lbrakk>valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q"by (auto dest:enrich_msgq_prop)lemma enrich_msgq_tainted: "\<lbrakk>valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> \<Longrightarrow> tainted (enrich_msgq s q q') = (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s})"by (auto dest:enrich_msgq_prop)lemma enrich_msgq_dalive: "\<lbrakk>q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> dalive (enrich_msgq s q q') obj = (dalive s obj \<or> obj = D_msgq q')"apply (case_tac obj)apply (auto simp:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs enrich_msgq_cur_procs)donelemma enrich_msgq_s2ss: "\<lbrakk>q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> s2ss (enrich_msgq s q q') = s2ss s"apply (auto simp add:s2ss_def)apply (simp add:enrich_msgq_dalive)apply (erule disjE)apply (rule_tac x = obj in exI) defer apply (rule_tac x = "D_msgq q" in exI) defer apply (rule_tac x = obj in exI) apply (case_tac[!] obj)apply (auto simp:enrich_msgq_duq enrich_msgq_tainted enrich_msgq_sq enrich_msgq_sf enrich_msgq_sp co2sobj.simps enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_procs enrich_msgq_cur_msgqs enrich_msgq_sfs split:option.splits dest:is_dir_in_current)doneendend