theory Proc_fd_of_file_prop

imports Main Flask Flask_type Valid_prop Current_files_prop Current_sockets_prop

begin

context flask begin

lemma proc_fd_in_procs: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk>  \<Longrightarrow> p \<in> current_procs \<tau>"

apply (induct \<tau> arbitrary: f) defer

apply (frule vd_cons, frule vt_grant_os, case_tac a)

apply (auto simp:file_of_proc_fd.simps current_procs.simps os_grant.simps split:if_splits option.splits)

by (drule init_filefd_valid, simp)

lemma proc_fd_in_fds_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> fd \<in> current_proc_fds \<tau> p"

apply (induct \<tau>)

apply (simp add:file_of_proc_fd.simps current_proc_fds.simps)

apply (clarify, drule init_filefd_valid, simp)

apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a)

apply (auto simp:file_of_proc_fd.simps current_proc_fds.simps split:if_splits option.splits t_sock_addr.splits)

done

lemma proc_fd_in_fds: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds \<tau> p"

by (rule proc_fd_in_fds_aux[rule_format], simp+)

lemma proc_fd_file_in_cur: "\<lbrakk>(p, fd) \<in> proc_fd_of_file \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"

by (auto simp:proc_fd_of_file_def intro:file_of_pfd_in_current)

lemma proc_fd_file_in_cur': "\<lbrakk>proc_fd_of_file \<tau> f \<noteq> {}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"

by (auto simp:proc_fd_file_in_cur)

lemma proc_fd_file_in_cur'': "\<lbrakk>proc_fd_of_file \<tau> f = {(p,fd)}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"

by (auto simp:proc_fd_file_in_cur')

lemma procfd_of_file_imp_fpfd: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f"

by (auto simp:proc_fd_of_file_def)

lemma procfd_of_file_imp_fpfd': "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd \<noteq> None"

by (auto simp:proc_fd_of_file_def)

lemma procfd_of_file_eq_fpfd'': "(p, fd) \<in> proc_fd_of_file \<tau> f = (file_of_proc_fd \<tau> p fd = Some f)"

by (auto simp:proc_fd_of_file_def)

lemma procfd_of_file_non_empty: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> proc_fd_of_file \<tau> f \<noteq> {}"

by (auto simp:proc_fd_of_file_def)

lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"

by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur')

lemma file_fds_subset_pfds:

  "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p"

by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds)

lemma filefd_socket_conflict:

  "\<lbrakk>file_of_proc_fd s p fd = Some f; (p, fd) \<in> current_sockets s; valid s\<rbrakk> \<Longrightarrow> False"

apply (induct s arbitrary:p)

apply (simp add:current_sockets_simps init_filefd_prop8)

apply (frule vt_grant_os, frule vd_cons, frule file_fds_subset_pfds, case_tac a)

apply (auto simp:current_sockets_simps split:if_splits option.splits 

            dest:cn_in_curp cn_in_curfd proc_fd_in_fds)

done

lemma is_tcp_in_current: "is_tcp_sock s sock \<Longrightarrow> sock \<in> current_sockets s"

by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits)

lemma is_udp_in_current: "is_udp_sock s sock \<Longrightarrow> sock \<in> current_sockets s"

by (auto simp:is_udp_sock_def current_sockets_def split:option.splits)

lemma tcp_not_file_fd:

  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"

apply (case_tac "file_of_proc_fd s p fd", simp)

apply (drule is_tcp_in_current)

apply (drule filefd_socket_conflict, simp+)

done

lemma udp_not_file_fd:

  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"

apply (case_tac "file_of_proc_fd s p fd", simp)

apply (drule is_udp_in_current)

apply (drule filefd_socket_conflict, simp+)

done

lemma tcp_notin_file_fds:

  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"

by (auto simp:proc_file_fds_def intro:tcp_not_file_fd)

lemma udp_notin_file_fds:

  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"

by (auto simp:proc_file_fds_def intro:udp_not_file_fd)

(******************* rebuild proc_fd_of_file simpset ***********************)

