# HG changeset patch
# User chunhan
# Date 1369876519 -28800
# Node ID 7b5e9fbeaf932ee1609277aa93a92f5b6e3e6f6e
# Parent  47a4b2ae0556de499e2ce9db5f9e3a5c7e178ea5
co2sobj simpset

diff -r 47a4b2ae0556 -r 7b5e9fbeaf93 Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Wed May 22 15:22:50 2013 +0800
+++ b/Co2sobj_prop.thy	Thu May 30 09:15:19 2013 +0800
@@ -616,15 +616,17 @@
 apply (rule set_eqI, rule iffI)
 apply (case_tac "x = a", simp)
 unfolding cpfd2sfds_def
-apply (erule CollectE, (erule conjE|erule exE)+)
-apply (simp split:if_splits)
-apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
-apply (case_tac "x = a", simp)
+apply (erule CollectE, (erule conjE|erule bexE)+)
+apply (simp add:proc_file_fds_def split:if_splits)
+apply (erule exE, rule_tac x = fda in exI)
+apply (simp add:cfd2sfd_open2)
+apply (case_tac "x = a", simp add:proc_file_fds_def)
 apply (rule_tac x = fd in exI, simp+)
-apply (erule conjE|erule exE)+
-apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
-apply (rule impI, drule proc_fd_in_fds, simp)
-apply (simp split:option.splits)
+apply (erule conjE|erule bexE)+
+apply (rule_tac x = fda in bexI)
+apply (simp add:proc_file_fds_def, erule exE)
+apply (simp add:cfd2sfd_open2)
+apply (simp add:proc_file_fds_def)
 done
 
 lemma cpfd2sfds_open1':
@@ -642,13 +644,12 @@
 apply (frule vt_grant_os, frule vd_cons)
 unfolding cpfd2sfds_def
 apply (rule set_eqI, rule iffI)
-apply (erule CollectE, (erule exE|erule conjE)+)
+apply (simp add:proc_file_fds_def)
+apply (erule exE|erule conjE)+
 apply (simp only:file_of_proc_fd.simps cfd2sfd_open2 split:if_splits)
-apply (rule CollectI)
-apply (rule_tac x = fda in exI, rule_tac x = fa in exI, simp)
-apply (erule CollectE, (erule exE|erule conjE)+)
-apply (simp only:file_of_proc_fd.simps split:if_splits)
-apply (rule CollectI)
+apply (rule_tac x = fda in exI, simp)
+apply (simp add:proc_file_fds_def)
+apply (erule exE|erule conjE)+
 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)
 done
 
@@ -665,14 +666,235 @@
 done
 
 lemma cpfd2sfds_execve:
-  "valid (Execve p fds # s) 
-   \<Longrightarrow> cpfd2sfds (Execve p fds # s)  = (cpfd2sfds s) (p := "
+  "valid (Execve p f fds # s) 
+   \<Longrightarrow> cpfd2sfds (Execve p f fds # s) = (cpfd2sfds s) (p := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext)
+apply (rule set_eqI, rule iffI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits)
+apply (frule_tac p' = p and fd' = fd in cfd2sfd_other, simp+)
+apply (rule_tac x = fd in bexI, simp+)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+apply (rule_tac x = fd in exI, simp)
+apply (simp split:if_splits)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+done
+
+lemma cpfd2sfds_clone:
+  "valid (Clone p p' fds shms # s) 
+   \<Longrightarrow> cpfd2sfds (Clone p p' fds shms # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext)
+apply (rule set_eqI, rule iffI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits)
+apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)
+apply (rule_tac x = fd in bexI, simp+)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)
+apply (rule_tac x = fd in exI, simp)
+apply (simp split:if_splits)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)
+done
 
 lemma cpfd2sfds_other:
   "\<lbrakk>valid (e # s);
-    \<forall> 
+    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p p'. e \<noteq> Kill p p';
+    \<forall> p. e \<noteq> Exit p;
+    \<forall> p fd. e \<noteq> CloseFd p fd;
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (case_tac e)
+using cfd2sfd_other
+by auto
+
+lemma cpfd2sfds_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> cpfd2sfds (Kill p p' # s) = (cpfd2sfds s) (p' := {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext, rule set_eqI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (rule iffI)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)
+apply (rule_tac x = fd in exI, simp)
+apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+done
+
+lemma cpfd2sfds_exit:
+  "valid (Exit p # s) \<Longrightarrow> cpfd2sfds (Exit p # s) = (cpfd2sfds s) (p := {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext, rule set_eqI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (rule iffI)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)
+apply (rule_tac x = fd in exI, simp)
+apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (rule_tac x = fd in exI, simp)
+apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)
+done
+
+lemma cpfd2sfds_closefd:
+  "valid (CloseFd p fd # s) \<Longrightarrow> cpfd2sfds (CloseFd p fd # s) = (cpfd2sfds s) (p := 
+     if (fd \<in> proc_file_fds s p)
+     then (case (cfd2sfd s p fd) of 
+             Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd)
+                          then cpfd2sfds s p else cpfd2sfds s p - {sfd})
+           | _        \<Rightarrow> cpfd2sfds s p)
+     else cpfd2sfds s p)"
+apply (frule vd_cons)
+apply (rule ext, rule set_eqI, rule iffI)
+unfolding cpfd2sfds_def proc_file_fds_def
+apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+
+apply (simp split:if_splits)
+apply (rule conjI, rule impI, rule conjI, rule impI, erule exE)
+apply (frule_tac p = p and fd = fd in current_filefd_has_sfd, simp)
+apply (erule exE, simp)
+apply (rule conjI, rule impI, (erule exE|erule conjE)+)
+apply (rule_tac x = fda in exI, simp, simp add:cfd2sfd_closefd)
+
+apply (rule impI, rule conjI)
+apply (rule_tac x = fda in exI, simp, simp add:cfd2sfd_closefd)
+apply (rule notI, simp)
+apply (erule_tac x = fda in allE, simp add:cfd2sfd_closefd)
+
+apply (rule impI, simp add:cpfd2sfds_def proc_file_fds_def)
+apply (erule exE, rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+
+apply (rule impI| rule conjI)+
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+
+apply (rule impI, simp add:cpfd2sfds_def proc_file_fds_def)
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
 
-lemma cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_other
+apply (simp split:if_splits)
+apply (frule_tac p = p and fd = fd in current_filefd_has_sfd, simp)
+apply (erule exE, simp)
+apply (case_tac "\<exists>fd'. fd' \<noteq> fd \<and> (\<exists>f'. file_of_proc_fd s p fd' = Some f') \<and> cfd2sfd s p fd' = Some sfd")
+apply simp
+apply (case_tac "xa = sfd")
+apply (erule exE|erule conjE)+
+apply (rule_tac x = fd' in exI, simp add:cfd2sfd_closefd)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+apply (rule notI, simp)
+apply (simp, (erule exE|erule conjE)+)
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+apply (rule notI, simp)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+apply (rule notI, simp)
+apply (simp add:cpfd2sfds_def proc_file_fds_def)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)
+done
+
+lemmas cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_execve cpfd2sfds_clone cpfd2sfds_kill cpfd2sfds_exit
+  cpfd2sfds_closefd cpfd2sfds_other
+
+(********* ch2sshm simpset ********)
+
+lemma ch2sshm_createshm:
+  "valid (CreateShM p h # s) 
+   \<Longrightarrow> ch2sshm (CreateShM p h # s) = (ch2sshm s) (h := 
+     (case (sectxt_of_obj (CreateShM p h # s) (O_shm h)) of
+                    Some sec \<Rightarrow> 
+ Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
+                  | _ \<Rightarrow> None))"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)
+done
+
+lemma ch2sshm_other:
+  "\<lbrakk>valid (e # s); 
+    \<forall> p h. e \<noteq> CreateShM p h; 
+    h' \<in> current_shms (e # s)\<rbrakk> \<Longrightarrow> ch2sshm (e # s) h' = ch2sshm s h'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac e)
+apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)
+done
+
+lemmas ch2sshm_simps = ch2sshm_createshm ch2sshm_other
+
+lemma current_shm_has_sh:
+  "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sh. ch2sshm s h = Some sh"
+by (auto simp:ch2sshm_def split:option.splits dest!:current_has_sec')
+
+lemma current_shm_has_sh':
+  "\<lbrakk>ch2sshm s h = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"
+by (auto dest:current_shm_has_sh)
+
+(********** cph2spshs simpset **********)
+
+  (*???*) 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
+
+definition
+  "fff x z = {xx. \<exists> y. xx = (x,y) \<and> (x, y) \<in> z}"
+thm fff_def
+
+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 cph2spshs_createshm:
+  "valid (Attach p h flag # s) \<Longrightarrow> 
+   cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := 
+     (case (ch2sshm s h) of 
+        Some sh \<Rightarrow> cph2spshs s p \<union> {(sh, flag)}
+      | _       \<Rightarrow> cph2spshs s p) )"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+unfolding cph2spshs_def
+using ch2sshm_other[where e = "Attach p h flag" and s = s]
+apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
+dest!:current_shm_has_sh'
+)
+thm current_shm_has_sshm
+apply (rule set_eqI, rule iffI)
+apply (case_tac xa, simp split:if_splits)
+apply (case_tac xa, erule CollectE)
+apply (simp, (erule conjE|erule bexE)+)
+apply (
+apply auto
+
+lemma cph2spshs_other:
+  "\<lbrakk>valid (e # s); "
+
+lemmas cph2spshs_simps = cph2spshs_other
 
 (******** cp2sproc simpset *********)
 
diff -r 47a4b2ae0556 -r 7b5e9fbeaf93 Flask.thy
--- a/Flask.thy	Wed May 22 15:22:50 2013 +0800
+++ b/Flask.thy	Thu May 30 09:15:19 2013 +0800
@@ -434,15 +434,19 @@
 | "procs_of_shm (Attach p h flag # \<tau>) = 
     (procs_of_shm \<tau>) (h := insert (p, flag) (procs_of_shm \<tau> h))"
 | "procs_of_shm (Detach p h # \<tau>) =
-    (procs_of_shm \<tau>) (h := (procs_of_shm \<tau> h) - {(p,flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"
+    (procs_of_shm \<tau>) (h := (procs_of_shm \<tau> h) - {(p,flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h})"
 | "procs_of_shm (DeleteShM p h # \<tau>) = (procs_of_shm \<tau>) (h := {})"
 | "procs_of_shm (Clone p p' fds shms # \<tau>) = 
     (\<lambda> h. if (h \<in> shms) 
-          then (procs_of_shm \<tau> h) \<union> {(p', flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h}
+          then (procs_of_shm \<tau> h) \<union> {(p', flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h}
           else procs_of_shm \<tau> h)"
 | "procs_of_shm (Execve p f fds # \<tau>) = 
-    (\<lambda> h. procs_of_shm \<tau> h - {(p, flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"
-| "procs_of_shm (e # \<tau>)          = procs_of_shm \<tau>"
+    (\<lambda> h. procs_of_shm \<tau> h - {(p, flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h})"
+| "procs_of_shm (Kill p p' # s) = 
+    (\<lambda> h. (procs_of_shm s h) - {(p', flag) | flag. (p', flag) \<in> procs_of_shm s h})"
+| "procs_of_shm (Exit p # s) = 
+    (\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})"
+| "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>"
 
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
@@ -765,6 +769,7 @@
 
 
 definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"
+where
   "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}"
 
 end
diff -r 47a4b2ae0556 -r 7b5e9fbeaf93 Init_prop.thy
--- a/Init_prop.thy	Wed May 22 15:22:50 2013 +0800
+++ b/Init_prop.thy	Thu May 30 09:15:19 2013 +0800
@@ -706,12 +706,14 @@
 
 lemma cpfd2sfds_nil_prop:
   "cpfd2sfds [] p = init_cfds2sfds p"
-apply (simp only:cpfd2sfds_def init_cfds2sfds_def)
+apply (simp only:cpfd2sfds_def init_cfds2sfds_def proc_file_fds_def init_proc_file_fds_def)
 apply (rule set_eqI, rule iffI)
-apply (drule CollectD, rule CollectI, (erule exE)+)
-apply (rule_tac x = fd in exI, rule_tac x = f in exI) defer
-apply (drule CollectD, rule CollectI, (erule exE)+)
-apply (rule_tac x = fd in exI, rule_tac x = f in exI)
+apply (drule CollectD, erule bexE, drule CollectD, erule exE)
+apply (rule CollectI, rule_tac x = fd in bexI) defer
+apply (rule CollectI, rule_tac x = f in exI, simp)
+apply (drule CollectD, erule bexE, drule CollectD, erule exE)
+apply (rule CollectI, rule_tac x = fd in bexI) defer
+apply (rule CollectI, rule_tac x = f in exI)
 using cfd2sfd_nil_prop 
 by auto