diff -r 0c209a3e2647 -r 8779d321cc2e Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Co2sobj_prop.thy	Wed May 15 11:21:39 2013 +0800
@@ -1,6 +1,6 @@
 (*<*)
 theory Co2sobj_prop
-imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop
+imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop
 begin
 (*<*)
 
@@ -10,6 +10,98 @@
 
 declare get_parentfs_ctxts.simps [simp del]
 
+lemma sroot_only:
+  "cf2sfile s [] = Some sroot"
+by (simp add:cf2sfile_def)
+
+lemma not_file_is_dir:
+  "\<lbrakk>\<not> is_file s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s f"
+by (auto simp:is_file_def current_files_def is_dir_def 
+         dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)
+
+lemma not_dir_is_file:
+  "\<lbrakk>\<not> is_dir s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f"
+by (auto simp:is_file_def current_files_def is_dir_def 
+         dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)
+
+lemma is_file_or_dir:
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f \<or> is_dir s f"
+by (auto dest:not_dir_is_file)
+
+lemma current_file_has_sfile:
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"
+apply (induct f)
+apply (rule_tac x = "sroot" in exI, simp add:sroot_only)
+apply (frule parentf_in_current', simp, clarsimp)
+apply (frule parentf_is_dir'', simp)
+apply (frule is_file_or_dir, simp)
+apply (auto dest!:current_has_sec'
+            simp:cf2sfile_def split:option.splits if_splits dest!:get_pfs_secs_prop)
+done
+
+definition sectxt_of_pf :: "t_state \<Rightarrow> t_file \<Rightarrow> security_context_t option"
+where
+  "sectxt_of_pf s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> sectxt_of_obj s (O_dir pf))"
+
+definition get_parentfs_ctxts' :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"
+where
+  "get_parentfs_ctxts' s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> get_parentfs_ctxts s pf)"
+
+lemma is_file_has_sfile:
+  "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec psec asecs. cf2sfile s f = Some 
+      (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created,
+       sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_file f) = Some sec) \<and>
+       (sectxt_of_pf s f = Some psec) \<and> (get_parentfs_ctxts' s f = Some asecs)"
+apply (case_tac f, simp, drule root_is_dir', simp, simp)
+apply (frule is_file_in_current)
+apply (drule current_file_has_sfile, simp)
+apply (auto simp:cf2sfile_def sectxt_of_pf_def get_parentfs_ctxts'_def split:if_splits option.splits)
+done
+
+lemma is_dir_has_sfile:
+  "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> (case f of
+      [] \<Rightarrow> cf2sfile s f = Some sroot
+    | a # pf \<Rightarrow> (\<exists> sec psec asecs. cf2sfile s f = Some 
+      (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created,
+       sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_dir f) = Some sec) \<and>
+       (sectxt_of_obj s (O_dir pf) = Some psec) \<and> (get_parentfs_ctxts s pf = Some asecs)))"
+apply (case_tac f, simp add:sroot_only)
+apply (frule is_dir_in_current, frule is_dir_not_file)
+apply (drule current_file_has_sfile, simp)
+apply (auto simp:cf2sfile_def split:if_splits option.splits)
+done
+
+lemma cf2sfile_path:
+  "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (
+     case (cf2sfile s pf) of
+       Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))
+         then (case (sectxt_of_obj s (O_file (f # pf))) of
+                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
+                                   else Created, fsec, Some pfsec, asecs \<union> {pfsec})
+               | None \<Rightarrow> None)
+         else (case (sectxt_of_obj s (O_dir (f # pf))) of
+                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
+                                   else Created, fsec, Some pfsec, asecs \<union> {pfsec})
+               | None \<Rightarrow> None)           )
+     | None \<Rightarrow> None)"
+apply (frule parentf_is_dir'', simp)
+apply (frule parentf_in_current', simp)
+apply (frule is_file_or_dir, simp)
+apply (frule_tac f = pf in current_file_has_sfile, simp, erule exE)
+apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop
+            simp:cf2sfile_def split:option.splits if_splits)
+apply (case_tac "is_file s (f # pf)")
+apply (frule is_file_has_sec, simp)
+apply (frule is_dir_has_sec, simp)
+apply (frule is_dir_not_file)
+apply (erule exE)+
+apply (auto split:option.splits)[1]
+apply simp
+
+apply (rule ext)
+apply (subst (1) cf2sfile_def)
+apply (auto simp del:deleted.simps get_parentfs_ctxts.simps split:option.splits if_splits)
+
 lemma cf2sfile_open_none1:
   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b"
 apply (frule vd_cons, frule vt_grant_os)
@@ -33,10 +125,6 @@
 apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2)
 done
 
-lemma sroot_only:
-  "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)"
-by (rule ext, simp add:cf2sfile_def)
-
 lemma cf2sfile_open_some1:
   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>
    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
@@ -60,7 +148,7 @@
 apply (frule vd_cons, drule is_dir_in_current)
 by (simp add:cf2sfile_open_some1)
 
-lemma cf2sfile_open_some:
+lemma cf2sfile_open_some4:
   "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f True = (
      case (parent f) of
        Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), 
