theory source_prop

imports Main rc_theory os_rc deleted_prop obj2sobj_prop

begin

context tainting_s_complete begin

lemma all_sobjs_srp_init'[rule_format]:

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

apply (erule all_sobjs.induct, auto) 

using init_proc_has_type 

by (simp add:bidirect_in_init_def)

lemma all_sobjs_srp_init:

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

by (auto dest!:all_sobjs_srp_init')

(*

lemma tainted_sproc_srp_init:

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

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

lemma source_proc_of_init_remains:

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

apply (induct s, simp)

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

apply (case_tac a, auto dest:not_deleted_imp_exists)

done

lemma init_proc_keeps_source:

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

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

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

apply (frule current_proc_has_sproc, simp)

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

done

lemma init_file_keeps_source:

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

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

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

apply (frule current_file_has_sfile, auto)

done

lemma init_ipc_keeps_source:

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

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

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

apply (frule current_ipc_has_sipc, auto)

done

lemma init_obj_keeps_source: 

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

apply (case_tac obj)

by (auto intro:init_ipc_keeps_source init_proc_keeps_source init_file_keeps_source 

      simp del:obj2sobj.simps)

end

context tainting_s_sound begin

lemma source_eq:

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

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

by (auto split:option.splits)

lemma proc_source_eq_prop:

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

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

  \<Longrightarrow> srp = Some p"

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

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

end

end