1(* 2 * Copyright 2017, Data61, CSIRO 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(DATA61_GPL) 9 *) 10 11chapter "Toplevel Refinement Statement" 12 13(* In progress c refinement *) 14 15theory Refine_C 16imports 17 Init_C 18 19 (* FIXME: Fastpath_C left out, imports lifted here: *) 20 SyscallArgs_C 21 Delete_C 22 Syscall_C 23 "Refine.RAB_FN" 24 "CLib.MonadicRewrite_C" 25 26 "../lib/CToCRefine" 27begin 28 29context begin interpretation Arch . (*FIXME: arch_split*) 30crunch ksQ[wp]: handleVMFault "\<lambda>s. P (ksReadyQueues s)" 31end 32 33context kernel_m 34begin 35 36declare liftE_handle [simp] 37 38lemma schedule_sch_act_wf: 39 "\<lbrace>invs'\<rbrace> schedule \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" 40apply (rule hoare_post_imp) 41 apply (erule invs_sch_act_wf') 42apply (rule schedule_invs') 43done 44 45lemma ucast_8_32_neq: 46 "x \<noteq> 0xFF \<Longrightarrow> UCAST(8 \<rightarrow> 32 signed) x \<noteq> 0xFF" 47 by uint_arith (clarsimp simp: uint_up_ucast is_up) 48 49lemma Arch_finaliseInterrupt_ccorres: 50 "ccorres dc xfdc \<top> UNIV [] (return a) (Call Arch_finaliseInterrupt_'proc)" 51 apply (rule ccorres_from_vcg) 52 apply (rule allI, rule conseqPre, vcg) 53 apply (simp add: return_def) 54 done 55 56lemma handleInterruptEntry_ccorres: 57 "ccorres dc xfdc 58 (invs' and sch_act_simple) 59 UNIV [] 60 (callKernel Interrupt) (Call handleInterruptEntry_'proc)" 61proof - 62 show ?thesis 63 apply (cinit') 64 apply (simp add: callKernel_def handleEvent_def minus_one_norm) 65 apply (simp add: liftE_bind bind_assoc) 66 apply (ctac (no_vcg) add: getActiveIRQ_ccorres) 67 apply (rule ccorres_Guard_Seq)? 68 apply wpc 69 apply (simp add: irqInvalid_def) 70 apply (rule ccorres_symb_exec_r) 71 apply (ctac (no_vcg) add: schedule_ccorres) 72 apply (rule ccorres_add_return2) 73 apply (ctac (no_vcg) add: activateThread_ccorres) 74 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 75 apply (rule allI, rule conseqPre, vcg) 76 apply (clarsimp simp: return_def) 77 apply (wp schedule_sch_act_wf schedule_invs' 78 | strengthen invs_queues_imp invs_valid_objs_strengthen)+ 79 apply vcg 80 apply vcg 81 apply (clarsimp simp: irqInvalid_def ucast_8_32_neq) 82 apply (rule ccorres_rhs_assoc) 83 apply (ctac (no_vcg) add: handleInterrupt_ccorres) 84 apply (rule ccorres_add_return, ctac (no_vcg) add: Arch_finaliseInterrupt_ccorres) 85 apply (ctac (no_vcg) add: schedule_ccorres) 86 apply (rule ccorres_add_return2) 87 apply (ctac (no_vcg) add: activateThread_ccorres) 88 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 89 apply (rule allI, rule conseqPre, vcg) 90 apply (clarsimp simp: return_def) 91 apply (wp schedule_sch_act_wf schedule_invs' 92 | strengthen invs_queues_imp invs_valid_objs_strengthen)+ 93 apply (rule_tac Q="\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> X64.maxIRQ) \<and> rv \<noteq> Some 0x3FF" in hoare_post_imp) 94 apply (clarsimp simp: non_kernel_IRQs_def) 95 apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+ 96 apply (clarsimp simp: invs'_def valid_state'_def) 97 done 98qed 99 100lemma handleUnknownSyscall_ccorres: 101 "ccorres dc xfdc 102 (invs' and ct_running' and 103 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) 104 (UNIV \<inter> {s. of_nat n = w_' s}) [] 105 (callKernel (UnknownSyscall n)) (Call handleUnknownSyscall_'proc)" 106 apply (cinit' lift: w_') 107 apply (simp add: callKernel_def handleEvent_def) 108 apply (simp add: liftE_bind bind_assoc) 109 apply (rule ccorres_symb_exec_r) 110 apply (rule ccorres_pre_getCurThread) 111 apply (ctac (no_vcg) add: handleFault_ccorres) 112 apply (ctac (no_vcg) add: schedule_ccorres) 113 apply (rule ccorres_add_return2) 114 apply (ctac (no_vcg) add: activateThread_ccorres) 115 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 116 apply (rule allI, rule conseqPre, vcg) 117 apply (clarsimp simp: return_def) 118 apply (wp schedule_sch_act_wf schedule_invs' 119 | strengthen invs_queues_imp invs_valid_objs_strengthen)+ 120 apply (clarsimp, vcg) 121 apply (clarsimp, rule conseqPre, vcg, clarsimp) 122 apply clarsimp 123 apply (intro impI conjI allI) 124 apply fastforce 125 apply (clarsimp simp: ct_not_ksQ) 126 apply (clarsimp simp add: sch_act_simple_def split: scheduler_action.split) 127 apply (rule active_ex_cap') 128 apply (erule active_from_running') 129 apply (erule invs_iflive') 130 apply (clarsimp simp: ct_in_state'_def) 131 apply (frule st_tcb_idle'[rotated]) 132 apply (erule invs_valid_idle') 133 apply (clarsimp simp: cfault_rel_def seL4_Fault_UnknownSyscall_lift is_cap_fault_def) 134 done 135 136lemma handleVMFaultEvent_ccorres: 137 "ccorres dc xfdc 138 (invs' and sch_act_simple and ct_running' and 139 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) 140 (UNIV \<inter> {s. vm_faultType_' s = vm_fault_type_from_H vmfault_type}) [] 141 (callKernel (VMFaultEvent vmfault_type)) (Call handleVMFaultEvent_'proc)" 142 apply (cinit' lift:vm_faultType_') 143 apply (simp add: callKernel_def handleEvent_def) 144 apply (simp add: liftE_bind bind_assoc) 145 apply (rule ccorres_pre_getCurThread) 146 apply (simp add: catch_def) 147 apply (rule ccorres_rhs_assoc2) 148 apply (rule ccorres_split_nothrow_novcg) 149 apply (rule ccorres_split_nothrow_case_sum) 150 apply (ctac (no_vcg) add: handleVMFault_ccorres) 151 apply ceqv 152 apply clarsimp 153 apply clarsimp 154 apply (rule ccorres_cond_univ) 155 apply (rule_tac P="\<lambda>s. ksCurThread s = rv" in ccorres_cross_over_guard) 156 apply (rule_tac xf'=xfdc in ccorres_call) 157 apply (ctac (no_vcg) add: handleFault_ccorres) 158 apply simp 159 apply simp 160 apply simp 161 apply (wp hv_inv_ex') 162 apply (simp add: guard_is_UNIV_def) 163 apply clarsimp 164 apply (vcg exspec=handleVMFault_modifies) 165 apply ceqv 166 apply clarsimp 167 apply (ctac (no_vcg) add: schedule_ccorres) 168 apply (rule ccorres_add_return2) 169 apply (ctac (no_vcg) add: activateThread_ccorres) 170 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 171 apply (rule allI, rule conseqPre, vcg) 172 apply (clarsimp simp: return_def) 173 apply (wp schedule_sch_act_wf schedule_invs' 174 | strengthen invs_queues_imp invs_valid_objs_strengthen)+ 175 apply (case_tac x, clarsimp, wp) 176 apply (clarsimp, wp, simp) 177 apply wp 178 apply (simp add: guard_is_UNIV_def) 179 apply (clarsimp simp: simple_sane_strg[unfolded sch_act_sane_not]) 180 by (auto simp: ct_in_state'_def cfault_rel_def is_cap_fault_def ct_not_ksQ 181 elim: pred_tcb'_weakenE st_tcb_ex_cap'' 182 dest: st_tcb_at_idle_thread' rf_sr_ksCurThread) 183 184 185lemma handleUserLevelFault_ccorres: 186 "ccorres dc xfdc 187 (invs' and sch_act_simple and ct_running' and 188 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) 189 (UNIV \<inter> {s. w_a_' s = word1} \<inter> {s. w_b_' s = word2 }) [] 190 (callKernel (UserLevelFault word1 word2)) (Call handleUserLevelFault_'proc)" 191 apply (cinit' lift:w_a_' w_b_') 192 apply (simp add: callKernel_def handleEvent_def) 193 apply (simp add: liftE_bind bind_assoc) 194 apply (rule ccorres_symb_exec_r) 195 apply (rule ccorres_pre_getCurThread) 196 apply (ctac (no_vcg) add: handleFault_ccorres) 197 apply (ctac (no_vcg) add: schedule_ccorres) 198 apply (rule ccorres_add_return2) 199 apply (ctac (no_vcg) add: activateThread_ccorres) 200 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 201 apply (rule allI, rule conseqPre, vcg) 202 apply (clarsimp simp: return_def) 203 apply (wp schedule_sch_act_wf schedule_invs' 204 | strengthen invs_queues_imp invs_valid_objs_strengthen)+ 205 apply (clarsimp, vcg) 206 apply (clarsimp, rule conseqPre, vcg, clarsimp) 207 apply clarsimp 208 apply (intro impI conjI allI) 209 apply (simp add: ct_in_state'_def) 210 apply (erule pred_tcb'_weakenE) 211 apply simp 212 apply (clarsimp simp: ct_not_ksQ) 213 apply (clarsimp simp add: sch_act_simple_def split: scheduler_action.split) 214 apply (rule active_ex_cap') 215 apply (erule active_from_running') 216 apply (erule invs_iflive') 217 apply (clarsimp simp: ct_in_state'_def) 218 apply (frule st_tcb_idle'[rotated]) 219 apply (erule invs_valid_idle') 220 apply simp 221 apply (clarsimp simp: cfault_rel_def seL4_Fault_UserException_lift) 222 apply (simp add: is_cap_fault_def) 223 done 224 225lemmas syscall_defs = 226 Kernel_C.SysSend_def Kernel_C.SysNBSend_def 227 Kernel_C.SysCall_def Kernel_C.SysRecv_def Kernel_C.SysNBRecv_def 228 Kernel_C.SysReply_def Kernel_C.SysReplyRecv_def Kernel_C.SysYield_def 229 230lemma ct_active_not_idle'_strengthen: 231 "invs' s \<and> ct_active' s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s" 232 by clarsimp 233 234 235 236lemma handleSyscall_ccorres: 237 "ccorres dc xfdc 238 (invs' and 239 sch_act_simple and ct_running' and 240 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) 241 (UNIV \<inter> {s. syscall_' s = syscall_from_H sysc }) [] 242 (callKernel (SyscallEvent sysc)) (Call handleSyscall_'proc)" 243 apply (cinit' lift: syscall_') 244 apply (simp add: callKernel_def handleEvent_def minus_one_norm) 245 apply (simp add: handleE_def handleE'_def) 246 apply (rule ccorres_split_nothrow_novcg) 247 apply wpc 248 prefer 3 249 \<comment> \<open>SysSend\<close> 250 apply (clarsimp simp: syscall_from_H_def syscall_defs) 251 apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+ 252 apply (simp add: handleSend_def) 253 apply (rule ccorres_split_nothrow_case_sum) 254 apply (ctac (no_vcg) add: handleInvocation_ccorres) 255 apply ceqv 256 apply clarsimp 257 apply (rule ccorres_cond_empty) 258 apply (rule ccorres_returnOk_skip[unfolded returnOk_def,simplified]) 259 apply clarsimp 260 apply (rule ccorres_cond_univ) 261 apply (simp add: liftE_def bind_assoc) 262 apply (ctac (no_vcg) add: getActiveIRQ_ccorres) 263 apply (rule ccorres_Guard)? 264 apply (simp only: irqInvalid_def)? 265 apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm) 266 apply (subst ccorres_seq_skip'[symmetric]) 267 apply (rule ccorres_split_nothrow_novcg) 268 apply (rule_tac R=\<top> and xf=xfdc in ccorres_when) 269 apply (case_tac rv, clarsimp, clarsimp simp: ucast_8_32_neq) 270 apply (rule ccorres_add_return2) 271 apply (ctac (no_vcg) add: handleInterrupt_ccorres) 272 apply (ctac (no_vcg) add: Arch_finaliseInterrupt_ccorres, wp) 273 apply ceqv 274 apply (rule_tac r=dc and xf=xfdc in ccorres_returnOk_skip[unfolded returnOk_def,simplified]) 275 apply wp 276 apply (simp add: guard_is_UNIV_def) 277 apply clarsimp 278 apply (rule_tac Q="\<lambda>rv s. invs' s \<and> 279 (\<forall>x. rv = Some x \<longrightarrow> x \<le> X64.maxIRQ) \<and> rv \<noteq> Some 0x3FF" 280 in hoare_post_imp) 281 apply (clarsimp simp: non_kernel_IRQs_def) 282 apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+ 283 apply (rule_tac Q=" invs' " in hoare_post_imp_dc2E, wp) 284 apply (simp add: invs'_def valid_state'_def) 285 apply clarsimp 286 apply (vcg exspec=handleInvocation_modifies) 287 prefer 3 288 \<comment> \<open>SysNBSend\<close> 289 apply (clarsimp simp: syscall_from_H_def syscall_defs) 290 apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+ 291 apply (simp add: handleSend_def) 292 apply (rule ccorres_split_nothrow_case_sum) 293 apply (ctac (no_vcg) add: handleInvocation_ccorres) 294 apply ceqv 295 apply clarsimp 296 apply (rule ccorres_cond_empty) 297 apply (rule ccorres_returnOk_skip[unfolded returnOk_def,simplified]) 298 apply clarsimp 299 apply (rule ccorres_cond_univ) 300 apply (simp add: liftE_def bind_assoc irqInvalid_def) 301 apply (ctac (no_vcg) add: getActiveIRQ_ccorres) 302 apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm) 303 apply (subst ccorres_seq_skip'[symmetric]) 304 apply (rule ccorres_split_nothrow_novcg) 305 apply (rule ccorres_Guard)? 306 apply (rule_tac R=\<top> and xf=xfdc in ccorres_when) 307 apply (case_tac rv, clarsimp, clarsimp simp: ucast_8_32_neq) 308 apply (rule ccorres_add_return2) 309 apply (ctac (no_vcg) add: handleInterrupt_ccorres) 310 apply (ctac (no_vcg) add: Arch_finaliseInterrupt_ccorres, wp) 311 apply ceqv 312 apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified]) 313 apply wp 314 apply (simp add: guard_is_UNIV_def) 315 apply clarsimp 316 apply (rule_tac Q="\<lambda>rv s. invs' s \<and> 317 (\<forall>x. rv = Some x \<longrightarrow> x \<le> X64.maxIRQ) \<and> rv \<noteq> Some 0x3FF" 318 in hoare_post_imp) 319 apply (clarsimp simp: non_kernel_IRQs_def) 320 apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+ 321 apply (rule_tac Q=" invs' " in hoare_post_imp_dc2E, wp) 322 apply (simp add: invs'_def valid_state'_def) 323 apply clarsimp 324 apply (vcg exspec=handleInvocation_modifies) 325 \<comment> \<open>SysCall\<close> 326 apply (clarsimp simp: syscall_from_H_def syscall_defs) 327 apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+ 328 apply (simp add: handleCall_def) 329 apply (rule ccorres_split_nothrow_case_sum) 330 apply (ctac (no_vcg) add: handleInvocation_ccorres) 331 apply ceqv 332 apply clarsimp 333 apply (rule ccorres_cond_empty) 334 apply (rule ccorres_returnOk_skip[unfolded returnOk_def,simplified]) 335 apply clarsimp 336 apply (rule ccorres_cond_univ) 337 apply (simp add: liftE_def bind_assoc irqInvalid_def) 338 apply (ctac (no_vcg) add: getActiveIRQ_ccorres) 339 apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm) 340 apply (subst ccorres_seq_skip'[symmetric]) 341 apply (rule ccorres_split_nothrow_novcg) 342 apply (rule ccorres_Guard)? 343 apply (rule_tac R=\<top> and xf=xfdc in ccorres_when) 344 apply (case_tac rv, clarsimp) 345 apply (clarsimp simp: ucast_8_32_neq) 346 apply clarsimp 347 apply (rule ccorres_add_return2) 348 apply (ctac (no_vcg) add: handleInterrupt_ccorres) 349 apply (ctac (no_vcg) add: Arch_finaliseInterrupt_ccorres, wp) 350 apply ceqv 351 apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified]) 352 apply wp 353 apply (simp add: guard_is_UNIV_def) 354 apply clarsimp 355 apply (rule_tac Q="\<lambda>rv s. invs' s \<and> 356 (\<forall>x. rv = Some x \<longrightarrow> x \<le> X64.maxIRQ) \<and> rv \<noteq> Some 0x3FF" 357 in hoare_post_imp) 358 apply (clarsimp simp: non_kernel_IRQs_def) 359 apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+ 360 apply (rule_tac Q=" invs' " in hoare_post_imp_dc2E, wp) 361 apply (simp add: invs'_def valid_state'_def) 362 apply clarsimp 363 apply (vcg exspec=handleInvocation_modifies) 364 prefer 2 365 \<comment> \<open>SysRecv\<close> 366 apply (clarsimp simp: syscall_from_H_def syscall_defs) 367 apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+ 368 apply (simp add: liftE_bind) 369 apply (subst ccorres_seq_skip'[symmetric]) 370 apply (ctac (no_vcg) add: handleRecv_ccorres) 371 apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified]) 372 apply wp 373 prefer 2 374 \<comment> \<open>SysReply\<close> 375 apply (clarsimp simp: syscall_from_H_def syscall_defs) 376 apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+ 377 apply (simp add: liftE_bind) 378 apply (subst ccorres_seq_skip'[symmetric]) 379 apply (ctac (no_vcg) add: handleReply_ccorres) 380 apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified]) 381 apply wp 382 \<comment> \<open>SysReplyRecv\<close> 383 apply (clarsimp simp: syscall_from_H_def syscall_defs) 384 apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+ 385 apply (simp add: liftE_bind bind_assoc) 386 apply (ctac (no_vcg) add: handleReply_ccorres) 387 apply (subst ccorres_seq_skip'[symmetric]) 388 apply (ctac (no_vcg) add: handleRecv_ccorres) 389 apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified]) 390 apply wp[1] 391 apply clarsimp 392 apply wp 393 apply (rule_tac Q="\<lambda>rv s. ct_in_state' simple' s \<and> sch_act_sane s \<and> 394 (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))" 395 in hoare_post_imp) 396 apply (simp add: ct_in_state'_def) 397 apply (wp handleReply_sane handleReply_ct_not_ksQ) 398 \<comment> \<open>SysYield\<close> 399 apply (clarsimp simp: syscall_from_H_def syscall_defs) 400 apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+ 401 apply (simp add: liftE_bind) 402 apply (subst ccorres_seq_skip'[symmetric]) 403 apply (ctac (no_vcg) add: handleYield_ccorres) 404 apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified]) 405 apply wp 406 \<comment> \<open>SysNBRecv\<close> 407 apply (clarsimp simp: syscall_from_H_def syscall_defs) 408 apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+ 409 apply (simp add: liftE_bind) 410 apply (subst ccorres_seq_skip'[symmetric]) 411 apply (ctac (no_vcg) add: handleRecv_ccorres) 412 apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified]) 413 apply wp 414 \<comment> \<open>rest of body\<close> 415 apply ceqv 416 apply (ctac (no_vcg) add: schedule_ccorres) 417 apply (rule ccorres_add_return2) 418 apply (ctac (no_vcg) add: activateThread_ccorres) 419 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 420 apply (rule allI, rule conseqPre, vcg) 421 apply (clarsimp simp: return_def) 422 apply (wp schedule_invs' schedule_sch_act_wf | strengthen invs_queues_imp invs_valid_objs_strengthen)+ 423 apply (simp 424 | wpc 425 | wp hoare_drop_imp handleReply_sane handleReply_nonz_cap_to_ct schedule_invs' 426 handleReply_ct_not_ksQ[simplified] 427 | strengthen ct_active_not_idle'_strengthen invs_valid_objs_strengthen)+ 428 apply (rule_tac Q="\<lambda>rv. invs' and ct_active'" in hoare_post_imp, simp) 429 apply (wp hy_invs') 430 apply (clarsimp simp add: liftE_def) 431 apply wp 432 apply (rule_tac Q="\<lambda>rv. invs' and ct_active'" in hoare_post_imp, simp) 433 apply (wp hy_invs') 434 apply (clarsimp simp: liftE_def) 435 apply (wp) 436 apply (rule_tac Q="\<lambda>_. invs'" in hoare_post_imp, simp) 437 apply (wp hw_invs') 438 apply (simp add: guard_is_UNIV_def) 439 apply clarsimp 440 apply (drule active_from_running') 441 apply (frule active_ex_cap') 442 apply (clarsimp simp: invs'_def valid_state'_def) 443 apply (clarsimp simp: simple_sane_strg ct_in_state'_def st_tcb_at'_def obj_at'_def 444 isReply_def ct_not_ksQ) 445 apply (rule conjI, fastforce) 446 apply (auto simp: syscall_from_H_def Kernel_C.SysSend_def 447 split: option.split_asm) 448 done 449 450lemma ccorres_corres_u: 451 "\<lbrakk> ccorres dc xfdc P (Collect P') [] H C; no_fail P H \<rbrakk> \<Longrightarrow> 452 corres_underlying rf_sr nf nf' dc P P' H (exec_C \<Gamma> C)" 453 apply (clarsimp simp: ccorres_underlying_def corres_underlying_def) 454 apply (drule (1) bspec) 455 apply (clarsimp simp: exec_C_def no_fail_def) 456 apply (rule conjI) 457 apply clarsimp 458 apply (erule_tac x=0 in allE) 459 apply (erule_tac x="Normal y" in allE) 460 apply simp 461 apply (erule impE) 462 apply (drule EHOther [where hs="[]"], simp) 463 apply simp 464 apply fastforce 465 apply clarsimp 466 apply (case_tac xs, simp_all) 467 apply (fastforce intro: EHAbrupt EHEmpty) 468 apply (fastforce intro: EHOther)+ 469 done 470 471lemma ccorres_corres_u_xf: 472 "\<lbrakk> ccorres rel xf P (Collect P') [] H C; no_fail P H \<rbrakk> \<Longrightarrow> 473 corres_underlying rf_sr nf nf' rel P P' H ((exec_C \<Gamma> C) >>= (\<lambda>_. gets xf))" 474 apply (clarsimp simp: ccorres_underlying_def corres_underlying_def) 475 apply (drule (1) bspec) 476 apply (clarsimp simp: exec_C_def no_fail_def) 477 apply (drule_tac x = a in spec) 478 apply (clarsimp simp:gets_def NonDetMonad.bind_def get_def return_def) 479 apply (rule conjI) 480 apply clarsimp 481 apply (erule_tac x=0 in allE) 482 apply (erule_tac x="Normal y" in allE) 483 apply simp 484 apply (erule impE) 485 apply (drule EHOther [where hs="[]"], simp) 486 apply simp 487 apply (simp add: unif_rrel_def) 488 apply (clarsimp simp:image_def) 489 apply (case_tac xs, simp_all) 490 apply (fastforce intro: EHAbrupt EHEmpty) 491 apply (fastforce intro: EHOther)+ 492 done 493 494definition 495 "all_invs' e \<equiv> \<lambda>s'. \<exists>s :: det_state. 496 (s,s') \<in> state_relation \<and> 497 (einvs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> 498 scheduler_action s = resume_cur_thread \<and> domain_time s \<noteq> 0) \<and> 499 (invs' s' \<and> 500 (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> 501 ksSchedulerAction s' = ResumeCurrentThread \<and> ksDomainTime s' \<noteq> 0)" 502 503lemma no_fail_callKernel: 504 "no_fail (all_invs' e) (callKernel e)" 505 unfolding all_invs'_def 506 apply (rule corres_nofail) 507 apply (rule corres_guard_imp) 508 apply (rule kernel_corres) 509 apply force 510 apply (simp add: sch_act_simple_def) 511 apply metis 512 done 513 514lemma handleHypervisorEvent_ccorres: 515 "ccorres dc xfdc 516 (invs' and sch_act_simple) 517 UNIV [] 518 (callKernel (HypervisorEvent t)) handleHypervisorEvent_C" 519 apply (simp add: callKernel_def handleEvent_def handleHypervisorEvent_C_def) 520 apply (simp add: liftE_def bind_assoc) 521 apply (rule ccorres_guard_imp) 522 apply (rule ccorres_symb_exec_l) 523 apply (cases t; simp add: handleHypervisorFault_def) 524 apply (ctac (no_vcg) add: schedule_ccorres) 525 apply (ctac (no_vcg) add: activateThread_ccorres) 526 apply (wp schedule_sch_act_wf schedule_invs' 527 | strengthen invs_queues_imp invs_valid_objs_strengthen)+ 528 apply clarsimp+ 529 done 530 531lemma callKernel_corres_C: 532 "corres_underlying rf_sr False True dc 533 (all_invs' e) 534 \<top> 535 (callKernel e) (callKernel_C e)" 536 using no_fail_callKernel [of e] 537 apply (clarsimp simp: callKernel_C_def) 538 apply (cases e, simp_all) 539 prefer 4 540 apply (rule ccorres_corres_u) 541 apply simp 542 apply (rule ccorres_guard_imp) 543 apply (rule handleInterruptEntry_ccorres) 544 apply (clarsimp simp: all_invs'_def sch_act_simple_def) 545 apply simp 546 apply assumption 547 prefer 2 548 apply (rule ccorres_corres_u [rotated], assumption) 549 apply simp 550 apply (rule ccorres_guard_imp) 551 apply (rule ccorres_call) 552 apply (rule handleUnknownSyscall_ccorres) 553 apply (clarsimp simp: all_invs'_def sch_act_simple_def)+ 554 prefer 3 555 apply (rule ccorres_corres_u [rotated], assumption) 556 apply (rule ccorres_guard_imp) 557 apply (rule ccorres_call) 558 apply (rule handleVMFaultEvent_ccorres) 559 apply (clarsimp simp: all_invs'_def sch_act_simple_def)+ 560 prefer 2 561 apply (rule ccorres_corres_u [rotated], assumption) 562 apply (rule ccorres_guard_imp) 563 apply (rule ccorres_call) 564 apply (rule handleUserLevelFault_ccorres) 565 apply (clarsimp simp: all_invs'_def sch_act_simple_def)+ 566 apply (rule ccorres_corres_u [rotated], assumption) 567 apply (rule ccorres_guard_imp) 568 apply (rule ccorres_call) 569 apply (rule handleSyscall_ccorres) 570 apply (clarsimp simp: all_invs'_def sch_act_simple_def)+ 571 apply (rule ccorres_corres_u [rotated], assumption) 572 apply (rule ccorres_guard_imp) 573 apply (rule handleHypervisorEvent_ccorres) 574 apply (clarsimp simp: all_invs'_def sch_act_simple_def) 575 apply simp 576 done 577 578lemma ccorres_add_gets: 579 "ccorresG rf_sr \<Gamma> rv xf P P' hs (do v \<leftarrow> gets f; m od) c 580 \<Longrightarrow> ccorresG rf_sr \<Gamma> rv xf P P' hs m c" 581 by (simp add: gets_bind_ign) 582 583lemma ccorres_get_registers: 584 "\<lbrakk> \<And>cptr msgInfo. ccorres dc xfdc 585 ((\<lambda>s. P s \<and> Q s \<and> 586 obj_at' (\<lambda>tcb. (user_regs o atcbContextGet o tcbArch) tcb X64.capRegister = cptr 587 \<and> (user_regs o atcbContextGet o tcbArch) tcb X64.msgInfoRegister = msgInfo) 588 (ksCurThread s) s) and R) 589 (UNIV \<inter> \<lbrace>\<acute>cptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>msgInfo = msgInfo\<rbrace>) [] m c \<rbrakk> 590 \<Longrightarrow> 591 ccorres dc xfdc 592 (P and Q and ct_in_state' \<top> and R) 593 {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v 594 \<and> cptr_' s = index (registers_C (tcbContext_C (tcbArch_C v))) (unat Kernel_C.capRegister) 595 \<and> msgInfo_' s = index (registers_C (tcbContext_C (tcbArch_C v))) (unat Kernel_C.msgInfoRegister)} [] 596 m c" 597 apply (rule ccorres_assume_pre) 598 apply (clarsimp simp: ct_in_state'_def st_tcb_at'_def) 599 apply (drule obj_at_ko_at', clarsimp) 600 apply (erule_tac x="(user_regs o atcbContextGet o tcbArch) ko X64.capRegister" in meta_allE) 601 apply (erule_tac x="(user_regs o atcbContextGet o tcbArch) ko X64.msgInfoRegister" in meta_allE) 602 apply (erule ccorres_guard_imp2) 603 apply (clarsimp simp: rf_sr_ksCurThread) 604 apply (drule(1) obj_at_cslift_tcb, clarsimp simp: obj_at'_def projectKOs) 605 apply (clarsimp simp: ctcb_relation_def ccontext_relation_def cregs_relation_def 606 X64.msgInfoRegister_def X64.capRegister_def 607 carch_tcb_relation_def 608 "StrictC'_register_defs") 609 done 610 611(* FIXME: move *) 612lemma st_tcb_at'_opeq_simp: 613 "st_tcb_at' ((=) Structures_H.thread_state.Running) (ksCurThread s) s 614 = st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s" 615 by (fastforce simp add: st_tcb_at'_def obj_at'_def) 616 617(* FIXME: fastpath 618lemma callKernel_withFastpath_corres_C: 619 "corres_underlying rf_sr False True dc 620 (all_invs' e) 621 \<top> 622 (callKernel e) (callKernel_withFastpath_C e)" 623 using no_fail_callKernel [of e] callKernel_corres_C [of e] 624 apply (cases "e = SyscallEvent syscall.SysCall \<or> 625 e = SyscallEvent syscall.SysReplyRecv") 626 apply (simp_all add: callKernel_withFastpath_C_def 627 del: Collect_const cong: call_ignore_cong) 628 apply (erule ccorres_corres_u[rotated]) 629 apply (rule ccorres_guard_imp2) 630 apply (rule ccorres_rhs_assoc)+ 631 apply (rule ccorres_symb_exec_r)+ 632 apply (rule ccorres_Cond_rhs) 633 apply (simp add: dc_def[symmetric]) 634 apply (ctac add: ccorres_get_registers[OF fastpath_call_ccorres_callKernel]) 635 apply (simp add: dc_def[symmetric]) 636 apply (ctac add: ccorres_get_registers[OF fastpath_reply_recv_ccorres_callKernel]) 637 apply vcg 638 apply (rule conseqPre, vcg, clarsimp) 639 apply vcg 640 apply (rule conseqPre, vcg, clarsimp) 641 apply (clarsimp simp: all_invs'_def rf_sr_ksCurThread) 642 apply (frule(1) obj_at_cslift_tcb[OF tcb_at_invs']) 643 apply (clarsimp simp: typ_heap_simps' ct_in_state'_def 644 "StrictC'_register_defs" word_sle_def word_sless_def 645 st_tcb_at'_opeq_simp) 646 apply (rule conjI, fastforce simp: st_tcb_at'_def) 647 apply (auto elim!: pred_tcb'_weakenE cnode_caps_gsCNodes_from_sr[rotated]) 648 done 649*) 650 651lemma threadSet_all_invs_triv': 652 "\<lbrace>all_invs' e and (\<lambda>s. t = ksCurThread s)\<rbrace> 653 threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet f (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_. all_invs' e\<rbrace>" 654 unfolding all_invs'_def 655 apply (rule hoare_pre) 656 apply (rule wp_from_corres_unit) 657 apply (rule threadset_corresT [where f="tcb_arch_update (arch_tcb_context_set f)"]) 658 apply (simp add: tcb_relation_def arch_tcb_context_set_def 659 atcbContextSet_def arch_tcb_relation_def) 660 apply (simp add: tcb_cap_cases_def) 661 apply (simp add: tcb_cte_cases_def) 662 apply (simp add: exst_same_def) 663 apply (wp thread_set_invs_trivial thread_set_ct_running thread_set_not_state_valid_sched 664 threadSet_invs_trivial threadSet_ct_running' static_imp_wp 665 thread_set_ct_idle 666 | simp add: tcb_cap_cases_def tcb_arch_ref_def 667 | rule threadSet_ct_in_state' 668 | wp_once hoare_vcg_disj_lift)+ 669 apply clarsimp 670 apply (rule exI, rule conjI, assumption) 671 apply (clarsimp simp: invs_def invs'_def cur_tcb_def cur_tcb'_def) 672 apply (simp add: state_relation_def) 673 done 674 675lemma getContext_corres: 676 "t' = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> 677 corres_underlying rf_sr False True (=) (tcb_at' t) \<top> 678 (threadGet (atcbContextGet o tcbArch) t) (gets (getContext_C t'))" 679 apply (clarsimp simp: corres_underlying_def simpler_gets_def) 680 apply (drule obj_at_ko_at') 681 apply clarsimp 682 apply (frule threadGet_eq) 683 apply (rule bexI) 684 prefer 2 685 apply assumption 686 apply clarsimp 687 apply (clarsimp simp: getContext_C_def) 688 apply (drule cmap_relation_ko_atD [rotated]) 689 apply fastforce 690 apply (clarsimp simp: typ_heap_simps ctcb_relation_def carch_tcb_relation_def from_user_context_C) 691 done 692 693lemma callKernel_cur: 694 "\<lbrace>all_invs' e\<rbrace> callKernel e \<lbrace>\<lambda>rv s. tcb_at' (ksCurThread s) s\<rbrace>" 695 apply (rule hoare_chain) 696 apply (rule ckernel_invs) 697 apply (clarsimp simp: all_invs'_def sch_act_simple_def) 698 apply clarsimp 699 done 700 701lemma entry_corres_C: 702 "fp = False \<Longrightarrow> (* FIXME: fastpath *) 703 corres_underlying rf_sr False True (=) 704 (all_invs' e) 705 \<top> 706 (kernelEntry e uc) (kernelEntry_C fp e uc)" 707 apply (simp add: kernelEntry_C_def kernelEntry_def getCurThread_def) 708 apply (rule corres_guard_imp) 709 apply (rule corres_split [where P=\<top> and P'=\<top> and r'="\<lambda>t t'. t' = tcb_ptr_to_ctcb_ptr t"]) 710 prefer 2 711 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 712 apply (rule corres_split) 713 prefer 2 714 apply (rule setTCBContext_C_corres, rule ccontext_rel_to_C, simp) 715 apply simp 716 apply (rule corres_split) 717 prefer 2 718(* FIXME: fastpath 719 apply (rule corres_cases[where R=fp], simp_all add: dc_def[symmetric])[1] 720 apply (rule callKernel_withFastpath_corres_C, simp) 721*) 722 apply (rule callKernel_corres_C[unfolded dc_def], simp) 723 apply (rule corres_split [where P=\<top> and P'=\<top> and r'="\<lambda>t t'. t' = tcb_ptr_to_ctcb_ptr t"]) 724 prefer 2 725 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 726 apply (rule getContext_corres[unfolded o_def], simp) 727 apply (wp threadSet_all_invs_triv' callKernel_cur)+ 728 apply (clarsimp simp: all_invs'_def invs'_def cur_tcb'_def valid_state'_def) 729 apply simp 730 done 731 732lemma entry_refinement_C: 733 "\<lbrakk>all_invs' e s; (s, t) \<in> rf_sr; fp = False (* FIXME: fastpath *) \<rbrakk> 734 \<Longrightarrow> \<not> snd (kernelEntry_C fp e tc t) 735 \<and> (\<forall>tc' t'. (tc',t') \<in> fst (kernelEntry_C fp e tc t) 736 \<longrightarrow> (\<exists>s'. (tc', s') \<in> fst (kernelEntry e tc s) \<and> (s',t') \<in> rf_sr))" 737 using entry_corres_C [where e=e and fp=False] 738 by (fastforce simp add: corres_underlying_def) 739 740lemma ct_running'_C: 741 "\<lbrakk> (s, t) \<in> rf_sr; invs' s \<rbrakk> \<Longrightarrow> ct_running' s = ct_running_C t" 742 apply (simp add: ct_running_C_def Let_def ct_in_state'_def st_tcb_at'_def) 743 apply (clarsimp simp: rf_sr_def cstate_relation_def cpspace_relation_def Let_def) 744 apply (rule iffI) 745 apply (drule obj_at_ko_at') 746 apply clarsimp 747 apply (erule (1) cmap_relation_ko_atE) 748 apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) 749 apply clarsimp 750 apply (drule (1) cmap_relation_cs_atD [where addr_fun=tcb_ptr_to_ctcb_ptr]) 751 apply simp 752 apply clarsimp 753 apply (frule (1) map_to_ko_atI') 754 apply (erule obj_at'_weakenE) 755 apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) 756 apply (case_tac "tcbState ko", simp_all add: 757 ThreadState_Running_def 758 ThreadState_BlockedOnReceive_def 759 ThreadState_BlockedOnSend_def 760 ThreadState_BlockedOnReply_def 761 ThreadState_BlockedOnNotification_def 762 ThreadState_Inactive_def 763 ThreadState_IdleThreadState_def 764 ThreadState_Restart_def) 765 done 766 767lemma full_invs_both: 768 "ADT_H uop \<Turnstile> 769 {s'. \<exists>s. (s,s') \<in> lift_state_relation state_relation \<and> 770 s \<in> full_invs \<and> s' \<in> full_invs'}" 771 apply (rule fw_inv_transport) 772 apply (rule akernel_invariant) 773 apply (rule ckernel_invariant) 774 apply (rule fw_sim_A_H) 775 done 776end 777 778(* FIXME: move to somewhere sensible *) 779lemma dom_eq: 780 "dom um = dom um' \<longleftrightarrow> (\<forall>a. um a = None \<longleftrightarrow> um' a = None)" 781 apply (simp add: dom_def del: not_None_eq) 782 apply (rule iffI) 783 apply (rule allI) 784 apply (simp add: set_eq_iff) 785 apply (drule_tac x=a in spec) 786 apply auto 787done 788 789lemma dom_user_mem': 790 "dom (user_mem' s) = {p. typ_at' UserDataT (p && ~~ mask pageBits) s}" 791 by (clarsimp simp:user_mem'_def dom_def pointerInUserData_def split:if_splits) 792 793(* FIXME:move *) 794lemma dom_device_mem': 795 "dom (device_mem' s) = {p. typ_at' UserDataDeviceT (p && ~~ mask pageBits) s}" 796 by (clarsimp simp: device_mem'_def dom_def pointerInDeviceData_def split: if_splits) 797 798context kernel_m 799begin 800 801lemma user_memory_update_corres_C_helper: 802 "\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; 803 dom um \<subseteq> dom (user_mem' a)\<rbrakk> 804 \<Longrightarrow> (ksMachineState_update 805 (underlying_memory_update 806 (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m [p\<leftarrow>e. p \<in> dom um])) a, 807 b\<lparr>globals := globals b 808 \<lparr>t_hrs_' := 809 (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) 810 [p\<leftarrow>e. p \<in> dom um], 811 snd (t_hrs_' (globals b)))\<rparr>\<rparr>) 812 \<in> rf_sr" 813apply (induct e) 814 apply simp 815 apply (subgoal_tac 816 "ksMachineState_update (underlying_memory_update (\<lambda>m. m)) a = a") 817 apply (simp (no_asm_simp)) 818 apply simp 819apply (rename_tac x xs) 820apply (simp add: foldl_fun_upd_eq_foldr) 821apply (case_tac "x \<in> dom um", simp_all) 822apply (frule_tac ptr=x and b="the (um x)" in storeByteUser_rf_sr_upd) 823 apply simp 824 apply simp 825 apply (thin_tac "(x,y) : rf_sr" for x y)+ 826 apply (fastforce simp add: pointerInUserData_def dom_user_mem') 827apply (simp add: o_def hrs_mem_update_def) 828done 829 830lemma user_memory_update_corres_C: 831 "corres_underlying rf_sr False nf (%_ _. True) 832 (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom um \<subseteq> dom (user_mem' s)) 833 \<top> 834 (doMachineOp (user_memory_update um)) (setUserMem_C um)" 835 apply (clarsimp simp: corres_underlying_def) 836 apply (rule conjI) 837 prefer 2 838 apply (clarsimp simp add: setUserMem_C_def simpler_modify_def) 839 apply (subgoal_tac 840 "doMachineOp (user_memory_update um) a = 841 modify (ksMachineState_update (underlying_memory_update 842 (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m [p\<leftarrow>enum. p \<in> dom um]))) 843 a") 844 prefer 2 845 apply (clarsimp simp add: doMachineOp_def user_memory_update_def 846 simpler_modify_def simpler_gets_def select_f_def 847 NonDetMonad.bind_def return_def) 848 apply (thin_tac P for P)+ 849 apply (case_tac a, clarsimp) 850 apply (case_tac ksMachineState, clarsimp) 851 apply (rule ext) 852 apply (simp add: foldl_fun_upd_value dom_def split: option.splits) 853 apply clarsimp 854 apply (cut_tac s'=a and s="globals b" in user_mem_C_relation[symmetric]) 855 apply (simp add: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) 856 apply simp+ 857 apply (simp add: setUserMem_C_def_foldl) 858 apply (clarsimp simp add: simpler_modify_def) 859 apply (thin_tac "doMachineOp p s = x" for p s x) 860 apply (drule sym, simp) 861 apply (rule user_memory_update_corres_C_helper,auto)[1] 862 done 863 864lemma device_update_corres_C: 865 "corres_underlying rf_sr False nf (=) (\<lambda>_. True) (\<lambda>_. True) 866 (doMachineOp (device_memory_update ms)) 867 (setDeviceState_C ms)" 868 apply (clarsimp simp: corres_underlying_def) 869 apply (rule conjI) 870 prefer 2 871 apply (clarsimp simp add: setDeviceState_C_def simpler_modify_def) 872 apply (rule ballI) 873 apply (clarsimp simp: simpler_modify_def setDeviceState_C_def) 874 apply (clarsimp simp: doMachineOp_def device_memory_update_def NonDetMonad.bind_def in_monad 875 gets_def get_def return_def simpler_modify_def select_f_def) 876 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 877 cmachine_state_relation_def) 878 done 879 880lemma mem_dom_split: 881 "(dom um \<subseteq> dom (user_mem' s) \<union> dom (device_mem' s)) 882 \<Longrightarrow> um = restrict_map um (dom (user_mem' s)) ++ restrict_map um (dom (device_mem' s))" 883 apply (rule ext) 884 apply (auto simp: map_add_def restrict_map_def split:if_splits option.splits) 885 done 886 887lemma dom_if_rewrite: 888 "dom (\<lambda>x. if P x then Some (f x) else None) = dom (\<lambda>x. if P x then Some () else None)" 889 by (auto split:if_splits) 890 891crunch dmo_typ_at_pre_dom[wp]: doMachineOp "\<lambda>s. P (dom (\<lambda>x. if typ_at' T (x && ~~ mask pageBits) s then Some () else None))" 892 (wp: crunch_wps simp: crunch_simps device_mem'_def) 893 894lemma dmo_domain_device_mem'[wp]: 895 "\<lbrace>\<lambda>s. P (dom (device_mem' s))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (device_mem' sa))\<rbrace>" 896 apply (simp add:device_mem'_def pointerInDeviceData_def) 897 apply (rule hoare_pre) 898 apply (subst dom_if_rewrite) 899 apply (wp doMachineOp_typ_at') 900 apply (erule arg_cong[where f = P,THEN iffD1,rotated]) 901 apply (auto split:if_splits) 902 done 903 904lemma dmo_domain_user_mem'[wp]: 905 "\<lbrace>\<lambda>s. P (dom (user_mem' s))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (user_mem' sa))\<rbrace>" 906 apply (simp add:user_mem'_def pointerInUserData_def) 907 apply (rule hoare_pre) 908 apply (subst dom_if_rewrite) 909 apply (wp doMachineOp_typ_at') 910 apply (erule arg_cong[where f = P,THEN iffD1,rotated]) 911 apply (auto split:if_splits) 912 done 913 914lemma do_user_op_corres_C: 915 "corres_underlying rf_sr False False (=) (invs' and ex_abs einvs) \<top> 916 (doUserOp f tc) (doUserOp_C f tc)" 917 apply (simp only: doUserOp_C_def doUserOp_def split_def) 918 apply (rule corres_guard_imp) 919 apply (rule_tac P=\<top> and P'=\<top> and r'="(=)" in corres_split) 920 prefer 2 921 apply (clarsimp simp: simpler_gets_def getCurThread_def 922 corres_underlying_def rf_sr_def cstate_relation_def Let_def) 923 apply (rule_tac P=valid_state' and P'=\<top> and r'="(=)" in corres_split) 924 prefer 2 925 apply (clarsimp simp: cstate_to_A_def absKState_def 926 rf_sr_def cstate_to_H_correct ptable_lift_def) 927 apply (rule_tac P=valid_state' and P'=\<top> and r'="(=)" in corres_split) 928 prefer 2 929 apply (clarsimp simp: cstate_to_A_def absKState_def 930 rf_sr_def cstate_to_H_correct ptable_rights_def) 931 apply (rule_tac P=pspace_distinct' and P'=\<top> and r'="(=)" 932 in corres_split) 933 prefer 2 934 apply clarsimp 935 apply (rule fun_cong[where x=ptrFromPAddr]) 936 apply (rule_tac f=comp in arg_cong) 937 apply (rule user_mem_C_relation[symmetric]) 938 apply (simp add: rf_sr_def cstate_relation_def Let_def 939 cpspace_relation_def) 940 apply assumption 941 apply (rule_tac P=pspace_distinct' and P'=\<top> and r'="(=)" 942 in corres_split) 943 prefer 2 944 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 945 cpspace_relation_def) 946 apply (drule(1) device_mem_C_relation[symmetric]) 947 apply (simp add: comp_def) 948 apply (rule_tac P=valid_state' and P'=\<top> and r'="(=)" in corres_split) 949 prefer 2 950 apply (clarsimp simp: cstate_relation_def rf_sr_def 951 Let_def cmachine_state_relation_def) 952 apply (rule_tac P=\<top> and P'=\<top> and r'="(=)" in corres_split) 953 prefer 2 954 apply (clarsimp simp add: corres_underlying_def fail_def 955 assert_def return_def 956 split:if_splits) 957 apply simp 958 apply (rule_tac P=\<top> and P'=\<top> and r'="(=)" in corres_split) 959 prefer 2 960 apply (clarsimp simp add: corres_underlying_def fail_def 961 assert_def return_def 962 split:if_splits) 963 apply simp 964 apply (rule_tac r'="(=)" in corres_split[OF _ corres_select]) 965 prefer 2 966 apply clarsimp 967 apply simp 968 apply (rule corres_split[OF _ user_memory_update_corres_C]) 969 apply (rule corres_split[OF _ device_update_corres_C, 970 where R="\<top>\<top>" and R'="\<top>\<top>"]) 971 apply (wp select_wp | simp)+ 972 apply (intro conjI allI ballI impI) 973 apply ((clarsimp simp add: invs'_def valid_state'_def valid_pspace'_def)+)[5] 974 apply (clarsimp simp: ex_abs_def restrict_map_def 975 split: if_splits) 976 apply (drule ptable_rights_imp_UserData[rotated -1]) 977 apply fastforce+ 978 apply (clarsimp simp: invs'_def valid_state'_def user_mem'_def device_mem'_def 979 split: if_splits) 980 apply (drule_tac c = x in subsetD[where B = "dom S" for S]) 981 apply (simp add:dom_def) 982 apply fastforce 983 apply clarsimp 984 done 985 986lemma check_active_irq_corres_C: 987 "corres_underlying rf_sr False True (=) 988 (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) \<top> 989 (checkActiveIRQ) (checkActiveIRQ_C)" 990 apply (simp add: checkActiveIRQ_C_def checkActiveIRQ_def getActiveIRQ_C_def) 991 apply (rule corres_guard_imp) 992 apply (subst bind_assoc[symmetric]) 993 apply (rule corres_split) 994 apply simp 995 apply (rule ccorres_corres_u_xf) 996 apply (rule ccorres_rel_imp, rule ccorres_guard_imp) 997 apply (ctac add:getActiveIRQ_ccorres) 998 apply (rule TrueI) 999 apply (simp (no_asm)) 1000 apply (clarsimp simp: irqInvalid_def ucast_up_ucast_id 1001 is_up_def source_size_def target_size_def word_size 1002 split: option.splits ) 1003 apply (rule no_fail_dmo') 1004 apply (rule no_fail_getActiveIRQ) 1005 apply (rule hoare_TrueI)+ 1006 apply (wp|simp)+ 1007 done 1008 1009 1010lemma refinement2_both: 1011 "fp = False \<Longrightarrow> (* FIXME: fastpath *) 1012 \<lparr> Init = Init_C, Fin = Fin_C, 1013 Step = (\<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)) \<rparr> 1014 \<sqsubseteq> ADT_H uop" 1015 supply word_neq_0_conv[simp] 1016 apply (rule sim_imp_refines) 1017 apply (rule L_invariantI [where I\<^sub>c=UNIV and r="lift_state_relation rf_sr"]) 1018 apply (rule full_invs_both) 1019 apply simp 1020 apply (unfold LI_def) 1021 apply (rule conjI) 1022 apply (simp add: ADT_H_def) 1023 apply (blast intro!: init_refinement_C) 1024 apply (rule conjI) 1025 prefer 2 1026 apply (simp add: ADT_H_def) 1027 apply (clarsimp simp: Fin_C_def) 1028 apply (drule lift_state_relationD) 1029 apply (clarsimp simp: cstate_to_A_def) 1030 apply (subst cstate_to_H_correct) 1031 apply (fastforce simp: full_invs'_def invs'_def) 1032 apply (clarsimp simp: rf_sr_def) 1033 apply (simp add:absKState_def observable_memory_def absExst_def) 1034 apply (rule MachineTypes.machine_state.equality,simp_all)[1] 1035 apply (rule ext) 1036 apply (clarsimp simp: user_mem'_def option_to_0_def split:if_splits) 1037 apply (simp add: ADT_H_def) 1038 apply (clarsimp simp: rel_semi_def global_automaton_def relcomp_unfold 1039 in_lift_state_relation_eq) 1040 1041 apply (erule_tac P="a \<and> (\<exists>x. b x)" for a b in disjE) 1042 apply (clarsimp simp add: kernel_call_C_def kernel_call_H_def) 1043 apply (subgoal_tac "all_invs' x b") 1044 apply (drule_tac fp=fp and tc=af in entry_refinement_C, simp+) 1045 apply clarsimp 1046 apply (drule spec, drule spec, drule(1) mp) 1047 apply (clarsimp simp: full_invs'_def) 1048 apply (frule use_valid, rule kernelEntry_invs', 1049 simp add: sch_act_simple_def) 1050 apply (fastforce simp: ct_running'_C) 1051 apply (clarsimp simp: full_invs_def full_invs'_def all_invs'_def) 1052 apply fastforce 1053 1054 apply (erule_tac P="a \<and> b \<and> c \<and> d \<and> e" for a b c d e in disjE) 1055 apply (clarsimp simp add: do_user_op_C_def do_user_op_H_def monad_to_transition_def) 1056 apply (rule rev_mp, rule_tac f="uop" and tc=af in do_user_op_corres_C) 1057 apply (clarsimp simp: corres_underlying_def invs_def ex_abs_def) 1058 apply (fastforce simp: full_invs'_def ex_abs_def) 1059 1060 apply (erule_tac P="a \<and> b \<and> c \<and> (\<exists>x. e x)" for a b c d e in disjE) 1061 apply (clarsimp simp add: do_user_op_C_def do_user_op_H_def monad_to_transition_def) 1062 apply (rule rev_mp, rule_tac f="uop" and tc=af in do_user_op_corres_C) 1063 apply (clarsimp simp: corres_underlying_def invs_def ex_abs_def) 1064 apply (fastforce simp: full_invs'_def ex_abs_def) 1065 1066 apply (clarsimp simp: check_active_irq_C_def check_active_irq_H_def) 1067 apply (rule rev_mp, rule check_active_irq_corres_C) 1068 apply (fastforce simp: corres_underlying_def full_invs'_def ex_abs_def) 1069 done 1070 1071theorem refinement2: 1072 "ADT_C uop \<sqsubseteq> ADT_H uop" 1073 unfolding ADT_C_def 1074 by (rule refinement2_both) simp 1075 1076(* FIXME: fastpath 1077theorem fp_refinement: 1078 "ADT_FP_C uop \<sqsubseteq> ADT_H uop" 1079 unfolding ADT_FP_C_def 1080 by (rule refinement2_both) 1081*) 1082 1083theorem seL4_refinement: 1084 "ADT_C uop \<sqsubseteq> ADT_A uop" 1085 by (blast intro: refinement refinement2 refinement_trans) 1086 1087(* FIXME: fastpath 1088theorem seL4_fastpath_refinement: 1089 "ADT_FP_C uop \<sqsubseteq> ADT_A uop" 1090 by (blast intro: refinement fp_refinement refinement_trans) 1091*) 1092 1093lemma exec_C_Basic: 1094 "exec_C Gamma (Basic f) = (modify f)" 1095 apply (rule ext) 1096 apply (simp add: exec_C_def simpler_modify_def) 1097 apply (auto elim: exec.cases intro: exec.intros) 1098 done 1099 1100lemma in_monad_imp_rewriteE: 1101 "\<lbrakk> (a, b) \<in> fst (f' s); monadic_rewrite F False \<top> f f'; F \<longrightarrow> \<not> snd (f s) \<rbrakk> 1102 \<Longrightarrow> (a, b) \<in> fst (f s)" 1103 by (auto simp add: monadic_rewrite_def) 1104 1105lemma ccorres_underlying_Fault: 1106 "\<lbrakk> ccorres_underlying srel Gamma rrefl xf arrel axf G G' hs m c; 1107 \<exists>s. (s, s') \<in> srel \<and> G s \<and> s' \<in> G' \<and> \<not> snd (m s) \<rbrakk> 1108 \<Longrightarrow> \<not> Gamma \<turnstile> \<langle>c, Normal s'\<rangle> \<Rightarrow> Fault ft" 1109 apply clarsimp 1110 apply (erule(4) ccorresE) 1111 apply (erule exec_handlers.EHOther) 1112 apply simp 1113 apply simp 1114 done 1115 1116lemma monadic_rewrite_\<Gamma>: 1117 "monadic_rewrite True False \<top> 1118 (exec_C \<Gamma> c) 1119 (exec_C (kernel_all_global_addresses.\<Gamma> symbol_table) c)" 1120 using spec_refine [of symbol_table domain] 1121 using spec_simulates_to_exec_simulates 1122 apply (clarsimp simp: spec_statefn_simulates_via_statefn 1123 o_def map_option_case monadic_rewrite_def exec_C_def 1124 split: option.splits 1125 cong: option.case_cong) 1126 apply blast 1127 done 1128 1129lemma no_fail_getActiveIRQ_C: 1130 "\<not>snd (getActiveIRQ_C s)" 1131 apply (clarsimp simp: getActiveIRQ_C_def exec_C_def) 1132 apply (drule getActiveIRQ_Normal) 1133 apply (clarsimp simp: isNormal_def) 1134 done 1135 1136lemma kernel_all_subset_kernel: 1137 "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) 1138 (kernel_global.kernel_call_C symbol_table fp) 1139 \<subseteq> global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)" 1140 apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def 1141 relcomp_unfold in_lift_state_relation_eq) 1142 apply (intro conjI) 1143 apply (simp_all add: kernel_global.kernel_call_C_def 1144 kernel_call_C_def kernelEntry_C_def 1145 setTCBContext_C_def 1146 kernel_global.kernelEntry_C_def 1147 exec_C_Basic 1148 kernel_global.setTCBContext_C_def 1149 kernel_call_H_def kernelEntry_def 1150 getContext_C_def 1151 check_active_irq_C_def checkActiveIRQ_C_def 1152 kernel_global.check_active_irq_C_def kernel_global.checkActiveIRQ_C_def 1153 check_active_irq_H_def checkActiveIRQ_def) 1154 apply clarsimp 1155 apply (erule in_monad_imp_rewriteE[where F=True]) 1156 apply (rule monadic_rewrite_imp) 1157 apply (rule monadic_rewrite_bind_tail)+ 1158 apply (rule monadic_rewrite_bind_head[where P=\<top>]) 1159 apply (simp add: callKernel_C_def callKernel_withFastpath_C_def 1160 kernel_global.callKernel_C_def 1161 kernel_global.callKernel_withFastpath_C_def 1162 handleHypervisorEvent_C_def 1163 split: event.split if_split) 1164 apply (intro allI impI conjI monadic_rewrite_\<Gamma>)[1] 1165 apply ((wp | simp)+)[3] 1166 apply (clarsimp simp: snd_bind snd_modify in_monad gets_def) 1167 apply clarsimp 1168 apply clarsimp 1169 apply clarsimp 1170 apply (clarsimp simp: in_monad) 1171 apply (erule (1) notE[OF _ in_monad_imp_rewriteE[where F=True]]) 1172 apply (simp add: kernel_global.getActiveIRQ_C_def getActiveIRQ_C_def) 1173 apply (rule monadic_rewrite_\<Gamma>) 1174 apply (simp add: no_fail_getActiveIRQ_C) 1175 apply (clarsimp simp: in_monad) 1176 apply (erule (1) notE[OF _ in_monad_imp_rewriteE[where F=True]]) 1177 apply (simp add: kernel_global.getActiveIRQ_C_def getActiveIRQ_C_def) 1178 apply (rule monadic_rewrite_\<Gamma>) 1179 apply (simp add: no_fail_getActiveIRQ_C) 1180 apply (clarsimp simp: in_monad) 1181 apply (erule (1) notE[OF _ in_monad_imp_rewriteE[where F=True]]) 1182 apply (simp add: kernel_global.getActiveIRQ_C_def getActiveIRQ_C_def) 1183 apply (rule monadic_rewrite_\<Gamma>) 1184 apply (simp add: no_fail_getActiveIRQ_C) 1185 done 1186 1187theorem true_refinement: 1188 "kernel_global.ADT_C symbol_table x64KSKernelVSpace_C uop 1189 \<sqsubseteq> ADT_H uop" 1190 apply (rule refinement_trans[OF _ refinement2]) 1191 apply (simp add: kernel_global.ADT_C_def ADT_C_def) 1192 apply (rule sim_imp_refines) 1193 apply (clarsimp simp: fw_simulates_def) 1194 apply (rule_tac x=Id in exI) 1195 using kernel_all_subset_kernel 1196 apply (simp add: fw_sim_def rel_semi_def) 1197 done 1198 1199(* FIXME: fastpath 1200theorem true_fp_refinement: 1201 "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop 1202 \<sqsubseteq> ADT_H uop" 1203 apply (rule refinement_trans[OF _ fp_refinement]) 1204 apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def) 1205 apply (rule sim_imp_refines) 1206 apply (clarsimp simp: fw_simulates_def) 1207 apply (rule_tac x=Id in exI) 1208 using kernel_all_subset_kernel 1209 apply (simp add: fw_sim_def rel_semi_def) 1210 done 1211*) 1212 1213end 1214 1215end 1216