theory Sectxt_prop

imports Main Flask Flask_type Current_files_prop Current_sockets_prop Alive_prop

begin

context flask begin

lemma alive_obj_has_type:

  assumes alive: "alive s obj" and vs: "valid s"

  shows "\<exists> t. type_of_obj s obj = Some t"

using alive vs

proof (induct s arbitrary:obj)

  case Nil

  thus ?case

    by (simp add:init_alive_prop[THEN sym] init_obj_has_type)

next

  case (Cons e s)

  hence a2: "alive (e # s) obj" and a3: "valid (e # s)" by auto

  hence a4: "valid s" and a5: "os_grant s e" and a6: "grant s e" 

    by (auto intro:vd_cons vt_grant_os vt_grant)  

  hence a1: "\<And> obj. alive s obj \<Longrightarrow> \<exists>t. type_of_obj s obj = Some t" using Cons by auto

  have a1': "\<And> obj. type_of_obj s obj = None \<Longrightarrow> \<not> alive s obj" by (rule_tac notI, auto dest:a1)

  have p1: "\<And> p. p \<in> current_procs s \<Longrightarrow> \<exists> t. type_of_obj s (O_proc p) = Some t" by (auto intro:a1)

  have p2: "\<And> f. is_file s f \<Longrightarrow> \<exists> t. type_of_obj s (O_file f) = Some t"

    by (auto intro!:a1 simp:is_file_in_current)

  have p3: "\<And> f. is_dir s f \<Longrightarrow> \<exists> t. type_of_obj s (O_dir f) = Some t" 

    by (auto intro!:a1 simp:is_dir_in_current)

  have p4: "\<And> sock. is_tcp_sock s sock \<Longrightarrow> \<exists> t. type_of_obj s (O_tcp_sock sock) = Some t"

    by (auto intro!:a1 simp:is_tcp_in_current)

  have p5: "\<And> sock. is_udp_sock s sock \<Longrightarrow> \<exists> t. type_of_obj s (O_udp_sock sock) = Some t"

    by (auto intro!:a1 simp:is_udp_in_current)

  have p6: "\<And> p fd. fd \<in> current_proc_fds s p \<Longrightarrow> \<exists> t. type_of_obj s (O_fd p fd) = Some t"

    by (auto intro:a1)

  have p7: "\<And> n. n \<in> init_nodes \<Longrightarrow> \<exists> t. type_of_obj s (O_node n) = Some t" by (auto intro:a1)

  have p8: "\<And> h. h \<in> current_shms s \<Longrightarrow> \<exists> t. type_of_obj s (O_shm h) = Some t" by (auto intro:a1)

  have p9: "\<And> q. q \<in> current_msgqs s \<Longrightarrow> \<exists> t. type_of_obj s (O_msgq q) = Some t" by (auto intro:a1)

  have p10: "\<And> q m. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s\<rbrakk>

    \<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" by (auto intro:a1)

  show ?case using a5 a2 a4 a3

    apply (case_tac e)

    apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits

                dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)

    apply (frule_tac p = nat1 in file_fds_subset_pfds)

    apply (rule a1, auto)

    done

qed

lemma alive_obj_has_user:

  assumes alive: "alive s obj" and vs: "valid s"

  shows "\<exists> t. user_of_obj s obj = Some t"

using alive vs

proof (induct s arbitrary:obj)

  case Nil

  thus ?case

    by (simp add:init_alive_prop[THEN sym] init_obj_has_user)