(*

lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow> 

  proc_fd_of_file (Open p f flags fd iopt # \<tau>) f' = (if (f' = f) then insert (p, fd) (proc_fd_of_file \<tau> f') else proc_fd_of_file \<tau> f')"

apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits)

apply (frule vd_cons, drule vt_grant_os, case_tac iopt)

apply (drule proc_fd_in_fds, simp, simp add:os_grant.simps nfd_notin_curfd)+

done

lemma proc_fd_of_file_closefd: "proc_fd_of_file (CloseFd p fd # \<tau>) f = (if (file_of_proc_fd \<tau> p fd = Some f) then (proc_fd_of_file \<tau> f - {(p,fd)}) else proc_fd_of_file \<tau> f) "

by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits)

lemma proc_fd_of_file_rename: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>)\<rbrakk> \<Longrightarrow> 

  proc_fd_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (if (f\<^isub>3 \<preceq> f) then proc_fd_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) else proc_fd_of_file \<tau> f)"

apply (frule vt_grant_os, frule vd_cons)

apply (case_tac "f\<^isub>3 \<preceq> f")

apply (subgoal_tac "f \<notin> current_files \<tau>") prefer 2 apply (rule notI)

apply (clarsimp simp:os_grant.simps, drule_tac f = f\<^isub>3 and f' = f in ancenf_in_current, simp, simp, simp)

apply (auto simp add:proc_fd_of_file_def)[1]

apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)

apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>1 = aa and f\<^isub>2 = f\<^isub>2 in file_renaming_prop5, simp)

apply (drule file_of_pfd_in_current, simp+)

apply (simp add:file_of_proc_fd.simps)

apply (rule conjI, rule impI, simp add:file_renaming_prop5')

apply (rule impI, simp add:file_before_rename_def)

apply (simp add:proc_fd_of_file_def split:if_splits)

apply auto

apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)

apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>2 = f\<^isub>2 and f = aa in file_renaming_prop1, simp)

apply (simp add:current_files_simps)

apply (erule exE| erule conjE)+

apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)

apply (drule_tac f = f\<^isub>1 in rename_renaming_decom', simp+)

apply (simp add:file_after_rename_def)

done

lemma proc_fd_of_file_kill: "proc_fd_of_file (Kill p\<^isub>1 p\<^isub>2 # \<tau>) f = {(p, fd). (p, fd) \<in> proc_fd_of_file \<tau> f \<and> p \<noteq> p\<^isub>2}"

by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

lemma proc_fd_of_file_exit: "proc_fd_of_file (Exit p' # \<tau>) f = {(p, fd). (p, fd) \<in> proc_fd_of_file \<tau> f \<and> p \<noteq> p'}"

by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

lemma proc_fd_of_file_clone: "Clone p\<^isub>1 p\<^isub>2 # valid \<tau> \<Longrightarrow> proc_fd_of_file (Clone p\<^isub>1 p\<^isub>2 # \<tau>) f = proc_fd_of_file \<tau> f \<union> {(p\<^isub>2, fd)| fd. (p\<^isub>1, fd) \<in> proc_fd_of_file \<tau> f}" 

apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

apply (frule vd_cons, drule vt_grant_os)

apply (drule proc_fd_in_procs, (simp add:os_grant.simps np_notin_curp)+)

done

lemma proc_fd_of_file_other: "\<lbrakk>e # valid \<tau>;

                               \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

                               \<forall> p fd. e \<noteq> CloseFd p fd;

                               \<forall> p f f'. e \<noteq> Rename p f f';

                               \<forall> p p'. e \<noteq> Kill p p';

                               \<forall> p. e \<noteq> Exit p;

                               \<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> proc_fd_of_file (e # \<tau>) f = proc_fd_of_file \<tau> f"

apply (case_tac e, auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

done

lemmas proc_fd_of_file_simps = proc_fd_of_file_open proc_fd_of_file_closefd proc_fd_of_file_rename proc_fd_of_file_kill proc_fd_of_file_exit proc_fd_of_file_clone proc_fd_of_file_other

*)

end

end