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 11theory Finalise_C 12imports IpcCancel_C 13begin 14 15context kernel_m 16begin 17 18declare if_split [split del] 19 20lemma empty_fail_getEndpoint: 21 "empty_fail (getEndpoint ep)" 22 unfolding getEndpoint_def 23 by (auto intro: empty_fail_getObject) 24 25definition 26 "option_map2 f m = option_map f \<circ> m" 27 28lemma tcbSchedEnqueue_cslift_spec: 29 "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. \<exists>d v. option_map2 tcbPriority_C (cslift s) \<acute>tcb = Some v 30 \<and> v \<le> ucast maxPrio 31 \<and> option_map2 tcbDomain_C (cslift s) \<acute>tcb = Some d 32 \<and> d \<le> ucast maxDom 33 \<and> (end_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))) \<noteq> NULL 34 \<longrightarrow> option_map2 tcbPriority_C (cslift s) 35 (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v)))) 36 \<noteq> None 37 \<and> option_map2 tcbDomain_C (cslift s) 38 (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v)))) 39 \<noteq> None)\<rbrace> 40 Call tcbSchedEnqueue_'proc 41 {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) 42 \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) 43 \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) 44 \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}" 45 apply (hoare_rule HoarePartial.ProcNoRec1) 46 apply (rule allI, rule conseqPre, vcg) 47 apply (clarsimp simp: option_map2_def fun_eq_iff h_t_valid_clift 48 h_t_valid_field[OF h_t_valid_clift]) 49 apply (rule conjI) 50 apply (clarsimp simp: typ_heap_simps cong: if_cong) 51 apply (simp split: if_split) 52 apply (clarsimp simp: typ_heap_simps if_Some_helper cong: if_cong) 53 by (simp split: if_split) 54 55lemma setThreadState_cslift_spec: 56 "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. ksSchedulerAction_' (globals s) = tcb_Ptr x 57 \<and> x \<noteq> 0 \<and> x \<noteq> 1 58 \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s) (tcb_Ptr x) = Some v 59 \<and> v \<le> ucast maxPrio 60 \<and> option_map2 tcbDomain_C (cslift s) (tcb_Ptr x) = Some d 61 \<and> d \<le> ucast maxDom 62 \<and> (end_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))) \<noteq> NULL 63 \<longrightarrow> option_map2 tcbPriority_C (cslift s) 64 (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v)))) 65 \<noteq> None 66 \<and> option_map2 tcbDomain_C (cslift s) 67 (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v)))) 68 \<noteq> None)))\<rbrace> 69 Call setThreadState_'proc 70 {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) 71 \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) 72 \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) 73 \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) 74 \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}" 75 apply (rule allI, rule conseqPre) 76 apply vcg_step 77 apply vcg_step 78 apply vcg_step 79 apply vcg_step 80 apply vcg_step 81 apply vcg_step 82 apply vcg_step 83 apply (vcg exspec=tcbSchedEnqueue_cslift_spec) 84 apply (vcg_step+)[2] 85 apply vcg_step 86 apply (vcg exspec=isRunnable_modifies) 87 apply vcg 88 apply vcg_step 89 apply vcg_step 90 apply (vcg_step+)[1] 91 apply vcg 92 apply vcg_step+ 93 apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff 94 fun_eq_iff option_map2_def) 95 by (simp split: if_split) 96 97lemma ep_queue_relation_shift: 98 "(option_map2 tcbEPNext_C (cslift s') 99 = option_map2 tcbEPNext_C (cslift s) 100 \<and> option_map2 tcbEPPrev_C (cslift s') 101 = option_map2 tcbEPPrev_C (cslift s)) 102 \<longrightarrow> ep_queue_relation (cslift s') ts qPrev qHead 103 = ep_queue_relation (cslift s) ts qPrev qHead" 104 apply clarsimp 105 apply (induct ts arbitrary: qPrev qHead) 106 apply simp 107 apply simp 108 apply (simp add: option_map2_def fun_eq_iff 109 map_option_case) 110 apply (drule_tac x=qHead in spec)+ 111 apply (clarsimp split: option.split_asm) 112 done 113 114lemma rf_sr_cscheduler_relation: 115 "(s, s') \<in> rf_sr \<Longrightarrow> cscheduler_action_relation 116 (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))" 117 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 118 119lemma obj_at_ko_at2': 120 "\<lbrakk> obj_at' P p s; ko_at' ko p s \<rbrakk> \<Longrightarrow> P ko" 121 apply (drule obj_at_ko_at') 122 apply clarsimp 123 apply (drule ko_at_obj_congD', simp+) 124 done 125 126lemma ctcb_relation_tcbDomain: 127 "ctcb_relation tcb tcb' \<Longrightarrow> ucast (tcbDomain tcb) = tcbDomain_C tcb'" 128 by (simp add: ctcb_relation_def) 129 130lemma ctcb_relation_tcbPriority: 131 "ctcb_relation tcb tcb' \<Longrightarrow> ucast (tcbPriority tcb) = tcbPriority_C tcb'" 132 by (simp add: ctcb_relation_def) 133 134lemma ctcb_relation_tcbDomain_maxDom: 135 "\<lbrakk> ctcb_relation tcb tcb'; tcbDomain tcb \<le> maxDomain \<rbrakk> \<Longrightarrow> tcbDomain_C tcb' \<le> ucast maxDom" 136 apply (subst ctcb_relation_tcbDomain[symmetric], simp) 137 apply (subst ucast_le_migrate) 138 apply ((simp add:maxDom_def word_size)+)[2] 139 apply (simp add: ucast_up_ucast is_up_def source_size_def word_size target_size_def) 140 apply (simp add: maxDom_to_H) 141 done 142 143lemma ctcb_relation_tcbPriority_maxPrio: 144 "\<lbrakk> ctcb_relation tcb tcb'; tcbPriority tcb \<le> maxPriority \<rbrakk> 145 \<Longrightarrow> tcbPriority_C tcb' \<le> ucast maxPrio" 146 apply (subst ctcb_relation_tcbPriority[symmetric], simp) 147 apply (subst ucast_le_migrate) 148 apply ((simp add: seL4_MaxPrio_def word_size)+)[2] 149 apply (simp add: ucast_up_ucast is_up_def source_size_def word_size target_size_def) 150 apply (simp add: maxPrio_to_H) 151 done 152 153lemma tcbSchedEnqueue_cslift_precond_discharge: 154 "\<lbrakk> (s, s') \<in> rf_sr; obj_at' (P :: tcb \<Rightarrow> bool) x s; 155 valid_queues s; valid_objs' s \<rbrakk> \<Longrightarrow> 156 (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some v 157 \<and> v \<le> ucast maxPrio 158 \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some d 159 \<and> d \<le> ucast maxDom 160 \<and> (end_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v))) \<noteq> NULL 161 \<longrightarrow> option_map2 tcbPriority_C (cslift s') 162 (head_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v)))) 163 \<noteq> None 164 \<and> option_map2 tcbDomain_C (cslift s') 165 (head_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v)))) 166 \<noteq> None))" 167 apply (drule(1) obj_at_cslift_tcb) 168 apply (clarsimp simp: typ_heap_simps' option_map2_def) 169 apply (frule_tac t=x in valid_objs'_maxPriority, fastforce simp: obj_at'_def) 170 apply (frule_tac t=x in valid_objs'_maxDomain, fastforce simp: obj_at'_def) 171 apply (drule_tac P="\<lambda>tcb. tcbPriority tcb \<le> maxPriority" in obj_at_ko_at2', simp) 172 apply (drule_tac P="\<lambda>tcb. tcbDomain tcb \<le> maxDomain" in obj_at_ko_at2', simp) 173 174 apply (simp add: ctcb_relation_tcbDomain_maxDom ctcb_relation_tcbPriority_maxPrio) 175 apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" 176 in rf_sr_sched_queue_relation) 177 apply (simp add: maxDom_to_H maxPrio_to_H)+ 178 apply (simp add: cready_queues_index_to_C_def2 numPriorities_def) 179 apply (clarsimp simp: ctcb_relation_def) 180 apply (frule arg_cong[where f=unat], subst(asm) unat_ucast_8_64) 181 apply (frule tcb_queue'_head_end_NULL) 182 apply (erule conjunct1[OF valid_queues_valid_q]) 183 apply (frule(1) tcb_queue_relation_qhead_valid') 184 apply (simp add: valid_queues_valid_q) 185 apply (clarsimp simp: h_t_valid_clift_Some_iff) 186 done 187 188lemma cancel_all_ccorres_helper: 189 "ccorres dc xfdc 190 (\<lambda>s. valid_objs' s \<and> valid_queues s 191 \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) 192 \<and> sch_act_wf (ksSchedulerAction s) s) 193 {s'. \<exists>p. ep_queue_relation (cslift s') ts 194 p (thread_' s')} hs 195 (mapM_x (\<lambda>t. do 196 y \<leftarrow> setThreadState Restart t; 197 tcbSchedEnqueue t 198 od) ts) 199 (WHILE \<acute>thread \<noteq> tcb_Ptr 0 DO 200 (CALL setThreadState(\<acute>thread, scast ThreadState_Restart));; 201 (CALL tcbSchedEnqueue(\<acute>thread));; 202 Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace> 203 (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr)) 204 OD)" 205 unfolding whileAnno_def 206proof (induct ts) 207 case Nil 208 show ?case 209 apply (simp del: Collect_const) 210 apply (rule iffD1 [OF ccorres_expand_while_iff]) 211 apply (rule ccorres_tmp_lift2[where G'=UNIV and G''="\<lambda>x. UNIV", simplified]) 212 apply ceqv 213 apply (simp add: ccorres_cond_iffs mapM_x_def sequence_x_def 214 dc_def[symmetric]) 215 apply (rule ccorres_guard_imp2, rule ccorres_return_Skip) 216 apply simp 217 done 218next 219 case (Cons thread threads) 220 show ?case 221 apply (rule iffD1 [OF ccorres_expand_while_iff]) 222 apply (simp del: Collect_const 223 add: dc_def[symmetric] mapM_x_Cons) 224 apply (rule ccorres_guard_imp2) 225 apply (rule_tac xf'=thread_' in ccorres_abstract) 226 apply ceqv 227 apply (rule_tac P="rv' = tcb_ptr_to_ctcb_ptr thread" 228 in ccorres_gen_asm2) 229 apply (rule_tac P="tcb_ptr_to_ctcb_ptr thread \<noteq> Ptr 0" 230 in ccorres_gen_asm) 231 apply (clarsimp simp add: Collect_True ccorres_cond_iffs 232 simp del: Collect_const) 233 apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow[where F=UNIV]) 234 apply (intro ccorres_rhs_assoc) 235 apply (ctac(no_vcg) add: setThreadState_ccorres) 236 apply (rule ccorres_add_return2) 237 apply (ctac(no_vcg) add: tcbSchedEnqueue_ccorres) 238 apply (rule_tac P="tcb_at' thread" 239 in ccorres_from_vcg[where P'=UNIV]) 240 apply (rule allI, rule conseqPre, vcg) 241 apply (clarsimp simp: return_def) 242 apply (drule obj_at_ko_at', clarsimp) 243 apply (erule cmap_relationE1 [OF cmap_relation_tcb]) 244 apply (erule ko_at_projectKO_opt) 245 apply (fastforce intro: typ_heap_simps) 246 apply (wp sts_running_valid_queues | simp)+ 247 apply (rule ceqv_refl) 248 apply (rule "Cons.hyps") 249 apply (wp sts_valid_objs' sts_sch_act sch_act_wf_lift hoare_vcg_const_Ball_lift 250 sts_running_valid_queues sts_st_tcb' setThreadState_oa_queued | simp)+ 251 252 apply (vcg exspec=setThreadState_cslift_spec exspec=tcbSchedEnqueue_cslift_spec) 253 apply (clarsimp simp: tcb_at_not_NULL 254 Collect_const_mem valid_tcb_state'_def 255 ThreadState_Restart_def mask_def 256 valid_objs'_maxDomain valid_objs'_maxPriority) 257 apply (drule(1) obj_at_cslift_tcb) 258 apply (clarsimp simp: typ_heap_simps) 259 apply (rule conjI) 260 apply clarsimp 261 apply (frule rf_sr_cscheduler_relation) 262 apply (clarsimp simp: cscheduler_action_relation_def 263 st_tcb_at'_def 264 split: scheduler_action.split_asm) 265 apply (rename_tac word) 266 apply (frule_tac x=word in tcbSchedEnqueue_cslift_precond_discharge) 267 apply simp 268 apply clarsimp 269 apply clarsimp 270 apply clarsimp 271 apply clarsimp 272 apply (rule conjI) 273 apply (frule(3) tcbSchedEnqueue_cslift_precond_discharge) 274 apply clarsimp 275 apply clarsimp 276 apply (subst ep_queue_relation_shift, fastforce) 277 apply (drule_tac x="tcb_ptr_to_ctcb_ptr thread" 278 in fun_cong)+ 279 apply (clarsimp simp add: option_map2_def typ_heap_simps) 280 apply fastforce 281 done 282qed 283 284lemma cancelAllIPC_ccorres: 285 "ccorres dc xfdc 286 (invs') (UNIV \<inter> {s. epptr_' s = Ptr epptr}) [] 287 (cancelAllIPC epptr) (Call cancelAllIPC_'proc)" 288 apply (cinit lift: epptr_') 289 apply (rule ccorres_symb_exec_l [OF _ getEndpoint_inv _ empty_fail_getEndpoint]) 290 apply (rule_tac xf'=ret__unsigned_longlong_' 291 and val="case rv of IdleEP \<Rightarrow> scast EPState_Idle 292 | RecvEP _ \<Rightarrow> scast EPState_Recv | SendEP _ \<Rightarrow> scast EPState_Send" 293 and R="ko_at' rv epptr" 294 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 295 apply vcg 296 apply clarsimp 297 apply (erule cmap_relationE1 [OF cmap_relation_ep]) 298 apply (erule ko_at_projectKO_opt) 299 apply (clarsimp simp add: typ_heap_simps) 300 apply (simp add: cendpoint_relation_def Let_def 301 split: endpoint.split_asm) 302 apply ceqv 303 apply (rule_tac A="invs' and ko_at' rv epptr" 304 in ccorres_guard_imp2[where A'=UNIV]) 305 apply wpc 306 apply (rename_tac list) 307 apply (simp add: endpoint_state_defs 308 Collect_False Collect_True 309 ccorres_cond_iffs 310 del: Collect_const) 311 apply (rule ccorres_rhs_assoc)+ 312 apply csymbr 313 apply (rule ccorres_abstract_cleanup) 314 apply csymbr 315 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 316 apply (rule_tac r'=dc and xf'=xfdc 317 in ccorres_split_nothrow) 318 apply (rule_tac P="ko_at' (RecvEP list) epptr and invs'" 319 in ccorres_from_vcg[where P'=UNIV]) 320 apply (rule allI, rule conseqPre, vcg) 321 apply clarsimp 322 apply (rule cmap_relationE1 [OF cmap_relation_ep]) 323 apply assumption 324 apply (erule ko_at_projectKO_opt) 325 apply (clarsimp simp: typ_heap_simps setEndpoint_def) 326 apply (rule rev_bexI) 327 apply (rule setObject_eq; simp add: objBits_simps')[1] 328 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 329 carch_state_relation_def carch_globals_def 330 cmachine_state_relation_def 331 fpu_null_state_heap_update_tag_disj_simps 332 packed_heap_update_collapse_hrs) 333 apply (clarsimp simp: cpspace_relation_def 334 update_ep_map_tos typ_heap_simps') 335 apply (erule(2) cpspace_relation_ep_update_ep) 336 subgoal by (simp add: cendpoint_relation_def endpoint_state_defs) 337 subgoal by simp 338 apply (rule ceqv_refl) 339 apply (simp only: ccorres_seq_skip dc_def[symmetric]) 340 apply (rule ccorres_split_nothrow_novcg) 341 apply (rule cancel_all_ccorres_helper) 342 apply ceqv 343 apply (ctac add: rescheduleRequired_ccorres) 344 apply (wp weak_sch_act_wf_lift_linear 345 cancelAllIPC_mapM_x_valid_queues 346 | simp)+ 347 apply (rule mapM_x_wp', wp)+ 348 apply (wp sts_st_tcb') 349 apply (clarsimp split: if_split) 350 apply (rule mapM_x_wp', wp)+ 351 apply (clarsimp simp: valid_tcb_state'_def) 352 apply (simp add: guard_is_UNIV_def) 353 apply (wp set_ep_valid_objs' hoare_vcg_const_Ball_lift 354 weak_sch_act_wf_lift_linear) 355 apply vcg 356 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 357 apply (rule ccorres_return_Skip) 358 apply (rename_tac list) 359 apply (simp add: endpoint_state_defs 360 Collect_False Collect_True 361 ccorres_cond_iffs dc_def[symmetric] 362 del: Collect_const) 363 apply (rule ccorres_rhs_assoc)+ 364 apply csymbr 365 apply (rule ccorres_abstract_cleanup) 366 apply csymbr 367 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 368 apply (rule_tac r'=dc and xf'=xfdc 369 in ccorres_split_nothrow) 370 apply (rule_tac P="ko_at' (SendEP list) epptr and invs'" 371 in ccorres_from_vcg[where P'=UNIV]) 372 apply (rule allI, rule conseqPre, vcg) 373 apply clarsimp 374 apply (rule cmap_relationE1 [OF cmap_relation_ep]) 375 apply assumption 376 apply (erule ko_at_projectKO_opt) 377 apply (clarsimp simp: typ_heap_simps setEndpoint_def) 378 apply (rule rev_bexI) 379 apply (rule setObject_eq, simp_all add: objBits_simps')[1] 380 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 381 carch_state_relation_def carch_globals_def 382 cmachine_state_relation_def 383 fpu_null_state_heap_update_tag_disj_simps 384 packed_heap_update_collapse_hrs) 385 apply (clarsimp simp: cpspace_relation_def typ_heap_simps' 386 update_ep_map_tos) 387 apply (erule(2) cpspace_relation_ep_update_ep) 388 subgoal by (simp add: cendpoint_relation_def endpoint_state_defs) 389 subgoal by simp 390 apply (rule ceqv_refl) 391 apply (simp only: ccorres_seq_skip dc_def[symmetric]) 392 apply (rule ccorres_split_nothrow_novcg) 393 apply (rule cancel_all_ccorres_helper) 394 apply ceqv 395 apply (ctac add: rescheduleRequired_ccorres) 396 apply (wp cancelAllIPC_mapM_x_valid_queues) 397 apply (wp mapM_x_wp' weak_sch_act_wf_lift_linear 398 sts_st_tcb' | clarsimp simp: valid_tcb_state'_def split: if_split)+ 399 apply (simp add: guard_is_UNIV_def) 400 apply (wp set_ep_valid_objs' hoare_vcg_const_Ball_lift 401 weak_sch_act_wf_lift_linear) 402 apply vcg 403 apply (clarsimp simp: valid_ep'_def invs_valid_objs' invs_queues) 404 apply (rule cmap_relationE1[OF cmap_relation_ep], assumption) 405 apply (erule ko_at_projectKO_opt) 406 apply (frule obj_at_valid_objs', clarsimp+) 407 apply (clarsimp simp: projectKOs valid_obj'_def valid_ep'_def) 408 subgoal by (auto simp: typ_heap_simps cendpoint_relation_def 409 Let_def tcb_queue_relation'_def 410 invs_valid_objs' valid_objs'_maxDomain valid_objs'_maxPriority 411 intro!: obj_at_conj') 412 apply (clarsimp simp: guard_is_UNIV_def) 413 apply (wp getEndpoint_wp) 414 apply clarsimp 415 done 416 417lemma empty_fail_getNotification: 418 "empty_fail (getNotification ep)" 419 unfolding getNotification_def 420 by (auto intro: empty_fail_getObject) 421 422lemma cancelAllSignals_ccorres: 423 "ccorres dc xfdc 424 (invs') (UNIV \<inter> {s. ntfnPtr_' s = Ptr ntfnptr}) [] 425 (cancelAllSignals ntfnptr) (Call cancelAllSignals_'proc)" 426 apply (cinit lift: ntfnPtr_') 427 apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) 428 apply (rule_tac xf'=ret__unsigned_longlong_' 429 and val="case ntfnObj rv of IdleNtfn \<Rightarrow> scast NtfnState_Idle 430 | ActiveNtfn _ \<Rightarrow> scast NtfnState_Active | WaitingNtfn _ \<Rightarrow> scast NtfnState_Waiting" 431 and R="ko_at' rv ntfnptr" 432 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 433 apply vcg 434 apply clarsimp 435 apply (erule cmap_relationE1 [OF cmap_relation_ntfn]) 436 apply (erule ko_at_projectKO_opt) 437 apply (clarsimp simp add: typ_heap_simps) 438 apply (simp add: cnotification_relation_def Let_def 439 split: ntfn.split_asm) 440 apply ceqv 441 apply (rule_tac A="invs' and ko_at' rv ntfnptr" 442 in ccorres_guard_imp2[where A'=UNIV]) 443 apply wpc 444 apply (simp add: notification_state_defs ccorres_cond_iffs 445 dc_def[symmetric]) 446 apply (rule ccorres_return_Skip) 447 apply (simp add: notification_state_defs ccorres_cond_iffs 448 dc_def[symmetric]) 449 apply (rule ccorres_return_Skip) 450 apply (rename_tac list) 451 apply (simp add: notification_state_defs ccorres_cond_iffs 452 dc_def[symmetric] Collect_True 453 del: Collect_const) 454 apply (rule ccorres_rhs_assoc)+ 455 apply csymbr 456 apply (rule ccorres_abstract_cleanup) 457 apply csymbr 458 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 459 apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) 460 apply (rule_tac P="ko_at' rv ntfnptr and invs'" 461 in ccorres_from_vcg[where P'=UNIV]) 462 apply (rule allI, rule conseqPre, vcg) 463 apply clarsimp 464 apply (rule_tac x=ntfnptr in cmap_relationE1 [OF cmap_relation_ntfn], assumption) 465 apply (erule ko_at_projectKO_opt) 466 apply (clarsimp simp: typ_heap_simps setNotification_def) 467 apply (rule rev_bexI) 468 apply (rule setObject_eq, simp_all add: objBits_simps')[1] 469 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 470 carch_state_relation_def carch_globals_def 471 cmachine_state_relation_def 472 fpu_null_state_heap_update_tag_disj_simps 473 packed_heap_update_collapse_hrs) 474 apply (clarsimp simp: cpspace_relation_def typ_heap_simps' 475 update_ntfn_map_tos) 476 apply (erule(2) cpspace_relation_ntfn_update_ntfn) 477 subgoal by (simp add: cnotification_relation_def notification_state_defs Let_def) 478 subgoal by simp 479 apply (rule ceqv_refl) 480 apply (simp only: ccorres_seq_skip dc_def[symmetric]) 481 apply (rule ccorres_split_nothrow_novcg) 482 apply (rule cancel_all_ccorres_helper) 483 apply ceqv 484 apply (ctac add: rescheduleRequired_ccorres) 485 apply (wp cancelAllIPC_mapM_x_valid_queues) 486 apply (wp mapM_x_wp' weak_sch_act_wf_lift_linear 487 sts_st_tcb' | clarsimp simp: valid_tcb_state'_def split: if_split)+ 488 apply (simp add: guard_is_UNIV_def) 489 apply (wp set_ntfn_valid_objs' hoare_vcg_const_Ball_lift 490 weak_sch_act_wf_lift_linear) 491 apply vcg 492 apply clarsimp 493 apply (rule cmap_relationE1[OF cmap_relation_ntfn], assumption) 494 apply (erule ko_at_projectKO_opt) 495 apply (frule obj_at_valid_objs', clarsimp+) 496 apply (clarsimp simp add: valid_obj'_def valid_ntfn'_def projectKOs) 497 subgoal by (auto simp: typ_heap_simps cnotification_relation_def 498 Let_def tcb_queue_relation'_def 499 invs_valid_objs' valid_objs'_maxDomain valid_objs'_maxPriority 500 intro!: obj_at_conj') 501 apply (clarsimp simp: guard_is_UNIV_def) 502 apply (wp getNotification_wp) 503 apply clarsimp 504 done 505 506lemma tcb_queue_concat: 507 "tcb_queue_relation getNext getPrev mp (xs @ z # ys) qprev qhead 508 \<Longrightarrow> tcb_queue_relation getNext getPrev mp (z # ys) 509 (tcb_ptr_to_ctcb_ptr (last ((ctcb_ptr_to_tcb_ptr qprev) # xs))) (tcb_ptr_to_ctcb_ptr z)" 510 apply (induct xs arbitrary: qprev qhead) 511 apply clarsimp 512 apply clarsimp 513 apply (elim meta_allE, drule(1) meta_mp) 514 apply (clarsimp cong: if_cong) 515 done 516 517lemma tcb_fields_ineq_helper: 518 "\<lbrakk> tcb_at' (ctcb_ptr_to_tcb_ptr x) s; tcb_at' (ctcb_ptr_to_tcb_ptr y) s \<rbrakk> \<Longrightarrow> 519 &(x\<rightarrow>[''tcbSchedPrev_C'']) \<noteq> &(y\<rightarrow>[''tcbSchedNext_C''])" 520 apply (clarsimp dest!: tcb_aligned'[OF obj_at'_weakenE, OF _ TrueI] 521 ctcb_ptr_to_tcb_ptr_aligned) 522 apply (clarsimp simp: field_lvalue_def ctcb_size_bits_def) 523 apply (subgoal_tac "is_aligned (ptr_val y - ptr_val x) 10" (*ctcb_size_bits*)) 524 apply (drule sym, fastforce simp: is_aligned_def dvd_def) 525 apply (erule(1) aligned_sub_aligned) 526 apply (simp add: word_bits_conv) 527 done 528 529end 530 531primrec 532 tcb_queue_relation2 :: "(tcb_C \<Rightarrow> tcb_C ptr) \<Rightarrow> (tcb_C \<Rightarrow> tcb_C ptr) 533 \<Rightarrow> (tcb_C ptr \<rightharpoonup> tcb_C) \<Rightarrow> tcb_C ptr list 534 \<Rightarrow> tcb_C ptr \<Rightarrow> tcb_C ptr \<Rightarrow> bool" 535where 536 "tcb_queue_relation2 getNext getPrev hp [] before after = True" 537| "tcb_queue_relation2 getNext getPrev hp (x # xs) before after = 538 (\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before 539 \<and> getNext tcb = hd (xs @ [after]) 540 \<and> tcb_queue_relation2 getNext getPrev hp xs x after)" 541 542lemma use_tcb_queue_relation2: 543 "tcb_queue_relation getNext getPrev hp xs qprev qhead 544 = (tcb_queue_relation2 getNext getPrev hp 545 (map tcb_ptr_to_ctcb_ptr xs) qprev (tcb_Ptr 0) 546 \<and> qhead = (hd (map tcb_ptr_to_ctcb_ptr xs @ [tcb_Ptr 0])))" 547 apply (induct xs arbitrary: qhead qprev) 548 apply simp 549 apply (simp add: conj_comms cong: conj_cong) 550 done 551 552lemma tcb_queue_relation2_concat: 553 "tcb_queue_relation2 getNext getPrev hp 554 (xs @ ys) before after 555 = (tcb_queue_relation2 getNext getPrev hp 556 xs before (hd (ys @ [after])) 557 \<and> tcb_queue_relation2 getNext getPrev hp 558 ys (last (before # xs)) after)" 559 apply (induct xs arbitrary: before) 560 apply simp 561 apply (rename_tac x xs before) 562 apply (simp split del: if_split) 563 apply (case_tac "hp x") 564 apply simp 565 apply simp 566 done 567 568lemma tcb_queue_relation2_cong: 569 "\<lbrakk>queue = queue'; before = before'; after = after'; 570 \<And>p. p \<in> set queue' \<Longrightarrow> mp p = mp' p\<rbrakk> 571 \<Longrightarrow> tcb_queue_relation2 getNext getPrev mp queue before after = 572 tcb_queue_relation2 getNext getPrev mp' queue' before' after'" 573 using [[hypsubst_thin = true]] 574 apply clarsimp 575 apply (induct queue' arbitrary: before') 576 apply simp+ 577 done 578 579context kernel_m begin 580 581lemma setThreadState_ccorres_valid_queues'_simple: 582 "ccorres dc xfdc (\<lambda>s. tcb_at' thread s \<and> valid_queues' s \<and> \<not> runnable' st \<and> sch_act_simple s) 583 ({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))} 584 \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] 585 (setThreadState st thread) (Call setThreadState_'proc)" 586 apply (cinit lift: tptr_' cong add: call_ignore_cong) 587 apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) 588 apply (ctac add: scheduleTCB_ccorres_valid_queues'_simple) 589 apply (wp threadSet_valid_queues'_and_not_runnable') 590 apply (clarsimp simp: weak_sch_act_wf_def valid_queues'_def) 591 done 592 593lemma suspend_ccorres: 594 assumes cteDeleteOne_ccorres: 595 "\<And>w slot. ccorres dc xfdc 596 (invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap 597 \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) 598 ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} 599 \<inter> {s. slot_' s = Ptr slot}) [] 600 (cteDeleteOne slot) (Call cteDeleteOne_'proc)" 601 shows 602 "ccorres dc xfdc 603 (invs' and sch_act_simple and tcb_at' thread and (\<lambda>s. thread \<noteq> ksIdleThread s)) 604 (UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) [] 605 (suspend thread) (Call suspend_'proc)" 606 apply (cinit lift: target_') 607 apply (ctac(no_vcg) add: cancelIPC_ccorres1 [OF cteDeleteOne_ccorres]) 608 apply (ctac(no_vcg) add: setThreadState_ccorres_valid_queues'_simple) 609 apply (ctac add: tcbSchedDequeue_ccorres') 610 apply (rule_tac Q="\<lambda>_. 611 (\<lambda>s. \<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> 612 obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d 613 \<and> tcbPriority tcb = p) t' s \<and> 614 (t' \<noteq> thread \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> 615 distinct (ksReadyQueues s (d, p))) and valid_queues' and valid_objs' and tcb_at' thread" 616 in hoare_post_imp) 617 apply clarsimp 618 apply (drule_tac x="t" in spec) 619 apply (drule_tac x=d in spec) 620 apply (drule_tac x=p in spec) 621 apply (clarsimp elim!: obj_at'_weakenE simp: inQ_def) 622 apply (wp_trace sts_valid_queues_partial)[1] 623 apply (rule hoare_strengthen_post) 624 apply (rule hoare_vcg_conj_lift) 625 apply (rule hoare_vcg_conj_lift) 626 apply (rule cancelIPC_sch_act_simple) 627 apply (rule cancelIPC_tcb_at'[where t=thread]) 628 apply (rule delete_one_conc_fr.cancelIPC_invs) 629 apply (fastforce simp: invs_valid_queues' invs_queues invs_valid_objs' 630 valid_tcb_state'_def) 631 apply (auto simp: "StrictC'_thread_state_defs") 632 done 633 634lemma cap_to_H_NTFNCap_tag: 635 "\<lbrakk> cap_to_H cap = NotificationCap word1 word2 a b; 636 cap_lift C_cap = Some cap \<rbrakk> \<Longrightarrow> 637 cap_get_tag C_cap = scast cap_notification_cap" 638 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) 639 by (simp_all add: Let_def cap_lift_def split: if_splits) 640 641lemmas ccorres_pre_getBoundNotification = ccorres_pre_threadGet [where f=tcbBoundNotification, folded getBoundNotification_def] 642 643lemma option_to_ptr_not_NULL: 644 "option_to_ptr x \<noteq> NULL \<Longrightarrow> x \<noteq> None" 645 by (auto simp: option_to_ptr_def option_to_0_def split: option.splits) 646 647lemma doUnbindNotification_ccorres: 648 "ccorres dc xfdc (invs' and tcb_at' tcb) 649 (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr} \<inter> {s. tcbptr_' s = tcb_ptr_to_ctcb_ptr tcb}) [] 650 (do ntfn \<leftarrow> getNotification ntfnptr; doUnbindNotification ntfnptr ntfn tcb od) 651 (Call doUnbindNotification_'proc)" 652 apply (cinit' lift: ntfnPtr_' tcbptr_') 653 apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) 654 apply (rule_tac P="invs' and ko_at' rv ntfnptr" and P'=UNIV 655 in ccorres_split_nothrow_novcg) 656 apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) 657 apply (rule allI, rule conseqPre, vcg) 658 apply (clarsimp simp: option_to_ptr_def option_to_0_def) 659 apply (frule cmap_relation_ntfn) 660 apply (erule (1) cmap_relation_ko_atE) 661 apply (rule conjI) 662 apply (erule h_t_valid_clift) 663 apply (clarsimp simp: setNotification_def split_def) 664 apply (rule bexI [OF _ setObject_eq]) 665 apply (simp add: rf_sr_def cstate_relation_def Let_def init_def 666 typ_heap_simps' 667 cpspace_relation_def update_ntfn_map_tos) 668 apply (elim conjE) 669 apply (intro conjI) 670 \<comment> \<open>tcb relation\<close> 671 apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) 672 apply (clarsimp simp: cnotification_relation_def Let_def 673 mask_def [where n=2] NtfnState_Waiting_def) 674 apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4]) 675 subgoal by (simp add: carch_state_relation_def 676 global_ioport_bitmap_heap_update_tag_disj_simps 677 fpu_null_state_heap_update_tag_disj_simps) 678 subgoal by (simp add: cmachine_state_relation_def) 679 subgoal by (simp add: h_t_valid_clift_Some_iff) 680 subgoal by (simp add: objBits_simps') 681 subgoal by (simp add: objBits_simps) 682 apply assumption 683 apply ceqv 684 apply (rule ccorres_move_c_guard_tcb) 685 apply (simp add: setBoundNotification_def) 686 apply (rule_tac P'="\<top>" and P="\<top>" 687 in threadSet_ccorres_lemma3[unfolded dc_def]) 688 apply vcg 689 apply simp 690 apply (erule(1) rf_sr_tcb_update_no_queue2) 691 apply (simp add: typ_heap_simps')+ 692 apply (simp add: tcb_cte_cases_def) 693 apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) 694 apply (simp add: invs'_def valid_state'_def) 695 apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ 696 done 697 698lemma doUnbindNotification_ccorres': 699 "ccorres dc xfdc (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) 700 (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr} \<inter> {s. tcbptr_' s = tcb_ptr_to_ctcb_ptr tcb}) [] 701 (doUnbindNotification ntfnptr ntfn tcb) 702 (Call doUnbindNotification_'proc)" 703 apply (cinit' lift: ntfnPtr_' tcbptr_') 704 apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV 705 in ccorres_split_nothrow_novcg) 706 apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) 707 apply (rule allI, rule conseqPre, vcg) 708 apply (clarsimp simp: option_to_ptr_def option_to_0_def) 709 apply (frule cmap_relation_ntfn) 710 apply (erule (1) cmap_relation_ko_atE) 711 apply (rule conjI) 712 apply (erule h_t_valid_clift) 713 apply (clarsimp simp: setNotification_def split_def) 714 apply (rule bexI [OF _ setObject_eq]) 715 apply (simp add: rf_sr_def cstate_relation_def Let_def init_def 716 typ_heap_simps' 717 cpspace_relation_def update_ntfn_map_tos) 718 apply (elim conjE) 719 apply (intro conjI) 720 \<comment> \<open>tcb relation\<close> 721 apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) 722 apply (clarsimp simp: cnotification_relation_def Let_def 723 mask_def [where n=2] NtfnState_Waiting_def) 724 apply (fold_subgoals (prefix))[2] 725 subgoal premises prems using prems 726 by (case_tac "ntfnObj ntfn", (simp add: option_to_ctcb_ptr_def)+) 727 subgoal by (simp add: carch_state_relation_def 728 global_ioport_bitmap_heap_update_tag_disj_simps 729 fpu_null_state_heap_update_tag_disj_simps) 730 subgoal by (simp add: cmachine_state_relation_def) 731 subgoal by (simp add: h_t_valid_clift_Some_iff) 732 subgoal by (simp add: objBits_simps') 733 subgoal by (simp add: objBits_simps) 734 apply assumption 735 apply ceqv 736 apply (rule ccorres_move_c_guard_tcb) 737 apply (simp add: setBoundNotification_def) 738 apply (rule_tac P'="\<top>" and P="\<top>" 739 in threadSet_ccorres_lemma3[unfolded dc_def]) 740 apply vcg 741 apply simp 742 apply (erule(1) rf_sr_tcb_update_no_queue2) 743 apply (simp add: typ_heap_simps')+ 744 apply (simp add: tcb_cte_cases_def) 745 apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) 746 apply (simp add: invs'_def valid_state'_def) 747 apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ 748 done 749 750 751lemma unbindNotification_ccorres: 752 "ccorres dc xfdc 753 (invs') (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb}) [] 754 (unbindNotification tcb) (Call unbindNotification_'proc)" 755 apply (cinit lift: tcb_') 756 apply (rule_tac xf'=ntfnPtr_' 757 and r'="\<lambda>rv rv'. rv' = option_to_ptr rv \<and> rv \<noteq> Some 0" 758 in ccorres_split_nothrow) 759 apply (simp add: getBoundNotification_def) 760 apply (rule_tac P="no_0_obj' and valid_objs'" in threadGet_vcg_corres_P) 761 apply (rule allI, rule conseqPre, vcg) 762 apply clarsimp 763 apply (drule obj_at_ko_at', clarsimp) 764 apply (drule spec, drule(1) mp, clarsimp) 765 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 766 apply (drule(1) ko_at_valid_objs', simp add: projectKOs) 767 apply (clarsimp simp: option_to_ptr_def option_to_0_def projectKOs 768 valid_obj'_def valid_tcb'_def) 769 apply ceqv 770 apply simp 771 apply wpc 772 apply (rule ccorres_cond_false) 773 apply (rule ccorres_return_Skip[unfolded dc_def]) 774 apply (rule ccorres_cond_true) 775 apply (ctac (no_vcg) add: doUnbindNotification_ccorres[unfolded dc_def, simplified]) 776 apply (wp gbn_wp') 777 apply vcg 778 apply (clarsimp simp: option_to_ptr_def option_to_0_def pred_tcb_at'_def 779 obj_at'_weakenE[OF _ TrueI] 780 split: option.splits) 781 apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) 782 done 783 784 785lemma unbindMaybeNotification_ccorres: 786 "ccorres dc xfdc (invs') (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) [] 787 (unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc)" 788 apply (cinit lift: ntfnPtr_') 789 apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) 790 apply (rule ccorres_rhs_assoc2) 791 apply (rule_tac P="ntfnBoundTCB rv \<noteq> None \<longrightarrow> 792 option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL" 793 in ccorres_gen_asm) 794 apply (rule_tac xf'=boundTCB_' 795 and val="option_to_ctcb_ptr (ntfnBoundTCB rv)" 796 and R="ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)" 797 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 798 apply vcg 799 apply clarsimp 800 apply (erule cmap_relationE1[OF cmap_relation_ntfn]) 801 apply (erule ko_at_projectKO_opt) 802 apply (clarsimp simp: typ_heap_simps cnotification_relation_def Let_def) 803 apply ceqv 804 apply wpc 805 apply (rule ccorres_cond_false) 806 apply (rule ccorres_return_Skip) 807 apply (rule ccorres_cond_true) 808 apply (rule ccorres_call[where xf'=xfdc]) 809 apply (rule doUnbindNotification_ccorres'[simplified]) 810 apply simp 811 apply simp 812 apply simp 813 apply (clarsimp simp add: guard_is_UNIV_def option_to_ctcb_ptr_def ) 814 apply (wp getNotification_wp) 815 apply (clarsimp ) 816 apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) 817 by (auto simp: valid_ntfn'_def valid_bound_tcb'_def obj_at'_def projectKOs 818 objBitsKO_def is_aligned_def option_to_ctcb_ptr_def tcb_at_not_NULL 819 split: ntfn.splits) 820 821lemma finaliseCap_True_cases_ccorres: 822 "\<And>final. isEndpointCap cap \<or> isNotificationCap cap 823 \<or> isReplyCap cap \<or> isDomainCap cap \<or> cap = NullCap \<Longrightarrow> 824 ccorres (\<lambda>rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') 825 \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 826 ret__struct_finaliseCap_ret_C_' 827 (invs') (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. final_' s = from_bool final} 828 \<inter> {s. exposed_' s = from_bool flag (* dave has name wrong *)}) [] 829 (finaliseCap cap final flag) (Call finaliseCap_'proc)" 830 apply (subgoal_tac "\<not> isArchCap \<top> cap") 831 prefer 2 832 apply (clarsimp simp: isCap_simps) 833 apply (cinit lift: cap_' final_' exposed_' cong: call_ignore_cong) 834 apply csymbr 835 apply (simp add: cap_get_tag_isCap Collect_False del: Collect_const) 836 apply (fold case_bool_If) 837 apply (simp add: false_def) 838 apply csymbr 839 apply wpc 840 apply (simp add: cap_get_tag_isCap ccorres_cond_univ_iff Let_def) 841 apply (rule ccorres_rhs_assoc)+ 842 apply (rule ccorres_split_nothrow_novcg) 843 apply (simp add: when_def) 844 apply (rule ccorres_cond2) 845 apply (clarsimp simp: Collect_const_mem from_bool_0) 846 apply csymbr 847 apply (rule ccorres_call[where xf'=xfdc], rule cancelAllIPC_ccorres) 848 apply simp 849 apply simp 850 apply simp 851 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 852 apply (simp add: return_def, vcg) 853 apply (rule ceqv_refl) 854 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 855 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 856 rule ccorres_split_throws) 857 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 858 apply (rule allI, rule conseqPre, vcg) 859 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff 860 irq_opt_relation_def) 861 apply vcg 862 apply wp 863 apply (simp add: guard_is_UNIV_def) 864 apply wpc 865 apply (simp add: cap_get_tag_isCap Let_def 866 ccorres_cond_empty_iff ccorres_cond_univ_iff) 867 apply (rule ccorres_rhs_assoc)+ 868 apply (rule ccorres_split_nothrow_novcg) 869 apply (simp add: when_def) 870 apply (rule ccorres_cond2) 871 apply (clarsimp simp: Collect_const_mem from_bool_0) 872 apply (subgoal_tac "cap_get_tag capa = scast cap_notification_cap") prefer 2 873 apply (clarsimp simp: ccap_relation_def isNotificationCap_def) 874 apply (case_tac cap, simp_all)[1] 875 apply (clarsimp simp: option_map_def split: option.splits) 876 apply (drule (2) cap_to_H_NTFNCap_tag[OF sym]) 877 apply (rule ccorres_rhs_assoc) 878 apply (rule ccorres_rhs_assoc) 879 apply csymbr 880 apply csymbr 881 apply (ctac (no_vcg) add: unbindMaybeNotification_ccorres) 882 apply (rule ccorres_call[where xf'=xfdc], rule cancelAllSignals_ccorres) 883 apply simp 884 apply simp 885 apply simp 886 apply (wp | wpc | simp add: guard_is_UNIV_def)+ 887 apply (rule ccorres_return_Skip') 888 apply (rule ceqv_refl) 889 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 890 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 891 rule ccorres_split_throws) 892 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 893 apply (rule allI, rule conseqPre, vcg) 894 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff 895 irq_opt_relation_def) 896 apply vcg 897 apply wp 898 apply (simp add: guard_is_UNIV_def) 899 apply wpc 900 apply (simp add: cap_get_tag_isCap Let_def 901 ccorres_cond_empty_iff ccorres_cond_univ_iff) 902 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 903 rule ccorres_split_throws) 904 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 905 apply (rule allI, rule conseqPre, vcg) 906 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff 907 irq_opt_relation_def) 908 apply vcg 909 apply wpc 910 apply (simp add: cap_get_tag_isCap Let_def 911 ccorres_cond_empty_iff ccorres_cond_univ_iff) 912 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 913 rule ccorres_split_throws) 914 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 915 apply (rule allI, rule conseqPre, vcg) 916 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff) 917 apply (clarsimp simp add: irq_opt_relation_def) 918 apply vcg 919 \<comment> \<open>NullCap case by exhaustion\<close> 920 apply (simp add: cap_get_tag_isCap Let_def 921 ccorres_cond_empty_iff ccorres_cond_univ_iff) 922 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 923 rule ccorres_split_throws) 924 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 925 apply (rule allI, rule conseqPre, vcg) 926 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff 927 irq_opt_relation_def) 928 apply vcg 929 apply (clarsimp simp: Collect_const_mem cap_get_tag_isCap) 930 apply (rule TrueI conjI impI TrueI)+ 931 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 932 apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def isNotificationCap_def 933 isEndpointCap_def valid_obj'_def projectKOs valid_ntfn'_def 934 valid_bound_tcb'_def 935 dest!: obj_at_valid_objs') 936 apply clarsimp 937 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 938 apply clarsimp 939 done 940 941lemma finaliseCap_True_standin_ccorres: 942 "\<And>final. 943 ccorres (\<lambda>rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') 944 \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 945 ret__struct_finaliseCap_ret_C_' 946 (invs') (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. final_' s = from_bool final} 947 \<inter> {s. exposed_' s = from_bool True (* dave has name wrong *)}) [] 948 (finaliseCapTrue_standin cap final) (Call finaliseCap_'proc)" 949 unfolding finaliseCapTrue_standin_simple_def 950 apply (case_tac "P :: bool" for P) 951 apply (erule finaliseCap_True_cases_ccorres) 952 apply (simp add: finaliseCap_def ccorres_fail') 953 done 954 955lemma offset_xf_for_sequence: 956 "\<forall>s f. offset_' (offset_'_update f s) = f (offset_' s) 957 \<and> globals (offset_'_update f s) = globals s" 958 by simp 959 960lemma invs'_invs_no_cicd': 961 "invs' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s" 962 by (simp add: invs'_invs_no_cicd) 963 964 965lemma hwASIDInvalidate_ccorres: 966 "ccorres dc xfdc \<top> 967 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vspace_' s = pml4e_Ptr vs}) hs 968 (hwASIDInvalidate asid vs) 969 (Call hwASIDInvalidate_'proc)" 970 apply (cinit lift: asid_' vspace_') 971 apply (ctac (no_vcg) add: invalidateASID_ccorres) 972 by clarsimp 973 974lemmas hwASIDInvalidate_typ_at'_lifts [wp] = typ_at_lifts [OF hwASIDInvalidate_typ_at'] 975 976crunches hwASIDInvalidate 977 for obj_at'[wp]: "\<lambda>s. P (obj_at' P' p s)" 978 and valid_objs'[wp]: valid_objs' 979 980lemma deleteASIDPool_ccorres: 981 "ccorres dc xfdc (invs' and (\<lambda>_. base < 2 ^ 12 \<and> pool \<noteq> 0)) 982 (UNIV \<inter> {s. asid_base_' s = base} \<inter> {s. pool_' s = Ptr pool}) [] 983 (deleteASIDPool base pool) (Call deleteASIDPool_'proc)" 984 apply (rule ccorres_gen_asm) 985 apply (cinit lift: asid_base_' pool_' simp: whileAnno_def) 986 apply (rule ccorres_assert) 987 apply (clarsimp simp: liftM_def dc_def[symmetric] fun_upd_def[symmetric] 988 when_def 989 simp del: Collect_const) 990 apply (rule ccorres_Guard)+ 991 apply (rule ccorres_pre_gets_x86KSASIDTable_ksArchState) 992 apply (rule_tac R="\<lambda>s. rv = x64KSASIDTable (ksArchState s)" in ccorres_cond2) 993 apply clarsimp 994 apply (subst rf_sr_x86KSASIDTable, assumption) 995 apply (simp add: asid_high_bits_word_bits) 996 apply (rule shiftr_less_t2n) 997 apply (simp add: asid_low_bits_def asid_high_bits_def) 998 apply (subst ucast_asid_high_bits_is_shift) 999 apply (simp add: mask_def, simp add: asid_bits_def) 1000 apply (simp add: option_to_ptr_def option_to_0_def split: option.split) 1001 apply (rule ccorres_Guard_Seq ccorres_rhs_assoc)+ 1002 apply (rule ccorres_pre_getObject_asidpool) 1003 apply (rename_tac poolKO) 1004 apply (simp only: mapM_discarded) 1005 apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) 1006 apply (simp add: word_sle_def Kernel_C.asidLowBits_def Collect_True 1007 del: Collect_const) 1008 apply (rule ccorres_semantic_equivD2[rotated]) 1009 apply (simp only: semantic_equiv_def) 1010 apply (rule Seq_ceqv [OF ceqv_refl _ xpres_triv]) 1011 apply (simp only: ceqv_Guard_UNIV) 1012 apply (rule While_ceqv [OF _ _ xpres_triv], rule impI, rule refl) 1013 apply (rule ceqv_remove_eqv_skip) 1014 apply (simp add: ceqv_Guard_UNIV ceqv_refl) 1015 apply (rule_tac F="\<lambda>n. ko_at' poolKO pool and valid_objs'" 1016 in ccorres_mapM_x_while_gen[OF _ _ _ _ _ offset_xf_for_sequence, 1017 where j=1, simplified]) 1018 apply (intro allI impI) 1019 apply (rule ccorres_guard_imp2) 1020 apply (rule_tac xf'="offset_'" in ccorres_abstract, ceqv) 1021 apply (rule_tac P="rv' = of_nat n" in ccorres_gen_asm2) 1022 apply (rule ccorres_rhs_assoc)+ 1023 apply (rule ccorres_Guard_Seq[where F=ArrayBounds]) 1024 apply (rule ccorres_move_c_guard_ap) 1025 apply (rule_tac xf' = asid_map_' 1026 and F = "\<lambda>rv. asid_map_relation (inv ASIDPool poolKO (of_nat n)) rv" 1027 and R = "ko_at' poolKO pool" 1028 in ccorres_symb_exec_r_rv_abstract[where R'=UNIV]) 1029 apply (vcg, clarsimp) 1030 apply (clarsimp dest!: rf_sr_cpspace_asidpool_relation) 1031 apply (erule(1) cmap_relation_ko_atE) 1032 apply (clarsimp simp: typ_heap_simps casid_pool_relation_def 1033 array_relation_def asid_low_bits_of_mask_eq 1034 split: asidpool.split_asm asid_pool_C.split_asm) 1035 apply (drule_tac x="of_nat n" in spec) 1036 apply (subst (asm) Suc_unat_minus_one, clarsimp simp: asid_low_bits_def) 1037 apply (subst (asm) word64_less_sub_le, clarsimp simp: asid_low_bits_def word_bits_def) 1038 apply (fastforce simp: word_of_nat_less inv_ASIDPool case_bool_If 1039 asid_map_relation_def asid_map_lift_def Let_def 1040 asid_map_tag_defs asid_low_bits_def unat_of_nat 1041 split: option.split_asm asid_map_CL.split_asm if_split_asm) 1042 apply ceqv 1043 apply csymbr 1044 apply (rule_tac R="ko_at' poolKO pool and valid_objs'" in ccorres_cond2) 1045 apply (clarsimp dest!: rf_sr_cpspace_asidpool_relation) 1046 apply (erule cmap_relationE1, erule ko_at_projectKO_opt) 1047 apply (clarsimp simp: casid_pool_relation_def typ_heap_simps 1048 inv_ASIDPool 1049 split: asidpool.split_asm asid_pool_C.split_asm) 1050 apply (simp add: upto_enum_word del: upt.simps) 1051 apply (drule(1) ko_at_valid_objs') 1052 apply (simp add: projectKOs) 1053 apply (clarsimp simp: array_relation_def valid_obj'_def ran_def) 1054 apply (drule_tac x="of_nat n" in spec)+ 1055 apply (simp add: asid_low_bits_def word_le_nat_alt) 1056 apply (simp add: word_unat.Abs_inverse unats_def) 1057 apply (clarsimp simp: asid_map_relation_def false_def asid_map_tag_defs 1058 asid_map_lift_def Let_def 1059 split: option.split_asm asid_map_CL.split_asm if_splits) 1060 apply (rule ccorres_rhs_assoc)+ 1061 apply csymbr 1062 apply csymbr 1063 apply (ctac (no_vcg) add: hwASIDInvalidate_ccorres) 1064 apply (rule ccorres_return_Skip) 1065 apply vcg 1066 apply (clarsimp simp: Collect_const_mem) 1067 apply (simp add: upto_enum_word typ_at_to_obj_at_arches 1068 obj_at'_weakenE[OF _ TrueI] 1069 del: upt.simps) 1070 apply (rule conjI, clarsimp simp: asid_low_bits_def) 1071 apply (rule conjI, clarsimp simp: ucast_of_nat_small) 1072 apply (clarsimp simp: asid_map_lifts asid_map_relation_def) 1073 apply (simp add: asid_low_bits_def word_of_nat_less) 1074 apply (clarsimp simp: asid_low_bits_def ucast_less_ucast[where y="0x200" and 'a=32, simplified]) 1075 apply (vcg exspec=hwASIDInvalidate_modifies) 1076 apply clarsimp 1077 apply (rule hoare_pre, wp) 1078 apply simp 1079 apply (simp add: upto_enum_word asid_low_bits_def) 1080 apply ceqv 1081 apply (rule ccorres_move_const_guard)+ 1082 apply (rule ccorres_split_nothrow_novcg_dc) 1083 apply (rule_tac P="\<lambda>s. rv = x64KSASIDTable (ksArchState s)" 1084 in ccorres_from_vcg[where P'=UNIV]) 1085 apply (rule allI, rule conseqPre, vcg) 1086 apply (clarsimp simp: simpler_modify_def) 1087 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 1088 carch_state_relation_def cmachine_state_relation_def 1089 carch_globals_def h_t_valid_clift_Some_iff) 1090 apply (erule array_relation_update[unfolded fun_upd_def]) 1091 apply (simp add: asid_high_bits_of_def unat_ucast asid_low_bits_def) 1092 apply (rule sym, rule nat_mod_eq') 1093 apply (rule order_less_le_trans, rule iffD1[OF word_less_nat_alt]) 1094 apply (rule shiftr_less_t2n[where m=3]) 1095 subgoal by simp 1096 subgoal by simp 1097 subgoal by (simp add: option_to_ptr_def option_to_0_def) 1098 subgoal by (simp add: asid_high_bits_def) 1099 apply (rule ccorres_pre_getCurThread) 1100 apply (ctac add: setVMRoot_ccorres) 1101 apply wp 1102 apply (simp add: guard_is_UNIV_def) 1103 apply (simp add: pred_conj_def fun_upd_def[symmetric] 1104 cur_tcb'_def[symmetric]) 1105 apply (strengthen invs'_invs_no_cicd', strengthen invs_asid_update_strg') 1106 apply (rule mapM_x_wp') 1107 apply (rule hoare_pre, wp) 1108 apply simp 1109 apply (simp add: guard_is_UNIV_def Kernel_C.asidLowBits_def 1110 word_sle_def word_sless_def Collect_const_mem 1111 mask_def asid_bits_def plus_one_helper 1112 asid_shiftr_low_bits_less) 1113 apply (rule ccorres_return_Skip) 1114 apply (simp add: Kernel_C.asidLowBits_def 1115 word_sle_def word_sless_def) 1116 apply (auto simp: asid_shiftr_low_bits_less Collect_const_mem 1117 mask_def asid_bits_def plus_one_helper) 1118 done 1119 1120 1121lemma deleteASID_ccorres: 1122 "ccorres dc xfdc (invs' and K (asid < 2 ^ 12) and K (vs \<noteq> 0)) 1123 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vspace_' s = Ptr vs}) [] 1124 (deleteASID asid vs) (Call deleteASID_'proc)" 1125 apply (cinit lift: asid_' vspace_' cong: call_ignore_cong) 1126 apply (rule ccorres_Guard_Seq)+ 1127 apply (rule_tac r'="\<lambda>rv rv'. case rv (ucast (asid_high_bits_of asid)) of 1128 None \<Rightarrow> rv' = NULL 1129 | Some v \<Rightarrow> rv' = Ptr v \<and> rv' \<noteq> NULL" 1130 and xf'="poolPtr_'" in ccorres_split_nothrow) 1131 apply (rule_tac P="invs' and K (asid < 2 ^ 12)" 1132 and P'=UNIV in ccorres_from_vcg) 1133 apply (rule allI, rule conseqPre, vcg) 1134 apply (clarsimp simp: simpler_gets_def Let_def) 1135 apply (erule(1) getKSASIDTable_ccorres_stuff) 1136 apply (simp add: asid_high_bits_of_def 1137 asidLowBits_def Kernel_C.asidLowBits_def 1138 asid_low_bits_def unat_ucast) 1139 apply (rule sym, rule Divides.mod_less, simp) 1140 apply (rule unat_less_power[where sz=3, simplified]) 1141 apply (simp add: word_bits_conv) 1142 apply (rule shiftr_less_t2n[where m=3, simplified]) 1143 apply simp 1144 apply (rule order_less_le_trans, rule ucast_less) 1145 apply simp 1146 apply (simp add: asid_high_bits_def) 1147 apply ceqv 1148 apply wpc 1149 apply (simp add: ccorres_cond_iffs dc_def[symmetric] 1150 Collect_False 1151 del: Collect_const 1152 cong: call_ignore_cong) 1153 apply (rule ccorres_return_Skip) 1154 apply (clarsimp simp: dc_def[symmetric] when_def 1155 Collect_True liftM_def 1156 cong: conj_cong call_ignore_cong 1157 del: Collect_const) 1158 apply ccorres_rewrite 1159 apply (rule ccorres_rhs_assoc)+ 1160 apply (rule ccorres_pre_getObject_asidpool) 1161 apply (rule ccorres_Guard_Seq[where F=ArrayBounds]) 1162 apply (rule ccorres_move_c_guard_ap) 1163 apply (rule ccorres_Guard_Seq)+ 1164 apply (rename_tac pool) 1165 apply (rule ccorres_rhs_assoc2) 1166 apply (rule ccorres_rhs_assoc2) 1167 apply (rule ccorres_rhs_assoc2) 1168 apply (rule_tac xf'=ret__int_' 1169 and val="from_bool (inv ASIDPool pool (ucast (asid_low_bits_of asid)) 1170 = Some vs)" 1171 and R="ko_at' pool x2 and K (vs \<noteq> 0)" 1172 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 1173 apply (vcg, clarsimp) 1174 apply (clarsimp dest!: rf_sr_cpspace_asidpool_relation) 1175 apply (erule(1) cmap_relation_ko_atE) 1176 apply (clarsimp simp: typ_heap_simps casid_pool_relation_def 1177 array_relation_def asid_low_bits_of_mask_eq 1178 split: asidpool.split_asm asid_pool_C.split_asm) 1179 apply (drule_tac x="asid && mask asid_low_bits" in spec) 1180 apply (simp add: asid_low_bits_def Kernel_C.asidLowBits_def 1181 mask_def word_and_le1 asid_map_relation_def) 1182 apply (rule conjI, fastforce simp: asid_map_lifts from_bool_def case_bool_If inv_ASIDPool) 1183 apply (fastforce simp: from_bool_def case_bool_If inv_ASIDPool asid_map_lift_def 1184 split: option.split_asm asid_map_CL.split_asm if_split_asm) 1185 apply ceqv 1186 apply (rule ccorres_cond2[where R=\<top>]) 1187 apply (simp add: Collect_const_mem from_bool_0) 1188 apply (rule ccorres_rhs_assoc)+ 1189 apply (ctac (no_vcg) add: hwASIDInvalidate_ccorres) 1190 apply csymbr 1191 apply (rule ccorres_Guard_Seq[where F=ArrayBounds]) 1192 apply (rule ccorres_move_c_guard_ap) 1193 apply (rule ccorres_Guard_Seq)+ 1194 apply (rule ccorres_split_nothrow_novcg_dc) 1195 apply (rule_tac P="ko_at' pool x2" in ccorres_from_vcg[where P'=UNIV]) 1196 apply (rule allI, rule conseqPre, vcg) 1197 apply clarsimp 1198 apply (rule cmap_relationE1[OF rf_sr_cpspace_asidpool_relation], 1199 assumption, erule ko_at_projectKO_opt) 1200 apply (rule bexI [OF _ setObject_eq], 1201 simp_all add: objBits_simps archObjSize_def pageBits_def)[1] 1202 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def typ_heap_simps) 1203 apply (rule conjI) 1204 apply (clarsimp simp: cpspace_relation_def typ_heap_simps' 1205 update_asidpool_map_tos 1206 update_asidpool_map_to_asidpools) 1207 apply (rule cmap_relation_updI, simp_all)[1] 1208 apply (simp add: casid_pool_relation_def fun_upd_def[symmetric] 1209 inv_ASIDPool 1210 split: asidpool.split_asm asid_pool_C.split_asm) 1211 apply (erule array_relation_update) 1212 subgoal by (simp add: mask_def asid_low_bits_of_mask_eq) 1213 subgoal by (clarsimp dest!: asid_map_lift_asid_map_none simp: asid_map_relation_def) 1214 subgoal by (simp add: asid_low_bits_def) 1215 subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def 1216 fpu_null_state_heap_update_tag_disj_simps 1217 global_ioport_bitmap_heap_update_tag_disj_simps 1218 carch_globals_def update_asidpool_map_tos) 1219 apply (rule ccorres_pre_getCurThread) 1220 apply (ctac add: setVMRoot_ccorres) 1221 apply (simp add: cur_tcb'_def[symmetric]) 1222 apply (strengthen invs'_invs_no_cicd') 1223 apply wp 1224 apply (clarsimp simp: rf_sr_def guard_is_UNIV_def 1225 cstate_relation_def Let_def) 1226 apply wp 1227 apply (rule ccorres_return_Skip) 1228 subgoal by (clarsimp simp: guard_is_UNIV_def Collect_const_mem 1229 word_sle_def word_sless_def 1230 Kernel_C.asidLowBits_def 1231 asid_low_bits_def order_le_less_trans [OF word_and_le1]) 1232 apply wp 1233 apply vcg 1234 apply (clarsimp simp: Collect_const_mem if_1_0_0 1235 word_sless_def word_sle_def 1236 Kernel_C.asidLowBits_def 1237 typ_at_to_obj_at_arches) 1238 apply (rule conjI) 1239 apply (clarsimp simp: mask_def inv_ASIDPool 1240 split: asidpool.split) 1241 apply (frule obj_at_valid_objs', clarsimp+) 1242 apply (clarsimp simp: asid_bits_def typ_at_to_obj_at_arches 1243 obj_at'_weakenE[OF _ TrueI] 1244 fun_upd_def[symmetric] valid_obj'_def 1245 projectKOs 1246 invs_cur') 1247 apply (rule conjI, blast) 1248 subgoal by (fastforce simp: inv_into_def ran_def split: if_split_asm) 1249 by (clarsimp simp: order_le_less_trans [OF word_and_le1] 1250 asid_shiftr_low_bits_less asid_bits_def mask_def 1251 plus_one_helper arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def] 1252 split: option.split_asm) 1253 1254lemma setObject_ccorres_lemma: 1255 fixes val :: "'a :: pspace_storable" shows 1256 "\<lbrakk> \<And>s. \<Gamma> \<turnstile> (Q s) c {s'. (s \<lparr> ksPSpace := ksPSpace s (ptr \<mapsto> injectKO val) \<rparr>, s') \<in> rf_sr},{}; 1257 \<And>s s' val (val' :: 'a). \<lbrakk> ko_at' val' ptr s; (s, s') \<in> rf_sr \<rbrakk> 1258 \<Longrightarrow> s' \<in> Q s; 1259 \<And>val :: 'a. updateObject val = updateObject_default val; 1260 \<And>val :: 'a. (1 :: machine_word) < 2 ^ objBits val; 1261 \<And>(val :: 'a) (val' :: 'a). objBits val = objBits val'; 1262 \<Gamma> \<turnstile> Q' c UNIV \<rbrakk> 1263 \<Longrightarrow> ccorres dc xfdc \<top> Q' hs 1264 (setObject ptr val) c" 1265 apply (rule ccorres_from_vcg_nofail) 1266 apply (rule allI) 1267 apply (case_tac "obj_at' (\<lambda>x :: 'a. True) ptr \<sigma>") 1268 apply (rule_tac P'="Q \<sigma>" in conseqPre, rule conseqPost, assumption) 1269 apply clarsimp 1270 apply (rule bexI [OF _ setObject_eq], simp+) 1271 apply (drule obj_at_ko_at') 1272 apply clarsimp 1273 apply clarsimp 1274 apply (rule conseqPre, erule conseqPost) 1275 apply clarsimp 1276 apply (subgoal_tac "fst (setObject ptr val \<sigma>) = {}") 1277 apply simp 1278 apply (erule notE, erule_tac s=\<sigma> in empty_failD[rotated]) 1279 apply (simp add: setObject_def split_def) 1280 apply (rule ccontr) 1281 apply (clarsimp elim!: nonemptyE) 1282 apply (frule use_valid [OF _ obj_at_setObject3[where P=\<top>]], simp_all)[1] 1283 apply (simp add: typ_at_to_obj_at'[symmetric]) 1284 apply (frule(1) use_valid [OF _ setObject_typ_at']) 1285 apply simp 1286 apply simp 1287 apply clarsimp 1288 done 1289 1290lemma findVSpaceForASID_nonzero: 1291 "\<lbrace>\<top>\<rbrace> findVSpaceForASID asid \<lbrace>\<lambda>rv s. rv \<noteq> 0\<rbrace>,-" 1292 apply (simp add: findVSpaceForASID_def cong: option.case_cong) 1293 apply (wp | wpc | simp only: o_def simp_thms)+ 1294 done 1295 1296lemma unat_shiftr_le_bound: 1297 "2 ^ (len_of TYPE('a :: len) - n) - 1 \<le> bnd \<Longrightarrow> 0 < n 1298 \<Longrightarrow> unat ((x :: 'a word) >> n) \<le> bnd" 1299 apply (erule order_trans[rotated], simp) 1300 apply (rule nat_le_Suc_less_imp) 1301 apply (rule unat_less_helper, simp) 1302 apply (rule shiftr_less_t2n3) 1303 apply simp 1304 apply simp 1305 done 1306 1307lemma flushTable_ccorres: 1308 "ccorres dc xfdc (invs' and page_table_at' ptPtr and (\<lambda>s. asid \<le> mask asid_bits \<and> vptr < pptrBase)) 1309 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vptr_' s = vptr} 1310 \<inter> {s. pt_' s = pte_Ptr ptPtr} \<inter> {s. vspace_' s = pml4e_Ptr vspace}) 1311 [] (flushTable vspace vptr ptPtr asid) (Call flushTable_'proc)" 1312 apply (rule ccorres_gen_asm) 1313 apply (cinit lift: asid_' vptr_' pt_' vspace_') 1314 apply (rule ccorres_assert) 1315 apply (rule ccorres_name_ksCurThread) 1316 apply (rule_tac val="tcb_ptr_to_ctcb_ptr rv" and xf'="\<lambda>s. ksCurThread_' (globals s)" 1317 in ccorres_abstract_known, ceqv) 1318 apply (simp add: cte_C_size del: Collect_const) 1319 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_move_c_guard_tcb_ctes)+ 1320 apply (rule ccorres_symb_exec_r) 1321 apply (rule ccorres_rel_imp) 1322 apply (clarsimp simp: whileAnno_def objBits_simps archObjSize_def) 1323 apply csymbr 1324 apply (rule_tac i="0" and F="\<lambda>n s. page_table_at' ptPtr s" in ccorres_mapM_x_while') 1325 apply (clarsimp simp: bit_simps) 1326 apply (rule ccorres_guard_imp2) 1327 apply (rule ccorres_pre_getObject_pte, rename_tac pte) 1328 apply (rule ccorres_move_array_assertion_pt) 1329 apply (rule ccorres_Guard_Seq) 1330 apply (rule ccorres_move_array_assertion_pt) 1331 apply (rule ccorres_rhs_assoc) 1332 apply csymbr 1333 apply (rule ccorres_abstract_cleanup) 1334 apply (rule ccorres_move_array_assertion_pt) 1335 apply ccorres_rewrite 1336 apply wpc 1337 apply (rule ccorres_cond_false, rule ccorres_return_Skip) 1338 apply (rule ccorres_cond_true) 1339 apply (rule_tac xf'=ret__int_' and val=1 and R=\<top> and R'=UNIV 1340 in ccorres_symb_exec_r_known_rv) 1341 apply vcg 1342 apply clarsimp 1343 apply ceqv 1344 apply ccorres_rewrite 1345 apply (ctac (no_vcg) add: invalidateTranslationSingleASID_ccorres) 1346 apply vcg 1347 apply (clarsimp simp: unat_gt_0) 1348 apply (rule conjI, clarsimp simp: cpte_relation_def upto_enum_word word_shift_by_3 1349 typ_heap_simps 1350 split: if_split_asm) 1351 apply (rule conjI, clarsimp simp: bit_simps upto_enum_word cpte_relation_def 1352 word_shift_by_3 typ_heap_simps 1353 split: if_split) 1354 apply (clarsimp simp: bit_simps) 1355 apply (rule context_conjI, rule word_unat_less_le, 1356 clarsimp simp: word_le_not_less 1357 dest!:unat_less_helper) 1358 apply clarsimp 1359 apply (rule c_guard_abs_pte[rule_format]) 1360 apply (rule conjI, assumption, 1361 clarsimp simp: word_shift_by_3 page_table_at'_def bit_simps) 1362 apply (drule_tac x="of_nat n" in spec) 1363 apply (clarsimp simp: word_le_not_less[symmetric]) 1364 apply unat_arith 1365 apply (clarsimp simp: bit_simps upto_enum_word) 1366 apply (rule allI, rule conseqPre, vcg) 1367 apply clarsimp 1368 apply (wpsimp wp: getPTE_wp) 1369 apply (clarsimp simp: bit_simps word_bits_def) 1370 apply clarsimp 1371 apply vcg 1372 apply (rule conseqPre, vcg, clarsimp) 1373 by (clarsimp simp: rf_sr_ksCurThread typ_heap_simps invs_cur'[simplified cur_tcb'_def] 1374 tcb_cnode_index_defs) 1375 1376lemma unmapPageTable_ccorres: 1377 "ccorres dc xfdc (invs' and page_table_at' ptPtr and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < pptrBase)) 1378 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vaddr___unsigned_long_' s = vaddr} \<inter> {s. pt_' s = Ptr ptPtr}) 1379 [] (unmapPageTable asid vaddr ptPtr) (Call unmapPageTable_'proc)" 1380 apply (rule ccorres_gen_asm) 1381 apply (cinit lift: asid_' vaddr___unsigned_long_' pt_') 1382 apply (clarsimp simp add: ignoreFailure_liftM) 1383 apply (ctac add: findVSpaceForASID_ccorres,rename_tac vspace find_ret) 1384 apply clarsimp 1385 apply (ctac add: lookupPDSlot_ccorres, rename_tac pdSlot lu_ret) 1386 apply (clarsimp simp add: pde_pde_pt_def liftE_bindE) 1387 apply (rule ccorres_rhs_assoc2) 1388 apply (rule ccorres_rhs_assoc2) 1389 apply (rule ccorres_rhs_assoc2) 1390 apply (rule ccorres_pre_getObject_pde) 1391 apply (simp only: pde_case_isPageTablePDE) 1392 apply (rule_tac xf'=ret__int_' 1393 and R'=UNIV 1394 and val="from_bool (isPageTablePDE pde \<and> pdeTable pde = addrFromPPtr ptPtr)" 1395 and R="ko_at' pde pdSlot" 1396 in ccorres_symb_exec_r_known_rv_UNIV) 1397 apply vcg 1398 apply clarsimp 1399 apply (erule cmap_relationE1[OF rf_sr_cpde_relation]) 1400 apply (erule ko_at_projectKO_opt) 1401 apply (rename_tac pde_C) 1402 apply (clarsimp simp: typ_heap_simps) 1403 apply (rule conjI, clarsimp simp: pde_pde_pt_def) 1404 apply (drule pde_lift_pde_pt[simplified pde_pde_pt_def, simplified]) 1405 apply (clarsimp simp: from_bool_def cpde_relation_def Let_def isPageTablePDE_def 1406 pde_pde_pt_lift_def case_bool_If 1407 split: pde.split_asm) 1408 apply clarsimp 1409 apply (simp add: from_bool_def split:bool.splits) 1410 apply (rule strenghten_False_imp) 1411 apply (simp add: cpde_relation_def Let_def) 1412 apply (subgoal_tac "pde_get_tag pde_C = 1") 1413 apply (clarsimp dest!: pde_lift_pde_large[simplified pde_pde_large_def, simplified] 1414 simp: isPageTablePDE_def split: pde.splits) 1415 apply (clarsimp simp: pde_get_tag_def word_and_1) 1416 apply ceqv 1417 apply (rule ccorres_Cond_rhs_Seq) 1418 apply (simp add: from_bool_0) 1419 apply ccorres_rewrite 1420 apply (clarsimp simp: throwError_def) 1421 apply (rule ccorres_return_void_C[simplified dc_def]) 1422 apply (simp add: from_bool_0) 1423 apply (rule ccorres_liftE[simplified dc_def]) 1424 apply (ctac add: flushTable_ccorres) 1425 apply (csymbr, rename_tac invalidPDE) 1426 apply (rule ccorres_split_nothrow_novcg_dc) 1427 apply (rule storePDE_Basic_ccorres) 1428 apply (simp add: cpde_relation_def Let_def) 1429 apply (csymbr, rename_tac root) 1430 apply (ctac add: invalidatePageStructureCacheASID_ccorres[simplified dc_def]) 1431 apply wp 1432 apply (clarsimp simp add: guard_is_UNIV_def) 1433 apply wp 1434 apply clarsimp 1435 apply (vcg exspec=flushTable_modifies) 1436 apply (clarsimp simp: guard_is_UNIV_def) 1437 apply (simp,ccorres_rewrite,simp add:throwError_def) 1438 apply (rule ccorres_return_void_C[simplified dc_def]) 1439 apply (clarsimp,wp) 1440 apply (rule_tac Q'="\<lambda>_ s. invs' s \<and> page_table_at' ptPtr s" in hoare_post_imp_R) 1441 apply wp 1442 apply clarsimp 1443 apply (vcg exspec=lookupPDSlot_modifies) 1444 apply (simp,ccorres_rewrite,simp add:throwError_def) 1445 apply (rule ccorres_return_void_C[simplified dc_def]) 1446 apply wp 1447 apply vcg 1448 apply (auto simp add: asid_wf_def mask_def) 1449 done 1450 1451lemma return_Null_ccorres: 1452 "ccorres ccap_relation ret__struct_cap_C_' 1453 \<top> UNIV (SKIP # hs) 1454 (return NullCap) (\<acute>ret__struct_cap_C :== CALL cap_null_cap_new() 1455 ;; return_C ret__struct_cap_C_'_update ret__struct_cap_C_')" 1456 apply (rule ccorres_from_vcg_throws) 1457 apply (rule allI, rule conseqPre, vcg) 1458 apply (clarsimp simp add: ccap_relation_NullCap_iff return_def) 1459 done 1460 1461lemma no_0_pml4_at'[elim!]: 1462 "\<lbrakk> page_map_l4_at' 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" 1463 apply (clarsimp simp: page_map_l4_at'_def) 1464 apply (drule spec[where x=0], clarsimp simp: bit_simps) 1465 done 1466 1467lemma ccte_relation_ccap_relation: 1468 "ccte_relation cte cte' \<Longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C cte')" 1469 by (clarsimp simp: ccte_relation_def ccap_relation_def 1470 cte_to_H_def map_option_Some_eq2 1471 c_valid_cte_def) 1472 1473lemma isFinalCapability_ccorres: 1474 "ccorres ((=) \<circ> from_bool) ret__unsigned_long_' 1475 (cte_wp_at' ((=) cte) slot and invs') 1476 (UNIV \<inter> {s. cte_' s = Ptr slot}) [] 1477 (isFinalCapability cte) (Call isFinalCapability_'proc)" 1478 apply (cinit lift: cte_') 1479 apply (rule ccorres_Guard_Seq) 1480 apply (simp add: Let_def del: Collect_const) 1481 apply (rule ccorres_symb_exec_r) 1482 apply (rule_tac xf'="mdb_'" in ccorres_abstract) 1483 apply ceqv 1484 apply (rule_tac P="mdb_node_to_H (mdb_node_lift rv') = cteMDBNode cte" in ccorres_gen_asm2) 1485 apply csymbr 1486 apply (rule_tac r'="(=) \<circ> from_bool" and xf'="prevIsSameObject_'" 1487 in ccorres_split_nothrow_novcg) 1488 apply (rule ccorres_cond2[where R=\<top>]) 1489 apply (clarsimp simp: Collect_const_mem nullPointer_def) 1490 apply (simp add: mdbPrev_to_H[symmetric]) 1491 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 1492 apply (rule allI, rule conseqPre, vcg) 1493 apply (simp add: return_def from_bool_def false_def) 1494 apply (rule ccorres_rhs_assoc)+ 1495 apply (rule ccorres_symb_exec_l[OF _ getCTE_inv getCTE_wp empty_fail_getCTE]) 1496 apply (rule_tac P="cte_wp_at' ((=) cte) slot 1497 and cte_wp_at' ((=) rv) (mdbPrev (cteMDBNode cte)) 1498 and valid_cap' (cteCap rv) 1499 and K (capAligned (cteCap cte) \<and> capAligned (cteCap rv))" 1500 and P'=UNIV in ccorres_from_vcg) 1501 apply (rule allI, rule conseqPre, vcg) 1502 apply (clarsimp simp: return_def mdbPrev_to_H[symmetric]) 1503 apply (simp add: rf_sr_cte_at_validD) 1504 apply (clarsimp simp: cte_wp_at_ctes_of) 1505 apply (rule cmap_relationE1 [OF cmap_relation_cte], assumption+, 1506 simp?, simp add: typ_heap_simps)+ 1507 apply (drule ccte_relation_ccap_relation)+ 1508 apply (rule exI, rule conjI, assumption)+ 1509 apply (auto)[1] 1510 apply ceqv 1511 apply (clarsimp simp del: Collect_const) 1512 apply (rule ccorres_cond2[where R=\<top>]) 1513 apply (simp add: from_bool_0 Collect_const_mem) 1514 apply (rule ccorres_return_C, simp+)[1] 1515 apply csymbr 1516 apply (rule ccorres_cond2[where R=\<top>]) 1517 apply (simp add: nullPointer_def Collect_const_mem mdbNext_to_H[symmetric]) 1518 apply (rule ccorres_return_C, simp+)[1] 1519 apply (rule ccorres_symb_exec_l[OF _ getCTE_inv getCTE_wp empty_fail_getCTE]) 1520 apply (rule_tac P="cte_wp_at' ((=) cte) slot 1521 and cte_wp_at' ((=) rva) (mdbNext (cteMDBNode cte)) 1522 and K (capAligned (cteCap rva) \<and> capAligned (cteCap cte)) 1523 and valid_cap' (cteCap cte)" 1524 and P'=UNIV in ccorres_from_vcg_throws) 1525 apply (rule allI, rule conseqPre, vcg) 1526 apply (clarsimp simp: return_def from_bool_eq_if from_bool_0 1527 mdbNext_to_H[symmetric] rf_sr_cte_at_validD) 1528 apply (clarsimp simp: cte_wp_at_ctes_of split: if_split) 1529 apply (rule cmap_relationE1 [OF cmap_relation_cte], assumption+, 1530 simp?, simp add: typ_heap_simps)+ 1531 apply (drule ccte_relation_ccap_relation)+ 1532 apply (auto simp: false_def true_def from_bool_def split: bool.splits)[1] 1533 apply (wp getCTE_wp') 1534 apply (clarsimp simp add: guard_is_UNIV_def Collect_const_mem false_def 1535 from_bool_0 true_def from_bool_def) 1536 apply vcg 1537 apply (rule conseqPre, vcg) 1538 apply clarsimp 1539 apply (clarsimp simp: Collect_const_mem) 1540 apply (frule(1) rf_sr_cte_at_validD, simp add: typ_heap_simps) 1541 apply (clarsimp simp: cte_wp_at_ctes_of) 1542 apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) 1543 apply (simp add: typ_heap_simps) 1544 apply (clarsimp simp add: ccte_relation_def map_option_Some_eq2) 1545 by (auto, 1546 auto dest!: ctes_of_valid' [OF _ invs_valid_objs'] 1547 elim!: valid_capAligned) 1548 1549lemmas cleanup_info_wf'_simps[simp] = cleanup_info_wf'_def[split_simps capability.split] 1550 1551lemma cteDeleteOne_ccorres: 1552 "ccorres dc xfdc 1553 (invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap 1554 \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) 1555 ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} 1556 \<inter> {s. slot_' s = Ptr slot}) [] 1557 (cteDeleteOne slot) (Call cteDeleteOne_'proc)" 1558 unfolding cteDeleteOne_def 1559 apply (rule ccorres_symb_exec_l' 1560 [OF _ getCTE_inv getCTE_sp empty_fail_getCTE]) 1561 apply (cinit' lift: slot_' cong: call_ignore_cong) 1562 apply (rule ccorres_move_c_guard_cte) 1563 apply csymbr 1564 apply (rule ccorres_abstract_cleanup) 1565 apply csymbr 1566 apply (rule ccorres_gen_asm2, 1567 erule_tac t="ret__unsigned_longlong = scast cap_null_cap" 1568 and s="cteCap cte = NullCap" 1569 in ssubst) 1570 apply (clarsimp simp only: when_def unless_def dc_def[symmetric]) 1571 apply (rule ccorres_cond2[where R=\<top>]) 1572 apply (clarsimp simp: Collect_const_mem) 1573 apply (rule ccorres_rhs_assoc)+ 1574 apply csymbr 1575 apply csymbr 1576 apply (rule ccorres_Guard_Seq) 1577 apply (rule ccorres_basic_srnoop) 1578 apply (ctac(no_vcg) add: isFinalCapability_ccorres[where slot=slot]) 1579 apply (rule_tac A="invs' and cte_wp_at' ((=) cte) slot" 1580 in ccorres_guard_imp2[where A'=UNIV]) 1581 apply (simp add: split_def dc_def[symmetric] 1582 del: Collect_const) 1583 apply (rule ccorres_move_c_guard_cte) 1584 apply (ctac(no_vcg) add: finaliseCap_True_standin_ccorres) 1585 apply (rule ccorres_assert) 1586 apply (simp add: dc_def[symmetric]) 1587 apply csymbr 1588 apply (ctac add: emptySlot_ccorres) 1589 apply (simp add: pred_conj_def finaliseCapTrue_standin_simple_def) 1590 apply (strengthen invs_mdb_strengthen' invs_urz) 1591 apply (wp typ_at_lifts isFinalCapability_inv 1592 | strengthen invs_valid_objs')+ 1593 apply (clarsimp simp: from_bool_def true_def irq_opt_relation_def 1594 invs_pspace_aligned' cte_wp_at_ctes_of) 1595 apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) 1596 apply (clarsimp simp: typ_heap_simps ccte_relation_ccap_relation ccap_relation_NullCap_iff) 1597 apply (wp isFinalCapability_inv) 1598 apply simp 1599 apply (simp del: Collect_const add: false_def) 1600 apply (rule ccorres_return_Skip) 1601 apply (clarsimp simp: Collect_const_mem cte_wp_at_ctes_of) 1602 apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) 1603 apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap 1604 dest!: ccte_relation_ccap_relation) 1605 apply (auto simp: o_def) 1606 done 1607 1608lemma getIRQSlot_ccorres_stuff: 1609 "\<lbrakk> (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> 1610 CTypesDefs.ptr_add (intStateIRQNode_' (globals s')) (uint (irq :: 8 word)) 1611 = Ptr (irq_node' s + 2 ^ cte_level_bits * ucast irq)" 1612 apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def 1613 cinterrupt_relation_def) 1614 apply (simp add: objBits_simps cte_level_bits_def 1615 size_of_def mult.commute mult.left_commute of_int_uint_ucast ) 1616 done 1617 1618lemma deletingIRQHandler_ccorres: 1619 "ccorres dc xfdc (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) 1620 (UNIV \<inter> {s. irq_opt_relation (Some irq) (irq_' s)}) [] 1621 (deletingIRQHandler irq) (Call deletingIRQHandler_'proc)" 1622 apply (cinit lift: irq_' cong: call_ignore_cong) 1623 apply (clarsimp simp: irq_opt_relation_def ptr_add_assertion_def dc_def[symmetric] 1624 cong: call_ignore_cong ) 1625 apply (rule_tac r'="\<lambda>rv rv'. rv' = Ptr rv" 1626 and xf'="slot_'" in ccorres_split_nothrow) 1627 apply (simp add: sint_ucast_eq_uint is_down) 1628 apply (rule ccorres_move_array_assertion_irq) 1629 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 1630 1631 apply (rule allI, rule conseqPre, vcg) 1632 apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def 1633 locateSlot_conv) 1634 apply (simp add: bind_def simpler_gets_def return_def 1635 ucast_nat_def uint_up_ucast is_up) 1636 apply (erule getIRQSlot_ccorres_stuff) 1637 apply ceqv 1638 apply (rule ccorres_symb_exec_l) 1639 apply (rule ccorres_symb_exec_l) 1640 apply (rule ccorres_symb_exec_r) 1641 apply (ctac add: cteDeleteOne_ccorres[where w="scast cap_notification_cap"]) 1642 apply vcg 1643 apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def 1644 gs_set_assn_Delete_cstate_relation[unfolded o_def]) 1645 apply (wp getCTE_wp' | simp add: getSlotCap_def getIRQSlot_def locateSlot_conv 1646 getInterruptState_def)+ 1647 apply vcg 1648 apply (clarsimp simp: cap_get_tag_isCap ghost_assertion_data_get_def 1649 ghost_assertion_data_set_def) 1650 apply (simp add: cap_tag_defs) 1651 apply (clarsimp simp: cte_wp_at_ctes_of Collect_const_mem 1652 irq_opt_relation_def Kernel_C.maxIRQ_def) 1653 apply (drule word_le_nat_alt[THEN iffD1]) 1654 apply (clarsimp simp:uint_0_iff unat_gt_0 uint_up_ucast is_up unat_def[symmetric]) 1655 done 1656 1657(* 6 = wordRadix, 1658 5 = tcb_cnode_radix + 1, 1659 7 = wordRadix+1*) 1660lemma Zombie_new_spec: 1661 "\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. type_' s = 64 \<or> type_' s < 63}) Call Zombie_new_'proc 1662 {s'. cap_zombie_cap_lift (ret__struct_cap_C_' s') = 1663 \<lparr> capZombieID_CL = \<^bsup>s\<^esup>ptr && ~~ mask (if \<^bsup>s\<^esup>type = (1 << 6) then 5 else unat (\<^bsup>s\<^esup>type + 1)) 1664 || \<^bsup>s\<^esup>number___unsigned_long && mask (if \<^bsup>s\<^esup>type = (1 << 6) then 5 else unat (\<^bsup>s\<^esup>type + 1)), 1665 capZombieType_CL = \<^bsup>s\<^esup>type && mask 7 \<rparr> 1666 \<and> cap_get_tag (ret__struct_cap_C_' s') = scast cap_zombie_cap}" 1667 apply vcg 1668 apply (clarsimp simp: word_sle_def) 1669 apply (simp add: mask_def word_log_esimps[where 'a=machine_word_len, simplified]) 1670 apply clarsimp thm Zombie_new_body_def 1671 apply (simp add: word_add_less_mono1[where k=1 and j="0x3F", simplified]) 1672 done 1673 1674lemma irq_opt_relation_Some_ucast: 1675 "\<lbrakk> x && mask 8 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: 8 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: machine_word) \<rbrakk> 1676 \<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast ((ucast x):: 8 word))" 1677 using ucast_ucast_mask[where x=x and 'a=8, symmetric] 1678 apply (simp add: irq_opt_relation_def) 1679 apply (rule conjI, clarsimp simp: irqInvalid_def Kernel_C.maxIRQ_def) 1680 apply (simp only: unat_arith_simps ) 1681 apply (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def) 1682 done 1683 1684lemmas upcast_ucast_id = Word_Lemmas.ucast_up_inj 1685 1686lemma irq_opt_relation_Some_ucast': 1687 "\<lbrakk> x && mask 8 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: 8 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: machine_word) \<rbrakk> 1688 \<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast x)" 1689 apply (rule_tac P = "%y. irq_opt_relation (Some (ucast x)) y" in subst[rotated]) 1690 apply (rule irq_opt_relation_Some_ucast[rotated]) 1691 apply simp+ 1692 done 1693 1694lemma ccap_relation_IRQHandler_mask: 1695 "\<lbrakk> ccap_relation acap ccap; isIRQHandlerCap acap \<rbrakk> 1696 \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 8 1697 = capIRQ_CL (cap_irq_handler_cap_lift ccap)" 1698 apply (simp only: cap_get_tag_isCap[symmetric]) 1699 apply (drule ccap_relation_c_valid_cap) 1700 apply (simp add: c_valid_cap_def cap_irq_handler_cap_lift cl_valid_cap_def) 1701 done 1702 1703lemma option_to_ctcb_ptr_not_0: 1704 "\<lbrakk> tcb_at' p s; option_to_ctcb_ptr v = tcb_ptr_to_ctcb_ptr p\<rbrakk> \<Longrightarrow> v = Some p" 1705 apply (clarsimp simp: option_to_ctcb_ptr_def tcb_ptr_to_ctcb_ptr_def 1706 split: option.splits) 1707 apply (frule tcb_aligned') 1708 apply (frule_tac y=ctcb_offset and n=tcbBlockSizeBits in aligned_offset_non_zero) 1709 apply (clarsimp simp: ctcb_offset_defs objBits_defs)+ 1710 done 1711 1712lemma update_tcb_map_to_tcb: 1713 "map_to_tcbs (ksPSpace s(p \<mapsto> KOTCB tcb)) 1714 = (map_to_tcbs (ksPSpace s))(p \<mapsto> tcb)" 1715 by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split) 1716 1717lemma ep_queue_relation_shift2: 1718 "(option_map2 tcbEPNext_C (f (cslift s)) 1719 = option_map2 tcbEPNext_C (cslift s) 1720 \<and> option_map2 tcbEPPrev_C (f (cslift s)) 1721 = option_map2 tcbEPPrev_C (cslift s)) 1722 \<Longrightarrow> ep_queue_relation (f (cslift s)) ts qPrev qHead 1723 = ep_queue_relation (cslift s) ts qPrev qHead" 1724 apply clarsimp 1725 apply (induct ts arbitrary: qPrev qHead) 1726 apply simp 1727 apply simp 1728 apply (simp add: option_map2_def fun_eq_iff 1729 map_option_case) 1730 apply (drule_tac x=qHead in spec)+ 1731 apply (clarsimp split: option.split_asm) 1732 done 1733 1734lemma sched_queue_relation_shift: 1735 "(option_map2 tcbSchedNext_C (f (cslift s)) 1736 = option_map2 tcbSchedNext_C (cslift s) 1737 \<and> option_map2 tcbSchedPrev_C (f (cslift s)) 1738 = option_map2 tcbSchedPrev_C (cslift s)) 1739 \<Longrightarrow> sched_queue_relation (f (cslift s)) ts qPrev qHead 1740 = sched_queue_relation (cslift s) ts qPrev qHead" 1741 apply clarsimp 1742 apply (induct ts arbitrary: qPrev qHead) 1743 apply simp 1744 apply simp 1745 apply (simp add: option_map2_def fun_eq_iff 1746 map_option_case) 1747 apply (drule_tac x=qHead in spec)+ 1748 apply (clarsimp split: option.split_asm) 1749 done 1750 1751lemma cendpoint_relation_udpate_arch: 1752 "\<lbrakk> cslift x p = Some tcb ; cendpoint_relation (cslift x) v v' \<rbrakk> 1753 \<Longrightarrow> cendpoint_relation (cslift x(p \<mapsto> tcbArch_C_update f tcb)) v v'" 1754 apply (clarsimp simp: cendpoint_relation_def Let_def tcb_queue_relation'_def 1755 split: endpoint.splits) 1756 apply (subst ep_queue_relation_shift2; simp add: fun_eq_iff) 1757 apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case) 1758 apply (subst ep_queue_relation_shift2; simp add: fun_eq_iff) 1759 apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case) 1760 done 1761 1762lemma cnotification_relation_udpate_arch: 1763 "\<lbrakk> cslift x p = Some tcb ; cnotification_relation (cslift x) v v' \<rbrakk> 1764 \<Longrightarrow> cnotification_relation (cslift x(p \<mapsto> tcbArch_C_update f tcb)) v v'" 1765 apply (clarsimp simp: cnotification_relation_def Let_def tcb_queue_relation'_def 1766 split: notification.splits ntfn.splits) 1767 apply (subst ep_queue_relation_shift2; simp add: fun_eq_iff) 1768 apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case) 1769 done 1770 1771(* 1772lemmas Kernel_C_reg_simps = Kernel_C.E_def Kernel_C.R1_def Kernel_C.CPSR_def 1773 Kernel_C.R2_def Kernel_C.R3_def Kernel_C.R4_def Kernel_C.R5_def Kernel_C.R6_def Kernel_C.R7_def 1774 Kernel_C.R8_def Kernel_C.R9_def Kernel_C.R10_def Kernel_C.R11_def Kernel_C.R12_def Kernel_C.SP_def 1775 Kernel_C.LR_def Kernel_C.FaultInstruction_def Kernel_C.TPIDRURW_def Kernel_C.LR_svc_def 1776*) 1777lemma sanitiseSetRegister_ccorres: 1778 "\<lbrakk> val = val'; reg' = register_from_H reg\<rbrakk> \<Longrightarrow> 1779 ccorres dc xfdc (tcb_at' tptr) 1780 UNIV 1781 hs 1782 (asUser tptr (setRegister reg (local.sanitiseRegister False reg val))) 1783 (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister(reg',val',0);; 1784 CALL setRegister(tcb_ptr_to_ctcb_ptr tptr,reg',\<acute>unsigned_long_eret_2))" 1785 apply (rule ccorres_guard_imp2) 1786 apply (rule ccorres_symb_exec_r) 1787 apply (ctac add: setRegister_ccorres) 1788 apply (vcg) 1789 apply (rule conseqPre, vcg) 1790 apply (fastforce simp: sanitiseRegister_def split: register.splits) 1791 by (auto simp: sanitiseRegister_def from_bool_def simp del: Collect_const split: register.splits bool.splits) 1792 1793lemma case_option_both[simp]: 1794 "(case f of None \<Rightarrow> P | _ \<Rightarrow> P) = P" 1795 by (auto split: option.splits) 1796 1797lemma flushPD_ccorres: 1798 "ccorres dc xfdc 1799 \<top> (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vspace_' s = pml4e_Ptr vs}) hs 1800 (flushPD vs asid) 1801 (Call flushPD_'proc)" 1802 apply (cinit lift: asid_' vspace_' simp: flushAll_def) 1803 apply (ctac add: invalidateASID_ccorres) 1804 by clarsimp 1805 1806lemma flushPDPT_ccorres: 1807 "ccorres dc xfdc 1808 \<top> (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vspace_' s = pml4e_Ptr vs}) hs 1809 (flushPDPT vs asid) 1810 (Call flushPDPT_'proc)" 1811 apply (cinit lift: asid_' vspace_' simp: flushAll_def) 1812 apply (rule ccorres_add_return2) 1813 apply (ctac (no_vcg) add: invalidateASID_ccorres) 1814 apply (rule ccorres_return_void_C) 1815 apply wp 1816 by clarsimp 1817 1818lemma unmapPageDirectory_ccorres: 1819 "ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < pptrBase)) 1820 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vaddr___unsigned_long_' s = vaddr} \<inter> {s. pd_' s = Ptr pdPtr}) 1821 [] (unmapPageDirectory asid vaddr pdPtr) (Call unmapPageDirectory_'proc)" 1822 apply (rule ccorres_gen_asm) 1823 apply (cinit lift: asid_' vaddr___unsigned_long_' pd_') 1824 apply (clarsimp simp add: ignoreFailure_liftM) 1825 apply (ctac add: findVSpaceForASID_ccorres,rename_tac vspace find_ret) 1826 apply clarsimp 1827 apply (ctac add: lookupPDPTSlot_ccorres, rename_tac pdptSlot lu_ret) 1828 apply (clarsimp simp add: pde_pde_pt_def liftE_bindE) 1829 apply (rule ccorres_rhs_assoc2) 1830 apply (rule ccorres_rhs_assoc2) 1831 apply (rule ccorres_rhs_assoc2) 1832 apply (rule ccorres_pre_getObject_pdpte) 1833 apply (simp only: pdpte_case_isPageDirectoryPDPTE) 1834 apply (rule_tac xf'=ret__int_' 1835 and R'=UNIV 1836 and val="from_bool (isPageDirectoryPDPTE pdpte \<and> pdpteTable pdpte = addrFromPPtr pdPtr)" 1837 and R="ko_at' pdpte pdptSlot" 1838 in ccorres_symb_exec_r_known_rv_UNIV) 1839 apply vcg 1840 apply clarsimp 1841 apply (erule cmap_relationE1[OF rf_sr_cpdpte_relation]) 1842 apply (erule ko_at_projectKO_opt) 1843 apply (rename_tac pdpte_C) 1844 apply (clarsimp simp: typ_heap_simps) 1845 apply (rule conjI, clarsimp simp: pdpte_pdpte_pd_def) 1846 apply (drule pdpte_lift_pdpte_pd[simplified pdpte_pdpte_pd_def, simplified]) 1847 apply (clarsimp simp: from_bool_def cpdpte_relation_def Let_def isPageDirectoryPDPTE_def 1848 pdpte_pdpte_pd_lift_def case_bool_If 1849 split: pdpte.split_asm) 1850 apply clarsimp 1851 apply (simp add: from_bool_def split:bool.splits) 1852 apply (rule strenghten_False_imp) 1853 apply (simp add: cpdpte_relation_def Let_def) 1854 apply (subgoal_tac "pdpte_get_tag pdpte_C = 1") 1855 apply (clarsimp dest!: pdpte_lift_pdpte_1g[simplified pdpte_pdpte_1g_def, simplified] 1856 simp: isPageDirectoryPDPTE_def split: pdpte.splits) 1857 apply (clarsimp simp: pdpte_get_tag_def word_and_1 pdpte_pdpte_pd_def split: if_splits) 1858 apply ceqv 1859 apply (rule ccorres_Cond_rhs_Seq) 1860 apply (simp add: from_bool_0) 1861 apply ccorres_rewrite 1862 apply (clarsimp simp: throwError_def) 1863 apply (rule ccorres_return_void_C[simplified dc_def]) 1864 apply (simp add: from_bool_0) 1865 apply (rule ccorres_liftE[simplified dc_def]) 1866 apply (ctac add: flushPD_ccorres) 1867 apply (csymbr, rename_tac invalidPDPTE) 1868 apply (rule ccorres_split_nothrow_novcg_dc) 1869 apply (rule storePDPTE_Basic_ccorres) 1870 apply (simp add: cpdpte_relation_def Let_def) 1871 apply (csymbr, rename_tac root) 1872 apply (ctac add: invalidatePageStructureCacheASID_ccorres[simplified dc_def]) 1873 apply wp 1874 apply (clarsimp simp add: guard_is_UNIV_def) 1875 apply wp 1876 apply clarsimp 1877 apply (vcg exspec=flushPD_modifies) 1878 apply (clarsimp simp: guard_is_UNIV_def) 1879 apply (simp,ccorres_rewrite,simp add:throwError_def) 1880 apply (rule ccorres_return_void_C[simplified dc_def]) 1881 apply wpsimp 1882 apply (vcg exspec=lookupPDPTSlot_modifies) 1883 apply (simp,ccorres_rewrite,simp add:throwError_def) 1884 apply (rule ccorres_return_void_C[simplified dc_def]) 1885 apply wp 1886 apply vcg 1887 apply (auto simp add: asid_wf_def mask_def) 1888 done 1889 1890lemma unmapPDPointerTable_ccorres: 1891 "ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < pptrBase)) 1892 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vaddr___unsigned_long_' s = vaddr} \<inter> {s. pdpt_' s = Ptr pdptPtr}) 1893 [] (unmapPDPT asid vaddr pdptPtr) (Call unmapPDPT_'proc)" 1894 supply Collect_const[simp del] 1895 apply (rule ccorres_gen_asm) 1896 apply (cinit lift: asid_' vaddr___unsigned_long_' pdpt_') 1897 apply (clarsimp simp add: ignoreFailure_liftM) 1898 apply (ctac add: findVSpaceForASID_ccorres, rename_tac vspace find_ret) 1899 apply (rule_tac P="page_map_l4_at' vspace" in ccorres_cross_over_guard) 1900 apply (simp add: liftE_bindE) 1901 apply (rule ccorres_pre_getObject_pml4e, rename_tac pml4e) 1902 apply ccorres_rewrite 1903 apply (rule ccorres_rhs_assoc2) 1904 apply (rule ccorres_rhs_assoc2) 1905 apply (rule ccorres_rhs_assoc2) 1906 apply (rule_tac xf'=ret__int_' and 1907 R'=UNIV and 1908 val="from_bool (isPDPointerTablePML4E pml4e \<and> pml4eTable pml4e = addrFromPPtr pdptPtr)" and 1909 R="ko_at' pml4e (lookup_pml4_slot vspace vaddr) and page_map_l4_at' vspace" 1910 in ccorres_symb_exec_r_known_rv) 1911 apply vcg 1912 apply clarsimp 1913 apply (clarsimp simp: page_map_l4_at'_array_assertion) 1914 apply (erule cmap_relationE1[OF rf_sr_cpml4e_relation]) 1915 apply (erule ko_at_projectKO_opt) 1916 apply (rename_tac pml4e_C) 1917 apply (fastforce simp: typ_heap_simps cpml4e_relation_def Let_def 1918 isPDPointerTablePML4E_def from_bool_def 1919 split: bool.splits if_split pml4e.split_asm) 1920 apply ceqv 1921 apply (rule ccorres_Cond_rhs_Seq) 1922 apply ccorres_rewrite 1923 apply (clarsimp simp: from_bool_0 isPDPointerTablePML4E_def split: pml4e.splits; 1924 clarsimp simp: throwError_def; 1925 rule ccorres_return_void_C[simplified dc_def]) 1926 apply (clarsimp simp: isPDPointerTablePML4E_def liftE_def bind_assoc split: pml4e.split_asm) 1927 apply (ctac add: flushPDPT_ccorres) 1928 apply csymbr 1929 apply (rule ccorres_seq_skip'[THEN iffD1]) 1930 apply (rule ccorres_split_nothrow_novcg_dc) 1931 apply (rule storePML4E_Basic_ccorres') 1932 apply (fastforce simp: cpml4e_relation_def) 1933 apply (rule ccorres_return_Skip[simplified dc_def]) 1934 apply wp 1935 apply (fastforce simp: guard_is_UNIV_def) 1936 apply wp 1937 apply (vcg exspec=flushPDPT_modifies) 1938 apply vcg 1939 apply ccorres_rewrite 1940 apply (clarsimp simp: throwError_def) 1941 apply (rule ccorres_return_void_C[simplified dc_def]) 1942 apply (wpsimp wp: hoare_drop_imps) 1943 apply (vcg exspec=findVSpaceForASID_modifies) 1944 apply (auto simp: invs_arch_state' invs_no_0_obj' asid_wf_def mask_def typ_heap_simps 1945 intro: page_map_l4_at'_array_assertion) 1946 done 1947 1948lemma ccap_relation_PDPT_IsMapped: 1949 "ccap_relation (ArchObjectCap (PDPointerTableCap x1 x2)) cap \<Longrightarrow> 1950 capPDPTIsMapped_CL (cap_pdpt_cap_lift cap) = from_bool (\<not> Option.is_none x2)" 1951 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1952 apply (clarsimp simp: ccap_relation_def cap_to_H_def cap_pdpt_cap_lift_def cap_lift_def Let_def 1953 cap_tag_defs to_bool_def true_def false_def 1954 split: if_split) 1955 apply word_bitwise 1956 done 1957 1958lemma ccap_relation_PML4_IsMapped: 1959 "ccap_relation (ArchObjectCap (PML4Cap x1 x2)) cap \<Longrightarrow> 1960 capPML4IsMapped_CL (cap_pml4_cap_lift cap) = from_bool (\<not> Option.is_none x2)" 1961 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1962 apply (clarsimp simp: ccap_relation_def cap_to_H_def cap_pml4_cap_lift_def cap_lift_def Let_def 1963 cap_tag_defs to_bool_def true_def false_def 1964 split: if_split) 1965 apply word_bitwise 1966 done 1967 1968lemma if_case_opt_same_branches: 1969 "cond \<longrightarrow> Option.is_none opt \<Longrightarrow> 1970 (if cond then 1971 case opt of 1972 None \<Rightarrow> f 1973 | Some x \<Rightarrow> g x 1974 else f) = f" 1975 by (cases cond; cases opt; clarsimp) 1976 1977method return_NullCap_pair_ccorres = 1978 solves \<open>((rule ccorres_rhs_assoc2)+), (rule ccorres_from_vcg_throws), 1979 (rule allI, rule conseqPre, vcg), (clarsimp simp: return_def ccap_relation_NullCap_iff)\<close> 1980 1981lemma Mode_finaliseCap_ccorres_pdpt: 1982 "cp = PDPointerTableCap x1 x2 \<Longrightarrow> 1983 ccorres 1984 (\<lambda>rv rv'. ccap_relation (fst rv) (remainder_C rv') \<and> 1985 ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 1986 ret__struct_finaliseCap_ret_C_' 1987 (invs' and 1988 valid_cap' (ArchObjectCap cp) and 1989 (\<lambda>s. 2 ^ acapBits cp \<le> gsMaxObjectSize s)) 1990 (UNIV \<inter> \<lbrace>ccap_relation (ArchObjectCap cp) \<acute>cap\<rbrace> 1991 \<inter> \<lbrace>\<acute>final = from_bool is_final\<rbrace>) 1992 hs 1993 (if is_final then 1994 case x2 of 1995 None \<Rightarrow> return (NullCap, NullCap) 1996 | Some (a, b) \<Rightarrow> do _ <- unmapPDPT a b x1; 1997 return (NullCap, NullCap) 1998 od 1999 else 2000 return (NullCap, NullCap)) 2001 (Call Mode_finaliseCap_'proc)" 2002 (is "_ \<Longrightarrow> ccorres _ _ ?abstract_pre ?c_pre _ _ _") 2003 supply Collect_const[simp del] 2004 apply (cinit' lift: cap_' final_') 2005 apply csymbr 2006 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs) 2007 apply ccorres_rewrite 2008 apply (rule ccorres_rhs_assoc) 2009 apply (rule_tac val="from_bool (is_final \<and> \<not> Option.is_none x2)" and 2010 xf'=ret__int_' and 2011 R=\<top> and 2012 R'=UNIV 2013 in ccorres_symb_exec_r_known_rv_UNIV) 2014 apply (vcg exspec=unmapPDPT_modifies) 2015 apply (fastforce simp: false_def cap_get_tag_isCap_unfolded_H_cap 2016 ccap_relation_PDPT_IsMapped from_bool_eq_if') 2017 apply ceqv 2018 apply (rule ccorres_Cond_rhs_Seq) 2019 apply (clarsimp simp: Option.is_none_def) 2020 apply (rule ccorres_rhs_assoc)+ 2021 apply csymbr 2022 apply csymbr 2023 apply csymbr 2024 (* Guard imp needed to deal with the variables introduced by x2 = Some (a, b) *) 2025 apply (rule ccorres_guard_imp[where A="?abstract_pre" and A'=UNIV]) 2026 apply (ctac add: unmapPDPointerTable_ccorres) 2027 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2028 apply return_NullCap_pair_ccorres 2029 apply wp 2030 apply (vcg exspec=unmapPDPT_modifies) 2031 apply (fastforce simp: valid_cap_simps' asid_wf_def mask_def) 2032 apply (fastforce elim!: ccap_relationE 2033 simp: cap_to_H_def cap_pdpt_cap_lift_def cap_get_tag_isCap_unfolded_H_cap 2034 c_valid_cap_def valid_cap_simps' Let_def 2035 split: cap_CL.splits if_split_asm) 2036 apply (clarsimp simp: if_case_opt_same_branches) 2037 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2038 apply return_NullCap_pair_ccorres 2039 apply (fastforce simp: guard_is_UNIV_def cap_get_tag_isCap_unfolded_H_cap)+ 2040 done 2041 2042(* Proof of this lemma is very similar to Mode_finaliseCap_ccorres_pdpt above *) 2043lemma Mode_finaliseCap_ccorres_pml4: 2044 "cp = PML4Cap x1 x2 \<Longrightarrow> 2045 ccorres 2046 (\<lambda>rv rv'. ccap_relation (fst rv) (remainder_C rv') \<and> 2047 ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 2048 ret__struct_finaliseCap_ret_C_' 2049 (invs' and 2050 valid_cap' (ArchObjectCap cp) and 2051 (\<lambda>s. 2 ^ acapBits cp \<le> gsMaxObjectSize s)) 2052 (UNIV \<inter> \<lbrace>ccap_relation (ArchObjectCap cp) \<acute>cap\<rbrace> 2053 \<inter> \<lbrace>\<acute>final = from_bool is_final\<rbrace>) 2054 hs 2055 (if is_final then 2056 case x2 of 2057 None \<Rightarrow> return (NullCap, NullCap) 2058 | Some asid \<Rightarrow> do _ <- deleteASID asid x1; 2059 return (NullCap, NullCap) 2060 od 2061 else 2062 return (NullCap, NullCap)) 2063 (Call Mode_finaliseCap_'proc)" 2064 (is "_ \<Longrightarrow> ccorres _ _ ?abstract_pre ?c_pre _ _ _") 2065 supply Collect_const[simp del] 2066 apply (cinit' lift: cap_' final_') 2067 apply csymbr 2068 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs) 2069 apply ccorres_rewrite 2070 apply (rule ccorres_rhs_assoc) 2071 apply (rule_tac val="from_bool (is_final \<and> \<not> Option.is_none x2)" and 2072 xf'=ret__int_' and 2073 R=\<top> and 2074 R'=UNIV 2075 in ccorres_symb_exec_r_known_rv_UNIV) 2076 apply vcg 2077 apply (fastforce simp: false_def cap_get_tag_isCap_unfolded_H_cap 2078 ccap_relation_PML4_IsMapped from_bool_eq_if') 2079 apply ceqv 2080 apply (rule ccorres_Cond_rhs_Seq) 2081 apply (clarsimp simp: Option.is_none_def) 2082 apply (rule ccorres_rhs_assoc)+ 2083 apply csymbr 2084 apply csymbr 2085 (* Guard imp needed to deal with the variables introduced by x2 = Some y *) 2086 apply (rule ccorres_guard_imp[where A="?abstract_pre" and A'=UNIV]) 2087 apply (ctac add: deleteASID_ccorres) 2088 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2089 apply return_NullCap_pair_ccorres 2090 apply wp 2091 apply (vcg exspec=deleteASID_modifies) 2092 apply (fastforce simp: valid_cap_simps' asid_wf_def asid_bits_def word_le_make_less) 2093 apply (fastforce elim!: ccap_relationE 2094 simp: cap_to_H_def cap_pml4_cap_lift_def cap_get_tag_isCap_unfolded_H_cap 2095 c_valid_cap_def valid_cap_simps' Let_def 2096 split: cap_CL.splits if_split_asm) 2097 apply (clarsimp simp: if_case_opt_same_branches) 2098 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2099 apply return_NullCap_pair_ccorres 2100 apply (fastforce simp: guard_is_UNIV_def cap_get_tag_isCap_unfolded_H_cap)+ 2101 done 2102 2103lemma ccap_relation_capFMappedASID_CL_0: 2104 "ccap_relation (ArchObjectCap (PageCap x0 x1 x2 x3 x4 None)) cap \<Longrightarrow> 2105 capFMappedASID_CL (cap_frame_cap_lift cap) = 0" 2106 apply (clarsimp simp: ccap_relation_def cap_frame_cap_lift_def) 2107 apply (case_tac "cap_lift cap") 2108 apply (fastforce simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm)+ 2109 done 2110 2111lemma Mode_finaliseCap_ccorres_page_cap: 2112 "cp = PageCap x0 x1 x2 x3 x4 x5 \<Longrightarrow> 2113 ccorres 2114 (\<lambda>rv rv'. 2115 ccap_relation (fst rv) (remainder_C rv') \<and> 2116 ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 2117 ret__struct_finaliseCap_ret_C_' 2118 (invs' and 2119 valid_cap' (ArchObjectCap cp) and 2120 (\<lambda>s. 2 ^ pageBitsForSize x3 \<le> gsMaxObjectSize s)) 2121 (UNIV \<inter> \<lbrace>ccap_relation (ArchObjectCap cp) \<acute>cap\<rbrace>) 2122 hs 2123 (case x5 of 2124 None \<Rightarrow> return (NullCap, NullCap) 2125 | Some (asid, ptr) \<Rightarrow> do _ <- unmapPage x3 asid ptr x0; 2126 return (NullCap, NullCap) 2127 od) 2128 (Call Mode_finaliseCap_'proc)" 2129 supply Collect_const[simp del] 2130 apply (cinit' lift: cap_' simp: false_def) 2131 apply csymbr 2132 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs) 2133 apply ccorres_rewrite 2134 apply (rule ccorres_rhs_assoc) 2135 apply csymbr 2136 apply wpc 2137 apply (clarsimp simp: ccap_relation_capFMappedASID_CL_0) 2138 apply ccorres_rewrite 2139 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2140 apply return_NullCap_pair_ccorres 2141 apply clarsimp 2142 apply (rule ccorres_cond_true_seq) 2143 apply (rule ccorres_rhs_assoc) 2144 apply csymbr 2145 apply (rule ccorres_cond_true_seq) 2146 apply (rule ccorres_rhs_assoc)+ 2147 apply csymbr 2148 apply csymbr 2149 apply csymbr 2150 apply csymbr 2151 apply wpfix 2152 apply (ctac add: unmapPage_ccorres) 2153 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2154 apply return_NullCap_pair_ccorres 2155 apply wp 2156 apply (vcg exspec=unmapPage_modifies) 2157 by (clarsimp elim!: ccap_relationE 2158 simp: cap_to_H_def cap_frame_cap_lift_def cap_get_tag_isCap_unfolded_H_cap 2159 c_valid_cap_def cl_valid_cap_def valid_cap_simps' 2160 maptype_to_H_def vm_page_map_type_defs Let_def 2161 split: cap_CL.splits if_split_asm 2162 dest!: x_less_2_0_1) 2163 2164lemma Arch_finaliseCap_ccorres: 2165 notes dc_simp[simp del] Collect_const[simp del] 2166 shows 2167 "ccorres (\<lambda>rv rv'. ccap_relation (fst rv) (remainder_C rv') \<and> 2168 ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 2169 ret__struct_finaliseCap_ret_C_' 2170 (invs' and valid_cap' (ArchObjectCap cp) 2171 and (\<lambda>s. 2 ^ acapBits cp \<le> gsMaxObjectSize s)) 2172 (UNIV \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)} 2173 \<inter> {s. final_' s = from_bool is_final}) [] 2174 (Arch.finaliseCap cp is_final) (Call Arch_finaliseCap_'proc)" 2175 (is "ccorres _ _ ?abstract_pre ?c_pre _ _ _") 2176 apply (cinit lift: cap_' final_' cong: call_ignore_cong) 2177 apply csymbr 2178 apply (simp add: X64_H.finaliseCap_def cap_get_tag_isCap_ArchObject) 2179 apply (rule ccorres_cases[where P=is_final]; clarsimp cong: arch_capability.case_cong) 2180 prefer 2 2181 apply (subgoal_tac "isPageCap cp \<longrightarrow> \<not> isPageTableCap cp \<and> \<not> isASIDPoolCap cp \<and> \<not> isIOPortCap cp \<and> \<not> isPageDirectoryCap cp \<and> \<not> isASIDControlCap cp \<and> \<not> isIOPortControlCap cp") 2182 apply (rule ccorres_cases[where P="isPageCap cp"]; clarsimp) 2183 prefer 2 2184 apply (rule ccorres_inst[where P="?abstract_pre" and P'=UNIV]) 2185 apply (cases cp; clarsimp simp: isCap_simps; ccorres_rewrite) 2186 apply return_NullCap_pair_ccorres (* ASIDPoolCap *) 2187 apply return_NullCap_pair_ccorres (* ASIDControlCap *) 2188 apply return_NullCap_pair_ccorres (* IOPortCap *) 2189 apply return_NullCap_pair_ccorres (* IOPortControlCap *) 2190 \<comment> \<open>PageTableCap\<close> 2191 apply (subst ccorres_cond_seq2_seq[symmetric]) 2192 apply (rule ccorres_guard_imp) 2193 apply (rule ccorres_rhs_assoc) 2194 apply csymbr 2195 apply clarsimp 2196 apply ccorres_rewrite 2197 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2198 apply (return_NullCap_pair_ccorres, simp+) 2199 \<comment> \<open>PageDirectoryCap\<close> 2200 apply (subst ccorres_cond_seq2_seq[symmetric]) 2201 apply (rule ccorres_guard_imp) 2202 apply (rule ccorres_rhs_assoc) 2203 apply csymbr 2204 apply clarsimp 2205 apply ccorres_rewrite 2206 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2207 apply (return_NullCap_pair_ccorres, simp+) 2208 \<comment> \<open>PDPointerTableCap\<close> 2209 apply (rule ccorres_guard_imp) 2210 apply (rule ccorres_add_return2) 2211 apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_pdpt[where is_final=False, simplified if_False]) 2212 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2213 apply (rule allI, rule conseqPre, vcg) 2214 apply (clarsimp simp: return_def) 2215 apply wp 2216 apply fastforce 2217 apply (fastforce simp: false_def) 2218 \<comment> \<open>PML4Cap\<close> 2219 apply (rule ccorres_guard_imp) 2220 apply (rule ccorres_add_return2) 2221 apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_pml4[where is_final=False, simplified if_False]) 2222 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2223 apply (rule allI, rule conseqPre, vcg) 2224 apply (clarsimp simp: return_def) 2225 apply wp 2226 apply fastforce 2227 apply (fastforce simp: false_def) 2228 \<comment> \<open>PageCap\<close> 2229 apply (clarsimp simp: isCap_simps) 2230 apply (rule ccorres_guard_imp[where A="?abstract_pre" and A'=UNIV]) 2231 apply ccorres_rewrite 2232 apply (rule ccorres_add_return2) 2233 apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_page_cap) 2234 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2235 apply (rule allI, rule conseqPre, vcg) 2236 apply (fastforce simp: return_def) 2237 apply wp 2238 apply fastforce 2239 apply fastforce 2240 apply (fastforce simp: isCap_simps) 2241 apply ccorres_rewrite 2242 apply (rule ccorres_Cond_rhs_Seq) 2243 \<comment> \<open>final \<and> PageDirectoryCap\<close> 2244 apply (clarsimp simp: isCap_simps) 2245 apply (rule ccorres_rhs_assoc)+ 2246 apply csymbr 2247 apply ccorres_rewrite 2248 apply (rule ccorres_rhs_assoc)+ 2249 apply csymbr 2250 apply csymbr 2251 apply clarsimp 2252 apply (rule ccorres_Cond_rhs_Seq) 2253 apply (subgoal_tac "capPDMappedAddress cp \<noteq> None") 2254 prefer 2 2255 apply (clarsimp simp add: isCap_simps) 2256 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2257 apply (frule cap_lift_page_directory_cap) 2258 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 2259 to_bool_def cap_page_directory_cap_lift_def 2260 asid_bits_def 2261 split: if_split_asm) 2262 apply clarsimp 2263 apply (rule ccorres_rhs_assoc)+ 2264 apply csymbr 2265 apply csymbr 2266 apply csymbr 2267 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2268 apply (subst (asm) ccap_relation_def) 2269 apply (clarsimp simp: cap_page_directory_cap_lift cap_to_H_def split: if_splits) 2270 apply (ctac (no_vcg) add: unmapPageDirectory_ccorres) 2271 apply (rule ccorres_inst[where P=\<top> and P'=UNIV], return_NullCap_pair_ccorres) 2272 apply (rule wp_post_taut) 2273 apply (subgoal_tac "capPDMappedAddress cp = None") 2274 prefer 2 2275 apply (clarsimp simp add: isCap_simps) 2276 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2277 apply (frule cap_lift_page_directory_cap) 2278 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 2279 to_bool_def cap_page_directory_cap_lift_def 2280 asid_bits_def 2281 split: if_split_asm) 2282 apply simp 2283 apply (rule ccorres_inst[where P=\<top> and P'=UNIV], return_NullCap_pair_ccorres) 2284 \<comment> \<open>final \<and> PageTableCap\<close> 2285 apply (rule ccorres_Cond_rhs_Seq) 2286 apply (clarsimp simp: isCap_simps) 2287 apply (rule ccorres_rhs_assoc)+ 2288 apply csymbr 2289 apply ccorres_rewrite 2290 apply (rule ccorres_rhs_assoc)+ 2291 apply csymbr 2292 apply csymbr 2293 apply clarsimp 2294 apply (rule ccorres_Cond_rhs_Seq) 2295 apply (subgoal_tac "capPTMappedAddress cp \<noteq> None") 2296 prefer 2 2297 apply (clarsimp simp add: isCap_simps) 2298 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2299 apply (frule cap_lift_page_table_cap) 2300 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 2301 to_bool_def cap_page_table_cap_lift_def 2302 asid_bits_def 2303 split: if_split_asm) 2304 apply clarsimp 2305 apply (rule ccorres_rhs_assoc)+ 2306 apply csymbr 2307 apply csymbr 2308 apply csymbr 2309 apply (simp add: split_def) 2310 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2311 apply (subst (asm) ccap_relation_def) 2312 apply (clarsimp simp: cap_page_table_cap_lift cap_to_H_def split: if_splits) 2313 apply (ctac (no_vcg) add: unmapPageTable_ccorres) 2314 apply (rule ccorres_inst[where P=\<top> and P'=UNIV], return_NullCap_pair_ccorres) 2315 apply (rule wp_post_taut) 2316 apply clarsimp 2317 apply (subgoal_tac "capPTMappedAddress cp = None") 2318 prefer 2 2319 apply (clarsimp simp add: isCap_simps) 2320 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2321 apply (frule cap_lift_page_table_cap) 2322 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 2323 to_bool_def cap_page_table_cap_lift_def 2324 asid_bits_def 2325 split: if_split_asm) 2326 apply simp 2327 apply (rule ccorres_inst[where P=\<top> and P'=UNIV], return_NullCap_pair_ccorres) 2328 \<comment> \<open>final \<and> ASIDPoolCap\<close> 2329 apply (rule ccorres_Cond_rhs_Seq) 2330 apply (clarsimp simp: isCap_simps) 2331 apply (rule ccorres_rhs_assoc)+ 2332 apply csymbr 2333 apply csymbr 2334 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2335 apply (subst (asm) ccap_relation_def) 2336 apply (clarsimp simp: cap_asid_pool_cap_lift cap_to_H_def split: if_splits) 2337 apply (ctac (no_vcg) add: deleteASIDPool_ccorres) 2338 apply (rule ccorres_inst[where P=\<top> and P'=UNIV], return_NullCap_pair_ccorres) 2339 apply (rule wp_post_taut) 2340 \<comment> \<open>final \<and> (ASIDControlCap \<or> IOPortControlCap\<close> 2341 apply (rule ccorres_Cond_rhs_Seq) 2342 apply (clarsimp simp: isCap_simps) 2343 apply (erule disjE; ccorres_rewrite; clarsimp; (rule ccorres_inst[where P=\<top> and P'=UNIV], return_NullCap_pair_ccorres)) 2344 \<comment> \<open>final \<and> IOPortCap\<close> 2345 apply (rule ccorres_Cond_rhs_Seq) 2346 apply (clarsimp simp: isCap_simps) 2347 apply ccorres_rewrite 2348 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2349 apply (rule allI, rule conseqPre, vcg) 2350 apply (clarsimp simp: return_def ccap_relation_NullCap_iff) 2351 \<comment> \<open>Mode_finaliseCap\<close> 2352 apply ccorres_rewrite 2353 (* Winnow out the irrelevant cases *) 2354 apply (wpc; (rule ccorres_inst[where P=\<top> and P'=UNIV], fastforce simp: isCap_simps)?) 2355 \<comment> \<open>PageCap\<close> 2356 apply clarsimp 2357 apply (rule ccorres_add_return2) 2358 apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_page_cap) 2359 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2360 apply (rule allI, rule conseqPre, vcg) 2361 apply (fastforce simp: return_def) 2362 apply wp 2363 \<comment> \<open>PDPointerTableCap\<close> 2364 apply (rule ccorres_add_return2) 2365 apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_pdpt[where is_final=True, simplified if_True]) 2366 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2367 apply (rule allI, rule conseqPre, vcg) 2368 apply (fastforce simp: return_def) 2369 apply wp 2370 \<comment> \<open>PML4Cap\<close> 2371 apply (rule ccorres_add_return2) 2372 apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_pml4[where is_final=True, simplified if_True]) 2373 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2374 apply (rule allI, rule conseqPre, vcg) 2375 apply (fastforce simp: return_def) 2376 apply wp 2377 by (auto elim: ccap_relationE 2378 simp: cap_to_H_def cap_get_tag_isCap_unfolded_H_cap 2379 cap_page_table_cap_lift_def cap_asid_pool_cap_lift_def 2380 cap_page_directory_cap_lift_def cap_frame_cap_lift_def 2381 c_valid_cap_def cl_valid_cap_def valid_cap_simps' 2382 asid_wf_def mask_def to_bool_def asid_bits_def word_le_make_less 2383 Let_def isCap_simps cap_get_tag_isCap_ArchObject 2384 split: cap_CL.splits if_split_asm) 2385 2386lemma fpuThreadDelete_ccorres: 2387 "ccorres dc xfdc 2388 (invs' and tcb_at' thread) 2389 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) hs 2390 (fpuThreadDelete thread) (Call fpuThreadDelete_'proc)" 2391 supply Collect_const[simp del] dc_simp[simp del] 2392 apply (cinit lift: thread_') 2393 apply clarsimp 2394 apply (ctac (no_vcg) add: nativeThreadUsingFPU_ccorres) 2395 apply clarsimp 2396 apply (rule ccorres_when[where R=\<top>]) 2397 apply fastforce 2398 apply (ctac add: switchFpuOwner_ccorres) 2399 apply wpsimp 2400 apply fastforce 2401 done 2402 2403lemma prepareThreadDelete_ccorres: 2404 "ccorres dc xfdc 2405 (invs' and tcb_at' thread) 2406 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) hs 2407 (prepareThreadDelete thread) (Call Arch_prepareThreadDelete_'proc)" 2408 supply dc_simp[simp del] 2409 apply (cinit lift: thread_', rename_tac cthread) 2410 apply (ctac add: fpuThreadDelete_ccorres) 2411 apply fastforce 2412 done 2413 2414lemma finaliseCap_ccorres: 2415 "\<And>final. 2416 ccorres (\<lambda>rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') 2417 \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 2418 ret__struct_finaliseCap_ret_C_' 2419 (invs' and sch_act_simple and valid_cap' cap and (\<lambda>s. ksIdleThread s \<notin> capRange cap) 2420 and (\<lambda>s. 2 ^ capBits cap \<le> gsMaxObjectSize s)) 2421 (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. final_' s = from_bool final} 2422 \<inter> {s. exposed_' s = from_bool flag (* dave has name wrong *)}) [] 2423 (finaliseCap cap final flag) (Call finaliseCap_'proc)" 2424 apply (rule_tac F="capAligned cap" in Corres_UL_C.ccorres_req) 2425 apply (clarsimp simp: valid_capAligned) 2426 apply (case_tac "P :: bool" for P) 2427 apply (rule ccorres_guard_imp2, erule finaliseCap_True_cases_ccorres) 2428 apply simp 2429 apply (subgoal_tac "\<exists>acap. (0 <=s (-1 :: word8)) \<or> acap = capCap cap") 2430 prefer 2 apply simp 2431 apply (erule exE) 2432 apply (cinit lift: cap_' final_' exposed_' cong: call_ignore_cong) 2433 apply csymbr 2434 apply (simp del: Collect_const) 2435 apply (rule ccorres_Cond_rhs_Seq) 2436 apply (clarsimp simp: cap_get_tag_isCap isCap_simps from_bool_neq_0 2437 cong: if_cong simp del: Collect_const) 2438 apply (clarsimp simp: word_sle_def) 2439 apply (rule ccorres_if_lhs) 2440 apply (rule ccorres_fail) 2441 apply (simp add: liftM_def del: Collect_const) 2442 apply (rule ccorres_rhs_assoc)+ 2443 apply (rule ccorres_add_return2) 2444 apply (ccorres_rewrite) 2445 apply (ctac add: Arch_finaliseCap_ccorres) 2446 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2447 apply (rule allI, rule conseqPre, vcg) 2448 apply (clarsimp simp: return_def Collect_const_mem) 2449 apply wp 2450 apply (vcg exspec=Arch_finaliseCap_modifies) 2451 apply (simp add: cap_get_tag_isCap Collect_False 2452 del: Collect_const) 2453 apply csymbr 2454 apply (simp add: cap_get_tag_isCap Collect_False Collect_True 2455 del: Collect_const) 2456 apply (rule ccorres_if_lhs) 2457 apply (simp, rule ccorres_fail) 2458 apply (simp add: from_bool_0 Collect_True Collect_False false_def 2459 del: Collect_const) 2460 apply csymbr 2461 apply (simp add: cap_get_tag_isCap Collect_False Collect_True 2462 del: Collect_const) 2463 apply (rule ccorres_if_lhs) 2464 apply (simp add: Let_def) 2465 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2466 apply (rule allI, rule conseqPre, vcg) 2467 apply (clarsimp simp: cap_get_tag_isCap word_sle_def 2468 return_def word_mod_less_divisor 2469 less_imp_neq [OF word_mod_less_divisor]) 2470 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2471 apply (clarsimp simp: isCap_simps capAligned_def 2472 objBits_simps word_bits_conv 2473 signed_shift_guard_simpler_64) 2474 apply (rule conjI) 2475 apply (simp add: word_less_nat_alt) 2476 apply (rule conjI) 2477 apply (auto simp: word_less_nat_alt word_le_not_less[symmetric] bit_simps objBits_defs)[1] 2478 apply (simp add: ccap_relation_def cap_zombie_cap_lift) 2479 apply (simp add: cap_to_H_def isZombieTCB_C_def ZombieTCB_C_def) 2480 apply (simp add: less_mask_eq word_less_nat_alt less_imp_neq) 2481 apply (simp add: mod_mask_drop[where n=6] mask_def[where n=6] 2482 less_imp_neq [OF word_mod_less_divisor] 2483 less_imp_neq Let_def objBits_simps') 2484 apply (thin_tac "a = b" for a b)+ 2485 apply (subgoal_tac "P" for P) 2486 apply (subst add.commute, subst unatSuc, assumption)+ 2487 apply clarsimp 2488 apply (rule conjI) 2489 apply (rule word_eqI) 2490 apply (simp add: word_size word_ops_nth_size nth_w2p 2491 less_Suc_eq_le is_aligned_nth) 2492 apply (safe, simp_all)[1] 2493 apply (simp add: shiftL_nat ccap_relation_NullCap_iff[symmetric, simplified ccap_relation_def]) 2494 apply (rule trans, rule unat_power_lower64[symmetric]) 2495 apply (simp add: word_bits_conv) 2496 apply (rule unat_cong, rule word_eqI) 2497 apply (simp add: word_size word_ops_nth_size nth_w2p 2498 is_aligned_nth less_Suc_eq_le) 2499 apply (safe, simp_all)[1] 2500 apply (subst add.commute, subst eq_diff_eq[symmetric]) 2501 apply (clarsimp simp: minus_one_norm) 2502 apply (rule ccorres_if_lhs) 2503 apply (simp add: Let_def getThreadCSpaceRoot_def locateSlot_conv 2504 Collect_True Collect_False 2505 del: Collect_const) 2506 apply (rule ccorres_rhs_assoc)+ 2507 apply csymbr 2508 apply csymbr 2509 apply csymbr 2510 apply csymbr 2511 apply (rule ccorres_Guard_Seq)+ 2512 apply csymbr 2513 apply (ctac(no_vcg) add: unbindNotification_ccorres) 2514 apply (ctac(no_vcg) add: suspend_ccorres[OF cteDeleteOne_ccorres]) 2515 apply (ctac(no_vcg) add: prepareThreadDelete_ccorres) 2516 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2517 apply (rule allI, rule conseqPre, vcg) 2518 apply (clarsimp simp: word_sle_def return_def) 2519 apply (subgoal_tac "cap_get_tag capa = scast cap_thread_cap") 2520 apply (drule(1) cap_get_tag_to_H) 2521 apply (clarsimp simp: isCap_simps capAligned_def ccap_relation_NullCap_iff) 2522 apply (simp add: ccap_relation_def cap_zombie_cap_lift) 2523 apply (simp add: cap_to_H_def isZombieTCB_C_def ZombieTCB_C_def 2524 mask_def) 2525 apply (simp add: cte_level_bits_def tcbCTableSlot_def 2526 Kernel_C.tcbCTable_def tcbCNodeEntries_def 2527 word_bool_alg.conj_disj_distrib2 2528 word_bw_assocs) 2529 apply (simp add: objBits_simps ctcb_ptr_to_tcb_ptr_def) 2530 apply (frule is_aligned_add_helper[where p="tcbptr - ctcb_offset" and d=ctcb_offset for tcbptr]) 2531 apply (simp add: ctcb_offset_defs objBits_defs) 2532 apply (simp add: mask_def objBits_defs tcb_arch_cnode_index_defs) 2533 apply (simp add: cap_get_tag_isCap) 2534 apply wp+ 2535 apply (rule ccorres_if_lhs) 2536 apply (simp add: Let_def) 2537 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2538 apply (rule allI, rule conseqPre, vcg) 2539 apply (clarsimp simp: return_def ccap_relation_NullCap_iff) 2540 apply (simp add: isArchCap_T_isArchObjectCap[symmetric] 2541 del: Collect_const) 2542 apply (rule ccorres_if_lhs) 2543 apply (simp add: Collect_False Collect_True Let_def true_def 2544 del: Collect_const) 2545 apply (rule_tac P="(capIRQ cap) \<le> X64.maxIRQ" in ccorres_gen_asm) 2546 apply (rule ccorres_rhs_assoc)+ 2547 apply csymbr 2548 apply csymbr 2549 apply (rule_tac xf'=irq_' in ccorres_abstract,ceqv) 2550 apply (rule_tac P="rv' = ucast (capIRQ cap)" in ccorres_gen_asm2) 2551 apply (ctac(no_vcg) add: deletingIRQHandler_ccorres) 2552 apply (rule ccorres_from_vcg_throws[where P=\<top> ]) 2553 apply (rule allI, rule conseqPre, vcg) 2554 apply (clarsimp simp: return_def) 2555 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2556 apply (simp add: ccap_relation_NullCap_iff split: if_split) 2557 apply wp 2558 apply (rule ccorres_if_lhs) 2559 apply simp 2560 apply (rule ccorres_fail) 2561 apply (rule ccorres_add_return, rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) 2562 apply (rule ccorres_Cond_rhs) 2563 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 2564 apply (rule ccorres_return_Skip) 2565 apply (rule ccorres_Cond_rhs) 2566 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 2567 apply (rule ccorres_return_Skip) 2568 apply (rule ccorres_Cond_rhs) 2569 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2570 apply simp 2571 apply (rule ccorres_Cond_rhs) 2572 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 2573 apply (rule ccorres_return_Skip) 2574 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 2575 apply (rule ccorres_return_Skip) 2576 apply (rule ceqv_refl) 2577 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2578 apply (rule allI, rule conseqPre, vcg) 2579 apply (clarsimp simp: return_def ccap_relation_NullCap_iff 2580 irq_opt_relation_def) 2581 apply wp 2582 apply (simp add: guard_is_UNIV_def) 2583 apply (clarsimp simp: cap_get_tag_isCap word_sle_def Collect_const_mem 2584 false_def from_bool_def) 2585 apply (intro impI conjI) 2586 apply (clarsimp split: bool.splits) 2587 apply (clarsimp split: bool.splits) 2588 apply (clarsimp simp: valid_cap'_def isCap_simps) 2589 apply (clarsimp simp: isCap_simps capRange_def capAligned_def) 2590 apply (clarsimp simp: isCap_simps valid_cap'_def) 2591 apply (clarsimp simp: isCap_simps capRange_def capAligned_def) 2592 apply (clarsimp simp: isCap_simps valid_cap'_def ) 2593 apply clarsimp 2594 apply (clarsimp simp: isCap_simps valid_cap'_def ) 2595 apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def ccap_relation_def isCap_simps 2596 c_valid_cap_def cap_thread_cap_lift_def cap_to_H_def 2597 ctcb_ptr_to_tcb_ptr_def Let_def 2598 split: option.splits cap_CL.splits if_splits) 2599 apply clarsimp 2600 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2601 apply (clarsimp simp: isCap_simps from_bool_def false_def) 2602 apply (clarsimp simp: tcb_cnode_index_defs ptr_add_assertion_def) 2603 apply clarsimp 2604 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2605 apply (frule(1) ccap_relation_IRQHandler_mask) 2606 apply (clarsimp simp: isCap_simps irqInvalid_def 2607 valid_cap'_def X64.maxIRQ_def 2608 Kernel_C.maxIRQ_def) 2609 apply (rule irq_opt_relation_Some_ucast', simp) 2610 apply (clarsimp simp: isCap_simps irqInvalid_def 2611 valid_cap'_def X64.maxIRQ_def 2612 Kernel_C.maxIRQ_def) 2613 apply fastforce 2614 apply clarsimp 2615 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2616 apply (frule(1) ccap_relation_IRQHandler_mask) 2617 apply (clarsimp simp add:mask_eq_ucast_eq) 2618 done 2619 end 2620 2621end 2622