next

  case (Cons e s)

  hence a2: "alive (e # s) obj" and a3: "valid (e # s)" by auto

  hence a4: "valid s" and a5: "os_grant s e" and a6: "grant s e" 

    by (auto intro:vd_cons vt_grant_os vt_grant)  

  hence a1: "\<And> obj. alive s obj \<Longrightarrow> \<exists>t. user_of_obj s obj = Some t" using Cons by auto

  have a1': "\<And> obj. user_of_obj s obj = None \<Longrightarrow> \<not> alive s obj" by (rule_tac notI, auto dest:a1)

  have p1: "\<And> p. p \<in> current_procs s \<Longrightarrow> \<exists> t. user_of_obj s (O_proc p) = Some t" by (auto intro:a1)

  have p2: "\<And> f. is_file s f \<Longrightarrow> \<exists> t. user_of_obj s (O_file f) = Some t"

    by (auto intro!:a1 simp:is_file_in_current)

  have p3: "\<And> f. is_dir s f \<Longrightarrow> \<exists> t. user_of_obj s (O_dir f) = Some t" 

    by (auto intro!:a1 simp:is_dir_in_current)

  have p4: "\<And> sock. is_tcp_sock s sock \<Longrightarrow> \<exists> t. user_of_obj s (O_tcp_sock sock) = Some t"

    by (auto intro!:a1 simp:is_tcp_in_current)

  have p5: "\<And> sock. is_udp_sock s sock \<Longrightarrow> \<exists> t. user_of_obj s (O_udp_sock sock) = Some t"

    by (auto intro!:a1 simp:is_udp_in_current)

  have p6: "\<And> p fd. fd \<in> current_proc_fds s p \<Longrightarrow> \<exists> t. user_of_obj s (O_fd p fd) = Some t"

    by (auto intro:a1)

  have p7: "\<And> n. n \<in> init_nodes \<Longrightarrow> \<exists> t. user_of_obj s (O_node n) = Some t" by (auto intro:a1)

  have p8: "\<And> h. h \<in> current_shms s \<Longrightarrow> \<exists> t. user_of_obj s (O_shm h) = Some t" by (auto intro:a1)

  have p9: "\<And> q. q \<in> current_msgqs s \<Longrightarrow> \<exists> t. user_of_obj s (O_msgq q) = Some t" by (auto intro:a1)

  have p10: "\<And> q m. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s\<rbrakk>

    \<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" by (auto intro:a1)

  show ?case using a5 a2 a4 a3

    apply (case_tac e)

    apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits

                dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)

    apply (frule_tac p = nat1 in file_fds_subset_pfds)

    apply (rule a1, auto)

    done

qed

lemma alive_obj_has_type': "\<lbrakk>type_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" 

by (rule_tac notI, auto dest:alive_obj_has_type)

lemma current_proc_has_type: 

  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_proc p) = Some t" 

by (auto intro:alive_obj_has_type)

lemma current_proc_has_type': 

  "\<lbrakk>type_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" 

by (rule notI, auto dest:current_proc_has_type)

lemma is_file_has_type: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_file f) = Some t"

by (auto intro:alive_obj_has_type simp:is_file_in_current)

lemma is_file_has_type': "\<lbrakk>type_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f"

by (auto intro:notI dest:is_file_has_type)

lemma is_dir_has_type: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_dir f) = Some t"

by (auto intro:alive_obj_has_type simp:is_dir_in_current)

lemma is_dir_has_type': "\<lbrakk>type_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"

by (auto intro:notI dest:is_dir_has_type)

lemma is_tcp_has_type: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_tcp_sock sock) = Some t"

by (auto intro:alive_obj_has_type simp:is_tcp_in_current)

lemma is_tcp_has_type': "\<lbrakk>type_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock"

by (auto intro:notI dest:is_tcp_has_type)

lemma is_udp_has_type: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_udp_sock sock) = Some t"

by (auto intro:alive_obj_has_type simp:is_udp_in_current)

lemma is_udp_has_type': "\<lbrakk>type_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock"

by (auto intro:notI dest:is_udp_has_type)

lemma current_fd_has_type: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_fd p fd) = Some t"

by (auto intro:alive_obj_has_type)

lemma current_fd_has_type': "\<lbrakk>type_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p"

by (auto intro:notI dest:current_fd_has_type)

lemma init_node_has_type: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_node n) = Some t" 

by (auto intro: alive_obj_has_type)

lemma init_node_has_type': "\<lbrakk>type_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" 

by (auto intro:notI dest:init_node_has_type)

lemma current_shm_has_type: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_shm h) = Some t" 

