5 

     6 datatype t_enrich_obj = 

     7   E_proc "t_process"

     8 | E_file "t_file"

     9 | E_fd   "t_process" "t_fd"

    10 | E_inum "nat"

    11 | E_msgq "t_msgq"

    12 | E_msg  "t_msgq"    "t_msg"

    89 lemma enrich_search_check':

    90   assumes grant: "search_check s (up, rp, tp) f"

    91   and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"

    92   and vd: "valid s" and vd': "valid s'" and f_in: "is_dir s f"  and f_in': "is_dir s' f"

    93   and sec: "sectxt_of_obj s' (O_dir f) = sectxt_of_obj s (O_dir f)"

    94   shows "search_check s' (up, rp, tp) f"

    95 proof (cases f)

    96   case Nil

    97   have "sectxt_of_obj s' (O_dir []) = sectxt_of_obj s (O_dir [])"

    98     using cf2sf 

    99     apply (erule_tac x = "[]" in allE)

   100     by (auto simp:cf2sfile_def root_sec_remains vd vd')

   101   thus ?thesis using grant Nil 

   102     by auto

   103 next

   104   case (Cons n pf)

   105   from vd f_in obtain sf where sf: "cf2sfile s f = Some sf"

   106     apply (drule_tac is_dir_in_current, drule_tac current_file_has_sfile, simp)

   107     apply (erule exE, simp)

   108     done

   109   then obtain psfs where psfs: "get_parentfs_ctxts s pf = Some psfs" using Cons

   110     by (auto simp:cf2sfile_def split:option.splits if_splits)

   111   from sf cf2sf f_in have sf': "cf2sfile s' f = Some sf" by (auto dest:is_dir_in_current)

   112   then obtain psfs' where psfs': "get_parentfs_ctxts s' pf = Some psfs'"using Cons

   113     by (auto simp:cf2sfile_def split:option.splits if_splits)

   114   with sf sf' psfs have psfs_eq: "set psfs' = set psfs" using Cons f_in f_in'

   115     apply (drule_tac is_dir_not_file)

   116     apply (drule is_dir_not_file)    

   117     apply (simp add:cf2sfile_def split:option.splits)

   118     apply (case_tac sf, simp)

   119     done

   120   show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec

   121     apply (drule_tac is_dir_not_file)

   122     apply (drule_tac is_dir_not_file)

   123     apply (simp add:Cons split:option.splits)

   124     by (case_tac a, simp)

   125 qed

   126 

   201     and hungs: "files_hung_by_del s' = files_hung_by_del s"

   204     and cq2sq: "\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq s' q = cq2smsgq s q"

   206     and fflags_remain: "\<forall> p fd flags. flags_of_proc_fd s p fd = Some flags \<longrightarrow> flags_of_proc_fd s' p fd = Some flags"

   207     and sms_remain: "\<forall> q. msgs_of_queue s' q = msgs_of_queue s q"

   208    (* and empty_remain: "\<forall> f. dir_is_empty s f \<longrightarrow> dir_is_empty s' f" *)

   297   case (Kill p p')

   298   have p_in: "p \<in> current_procs s'" using os alive

   299     apply (erule_tac x = "O_proc p" in allE)

   300     by (auto simp:Kill)

   301   have p'_in: "p' \<in> current_procs s'" using os alive

   302     apply (erule_tac x = "O_proc p'" in allE)

   303     by (auto simp:Kill)

   304   have "os_grant s' e" using p_in p'_in by (simp add:Kill)

   305   moreover have "grant s' e" 

   306   proof-

   307     from grant obtain up rp tp up' rp' tp'

   308       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   309       and p'1: "sectxt_of_obj s (O_proc p') = Some (up', rp', tp')"

   310       apply (simp add:Kill split:option.splits)

   311       by (case_tac a, case_tac aa, blast)

   312     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   313       using os cp2sp

   314       apply (erule_tac x = p in allE)

   315       by (auto simp:Kill co2sobj.simps cp2sproc_def split:option.splits)

   316     from p'1 have p'1': "sectxt_of_obj s' (O_proc p') = Some (up', rp', tp')"

   317       using os cp2sp

   318       apply (erule_tac x = p' in allE)

   319       by (auto simp:Kill co2sobj.simps cp2sproc_def split:option.splits)

   320     show ?thesis using p1 p'1 p1' p'1' grant

   321       by (simp add:Kill)

   322   qed

   323   ultimately show ?thesis using vs'

   324     by (erule_tac valid.intros(2), simp+)

   325 next

   326   case (Ptrace p p')

   327   have p_in: "p \<in> current_procs s'" using os alive

   328     apply (erule_tac x = "O_proc p" in allE)

   329     by (auto simp:Ptrace)

   330   have p'_in: "p' \<in> current_procs s'" using os alive

   331     apply (erule_tac x = "O_proc p'" in allE)

   332     by (auto simp:Ptrace)

   333   have "os_grant s' e" using p_in p'_in by (simp add:Ptrace)

   334   moreover have "grant s' e" 

   335   proof-

   336     from grant obtain up rp tp up' rp' tp'

   337       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   338       and p'1: "sectxt_of_obj s (O_proc p') = Some (up', rp', tp')"

   339       apply (simp add:Ptrace split:option.splits)

   340       by (case_tac a, case_tac aa, blast)

   341     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   342       using os cp2sp

   343       apply (erule_tac x = p in allE)

   344       by (auto simp:Ptrace co2sobj.simps cp2sproc_def split:option.splits)

   345     from p'1 have p'1': "sectxt_of_obj s' (O_proc p') = Some (up', rp', tp')"

   346       using os cp2sp

   347       apply (erule_tac x = p' in allE)

   348       by (auto simp:Ptrace co2sobj.simps cp2sproc_def split:option.splits)

   349     show ?thesis using p1 p'1 p1' p'1' grant

   350       by (simp add:Ptrace)

   351   qed

   352   ultimately show ?thesis using vs'

   353     by (erule_tac valid.intros(2), simp+)

   354 next

   355   case (Exit p)

   356   have p_in: "p \<in> current_procs s'" using os alive

   357     apply (erule_tac x = "O_proc p" in allE)

   358     by (auto simp:Exit)

   359   have "os_grant s' e" using p_in by (simp add:Exit)

   360   moreover have "grant s' e" 

   361     by (simp add:Exit)

   362   ultimately show ?thesis using vs'

   363     by (erule_tac valid.intros(2), simp+)

   364 next

   365   case (Open p f flags fd opt)

   366   show ?thesis

   367   proof (cases opt)

   368     case None

   369     have p_in: "p \<in> current_procs s'" using os alive

   370       apply (erule_tac x = "O_proc p" in allE)

   371       by (auto simp:Open None)

   372     have f_in: "is_file s' f" using os alive

   373       apply (erule_tac x = "O_file f" in allE)

   374       by (auto simp:Open None)

   375     have fd_not_in: "fd \<notin> current_proc_fds s' p"

   376       using os alive' p_in

   377       apply (erule_tac x = "E_fd p fd" in allE)

   378       by (simp add:Open None)

   379     have "os_grant s' e" using p_in f_in fd_not_in os

   380       by (simp add:Open None)

   381     moreover have "grant s' e" 

   382     proof-

   383       from grant obtain up rp tp uf rf tf 

   384         where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   385         and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 

   386         apply (simp add:Open None split:option.splits)

   387         by (case_tac a, case_tac aa, blast)

   388       from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   389         using os cp2sp

   390         apply (erule_tac x = p in allE)

   391         by (auto simp:Open None co2sobj.simps cp2sproc_def split:option.splits)

   392       from os have f_in': "is_file s f" by (simp add:Open None)

   393       from vd os have "\<exists> sf. cf2sfile s f = Some sf"

   394         by (auto dest!:is_file_in_current current_file_has_sfile simp:Open None)

   395       hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf

   396         apply (erule_tac x = f in allE)

   397         apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits)

   398         apply (case_tac f, simp)

   399         apply (drule_tac s = s in root_is_dir', simp add:vd, simp+)

   400         done

   401       have "search_check s' (up, rp, tp) f"

   402         using p1 p2 p2' vd cf2sf f_in' grant Open None f_in

   403         apply (rule_tac s = s in enrich_search_check)

   404         by (simp_all split:option.splits)

   405       thus ?thesis using p1' p2' 

   406         apply (simp add:Open None split:option.splits) 

   407         using grant Open None p1 p2 

   408         by simp

   409     qed

   410     ultimately show ?thesis using vs'

   411       by (erule_tac valid.intros(2), simp+)

   412   next

   413     case (Some inum)

   414     from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f = Some pf"

   415       by (auto simp:Open Some)

   416     have pf_in: "is_dir s' pf" using pf_in_s alive

   417       apply (erule_tac x = "O_dir pf" in allE)

   418       by simp

   419     have p_in: "p \<in> current_procs s'" using os alive

   420       apply (erule_tac x = "O_proc p" in allE)

   421       by (auto simp:Open Some)

   422     have f_not_in: "f \<notin> current_files s'" using os alive'

   423       apply (erule_tac x = "E_file f" in allE)

   424       by (auto simp:Open Some)

   425     have fd_not_in: "fd \<notin> current_proc_fds s' p"

   426       using os alive' p_in

   427       apply (erule_tac x = "E_fd p fd" in allE)

   428       by (simp add:Open Some)

   429     have inum_not_in: "inum \<notin> current_inode_nums s'"

   430       using os alive' 

   431       apply (erule_tac x = "E_inum inum" in allE)

   432       by (simp add:Open Some)

   433     have "os_grant s' e" using p_in pf_in parent f_not_in fd_not_in inum_not_in os

   434       by (simp add:Open Some hungs)

   435     moreover have "grant s' e"  

   436     proof-

   437       from grant parent obtain up rp tp uf rf tf 

   438         where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   439         and p2: "sectxt_of_obj s (O_dir pf) = Some (uf, rf, tf)" 

   440         apply (simp add:Open Some split:option.splits)

   441         by (case_tac a, case_tac aa, blast)

   442       from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   443         using os cp2sp

   444         apply (erule_tac x = p in allE)

   445         by (auto simp:Open Some co2sobj.simps cp2sproc_def split:option.splits)

   446       from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf"

   447         by (auto dest!:is_dir_in_current current_file_has_sfile simp:Open Some)

   448       hence p2': "sectxt_of_obj s' (O_dir pf) = Some (uf, rf, tf)" using p2 cf2sf pf_in pf_in_s

   449         apply (erule_tac x = pf in allE)

   450         apply (erule exE, frule_tac s = s in is_dir_in_current, simp)

   451         apply (drule is_dir_not_file, drule is_dir_not_file)

   452         apply (auto simp:cf2sfile_def split:option.splits)

   453         apply (case_tac pf, simp_all)

   454         by (simp add:sroot_def root_sec_remains vd vs')

   455       have "search_check s' (up, rp, tp) pf"

   456         using p1 p2 p2' vd cf2sf pf_in grant Open Some pf_in_s parent vs'

   457         apply (rule_tac s = s in enrich_search_check')

   458         by (simp_all split:option.splits)

   459       thus ?thesis using p1' p2' parent 

   460         apply (simp add:Open Some split:option.splits) 

   461         using grant Open Some p1 p2 

   462         by simp

   463     qed

   464     ultimately show ?thesis using vs'

   465       by (erule_tac valid.intros(2), simp+)

   466   qed

   467 next

   468   case (ReadFile p fd)

   469   have p_in: "p \<in> current_procs s'" using os alive

   470     apply (erule_tac x = "O_proc p" in allE)

   471     by (auto simp:ReadFile)

   472   have fd_in: "fd \<in> current_proc_fds s' p" using os alive

   473     apply (erule_tac x = "O_fd p fd" in allE)

   474     by (auto simp:ReadFile)

   475   obtain f where ffd: "file_of_proc_fd s p fd = Some f"

   476     using os ReadFile by auto

   477   hence f_in_s: "is_file s f" using vd

   478     by (auto intro:file_of_pfd_is_file)

   479   obtain flags where fflag: "flags_of_proc_fd s p fd = Some flags"

   480     using os ReadFile by auto

   481   have ffd_in: "file_of_proc_fd s' p fd = Some f"

   482     using ffd_remain ffd by auto

   483   hence f_in: "is_file s' f" using vs'

   484     by (auto intro:file_of_pfd_is_file)

   485   have flags_in: "flags_of_proc_fd s' p fd = Some flags"

   486     using fflags_remain fflag by auto

   487   have "os_grant s' e" using p_in fd_in ffd_in flags_in fflag os f_in 

   488     by (auto simp add:ReadFile is_file_in_current)

   489   moreover have "grant s' e" 

   490   proof-

   491     from grant ffd obtain up rp tp uf rf tf ufd rfd tfd

   492       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   493       and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)"

   494       and p3: "sectxt_of_obj s (O_fd p fd) = Some (ufd, rfd, tfd)"

   495       apply (simp add:ReadFile split:option.splits)

   496       by (case_tac a, case_tac aa, case_tac ab, blast)

   497     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   498       using os cp2sp

   499       apply (erule_tac x = p in allE)

   500       by (auto simp:ReadFile co2sobj.simps cp2sproc_def split:option.splits)

   501     from vd f_in_s have "\<exists> sf. cf2sfile s f = Some sf"

   502       by (auto dest!:is_file_in_current current_file_has_sfile)

   503     hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in_s p2 cf2sf

   504       apply (erule_tac x = f in allE)

   505       apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits)

   506       apply (case_tac f, simp)

   507       apply (drule_tac s = s in root_is_dir', simp add:vd, simp+)

   508       done

   509     have p3': "sectxt_of_obj s' (O_fd p fd) = Some (ufd, rfd, tfd)" 

   510       using cfd2sfd ffd_in ffd p3 f_in f_in_s vd

   511       apply (erule_tac x = p in allE)

   512       apply (erule_tac x = fd in allE)

   513       apply (simp add:proc_file_fds_def)

   514       apply (auto simp:cfd2sfd_def fflag flags_in p3 split:option.splits

   515         dest!:current_file_has_sfile' simp:is_file_in_current)

   516       done

   517     show ?thesis using p1' p2' p3' ffd_in ffd

   518       apply (simp add:ReadFile split:option.splits) 

   519       using grant p1 p2 p3 ReadFile

   520       by simp

   521   qed

   522   ultimately show ?thesis using vs'

   523     by (erule_tac valid.intros(2), simp+)

   524 next

   525   case (WriteFile p fd)

   526   have p_in: "p \<in> current_procs s'" using os alive

   527     apply (erule_tac x = "O_proc p" in allE)

   528     by (auto simp:WriteFile)

   529   have fd_in: "fd \<in> current_proc_fds s' p" using os alive

   530     apply (erule_tac x = "O_fd p fd" in allE)

   531     by (auto simp:WriteFile)

   532   obtain f where ffd: "file_of_proc_fd s p fd = Some f"

   533     using os WriteFile by auto

   534   hence f_in_s: "is_file s f" using vd

   535     by (auto intro:file_of_pfd_is_file)

   536   obtain flags where fflag: "flags_of_proc_fd s p fd = Some flags"

   537     using os WriteFile by auto

   538   have ffd_in: "file_of_proc_fd s' p fd = Some f"

   539     using ffd_remain ffd by auto

   540   hence f_in: "is_file s' f" using vs'

   541     by (auto intro:file_of_pfd_is_file)

   542   have flags_in: "flags_of_proc_fd s' p fd = Some flags"

   543     using fflags_remain fflag by auto

   544   have "os_grant s' e" using p_in fd_in ffd_in flags_in fflag os f_in 

   545     by (auto simp add:WriteFile is_file_in_current)

   546   moreover have "grant s' e" 

   547   proof-

   548     from grant ffd obtain up rp tp uf rf tf ufd rfd tfd

   549       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   550       and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)"

   551       and p3: "sectxt_of_obj s (O_fd p fd) = Some (ufd, rfd, tfd)"

   552       apply (simp add:WriteFile split:option.splits)

   553       by (case_tac a, case_tac aa, case_tac ab, blast)

   554     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   555       using os cp2sp

   556       apply (erule_tac x = p in allE)

   557       by (auto simp:WriteFile co2sobj.simps cp2sproc_def split:option.splits)

   558     from vd f_in_s have "\<exists> sf. cf2sfile s f = Some sf"

   559       by (auto dest!:is_file_in_current current_file_has_sfile)

   560     hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in_s p2 cf2sf

   561       apply (erule_tac x = f in allE)

   562       apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits)

   563       apply (case_tac f, simp)

   564       apply (drule_tac s = s in root_is_dir', simp add:vd, simp+)

   565       done

   566     have p3': "sectxt_of_obj s' (O_fd p fd) = Some (ufd, rfd, tfd)" 

   567       using cfd2sfd ffd_in ffd p3 f_in f_in_s vd

   568       apply (erule_tac x = p in allE)

   569       apply (erule_tac x = fd in allE)

   570       apply (simp add:proc_file_fds_def)

   571       apply (auto simp:cfd2sfd_def fflag flags_in p3 split:option.splits

   572         dest!:current_file_has_sfile' simp:is_file_in_current)

   573       done

   574     show ?thesis using p1' p2' p3' ffd_in ffd

   575       apply (simp add:WriteFile split:option.splits) 

   576       using grant p1 p2 p3 WriteFile

   577       by simp

   578   qed

   579   ultimately show ?thesis using vs'

   580     by (erule_tac valid.intros(2), simp+)

   581 next

   582   case (CloseFd p fd)

   583   have p_in: "p \<in> current_procs s'" using os alive

   584     apply (erule_tac x = "O_proc p" in allE)

   585     by (auto simp:CloseFd)

   586   have fd_in: "fd \<in> current_proc_fds s' p" using os alive

   587     apply (erule_tac x = "O_fd p fd" in allE)

   588     by (auto simp:CloseFd)

   589   have "os_grant s' e" using p_in fd_in 

   590     by (auto simp add:CloseFd)

   591   moreover have "grant s' e" 

   592     by(simp add:CloseFd)

   593   ultimately show ?thesis using vs'

   594     by (erule_tac valid.intros(2), simp+)

   595 next

   596   case (UnLink p f)

   597   have p_in: "p \<in> current_procs s'" using os alive

   598     apply (erule_tac x = "O_proc p" in allE)

   599     by (auto simp:UnLink)

   600   have f_in: "is_file s' f" using os alive

   601     apply (erule_tac x = "O_file f" in allE)

   602     by (auto simp:UnLink)

   603   from os vd obtain pf where pf_in_s: "is_dir s pf"

   604     and parent: "parent f = Some pf"

   605     by (auto simp:UnLink dest!:file_has_parent)

   606   from pf_in_s alive have pf_in: "is_dir s' pf"

   607     apply (erule_tac x = "O_dir pf" in allE)

   608     by (auto simp:UnLink)

   609   have "os_grant s' e" using p_in f_in os

   610     by (simp add:UnLink hungs)

   611   moreover have "grant s' e" 

   612   proof-    

   613     from grant parent obtain up rp tp uf rf tf upf rpf tpf

   614       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   615       and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 

   616       and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" 

   617       apply (simp add:UnLink split:option.splits)

   618       by (case_tac a, case_tac aa, case_tac ab, blast) 

   619     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   620       using os cp2sp

   621       apply (erule_tac x = p in allE)

   622       by (auto simp:UnLink co2sobj.simps cp2sproc_def split:option.splits)

   623     from vd os pf_in_s have "\<exists> sf. cf2sfile s f = Some sf"

   624       by (auto dest!:is_file_in_current current_file_has_sfile simp:UnLink)

   625     hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" 

   626       using p2 cf2sf f_in os parent 

   627       apply (erule_tac x = f in allE)

   628       apply (erule exE, clarsimp simp:UnLink)

   629       apply (frule_tac s = s in is_file_in_current, simp)

   630       by (auto simp:cf2sfile_def split:option.splits)

   631     from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf"

   632       by (auto dest!:is_dir_in_current current_file_has_sfile simp:UnLink)

   633     hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s

   634       apply (erule_tac x = pf in allE)

   635       apply (erule exE, frule_tac s = s in is_dir_in_current, simp)

   636       apply (drule is_dir_not_file, drule is_dir_not_file)

   637       apply (auto simp:cf2sfile_def split:option.splits)

   638       apply (case_tac pf, simp_all)

   639       by (simp add:sroot_def root_sec_remains vd vs')

   640     have "search_check s' (up, rp, tp) f"

   641       using p1 p2 p2' vd cf2sf f_in grant UnLink os parent vs'

   642       apply (rule_tac s = s in enrich_search_check)

   643       by (simp_all split:option.splits)

   644     thus ?thesis using p1' p2' p3' parent 

   645       apply (simp add:UnLink split:option.splits) 

   646       using grant UnLink p1 p2 p3

   647       by simp

   648   qed

   649   ultimately show ?thesis using vs'

   650     by (erule_tac valid.intros(2), simp+)

   651 next

   652   case (Rmdir p f)

   653   have p_in: "p \<in> current_procs s'" using os alive

   654     apply (erule_tac x = "O_proc p" in allE)

   655     by (auto simp:Rmdir)

   656   have f_in: "is_dir s' f" using os alive

   657     apply (erule_tac x = "O_dir f" in allE)

   658     by (auto simp:Rmdir dir_is_empty_def)

   659   have not_root: "f \<noteq> []" using os 

   660     by (auto simp:Rmdir)

   661   from os vd obtain pf where pf_in_s: "is_dir s pf"

   662     and parent: "parent f = Some pf"

   663     apply (auto simp:Rmdir dir_is_empty_def)

   664     apply (case_tac f, simp+)

   665     apply (drule parentf_is_dir_prop1, auto)

   666     done

   667   from pf_in_s alive have pf_in: "is_dir s' pf"

   668     apply (erule_tac x = "O_dir pf" in allE)

   669     by (auto simp:Rmdir)

   670   have empty_in: "dir_is_empty s' f" using os

   671     apply (simp add:dir_is_empty_def f_in)

   672     apply auto using alive'

   673     apply (erule_tac x = "E_file f'" in allE)

   674     by (simp add:Rmdir dir_is_empty_def)

   675   have "os_grant s' e" using p_in f_in os empty_in

   676     by (simp add:Rmdir hungs)

   677   moreover have "grant s' e" 

   678   proof-

   679     from grant parent obtain up rp tp uf rf tf upf rpf tpf

   680       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   681       and p2: "sectxt_of_obj s (O_dir f) = Some (uf, rf, tf)" 

   682       and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" 

   683       apply (simp add:Rmdir split:option.splits)

   684       by (case_tac a, case_tac aa, case_tac ab, blast) 

   685     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   686       using os cp2sp

   687       apply (erule_tac x = p in allE)

   688       by (auto simp:Rmdir co2sobj.simps cp2sproc_def split:option.splits)

   689     from vd os pf_in_s have "\<exists> sf. cf2sfile s f = Some sf"

   690       by (auto dest!:is_dir_in_current current_file_has_sfile simp:dir_is_empty_def Rmdir)

   691     hence p2': "sectxt_of_obj s' (O_dir f) = Some (uf, rf, tf)" 

   692       using p2 cf2sf f_in os parent 

   693       apply (erule_tac x = f in allE)

   694       apply (erule exE, clarsimp simp:Rmdir dir_is_empty_def)

   695       apply (frule_tac s = s in is_dir_in_current, simp)

   696       apply (drule is_dir_not_file, drule is_dir_not_file)

   697       by (auto simp:cf2sfile_def split:option.splits)

   698     from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf"

   699       by (auto dest!:is_dir_in_current current_file_has_sfile simp:Rmdir)

   700     hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s

   701       apply (erule_tac x = pf in allE)

   702       apply (erule exE, frule_tac s = s in is_dir_in_current, simp)

   703       apply (drule is_dir_not_file, drule is_dir_not_file)

   704       apply (auto simp:cf2sfile_def split:option.splits)

   705       apply (case_tac pf, simp_all)

   706       by (simp add:sroot_def root_sec_remains vd vs')

   707     have "search_check s' (up, rp, tp) f"

   708       using p1 p2 p2' vd cf2sf f_in grant Rmdir os parent vs'

   709       apply (rule_tac s = s in enrich_search_check')

   710       by (simp_all add:dir_is_empty_def split:option.splits)

   711     thus ?thesis using p1' p2' p3' parent 

   712       apply (simp add:Rmdir split:option.splits) 

   713       using grant Rmdir p1 p2 p3

   714       by simp

   715   qed

   716   ultimately show ?thesis using vs'

   717     by (erule_tac valid.intros(2), simp+)

   718 next

   719   case (Mkdir p f inum)

   720   from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f = Some pf"

   721     by (auto simp:Mkdir)

   722   have pf_in: "is_dir s' pf" using pf_in_s alive

   723     apply (erule_tac x = "O_dir pf" in allE)

   724     by simp

   725   have p_in: "p \<in> current_procs s'" using os alive

   726     apply (erule_tac x = "O_proc p" in allE)

   727     by (auto simp:Mkdir)

   728   have f_not_in: "f \<notin> current_files s'" using os alive'

   729     apply (erule_tac x = "E_file f" in allE)

   730     by (auto simp:Mkdir)

   731   have inum_not_in: "inum \<notin> current_inode_nums s'"

   732     using os alive' 

   733     apply (erule_tac x = "E_inum inum" in allE)

   734     by (simp add:Mkdir)

   735   have "os_grant s' e" using p_in pf_in parent f_not_in os inum_not_in

   736     by (simp add:Mkdir hungs)

   737   moreover have "grant s' e"  

   738   proof-

   739     from grant parent obtain up rp tp uf rf tf 

   740       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   741       and p2: "sectxt_of_obj s (O_dir pf) = Some (uf, rf, tf)" 

   742       apply (simp add:Mkdir split:option.splits)

   743       by (case_tac a, case_tac aa, blast)

   744     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   745       using os cp2sp

   746       apply (erule_tac x = p in allE)

   747       by (auto simp:Mkdir co2sobj.simps cp2sproc_def split:option.splits)

   748     from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf"

   749       by (auto dest!:is_dir_in_current current_file_has_sfile simp:Mkdir)

   750     hence p2': "sectxt_of_obj s' (O_dir pf) = Some (uf, rf, tf)" using p2 cf2sf pf_in pf_in_s

   751       apply (erule_tac x = pf in allE)

   752       apply (erule exE, frule_tac s = s in is_dir_in_current, simp)

   753       apply (drule is_dir_not_file, drule is_dir_not_file)

   754       apply (auto simp:cf2sfile_def split:option.splits)

   755       apply (case_tac pf, simp_all)

   756       by (simp add:sroot_def root_sec_remains vd vs')

   757     have "search_check s' (up, rp, tp) pf"

   758       using p1 p2 p2' vd cf2sf pf_in grant Mkdir pf_in_s parent vs'

   759       apply (rule_tac s = s in enrich_search_check')

   760       apply (simp_all split:option.splits)

   761       done

   762     thus ?thesis using p1' p2' parent 

   763       apply (simp add:Mkdir split:option.splits) 

   764       using grant Mkdir p1 p2 

   765       apply simp 

   766       done

   767   qed

   768   ultimately show ?thesis using vs'

   769     by (erule_tac valid.intros(2), simp+)

   770 next

   771   case (LinkHard p f f')

   772   from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f' = Some pf"

   773     by (auto simp:LinkHard)

   774   have pf_in: "is_dir s' pf" using pf_in_s alive

   775     apply (erule_tac x = "O_dir pf" in allE)

   776     by simp

   777   have p_in: "p \<in> current_procs s'" using os alive

   778     apply (erule_tac x = "O_proc p" in allE)

   779     by (auto simp:LinkHard)

   780   have f'_not_in: "f' \<notin> current_files s'" using os alive'

   781     apply (erule_tac x = "E_file f'" in allE)

   782     by (auto simp:LinkHard)

   783   have f_in: "is_file s' f" using os alive

   784     apply (erule_tac x = "O_file f" in allE)

   785     by (auto simp:LinkHard)

   786   have "os_grant s' e" using p_in pf_in parent os f_in f'_not_in

   787     by (simp add:LinkHard hungs)

   788   moreover have "grant s' e"

   789   proof-

   790     from grant parent obtain up rp tp uf rf tf upf rpf tpf

   791       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   792       and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 

   793       and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" 

   794       apply (simp add:LinkHard split:option.splits)

   795       by (case_tac a, case_tac aa, case_tac ab, blast) 

   796     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   797       using os cp2sp

   798       apply (erule_tac x = p in allE)

   799       by (auto simp:LinkHard co2sobj.simps cp2sproc_def split:option.splits)

   800     from vd os pf_in_s have "\<exists> sf. cf2sfile s f = Some sf"

   801       by (auto dest!:is_file_in_current current_file_has_sfile simp:LinkHard)

   802     hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" 

   803       using p2 cf2sf f_in os parent 

   804       apply (erule_tac x = f in allE)

   805       apply (erule exE, clarsimp simp:LinkHard)

   806       apply (frule_tac s = s in is_file_in_current, simp)

   807       apply (auto simp:cf2sfile_def split:option.splits)

   808       apply (case_tac f, simp)

   809       by (drule_tac s = s in root_is_dir', simp add:vd, simp+)

   810     from vd os pf_in_s have "\<exists> sf. cf2sfile s pf = Some sf"

   811       by (auto dest!:is_dir_in_current current_file_has_sfile simp:LinkHard)

   812     hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s

   813       apply (erule_tac x = pf in allE)

   814       apply (erule exE, frule_tac s = s in is_dir_in_current, simp)

   815       apply (drule is_dir_not_file, drule is_dir_not_file)

   816       apply (auto simp:cf2sfile_def split:option.splits)

   817       apply (case_tac pf, simp_all)

   818       by (simp add:sroot_def root_sec_remains vd vs')

   819     have "search_check s' (up, rp, tp) f"

   820       using p1 p2 p2' vd cf2sf f_in grant LinkHard os parent vs'

   821       apply (rule_tac s = s in enrich_search_check)

   822       by (simp_all split:option.splits)

   823     moreover have "search_check s' (up, rp, tp) pf"

   824       using p1 p3 p3' vd cf2sf pf_in grant LinkHard os parent vs'

   825       apply (rule_tac s = s in enrich_search_check')

   826       apply (simp_all split:option.splits)

   827       done

   828     ultimately show ?thesis using p1' p2' p3' parent 

   829       apply (simp add:LinkHard split:option.splits) 

   830       using grant LinkHard p1 p2 p3

   831       apply simp 

   832       done

   833   qed

   834   ultimately show ?thesis using vs'

   835     by (erule_tac valid.intros(2), simp+)

   836 next

   837   case (Truncate p f len)

   838   have p_in: "p \<in> current_procs s'" using os alive

   839     apply (erule_tac x = "O_proc p" in allE)

   840     by (auto simp:Truncate)

   841   have f_in: "is_file s' f" using os alive

   842     apply (erule_tac x = "O_file f" in allE)

   843     by (auto simp:Truncate)

   844   have "os_grant s' e" using p_in f_in by (simp add:Truncate)

   845   moreover have "grant s' e"

   846   proof-

   847     from grant obtain up rp tp uf rf tf 

   848       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   849       and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 

   850       apply (simp add:Truncate split:option.splits)

   851       by (case_tac a, case_tac aa, blast)

   852     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   853       using os cp2sp

   854       apply (erule_tac x = p in allE)

   855       by (auto simp:Truncate co2sobj.simps cp2sproc_def split:option.splits)

   856     from os have f_in': "is_file s f" by (simp add:Truncate)

   857     from vd os have "\<exists> sf. cf2sfile s f = Some sf"

   858       by (auto dest!:is_file_in_current current_file_has_sfile simp:Truncate)

   859     hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf

   860       apply (erule_tac x = f in allE)

   861       apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits)

   862       apply (case_tac f, simp)

   863       apply (drule_tac s = s in root_is_dir', simp add:vd, simp+)

   864       done

   865     have "search_check s' (up, rp, tp) f"

   866       using p1 p2 p2' vd cf2sf f_in' grant Truncate f_in

   867       apply (rule_tac s = s in enrich_search_check)

   868       by (simp_all split:option.splits)

   869     thus ?thesis using p1' p2' 

   870       apply (simp add:Truncate split:option.splits) 

   871       using grant Truncate p1 p2

   872       by (simp add:Truncate grant p1 p2)

   873   qed

   874   ultimately show ?thesis using vs'

   875     by (erule_tac valid.intros(2), simp+)

   876 next

   877   case (CreateMsgq p q)

   878   have p_in: "p \<in> current_procs s'" using os alive

   879     apply (erule_tac x = "O_proc p" in allE)

   880     by (auto simp:CreateMsgq)

   881   have q_not_in: "q \<notin> current_msgqs s'" using os alive'

   882     apply (erule_tac x = "E_msgq q" in allE)

   883     by (simp add:CreateMsgq)

   884   have "os_grant s' e" using p_in q_not_in by (simp add:CreateMsgq)

   885   moreover have "grant s' e" 

   886   proof-

   887     from grant obtain up rp tp 

   888       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   889       apply (simp add:CreateMsgq split:option.splits)

   890       by (case_tac a, blast)

   891     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   892       using os cp2sp

   893       apply (erule_tac x = p in allE)

   894       by (auto simp:CreateMsgq co2sobj.simps cp2sproc_def split:option.splits)

   895     show ?thesis using p1' 

   896       apply (simp add:CreateMsgq split:option.splits) 

   897       using grant CreateMsgq p1

   898       by simp

   899   qed

   900   ultimately show ?thesis using vs'

   901     by (erule_tac valid.intros(2), simp+)

   902 next

   903   case (RemoveMsgq p q)

   904   have p_in: "p \<in> current_procs s'" using os alive

   905     apply (erule_tac x = "O_proc p" in allE)

   906     by (auto simp:RemoveMsgq)

   907   have q_in: "q \<in> current_msgqs s'" using os alive

   908     apply (erule_tac x = "O_msgq q" in allE)

   909     by (simp add:RemoveMsgq)

   910   have "os_grant s' e" using p_in q_in by (simp add:RemoveMsgq)

   911   moreover have "grant s' e" 

   912   proof-

   913     from grant obtain up rp tp uq rq tq

   914       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   915       and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)"

   916       apply (simp add:RemoveMsgq split:option.splits)

   917       by (case_tac a, case_tac aa, blast)

   918     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   919       using os cp2sp

   920       apply (erule_tac x = p in allE)

   921       by (auto simp:RemoveMsgq co2sobj.simps cp2sproc_def split:option.splits)

   922     from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)"

   923       using os cq2sq vd

   924       apply (erule_tac x = q in allE)

   925       by (auto simp:RemoveMsgq co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits)

   926     show ?thesis using p1' p2' grant p1 p2

   927       by (simp add:RemoveMsgq)

   928   qed

   929   ultimately show ?thesis using vs'

   930     by (erule_tac valid.intros(2), simp+)  

   931 next

   932   case (SendMsg p q m)

   933   have p_in: "p \<in> current_procs s'" using os alive

   934     apply (erule_tac x = "O_proc p" in allE)

   935     by (auto simp:SendMsg)

   936   have q_in: "q \<in> current_msgqs s'" using os alive

   937     apply (erule_tac x = "O_msgq q" in allE)

   938     by (simp add:SendMsg)

   939   have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive'

   940     apply (erule_tac x = "E_msg q m" in allE)

   941     by (simp add:SendMsg q_in)

   942   have "os_grant s' e" using p_in q_in m_not_in

   943     by (simp add:SendMsg)

   944   moreover have "grant s' e" 

   945   proof-

   946     from grant obtain up rp tp uq rq tq

   947       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   948       and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)"

   949       apply (simp add:SendMsg split:option.splits)

   950       by (case_tac a, case_tac aa, blast)

   951     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   952       using os cp2sp

   953       apply (erule_tac x = p in allE)

   954       by (auto simp:SendMsg co2sobj.simps cp2sproc_def split:option.splits)

   955     from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)"

   956       using os cq2sq vd

   957       apply (erule_tac x = q in allE)

   958       by (auto simp:SendMsg co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits)

   959     show ?thesis using p1' p2' grant p1 p2

   960       by (simp add:SendMsg)

   961   qed

   962   ultimately show ?thesis using vs'

   963     by (erule_tac valid.intros(2), simp+)  

   964 next

   965   case (RecvMsg p q m)

   966   have p_in: "p \<in> current_procs s'" using os alive

   967     apply (erule_tac x = "O_proc p" in allE)

   968     by (auto simp:RecvMsg)

   969   have q_in: "q \<in> current_msgqs s'" using os alive

   970     apply (erule_tac x = "O_msgq q" in allE)

   971     by (simp add:RecvMsg) 

   972   have m_in: "m = hd (msgs_of_queue s' q)" 

   973     and sms_not_empty: "msgs_of_queue s' q \<noteq> []"

   974     using os sms_remain

   975     by (auto simp:RecvMsg)

   976   have "os_grant s' e" using p_in q_in m_in sms_not_empty os

   977     by (simp add:RecvMsg)

   978   moreover have "grant s' e" 

   979   proof-

   980     from grant obtain up rp tp uq rq tq um rm tm

   981       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"

   982       and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)"

   983       and p3: "sectxt_of_obj s (O_msg q m) = Some (um, rm, tm)"

   984       apply (simp add:RecvMsg split:option.splits)

   985       by (case_tac a, case_tac aa, case_tac ab, blast)

   986     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"

   987       using os cp2sp

   988       apply (erule_tac x = p in allE)

   989       by (auto simp:RecvMsg co2sobj.simps cp2sproc_def split:option.splits)

   990     from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)"

   991       using os cq2sq vd

   992       apply (erule_tac x = q in allE)

   993       by (auto simp:RecvMsg co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits)

   994     from p3 have p3': "sectxt_of_obj s' (O_msg q m) = Some (um, rm, tm)"

   995       using sms_remain cq2sq vd os p2 p2' p3 

   996       apply (erule_tac x = q in allE)

   997       apply (erule_tac x = q in allE)

   998       apply (clarsimp simp:RecvMsg)

   999       apply (simp add:cq2smsgq_def split:option.splits if_splits)

  1000       apply (drule current_has_sms', simp, simp)

  1001       apply (case_tac "msgs_of_queue s q", simp)

  1002       apply (simp add:cqm2sms.simps split:option.splits)

  1003       apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1]

  1004       apply (case_tac "msgs_of_queue s q", simp)

  1005       apply (simp add:cqm2sms.simps split:option.splits)

  1006       apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1]

  1007       done

  1008     show ?thesis using p1' p2' p3' grant p1 p2 p3

  1009       by (simp add:RecvMsg)

  1010   qed

  1011   ultimately show ?thesis using vs'

  1012     by (erule_tac valid.intros(2), simp+)  

  1013 next

  1014   case (CreateSock p af st fd inum)

  1015   show ?thesis using grant

  1016     by (simp add:CreateSock)

  1017 next

  1018   case (Bind p fd addr)

  1019   show ?thesis using grant

  1020     by (simp add:Bind)

  1021 next

  1022   case (Connect p fd addr)

  1023   show ?thesis using grant

  1024     by (simp add:Connect)

  1025 next

  1026   case (Listen p fd)

  1027   show ?thesis using grant

  1028     by (simp add:Listen)

  1029 next

  1030   case (Accept p fd addr port fd' inum)

  1031   show ?thesis using grant

  1032     by (simp add:Accept)

  1033 next

  1034   case (SendSock p fd)

  1035   show ?thesis using grant

  1036     by (simp add:SendSock)

  1037 next

  1038   case (RecvSock p fd)

  1039   show ?thesis using grant

  1040     by (simp add:RecvSock)

  1041 next

  1042   case (Shutdown p fd how)

  1043   show ?thesis using grant

  1044     by (simp add:Shutdown)

  1045 qed