lemma flag_of_proc_shm_prop1:

  "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"

apply (induct s arbitrary:p flag)

apply (simp, drule init_shmflag_has_proc, simp)

apply (frule vd_cons, frule vt_grant_os)

apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)

done

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

lemma one_flow_not_self:

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

by (simp add:one_flow_shm_def)

lemma one_flow_shm_attach:

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

     if (h' = h) 

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

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

          (one_flow_shm s h pa pb)               

     else one_flow_shm s h' pa pb        )"

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

by (auto simp add: one_flow_shm_def)

lemma one_flow_shm_detach:

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

     if (h' = h) 

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

     else one_flow_shm s h' pa pb)"

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

by (auto simp:one_flow_shm_def)

lemma one_flow_shm_deleteshm:

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

     if (h' = h) 

     then False

     else one_flow_shm s h' pa pb)"

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

by (auto simp: one_flow_shm_def)

lemma one_flow_shm_clone:

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

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

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

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

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

          else one_flow_shm s h pa pb)"

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

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

apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)

done

lemma one_flow_shm_execve:

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

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

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

by (auto simp:one_flow_shm_def)

lemma one_flow_shm_kill:

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

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

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

by (auto simp:one_flow_shm_def)

lemma one_flow_shm_exit:

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

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

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

by (auto simp:one_flow_shm_def)

lemma one_flow_shm_other:

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

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

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

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

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

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

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

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

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

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

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

apply (drule procs_of_shm_prop1, auto)

done

lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm

  one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit

inductive Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

where

  ifs_self: "p \<in> current_procs s \<Longrightarrow> Info_flow_shm s p p"

| ifs_flow:"\<lbrakk>Info_flow_shm s p p'; one_flow_shm s h p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"

lemma Info_flow_trans_aux:

  "Info_flow_shm s p' p'' \<Longrightarrow> \<forall>p. Info_flow_shm s p p' \<longrightarrow> Info_flow_shm s p p''"

apply (erule Info_flow_shm.induct)

by (auto intro:Info_flow_shm.intros)

lemma Info_flow_trans:

  "\<lbrakk>Info_flow_shm s p p'; Info_flow_shm s p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"

by (auto dest:Info_flow_trans_aux)

lemma one_flow_flows:

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

apply (rule Info_flow_shm.intros(2), simp_all)

apply (rule Info_flow_shm.intros(1))

apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)

done

lemma ifs_flow': "\<lbrakk>one_flow_shm s h p p'; Info_flow_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"

apply (drule one_flow_flows, simp+)

apply (erule Info_flow_trans, simp+)

done

lemma Info_flow_shm_cases1:

  "\<lbrakk>Info_flow_shm s pa pb; 

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

    \<And>\<tau> p p' h p''. \<lbrakk>\<tau> = s; pa = p; pb = p''; Info_flow_shm \<tau> p p'; one_flow_shm \<tau> h p' p''\<rbrakk> \<Longrightarrow> P\<rbrakk>

   \<Longrightarrow> P"

by (erule Info_flow_shm.cases, auto)

lemma Info_flow_shm_prop1:

  "\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s" 

by (rule notI, drule Info_flow_shm.intros(1), simp)

lemma Info_flow_shm_intro4:

  "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p"

by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros)

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

