(*<*)+
−
theory Co2sobj_prop+
−
imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop+
−
begin+
−
(*<*)+
−
+
−
context tainting_s begin+
−
+
−
(****************** cf2sfile path simpset ***************)+
−
+
−
thm cpfd2sfds_def+
−
+
−
lemma sroot_only:+
−
  "cf2sfile s [] = Some sroot"+
−
by (simp add:cf2sfile_def)+
−
+
−
lemma not_file_is_dir:+
−
  "\<lbrakk>\<not> is_file s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s f"+
−
by (auto simp:is_file_def current_files_def is_dir_def +
−
         dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)+
−
+
−
lemma not_dir_is_file:+
−
  "\<lbrakk>\<not> is_dir s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f"+
−
by (auto simp:is_file_def current_files_def is_dir_def +
−
         dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)+
−
+
−
lemma is_file_or_dir:+
−
  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f \<or> is_dir s f"+
−
by (auto dest:not_dir_is_file)+
−
+
−
lemma current_file_has_sfile:+
−
  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"+
−
apply (induct f)+
−
apply (rule_tac x = "sroot" in exI, simp add:sroot_only)+
−
apply (frule parentf_in_current', simp, clarsimp)+
−
apply (frule parentf_is_dir'', simp)+
−
apply (frule is_file_or_dir, simp)+
−
apply (auto dest!:current_has_sec'+
−
            simp:cf2sfile_def split:option.splits if_splits dest!:get_pfs_secs_prop')+
−
done+
−
+
−
definition sectxt_of_pf :: "t_state \<Rightarrow> t_file \<Rightarrow> security_context_t option"+
−
where+
−
  "sectxt_of_pf s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> sectxt_of_obj s (O_dir pf))"+
−
+
−
definition get_parentfs_ctxts' :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"+
−
where+
−
  "get_parentfs_ctxts' s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> get_parentfs_ctxts s pf)"+
−
+
−
lemma is_file_has_sfile:+
−
  "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec psec asecs. cf2sfile s f = Some +
−
      (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created,+
−
       sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_file f) = Some sec) \<and>+
−
       (sectxt_of_pf s f = Some psec) \<and> (get_parentfs_ctxts' s f = Some asecs)"+
−
apply (case_tac f, simp, drule root_is_dir', simp, simp)+
−
apply (frule is_file_in_current)+
−
apply (drule current_file_has_sfile, simp)+
−
apply (auto simp:cf2sfile_def sectxt_of_pf_def get_parentfs_ctxts'_def split:if_splits option.splits)+
−
done+
−
+
−
lemma is_dir_has_sfile:+
−
  "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> (case f of+
−
      [] \<Rightarrow> cf2sfile s f = Some sroot+
−
    | a # pf \<Rightarrow> (\<exists> sec psec asecs. cf2sfile s f = Some +
−
      (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created,+
−
       sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_dir f) = Some sec) \<and>+
−
       (sectxt_of_obj s (O_dir pf) = Some psec) \<and> (get_parentfs_ctxts s pf = Some asecs)))"+
−
apply (case_tac f, simp add:sroot_only)+
−
apply (frule is_dir_in_current, frule is_dir_not_file)+
−
apply (drule current_file_has_sfile, simp)+
−
apply (auto simp:cf2sfile_def split:if_splits option.splits)+
−
done+
−
+
−
lemma sroot_set:+
−
  "valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec"+
−
apply (frule root_is_dir)+
−
apply (drule is_dir_has_sec, simp)+
−
apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps +
−
                 root_type_remains root_user_remains+
−
           dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'+
−
           split:option.splits)+
−
done+
−
+
−
lemma cf2sfile_path_file:+
−
  "\<lbrakk>is_file s (f # pf); valid s\<rbrakk>+
−
   \<Longrightarrow> cf2sfile s (f # pf) = (+
−
     case (cf2sfile s pf) of+
−
       Some (pfi, pfsec, psec, asecs) \<Rightarrow> +
−
          (case (sectxt_of_obj s (O_file (f # pf))) of+
−
              Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)+
−
                                else Created, fsec, Some pfsec, asecs \<union> {pfsec})+
−
           | None \<Rightarrow> None)+
−
     | _ \<Rightarrow> None)"+
−
apply (frule is_file_in_current, drule parentf_is_dir'', simp)+
−
apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)+
−
apply (frule sroot_set)+
−
apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) +
−
done+
−
+
−
lemma cf2sfile_path_dir:+
−
  "\<lbrakk>is_dir s (f # pf); valid s\<rbrakk>+
−
   \<Longrightarrow> cf2sfile s (f # pf) = (+
−
     case (cf2sfile s pf) of+
−
       Some (pfi, pfsec, psec, asecs) \<Rightarrow> +
−
          (case (sectxt_of_obj s (O_dir (f # pf))) of+
−
              Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)+
−
                                else Created, fsec, Some pfsec, asecs \<union> {pfsec})+
−
           | None \<Rightarrow> None)+
−
     | _ \<Rightarrow> None)"+
−
apply (frule is_dir_in_current, drule parentf_is_dir'', simp)+
−
apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp)+
−
apply (frule_tac f = "pf" in is_dir_has_sfile, simp)+
−
apply (frule sroot_set)+
−
apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) +
−
done  +
−
+
−
lemma cf2sfile_path:+
−
  "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (+
−
     case (cf2sfile s pf) of+
−
       Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))+
−
         then (case (sectxt_of_obj s (O_file (f # pf))) of+
−
                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)+
−
                                   else Created, fsec, Some pfsec, asecs \<union> {pfsec})+
−
               | None \<Rightarrow> None)+
−
         else (case (sectxt_of_obj s (O_dir (f # pf))) of+
−
                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)+
−
                                   else Created, fsec, Some pfsec, asecs \<union> {pfsec})+
−
               | None \<Rightarrow> None)           )+
−
     | None \<Rightarrow> None)"+
−
apply (drule is_file_or_dir, simp)+
−
apply (erule disjE)+
−
apply (frule cf2sfile_path_file, simp) defer+
−
apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file)+
−
apply (auto split:option.splits)+
−
done+
−
+
−
lemma cf2sfile_path_file_prop1:+
−
  "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>+
