(*<*)

theory S2ss_prop2

imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop S2ss_prop

begin

(*>*)

context tainting_s begin

definition unbackuped_sprocs :: "t_state \<Rightarrow> t_event \<Rightarrow> t_process set \<Rightarrow> t_sobject set"

where

  "unbackuped_sprocs s e procs \<equiv> 

    {sp | p sp. p \<in> procs \<and> co2sobj s (O_proc p) = Some sp \<and> 

                (\<forall> p' \<in> procs. co2sobj (e # s) (O_proc p') \<noteq> Some sp) \<and>

                (\<forall> p' \<in> (current_procs s - procs). co2sobj s (O_proc p') \<noteq> Some sp)}"

definition update_s2ss_procs :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_event \<Rightarrow> t_process set \<Rightarrow> t_static_state"

where

  "update_s2ss_procs s ss e procs \<equiv> 

     ss \<union> {sp | p sp. p \<in> procs \<and> co2sobj (e # s) (O_proc p) = Some sp}

        - unbackuped_sprocs s e procs"

 (* new sp after event may exists as same before the event in procs *)

lemma unbked_sps_D:

  "\<lbrakk>x \<in> unbackuped_sprocs s e procs; p \<in> procs\<rbrakk> \<Longrightarrow> co2sobj (e # s) (O_proc p) \<noteq> Some x"

by (auto simp add:unbackuped_sprocs_def)

lemma unbked_sps_D':

  "\<lbrakk>x \<in> unbackuped_sprocs s e procs; p \<notin> procs; p \<in> current_procs s; 

    co2sobj (e # s) (O_proc p) = co2sobj s (O_proc p)\<rbrakk>

   \<Longrightarrow> co2sobj (e # s) (O_proc p) \<noteq> Some x"

by (auto simp:unbackuped_sprocs_def)

lemma not_unbked_sps_D:

  "\<lbrakk>x \<notin> unbackuped_sprocs s e procs; p \<in> procs; co2sobj s (O_proc p) = Some x\<rbrakk> 

   \<Longrightarrow> (\<exists> p' \<in> procs. co2sobj (e # s) (O_proc p') = Some x) \<or>

       (\<exists> p' \<in> current_procs s - procs. co2sobj s (O_proc p') = Some x)"

by (auto simp:unbackuped_sprocs_def)

lemma unbked_sps_I:

  "\<lbrakk>co2sobj s obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> unbackuped_sprocs s' e procs"

apply (case_tac obj)

apply (auto simp add:unbackuped_sprocs_def co2sobj.simps split:option.splits)

done

lemma co2sobj_proc_deleteshm:

  "\<lbrakk>valid (DeleteShM p h # s); \<forall>flag. (pa, flag) \<notin> procs_of_shm s h; pa \<in> current_procs s\<rbrakk>

   \<Longrightarrow> co2sobj (DeleteShM p h # s) (O_proc pa) = co2sobj s (O_proc pa)"

thm co2sobj_deleteshm

apply (frule_tac obj = "O_proc pa" in co2sobj_deleteshm, simp)

apply (frule vd_cons, frule_tac p = pa in current_proc_has_sp, simp, erule exE)

apply (auto dest!:current_proc_has_sp' current_has_sec' current_shm_has_sh'

  split:t_object.splits option.splits if_splits dest:flag_of_proc_shm_prop1

  simp:co2sobj.simps tainted_eq_Tainted cp2sproc_deleteshm)

done

lemma s2ss_deleteshm:

  "valid (DeleteShM p h # s) \<Longrightarrow> s2ss (DeleteShM p h # s) = 

     (case ch2sshm s h of

        Some sh \<Rightarrow> del_s2ss_obj s 

                      (update_s2ss_procs s (s2ss s) (DeleteShM p h) {p'| p' flag. (p', flag) \<in> procs_of_shm s h})

                      (O_shm h) (S_shm sh)

      | _       \<Rightarrow> {})"

apply (frule vt_grant_os, frule vd_cons)

apply (case_tac "ch2sshm s h")

apply (drule current_shm_has_sh', simp, simp)

apply (simp add:del_s2ss_obj_def)

apply (tactic {*my_clarify_tac 1*})

unfolding update_s2ss_procs_def

apply (tactic {*my_seteq_tac 1*})

apply (erule_tac obj = obj in co2sobj_some_caseD)

apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h")

apply (erule exE, rule DiffI, rule UnI2, simp)

apply (rule_tac x = pa in exI, simp, rule_tac x = flag in exI, simp)

apply (rule notI, drule_tac p = pa in unbked_sps_D, simp)

apply (rule_tac x = flag in exI, simp, simp)

apply (rule DiffI, rule UnI1, simp)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm split:option.splits)

apply (simp add:cp2sproc_deleteshm split:option.splits if_splits)

apply (simp add:co2sobj.simps tainted_eq_Tainted)

apply (drule current_has_sec', simp, simp)

apply (simp add:co2sobj.simps tainted_eq_Tainted)

apply (drule flag_of_proc_shm_prop1, simp, simp)

apply (drule flag_of_proc_shm_prop1, simp, simp)

apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+)

apply (simp add:co2sobj_proc_deleteshm)

apply (simp add:co2sobj_proc_deleteshm)

apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps)

apply (erule unbked_sps_I, simp)

apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm)

apply (erule unbked_sps_I, simp)

apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps)

apply (erule unbked_sps_I, simp)

apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm)

apply (erule unbked_sps_I, simp)

apply (erule DiffE, erule UnE)

apply (tactic {*my_setiff_tac 1*})

apply (erule_tac obj = obj in co2sobj_some_caseD)

apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h", erule exE)

apply (drule_tac p = pa in not_unbked_sps_D, simp)

apply (rule_tac x = flag in exI, simp)

apply (simp, erule disjE, clarsimp)

apply (rule_tac x = "O_proc p'" in exI, simp add:procs_of_shm_prop2)

apply (erule bexE, simp, (erule conjE)+)

apply (frule_tac pa = p' in co2sobj_proc_deleteshm, simp+)

apply (rule_tac x = "O_proc p'" in exI, simp)

apply (frule_tac pa = pa in co2sobj_proc_deleteshm, simp+)

apply (rule_tac x = "O_proc pa" in exI, simp)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps)

apply (frule_tac co2sobj_sshm_imp, erule exE)

apply (case_tac "ha = h")

apply (rule_tac x = obj' in exI, simp add:co2sobj_deleteshm)

apply (simp add:co2sobj.simps)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm)

apply (tactic {*my_setiff_tac 1*}, clarsimp)

apply (rule_tac x = "O_proc pa" in exI, simp add:procs_of_shm_prop2)

apply (tactic {*my_clarify_tac 1*})

unfolding update_s2ss_procs_def

apply (tactic {*my_seteq_tac 1*})

apply (erule_tac obj = obj in co2sobj_some_caseD)

apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h")

apply (erule exE, rule DiffI, rule DiffI, rule UnI2, simp)

apply (rule_tac x = pa in exI, simp, rule_tac x = flag in exI, simp)

apply (rule notI, drule_tac p = pa in unbked_sps_D, simp)

apply (rule_tac x = flag in exI, simp, simp)

apply (rule notI, simp add:co2sobj.simps split:option.splits)

apply (rule DiffI, rule DiffI, rule UnI1, simp)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm split:option.splits)

apply (simp add:cp2sproc_deleteshm split:option.splits if_splits)

apply (simp add:co2sobj.simps tainted_eq_Tainted)

apply (drule current_has_sec', simp, simp)

apply (simp add:co2sobj.simps tainted_eq_Tainted)

apply (drule flag_of_proc_shm_prop1, simp, simp)

apply (drule flag_of_proc_shm_prop1, simp, simp)

apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+)

apply (simp add:co2sobj_proc_deleteshm)

apply (simp add:co2sobj_proc_deleteshm)

apply (rule notI, simp add:co2sobj.simps split:option.splits)

apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps)

apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps)

apply (case_tac "ha = h", simp)

apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm)

apply (erule unbked_sps_I, simp)

apply (rule notI, simp add:co2sobj_deleteshm, erule_tac x = "O_shm ha" in allE, simp)

apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps)

apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps split:option.splits)

apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm)

apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps split:option.splits)

apply (erule DiffE, erule DiffE, erule UnE)

apply (tactic {*my_setiff_tac 1*})

apply (erule_tac obj = obj in co2sobj_some_caseD)

apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h", erule exE)

apply (drule_tac p = pa in not_unbked_sps_D, simp)

apply (rule_tac x = flag in exI, simp)

apply (simp, erule disjE, clarsimp)

apply (rule_tac x = "O_proc p'" in exI, simp add:procs_of_shm_prop2)

apply (erule bexE, simp, (erule conjE)+)

apply (frule_tac pa = p' in co2sobj_proc_deleteshm, simp+)

apply (rule_tac x = "O_proc p'" in exI, simp)

apply (frule_tac pa = pa in co2sobj_proc_deleteshm, simp+)

apply (rule_tac x = "O_proc pa" in exI, simp)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps)

apply (case_tac "ha = h", simp add:co2sobj.simps)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps)

apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm)

apply (tactic {*my_setiff_tac 1*}, clarsimp)

