find bug: a created proc can be tainted by a message, which cannot remain and maynot be duplicated
(*<*)
theory Current_files_prop
imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop
begin
(*<*)
context init begin
lemma current_files_ndef: "f \<notin> current_files \<tau> \<Longrightarrow> inum_of_file \<tau> f = None"
by (simp add:current_files_def)
(************** file_of_proc_fd vs proc_fd_of_file *****************)
lemma pfdof_simp1: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> (p, fd) \<in> proc_fd_of_file \<tau> f"
by (simp add:proc_fd_of_file_def)
lemma pfdof_simp2: "(p, fd) \<in> proc_fd_of_file \<tau> f \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f"
by (simp add:proc_fd_of_file_def)
lemma pfdof_simp3: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> \<forall> p' fd'. (file_of_proc_fd \<tau> p' fd' = Some f \<longrightarrow> p = p' \<and> fd = fd')"
by (simp add:proc_fd_of_file_def, auto)
lemma pfdof_simp4: "\<lbrakk>file_of_proc_fd \<tau> p' fd' = Some f; proc_fd_of_file \<tau> f = {(p, fd)}\<rbrakk> \<Longrightarrow> p' = p \<and> fd' = fd"
by (drule pfdof_simp3, auto)
end
context flask begin
(***************** inode number lemmas *************************)
lemma iof's_im_in_cim: "inum_of_file \<tau> f = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>"
by (auto simp add:current_inode_nums_def current_file_inums_def)
lemma ios's_im_in_cim: "inum_of_socket \<tau> s = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>"
by (case_tac s, auto simp add:current_inode_nums_def current_sock_inums_def)
lemma fim_noninter_sim_aux[rule_format]:
"\<forall> f s. inum_of_file \<tau> f = Some im \<and> inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> False"
apply (induct \<tau>)
apply (clarsimp simp:inum_of_file.simps inum_of_socket.simps)
apply (drule init_inum_sock_file_noninter, simp, simp)
apply ((rule allI|rule impI|erule conjE)+)
apply (frule vd_cons, frule vt_grant_os, simp, case_tac a)
apply (auto simp:inum_of_file.simps inum_of_socket.simps split:if_splits option.splits
dest:ios's_im_in_cim iof's_im_in_cim)
done
lemma fim_noninter_sim':"\<lbrakk>inum_of_file \<tau> f = Some im; inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
by (auto intro:fim_noninter_sim_aux)
lemma fim_noninter_sim'':"\<lbrakk>inum_of_socket \<tau> s = Some im; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
by (auto intro:fim_noninter_sim_aux)
lemma fim_noninter_sim: "valid \<tau> \<Longrightarrow> (current_file_inums \<tau>) \<inter> (current_sock_inums \<tau>) = {}"
by (auto simp:current_file_inums_def current_sock_inums_def intro:fim_noninter_sim_aux[rule_format])
(******************* file inum has inode tag ************************)
lemma finum_has_itag_aux[rule_format]:
"\<forall> f im. inum_of_file \<tau> f = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None"
apply (induct \<tau>)
apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props)
apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
apply (auto simp add:inum_of_file.simps itag_of_inum.simps os_grant.simps current_files_def
dest:fim_noninter_sim'' split:option.splits if_splits t_socket_type.splits)
done
lemma finum_has_itag: "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag"
by (auto dest:conjI[THEN finum_has_itag_aux])
(*********************** file inum is file itag *************************)
lemma finum_has_ftag_aux[rule_format]:
"\<forall> f tag. inum_of_file \<tau> f = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_file_dir_itag tag"
apply (induct \<tau>)
apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props)
apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
apply (auto simp:inum_of_file.simps os_grant.simps current_files_def itag_of_inum.simps
split:if_splits option.splits t_socket_type.splits
dest:ios's_im_in_cim iof's_im_in_cim)
done
lemma finum_has_ftag:
"\<lbrakk>inum_of_file \<tau> f = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_file_dir_itag tag"
by (auto intro:finum_has_ftag_aux)
lemma finum_has_ftag':
"\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE \<or> itag_of_inum \<tau> im = Some Tag_DIR"
apply (frule finum_has_itag, simp, erule exE, drule finum_has_ftag, simp+)
apply (case_tac tag, auto)
done
(******************* sock inum has inode tag ************************)
lemma sinum_has_itag_aux[rule_format]:
"\<forall> s im. inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None"
apply (induct \<tau>)
apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps)
apply (drule init_inumos_prop4, clarsimp)
apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps
dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim
split:option.splits if_splits t_socket_type.splits)
done
lemma sinum_has_itag: "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag"
by (auto dest:conjI[THEN sinum_has_itag_aux])
(********************** socket inum is socket itag **********************)
lemma sinum_has_stag_aux[rule_format]:
"\<forall> s tag. inum_of_socket \<tau> s = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_sock_itag tag"
apply (induct \<tau>)
apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps)
apply (drule init_inumos_prop4, clarsimp)
apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps
dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim
split:option.splits if_splits t_socket_type.splits)
done
lemma sinum_has_stag: "\<lbrakk>inum_of_socket \<tau> s = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_sock_itag tag"
by (auto dest:conjI[THEN sinum_has_stag_aux])
lemma sinum_has_stag':
"\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk>
\<Longrightarrow> itag_of_inum \<tau> im = Some Tag_UDP_SOCK \<or> itag_of_inum \<tau> im = Some Tag_TCP_SOCK"
apply (frule sinum_has_itag, simp, erule exE)
apply (drule sinum_has_stag, simp+, case_tac tag, simp+)
done
(************************************ 4 in 1 *************************************)
lemma file_leveling: "valid \<tau> \<longrightarrow> (
(\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and>
(\<forall> f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and>
(\<forall> f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and>
(\<forall> f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False) )"
proof (induct \<tau>)
case Nil
show ?case
apply (auto simp:inum_of_file.simps files_hung_by_del.simps is_file_def itag_of_inum.simps parent_file_in_init split:option.splits t_inode_tag.splits)
apply (drule init_files_hung_by_del_props, simp add:init_file_has_inum)
apply (rule init_parent_file_has_inum, simp+)
apply (rule init_file_has_no_son', simp+)
apply (rule init_file_hung_has_no_son, simp+)
done
next
case (Cons a \<tau>)
assume pre: "valid \<tau> \<longrightarrow>
(\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and>
(\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and>
(\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and>
(\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False)"
show ?case
proof
assume cons:"valid (a # \<tau>)"
show "(\<forall>f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None) \<and>
(\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None) \<and>
(\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False) \<and>
(\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> parent f' = Some f \<longrightarrow> False)"
proof-
have vt: "valid \<tau>" using cons by (auto dest:vd_cons)
have os: "os_grant \<tau> a" using cons by (auto dest:vt_grant_os)
have fin: "\<forall>f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" using vt pre by auto
have pin: "\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None"
using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
have fns: "\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False"
using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
have hns: "\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False"
using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
have ain: "\<forall>f' f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
proof
fix f'
show " \<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
proof (induct f')
case Nil show ?case by (auto simp: no_junior_def)
next
case (Cons a f')
assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
proof clarify
fix f im
assume h1: "f \<preceq> a # f'"
and h2: "inum_of_file \<tau> (a # f') = Some im"
show "\<exists>y. inum_of_file \<tau> f = Some y"
proof-
have h3: "\<exists> y. inum_of_file \<tau> f' = Some y"
proof-
have "parent (a # f') = Some f'" by simp
hence "\<exists> y. inum_of_file \<tau> f' = Some y" using pin h2 by blast
with h1 show ?thesis by simp
qed
from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def)
moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp
moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h3 by simp
moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 by simp
ultimately show ?thesis by auto
qed
qed
qed
qed
have fin': "\<And> f. f \<in> files_hung_by_del \<tau> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" using fin by auto
have pin': "\<And> f pf im. \<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'"
using pin by auto
have fns': "\<And> f f' im. \<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False" using fns by auto
have fns'': "\<And> f f' im im'. \<lbrakk>itag_of_inum \<tau> im = Some Tag_FILE; inum_of_file \<tau> f = Some im; parent f' = Some f; inum_of_file \<tau> f' = Some im'\<rbrakk> \<Longrightarrow> False"
by (rule_tac f = f and f' = f' in fns', auto simp:is_file_def)
have hns': "\<And> f f' im. \<lbrakk>f \<in> files_hung_by_del \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False" using hns by auto
have ain': "\<And> f f' im. \<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'" using ain by auto
have dns': "\<And> f f' im. \<lbrakk>dir_is_empty \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False"
apply (auto simp:dir_is_empty_def current_files_def is_dir_def split:option.splits)
by (erule_tac x = f' in allE, simp add:noJ_Anc parent_is_ancen, drule parent_is_parent, simp+)
have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None"
apply (clarify, case_tac a) using os fin
apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def is_file_def
split:if_splits option.splits)
done
moreover
have "\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None"
apply (clarify, case_tac a)
using vt os pin'
apply (auto simp:os_grant.simps current_files_def inum_of_file.simps is_file_def is_dir_def
split:if_splits option.splits t_inode_tag.splits)
apply (drule_tac f = pf and f' = f in hns', simp, simp, simp)
apply (rule_tac f = list and f' = f in fns', simp add:is_file_def, simp, simp)
apply (rule_tac f = list and f' = f in dns', simp add:is_dir_def, simp, simp)
done
moreover have "\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False"
apply (clarify, case_tac a)
using vt os fns'' cons
apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps
is_file_def is_dir_def
dest:ios's_im_in_cim iof's_im_in_cim
split:if_splits option.splits t_inode_tag.splits t_socket_type.splits)
apply (rule_tac im = a and f = f and f' = f' in fns'', simp+)
apply (drule_tac f = f' and pf = list in pin', simp, simp)
apply (drule_tac f = f' and pf = list2 in pin', simp, simp)
done
moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and>
parent f' = Some f \<longrightarrow> False"
apply (clarify, case_tac a)
using vt os hns'
apply (auto simp:os_grant.simps current_files_def inum_of_file.simps files_hung_by_del.simps
split:if_splits option.splits t_sock_addr.splits)
apply (drule fns', simp+)
done
ultimately show ?thesis by blast
qed
qed
qed
(**************** hung file in current ***********************)
lemma hung_file_has_inum:"\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
by (drule file_leveling[rule_format], blast)
lemma hung_file_has_inum': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im"
by (auto dest:hung_file_has_inum)
lemma hung_file_in_current: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
by (clarsimp simp add:current_files_def hung_file_has_inum')
lemma parentf_has_inum: "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> pf \<noteq> None"
by (drule file_leveling[rule_format], blast)
lemma parentf_has_inum': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'"
by (auto dest:parentf_has_inum)
lemma parentf_in_current: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>"
by (clarsimp simp add:current_files_def parentf_has_inum')
lemma parentf_in_current': "\<lbrakk>a # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>"
apply (subgoal_tac "parent (a # pf) = Some pf")
by (erule parentf_in_current, simp+)
lemma ancenf_has_inum_aux: "\<forall> f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
proof (induct f')
case Nil show ?case by (auto simp: no_junior_def)
next
case (Cons a f')
assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
proof clarify
fix f im
assume h1: "f \<preceq> a # f'"
and h2: "inum_of_file \<tau> (a # f') = Some im"
and h3: "valid \<tau>"
show "\<exists>y. inum_of_file \<tau> f = Some y"
proof-
have h4: "\<exists> y. inum_of_file \<tau> f' = Some y"
proof-
have "parent (a # f') = Some f'" by simp
hence "\<exists> y. inum_of_file \<tau> f' = Some y" using parentf_has_inum' h2 h3 by blast
with h1 show ?thesis by simp
qed
from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def)
moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp
moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h4 by simp
moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 h4 by simp
ultimately show ?thesis by auto
qed
qed
qed
lemma ancenf_has_inum: "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
by (rule ancenf_has_inum_aux[rule_format], auto)
lemma ancenf_has_inum': "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'"
by (auto dest:ancenf_has_inum)
lemma ancenf_in_current: "\<lbrakk>f \<preceq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
by (simp add:current_files_def, erule exE, simp add:ancenf_has_inum')
lemma file_has_no_son: "\<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
by (drule file_leveling[rule_format], blast)
lemma file_has_no_son': "\<lbrakk>is_file \<tau> f; parent f' = Some f; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"
by (simp add:current_files_def, erule exE, auto intro:file_has_no_son)
lemma hung_file_no_son: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False"
by (drule file_leveling[rule_format], blast)
lemma hung_file_no_son': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; parent f' = Some f\<rbrakk> \<Longrightarrow> False"
by (simp add:current_files_def, erule exE, auto intro:hung_file_no_son)
lemma hung_file_no_des_aux: "\<forall> f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> f' \<in> current_files \<tau> \<and> f \<preceq> f' \<and> f \<noteq> f' \<longrightarrow> False"
proof (induct f')
case Nil
show ?case
by (auto simp:files_hung_by_del.simps current_files_def inum_of_file.simps no_junior_def split:if_splits option.splits)
next
case (Cons a pf)
assume pre: "\<forall>f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> pf \<in> current_files \<tau> \<and> f \<preceq> pf \<and> f \<noteq> pf\<longrightarrow> False"
show ?case
proof clarify
fix f
assume h1: "f \<in> files_hung_by_del \<tau>"
and h2: "valid \<tau>"
and h3: "a # pf \<in> current_files \<tau>"
and h4: "f \<preceq> a # pf"
and h5: "f \<noteq> a # pf"
have h6: "parent (a # pf) = Some pf" by simp
with h2 h3 have h7: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto)
from h4 h5 have h8: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def)
show False
proof (cases "f = pf")
case True with h6 h2 h3 h1
show False by (auto intro!:hung_file_no_son')
next
case False with pre h1 h2 h7 h8
show False by blast
qed
qed
qed
lemma hung_file_no_des: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; f \<preceq> f'; f \<noteq> f'\<rbrakk> \<Longrightarrow> False"
by (rule hung_file_no_des_aux[rule_format], blast)
(* current version, dir can not be opened, so hung_files are all files
lemma hung_file_is_leaf: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f \<or> dir_is_empty \<tau> f"
apply (frule hung_file_has_inum', simp, erule exE)
apply (auto simp add:is_file_def dir_is_empty_def is_dir_def dest:finum_has_itag finum_has_ftag split:option.splits if_splits t_inode_tag.splits)
by (simp add: noJ_Anc, auto dest:hung_file_no_des)
*)
lemma hung_file_has_filetag:
"\<lbrakk>f \<in> files_hung_by_del s; inum_of_file s f = Some im; valid s\<rbrakk> \<Longrightarrow> itag_of_inum s im = Some Tag_FILE"
apply (induct s)
apply (simp add:files_hung_by_del.simps)
apply (drule init_files_hung_prop2, (erule exE)+)
apply (drule init_filefd_prop5, clarsimp simp:is_init_file_def split:t_inode_tag.splits option.splits)
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto simp:files_hung_by_del.simps is_file_def is_dir_def current_files_def current_inode_nums_def
split:if_splits option.splits t_inode_tag.splits t_socket_type.splits
dest:hung_file_has_inum iof's_im_in_cim)
done
lemma hung_file_is_file: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f"
apply (frule hung_file_has_inum', simp, erule exE)
apply (drule hung_file_has_filetag, auto simp:is_file_def)
done
(*********************** 2 in 1 *********************)
lemma file_of_pfd_2in1: "valid s \<Longrightarrow> (
(\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> inum_of_file s f \<noteq> None) \<and>
(\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> is_file s f) )"
proof (induct s)
case Nil
show ?case
by (auto dest:init_filefd_valid simp:is_file_def)
next
case (Cons e s)
hence vd_e: "valid (e # s)" and vd_s: "valid s" and os: "os_grant s e"
and pfd: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> inum_of_file s f \<noteq> None"
and isf: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> is_file s f"
by (auto dest:vd_cons vt_grant_os)
from pfd have pfd': "\<And> p fd f. inum_of_file s f = None \<Longrightarrow> file_of_proc_fd s p fd \<noteq> Some f"
by (rule_tac notI, drule_tac pfd, simp)
have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> inum_of_file (e # s) f \<noteq> None"
apply (case_tac e) using os
apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def
dir_is_empty_def is_file_def is_dir_def
split:if_splits option.splits dest:pfd)
apply (simp add:pfdof_simp3)+
apply (simp add:proc_fd_of_file_def)
apply (drule isf, simp add:is_file_def split:t_inode_tag.splits)
done
moreover
have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> is_file (e # s) f"
apply (case_tac e) using os
apply (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits
dest:pfd isf iof's_im_in_cim
simp:is_file_def is_dir_def dir_is_empty_def current_files_def)
apply (simp add:pfdof_simp3)+
apply (simp add:proc_fd_of_file_def)
done
ultimately show ?case by auto
qed
(************** file_of_proc_fd in current ********************)
lemma file_of_pfd_imp_inode': "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
by (drule file_of_pfd_2in1, blast)
lemma file_of_pfd_imp_inode: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im"
by (auto dest!:file_of_pfd_imp_inode')
lemma file_of_pfd_in_current: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def)
(*************** file_of_proc_fd is file *********************)
lemma file_of_pfd_is_file:
"\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f"
by (drule file_of_pfd_2in1, auto simp:is_file_def)
lemma file_of_pfd_is_file':
"\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False"
by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)
lemma file_of_pfd_is_file_tag:
"\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE"
by (drule file_of_pfd_is_file, auto simp:is_file_def split:option.splits t_inode_tag.splits)
(************** parent file / ancestral file is dir *******************)
lemma parentf_is_dir_aux: "\<forall> f pf. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<and> inum_of_file \<tau> pf = Some ipm \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR"
apply (induct \<tau>)
apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_parent_file_is_dir')
apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto simp:inum_of_file.simps itag_of_inum.simps os_grant.simps
current_files_def is_dir_def is_file_def
dest: ios's_im_in_cim iof's_im_in_cim
split:if_splits option.splits t_sock_addr.splits t_inode_tag.splits t_socket_type.splits)
apply (drule parentf_has_inum', simp, simp, simp)+
done
lemma parentf_has_dirtag:
"\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; inum_of_file \<tau> pf = Some ipm; valid \<tau>\<rbrakk>
\<Longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR"
by (auto intro:parentf_is_dir_aux[rule_format])
lemma parentf_is_dir': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
apply (frule parentf_has_inum', simp+, erule exE, simp add:is_dir_def split:t_inode_tag.splits option.splits)
by (auto dest:parentf_has_dirtag)
lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
by (clarsimp simp:current_files_def parentf_is_dir')
lemma parentf_is_dir'': "\<lbrakk>f # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
by (auto intro!:parentf_is_dir)
lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"
proof (induct f')
case Nil show ?case
by (auto simp:current_files_def no_junior_def)
next
case (Cons a pf)
assume pre: "\<forall>f. f \<preceq> pf \<and> f \<noteq> pf \<and> pf \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"
show ?case
proof clarify
fix f
assume h1: "f \<preceq> a # pf"
and h2: "f \<noteq> a # pf"
and h3: "a # pf \<in> current_files \<tau>"
and h4: "valid \<tau>"
have h5: "parent (a # pf) = Some pf" by simp
with h3 h4 have h6: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto)
from h1 h2 have h7: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def)
show "is_dir \<tau> f"
proof (cases "f = pf")
case True with h3 h4 h5 show "is_dir \<tau> f" by (drule_tac parentf_is_dir, auto)
next
case False with pre h6 h7 h4 show "is_dir \<tau> f" by blast
qed
qed
qed
lemma ancenf_is_dir: "\<lbrakk>f \<preceq> f'; f \<noteq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> f"
by (auto intro:ancenf_is_dir_aux[rule_format])
(************* rebuild current_files simpset ***********************)
lemma current_files_nil: "current_files [] = init_files"
apply (simp add:current_files_def inum_of_file.simps)
by (auto dest:inof_has_file_tag init_file_has_inum)
lemma current_files_open: "current_files (Open p f flags fd (Some i) # \<tau>) = insert f (current_files \<tau>)"
by (auto simp add:current_files_def inum_of_file.simps split:option.splits)
lemma current_files_open': "current_files (Open p f flags fd None # \<tau>) = current_files \<tau>"
by (simp add:current_files_def inum_of_file.simps split:option.splits)
lemma current_files_closefd: "current_files (CloseFd p fd # \<tau>) = (
case (file_of_proc_fd \<tau> p fd) of
Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>))
then current_files \<tau> - {f}
else current_files \<tau>)
| _ \<Rightarrow> current_files \<tau> )"
by (auto simp:current_files_def inum_of_file.simps split:option.splits)
lemma current_files_unlink: "current_files (UnLink p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then (current_files \<tau>) - {f} else current_files \<tau>)"
by (auto simp:current_files_def inum_of_file.simps split:option.splits)
lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = current_files \<tau> - {f}"
by (auto simp:current_files_def inum_of_file.simps split:option.splits)
lemma current_files_mkdir: "current_files (Mkdir p f ino # \<tau>) = insert f (current_files \<tau>)"
by (auto simp:current_files_def inum_of_file.simps split:option.splits)
lemma current_files_linkhard:
"valid (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) \<Longrightarrow> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = insert f\<^isub>2 (current_files \<tau>)"
apply (frule vt_grant_os, frule vd_cons)
by (auto simp:current_files_def inum_of_file.simps os_grant.simps is_file_def split:option.splits)
(*
lemma rename_renaming_decom:
"\<lbrakk>f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f"
apply (case_tac "f\<^isub>2 \<preceq> f", simp)
apply (simp add:file_after_rename_def split:if_splits)
by (frule vd_cons, frule vt_grant_os, auto simp:os_grant.simps dest!:ancenf_in_current)
lemma rename_renaming_decom':
"\<lbrakk>\<not> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f"
by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+)
lemma current_files_rename: "Rename p f\<^isub>2 f\<^isub>3 # valid \<tau> \<Longrightarrow> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> current_files \<tau>}"
apply (frule vt_grant_os, frule vd_cons)
apply (auto simp:current_files_def inum_of_file.simps os_grant.simps split:if_splits option.splits)
apply (rule_tac x = x in exI, simp add:file_after_rename_def)
apply (frule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop1', drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop5')
apply (erule_tac x = "file_before_rename f\<^isub>2 f\<^isub>3 x" in allE, simp)
apply (rule_tac x = x in exI, simp add:file_after_rename_def)
apply (drule_tac a = f\<^isub>3 and b = f\<^isub>2 in no_junior_conf, simp, simp)
apply (drule_tac f = f\<^isub>3 and f' = f\<^isub>2 in ancenf_has_inum', simp, simp, simp)
apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom, simp, simp add:current_files_def, simp add:file_renaming_prop5)
apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def)
apply (simp add:file_after_rename_def)
apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def)
apply (simp add:file_after_rename_def)
done
*)
lemma current_files_other:
"\<lbrakk>\<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'\<rbrakk> \<Longrightarrow> current_files (e # \<tau>) = current_files \<tau>"
by (case_tac e, auto simp:current_files_def inum_of_file.simps)
lemmas current_files_simps = current_files_nil current_files_open current_files_open'
current_files_closefd current_files_unlink current_files_rmdir
current_files_mkdir current_files_linkhard current_files_other
(******************** is_file simpset *********************)
lemma is_file_open:
"valid (Open p f flags fd opt # s) \<Longrightarrow>
is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))"
apply (frule vd_cons, drule vt_grant_os, rule ext)
apply (auto dest:finum_has_itag iof's_im_in_cim
split:if_splits option.splits t_inode_tag.splits
simp:is_file_def current_files_def)
done
lemma is_file_closefd:
"valid (CloseFd p fd # s) \<Longrightarrow> is_file (CloseFd p fd # s) = (
case (file_of_proc_fd s p fd) of
Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))
then (is_file s) (f := False)
else is_file s)
| _ \<Rightarrow> is_file s )"
apply (frule vd_cons, drule vt_grant_os, rule ext)
apply (auto dest:finum_has_itag iof's_im_in_cim
split:if_splits option.splits t_inode_tag.splits
simp:is_file_def)
done
lemma is_file_unlink:
"valid (UnLink p f # s) \<Longrightarrow> is_file (UnLink p f # s) = (
if (proc_fd_of_file s f = {}) then (is_file s) (f := False) else is_file s)"
apply (frule vd_cons, drule vt_grant_os, rule ext)
apply (auto dest:finum_has_itag iof's_im_in_cim
split:if_splits option.splits t_inode_tag.splits
simp:is_file_def)
done
lemma is_file_linkhard:
"valid (LinkHard p f f' # s) \<Longrightarrow> is_file (LinkHard p f f' # s) = (is_file s) (f' := True)"
apply (frule vd_cons, drule vt_grant_os, rule ext)
apply (auto dest:finum_has_itag iof's_im_in_cim
split:if_splits option.splits t_inode_tag.splits
simp:is_file_def)
done
lemma is_file_other:
"\<lbrakk>valid (e # \<tau>);
\<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> is_file (e # \<tau>) = is_file \<tau>"
apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e)
apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
split:if_splits option.splits t_inode_tag.split t_socket_type.splits
simp:is_file_def dir_is_empty_def is_dir_def current_files_def)
done
lemma file_dir_conflict: "\<lbrakk>is_file s f; is_dir s f\<rbrakk> \<Longrightarrow> False"
by (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)
lemma is_file_not_dir: "is_file s f \<Longrightarrow> \<not> is_dir s f"
by (rule notI, erule file_dir_conflict, simp)
lemma is_dir_not_file: "is_dir s f \<Longrightarrow> \<not> is_file s f"
by (rule notI, erule file_dir_conflict, simp)
lemmas is_file_simps = is_file_nil is_file_open is_file_closefd is_file_unlink is_file_linkhard is_file_other
(********* is_dir simpset **********)
lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)"
apply (frule vd_cons, drule vt_grant_os, rule_tac ext)
apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
split:if_splits option.splits t_inode_tag.split t_socket_type.splits
simp:is_dir_def dir_is_empty_def is_dir_def current_files_def)
done
lemma is_dir_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> is_dir (Rmdir p f # s) = (is_dir s) (f := False)"
apply (frule vd_cons, drule vt_grant_os, rule_tac ext)
apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
split:if_splits option.splits t_inode_tag.split t_socket_type.splits
simp:is_dir_def dir_is_empty_def is_dir_def current_files_def)
done
lemma is_dir_other:
"\<lbrakk>valid (e # s);
\<forall> p f. e \<noteq> Rmdir p f;
\<forall> p f i. e \<noteq> Mkdir p f i\<rbrakk> \<Longrightarrow> is_dir (e # s) = is_dir s"
apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e)
apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
split:if_splits option.splits t_inode_tag.split t_socket_type.splits
simp:is_file_def dir_is_empty_def is_dir_def current_files_def)
apply (drule file_of_pfd_is_file, simp)
apply (simp add:is_file_def split:t_inode_tag.splits option.splits)
done
lemmas is_dir_simps = is_dir_nil is_dir_mkdir is_dir_rmdir is_dir_other
(*********** no root dir involved ***********)
lemma root_is_dir: "valid s \<Longrightarrow> is_dir s []"
apply (induct s, simp add:is_dir_nil root_is_init_dir)
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto simp:is_dir_simps)
done
lemma root_is_dir': "\<lbrakk>is_file s []; valid s\<rbrakk> \<Longrightarrow> False"
apply (drule root_is_dir)
apply (erule file_dir_conflict, simp)
done
lemma noroot_execve:
"valid (Execve p f fds # s) \<Longrightarrow> f \<noteq> []"
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
lemma noroot_execve':
"valid (Execve p [] fds # s) \<Longrightarrow> False"
by (drule noroot_execve, simp)
lemma noroot_open:
"valid (Open p f flags fd opt # s) \<Longrightarrow> f \<noteq> []"
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir' split:option.splits)
lemma noroot_open':
"valid (Open p [] flags fd opt # s) \<Longrightarrow> False"
by (drule noroot_open, simp)
lemma noroot_filefd':
"\<lbrakk>file_of_proc_fd s p fd = Some []; valid s\<rbrakk> \<Longrightarrow> False"
apply (induct s arbitrary:p, simp)
apply (drule init_filefd_prop5, erule root_is_init_dir')
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto split:if_splits option.splits dest!:root_is_dir')
done
lemma noroot_filefd:
"\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> f \<noteq> []"
by (rule notI, simp, erule noroot_filefd', simp)
lemma noroot_unlink:
"valid (UnLink p f # s) \<Longrightarrow> f \<noteq> []"
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
lemma noroot_unlink':
"valid (UnLink p [] # s) \<Longrightarrow> False"
by (drule noroot_unlink, simp)
lemma noroot_rmdir:
"valid (Rmdir p f # s) \<Longrightarrow> f \<noteq> []"
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
lemma noroot_rmdir':
"valid (Rmdir p [] # s) \<Longrightarrow> False"
by (drule noroot_rmdir, simp)
lemma noroot_mkdir:
"valid (Mkdir p f inum # s) \<Longrightarrow> f \<noteq> []"
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
lemma noroot_mkdir':
"valid (Mkdir p [] inum # s) \<Longrightarrow> False"
by (drule noroot_mkdir, simp)
lemma noroot_linkhard:
"valid (LinkHard p f f' # s) \<Longrightarrow> f \<noteq> [] \<and> f' \<noteq> []"
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
lemma noroot_linkhard':
"valid (LinkHard p [] f # s) \<Longrightarrow> False"
by (drule noroot_linkhard, simp)
lemma noroot_linkhard'':
"valid (LinkHard p f [] # s) \<Longrightarrow> False"
by (drule noroot_linkhard, simp)
lemma noroot_truncate:
"valid (Truncate p f len # s) \<Longrightarrow> f \<noteq> []"
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
lemma noroot_truncate':
"valid (Truncate p [] len # s) \<Longrightarrow> False"
by (drule noroot_truncate, simp)
lemmas noroot_events = noroot_execve noroot_open noroot_filefd noroot_unlink noroot_rmdir
noroot_mkdir noroot_linkhard noroot_truncate
lemmas noroot_events' = noroot_execve' noroot_open' noroot_filefd' noroot_unlink' noroot_rmdir'
noroot_mkdir' noroot_linkhard' noroot_linkhard'' noroot_truncate'
lemma is_file_in_current:
"is_file s f \<Longrightarrow> f \<in> current_files s"
by (auto simp:is_file_def current_files_def split:option.splits)
lemma is_dir_in_current:
"is_dir s f \<Longrightarrow> f \<in> current_files s"
by (auto simp:is_dir_def current_files_def split:option.splits)
(* simpset for same_inode_files: Current_files_prop.thy *)
lemma same_inode_files_nil:
"same_inode_files [] = init_same_inode_files"
by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil)
lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>"
by (auto simp add:current_inode_nums_def current_file_inums_def)
lemma same_inode_files_open:
"valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'.
if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')"
apply (frule vt_grant_os, frule vd_cons, rule ext)
apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits
dest:iof's_im_in_cim iof's_im_in_cim')
apply (drule is_file_in_current)
apply (simp add:current_files_def)
done
lemma same_inode_files_linkhard:
"valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'.
if (f' = f \<or> f' \<in> same_inode_files s oldf)
then same_inode_files s oldf \<union> {f}
else same_inode_files s f')"
apply (frule vt_grant_os, frule vd_cons, rule ext)
apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits
dest:iof's_im_in_cim iof's_im_in_cim')
apply (drule is_file_in_current)
apply (simp add:current_files_def is_file_def)
apply (simp add:is_file_def)
done
lemma inum_of_file_none_prop:
"\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
by (simp add:current_files_def)
lemma same_inode_files_closefd:
"\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow>
same_inode_files (CloseFd p fd # s) f' = (
case (file_of_proc_fd s p fd) of
Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))
then same_inode_files s f' - {f}
else same_inode_files s f' )
| None \<Rightarrow> same_inode_files s f' )"
apply (frule vt_grant_os, frule vd_cons)
apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd
split:if_splits option.splits
dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)
done
lemma same_inode_files_unlink:
"\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>
\<Longrightarrow> same_inode_files (UnLink p f # s) f' = (
if (proc_fd_of_file s f = {})
then same_inode_files s f' - {f}
else same_inode_files s f')"
apply (frule vt_grant_os, frule vd_cons)
apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink
split:if_splits option.splits
dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)
done
lemma same_inode_files_mkdir:
"valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)"
apply (frule vt_grant_os, frule vd_cons, rule ext)
apply (auto simp:same_inode_files_def is_file_simps current_files_simps
split:if_splits option.splits
dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current)
apply (simp add:current_files_def is_file_def)
done
lemma same_inode_files_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> same_inode_files (e # s) = same_inode_files s"
apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e)
apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def
split:if_splits option.splits
dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir)
apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+
done
lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard
same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other
lemma same_inode_files_prop1:
"f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s"
by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits)
lemma same_inode_files_prop2:
"\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''"
by (auto dest:same_inode_files_prop1)
lemma same_inode_files_prop3:
"\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"
apply (rule notI)
apply (simp add:same_inode_files_def is_file_def is_dir_def
split:if_splits option.splits t_inode_tag.splits)
done
lemma same_inode_files_prop4:
"\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"
by (auto simp:same_inode_files_def split:if_splits)
lemma same_inode_files_prop5:
"f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"
by (auto simp:same_inode_files_def is_file_def split:if_splits)
lemma same_inode_files_prop6:
"f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f"
by (auto simp:same_inode_files_def is_file_def split:if_splits)
lemma same_inode_files_prop7:
"f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'"
by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
lemma same_inode_files_prop8:
"f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f"
by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
end
end