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