by (auto intro:alive_obj_has_type)

lemma current_shm_has_type': "\<lbrakk>type_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" 

by (auto intro:notI dest:current_shm_has_type)

lemma current_msgq_has_type: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_msgq q) = Some t" 

by (auto intro:alive_obj_has_type)

lemma current_msgq_has_type': "\<lbrakk>type_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" 

by (auto intro:notI dest:current_msgq_has_type)

lemma current_msg_has_type: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>

    \<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" 

by (auto intro:alive_obj_has_type)

lemma current_msg_has_type': "\<lbrakk>type_of_obj s (O_msg q m) = None; valid s\<rbrakk>

    \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" 

by (auto dest!:current_msg_has_type)

lemmas current_has_type = alive_obj_has_type current_proc_has_type is_file_has_type is_dir_has_type 

  is_tcp_has_type is_udp_has_type current_fd_has_type init_node_has_type current_shm_has_type

  current_msgq_has_type current_msg_has_type

lemmas current_has_type' = alive_obj_has_type' current_proc_has_type' is_file_has_type' is_dir_has_type'

  is_tcp_has_type' is_udp_has_type' current_fd_has_type' init_node_has_type' current_shm_has_type'

  current_msgq_has_type' current_msg_has_type' 

lemma alive_obj_has_user': "\<lbrakk>user_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" 

by (rule_tac notI, auto dest:alive_obj_has_user)

lemma current_proc_has_user: 

  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_proc p) = Some t" 

by (auto intro:alive_obj_has_user)

lemma current_proc_has_user': 

  "\<lbrakk>user_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" 

by (rule notI, auto dest:current_proc_has_user)

lemma is_file_has_user: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_file f) = Some t"

by (auto intro:alive_obj_has_user simp:is_file_in_current)

lemma is_file_has_user': "\<lbrakk>user_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f"

by (auto intro:notI dest:is_file_has_user)

lemma is_dir_has_user: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_dir f) = Some t"

by (auto intro:alive_obj_has_user simp:is_dir_in_current)

lemma is_dir_has_user': "\<lbrakk>user_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"

by (auto intro:notI dest:is_dir_has_user)

lemma is_tcp_has_user: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_tcp_sock sock) = Some t"

by (auto intro:alive_obj_has_user simp:is_tcp_in_current)

lemma is_tcp_has_user': "\<lbrakk>user_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock"

by (auto intro:notI dest:is_tcp_has_user)

lemma is_udp_has_user: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_udp_sock sock) = Some t"

by (auto intro:alive_obj_has_user simp:is_udp_in_current)

lemma is_udp_has_user': "\<lbrakk>user_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock"

by (auto intro:notI dest:is_udp_has_user)

lemma current_fd_has_user: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_fd p fd) = Some t"

by (auto intro:alive_obj_has_user)

lemma current_fd_has_user': "\<lbrakk>user_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p"

by (auto intro:notI dest:current_fd_has_user)

lemma init_node_has_user: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_node n) = Some t" 

by (auto intro: alive_obj_has_user)

lemma init_node_has_user': "\<lbrakk>user_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" 

by (auto intro:notI dest:init_node_has_user)

lemma current_shm_has_user: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_shm h) = Some t" 

by (auto intro:alive_obj_has_user)

lemma current_shm_has_user': "\<lbrakk>user_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" 

by (auto intro:notI dest:current_shm_has_user)

lemma current_msgq_has_user: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_msgq q) = Some t" 

by (auto intro:alive_obj_has_user)

lemma current_msgq_has_user': "\<lbrakk>user_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" 

by (auto intro:notI dest:current_msgq_has_user)

lemma current_msg_has_user: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>

    \<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" 

by (auto intro:alive_obj_has_user)

lemma current_msg_has_user': "\<lbrakk>user_of_obj s (O_msg q m) = None; valid s\<rbrakk>

    \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" 

by (auto dest!:current_msg_has_user)