−
   \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = +
−
                 Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)+
−
                       else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> +
−
               sectxt_of_obj s (O_file (f # pf)) = Some fsec"+
−
apply (frule is_file_has_sfile, simp)+
−
by (auto simp:cf2sfile_path_file)+
−
+
−
lemma cf2sfile_path_file_prop2:+
−
  "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); +
−
    sectxt_of_obj s (O_file (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = +
−
      Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)+
−
            else Created, fsec, Some pfsec, asecs \<union> {pfsec})"+
−
by (drule cf2sfile_path_file_prop1, auto)+
−
+
−
lemma cf2sfile_path_dir_prop1:+
−
  "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>+
−
   \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = +
−
                 Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)+
−
                       else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> +
−
               sectxt_of_obj s (O_dir (f # pf)) = Some fsec"+
−
apply (frule is_dir_has_sfile, simp)+
−
by (auto simp:cf2sfile_path_dir)+
−
+
−
lemma cf2sfile_path_dir_prop2:+
−
  "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); +
−
    sectxt_of_obj s (O_dir (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = +
−
      Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)+
−
            else Created, fsec, Some pfsec, asecs \<union> {pfsec})"+
−
by (drule cf2sfile_path_dir_prop1, auto)+
−
+
−
(**************** cf2sfile event list simpset ****************)+
−
+
−
lemma cf2sfile_open_none':+
−
  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f'= cf2sfile s f'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (induct f', simp add:cf2sfile_def)+
−
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps +
−
               get_parentfs_ctxts_simps)+
−
done+
−
+
−
lemma cf2sfile_open_none:+
−
  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s"+
−
apply (rule ext)+
−
by (simp add:cf2sfile_open_none')+
−
+
−
lemma cf2sfile_open_some1:+
−
  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)+
−
apply (case_tac "f = f'", simp)+
−
apply (induct f', simp add:sroot_only, simp)+
−
apply (frule parentf_in_current', simp+)+
−
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps +
−
               get_parentfs_ctxts_simps)+
−
done+
−
+
−
lemma cf2sfile_open_some2:+
−
  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, drule is_file_in_current)+
−
by (simp add:cf2sfile_open_some1)+
−
+
−
lemma cf2sfile_open_some3:+
−
  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, drule is_dir_in_current)+
−
by (simp add:cf2sfile_open_some1)+
−
+
−
lemma cf2sfile_open_some4:+
−
  "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f = (+
−
     case (parent f) of+
−
       Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), +
−
                         get_parentfs_ctxts s pf) of+
−
                    (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)+
−
                  | _ \<Rightarrow> None)+
−
     | None \<Rightarrow> None)"+
−
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)+
−
apply (case_tac f, simp)+
−
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps +
−
               get_parentfs_ctxts_simps)+
−
apply (rule impI, (erule conjE)+)+
−
apply (drule not_deleted_init_file, simp+)+
−
apply (simp add:is_file_in_current)+
−
done+
−
+
−
lemma cf2sfile_open:+
−
  "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' = (+
−
     if (opt = None) then cf2sfile s f'+
−
     else if (f' = f) +
−
     then (case (parent f) of+
−
             Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf), +
−
                 get_parentfs_ctxts s pf) of+
−
                          (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)+
−
                        | _ \<Rightarrow> None)+
−
           | None \<Rightarrow> None)+
−
     else cf2sfile s f')"+
−
apply (case_tac opt)+
−
apply (simp add:cf2sfile_open_none)+
−
apply (case_tac "f = f'")+
−
apply (simp add:cf2sfile_open_some4 split:option.splits)+
−
apply (simp add:cf2sfile_open_some1 current_files_simps)+
−
done+
−
+
−
lemma cf2sfile_mkdir1:+
−
  "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)+
−
apply (case_tac "f = f'", simp)+
−
apply (induct f', simp add:sroot_only, simp)+
−
apply (frule parentf_in_current', simp+)+
−
apply (case_tac "f = f'", simp)+
−
apply (simp add:cf2sfile_path is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps +
−
               get_parentfs_ctxts_simps split:if_splits option.splits)+
−
done+
−
+
−
lemma cf2sfile_mkdir2:+
−
  "\<lbrakk>valid (Mkdir p f i # s); is_file s f'\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, drule is_file_in_current)+
−
by (simp add:cf2sfile_mkdir1)+
−
+
−
lemma cf2sfile_mkdir3:+
−
  "\<lbrakk>valid (Mkdir p f i # s); is_dir s f'\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, drule is_dir_in_current)+
−
by (simp add:cf2sfile_mkdir1)+
−
+
−
lemma cf2sfile_mkdir4:+
−
  "valid (Mkdir p f i # s)+
−
  \<Longrightarrow> cf2sfile (Mkdir p f i # s) f = (case (parent f) of+
−
         Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), +
−
                           get_parentfs_ctxts s pf) of+
−
                      (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)+
−
                    | _ \<Rightarrow> None)+
−
       | None \<Rightarrow> None)"+
−
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)+
−
apply (case_tac f, simp)+
−
apply (clarsimp simp:os_grant.simps)+
−
apply (simp add:sectxt_of_obj_simps)+
−
apply (frule current_proc_has_sec, simp)+
−
apply (frule is_dir_has_sec, simp)+
−
apply (frule get_pfs_secs_prop, simp)+
−
apply (frule is_dir_not_file)+
−
apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps +
−
               get_parentfs_ctxts_simps split:option.splits if_splits +
−
            dest:not_deleted_init_dir is_dir_in_current not_deleted_init_file is_file_in_current)+
−
done+
−
+
−
lemma cf2sfile_mkdir:+
−
  "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files (Mkdir p f i # s)\<rbrakk>+
−
  \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = (+
−
    if (f' = f) +
−
    then (case (parent f) of+
−
             Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), +
−
                 get_parentfs_ctxts s pf) of+
−
                          (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)+
−
                        | _ \<Rightarrow> None)+
−
           | None \<Rightarrow> None)+
−
     else cf2sfile s f')"+