lemma Info_flow_shm_attach1:

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

    ((Info_flow_shm s pa pb) \<or> 

     (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> 

       (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>

     (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> 

       (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')))"

proof (induct rule:Info_flow_shm.induct)

  case (ifs_self proc \<tau>)

  show ?case

  proof (rule impI)

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

    hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)

    hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)

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

    hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)

    show "Info_flow_shm s proc proc \<or>

          (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> flag = SHM_RDWR \<and> 

           (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc)) \<or>

          (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> 

           (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'))"

      using p4 p3 by auto

  qed

next

  case (ifs_flow \<tau> pa pb h' pc)

  thus ?case

  proof (rule_tac impI)

    assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> (\<tau> = Attach p h flag # s) \<longrightarrow> Info_flow_shm s pa pb \<or>

     \<not> Info_flow_shm s pa pb \<and> pa = p \<and>

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

     \<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')"

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

    from p2 and p4 have p2': "Info_flow_shm s pa pb \<or> 

      (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> 

       (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>

      (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> 

       (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"

      by (erule_tac impE, simp)

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

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

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

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

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

          (one_flow_shm s h pb pc)               

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

    have "\<lbrakk>pa = p; pc = p\<rbrakk> \<Longrightarrow> Info_flow_shm s pa pc " using p7 by simp

    moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag = SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk> 

      \<Longrightarrow> \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"

      sorry

    moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag \<noteq> SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>

      \<Longrightarrow> Info_flow_shm s pa pc"

      sorry

    moreover have "\<lbrakk>pc = p; pa \<noteq> p; \<not> Info_flow_shm s pa pc\<rbrakk>

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

      sorry

    ultimately 

    show "Info_flow_shm s pa pc \<or>

      (\<not> Info_flow_shm s pa pc \<and> pa = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> 

       (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc)) \<or>

      (\<not> Info_flow_shm s pa pc \<and> pc = p \<and> pa \<noteq> p \<and> 

       (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"

      apply auto

      sorry

  qed

qed

lemma Info_flow_shm_intro3:

  "\<lbrakk>Info_flow_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h\<rbrakk>

   \<Longrightarrow> Info_flow_shm s p to"

apply (case_tac "from = to", simp)

apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def)

by (rule_tac x = flag in exI, simp)

lemma Info_flow_shm_attach1:

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

     (if Info_flow_shm s pa pb then True else

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

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

      else if (pb = p) 

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

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

                             Info_flow_shm s p' pb) \<or>

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

     )  )"

proof (induct rule:Info_flow_shm.induct)

  case (ifs_self proc \<tau>)

  show ?case

  proof (rule impI)

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

    hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)

    hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)

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

    hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)

    show "if Info_flow_shm s proc proc then True

    else if proc = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc

         else if proc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'

              else (\<exists>p' flag'. Info_flow_shm s proc p \<and>

                       flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc) \<or>

                   (\<exists>p'. Info_flow_shm s proc p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p proc)"      using p4 p3 by auto

  qed

next

  case (ifs_flow \<tau> pa pb h' pc)

  thus ?case

  proof (rule_tac impI)

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

     (if Info_flow_shm s pa pb then True

      else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb

           else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'

                else (\<exists>p' flag'. Info_flow_shm s pa p \<and>

                         flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>

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

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

    from p2 and p4 have p2': "(if Info_flow_shm s pa pb then True

      else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb

           else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'

                else (\<exists>p' flag'. Info_flow_shm s pa p \<and>

                         flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>

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

      by (erule_tac impE, simp)

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

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

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

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

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

          (one_flow_shm s h pb pc)               

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

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

      \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"

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

      by (simp add:p5, simp add:Info_flow_shm.intros(1))

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

      Info_flow_shm s pa pc"

      using p2' p7 p8 p5

      by (auto split:if_splits dest:Info_flow_shm.intros(2))      

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

    moreover have "pc = p \<Longrightarrow> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p') 

                            \<or> Info_flow_shm s pa pc"

      using p2' p7 p8 p5

      by (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)

    moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> (\<exists>p' flag'. Info_flow_shm s pa p \<and>

                          flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>

                      (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc) \<or>

                      Info_flow_shm s pa pc"

      using p2' p7 p8 p5

      apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)

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

      apply (rule_tac x = flagb in exI, simp)      

      done

    ultimately  show "if Info_flow_shm s pa pc then True

       else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc

            else if pc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'

                 else (\<exists>p' flag'. Info_flow_shm s pa p \<and>

                          flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>

                      (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc)"

      using p7 by auto

  qed

qed

lemma Info_flow_shm_attach:

  "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>

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

     (pb = p \<and> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pa)) )"

apply (rule ext, rule ext, rule iffI)

apply (case_tac "Info_flow_shm s pa pb", simp)

apply (case_tac "pa = p \<and> flag = SHM_RDWR \<and> (\<exists>flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)", simp)

apply (erule Info_flow_shm_cases1, simp, drule_tac p = pc in Info_flow_shm.intros(1), simp)

apply (simp add:one_flow_shm_simps split:if_splits, erule disjE, simp)

apply (simp split:if_splits, (rule impI|rule allI|rule conjI|erule conjE|erule exE)+, simp)

apply (simp)

apply (simp, erule Info_flow_shm_cases', simp, simp)

apply (rule_tac x = 

apply (auto dest:Info_flow_shm.cases)

apply (auto simp add:one_flow_shm_simps)