1 (*<*)

     2 theory Init_prop

     3 imports Main OS_type_def Flask Flask_type Static_type Static

     4 begin

     5 (*>*)

     6 

     7 context init begin

     8 

     9 lemma init_files_prop1: "init_inum_of_file f = Some im \<Longrightarrow> f \<in> init_files"

    10 by (simp add:inof_has_file_tag)

    11 

    12 lemma init_files_prop2: "finite init_files" 

    13 by (simp add:init_finite_sets)

    14 

    15 lemma init_files_prop3: "f \<in> init_files \<Longrightarrow> init_inum_of_file f \<noteq> None"

    16 by (auto dest:init_file_has_inum)

    17 

    18 lemma init_files_prop4: "(f \<in> init_files) = (f \<in> current_files [])"

    19 apply (simp add:current_files_def, rule iffI)

    20 using init_files_prop1 init_files_prop3 by auto

    21 

    22 lemmas init_files_props = init_file_has_inum init_files_prop1 init_files_prop2 init_files_prop3 init_files_prop4

    23 

    24 lemma init_inumof_prop1: "init_inum_of_file f = Some im \<Longrightarrow> \<exists> tag. init_itag_of_inum im = Some tag"

    25 by (auto dest:inof_has_file_tag)

    26 

    27 lemma init_inumof_prop2:  "init_inum_of_file f = Some im \<Longrightarrow> init_itag_of_inum im \<noteq> None"

    28 by (auto dest:inof_has_file_tag)

    29 

    30 lemma init_inumof_prop3: "\<lbrakk>init_inum_of_file f = Some im; init_itag_of_inum im = Some tag\<rbrakk> \<Longrightarrow> is_file_dir_itag tag"

    31 by (auto dest:inof_has_file_tag)

    32 

    33 lemmas init_inum_of_file_props = init_files_prop1 init_inumof_prop1 init_inumof_prop2 init_inumof_prop3

    34 

    35 lemma init_inumos_prop1: "init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets"

    36 by (auto dest:inos_has_sock_tag)

    37 

    38 lemma init_inumos_prop2: "init_inum_of_socket s = Some im \<Longrightarrow> init_itag_of_inum im = Some Tag_TCP_SOCK \<or> init_itag_of_inum im = Some Tag_UDP_SOCK"

    39 apply (auto dest!:inos_has_sock_tag) 

    40 apply (case_tac tag, simp+)

    41 done

    42 

    43 lemma init_inumos_prop3: "init_inum_of_socket s = Some im \<Longrightarrow> init_itag_of_inum im \<noteq> None"

    44 by (auto dest:inos_has_sock_tag)

    45 

    46 lemma init_inumos_prop4: "init_inum_of_socket s = Some im \<Longrightarrow> \<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag"

    47 by (auto dest!:inos_has_sock_tag) 

    48 

    49 lemmas init_inum_of_socket_props = init_inumos_prop1 init_inumos_prop2 init_inumos_prop3 init_inumos_prop4

    50 

    51 lemma init_sockets_prop1: "(p, fd) \<in> init_sockets \<Longrightarrow> p \<in> init_procs"

    52 by (auto dest: init_socket_has_inode)

    53 

    54 lemma init_sockets_prop2: "(p, fd) \<in> init_sockets \<Longrightarrow> fd \<in> init_fds_of_proc p"

    55 by (auto dest:init_socket_has_inode)

    56 

    57 lemma init_sockets_prop3: "s \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket s = Some im"

    58 by (case_tac s, auto dest:init_socket_has_inode)

    59 

    60 lemma init_sockets_prop4: "s \<in> init_sockets \<Longrightarrow> init_inum_of_socket s \<noteq> None"

    61 by (simp add:init_sockets_prop3)

    62 

    63 lemma init_sockets_prop5: "s \<in> init_sockets = (s \<in> current_sockets [])"

    64 apply (simp add:current_sockets_def, rule iffI)

    65 using init_sockets_prop4 inos_has_sock_tag apply auto

    66 apply (case_tac s, auto)

    67 done

    68 

    69 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5

    70 

    71 lemma is_init_file_prop1: "is_init_file f = (f \<in> init_files \<and> is_file [] f)"

    72 by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits)

    73 

    74 lemma is_init_file_prop2: "is_init_file f = (init_alive (O_file f))"

    75 by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits)

    76 

    77 lemmas is_init_file_props = is_init_file_prop1 is_init_file_prop2

    78 

    79 lemma is_init_dir_prop1: "is_init_dir f = (f \<in> init_files \<and> is_dir [] f)"

    80 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)

    81 

    82 lemma is_init_dir_prop2: "is_init_dir f = (init_alive (O_dir f))"

    83 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)

    84 

    85 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2

    86 

    87 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)"

    88 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 

    89                 dest:init_socket_has_inode split:option.splits)       

    90 done

    91 

    92 lemma is_init_udp_sock_prop2: "is_init_udp_sock s = (init_alive (O_udp_sock s))"

    93 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 

    94                 dest:init_socket_has_inode split:option.splits)       

    95 done

    96 

    97 lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2

    98 

    99 lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)"

   100 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 

   101                 dest:init_socket_has_inode split:option.splits)       

   102 done

   103 

   104 lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s = (init_alive (O_tcp_sock s))"

   105 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 

   106                 dest:init_socket_has_inode split:option.splits)       

   107 done

   108 

   109 lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2

   110 

   111 

   112 lemma init_parent_file_prop1: 

   113   "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"

   114 apply (frule parent_file_in_init, simp, frule_tac f = pf in init_files_prop3)

   115 apply (clarsimp, drule_tac im = y in init_parentf_is_dir, simp+)

   116 by (simp add:is_init_dir_def)

   117 

   118 lemma init_parent_file_prop1': 

   119   "a # f \<in> init_files \<Longrightarrow> is_init_dir f"

   120 by (rule_tac pf = f in init_parent_file_prop1, auto)

   121 

   122 lemma init_parent_file_prop2:

   123   "\<lbrakk>parent f = Some pf; is_init_file f\<rbrakk> \<Longrightarrow> is_init_dir pf"

   124 by (rule init_parent_file_prop1, simp, simp add: is_init_file_props)

   125 

   126 lemma init_parent_file_prop2':

   127   "is_init_file (f#pf) \<Longrightarrow> is_init_dir pf"

   128 apply (rule init_parent_file_prop2)

   129 by auto

   130 

   131 lemma init_parent_file_prop3:

   132   "\<lbrakk>parent f = Some pf; is_init_dir f\<rbrakk> \<Longrightarrow> is_init_dir pf"

   133 by (rule init_parent_file_prop1, simp, simp add: is_init_dir_props)

   134 

   135 lemma init_parent_file_prop3':

   136   "is_init_dir (f#pf) \<Longrightarrow> is_init_dir pf"

   137 apply (rule init_parent_file_prop3)

   138 by auto

   139 

   140 lemma parent_file_in_init': "a # f \<in> init_files \<Longrightarrow> f \<in> init_files"

   141 by (subgoal_tac "parent (a # f) = Some f", drule parent_file_in_init, auto)

   142 

   143 lemmas init_parent_file_props = parent_file_in_init init_parent_file_prop1 parent_file_in_init' init_parent_file_prop1' init_parent_file_prop2 init_parent_file_prop2' init_parent_file_prop3 init_parent_file_prop3'

   144 

   145 lemma root_in_filesystem:  "[] \<in> init_files" 

   146 using init_files_prop1 root_is_dir by auto

   147 

   148 lemma root_is_init_dir: "is_init_dir []"

   149 using root_is_dir

   150 by (auto simp add:is_init_dir_def split:option.splits)

   151 

   152 lemma root_is_init_dir': "is_init_file [] \<Longrightarrow> False"

   153 using root_is_dir

   154 by (auto simp:is_init_file_def split:option.splits)

   155 

   156 

   157 lemma init_files_hung_prop1: "f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files"

   158 by (auto dest:init_files_hung_valid)

   159 

   160 lemma init_files_hung_prop2: "f \<in> init_files_hung_by_del \<Longrightarrow> \<exists> p fd. init_file_of_proc_fd p fd = Some f"

   161 by (auto dest:init_files_hung_valid)

   162 

   163 lemmas init_files_hung_by_del_props = init_files_hung_prop1 init_files_hung_prop2 init_files_hung_valid'

   164 

   165 

   166 lemma init_fds_of_proc_prop1: "fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs"

   167 by (auto dest!:init_procfds_valid)

   168 

   169 lemma init_fds_of_proc_prop2: "fd \<in> init_fds_of_proc p \<Longrightarrow> (\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets"

   170 by (auto dest:init_procfds_valid)

   171 

   172 lemmas init_fds_of_proc_props = init_fds_of_proc_prop1 init_fds_of_proc_prop2

   173 

   174 lemma init_filefd_prop1: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> f \<in> init_files"

   175 by (auto dest!:init_filefd_valid intro:init_files_prop1)

   176 

   177 lemma init_filefd_prop2: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> p \<in> init_procs"

   178 by (auto dest:init_filefd_valid)

   179 

   180 lemma init_filefd_prop3: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p"

   181 by (auto dest:init_filefd_valid)

   182 

   183 lemma init_filefd_prop4: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<exists> flags. init_oflags_of_proc_fd p fd = Some flags"

   184 by (auto dest:init_filefd_valid)

   185 

   186 lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f"

   187 by (auto dest:init_filefd_valid simp:is_init_file_def)

   188 

   189 lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5

   190 

   191 lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs"

   192 by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)

   193 

   194 lemma init_oflags_prop2: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> fd \<in> init_fds_of_proc p"

   195 by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)

   196 

   197 lemmas init_oflags_of_proc_fd_props = init_oflags_prop1 init_oflags_prop2 init_fileflag_valid

   198 

   199 (*

   200 lemma init_socketstate_prop1: "s \<in> init_sockets \<Longrightarrow> init_socket_state s \<noteq> None"

   201 using init_socket_has_state

   202 by (case_tac s, simp add:bidirect_in_init_def)

   203 

   204 lemma init_socketstate_prop2: "s \<in> init_sockets \<Longrightarrow> \<exists> t. init_socket_state s = Some t"

   205 using init_socket_has_state

   206 by (case_tac s, simp add:bidirect_in_init_def)

   207 

   208 lemma init_socketstate_prop3: "init_socket_state s = Some t \<Longrightarrow> s \<in> init_sockets"

   209 using init_socket_has_state

   210 by (case_tac s, simp add:bidirect_in_init_def)

   211 

   212 lemmas init_socket_state_props = init_socketstate_prop1 init_socketstate_prop2 init_socketstate_prop3

   213 *)

   214 

   215 lemma init_inum_sock_file_noninter: "\<lbrakk>init_inum_of_socket s = Some im; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> False"

   216 apply (frule init_inumof_prop1, erule exE, drule init_inumof_prop3, simp)

   217 apply (frule init_inumos_prop2)

   218 apply (case_tac tag, simp+)

   219 done

   220 

   221 lemma init_parent_file_has_inum: "\<lbrakk>parent f = Some pf; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> \<exists> im. init_inum_of_file pf = Some im"

   222 by (drule init_files_prop1, drule parent_file_in_init, simp, simp add:init_files_props)

   223 

   224 lemma init_file_has_no_son': "\<lbrakk>init_itag_of_inum im = Some Tag_FILE; init_inum_of_file f = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> init_inum_of_file f' = None"

   225 apply (drule init_file_no_son, simp)

   226 by (case_tac "init_inum_of_file f'", auto dest:init_files_prop1)

   227 

   228 lemma init_parent_file_is_dir': "\<lbrakk>parent f = Some pf; init_inum_of_file f = Some im; init_inum_of_file pf = Some ipm\<rbrakk> \<Longrightarrow> init_itag_of_inum ipm = Some Tag_DIR"

   229 by (drule init_parentf_is_dir, auto dest:init_files_prop1)

   230 

   231 lemma init_file_hung_has_no_son: "\<lbrakk>f \<in> init_files_hung_by_del; parent f' = Some f; init_inum_of_file f' = Some im\<rbrakk> \<Longrightarrow> False"

   232 apply (frule init_files_hung_prop1, drule init_file_has_inum, erule exE)

   233 apply (drule init_files_hung_valid', simp)

   234 apply (frule init_parent_file_is_dir', simp+)

   235 apply (drule init_files_prop1)

   236 apply (erule_tac x = f' in allE, simp)

   237 by (case_tac f', simp_all add:no_junior_def)

   238 

   239 

   240 end

   241 

   242 context flask begin

   243 

   244 lemma init_alive_prop: "init_alive obj = alive [] obj"

   245 apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props

   246          is_init_udp_sock_props init_files_props init_sockets_props)

   247 done

   248 

   249 lemma init_alive_proc: "p \<in> init_procs \<Longrightarrow> init_alive (O_proc p)" by simp

   250 lemma init_alive_file: "is_init_file f \<Longrightarrow> init_alive (O_file f)" by simp

   251 lemma init_alive_dir: "is_init_dir f \<Longrightarrow> init_alive (O_dir f)" by simp

   252 lemma init_alive_fd: "fd \<in> init_fds_of_proc p \<Longrightarrow> init_alive (O_fd p fd)" by simp

   253 lemma init_alive_tcp: "is_init_tcp_sock s \<Longrightarrow> init_alive (O_tcp_sock s)" by simp

   254 lemma init_alive_udp: "is_init_udp_sock s \<Longrightarrow> init_alive (O_udp_sock s)" by simp

   255 lemma init_alive_node: "n \<in> init_nodes \<Longrightarrow> init_alive (O_node n)" by simp

   256 lemma init_alive_shm: "h \<in> init_shms \<Longrightarrow> init_alive (O_shm h)" by simp

   257 lemma init_alive_msgq: "q \<in> init_msgqs \<Longrightarrow> init_alive (O_msgq q)" by simp

   258 lemma init_alive_msg: "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk>

   259   \<Longrightarrow> init_alive (O_msg q m)" by simp

   260 

   261 lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd 

   262   init_alive_tcp init_alive_udp init_alive_node init_alive_shm init_alive_msgq init_alive_msg

   263 

   264 

   265 lemma init_file_type_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_type_of_obj (O_file f) = Some t"

   266 using init_obj_has_type

   267 by (auto simp:is_init_file_def split:option.splits)

   268 

   269 lemma init_file_type_prop2: "is_init_file f \<Longrightarrow> init_type_of_obj (O_file f) \<noteq> None"

   270 by (simp add:init_file_type_prop1)

   271 

   272 lemma init_file_type_prop3: "init_type_of_obj (O_file f) = Some t \<Longrightarrow> f \<in> init_files"

   273 apply (drule init_type_has_obj) 

   274 by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)

   275 

   276 lemma init_file_type_prop4: "init_type_of_obj (O_file f) = Some t \<Longrightarrow> is_init_file f"

   277 apply (drule init_type_has_obj) 

   278 by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)

   279 

   280 lemmas init_file_types_props = init_file_type_prop1 init_file_type_prop2 init_file_type_prop3 init_file_type_prop4

   281 

   282 lemma init_dir_type_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_type_of_obj (O_dir f) = Some t"

   283 using init_obj_has_type

   284 by (auto simp:is_init_dir_def split:option.splits)

   285 

   286 lemma init_dir_type_prop2: "is_init_dir f \<Longrightarrow> init_type_of_obj (O_dir f) \<noteq> None"

   287 by (simp add:init_dir_type_prop1)

   288 

   289 lemma init_dir_type_prop3: "init_type_of_obj (O_dir f) = Some t \<Longrightarrow> f \<in> init_files"

   290 apply (drule init_type_has_obj) 

   291 by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)

   292 

   293 lemma init_dir_type_prop4: "init_type_of_obj (O_dir f) = Some t \<Longrightarrow> is_init_dir f"

   294 apply (drule init_type_has_obj) 

   295 by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)

   296 

   297 lemmas init_dir_types_props = init_dir_type_prop1 init_dir_type_prop2 init_dir_type_prop3 init_dir_type_prop4

   298 

   299 lemma init_procrole_prop1: "init_role_of_proc p = Some r \<Longrightarrow> p \<in> init_procs"

   300 using init_proc_has_role

   301 by (auto simp:bidirect_in_init_def)

   302 

   303 lemma init_procrole_prop2: "p \<in> init_procs \<Longrightarrow> \<exists> r. init_role_of_proc p = Some r"

   304 using init_proc_has_role

   305 by (auto simp:bidirect_in_init_def)

   306 

   307 lemma init_procrole_prop3: "p \<in> init_procs \<Longrightarrow> init_role_of_proc p \<noteq> None"

   308 using init_proc_has_role

   309 by (auto simp:bidirect_in_init_def)

   310 

   311 lemmas init_role_of_proc_props = init_procrole_prop1 init_procrole_prop2 init_procrole_prop3

   312 

   313 lemma init_file_user_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_user_of_obj (O_file f) = Some t"

   314 apply (simp only: is_init_file_prop2)

   315 by (drule init_obj_has_user, auto)

   316 

   317 lemma init_file_user_prop2: "is_init_file f \<Longrightarrow> init_user_of_obj (O_file f) \<noteq> None"

   318 by (simp add:init_file_user_prop1)

   319 

   320 lemma init_file_user_prop3: "init_user_of_obj (O_file f) = Some t \<Longrightarrow> f \<in> init_files"

   321 apply (drule init_user_has_obj) 

   322 by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)

   323 

   324 lemma init_file_user_prop4: "init_user_of_obj (O_file f) = Some t \<Longrightarrow> is_init_file f"

   325 apply (drule init_user_has_obj) 

   326 by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)

   327 

   328 lemma init_file_user_prop5: "init_user_of_obj (O_file f) = Some u \<Longrightarrow> u \<in> init_users"

   329 by (simp add:init_user_has_obj)

   330 

   331 lemmas init_file_users_props = init_file_user_prop1 init_file_user_prop2 init_file_user_prop3 init_file_user_prop4 init_file_user_prop5

   332 

   333 lemma init_dir_user_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_user_of_obj (O_dir f) = Some t"

   334 apply (simp only: is_init_dir_prop2)

   335 by (drule init_obj_has_user, auto)

   336 

   337 lemma init_dir_user_prop2: "is_init_dir f \<Longrightarrow> init_user_of_obj (O_dir f) \<noteq> None"

   338 by (simp add:init_dir_user_prop1)

   339 

   340 lemma init_dir_user_prop3: "init_user_of_obj (O_dir f) = Some t \<Longrightarrow> f \<in> init_files"

   341 apply (drule init_user_has_obj) 

   342 by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)

   343 

   344 lemma init_dir_user_prop4: "init_user_of_obj (O_dir f) = Some t \<Longrightarrow> is_init_dir f"

   345 apply (drule init_user_has_obj) 

   346 by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)

   347 

   348 lemma init_dir_user_prop5: "init_user_of_obj (O_dir f) = Some u \<Longrightarrow> u \<in> init_users"

   349 by (simp add:init_user_has_obj)

   350 

   351 lemmas init_dir_users_props = init_dir_user_prop1 init_dir_user_prop2 init_dir_user_prop3 init_dir_user_prop4 init_dir_user_prop5

   352 

   353 end

   354 

   355 

   356 context tainting_s begin

   357 

   358 lemma init_file_has_ctxt:

   359   "is_init_file f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_file f) = Some sec"

   360 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   361 apply (rule conjI, rule init_obj_has_user, simp add:is_init_file_props)

   362 by (simp add:init_file_types_props)

   363 

   364 lemma init_file_has_ctxt':

   365   "init_sectxt_of_obj (O_file f) = None \<Longrightarrow> \<not> is_init_file f"

   366 by (rule notI, drule init_file_has_ctxt, simp)

   367 

   368 lemma init_dir_has_ctxt:

   369   "is_init_dir f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_dir f) = Some sec"

   370 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   371 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   372 by (simp add:init_dir_types_props)

   373 

   374 lemma init_dir_has_ctxt':

   375   "init_sectxt_of_obj (O_dir f) = None \<Longrightarrow> \<not> is_init_dir f"

   376 by (rule notI, drule init_dir_has_ctxt, simp)

   377 

   378 lemma init_proc_has_ctxt:

   379   "p \<in> init_procs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_proc p) = Some sec"

   380 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   381 apply (rule conjI, rule init_obj_has_user, simp)

   382 apply (frule init_alive_proc, drule init_obj_has_type)

   383 by (drule init_procrole_prop2, auto)

   384 

   385 lemma init_proc_has_ctxt':

   386   "init_sectxt_of_obj (O_proc p) = None \<Longrightarrow> p \<notin> init_procs"

   387 by (rule notI, drule init_proc_has_ctxt, simp)

   388 

   389 lemma init_fd_has_ctxt:

   390   "fd \<in> init_fds_of_proc p \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_fd p fd) = Some sec"

   391 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   392 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   393 apply (drule init_alive_intros)

   394 apply (drule init_obj_has_type, clarsimp)

   395 done

   396 

   397 lemma init_fd_has_ctxt':

   398   "init_sectxt_of_obj (O_fd p fd) = None \<Longrightarrow> fd \<notin> init_fds_of_proc p"

   399 by (rule notI, drule init_fd_has_ctxt, simp)

   400 

   401 lemma init_node_has_ctxt:

   402   "n \<in> init_nodes \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_node n) = Some sec"

   403 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   404 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   405 apply (drule init_alive_intros)

   406 apply (drule init_obj_has_type, clarsimp)

   407 done

   408 

   409 lemma init_node_has_ctxt':

   410   "init_sectxt_of_obj (O_node n) = None \<Longrightarrow> n \<notin> init_nodes"

   411 by (rule notI, drule init_node_has_ctxt, simp)

   412 

   413 lemma init_tcp_has_ctxt:

   414   "is_init_tcp_sock s \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_tcp_sock s) = Some sec"

   415 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   416 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   417 apply (drule init_alive_intros)

   418 apply (drule init_obj_has_type, clarsimp)

   419 done

   420 

   421 lemma init_tcp_has_ctxt':

   422   "init_sectxt_of_obj (O_tcp_sock s) = None \<Longrightarrow> \<not> is_init_tcp_sock s"

   423 by (rule notI, drule init_tcp_has_ctxt, simp)

   424 

   425 lemma init_udp_has_ctxt:

   426   "is_init_udp_sock s \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_udp_sock s) = Some sec"

   427 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   428 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   429 by (drule init_alive_intros, drule init_obj_has_type, clarsimp)

   430 

   431 lemma init_udp_has_ctxt':

   432   "init_sectxt_of_obj (O_udp_sock s) = None \<Longrightarrow> \<not> is_init_udp_sock s"

   433 by (rule notI, drule init_udp_has_ctxt, simp)

   434 

   435 lemma init_shm_has_ctxt:

   436   "h \<in> init_shms \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_shm h) = Some sec"

   437 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   438 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   439 by (drule init_alive_intros, drule init_obj_has_type, clarsimp)

   440 

   441 lemma init_shm_has_ctxt':

   442   "init_sectxt_of_obj (O_shm h) = None \<Longrightarrow> h \<notin> init_shms"

   443 by (rule notI, drule init_shm_has_ctxt, simp)

   444 

   445 lemma init_msgq_has_ctxt:

   446   "q \<in> init_msgqs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msgq q) = Some sec"

   447 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   448 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   449 by (drule init_alive_intros, drule init_obj_has_type, clarsimp)

   450 

   451 lemma init_msgq_has_ctxt':

   452   "init_sectxt_of_obj (O_msgq q) = None \<Longrightarrow> q \<notin> init_msgqs"

   453 by (rule notI, drule init_msgq_has_ctxt, simp)

   454 

   455 lemma init_msg_has_ctxt:

   456   "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msg q m) = Some sec"

   457 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   458 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   459 by (drule init_alive_intros, simp, drule init_obj_has_type, clarsimp)

   460 

   461 lemma init_msg_has_ctxt':

   462   "init_sectxt_of_obj (O_msg q m) = None \<Longrightarrow> m \<notin> set (init_msgs_of_queue q) \<or> q \<notin> init_msgqs"

   463 by (auto dest:init_msg_has_ctxt)

   464 

   465 lemma init_rootf_has_ctxt:

   466   "\<exists> sec. init_sectxt_of_obj (O_dir []) = Some sec"

   467 apply (rule init_dir_has_ctxt, simp add:is_init_dir_def split:option.splits)

   468 using root_is_dir by auto

   469 

   470 lemma init_rootf_has_ctxt':

   471   "init_sectxt_of_obj (O_dir []) = None \<Longrightarrow> False" 

   472 using init_rootf_has_ctxt by auto

   473 

   474 lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt

   475   init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt init_shm_has_ctxt init_msgq_has_ctxt

   476   init_msg_has_ctxt init_rootf_has_ctxt

   477 

   478 lemmas init_has_ctxt' = init_file_has_ctxt' init_dir_has_ctxt' init_proc_has_ctxt' init_fd_has_ctxt'

   479   init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' init_shm_has_ctxt' init_msgq_has_ctxt'

   480   init_msg_has_ctxt' init_rootf_has_ctxt'

   481 

   482 lemma sec_of_root_valid:

   483   "init_sectxt_of_obj (O_dir []) = Some sec_of_root"

   484 using init_rootf_has_ctxt

   485 by (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits)

   486 

   487 lemma sec_of_root_is_tuple:

   488   "\<exists> u t. sec_of_root = (u, R_object, t)"

   489 using sec_of_root_valid

   490 by (auto simp:sec_of_root_def init_sectxt_of_obj_def split:option.splits)

   491 

   492 lemma sroot_valid:

   493   "init_cf2sfile [] = Some sroot"

   494 by (simp add:init_cf2sfile_def)

   495 

   496 lemma sroot_valid':

   497   "cf2sfile s [] False = Some sroot"

   498 by (simp add:cf2sfile_def)  

   499 

   500 lemma init_sectxt_prop:

   501   "sectxt_of_obj [] obj = init_sectxt_of_obj obj"

   502 apply (auto simp:init_sectxt_of_obj_def sectxt_of_obj_def split:option.splits)

   503 apply (case_tac [!] obj, simp+)

   504 done

   505 

   506 lemma init_sectxt_prop2:

   507   "init_sectxt_of_obj obj = Some sec \<Longrightarrow> init_alive obj"

   508 by (case_tac obj, auto simp:init_sectxt_of_obj_def split:option.splits dest:init_type_has_obj)

   509 

   510 lemma init_dir_has_seclist:

   511   "is_init_dir f \<Longrightarrow> \<exists> seclist. get_parentfs_ctxts [] f = Some seclist"

   512 apply (induct f)

   513 apply (simp only:get_parentfs_ctxts.simps init_sectxt_prop)

   514 using init_rootf_has_ctxt apply (auto)[1]

   515 apply (frule init_parent_file_prop3', simp del:get_parentfs_ctxts.simps)

   516 apply (erule exE, drule init_dir_has_ctxt)

   517 by (auto simp add:init_sectxt_prop)

   518 

   519 lemma is_init_file_dir_prop1:

   520   "is_init_dir f \<Longrightarrow> \<not> is_init_file f"

   521 by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

   522 

   523 lemma is_init_file_dir_prop2:

   524   "is_init_file f \<Longrightarrow> \<not> is_init_dir f"

   525 by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

   526 

   527 lemma is_init_file_dir_prop3:

   528   "\<lbrakk>is_init_dir f; is_init_file f\<rbrakk> \<Longrightarrow> False"

   529 by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

   530 

   531 lemma is_init_file_dir_prop4:

   532   "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"

   533 by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

   534 

   535 lemmas is_init_file_dir_props = is_init_file_dir_prop1 is_init_file_dir_prop2 is_init_file_dir_prop3 is_init_file_dir_prop4

   536 

   537 lemma init_dir_has_sfile:

   538   "is_init_dir f \<Longrightarrow> \<exists> sf. init_cf2sfile f = Some sf"

   539 apply (case_tac f)

   540 using init_rootf_has_ctxt apply (auto)[1]

   541 apply (simp add:sec_of_root_valid sroot_valid sroot_def)

   542 apply (simp, frule init_parent_file_prop3')

   543 apply (frule_tac f = list in init_dir_has_seclist)

   544 apply (frule_tac f = list in init_dir_has_ctxt)

   545 apply (frule_tac f = "a # list" in init_dir_has_ctxt)

   546 apply ((erule exE)+, case_tac sec, auto simp:init_cf2sfile_def split:option.splits)

   547 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

   548 

   549 lemma init_file_has_sfile:

   550   "is_init_file f \<Longrightarrow> \<exists> sf. init_cf2sfile f = Some sf"

   551 apply (case_tac f)

   552 apply (simp, drule root_is_init_dir', simp)

   553 apply (simp, frule init_parent_file_prop2')

   554 apply (frule_tac f = list in init_dir_has_seclist)

   555 apply (frule_tac f = list in init_dir_has_ctxt)

   556 apply (frule_tac f = "a # list" in init_file_has_ctxt)

   557 by ((erule exE)+, case_tac sec, auto simp:init_cf2sfile_def)

   558   

   559 lemma init_shm_has_sshm:

   560   "h \<in> init_shms \<Longrightarrow> \<exists> sh. init_ch2sshm h = Some sh"

   561 apply (drule init_shm_has_ctxt)

   562 by (auto simp add:init_ch2sshm_def)

   563 

   564 lemma init_proc_has_sproc:

   565   "p \<in> init_procs \<Longrightarrow> \<exists> sp. init_cp2sproc p = Some sp"

   566 apply (frule init_proc_has_ctxt, erule exE)

   567 apply (simp add:init_cp2sproc_def)

   568 by (case_tac sec, simp+)

   569 

   570 lemma init_cqm2sms_has_sms_aux:

   571   "\<forall> m \<in> set ms. init_sectxt_of_obj (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. init_cqm2sms q ms = Some sms)"

   572 by (induct ms, auto split:option.splits simp:init_cm2smsg_def)

   573 

   574 lemma init_cqm2sms_has_sms: 

   575   "q \<in> init_msgqs \<Longrightarrow> \<exists> sms. init_cqm2sms q (init_msgs_of_queue q) = Some sms"

   576 apply (rule init_cqm2sms_has_sms_aux)

   577 using init_msg_has_ctxt by auto

   578 

   579 lemma init_msgq_has_smsgq:

   580   "q \<in> init_msgqs \<Longrightarrow> \<exists> sq. init_cq2smsgq q = Some sq"

   581 apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)

   582 apply (simp add:init_cq2smsgq_def)

   583 by (case_tac sec, simp+)

   584 

   585 lemma cf2sfile_nil_prop1:

   586   "f \<in> init_files \<Longrightarrow> cf2sfile [] f (is_init_file f) = init_cf2sfile f"

   587 apply (case_tac f)

   588 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)

   589 apply (rule notI, drule root_is_init_dir', simp)

   590 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')

   591 apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits

   592             dest:init_file_has_inum inof_has_file_tag)

   593 done

   594 

   595 lemma init_file_dir_conflict: "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"

   596 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

   597 

   598 lemma init_file_dir_conflict1: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"

   599 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

   600 

   601 lemma init_file_dir_conflict2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"

   602 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

   603 

   604 lemma init_sec_file_dir:

   605   "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False"

   606 apply (drule init_sectxt_prop2)+

   607 apply (auto intro:init_file_dir_conflict)

   608 done

   609 

   610 lemma cf2sfile_nil_prop2:

   611   "f \<in> init_files \<Longrightarrow> cf2sfile [] f (\<not> is_init_file f) = None"

   612 apply (case_tac f)

   613 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)

   614 apply (rule notI, drule root_is_init_dir', simp)

   615 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')

   616 apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits

   617             dest:init_file_has_inum inof_has_file_tag init_sec_file_dir)

   618 done

   619 

   620 lemma cf2sfile_nil_prop:

   621   "f \<in> init_files \<Longrightarrow> cf2sfile [] f = (\<lambda> b. if (b = is_init_file f) then init_cf2sfile f else None)"

   622 apply (frule cf2sfile_nil_prop1, frule cf2sfile_nil_prop2)

   623 by (rule ext, auto split:if_splits)

   624 

   625 lemma cf2sfile_nil_prop3:

   626   "is_init_file f \<Longrightarrow> cf2sfile [] f True = init_cf2sfile f"

   627 by (simp add:is_init_file_prop1 cf2sfile_nil_prop)

   628 

   629 lemma cf2sfile_nil_prop4:

   630   "is_init_dir f \<Longrightarrow> cf2sfile [] f False = init_cf2sfile f"

   631 apply (frule init_file_dir_conflict2)

   632 by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop)

   633 

   634 lemma cfs2sfiles_nil_prop:

   635   "\<forall> f \<in> fs. f \<in> init_files \<Longrightarrow> cfs2sfiles [] fs = init_cfs2sfiles fs"

   636 apply (simp add:cfs2sfiles_def init_cfs2sfiles_def)

   637 using cf2sfile_nil_prop apply auto

   638 

   639 lemma cfd2sfd_nil_prop:

   640   "init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd"

   641 apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def)

   642 apply (drule init_filefd_prop1, drule cf2sfile_nil_prop)

   643 by (auto split:option.splits)

   644 

   645 lemma cpfd2sfds_nil_prop:

   646   "cpfd2sfds [] p = init_cfds2sfds p"

   647 apply (simp only:cpfd2sfds_def init_cfds2sfds_def)

   648 apply (rule set_eqI, rule iffI)

   649 apply (drule CollectD, rule CollectI, (erule exE)+)

   650 apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI) defer

   651 apply (drule CollectD, rule CollectI, (erule exE)+)

   652 apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI)

   653 using cfd2sfd_nil_prop by auto

   654 

   655 lemma ch2sshm_nil_prop:

   656   "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h"

   657 by (simp add:ch2sshm_def init_sectxt_prop init_ch2sshm_def)

   658 

   659 lemma cph2spshs_nil_prop:

   660   "cph2spshs [] p = init_cph2spshs p"

   661 apply (auto simp add:init_cph2spshs_def cph2spshs_def init_sectxt_prop)

   662 apply (rule_tac x = h in exI, simp) defer

   663 apply (rule_tac x = h in exI, simp)

   664 by (auto simp:ch2sshm_nil_prop dest:init_procs_has_shm)

   665 

   666 lemma cp2sproc_nil_prop:

   667   "p \<in> init_procs \<Longrightarrow> cp2sproc [] p = init_cp2sproc p"

   668 by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cph2spshs_nil_prop cpfd2sfds_nil_prop

   669          split:option.splits)

   670 

   671 lemma tainted_nil_prop:

   672   "(x \<in> tainted []) = (x \<in> seeds)"

   673 apply (rule iffI)

   674 apply (erule tainted.cases, simp+)

   675 apply (erule t_init)

   676 done

   677 

   678 lemma msg_has_sec_imp_init: 

   679   "init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)"

   680 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   681 by (drule init_type_has_obj, simp)

   682 

   683 lemma msgq_has_sec_imp_init:

   684   "init_sectxt_of_obj (O_msgq q) = Some sec \<Longrightarrow> q \<in> init_msgqs"

   685 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   686 by (drule init_type_has_obj, simp)

   687 

   688 lemma cm2smsg_nil_prop:

   689   "cm2smsg [] q m = init_cm2smsg q m"

   690 by (auto simp add:init_sectxt_prop cm2smsg_def init_cm2smsg_def split:option.splits

   691              dest: msg_has_sec_imp_init intro:t_init elim:tainted.cases)

   692 

   693 lemma cqm2sms_nil_prop:

   694   "cqm2sms [] q ms = init_cqm2sms q ms"

   695 apply (induct ms, simp)

   696 by (auto simp add:cm2smsg_def init_sectxt_prop tainted_nil_prop msg_has_sec_imp_init init_cm2smsg_def

   697          split:option.splits)

   698 

   699 lemma cq2smsga_nil_prop:

   700   "cq2smsgq [] q = init_cq2smsgq q"

   701 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop

   702             intro:msgq_has_sec_imp_init split:option.splits)

   703 

   704 lemma same_inode_nil_prop:

   705   "same_inode_files [] f = init_same_inode_files f"

   706 by (simp add:same_inode_files_def init_same_inode_files_def)

   707 

   708 lemma init_same_inode_prop1:

   709   "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"

   710 apply (simp add:init_same_inode_files_def)

   711 apply (drule init_files_prop3)

   712 apply (auto simp:init_files_prop1)

   713 done

   714 

   715 lemma co2sobj_nil_prop:

   716   "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"

   717 apply (case_tac obj)

   718 apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop 

   719                      cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1

   720                      is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop 

   721                      same_inode_nil_prop  cm2smsg_nil_prop dest:init_same_inode_prop1 

   722                split:option.splits)

   723 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)

   724 by (simp add:init_files_props)

   725 

   726 lemma s2ss_nil_prop:

   727   "s2ss [] = init_static_state"

   728 using co2sobj_nil_prop init_alive_prop

   729 by (auto simp add:s2ss_def init_static_state_def)

   730 

   731 end

   732 

   733 (*<*)

   734 end

   735 (*>*)