@@ -72,30 +160,87 @@
 apply (case_tac f, simp)
 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)
-apply (rule impI)
-thm not_deleted_imp_exists
-apply (auto split:if_splits option.splits    dest!:current_has_sec'
-          simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
-               get_parentfs_ctxts_simps)
+apply (rule impI, (erule conjE)+)
+apply (drule not_deleted_init_file, simp+)
+apply (simp add:is_file_in_current)
+done
+
+lemma cf2sfile_open_some5:
+  "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> 
+   cf2sfile (Open p f flag fd (Some inum) # s) f False = cf2sfile s f False"
+apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
+apply (case_tac f, simp)
+apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps split:option.splits)
+done
+
+lemma cf2sfile_open:
+  "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>
+   \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' b = (
+     if (opt = None) then cf2sfile s f' b
+     else if (f' = f \<and> b) 
+     then (case (parent f) of
+             Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf), 
+                 get_parentfs_ctxts s pf) of
+                          (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
+                        | _ \<Rightarrow> None)
+           | None \<Rightarrow> None)
+     else cf2sfile s f' b)"
+apply (case_tac opt)
+apply (simp add:cf2sfile_open_none)
+apply (case_tac "f = f'")
+apply (auto simp:cf2sfile_open_some1 cf2sfile_open_some4 cf2sfile_open_some5 current_files_simps)
+done
+
+lemma cf2sfile_mkdir1:
+  "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk>
+   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"
+apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext)
+apply (case_tac "f = f'", simp)
+apply (induct f', simp add:sroot_only, simp)
+apply (frule parentf_in_current', simp+)
+apply clarsimp
+apply (case_tac "f = f'", simp+)
+apply (simp (no_asm_simp) add:cf2sfile_def)
+apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps split:if_splits option.splits)
+done
+
+lemma cf2sfile_mkdir2:
+  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk>
+   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' True = cf2sfile s f' True"
+apply (frule vd_cons, drule is_file_in_current)
+by (simp add:cf2sfile_open_some1)
+
+lemma cf2sfile_mkdir3:
+  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk>
+   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' False = cf2sfile s f' False"
+apply (frule vd_cons, drule is_dir_in_current)
+by (simp add:cf2sfile_open_some1)
+
+
+lemma cf2sfile_mkdir:
+  "valid (Mkdir p f i # s)
+  \<Longrightarrow> cf2sfile (Mkdir p f i # s) = (\<lambda> f' b. 
+    if (f' = f \<and> \<not> b) 
+    then (case (parent f) of
+             Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), 
+                 get_parentfs_ctxts s pf) of
+                          (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
+                        | _ \<Rightarrow> None)
+           | None \<Rightarrow> None)
+     else cf2sfile s f' b)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext, rule ext)
+
+apply (auto simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps  split:if_splits option.splits)
 
 
 
-lemma cf2sfile_open:
-  "valid (Open p f flag fd opt # s) \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) = (\<lambda> f' b. 
-     if (opt = None) then cf2sfile s f' b
-     else if (f' = f \<and> b = True) 
-     then (case (parent f) of
-             Some pf \<Rightarrow> (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), 
-                 get_parentfs_ctxts s pf) of
-                          (Some sec, Some psec, Some asecs) \<Rightarrow>
-                              Some (if (\<not> deleted (O_file f) s \<and> f \<in> init_files) 
-                                    then Init f else Created, sec, Some psec, set asecs)
-                        | _ \<Rightarrow> None)
-           | None \<Rightarrow> None)
-     else cf2sfile s f' b)"
-apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
-apply (auto split:if_splits option.splits 
-             simp:sectxt_of_obj_simps)
+
+
+