(*<*)
theory Current_prop
imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop
begin
(*>*)

context flask begin

lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
apply (induct s arbitrary:p_flag)
apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits)
done

lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
apply (induct s arbitrary:p flag)
apply (simp, drule init_procs_has_shm, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits)
done

lemma procs_of_shm_prop2':
  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<forall> flag h. (p, flag) \<notin> procs_of_shm s h"
by (auto dest:procs_of_shm_prop2)

lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>
  \<Longrightarrow> flag = flag'"
apply (induct s arbitrary:p flag flag')
apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
done

lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag"
apply (induct s arbitrary:p flag)
apply (simp, drule init_procs_has_shm, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
done

lemma procs_of_shm_prop4':
  "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"
by (auto dest:procs_of_shm_prop4)

lemma not_init_intro_proc:
  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
using not_deleted_init_proc by auto

lemma not_init_intro_proc':
  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
using not_deleted_init_proc by auto

lemma info_shm_flow_in_procs:
  "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)

(*********** simpset for info_flow_shm **************)

lemma info_flow_shm_attach:
  "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. 
     (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
     (pb = p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
     (info_flow_shm s pa pb)                       )"
apply (rule ext, rule ext, frule vt_grant_os)
by (auto simp add:info_flow_shm_def one_flow_shm_def)

lemma info_flow_shm_detach:
  "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. 
     self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or>
     (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"
apply (rule ext, rule ext, frule vt_grant_os)
by (auto simp:info_flow_shm_def one_flow_shm_def)

lemma info_flow_shm_deleteshm:
  "valid (DeleteShM p h # s) \<Longrightarrow> info_flow_shm (DeleteShM p h # s) = (\<lambda> pa pb. 
     self_shm s pa pb \<or> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)     )"
apply (rule ext, rule ext, frule vt_grant_os)
by (auto simp:info_flow_shm_def one_flow_shm_def)

lemma info_flow_shm_clone:
  "valid (Clone p p' fds shms # s) \<Longrightarrow> info_flow_shm (Clone p p' fds shms # s) = (\<lambda> pa pb. 
     (pa = p' \<and> pb = p') \<or> (pa = p' \<and> pb \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h p pb)) \<or> 
     (pb = p' \<and> pa \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h pa p)) \<or> 
     (pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
apply (frule_tac p = p' in procs_of_shm_prop2', simp)
apply (auto simp:info_flow_shm_def one_flow_shm_def)
done

lemma info_flow_shm_execve:
  "valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb. 
     (pa = p \<and> pb = p) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb)    )"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:info_flow_shm_def one_flow_shm_def)

lemma info_flow_shm_kill:
  "valid (Kill p p' # s) \<Longrightarrow> info_flow_shm (Kill p p' # s) = (\<lambda> pa pb. 
     pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb                 )"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:info_flow_shm_def one_flow_shm_def)

lemma info_flow_shm_exit:
  "valid (Exit p # s) \<Longrightarrow> info_flow_shm (Exit p # s) = (\<lambda> pa pb. 
     pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb                          )"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:info_flow_shm_def one_flow_shm_def)

lemma info_flow_shm_other:
  "\<lbrakk>valid (e # s); 
    \<forall> p h flag. e \<noteq> Attach p h flag;
    \<forall> p h. e \<noteq> Detach p h;
    \<forall> p h. e \<noteq> DeleteShM p h;
    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
    \<forall> p f fds. e \<noteq> Execve p f fds;
    \<forall> p p'. e \<noteq> Kill p p';
    \<forall> p. e \<noteq> Exit p
   \<rbrakk> \<Longrightarrow> info_flow_shm (e # s) = info_flow_shm s"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
apply (case_tac e, auto simp:info_flow_shm_def one_flow_shm_def dest:procs_of_shm_prop2)
apply (erule_tac x = h in allE, simp)
apply (drule procs_of_shm_prop1, auto)
done


(*
lemma info_flow_shm_prop1: 
  "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> 
   \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"
by (induct rule: info_flow_shm.induct, auto)

lemma info_flow_shm_cases:
  "\<lbrakk>info_flow_shm \<tau> pa pb; \<And>p s. \<lbrakk>s = \<tau> ; pa = p; pb = p; p \<in> current_procs s\<rbrakk> \<Longrightarrow> P;
  \<And>s p p' h p'' flag. \<lbrakk>s = \<tau>; pa = p; pb = p''; info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h;
                       (p'', flag) \<in> procs_of_shm s h\<rbrakk>\<Longrightarrow> P\<rbrakk>
  \<Longrightarrow> P"
by (erule info_flow_shm.cases, auto)

definition one_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
where
  "one_flow_shm s p p' \<equiv> p \<noteq> p' \<and> (\<exists> h flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h)"

inductive flows_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
where
  "p \<in> current_procs s \<Longrightarrow> flows_shm s p p"
| "\<lbrakk>flows_shm s p p'; one_flow_shm s p' p''\<rbrakk> \<Longrightarrow> flows_shm s p p''"

definition attached_procs :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
where
  "attached_procs s h \<equiv> {p. \<exists> flag. (p, flag) \<in> procs_of_shm s h}"

definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
where
  "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"

inductive flowed_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm set"

fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"
where
  "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"
| "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. 
     if (p' = p) then flowed_procs s h 
     else if ()
    "


lemma info_flow_shm_attach:
  "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or> 
     (if (pa = p) 
      then (if (flag = SHM_RDWR) 
            then (\<exists> flag. (pb, flag) \<in> procs_of_shm s h)
            else (pb = p)) 
      else (if (pb = p) 
            then (pa, SHM_RDWR) \<in> procs_of_shm s h
            else info_flow_shm s pa pb)) )"
apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
apply (case_tac "info_flow_shm s pa pb", simp)

thm info_flow_shm.cases
apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)
apply (erule info_flow_shm_cases, simp, simp split:if_splits)
apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)
apply (rule notI, erule info_flow_shm.cases, simp+)
pr 5
*)
lemmas info_flow_shm_simps = info_flow_shm_other info_flow_shm_attach info_flow_shm_detach info_flow_shm_deleteshm
  info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exit

lemma has_same_inode_in_current:
  "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
by (auto simp add:has_same_inode_def current_files_def)

lemma has_same_inode_prop1:
  "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
by (auto simp:has_same_inode_def is_file_def)

lemma has_same_inode_prop1':
  "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
by (auto simp:has_same_inode_def is_file_def)

lemma has_same_inode_prop2:
  "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
apply (drule has_same_inode_prop1)
apply (simp add:file_of_pfd_is_file, simp+)
done

lemma has_same_inode_prop2':
  "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
apply (drule has_same_inode_prop1')
apply (simp add:file_of_pfd_is_file, simp+)
done

lemma tobj_in_init_alive:
  "tobj_in_init obj \<Longrightarrow> init_alive obj"
by (case_tac obj, auto)

lemma tobj_in_alive:
  "tobj_in_init obj \<Longrightarrow> alive [] obj"
by (case_tac obj, auto simp:is_file_nil)

end

end