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