1 theory Enrich2 |
1 theory Enrich2 |
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
3 Temp Enrich Proc_fd_of_file_prop |
3 Temp Enrich Proc_fd_of_file_prop New_obj_prop |
4 begin |
4 begin |
5 |
5 |
|
6 fun assoc :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" |
|
7 where |
|
8 "assoc [] a = None" |
|
9 | "assoc (e # l) a = (if (fst e = a) then Some (snd e) else assoc l a)" |
|
10 |
|
11 context flask begin |
|
12 |
|
13 lemma sock_inum_eq_prop: |
|
14 "\<lbrakk>inum_of_socket s (p, fd) = Some im; inum_of_socket s (p', fd') = Some im; valid s\<rbrakk> |
|
15 \<Longrightarrow> (p' = p \<and> fd' = fd)" |
|
16 apply (induct s arbitrary:p p') |
|
17 apply (simp) defer |
|
18 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
19 apply (auto split:if_splits option.splits simp:proc_file_fds_def) |
|
20 sorry |
|
21 |
|
22 lemma inums_execve: |
|
23 "valid (Execve p f fds # s) \<Longrightarrow> |
|
24 current_inode_nums (Execve p f fds # s) = current_inode_nums s - |
|
25 {inum. \<exists> fd. inum_of_socket s (p, fd) = Some inum}" |
|
26 apply (frule vt_grant_os, frule vd_cons) |
|
27 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def |
|
28 dest:filefd_socket_conflict fim_noninter_sim' dest:fim_noninter_sim'' sock_inum_eq_prop) |
|
29 apply (drule set_mp, simp, simp, erule exE, drule filefd_socket_conflict, |
|
30 simp add:current_sockets_def, simp, simp)+ |
|
31 apply (case_tac "a = p", simp) |
|
32 apply (auto) |
|
33 done |
|
34 |
|
35 lemma inums_clone: |
|
36 "valid (Clone p p' fds # s) \<Longrightarrow> |
|
37 current_inode_nums (Clone p p' fds # s) = current_inode_nums s" |
|
38 apply (frule vt_grant_os, frule vd_cons) |
|
39 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def |
|
40 dest:filefd_socket_conflict fim_noninter_sim' dest:fim_noninter_sim'' sock_inum_eq_prop) |
|
41 apply (case_tac "a = p'") |
|
42 apply (subgoal_tac "(p', b) \<in> current_sockets s") |
|
43 apply (drule cn_in_curp, simp, simp, simp add:current_sockets_def) |
|
44 apply auto |
|
45 done |
|
46 |
|
47 lemma inums_kill: |
|
48 "valid (Kill p p' # s) \<Longrightarrow> current_inode_nums (Kill p p' # s) = current_inode_nums s - |
|
49 {inum. \<exists> fd. inum_of_socket s (p', fd) = Some inum}" |
|
50 apply (frule vt_grant_os, frule vd_cons) |
|
51 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def |
|
52 dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop) |
|
53 done |
|
54 |
|
55 lemma inums_exit: |
|
56 "valid (Exit p # s) \<Longrightarrow> current_inode_nums (Exit p # s) = current_inode_nums s - |
|
57 {inum. \<exists> fd. inum_of_socket s (p, fd) = Some inum}" |
|
58 apply (frule vt_grant_os, frule vd_cons) |
|
59 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def |
|
60 dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop) |
|
61 done |
|
62 |
|
63 lemma inums_ptrace: |
|
64 "current_inode_nums (Ptrace p p' # s) = current_inode_nums s" |
|
65 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def |
|
66 dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop) |
|
67 done |
|
68 |
|
69 lemma inums_open: |
|
70 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
|
71 current_inode_nums (Open p f flags fd opt # s) = ( |
|
72 case opt of |
|
73 None \<Rightarrow> current_inode_nums s |
|
74 | Some i \<Rightarrow> current_inode_nums s \<union> {i})" |
|
75 apply (frule vt_grant_os, frule vd_cons) |
|
76 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def |
|
77 dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits) |
|
78 apply (case_tac "fa = f", simp add:current_files_def) |
|
79 apply (rule_tac x = fa in exI, auto) |
|
80 done |
|
81 |
|
82 lemma inums_readfile: |
|
83 "current_inode_nums (ReadFile p fd # s) = current_inode_nums s" |
|
84 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def) |
|
85 done |
|
86 |
|
87 lemma inums_writefile: |
|
88 "current_inode_nums (WriteFile p fd # s) = current_inode_nums s" |
|
89 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def) |
|
90 done |
|
91 |
|
92 lemma inums_mkdir: |
|
93 "valid (Mkdir p f inum # s) \<Longrightarrow> current_inode_nums (Mkdir p f inum # s) = current_inode_nums s \<union> {inum}" |
|
94 apply (frule vt_grant_os, frule vd_cons) |
|
95 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def |
|
96 dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits) |
|
97 apply (case_tac "fa = f", simp add:current_files_def) |
|
98 apply (rule_tac x = fa in exI, auto) |
|
99 done |
|
100 |
|
101 lemma inums_linkhard: |
|
102 "valid (LinkHard p f f' # s) \<Longrightarrow> current_inode_nums (LinkHard p f f' # s) = current_inode_nums s" |
|
103 apply (frule vt_grant_os, frule vd_cons) |
|
104 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def |
|
105 dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits) |
|
106 apply (case_tac "fa = f'", simp add:current_files_def) |
|
107 apply (rule_tac x = fa in exI, auto) |
|
108 done |
|
109 |
|
110 lemma inums_truncate: |
|
111 "current_inode_nums (Truncate p f len # s) = current_inode_nums s" |
|
112 apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def) |
|
113 done |
|
114 |
|
115 lemma inums_createmsgq: |
|
116 "current_inode_nums (CreateMsgq p q # s) = current_inode_nums s" |
|
117 by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def) |
|
118 |
|
119 lemma inums_sendmsg: |
|
120 "current_inode_nums (SendMsg p q m # s) = current_inode_nums s" |
|
121 by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def) |
|
122 |
|
123 lemma inums_recvmsg: |
|
124 "current_inode_nums (RecvMsg p q m # s) = current_inode_nums s" |
|
125 by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def) |
|
126 |
|
127 lemma inums_removemsgq: |
|
128 "current_inode_nums (RemoveMsgq p q # s) = current_inode_nums s" |
|
129 by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def) |
|
130 |
|
131 lemma inums_bind: |
|
132 "valid (Bind p fd addr # s) \<Longrightarrow> current_inode_nums (Bind p fd addr # s) = current_inode_nums s" |
|
133 by (auto dest:vt_grant) |
|
134 |
|
135 lemma inums_connect: |
|
136 "valid (Connect p fd addr # s) \<Longrightarrow> current_inode_nums (Connect p fd addr # s) = current_inode_nums s" |
|
137 by (auto dest:vt_grant) |
|
138 |
|
139 lemma inums_listen: |
|
140 "valid (Listen p fd # s) \<Longrightarrow> current_inode_nums (Listen p fd # s) = current_inode_nums s" |
|
141 by (auto dest:vt_grant) |
|
142 |
|
143 lemma inums_sendsock: |
|
144 "valid (SendSock p fd # s) \<Longrightarrow> current_inode_nums (SendSock p fd # s) = current_inode_nums s" |
|
145 by (auto dest:vt_grant) |
|
146 |
|
147 lemma inums_recvsock: |
|
148 "valid (RecvSock p fd # s) \<Longrightarrow> current_inode_nums (RecvSock p fd # s) = current_inode_nums s" |
|
149 by (auto dest:vt_grant) |
|
150 |
|
151 lemma inums_shutdown: |
|
152 "valid (Shutdown p fd how # s) \<Longrightarrow> current_inode_nums (Shutdown p fd how # s) = current_inode_nums s" |
|
153 by (auto dest:vt_grant) |
|
154 |
|
155 lemma inums_createsock: |
|
156 "valid (CreateSock p af st fd inum # s) \<Longrightarrow> current_inode_nums (CreateSock p af st fd inum # s) = |
|
157 current_inode_nums s" |
|
158 by (auto dest:vt_grant) |
|
159 |
|
160 lemma inums_accept: |
|
161 "valid (Accept p fd addr port fd inum # s) \<Longrightarrow> current_inode_nums (Accept p fd addr port fd inum # s) = |
|
162 current_inode_nums s" |
|
163 by (auto dest:vt_grant) |
|
164 |
|
165 lemmas current_inode_nums_simps = inums_execve inums_open inums_mkdir |
|
166 inums_linkhard inums_createmsgq inums_sendmsg |
|
167 inums_createsock inums_accept inums_clone inums_kill inums_ptrace inums_exit inums_readfile |
|
168 inums_writefile inums_truncate inums_recvmsg inums_removemsgq |
|
169 inums_bind inums_connect inums_listen inums_sendsock |
|
170 inums_recvsock inums_shutdown |
|
171 |
|
172 end |
|
173 |
6 context tainting_s begin |
174 context tainting_s begin |
7 |
175 |
8 fun new_cf :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_file \<Rightarrow> t_file" |
176 fun new_cf :: "t_file set \<Rightarrow> t_file \<Rightarrow> t_file" |
9 where |
177 where |
10 "new_cf s fs [] = []" |
178 "new_cf fs [] = []" |
11 | "new_cf s fs (f#pf) = new_childf_general pf s fs" |
179 | "new_cf fs (f#pf) = new_childf_general pf fs" |
12 |
180 |
13 fun enrich_dufs:: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_file) list" |
181 lemma new_cf_notin_fs: |
|
182 "\<lbrakk>finite fs; f \<noteq> []\<rbrakk> \<Longrightarrow> new_cf fs f \<notin> fs" |
|
183 apply (case_tac f, simp) |
|
184 apply (auto simp:ncf_notin_curf_general) |
|
185 done |
|
186 |
|
187 fun enrich_dufs:: "t_state \<Rightarrow> t_file set \<Rightarrow> t_file set \<Rightarrow> (t_file \<times> t_file) list" |
14 where |
188 where |
15 "enrich_dufs [] tf s = []" |
189 "enrich_dufs [] sames curfs = []" |
16 | "enrich_dufs (Open p f flags fd (Some inum) # s) tf s' = |
190 | "enrich_dufs (Open p f flags fd opt # s) sames curfs = |
17 (if (f \<in> same_inode_files s' tf) |
191 (if (f \<in> sames \<and> opt \<noteq> None) |
18 then [(f, new_cf s' {} f)] |
192 then (f, new_cf (curfs \<union> set (map snd (enrich_dufs s sames curfs))) f) # enrich_dufs s sames curfs |
19 else enrich_dufs s tf s')" |
193 else enrich_dufs s sames curfs)" |
20 | "enrich_dufs (LinkHard p f f' # s) tf s' = |
194 | "enrich_dufs (LinkHard p f f' # s) sames curfs = |
21 (if (f' \<in> same_inode_files s' tf) |
195 (if (f' \<in> sames) |
22 then (f', new_cf s' (set (map snd (enrich_dufs s tf s'))) f') # enrich_dufs s tf s' |
196 then (f', new_cf (curfs \<union> set (map snd (enrich_dufs s sames curfs))) f') # enrich_dufs s sames curfs |
23 else enrich_dufs s tf s')" |
197 else enrich_dufs s sames curfs)" |
24 | "enrich_dufs (_ # s) tf s' = enrich_dufs s tf s'" |
198 | "enrich_dufs (_ # s) sames curfs = enrich_dufs s sames curfs" |
|
199 |
|
200 lemma enrich_dufs_sameinodes1: |
|
201 "set (map fst (enrich_dufs s sames curfs)) \<subseteq> sames" |
|
202 apply (induct s, simp) |
|
203 by (case_tac a, auto) |
25 |
204 |
26 lemma enrich_dufs_sameinodes: |
205 lemma enrich_dufs_sameinodes: |
27 "valid s \<Longrightarrow> set (map snd (enrich_dufs s f s)) = same_inode_files s f" |
206 "\<lbrakk>valid s; \<forall> f \<in> sames. f \<notin> init_files; no_del_event s\<rbrakk> |
28 thm enrich_dufs.induct |
207 \<Longrightarrow> set (map fst (enrich_dufs s sames curfs)) = sames \<inter> {f. is_file s f} " |
29 apply (induct rule:enrich_dufs.induct) |
208 apply (induct s) |
30 |
209 apply (auto simp:is_file_nil is_init_file_props current_files_simps)[1] |
31 apply (erule enrich_dufs.induct) |
210 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
32 |
211 apply (auto simp:is_file_simps is_file_in_current current_files_simps |
33 fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_inode_num \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)" |
212 same_inode_files_simps split:option.splits if_splits) |
|
213 done |
|
214 |
|
215 lemma finite_enrich_nfs: |
|
216 "finite (snd ` set (enrich_dufs s sames curfs))" |
|
217 by (auto) |
|
218 |
|
219 lemma new_cf_enrich: |
|
220 "\<lbrakk>finite curfs; f \<noteq> []\<rbrakk> \<Longrightarrow> new_cf (curfs \<union> snd ` set (enrich_dufs s sames curfs)) f \<notin> curfs \<union> snd ` set (enrich_dufs s sames curfs)" |
|
221 using finite_enrich_nfs[where s = s and sames =sames and curfs = curfs] |
|
222 apply (drule_tac F = curfs and G = "snd ` set (enrich_dufs s sames curfs)" in finite_UnI, simp) |
|
223 apply (rule new_cf_notin_fs, simp+) |
|
224 done |
|
225 |
|
226 lemma enrich_dufs_nfs: |
|
227 "\<lbrakk>finite curfs; [] \<notin> sames\<rbrakk> |
|
228 \<Longrightarrow> set (map snd (enrich_dufs s sames curfs)) \<inter> curfs = {}" |
|
229 apply (induct s) |
|
230 apply (simp) |
|
231 apply ( case_tac a) |
|
232 apply (auto simp:is_file_in_current) |
|
233 apply (drule_tac f = list and sames = sames and curfs = curfs and s = s in new_cf_enrich) |
|
234 apply (rule notI, simp+) |
|
235 apply (drule_tac f = list2 and sames = sames and curfs = curfs and s = s in new_cf_enrich) |
|
236 apply (rule notI, simp+) |
|
237 done |
|
238 |
|
239 lemma pair_list_set: "(a, b) \<in> set l \<Longrightarrow> b \<in> snd ` set l" |
|
240 by (induct l, auto) |
|
241 |
|
242 lemma enrich_dufs_nfs_distinct: |
|
243 "\<lbrakk>finite curfs; [] \<notin> sames\<rbrakk> \<Longrightarrow> distinct (map snd (enrich_dufs s sames curfs))" |
|
244 apply (induct s, simp) |
|
245 apply (case_tac a, auto) |
|
246 apply (drule pair_list_set) |
|
247 apply (drule_tac f = list and s = s and sames = sames and curfs = curfs in new_cf_enrich) |
|
248 apply (rule notI, simp, simp) |
|
249 apply (drule pair_list_set) |
|
250 apply (drule_tac f = list2 and s = s and sames = sames and curfs = curfs in new_cf_enrich) |
|
251 apply (rule notI, simp, simp) |
|
252 done |
|
253 |
|
254 fun all_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set" |
34 where |
255 where |
35 "enrich_file [] tf ninum s = ({}, [])" |
256 "all_fds [] = init_fds_of_proc" |
36 | "enrich_file (Open p f flags fd (Some inum) # s) tf ninum s = |
257 | "all_fds (Open p f flags fd ipt # s) = (all_fds s) (p := all_fds s p \<union> {fd})" (* |
37 if (f \<in> same_inode_fies s tf) |
258 | "all_fds (CreateSock p sf st fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})" |
38 then Open p f flags fd (Some" |
259 | "all_fds (Accept p fd' raddr port fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})" *) |
39 |
260 | "all_fds (Clone p p' fds # s) = (all_fds s) (p' := fds)" |
40 |
261 | "all_fds (_ # s) = all_fds s" |
|
262 |
|
263 fun enrich_dufds :: "t_state \<Rightarrow> t_file set \<Rightarrow> (t_process \<Rightarrow> t_fd set) \<Rightarrow> (t_state \<times> t_fd) list" |
|
264 where |
|
265 "enrich_dufds [] sames allpfds = []" |
|
266 | "enrich_dufds (Open p f flags fd opt # s) sames allpfds = |
|
267 (if (f \<in> sames) |
|
268 then (Open p f flags fd opt # s, next_nat (allpfds p \<union> set (map snd (enrich_dufds s sames allpfds)))) # |
|
269 (enrich_dufds s sames allpfds) |
|
270 else enrich_dufds s sames allpfds)" |
|
271 | "enrich_dufds (e # s) sames allpfds = enrich_dufds s sames allpfds" |
|
272 |
|
273 fun index_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_state" |
|
274 where |
|
275 "index_fd [] p fd = []" |
|
276 | "index_fd (Open p f flags fd opt # s) p' fd' = |
|
277 (if (p' = p \<and> fd' = fd) then Open p f flags fd opt # s |
|
278 else index_fd s p' fd')" |
|
279 | "index_fd (e # s) p fd = index_fd s p fd" |
|
280 |
|
281 definition enrich_fdset :: "t_state \<Rightarrow> (t_state \<times> t_fd) list \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> t_fd set" |
|
282 where |
|
283 "enrich_fdset s dufds p fds \<equiv> |
|
284 fds \<union> {fd'. \<exists> fd \<in> fds. assoc dufds (index_fd s p fd) = Some fd'}" |
|
285 |
|
286 |
|
287 fun enrich_file :: "t_state \<Rightarrow> t_inode_num \<Rightarrow> (t_file \<times> t_file) list |
|
288 \<Rightarrow> ((t_file \<times> t_process \<times> t_fd) \<times> t_fd) list \<Rightarrow> t_state" |
|
289 where |
|
290 "enrich_file [] inum dufs dufds = []" |
|
291 | "enrich_file (Open p f flags fd None # s) inum dufs dufds = |
|
292 (case (assoc dufds (Open p f flags fd None # s), assoc dufs f) of |
|
293 (Some fd', Some f') \<Rightarrow> Open p f' flags fd' None # Open p f flags fd None # enrich_file s inum dufs dufds |
|
294 | _ \<Rightarrow> Open p f flags fd None # (enrich_file s inum dufs dufds))" |
|
295 | "enrich_file (Open p f flags fd (Some inum) # s) inum' dufs dufds = |
|
296 (case (assoc dufs f, assoc dufds (f, p, fd)) of |
|
297 (Some f', Some fd') \<Rightarrow> Open p f' flags fd' (Some inum') # Open p f flags fd (Some inum) # |
|
298 enrich_file s inum dufs dufds |
|
299 | _ \<Rightarrow> Open p f flags fd (Some inum) # enrich_file s inum dufs dufds)" |
|
300 | "enrich_file (LinkHard p f f' # s) inum dufs dufds = |
|
301 (case (assoc dufs f, assoc dufs f') of |
|
302 (Some df, Some df') \<Rightarrow> LinkHard p df df' # LinkHard p f f' # enrich_file s inum dufs dufds |
|
303 | _ \<Rightarrow> LinkHard p f f' # enrich_file s inum dufs dufds)" |
|
304 | "enrich_file (Clone p p' fds # s) inum dufs dufds = |
|
305 Clone p p' (enrich_fdset s dufds p fds) # (enrich_file s inum dufs dufds)" |
|
306 | "enrich_file (Execve p f fds # s) inum dufs dufds = |
|
307 Execve p f (enrich_fdset s dufds p fds) # (enrich_file s inum dufs dufds)" |
|
308 | "enrich_file (WriteFile p fd # s) inum dufs dufds = |
|
309 (case (file_of_proc_fd s p fd) of |
|
310 Some f \<Rightarrow> (case (assoc dufds (f, p, fd)) of |
|
311 Some fd' \<Rightarrow> WriteFile p fd' # WriteFile p fd # enrich_file s inum dufs dufds |
|
312 | _ \<Rightarrow> WriteFile p fd # enrich_file s inum dufs dufds) |
|
313 | _ \<Rightarrow> [])" |
|
314 | "enrich_file (e # s) inum dufs dufds = e # enrich_file s inum dufs dufds" |
|
315 |
|
316 definition same_inodes_list :: "t_state \<Rightarrow> t_file list \<Rightarrow> bool" |
|
317 where |
|
318 "same_inodes_list s flist \<equiv> flist \<noteq> [] \<and> set flist = same_inode_files s (hd flist)" |
|
319 |
|
320 lemma assoc_dufs_prop1: |
|
321 "\<lbrakk>\<forall> f \<in> set (map snd dufs). f \<notin> current_files s; assoc dufs f = Some f'\<rbrakk> \<Longrightarrow> f' \<notin> current_files s" |
|
322 apply (erule_tac x = "f'" in ballE) |
|
323 apply auto |
|
324 apply (induct dufs, auto split:if_splits) |
|
325 done |
|
326 |
|
327 |
|
328 lemma enrich_file_dufs_inode_aux1: |
|
329 "\<lbrakk>no_del_event s; valid s; f \<in> current_files s; \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> f' \<notin> current_files s\<rbrakk> |
|
330 \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f = inum_of_file s f" |
|
331 apply (induct s arbitrary:f, simp) |
|
332 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
333 apply (auto split:option.splits simp:current_files_simps dest:is_file_in_current is_dir_in_current) |
|
334 done |
|
335 |
|
336 lemma enrich_file_dufs_inode1: |
|
337 "\<lbrakk>no_del_event s; valid s; f \<in> current_files s; \<forall> f \<in> set (map snd dufs). f \<notin> current_files s\<rbrakk> |
|
338 \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f = inum_of_file s f" |
|
339 apply (erule enrich_file_dufs_inode_aux1) |
|
340 apply (simp, simp) |
|
341 apply (erule assoc_dufs_prop1, simp+) |
|
342 done |
|
343 |
|
344 lemma enrich_file_dufs_inode2: |
|
345 "\<lbrakk>no_del_event s; valid s; is_file s f; f \<notin> init_files; assoc dufs f = Some f'; |
|
346 \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> f' \<notin> current_files s; |
|
347 \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> inum_of_file s f' = None\<rbrakk> |
|
348 \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f' = Some inum" |
|
349 apply (induct s arbitrary:f f', simp) defer |
|
350 apply(frule vt_grant_os, frule vd_cons, case_tac a) |
|
351 apply (auto split:option.splits if_splits |
|
352 simp:current_files_simps current_inode_nums_simps is_file_simps |
|
353 dest:is_file_in_current is_dir_in_current) |
|
354 |
|
355 |
|
356 lemma enrich_file_dufs_sameinodes: |
|
357 "\<lbrakk>same_inodes_list s (map fst dufs); \<forall> f \<in> set (map fst dufs). f \<notin> init_files; inum \<notin> current_inode_nums s; |
|
358 distinct (map snd dufs); \<forall> f \<in> set (map snd dufs). f \<notin> current_files s; valid s\<rbrakk> |
|
359 \<Longrightarrow> same_inodes_list (enrich_file s inum dufs) (map snd dufs)" |
|
360 apply (induct s) apply (simp add:same_inodes_list_def same_inode_files_simps) |
|
361 defer |
|
362 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
363 apply (auto simp:same_inodes_list_def same_inode_files_simps) |
|
364 |
|
365 |
|
366 |
|
367 lemma enrich_dufs_fst: |
|
368 "\<lbrakk>valid s; " |
41 |
369 |
42 |
370 |
43 lemma enrich_msgq_s2ss: |
371 lemma enrich_msgq_s2ss: |
44 "" |
372 "" |
45 |
373 |