1 (*<*) |
1 (*<*) |
2 theory Co2sobj_prop |
2 theory Co2sobj_prop |
3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop |
3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop |
4 begin |
4 begin |
5 (*<*) |
5 (*<*) |
6 |
6 |
|
7 ML {* |
|
8 fun print_ss ss = |
|
9 let |
|
10 val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss |
|
11 in |
|
12 simps |
|
13 end |
|
14 *} |
|
15 |
|
16 |
7 context tainting_s begin |
17 context tainting_s begin |
8 |
18 |
9 (********************* cm2smsg simpset ***********************) |
19 (********************* cm2smsg simpset ***********************) |
10 |
20 |
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" |
21 lemma cm2smsg_other: |
|
22 "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m; \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> |
|
23 \<Longrightarrow> cm2smsg (e # s) = cm2smsg s" |
12 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext) |
24 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext) |
|
25 unfolding cm2smsg_def |
13 apply (case_tac e) |
26 apply (case_tac e) |
14 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits |
27 apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted |
15 intro:tainted.intro |
28 split:t_object.splits option.splits if_splits |
16 |
29 dest:not_deleted_init_msg dest!:current_has_sec') |
17 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
30 done |
18 |
31 |
19 |
32 lemma cm2smsg_sendmsg: |
|
33 "valid (SendMsg p q m # s) \<Longrightarrow> cm2smsg (SendMsg p q m # s) = (\<lambda> q' m'. |
|
34 if (q' = q \<and> m' = m) |
|
35 then (case (sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of |
|
36 Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s)) |
|
37 | _ \<Rightarrow> None) |
|
38 else cm2smsg s q' m') " |
|
39 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext) |
|
40 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps |
|
41 split:if_splits option.splits |
|
42 dest:not_deleted_init_msg dest!:current_has_sec') |
|
43 done |
|
44 |
|
45 lemma cm2smsg_recvmsg1: |
|
46 "\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'" |
|
47 apply (frule vd_cons, frule vt_grant_os, rule ext) |
|
48 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps |
|
49 split:if_splits option.splits) |
|
50 done |
|
51 |
|
52 lemma cm2smsg_recvmsg2: |
|
53 "\<lbrakk>m' \<noteq> m; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'" |
|
54 apply (frule vd_cons, frule vt_grant_os) |
|
55 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps |
|
56 split:if_splits option.splits) |
|
57 done |
|
58 |
|
59 lemma cm2smsg_recvmsg1': |
|
60 "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'" |
|
61 apply (frule vd_cons, frule vt_grant_os, rule ext) |
|
62 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps |
|
63 split:if_splits option.splits) |
|
64 done |
|
65 |
|
66 lemma cm2smsg_recvmsg2': |
|
67 "\<lbrakk>valid (RecvMsg p q m # s); m' \<noteq> m\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'" |
|
68 apply (frule vd_cons, frule vt_grant_os) |
|
69 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps |
|
70 split:if_splits option.splits) |
|
71 done |
|
72 |
|
73 lemma cm2smsg_removemsgq: |
|
74 "\<lbrakk>q' \<noteq> q; valid (RemoveMsgq p q # s)\<rbrakk> \<Longrightarrow> cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'" |
|
75 apply (frule vd_cons, frule vt_grant_os, rule ext) |
|
76 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps |
|
77 split:if_splits option.splits) |
|
78 done |
|
79 |
|
80 lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2' |
|
81 cm2smsg_removemsgq cm2smsg_other |
|
82 |
|
83 lemma init_cm2smsg_has_smsg: |
|
84 "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm" |
|
85 by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt) |
|
86 |
|
87 lemma hd_set_prop1: |
|
88 "hd l \<notin> set l \<Longrightarrow> l = []" |
|
89 by (case_tac l, auto) |
|
90 |
|
91 lemma tl_set_prop1: |
|
92 "a \<in> set (tl l) \<Longrightarrow> a \<in> set l" |
|
93 by (case_tac l, auto) |
|
94 |
|
95 lemma current_has_smsg: |
|
96 "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sm. cm2smsg s q m = Some sm" |
|
97 apply (induct s) |
|
98 apply (simp only:cm2smsg_nil_prop msgs_of_queue.simps current_msgqs.simps init_cm2smsg_has_smsg) |
|
99 |
|
100 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
101 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits |
|
102 dest!:current_has_sec' hd_set_prop1 dest:not_deleted_init_msg tl_set_prop1) |
|
103 done |
|
104 |
|
105 lemma current_has_smsg': |
|
106 "\<lbrakk>cm2smsg s q m = None; q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> m \<notin> set (msgs_of_queue s q)" |
|
107 by (auto dest:current_has_smsg) |
|
108 |
|
109 lemma cqm2sms_has_sms_aux: |
|
110 "\<forall> m \<in> set ms. sectxt_of_obj s (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. cqm2sms s q ms = Some sms)" |
|
111 by (induct ms, auto split:option.splits simp:cm2smsg_def) |
|
112 |
|
113 lemma current_has_sms: |
|
114 "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sms. cqm2sms s q (msgs_of_queue s q) = Some sms" |
|
115 apply (rule cqm2sms_has_sms_aux) |
|
116 apply (auto dest:current_msg_has_sec) |
|
117 done |
|
118 |
|
119 lemma current_has_sms': |
|
120 "\<lbrakk>cqm2sms s q (msgs_of_queue s q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" |
|
121 by (auto dest:current_has_sms) |
|
122 |
|
123 (********************* cqm2sms simpset ***********************) |
|
124 |
|
125 lemma cqm2sms_other: |
|
126 "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; |
|
127 \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> |
|
128 \<Longrightarrow> cqm2sms (e # s) = cqm2sms s" |
|
129 apply (rule ext, rule ext) |
|
130 apply (induct_tac xa, simp) |
|
131 apply (frule vt_grant_os, frule vd_cons, case_tac e) |
|
132 apply (auto split:option.splits dest:cm2smsg_other) |
|
133 done |
|
134 |
|
135 lemma cqm2sms_createmsgq: |
|
136 "valid (CreateMsgq p q # s) \<Longrightarrow> cqm2sms (CreateMsgq p q # s) = (\<lambda> q' ms'. |
|
137 if (q' = q \<and> ms' = []) then Some [] |
|
138 else cqm2sms s q' ms')" |
|
139 apply (rule ext, rule ext) |
|
140 apply (frule vt_grant_os, frule vd_cons, induct_tac ms') |
|
141 apply (auto split:if_splits option.splits dest:cm2smsg_other) |
|
142 done |
|
143 |
|
144 lemma cqm2sms_2: |
|
145 "cqm2sms s q (ms @ [m]) = |
|
146 (case (cqm2sms s q ms, cm2smsg s q m) of |
|
147 (Some sms, Some sm) \<Rightarrow> Some (sms @ [sm]) |
|
148 | _ \<Rightarrow> None)" |
|
149 apply (induct ms, simp split:option.splits) |
|
150 by (auto split:option.splits) |
|
151 |
|
152 lemmas cqm2sms_simps2 = cqm2sms.simps(1) cqm2sms_2 |
|
153 |
|
154 declare cqm2sms.simps [simp del] |
|
155 |
|
156 lemma cqm2sms_prop1: |
|
157 "cqm2sms s q ms = None \<Longrightarrow> \<exists> m \<in> set ms. cm2smsg s q m = None" |
|
158 by (induct ms, auto simp:cqm2sms.simps split:option.splits) |
|
159 |
|
160 lemma cqm2sms_sendmsg1: |
|
161 "\<lbrakk>valid (SendMsg p q m # s); m \<notin> set ms\<rbrakk> |
|
162 \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms" |
|
163 apply (frule vt_grant_os, frule vd_cons) |
|
164 apply (frule cm2smsg_sendmsg) |
|
165 apply (induct ms rule:rev_induct) |
|
166 apply (auto split:if_splits option.splits simp:cqm2sms_simps2) |
|
167 done |
|
168 |
|
169 lemma cqm2sms_sendmsg2: |
|
170 "\<lbrakk>valid (SendMsg p q m # s); q' \<noteq> q\<rbrakk> |
|
171 \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms" |
|
172 apply (frule vt_grant_os, frule vd_cons) |
|
173 apply (frule cm2smsg_sendmsg) |
|
174 apply (induct ms rule:rev_induct) |
|
175 apply (auto split:if_splits option.splits simp:cqm2sms_simps2) |
|
176 done |
|
177 |
|
178 lemma cqm2sms_sendmsg3: |
|
179 "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q\<rbrakk> |
|
180 \<Longrightarrow> cqm2sms (SendMsg p q m # s) q ms' = |
|
181 (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of |
|
182 (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))]) |
|
183 | _ \<Rightarrow> None)" |
|
184 apply (frule vt_grant_os, frule vd_cons) |
|
185 apply (frule cm2smsg_sendmsg) |
|
186 apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cqm2sms_sendmsg1) |
|
187 done |
|
188 |
|
189 lemma cqm2sms_sendmsg: |
|
190 "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q'\<rbrakk> |
|
191 \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms' = ( |
|
192 if (q' = q) |
|
193 then (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of |
|
194 (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))]) |
|
195 | _ \<Rightarrow> None) |
|
196 else cqm2sms s q' ms' )" |
|
197 apply (simp split:if_splits add:cqm2sms_sendmsg2 cqm2sms_sendmsg3) |
|
198 done |
|
199 |
|
200 lemma cqm2sms_recvmsg1: |
|
201 "\<lbrakk>valid (RecvMsg p q m # s); m \<notin> set ms\<rbrakk> |
|
202 \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q ms = cqm2sms s q ms" |
|
203 apply (frule vt_grant_os, frule vd_cons) |
|
204 apply (induct ms rule:rev_induct) |
|
205 apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg2') |
|
206 done |
|
207 |
|
208 lemma cqm2sms_recvmsg2: |
|
209 "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk> |
|
210 \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = cqm2sms s q' ms" |
|
211 apply (frule vt_grant_os, frule vd_cons) |
|
212 apply (induct ms rule:rev_induct) |
|
213 apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg1') |
|
214 done |
|
215 |
|
216 lemma cqm2sms_recvmsg: |
|
217 "\<lbrakk>valid (RecvMsg p q m # s); ms = msgs_of_queue (RecvMsg p q m # s) q'\<rbrakk> |
|
218 \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = ( |
|
219 if (q' = q) |
|
220 then (case (cqm2sms s q (msgs_of_queue s q)) of |
|
221 Some sms \<Rightarrow> Some (tl sms) |
|
222 | _ \<Rightarrow> None) |
|
223 else cqm2sms s q' ms)" |
|
224 apply (frule vt_grant_os, frule vd_cons) |
|
225 apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2) |
|
226 using cm2smsg_recvmsg1 cm2smsg_recvmsg2 |
|
227 apply (auto split:if_splits option.splits) |
|
228 |
|
229 |
|
230 lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg |
20 |
231 |
21 (********************* cq2smsgq simpset ***********************) |
232 (********************* cq2smsgq simpset ***********************) |
22 |
233 |
23 lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" |
234 lemma cq2smsgq_other: |
24 apply (case_tac e) |
235 "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; |
25 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) |
236 \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> |
|
237 \<Longrightarrow> cq2smsgq (e # s) = cq2smsgq s" |
|
238 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e) |
|
239 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps |
|
240 split:t_object.splits option.splits if_splits |
|
241 dest:not_deleted_init_msg dest!:current_has_sec') |
|
242 |
|
243 |
|
244 |
|
245 |
26 |
246 |
27 lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
247 lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
28 |
248 |
29 |
249 |
30 lemma sm_in_sqsms: |
250 lemma sm_in_sqsms: |