1 (*<*)

     2 theory Current_prop

     3 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop

     4 begin

     5 (*>*)

     6 

     7 context tainting begin

     8 

     9 (*

    10 lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"

    11 apply (induct s arbitrary:p_flag)

    12 apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)

    13 apply (frule vd_cons, frule vt_grant_os)

    14 apply (case_tac a, auto split:if_splits option.splits)

    15 done

    16 

    17 lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"

    18 apply (induct s arbitrary:p flag)

    19 apply (simp, drule init_procs_has_shm, simp)

    20 apply (frule vd_cons, frule vt_grant_os)

    21 apply (case_tac a, auto split:if_splits option.splits)

    22 done

    23 

    24 lemma procs_of_shm_prop2':

    25   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<forall> flag h. (p, flag) \<notin> procs_of_shm s h"

    26 by (auto dest:procs_of_shm_prop2)

    27 

    28 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>

    29   \<Longrightarrow> flag = flag'"

    30 apply (induct s arbitrary:p flag flag')

    31 apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)

    32 apply (frule vd_cons, frule vt_grant_os)

    33 apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)

    34 done

    35 

    36 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"

    37 apply (induct s arbitrary:p flag)

    38 apply (simp, drule init_procs_has_shm, simp)

    39 apply (frule vd_cons, frule vt_grant_os)

    40 apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)

    41 done

    42 

    43 lemma procs_of_shm_prop4':

    44   "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"

    45 by (auto dest:procs_of_shm_prop4)

    46 *)

    47 

    48 lemma not_init_intro_proc:

    49   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> died (O_proc p) s \<or> p \<notin> init_procs"

    50 using not_died_init_proc by auto

    51 

    52 lemma not_init_intro_proc':

    53   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> died (O_proc p) s \<and> p \<in> init_procs)"

    54 using not_died_init_proc by auto

    55 

    56 (*

    57 lemma info_shm_flow_in_procs:

    58   "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"

    59 by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)

    60 

    61 lemma flag_of_proc_shm_prop1:

    62   "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"

    63 apply (induct s arbitrary:p flag)

    64 apply (simp, drule init_shmflag_has_proc, simp)

    65 apply (frule vd_cons, frule vt_grant_os)

    66 apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)

    67 done

    68 *)

    69 

    70 lemma has_same_inode_in_current:

    71   "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"

    72 by (auto simp add:has_same_inode_def current_files_def same_inode_files_def 

    73   is_file_def split:if_splits option.splits)

    74 

    75 

    76 lemma has_same_inode_prop1:

    77   "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"

    78 by (auto simp:has_same_inode_def same_inode_files_def is_file_def)

    79 

    80 lemma has_same_inode_prop1':

    81   "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"

    82 by (auto simp:has_same_inode_def is_file_def same_inode_files_def 

    83  split:if_splits option.splits)

    84 

    85 lemma has_same_inode_prop2:

    86   "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"

    87 apply (drule has_same_inode_prop1)

    88 apply (simp add:file_of_pfd_is_file, simp+)

    89 done

    90 

    91 lemma has_same_inode_prop2':

    92   "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"

    93 apply (drule has_same_inode_prop1')

    94 apply (simp add:file_of_pfd_is_file, simp+)

    95 done

    96 

    97 lemma tobj_in_init_alive:

    98   "tobj_in_init obj \<Longrightarrow> init_alive obj"

    99 by (case_tac obj, auto)

   100 

   101 lemma tobj_in_alive:

   102   "tobj_in_init obj \<Longrightarrow> alive [] obj"

   103 by (case_tac obj, auto simp:is_file_nil)

   104 

   105 end

   106 

   107 end