54 

    55 sorry

    56 

    57 definition enrich:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"

    58 where

    59   "enrich s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. obj' \<notin> objs \<and> alive s' obj \<and> co2sobj s' obj' = co2sobj s' obj"

    60 

    61 definition reserve:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"

    62 where

    63   "reserve s objs s' \<equiv> \<forall> obj. alive s obj \<longrightarrow> alive s' obj \<and> co2sobj s' obj = co2sobj s obj"

    64 

    65 definition enrichable :: "t_state \<Rightarrow> t_object set \<Rightarrow> bool"

    66 where

    67   "enrichable s objs \<equiv> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enrich s objs s' \<and> reserve s objs s'"

    68 

    69 definition is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"

    70 where

    71   "is_created s obj \<equiv> init_alive obj \<longrightarrow> deleted obj s"

    72 

    73 definition is_inited :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"

    74 where

    75   "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s"

    76 

    77 lemma is_inited_eq_not_created:

    78   "is_inited s obj = (\<not> is_created s obj)"

    79 by (auto simp:is_created_def is_inited_def)

    80 

    81 (* recorded in our static world *)

    82 fun recorded :: "t_object \<Rightarrow> bool"

    83 where

    84   "recorded (O_proc p)     = True"

    85 | "recorded (O_file f)     = True"

    86 | "recorded (O_dir  f)     = True"

    87 | "recorded (O_node n)     = False" (* cause socket is temperary not considered *)

    88 | "recorded (O_shm  h)     = True"

    89 | "recorded (O_msgq q)     = True"

    90 | "recorded _              = False"

    91 

    92 lemma enrichability: 

    93   "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk>

    94    \<Longrightarrow> enrichable s objs"

    95 proof (induct s arbitrary:objs)

    96   case Nil

    97   hence "objs = {}" 

    98     apply (auto simp:is_created_def)

    99     apply (erule_tac x = x in ballE)

   100     apply (auto simp:init_alive_prop)

   101     done

   102   thus ?case using Nil unfolding enrichable_def enrich_def reserve_def

   103     by (rule_tac x = "[]" in exI, auto)

   104 next

   105   case (Cons e s)

   106   hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj \<Longrightarrow> enrichable s objs"

   107     and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj"

   108     and os: "os_grant s e" and se: "grant s e" and vd: "valid s"

   109     by (auto dest:vt_grant_os vd_cons vt_grant)

   110   show ?case

   111   proof (cases e)

   112     case (Execve p f fds)

   113     hence p4: "e = Execve p f fds" by simp

   114     from p3 have p5: "is_inited s (O_proc p) \<Longrightarrow> (O_proc p) \<notin> objs"

   115       by (auto simp:is_created_def is_inited_def p4 elim!:ballE[where x = "O_proc p"])

   116     show "enrichable (e # s) objs"

   117     proof (case "is_inited s (O_proc p)")

   118       apply (simp add:enrichable_def p4)

   119 

   120       

   121   

   122     apply auto

   123     apply (auto simp:enrichable_def)

   124 apply (induct s)

   125 

   126 

   127 

   128 done

   129 

   130 

   131 (* for the object set, there exists another trace which keeps this objects but also add new identical objects

   132  * that have the same static-signature

   133  *)

   134 

   135 definition potential_trace:: "t_state \<Rightarrow> bool"

   136 where

   137   "potential_trace s \<equiv> \<forall> obj. alive s obj \<and> is_created s obj \<longrightarrow> 

   138       (\<exists> s' obj'. valid s' \<and> s2ss s' = ss \<and> obj' \<noteq> obj \<and> co2sobj s' obj = co2sobj s' obj)

   139      "

   140 

   141 lemma s2d_main_general:

   142   "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss \<and> (\<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<longrightarrow> (\<exists> s'. valid s' \<and> s2ss s' = ss \<and> (\<exists> obj'. obj' \<noteq> obj \<and> co2sobj s' obj = co2sobj s' obj')))"

   143 apply (erule static.induct)

   144 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) defer

   145 

   146 apply (erule exE|erule conjE)+

   147 

   148 apply (simp add:update_ss_def)

   149 

   150 sorry

   151 

   152 lemma s2d_main:

   153   "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"

   154 apply (erule static.induct)

   155 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)

   156 

   157 apply (erule exE|erule conjE)+

   158 

   159 apply (simp add:update_ss_def)