−
apply (case_tac "f = f'")+
−
apply (simp add:cf2sfile_mkdir4 split:option.splits)+
−
apply (simp add:cf2sfile_mkdir1 current_files_simps)+
−
done+
−
+
−
lemma cf2sfile_linkhard1:+
−
  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)+
−
apply (case_tac "f = f'", simp)+
−
apply (induct f', simp add:sroot_only, simp)+
−
apply (frule parentf_in_current', simp+)+
−
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps +
−
               get_parentfs_ctxts_simps split:if_splits option.splits)+
−
done+
−
+
−
lemma cf2sfile_linkhard2:+
−
  "\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, drule is_file_in_current)+
−
by (simp add:cf2sfile_linkhard1)+
−
+
−
lemma cf2sfile_linkhard3:+
−
  "\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, drule is_dir_in_current)+
−
by (simp add:cf2sfile_linkhard1)+
−
+
−
lemma cf2sfile_linkhard4:+
−
  "valid (LinkHard p oldf f # s)+
−
  \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of+
−
         Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), +
−
                           get_parentfs_ctxts s pf) of+
−
                      (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)+
−
                    | _ \<Rightarrow> None)+
−
       | None \<Rightarrow> None)"+
−
apply (frule vd_cons, frule vt_grant_os, frule noroot_events)+
−
apply (case_tac f, simp)+
−
apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps +
−
               get_parentfs_ctxts_simps)+
−
apply (rule impI, (erule conjE)+)+
−
apply (drule not_deleted_init_file, simp+)+
−
apply (simp add:is_file_in_current)+
−
done+
−
+
−
lemma cf2sfile_linkhard:+
−
  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk>+
−
  \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = (+
−
    if (f' = f) +
−
    then (case (parent f) of+
−
             Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), +
−
                 get_parentfs_ctxts s pf) of+
−
                          (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)+
−
                        | _ \<Rightarrow> None)+
−
           | None \<Rightarrow> None)+
−
     else cf2sfile s f')"+
−
apply (case_tac "f = f'")+
−
apply (simp add:cf2sfile_linkhard4 split:option.splits)+
−
apply (simp add:cf2sfile_linkhard1 current_files_simps)+
−
done+
−
+
−
lemma cf2sfile_other:+
−
  "\<lbrakk>ff \<in> current_files s;+
−
    \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;+
−
    \<forall> p fd. e \<noteq> CloseFd p fd;+
−
    \<forall> p f. e \<noteq> UnLink p f;+
−
    \<forall> p f. e \<noteq> Rmdir p f;+
−
    \<forall> p f i. e \<noteq> Mkdir p f i;+
−
    \<forall> p f f'. e \<noteq> LinkHard p f f'; +
−
    valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (induct ff, simp add:sroot_only)+
−
apply (frule parentf_in_current', simp+, case_tac e)+
−
apply (auto simp:current_files_simps is_file_simps is_dir_simps sectxt_of_obj_simps cf2sfile_path +
−
           split:if_splits option.splits)                     +
−
done     +
−
+
−
lemma cf2sfile_other':+
−
  "\<lbrakk>valid (e # s); +
−
    \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;+
−
    \<forall> p fd. e \<noteq> CloseFd p fd;+
−
    \<forall> p f. e \<noteq> UnLink p f;+
−
    \<forall> p f. e \<noteq> Rmdir p f;+
−
    \<forall> p f i. e \<noteq> Mkdir p f i;+
−
    \<forall> p f f'. e \<noteq> LinkHard p f f'; +
−
    ff \<in> current_files s\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"+
−
by (auto intro!:cf2sfile_other)+
−
  +
−
lemma cf2sfile_unlink:+
−
  "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (simp add:current_files_simps split:if_splits)+
−
apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps+
−
           split:if_splits option.splits)+
−
done+
−
+
−
lemma cf2sfile_rmdir:+
−
  "\<lbrakk>valid (Rmdir p f # s); f' \<in> current_files (Rmdir p f # s)\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (Rmdir p f # s) f' = cf2sfile s f'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (simp add:current_files_simps split:if_splits)+
−
apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps+
−
           split:if_splits option.splits)+
−
done+
−
+
−
lemma pfdof_simp5: "\<lbrakk>proc_fd_of_file s f = {(p, fd)}; file_of_proc_fd s p fd = None\<rbrakk> \<Longrightarrow> False"+
−
apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")+
−
by (simp add:pfdof_simp2, simp)+
−
+
−
lemma pfdof_simp6: "proc_fd_of_file s f = {(p, fd)} \<Longrightarrow> file_of_proc_fd s p fd = Some f"+
−
apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")+
−
by (simp add:pfdof_simp2, simp)+
−
+
−
lemma cf2sfile_closefd:+
−
  "\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (simp add:current_files_simps split:if_splits option.splits) +
−
(* costs too much time, but solved+
−
+
−
apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps +
−
           split:if_splits option.splits  +
−
            dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file+
−
                 not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file+
−
            dest!:current_has_sec')+
−
done+
−
*)+
−
sorry+
−
+
−
lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other+
−
  cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd+
−
  +
−
(*********** cfd2sfd simpset *********)+
−
+
−
lemma cfd2sfd_open1:+
−
  "valid (Open p f flags fd opt # s)+
−
   \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = +
−
     (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of+
−
        (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)+
−
      | _ \<Rightarrow> None)"+
−
by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits)+
−
+
−
lemma cfd2sfd_open_some2:+
−
  "\<lbrakk>valid (Open p f flags fd (Some inum) # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>+
−
  \<Longrightarrow> cfd2sfd (Open p f flags fd (Some inum) # s) p' fd' = cfd2sfd s p' fd'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (frule proc_fd_in_fds, simp)+
−
apply (frule file_of_proc_fd_in_curf, simp)+
−
apply (case_tac "f = f'", simp)+
−
apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_some1)+
−
apply (case_tac "p = p'", simp)+
−
apply (rule conjI, rule impI, simp)+
−
apply (drule cf2sfile_open_some1, simp)+
−
apply (auto split:option.splits)[1]+
−
apply simp+
−
apply (drule cf2sfile_open_some1, simp)+
−
apply (auto split:option.splits)[1]+
−
done+
−
+
−
lemma cfd2sfd_open_none2:+
−
  "\<lbrakk>valid (Open p f flags fd None # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>+
