diff -r f27882976251 -r 289a30c4cfb7 Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Wed May 15 15:42:46 2013 +0800
+++ b/Co2sobj_prop.thy	Thu May 16 15:18:44 2013 +0800
@@ -6,7 +6,7 @@
 
 context tainting_s begin
 
-(************ simpset for cf2sfile ***************)
+(****************** cf2sfile path simpset ***************)
 
 lemma sroot_only:
   "cf2sfile s [] = Some sroot"
@@ -34,7 +34,7 @@
 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)
+            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"
@@ -132,50 +132,42 @@
 apply (auto split:option.splits)
 done
 
-
+lemma cf2sfile_path_file_prop1:
+  "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>
+   \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = 
+                 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}) \<and> 
+               sectxt_of_obj s (O_file (f # pf)) = Some fsec"
+apply (frule is_file_has_sfile, simp)
+by (auto simp:cf2sfile_path_file)
 
-apply simp
+lemma cf2sfile_path_file_prop2:
+  "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); 
+    sectxt_of_obj s (O_file (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = 
+      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})"
+by (drule cf2sfile_path_file_prop1, auto)
 
-thm cf2sfile_def
-apply (simp (no_asm_simp))
-apply simp
-apply (frule cf2sfile_path_file, simp)
-apply (simp add: cf2sfile_path_file)
-apply auto
-apply (simp only:cf2sfile_path_file)
-by (simp add:cf2sfile_path_file cf2sfile_path_dir)
-apply (frule parentf_is_dir'', simp)
-apply (frule is_file_or_dir, simp)
-apply (frule sroot_set, erule disjE)
-apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)
-apply (case_tac pf, clarsimp)
-apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop simp:cf2sfile_def get_parentfs_ctxts.simps
-            simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1]
-apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop 
-            simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1]
-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
+lemma cf2sfile_path_dir_prop1:
+  "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>
+   \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = 
+                 Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
+                       else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> 
+               sectxt_of_obj s (O_dir (f # pf)) = Some fsec"
+apply (frule is_dir_has_sfile, simp)
+by (auto simp:cf2sfile_path_dir)
 
-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_path_dir_prop2:
+  "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); 
+    sectxt_of_obj s (O_dir (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = 
+      Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
+            else Created, fsec, Some pfsec, asecs \<union> {pfsec})"
+by (drule cf2sfile_path_dir_prop1, auto)
 
-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)
-apply (frule noroot_events, case_tac f, simp)
-apply (auto split:if_splits option.splits    dest!:current_has_sec' dest:parentf_in_current'
-          simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
-               get_parentfs_ctxts_simps)
-done
+(**************** cf2sfile event list simpset ****************)
 
-lemma cf2sfile_open_none2:
-  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f' b = cf2sfile s f' b"
+lemma cf2sfile_open_none':
+  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f'= cf2sfile s f'"
 apply (frule vd_cons, frule vt_grant_os)
 apply (induct f', simp add:cf2sfile_def)
 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
@@ -184,14 +176,13 @@
 
 lemma cf2sfile_open_none:
   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s"
-apply (rule ext, rule ext)
-apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2)
-done
+apply (rule ext)
+by (simp add:cf2sfile_open_none')
 
 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'"
-apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext)
+apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
 apply (case_tac "f = f'", simp)
 apply (induct f', simp add:sroot_only, simp)
 apply (frule parentf_in_current', simp+)
@@ -201,18 +192,18 @@
 
 lemma cf2sfile_open_some2:
   "\<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"
+   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
 apply (frule vd_cons, drule is_file_in_current)
 by (simp add:cf2sfile_open_some1)
 
 lemma cf2sfile_open_some3:
   "\<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"
+   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
 apply (frule vd_cons, drule is_dir_in_current)
 by (simp add:cf2sfile_open_some1)
 
 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 = (
+  "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f = (
      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), 
                          get_parentfs_ctxts s pf) of
@@ -228,80 +219,169 @@
 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) 
+   \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' = (
+     if (opt = None) then cf2sfile s f'
+     else if (f' = f) 
      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)"
+     else cf2sfile s f')"
 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)
+apply (simp add:cf2sfile_open_some4 split:option.splits)
+apply (simp add:cf2sfile_open_some1 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 (frule vd_cons, frule vt_grant_os, frule noroot_events)
 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 
+apply (case_tac "f = f'", simp)
+apply (simp add:cf2sfile_path 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"
+  "\<lbrakk>valid (Mkdir p f i # s); is_file s f'\<rbrakk>
+   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"
 apply (frule vd_cons, drule is_file_in_current)
-by (simp add:cf2sfile_open_some1)
+by (simp add:cf2sfile_mkdir1)
 
 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"
+  "\<lbrakk>valid (Mkdir p f i # s); is_dir s f'\<rbrakk>
+   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"
 apply (frule vd_cons, drule is_dir_in_current)
-by (simp add:cf2sfile_open_some1)
+by (simp add:cf2sfile_mkdir1)
 
+lemma cf2sfile_mkdir4:
+  "valid (Mkdir p f i # s)
+  \<Longrightarrow> cf2sfile (Mkdir p f i # s) f = (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)"
+apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
+apply (case_tac f, simp)
+apply (clarsimp simp:os_grant.simps)
+apply (simp add:sectxt_of_obj_simps)
+apply (frule current_proc_has_sec, simp)
+apply (frule is_dir_has_sec, simp)
+apply (frule get_pfs_secs_prop, simp)
+apply (frule is_dir_not_file)
+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 if_splits 
+            dest:not_deleted_init_dir is_dir_in_current not_deleted_init_file is_file_in_current)
+done
 
 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) 
+  "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files (Mkdir p f i # s)\<rbrakk>
+  \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = (
+    if (f' = f) 
     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)"
+     else cf2sfile s f')"
+apply (case_tac "f = f'")
+apply (simp add:cf2sfile_mkdir4 split:option.splits)
+apply (simp add:cf2sfile_mkdir1 current_files_simps)
+done
+
+lemma cf2sfile_linkhard1:
+  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk>
+   \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
+apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
+apply (case_tac "f = f'", simp)
+apply (induct f', simp add:sroot_only, simp)
+apply (frule parentf_in_current', simp+)
+apply (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_linkhard2:
+  "\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk>
+   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"
+apply (frule vd_cons, drule is_file_in_current)
+by (simp add:cf2sfile_linkhard1)
+
+lemma cf2sfile_linkhard3:
+  "\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk>
+   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"
+apply (frule vd_cons, drule is_dir_in_current)
+by (simp add:cf2sfile_linkhard1)
+
+lemma cf2sfile_linkhard4:
+  "valid (LinkHard p oldf f # s)
+  \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of
+         Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # 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)"
+apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
+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, (erule conjE)+)
+apply (drule not_deleted_init_file, simp+)
+apply (simp add:is_file_in_current)
+done
+
+lemma cf2sfile_linkhard:
+  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk>
+  \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = (
+    if (f' = f) 
+    then (case (parent f) of
+             Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # 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')"
+apply (case_tac "f = f'")
+apply (simp add:cf2sfile_linkhard4 split:option.splits)
+apply (simp add:cf2sfile_linkhard1 current_files_simps)
+done
+
+lemma cf2sfile_other:
+  "\<lbrakk>ff \<in> current_files s;
+    \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
+    \<forall> p fd. e \<noteq> CloseFd p fd;
+    \<forall> p f. e \<noteq> UnLink p f;
+    \<forall> p f. e \<noteq> Rmdir p f;
+    \<forall> p f i. e \<noteq> Mkdir p f i;
+    \<forall> p f f'. e \<noteq> LinkHard p f f'; 
+    valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"
 apply (frule vd_cons, frule vt_grant_os)
-apply (rule ext, rule ext)
+apply (induct ff, simp add:sroot_only)
+apply (frule parentf_in_current', simp+, case_tac e)
+apply (auto simp:current_files_simps is_file_simps is_dir_simps sectxt_of_obj_simps cf2sfile_path 
+           split:if_splits option.splits)                     
+done     
 
-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_unlink:
+  "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>
+   \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (simp add:current_files_simps split:if_splits)
+apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps
+ split:if_splits option.splits)
 
 
-
-
+lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other
+