lemmas current_has_user = alive_obj_has_user current_proc_has_user is_file_has_user is_dir_has_user 

  is_tcp_has_user is_udp_has_user current_fd_has_user init_node_has_user current_shm_has_user

  current_msgq_has_user current_msg_has_user

lemmas current_has_user' = alive_obj_has_user' current_proc_has_user' is_file_has_user' is_dir_has_user'

  is_tcp_has_user' is_udp_has_user' current_fd_has_user' init_node_has_user' current_shm_has_user'

  current_msgq_has_user' current_msg_has_user' 

lemma current_proc_has_role:

  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. role_of_proc s p = Some r"

apply (induct s arbitrary:p, simp add:init_procrole_prop2)

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

apply (auto split:option.splits dest:current_has_type' simp:sectxt_of_obj_def)

done

lemma current_proc_has_role':

  "\<lbrakk>role_of_proc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"

by (auto dest:current_proc_has_role)

lemma alive_obj_has_role:

  "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> r. role_of_obj s obj = Some r"

by (case_tac obj, auto intro:current_proc_has_role)

lemma alive_obj_has_sec:

  "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s obj = Some sec"

apply (frule alive_obj_has_type, simp)

apply (frule alive_obj_has_role, simp)

apply (frule alive_obj_has_user, simp)

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

done

lemma alive_obj_has_sec':

  "\<lbrakk>sectxt_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"

by (auto dest:alive_obj_has_sec)

lemma alive_obj_has_sec'':

  "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s obj = Some (u,r,t)"

by (auto dest:alive_obj_has_sec)

lemma current_proc_has_sec: 

  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_proc p) = Some sec"

by (rule alive_obj_has_sec, simp+) 

lemma current_proc_has_sec': 

  "\<lbrakk>sectxt_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" 

by (rule notI, auto dest:current_proc_has_sec)

lemma current_proc_has_sec'': 

  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_proc p) = Some (u,r,t)"

by (drule current_proc_has_sec, auto)

lemma is_file_has_sec: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_file f) = Some sec"

by (rule alive_obj_has_sec, simp_all add:is_file_in_current)

lemma is_file_has_sec': "\<lbrakk>sectxt_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f"

by (auto intro:notI dest:is_file_has_sec)

lemma is_file_has_sec'': "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_file f) = Some (u,r,t)"

by (drule is_file_has_sec, auto)

lemma is_dir_has_sec: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_dir f) = Some sec"

by (rule alive_obj_has_sec, simp_all add:is_dir_in_current)

lemma is_dir_has_sec': "\<lbrakk>sectxt_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"

by (auto intro:notI dest:is_dir_has_sec)

lemma is_dir_has_sec'': "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_dir f) = Some (u,r,t)"

by (drule is_dir_has_sec, auto)

lemma is_tcp_has_sec: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_tcp_sock sock) = Some sec"

by (rule alive_obj_has_sec, simp_all add:is_tcp_in_current)

lemma is_tcp_has_sec': "\<lbrakk>sectxt_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock"

by (auto intro:notI dest:is_tcp_has_sec)

lemma is_tcp_has_sec'': "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> 

  \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_tcp_sock sock) = Some (u,r,t)"

by (drule is_tcp_has_sec, simp_all add:is_tcp_in_current)

lemma is_udp_has_sec: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_udp_sock sock) = Some sec"

by (rule alive_obj_has_sec, simp_all add:is_udp_in_current)

lemma is_udp_has_sec': "\<lbrakk>sectxt_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock"

by (auto intro:notI dest:is_udp_has_sec)

lemma is_udp_has_sec'': "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> 

  \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_udp_sock sock) = Some (u,r,t)"

by (drule is_udp_has_sec, simp_all add:is_udp_in_current)

lemma current_fd_has_sec: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_fd p fd) = Some sec"

by (rule alive_obj_has_sec, simp+)

lemma current_fd_has_sec': "\<lbrakk>sectxt_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p"

by (auto intro:notI dest:current_fd_has_sec)

lemma current_fd_has_sec'': "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> 

  \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_fd p fd) = Some (u, r, t)"