apply (rule_tac x = "O_proc pa" in exI, simp add:procs_of_shm_prop2)

done

lemma s2ss_detach:

  "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = (

     case (cp2sproc s p, cp2sproc (Detach p h # s) p) of 

       (Some sp, Some sp') \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) 

           (S_proc sp (O_proc p \<in> Tainted s)) (S_proc sp' (O_proc p \<in> Tainted s))

     | _ \<Rightarrow> {} )"

apply (frule vd_cons, frule vt_grant_os)

apply (case_tac "cp2sproc s p")

apply (drule current_proc_has_sp', simp+)

apply (case_tac "cp2sproc (Detach p h # s) p")

apply (drule current_proc_has_sp', simp+)

apply (erule exE|erule conjE)+

apply (simp add:update_s2ss_obj_def)

apply (tactic {*my_clarify_tac 1*})

apply (tactic {*my_seteq_tac 1*})

apply (case_tac "obj = O_proc p")

apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)

apply (rule disjI2, simp, rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_detach, simp add:alive_simps)

apply (simp add:is_file_simps is_dir_simps split:t_object.splits)

apply (simp add:co2sobj.simps, simp add:co2sobj.simps)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)

apply (tactic {*my_setiff_tac 1*})

apply (case_tac "obj = O_proc p")

apply (rule_tac x = obj' in exI)

apply (frule_tac obj = obj' in co2sobj_detach, simp)

apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1]

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_detach)

apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1]

apply (tactic {*my_clarify_tac 1*})

apply (tactic {*my_seteq_tac 1*})

apply (case_tac "obj = O_proc p")

apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)

apply (rule disjI2, rule DiffI, simp, rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_detach, simp add:alive_simps)

apply (simp add:is_file_simps is_dir_simps split:t_object.splits)

apply (simp add:co2sobj.simps, simp add:co2sobj.simps)

apply (rule notI, simp, erule_tac x = obj in allE, erule impE, simp add:alive_simps, simp)

apply (frule_tac obj = obj in co2sobj_detach)

apply (simp add:alive_simps)

apply (simp split:t_object.splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)

apply (tactic {*my_setiff_tac 1*}, simp)

apply (case_tac "obj = O_proc p")

apply (simp add:co2sobj.simps tainted_eq_Tainted)

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_detach)

apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1]

done

