1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11(* 12 * The layout of the capability space and other parts of the system-initialiser. 13 *) 14theory RootTask_SI 15imports WellFormed_SI 16begin 17 18(****************************************************************** 19 * Definition of the CSpace of the root task. * 20 * This requires a default cap to all of the objects created, * 21 * and a copy of caps to all of the CNodes (for installing caps). * 22 ******************************************************************) 23 24consts 25 si_cnode_id :: cdl_object_id 26 si_asidpool_id :: cdl_object_id 27 si_asidpool_base :: nat 28 29definition 30 si_cnode_size :: cdl_size_bits 31where 32 "si_cnode_size = 12" 33 34(* If we axioimise this size, we need it to be smaller than the word size. 35 * We need this to prove that: 36 - word_bits - si_cnode_size + si_cnode_size = word_bits. 37 - offset (of_nat slot) si_cnode_size = slot 38 *) 39lemma si_cnode_size_less_than_word_size [simp]: 40 "si_cnode_size < word_bits" 41 by (clarsimp simp: si_cnode_size_def word_bits_def) 42 43lemma si_cnode_size_less_than_eq_word_size [simp]: 44 "si_cnode_size \<le> word_bits" 45 by (rule less_imp_le_nat, simp) 46 47lemma si_cnode_size_greater_than_1 [simp]: 48 "1 < si_cnode_size" 49 by (clarsimp simp: si_cnode_size_def) 50 51lemma si_cnode_size_greater_than_2 [simp]: 52 "2 < si_cnode_size" 53 by (clarsimp simp: si_cnode_size_def) 54 55lemma unat_less_2_si_cnode_size: 56 "unat (cptr::32 word) < 2 ^ si_cnode_size 57 \<Longrightarrow> cptr < 2 ^ si_cnode_size" 58 by (metis si_cnode_size_less_than_word_size unat_power_lower32 word_less_nat_alt) 59 60lemma unat_less_2_si_cnode_size': 61 "(cptr::32 word) < 2 ^ si_cnode_size 62 \<Longrightarrow> unat cptr < 2 ^ si_cnode_size" 63 by (metis unat_less_helper word_unat_power) 64 65(* This is stored in the root TCB. *) 66definition 67 si_cspace_cap :: cdl_cap 68where 69 "si_cspace_cap = CNodeCap si_cnode_id 0 (word_bits - si_cnode_size) si_cnode_size" 70 71(* This is the cap the root TCB has to its own root cnode (stored in its root CNode). *) 72definition 73 si_cnode_cap :: cdl_cap 74where 75 "si_cnode_cap = CNodeCap si_cnode_id 0 (word_bits - si_cnode_size) si_cnode_size" 76 77definition 78 root_tcb :: cdl_object 79where 80 "root_tcb = update_slots [tcb_cspace_slot \<mapsto> si_cspace_cap, 81 tcb_vspace_slot \<mapsto> undefined, 82 tcb_replycap_slot \<mapsto> undefined, 83 tcb_caller_slot \<mapsto> undefined, 84 tcb_ipcbuffer_slot \<mapsto> undefined, 85 tcb_pending_op_slot \<mapsto> undefined] (Tcb (default_tcb minBound))" 86 87definition 88 empty_asid :: cdl_asid_pool 89where 90 "empty_asid = \<lparr>cdl_asid_pool_caps = empty_cap_map asid_low_bits\<rparr>" 91 92definition 93 si_asid :: "sep_state \<Rightarrow> bool" 94where 95 "si_asid \<equiv> 96 (si_cnode_id, unat seL4_CapInitThreadASIDPool) \<mapsto>c AsidPoolCap si_asidpool_id si_asidpool_base \<and>* 97 si_asidpool_id \<mapsto>f AsidPool empty_asid \<and>* 98 (\<And>* offset\<in>{offset. offset < 2 ^ asid_low_bits}. 99 (si_asidpool_id, offset) \<mapsto>c -)" 100 101abbreviation "si_tcb_id \<equiv> root_tcb_id" 102 103definition si_objects :: "sep_state \<Rightarrow> bool" 104where 105 "si_objects \<equiv> 106 si_tcb_id \<mapsto>f root_tcb \<and>* 107 si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>* 108 (si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>* 109 (si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* 110 (si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>* 111 (si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>* 112 si_asid" 113 114definition 115 si_objects_extra_caps' :: "cdl_object_id set \<Rightarrow> cdl_cptr list \<Rightarrow> cdl_cptr list \<Rightarrow> sep_state \<Rightarrow> bool" 116where 117 "si_objects_extra_caps' obj_ids free_cptrs untyped_cptrs \<equiv> \<lambda>s. 118 \<exists>untyped_caps all_available_ids. 119 ((\<And>* (cptr, cap) \<in> set (zip untyped_cptrs untyped_caps). (si_cnode_id, unat cptr) \<mapsto>c cap) \<and>* 120 (\<And>* cptr \<in> set (drop (card obj_ids) free_cptrs). (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>* 121 (\<And>* obj_id\<in>all_available_ids. obj_id \<mapsto>o Untyped)) s" 122 123definition 124 si_objects_extra_caps :: "cdl_object_id set \<Rightarrow> cdl_cptr list \<Rightarrow> cdl_cptr list 125 \<Rightarrow> cdl_state \<Rightarrow> sep_state \<Rightarrow> bool" 126where 127 "si_objects_extra_caps obj_ids free_cptrs untyped_cptrs spec \<equiv> \<lambda>s. 128 \<exists>untyped_caps all_available_ids. 129 ((\<And>* (cptr, cap) \<in> set (zip untyped_cptrs untyped_caps). (si_cnode_id, unat cptr) \<mapsto>c cap) \<and>* 130 (\<And>* cptr \<in> set (drop (card obj_ids + card {obj_id \<in> obj_ids. cnode_or_tcb_at obj_id spec}) free_cptrs). 131 (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>* 132 (\<And>* obj_id\<in>all_available_ids. obj_id \<mapsto>o Untyped)) s" 133 134 135lemma distinct_take_drop_append: 136 "distinct xs \<Longrightarrow> set (take b (drop a xs)) \<inter> set (drop (a + b) xs) = {}" 137 by (metis distinct_append distinct_drop take_drop_append) 138 139lemma si_objects_extra_caps'_si_objects_extra_caps: 140 "distinct free_slots \<Longrightarrow> 141 si_objects_extra_caps' obj_ids free_slots untyped_cptrs = 142 (si_objects_extra_caps obj_ids free_slots untyped_cptrs spec \<and>* 143 (\<And>* cptr \<in> set (take (card {obj_id \<in> obj_ids. cnode_or_tcb_at obj_id spec}) 144 (drop (card obj_ids) free_slots)). 145 (si_cnode_id, unat cptr) \<mapsto>c NullCap))" 146 apply (rule ext) 147 apply (clarsimp simp: si_objects_extra_caps'_def si_objects_extra_caps_def sep_conj_exists) 148 apply (rule ex_eqI)+ 149 apply (subst take_drop_append [where a="card obj_ids" and 150 b="card {obj_id \<in> obj_ids. cnode_or_tcb_at obj_id spec}"]) 151 apply clarsimp 152 apply (subst sep.prod.union_disjoint, (simp add: distinct_take_drop_append)+)+ 153 apply (clarsimp simp: sep_conj_ac) 154 done 155 156definition 157 si_irq_nodes :: "cdl_state \<Rightarrow> sep_state \<Rightarrow> bool" 158where 159 "si_irq_nodes spec \<equiv> 160 (\<lambda>s. \<exists>k_irq_table. (\<And>* irq\<in>used_irqs spec. irq \<mapsto>irq k_irq_table irq \<and>* 161 k_irq_table irq \<mapsto>o IRQNode empty_irq_node) s)" 162 163 164(*************************************** 165 * Lemmas about the root task objects. * 166 ***************************************) 167 168lemma is_cnode_cap_si_cspace_cap [simp]: 169 "is_cnode_cap si_cspace_cap" 170 by (clarsimp simp: si_cspace_cap_def) 171 172lemma is_cnode_cap_si_cnode_cap [simp]: 173 "is_cnode_cap si_cnode_cap" 174 by (clarsimp simp: si_cnode_cap_def) 175 176lemma is_tcb_root_tcb [simp]: 177 "is_tcb root_tcb" 178 by (clarsimp simp: root_tcb_def) 179 180lemma cap_guard_size_si_cnode_cap_plus_si_cnode_size [simp]: 181 "cap_guard_size si_cnode_cap + si_cnode_size = word_bits" 182 by (clarsimp simp: si_cnode_cap_def) 183 184lemma cap_object_si_cspace_cap [simp]: 185 "cap_object si_cspace_cap = si_cnode_id" 186 by (clarsimp simp: cap_object_def cap_has_object_def si_cspace_cap_def) 187 188lemma cap_object_si_cnode_cap [simp]: 189 "cap_object si_cnode_cap = si_cnode_id" 190 by (clarsimp simp: cap_object_def cap_has_object_def si_cnode_cap_def) 191 192 193lemma offset_slot_si_cnode_size: 194 "slot < 2^si_cnode_size \<Longrightarrow> offset (of_nat slot) si_cnode_size = slot" 195 by (clarsimp simp: offset_slot) 196 197lemma offset_slot_si_cnode_size': 198 "slot < 2^si_cnode_size \<Longrightarrow> offset slot si_cnode_size = unat slot" 199 by (clarsimp simp: offset_slot') 200 201lemma guard_equal_si_cspace_cap: 202 "src_index < 2 ^ si_cnode_size \<Longrightarrow> guard_equal si_cspace_cap src_index 32" 203 apply (clarsimp simp: si_cspace_cap_def guard_equal_def Let_unfold) 204 apply (subst and_mask_eq_iff_shiftr_0 [THEN iffD1]) 205 apply (clarsimp simp: word_bits_def) 206 apply (erule less_mask_eq) 207 apply (clarsimp simp: mask_def) 208 done 209 210lemma guard_equal_si_cspace_cap': 211 "src_index < 2 ^ si_cnode_size \<Longrightarrow> guard_equal si_cspace_cap src_index word_bits" 212 by (drule guard_equal_si_cspace_cap, simp add: word_bits_def) 213 214lemma guard_equal_si_cnode_cap: 215 "src_index < 2 ^ si_cnode_size \<Longrightarrow> guard_equal si_cnode_cap src_index 32" 216 apply (clarsimp simp: si_cnode_cap_def guard_equal_def Let_unfold) 217 apply (subst and_mask_eq_iff_shiftr_0 [THEN iffD1]) 218 apply (clarsimp simp: word_bits_def) 219 apply (erule less_mask_eq) 220 apply (clarsimp simp: mask_def) 221 done 222 223lemma seL4_CapInitThreadASIDPool_si_cnode_size [simp]: 224 "seL4_CapInitThreadASIDPool < 2 ^ si_cnode_size" 225 by (clarsimp simp: seL4_CapInitThreadASIDPool_def si_cnode_size_def) 226 227lemma guard_equal_si_cspace_cap_seL4_CapInitThreadASIDPool [simp]: 228 "guard_equal si_cspace_cap seL4_CapInitThreadASIDPool word_bits" 229 by (rule guard_equal_si_cspace_cap', simp) 230 231lemma si_cspace_cap_guard_equal: 232 "guard_equal si_cnode_cap src_index 32 \<Longrightarrow> src_index < 2 ^ si_cnode_size" 233 apply (clarsimp simp: si_cnode_cap_def guard_equal_def 234 Let_unfold si_cnode_size_def) 235 apply (subst (asm) shiftr_mask_eq') 236 apply (simp add: word_bits_size word_bits_def) 237 apply (subst (asm) le_mask_iff [symmetric]) 238 apply (clarsimp simp: mask_def) 239 apply (insert word32_less_sub_le [where x=src_index and n=12]) 240 apply (clarsimp simp: word_bits_def) 241 done 242 243lemma one_lvl_lookup_si_cspace_cap [simp]: 244 "one_lvl_lookup si_cspace_cap word_bits si_cnode_size" 245 by (clarsimp simp: one_lvl_lookup_def si_cspace_cap_def) 246 247lemmas one_lvl_lookup_si_cspace_cap' [simp] = 248 one_lvl_lookup_si_cspace_cap [simplified word_bits_def, simplified] 249 250lemma one_lvl_lookup_si_cnode_cap [simp]: 251 "one_lvl_lookup si_cnode_cap word_bits si_cnode_size" 252 by (clarsimp simp: one_lvl_lookup_def si_cnode_cap_def) 253 254lemmas one_lvl_lookup_si_cnode_cap' [simp] = 255 one_lvl_lookup_si_cnode_cap [simplified word_bits_def, simplified] 256 257lemma obj_tcb_root_tcb [simp]: 258 "Tcb (obj_tcb root_tcb) = root_tcb" 259 by (clarsimp simp: obj_tcb_def root_tcb_def update_slots_def) 260 261(*************************** 262 * Lemmas about word size. * 263 ***************************) 264lemma seL4_CapInitThreadCNode_less_than_si_cnode_size [simp]: 265 "seL4_CapInitThreadCNode < 2 ^ si_cnode_size" 266 apply (insert si_cnode_size_greater_than_1) 267 apply (insert power_strict_increasing [where n=1 and a="(2::nat)" and N=si_cnode_size, simplified]) 268 apply (clarsimp) 269 apply (drule of_nat_less_pow_32) 270 apply (clarsimp simp: seL4_CapInitThreadCNode_def)+ 271 done 272 273lemma offset_seL4_CapInitThreadCNode [simp]: 274 "offset seL4_CapInitThreadCNode si_cnode_size = unat seL4_CapInitThreadCNode" 275 by (rule offset_slot', simp) 276 277lemma seL4_CapIRQControl_less_than_si_cnode_size [simp]: 278 "seL4_CapIRQControl < 2 ^ si_cnode_size" 279 apply (simp add: seL4_CapIRQControl_def) 280 apply (insert si_cnode_size_greater_than_2) 281 apply (insert power_strict_increasing [where n=2 and a="(2::nat)" and N=si_cnode_size, simplified]) 282 apply (drule of_nat_less_pow_32, simp_all) 283 done 284 285lemma offset_seL4_CapIRQControl [simp]: 286 "offset seL4_CapIRQControl si_cnode_size = unat seL4_CapIRQControl" 287 by (rule offset_slot', simp) 288 289(* There is a cap in the root cnode that points to the obj_id specified. 290 * This cap should be the default cap to that object. 291 * 292 * This predicate can be used for spec objects, or the duplicated cnode caps. 293 *) 294definition si_cap_at :: "(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 295 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> bool \<Rightarrow> 296 cdl_object_id \<Rightarrow> sep_pred" 297where 298 "si_cap_at t si_caps spec dev obj_id \<equiv> \<lambda>s. 299 \<exists>cap_ptr slot obj kobj_id. 300 ((si_cnode_id, slot) \<mapsto>c default_cap (object_type obj) {kobj_id} (object_size_bits obj) dev) s \<and> 301 si_caps obj_id = Some cap_ptr \<and> 302 unat cap_ptr = slot \<and> 303 cap_ptr < 2 ^ si_cnode_size \<and> 304 cdl_objects spec obj_id = Some obj \<and> 305 t obj_id = Some kobj_id" 306 307definition si_irq_cap_at :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 308 cdl_irq \<Rightarrow> sep_pred" 309where 310 "si_irq_cap_at si_irq_caps spec irq \<equiv> \<lambda>s. 311 \<exists>cap_ptr slot. 312 ((si_cnode_id, slot) \<mapsto>c IrqHandlerCap irq) s \<and> 313 si_irq_caps irq = Some cap_ptr \<and> 314 unat cap_ptr = slot \<and> 315 cap_ptr < 2 ^ si_cnode_size" 316 317definition si_caps_at :: "(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 318 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> bool \<Rightarrow> 319 cdl_object_id set \<Rightarrow> sep_pred" 320where 321 "si_caps_at t si_caps spec dev obj_ids \<equiv> 322 \<And>* obj_id \<in> obj_ids. (si_cap_at t si_caps spec) dev obj_id" 323 324definition si_irq_caps_at :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 325 cdl_irq set \<Rightarrow> sep_pred" 326where 327 "si_irq_caps_at si_irq_caps spec irqs \<equiv> 328 \<And>* irq \<in> irqs. si_irq_cap_at si_irq_caps spec irq" 329 330definition 331 si_obj_cap_at' :: " (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 332 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> bool \<Rightarrow> 333 cdl_object_id \<Rightarrow> cdl_cnode_index \<Rightarrow> sep_pred" 334where 335 "si_obj_cap_at' t si_caps spec dev obj_id slot \<equiv> \<lambda>s. \<exists> spec_cap. 336 si_cap_at t si_caps spec dev (cap_object spec_cap) s \<and> 337 opt_cap (obj_id, slot) spec = Some spec_cap" 338 339definition si_obj_cap_at where 340 "si_obj_cap_at t si_caps spec dev obj_id slot \<equiv> 341 if original_cap_at (obj_id, slot) spec \<and> cap_at cap_has_object (obj_id, slot) spec 342 then si_obj_cap_at' t si_caps spec dev obj_id slot 343 else \<box>" 344 345definition 346 si_obj_caps_at :: "(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 347 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> bool \<Rightarrow> 348 cdl_object_id \<Rightarrow> sep_pred" 349where 350 "si_obj_caps_at t si_caps spec dev obj_id \<equiv> 351 \<And>* slot \<in> dom (slots_of obj_id spec). si_obj_cap_at t si_caps spec dev obj_id slot" 352 353definition 354 si_objs_caps_at :: "(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 355 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> bool \<Rightarrow> 356 cdl_object_id set \<Rightarrow> sep_pred" 357where 358 "si_objs_caps_at t si_caps spec dev obj_ids \<equiv> 359 \<And>* obj_id \<in> obj_ids. (si_obj_caps_at t si_caps spec) dev obj_id" 360 361definition 362 si_spec_irq_cap_at' :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 363 cdl_object_id \<Rightarrow> cdl_cnode_index \<Rightarrow> sep_pred" 364where 365 "si_spec_irq_cap_at' si_irq_caps spec obj_id slot \<equiv> \<lambda>s. \<exists> spec_cap. 366 si_irq_cap_at si_irq_caps spec (cap_irq spec_cap) s \<and> 367 opt_cap (obj_id, slot) spec = Some spec_cap" 368 369definition si_spec_irq_cap_at where 370 "si_spec_irq_cap_at si_irq_caps spec obj_id slot \<equiv> 371 if irqhandler_cap_at (obj_id, slot) spec 372 then si_spec_irq_cap_at' si_irq_caps spec obj_id slot 373 else \<box>" 374 375definition 376 si_spec_irq_caps_at :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 377 cdl_object_id \<Rightarrow> sep_pred" 378where 379 "si_spec_irq_caps_at si_irq_caps spec obj_id \<equiv> 380 \<And>* slot \<in> dom (slots_of obj_id spec). si_spec_irq_cap_at si_irq_caps spec obj_id slot" 381 382definition 383 si_spec_irqs_caps_at :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 384 cdl_object_id set \<Rightarrow> sep_pred" 385where 386 "si_spec_irqs_caps_at si_irq_caps spec obj_ids \<equiv> 387 \<And>* obj_id \<in> obj_ids. si_spec_irq_caps_at si_irq_caps spec obj_id" 388 389definition 390 "si_null_cap_at t si_irq_caps spec obj_id \<equiv> 391 \<lambda>s. \<exists>cap_ptr slot obj kobj_id. 392 ((si_cnode_id, slot) \<mapsto>c NullCap) s \<and> 393 si_irq_caps obj_id = Some cap_ptr \<and> 394 unat cap_ptr = slot \<and> 395 cap_ptr < 2 ^ si_cnode_size \<and> 396 cdl_objects spec obj_id = Some obj \<and> t obj_id = Some kobj_id" 397 398definition 399 "si_null_irq_cap_at si_irq_caps spec irq \<equiv> 400 \<lambda>s. \<exists>cap_ptr slot. 401 ((si_cnode_id, slot) \<mapsto>c NullCap) s \<and> 402 si_irq_caps irq = Some cap_ptr \<and> 403 unat cap_ptr = slot \<and> 404 cap_ptr < 2 ^ si_cnode_size" 405 406definition 407 si_spec_obj_null_cap_at' :: " (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 408 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 409 cdl_object_id \<Rightarrow> cdl_cnode_index \<Rightarrow> sep_pred" 410where 411 "si_spec_obj_null_cap_at' t si_irq_caps spec obj_id slot \<equiv> \<lambda>s. \<exists> spec_cap. 412 si_null_cap_at t si_irq_caps spec (cap_object spec_cap) s \<and> 413 opt_cap (obj_id, slot) spec = Some spec_cap" 414 415definition si_spec_obj_null_cap_at where 416 "si_spec_obj_null_cap_at t si_irq_caps spec obj_id slot \<equiv> 417 if original_cap_at (obj_id, slot) spec \<and> cap_at cap_has_object (obj_id, slot) spec 418 then si_spec_obj_null_cap_at' t si_irq_caps spec obj_id slot 419 else \<box>" 420 421definition 422 si_spec_obj_null_caps_at :: "(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 423 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 424 cdl_object_id \<Rightarrow> sep_pred" 425where 426 "si_spec_obj_null_caps_at t si_irq_caps spec obj_id \<equiv> 427 \<And>* slot \<in> dom (slots_of obj_id spec). si_spec_obj_null_cap_at t si_irq_caps spec obj_id slot" 428 429definition 430 si_spec_objs_null_caps_at :: "(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 431 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 432 cdl_object_id set \<Rightarrow> sep_pred" 433where 434 "si_spec_objs_null_caps_at t si_irq_caps spec obj_ids \<equiv> 435 \<And>* obj_id \<in> obj_ids. si_spec_obj_null_caps_at t si_irq_caps spec obj_id" 436 437definition 438 si_spec_irq_null_cap_at' :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 439 cdl_object_id \<Rightarrow> cdl_cnode_index \<Rightarrow> sep_pred" 440where 441 "si_spec_irq_null_cap_at' si_irq_caps spec obj_id slot \<equiv> \<lambda>s. \<exists> spec_cap. 442 si_null_irq_cap_at si_irq_caps spec (cap_irq spec_cap) s \<and> 443 opt_cap (obj_id, slot) spec = Some spec_cap \<and> \<not>is_untyped_cap spec_cap" 444 445definition si_spec_irq_null_cap_at where 446 "si_spec_irq_null_cap_at si_irq_caps spec obj_id slot \<equiv> 447 if irqhandler_cap_at (obj_id, slot) spec 448 then si_spec_irq_null_cap_at' si_irq_caps spec obj_id slot 449 else \<box>" 450 451definition 452 si_spec_irq_null_caps_at :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 453 cdl_object_id \<Rightarrow> sep_pred" 454where 455 "si_spec_irq_null_caps_at si_irq_caps spec obj_id \<equiv> 456 \<And>* slot \<in> dom (slots_of obj_id spec). si_spec_irq_null_cap_at si_irq_caps spec obj_id slot" 457 458definition 459 si_spec_irqs_null_caps_at :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 460 cdl_object_id set \<Rightarrow> sep_pred" 461where 462 "si_spec_irqs_null_caps_at si_irq_caps spec obj_ids \<equiv> 463 \<And>* obj_id \<in> obj_ids. si_spec_irq_null_caps_at si_irq_caps spec obj_id" 464 465definition si_null_caps_at :: "(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> 466 (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 467 cdl_object_id set \<Rightarrow> sep_pred" 468where 469 "si_null_caps_at t si_caps spec obj_ids \<equiv> 470 \<And>* obj_id \<in> obj_ids. si_null_cap_at t si_caps spec obj_id" 471 472 473lemma si_cap_at_less_si_cnode_size: 474 "\<lbrakk>\<guillemotleft>si_cap_at t opt_sel4_cap spec dev obj_id \<and>* R\<guillemotright> s; 475 Some cap_ptr = opt_sel4_cap obj_id\<rbrakk> 476 \<Longrightarrow> cap_ptr < 2 ^ si_cnode_size" 477 by (clarsimp simp: si_cap_at_def sep_conj_exists) 478 479lemma si_irq_cap_at_less_si_cnode_size: 480 "\<lbrakk>\<guillemotleft>si_irq_cap_at opt_sel4_cap spec obj_id \<and>* R\<guillemotright> s; 481 Some cap_ptr = opt_sel4_cap obj_id\<rbrakk> 482 \<Longrightarrow> cap_ptr < 2 ^ si_cnode_size" 483 by (clarsimp simp: si_irq_cap_at_def sep_conj_exists) 484 485lemma si_cap_at_has_k_obj_id: 486 "\<lbrakk>\<guillemotleft>si_cap_at t opt_sel4_cap spec dev obj_id \<and>* R\<guillemotright> s\<rbrakk> 487 \<Longrightarrow> \<exists>cap_object_id. t obj_id = Some cap_object_id" 488 by (clarsimp simp: si_cap_at_def sep_conj_exists) 489 490(****************************************************** 491 * Using just si_cap_at when you have si_caps_at. * 492 ******************************************************) 493 494lemma valid_si_caps_at_si_cap_at: 495 "\<lbrakk>finite obj_ids; obj_id \<in> obj_ids; 496 (\<And>R. \<lbrace>\<guillemotleft>si_cap_at t orig_caps spec dev obj_id \<and>* P \<and>* R\<guillemotright>\<rbrace> 497 f 498 \<lbrace>\<lambda>_.\<guillemotleft>si_cap_at t orig_caps spec dev obj_id \<and>* Q \<and>* R\<guillemotright>\<rbrace>)\<rbrakk> 499 \<Longrightarrow> 500 \<lbrace>\<guillemotleft>si_caps_at t orig_caps spec dev obj_ids \<and>* P \<and>* R\<guillemotright>\<rbrace> 501 f 502 \<lbrace>\<lambda>_.\<guillemotleft>si_caps_at t orig_caps spec dev obj_ids \<and>* Q \<and>* R\<guillemotright>\<rbrace>" 503 apply (clarsimp simp: si_caps_at_def) 504 apply (drule sep_set_conj_map_singleton_wp [where f=f and 505 I="si_cap_at t orig_caps spec dev" and P=P and Q=Q and R=R, rotated]) 506 apply (clarsimp simp: sep_conj_ac)+ 507 done 508 509(********************************************************** 510 * The pre and post conditions of the system initialiser. * 511 **********************************************************) 512 513(* That the boot info is valid, and that there are enough free slots to initialise a system. *) 514definition 515 valid_boot_info 516where 517 "valid_boot_info bootinfo spec \<equiv> \<lambda>s. 518 \<exists>untyped_caps fstart fend ustart uend. 519 ((\<And>*(cptr, cap) \<in> set (zip [ustart .e. uend - 1] untyped_caps). (si_cnode_id, unat cptr) \<mapsto>c cap) \<and>* 520 (\<And>* cptr \<in> set [fstart .e. fend - 1]. (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>* 521 (\<And>* obj_id\<in>(\<Union>cap\<in>set untyped_caps. cap_free_ids cap). obj_id \<mapsto>o Untyped) \<and>* 522 si_objects \<and>* si_irq_nodes spec) s \<and> 523 card (dom (cdl_objects spec)) + 524 card {obj_id. cnode_or_tcb_at obj_id spec} \<le> unat fend - unat fstart \<and> 525 length untyped_caps = unat uend - unat ustart \<and> 526 distinct_sets (map cap_free_ids untyped_caps) \<and> 527 list_all is_full_untyped_cap untyped_caps \<and> 528 list_all well_formed_untyped_cap untyped_caps \<and> 529 list_all (\<lambda>c. \<not> is_device_cap c) untyped_caps \<and> 530 bi_untypes bootinfo = (ustart, uend) \<and> 531 bi_free_slots bootinfo = (fstart, fend) \<and> 532 ustart < 2 ^ si_cnode_size \<and> 533 (uend - 1) < 2 ^ si_cnode_size \<and> 534 fstart < 2 ^ si_cnode_size \<and> 535 (fend - 1) < 2 ^ si_cnode_size \<and> 536 uend \<noteq> 0 \<and> fend \<noteq> 0" 537 538definition 539 si_final_objects :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> sep_pred" 540where 541 "si_final_objects spec t \<equiv> \<lambda>s. 542 \<exists>dup_caps (untyped_cptrs::32 word list) (free_cptrs::32 word list) untyped_caps all_available_ids. 543 ((\<And>* cptr \<in> set (take (card (dom (cdl_objects spec))) free_cptrs). 544 (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>* 545 (\<And>* cptr \<in> set (drop (card (dom (cdl_objects spec)) + 546 card ({obj_id. cnode_or_tcb_at obj_id spec})) free_cptrs). 547 (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>* 548 (\<And>* (cptr, untyped_cap) \<in> set (zip untyped_cptrs untyped_caps). 549 (si_cnode_id, unat cptr) \<mapsto>c untyped_cap) \<and>* 550 (\<And>* obj_id \<in> all_available_ids. obj_id \<mapsto>o Untyped) \<and>* 551 (\<And>* obj_id \<in> {obj_id. cnode_or_tcb_at obj_id spec}. (si_cap_at t dup_caps spec False obj_id)) \<and>* 552 si_objects) s" 553 554(******************************************************** 555 * Conversion of si_objs_caps_at to si_caps_at * 556 ********************************************************) 557 558lemma orig_cap_rewrite: 559 "Set.filter (\<lambda>cap_ref. original_cap_at cap_ref spec \<and> cap_at cap_has_object cap_ref spec) 560 (SIGMA obj_id:{obj_id. cnode_at obj_id spec}. 561 dom (slots_of obj_id spec)) = 562 {cap_ref. original_cap_at cap_ref spec \<and> object_cap_ref cap_ref spec}" 563 by (auto simp: object_cap_ref_def opt_cap_def object_at_def cap_at_def real_object_at_def 564 split: option.splits) 565 566lemma slots_tcb: 567 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; 568 cdl_objects spec obj_id = Some obj; obj = Tcb tcb\<rbrakk> \<Longrightarrow> 569 slot = 0 \<or> 570 slot = 1 \<or> 571 slot = 2 \<or> 572 slot = 3 \<or> 573 slot = 4 \<or> 574 slot = 5 \<or> 575 slot = 6" 576 apply (frule (1) well_formed_object_slots) 577 apply (drule (1) well_formed_well_formed_tcb) 578 apply (clarsimp simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def) 579 apply (drule (1) dom_eqD) 580 apply (clarsimp simp: object_default_state_def2 dom_object_slots_default_tcb 581 tcb_pending_op_slot_def tcb_boundntfn_slot_def) 582 done 583 584lemma object_at_dom_cdl_objects: 585 "object_at P obj_id s \<Longrightarrow> obj_id \<in> dom (cdl_objects s)" 586 by (clarsimp simp: object_at_def) 587 588lemma foo: 589 "\<lbrakk>well_formed spec; irq_node_at obj_id spec\<rbrakk> 590 \<Longrightarrow> obj_id \<in> irq_nodes spec" 591 by (metis irq_nodes_def mem_Collect_eq) 592 593lemma well_formed_irqhandler_cap_in_cnode: 594 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; 595 is_irqhandler_cap cap; cdl_objects spec obj_id = Some obj\<rbrakk> 596 \<Longrightarrow> is_cnode obj" 597 apply (case_tac obj) 598 apply (fastforce simp: opt_cap_def slots_of_def object_slots_def opt_object_def 599 is_cnode_def object_at_def is_asidpool_def)+ 600 apply (frule (3) slots_tcb) 601 apply (drule (1) well_formed_well_formed_tcb) 602 apply (clarsimp simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def) 603 apply (erule allE [where x=slot]) 604 apply (simp add: tcb_slot_defs cap_type_def split: cdl_cap.splits) 605 apply (fastforce simp: opt_cap_def slots_of_def object_slots_def opt_object_def 606 is_cnode_def object_at_def is_asidpool_def) 607 apply (frule_tac obj_id=obj_id in well_formed_asidpool_at, simp add: object_at_def) 608 apply (frule (1) well_formed_pt, simp add: object_at_def, simp+) 609 apply (frule (1) well_formed_pd, simp add: object_at_def, simp+) 610 apply (clarsimp simp: is_fake_pt_cap_def split: cdl_cap.splits) 611 apply (fastforce simp: opt_cap_def slots_of_def object_slots_def opt_object_def 612 is_cnode_def object_at_def is_asidpool_def)+ 613 apply (frule (1) well_formed_well_formed_irq_node) 614 apply (fastforce simp: well_formed_irq_node_def opt_cap_def slots_of_def opt_object_def 615 object_at_def irq_nodes_def is_irq_node_def) 616 done 617 618lemma well_formed_irqhandler_cap_in_cnode_at: 619 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; is_irqhandler_cap cap\<rbrakk> 620 \<Longrightarrow> cnode_at obj_id spec" 621 apply (frule opt_cap_cdl_objects, clarsimp) 622 apply (drule (3) well_formed_irqhandler_cap_in_cnode) 623 apply (clarsimp simp: object_at_def) 624 done 625 626lemma irqhandler_cap_rewrite: 627 "well_formed spec \<Longrightarrow> 628 Set.filter (\<lambda>irq. irqhandler_cap_at irq spec) 629 (SIGMA obj_id:{obj_id. cnode_at obj_id spec}. 630 dom (slots_of obj_id spec)) = 631 {cap_ref. irqhandler_cap_at cap_ref spec}" 632 apply (clarsimp simp: object_cap_ref_def object_at_def cap_at_def 633 split: option.splits) 634 apply rule 635 apply clarsimp 636 apply clarsimp 637 apply (frule opt_cap_dom_cdl_objects) 638 apply (frule opt_cap_dom_slots_of, clarsimp) 639 apply (frule (3) well_formed_irqhandler_cap_in_cnode) 640 apply (frule (1) well_formed_well_formed_irq_node) 641 apply (clarsimp simp: well_formed_irq_node_def object_at_def 642 opt_cap_def slots_of_def opt_object_def dom_def) 643 done 644 645lemma well_formed_object_cap_real: 646 "well_formed spec 647 \<Longrightarrow> object_cap_ref cap_ref spec = 648 (cap_at_to_real_object cap_ref spec \<and> 649 cnode_at (fst cap_ref) spec)" 650 apply (clarsimp simp: cap_at_def cap_at_to_real_object_def object_cap_ref_def) 651 apply (rule iffI) 652 apply clarsimp 653 apply (drule (1) well_formed_well_formed_cap_to_real_object', simp) 654 apply (clarsimp simp: well_formed_cap_to_real_object_def real_object_at_def) 655 apply (clarsimp simp: real_object_at_def opt_cap_dom_cdl_objects) 656 done 657 658(* This lemma converts between the two represenatations of the fact that the 659 * root task has orig caps to each of the objects. 660 * 661 * This can be specified either: 662 * - on the objects themselves. 663 * - on the cap slots of CNodes that have a orig cap in them. 664 * 665 * This relies on the bijection between orig capabilities and objects in the spec. 666 *) 667 668lemma si_caps_at_conversion: 669 "\<lbrakk>well_formed spec; 670 real_ids = {obj_id. real_object_at obj_id spec}; 671 cnode_ids = {obj_id. cnode_at obj_id spec}\<rbrakk> 672 \<Longrightarrow> si_objs_caps_at t si_caps spec dev cnode_ids = 673 si_caps_at t si_caps spec dev real_ids" 674 apply (clarsimp simp: si_objs_caps_at_def si_obj_caps_at_def [abs_def] 675 si_obj_cap_at_def [abs_def] si_caps_at_def) 676 apply (subst sep.prod.Sigma, clarsimp+) 677 apply (clarsimp simp: split_def) 678 apply (subst sep_map_set_conj_restrict_predicate) 679 apply (rule finite_SigmaI, clarsimp+) 680 apply (subst orig_cap_rewrite) 681 apply (frule well_formed_bij) 682 apply (clarsimp simp: bij_betw_def) 683 apply (rule sep_map_set_conj_reindex_cong [where f="\<lambda>cap_ref. cap_ref_object cap_ref spec", symmetric]) 684 apply (subst well_formed_object_cap_real, simp+) 685 apply (simp add: real_objects_def real_object_at_def) 686 apply (subst well_formed_object_cap_real, simp+) 687 apply (clarsimp simp: cap_ref_object_def object_cap_ref_def si_obj_cap_at'_def) 688 done 689 690 691lemma si_null_caps_at_conversion: 692 "\<lbrakk>well_formed spec; 693 real_ids = {obj_id. real_object_at obj_id spec}; 694 cnode_ids = {obj_id. cnode_at obj_id spec}\<rbrakk> 695 \<Longrightarrow> si_spec_objs_null_caps_at t si_caps spec cnode_ids = 696 si_null_caps_at t si_caps spec real_ids" 697 apply (clarsimp simp: si_spec_objs_null_caps_at_def si_spec_obj_null_caps_at_def [abs_def] 698 si_spec_obj_null_cap_at_def [abs_def] si_null_caps_at_def) 699 apply (subst sep.prod.Sigma, clarsimp+) 700 apply (clarsimp simp: split_def) 701 apply (subst sep_map_set_conj_restrict_predicate) 702 apply (rule finite_SigmaI, clarsimp+) 703 apply (subst orig_cap_rewrite) 704 apply (frule well_formed_bij) 705 apply (clarsimp simp: bij_betw_def) 706 apply (rule sep_map_set_conj_reindex_cong [where f="\<lambda>cap_ref. cap_ref_object cap_ref spec" 707 and h="(si_null_cap_at t si_caps spec)" 708 and B="{obj_id. real_object_at obj_id spec}", symmetric]) 709 apply (subst well_formed_object_cap_real, simp+) 710 apply (simp add: real_objects_def real_object_at_def) 711 apply (subst well_formed_object_cap_real, simp+) 712 apply (clarsimp simp: cap_ref_object_def object_cap_ref_def si_spec_obj_null_cap_at'_def) 713 done 714 715lemma si_null_caps_at_reindex: 716 "\<lbrakk>distinct (obj_ids::32 word list); distinct (free_cptrs); 717 orig_caps = map_of (zip obj_ids free_cptrs); 718 length obj_ids \<le> length free_cptrs\<rbrakk> 719 \<Longrightarrow> (\<And>* obj_id\<in>set obj_ids. 720 (\<lambda>s. \<exists>cap_ptr. ((si_cnode_id, unat cap_ptr) \<mapsto>c NullCap) s \<and> 721 orig_caps obj_id = Some cap_ptr)) 722 = (\<And>* cptr\<in>set (take (length obj_ids) free_cptrs). 723 (si_cnode_id, unat cptr) \<mapsto>c NullCap)" 724 apply (rule sep_map_set_conj_reindex_cong [symmetric, where 725 f="\<lambda>obj_id. the (orig_caps obj_id)" 726 and h="\<lambda>cptr. (si_cnode_id, unat cptr) \<mapsto>c NullCap" 727 and B="set (take (length obj_ids) free_cptrs)"]) 728 apply clarsimp 729 apply (erule (2) map_of_zip_inj') 730 apply clarsimp 731 apply (subst zip_take_length[symmetric]) 732 apply (subst map_of_zip_range) 733 apply (clarsimp simp: min_def) 734 apply assumption 735 apply simp 736 apply clarsimp 737 apply (rule ext) 738 apply rule 739 apply clarsimp 740 apply (rule_tac x="the (map_of (zip obj_ids free_cptrs) a)" in exI) 741 apply clarsimp 742 apply (frule_tac x=a in map_of_zip_is_Some', clarsimp) 743 done 744 745lemma si_null_caps_at_simplified_helper: 746 "\<lbrakk>(si_null_caps_at t orig_caps spec obj_ids) s\<rbrakk> \<Longrightarrow> 747 (\<And>* obj_id \<in> obj_ids. (\<lambda>s. \<exists>cap_ptr. ((si_cnode_id, unat cap_ptr) \<mapsto>c NullCap) s \<and> 748 orig_caps obj_id = Some cap_ptr)) s" 749 apply (clarsimp simp: si_null_caps_at_def si_null_cap_at_def [abs_def]) 750 apply (erule sep_map_set_conj_impl) 751 apply blast 752 apply clarsimp 753 done 754 755lemma si_null_caps_at_simplified: 756 "\<lbrakk>(si_spec_objs_null_caps_at t si_caps spec cnode_ids) s; 757 well_formed spec; 758 cnode_ids = {obj_id. cnode_at obj_id spec}; 759 real_ids = {obj_id. real_object_at obj_id spec}; 760 real_ids = set obj_ids; 761 distinct obj_ids; distinct free_cptrs; 762 si_caps = map_of (zip obj_ids free_cptrs); 763 length obj_ids \<le> length free_cptrs\<rbrakk> \<Longrightarrow> 764 (\<And>* cptr \<in> set (take (length obj_ids) free_cptrs). ((si_cnode_id, unat cptr) \<mapsto>c NullCap)) s" 765 apply (subst (asm) si_null_caps_at_conversion, assumption+) 766 apply (drule si_null_caps_at_simplified_helper) 767 apply (subst si_null_caps_at_reindex [symmetric], simp+) 768 done 769 770lemma map_of_zip_range': 771 "\<lbrakk>length xs = length ys; distinct xs; set xs = X\<rbrakk> 772 \<Longrightarrow> (\<lambda>x. (the (map_of (zip xs ys) x))) ` X = set ys" 773 by (metis map_of_zip_range) 774 775 776 777 778lemma si_irq_caps_at_conversion: 779 "\<lbrakk>well_formed spec; 780 cnode_ids = {obj_id. cnode_at obj_id spec}; 781 irqs = used_irqs spec\<rbrakk> 782 \<Longrightarrow> si_spec_irqs_caps_at irq_caps spec cnode_ids = 783 si_irq_caps_at irq_caps spec irqs" 784 apply (clarsimp simp: si_spec_irqs_caps_at_def si_irq_caps_at_def 785 si_spec_irq_caps_at_def [abs_def] 786 si_spec_irq_cap_at_def [abs_def]) 787 apply (subst sep.prod.Sigma, clarsimp+) 788 apply (clarsimp simp: split_def) 789 apply (subst sep_map_set_conj_restrict_predicate) 790 apply (rule finite_SigmaI, clarsimp+) 791 apply (subst irqhandler_cap_rewrite, assumption) 792 apply (frule well_formed_irqhandler_bij) 793 apply (clarsimp simp: bij_betw_def) 794 apply (rule sep_map_set_conj_reindex_cong [where f="\<lambda>cap_ref. cap_ref_irq cap_ref spec", symmetric], simp+) 795 apply (clarsimp simp: si_spec_irq_cap_at'_def cap_ref_irq_def cap_at_def) 796 done 797 798definition si_null_irq_caps_at :: "(cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_state \<Rightarrow> 799 cdl_irq set \<Rightarrow> sep_pred" 800where 801 "si_null_irq_caps_at si_irq_caps spec irqs \<equiv> 802 \<And>* irq \<in> irqs. si_null_irq_cap_at si_irq_caps spec irq" 803 804lemma si_null_irq_caps_at_simplified_helper: 805 "\<lbrakk>(si_null_irq_caps_at si_irq_caps spec irqs) s\<rbrakk> \<Longrightarrow> 806 (\<And>* irq \<in> irqs. (\<lambda>s. \<exists>cap_ptr. ((si_cnode_id, unat cap_ptr) \<mapsto>c NullCap) s \<and> 807 si_irq_caps irq = Some cap_ptr)) s" 808 apply (clarsimp simp: si_null_irq_caps_at_def si_null_irq_cap_at_def) 809 apply (erule sep_map_set_conj_impl) 810 apply blast 811 apply clarsimp 812 done 813 814lemma map_of_zip_inj2: 815 "\<lbrakk>distinct xs; distinct ys; length xs \<le> length ys; set xs = X\<rbrakk> 816 \<Longrightarrow> inj_on (\<lambda>x. the (map_of (zip xs ys) x)) X" 817 by (metis map_of_zip_inj') 818 819lemma opt_cap_has_slots: 820 "\<lbrakk>opt_cap (obj_id, slot) spec = Some cap\<rbrakk> 821 \<Longrightarrow> object_at has_slots obj_id spec" 822 by (auto simp: object_at_def has_slots_def opt_cap_def slots_of_def opt_object_def object_slots_def 823 split: option.splits cdl_object.splits) 824 825lemma well_formed_non_ntfn_in_real_object: 826 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; \<not>is_ntfn_cap cap; cap \<noteq> NullCap\<rbrakk> 827 \<Longrightarrow> real_object_at obj_id spec" 828 apply (frule opt_cap_cdl_objects, clarsimp) 829 apply (frule (1) well_formed_well_formed_irq_node) 830 apply (clarsimp simp: well_formed_irq_node_def real_object_at_def 831 opt_cap_def slots_of_def opt_object_def opt_cap_dom_cdl_objects) 832 done 833 834 835lemma irqhandler_cap_at_simp: 836 "well_formed spec \<Longrightarrow> 837 {(obj_id, slot). cnode_at obj_id spec \<and> irqhandler_cap_at (obj_id, slot) spec} = 838 {(obj_id, slot). irqhandler_cap_at (obj_id, slot) spec}" 839 apply (safe) 840 apply (clarsimp simp: cap_at_def) 841 apply (frule (2) well_formed_irqhandler_cap_in_cnode_at) 842 apply (frule (1) well_formed_non_ntfn_in_real_object, simp+) 843 done 844 845lemma orig_cap_rewrite_v2: 846 "(SIGMA obj_id:{obj_id. cnode_at obj_id spec}. dom (slots_of obj_id spec)) = 847 {(obj_id, slot). cnode_at obj_id spec \<and> slots_of obj_id spec slot \<noteq> None}" 848 by auto 849 850lemma rewrite_irqhandler_cap_at: 851 "well_formed spec \<Longrightarrow> 852 Set.filter (\<lambda>cap_ref. irqhandler_cap_at cap_ref spec) 853 (SIGMA obj_id:{obj_id. cnode_at obj_id spec}. dom (slots_of obj_id spec)) = 854 {(obj_id, slot). irqhandler_cap_at (obj_id, slot) spec}" 855 apply (subst irqhandler_cap_at_simp [symmetric]) 856 by (auto simp: opt_cap_def cap_at_def) 857 858lemma well_formed_used_irqs_rewrite: 859 "well_formed spec \<Longrightarrow> 860 (\<lambda>cap_ref. cap_ref_irq cap_ref spec) ` {(obj_id, slot). irqhandler_cap_at (obj_id, slot) spec} = 861 used_irqs spec" 862 apply (drule well_formed_irqhandler_bij) 863 apply (auto simp: bij_betw_def) 864 done 865 866 867lemma si_irq_null_caps_at_simplified: 868 "\<lbrakk>(si_spec_irqs_null_caps_at irq_caps spec {obj_id. cnode_at obj_id spec}) s; 869 well_formed spec; 870 distinct irqs; distinct free_cptrs; 871 set irqs = used_irqs spec; 872 irq_caps = map_of (zip irqs free_cptrs); 873 length irqs \<le> length free_cptrs\<rbrakk> \<Longrightarrow> 874 (\<And>* cptr \<in> set (take (length irqs) free_cptrs). ((si_cnode_id, unat cptr) \<mapsto>c NullCap)) s" 875 apply (clarsimp simp: si_spec_irqs_null_caps_at_def si_spec_irq_null_caps_at_def 876 si_spec_irq_null_cap_at_def si_spec_irqs_caps_at_def) 877 apply (subst (asm) sep.prod.Sigma, clarsimp+) 878 apply (clarsimp simp: split_def) 879 apply (subst (asm) sep_map_set_conj_restrict_predicate, rule finite_SigmaI, clarsimp+) 880 apply (subst (asm) rewrite_irqhandler_cap_at, simp) 881 apply (subst (asm) sep_map_set_conj_reindex_cong [where 882 f = "\<lambda>cap_ref. cap_ref_irq cap_ref spec" 883 and h = "si_null_irq_cap_at (map_of (zip irqs free_cptrs)) spec", symmetric]) 884 apply (drule well_formed_irqhandler_bij) 885 apply (clarsimp simp: bij_betw_def cond_case_prod_eta) 886 apply simp 887 apply (clarsimp simp: si_spec_irq_null_cap_at'_def cap_at_def cap_ref_irq_def) 888 apply clarsimp 889 apply (drule si_null_irq_caps_at_simplified_helper [simplified si_null_irq_caps_at_def]) 890 apply (subst (asm) sep_map_set_conj_reindex_cong [symmetric, where 891 f = "\<lambda>irq. the ( map_of (zip irqs free_cptrs) irq)" 892 and h = "\<lambda>cptr. (si_cnode_id, unat cptr) \<mapsto>c NullCap" 893 and B = "set (take (length irqs) free_cptrs)"]) 894 apply (subst well_formed_used_irqs_rewrite, assumption) 895 apply (metis map_of_zip_inj') 896 apply (subst well_formed_used_irqs_rewrite, assumption) 897 apply (subst zip_take_length[symmetric], subst map_of_zip_range', simp+) 898 apply (rule ext) 899 apply rule 900 apply clarsimp 901 apply (rule_tac x="the (map_of (zip irqs free_cptrs) a)" in exI) 902 apply clarsimp 903 apply (frule_tac x1="(cap_irq (the (opt_cap (aa, b) spec)))" in map_of_zip_is_Some'[THEN iffD1], clarsimp) 904 apply (fastforce simp: cap_at_def used_irqs_def all_caps_def) 905 apply (clarsimp simp: cap_ref_irq_def) 906 apply simp 907 done 908 909end 910