selinux: comparison simple_selinux/Co2sobj

equal deleted inserted replaced

-:271e9818b6f6
+:99af1986e1e0
 "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m; \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk>
 \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
 unfolding cm2smsg_def
 apply (case_tac e)
-apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted
+apply (auto simp:sectxt_of_obj_simps
 split:t_object.splits option.splits if_splits
 dest:not_deleted_init_msg  dest!:current_has_sec')
 done
 lemma cm2smsg_sendmsg:
 then (case (sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of
 Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))
 | _ \<Rightarrow> None)
 else cm2smsg s q' m') "
 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
 split:if_splits option.splits
 dest:not_deleted_init_msg  dest!:current_has_sec')
 done
 lemma cm2smsg_recvmsg1:
 "\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"
 apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
 split:if_splits option.splits)
 done
 lemma cm2smsg_recvmsg2:
 "\<lbrakk>m' \<noteq> m; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"
 apply (frule vd_cons, frule vt_grant_os)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
 split:if_splits option.splits)
 done
 lemma cm2smsg_recvmsg1':
 "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"
 apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
 split:if_splits option.splits)
 done
 lemma cm2smsg_recvmsg2':
 "\<lbrakk>valid (RecvMsg p q m # s); m' \<noteq> m\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"
 apply (frule vd_cons, frule vt_grant_os)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
 split:if_splits option.splits)
 done
 lemma cm2smsg_removemsgq:
 "\<lbrakk>q' \<noteq> q; valid (RemoveMsgq p q # s)\<rbrakk> \<Longrightarrow> cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'"
 apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
 split:if_splits option.splits)
 done
 lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
 cm2smsg_removemsgq cm2smsg_other
 apply (rule_tac m = m and q = q and qi = qi and qsec = qsec in p1, simp+)
 apply (case_tac "q = nat2", simp)
 apply (drule cq2smsg_createmsgq, simp, simp)
 apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)
+apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)
 apply (simp add:cq2smsgq_def split:option.splits)
 apply (rule_tac m = m and sm = sm in cqm2sms_prop0, simp+)
 apply (simp add:cqm2sms_recvmsg)
 done
 apply (case_tac "f = f'")
 apply (simp add:cf2sfile_mkdir4 split:option.splits)
 apply (simp add:cf2sfile_mkdir1 current_files_simps)
 done
-lemma cf2sfile_linkhard1:
-"\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk>
-\<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
-apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
-apply (case_tac "f = f'", simp)
-apply (induct f', simp add:sroot_only, simp)
-apply (frule parentf_in_current', simp+)
-apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
-get_parentfs_ctxts_simps split:if_splits option.splits)
-done
-lemma cf2sfile_linkhard2:
-"\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk>
-\<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"
-apply (frule vd_cons, drule is_file_in_current)
-by (simp add:cf2sfile_linkhard1)
-lemma cf2sfile_linkhard3:
-"\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk>
-\<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"
-apply (frule vd_cons, drule is_dir_in_current)
-by (simp add:cf2sfile_linkhard1)
-lemma cf2sfile_linkhard4:
-"valid (LinkHard p oldf f # s)
-\<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of
-Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf),
-get_parentfs_ctxts s pf) of
-(Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
-| _ \<Rightarrow> None)
-| None \<Rightarrow> None)"
-apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
-apply (case_tac f, simp)
-apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
-get_parentfs_ctxts_simps)
-apply (rule impI, (erule conjE)+)
-apply (drule not_deleted_init_file, simp+)
-apply (simp add:is_file_in_current)
-done
-lemma cf2sfile_linkhard:
-"\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk>
-\<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = (
-if (f' = f)
-then (case (parent f) of
-Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf),
-get_parentfs_ctxts s pf) of
-(Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
-| _ \<Rightarrow> None)
-| None \<Rightarrow> None)
-else cf2sfile s f')"
-apply (case_tac "f = f'")
-apply (simp add:cf2sfile_linkhard4 split:option.splits)
-apply (simp add:cf2sfile_linkhard1 current_files_simps)
-done
 lemma cf2sfile_other:
 "\<lbrakk>ff \<in> current_files s;
 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
 \<forall> p fd. e \<noteq> CloseFd p fd;
 \<forall> p f. e \<noteq> UnLink p f;
 \<forall> p f. e \<noteq> Rmdir p f;
 \<forall> p f i. e \<noteq> Mkdir p f i;