definition attach_Tainted_procs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag \<Rightarrow> t_process set"

where

  "attach_Tainted_procs s p h flag \<equiv> 

     (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) 

      then {p''. \<exists> p' flag'. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p'' \<and> 

                                       O_proc p'' \<notin> Tainted s}

      else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)

           then {p'. info_flow_shm s p p' \<and> O_proc p' \<notin> Tainted s}

           else {})"

lemma attach_Tainted_procs_prop1:

  "valid s \<Longrightarrow> Tainted (Attach p h flag # s) = Tainted s \<union> {O_proc p' | p'. p' \<in> attach_Tainted_procs s p h flag}"

apply (auto simp:attach_Tainted_procs_def intro:info_flow_shm_Tainted)

done

lemma attach_Tainted_procs_prop2:

  "valid (Attach p h flag # s) \<Longrightarrow> {O_proc p'| p'. p' \<in> attach_Tainted_procs s p h flag} \<inter> Tainted s = {}"

by (auto simp:attach_Tainted_procs_def)

lemma attach_Tainted_procs_prop3:

  "\<lbrakk>p' \<in> attach_Tainted_procs s p h flag; valid s\<rbrakk> \<Longrightarrow> p' \<in> current_procs s"

by (auto simp:attach_Tainted_procs_def info_shm_flow_in_procs split:if_splits)

lemma co2sobj_attach':

  "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = 

     (case obj of 

        O_proc p' \<Rightarrow> if (p' = p) 

                     then (case cp2sproc (Attach p h flag # s) p of

                             Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> p \<in> attach_Tainted_procs s p h flag))

                           | _       \<Rightarrow> None)

                     else if (p' \<in> attach_Tainted_procs s p h flag)

                          then case cp2sproc s p' of 

                                 None \<Rightarrow> None

                               | Some sp \<Rightarrow> Some (S_proc sp True)

                          else co2sobj s obj

      | _         \<Rightarrow> co2sobj s obj)"

apply (frule vt_grant_os, frule vd_cons, case_tac obj)

apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted co2sobj.simps)

apply (frule current_proc_has_sp, simp, erule exE, (erule conjE)+)

apply (case_tac "cp2sproc (Attach p h flag # s) nat", drule current_proc_has_sp', simp+)

apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp+)

apply (simp add:tainted_eq_Tainted attach_Tainted_procs_prop1 del:Tainted.simps)

apply (simp add:cp2sproc_attach split:if_splits)

apply (auto split:if_splits option.splits dest!:current_file_has_sfile' 

             simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted

                  same_inode_files_prop6 

             dest:is_file_in_current is_dir_in_current)

done

lemma s2ss_attach:

  "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = 

     update_s2ss_procs s (s2ss s) (Attach p h flag) (attach_Tainted_procs s p h flag \<union> {p})"

apply (frule vt_grant_os, frule vd_cons)

apply (case_tac "cp2sproc s p", drule current_proc_has_sp', simp, simp)

apply (case_tac "ch2sshm s h", drule current_shm_has_sh', simp, simp)

apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp, simp)

unfolding update_s2ss_procs_def

apply (tactic {*my_seteq_tac 1*})

apply (erule_tac obj = obj in co2sobj_some_caseD)

apply (case_tac "pa = p")

apply (rule DiffI, rule UnI2, simp, rule_tac x = pa in exI, simp)

apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp)

apply (case_tac "pa \<in> attach_Tainted_procs s p h flag")

apply (rule DiffI, rule UnI2, simp)

apply (rule_tac x = pa in exI, simp)

apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp)

apply (rule DiffI, rule UnI1, simp)

apply (rule_tac x = obj in exI, simp add:co2sobj_attach')

apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+)

apply (simp add:co2sobj_attach')

apply (simp add:co2sobj_attach')

apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps)

apply (erule unbked_sps_I, simp)

apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach')

apply (erule unbked_sps_I, simp)

apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps)

