--- a/Dynamic2static.thy	Wed Oct 16 14:43:28 2013 +0800
+++ b/Dynamic2static.thy	Mon Oct 21 16:18:19 2013 +0800
@@ -1,39 +1,72 @@
 theory Dynamic2static
-imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop
+imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
 begin
 
 context tainting_s begin
 
+lemma many_sq_imp_sms:
+  "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm"
+sorry
+
+definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100)
+where
+  "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss"
+
+lemma [simp]: "ss \<doteq> ss"
+by (auto simp:init_ss_eq_def)
+
+definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101)
+where
+  "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'"
+
+lemma s2ss_included_sobj:
+  "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
+by (simp add:s2ss_def, rule_tac x = obj in exI, simp)
+
+lemma init_ss_in_prop:
+  "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk>
+   \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss"
+apply (simp add:init_ss_in_def init_ss_eq_def)
+apply (erule bexE, erule conjE)
+apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj)
+done
+
+
+
+
+
+
+lemma d2s_main_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) \<in> static"
+apply (frule vd_cons, frule vt_grant_os, clarsimp simp:s2ss_execve)
+sorry
+
 lemma d2s_main:
-  "valid s \<Longrightarrow> s2ss s \<in> static"
-apply (induct s, simp add:s2ss_nil_prop s_init)
-apply (frule vd_cons, simp)
-apply (case_tac a, simp_all) 
-(*
-apply 
-induct s, case tac e, every event analysis
-*)
-thm s2ss_def
+  "valid s \<Longrightarrow> s2ss s \<propto> static"
+apply (induct s, simp add:s2ss_nil_prop init_ss_in_def)
+apply (rule_tac x = "init_static_state" in bexI, simp, simp add:s_init)
+apply (frule vd_cons, frule vt_grant_os, simp)
+apply (case_tac a) 
+apply (clarsimp simp add:s2ss_execve)
+apply (rule conjI, rule impI)
+
 
 
 sorry
 
-lemma d2s_main':
-  "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
-by (simp add:s2ss_def, rule_tac x = obj in exI, simp)
 
 lemma tainted_has_sobj:
   "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj"
-sorry
+apply (frule tainted_in_current, case_tac obj)
+apply (auto dest:valid_tainted_obj simp:co2sobj.simps split:option.splits)
+oops
 
 lemma t2ts:
   "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"
 apply (frule tainted_in_current, frule tainted_is_valid)
-apply (simp add:s2ss_def)
+apply (frule d2s_main', simp)
 apply (case_tac sobj, simp_all)
-apply (case_tac [!] obj, simp_all split:option.splits if_splits)
-apply (rule_tac x = "O_proc nat" in exI, simp)
-apply (rule_tac x = "O_file list" in exI, simp)
+apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits)
 apply (drule dir_not_tainted, simp)
 apply (drule msgq_not_tainted, simp)
 apply (drule shm_not_tainted, simp)
@@ -44,6 +77,12 @@
 apply (induct s, simp)
 by (case_tac a, auto)
 
+lemma tainted_s_subset_prop:
+  "\<lbrakk>tainted_s ss sobj; ss \<subseteq> ss'\<rbrakk> \<Longrightarrow> tainted_s ss' sobj"
+apply (case_tac sobj)
+apply auto
+done
+
 theorem static_complete: 
   assumes undel: "undeletable obj" and tbl: "taintable obj"
   shows "taintable_s obj"
@@ -51,14 +90,15 @@
   from tbl obtain s where tainted: "obj \<in> tainted s"
     by (auto simp:taintable_def)
   hence vs: "valid s" by (simp add:tainted_is_valid)
-  hence static: "s2ss s \<in> static" using d2s_main by auto
-  from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj"
-    using vs tainted_has_sobj by blast
+  hence static: "s2ss s \<propto> static" using d2s_main by auto
+  from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" sorry 
+(* should constrain undeletable with file/dir/process only, while msg and fd are excluded 
+    using vs tainted_has_sobj by blast *)
   from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" 
     by (auto simp:undeletable_def)
   with vs sobj have "init_obj_related sobj obj"
     apply (case_tac obj, case_tac [!] sobj)
-    apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)
+    apply (auto split:option.splits if_splits simp:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)
     apply (frule not_deleted_init_file, simp+) 
     apply (drule is_file_has_sfile', simp, erule exE)
     apply (rule_tac x = sf in bexI)
@@ -75,10 +115,13 @@
     apply (drule file_dir_conflict, simp+)
     done
   with tainted t2ts init_alive sobj static
-  show ?thesis unfolding taintable_s_def
-    apply (rule_tac x = "s2ss s" in bexI, simp)
-    apply (rule_tac x = "sobj" in exI, auto)
-    done
+  show ?thesis unfolding taintable_s_def 
+    apply (simp add:init_ss_in_def)
+    apply (erule bexE)
+    apply (simp add:init_ss_eq_def)
+    apply (rule_tac x = "ss'" in bexI)
+    apply (rule_tac x = "sobj" in exI)
+    by (auto intro:tainted_s_subset_prop)
 qed
 
 lemma cp2sproc_pi:
@@ -117,17 +160,26 @@
 apply (rule notI)
 apply (clarsimp simp:s2ss_def)
 apply (case_tac obj, case_tac [!] obja, case_tac sobj)
-apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)
-apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def
+apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi simp:co2sobj.simps)
+apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def co2sobj.simps
            split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
 done
 
 lemma deleted_imp_deletable_s:
   "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"
 apply (simp add:deletable_s_def)
-apply (rule_tac x = "s2ss s" in bexI)
-apply (clarify, simp add:init_deled_imp_deled_s)
-apply (erule d2s_main)
+apply (frule d2s_main)
+apply (simp add:init_ss_in_def)
+apply (erule bexE)
+apply (rule_tac x = ss' in bexI)
+apply (auto simp add: init_ss_eq_def dest!:init_deled_imp_deled_s)
+apply (case_tac obj, case_tac [!] sobj)
+apply auto
+apply (erule set_mp)
+apply (simp)
+apply auto
+apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI)
+apply auto
 done
 
 theorem undeletable_s_complete:
@@ -141,9 +193,9 @@
   proof
     assume "\<exists> s. valid s \<and> deleted obj s"
     then obtain s where vs: "valid s" and del: "deleted obj s" by auto
-    from vs have vss: "s2ss s \<in> static" by (rule d2s_main) 
+    from vs have vss: "s2ss s \<propto> static" by (rule d2s_main) 
     with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" 
-      and related: "init_obj_related sobj obj" by auto
+      and related: "init_obj_related sobj obj" apply auto
     from init_alive del vs have "deletable_s obj" 
       by (auto elim:deleted_imp_deletable_s)
     with alive_s