1 theory Proc_fd_of_file_prop

     2 imports Main Flask Flask_type Valid_prop Current_files_prop Current_sockets_prop

     3 begin

     4 

     5 context flask begin

     6 

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

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

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

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

    11 by (drule init_filefd_valid, simp)

    12 

    13 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"

    14 apply (induct \<tau>)

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

    16 apply (clarify, drule init_filefd_valid, simp)

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

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

    19 done

    20 

    21 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"

    22 by (rule proc_fd_in_fds_aux[rule_format], simp+)

    23 

    24 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>"

    25 by (auto simp:proc_fd_of_file_def intro:file_of_pfd_in_current)

    26 

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

    28 by (auto simp:proc_fd_file_in_cur)

    29 

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

    31 by (auto simp:proc_fd_file_in_cur')

    32 

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

    34 by (auto simp:proc_fd_of_file_def)

    35 

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

    37 by (auto simp:proc_fd_of_file_def)

    38 

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

    40 by (auto simp:proc_fd_of_file_def)

    41 

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

    43 by (auto simp:proc_fd_of_file_def)

    44 

    45 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>"

    46 by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur')

    47 

    48 lemma file_fds_subset_pfds:

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

    50 by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds)

    51 

    52 lemma filefd_socket_conflict:

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

    54 apply (induct s arbitrary:p)

    55 apply (simp add:current_sockets_simps init_filefd_prop8)

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

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

    58             dest:cn_in_curp cn_in_curfd proc_fd_in_fds)

    59 done

    60 

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

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

    63 

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

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

    66 

    67 lemma tcp_not_file_fd:

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

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

    70 apply (drule is_tcp_in_current)

    71 apply (drule filefd_socket_conflict, simp+)

    72 done

    73 

    74 lemma udp_not_file_fd:

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

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

    77 apply (drule is_udp_in_current)

    78 apply (drule filefd_socket_conflict, simp+)

    79 done

    80 

    81 lemma tcp_notin_file_fds:

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

    83 by (auto simp:proc_file_fds_def intro:tcp_not_file_fd)

    84 

    85 lemma udp_notin_file_fds:

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

    87 by (auto simp:proc_file_fds_def intro:udp_not_file_fd)

    88 

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

    90 (*

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

    92   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')"

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

    94 apply (frule vd_cons, drule vt_grant_os, case_tac iopt)

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

    96 done

    97 

    98 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) "

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

   100 

   101 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> 

   102   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)"

   103 apply (frule vt_grant_os, frule vd_cons)

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

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

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

   107 apply (auto simp add:proc_fd_of_file_def)[1]

   108 

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

   110 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)

   111 apply (drule file_of_pfd_in_current, simp+)

   112 apply (simp add:file_of_proc_fd.simps)

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

   114 apply (rule impI, simp add:file_before_rename_def)

   115 

   116 apply (simp add:proc_fd_of_file_def split:if_splits)

   117 apply auto

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

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

   120 apply (simp add:current_files_simps)

   121 apply (erule exE| erule conjE)+

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

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

   124 apply (simp add:file_after_rename_def)

   125 done

   126 

   127 

   128 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}"

   129 by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

   130 

   131 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'}"

   132 by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

   133 

   134 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}" 

   135 apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

   136 apply (frule vd_cons, drule vt_grant_os)

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

   138 done

   139 

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

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

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

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

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

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

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

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

   148 done

   149 

   150 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

   151 *)

   152 end

   153 

   154 

   155 end