apply (erule unbked_sps_I, simp)

apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach')

apply (erule unbked_sps_I, simp)

apply (erule DiffE, erule UnE)

apply (tactic {*my_setiff_tac 1*})

apply (erule_tac obj = obj in co2sobj_some_caseD)

apply (case_tac "pa \<in> attach_Tainted_procs s p h flag \<union> {p}")

apply (drule_tac p = pa in not_unbked_sps_D, simp, simp)

apply (erule disjE, erule bexE)

apply (rule_tac x = "O_proc p'" in exI, simp)

apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3)

apply (erule bexE, simp, (erule conjE)+)

apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_attach')

apply (rule_tac x = "O_proc pa" in exI, simp add:co2sobj_attach')

apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps)

apply (rule_tac x = obj in exI, simp add:co2sobj_attach')

apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps)

apply (rule_tac x = obj in exI, simp add:co2sobj_attach')

apply (tactic {*my_setiff_tac 1*}, clarsimp)

apply (rule_tac x = "O_proc pa" in exI, simp)

apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3)

done

(* should be modified when socket is model in static *)

lemma s2ss_createsock:

  "valid (CreateSock p af st fd inum # s) \<Longrightarrow> s2ss (CreateSock p af st fd inum # s) = s2ss s"

apply (simp add:s2ss_def)

apply (tactic {*my_seteq_tac 1*})

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_other)

apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_other)

apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

done

lemma s2ss_bind:

  "valid (Bind p fd addr # s) \<Longrightarrow> s2ss (Bind p fd addr # s) = s2ss s"

apply (simp add:s2ss_def)

apply (tactic {*my_seteq_tac 1*})

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_other)

apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_other)

apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

done

lemma s2ss_connect:

  "valid (Connect p fd addr # s) \<Longrightarrow> s2ss (Connect p fd addr # s) = s2ss s"

apply (simp add:s2ss_def)

apply (tactic {*my_seteq_tac 1*})

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_other)

apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_other)

apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

done

lemma s2ss_listen:

  "valid (Listen p fd # s) \<Longrightarrow> s2ss (Listen p fd # s) = s2ss s"

apply (simp add:s2ss_def)

apply (tactic {*my_seteq_tac 1*})

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_other)

apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_other)

apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

done

lemma s2ss_accept:

  "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> s2ss (Accept p fd addr port fd' inum # s) = s2ss s"

apply (simp add:s2ss_def)

apply (tactic {*my_seteq_tac 1*})

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_other)

apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_other)

apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

done

lemma s2ss_send:

  "valid (SendSock p fd # s) \<Longrightarrow> s2ss (SendSock p fd # s) = s2ss s"

apply (simp add:s2ss_def)

apply (tactic {*my_seteq_tac 1*})

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_other)

apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_other)

apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

done

lemma s2ss_recv:

  "valid (RecvSock p fd # s) \<Longrightarrow> s2ss (RecvSock p fd # s) = s2ss s"

apply (simp add:s2ss_def)

apply (tactic {*my_seteq_tac 1*})

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_other)

apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_other)

apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

done

lemma s2ss_shutdown:

  "valid (Shutdown p fd how # s) \<Longrightarrow> s2ss (Shutdown p fd how # s) = s2ss s"

apply (simp add:s2ss_def)

apply (tactic {*my_seteq_tac 1*})

apply (rule_tac x = obj in exI)

apply (simp add:co2sobj_other)

apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)

apply (tactic {*my_setiff_tac 1*})

apply (rule_tac x = obj in exI)

apply (frule_tac obj = obj in co2sobj_other)

apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)

done

lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open

  s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard

  s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg

  s2ss_createshm s2ss_detach s2ss_deleteshm s2ss_attach

  s2ss_createsock s2ss_bind s2ss_connect s2ss_listen s2ss_accept s2ss_send 

  s2ss_recv s2ss_shutdown

end

end