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 Alive_prop
begin

ML {*quick_and_dirty := true*}

context tainting begin

lemma valid_tainted_obj:
  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and>  (\<forall> p fd. obj \<noteq> O_fd p fd) \<and> (\<forall> s. obj \<noteq> O_tcp_sock s) \<and> (\<forall> s. obj \<noteq> O_udp_sock s)"
apply (induct s, simp)
apply (drule seeds_in_init, case_tac obj, simp+)
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto split:if_splits option.splits)
done

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

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

lemma tainted_in_current:
  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
apply (induct s, simp)
apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil)
apply (frule vd_cons, frule valid_tainted_obj, simp, frule vt_grant_os, case_tac a)
apply (auto simp:alive_simps split:if_splits option.splits t_object.splits intro:file_of_pfd_is_file)
done

lemma tainted_proc_in_current:
  "\<lbrakk>O_proc p \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
by (drule tainted_in_current, simp+)

lemma t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> 
             \<Longrightarrow> obj \<in> tainted (e # s)"
apply (frule vd_cons, frule vt_grant_os, case_tac e)
apply (auto simp:alive_simps split:option.splits if_splits)
done

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)
apply (simp add:vd_cons)
apply (simp add:not_deleted_imp_alive_cons)
done



end

end