1(* 2 * Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9 *) 10 11(* 12 Refinement for interrupt controller operations 13*) 14 15theory Interrupt_R 16imports Ipc_R Invocations_R 17begin 18 19context Arch begin 20 21(*FIXME: arch_split: move up *) 22requalify_types 23 irqcontrol_invocation 24 25lemmas [crunch_def] = decodeIRQControlInvocation_def performIRQControl_def 26 27context begin global_naming global 28 29(*FIXME: arch_split: move up *) 30requalify_types 31 Invocations_H.irqcontrol_invocation 32 33(*FIXME: arch_split*) 34requalify_facts 35 Interrupt_H.decodeIRQControlInvocation_def 36 Interrupt_H.performIRQControl_def 37 38end 39end 40 41primrec 42 irq_handler_inv_relation :: "irq_handler_invocation \<Rightarrow> irqhandler_invocation \<Rightarrow> bool" 43where 44 "irq_handler_inv_relation (Invocations_A.ACKIrq irq) x = (x = AckIRQ irq)" 45| "irq_handler_inv_relation (Invocations_A.ClearIRQHandler irq) x = (x = ClearIRQHandler irq)" 46| "irq_handler_inv_relation (Invocations_A.SetIRQHandler irq cap ptr) x = 47 (\<exists>cap'. x = SetIRQHandler irq cap' (cte_map ptr) \<and> cap_relation cap cap')" 48 49consts 50 interrupt_control_relation :: "arch_irq_control_invocation \<Rightarrow> Arch.irqcontrol_invocation \<Rightarrow> bool" 51 52primrec 53 arch_irq_control_inv_relation :: "arch_irq_control_invocation \<Rightarrow> Arch.irqcontrol_invocation \<Rightarrow> bool" 54where 55 "arch_irq_control_inv_relation (ARM_A.ArchIRQControlIssue i ptr1 ptr2 t) x = 56 (x = ARM_H.IssueIRQHandler i (cte_map ptr1) (cte_map ptr2) t)" 57 58primrec 59 irq_control_inv_relation :: "irq_control_invocation \<Rightarrow> irqcontrol_invocation \<Rightarrow> bool" 60where 61 "irq_control_inv_relation (Invocations_A.IRQControl irq slot slot') x 62 = (x = IssueIRQHandler irq (cte_map slot) (cte_map slot'))" 63| "irq_control_inv_relation (Invocations_A.ArchIRQControl ivk) x 64 = (\<exists>ivk'. x = ArchIRQControl ivk' \<and> arch_irq_control_inv_relation ivk ivk')" 65 66primrec 67 irq_handler_inv_valid' :: "irqhandler_invocation \<Rightarrow> kernel_state \<Rightarrow> bool" 68where 69 "irq_handler_inv_valid' (AckIRQ irq) = (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive)" 70| "irq_handler_inv_valid' (ClearIRQHandler irq) = \<top>" 71| "irq_handler_inv_valid' (SetIRQHandler irq cap cte_ptr) 72 = (valid_cap' cap and valid_cap' (IRQHandlerCap irq) 73 and K (isNotificationCap cap) 74 and cte_wp_at' (badge_derived' cap \<circ> cteCap) cte_ptr 75 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = IRQHandlerCap irq) ptr' s) 76 and ex_cte_cap_wp_to' isCNodeCap cte_ptr)" 77 78primrec 79 arch_irq_control_inv_valid' :: "Arch.irqcontrol_invocation \<Rightarrow> kernel_state \<Rightarrow> bool" 80where 81 "arch_irq_control_inv_valid' (ARM_H.IssueIRQHandler irq p p' t) = 82 (cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) p and 83 cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) p' and 84 ex_cte_cap_to' p and real_cte_at' p and 85 (Not o irq_issued' irq) and K (irq \<le> maxIRQ))" 86 87primrec 88 irq_control_inv_valid' :: "irqcontrol_invocation \<Rightarrow> kernel_state \<Rightarrow> bool" 89where 90 "irq_control_inv_valid' (ArchIRQControl ivk) = arch_irq_control_inv_valid' ivk" 91| "irq_control_inv_valid' (IssueIRQHandler irq ptr ptr') = 92 (cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) ptr and 93 cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) ptr' and 94 ex_cte_cap_to' ptr and real_cte_at' ptr and 95 (Not o irq_issued' irq) and K (irq \<le> maxIRQ))" 96 97context begin interpretation Arch . (*FIXME: arch_split*) 98 99lemma decode_irq_handler_corres: 100 "\<lbrakk> list_all2 cap_relation (map fst caps) (map fst caps'); 101 list_all2 (\<lambda>p pa. snd pa = cte_map (snd p)) caps caps' \<rbrakk> \<Longrightarrow> 102 corres (ser \<oplus> irq_handler_inv_relation) invs invs' 103 (decode_irq_handler_invocation label irq caps) 104 (decodeIRQHandlerInvocation label irq caps')" 105 apply (simp add: decode_irq_handler_invocation_def decodeIRQHandlerInvocation_def 106 split del: if_split) 107 apply (cases caps) 108 apply (simp add: returnOk_def split: invocation_label.split list.splits split del: if_split) 109 apply (clarsimp simp: list_all2_Cons1 split del: if_split) 110 apply (simp add: returnOk_def split: invocation_label.split list.splits) 111 apply (clarsimp split: cap_relation_split_asm arch_cap.split_asm simp: returnOk_def) 112 done 113 114crunch inv[wp]: decodeIRQHandlerInvocation "P" 115 (simp: crunch_simps) 116 117lemma decode_irq_handler_valid'[wp]: 118 "\<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap \<in> set caps. s \<turnstile>' fst cap) 119 \<and> (\<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = IRQHandlerCap irq) ptr' s) 120 \<and> (\<forall>cap \<in> set caps. \<forall>r \<in> cte_refs' (fst cap) (irq_node' s). ex_cte_cap_to' r s) 121 \<and> (\<forall>cap \<in> set caps. ex_cte_cap_wp_to' isCNodeCap (snd cap) s) 122 \<and> (\<forall>cap \<in> set caps. cte_wp_at' (badge_derived' (fst cap) \<circ> cteCap) (snd cap) s) 123 \<and> s \<turnstile>' IRQHandlerCap irq\<rbrace> 124 decodeIRQHandlerInvocation label irq caps 125 \<lbrace>irq_handler_inv_valid'\<rbrace>,-" 126 apply (simp add: decodeIRQHandlerInvocation_def Let_def split_def 127 split del: if_split) 128 apply (rule hoare_pre) 129 apply (wp | wpc | simp)+ 130 apply (clarsimp simp: neq_Nil_conv isCap_simps) 131 apply (rule conjI) 132 apply (clarsimp simp: cte_wp_at_ctes_of) 133 apply (drule (1) valid_irq_handlers_ctes_ofD) 134 apply (simp add: invs'_def valid_state'_def) 135 apply (simp add: irq_issued'_def) 136 apply clarsimp 137 done 138 139lemma is_irq_active_corres: 140 "corres (=) \<top> \<top> (is_irq_active irq) (isIRQActive irq)" 141 apply (simp add: is_irq_active_def isIRQActive_def get_irq_state_def 142 getIRQState_def getInterruptState_def) 143 apply (clarsimp simp: state_relation_def interrupt_state_relation_def) 144 apply (drule_tac x=irq in spec)+ 145 apply (simp add: irq_state_relation_def 146 split: irqstate.split_asm irq_state.split_asm) 147 done 148 149crunch inv: isIRQActive "P" 150 151lemma isIRQActive_wp: 152 "\<lbrace>\<lambda>s. \<forall>rv. (irq_issued' irq s \<longrightarrow> rv) \<longrightarrow> Q rv s\<rbrace> isIRQActive irq \<lbrace>Q\<rbrace>" 153 apply (simp add: isIRQActive_def getIRQState_def 154 getInterruptState_def) 155 apply wp 156 apply (clarsimp simp: irq_issued'_def) 157 done 158 159lemma arch_check_irq_corres: 160 "corres (ser \<oplus> dc) \<top> \<top> (arch_check_irq irq) (checkIRQ irq)" 161 unfolding arch_check_irq_def checkIRQ_def rangeCheck_def 162 apply (rule corres_guard_imp) 163 apply (clarsimp simp: minIRQ_def unlessE_whenE not_le) 164 apply (rule corres_whenE) 165 apply (fastforce simp: ucast_nat_def)+ 166 done 167 168lemma whenE_rangeCheck_eq: 169 "(rangeCheck (x :: 'a :: {linorder, integral}) y z) = 170 (whenE (x < fromIntegral y \<or> fromIntegral z < x) 171 (throwError (RangeError (fromIntegral y) (fromIntegral z))))" 172 by (simp add: rangeCheck_def unlessE_whenE ucast_id linorder_not_le[symmetric]) 173 174(* 125 = maxIRQ *) 175lemma unat_ucast_ucast_shenanigans[simp]: 176 "unat (yf :: machine_word) \<le> (125::nat) \<Longrightarrow> ucast ((ucast yf) :: word8) = yf" 177 apply (subgoal_tac "unat yf \<le> unat 125") 178 apply (thin_tac "unat yf \<le> 125") 179 apply (subst (asm) word_le_nat_alt[symmetric]) 180 apply (simp add: ucast_ucast_mask mask_def) 181 by (word_bitwise, auto) 182 183lemmas irq_const_defs = 184 maxIRQ_def minIRQ_def 185 186crunches arch_check_irq, checkIRQ 187 for inv: "P" 188 (simp: crunch_simps) 189 190lemma arch_check_irq_maxIRQ_valid: 191 "\<lbrace>\<top>\<rbrace> arch_check_irq y \<lbrace>\<lambda>_. (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, -" 192 unfolding arch_check_irq_def 193 apply (wpsimp simp: validE_R_def wp: whenE_throwError_wp) 194 by (metis unat_ucast_10_32 word_le_nat_alt word_le_not_less) 195 196lemma arch_check_irq_maxIRQ_valid': 197 "\<lbrace>\<top>\<rbrace> arch_check_irq y \<lbrace>\<lambda>_ _. unat y \<le> unat maxIRQ\<rbrace>, \<lbrace>\<lambda>_. \<top>\<rbrace>" 198 by (wp arch_check_irq_maxIRQ_valid) 199 200lemma arch_decode_irq_control_corres: 201 "list_all2 cap_relation caps caps' \<Longrightarrow> 202 corres (ser \<oplus> arch_irq_control_inv_relation) 203 (invs and (\<lambda>s. \<forall>cp \<in> set caps. s \<turnstile> cp)) 204 (invs' and (\<lambda>s. \<forall>cp \<in> set caps'. s \<turnstile>' cp)) 205 (arch_decode_irq_control_invocation label args slot caps) 206 (ARM_H.decodeIRQControlInvocation label args (cte_map slot) caps')" 207 apply (clarsimp simp: arch_decode_irq_control_invocation_def ARM_H.decodeIRQControlInvocation_def Let_def) 208 apply (rule conjI, clarsimp) 209 prefer 2 210 apply clarsimp 211 apply (cases caps, simp) 212 apply (auto split: arch_invocation_label.splits list.splits invocation_label.splits 213 simp: length_Suc_conv list_all2_Cons1 whenE_rangeCheck_eq liftE_bindE split_def)[2] 214 apply (cases caps, simp split: list.split) 215 apply (case_tac "\<exists>n. length args = Suc (Suc (Suc (Suc n)))", 216 clarsimp simp: length_Suc_conv list_all2_Cons1 whenE_rangeCheck_eq 217 liftE_bindE split_def) 218 prefer 2 apply (auto split: list.split)[1] 219 \<comment>\<open>ARMIRQIssueIRQHandler\<close> 220 apply (rule conjI, clarsimp) 221 apply (rule corres_guard_imp) 222 apply (rule corres_splitEE[OF _ arch_check_irq_corres]) 223 apply (rule_tac F="unat y \<le> unat maxIRQ" in corres_gen_asm) 224 apply (clarsimp simp add: minIRQ_def maxIRQ_def ucast_nat_def) 225 apply (rule corres_split_eqr[OF _ is_irq_active_corres]) 226 apply (rule whenE_throwError_corres, clarsimp, clarsimp) 227 apply (rule corres_splitEE[OF _ lsfc_corres]) 228 apply (rule corres_splitEE[OF _ ensure_empty_corres]) 229 apply (rule corres_returnOkTT) 230 apply (clarsimp simp: arch_irq_control_inv_relation_def ) 231 apply ((wpsimp wp: isIRQActive_inv arch_check_irq_maxIRQ_valid' checkIRQ_inv 232 simp: invs_valid_objs invs_psp_aligned invs_valid_objs' 233 invs_pspace_aligned' invs_pspace_distinct' 234 | strengthen invs_valid_objs invs_psp_aligned 235 | wp_once hoare_drop_imps arch_check_irq_inv)+) 236 apply (auto split: arch_invocation_label.splits invocation_label.splits) 237 done 238 239lemma irqhandler_simp[simp]: 240 "invocation_type label \<noteq> IRQIssueIRQHandler \<Longrightarrow> (case invocation_type label of IRQIssueIRQHandler \<Rightarrow> b | _ \<Rightarrow> c) = c" 241 by (clarsimp split: invocation_label.splits) 242 243lemmas unat_le_mono = word_le_nat_alt [THEN iffD1] 244 245lemma decode_irq_control_corres: 246 "list_all2 cap_relation caps caps' \<Longrightarrow> 247 corres (ser \<oplus> irq_control_inv_relation) 248 (invs and (\<lambda>s. \<forall>cp \<in> set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp \<in> set caps'. s \<turnstile>' cp)) 249 (decode_irq_control_invocation label args slot caps) 250 (decodeIRQControlInvocation label args (cte_map slot) caps')" 251 apply (clarsimp simp: decode_irq_control_invocation_def decodeIRQControlInvocation_def 252 arch_check_irq_def ARM_H.checkIRQ_def 253 split del: if_split cong: if_cong 254 split: ) 255 apply clarsimp 256 apply (rule conjI, clarsimp) 257 apply (rule conjI, clarsimp) 258 apply (cases caps, simp split: list.split) 259 apply (case_tac "\<exists>n. length args = Suc (Suc (Suc n))") 260 apply (clarsimp simp: list_all2_Cons1 Let_def split_def liftE_bindE 261 length_Suc_conv checkIRQ_def ) 262 defer 263 apply (subgoal_tac "length args \<le> 2", clarsimp split: list.split) 264 apply arith 265 apply (simp add: minIRQ_def o_def) 266 apply (auto intro!: corres_guard_imp[OF arch_decode_irq_control_corres])[1] 267 apply (auto intro!: corres_guard_imp[OF arch_decode_irq_control_corres] 268 dest!: not_le_imp_less 269 simp: minIRQ_def o_def length_Suc_conv whenE_rangeCheck_eq ucast_nat_def 270 split: list.splits)[1] 271 apply (simp add: minIRQ_def o_def length_Suc_conv whenE_rangeCheck_eq ucast_nat_def[symmetric]) 272 apply (rule corres_guard_imp) 273 apply (rule whenE_throwError_corres, clarsimp, clarsimp) 274 apply (rule_tac F="unat y \<le> unat maxIRQ" in corres_gen_asm) 275 apply (clarsimp simp add: minIRQ_def maxIRQ_def ucast_nat_def) 276 apply (rule corres_split_eqr[OF _ is_irq_active_corres]) 277 apply (rule whenE_throwError_corres, clarsimp, clarsimp) 278 apply (rule corres_splitEE[OF _ lsfc_corres]) 279 apply (rule corres_splitEE[OF _ ensure_empty_corres]) 280 apply (rule corres_returnOkTT) 281 apply (clarsimp simp: arch_irq_control_inv_relation_def ) 282 apply (wpsimp wp: isIRQActive_inv arch_check_irq_maxIRQ_valid' checkIRQ_inv 283 simp: invs_valid_objs invs_psp_aligned invs_valid_objs' 284 invs_pspace_aligned' invs_pspace_distinct' 285 | strengthen invs_valid_objs invs_psp_aligned 286 | wp_once hoare_drop_imps arch_check_irq_inv)+ 287 apply (auto split: arch_invocation_label.splits invocation_label.splits 288 simp: not_less unat_le_helper) 289 done 290 291crunch inv[wp]: "InterruptDecls_H.decodeIRQControlInvocation" "P" 292 (simp: crunch_simps) 293 294 295(* Levity: added (20090201 10:50:27) *) 296declare ensureEmptySlot_stronger [wp] 297 298lemma lsfco_real_cte_at'[wp]: 299 "\<lbrace>valid_objs' and valid_cap' croot\<rbrace> 300 lookupSlotForCNodeOp is_src croot ptr depth 301 \<lbrace>\<lambda>rv s. real_cte_at' rv s\<rbrace>,-" 302 apply (simp add: lookupSlotForCNodeOp_def split_def unlessE_def 303 whenE_def 304 split del: if_split 305 cong: if_cong list.case_cong capability.case_cong) 306 apply (rule hoare_pre) 307 apply (wp resolveAddressBits_real_cte_at' 308 | simp 309 | wpc | wp_once hoare_drop_imps)+ 310 done 311 312lemma arch_decode_irq_control_valid'[wp]: 313 "\<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap \<in> set caps. s \<turnstile>' cap) 314 \<and> (\<forall>cap \<in> set caps. \<forall>r \<in> cte_refs' cap (irq_node' s). ex_cte_cap_to' r s) 315 \<and> cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) slot s\<rbrace> 316 ARM_H.decodeIRQControlInvocation label args slot caps 317 \<lbrace>arch_irq_control_inv_valid'\<rbrace>,-" 318 apply (clarsimp simp add: ARM_H.decodeIRQControlInvocation_def Let_def split_def 319 rangeCheck_def unlessE_whenE 320 split del: if_split 321 cong: if_cong list.case_cong prod.case_cong arch_invocation_label.case_cong) 322 apply (rule hoare_pre) 323 apply (simp add: rangeCheck_def unlessE_whenE checkIRQ_def 324 cong: list.case_cong prod.case_cong 325 | wp whenE_throwError_wp isIRQActive_wp ensureEmptySlot_stronger 326 | wpc 327 | wp_once hoare_drop_imps)+ 328 apply (clarsimp simp add: invs_valid_objs' irq_const_defs unat_word_ariths word_le_nat_alt 329 not_less unat_le_helper unat_of_nat) 330 done 331 332lemma decode_irq_control_valid'[wp]: 333 "\<lbrace>\<lambda>s. invs' s \<and> (\<forall>cap \<in> set caps. s \<turnstile>' cap) 334 \<and> (\<forall>cap \<in> set caps. \<forall>r \<in> cte_refs' cap (irq_node' s). ex_cte_cap_to' r s) 335 \<and> cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) slot s\<rbrace> 336 decodeIRQControlInvocation label args slot caps 337 \<lbrace>irq_control_inv_valid'\<rbrace>,-" 338 apply (simp add: decodeIRQControlInvocation_def Let_def split_def checkIRQ_def 339 rangeCheck_def unlessE_whenE 340 split del: if_split cong: if_cong list.case_cong 341 invocation_label.case_cong) 342 apply (wpsimp wp: ensureEmptySlot_stronger isIRQActive_wp whenE_throwError_wp 343 simp: o_def 344 | wp_once hoare_drop_imps)+ 345 apply (clarsimp simp: invs_valid_objs' irq_const_defs unat_word_ariths word_le_nat_alt 346 not_less unat_le_helper unat_of_nat) 347 done 348 349lemma irq_nodes_global_refs: 350 "irq_node' s + (ucast (irq:: 10 word)) * 0x10 \<in> global_refs' s" 351 by (simp add: global_refs'_def mult.commute mult.left_commute) 352 353lemma valid_globals_ex_cte_cap_irq: 354 "\<lbrakk> ex_cte_cap_wp_to' isCNodeCap ptr s; valid_global_refs' s; 355 valid_objs' s \<rbrakk> 356 \<Longrightarrow> ptr \<noteq> intStateIRQNode (ksInterruptState s) + 2 ^ cte_level_bits * ucast (irq :: 10 word)" 357 apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_wp_to'_def) 358 apply (drule(1) ctes_of_valid'[rotated]) 359 apply (drule(1) valid_global_refsD') 360 apply (drule subsetD[rotated], erule cte_refs_capRange) 361 apply (clarsimp simp: isCap_simps) 362 apply (subgoal_tac "irq_node' s + 2 ^ cte_level_bits * ucast irq \<in> global_refs' s") 363 apply blast 364 apply (simp add: global_refs'_def cte_level_bits_def 365 mult.commute mult.left_commute) 366 done 367 368lemma invoke_irq_handler_corres: 369 "irq_handler_inv_relation i i' \<Longrightarrow> 370 corres dc (einvs and irq_handler_inv_valid i) 371 (invs' and irq_handler_inv_valid' i') 372 (invoke_irq_handler i) 373 (invokeIRQHandler i')" 374 apply (cases i, simp_all add: invokeIRQHandler_def) 375 apply (rule corres_guard_imp, rule corres_machine_op) 376 apply (rule corres_Id, simp_all) 377 apply (rule no_fail_maskInterrupt) 378 apply (rename_tac word cap prod) 379 apply clarsimp 380 apply (rule corres_guard_imp) 381 apply (rule corres_split [OF _ get_irq_slot_corres]) 382 apply simp 383 apply (rule corres_split_nor [OF _ cap_delete_one_corres]) 384 apply (rule cins_corres, simp+) 385 apply (rule_tac Q="\<lambda>rv s. einvs s \<and> cte_wp_at (\<lambda>c. c = cap.NullCap) irq_slot s 386 \<and> (a, b) \<noteq> irq_slot 387 \<and> cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s" 388 in hoare_post_imp) 389 apply fastforce 390 apply (wp cap_delete_one_still_derived)+ 391 apply (strengthen invs_mdb_strengthen') 392 apply wp+ 393 apply (simp add: conj_comms eq_commute) 394 apply (wp get_irq_slot_different hoare_drop_imps)+ 395 apply (clarsimp simp: valid_state_def invs_def) 396 apply (erule cte_wp_at_weakenE, simp add: is_derived_use_interrupt) 397 apply fastforce 398 apply (rule corres_guard_imp) 399 apply (rule corres_split [OF _ get_irq_slot_corres]) 400 apply simp 401 apply (rule cap_delete_one_corres) 402 apply wp+ 403 apply simp+ 404 done 405 406lemma ntfn_badge_derived_enough_strg: 407 "cte_wp_at' (\<lambda>cte. isNotificationCap cap \<and> badge_derived' cap (cteCap cte)) ptr s 408 \<longrightarrow> cte_wp_at' (is_derived' ctes ptr cap \<circ> cteCap) ptr s" 409 by (clarsimp simp: cte_wp_at_ctes_of isCap_simps 410 badge_derived'_def is_derived'_def vsCapRef_def) 411 412lemma cteDeleteOne_ex_cte_cap_to'[wp]: 413 "\<lbrace>ex_cte_cap_wp_to' P p\<rbrace> cteDeleteOne ptr \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p\<rbrace>" 414 apply (simp add: ex_cte_cap_to'_def) 415 apply (rule hoare_pre) 416 apply (rule hoare_use_eq_irq_node' [OF cteDeleteOne_irq_node']) 417 apply (wp hoare_vcg_ex_lift cteDeleteOne_cte_wp_at_preserved) 418 apply (case_tac cap, simp_all add: finaliseCap_def isCap_simps) 419 done 420 421lemma cteDeleteOne_other_cap: 422 "\<lbrace>(\<lambda>s. cte_wp_at' (P o cteCap) p s) and K (p \<noteq> p')\<rbrace> 423 cteDeleteOne p' 424 \<lbrace>\<lambda>rv s. cte_wp_at' (P o cteCap) p s\<rbrace>" 425 apply (rule hoare_gen_asm) 426 apply (simp add: tree_cte_cteCap_eq) 427 apply (wp cteDeleteOne_cteCaps_of) 428 apply simp 429 done 430 431lemma isnt_irq_handler_strg: 432 "(\<not> isIRQHandlerCap cap) \<longrightarrow> (\<forall>irq. cap = IRQHandlerCap irq \<longrightarrow> P irq)" 433 by (clarsimp simp: isCap_simps) 434 435lemma ct_in_current_domain_ksMachineState: 436 "ct_idle_or_in_cur_domain' (ksMachineState_update p s) = ct_idle_or_in_cur_domain' s" 437 apply (simp add:ct_idle_or_in_cur_domain'_def) 438 apply (simp add:tcb_in_cur_domain'_def) 439 done 440 441lemma invoke_irq_handler_invs'[wp]: 442 "\<lbrace>invs' and irq_handler_inv_valid' i\<rbrace> 443 invokeIRQHandler i \<lbrace>\<lambda>rv. invs'\<rbrace>" 444 apply (cases i, simp_all add: invokeIRQHandler_def) 445 apply (wp dmo_maskInterrupt) 446 apply (clarsimp simp add: invs'_def valid_state'_def valid_irq_masks'_def 447 valid_machine_state'_def ct_not_inQ_def 448 ct_in_current_domain_ksMachineState) 449 apply (wp cteInsert_invs)+ 450 apply (strengthen ntfn_badge_derived_enough_strg isnt_irq_handler_strg) 451 apply (wp cteDeleteOne_other_cap cteDeleteOne_other_cap[unfolded o_def]) 452 apply (rename_tac word1 cap word2) 453 apply (simp add: getInterruptState_def getIRQSlot_def locateSlot_conv) 454 apply wp 455 apply (rename_tac word1 cap word2 s) 456 apply (clarsimp simp: ucast_nat_def) 457 apply (drule_tac irq=word1 in valid_globals_ex_cte_cap_irq) 458 apply clarsimp+ 459 apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_to'_def 460 isCap_simps untyped_derived_eq_def) 461 apply (fastforce simp: cte_level_bits_def badge_derived'_def)+ 462 done 463 464lemma IRQHandler_valid': 465 "(s' \<turnstile>' IRQHandlerCap irq) = (irq \<le> maxIRQ)" 466 by (simp add: valid_cap'_def capAligned_def word_bits_conv) 467 468lemma valid_mdb_interrupts'[simp]: 469 "valid_mdb' (ksInterruptState_update f s) = valid_mdb' s" 470 by (simp add: valid_mdb'_def) 471crunch valid_mdb'[wp]: setIRQState "valid_mdb'" 472crunch cte_wp_at[wp]: setIRQState "cte_wp_at' P p" 473 474lemma no_fail_setIRQTrigger: "no_fail \<top> (setIRQTrigger irq trig)" 475 by (simp add: setIRQTrigger_def) 476 477lemma setIRQTrigger_corres: 478 "corres dc \<top> \<top> (do_machine_op (setIRQTrigger irq t)) (doMachineOp (setIRQTrigger irq t))" 479 apply (rule corres_machine_op) 480 apply (rule corres_guard_imp) 481 apply (rule corres_rel_imp) 482 apply (wp 483 | rule corres_underlying_trivial 484 | rule no_fail_setIRQTrigger 485 | simp add: dc_def)+ 486 done 487 488lemma arch_invoke_irq_control_corres: 489 "arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (intr \<oplus> dc) 490 (einvs and arch_irq_control_inv_valid x2) 491 (invs' and arch_irq_control_inv_valid' ivk') 492 (arch_invoke_irq_control x2) 493 (Arch.performIRQControl ivk')" 494 apply (cases x2; simp add: ARM_H.performIRQControl_def invoke_irq_control.cases IRQ_def) 495 apply (rule corres_guard_imp) 496 apply (rule corres_split_nor) 497 apply (rule corres_split_nor) 498 apply (rule cins_corres_simple; simp) 499 apply (rule set_irq_state_corres) 500 apply (simp add: irq_state_relation_def) 501 apply (wp | simp add: irq_state_relation_def IRQHandler_valid IRQHandler_valid')+ 502 apply (rule setIRQTrigger_corres) 503 apply wp+ 504 apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state 505 is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def 506 safe_parent_for_def) 507 apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def IRQHandler_valid 508 IRQHandler_valid' is_simple_cap'_def isCap_simps IRQ_def) 509 apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of) 510 apply (case_tac ctea) 511 apply (clarsimp simp: isCap_simps sameRegionAs_def3) 512 apply (auto dest: valid_irq_handlers_ctes_ofD)[1] 513 done 514 515lemma invoke_irq_control_corres: 516 "irq_control_inv_relation i i' \<Longrightarrow> 517 corres (intr \<oplus> dc) (einvs and irq_control_inv_valid i) 518 (invs' and irq_control_inv_valid' i') 519 (invoke_irq_control i) 520 (performIRQControl i')" 521 apply (cases i, simp_all add: performIRQControl_def) 522 apply (rule corres_guard_imp) 523 apply (rule corres_split_nor [OF _ set_irq_state_corres]) 524 apply (rule cins_corres_simple) 525 apply (wp | simp add: irq_state_relation_def 526 IRQHandler_valid IRQHandler_valid')+ 527 apply (clarsimp simp: invs_def valid_state_def valid_pspace_def 528 cte_wp_at_caps_of_state is_simple_cap_def 529 is_cap_simps safe_parent_for_def) 530 apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def 531 IRQHandler_valid IRQHandler_valid' is_simple_cap'_def 532 isCap_simps) 533 apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of) 534 apply (case_tac ctea) 535 apply (clarsimp simp: isCap_simps sameRegionAs_def3) 536 apply (auto dest: valid_irq_handlers_ctes_ofD)[1] 537 by (clarsimp simp: arch_invoke_irq_control_corres) 538 539crunch valid_cap'[wp]: setIRQState "valid_cap' cap" 540 541lemma setIRQState_cte_cap_to'[wp]: 542 "\<lbrace>ex_cte_cap_to' p\<rbrace> setIRQState st irq \<lbrace>\<lambda>_. ex_cte_cap_to' p\<rbrace>" 543 apply (simp add: setIRQState_def doMachineOp_def 544 split_def setInterruptState_def getInterruptState_def) 545 apply wp 546 apply (clarsimp simp: ex_cte_cap_to'_def) 547 done 548 549lemma setIRQState_issued[wp]: 550 "\<lbrace>K (st = IRQSignal)\<rbrace> setIRQState st irq \<lbrace>\<lambda>rv. irq_issued' irq\<rbrace>" 551 apply (simp add: setIRQState_def irq_issued'_def setInterruptState_def 552 getInterruptState_def) 553 apply wp 554 apply clarsimp 555 done 556 557lemma dmo_setIRQTrigger_invs'[wp]: 558 "\<lbrace>invs'\<rbrace> doMachineOp (setIRQTrigger irq t) \<lbrace>\<lambda>r. invs'\<rbrace>" 559 apply (wp dmo_invs' no_irq_setIRQTrigger no_irq) 560 apply clarsimp 561 apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p" 562 in use_valid[where P=P and Q="\<lambda>_. P" for P]) 563 apply (simp add: setIRQTrigger_def machine_op_lift_def 564 machine_rest_lift_def split_def | wp)+ 565 done 566 567lemma arch_invoke_irq_control_invs'[wp]: 568 "\<lbrace>invs' and arch_irq_control_inv_valid' i\<rbrace> ARM_H.performIRQControl i \<lbrace>\<lambda>rv. invs'\<rbrace>" 569 apply (simp add: ARM_H.performIRQControl_def) 570 apply (rule hoare_pre) 571 apply (wp cteInsert_simple_invs 572 | simp add: cte_wp_at_ctes_of isCap_simps IRQ_def 573 | wpc)+ 574 apply (clarsimp simp: cte_wp_at_ctes_of IRQHandler_valid' is_simple_cap'_def isCap_simps 575 safe_parent_for'_def sameRegionAs_def3) 576 apply (rule conjI, clarsimp simp: cte_wp_at_ctes_of) 577 apply (case_tac ctea) 578 apply (auto dest: valid_irq_handlers_ctes_ofD 579 simp: invs'_def valid_state'_def IRQ_def) 580 done 581 582lemma invoke_irq_control_invs'[wp]: 583 "\<lbrace>invs' and irq_control_inv_valid' i\<rbrace> performIRQControl i \<lbrace>\<lambda>rv. invs'\<rbrace>" 584 apply (cases i, simp_all add: performIRQControl_def) 585 apply (rule hoare_pre) 586 apply (wp cteInsert_simple_invs | simp add: cte_wp_at_ctes_of)+ 587 apply (clarsimp simp: cte_wp_at_ctes_of IRQHandler_valid' 588 is_simple_cap'_def isCap_simps 589 safe_parent_for'_def sameRegionAs_def3) 590 apply (case_tac ctea) 591 apply (auto dest: valid_irq_handlers_ctes_ofD 592 simp: invs'_def valid_state'_def) 593 done 594 595lemma get_irq_state_corres: 596 "corres irq_state_relation \<top> \<top> 597 (get_irq_state irq) (getIRQState irq)" 598 apply (simp add: get_irq_state_def getIRQState_def getInterruptState_def) 599 apply (clarsimp simp: state_relation_def interrupt_state_relation_def) 600 done 601 602lemma getIRQState_prop: 603 "\<lbrace>\<lambda>s. P (intStateIRQTable (ksInterruptState s) irq)\<rbrace> 604 getIRQState irq 605 \<lbrace>\<lambda>rv s. P rv\<rbrace>" 606 apply (simp add: getIRQState_def getInterruptState_def) 607 apply wp 608 apply simp 609 done 610 611lemma num_domains[simp]: 612 "num_domains = numDomains" 613 apply(simp add: num_domains_def numDomains_def) 614 done 615 616lemma dec_domain_time_corres: 617 "corres dc \<top> \<top> dec_domain_time decDomainTime" 618 apply (simp add:dec_domain_time_def corres_underlying_def 619 decDomainTime_def simpler_modify_def) 620 apply (clarsimp simp:state_relation_def) 621 done 622 623lemma weak_sch_act_wf_updateDomainTime[simp]: 624 "weak_sch_act_wf m (s\<lparr>ksDomainTime := t\<rparr>) 625 = weak_sch_act_wf m s" 626 by (simp add:weak_sch_act_wf_def tcb_in_cur_domain'_def ) 627 628lemma tcbSchedAppend_valid_objs': 629 "\<lbrace>valid_objs'\<rbrace>tcbSchedAppend t \<lbrace>\<lambda>r. valid_objs'\<rbrace>" 630 apply (simp add:tcbSchedAppend_def) 631 apply (wp hoare_unless_wp 632 threadSet_valid_objs' threadGet_wp 633 | simp add:valid_tcb_tcbQueued)+ 634 apply (clarsimp simp add:obj_at'_def typ_at'_def) 635 done 636 637lemma valid_tcb_tcbTimeSlice_update[simp]: 638 "valid_tcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) s = valid_tcb' tcb s" 639 by (simp add:valid_tcb'_def tcb_cte_cases_def) 640 641lemma thread_state_case_if: 642 "(case state of Structures_A.thread_state.Running \<Rightarrow> f | _ \<Rightarrow> g) = 643 (if state = Structures_A.thread_state.Running then f else g)" 644 by (case_tac state,auto) 645 646lemma threadState_case_if: 647 "(case state of Structures_H.thread_state.Running \<Rightarrow> f | _ \<Rightarrow> g) = 648 (if state = Structures_H.thread_state.Running then f else g)" 649 by (case_tac state,auto) 650 651lemma tcbSchedAppend_invs_but_ct_not_inQ': 652 "\<lbrace>invs' and st_tcb_at' runnable' t \<rbrace> 653 tcbSchedAppend t \<lbrace>\<lambda>_. all_invs_but_ct_not_inQ'\<rbrace>" 654 apply (simp add: invs'_def valid_state'_def) 655 apply (rule hoare_pre) 656 apply (wp sch_act_wf_lift valid_irq_node_lift irqs_masked_lift 657 valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2 658 untyped_ranges_zero_lift 659 | simp add: cteCaps_of_def o_def 660 | fastforce elim!: st_tcb_ex_cap'' split: thread_state.split_asm)+ 661 done 662 663lemma timerTick_corres: 664 "corres dc (cur_tcb and valid_sched) 665 invs' 666 timer_tick timerTick" 667 apply (simp add: timerTick_def timer_tick_def) 668 apply (simp add:thread_state_case_if threadState_case_if) 669 apply (rule_tac Q="\<top> and (cur_tcb and valid_sched)" and Q'="\<top> and invs'" in corres_guard_imp) 670 apply (rule corres_guard_imp) 671 apply (rule corres_split [OF _ gct_corres]) 672 apply simp 673 apply (rule corres_split [OF _ gts_corres]) 674 apply (rename_tac state state') 675 apply (rule corres_split[where r' = dc ]) 676 apply simp 677 apply (rule corres_when,simp) 678 apply (rule corres_split[OF _ dec_domain_time_corres]) 679 apply (rule corres_split[OF _ domain_time_corres]) 680 apply (rule corres_when,simp) 681 apply (rule rescheduleRequired_corres) 682 apply (wp hoare_drop_imp)+ 683 apply (simp add:dec_domain_time_def) 684 apply wp+ 685 apply (simp add:decDomainTime_def) 686 apply wp 687 apply (rule corres_if[where Q = \<top> and Q' = \<top>]) 688 apply (case_tac state,simp_all)[1] 689 apply (simp add: Let_def) 690 apply (rule_tac r'="(=)" in corres_split [OF _ ethreadget_corres]) 691 apply (rename_tac ts ts') 692 apply (rule_tac R="1 < ts" in corres_cases) 693 apply (simp) 694 apply (unfold thread_set_time_slice_def) 695 apply (fold dc_def) 696 apply (rule ethread_set_corres, simp+) 697 apply (clarsimp simp: etcb_relation_def) 698 apply simp 699 apply (rule corres_split [OF _ ethread_set_corres]) 700 apply (rule corres_split [OF _ tcbSchedAppend_corres]) 701 apply (fold dc_def) 702 apply (rule rescheduleRequired_corres) 703 apply (wp)[1] 704 apply (rule hoare_strengthen_post) 705 apply (rule tcbSchedAppend_invs_but_ct_not_inQ', clarsimp simp: sch_act_wf_weak) 706 apply (simp add: sch_act_wf_weak etcb_relation_def 707 time_slice_def timeSlice_def pred_conj_def)+ 708 apply (wp threadSet_timeslice_invs threadSet_valid_queues 709 threadSet_valid_queues' threadSet_pred_tcb_at_state)+ 710 apply (simp add:etcb_relation_def) 711 apply (wp threadSet_timeslice_invs threadSet_valid_queues 712 threadSet_valid_queues' threadSet_pred_tcb_at_state) 713 apply simp 714 apply (wp|wpc|unfold Let_def|simp)+ 715 apply (wp static_imp_wp threadSet_timeslice_invs threadSet_valid_queues threadSet_valid_queues' 716 threadSet_pred_tcb_at_state threadSet_weak_sch_act_wf tcbSchedAppend_valid_objs' 717 rescheduleRequired_weak_sch_act_wf tcbSchedAppend_valid_queues| simp)+ 718 apply (strengthen sch_act_wf_weak) 719 apply (clarsimp simp:conj_comms) 720 apply (wp tcbSchedAppend_valid_queues tcbSchedAppend_sch_act_wf) 721 apply simp 722 apply (wp threadSet_valid_queues threadSet_pred_tcb_at_state threadSet_sch_act 723 threadSet_tcbDomain_triv threadSet_valid_queues' threadSet_valid_objs'| simp)+ 724 apply (wp threadGet_wp gts_wp gts_wp')+ 725 apply (clarsimp simp: cur_tcb_def tcb_at_is_etcb_at valid_sched_def valid_sched_action_def) 726 apply (subgoal_tac "is_etcb_at thread s \<and> tcb_at thread s \<and> valid_etcbs s \<and> weak_valid_sched_action s") 727 prefer 2 728 apply assumption 729 apply clarsimp 730 apply (wp gts_wp')+ 731 apply (clarsimp simp add:cur_tcb_def valid_sched_def 732 valid_sched_action_def valid_etcbs_def is_tcb_def 733 is_etcb_at_def st_tcb_at_def obj_at_def 734 dest!:get_tcb_SomeD) 735 apply (simp split:Structures_A.kernel_object.splits) 736 apply (drule_tac x = "cur_thread s" in spec) 737 apply clarsimp 738 apply (clarsimp simp: invs'_def valid_state'_def 739 sch_act_wf_weak 740 cur_tcb'_def inQ_def 741 ct_in_state'_def obj_at'_def) 742 apply (clarsimp simp:st_tcb_at'_def 743 valid_idle'_def ct_idle_or_in_cur_domain'_def 744 obj_at'_def projectKO_eq) 745 apply simp 746 apply simp 747 done 748 749lemmas corres_eq_trivial = corres_Id[where f = h and g = h for h, simplified] 750thm corres_Id 751 752lemma handle_interrupt_corres: 753 "corres dc 754 (einvs) (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive)) 755 (handle_interrupt irq) (handleInterrupt irq)" 756 (is "corres dc (einvs) ?P' ?f ?g") 757 apply (simp add: handle_interrupt_def handleInterrupt_def ) 758 apply (rule conjI[rotated]; rule impI) 759 760 apply (rule corres_guard_imp) 761 apply (rule corres_split [OF _ get_irq_state_corres, 762 where R="\<lambda>rv. einvs" 763 and R'="\<lambda>rv. invs' and (\<lambda>s. rv \<noteq> IRQInactive)"]) 764 defer 765 apply (wp getIRQState_prop getIRQState_inv do_machine_op_bind doMachineOp_bind | simp add: do_machine_op_bind doMachineOp_bind )+ 766 apply (rule corres_guard_imp) 767apply (rule corres_split) 768 apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: dc_def no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+ 769 apply ((wp | simp)+)[4] 770 apply (rule corres_gen_asm2) 771 772 apply (case_tac st, simp_all add: irq_state_relation_def split: irqstate.split_asm) 773 apply (simp add: getSlotCap_def bind_assoc) 774 apply (rule corres_guard_imp) 775 apply (rule corres_split [OF _ get_irq_slot_corres]) 776 apply simp 777 apply (rule corres_split [OF _ get_cap_corres, 778 where R="\<lambda>rv. einvs and valid_cap rv" 779 and R'="\<lambda>rv. invs' and valid_cap' (cteCap rv)"]) 780 apply (rule corres_split'[where r'=dc]) 781 apply (case_tac xb, simp_all add: doMachineOp_return)[1] 782 apply (clarsimp simp add: when_def doMachineOp_return) 783 apply (rule corres_guard_imp, rule send_signal_corres) 784 apply (clarsimp simp: valid_cap_def valid_cap'_def do_machine_op_bind doMachineOp_bind)+ 785 apply ( rule corres_split) 786 apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+ 787 apply ((wp |simp)+) 788 apply clarsimp 789 apply fastforce 790 apply (rule corres_guard_imp) 791 apply (rule corres_split) 792 apply simp 793 apply (rule corres_split [OF corres_machine_op timerTick_corres]) 794 apply (rule corres_eq_trivial, simp+) 795 apply (rule corres_machine_op) 796 apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+) 797 apply wp+ 798 apply clarsimp 799 apply clarsimp 800 done 801 802lemma invs_ChooseNewThread: 803 "invs' s \<Longrightarrow> invs' (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)" 804 by (rule invs'_update_cnt) 805 806lemma ksDomainTime_invs[simp]: 807 "invs' (a\<lparr>ksDomainTime := t\<rparr>) = invs' a" 808 by (simp add:invs'_def valid_state'_def 809 cur_tcb'_def ct_not_inQ_def ct_idle_or_in_cur_domain'_def 810 tcb_in_cur_domain'_def valid_machine_state'_def) 811 812lemma valid_machine_state'_ksDomainTime[simp]: 813 "valid_machine_state' (a\<lparr>ksDomainTime := t\<rparr>) = valid_machine_state' a" 814 by (simp add:valid_machine_state'_def) 815 816lemma cur_tcb'_ksDomainTime[simp]: 817 "cur_tcb' (a\<lparr>ksDomainTime := 0\<rparr>) = cur_tcb' a" 818 by (simp add:cur_tcb'_def) 819 820lemma ct_idle_or_in_cur_domain'_ksDomainTime[simp]: 821 "ct_idle_or_in_cur_domain' (a\<lparr>ksDomainTime := t \<rparr>) = ct_idle_or_in_cur_domain' a" 822 by (simp add:ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) 823 824lemma threadSet_ksDomainTime[wp]: 825 "\<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> threadSet f ptr \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace>" 826 apply (simp add: threadSet_def setObject_def split_def) 827 apply (wp crunch_wps | simp add:updateObject_default_def)+ 828 done 829 830crunch ksDomainTime[wp]: rescheduleRequired "\<lambda>s. P (ksDomainTime s)" 831(simp:tcbSchedEnqueue_def wp:hoare_unless_wp) 832 833crunch ksDomainTime[wp]: tcbSchedAppend "\<lambda>s. P (ksDomainTime s)" 834(simp:tcbSchedEnqueue_def wp:hoare_unless_wp) 835 836lemma updateTimeSlice_valid_pspace[wp]: 837 "\<lbrace>valid_pspace'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 838 \<lbrace>\<lambda>r. valid_pspace'\<rbrace>" 839 apply (wp threadSet_valid_pspace'T) 840 apply (auto simp:tcb_cte_cases_def) 841 done 842 843lemma updateTimeSlice_sch_act_wf[wp]: 844 "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<rbrace> 845 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 846 \<lbrace>\<lambda>r s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" 847 by (wp threadSet_sch_act,simp) 848 849 850lemma updateTimeSlice_valid_queues[wp]: 851 "\<lbrace>\<lambda>s. Invariants_H.valid_queues s \<rbrace> 852 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 853 \<lbrace>\<lambda>r s. Invariants_H.valid_queues s\<rbrace>" 854 apply (wp threadSet_valid_queues,simp) 855 apply (clarsimp simp:obj_at'_def inQ_def) 856 done 857 858 859lemma updateTimeSlice_sym_refs[wp]: 860 "\<lbrace>\<lambda>s. sym_refs (state_refs_of' s)\<rbrace> 861 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 862 \<lbrace>\<lambda>r s. sym_refs (state_refs_of' s)\<rbrace>" 863 apply (simp add: threadSet_def setObject_def split_def) 864 apply (wp crunch_wps getObject_tcb_wp 865 | simp add: updateObject_default_def loadObject_default_def 866 | wpc)+ 867 apply (clarsimp simp:state_refs_of'_def 868 obj_at'_def lookupAround2_known1) 869 apply (subst lookupAround2_known1) 870 apply simp 871 apply (erule_tac f1 = sym_refs in arg_cong[THEN iffD1,rotated]) 872 apply (rule ext) 873 apply (subst option.sel) 874 apply (subst fst_conv)+ 875 apply (clarsimp simp:projectKO_eq projectKO_opt_tcb split:Structures_H.kernel_object.splits) 876 apply (simp add:objBits_simps) 877 apply (frule_tac s' = s and 878 v' = "(KOTCB (tcbTimeSlice_update (\<lambda>_. ts') obj))" in ps_clear_updE) 879 apply simp 880 apply (clarsimp simp:fun_upd_def) 881 apply (rule set_eqI) 882 apply (rule iffI) 883 apply (clarsimp split:option.splits if_split_asm) 884 apply (intro conjI impI) 885 apply simp 886 apply clarsimp 887 apply (drule_tac s' = s and y = thread and x = x and 888 v' = "(KOTCB (tcbTimeSlice_update (\<lambda>_. ts') obj))" 889 in ps_clear_updE[rotated]) 890 apply simp 891 apply (clarsimp simp:fun_upd_def) 892 apply (clarsimp split:option.splits if_split_asm) 893 apply (intro conjI impI) 894 apply simp 895 apply clarsimp 896 apply (drule_tac y = thread and x = x and s' = s and 897 v' = "KOTCB obj" 898 in ps_clear_updE) 899 apply simp 900 apply (simp add:fun_upd_def[symmetric]) 901 apply (subgoal_tac "s\<lparr>ksPSpace := ksPSpace s(thread \<mapsto> KOTCB obj)\<rparr> = s") 902 apply simp 903 apply (case_tac s) 904 apply simp 905 apply (rule ext,simp) 906 done 907 908lemma updateTimeSlice_if_live_then_nonz_cap'[wp]: 909 "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s\<rbrace> 910 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 911 \<lbrace>\<lambda>r s. if_live_then_nonz_cap' s\<rbrace>" 912 apply (wp threadSet_iflive'T) 913 apply (simp add:tcb_cte_cases_def) 914 apply (clarsimp simp:if_live_then_nonz_cap'_def 915 ko_wp_at'_def) 916 apply (intro conjI) 917 apply (clarsimp simp:obj_at'_real_def)+ 918 done 919 920lemma updateTimeSlice_if_unsafe_then_cap'[wp]: 921 "\<lbrace>\<lambda>s. if_unsafe_then_cap' s\<rbrace> 922 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 923 \<lbrace>\<lambda>r s. if_unsafe_then_cap' s\<rbrace>" 924 apply (wp threadSet_ifunsafe'T) 925 apply (simp add:tcb_cte_cases_def)+ 926 done 927 928lemma updateTimeSlice_valid_idle'[wp]: 929 "\<lbrace>\<lambda>s. valid_idle' s\<rbrace> 930 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 931 \<lbrace>\<lambda>r s. valid_idle' s\<rbrace>" 932 apply (wp threadSet_idle'T) 933 apply (simp add:tcb_cte_cases_def) 934 apply (clarsimp simp:valid_idle'_def) 935 done 936 937lemma updateTimeSlice_valid_global_refs'[wp]: 938 "\<lbrace>\<lambda>s. valid_global_refs' s\<rbrace> 939 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 940 \<lbrace>\<lambda>r s. valid_global_refs' s\<rbrace>" 941 apply (wp threadSet_idle'T) 942 apply (simp add:tcb_cte_cases_def)+ 943 done 944 945lemma updateTimeSlice_valid_irq_node'[wp]: 946 "\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s\<rbrace> 947 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 948 \<lbrace>\<lambda>r s. valid_irq_node' (irq_node' s) s\<rbrace>" 949 apply (rule hoare_pre) 950 apply wps 951 apply (simp add: valid_irq_node'_def 952 | wp hoare_vcg_all_lift)+ 953 done 954 955lemma updateTimeSlice_irq_handlers'[wp]: 956 "\<lbrace>\<lambda>s. valid_irq_handlers' s\<rbrace> 957 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 958 \<lbrace>\<lambda>r s. valid_irq_handlers' s\<rbrace>" 959 apply (rule hoare_pre) 960 apply (wp threadSet_irq_handlers' | 961 simp add: tcb_cte_cases_def)+ 962 done 963 964 965lemma updateTimeSlice_valid_queues'[wp]: 966 "\<lbrace>\<lambda>s. valid_queues' s \<rbrace> 967 threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread 968 \<lbrace>\<lambda>r s. valid_queues' s\<rbrace>" 969 apply (wp threadSet_valid_queues') 970 apply (auto simp:inQ_def) 971 done 972 973lemma rescheduleRequired_valid_irq_node'[wp]: 974 "\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s\<rbrace> rescheduleRequired 975 \<lbrace>\<lambda>rv s. valid_irq_node' (irq_node' s) s \<rbrace>" 976 apply (simp add:rescheduleRequired_def valid_irq_node'_def) 977 apply (wp hoare_vcg_all_lift | wpc |simp)+ 978 apply (simp add:tcbSchedEnqueue_def) 979 apply (wp hoare_unless_wp) 980 apply (wp threadSet_typ_at_lifts | wps)+ 981 apply simp 982 done 983 984(* catch up tcbSchedAppend to tcbSchedEnqueue, which has these from crunches on possibleSwitchTo *) 985crunch ifunsafe[wp]: tcbSchedAppend if_unsafe_then_cap' 986crunch irq_handlers'[wp]: tcbSchedAppend valid_irq_handlers' 987 (simp: unless_def tcb_cte_cases_def wp: crunch_wps) 988crunch irq_states'[wp]: tcbSchedAppend valid_irq_states' 989crunch pde_mappigns'[wp]: tcbSchedAppend valid_pde_mappings' 990crunch irqs_masked'[wp]: tcbSchedAppend irqs_masked' 991 (simp: unless_def wp: crunch_wps) 992crunch ct[wp]: tcbSchedAppend cur_tcb' 993 (wp: cur_tcb_lift crunch_wps) 994 995crunch cur_tcb'[wp]: tcbSchedAppend cur_tcb' 996 (simp: unless_def wp: crunch_wps) 997 998lemma timerTick_invs'[wp]: 999 "\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>" 1000 apply (simp add: numDomains_def timerTick_def) 1001 apply (wp threadSet_invs_trivial threadSet_pred_tcb_no_state 1002 rescheduleRequired_all_invs_but_ct_not_inQ 1003 tcbSchedAppend_invs_but_ct_not_inQ' 1004 | simp add: tcb_cte_cases_def numDomains_def invs_ChooseNewThread 1005 | wpc)+ 1006 apply (simp add:decDomainTime_def) 1007 apply wp 1008 apply simp 1009 apply (rule_tac Q="\<lambda>rv. invs'" in hoare_post_imp) 1010 apply (clarsimp simp add:invs'_def valid_state'_def) 1011 apply wpc 1012 apply (wp add: threadGet_wp threadSet_cur threadSet_timeslice_invs 1013 rescheduleRequired_all_invs_but_ct_not_inQ 1014 hoare_vcg_imp_lift threadSet_ct_idle_or_in_cur_domain' 1015 del: tcbSchedAppend_sch_act_wf)+ 1016 apply (rule hoare_strengthen_post[OF tcbSchedAppend_invs_but_ct_not_inQ']) 1017 apply (wpsimp simp: valid_pspace'_def sch_act_wf_weak)+ 1018 apply (wpsimp wp: threadSet_pred_tcb_no_state threadSet_tcbDomain_triv 1019 threadSet_valid_objs' threadSet_timeslice_invs)+ 1020 apply (wp threadGet_wp) 1021 apply (wp gts_wp')+ 1022 apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def numDomains_def) 1023 done 1024 1025lemma resetTimer_invs'[wp]: 1026 "\<lbrace>invs'\<rbrace> doMachineOp resetTimer \<lbrace>\<lambda>_. invs'\<rbrace>" 1027 apply (wp dmo_invs' no_irq no_irq_resetTimer) 1028 apply clarsimp 1029 apply (drule_tac Q="%_ b. underlying_memory b p = underlying_memory m p" 1030 in use_valid) 1031 apply (simp add: resetTimer_def 1032 machine_op_lift_def machine_rest_lift_def split_def) 1033 apply wp 1034 apply clarsimp+ 1035 done 1036 1037lemma dmo_ackInterrupt[wp]: 1038"\<lbrace>invs'\<rbrace> doMachineOp (ackInterrupt irq) \<lbrace>\<lambda>y. invs'\<rbrace>" 1039 apply (wp dmo_invs' no_irq no_irq_ackInterrupt) 1040 apply safe 1041 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 1042 in use_valid) 1043 apply ((clarsimp simp: ackInterrupt_def machine_op_lift_def 1044 machine_rest_lift_def split_def | wp)+)[3] 1045 done 1046 1047lemma hint_invs[wp]: 1048 "\<lbrace>invs'\<rbrace> handleInterrupt irq \<lbrace>\<lambda>rv. invs'\<rbrace>" 1049 apply (simp add: handleInterrupt_def getSlotCap_def 1050 cong: irqstate.case_cong) 1051 apply (rule conjI; rule impI) 1052 1053 apply (wp dmo_maskInterrupt_True getCTE_wp' 1054 | wpc | simp add: doMachineOp_bind )+ 1055 apply (rule_tac Q="\<lambda>rv. invs'" in hoare_post_imp) 1056 apply (clarsimp simp: cte_wp_at_ctes_of ex_nonz_cap_to'_def) 1057 apply fastforce 1058 apply (wp threadSet_invs_trivial | simp add: inQ_def handleReservedIRQ_def)+ 1059 apply (wp hoare_post_comb_imp_conj hoare_drop_imp getIRQState_inv) 1060 apply (assumption)+ 1061 done 1062 1063 1064crunch st_tcb_at'[wp]: timerTick "st_tcb_at' P t" 1065 (wp: threadSet_pred_tcb_no_state) 1066 1067lemma handleInterrupt_runnable: 1068 "\<lbrace>st_tcb_at' runnable' t\<rbrace> handleInterrupt irq \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>" 1069 apply (simp add: handleInterrupt_def) 1070 apply (rule conjI; rule impI) 1071 apply (wp sai_st_tcb' hoare_vcg_all_lift hoare_drop_imps 1072 threadSet_pred_tcb_no_state getIRQState_inv haskell_fail_wp 1073 |wpc|simp add: handleReservedIRQ_def)+ 1074 done 1075 1076end 1077 1078end 1079