# HG changeset patch
# User chunhan
# Date 1368688724 -28800
# Node ID 289a30c4cfb7ef9deef6948696ee6520e3845c0b
# Parent f2788297625144067ade592ab318ca91b4ad37b0
find bugs in deleted & inum_of_file
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
+
diff -r f27882976251 -r 289a30c4cfb7 Flask.thy
--- a/Flask.thy Wed May 15 15:42:46 2013 +0800
+++ b/Flask.thy Thu May 16 15:18:44 2013 +0800
@@ -294,10 +294,7 @@
if (proc_fd_of_file \<tau> f = {})
then (inum_of_file \<tau>) (f := None)
else inum_of_file \<tau> )"
-| "inum_of_file (Rmdir p f # \<tau>) = (
- if (proc_fd_of_file \<tau> f = {})
- then (inum_of_file \<tau>) (f := None)
- else inum_of_file \<tau> )"
+| "inum_of_file (Rmdir p f # \<tau>) = (inum_of_file \<tau>) (f := None)"
| "inum_of_file (Mkdir p f ino # \<tau>) = (inum_of_file \<tau>) (f:= Some ino)"
| "inum_of_file (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = (inum_of_file \<tau>) (f\<^isub>2 := inum_of_file \<tau> f\<^isub>1)"
(*
@@ -744,7 +741,7 @@
deleted obj s)"
| "deleted obj (Clone p p' fds shms # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p' fd \<and> fd \<notin> fds) \<or>
deleted obj s)"
-| "deleted obj (UnLink p f # s) = ((obj = O_file f) \<or> deleted obj s)"
+| "deleted obj (UnLink p f # s) = ((proc_fd_of_file s f = {} \<and> obj = O_file f) \<or> deleted obj s)"
| "deleted obj (Rmdir p f # s) = ((obj = O_dir f) \<or> deleted obj s)"
| "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or>
(\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or>
diff -r f27882976251 -r 289a30c4cfb7 Sectxt_prop.thy
--- a/Sectxt_prop.thy Wed May 15 15:42:46 2013 +0800
+++ b/Sectxt_prop.thy Thu May 16 15:18:44 2013 +0800
@@ -617,11 +617,16 @@
apply (rule_tac f = "x # pf" in parentf_is_dir)
by (auto simp:is_dir_def current_files_def split:option.splits t_inode_tag.splits)
-lemma get_pfs_secs_prop:
+lemma get_pfs_secs_prop':
"\<lbrakk>get_parentfs_ctxts s f = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"
apply (induct f)
by (auto split:option.splits dest:current_has_sec' parentf_is_dir_prop1)
+lemma get_pfs_secs_prop:
+ "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> asecs. get_parentfs_ctxts s f = Some asecs"
+using get_pfs_secs_prop'
+by (auto)
+
lemma get_pfs_secs_open:
"valid (Open p f flags fd opt # s) \<Longrightarrow> get_parentfs_ctxts (Open p f flags fd opt # s) = get_parentfs_ctxts s"
apply (frule noroot_events, frule vd_cons, frule vt_grant_os)
@@ -656,7 +661,7 @@
from p1 os have p5: "f' \<noteq> f" by (auto simp:is_dir_in_current)
show ?case using mkdir vd os p4 p5 p1
by (auto simp:sectxt_of_obj_simps is_dir_simps p3
- split:option.splits dest:current_has_sec' get_pfs_secs_prop)
+ split:option.splits dest:current_has_sec' get_pfs_secs_prop')
qed
qed
@@ -669,7 +674,7 @@
| _ \<Rightarrow> None))"
apply (frule vd_cons, frule vt_grant_os)
apply (frule noroot_events, case_tac f)
-by (auto split:option.splits dest:current_has_sec' get_pfs_secs_prop get_pfs_secs_mkdir1
+by (auto split:option.splits dest:current_has_sec' get_pfs_secs_prop' get_pfs_secs_mkdir1
simp:sectxt_of_obj_simps is_dir_simps)
lemmas get_parentfs_ctxts_simps = get_pfs_secs_other get_pfs_secs_mkdir1 get_pfs_secs_mkdir2