1
+ − 1
(*<*)
+ − 2
theory Init_prop
+ − 3
imports Main OS_type_def Flask Flask_type Static_type Static
+ − 4
begin
+ − 5
(*>*)
+ − 6
+ − 7
context init begin
+ − 8
+ − 9
lemma init_files_prop1: "init_inum_of_file f = Some im \<Longrightarrow> f \<in> init_files"
+ − 10
by (simp add:inof_has_file_tag)
+ − 11
+ − 12
lemma init_files_prop2: "finite init_files"
+ − 13
by (simp add:init_finite_sets)
+ − 14
+ − 15
lemma init_files_prop3: "f \<in> init_files \<Longrightarrow> init_inum_of_file f \<noteq> None"
+ − 16
by (auto dest:init_file_has_inum)
+ − 17
+ − 18
lemma init_files_prop4: "(f \<in> init_files) = (f \<in> current_files [])"
+ − 19
apply (simp add:current_files_def, rule iffI)
+ − 20
using init_files_prop1 init_files_prop3 by auto
+ − 21
+ − 22
lemmas init_files_props = init_file_has_inum init_files_prop1 init_files_prop2 init_files_prop3 init_files_prop4
+ − 23
+ − 24
lemma init_inumof_prop1: "init_inum_of_file f = Some im \<Longrightarrow> \<exists> tag. init_itag_of_inum im = Some tag"
+ − 25
by (auto dest:inof_has_file_tag)
+ − 26
+ − 27
lemma init_inumof_prop2: "init_inum_of_file f = Some im \<Longrightarrow> init_itag_of_inum im \<noteq> None"
+ − 28
by (auto dest:inof_has_file_tag)
+ − 29
+ − 30
lemma init_inumof_prop3: "\<lbrakk>init_inum_of_file f = Some im; init_itag_of_inum im = Some tag\<rbrakk> \<Longrightarrow> is_file_dir_itag tag"
+ − 31
by (auto dest:inof_has_file_tag)
+ − 32
+ − 33
lemmas init_inum_of_file_props = init_files_prop1 init_inumof_prop1 init_inumof_prop2 init_inumof_prop3
+ − 34
+ − 35
lemma init_inumos_prop1: "init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets"
+ − 36
by (auto dest:inos_has_sock_tag)
+ − 37
+ − 38
lemma init_inumos_prop2: "init_inum_of_socket s = Some im \<Longrightarrow> init_itag_of_inum im = Some Tag_TCP_SOCK \<or> init_itag_of_inum im = Some Tag_UDP_SOCK"
+ − 39
apply (auto dest!:inos_has_sock_tag)
+ − 40
apply (case_tac tag, simp+)
+ − 41
done
+ − 42
+ − 43
lemma init_inumos_prop3: "init_inum_of_socket s = Some im \<Longrightarrow> init_itag_of_inum im \<noteq> None"
+ − 44
by (auto dest:inos_has_sock_tag)
+ − 45
+ − 46
lemma init_inumos_prop4: "init_inum_of_socket s = Some im \<Longrightarrow> \<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag"
+ − 47
by (auto dest!:inos_has_sock_tag)
+ − 48
+ − 49
lemmas init_inum_of_socket_props = init_inumos_prop1 init_inumos_prop2 init_inumos_prop3 init_inumos_prop4
+ − 50
+ − 51
lemma init_sockets_prop1: "(p, fd) \<in> init_sockets \<Longrightarrow> p \<in> init_procs"
+ − 52
by (auto dest: init_socket_has_inode)
+ − 53
+ − 54
lemma init_sockets_prop2: "(p, fd) \<in> init_sockets \<Longrightarrow> fd \<in> init_fds_of_proc p"
+ − 55
by (auto dest:init_socket_has_inode)
+ − 56
+ − 57
lemma init_sockets_prop3: "s \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket s = Some im"
+ − 58
by (case_tac s, auto dest:init_socket_has_inode)
+ − 59
+ − 60
lemma init_sockets_prop4: "s \<in> init_sockets \<Longrightarrow> init_inum_of_socket s \<noteq> None"
+ − 61
by (simp add:init_sockets_prop3)
+ − 62
+ − 63
lemma init_sockets_prop5: "s \<in> init_sockets = (s \<in> current_sockets [])"
+ − 64
apply (simp add:current_sockets_def, rule iffI)
+ − 65
using init_sockets_prop4 inos_has_sock_tag apply auto
+ − 66
apply (case_tac s, auto)
+ − 67
done
+ − 68
+ − 69
lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5
+ − 70
+ − 71
lemma is_init_file_prop1: "is_init_file f = (f \<in> init_files \<and> is_file [] f)"
+ − 72
by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits)
+ − 73
+ − 74
lemma is_init_file_prop2: "is_init_file f = (init_alive (O_file f))"
+ − 75
by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits)
+ − 76
+ − 77
lemmas is_init_file_props = is_init_file_prop1 is_init_file_prop2
+ − 78
+ − 79
lemma is_init_dir_prop1: "is_init_dir f = (f \<in> init_files \<and> is_dir [] f)"
+ − 80
by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)
+ − 81
+ − 82
lemma is_init_dir_prop2: "is_init_dir f = (init_alive (O_dir f))"
+ − 83
by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)
+ − 84
+ − 85
lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2
+ − 86
2
+ − 87
lemma is_file_nil: "is_file [] = is_init_file"
+ − 88
by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits)
+ − 89
+ − 90
lemma is_dir_nil: "is_dir [] = is_init_dir"
+ − 91
by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)
+ − 92
1
+ − 93
lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)"
+ − 94
apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props
+ − 95
dest:init_socket_has_inode split:option.splits)
+ − 96
done
+ − 97
+ − 98
lemma is_init_udp_sock_prop2: "is_init_udp_sock s = (init_alive (O_udp_sock s))"
+ − 99
apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props
+ − 100
dest:init_socket_has_inode split:option.splits)
+ − 101
done
+ − 102
+ − 103
lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2
+ − 104
+ − 105
lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)"
+ − 106
apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props
+ − 107
dest:init_socket_has_inode split:option.splits)
+ − 108
done
+ − 109
+ − 110
lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s = (init_alive (O_tcp_sock s))"
+ − 111
apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props
+ − 112
dest:init_socket_has_inode split:option.splits)
+ − 113
done
+ − 114
+ − 115
lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2
+ − 116
+ − 117
+ − 118
lemma init_parent_file_prop1:
+ − 119
"\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"
+ − 120
apply (frule parent_file_in_init, simp, frule_tac f = pf in init_files_prop3)
+ − 121
apply (clarsimp, drule_tac im = y in init_parentf_is_dir, simp+)
+ − 122
by (simp add:is_init_dir_def)
+ − 123
+ − 124
lemma init_parent_file_prop1':
+ − 125
"a # f \<in> init_files \<Longrightarrow> is_init_dir f"
+ − 126
by (rule_tac pf = f in init_parent_file_prop1, auto)
+ − 127
+ − 128
lemma init_parent_file_prop2:
+ − 129
"\<lbrakk>parent f = Some pf; is_init_file f\<rbrakk> \<Longrightarrow> is_init_dir pf"
+ − 130
by (rule init_parent_file_prop1, simp, simp add: is_init_file_props)
+ − 131
+ − 132
lemma init_parent_file_prop2':
+ − 133
"is_init_file (f#pf) \<Longrightarrow> is_init_dir pf"
+ − 134
apply (rule init_parent_file_prop2)
+ − 135
by auto
+ − 136
+ − 137
lemma init_parent_file_prop3:
+ − 138
"\<lbrakk>parent f = Some pf; is_init_dir f\<rbrakk> \<Longrightarrow> is_init_dir pf"
+ − 139
by (rule init_parent_file_prop1, simp, simp add: is_init_dir_props)
+ − 140
+ − 141
lemma init_parent_file_prop3':
+ − 142
"is_init_dir (f#pf) \<Longrightarrow> is_init_dir pf"
+ − 143
apply (rule init_parent_file_prop3)
+ − 144
by auto
+ − 145
+ − 146
lemma parent_file_in_init': "a # f \<in> init_files \<Longrightarrow> f \<in> init_files"
+ − 147
by (subgoal_tac "parent (a # f) = Some f", drule parent_file_in_init, auto)
+ − 148
+ − 149
lemmas init_parent_file_props = parent_file_in_init init_parent_file_prop1 parent_file_in_init' init_parent_file_prop1' init_parent_file_prop2 init_parent_file_prop2' init_parent_file_prop3 init_parent_file_prop3'
+ − 150
+ − 151
lemma root_in_filesystem: "[] \<in> init_files"
+ − 152
using init_files_prop1 root_is_dir by auto
+ − 153
+ − 154
lemma root_is_init_dir: "is_init_dir []"
+ − 155
using root_is_dir
+ − 156
by (auto simp add:is_init_dir_def split:option.splits)
+ − 157
+ − 158
lemma root_is_init_dir': "is_init_file [] \<Longrightarrow> False"
+ − 159
using root_is_dir
+ − 160
by (auto simp:is_init_file_def split:option.splits)
+ − 161
+ − 162
+ − 163
lemma init_files_hung_prop1: "f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files"
+ − 164
by (auto dest:init_files_hung_valid)
+ − 165
+ − 166
lemma init_files_hung_prop2: "f \<in> init_files_hung_by_del \<Longrightarrow> \<exists> p fd. init_file_of_proc_fd p fd = Some f"
+ − 167
by (auto dest:init_files_hung_valid)
+ − 168
+ − 169
lemmas init_files_hung_by_del_props = init_files_hung_prop1 init_files_hung_prop2 init_files_hung_valid'
+ − 170
+ − 171
+ − 172
lemma init_fds_of_proc_prop1: "fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs"
+ − 173
by (auto dest!:init_procfds_valid)
+ − 174
+ − 175
lemma init_fds_of_proc_prop2: "fd \<in> init_fds_of_proc p \<Longrightarrow> (\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets"
+ − 176
by (auto dest:init_procfds_valid)
+ − 177
+ − 178
lemmas init_fds_of_proc_props = init_fds_of_proc_prop1 init_fds_of_proc_prop2
+ − 179
+ − 180
lemma init_filefd_prop1: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> f \<in> init_files"
+ − 181
by (auto dest!:init_filefd_valid intro:init_files_prop1)
+ − 182
+ − 183
lemma init_filefd_prop2: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> p \<in> init_procs"
+ − 184
by (auto dest:init_filefd_valid)
+ − 185
+ − 186
lemma init_filefd_prop3: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p"
+ − 187
by (auto dest:init_filefd_valid)
+ − 188
+ − 189
lemma init_filefd_prop4: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<exists> flags. init_oflags_of_proc_fd p fd = Some flags"
+ − 190
by (auto dest:init_filefd_valid)
+ − 191
+ − 192
lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f"
+ − 193
by (auto dest:init_filefd_valid simp:is_init_file_def)
+ − 194
+ − 195
lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5
+ − 196
+ − 197
lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs"
+ − 198
by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)
+ − 199
+ − 200
lemma init_oflags_prop2: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> fd \<in> init_fds_of_proc p"
+ − 201
by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)
+ − 202
+ − 203
lemmas init_oflags_of_proc_fd_props = init_oflags_prop1 init_oflags_prop2 init_fileflag_valid
+ − 204
+ − 205
(*
+ − 206
lemma init_socketstate_prop1: "s \<in> init_sockets \<Longrightarrow> init_socket_state s \<noteq> None"
+ − 207
using init_socket_has_state
+ − 208
by (case_tac s, simp add:bidirect_in_init_def)
+ − 209
+ − 210
lemma init_socketstate_prop2: "s \<in> init_sockets \<Longrightarrow> \<exists> t. init_socket_state s = Some t"
+ − 211
using init_socket_has_state
+ − 212
by (case_tac s, simp add:bidirect_in_init_def)
+ − 213
+ − 214
lemma init_socketstate_prop3: "init_socket_state s = Some t \<Longrightarrow> s \<in> init_sockets"
+ − 215
using init_socket_has_state
+ − 216
by (case_tac s, simp add:bidirect_in_init_def)
+ − 217
+ − 218
lemmas init_socket_state_props = init_socketstate_prop1 init_socketstate_prop2 init_socketstate_prop3
+ − 219
*)
+ − 220
+ − 221
lemma init_inum_sock_file_noninter: "\<lbrakk>init_inum_of_socket s = Some im; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> False"
+ − 222
apply (frule init_inumof_prop1, erule exE, drule init_inumof_prop3, simp)
+ − 223
apply (frule init_inumos_prop2)
+ − 224
apply (case_tac tag, simp+)
+ − 225
done
+ − 226
+ − 227
lemma init_parent_file_has_inum: "\<lbrakk>parent f = Some pf; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> \<exists> im. init_inum_of_file pf = Some im"
+ − 228
by (drule init_files_prop1, drule parent_file_in_init, simp, simp add:init_files_props)
+ − 229
+ − 230
lemma init_file_has_no_son': "\<lbrakk>init_itag_of_inum im = Some Tag_FILE; init_inum_of_file f = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> init_inum_of_file f' = None"
+ − 231
apply (drule init_file_no_son, simp)
+ − 232
by (case_tac "init_inum_of_file f'", auto dest:init_files_prop1)
+ − 233
+ − 234
lemma init_parent_file_is_dir': "\<lbrakk>parent f = Some pf; init_inum_of_file f = Some im; init_inum_of_file pf = Some ipm\<rbrakk> \<Longrightarrow> init_itag_of_inum ipm = Some Tag_DIR"
+ − 235
by (drule init_parentf_is_dir, auto dest:init_files_prop1)
+ − 236
+ − 237
lemma init_file_hung_has_no_son: "\<lbrakk>f \<in> init_files_hung_by_del; parent f' = Some f; init_inum_of_file f' = Some im\<rbrakk> \<Longrightarrow> False"
+ − 238
apply (frule init_files_hung_prop1, drule init_file_has_inum, erule exE)
+ − 239
apply (drule init_files_hung_valid', simp)
+ − 240
apply (frule init_parent_file_is_dir', simp+)
+ − 241
apply (drule init_files_prop1)
+ − 242
apply (erule_tac x = f' in allE, simp)
+ − 243
by (case_tac f', simp_all add:no_junior_def)
+ − 244
2
+ − 245
lemma same_inode_nil_prop:
+ − 246
"same_inode_files [] f = init_same_inode_files f"
+ − 247
by (simp add:same_inode_files_def init_same_inode_files_def)
+ − 248
+ − 249
lemma init_same_inode_prop1:
+ − 250
"f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"
+ − 251
apply (simp add:init_same_inode_files_def)
+ − 252
apply (drule init_files_prop3)
+ − 253
apply (auto simp:init_files_prop1)
+ − 254
done
1
+ − 255
+ − 256
end
+ − 257
+ − 258
context flask begin
+ − 259
+ − 260
lemma init_alive_prop: "init_alive obj = alive [] obj"
+ − 261
apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props
+ − 262
is_init_udp_sock_props init_files_props init_sockets_props)
+ − 263
done
+ − 264
+ − 265
lemma init_alive_proc: "p \<in> init_procs \<Longrightarrow> init_alive (O_proc p)" by simp
+ − 266
lemma init_alive_file: "is_init_file f \<Longrightarrow> init_alive (O_file f)" by simp
+ − 267
lemma init_alive_dir: "is_init_dir f \<Longrightarrow> init_alive (O_dir f)" by simp
+ − 268
lemma init_alive_fd: "fd \<in> init_fds_of_proc p \<Longrightarrow> init_alive (O_fd p fd)" by simp
+ − 269
lemma init_alive_tcp: "is_init_tcp_sock s \<Longrightarrow> init_alive (O_tcp_sock s)" by simp
+ − 270
lemma init_alive_udp: "is_init_udp_sock s \<Longrightarrow> init_alive (O_udp_sock s)" by simp
+ − 271
lemma init_alive_node: "n \<in> init_nodes \<Longrightarrow> init_alive (O_node n)" by simp
+ − 272
lemma init_alive_shm: "h \<in> init_shms \<Longrightarrow> init_alive (O_shm h)" by simp
+ − 273
lemma init_alive_msgq: "q \<in> init_msgqs \<Longrightarrow> init_alive (O_msgq q)" by simp
+ − 274
lemma init_alive_msg: "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk>
+ − 275
\<Longrightarrow> init_alive (O_msg q m)" by simp
+ − 276
+ − 277
lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd
+ − 278
init_alive_tcp init_alive_udp init_alive_node init_alive_shm init_alive_msgq init_alive_msg
+ − 279
+ − 280
+ − 281
lemma init_file_type_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_type_of_obj (O_file f) = Some t"
+ − 282
using init_obj_has_type
+ − 283
by (auto simp:is_init_file_def split:option.splits)
+ − 284
+ − 285
lemma init_file_type_prop2: "is_init_file f \<Longrightarrow> init_type_of_obj (O_file f) \<noteq> None"
+ − 286
by (simp add:init_file_type_prop1)
+ − 287
+ − 288
lemma init_file_type_prop3: "init_type_of_obj (O_file f) = Some t \<Longrightarrow> f \<in> init_files"
+ − 289
apply (drule init_type_has_obj)
+ − 290
by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)
+ − 291
+ − 292
lemma init_file_type_prop4: "init_type_of_obj (O_file f) = Some t \<Longrightarrow> is_init_file f"
+ − 293
apply (drule init_type_has_obj)
+ − 294
by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)
+ − 295
+ − 296
lemmas init_file_types_props = init_file_type_prop1 init_file_type_prop2 init_file_type_prop3 init_file_type_prop4
+ − 297
+ − 298
lemma init_dir_type_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_type_of_obj (O_dir f) = Some t"
+ − 299
using init_obj_has_type
+ − 300
by (auto simp:is_init_dir_def split:option.splits)
+ − 301
+ − 302
lemma init_dir_type_prop2: "is_init_dir f \<Longrightarrow> init_type_of_obj (O_dir f) \<noteq> None"
+ − 303
by (simp add:init_dir_type_prop1)
+ − 304
+ − 305
lemma init_dir_type_prop3: "init_type_of_obj (O_dir f) = Some t \<Longrightarrow> f \<in> init_files"
+ − 306
apply (drule init_type_has_obj)
+ − 307
by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)
+ − 308
+ − 309
lemma init_dir_type_prop4: "init_type_of_obj (O_dir f) = Some t \<Longrightarrow> is_init_dir f"
+ − 310
apply (drule init_type_has_obj)
+ − 311
by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)
+ − 312
+ − 313
lemmas init_dir_types_props = init_dir_type_prop1 init_dir_type_prop2 init_dir_type_prop3 init_dir_type_prop4
+ − 314
+ − 315
lemma init_procrole_prop1: "init_role_of_proc p = Some r \<Longrightarrow> p \<in> init_procs"
+ − 316
using init_proc_has_role
+ − 317
by (auto simp:bidirect_in_init_def)
+ − 318
+ − 319
lemma init_procrole_prop2: "p \<in> init_procs \<Longrightarrow> \<exists> r. init_role_of_proc p = Some r"
+ − 320
using init_proc_has_role
+ − 321
by (auto simp:bidirect_in_init_def)
+ − 322
+ − 323
lemma init_procrole_prop3: "p \<in> init_procs \<Longrightarrow> init_role_of_proc p \<noteq> None"
+ − 324
using init_proc_has_role
+ − 325
by (auto simp:bidirect_in_init_def)
+ − 326
+ − 327
lemmas init_role_of_proc_props = init_procrole_prop1 init_procrole_prop2 init_procrole_prop3
+ − 328
+ − 329
lemma init_file_user_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_user_of_obj (O_file f) = Some t"
+ − 330
apply (simp only: is_init_file_prop2)
+ − 331
by (drule init_obj_has_user, auto)
+ − 332
+ − 333
lemma init_file_user_prop2: "is_init_file f \<Longrightarrow> init_user_of_obj (O_file f) \<noteq> None"
+ − 334
by (simp add:init_file_user_prop1)
+ − 335
+ − 336
lemma init_file_user_prop3: "init_user_of_obj (O_file f) = Some t \<Longrightarrow> f \<in> init_files"
+ − 337
apply (drule init_user_has_obj)
+ − 338
by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)
+ − 339
+ − 340
lemma init_file_user_prop4: "init_user_of_obj (O_file f) = Some t \<Longrightarrow> is_init_file f"
+ − 341
apply (drule init_user_has_obj)
+ − 342
by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)
+ − 343
+ − 344
lemma init_file_user_prop5: "init_user_of_obj (O_file f) = Some u \<Longrightarrow> u \<in> init_users"
+ − 345
by (simp add:init_user_has_obj)
+ − 346
+ − 347
lemmas init_file_users_props = init_file_user_prop1 init_file_user_prop2 init_file_user_prop3 init_file_user_prop4 init_file_user_prop5
+ − 348
+ − 349
lemma init_dir_user_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_user_of_obj (O_dir f) = Some t"
+ − 350
apply (simp only: is_init_dir_prop2)
+ − 351
by (drule init_obj_has_user, auto)
+ − 352
+ − 353
lemma init_dir_user_prop2: "is_init_dir f \<Longrightarrow> init_user_of_obj (O_dir f) \<noteq> None"
+ − 354
by (simp add:init_dir_user_prop1)
+ − 355
+ − 356
lemma init_dir_user_prop3: "init_user_of_obj (O_dir f) = Some t \<Longrightarrow> f \<in> init_files"
+ − 357
apply (drule init_user_has_obj)
+ − 358
by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)
+ − 359
+ − 360
lemma init_dir_user_prop4: "init_user_of_obj (O_dir f) = Some t \<Longrightarrow> is_init_dir f"
+ − 361
apply (drule init_user_has_obj)
+ − 362
by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)
+ − 363
+ − 364
lemma init_dir_user_prop5: "init_user_of_obj (O_dir f) = Some u \<Longrightarrow> u \<in> init_users"
+ − 365
by (simp add:init_user_has_obj)
+ − 366
+ − 367
lemmas init_dir_users_props = init_dir_user_prop1 init_dir_user_prop2 init_dir_user_prop3 init_dir_user_prop4 init_dir_user_prop5
+ − 368
2
+ − 369
lemma init_file_dir_conflict: "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"
+ − 370
by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+ − 371
+ − 372
lemma init_file_dir_conflict1: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"
+ − 373
by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+ − 374
+ − 375
lemma init_file_dir_conflict2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"
+ − 376
by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+ − 377
1
+ − 378
end
+ − 379
2
+ − 380
context tainting begin
+ − 381
+ − 382
lemma tainted_nil_prop:
+ − 383
"(x \<in> tainted []) = (x \<in> seeds)"
+ − 384
apply (rule iffI)
+ − 385
apply (erule tainted.cases, simp+)
+ − 386
apply (erule t_init)
+ − 387
done
+ − 388
+ − 389
end
1
+ − 390
+ − 391
context tainting_s begin
+ − 392
+ − 393
lemma init_file_has_ctxt:
+ − 394
"is_init_file f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_file f) = Some sec"
+ − 395
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 396
apply (rule conjI, rule init_obj_has_user, simp add:is_init_file_props)
+ − 397
by (simp add:init_file_types_props)
+ − 398
+ − 399
lemma init_file_has_ctxt':
+ − 400
"init_sectxt_of_obj (O_file f) = None \<Longrightarrow> \<not> is_init_file f"
+ − 401
by (rule notI, drule init_file_has_ctxt, simp)
+ − 402
+ − 403
lemma init_dir_has_ctxt:
+ − 404
"is_init_dir f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_dir f) = Some sec"
+ − 405
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 406
apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+ − 407
by (simp add:init_dir_types_props)
+ − 408
+ − 409
lemma init_dir_has_ctxt':
+ − 410
"init_sectxt_of_obj (O_dir f) = None \<Longrightarrow> \<not> is_init_dir f"
+ − 411
by (rule notI, drule init_dir_has_ctxt, simp)
+ − 412
+ − 413
lemma init_proc_has_ctxt:
+ − 414
"p \<in> init_procs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_proc p) = Some sec"
+ − 415
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 416
apply (rule conjI, rule init_obj_has_user, simp)
+ − 417
apply (frule init_alive_proc, drule init_obj_has_type)
+ − 418
by (drule init_procrole_prop2, auto)
+ − 419
+ − 420
lemma init_proc_has_ctxt':
+ − 421
"init_sectxt_of_obj (O_proc p) = None \<Longrightarrow> p \<notin> init_procs"
+ − 422
by (rule notI, drule init_proc_has_ctxt, simp)
+ − 423
+ − 424
lemma init_fd_has_ctxt:
+ − 425
"fd \<in> init_fds_of_proc p \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_fd p fd) = Some sec"
+ − 426
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 427
apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+ − 428
apply (drule init_alive_intros)
+ − 429
apply (drule init_obj_has_type, clarsimp)
+ − 430
done
+ − 431
+ − 432
lemma init_fd_has_ctxt':
+ − 433
"init_sectxt_of_obj (O_fd p fd) = None \<Longrightarrow> fd \<notin> init_fds_of_proc p"
+ − 434
by (rule notI, drule init_fd_has_ctxt, simp)
+ − 435
+ − 436
lemma init_node_has_ctxt:
+ − 437
"n \<in> init_nodes \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_node n) = Some sec"
+ − 438
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 439
apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+ − 440
apply (drule init_alive_intros)
+ − 441
apply (drule init_obj_has_type, clarsimp)
+ − 442
done
+ − 443
+ − 444
lemma init_node_has_ctxt':
+ − 445
"init_sectxt_of_obj (O_node n) = None \<Longrightarrow> n \<notin> init_nodes"
+ − 446
by (rule notI, drule init_node_has_ctxt, simp)
+ − 447
+ − 448
lemma init_tcp_has_ctxt:
+ − 449
"is_init_tcp_sock s \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_tcp_sock s) = Some sec"
+ − 450
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 451
apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+ − 452
apply (drule init_alive_intros)
+ − 453
apply (drule init_obj_has_type, clarsimp)
+ − 454
done
+ − 455
+ − 456
lemma init_tcp_has_ctxt':
+ − 457
"init_sectxt_of_obj (O_tcp_sock s) = None \<Longrightarrow> \<not> is_init_tcp_sock s"
+ − 458
by (rule notI, drule init_tcp_has_ctxt, simp)
+ − 459
+ − 460
lemma init_udp_has_ctxt:
+ − 461
"is_init_udp_sock s \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_udp_sock s) = Some sec"
+ − 462
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 463
apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+ − 464
by (drule init_alive_intros, drule init_obj_has_type, clarsimp)
+ − 465
+ − 466
lemma init_udp_has_ctxt':
+ − 467
"init_sectxt_of_obj (O_udp_sock s) = None \<Longrightarrow> \<not> is_init_udp_sock s"
+ − 468
by (rule notI, drule init_udp_has_ctxt, simp)
+ − 469
+ − 470
lemma init_shm_has_ctxt:
+ − 471
"h \<in> init_shms \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_shm h) = Some sec"
+ − 472
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 473
apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+ − 474
by (drule init_alive_intros, drule init_obj_has_type, clarsimp)
+ − 475
+ − 476
lemma init_shm_has_ctxt':
+ − 477
"init_sectxt_of_obj (O_shm h) = None \<Longrightarrow> h \<notin> init_shms"
+ − 478
by (rule notI, drule init_shm_has_ctxt, simp)
+ − 479
+ − 480
lemma init_msgq_has_ctxt:
+ − 481
"q \<in> init_msgqs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msgq q) = Some sec"
+ − 482
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 483
apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+ − 484
by (drule init_alive_intros, drule init_obj_has_type, clarsimp)
+ − 485
+ − 486
lemma init_msgq_has_ctxt':
+ − 487
"init_sectxt_of_obj (O_msgq q) = None \<Longrightarrow> q \<notin> init_msgqs"
+ − 488
by (rule notI, drule init_msgq_has_ctxt, simp)
+ − 489
+ − 490
lemma init_msg_has_ctxt:
+ − 491
"\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msg q m) = Some sec"
+ − 492
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 493
apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+ − 494
by (drule init_alive_intros, simp, drule init_obj_has_type, clarsimp)
+ − 495
+ − 496
lemma init_msg_has_ctxt':
+ − 497
"init_sectxt_of_obj (O_msg q m) = None \<Longrightarrow> m \<notin> set (init_msgs_of_queue q) \<or> q \<notin> init_msgqs"
+ − 498
by (auto dest:init_msg_has_ctxt)
+ − 499
+ − 500
lemma init_rootf_has_ctxt:
+ − 501
"\<exists> sec. init_sectxt_of_obj (O_dir []) = Some sec"
+ − 502
apply (rule init_dir_has_ctxt, simp add:is_init_dir_def split:option.splits)
+ − 503
using root_is_dir by auto
+ − 504
+ − 505
lemma init_rootf_has_ctxt':
+ − 506
"init_sectxt_of_obj (O_dir []) = None \<Longrightarrow> False"
+ − 507
using init_rootf_has_ctxt by auto
+ − 508
+ − 509
lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt
+ − 510
init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt init_shm_has_ctxt init_msgq_has_ctxt
+ − 511
init_msg_has_ctxt init_rootf_has_ctxt
+ − 512
+ − 513
lemmas init_has_ctxt' = init_file_has_ctxt' init_dir_has_ctxt' init_proc_has_ctxt' init_fd_has_ctxt'
+ − 514
init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' init_shm_has_ctxt' init_msgq_has_ctxt'
+ − 515
init_msg_has_ctxt' init_rootf_has_ctxt'
+ − 516
+ − 517
lemma sec_of_root_valid:
+ − 518
"init_sectxt_of_obj (O_dir []) = Some sec_of_root"
+ − 519
using init_rootf_has_ctxt
+ − 520
by (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits)
+ − 521
+ − 522
lemma sec_of_root_is_tuple:
+ − 523
"\<exists> u t. sec_of_root = (u, R_object, t)"
+ − 524
using sec_of_root_valid
+ − 525
by (auto simp:sec_of_root_def init_sectxt_of_obj_def split:option.splits)
+ − 526
+ − 527
lemma sroot_valid:
+ − 528
"init_cf2sfile [] = Some sroot"
+ − 529
by (simp add:init_cf2sfile_def)
+ − 530
+ − 531
lemma sroot_valid':
+ − 532
"cf2sfile s [] False = Some sroot"
+ − 533
by (simp add:cf2sfile_def)
+ − 534
+ − 535
lemma init_sectxt_prop:
+ − 536
"sectxt_of_obj [] obj = init_sectxt_of_obj obj"
+ − 537
apply (auto simp:init_sectxt_of_obj_def sectxt_of_obj_def split:option.splits)
+ − 538
apply (case_tac [!] obj, simp+)
+ − 539
done
+ − 540
+ − 541
lemma init_sectxt_prop2:
+ − 542
"init_sectxt_of_obj obj = Some sec \<Longrightarrow> init_alive obj"
+ − 543
by (case_tac obj, auto simp:init_sectxt_of_obj_def split:option.splits dest:init_type_has_obj)
+ − 544
+ − 545
lemma init_dir_has_seclist:
+ − 546
"is_init_dir f \<Longrightarrow> \<exists> seclist. get_parentfs_ctxts [] f = Some seclist"
+ − 547
apply (induct f)
+ − 548
apply (simp only:get_parentfs_ctxts.simps init_sectxt_prop)
+ − 549
using init_rootf_has_ctxt apply (auto)[1]
+ − 550
apply (frule init_parent_file_prop3', simp del:get_parentfs_ctxts.simps)
+ − 551
apply (erule exE, drule init_dir_has_ctxt)
+ − 552
by (auto simp add:init_sectxt_prop)
+ − 553
+ − 554
lemma is_init_file_dir_prop1:
+ − 555
"is_init_dir f \<Longrightarrow> \<not> is_init_file f"
+ − 556
by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
+ − 557
+ − 558
lemma is_init_file_dir_prop2:
+ − 559
"is_init_file f \<Longrightarrow> \<not> is_init_dir f"
+ − 560
by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
+ − 561
+ − 562
lemma is_init_file_dir_prop3:
+ − 563
"\<lbrakk>is_init_dir f; is_init_file f\<rbrakk> \<Longrightarrow> False"
+ − 564
by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
+ − 565
+ − 566
lemma is_init_file_dir_prop4:
+ − 567
"\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"
+ − 568
by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
+ − 569
+ − 570
lemmas is_init_file_dir_props = is_init_file_dir_prop1 is_init_file_dir_prop2 is_init_file_dir_prop3 is_init_file_dir_prop4
+ − 571
+ − 572
lemma init_dir_has_sfile:
+ − 573
"is_init_dir f \<Longrightarrow> \<exists> sf. init_cf2sfile f = Some sf"
+ − 574
apply (case_tac f)
+ − 575
using init_rootf_has_ctxt apply (auto)[1]
+ − 576
apply (simp add:sec_of_root_valid sroot_valid sroot_def)
+ − 577
apply (simp, frule init_parent_file_prop3')
+ − 578
apply (frule_tac f = list in init_dir_has_seclist)
+ − 579
apply (frule_tac f = list in init_dir_has_ctxt)
+ − 580
apply (frule_tac f = "a # list" in init_dir_has_ctxt)
+ − 581
apply ((erule exE)+, case_tac sec, auto simp:init_cf2sfile_def split:option.splits)
+ − 582
by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+ − 583
+ − 584
lemma init_file_has_sfile:
+ − 585
"is_init_file f \<Longrightarrow> \<exists> sf. init_cf2sfile f = Some sf"
+ − 586
apply (case_tac f)
+ − 587
apply (simp, drule root_is_init_dir', simp)
+ − 588
apply (simp, frule init_parent_file_prop2')
+ − 589
apply (frule_tac f = list in init_dir_has_seclist)
+ − 590
apply (frule_tac f = list in init_dir_has_ctxt)
+ − 591
apply (frule_tac f = "a # list" in init_file_has_ctxt)
+ − 592
by ((erule exE)+, case_tac sec, auto simp:init_cf2sfile_def)
+ − 593
+ − 594
lemma init_shm_has_sshm:
+ − 595
"h \<in> init_shms \<Longrightarrow> \<exists> sh. init_ch2sshm h = Some sh"
+ − 596
apply (drule init_shm_has_ctxt)
+ − 597
by (auto simp add:init_ch2sshm_def)
+ − 598
+ − 599
lemma init_proc_has_sproc:
+ − 600
"p \<in> init_procs \<Longrightarrow> \<exists> sp. init_cp2sproc p = Some sp"
+ − 601
apply (frule init_proc_has_ctxt, erule exE)
+ − 602
apply (simp add:init_cp2sproc_def)
+ − 603
by (case_tac sec, simp+)
+ − 604
+ − 605
lemma init_cqm2sms_has_sms_aux:
+ − 606
"\<forall> m \<in> set ms. init_sectxt_of_obj (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. init_cqm2sms q ms = Some sms)"
+ − 607
by (induct ms, auto split:option.splits simp:init_cm2smsg_def)
+ − 608
+ − 609
lemma init_cqm2sms_has_sms:
+ − 610
"q \<in> init_msgqs \<Longrightarrow> \<exists> sms. init_cqm2sms q (init_msgs_of_queue q) = Some sms"
+ − 611
apply (rule init_cqm2sms_has_sms_aux)
+ − 612
using init_msg_has_ctxt by auto
+ − 613
+ − 614
lemma init_msgq_has_smsgq:
+ − 615
"q \<in> init_msgqs \<Longrightarrow> \<exists> sq. init_cq2smsgq q = Some sq"
+ − 616
apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)
+ − 617
apply (simp add:init_cq2smsgq_def)
+ − 618
by (case_tac sec, simp+)
+ − 619
+ − 620
lemma cf2sfile_nil_prop1:
+ − 621
"f \<in> init_files \<Longrightarrow> cf2sfile [] f (is_init_file f) = init_cf2sfile f"
+ − 622
apply (case_tac f)
+ − 623
apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
+ − 624
apply (rule notI, drule root_is_init_dir', simp)
+ − 625
apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
+ − 626
apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits
+ − 627
dest:init_file_has_inum inof_has_file_tag)
+ − 628
done
+ − 629
+ − 630
+ − 631
lemma init_sec_file_dir:
+ − 632
"\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False"
+ − 633
apply (drule init_sectxt_prop2)+
+ − 634
apply (auto intro:init_file_dir_conflict)
+ − 635
done
+ − 636
+ − 637
lemma cf2sfile_nil_prop2:
+ − 638
"f \<in> init_files \<Longrightarrow> cf2sfile [] f (\<not> is_init_file f) = None"
+ − 639
apply (case_tac f)
+ − 640
apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
+ − 641
apply (rule notI, drule root_is_init_dir', simp)
+ − 642
apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
+ − 643
apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits
+ − 644
dest:init_file_has_inum inof_has_file_tag init_sec_file_dir)
+ − 645
done
+ − 646
+ − 647
lemma cf2sfile_nil_prop:
+ − 648
"f \<in> init_files \<Longrightarrow> cf2sfile [] f = (\<lambda> b. if (b = is_init_file f) then init_cf2sfile f else None)"
+ − 649
apply (frule cf2sfile_nil_prop1, frule cf2sfile_nil_prop2)
+ − 650
by (rule ext, auto split:if_splits)
+ − 651
+ − 652
lemma cf2sfile_nil_prop3:
+ − 653
"is_init_file f \<Longrightarrow> cf2sfile [] f True = init_cf2sfile f"
+ − 654
by (simp add:is_init_file_prop1 cf2sfile_nil_prop)
+ − 655
+ − 656
lemma cf2sfile_nil_prop4:
+ − 657
"is_init_dir f \<Longrightarrow> cf2sfile [] f False = init_cf2sfile f"
+ − 658
apply (frule init_file_dir_conflict2)
+ − 659
by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop)
+ − 660
+ − 661
lemma cfs2sfiles_nil_prop:
+ − 662
"\<forall> f \<in> fs. f \<in> init_files \<Longrightarrow> cfs2sfiles [] fs = init_cfs2sfiles fs"
+ − 663
apply (simp add:cfs2sfiles_def init_cfs2sfiles_def)
2
+ − 664
apply (rule set_eqI, rule iffI, auto simp:cf2sfile_nil_prop split:if_splits)
+ − 665
done
1
+ − 666
+ − 667
lemma cfd2sfd_nil_prop:
+ − 668
"init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd"
+ − 669
apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def)
2
+ − 670
apply (frule init_filefd_prop5, drule init_filefd_prop1, drule cf2sfile_nil_prop)
1
+ − 671
by (auto split:option.splits)
+ − 672
+ − 673
lemma cpfd2sfds_nil_prop:
+ − 674
"cpfd2sfds [] p = init_cfds2sfds p"
+ − 675
apply (simp only:cpfd2sfds_def init_cfds2sfds_def)
+ − 676
apply (rule set_eqI, rule iffI)
+ − 677
apply (drule CollectD, rule CollectI, (erule exE)+)
+ − 678
apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI) defer
+ − 679
apply (drule CollectD, rule CollectI, (erule exE)+)
+ − 680
apply (rule_tac x = fd in exI, rule_tac x = sfd in exI, rule_tac x = f in exI)
+ − 681
using cfd2sfd_nil_prop by auto
+ − 682
+ − 683
lemma ch2sshm_nil_prop:
+ − 684
"h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h"
+ − 685
by (simp add:ch2sshm_def init_sectxt_prop init_ch2sshm_def)
+ − 686
+ − 687
lemma cph2spshs_nil_prop:
+ − 688
"cph2spshs [] p = init_cph2spshs p"
+ − 689
apply (auto simp add:init_cph2spshs_def cph2spshs_def init_sectxt_prop)
+ − 690
apply (rule_tac x = h in exI, simp) defer
+ − 691
apply (rule_tac x = h in exI, simp)
+ − 692
by (auto simp:ch2sshm_nil_prop dest:init_procs_has_shm)
+ − 693
+ − 694
lemma cp2sproc_nil_prop:
+ − 695
"p \<in> init_procs \<Longrightarrow> cp2sproc [] p = init_cp2sproc p"
+ − 696
by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cph2spshs_nil_prop cpfd2sfds_nil_prop
+ − 697
split:option.splits)
+ − 698
+ − 699
lemma msg_has_sec_imp_init:
+ − 700
"init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)"
+ − 701
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 702
by (drule init_type_has_obj, simp)
+ − 703
+ − 704
lemma msgq_has_sec_imp_init:
+ − 705
"init_sectxt_of_obj (O_msgq q) = Some sec \<Longrightarrow> q \<in> init_msgqs"
+ − 706
apply (simp add:init_sectxt_of_obj_def split:option.splits)
+ − 707
by (drule init_type_has_obj, simp)
+ − 708
+ − 709
lemma cm2smsg_nil_prop:
+ − 710
"cm2smsg [] q m = init_cm2smsg q m"
+ − 711
by (auto simp add:init_sectxt_prop cm2smsg_def init_cm2smsg_def split:option.splits
+ − 712
dest: msg_has_sec_imp_init intro:t_init elim:tainted.cases)
+ − 713
+ − 714
lemma cqm2sms_nil_prop:
+ − 715
"cqm2sms [] q ms = init_cqm2sms q ms"
+ − 716
apply (induct ms, simp)
+ − 717
by (auto simp add:cm2smsg_def init_sectxt_prop tainted_nil_prop msg_has_sec_imp_init init_cm2smsg_def
+ − 718
split:option.splits)
+ − 719
+ − 720
lemma cq2smsga_nil_prop:
+ − 721
"cq2smsgq [] q = init_cq2smsgq q"
+ − 722
by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop
+ − 723
intro:msgq_has_sec_imp_init split:option.splits)
+ − 724
+ − 725
lemma co2sobj_nil_prop:
+ − 726
"init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
+ − 727
apply (case_tac obj)
+ − 728
apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop
+ − 729
cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1
+ − 730
is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop
2
+ − 731
same_inode_nil_prop cm2smsg_nil_prop
+ − 732
dest:init_same_inode_prop1
1
+ − 733
split:option.splits)
+ − 734
apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
2
+ − 735
apply (simp add:init_files_props)
+ − 736
apply (auto simp:is_dir_nil is_file_nil dest:init_file_dir_conflict)
+ − 737
done
1
+ − 738
+ − 739
lemma s2ss_nil_prop:
+ − 740
"s2ss [] = init_static_state"
+ − 741
using co2sobj_nil_prop init_alive_prop
+ − 742
by (auto simp add:s2ss_def init_static_state_def)
+ − 743
+ − 744
end
+ − 745
+ − 746
(*<*)
+ − 747
end
+ − 748
(*>*)