1 (*<*)

     2 theory Co2sobj_prop

     3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop Alive_prop

     4 begin

     5 (*<*)

     6 

     7 ML {*

     8 fun print_ss ss =

     9 let

    10 val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss

    11 in

    12 simps

    13 end

    14 *}

    15 

    16 

    17 context tainting_s begin

    18 

    19 (********************* cm2smsg simpset ***********************)

    20 

    21 lemma cm2smsg_other: 

    22   "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m; \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 

    23    \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"

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

    25 unfolding cm2smsg_def

    26 apply (case_tac e)

    27 apply (auto simp:sectxt_of_obj_simps 

    28            split:t_object.splits option.splits if_splits 

    29            dest!:current_has_sec')

    30 done

    31 

    32 lemma cm2smsg_sendmsg:

    33   "valid (SendMsg p q m # s) \<Longrightarrow> cm2smsg (SendMsg p q m # s) = (\<lambda> q' m'. 

    34      if (q' = q \<and> m' = m)

    35      then (case (sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of

    36              Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))

    37            | _ \<Rightarrow> None)

    38      else cm2smsg s q' m') "

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

    40 apply (auto simp:cm2smsg_def sectxt_of_obj_simps 

    41   split:if_splits option.splits dest:not_died_init_msg

    42   dest!:current_has_sec')

    43 done

    44 

    45 lemma cm2smsg_recvmsg1:

    46   "\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"

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

    48 apply (auto simp:cm2smsg_def sectxt_of_obj_simps 

    49   split:if_splits option.splits)

    50 done

    51 

    52 lemma cm2smsg_recvmsg2:

    53   "\<lbrakk>m' \<noteq> m; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"

    54 apply (frule vd_cons, frule vt_grant_os)

    55 apply (auto simp:cm2smsg_def sectxt_of_obj_simps 

    56   split:if_splits option.splits)

    57 done

    58 

    59 lemma cm2smsg_recvmsg1':

    60   "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"

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

    62 apply (auto simp:cm2smsg_def sectxt_of_obj_simps 

    63   split:if_splits option.splits)

    64 done

    65 

    66 lemma cm2smsg_recvmsg2':

    67   "\<lbrakk>valid (RecvMsg p q m # s); m' \<noteq> m\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"

    68 apply (frule vd_cons, frule vt_grant_os)

    69 apply (auto simp:cm2smsg_def sectxt_of_obj_simps 

    70   split:if_splits option.splits)

    71 done

    72 

    73 lemma cm2smsg_removemsgq:

    74   "\<lbrakk>q' \<noteq> q; valid (RemoveMsgq p q # s)\<rbrakk> \<Longrightarrow> cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'"

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

    76 apply (auto simp:cm2smsg_def sectxt_of_obj_simps 

    77   split:if_splits option.splits)

    78 done

    79 

    80 lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'

    81   cm2smsg_removemsgq cm2smsg_other

    82 

    83 lemma init_cm2smsg_has_smsg:

    84   "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm"

    85 by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt)

    86 

    87 lemma hd_set_prop1:

    88   "hd l \<notin> set l \<Longrightarrow> l = []"

    89 by (case_tac l, auto)

    90 

    91 lemma tl_set_prop1:

    92   "a \<in> set (tl l) \<Longrightarrow> a \<in> set l"

    93 by (case_tac l, auto)

    94 

    95 lemma current_has_smsg:

    96   "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sm. cm2smsg s q m = Some sm"

    97 apply (induct s)

    98 apply (simp only:cm2smsg_nil_prop msgs_of_queue.simps current_msgqs.simps init_cm2smsg_has_smsg)

    99 

   100 apply (frule vt_grant_os, frule vd_cons, case_tac a)

   101 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits

   102   dest!:current_has_sec' hd_set_prop1 dest:not_died_init_msg tl_set_prop1)

   103 done 

   104 

   105 lemma current_has_smsg':

   106   "\<lbrakk>cm2smsg s q m = None; q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> m \<notin> set (msgs_of_queue s q)"

   107 by (auto dest:current_has_smsg)

   108 

   109 lemma cqm2sms_has_sms_aux:

   110   "\<forall> m \<in> set ms. sectxt_of_obj s (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. cqm2sms s q ms = Some sms)"

   111 by (induct ms, auto split:option.splits simp:cm2smsg_def)

   112 

   113 lemma current_has_sms:

   114   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sms. cqm2sms s q (msgs_of_queue s q) = Some sms"

   115 apply (rule cqm2sms_has_sms_aux)

   116 apply (auto dest:current_msg_has_sec)

   117 done

   118 

   119 lemma current_has_sms':

   120   "\<lbrakk>cqm2sms s q (msgs_of_queue s q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"

   121 by (auto dest:current_has_sms)

   122 

   123 (********************* cqm2sms simpset ***********************) 

   124 

   125 lemma cqm2sms_other:

   126   "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 

   127     \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 

   128    \<Longrightarrow> cqm2sms (e # s) = cqm2sms s"

   129 apply (rule ext, rule ext)

   130 apply (induct_tac xa, simp)

   131 apply (frule vt_grant_os, frule vd_cons, case_tac e)

   132 apply (auto split:option.splits dest:cm2smsg_other) 

   133 done

   134 

   135 lemma cqm2sms_createmsgq:

   136   "valid (CreateMsgq p q # s) \<Longrightarrow> cqm2sms (CreateMsgq p q # s) = (\<lambda> q' ms'. 

   137      if (q' = q \<and> ms' = []) then Some []

   138      else cqm2sms s q' ms')"

   139 apply (rule ext, rule ext)

   140 apply (frule vt_grant_os, frule vd_cons, induct_tac ms')

   141 apply (auto split:if_splits option.splits dest:cm2smsg_other)

   142 done

   143 

   144 lemma cqm2sms_2:

   145   "cqm2sms s q (ms @ [m]) = 

   146      (case (cqm2sms s q ms, cm2smsg s q m) of 

   147        (Some sms, Some sm) \<Rightarrow> Some (sms @ [sm]) 

   148      | _ \<Rightarrow> None)"

   149 apply (induct ms, simp split:option.splits)

   150 by (auto split:option.splits)

   151 

   152 lemmas cqm2sms_simps2 = cqm2sms.simps(1) cqm2sms_2

   153 

   154 declare cqm2sms.simps [simp del]

   155 

   156 lemma cqm2sms_prop1:

   157   "cqm2sms s q ms = None \<Longrightarrow> \<exists> m \<in> set ms. cm2smsg s q m = None"

   158 by (induct ms, auto simp:cqm2sms.simps split:option.splits)

   159 

   160 lemma cqm2sms_sendmsg1:

   161   "\<lbrakk>valid (SendMsg p q m # s); m \<notin> set ms\<rbrakk>

   162    \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms"

   163 apply (frule vt_grant_os, frule vd_cons)

   164 apply (frule cm2smsg_sendmsg)

   165 apply (induct ms rule:rev_induct)

   166 apply (auto split:if_splits option.splits  simp:cqm2sms_simps2)

   167 done

   168 

   169 lemma cqm2sms_sendmsg2:

   170   "\<lbrakk>valid (SendMsg p q m # s); q' \<noteq> q\<rbrakk>

   171    \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms"

   172 apply (frule vt_grant_os, frule vd_cons)

   173 apply (frule cm2smsg_sendmsg)

   174 apply (induct ms rule:rev_induct)

   175 apply (auto split:if_splits option.splits  simp:cqm2sms_simps2)

   176 done

   177 

   178 lemma cqm2sms_sendmsg3:

   179   "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q\<rbrakk>

   180    \<Longrightarrow> cqm2sms (SendMsg p q m # s) q ms' = 

   181      (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of

   182        (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))])

   183      | _ \<Rightarrow> None)"

   184 apply (frule vt_grant_os, frule vd_cons)

   185 apply (frule cm2smsg_sendmsg)

   186 apply (auto split:if_splits option.splits  simp:cqm2sms_simps2 cqm2sms_sendmsg1)

   187 done

   188 

   189 lemma cqm2sms_sendmsg:

   190   "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q'\<rbrakk> 

   191    \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms' = (

   192      if (q' = q) 

   193      then (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of

   194              (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))])

   195            | _ \<Rightarrow> None)

   196      else cqm2sms s q' ms' )"

   197 apply (simp split:if_splits add:cqm2sms_sendmsg2 cqm2sms_sendmsg3)

   198 done

   199 

   200 lemma cqm2sms_recvmsg1:

   201   "\<lbrakk>valid (RecvMsg p q m # s); m \<notin> set ms\<rbrakk> 

   202    \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q ms = cqm2sms s q ms"

   203 apply (frule vt_grant_os, frule vd_cons)

   204 apply (induct ms rule:rev_induct)

   205 apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg2')

   206 done

   207 

   208 lemma cqm2sms_recvmsg2:

   209   "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk>

   210    \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = cqm2sms s q' ms"

   211 apply (frule vt_grant_os, frule vd_cons)

   212 apply (induct ms rule:rev_induct)

   213 apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg1')

   214 done

   215 

   216 lemma cqm2sms_recvmsg:

   217   "\<lbrakk>valid (RecvMsg p q m # s); ms = msgs_of_queue (RecvMsg p q m # s) q'\<rbrakk>

   218    \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = (

   219      if (q' = q) 

   220      then (case (cqm2sms s q (msgs_of_queue s q)) of

   221              Some sms \<Rightarrow> Some (tl sms)

   222            | _ \<Rightarrow> None)

   223      else cqm2sms s q' ms)"

   224 apply (frule vt_grant_os, frule vd_cons)

   225 apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2 

   226      dest!:current_has_sms')

   227 apply (case_tac "msgs_of_queue s q", simp)

   228 apply (frule_tac ms = "tl (msgs_of_queue s q)" in cqm2sms_recvmsg1)

   229 apply (drule_tac q = q in distinct_queue_msgs, simp+)

   230 apply (case_tac a, auto simp:cqm2sms.simps split:option.splits if_splits)

   231 done

   232 

   233 lemma cqm2sms_removemsgq:

   234   "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk> 

   235    \<Longrightarrow> cqm2sms (RemoveMsgq p q # s) q' ms = cqm2sms s q' ms"

   236 apply (frule vt_grant_os, frule vd_cons)

   237 apply (induct ms rule:rev_induct)

   238 apply (auto simp:cqm2sms_simps2 cm2smsg_removemsgq split:option.splits if_splits)

   239 done

   240   

   241 lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg cqm2sms_removemsgq

   242 

   243 (********************* cq2smsgq simpset ***********************) 

   244  

   245 lemma cq2smsgq_other: 

   246   "\<lbrakk>valid (e # s); \<forall> p q. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 

   247     \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 

   248    \<Longrightarrow> cq2smsgq (e # s) = cq2smsgq s" 

   249 apply (frule cqm2sms_other, simp+)

   250 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e) 

   251 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps 

   252            split:t_object.splits option.splits if_splits 

   253             dest:not_died_init_msg) 

   254 done

   255 

   256 lemma cq2smsg_createmsgq:

   257   "valid (CreateMsgq p q # s)

   258    \<Longrightarrow> cq2smsgq (CreateMsgq p q # s) = (cq2smsgq s) (q := 

   259      case (sectxt_of_obj s (O_proc p)) of

   260        Some psec \<Rightarrow> Some (Created, (fst psec, R_object, (snd o snd) psec), [])

   261      | None     \<Rightarrow> None)"

   262 apply (frule vd_cons, frule vt_grant_os)

   263 apply (frule cqm2sms_createmsgq)

   264 apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq 

   265   split:option.splits if_splits dest:not_died_init_msgq)

   266 done

   267 

   268 lemma cq2smsg_sendmsg:

   269   "valid (SendMsg p q m # s) 

   270    \<Longrightarrow> cq2smsgq (SendMsg p q m # s) = (cq2smsgq s) (q := 

   271      case (cq2smsgq s q, sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of 

   272        (Some (qi, sec, sms), Some msec) \<Rightarrow> 

   273           Some (qi, sec, sms @ [(Created, msec, O_msg q m \<in> tainted (SendMsg p q m # s))])

   274      | _ \<Rightarrow> None)"

   275 apply (frule vd_cons, frule vt_grant_os)

   276 apply (rule ext)

   277 apply (frule_tac q' = x in cqm2sms_sendmsg, simp)

   278 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps  split:option.splits if_splits

   279   dest!:current_has_sms' current_has_sec')

   280 done

   281 

   282 lemma current_has_smsgq:

   283   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sq. cq2smsgq s q = Some sq"

   284 by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sec' current_has_sms')

   285 

   286 lemma current_has_smsgq':

   287   "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"

   288 by (auto dest:current_has_smsgq)

   289 

   290 lemma cq2smsg_recvmsg:

   291   "valid (RecvMsg p q m # s) 

   292    \<Longrightarrow> cq2smsgq (RecvMsg p q m # s) = (cq2smsgq s) (q := 

   293     case (cq2smsgq s q) of

   294       Some (qi, sec, sms) \<Rightarrow> Some (qi, sec, tl sms)

   295     | _ \<Rightarrow> None)"

   296 apply (frule vd_cons, frule vt_grant_os)

   297 apply (rule ext, frule_tac q' = x in cqm2sms_recvmsg, simp)

   298 apply (auto simp add:cq2smsgq_def sectxt_of_obj_simps split:option.splits if_splits 

   299   dest!:current_has_sec' current_has_sms' current_has_smsgq')

   300 done

   301 

   302 lemma cq2smsg_removemsgq:

   303   "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk>

   304    \<Longrightarrow> cq2smsgq (RemoveMsgq p q # s) q' = cq2smsgq s q'"

   305 apply (frule vd_cons, frule vt_grant_os)

   306 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps cqm2sms_removemsgq split:if_splits option.splits 

   307   dest!:current_has_sec' current_has_sms' current_has_smsgq')

   308 done

   309 

   310 lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq

   311 

   312 lemma sm_in_sqsms_init_aux:

   313   "\<lbrakk>m \<in> set ms; init_cm2smsg q m = Some sm; q \<in> init_msgqs; 

   314     init_cqm2sms q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   315 apply (induct ms arbitrary:m sm sms)

   316 by (auto split:if_splits option.splits)

   317 

   318 lemma sm_in_sqsms_init:

   319   "\<lbrakk>m \<in> set (init_msgs_of_queue q); init_cm2smsg q m = Some sm; q \<in> init_msgqs; 

   320     init_cqm2sms q (init_msgs_of_queue q) = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   321 by (simp add:sm_in_sqsms_init_aux)

   322 

   323 lemma cqm2sms_prop0:

   324   "\<lbrakk>m \<in> set ms; cm2smsg s q m = Some sm; cqm2sms s q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   325 apply (induct ms arbitrary:m sm sms)

   326 apply (auto simp:cqm2sms.simps split:option.splits)

   327 done

   328 

   329 lemma sm_in_sqsms:

   330   "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; cq2smsgq s q = Some (qi, qsec, sms);

   331     cm2smsg s q m = Some sm\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   332 proof (induct s arbitrary:m q qi qsec sms sm)

   333   case Nil

   334   thus ?case 

   335     by (simp add:cq2smsga_nil_prop cm2smsg_nil_prop init_cq2smsgq_def sm_in_sqsms_init 

   336            split:option.splits)

   337 next

   338   case (Cons e s)

   339   hence p1:"\<And> m q qi qsec sms sm. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; 

   340     cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>

   341     \<Longrightarrow> sm \<in> set sms" and p2: "m \<in> set (msgs_of_queue (e # s) q)" 

   342     and p3: "q \<in> current_msgqs (e # s)" and p4: "valid (e # s)"

   343     and p5: "cq2smsgq (e # s) q = Some (qi, qsec, sms)"

   344     and p6: "cm2smsg (e # s) q m = Some sm" by auto

   345   from p4 have os: "os_grant s e" and vd: "valid s" by (auto dest:vd_cons vt_grant_os)

   346 (*

   347   from p1 have p1':

   348     "\<And> m q qi qsec sms sm ms. \<lbrakk>m \<in> set ms; set ms \<subseteq> set (msgs_of_queue s q); q \<in> current_msgqs s;

   349     valid s; cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>

   350     \<Longrightarrow> sm \<in> set "

   351 *)

   352   show ?case using p2 p3 p4 p5 p6 vd os

   353     apply (case_tac e)

   354     apply (auto simp:cq2smsgq_simps cm2smsg_simps split:if_splits option.splits intro:p1)

   355 

   356     apply (rule_tac m = m and q = q and qi = qi and qsec = qsec in p1, simp+)

   357     apply (case_tac "q = nat2", simp)

   358     apply (drule cq2smsg_createmsgq, simp, simp)

   359 

   360     apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)

   361     apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)

   362 

   363     apply (simp add:cq2smsgq_def split:option.splits)

   364     apply (rule_tac m = m and sm = sm in cqm2sms_prop0, simp+)

   365     apply (simp add:cqm2sms_recvmsg)

   366     done

   367 qed

   368 

   369 (****************** cf2sfile path simpset ***************)

   370 

   371 lemma sroot_only:

   372   "cf2sfile s [] = Some sroot"

   373 by (simp add:cf2sfile_def)

   374 

   375 lemma not_file_is_dir:

   376   "\<lbrakk>\<not> is_file s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s f"

   377 by (auto simp:is_file_def current_files_def is_dir_def 

   378          dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)

   379 

   380 lemma not_dir_is_file:

   381   "\<lbrakk>\<not> is_dir s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f"

   382 by (auto simp:is_file_def current_files_def is_dir_def 

   383          dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)

   384 

   385 lemma is_file_or_dir:

   386   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f \<or> is_dir s f"

   387 by (auto dest:not_dir_is_file)

   388 

   389 lemma current_file_has_sfile:

   390   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

   391 apply (induct f)

   392 apply (rule_tac x = "sroot" in exI, simp add:sroot_only)

   393 apply (frule parentf_in_current', simp, clarsimp)

   394 apply (frule parentf_is_dir'', simp)

   395 apply (frule is_file_or_dir, simp)

   396 apply (auto dest!:current_has_sec'

   397             simp:cf2sfile_def split:option.splits if_splits dest!:get_pfs_secs_prop')

   398 done

   399 

   400 definition sectxt_of_pf :: "t_state \<Rightarrow> t_file \<Rightarrow> security_context_t option"

   401 where

   402   "sectxt_of_pf s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> sectxt_of_obj s (O_dir pf))"

   403 

   404 definition get_parentfs_ctxts' :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"

   405 where

   406   "get_parentfs_ctxts' s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> get_parentfs_ctxts s pf)"

   407 

   408 lemma is_file_has_sfile:

   409   "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec psec asecs. cf2sfile s f = Some 

   410       (if (\<not> died (O_file f) s \<and> is_init_file f) then Init f else Created,

   411        sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_file f) = Some sec) \<and>

   412        (sectxt_of_pf s f = Some psec) \<and> (get_parentfs_ctxts' s f = Some asecs)"

   413 apply (case_tac f, simp, drule root_is_dir', simp, simp)

   414 apply (frule is_file_in_current)

   415 apply (drule current_file_has_sfile, simp)

   416 apply (auto simp:cf2sfile_def sectxt_of_pf_def get_parentfs_ctxts'_def split:if_splits option.splits)

   417 done

   418 

   419 lemma is_file_has_sfile':

   420   "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

   421 by (drule is_file_has_sfile, auto)

   422 

   423 lemma is_dir_has_sfile:

   424   "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> (case f of

   425       [] \<Rightarrow> cf2sfile s f = Some sroot

   426     | a # pf \<Rightarrow> (\<exists> sec psec asecs. cf2sfile s f = Some 

   427       (if (\<not> died (O_dir f) s \<and> is_init_dir f) then Init f else Created,

   428        sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_dir f) = Some sec) \<and>

   429        (sectxt_of_obj s (O_dir pf) = Some psec) \<and> (get_parentfs_ctxts s pf = Some asecs)))"

   430 apply (case_tac f, simp add:sroot_only)

   431 apply (frule is_dir_in_current, frule is_dir_not_file)

   432 apply (drule current_file_has_sfile, simp)

   433 apply (auto simp:cf2sfile_def split:if_splits option.splits)

   434 done

   435 

   436 lemma is_dir_has_sdir':

   437   "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

   438 apply (case_tac f)

   439 apply (rule_tac x = sroot in exI)

   440 apply (simp add:sroot_only)

   441 apply (drule is_dir_has_sfile, auto)

   442 done

   443 

   444 lemma sroot_set:

   445   "valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec"

   446 apply (frule root_is_dir)

   447 apply (drule is_dir_has_sec, simp)

   448 apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps 

   449                  root_type_remains root_user_remains

   450            dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'

   451            split:option.splits)

   452 done

   453 

   454 lemma cf2sfile_path_file:

   455   "\<lbrakk>is_file s (f # pf); valid s\<rbrakk>

   456    \<Longrightarrow> cf2sfile s (f # pf) = (

   457      case (cf2sfile s pf) of

   458        Some (pfi, pfsec, psec, asecs) \<Rightarrow> 

   459           (case (sectxt_of_obj s (O_file (f # pf))) of

   460               Some fsec \<Rightarrow> Some (if (\<not> died (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

   461                                 else Created, fsec, Some pfsec, asecs \<union> {pfsec})

   462            | None \<Rightarrow> None)

   463      | _ \<Rightarrow> None)"

   464 apply (frule is_file_in_current, drule parentf_is_dir'', simp)

   465 apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)

   466 apply (frule sroot_set)

   467 apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 

   468 done

   469 

   470 lemma cf2sfile_path_dir:

   471   "\<lbrakk>is_dir s (f # pf); valid s\<rbrakk>

   472    \<Longrightarrow> cf2sfile s (f # pf) = (

   473      case (cf2sfile s pf) of

   474        Some (pfi, pfsec, psec, asecs) \<Rightarrow> 

   475           (case (sectxt_of_obj s (O_dir (f # pf))) of

   476               Some fsec \<Rightarrow> Some (if (\<not> died (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

   477                                 else Created, fsec, Some pfsec, asecs \<union> {pfsec})

   478            | None \<Rightarrow> None)

   479      | _ \<Rightarrow> None)"

   480 apply (frule is_dir_in_current, drule parentf_is_dir'', simp)

   481 apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp)

   482 apply (frule_tac f = "pf" in is_dir_has_sfile, simp)

   483 apply (frule sroot_set)

   484 apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 

   485 done  

   486 

   487 lemma cf2sfile_path:

   488   "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (

   489      case (cf2sfile s pf) of

   490        Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))

   491          then (case (sectxt_of_obj s (O_file (f # pf))) of

   492                  Some fsec \<Rightarrow> Some (if (\<not> died (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

   493                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})

   494                | None \<Rightarrow> None)

   495          else (case (sectxt_of_obj s (O_dir (f # pf))) of

   496                  Some fsec \<Rightarrow> Some (if (\<not> died (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

   497                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})

   498                | None \<Rightarrow> None)           )

   499      | None \<Rightarrow> None)"

   500 apply (drule is_file_or_dir, simp)

   501 apply (erule disjE)

   502 apply (frule cf2sfile_path_file, simp) defer

   503 apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file)

   504 apply (auto split:option.splits)

   505 done

   506 

   507 lemma cf2sfile_path_file_prop1:

   508   "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>

   509    \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = 

   510                  Some (if (\<not> died (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

   511                        else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> 

   512                sectxt_of_obj s (O_file (f # pf)) = Some fsec"

   513 apply (frule is_file_has_sfile, simp)

   514 by (auto simp:cf2sfile_path_file)

   515 

   516 lemma cf2sfile_path_file_prop2:

   517   "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); 

   518     sectxt_of_obj s (O_file (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = 

   519       Some (if (\<not> died (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

   520             else Created, fsec, Some pfsec, asecs \<union> {pfsec})"

   521 by (drule cf2sfile_path_file_prop1, auto)

   522 

   523 lemma cf2sfile_path_dir_prop1:

   524   "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>

   525    \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = 

   526                  Some (if (\<not> died (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

   527                        else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> 

   528                sectxt_of_obj s (O_dir (f # pf)) = Some fsec"

   529 apply (frule is_dir_has_sfile, simp)

   530 by (auto simp:cf2sfile_path_dir)

   531 

   532 lemma cf2sfile_path_dir_prop2:

   533   "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); 

   534     sectxt_of_obj s (O_dir (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = 

   535       Some (if (\<not> died (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

   536             else Created, fsec, Some pfsec, asecs \<union> {pfsec})"

   537 by (drule cf2sfile_path_dir_prop1, auto)

   538 

   539 (**************** cf2sfile event list simpset ****************)

   540 

   541 lemma cf2sfile_open_none':

   542   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f'= cf2sfile s f'"

   543 apply (frule vd_cons, frule vt_grant_os)

   544 apply (induct f', simp add:cf2sfile_def)

   545 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   546                get_parentfs_ctxts_simps)

   547 done

   548 

   549 lemma cf2sfile_open_none:

   550   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s"

   551 apply (rule ext)

   552 by (simp add:cf2sfile_open_none')

   553 

   554 lemma cf2sfile_open_some1:

   555   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>

   556    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

   557 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   558 apply (case_tac "f = f'", simp)

   559 apply (induct f', simp add:sroot_only, simp)

   560 apply (frule parentf_in_current', simp+)

   561 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   562                get_parentfs_ctxts_simps)

   563 done

   564 

   565 lemma cf2sfile_open_some2:

   566   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk>

   567    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

   568 apply (frule vd_cons, drule is_file_in_current)

   569 by (simp add:cf2sfile_open_some1)

   570 

   571 lemma cf2sfile_open_some3:

   572   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk>

   573    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

   574 apply (frule vd_cons, drule is_dir_in_current)

   575 by (simp add:cf2sfile_open_some1)

   576 

   577 lemma cf2sfile_open_some4:

   578   "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f = (

   579      case (parent f) of

   580        Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), 

   581                          get_parentfs_ctxts s pf) of

   582                     (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   583                   | _ \<Rightarrow> None)

   584      | None \<Rightarrow> None)"

   585 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   586 apply (case_tac f, simp)

   587 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   588                get_parentfs_ctxts_simps)

   589 apply (rule impI, (erule conjE)+)

   590 apply (drule not_died_init_file, simp+)

   591 apply (simp add:is_file_in_current)

   592 done

   593 

   594 lemma cf2sfile_open:

   595   "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>

   596    \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' = (

   597      if (opt = None) then cf2sfile s f'

   598      else if (f' = f) 

   599      then (case (parent f) of

   600              Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf), 

   601                  get_parentfs_ctxts s pf) of

   602                           (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   603                         | _ \<Rightarrow> None)

   604            | None \<Rightarrow> None)

   605      else cf2sfile s f')"

   606 apply (case_tac opt)

   607 apply (simp add:cf2sfile_open_none)

   608 apply (case_tac "f = f'")

   609 apply (simp add:cf2sfile_open_some4 split:option.splits)

   610 apply (simp add:cf2sfile_open_some1 current_files_simps)

   611 done

   612 

   613 lemma cf2sfile_mkdir1:

   614   "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk>

   615    \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

   616 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   617 apply (case_tac "f = f'", simp)

   618 apply (induct f', simp add:sroot_only, simp)

   619 apply (frule parentf_in_current', simp+)

   620 apply (case_tac "f = f'", simp)

   621 apply (simp add:cf2sfile_path is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   622                get_parentfs_ctxts_simps split:if_splits option.splits)

   623 done

   624 

   625 lemma cf2sfile_mkdir2:

   626   "\<lbrakk>valid (Mkdir p f i # s); is_file s f'\<rbrakk>

   627    \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

   628 apply (frule vd_cons, drule is_file_in_current)

   629 by (simp add:cf2sfile_mkdir1)

   630 

   631 lemma cf2sfile_mkdir3:

   632   "\<lbrakk>valid (Mkdir p f i # s); is_dir s f'\<rbrakk>

   633    \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

   634 apply (frule vd_cons, drule is_dir_in_current)

   635 by (simp add:cf2sfile_mkdir1)

   636 

   637 lemma cf2sfile_mkdir4:

   638   "valid (Mkdir p f i # s)

   639   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f = (case (parent f) of

   640          Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), 

   641                            get_parentfs_ctxts s pf) of

   642                       (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   643                     | _ \<Rightarrow> None)

   644        | None \<Rightarrow> None)"

   645 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   646 apply (case_tac f, simp)

   647 apply (clarsimp simp:os_grant.simps)

   648 apply (simp add:sectxt_of_obj_simps)

   649 apply (frule current_proc_has_sec, simp)

   650 apply (frule is_dir_has_sec, simp)

   651 apply (frule get_pfs_secs_prop, simp)

   652 apply (frule is_dir_not_file)

   653 apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   654                get_parentfs_ctxts_simps split:option.splits if_splits 

   655             dest:not_died_init_dir is_dir_in_current not_died_init_file is_file_in_current)

   656 done

   657 

   658 lemma cf2sfile_mkdir:

   659   "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files (Mkdir p f i # s)\<rbrakk>

   660   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = (

   661     if (f' = f) 

   662     then (case (parent f) of

   663              Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), 

   664                  get_parentfs_ctxts s pf) of

   665                           (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   666                         | _ \<Rightarrow> None)

   667            | None \<Rightarrow> None)

   668      else cf2sfile s f')"

   669 apply (case_tac "f = f'")

   670 apply (simp add:cf2sfile_mkdir4 split:option.splits)

   671 apply (simp add:cf2sfile_mkdir1 current_files_simps)

   672 done

   673 

   674 lemma cf2sfile_linkhard1:

   675   "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk>

   676    \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"

   677 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   678 apply (case_tac "f = f'", simp)

   679 apply (induct f', simp add:sroot_only, simp)

   680 apply (frule parentf_in_current', simp+)

   681 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   682                get_parentfs_ctxts_simps split:if_splits option.splits)

   683 done

   684 

   685 lemma cf2sfile_linkhard2:

   686   "\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk>

   687    \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"

   688 apply (frule vd_cons, drule is_file_in_current)

   689 by (simp add:cf2sfile_linkhard1)

   690 

   691 lemma cf2sfile_linkhard3:

   692   "\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk>

   693    \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"

   694 apply (frule vd_cons, drule is_dir_in_current)

   695 by (simp add:cf2sfile_linkhard1)

   696 

   697 lemma cf2sfile_linkhard4:

   698   "valid (LinkHard p oldf f # s)

   699   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of

   700          Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), 

   701                            get_parentfs_ctxts s pf) of

   702                       (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   703                     | _ \<Rightarrow> None)

   704        | None \<Rightarrow> None)"

   705 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   706 apply (case_tac f, simp)

   707 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   708                get_parentfs_ctxts_simps)

   709 apply (rule impI, (erule conjE)+)

   710 apply (drule not_died_init_file, simp+)

   711 apply (simp add:is_file_in_current)

   712 done

   713 

   714 lemma cf2sfile_linkhard:

   715   "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk>

   716   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = (

   717     if (f' = f) 

   718     then (case (parent f) of

   719              Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), 

   720                  get_parentfs_ctxts s pf) of

   721                           (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   722                         | _ \<Rightarrow> None)

   723            | None \<Rightarrow> None)

   724      else cf2sfile s f')"

   725 apply (case_tac "f = f'")

   726 apply (simp add:cf2sfile_linkhard4 split:option.splits)

   727 apply (simp add:cf2sfile_linkhard1 current_files_simps)

   728 done

   729 

   730 lemma cf2sfile_other:

   731   "\<lbrakk>ff \<in> current_files s;

   732     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   733     \<forall> p fd. e \<noteq> CloseFd p fd;

   734     \<forall> p f. e \<noteq> UnLink p f;

   735     \<forall> p f. e \<noteq> Rmdir p f;

   736     \<forall> p f i. e \<noteq> Mkdir p f i;

   737     \<forall> p f f'. e \<noteq> LinkHard p f f'; 

   738     valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"

   739 apply (frule vd_cons, frule vt_grant_os)

   740 apply (induct ff, simp add:sroot_only)

   741 apply (frule parentf_in_current', simp+, case_tac e)

   742 apply (auto simp:current_files_simps is_file_simps is_dir_simps sectxt_of_obj_simps cf2sfile_path 

   743            split:if_splits option.splits)                     

   744 done     

   745 

   746 lemma cf2sfile_other':

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

   748     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   749     \<forall> p fd. e \<noteq> CloseFd p fd;

   750     \<forall> p f. e \<noteq> UnLink p f;

   751     \<forall> p f. e \<noteq> Rmdir p f;

   752     \<forall> p f i. e \<noteq> Mkdir p f i;

   753     \<forall> p f f'. e \<noteq> LinkHard p f f'; 

   754     ff \<in> current_files s\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"

   755 by (auto intro!:cf2sfile_other)

   756   

   757 lemma cf2sfile_unlink:

   758   "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>

   759    \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"

   760 apply (frule vd_cons, frule vt_grant_os)

   761 apply (simp add:current_files_simps split:if_splits)

   762 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps

   763            split:if_splits option.splits)

   764 done

   765 

   766 lemma cf2sfile_rmdir:

   767   "\<lbrakk>valid (Rmdir p f # s); f' \<in> current_files (Rmdir p f # s)\<rbrakk>

   768    \<Longrightarrow> cf2sfile (Rmdir p f # s) f' = cf2sfile s f'"

   769 apply (frule vd_cons, frule vt_grant_os)

   770 apply (simp add:current_files_simps split:if_splits)

   771 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps

   772            split:if_splits option.splits)

   773 done

   774 

   775 lemma pfdof_simp5: "\<lbrakk>proc_fd_of_file s f = {(p, fd)}; file_of_proc_fd s p fd = None\<rbrakk> \<Longrightarrow> False"

   776 apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")

   777 by (simp add:pfdof_simp2, simp)

   778 

   779 lemma pfdof_simp6: "proc_fd_of_file s f = {(p, fd)} \<Longrightarrow> file_of_proc_fd s p fd = Some f"

   780 apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")

   781 by (simp add:pfdof_simp2, simp)

   782 

   783 lemma cf2sfile_closefd:

   784   "\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk>

   785    \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"

   786 apply (frule vd_cons, frule vt_grant_os)

   787 apply (simp add:current_files_simps split:if_splits option.splits) 

   788 (* costs too much time, but solved *)

   789 (*

   790 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps 

   791            split:if_splits option.splits  

   792             dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file

   793                  not_died_init_file not_died_init_dir is_file_not_dir is_dir_not_file

   794             dest!:current_has_sec') 

   795 done

   796 *)

   797 sorry

   798 

   799 lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other

   800   cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd

   801   

   802 (*********** cfd2sfd simpset *********)

   803 

   804 lemma cfd2sfd_open1:

   805   "valid (Open p f flags fd opt # s)

   806    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = 

   807      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

   808         (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)

   809       | _ \<Rightarrow> None)"

   810 by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits)

   811 

   812 lemma cfd2sfd_open_some2:

   813   "\<lbrakk>valid (Open p f flags fd (Some inum) # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   814   \<Longrightarrow> cfd2sfd (Open p f flags fd (Some inum) # s) p' fd' = cfd2sfd s p' fd'"

   815 apply (frule vd_cons, frule vt_grant_os)

   816 apply (frule proc_fd_in_fds, simp)

   817 apply (frule file_of_proc_fd_in_curf, simp)

   818 apply (case_tac "f = f'", simp)

   819 apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_some1)

   820 apply (case_tac "p = p'", simp)

   821 apply (rule conjI, rule impI, simp)

   822 apply (drule cf2sfile_open_some1, simp)

   823 apply (auto split:option.splits)[1]

   824 apply simp

   825 apply (drule cf2sfile_open_some1, simp)

   826 apply (auto split:option.splits)[1]

   827 done

   828 

   829 lemma cfd2sfd_open_none2:

   830   "\<lbrakk>valid (Open p f flags fd None # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   831   \<Longrightarrow> cfd2sfd (Open p f flags fd None # s) p' fd' = cfd2sfd s p' fd'"

   832 apply (frule vd_cons, frule vt_grant_os)

   833 apply (frule proc_fd_in_fds, simp)

   834 apply (frule file_of_proc_fd_in_curf, simp)

   835 apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_none)

   836 apply (case_tac "p = p'", simp)

   837 apply (rule conjI, rule impI, simp)

   838 apply (drule cf2sfile_open_none)

   839 apply (auto split:option.splits)[1]

   840 apply simp

   841 apply (drule cf2sfile_open_none)

   842 apply (auto split:option.splits)[1]

   843 done

   844   

   845 lemma cfd2sfd_open2:

   846   "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   847   \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = cfd2sfd s p' fd'"

   848 apply (case_tac opt)

   849 apply (simp add:cfd2sfd_open_none2)

   850 apply (simp add:cfd2sfd_open_some2)

   851 done

   852 

   853 lemma cfd2sfd_open:

   854   "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd (Open p f flags fd opt # s) p' fd' = Some f'\<rbrakk>

   855    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then 

   856      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

   857         (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)

   858       | _ \<Rightarrow> None)         else cfd2sfd s p' fd')"

   859 apply (simp split:if_splits)

   860 apply (simp add:cfd2sfd_open1 split:option.splits)

   861 apply (simp add:cfd2sfd_open2)

   862 apply (rule impI, simp)

   863 done

   864 

   865 lemma cfd2sfd_closefd:

   866   "\<lbrakk>valid (CloseFd p fd # s); file_of_proc_fd (CloseFd p fd # s) p' fd' = Some f\<rbrakk>

   867    \<Longrightarrow> cfd2sfd (CloseFd p fd # s) p' fd' = cfd2sfd  s p' fd'"

   868 apply (frule vd_cons, frule vt_grant_os)

   869 apply (frule proc_fd_in_fds, simp)

   870 apply (frule file_of_proc_fd_in_curf, simp)

   871 apply (frule cf2sfile_closefd, simp)

   872 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   873 apply (auto split:option.splits if_splits)

   874 done

   875 

   876 lemma cfd2sfd_clone:

   877   "\<lbrakk>valid (Clone p p' fds # s); file_of_proc_fd (Clone p p' fds # s) p'' fd' = Some f\<rbrakk>

   878    \<Longrightarrow> cfd2sfd (Clone p p' fds # s) p'' fd' = (

   879      if (p'' = p') then cfd2sfd s p fd'

   880      else cfd2sfd s p'' fd')"

   881 apply (frule vd_cons, frule vt_grant_os)

   882 apply (frule proc_fd_in_fds, simp)

   883 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   884 apply (frule_tac cf2sfile_other', simp+)

   885 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   886 apply (case_tac "p'' = p'", simp)

   887 apply (auto split:option.splits if_splits)[1]

   888 apply (simp)

   889 apply (auto split:option.splits if_splits)[1]

   890 done

   891 

   892 lemma cfd2sfd_execve:

   893   "\<lbrakk>valid (Execve p f fds # s); file_of_proc_fd (Execve p f fds # s) p' fd' = Some f'\<rbrakk>

   894    \<Longrightarrow> cfd2sfd (Execve p f fds # s) p' fd' = cfd2sfd s p' fd'"

   895 apply (frule vd_cons, frule vt_grant_os)

   896 apply (frule proc_fd_in_fds, simp)

   897 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   898 apply (frule_tac cf2sfile_other', simp+)

   899 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   900 apply (case_tac "p' = p", simp)

   901 apply (auto split:option.splits if_splits)[1]

   902 apply (simp)

   903 apply (auto split:option.splits if_splits)[1]

   904 done

   905 

   906 lemma cfd2sfd_kill:

   907   "\<lbrakk>valid (Kill p p'' # s); file_of_proc_fd (Kill p p'' # s) p' fd' = Some f'\<rbrakk>

   908    \<Longrightarrow> cfd2sfd (Kill p p'' # s) p' fd' = cfd2sfd s p' fd'"

   909 apply (frule vd_cons, frule vt_grant_os)

   910 apply (frule proc_fd_in_fds, simp)

   911 apply (frule proc_fd_in_procs, simp)

   912 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   913 apply (frule_tac cf2sfile_other', simp+)

   914 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   915 apply (auto split:option.splits if_splits)

   916 done

   917 

   918 lemma cfd2sfd_exit:

   919   "\<lbrakk>valid (Exit p # s); file_of_proc_fd (Exit p # s) p' fd' = Some f'\<rbrakk>

   920    \<Longrightarrow> cfd2sfd (Exit p # s) p' fd' = cfd2sfd s p' fd'"

   921 apply (frule vd_cons, frule vt_grant_os)

   922 apply (frule proc_fd_in_fds, simp)

   923 apply (frule proc_fd_in_procs, simp)

   924 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   925 apply (frule_tac cf2sfile_other', simp+)

   926 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   927 apply (auto split:option.splits if_splits)

   928 done

   929 

   930 lemma cfd2sfd_other:

   931   "\<lbrakk>valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f';

   932     \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   933     \<forall> p p'' fds. e \<noteq> Clone p p'' fds\<rbrakk>

   934    \<Longrightarrow> cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'"

   935 apply (frule vd_cons, frule vt_grant_os)

   936 apply (frule proc_fd_in_fds, simp)

   937 apply (frule proc_fd_in_procs, simp)

   938 apply (frule file_of_proc_fd_in_curf, simp)

   939 apply (case_tac e)

   940 apply (auto intro!:cfd2sfd_execve cfd2sfd_closefd cfd2sfd_kill cfd2sfd_exit)

   941 apply (auto simp:cfd2sfd_def sectxt_of_obj_simps current_files_simps cf2sfile_simps split:option.splits)

   942 apply (auto dest!:current_has_sec' dest:file_of_proc_fd_in_curf proc_fd_in_fds)

   943 done

   944 

   945 lemmas cfd2sfd_simps = cfd2sfd_open cfd2sfd_clone cfd2sfd_other

   946 

   947 (********** cpfd2sfds simpset **********)

   948 

   949 lemma current_filefd_has_flags:

   950   "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists> flags. flags_of_proc_fd s p fd = Some flags"

   951 apply (induct s arbitrary:p)

   952 apply (simp only:flags_of_proc_fd.simps file_of_proc_fd.simps init_filefd_prop4)

   953 apply (frule vd_cons, frule vt_grant_os, case_tac a)

   954 apply (auto split:if_splits option.splits dest:proc_fd_in_fds)

   955 done

   956 

   957 lemma current_filefd_has_flags':

   958   "\<lbrakk>flags_of_proc_fd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"

   959 apply (case_tac "file_of_proc_fd s p fd")

   960 apply (simp, drule current_filefd_has_flags, simp+)

   961 done

   962 

   963 lemma current_file_has_sfile':

   964   "\<lbrakk>cf2sfile s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

   965 by (rule notI, drule current_file_has_sfile, simp+)

   966 

   967 lemma current_filefd_has_sfd:

   968   "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists>sfd. cfd2sfd s p fd = Some sfd"

   969 by (auto simp:cfd2sfd_def split:option.splits dest!:current_has_sec' current_file_has_sfile' 

   970          dest:file_of_proc_fd_in_curf proc_fd_in_fds current_filefd_has_flags)

   971 

   972 lemma current_filefd_has_sfd':

   973   "\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"

   974 by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd)

   975 

   976 lemma cpfd2sfds_open1:

   977   "valid (Open p f flags fd opt # s) \<Longrightarrow>

   978    cpfd2sfds (Open p f flags fd opt # s) p = (

   979     case (cfd2sfd (Open p f flags fd opt # s) p fd) of

   980         Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd}

   981       | _ \<Rightarrow> cpfd2sfds s p)"

   982 apply (frule vd_cons, frule vt_grant_os)

   983 apply (split option.splits)

   984 apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp)

   985 apply (rule allI, rule impI)

   986 apply (rule set_eqI, rule iffI)

   987 apply (case_tac "x = a", simp)

   988 unfolding cpfd2sfds_def

   989 apply (erule CollectE, (erule conjE|erule bexE)+)

   990 apply (simp add:proc_file_fds_def split:if_splits)

   991 apply (erule exE, rule_tac x = fda in exI)

   992 apply (simp add:cfd2sfd_open2)

   993 apply (case_tac "x = a", simp add:proc_file_fds_def)

   994 apply (rule_tac x = fd in exI, simp+)

   995 apply (erule conjE|erule bexE)+

   996 apply (rule_tac x = fda in bexI)

   997 apply (simp add:proc_file_fds_def, erule exE)

   998 apply (simp add:cfd2sfd_open2)

   999 apply (simp add:proc_file_fds_def)

  1000 done

  1001 

  1002 lemma cpfd2sfds_open1':

  1003   "valid (Open p f flags fd opt # s) \<Longrightarrow>

  1004    cpfd2sfds (Open p f flags fd opt # s) p = (

  1005     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

  1006         (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}

  1007       | _ \<Rightarrow> cpfd2sfds s p)"

  1008 apply (frule cfd2sfd_open1)

  1009 apply (auto dest:cpfd2sfds_open1 split:option.splits)

  1010 done

  1011 

  1012 lemma cpfd2sfds_open2:

  1013   "\<lbrakk>valid (Open p f flags fd opt # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) p' = cpfd2sfds s p'"

  1014 apply (frule vt_grant_os, frule vd_cons)

  1015 unfolding cpfd2sfds_def

  1016 apply (rule set_eqI, rule iffI)

  1017 apply (simp add:proc_file_fds_def)

  1018 apply (erule exE|erule conjE)+

  1019 apply (simp only:file_of_proc_fd.simps cfd2sfd_open2 split:if_splits)

  1020 apply (rule_tac x = fda in exI, simp)

  1021 apply (simp add:proc_file_fds_def)

  1022 apply (erule exE|erule conjE)+

  1023 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)

  1024 done

  1025 

  1026 lemma cpfd2sfds_open:

  1027   "valid (Open p f flags fd opt # s)

  1028    \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := (

  1029     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

  1030         (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}

  1031       | _ \<Rightarrow> cpfd2sfds s p))"

  1032 apply (rule ext)

  1033 apply (case_tac "x \<noteq> p")

  1034 apply (simp add:cpfd2sfds_open2)

  1035 apply (simp add:cpfd2sfds_open1')

  1036 done

  1037 

  1038 lemma cpfd2sfds_execve:

  1039   "valid (Execve p f fds # s) 

  1040    \<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})"

  1041 apply (frule vd_cons, frule vt_grant_os)

  1042 apply (rule ext)

  1043 apply (rule set_eqI, rule iffI)

  1044 unfolding cpfd2sfds_def proc_file_fds_def

  1045 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1046 apply (simp split:if_splits)

  1047 apply (frule_tac p' = p and fd' = fd in cfd2sfd_other, simp+)

  1048 apply (rule_tac x = fd in bexI, simp+)

  1049 apply (simp add:cpfd2sfds_def proc_file_fds_def)

  1050 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1051 apply (rule_tac x = fd in exI, simp)

  1052 apply (simp split:if_splits)

  1053 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1054 apply (rule_tac x = fd in exI, simp)

  1055 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1056 apply (simp add:cpfd2sfds_def proc_file_fds_def)

  1057 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1058 apply (rule_tac x = fd in exI, simp)

  1059 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1060 done

  1061 

  1062 lemma cpfd2sfds_clone:

  1063   "valid (Clone p p' fds # s) 

  1064    \<Longrightarrow> cpfd2sfds (Clone p p' 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})"

  1065 apply (frule vd_cons, frule vt_grant_os)

  1066 apply (rule ext)

  1067 apply (rule set_eqI, rule iffI)

  1068 unfolding cpfd2sfds_def proc_file_fds_def

  1069 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1070 apply (simp split:if_splits)

  1071 apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)

  1072 apply (rule_tac x = fd in bexI, simp+)

  1073 apply (simp add:cpfd2sfds_def proc_file_fds_def)

  1074 apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)

  1075 apply (rule_tac x = fd in exI, simp)

  1076 apply (simp split:if_splits)

  1077 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1078 apply (rule_tac x = fd in exI, simp)

  1079 apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)

  1080 apply (simp add:cpfd2sfds_def proc_file_fds_def)

  1081 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1082 apply (rule_tac x = fd in exI, simp)

  1083 apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)

  1084 done

  1085 

  1086 lemma cpfd2sfds_other:

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

  1088     \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

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

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

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

  1092     \<forall> p fd. e \<noteq> CloseFd p fd;

  1093     \<forall> p p' fds. e \<noteq> Clone p p' fds\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"

  1094 apply (frule vd_cons, frule vt_grant_os)

  1095 apply (rule ext)

  1096 unfolding cpfd2sfds_def proc_file_fds_def

  1097 apply (case_tac e)

  1098 using cfd2sfd_other

  1099 by auto

  1100 

  1101 lemma cpfd2sfds_kill:

  1102   "valid (Kill p p' # s) \<Longrightarrow> cpfd2sfds (Kill p p' # s) = (cpfd2sfds s) (p' := {})"

  1103 apply (frule vd_cons, frule vt_grant_os)

  1104 apply (rule ext, rule set_eqI)

  1105 unfolding cpfd2sfds_def proc_file_fds_def

  1106 apply (rule iffI)

  1107 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1108 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

  1109 apply (rule_tac x = fd in exI, simp)

  1110 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1111 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

  1112 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1113 apply (rule_tac x = fd in exI, simp)

  1114 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1115 done

  1116 

  1117 lemma cpfd2sfds_exit:

  1118   "valid (Exit p # s) \<Longrightarrow> cpfd2sfds (Exit p # s) = (cpfd2sfds s) (p := {})"

  1119 apply (frule vd_cons, frule vt_grant_os)

  1120 apply (rule ext, rule set_eqI)

  1121 unfolding cpfd2sfds_def proc_file_fds_def

  1122 apply (rule iffI)

  1123 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1124 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

  1125 apply (rule_tac x = fd in exI, simp)

  1126 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1127 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

  1128 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1129 apply (rule_tac x = fd in exI, simp)

  1130 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1131 done

  1132 

  1133 lemma cpfd2sfds_closefd:

  1134   "valid (CloseFd p fd # s) \<Longrightarrow> cpfd2sfds (CloseFd p fd # s) = (cpfd2sfds s) (p := 

  1135      if (fd \<in> proc_file_fds s p)