-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCreateIRQCaps_SI.thy
431 lines (381 loc) · 18.7 KB
/
CreateIRQCaps_SI.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(NICTA_GPL)
*)
theory CreateIRQCaps_SI
imports
"../proof/capDL-api/IRQ_DP"
ObjectInitialised_SI
RootTask_SI
SysInit_SI
begin
(*****************
* Helper lemmas *
*****************)
lemma si_cnode_caps:
"si_cnode_cap = si_cspace_cap"
by (simp add: si_cnode_cap_def si_cspace_cap_def)
lemma hoare_grab_exs2:
"(\<And>x. P x \<Longrightarrow> \<lbrace>P' x\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x \<and> P' x s\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp: valid_def)
lemma sep_map_irq_sep_irq_node:
"(irq \<mapsto>irq k_irq_table irq \<and>* R) s
\<Longrightarrow> sep_irq_node s irq = Some (k_irq_table irq)"
by (fastforce simp: sep_map_irq_def sep_conj_def
sep_disj_sep_state_def sep_state_disj_def
plus_sep_state_def sep_state_add_def
map_disj_def map_add_Some_iff)
(*********************************************************************************
* A new definition of si_irq_nodes that states that the mapping is injective. *
*********************************************************************************)
lemma sep_map_o_distinct:
"(obj_id \<mapsto>o obj \<and>* obj_id' \<mapsto>o obj') s \<Longrightarrow> obj_id \<noteq> obj_id'"
by (fastforce simp: sep_map_o_def sep_map_general_def sep_conj_def object_to_sep_state_def
sep_disj_sep_state_def sep_state_disj_def
map_disj_def dom_def disjoint_iff_not_equal)
lemma sep_any_map_o_false_eq:
"(obj_id \<mapsto>o - \<and>* obj_id \<mapsto>o -) = sep_false"
by (fastforce simp: sep_any_def sep_map_o_def sep_map_general_def sep_conj_def
object_to_sep_state_def sep_disj_sep_state_def sep_state_disj_def
map_disj_def dom_def disjoint_iff_not_equal)
lemma sep_any_map_o_false:
"(obj_id \<mapsto>o - \<and>* obj_id \<mapsto>o -) s \<Longrightarrow> False"
by (simp add: sep_any_map_o_false_eq)
lemma sep_map_o_false:
"(obj_id \<mapsto>o obj \<and>* obj_id \<mapsto>o obj') s \<Longrightarrow> False"
by (metis sep_map_o_distinct)
lemma sep_map_o_any_distinct_list:
"((f x) \<mapsto>o - \<and>* \<And>* map (\<lambda>x. (f x) \<mapsto>o -) xs) s
\<Longrightarrow> x \<notin> set xs"
apply clarsimp
apply (subst (asm) sep_list_conj_map_remove1, assumption)
apply (sep_drule sep_any_map_o_false)
apply clarsimp
done
lemma sep_any_map_o_inj_on:
"(\<And>* map (\<lambda>x. (f x) \<mapsto>o -) xs) s
\<Longrightarrow> inj_on f (set xs)"
apply (induct xs arbitrary: s)
apply clarsimp
apply clarsimp
apply (rule conjI)
apply (clarsimp simp: sep_conj_def)
apply clarsimp
apply (frule sep_map_o_any_distinct_list)
apply simp
done
lemma sep_any_map_o_inj_on_set:
"\<lbrakk>(\<And>* x \<in> A. (f x) \<mapsto>o -) s; finite A\<rbrakk>
\<Longrightarrow> inj_on f A"
apply (drule sep_map_set_conj_sep_list_conj [where P="\<lambda>x. (f x) \<mapsto>o -"])
apply clarsimp
apply (erule sep_any_map_o_inj_on)
done
lemma sep_map_o_inj_on_set:
"\<lbrakk>(\<And>* x \<in> A. (f x) \<mapsto>o obj) s; finite A\<rbrakk>
\<Longrightarrow> inj_on f A"
apply (rule sep_any_map_o_inj_on_set [rotated, where s=s], assumption)
apply (erule sep_map_set_conj_impl)
apply (fastforce simp: sep_any_def)
apply simp
done
lemma sep_conj_existL:
"(P \<and>* Q) s \<Longrightarrow> \<exists>s. P s"
by (auto simp: sep_conj_def)
lemma sep_conj_existR:
"(P \<and>* Q) s \<Longrightarrow> \<exists>s. Q s"
by (auto simp: sep_conj_def)
lemma si_irq_nodes_def2:
"si_irq_nodes spec =
(\<lambda>s. \<exists>k_irq_table. inj_on k_irq_table (used_irqs spec) \<and>
(\<And>* irq\<in>used_irqs spec. irq \<mapsto>irq k_irq_table irq \<and>*
k_irq_table irq \<mapsto>o empty_irq_node) s)"
apply (rule ext)
apply (clarsimp simp: si_irq_nodes_def)
apply (rule iffI)
apply clarsimp
apply (rule_tac x=k_irq_table in exI, simp)
apply (subst (asm) sep.setprod.distrib)
apply (drule sep_conj_existR, clarsimp)
apply (erule sep_map_o_inj_on_set) (* Why doesn't sep_rule work? *)
apply simp
apply blast
done
(*******************************************
* The actual proofs about create_irq_caps *
*******************************************)
lemma well_formed_default_irq_node_empty:
"\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk>
\<Longrightarrow> object_at (\<lambda>obj. object_default_state obj = empty_irq_node) (cdl_irq_node spec irq) spec"
apply (frule (1) well_formed_used_irqs_have_cnode, clarsimp)
apply (frule (1) well_formed_irq_is_cnode)
apply (frule (1) well_formed_size_irq_cnode)
apply (clarsimp simp: object_at_def empty_irq_node_def object_default_state_def2
is_cnode_def object_size_bits_def
split: cdl_object.splits)
done
lemma create_irq_cap_sep:
"\<lbrace>\<guillemotleft>(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
irq \<mapsto>irq kernel_irq_id \<and>*
kernel_irq_id \<mapsto>o empty_irq_node \<and>*
si_objects \<and>* R\<guillemotright> and
K(well_formed spec \<and>
irq \<in> used_irqs spec \<and>
t' (cdl_irq_node spec irq) = Some kernel_irq_id \<and>
irq_caps irq = Some free_cptr \<and>
free_cptr < 2 ^ si_cnode_size)\<rbrace>
create_irq_cap spec (irq, free_cptr)
\<lbrace>\<lambda>_.
\<guillemotleft>irq_empty spec t' irq \<and>*
si_irq_cap_at irq_caps spec irq \<and>*
si_objects \<and>*
R\<guillemotright>\<rbrace>"
apply (rule hoare_gen_asm, clarsimp)
apply (frule (1) well_formed_used_irqs_have_cnode, clarsimp)
apply (frule (1) well_formed_default_irq_node_empty, clarsimp simp: object_at_def)
apply (clarsimp simp: create_irq_cap_def si_objects_def si_cnode_caps
irq_empty_def irq_initialised_general_def
si_irq_cap_at_def sep_conj_assoc)
apply (wp add: hoare_drop_imp sep_wp: seL4_IRQHandler_IRQControl_Get, simp)
apply (rule conjI)
apply sep_solve
apply (simp add: offset_slot_si_cnode_size' guard_equal_si_cspace_cap word_bits_def)
done
lemma create_irq_caps_sep_helper:
"\<lbrace>\<guillemotleft>((\<And>* cptr \<in> set (take (card (used_irqs spec)) free_cptrs).
((si_cnode_id, unat cptr) \<mapsto>c NullCap)) \<and>*
si_caps_at t orig_caps spec {obj_id. real_object_at obj_id spec} \<and>*
si_objects \<and>* si_irq_nodes spec \<and>* R) and
K (well_formed spec \<and>
list_all (\<lambda>n. n < 2 ^ si_cnode_size) free_cptrs \<and>
distinct free_cptrs \<and>
card (used_irqs spec) \<le> length free_cptrs)\<guillemotright> \<rbrace>
create_irq_caps spec free_cptrs
\<lbrace>\<lambda>rv s. \<exists>(t'::32 word \<Rightarrow> 32 word option).
\<guillemotleft>(irqs_empty spec t' (used_irqs spec) \<and>*
si_irq_caps_at (fst rv) spec (used_irqs spec) \<and>*
si_caps_at t orig_caps spec {obj_id. real_object_at obj_id spec} \<and>*
si_objects \<and>* R)
and K ((map_of (zip (used_irq_list spec) free_cptrs), drop (card (used_irqs spec)) free_cptrs) = rv \<and>
inj_on t' (used_irq_cnodes spec) \<and>
dom t' = used_irq_cnodes spec)\<guillemotright> s\<rbrace>"
apply clarsimp
apply (rule hoare_gen_asm_conj)
apply (clarsimp simp: create_irq_caps_def si_irq_nodes_def2 sep_conj_exists)
apply wp
apply simp
apply (rule hoare_grab_exs2)
apply (rule_tac x="(\<lambda>obj_id. Some ((k_irq_table \<circ> inv (cdl_irq_node spec)) obj_id))
|` used_irq_cnodes spec" in hoare_exI)
apply (rule_tac P1 = "\<lambda>(irq,free_cptr). (si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
irq \<mapsto>irq k_irq_table irq \<and>*
k_irq_table irq \<mapsto>o empty_irq_node" and
Q1 = "\<lambda>(irq,free_cptr). irq_empty spec ((\<lambda>obj_id. Some ((k_irq_table \<circ> inv (cdl_irq_node spec)) obj_id))
|` used_irq_cnodes spec) irq \<and>*
si_irq_cap_at (map_of (zip (used_irq_list spec) free_cptrs)) spec irq" and
I1 = "si_objects" and
R1 = "si_caps_at t orig_caps spec {obj_id. real_object_at obj_id spec} \<and>*
R" in hoare_chain [OF mapM_x_set_sep])
apply (metis distinct_zipI2)
apply (clarsimp split:prod.splits)
apply (clarsimp simp: sep_conj_assoc)
apply (wp sep_wp: create_irq_cap_sep, simp+)
apply (rule conjI)
apply (clarsimp simp: sep_conj_assoc sep_conj_exists)
apply sep_solve
apply (frule well_formed_inj_cdl_irq_node)
apply (frule set_zip_leftD)
apply (frule in_set_zip2)
apply (simp add: map_of_zip_tuple_in list_all_iff unat_less_2_si_cnode_size
restrict_map_def used_irq_cnodes_def)
apply (subst sep_list_conj_sep_map_set_conj [symmetric], erule distinct_zipI2)
apply (subst (asm) sep_list_conj_sep_map_set_conj [symmetric, where xs = "used_irq_list spec", simplified])
apply (subst split_beta')
apply (subst sep_list_conj_map_add)
apply (subst zip_take_length [symmetric])
apply (subst split_beta' [symmetric])+
apply (subst map_zip_snd', simp)
apply (subst (asm) (3) append_take_drop_id [where n="card (used_irqs spec)" and xs=free_cptrs, symmetric])
apply (subst map_zip_fst', simp)
apply (subst sep_list_conj_sep_map_set_conj, fastforce simp: used_irq_list_def)
apply (simp add: comp_def)
apply sep_solve
apply simp
apply (subst (asm) sep_list_conj_sep_map_set_conj [symmetric], erule distinct_zipI2)
apply (subst (asm) map_zip_fst', simp)
apply (subst (asm) sep_list_conj_map_add)
apply (subst (asm) sep_list_conj_sep_map_set_conj,
metis used_irq_list_def distinct_sorted_list_of_set)
apply (subst (asm) sep_list_conj_sep_map_set_conj,
metis used_irq_list_def distinct_sorted_list_of_set)
apply (clarsimp simp: irqs_empty_def si_irq_caps_at_def)
apply (rule conjI)
apply sep_solve
apply (frule well_formed_inj_cdl_irq_node)
apply (fastforce simp: inj_on_def used_irq_cnodes_def)
done
(*****************************************************************************
* The above lemma has an injection on just the IRQs. *
* We take the above proof, and join it with the result of CreateObjects *
* to produce an injection on all objects. *
* *
* The sum of the two injections "t_irqs" and "t_real" is injective because: *
* - Each individual relation is injective *
* - The domains are separate *
* - The ranges are separate *
* *
* The first two are easily true. *
* The last one is hard and only true because we have *
obj_id \<mapsto>o Untyped \<and>* obj_id \<mapsto> IRQ, and so the obj_ids are distinct. *
*****************************************************************************)
lemma irq_empty_cong:
"t (cdl_irq_node spec irq) = t' (cdl_irq_node spec irq)
\<Longrightarrow> irq_empty spec t irq = irq_empty spec t' irq"
by (clarsimp simp: irq_empty_def irq_initialised_general_def)
lemma object_empty_cong:
"t obj_id = t' obj_id
\<Longrightarrow> object_empty spec t obj_id = object_empty spec t' obj_id"
by (clarsimp simp: object_empty_def object_initialised_general_def)
lemma si_cap_at_cong:
"t obj_id = t' obj_id
\<Longrightarrow> si_cap_at t si_caps spec obj_id = si_cap_at t' si_caps spec obj_id"
by (clarsimp simp: si_cap_at_def)
lemma irq_empty_map_add:
"\<lbrakk>dom t' = cdl_irq_node spec ` irqs\<rbrakk>
\<Longrightarrow> irqs_empty spec t' irqs = irqs_empty spec (t++t') irqs"
apply (clarsimp simp: irqs_empty_def)
apply (rule sep.setprod.cong, simp)
apply (subst irq_empty_cong [where t'="t++t'" and t=t'], simp_all)
by (metis imageI map_add_eval_right)
lemma object_empty_map_add:
"\<lbrakk>dom t = obj_ids; map_disj t t'\<rbrakk>
\<Longrightarrow> objects_empty spec t obj_ids = objects_empty spec (t++t') obj_ids"
apply (clarsimp simp: objects_empty_def)
apply (rule sep.setprod.cong, simp)
apply (subst object_empty_cong [where t'="t++t'" and t=t], simp_all)
by (metis map_add_eval_left)
lemma si_caps_at_map_add:
"\<lbrakk>dom t = obj_ids; map_disj t t'\<rbrakk>
\<Longrightarrow> si_caps_at t si_caps spec obj_ids = si_caps_at (t++t') si_caps spec obj_ids"
apply (clarsimp simp: si_caps_at_def)
apply (rule sep.setprod.cong, simp)
apply (subst si_cap_at_cong [where t'="t++t'" and t=t], simp_all)
by (metis map_add_eval_left)
lemma inj_on_map_add:
"\<lbrakk>inj_on m (dom m); inj_on m' (dom m');
dom m \<inter> dom m' = {}; ran m \<inter> ran m' = {}; A = dom m \<union> dom m'\<rbrakk>
\<Longrightarrow> inj_on (m ++ m') A"
apply (rule inj_onI)
apply clarsimp
apply (elim disjE)
apply (metis inj_on_eq_iff inter_empty_not_both map_add_eval_left')
apply (metis dom_ran map_add_comm map_add_eval_right orthD1)
apply (metis dom_ran map_add_comm map_add_eval_right orthD1)
apply (metis inj_on_def map_add_eval_right)
done
lemma inter_emptyI:
"\<lbrakk>\<And>x. x \<in> A \<and> x \<in> B \<Longrightarrow> False\<rbrakk> \<Longrightarrow> A \<inter> B = {}"
by auto
lemma ran_inter_emptyI:
"\<lbrakk>\<And>x a b. f a = Some x \<and> g b = Some x \<Longrightarrow> False\<rbrakk> \<Longrightarrow> ran f \<inter> ran g = {}"
apply (rule inter_emptyI)
apply (auto simp: ran_def)
done
lemma irq_empty_objects_empty_ran_distinct:
"\<lbrakk>\<guillemotleft>irqs_empty spec t_irq (used_irqs spec) \<and>*
objects_empty spec t_real {obj_id. real_object_at obj_id spec} \<and>* R\<guillemotright> s;
well_formed spec;
inj_on t_irq (cdl_irq_node spec ` used_irqs spec); dom t_irq = cdl_irq_node spec ` used_irqs spec;
inj_on t_real {obj_id. real_object_at obj_id spec}; dom t_real = {obj_id. real_object_at obj_id spec}\<rbrakk>
\<Longrightarrow> ran t_real \<inter> ran t_irq = {}"
apply (frule well_formed_inj_cdl_irq_node)
apply (clarsimp simp: irqs_empty_def irq_empty_def irq_initialised_general_def
objects_empty_def object_empty_def object_initialised_general_def)
apply (rule ran_inter_emptyI)
apply clarsimp
apply (frule domI [where m=t_real])
apply (frule domI [where m=t_irq])
apply clarsimp
apply (rename_tac irq_obj_id obj_id irq)
apply (subst (asm) sep.setprod.remove, simp, assumption)
apply (subst (asm) sep.setprod.remove, simp, fast)
apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
apply (sep_drule sep_map_o_false, simp)
done
lemma si_objects_extra_caps'_split:
"\<lbrakk>well_formed spec; distinct free_cptrs';
free_cptrs = drop (card {obj_id. real_object_at obj_id spec}) free_cptrs'\<rbrakk> \<Longrightarrow>
si_objects_extra_caps' {obj_id. real_object_at obj_id spec} free_cptrs' untyped_cptrs
=
((\<And>* cptr \<in> set (take (card (used_irqs spec)) free_cptrs). (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>*
si_objects_extra_caps' (dom (cdl_objects spec)) free_cptrs' untyped_cptrs)"
apply (frule well_formed_objects_card [symmetric])
apply (subst (asm) nat_add_commute)
apply (clarsimp simp: si_objects_extra_caps'_def sep_conj_exists sep_conj_assoc)
apply (subst take_drop_append [where a="card {obj_id. real_object_at obj_id spec}"
and b="card (used_irqs spec)"])
apply clarsimp
apply (subst sep.setprod.union_disjoint, (simp add: distinct_take_drop_append)+)
apply (clarsimp simp: sep_conj_ac)
done
lemma create_irq_caps_sep:
"\<lbrace>\<lambda>s. \<exists>t_real.
\<guillemotleft>(objects_empty spec t_real {obj_id. real_object_at obj_id spec} \<and>*
si_caps_at t_real orig_caps spec {obj_id. real_object_at obj_id spec} \<and>*
si_objects \<and>*
si_objects_extra_caps' {obj_id. real_object_at obj_id spec} free_cptrs_orig untyped_cptrs \<and>*
si_irq_nodes spec \<and>* R) and
K (well_formed spec \<and>
distinct free_cptrs_orig \<and>
list_all (\<lambda>n. n < 2 ^ si_cnode_size) free_cptrs \<and>
card (used_irqs spec) \<le> length free_cptrs \<and>
inj_on t_real {obj_id. real_object_at obj_id spec} \<and>
dom t_real = {obj_id. real_object_at obj_id spec} \<and>
dom orig_caps = {obj_id. real_object_at obj_id spec} \<and>
free_cptrs = drop (card {obj_id. real_object_at obj_id spec}) free_cptrs_orig)\<guillemotright> s\<rbrace>
create_irq_caps spec free_cptrs
\<lbrace>\<lambda>rv s. \<exists>(t::32 word \<Rightarrow> 32 word option).
\<guillemotleft>(objects_empty spec t {obj_id. real_object_at obj_id spec} \<and>*
irqs_empty spec t (used_irqs spec) \<and>*
si_caps_at t orig_caps spec {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at (fst rv) spec (used_irqs spec) \<and>*
si_objects \<and>*
si_objects_extra_caps' (dom (cdl_objects spec)) free_cptrs_orig untyped_cptrs \<and>*
R) and
K ((map_of (zip (used_irq_list spec) free_cptrs), drop (card (used_irqs spec)) free_cptrs) = rv \<and>
inj_on t (dom (cdl_objects spec)) \<and> dom t = dom (cdl_objects spec))\<guillemotright> s\<rbrace>"
apply (rule hoare_ex_pre)
apply (rule hoare_gen_lifted_asm)
apply (elim conjE)
apply (subst si_objects_extra_caps'_split, assumption+)
apply (rule hoare_chain [OF create_irq_caps_sep_helper, standard, where orig_caps=orig_caps])
apply (rule pred_andI)
apply sep_solve
apply clarsimp
apply clarsimp
apply (rule_tac x="t_real ++ t'" in exI)
apply clarsimp
apply (frule well_formed_objects_real_or_irq)
apply (frule well_formed_objects_only_real_or_irq)
apply (clarsimp simp: used_irq_cnodes_def)
apply (subgoal_tac "map_disj t_real t'")
apply (rule conjI)
apply (subst object_empty_map_add [symmetric], assumption+)
apply (subst irq_empty_map_add [symmetric],simp add: used_irq_cnodes_def)
apply (subst si_caps_at_map_add [symmetric], assumption+)
apply (clarsimp simp: si_objects_extra_caps'_def sep_conj_exists sep_conj_assoc)
apply (rule_tac x=untyped_caps in exI)
apply (rule_tac x=all_available_ids in exI)
apply sep_solve
apply (rule conjI)
apply (rule inj_on_map_add, simp+)
apply (rule irq_empty_objects_empty_ran_distinct, sep_solve, simp+)
apply (metis sup_commute)
apply (clarsimp simp: map_disjI)
done
end