−
  \<Longrightarrow> cfd2sfd (Open p f flags fd None # s) p' fd' = cfd2sfd s p' fd'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (frule proc_fd_in_fds, simp)+
−
apply (frule file_of_proc_fd_in_curf, simp)+
−
apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_none)+
−
apply (case_tac "p = p'", simp)+
−
apply (rule conjI, rule impI, simp)+
−
apply (drule cf2sfile_open_none)+
−
apply (auto split:option.splits)[1]+
−
apply simp+
−
apply (drule cf2sfile_open_none)+
−
apply (auto split:option.splits)[1]+
−
done+
−
  +
−
lemma cfd2sfd_open2:+
−
  "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>+
−
  \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = cfd2sfd s p' fd'"+
−
apply (case_tac opt)+
−
apply (simp add:cfd2sfd_open_none2)+
−
apply (simp add:cfd2sfd_open_some2)+
−
done+
−
+
−
lemma cfd2sfd_open:+
−
  "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd (Open p f flags fd opt # s) p' fd' = Some f'\<rbrakk>+
−
   \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then +
−
     (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of+
−
        (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)+
−
      | _ \<Rightarrow> None)         else cfd2sfd s p' fd')"+
−
apply (simp split:if_splits)+
−
apply (simp add:cfd2sfd_open1 split:option.splits)+
−
apply (simp add:cfd2sfd_open2)+
−
apply (rule impI, simp)+
−
done+
−
+
−
lemma cfd2sfd_closefd:+
−
  "\<lbrakk>valid (CloseFd p fd # s); file_of_proc_fd (CloseFd p fd # s) p' fd' = Some f\<rbrakk>+
−
   \<Longrightarrow> cfd2sfd (CloseFd p fd # s) p' fd' = cfd2sfd  s p' fd'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (frule proc_fd_in_fds, simp)+
−
apply (frule file_of_proc_fd_in_curf, simp)+
−
apply (frule cf2sfile_closefd, simp)+
−
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)+
−
apply (auto split:option.splits if_splits)+
−
done+
−
+
−
lemma cfd2sfd_clone:+
−
  "\<lbrakk>valid (Clone p p' fds shms # s); file_of_proc_fd (Clone p p' fds shms # s) p'' fd' = Some f\<rbrakk>+
