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 Tcb_C 12imports Delete_C Ipc_C 13begin 14 15lemma asUser_obj_at' : 16 "\<lbrace> K(t\<noteq>t') and obj_at' P t' \<rbrace> asUser t f \<lbrace> \<lambda>_. obj_at' (P::Structures_H.tcb \<Rightarrow> bool) t' \<rbrace>" 17 including no_pre 18 apply (wpsimp wp: hoare_vcg_ball_lift threadGet_wp simp: split_def asUser_def) 19 by (drule obj_at_ko_at', fastforce) 20 21lemma getObject_sched: 22 "(x::tcb, s') \<in> fst (getObject t s) \<Longrightarrow> 23 (x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" 24 apply (clarsimp simp: in_monad getObject_def split_def loadObject_default_def 25 magnitudeCheck_def projectKOs 26 split: option.splits) 27 done 28 29lemma threadGet_sched: 30 "(x, s') \<in> fst (threadGet t f s) \<Longrightarrow> 31 (x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadGet t f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" 32 apply (clarsimp simp: in_monad threadGet_def liftM_def) 33 apply (drule getObject_sched) 34 apply fastforce 35 done 36 37lemma setObject_sched: 38 "(x, s') \<in> fst (setObject t (v::tcb) s) \<Longrightarrow> 39 (x, s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (setObject t v (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" 40 apply (clarsimp simp: in_monad setObject_def split_def updateObject_default_def 41 magnitudeCheck_def projectKOs 42 split: option.splits) 43 done 44 45lemma threadSet_sched: 46 "(x, s') \<in> fst (threadSet f t s) \<Longrightarrow> 47 (x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadSet f t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" 48 apply (clarsimp simp: in_monad threadSet_def) 49 apply (drule getObject_sched) 50 apply (drule setObject_sched) 51 apply fastforce 52 done 53 54lemma asUser_sched: 55 "(rv,s') \<in> fst (asUser t f s) \<Longrightarrow> 56 (rv,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (asUser t f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" 57 apply (clarsimp simp: asUser_def split_def in_monad select_f_def) 58 apply (drule threadGet_sched) 59 apply (drule threadSet_sched) 60 apply fastforce 61 done 62 63lemma doMachineOp_sched: 64 "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow> 65 (rv,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (doMachineOp f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" 66 apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def) 67 apply fastforce 68 done 69 70context begin interpretation Arch . (*FIXME: arch_split*) 71crunch queues[wp]: setupReplyMaster "valid_queues" 72 (simp: crunch_simps wp: crunch_wps) 73 74crunch curThread [wp]: restart "\<lambda>s. P (ksCurThread s)" 75 (wp: crunch_wps simp: crunch_simps) 76end 77 78context kernel_m 79begin 80 81lemma getMRs_rel_sched: 82 "\<lbrakk> getMRs_rel args buffer s; 83 (cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer) s \<rbrakk> 84 \<Longrightarrow> getMRs_rel args buffer (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)" 85 apply (clarsimp simp: getMRs_rel_def) 86 apply (rule exI, rule conjI, assumption) 87 apply (subst det_wp_use, rule det_wp_getMRs) 88 apply (simp add: cur_tcb'_def split: option.splits) 89 apply (simp add: valid_ipc_buffer_ptr'_def) 90 apply (subst (asm) det_wp_use, rule det_wp_getMRs) 91 apply (simp add: cur_tcb'_def) 92 apply (clarsimp simp: getMRs_def in_monad) 93 apply (drule asUser_sched) 94 apply (intro exI) 95 apply (erule conjI) 96 apply (cases buffer) 97 apply (simp add: return_def) 98 apply clarsimp 99 apply (drule mapM_upd [rotated]) 100 prefer 2 101 apply fastforce 102 apply (clarsimp simp: loadWordUser_def in_monad stateAssert_def word_size) 103 apply (erule doMachineOp_sched) 104 done 105 106lemma getObject_state: 107 " \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> 108 \<Longrightarrow> (if t = t' then tcbState_update (\<lambda>_. st) x else x, 109 s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) 110 \<in> fst (getObject t' (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))" 111 apply (simp split: if_split) 112 apply (rule conjI) 113 apply clarsimp 114 apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad 115 Corres_C.in_magnitude_check' projectKOs objBits_simps') 116 apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps) 117 apply (simp add: magnitudeCheck_def in_monad split: option.splits) 118 apply clarsimp 119 apply (simp add: lookupAround2_char2) 120 apply (clarsimp split: if_split_asm) 121 apply (erule_tac x=x2 in allE) 122 apply (clarsimp simp: ps_clear_def) 123 apply (drule_tac x=x2 in orthD2) 124 apply fastforce 125 apply clarsimp 126 apply (erule impE) 127 apply simp 128 apply (erule notE, rule word_diff_ls'(3)) 129 apply unat_arith 130 apply (drule is_aligned_no_overflow, simp add: word_bits_def) 131 apply clarsimp 132 apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad 133 Corres_C.in_magnitude_check' projectKOs objBits_simps') 134 apply (simp add: magnitudeCheck_def in_monad split: option.splits) 135 apply clarsimp 136 apply (simp add: lookupAround2_char2) 137 apply (clarsimp split: if_split_asm) 138 apply (erule_tac x=t in allE) 139 apply simp 140 apply (clarsimp simp: obj_at'_real_def projectKOs 141 ko_wp_at'_def objBits_simps) 142 apply (simp add: ps_clear_def) 143 apply (drule_tac x=t in orthD2) 144 apply fastforce 145 apply clarsimp 146 apply (erule impE) 147 apply simp 148 apply (erule notE, rule word_diff_ls'(3)) 149 apply unat_arith 150 apply (drule is_aligned_no_overflow) 151 apply simp 152 apply (erule_tac x=x2 in allE) 153 apply (clarsimp simp: ps_clear_def) 154 apply (drule_tac x=x2 in orthD2) 155 apply fastforce 156 apply clarsimp 157 apply (erule impE) 158 apply (rule word_diff_ls'(3)) 159 apply unat_arith 160 apply (drule is_aligned_no_overflow) 161 apply simp 162 apply fastforce 163 done 164 165 166lemma threadGet_state: 167 "\<lbrakk> (uc, s') \<in> fst (threadGet (atcbContextGet o tcbArch) t' s); ko_at' ko t s \<rbrakk> \<Longrightarrow> 168 (uc, s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> 169 fst (threadGet (atcbContextGet o tcbArch) t' (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))" 170 apply (clarsimp simp: threadGet_def liftM_def in_monad) 171 apply (drule (1) getObject_state [where st=st]) 172 apply (rule exI) 173 apply (erule conjI) 174 apply (simp split: if_splits) 175 done 176 177lemma asUser_state: 178 "\<lbrakk>(x,s) \<in> fst (asUser t' f s); ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace> \<rbrakk> \<Longrightarrow> 179 (x,s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> 180 fst (asUser t' f (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))" 181 apply (clarsimp simp: asUser_def in_monad select_f_def) 182 apply (frule use_valid, rule threadGet_inv [where P="(=) s"], rule refl) 183 apply (frule use_valid, assumption, rule refl) 184 apply clarsimp 185 apply (frule (1) threadGet_state) 186 apply (intro exI) 187 apply (erule conjI) 188 apply (rule exI, erule conjI) 189 apply (clarsimp simp: threadSet_def in_monad) 190 apply (frule use_valid, rule getObject_inv [where P="(=) s"]) 191 apply (simp add: loadObject_default_def) 192 apply wp 193 apply simp 194 apply (rule refl) 195 apply clarsimp 196 apply (frule (1) getObject_state) 197 apply (intro exI) 198 apply (erule conjI) 199 apply (clarsimp simp: setObject_def split_def updateObject_default_def threadGet_def 200 in_magnitude_check' getObject_def loadObject_default_def liftM_def 201 objBits_simps' projectKOs in_monad) 202 apply (simp split: if_split) 203 apply (rule conjI) 204 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) 205 apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits) 206 apply (rule conjI) 207 apply clarsimp 208 apply (cases s, simp) 209 apply (rule ext) 210 apply (clarsimp split: if_split) 211 apply (cases ko) 212 apply clarsimp 213 apply clarsimp 214 apply (rule conjI) 215 apply (clarsimp simp add: lookupAround2_char2 split: if_split_asm) 216 apply (erule_tac x=x2 in allE) 217 apply simp 218 apply (simp add: ps_clear_def) 219 apply (drule_tac x=x2 in orthD2) 220 apply fastforce 221 apply clarsimp 222 apply (erule impE, simp) 223 apply (erule notE, rule word_diff_ls'(3)) 224 apply unat_arith 225 apply (drule is_aligned_no_overflow) 226 apply simp 227 apply (rule exI) 228 apply (rule conjI, fastforce) 229 apply clarsimp 230 apply (cases s, clarsimp) 231 apply (rule ext, clarsimp split: if_split) 232 apply (cases ko, clarsimp) 233 apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits) 234 apply (rule conjI) 235 apply clarsimp 236 apply (cases s, clarsimp) 237 apply (rule ext, clarsimp split: if_split) 238 apply (case_tac tcb, clarsimp) 239 apply clarsimp 240 apply (rule conjI) 241 apply (clarsimp simp add: lookupAround2_char2 split: if_split_asm) 242 apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps) 243 apply (erule_tac x=t in allE) 244 apply simp 245 apply (simp add: ps_clear_def) 246 apply (drule_tac x=t in orthD2) 247 apply fastforce 248 apply clarsimp 249 apply (erule impE, simp) 250 apply (erule notE, rule word_diff_ls'(3)) 251 apply unat_arith 252 apply (drule is_aligned_no_overflow) 253 apply simp 254 apply (erule_tac x=x2 in allE) 255 apply simp 256 apply (simp add: ps_clear_def) 257 apply (drule_tac x=x2 in orthD2) 258 apply fastforce 259 apply clarsimp 260 apply (erule impE) 261 apply (rule word_diff_ls'(3)) 262 apply unat_arith 263 apply (drule is_aligned_no_overflow) 264 apply simp 265 apply (erule impE, simp) 266 apply simp 267 apply (rule exI) 268 apply (rule conjI, fastforce) 269 apply clarsimp 270 apply (cases s, clarsimp) 271 apply (rule ext, clarsimp split: if_split) 272 apply (case_tac tcb, clarsimp) 273 done 274 275lemma doMachineOp_state: 276 "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow> 277 (rv,s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) 278 \<in> fst (doMachineOp f (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))" 279 apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def) 280 apply fastforce 281 done 282 283lemma mapM_upd_inv: 284 assumes f: "\<And>x rv. (rv,s) \<in> fst (f x s) \<Longrightarrow> x \<in> set xs \<Longrightarrow> (rv, g s) \<in> fst (f x (g s))" 285 assumes inv: "\<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>" 286 shows "(rv,s) \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s))" 287 using f inv 288proof (induct xs arbitrary: rv s) 289 case Nil 290 thus ?case by (simp add: mapM_Nil return_def) 291next 292 case (Cons z zs) 293 from Cons.prems 294 show ?case 295 apply (clarsimp simp: mapM_Cons in_monad) 296 apply (frule use_valid, assumption, rule refl) 297 apply clarsimp 298 apply (drule Cons.prems, simp) 299 apply (rule exI, erule conjI) 300 apply (drule Cons.hyps) 301 apply simp 302 apply assumption 303 apply simp 304 done 305qed 306 307lemma getMRs_rel_state: 308 "\<lbrakk>getMRs_rel args buffer s; 309 (cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer) s; 310 ko_at' ko t s \<rbrakk> \<Longrightarrow> 311 getMRs_rel args buffer (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)" 312 apply (clarsimp simp: getMRs_rel_def) 313 apply (rule exI, erule conjI) 314 apply (subst (asm) det_wp_use, rule det_wp_getMRs) 315 apply (simp add: cur_tcb'_def) 316 apply (subst det_wp_use, rule det_wp_getMRs) 317 apply (simp add: cur_tcb'_def) 318 apply (rule conjI) 319 apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs 320 objBits_simps ps_clear_def split: if_split) 321 apply (clarsimp simp: valid_ipc_buffer_ptr'_def split: option.splits) 322 apply (clarsimp simp: typ_at'_def ko_wp_at'_def projectKOs obj_at'_real_def 323 objBits_simps ps_clear_def split: if_split) 324 apply (clarsimp simp: getMRs_def in_monad) 325 apply (frule use_valid, rule asUser_inv [where P="(=) s"]) 326 apply (wp mapM_wp' getRegister_inv)[1] 327 apply simp 328 apply clarsimp 329 apply (drule (1) asUser_state) 330 apply (wp mapM_wp' getRegister_inv)[1] 331 apply (intro exI) 332 apply (erule conjI) 333 apply (cases buffer) 334 apply (clarsimp simp: return_def) 335 apply clarsimp 336 apply (drule mapM_upd_inv [rotated -1]) 337 prefer 3 338 apply fastforce 339 prefer 2 340 apply wp 341 apply (clarsimp simp: loadWordUser_def in_monad stateAssert_def word_size 342 simp del: fun_upd_apply) 343 apply (rule conjI) 344 apply (clarsimp simp: pointerInUserData_def typ_at'_def ko_wp_at'_def 345 projectKOs ps_clear_def obj_at'_real_def 346 split: if_split) 347 apply (erule doMachineOp_state) 348 done 349 350(* FIXME: move *) 351lemma setTCB_cur: 352 "\<lbrace>cur_tcb'\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>_. cur_tcb'\<rbrace>" 353 including no_pre 354 apply (wp cur_tcb_lift) 355 apply (simp add: setObject_def split_def updateObject_default_def) 356 apply wp 357 apply simp 358 done 359 360lemma setThreadState_getMRs_rel: 361 "\<lbrace>getMRs_rel args buffer and cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer 362 and (\<lambda>_. runnable' st)\<rbrace> 363 setThreadState st t \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace>" 364 apply (rule hoare_gen_asm') 365 apply (simp add: setThreadState_runnable_simp) 366 apply (simp add: threadSet_def) 367 apply wp 368 apply (simp add: setObject_def split_def updateObject_default_def) 369 apply wp 370 apply (simp del: fun_upd_apply) 371 apply (wp getObject_tcb_wp) 372 apply (clarsimp simp del: fun_upd_apply) 373 apply (drule obj_at_ko_at')+ 374 apply (clarsimp simp del: fun_upd_apply) 375 apply (rule exI, rule conjI, assumption) 376 apply (clarsimp split: if_split simp del: fun_upd_apply) 377 apply (simp add: getMRs_rel_state) 378 done 379 380lemma setThreadState_sysargs_rel: 381 "\<lbrace>sysargs_rel args buffer and (\<lambda>_. runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. sysargs_rel args buffer\<rbrace>" 382 apply (cases buffer, simp_all add: sysargs_rel_def) 383 apply (rule hoare_pre) 384 apply (wp setThreadState_getMRs_rel hoare_valid_ipc_buffer_ptr_typ_at'|simp)+ 385 done 386 387lemma ccorres_abstract_known: 388 "\<lbrakk> \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val) \<rbrakk> 389 \<Longrightarrow> ccorres rvr xf P (P' \<inter> {s. xf' s = val}) hs f g" 390 apply (rule ccorres_guard_imp2) 391 apply (rule_tac xf'=xf' in ccorres_abstract) 392 apply assumption 393 apply (rule_tac P="rv' = val" in ccorres_gen_asm2) 394 apply simp 395 apply simp 396 done 397 398lemma distinct_remove1_filter: 399 "distinct xs \<Longrightarrow> remove1 v xs = [x\<leftarrow>xs. x \<noteq> v]" 400 apply (induct xs) 401 apply simp 402 apply (clarsimp split: if_split) 403 apply (rule sym, simp add: filter_id_conv) 404 apply clarsimp 405 done 406 407lemma hrs_mem_update_cong: 408 "\<lbrakk> \<And>x. f x = f' x \<rbrakk> \<Longrightarrow> hrs_mem_update f = hrs_mem_update f'" 409 by (simp add: hrs_mem_update_def) 410 411lemma setPriority_ccorres: 412 "ccorres dc xfdc 413 (invs' and tcb_at' t and (\<lambda>s. priority \<le> maxPriority)) 414 (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. prio_' s = ucast priority}) 415 [] (setPriority t priority) (Call setPriority_'proc)" 416 apply (rule ccorres_gen_asm) 417 apply (cinit lift: tptr_' prio_') 418 apply (ctac(no_vcg) add: tcbSchedDequeue_ccorres) 419 apply (rule ccorres_move_c_guard_tcb) 420 apply (rule ccorres_split_nothrow_novcg_dc) 421 apply (rule threadSet_ccorres_lemma2[where P=\<top>]) 422 apply vcg 423 apply clarsimp 424 apply (erule(1) rf_sr_tcb_update_no_queue2, 425 (simp add: typ_heap_simps')+, simp_all?)[1] 426 apply (rule ball_tcb_cte_casesI, simp+) 427 apply (simp add: ctcb_relation_def cast_simps) 428 apply (ctac(no_vcg) add: isRunnable_ccorres) 429 apply (simp add: when_def to_bool_def del: Collect_const) 430 apply (rule ccorres_cond2[where R=\<top>], simp add: Collect_const_mem) 431 apply (ctac add: tcbSchedEnqueue_ccorres) 432 apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def]) 433 apply wp 434 apply vcg 435 apply (rule ccorres_return_Skip') 436 apply (wp isRunnable_wp) 437 apply clarsimp 438 apply (wp hoare_drop_imps threadSet_valid_queues threadSet_valid_objs' 439 weak_sch_act_wf_lift_linear threadSet_pred_tcb_at_state) 440 apply (clarsimp simp: st_tcb_at'_def o_def split: if_splits) 441 apply (wpsimp wp: threadSet_tcbDomain_triv) 442 apply (wp threadSet_valid_objs') 443 apply (simp add: guard_is_UNIV_def) 444 apply (rule hoare_strengthen_post[where Q="\<lambda>rv s. 445 obj_at' (\<lambda>_. True) t s \<and> 446 Invariants_H.valid_queues s \<and> 447 valid_objs' s \<and> 448 weak_sch_act_wf (ksSchedulerAction s) s \<and> 449 (\<forall>d p. \<not> t \<in> set (ksReadyQueues s (d, p)))"]) 450 apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues tcbSchedDequeue_nonq) 451 apply (clarsimp simp: valid_tcb'_tcbPriority_update) 452 apply (fastforce simp: invs'_def valid_state'_def 453 valid_objs'_maxDomain valid_objs'_maxPriority) 454 done 455 456lemma setMCPriority_ccorres: 457 "ccorres dc xfdc 458 (invs' and tcb_at' t and (\<lambda>s. priority \<le> maxPriority)) 459 (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. mcp_' s = ucast priority}) 460 [] (setMCPriority t priority) (Call setMCPriority_'proc)" 461 apply (rule ccorres_gen_asm) 462 apply (cinit lift: tptr_' mcp_') 463 apply (rule ccorres_move_c_guard_tcb) 464 apply (rule threadSet_ccorres_lemma2[where P=\<top>]) 465 apply vcg 466 apply clarsimp 467 apply (erule(1) rf_sr_tcb_update_no_queue2, 468 (simp add: typ_heap_simps')+)[1] 469 apply (rule ball_tcb_cte_casesI, simp+) 470 apply (simp add: ctcb_relation_def cast_simps) 471 apply (clarsimp simp: down_cast_same [symmetric] ucast_up_ucast is_up is_down) 472 done 473 474lemma ccorres_subgoal_tailE: 475 "\<lbrakk> ccorres rvr xf Q Q' hs (b ()) d; 476 ccorres rvr xf Q Q' hs (b ()) d \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d) \<rbrakk> 477 \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d)" 478 by simp 479 480lemma checkCapAt_ccorres: 481 "\<lbrakk> \<And>rv' t t'. ceqv \<Gamma> ret__unsigned_long_' rv' t t' c (c' rv'); 482 ccorres rvr xf P P' hs (f >>= g) (c' (scast true)); 483 ccorres rvr xf Q Q' hs (g ()) (c' (scast false)); 484 guard_is_UNIV dc xfdc (\<lambda>_ _. P' \<inter> Q') \<rbrakk> 485 \<Longrightarrow> ccorres rvr xf (invs' and valid_cap' cap and P and Q) 486 (UNIV \<inter> {s. ccap_relation cap cap'} \<inter> {s. slot' = cte_Ptr slot}) hs 487 (checkCapAt cap slot f >>= g) 488 (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t slot'\<rbrace> 489 (\<acute>ret__unsigned_long :== CALL sameObjectAs(cap', 490 h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))));;c)" 491 apply (rule ccorres_gen_asm2)+ 492 apply (simp add: checkCapAt_def liftM_def bind_assoc del: Collect_const) 493 apply (rule ccorres_symb_exec_l' [OF _ getCTE_inv getCTE_sp empty_fail_getCTE]) 494 apply (rule ccorres_guard_imp2) 495 apply (rule ccorres_move_c_guard_cte) 496 apply (rule_tac xf'=ret__unsigned_long_' and val="from_bool (sameObjectAs cap (cteCap x))" 497 and R="cte_wp_at' ((=) x) slot and valid_cap' cap and invs'" 498 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 499 apply vcg 500 apply (clarsimp simp: cte_wp_at_ctes_of) 501 apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) 502 apply (rule exI, rule conjI, assumption) 503 apply (clarsimp simp: typ_heap_simps dest!: ccte_relation_ccap_relation) 504 apply (rule exI, rule conjI, assumption) 505 apply (auto intro: valid_capAligned dest: ctes_of_valid')[1] 506 apply assumption 507 apply (simp only: when_def if_to_top_of_bind) 508 apply (rule ccorres_if_lhs) 509 apply (simp add: from_bool_def true_def) 510 apply (simp add: from_bool_def false_def) 511 apply (simp add: guard_is_UNIV_def) 512 apply (clarsimp simp: cte_wp_at_ctes_of) 513 done 514 515lemmas checkCapAt_ccorres2 516 = checkCapAt_ccorres[where g=return, simplified bind_return] 517 518lemma invs_psp_aligned_strg': 519 "invs' s \<longrightarrow> pspace_aligned' s" 520 by clarsimp 521 522lemma cte_is_derived_capMasterCap_strg: 523 "cte_wp_at' (is_derived' (ctes_of s) ptr cap \<circ> cteCap) ptr s 524 \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> P) ptr s" 525 by (clarsimp simp: cte_wp_at_ctes_of is_derived'_def 526 badge_derived'_def) 527 528lemma cteInsert_cap_to'2: 529 "\<lbrace>ex_nonz_cap_to' p\<rbrace> 530 cteInsert newCap srcSlot destSlot 531 \<lbrace>\<lambda>_. ex_nonz_cap_to' p\<rbrace>" 532 apply (simp add: cteInsert_def ex_nonz_cap_to'_def setUntypedCapAsFull_def) 533 apply (rule hoare_vcg_ex_lift) 534 apply (wp updateMDB_weak_cte_wp_at 535 updateCap_cte_wp_at_cases getCTE_wp' static_imp_wp) 536 apply (clarsimp simp: cte_wp_at_ctes_of) 537 apply auto 538 done 539 540lemma why_oh_why:" (if \<exists>a b. snd (the buf) = Some (a, b) 541 then P (snd (the buf)) else Q) = 542 (case the buf of (ptr, None) \<Rightarrow> Q | (ptr, Some (cap, slot)) \<Rightarrow> P (Some (cap, slot)))" 543 by (clarsimp simp: split_def case_option_If2) 544 545lemma shouldnt_need_this: "(case buf of None \<Rightarrow> Q 546 | Some (ptr, None) \<Rightarrow> Q 547 | Some (ptr, Some (cap, slot)) \<Rightarrow> P cap slot) = 548 (if \<exists>a b. buf = Some (a, b) then case the buf of (ptr, None) \<Rightarrow> Q 549 | (ptr, Some (cap, slot)) \<Rightarrow> P cap slot 550 else Q)" 551 by (simp add: case_option_If2) 552 553lemma archSetIPCBuffer_ccorres: 554 "ccorres dc xfdc \<top> (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr target} \<inter> {s. bufferAddr_' s = buf}) [] 555 (asUser target $ setTCBIPCBuffer buf) 556 (Call Arch_setTCBIPCBuffer_'proc)" 557 apply (cinit lift: thread_' bufferAddr_') 558 apply (simp add: setTCBIPCBuffer_def) 559 apply (subst submonad_asUser.return) 560 apply (rule ccorres_stateAssert) 561 apply (rule ccorres_return_Skip') 562 apply simp 563 done 564 565lemma threadSet_ipcbuffer_invs: 566 "is_aligned a msg_align_bits \<Longrightarrow> 567 \<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbIPCBuffer_update (\<lambda>_. a)) t \<lbrace>\<lambda>rv. invs'\<rbrace>" 568 apply (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong) 569 done 570 571lemma canonical_address_bitfield_extract_tcb: 572 "\<lbrakk>canonical_address t; is_aligned t tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 573 t = ctcb_ptr_to_tcb_ptr (tcb_Ptr (sign_extend 47 (ptr_val (tcb_ptr_to_ctcb_ptr t))))" 574 apply (drule (1) canonical_address_tcb_ptr) 575 by (fastforce simp: sign_extended_iff_sign_extend canonical_address_sign_extended) 576 577lemma invokeTCB_ThreadControl_ccorres: 578 notes prod.case_cong_weak[cong] 579 shows 580 "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') 581 (invs' and sch_act_simple 582 and tcb_inv_wf' (ThreadControl target slot faultep mcp priority cRoot vRoot buf) 583 and (\<lambda>_. (faultep = None) = (cRoot = None) \<and> (cRoot = None) = (vRoot = None) 584 \<and> (case buf of Some (ptr, Some (cap, slot)) \<Rightarrow> slot \<noteq> 0 | _ \<Rightarrow> True))) 585 (UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr target} 586 \<inter> {s. (cRoot \<noteq> None \<or> buf \<noteq> None) \<longrightarrow> slot_' s = cte_Ptr slot} 587 \<inter> {s. faultep_' s = option_to_0 faultep} 588 \<inter> {s. mcp_' s = case_option 0 (ucast o fst) mcp} 589 \<inter> {s. priority_' s = case_option 0 (ucast o fst) priority} 590 \<inter> {s. case cRoot of None \<Rightarrow> True | Some (cRootCap, cRootSlot) \<Rightarrow> ccap_relation cRootCap (cRoot_newCap_' s)} 591 \<inter> {s. cRoot_srcSlot_' s = cte_Ptr (option_to_0 (option_map snd cRoot))} 592 \<inter> {s. case vRoot of None \<Rightarrow> True | Some (vRootCap, vRootSlot) \<Rightarrow> ccap_relation vRootCap (vRoot_newCap_' s)} 593 \<inter> {s. vRoot_srcSlot_' s = cte_Ptr (option_to_0 (option_map snd vRoot))} 594 \<inter> {s. bufferAddr_' s = option_to_0 (option_map fst buf)} 595 \<inter> {s. bufferSrcSlot_' s = cte_Ptr (case buf of Some (ptr, Some (cap, slot)) \<Rightarrow> slot | _ \<Rightarrow> 0)} 596 \<inter> {s. case buf of Some (ptr, Some (cap, slot)) \<Rightarrow> ccap_relation cap (bufferCap_' s) | _ \<Rightarrow> True} 597 \<inter> {s. updateFlags_' s = (if mcp \<noteq> None then scast thread_control_update_mcp else 0) 598 || (if priority \<noteq> None then scast thread_control_update_priority else 0) 599 || (if buf \<noteq> None then scast thread_control_update_ipc_buffer else 0) 600 || (if cRoot \<noteq> None then scast thread_control_update_space else 0)}) 601 [] 602 (invokeTCB (ThreadControl target slot faultep mcp priority cRoot vRoot buf)) 603 (Call invokeTCB_ThreadControl_'proc)" 604 (is "ccorres ?rvr ?xf (?P and (\<lambda>_. ?P')) ?Q [] ?af ?cf") 605 apply (rule ccorres_gen_asm) using [[goals_limit=1]] 606 apply (cinit lift: target_' slot_' faultep_' mcp_' priority_' cRoot_newCap_' cRoot_srcSlot_' 607 vRoot_newCap_' vRoot_srcSlot_' bufferAddr_' bufferSrcSlot_' bufferCap_' 608 updateFlags_') 609 apply csymbr 610 apply(simp add: liftE_bindE thread_control_flag_defs case_option_If2 611 word_ao_dist if_and_helper if_n_0_0 fun_app_def 612 tcb_cnode_index_defs[THEN ptr_add_assertion_positive[OF ptr_add_assertion_positive_helper]] 613 del: Collect_const cong add: call_ignore_cong if_cong) 614 apply (rule_tac P="ptr_val (tcb_ptr_to_ctcb_ptr target) && ~~ mask 5 615 = ptr_val (tcb_ptr_to_ctcb_ptr target) 616 \<and> ptr_val (tcb_ptr_to_ctcb_ptr target) && ~~ mask tcbBlockSizeBits = target 617 \<and> canonical_address target \<and> is_aligned target tcbBlockSizeBits" 618 in ccorres_gen_asm) 619 apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg) 620 apply (rule ccorres_cond_both'[where Q=\<top> and Q'=\<top>]) 621 apply (simp add: Collect_const_mem) 622 apply (rule ccorres_move_c_guard_tcb) 623 apply (rule threadSet_ccorres_lemma2[where P=\<top>]) 624 apply vcg 625 apply clarsimp 626 apply (subst StateSpace.state.fold_congs[OF refl refl]) 627 apply (rule globals.fold_congs[OF refl refl]) 628 apply (rule heap_update_field_hrs) 629 apply (simp add: typ_heap_simps) 630 apply (fastforce intro: typ_heap_simps) 631 apply simp 632 apply (erule(1) rf_sr_tcb_update_no_queue2, 633 (simp add: typ_heap_simps)+) 634 apply (rule ball_tcb_cte_casesI, simp+) 635 apply (clarsimp simp: ctcb_relation_def option_to_0_def) 636 apply (rule ccorres_return_Skip) 637 apply (rule ceqv_refl) 638 apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg) 639 apply (rule ccorres_cond_both'[where Q=\<top> and Q'=\<top>]) 640 apply (simp add: Collect_const_mem) 641 apply (ctac add: setMCPriority_ccorres) 642 apply (rule ccorres_return_Skip) 643 apply (rule ceqv_refl) 644 apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg) 645 apply (rule ccorres_cond_both'[where Q=\<top> and Q'=\<top>]) 646 apply (simp add: Collect_const_mem) 647 apply (ctac add: setPriority_ccorres) 648 apply (rule ccorres_return_Skip) 649 apply (rule ceqv_refl) 650 apply (rule ccorres_subgoal_tailE) 651 apply (rule ccorres_subgoal_tailE) 652 apply (rule_tac A="invs' and sch_act_simple and tcb_at' target 653 and case_option \<top> (case_option \<top> (valid_cap' \<circ> fst) \<circ> snd) buf 654 and case_option \<top> (case_option \<top> (cte_at' \<circ> snd) \<circ> snd) buf 655 and K (case_option True (swp is_aligned msg_align_bits \<circ> fst) buf) 656 and K (case_option True (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) buf)" 657 (* bits of tcb_inv_wf' *) 658 in ccorres_guard_imp2[where A'=UNIV]) 659 apply (rule ccorres_Cond_rhs_Seq) 660 apply (simp only: if_True Collect_True split_def bindE_assoc) 661 apply (rule ccorres_rhs_assoc)+ 662 apply csymbr 663 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq)+ 664 apply csymbr 665 apply (simp add: liftE_bindE[symmetric] bindE_assoc getThreadBufferSlot_def 666 locateSlot_conv o_def 667 del: Collect_const) using [[goals_limit=1]] 668 apply (simp add: liftE_bindE del: Collect_const) 669 apply (ctac(no_vcg) add: cteDelete_ccorres) 670 apply (simp del: Collect_const add: Collect_False) 671 apply (rule ccorres_move_c_guard_tcb) 672 apply (rule ccorres_split_nothrow_novcg) 673 apply (rule threadSet_ccorres_lemma2[where P=\<top>]) 674 apply vcg 675 apply clarsimp 676 apply (erule(1) rf_sr_tcb_update_no_queue2, 677 (simp add: typ_heap_simps')+, simp_all?)[1] 678 apply (rule ball_tcb_cte_casesI, simp+) 679 apply (clarsimp simp: ctcb_relation_def option_to_0_def) 680 apply (rule ceqv_refl) 681 apply (ctac(no_vcg) add: archSetIPCBuffer_ccorres[simplified]) 682 apply csymbr 683 apply (simp add: ccorres_cond_iffs Collect_False split_def 684 del: Collect_const) 685 apply (rule ccorres_Cond_rhs_Seq) 686 (* P *) 687 apply (rule ccorres_rhs_assoc)+ 688 apply (simp add: case_option_If2 if_n_0_0 split_def 689 del: Collect_const) 690 apply (rule checkCapAt_ccorres) 691 692 apply ceqv 693 694 apply csymbr 695 apply (simp add: if_1_0_0 true_def Collect_True 696 del: Collect_const) 697 apply (rule ccorres_rhs_assoc)+ 698 apply (rule checkCapAt_ccorres) 699 apply ceqv using [[goals_limit=10]] 700 apply csymbr 701 apply (simp add: if_1_0_0 true_def Collect_True 702 del: Collect_const) 703 apply (simp add: assertDerived_def bind_assoc del: Collect_const) 704 apply (rule ccorres_symb_exec_l) 705 apply (ctac(no_vcg) add: cteInsert_ccorres) 706 apply (rule ccorres_pre_getCurThread) 707 apply (rule ccorres_split_nothrow_novcg_dc) 708 apply (simp add: when_def) 709 apply (rule_tac R="\<lambda>s. rva = ksCurThread s" in ccorres_cond2) 710 apply (clarsimp simp: rf_sr_ksCurThread) 711 apply simp 712 apply (ctac (no_vcg) add: rescheduleRequired_ccorres[unfolded dc_def]) 713 apply (rule ccorres_return_Skip') 714 apply simp 715 apply (rule ccorres_return_CE, simp+)[1] 716 apply wp 717 apply (clarsimp simp: guard_is_UNIV_def) 718 apply simp 719 apply (wp hoare_drop_imp) 720 apply (strengthen sch_act_wf_weak, wp) 721 apply (wp empty_fail_stateAssert hoare_case_option_wp | simp del: Collect_const)+ 722 apply csymbr 723 apply (simp add: if_1_0_0 false_def Collect_False ccorres_cond_iffs 724 del: Collect_const) 725 apply (rule ccorres_pre_getCurThread) 726 apply (simp add: when_def to_bool_def) 727 apply (rule ccorres_split_nothrow_novcg_dc) 728 apply (rule_tac R="\<lambda>s. x = ksCurThread s" in ccorres_cond2) 729 apply (clarsimp simp: rf_sr_ksCurThread) 730 apply clarsimp 731 apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def]) 732 apply (rule ccorres_return_Skip') 733 apply simp 734 apply (rule ccorres_return_CE, simp+) 735 apply wp 736 apply (clarsimp simp: guard_is_UNIV_def) 737 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem 738 tcb_ptr_to_ctcb_ptr_mask tcbBuffer_def 739 size_of_def cte_level_bits_def 740 tcbIPCBufferSlot_def objBits_defs mask_def) 741 apply csymbr 742 apply (simp add: if_1_0_0 Collect_False false_def 743 del: Collect_const) 744 apply (rule ccorres_cond_false_seq, simp) 745 apply (rule ccorres_pre_getCurThread) 746 apply (simp add: when_def to_bool_def) 747 apply (rule ccorres_split_nothrow_novcg_dc) 748 apply (rule_tac R="\<lambda>s. x = ksCurThread s" in ccorres_cond2) 749 apply (clarsimp simp: rf_sr_ksCurThread) 750 apply clarsimp 751 apply (ctac(no_vcg) add: rescheduleRequired_ccorres[unfolded dc_def]) 752 apply (rule ccorres_return_Skip', simp+) 753 apply (rule ccorres_return_CE, simp+) 754 apply wp 755 apply (clarsimp simp: guard_is_UNIV_def) 756 apply (simp add: guard_is_UNIV_def if_1_0_0 false_def 757 Collect_const_mem) 758 apply (clarsimp simp: ccap_relation_def cap_thread_cap_lift cap_to_H_def 759 canonical_address_bitfield_extract_tcb) 760 (* \<not>P *) 761 apply simp 762 apply (rule ccorres_cond_false_seq, simp) 763 apply (rule ccorres_cond_false_seq, simp) 764 apply (simp split: option.split_asm) 765 apply (rule ccorres_pre_getCurThread) 766 apply (simp add: when_def to_bool_def) 767 apply (rule ccorres_split_nothrow_novcg_dc) 768 apply (rule_tac R="\<lambda>s. x = ksCurThread s" in ccorres_cond2) 769 apply (clarsimp simp: rf_sr_ksCurThread) 770 apply clarsimp 771 apply (ctac(no_vcg) add: rescheduleRequired_ccorres[unfolded dc_def]) 772 apply (rule ccorres_return_Skip', simp+) 773 apply (rule ccorres_return_CE, simp+)[1] 774 apply wp 775 apply (clarsimp simp: guard_is_UNIV_def) 776 apply simp 777 apply (rule hoare_strengthen_post[where 778 Q="\<lambda>a b. ((case snd (the buf) of None \<Rightarrow> 0 | Some x \<Rightarrow> snd x) \<noteq> 0 \<longrightarrow> 779 valid_cap' (fst (the (snd (the buf)))) b \<and> 780 invs' b \<and> 781 valid_cap' (capability.ThreadCap target) b \<and> 782 (cte_wp_at' 783 (\<lambda>a. is_derived' (ctes_of b) (snd (the (snd (the buf)))) (fst (the (snd (the buf)))) (cteCap a)) 784 (snd (the (snd (the buf)))) b \<longrightarrow> 785 cte_wp_at' 786 (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap (fst (the (snd (the buf)))) \<or> 787 is_simple_cap' (fst (the (snd (the buf))))) 788 (snd (the (snd (the buf)))) b \<and> 789 cte_wp_at' (\<lambda>c. True) (snd (the (snd (the buf)))) b)) \<and> 790 (target = ksCurThread b \<longrightarrow> 791 Invariants_H.valid_queues b \<and> weak_sch_act_wf (ksSchedulerAction b) b \<and> valid_objs' b)"]) 792 prefer 2 subgoal by auto 793 apply (wp hoare_vcg_conj_lift) 794 apply (strengthen cte_is_derived_capMasterCap_strg, simp add: o_def) 795 apply (wp static_imp_wp ) 796 apply (wp hoare_drop_imp) 797 apply (wp hoare_drop_imp) 798 apply (rule_tac P="is_aligned (fst (the buf)) msg_align_bits" 799 in hoare_gen_asm) 800 apply (wp threadSet_ipcbuffer_trivial static_imp_wp 801 | simp 802 | strengthen invs_sch_act_wf' invs_valid_objs' 803 invs_weak_sch_act_wf invs_queues)+ 804 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem 805 option_to_0_def 806 split: option.split_asm) 807 apply (clarsimp simp: ccap_relation_def cap_thread_cap_lift cap_to_H_def) 808 apply (rule ccorres_split_throws) 809 apply (rule ccorres_return_C_errorE, simp+)[1] 810 apply vcg 811 apply (simp add: conj_comms cong: conj_cong) 812 apply (wp hoare_vcg_const_imp_lift_R cteDelete_invs') 813 apply simp 814 apply (rule ccorres_return_CE) 815 apply (simp+)[3] 816 apply (clarsimp simp: inQ_def Collect_const_mem cintr_def 817 exception_defs tcb_cnode_index_defs) 818 apply (simp add: tcbBuffer_def tcbIPCBufferSlot_def word_sle_def 819 cte_level_bits_def from_bool_def true_def size_of_def) 820 apply (clarsimp simp: case_option_If2 if_n_0_0) 821 apply (simp add: valid_cap'_def capAligned_def) 822 apply (clarsimp simp: objBits_simps' word_bits_conv 823 obj_at'_def projectKOs) 824 apply (rule ccorres_Cond_rhs_Seq) 825 apply (rule ccorres_rhs_assoc)+ 826 apply csymbr 827 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq)+ 828 apply (simp add: split_def getThreadVSpaceRoot_def locateSlot_conv 829 bindE_assoc liftE_bindE 830 del: Collect_const) 831 apply csymbr 832 apply (ctac(no_vcg) add: cteDelete_ccorres) 833 apply (simp add: liftE_bindE Collect_False ccorres_cond_iffs 834 dc_def 835 del: Collect_const) 836 apply ((rule ccorres_split_nothrow_novcg_dc[rotated], assumption) 837 | rule ccorres_rhs_assoc2)+ 838 apply (simp add: conj_comms pred_conj_def) 839 apply (simp add: o_def cong: conj_cong option.case_cong) 840 apply (wp checked_insert_tcb_invs' hoare_case_option_wp 841 checkCap_inv [where P="tcb_at' p0" for p0] 842 checkCap_inv [where P="cte_at' p0" for p0] 843 checkCap_inv [where P="valid_cap' c" for c] 844 checkCap_inv [where P="sch_act_simple"] 845 | simp)+ 846 apply (simp add: guard_is_UNIV_def) 847 apply (thin_tac "ccorres a1 a2 a3 a4 a5 a6 a7" for a1 a2 a3 a4 a5 a6 a7) 848 apply (rule ccorres_rhs_assoc)+ 849 apply (rule checkCapAt_ccorres2) 850 apply ceqv 851 apply csymbr 852 apply (simp add: if_1_0_0 true_def Collect_True 853 del: Collect_const) 854 apply (rule ccorres_rhs_assoc)+ 855 apply (rule checkCapAt_ccorres2) 856 apply ceqv 857 apply csymbr 858 apply (simp add: if_1_0_0 true_def Collect_True 859 assertDerived_def bind_assoc 860 ccorres_cond_iffs dc_def[symmetric] 861 del: Collect_const) 862 apply (rule ccorres_symb_exec_l) 863 apply (ctac add: cteInsert_ccorres) 864 apply (wp empty_fail_stateAssert 865 hoare_case_option_wp | simp del: Collect_const)+ 866 apply csymbr 867 apply (simp add: if_1_0_0 false_def Collect_False ccorres_cond_iffs 868 del: Collect_const) 869 apply (rule ccorres_return_Skip[unfolded dc_def]) 870 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem 871 tcbVTable_def tcbVTableSlot_def Kernel_C.tcbVTable_def 872 cte_level_bits_def size_of_def option_to_0_def objBits_defs 873 mask_def) 874 apply csymbr 875 apply (simp add: if_1_0_0 false_def Collect_False 876 del: Collect_const) 877 apply (rule ccorres_cond_false) 878 apply (rule ccorres_return_Skip[unfolded dc_def]) 879 apply (clarsimp simp: guard_is_UNIV_def false_def 880 ccap_relation_def cap_thread_cap_lift 881 cap_to_H_def if_1_0_0 882 Collect_const_mem canonical_address_bitfield_extract_tcb) 883 apply simp 884 apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+) 885 apply vcg 886 apply (simp add: conj_comms, simp cong: conj_cong add: invs_mdb' invs_pspace_aligned') 887 apply (simp add: cte_is_derived_capMasterCap_strg o_def) 888 apply (wp cteDelete_invs' hoare_case_option_wp cteDelete_deletes 889 cteDelete_sch_act_simple 890 | strengthen invs_valid_objs')+ 891 apply (rule hoare_post_imp_R[where Q' = "\<lambda>r. invs'"]) 892 apply (wp cteDelete_invs') 893 apply (clarsimp simp:cte_wp_at_ctes_of) 894 apply simp 895 apply (rule ccorres_Cond_rhs_Seq) 896 apply (rule ccorres_rhs_assoc)+ 897 apply csymbr 898 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq)+ 899 apply (simp add: split_def getThreadCSpaceRoot_def locateSlot_conv 900 bindE_assoc liftE_bindE 901 del: Collect_const) 902 apply csymbr 903 apply (ctac(no_vcg) add: cteDelete_ccorres) 904 apply (simp add: liftE_bindE Collect_False ccorres_cond_iffs 905 dc_def 906 del: Collect_const) 907 apply ((rule ccorres_split_nothrow_novcg_dc[rotated], assumption) 908 | rule ccorres_rhs_assoc2)+ 909 apply (simp add: conj_comms pred_conj_def) 910 apply (simp add: o_def cong: conj_cong option.case_cong) 911 apply (wp checked_insert_tcb_invs' hoare_case_option_wp 912 checkCap_inv [where P="tcb_at' p0" for p0] 913 checkCap_inv [where P="cte_at' p0" for p0] 914 checkCap_inv [where P="valid_cap' c" for c] 915 checkCap_inv [where P="sch_act_simple"] 916 | simp)+ 917 apply (clarsimp simp: guard_is_UNIV_def from_bool_def true_def 918 word_sle_def if_1_0_0 Collect_const_mem 919 option_to_0_def Kernel_C.tcbVTable_def tcbVTableSlot_def 920 cte_level_bits_def size_of_def cintr_def 921 tcb_cnode_index_defs objBits_defs mask_def) 922 apply (thin_tac "ccorres a1 a2 a3 a4 a5 a6 a7" for a1 a2 a3 a4 a5 a6 a7) 923 apply (rule ccorres_rhs_assoc)+ 924 apply (rule checkCapAt_ccorres2) 925 apply ceqv 926 apply csymbr 927 apply (simp add: if_1_0_0 true_def Collect_True 928 del: Collect_const) 929 apply (rule ccorres_rhs_assoc)+ 930 apply (rule checkCapAt_ccorres2) 931 apply ceqv 932 apply csymbr 933 apply (simp add: if_1_0_0 true_def Collect_True 934 assertDerived_def bind_assoc 935 ccorres_cond_iffs dc_def[symmetric] 936 del: Collect_const) 937 apply (rule ccorres_symb_exec_l) 938 apply (ctac add: cteInsert_ccorres) 939 apply (wp empty_fail_stateAssert 940 hoare_case_option_wp 941 | simp del: Collect_const)+ 942 apply csymbr 943 apply (simp add: if_1_0_0 false_def Collect_False ccorres_cond_iffs 944 del: Collect_const) 945 apply (rule ccorres_return_Skip[unfolded dc_def]) 946 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem 947 Kernel_C.tcbCTable_def tcbCTableSlot_def 948 cte_level_bits_def size_of_def option_to_0_def 949 mask_def objBits_defs) 950 apply csymbr 951 apply (simp add: if_1_0_0 false_def Collect_False 952 del: Collect_const) 953 apply (rule ccorres_cond_false) 954 apply (rule ccorres_return_Skip[unfolded dc_def]) 955 apply (clarsimp simp: guard_is_UNIV_def false_def 956 ccap_relation_def cap_thread_cap_lift 957 cap_to_H_def if_1_0_0 958 Collect_const_mem canonical_address_bitfield_extract_tcb) 959 apply simp 960 apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+) 961 apply vcg 962 apply (simp add: conj_comms, simp cong: conj_cong add: invs_mdb' invs_pspace_aligned') 963 apply (simp add: cte_is_derived_capMasterCap_strg o_def) 964 apply (wp cteDelete_invs' hoare_case_option_wp cteDelete_deletes 965 cteDelete_sch_act_simple 966 | strengthen invs_valid_objs')+ 967 apply (rule hoare_post_imp_R[where Q' = "\<lambda>r. invs'"]) 968 apply (wp cteDelete_invs') 969 apply (clarsimp simp:cte_wp_at_ctes_of) 970 apply simp 971 apply (wp hoare_case_option_wp setP_invs' static_imp_wp | simp)+ 972 apply (clarsimp simp: guard_is_UNIV_def tcbCTableSlot_def Kernel_C.tcbCTable_def 973 cte_level_bits_def size_of_def word_sle_def option_to_0_def 974 true_def from_bool_def cintr_def objBits_defs mask_def) 975 apply (simp add: conj_comms) 976 apply (wp hoare_case_option_wp threadSet_invs_trivial setMCPriority_invs' 977 typ_at_lifts[OF setMCPriority_typ_at'] 978 threadSet_cap_to' static_imp_wp | simp)+ 979 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) 980 apply (simp add: conj_comms) 981 apply (wp hoare_case_option_wp threadSet_invs_trivial 982 threadSet_cap_to' static_imp_wp | simp)+ 983 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) 984 apply (clarsimp simp: inQ_def) 985 apply (subst is_aligned_neg_mask_eq) 986 apply (simp add: tcb_ptr_to_ctcb_ptr_def) 987 apply (rule aligned_add_aligned) 988 apply (fastforce simp add: obj_at'_def projectKOs objBits_simps') 989 apply (simp add: ctcb_offset_defs is_aligned_def) 990 apply (simp add: word_bits_conv) 991 apply simp 992 apply (subgoal_tac "s \<turnstile>' capability.ThreadCap target") 993 apply (clarsimp simp: cte_level_bits_def Kernel_C.tcbCTable_def Kernel_C.tcbVTable_def 994 tcbCTableSlot_def tcbVTableSlot_def size_of_def 995 tcb_cte_cases_def isCap_simps tcb_aligned' obj_at'_is_canonical 996 split: option.split_asm 997 dest!: isValidVTableRootD invs_pspace_canonical') 998 apply (clarsimp simp: valid_cap'_def capAligned_def word_bits_conv 999 obj_at'_def objBits_simps' projectKOs) 1000 done 1001 1002lemma setupReplyMaster_ccorres: 1003 "ccorres dc xfdc (tcb_at' t) 1004 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}) [] 1005 (setupReplyMaster t) (Call setupReplyMaster_'proc)" 1006 apply (cinit lift: thread_') 1007 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq)+ 1008 apply ctac 1009 apply (simp del: Collect_const add: dc_def[symmetric]) 1010 apply (rule ccorres_pre_getCTE) 1011 apply (rule ccorres_move_c_guard_cte) 1012 apply (rule_tac F="\<lambda>rv'. (rv' = scast cap_null_cap) = (cteCap oldCTE = NullCap)" 1013 and R="cte_wp_at' ((=) oldCTE) rv" 1014 and xf'=ret__unsigned_longlong_' 1015 in ccorres_symb_exec_r_abstract_UNIV[where R'=UNIV]) 1016 apply (rule conseqPre, vcg) 1017 apply (clarsimp simp: cte_wp_at_ctes_of) 1018 apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) 1019 apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap 1020 dest!: ccte_relation_ccap_relation) 1021 apply ceqv 1022 apply (simp only:) 1023 apply (rule ccorres_when[where R=\<top>]) 1024 apply (simp add: Collect_const_mem) 1025 apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_stateAssert]) 1026 apply (rule_tac P="cte_at' rv and tcb_at' t" in ccorres_from_vcg[where P'=UNIV]) 1027 apply (rule allI, rule conseqPre, vcg) 1028 apply (clarsimp simp: cte_wp_at_ctes_of) 1029 apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+) 1030 apply (rule conjI, fastforce intro: typ_heap_simps) 1031 apply (clarsimp simp: typ_heap_simps) 1032 apply (rule fst_setCTE[OF ctes_of_cte_at], assumption) 1033 apply (rule rev_bexI, assumption) 1034 apply (clarsimp simp: rf_sr_def cstate_relation_def 1035 cpspace_relation_def Let_def 1036 typ_heap_simps') 1037 apply (subst setCTE_tcb_case, assumption+) 1038 apply (rule_tac r="s'" in KernelStateData_H.kernel_state.cases) 1039 apply clarsimp 1040 apply (rule conjI) 1041 apply (erule(2) cmap_relation_updI) 1042 apply (clarsimp simp: ccte_relation_def cap_reply_cap_lift cte_lift_def 1043 cong: option.case_cong_weak) 1044 apply (simp add: cte_to_H_def cap_to_H_def mdb_node_to_H_def 1045 nullMDBNode_def c_valid_cte_def) 1046 apply (simp add: cap_reply_cap_lift) 1047 apply (simp add: true_def mask_def to_bool_def) 1048 apply simp 1049 apply (simp add: cmachine_state_relation_def packed_heap_update_collapse_hrs 1050 carch_state_relation_def carch_globals_def 1051 fpu_null_state_heap_update_tag_disj_simps 1052 global_ioport_bitmap_heap_update_tag_disj_simps 1053 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) 1054 apply (wp | simp)+ 1055 apply (clarsimp simp: guard_is_UNIV_def) 1056 apply (wp | simp add: locateSlot_conv)+ 1057 apply vcg 1058 apply (clarsimp simp: word_sle_def cte_wp_at_ctes_of 1059 tcb_cnode_index_defs tcbReplySlot_def) 1060 done 1061 1062lemma restart_ccorres: 1063 "ccorres dc xfdc (invs' and tcb_at' thread and sch_act_simple) 1064 (UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) [] 1065 (restart thread) (Call restart_'proc)" 1066 apply (cinit lift: target_') 1067 apply (ctac(no_vcg) add: isBlocked_ccorres) 1068 apply (simp only: when_def) 1069 apply (rule ccorres_cond2[where R=\<top>]) 1070 apply (simp add: to_bool_def Collect_const_mem) 1071 apply (rule ccorres_rhs_assoc)+ 1072 apply (ctac(no_vcg) add: cancelIPC_ccorres1[OF cteDeleteOne_ccorres]) 1073 apply (ctac(no_vcg) add: setupReplyMaster_ccorres) 1074 apply (ctac(no_vcg)) 1075 apply (ctac(no_vcg) add: tcbSchedEnqueue_ccorres) 1076 apply (ctac add: possibleSwitchTo_ccorres) 1077 apply (wp weak_sch_act_wf_lift)[1] 1078 apply (wp sts_valid_queues setThreadState_st_tcb)[1] 1079 apply (simp add: valid_tcb_state'_def) 1080 apply wp 1081 apply (wp_once sch_act_wf_lift, (wp tcb_in_cur_domain'_lift)+) 1082 apply (rule hoare_strengthen_post) 1083 apply (rule hoare_vcg_conj_lift) 1084 apply (rule delete_one_conc_fr.cancelIPC_invs) 1085 1086 apply (rule cancelIPC_tcb_at'[where t=thread]) 1087 apply fastforce 1088 apply (rule ccorres_return_Skip) 1089 apply (wp hoare_drop_imps) 1090 apply (auto simp: Collect_const_mem mask_def "StrictC'_thread_state_defs") 1091 done 1092 1093lemma setNextPC_ccorres: 1094 "ccorres dc xfdc \<top> 1095 (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> 1096 \<inter> {s. v_' s = val}) [] 1097 (asUser thread (setNextPC val)) 1098 (Call setNextPC_'proc)" 1099 apply (cinit') 1100 apply (simp add: setNextPC_def) 1101 apply (ctac add: setRegister_ccorres) 1102 apply simp 1103 done 1104 1105lemma Arch_performTransfer_ccorres: 1106 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 1107 \<top> UNIV [] 1108 (liftE (performTransfer a b c)) 1109 (Call Arch_performTransfer_'proc)" 1110 apply (cinit' simp: performTransfer_def) 1111 apply (fold returnOk_liftE) 1112 apply (rule ccorres_return_CE) 1113 apply simp+ 1114 done 1115 1116(*FIXME: arch_split: C kernel names hidden by Haskell names *) 1117abbreviation "frameRegistersC \<equiv> kernel_all_substitute.frameRegisters" 1118lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def 1119abbreviation "gpRegistersC \<equiv> kernel_all_substitute.gpRegisters" 1120lemmas gpRegistersC_def = kernel_all_substitute.gpRegisters_def 1121 1122lemma frame_gp_registers_convs: 1123 "length X64_H.frameRegisters = unat n_frameRegisters" 1124 "length X64_H.gpRegisters = unat n_gpRegisters" 1125 "n < length X64_H.frameRegisters \<Longrightarrow> 1126 index frameRegistersC n = register_from_H (X64_H.frameRegisters ! n)" 1127 "n < length X64_H.gpRegisters \<Longrightarrow> 1128 index gpRegistersC n = register_from_H (X64_H.gpRegisters ! n)" 1129 apply (simp_all add: X64_H.gpRegisters_def X64_H.frameRegisters_def 1130 X64.gpRegisters_def n_gpRegisters_def 1131 X64.frameRegisters_def n_frameRegisters_def 1132 frameRegistersC_def gpRegistersC_def msgRegisters_unfold 1133 fupdate_def Arrays.update_def toEnum_def 1134 upto_enum_def fromEnum_def enum_register) 1135 apply (auto simp: less_Suc_eq fcp_beta) 1136 done 1137 1138 1139lemma postModifyRegisters_ccorres: 1140 "ccorres dc xfdc 1141 (\<lambda>s. ct = ksCurThread s) 1142 \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr dest\<rbrace> hs 1143 (asUser dest (postModifyRegisters ct dest)) 1144 (Call Arch_postModifyRegisters_'proc)" 1145 apply (cinit' lift: tptr_') 1146 apply (rule_tac xf'' = xfdc and 1147 A = "(\<lambda>s. ct = ksCurThread s)" and 1148 C'= "UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr dest}" 1149 in ccorres_call[rotated]) 1150 apply (simp+)[3] 1151 apply (cinit' lift: tptr_' simp: postModifyRegisters_def when_def) 1152 apply (simp add: if_distrib[where f="asUser t" for t] asUser_return) 1153 apply (rule_tac R="\<lambda>s. ct = ksCurThread s" in ccorres_cond2) 1154 apply (clarsimp simp: rf_sr_ksCurThread) 1155 apply (ctac add: setRegister_ccorres[unfolded dc_def]) 1156 apply (rule ccorres_add_return2) 1157 apply (rule ccorres_stateAssert) 1158 apply (rule ccorres_return_Skip'[unfolded dc_def]) 1159 by simp+ 1160 1161lemma invokeTCB_CopyRegisters_ccorres: 1162 "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') 1163 (invs' and sch_act_simple and tcb_at' destn and tcb_at' source 1164 and ex_nonz_cap_to' destn and ex_nonz_cap_to' source) 1165 (UNIV \<inter> {s. dest___ptr_to_struct_tcb_C_' s = tcb_ptr_to_ctcb_ptr destn} 1166 \<inter> {s. tcb_src_' s = tcb_ptr_to_ctcb_ptr source} 1167 \<inter> {s. to_bool (resumeTarget_' s) = resume} 1168 \<inter> {s. to_bool (suspendSource_' s) = susp} 1169 \<inter> {s. to_bool (transferFrame_' s) = frames} 1170 \<inter> {s. to_bool (transferInteger_' s) = ints}) [] 1171 (invokeTCB (CopyRegisters destn source susp resume frames ints arch)) 1172 (Call invokeTCB_CopyRegisters_'proc)" 1173 apply (cinit lift: dest___ptr_to_struct_tcb_C_' tcb_src_' resumeTarget_' 1174 suspendSource_' transferFrame_' transferInteger_' 1175 simp: whileAnno_def) 1176 apply (simp add: liftE_def bind_assoc whileAnno_def 1177 del: Collect_const) 1178 apply (rule ccorres_split_nothrow_novcg_dc) 1179 apply (rule ccorres_when[where R=\<top>]) 1180 apply (simp add: to_bool_def del: Collect_const) 1181 apply (ctac add: suspend_ccorres[OF cteDeleteOne_ccorres]) 1182 apply (rule ccorres_split_nothrow_novcg_dc) 1183 apply (rule ccorres_when[where R=\<top>]) 1184 apply (simp add: to_bool_def del: Collect_const) 1185 apply (ctac add: restart_ccorres) 1186 apply (rule ccorres_split_nothrow_novcg_dc) 1187 apply (rule ccorres_when[where R=\<top>]) 1188 apply (simp add: to_bool_def Collect_const_mem) 1189 apply (rule ccorres_rhs_assoc)+ 1190 apply (csymbr, csymbr, csymbr) 1191 apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg_dc) 1192 apply (rule ccorres_rel_imp) 1193 apply (rule ccorres_mapM_x_while[where F="\<lambda>x. tcb_at' destn and tcb_at' source"]) 1194 apply clarsimp 1195 apply (rule ccorres_guard_imp2) 1196 apply (ctac(no_vcg) add: getRegister_ccorres) 1197 apply (ctac add: setRegister_ccorres) 1198 apply wp 1199 apply (clarsimp simp: frame_gp_registers_convs 1200 n_frameRegisters_def unat_of_nat64 1201 word_bits_def word_of_nat_less) 1202 apply (simp add: frame_gp_registers_convs n_frameRegisters_def) 1203 apply (rule allI, rule conseqPre, vcg) 1204 apply clarsimp 1205 apply (wp | simp)+ 1206 apply (simp add: frame_gp_registers_convs n_frameRegisters_def 1207 word_bits_def) 1208 apply simp 1209 apply (ctac(no_vcg) add: getRestartPC_ccorres) 1210 apply (ctac add: setNextPC_ccorres) 1211 apply wp+ 1212 apply (clarsimp simp: guard_is_UNIV_def) 1213 apply (rule ccorres_split_nothrow_novcg_dc) 1214 apply (rule ccorres_when[where R=\<top>]) 1215 apply (simp add: to_bool_def Collect_const_mem) 1216 apply (rule ccorres_rhs_assoc)+ 1217 apply (csymbr, csymbr) 1218 apply (rule ccorres_rel_imp) 1219 apply (rule ccorres_mapM_x_while[where F="\<lambda>x. tcb_at' destn and tcb_at' source"]) 1220 apply clarsimp 1221 apply (rule ccorres_guard_imp2) 1222 apply ((wp | ctac(no_vcg) add: getRegister_ccorres setRegister_ccorres)+)[1] 1223 apply (clarsimp simp: frame_gp_registers_convs n_gpRegisters_def 1224 unat_of_nat64 word_bits_def word_of_nat_less) 1225 apply (simp add: frame_gp_registers_convs n_gpRegisters_def) 1226 apply (rule allI, rule conseqPre, vcg) 1227 apply clarsimp 1228 apply (wp | simp)+ 1229 apply (simp add: word_bits_def frame_gp_registers_convs n_gpRegisters_def) 1230 apply simp 1231 apply (rule ccorres_pre_getCurThread) 1232 apply (ctac add: postModifyRegisters_ccorres) 1233 apply (rule ccorres_split_nothrow_novcg_dc) 1234 apply (rule_tac R="\<lambda>s. rvd = ksCurThread s" 1235 in ccorres_when) 1236 apply (clarsimp simp: rf_sr_ksCurThread) 1237 apply clarsimp 1238 apply (ctac (no_vcg) add: rescheduleRequired_ccorres) 1239 apply (simp only: liftE_bindE[symmetric] return_returnOk) 1240 apply (ctac(no_vcg) add: Arch_performTransfer_ccorres) 1241 apply (rule ccorres_return_CE, simp+)[1] 1242 apply (rule ccorres_return_C_errorE, simp+)[1] 1243 apply simp 1244 apply wp+ 1245 apply (clarsimp simp: guard_is_UNIV_def) 1246 apply simp 1247 apply (wpsimp simp: postModifyRegisters_def pred_conj_def 1248 cong: if_cong 1249 wp: hoare_drop_imp) 1250 apply vcg 1251 apply (simp add: pred_conj_def guard_is_UNIV_def cong: if_cong 1252 | wp mapM_x_wp_inv hoare_drop_imp)+ 1253 apply clarsimp 1254 apply (rule_tac Q="\<lambda>rv. invs' and tcb_at' destn" in hoare_strengthen_post[rotated]) 1255 apply (fastforce simp: sch_act_wf_weak) 1256 apply (wpsimp wp: hoare_drop_imp restart_invs')+ 1257 apply (clarsimp simp add: guard_is_UNIV_def) 1258 apply (wp hoare_drop_imp hoare_vcg_if_lift)+ 1259 apply simp 1260 apply (rule_tac Q="\<lambda>rv. invs' and tcb_at' destn" in hoare_strengthen_post[rotated]) 1261 apply (fastforce simp: sch_act_wf_weak) 1262 apply (wpsimp wp: hoare_drop_imp)+ 1263 apply (clarsimp simp add: guard_is_UNIV_def) 1264 apply (clarsimp simp: to_bool_def invs_weak_sch_act_wf invs_valid_objs' 1265 split: if_split cong: if_cong | rule conjI)+ 1266 apply (clarsimp dest!: global'_no_ex_cap simp: invs'_def valid_state'_def | rule conjI)+ 1267 done 1268 1269(* FIXME: move *) 1270lemmas mapM_x_append = mapM_x_append2 1271 1272lemma invokeTCB_WriteRegisters_ccorres_helper: 1273 "\<lbrakk> unat (f (of_nat n)) = incn 1274 \<and> g (of_nat n) = register_from_H reg \<and> n'=incn 1275 \<and> of_nat n < bnd \<and> of_nat n < bnd2 \<rbrakk> \<Longrightarrow> 1276 ccorres dc xfdc (sysargs_rel args buffer and sysargs_rel_n args buffer n' and 1277 tcb_at' dst and P) 1278 (\<lbrace>\<acute>i = of_nat n\<rbrace>) hs 1279 (asUser dst (setRegister reg 1280 (sanitiseRegister t reg (args ! incn)))) 1281 (\<acute>ret__unsigned_long :== CALL getSyscallArg(f (\<acute>i),option_to_ptr buffer);; 1282 Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> 1283 (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister(g (\<acute>i),\<acute>ret__unsigned_long,from_bool t));; 1284 Guard ArrayBounds \<lbrace>\<acute>i < bnd2\<rbrace> 1285 (CALL setRegister(tcb_ptr_to_ctcb_ptr dst,g (\<acute>i),\<acute>unsigned_long_eret_2)))" 1286 apply (rule ccorres_guard_imp2) 1287 apply (rule ccorres_add_return) 1288 apply (rule ccorres_rhs_assoc)+ 1289 apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n="incn" and buffer=buffer]) 1290 apply (rule ccorres_symb_exec_r) 1291 apply (ctac add: setRegister_ccorres) 1292 apply (vcg) 1293 apply clarsimp 1294 apply (rule conseqPre, vcg, clarsimp) 1295 apply wp 1296 apply simp 1297 apply (vcg exspec=getSyscallArg_modifies) 1298 apply fastforce 1299 done 1300 1301lemma doMachineOp_context: 1302 "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow> 1303 (rv,s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) 1304 \<in> fst (doMachineOp f (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))" 1305 apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def) 1306 apply fastforce 1307 done 1308 1309 1310lemma getObject_context: 1311 " \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> 1312 \<Longrightarrow> (if t = t' then tcbContext_update (\<lambda>_. st) x else x, 1313 s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) 1314 \<in> fst (getObject t' (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))" 1315 apply (simp split: if_split) 1316 apply (rule conjI) 1317 apply clarsimp 1318 apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad 1319 Corres_C.in_magnitude_check' projectKOs objBits_simps') 1320 apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps) 1321 apply (simp add: magnitudeCheck_def in_monad split: option.splits) 1322 apply clarsimp 1323 apply (simp add: lookupAround2_char2) 1324 apply (clarsimp split: if_split_asm) 1325 apply (erule_tac x=x2 in allE) 1326 apply (clarsimp simp: ps_clear_def) 1327 apply (drule_tac x=x2 in orthD2) 1328 apply fastforce 1329 apply clarsimp 1330 apply (erule impE) 1331 apply simp 1332 apply (erule notE, rule word_diff_ls'(3)) 1333 apply unat_arith 1334 apply (drule is_aligned_no_overflow) 1335 apply simp 1336 apply clarsimp 1337 apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad 1338 Corres_C.in_magnitude_check' projectKOs objBits_simps') 1339 apply (simp add: magnitudeCheck_def in_monad split: option.splits) 1340 apply clarsimp 1341 apply (simp add: lookupAround2_char2) 1342 apply (clarsimp split: if_split_asm) 1343 apply (erule_tac x=t in allE) 1344 apply simp 1345 apply (clarsimp simp: obj_at'_real_def projectKOs 1346 ko_wp_at'_def objBits_simps) 1347 apply (simp add: ps_clear_def) 1348 apply (drule_tac x=t in orthD2) 1349 apply fastforce 1350 apply clarsimp 1351 apply (erule impE) 1352 apply simp 1353 apply (erule notE, rule word_diff_ls'(3)) 1354 apply unat_arith 1355 apply (drule is_aligned_no_overflow) 1356 apply simp 1357 apply (erule_tac x=x2 in allE) 1358 apply (clarsimp simp: ps_clear_def) 1359 apply (drule_tac x=x2 in orthD2) 1360 apply fastforce 1361 apply clarsimp 1362 apply (erule impE) 1363 apply (rule word_diff_ls'(3)) 1364 apply unat_arith 1365 apply (drule is_aligned_no_overflow) 1366 apply simp 1367 apply fastforce 1368 done 1369 1370lemma threadGet_context: 1371 "\<lbrakk> (uc, s') \<in> fst (threadGet (atcbContextGet o tcbArch) (ksCurThread s) s); ko_at' ko t s; 1372 t \<noteq> ksCurThread s \<rbrakk> \<Longrightarrow> 1373 (uc, s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> 1374 fst (threadGet (atcbContextGet o tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>))" 1375 apply (clarsimp simp: threadGet_def liftM_def in_monad) 1376 apply (drule (1) getObject_context [where st=st]) 1377 apply (rule exI) 1378 apply (erule conjI) 1379 apply (simp split: if_splits) 1380done 1381 1382 1383lemma asUser_context: 1384 "\<lbrakk>(x,s) \<in> fst (asUser (ksCurThread s) f s); ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace> ; 1385 t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow> 1386 (x,s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> 1387 fst (asUser (ksCurThread s) f (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>))" 1388 apply (clarsimp simp: asUser_def in_monad select_f_def) 1389 apply (frule use_valid, rule threadGet_inv [where P="(=) s"], rule refl) 1390 apply (frule use_valid, assumption, rule refl) 1391 apply clarsimp 1392 apply (frule (2) threadGet_context) 1393 apply (intro exI) 1394 apply (erule conjI) 1395 apply (rule exI, erule conjI) 1396 apply (clarsimp simp: threadSet_def in_monad) 1397 apply (frule use_valid, rule getObject_inv [where P="(=) s"]) 1398 apply (simp add: loadObject_default_def) 1399 apply wp 1400 apply simp 1401 apply (rule refl) 1402 apply clarsimp 1403 apply (frule (1) getObject_context) 1404 apply (intro exI) 1405 apply (erule conjI) 1406 apply (clarsimp simp: setObject_def split_def updateObject_default_def threadGet_def 1407 Corres_C.in_magnitude_check' getObject_def loadObject_default_def liftM_def 1408 objBits_simps' projectKOs in_monad) 1409 1410 apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits) 1411 apply (rule conjI) 1412 apply clarsimp 1413 apply (cases s, simp) 1414 apply (rule ext, clarsimp split: if_split) 1415 apply (case_tac tcb, simp) 1416 1417 apply clarsimp 1418 apply (rule conjI) 1419 apply (clarsimp simp add: lookupAround2_char2 split: if_split_asm) 1420 apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps) 1421 apply (erule_tac x=t in allE) 1422 apply simp 1423 apply (simp add: ps_clear_def) 1424 apply (drule_tac x=t in orthD2) 1425 apply fastforce 1426 apply clarsimp 1427 apply (erule impE, simp) 1428 apply (erule notE, rule word_diff_ls'(3)) 1429 apply unat_arith 1430 apply (drule is_aligned_no_overflow) 1431 apply simp 1432 apply (erule_tac x=x2 in allE) 1433 apply simp 1434 apply (simp add: ps_clear_def) 1435 apply (drule_tac x=x2 in orthD2) 1436 apply fastforce 1437 apply clarsimp 1438 apply (erule impE) 1439 apply (rule word_diff_ls'(3)) 1440 apply unat_arith 1441 apply (drule is_aligned_no_overflow) 1442 apply simp 1443 apply (erule impE, simp) 1444 apply simp 1445 apply (rule exI) 1446 apply (rule conjI, fastforce) 1447 apply clarsimp 1448 apply (cases s, clarsimp) 1449 apply (rule ext, clarsimp split: if_split) 1450 apply (case_tac tcb, clarsimp) 1451done 1452 1453 1454lemma getMRs_rel_context: 1455 "\<lbrakk>getMRs_rel args buffer s; 1456 (cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer) s; 1457 ko_at' ko t s ; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow> 1458 getMRs_rel args buffer (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)" 1459 apply (clarsimp simp: getMRs_rel_def) 1460 apply (rule exI, erule conjI) 1461 apply (subst (asm) det_wp_use, rule det_wp_getMRs) 1462 apply (simp add: cur_tcb'_def) 1463 apply (subst det_wp_use, rule det_wp_getMRs) 1464 apply (simp add: cur_tcb'_def) 1465 apply (rule conjI) 1466 apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs 1467 objBits_simps ps_clear_def split: if_split) 1468 apply (clarsimp simp: valid_ipc_buffer_ptr'_def split: option.splits) 1469 apply (clarsimp simp: typ_at'_def ko_wp_at'_def projectKOs obj_at'_real_def 1470 objBits_simps ps_clear_def split: if_split) 1471 apply (clarsimp simp: getMRs_def in_monad) 1472 apply (frule use_valid, rule asUser_inv [where P="(=) s"]) 1473 apply (wp mapM_wp' getRegister_inv)[1] 1474 apply simp 1475 apply clarsimp 1476 apply (drule (1) asUser_context) 1477 apply (wp mapM_wp' getRegister_inv)[1] 1478 apply assumption 1479 apply (intro exI) 1480 apply (erule conjI) 1481 apply (cases buffer) 1482 apply (clarsimp simp: return_def) 1483 apply clarsimp 1484 apply (drule mapM_upd_inv [rotated -1]) 1485 prefer 3 1486 apply fastforce 1487 prefer 2 1488 apply wp 1489 apply (clarsimp simp: loadWordUser_def in_monad stateAssert_def word_size 1490 simp del: fun_upd_apply) 1491 apply (rule conjI) 1492 apply (clarsimp simp: pointerInUserData_def typ_at'_def ko_wp_at'_def 1493 projectKOs ps_clear_def obj_at'_real_def 1494 split: if_split) 1495 apply (erule doMachineOp_context) 1496done 1497 1498lemma asUser_getMRs_rel: 1499 "\<lbrace>(\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' 1500 and case_option \<top> valid_ipc_buffer_ptr' buffer \<rbrace> 1501 asUser t f \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace>" 1502 apply (simp add: asUser_def) 1503 apply (rule hoare_pre, wp) 1504 apply (simp add: threadSet_def) 1505 apply (simp add: setObject_def split_def updateObject_default_def) 1506 apply wp 1507 apply (simp del: fun_upd_apply) 1508 apply (wp getObject_tcb_wp) 1509 apply (wp threadGet_wp)+ 1510 apply (clarsimp simp del: fun_upd_apply) 1511 apply (drule obj_at_ko_at')+ 1512 apply (clarsimp simp del: fun_upd_apply) 1513 apply (rule exI, rule conjI, assumption) 1514 apply (clarsimp split: if_split simp del: fun_upd_apply) 1515 apply (erule getMRs_rel_context, simp) 1516 apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs) 1517 apply simp 1518done 1519 1520 1521lemma asUser_sysargs_rel: 1522 "\<lbrace>\<lambda>s. t \<noteq> ksCurThread s \<and> sysargs_rel args buffer s\<rbrace> 1523 asUser t f \<lbrace>\<lambda>_. sysargs_rel args buffer\<rbrace>" 1524 apply (cases buffer, simp_all add: sysargs_rel_def) 1525 apply (rule hoare_pre) 1526 apply (wp asUser_getMRs_rel hoare_valid_ipc_buffer_ptr_typ_at'|simp)+ 1527done 1528 1529lemma threadSet_same: 1530 "\<lbrace>\<lambda>s. \<exists>tcb'. ko_at' tcb' t s \<and> tcb = f tcb'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ko_at' tcb t\<rbrace>" 1531 unfolding threadSet_def 1532 by (wpsimp wp: setObject_tcb_strongest getObject_tcb_wp) fastforce 1533 1534lemma asUser_setRegister_ko_at': 1535 "\<lbrace>obj_at' (\<lambda>tcb'. tcb = tcbArch_update (\<lambda>_. atcbContextSet (modify_registers (\<lambda>regs. regs(r := v)) (atcbContextGet (tcbArch tcb'))) (tcbArch tcb')) tcb') dst\<rbrace> 1536 asUser dst (setRegister r v) \<lbrace>\<lambda>rv. ko_at' (tcb::tcb) dst\<rbrace>" 1537 unfolding asUser_def 1538 apply (wpsimp wp: threadSet_same threadGet_wp) 1539 apply (clarsimp simp: setRegister_def simpler_modify_def obj_at'_def modify_registers_def) 1540 done 1541 1542lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: 1543 notes static_imp_wp [wp] word_less_1[simp del] 1544 shows 1545 "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') 1546 (invs' and tcb_at' dst and ex_nonz_cap_to' dst and sch_act_simple 1547 and sysargs_rel args buffer 1548 and (\<lambda>s. dst \<noteq> ksCurThread s) 1549 and (\<lambda>_. values = take someNum (drop 2 args) 1550 \<and> someNum + 2 \<le> length args)) 1551 ({s. unat (n_' s) = length values} \<inter> S 1552 \<inter> {s. unat (n_' s) = length values} 1553 \<inter> {s. dest___ptr_to_struct_tcb_C_' s = tcb_ptr_to_ctcb_ptr dst} 1554 \<inter> {s. resumeTarget_' s = from_bool resume} 1555 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 1556 (invokeTCB (WriteRegisters dst resume values arch)) 1557 (Call invokeTCB_WriteRegisters_'proc)" 1558 apply (rule ccorres_gen_asm) 1559 apply (erule conjE) 1560 apply (cinit lift: n_' dest___ptr_to_struct_tcb_C_' resumeTarget_' buffer_' 1561 simp: whileAnno_def) 1562 (* using S not univ seems to stop cinit doing this? *) 1563 apply (csymbr, csymbr, csymbr, csymbr) 1564 apply (simp add: liftE_def bind_assoc 1565 del: Collect_const) 1566 apply (rule ccorres_pre_getCurThread) 1567 apply (rule_tac P="\<lambda>a. ccorres_underlying rf_sr \<Gamma> r' xf arrel axf P P' hs a c" for r' xf arrel axf P P' hs c in subst) 1568 apply (rule liftE_bindE) 1569 1570 apply (ctac add: Arch_performTransfer_ccorres) 1571 apply (simp add: Collect_False whileAnno_def del: Collect_const) 1572 apply (rule ccorres_add_return) 1573 apply (rule_tac xf'=n_' and r'="\<lambda>rv rv'. rv' = min n (scast n_frameRegisters + scast n_gpRegisters)" 1574 in ccorres_split_nothrow) 1575 apply (rule_tac P'="{s. n_' s = n}" in ccorres_from_vcg[where P=\<top>]) 1576 apply (rule allI, rule conseqPre, vcg) 1577 apply (clarsimp simp: return_def min_def) 1578 apply (simp add: linorder_not_less[symmetric] n_gpRegisters_def n_frameRegisters_def) 1579 apply ceqv 1580 apply (ctac add: Arch_getSanitiseRegisterInfo_ccorres) 1581 apply (simp add: zipWithM_mapM split_def zip_append1 mapM_discarded mapM_x_append 1582 del: Collect_const) 1583 apply (simp add: asUser_bind_distrib getRestartPC_def setNextPC_def bind_assoc 1584 del: Collect_const) 1585 apply (simp only: getRestartPC_def[symmetric] setNextPC_def[symmetric]) 1586 apply (simp add: asUser_mapM_x bind_assoc) 1587 apply (rule ccorres_stateAssert) 1588 apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) 1589 apply (drule_tac t="archInfo" in sym, simp only:) 1590 apply (rule_tac F="\<lambda>n. sysargs_rel args buffer and sysargs_rel_n args buffer (n + 2) and 1591 tcb_at' dst and (\<lambda>s. dst \<noteq> ksCurThread s)" 1592 and Q=UNIV in ccorres_mapM_x_whileQ) 1593 apply clarsimp 1594 apply (rule invokeTCB_WriteRegisters_ccorres_helper [where args=args]) 1595 apply (simp add: unat_word_ariths frame_gp_registers_convs n_frameRegisters_def 1596 unat_of_nat64 word_bits_def word_of_nat_less) 1597 apply (simp add: n_frameRegisters_def n_gpRegisters_def 1598 frame_gp_registers_convs word_less_nat_alt) 1599 apply (simp add: unat_of_nat64 word_bits_def) 1600 apply arith 1601 apply clarsimp 1602 apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies 1603 exspec=sanitiseRegister_modifies) 1604 apply clarsimp 1605 apply (simp add: sysargs_rel_n_def) 1606 apply (rule hoare_pre, wp asUser_sysargs_rel asUser_setRegister_ko_at') 1607 apply (clarsimp simp: n_msgRegisters_def sysargs_rel_def) 1608 apply (simp add: frame_gp_registers_convs n_frameRegisters_def word_bits_def) 1609 apply simp 1610 apply (rule ceqv_refl) 1611 apply (rule ccorres_stateAssert) 1612 apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) 1613 apply (drule_tac t="archInfo" in sym, simp only:) 1614 apply (rule_tac F="\<lambda>n. sysargs_rel args buffer 1615 and sysargs_rel_n args buffer (n + length X64_H.frameRegisters + 2) 1616 and tcb_at' dst and (\<lambda>s. dst \<noteq> ksCurThread s)" 1617 and Q=UNIV in ccorres_mapM_x_whileQ) 1618 apply clarsimp 1619 apply (rule invokeTCB_WriteRegisters_ccorres_helper [where args=args]) 1620 apply (simp add: n_gpRegisters_def unat_word_ariths 1621 frame_gp_registers_convs unat_of_nat64 1622 word_bits_def n_frameRegisters_def 1623 word_of_nat_less word_less_1) 1624 apply (simp add: n_frameRegisters_def n_gpRegisters_def 1625 frame_gp_registers_convs unat_of_nat64 1626 word_less_nat_alt word_bits_def 1627 less_diff_conv) 1628 apply (simp add: unat_word_ariths cong: conj_cong) 1629 apply clarsimp 1630 apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies 1631 exspec=sanitiseRegister_modifies) 1632 apply clarsimp 1633 apply (simp add: sysargs_rel_n_def) 1634 apply (rule hoare_pre, wp asUser_sysargs_rel) 1635 apply (clarsimp simp: n_msgRegisters_def frame_gp_registers_convs 1636 n_frameRegisters_def) 1637 apply arith 1638 apply (simp add: X64_H.gpRegisters_def word_bits_def 1639 X64.gpRegisters_def) 1640 apply simp 1641 apply (rule ceqv_refl) 1642 apply (ctac(no_vcg) add: getRestartPC_ccorres) 1643 apply simp 1644 apply (ctac(no_vcg) add: setNextPC_ccorres) 1645 apply (ctac (no_vcg) add: postModifyRegisters_ccorres) 1646 apply (rule ccorres_split_nothrow_novcg) 1647 apply (rule ccorres_when[where R=\<top>]) 1648 apply (simp add: from_bool_0 Collect_const_mem) 1649 apply (rule_tac xf'="\<lambda>_. 0" in ccorres_call) 1650 apply (rule restart_ccorres) 1651 apply simp 1652 apply (simp add: xfdc_def) 1653 apply simp 1654 apply (rule ceqv_refl) 1655 apply (rule ccorres_split_nothrow_novcg_dc) 1656 apply (rule_tac R="\<lambda>s. rv = ksCurThread s" 1657 in ccorres_when) 1658 apply (clarsimp simp: rf_sr_ksCurThread) 1659 apply clarsimp 1660 apply (ctac (no_vcg) add: rescheduleRequired_ccorres) 1661 apply (unfold return_returnOk)[1] 1662 apply (rule ccorres_return_CE, simp+)[1] 1663 apply wp 1664 apply (simp add: guard_is_UNIV_def) 1665 apply (wp hoare_drop_imp) 1666 apply (rule_tac Q="\<lambda>rv. invs' and tcb_at' dst" in hoare_strengthen_post[rotated]) 1667 apply (fastforce simp: sch_act_wf_weak) 1668 apply (wpsimp wp: restart_invs')+ 1669 apply (clarsimp simp add: guard_is_UNIV_def) 1670 apply (wp hoare_drop_imp hoare_vcg_if_lift)+ 1671 apply simp 1672 apply (rule mapM_x_wp') 1673 apply (wpsimp) 1674 apply (simp add: guard_is_UNIV_def) 1675 apply (rule hoare_drop_imps) 1676 apply (simp add: sysargs_rel_n_def) 1677 apply (wp mapM_x_wp') 1678 apply (rule hoare_pre, wp asUser_sysargs_rel) 1679 apply clarsimp 1680 apply wpsimp 1681 apply (simp add: guard_is_UNIV_def) 1682 apply (wp) 1683 apply vcg 1684 apply (wp threadGet_wp) 1685 apply vcg 1686 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 1687 apply simp 1688 apply (simp add: performTransfer_def) 1689 apply wp 1690 apply clarsimp 1691 apply vcg 1692 apply (clarsimp simp: n_msgRegisters_def sysargs_rel_n_def invs_valid_objs' invs_no_0_obj' split: if_split) 1693 apply (rule conjI) 1694 apply (cases args, simp) 1695 apply (case_tac list, simp) 1696 apply (case_tac lista, clarsimp simp: unat_eq_0) 1697 apply fastforce 1698 apply (clarsimp simp: frame_gp_registers_convs word_less_nat_alt 1699 sysargs_rel_def n_frameRegisters_def n_msgRegisters_def 1700 split: if_split_asm) 1701 apply (simp add: invs_weak_sch_act_wf invs_valid_objs' invs_queues) 1702 apply (fastforce dest!: global'_no_ex_cap simp: invs'_def valid_state'_def) 1703 done 1704 1705lemma invokeTCB_Suspend_ccorres: 1706 "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') 1707 (invs' and sch_act_simple and tcb_at' t and ex_nonz_cap_to' t) 1708 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}) [] 1709 (invokeTCB (Suspend t)) (Call invokeTCB_Suspend_'proc)" 1710 apply (cinit lift: thread_') 1711 apply (simp add: liftE_def return_returnOk) 1712 apply (ctac(no_vcg) add: suspend_ccorres[OF cteDeleteOne_ccorres]) 1713 apply (rule ccorres_return_CE, simp+)[1] 1714 apply wp 1715 apply (clarsimp simp: from_bool_def true_def) 1716 apply (auto simp: invs'_def valid_state'_def global'_no_ex_cap) 1717 done 1718 1719lemma invokeTCB_Resume_ccorres: 1720 "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') 1721 (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple) 1722 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}) [] 1723 (invokeTCB (Resume t)) (Call invokeTCB_Resume_'proc)" 1724 apply (cinit lift: thread_') 1725 apply (simp add: liftE_def return_returnOk) 1726 apply (ctac(no_vcg) add: restart_ccorres) 1727 apply (rule ccorres_return_CE, simp+)[1] 1728 apply wp 1729 apply (clarsimp simp: from_bool_def true_def) 1730 done 1731 1732lemma Arch_decodeTransfer_spec: 1733 "\<forall>s. \<Gamma> \<turnstile> {s} Call Arch_decodeTransfer_'proc {s'. ret__unsigned_long_' s' = 0}" 1734 by (vcg, simp) 1735 1736lemmas ccorres_split_nothrow_dc 1737 = ccorres_split_nothrow[where r'=dc and xf'=xfdc, OF _ ceqv_refl] 1738 1739lemmas getRegister_ccorres_defer 1740 = ccorres_defer[OF getRegister_ccorres, OF no_fail_asUser [OF no_fail_getRegister]] 1741 1742lemma msg_registers_convs: 1743 "length X64_H.msgRegisters = unat n_msgRegisters" 1744 "n < length X64_H.msgRegisters \<Longrightarrow> 1745 index msgRegistersC n = register_from_H (X64_H.msgRegisters ! n)" 1746 apply (simp_all add: msgRegisters_unfold 1747 X64.msgRegisters_def n_msgRegisters_def 1748 msgRegistersC_def fupdate_def Arrays.update_def) 1749 apply (auto simp: less_Suc_eq fcp_beta) 1750 done 1751 1752lemma mapM_x_split_append: 1753 "mapM_x f xs = do _ \<leftarrow> mapM_x f (take n xs); mapM_x f (drop n xs) od" 1754 using mapM_x_append[where f=f and xs="take n xs" and ys="drop n xs"] 1755 by simp 1756 1757lemma ccorres_abstract_cong: 1758 "\<lbrakk> \<And>s s'. \<lbrakk> P s ; s' \<in> P'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> a s = b s \<rbrakk> \<Longrightarrow> 1759 ccorres_underlying sr G r xf ar axf P P' hs a c 1760 = ccorres_underlying sr G r xf ar axf P P' hs b c" 1761 by (simp add: ccorres_underlying_def split_paired_Ball imp_conjL 1762 cong: conj_cong xstate.case_cong) 1763 1764lemma is_aligned_the_x_strengthen: 1765 "x \<noteq> None \<and> case_option \<top> valid_ipc_buffer_ptr' x s \<longrightarrow> is_aligned (the x) msg_align_bits" 1766 by (clarsimp simp: valid_ipc_buffer_ptr'_def) 1767 1768lemma valid_ipc_buffer_ptr_the_strengthen: 1769 "x \<noteq> None \<and> case_option \<top> valid_ipc_buffer_ptr' x s \<longrightarrow> valid_ipc_buffer_ptr' (the x) s" 1770 by clarsimp 1771 1772 1773lemma lookupIPCBuffer_Some_0: 1774 "\<lbrace>\<top>\<rbrace> lookupIPCBuffer w t \<lbrace>\<lambda>rv s. rv \<noteq> Some 0\<rbrace>" 1775 apply (simp add: lookupIPCBuffer_def 1776 X64_H.lookupIPCBuffer_def 1777 Let_def getThreadBufferSlot_def 1778 locateSlot_conv 1779 cong: if_cong) 1780 apply (wp haskell_assert_wp | wpc | simp)+ 1781 done 1782 1783lemma asUser_valid_ipc_buffer_ptr': 1784 "\<lbrace> valid_ipc_buffer_ptr' p \<rbrace> asUser t m \<lbrace> \<lambda>rv s. valid_ipc_buffer_ptr' p s \<rbrace>" 1785 by (simp add: valid_ipc_buffer_ptr'_def, wp, auto simp: valid_ipc_buffer_ptr'_def) 1786 1787lemma invokeTCB_ReadRegisters_ccorres: 1788notes 1789 nat_min_simps [simp del] 1790 wordSize_def' [simp] 1791 option.case_cong_weak [cong] 1792 prod.case_cong_weak [cong] 1793shows 1794 "ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 1795 (invs' and (\<lambda>s. ksCurThread s = thread) and ct_in_state' ((=) Restart) 1796 and tcb_at' target and sch_act_simple and (\<lambda>s. target \<noteq> ksIdleThread s) 1797 and (\<lambda>_. target \<noteq> thread)) 1798 (UNIV 1799 \<inter> {s. tcb_src_' s = tcb_ptr_to_ctcb_ptr target} 1800 \<inter> {s. suspendSource_' s = from_bool susp} 1801 \<inter> {s. n_' s = n} 1802 \<inter> {s. call_' s = from_bool isCall}) [] 1803 (doE reply \<leftarrow> invokeTCB (ReadRegisters target susp n archCp); 1804 liftE (replyOnRestart thread reply isCall) odE) 1805 (Call invokeTCB_ReadRegisters_'proc)" 1806 apply (rule ccorres_gen_asm) using [[goals_limit=1]] 1807 apply (cinit' lift: tcb_src_' suspendSource_' n_' call_' 1808 simp: invokeTCB_def liftE_bindE bind_assoc) 1809 apply (rule ccorres_symb_exec_r) 1810 apply (rule_tac xf'=thread_' in ccorres_abstract, ceqv) 1811 apply (rename_tac cthread, 1812 rule_tac P="cthread = tcb_ptr_to_ctcb_ptr thread" in ccorres_gen_asm2) 1813 apply (rule ccorres_split_nothrow_dc) 1814 apply (simp add: when_def del: Collect_const split del: if_split) 1815 apply (rule ccorres_cond2[where R=\<top>], simp add: from_bool_0 Collect_const_mem) 1816 apply (ctac add: suspend_ccorres[OF cteDeleteOne_ccorres]) 1817 apply (rule ccorres_return_Skip) 1818 apply (rule ccorres_pre_getCurThread) 1819 apply (simp only: liftE_bindE[symmetric]) 1820 apply (ctac add: Arch_performTransfer_ccorres) 1821 apply (simp add: liftE_bindE Collect_False 1822 del: Collect_const) 1823 apply (simp add: replyOnRestart_def liftE_def bind_assoc when_def 1824 replyFromKernel_def if_to_top_of_bind setMRs_def 1825 zipWithM_x_mapM_x asUser_mapM_x split_def 1826 del: Collect_const cong: if_cong) 1827 apply (rule ccorres_symb_exec_l) 1828 apply (rule ccorres_symb_exec_l[OF _ _ _ empty_fail_getThreadState]) 1829 apply (rule ccorres_if_lhs[OF _ ccorres_False[where P'=UNIV]]) 1830 apply (rule ccorres_if_lhs) 1831 apply (simp add: Collect_True true_def whileAnno_def del: Collect_const) 1832 apply (rule ccorres_rhs_assoc)+ 1833 apply csymbr 1834 apply (ctac add: lookupIPCBuffer_ccorres) 1835 apply (ctac add: setRegister_ccorres) 1836 apply (rule ccorres_stateAssert) 1837 apply (rule ccorres_rhs_assoc2) 1838 apply (rule_tac P="length reply 1839 = min (unat n) (unat n_frameRegisters + unat n_gpRegisters)" 1840 in ccorres_gen_asm) 1841 apply (rule ccorres_split_nothrow_novcg) 1842 apply (rule_tac F="\<lambda>m s. obj_at' (\<lambda>tcb. map ((user_regs o atcbContextGet o tcbArch) tcb) (genericTake n 1843 (X64_H.frameRegisters @ X64_H.gpRegisters)) 1844 = reply) target s" 1845 in ccorres_mapM_x_while) 1846 apply clarsimp 1847 apply (rule ccorres_guard_imp2) 1848 apply (rule ccorres_add_return, 1849 ctac add: getRegister_ccorres_defer[where thread=target]) 1850 apply (ctac add: setRegister_ccorres) 1851 apply wp 1852 apply simp 1853 apply (vcg exspec=getRegister_modifies) 1854 apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets) 1855 apply (clarsimp simp: simpler_gets_def obj_at'_weakenE[OF _ TrueI] 1856 msg_registers_convs) 1857 apply (cut_tac x=na in unat_of_nat64) 1858 apply (simp add: word_bits_def n_msgRegisters_def) 1859 apply (simp add: msg_registers_convs n_msgRegisters_def 1860 word_of_nat_less) 1861 apply (subgoal_tac "na < unat n_frameRegisters") 1862 apply (intro conjI[rotated] allI impI) 1863 apply (assumption | erule sym) 1864 apply (rule frame_gp_registers_convs) 1865 apply (simp add: frame_gp_registers_convs) 1866 apply (drule obj_at_ko_at') 1867 apply (clarsimp simp: obj_at'_def projectKOs asUser_fetch_def 1868 frame_gp_registers_convs genericTake_def 1869 nth_append 1870 split: if_split) 1871 apply (simp add: n_frameRegisters_def n_msgRegisters_def) 1872 apply (simp add: frame_gp_registers_convs msg_registers_convs 1873 n_msgRegisters_def n_frameRegisters_def 1874 n_gpRegisters_def msgMaxLength_def msgLengthBits_def 1875 split: option.split) 1876 apply (simp add: min_def word_less_nat_alt split: if_split)[1] 1877 apply arith 1878 apply (rule allI, rule conseqPre, vcg exspec=setRegister_modifies 1879 exspec=getRegister_modifies) 1880 apply clarsimp 1881 apply (wp asUser_obj_at') 1882 apply simp 1883 apply (simp add: word_bits_def msgMaxLength_def 1884 msg_registers_convs n_msgRegisters_def) 1885 apply ceqv 1886 (* got to split reply into frameregisters part and gpregisters 1887 part remaining, match against 2nd and 4th loop. 3rd loop 1888 never executes with current configuration *) 1889 apply (simp add: msg_registers_convs del: Collect_const) 1890 apply (rule iffD2 [OF ccorres_abstract_cong]) 1891 apply (rule bind_apply_cong[OF _ refl]) 1892 apply (rule_tac n1="min (unat n_frameRegisters - unat n_msgRegisters) (unat n)" 1893 in fun_cong [OF mapM_x_split_append]) 1894 apply (rule_tac P="rva \<noteq> Some 0" in ccorres_gen_asm) 1895 apply (subgoal_tac "(ipcBuffer = NULL) = (rva = None)") 1896 prefer 2 1897 apply (clarsimp simp: option_to_ptr_def option_to_0_def 1898 split: option.split_asm) 1899 apply (simp add: bind_assoc del: Collect_const) 1900 apply (rule_tac xf'=i_' and r'="\<lambda>_ rv. unat rv = min (unat n_frameRegisters) 1901 (min (unat n) 1902 (case rva of None \<Rightarrow> unat n_msgRegisters 1903 | _ \<Rightarrow> unat n_frameRegisters))" 1904 in ccorres_split_nothrow_novcg) 1905 apply (rule ccorres_Cond_rhs) 1906 apply (rule ccorres_rel_imp, 1907 rule_tac F="\<lambda>m s. obj_at' (\<lambda>tcb. map ((user_regs o atcbContextGet o tcbArch) tcb) (genericTake n 1908 (X64_H.frameRegisters @ X64_H.gpRegisters)) 1909 = reply) target s 1910 \<and> valid_ipc_buffer_ptr' (the rva) s 1911 \<and> valid_pspace' s" 1912 and i="unat n_msgRegisters" 1913 in ccorres_mapM_x_while') 1914 apply (intro allI impI, elim conjE exE, hypsubst, simp) 1915 apply (simp add: less_diff_conv) 1916 apply (rule ccorres_guard_imp2) 1917 apply (rule ccorres_add_return, 1918 ctac add: getRegister_ccorres_defer[where thread=target]) 1919 apply (rule ccorres_move_array_assertion_ipc_buffer 1920 | (rule ccorres_flip_Guard, 1921 rule ccorres_move_array_assertion_ipc_buffer))+ 1922 apply (rule storeWordUser_ccorres) 1923 apply wp 1924 apply (vcg exspec=getRegister_modifies) 1925 apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI] 1926 word_size unat_gt_0 option_to_ptr_def 1927 option_to_0_def) 1928 apply (intro conjI[rotated] impI allI) 1929 apply (simp add: n_msgRegisters_def n_frameRegisters_def 1930 word_less_nat_alt) 1931 apply (subst unat_add_lem[THEN iffD1], simp_all add: unat_of_nat)[1] 1932 prefer 3 1933 apply (erule sym) 1934 apply (simp add: n_msgRegisters_def msg_registers_convs 1935 msg_align_bits msgMaxLength_def) 1936 apply (simp(no_asm) add: unat_arith_simps unat_of_nat 1937 cong: if_cong, simp) 1938 apply (simp add: n_msgRegisters_def msg_registers_convs 1939 msg_align_bits msgMaxLength_def) 1940 apply (simp(no_asm) add: unat_arith_simps unat_of_nat 1941 cong: if_cong, simp) 1942 apply (simp add: option_to_ptr_def option_to_0_def 1943 msg_registers_convs upto_enum_word wordSize_def' 1944 del: upt.simps) 1945 apply (rule frame_gp_registers_convs) 1946 apply (simp add: frame_gp_registers_convs less_diff_conv) 1947 apply (subst iffD1 [OF unat_add_lem]) 1948 apply (simp add: n_msgRegisters_def n_frameRegisters_def 1949 word_le_nat_alt unat_of_nat) 1950 apply (simp add: n_frameRegisters_def n_msgRegisters_def 1951 unat_of_nat) 1952 apply (clarsimp simp: valid_ipc_buffer_ptr'_def) 1953 apply (erule aligned_add_aligned) 1954 apply (rule is_aligned_mult_triv2[where n=3, simplified]) 1955 apply (simp add: msg_align_bits_def word_size_bits_def) 1956 apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets 1957 obj_at'_weakenE[OF _ TrueI]) 1958 apply (clarsimp simp: asUser_fetch_def simpler_gets_def 1959 obj_at'_def projectKOs genericTake_def 1960 nth_append frame_gp_registers_convs) 1961 apply (simp add: n_msgRegisters_def unat_of_nat n_frameRegisters_def) 1962 apply (subst iffD1 [OF unat_add_lem]) 1963 apply (simp add: unat_of_nat)+ 1964 apply (clarsimp simp: less_diff_conv) 1965 apply (simp add: frame_gp_registers_convs msg_registers_convs 1966 n_msgRegisters_def n_frameRegisters_def 1967 n_gpRegisters_def Types_H.msgMaxLength_def 1968 Types_H.msgLengthBits_def 1969 split: option.split) 1970 apply (simp add: min_def word_less_nat_alt split: if_split)[1] 1971 apply (simp split: if_split_asm, arith+)[1] 1972 apply (rule allI, rule conseqPre, vcg) 1973 apply clarsimp 1974 apply (wp) 1975 apply (clarsimp simp: less_diff_conv) 1976 apply (simp add: word_bits_def n_msgRegisters_def n_frameRegisters_def 1977 Types_H.msgLengthBits_def Types_H.msgMaxLength_def 1978 msg_registers_convs) 1979 apply (clarsimp simp: n_msgRegisters_def n_frameRegisters_def 1980 msgMaxLength_def Types_H.msgLengthBits_def 1981 n_gpRegisters_def msg_registers_convs 1982 split: option.split_asm) 1983 apply (simp add: min_def split: if_split_asm if_split) 1984 apply (drule_tac s=rv'a in sym, simp) 1985 apply (rule_tac P=\<top> and P'="{s. i_' s = rv'a}" in ccorres_inst) 1986 apply clarsimp 1987 apply (elim disjE impCE) 1988 apply (clarsimp simp: word_le_nat_alt linorder_not_less) 1989 apply (subst (asm) unat_of_nat64) 1990 apply (simp add: n_msgRegisters_def word_bits_def) 1991 apply (clarsimp simp: mapM_x_Nil) 1992 apply (rule ccorres_guard_imp2, rule ccorres_return_Skip') 1993 apply (simp add: n_msgRegisters_def n_frameRegisters_def 1994 n_gpRegisters_def cong: option.case_cong) 1995 apply (simp add: min_def split: if_split option.split) 1996 apply (simp add: mapM_x_Nil) 1997 apply (rule ccorres_guard_imp2, rule ccorres_return_Skip') 1998 apply (simp add: n_msgRegisters_def n_frameRegisters_def 1999 n_gpRegisters_def cong: option.case_cong) 2000 apply (simp add: min_def split: if_split option.split) 2001 apply (clarsimp simp only: unat_arith_simps, simp) 2002 apply (clarsimp simp: less_diff_conv word_le_nat_alt linorder_not_less) 2003 apply (subst(asm) unat_of_nat64) 2004 apply (simp add: word_bits_def n_msgRegisters_def) 2005 apply (simp add: mapM_x_Nil n_frameRegisters_def n_gpRegisters_def) 2006 apply (rule ccorres_guard_imp2, rule ccorres_return_Skip') 2007 apply (simp add: n_msgRegisters_def n_frameRegisters_def 2008 n_gpRegisters_def cong: option.case_cong) 2009 apply ceqv 2010 apply csymbr 2011 apply csymbr 2012 apply (rule iffD1[OF ccorres_expand_while_iff_Seq]) 2013 apply (rule ccorres_cond_false) 2014 apply (rule ccorres_split_nothrow_novcg) 2015 apply (rule_tac xf'=i_' in ccorres_abstract, ceqv) 2016 apply (rename_tac i_c, rule_tac P="i_c = 0" in ccorres_gen_asm2) 2017 apply (simp add: drop_zip del: Collect_const) 2018 apply (rule ccorres_Cond_rhs) 2019 apply (simp del: Collect_const) 2020 apply (rule_tac F="\<lambda>m s. obj_at' (\<lambda>tcb. map ((user_regs o atcbContextGet o tcbArch) tcb) (genericTake n 2021 (X64_H.frameRegisters @ X64_H.gpRegisters)) 2022 = reply) target s 2023 \<and> valid_ipc_buffer_ptr' (the rva) s \<and> valid_pspace' s" 2024 and i="0" in ccorres_mapM_x_while') 2025 apply (clarsimp simp: less_diff_conv drop_zip) 2026 apply (rule ccorres_guard_imp2) 2027 apply (rule ccorres_add_return, 2028 ctac add: getRegister_ccorres_defer[where thread=target]) 2029 apply (rule ccorres_move_array_assertion_ipc_buffer 2030 | (rule ccorres_flip_Guard, 2031 rule ccorres_move_array_assertion_ipc_buffer))+ 2032 apply (rule storeWordUser_ccorres) 2033 apply wp 2034 apply (vcg exspec=getRegister_modifies) 2035 apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI] 2036 word_size unat_gt_0 option_to_ptr_def 2037 option_to_0_def) 2038 apply (intro conjI[rotated] impI allI) 2039 apply (simp add: n_frameRegisters_def n_msgRegisters_def 2040 length_msgRegisters word_of_nat_less 2041 n_gpRegisters_def msgMaxLength_def) 2042 2043 subgoal 2044 apply (case_tac "unat n < 14", simp_all) 2045 apply (simp add: le_def[symmetric]) 2046 apply (drule min_absorb1, simp) 2047 done 2048 prefer 3 2049 apply (erule sym) 2050 apply (simp add: n_frameRegisters_def n_msgRegisters_def msg_registers_convs 2051 msg_align_bits msgMaxLength_def) 2052 apply (simp(no_asm) add: unat_arith_simps unat_of_nat 2053 cong: if_cong, simp) 2054 apply (simp add: n_frameRegisters_def n_msgRegisters_def msg_registers_convs 2055 msg_align_bits msgMaxLength_def) 2056 apply (simp(no_asm) add: unat_arith_simps unat_of_nat 2057 cong: if_cong, simp) 2058 apply (simp add: option_to_ptr_def option_to_0_def 2059 msg_registers_convs upto_enum_word 2060 n_msgRegisters_def n_frameRegisters_def 2061 n_gpRegisters_def msgMaxLength_def msgLengthBits_def 2062 del: upt.simps upt_rec_numeral) 2063 apply (simp add: min_def split: if_split_asm) 2064 apply (rule frame_gp_registers_convs) 2065 apply (simp add: frame_gp_registers_convs n_msgRegisters_def n_frameRegisters_def 2066 n_gpRegisters_def msgMaxLength_def msgLengthBits_def 2067 unat_of_nat) 2068 apply (clarsimp simp: valid_ipc_buffer_ptr'_def, 2069 erule aligned_add_aligned) 2070 apply (rule is_aligned_mult_triv2[where n=3, simplified]) 2071 apply (simp add: msg_align_bits_def word_size_bits_def) 2072 apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets 2073 obj_at'_weakenE[OF _ TrueI]) 2074 apply (clarsimp simp: asUser_fetch_def simpler_gets_def 2075 obj_at'_def projectKOs genericTake_def 2076 nth_append frame_gp_registers_convs 2077 n_frameRegisters_def n_gpRegisters_def 2078 n_msgRegisters_def frame_gp_registers_convs 2079 cong: if_cong split: if_split) 2080 apply (clarsimp simp: frame_gp_registers_convs n_gpRegisters_def 2081 min.absorb1 unat_of_nat) 2082 apply (clarsimp simp: less_diff_conv) 2083 apply (clarsimp simp: nth_append frame_gp_registers_convs 2084 n_frameRegisters_def n_gpRegisters_def 2085 n_msgRegisters_def frame_gp_registers_convs 2086 Types_H.msgMaxLength_def Types_H.msgLengthBits_def 2087 msg_registers_convs 2088 cong: if_cong split: if_split) 2089 apply (simp add: word_less_nat_alt unat_of_nat) 2090 apply (simp add: iffD1[OF unat_add_lem] cong: conj_cong) 2091 apply (simp add: min_def 2092 split: if_split if_split_asm, 2093 unat_arith, 2094 fastforce simp: unat_eq_0)[1] 2095 apply (rule allI, rule conseqPre, vcg) 2096 apply clarsimp 2097 apply wp 2098 apply (simp add: word_bits_def n_frameRegisters_def n_gpRegisters_def 2099 n_msgRegisters_def) 2100 apply (simp add: min_less_iff_disj less_imp_diff_less) 2101 apply (simp add: drop_zip n_gpRegisters_def) 2102 apply (elim disjE impCE) 2103 apply (clarsimp simp: mapM_x_Nil) 2104 apply (rule ccorres_return_Skip') 2105 apply (simp add: linorder_not_less word_le_nat_alt 2106 drop_zip mapM_x_Nil n_frameRegisters_def 2107 min.absorb1 n_msgRegisters_def) 2108 apply (rule ccorres_guard_imp2, rule ccorres_return_Skip') 2109 apply simp 2110 apply ceqv 2111 apply csymbr 2112 apply (rule ccorres_rhs_assoc2) 2113 apply (ctac (no_vcg) add: setMessageInfo_ccorres) 2114 apply (ctac (no_vcg)) 2115 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2116 apply (rule allI, rule conseqPre, vcg) 2117 apply (clarsimp simp: return_def) 2118 apply (wp | simp add: valid_tcb_state'_def)+ 2119 apply (clarsimp simp: ThreadState_Running_def mask_def) 2120 apply (rule mapM_x_wp') 2121 apply (rule hoare_pre) 2122 apply (wp sch_act_wf_lift valid_queues_lift tcb_in_cur_domain'_lift) 2123 apply clarsimp 2124 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) 2125 apply (simp add: message_info_to_H_def) 2126 apply (clarsimp simp: n_frameRegisters_def n_msgRegisters_def 2127 n_gpRegisters_def field_simps upto_enum_word 2128 word_less_nat_alt Types_H.msgMaxLength_def 2129 Types_H.msgLengthBits_def 2130 simp del: upt.simps 2131 split: option.split_asm) 2132 apply (clarsimp simp: min_def iffD2 [OF mask_eq_iff_w2p] word_size 2133 word_less_nat_alt 2134 split: if_split_asm dest!: word_unat.Rep_inverse') 2135 apply (clarsimp simp: length_msgRegisters n_msgRegisters_def) 2136 apply (clarsimp simp: min_def iffD2 [OF mask_eq_iff_w2p] word_size 2137 word_less_nat_alt 2138 split: if_split_asm dest!: word_unat.Rep_inverse') 2139 apply unat_arith 2140 apply simp 2141 apply (wp mapM_x_wp' sch_act_wf_lift valid_queues_lift static_imp_wp 2142 tcb_in_cur_domain'_lift) 2143 apply (simp add: n_frameRegisters_def n_msgRegisters_def 2144 guard_is_UNIV_def) 2145 apply simp 2146 apply (rule mapM_x_wp') 2147 apply (rule hoare_pre) 2148 apply (wp asUser_obj_at'[where t'=target] static_imp_wp 2149 asUser_valid_ipc_buffer_ptr') 2150 apply clarsimp 2151 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem 2152 msg_registers_convs n_msgRegisters_def 2153 n_frameRegisters_def n_gpRegisters_def 2154 msgMaxLength_def msgLengthBits_def 2155 word_less_nat_alt unat_of_nat) 2156 apply (simp add: min_def split: if_split_asm) 2157 apply (wp_once hoare_drop_imps) 2158 apply (wp asUser_obj_at'[where t'=target] static_imp_wp 2159 asUser_valid_ipc_buffer_ptr') 2160 apply (vcg exspec=setRegister_modifies) 2161 apply simp 2162 apply (strengthen valid_ipc_buffer_ptr_the_strengthen) 2163 apply simp 2164 apply (wp lookupIPCBuffer_Some_0 | wp_once hoare_drop_imps)+ 2165 apply (simp add: Collect_const_mem X64_H.badgeRegister_def 2166 X64.badgeRegister_def X64.capRegister_def 2167 "StrictC'_register_defs") 2168 apply (vcg exspec=lookupIPCBuffer_modifies) 2169 apply (simp add: false_def) 2170 apply (ctac(no_vcg) add: setThreadState_ccorres) 2171 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2172 apply (rule allI, rule conseqPre, vcg) 2173 apply (simp add: return_def) 2174 apply wp+ 2175 apply (simp cong: rev_conj_cong) 2176 apply wp 2177 apply (wp asUser_inv mapM_wp' getRegister_inv 2178 asUser_get_registers[simplified] static_imp_wp)+ 2179 apply (rule hoare_strengthen_post, rule asUser_get_registers) 2180 apply (clarsimp simp: obj_at'_def genericTake_def 2181 frame_gp_registers_convs) 2182 apply arith 2183 apply (wp static_imp_wp) 2184 apply simp 2185 apply (rule ccorres_inst[where P=\<top> and P'=UNIV], simp) 2186 apply (simp add: performTransfer_def) 2187 apply wp 2188 apply (simp add: Collect_const_mem "StrictC'_thread_state_defs" 2189 mask_def) 2190 apply vcg 2191 apply (rule_tac Q="\<lambda>rv. invs' and st_tcb_at' ((=) Restart) thread 2192 and tcb_at' target" in hoare_post_imp) 2193 apply (clarsimp simp: pred_tcb_at') 2194 apply (auto elim!: pred_tcb'_weakenE)[1] 2195 apply (wp suspend_st_tcb_at') 2196 apply (vcg exspec=suspend_modifies) 2197 apply vcg 2198 apply (rule conseqPre, vcg, clarsimp) 2199 apply (clarsimp simp: rf_sr_ksCurThread ct_in_state'_def true_def dc_def 2200 split: if_split) 2201 done 2202 2203lemma decodeReadRegisters_ccorres: 2204 "ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2205 (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' 2206 and sysargs_rel args buffer 2207 and tcb_at' (capTCBPtr cp) and ex_nonz_cap_to' (capTCBPtr cp) 2208 and K (isThreadCap cp)) 2209 (UNIV 2210 \<inter> {s. ccap_relation cp (cap_' s)} 2211 \<inter> {s. unat (length___unsigned_long_' s) = length args} 2212 \<inter> {s. call_' s = from_bool isCall} 2213 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 2214 (decodeReadRegisters args cp 2215 >>= invocationCatch thread isBlocking isCall InvokeTCB) 2216 (Call decodeReadRegisters_'proc)" 2217 apply (cinit' lift: cap_' length___unsigned_long_' call_' buffer_') 2218 apply (simp add: decodeReadRegisters_def decodeTransfer_def 2219 del: Collect_const cong: list.case_cong) 2220 apply wpc 2221 apply (drule word_unat.Rep_inverse') 2222 apply (simp add: throwError_bind invocationCatch_def 2223 cong: StateSpace.state.fold_congs globals.fold_congs) 2224 apply (rule syscall_error_throwError_ccorres_n) 2225 apply (simp add: syscall_error_to_H_cases) 2226 apply wpc 2227 apply (drule word_unat.Rep_inverse') 2228 apply (simp add: throwError_bind invocationCatch_def 2229 cong: StateSpace.state.fold_congs globals.fold_congs) 2230 apply (rule syscall_error_throwError_ccorres_n) 2231 apply (simp add: syscall_error_to_H_cases) 2232 apply (simp add: word_less_nat_alt Collect_False del: Collect_const) 2233 apply (rule ccorres_add_return, 2234 ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer]) 2235 apply (rule ccorres_add_return, 2236 ctac add: getSyscallArg_ccorres_foo[where args=args and n=1 and buffer=buffer]) 2237 apply (rule ccorres_move_const_guards)+ 2238 apply (simp add: rangeCheck_def unlessE_whenE whenE_def if_to_top_of_bindE 2239 ccorres_seq_cond_raise if_to_top_of_bind 2240 del: Collect_const) 2241 apply (rule ccorres_cond2[where R=\<top>]) 2242 apply (simp add: frame_gp_registers_convs n_frameRegisters_def 2243 n_gpRegisters_def Collect_const_mem) 2244 apply unat_arith 2245 apply (simp add: throwError_bind invocationCatch_def 2246 cong: StateSpace.state.fold_congs globals.fold_congs) 2247 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2248 apply vcg 2249 apply (rule conseqPre, vcg) 2250 apply (clarsimp simp: throwError_def return_def intr_and_se_rel_def 2251 syscall_error_rel_def syscall_error_to_H_cases 2252 exception_defs Collect_const_mem) 2253 apply (simp add: frame_gp_registers_convs n_frameRegisters_def 2254 n_gpRegisters_def) 2255 apply (simp add: ccorres_invocationCatch_Inr returnOk_bind 2256 performInvocation_def 2257 del: Collect_const) 2258 apply csymbr 2259 apply csymbr 2260 apply csymbr 2261 apply (simp add: liftE_bindE bind_assoc) 2262 apply (rule ccorres_pre_getCurThread) 2263 apply (rule ccorres_cond_seq) 2264 apply (rule_tac R="\<lambda>s. rv = ksCurThread s \<and> isThreadCap cp" and P="\<lambda>s. capTCBPtr cp = rv" in ccorres_cond_both) 2265 apply clarsimp 2266 apply (frule rf_sr_ksCurThread) 2267 apply clarsimp 2268 apply (frule (1) cap_get_tag_isCap[symmetric, THEN iffD1]) 2269 apply (drule (1) cap_get_tag_to_H) 2270 apply clarsimp 2271 apply (rule iffI) 2272 apply (drule_tac t="ksCurThread s" in sym) 2273 apply simp 2274 apply simp 2275 apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) 2276 apply simp 2277 apply (simp add: throwError_bind invocationCatch_def 2278 cong: StateSpace.state.fold_congs globals.fold_congs) 2279 apply (rule syscall_error_throwError_ccorres_n) 2280 apply (simp add: syscall_error_to_H_cases) 2281 apply (rule_tac P="capTCBPtr cp \<noteq> rv" in ccorres_gen_asm) 2282 apply (simp add: returnOk_bind) 2283 apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) 2284 apply (ctac add: setThreadState_ccorres) 2285 apply csymbr 2286 apply (rule ccorres_Guard_Seq)+ 2287 apply (rule ccorres_nondet_refinement) 2288 apply (rule is_nondet_refinement_bindE) 2289 apply (rule is_nondet_refinement_refl) 2290 apply (simp split: if_split) 2291 apply (rule conjI[rotated], rule impI, rule is_nondet_refinement_refl) 2292 apply (rule impI) 2293 apply (rule is_nondet_refinement_alternative1) 2294 apply (simp add: performInvocation_def) 2295 apply (rule ccorres_add_returnOk) 2296 apply (ctac(no_vcg) add: invokeTCB_ReadRegisters_ccorres) 2297 apply (rule ccorres_return_CE, simp+)[1] 2298 apply (rule ccorres_return_C_errorE, simp+)[1] 2299 apply wp 2300 apply (wp ct_in_state'_set sts_invs_minor') 2301 apply (simp add: Collect_const_mem intr_and_se_rel_def 2302 cintr_def exception_defs) 2303 apply (vcg exspec=setThreadState_modifies) 2304 apply wp 2305 apply (vcg exspec=getSyscallArg_modifies) 2306 apply wp 2307 apply (vcg exspec=getSyscallArg_modifies) 2308 apply (clarsimp simp: Collect_const_mem rf_sr_ksCurThread 2309 "StrictC'_thread_state_defs" word_sless_def word_sle_def 2310 mask_eq_iff_w2p word_size isCap_simps 2311 ReadRegistersFlags_defs tcb_at_invs' 2312 cap_get_tag_isCap capTCBPtr_eq) 2313 apply (frule global'_no_ex_cap[OF invs_valid_global'], clarsimp) 2314 apply (rule conjI) 2315 apply clarsimp 2316 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 2317 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 2318 apply (auto simp: ct_in_state'_def n_frameRegisters_def n_gpRegisters_def 2319 valid_tcb_state'_def 2320 elim!: pred_tcb'_weakenE 2321 dest!: st_tcb_at_idle_thread')[1] 2322 apply (clarsimp simp: from_bool_def word_and_1 split: if_split) 2323 done 2324 2325lemma decodeWriteRegisters_ccorres: 2326 "ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2327 (invs' and sch_act_simple 2328 and (\<lambda>s. ksCurThread s = thread) and ct_active' and K (isThreadCap cp) 2329 and valid_cap' cp and (\<lambda>s. \<forall>x \<in> zobj_refs' cp. ex_nonz_cap_to' x s) 2330 and sysargs_rel args buffer) 2331 (UNIV 2332 \<inter> {s. ccap_relation cp (cap_' s)} 2333 \<inter> {s. unat (length___unsigned_long_' s) = length args} 2334 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 2335 (decodeWriteRegisters args cp 2336 >>= invocationCatch thread isBlocking isCall InvokeTCB) 2337 (Call decodeWriteRegisters_'proc)" 2338 apply (cinit' lift: cap_' length___unsigned_long_' buffer_' simp: decodeWriteRegisters_def) 2339 apply (rename_tac length' cap') 2340 apply (rule ccorres_Cond_rhs_Seq) 2341 apply wpc 2342 apply (simp add: throwError_bind invocationCatch_def 2343 cong: StateSpace.state.fold_congs globals.fold_congs) 2344 apply (rule syscall_error_throwError_ccorres_n) 2345 apply (simp add: syscall_error_to_H_cases) 2346 apply (simp add: word_less_nat_alt) 2347 apply (simp add: throwError_bind invocationCatch_def 2348 cong: StateSpace.state.fold_congs globals.fold_congs) 2349 apply (rule syscall_error_throwError_ccorres_n) 2350 apply (simp add: syscall_error_to_H_cases) 2351 apply (simp add: word_less_nat_alt del: Collect_const) 2352 apply (rule_tac P="\<lambda>a. ccorres rvr xf P P' hs a c" for rvr xf P P' hs c in ssubst, 2353 rule bind_cong [OF _ refl], rule list_case_helper, 2354 clarsimp simp: tl_drop_1)+ 2355 apply (rule ccorres_add_return) 2356 apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer]) 2357 apply (rule ccorres_add_return) 2358 apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=1 and buffer=buffer]) 2359 apply (rule_tac P="unat (of_nat (length args) :: machine_word) = length args" 2360 in ccorres_gen_asm) 2361 apply (simp add: unat_sub word_le_nat_alt genericLength_def 2362 word_less_nat_alt hd_drop_conv_nth2 tl_drop_1 2363 del: Collect_const) 2364 apply (rule ccorres_Cond_rhs_Seq) 2365 apply (simp add: whenE_def throwError_bind invocationCatch_def 2366 cong: StateSpace.state.fold_congs globals.fold_congs) 2367 apply (rule syscall_error_throwError_ccorres_n) 2368 apply (simp add: syscall_error_to_H_cases) 2369 apply (simp add: whenE_def decodeTransfer_def returnOk_bind del: Collect_const) 2370 apply csymbr 2371 apply csymbr 2372 apply csymbr 2373 apply (simp add: liftE_bindE bind_assoc) 2374 apply (rule ccorres_pre_getCurThread) 2375 apply (rule ccorres_cond_seq) 2376 apply (rule_tac R="\<lambda>s. rv = ksCurThread s \<and> isThreadCap cp" and P="\<lambda>s. capTCBPtr cp = rv" in ccorres_cond_both) 2377 apply clarsimp 2378 apply (frule rf_sr_ksCurThread) 2379 apply clarsimp 2380 apply (frule (1) cap_get_tag_isCap[symmetric, THEN iffD1]) 2381 apply (drule (1) cap_get_tag_to_H) 2382 apply clarsimp 2383 apply (rule iffI) 2384 apply (drule_tac t="ksCurThread s" in sym) 2385 apply simp 2386 apply simp 2387 apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) 2388 apply simp 2389 apply (simp add: throwError_bind invocationCatch_def 2390 cong: StateSpace.state.fold_congs globals.fold_congs) 2391 apply (rule syscall_error_throwError_ccorres_n) 2392 apply (simp add: syscall_error_to_H_cases) 2393 apply (rule_tac P="capTCBPtr cp \<noteq> rv" in ccorres_gen_asm) 2394 apply (simp add: returnOk_bind) 2395 apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) 2396 apply (ctac add: setThreadState_ccorres) 2397 apply (rule ccorres_Guard_Seq)+ 2398 apply (simp add: performInvocation_def) 2399 apply (ctac(no_vcg) add: invokeTCB_WriteRegisters_ccorres 2400 [where args=args and someNum="unat (args ! 1)"]) 2401 apply (simp add: dc_def[symmetric] o_def) 2402 apply (rule ccorres_alternative2, rule ccorres_return_CE, simp+) 2403 apply (rule ccorres_return_C_errorE, simp+)[1] 2404 apply wp[1] 2405 apply simp 2406 apply (wp sts_invs_minor' setThreadState_sysargs_rel) 2407 apply (simp add: Collect_const_mem cintr_def intr_and_se_rel_def 2408 exception_defs) 2409 apply (vcg exspec=setThreadState_modifies) 2410 apply wp 2411 apply (vcg exspec=getSyscallArg_modifies) 2412 apply wp 2413 apply (vcg exspec=getSyscallArg_modifies) 2414 apply (clarsimp simp: Collect_const_mem ct_in_state'_def pred_tcb_at') 2415 apply (simp add: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) 2416 apply (clarsimp simp: valid_cap'_def "StrictC'_thread_state_defs" 2417 mask_eq_iff_w2p word_size rf_sr_ksCurThread 2418 WriteRegisters_resume_def word_sle_def word_sless_def 2419 numeral_eqs) 2420 apply (frule arg_cong[where f="\<lambda>x. unat (of_nat x :: machine_word)"], 2421 simp(no_asm_use) only: word_unat.Rep_inverse o_def, 2422 simp) 2423 apply (rule conjI) 2424 apply clarsimp 2425 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def word_less_nat_alt) 2426 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def word_less_nat_alt) 2427 apply (auto simp: genericTake_def cur_tcb'_def linorder_not_less word_le_nat_alt 2428 valid_tcb_state'_def 2429 elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1] 2430 apply (intro allI impI) 2431 apply (rule disjCI2) 2432 apply (clarsimp simp: genericTake_def linorder_not_less) 2433 apply (subst hd_conv_nth, clarsimp simp: unat_eq_0) 2434 apply (clarsimp simp: from_bool_def word_and_1 2435 split: if_split) 2436 done 2437 2438lemma excaps_map_Nil: "(excaps_map caps = []) = (caps = [])" 2439 by (simp add: excaps_map_def) 2440 2441(* FIXME: move *) 2442lemma and_eq_0_is_nth: 2443 fixes x :: "('a :: len) word" 2444 shows "y = 1 << n \<Longrightarrow> ((x && y) = 0) = (\<not> (x !! n))" 2445 by (metis (poly_guards_query) and_eq_0_is_nth) 2446 2447(* FIXME: move *) 2448lemmas and_neq_0_is_nth = arg_cong [where f=Not, OF and_eq_0_is_nth, simplified] 2449 2450lemma decodeCopyRegisters_ccorres: 2451 "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow> 2452 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2453 (invs' and sch_act_simple 2454 and (\<lambda>s. ksCurThread s = thread) and ct_active' 2455 and (excaps_in_mem extraCaps o ctes_of) 2456 and (\<lambda>s. \<forall>v \<in> set extraCaps. 2457 ex_cte_cap_wp_to' isCNodeCap (snd v) s) 2458 and tcb_at' (capTCBPtr cp) and ex_nonz_cap_to' (capTCBPtr cp) 2459 and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v). 2460 ex_nonz_cap_to' y s) 2461 and sysargs_rel args buffer 2462 and K (isThreadCap cp)) 2463 (UNIV 2464 \<inter> {s. ccap_relation cp (cap_' s)} 2465 \<inter> {s. unat (length___unsigned_long_' s) = length args} 2466 \<inter> {s. excaps_' s = extraCaps'} 2467 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 2468 (decodeCopyRegisters args cp (map fst extraCaps) 2469 >>= invocationCatch thread isBlocking isCall InvokeTCB) 2470 (Call decodeCopyRegisters_'proc)" 2471 apply (cinit' lift: cap_' length___unsigned_long_' excaps_' buffer_' simp: decodeCopyRegisters_def) 2472 apply csymbr 2473 apply wpc 2474 apply (simp add: if_1_0_0 unat_eq_0) 2475 apply (rule ccorres_cond_true_seq) 2476 apply (simp add: invocationCatch_def throwError_bind 2477 cong: StateSpace.state.fold_congs globals.fold_congs) 2478 apply (rule syscall_error_throwError_ccorres_n) 2479 apply (simp add: syscall_error_to_H_cases) 2480 apply (simp add: if_1_0_0 del: Collect_const) 2481 apply (subst unat_eq_0[symmetric], simp add: Collect_False del: Collect_const) 2482 apply csymbr 2483 apply (simp add: if_1_0_0 interpret_excaps_test_null decodeTransfer_def 2484 del: Collect_const) 2485 apply (rule ccorres_Cond_rhs_Seq) 2486 apply (simp add: excaps_map_def invocationCatch_def throwError_bind null_def 2487 cong: StateSpace.state.fold_congs globals.fold_congs) 2488 apply (rule syscall_error_throwError_ccorres_n) 2489 apply (simp add: syscall_error_to_H_cases) 2490 apply (simp add: excaps_map_def null_def del: Collect_const) 2491 apply (rule ccorres_add_return, 2492 ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer]) 2493 apply (rule ccorres_symb_exec_r) 2494 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0]) 2495 apply (rule ccorres_move_c_guard_cte) 2496 apply ctac 2497 apply csymbr 2498 apply (simp add: cap_get_tag_isCap if_1_0_0 del: Collect_const) 2499 apply (rule ccorres_assert2) 2500 apply (rule ccorres_Cond_rhs_Seq) 2501 apply (rule_tac P="Q' (capTCBPtr rva) rva" for Q' 2502 in ccorres_inst) 2503 apply (rule ccorres_rhs_assoc)+ 2504 apply (csymbr, csymbr) 2505 apply (simp add: hd_map del: Collect_const, 2506 simp add: hd_conv_nth del: Collect_const) 2507 apply (simp only: cap_get_tag_isCap[symmetric], 2508 drule(1) cap_get_tag_to_H) 2509 apply (simp add: case_bool_If if_to_top_of_bindE 2510 if_to_top_of_bind 2511 del: Collect_const cong: if_cong) 2512 apply (simp add: to_bool_def returnOk_bind Collect_True 2513 ccorres_invocationCatch_Inr performInvocation_def 2514 del: Collect_const) 2515 apply (ctac add: setThreadState_ccorres) 2516 apply csymbr 2517 apply (rule ccorres_Guard_Seq)+ 2518 apply (ctac add: invokeTCB_CopyRegisters_ccorres) 2519 apply simp 2520 apply (rule ccorres_alternative2) 2521 apply (rule ccorres_return_CE, simp+)[1] 2522 apply (rule ccorres_return_C_errorE, simp+)[1] 2523 apply wp 2524 apply (simp add: cintr_def intr_and_se_rel_def exception_defs) 2525 apply (vcg exspec=invokeTCB_CopyRegisters_modifies) 2526 apply (wp sts_invs_minor') 2527 apply (simp add: Collect_const_mem) 2528 apply (vcg exspec=setThreadState_modifies) 2529 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2530 apply vcg 2531 apply (rule conseqPre, vcg) 2532 apply (simp add: hd_map isCap_simps hd_conv_nth) 2533 apply (clarsimp simp: invocationCatch_def throwError_bind 2534 split: capability.split, 2535 auto simp: throwError_def return_def intr_and_se_rel_def 2536 syscall_error_rel_def syscall_error_to_H_cases 2537 exception_defs)[1] 2538 apply (simp add: getSlotCap_def) 2539 apply (wp getCTE_wp) 2540 apply (simp add: Collect_const_mem if_1_0_0 cap_get_tag_isCap) 2541 apply vcg 2542 apply (simp add: Collect_const_mem) 2543 apply vcg 2544 apply (rule conseqPre, vcg) 2545 apply clarsimp 2546 apply wp 2547 apply (simp add: Collect_const_mem) 2548 apply (vcg exspec=getSyscallArg_modifies) 2549 apply (clarsimp simp: Collect_const_mem excaps_map_Nil) 2550 apply (rule conjI) 2551 apply (clarsimp simp: excaps_in_mem_def neq_Nil_conv 2552 slotcap_in_mem_def cte_wp_at_ctes_of 2553 ct_in_state'_def pred_tcb_at') 2554 apply (rule conjI) 2555 apply (clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 2556 apply (clarsimp simp: isCap_simps simp del: capMasterCap_maskCapRights) 2557 apply (frule ctes_of_valid', clarsimp+) 2558 apply (auto simp: valid_cap'_def excaps_map_def valid_tcb_state'_def 2559 elim!: pred_tcb'_weakenE 2560 dest!: st_tcb_at_idle_thread' interpret_excaps_eq)[1] 2561 apply (clarsimp simp: word_sle_def CopyRegistersFlags_defs word_sless_def 2562 "StrictC'_thread_state_defs" rf_sr_ksCurThread 2563 split: if_split) 2564 apply (drule interpret_excaps_eq) 2565 apply (clarsimp simp: mask_def excaps_map_def split_def ccap_rights_relation_def 2566 rightsFromWord_wordFromRights excaps_map_Nil) 2567 apply (simp only: cap_get_tag_isCap[symmetric], 2568 drule(1) cap_get_tag_to_H) 2569 apply (clarsimp simp: cap_get_tag_isCap to_bool_def) 2570 apply (auto simp: unat_eq_of_nat word_and_1_shiftls 2571 word_and_1_shiftl [where n=3,simplified] cap_get_tag_isCap[symmetric] split: if_split_asm) 2572 done 2573 2574(* FIXME: move *) 2575lemma ucast_le_ucast_8_32: 2576 "(ucast x \<le> (ucast y :: word32)) = (x \<le> (y :: word8))" 2577 by (simp add: word_le_nat_alt) 2578 2579method wrong_cap_throwError_ccorres = solves \<open> 2580 (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2581 , vcg 2582 , (rule conseqPre, vcg) 2583 , (auto simp: syscall_error_rel_def syscall_error_to_H_cases isCap_simps 2584 exception_defs throwError_def return_def if_1_0_0 2585 split: capability.split arch_capability.split if_split_asm)[1] 2586 \<close> 2587 2588add_try_method wrong_cap_throwError_ccorres 2589 2590lemma checkValidIPCBuffer_ccorres: 2591 "ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2592 (invs') (UNIV \<inter> {s. vptr_' s = vptr} \<inter> {s. ccap_relation cp (cap_' s)}) [] 2593 (checkValidIPCBuffer vptr cp) 2594 (Call checkValidIPCBuffer_'proc)" 2595 apply (simp add:checkValidIPCBuffer_def X64_H.checkValidIPCBuffer_def) 2596 apply (cases "isArchPageCap cp \<and> \<not> isDeviceCap cp") 2597 apply (simp only: isCap_simps isDeviceCap.simps, safe)[1] 2598 apply (cinit lift: vptr_' cap_') 2599 apply (simp add: X64_H.checkValidIPCBuffer_def if_1_0_0 del: Collect_const) 2600 apply csymbr 2601 apply (rule ccorres_cond_false_seq) 2602 apply simp 2603 apply csymbr 2604 apply (rule ccorres_cond_false_seq) 2605 apply clarsimp 2606 apply (simp only:Cond_if_mem) 2607 apply (rule ccorres_Cond_rhs_Seq) 2608 apply (clarsimp simp add: msgAlignBits_def mask_def whenE_def) 2609 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2610 apply vcg 2611 apply (rule conseqPre, vcg) 2612 apply (clarsimp simp: throwError_def return_def exception_defs 2613 syscall_error_rel_def syscall_error_to_H_cases) 2614 apply (simp add: whenE_def msgAlignBits_def mask_def) 2615 apply (rule ccorres_return_CE, simp+)[1] 2616 apply (clarsimp simp: cap_get_tag_isCap isCap_simps pageSize_def 2617 Collect_const_mem if_1_0_0 ccap_relation_page_is_device 2618 word_sle_def) 2619 apply (cases "isArchPageCap cp") 2620 apply (simp only: isCap_simps isDeviceCap.simps)[1] 2621 apply clarsimp 2622 apply (cinit lift: vptr_' cap_') 2623 apply (simp add: X64_H.checkValidIPCBuffer_def if_1_0_0 del: Collect_const) 2624 apply csymbr 2625 apply (rule ccorres_cond_false_seq) 2626 apply simp 2627 apply csymbr 2628 apply (rule ccorres_cond_true_seq) 2629 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2630 apply vcg 2631 apply (rule conseqPre, vcg) 2632 apply (clarsimp simp: throwError_def return_def exception_defs 2633 syscall_error_rel_def syscall_error_to_H_cases) 2634 apply (simp add: cap_get_tag_isCap isCap_simps pageSize_def ccap_relation_page_is_device) 2635 apply (cinit' lift: vptr_' cap_') 2636 apply csymbr 2637 apply (simp add: X64_H.checkValidIPCBuffer_def cap_get_tag_isCap) 2638 apply (wpc; wrong_cap_throwError_ccorres) 2639 apply clarsimp 2640 done 2641 2642lemma slotCapLongRunningDelete_ccorres: 2643 "ccorres ((=) \<circ> from_bool) ret__unsigned_long_' invs' 2644 (UNIV \<inter> {s. slot_' s = cte_Ptr slot}) [] 2645 (slotCapLongRunningDelete slot) (Call slotCapLongRunningDelete_'proc)" 2646 apply (cinit lift: slot_') 2647 apply (simp add: case_Null_If del: Collect_const) 2648 apply (rule ccorres_pre_getCTE) 2649 apply (rule ccorres_move_c_guard_cte) 2650 apply (rule_tac P="cte_wp_at' ((=) rv) slot" 2651 in ccorres_cross_over_guard) 2652 apply (rule ccorres_symb_exec_r) 2653 apply (rule ccorres_if_lhs) 2654 apply (rule ccorres_cond_true_seq) 2655 apply (rule ccorres_split_throws, rule ccorres_return_C, simp+) 2656 apply vcg 2657 apply (rule ccorres_cond_false_seq) 2658 apply (rule ccorres_rhs_assoc)+ 2659 apply (rule_tac xf'=ret__unsigned_long_' in ccorres_split_nothrow_novcg) 2660 apply (ctac add: isFinalCapability_ccorres[where slot=slot]) 2661 apply (rule Seq_weak_ceqv) 2662 apply (rule Cond_ceqv [OF _ ceqv_refl ceqv_refl]) 2663 apply simp 2664 apply (rule impI, rule sym, rule mem_simps) 2665 apply (clarsimp simp del: Collect_const) 2666 apply (rule ccorres_Cond_rhs_Seq) 2667 apply (rule ccorres_split_throws, rule ccorres_return_C, simp+) 2668 apply vcg 2669 apply (simp del: Collect_const) 2670 apply (rule ccorres_move_c_guard_cte) 2671 apply (rule_tac P="cte_wp_at' ((=) rv) slot" 2672 in ccorres_from_vcg_throws[where P'=UNIV]) 2673 apply (rule allI, rule conseqPre, vcg) 2674 apply (clarsimp simp: cte_wp_at_ctes_of return_def) 2675 apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) 2676 apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap 2677 from_bool_0 2678 dest!: ccte_relation_ccap_relation) 2679 apply (simp add: from_bool_def false_def true_def 2680 split: bool.split) 2681 apply (auto simp add: longRunningDelete_def isCap_simps 2682 split: capability.split)[1] 2683 apply simp 2684 apply (wp hoare_drop_imps isFinalCapability_inv) 2685 apply (clarsimp simp: Collect_const_mem guard_is_UNIV_def) 2686 apply (rename_tac rv') 2687 apply (case_tac rv'; clarsimp simp: false_def true_def) 2688 apply vcg 2689 apply (rule conseqPre, vcg, clarsimp) 2690 apply (clarsimp simp: cte_wp_at_ctes_of) 2691 apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) 2692 apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap 2693 from_bool_def false_def map_comp_Some_iff 2694 dest!: ccte_relation_ccap_relation) 2695 done 2696 2697(* FIXME: move *) 2698lemma empty_fail_slotCapLongRunningDelete: 2699 "empty_fail (slotCapLongRunningDelete slot)" 2700 by (auto simp: slotCapLongRunningDelete_def Let_def 2701 case_Null_If isFinalCapability_def 2702 split: if_split 2703 intro!: empty_fail_bind) 2704 2705definition 2706 isValidVTableRoot_C :: "cap_C \<Rightarrow> bool" 2707where 2708 "isValidVTableRoot_C cap \<equiv> cap_get_tag cap = scast cap_pml4_cap 2709 \<and> to_bool (capPML4IsMapped_CL (cap_pml4_cap_lift cap))" 2710 2711lemma isValidVTableRoot_spec: 2712 "\<forall>s. \<Gamma> \<turnstile> {s} Call isValidVTableRoot_'proc 2713 {s'. ret__unsigned_long_' s' = from_bool (isValidVTableRoot_C (cap_' s))}" 2714 apply vcg 2715 apply (clarsimp simp: isValidVTableRoot_C_def if_1_0_0 from_bool_0) 2716 apply (simp add: from_bool_def to_bool_def false_def split: if_split) 2717 done 2718 2719lemma isValidVTableRoot_conv: 2720 "\<lbrakk> ccap_relation cap cap' \<rbrakk> 2721 \<Longrightarrow> isValidVTableRoot_C cap' = isValidVTableRoot cap" 2722 apply (clarsimp simp: isValidVTableRoot_C_def 2723 if_1_0_0 from_bool_0 isValidVTableRoot_def 2724 X64_H.isValidVTableRoot_def) 2725 apply (case_tac "isArchCap_tag (cap_get_tag cap')") 2726 apply (clarsimp simp: cap_get_tag_isCap cap_get_tag_isCap_ArchObject) 2727 apply (case_tac "cap_get_tag cap' = scast cap_pml4_cap") 2728 apply (clarsimp split: arch_capability.split simp: isCap_simps) 2729 apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 2730 cap_pml4_cap_lift cap_to_H_def 2731 from_bool_def) 2732 apply (clarsimp simp: to_bool_def split: if_split) 2733 apply (clarsimp simp: cap_get_tag_isCap cap_get_tag_isCap_ArchObject) 2734 apply (simp split: arch_capability.split_asm add: isCap_simps) 2735 apply (case_tac "cap_get_tag cap' = scast cap_pml4_cap") 2736 apply (clarsimp simp: cap_pml4_cap_def isArchCap_tag_def2) 2737 apply (clarsimp simp: cap_get_tag_isCap split: capability.split_asm) 2738 done 2739 2740lemma updateCapData_spec: 2741 "\<forall>cap preserve newData. \<Gamma>\<turnstile> \<lbrace>ccap_relation cap \<acute>cap \<and> preserve = to_bool \<acute>preserve \<and> newData = \<acute>newData\<rbrace> 2742 Call updateCapData_'proc 2743 \<lbrace>ccap_relation (RetypeDecls_H.updateCapData preserve newData cap) \<acute>ret__struct_cap_C\<rbrace>" 2744 by (simp add: updateCapData_spec) 2745 2746lemma if_n_updateCapData_valid_strg: 2747 "s \<turnstile>' cap \<longrightarrow> s \<turnstile>' (if P then cap else updateCapData prs v cap)" 2748 by (simp add: valid_updateCapDataI split: if_split) 2749 2750lemma length_excaps_map: 2751 "length (excaps_map xcs) = length xcs" 2752 by (simp add: excaps_map_def) 2753 2754(* FIXME: move *) 2755lemma from_bool_all_helper: 2756 "(\<forall>bool. from_bool bool = val \<longrightarrow> P bool) 2757 = ((\<exists>bool. from_bool bool = val) \<longrightarrow> P (val \<noteq> 0))" 2758 by (auto simp: from_bool_0) 2759 2760lemma getSyscallArg_ccorres_foo': 2761 "ccorres (\<lambda>a rv. rv = ucast (args ! n)) (\<lambda>x. ucast (ret__unsigned_long_' x)) 2762 (sysargs_rel args buffer and sysargs_rel_n args buffer n) 2763 (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) [] 2764 (return ()) (Call getSyscallArg_'proc)" 2765 apply (insert getSyscallArg_ccorres_foo 2766 [where args=args and n=n and buffer=buffer]) 2767 apply (clarsimp simp: ccorres_underlying_def) 2768 apply (erule (1) my_BallE) 2769 apply clarsimp 2770 apply (erule allE, erule allE, erule (1) impE) 2771 apply (clarsimp simp: return_def unif_rrel_def split: xstate.splits) 2772 done 2773 2774lemma scast_mask_8: 2775 "scast (mask 8 :: sword32) = (mask 8 :: word32)" 2776 by (clarsimp simp: mask_def) 2777 2778lemma tcb_at_capTCBPtr_CL: 2779 "ccap_relation cp cap \<Longrightarrow> valid_cap' cp s 2780 \<Longrightarrow> isThreadCap cp 2781 \<Longrightarrow> tcb_at' (cap_thread_cap_CL.capTCBPtr_CL 2782 (cap_thread_cap_lift cap) && ~~mask tcbBlockSizeBits) s" 2783 apply (clarsimp simp: cap_get_tag_isCap[symmetric] 2784 valid_cap_simps' 2785 dest!: cap_get_tag_to_H) 2786 apply (frule ctcb_ptr_to_tcb_ptr_mask[OF tcb_aligned'], simp) 2787 done 2788 2789lemma checkPrio_ccorres: 2790 "ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2791 (tcb_at' auth) 2792 (UNIV \<inter> {s. prio_' s = prio} \<inter> {s. auth_' s = tcb_ptr_to_ctcb_ptr auth}) [] 2793 (checkPrio prio auth) 2794 (Call checkPrio_'proc)" 2795 apply (cinit lift: prio_' auth_') 2796 apply (clarsimp simp: liftE_bindE) 2797 apply (rule ccorres_split_nothrow_novcg[where r'="\<lambda>rv rv'. rv' = ucast rv" and xf'=mcp_']) 2798 apply (rule threadGet_vcg_corres) 2799 apply (rule allI, rule conseqPre, vcg) 2800 apply (clarsimp simp: rf_sr_ksCurThread obj_at'_def projectKOs 2801 typ_heap_simps' ctcb_relation_def) 2802 apply ceqv 2803 apply (simp add: whenE_def del: Collect_const split: if_split) 2804 apply (rule conjI; clarsimp) 2805 apply (rule ccorres_from_vcg_split_throws) 2806 apply vcg 2807 apply (rule conseqPre, vcg) 2808 apply (clarsimp simp: throwError_def syscall_error_rel_def syscall_error_to_H_cases 2809 exception_defs Collect_const_mem rf_sr_ksCurThread return_def 2810 seL4_MinPrio_def minPriority_def) 2811 apply clarsimp 2812 apply (rule ccorres_return_CE) 2813 apply clarsimp+ 2814 apply wp 2815 apply (simp add: guard_is_UNIV_def)+ 2816 done 2817 2818lemma mcpriority_tcb_at'_prio_bounded': 2819 assumes "mcpriority_tcb_at' (\<lambda>mcp. prio \<le> ucast mcp) t s" 2820 "priorityBits \<le> len_of TYPE('a)" 2821 shows "(prio::'a::len word) \<le> ucast (max_word :: priority)" 2822 using assms 2823 by (clarsimp simp: pred_tcb_at'_def obj_at'_def priorityBits_def ucast_le_ucast 2824 elim!: order.trans) 2825 2826lemmas mcpriority_tcb_at'_prio_bounded 2827 = mcpriority_tcb_at'_prio_bounded'[simplified priorityBits_def] 2828 2829lemma decodeTCBConfigure_ccorres: 2830 notes tl_drop_1[simp] scast_mask_8 [simp] 2831 shows 2832 "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow> 2833 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2834 (invs' and sch_act_simple 2835 and (\<lambda>s. ksCurThread s = thread) and ct_active' 2836 and (excaps_in_mem extraCaps o ctes_of) 2837 and valid_cap' cp and cte_at' slot and K (isThreadCap cp) 2838 and ex_nonz_cap_to' (capTCBPtr cp) and tcb_at' (capTCBPtr cp) 2839 and (\<lambda>s. \<forall>v \<in> set extraCaps. 2840 s \<turnstile>' fst v \<and> cte_at' (snd v) s) 2841 and (\<lambda>s. \<forall>v \<in> set extraCaps. 2842 ex_cte_cap_wp_to' isCNodeCap (snd v) s) 2843 and sysargs_rel args buffer) 2844 (UNIV 2845 \<inter> {s. ccap_relation cp (cap_' s)} 2846 \<inter> {s. unat (length___unsigned_long_' s) = length args} 2847 \<inter> {s. slot_' s = cte_Ptr slot} 2848 \<inter> {s. rootCaps_' s = extraCaps'} 2849 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 2850 (decodeTCBConfigure args cp slot extraCaps 2851 >>= invocationCatch thread isBlocking isCall InvokeTCB) 2852 (Call decodeTCBConfigure_'proc)" 2853 apply (cinit' lift: cap_' length___unsigned_long_' slot_' rootCaps_' buffer_' simp: decodeTCBConfigure_def) 2854 apply csymbr 2855 apply (clarsimp cong: StateSpace.state.fold_congs globals.fold_congs 2856 simp del: Collect_const 2857 simp add: interpret_excaps_test_null2 excaps_map_Nil) 2858 apply (rule ccorres_Cond_rhs_Seq) 2859 apply (rule ccorres_cond_true_seq | simp)+ 2860 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2861 apply vcg 2862 apply (rule conseqPre, vcg) 2863 apply (clarsimp simp: if_1_0_0 word_less_nat_alt) 2864 apply (clarsimp split: list.split 2865 simp: throwError_def invocationCatch_def fst_return 2866 intr_and_se_rel_def 2867 Collect_const_mem syscall_error_rel_def 2868 exception_defs syscall_error_to_H_cases) 2869 apply csymbr 2870 apply (rule ccorres_Cond_rhs_Seq) 2871 apply (rule ccorres_cond_true_seq | simp)+ 2872 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2873 apply vcg 2874 apply (rule conseqPre, vcg) 2875 apply (clarsimp simp: if_1_0_0 word_less_nat_alt) 2876 apply (clarsimp split: list.split 2877 simp: throwError_def invocationCatch_def fst_return 2878 intr_and_se_rel_def 2879 Collect_const_mem syscall_error_rel_def 2880 exception_defs syscall_error_to_H_cases) 2881 apply csymbr 2882 apply (rule ccorres_Cond_rhs_Seq) 2883 apply (rule ccorres_cond_true_seq | simp)+ 2884 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2885 apply vcg 2886 apply (rule conseqPre, vcg) 2887 apply (clarsimp simp: if_1_0_0 word_less_nat_alt) 2888 apply (clarsimp split: list.split 2889 simp: throwError_def invocationCatch_def fst_return 2890 intr_and_se_rel_def excaps_map_def 2891 Collect_const_mem syscall_error_rel_def 2892 exception_defs syscall_error_to_H_cases) 2893 apply csymbr 2894 apply (rule ccorres_Cond_rhs_Seq) 2895 apply (rule ccorres_cond_true_seq | simp)+ 2896 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 2897 apply vcg 2898 apply (rule conseqPre, vcg) 2899 apply (clarsimp simp: if_1_0_0 word_less_nat_alt) 2900 apply (clarsimp split: list.split 2901 simp: throwError_def invocationCatch_def fst_return 2902 intr_and_se_rel_def excaps_map_def 2903 Collect_const_mem syscall_error_rel_def 2904 exception_defs syscall_error_to_H_cases) 2905 apply (simp add: if_1_0_0 word_less_nat_alt linorder_not_less 2906 del: Collect_const) 2907 apply (rename_tac length' cap') 2908 apply (subgoal_tac "length extraCaps \<ge> 3") 2909 prefer 2 2910 apply (clarsimp simp: idButNot_def interpret_excaps_test_null 2911 excaps_map_def neq_Nil_conv) 2912 apply (thin_tac "P \<longrightarrow> index exc n \<noteq> NULL" for P exc n)+ 2913 apply (rule_tac P="\<lambda>a. ccorres rvr xf P P' hs a c" for rvr xf P P' hs c in ssubst, 2914 rule bind_cong [OF _ refl], rule list_case_helper, clarsimp)+ 2915 apply (simp add: hd_drop_conv_nth2 del: Collect_const) 2916 apply (rule ccorres_add_return, 2917 ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer]) 2918 apply (rule ccorres_add_return, 2919 ctac add: getSyscallArg_ccorres_foo'[where args=args and n=1 and buffer=buffer]) 2920 apply (rule ccorres_add_return, 2921 ctac add: getSyscallArg_ccorres_foo[where args=args and n=2 and buffer=buffer]) 2922 apply (rule ccorres_add_return, 2923 ctac add: getSyscallArg_ccorres_foo[where args=args and n=3 and buffer=buffer]) 2924 apply csymbr 2925 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0]) 2926 apply (rule ccorres_move_c_guard_cte) 2927 apply ctac 2928 apply (rule ccorres_assert2) 2929 apply csymbr 2930 apply (rule ccorres_move_c_guard_cte) 2931 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=1]) 2932 apply ctac 2933 apply (rule ccorres_assert2) 2934 apply csymbr 2935 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=2]) 2936 apply (rule ccorres_move_c_guard_cte) 2937 apply ctac 2938 apply (rule ccorres_assert2) 2939 apply (simp add: decodeSetIPCBuffer_def split_def 2940 bindE_assoc invocationCatch_use_injection_handler 2941 injection_bindE[OF refl refl] injection_handler_returnOk 2942 injection_handler_If 2943 del: Collect_const cong: if_cong) 2944 apply (rule_tac xf'="\<lambda>s. (bufferCap_' s, bufferSlot_' s)" and 2945 r'="\<lambda>v (cp', sl'). case v of None \<Rightarrow> args ! 3 = 0 \<and> sl' = cte_Ptr 0 2946 | Some (cp, sl) \<Rightarrow> ccap_relation cp cp' 2947 \<and> args ! 3 \<noteq> 0 2948 \<and> sl' = cte_Ptr sl" 2949 in ccorres_splitE) 2950 apply (rule ccorres_cond2[where R=\<top>]) 2951 apply (clarsimp simp add: Collect_const_mem numeral_eqs) 2952 apply (rule_tac P="\<lambda>s. args ! 3 = 0" in ccorres_from_vcg[where P'=UNIV]) 2953 apply (rule allI, rule conseqPre, vcg) 2954 apply (clarsimp simp: returnOk_def return_def) 2955 apply (rule ccorres_rhs_assoc)+ 2956 apply (rule ccorres_split_nothrowE) 2957 apply (simp add: numeral_eqs) 2958 apply (ctac add: ccorres_injection_handler_csum1[OF deriveCap_ccorres]) 2959 apply ceqv 2960 apply simp 2961 apply (clarsimp simp: numeral_eqs) 2962 apply csymbr 2963 apply (rule ccorres_split_nothrowE) 2964 apply (ctac add: ccorres_injection_handler_csum1[OF checkValidIPCBuffer_ccorres]) 2965 apply ceqv 2966 apply (match premises in "ccap_relation _ (deriveCap_ret_C.cap_C ccap)" for ccap 2967 \<Rightarrow> \<open>rule ccorres_from_vcg 2968 [where P'="{s. bufferCap_' s = (deriveCap_ret_C.cap_C ccap) 2969 \<and> bufferSlot_' s = cte_Ptr (snd (extraCaps ! 2))}" 2970 and P="\<lambda>s. args ! 3 \<noteq> 0"]\<close>) 2971 apply (rule allI, rule conseqPre, vcg) 2972 apply (clarsimp simp: returnOk_def return_def numeral_eqs) 2973 apply (rule_tac P'="{s. err' = errstate s}" 2974 in ccorres_from_vcg_throws[where P=\<top>]) 2975 apply (rule allI, rule conseqPre, vcg) 2976 apply (clarsimp simp: throwError_def return_def 2977 syscall_error_rel_def 2978 intr_and_se_rel_def) 2979 apply wp 2980 apply simp 2981 apply (vcg exspec=checkValidIPCBuffer_modifies) 2982 apply simp 2983 apply (rule_tac P'="{s. err' = errstate s}" 2984 in ccorres_from_vcg_split_throws[where P=\<top>]) 2985 apply vcg 2986 apply (rule conseqPre, vcg) 2987 apply (clarsimp simp: throwError_def return_def 2988 intr_and_se_rel_def syscall_error_rel_def) 2989 apply simp 2990 apply (wp injection_wp_E [OF refl]) 2991 apply (simp add: all_ex_eq_helper Collect_const_mem numeral_eqs) 2992 apply (vcg exspec=deriveCap_modifies) 2993 apply (rule ceqv_tuple2, ceqv, ceqv) 2994 apply (rename_tac rv'dc) 2995 apply (rule_tac P="P (fst rv'dc) (snd rv'dc)" 2996 and P'="P' (fst rv'dc) (snd rv'dc)" 2997 for P P' in ccorres_inst) 2998 apply (clarsimp simp: tcb_cnode_index_defs 2999 [THEN ptr_add_assertion_positive 3000 [OF ptr_add_assertion_positive_helper]] 3001 simp del: Collect_const) 3002 apply csymbr 3003 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq)+ 3004 apply (simp add: decodeSetSpace_def injection_bindE[OF refl] split_def 3005 del: Collect_const) 3006 apply (simp add: injection_liftE[OF refl] bindE_assoc 3007 liftM_def getThreadCSpaceRoot 3008 getThreadVSpaceRoot del: Collect_const) 3009 apply (simp add: liftE_bindE del: Collect_const) 3010 apply (rule ccorres_rhs_assoc)+ 3011 apply (ctac add: slotCapLongRunningDelete_ccorres) 3012 apply (rule ccorres_move_array_assertion_tcb_ctes) 3013 apply (simp del: Collect_const) 3014 apply csymbr 3015 apply (clarsimp simp add: if_1_0_0 from_bool_0 3016 simp del: Collect_const) 3017 apply (rule ccorres_Cond_rhs_Seq) 3018 apply (rule ccorres_symb_exec_l3 3019 [OF _ _ _ empty_fail_slotCapLongRunningDelete]) 3020 apply (simp add: unlessE_def injection_handler_throwError 3021 cong: StateSpace.state.fold_congs globals.fold_congs) 3022 apply (rule ccorres_cond_true_seq) 3023 apply (rule syscall_error_throwError_ccorres_n) 3024 apply (simp add: syscall_error_to_H_cases) 3025 apply wp+ 3026 apply (rule ccorres_rhs_assoc)+ 3027 apply csymbr 3028 apply (simp del: Collect_const) 3029 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq 3030 ccorres_rhs_assoc)+ 3031 apply (ctac add: slotCapLongRunningDelete_ccorres) 3032 apply (rule ccorres_move_array_assertion_tcb_ctes) 3033 apply (simp del: Collect_const) 3034 apply csymbr 3035 apply (clarsimp simp add: if_1_0_0 from_bool_0 3036 simp del: Collect_const) 3037 apply (rule ccorres_Cond_rhs_Seq) 3038 apply (simp add: unlessE_def injection_handler_throwError 3039 cong: StateSpace.state.fold_congs globals.fold_congs) 3040 apply (rule syscall_error_throwError_ccorres_n) 3041 apply (simp add: syscall_error_to_H_cases) 3042 apply (simp add: unlessE_def injection_handler_returnOk 3043 del: Collect_const) 3044 apply (rule ccorres_add_return, 3045 rule_tac r'="\<lambda>rv rv'. ccap_relation 3046 (if args ! 1 = 0 3047 then fst (hd extraCaps) 3048 else updateCapData False (args ! 1) (fst (hd extraCaps))) rv'" 3049 and xf'="cRootCap_'" 3050 in ccorres_split_nothrow) 3051 apply (rule_tac P'="{s. cRootCap = cRootCap_' s}" 3052 in ccorres_from_vcg[where P=\<top>]) 3053 apply (rule allI, rule conseqPre, vcg) 3054 apply (subgoal_tac "extraCaps \<noteq> []") 3055 apply (clarsimp simp: returnOk_def return_def hd_conv_nth false_def) 3056 apply fastforce 3057 apply clarsimp 3058 apply ceqv 3059 apply (ctac add: ccorres_injection_handler_csum1 3060 [OF deriveCap_ccorres]) 3061 apply (simp add: Collect_False del: Collect_const) 3062 apply (csymbr, csymbr) 3063 apply (simp add: cap_get_tag_isCap cnode_cap_case_if 3064 del: Collect_const) 3065 apply (rule ccorres_Cond_rhs_Seq) 3066 apply (simp add: injection_handler_throwError 3067 cong: StateSpace.state.fold_congs globals.fold_congs) 3068 apply (rule syscall_error_throwError_ccorres_n) 3069 apply (simp add: syscall_error_to_H_cases) 3070 apply (simp add: injection_handler_returnOk del: Collect_const) 3071 apply (rule ccorres_add_return, 3072 rule_tac r'="\<lambda>rv rv'. ccap_relation 3073 (if args ! 2 = 0 3074 then fst (extraCaps ! Suc 0) 3075 else updateCapData False (args ! 2) (fst (extraCaps ! Suc 0))) rv'" 3076 and xf'="vRootCap_'" 3077 in ccorres_split_nothrow) 3078 apply (rule_tac P'="{s. vRootCap = vRootCap_' s}" 3079 in ccorres_from_vcg[where P=\<top>]) 3080 apply (rule allI, rule conseqPre, vcg) 3081 apply (clarsimp simp: returnOk_def return_def 3082 hd_drop_conv_nth2 false_def) 3083 apply fastforce 3084 apply ceqv 3085 apply (ctac add: ccorres_injection_handler_csum1 3086 [OF deriveCap_ccorres]) 3087 apply (simp add: Collect_False del: Collect_const) 3088 apply csymbr 3089 apply csymbr 3090 apply (simp add: from_bool_0 isValidVTableRoot_conv del: Collect_const) 3091 apply (rule ccorres_Cond_rhs_Seq) 3092 apply (simp add: injection_handler_throwError 3093 cong: StateSpace.state.fold_congs globals.fold_congs) 3094 apply (rule syscall_error_throwError_ccorres_n) 3095 apply (simp add: syscall_error_to_H_cases) 3096 apply (simp add: injection_handler_returnOk ccorres_invocationCatch_Inr 3097 performInvocation_def) 3098 apply (ctac add: setThreadState_ccorres) 3099 apply csymbr 3100 apply (ctac(no_vcg) add: invokeTCB_ThreadControl_ccorres) 3101 apply (simp, rule ccorres_alternative2) 3102 apply (rule ccorres_return_CE, simp+) 3103 apply (rule ccorres_return_C_errorE, simp+)[1] 3104 apply wp 3105 apply (simp add: o_def) 3106 apply (wp sts_invs_minor' hoare_case_option_wp) 3107 apply (simp add: Collect_const_mem cintr_def intr_and_se_rel_def 3108 exception_defs 3109 cong: option.case_cong) 3110 apply (vcg exspec=setThreadState_modifies) 3111 apply simp 3112 apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+) 3113 apply vcg 3114 apply simp 3115 apply (wp injection_wp_E[OF refl] hoare_drop_imps) 3116 apply (vcg exspec=deriveCap_modifies) 3117 apply (simp add: pred_conj_def cong: if_cong) 3118 apply wp 3119 apply (simp add: Collect_const_mem) 3120 apply (vcg) 3121 apply simp 3122 apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+) 3123 apply vcg 3124 apply (simp cong: if_cong) 3125 apply (wp injection_wp_E[OF refl] hoare_drop_imps) 3126 apply (simp add: Collect_const_mem intr_and_se_rel_def 3127 syscall_error_rel_def exception_defs 3128 cong: option.case_cong sum.case_cong) 3129 apply (simp add: all_ex_eq_helper numeral_eqs) 3130 apply (vcg exspec=deriveCap_modifies) 3131 apply (simp cong: if_cong) 3132 apply wp 3133 apply (simp add: Collect_const_mem del: Collect_const) 3134 apply vcg 3135 apply (simp cong: if_cong) 3136 apply (wp | wp_once hoare_drop_imps)+ 3137 apply (simp add: Collect_const_mem all_ex_eq_helper 3138 cong: option.case_cong) 3139 apply (vcg exspec=slotCapLongRunningDelete_modifies) 3140 apply (simp cong: if_cong) 3141 apply (wp | wp_once hoare_drop_imps)+ 3142 apply (simp add: Collect_const_mem) 3143 apply (vcg exspec=slotCapLongRunningDelete_modifies) 3144 apply (simp add: pred_conj_def cong: if_cong) 3145 apply (wp injection_wp_E[OF refl] checkValidIPCBuffer_ArchObject_wp) 3146 apply simp 3147 apply (wp | wp_once hoare_drop_imps)+ 3148 apply (simp add: Collect_const_mem all_ex_eq_helper) 3149 apply (rule_tac P="{s. cRootCap_' s = cRootCap \<and> vRootCap_' s = vRootCap 3150 \<and> bufferAddr_' s = args ! 3 3151 \<and> ccap_relation cp cap' \<and> isThreadCap cp 3152 \<and> is_aligned (capTCBPtr cp) tcbBlockSizeBits 3153 \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread}" 3154 in conseqPre) 3155 apply (simp add: cong: option.case_cong) 3156 apply (vcg exspec=deriveCap_modifies exspec=checkValidIPCBuffer_modifies) 3157 apply (clarsimp simp: excaps_map_def Collect_const_mem ccHoarePost_def 3158 numeral_eqs 3159 cong: option.case_cong) 3160 apply (frule interpret_excaps_eq[rule_format, where n=0], clarsimp) 3161 apply (frule interpret_excaps_eq[rule_format, where n=1], clarsimp) 3162 apply (frule interpret_excaps_eq[rule_format, where n=2], clarsimp) 3163 apply (clarsimp simp: mask_def[where n=4] ccap_rights_relation_def 3164 rightsFromWord_wordFromRights capTCBPtr_eq 3165 ptr_val_tcb_ptr_mask2[unfolded mask_def objBits_defs, simplified] 3166 tcb_cnode_index_defs size_of_def 3167 option_to_0_def rf_sr_ksCurThread 3168 StrictC'_thread_state_defs mask_eq_iff_w2p word_size 3169 from_bool_all_helper all_ex_eq_helper 3170 ucast_ucast_mask objBits_defs) 3171 apply (subgoal_tac "args \<noteq> [] \<and> extraCaps \<noteq> []") 3172 apply (simp add: word_sle_def cap_get_tag_isCap numeral_eqs 3173 hd_conv_nth hd_drop_conv_nth2 3174 word_FF_is_mask split_def 3175 thread_control_update_priority_def 3176 thread_control_update_mcp_def 3177 thread_control_update_space_def 3178 thread_control_update_ipc_buffer_def) 3179 apply (auto split: option.split elim!: inl_inrE)[1] 3180 apply (fastforce+)[2] 3181 apply clarsimp 3182 apply (strengthen if_n_updateCapData_valid_strg) 3183 apply (wp | wp_once hoare_drop_imps)+ 3184 apply (clarsimp simp: Collect_const_mem all_ex_eq_helper 3185 cong: option.case_cong) 3186 apply vcg 3187 apply simp 3188 apply (wp | wp_once hoare_drop_imps)+ 3189 apply (simp add: Collect_const_mem all_ex_eq_helper) 3190 apply vcg 3191 apply simp 3192 apply (wp | wp_once hoare_drop_imps)+ 3193 apply (wpsimp | vcg exspec=getSyscallArg_modifies)+ 3194 apply (clarsimp simp: Collect_const_mem all_ex_eq_helper) 3195 apply (rule conjI) 3196 apply (clarsimp simp: idButNot_def interpret_excaps_test_null 3197 excaps_map_def neq_Nil_conv) 3198 apply (clarsimp simp: sysargs_rel_to_n word_less_nat_alt) 3199 apply (frule invs_mdb') 3200 apply (frule(2) tcb_at_capTCBPtr_CL) 3201 apply (rule conjI, fastforce) 3202 apply (drule interpret_excaps_eq) 3203 apply (clarsimp simp: cte_wp_at_ctes_of valid_tcb_state'_def numeral_eqs le_ucast_ucast_le 3204 tcb_at_invs' invs_valid_objs' invs_queues invs_sch_act_wf' 3205 ct_in_state'_def pred_tcb_at'_def obj_at'_def tcb_st_refs_of'_def) 3206 apply (erule disjE; simp add: objBits_defs mask_def) 3207 apply (clarsimp simp: idButNot_def interpret_excaps_test_null 3208 excaps_map_def neq_Nil_conv word_sle_def word_sless_def) 3209 apply (frule interpret_excaps_eq[rule_format, where n=0], simp) 3210 apply (frule interpret_excaps_eq[rule_format, where n=1], simp) 3211 apply (frule interpret_excaps_eq[rule_format, where n=2], simp) 3212 apply (clarsimp simp: mask_def[where n=4] ccap_rights_relation_def 3213 rightsFromWord_wordFromRights 3214 capTCBPtr_eq tcb_ptr_to_ctcb_ptr_mask 3215 tcb_cnode_index_defs size_of_def 3216 option_to_0_def rf_sr_ksCurThread 3217 StrictC'_thread_state_defs mask_eq_iff_w2p word_size 3218 from_bool_all_helper) 3219 apply (frule(1) tcb_at_h_t_valid [OF tcb_at_invs']) 3220 apply (clarsimp simp: typ_heap_simps numeral_eqs isCap_simps valid_cap'_def capAligned_def 3221 objBits_simps) 3222 done 3223 3224lemma not_isThreadCap_case: 3225 "\<lbrakk>\<not>isThreadCap cap\<rbrakk> \<Longrightarrow> 3226 (case cap of ThreadCap x \<Rightarrow> f x | _ \<Rightarrow> g) = g" 3227 by (clarsimp simp: isThreadCap_def split: capability.splits) 3228 3229lemma decodeSetMCPriority_ccorres: 3230 "\<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps\<rbrakk> \<Longrightarrow> 3231 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 3232 (invs' and (\<lambda>s. ksCurThread s = thread) 3233 and ct_active' and sch_act_simple 3234 and (excaps_in_mem extraCaps \<circ> ctes_of) 3235 and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s) 3236 and valid_cap' cp and K (isThreadCap cp) 3237 and (\<lambda>s. \<forall>v \<in> set extraCaps. 3238 ex_cte_cap_wp_to' isCNodeCap (snd v) s) 3239 and (\<lambda>s. \<forall>v \<in> set extraCaps. 3240 s \<turnstile>' fst v \<and> cte_at' (snd v) s) 3241 and sysargs_rel args buffer) 3242 (UNIV 3243 \<inter> {s. ccap_relation cp (cap_' s)} 3244 \<inter> {s. unat (length___unsigned_long_' s) = length args} 3245 \<inter> {s. excaps_' s = extraCaps'} 3246 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 3247 (decodeSetMCPriority args cp extraCaps 3248 >>= invocationCatch thread isBlocking isCall InvokeTCB) 3249 (Call decodeSetMCPriority_'proc)" 3250 supply Collect_const[simp del] 3251 supply dc_simp[simp del] 3252 apply (cinit' lift: cap_' length___unsigned_long_' excaps_' buffer_' simp: decodeSetMCPriority_def) 3253 apply (simp cong: StateSpace.state.fold_congs globals.fold_congs) 3254 apply (rule ccorres_rhs_assoc2) 3255 apply (rule_tac xf'=ret__int_' and R'=UNIV and R=\<top> and 3256 val="from_bool (length args = 0 \<or> length extraCaps = 0)" in 3257 ccorres_symb_exec_r_known_rv) 3258 apply vcg 3259 apply (force simp: interpret_excaps_test_null excaps_map_def from_bool_def unat_eq_0 3260 split: bool.splits) 3261 apply ceqv 3262 apply clarsimp 3263 apply wpc 3264 (* Case args = [] *) 3265 apply (rule ccorres_cond_true_seq) 3266 apply (clarsimp simp: throwError_bind invocationCatch_def) 3267 apply (rule ccorres_rhs_assoc) 3268 apply (ccorres_rewrite) 3269 apply (rule syscall_error_throwError_ccorres_n) 3270 apply (simp add: syscall_error_to_H_cases) 3271 (* Case args is Cons *) 3272 apply wpc 3273 (* Sub-case extraCaps = [] *) 3274 apply (rule ccorres_cond_true_seq) 3275 apply (clarsimp simp: throwError_bind invocationCatch_def) 3276 apply (rule ccorres_rhs_assoc) 3277 apply (ccorres_rewrite) 3278 apply (rule syscall_error_throwError_ccorres_n) 3279 apply (simp add: syscall_error_to_H_cases) 3280 (* Main case where args and extraCaps are both Cons *) 3281 apply (rule ccorres_cond_false_seq) 3282 apply (simp add: split_def) 3283 apply (rule ccorres_add_return, 3284 ctac add: getSyscallArg_ccorres_foo'[where args=args and n=0 and buffer=buffer]) 3285 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0]) 3286 apply (rule ccorres_move_c_guard_cte) 3287 apply ctac 3288 apply csymbr 3289 apply (simp add: cap_get_tag_isCap cong: call_ignore_cong) 3290 apply (rule ccorres_assert2) 3291 apply (rule ccorres_Cond_rhs_Seq) 3292 apply (rule ccorres_rhs_assoc) 3293 apply ccorres_rewrite 3294 apply (clarsimp simp: not_isThreadCap_case throwError_bind invocationCatch_def 3295 simp del: id_simps) 3296 apply (rule syscall_error_throwError_ccorres_n) 3297 apply (simp add: syscall_error_to_H_cases) 3298 apply (clarsimp simp: isCap_simps) 3299 apply csymbr 3300 apply csymbr 3301 (* Pre-conditions need to depend on the inner value of the thread cap *) 3302 apply (rule ccorres_inst[where P="Q (capTCBPtr (fst (extraCaps ! 0)))" and 3303 P'="Q' (capTCBPtr (fst (extraCaps ! 0)))" for Q Q']) 3304 apply (clarsimp simp: capTCBPtr_eq isCap_simps invocationCatch_use_injection_handler 3305 injection_bindE[OF refl refl] bindE_assoc injection_handler_returnOk) 3306 apply (ctac add: ccorres_injection_handler_csum1[OF checkPrio_ccorres]) 3307 apply (rule_tac P="hd args \<le> ucast (max_word :: priority)" 3308 in ccorres_cross_over_guard_no_st) 3309 apply (simp add: ccorres_invocationCatch_Inr performInvocation_def) 3310 apply ccorres_rewrite 3311 apply (ctac add: setThreadState_ccorres) 3312 apply (simp add: invocationCatch_def) 3313 apply ccorres_rewrite 3314 apply csymbr 3315 apply csymbr 3316 apply csymbr 3317 apply csymbr 3318 apply (ctac (no_vcg) add: invokeTCB_ThreadControl_ccorres) 3319 (* HACK: delete rules from the simpset to avoid the RVRs getting out of sync *) 3320 apply (clarsimp simp del: intr_and_se_rel_simps comp_apply dc_simp) 3321 apply (rule ccorres_alternative2) 3322 apply (rule ccorres_return_CE; simp) 3323 apply (rule ccorres_return_C_errorE; simp) 3324 apply wp 3325 apply (wpsimp wp: sts_invs_minor') 3326 apply simp 3327 apply (vcg exspec=setThreadState_modifies) 3328 apply simp 3329 apply (rename_tac err_c) 3330 apply (rule_tac P'="{s. err_c = errstate s}" in ccorres_from_vcg_split_throws) 3331 apply vcg 3332 apply (rule conseqPre, vcg) 3333 apply (clarsimp simp: throwError_def return_def intr_and_se_rel_def syscall_error_rel_def) 3334 apply simp 3335 apply (rule injection_handler_wp) 3336 apply (rule checkPrio_wp[simplified validE_R_def]) 3337 apply vcg 3338 apply (wp | simp | wpc | wp_once hoare_drop_imps)+ 3339 apply vcg 3340 apply wp 3341 apply (vcg exspec=getSyscallArg_modifies) 3342 apply (clarsimp simp: EXCEPTION_SYSCALL_ERROR_def EXCEPTION_NONE_def) 3343 apply vcg 3344 apply clarsimp 3345 apply (rule conjI) 3346 apply (clarsimp simp: ct_in_state'_def pred_tcb_at' 3347 valid_cap'_def isCap_simps) 3348 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 3349 apply (clarsimp simp: maxPriority_def numPriorities_def) 3350 apply (fold max_word_def[where 'a=8, simplified]) 3351 apply (rule conjI, clarsimp) 3352 apply (frule mcpriority_tcb_at'_prio_bounded, simp) 3353 apply (auto simp: valid_tcb_state'_def le_ucast_ucast_le 3354 elim!: obj_at'_weakenE pred_tcb'_weakenE 3355 dest!: st_tcb_at_idle_thread')[1] 3356 apply (clarsimp simp: interpret_excaps_eq excaps_map_def) 3357 apply (simp add: StrictC'_thread_state_defs mask_eq_iff_w2p word_size option_to_0_def) 3358 apply (frule rf_sr_ksCurThread) 3359 apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) 3360 apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def) 3361 apply (intro conjI impI allI) 3362 apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id cap_get_tag_isCap_unfolded_H_cap isCap_simps)+ 3363 done 3364 3365lemma decodeSetPriority_ccorres: 3366 "\<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps\<rbrakk> \<Longrightarrow> 3367 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 3368 (invs' and (\<lambda>s. ksCurThread s = thread) 3369 and ct_active' and sch_act_simple 3370 and (excaps_in_mem extraCaps \<circ> ctes_of) 3371 and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s) 3372 and valid_cap' cp and K (isThreadCap cp) 3373 and (\<lambda>s. \<forall>v \<in> set extraCaps. 3374 ex_cte_cap_wp_to' isCNodeCap (snd v) s) 3375 and (\<lambda>s. \<forall>v \<in> set extraCaps. 3376 s \<turnstile>' fst v \<and> cte_at' (snd v) s) 3377 and sysargs_rel args buffer) 3378 (UNIV 3379 \<inter> {s. ccap_relation cp (cap_' s)} 3380 \<inter> {s. unat (length___unsigned_long_' s) = length args} 3381 \<inter> {s. excaps_' s = extraCaps'} 3382 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 3383 (decodeSetPriority args cp extraCaps 3384 >>= invocationCatch thread isBlocking isCall InvokeTCB) 3385 (Call decodeSetPriority_'proc)" 3386 supply Collect_const[simp del] dc_simp[simp del] 3387 apply (cinit' lift: cap_' length___unsigned_long_' excaps_' buffer_' simp: decodeSetPriority_def) 3388 apply (simp cong: StateSpace.state.fold_congs globals.fold_congs) 3389 apply (rule ccorres_rhs_assoc2) 3390 apply (rule_tac xf'=ret__int_' and R'=UNIV and R=\<top> and 3391 val="from_bool (length args = 0 \<or> length extraCaps = 0)" in 3392 ccorres_symb_exec_r_known_rv) 3393 apply vcg 3394 apply (force simp: interpret_excaps_test_null excaps_map_def from_bool_def unat_eq_0 3395 split: bool.splits) 3396 apply ceqv 3397 apply clarsimp 3398 apply wpc 3399 (* Case args = [] *) 3400 apply (rule ccorres_cond_true_seq) 3401 apply (clarsimp simp: throwError_bind invocationCatch_def) 3402 apply (rule ccorres_rhs_assoc) 3403 apply (ccorres_rewrite) 3404 apply (rule syscall_error_throwError_ccorres_n) 3405 apply (simp add: syscall_error_to_H_cases) 3406 (* Case args is Cons *) 3407 apply wpc 3408 (* Sub-case extraCaps = [] *) 3409 apply (rule ccorres_cond_true_seq) 3410 apply (clarsimp simp: throwError_bind invocationCatch_def) 3411 apply (rule ccorres_rhs_assoc) 3412 apply (ccorres_rewrite) 3413 apply (rule syscall_error_throwError_ccorres_n) 3414 apply (simp add: syscall_error_to_H_cases) 3415 (* Main case where args and extraCaps are both Cons *) 3416 apply (rule ccorres_cond_false_seq) 3417 apply (simp add: split_def) 3418 apply (rule ccorres_add_return, 3419 ctac add: getSyscallArg_ccorres_foo'[where args=args and n=0 and buffer=buffer]) 3420 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0]) 3421 apply (rule ccorres_move_c_guard_cte) 3422 apply ctac 3423 apply csymbr 3424 apply (simp add: cap_get_tag_isCap cong: call_ignore_cong) 3425 apply (rule ccorres_assert2) 3426 apply (rule ccorres_Cond_rhs_Seq) 3427 apply (rule ccorres_rhs_assoc) 3428 apply ccorres_rewrite 3429 apply (clarsimp simp: not_isThreadCap_case throwError_bind invocationCatch_def 3430 simp del: id_simps) 3431 apply (rule syscall_error_throwError_ccorres_n) 3432 apply (simp add: syscall_error_to_H_cases) 3433 apply (clarsimp simp: isCap_simps) 3434 apply csymbr 3435 apply csymbr 3436 (* Pre-conditions need to depend on the inner value of the thread cap *) 3437 apply (rule ccorres_inst[where P="Q (capTCBPtr (fst (extraCaps ! 0)))" and 3438 P'="Q' (capTCBPtr (fst (extraCaps ! 0)))" for Q Q']) 3439 apply (clarsimp simp: capTCBPtr_eq isCap_simps invocationCatch_use_injection_handler 3440 injection_bindE[OF refl refl] bindE_assoc injection_handler_returnOk) 3441 apply (ctac add: ccorres_injection_handler_csum1[OF checkPrio_ccorres]) 3442 apply (rule_tac P="hd args \<le> ucast (max_word :: priority)" 3443 in ccorres_cross_over_guard_no_st) 3444 apply (simp add: ccorres_invocationCatch_Inr performInvocation_def) 3445 apply ccorres_rewrite 3446 apply (ctac add: setThreadState_ccorres) 3447 apply (simp add: invocationCatch_def) 3448 apply ccorres_rewrite 3449 apply csymbr 3450 apply csymbr 3451 apply csymbr 3452 apply csymbr 3453 apply (ctac (no_vcg) add: invokeTCB_ThreadControl_ccorres) 3454 (* HACK: delete rules from the simpset to avoid the RVRs getting out of sync *) 3455 apply (clarsimp simp del: intr_and_se_rel_simps comp_apply dc_simp) 3456 apply (rule ccorres_alternative2) 3457 apply (rule ccorres_return_CE; simp) 3458 apply (rule ccorres_return_C_errorE; simp) 3459 apply wp 3460 apply (wpsimp wp: sts_invs_minor') 3461 apply simp 3462 apply (vcg exspec=setThreadState_modifies) 3463 apply simp 3464 apply (rename_tac err_c) 3465 apply (rule_tac P'="{s. err_c = errstate s}" in ccorres_from_vcg_split_throws) 3466 apply vcg 3467 apply (rule conseqPre, vcg) 3468 apply (clarsimp simp: throwError_def return_def intr_and_se_rel_def syscall_error_rel_def) 3469 apply simp 3470 apply (rule injection_handler_wp) 3471 apply (rule checkPrio_wp[simplified validE_R_def]) 3472 apply vcg 3473 apply (wp | simp | wpc | wp_once hoare_drop_imps)+ 3474 apply vcg 3475 apply wp 3476 apply (vcg exspec=getSyscallArg_modifies) 3477 apply (clarsimp simp: EXCEPTION_SYSCALL_ERROR_def EXCEPTION_NONE_def) 3478 apply vcg 3479 apply clarsimp 3480 apply (rule conjI) 3481 apply (clarsimp simp: ct_in_state'_def pred_tcb_at' 3482 valid_cap'_def isCap_simps) 3483 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 3484 apply (clarsimp simp: maxPriority_def numPriorities_def) 3485 apply (fold max_word_def[where 'a=8, simplified]) 3486 apply (rule conjI, clarsimp) 3487 apply (frule mcpriority_tcb_at'_prio_bounded, simp) 3488 apply (auto simp: valid_tcb_state'_def le_ucast_ucast_le 3489 elim!: obj_at'_weakenE pred_tcb'_weakenE 3490 dest!: st_tcb_at_idle_thread')[1] 3491 apply (clarsimp simp: interpret_excaps_eq excaps_map_def) 3492 apply (simp add: StrictC'_thread_state_defs mask_eq_iff_w2p word_size option_to_0_def) 3493 apply (frule rf_sr_ksCurThread) 3494 apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) 3495 apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def) 3496 apply (intro conjI impI allI) 3497 apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id cap_get_tag_isCap_unfolded_H_cap isCap_simps)+ 3498 done 3499 3500lemma ucast_le_8_64_equiv: 3501 "x \<le> UCAST (8 \<rightarrow> 64) max_word \<Longrightarrow> 3502 (UCAST (64 \<rightarrow> 8) x \<le> y) = (x \<le> UCAST (8 \<rightarrow> 64) y)" 3503 apply (rule iffI) 3504 apply (word_bitwise; simp) 3505 apply (simp add: le_ucast_ucast_le) 3506 done 3507 3508lemma mcpriority_tcb_at'_le_ucast: 3509 "pred_tcb_at' itcbMCP (\<lambda>mcp. x \<le> UCAST(8 \<rightarrow> 64) mcp) v s \<Longrightarrow> 3510 pred_tcb_at' itcbMCP (\<lambda>mcp. UCAST(64 \<rightarrow> 8) x \<le> mcp) v s" 3511 apply (clarsimp simp: ucast_le_8_64_equiv mcpriority_tcb_at'_prio_bounded) 3512 done 3513 3514lemma decodeSetSchedParams_ccorres: 3515 "\<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps\<rbrakk> \<Longrightarrow> 3516 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 3517 (invs' and (\<lambda>s. ksCurThread s = thread) 3518 and ct_active' and sch_act_simple 3519 and (excaps_in_mem extraCaps \<circ> ctes_of) 3520 and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s) 3521 and valid_cap' cp and K (isThreadCap cp) 3522 and (\<lambda>s. \<forall>v \<in> set extraCaps. 3523 ex_cte_cap_wp_to' isCNodeCap (snd v) s) 3524 and (\<lambda>s. \<forall>v \<in> set extraCaps. 3525 s \<turnstile>' fst v \<and> cte_at' (snd v) s) 3526 and sysargs_rel args buffer) 3527 (UNIV 3528 \<inter> {s. ccap_relation cp (cap_' s)} 3529 \<inter> {s. unat (length___unsigned_long_' s) = length args} 3530 \<inter> {s. excaps_' s = extraCaps'} 3531 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 3532 (decodeSetSchedParams args cp extraCaps 3533 >>= invocationCatch thread isBlocking isCall InvokeTCB) 3534 (Call decodeSetSchedParams_'proc)" 3535 supply Collect_const[simp del] dc_simp[simp del] 3536 apply (cinit' lift: cap_' length___unsigned_long_' excaps_' buffer_' simp: decodeSetSchedParams_def) 3537 apply (simp cong: StateSpace.state.fold_congs globals.fold_congs) 3538 apply (rule ccorres_rhs_assoc2) 3539 apply (rule_tac xf'=ret__int_' and R'=UNIV and R=\<top> and 3540 val="from_bool (length args < 2 \<or> length extraCaps = 0)" in 3541 ccorres_symb_exec_r_known_rv) 3542 apply vcg 3543 apply (auto simp: interpret_excaps_test_null excaps_map_def from_bool_def unat_eq_0 3544 split: bool.splits)[1] 3545 apply (unat_arith+)[2] 3546 apply ceqv 3547 apply clarsimp 3548(* 3549 apply (wpc) 3550 apply (rule ccorres_cond_true_seq) 3551 apply (clarsimp simp: throwError_bind invocationCatch_def) 3552 apply (rule ccorres_rhs_assoc) 3553 apply (ccorres_rewrite) 3554 apply (fastforce intro: syscall_error_throwError_ccorres_n simp: syscall_error_to_H_cases) 3555 apply (wpc) 3556 apply (rule ccorres_cond_true_seq) 3557 apply (clarsimp simp: throwError_bind invocationCatch_def) 3558 apply (rule ccorres_rhs_assoc) 3559 apply (ccorres_rewrite) 3560 apply (fastforce intro: syscall_error_throwError_ccorres_n simp: syscall_error_to_H_cases) 3561 apply (wpc) 3562 apply (rule ccorres_cond_true_seq) 3563 apply (clarsimp simp: throwError_bind invocationCatch_def) 3564 apply (rule ccorres_rhs_assoc) 3565 apply (ccorres_rewrite) 3566 apply (fastforce intro: syscall_error_throwError_ccorres_n simp: syscall_error_to_H_cases) 3567*) 3568 apply (wpc, 3569 rule ccorres_cond_true_seq, 3570 clarsimp simp: throwError_bind invocationCatch_def, 3571 rule ccorres_rhs_assoc, 3572 ccorres_rewrite, 3573 fastforce intro: syscall_error_throwError_ccorres_n simp: syscall_error_to_H_cases)+ 3574 (* Main case where args and extraCaps are both well-formed *) 3575 apply (rule ccorres_cond_false_seq) 3576 apply (simp add: split_def) 3577 apply (rule ccorres_add_return, 3578 ctac add: getSyscallArg_ccorres_foo'[where args=args and n=0 and buffer=buffer]) 3579 apply (rule ccorres_add_return, 3580 ctac add: getSyscallArg_ccorres_foo'[where args=args and n=1 and buffer=buffer]) 3581 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0]) 3582 apply (rule ccorres_move_c_guard_cte) 3583 apply ctac 3584 apply csymbr 3585 apply (simp add: cap_get_tag_isCap cong: call_ignore_cong) 3586 apply (rule ccorres_assert2) 3587 apply (rule ccorres_Cond_rhs_Seq) 3588 apply (rule ccorres_rhs_assoc) 3589 apply ccorres_rewrite 3590 apply (clarsimp simp: not_isThreadCap_case throwError_bind invocationCatch_def 3591 simp del: id_simps) 3592 apply (rule syscall_error_throwError_ccorres_n) 3593 apply (simp add: syscall_error_to_H_cases) 3594 apply (clarsimp simp: isCap_simps) 3595 apply csymbr 3596 apply csymbr 3597 (* Pre-conditions need to depend on the inner value of the thread cap *) 3598 apply (rule ccorres_inst[where P="Q (capTCBPtr (fst (extraCaps ! 0)))" and 3599 P'="Q' (capTCBPtr (fst (extraCaps ! 0)))" for Q Q']) 3600 apply (clarsimp simp: capTCBPtr_eq isCap_simps invocationCatch_use_injection_handler 3601 injection_bindE[OF refl refl] bindE_assoc injection_handler_returnOk) 3602 apply (ctac add: ccorres_injection_handler_csum1[OF checkPrio_ccorres]) 3603 apply (rule_tac P="args ! 0 \<le> ucast (max_word :: priority)" 3604 in ccorres_cross_over_guard_no_st) 3605 apply (simp add: ccorres_invocationCatch_Inr performInvocation_def) 3606 apply ccorres_rewrite 3607 apply (clarsimp simp: capTCBPtr_eq isCap_simps invocationCatch_use_injection_handler 3608 injection_bindE[OF refl refl] bindE_assoc injection_handler_returnOk) 3609 apply (ctac add: ccorres_injection_handler_csum1[OF checkPrio_ccorres]) 3610 apply (rule_tac P="args ! 1 \<le> ucast (max_word :: priority)" 3611 in ccorres_cross_over_guard_no_st) 3612 apply (simp add: ccorres_invocationCatch_Inr performInvocation_def) 3613 apply ccorres_rewrite 3614 apply (ctac add: setThreadState_ccorres) 3615 apply (simp add: invocationCatch_def) 3616 apply ccorres_rewrite 3617 apply csymbr 3618 apply csymbr 3619 apply csymbr 3620 apply csymbr 3621 apply (ctac (no_vcg) add: invokeTCB_ThreadControl_ccorres) 3622 (* HACK: delete rules from the simpset to avoid the RVRs getting out of sync *) 3623 apply (clarsimp simp del: intr_and_se_rel_simps comp_apply dc_simp) 3624 apply (rule ccorres_alternative2) 3625 apply (rule ccorres_return_CE; simp) 3626 apply (rule ccorres_return_C_errorE; simp) 3627 apply wp 3628 apply (wpsimp wp: sts_invs_minor') 3629 apply simp 3630 apply (vcg exspec=setThreadState_modifies) 3631 apply simp 3632 apply (rename_tac err_c) 3633 apply (rule_tac P'="{s. err_c = errstate s}" in ccorres_from_vcg_split_throws) 3634 apply vcg 3635 apply (rule conseqPre, vcg) 3636 apply (clarsimp simp: throwError_def return_def intr_and_se_rel_def syscall_error_rel_def) 3637 apply simp 3638 apply (rule injection_handler_wp) 3639 apply (rule checkPrio_wp[simplified validE_R_def]) 3640 apply vcg 3641 apply clarsimp 3642 apply ccorres_rewrite 3643 apply (rule ccorres_return_C_errorE; simp) 3644 apply simp 3645 apply (rule injection_handler_wp) 3646 apply (rule checkPrio_wp[simplified validE_R_def]) 3647 apply vcg 3648 apply (wp | simp | wpc | wp_once hoare_drop_imps)+ 3649 apply vcg 3650 apply simp 3651 apply (rule return_wp) 3652 apply (vcg exspec=getSyscallArg_modifies) 3653 apply simp 3654 apply (rule return_wp) 3655 apply simp 3656 apply (vcg exspec=getSyscallArg_modifies) 3657 apply simp 3658 apply (vcg exspec=getSyscallArg_modifies) 3659 apply clarsimp 3660 apply (rule conjI) 3661 apply (clarsimp simp: ct_in_state'_def pred_tcb_at' 3662 valid_cap'_def isCap_simps) 3663 apply (rule conjI; clarsimp simp: sysargs_rel_to_n n_msgRegisters_def) 3664 apply (clarsimp simp: maxPriority_def numPriorities_def) 3665 apply (fold max_word_def[where 'a=8, simplified]) 3666 apply (rule conjI, clarsimp) 3667 apply (insert mcpriority_tcb_at'_prio_bounded[where prio="args ! 0"]) 3668 apply (insert mcpriority_tcb_at'_prio_bounded[where prio="args ! 1"]) 3669 apply (auto simp: valid_tcb_state'_def mcpriority_tcb_at'_le_ucast 3670 elim!: obj_at'_weakenE pred_tcb'_weakenE 3671 dest!: st_tcb_at_idle_thread')[1] 3672 apply (clarsimp simp: interpret_excaps_eq excaps_map_def) 3673 apply (simp add: StrictC'_thread_state_defs mask_eq_iff_w2p word_size option_to_0_def) 3674 apply (frule rf_sr_ksCurThread) 3675 apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) 3676 apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def) 3677 apply (intro conjI impI allI) 3678 apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id 3679 thread_control_update_mcp_def thread_control_update_priority_def 3680 cap_get_tag_isCap_unfolded_H_cap isCap_simps 3681 interpret_excaps_eq excaps_map_def)+ 3682 done 3683 3684lemma decodeSetIPCBuffer_ccorres: 3685 "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow> 3686 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 3687 (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple 3688 and valid_cap' cp and cte_at' slot and K (isThreadCap cp) 3689 and (excaps_in_mem extraCaps o ctes_of) 3690 and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s) 3691 and (\<lambda>s. \<forall>v \<in> set extraCaps. 3692 s \<turnstile>' fst v \<and> cte_at' (snd v) s) 3693 and (\<lambda>s. \<forall>v \<in> set extraCaps. 3694 ex_cte_cap_wp_to' isCNodeCap (snd v) s) 3695 and sysargs_rel args buffer) 3696 (UNIV 3697 \<inter> {s. ccap_relation cp (cap_' s)} 3698 \<inter> {s. unat (length___unsigned_long_' s) = length args} 3699 \<inter> {s. slot_' s = cte_Ptr slot} 3700 \<inter> {s. excaps_' s = extraCaps'} 3701 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 3702 (decodeSetIPCBuffer args cp slot extraCaps 3703 >>= invocationCatch thread isBlocking isCall InvokeTCB) 3704 (Call decodeSetIPCBuffer_'proc)" 3705 apply (cinit' lift: cap_' length___unsigned_long_' slot_' excaps_' buffer_' 3706 simp: decodeSetIPCBuffer_def) 3707 apply wpc 3708 apply (simp add: unat_eq_0) 3709 apply csymbr 3710 apply simp 3711 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 3712 apply vcg 3713 apply (rule conseqPre, vcg) 3714 apply (simp add: throwError_bind invocationCatch_def) 3715 apply (clarsimp simp: throwError_def return_def 3716 intr_and_se_rel_def exception_defs 3717 syscall_error_rel_def syscall_error_to_H_cases) 3718 apply csymbr 3719 apply (rule ccorres_cond_false_seq) 3720 apply csymbr 3721 apply (simp del: Collect_const) 3722 apply (simp add: interpret_excaps_test_null excaps_map_Nil if_1_0_0 3723 del: Collect_const) 3724 apply wpc 3725 apply (simp add: throwError_bind invocationCatch_def 3726 cong: StateSpace.state.fold_congs globals.fold_congs) 3727 apply (rule syscall_error_throwError_ccorres_n) 3728 apply (simp add: syscall_error_to_H_cases) 3729 apply (rule ccorres_cond_false_seq) 3730 apply (simp add: split_def 3731 del: Collect_const) 3732 apply (rule ccorres_add_return, 3733 ctac add: getSyscallArg_ccorres_foo [where args=args and n=0 and buffer=buffer]) 3734 apply csymbr 3735 apply (rule ccorres_move_c_guard_cte) 3736 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0]) 3737 apply ctac 3738 apply (rule ccorres_assert2) 3739 apply (rule ccorres_Cond_rhs_Seq) 3740 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr performInvocation_def) 3741 apply csymbr 3742 apply (ctac add: setThreadState_ccorres) 3743 apply csymbr 3744 apply csymbr 3745 apply csymbr 3746 apply (ctac add: invokeTCB_ThreadControl_ccorres) 3747 apply simp 3748 apply (rule ccorres_alternative2) 3749 apply (rule ccorres_return_CE, simp+)[1] 3750 apply (rule ccorres_return_C_errorE, simp+)[1] 3751 apply wp 3752 apply (vcg exspec=invokeTCB_ThreadControl_modifies) 3753 apply simp 3754 apply (wp sts_invs_minor') 3755 apply (vcg exspec=setThreadState_modifies) 3756 apply (simp add: bindE_assoc del: Collect_const) 3757 apply (rule ccorres_rhs_assoc)+ 3758 apply (csymbr, csymbr) 3759 apply (simp add: bindE_bind_linearise) 3760 apply (rule ccorres_split_nothrow_case_sum) 3761 apply (ctac add: deriveCap_ccorres) 3762 apply ceqv 3763 apply (simp add: Collect_False del: Collect_const) 3764 apply csymbr 3765 apply (rule ccorres_split_nothrow_case_sum) 3766 apply (ctac add: checkValidIPCBuffer_ccorres) 3767 apply ceqv 3768 apply (simp add: Collect_False returnOk_bind 3769 ccorres_invocationCatch_Inr 3770 del: Collect_const) 3771 apply (ctac add: setThreadState_ccorres) 3772 apply (simp add: performInvocation_def) 3773 apply (csymbr, csymbr, csymbr) 3774 apply (ctac add: invokeTCB_ThreadControl_ccorres) 3775 apply simp 3776 apply (rule ccorres_alternative2) 3777 apply (rule ccorres_return_CE, simp+)[1] 3778 apply (rule ccorres_return_C_errorE, simp+)[1] 3779 apply wp 3780 apply (vcg exspec=invokeTCB_ThreadControl_modifies) 3781 apply simp 3782 apply (wp sts_invs_minor') 3783 apply (simp add: Collect_const_mem cintr_def intr_and_se_rel_def) 3784 apply (vcg exspec=setThreadState_modifies) 3785 apply (simp add: invocationCatch_def) 3786 apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+) 3787 apply vcg 3788 apply simp 3789 apply (wp checkValidIPCBuffer_ArchObject_wp) 3790 apply (simp add: intr_and_se_rel_def syscall_error_rel_def 3791 exception_defs) 3792 apply (vcg exspec=checkValidIPCBuffer_modifies) 3793 apply (simp add: invocationCatch_def) 3794 apply (rule ccorres_split_throws) 3795 apply (rule ccorres_return_C_errorE, simp+)[1] 3796 apply vcg 3797 apply simp 3798 apply (wp | wp_once hoare_drop_imps)+ 3799 apply (simp add: Collect_const_mem) 3800 apply (vcg exspec=deriveCap_modifies) 3801 apply simp 3802 apply (wp | wp_once hoare_drop_imps)+ 3803 apply simp 3804 apply vcg 3805 apply wp 3806 apply simp 3807 apply (vcg exspec=getSyscallArg_modifies) 3808 apply (clarsimp simp: Collect_const_mem if_1_0_0 ct_in_state'_def 3809 pred_tcb_at' cintr_def intr_and_se_rel_def 3810 exception_defs syscall_error_rel_def) 3811 apply (rule conjI) 3812 apply (clarsimp simp: excaps_in_mem_def slotcap_in_mem_def) 3813 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 3814 apply (frule invs_mdb') 3815 apply (frule(2) tcb_at_capTCBPtr_CL) 3816 apply (auto simp: isCap_simps valid_cap'_def valid_mdb'_def valid_tcb_state'_def 3817 valid_mdb_ctes_def no_0_def excaps_map_def 3818 elim: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread' 3819 dest!: interpret_excaps_eq)[1] 3820 apply (clarsimp simp: option_to_0_def rf_sr_ksCurThread word_sless_def 3821 word_sle_def ThreadState_Restart_def mask_def) 3822 apply (rule conjI[rotated], clarsimp+) 3823 apply (drule interpret_excaps_eq[rule_format, where n=0], simp add: excaps_map_Nil) 3824 apply (simp add: mask_def "StrictC'_thread_state_defs" excaps_map_def) 3825 apply (clarsimp simp: ccap_rights_relation_def rightsFromWord_wordFromRights 3826 cap_get_tag_isCap) 3827 apply (frule cap_get_tag_to_H, subst cap_get_tag_isCap, assumption, assumption) 3828 apply clarsimp 3829 done 3830 3831lemma bindNTFN_alignment_junk: 3832 "\<lbrakk> is_aligned tcb tcbBlockSizeBits; bits \<le> ctcb_size_bits \<rbrakk> 3833 \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask bits = ptr_val (tcb_ptr_to_ctcb_ptr tcb)" 3834 apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def projectKOs) 3835 apply (rule is_aligned_neg_mask_eq) 3836 apply (erule aligned_add_aligned) 3837 apply (erule is_aligned_weaken[rotated]) 3838 by (auto simp add: is_aligned_def objBits_defs ctcb_offset_defs) 3839 3840lemma option_to_ctcb_ptr_canonical: 3841 "\<lbrakk>pspace_canonical' s; tcb_at' tcb s\<rbrakk> \<Longrightarrow> 3842 option_to_ctcb_ptr (Some tcb) = tcb_Ptr (sign_extend 47 (ptr_val (tcb_ptr_to_ctcb_ptr tcb)))" 3843 apply (clarsimp simp: option_to_ctcb_ptr_def) 3844 apply (frule (1) obj_at'_is_canonical) 3845 by (fastforce dest: canonical_address_tcb_ptr 3846 simp: obj_at'_def objBits_simps' projectKOs canonical_address_sign_extended 3847 sign_extended_iff_sign_extend) 3848 3849lemma bindNotification_ccorres: 3850 "ccorres dc xfdc (invs' and tcb_at' tcb) 3851 (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb} 3852 \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) [] 3853 (bindNotification tcb ntfnptr) 3854 (Call bindNotification_'proc)" 3855 apply (cinit lift: tcb_' ntfnPtr_' simp: bindNotification_def) 3856 apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) 3857 apply (rule_tac P="invs' and ko_at' rv ntfnptr and tcb_at' tcb" and P'=UNIV 3858 in ccorres_split_nothrow_novcg) 3859 apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) 3860 apply (rule allI, rule conseqPre, vcg) 3861 apply (clarsimp) 3862 apply (frule cmap_relation_ntfn) 3863 apply (erule (1) cmap_relation_ko_atE) 3864 apply (rule conjI) 3865 apply (erule h_t_valid_clift) 3866 apply (clarsimp simp: setNotification_def split_def) 3867 apply (rule bexI [OF _ setObject_eq]) 3868 apply (simp add: rf_sr_def cstate_relation_def Let_def init_def 3869 cpspace_relation_def update_ntfn_map_tos 3870 typ_heap_simps') 3871 apply (elim conjE) 3872 apply (intro conjI) 3873 \<comment> \<open>tcb relation\<close> 3874 apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) 3875 apply (clarsimp simp: cnotification_relation_def Let_def 3876 mask_def [where n=2] NtfnState_Waiting_def) 3877 apply (case_tac "ntfnObj rv") 3878 apply ((clarsimp simp: option_to_ctcb_ptr_canonical[OF invs_pspace_canonical'])+)[3] 3879 apply (auto simp: option_to_ctcb_ptr_def objBits_simps' 3880 bindNTFN_alignment_junk)[1] 3881 apply (simp add: carch_state_relation_def fpu_null_state_heap_update_tag_disj_simps 3882 global_ioport_bitmap_heap_update_tag_disj_simps) 3883 apply (simp add: cmachine_state_relation_def) 3884 apply (simp add: h_t_valid_clift_Some_iff) 3885 apply (simp add: objBits_simps') 3886 apply (simp add: objBits_simps) 3887 apply assumption 3888 apply ceqv 3889 apply (rule ccorres_move_c_guard_tcb) 3890 apply (simp add: setBoundNotification_def) 3891 apply (rule_tac P'=\<top> and P=\<top> in threadSet_ccorres_lemma3[unfolded dc_def]) 3892 apply vcg 3893 apply simp 3894 apply (erule (1) rf_sr_tcb_update_no_queue2, 3895 (simp add: typ_heap_simps')+, simp_all?)[1] 3896 apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) 3897 apply simp 3898 apply (wp get_ntfn_ko'| simp add: guard_is_UNIV_def)+ 3899 done 3900 3901lemma invokeTCB_NotificationControl_bind_ccorres: 3902 "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') 3903 (invs' and tcb_inv_wf' (tcbinvocation.NotificationControl t (Some a))) 3904 (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. ntfnPtr_' s = ntfn_Ptr a}) [] 3905 (invokeTCB (tcbinvocation.NotificationControl t (Some a))) 3906 (Call invokeTCB_NotificationControl_'proc)" 3907 apply (cinit lift: tcb_' ntfnPtr_') 3908 apply (clarsimp simp: option_to_0_def liftE_def) 3909 apply (rule ccorres_cond_true_seq) 3910 apply (ctac(no_vcg) add: bindNotification_ccorres) 3911 apply (rule ccorres_return_CE[unfolded returnOk_def, simplified]) 3912 apply simp 3913 apply simp 3914 apply simp 3915 apply wp 3916 apply (case_tac "a = 0", auto) 3917 done 3918 3919lemma invokeTCB_NotificationControl_unbind_ccorres: 3920 "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') 3921 (invs' and tcb_inv_wf' (tcbinvocation.NotificationControl t None)) 3922 (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. ntfnPtr_' s = NULL}) [] 3923 (invokeTCB (tcbinvocation.NotificationControl t None)) 3924 (Call invokeTCB_NotificationControl_'proc)" 3925 apply (cinit lift: tcb_' ntfnPtr_') 3926 apply (clarsimp simp add: option_to_0_def liftE_def) 3927 apply (ctac(no_vcg) add: unbindNotification_ccorres) 3928 apply (rule ccorres_return_CE[unfolded returnOk_def, simplified]) 3929 apply simp 3930 apply simp 3931 apply simp 3932 apply wp 3933 apply (clarsimp simp: option_to_0_def) 3934 done 3935 3936lemma valid_objs_boundNTFN_NULL: 3937 "ko_at' tcb p s ==> valid_objs' s \<Longrightarrow> no_0_obj' s \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0" 3938 apply (drule(1) obj_at_valid_objs') 3939 apply (clarsimp simp: valid_tcb'_def projectKOs valid_obj'_def) 3940 done 3941 3942lemma decodeUnbindNotification_ccorres: 3943 "ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 3944 (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple 3945 and valid_cap' cp and K (isThreadCap cp) 3946 and tcb_at' (capTCBPtr cp) 3947 and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s)) 3948 (UNIV \<inter> {s. ccap_relation cp (cap_' s)}) [] 3949 (decodeUnbindNotification cp >>= invocationCatch thread isBlocking isCall InvokeTCB) 3950 (Call decodeUnbindNotification_'proc)" 3951 apply (cinit' lift: cap_' simp: decodeUnbindNotification_def) 3952 apply csymbr 3953 apply csymbr 3954 apply (rule ccorres_Guard_Seq) 3955 apply (simp add: liftE_bindE bind_assoc) 3956 apply (rule ccorres_pre_getBoundNotification) 3957 apply (rule_tac P="\<lambda>s. rv \<noteq> Some 0" in ccorres_cross_over_guard) 3958 apply (simp add: bindE_bind_linearise) 3959 apply wpc 3960 apply (simp add: bindE_bind_linearise[symmetric] 3961 injection_handler_throwError 3962 invocationCatch_use_injection_handler) 3963 apply (rule ccorres_cond_true_seq) 3964 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 3965 apply vcg 3966 apply (rule conseqPre, vcg) 3967 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def 3968 syscall_error_to_H_cases exception_defs) 3969 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr 3970 performInvocation_def) 3971 apply (rule ccorres_cond_false_seq) 3972 apply simp 3973 apply (ctac add: setThreadState_ccorres) 3974 apply (ctac add: invokeTCB_NotificationControl_unbind_ccorres) 3975 apply simp 3976 apply (rule ccorres_alternative2) 3977 apply (rule ccorres_return_CE, simp+)[1] 3978 apply (rule ccorres_return_C_errorE, simp+)[1] 3979 apply wp 3980 apply (vcg exspec=invokeTCB_NotificationControl_modifies) 3981 apply simp 3982 apply (wp sts_invs_minor' hoare_case_option_wp sts_bound_tcb_at' | wpc | simp)+ 3983 apply (vcg exspec=setThreadState_modifies) 3984 apply (clarsimp, frule obj_at_ko_at', clarsimp) 3985 apply (rule cmap_relationE1[OF cmap_relation_tcb], assumption) 3986 apply (erule ko_at_projectKO_opt) 3987 apply (clarsimp simp: isCap_simps) 3988 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3989 apply (auto simp: ctcb_relation_def typ_heap_simps cap_get_tag_ThreadCap ct_in_state'_def 3990 option_to_ptr_def option_to_0_def ThreadState_Restart_def 3991 mask_def rf_sr_ksCurThread valid_tcb_state'_def 3992 elim!: pred_tcb'_weakenE 3993 dest!: valid_objs_boundNTFN_NULL) 3994 done 3995 3996lemma nTFN_case_If_ptr: 3997 "(case x of capability.NotificationCap a b c d \<Rightarrow> P a d | _ \<Rightarrow> Q) = (if (isNotificationCap x) then P (capNtfnPtr x) (capNtfnCanReceive x) else Q)" 3998 by (auto simp: isNotificationCap_def split: capability.splits) 3999 4000lemma decodeBindNotification_ccorres: 4001 notes prod.case_cong_weak[cong] 4002 option.case_cong_weak[cong] 4003 shows 4004 "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow> 4005 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 4006 (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple 4007 and valid_cap' cp 4008 and tcb_at' (capTCBPtr cp) and ex_nonz_cap_to' (capTCBPtr cp) 4009 and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s) 4010 and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v). ex_nonz_cap_to' y s ) 4011 and (excaps_in_mem extraCaps o ctes_of) 4012 and K (isThreadCap cp)) 4013 (UNIV \<inter> {s. ccap_relation cp (cap_' s)} 4014 \<inter> {s. excaps_' s = extraCaps'}) [] 4015 (decodeBindNotification cp extraCaps >>= invocationCatch thread isBlocking isCall InvokeTCB) 4016 (Call decodeBindNotification_'proc)" 4017 using [[goals_limit=1]] 4018 apply (simp, rule ccorres_gen_asm) 4019 apply (cinit' lift: cap_' excaps_' simp: decodeBindNotification_def) 4020 apply (simp add: bind_assoc whenE_def bind_bindE_assoc interpret_excaps_test_null 4021 del: Collect_const cong: call_ignore_cong) 4022 apply (rule ccorres_Cond_rhs_Seq) 4023 apply (simp add: excaps_map_def invocationCatch_def throwError_bind null_def 4024 cong: StateSpace.state.fold_congs globals.fold_congs) 4025 apply (rule syscall_error_throwError_ccorres_n) 4026 apply (simp add: syscall_error_to_H_cases) 4027 apply (simp add: excaps_map_def null_def del: Collect_const cong: call_ignore_cong) 4028 apply csymbr 4029 apply csymbr 4030 apply (rule ccorres_Guard_Seq) 4031 apply (simp add: liftE_bindE bind_assoc cong: call_ignore_cong) 4032 apply (rule ccorres_pre_getBoundNotification) 4033 apply (rule_tac P="\<lambda>s. rv \<noteq> Some 0" in ccorres_cross_over_guard) 4034 apply (simp add: bindE_bind_linearise cong: call_ignore_cong) 4035 apply wpc 4036 prefer 2 4037 apply (simp add: bindE_bind_linearise[symmetric] injection_handler_throwError 4038 invocationCatch_use_injection_handler throwError_bind invocationCatch_def) 4039 apply (rule ccorres_cond_true_seq) 4040 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4041 apply vcg 4042 apply (rule conseqPre, vcg) 4043 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def syscall_error_to_H_cases 4044 exception_defs) 4045 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr performInvocation_def 4046 bindE_bind_linearise[symmetric] cong: call_ignore_cong) 4047 apply (rule ccorres_cond_false_seq) 4048 apply (simp cong: call_ignore_cong) 4049 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0]) 4050 apply (rule ccorres_move_c_guard_cte) 4051 apply ctac 4052 apply csymbr 4053 apply (simp add: cap_get_tag_isCap if_1_0_0 del: Collect_const cong: call_ignore_cong) 4054 apply (rule ccorres_assert2) 4055 apply (rule ccorres_Cond_rhs_Seq) 4056 apply (rule_tac P="Q (capNtfnPtr rva) (capNtfnCanReceive rva) rva"for Q in ccorres_inst) 4057 apply (rule ccorres_rhs_assoc)+ 4058 apply csymbr 4059 apply csymbr 4060 apply (simp add: hd_conv_nth del: Collect_const cong: call_ignore_cong) 4061 apply (simp only: cap_get_tag_isCap(3)[symmetric] cong: call_ignore_cong, frule(1) cap_get_tag_to_H(3) ) 4062 apply (simp add: case_bool_If if_to_top_of_bindE if_to_top_of_bind bind_assoc 4063 del: Collect_const cong: if_cong call_ignore_cong) 4064 apply csymbr 4065 apply (clarsimp simp add: if_to_top_of_bind to_bool_eq_0[symmetric] simp del: Collect_const) 4066 apply (rule ccorres_Cond_rhs_Seq) 4067 apply (clarsimp simp: to_bool_def throwError_bind invocationCatch_def) 4068 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4069 apply vcg 4070 apply (rule conseqPre, vcg) 4071 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def syscall_error_to_H_cases exception_defs) 4072 apply (clarsimp simp: to_bool_def) 4073 apply (rule ccorres_pre_getNotification) 4074 apply (rename_tac ntfn) 4075 apply (rule ccorres_rhs_assoc2) 4076 apply (rule ccorres_rhs_assoc2) 4077 apply (rule_tac xf'="ret__int_'" and val="from_bool (ntfnBoundTCB ntfn \<noteq> None \<or> 4078 isWaitingNtfn (ntfnObj ntfn))" 4079 and R="ko_at' ntfn (capNtfnPtr_CL (cap_notification_cap_lift ntfn_cap)) 4080 and valid_ntfn' ntfn" 4081 and R'=UNIV 4082 in ccorres_symb_exec_r_known_rv_UNIV) 4083 apply (rule conseqPre, vcg) 4084 apply (clarsimp simp: if_1_0_0) 4085 4086 apply (erule cmap_relationE1[OF cmap_relation_ntfn], erule ko_at_projectKO_opt) 4087 apply (clarsimp simp: typ_heap_simps cnotification_relation_def Let_def 4088 valid_ntfn'_def) 4089 apply (case_tac "ntfnObj ntfn", simp_all add: isWaitingNtfn_def option_to_ctcb_ptr_def 4090 false_def true_def split: option.split_asm if_split, 4091 auto simp: neq_Nil_conv tcb_queue_relation'_def tcb_at_not_NULL[symmetric] 4092 tcb_at_not_NULL)[1] 4093 apply ceqv 4094 apply (rule_tac P="\<lambda>s. ksCurThread s = thread" in ccorres_cross_over_guard) 4095 apply (simp add: bindE_bind_linearise del: Collect_const) 4096 apply wpc 4097 \<comment> \<open>IdleNtfn\<close> 4098 apply (simp add: case_option_If del: Collect_const) 4099 apply (rule ccorres_Cond_rhs_Seq) 4100 apply (clarsimp simp: isWaitingNtfn_def from_bool_neq_0) 4101 apply (simp add: bindE_bind_linearise[symmetric] injection_handler_throwError 4102 invocationCatch_use_injection_handler throwError_bind invocationCatch_def) 4103 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4104 apply vcg 4105 apply (rule conseqPre, vcg) 4106 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def 4107 syscall_error_to_H_cases exception_defs) 4108 apply (clarsimp simp: isWaitingNtfn_def from_bool_neq_0 returnOk_bind) 4109 apply (clarsimp simp: isWaitingNtfn_def from_bool_neq_0 returnOk_bind 4110 ccorres_invocationCatch_Inr performInvocation_def) 4111 apply (ctac add: setThreadState_ccorres) 4112 apply (ctac add: invokeTCB_NotificationControl_bind_ccorres) 4113 apply simp 4114 apply (rule ccorres_alternative2) 4115 apply (rule ccorres_return_CE, simp+)[1] 4116 apply (rule ccorres_return_C_errorE, simp+)[1] 4117 apply wp 4118 apply (vcg exspec=invokeTCB_NotificationControl_modifies) 4119 apply simp 4120 apply (wp sts_invs_minor' hoare_case_option_wp sts_bound_tcb_at' | wpc | simp)+ 4121 apply (vcg exspec=setThreadState_modifies) 4122 apply (simp add: case_option_If del: Collect_const) 4123 apply (rule ccorres_Cond_rhs_Seq) 4124 apply (clarsimp simp: isWaitingNtfn_def from_bool_neq_0) 4125 apply (simp add: bindE_bind_linearise[symmetric] injection_handler_throwError 4126 invocationCatch_use_injection_handler throwError_bind invocationCatch_def) 4127 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4128 apply vcg 4129 apply (rule conseqPre, vcg) 4130 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def 4131 syscall_error_to_H_cases exception_defs) 4132 apply (clarsimp simp: isWaitingNtfn_def from_bool_neq_0 returnOk_bind) 4133 apply (clarsimp simp: isWaitingNtfn_def from_bool_neq_0 returnOk_bind 4134 ccorres_invocationCatch_Inr performInvocation_def) 4135 apply (ctac add: setThreadState_ccorres) 4136 apply (ctac add: invokeTCB_NotificationControl_bind_ccorres) 4137 apply simp 4138 apply (rule ccorres_alternative2) 4139 apply (rule ccorres_return_CE, simp+)[1] 4140 apply (rule ccorres_return_C_errorE, simp+)[1] 4141 apply wp 4142 apply (vcg exspec=invokeTCB_NotificationControl_modifies) 4143 apply simp 4144 apply (wp sts_invs_minor' hoare_case_option_wp sts_bound_tcb_at' | wpc | simp)+ 4145 apply (vcg exspec=setThreadState_modifies) 4146 apply (simp add: bindE_bind_linearise[symmetric] injection_handler_throwError 4147 invocationCatch_use_injection_handler throwError_bind invocationCatch_def) 4148 apply (rule ccorres_cond_true_seq) 4149 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4150 apply vcg 4151 apply (rule conseqPre, vcg) 4152 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def 4153 syscall_error_to_H_cases exception_defs) 4154 apply (clarsimp simp add: guard_is_UNIV_def isWaitingNtfn_def from_bool_0 4155 ThreadState_Restart_def mask_def true_def 4156 rf_sr_ksCurThread capTCBPtr_eq) 4157 apply (simp add: hd_conv_nth bindE_bind_linearise nTFN_case_If_ptr throwError_bind invocationCatch_def) 4158 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4159 apply vcg 4160 apply (rule conseqPre, vcg) 4161 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def syscall_error_to_H_cases 4162 exception_defs) 4163 apply clarsimp 4164 apply (wp | simp | wpc | wp_once hoare_drop_imps)+ 4165 apply vcg 4166 apply clarsimp 4167 apply (rule conjI) 4168 apply safe[1] 4169 apply (fastforce simp: invs'_def valid_state'_def valid_pspace'_def 4170 dest!: valid_objs_boundNTFN_NULL) 4171 apply ((fastforce elim!: pred_tcb'_weakenE obj_at'_weakenE 4172 simp: ct_in_state'_def from_bool_0 isCap_simps excaps_map_def 4173 neq_Nil_conv obj_at'_def pred_tcb_at'_def valid_tcb_state'_def)+)[12] 4174 apply (clarsimp dest!: obj_at_valid_objs'[OF _ invs_valid_objs'] 4175 simp: projectKOs valid_obj'_def) 4176 apply (clarsimp simp: excaps_map_Nil cte_wp_at_ctes_of excaps_map_def neq_Nil_conv 4177 dest!: interpret_excaps_eq ) 4178 apply (clarsimp simp: excaps_map_Nil) 4179 apply (frule obj_at_ko_at', clarsimp) 4180 apply (rule cmap_relationE1[OF cmap_relation_tcb], assumption) 4181 apply (erule ko_at_projectKO_opt) 4182 apply (clarsimp simp: isCap_simps) 4183 apply (frule cap_get_tag_isCap_unfolded_H_cap) 4184 apply safe[1] 4185 apply (clarsimp simp: typ_heap_simps excaps_map_def neq_Nil_conv 4186 dest!: interpret_excaps_eq) 4187 apply clarsimp 4188 apply (frule cap_get_tag_isCap_unfolded_H_cap(3)) 4189 apply (clarsimp simp: typ_heap_simps cap_get_tag_ThreadCap ccap_relation_def) 4190 apply (auto simp: word_sless_alt typ_heap_simps cap_get_tag_ThreadCap ctcb_relation_def 4191 option_to_ptr_def option_to_0_def 4192 split: if_split) 4193 done 4194 4195 4196lemma decodeSetSpace_ccorres: 4197 notes tl_drop_1[simp] scast_mask_8 [simp] 4198 shows 4199 "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow> 4200 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 4201 (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple 4202 and valid_cap' cp and cte_at' slot and K (isThreadCap cp) 4203 and tcb_at' (capTCBPtr cp) 4204 and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s) 4205 and (excaps_in_mem extraCaps o ctes_of) 4206 and (\<lambda>s. \<forall>v \<in> set extraCaps. 4207 s \<turnstile>' fst v \<and> cte_at' (snd v) s) 4208 and (\<lambda>s. \<forall>v \<in> set extraCaps. 4209 ex_cte_cap_wp_to' isCNodeCap (snd v) s) 4210 and sysargs_rel args buffer) 4211 (UNIV 4212 \<inter> {s. ccap_relation cp (cap_' s)} 4213 \<inter> {s. unat (length___unsigned_long_' s) = length args} 4214 \<inter> {s. slot_' s = cte_Ptr slot} 4215 \<inter> {s. excaps_' s = extraCaps'} 4216 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 4217 (decodeSetSpace args cp slot extraCaps 4218 >>= invocationCatch thread isBlocking isCall InvokeTCB) 4219 (Call decodeSetSpace_'proc)" 4220 apply (cinit' lift: cap_' length___unsigned_long_' slot_' excaps_' buffer_' 4221 simp: decodeSetSpace_def) 4222 apply csymbr 4223 apply (rule ccorres_Cond_rhs_Seq) 4224 apply (simp add: if_1_0_0) 4225 apply (rule ccorres_cond_true_seq | simp)+ 4226 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4227 apply vcg 4228 apply (rule conseqPre, vcg) 4229 apply (subgoal_tac "unat length___unsigned_long < 3") 4230 apply (clarsimp simp: throwError_def invocationCatch_def fst_return 4231 intr_and_se_rel_def syscall_error_rel_def 4232 syscall_error_to_H_cases exception_defs 4233 subset_iff 4234 split: list.split) 4235 apply unat_arith 4236 apply csymbr 4237 apply (rule ccorres_Cond_rhs_Seq) 4238 apply (simp add: if_1_0_0 interpret_excaps_test_null excaps_map_Nil) 4239 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4240 apply vcg 4241 apply (rule conseqPre, vcg) 4242 apply clarsimp 4243 apply (clarsimp simp: throwError_def invocationCatch_def fst_return 4244 intr_and_se_rel_def syscall_error_rel_def 4245 syscall_error_to_H_cases exception_defs 4246 split: list.split) 4247 apply csymbr 4248 apply (simp add: if_1_0_0 interpret_excaps_test_null del: Collect_const) 4249 apply (rule_tac P="\<lambda>c. ccorres rvr xf P P' hs a (Cond c c1 c2 ;; c3)" for rvr xf P P' hs a c1 c2 c3 in ssubst) 4250 apply (rule Collect_cong) 4251 apply (rule interpret_excaps_test_null) 4252 apply (clarsimp simp: neq_Nil_conv) 4253 apply simp 4254 apply (rule ccorres_Cond_rhs_Seq) 4255 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4256 apply vcg 4257 apply (rule conseqPre, vcg) 4258 apply clarsimp 4259 apply (clarsimp simp: throwError_def invocationCatch_def fst_return 4260 intr_and_se_rel_def syscall_error_rel_def 4261 syscall_error_to_H_cases exception_defs 4262 excaps_map_def 4263 split: list.split) 4264 apply (clarsimp simp add: linorder_not_less word_le_nat_alt 4265 excaps_map_Nil length_excaps_map 4266 simp del: Collect_const) 4267 apply (drule_tac a="Suc 0" in neq_le_trans [OF not_sym]) 4268 apply (clarsimp simp: neq_Nil_conv) 4269 apply (rule_tac P="\<lambda>a. ccorres rvr xf P P' hs a c" for rvr xf P P' hs c in ssubst, 4270 rule bind_cong [OF _ refl], rule list_case_helper, 4271 clarsimp)+ 4272 apply (simp add: hd_drop_conv_nth2 del: Collect_const) 4273 apply (rule ccorres_add_return, 4274 ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer]) 4275 apply (rule ccorres_add_return, 4276 ctac add: getSyscallArg_ccorres_foo[where args=args and n=1 and buffer=buffer]) 4277 apply (rule ccorres_add_return, 4278 ctac add: getSyscallArg_ccorres_foo[where args=args and n=2 and buffer=buffer]) 4279 apply csymbr 4280 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0]) 4281 apply (rule ccorres_move_c_guard_cte) 4282 apply ctac 4283 apply (rule ccorres_assert2) 4284 apply csymbr 4285 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=1]) 4286 apply (rule ccorres_move_c_guard_cte) 4287 apply ctac 4288 apply (rule ccorres_assert2) 4289 apply csymbr 4290 apply (simp add: decodeSetSpace_def injection_bindE[OF refl] 4291 split_def 4292 tcb_cnode_index_defs[THEN ptr_add_assertion_positive[OF ptr_add_assertion_positive_helper]] 4293 del: Collect_const) 4294 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq 4295 ccorres_rhs_assoc)+ 4296 apply (simp add: injection_liftE[OF refl] bindE_assoc 4297 liftM_def getThreadCSpaceRoot 4298 getThreadVSpaceRoot del: Collect_const) 4299 apply (simp add: liftE_bindE bind_assoc del: Collect_const) 4300 apply (ctac add: slotCapLongRunningDelete_ccorres) 4301 apply (rule ccorres_move_array_assertion_tcb_ctes) 4302 apply (simp del: Collect_const) 4303 apply csymbr 4304 apply (clarsimp simp add: if_1_0_0 from_bool_0 4305 simp del: Collect_const) 4306 apply (rule ccorres_Cond_rhs_Seq) 4307 apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_slotCapLongRunningDelete]) 4308 apply (simp add: unlessE_def throwError_bind invocationCatch_def 4309 cong: StateSpace.state.fold_congs globals.fold_congs) 4310 apply (rule ccorres_cond_true_seq) 4311 apply (rule syscall_error_throwError_ccorres_n) 4312 apply (simp add: syscall_error_to_H_cases) 4313 apply wp+ 4314 apply (rule ccorres_rhs_assoc)+ 4315 apply csymbr 4316 apply (simp add: tcb_cnode_index_defs[THEN ptr_add_assertion_positive[OF ptr_add_assertion_positive_helper]] 4317 del: Collect_const) 4318 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq 4319 ccorres_rhs_assoc)+ 4320 apply (ctac add: slotCapLongRunningDelete_ccorres) 4321 apply (rule ccorres_move_array_assertion_tcb_ctes) 4322 apply (simp del: Collect_const) 4323 apply csymbr 4324 apply (clarsimp simp add: if_1_0_0 from_bool_0 4325 simp del: Collect_const) 4326 apply (rule ccorres_Cond_rhs_Seq) 4327 apply (simp add: unlessE_def throwError_bind invocationCatch_def 4328 cong: StateSpace.state.fold_congs globals.fold_congs) 4329 apply (rule syscall_error_throwError_ccorres_n) 4330 apply (simp add: syscall_error_to_H_cases) 4331 apply (simp add: unlessE_def 4332 del: Collect_const) 4333 apply (rule ccorres_add_return, 4334 rule_tac r'="\<lambda>rv rv'. ccap_relation (if args ! Suc 0 = 0 then fst (hd extraCaps) 4335 else updateCapData False (args ! Suc 0) (fst (hd extraCaps))) rv'" 4336 and xf'="cRootCap_'" in ccorres_split_nothrow) 4337 apply (rule_tac P'="{s. cRootCap = cRootCap_' s}" 4338 in ccorres_from_vcg[where P=\<top>]) 4339 apply (rule allI, rule conseqPre, vcg) 4340 apply (subgoal_tac "extraCaps \<noteq> []") 4341 apply (clarsimp simp: returnOk_def return_def hd_conv_nth false_def) 4342 apply fastforce 4343 apply clarsimp 4344 apply ceqv 4345 apply (simp add: invocationCatch_use_injection_handler 4346 injection_bindE [OF refl refl] bindE_assoc 4347 del: Collect_const) 4348 apply (ctac add: ccorres_injection_handler_csum1 4349 [OF deriveCap_ccorres]) 4350 apply (simp add: Collect_False del: Collect_const) 4351 apply csymbr 4352 apply csymbr 4353 apply (simp add: cnode_cap_case_if cap_get_tag_isCap dc_def[symmetric] 4354 del: Collect_const) 4355 apply (rule ccorres_Cond_rhs_Seq) 4356 apply (simp add: injection_handler_throwError 4357 cong: StateSpace.state.fold_congs globals.fold_congs) 4358 apply (rule syscall_error_throwError_ccorres_n) 4359 apply (simp add: syscall_error_to_H_cases) 4360 apply (simp add: injection_handler_returnOk del: Collect_const) 4361 apply (rule ccorres_add_return, 4362 rule_tac r'="\<lambda>rv rv'. ccap_relation (if args ! 2 = 0 then fst (extraCaps ! Suc 0) 4363 else updateCapData False (args ! 2) (fst (extraCaps ! Suc 0))) rv'" 4364 and xf'="vRootCap_'" in ccorres_split_nothrow) 4365 apply (rule_tac P'="{s. vRootCap = vRootCap_' s}" 4366 in ccorres_from_vcg[where P=\<top>]) 4367 apply (rule allI, rule conseqPre, vcg) 4368 apply (clarsimp simp: returnOk_def return_def 4369 hd_drop_conv_nth2 false_def) 4370 apply fastforce 4371 apply ceqv 4372 apply (ctac add: ccorres_injection_handler_csum1 4373 [OF deriveCap_ccorres]) 4374 apply (simp add: Collect_False del: Collect_const) 4375 apply csymbr 4376 apply csymbr 4377 apply (simp add: from_bool_0 isValidVTableRoot_conv del: Collect_const) 4378 apply (rule ccorres_Cond_rhs_Seq) 4379 apply (simp add: injection_handler_throwError 4380 cong: StateSpace.state.fold_congs globals.fold_congs) 4381 apply (rule syscall_error_throwError_ccorres_n) 4382 apply (simp add: syscall_error_to_H_cases) 4383 apply (simp add: injection_handler_returnOk ccorres_invocationCatch_Inr 4384 performInvocation_def) 4385 apply (ctac add: setThreadState_ccorres) 4386 apply csymbr 4387 apply csymbr 4388 apply (ctac(no_vcg) add: invokeTCB_ThreadControl_ccorres) 4389 apply simp 4390 apply (rule ccorres_alternative2) 4391 apply (rule ccorres_return_CE, simp+)[1] 4392 apply (rule ccorres_return_C_errorE, simp+)[1] 4393 apply wp 4394 apply simp 4395 apply (wp sts_invs_minor') 4396 apply (vcg exspec=setThreadState_modifies) 4397 apply simp 4398 apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+) 4399 apply vcg 4400 apply simp 4401 apply (wp hoare_drop_imps) 4402 apply (wp injection_wp_E [OF refl]) 4403 apply (simp add: Collect_const_mem cintr_def intr_and_se_rel_def 4404 all_ex_eq_helper syscall_error_rel_def 4405 exception_defs) 4406 apply (vcg exspec=deriveCap_modifies) 4407 apply (simp cong: if_cong) 4408 apply wp 4409 apply (simp add: Collect_const_mem all_ex_eq_helper) 4410 apply vcg 4411 apply simp 4412 apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+) 4413 apply vcg 4414 apply (simp cong: if_cong) 4415 apply (wp hoare_drop_imps injection_wp_E[OF refl]) 4416 apply (simp add: Collect_const_mem all_ex_eq_helper 4417 numeral_eqs syscall_error_rel_def 4418 exception_defs cintr_def intr_and_se_rel_def) 4419 apply (vcg exspec=deriveCap_modifies) 4420 apply (simp cong: if_cong) 4421 apply wp 4422 apply (simp add: Collect_const_mem all_ex_eq_helper 4423 numeral_eqs syscall_error_rel_def 4424 exception_defs cintr_def intr_and_se_rel_def 4425 hd_drop_conv_nth2 4426 cong: if_cong) 4427 apply vcg 4428 apply (simp cong: if_cong) 4429 apply (wp hoare_drop_imps) 4430 apply (simp add: Collect_const_mem) 4431 apply (vcg exspec=slotCapLongRunningDelete_modifies) 4432 apply (simp cong: if_cong) 4433 apply (wp hoare_drop_imps) 4434 apply (simp add: Collect_const_mem all_ex_eq_helper 4435 numeral_eqs syscall_error_rel_def 4436 exception_defs cintr_def intr_and_se_rel_def) 4437 apply (vcg exspec=slotCapLongRunningDelete_modifies) 4438 apply (simp add: pred_conj_def cong: if_cong) 4439 apply (strengthen if_n_updateCapData_valid_strg) 4440 apply (wp hoare_drop_imps) 4441 apply (simp add: Collect_const_mem all_ex_eq_helper 4442 numeral_eqs syscall_error_rel_def 4443 exception_defs cintr_def intr_and_se_rel_def) 4444 apply vcg 4445 apply simp 4446 apply (wp hoare_drop_imps) 4447 apply (simp add: Collect_const_mem all_ex_eq_helper 4448 numeral_eqs syscall_error_rel_def 4449 exception_defs cintr_def intr_and_se_rel_def) 4450 apply vcg 4451 apply simp 4452 apply (wp hoare_drop_imps) 4453 apply (simp add: Collect_const_mem all_ex_eq_helper 4454 numeral_eqs syscall_error_rel_def 4455 exception_defs cintr_def intr_and_se_rel_def 4456 cong: if_cong 4457 | vcg exspec=getSyscallArg_modifies 4458 | wp)+ 4459 apply (clarsimp simp: if_1_0_0 word_less_nat_alt) 4460 apply (rule conjI) 4461 apply (clarsimp simp: ct_in_state'_def interpret_excaps_test_null 4462 excaps_map_def neq_Nil_conv) 4463 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 4464 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 4465 apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def) 4466 apply (frule(2) tcb_at_capTCBPtr_CL) 4467 apply (auto simp: isCap_simps valid_tcb_state'_def objBits_defs mask_def 4468 elim!: pred_tcb'_weakenE 4469 dest!: st_tcb_at_idle_thread' interpret_excaps_eq)[1] 4470 apply (clarsimp simp: linorder_not_le interpret_excaps_test_null 4471 excaps_map_def neq_Nil_conv word_sle_def 4472 word_sless_def) 4473 apply (frule interpret_excaps_eq[rule_format, where n=0], simp) 4474 apply (frule interpret_excaps_eq[rule_format, where n=1], simp) 4475 apply (clarsimp simp: mask_def[where n=4] ccap_rights_relation_def 4476 rightsFromWord_wordFromRights 4477 capTCBPtr_eq tcb_cnode_index_defs size_of_def 4478 option_to_0_def rf_sr_ksCurThread 4479 "StrictC'_thread_state_defs" mask_eq_iff_w2p word_size) 4480 apply (simp add: word_sle_def cap_get_tag_isCap) 4481 apply (subgoal_tac "args \<noteq> []") 4482 apply (clarsimp simp: hd_conv_nth) 4483 apply (drule sym, simp, simp add: true_def from_bool_0) 4484 apply (clarsimp simp: objBits_simps') 4485 apply fastforce 4486 apply clarsimp 4487 done 4488 4489lemma invokeTCB_SetTLSBase_ccorres: 4490 notes static_imp_wp [wp] 4491 shows 4492 "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') 4493 (invs') 4494 ({s. thread_' s = tcb_ptr_to_ctcb_ptr tcb} 4495 \<inter> {s. tls_base_' s = tls_base}) [] 4496 (invokeTCB (SetTLSBase tcb tls_base)) 4497 (Call invokeSetTLSBase_'proc)" 4498 apply (cinit lift: thread_' tls_base_') 4499 apply (simp add: liftE_def bind_assoc 4500 del: Collect_const) 4501 apply (ctac add: setRegister_ccorres[simplified dc_def]) 4502 apply (rule ccorres_pre_getCurThread) 4503 apply (rename_tac cur_thr) 4504 apply (rule ccorres_split_nothrow_novcg_dc) 4505 apply (rule_tac R="\<lambda>s. cur_thr = ksCurThread s" in ccorres_when) 4506 apply (clarsimp simp: rf_sr_ksCurThread) 4507 apply clarsimp 4508 apply (ctac (no_vcg) add: rescheduleRequired_ccorres) 4509 apply (unfold return_returnOk)[1] 4510 apply (rule ccorres_return_CE, simp+)[1] 4511 apply (wpsimp wp: hoare_drop_imp simp: guard_is_UNIV_def)+ 4512 apply vcg 4513 apply (clarsimp simp: tlsBaseRegister_def X64.tlsBaseRegister_def 4514 invs_weak_sch_act_wf invs_queues 4515 split: if_split) 4516 done 4517 4518lemma decodeSetTLSBase_ccorres: 4519 "ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 4520 (invs' and sch_act_simple 4521 and (\<lambda>s. ksCurThread s = thread) and ct_active' and K (isThreadCap cp) 4522 and valid_cap' cp and (\<lambda>s. \<forall>x \<in> zobj_refs' cp. ex_nonz_cap_to' x s) 4523 and sysargs_rel args buffer) 4524 (UNIV 4525 \<inter> {s. ccap_relation cp (cap_' s)} 4526 \<inter> {s. unat (length___unsigned_long_' s) = length args} 4527 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 4528 (decodeSetTLSBase args cp 4529 >>= invocationCatch thread isBlocking isCall InvokeTCB) 4530 (Call decodeSetTLSBase_'proc)" 4531 apply (cinit' lift: cap_' length___unsigned_long_' buffer_' 4532 simp: decodeSetTLSBase_def) 4533 apply wpc 4534 apply (simp add: throwError_bind invocationCatch_def) 4535 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 4536 apply vcg 4537 apply (rule conseqPre, vcg) 4538 apply (clarsimp simp: throwError_def return_def 4539 exception_defs syscall_error_rel_def 4540 syscall_error_to_H_cases) 4541 apply (rule ccorres_cond_false_seq; simp) 4542 apply (rule ccorres_add_return, 4543 ctac add: getSyscallArg_ccorres_foo'[where args=args and n=0 and buffer=buffer]) 4544 apply (simp add: invocationCatch_use_injection_handler 4545 bindE_assoc injection_handler_returnOk 4546 ccorres_invocationCatch_Inr performInvocation_def) 4547 apply (ctac add: setThreadState_ccorres) 4548 apply csymbr 4549 apply (ctac (no_vcg) add: invokeTCB_SetTLSBase_ccorres) 4550 apply simp 4551 apply (rule ccorres_alternative2) 4552 apply (rule ccorres_return_CE, simp+)[1] 4553 apply (rule ccorres_return_C_errorE, simp+)[1] 4554 apply (wpsimp wp: sts_invs_minor')+ 4555 apply (vcg exspec=setThreadState_modifies) 4556 apply wp 4557 apply vcg 4558 apply (clarsimp simp: Collect_const_mem) 4559 apply (rule conjI) 4560 apply (clarsimp simp: ct_in_state'_def sysargs_rel_n_def n_msgRegisters_def) 4561 apply (auto simp: valid_tcb_state'_def 4562 elim!: pred_tcb'_weakenE)[1] 4563 apply (simp add: StrictC'_thread_state_defs mask_eq_iff_w2p word_size) 4564 apply (frule rf_sr_ksCurThread) 4565 apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) 4566 apply (auto simp: unat_eq_0 le_max_word_ucast_id)+ 4567 done 4568 4569lemma decodeTCBInvocation_ccorres: 4570 "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow> 4571 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 4572 (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple 4573 and valid_cap' cp and cte_at' slot and K (isThreadCap cp) 4574 and (excaps_in_mem extraCaps o ctes_of) 4575 and tcb_at' (capTCBPtr cp) and ex_nonz_cap_to' (capTCBPtr cp) 4576 and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v). 4577 ex_nonz_cap_to' y s) 4578 and (\<lambda>s. \<forall>v \<in> set extraCaps. 4579 s \<turnstile>' fst v \<and> cte_at' (snd v) s) 4580 and (\<lambda>s. \<forall>v \<in> set extraCaps. 4581 ex_cte_cap_wp_to' isCNodeCap (snd v) s) 4582 and sysargs_rel args buffer) 4583 (UNIV 4584 \<inter> {s. invLabel_' s = label} 4585 \<inter> {s. ccap_relation cp (cap_' s)} 4586 \<inter> {s. unat (length___unsigned_long_' s) = length args} 4587 \<inter> {s. slot_' s = cte_Ptr slot} 4588 \<inter> {s. excaps_' s = extraCaps'} 4589 \<inter> {s. call_' s = from_bool isCall} 4590 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 4591 (decodeTCBInvocation label args cp slot extraCaps 4592 >>= invocationCatch thread isBlocking isCall InvokeTCB) 4593 (Call decodeTCBInvocation_'proc)" 4594 apply (cinit' lift: invLabel_' cap_' length___unsigned_long_' slot_' excaps_' call_' buffer_') 4595 apply (simp add: decodeTCBInvocation_def invocation_eq_use_types 4596 del: Collect_const) 4597 apply (rule ccorres_Cond_rhs) 4598 apply simp 4599 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeReadRegisters_ccorres [where buffer=buffer]) 4600 apply (rule ccorres_return_CE, simp+)[1] 4601 apply (rule ccorres_return_C_errorE, simp+)[1] 4602 apply wp 4603 apply (rule ccorres_Cond_rhs) 4604 apply simp 4605 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeWriteRegisters_ccorres [where buffer=buffer]) 4606 apply (rule ccorres_return_CE, simp+)[1] 4607 apply (rule ccorres_return_C_errorE, simp+)[1] 4608 apply wp 4609 apply (rule ccorres_Cond_rhs) 4610 apply simp 4611 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeCopyRegisters_ccorres [where buffer=buffer]) 4612 apply (rule ccorres_return_CE, simp+)[1] 4613 apply (rule ccorres_return_C_errorE, simp+)[1] 4614 apply wp 4615 apply (rule ccorres_Cond_rhs) 4616 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr) 4617 apply (rule ccorres_rhs_assoc)+ 4618 apply (ctac add: setThreadState_ccorres) 4619 apply csymbr 4620 apply (simp add: performInvocation_def) 4621 apply (ctac add: invokeTCB_Suspend_ccorres) 4622 apply simp 4623 apply (rule ccorres_alternative2) 4624 apply (rule ccorres_return_CE, simp+)[1] 4625 apply (rule ccorres_return_C_errorE, simp+)[1] 4626 apply wp 4627 apply (vcg exspec=invokeTCB_Suspend_modifies) 4628 apply (wp sts_invs_minor') 4629 apply (vcg exspec=setThreadState_modifies) 4630 apply (rule ccorres_Cond_rhs) 4631 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr) 4632 apply (rule ccorres_rhs_assoc)+ 4633 apply (ctac add: setThreadState_ccorres) 4634 apply csymbr 4635 apply (simp add: performInvocation_def) 4636 apply (ctac add: invokeTCB_Resume_ccorres) 4637 apply simp 4638 apply (rule ccorres_alternative2) 4639 apply (rule ccorres_return_CE, simp+)[1] 4640 apply (rule ccorres_return_C_errorE, simp+)[1] 4641 apply wp 4642 apply (vcg exspec=invokeTCB_Resume_modifies) 4643 apply (wp sts_invs_minor') 4644 apply (vcg exspec=setThreadState_modifies) 4645 apply (rule ccorres_Cond_rhs) 4646 apply simp 4647 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeTCBConfigure_ccorres [where buffer=buffer]) 4648 apply (rule ccorres_return_CE, simp+)[1] 4649 apply (rule ccorres_return_C_errorE, simp+)[1] 4650 apply wp 4651 apply (rule ccorres_Cond_rhs) 4652 apply simp 4653 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetPriority_ccorres [where buffer=buffer]) 4654 apply (rule ccorres_return_CE, simp+)[1] 4655 apply (rule ccorres_return_C_errorE, simp+)[1] 4656 apply wp 4657 apply (rule ccorres_Cond_rhs) 4658 apply simp 4659 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetMCPriority_ccorres [where buffer=buffer]) 4660 apply (rule ccorres_return_CE, simp+)[1] 4661 apply (rule ccorres_return_C_errorE, simp+)[1] 4662 apply wp 4663 apply (rule ccorres_Cond_rhs) 4664 apply simp 4665 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetSchedParams_ccorres [where buffer=buffer]) 4666 apply (rule ccorres_return_CE, simp+)[1] 4667 apply (rule ccorres_return_C_errorE, simp+)[1] 4668 apply wp 4669 apply (rule ccorres_Cond_rhs) 4670 apply simp 4671 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetIPCBuffer_ccorres [where buffer=buffer]) 4672 apply (rule ccorres_return_CE, simp+)[1] 4673 apply (rule ccorres_return_C_errorE, simp+)[1] 4674 apply wp 4675 apply (rule ccorres_Cond_rhs) 4676 apply simp 4677 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetSpace_ccorres [where buffer=buffer]) 4678 apply (rule ccorres_return_CE, simp+)[1] 4679 apply (rule ccorres_return_C_errorE, simp+)[1] 4680 apply wp 4681 apply (rule ccorres_Cond_rhs) 4682 apply simp 4683 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeBindNotification_ccorres) 4684 apply (rule ccorres_return_CE, simp+)[1] 4685 apply (rule ccorres_return_C_errorE, simp+)[1] 4686 apply wp 4687 apply (rule ccorres_Cond_rhs) 4688 apply simp 4689 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeUnbindNotification_ccorres) 4690 apply (rule ccorres_return_CE, simp+)[1] 4691 apply (rule ccorres_return_C_errorE, simp+)[1] 4692 apply wp 4693 apply (rule ccorres_Cond_rhs) 4694 apply simp 4695 apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetTLSBase_ccorres) 4696 apply (rule ccorres_return_CE, simp+)[1] 4697 apply (rule ccorres_return_C_errorE, simp+)[1] 4698 apply wp 4699 apply (rule ccorres_equals_throwError) 4700 apply (fastforce simp: throwError_bind invocationCatch_def 4701 split: invocation_label.split) 4702 apply (simp add: ccorres_cond_iffs 4703 cong: StateSpace.state.fold_congs globals.fold_congs) 4704 apply (rule syscall_error_throwError_ccorres_n) 4705 apply (simp add: syscall_error_to_H_cases) 4706 apply (clarsimp simp: cintr_def intr_and_se_rel_def 4707 exception_defs rf_sr_ksCurThread 4708 Collect_const_mem) 4709 apply (rule conjI) 4710 apply (auto simp: ct_in_state'_def isCap_simps valid_tcb_state'_def 4711 elim!: pred_tcb'_weakenE 4712 dest!: st_tcb_at_idle_thread')[1] 4713 apply (simp split: sum.split add: cintr_def intr_and_se_rel_def 4714 exception_defs syscall_error_rel_def) 4715 apply (simp add: "StrictC'_thread_state_defs" mask_eq_iff_w2p word_size 4716 cap_get_tag_isCap) 4717 apply (simp add: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) 4718 apply clarsimp 4719 done 4720 4721end 4722end 4723