1199 apply (erule enrich_proc_dup_ffd', simp+) |
1199 apply (erule enrich_proc_dup_ffd', simp+) |
1200 apply (rule_tac x = f in exI) |
1200 apply (rule_tac x = f in exI) |
1201 apply (erule enrich_proc_dup_ffd, simp+) |
1201 apply (erule enrich_proc_dup_ffd, simp+) |
1202 done |
1202 done |
1203 |
1203 |
1204 lemma enrich_proc_prop: |
1204 lemma enrich_proc_dup_ffds_eq_fds: |
1205 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
1205 "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk> |
1206 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
1206 \<Longrightarrow> current_proc_fds (enrich_proc s p p') p' = proc_file_fds s p" |
1207 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
1207 apply (induct s arbitrary:p) |
1208 (\<forall> obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and> |
1208 apply (simp add: is_created_proc_def) |
1209 (files_hung_by_del (enrich_proc s p p') = files_hung_by_del s) \<and> |
1209 apply (frule not_all_procs_prop3) |
1210 (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and> |
1210 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
1211 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
1211 apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3 |
1212 (\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> |
1212 simp:proc_file_fds_def is_created_proc_def) |
1213 (\<forall> tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f) \<and> |
1213 done |
1214 (\<forall> tp fd flags. flags_of_proc_fd s tp fd = Some flags \<longrightarrow> |
1214 |
1215 flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and> |
1215 lemma oflags_check_remove_create: |
1216 (\<forall> q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and> |
1216 "oflags_check flags sp sf \<Longrightarrow> oflags_check (remove_create_flag flags) sp sf" |
1217 (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and> |
1217 apply (case_tac flags) |
1218 (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
1218 apply (auto simp:oflags_check_def perms_of_flags_def perm_of_oflag_def split:bool.splits) |
1219 (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)" |
1219 done |
1220 proof (induct s) |
1220 |
1221 case Nil |
1221 end |
1222 thus ?case by (auto simp:is_created_proc_def) |
1222 |
1223 next |
1223 end |
1224 case (Cons e s) |
|
1225 hence vd_cons: "valid (e # s)" and created_cons: "is_created_proc (e # s) p" |
|
1226 and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s" |
|
1227 and os: "os_grant s e" and grant: "grant s e" |
|
1228 by (auto dest:vd_cons vt_grant_os vt_grant) |
|
1229 from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto) |
|
1230 from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and> |
|
1231 (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
|
1232 (\<forall>obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and> |
|
1233 files_hung_by_del (enrich_proc s p p') = files_hung_by_del s \<and> |
|
1234 (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and> |
|
1235 (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
|
1236 (\<forall>q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> |
|
1237 (\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f) \<and> |
|
1238 (\<forall>tp fd flags. |
|
1239 flags_of_proc_fd s tp fd = Some flags \<longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and> |
|
1240 (\<forall>q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and> |
|
1241 (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and> |
|
1242 (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
|
1243 (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)" |
|
1244 using vd all_procs by auto |
|
1245 have alive_pre: "is_created_proc s p \<Longrightarrow> (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj)" |
|
1246 using pre by simp |
|
1247 hence curf_pre: "is_created_proc s p \<Longrightarrow> (\<forall>f. f \<in> current_files s \<longrightarrow> f \<in> current_files (enrich_proc s p p'))" |
|
1248 using vd apply auto |
|
1249 apply (drule is_file_or_dir, simp) |
|
1250 apply (erule disjE) |
|
1251 apply (erule_tac x = "O_file f" in allE, simp add:is_file_in_current) |
|
1252 apply (erule_tac x = "O_dir f" in allE, simp add:is_dir_in_current) |
|
1253 done |
|
1254 have "valid (enrich_proc (e # s) p p')" |
|
1255 proof- |
|
1256 from pre have pre': "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp |
|
1257 have "is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" |
|
1258 apply (frule pre') |
|
1259 apply (erule_tac s = s in enrich_valid_intro_cons) |
|
1260 apply (simp_all add:os grant vd pre) |
|
1261 done |
|
1262 moreover have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p; |
|
1263 valid (Execve p f fds # s); p' \<notin> all_procs s\<rbrakk> |
|
1264 \<Longrightarrow> valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')" |
|
1265 proof- |
|
1266 fix f fds |
|
1267 assume a1: "valid (Execve p f fds # enrich_proc s p p')" and a2: "is_created_proc s p" |
|
1268 and a3: "valid (Execve p f fds # s)" and a0: "p' \<notin> all_procs s" |
|
1269 have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp" |
|
1270 and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf" |
|
1271 and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd" |
|
1272 and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> |
|
1273 file_of_proc_fd (enrich_proc s p p') tp fd = Some f" |
|
1274 and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p" |
|
1275 and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd" |
|
1276 using pre a2 by auto |
|
1277 show "valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')" |
|
1278 proof- |
|
1279 from a0 a3 have a0': "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3) |
|
1280 from a3 have grant: "grant s (Execve p f fds)" and os: "os_grant s (Execve p f fds)" |
|
1281 by (auto dest:vt_grant_os vt_grant simp del:os_grant.simps) |
|
1282 have f_in: "is_file (enrich_proc s p p') f" |
|
1283 proof- |
|
1284 from pre a2 |
|
1285 have a4: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj" |
|
1286 by (auto) |
|
1287 show ?thesis using a3 a4 |
|
1288 apply (erule_tac x = "O_file f" in allE) |
|
1289 by (auto dest:vt_grant_os) |
|
1290 qed |
|
1291 moreover have a5: "proc_file_fds s p \<subseteq> proc_file_fds (Execve p f fds # enrich_proc s p p') p'" |
|
1292 using a3 a0' |
|
1293 apply (frule_tac vt_grant_os) |
|
1294 apply (auto simp:proc_file_fds_def) |
|
1295 apply (rule_tac x = fa in exI) |
|
1296 apply (erule enrich_proc_dup_ffd) |
|
1297 apply (simp_all add:vd all_procs a2) |
|
1298 done |
|
1299 ultimately have "os_grant (Execve p f fds # enrich_proc s p p') (Execve p' f (fds \<inter> proc_file_fds s p))" |
|
1300 apply (auto simp:is_file_simps enrich_proc_dup_in a2 vd all_procs a1 enrich_proc_dup_ffds) |
|
1301 done |
|
1302 moreover have "grant (Execve p f fds # enrich_proc s p p') (Execve p' f (fds \<inter> proc_file_fds s p))" |
|
1303 proof- |
|
1304 from grant obtain up rp tp uf rf tf |
|
1305 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
|
1306 and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" |
|
1307 by (simp split:option.splits, blast) |
|
1308 with grant obtain pu nr nt where p3: "npctxt_execve (up, rp, tp) (uf, rf, tf) = Some (pu, nr, nt)" |
|
1309 by (simp split:option.splits del:npctxt_execve.simps, blast) |
|
1310 have p1': "sectxt_of_obj (Execve p f fds # enrich_proc s p p') (O_proc p') = Some (up, rp, tp)" |
|
1311 using p1 dup_sp a1 a0' |
|
1312 apply (simp add:sectxt_of_obj_simps) |
|
1313 by (simp add:cp2sproc_def split:option.splits) |
|
1314 from os have f_in': "is_file s f" by simp |
|
1315 from vd os have "\<exists> sf. cf2sfile s f = Some sf" |
|
1316 by (auto dest!:is_file_in_current current_file_has_sfile) |
|
1317 hence p2': "sectxt_of_obj (Execve p f fds # enrich_proc s p p') (O_file f) = Some (uf, rf, tf)" |
|
1318 using f_in p2 cf2sf os a1 |
|
1319 apply (erule_tac x = f in allE) |
|
1320 apply (auto dest:is_file_in_current simp:cf2sfile_def sectxt_of_obj_simps split:option.splits) |
|
1321 apply (case_tac f, simp) |
|
1322 apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) |
|
1323 done |
|
1324 from dup_sfd a5 have "\<forall>fd. fd \<in> proc_file_fds s p \<longrightarrow> |
|
1325 cfd2sfd (Execve p f fds # enrich_proc s p p') p' fd = cfd2sfd s p fd" |
|
1326 apply (rule_tac allI) |
|
1327 apply (erule_tac x = fd in allE, clarsimp) |
|
1328 apply (drule set_mp, simp) |
|
1329 apply (auto simp:cfd2sfd_execve proc_file_fds_def a1) |
|
1330 done |
|
1331 hence "inherit_fds_check (Execve p f fds # enrich_proc s p p') (up, nr, nt) p' (fds \<inter> proc_file_fds s p)" |
|
1332 using grant os p1 p2 p3 vd |
|
1333 apply (clarsimp) |
|
1334 apply (rule_tac s = s and p = p and fds = fds in enrich_inherit_fds_check_dup) |
|
1335 apply simp_all |
|
1336 done |
|
1337 moreover have "search_check (Execve p f fds # enrich_proc s p p') (up, rp, tp) f" |
|
1338 using p1 p2 p2' vd cf2sf f_in f_in' grant p3 f_in a1 |
|
1339 apply (rule_tac s = s in enrich_search_check) |
|
1340 apply (simp_all add:is_file_simps) |
|
1341 apply (rule allI, rule impI, erule_tac x = fa in allE, simp) |
|
1342 apply (drule_tac ff = fa in cf2sfile_other') |
|
1343 by (auto simp:a2 curf_pre) |
|
1344 ultimately show ?thesis |
|
1345 using p1' p2' p3 |
|
1346 apply (simp split:option.splits) |
|
1347 using grant p1 p2 |
|
1348 apply simp |
|
1349 done |
|
1350 qed |
|
1351 ultimately show ?thesis using a1 |
|
1352 by (erule_tac valid.intros(2), auto) |
|
1353 qed |
|
1354 qed |
|
1355 moreover have "\<And>tp fds. \<lbrakk>valid (Clone tp p fds # s); p' \<noteq> p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> |
|
1356 valid (Clone tp p' (fds \<inter> proc_file_fds s tp) # Clone tp p fds # s)" |
|
1357 apply (frule vt_grant_os, frule vt_grant, drule not_all_procs_prop3) |
|
1358 apply (rule valid.intros(2)) |
|
1359 apply (simp_all split:option.splits add:sectxt_of_obj_simps) |
|
1360 apply (auto simp add:proc_file_fds_def)[1] |
|
1361 apply (auto simp:inherit_fds_check_def sectxt_of_obj_simps sectxts_of_fds_def inherit_fds_check_ctxt_def) |
|
1362 done |
|
1363 moreover have "\<And>f flags fd opt. \<lbrakk>valid (Open p f flags fd opt # enrich_proc s p p'); |
|
1364 is_created_proc s p; valid (Open p f flags fd opt # s); p' \<notin> all_procs s\<rbrakk> |
|
1365 \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')" |
|
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 |
|
1380 moreover have "\<And>fd. \<lbrakk>valid (CloseFd p fd # enrich_proc s p p'); is_created_proc s p; |
|
1381 valid (CloseFd p fd # s); p' \<notin> all_procs s; fd \<in> proc_file_fds s p\<rbrakk> |
|
1382 \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
|
1383 proof- |
|
1384 fix fd |
|
1385 assume a1: "valid (CloseFd p fd # enrich_proc s p p')" and a2: "is_created_proc s p" |
|
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" |
|
1388 from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3) |
|
1389 have "p' \<in> current_procs (enrich_proc s p p')" |
|
1390 using a2 a3 vd |
|
1391 by (auto intro:enrich_proc_dup_in) |
|
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 |
|
1399 ultimately show "valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
|
1400 apply (rule_tac valid.intros(2)) |
|
1401 apply (simp_all add:a1 a0 a2 pre') |
|
1402 done |
|
1403 qed |
|
1404 ultimately show ?thesis using created_cons vd_cons all_procs_cons |
|
1405 apply (case_tac e) |
|
1406 apply (auto simp:is_created_proc_simps split:if_splits) |
|
1407 done |
|
1408 qed |
|
1409 moreover have "\<forall>obj. alive (e # s) obj \<longrightarrow> alive (enrich_proc (e # s) p p') obj" |
|
1410 sorry |
|
1411 moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj" |
|
1412 sorry |
|
1413 moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)" |
|
1414 sorry |
|
1415 moreover have "\<forall>p. p \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') p = cp2sproc (e # s) p" |
|
1416 sorry |
|
1417 moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" |
|
1418 sorry |
|
1419 moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q" |
|
1420 sorry |
|
1421 moreover have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> |
|
1422 file_of_proc_fd (enrich_proc (e # s) p p') p fd = Some f" |
|
1423 sorry |
|
1424 moreover have "\<forall>p fd flags. flags_of_proc_fd (e # s) p fd = Some flags \<longrightarrow> |
|
1425 flags_of_proc_fd (enrich_proc (e # s) p p') p fd = Some flags" |
|
1426 sorry |
|
1427 moreover have "\<forall>q. msgs_of_queue (enrich_proc (e # s) p p') q = msgs_of_queue (e # s) q" |
|
1428 sorry |
|
1429 moreover have "\<forall>p fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow> |
|
1430 cfd2sfd (enrich_proc (e # s) p p') p fd = cfd2sfd (e # s) p fd" |
|
1431 sorry |
|
1432 ultimately show ?case |
|
1433 by auto |
|
1434 qed |
|
1435 |
|
1436 |
|
1437 lemma enrich_proc_valid: |
|
1438 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')" |
|
1439 by (auto dest:enrich_proc_prop) |
|
1440 |
|
1441 lemma enrich_proc_valid: |
|
1442 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> " |
|
1443 |
|
1444 |
|
1445 |
|