# HG changeset patch
# User chunhan
# Date 1381905808 -28800
# Node ID 03d173288afeb86b326de51f3b56b5826b5a58c5
# Parent  89770d3c8a9b9cadcc4a32240d329d855388bd82
s2ss_prop2

diff -r 89770d3c8a9b -r 03d173288afe S2ss_prop2.thy
--- a/S2ss_prop2.thy	Wed Oct 16 13:38:31 2013 +0800
+++ b/S2ss_prop2.thy	Wed Oct 16 14:43:28 2013 +0800
@@ -332,12 +332,117 @@
 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