by (drule current_fd_has_sec, simp+)

lemma init_node_has_sec: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_node n) = Some sec" 

by (rule alive_obj_has_sec, simp+)

lemma init_node_has_sec': "\<lbrakk>sectxt_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" 

by (auto intro:notI dest:init_node_has_sec)

lemma init_node_has_sec'': "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_node n) = Some (u,r,t)" 

by (drule init_node_has_sec, simp+)

lemma current_shm_has_sec: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_shm h) = Some sec" 

by (rule alive_obj_has_sec, simp+)

lemma current_shm_has_sec': "\<lbrakk>sectxt_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" 

by (auto intro:notI dest:current_shm_has_sec)

lemma current_shm_has_sec'': "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_shm h) = Some (u,r,t)" 

by (drule current_shm_has_sec, simp+)

lemma current_msgq_has_sec: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_msgq q) = Some sec" 

by (rule alive_obj_has_sec, simp+)

lemma current_msgq_has_sec': "\<lbrakk>sectxt_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" 

by (auto intro:notI dest:current_msgq_has_sec)

lemma current_msgq_has_sec'': "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> 

  \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_msgq q) = Some (u,r,t)" 

by (drule current_msgq_has_sec, simp+)

lemma current_msg_has_sec: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>

    \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_msg q m) = Some sec" 

by (rule alive_obj_has_sec, simp+)

lemma current_msg_has_sec': "\<lbrakk>sectxt_of_obj s (O_msg q m) = None; valid s\<rbrakk>

    \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" 

by (auto dest!:current_msg_has_sec)

lemma current_msg_has_sec'': "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>

    \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_msg q m) = Some (u, r, t)" 

by (drule current_msg_has_sec, simp+)

lemmas current_has_sec = alive_obj_has_sec current_proc_has_sec is_file_has_sec is_dir_has_sec 

  is_tcp_has_sec is_udp_has_sec current_fd_has_sec init_node_has_sec current_shm_has_sec

  current_msgq_has_sec current_msg_has_sec

lemmas current_has_sec' = alive_obj_has_sec' current_proc_has_sec' is_file_has_sec' is_dir_has_sec'

  is_tcp_has_sec' is_udp_has_sec' current_fd_has_sec' init_node_has_sec' current_shm_has_sec'

  current_msgq_has_sec' current_msg_has_sec' 

lemmas current_has_sec'' = alive_obj_has_sec'' current_proc_has_sec'' is_file_has_sec'' is_dir_has_sec''

  is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' current_shm_has_sec''

  current_msgq_has_sec'' current_msg_has_sec'' 

(************ root sec remains ************)

lemma root_type_remains:

  "valid s \<Longrightarrow> type_of_obj s (O_dir []) = init_type_of_obj (O_dir [])"

apply (induct s)

apply (simp)

apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 

by (case_tac option, auto)

lemma root_user_remains:

  "valid s \<Longrightarrow> user_of_obj s (O_dir []) = init_user_of_obj (O_dir [])"

apply (induct s)

apply (simp)

apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 

by (case_tac option, auto)

lemma root_has_type':

  "\<lbrakk>type_of_obj s (O_dir []) = None; valid s\<rbrakk> \<Longrightarrow> False"