−
   \<Longrightarrow> cfd2sfd (Clone p p' fds shms # s) p'' fd' = (+
−
     if (p'' = p') then cfd2sfd s p fd'+
−
     else cfd2sfd s p'' fd')"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (frule proc_fd_in_fds, simp)+
−
apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)+
−
apply (frule_tac cf2sfile_other', simp+)+
−
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)+
−
apply (case_tac "p'' = p'", simp)+
−
apply (auto split:option.splits if_splits)[1]+
−
apply (simp)+
−
apply (auto split:option.splits if_splits)[1]+
−
done+
−
+
−
lemma cfd2sfd_execve:+
−
  "\<lbrakk>valid (Execve p f fds # s); file_of_proc_fd (Execve p f fds # s) p' fd' = Some f'\<rbrakk>+
−
   \<Longrightarrow> cfd2sfd (Execve p f fds # s) p' fd' = cfd2sfd s p' fd'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (frule proc_fd_in_fds, simp)+
−
apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)+
−
apply (frule_tac cf2sfile_other', simp+)+
−
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)+
−
apply (case_tac "p' = p", simp)+
−
apply (auto split:option.splits if_splits)[1]+
−
apply (simp)+
−
apply (auto split:option.splits if_splits)[1]+
−
done+
−
+
−
lemma cfd2sfd_kill:+
−
  "\<lbrakk>valid (Kill p p'' # s); file_of_proc_fd (Kill p p'' # s) p' fd' = Some f'\<rbrakk>+
−
   \<Longrightarrow> cfd2sfd (Kill p p'' # s) p' fd' = cfd2sfd s p' fd'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (frule proc_fd_in_fds, simp)+
−
apply (frule proc_fd_in_procs, simp)+
−
apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)+
−
apply (frule_tac cf2sfile_other', simp+)+
−
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)+
−
apply (auto split:option.splits if_splits)+
−
done+
−
+
−
lemma cfd2sfd_exit:+
−
  "\<lbrakk>valid (Exit p # s); file_of_proc_fd (Exit p # s) p' fd' = Some f'\<rbrakk>+
−
   \<Longrightarrow> cfd2sfd (Exit p # s) p' fd' = cfd2sfd s p' fd'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (frule proc_fd_in_fds, simp)+
−
apply (frule proc_fd_in_procs, simp)+
−
apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)+
−
apply (frule_tac cf2sfile_other', simp+)+
−
apply (simp add:cfd2sfd_def sectxt_of_obj_simps)+
−
apply (auto split:option.splits if_splits)+
−
done+
−
+
−
lemma cfd2sfd_other:+
−
  "\<lbrakk>valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f';+
−
    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;+
−
    \<forall> p p'' fds shms. e \<noteq> Clone p p'' fds shms\<rbrakk>+
−
   \<Longrightarrow> cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (frule proc_fd_in_fds, simp)+
−
apply (frule proc_fd_in_procs, simp)+
−
apply (frule file_of_proc_fd_in_curf, simp)+
−
apply (case_tac e)+
−
apply (auto intro!:cfd2sfd_execve cfd2sfd_closefd cfd2sfd_kill cfd2sfd_exit)+
−
apply (auto simp:cfd2sfd_def sectxt_of_obj_simps current_files_simps cf2sfile_simps split:option.splits)+
−
apply (auto dest!:current_has_sec' dest:file_of_proc_fd_in_curf proc_fd_in_fds)+
−
done+
−
+
−
lemmas cfd2sfd_simps = cfd2sfd_open cfd2sfd_clone cfd2sfd_other+
−
+
−
(********** cpfd2sfds simpset **********)+
−
+
−
lemma current_filefd_has_flags:+
−
  "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists> flags. flags_of_proc_fd s p fd = Some flags"+
−
apply (induct s arbitrary:p)+
−
apply (simp only:flags_of_proc_fd.simps file_of_proc_fd.simps init_filefd_prop4)+
−
apply (frule vd_cons, frule vt_grant_os, case_tac a)+
−
apply (auto split:if_splits option.splits dest:proc_fd_in_fds)+
−
done+
−
+
−
lemma current_filefd_has_flags':+
−
  "\<lbrakk>flags_of_proc_fd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"+
−
apply (case_tac "file_of_proc_fd s p fd")+
−
apply (simp, drule current_filefd_has_flags, simp+)+
−
done+
−
+
−
lemma current_file_has_sfile':+
−
  "\<lbrakk>cf2sfile s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"+
−
by (rule notI, drule current_file_has_sfile, simp+)+
−
+
−
lemma current_filefd_has_sfd:+
−
  "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists>sfd. cfd2sfd s p fd = Some sfd"+
−
by (auto simp:cfd2sfd_def split:option.splits dest!:current_has_sec' current_file_has_sfile' +
−
         dest:file_of_proc_fd_in_curf proc_fd_in_fds current_filefd_has_flags)+
−
+
−
lemma current_filefd_has_sfd':+
−
  "\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"+
−
by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd)+
−
+
−
lemma cpfd2sfds_open1:+
−
  "valid (Open p f flags fd opt # s) \<Longrightarrow>+
−
   cpfd2sfds (Open p f flags fd opt # s) p = (+
−
    case (cfd2sfd (Open p f flags fd opt # s) p fd) of+
−
        Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd}+
−
      | _ \<Rightarrow> cpfd2sfds s p)"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (split option.splits)+
−
apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp)+
−
apply (rule allI, rule impI)+
−
apply (rule set_eqI, rule iffI)+
−
apply (case_tac "x = a", simp)+
−
unfolding cpfd2sfds_def+
−
apply (erule CollectE, (erule conjE|erule bexE)+)+
−
apply (simp add:proc_file_fds_def split:if_splits)+
−
apply (erule exE, rule_tac x = fda in exI)+
−
apply (simp add:cfd2sfd_open2)+
−
apply (case_tac "x = a", simp add:proc_file_fds_def)+
−
apply (rule_tac x = fd in exI, simp+)+
−
apply (erule conjE|erule bexE)++
−
apply (rule_tac x = fda in bexI)+
−
apply (simp add:proc_file_fds_def, erule exE)+
−
apply (simp add:cfd2sfd_open2)+
−
apply (simp add:proc_file_fds_def)+
−
done+
−
+
−
lemma cpfd2sfds_open1':+
−
  "valid (Open p f flags fd opt # s) \<Longrightarrow>+
−
   cpfd2sfds (Open p f flags fd opt # s) p = (+
−
    case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of+
−
        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}+
−
      | _ \<Rightarrow> cpfd2sfds s p)"+
−
apply (frule cfd2sfd_open1)+
−
apply (auto dest:cpfd2sfds_open1 split:option.splits)+
−
done+
−
+
−
lemma cpfd2sfds_open2:+
−
  "\<lbrakk>valid (Open p f flags fd opt # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) p' = cpfd2sfds s p'"+
−
apply (frule vt_grant_os, frule vd_cons)+
−
unfolding cpfd2sfds_def+
−
apply (rule set_eqI, rule iffI)+
−
apply (simp add:proc_file_fds_def)+
−
apply (erule exE|erule conjE)++
−
apply (simp only:file_of_proc_fd.simps cfd2sfd_open2 split:if_splits)+
−
apply (rule_tac x = fda in exI, simp)+
−
apply (simp add:proc_file_fds_def)+
−
apply (erule exE|erule conjE)++
−
apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)+
−
done+
−
+
−
lemma cpfd2sfds_open:+
−
  "valid (Open p f flags fd opt # s)+
−
   \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := (+
−
    case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of+
−
        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}+
−
      | _ \<Rightarrow> cpfd2sfds s p))"+
−
apply (rule ext)+
−
apply (case_tac "x \<noteq> p")+
−
apply (simp add:cpfd2sfds_open2)+
−
apply (simp add:cpfd2sfds_open1')+
−
done+
−
+
−
lemma cpfd2sfds_execve:+
−
  "valid (Execve p f fds # s) +
−
   \<Longrightarrow> cpfd2sfds (Execve p f fds # s) = (cpfd2sfds s) (p := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (rule ext)+
−
apply (rule set_eqI, rule iffI)+
−
unfolding cpfd2sfds_def proc_file_fds_def+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (simp split:if_splits)+
−
apply (frule_tac p' = p and fd' = fd in cfd2sfd_other, simp+)+
−
apply (rule_tac x = fd in bexI, simp+)+
−
apply (simp add:cpfd2sfds_def proc_file_fds_def)+
−
apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)+
−
apply (rule_tac x = fd in exI, simp)+
−
apply (simp split:if_splits)+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (rule_tac x = fd in exI, simp)+
−
apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)+
−
apply (simp add:cpfd2sfds_def proc_file_fds_def)+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (rule_tac x = fd in exI, simp)+
−
apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)+
−
done+
−
+
−
lemma cpfd2sfds_clone:+
−
  "valid (Clone p p' fds shms # s) +
−
   \<Longrightarrow> cpfd2sfds (Clone p p' fds shms # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (rule ext)+
−
apply (rule set_eqI, rule iffI)+
−
unfolding cpfd2sfds_def proc_file_fds_def+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (simp split:if_splits)+
−
apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)+
−
apply (rule_tac x = fd in bexI, simp+)+
−
apply (simp add:cpfd2sfds_def proc_file_fds_def)+
−
apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)+
−
apply (rule_tac x = fd in exI, simp)+
−
apply (simp split:if_splits)+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (rule_tac x = fd in exI, simp)+
−
apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)+
−
apply (simp add:cpfd2sfds_def proc_file_fds_def)+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (rule_tac x = fd in exI, simp)+
−
apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)+
−
done+
−
+
−
lemma cpfd2sfds_other:+
−
  "\<lbrakk>valid (e # s);+
