|
1 (*<*) |
|
2 theory Current_files_prop |
|
3 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop |
|
4 begin |
|
5 (*<*) |
|
6 |
|
7 context init begin |
|
8 |
|
9 lemma current_files_ndef: "f \<notin> current_files \<tau> \<Longrightarrow> inum_of_file \<tau> f = None" |
|
10 by (simp add:current_files_def) |
|
11 |
|
12 (************** file_of_proc_fd vs proc_fd_of_file *****************) |
|
13 lemma pfdof_simp1: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> (p, fd) \<in> proc_fd_of_file \<tau> f" |
|
14 by (simp add:proc_fd_of_file_def) |
|
15 |
|
16 lemma pfdof_simp2: "(p, fd) \<in> proc_fd_of_file \<tau> f \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f" |
|
17 by (simp add:proc_fd_of_file_def) |
|
18 |
|
19 lemma pfdof_simp3: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> \<forall> p' fd'. (file_of_proc_fd \<tau> p' fd' = Some f \<longrightarrow> p = p' \<and> fd = fd')" |
|
20 by (simp add:proc_fd_of_file_def, auto) |
|
21 |
|
22 lemma pfdof_simp4: "\<lbrakk>file_of_proc_fd \<tau> p' fd' = Some f; proc_fd_of_file \<tau> f = {(p, fd)}\<rbrakk> \<Longrightarrow> p' = p \<and> fd' = fd" |
|
23 by (drule pfdof_simp3, auto) |
|
24 |
|
25 end |
|
26 |
|
27 context flask begin |
|
28 |
|
29 (***************** inode number lemmas *************************) |
|
30 |
|
31 lemma iof's_im_in_cim: "inum_of_file \<tau> f = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>" |
|
32 by (auto simp add:current_inode_nums_def current_file_inums_def) |
|
33 |
|
34 lemma ios's_im_in_cim: "inum_of_socket \<tau> s = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>" |
|
35 by (case_tac s, auto simp add:current_inode_nums_def current_sock_inums_def) |
|
36 |
|
37 lemma fim_noninter_sim_aux[rule_format]: |
|
38 "\<forall> f s. inum_of_file \<tau> f = Some im \<and> inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> False" |
|
39 apply (induct \<tau>) |
|
40 apply (clarsimp simp:inum_of_file.simps inum_of_socket.simps) |
|
41 apply (drule init_inum_sock_file_noninter, simp, simp) |
|
42 apply ((rule allI|rule impI|erule conjE)+) |
|
43 apply (frule vd_cons, frule vt_grant_os, simp, case_tac a) |
|
44 apply (auto simp:inum_of_file.simps inum_of_socket.simps split:if_splits option.splits |
|
45 dest:ios's_im_in_cim iof's_im_in_cim) |
|
46 done |
|
47 |
|
48 lemma fim_noninter_sim':"\<lbrakk>inum_of_file \<tau> f = Some im; inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
49 by (auto intro:fim_noninter_sim_aux) |
|
50 |
|
51 lemma fim_noninter_sim'':"\<lbrakk>inum_of_socket \<tau> s = Some im; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
52 by (auto intro:fim_noninter_sim_aux) |
|
53 |
|
54 lemma fim_noninter_sim: "valid \<tau> \<Longrightarrow> (current_file_inums \<tau>) \<inter> (current_sock_inums \<tau>) = {}" |
|
55 by (auto simp:current_file_inums_def current_sock_inums_def intro:fim_noninter_sim_aux[rule_format]) |
|
56 |
|
57 (******************* file inum has inode tag ************************) |
|
58 |
|
59 lemma finum_has_itag_aux[rule_format]: |
|
60 "\<forall> f im. inum_of_file \<tau> f = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None" |
|
61 apply (induct \<tau>) |
|
62 apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props) |
|
63 apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a) |
|
64 apply (auto simp add:inum_of_file.simps itag_of_inum.simps os_grant.simps current_files_def |
|
65 dest:fim_noninter_sim'' split:option.splits if_splits t_socket_type.splits) |
|
66 done |
|
67 |
|
68 lemma finum_has_itag: "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag" |
|
69 by (auto dest:conjI[THEN finum_has_itag_aux]) |
|
70 |
|
71 (*********************** file inum is file itag *************************) |
|
72 |
|
73 lemma finum_has_ftag_aux[rule_format]: |
|
74 "\<forall> f tag. inum_of_file \<tau> f = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_file_dir_itag tag" |
|
75 apply (induct \<tau>) |
|
76 apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props) |
|
77 apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a) |
|
78 apply (auto simp:inum_of_file.simps os_grant.simps current_files_def itag_of_inum.simps |
|
79 split:if_splits option.splits t_socket_type.splits |
|
80 dest:ios's_im_in_cim iof's_im_in_cim) |
|
81 done |
|
82 |
|
83 lemma finum_has_ftag: |
|
84 "\<lbrakk>inum_of_file \<tau> f = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_file_dir_itag tag" |
|
85 by (auto intro:finum_has_ftag_aux) |
|
86 |
|
87 lemma finum_has_ftag': |
|
88 "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE \<or> itag_of_inum \<tau> im = Some Tag_DIR" |
|
89 apply (frule finum_has_itag, simp, erule exE, drule finum_has_ftag, simp+) |
|
90 apply (case_tac tag, auto) |
|
91 done |
|
92 |
|
93 (******************* sock inum has inode tag ************************) |
|
94 |
|
95 lemma sinum_has_itag_aux[rule_format]: |
|
96 "\<forall> s im. inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None" |
|
97 apply (induct \<tau>) |
|
98 apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps) |
|
99 apply (drule init_inumos_prop4, clarsimp) |
|
100 apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a) |
|
101 apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps |
|
102 dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim |
|
103 split:option.splits if_splits t_socket_type.splits) |
|
104 done |
|
105 |
|
106 lemma sinum_has_itag: "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag" |
|
107 by (auto dest:conjI[THEN sinum_has_itag_aux]) |
|
108 |
|
109 (********************** socket inum is socket itag **********************) |
|
110 |
|
111 lemma sinum_has_stag_aux[rule_format]: |
|
112 "\<forall> s tag. inum_of_socket \<tau> s = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_sock_itag tag" |
|
113 apply (induct \<tau>) |
|
114 apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps) |
|
115 apply (drule init_inumos_prop4, clarsimp) |
|
116 apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a) |
|
117 apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps |
|
118 dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim |
|
119 split:option.splits if_splits t_socket_type.splits) |
|
120 done |
|
121 |
|
122 lemma sinum_has_stag: "\<lbrakk>inum_of_socket \<tau> s = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_sock_itag tag" |
|
123 by (auto dest:conjI[THEN sinum_has_stag_aux]) |
|
124 |
|
125 lemma sinum_has_stag': |
|
126 "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> |
|
127 \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_UDP_SOCK \<or> itag_of_inum \<tau> im = Some Tag_TCP_SOCK" |
|
128 apply (frule sinum_has_itag, simp, erule exE) |
|
129 apply (drule sinum_has_stag, simp+, case_tac tag, simp+) |
|
130 done |
|
131 |
|
132 (************************************ 4 in 1 *************************************) |
|
133 |
|
134 lemma file_leveling: "valid \<tau> \<longrightarrow> ( |
|
135 (\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and> |
|
136 (\<forall> f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and> |
|
137 (\<forall> f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and> |
|
138 (\<forall> f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False) )" |
|
139 proof (induct \<tau>) |
|
140 case Nil |
|
141 show ?case |
|
142 apply (auto simp:inum_of_file.simps files_hung_by_del.simps is_file_def itag_of_inum.simps parent_file_in_init split:option.splits t_inode_tag.splits) |
|
143 apply (drule init_files_hung_by_del_props, simp add:init_file_has_inum) |
|
144 apply (rule init_parent_file_has_inum, simp+) |
|
145 apply (rule init_file_has_no_son', simp+) |
|
146 apply (rule init_file_hung_has_no_son, simp+) |
|
147 done |
|
148 next |
|
149 case (Cons a \<tau>) |
|
150 assume pre: "valid \<tau> \<longrightarrow> |
|
151 (\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and> |
|
152 (\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and> |
|
153 (\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and> |
|
154 (\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False)" |
|
155 show ?case |
|
156 proof |
|
157 assume cons:"valid (a # \<tau>)" |
|
158 show "(\<forall>f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None) \<and> |
|
159 (\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None) \<and> |
|
160 (\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False) \<and> |
|
161 (\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> parent f' = Some f \<longrightarrow> False)" |
|
162 proof- |
|
163 have vt: "valid \<tau>" using cons by (auto dest:vd_cons) |
|
164 have os: "os_grant \<tau> a" using cons by (auto dest:vt_grant_os) |
|
165 have fin: "\<forall>f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" using vt pre by auto |
|
166 have pin: "\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None" |
|
167 using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption) |
|
168 have fns: "\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False" |
|
169 using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption) |
|
170 have hns: "\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False" |
|
171 using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption) |
|
172 have ain: "\<forall>f' f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
173 proof |
|
174 fix f' |
|
175 show " \<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
176 proof (induct f') |
|
177 case Nil show ?case by (auto simp: no_junior_def) |
|
178 next |
|
179 case (Cons a f') |
|
180 assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
181 show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
182 proof clarify |
|
183 fix f im |
|
184 assume h1: "f \<preceq> a # f'" |
|
185 and h2: "inum_of_file \<tau> (a # f') = Some im" |
|
186 show "\<exists>y. inum_of_file \<tau> f = Some y" |
|
187 proof- |
|
188 have h3: "\<exists> y. inum_of_file \<tau> f' = Some y" |
|
189 proof- |
|
190 have "parent (a # f') = Some f'" by simp |
|
191 hence "\<exists> y. inum_of_file \<tau> f' = Some y" using pin h2 by blast |
|
192 with h1 show ?thesis by simp |
|
193 qed |
|
194 from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def) |
|
195 moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp |
|
196 moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h3 by simp |
|
197 moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 by simp |
|
198 ultimately show ?thesis by auto |
|
199 qed |
|
200 qed |
|
201 qed |
|
202 qed |
|
203 |
|
204 have fin': "\<And> f. f \<in> files_hung_by_del \<tau> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" using fin by auto |
|
205 have pin': "\<And> f pf im. \<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'" |
|
206 using pin by auto |
|
207 have fns': "\<And> f f' im. \<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False" using fns by auto |
|
208 have fns'': "\<And> f f' im im'. \<lbrakk>itag_of_inum \<tau> im = Some Tag_FILE; inum_of_file \<tau> f = Some im; parent f' = Some f; inum_of_file \<tau> f' = Some im'\<rbrakk> \<Longrightarrow> False" |
|
209 by (rule_tac f = f and f' = f' in fns', auto simp:is_file_def) |
|
210 have hns': "\<And> f f' im. \<lbrakk>f \<in> files_hung_by_del \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False" using hns by auto |
|
211 have ain': "\<And> f f' im. \<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'" using ain by auto |
|
212 have dns': "\<And> f f' im. \<lbrakk>dir_is_empty \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False" |
|
213 apply (auto simp:dir_is_empty_def current_files_def is_dir_def split:option.splits) |
|
214 by (erule_tac x = f' in allE, simp add:noJ_Anc parent_is_ancen, drule parent_is_parent, simp+) |
|
215 |
|
216 have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None" |
|
217 apply (clarify, case_tac a) using os fin |
|
218 apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def is_file_def |
|
219 split:if_splits option.splits) |
|
220 done |
|
221 moreover |
|
222 have "\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None" |
|
223 apply (clarify, case_tac a) |
|
224 using vt os pin' |
|
225 apply (auto simp:os_grant.simps current_files_def inum_of_file.simps is_file_def is_dir_def |
|
226 split:if_splits option.splits t_inode_tag.splits) |
|
227 apply (drule_tac f = pf and f' = f in hns', simp, simp, simp) |
|
228 apply (rule_tac f = list and f' = f in fns', simp add:is_file_def, simp, simp) |
|
229 apply (rule_tac f = list and f' = f in dns', simp add:is_dir_def, simp, simp) |
|
230 done |
|
231 moreover have "\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False" |
|
232 apply (clarify, case_tac a) |
|
233 using vt os fns'' cons |
|
234 apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps |
|
235 is_file_def is_dir_def |
|
236 dest:ios's_im_in_cim iof's_im_in_cim |
|
237 split:if_splits option.splits t_inode_tag.splits t_socket_type.splits) |
|
238 apply (rule_tac im = a and f = f and f' = f' in fns'', simp+) |
|
239 apply (drule_tac f = f' and pf = list in pin', simp, simp) |
|
240 done |
|
241 moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> |
|
242 parent f' = Some f \<longrightarrow> False" |
|
243 apply (clarify, case_tac a) |
|
244 using vt os hns' |
|
245 apply (auto simp:os_grant.simps current_files_def inum_of_file.simps files_hung_by_del.simps |
|
246 split:if_splits option.splits t_sock_addr.splits) |
|
247 apply (drule fns', simp+) |
|
248 done |
|
249 ultimately show ?thesis by blast |
|
250 qed |
|
251 qed |
|
252 qed |
|
253 |
|
254 (**************** hung file in current ***********************) |
|
255 |
|
256 lemma hung_file_has_inum:"\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
257 by (drule file_leveling[rule_format], blast) |
|
258 |
|
259 lemma hung_file_has_inum': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" |
|
260 by (auto dest:hung_file_has_inum) |
|
261 |
|
262 lemma hung_file_in_current: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
263 by (clarsimp simp add:current_files_def hung_file_has_inum') |
|
264 |
|
265 lemma parentf_has_inum: "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> pf \<noteq> None" |
|
266 by (drule file_leveling[rule_format], blast) |
|
267 |
|
268 lemma parentf_has_inum': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'" |
|
269 by (auto dest:parentf_has_inum) |
|
270 |
|
271 lemma parentf_in_current: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>" |
|
272 by (clarsimp simp add:current_files_def parentf_has_inum') |
|
273 |
|
274 lemma parentf_in_current': "\<lbrakk>a # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>" |
|
275 apply (subgoal_tac "parent (a # pf) = Some pf") |
|
276 by (erule parentf_in_current, simp+) |
|
277 |
|
278 lemma ancenf_has_inum_aux: "\<forall> f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
279 proof (induct f') |
|
280 case Nil show ?case by (auto simp: no_junior_def) |
|
281 next |
|
282 case (Cons a f') |
|
283 assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
284 show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
285 proof clarify |
|
286 fix f im |
|
287 assume h1: "f \<preceq> a # f'" |
|
288 and h2: "inum_of_file \<tau> (a # f') = Some im" |
|
289 and h3: "valid \<tau>" |
|
290 show "\<exists>y. inum_of_file \<tau> f = Some y" |
|
291 proof- |
|
292 have h4: "\<exists> y. inum_of_file \<tau> f' = Some y" |
|
293 proof- |
|
294 have "parent (a # f') = Some f'" by simp |
|
295 hence "\<exists> y. inum_of_file \<tau> f' = Some y" using parentf_has_inum' h2 h3 by blast |
|
296 with h1 show ?thesis by simp |
|
297 qed |
|
298 from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def) |
|
299 moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp |
|
300 moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h4 by simp |
|
301 moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 h4 by simp |
|
302 ultimately show ?thesis by auto |
|
303 qed |
|
304 qed |
|
305 qed |
|
306 |
|
307 lemma ancenf_has_inum: "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
308 by (rule ancenf_has_inum_aux[rule_format], auto) |
|
309 |
|
310 lemma ancenf_has_inum': "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'" |
|
311 by (auto dest:ancenf_has_inum) |
|
312 |
|
313 lemma ancenf_in_current: "\<lbrakk>f \<preceq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
314 by (simp add:current_files_def, erule exE, simp add:ancenf_has_inum') |
|
315 |
|
316 lemma file_has_no_son: "\<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
317 by (drule file_leveling[rule_format], blast) |
|
318 |
|
319 lemma file_has_no_son': "\<lbrakk>is_file \<tau> f; parent f' = Some f; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
320 by (simp add:current_files_def, erule exE, auto intro:file_has_no_son) |
|
321 |
|
322 lemma hung_file_no_son: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False" |
|
323 by (drule file_leveling[rule_format], blast) |
|
324 |
|
325 lemma hung_file_no_son': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; parent f' = Some f\<rbrakk> \<Longrightarrow> False" |
|
326 by (simp add:current_files_def, erule exE, auto intro:hung_file_no_son) |
|
327 |
|
328 lemma hung_file_no_des_aux: "\<forall> f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> f' \<in> current_files \<tau> \<and> f \<preceq> f' \<and> f \<noteq> f' \<longrightarrow> False" |
|
329 proof (induct f') |
|
330 case Nil |
|
331 show ?case |
|
332 by (auto simp:files_hung_by_del.simps current_files_def inum_of_file.simps no_junior_def split:if_splits option.splits) |
|
333 next |
|
334 case (Cons a pf) |
|
335 assume pre: "\<forall>f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> pf \<in> current_files \<tau> \<and> f \<preceq> pf \<and> f \<noteq> pf\<longrightarrow> False" |
|
336 show ?case |
|
337 proof clarify |
|
338 fix f |
|
339 assume h1: "f \<in> files_hung_by_del \<tau>" |
|
340 and h2: "valid \<tau>" |
|
341 and h3: "a # pf \<in> current_files \<tau>" |
|
342 and h4: "f \<preceq> a # pf" |
|
343 and h5: "f \<noteq> a # pf" |
|
344 have h6: "parent (a # pf) = Some pf" by simp |
|
345 with h2 h3 have h7: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto) |
|
346 from h4 h5 have h8: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def) |
|
347 show False |
|
348 proof (cases "f = pf") |
|
349 case True with h6 h2 h3 h1 |
|
350 show False by (auto intro!:hung_file_no_son') |
|
351 next |
|
352 case False with pre h1 h2 h7 h8 |
|
353 show False by blast |
|
354 qed |
|
355 qed |
|
356 qed |
|
357 |
|
358 lemma hung_file_no_des: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; f \<preceq> f'; f \<noteq> f'\<rbrakk> \<Longrightarrow> False" |
|
359 by (rule hung_file_no_des_aux[rule_format], blast) |
|
360 |
|
361 (* current version, dir can not be opened, so hung_files are all files |
|
362 lemma hung_file_is_leaf: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f \<or> dir_is_empty \<tau> f" |
|
363 apply (frule hung_file_has_inum', simp, erule exE) |
|
364 apply (auto simp add:is_file_def dir_is_empty_def is_dir_def dest:finum_has_itag finum_has_ftag split:option.splits if_splits t_inode_tag.splits) |
|
365 by (simp add: noJ_Anc, auto dest:hung_file_no_des) |
|
366 *) |
|
367 |
|
368 lemma hung_file_has_filetag: |
|
369 "\<lbrakk>f \<in> files_hung_by_del s; inum_of_file s f = Some im; valid s\<rbrakk> \<Longrightarrow> itag_of_inum s im = Some Tag_FILE" |
|
370 apply (induct s) |
|
371 apply (simp add:files_hung_by_del.simps) |
|
372 apply (drule init_files_hung_prop2, (erule exE)+) |
|
373 apply (drule init_filefd_prop5, clarsimp simp:is_init_file_def split:t_inode_tag.splits option.splits) |
|
374 |
|
375 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
376 apply (auto simp:files_hung_by_del.simps is_file_def is_dir_def current_files_def current_inode_nums_def |
|
377 split:if_splits option.splits t_inode_tag.splits t_socket_type.splits |
|
378 dest:hung_file_has_inum iof's_im_in_cim) |
|
379 done |
|
380 |
|
381 lemma hung_file_is_file: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f" |
|
382 apply (frule hung_file_has_inum', simp, erule exE) |
|
383 apply (drule hung_file_has_filetag, auto simp:is_file_def) |
|
384 done |
|
385 |
|
386 (*********************** 2 in 1 *********************) |
|
387 |
|
388 lemma file_of_pfd_2in1: "valid s \<Longrightarrow> ( |
|
389 (\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> inum_of_file s f \<noteq> None) \<and> |
|
390 (\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> is_file s f) )" |
|
391 proof (induct s) |
|
392 case Nil |
|
393 show ?case |
|
394 by (auto dest:init_filefd_valid simp:is_file_def) |
|
395 next |
|
396 case (Cons e s) |
|
397 hence vd_e: "valid (e # s)" and vd_s: "valid s" and os: "os_grant s e" |
|
398 and pfd: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> inum_of_file s f \<noteq> None" |
|
399 and isf: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> is_file s f" |
|
400 by (auto dest:vd_cons vt_grant_os) |
|
401 from pfd have pfd': "\<And> p fd f. inum_of_file s f = None \<Longrightarrow> file_of_proc_fd s p fd \<noteq> Some f" |
|
402 by (rule_tac notI, drule_tac pfd, simp) |
|
403 |
|
404 have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> inum_of_file (e # s) f \<noteq> None" |
|
405 apply (case_tac e) using os |
|
406 apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def |
|
407 dir_is_empty_def is_file_def is_dir_def |
|
408 split:if_splits option.splits dest:pfd) |
|
409 apply (simp add:pfdof_simp3)+ |
|
410 apply (simp add:proc_fd_of_file_def) |
|
411 apply (drule isf, simp add:is_file_def split:t_inode_tag.splits) |
|
412 done |
|
413 moreover |
|
414 have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> is_file (e # s) f" |
|
415 apply (case_tac e) using os |
|
416 apply (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits |
|
417 dest:pfd isf iof's_im_in_cim |
|
418 simp:is_file_def is_dir_def dir_is_empty_def current_files_def) |
|
419 apply (simp add:pfdof_simp3)+ |
|
420 apply (simp add:proc_fd_of_file_def) |
|
421 done |
|
422 ultimately show ?case by auto |
|
423 qed |
|
424 |
|
425 |
|
426 (************** file_of_proc_fd in current ********************) |
|
427 |
|
428 lemma file_of_pfd_imp_inode': "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
429 by (drule file_of_pfd_2in1, blast) |
|
430 |
|
431 lemma file_of_pfd_imp_inode: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" |
|
432 by (auto dest!:file_of_pfd_imp_inode') |
|
433 |
|
434 lemma file_of_pfd_in_current: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
435 by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def) |
|
436 |
|
437 |
|
438 (*************** file_of_proc_fd is file *********************) |
|
439 |
|
440 lemma file_of_pfd_is_file: |
|
441 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f" |
|
442 by (drule file_of_pfd_2in1, auto simp:is_file_def) |
|
443 |
|
444 lemma file_of_pfd_is_file': |
|
445 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
446 by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
|
447 |
|
448 lemma file_of_pfd_is_file_tag: |
|
449 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE" |
|
450 by (drule file_of_pfd_is_file, auto simp:is_file_def split:option.splits t_inode_tag.splits) |
|
451 |
|
452 (************** parent file / ancestral file is dir *******************) |
|
453 |
|
454 lemma parentf_is_dir_aux: "\<forall> f pf. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<and> inum_of_file \<tau> pf = Some ipm \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR" |
|
455 apply (induct \<tau>) |
|
456 apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_parent_file_is_dir') |
|
457 apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a) |
|
458 apply (auto simp:inum_of_file.simps itag_of_inum.simps os_grant.simps |
|
459 current_files_def is_dir_def is_file_def |
|
460 dest: ios's_im_in_cim iof's_im_in_cim |
|
461 split:if_splits option.splits t_sock_addr.splits t_inode_tag.splits t_socket_type.splits) |
|
462 apply (drule parentf_has_inum', simp, simp, simp)+ |
|
463 done |
|
464 |
|
465 lemma parentf_has_dirtag: |
|
466 "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; inum_of_file \<tau> pf = Some ipm; valid \<tau>\<rbrakk> |
|
467 \<Longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR" |
|
468 by (auto intro:parentf_is_dir_aux[rule_format]) |
|
469 |
|
470 lemma parentf_is_dir': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf" |
|
471 apply (frule parentf_has_inum', simp+, erule exE, simp add:is_dir_def split:t_inode_tag.splits option.splits) |
|
472 by (auto dest:parentf_has_dirtag) |
|
473 |
|
474 lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf" |
|
475 by (clarsimp simp:current_files_def parentf_is_dir') |
|
476 |
|
477 lemma parentf_is_dir'': "\<lbrakk>f # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf" |
|
478 by (auto intro!:parentf_is_dir) |
|
479 |
|
480 lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f" |
|
481 proof (induct f') |
|
482 case Nil show ?case |
|
483 by (auto simp:current_files_def no_junior_def) |
|
484 next |
|
485 case (Cons a pf) |
|
486 assume pre: "\<forall>f. f \<preceq> pf \<and> f \<noteq> pf \<and> pf \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f" |
|
487 show ?case |
|
488 proof clarify |
|
489 fix f |
|
490 assume h1: "f \<preceq> a # pf" |
|
491 and h2: "f \<noteq> a # pf" |
|
492 and h3: "a # pf \<in> current_files \<tau>" |
|
493 and h4: "valid \<tau>" |
|
494 have h5: "parent (a # pf) = Some pf" by simp |
|
495 with h3 h4 have h6: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto) |
|
496 from h1 h2 have h7: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def) |
|
497 show "is_dir \<tau> f" |
|
498 proof (cases "f = pf") |
|
499 case True with h3 h4 h5 show "is_dir \<tau> f" by (drule_tac parentf_is_dir, auto) |
|
500 next |
|
501 case False with pre h6 h7 h4 show "is_dir \<tau> f" by blast |
|
502 qed |
|
503 qed |
|
504 qed |
|
505 |
|
506 lemma ancenf_is_dir: "\<lbrakk>f \<preceq> f'; f \<noteq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> f" |
|
507 by (auto intro:ancenf_is_dir_aux[rule_format]) |
|
508 |
|
509 (************* rebuild current_files simpset ***********************) |
|
510 |
|
511 lemma current_files_nil: "current_files [] = init_files" |
|
512 apply (simp add:current_files_def inum_of_file.simps) |
|
513 by (auto dest:inof_has_file_tag init_file_has_inum) |
|
514 |
|
515 lemma current_files_open: "current_files (Open p f flags fd (Some i) # \<tau>) = insert f (current_files \<tau>)" |
|
516 by (auto simp add:current_files_def inum_of_file.simps split:option.splits) |
|
517 |
|
518 lemma current_files_open': "current_files (Open p f flags fd None # \<tau>) = current_files \<tau>" |
|
519 by (simp add:current_files_def inum_of_file.simps split:option.splits) |
|
520 |
|
521 lemma current_files_closefd: "current_files (CloseFd p fd # \<tau>) = ( |
|
522 case (file_of_proc_fd \<tau> p fd) of |
|
523 Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>)) |
|
524 then current_files \<tau> - {f} |
|
525 else current_files \<tau>) |
|
526 | _ \<Rightarrow> current_files \<tau> )" |
|
527 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
528 |
|
529 lemma current_files_unlink: "current_files (UnLink p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then (current_files \<tau>) - {f} else current_files \<tau>)" |
|
530 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
531 |
|
532 lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = current_files \<tau> - {f}" |
|
533 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
534 |
|
535 lemma current_files_mkdir: "current_files (Mkdir p f ino # \<tau>) = insert f (current_files \<tau>)" |
|
536 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
537 |
|
538 (* |
|
539 lemma rename_renaming_decom: |
|
540 "\<lbrakk>f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f" |
|
541 apply (case_tac "f\<^isub>2 \<preceq> f", simp) |
|
542 apply (simp add:file_after_rename_def split:if_splits) |
|
543 by (frule vd_cons, frule vt_grant_os, auto simp:os_grant.simps dest!:ancenf_in_current) |
|
544 |
|
545 lemma rename_renaming_decom': |
|
546 "\<lbrakk>\<not> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f" |
|
547 by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+) |
|
548 |
|
549 lemma current_files_rename: "Rename p f\<^isub>2 f\<^isub>3 # valid \<tau> \<Longrightarrow> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> current_files \<tau>}" |
|
550 apply (frule vt_grant_os, frule vd_cons) |
|
551 apply (auto simp:current_files_def inum_of_file.simps os_grant.simps split:if_splits option.splits) |
|
552 apply (rule_tac x = x in exI, simp add:file_after_rename_def) |
|
553 apply (frule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop1', drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop5') |
|
554 apply (erule_tac x = "file_before_rename f\<^isub>2 f\<^isub>3 x" in allE, simp) |
|
555 apply (rule_tac x = x in exI, simp add:file_after_rename_def) |
|
556 apply (drule_tac a = f\<^isub>3 and b = f\<^isub>2 in no_junior_conf, simp, simp) |
|
557 apply (drule_tac f = f\<^isub>3 and f' = f\<^isub>2 in ancenf_has_inum', simp, simp, simp) |
|
558 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom, simp, simp add:current_files_def, simp add:file_renaming_prop5) |
|
559 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def) |
|
560 apply (simp add:file_after_rename_def) |
|
561 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def) |
|
562 apply (simp add:file_after_rename_def) |
|
563 done |
|
564 *) |
|
565 |
|
566 lemma current_files_other: |
|
567 "\<lbrakk>\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
568 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
569 \<forall> p f. e \<noteq> UnLink p f; |
|
570 \<forall> p f. e \<noteq> Rmdir p f; |
|
571 \<forall> p f i. e \<noteq> Mkdir p f i\<rbrakk> \<Longrightarrow> current_files (e # \<tau>) = current_files \<tau>" |
|
572 by (case_tac e, auto simp:current_files_def inum_of_file.simps) |
|
573 |
|
574 lemmas current_files_simps = current_files_nil current_files_open current_files_open' |
|
575 current_files_closefd current_files_unlink current_files_rmdir |
|
576 current_files_mkdir current_files_other |
|
577 |
|
578 |
|
579 (******************** is_file simpset *********************) |
|
580 |
|
581 lemma is_file_open: |
|
582 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
|
583 is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))" |
|
584 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
585 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
586 split:if_splits option.splits t_inode_tag.splits |
|
587 simp:is_file_def current_files_def) |
|
588 done |
|
589 |
|
590 lemma is_file_closefd: |
|
591 "valid (CloseFd p fd # s) \<Longrightarrow> is_file (CloseFd p fd # s) = ( |
|
592 case (file_of_proc_fd s p fd) of |
|
593 Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s)) |
|
594 then (is_file s) (f := False) |
|
595 else is_file s) |
|
596 | _ \<Rightarrow> is_file s )" |
|
597 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
598 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
599 split:if_splits option.splits t_inode_tag.splits |
|
600 simp:is_file_def) |
|
601 done |
|
602 |
|
603 lemma is_file_unlink: |
|
604 "valid (UnLink p f # s) \<Longrightarrow> is_file (UnLink p f # s) = ( |
|
605 if (proc_fd_of_file s f = {}) then (is_file s) (f := False) else is_file s)" |
|
606 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
607 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
608 split:if_splits option.splits t_inode_tag.splits |
|
609 simp:is_file_def) |
|
610 done |
|
611 |
|
612 lemma is_file_other: |
|
613 "\<lbrakk>valid (e # \<tau>); |
|
614 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
615 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
616 \<forall> p f. e \<noteq> UnLink p f\<rbrakk> \<Longrightarrow> is_file (e # \<tau>) = is_file \<tau>" |
|
617 apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e) |
|
618 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
619 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
620 simp:is_file_def dir_is_empty_def is_dir_def current_files_def) |
|
621 done |
|
622 |
|
623 lemma file_dir_conflict: "\<lbrakk>is_file s f; is_dir s f\<rbrakk> \<Longrightarrow> False" |
|
624 by (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
|
625 |
|
626 lemma is_file_not_dir: "is_file s f \<Longrightarrow> \<not> is_dir s f" |
|
627 by (rule notI, erule file_dir_conflict, simp) |
|
628 |
|
629 lemma is_dir_not_file: "is_dir s f \<Longrightarrow> \<not> is_file s f" |
|
630 by (rule notI, erule file_dir_conflict, simp) |
|
631 |
|
632 lemmas is_file_simps = is_file_nil is_file_open is_file_closefd is_file_unlink is_file_other |
|
633 |
|
634 (********* is_dir simpset **********) |
|
635 |
|
636 lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)" |
|
637 apply (frule vd_cons, drule vt_grant_os, rule_tac ext) |
|
638 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
639 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
640 simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) |
|
641 done |
|
642 |
|
643 lemma is_dir_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> is_dir (Rmdir p f # s) = (is_dir s) (f := False)" |
|
644 apply (frule vd_cons, drule vt_grant_os, rule_tac ext) |
|
645 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
646 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
647 simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) |
|
648 done |
|
649 |
|
650 lemma is_dir_other: |
|
651 "\<lbrakk>valid (e # s); |
|
652 \<forall> p f. e \<noteq> Rmdir p f; |
|
653 \<forall> p f i. e \<noteq> Mkdir p f i\<rbrakk> \<Longrightarrow> is_dir (e # s) = is_dir s" |
|
654 apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e) |
|
655 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
656 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
657 simp:is_file_def dir_is_empty_def is_dir_def current_files_def) |
|
658 apply (drule file_of_pfd_is_file, simp) |
|
659 apply (simp add:is_file_def split:t_inode_tag.splits option.splits) |
|
660 done |
|
661 |
|
662 lemmas is_dir_simps = is_dir_nil is_dir_mkdir is_dir_rmdir is_dir_other |
|
663 |
|
664 (*********** no root dir involved ***********) |
|
665 |
|
666 lemma root_is_dir: "valid s \<Longrightarrow> is_dir s []" |
|
667 apply (induct s, simp add:is_dir_nil root_is_init_dir) |
|
668 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
669 apply (auto simp:is_dir_simps) |
|
670 done |
|
671 |
|
672 lemma root_is_dir': "\<lbrakk>is_file s []; valid s\<rbrakk> \<Longrightarrow> False" |
|
673 apply (drule root_is_dir) |
|
674 apply (erule file_dir_conflict, simp) |
|
675 done |
|
676 |
|
677 lemma noroot_execve: |
|
678 "valid (Execve p f fds # s) \<Longrightarrow> f \<noteq> []" |
|
679 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
680 |
|
681 lemma noroot_execve': |
|
682 "valid (Execve p [] fds # s) \<Longrightarrow> False" |
|
683 by (drule noroot_execve, simp) |
|
684 |
|
685 lemma noroot_open: |
|
686 "valid (Open p f flags fd opt # s) \<Longrightarrow> f \<noteq> []" |
|
687 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir' split:option.splits) |
|
688 |
|
689 lemma noroot_open': |
|
690 "valid (Open p [] flags fd opt # s) \<Longrightarrow> False" |
|
691 by (drule noroot_open, simp) |
|
692 |
|
693 lemma noroot_filefd': |
|
694 "\<lbrakk>file_of_proc_fd s p fd = Some []; valid s\<rbrakk> \<Longrightarrow> False" |
|
695 apply (induct s arbitrary:p, simp) |
|
696 apply (drule init_filefd_prop5, erule root_is_init_dir') |
|
697 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
698 apply (auto split:if_splits option.splits dest!:root_is_dir') |
|
699 done |
|
700 |
|
701 lemma noroot_filefd: |
|
702 "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> f \<noteq> []" |
|
703 by (rule notI, simp, erule noroot_filefd', simp) |
|
704 |
|
705 lemma noroot_unlink: |
|
706 "valid (UnLink p f # s) \<Longrightarrow> f \<noteq> []" |
|
707 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
708 |
|
709 lemma noroot_unlink': |
|
710 "valid (UnLink p [] # s) \<Longrightarrow> False" |
|
711 by (drule noroot_unlink, simp) |
|
712 |
|
713 lemma noroot_rmdir: |
|
714 "valid (Rmdir p f # s) \<Longrightarrow> f \<noteq> []" |
|
715 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
716 |
|
717 lemma noroot_rmdir': |
|
718 "valid (Rmdir p [] # s) \<Longrightarrow> False" |
|
719 by (drule noroot_rmdir, simp) |
|
720 |
|
721 lemma noroot_mkdir: |
|
722 "valid (Mkdir p f inum # s) \<Longrightarrow> f \<noteq> []" |
|
723 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
724 |
|
725 lemma noroot_mkdir': |
|
726 "valid (Mkdir p [] inum # s) \<Longrightarrow> False" |
|
727 by (drule noroot_mkdir, simp) |
|
728 |
|
729 lemma noroot_truncate: |
|
730 "valid (Truncate p f len # s) \<Longrightarrow> f \<noteq> []" |
|
731 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
732 |
|
733 lemma noroot_truncate': |
|
734 "valid (Truncate p [] len # s) \<Longrightarrow> False" |
|
735 by (drule noroot_truncate, simp) |
|
736 |
|
737 lemmas noroot_events = noroot_execve noroot_open noroot_filefd noroot_unlink noroot_rmdir |
|
738 noroot_mkdir noroot_truncate |
|
739 |
|
740 lemmas noroot_events' = noroot_execve' noroot_open' noroot_filefd' noroot_unlink' noroot_rmdir' |
|
741 noroot_mkdir' noroot_truncate' |
|
742 |
|
743 |
|
744 lemma is_file_in_current: |
|
745 "is_file s f \<Longrightarrow> f \<in> current_files s" |
|
746 by (auto simp:is_file_def current_files_def split:option.splits) |
|
747 |
|
748 lemma is_dir_in_current: |
|
749 "is_dir s f \<Longrightarrow> f \<in> current_files s" |
|
750 by (auto simp:is_dir_def current_files_def split:option.splits) |
|
751 |
|
752 |
|
753 (* simpset for same_inode_files: Current_files_prop.thy *) |
|
754 (* |
|
755 lemma same_inode_files_nil: |
|
756 "same_inode_files [] = init_same_inode_files" |
|
757 by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil) |
|
758 |
|
759 lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>" |
|
760 by (auto simp add:current_inode_nums_def current_file_inums_def) |
|
761 |
|
762 lemma same_inode_files_open: |
|
763 "valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'. |
|
764 if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')" |
|
765 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
766 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits |
|
767 dest:iof's_im_in_cim iof's_im_in_cim') |
|
768 apply (drule is_file_in_current) |
|
769 apply (simp add:current_files_def) |
|
770 done |
|
771 |
|
772 lemma same_inode_files_linkhard: |
|
773 "valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'. |
|
774 if (f' = f \<or> f' \<in> same_inode_files s oldf) |
|
775 then same_inode_files s oldf \<union> {f} |
|
776 else same_inode_files s f')" |
|
777 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
778 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits |
|
779 dest:iof's_im_in_cim iof's_im_in_cim') |
|
780 apply (drule is_file_in_current) |
|
781 apply (simp add:current_files_def is_file_def) |
|
782 apply (simp add:is_file_def) |
|
783 done |
|
784 |
|
785 lemma inum_of_file_none_prop: |
|
786 "\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s" |
|
787 by (simp add:current_files_def) |
|
788 |
|
789 lemma same_inode_files_closefd: |
|
790 "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> |
|
791 same_inode_files (CloseFd p fd # s) f' = ( |
|
792 case (file_of_proc_fd s p fd) of |
|
793 Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s)) |
|
794 then same_inode_files s f' - {f} |
|
795 else same_inode_files s f' ) |
|
796 | None \<Rightarrow> same_inode_files s f' )" |
|
797 apply (frule vt_grant_os, frule vd_cons) |
|
798 apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd |
|
799 split:if_splits option.splits |
|
800 dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop) |
|
801 done |
|
802 |
|
803 lemma same_inode_files_unlink: |
|
804 "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> |
|
805 \<Longrightarrow> same_inode_files (UnLink p f # s) f' = ( |
|
806 if (proc_fd_of_file s f = {}) |
|
807 then same_inode_files s f' - {f} |
|
808 else same_inode_files s f')" |
|
809 apply (frule vt_grant_os, frule vd_cons) |
|
810 apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink |
|
811 split:if_splits option.splits |
|
812 dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop) |
|
813 done |
|
814 |
|
815 lemma same_inode_files_mkdir: |
|
816 "valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)" |
|
817 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
818 apply (auto simp:same_inode_files_def is_file_simps current_files_simps |
|
819 split:if_splits option.splits |
|
820 dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current) |
|
821 apply (simp add:current_files_def is_file_def) |
|
822 done |
|
823 |
|
824 lemma same_inode_files_other: |
|
825 "\<lbrakk>valid (e # s); |
|
826 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
827 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
828 \<forall> p f. e \<noteq> UnLink p f; |
|
829 \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s) = same_inode_files s" |
|
830 apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e) |
|
831 apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def |
|
832 split:if_splits option.splits |
|
833 dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir) |
|
834 apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+ |
|
835 done |
|
836 |
|
837 lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard |
|
838 same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other |
|
839 |
|
840 lemma same_inode_files_prop1: |
|
841 "f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s" |
|
842 by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits) |
|
843 |
|
844 lemma same_inode_files_prop2: |
|
845 "\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''" |
|
846 by (auto dest:same_inode_files_prop1) |
|
847 |
|
848 lemma same_inode_files_prop3: |
|
849 "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''" |
|
850 apply (rule notI) |
|
851 apply (simp add:same_inode_files_def is_file_def is_dir_def |
|
852 split:if_splits option.splits t_inode_tag.splits) |
|
853 done |
|
854 |
|
855 lemma same_inode_files_prop4: |
|
856 "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f" |
|
857 by (auto simp:same_inode_files_def split:if_splits) |
|
858 |
|
859 lemma same_inode_files_prop5: |
|
860 "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'" |
|
861 by (auto simp:same_inode_files_def is_file_def split:if_splits) |
|
862 |
|
863 lemma same_inode_files_prop6: |
|
864 "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f" |
|
865 by (auto simp:same_inode_files_def is_file_def split:if_splits) |
|
866 |
|
867 lemma same_inode_files_prop7: |
|
868 "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'" |
|
869 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits) |
|
870 |
|
871 lemma same_inode_files_prop8: |
|
872 "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f" |
|
873 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits) |
|
874 *) |
|
875 |
|
876 end |
|
877 |
|
878 end |