theory Tainted_prop 
imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop
begin

context tainting begin

lemma tainted_in_current:
  "obj \<in> tainted s \<Longrightarrow> alive s obj"
apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps)
apply (drule seeds_in_init, simp add:tobj_in_alive)
apply (erule has_same_inode_prop2, simp, simp add:vd_cons)
apply (frule vt_grant_os, simp)
apply (erule has_same_inode_prop1, simp, simp add:vd_cons)
done

lemma tainted_is_valid:
  "obj \<in> tainted s \<Longrightarrow> valid s"
by (erule tainted.induct, auto intro:valid.intros)

lemma t_remain_app:
  "\<lbrakk>obj \<in> tainted s; \<not> deleted obj (s' @ s); valid (s' @ s)\<rbrakk> 
  \<Longrightarrow> obj \<in> tainted (s' @ s)"
apply (induct s', simp)
apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain)
apply (simp_all add:not_deleted_cons_D vd_cons)
apply (drule tainted_in_current, simp add:not_deleted_imp_alive_cons)
done

lemma valid_tainted_obj:
  "obj \<in> tainted s \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h)"
apply (erule tainted.induct)
apply (drule seeds_in_init)
by auto

lemma dir_not_tainted: "O_dir f \<in> tainted s \<Longrightarrow> False"
by (auto dest:valid_tainted_obj)

lemma msgq_not_tainted: "O_msgq q \<in> tainted s \<Longrightarrow> False"
by (auto dest:valid_tainted_obj)

lemma shm_not_tainted: "O_shm h \<in> tainted s \<Longrightarrow> False"
by (auto dest:valid_tainted_obj)

end

end