9 

    10 lemma current_proc_has_sp:

    11   "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sp. cp2sproc s p = Some sp"

    12 by (auto simp:cp2sproc_def split:option.splits dest!:current_has_sec')

    13 

    14 lemma current_proc_has_sp':

    15   "\<lbrakk>cp2sproc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"

    16 by (auto dest:current_proc_has_sp)

    17 

    18 lemma is_dir_has_sdir':

    19   "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

    20 apply (case_tac f)

    21 apply (rule_tac x = sroot in exI)

    22 apply (simp add:sroot_only)

    23 apply (drule is_dir_has_sfile, auto)

    24 done

    25 

    26 lemma is_file_has_sfile':

    27   "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

    28 by (drule is_file_has_sfile, auto)

    29 

    30 (* simpset for same_inode_files: Current_files_prop.thy *)

    31 

    32 lemma same_inode_files_nil:

    33   "same_inode_files [] = init_same_inode_files"

    34 by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil)

    35 

    36 lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>"

    37 by (auto simp add:current_inode_nums_def current_file_inums_def)

    38 

    39 lemma same_inode_files_open:

    40   "valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'.

    41      if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')"

    42 apply (frule vt_grant_os, frule vd_cons, rule ext)

    43 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits

    44             dest:iof's_im_in_cim iof's_im_in_cim')

    45 apply (drule is_file_in_current)

    46 apply (simp add:current_files_def)

    47 done

    48 

    49 lemma same_inode_files_linkhard:

    50   "valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'. 

    51      if (f' = f \<or> f' \<in> same_inode_files s oldf) 

    52      then same_inode_files s oldf \<union> {f}

    53      else same_inode_files s f')"

    54 apply (frule vt_grant_os, frule vd_cons, rule ext)

    55 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits

    56             dest:iof's_im_in_cim iof's_im_in_cim')

    57 apply (drule is_file_in_current)

    58 apply (simp add:current_files_def is_file_def)

    59 apply (simp add:is_file_def)

    60 done

    61 

    62 lemma inum_of_file_none_prop:

    63   "\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

    64 by (simp add:current_files_def)

    65 

    66 lemma same_inode_files_closefd:

    67   "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> 

    68    same_inode_files (CloseFd p fd # s) f' = (

    69      case (file_of_proc_fd s p fd) of 

    70        Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))

    71                  then same_inode_files s f' - {f}

    72                  else same_inode_files s f' )

    73      | None   \<Rightarrow> same_inode_files s f' )"

    74 apply (frule vt_grant_os, frule vd_cons)

    75 apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd 

    76            split:if_splits option.splits

    77             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)

    78 done

    79 

    80 lemma same_inode_files_unlink:

    81   "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> 

    82    \<Longrightarrow> same_inode_files (UnLink p f # s) f' = (

    83      if (proc_fd_of_file s f = {}) 

    84      then same_inode_files s f' - {f}

    85      else same_inode_files s f')"

    86 apply (frule vt_grant_os, frule vd_cons)

    87 apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink 

    88            split:if_splits option.splits

    89             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)

    90 done

    91 

    92 lemma same_inode_files_mkdir:

    93   "valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)"

    94 apply (frule vt_grant_os, frule vd_cons, rule ext)

    95 apply (auto simp:same_inode_files_def is_file_simps current_files_simps 

    96            split:if_splits option.splits

    97             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current)

    98 apply (simp add:current_files_def is_file_def)

    99 done

   100 

   101 lemma same_inode_files_other:

   102   "\<lbrakk>valid (e # s); 

   103     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   104     \<forall> p fd. e \<noteq> CloseFd p fd;

   105     \<forall> p f. e \<noteq> UnLink p f;

   106     \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s)  = same_inode_files s"

   107 apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e)

   108 apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def

   109            split:if_splits option.splits

   110             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir)

   111 apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+

   112 done

   113  

   114 lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard

   115   same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other

   116 

   117 lemma same_inode_files_prop1:

   118   "f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s"

   119 by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits)

   120 

   121 lemma same_inode_files_prop2:

   122   "\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''"

   123 by (auto dest:same_inode_files_prop1)

   124 

   125 lemma same_inode_files_prop3:

   126   "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"

   127 apply (rule notI)

   128 apply (simp add:same_inode_files_def is_file_def is_dir_def 

   129           split:if_splits option.splits t_inode_tag.splits)

   130 done

   131 

   132 (* simpset for cf2sfiles *)

   133 

   134 lemma cf2sfiles_open:

   135   "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>

   136    \<Longrightarrow> cf2sfiles (Open p f flag fd opt # s) f' = (

   137      if (f' = f \<and> opt \<noteq> None) 

   138      then (case cf2sfile (Open p f flag fd opt # s) f of 

   139              Some sf \<Rightarrow> {sf}  

   140            | _       \<Rightarrow> {} )

   141      else cf2sfiles s f')"

   142 apply (frule vt_grant_os, frule vd_cons)

   143 apply (auto simp:cf2sfiles_def cf2sfile_open_none cf2sfile_simps same_inode_files_open

   144   split:if_splits option.splits dest!:current_file_has_sfile' dest:cf2sfile_open)

   145 apply (rule_tac x = "f'a" in bexI, drule same_inode_files_prop1, simp add:cf2sfile_open_some1, simp)+

   146 done

   147 

   148 lemma cf2sfiles_other:

   149   "\<lbrakk>valid (e # s);

   150     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   151     \<forall> p fd. e \<noteq> CloseFd p fd;

   152     \<forall> p f. e \<noteq> UnLink p f;

   153     \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> cf2sfiles (e # s) = cf2sfiles s"

   154 apply (frule vt_grant_os, frule vd_cons, rule ext)

   155 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI)

   156 apply (drule Set.CollectD, erule bexE, rule CollectI)

   157 apply (rule_tac x = f' in bexI, case_tac e)

   158 apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps

   159   split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')

   160 apply (drule_tac f' = f' in cf2sfile_rmdir)

   161 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+

   162 

   163 apply (rule_tac x = f' in bexI, case_tac e)

   164 apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps

   165   split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')

   166 apply (drule_tac f' = f' in cf2sfile_rmdir)

   167 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+

   168 done

   169 

   170 lemma cf2sfiles_linkhard:

   171   "valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'. 

   172      if (f' = f \<or> f' \<in> same_inode_files s oldf)

   173      then (case (cf2sfile (LinkHard p oldf f # s) f) of

   174              Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf}

   175            | _       \<Rightarrow> {})

   176      else cf2sfiles s f')"

   177 apply (frule vt_grant_os, frule vd_cons, rule ext)

   178 apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps

   179   split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1)

   180 apply (simp add:cf2sfiles_def)

   181 

   182 lemma cf2sfiles_unlink:

   183 

   184 lemma cf2sfiles_closefd:

   185 

   186 lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other

   187   cf2sfiles_unlink cf2sfiles_closefd

   188   

   189 

   190 (* simpset for co2sobj *)

   191 

   192 lemma co2sobj_execve:

   193   "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (

   194       if (obj = O_proc p)

   195       then (case (cp2sproc (Execve p f fds # s) p) of

   196               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))

   197             | _       \<Rightarrow> None) 

   198       else co2sobj s obj )"

   199 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   200 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   201 apply (case_tac "cp2sproc (Execve p f fds # s) p")

   202 apply (drule current_proc_has_sp', simp, simp)

   203 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)

   204 

   205 apply (rule impI, simp add:cf2sfiles_def) defer

   206 

   207 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)

   208 apply (frule_tac ff = list in cf2sfile_other', simp_all)

   209 apply (simp add:is_dir_in_current)

   210 done

   211 

   212 end

   213