(*<*)
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

(* 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)
thm co2sobj_other
apply (simp add:co2sobj_other)
apply (simp add:co2sobj.simps dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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 dalive_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_createsock s2ss_bind s2ss_connect s2ss_listen s2ss_accept s2ss_send 
  s2ss_recv s2ss_shutdown

end

end