-\<forall> p f f'. e \<noteq> LinkHard p f f';
 valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"
 apply (frule vd_cons, frule vt_grant_os)
 apply (induct ff, simp add:sroot_only)
 apply (frule parentf_in_current', simp+, case_tac e)
 apply (auto simp:current_files_simps is_file_simps is_dir_simps sectxt_of_obj_simps cf2sfile_path
 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
 \<forall> p fd. e \<noteq> CloseFd p fd;
 \<forall> p f. e \<noteq> UnLink p f;
 \<forall> p f. e \<noteq> Rmdir p f;
 \<forall> p f i. e \<noteq> Mkdir p f i;
-\<forall> p f f'. e \<noteq> LinkHard p f f';
 ff \<in> current_files s\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"
 by (auto intro!:cf2sfile_other)
 lemma cf2sfile_unlink:
 "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>
 "\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk>
 \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"
 apply (frule vd_cons, frule vt_grant_os)
 apply (simp add:current_files_simps split:if_splits option.splits)
 (* costs too much time, but solved *)
+(*
 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps
 split:if_splits option.splits
 dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file
 not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file
 dest!:current_has_sec')
 done
+*)
-lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other
+sorry
+lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_other
 cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd
 (*********** cfd2sfd simpset *********)
 lemma cfd2sfd_open1:
 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
 apply (auto split:option.splits if_splits)
 done
 lemma cfd2sfd_clone:
-"\<lbrakk>valid (Clone p p' fds shms # s); file_of_proc_fd (Clone p p' fds shms # s) p'' fd' = Some f\<rbrakk>
+"\<lbrakk>valid (Clone p p' fds # s); file_of_proc_fd (Clone p p' fds # s) p'' fd' = Some f\<rbrakk>
-\<Longrightarrow> cfd2sfd (Clone p p' fds shms # s) p'' fd' = (
+\<Longrightarrow> cfd2sfd (Clone p p' fds # s) p'' fd' = (
 if (p'' = p') then cfd2sfd s p fd'
 else cfd2sfd s p'' fd')"
 apply (frule vd_cons, frule vt_grant_os)
 apply (frule proc_fd_in_fds, simp)
 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
 done
 lemma cfd2sfd_other:
 "\<lbrakk>valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f';
 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
-\<forall> p p'' fds shms. e \<noteq> Clone p p'' fds shms\<rbrakk>
+\<forall> p p'' fds. e \<noteq> Clone p p'' fds\<rbrakk>
 \<Longrightarrow> cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'"
 apply (frule vd_cons, frule vt_grant_os)
 apply (frule proc_fd_in_fds, simp)
 apply (frule proc_fd_in_procs, simp)
 apply (frule file_of_proc_fd_in_curf, simp)
 apply (rule_tac x = fd in exI, simp)
 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
 done
 lemma cpfd2sfds_clone:
-"valid (Clone p p' fds shms # s)
+"valid (Clone p p' fds # s)
-\<Longrightarrow> cpfd2sfds (Clone p p' fds shms # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"
+\<Longrightarrow> cpfd2sfds (Clone p p' fds # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"
 apply (frule vd_cons, frule vt_grant_os)
 apply (rule ext)
 apply (rule set_eqI, rule iffI)
 unfolding cpfd2sfds_def proc_file_fds_def
 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
 \<forall> p f fds. e \<noteq> Execve p f fds;
 \<forall> p p'. e \<noteq> Kill p p';
 \<forall> p. e \<noteq> Exit p;
 \<forall> p fd. e \<noteq> CloseFd p fd;
-\<forall> p p' fds shms. e \<noteq> Clone p p' fds shms\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"
+\<forall> p p' fds. e \<noteq> Clone p p' fds\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"
 apply (frule vd_cons, frule vt_grant_os)
 apply (rule ext)
 unfolding cpfd2sfds_def proc_file_fds_def
 apply (case_tac e)
 using cfd2sfd_other
 done
 lemmas cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_execve cpfd2sfds_clone cpfd2sfds_kill cpfd2sfds_exit
 cpfd2sfds_closefd cpfd2sfds_other
-(********* ch2sshm simpset ********)
-lemma ch2sshm_createshm:
-"valid (CreateShM p h # s)
-\<Longrightarrow> ch2sshm (CreateShM p h # s) = (ch2sshm s) (h :=
-(case (sectxt_of_obj (CreateShM p h # s) (O_shm h)) of
-Some sec \<Rightarrow>
-Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
-| _ \<Rightarrow> None))"
-apply (frule vd_cons, frule vt_grant_os)
-apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)
-done
-lemma ch2sshm_other:
-"\<lbrakk>valid (e # s);
-\<forall> p h. e \<noteq> CreateShM p h;
-h' \<in> current_shms (e # s)\<rbrakk> \<Longrightarrow> ch2sshm (e # s) h' = ch2sshm s h'"
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac e)
-apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)
-done
-lemmas ch2sshm_simps = ch2sshm_createshm ch2sshm_other
-lemma current_shm_has_sh:
-"\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sh. ch2sshm s h = Some sh"
-by (auto simp:ch2sshm_def split:option.splits dest!:current_has_sec')
-lemma current_shm_has_sh':
-"\<lbrakk>ch2sshm s h = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"
-by (auto dest:current_shm_has_sh)
-(********** cph2spshs simpset **********)
-lemma cph2spshs_attach:
-"valid (Attach p h flag # s) \<Longrightarrow>
-cph2spshs (Attach p h flag # s) = (cph2spshs s) (p :=
-(case (ch2sshm s h) of
-Some sh \<Rightarrow> cph2spshs s p \<union> {(sh, flag)}
-| _       \<Rightarrow> cph2spshs s p) )"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Attach p h flag" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp)
-apply (rule_tac x = ha in exI, simp)
-apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp)
-apply (rule_tac x = ha in exI, simp)
-apply (frule procs_of_shm_prop1, simp, simp)
-apply (rule impI, simp)
-done
-lemma cph2spshs_detach: "valid (Detach p h # s) \<Longrightarrow>
-cph2spshs (Detach p h # s) = (cph2spshs s) (p :=
-(case (ch2sshm s h, flag_of_proc_shm s p h) of
-(Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
-then cph2spshs s p else cph2spshs s p - {(sh, flag)}
-| _       \<Rightarrow> cph2spshs s p)             )"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (case_tac "x = p")  defer
-using ch2sshm_other[where e = "Detach p h" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]
-apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp)
-apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp)
-apply (rule impI, simp)
-apply (clarsimp)
-apply (frule current_shm_has_sh, simp, erule exE)
-apply (frule procs_of_shm_prop4, simp, simp)
-apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
-apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
-apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
-apply (case_tac "ha = h", simp)
-apply (rule_tac x = sha in exI, rule_tac x = flaga in exI, rule_tac x = ha in exI, simp)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
-apply (case_tac "ha = h", simp)
-apply (rule_tac x = h' in exI, simp)
-apply (frule_tac flag = flag and flag' = flaga in procs_of_shm_prop3, simp+)
-apply (frule_tac flag = flaga in procs_of_shm_prop4, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)
-apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
-apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
-apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+
-apply (simp split:if_splits)
-apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (rule notI, simp split:if_splits)
-apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+
-apply (simp split:if_splits)
-apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)
-apply (case_tac "ha = h", simp add:procs_of_shm_prop3, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-done
-lemma cph2spshs_deleteshm:
-"valid (DeleteShM p h # s) \<Longrightarrow>
-cph2spshs (DeleteShM p h # s) = (\<lambda> p'.
-(case (ch2sshm s h, flag_of_proc_shm s p' h) of
-(Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
-then cph2spshs s p' else cph2spshs s p' - {(sh, flag)}
-| _       \<Rightarrow> cph2spshs s p')   )"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (clarsimp)
-apply (frule current_shm_has_sh, simp, erule exE, simp, simp split:option.splits)
-apply (rule conjI, rule impI)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]
-apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp+)
-apply (rule_tac x = ha in exI, simp)
-apply (case_tac "ha = h", simp+, frule_tac h = ha in procs_of_shm_prop1, simp+)
-apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
-apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
-apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
-apply (case_tac "ha = h", simp)
-apply (rule_tac x = sha in exI, rule_tac x = flag in exI, rule_tac x = ha in exI, simp)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
-apply (case_tac "ha = h", simp)
-apply (rule_tac x = h' in exI, simp)
-apply (frule_tac flag = flag in procs_of_shm_prop4, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)
-apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
-apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
-apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+
-apply (simp split:if_splits)
-apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (rule notI, simp split:if_splits)
-apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+
-apply (simp split:if_splits)
-apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)
-apply (case_tac "ha = h", simp add:procs_of_shm_prop4)
-apply (frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-done
-lemma flag_of_proc_shm_prop1:
-"\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"
-apply (induct s arbitrary:p)
-apply (simp add:init_shmflag_has_proc)
-apply (frule vt_grant_os, frule vd_cons, case_tac a, auto split:if_splits option.splits)
-done
-lemma cph2spshs_clone:
-"valid (Clone p p' fds shms # s) \<Longrightarrow>
-cph2spshs (Clone p p' fds shms # s) = (cph2spshs s) (p' :=
-{(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag} )"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Clone p p' fds shms" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (erule_tac x = h in allE, frule procs_of_shm_prop1, simp, simp add:procs_of_shm_prop4)
-apply (rule_tac x = h in exI, simp, frule flag_of_proc_shm_prop1, simp+, simp add:procs_of_shm_prop1)
-apply (rule_tac x = h in exI, simp, frule procs_of_shm_prop1, simp+)+
-done
-lemma cph2spshs_execve:
-"valid (Execve p f fds # s) \<Longrightarrow>
-cph2spshs (Execve p f fds # s) = (cph2spshs s) (p := {})"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Execve p f fds" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
-done
-lemma cph2spshs_kill:
-"valid (Kill p p' # s) \<Longrightarrow> cph2spshs (Kill p p' # s) = (cph2spshs s) (p' := {})"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Kill p p'" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
-done
-lemma cph2spshs_exit:
-"valid (Exit p # s) \<Longrightarrow> cph2spshs (Exit p # s) = (cph2spshs s) (p := {})"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Exit p" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
-done
-lemma cph2spshs_createshm:
-"valid (CreateShM p h # s) \<Longrightarrow> cph2spshs (CreateShM p h # s) = cph2spshs s"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:cph2spshs_def)
-using ch2sshm_createshm
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (rule_tac x = ha in exI, auto simp:procs_of_shm_prop1)
-done
-lemma cph2spshs_other:
-"\<lbrakk>valid (e # s);
-\<forall> p h flag. e \<noteq> Attach p h flag;
-\<forall> p h. e \<noteq> Detach p h;
-\<forall> p h. e \<noteq> DeleteShM p h;
-\<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
-\<forall> p f fds. e \<noteq> Execve p f fds;
-\<forall> p p'. e \<noteq> Kill p p';
-\<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cph2spshs (e # s) = cph2spshs s"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-unfolding cph2spshs_def
-apply (rule set_eqI, rule iffI)
-apply (erule CollectE | erule conjE| erule exE| rule conjI| rule impI| rule CollectI)+
-apply (frule procs_of_shm_prop1, simp, rule_tac x= sh in exI, rule_tac x = flag in exI, rule_tac x = h in exI)
-apply (case_tac e)
-using ch2sshm_other[where e = e and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3
-simp:ch2sshm_createshm)
-apply (rule_tac x = h in exI, case_tac e)
-using ch2sshm_other[where e = e and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3
-simp:ch2sshm_createshm)
-done
-lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve
-cph2spshs_exit cph2spshs_kill cph2spshs_other
-(******** cp2sproc simpset *********)
 lemma cp2sproc_clone:
-"valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' :=
+"valid (Clone p p' fds # s) \<Longrightarrow> cp2sproc (Clone p p' fds # s) = (cp2sproc s) (p' :=
 case (sectxt_of_obj s (O_proc p)) of
 Some sec \<Rightarrow> Some (Created, sec,
-{sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd},
+{sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})
-{(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag})
 | _        \<Rightarrow> None)"
-apply (frule cph2spshs_clone, frule cpfd2sfds_clone)
+apply (frule cpfd2sfds_clone)
 apply (frule vd_cons, frule vt_grant_os, simp only:os_grant.simps)
 apply ((erule exE| erule conjE)+, frule not_init_intro_proc, simp, rule ext, case_tac "x = p'", simp)
 apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec'
 dest:current_proc_has_sec split:option.splits if_splits)
 done
 lemma cp2sproc_other:
 "\<lbrakk>valid (e # s);
 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
 \<forall> p fd. e \<noteq> CloseFd p fd;
-\<forall> p h flag. e \<noteq> Attach p h flag;
+\<forall> p p' fds. e \<noteq> Clone p p' fds;
-\<forall> p h. e \<noteq> Detach p h;
-\<forall> p h. e \<noteq> DeleteShM p h;
-\<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
 \<forall> p f fds. e \<noteq> Execve p f fds;
 \<forall> p p'. e \<noteq> Kill p p';
 \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cp2sproc (e # s) = cp2sproc s"
-apply (frule cph2spshs_other, simp+, frule cpfd2sfds_other, simp+)
+apply (frule cpfd2sfds_other, simp+)
 apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e, simp_all)
 apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec'
 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
 done
 cp2sproc (Open p f flags fd opt # s) = (cp2sproc s) (p :=
 case (sectxt_of_obj s (O_proc p), sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd),
 cf2sfile (Open p f flags fd opt # s) f) of
 (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
 then Init p else Created, sec,
-(cpfd2sfds s p) \<union> {(fdsec, flags, sf)}, cph2spshs s p)
+(cpfd2sfds s p) \<union> {(fdsec, flags, sf)})
 | _        \<Rightarrow> None)"
-apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
 apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext)
 apply (case_tac "x = p")
 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
 Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd)
 then cp2sproc s p
 else (case (sectxt_of_obj s (O_proc p)) of
 Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
 then Init p else Created,
-sec, cpfd2sfds s p - {sfd}, cph2spshs s p)
+sec, cpfd2sfds s p - {sfd})
 | _        \<Rightarrow> None))
 | _        \<Rightarrow> cp2sproc s p)
 else cp2sproc s p)"
-apply (frule cpfd2sfds_closefd, frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
+apply (frule cpfd2sfds_closefd)
 apply (frule vt_grant_os, frule vd_cons, rule ext)
 apply (case_tac "x = p")
 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
 done
-lemma cp2sproc_attach:
-"valid (Attach p h flag # s) \<Longrightarrow>
-cp2sproc (Attach p h flag # s) = (cp2sproc s) (p :=
-(case (ch2sshm s h) of
-Some sh \<Rightarrow> (case (sectxt_of_obj s (O_proc p)) of
-Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
-then Init p else Created,
-sec, cpfd2sfds s p, cph2spshs s p \<union> {(sh, flag)})
-| _        \<Rightarrow> None)
-| _       \<Rightarrow> cp2sproc s p) )"
-apply (frule cph2spshs_attach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (case_tac "x = p")
-apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
-dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
-dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
-done
-lemma cp2sproc_detach:
-"valid (Detach p h # s) \<Longrightarrow>
-cp2sproc (Detach p h # s) = (cp2sproc s) (p :=
-(case (ch2sshm s h, flag_of_proc_shm s p h) of
-(Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
-then cp2sproc s p
-else (case (sectxt_of_obj s (O_proc p)) of
-Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
-then Init p else Created, sec,
-cpfd2sfds s p, cph2spshs s p - {(sh, flag)})
-| None     \<Rightarrow> None)
-| _       \<Rightarrow> cp2sproc s p)             )"
-apply (frule cph2spshs_detach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (case_tac "x = p")
-apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
-dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
-dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
-done
-lemma cp2sproc_deleteshm:
-"valid (DeleteShM p h # s) \<Longrightarrow>
-cp2sproc (DeleteShM p h # s) = (\<lambda> p'.
-(case (ch2sshm s h, flag_of_proc_shm s p' h) of
-(Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
-then cp2sproc s p'
-else (case (sectxt_of_obj s (O_proc p')) of
-Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p') s \<and> p' \<in> init_procs)
-then Init p' else Created, sec,
-cpfd2sfds s p', cph2spshs s p' - {(sh, flag)})
-| None     \<Rightarrow> None)
-| _       \<Rightarrow> cp2sproc s p')             )"
-apply (frule cph2spshs_deleteshm, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
-dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
-dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
-done
 lemma cp2sproc_execve:
 "valid (Execve p f fds # s) \<Longrightarrow>
 cp2sproc (Execve p f fds # s) = (cp2sproc s) (p :=
 (case (sectxt_of_obj (Execve p f fds # s) (O_proc p)) of
 Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec,
-{sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, {})
+{sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})
 | _        \<Rightarrow> None)                        )"
-apply (frule cph2spshs_execve, frule cpfd2sfds_execve)
+apply (frule cpfd2sfds_execve)
 apply (frule vt_grant_os, frule vd_cons, rule ext)
 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
 done
 lemma cp2sproc_kill:
 "\<lbrakk>valid (Kill p p' # s); p'' \<noteq> p'\<rbrakk> \<Longrightarrow>
 cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''"
-apply (frule cph2spshs_kill, frule cpfd2sfds_kill)
+apply (frule cpfd2sfds_kill)
 apply (frule vt_grant_os, frule vd_cons)
 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
 done
 by (drule_tac p'' = p'' in cp2sproc_kill, simp+)
 lemma cp2sproc_exit:
 "\<lbrakk>valid (Exit p # s); p' \<noteq> p\<rbrakk> \<Longrightarrow>
 cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
-apply (frule cph2spshs_exit, frule cpfd2sfds_exit)
+apply (frule cpfd2sfds_exit)
 apply (frule vt_grant_os, frule vd_cons)
 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
 done
 lemma cp2sproc_exit':
 "\<lbrakk>valid (Exit p # s); p' \<in> current_procs (Exit p # s)\<rbrakk> \<Longrightarrow>
 cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
 by (drule_tac p'= p' in cp2sproc_exit, simp+)
-lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
+lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_clone cp2sproc_execve
-cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other
+cp2sproc_kill cp2sproc_exit cp2sproc_other
 lemma current_proc_has_sp:
 "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sp. cp2sproc s p = Some sp"
 by (auto simp:cp2sproc_def split:option.splits dest!:current_has_sec')
 lemma current_proc_has_sp':
 "\<lbrakk>cp2sproc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
 by (auto dest:current_proc_has_sp)
-(* simpset for cf2sfiles *)
-lemma cf2sfiles_open:
-"\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>
-\<Longrightarrow> cf2sfiles (Open p f flag fd opt # s) f' = (
-if (f' = f \<and> opt \<noteq> None)
-then (case cf2sfile (Open p f flag fd opt # s) f of
-Some sf \<Rightarrow> {sf}
-| _       \<Rightarrow> {} )
-else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons)
-apply (auto simp:cf2sfiles_def cf2sfile_open_none cf2sfile_simps same_inode_files_open
-split:if_splits option.splits dest!:current_file_has_sfile' dest:cf2sfile_open)
-apply (rule_tac x = "f'a" in bexI, drule same_inode_files_prop1, simp add:cf2sfile_open_some1, simp)+
-done
-lemma cf2sfiles_other:
-"\<lbrakk>valid (e # s);
-\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
-\<forall> p fd. e \<noteq> CloseFd p fd;
-\<forall> p f. e \<noteq> UnLink p f;
-\<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> cf2sfiles (e # s) = cf2sfiles s"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI)
-apply (drule Set.CollectD, erule bexE, rule CollectI)
-apply (rule_tac x = f' in bexI, case_tac e)
-apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps
-split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')
-apply (drule_tac f' = f' in cf2sfile_rmdir)
-apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
-apply (rule_tac x = f' in bexI, case_tac e)
-apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps
-split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')
-apply (drule_tac f' = f' in cf2sfile_rmdir)
-apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
-done
-lemma cf2sfile_linkhard1':
-"\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> same_inode_files s f''\<rbrakk>
-\<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
-apply (drule same_inode_files_prop1)
-by (simp add:cf2sfile_linkhard1)
-lemma cf2sfiles_linkhard:
-"valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'.
-if (f' = f \<or> f' \<in> same_inode_files s oldf)
-then (case (cf2sfile (LinkHard p oldf f # s) f) of
-Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf}
-| _       \<Rightarrow> {})
-else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:cf2sfiles_def cf2sfile_linkhard1' same_inode_files_linkhard current_files_linkhard
-split:if_splits option.splits dest!:current_file_has_sfile' current_has_sec' dest:same_inode_files_prop1)
-done
-lemma cf2sfile_unlink':
-"\<lbrakk>valid (UnLink p f # s); f' \<in> same_inode_files (UnLink p f # s) f''\<rbrakk>
-\<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"
-apply (drule same_inode_files_prop1)
-by (simp add:cf2sfile_unlink)
-lemma cf2sfiles_unlink:
-"\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> \<Longrightarrow> cf2sfiles (UnLink p f # s) f' = (
-if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and>
-(\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) then
-(case (cf2sfile s f) of
-Some sf \<Rightarrow> cf2sfiles s f' - {sf}
-| _       \<Rightarrow> {})
-else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons, simp add:current_files_simps split:if_splits)
-apply (rule conjI, clarify, frule is_file_has_sfile', simp, erule exE, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp, erule conjE)
-apply (erule_tac x = f'a in ballE, frule_tac f' = "f'a" in cf2sfile_unlink)
-apply (simp add:current_files_unlink same_inode_files_prop1, simp)
-apply (rule_tac x = f'a in bexI, simp, simp)
-apply (drule_tac f = f and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
-apply (erule conjE|erule exE|erule bexE)+
-apply (case_tac "f'a = f", simp)
-apply (frule_tac f' = f' in same_inode_files_unlink, simp add:current_files_unlink)
-apply (frule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (rule_tac x = f'a in bexI, simp, simp)
-apply (rule impI)+
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp, (erule conjE)+)
-apply (rule_tac x = f'a in bexI, frule_tac f' = "f'a" in cf2sfile_unlink)
-apply (simp add:current_files_unlink same_inode_files_prop1, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (case_tac "f'a = f", simp)
-apply (frule_tac f = f' and f' = f in same_inode_files_prop5, simp)
-apply (erule bexE, erule conjE)
-apply (rule_tac x = f'' in bexI)
-apply (drule_tac f' = f'' in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (simp, simp, erule same_inode_files_prop4, simp)
-apply (rule_tac x = f'a in bexI)
-apply (drule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (simp, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f' = f'a in cf2sfile_unlink)
-apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f' = f'a in cf2sfile_unlink)
-apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
-done
-lemma cf2sfiles_closefd:
-"\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> cf2sfiles (CloseFd p fd # s) f' = (
-case (file_of_proc_fd s p fd) of
-Some f \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s \<and>
-(\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
-then (case (cf2sfile s f) of
-Some sf \<Rightarrow> cf2sfiles s f' - {sf}
-| _       \<Rightarrow> {})
-else cf2sfiles s f'
-| _       \<Rightarrow> cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons, case_tac "file_of_proc_fd s p fd")
-apply (simp_all add:current_files_simps split:if_splits)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (rule conjI, clarify, frule file_of_pfd_is_file, simp)
-apply (frule is_file_has_sfile', simp, erule exE, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp, erule conjE)
-apply (erule_tac x = f'a in ballE, frule_tac f = "f'a" in cf2sfile_closefd)
-apply (simp add:current_files_closefd same_inode_files_prop1, simp)
-apply (rule_tac x = f'a in bexI, simp, simp)
-apply (drule_tac f = a and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
-apply (erule conjE|erule exE|erule bexE)+
-apply (case_tac "f'a = a", simp)
-apply (frule_tac f' = f' in same_inode_files_closefd, simp add:current_files_closefd, simp)
-apply (frule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (rule_tac x = f'a in bexI, simp, simp)
-apply (rule impI)+
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp, (erule conjE)+)
-apply (rule_tac x = f'a in bexI, frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:current_files_closefd same_inode_files_prop1, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (case_tac "f'a = a", simp)
-apply (frule_tac f = f' and f' = a in same_inode_files_prop5, simp)
-apply (erule bexE, erule conjE)
-apply (rule_tac x = f'' in bexI)
-apply (drule_tac f = f'' in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (simp, simp, erule same_inode_files_prop4, simp)
-apply (rule_tac x = f'a in bexI)
-apply (drule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (simp, simp)
-apply (rule conjI, clarify)
-apply (rule impI)
-apply (case_tac "a \<in> files_hung_by_del s", simp_all)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-done
-lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other
-cf2sfiles_unlink cf2sfiles_closefd
 (* simpset for co2sobj *)
 lemma co2sobj_execve:
 "\<lbrakk>valid (Execve p f fds # s); alive (Execve p f fds # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
 if (obj = O_proc p)
 then (case (cp2sproc (Execve p f fds # s) p) of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))
+Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cq2smsgq_other cf2sfile_other)
 apply (case_tac "cp2sproc (Execve p f fds # s) p")
 apply (drule current_proc_has_sp', simp, simp)
-apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
+apply (simp (no_asm_simp) add:cp2sproc_execve split:option.splits)
+apply (simp add:is_file_simps, frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
 apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_execve':
 "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
 if (obj = O_proc p)
 then (case (cp2sproc (Execve p f fds # s) p) of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))
+Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other)
 apply (case_tac "cp2sproc (Execve p f fds # s) p")
 apply (drule current_proc_has_sp', simp, simp)
-apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
+apply (simp (no_asm_simp) add:cp2sproc_execve split:option.splits)
+apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_clone':
-"\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (
+"\<lbrakk>valid (Clone p p' fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
 if (obj = O_proc p')
-then (case (cp2sproc (Clone p p' fds shms # s) p') of
+then (case (cp2sproc (Clone p p' fds # s) p') of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other  )
-apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")
+apply (case_tac "cp2sproc (Clone p p' fds # s) p'")
 apply (drule current_proc_has_sp', simp, simp)
 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)
-apply (rule conjI, rule impI, simp)
+apply (simp (no_asm_simp) add:cp2sproc_clone split:option.splits)
-apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits)
+apply (case_tac "nat = p'", simp, simp)
+apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_clone:
-"\<lbrakk>valid (Clone p p' fds shms # s); alive (Clone p p' fds shms # s) obj\<rbrakk>
+"\<lbrakk>valid (Clone p p' fds # s); alive (Clone p p' fds # s) obj\<rbrakk>
-\<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (
+\<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
 if (obj = O_proc p')
-then (case (cp2sproc (Clone p p' fds shms # s) p') of
+then (case (cp2sproc (Clone p p' fds # s) p') of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other
+apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other)
-cq2smsgq_other tainted_eq_Tainted)
 apply (rule conjI, rule impI, simp)
-apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")
+apply (case_tac "cp2sproc (Clone p p' fds # s) p'")
 apply (drule current_proc_has_sp', simp, simp)
 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)
-apply (simp add:tainted_eq_Tainted, rule impI, rule notI)
+apply (rule impI,rule notI, drule tainted_in_current, simp+)
-apply (drule Tainted_in_current, simp+)
 apply (rule impI, simp)
 apply (drule current_proc_has_sp, simp, (erule exE|erule conjE)+)
-apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted Tainted_in_current split:option.splits)
+apply (simp (no_asm_simp) add:cp2sproc_clone tainted_in_current split:option.splits)
+apply (simp add:is_file_simps, frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
 apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_ptrace:
 "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
 case obj of
-O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'')
+O_proc p'' \<Rightarrow> if (p'' = p')
 then (case (cp2sproc s p'') of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
+Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
-else if (info_flow_shm s p p'')
+else if (p'' = p)
 then (case (cp2sproc s p'') of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p' \<in> Tainted s))
+Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p' \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s (O_proc p'')
 | _          \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cq2smsgq_other cf2sfile_other)
-apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits
+apply (auto simp:cp2sproc_other split:option.splits
-dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+dest!:current_proc_has_sec' current_proc_has_sp')[1]
+apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_open:
 "\<lbrakk>valid (Open p f flag fd opt # s); alive (Open p f flag fd opt # s) obj\<rbrakk>
 \<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of
 O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)
 then (case (cf2sfile (Open p f flag fd opt # s) f) of
-Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))
+Some sf \<Rightarrow> Some (S_file sf (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s (O_file f')
 | O_proc p' \<Rightarrow> if (p' = p)
 then (case (cp2sproc (Open p f flag fd opt # s) p) of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s (O_proc p')
 | _         \<Rightarrow> co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits
+apply (auto simp:cp2sproc_simps split:option.splits dest!:current_proc_has_sp')[1]
-dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
 apply (simp split:if_splits t_object.splits)
 apply (rule conjI, rule impI, erule conjE, erule exE, simp, (erule exE|erule conjE)+)
 apply (case_tac "cf2sfile (Open p f flag fd (Some y) # s) f")
 apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp)
-apply (frule_tac f' = f in cf2sfiles_open, simp add:current_files_simps)
+apply (frule_tac f' = f in cf2sfile_open, simp add:current_files_simps)
-apply (simp add:tainted_eq_Tainted)
+apply (rule impI, rule notI, drule tainted_in_current, simp, simp add:is_file_in_current)
-apply (rule impI, rule notI, drule Tainted_in_current, simp, simp add:is_file_in_current)
+apply (rule impI, simp add:cf2sfile_open is_file_in_current split:option.splits)
-apply (rule impI, simp add:tainted_eq_Tainted cf2sfiles_open is_file_in_current split:option.splits)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 apply (frule is_dir_in_current)
 apply (frule_tac f' = list in cf2sfile_open)
 apply (simp add:current_files_simps split:option.splits)
 apply (simp split:if_splits option.splits)
 lemma co2sobj_readfile:
 "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
 case obj of
 O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
-Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> Tainted s)
+Some f \<Rightarrow> (if (p' = p \<and> O_file f \<in> tainted s)
 then (case (cp2sproc s p') of
 Some sp \<Rightarrow> Some (S_proc sp True)
 | _       \<Rightarrow> None)
 else co2sobj s obj)
 | _       \<Rightarrow> None)
 | _         \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits
+apply (auto simp:cp2sproc_simps split:option.splits dest!:current_proc_has_sp')[1]
-dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps
+simp:current_files_simps cf2sfile_simps
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_writefile:
 "\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (
 case obj of
 O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
-Some f \<Rightarrow> (if (f \<in> same_inode_files s f')
+Some f \<Rightarrow> (if (f' = f)
-then Some (S_file (cf2sfiles s f')
+then (case cf2sfile s f of
-(O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
+Some sf \<Rightarrow> Some (S_file sf                                                                                                                 (O_file f \<in> tainted s \<or> O_proc p \<in> tainted s))
+| _       \<Rightarrow> None)
 else co2sobj s obj)
 | _       \<Rightarrow> None)
 | _         \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
+simp:current_files_simps cf2sfile_simps cp2sproc_simps
-same_inode_files_prop6
 dest:is_file_in_current is_dir_in_current)
+done
-(* should delete has_same_inode !?!?*)
-by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
 lemma co2sobj_closefd:
 "\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
 case obj of
-O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
+O_proc p' \<Rightarrow> (if (p = p')
-Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and>
-f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f.
-f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
-then (case (cf2sfile s f, co2sobj s (O_file f')) of
-(Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
-| _                              \<Rightarrow> None)
-else co2sobj s obj)
-| _       \<Rightarrow> co2sobj s obj)
-| O_proc p' \<Rightarrow> (if (p = p')
 then (case (cp2sproc (CloseFd p fd # s) p) of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj)
 | _         \<Rightarrow> co2sobj s obj) "
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cq2smsgq_other)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
+apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1]
-dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
 apply (frule is_file_in_current)
 apply (case_tac "file_of_proc_fd s p fd")
-apply (simp add:tainted_eq_Tainted)
+apply (simp add:current_files_simps is_file_simps tainted.simps)
-apply (drule_tac f' = list in cf2sfiles_closefd, simp add:current_files_closefd, simp)
+apply (drule_tac f = list in cf2sfile_closefd, simp add:current_files_simps)
-apply (frule_tac f' = list in cf2sfiles_closefd, simp)
+apply (simp split:option.splits)
-apply (simp add:is_file_simps current_files_simps)
+apply (frule_tac f = list in cf2sfile_closefd, simp)
-apply (auto simp add:tainted_eq_Tainted cf2sfile_closefd split:if_splits option.splits
+apply (simp split:option.splits)
-dest!:current_file_has_sfile' dest:hung_file_in_current)[1]
+apply (simp add:is_file_simps current_files_simps split:if_splits)
+apply (rule impI, simp)
 apply (simp add:is_dir_simps, frule is_dir_in_current)
 apply (frule_tac f = list in cf2sfile_closefd)
 apply (clarsimp simp:current_files_closefd split:option.splits)
 apply (drule file_of_pfd_is_file', simp+)
 done
 lemma co2sobj_unlink:
-"\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (
+"\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk>
-case obj of
+\<Longrightarrow> co2sobj (UnLink p f # s) obj = co2sobj s obj"
-O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and>
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-(\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
+apply (simp_all add:current_files_simps cq2smsgq_other)
-then (case (cf2sfile s f, co2sobj s (O_file f')) of
+apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1]
-(Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
-| _                              \<Rightarrow> None)
-else co2sobj s obj
-| _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
-dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
 apply (frule is_file_in_current)
 apply (frule_tac f' = list in cf2sfile_unlink, simp)
-apply (frule_tac f' = list in cf2sfiles_unlink, simp)
+apply (simp add:is_file_simps current_files_simps split:option.splits if_splits)
-apply (simp add:is_file_simps current_files_simps)
-apply (auto simp add:tainted_eq_Tainted is_file_in_current split:if_splits option.splits
-dest!:current_file_has_sfile')[1]
 apply (simp add:is_dir_simps, frule is_dir_in_current)
 apply (frule_tac f' = list in cf2sfile_unlink)
 apply (clarsimp simp:current_files_unlink split:option.splits)
 apply (drule file_dir_conflict, simp+)
 done
 lemma co2sobj_rmdir:
 "\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cq2smsgq_other)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
+apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1]
-dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
 apply (simp add:is_file_simps dir_is_empty_def)
 apply (case_tac "f = list", drule file_dir_conflict, simp, simp)
-apply (simp add:cf2sfiles_other)
+apply (frule_tac f' = list in cf2sfile_rmdir, simp add:is_file_in_current current_files_simps)
-apply (auto simp:cf2sfile_simps dest:is_dir_in_current)
+apply (simp split:option.splits)
+apply (auto simp:cf2sfile_simps cf2sfile_other dest:is_dir_in_current)
 done
 lemma co2sobj_mkdir:
 "\<lbrakk>valid (Mkdir p f i # s); alive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (
 if (obj = O_dir f)
 then (case (cf2sfile (Mkdir p f i # s) f) of
 Some sf \<Rightarrow> Some (S_dir sf)
 | _       \<Rightarrow> None)
 else co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cq2smsgq_other)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
+apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1]
-dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (case_tac "f = list", simp add:is_file_simps is_file_in_current)
-apply (frule_tac cf2sfiles_other, simp+)
+apply (frule_tac f' = list in cf2sfile_mkdir)
+apply (simp add:is_file_in_current)
+apply (simp split:option.splits)
 apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir)
 apply (frule current_file_has_sfile, simp, erule exE, simp)
 apply (drule cf2sfile_mkdir1, simp+)
 done
-lemma co2sobj_linkhard:
-"\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk>
-\<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = (
-case obj of
-O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)
-then (case (cf2sfile (LinkHard p oldf f # s) f) of
-Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> Tainted s))
-| _       \<Rightarrow> None)
-else co2sobj s obj
-| _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
-dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (frule_tac cf2sfiles_linkhard, simp+)
-apply (frule_tac f' = f in cf2sfile_linkhard, simp add:current_files_linkhard)
-apply (auto simp:is_file_simps sectxt_of_obj_simps current_files_simps is_file_in_current same_inodes_Tainted
-split:option.splits if_splits dest:Tainted_in_current
-dest!:current_has_sec' current_file_has_sfile')[1]
-apply (frule is_dir_in_current, simp add:current_files_linkhard is_dir_simps is_dir_in_current)
-apply (frule is_dir_in_current)
-apply (frule current_file_has_sfile, simp)
-apply (drule cf2sfile_linkhard1, simp+)
-done
 lemma co2sobj_truncate:
 "\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (
 case obj of
-O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)
+O_file f' \<Rightarrow> if (f' = f \<and> len > 0)
-then Some (S_file (cf2sfiles s f') (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
+then (case cf2sfile s f of
+Some sf \<Rightarrow> Some (S_file sf (O_file f' \<in> tainted s \<or> O_proc p \<in> tainted s))
+| _       \<Rightarrow> None)
 else co2sobj s obj
 | _         \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
+simp:current_files_simps cf2sfile_simps cp2sproc_simps
-same_inode_files_prop6
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_kill:
 "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
+simp:current_files_simps cf2sfile_simps cp2sproc_simps
-same_inode_files_prop6
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_exit:
 "\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other  )
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
+simp:current_files_simps cf2sfile_simps cp2sproc_simps
-same_inode_files_prop6
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_createmsgq:
 "\<lbrakk>valid (CreateMsgq p q # s); alive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (
 Some sq \<Rightarrow> Some (S_msgq sq)
 | _       \<Rightarrow> None)
 else co2sobj s obj
 | _        \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other  )
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
+simp:current_files_simps cf2sfile_simps cp2sproc_simps
-same_inode_files_prop6
 dest!:current_has_smsgq'
 dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq)
 done
 lemma co2sobj_sendmsg:
 Some sq \<Rightarrow> Some (S_msgq sq)
 | _       \<Rightarrow> None)
 else co2sobj s obj
 | _        \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other  )
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
+simp:current_files_simps cf2sfile_simps cp2sproc_simps
-same_inode_files_prop6
 dest!:current_has_smsgq'
 dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg)
 done
 lemma co2sobj_recvmsg:
 case obj of
 O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
 Some sq \<Rightarrow> Some (S_msgq sq)
 | _       \<Rightarrow> None)
 else co2sobj s obj
-| O_proc p' \<Rightarrow> if (info_flow_shm s p p' \<and> O_msg q m \<in> Tainted s)
+| O_proc p' \<Rightarrow> if (p' = p \<and> O_msg q m \<in> tainted s)
 then (case (cp2sproc s p') of
 Some sp \<Rightarrow> Some (S_proc sp True)
 | _       \<Rightarrow> None)
 else co2sobj s obj
 | _         \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
+simp:current_files_simps cf2sfile_simps cp2sproc_simps
-same_inode_files_prop6
 dest!:current_has_smsgq'
 dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg)
 done
 lemma co2sobj_removemsgq:
 "\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk>
 \<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
+simp:current_files_simps cf2sfile_simps cp2sproc_simps
-same_inode_files_prop6
 dest!:current_has_smsgq'
 dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq)
 done
-lemma co2sobj_createshm:
-"\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
-case obj of
-O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of
-Some sh \<Rightarrow> Some (S_shm sh)
-| _       \<Rightarrow> None)
-else co2sobj s obj
-| _        \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-same_inode_files_prop6 ch2sshm_simps
-dest!:current_shm_has_sh'
-dest:is_file_in_current is_dir_in_current)
-done
-lemma co2sobj_detach:
-"\<lbrakk>valid (Detach p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (
-case obj of
-O_proc p' \<Rightarrow> if (p' = p) then (case (cp2sproc (Detach p h # s) p) of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
-| _       \<Rightarrow> None)
-else co2sobj s obj
-| _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-same_inode_files_prop6 ch2sshm_simps
-dest!:current_shm_has_sh'
-dest:is_file_in_current is_dir_in_current)
-done
-lemma co2sobj_deleteshm:
-"\<lbrakk>valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (
-case obj of
-O_proc p' \<Rightarrow> (case (cp2sproc (DeleteShM p h # s) p') of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s))
-| _       \<Rightarrow> None)
-| _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted
-same_inode_files_prop6 ch2sshm_simps
-dest!:current_shm_has_sh'
-dest:is_file_in_current is_dir_in_current)
-done
 declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
-lemma info_flow_shm_prop1:
-"p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"
-by (simp add:info_flow_shm_def)
-lemma co2sobj_attach:
-"\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
-case obj of
-O_proc p' \<Rightarrow> if (info_flow_shm s p p')
-then (case (cp2sproc (Attach p h flag # s) p') of
-Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or>
-(\<exists> p''. O_proc p'' \<in> Tainted s \<and> (p'', SHM_RDWR) \<in> procs_of_shm s h)))
-| _       \<Rightarrow> None)
-else if (\<exists> p'' flag'. (p'', flag') \<in> procs_of_shm s h \<and> flag = SHM_RDWR \<and> O_proc p \<in> Tainted s \<and>
-info_flow_shm s p'' p')
-then (case (cp2sproc s p') of
-Some sp \<Rightarrow> Some (S_proc sp True)
-| _       \<Rightarrow> None)
-else co2sobj s obj
-| _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (rule conjI|rule impI|erule exE)+
-apply (simp split:option.splits del:split_paired_Ex)
-apply (rule impI, frule current_proc_has_sp, simp)
-apply ((erule exE)+, auto simp:tainted_eq_Tainted intro:info_flow_shm_Tainted)[1]
-apply (rule impI, simp add:tainted_eq_Tainted split:option.splits del:split_paired_Ex)
-apply (auto simp:info_flow_shm_prop1 cp2sproc_attach dest!:current_proc_has_sp')[1]
-apply (case_tac "cp2sproc (Attach p h flag # s) nat")
-apply (drule current_proc_has_sp', simp+)
-apply (rule conjI|erule exE|erule conjE|rule impI)+
-apply (simp add:tainted_eq_Tainted)
-apply (auto simp:info_flow_shm_prop1 cp2sproc_attach intro:info_flow_shm_Tainted dest!:current_proc_has_sp')[1]
-apply (auto simp:info_flow_shm_prop1 cp2sproc_attach tainted_eq_Tainted intro:info_flow_shm_Tainted dest!:current_proc_has_sp'
-split:option.splits if_splits)[1]
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile'
-simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted
-same_inode_files_prop6
-dest:is_file_in_current is_dir_in_current)
-done
 lemma co2sobj_other:
 "\<lbrakk>valid (e # s); alive (e # s) obj;
 \<forall> p f fds. e \<noteq> Execve p f fds;
-\<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+\<forall> p p' fds. e \<noteq> Clone p p' fds;
 \<forall> p p'. e \<noteq> Ptrace p p';
 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
 \<forall> p fd. e \<noteq> ReadFile p fd;
 \<forall> p fd. e \<noteq> WriteFile p fd;
 \<forall> p fd. e \<noteq> CloseFd p fd;
 \<forall> p f. e \<noteq> UnLink p f;
 \<forall> p f. e \<noteq> Rmdir p f;
 \<forall> p f i. e \<noteq> Mkdir p f i;
-\<forall> p f f'. e \<noteq> LinkHard p f f';
 \<forall> p f len. e \<noteq> Truncate p f len;
 \<forall> p q. e \<noteq> CreateMsgq p q;
 \<forall> p q m. e \<noteq> SendMsg p q m;
 \<forall> p q m. e \<noteq> RecvMsg p q m;
-\<forall> p q. e \<noteq> RemoveMsgq p q;
+\<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk>
-\<forall> p h. e \<noteq> CreateShM p h;
+\<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"
-\<forall> p h flag. e \<noteq> Attach p h flag;
-\<forall> p h. e \<noteq> Detach p h;
-\<forall> p h. e \<noteq> DeleteShM p h
-\<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"
 apply (frule vt_grant, case_tac e)
 apply (auto intro:co2sobj_kill co2sobj_exit)
 done
 lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open co2sobj_readfile
-co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard
+co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir
 co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg
-co2sobj_removemsgq co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm
+co2sobj_removemsgq
 end
 (*<*)
 end

changeset 75	99af1986e1e0
parent 74	271e9818b6f6