-
Notifications
You must be signed in to change notification settings - Fork 108
/
InitIRQ_SI.thy
284 lines (269 loc) · 13.9 KB
/
InitIRQ_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
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory InitIRQ_SI
imports
"DSpecProofs.IRQ_DP"
ObjectInitialised_SI
RootTask_SI
SysInit_SI
begin
lemma seL4_IRQHandler_SetEndpoint_irq_initialised_helper_sep:
"\<lbrace>\<guillemotleft>irq_empty spec t irq \<and>*
si_cap_at t orig_caps spec dev ntfn_id \<and>*
si_irq_cap_at irq_caps spec irq \<and>*
si_objects \<and>* R\<guillemotright> and
K(well_formed spec \<and>
cdl_objects spec ntfn_id = Some ntfn \<and>
is_ntfn ntfn \<and>
irq \<in> bound_irqs spec \<and>
opt_cap (cdl_irq_node spec irq, 0) spec = Some ntfn_cap \<and>
ntfn_id = cap_object ntfn_cap \<and>
t (cdl_irq_node spec irq) = Some kernel_irq_id \<and>
t ntfn_id = Some kernel_ntfn_id \<and>
cdl_objects spec (cdl_irq_node spec irq) = Some spec_irq \<and>
irq_caps irq = Some irq_handler_cptr \<and>
orig_caps ntfn_id = Some endpoint_cptr \<and>
irq_handler_cptr < 2 ^ si_cnode_size \<and>
endpoint_cptr < 2 ^ si_cnode_size)\<rbrace>
seL4_IRQHandler_SetEndpoint irq_handler_cptr endpoint_cptr
\<lbrace>\<lambda>_.
\<guillemotleft>irq_initialised spec t irq \<and>*
si_cap_at t orig_caps spec dev ntfn_id \<and>*
si_irq_cap_at irq_caps spec irq \<and>*
si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_gen_asm, clarsimp)
apply (frule well_formed_bound_irqs_are_used_irqs)
apply (subst irq_initialised_decomp_total, assumption+, fast)
apply (subst irq_empty_decomp_total, assumption+, fast)
apply (clarsimp simp: irq_slot_initialised_def irq_slot_empty_def irq_initialised_general_def
si_cap_at_def si_irq_cap_at_def si_objects_def
sep_conj_assoc sep_conj_exists)
apply (frule (1) well_formed_irq_is_irq_node)
apply (frule (1) well_formed_size_irq_node)
apply (frule (2) well_formed_irq_ntfn_cap)
apply (rule hoare_chain)
apply (rule seL4_IRQHandler_SetEndpoint_wp [where
root_tcb = root_tcb
and cnode_cap = si_cspace_cap
and cnode_id = si_cnode_id
and root_size = si_cnode_size
and irq = irq
and irq_handler_slot = "unat (the (irq_caps irq))"
and endpoint_slot = "unat (the (orig_caps (cap_object ntfn_cap)))"
and irq_id = "the (t (cdl_irq_node spec irq))"
and old_cap = NullCap
and endpoint_cap = "NotificationCap (the (t (cap_object ntfn_cap))) 0 {AllowRead, AllowWrite}"
and R="object_empty_slots_initialised spec t (cdl_irq_node spec irq) \<and>*
object_fields_empty spec t (cdl_irq_node spec irq) \<and>*
(si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>*
(si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>*
si_asid \<and>* R"])
apply (intro pred_conjI)
apply (clarsimp simp: object_type_is_object default_cap_def)
apply (sep_drule sep_map_c_sep_map_s [where cap=NullCap])
apply (rule object_slots_object_default_state_NullCap', (simp add: object_type_has_slots)+)
apply sep_solve
apply simp
apply (frule guard_equal_si_cspace_cap' [where src_index=irq_handler_cptr])
apply (frule guard_equal_si_cspace_cap' [where src_index=endpoint_cptr])
apply (clarsimp simp: ep_related_cap_def offset_slot')
apply simp
apply (clarsimp simp: object_type_is_object default_cap_def)
apply (subst (asm) irq_node_fields_empty_initialised)
apply (simp add: object_type_object_at)
apply (simp add: object_fields_initialised_def object_initialised_general_def)
apply (sep_drule sep_map_s_sep_map_c [where obj_id = kernel_irq_id
and cap = "NotificationCap kernel_ntfn_id 0 {AllowRead, AllowWrite}"
and obj = "spec2s t spec_irq"])
apply simp
apply (frule (1) object_slots_opt_capI)
apply (subst object_slots_spec2s,
(fastforce simp: object_type_has_slots cap_has_object_def
update_cap_object_def cap_type_def
split: cdl_cap.splits)+)
apply sep_solve
done
lemma seL4_IRQHandler_SetEndpoint_irq_initialised_sep:
"\<lbrace>\<guillemotleft>irq_empty spec t irq \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (bound_irqs spec) \<and>*
si_objects \<and>* R\<guillemotright> and
K(well_formed spec \<and>
irq \<in> bound_irqs spec \<and>
irq_caps irq = Some irq_handler_cptr \<and>
orig_caps (cap_object (the (opt_cap (cdl_irq_node spec irq, 0) spec))) = Some endpoint_cptr)\<rbrace>
seL4_IRQHandler_SetEndpoint irq_handler_cptr endpoint_cptr
\<lbrace>\<lambda>_.
\<guillemotleft>irq_initialised spec t irq \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (bound_irqs spec) \<and>*
si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_gen_asm)
apply (clarsimp simp: si_irq_caps_at_def)
apply (frule well_formed_bound_irqs_are_used_irqs)
apply (frule (1) well_formed_cap_object_cdl_irq_node, clarsimp)
apply (frule object_at_real_object_at [where obj_id = "cap_object (the (opt_cap (cdl_irq_node spec irq, 0) spec))"],
fastforce simp: object_at_def)
apply (frule well_formed_slot_0_of_used_irq_node, fast, clarsimp)
apply (frule slots_of_cdl_objects, clarsimp)
apply (rule hoare_chain [OF sep_set_conj_map_singleton_wp
[where P = "irq_empty spec t irq \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_objects"
and Q = "irq_initialised spec t irq \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_objects"
and I = "si_irq_cap_at irq_caps spec"
and x = irq
and xs = "bound_irqs spec"]], simp+)
apply (clarsimp simp: si_irq_caps_at_def si_caps_at_def)
apply (rule hoare_chain [OF sep_set_conj_map_singleton_wp
[where P = "irq_empty spec t irq \<and>*
si_irq_cap_at irq_caps spec irq \<and>*
si_objects"
and Q = "irq_initialised spec t irq \<and>*
si_irq_cap_at irq_caps spec irq \<and>*
si_objects"
and I = "si_cap_at t orig_caps spec dev"
and x = "cap_object (the (opt_cap (cdl_irq_node spec irq, 0) spec))"
and xs = "{obj_id. real_object_at obj_id spec}"]], simp+)
apply (wp sep_wp: seL4_IRQHandler_SetEndpoint_irq_initialised_helper_sep [where t=t and spec=spec and irq=irq
and ntfn_cap = "the (opt_cap (cdl_irq_node spec irq, 0) spec)"
and kernel_irq_id = "the (t (cdl_irq_node spec irq))"
and kernel_ntfn_id = "the (t (cap_object (the (opt_cap (cdl_irq_node spec irq, 0) spec))))"], simp)
apply (rule conjI)
apply sep_solve
apply (fastforce simp: opt_cap_def irq_empty_def irq_initialised_general_def
si_irq_cap_at_def si_cap_at_def sep_conj_exists)
apply sep_solve
apply sep_solve
apply sep_solve
apply sep_solve
done
lemma init_irq_sep:
"\<lbrace>\<guillemotleft>irq_empty spec t irq \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (bound_irqs spec) \<and>*
si_objects \<and>* R\<guillemotright> and
K(well_formed spec \<and>
irq \<in> bound_irqs spec)\<rbrace>
init_irq spec orig_caps irq_caps irq
\<lbrace>\<lambda>_. \<guillemotleft>irq_initialised spec t irq \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (bound_irqs spec) \<and>*
si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_gen_asm, clarsimp)
apply (clarsimp simp: init_irq_def)
apply (wp hoare_drop_imp seL4_IRQHandler_SetEndpoint_irq_initialised_sep | simp)+
apply (frule (1) well_formed_cap_object_cdl_irq_node)
apply (frule object_at_real_object_at [where obj_id = "cap_object (the (opt_cap (cdl_irq_node spec irq, 0) spec))"],
fastforce simp: object_at_def)
apply (clarsimp simp: si_caps_at_def get_irq_slot_def)
apply (subst (asm) sep.prod.remove [where x="cap_object (the (opt_cap (cdl_irq_node spec irq, 0) spec))"], simp)
apply clarsimp
apply (clarsimp simp: si_cap_at_def sep_conj_exists)
done
lemma init_irqs_bound_irqs_sep:
"\<lbrace>\<guillemotleft>irqs_empty spec t (bound_irqs spec) \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (bound_irqs spec) \<and>*
si_objects \<and>* R\<guillemotright> and
K(well_formed spec)\<rbrace>
init_irqs spec orig_caps irq_caps
\<lbrace>\<lambda>_.\<guillemotleft>irqs_initialised spec t (bound_irqs spec) \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (bound_irqs spec) \<and>*
si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_gen_asm)
apply (clarsimp simp: init_irqs_def)
apply (clarsimp simp: irqs_empty_def irqs_initialised_def)
apply (rule mapM_x_set_sep' [where
P="irq_empty spec t" and
Q="irq_initialised spec t" and
I="si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (bound_irqs spec) \<and>*
si_objects" and
R=R, simplified sep_conj_assoc], fastforce+)
apply (wp init_irq_sep, simp+)
done
lemma irq_slot_empty_initialised_NullCap:
"\<lbrakk>well_formed spec; slots_of (cdl_irq_node spec irq) spec slot = Some NullCap\<rbrakk>
\<Longrightarrow> irq_slot_empty spec t irq slot = irq_slot_initialised spec t irq slot"
apply (frule slots_of_cdl_objects, clarsimp)
apply (frule (1) well_formed_irq_is_irq_node)
apply (frule (1) well_formed_object_slots)
apply (rule ext)
apply (clarsimp simp: irq_slot_empty_def irq_slot_initialised_def irq_initialised_general_def slots_of_def
split: option.splits)
apply (subgoal_tac "object_slots (object_default_state obj) slot = object_slots (spec2s t obj) slot")
apply (subst sep_map_s_object_slots_equal, assumption, simp)
apply clarsimp
apply (frule object_slots_spec2s_NullCap [where t=t], simp)
apply (erule object_slots_object_default_state_NullCap
[where obj_id = "cdl_irq_node spec irq" and cap = NullCap])
apply (clarsimp simp: object_at_def object_type_is_object)
apply (clarsimp simp: opt_cap_def slots_of_def)
apply simp
done
lemma irq_slot_empty_initialised:
"\<lbrakk>well_formed spec; irq \<notin> bound_irqs spec; irq \<in> used_irqs spec;
cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
\<Longrightarrow> irq_slot_empty spec t irq 0 = irq_slot_initialised spec t irq 0"
apply (frule (1) well_formed_slots_of_used_irq_node)
apply (erule irq_slot_empty_initialised_NullCap)
apply (clarsimp simp: bound_irqs_def)
apply blast
done
lemma irq_empty_initialised:
"\<lbrakk>well_formed spec; irq \<notin> bound_irqs spec; irq \<in> used_irqs spec\<rbrakk>
\<Longrightarrow> irq_empty spec t irq = irq_initialised spec t irq"
apply (frule (1) well_formed_used_irqs_have_irq_node, clarsimp)
apply (frule (1) well_formed_irq_is_irq_node)
apply (subst irq_empty_decomp_total, assumption+)
apply (subst irq_initialised_decomp_total, assumption+)
apply (subst irq_node_fields_empty_initialised)
apply (simp add: object_type_object_at object_at_def)
apply (subst irq_slot_empty_initialised, assumption+)
apply simp
done
(* If all the bound IRQs are done, then all the used ones are too.
To show this is true we note that:
- by well_formed_bound_irqs_are_used_irqs:
well_formed spec \<Longrightarrow> bound_irqs spec \<subseteq> used_irqs spec
- empty (used and not bound) IRQs don't need any setting up
- there's no problem having si_irq_caps_at to more IRQ caps.
*)
lemma init_irqs_sep:
"\<lbrace>\<guillemotleft>irqs_empty spec t (used_irqs spec) \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (used_irqs spec) \<and>*
si_objects \<and>* R\<guillemotright> and
K(well_formed spec)\<rbrace>
init_irqs spec orig_caps irq_caps
\<lbrace>\<lambda>_.\<guillemotleft>irqs_initialised spec t (used_irqs spec) \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
si_irq_caps_at irq_caps spec (used_irqs spec) \<and>*
si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_gen_asm)
apply (clarsimp simp: si_irq_caps_at_def irqs_initialised_def irqs_empty_def)
apply (frule well_formed_bound_irqs_are_used_irqs)
apply (frule sep_set_conj_subset_wp
[where P = "sep_map_set_conj (irq_empty spec t) (used_irqs spec) \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>* si_objects"
and Q = "sep_map_set_conj (irq_initialised spec t) (used_irqs spec) \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>* si_objects"
and f = "init_irqs spec orig_caps irq_caps"], simp+)
apply (subst sep.prod.subset_diff, assumption, simp)+
apply (rule hoare_pre, sep_wp init_irqs_bound_irqs_sep [where t=t])
apply (simp add: si_irq_caps_at_def irqs_initialised_def irqs_empty_def sep_conj_assoc)
apply(subgoal_tac "sep_map_set_conj (irq_empty spec t) (used_irqs spec - bound_irqs spec)
= sep_map_set_conj (irq_initialised spec t) (used_irqs spec - bound_irqs spec)", simp)
apply sep_solve
apply (rule sep.prod.cong, simp)
apply (subst irq_empty_initialised, simp+)
apply (erule hoare_chain, sep_solve, sep_solve)
done
end