1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11 12theory CSpace_C 13imports CSpaceAcc_C Machine_C 14begin 15 16context kernel_m 17begin 18 19lemma maskCapRights_cap_cases: 20 "return (maskCapRights R c) = 21 (case c of 22 ArchObjectCap ac \<Rightarrow> return (Arch.maskCapRights R ac) 23 | EndpointCap _ _ _ _ _ \<Rightarrow> 24 return (capEPCanGrant_update 25 (\<lambda>_. capEPCanGrant c \<and> capAllowGrant R) 26 (capEPCanReceive_update 27 (\<lambda>_. capEPCanReceive c \<and> capAllowRead R) 28 (capEPCanSend_update 29 (\<lambda>_. capEPCanSend c \<and> capAllowWrite R) c))) 30 | NotificationCap _ _ _ _ \<Rightarrow> 31 return (capNtfnCanReceive_update 32 (\<lambda>_. capNtfnCanReceive c \<and> capAllowRead R) 33 (capNtfnCanSend_update 34 (\<lambda>_. capNtfnCanSend c \<and> capAllowWrite R) c)) 35 | _ \<Rightarrow> return c)" 36 apply (simp add: maskCapRights_def Let_def split del: if_split) 37 apply (cases c; simp add: isCap_simps split del: if_split) 38 done 39 40 41lemma imp_ignore: "B \<Longrightarrow> A \<longrightarrow> B" by blast 42 43(* FIXME x64: ucast? see how it goes *) 44lemma wordFromVMRights_spec: 45 "\<forall>s. \<Gamma> \<turnstile> {s} Call wordFromVMRights_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>vm_rights\<rbrace>" 46 by vcg simp? 47 48(* FIXME x64: ucast? see how it goes *) 49lemma vmRightsFromWord_spec: 50 "\<forall>s. \<Gamma> \<turnstile> {s} Call vmRightsFromWord_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>w\<rbrace>" 51 by vcg simp? 52 53lemmas vmrights_defs = 54 Kernel_C.VMReadOnly_def 55 Kernel_C.VMKernelOnly_def 56 Kernel_C.VMReadWrite_def 57 58lemma maskVMRights_spec: 59 "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> 60 \<lbrace> \<acute>vm_rights && mask 2 = \<acute>vm_rights \<rbrace>) 61 Call maskVMRights_'proc 62 \<lbrace> vmrights_to_H \<acute>ret__unsigned_long = 63 maskVMRights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) (cap_rights_to_H (seL4_CapRights_lift \<^bsup>s\<^esup>cap_rights_mask)) \<and> 64 \<acute>ret__unsigned_long && mask 2 = \<acute>ret__unsigned_long \<and> 65 \<acute>ret__unsigned_long \<noteq> 0 \<rbrace>" 66 apply vcg 67 apply clarsimp 68 apply (rule conjI) 69 apply ((auto simp: vmrights_to_H_def maskVMRights_def vmrights_defs 70 cap_rights_to_H_def to_bool_def 71 split: bool.split 72 | simp add: mask_def 73 | word_bitwise)+)[1] 74 apply clarsimp 75 apply (subgoal_tac "vm_rights = 0 \<or> vm_rights = 1 \<or> vm_rights = 2 \<or> vm_rights = 3") 76 apply (auto simp: vmrights_to_H_def maskVMRights_def vmrights_defs 77 cap_rights_to_H_def seL4_CapRights_lift_def 78 to_bool_def mask_def 79 split: bool.splits)[1] 80 apply (subst(asm) mask_eq_iff_w2p) 81 apply (simp add: word_size) 82 apply (rule ccontr, clarsimp) 83 apply (drule inc_le, simp, drule(1) order_le_neq_trans [OF _ not_sym])+ 84 apply (drule inc_le, simp) 85 done 86 87lemma frame_cap_rights [simp]: 88 "cap_get_tag cap = scast cap_frame_cap 89 \<Longrightarrow> cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) && mask 2 = 90 cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap)" 91 apply (simp add: cap_frame_cap_lift_def) 92 by (simp add: cap_lift_def cap_tag_defs mask_def word_bw_assocs) 93 94lemma Arch_maskCapRights_ccorres [corres]: 95 "ccorres ccap_relation ret__struct_cap_C_' 96 \<top> 97 (UNIV \<inter> \<lbrace>ccap_relation (ArchObjectCap arch_cap) \<acute>cap\<rbrace> \<inter> 98 \<lbrace>ccap_rights_relation R \<acute>cap_rights_mask\<rbrace>) 99 [] 100 (return (Arch.maskCapRights R arch_cap)) 101 (Call Arch_maskCapRights_'proc)" 102 apply (cinit' lift: cap_' cap_rights_mask_') 103 apply csymbr 104 apply (unfold X64_H.maskCapRights_def) 105 apply (simp only: Let_def) 106 apply (case_tac "cap_get_tag cap = scast cap_frame_cap") 107 apply (clarsimp simp add: ccorres_cond_iffs cap_get_tag_isCap isCap_simps split del: if_splits) 108 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 109 apply (rule allI, rule conseqPre, vcg) 110 apply (clarsimp simp: cap_get_tag_isCap isCap_simps) 111 apply (clarsimp simp: return_def) 112 apply (unfold ccap_relation_def)[1] 113 apply (simp add: cap_frame_cap_lift [THEN iffD1]) 114 apply (clarsimp simp: cap_to_H_def) 115 apply (simp add: map_option_case split: option.splits) 116 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) 117 apply (clarsimp simp: cap_frame_cap_lift_def) 118 apply (clarsimp simp: ccap_rights_relation_def cap_frame_cap_lift c_valid_cap_def 119 cl_valid_cap_def mask_eq_iff word_less_alt 120 split: option.splits cap_CL.splits) 121 apply (clarsimp simp: cap_frame_cap_lift_def) 122 apply (clarsimp simp: ccap_rights_relation_def c_valid_cap_def cap_frame_cap_lift 123 cl_valid_cap_def mask_eq_iff word_less_alt) 124 apply (clarsimp simp add: cap_get_tag_isCap isCap_simps simp del: not_ex) 125 apply (rule conjI, clarsimp) 126 apply (simp add: ccorres_cond_iffs) 127 apply (rule ccorres_from_vcg_throws) 128 apply (rule allI, rule conseqPre, vcg) 129 apply (clarsimp simp add: return_def simp del: not_ex) 130 apply (cases arch_cap) 131 by (fastforce simp add: cap_get_tag_isCap isCap_simps simp del: not_ex omgwtfbbq)+ 132 133lemma to_bool_mask_to_bool_bf: 134 "to_bool (x && mask (Suc 0)) = to_bool_bf (x::machine_word)" 135 apply (simp add: to_bool_bf_def to_bool_def) 136 apply (rule iffI) 137 prefer 2 138 apply simp 139 apply (subgoal_tac "x && mask (Suc 0) < 2^(Suc 0)") 140 apply simp 141 apply (drule word_less_cases [where y=2]) 142 apply auto[1] 143 apply (rule and_mask_less') 144 apply simp 145 done 146 147lemma to_bool_cap_rights_bf: 148 "to_bool (capAllowRead_CL (seL4_CapRights_lift R)) = 149 to_bool_bf (capAllowRead_CL (seL4_CapRights_lift R))" 150 "to_bool (capAllowWrite_CL (seL4_CapRights_lift R)) = 151 to_bool_bf (capAllowWrite_CL (seL4_CapRights_lift R))" 152 "to_bool (capAllowGrant_CL (seL4_CapRights_lift R)) = 153 to_bool_bf (capAllowGrant_CL (seL4_CapRights_lift R))" 154 by (subst to_bool_bf_to_bool_mask, 155 simp add: seL4_CapRights_lift_def mask_def word_bw_assocs, simp)+ 156 157lemma to_bool_ntfn_cap_bf: 158 "cap_lift c = Some (Cap_notification_cap cap) \<Longrightarrow> 159 to_bool (capNtfnCanSend_CL cap) = to_bool_bf (capNtfnCanSend_CL cap) \<and> 160 to_bool (capNtfnCanReceive_CL cap) = to_bool_bf (capNtfnCanReceive_CL cap)" 161 apply (simp add:cap_lift_def Let_def split: if_split_asm) 162 apply (subst to_bool_bf_to_bool_mask, 163 clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+ 164 apply simp 165 done 166 167lemma to_bool_ep_cap_bf: 168 "cap_lift c = Some (Cap_endpoint_cap cap) \<Longrightarrow> 169 to_bool (capCanSend_CL cap) = to_bool_bf (capCanSend_CL cap) \<and> 170 to_bool (capCanReceive_CL cap) = to_bool_bf (capCanReceive_CL cap) \<and> 171 to_bool (capCanGrant_CL cap) = to_bool_bf (capCanGrant_CL cap)" 172 apply (simp add:cap_lift_def Let_def split: if_split_asm) 173 apply (subst to_bool_bf_to_bool_mask, 174 clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+ 175 apply simp 176 done 177 178lemma isArchCap_spec: 179 "\<forall>s. \<Gamma>\<turnstile> {s} Call isArchCap_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag (cap_' s)))\<rbrace>" 180 apply vcg 181 apply (clarsimp simp: from_bool_def isArchCap_tag_def bool.split) 182 apply (clarsimp simp: word_mod_2p_is_mask[where n=1, simplified] mask_def) 183 apply word_bitwise 184 done 185 186lemma maskCapRights_ccorres [corres]: 187 "ccorres ccap_relation ret__struct_cap_C_' 188 \<top> 189 (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>ccap_rights_relation R \<acute>cap_rights\<rbrace>) 190 [] 191 (return (RetypeDecls_H.maskCapRights R cap)) (Call maskCapRights_'proc)" 192 apply (cinit' lift: cap_' cap_rights_') 193 apply csymbr 194 apply (simp add: maskCapRights_cap_cases cap_get_tag_isCap del: Collect_const) 195 apply wpc 196 apply (simp add: Collect_const_mem from_bool_def) 197 apply csymbr 198 apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) 199 apply (simp add: ccorres_cond_iffs) 200 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 201 apply (rule allI) 202 apply (rule conseqPre) 203 apply vcg 204 apply clarsimp 205 apply (simp add: cap_get_tag_isCap isCap_simps return_def) 206 apply (simp add: Collect_const_mem from_bool_def) 207 apply csymbr 208 apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) 209 apply (simp add: ccorres_cond_iffs) 210 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 211 apply (rule allI) 212 apply (rule conseqPre) 213 apply vcg 214 apply (clarsimp simp: return_def) 215 apply (simp add: Collect_const_mem from_bool_def) 216 apply csymbr 217 apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) 218 apply (simp add: ccorres_cond_iffs) 219 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 220 apply (rule allI) 221 apply (rule conseqPre) 222 apply vcg 223 apply clarsimp 224 apply (simp add: cap_get_tag_isCap isCap_simps return_def) 225 apply (rule imp_ignore) 226 apply (rule imp_ignore) 227 apply (rule imp_ignore) 228 apply (rule imp_ignore) 229 apply (rule imp_ignore) 230 apply clarsimp 231 apply (unfold ccap_relation_def)[1] 232 apply (simp add: cap_notification_cap_lift [THEN iffD1]) 233 apply (clarsimp simp: cap_to_H_def) 234 apply (simp add: map_option_case split: option.splits) 235 apply (clarsimp simp add: cap_to_H_def Let_def 236 split: cap_CL.splits if_split_asm) 237 apply (simp add: cap_notification_cap_lift_def) 238 apply (simp add: ccap_rights_relation_def cap_rights_to_H_def 239 to_bool_ntfn_cap_bf 240 to_bool_mask_to_bool_bf to_bool_cap_rights_bf) 241 apply (simp add: Collect_const_mem from_bool_def) 242 apply csymbr 243 apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs) 244 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 245 apply (rule allI) 246 apply (rule conseqPre) 247 apply vcg 248 apply (clarsimp simp: cap_get_tag_isCap isCap_simps return_def) 249 apply (simp add: Collect_const_mem from_bool_def) 250 apply csymbr 251 apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs) 252 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 253 apply (rule allI) 254 apply (rule conseqPre) 255 apply vcg 256 apply clarsimp 257 apply (simp add: cap_get_tag_isCap isCap_simps return_def) 258 apply (rule imp_ignore) 259 apply (rule imp_ignore) 260 apply (rule imp_ignore) 261 apply (rule imp_ignore) 262 apply (rule imp_ignore) 263 apply (rule imp_ignore) 264 apply (rule imp_ignore) 265 apply (rule imp_ignore) 266 apply clarsimp 267 apply (unfold ccap_relation_def)[1] 268 apply (simp add: cap_endpoint_cap_lift [THEN iffD1]) 269 apply (clarsimp simp: cap_to_H_def) 270 apply (simp add: map_option_case split: option.splits) 271 apply (clarsimp simp add: cap_to_H_def Let_def 272 split: cap_CL.splits if_split_asm) 273 apply (simp add: cap_endpoint_cap_lift_def) 274 apply (simp add: ccap_rights_relation_def cap_rights_to_H_def 275 to_bool_ep_cap_bf 276 to_bool_mask_to_bool_bf to_bool_cap_rights_bf) 277 apply (simp add: Collect_const_mem from_bool_def) 278 apply csymbr 279 apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) 280 apply (simp add: ccorres_cond_iffs) 281 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 282 apply (rule allI) 283 apply (rule conseqPre) 284 apply vcg 285 apply (clarsimp simp: return_def) 286 apply (simp add: Collect_const_mem from_bool_def) 287 apply csymbr 288 apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs) 289 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 290 apply (rule allI) 291 apply (rule conseqPre) 292 apply vcg 293 apply (clarsimp simp: cap_get_tag_isCap isCap_simps return_def) 294 apply (simp add: Collect_const_mem from_bool_def) 295 apply (subst bind_return [symmetric]) 296 apply (rule ccorres_split_throws) 297 apply ctac 298 apply (rule_tac P=\<top> and P'="\<lbrace>\<acute>ret__struct_cap_C = ret__struct_cap_C\<rbrace>" in ccorres_inst) 299 apply (rule ccorres_from_vcg_throws) 300 apply (clarsimp simp: return_def) 301 apply (rule conseqPre) 302 apply vcg 303 apply clarsimp 304 apply wp 305 apply vcg 306 apply vcg 307 apply (simp add: Collect_const_mem from_bool_def) 308 apply csymbr 309 apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) 310 apply (simp add: ccorres_cond_iffs) 311 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 312 apply (rule allI) 313 apply (rule conseqPre) 314 apply vcg 315 apply (clarsimp simp: return_def) 316 apply (simp add: Collect_const_mem from_bool_def) 317 apply csymbr 318 apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) 319 apply (simp add: ccorres_cond_iffs) 320 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 321 apply (rule allI) 322 apply (rule conseqPre) 323 apply vcg 324 apply (clarsimp simp: return_def) 325 apply (simp add: Collect_const_mem from_bool_def) 326 apply csymbr 327 apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) 328 apply (simp add: ccorres_cond_iffs) 329 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 330 apply (rule allI) 331 apply (rule conseqPre) 332 apply vcg 333 apply clarsimp 334 apply (simp add: cap_get_tag_isCap isCap_simps return_def) 335 apply (simp add: Collect_const_mem from_bool_def) 336 apply csymbr 337 apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) 338 apply (simp add: ccorres_cond_iffs) 339 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 340 apply (rule allI) 341 apply (rule conseqPre) 342 apply vcg 343 apply (clarsimp simp: return_def) 344 apply clarsimp 345 done 346 347abbreviation 348 "lookupCap_xf \<equiv> liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_'" 349 350lemma ccorres_return_cte_cteCap [corres]: 351 fixes ptr' :: "cstate \<Rightarrow> cte_C ptr" 352 assumes r1: "\<And>s s' g. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu g s') \<in> rf_sr" 353 and xf_xfu: "\<And>s g. xf (xfu g s) = g s" 354 shows "ccorres ccap_relation xf 355 (\<lambda>s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr} hs 356 (return (cteCap cte)) 357 (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) 358 (Ptr &(ptr' s \<rightarrow>[''cap_C'']))) s))" 359 apply (rule ccorres_return) 360 apply (rule conseqPre) 361 apply vcg 362 apply (clarsimp simp: xf_xfu ccap_relation_def) 363 apply rule 364 apply (erule r1) 365 apply (drule (1) rf_sr_ctes_of_clift) 366 apply (clarsimp simp: typ_heap_simps) 367 apply (simp add: c_valid_cte_def) 368done 369 370 371lemma ccorres_return_cte_mdbnode [corres]: 372 fixes ptr' :: "cstate \<Rightarrow> cte_C ptr" 373 assumes r1: "\<And>s s' g. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu g s') \<in> rf_sr" 374 and xf_xfu: "\<And>s g. xf (xfu g s) = g s" 375 shows "ccorres cmdbnode_relation xf 376 (\<lambda>s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr} hs 377 (return (cteMDBNode cte)) 378 (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) 379 (Ptr &(ptr' s \<rightarrow>[''cteMDBNode_C'']))) s))" 380 apply (rule ccorres_from_vcg) 381 apply (rule allI, rule conseqPre, vcg) 382 apply (clarsimp simp add: return_def xf_xfu) 383 apply (frule (1) rf_sr_ctes_of_clift) 384 apply (clarsimp simp: typ_heap_simps) 385 apply (erule r1) 386 done 387 388 389(* FIXME: MOVE *) 390lemma heap_update_field_ext: 391 "\<lbrakk>field_ti TYPE('a :: packed_type) f = Some t; c_guard p; 392 export_uinfo t = export_uinfo (typ_info_t TYPE('b :: packed_type))\<rbrakk> 393 \<Longrightarrow> heap_update (Ptr &(p\<rightarrow>f) :: 'b ptr) = 394 (\<lambda>v hp. heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp)" 395 apply (rule ext, rule ext) 396 apply (erule (2) heap_update_field) 397 done 398 399lemma ccorres_updateCap [corres]: 400 fixes ptr :: "cstate \<Rightarrow> cte_C ptr" and val :: "cstate \<Rightarrow> cap_C" 401 shows "ccorres dc xfdc \<top> 402 ({s. ccap_relation cap (val s)} \<inter> {s. ptr s = Ptr dest}) hs 403 (updateCap dest cap) 404 (Basic 405 (\<lambda>s. globals_update 406 (t_hrs_'_update 407 (hrs_mem_update (heap_update (Ptr &(ptr s\<rightarrow>[''cap_C''])) (val s)))) s))" 408 unfolding updateCap_def 409 apply (cinitlift ptr) 410 apply (erule ssubst) 411 apply (rule ccorres_guard_imp2) 412 apply (rule ccorres_pre_getCTE) 413 apply (rule_tac P = "\<lambda>s. ctes_of s dest = Some rva" in 414 ccorres_from_vcg [where P' = "{s. ccap_relation cap (val s)}"]) 415 apply (rule allI) 416 apply (rule conseqPre) 417 apply vcg 418 apply clarsimp 419 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) 420 apply (erule bexI [rotated]) 421 apply (clarsimp simp: cte_wp_at_ctes_of) 422 apply (frule (1) rf_sr_ctes_of_clift) 423 apply (clarsimp simp add: rf_sr_def cstate_relation_def 424 Let_def cpspace_relation_def 425 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) 426 apply (simp add:typ_heap_simps) 427 apply (rule conjI) 428 apply (erule (3) cpspace_cte_relation_upd_capI) 429 apply (frule_tac f="ksPSpace" in arg_cong) 430 apply (erule_tac t = s' in ssubst) 431 apply simp 432 apply (simp add: heap_to_user_data_def heap_to_device_data_def) 433 apply (rule conjI) 434 apply (erule (1) setCTE_tcb_case) 435 by (auto simp: carch_state_relation_def cmachine_state_relation_def 436 global_ioport_bitmap_heap_update_tag_disj_simps 437 fpu_null_state_heap_update_tag_disj_simps) 438 439lemma ccorres_updateMDB_const [corres]: 440 fixes ptr :: "cstate \<Rightarrow> cte_C ptr" and val :: "cstate \<Rightarrow> mdb_node_C" 441 shows "ccorres dc xfdc (\<lambda>_. dest \<noteq> 0) 442 ({s. cmdbnode_relation m (val s)} \<inter> {s. ptr s = Ptr dest}) hs 443 (updateMDB dest (const m)) 444 (Basic 445 (\<lambda>s. globals_update 446 (t_hrs_'_update 447 (hrs_mem_update (heap_update (Ptr &(ptr s\<rightarrow>[''cteMDBNode_C''])) (val s)))) s))" 448 unfolding updateMDB_def 449 apply (cinitlift ptr) 450 apply (erule ssubst) 451 apply (rule ccorres_gen_asm [where G = \<top>, simplified]) 452 apply (simp only: Let_def) 453 apply simp 454 apply (rule ccorres_guard_imp2) 455 apply (rule ccorres_pre_getCTE) 456 apply (rule_tac P = "\<lambda>s. ctes_of s dest = Some cte" in ccorres_from_vcg [where P' = "{s. cmdbnode_relation m (val s)}"]) 457 apply (rule allI) 458 apply (rule conseqPre) 459 apply vcg 460 apply clarsimp 461 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption ) 462 apply (erule bexI [rotated]) 463 apply (frule (1) rf_sr_ctes_of_clift) 464 apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps 465 Let_def cpspace_relation_def 466 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) 467 apply (rule conjI) 468 apply (erule (3) cspace_cte_relation_upd_mdbI) 469 apply (erule_tac t = s' in ssubst) 470 apply (simp add: heap_to_user_data_def) 471 apply (rule conjI) 472 apply (erule (1) setCTE_tcb_case) 473 by (auto simp: carch_state_relation_def cmachine_state_relation_def 474 global_ioport_bitmap_heap_update_tag_disj_simps 475 fpu_null_state_heap_update_tag_disj_simps) 476 477(* 64 == badgeBits *) 478lemma cap_lift_capNtfnBadge_mask_eq: 479 "cap_lift cap = Some (Cap_notification_cap ec) 480 \<Longrightarrow> capNtfnBadge_CL ec && mask 64 = capNtfnBadge_CL ec" 481 unfolding cap_lift_def 482 by (fastforce simp: Let_def mask_def word_bw_assocs split: if_split_asm) 483 484lemma cap_lift_capEPBadge_mask_eq: 485 "cap_lift cap = Some (Cap_endpoint_cap ec) 486 \<Longrightarrow> capEPBadge_CL ec && mask 64 = capEPBadge_CL ec" 487 unfolding cap_lift_def 488 by (fastforce simp: Let_def mask_def word_bw_assocs split: if_split_asm) 489 490lemma Arch_isCapRevocable_spec: 491 "\<forall>s. \<Gamma>\<turnstile> {\<sigma>. s = \<sigma> \<and> True} 492 Call Arch_isCapRevocable_'proc 493 {t. \<forall>c c'. ccap_relation c (derivedCap_' s) \<and> ccap_relation c' (srcCap_' s) 494 \<longrightarrow> ret__unsigned_long_' t = from_bool (Arch.isCapRevocable c c')}" 495 apply vcg 496 by (auto simp: false_def from_bool_def X64_H.isCapRevocable_def 497 cap_get_tag_isCap_unfolded_H_cap cap_tag_defs isCap_simps 498 cap_get_tag_isCap[unfolded cap_io_port_control_cap_def, simplified] 499 split: capability.splits arch_capability.splits bool.splits) 500 501lemmas isCapRevocable_simps[simp] = Retype_H.isCapRevocable_def[split_simps capability.split] 502 503context begin (* revokable_ccorres *) 504 505private method revokable'_hammer = solves \<open>( 506 simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def, 507 rule ccorres_guard_imp, 508 rule ccorres_return_C; clarsimp)\<close> 509 510lemma revokable_ccorres: 511 "ccorres (\<lambda>a c. from_bool a = c) ret__unsigned_long_' 512 (\<lambda>_. capMasterCap cap = capMasterCap parent \<or> is_simple_cap' cap) 513 (UNIV \<inter> {s. ccap_relation cap (derivedCap_' s)} \<inter> {s. ccap_relation parent (srcCap_' s)}) hs 514 (return (isCapRevocable cap parent)) 515 (Call isCapRevocable_'proc)" 516 apply (rule ccorres_gen_asm[where G=\<top>, simplified]) 517 apply (cinit' lift: derivedCap_' srcCap_') 518 \<comment> \<open>Clear up Arch cap case\<close> 519 apply csymbr 520 apply (clarsimp simp: cap_get_tag_isCap split del: if_splits simp del: Collect_const) 521 apply (rule ccorres_Cond_rhs_Seq) 522 apply (rule ccorres_rhs_assoc) 523 apply (clarsimp simp: isCap_simps) 524 apply csymbr 525 apply (drule spec, drule spec, drule mp, fastforce) 526 apply ccorres_rewrite 527 apply (drule sym, simp only:) 528 apply (rule ccorres_return_C, clarsimp+) 529 apply csymbr 530 apply (rule_tac P'=UNIV and P=\<top> in ccorres_inst) 531 apply (cases cap) 532 \<comment> \<open>Uninteresting caps\<close> 533 apply revokable'_hammer+ 534 \<comment> \<open>NotificationCap\<close> 535 apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def) 536 apply (rule ccorres_guard_imp, (rule ccorres_rhs_assoc)+, csymbr, csymbr) 537 apply (rule ccorres_return_C, clarsimp+) 538 apply (frule_tac cap'1=srcCap in cap_get_tag_NotificationCap[THEN iffD1]) 539 apply (clarsimp simp: cap_get_tag_isCap isCap_simps is_simple_cap'_def) 540 apply (frule_tac cap'1=derivedCap in cap_get_tag_NotificationCap[THEN iffD1]) 541 apply (clarsimp simp: cap_get_tag_isCap isCap_simps) 542 apply (fastforce simp: cap_get_tag_isCap isCap_simps) 543 \<comment> \<open>IRQHandlerCap\<close> 544 apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def) 545 apply (rule ccorres_guard_imp, csymbr) 546 apply (rule ccorres_return_C, clarsimp+) 547 apply (fastforce simp: cap_get_tag_isCap isCap_simps) 548 \<comment> \<open>EndpointCap\<close> 549 apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def) 550 apply (rule ccorres_guard_imp, (rule ccorres_rhs_assoc)+, csymbr, csymbr) 551 apply (rule ccorres_return_C, clarsimp+) 552 apply (frule_tac cap'1=srcCap in cap_get_tag_EndpointCap[THEN iffD1]) 553 apply (clarsimp simp: cap_get_tag_isCap isCap_simps is_simple_cap'_def) 554 apply (frule_tac cap'1=derivedCap in cap_get_tag_EndpointCap[THEN iffD1]) 555 apply (clarsimp simp: cap_get_tag_isCap isCap_simps) 556 apply (fastforce simp: cap_get_tag_isCap isCap_simps) 557 \<comment> \<open>Other Caps\<close> 558 by (revokable'_hammer | fastforce simp: isCap_simps)+ 559 560end (* revokable_ccorres *) 561 562lemma cteInsert_ccorres_mdb_helper: 563 "\<lbrakk>cmdbnode_relation rva srcMDB; from_bool rvc = (newCapIsRevocable :: machine_word); srcSlot = Ptr src\<rbrakk> 564 \<Longrightarrow> ccorres cmdbnode_relation newMDB_' (K (is_aligned src 3)) 565 UNIV hs 566 (return 567 (mdbFirstBadged_update (\<lambda>_. rvc) 568 (mdbRevocable_update (\<lambda>_. rvc) 569 (mdbPrev_update (\<lambda>_. src) rva)))) 570 (\<acute>newMDB :== CALL mdb_node_set_mdbPrev(srcMDB, 571 ptr_val srcSlot);; 572 \<acute>newMDB :== CALL mdb_node_set_mdbRevocable(\<acute>newMDB, 573 newCapIsRevocable);; 574 \<acute>newMDB :== CALL mdb_node_set_mdbFirstBadged(\<acute>newMDB, 575 newCapIsRevocable))" 576 apply (rule ccorres_from_vcg) 577 apply (rule allI) 578 apply (rule conseqPre) 579 apply vcg 580 apply (clarsimp simp: return_def cmdbnode_relation_def mask_def) 581 done 582 583lemma ccorres_updateMDB_set_mdbNext [corres]: 584 "src=src' \<Longrightarrow> 585 ccorres dc xfdc ((\<lambda>_. src \<noteq> 0 \<and> is_aligned dest cteSizeBits \<and> canonical_address dest)) 586 ({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])} \<inter> 587 {s. v64_' s = dest}) [] 588 (updateMDB src (mdbNext_update (\<lambda>_. dest))) 589 (Call mdb_node_ptr_set_mdbNext_'proc)" 590 unfolding updateMDB_def 591 apply (hypsubst) 592 apply (rule ccorres_gen_asm [where G = \<top>, simplified]) 593 apply (simp only: Let_def) 594 apply simp 595 apply (rule ccorres_guard_imp2) 596 apply (rule ccorres_pre_getCTE 597 [where P = "\<lambda>cte s. ctes_of s src' = Some cte" 598 and P'= "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> 599 \<inter> \<lbrace>\<acute>v64 = dest\<rbrace>)"]) 600 apply (rule ccorres_from_spec_modifies_heap) 601 apply (rule mdb_node_ptr_set_mdbNext_spec) 602 apply (rule mdb_node_ptr_set_mdbNext_modifies) 603 apply simp 604 apply clarsimp 605 apply (rule rf_sr_cte_at_valid) 606 apply simp 607 apply (erule ctes_of_cte_at) 608 apply assumption 609 apply clarsimp 610 apply (frule (1) rf_sr_ctes_of_clift) 611 apply (clarsimp simp: typ_heap_simps) 612 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) 613 apply (erule bexI [rotated]) 614 apply (clarsimp simp: rf_sr_def cstate_relation_def 615 Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_user_data_def 616 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] 617 typ_heap_simps') 618 apply (rule conjI) 619 apply (erule (2) cspace_cte_relation_upd_mdbI) 620 apply (simp add: cmdbnode_relation_def) 621 apply (intro arg_cong[where f="\<lambda>f. mdbNext_update f mdb" for mdb] ext word_eqI) 622 apply (simp add: sign_extend_bitwise_if' neg_mask_bang word_size) 623 apply (match premises in C: "canonical_address _" and A: "is_aligned _ _" (multi) \<Rightarrow> 624 \<open>match premises in H[thin]: _ (multi) \<Rightarrow> \<open>insert C A\<close>\<close>) 625 apply (drule is_aligned_weaken[where y=2], simp add: objBits_defs) 626 apply (case_tac "n < 2"; case_tac "n \<le> 47"; 627 clarsimp simp: linorder_not_less linorder_not_le is_aligned_nth[THEN iffD1]) 628 apply (fastforce simp: word_size dest: canonical_address_high_bits) 629 apply (erule_tac t = s'a in ssubst) 630 apply simp 631 apply (rule conjI) 632 apply (erule (1) setCTE_tcb_case) 633 by (auto simp: carch_state_relation_def cmachine_state_relation_def 634 global_ioport_bitmap_heap_update_tag_disj_simps 635 fpu_null_state_heap_update_tag_disj_simps) 636 637lemma ccorres_updateMDB_set_mdbPrev [corres]: 638 "src=src' \<Longrightarrow> 639 ccorres dc xfdc (\<lambda>_. src \<noteq> 0 \<and> is_aligned dest cteSizeBits) 640 ({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])} \<inter> 641 {s. v64_' s = dest}) [] 642 (updateMDB src (mdbPrev_update (\<lambda>_. dest))) 643 (Call mdb_node_ptr_set_mdbPrev_'proc)" 644 unfolding updateMDB_def 645 apply (hypsubst) 646 apply (rule ccorres_gen_asm [where G = \<top>, simplified]) 647 apply (simp only: Let_def) 648 apply simp 649 apply (rule ccorres_guard_imp2) 650 apply (rule ccorres_pre_getCTE 651 [where P = "\<lambda>cte s. ctes_of s src' = Some cte" 652 and P' = "\<lambda>_. (\<lbrace>\<acute>mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\<rightarrow>[''cteMDBNode_C''])\<rbrace> 653 \<inter> \<lbrace>\<acute>v64 = dest\<rbrace>)"]) 654 apply (rule ccorres_from_spec_modifies_heap) 655 apply (rule mdb_node_ptr_set_mdbPrev_spec) 656 apply (rule mdb_node_ptr_set_mdbPrev_modifies) 657 apply simp 658 apply clarsimp 659 apply (rule rf_sr_cte_at_valid) 660 apply simp 661 apply (erule ctes_of_cte_at) 662 apply assumption 663 apply (clarsimp simp: cte_wp_at_ctes_of) 664 apply (frule (1) rf_sr_ctes_of_clift) 665 apply (clarsimp simp: typ_heap_simps) 666 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) 667 apply (erule bexI[rotated]) 668 apply (clarsimp simp: rf_sr_def cstate_relation_def 669 Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_user_data_def 670 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] 671 typ_heap_simps') 672 apply (rule conjI) 673 apply (erule (2) cspace_cte_relation_upd_mdbI) 674 apply (simp add: cmdbnode_relation_def mask_def) 675 apply (erule_tac t = s'a in ssubst) 676 apply (simp add: carch_state_relation_def cmachine_state_relation_def 677 fpu_null_state_heap_update_tag_disj_simps 678 global_ioport_bitmap_heap_update_tag_disj_simps) 679 apply (erule (1) setCTE_tcb_case) 680 by clarsimp 681 682lemma ccorres_updateMDB_skip: 683 "ccorres dc xfdc (\<top> and (\<lambda>_. n = 0)) UNIV hs (updateMDB n f) SKIP" 684 unfolding updateMDB_def 685 apply (rule ccorres_gen_asm) 686 apply simp 687 apply (rule ccorres_return) 688 apply simp 689 apply vcg 690 done 691 692definition 693 "is_simple_cap_tag (tag :: machine_word) \<equiv> 694 tag \<noteq> scast cap_null_cap \<and> tag \<noteq> scast cap_irq_control_cap 695 \<and> tag \<noteq> scast cap_untyped_cap \<and> tag \<noteq> scast cap_reply_cap 696 \<and> tag \<noteq> scast cap_endpoint_cap \<and> tag \<noteq> scast cap_notification_cap 697 \<and> tag \<noteq> scast cap_thread_cap \<and> tag \<noteq> scast cap_cnode_cap 698 \<and> tag \<noteq> scast cap_zombie_cap \<and> tag \<noteq> scast cap_io_port_control_cap 699 \<and> tag \<noteq> scast cap_frame_cap" 700 701(* Useful: 702 apply (tactic {* let val _ = reset CtacImpl.trace_ceqv; val _ = reset CtacImpl.trace_ctac in all_tac end; *}) 703 *) 704declare word_neq_0_conv [simp del] 705 706schematic_goal ccap_relation_tag_Master: 707 "\<And>ccap. \<lbrakk> ccap_relation cap ccap \<rbrakk> 708 \<Longrightarrow> cap_get_tag ccap = 709 case_capability ?a ?b ?c ?d ?e ?f ?g 710 (case_arch_capability ?aa ?ab ?ac 711 ?ad ?ae ?af ?ag ?ah ?ai) ?h ?i ?j ?k 712 (capMasterCap cap)" 713 by (fastforce simp: ccap_relation_def map_option_Some_eq2 714 Let_def cap_lift_def cap_to_H_def 715 split: if_split_asm) 716 717lemma ccap_relation_is_derived_tag_equal: 718 "\<lbrakk> is_derived' cs p cap cap'; ccap_relation cap ccap; ccap_relation cap' ccap' \<rbrakk> 719 \<Longrightarrow> cap_get_tag ccap' = cap_get_tag ccap" 720 unfolding badge_derived'_def is_derived'_def 721 by (clarsimp simp: ccap_relation_tag_Master) 722 723lemma ccap_relation_Master_tags_eq: 724 "\<lbrakk> capMasterCap cap = capMasterCap cap'; ccap_relation cap ccap; ccap_relation cap' ccap' \<rbrakk> 725 \<Longrightarrow> cap_get_tag ccap' = cap_get_tag ccap" 726 by (clarsimp simp: ccap_relation_tag_Master) 727 728lemma is_simple_cap_get_tag_relation: 729 "ccap_relation cap ccap 730 \<Longrightarrow> is_simple_cap_tag (cap_get_tag ccap) = is_simple_cap' cap" 731 apply (simp add: is_simple_cap_tag_def is_simple_cap'_def 732 cap_get_tag_isCap) 733 apply (auto simp: isCap_simps) 734 done 735 736lemma setUntypedCapAsFull_cte_at_wp [wp]: 737 "\<lbrace> cte_at' x \<rbrace> setUntypedCapAsFull rvb cap src \<lbrace> \<lambda>_. cte_at' x \<rbrace>" 738 apply (clarsimp simp: setUntypedCapAsFull_def) 739 apply wp 740 done 741 742lemma valid_cap_untyped_inv: 743 "valid_cap' (UntypedCap d r n f) s \<Longrightarrow> 744 n \<ge> minUntypedSizeBits \<and> is_aligned (of_nat f :: machine_word) minUntypedSizeBits 745 \<and> n \<le> maxUntypedSizeBits \<and> n < word_bits" 746 apply (clarsimp simp:valid_cap'_def capAligned_def) 747 done 748 749lemma update_freeIndex': 750 assumes i'_align: "is_aligned (of_nat i' :: machine_word) minUntypedSizeBits" 751 assumes sz_bound: "sz \<le> maxUntypedSizeBits" 752 assumes i'_bound: "i'\<le> 2^sz" 753 shows "ccorres dc xfdc 754 (cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot) 755 (UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> 756 \<inter> \<lbrace>\<acute>v64 = of_nat i' >> minUntypedSizeBits\<rbrace>) [] 757 (updateCap srcSlot (capability.UntypedCap d p sz i')) 758 (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)" 759 proof - 760 note i'_bound_concrete 761 = order_trans[OF i'_bound power_increasing[OF sz_bound], simplified untypedBits_defs, simplified] 762 have i'_bound_word: "(of_nat i' :: machine_word) \<le> 2 ^ maxUntypedSizeBits" 763 using order_trans[OF i'_bound power_increasing[OF sz_bound], simplified] 764 by (simp add: word_of_nat_le untypedBits_defs) 765 show ?thesis 766 apply (cinit lift: cap_ptr_' v64_') 767 apply (rule ccorres_pre_getCTE) 768 apply (rule_tac P="\<lambda>s. ctes_of s srcSlot = Some rv \<and> (\<exists>i. cteCap rv = UntypedCap d p sz i)" 769 in ccorres_from_vcg[where P' = UNIV]) 770 apply (rule allI) 771 apply (rule conseqPre) 772 apply vcg 773 apply (clarsimp simp: guard_simps) 774 apply (intro conjI) 775 apply (frule (1) rf_sr_ctes_of_clift) 776 apply (clarsimp simp: typ_heap_simps) 777 apply (frule (1) rf_sr_ctes_of_clift) 778 apply (clarsimp simp: split_def) 779 apply (simp add: hrs_htd_def typ_heap_simps) 780 apply (rule fst_setCTE[OF ctes_of_cte_at], assumption) 781 apply (erule bexI[rotated], clarsimp) 782 apply (frule (1) rf_sr_ctes_of_clift) 783 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 784 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) 785 apply (simp add: cpspace_relation_def) 786 apply (clarsimp simp: typ_heap_simps') 787 apply (rule conjI) 788 apply (erule (2) cpspace_cte_relation_upd_capI) 789 apply (simp only: cte_lift_def split: option.splits; simp) 790 apply (simp add: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) 791 apply (case_tac y) 792 apply (simp add: cap_lift_def Let_def split: if_split_asm) 793 apply (case_tac cte', simp) 794 apply (clarsimp simp: ccap_relation_def cap_lift_def cap_get_tag_def cap_to_H_def) 795 apply (thin_tac _)+ 796 apply (simp add: mask_def to_bool_and_1 nth_shiftr word_ao_dist word_bool_alg.conj.assoc) 797 apply (rule inj_onD[OF word_unat.Abs_inj_on[where 'a=machine_word_len]], simp) 798 apply (cut_tac i'_align i'_bound_word) 799 apply (simp add: is_aligned_mask) 800 apply word_bitwise 801 subgoal by (simp add: word_size untypedBits_defs) 802 apply (cut_tac i'_bound_concrete) 803 subgoal by (simp add: unats_def) 804 subgoal by (simp add: word_unat.Rep[where 'a=machine_word_len, simplified]) 805 apply (erule_tac t = s' in ssubst) 806 apply clarsimp 807 apply (rule conjI) 808 subgoal by (erule (1) setCTE_tcb_case) 809 apply (clarsimp simp: carch_state_relation_def cmachine_state_relation_def 810 fpu_null_state_heap_update_tag_disj_simps 811 global_ioport_bitmap_heap_update_tag_disj_simps 812 packed_heap_update_collapse_hrs) 813 by (clarsimp simp: cte_wp_at_ctes_of) 814 qed 815 816lemma update_freeIndex: 817 "ccorres dc xfdc 818 (valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = UntypedCap d p sz i) srcSlot 819 and (\<lambda>_. is_aligned (of_nat i' :: machine_word) minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) 820 (UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> 821 \<inter> \<lbrace>\<acute>v64 = of_nat i' >> minUntypedSizeBits\<rbrace>) [] 822 (updateCap srcSlot (UntypedCap d p sz i')) 823 (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)" 824 apply (rule ccorres_assume_pre, rule ccorres_guard_imp) 825 apply (rule update_freeIndex'; clarsimp simp: cte_wp_at_ctes_of) 826 apply (case_tac cte; clarsimp dest!: ctes_of_valid_cap' simp: valid_cap'_def) 827 by auto 828 829(* FIXME: move *) 830lemma ccorres_cases: 831 assumes P: " P \<Longrightarrow> ccorres r xf G G' hs a b" 832 assumes notP: "\<not>P \<Longrightarrow> ccorres r xf H H' hs a b" 833 shows "ccorres r xf (\<lambda>s. (P \<longrightarrow> G s) \<and> (\<not>P \<longrightarrow> H s)) 834 ({s. P \<longrightarrow> s \<in> G'} \<inter> {s. \<not>P \<longrightarrow> s \<in> H'}) 835 hs a b" 836 apply (cases P, auto simp: P notP) 837 done 838 839lemma capBlockSize_CL_maxSize: 840 " \<lbrakk> cap_get_tag c = scast cap_untyped_cap \<rbrakk> \<Longrightarrow> capBlockSize_CL (cap_untyped_cap_lift c) < 0x40" 841 apply (clarsimp simp: cap_untyped_cap_lift_def) 842 apply (clarsimp simp: cap_lift_def) 843 apply (clarsimp simp: cap_untyped_cap_def cap_null_cap_def) 844 apply (rule word_and_less') 845 apply (simp add: mask_def) 846 done 847 848lemma setUntypedCapAsFull_ccorres [corres]: 849 notes if_split [split del] 850 notes Collect_const [simp del] 851 notes Collect_True [simp] Collect_False [simp] 852 shows 853 "ccorres dc xfdc 854 ((cte_wp_at' (\<lambda>c. (cteCap c) = srcCap) srcSlot) and valid_mdb' and pspace_aligned' and valid_objs' 855 and (K (isUntypedCap newCap \<longrightarrow> (minUntypedSizeBits \<le> capBlockSize newCap))) 856 and (K (isUntypedCap srcCap \<longrightarrow> (minUntypedSizeBits \<le> capBlockSize srcCap)))) 857 (UNIV \<inter> {s. ccap_relation srcCap (srcCap_' s)} 858 \<inter> {s. ccap_relation newCap (newCap_' s)} 859 \<inter> {s. srcSlot_' s = Ptr srcSlot}) 860 [] 861 (setUntypedCapAsFull srcCap newCap srcSlot) 862 (Call setUntypedCapAsFull_'proc)" 863 apply (cinit lift: srcCap_' newCap_' srcSlot_') 864 apply (rule ccorres_if_lhs) 865 apply (clarsimp simp: isCap_simps) 866 apply csymbr 867 apply csymbr 868 apply (simp add: if_then_0_else_1 if_then_1_else_0 cap_get_tag_isCap_unfolded_H_cap) 869 apply (rule ccorres_rhs_assoc)+ 870 apply csymbr 871 apply csymbr 872 apply (simp add: cap_get_tag_isCap_unfolded_H_cap ccorres_cond_univ_iff) 873 apply (rule ccorres_rhs_assoc)+ 874 apply csymbr 875 apply csymbr 876 apply csymbr 877 apply (frule cap_get_tag_to_H(9)) 878 apply (simp add: cap_get_tag_isCap_unfolded_H_cap) 879 apply (rotate_tac 1) 880 apply (frule cap_get_tag_to_H(9)) 881 apply (simp add: cap_get_tag_isCap_unfolded_H_cap) 882 apply simp 883 apply (rule ccorres_rhs_assoc)+ 884 apply csymbr 885 apply csymbr 886 apply csymbr 887 apply (simp add: ccorres_cond_univ_iff) 888 apply csymbr+ 889 apply (rule ccorres_move_c_guard_cte) 890 apply (rule ccorres_Guard) 891 apply (rule ccorres_call) 892 apply (rule update_freeIndex [unfolded dc_def]) 893 apply simp 894 apply simp 895 apply simp 896 apply clarsimp 897 apply (csymbr) 898 apply (csymbr) 899 apply (simp add: cap_get_tag_isCap) 900 apply (rule ccorres_Cond_rhs_Seq) 901 apply (rule ccorres_rhs_assoc)+ 902 apply csymbr 903 apply csymbr 904 apply (simp add: cap_get_tag_isCap) 905 apply (rule ccorres_Cond_rhs) 906 apply (rule ccorres_rhs_assoc)+ 907 apply csymbr 908 apply csymbr 909 apply csymbr 910 apply (rule ccorres_cases [where P="capPtr srcCap = capPtr newCap"]) 911 apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm) 912 apply (rule ccorres_rhs_assoc)+ 913 apply csymbr 914 apply csymbr 915 apply csymbr 916 apply (clarsimp simp: cap_get_tag_to_H cap_get_tag_UntypedCap split: if_split_asm) 917 apply (rule ccorres_cond_false) 918 apply (rule ccorres_return_Skip [unfolded dc_def]) 919 apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm) 920 apply (rule ccorres_cond_false) 921 apply (rule ccorres_return_Skip [unfolded dc_def]) 922 apply (rule ccorres_return_Skip [unfolded dc_def]) 923 apply clarsimp 924 apply (rule ccorres_cond_false) 925 apply (rule ccorres_return_Skip [unfolded dc_def]) 926 apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap) 927 apply (frule(1) cte_wp_at_valid_objs_valid_cap') 928 apply (clarsimp simp: untypedBits_defs) 929 apply (intro conjI impI allI) 930 apply (erule cte_wp_at_weakenE') 931 apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm) 932 apply clarsimp 933 apply (drule valid_cap_untyped_inv,clarsimp simp:max_free_index_def) 934 apply (rule is_aligned_weaken) 935 apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) 936 apply assumption 937 apply (clarsimp simp: max_free_index_def shiftL_nat valid_cap'_def capAligned_def) 938 apply (simp add:power_minus_is_div unat_sub word_le_nat_alt t2p_shiftr) 939 apply clarsimp 940 apply (erule cte_wp_at_weakenE', simp) 941 apply clarsimp 942 apply (drule valid_cap_untyped_inv) 943 apply (clarsimp simp: max_free_index_def t2p_shiftr unat_sub word_le_nat_alt word_bits_def) 944 apply (rule word_less_imp_diff_less) 945 apply (subst (asm) eq_commute, fastforce simp: unat_sub word_le_nat_alt) 946 apply (rule capBlockSize_CL_maxSize) 947 apply (clarsimp simp: cap_get_tag_UntypedCap) 948 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap) 949 done 950 951lemma ccte_lift: 952 "\<lbrakk>(s, s') \<in> rf_sr; cslift s' (cte_Ptr p) = Some cte'; 953 cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> 954 \<Longrightarrow> ctes_of s p = Some (cte_to_H (the (cte_lift cte')))" 955 apply (clarsimp simp:rf_sr_def cstate_relation_def Let_def cpspace_relation_def) 956 apply (drule(1) cmap_relation_cs_atD) 957 apply simp 958 apply (clarsimp simp:ccte_relation_def) 959 done 960 961lemma cmdb_node_relation_mdbNext: 962 "cmdbnode_relation n n' 963 \<Longrightarrow> mdbNext_CL (mdb_node_lift n') = mdbNext n" 964 by (simp add:cmdbnode_relation_def) 965 966lemma cslift_ptr_safe: 967 "cslift x ptr = Some a 968 \<Longrightarrow> ptr_safe ptr (hrs_htd (t_hrs_' (globals x)))" 969 apply (rule_tac h = "fst (t_hrs_' (globals x))" 970 in lift_t_ptr_safe[where g = c_guard]) 971 apply (fastforce simp add:typ_heap_simps hrs_htd_def) 972 done 973 974lemma ccorres_move_ptr_safe: 975 "ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a c \<Longrightarrow> 976 ccorres_underlying rf_sr \<Gamma> r xf arrel axf 977 (A and K (dest = cte_Ptr (ptr_val dest)) and cte_wp_at' (\<lambda>_. True) (ptr_val dest)) 978 (C' \<inter> \<lbrace>True\<rbrace>) hs a (Guard MemorySafety \<lbrace>ptr_safe (dest) (hrs_htd \<acute>t_hrs) \<rbrace> c)" 979 apply (rule ccorres_guard_imp2) 980 apply (rule ccorres_Guard) 981 apply simp 982 apply (clarsimp simp:cte_wp_at_ctes_of) 983 apply (drule(1) rf_sr_ctes_of_clift) 984 apply (case_tac dest) 985 apply (clarsimp simp:ptr_coerce_def) 986 apply (erule cslift_ptr_safe) 987 done 988 989lemma ccorres_move_ptr_safe_Seq: 990 "ccorres_underlying rf_sr \<Gamma> r xf arrel axf A C' hs a (c;;d) \<Longrightarrow> 991 ccorres_underlying rf_sr \<Gamma> r xf arrel axf 992 (A and cte_wp_at' (\<lambda>_. True) (ptr_val dest) and K (dest = cte_Ptr (ptr_val dest))) 993 (C' \<inter> \<lbrace>True\<rbrace>) hs a 994 (Guard MemorySafety \<lbrace>ptr_safe (dest) (hrs_htd \<acute>t_hrs) \<rbrace> c;;d)" 995 apply (rule ccorres_guard_imp2) 996 apply (rule ccorres_Guard_Seq) 997 apply simp 998 apply (clarsimp simp:cte_wp_at_ctes_of) 999 apply (drule(1) rf_sr_ctes_of_clift) 1000 apply clarsimp 1001 apply (erule cslift_ptr_safe) 1002 done 1003 1004lemmas ccorres_move_guard_ptr_safe = ccorres_move_ptr_safe_Seq ccorres_move_ptr_safe 1005 1006lemma cteInsert_ccorres: 1007 "ccorres dc xfdc 1008 (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> is_simple_cap' cap) src 1009 and valid_mdb' and valid_objs' and pspace_aligned' and pspace_canonical' 1010 and (valid_cap' cap)) 1011 (UNIV \<inter> {s. destSlot_' s = Ptr dest} 1012 \<inter> {s. srcSlot_' s = Ptr src} 1013 \<inter> {s. ccap_relation cap (newCap_' s)}) [] 1014 (cteInsert cap src dest) 1015 (Call cteInsert_'proc)" 1016 supply ctes_of_aligned_bits[simp] 1017 apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' 1018 simp del: return_bind simp add: Collect_const) 1019 apply (rule ccorres_move_c_guard_cte) 1020 apply (ctac pre: ccorres_pre_getCTE) 1021 apply (rule ccorres_move_c_guard_cte) 1022 apply (ctac pre: ccorres_pre_getCTE) 1023 apply (ctac (no_vcg) add: revokable_ccorres) 1024 apply (ctac (c_lines 3) add: cteInsert_ccorres_mdb_helper) 1025 apply (simp del: Collect_const) 1026 apply (rule ccorres_pre_getCTE ccorres_assert)+ 1027 apply (ctac add: setUntypedCapAsFull_ccorres) 1028 apply (rule ccorres_move_c_guard_cte) 1029 apply (ctac) 1030 apply (rule ccorres_move_c_guard_cte) 1031 apply ctac 1032 apply (rule ccorres_move_c_guard_cte) 1033 apply (ctac(no_vcg)) 1034 apply csymbr 1035 apply (erule_tac t = ret__unsigned_longlong in ssubst) 1036 apply (rule ccorres_cond_both [where R = \<top>, simplified]) 1037 apply (erule mdbNext_not_zero_eq) 1038 apply csymbr 1039 apply simp 1040 apply (rule ccorres_move_c_guard_cte) 1041 apply (simp add:dc_def[symmetric]) 1042 apply (ctac ccorres:ccorres_updateMDB_set_mdbPrev) 1043 apply (simp add:dc_def[symmetric]) 1044 apply (ctac ccorres: ccorres_updateMDB_skip) 1045 apply (wp static_imp_wp)+ 1046 apply (clarsimp simp: Collect_const_mem dc_def split del: if_split) 1047 apply vcg 1048 apply (wp static_imp_wp) 1049 apply (clarsimp simp: Collect_const_mem dc_def split del: if_split) 1050 apply vcg 1051 apply (clarsimp simp:cmdb_node_relation_mdbNext) 1052 apply (wp setUntypedCapAsFull_cte_at_wp static_imp_wp) 1053 apply (clarsimp simp: Collect_const_mem dc_def split del: if_split) 1054 apply (vcg exspec=setUntypedCapAsFull_modifies) 1055 apply wp 1056 apply vcg 1057 apply wp 1058 apply wp 1059 apply vcg 1060 apply wp 1061 apply vcg 1062 apply (simp add: Collect_const_mem split del: if_split) \<comment> \<open>Takes a while\<close> 1063 apply (rule conjI) 1064 apply (clarsimp simp: conj_comms cte_wp_at_ctes_of) 1065 apply (intro conjI) 1066 apply clarsimp 1067 apply simp 1068 apply simp 1069 apply (clarsimp simp: ctes_of_canonical objBits_defs cte_level_bits_def) 1070 apply (rule conjI) 1071 apply (clarsimp simp: isUntypedCap_def split: capability.split_asm) 1072 apply (frule valid_cap_untyped_inv) 1073 apply clarsimp 1074 apply (rule conjI) 1075 apply (case_tac ctea) 1076 apply (clarsimp simp: isUntypedCap_def split: capability.splits) 1077 apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) 1078 apply fastforce 1079 apply clarsimp+ 1080 apply (drule valid_dlist_nextD) 1081 apply (simp add:valid_mdb'_def valid_mdb_ctes_def) 1082 apply simp 1083 apply clarsimp 1084 apply (clarsimp simp: map_comp_Some_iff cte_wp_at_ctes_of 1085 split del: if_split) 1086 apply (clarsimp simp: typ_heap_simps c_guard_clift split_def) 1087 apply (clarsimp simp: is_simple_cap_get_tag_relation ccte_relation_ccap_relation cmdb_node_relation_mdbNext[symmetric]) 1088 done 1089 1090(****************************************************************************) 1091(* *) 1092(* Lemmas dealing with updateMDB on Haskell side and IF-THEN-ELSE on C side *) 1093(* *) 1094(****************************************************************************) 1095 1096lemma updateMDB_mdbNext_set_mdbPrev: 1097 "\<lbrakk> slotc = Ptr slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> 1098 ccorres dc xfdc 1099 (\<lambda>s. is_aligned slota cteSizeBits) 1100 UNIV hs 1101 (updateMDB (mdbNext mdba) (mdbPrev_update (\<lambda>_. slota))) 1102 (IF mdbNext_CL (mdb_node_lift mdbc) \<noteq> 0 1103 THEN Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr (mdbNext_CL (mdb_node_lift mdbc)) :: cte_C ptr)\<rbrace> 1104 (call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr (mdbNext_CL (mdb_node_lift mdbc)):: cte_C ptr 1105 \<rightarrow>[''cteMDBNode_C'']), 1106 v64_' := ptr_val slotc |)) 1107 mdb_node_ptr_set_mdbPrev_'proc 1108 (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a))) 1109 FI)" 1110 apply (rule ccorres_guard_imp2) 1111 apply (rule ccorres_cond_both[where R=\<top>, simplified]) 1112 apply (erule mdbNext_not_zero_eq) 1113 apply (rule ccorres_updateMDB_cte_at) 1114 apply (ctac add: ccorres_updateMDB_set_mdbPrev) 1115 apply (ctac ccorres: ccorres_updateMDB_skip) 1116 apply (clarsimp simp: cmdbnode_relation_def cte_wp_at_ctes_of) 1117 done 1118 1119lemma updateMDB_mdbPrev_set_mdbNext: 1120 "\<lbrakk> slotc = Ptr slota; cmdbnode_relation mdba mdbc\<rbrakk> \<Longrightarrow> 1121 ccorres dc xfdc 1122 (\<lambda>s. is_aligned slota cteSizeBits \<and> canonical_address slota) 1123 UNIV hs 1124 (updateMDB (mdbPrev mdba) (mdbNext_update (\<lambda>_. slota))) 1125 (IF mdbPrev_CL (mdb_node_lift mdbc) \<noteq> 0 1126 THEN Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr (mdbPrev_CL (mdb_node_lift mdbc)):: cte_C ptr)\<rbrace> 1127 (call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr (mdbPrev_CL (mdb_node_lift mdbc)):: cte_C ptr 1128 \<rightarrow>[''cteMDBNode_C'']), 1129 v64_' := ptr_val slotc |)) 1130 mdb_node_ptr_set_mdbNext_'proc 1131 (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a))) 1132 FI)" 1133 apply (rule ccorres_guard_imp2) 1134 apply (rule ccorres_cond_both[where R=\<top>, simplified]) 1135 apply (erule mdbPrev_not_zero_eq) 1136 apply (rule ccorres_updateMDB_cte_at) 1137 apply (ctac add: ccorres_updateMDB_set_mdbNext) 1138 apply (ctac ccorres: ccorres_updateMDB_skip) 1139 apply (clarsimp simp: cte_wp_at_ctes_of cmdbnode_relation_def) 1140 done 1141 1142 1143(************************************************************************) 1144(* *) 1145(* cteMove_ccorres ******************************************************) 1146(* *) 1147(************************************************************************) 1148 1149(* FIXME: move *) 1150lemma cteSizeBits_eq: 1151 "cteSizeBits = cte_level_bits" 1152 by (simp add: cte_level_bits_def cteSizeBits_def) 1153 1154(* FIXME: move *) 1155lemma cteSizeBits_le_cte_level_bits[simp]: 1156 "cteSizeBits \<le> cte_level_bits" 1157 by (simp add: cte_level_bits_def cteSizeBits_def) 1158 1159(* FIXME: rename *) 1160lemma is_aligned_3_prev: 1161 "\<lbrakk> valid_mdb' s; pspace_aligned' s; ctes_of s p = Some cte \<rbrakk> 1162 \<Longrightarrow> is_aligned (mdbPrev (cteMDBNode cte)) cteSizeBits" 1163 apply (cases "mdbPrev (cteMDBNode cte) = 0", simp) 1164 apply (drule (2) valid_mdb_ctes_of_prev) 1165 apply (clarsimp simp: cte_wp_at_ctes_of cteSizeBits_eq ctes_of_aligned_bits) 1166 done 1167 1168(* FIXME: rename *) 1169lemma is_aligned_3_next: 1170 "\<lbrakk> valid_mdb' s; pspace_aligned' s; ctes_of s p = Some cte \<rbrakk> 1171 \<Longrightarrow> is_aligned (mdbNext (cteMDBNode cte)) cteSizeBits" 1172 apply (cases "mdbNext (cteMDBNode cte) = 0", simp) 1173 apply (drule (2) valid_mdb_ctes_of_next) 1174 apply (clarsimp simp: cte_wp_at_ctes_of cteSizeBits_eq ctes_of_aligned_bits) 1175 done 1176 1177lemma cteMove_ccorres: 1178 "ccorres dc xfdc 1179 (valid_mdb' and pspace_aligned' and pspace_canonical') 1180 (UNIV \<inter> {s. destSlot_' s = Ptr dest} 1181 \<inter> {s. srcSlot_' s = Ptr src} 1182 \<inter> {s. ccap_relation cap (newCap_' s)}) [] 1183 (cteMove cap src dest) 1184 (Call cteMove_'proc)" 1185 apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' simp del: return_bind) 1186 apply (ctac pre: ccorres_pre_getCTE ccorres_assert) 1187 apply (ctac+, csymbr+)+ 1188 apply (erule_tac t=ret__unsigned_longlong in ssubst) 1189 apply (ctac add: updateMDB_mdbPrev_set_mdbNext) 1190 apply csymbr 1191 apply csymbr 1192 apply (erule_tac t=ret__unsigned_longlong in ssubst) 1193 apply (rule updateMDB_mdbNext_set_mdbPrev) 1194 apply simp+ 1195 apply (wp, vcg)+ 1196 apply (rule conjI) 1197 apply (clarsimp simp: cte_wp_at_ctes_of cteSizeBits_eq ctes_of_canonical ctes_of_aligned_bits) 1198 apply assumption 1199 apply (clarsimp simp: ccap_relation_NullCap_iff cmdbnode_relation_def 1200 mdb_node_to_H_def nullMDBNode_def false_def) 1201 done 1202 1203(************************************************************************) 1204(* *) 1205(* lemmas used in cteSwap_ccorres ***************************************) 1206(* *) 1207(************************************************************************) 1208 1209 1210 1211(*---------------------------------------------------------------------------------------*) 1212(* corres lemma for return of mdbnode but 'safer' than ccorres_return_cte_mdbnode ------ *) 1213(*---------------------------------------------------------------------------------------*) 1214 1215lemma ccorres_return_cte_mdbnode_safer: 1216 fixes ptr' :: "cstate \<Rightarrow> cte_C ptr" 1217 assumes r1: "\<And>s s' g. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu g s') \<in> rf_sr" 1218 and xf_xfu: "\<And>s g. xf (xfu g s) = g s" 1219 shows "ccorres cmdbnode_relation xf 1220 (\<lambda>s. \<exists> cte'. ctes_of s ptr = Some cte' \<and> cteMDBNode cte = cteMDBNode cte') {s. ptr_val (ptr' s) = ptr} hs 1221 (return (cteMDBNode cte)) 1222 (Basic (\<lambda>s. xfu (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) 1223 (Ptr &(ptr' s \<rightarrow>[''cteMDBNode_C'']))) s))" 1224 apply (rule ccorres_from_vcg) 1225 apply (rule allI, rule conseqPre, vcg) 1226 apply (clarsimp simp add: return_def) 1227 apply rule 1228 apply (erule r1) 1229 apply (simp add: xf_xfu) 1230 apply (drule (1) rf_sr_ctes_of_clift) 1231 apply (clarsimp simp: typ_heap_simps) 1232 done 1233 1234 1235 1236 1237 1238 1239(*-----------------------------------------------------------------------*) 1240(* lemmas about map and hrs_mem -----------------------------------------*) 1241(*-----------------------------------------------------------------------*) 1242 1243declare modify_map_exists_cte[simp] 1244 1245 1246 1247 1248 1249 1250 1251(*------------------------------------------------------------------------------*) 1252(* lemmas about pointer equality given valid_mdb (prev\<noteq>next, prev\<noteq>myself, etc) *) 1253(*------------------------------------------------------------------------------*) 1254 1255lemma valid_mdb_Prev_neq_Next: 1256 "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> 1257 (mdbNext (cteMDBNode cte)) \<noteq> (mdbPrev (cteMDBNode cte))" 1258 apply (simp add: valid_mdb'_def) 1259 apply (simp add: valid_mdb_ctes_def) 1260 apply (elim conjE) 1261 apply (drule (1) mdb_chain_0_no_loops) 1262 apply (simp add: valid_dlist_def) 1263 apply (erule_tac x=p in allE) 1264 apply (erule_tac x=cte in allE) 1265 apply (simp add: Let_def) 1266 apply clarsimp 1267 apply (drule_tac s="mdbNext (cteMDBNode cte)" in sym) 1268 apply simp 1269 apply (simp add: no_loops_def) 1270 apply (erule_tac x= "(mdbNext (cteMDBNode cte))" in allE) 1271 apply (erule notE, rule trancl_trans) 1272 apply (rule r_into_trancl) 1273 apply (simp add: mdb_next_unfold) 1274 apply (rule r_into_trancl) 1275 apply (simp add: mdb_next_unfold) 1276done 1277 1278lemma valid_mdb_Prev_neq_itself: 1279 "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte \<rbrakk> \<Longrightarrow> 1280 (mdbPrev (cteMDBNode cte)) \<noteq> p" 1281 apply (unfold valid_mdb'_def) 1282 apply (simp add: CSpace_I.no_self_loop_prev) 1283done 1284 1285lemma valid_mdb_Next_neq_itself: 1286 "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte \<rbrakk> \<Longrightarrow> 1287 (mdbNext (cteMDBNode cte)) \<noteq> p" 1288 apply (unfold valid_mdb'_def) 1289 apply (simp add: CSpace_I.no_self_loop_next) 1290done 1291 1292lemma valid_mdb_not_same_Next : 1293 "\<lbrakk> valid_mdb' s; p\<noteq>p'; ctes_of s p = Some cte; ctes_of s p' = Some cte'; 1294 (mdbNext (cteMDBNode cte))\<noteq>0 \<or> (mdbNext (cteMDBNode cte'))\<noteq>0 \<rbrakk> \<Longrightarrow> 1295 (mdbNext (cteMDBNode cte)) \<noteq> (mdbNext (cteMDBNode cte')) " 1296 apply (clarsimp) 1297 apply (case_tac cte, clarsimp) 1298 apply (rename_tac capability mdbnode) 1299 apply (case_tac cte', clarsimp) 1300 apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode") 1301 apply (drule (2) mdb_ptr.p_nextD) 1302 apply clarsimp 1303 apply (unfold mdb_ptr_def vmdb_def mdb_ptr_axioms_def valid_mdb'_def, simp) 1304 done 1305 1306lemma valid_mdb_not_same_Prev : 1307 "\<lbrakk> valid_mdb' s; p\<noteq>p'; ctes_of s p = Some cte; ctes_of s p' = Some cte'; 1308 (mdbPrev (cteMDBNode cte))\<noteq>0 \<or> (mdbPrev (cteMDBNode cte'))\<noteq>0 \<rbrakk> \<Longrightarrow> 1309 (mdbPrev (cteMDBNode cte)) \<noteq> (mdbPrev (cteMDBNode cte')) " 1310 apply (clarsimp) 1311 apply (case_tac cte, clarsimp) 1312 apply (rename_tac capability mdbnode) 1313 apply (case_tac cte', clarsimp) 1314 apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode") 1315 apply (drule (2) mdb_ptr.p_prevD) 1316 apply clarsimp 1317 apply (unfold mdb_ptr_def vmdb_def mdb_ptr_axioms_def valid_mdb'_def, simp) 1318 done 1319 1320 1321 1322 1323(*---------------------------------------------------------------------------------*) 1324(* lemmas to simplify the big last goal on C side to avoid proving things twice ---*) 1325(*---------------------------------------------------------------------------------*) 1326 1327lemma c_guard_and_h_t_valid_eq_h_t_valid: 1328 "(POINTER \<noteq> 0 \<longrightarrow> 1329 c_guard ((Ptr &(Ptr POINTER ::cte_C ptr \<rightarrow>[''cteMDBNode_C''])) ::mdb_node_C ptr) \<and> 1330 s' \<Turnstile>\<^sub>c (Ptr (POINTER)::cte_C ptr)) = 1331 (POINTER \<noteq> 0 \<longrightarrow> 1332 s' \<Turnstile>\<^sub>c (Ptr (POINTER)::cte_C ptr))" 1333 apply (rule iffI, clarsimp+) 1334 apply (rule c_guard_field_lvalue) 1335 apply (rule c_guard_h_t_valid, assumption) 1336 apply (fastforce simp: typ_uinfo_t_def)+ 1337done 1338 1339 1340lemma c_guard_and_h_t_valid_and_rest_eq_h_t_valid_and_rest: 1341 "(POINTER \<noteq> 0 \<longrightarrow> 1342 c_guard ((Ptr &(Ptr POINTER ::cte_C ptr \<rightarrow>[''cteMDBNode_C''])) ::mdb_node_C ptr) \<and> 1343 s' \<Turnstile>\<^sub>c (Ptr (POINTER)::cte_C ptr) \<and> REST) = 1344 (POINTER \<noteq> 0 \<longrightarrow> 1345 s' \<Turnstile>\<^sub>c (Ptr (POINTER)::cte_C ptr) \<and> REST)" 1346 apply (rule iffI, clarsimp+) 1347 apply (rule c_guard_field_lvalue) 1348 apply (rule c_guard_h_t_valid, assumption) 1349 apply (fastforce simp: typ_uinfo_t_def)+ 1350done 1351 1352 1353(************************************************************************) 1354(* *) 1355(* cteSwap_ccorres ******************************************************) 1356(* *) 1357(************************************************************************) 1358 1359lemma cteSwap_ccorres: 1360 "ccorres dc xfdc 1361 (valid_mdb' and pspace_aligned' and pspace_canonical' 1362 and (\<lambda>_. slot1 \<noteq> slot2)) 1363 (UNIV \<inter> {s. slot1_' s = Ptr slot1} 1364 \<inter> {s. slot2_' s = Ptr slot2} 1365 \<inter> {s. ccap_relation cap1 (cap1_' s)} 1366 \<inter> {s. ccap_relation cap2 (cap2_' s)}) 1367 [] 1368 (cteSwap cap1 slot1 cap2 slot2) 1369 (Call cteSwap_'proc)" 1370 supply ctes_of_aligned_bits[simp] 1371 apply (cinit (no_ignore_call) lift: slot1_' slot2_' cap1_' cap2_' simp del: return_bind) 1372 apply (ctac (no_vcg) pre: ccorres_pre_getCTE ccorres_move_guard_ptr_safe) 1373 apply (rule ccorres_updateCap_cte_at) 1374 apply (ctac (no_vcg) add: ccorres_return_cte_mdbnode_safer [where ptr=slot1])+ 1375 apply csymbr 1376 apply csymbr 1377 apply (erule_tac t=ret__unsigned_longlong in ssubst) 1378 apply (ctac (no_vcg) add: updateMDB_mdbPrev_set_mdbNext) 1379 apply csymbr 1380 apply csymbr 1381 apply (erule_tac t=ret__unsigned_longlong in ssubst) 1382 apply (ctac (no_vcg) add: updateMDB_mdbNext_set_mdbPrev) 1383 apply (rule ccorres_move_c_guard_cte) 1384 apply (ctac (no_vcg) pre: ccorres_getCTE ccorres_move_guard_ptr_safe 1385 add: ccorres_return_cte_mdbnode[where ptr=slot2] 1386 ccorres_move_guard_ptr_safe)+ 1387 apply csymbr 1388 apply csymbr 1389 apply (erule_tac t=ret__unsigned_longlong in ssubst) 1390 apply (ctac (no_vcg) add: updateMDB_mdbPrev_set_mdbNext) 1391 apply csymbr 1392 apply csymbr 1393 apply (erule_tac t=ret__unsigned_longlong in ssubst) 1394 apply (ctac (no_vcg) add: updateMDB_mdbNext_set_mdbPrev) 1395 apply wp 1396 apply simp 1397 apply wp 1398 apply simp 1399 apply wp 1400 apply simp 1401 apply wp 1402 apply simp 1403 apply (clarsimp simp : cte_wp_at_ctes_of) 1404 apply wp 1405 apply simp 1406 apply wp 1407 apply simp 1408 apply wp 1409 apply simp 1410 apply (clarsimp simp : cte_wp_at_ctes_of) 1411 apply (wp updateCap_ctes_of_wp) 1412 apply simp 1413 apply (clarsimp simp : cte_wp_at_ctes_of) 1414 apply (wp updateCap_ctes_of_wp) 1415 apply simp 1416 apply (clarsimp simp: cte_wp_at_ctes_of) 1417 apply (apply_conjunct \<open>match conclusion in \<open>no_0 _\<close> 1418 \<Rightarrow> \<open>simp add: valid_mdb'_def, erule (1) valid_mdb_ctesE\<close>\<close>) 1419 apply (case_tac cte; simp add: modify_map_if ctes_of_canonical) 1420 done 1421 1422(* todo change in cteMove (\<lambda>s. ctes_of s src = Some scte) *) 1423 1424 1425(************************************************************************) 1426(* *) 1427(* lemmas used in emptySlot_ccorres *************************************) 1428(* *) 1429(************************************************************************) 1430 1431 1432declare if_split [split del] 1433 1434(* rq CALL mdb_node_ptr_set_mdbNext_'proc \<dots>) is a printing bug 1435 one should write CALL mdb_node_ptr_set_mdbNext 1436*) 1437 1438lemma not_NullCap_eq_not_cap_null_cap: 1439 " \<lbrakk>ccap_relation cap cap' ; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> 1440 (cap \<noteq> NullCap) = (s' \<in> {_. (cap_get_tag cap' \<noteq> scast cap_null_cap)})" 1441 apply (rule iffI) 1442 apply (case_tac "cap_get_tag cap' \<noteq> scast cap_null_cap", clarsimp+) 1443 apply (erule notE) 1444 apply (simp add: cap_get_tag_NullCap) 1445 apply (case_tac "cap_get_tag cap' \<noteq> scast cap_null_cap") 1446 apply (rule notI) 1447 apply (erule notE) 1448 apply (simp add: cap_get_tag_NullCap) 1449 apply clarsimp 1450done 1451 1452lemma emptySlot_helper: 1453 fixes mdbNode 1454 defines "nextmdb \<equiv> Ptr &(Ptr ((mdbNext_CL (mdb_node_lift mdbNode)))::cte_C ptr\<rightarrow>[''cteMDBNode_C'']) :: mdb_node_C ptr" 1455 defines "nextcte \<equiv> Ptr ((mdbNext_CL (mdb_node_lift mdbNode)))::cte_C ptr" 1456 shows "\<lbrakk>cmdbnode_relation rva mdbNode\<rbrakk> 1457 \<Longrightarrow> ccorres dc xfdc \<top> UNIV hs 1458 (updateMDB (mdbNext rva) 1459 (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged rva) (mdbPrev_update (\<lambda>_. mdbPrev rva) mdb))) 1460 (IF mdbNext_CL (mdb_node_lift mdbNode) \<noteq> 0 THEN 1461 Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t nextcte\<rbrace> 1462 (CALL mdb_node_ptr_set_mdbPrev(nextmdb, ptr_val (Ptr (mdbPrev_CL (mdb_node_lift mdbNode))))) 1463 FI;; 1464 IF mdbNext_CL (mdb_node_lift mdbNode) \<noteq> 0 THEN 1465 Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t nextcte\<rbrace> 1466 (\<acute>ret__unsigned_longlong :== CALL mdb_node_get_mdbFirstBadged(h_val (hrs_mem \<acute>t_hrs) nextmdb));; 1467 \<acute>ret__int :== (if \<acute>ret__unsigned_longlong \<noteq> 0 then 1 else 0);; 1468 IF \<acute>ret__int \<noteq> 0 THEN 1469 SKIP 1470 ELSE 1471 \<acute>ret__unsigned_longlong :== CALL mdb_node_get_mdbFirstBadged(mdbNode);; 1472 \<acute>ret__int :== (if \<acute>ret__unsigned_longlong \<noteq> 0 then 1 else 0) 1473 FI;; 1474 Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t nextcte\<rbrace> 1475 (CALL mdb_node_ptr_set_mdbFirstBadged(nextmdb,scast \<acute>ret__int)) 1476 FI)" 1477 apply (rule ccorres_guard_imp2) 1478 apply (rule ccorres_updateMDB_cte_at) 1479 apply (subgoal_tac "mdbNext rva=(mdbNext_CL (mdb_node_lift mdbNode))") 1480 prefer 2 1481 apply (simp add: cmdbnode_relation_def) 1482 1483 apply (case_tac "mdbNext rva \<noteq> 0") 1484 apply (case_tac "mdbNext_CL (mdb_node_lift mdbNode) = 0", simp) 1485 1486 \<comment> \<open>case where mdbNext rva \<noteq> 0 and mdbNext_CL (mdb_node_lift mdbNode) \<noteq> 0\<close> 1487 apply (unfold updateMDB_def) 1488 apply (clarsimp simp: Let_def) 1489 apply (rule ccorres_pre_getCTE [where P = "\<lambda>cte s. ctes_of s (mdbNext rva) = Some cte" and P' = "\<lambda>_. UNIV"]) 1490 apply (rule ccorres_from_vcg) 1491 apply (rule allI) 1492 apply (rule conseqPre, vcg) 1493 apply clarsimp 1494 1495 apply (frule(1) rf_sr_ctes_of_clift) 1496 apply (clarsimp simp: typ_heap_simps' nextmdb_def if_1_0_0 nextcte_def) 1497 apply (intro conjI impI allI) 1498 \<comment> \<open>\<dots> \<exists>x\<in>fst \<dots>\<close> 1499 apply clarsimp 1500 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption ) 1501 apply (erule bexI [rotated]) 1502 apply (frule (1) rf_sr_ctes_of_clift) 1503 apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps 1504 Let_def cpspace_relation_def) 1505 apply (rule conjI) 1506 prefer 2 1507 apply (erule_tac t = s' in ssubst) 1508 apply (simp add: carch_state_relation_def cmachine_state_relation_def 1509 fpu_null_state_heap_update_tag_disj_simps 1510 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] 1511 h_t_valid_clift_Some_iff typ_heap_simps' 1512 cong: lifth_update) 1513 apply (erule (1) setCTE_tcb_case) 1514 1515 apply (erule (2) cspace_cte_relation_upd_mdbI) 1516 apply (simp add: cmdbnode_relation_def) 1517 apply (simp add: mdb_node_to_H_def) 1518 1519 apply (subgoal_tac "mdbFirstBadged_CL (mdb_node_lift mdbNode) && mask (Suc 0) = 1520 mdbFirstBadged_CL (mdb_node_lift mdbNode)") 1521 prefer 2 1522 subgoal by (simp add: mdb_node_lift_def mask_def word_bw_assocs) 1523 apply (subgoal_tac "mdbFirstBadged_CL (cteMDBNode_CL y) && mask (Suc 0) = 1524 mdbFirstBadged_CL (cteMDBNode_CL y)") 1525 prefer 2 1526 apply (drule cteMDBNode_CL_lift [symmetric]) 1527 subgoal by (simp add: mdb_node_lift_def mask_def word_bw_assocs) 1528 subgoal by (simp add: to_bool_def mask_def) 1529 \<comment> \<open>\<dots> \<exists>x\<in>fst \<dots>\<close> 1530 apply clarsimp 1531 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption ) 1532 apply (erule bexI [rotated]) 1533 apply (frule (1) rf_sr_ctes_of_clift) 1534 apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps 1535 Let_def cpspace_relation_def) 1536 apply (rule conjI) 1537 prefer 2 1538 apply (erule_tac t = s' in ssubst) 1539 apply (simp add: carch_state_relation_def cmachine_state_relation_def 1540 fpu_null_state_heap_update_tag_disj_simps 1541 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] 1542 typ_heap_simps' h_t_valid_clift_Some_iff 1543 cong: lifth_update) 1544 apply (erule (1) setCTE_tcb_case) 1545 1546 apply (erule (2) cspace_cte_relation_upd_mdbI) 1547 apply (simp add: cmdbnode_relation_def) 1548 apply (simp add: mdb_node_to_H_def) 1549 1550 apply (subgoal_tac "mdbFirstBadged_CL (mdb_node_lift mdbNode) && mask (Suc 0) = 1551 mdbFirstBadged_CL (mdb_node_lift mdbNode)") 1552 prefer 2 1553 subgoal by (simp add: mdb_node_lift_def mask_def word_bw_assocs) 1554 apply (subgoal_tac "mdbFirstBadged_CL (cteMDBNode_CL y) && mask (Suc 0) = 1555 mdbFirstBadged_CL (cteMDBNode_CL y)") 1556 prefer 2 1557 apply (drule cteMDBNode_CL_lift [symmetric]) 1558 subgoal by (simp add: mdb_node_lift_def mask_def word_bw_assocs) 1559 apply (simp add: to_bool_def mask_def split: if_split) 1560 1561 \<comment> \<open>trivial case where mdbNext rva = 0\<close> 1562 apply (simp add:ccorres_cond_empty_iff) 1563 apply (rule ccorres_guard_imp2) 1564 apply (rule ccorres_return_Skip) 1565 apply simp 1566 apply (clarsimp simp: cmdbnode_relation_def) 1567done 1568 1569 1570 1571(************************************************************************) 1572(* *) 1573(* emptySlot_ccorres ****************************************************) 1574(* *) 1575(************************************************************************) 1576 1577 1578(* ML "set CtacImpl.trace_ctac"*) 1579 1580 1581lemma mdbNext_CL_mdb_node_lift_eq_mdbNext: 1582 "cmdbnode_relation n n' \<Longrightarrow> (mdbNext_CL (mdb_node_lift n')) =(mdbNext n)" 1583 by (erule cmdbnode_relationE, fastforce simp: mdbNext_to_H) 1584 1585lemma mdbPrev_CL_mdb_node_lift_eq_mdbPrev: 1586 "cmdbnode_relation n n' \<Longrightarrow> (mdbPrev_CL (mdb_node_lift n')) =(mdbPrev n)" 1587 by (erule cmdbnode_relationE, fastforce simp: mdbNext_to_H) 1588 1589 1590lemma mdbNext_not_zero_eq_simpler: 1591 "cmdbnode_relation n n' \<Longrightarrow> (mdbNext n \<noteq> 0) = (mdbNext_CL (mdb_node_lift n') \<noteq> 0)" 1592 apply clarsimp 1593 apply (erule cmdbnode_relationE) 1594 apply (fastforce simp: mdbNext_to_H) 1595 done 1596 1597 1598 1599lemma mdbPrev_not_zero_eq_simpler: 1600 "cmdbnode_relation n n' \<Longrightarrow> (mdbPrev n \<noteq> 0) = (mdbPrev_CL (mdb_node_lift n') \<noteq> 0)" 1601 apply clarsimp 1602 apply (erule cmdbnode_relationE) 1603 apply (fastforce simp: mdbPrev_to_H) 1604 done 1605 1606lemma h_t_valid_and_cslift_and_c_guard_field_mdbPrev_CL: 1607 " \<lbrakk>(s, s') \<in> rf_sr; cte_at' slot s; valid_mdb' s; cslift s' (Ptr slot) = Some cte'\<rbrakk> 1608 \<Longrightarrow> (mdbPrev_CL (mdb_node_lift (cteMDBNode_C cte')) \<noteq> 0) \<longrightarrow> 1609 s' \<Turnstile>\<^sub>c ( Ptr (mdbPrev_CL (mdb_node_lift (cteMDBNode_C cte'))) :: cte_C ptr) \<and> 1610 (\<exists> cten. cslift s' (Ptr (mdbPrev_CL (mdb_node_lift (cteMDBNode_C cte'))) :: cte_C ptr) = Some cten) \<and> 1611 c_guard (Ptr &(Ptr (mdbPrev_CL (mdb_node_lift (cteMDBNode_C cte')))::cte_C ptr\<rightarrow>[''cteMDBNode_C'']) :: mdb_node_C ptr)" 1612 apply (clarsimp simp: cte_wp_at_ctes_of) 1613 apply (drule (1) valid_mdb_ctes_of_prev) 1614 apply (frule (2) rf_sr_cte_relation) 1615 apply (drule ccte_relation_cmdbnode_relation) 1616 apply (simp add: mdbPrev_not_zero_eq_simpler) 1617 apply (clarsimp simp: cte_wp_at_ctes_of) 1618 apply (drule (1) rf_sr_ctes_of_clift [rotated])+ 1619 apply (clarsimp simp: typ_heap_simps) 1620 1621 apply (rule c_guard_field_lvalue [rotated]) 1622 apply (fastforce simp: typ_uinfo_t_def)+ 1623 apply (rule c_guard_clift) 1624 apply (simp add: typ_heap_simps) 1625done 1626 1627lemma h_t_valid_and_cslift_and_c_guard_field_mdbNext_CL: 1628 " \<lbrakk>(s, s') \<in> rf_sr; cte_at' slot s; valid_mdb' s; cslift s' (Ptr slot) = Some cte'\<rbrakk> 1629 \<Longrightarrow> (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte')) \<noteq> 0) \<longrightarrow> 1630 s' \<Turnstile>\<^sub>c ( Ptr (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte'))) :: cte_C ptr) \<and> 1631 (\<exists> cten. cslift s' (Ptr (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte'))) :: cte_C ptr) = Some cten) \<and> 1632 c_guard (Ptr &(Ptr (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte')))::cte_C ptr\<rightarrow>[''cteMDBNode_C'']) :: mdb_node_C ptr)" 1633 apply (clarsimp simp: cte_wp_at_ctes_of) 1634 apply (drule (1) valid_mdb_ctes_of_next) 1635 apply (frule (2) rf_sr_cte_relation) 1636 apply (drule ccte_relation_cmdbnode_relation) 1637 apply (simp add: mdbNext_not_zero_eq_simpler) 1638 apply (clarsimp simp: cte_wp_at_ctes_of) 1639 apply (drule (1) rf_sr_ctes_of_clift [rotated])+ 1640 apply (clarsimp simp: typ_heap_simps) 1641 1642 apply (rule c_guard_field_lvalue [rotated]) 1643 apply (fastforce simp: typ_uinfo_t_def)+ 1644 apply (rule c_guard_clift) 1645 apply (simp add: typ_heap_simps) 1646done 1647 1648 1649lemma valid_mdb_Prev_neq_Next_better: 1650 "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte \<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> 1651 (mdbNext (cteMDBNode cte)) \<noteq> (mdbPrev (cteMDBNode cte))" 1652 apply (rule impI) 1653 apply (simp add: valid_mdb'_def) 1654 apply (simp add: valid_mdb_ctes_def) 1655 apply (elim conjE) 1656 apply (drule (1) mdb_chain_0_no_loops) 1657 apply (simp add: valid_dlist_def) 1658 apply (erule_tac x=p in allE) 1659 apply (erule_tac x=cte in allE) 1660 apply (simp add: Let_def) 1661 apply clarsimp 1662 apply (drule_tac s="mdbNext (cteMDBNode cte)" in sym) 1663 apply simp 1664 apply (simp add: no_loops_def) 1665 apply (erule_tac x= "(mdbNext (cteMDBNode cte))" in allE) 1666 apply (erule notE, rule trancl_trans) 1667 apply (rule r_into_trancl) 1668 apply (simp add: mdb_next_unfold) 1669 apply (rule r_into_trancl) 1670 apply (simp add: mdb_next_unfold) 1671done 1672 1673(* TODO: move *) 1674 1675definition 1676 irq_opt_relation_def: 1677 "irq_opt_relation (airq :: (8 word) option) (cirq :: word8) \<equiv> 1678 case airq of 1679 Some irq \<Rightarrow> (cirq = ucast irq \<and> 1680 irq \<noteq> scast irqInvalid \<and> 1681 ucast irq \<le> (scast Kernel_C.maxIRQ :: word8)) 1682 | None \<Rightarrow> cirq = scast irqInvalid" 1683 1684 1685declare unat_ucast_up_simp[simp] 1686 1687 1688lemma setIRQState_ccorres: 1689 "ccorres dc xfdc 1690 (\<top> and (\<lambda>s. irq \<le> scast Kernel_C.maxIRQ)) 1691 (UNIV \<inter> {s. irqState_' s = irqstate_to_C irqState} 1692 \<inter> {s. irq_' s = irq}) 1693 [] 1694 (setIRQState irqState irq) 1695 (Call setIRQState_'proc )" 1696proof - 1697 have is_up_8_16[simp]: "is_up (ucast :: word8 \<Rightarrow> word16)" 1698 by (simp add: is_up_def source_size_def target_size_def word_size) 1699 1700 1701show ?thesis 1702 apply (rule ccorres_gen_asm) 1703 apply (cinit simp del: return_bind) 1704 apply (rule ccorres_symb_exec_l) 1705 apply simp 1706 apply (rule_tac r'="dc" and xf'="xfdc" in ccorres_split_nothrow) 1707 apply (rule_tac P= "\<lambda>s. st = (ksInterruptState s)" 1708 and P'= "(UNIV \<inter> {s. irqState_' s = irqstate_to_C irqState} 1709 \<inter> {s. irq_' s = ucast irq} )" 1710 in ccorres_from_vcg) 1711 apply (rule allI, rule conseqPre, vcg) 1712 apply (clarsimp simp: setInterruptState_def) 1713 apply (clarsimp simp: simpler_modify_def) 1714 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 1715 carch_state_relation_def cmachine_state_relation_def) 1716 apply (simp add: cinterrupt_relation_def Kernel_C.maxIRQ_def) 1717 apply (clarsimp simp: word_sless_msb_less order_le_less_trans 1718 unat_ucast_no_overflow_le word_le_nat_alt ucast_ucast_b 1719 split: if_split ) 1720 apply ceqv 1721 apply (ctac add: maskInterrupt_ccorres) 1722 apply wp 1723 apply vcg 1724 apply wp 1725 apply (simp add: getInterruptState_def gets_def) 1726 apply wp 1727 apply (simp add: empty_fail_def getInterruptState_def simpler_gets_def) 1728 apply clarsimp 1729 apply (simp add: from_bool_def) 1730 apply (cases irqState, simp_all) 1731 apply (simp add: Kernel_C.IRQSignal_def Kernel_C.IRQInactive_def) 1732 apply (simp add: Kernel_C.IRQTimer_def Kernel_C.IRQInactive_def) 1733 apply (simp add: Kernel_C.IRQInactive_def Kernel_C.IRQReserved_def) 1734 done 1735qed 1736 1737 1738lemma deletedIRQHandler_ccorres: 1739 "ccorres dc xfdc 1740 (\<lambda>s. irq \<le> scast Kernel_C.maxIRQ) 1741 (UNIV \<inter> {s. irq_' s = ucast irq}) [] 1742 (deletedIRQHandler irq) 1743 (Call deletedIRQHandler_'proc)" 1744 apply (cinit simp del: return_bind) 1745 apply (ctac add: setIRQState_ccorres) 1746 apply clarsimp 1747done 1748 1749lemmas ccorres_split_noop_lhs 1750 = ccorres_split_nothrow[where c=Skip, OF _ ceqv_refl _ _ hoarep.Skip, 1751 simplified ccorres_seq_skip] 1752 1753(* FIXME: to SR_Lemmas *) 1754lemma region_is_bytes_subset: 1755 "region_is_bytes' ptr sz htd 1756 \<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz} 1757 \<Longrightarrow> region_is_bytes' ptr' sz' htd" 1758 by (auto simp: region_is_bytes'_def) 1759 1760lemma region_actually_is_bytes_subset: 1761 "region_actually_is_bytes' ptr sz htd 1762 \<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz} 1763 \<Longrightarrow> region_actually_is_bytes' ptr' sz' htd" 1764 by (auto simp: region_actually_is_bytes'_def) 1765 1766lemma intvl_both_le: 1767 "\<lbrakk> a \<le> x; unat x + y \<le> unat a + b \<rbrakk> 1768 \<Longrightarrow> {x ..+ y} \<le> {a ..+ b}" 1769 apply (rule order_trans[OF _ intvl_sub_offset[where x="x - a"]]) 1770 apply (simp, rule order_refl) 1771 apply unat_arith 1772 done 1773 1774lemma untypedZeroRange_idx_forward_helper: 1775 "isUntypedCap cap 1776 \<Longrightarrow> capFreeIndex cap \<le> idx 1777 \<Longrightarrow> idx \<le> 2 ^ capBlockSize cap 1778 \<Longrightarrow> valid_cap' cap s 1779 \<Longrightarrow> (case (untypedZeroRange cap, untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap)) 1780 of (Some (a, b), Some (a', b')) \<Rightarrow> {a' ..+ unat (b' + 1 - a')} \<subseteq> {a ..+ unat (b + 1 - a)} 1781 | _ \<Rightarrow> True)" 1782 apply (clarsimp split: option.split) 1783 apply (clarsimp simp: untypedZeroRange_def max_free_index_def Let_def 1784 isCap_simps valid_cap_simps' capAligned_def untypedBits_defs 1785 split: if_split_asm) 1786 apply (erule subsetD[rotated], rule intvl_both_le) 1787 apply (clarsimp simp: getFreeRef_def) 1788 apply (rule word_plus_mono_right) 1789 apply (rule PackedTypes.of_nat_mono_maybe_le) 1790 apply (erule order_le_less_trans, rule power_strict_increasing, simp_all) 1791 apply (erule is_aligned_no_wrap') 1792 apply (rule word_of_nat_less, simp) 1793 apply (simp add: getFreeRef_def) 1794 apply (simp add: unat_plus_simple[THEN iffD1, OF is_aligned_no_wrap'] 1795 word_of_nat_less) 1796 apply (simp add: word_of_nat_le unat_sub 1797 order_le_less_trans[OF _ power_strict_increasing] 1798 unat_of_nat_eq[where 'a=machine_word_len, folded word_bits_def]) 1799 done 1800 1801lemma intvl_close_Un: 1802 "y = x + of_nat n 1803 \<Longrightarrow> ({x ..+ n} \<union> {y ..+ m}) = {x ..+ n + m}" 1804 apply ((simp add: intvl_def, safe, simp_all, 1805 simp_all only: of_nat_add[symmetric]); (rule exI, strengthen refl)) 1806 apply simp_all 1807 apply (rule ccontr) 1808 apply (drule_tac x="k - n" in spec) 1809 apply simp 1810 done 1811 1812lemma untypedZeroRange_idx_backward_helper: 1813 "isUntypedCap cap 1814 \<Longrightarrow> idx \<le> capFreeIndex cap 1815 \<Longrightarrow> idx \<le> 2 ^ capBlockSize cap 1816 \<Longrightarrow> valid_cap' cap s 1817 \<Longrightarrow> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) 1818 of None \<Rightarrow> True | Some (a', b') \<Rightarrow> 1819 {a' ..+ unat (b' + 1 - a')} \<subseteq> {capPtr cap + of_nat idx ..+ (capFreeIndex cap - idx)} 1820 \<union> (case untypedZeroRange cap 1821 of Some (a, b) \<Rightarrow> {a ..+ unat (b + 1 - a)} 1822 | None \<Rightarrow> {}) 1823 )" 1824 apply (clarsimp split: option.split, intro impI conjI allI) 1825 apply (rule intvl_both_le; clarsimp simp: untypedZeroRange_def 1826 max_free_index_def Let_def 1827 isCap_simps valid_cap_simps' capAligned_def 1828 split: if_split_asm) 1829 apply (clarsimp simp: getFreeRef_def) 1830 apply (clarsimp simp: getFreeRef_def) 1831 apply (simp add: word_of_nat_le unat_sub 1832 order_le_less_trans[OF _ power_strict_increasing] 1833 unat_of_nat_eq[where 'a=machine_word_len, folded word_bits_def]) 1834 apply (subst intvl_close_Un) 1835 apply (clarsimp simp: untypedZeroRange_def 1836 max_free_index_def Let_def 1837 getFreeRef_def 1838 split: if_split_asm) 1839 apply (clarsimp simp: untypedZeroRange_def 1840 max_free_index_def Let_def 1841 getFreeRef_def isCap_simps valid_cap_simps' 1842 split: if_split_asm) 1843 apply (simp add: word_of_nat_le unat_sub capAligned_def 1844 order_le_less_trans[OF _ power_strict_increasing] 1845 order_le_less_trans[where x=idx] 1846 unat_of_nat_eq[where 'a=machine_word_len, folded word_bits_def]) 1847 done 1848 1849lemma ctes_of_untyped_zero_rf_sr_case: 1850 "\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr; 1851 untyped_ranges_zero' s \<rbrakk> 1852 \<Longrightarrow> case untypedZeroRange (cteCap cte) 1853 of None \<Rightarrow> True 1854 | Some (start, end) \<Rightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'" 1855 by (simp split: option.split add: ctes_of_untyped_zero_rf_sr) 1856 1857lemma gsUntypedZeroRanges_update_helper: 1858 "(\<sigma>, s) \<in> rf_sr 1859 \<Longrightarrow> (zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)) 1860 \<longrightarrow> zero_ranges_are_zero (f (gsUntypedZeroRanges \<sigma>)) (t_hrs_' (globals s))) 1861 \<Longrightarrow> (gsUntypedZeroRanges_update f \<sigma>, s) \<in> rf_sr" 1862 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 1863 1864lemma heap_list_zero_Ball_intvl: 1865 "heap_list_is_zero hmem ptr n = (\<forall>x \<in> {ptr ..+ n}. hmem x = 0)" 1866 apply safe 1867 apply (erule heap_list_h_eq_better) 1868 apply (simp add: heap_list_rpbs) 1869 apply (rule trans[OF heap_list_h_eq2 heap_list_rpbs]) 1870 apply simp 1871 done 1872 1873lemma untypedZeroRange_not_device: 1874 "untypedZeroRange cap = Some r 1875 \<Longrightarrow> \<not> capIsDevice cap" 1876 by (clarsimp simp: untypedZeroRange_def) 1877 1878lemma updateTrackedFreeIndex_noop_ccorres: 1879 "ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap 1880 \<and> idx \<le> 2 ^ capBlockSize cap 1881 \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) o cteCap) slot 1882 and valid_objs' and untyped_ranges_zero') 1883 {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_zero_bytes (capPtr cap' + of_nat idx) (capFreeIndex cap' - idx) s} hs 1884 (updateTrackedFreeIndex slot idx) Skip" 1885 (is "ccorres dc xfdc ?P ?P' _ _ _") 1886 apply (simp add: updateTrackedFreeIndex_def getSlotCap_def) 1887 apply (rule ccorres_guard_imp) 1888 apply (rule ccorres_pre_getCTE[where P="\<lambda>rv. 1889 cte_wp_at' ((=) rv) slot and ?P" and P'="K ?P'"]) 1890 apply (rule ccorres_from_vcg) 1891 apply (rule allI, rule conseqPre, vcg) 1892 apply (clarsimp simp: cte_wp_at_ctes_of) 1893 apply (frule(1) ctes_of_valid') 1894 apply (frule(2) ctes_of_untyped_zero_rf_sr_case) 1895 apply (clarsimp simp: simpler_modify_def bind_def cte_wp_at_ctes_of) 1896 apply (erule gsUntypedZeroRanges_update_helper) 1897 apply (clarsimp simp: zero_ranges_are_zero_def 1898 split: if_split) 1899 apply (case_tac "(a, b) \<in> gsUntypedZeroRanges \<sigma>") 1900 apply (drule(1) bspec, simp) 1901 apply (erule disjE_L) 1902 apply (frule(3) untypedZeroRange_idx_forward_helper) 1903 apply (clarsimp simp: isCap_simps valid_cap_simps') 1904 apply (case_tac "untypedZeroRange (cteCap cte)") 1905 apply (clarsimp simp: untypedZeroRange_def 1906 valid_cap_simps' 1907 max_free_index_def Let_def 1908 split: if_split_asm) 1909 apply clarsimp 1910 apply (thin_tac "\<not> capIsDevice cap' \<longrightarrow> P" for P) 1911 apply (clarsimp split: option.split_asm) 1912 apply (subst region_actually_is_bytes_subset, simp+) 1913 apply (subst heap_list_is_zero_mono2, simp+) 1914 apply (frule untypedZeroRange_idx_backward_helper[where idx=idx], 1915 simp+) 1916 apply (clarsimp simp: isCap_simps valid_cap_simps') 1917 apply (clarsimp split: option.split_asm) 1918 apply (clarsimp dest!: untypedZeroRange_not_device) 1919 apply (subst region_actually_is_bytes_subset, simp+) 1920 apply (subst heap_list_is_zero_mono2, simp+) 1921 apply (simp add: region_actually_is_bytes'_def heap_list_zero_Ball_intvl) 1922 apply (clarsimp dest!: untypedZeroRange_not_device) 1923 apply blast 1924 apply (clarsimp simp: cte_wp_at_ctes_of) 1925 apply clarsimp 1926 done 1927 1928lemma updateTrackedFreeIndex_forward_noop_ccorres: 1929 "ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap 1930 \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) o cteCap) slot 1931 and valid_objs' and untyped_ranges_zero') UNIV hs 1932 (updateTrackedFreeIndex slot idx) Skip" 1933 (is "ccorres dc xfdc ?P UNIV _ _ _") 1934 apply (rule ccorres_name_pre) 1935 apply (rule ccorres_guard_imp2, 1936 rule_tac cap'="cteCap (the (ctes_of s slot))" in updateTrackedFreeIndex_noop_ccorres) 1937 apply (clarsimp simp: cte_wp_at_ctes_of region_actually_is_bytes'_def) 1938 done 1939 1940lemma clearUntypedFreeIndex_noop_ccorres: 1941 "ccorres dc xfdc (valid_objs' and untyped_ranges_zero') UNIV hs 1942 (clearUntypedFreeIndex p) Skip" 1943 apply (simp add: clearUntypedFreeIndex_def getSlotCap_def) 1944 apply (rule ccorres_guard_imp) 1945 apply (rule ccorres_pre_getCTE[where P="\<lambda>rv. cte_wp_at' ((=) rv) p 1946 and valid_objs' and untyped_ranges_zero'" and P'="K UNIV"]) 1947 apply (case_tac "cteCap cte", simp_all add: ccorres_guard_imp[OF ccorres_return_Skip])[1] 1948 apply (rule ccorres_guard_imp, rule updateTrackedFreeIndex_forward_noop_ccorres) 1949 apply (clarsimp simp: cte_wp_at_ctes_of max_free_index_def) 1950 apply (frule(1) Finalise_R.ctes_of_valid') 1951 apply (clarsimp simp: valid_cap_simps') 1952 apply simp 1953 apply (clarsimp simp: cte_wp_at_ctes_of) 1954 apply simp 1955 done 1956 1957lemma canonical_address_mdbNext_CL: 1958 "canonical_address (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte')))" 1959 by (simp add: mdb_node_lift_def canonical_address_sign_extended sign_extended_sign_extend) 1960 1961lemma canonical_address_mdbNext': 1962 "ccte_relation cte cte' \<Longrightarrow> canonical_address (mdbNext (cteMDBNode cte))" 1963 apply (rule rsubst[where P=canonical_address, OF canonical_address_mdbNext_CL]) 1964 apply (rule cmdb_node_relation_mdbNext) 1965 apply (erule ccte_relation_cmdbnode_relation) 1966 done 1967 1968lemma canonical_address_mdbNext: 1969 "\<lbrakk> (s, s') \<in> rf_sr; ctes_of s slot = Some cte \<rbrakk> \<Longrightarrow> canonical_address (mdbNext (cteMDBNode cte))" 1970 apply (drule cmap_relation_cte) 1971 apply (erule (1) cmap_relationE1) 1972 apply (erule canonical_address_mdbNext') 1973 done 1974 1975definition 1976 arch_cleanup_info_wf' :: "arch_capability \<Rightarrow> bool" 1977where 1978 "arch_cleanup_info_wf' acap \<equiv> case acap of IOPortCap f l \<Rightarrow> f \<le> l | _ \<Rightarrow> True" 1979 1980definition 1981 cleanup_info_wf' :: "capability \<Rightarrow> bool" 1982where 1983 "cleanup_info_wf' cap \<equiv> case cap of IRQHandlerCap irq \<Rightarrow> 1984 UCAST(8\<rightarrow>16) irq \<le> SCAST(32 signed\<rightarrow>16) Kernel_C.maxIRQ | ArchObjectCap acap \<Rightarrow> arch_cleanup_info_wf' acap | _ \<Rightarrow> True" 1985 1986(* FIXME: move *) 1987lemma hrs_mem_update_compose: 1988 "hrs_mem_update f (hrs_mem_update g h) = hrs_mem_update (f \<circ> g) h" 1989 by (auto simp: hrs_mem_update_def split: prod.split) 1990 1991(* FIXME: move *) 1992lemma packed_heap_update_collapse': 1993 fixes p :: "'a::packed_type ptr" 1994 shows "heap_update p v \<circ> heap_update p u = heap_update p v" 1995 by (auto simp: packed_heap_update_collapse) 1996 1997(* FIXME: move *) 1998lemma access_array_from_elements: 1999 fixes v :: "'a::packed_type['b::finite]" 2000 assumes "\<forall>i < CARD('b). h_val h (array_ptr_index p False i) = v.[i]" 2001 shows "h_val h p = v" 2002 by (rule cart_eq[THEN iffD2]) (simp add: assms heap_access_Array_element') 2003 2004(* FIXME: move *) 2005lemma h_val_foldr_heap_update: 2006 fixes v :: "'i \<Rightarrow> 'a::mem_type" 2007 assumes "\<forall>x y. {x,y} \<subseteq> set xs \<longrightarrow> x \<noteq> y \<longrightarrow> ptr_span (p x) \<inter> ptr_span (p y) = {}" 2008 assumes "distinct xs" "i \<in> set xs" 2009 shows "h_val (foldr (\<lambda>i. heap_update (p i) (v i)) xs h) (p i) = v i" 2010 using assms by (induct xs arbitrary: h; 2011 fastforce simp: h_val_heap_update h_val_update_regions_disjoint) 2012 2013(* FIXME: move *) 2014lemma ptr_span_array_ptr_index_disjoint: 2015 fixes p :: "('a::packed_type['b::finite]) ptr" 2016 assumes s: "CARD('b) * size_of TYPE('a) \<le> 2 ^ addr_bitsize" 2017 assumes b: "x < CARD('b)" "y < CARD('b)" 2018 assumes n: "x \<noteq> y" 2019 shows "ptr_span (array_ptr_index p False x) \<inter> ptr_span (array_ptr_index p False y) = {}" 2020 proof - 2021 have l: "CARD('b) * size_of TYPE('a) \<le> 2 ^ LENGTH(64)" using s by simp 2022 have p: "\<And>x k. x < CARD('b) \<Longrightarrow> k < size_of TYPE('a) 2023 \<Longrightarrow> x * size_of TYPE('a) + k < 2 ^ LENGTH(64)" 2024 by (metis less_le_trans[OF _ l] less_imp_not_less mod_lemma mult.commute nat_mod_lem neq0_conv) 2025 show ?thesis 2026 apply (clarsimp simp: array_ptr_index_def ptr_add_def intvl_disj_offset) 2027 apply (rule disjointI) 2028 apply (clarsimp simp: intvl_def) 2029 apply (subst (asm) of_nat_mult[symmetric])+ 2030 apply (subst (asm) of_nat_add[symmetric])+ 2031 apply (subst (asm) of_nat_inj[OF p p]; (simp add: b)?) 2032 apply (drule arg_cong[where f="\<lambda>x. x div size_of TYPE('a)"]; simp add: n) 2033 done 2034 qed 2035 2036(* FIXME: move *) 2037lemma h_val_heap_update_Array: 2038 fixes v :: "'a::packed_type['b::finite]" 2039 assumes s: "CARD('b) * size_of TYPE('a) \<le> 2 ^ addr_bitsize" 2040 shows "h_val (heap_update p v h) p = v" 2041 apply (rule access_array_from_elements) 2042 apply (clarsimp simp: heap_update_Array foldl_conv_foldr) 2043 apply (rule h_val_foldr_heap_update; clarsimp simp: ptr_span_array_ptr_index_disjoint[OF s]) 2044 done 2045 2046(* FIXME: move *) 2047lemma foldr_heap_update_commute: 2048 assumes "\<forall>y. y \<in> set xs \<longrightarrow> ptr_span q \<inter> ptr_span (p y) = {}" 2049 shows "foldr (\<lambda>i. heap_update (p i) (v i)) xs (heap_update q u h) 2050 = heap_update q u (foldr (\<lambda>i. heap_update (p i) (v i)) xs h)" 2051 using assms by (induct xs) (auto simp: LemmaBucket_C.heap_update_commute) 2052 2053(* FIXME: move *) 2054lemma foldr_packed_heap_update_collapse: 2055 fixes u v :: "'i \<Rightarrow> 'a::packed_type" 2056 assumes "\<forall>x y. {x,y} \<subseteq> set xs \<longrightarrow> y \<noteq> x \<longrightarrow> ptr_span (p x) \<inter> ptr_span (p y) = {}" 2057 assumes "distinct xs" 2058 shows "foldr (\<lambda>i. heap_update (p i) (v i)) xs (foldr (\<lambda>i. heap_update (p i) (u i)) xs h) 2059 = foldr (\<lambda>i. heap_update (p i) (v i)) xs h" 2060 using assms 2061 apply - 2062 apply (induct xs arbitrary: h; clarsimp; rename_tac x xs h) 2063 apply (drule_tac x=x in spec; clarsimp) 2064 apply (subst foldr_heap_update_commute; clarsimp simp: packed_heap_update_collapse) 2065 apply (drule_tac x=y in spec; clarsimp) 2066 done 2067 2068(* FIXME: move *) 2069lemma packed_Array_heap_update_collapse: 2070 fixes p :: "('a::packed_type['b::finite]) ptr" 2071 assumes s: "CARD('b) * size_of TYPE('a) \<le> 2 ^ addr_bitsize" 2072 shows "heap_update p v (heap_update p u h) = heap_update p v h" 2073 by (simp add: heap_update_Array foldl_conv_foldr foldr_packed_heap_update_collapse 2074 ptr_span_array_ptr_index_disjoint[OF s]) 2075 2076(* FIXME: move *) 2077lemma packed_Array_heap_update_collapse': 2078 fixes p :: "('a::packed_type['b::finite]) ptr" 2079 assumes s: "CARD('b) * size_of TYPE('a) \<le> 2 ^ addr_bitsize" 2080 shows "heap_update p v \<circ> heap_update p u = heap_update p v" 2081 by (auto simp: packed_Array_heap_update_collapse[OF s]) 2082 2083(* FIXME: move *) 2084definition 2085 heap_modify :: "'a::c_type ptr \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> heap_mem \<Rightarrow> heap_mem" 2086where 2087 "heap_modify p f \<equiv> \<lambda>h. heap_update p (f (h_val h p)) h" 2088 2089(* FIXME: move *) 2090lemma heap_modify_def2: 2091 "heap_modify (p::'a::c_type ptr) f \<equiv> 2092 \<lambda>h. let bytes = heap_list h (size_of TYPE('a)) (ptr_val p) in 2093 heap_update_list (ptr_val p) (to_bytes (f (from_bytes bytes)) bytes) h" 2094 by (simp add: heap_modify_def Let_def heap_update_def h_val_def) 2095 2096(* FIXME: move *) 2097lemma heap_modify_compose: 2098 fixes p :: "'a::packed_type ptr" 2099 shows "heap_modify p f \<circ> heap_modify p g = heap_modify p (f \<circ> g)" 2100 and "heap_modify p f (heap_modify p g h) = heap_modify p (f \<circ> g) h" 2101 by (auto simp: heap_modify_def h_val_heap_update packed_heap_update_collapse) 2102 2103(* FIXME: move *) 2104lemma heap_modify_compose_Array: 2105 fixes p :: "('a::packed_type['b::finite]) ptr" 2106 assumes s: "CARD('b) * size_of TYPE('a) \<le> 2 ^ addr_bitsize" 2107 shows "heap_modify p f \<circ> heap_modify p g = heap_modify p (f \<circ> g)" 2108 and "heap_modify p f (heap_modify p g h) = heap_modify p (f \<circ> g) h" 2109 by (auto simp: heap_modify_def h_val_heap_update_Array[OF s] 2110 packed_Array_heap_update_collapse[OF s]) 2111 2112(* FIXME: move *) 2113lemma fold_heap_modify_commute: 2114 fixes p :: "'a::packed_type ptr" 2115 shows "fold (heap_modify p \<circ> f) upds = heap_modify p (fold f upds)" 2116 apply (induction upds) 2117 apply (simp add: heap_modify_def heap_update_id) 2118 apply (clarsimp simp: heap_modify_compose[THEN fun_cong, simplified] o_def) 2119 done 2120 2121(* FIXME: move *) 2122lemma fold_heap_modify_commute_Array: 2123 fixes p :: "('a::packed_type['b::finite]) ptr" 2124 assumes s: "CARD('b) * size_of TYPE('a) \<le> 2 ^ addr_bitsize" 2125 shows "fold (heap_modify p \<circ> f) upds = heap_modify p (fold f upds)" 2126 apply (induction upds) 2127 apply (simp add: heap_modify_def heap_update_id_Array) 2128 apply (clarsimp simp: heap_modify_compose_Array[OF s, THEN fun_cong, simplified] o_def) 2129 done 2130 2131(* FIXME: move *) 2132lemma msb_le_mono: 2133 fixes v w :: "'a::len word" 2134 shows "v \<le> w \<Longrightarrow> msb v \<Longrightarrow> msb w" 2135 by (simp add: msb_big) 2136 2137(* FIXME: move *) 2138lemma neg_msb_le_mono: 2139 fixes v w :: "'a::len word" 2140 shows "v \<le> w \<Longrightarrow> \<not> msb w \<Longrightarrow> \<not> msb v" 2141 by (simp add: msb_big) 2142 2143(* FIXME: move *) 2144lemmas msb_less_mono = msb_le_mono[OF less_imp_le] 2145lemmas neg_msb_less_mono = neg_msb_le_mono[OF less_imp_le] 2146 2147(* FIXME: move *) 2148lemma word_sless_iff_less: 2149 "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <s w \<longleftrightarrow> v < w" 2150 by (simp add: word_sless_alt sint_eq_uint word_less_alt) 2151 2152(* FIXME: move *) 2153lemmas word_sless_imp_less = word_sless_iff_less[THEN iffD1, rotated 2] 2154lemmas word_less_imp_sless = word_sless_iff_less[THEN iffD2, rotated 2] 2155 2156(* FIXME: move *) 2157lemma word_sle_iff_le: 2158 "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <=s w \<longleftrightarrow> v \<le> w" 2159 by (simp add: word_sle_def sint_eq_uint word_le_def) 2160 2161(* FIXME: move *) 2162lemmas word_sle_imp_le = word_sle_iff_le[THEN iffD1, rotated 2] 2163lemmas word_le_imp_sle = word_sle_iff_le[THEN iffD2, rotated 2] 2164 2165(* FIXME: move to Word_Lib *) 2166lemma word_upcast_shiftr: 2167 assumes "LENGTH('a::len) \<le> LENGTH('b::len)" 2168 shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n" 2169 apply (intro word_eqI impI iffI; clarsimp simp: word_size nth_shiftr nth_ucast) 2170 apply (drule test_bit_size) 2171 using assms by (simp add: word_size) 2172 2173lemma word_upcast_neg_msb: 2174 "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w)" 2175 apply (clarsimp simp: ucast_def msb_word_of_int) 2176 apply (drule bin_nth_uint_imp) 2177 by simp 2178 2179(* FIXME: move to Word_Lib *) 2180lemma word_upcast_0_sle: 2181 "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w" 2182 by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb]) 2183 2184(* FIXME: move to Word_Lib *) 2185lemma scast_ucast_up_eq_ucast: 2186 assumes "LENGTH('a::len) < LENGTH('b::len)" 2187 shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w" 2188 using assms 2189 apply (subst scast_eq_ucast; simp) 2190 apply (clarsimp simp: ucast_def msb_word_of_int) 2191 apply (drule bin_nth_uint_imp) 2192 apply simp 2193 done 2194 2195lemma not_max_word_iff_less: 2196 "w \<noteq> max_word \<longleftrightarrow> w < max_word" 2197 by (simp add: order_less_le) 2198 2199lemma ucast_increment: 2200 assumes "w \<noteq> max_word" 2201 shows "UCAST('a::len \<rightarrow> 'b::len) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)" 2202 apply (cases "LENGTH('b) \<le> LENGTH('a)") 2203 apply (simp add: ucast_down_add is_down) 2204 apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('a)") 2205 apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('b)") 2206 apply (subst word_uint_eq_iff) 2207 apply (simp add: uint_arith_simps uint_up_ucast is_up) 2208 apply (erule less_trans, rule power_strict_increasing, simp, simp) 2209 apply (subst less_diff_eq[symmetric]) 2210 using assms 2211 apply (simp add: not_max_word_iff_less word_less_alt) 2212 apply (erule less_le_trans) 2213 apply (simp add: max_word_def) 2214 done 2215 2216lemma max_word_gt_0: 2217 "0 < max_word" 2218 by (simp add: le_neq_trans[OF max_word_max] max_word_not_0) 2219 2220lemma and_not_max_word: 2221 "m \<noteq> max_word \<Longrightarrow> w && m \<noteq> max_word" 2222 by (simp add: not_max_word_iff_less word_and_less') 2223 2224lemma mask_not_max_word: 2225 "m < LENGTH('a::len) \<Longrightarrow> mask m \<noteq> (max_word :: 'a word)" 2226 by (metis shiftl_1_not_0 shiftl_mask_is_0 word_bool_alg.conj_one_right) 2227 2228lemmas and_mask_not_max_word = 2229 and_not_max_word[OF mask_not_max_word] 2230 2231lemma shiftr_not_max_word: 2232 "0 < n \<Longrightarrow> w >> n \<noteq> max_word" 2233 apply (simp add: not_max_word_iff_less) 2234 apply (cases "n < size w") 2235 apply (cases "w = 0") 2236 apply (simp add: max_word_gt_0) 2237 apply (subst shiftr_div_2n_w, assumption) 2238 apply (rule less_le_trans[OF div_less_dividend_word max_word_max]) 2239 apply simp 2240 apply (metis word_size_gt_0 less_numeral_extra(3) mask_def nth_mask power_0 shiftl_t2n) 2241 apply (simp add: not_less word_size) 2242 apply (subgoal_tac "w >> n = 0"; simp add: max_word_gt_0 shiftr_eq_0) 2243 done 2244 2245lemma word_sandwich1: 2246 fixes a b c :: "'a::len word" 2247 assumes "a < b" 2248 assumes "b <= c" 2249 shows "0 < b - a \<and> b - a <= c" 2250 using assms diff_add_cancel order_less_irrefl add_0 word_le_imp_diff_le 2251 word_le_less_eq word_neq_0_conv 2252 by metis 2253 2254lemma word_sandwich2: 2255 fixes a b :: "'a::len word" 2256 assumes "0 < a" 2257 assumes "a <= b" 2258 shows "b - a < b" 2259 using assms less_le_trans word_diff_less 2260 by blast 2261 2262lemma make_pattern_spec: 2263 defines "bits \<equiv> 0x40 :: 32 sword" 2264 notes word_less_imp_less_0 = revcut_rl[OF word_less_imp_sless[OF _ word_msb_0]] 2265 notes word_le_imp_le_0 = revcut_rl[OF word_le_imp_sle[OF _ word_msb_0]] 2266 shows 2267 "\<forall>\<sigma>. \<Gamma> \<turnstile> 2268 {s. s = \<sigma> \<and> start___int_' s < end___int_' s 2269 \<and> end___int_' s \<le> bits } 2270 Call make_pattern_'proc 2271 {t. ret__unsigned_long_' t = 2272 mask (unat (end___int_' \<sigma>)) && ~~ mask (unat (start___int_' \<sigma>))}" 2273 apply (rule allI, rule conseqPre, hoare_rule HoarePartial.ProcNoRec1, vcg, clarsimp) 2274 apply (fold bits_def) 2275 subgoal for \<sigma> 2276 apply (frule (1) word_sandwich1[of "start___int_' \<sigma>" "end___int_' \<sigma>" bits]; clarsimp) 2277 apply (frule (1) word_sandwich2[of "end___int_' \<sigma> - start___int_' \<sigma>" bits]) 2278 apply (subgoal_tac "\<not> msb bits") 2279 prefer 2 subgoal by (simp add: bits_def) 2280 apply (frule (1) neg_msb_le_mono[of "end___int_' \<sigma>"]) 2281 apply (frule (1) neg_msb_less_mono[of "start___int_' \<sigma>"]) 2282 apply (frule (1) neg_msb_le_mono[of "end___int_' \<sigma> - start___int_' \<sigma>"]) 2283 apply (frule (1) neg_msb_less_mono[of "bits - (end___int_' \<sigma> - start___int_' \<sigma>)"]) 2284 apply (rule word_le_imp_le_0[of "start___int_' \<sigma>"], simp, simp) 2285 apply (frule (2) word_less_imp_sless[of "start___int_' \<sigma>" "end___int_' \<sigma>"]) 2286 apply (frule (2) word_le_imp_sle[of "end___int_' \<sigma>" bits]) 2287 apply (rule word_less_imp_less_0[of "end___int_' \<sigma> - start___int_' \<sigma>"], simp, simp) 2288 apply (frule (2) word_le_imp_sle[of "end___int_' \<sigma> - start___int_' \<sigma>" bits]) 2289 apply (rule word_le_imp_le_0[of "bits - (end___int_' \<sigma> - start___int_' \<sigma>)"], simp, simp) 2290 apply (frule (2) word_less_imp_sless[of "bits - (end___int_' \<sigma> - start___int_' \<sigma>)" bits]) 2291 apply (intro conjI; (fastforce simp: word_sle_def word_sless_def bits_def | simp)?) 2292 apply (subgoal_tac "start___int_' \<sigma> \<le> bits - (end___int_' \<sigma> - start___int_' \<sigma>)") 2293 prefer 2 2294 apply (meson le_minus_minus order.strict_implies_order order_trans word_le_minus_mono_left) 2295 apply (simp add: shiftr_shiftl1 word_le_nat_alt[symmetric] unat_sub[symmetric] max_word_mask) 2296 apply (subst shiftr_mask2, simp) 2297 apply (simp add: unat_sub word_le_nat_alt bits_def) 2298 done 2299 done 2300 2301definition 2302 word_set_or_clear :: "bool \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word" 2303where 2304 "word_set_or_clear s p w \<equiv> if s then w || p else w && ~~ p" 2305 2306lemma apply_pattern_spec: 2307 "\<forall>\<sigma>. \<Gamma> \<turnstile> 2308 {s. s = \<sigma> \<and> s \<Turnstile>\<^sub>c w___ptr_to_unsigned_long_' \<sigma>} 2309 Call apply_pattern_'proc 2310 {globals_update 2311 (t_hrs_'_update 2312 (hrs_mem_update 2313 (heap_update (w___ptr_to_unsigned_long_' \<sigma>) 2314 (word_set_or_clear (to_bool (set_' \<sigma>)) 2315 (pattern_' \<sigma>) 2316 (h_val (hrs_mem (t_hrs_' (globals \<sigma>))) 2317 (w___ptr_to_unsigned_long_' \<sigma>)))))) \<sigma>}" 2318 apply (rule allI, rule conseqPre, hoare_rule HoarePartial.ProcNoRec1, vcg) 2319 apply (clarsimp simp: word_set_or_clear_def to_bool_def) 2320 done 2321 2322(* FIXME: move *) 2323lemma whileAnno_subst_invariant: 2324 "whileAnno b I' V c = whileAnno b I V c" 2325 by (simp add: whileAnno_def) 2326 2327abbreviation 2328 ioport_table_ptr_coerce :: "'a ptr \<Rightarrow> ioport_table_C ptr" 2329where 2330 "ioport_table_ptr_coerce \<equiv> ptr_coerce" 2331 2332lemma hoarep_conseq_spec_state: 2333 fixes \<Gamma> :: "'p \<Rightarrow> ('s,'p,'f) com option" 2334 assumes "\<forall>\<sigma>. \<Gamma> \<turnstile> {s. s = \<sigma> \<and> P s} c (Q \<sigma>)" 2335 assumes "\<forall>\<sigma>. \<sigma> \<in> P' \<longrightarrow> P \<sigma> \<and> Q \<sigma> \<subseteq> Q'" 2336 shows "\<Gamma> \<turnstile> P' c Q'" 2337 using assms by (fastforce intro: hoarep.Conseq) 2338 2339lemma hrs_simps: 2340 "hrs_mem (mem, htd) = mem" 2341 "hrs_mem_update f (mem, htd) = (f mem, htd)" 2342 "hrs_htd (mem, htd) = htd" 2343 "hrs_htd_update g (mem, htd) = (mem, g htd)" 2344 by (auto simp: hrs_mem_def hrs_mem_update_def hrs_htd_def hrs_htd_update_def) 2345 2346lemma clift_heap_modify_same: 2347 fixes p :: "'a :: mem_type ptr" 2348 assumes "hrs_htd hp \<Turnstile>\<^sub>t p" 2349 assumes "typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b)" 2350 shows "clift (hrs_mem_update (heap_modify p f) hp) = (clift hp :: 'b :: mem_type typ_heap)" 2351 using assms unfolding hrs_mem_update_def 2352 apply (cases hp) 2353 apply (simp add: split_def hrs_htd_def heap_modify_def) 2354 apply (erule lift_t_heap_update_same) 2355 apply simp 2356 done 2357 2358lemma zero_ranges_are_zero_modify[simp]: 2359 "h_t_valid (hrs_htd hrs) c_guard (ptr :: 'a ptr) 2360 \<Longrightarrow> typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8) 2361 \<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_modify ptr f) hrs) 2362 = zero_ranges_are_zero rs hrs" 2363 apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update 2364 intro!: ball_cong[OF refl] conj_cong[OF refl]) 2365 apply (drule region_actually_is_bytes) 2366 apply (drule(2) region_is_bytes_disjoint) 2367 apply (simp add: heap_modify_def heap_update_def heap_list_update_disjoint_same Int_commute) 2368 done 2369 2370lemma h_val_heap_modify: 2371 fixes p :: "'a::mem_type ptr" 2372 shows "h_val (heap_modify p f h) p = f (h_val h p)" 2373 by (simp add: heap_modify_def h_val_heap_update) 2374 2375lemma array_fupdate_index: 2376 fixes arr :: "'a::c_type['b::finite]" 2377 assumes "i < CARD('b)" "j < CARD('b)" 2378 shows "fupdate i f arr.[j] = (if i = j then f (arr.[i]) else arr.[j])" 2379 using assms by (cases "i = j"; simp add: fupdate_def) 2380 2381lemma foldl_map_pair_constant: 2382 "foldl (\<lambda>acc p. f acc (fst p) (snd p)) z (map (\<lambda>x. (x,v)) xs) = foldl (\<lambda>acc x. f acc x v) z xs" 2383 by (induct xs arbitrary: z) auto 2384 2385lemma word_set_or_clear_test_bit: 2386 fixes w :: "'a::len word" 2387 shows "i < LENGTH('a) \<Longrightarrow> word_set_or_clear b p w !! i = (if p !! i then b else w !! i)" 2388 by (auto simp: word_set_or_clear_def word_ops_nth_size word_size split: if_splits) 2389 2390lemma unat_and_mask_less_2p: 2391 fixes w :: "'a::len word" 2392 shows "m < LENGTH('a) \<Longrightarrow> unat (w && mask m) < 2 ^ m" 2393 by (simp add: unat_less_helper and_mask_less') 2394 2395lemma unat_shiftr_less_2p: 2396 fixes w :: "'a::len word" 2397 shows "n + m = LENGTH('a) \<Longrightarrow> unat (w >> n) < 2 ^ m" 2398 by (cases "n = 0"; simp add: unat_less_helper shiftr_less_t2n3) 2399 2400lemma nat_div_less_mono: 2401 fixes m n :: nat 2402 shows "m div d < n div d \<Longrightarrow> m < n" 2403 by (meson div_le_mono not_less) 2404 2405lemma word_shiftr_less_mono: 2406 fixes w :: "'a::len word" 2407 shows "w >> n < v >> n \<Longrightarrow> w < v" 2408 by (auto simp: word_less_nat_alt shiftr_div_2n' elim: nat_div_less_mono) 2409 2410lemma word_shiftr_less_mask: 2411 fixes w :: "'a::len word" 2412 shows "(w >> n < v >> n) \<longleftrightarrow> (w && ~~mask n < v && ~~mask n)" 2413 by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less) 2414 2415lemma word_shiftr_le_mask: 2416 fixes w :: "'a::len word" 2417 shows "(w >> n \<le> v >> n) \<longleftrightarrow> (w && ~~mask n \<le> v && ~~mask n)" 2418 by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less) 2419 2420lemma word_shiftr_eq_mask: 2421 fixes w :: "'a::len word" 2422 shows "(w >> n = v >> n) \<longleftrightarrow> (w && ~~mask n = v && ~~mask n)" 2423 by (metis (mono_tags) mask_shift shiftr_eq_neg_mask_eq) 2424 2425lemmas word_shiftr_cmp_mask = 2426 word_shiftr_less_mask word_shiftr_le_mask word_shiftr_eq_mask 2427 2428lemma fold_array_update_index: 2429 fixes arr :: "'a::c_type['b::finite]" 2430 assumes "i < CARD('b)" 2431 shows "fold (\<lambda>i arr. Arrays.update arr i (f i)) is arr.[i] = (if i \<in> set is then f i else arr.[i])" 2432 using assms by (induct "is" arbitrary: arr) (auto split: if_splits) 2433 2434lemma if_if_if_same_output: 2435 "(if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \<and> c2 \<or> \<not>c1 \<and> c3 then t else f)" 2436 by (simp split: if_splits) 2437 2438lemma word_le_split_mask: 2439 "(w \<le> v) \<longleftrightarrow> (w >> n < v >> n \<or> w >> n = v >> n \<and> w && mask n \<le> v && mask n)" 2440 apply (simp add: word_shiftr_eq_mask word_shiftr_less_mask) 2441 apply (rule subst[where P="\<lambda>c. c \<le> d = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]]) 2442 apply (rule subst[where P="\<lambda>c. d \<le> c = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]]) 2443 apply (rule iffI) 2444 apply safe 2445 apply (fold_subgoals (prefix))[2] 2446 apply (subst atomize_conj) 2447 apply (rule context_conjI) 2448 apply (metis AND_NOT_mask_plus_AND_mask_eq neg_mask_mono_le word_le_less_eq) 2449 apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_4) 2450 apply (metis Groups.add_ac(2) neg_mask_mono_le word_le_less_eq word_not_le word_plus_and_or_coroll2) 2451 apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_3) 2452 done 2453 2454lemma heap_modify_fold: 2455 "heap_update p (f (h_val h p)) h = heap_modify p f h" 2456 by (simp add: heap_modify_def) 2457 2458lemma t_hrs_'_update_heap_modify_fold: 2459 "gs\<lparr> t_hrs_' := hrs_mem_update (heap_update p (f (h_val (hrs_mem (t_hrs_' gs)) p))) (t_hrs_' gs) \<rparr> 2460 = t_hrs_'_update (hrs_mem_update (heap_modify p f)) gs" 2461 by (clarsimp simp: heap_modify_def hrs_mem_update_def hrs_mem_def split: prod.splits) 2462 2463lemma heap_modify_Array_element: 2464 fixes p :: "'a::packed_type ptr" 2465 fixes p' :: "('a['b::finite]) ptr" 2466 assumes "p = ptr_coerce p' +\<^sub>p int n" 2467 assumes "n < CARD('b)" 2468 assumes "CARD('b) * size_of TYPE('a) < 2 ^ addr_bitsize" 2469 shows "heap_modify p f = heap_modify p' (fupdate n f)" 2470 using assms by (simp add: heap_access_Array_element heap_update_Array_element' 2471 heap_modify_def fupdate_def) 2472 2473lemma fupdate_word_set_or_clear_max_word: 2474 "fupdate i (word_set_or_clear b max_word) arr = Arrays.update arr i (if b then max_word else 0)" 2475 by (simp add: fupdate_def word_set_or_clear_def) 2476 2477lemma h_t_valid_Array_element': 2478 "\<lbrakk> htd \<Turnstile>\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); 0 \<le> n; n < CARD('b) \<rbrakk> 2479 \<Longrightarrow> htd \<Turnstile>\<^sub>t ((ptr_coerce p :: 'a ptr) +\<^sub>p n)" 2480 apply (drule_tac n="nat n" and coerce=False in h_t_valid_Array_element') 2481 apply simp 2482 apply (simp add: array_ptr_index_def) 2483 done 2484 2485lemma setIOPortMask_spec: 2486 notes ucast_mask = ucast_and_mask[where n=6, simplified mask_def, simplified] 2487 notes not_max_word_simps = and_not_max_word shiftr_not_max_word and_mask_not_max_word 2488 notes ucast_cmp_ucast = ucast_le_ucast ucast_less_ucast 2489 notes array_assert = array_assertion_shrink_right[OF array_ptr_valid_array_assertionD] 2490 notes word_unat.Rep_inject[simp del] 2491 shows 2492 "\<forall>\<sigma>. \<Gamma> \<turnstile> 2493 {s. s = \<sigma> \<and> low_' s \<le> high_' s \<and> s \<Turnstile>\<^sub>c ioport_table_ptr_coerce (ioport_bitmap_' s)} 2494 Call setIOPortMask_'proc 2495 {t. globals t = t_hrs_'_update 2496 (hrs_mem_update 2497 (heap_modify 2498 (ioport_table_ptr_coerce (ioport_bitmap_' \<sigma>)) 2499 (let low_word = low_' \<sigma> >> wordRadix; 2500 high_word = high_' \<sigma> >> wordRadix; 2501 low_mask = ~~ mask (unat (low_' \<sigma> && mask wordRadix)); 2502 high_mask = mask (Suc (unat (high_' \<sigma> && mask wordRadix))); 2503 b = to_bool (set_' \<sigma>) in 2504 if low_word = high_word 2505 then fupdate (unat low_word) (word_set_or_clear b (high_mask && low_mask)) 2506 else fupdate (unat high_word) (word_set_or_clear b high_mask) 2507 \<circ> fold (\<lambda>i arr. Arrays.update arr i (if b then max_word else 0)) 2508 ([Suc (unat low_word) ..< unat high_word]) 2509 \<circ> fupdate (unat low_word) (word_set_or_clear b low_mask)))) 2510 (globals \<sigma>)}" 2511 apply (rule allI) 2512 apply (hoare_rule HoarePartial.ProcNoRec1) 2513 apply (simp add: scast_ucast_up_eq_ucast word_upcast_shiftr[symmetric] ucast_mask[symmetric] 2514 word_upcast_0_sle) 2515 apply (rule ssubst[where P="\<lambda>c. hoarep \<Gamma> {} {} P (Catch (c1;; (Cond b c2 (c3;; c;; c4;; c5))) Skip) Q A" 2516 for P c1 b c2 c3 c4 c5 Q A], 2517 rule_tac I="{s. s \<Turnstile>\<^sub>c ioport_table_ptr_coerce (bitmap_' s) 2518 \<and> bitmap_' s = ptr_coerce (ioport_bitmap_' \<sigma>) 2519 \<and> ucast (low_' \<sigma> >> wordRadix) < low_word_' s 2520 \<and> low_word_' s <= high_word_' s 2521 \<and> high_word_' s = ucast (high_' \<sigma> >> wordRadix) 2522 \<and> high_index_' s = ucast (high_' \<sigma> && mask wordRadix) 2523 \<and> set_' s = set_' \<sigma> 2524 \<and> globals s = t_hrs_'_update 2525 (hrs_mem_update 2526 (heap_modify 2527 (ioport_table_ptr_coerce (ioport_bitmap_' \<sigma>)) 2528 (fold (\<lambda>i arr. Arrays.update arr i (if to_bool (set_' \<sigma>) then max_word else 0)) 2529 ([Suc (unat (low_' \<sigma> >> wordRadix)) ..< unat (low_word_' s)]) 2530 \<circ> fupdate 2531 (unat (low_' \<sigma> >> wordRadix)) 2532 (word_set_or_clear 2533 (to_bool (set_' \<sigma>)) 2534 (~~ mask (unat (low_' \<sigma> && mask wordRadix))))))) 2535 (globals \<sigma>)}" 2536 in whileAnno_subst_invariant) 2537 apply (rule conseqPre, vcg) 2538 apply (all \<open>clarsimp simp: Let_def wordRadix_def hrs_simps is_up is_down 2539 unat_ucast_upcast uint_up_ucast sint_ucast_eq_uint up_ucast_inj_eq 2540 not_max_word_simps[THEN ucast_increment, simplified max_word_def] 2541 ucast_cmp_ucast ucast_cmp_ucast[where 'a=16 and y="0x40", simplified] 2542 heap_modify_fold t_hrs_'_update_heap_modify_fold 2543 cong: conj_cong\<close>) 2544 subgoal for mem htd ioport_bitmap high set low low_word 2545 (* Loop invariant is preserved. *) 2546 apply (frule neg_msb_le_mono[OF _ word_upcast_neg_msb]; 2547 simp add: word_sless_iff_less[OF _ word_upcast_neg_msb] sint_eq_uint unat_arith_simps) 2548 apply (frule less_trans[OF _ unat_shiftr_less_2p[where m=10]]; simp) 2549 apply (frule h_t_valid_Array_element[where n="uint low_word"]; 2550 simp add: uint_nat heap_modify_compose o_def fupdate_word_set_or_clear_max_word 2551 heap_modify_Array_element[where 'b=1024 and p'="ptr_coerce ioport_bitmap"]) 2552 apply (clarsimp elim!: array_assertion_shrink_right dest!: array_ptr_valid_array_assertionD) 2553 done 2554 subgoal for mem htd ioport_bitmap high set low low_word 2555 (* Invariant plus loop termination condition is sufficient to establish VCG postcondition. *) 2556 apply (frule neg_msb_le_mono[OF _ word_upcast_neg_msb]; 2557 simp add: word_sless_iff_less[OF _ word_upcast_neg_msb] sint_eq_uint unat_arith_simps) 2558 apply (cut_tac unat_and_mask_less_2p[of 6 high]; simp) 2559 apply (cut_tac unat_shiftr_less_2p[of 6 10 high]; simp) 2560 apply (frule h_t_valid_Array_element[where n="uint low_word"]; 2561 simp add: uint_nat heap_modify_compose o_def fupdate_word_set_or_clear_max_word 2562 heap_modify_Array_element[where 'b=1024 and p'="ptr_coerce ioport_bitmap"]) 2563 apply (clarsimp elim!: array_assertion_shrink_right dest!: array_ptr_valid_array_assertionD) 2564 done 2565 subgoal for \<sigma>' 2566 (* VCG precondition is sufficient to establish loop invariant. *) 2567 apply (frule word_le_split_mask[where n=6, THEN iffD1]) 2568 apply (simp add: unat_arith_simps) 2569 apply (cut_tac unat_shiftr_less_2p[of 6 10 "low_' \<sigma>'"]; simp) 2570 apply (cut_tac unat_shiftr_less_2p[of 6 10 "high_' \<sigma>'"]; simp) 2571 apply (cut_tac unat_and_mask_less_2p[of 6 "low_' \<sigma>'"]; simp) 2572 apply (cut_tac unat_and_mask_less_2p[of 6 "high_' \<sigma>'"]; simp) 2573 apply (simp add: uint_nat mask_def[where n=6] mask_def[where n=64] less_Suc_eq_le Suc_le_eq 2574 heap_modify_Array_element[where 'b=1024 and p'="ptr_coerce (ioport_bitmap_' \<sigma>')"]) 2575 apply (frule h_t_valid_Array_element[where n="uint (low_' \<sigma>' >> 6)"]; simp add: uint_nat) 2576 apply (frule h_t_valid_Array_element[where n="uint (high_' \<sigma>' >> 6)"]; simp add: uint_nat) 2577 apply (frule array_assert[where n'="unat (low_' \<sigma>' >> 6)"]; simp) 2578 apply (frule array_assert[where n'="unat (high_' \<sigma>' >> 6)"]; simp) 2579 by auto 2580 done 2581 2582lemma setIOPortMask_ccorres: 2583 notes Collect_const[simp del] 2584 shows 2585 "ccorres dc xfdc 2586 (\<lambda>_. f \<le> l) 2587 (UNIV \<inter> \<lbrace>\<acute>ioport_bitmap = Ptr (symbol_table ''x86KSAllocatedIOPorts'')\<rbrace> 2588 \<inter> \<lbrace>\<acute>low = f\<rbrace> 2589 \<inter> \<lbrace>\<acute>high = l\<rbrace> 2590 \<inter> \<lbrace>\<acute>set = from_bool b\<rbrace>) hs 2591 (setIOPortMask f l b) 2592 (Call setIOPortMask_'proc)" 2593 apply (intro ccorres_from_vcg hoarep_conseq_spec_state[OF setIOPortMask_spec] allI) 2594 apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def 2595 global_ioport_bitmap_relation_def2 2596 setIOPortMask_def gets_def get_def modify_def put_def 2597 monad_simps in_monad 2598 hrs_mem_update h_val_heap_modify 2599 clift_heap_modify_same tag_disj_via_td_name 2600 cpspace_relation_def carch_globals_def cmachine_state_relation_def 2601 fpu_null_state_relation_def) 2602 apply (match premises in H: \<open>cioport_bitmap_to_H _ = _\<close> and O: \<open>low_' s \<le> high_' s\<close> for s 2603 \<Rightarrow> \<open>match premises in _[thin]: _(multi) \<Rightarrow> \<open>insert O H\<close>\<close>) 2604 apply (clarsimp simp: cioport_bitmap_to_H_def wordRadix_def, rule ext, drule_tac x=port in fun_cong) 2605 apply (clarsimp simp: foldl_map_pair_constant foldl_fun_upd_value) 2606 apply (rule ssubst[where P="\<lambda>f. test_bit f i = e" for e i, OF if_distrib[where f="\<lambda>c. c v.[i]" for v i]]) 2607 apply (simp add: array_fupdate_index fold_array_update_index word_set_or_clear_test_bit 2608 if_distrib[where f="\<lambda>c. test_bit c i" for i] word_ops_nth_size word_size 2609 unat_shiftr_less_2p[of 6 10, simplified] unat_and_mask_less_2p[of 6, simplified] 2610 less_Suc_eq_le Suc_le_eq not_less unat_arith_simps(1,2)[symmetric] 2611 if_if_same_output if_if_if_same_output) 2612 apply (thin_tac "_ = _") 2613 apply (rule if_weak_cong) 2614 apply (rule ssubst[OF word_le_split_mask[where n=6], where P="\<lambda>f. e \<longleftrightarrow> f \<and> c" for e c]) 2615 apply (rule ssubst[OF word_le_split_mask[where n=6], where P="\<lambda>f. e \<longleftrightarrow> c \<and> f" for e c]) 2616 apply (drule word_le_split_mask[where n=6, THEN iffD1]) 2617 by auto 2618 2619lemma freeIOPortRange_ccorres: 2620 "ccorres dc xfdc (\<top> and (\<lambda>s. f \<le> l)) 2621 (UNIV \<inter> {s. first_port_' s = f} \<inter> {s. last_port_' s = l}) hs 2622 (freeIOPortRange f l) 2623 (Call freeIOPortRange_'proc)" 2624 apply (cinit lift: first_port_' last_port_') 2625 apply (rule ccorres_Guard) 2626 apply (ctac add: setIOPortMask_ccorres) 2627 by (clarsimp simp: false_def rf_sr_def cstate_relation_def Let_def carch_state_relation_def 2628 global_ioport_bitmap_relation_def typ_heap_simps 2629 split: if_splits) 2630 2631lemma Arch_postCapDeletion_ccorres: 2632 "ccorres dc xfdc 2633 (\<top> and (\<lambda>s. arch_cleanup_info_wf' acap)) 2634 (UNIV \<inter> {s. ccap_relation (ArchObjectCap acap) (cap_' s)}) hs 2635 (X64_H.postCapDeletion acap) 2636 (Call Arch_postCapDeletion_'proc)" 2637 apply (cinit lift: cap_') 2638 apply csymbr 2639 apply (wpc; clarsimp simp: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs; ccorres_rewrite) 2640 prefer 3 (* IOPort case *) 2641 apply (rule ccorres_rhs_assoc)+ 2642 apply csymbr+ 2643 apply (ctac add: freeIOPortRange_ccorres[simplified dc_def]) 2644 apply (rule ccorres_return_Skip[simplified dc_def])+ 2645 apply (clarsimp simp: arch_cleanup_info_wf'_def split: arch_capability.splits) 2646 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2647 by (clarsimp simp: ccap_relation_def cap_io_port_cap_lift cap_to_H_def) 2648 2649lemma not_irq_or_arch_cap_case: 2650 "\<lbrakk>\<not>isIRQHandlerCap cap; \<not> isArchCap \<top> cap\<rbrakk> \<Longrightarrow> 2651 (case cap of IRQHandlerCap irq \<Rightarrow> f irq | ArchObjectCap acap \<Rightarrow> g acap | _ \<Rightarrow> h) = h" 2652 by (case_tac cap; clarsimp simp: isCap_simps) 2653 2654lemma postCapDeletion_ccorres: 2655 "cleanup_info_wf' cap \<Longrightarrow> 2656 ccorres dc xfdc 2657 \<top> (UNIV \<inter> {s. ccap_relation cap (cap_' s)}) hs 2658 (postCapDeletion cap) 2659 (Call postCapDeletion_'proc)" 2660 supply Collect_const[simp del] 2661 apply (cinit lift: cap_' simp: Retype_H.postCapDeletion_def) 2662 apply csymbr 2663 apply (clarsimp simp: cap_get_tag_isCap) 2664 apply (rule ccorres_Cond_rhs) 2665 apply (clarsimp simp: isCap_simps ) 2666 apply (rule ccorres_symb_exec_r) 2667 apply (rule_tac xf'=irq_' in ccorres_abstract, ceqv) 2668 apply (rule_tac P="rv' = ucast (capIRQ cap)" in ccorres_gen_asm2) 2669 apply (fold dc_def) 2670 apply (frule cap_get_tag_to_H, solves \<open>clarsimp simp: cap_get_tag_isCap_unfolded_H_cap\<close>) 2671 apply (clarsimp simp: cap_irq_handler_cap_lift) 2672 apply (ctac(no_vcg) add: deletedIRQHandler_ccorres) 2673 apply vcg 2674 apply (rule conseqPre, vcg) 2675 apply clarsimp 2676 apply csymbr 2677 apply (clarsimp simp: cap_get_tag_isCap) 2678 apply (rule ccorres_Cond_rhs) 2679 apply (wpc; clarsimp simp: isCap_simps) 2680 apply (ctac(no_vcg) add: Arch_postCapDeletion_ccorres[unfolded dc_def]) 2681 apply (simp add: not_irq_or_arch_cap_case) 2682 apply (rule ccorres_return_Skip[unfolded dc_def])+ 2683 apply clarsimp 2684 apply (rule conjI, clarsimp simp: isCap_simps Kernel_C.maxIRQ_def) 2685 apply (frule cap_get_tag_isCap_unfolded_H_cap(5)) 2686 apply (clarsimp simp: cap_irq_handler_cap_lift ccap_relation_def cap_to_H_def 2687 cleanup_info_wf'_def maxIRQ_def Kernel_C.maxIRQ_def) 2688 apply word_bitwise 2689 apply (rule conjI, clarsimp simp: isCap_simps cleanup_info_wf'_def) 2690 apply (rule conjI[rotated], clarsimp simp: isCap_simps) 2691 apply (clarsimp simp: isCap_simps) 2692 apply (frule cap_get_tag_isCap_unfolded_H_cap(5)) 2693 apply (clarsimp simp: cap_irq_handler_cap_lift ccap_relation_def cap_to_H_def 2694 cleanup_info_wf'_def c_valid_cap_def cl_valid_cap_def mask_def) 2695 done 2696 2697lemma emptySlot_ccorres: 2698 "ccorres dc xfdc 2699 (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero') 2700 (UNIV \<inter> {s. slot_' s = Ptr slot} 2701 \<inter> {s. ccap_relation info (cleanupInfo_' s) \<and> cleanup_info_wf' info} ) 2702 [] 2703 (emptySlot slot info) 2704 (Call emptySlot_'proc)" 2705 apply (cinit lift: slot_' cleanupInfo_' simp: case_Null_If) 2706 2707 \<comment> \<open>--- handle the clearUntypedFreeIndex\<close> 2708 apply (rule ccorres_split_noop_lhs, rule clearUntypedFreeIndex_noop_ccorres) 2709 2710 \<comment> \<open>--- instruction: newCTE \<leftarrow> getCTE slot; ---\<close> 2711 apply (rule ccorres_pre_getCTE) 2712 \<comment> \<open>--- instruction: CALL on C side\<close> 2713 apply (rule ccorres_move_c_guard_cte) 2714 apply csymbr 2715 apply (rule ccorres_abstract_cleanup) 2716 apply (rename_tac cap_tag) 2717 apply (rule_tac P="(cap_tag = scast cap_null_cap) 2718 = (cteCap newCTE = NullCap)" in ccorres_gen_asm2) 2719 apply (simp del: Collect_const) 2720 2721 \<comment> \<open>--- instruction: if-then-else / IF-THEN-ELSE\<close> 2722 apply (rule ccorres_cond2'[where R=\<top>]) 2723 2724 \<comment> \<open>*** link between abstract and concrete conditionals ***\<close> 2725 apply (clarsimp split: if_split) 2726 2727 \<comment> \<open>*** proof for the 'else' branch (return () and SKIP) ***\<close> 2728 prefer 2 2729 apply (ctac add: ccorres_return_Skip[unfolded dc_def]) 2730 2731 \<comment> \<open>*** proof for the 'then' branch ***\<close> 2732 2733 \<comment> \<open>---instructions: multiple on C side, including mdbNode fetch\<close> 2734 apply (rule ccorres_rhs_assoc)+ 2735 \<comment> \<open>we have to do it here because the first assoc did not apply inside the then block\<close> 2736 apply (rule ccorres_move_c_guard_cte | csymbr)+ 2737 apply (rule ccorres_symb_exec_r) 2738 apply (rule_tac xf'="mdbNode_'" in ccorres_abstract, ceqv) 2739 apply (rename_tac "cmdbNode") 2740 apply (rule_tac P="cmdbnode_relation (cteMDBNode newCTE) cmdbNode" 2741 in ccorres_gen_asm2) 2742 apply csymbr+ 2743 2744 \<comment> \<open>--- instruction: updateMDB (mdbPrev rva) (mdbNext_update \<dots>) but with Ptr\<dots>\<noteq> NULL on C side\<close> 2745 apply (simp only:Ptr_not_null_pointer_not_zero) \<comment> \<open>replaces Ptr p \<noteq> NULL with p\<noteq>0\<close> 2746 2747 \<comment> \<open>--- instruction: y \<leftarrow> updateMDB (mdbPrev rva) (mdbNext_update (\<lambda>_. mdbNext rva))\<close> 2748 apply (ctac (no_simp, no_vcg) pre:ccorres_move_guard_ptr_safe 2749 add: updateMDB_mdbPrev_set_mdbNext) 2750 \<comment> \<open>here ctac alone does not apply because the subgoal generated 2751 by the rule are not solvable by simp\<close> 2752 \<comment> \<open>so we have to use (no_simp) (or apply (rule ccorres_split_nothrow))\<close> 2753 apply (simp add: cmdbnode_relation_def) 2754 apply assumption 2755 \<comment> \<open>*** Main goal ***\<close> 2756 \<comment> \<open>--- instruction: updateMDB (mdbNext rva) 2757 (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged rva) 2758 (mdbPrev_update (\<lambda>_. mdbPrev rva) mdb));\<close> 2759 apply (rule ccorres_rhs_assoc2 ) \<comment> \<open>to group the 2 first C instrutions together\<close> 2760 apply (ctac (no_vcg) add: emptySlot_helper) 2761 2762 \<comment> \<open>--- instruction: y \<leftarrow> updateCap slot capability.NullCap;\<close> 2763 apply (simp del: Collect_const) 2764 apply csymbr 2765 apply (ctac (no_vcg) pre:ccorres_move_guard_ptr_safe) 2766 apply csymbr 2767 apply (rule ccorres_move_c_guard_cte) 2768 \<comment> \<open>--- instruction y \<leftarrow> updateMDB slot (\<lambda>a. nullMDBNode);\<close> 2769 apply (ctac (no_vcg) pre: ccorres_move_guard_ptr_safe 2770 add: ccorres_updateMDB_const [unfolded const_def]) 2771 2772 \<comment> \<open>the post_cap_deletion case\<close> 2773 2774 apply (ctac(no_vcg) add: postCapDeletion_ccorres [unfolded dc_def]) 2775 2776 \<comment> \<open>Haskell pre/post for y \<leftarrow> updateMDB slot (\<lambda>a. nullMDBNode);\<close> 2777 apply wp 2778 \<comment> \<open>C pre/post for y \<leftarrow> updateMDB slot (\<lambda>a. nullMDBNode);\<close> 2779 apply simp 2780 \<comment> \<open>C pre/post for the 2nd CALL\<close> 2781 \<comment> \<open>Haskell pre/post for y \<leftarrow> updateCap slot capability.NullCap;\<close> 2782 apply wp 2783 \<comment> \<open>C pre/post for y \<leftarrow> updateCap slot capability.NullCap;\<close> 2784 apply (simp add: Collect_const_mem cmdbnode_relation_def mdb_node_to_H_def nullMDBNode_def false_def) 2785 \<comment> \<open>Haskell pre/post for the two nested updates\<close> 2786 apply wp 2787 \<comment> \<open>C pre/post for the two nested updates\<close> 2788 apply (simp add: Collect_const_mem ccap_relation_NullCap_iff) 2789 \<comment> \<open>Haskell pre/post for (updateMDB (mdbPrev rva) (mdbNext_update (\<lambda>_. mdbNext rva)))\<close> 2790 apply (simp, wp) 2791 \<comment> \<open>C pre/post for (updateMDB (mdbPrev rva) (mdbNext_update (\<lambda>_. mdbNext rva)))\<close> 2792 apply simp+ 2793 apply vcg 2794 apply (rule conseqPre, vcg) 2795 apply clarsimp 2796 apply simp 2797 apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift) 2798 2799 \<comment> \<open>final precondition proof\<close> 2800 apply (clarsimp simp: typ_heap_simps Collect_const_mem 2801 cte_wp_at_ctes_of) 2802 2803 apply (rule conjI) 2804 \<comment> \<open>Haskell side\<close> 2805 apply (simp add: is_aligned_3_next canonical_address_mdbNext) 2806 2807 \<comment> \<open>C side\<close> 2808 apply (clarsimp simp: map_comp_Some_iff typ_heap_simps) 2809 apply (subst cap_get_tag_isCap) 2810 apply (rule ccte_relation_ccap_relation) 2811 apply (simp add: ccte_relation_def c_valid_cte_def 2812 cl_valid_cte_def c_valid_cap_def) 2813 apply simp 2814 done 2815 2816 2817(************************************************************************) 2818(* *) 2819(* capSwapForDelete_ccorres *********************************************) 2820(* *) 2821(************************************************************************) 2822 2823lemma ccorres_return_void_C: 2824 "ccorres dc xfdc \<top> UNIV (SKIP # hs) (return rv) (return_void_C)" 2825 apply (rule ccorres_from_vcg_throws) 2826 apply (simp add: return_def) 2827 apply (rule allI, rule conseqPre) 2828 apply vcg 2829 apply simp 2830 done 2831 2832declare Collect_const [simp del] 2833 2834lemma capSwapForDelete_ccorres: 2835 "ccorres dc xfdc 2836 (valid_mdb' and pspace_aligned' and pspace_canonical') 2837 (UNIV \<inter> {s. slot1_' s = Ptr slot1} 2838 \<inter> {s. slot2_' s = Ptr slot2}) 2839 [] 2840 (capSwapForDelete slot1 slot2) 2841 (Call capSwapForDelete_'proc)" 2842 apply (cinit lift: slot1_' slot2_' simp del: return_bind) 2843 \<comment> \<open>***Main goal***\<close> 2844 \<comment> \<open>--- instruction: when (slot1 \<noteq> slot2) \<dots> / IF Ptr slot1 = Ptr slot2 THEN \<dots>\<close> 2845 apply (simp add:when_def) 2846 apply (rule ccorres_if_cond_throws2 [where Q = \<top> and Q' = \<top>]) 2847 apply (case_tac "slot1=slot2", simp+) 2848 apply (rule ccorres_return_void_C [simplified dc_def]) 2849 2850 \<comment> \<open>***Main goal***\<close> 2851 \<comment> \<open>--- ccorres goal with 2 affectations (cap1 and cap2) on both on Haskell and C\<close> 2852 \<comment> \<open>--- \<Longrightarrow> execute each part independently\<close> 2853 apply (simp add: liftM_def cong: call_ignore_cong) 2854 apply (rule ccorres_pre_getCTE)+ 2855 apply (rule ccorres_move_c_guard_cte, rule ccorres_symb_exec_r)+ 2856 \<comment> \<open>***Main goal***\<close> 2857 apply (ctac (no_vcg) add: cteSwap_ccorres [unfolded dc_def] ) 2858 \<comment> \<open>C Hoare triple for \<acute>cap2 :== \<dots>\<close> 2859 apply vcg 2860 \<comment> \<open>C existential Hoare triple for \<acute>cap2 :== \<dots>\<close> 2861 apply simp 2862 apply (rule conseqPre) 2863 apply vcg 2864 apply simp 2865 \<comment> \<open>C Hoare triple for \<acute>cap1 :== \<dots>\<close> 2866 apply vcg 2867 \<comment> \<open>C existential Hoare triple for \<acute>cap1 :== \<dots>\<close> 2868 apply simp 2869 apply (rule conseqPre) 2870 apply vcg 2871 apply simp 2872 2873 \<comment> \<open>Hoare triple for return_void\<close> 2874 apply vcg 2875 2876 \<comment> \<open>***Generalized preconditions***\<close> 2877 apply simp 2878 apply (clarsimp simp: cte_wp_at_ctes_of map_comp_Some_iff 2879 typ_heap_simps ccap_relation_def) 2880 apply (simp add: cl_valid_cte_def c_valid_cap_def) 2881done 2882 2883 2884 2885declare Collect_const [simp add] 2886 2887(************************************************************************) 2888(* *) 2889(* Arch_sameRegionAs_ccorres ********************************************) 2890(* *) 2891(************************************************************************) 2892 2893lemma cap_get_tag_PageCap_frame: 2894 "ccap_relation cap cap' \<Longrightarrow> 2895 (cap_get_tag cap' = scast cap_frame_cap) = 2896 (cap = 2897 capability.ArchObjectCap 2898 (PageCap (cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap')) 2899 (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap'))) 2900 (maptype_to_H (cap_frame_cap_CL.capFMapType_CL (cap_frame_cap_lift cap'))) 2901 (framesize_to_H (capFSize_CL (cap_frame_cap_lift cap'))) 2902 (to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap'))) 2903 (if cap_frame_cap_CL.capFMappedASID_CL (cap_frame_cap_lift cap') = 0 2904 then None else 2905 Some ((cap_frame_cap_CL.capFMappedASID_CL (cap_frame_cap_lift cap')), 2906 cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift cap')))))" 2907 apply (rule iffI) 2908 apply (erule ccap_relationE) 2909 apply (clarsimp simp add: cap_lifts cap_to_H_def Let_def split: if_split) 2910 apply (simp add: cap_get_tag_isCap isCap_simps pageSize_def) 2911done 2912 2913lemma fff_is_pageBits: 2914 "(0xFFF :: machine_word) = 2 ^ pageBits - 1" 2915 by (simp add: pageBits_def) 2916 2917 2918(* used? *) 2919lemma valid_cap'_PageCap_is_aligned: 2920 "valid_cap' (ArchObjectCap (arch_capability.PageCap w r mt sz d option)) t \<Longrightarrow> 2921 is_aligned w (pageBitsForSize sz)" 2922 apply (simp add: valid_cap'_def capAligned_def) 2923done 2924 2925lemma Arch_sameRegionAs_spec: 2926 notes cap_get_tag = ccap_rel_cap_get_tag_cases_arch' 2927 shows 2928 "\<forall>capa capb. \<Gamma> \<turnstile> \<lbrace> ccap_relation (ArchObjectCap capa) \<acute>cap_a \<and> 2929 ccap_relation (ArchObjectCap capb) \<acute>cap_b \<rbrace> 2930 Call Arch_sameRegionAs_'proc 2931 \<lbrace> \<acute>ret__unsigned_long = from_bool (Arch.sameRegionAs capa capb) \<rbrace>" 2932 apply vcg 2933 apply clarsimp 2934 apply (simp add: X64_H.sameRegionAs_def) 2935 subgoal for capa capb cap_b cap_a 2936 apply (cases capa; cases capb; 2937 frule (1) cap_get_tag[where cap'=cap_a]; (frule cap_lifts[where c=cap_a, THEN iffD1])?; 2938 frule (1) cap_get_tag[where cap'=cap_b]; (frule cap_lifts[where c=cap_b, THEN iffD1])?) 2939 apply (simp_all add: cap_tag_defs isCap_simps from_bool_def true_def false_def if_0_1_eq) 2940 apply (all \<open>clarsimp simp: ccap_relation_def cap_to_H_def 2941 c_valid_cap_def cl_valid_cap_def Let_def\<close>) 2942 apply (simp add: cap_io_port_cap_lift_def'[simplified cap_tag_defs] mask_def 2943 ucast_le_ucast_eq[OF and_mask_less' and_mask_less'] split: bool.splits) 2944 apply (intro conjI impI; clarsimp; word_bitwise; auto) 2945 apply (clarsimp simp: cap_frame_cap_lift_def'[simplified cap_tag_defs] 2946 framesize_to_H_def pageBitsForSize_def field_simps 2947 X86_SmallPage_def X86_LargePage_def pageBits_def ptTranslationBits_def 2948 split: vmpage_size.splits if_splits) 2949 done 2950 done 2951 2952(* combination of cap_get_capSizeBits + cap_get_archCapSizeBits from C *) 2953definition 2954 get_capSizeBits_CL :: "cap_CL option \<Rightarrow> nat" where 2955 "get_capSizeBits_CL \<equiv> \<lambda>cap. case cap of 2956 Some (Cap_untyped_cap c) \<Rightarrow> unat (cap_untyped_cap_CL.capBlockSize_CL c) 2957 | Some (Cap_endpoint_cap c) \<Rightarrow> epSizeBits 2958 | Some (Cap_notification_cap c) \<Rightarrow> ntfnSizeBits 2959 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + cteSizeBits 2960 | Some (Cap_thread_cap c) \<Rightarrow> tcbBlockSizeBits 2961 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (framesize_to_H $ cap_frame_cap_CL.capFSize_CL c) 2962 | Some (Cap_page_table_cap c) \<Rightarrow> 12 2963 | Some (Cap_page_directory_cap c) \<Rightarrow> 12 2964 | Some (Cap_pdpt_cap c) \<Rightarrow> 12 2965 | Some (Cap_pml4_cap c) \<Rightarrow> 12 2966 | Some (Cap_asid_pool_cap c) \<Rightarrow> 12 2967 | Some (Cap_zombie_cap c) \<Rightarrow> 2968 let type = cap_zombie_cap_CL.capZombieType_CL c in 2969 if isZombieTCB_C type 2970 then tcbBlockSizeBits 2971 else unat (type && mask wordRadix) + cteSizeBits 2972 | _ \<Rightarrow> 0" 2973 2974lemma frame_cap_size [simp]: 2975 "cap_get_tag cap = scast cap_frame_cap 2976 \<Longrightarrow> cap_frame_cap_CL.capFSize_CL (cap_frame_cap_lift cap) && mask 2 = 2977 cap_frame_cap_CL.capFSize_CL (cap_frame_cap_lift cap)" 2978 apply (simp add: cap_frame_cap_lift_def) 2979 by (simp add: cap_lift_def cap_tag_defs) 2980 2981lemma cap_get_tag_bound: 2982 "cap_get_tag x < 32" 2983 apply (simp add: cap_get_tag_def mask_def) 2984 by word_bitwise 2985 2986lemma cap_get_tag_scast: 2987 "UCAST(64 \<rightarrow> 32 signed) (cap_get_tag cap) = tag \<longleftrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 64) tag" 2988 apply (rule iffI; simp add: cap_get_tag_def) 2989 apply (drule sym; simp add: ucast_and_mask scast_eq_ucast msb_nth ucast_ucast_mask mask_twice) 2990 done 2991 2992lemma cap_get_capSizeBits_spec: 2993 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. c_valid_cap (cap_' s)\<rbrace> 2994 \<acute>ret__unsigned_long :== PROC cap_get_capSizeBits(\<acute>cap) 2995 \<lbrace>\<acute>ret__unsigned_long = of_nat (get_capSizeBits_CL (cap_lift \<^bsup>s\<^esup>cap))\<rbrace>" 2996 apply vcg 2997 apply (clarsimp simp: get_capSizeBits_CL_def) 2998 apply (intro conjI impI; 2999 clarsimp simp: cap_lifts 3000 cap_lift_asid_control_cap 3001 cap_lift_irq_control_cap cap_lift_null_cap 3002 Kernel_C.asidLowBits_def asid_low_bits_def 3003 word_sle_def Let_def mask_def 3004 isZombieTCB_C_def ZombieTCB_C_def 3005 cap_lift_domain_cap cap_get_tag_scast 3006 objBits_defs wordRadix_def 3007 c_valid_cap_def cl_valid_cap_def 3008 dest!: sym [where t = "ucast (cap_get_tag cap)" for cap]) 3009 apply (clarsimp split: option.splits cap_CL.splits dest!: cap_lift_Some_CapD) 3010 done 3011 3012lemma ccap_relation_get_capSizeBits_physical: 3013 "\<lbrakk> ccap_relation hcap ccap; capClass hcap = PhysicalClass; capAligned hcap \<rbrakk> 3014 \<Longrightarrow> 2 ^ get_capSizeBits_CL (cap_lift ccap) = capUntypedSize hcap" 3015 apply (cases hcap; 3016 (match premises in "hcap = ArchObjectCap c" for c \<Rightarrow> \<open>cases c\<close>)?; 3017 (frule (1) ccap_rel_cap_get_tag_cases_generic)?; 3018 (frule (2) ccap_rel_cap_get_tag_cases_arch)?; 3019 (frule cap_lifts[THEN iffD1])?) 3020 apply (all \<open>clarsimp simp: get_capSizeBits_CL_def objBits_simps Let_def X64_H.capUntypedSize_def 3021 asid_low_bits_def\<close>) 3022 (* Zombie, Page, Untyped, CNode caps remain. *) 3023 apply (all \<open>thin_tac \<open>hcap = _\<close>\<close>) 3024 apply (all \<open>rule arg_cong[where f="\<lambda>s. 2 ^ s"]\<close>) 3025 apply (all \<open>simp add: ccap_relation_def cap_lift_defs cap_lift_def cap_tag_defs cap_to_H_def\<close>) 3026 (* Now just Zombie caps *) 3027 apply (clarsimp simp: Let_def objBits_simps' wordRadix_def capAligned_def 3028 word_bits_def word_less_nat_alt 3029 intro!: less_mask_eq 3030 split: if_splits) 3031 done 3032 3033lemma ccap_relation_get_capSizeBits_untyped: 3034 "\<lbrakk> ccap_relation (UntypedCap d word bits idx) ccap \<rbrakk> \<Longrightarrow> 3035 get_capSizeBits_CL (cap_lift ccap) = bits" 3036 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3037 by (clarsimp simp: get_capSizeBits_CL_def ccap_relation_def 3038 map_option_case cap_to_H_def cap_lift_def cap_tag_defs) 3039 3040definition 3041 get_capZombieBits_CL :: "cap_zombie_cap_CL \<Rightarrow> machine_word" where 3042 "get_capZombieBits_CL \<equiv> \<lambda>cap. 3043 let type = cap_zombie_cap_CL.capZombieType_CL cap in 3044 if isZombieTCB_C type then 4 else type && mask 6" 3045 3046 3047lemma get_capSizeBits_valid_shift: 3048 "\<lbrakk> ccap_relation hcap ccap; capAligned hcap \<rbrakk> \<Longrightarrow> 3049 get_capSizeBits_CL (cap_lift ccap) < 64" 3050 apply (cases hcap; 3051 (match premises in "hcap = ArchObjectCap c" for c \<Rightarrow> \<open>cases c\<close>)?; 3052 (frule (1) ccap_rel_cap_get_tag_cases_generic)?; 3053 (frule (2) ccap_rel_cap_get_tag_cases_arch)?; 3054 (frule cap_lifts[THEN iffD1])?) 3055 (* Deal with simple cases quickly. *) 3056 apply (all \<open>clarsimp simp: get_capSizeBits_CL_def objBits_simps' wordRadix_def Let_def 3057 split: option.splits if_splits; 3058 thin_tac \<open>hcap = _\<close>\<close>) 3059 (* Deal with non-physical caps quickly. *) 3060 apply (all \<open>(match conclusion in "case_cap_CL _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ < _" \<Rightarrow> 3061 \<open>clarsimp simp: cap_lift_def cap_tag_defs\<close>)?\<close>) 3062 (* Slow cases: Zombie, Page, Untyped and CNode caps. *) 3063 apply (all \<open>clarsimp simp: cap_lift_def cap_lift_defs cap_tag_defs 3064 ccap_relation_def cap_to_H_def Let_def 3065 capAligned_def objBits_simps' word_bits_def 3066 unat_ucast_less_no_overflow_simp\<close>) 3067 (* Zombie arithmetic. *) 3068 apply (subst less_mask_eq[where n=6]; clarsimp elim!: less_trans) 3069 done 3070 3071lemma get_capSizeBits_valid_shift_word: 3072 "\<lbrakk> ccap_relation hcap ccap; capAligned hcap \<rbrakk> \<Longrightarrow> 3073 of_nat (get_capSizeBits_CL (cap_lift ccap)) < (0x40::machine_word)" 3074 apply (subgoal_tac "of_nat (get_capSizeBits_CL (cap_lift ccap)) < (of_nat 64::machine_word)", simp) 3075 apply (rule of_nat_mono_maybe, simp+) 3076 apply (simp add: get_capSizeBits_valid_shift) 3077 done 3078 3079lemma cap_zombie_cap_get_capZombieBits_spec: 3080 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_zombie_cap \<rbrace> 3081 \<acute>ret__unsigned_long :== PROC cap_zombie_cap_get_capZombieBits(\<acute>cap) 3082 \<lbrace>\<acute>ret__unsigned_long = get_capZombieBits_CL (cap_zombie_cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" 3083 apply vcg 3084 apply (clarsimp simp: get_capZombieBits_CL_def word_sle_def mask_def 3085 isZombieTCB_C_def ZombieTCB_C_def Let_def) 3086 done 3087 3088definition 3089 get_capZombiePtr_CL :: "cap_zombie_cap_CL \<Rightarrow> machine_word" where 3090 "get_capZombiePtr_CL \<equiv> \<lambda>cap. 3091 let radix = unat (get_capZombieBits_CL cap) in 3092 cap_zombie_cap_CL.capZombieID_CL cap && ~~ (mask (radix+1))" 3093 3094lemma cap_zombie_cap_get_capZombiePtr_spec: 3095 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_zombie_cap 3096 \<and> get_capZombieBits_CL (cap_zombie_cap_lift \<acute>cap) < 0x3F \<rbrace> 3097 \<acute>ret__unsigned_long :== PROC cap_zombie_cap_get_capZombiePtr(\<acute>cap) 3098 \<lbrace>\<acute>ret__unsigned_long = get_capZombiePtr_CL (cap_zombie_cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" 3099 apply vcg 3100 apply (clarsimp simp: get_capZombiePtr_CL_def word_sle_def mask_def 3101 isZombieTCB_C_def ZombieTCB_C_def Let_def) 3102 apply (intro conjI) 3103 apply (simp add: word_add_less_mono1[where k=1 and j="0x3F", simplified]) 3104 apply (subst unat_plus_if_size) 3105 apply (clarsimp split: if_split) 3106 apply (clarsimp simp: get_capZombieBits_CL_def Let_def word_size 3107 split: if_split if_split_asm) 3108 apply (subgoal_tac "unat (capZombieType_CL (cap_zombie_cap_lift cap) && mask 6) 3109 < unat ((2::machine_word) ^ 6)") 3110 apply clarsimp 3111 apply (rule unat_mono) 3112 apply (rule and_mask_less_size) 3113 apply (clarsimp simp: word_size) 3114 done 3115 3116definition 3117 get_capPtr_CL :: "cap_CL option \<Rightarrow> unit ptr" where 3118 "get_capPtr_CL \<equiv> \<lambda>cap. Ptr (case cap of 3119 Some (Cap_untyped_cap c) \<Rightarrow> cap_untyped_cap_CL.capPtr_CL c 3120 | Some (Cap_endpoint_cap c) \<Rightarrow> cap_endpoint_cap_CL.capEPPtr_CL c 3121 | Some (Cap_notification_cap c) \<Rightarrow> cap_notification_cap_CL.capNtfnPtr_CL c 3122 | Some (Cap_cnode_cap c) \<Rightarrow> cap_cnode_cap_CL.capCNodePtr_CL c 3123 | Some (Cap_thread_cap c) \<Rightarrow> (cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits (undefined :: tcb))) 3124 | Some (Cap_frame_cap c) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL c 3125 | Some (Cap_page_table_cap c) \<Rightarrow> cap_page_table_cap_CL.capPTBasePtr_CL c 3126 | Some (Cap_page_directory_cap c) \<Rightarrow> cap_page_directory_cap_CL.capPDBasePtr_CL c 3127 | Some (Cap_pdpt_cap c) \<Rightarrow> cap_pdpt_cap_CL.capPDPTBasePtr_CL c 3128 | Some (Cap_pml4_cap c) \<Rightarrow> cap_pml4_cap_CL.capPML4BasePtr_CL c 3129 | Some (Cap_asid_pool_cap c) \<Rightarrow> cap_asid_pool_cap_CL.capASIDPool_CL c 3130 | Some (Cap_zombie_cap c) \<Rightarrow> get_capZombiePtr_CL c 3131 | _ \<Rightarrow> 0)" 3132 3133lemma cap_get_capPtr_spec: 3134 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. (cap_get_tag \<acute>cap = scast cap_zombie_cap 3135 \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift \<acute>cap) < 0x3F)\<rbrace> 3136 \<acute>ret__ptr_to_void :== PROC cap_get_capPtr(\<acute>cap) 3137 \<lbrace>\<acute>ret__ptr_to_void = get_capPtr_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" 3138 apply vcg 3139 apply (clarsimp simp: get_capPtr_CL_def) 3140 apply (intro impI conjI) 3141 apply (clarsimp simp: cap_lifts pageBitsForSize_def 3142 cap_lift_asid_control_cap word_sle_def 3143 cap_lift_irq_control_cap cap_lift_null_cap 3144 mask_def objBits_simps' cap_lift_domain_cap 3145 ptr_add_assertion_positive cap_get_tag_scast 3146 dest!: sym [where t = "ucast (cap_get_tag cap)" for cap] 3147 split: vmpage_size.splits)+ 3148 (* XXX: slow. there should be a rule for this *) 3149 by (case_tac "cap_lift cap", simp_all, case_tac "a", 3150 auto simp: cap_lift_def cap_lift_defs cap_tag_defs Let_def 3151 split: if_split_asm) 3152 3153definition get_capIsPhysical_CL :: "cap_CL option \<Rightarrow> bool" 3154where 3155 "get_capIsPhysical_CL \<equiv> \<lambda>cap. (case cap of 3156 Some (Cap_untyped_cap c) \<Rightarrow> True 3157 | Some (Cap_endpoint_cap c) \<Rightarrow> True 3158 | Some (Cap_notification_cap c) \<Rightarrow> True 3159 | Some (Cap_cnode_cap c) \<Rightarrow> True 3160 | Some (Cap_thread_cap c) \<Rightarrow> True 3161 | Some (Cap_frame_cap c) \<Rightarrow> True 3162 | Some (Cap_page_table_cap c) \<Rightarrow> True 3163 | Some (Cap_page_directory_cap c) \<Rightarrow> True 3164 | Some (Cap_pdpt_cap c) \<Rightarrow> True 3165 | Some (Cap_pml4_cap c) \<Rightarrow> True 3166 | Some (Cap_asid_pool_cap c) \<Rightarrow> True 3167 | Some (Cap_zombie_cap c) \<Rightarrow> True 3168 | _ \<Rightarrow> False)" 3169 3170lemma cap_get_capIsPhysical_spec: 3171 "\<forall>s. \<Gamma> \<turnstile> {s} 3172 Call cap_get_capIsPhysical_'proc 3173 \<lbrace>\<acute>ret__unsigned_long = from_bool (get_capIsPhysical_CL (cap_lift \<^bsup>s\<^esup>cap))\<rbrace>" 3174 apply vcg 3175 apply (clarsimp simp: get_capIsPhysical_CL_def) 3176 apply (intro impI conjI) 3177 apply (clarsimp simp: cap_lifts pageBitsForSize_def 3178 cap_lift_asid_control_cap word_sle_def 3179 cap_lift_irq_control_cap cap_lift_null_cap 3180 mask_def objBits_simps cap_lift_domain_cap 3181 ptr_add_assertion_positive from_bool_def 3182 true_def false_def cap_get_tag_scast 3183 dest!: sym [where t = "ucast (cap_get_tag cap)" for cap] 3184 split: vmpage_size.splits)+ 3185 (* XXX: slow. there should be a rule for this *) 3186 by (case_tac "cap_lift cap", simp_all, case_tac a, 3187 auto simp: cap_lift_def cap_lift_defs cap_tag_defs Let_def 3188 split: if_split_asm) 3189 3190lemma ccap_relation_get_capPtr_not_physical: 3191 "\<lbrakk> ccap_relation hcap ccap; capClass hcap \<noteq> PhysicalClass \<rbrakk> \<Longrightarrow> 3192 get_capPtr_CL (cap_lift ccap) = Ptr 0" 3193 by (clarsimp simp: ccap_relation_def get_capPtr_CL_def cap_to_H_def Let_def 3194 split: option.split cap_CL.split_asm if_split_asm) 3195 3196lemma ccap_relation_get_capIsPhysical: 3197 "ccap_relation hcap ccap \<Longrightarrow> isPhysicalCap hcap = get_capIsPhysical_CL (cap_lift ccap)" 3198 apply (case_tac hcap; clarsimp simp: cap_lifts cap_lift_domain_cap cap_lift_null_cap 3199 cap_lift_irq_control_cap cap_to_H_def 3200 get_capIsPhysical_CL_def 3201 dest!: cap_get_tag_isCap_unfolded_H_cap) 3202 apply (rename_tac arch_cap) 3203 apply (case_tac arch_cap; clarsimp simp: cap_lifts cap_lift_asid_control_cap cap_lift_io_port_control_cap 3204 dest!: cap_get_tag_isCap_unfolded_H_cap) 3205 done 3206 3207lemma ctcb_ptr_to_tcb_ptr_mask': 3208 "is_aligned (ctcb_ptr_to_tcb_ptr (tcb_Ptr x)) (objBits (undefined :: tcb)) \<Longrightarrow> 3209 ctcb_ptr_to_tcb_ptr (tcb_Ptr x) = x && ~~ mask (objBits (undefined :: tcb))" 3210 apply (simp add: ctcb_ptr_to_tcb_ptr_def) 3211 apply (drule_tac d=ctcb_offset in is_aligned_add_helper) 3212 apply (simp add: objBits_simps' ctcb_offset_defs) 3213 apply simp 3214 done 3215 3216lemmas ctcb_ptr_to_tcb_ptr_mask 3217 = ctcb_ptr_to_tcb_ptr_mask'[simplified objBits_simps, simplified] 3218 3219lemma ccap_relation_get_capPtr_physical: 3220 "\<lbrakk> ccap_relation hcap ccap; capClass hcap = PhysicalClass; capAligned hcap \<rbrakk> \<Longrightarrow> 3221 get_capPtr_CL (cap_lift ccap) 3222 = Ptr (capUntypedPtr hcap)" 3223 apply (cases hcap; 3224 (match premises in "hcap = ArchObjectCap c" for c \<Rightarrow> \<open>cases c\<close>)?; 3225 (frule (1) ccap_rel_cap_get_tag_cases_generic)?; 3226 (frule (2) ccap_rel_cap_get_tag_cases_arch)?; 3227 (frule cap_lifts[THEN iffD1])?) 3228 apply (all \<open>clarsimp simp: get_capPtr_CL_def get_capZombiePtr_CL_def get_capZombieBits_CL_def 3229 objBits_simps ccap_relation_def cap_to_H_def Let_def capAligned_def 3230 ctcb_ptr_to_tcb_ptr_mask 3231 split: if_splits; 3232 thin_tac \<open>hcap = _\<close>\<close>) 3233 apply (rule arg_cong[OF less_mask_eq]) 3234 apply (clarsimp simp: cap_lift_def cap_lift_defs Let_def cap_tag_defs word_less_nat_alt 3235 word_bits_conv) 3236 done 3237 3238lemma ccap_relation_get_capPtr_untyped: 3239 "\<lbrakk> ccap_relation (UntypedCap d word bits idx) ccap \<rbrakk> \<Longrightarrow> 3240 get_capPtr_CL (cap_lift ccap) = Ptr word" 3241 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3242 by (clarsimp simp: get_capPtr_CL_def ccap_relation_def 3243 map_option_case cap_to_H_def cap_lift_def cap_tag_defs) 3244 3245lemma cap_get_tag_isArchCap_unfolded_H_cap: 3246 "ccap_relation (capability.ArchObjectCap a_cap) cap' \<Longrightarrow> 3247 (isArchCap_tag (cap_get_tag cap'))" 3248 apply (frule cap_get_tag_isCap(11), simp) 3249 done 3250 3251lemmas ccap_rel_cap_get_tag_cases_generic' = 3252 ccap_rel_cap_get_tag_cases_generic 3253 cap_get_tag_isArchCap_unfolded_H_cap[OF back_subst[of "\<lambda>cap. ccap_relation cap cap'" for cap']] 3254 3255lemma sameRegionAs_spec: 3256 notes cap_get_tag = ccap_rel_cap_get_tag_cases_generic' 3257 shows 3258 "\<forall>capa capb. \<Gamma> \<turnstile> \<lbrace>ccap_relation capa \<acute>cap_a \<and> ccap_relation capb \<acute>cap_b \<and> capAligned capb\<rbrace> 3259 Call sameRegionAs_'proc 3260 \<lbrace> \<acute>ret__unsigned_long = from_bool (sameRegionAs capa capb) \<rbrace>" 3261 apply vcg 3262 apply clarsimp 3263 apply (simp add: sameRegionAs_def isArchCap_tag_def2 ccap_relation_c_valid_cap) 3264 apply (case_tac capa, simp_all add: cap_get_tag_isCap_unfolded_H_cap isCap_simps) 3265 \<comment> \<open>capa is a ThreadCap\<close> 3266 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3267 isCap_simps cap_tag_defs from_bool_def false_def)[1] 3268 apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(1)) 3269 apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(1)) 3270 apply (simp add: ccap_relation_def map_option_case) 3271 apply (simp add: cap_thread_cap_lift) 3272 apply (simp add: cap_to_H_def) 3273 apply (clarsimp simp: case_bool_If ctcb_ptr_to_tcb_ptr_def if_distrib 3274 cong: if_cong) 3275 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3276 apply (clarsimp simp: isArchCap_tag_def2) 3277 \<comment> \<open>capa is a NullCap\<close> 3278 apply (simp add: cap_tag_defs from_bool_def false_def) 3279 \<comment> \<open>capa is an NotificationCap\<close> 3280 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3281 isCap_simps cap_tag_defs from_bool_def false_def)[1] 3282 apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(3)) 3283 apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(3)) 3284 apply (simp add: ccap_relation_def map_option_case) 3285 apply (simp add: cap_notification_cap_lift) 3286 apply (simp add: cap_to_H_def) 3287 apply (clarsimp split: if_split) 3288 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3289 apply (clarsimp simp: isArchCap_tag_def2) 3290 \<comment> \<open>capa is an IRQHandlerCap\<close> 3291 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3292 isCap_simps cap_tag_defs from_bool_def false_def)[1] 3293 apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(5)) 3294 apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(5)) 3295 apply (simp add: ccap_relation_def map_option_case) 3296 apply (simp add: cap_irq_handler_cap_lift) 3297 apply (simp add: cap_to_H_def) 3298 apply (clarsimp simp: up_ucast_inj_eq c_valid_cap_def 3299 cl_valid_cap_def mask_twice 3300 split: if_split bool.split 3301 | intro impI conjI 3302 | simp ) 3303 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3304 apply (clarsimp simp: isArchCap_tag_def2) 3305 \<comment> \<open>capa is an EndpointCap\<close> 3306 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3307 isCap_simps cap_tag_defs from_bool_def false_def)[1] 3308 apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(4)) 3309 apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(4)) 3310 apply (simp add: ccap_relation_def map_option_case) 3311 apply (simp add: cap_endpoint_cap_lift) 3312 apply (simp add: cap_to_H_def) 3313 apply (clarsimp split: if_split) 3314 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3315 apply (clarsimp simp: isArchCap_tag_def2) 3316 \<comment> \<open>capa is a DomainCap\<close> 3317 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3318 isCap_simps cap_tag_defs from_bool_def false_def true_def)[1] 3319 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3320 apply (fastforce simp: isArchCap_tag_def2 split: if_split) 3321 \<comment> \<open>capa is a Zombie\<close> 3322 apply (simp add: cap_tag_defs from_bool_def false_def) 3323 \<comment> \<open>capa is an Arch object cap\<close> 3324 apply (frule_tac cap'=cap_a in cap_get_tag_isArchCap_unfolded_H_cap) 3325 apply (clarsimp simp: isArchCap_tag_def2 cap_tag_defs linorder_not_less [THEN sym]) 3326 apply (rule conjI, clarsimp, rule impI)+ 3327 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3328 isCap_simps cap_tag_defs from_bool_def false_def)[1] 3329 \<comment> \<open>capb is an Arch object cap\<close> 3330 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3331 apply (fastforce simp: isArchCap_tag_def2 cap_tag_defs linorder_not_less [THEN sym]) 3332 \<comment> \<open>capa is a ReplyCap\<close> 3333 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3334 isCap_simps cap_tag_defs from_bool_def false_def)[1] 3335 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3336 apply (clarsimp simp: isArchCap_tag_def2) 3337 apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(8)) 3338 apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(8)) 3339 apply (simp add: ccap_relation_def map_option_case) 3340 apply (simp add: cap_reply_cap_lift) 3341 apply (simp add: cap_to_H_def ctcb_ptr_to_tcb_ptr_def) 3342 apply (clarsimp split: if_split) 3343 \<comment> \<open>capa is an UntypedCap\<close> 3344 apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(9)) 3345 apply (intro conjI) 3346 apply (rule impI, intro conjI) 3347 apply (rule impI, drule(1) cap_get_tag_to_H)+ 3348 apply (clarsimp simp: capAligned_def word_bits_conv 3349 objBits_simps' get_capZombieBits_CL_def 3350 Let_def word_less_nat_alt 3351 less_mask_eq true_def 3352 split: if_split_asm) 3353 apply (subgoal_tac "capBlockSize_CL (cap_untyped_cap_lift cap_a) \<le> 0x3F") 3354 apply (simp add: word_le_make_less) 3355 apply (simp add: cap_untyped_cap_lift_def cap_lift_def 3356 cap_tag_defs word_and_le1 mask_def) 3357 apply (clarsimp simp: get_capSizeBits_valid_shift_word) 3358 apply (clarsimp simp: from_bool_def Let_def split: if_split bool.splits) 3359 apply (subst unat_of_nat64, 3360 clarsimp simp: unat_of_nat64 word_bits_def 3361 dest!: get_capSizeBits_valid_shift)+ 3362 apply (clarsimp simp: ccap_relation_get_capPtr_physical 3363 ccap_relation_get_capPtr_untyped 3364 ccap_relation_get_capIsPhysical[symmetric] 3365 ccap_relation_get_capSizeBits_physical 3366 ccap_relation_get_capSizeBits_untyped) 3367 apply (intro conjI impI) 3368 apply ((clarsimp simp: ccap_relation_def map_option_case 3369 cap_untyped_cap_lift cap_to_H_def 3370 field_simps valid_cap'_def)+)[4] 3371 apply (rule impI, simp add: from_bool_0 ccap_relation_get_capIsPhysical[symmetric]) 3372 apply (simp add: from_bool_def false_def) 3373 \<comment> \<open>capa is a CNodeCap\<close> 3374 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3375 isCap_simps cap_tag_defs from_bool_def false_def)[1] 3376 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3377 apply (clarsimp simp: isArchCap_tag_def2) 3378 apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(10)) 3379 apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(10)) 3380 apply (simp add: ccap_relation_def map_option_case) 3381 apply (simp add: cap_cnode_cap_lift) 3382 apply (simp add: cap_to_H_def) 3383 apply (clarsimp split: if_split bool.split) 3384 \<comment> \<open>capa is an IRQControlCap\<close> 3385 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3386 isCap_simps cap_tag_defs from_bool_def false_def true_def)[1] 3387 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3388 apply (fastforce simp: isArchCap_tag_def2 split: if_split) 3389 done 3390 3391lemma framesize_to_H_eq: 3392 "\<lbrakk> a \<le> 2; b \<le> 2 \<rbrakk> \<Longrightarrow> 3393 (framesize_to_H a = framesize_to_H b) = (a = b)" 3394 by (fastforce simp: framesize_to_H_def Kernel_C.X86_SmallPage_def 3395 Kernel_C.X86_LargePage_def Kernel_C.X64_HugePage_def 3396 word_le_make_less 3397 split: if_split 3398 dest: word_less_cases) 3399 3400lemma capFSize_range: 3401 "\<And>cap. cap_get_tag cap = scast cap_frame_cap \<Longrightarrow> c_valid_cap cap \<Longrightarrow> 3402 capFSize_CL (cap_frame_cap_lift cap) \<le> 2" 3403 apply (simp add: cap_frame_cap_lift_def c_valid_cap_def cl_valid_cap_def) 3404 apply (clarsimp simp: cap_frame_cap_lift) 3405 apply (drule word_less_sub_1, simp) 3406 done 3407 3408lemma ccap_relation_PageCap_BasePtr: 3409 "ccap_relation (ArchObjectCap (PageCap p r t s d m)) ccap 3410 \<Longrightarrow> capFBasePtr_CL (cap_frame_cap_lift ccap) = p" 3411 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3412 by (clarsimp simp: ccap_relation_def cap_to_H_def cap_lift_def cap_lift_defs cap_tag_defs 3413 Let_def) 3414 3415lemma ccap_relation_PageCap_IsDevice: 3416 "ccap_relation (ArchObjectCap (PageCap p r t s d m)) ccap 3417 \<Longrightarrow> capFIsDevice_CL (cap_frame_cap_lift ccap) = (if d then 1 else 0)" 3418 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3419 apply (clarsimp simp: ccap_relation_def cap_to_H_def cap_lift_def cap_lift_defs cap_tag_defs 3420 Let_def) 3421 apply (thin_tac _)+ 3422 by (clarsimp simp: to_bool_def mask_def word_and_1 split: if_splits) 3423 3424lemma ccap_relation_PageCap_Size: 3425 "ccap_relation (ArchObjectCap (PageCap p r t s d m)) ccap 3426 \<Longrightarrow> capFSize_CL (cap_frame_cap_lift ccap) = framesize_from_H s" 3427 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3428 apply (clarsimp simp: ccap_relation_def cap_to_H_def cap_lift_def cap_lift_defs cap_tag_defs 3429 Let_def c_valid_cap_def cl_valid_cap_def) 3430 apply (thin_tac "p = _", thin_tac "r = _", thin_tac "t = _", thin_tac "d = _", thin_tac "m = _") 3431 apply (cases s; clarsimp simp: framesize_to_H_def framesize_from_H_def 3432 X86_SmallPage_def X86_LargePage_def X64_HugePage_def 3433 split: if_splits cong: conj_cong) 3434 apply (word_bitwise, simp) 3435 done 3436 3437lemma ccap_relation_PageCap_MappedASID: 3438 "ccap_relation (ArchObjectCap (PageCap p r t s d (Some (a, b)))) ccap 3439 \<Longrightarrow> capFMappedASID_CL (cap_frame_cap_lift ccap) = a" 3440 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3441 apply (frule cap_get_tag_PageCap_frame) 3442 apply (clarsimp split: if_split_asm) 3443 done 3444 3445lemma ccap_relation_PageCap_MappedAddress: 3446 "ccap_relation (ArchObjectCap (PageCap p r t s d (Some (a, b)))) ccap 3447 \<Longrightarrow> capFMappedAddress_CL (cap_frame_cap_lift ccap) = b" 3448 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3449 apply (frule cap_get_tag_PageCap_frame) 3450 apply (clarsimp split: if_split_asm) 3451 done 3452 3453lemmas ccap_relation_PageCap_fields = 3454 ccap_relation_PageCap_BasePtr ccap_relation_PageCap_IsDevice ccap_relation_PageCap_Size 3455 3456lemma case_bool_of_nat_eq: 3457 defines "cases_of c \<equiv> case c of True \<Rightarrow> of_nat 1 | False \<Rightarrow> of_nat 0" 3458 shows "(cases_of c = 0) = (\<not> c)" 3459 "(cases_of c = 1) = c" 3460 "(cases_of c = cases_of d) = (c = d)" 3461 by (cases c; simp add: cases_of_def; cases d; simp)+ 3462 3463lemma Arch_sameObjectAs_spec: 3464 "\<forall>capa capb. \<Gamma> \<turnstile> \<lbrace>ccap_relation (ArchObjectCap capa) \<acute>cap_a \<and> 3465 ccap_relation (ArchObjectCap capb) \<acute>cap_b \<and> 3466 capAligned (ArchObjectCap capa) \<and> 3467 capAligned (ArchObjectCap capb) \<rbrace> 3468 Call Arch_sameObjectAs_'proc 3469 \<lbrace> \<acute>ret__unsigned_long = from_bool (Arch.sameObjectAs capa capb) \<rbrace>" 3470 proof - 3471 note cap_get_tag = ccap_rel_cap_get_tag_cases_arch' 3472 note case_bool_of_nat_eq[simp] 3473 have [simp]: "(\<forall>d. d) = False" "(\<forall>d. \<not>d) = False" by auto 3474 show ?thesis 3475 apply vcg 3476 apply (clarsimp simp: X64_H.sameObjectAs_def) 3477 subgoal for capa capb cap_b cap_a 3478 apply (cases capa) 3479 apply (all \<open>frule (1) cap_get_tag[where cap'=cap_a]\<close>) 3480 apply (all \<open>(frule cap_lifts[where c=cap_a, THEN iffD1])?\<close>) 3481 apply (all \<open>clarsimp simp: cap_tag_defs isCap_simps from_bool_def true_def false_def if_0_1_eq 3482 split: if_splits\<close>) 3483 apply (all \<open>fastforce?\<close>) 3484 (* IO ports and frames remain. *) 3485 apply (all \<open>cases capb\<close>) 3486 apply (all \<open>frule (1) cap_get_tag[where cap'=cap_b]\<close>) 3487 apply (all \<open>(frule cap_lifts[where c=cap_b, THEN iffD1])?\<close>) 3488 apply (all \<open>clarsimp simp: cap_tag_defs isCap_simps from_bool_def true_def false_def if_0_1_eq 3489 ccap_relation_PageCap_fields framesize_from_H_eq capAligned_def 3490 split: if_splits\<close>) 3491 apply (all \<open>(fastforce simp: X64_H.sameRegionAs_def isCap_simps)?\<close>) 3492 done 3493 done 3494 qed 3495 3496lemma sameObjectAs_spec: 3497 "\<forall>capa capb. \<Gamma> \<turnstile> \<lbrace>ccap_relation capa \<acute>cap_a \<and> 3498 ccap_relation capb \<acute>cap_b \<and> 3499 capAligned capa \<and> capAligned capb \<and> (\<exists>s. s \<turnstile>' capa)\<rbrace> 3500 Call sameObjectAs_'proc 3501 \<lbrace> \<acute>ret__unsigned_long = from_bool (sameObjectAs capa capb) \<rbrace>" 3502 apply vcg 3503 apply (clarsimp simp: sameObjectAs_def isArchCap_tag_def2) 3504 apply (case_tac capa, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3505 isCap_simps cap_tag_defs 3506 from_bool_def false_def) 3507 apply fastforce+ 3508 \<comment> \<open>capa is an arch cap\<close> 3509 apply (frule cap_get_tag_isArchCap_unfolded_H_cap) 3510 apply (simp add: isArchCap_tag_def2) 3511 apply (rule conjI, rule impI, clarsimp, rule impI)+ 3512 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3513 isCap_simps cap_tag_defs)[1] 3514 apply ((fastforce)+)[7] 3515 \<comment> \<open>capb is an arch cap\<close> 3516 apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) 3517 apply (fastforce simp: isArchCap_tag_def2 linorder_not_less [symmetric])+ 3518 \<comment> \<open>capa is an irq handler cap\<close> 3519 apply (case_tac capb, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3520 isCap_simps cap_tag_defs) 3521 apply fastforce+ 3522 \<comment> \<open>capb is an arch cap\<close> 3523 apply (frule cap_get_tag_isArchCap_unfolded_H_cap) 3524 apply (fastforce simp: isArchCap_tag_def2)+ 3525 done 3526 3527lemma sameRegionAs_EndpointCap: 3528 shows "\<lbrakk>ccap_relation capa capc; 3529 RetypeDecls_H.sameRegionAs (capability.EndpointCap x y z u v) capa\<rbrakk> 3530 \<Longrightarrow> cap_get_tag capc = scast cap_endpoint_cap" 3531 apply (simp add: sameRegionAs_def Let_def) 3532 apply (case_tac capa; 3533 simp add: isUntypedCap_def isEndpointCap_def isNotificationCap_def 3534 isCNodeCap_def isThreadCap_def isReplyCap_def isIRQControlCap_def 3535 isIRQHandlerCap_def isArchObjectCap_def) 3536 apply (clarsimp simp: ccap_relation_def map_option_case) 3537 apply (case_tac "cap_lift capc"; simp) 3538 apply (simp add: cap_to_H_def) 3539 apply (case_tac a; simp) 3540 apply (simp add:cap_endpoint_cap_lift cap_endpoint_cap_lift_def) 3541 apply (rename_tac zombie_cap) 3542 apply (case_tac "isZombieTCB_C (capZombieType_CL zombie_cap)"; simp add: Let_def) 3543 done 3544 3545lemma sameRegionAs_NotificationCap: 3546 shows "\<lbrakk>ccap_relation capa capc; 3547 RetypeDecls_H.sameRegionAs 3548 (capability.NotificationCap x y z u ) capa\<rbrakk> 3549 \<Longrightarrow> cap_get_tag capc = scast cap_notification_cap" 3550 apply (simp add: sameRegionAs_def Let_def) 3551 apply (case_tac capa; 3552 simp add: isUntypedCap_def isEndpointCap_def isNotificationCap_def 3553 isCNodeCap_def isThreadCap_def isReplyCap_def isIRQControlCap_def 3554 isIRQHandlerCap_def isArchObjectCap_def) 3555 apply (clarsimp simp: ccap_relation_def map_option_case) 3556 apply (case_tac "cap_lift capc"; simp) 3557 apply (simp add: cap_to_H_def) 3558 apply (case_tac a; simp) 3559 apply (simp add: cap_notification_cap_lift cap_notification_cap_lift_def) 3560 apply (rename_tac zombie_cap) 3561 apply (case_tac "isZombieTCB_C (capZombieType_CL zombie_cap)"; simp add: Let_def) 3562 done 3563 3564lemma isMDBParentOf_spec: 3565 notes option.case_cong_weak [cong] 3566 shows "\<forall>ctea cte_a cteb cte_b. 3567 \<Gamma> \<turnstile> {s. cslift s (cte_a_' s) = Some cte_a \<and> 3568 ccte_relation ctea cte_a \<and> 3569 cslift s (cte_b_' s) = Some cte_b \<and> 3570 ccte_relation cteb cte_b \<and> 3571 capAligned (cteCap cteb) \<and> 3572 (\<exists>s. s \<turnstile>' (cteCap ctea)) } 3573 Call isMDBParentOf_'proc 3574 \<lbrace> \<acute>ret__unsigned_long = from_bool (isMDBParentOf ctea cteb) \<rbrace>" 3575 apply (intro allI, rule conseqPre) 3576 apply vcg 3577 apply (clarsimp simp: isMDBParentOf_def) 3578 apply (frule_tac cte=ctea in ccte_relation_ccap_relation) 3579 apply (frule_tac cte=cteb in ccte_relation_ccap_relation) 3580 3581 apply (rule conjI, clarsimp simp: typ_heap_simps dest!: lift_t_g) 3582 apply (intro conjI impI) 3583 apply (simp add: ccte_relation_def map_option_case) 3584 apply (simp add: cte_lift_def) 3585 apply (clarsimp simp: cte_to_H_def mdb_node_to_H_def split: option.split_asm) 3586 apply (clarsimp simp: Let_def false_def from_bool_def to_bool_def 3587 split: if_split bool.splits) 3588 apply ((clarsimp simp: typ_heap_simps dest!: lift_t_g)+)[3] 3589 apply (rule_tac x="cteCap ctea" in exI, rule conjI) 3590 apply (clarsimp simp: ccte_relation_ccap_relation typ_heap_simps 3591 dest!: lift_t_g) 3592 apply (rule_tac x="cteCap cteb" in exI, rule conjI) 3593 apply (clarsimp simp: ccte_relation_ccap_relation typ_heap_simps 3594 dest!: lift_t_g) 3595 apply (clarsimp simp: ccte_relation_def map_option_case) 3596 apply (simp add: cte_lift_def) 3597 apply (clarsimp simp: cte_to_H_def mdb_node_to_H_def 3598 split: option.split_asm) 3599 3600 apply (rule conjI) 3601 \<comment> \<open>sameRegionAs = 0\<close> 3602 apply (rule impI) 3603 apply (clarsimp simp: from_bool_def false_def 3604 split: if_split bool.splits) 3605 3606 \<comment> \<open>sameRegionAs \<noteq> 0\<close> 3607 apply (clarsimp simp: from_bool_def false_def) 3608 apply (clarsimp cong:bool.case_cong if_cong simp: typ_heap_simps) 3609 3610 apply (rule conjI) 3611 \<comment> \<open>cap_get_tag of cte_a is an endpoint\<close> 3612 apply clarsimp 3613 apply (frule cap_get_tag_EndpointCap) 3614 apply simp 3615 apply (clarsimp simp: to_bool_def isNotificationCap_def isEndpointCap_def true_def) \<comment> \<open>badge of A is not 0 now\<close> 3616 3617 3618 apply (subgoal_tac "cap_get_tag (cte_C.cap_C cte_b) = scast cap_endpoint_cap") \<comment> \<open>needed also after\<close> 3619 prefer 2 3620 apply (rule sameRegionAs_EndpointCap, assumption+) 3621 3622 apply (clarsimp simp: if_1_0_0 typ_heap_simps' Let_def case_bool_If) 3623 apply (frule_tac cap="(cap_to_H x2c)" in cap_get_tag_EndpointCap) 3624 apply (clarsimp split: if_split_asm simp: if_distrib [where f=scast]) 3625 3626 apply (clarsimp, rule conjI) 3627 \<comment> \<open>cap_get_tag of cte_a is an notification\<close> 3628 apply clarsimp 3629 apply (frule cap_get_tag_NotificationCap) 3630 apply simp 3631 apply (clarsimp simp: to_bool_def isNotificationCap_def isEndpointCap_def true_def) \<comment> \<open>badge of A is not 0 now\<close> 3632 3633 3634 apply (subgoal_tac "cap_get_tag (cte_C.cap_C cte_b) = scast cap_notification_cap") \<comment> \<open>needed also after\<close> 3635 prefer 2 3636 apply (rule sameRegionAs_NotificationCap, assumption+) 3637 3638 apply (rule conjI, simp) 3639 apply clarsimp 3640 apply (simp add: Let_def case_bool_If) 3641 apply (frule_tac cap="(cap_to_H x2c)" in cap_get_tag_NotificationCap) 3642 apply clarsimp 3643 3644 \<comment> \<open>main goal\<close> 3645 apply clarsimp 3646 apply (simp add: to_bool_def) 3647 apply (subgoal_tac "(\<not> (isEndpointCap (cap_to_H x2b))) \<and> ( \<not> (isNotificationCap (cap_to_H x2b)))") 3648 apply (clarsimp simp: true_def) 3649 apply (clarsimp simp: cap_get_tag_isCap [symmetric]) 3650 done 3651 3652lemma updateCapData_spec: 3653 "\<forall>cap. \<Gamma> \<turnstile> \<lbrace> ccap_relation cap \<acute>cap \<and> preserve = to_bool (\<acute>preserve) \<and> newData = \<acute>newData\<rbrace> 3654 Call updateCapData_'proc 3655 \<lbrace> ccap_relation (updateCapData preserve newData cap) \<acute>ret__struct_cap_C \<rbrace>" 3656 apply (rule allI, rule conseqPre) 3657 apply vcg 3658 apply (clarsimp simp: if_1_0_0) 3659 3660 apply (simp add: updateCapData_def) 3661 3662 apply (case_tac cap, simp_all add: cap_get_tag_isCap_unfolded_H_cap 3663 isCap_simps from_bool_def isArchCap_tag_def2 cap_tag_defs Let_def) 3664 \<comment> \<open>NotificationCap\<close> 3665 apply clarsimp 3666 apply (frule cap_get_tag_isCap_unfolded_H_cap(3)) 3667 apply (frule (1) iffD1[OF cap_get_tag_NotificationCap]) 3668 apply clarsimp 3669 3670 apply (intro conjI impI) 3671 \<comment> \<open>preserve is zero and capNtfnBadge_CL \<dots> = 0\<close> 3672 apply clarsimp 3673 apply (clarsimp simp:cap_notification_cap_lift_def cap_lift_def cap_tag_defs) 3674 apply (simp add: ccap_relation_def cap_lift_def cap_tag_defs cap_to_H_def) 3675 \<comment> \<open>preserve is zero and capNtfnBadge_CL \<dots> \<noteq> 0\<close> 3676 apply clarsimp 3677 apply (simp add: ccap_relation_NullCap_iff cap_tag_defs) 3678 \<comment> \<open>preserve is not zero\<close> 3679 apply clarsimp 3680 apply (simp add: to_bool_def) 3681 apply (case_tac "preserve_' x = 0 \<and> capNtfnBadge_CL (cap_notification_cap_lift (cap_' x))= 0", 3682 clarsimp) 3683 apply (simp add: if_not_P) 3684 apply (simp add: ccap_relation_NullCap_iff cap_tag_defs) 3685 3686 \<comment> \<open>EndpointCap\<close> 3687 apply clarsimp 3688 apply (frule cap_get_tag_isCap_unfolded_H_cap(4)) 3689 apply (frule (1) iffD1[OF cap_get_tag_EndpointCap]) 3690 apply clarsimp 3691 3692 apply (intro impI conjI) 3693 \<comment> \<open>preserve is zero and capNtfnBadge_CL \<dots> = 0\<close> 3694 apply clarsimp 3695 apply (clarsimp simp:cap_endpoint_cap_lift_def cap_lift_def cap_tag_defs) 3696 apply (simp add: ccap_relation_def cap_lift_def cap_tag_defs cap_to_H_def) 3697 \<comment> \<open>preserve is zero and capNtfnBadge_CL \<dots> \<noteq> 0\<close> 3698 apply clarsimp 3699 apply (simp add: ccap_relation_NullCap_iff cap_tag_defs) 3700 \<comment> \<open>preserve is not zero\<close> 3701 apply clarsimp 3702 apply (simp add: to_bool_def) 3703 apply (case_tac "preserve_' x = 0 \<and> capEPBadge_CL (cap_endpoint_cap_lift (cap_' x))= 0", clarsimp) 3704 apply (simp add: if_not_P) 3705 apply (simp add: ccap_relation_NullCap_iff cap_tag_defs) 3706 3707 \<comment> \<open>ArchObjectCap\<close> 3708 apply clarsimp 3709 apply (frule cap_get_tag_isArchCap_unfolded_H_cap) 3710 apply (simp add: isArchCap_tag_def2) 3711 apply (simp add: X64_H.updateCapData_def) 3712 3713 \<comment> \<open>CNodeCap\<close> 3714 apply (clarsimp simp: cteRightsBits_def cteGuardBits_def) 3715 apply (frule cap_get_tag_isCap_unfolded_H_cap(10)) 3716 apply (frule (1) iffD1[OF cap_get_tag_CNodeCap]) 3717 apply clarsimp 3718 3719 apply (thin_tac "ccap_relation x y" for x y) 3720 apply (thin_tac "ret__unsigned_long_' t = v" for t v)+ 3721 3722 apply (simp add: seL4_CNode_CapData_lift_def fupdate_def word_size word_less_nat_alt mask_def 3723 cong: if_cong) 3724 apply (simp only: unat_word_ariths(1)) 3725 apply (rule ssubst [OF nat_mod_eq' [where n = "2 ^ len_of TYPE(64)"]]) 3726 \<comment> \<open>unat (\<dots> && 0x3F) + unat (\<dots> mod 0x40) < 2 ^ len_of TYPE(64)\<close> 3727 apply (rule order_le_less_trans, rule add_le_mono) 3728 apply (rule word_le_nat_alt[THEN iffD1]) 3729 apply (rule word_and_le1) 3730 apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap) 3731 apply (rule word_le_nat_alt[THEN iffD1]) 3732 apply (rule word_and_le1) 3733 apply (simp add: mask_def) 3734 3735 apply (simp add: word_sle_def) 3736 apply (rule conjI, clarsimp simp: ccap_relation_NullCap_iff cap_tag_defs) 3737 apply clarsimp 3738 apply (rule conjI) 3739 apply (rule unat_less_power[where sz=6, simplified], simp add: word_bits_def) 3740 apply (rule and_mask_less'[where n=6, unfolded mask_def, simplified], simp) 3741 3742 apply clarsimp 3743 apply (simp add: ccap_relation_def c_valid_cap_def cl_valid_cap_def 3744 cap_lift_cnode_cap cap_tag_defs cap_to_H_simps 3745 cap_cnode_cap_lift_def) 3746 apply (simp add: word_bw_assocs word_bw_comms word_bw_lcs) 3747 done 3748 3749abbreviation 3750 "deriveCap_xf \<equiv> liftxf errstate deriveCap_ret_C.status_C deriveCap_ret_C.cap_C ret__struct_deriveCap_ret_C_'" 3751 3752 3753lemma ensureNoChildren_ccorres: 3754 "ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_') 3755 (\<lambda>s. valid_objs' s \<and> valid_mdb' s) (UNIV \<inter> \<lbrace>slot = ptr_val (\<acute>slot)\<rbrace>) [] 3756 (ensureNoChildren slot) (Call ensureNoChildren_'proc)" 3757 apply (cinit lift: slot_') 3758 apply (rule ccorres_liftE_Seq) 3759 apply (rule ccorres_getCTE) 3760 apply (rule ccorres_move_c_guard_cte) 3761 3762 apply (rule_tac P= "\<lambda> s. valid_objs' s \<and> valid_mdb' s \<and> ctes_of s (ptr_val slota) = Some cte" 3763 and P' =UNIV in ccorres_from_vcg_throws) 3764 apply (rule allI, rule conseqPre, vcg) 3765 apply clarsimp 3766 3767 apply (frule (1) rf_sr_ctes_of_clift, clarsimp) 3768 apply (simp add: typ_heap_simps) 3769 3770 apply (clarsimp simp: whenE_def throwError_def return_def nullPointer_def liftE_bindE) 3771 3772 apply (clarsimp simp: returnOk_def return_def) \<comment> \<open>solve the case where mdbNext is zero\<close> 3773 3774 \<comment> \<open>main goal\<close> 3775 apply (simp add: ccte_relation_def) 3776 apply (frule_tac cte="cte_to_H y" in valid_mdb_ctes_of_next, simp+) 3777 apply (clarsimp simp: cte_wp_at_ctes_of) 3778 apply (frule_tac cte=cte in rf_sr_ctes_of_clift, assumption, clarsimp) 3779 apply (rule conjI) 3780 apply (frule_tac cte="(cte_to_H ya)" in ctes_of_valid', assumption, simp) 3781 apply (rule valid_capAligned, assumption) 3782 apply (rule conjI) 3783 apply (frule_tac cte="(cte_to_H y)" in ctes_of_valid', assumption, simp) 3784 apply blast 3785 3786 apply clarsimp 3787 apply (rule conjI) 3788 \<comment> \<open>isMDBParentOf is not zero\<close> 3789 apply clarsimp 3790 apply (simp add: from_bool_def) 3791 apply (case_tac "isMDBParentOf (cte_to_H y) (cte_to_H ya)", simp_all)[1] 3792 3793 apply (simp add: bind_def) 3794 apply (simp add: split_paired_Bex) 3795 apply (clarsimp simp: in_getCTE_cte_wp_at') 3796 apply (simp add: cte_wp_at_ctes_of) 3797 apply (simp add: syscall_error_rel_def EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def) 3798 apply (simp add: syscall_error_to_H_cases(9)) 3799 \<comment> \<open>isMDBParentOf is zero\<close> 3800 apply clarsimp 3801 apply (simp add: from_bool_def) 3802 apply (case_tac "isMDBParentOf (cte_to_H y) (cte_to_H ya)", simp_all)[1] 3803 apply (simp add: bind_def) 3804 apply (simp add: split_paired_Bex) 3805 apply (clarsimp simp: in_getCTE_cte_wp_at') 3806 apply (simp add: cte_wp_at_ctes_of) 3807 apply (simp add: returnOk_def return_def) 3808 3809 \<comment> \<open>last goal\<close> 3810 apply clarsimp 3811 apply (simp add: cte_wp_at_ctes_of) 3812 done 3813 3814lemma Arch_deriveCap_ccorres: 3815 "ccorres (syscall_error_rel \<currency> ccap_relation) deriveCap_xf 3816 \<top> (UNIV \<inter> {s. ccap_relation (ArchObjectCap cap) (cap_' s)}) [] 3817 (Arch.deriveCap slot cap) (Call Arch_deriveCap_'proc)" 3818 apply (cinit lift: cap_') 3819 apply csymbr 3820 apply (unfold X64_H.deriveCap_def Let_def) 3821 apply (fold case_bool_If) 3822 apply wpc 3823 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3824 ccorres_cond_iffs) 3825 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3826 apply (rule allI, rule conseqPre, vcg) 3827 apply clarsimp 3828 apply (rule context_conjI) 3829 apply (simp add: cap_get_tag_isCap_ArchObject) 3830 apply (clarsimp simp: returnOk_def return_def) 3831 subgoal by (simp add: ccap_relation_def cap_lift_def Let_def 3832 cap_tag_defs cap_to_H_def 3833 cap_page_table_cap_lift_def) 3834 apply wpc 3835 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3836 ccorres_cond_iffs) 3837 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3838 apply (rule allI, rule conseqPre, vcg) 3839 apply clarsimp 3840 apply (rule context_conjI) 3841 apply (simp add: cap_get_tag_isCap_ArchObject) 3842 apply (clarsimp simp: throwError_def return_def 3843 errstate_def syscall_error_rel_def 3844 syscall_error_to_H_cases 3845 exception_defs) 3846 subgoal by (simp add: ccap_relation_def cap_lift_def Let_def 3847 cap_tag_defs cap_to_H_def to_bool_def 3848 cap_page_table_cap_lift_def 3849 split: if_split_asm) 3850 apply wpc 3851 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3852 ccorres_cond_iffs) 3853 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3854 apply (rule allI, rule conseqPre, vcg) 3855 apply clarsimp 3856 apply (rule context_conjI) 3857 apply (simp add: cap_get_tag_isCap_ArchObject) 3858 apply (clarsimp simp: returnOk_def return_def) 3859 subgoal by (simp add: ccap_relation_def cap_lift_def Let_def 3860 cap_tag_defs cap_to_H_def 3861 cap_page_directory_cap_lift_def) 3862 apply wpc 3863 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3864 ccorres_cond_iffs) 3865 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3866 apply (rule allI, rule conseqPre, vcg) 3867 apply clarsimp 3868 apply (rule context_conjI) 3869 apply (simp add: cap_get_tag_isCap_ArchObject) 3870 apply (clarsimp simp: throwError_def return_def 3871 errstate_def syscall_error_rel_def 3872 syscall_error_to_H_cases 3873 exception_defs) 3874 subgoal by (simp add: ccap_relation_def cap_lift_def Let_def 3875 cap_tag_defs cap_to_H_def to_bool_def 3876 cap_page_directory_cap_lift_def 3877 split: if_split_asm) 3878 \<comment> \<open>PDPTCap\<close> 3879 apply wpc 3880 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3881 ccorres_cond_iffs) 3882 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3883 apply (rule allI, rule conseqPre, vcg) 3884 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap isCap_simps) 3885 apply (rule context_conjI) 3886 apply (clarsimp simp: returnOk_def return_def cap_tag_defs) 3887 apply (clarsimp simp: returnOk_def return_def exception_defs) 3888 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3889 apply (clarsimp simp: cap_pdpt_cap_lift ccap_relation_def cap_to_H_def) 3890 apply wpc 3891 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3892 ccorres_cond_iffs) 3893 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3894 apply (rule allI, rule conseqPre, vcg) 3895 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap isCap_simps) 3896 apply (rule context_conjI) 3897 apply (clarsimp simp: throwError_def return_def cap_tag_defs 3898 errstate_def syscall_error_rel_def 3899 syscall_error_to_H_cases 3900 exception_defs) 3901 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3902 apply (clarsimp simp: cap_pdpt_cap_lift ccap_relation_def cap_to_H_def to_bool_def 3903 split: if_split_asm) 3904 apply (clarsimp simp: throwError_def return_def 3905 errstate_def syscall_error_rel_def 3906 syscall_error_to_H_cases 3907 exception_defs) 3908 \<comment> \<open>PML4Cap\<close> 3909 apply wpc 3910 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3911 ccorres_cond_iffs) 3912 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3913 apply (rule allI, rule conseqPre, vcg) 3914 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap isCap_simps) 3915 apply (rule context_conjI) 3916 apply (clarsimp simp: returnOk_def return_def) 3917 apply (clarsimp simp: returnOk_def return_def exception_defs) 3918 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3919 apply (clarsimp simp: cap_pml4_cap_lift ccap_relation_def cap_to_H_def) 3920 apply wpc 3921 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3922 ccorres_cond_iffs) 3923 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3924 apply (rule allI, rule conseqPre, vcg) 3925 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap isCap_simps) 3926 apply (rule context_conjI) 3927 apply (clarsimp simp: throwError_def return_def 3928 errstate_def syscall_error_rel_def 3929 syscall_error_to_H_cases 3930 exception_defs) 3931 apply (frule cap_get_tag_isCap_unfolded_H_cap) 3932 apply (clarsimp simp: cap_pml4_cap_lift ccap_relation_def cap_to_H_def to_bool_def 3933 split: if_split_asm) 3934 apply (clarsimp simp: throwError_def return_def 3935 errstate_def syscall_error_rel_def 3936 syscall_error_to_H_cases 3937 exception_defs) 3938 \<comment> \<open>PageCap\<close> 3939 apply wpc 3940 apply (clarsimp simp: cap_get_tag_isCap_ArchObject 3941 ccorres_cond_iffs) 3942 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3943 apply (rule allI, rule conseqPre, vcg) 3944 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap isCap_simps) 3945 apply (rule context_conjI) 3946 apply (simp add: cap_tag_defs) 3947 apply (clarsimp simp: returnOk_def return_def isCap_simps) 3948 subgoal apply (frule cap_get_tag_isCap_unfolded_H_cap) 3949 by (clarsimp simp: cap_frame_cap_lift[simplified cap_tag_defs, simplified] cap_tag_defs 3950 ccap_relation_def cap_to_H_def asidInvalid_def maptype_to_H_def 3951 vm_page_map_type_defs c_valid_cap_def cl_valid_cap_def 3952 split: if_splits) 3953 apply (simp add: cap_get_tag_isCap_ArchObject 3954 ccorres_cond_iffs) 3955 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3956 apply (rule allI, rule conseqPre, vcg) 3957 apply (clarsimp simp: returnOk_def return_def subset_iff 3958 split: bool.split) 3959 apply (cases cap, simp_all add: isCap_simps ccap_relation_NullCap_iff)[1] 3960 apply clarsimp 3961 done 3962 3963 3964lemma isArchCap_T_isArchObjectCap: 3965 "isArchCap \<top> = isArchObjectCap" 3966 by (rule ext, auto simp: isCap_simps) 3967 3968lemma deriveCap_ccorres': 3969 "ccorres (syscall_error_rel \<currency> ccap_relation) deriveCap_xf 3970 (valid_objs' and valid_mdb') (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. slot_' s = Ptr slot}) [] 3971 (deriveCap slot cap) (Call deriveCap_'proc)" 3972 apply (cinit lift: cap_' slot_') 3973 apply csymbr 3974 apply (fold case_bool_If) 3975 apply wpc 3976 apply (clarsimp simp: cap_get_tag_isCap isCap_simps from_bool_def) 3977 apply csymbr 3978 apply (clarsimp simp: cap_get_tag_isCap) 3979 apply (rule ccorres_from_vcg_throws [where P=\<top> and P' = UNIV]) 3980 apply (simp add: returnOk_def return_def ccap_relation_NullCap_iff) 3981 apply (rule allI, rule conseqPre) 3982 apply vcg 3983 apply clarsimp 3984 apply wpc 3985 apply (clarsimp simp: isCap_simps cap_get_tag_isCap from_bool_def) 3986 apply csymbr 3987 apply (clarsimp simp: isCap_simps cap_get_tag_isCap) 3988 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 3989 apply (rule allI, rule conseqPre, vcg) 3990 apply (clarsimp simp: returnOk_def return_def 3991 ccap_relation_NullCap_iff) 3992 apply wpc 3993 apply (clarsimp simp: isCap_simps cap_get_tag_isCap from_bool_def) 3994 apply csymbr 3995 apply (clarsimp simp: isCap_simps cap_get_tag_isCap) 3996 apply (rule ccorres_rhs_assoc)+ 3997 apply ctac_print_xf 3998 apply (rule ccorres_split_nothrow_call_novcgE 3999 [where xf'="ret__unsigned_long_'"]) 4000 apply (rule ensureNoChildren_ccorres) 4001 apply simp+ 4002 apply ceqv 4003 apply simp 4004 apply (rule_tac P'="\<lbrace>\<acute>ret__unsigned_long = scast EXCEPTION_NONE\<rbrace>" 4005 in ccorres_from_vcg_throws[where P=\<top>]) 4006 apply (rule allI, rule conseqPre, vcg) 4007 apply (clarsimp simp: return_def returnOk_def) 4008 apply simp 4009 apply (rule_tac P'="{s. ret__unsigned_long_' s = rv' \<and> errstate s = err'}" 4010 in ccorres_from_vcg_throws[where P=\<top>]) 4011 apply (rule allI, rule conseqPre, vcg) 4012 apply (clarsimp simp: throwError_def return_def 4013 errstate_def) 4014 apply wp 4015 apply wpc 4016 apply (clarsimp simp: isCap_simps cap_get_tag_isCap from_bool_def) 4017 apply csymbr 4018 apply (clarsimp simp: isCap_simps cap_get_tag_isCap) 4019 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 4020 apply (rule allI, rule conseqPre, vcg) 4021 apply (clarsimp simp: returnOk_def return_def 4022 ccap_relation_NullCap_iff) 4023 apply wpc 4024 apply (rule ccorres_split_throws[rotated]) 4025 apply (clarsimp simp: cap_get_tag_isCap 4026 liftME_def Let_def isArchCap_T_isArchObjectCap) 4027 apply vcg 4028 apply (clarsimp simp: cap_get_tag_isCap 4029 liftME_def Let_def isArchCap_T_isArchObjectCap 4030 ccorres_cond_univ_iff from_bool_def) 4031 apply (rule ccorres_add_returnOk) 4032 apply (rule ccorres_split_nothrow_call_novcgE 4033 [where xf'=ret__struct_deriveCap_ret_C_']) 4034 apply (rule Arch_deriveCap_ccorres) 4035 apply simp+ 4036 apply (rule ceqv_refl) 4037 apply (rule_tac P'="\<lbrace>\<acute>ret__struct_deriveCap_ret_C 4038 = rv'\<rbrace>" 4039 in ccorres_from_vcg_throws[where P=\<top>]) 4040 apply (rule allI, rule conseqPre, vcg) 4041 apply (clarsimp simp: return_def returnOk_def) 4042 apply (rule_tac P'="{s. (ret__struct_deriveCap_ret_C_' s) 4043 = rv' \<and> errstate s = err'}" 4044 in ccorres_from_vcg_throws[where P=\<top>]) 4045 apply (rule allI, rule conseqPre, vcg) 4046 apply (clarsimp simp: return_def throwError_def) 4047 apply wp 4048 apply (simp add: cap_get_tag_isCap isArchCap_T_isArchObjectCap from_bool_def) 4049 apply csymbr 4050 apply (simp add: cap_get_tag_isCap) 4051 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 4052 apply (rule allI, rule conseqPre, vcg) 4053 apply (clarsimp simp: return_def returnOk_def) 4054 apply (clarsimp simp: errstate_def isCap_simps 4055 Collect_const_mem from_bool_0 4056 cap_get_tag_isArchCap_unfolded_H_cap) 4057 done 4058 4059 4060lemma deriveCap_ccorres: 4061 "ccorres (syscall_error_rel \<currency> ccap_relation) deriveCap_xf 4062 (invs') (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. slot_' s = Ptr slot}) [] 4063 (deriveCap slot cap) (Call deriveCap_'proc)" 4064 apply (rule ccorres_guard_imp2, rule deriveCap_ccorres') 4065 apply fastforce 4066 done 4067 4068lemma ensureEmptySlot_ccorres: 4069 "ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_') 4070 \<top> (UNIV \<inter> \<lbrace>slot = ptr_val (\<acute>slot)\<rbrace>) [] 4071 (ensureEmptySlot slot) (Call ensureEmptySlot_'proc)" 4072 apply (cinit lift: slot_') 4073 apply (rule ccorres_liftE_Seq) 4074 apply (rule ccorres_getCTE) 4075 apply (rule ccorres_move_c_guard_cte) 4076 apply (rule_tac P= "\<lambda> s. ctes_of s (ptr_val slota) = Some cte" 4077 and P' =UNIV in ccorres_from_vcg_throws) 4078 apply (rule allI, rule conseqPre, vcg) 4079 apply clarsimp 4080 4081 apply (frule (1) rf_sr_ctes_of_clift, clarsimp) 4082 apply (simp add: typ_heap_simps) 4083 4084 apply (rule conjI) 4085 apply (clarsimp simp: unlessE_def throwError_def return_def) 4086 apply (subgoal_tac "cap_to_H (cap_CL y) \<noteq> capability.NullCap") 4087 apply simp 4088 apply (simp add: syscall_error_rel_def EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def) 4089 apply (rule syscall_error_to_H_cases(8)) 4090 apply simp 4091 apply (subst cap_get_tag_NullCap [symmetric]) 4092 prefer 2 apply assumption 4093 apply (simp add: ccap_relation_def c_valid_cte_def) 4094 4095 apply (clarsimp simp: unlessE_def throwError_def return_def) 4096 apply (subgoal_tac "cap_to_H (cap_CL y) = capability.NullCap") 4097 apply simp 4098 apply (simp add: returnOk_def return_def) 4099 apply (subst cap_get_tag_NullCap [symmetric]) 4100 prefer 2 apply assumption 4101 apply (simp add: ccap_relation_def c_valid_cte_def) 4102 4103 apply clarsimp 4104 apply (simp add: cte_wp_at_ctes_of) 4105done 4106 4107lemma updateMDB_set_mdbPrev: 4108 "ccorres dc xfdc 4109 (\<lambda>s. is_aligned slota cteSizeBits) 4110 {s. slotc = slota } hs 4111 (updateMDB ptr (mdbPrev_update (\<lambda>_. slota))) 4112 (IF ptr \<noteq> 0 4113 THEN 4114 Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr ptr:: cte_C ptr)\<rbrace> 4115 (call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr ptr:: cte_C ptr\<rightarrow>[''cteMDBNode_C'']), 4116 v64_' := slotc |)) 4117 mdb_node_ptr_set_mdbPrev_'proc (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a))) 4118 FI)" 4119 apply (rule ccorres_guard_imp2) 4120 apply (rule ccorres_Cond_rhs) 4121 apply (rule ccorres_updateMDB_cte_at) 4122 apply (ctac add: ccorres_updateMDB_set_mdbPrev) 4123 apply (ctac ccorres: ccorres_updateMDB_skip) 4124 apply (simp) 4125 done 4126 4127lemma updateMDB_set_mdbNext: 4128 "ccorres dc xfdc 4129 (\<lambda>s. is_aligned slota cteSizeBits \<and> canonical_address slota) 4130 {s. slotc = slota} hs 4131 (updateMDB ptr (mdbNext_update (\<lambda>_. slota))) 4132 (IF ptr \<noteq> 0 4133 THEN 4134 Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr ptr:: cte_C ptr)\<rbrace> 4135 (call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr ptr:: cte_C ptr\<rightarrow>[''cteMDBNode_C'']), 4136 v64_' := slotc |)) 4137 mdb_node_ptr_set_mdbNext_'proc (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a))) 4138 FI)" 4139 apply (rule ccorres_guard_imp2) 4140 apply (rule ccorres_Cond_rhs) 4141 apply (rule ccorres_updateMDB_cte_at) 4142 apply (ctac add: ccorres_updateMDB_set_mdbNext) 4143 apply (ctac ccorres: ccorres_updateMDB_skip) 4144 apply simp 4145 done 4146 4147end 4148end 4149