apply (drule alive_obj_has_type', simp)

by (drule root_is_dir, simp)

lemma root_has_user':

  "\<lbrakk>user_of_obj s (O_dir []) = None; valid s\<rbrakk> \<Longrightarrow> False"

apply (drule alive_obj_has_user', simp)

by (drule root_is_dir, simp)

lemma root_has_init_type':

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

using init_obj_has_type[where obj = "O_dir []"] root_is_init_dir

by auto

lemma root_has_init_user':

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

using init_obj_has_user[where obj = "O_dir []"] root_is_init_dir

by auto

lemma root_sec_remains:

  "valid s \<Longrightarrow> sectxt_of_obj s (O_dir []) = init_sectxt_of_obj (O_dir [])"

by (auto simp:root_user_remains root_type_remains sectxt_of_obj_def init_sectxt_of_obj_def

        split:option.splits)

lemma root_sec_set:

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

by (auto simp:sec_of_root_def split:option.splits

        dest!: root_has_init_type' root_has_init_user')

lemma sec_of_root_set:

  "init_sectxt_of_obj (O_dir []) = Some sec_of_root"

using root_has_init_type' root_has_init_user'

apply (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits)

done

(*************** sectxt_of_obj simpset ****************)

lemma sec_execve:

  "valid (Execve p f fds # s) \<Longrightarrow> sectxt_of_obj (Execve p f fds # s) = 

   (sectxt_of_obj s) (O_proc p := (

     case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of

       (Some psec, Some fsec) \<Rightarrow> npctxt_execve psec fsec

     | _ \<Rightarrow> None))"

apply (rule ext, frule vd_cons, frule vt_grant_os, frule vt_grant,case_tac x)

apply (auto simp:sectxt_of_obj_def split:option.splits 

           dest!:current_has_type' current_proc_has_role' current_has_user')

done

lemma sec_clone:

  "valid (Clone p p' fds shms # s) \<Longrightarrow> sectxt_of_obj (Clone p p' fds shms # s) = (\<lambda> obj. 

     case obj of 

       O_proc p'' \<Rightarrow> if (p'' = p') then sectxt_of_obj s (O_proc p) 

                     else sectxt_of_obj s obj

     | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_fd p fd)

                      else if (p'' = p') then None

                      else sectxt_of_obj s obj

     | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_tcp_sock (p, fd))

                               else if (p'' = p') then None

                               else sectxt_of_obj s obj

     | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_udp_sock (p, fd))

                               else if (p'' = p') then None

                               else sectxt_of_obj s obj

     | _ \<Rightarrow> sectxt_of_obj s obj )"

apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj)

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

           dest!:current_has_type' current_proc_has_role' current_has_user')

done

lemma sec_open:

  "valid (Open p f flags fd opt # s) \<Longrightarrow> sectxt_of_obj (Open p f flags fd opt # s) = (\<lambda> obj. 

     case obj of

       O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None) then 

                      (case (parent f) of 

                         None \<Rightarrow> None

                       | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of

                                      (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, 

                                        type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_file True)

                                    | _ \<Rightarrow> None))

                    else sectxt_of_obj s obj

     | O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then 

                        (case (sectxt_of_obj s (O_proc p)) of 

                           Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)

                         | _ \<Rightarrow> None)

                      else sectxt_of_obj s obj

     | _ \<Rightarrow> sectxt_of_obj s obj)"

apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj)

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

           dest!:current_has_type' current_proc_has_role' current_has_user')

done

lemma sec_mkdir:

  "valid (Mkdir p f inum # s) \<Longrightarrow> sectxt_of_obj (Mkdir p f inum # s) = 

     (sectxt_of_obj s) (O_dir f := 

        (case parent f of 

           None \<Rightarrow> None

         | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of

                         (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, 

                            type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_dir True)

                      | _ \<Rightarrow> None)))"

apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)

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

           dest!:current_has_type' current_proc_has_role' current_has_user')

done

lemma sec_linkhard:

  "valid (LinkHard p f f' # s) \<Longrightarrow> sectxt_of_obj (LinkHard p f f' # s) = 

     (sectxt_of_obj s) (O_file f' := 

        (case parent f' of 

           None \<Rightarrow> None

         | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of

                         (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, 

                            type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_file True)

                      | _ \<Rightarrow> None)))"

apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)

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

           dest!:current_has_type' current_proc_has_role' current_has_user')

done

lemma sec_createmsgq:

  "valid (CreateMsgq p q # s) \<Longrightarrow> sectxt_of_obj (CreateMsgq p q # s) = (sectxt_of_obj s) (O_msgq q := 

     (case (sectxt_of_obj s (O_proc p)) of

        Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)

      | _ \<Rightarrow> None))"

apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)

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

           dest!:current_has_type' current_proc_has_role' current_has_user')

done

lemma sec_sendmsg: