1 theory Info_flow_shm_prop

     2 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop Current_prop

     3 begin

     4 

     5 context flask begin

     6 

     7 (*********** simpset for one_flow_shm **************)

     8 

     9 lemma one_flow_not_self:

    10   "one_flow_shm s h p p \<Longrightarrow> False"

    11 by (simp add:one_flow_shm_def)

    12 

    13 lemma one_flow_shm_attach:

    14   "valid (Attach p h flag # s) \<Longrightarrow> one_flow_shm (Attach p h flag # s) = (\<lambda> h' pa pb. 

    15      if (h' = h) 

    16      then (pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>

    17           (pb = p \<and> pa \<noteq> p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>

    18           (one_flow_shm s h pa pb)               

    19      else one_flow_shm s h' pa pb        )"

    20 apply (rule ext, rule ext, rule ext, frule vd_cons, frule vt_grant_os)

    21 by (auto simp add: one_flow_shm_def)

    22 

    23 lemma one_flow_shm_detach:

    24   "valid (Detach p h # s) \<Longrightarrow> one_flow_shm (Detach p h # s) = (\<lambda> h' pa pb.

    25      if (h' = h) 

    26      then (pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h' pa pb)

    27      else one_flow_shm s h' pa pb)"

    28 apply (rule ext, rule ext, rule ext, frule vt_grant_os)

    29 by (auto simp:one_flow_shm_def)

    30 

    31 lemma one_flow_shm_deleteshm:

    32   "valid (DeleteShM p h # s) \<Longrightarrow> one_flow_shm (DeleteShM p h # s) = (\<lambda> h' pa pb. 

    33      if (h' = h) 

    34      then False

    35      else one_flow_shm s h' pa pb)"

    36 apply (rule ext, rule ext, rule ext, frule vt_grant_os)

    37 by (auto simp: one_flow_shm_def)

    38 

    39 lemma one_flow_shm_clone:

    40   "valid (Clone p p' fds shms # s) \<Longrightarrow> one_flow_shm (Clone p p' fds shms # s) = (\<lambda> h pa pb. 

    41      if (pa = p' \<and> pb \<noteq> p' \<and> h \<in> shms)

    42      then (if (pb = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h p pb)

    43      else if (pb = p' \<and> pa \<noteq> p' \<and> h \<in> shms)

    44           then (if (pa = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h pa p)

    45           else one_flow_shm s h pa pb)"

    46 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)

    47 apply (frule_tac p = p' in procs_of_shm_prop2', simp)

    48 apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)

    49 done

    50 

    51 lemma one_flow_shm_execve:

    52   "valid (Execve p f fds # s) \<Longrightarrow> one_flow_shm (Execve p f fds # s) = (\<lambda> h pa pb. 

    53      pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb    )"

    54 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)

    55 by (auto simp:one_flow_shm_def)

    56 

    57 lemma one_flow_shm_kill:

    58   "valid (Kill p p' # s) \<Longrightarrow> one_flow_shm (Kill p p' # s) = (\<lambda> h pa pb. 

    59      pa \<noteq> p' \<and> pb \<noteq> p' \<and> one_flow_shm s h pa pb                 )"

    60 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)

    61 by (auto simp:one_flow_shm_def)

    62 

    63 lemma one_flow_shm_exit:

    64   "valid (Exit p # s) \<Longrightarrow> one_flow_shm (Exit p # s) = (\<lambda> h pa pb. 

    65      pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb                          )"

    66 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)

    67 by (auto simp:one_flow_shm_def)

    68 

    69 lemma one_flow_shm_other:

    70   "\<lbrakk>valid (e # s); 

    71     \<forall> p h flag. e \<noteq> Attach p h flag;

    72     \<forall> p h. e \<noteq> Detach p h;

    73     \<forall> p h. e \<noteq> DeleteShM p h;

    74     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;

    75     \<forall> p f fds. e \<noteq> Execve p f fds;

    76     \<forall> p p'. e \<noteq> Kill p p';

    77     \<forall> p. e \<noteq> Exit p

    78    \<rbrakk> \<Longrightarrow> one_flow_shm (e # s) = one_flow_shm s"

    79 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)

    80 apply (case_tac e, auto simp:one_flow_shm_def dest:procs_of_shm_prop2)

    81 apply (drule procs_of_shm_prop1, auto)

    82 done

    83 

    84 lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm

    85   one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit

    86 

    87 type_synonym t_edge_shm = "t_process \<times> t_shm \<times> t_process"

    88 fun Fst:: "t_edge_shm \<Rightarrow> t_process" where "Fst (a, b, c) = a"

    89 fun Snd:: "t_edge_shm \<Rightarrow> t_shm" where "Snd (a, b, c) = b"

    90 fun Trd:: "t_edge_shm \<Rightarrow> t_process" where "Trd (a, b, c) = c"

    91 

    92 fun edge_related:: "t_edge_shm list \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> bool"

    93 where

    94   "edge_related [] p h = False"

    95 | "edge_related ((from, shm, to) # path) p h = 

    96      (if (((p = from) \<or> (p = to)) \<and> (h = shm)) then True 

    97       else edge_related path p h)"

    98          

    99 inductive path_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"

   100 where

   101   pbs1: "p \<in> current_procs s \<Longrightarrow> path_by_shm s p [] p"

   102 | pbs2: "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path)\<rbrakk> 

   103          \<Longrightarrow> path_by_shm s p ((p', h, p'')# path) p''"

   104 

   105 

   106 lemma one_step_path: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [(p, h, p')] p'"

   107 apply (rule_tac path = "[]" and p = p in path_by_shm.intros(2))

   108 apply (rule path_by_shm.intros(1))

   109 apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)

   110 done

   111 

   112 lemma pbs_prop1:

   113   "path_by_shm s p path p' \<Longrightarrow> ((path = []) = (p = p')) \<and> (path \<noteq> [] \<longrightarrow> p \<in> set (map Fst path))"

   114 apply (erule path_by_shm.induct, simp)

   115 apply (auto simp:one_flow_shm_def)

   116 done

   117 

   118 lemma pbs_prop2:

   119   "path_by_shm s p path p' \<Longrightarrow> (path = []) = (p = p')"

   120 by (simp add:pbs_prop1)

   121 

   122 lemma pbs_prop2':

   123   "path_by_shm s p path p \<Longrightarrow> path = []"

   124 by (simp add:pbs_prop2)

   125 

   126 lemma pbs_prop3:

   127   "\<lbrakk>path_by_shm s p path p'; path \<noteq> []\<rbrakk> \<Longrightarrow> p \<in> set (map Fst path)"

   128 by (drule pbs_prop1, auto)

   129 

   130 lemma pbs_prop4[rule_format]:

   131   "path_by_shm s p path p'\<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<in> set (map Trd path)"

   132 by (erule path_by_shm.induct, auto)

   133 

   134 lemma pbs_prop5[rule_format]:

   135   "path_by_shm s p path p' \<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<notin> set (map Fst path)"

   136 by (erule path_by_shm.induct, auto simp:one_flow_shm_def)

   137 

   138 lemma pbs_prop6_aux:

   139   "path_by_shm s pa pathac pc \<Longrightarrow> valid s \<longrightarrow> (\<forall> pb \<in> set (map Fst pathac). \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab)"

   140 apply (erule path_by_shm.induct)

   141 apply simp

   142 apply clarify

   143 apply (case_tac "pb = p'", simp)

   144 apply (rule_tac x = path in exI, simp)

   145 apply (erule one_step_path, simp)

   146 apply (erule_tac x = pb in ballE, simp_all, clarsimp)

   147 apply (rule_tac x = pathab in exI, simp)

   148 apply (erule pbs2, auto)

   149 done

   150 

   151 lemma pbs_prop6:

   152   "\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Fst pathac); valid s\<rbrakk>

   153    \<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"

   154 by (drule pbs_prop6_aux, auto)

   155 

   156 lemma pbs_prop7_aux:

   157   "path_by_shm s pa pathac pc \<Longrightarrow> valid s \<longrightarrow> (\<forall> pb \<in> set (map Trd pathac). \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab)"

   158 apply (erule path_by_shm.induct)

   159 apply simp

   160 apply clarify

   161 apply (case_tac "pb = p''", simp)

   162 apply (rule_tac x = "(p',h,p'') # path" in exI, simp)

   163 apply (rule conjI, erule pbs2, simp+)

   164 apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)

   165 apply (erule_tac x = pb in ballE, simp_all, clarsimp)

   166 apply (rule_tac x = pathab in exI, simp)

   167 apply (erule pbs2, auto)

   168 done

   169 

   170 lemma pbs_prop7:

   171   "\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Trd pathac); valid s\<rbrakk>

   172    \<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"

   173 by (drule pbs_prop7_aux, drule mp, simp, erule_tac x = pb in ballE, auto)

   174 

   175 lemma pbs_prop8:

   176   "path_by_shm s p path p' \<Longrightarrow> (set (map Fst path) - {p}) = (set (map Trd path) - {p'})"

   177 proof (induct rule:path_by_shm.induct)

   178   case (pbs1 p s)

   179   thus ?case by simp

   180 next

   181   case (pbs2 s p path p' h p'')

   182   assume p1:"path_by_shm s p path p'" and p2: "set (map Fst path) - {p} = set (map Trd path) - {p'}"

   183     and p3: "one_flow_shm s h p' p''" and p4: "p'' \<notin> set (map Fst path)" 

   184   show "set (map Fst ((p', h, p'') # path)) - {p} = set (map Trd ((p', h, p'') # path)) - {p''}"

   185     (is "?left = ?right")

   186   proof (cases "path = []")

   187     case True

   188     with p1 have "p = p'" by (drule_tac pbs_prop2, simp)

   189     thus ?thesis using True

   190       using p2 by (simp)

   191   next

   192     case False

   193     with p1 have a1: "p \<noteq> p'" by (drule_tac pbs_prop2, simp)

   194     from p3 have a2: "p' \<noteq> p''" by (simp add:one_flow_shm_def)

   195     from p1 False have a3: "p' \<in> set (map Trd path)" by (drule_tac pbs_prop4, simp+)

   196     from p4 p1 False have a4: "p \<noteq> p''" by (drule_tac pbs_prop3, auto)

   197     with p2 a2 p4 have a5: "p'' \<notin> set (map Trd path)" by auto

   198     

   199     have "?left = (set (map Fst path) - {p}) \<union> {p'}" using a1 by auto

   200     moreover have "... = (set (map Trd path) - {p'}) \<union> {p'}"  

   201       using p2 by auto

   202     moreover have "... = set (map Trd path)" using a3 by auto

   203     moreover have "... = set (map Trd path) - {p''}" using a5 by simp

   204     moreover have "... = ?right" by simp

   205     ultimately show ?thesis by simp

   206   qed

   207 qed

   208 

   209 lemma pbs_prop9_aux[rule_format]:

   210   "path_by_shm s p path p' \<Longrightarrow> h \<in> set (map Snd path) \<and> valid s \<longrightarrow> (\<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and> one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha))"

   211 apply (erule path_by_shm.induct, simp)

   212 apply (rule impI, case_tac "h \<in> set (map Snd path)", simp_all)

   213 apply (erule exE|erule conjE)+

   214 apply (rule_tac x = pa in exI, rule_tac x = pb in exI, rule_tac x = patha in exI, simp)

   215 apply (rule pbs2, auto)

   216 apply (rule_tac x = p' in exI, rule_tac x = p'' in exI, rule_tac x = path in exI, simp)

   217 apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)

   218 done

   219 

   220 lemma pbs_prop9:

   221   "\<lbrakk>h \<in> set (map Snd path); path_by_shm s p path p'; valid s\<rbrakk>

   222    \<Longrightarrow> \<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and> 

   223         one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha)"

   224 by (rule pbs_prop9_aux, auto)

   225 

   226 lemma path_by_shm_trans_aux[rule_format]:

   227   "path_by_shm s p' path' p'' \<Longrightarrow> valid s \<longrightarrow> (\<forall> p path. path_by_shm s p path p' \<longrightarrow> (\<exists> path''. path_by_shm s p path'' p''))"

   228 proof (induct rule:path_by_shm.induct)

   229   case (pbs1 p s)

   230   thus ?case

   231     by (clarify, rule_tac x = path in exI, simp)

   232 next

   233   case (pbs2 s p path p' h p'')

   234   hence p1: "path_by_shm s p path p'" and p2: "one_flow_shm s h p' p''" 

   235     and p3: "valid s \<longrightarrow> (\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p'))"

   236     and p4: "p'' \<notin> set (map Fst path)" by auto

   237   show ?case

   238   proof clarify

   239     fix pa path'

   240     assume p5: "path_by_shm s pa path' p" and p6: "valid s"

   241     with p3 obtain path'' where a1: "path_by_shm s pa path'' p'" by auto

   242     have p3': "\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p')" 

   243       using p3 p6 by simp

   244     show "\<exists>path''. path_by_shm s pa path'' p''"

   245     proof (cases "p'' \<in> set (map Fst path'')")

   246       case True

   247       then obtain res where "path_by_shm s pa res p''" using a1 pbs_prop6 p6 by blast

   248       thus ?thesis by auto

   249     next

   250       case False

   251       with p2 a1 show ?thesis 

   252         apply (rule_tac x = "(p', h, p'') # path''" in exI)

   253         apply (rule path_by_shm.intros(2), auto)

   254         done

   255     qed

   256   qed

   257 qed

   258 

   259 lemma path_by_shm_trans:

   260   "\<lbrakk>path_by_shm s p path p'; path_by_shm s p' path' p''; valid s\<rbrakk> \<Longrightarrow> \<exists> path''. path_by_shm s p path'' p''"

   261 by (drule_tac p' = p' and p'' = p'' in path_by_shm_trans_aux, auto)

   262 

   263 lemma path_by_shm_intro1_prop:

   264   "\<not> path_by_shm s p [] p \<Longrightarrow> p \<notin> current_procs s"

   265 by (auto dest:path_by_shm.intros(1))

   266 

   267 lemma path_by_shm_intro3:

   268   "\<lbrakk>path_by_shm s p path from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h; 

   269     to \<notin> set (map Fst path); from \<noteq> to\<rbrakk>

   270    \<Longrightarrow> path_by_shm s p ((from, h, to)#path) to"

   271 apply (rule path_by_shm.intros(2), simp_all)

   272 by (auto simp:one_flow_shm_def)

   273 

   274 lemma path_by_shm_intro4:

   275   "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [] p"

   276 by (drule procs_of_shm_prop2, simp, simp add:path_by_shm.intros(1))

   277 

   278 lemma path_by_shm_intro5:

   279   "\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk>

   280    \<Longrightarrow> path_by_shm s from [(from, h, to)] to"

   281 apply (rule_tac p' = "from" and h = h in path_by_shm.intros(2))

   282 apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)

   283 apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)

   284 done

   285 

   286 (* p'' \<notin> set (map Fst path): not duplicated target process;

   287  * p1 - ha \<rightarrow> p2; p2 - hb \<rightarrow> p3; p3 - ha \<rightarrow> p4; so path_by_shm p1 [(p3,ha,p4), (p2,hb,p3),(p1,ha,p2)] p4,

   288  * but this could be also path_by_shm p1 [(p1,ha,p4)] p4, so the former one is redundant!  *)

   289 

   290 inductive path_by_shm':: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"

   291 where

   292   pbs1': "p \<in> current_procs s \<Longrightarrow> path_by_shm' s p [] p"

   293 | pbs2': "\<lbrakk>path_by_shm' s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path); 

   294            h \<notin> set (map Snd path)\<rbrakk> 

   295           \<Longrightarrow> path_by_shm' s p ((p', h, p'')# path) p''"

   296 

   297 lemma pbs_prop10:

   298   "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; valid s\<rbrakk> \<Longrightarrow> \<exists>path'. path_by_shm s p path' p''"

   299 apply (case_tac "p'' \<in> set (map Fst path)")

   300 apply (drule_tac pb = p'' in pbs_prop6, simp+)

   301 apply ((erule exE|erule conjE)+, rule_tac x = pathab in exI, simp)

   302 apply (rule_tac x = "(p', h, p'') # path" in exI)

   303 apply (erule pbs2, simp+)

   304 done

   305 

   306 lemma pbs'_imp_pbs[rule_format]:

   307   "path_by_shm' s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm s p path' p')"

   308 apply (erule path_by_shm'.induct)

   309 apply (rule impI, rule_tac x = "[]" in exI, simp add:pbs1)

   310 apply (rule impI, clarsimp)

   311 apply (erule pbs_prop10, simp+)

   312 done

   313 

   314 lemma pbs_imp_pbs'[rule_format]:

   315   "path_by_shm s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm' s p path' p')"

   316 apply (erule path_by_shm.induct)

   317 apply (rule impI, rule_tac x = "[]" in exI, erule pbs1')

   318 apply (rule impI, simp, erule exE) (*

   319 apply ( erule exE, case_tac "h \<in> set (map Snd path)")

   320 apply (drule_tac s = s and p = p and p' = p' in pbs_prop9, simp+) defer

   321 apply (rule_tac x = "(p', h, p'') # path'" in exI)

   322 apply (erule pbs2', simp+) 

   323 apply ((erule exE|erule conjE)+)

   324 apply (rule_tac x = "(pa, h, p'') # patha" in exI)

   325 apply (erule pbs2', auto simp:one_flow_shm_def)

   326 done*)

   327 sorry

   328 

   329 

   330 lemma pbs'_eq_pbs:

   331   "valid s \<Longrightarrow> (\<exists> path'. path_by_shm' s p path' p') = (\<exists> path. path_by_shm s p path p')"

   332 by (rule iffI, auto intro:pbs_imp_pbs' pbs'_imp_pbs)

   333 

   334 definition flow_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

   335 where

   336   "flow_by_shm s p p' \<equiv> \<exists> path. path_by_shm s p path p'"

   337 

   338 lemma flow_by_shm_intro':

   339   "valid s \<Longrightarrow> flow_by_shm s p p' = (\<exists> path. path_by_shm' s p path p')"

   340 by (auto simp:flow_by_shm_def pbs'_eq_pbs)

   341 

   342 lemma one_step_flows: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p'"

   343 by (drule one_step_path, auto simp:flow_by_shm_def)

   344 

   345 lemma flow_by_shm_trans:

   346   "\<lbrakk>flow_by_shm s p p'; flow_by_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"

   347 by (auto simp:flow_by_shm_def intro!:path_by_shm_trans)

   348 

   349 lemma flow_by_shm_intro1_prop:

   350   "\<not> flow_by_shm s p p \<Longrightarrow> p \<notin> current_procs s"

   351 by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)

   352 

   353 lemma flow_by_shm_intro1:

   354   "p \<in> current_procs s \<Longrightarrow> flow_by_shm s p p"

   355 by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)

   356 

   357 lemma flow_by_shm_intro2:

   358   "\<lbrakk>flow_by_shm s p p'; one_flow_shm s h p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"

   359 by (auto intro:flow_by_shm_trans dest:one_step_flows)

   360 

   361 lemma flow_by_shm_intro3:

   362   "\<lbrakk>flow_by_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h; from \<noteq> to; valid s\<rbrakk>

   363    \<Longrightarrow> flow_by_shm s p to"

   364 apply (rule flow_by_shm_intro2)

   365 by (auto simp:one_flow_shm_def)

   366 

   367 lemma flow_by_shm_intro4:

   368   "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p"

   369 by (drule procs_of_shm_prop2, simp, simp add:flow_by_shm_intro1)

   370 

   371 lemma flow_by_shm_intro5:

   372   "\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk>

   373    \<Longrightarrow> flow_by_shm s from  to"

   374 apply (rule_tac p' = "from" and h = h in flow_by_shm_intro2)

   375 apply (rule flow_by_shm_intro1, simp add:procs_of_shm_prop2)

   376 apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)

   377 done

   378 

   379 lemma flow_by_shm_intro6:

   380   "path_by_shm s p path p' \<Longrightarrow> flow_by_shm s p p'"

   381 by (auto simp:flow_by_shm_def)

   382 

   383 (********* simpset for inductive Info_flow_shm **********)

   384 lemma path_by_shm_detach1_aux:

   385   "path_by_shm s' pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> (s' = Detach p h # s) 

   386      \<longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"

   387 apply (erule path_by_shm.induct, simp)

   388 apply (rule impI, rule path_by_shm.intros(1), simp+)

   389 by (auto simp:one_flow_shm_def split:if_splits intro:path_by_shm_intro3)

   390 

   391 lemma path_by_shm_detach1:

   392   "\<lbrakk>path_by_shm (Detach p h # s) pa path pb; valid (Detach p h # s)\<rbrakk> 

   393    \<Longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"

   394 by (auto dest:path_by_shm_detach1_aux)

   395 

   396 lemma path_by_shm_detach2_aux[rule_format]:

   397   "path_by_shm s pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> \<not> edge_related path p h 

   398    \<longrightarrow> path_by_shm (Detach p h # s) pa path pb"

   399 apply (induct rule:path_by_shm.induct)

   400 apply (rule impI, rule path_by_shm.intros(1), simp)

   401 apply (rule impI, erule conjE, simp split:if_splits)

   402 apply (rule path_by_shm.intros(2), simp)

   403 apply (simp add:one_flow_shm_detach)

   404 apply (rule impI, simp+)

   405 done

   406 

   407 lemma path_by_shm_detach2:

   408   "\<lbrakk>valid (Detach p h # s); \<not> edge_related path p h; path_by_shm s pa path pb\<rbrakk> 

   409    \<Longrightarrow> path_by_shm (Detach p h # s) pa path pb"

   410 by (auto intro!:path_by_shm_detach2_aux)

   411 

   412 lemma path_by_shm_detach:

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

   414    path_by_shm (Detach p h # s) pa path pb = (\<not> edge_related path p h  \<and> path_by_shm s pa path pb)"

   415 by (auto dest:path_by_shm_detach1 path_by_shm_detach2)

   416 

   417 lemma flow_by_shm_detach:

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

   419    flow_by_shm (Detach p h # s) pa pb = (\<exists> path. \<not> edge_related path p h \<and> path_by_shm s pa path pb)"

   420 by (auto dest:path_by_shm_detach simp:flow_by_shm_def)

   421 

   422 lemma path_by_shm'_attach1_aux:

   423   "path_by_shm' s' pa path pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>

   424      (path_by_shm' s pa path pb) \<or>

   425      (\<exists> path1 path2 p'. path_by_shm' s pa path1 p' \<and> path_by_shm' s p path2 pb \<and> 

   426          (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path = path2 @ [(p', h, p)] @ path1 ) \<or>

   427      (\<exists> path1 path2 p' flag'. path_by_shm' s pa path1 p \<and> path_by_shm' s p' path2 pb \<and> 

   428          (p', flag') \<in> procs_of_shm s h \<and> path = path2 @ [(p, h, p')] @ path1 \<and> flag = SHM_RDWR)"

   429 apply (erule path_by_shm'.induct)

   430 apply (simp, rule impI, rule pbs1', simp)

   431 apply (rule impI, erule impE, clarsimp)

   432 apply (erule disjE)

   433 apply (clarsimp simp:one_flow_shm_attach split:if_splits)

   434 apply (erule disjE, clarsimp)

   435 apply (erule_tac x = path in allE, clarsimp)

   436 apply (erule impE, rule pbs1', erule procs_of_shm_prop2, erule vd_cons, simp)

   437 apply (erule disjE, clarsimp)

   438 apply (rule_tac x = path in exI, rule_tac x = "[]" in exI, rule_tac x = p' in exI, simp)

   439 apply (rule pbs1', drule vt_grant_os, clarsimp)

   440 apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2', simp+)

   441 apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2', simp+)

   442 

   443 apply (erule disjE)

   444 apply ((erule exE|erule conjE)+, clarsimp split:if_splits simp:one_flow_shm_attach)

   445 apply (clarsimp simp:one_flow_shm_attach split:if_splits)

   446 apply (erule disjE, clarsimp)

   447 apply (clarsimp)

   448 

   449 

   450 apply (erule conjE)+

   451 

   452 

   453 

   454 apply (erule conjE, clarsimp simp only:one_flow_shm_attach split:if_splits)

   455 apply simp

   456 

   457 

   458 

   459 lemma path_by_shm_attach1_aux:

   460   "path_by_shm s' pa path pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> 

   461      path_by_shm s pa path pb \<or>

   462       (if (pa = p \<and> flag = SHM_RDWR)

   463        then \<exists> p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> 

   464                path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]

   465        else if (pb = p)

   466             then \<exists> p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> 

   467                    (p', SHM_RDWR) \<in> procs_of_shm s h

   468             else (\<exists> p' flag' patha pathb. path_by_shm s pa patha p \<and> flag = SHM_RDWR \<and> 

   469                    (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 

   470                    path = pathb @ [(p, h, p')] @ patha) \<or>

   471                  (\<exists> p' patha pathb. path_by_shm s pa patha p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> 

   472                    path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ patha))"

   473 proof (induct rule:path_by_shm.induct)

   474   case (pbs1 proc \<tau>)

   475   show ?case

   476   proof (rule impI)

   477     assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"

   478     from pbs1 pre have "proc \<in> current_procs s" by simp 

   479     thus "path_by_shm s proc [] proc \<or>

   480          (if proc = p \<and> flag = SHM_RDWR

   481           then \<exists>p' flagb path'.

   482                   (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' proc \<and> [] = path' @ [(p, h, p')]

   483           else if proc = p

   484                then \<exists>p' path'.

   485                        path_by_shm s proc path' p' \<and> [] = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h

   486                else (\<exists>p' flag' patha pathb.

   487                         path_by_shm s proc patha p \<and>

   488                         flag = SHM_RDWR \<and>

   489                         (p', flag') \<in> procs_of_shm s h \<and>

   490                         path_by_shm s p' pathb proc \<and> [] = pathb @ [(p, h, p')] @ patha) \<or>

   491                     (\<exists>p' patha pathb.

   492                         path_by_shm s proc patha p' \<and>

   493                         (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   494                         path_by_shm s p pathb proc \<and> [] = pathb @ [(p', h, p)] @ patha))"

   495       by (auto intro:path_by_shm.intros)

   496   qed

   497 next

   498   case (pbs2 \<tau> pa path pb h' pc)

   499   thus ?case

   500   proof (rule_tac impI)

   501     assume p1:"path_by_shm \<tau> pa path pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow>

   502      path_by_shm s pa path pb \<or>

   503      (if pa = p \<and> flag = SHM_RDWR

   504       then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]

   505       else if pb = p

   506            then \<exists>p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h

   507            else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> 

   508                     (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 

   509                     path = pathb @ [(p, h, p')] @ pathaa) \<or>

   510                 (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   511                     path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))"

   512       and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"

   513     

   514     from p2 and p4 have p2': "

   515       path_by_shm s pa path pb \<or>

   516      (if pa = p \<and> flag = SHM_RDWR

   517       then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]

   518       else if pb = p

   519            then \<exists>p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h

   520            else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> 

   521                     (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 

   522                     path = pathb @ [(p, h, p')] @ pathaa) \<or>

   523                 (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   524                     path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))"

   525       by (erule_tac impE, simp)

   526     from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)

   527     from p6 have "p \<in> current_procs s" by simp hence p7:"path_by_shm s p [] p" by (erule_tac path_by_shm.intros)

   528     from p3 p4 have p8: "if (h' = h) 

   529      then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>

   530           (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>

   531           (one_flow_shm s h pb pc)               

   532      else one_flow_shm s h' pb pc" by (auto simp add:one_flow_shm_attach) 

   533     

   534     

   535 (*

   536     have "\<And> flagb. (pc, flagb) \<in> procs_of_shm s h 

   537       \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' [] pc"

   538       apply (rule_tac x= pc in exI, rule_tac x = flagb in exI, frule procs_of_shm_prop2)

   539       by (simp add:p5, simp add:path_by_shm.intros(1))

   540     hence p10: "\<not> path_by_shm s p path pc \<Longrightarrow> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p'  pc) \<or>

   541       path_by_shm s pa pc"

   542       using p2' p7 p8 p5

   543       by (auto split:if_splits dest:path_by_shm.intros(2))      

   544   (*     apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+  *) *)

   545 

   546     from p1 have a0: "(path = []) = (pa = pb)" using pbs_prop2 by simp

   547     have a1:"\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pb\<rbrakk> \<Longrightarrow> 

   548       \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]"

   549       using p2' by auto

   550     have b1: "\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pc\<rbrakk> \<Longrightarrow> 

   551       \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pc \<and>

   552         (pb, h', pc) # path = path' @ [(p, h, p')]"

   553       

   554       

   555       using p8 a1 p7 p5 a0 

   556       apply (auto split:if_splits elim:path_by_shm_intro4)

   557       apply (rule_tac x = pb in exI, rule conjI, rule_tac x = SHM_RDWR in exI, simp)

   558       apply (rule_tac x = pc in exI, rule conjI, rule_tac x = flagb in exI, simp)

   559       apply (rule_tac x = "[]" in exI, rule conjI)

   560 apply (erule path_by_shm_intro4, simp)

   561 

   562       apply (case_tac "path_by_shm s pa path pb", simp) defer

   563       apply (drule a1, simp+, clarsimp)

   564       apply (rule conjI, rule_tac x = flagb in exI, simp)

   565       apply (rule path_by_shm_

   566       using p2' p8 p5

   567       apply (auto split:if_splits dest!:pbs_prop2' simp:path_by_shm_intro4)

   568       apply (drule pbs_prop2', simp)

   569       apply (erule_tac x = pc in allE, simp add:path_by_shm_intro4)

   570      

   571       apply (drule_tac x = "pc" in allE)

   572       

   573       apply simp

   574 

   575       sorry

   576     moreover have "pc = p \<Longrightarrow> (\<exists>p' path'. path_by_shm s pa path' p' \<and>

   577              (pb, h', pc) # path = path' @ [(p', h, p)] \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) \<or>

   578       (path_by_shm s pa path pc \<and> \<not> edge_related path p h)"

   579       using p2' p7 p8 p5

   580       sorry (*

   581       apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def) *)

   582     moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> 

   583       (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>

   584            path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p, h, p')] @ pathb) \<or>

   585       (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   586            path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p', h, p)] @ pathb) \<or>

   587       (path_by_shm s pa path pc \<and> \<not> edge_related path p h)"

   588       using p2' p7 p8 p5 (*

   589       apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def)

   590       apply (rule_tac x = pc in exI, simp add:path_by_shm_intro4)

   591       apply (rule_tac x = flagb in exI, simp)      

   592       done *)

   593       sorry

   594     ultimately  

   595     show "if (pb, h', pc) # path = [] then pa = pc \<and> pa \<in> current_procs s

   596        else path_by_shm s pa ((pb, h', pc) # path) pc \<and> \<not> edge_related ((pb, h', pc) # path) p h \<or>

   597        (if pa = p \<and> flag = SHM_RDWR

   598         then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and>

   599                 path_by_shm s p' path' pc \<and> (pb, h', pc) # path = path' @ [(p, h, p')]

   600         else if pc = p

   601              then \<exists>p' path'. path_by_shm s pa path' p' \<and>

   602                      (pb, h', pc) # path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h

   603              else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and>

   604                       (p', flag') \<in> procs_of_shm s h \<and>

   605                       path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathb @ [(p, h, p')] @ pathaa) \<or>

   606                   (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   607                       path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathb @ [(p', h, p)] @ pathaa))"

   608         apply (auto split:if_splits)

   609         using p7 by auto

   610   qed

   611 qed

   612 

   613 lemma path_by_shm_attach1:

   614   "\<lbrakk>valid (Attach p h flag # s); path_by_shm (Attach p h flag # s) pa pb\<rbrakk>

   615    \<Longrightarrow> (if path_by_shm s pa pb then True else

   616      (if (pa = p \<and> flag = SHM_RDWR) 

   617       then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)

   618       else if (pb = p) 

   619            then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')

   620            else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 

   621                              path_by_shm s p' pb) \<or>

   622                 (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb)

   623      )  )"

   624 apply (drule_tac p = p and h = h and flag = flag in path_by_shm_attach1_aux)

   625 by auto

   626 

   627 lemma path_by_shm_attach_aux[rule_format]:

   628   "path_by_shm s pa pb \<Longrightarrow> valid (Attach p h flag # s) \<longrightarrow> path_by_shm (Attach p h flag # s) pa pb"

   629 apply (erule path_by_shm.induct)

   630 apply (rule impI, rule path_by_shm.intros(1), simp)

   631 apply (rule impI, simp, rule_tac h = ha in path_by_shm.intros(2), simp)

   632 apply (auto simp add:one_flow_shm_simps)

   633 done

   634 

   635 lemma path_by_shm_attach2:

   636   "\<lbrakk>valid (Attach p h flag # s); if path_by_shm s pa pb then True else

   637      (if (pa = p \<and> flag = SHM_RDWR) 

   638       then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)

   639       else if (pb = p) 

   640            then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')

   641            else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 

   642                              path_by_shm s p' pb) \<or>

   643                 (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb))\<rbrakk>

   644    \<Longrightarrow> path_by_shm (Attach p h flag # s) pa pb"

   645 apply (frule vt_grant_os, frule vd_cons)

   646 apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def intro:path_by_shm_attach_aux)

   647 apply (rule_tac p' = p' in Info_flow_trans)

   648 apply (rule_tac p' = p and h = h in path_by_shm.intros(2))

   649 apply (rule path_by_shm.intros(1), simp)

   650 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)

   651 apply (rule conjI, rule notI, simp, rule_tac x = flagb in exI, simp)

   652 apply (simp add:path_by_shm_attach_aux)

   653 

   654 apply (rule_tac p' = p' in Info_flow_trans)

   655 apply (rule_tac p' = p in Info_flow_trans)

   656 apply (simp add:path_by_shm_attach_aux)

   657 apply (rule_tac p' = p and h = h in path_by_shm.intros(2))

   658 apply (rule path_by_shm.intros(1), simp)

   659 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)

   660 apply (rule conjI, rule notI, simp, rule_tac x = flag' in exI, simp)

   661 apply (simp add:path_by_shm_attach_aux)

   662 

   663 apply (rule_tac p' = p in Info_flow_trans)

   664 apply (rule_tac p' = p' in Info_flow_trans)

   665 apply (simp add:path_by_shm_attach_aux)

   666 apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))

   667 apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)

   668 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)

   669 apply (rule notI, simp)

   670 apply (simp add:path_by_shm_attach_aux)

   671 

   672 apply (rule_tac p' = p in Info_flow_trans)

   673 apply (rule_tac p' = p' in Info_flow_trans)

   674 apply (simp add:path_by_shm_attach_aux)

   675 apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))

   676 apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)

   677 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)

   678 apply (rule notI, simp)

   679 apply (simp add:path_by_shm_attach_aux)

   680 done

   681 

   682 lemma path_by_shm_attach:

   683   "valid (Attach p h flag # s) \<Longrightarrow> path_by_shm (Attach p h flag # s) = (\<lambda> pa pb. 

   684      path_by_shm s pa pb \<or>

   685      (if (pa = p \<and> flag = SHM_RDWR) 

   686       then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)

   687       else if (pb = p) 

   688            then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')

   689            else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 

   690                              path_by_shm s p' pb) \<or>

   691                 (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb)

   692      )  )"

   693 apply (rule ext, rule ext, rule iffI)

   694 apply (drule_tac pa = pa and pb = pb in path_by_shm_attach1, simp)

   695 apply (auto split:if_splits)[1]

   696 apply (drule_tac pa = pa and pb = pb in path_by_shm_attach2)

   697 apply (auto split:if_splits)

   698 done

   699 

   700 

   701 

   702 lemma info_flow_shm_detach:

   703   "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. 

   704      self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or>

   705      (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"

   706 apply (rule ext, rule ext, frule vt_grant_os)

   707 by (auto simp:info_flow_shm_def one_flow_shm_def)

   708 

   709 lemma info_flow_shm_deleteshm:

   710   "valid (DeleteShM p h # s) \<Longrightarrow> info_flow_shm (DeleteShM p h # s) = (\<lambda> pa pb. 

   711      self_shm s pa pb \<or> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)     )"

   712 apply (rule ext, rule ext, frule vt_grant_os)

   713 by (auto simp:info_flow_shm_def one_flow_shm_def)

   714 

   715 lemma info_flow_shm_clone:

   716   "valid (Clone p p' fds shms # s) \<Longrightarrow> info_flow_shm (Clone p p' fds shms # s) = (\<lambda> pa pb. 

   717      (pa = p' \<and> pb = p') \<or> (pa = p' \<and> pb \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h p pb)) \<or> 

   718      (pb = p' \<and> pa \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h pa p)) \<or> 

   719      (pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"

   720 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)

   721 apply (frule_tac p = p' in procs_of_shm_prop2', simp)

   722 sorry (*

   723 apply (auto simp:info_flow_shm_def one_flow_shm_def)

   724 done *)

   725 

   726 lemma info_flow_shm_execve:

   727   "valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb. 

   728      (pa = p \<and> pb = p) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb)    )"

   729 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)

   730 by (auto simp:info_flow_shm_def one_flow_shm_def)

   731 

   732 lemma info_flow_shm_kill:

   733   "valid (Kill p p' # s) \<Longrightarrow> info_flow_shm (Kill p p' # s) = (\<lambda> pa pb. 

   734      pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb                 )"

   735 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)

   736 by (auto simp:info_flow_shm_def one_flow_shm_def)

   737 

   738 lemma info_flow_shm_exit:

   739   "valid (Exit p # s) \<Longrightarrow> info_flow_shm (Exit p # s) = (\<lambda> pa pb. 

   740      pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb                          )"

   741 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)

   742 by (auto simp:info_flow_shm_def one_flow_shm_def)

   743 

   744 lemma info_flow_shm_other:

   745   "\<lbrakk>valid (e # s); 

   746     \<forall> p h flag. e \<noteq> Attach p h flag;

   747     \<forall> p h. e \<noteq> Detach p h;

   748     \<forall> p h. e \<noteq> DeleteShM p h;

   749     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;

   750     \<forall> p f fds. e \<noteq> Execve p f fds;

   751     \<forall> p p'. e \<noteq> Kill p p';

   752     \<forall> p. e \<noteq> Exit p

   753    \<rbrakk> \<Longrightarrow> info_flow_shm (e # s) = info_flow_shm s"

   754 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)

   755 apply (case_tac e, auto simp:info_flow_shm_def one_flow_shm_def dest:procs_of_shm_prop2)

   756 apply (erule_tac x = h in allE, simp)

   757 apply (drule procs_of_shm_prop1, auto)

   758 done

   759 

   760 

   761 (*

   762 lemma info_flow_shm_prop1: 

   763   "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> 

   764    \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"

   765 by (induct rule: info_flow_shm.induct, auto)

   766 

   767 lemma info_flow_shm_cases:

   768   "\<lbrakk>info_flow_shm \<tau> pa pb; \<And>p s. \<lbrakk>s = \<tau> ; pa = p; pb = p; p \<in> current_procs s\<rbrakk> \<Longrightarrow> P;

   769   \<And>s p p' h p'' flag. \<lbrakk>s = \<tau>; pa = p; pb = p''; info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h;

   770                        (p'', flag) \<in> procs_of_shm s h\<rbrakk>\<Longrightarrow> P\<rbrakk>

   771   \<Longrightarrow> P"

   772 by (erule info_flow_shm.cases, auto)

   773 

   774 definition one_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

   775 where

   776   "one_flow_shm s p p' \<equiv> p \<noteq> p' \<and> (\<exists> h flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h)"

   777 

   778 inductive flows_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

   779 where

   780   "p \<in> current_procs s \<Longrightarrow> flows_shm s p p"

   781 | "\<lbrakk>flows_shm s p p'; one_flow_shm s p' p''\<rbrakk> \<Longrightarrow> flows_shm s p p''"

   782 

   783 definition attached_procs :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"

   784 where

   785   "attached_procs s h \<equiv> {p. \<exists> flag. (p, flag) \<in> procs_of_shm s h}"

   786 

   787 definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"

   788 where

   789   "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"

   790 

   791 inductive flowed_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm set"

   792 

   793 fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"

   794 where

   795   "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"

   796 | "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. 

   797      if (p' = p) then flowed_procs s h 

   798      else if ()

   799     "

   800 

   801 

   802 lemma info_flow_shm_attach:

   803   "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or> 

   804      (if (pa = p) 

   805       then (if (flag = SHM_RDWR) 

   806             then (\<exists> flag. (pb, flag) \<in> procs_of_shm s h)

   807             else (pb = p)) 

   808       else (if (pb = p) 

   809             then (pa, SHM_RDWR) \<in> procs_of_shm s h

   810             else info_flow_shm s pa pb)) )"

   811 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)

   812 apply (case_tac "info_flow_shm s pa pb", simp)

   813 

   814 thm info_flow_shm.cases

   815 apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)

   816 apply (erule info_flow_shm_cases, simp, simp split:if_splits)

   817 apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)

   818 apply (rule notI, erule info_flow_shm.cases, simp+)

   819 pr 5

   820 *)

   821 lemmas info_flow_shm_simps = info_flow_shm_other (* info_flow_shm_attach *) info_flow_shm_detach info_flow_shm_deleteshm

   822   info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exit

   823 

   824 

   825 

   826 

   827 

   828 

   829 end

   830 

   831 end