25 if (tp = p') |
25 if (tp = p') |
26 then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s |
26 then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s |
27 else Clone p p' fds # (enrich_proc s tp dp))" |
27 else Clone p p' fds # (enrich_proc s tp dp))" |
28 | "enrich_proc (Open p f flags fd opt # s) tp dp = ( |
28 | "enrich_proc (Open p f flags fd opt # s) tp dp = ( |
29 if (tp = p) |
29 if (tp = p) |
30 then Open dp f (remove_create_flag flags) fd opt # Open p f flags fd opt # (enrich_proc s tp dp) |
30 then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp) |
31 else Open p f flags fd opt # (enrich_proc s tp dp))" |
31 else Open p f flags fd opt # (enrich_proc s tp dp))" |
|
32 | "enrich_proc (ReadFile p fd # s) tp dp = ( |
|
33 if (tp = p) |
|
34 then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp) |
|
35 else ReadFile p fd # (enrich_proc s tp dp))" |
32 | "enrich_proc (CloseFd p fd # s) tp dp = ( |
36 | "enrich_proc (CloseFd p fd # s) tp dp = ( |
33 if (tp = p \<and> fd \<in> proc_file_fds s p) |
37 if (tp = p \<and> fd \<in> proc_file_fds s p) |
34 then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp) |
38 then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp) |
35 else CloseFd p fd # (enrich_proc s tp dp))" |
39 else CloseFd p fd # (enrich_proc s tp dp))" |
36 (* |
40 (* |
1354 apply (rule valid.intros(2)) |
1358 apply (rule valid.intros(2)) |
1355 apply (simp_all split:option.splits add:sectxt_of_obj_simps) |
1359 apply (simp_all split:option.splits add:sectxt_of_obj_simps) |
1356 apply (auto simp add:proc_file_fds_def)[1] |
1360 apply (auto simp add:proc_file_fds_def)[1] |
1357 apply (auto simp:inherit_fds_check_def sectxt_of_obj_simps sectxts_of_fds_def inherit_fds_check_ctxt_def) |
1361 apply (auto simp:inherit_fds_check_def sectxt_of_obj_simps sectxts_of_fds_def inherit_fds_check_ctxt_def) |
1358 done |
1362 done |
1359 moreover have "\<And>f flags fd inum. |
1363 moreover have "\<And>f flags fd opt. \<lbrakk>valid (Open p f flags fd opt # enrich_proc s p p'); |
1360 \<lbrakk>valid (Open p f flags fd inum # enrich_proc s p p'); is_created_proc s p\<rbrakk> |
1364 is_created_proc s p; valid (Open p f flags fd opt # s); p' \<notin> all_procs s\<rbrakk> |
1361 \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd inum # Open p f flags fd inum # enrich_proc s p p')" |
1365 \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')" |
1362 sorry |
1366 proof- |
|
1367 fix f flags fd inum |
|
1368 assume a1: "valid (Open p f flags fd inum # enrich_proc s p p')" and a2: "is_created_proc s p" |
|
1369 and a3: "valid (Open p f flags fd inum # s)" and a4: "p' \<notin> all_procs s" |
|
1370 show "valid (Open p' f (remove_create_flag flags) fd inum # Open p f flags fd inum # enrich_proc s p p')" |
|
1371 proof (cases " |
|
1372 apply (rule_tac valid.intros(2)) |
|
1373 apply (simp_all add:a1) |
|
1374 |
|
1375 |
|
1376 |
|
1377 |
|
1378 |
|
1379 sorry |
1363 moreover have "\<And>fd. \<lbrakk>valid (CloseFd p fd # enrich_proc s p p'); is_created_proc s p; |
1380 moreover have "\<And>fd. \<lbrakk>valid (CloseFd p fd # enrich_proc s p p'); is_created_proc s p; |
1364 valid (CloseFd p fd # s); p' \<notin> all_procs s\<rbrakk> |
1381 valid (CloseFd p fd # s); p' \<notin> all_procs s; fd \<in> proc_file_fds s p\<rbrakk> |
1365 \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
1382 \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
1366 proof- |
1383 proof- |
1367 fix fd |
1384 fix fd |
1368 assume a1: "valid (CloseFd p fd # enrich_proc s p p')" and a2: "is_created_proc s p" |
1385 assume a1: "valid (CloseFd p fd # enrich_proc s p p')" and a2: "is_created_proc s p" |
1369 and a3: "p' \<notin> all_procs s" and a4: "valid (CloseFd p fd # s)" |
1386 and a3: "p' \<notin> all_procs s" and a4: "valid (CloseFd p fd # s)" |
|
1387 and a5: "fd \<in> proc_file_fds s p" |
1370 from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3) |
1388 from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3) |
1371 have "p' \<in> current_procs (enrich_proc s p p')" |
1389 have "p' \<in> current_procs (enrich_proc s p p')" |
1372 using a2 a3 vd |
1390 using a2 a3 vd |
1373 by (auto intro:enrich_proc_dup_in) |
1391 by (auto intro:enrich_proc_dup_in) |
1374 moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'" |
1392 moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'" |
|
1393 using a5 a2 a3 vd pre' |
|
1394 apply (simp) |
|
1395 apply (drule_tac s = "enrich_proc s p p'" and p = p' in file_fds_subset_pfds) |
|
1396 apply (erule set_mp) |
|
1397 apply (simp add:enrich_proc_dup_ffds) |
|
1398 done |
1375 ultimately show "valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
1399 ultimately show "valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
1376 apply (rule valid.intros(2)) |
1400 apply (rule_tac valid.intros(2)) |
1377 apply (simp_all add:a1 a0 a2 pre') |
1401 apply (simp_all add:a1 a0 a2 pre') |
1378 |
1402 done |
1379 |
1403 qed |
1380 |
|
1381 sorry |
|
1382 (* |
|
1383 thus ?thesis using created_cons vd_cons all_procs_cons |
|
1384 apply (case_tac e) |
|
1385 apply (auto simp:is_created_proc_simps split:if_splits) |
|
1386 *) |
|
1387 ultimately show ?thesis using created_cons vd_cons all_procs_cons |
1404 ultimately show ?thesis using created_cons vd_cons all_procs_cons |
1388 apply (case_tac e) |
1405 apply (case_tac e) |
1389 apply (auto simp:is_created_proc_simps split:if_splits) |
1406 apply (auto simp:is_created_proc_simps split:if_splits) |
1390 done |
1407 done |
1391 qed |
1408 qed |