1 theory source_prop

     2 imports Main rc_theory os_rc deleted_prop obj2sobj_prop

     3 begin

     4 

     5 context tainting_s_complete begin

     6 

     7 lemma all_sobjs_srp_init'[rule_format]:

     8   "sobj \<in> all_sobjs \<Longrightarrow> \<forall> sp srp. sobj = SProc sp (Some srp) \<longrightarrow> srp \<in> init_processes"

     9 apply (erule all_sobjs.induct, auto) 

    10 using init_proc_has_type 

    11 by (simp add:bidirect_in_init_def)

    12 

    13 lemma all_sobjs_srp_init:

    14   "SProc sp (Some srp) \<in> all_sobjs \<Longrightarrow> srp \<in> init_processes"

    15 by (auto dest!:all_sobjs_srp_init')

    16 

    17 (*

    18 lemma tainted_sproc_srp_init:

    19   "SProc sp (Some srp) \<in> tainted_s \<Longrightarrow> srp \<in> init_processes"

    20 by (auto dest:tainted_s_in_all_sobjs intro:all_sobjs_srp_init) *)

    21 

    22 lemma source_proc_of_init_remains:

    23   "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> source_proc s p = Some p"

    24 apply (induct s, simp)

    25 apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)

    26 apply (case_tac a, auto simp:np_notin_curp dest:not_deleted_imp_exists)

    27 done

    28 

    29 lemma init_proc_keeps_source:

    30   "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> 

    31    \<Longrightarrow> source_of_sobj (obj2sobj s (Proc p)) = Some (Proc p)"

    32 apply (frule not_deleted_imp_exists, simp, simp only:exists.simps)

    33 apply (frule current_proc_has_sproc, simp)

    34 apply (clarsimp split:option.splits simp:source_proc_of_init_remains)

    35 done

    36 

    37 lemma init_file_keeps_source:

    38   "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk> 

    39    \<Longrightarrow> source_of_sobj (obj2sobj s (File f)) = Some (File f)"

    40 apply (frule not_deleted_imp_exists, simp, simp only:exists.simps)

    41 apply (frule current_file_has_sfile, auto)

    42 done

    43 

    44 lemma init_ipc_keeps_source:

    45   "\<lbrakk>i \<in> init_ipcs; \<not> deleted (IPC i) s; valid s\<rbrakk> 

    46    \<Longrightarrow> source_of_sobj (obj2sobj s (IPC i)) = Some (IPC i)"

    47 apply (frule not_deleted_imp_exists, simp, simp only:exists.simps)

    48 apply (frule current_ipc_has_sipc, auto)

    49 done

    50  

    51 lemma init_obj_keeps_source: 

    52   "\<lbrakk>exists [] obj; \<not> deleted obj s; valid s\<rbrakk> \<Longrightarrow> source_of_sobj (obj2sobj s obj) = Some obj"

    53 apply (case_tac obj)

    54 by (auto intro:init_ipc_keeps_source init_proc_keeps_source init_file_keeps_source 

    55       simp del:obj2sobj.simps)

    56 

    57 end

    58 

    59 context tainting_s_sound begin

    60 

    61 lemma source_eq:

    62   "\<lbrakk>source_of_sobj sobj = Some obj; sobj_source_eq_obj sobj obj'\<rbrakk> \<Longrightarrow> obj = obj'"

    63 apply (case_tac obj, case_tac [!] sobj, case_tac [!] obj')

    64 by (auto split:option.splits)

    65 

    66 lemma proc_source_eq_prop:

    67   "\<lbrakk>obj2sobj s (Proc p) = SProc sp srp; p \<in> current_procs s;

    68     sobj_source_eq_obj (SProc sp srp) (Proc p); valid s\<rbrakk>

    69   \<Longrightarrow> srp = Some p"

    70 apply (frule current_proc_has_srp,auto split:option.splits)

    71 by (case_tac "source_proc s p", simp+)

    72 

    73 end

    74 

    75 end