−
    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;+
−
    \<forall> p f fds. e \<noteq> Execve p f fds;+
−
    \<forall> p p'. e \<noteq> Kill p p';+
−
    \<forall> p. e \<noteq> Exit p;+
−
    \<forall> p fd. e \<noteq> CloseFd p fd;+
−
    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (rule ext)+
−
unfolding cpfd2sfds_def proc_file_fds_def+
−
apply (case_tac e)+
−
using cfd2sfd_other+
−
by auto+
−
+
−
lemma cpfd2sfds_kill:+
−
  "valid (Kill p p' # s) \<Longrightarrow> cpfd2sfds (Kill p p' # s) = (cpfd2sfds s) (p' := {})"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (rule ext, rule set_eqI)+
−
unfolding cpfd2sfds_def proc_file_fds_def+
−
apply (rule iffI)+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)+
−
apply (rule_tac x = fd in exI, simp)+
−
apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)+
−
apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (rule_tac x = fd in exI, simp)+
−
apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)+
−
done+
−
+
−
lemma cpfd2sfds_exit:+
−
  "valid (Exit p # s) \<Longrightarrow> cpfd2sfds (Exit p # s) = (cpfd2sfds s) (p := {})"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (rule ext, rule set_eqI)+
−
unfolding cpfd2sfds_def proc_file_fds_def+
−
apply (rule iffI)+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)+
−
apply (rule_tac x = fd in exI, simp)+
−
apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)+
−
apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (rule_tac x = fd in exI, simp)+
−
apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)+
−
done+
−
+
−
lemma cpfd2sfds_closefd:+
−
  "valid (CloseFd p fd # s) \<Longrightarrow> cpfd2sfds (CloseFd p fd # s) = (cpfd2sfds s) (p := +
−
     if (fd \<in> proc_file_fds s p)+
−
     then (case (cfd2sfd s p fd) of +
−
             Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd)+
−
                          then cpfd2sfds s p else cpfd2sfds s p - {sfd})+
−
           | _        \<Rightarrow> cpfd2sfds s p)+
−
     else cpfd2sfds s p)"+
−
apply (frule vd_cons)+
−
apply (rule ext, rule set_eqI, rule iffI)+
−
unfolding cpfd2sfds_def proc_file_fds_def+
−
apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)++
−
apply (simp split:if_splits)+
−
apply (rule conjI, rule impI, rule conjI, rule impI, erule exE)+
−
apply (frule_tac p = p and fd = fd in current_filefd_has_sfd, simp)+
−
apply (erule exE, simp)+
−
apply (rule conjI, rule impI, (erule exE|erule conjE)+)+
−
apply (rule_tac x = fda in exI, simp, simp add:cfd2sfd_closefd)+
−
+
−
apply (rule impI, rule conjI)+
−
apply (rule_tac x = fda in exI, simp, simp add:cfd2sfd_closefd)+
−
apply (rule notI, simp)+
−
apply (erule_tac x = fda in allE, simp add:cfd2sfd_closefd)+
−
+
−
apply (rule impI, simp add:cpfd2sfds_def proc_file_fds_def)+
−
apply (erule exE, rule_tac x = fda in exI, simp add:cfd2sfd_closefd)+
−
+
−
apply (rule impI| rule conjI)++
−
apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)+
−
+
−
apply (rule impI, simp add:cpfd2sfds_def proc_file_fds_def)+
−
apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)+
−
+
−
apply (simp split:if_splits)+
−
apply (frule_tac p = p and fd = fd in current_filefd_has_sfd, simp)+
−
apply (erule exE, simp)+
−
apply (case_tac "\<exists>fd'. fd' \<noteq> fd \<and> (\<exists>f'. file_of_proc_fd s p fd' = Some f') \<and> cfd2sfd s p fd' = Some sfd")+
−
apply simp+
−
apply (case_tac "xa = sfd")+
−
apply (erule exE|erule conjE)++
−
apply (rule_tac x = fd' in exI, simp add:cfd2sfd_closefd)+
−
apply (erule exE|erule conjE)++
−
apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)+
−
apply (rule notI, simp)+
−
apply (simp, (erule exE|erule conjE)+)+
−
apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)+
−
apply (rule notI, simp)+
−
apply (erule exE|erule conjE)++
−
apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)+
−
apply (rule notI, simp)+
−
apply (simp add:cpfd2sfds_def proc_file_fds_def)+
−
apply (erule exE|erule conjE)++
−
apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)+
−
done+
−
+
−
lemmas cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_execve cpfd2sfds_clone cpfd2sfds_kill cpfd2sfds_exit+
−
  cpfd2sfds_closefd cpfd2sfds_other+
−
+
−
(********* ch2sshm simpset ********)+
−
+
−
lemma ch2sshm_createshm:+
−
  "valid (CreateShM p h # s) +
−
   \<Longrightarrow> ch2sshm (CreateShM p h # s) = (ch2sshm s) (h := +
−
     (case (sectxt_of_obj (CreateShM p h # s) (O_shm h)) of+
−
                    Some sec \<Rightarrow> +
−
 Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)+
−
                  | _ \<Rightarrow> None))"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)+
−
done+
−
+
−
lemma ch2sshm_other:+
−
  "\<lbrakk>valid (e # s); +
−
    \<forall> p h. e \<noteq> CreateShM p h; +
−
    h' \<in> current_shms (e # s)\<rbrakk> \<Longrightarrow> ch2sshm (e # s) h' = ch2sshm s h'"+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (case_tac e)+
−
apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)+
−
done+
−
+
−
lemmas ch2sshm_simps = ch2sshm_createshm ch2sshm_other+
−
+
−
lemma current_shm_has_sh:+
−
  "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sh. ch2sshm s h = Some sh"+
