1314 | "grant s (Mkdir p f inum) = |
1314 | "grant s (Mkdir p f inum) = |
1315 (case (parent f) of |
1315 (case (parent f) of |
1316 Some pf \<Rightarrow> |
1316 Some pf \<Rightarrow> |
1317 (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
1317 (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
1318 (Some (pu,pr,pt), Some (du,dr,dt)) \<Rightarrow> |
1318 (Some (pu,pr,pt), Some (du,dr,dt)) \<Rightarrow> |
1319 (search_check s (pu,pr,pt) f \<and> |
1319 (search_check s (pu,pr,pt) pf \<and> |
1320 permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \<and> |
1320 permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \<and> |
1321 permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name) |
1321 permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name) |
1322 | _ \<Rightarrow> False) |
1322 | _ \<Rightarrow> False) |
1323 | _ \<Rightarrow> False)" |
1323 | _ \<Rightarrow> False)" |
1324 | "grant s (LinkHard p f f') = |
1324 | "grant s (LinkHard p f f') = |