1376 | "grant s (Mkdir p f inum) = |
1376 | "grant s (Mkdir p f inum) = |
1377 (case (parent f) of |
1377 (case (parent f) of |
1378 Some pf \<Rightarrow> |
1378 Some pf \<Rightarrow> |
1379 (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
1379 (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
1380 (Some (pu,pr,pt), Some (du,dr,dt)) \<Rightarrow> |
1380 (Some (pu,pr,pt), Some (du,dr,dt)) \<Rightarrow> |
1381 (search_check s (pu,pr,pt) f \<and> |
1381 (search_check s (pu,pr,pt) pf \<and> |
1382 permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \<and> |
1382 permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \<and> |
1383 permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name) |
1383 permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name) |
1384 | _ \<Rightarrow> False) |
1384 | _ \<Rightarrow> False) |
1385 | _ \<Rightarrow> False)" |
1385 | _ \<Rightarrow> False)" |
1386 | "grant s (LinkHard p f f') = |
1386 | "grant s (LinkHard p f f') = |