equal
deleted
inserted
replaced
4 begin |
4 begin |
5 (*<*) |
5 (*<*) |
6 |
6 |
7 context tainting_s begin |
7 context tainting_s begin |
8 |
8 |
|
9 (********************* cm2smsg simpset ***********************) |
|
10 |
|
11 lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s" |
|
12 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext) |
|
13 apply (case_tac e) |
|
14 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits |
|
15 intro:tainted.intro |
|
16 |
|
17 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
|
18 |
|
19 |
|
20 |
|
21 (********************* cq2smsgq simpset ***********************) |
|
22 |
|
23 lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" |
|
24 apply (case_tac e) |
|
25 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) |
|
26 |
|
27 lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
|
28 |
|
29 |
|
30 lemma sm_in_sqsms: |
|
31 "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; cq2smsgq s q = Some (qi, qsec, sms); |
|
32 cm2smsg s q m = Some sm\<rbrakk> \<Longrightarrow> sm \<in> set sms" |
|
33 sorry |
|
34 |
|
35 |
|
36 |
9 (****************** cf2sfile path simpset ***************) |
37 (****************** cf2sfile path simpset ***************) |
10 |
|
11 thm cpfd2sfds_def |
|
12 |
38 |
13 lemma sroot_only: |
39 lemma sroot_only: |
14 "cf2sfile s [] = Some sroot" |
40 "cf2sfile s [] = Some sroot" |
15 by (simp add:cf2sfile_def) |
41 by (simp add:cf2sfile_def) |
16 |
42 |
1241 by (drule_tac p'= p' in cp2sproc_exit, simp+) |
1267 by (drule_tac p'= p' in cp2sproc_exit, simp+) |
1242 |
1268 |
1243 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm |
1269 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm |
1244 cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other |
1270 cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other |
1245 |
1271 |
1246 (********************* cm2smsg simpset ***********************) |
|
1247 |
|
1248 lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s" |
|
1249 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext) |
|
1250 apply (case_tac e) |
|
1251 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits) |
|
1252 |
|
1253 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
|
1254 |
|
1255 |
|
1256 |
|
1257 (********************* cq2smsgq simpset ***********************) |
|
1258 |
|
1259 lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" |
|
1260 apply (case_tac e) |
|
1261 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) |
|
1262 |
|
1263 lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
|
1264 |
1272 |
1265 |
1273 |
1266 |
1274 |
1267 |
1275 |
1268 end |
1276 end |