−
by (auto simp:ch2sshm_def split:option.splits dest!:current_has_sec')+
−
+
−
lemma current_shm_has_sh':+
−
  "\<lbrakk>ch2sshm s h = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"+
−
by (auto dest:current_shm_has_sh)+
−
+
−
(********** cph2spshs simpset **********)+
−
+
−
  (*???*) lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"+
−
apply (induct s arbitrary:p_flag)+
−
apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (case_tac a, auto split:if_splits option.splits)+
−
done+
−
+
−
lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"+
−
apply (induct s arbitrary:p flag)+
−
apply (simp, drule init_procs_has_shm, simp)+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (case_tac a, auto split:if_splits option.splits)+
−
done+
−
+
−
lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>+
−
  \<Longrightarrow> flag = flag'"+
−
apply (induct s arbitrary:p flag flag')+
−
apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)+
−
done+
−
+
−
lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag"+
−
apply (induct s arbitrary:p flag)+
−
apply (simp, drule init_procs_has_shm, simp)+
−
apply (frule vd_cons, frule vt_grant_os)+
−
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)+
−
done+
−
+
−
lemma procs_of_shm_prop4':+
−
  "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"+
−
by (auto dest:procs_of_shm_prop4)+
−
+
−
lemma cph2spshs_attach:+
−
  "valid (Attach p h flag # s) \<Longrightarrow> +
−
   cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := +
−
     (case (ch2sshm s h) of +
−
        Some sh \<Rightarrow> cph2spshs s p \<union> {(sh, flag)}+
−
      | _       \<Rightarrow> cph2spshs s p) )"+
−
apply (frule vd_cons, frule vt_grant_os, rule ext)+
−
using ch2sshm_other[where e = "Attach p h flag" and s = s]+
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def)+
−
apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)+
−
apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)+
−
apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)+
−
apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)+
−
apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)+
−
apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp)+
−
apply (rule_tac x = ha in exI, simp)+
−
apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp)+
−
apply (rule_tac x = ha in exI, simp)+
−
apply (frule procs_of_shm_prop1, simp, simp)+
−
apply (rule impI, simp)+
−
done+
−
+
−
lemma cph2spshs_detach: "valid (Detach p h # s) \<Longrightarrow> +
−
  cph2spshs (Detach p h # s) = (cph2spshs s) (p := +
−
    (case (ch2sshm s h, flag_of_proc_shm s p h) of +
−
       (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)+
−
                  then cph2spshs s p else cph2spshs s p - {(sh, flag)}+
−
     | _       \<Rightarrow> cph2spshs s p)             )"+
−
apply (frule vd_cons, frule vt_grant_os, rule ext)+
−
apply (case_tac "x = p")  defer+
−
using ch2sshm_other[where e = "Detach p h" and s = s] +
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]+
−
apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp)+
−
apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp)+
−
apply (rule impI, simp)+
−
+
−
apply (clarsimp)+
−
apply (frule current_shm_has_sh, simp, erule exE)+
−
apply (frule procs_of_shm_prop4, simp, simp)+
−
apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)++
−
+
−
apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)+
−
apply (erule CollectE | erule exE| erule conjE| rule CollectI)++
−
apply (case_tac "ha = h", simp)+
−
apply (rule_tac x = sha in exI, rule_tac x = flaga in exI, rule_tac x = ha in exI, simp)+
−
using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
+
−
apply (erule CollectE | erule exE| erule conjE| rule CollectI)++
−
apply (case_tac "ha = h", simp)+
−
apply (rule_tac x = h' in exI, simp)+
−
apply (frule_tac flag = flag and flag' = flaga in procs_of_shm_prop3, simp+)+
−
apply (frule_tac flag = flaga in procs_of_shm_prop4, simp+)+
−
using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)+
−
apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
+
−
apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)++
−
apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)+
−
apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)++
−
apply (simp split:if_splits)+
−
apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
apply (rule notI, simp split:if_splits)+
−
apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)++
−
apply (simp split:if_splits)+
−
apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)+
−
apply (case_tac "ha = h", simp add:procs_of_shm_prop3, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
done+
−
+
−
lemma cph2spshs_deleteshm:+
−
  "valid (DeleteShM p h # s) \<Longrightarrow>     +
−
   cph2spshs (DeleteShM p h # s) = (\<lambda> p'. +
−
    (case (ch2sshm s h, flag_of_proc_shm s p' h) of +
−
       (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)+
−
                  then cph2spshs s p' else cph2spshs s p' - {(sh, flag)}+
−
     | _       \<Rightarrow> cph2spshs s p')   )"+
−
apply (frule vd_cons, frule vt_grant_os, rule ext)+
−
+
−
apply (clarsimp)+
−
apply (frule current_shm_has_sh, simp, erule exE, simp, simp split:option.splits)+
−
apply (rule conjI, rule impI)+
−
using ch2sshm_other[where e = "DeleteShM p h" and s = s] +
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]+
−
apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
apply (rule_tac x = ha in exI, simp)+
−
apply (case_tac "ha = h", simp+, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
+
−
apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)++
−
+
−
apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)+
−
apply (erule CollectE | erule exE| erule conjE| rule CollectI)++
−
apply (case_tac "ha = h", simp)+
−
apply (rule_tac x = sha in exI, rule_tac x = flag in exI, rule_tac x = ha in exI, simp)+
−
using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
+
−
apply (erule CollectE | erule exE| erule conjE| rule CollectI)++
−
apply (case_tac "ha = h", simp)+
−
apply (rule_tac x = h' in exI, simp)+
−
apply (frule_tac flag = flag in procs_of_shm_prop4, simp+)+
−
using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)+
−
apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
+
−
apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)++
−
apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)+
−
apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)++
−
apply (simp split:if_splits)+
−
apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
apply (rule notI, simp split:if_splits)+
−
apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)++
−
apply (simp split:if_splits)+
−
apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)+
−
apply (case_tac "ha = h", simp add:procs_of_shm_prop4)+
−
apply (frule_tac h = ha in procs_of_shm_prop1, simp+)+
−
using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)+
−
done+
−
+
−
lemma flag_of_proc_shm_prop1:+
−
  "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"+
−
apply (induct s arbitrary:p)+
−
apply (simp add:init_shmflag_has_proc)+
−
apply (frule vt_grant_os, frule vd_cons, case_tac a, auto split:if_splits option.splits)+
−
done+
−
+
−
lemma cph2spshs_clone:+
−
  "valid (Clone p p' fds shms # s) \<Longrightarrow> +
−
   cph2spshs (Clone p p' fds shms # s) = (cph2spshs s) (p' := +
−
     {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag} )"+
−
apply (frule vd_cons, frule vt_grant_os, rule ext)+
−
using ch2sshm_other[where e = "Clone p p' fds shms" and s = s]+
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)+
−
apply (erule_tac x = h in allE, frule procs_of_shm_prop1, simp, simp add:procs_of_shm_prop4)+
−
apply (rule_tac x = h in exI, simp, frule flag_of_proc_shm_prop1, simp+, simp add:procs_of_shm_prop1)+
−
apply (rule_tac x = h in exI, simp, frule procs_of_shm_prop1, simp+)++
−
done+
−
+
−
lemma cph2spshs_execve:+
−
  "valid (Execve p f fds # s) \<Longrightarrow>+
−
  cph2spshs (Execve p f fds # s) = (cph2spshs s) (p := {})"+
−
apply (frule vd_cons, frule vt_grant_os, rule ext)+
−
using ch2sshm_other[where e = "Execve p f fds" and s = s]+
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)+
−
apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)++
−
done+
−
+
−
lemma cph2spshs_kill:+
−
  "valid (Kill p p' # s) \<Longrightarrow> cph2spshs (Kill p p' # s) = (cph2spshs s) (p' := {})"+
−
apply (frule vd_cons, frule vt_grant_os, rule ext)+
−
using ch2sshm_other[where e = "Kill p p'" and s = s]+
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)+
−
apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)++
−
done+
−
+
−
lemma cph2spshs_exit:+
−
  "valid (Exit p # s) \<Longrightarrow> cph2spshs (Exit p # s) = (cph2spshs s) (p := {})"+
−
apply (frule vd_cons, frule vt_grant_os, rule ext)+
−
using ch2sshm_other[where e = "Exit p" and s = s]+
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)+
−
apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)++
−
done+
−
+
−
lemma cph2spshs_createshm:+
−
  "valid (CreateShM p h # s) \<Longrightarrow> cph2spshs (CreateShM p h # s) = cph2spshs s"+
−
apply (frule vt_grant_os, frule vd_cons, rule ext)+
−
apply (auto simp:cph2spshs_def)+
−
using ch2sshm_createshm+
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)+
−
apply (rule_tac x = ha in exI, auto simp:procs_of_shm_prop1)+
−
done+
−
+
−
lemma cph2spshs_other:+
−
  "\<lbrakk>valid (e # s); +
−
    \<forall> p h flag. e \<noteq> Attach p h flag;+
−
    \<forall> p h. e \<noteq> Detach p h;+
−
    \<forall> p h. e \<noteq> DeleteShM p h;+
−
    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;+
−
    \<forall> p f fds. e \<noteq> Execve p f fds;+
−
    \<forall> p p'. e \<noteq> Kill p p';+
−
    \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cph2spshs (e # s) = cph2spshs s"+
−
apply (frule vt_grant_os, frule vd_cons, rule ext)+
−
unfolding cph2spshs_def +
−
apply (rule set_eqI, rule iffI)+
−
apply (erule CollectE | erule conjE| erule exE| rule conjI| rule impI| rule CollectI)++
−
apply (frule procs_of_shm_prop1, simp, rule_tac x= sh in exI, rule_tac x = flag in exI, rule_tac x = h in exI)+
−
apply (case_tac e)+
−
using ch2sshm_other[where e = e and s = s] +
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3+
−
 simp:ch2sshm_createshm)+
−
apply (rule_tac x = h in exI, case_tac e)+
−
using ch2sshm_other[where e = e and s = s] +
−
apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits+
−
dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 +
−
 simp:ch2sshm_createshm)+
−
done+
−
+
−
lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve+
−
  cph2spshs_exit cph2spshs_kill cph2spshs_other+
−
+
−
(******** cp2sproc simpset *********)+
−
+
−
lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p"+
−
apply (simp add:cp2sproc_def)+
−
by (simp add:cp2sproc_def index_of_proc.simps)+
−
+
−
lemma cp2sproc_nil': "p \<in> current_procs [] \<Longrightarrow> cp2sproc [] p = SInit p"+
−
by (simp add:cp2sproc_nil current_procs.simps)+
−
+
−
lemma cp2sproc_clone: "cp2sproc (Clone p p' # \<tau>) p'' = (+
−
                         if (p'' = p') then SCrea (Suc (length \<tau>))+
−
                         else cp2sproc \<tau> p''           )"+
−
by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)+
−
+
−
lemma cp2sproc_other: "\<forall> p p'. e \<noteq> Clone p p' \<Longrightarrow> cp2sproc (e # \<tau>) p'' = cp2sproc \<tau> p''"+
−
apply (case_tac e)+
−
by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)+
−
+
−
lemmas cp2sproc_simps = cp2sproc_nil cp2sproc_nil' cp2sproc_clone cp2sproc_other+
−
+
−
(********************* cm2smsg simpset ***********************)+
−
+
−
lemma cm2smsg_nil: "m \<in> init_msgs \<Longrightarrow> cm2smsg [] m = SInit m"+
−
by (simp add:cm2smsg_def index_of_msg.simps)+
−
+
−
lemma cm2smsg_nil': "m \<in> current_msgs [] \<Longrightarrow> cm2smsg [] m = SInit m"+
−
by (simp add:cm2smsg_nil current_msgs.simps)+
−
+
−
lemma cm2smsg_createmsg: "cm2smsg (CreateMsg p m # \<tau>) m' = (if (m' = m) then SCrea (Suc (length \<tau>)) else cm2smsg \<tau> m')"+
−
by (simp add:cm2smsg_def index_of_msg.simps d2s_aux.simps)+
−
+
−
lemma cm2smsg_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'"+
−
apply (case_tac e)+
−
by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps)+
−
+
−
lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other+
−
+
−
+
−
+
−
end+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−