1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11theory Recycle_C 12imports Delete_C Retype_C 13begin 14 15context kernel_m 16begin 17 18lemma isArchPageCap_ArchObjectCap: 19 "isArchPageCap (ArchObjectCap acap) 20 = isPageCap acap" 21 by (simp add: isArchPageCap_def isPageCap_def) 22 23definition 24 "replicateHider \<equiv> replicate" 25 26lemma collapse_foldl_replicate: 27 "replicate (length xs) v = xs \<Longrightarrow> 28 foldl (@) [] (map (\<lambda>_. xs) ys) 29 = replicateHider (length xs * length ys) v" 30 apply (induct ys rule: rev_induct) 31 apply (simp add: replicateHider_def) 32 apply (simp add: replicateHider_def) 33 apply (subst add.commute, simp add: replicate_add) 34 done 35 36lemma coerce_memset_to_heap_update_user_data: 37 "heap_update_list x (replicateHider 4096 0) 38 = heap_update (Ptr x :: user_data_C ptr) 39 (user_data_C (FCP (\<lambda>_. 0)))" 40 apply (intro ext, simp add: heap_update_def) 41 apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) 42 apply (simp add: to_bytes_def size_of_def typ_info_simps user_data_C_tag_def) 43 apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def 44 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) 45 apply (simp add: typ_info_simps 46 user_context_C_tag_def thread_state_C_tag_def seL4_Fault_C_tag_def 47 lookup_fault_C_tag_def update_ti_t_ptr_0s 48 ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td 49 ti_typ_combine_empty_ti ti_typ_combine_td 50 align_of_def padup_def 51 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def 52 align_td_array' size_td_array) 53 apply (simp add: typ_info_array') 54 apply (subst access_ti_list_array) 55 apply simp 56 apply simp 57 apply (simp add: fcp_beta typ_info_word typ_info_ptr word_rsplit_0) 58 apply fastforce 59 apply (simp add: collapse_foldl_replicate) 60 done 61 62lemma clift_foldl_hrs_mem_update: 63 "\<lbrakk> \<forall>x \<in> set xs. hrs_htd s \<Turnstile>\<^sub>t f x; 64 \<And>x s. hrs_htd s \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) s) 65 = g (clift s :: ('a :: c_type) ptr \<rightharpoonup> 'a) x \<rbrakk> 66 \<Longrightarrow> 67 clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s xs) s) 68 = foldl g (clift s :: 'a ptr \<rightharpoonup> 'a) xs" 69 using [[hypsubst_thin]] 70 apply (cases s, clarsimp) 71 apply (induct xs arbitrary: a b) 72 apply (simp add: hrs_mem_update_def) 73 apply (clarsimp simp add: hrs_mem_update_def split_def hrs_htd_def) 74 done 75 76lemma map_to_user_data_aligned: 77 "\<lbrakk> map_to_user_data (ksPSpace s) x = Some y; pspace_aligned' s \<rbrakk> 78 \<Longrightarrow> is_aligned x pageBits" 79 apply (clarsimp simp: map_comp_eq projectKOs split: option.split_asm) 80 apply (drule(1) pspace_alignedD') 81 apply (simp add: objBits_simps) 82 done 83 84lemma help_force_intvl_range_conv: 85 "\<lbrakk> is_aligned (p::machine_word) n; v = 2 ^ n; n < word_bits \<rbrakk> 86 \<Longrightarrow> {p ..+ v} = {p .. p + 2 ^ n - 1}" 87 by (simp add: intvl_range_conv word_bits_def) 88 89lemma cmap_relation_If_upd: 90 "\<lbrakk> cmap_relation f g ptrfun rel; rel v v'; ptrfun ` S = S'; inj ptrfun \<rbrakk> 91 \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> S then Some v else f x) 92 (\<lambda>y. if y \<in> S' then Some v' else g y) 93 ptrfun rel" 94 apply (simp add: cmap_relation_def dom_If_Some) 95 apply (rule context_conjI) 96 apply blast 97 apply clarsimp 98 apply (case_tac "x \<in> S") 99 apply simp 100 apply clarsimp 101 apply (subst if_not_P) 102 apply (clarsimp simp: inj_eq) 103 apply (drule bspec, erule domI) 104 apply simp 105 done 106 107lemma length_replicateHider [simp]: 108 "length (replicateHider n x) = n" 109 by (simp add: replicateHider_def) 110 111lemma coerce_heap_update_to_heap_updates': 112 "n = chunk * m \<Longrightarrow> 113 heap_update_list x (replicateHider n 0) 114 = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s 115 (map (\<lambda>n. x + (of_nat n * of_nat chunk)) [0 ..< m]))" 116 using [[hypsubst_thin]] 117 apply clarsimp 118 apply (induct m arbitrary: x) 119 apply (rule ext, simp) 120 apply (simp add: replicateHider_def) 121 apply (rule ext) 122 apply (simp only: map_upt_unfold map_Suc_upt[symmetric]) 123 apply (simp add: replicate_add[folded replicateHider_def] 124 heap_update_list_concat_unfold 125 o_def field_simps 126 length_replicate[folded replicateHider_def]) 127 done 128 129lemma h_t_valid_dom_s: 130 "\<lbrakk> h_t_valid htd c_guard p; x = ptr_val (p :: ('a :: mem_type) ptr); 131 n = size_of TYPE ('a) \<rbrakk> 132 \<Longrightarrow> {x ..+ n} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s htd" 133 apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def 134 intvl_def) 135 apply (drule_tac x=k in spec, simp add: size_of_def) 136 apply (clarsimp simp: dom_s_def) 137 apply (drule_tac x=0 in map_leD, simp_all) 138 done 139 140lemma user_data_at_rf_sr_dom_s: 141 "\<lbrakk> typ_at' UserDataT x s; (s, s') \<in> rf_sr \<rbrakk> 142 \<Longrightarrow> {x ..+ 2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} 143 \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" 144 apply (drule rf_sr_heap_user_data_relation) 145 apply (drule user_data_at_ko) 146 apply (erule_tac x=x in cmap_relationE1) 147 apply (simp only: heap_to_user_data_def Let_def ko_at_projectKO_opt) 148 apply simp 149 apply (drule h_t_valid_clift) 150 apply (simp add: h_t_valid_dom_s pageBits_def) 151 done 152 153lemma device_data_at_rf_sr_dom_s: 154 "\<lbrakk> typ_at' UserDataDeviceT x s; (s, s') \<in> rf_sr \<rbrakk> 155 \<Longrightarrow> {x ..+ 2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} 156 \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" 157 apply (drule rf_sr_heap_device_data_relation) 158 apply (drule device_data_at_ko) 159 apply (erule_tac x=x in cmap_relationE1) 160 apply (simp only: heap_to_device_data_def Let_def ko_at_projectKO_opt) 161 apply simp 162 apply (drule h_t_valid_clift) 163 apply (simp add: h_t_valid_dom_s pageBits_def) 164 done 165 166lemma intvl_2_power_times_decomp: 167 "\<forall>y < 2 ^ (n - m). {x + y * 2 ^ m ..+ 2 ^ m} \<times> S \<subseteq> T 168 \<Longrightarrow> m \<le> n \<Longrightarrow> n < word_bits 169 \<Longrightarrow> {(x :: machine_word) ..+ 2 ^ n} \<times> S \<subseteq> T" 170 apply (clarsimp simp: intvl_def) 171 apply (drule_tac x="of_nat k >> m" in spec) 172 apply (drule mp) 173 apply (rule shiftr_less_t2n) 174 apply (rule word_of_nat_less) 175 apply (simp add: word_of_nat_less) 176 apply (erule subsetD) 177 apply (clarsimp simp: shiftl_t2n[simplified mult.commute mult.left_commute, symmetric] 178 shiftr_shiftl1) 179 apply (rule_tac x="unat (of_nat k && mask m :: machine_word)" in exI) 180 apply (simp add: field_simps word_plus_and_or_coroll2) 181 apply (simp add: word_bits_def unat_less_power and_mask_less') 182 done 183 184lemma flex_user_data_at_rf_sr_dom_s: 185 "\<lbrakk> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). 186 typ_at' UserDataT (x + p * 2 ^ pageBits) s); (s, s') \<in> rf_sr \<rbrakk> 187 \<Longrightarrow> {x ..+ 2 ^ pageBitsForSize sz} \<times> {SIndexVal, SIndexTyp 0} 188 \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" 189 apply (rule_tac m=pageBits in intvl_2_power_times_decomp, 190 simp_all add: pbfs_atleast_pageBits pbfs_less_wb') 191 apply (erule allEI, clarsimp) 192 apply (drule(1) user_data_at_rf_sr_dom_s) 193 apply (erule subsetD) 194 apply simp 195 done 196 197lemma hrs_mem_update_fold_eq: 198 "hrs_mem_update (fold f xs) 199 = fold (hrs_mem_update o f) xs" 200 apply (rule sym, induct xs) 201 apply (simp add: hrs_mem_update_def) 202 apply (simp add: hrs_mem_update_def fun_eq_iff) 203 done 204 205lemma power_user_page_foldl_zero_ranges: 206 " \<forall>p<2 ^ (pageBitsForSize sz - pageBits). 207 hrs_htd hrs \<Turnstile>\<^sub>t (Ptr (ptr + of_nat p * 0x1000) :: user_data_C ptr) 208 \<Longrightarrow> zero_ranges_are_zero rngs hrs 209 \<Longrightarrow> zero_ranges_are_zero rngs 210 (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (Ptr x) (user_data_C (arr x)) s) s 211 (map (\<lambda>n. ptr + of_nat n * 0x1000) [0..<2 ^ (pageBitsForSize sz - pageBits)])) 212 hrs)" 213 apply (simp add: foldl_conv_fold hrs_mem_update_fold_eq) 214 apply (rule conjunct1) 215 apply (rule fold_invariant[where P="\<lambda>hrs'. zero_ranges_are_zero rngs hrs' 216 \<and> hrs_htd hrs' = hrs_htd hrs" 217 and xs=xs and Q="\<lambda>x. x \<in> set xs" for xs], simp_all) 218 apply (subst zero_ranges_are_zero_update, simp_all) 219 apply clarsimp 220 done 221 222lemma heap_to_device_data_disj_mdf': 223 "\<lbrakk>is_aligned ptr (pageBitsForSize sz); ksPSpace \<sigma> a = Some obj; objBitsKO obj = pageBits; pspace_aligned' \<sigma>; 224 pspace_distinct' \<sigma>; pspace_no_overlap' ptr (pageBitsForSize sz) \<sigma>\<rbrakk> 225\<Longrightarrow> heap_to_device_data (ksPSpace \<sigma>) 226 (\<lambda>x. if x \<in> {ptr..+2 ^ (pageBitsForSize sz)} then 0 227 else underlying_memory (ksMachineState \<sigma>) x) 228 a = 229 heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a" 230 apply (cut_tac heap_to_device_data_disj_mdf[where ptr = ptr 231 and gbits = "pageBitsForSize sz - pageBits" and n = 1 232 and sz = "pageBitsForSize sz",simplified]) 233 apply (simp add: pbfs_atleast_pageBits pbfs_less_wb' field_simps| intro range_cover_full )+ 234 done 235 236lemma range_cover_nca_neg: "\<And>x p (off :: 9 word). 237 \<lbrakk>(x::machine_word) < 8; {p..+2 ^pageBits } \<inter> {ptr..ptr + (of_nat n * 2 ^ bits - 1)} = {}; 238 range_cover ptr sz bits n\<rbrakk> 239 \<Longrightarrow> p + ucast off * 8 + x \<notin> {ptr..+n * 2 ^ bits}" 240 apply (case_tac "n = 0") 241 apply simp 242 apply (subst range_cover_intvl,simp) 243 apply simp 244 apply (subgoal_tac " p + ucast off * 8 + x \<in> {p..+2 ^ pageBits}") 245 apply blast 246 apply (clarsimp simp: intvl_def) 247 apply (rule_tac x = "unat off * 8 + unat x" in exI) 248 apply (simp add: ucast_nat_def) 249 apply (rule nat_add_offset_less [where n = 3, simplified]) 250 apply (simp add: word_less_nat_alt) 251 apply (rule unat_lt2p) 252 apply (simp add: pageBits_def objBits_simps) 253 done 254 255lemmas unat_of_nat32' = unat_of_nat_eq[where 'a=32] 256 257lemma unat_of_nat_pageBitsForSize_32 [simp]: 258 "unat (of_nat (pageBitsForSize x)::32 word) = pageBitsForSize x" 259 apply (subst unat_of_nat32') 260 apply (rule order_le_less_trans, rule pageBitsForSize_le) 261 apply (simp add: word_bits_def) 262 apply simp 263 done 264 265lemma clearMemory_PageCap_ccorres: 266 "ccorres dc xfdc (invs' and valid_cap' (ArchObjectCap (PageCap ptr undefined mt sz False None)) 267 and (\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s) 268 and K ({ptr .. ptr + 2 ^ (pageBitsForSize sz) - 1} \<inter> kernel_data_refs = {}) 269 ) 270 (UNIV \<inter> {s. bits_' s = of_nat (pageBitsForSize sz)} 271 \<inter> {s. ptr___ptr_to_void_' s = Ptr ptr}) 272 [] 273 (doMachineOp (clearMemory ptr (2 ^ pageBitsForSize sz))) (Call clearMemory_'proc)" 274 (is "ccorres dc xfdc ?P ?P' [] ?m ?c") 275 apply (cinit' lift: bits_' ptr___ptr_to_void_') 276 apply (rule_tac P="capAligned (ArchObjectCap (PageCap ptr undefined mt sz False None))" 277 in ccorres_gen_asm) 278 apply (rule ccorres_Guard) 279 apply (simp add: clearMemory_def) 280 apply (rule_tac P="?P" in ccorres_from_vcg[where P'=UNIV]) 281 apply (rule allI, rule conseqPre, vcg) 282 apply (clarsimp simp: valid_cap'_def capAligned_def bit_simps 283 is_aligned_no_wrap'[OF _ word64_power_less_1]) 284 apply (subgoal_tac "3 \<le> pageBitsForSize sz") 285 prefer 2 286 apply (simp add: pageBitsForSize_def split: vmpage_size.split) 287 apply (clarsimp simp: bit_simps) 288 apply (rule conjI) 289 apply (erule is_aligned_weaken) 290 apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits) 291 apply (rule conjI) 292 apply (rule is_aligned_power2) 293 apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits) 294 apply (clarsimp simp: ghost_assertion_size_logic[unfolded o_def]) 295 apply (simp add: flex_user_data_at_rf_sr_dom_s bit_simps) 296 apply (clarsimp simp: field_simps word_size_def mapM_x_storeWord_step) 297 apply (simp add: doMachineOp_def split_def exec_gets) 298 apply (simp add: select_f_def simpler_modify_def bind_def) 299 apply (fold replicateHider_def)[1] 300 apply (subst coerce_heap_update_to_heap_updates' 301 [where chunk=4096 and m="2 ^ (pageBitsForSize sz - pageBits)"]) 302 apply (simp add: pageBitsForSize_def bit_simps split: vmpage_size.split) 303 apply (subst coerce_memset_to_heap_update_user_data) 304 apply (subgoal_tac "\<forall>p<2 ^ (pageBitsForSize sz - pageBits). 305 x \<Turnstile>\<^sub>c (Ptr (ptr + of_nat p * 0x1000) :: user_data_C ptr)") 306 prefer 2 307 apply (erule allfEI[where f=of_nat]) 308 apply (clarsimp simp: bit_simps) 309 apply (subst(asm) of_nat_power, assumption) 310 apply simp 311 apply (insert pageBitsForSize_32 [of sz])[1] 312 apply (erule order_le_less_trans [rotated]) 313 apply simp 314 apply (simp, drule ko_at_projectKO_opt[OF user_data_at_ko]) 315 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) 316 apply (erule cmap_relationE1, simp(no_asm) add: heap_to_user_data_def Let_def) 317 apply fastforce 318 subgoal by (simp add: pageBits_def typ_heap_simps) 319 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 320 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 321 clift_foldl_hrs_mem_update foldl_id 322 carch_state_relation_def fpu_null_state_relation_def 323 cmachine_state_relation_def 324 foldl_fun_upd_const[unfolded fun_upd_def] 325 power_user_page_foldl_zero_ranges 326 dom_heap_to_device_data) 327 apply (rule conjI[rotated]) 328 apply (simp add:pageBitsForSize_mess_multi) 329 apply (rule cmap_relationI) 330 apply (clarsimp simp: dom_heap_to_device_data cmap_relation_def) 331 apply (simp add:cuser_user_data_device_relation_def) 332 apply (subst help_force_intvl_range_conv, assumption) 333 subgoal by (simp add: pageBitsForSize_def bit_simps split: vmpage_size.split) 334 apply assumption 335 apply (subst heap_to_user_data_update_region) 336 apply (drule map_to_user_data_aligned, clarsimp) 337 apply (rule aligned_range_offset_mem[where m=pageBits], simp_all)[1] 338 apply (rule pbfs_atleast_pageBits) 339 apply (erule cmap_relation_If_upd) 340 apply (clarsimp simp: cuser_user_data_relation_def order_less_le_trans[OF unat_lt2p]) 341 apply (fold word_rsplit_0, simp add: word_rcat_rsplit)[1] 342 apply (rule image_cong[OF _ refl]) 343 apply (rule set_eqI, rule iffI) 344 apply (clarsimp simp del: atLeastAtMost_iff) 345 apply (drule map_to_user_data_aligned, clarsimp) 346 apply (simp only: mask_in_range[symmetric]) 347 apply (rule_tac x="unat ((xa && mask (pageBitsForSize sz)) >> pageBits)" in image_eqI) 348 apply (simp add: subtract_mask(2)[symmetric]) 349 apply (cut_tac w="xa - ptr" and n=pageBits in and_not_mask[symmetric]) 350 apply (simp add: shiftl_t2n field_simps pageBits_def) 351 apply (subst is_aligned_neg_mask_eq, simp_all)[1] 352 apply (erule aligned_sub_aligned, simp_all add: word_bits_def)[1] 353 apply (erule is_aligned_weaken) 354 apply (rule pbfs_atleast_pageBits[unfolded pageBits_def]) 355 apply simp 356 apply (rule unat_less_power) 357 apply (fold word_bits_def, simp) 358 apply (rule shiftr_less_t2n) 359 apply (simp add: pbfs_atleast_pageBits) 360 apply (rule and_mask_less_size) 361 apply (simp add: word_bits_def word_size) 362 apply (rule IntI) 363 apply (clarsimp simp del: atLeastAtMost_iff) 364 apply (subst aligned_range_offset_mem, assumption, simp_all)[1] 365 apply (rule order_le_less_trans[rotated], erule shiftl_less_t2n [OF of_nat_power], 366 simp_all add: word_bits_def)[1] 367 apply (insert pageBitsForSize_32 [of sz])[1] 368 apply (erule order_le_less_trans [rotated]) 369 subgoal by simp 370 subgoal by (simp add: pageBits_def shiftl_t2n field_simps) 371 apply (clarsimp simp: image_iff) 372 apply (rename_tac n) 373 apply (drule_tac x="of_nat n" in spec) 374 apply (simp add: bit_simps) 375 apply (simp add: of_nat_power[where 'a=64, folded word_bits_def]) 376 apply (simp add: pageBits_def ko_at_projectKO_opt[OF user_data_at_ko]) 377 apply (rule inj_Ptr) 378 by (simp add: word_bits_def capAligned_def word_of_nat_less valid_cap'_def) 379 380 381(* FIXME x64: asid_map 382lemma coerce_memset_to_heap_update_asidpool: 383 "heap_update_list x (replicateHider 4096 0) 384 = heap_update (Ptr x :: asid_pool_C ptr) 385 (asid_pool_C (FCP (\<lambda>x. Ptr 0)))" 386 apply (intro ext, simp add: heap_update_def) 387 apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) 388 apply (simp add: to_bytes_def size_of_def typ_info_simps asid_pool_C_tag_def) 389 apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def 390 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) 391 apply (simp add: typ_info_simps 392 user_context_C_tag_def thread_state_C_tag_def seL4_Fault_C_tag_def 393 lookup_fault_C_tag_def update_ti_t_ptr_0s 394 ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td 395 ti_typ_combine_empty_ti ti_typ_combine_td 396 align_of_def padup_def 397 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def 398 align_td_array' size_td_array) 399 apply (simp add: typ_info_array') 400 apply (subst access_ti_list_array) 401 apply simp 402 apply simp 403 apply (simp add: fcp_beta typ_info_word typ_info_ptr word_rsplit_0) 404 apply fastforce 405 apply (simp add: collapse_foldl_replicate) 406 done 407*) 408 409declare replicate_numeral [simp] 410 411lemma coerce_memset_to_heap_update_pte: 412 "heap_update_list x (replicateHider 8 0) 413 = heap_update (Ptr x :: pte_C ptr) 414 (pte_C.pte_C (FCP (\<lambda>x. 0)))" 415 apply (intro ext, simp add: heap_update_def) 416 apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) 417 apply (simp add: to_bytes_def size_of_def typ_info_simps pte_C_tag_def) 418 apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def 419 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) 420 apply (simp add: typ_info_simps align_td_array' size_td_array) 421 apply (simp add: typ_info_array' typ_info_word word_rsplit_0) 422 apply (simp add: numeral_nat word_rsplit_0) 423 apply (simp add: replicateHider_def) 424 done 425 426lemma coerce_memset_to_heap_update_pde: 427 "heap_update_list x (replicateHider 8 0) 428 = heap_update (Ptr x :: pde_C ptr) 429 (pde_C.pde_C (FCP (\<lambda>x. 0)))" 430 apply (intro ext, simp add: heap_update_def) 431 apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) 432 apply (simp add: to_bytes_def size_of_def typ_info_simps pde_C_tag_def) 433 apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def 434 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) 435 apply (simp add: typ_info_simps align_td_array' size_td_array) 436 apply (simp add: typ_info_array' typ_info_word word_rsplit_0) 437 apply (simp add: numeral_nat word_rsplit_0) 438 apply (simp add: replicateHider_def) 439 done 440 441lemma coerce_memset_to_heap_update_pdpte: 442 "heap_update_list x (replicateHider 8 0) 443 = heap_update (Ptr x :: pdpte_C ptr) 444 (pdpte_C.pdpte_C (FCP (\<lambda>x. 0)))" 445 apply (intro ext, simp add: heap_update_def) 446 apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) 447 apply (simp add: to_bytes_def size_of_def typ_info_simps pdpte_C_tag_def) 448 apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def 449 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) 450 apply (simp add: typ_info_simps align_td_array' size_td_array) 451 apply (simp add: typ_info_array' typ_info_word word_rsplit_0) 452 apply (simp add: numeral_nat word_rsplit_0) 453 apply (simp add: replicateHider_def) 454 done 455 456lemma coerce_memset_to_heap_update_pml4e: 457 "heap_update_list x (replicateHider 8 0) 458 = heap_update (Ptr x :: pml4e_C ptr) 459 (pml4e_C.pml4e_C (FCP (\<lambda>x. 0)))" 460 apply (intro ext, simp add: heap_update_def) 461 apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) 462 apply (simp add: to_bytes_def size_of_def typ_info_simps pml4e_C_tag_def) 463 apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def 464 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) 465 apply (simp add: typ_info_simps align_td_array' size_td_array) 466 apply (simp add: typ_info_array' typ_info_word word_rsplit_0) 467 apply (simp add: numeral_nat word_rsplit_0) 468 apply (simp add: replicateHider_def) 469 done 470 471lemma objBits_eq_by_type: 472 fixes x :: "'a :: pspace_storable" and y :: 'a 473 shows "objBits x = objBits y" 474 apply (simp add: objBits_def) 475 apply (rule objBits_type) 476 apply (simp add: koTypeOf_injectKO) 477 done 478 479lemma mapM_x_store_memset_ccorres_assist: 480 fixes val :: "'a :: pspace_storable" 481 assumes nofail: "\<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>)" 482 assumes slots1: "\<forall>n < length slots. slots ! n = hd slots + (of_nat n << objBits val)" 483 assumes slots2: "n = length slots * (2 ^ objBits val)" 484 assumes ptr: "ptr = hd slots" 485 assumes ko: "\<And>ko :: 'a. updateObject ko = updateObject_default ko" 486 "\<And>ko :: 'a. (1 :: machine_word) < 2 ^ objBits ko" 487 assumes restr: "set slots \<subseteq> S" 488 assumes worker: "\<And>ptr s s' (ko :: 'a). \<lbrakk> (s, s') \<in> rf_sr; ko_at' ko ptr s; ptr \<in> S \<rbrakk> 489 \<Longrightarrow> (s \<lparr> ksPSpace := ksPSpace s (ptr \<mapsto> injectKO val)\<rparr>, 490 globals_update (t_hrs_'_update (hrs_mem_update 491 (heap_update_list ptr 492 (replicateHider (2 ^ objBits val) (ucast c))))) s') \<in> rf_sr" 493 assumes rf_sr: "(\<sigma>, s) \<in> rf_sr" 494 shows 495 "\<exists>(rv, \<sigma>') \<in> fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). 496 (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update 497 (heap_update_list ptr (replicateHider n c)))) s) \<in> rf_sr" 498 unfolding slots2 ptr using rf_sr slots1 nofail restr 499proof (induct slots arbitrary: s \<sigma>) 500 case Nil 501 show ?case 502 using Nil.prems 503 apply (simp add: mapM_x_def sequence_x_def return_def replicateHider_def) 504 apply (simp add: rf_sr_def hrs_mem_update_def cstate_relation_def Let_def 505 carch_state_relation_def cmachine_state_relation_def 506 h_t_valid_clift_Some_iff) 507 done 508next 509 case (Cons x xs tPre sPre) 510 511 note nofail_bind = Cons.prems(3)[unfolded mapM_x_Cons K_bind_def] 512 513 have obj_at: "obj_at' (\<lambda>x :: 'a. True) x sPre" 514 using not_snd_bindI1[OF nofail_bind] 515 apply (subst(asm) setObject_obj_at_pre, simp_all add: ko snd_bind) 516 apply (clarsimp simp: stateAssert_def exec_get return_def) 517 apply (simp add: koTypeOf_injectKO typ_at_to_obj_at') 518 done 519 520 note in_setObject = setObject_eq[OF _ _ objBits_eq_by_type obj_at, 521 where ko=val, simplified ko, simplified] 522 523 note nofail_mapM = not_snd_bindI2[OF nofail_bind, OF in_setObject] 524 525 have hd_xs: "xs \<noteq> [] \<Longrightarrow> hd xs = x + (2 ^ objBits val)" 526 using Cons.prems(2)[rule_format, where n=1] 527 by (simp add: hd_conv_nth) 528 529 show ?case 530 using obj_at_ko_at'[OF obj_at] Cons.prems(4) 531 apply (clarsimp simp add: mapM_x_Cons bind_def split_def) 532 apply (rule rev_bexI, rule in_setObject) 533 apply (cut_tac Cons.hyps[OF _ _ nofail_mapM]) 534 defer 535 apply (rule worker, rule Cons.prems, assumption+) 536 apply clarsimp 537 apply (case_tac "xs = []", simp_all)[1] 538 apply (insert Cons.prems, simp)[1] 539 apply (frule_tac x="Suc n" in spec) 540 apply (simp add: hd_xs shiftl_t2n field_simps) 541 apply assumption 542 apply clarsimp 543 apply (rule rev_bexI, assumption) 544 apply (simp add: o_def) 545 apply (case_tac "xs = []") 546 apply (simp add: hrs_mem_update_def split_def replicateHider_def) 547 apply (subst(asm) heap_update_list_concat_fold_hrs_mem) 548 apply (simp add: hd_xs replicateHider_def) 549 apply (simp add: replicateHider_def replicate_add) 550 done 551qed 552 553(* FIXME: also in VSpace_C *) 554lemma ignoreFailure_liftM: 555 "ignoreFailure = liftM (\<lambda>v. ())" 556 apply (rule ext)+ 557 apply (simp add: ignoreFailure_def liftM_def 558 catch_def) 559 apply (rule bind_apply_cong[OF refl]) 560 apply (simp split: sum.split) 561 done 562 563end 564 565lemma option_to_0_user_mem': 566 "option_to_0 \<circ> user_mem' as =(\<lambda>x. if x \<in> {y. \<not> pointerInUserData y as} then 0 567 else underlying_memory (ksMachineState as) x) " 568 apply (rule ext) 569 apply (simp add:user_mem'_def option_to_0_def split:if_splits) 570 done 571 572lemma heap_to_user_data_in_user_mem'[simp]: 573 "\<lbrakk>pspace_aligned' as;pspace_distinct' as\<rbrakk> \<Longrightarrow> heap_to_user_data (ksPSpace as) (option_to_0 \<circ> user_mem' as) = 574 heap_to_user_data (ksPSpace as)(underlying_memory (ksMachineState as))" 575 apply (rule ext)+ 576 apply (clarsimp simp: heap_to_user_data_def option_map_def 577 split: option.splits) 578 apply (subst option_to_0_user_mem') 579 apply (subst map_option_byte_to_word_heap) 580 apply (clarsimp simp: projectKO_opt_user_data map_comp_def 581 split: option.split_asm kernel_object.split_asm) 582 apply (frule(1) pspace_alignedD') 583 apply (frule(1) pspace_distinctD') 584 apply (subgoal_tac "x + ucast off * 8 + xa && ~~ mask pageBits = x" ) 585 apply (clarsimp simp: pointerInUserData_def typ_at'_def ko_wp_at'_def) 586 apply (simp add: X64.pageBits_def) 587 apply (subst mask_lower_twice2[where n = 3 and m = 12,simplified,symmetric]) 588 apply (subst is_aligned_add_helper[THEN conjunct2,where n1 = 3]) 589 apply (erule aligned_add_aligned) 590 apply (simp add: is_aligned_mult_triv2[where n = 3,simplified]) 591 apply (clarsimp simp: objBits_simps X64.pageBits_def) 592 apply simp 593 apply (rule is_aligned_add_helper[THEN conjunct2]) 594 apply (simp add: X64.pageBits_def objBits_simps) 595 apply (rule word_less_power_trans2[where k = 3,simplified]) 596 apply (rule less_le_trans[OF ucast_less]) 597 apply simp+ 598 done 599 600context begin interpretation Arch . (*FIXME: arch_split*) 601crunch gsMaxObjectSize[wp]: deleteASIDPool "\<lambda>s. P (gsMaxObjectSize s)" 602 (ignore: setObject getObject wp: crunch_wps getObject_inv loadObject_default_inv 603 simp: crunch_simps) 604end 605 606context kernel_m begin 607 608lemma page_table_at_rf_sr_dom_s: 609 "\<lbrakk> page_table_at' x s; (s, s') \<in> rf_sr \<rbrakk> 610 \<Longrightarrow> {x ..+ 2 ^ ptBits} \<times> {SIndexVal, SIndexTyp 0} 611 \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" 612 apply (rule_tac m=3 in intvl_2_power_times_decomp, 613 simp_all add: shiftl_t2n field_simps bit_simps 614 word_bits_def) 615 apply (clarsimp simp: page_table_at'_def intvl_def bit_simps) 616 apply (drule spec, drule(1) mp) 617 apply (simp add: typ_at_to_obj_at_arches) 618 apply (drule obj_at_ko_at', clarsimp) 619 apply (erule cmap_relationE1[OF rf_sr_cpte_relation]) 620 apply (erule ko_at_projectKO_opt) 621 apply (drule h_t_valid_clift) 622 apply (drule h_t_valid_dom_s[OF _ refl refl]) 623 apply (erule subsetD) 624 apply (auto simp add: intvl_def shiftl_t2n)[1] 625 done 626 627lemma page_directory_at_rf_sr_dom_s: 628 "\<lbrakk> page_directory_at' x s; (s, s') \<in> rf_sr \<rbrakk> 629 \<Longrightarrow> {x ..+ 2 ^ pdBits} \<times> {SIndexVal, SIndexTyp 0} 630 \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" 631 apply (rule_tac m=3 in intvl_2_power_times_decomp, 632 simp_all add: shiftl_t2n field_simps bit_simps 633 word_bits_def) 634 apply (clarsimp simp: page_directory_at'_def intvl_def bit_simps) 635 apply (drule spec, drule(1) mp) 636 apply (simp add: typ_at_to_obj_at_arches) 637 apply (drule obj_at_ko_at', clarsimp) 638 apply (erule cmap_relationE1[OF rf_sr_cpde_relation]) 639 apply (erule ko_at_projectKO_opt) 640 apply (drule h_t_valid_clift) 641 apply (drule h_t_valid_dom_s[OF _ refl refl]) 642 apply (erule subsetD) 643 apply (auto simp add: intvl_def shiftl_t2n)[1] 644 done 645 646lemma pd_pointer_table_at_rf_sr_dom_s: 647 "\<lbrakk> pd_pointer_table_at' x s; (s, s') \<in> rf_sr \<rbrakk> 648 \<Longrightarrow> {x ..+ 2 ^ pdptBits} \<times> {SIndexVal, SIndexTyp 0} 649 \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" 650 apply (rule_tac m=3 in intvl_2_power_times_decomp, 651 simp_all add: shiftl_t2n field_simps bit_simps 652 word_bits_def) 653 apply (clarsimp simp: pd_pointer_table_at'_def intvl_def bit_simps) 654 apply (drule spec, drule(1) mp) 655 apply (simp add: typ_at_to_obj_at_arches) 656 apply (drule obj_at_ko_at', clarsimp) 657 apply (erule cmap_relationE1[OF rf_sr_cpdpte_relation]) 658 apply (erule ko_at_projectKO_opt) 659 apply (drule h_t_valid_clift) 660 apply (drule h_t_valid_dom_s[OF _ refl refl]) 661 apply (erule subsetD) 662 apply (auto simp add: intvl_def shiftl_t2n)[1] 663 done 664 665lemma page_map_l4_at_rf_sr_dom_s: 666 "\<lbrakk> page_map_l4_at' x s; (s, s') \<in> rf_sr \<rbrakk> 667 \<Longrightarrow> {x ..+ 2 ^ pml4Bits} \<times> {SIndexVal, SIndexTyp 0} 668 \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" 669 apply (rule_tac m=3 in intvl_2_power_times_decomp, 670 simp_all add: shiftl_t2n field_simps bit_simps 671 word_bits_def) 672 apply (clarsimp simp: page_map_l4_at'_def intvl_def bit_simps) 673 apply (drule spec, drule(1) mp) 674 apply (simp add: typ_at_to_obj_at_arches) 675 apply (drule obj_at_ko_at', clarsimp) 676 apply (erule cmap_relationE1[OF rf_sr_cpml4e_relation]) 677 apply (erule ko_at_projectKO_opt) 678 apply (drule h_t_valid_clift) 679 apply (drule h_t_valid_dom_s[OF _ refl refl]) 680 apply (erule subsetD) 681 apply (auto simp add: intvl_def shiftl_t2n)[1] 682 done 683 684(* FIXME x64: copies needed for PDE, PDPTE etc *) 685lemma clearMemory_setObject_PTE_ccorres: 686 "ccorres dc xfdc (page_table_at' ptr 687 and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) 688 and (\<lambda>_. is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr)) 689 (UNIV \<inter> {s. ptr___ptr_to_void_' s = Ptr ptr} \<inter> {s. bits_' s = of_nat ptBits}) [] 690 (mapM_x (\<lambda>a. setObject a X64_H.InvalidPTE) 691 [ptr , ptr + 2 ^ objBits X64_H.InvalidPTE .e. ptr + 2 ^ ptBits - 1]) 692 (Call clearMemory_'proc)" 693 apply (rule ccorres_gen_asm)+ 694 apply (cinit' lift: ptr___ptr_to_void_' bits_') 695 apply (rule_tac P="page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)" 696 in ccorres_from_vcg_nofail[where P'=UNIV]) 697 apply (rule allI, rule conseqPre, vcg) 698 apply clarsimp 699 apply (subst ghost_assertion_size_logic[unfolded o_def]) 700 apply (simp add: bit_simps) 701 apply simp 702 apply (clarsimp simp: replicateHider_def[symmetric] bit_simps) 703 apply (frule is_aligned_no_overflow', simp) 704 apply (intro conjI) 705 apply (erule is_aligned_weaken, simp) 706 apply (clarsimp simp: is_aligned_def) 707 apply (erule (1) page_table_at_rf_sr_dom_s[unfolded ptBits_def bit_simps, simplified]) 708 apply (clarsimp simp add: bit_simps 709 cong: StateSpace.state.fold_congs globals.fold_congs) 710 apply (simp add: upto_enum_step_def objBits_simps bit_simps 711 field_simps linorder_not_less[symmetric] archObjSize_def 712 upto_enum_word split_def) 713 apply (erule mapM_x_store_memset_ccorres_assist 714 [unfolded split_def, OF _ _ _ _ _ _ subset_refl], 715 simp_all add: shiftl_t2n hd_map objBits_simps archObjSize_def bit_simps)[1] 716 apply (rule cmap_relationE1, erule rf_sr_cpte_relation, erule ko_at_projectKO_opt) 717 apply (subst coerce_memset_to_heap_update_pte) 718 apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps) 719 apply (rule conjI) 720 apply (simp add: cpspace_relation_def typ_heap_simps update_pte_map_tos 721 update_pte_map_to_ptes carray_map_relation_upd_triv) 722 apply (rule cmap_relation_updI, simp_all)[1] 723 apply (simp add: cpte_relation_def Let_def pte_lift_def) 724 apply (simp add: carch_state_relation_def cmachine_state_relation_def 725 fpu_null_state_heap_update_tag_disj_simps 726 global_ioport_bitmap_heap_update_tag_disj_simps 727 update_pte_map_tos) 728 apply simp 729 done 730 731lemma ccorres_make_xfdc: 732 "ccorresG rf_sr \<Gamma> r xf P P' h a c \<Longrightarrow> ccorresG rf_sr \<Gamma> dc xfdc P P' h a c" 733 apply (erule ccorres_rel_imp) 734 apply simp 735 done 736 737lemma ccorres_if_True_False_simps: 738 "ccorres r xf P P' hs a (IF True THEN c ELSE c' FI) = ccorres r xf P P' hs a c" 739 "ccorres r xf P P' hs a (IF False THEN c ELSE c' FI) = ccorres r xf P P' hs a c'" 740 "ccorres r xf P P' hs a (IF True THEN c ELSE c' FI ;; d) = ccorres r xf P P' hs a (c ;; d)" 741 "ccorres r xf P P' hs a (IF False THEN c ELSE c' FI ;; d) = ccorres r xf P P' hs a (c' ;; d)" 742 by (simp_all add: ccorres_cond_iffs ccorres_seq_simps) 743 744lemmas cap_tag_values = 745 cap_untyped_cap_def 746 cap_endpoint_cap_def 747 cap_notification_cap_def 748 cap_reply_cap_def 749 cap_cnode_cap_def 750 cap_thread_cap_def 751 cap_irq_handler_cap_def 752 cap_null_cap_def 753 cap_irq_control_cap_def 754 cap_zombie_cap_def 755 cap_frame_cap_def 756 cap_page_table_cap_def 757 cap_page_directory_cap_def 758 cap_pml4_cap_def 759 cap_pdpt_cap_def 760 cap_asid_pool_cap_def 761 762lemma ccorres_return_C_seq: 763 "\<lbrakk>\<And>s f. xf (global_exn_var_'_update f (xfu (\<lambda>_. v s) s)) = v s; \<And>s f. globals (xfu f s) = globals s; wfhandlers hs\<rbrakk> 764 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r rvxf arrel xf (\<lambda>_. True) {s. arrel rv (v s)} hs (return rv) (return_C xfu v ;; d)" 765 apply (rule ccorres_guard_imp) 766 apply (rule ccorres_split_throws, rule ccorres_return_C, simp+) 767 apply vcg 768 apply simp_all 769 done 770 771 772lemma ccap_relation_get_capZombiePtr_CL: 773 "\<lbrakk> ccap_relation cap cap'; isZombie cap; capAligned cap \<rbrakk> 774 \<Longrightarrow> get_capZombiePtr_CL (cap_zombie_cap_lift cap') = capZombiePtr cap" 775 apply (simp only: cap_get_tag_isCap[symmetric]) 776 apply (drule(1) cap_get_tag_to_H) 777 apply (clarsimp simp: get_capZombiePtr_CL_def get_capZombieBits_CL_def Let_def split: if_split) 778 apply (subst less_mask_eq) 779 apply (clarsimp simp add: capAligned_def objBits_simps word_bits_conv) 780 apply unat_arith 781 apply simp 782 done 783 784lemma modify_gets_helper: 785 "do y \<leftarrow> modify (ksPSpace_update (\<lambda>_. ps)); ps' \<leftarrow> gets ksPSpace; f ps' od 786 = do y \<leftarrow> modify (ksPSpace_update (\<lambda>_. ps)); f ps od" 787 by (simp add: bind_def simpler_modify_def simpler_gets_def) 788 789lemma snd_lookupAround2_update: 790 "ps y \<noteq> None \<Longrightarrow> 791 snd (lookupAround2 x (ps (y \<mapsto> v'))) = snd (lookupAround2 x ps)" 792 apply (clarsimp simp: lookupAround2_def lookupAround_def Let_def 793 dom_fun_upd2 794 simp del: dom_fun_upd cong: if_cong option.case_cong) 795 apply (clarsimp split: option.split if_split cong: if_cong) 796 apply auto 797 done 798 799lemma double_setEndpoint: 800 "do y \<leftarrow> setEndpoint epptr v1; setEndpoint epptr v2 od 801 = setEndpoint epptr v2" 802 apply (simp add: setEndpoint_def setObject_def bind_assoc split_def 803 modify_gets_helper) 804 apply (simp add: updateObject_default_def bind_assoc objBits_simps) 805 apply (rule ext) 806 apply (rule bind_apply_cong, rule refl)+ 807 apply (clarsimp simp add: in_monad projectKOs magnitudeCheck_assert 808 snd_lookupAround2_update) 809 apply (simp add: lookupAround2_known1 assert_opt_def projectKO_def projectKO_opt_ep 810 alignCheck_assert) 811 apply (simp add: bind_def simpler_modify_def) 812 done 813 814lemma filterM_setEndpoint_adjustment: 815 "\<lbrakk> \<And>v. do setEndpoint epptr IdleEP; body v od 816 = do v' \<leftarrow> body v; setEndpoint epptr IdleEP; return v' od \<rbrakk> 817 \<Longrightarrow> 818 (do q' \<leftarrow> filterM body q; setEndpoint epptr (f q') od) 819 = (do setEndpoint epptr IdleEP; q' \<leftarrow> filterM body q; setEndpoint epptr (f q') od)" 820 apply (rule sym) 821 apply (induct q arbitrary: f) 822 apply (simp add: double_setEndpoint) 823 apply (simp add: bind_assoc) 824 apply (subst bind_assoc[symmetric], simp, simp add: bind_assoc) 825 done 826 827lemma ccorres_inst_voodoo: 828 "\<forall>x. ccorres r xf (P x) (P' x) hs (h x) (c x) 829 \<Longrightarrow> \<forall>x. ccorres r xf (P x) (P' x) hs (h x) (c x)" 830 by simp 831 832lemma cpspace_relation_ep_update_ep2: 833 "\<lbrakk> ko_at' (ep :: endpoint) epptr s; 834 cmap_relation (map_to_eps (ksPSpace s)) 835 (cslift t) ep_Ptr (cendpoint_relation (cslift t)); 836 cendpoint_relation (cslift t') ep' endpoint; 837 (cslift t' :: tcb_C ptr \<rightharpoonup> tcb_C) = cslift t \<rbrakk> 838 \<Longrightarrow> cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep'))) 839 (cslift t(ep_Ptr epptr \<mapsto> endpoint)) 840 ep_Ptr (cendpoint_relation (cslift t'))" 841 apply (rule cmap_relationE1, assumption, erule ko_at_projectKO_opt) 842 apply (rule_tac P="\<lambda>a. cmap_relation a b c d" for b c d in rsubst, 843 erule cmap_relation_upd_relI, assumption+) 844 apply simp+ 845 apply (rule ext, simp add: map_comp_def projectKO_opt_ep split: if_split) 846 done 847 848end 849 850context begin interpretation Arch . (*FIXME: arch_split*) 851lemma setObject_tcb_ep_obj_at'[wp]: 852 "\<lbrace>obj_at' (P :: endpoint \<Rightarrow> bool) ptr\<rbrace> setObject ptr' (tcb :: tcb) \<lbrace>\<lambda>rv. obj_at' P ptr\<rbrace>" 853 apply (rule obj_at_setObject2, simp_all) 854 apply (clarsimp simp: updateObject_default_def in_monad) 855 done 856end 857 858crunch ep_obj_at'[wp]: setThreadState "obj_at' (P :: endpoint \<Rightarrow> bool) ptr" 859 (ignore: getObject setObject simp: unless_def) 860 861crunch pspace_canonical'[wp]: setThreadState pspace_canonical' 862 863context kernel_m begin 864 865lemma ccorres_abstract_h_val: 866 "(\<And>rv. P rv \<Longrightarrow> ccorres r xf G (G' rv) hs a c) \<Longrightarrow> 867 ccorres r xf G ({s. P (h_val (hrs_mem (t_hrs_' (globals s))) p) 868 \<longrightarrow> s \<in> G' (h_val (hrs_mem (t_hrs_' (globals s))) 869 p)} 870 \<inter> {s. P (h_val (hrs_mem (t_hrs_' (globals s))) p)}) hs a c" 871 apply (rule ccorres_tmp_lift1 [where P = P]) 872 apply (clarsimp simp: Collect_conj_eq [symmetric]) 873 apply (fastforce intro: ccorres_guard_imp) 874 done 875 876lemma ccorres_subst_basic_helper: 877 "\<lbrakk> \<And>s s'. \<lbrakk> P s; s' \<in> P'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> f s' = f' s'; 878 \<And>s s'. \<lbrakk> P s; s' \<in> P'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; 879 \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); 880 ccorres rrel xf Q Q' hs a (c' v) \<rbrakk> 881 \<Longrightarrow> ccorres rrel xf (P and Q) {s. s \<in> P' \<and> f' s \<in> Q'} hs a (Basic f ;; c)" 882 apply (rule ccorres_guard_imp2) 883 apply (rule ccorres_add_return) 884 apply (rule ccorres_split_nothrow[where xf'=xf' and r'="\<lambda>rv rv'. rv' = v"]) 885 apply (rule ccorres_from_vcg[where P=P and P'=P']) 886 apply (rule allI, rule conseqPre, vcg) 887 apply (clarsimp simp: return_def) 888 apply assumption 889 apply simp 890 apply wp 891 apply vcg 892 apply clarsimp 893 done 894 895lemma ctcb_relation_blocking_ipc_badge: 896 "\<lbrakk> ctcb_relation tcb ctcb; isBlockedOnSend (tcbState tcb) \<rbrakk> \<Longrightarrow> 897 tsType_CL (thread_state_lift (tcbState_C ctcb)) = scast ThreadState_BlockedOnSend" 898 "\<lbrakk> ctcb_relation tcb ctcb; 899 tsType_CL (thread_state_lift (tcbState_C ctcb)) = scast ThreadState_BlockedOnSend \<rbrakk> 900 \<Longrightarrow> blockingIPCBadge (tcbState tcb) 901 = blockingIPCBadge_CL (thread_state_lift (tcbState_C ctcb))" 902 apply (clarsimp simp add: ctcb_relation_def) 903 apply (simp add: isBlockedOnSend_def split: Structures_H.thread_state.split_asm) 904 apply (clarsimp simp: cthread_state_relation_def) 905 apply (clarsimp simp add: ctcb_relation_def cthread_state_relation_def) 906 apply (cases "tcbState tcb", simp_all add: "StrictC'_thread_state_defs") 907 done 908 909lemma cendpoint_relation_q_cong: 910 "\<lbrakk> \<And>t rf. (t, rf) \<in> ep_q_refs_of' ep \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t) \<rbrakk> 911 \<Longrightarrow> cendpoint_relation hp ep ep' = cendpoint_relation hp' ep ep'" 912 apply (cases ep, simp_all add: cendpoint_relation_def Let_def) 913 apply (rule conj_cong [OF refl]) 914 apply (rule tcb_queue_relation'_cong[OF refl refl refl]) 915 apply clarsimp 916 apply (rule conj_cong [OF refl]) 917 apply (rule tcb_queue_relation'_cong[OF refl refl refl]) 918 apply clarsimp 919 done 920 921lemma cnotification_relation_q_cong: 922 "\<lbrakk>\<And>t rf. (t, rf) \<in> ntfn_q_refs_of' (ntfnObj ntfn) \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t)\<rbrakk> 923 \<Longrightarrow> cnotification_relation hp ntfn ntfn' = cnotification_relation hp' ntfn ntfn'" 924 apply (cases "ntfnObj ntfn", simp_all add: cnotification_relation_def Let_def) 925 apply (auto intro: iffD1[OF tcb_queue_relation'_cong[OF refl refl refl]]) 926 done 927 928lemma tcbSchedEnqueue_ep_at: 929 "\<lbrace>obj_at' (P :: endpoint \<Rightarrow> bool) ep\<rbrace> 930 tcbSchedEnqueue t 931 \<lbrace>\<lambda>rv. obj_at' P ep\<rbrace>" 932 including no_pre 933 apply (simp add: tcbSchedEnqueue_def unless_def null_def) 934 apply (wp threadGet_wp, clarsimp, wp+) 935 apply (clarsimp split: if_split, wp) 936 done 937 938lemma ccorres_duplicate_guard: 939 "ccorres r xf (P and P) Q hs f f' \<Longrightarrow> ccorres r xf P Q hs f f'" 940 by (erule ccorres_guard_imp, auto) 941 942 943lemma ep_q_refs'_no_NTFNBound[simp]: 944 "(x, NTFNBound) \<notin> ep_q_refs_of' ep" 945 by (auto simp: ep_q_refs_of'_def split: endpoint.splits) 946 947 948lemma ntfn_q_refs'_no_NTFNBound[simp]: 949 "(x, NTFNBound) \<notin> ntfn_q_refs_of' ntfn" 950 by (auto simp: ntfn_q_refs_of'_def split: ntfn.splits) 951 952lemma cancelBadgedSends_ccorres: 953 "ccorres dc xfdc (invs' and ep_at' ptr) 954 (UNIV \<inter> {s. epptr_' s = Ptr ptr} \<inter> {s. badge_' s = bdg}) [] 955 (cancelBadgedSends ptr bdg) (Call cancelBadgedSends_'proc)" 956 apply (cinit lift: epptr_' badge_' simp: whileAnno_def) 957 apply (simp add: list_case_return2 958 cong: list.case_cong Structures_H.endpoint.case_cong call_ignore_cong 959 del: Collect_const) 960 apply (rule ccorres_pre_getEndpoint) 961 apply (rule_tac R="ko_at' rv ptr" and xf'="ret__unsigned_longlong_'" 962 and val="case rv of RecvEP q \<Rightarrow> scast EPState_Recv | IdleEP \<Rightarrow> scast EPState_Idle 963 | SendEP q \<Rightarrow> scast EPState_Send" 964 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 965 apply vcg 966 apply clarsimp 967 apply (erule cmap_relationE1 [OF cmap_relation_ep], erule ko_at_projectKO_opt) 968 apply (clarsimp simp: typ_heap_simps cendpoint_relation_def Let_def 969 split: Structures_H.endpoint.split_asm) 970 apply ceqv 971 apply wpc 972 apply (simp add: dc_def[symmetric] ccorres_cond_iffs) 973 apply (rule ccorres_return_Skip) 974 apply (simp add: dc_def[symmetric] ccorres_cond_iffs) 975 apply (rule ccorres_return_Skip) 976 apply (rename_tac list) 977 apply (simp add: Collect_True Collect_False endpoint_state_defs 978 ccorres_cond_iffs dc_def[symmetric] 979 del: Collect_const cong: call_ignore_cong) 980 apply (rule ccorres_rhs_assoc)+ 981 apply (csymbr, csymbr) 982 apply (drule_tac s = rv in sym, simp only:) 983 apply (rule_tac P="ko_at' rv ptr and invs'" in ccorres_cross_over_guard) 984 apply (rule ccorres_symb_exec_r) 985 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 986 apply (rule ccorres_split_nothrow[where r'=dc and xf'=xfdc, OF _ ceqv_refl]) 987 apply (rule_tac P="ko_at' rv ptr" 988 in ccorres_from_vcg[where P'=UNIV]) 989 apply (rule allI, rule conseqPre, vcg) 990 apply clarsimp 991 apply (rule cmap_relationE1[OF cmap_relation_ep], assumption) 992 apply (erule ko_at_projectKO_opt) 993 apply (clarsimp simp: typ_heap_simps setEndpoint_def) 994 apply (rule rev_bexI) 995 apply (rule setObject_eq; simp add: objBits_simps')[1] 996 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 997 carch_state_relation_def cmachine_state_relation_def 998 packed_heap_update_collapse_hrs 999 fpu_null_state_heap_update_tag_disj_simps) 1000 apply (clarsimp simp: cpspace_relation_def update_ep_map_tos typ_heap_simps') 1001 apply (erule(1) cpspace_relation_ep_update_ep2) 1002 apply (simp add: cendpoint_relation_def endpoint_state_defs) 1003 subgoal by simp 1004 apply (rule ccorres_symb_exec_r) 1005 apply (rule_tac xs=list in filterM_voodoo) 1006 apply (rule_tac P="\<lambda>xs s. (\<forall>x \<in> set xs \<union> set list. 1007 st_tcb_at' (\<lambda>st. isBlockedOnSend st \<and> blockingObject st = ptr) x s) 1008 \<and> distinct (xs @ list) \<and> ko_at' IdleEP ptr s 1009 \<and> (\<forall>p. \<forall>x \<in> set (xs @ list). \<forall>rf. (x, rf) \<notin> {r \<in> state_refs_of' s p. snd r \<noteq> NTFNBound}) 1010 \<and> valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_canonical' s 1011 \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s" 1012 and P'="\<lambda>xs. {s. ep_queue_relation' (cslift s) (xs @ list) 1013 (head_C (queue_' s)) (end_C (queue_' s))} 1014 \<inter> {s. thread_' s = (case list of [] \<Rightarrow> tcb_Ptr 0 1015 | x # xs \<Rightarrow> tcb_ptr_to_ctcb_ptr x)}" 1016 in ccorres_inst_voodoo) 1017 apply (induct_tac list) 1018 apply (rule allI) 1019 apply (rule iffD1 [OF ccorres_expand_while_iff_Seq]) 1020 apply (rule ccorres_tmp_lift2 [OF _ _ refl]) 1021 apply ceqv 1022 apply (simp add: ccorres_cond_iffs) 1023 apply (rule ccorres_rhs_assoc2) 1024 apply (rule ccorres_duplicate_guard, rule ccorres_split_nothrow_novcg_dc) 1025 apply (rule ccorres_from_vcg, rule allI, rule conseqPre, vcg) 1026 apply clarsimp 1027 apply (drule obj_at_ko_at', clarsimp) 1028 apply (rule cmap_relationE1[OF cmap_relation_ep], assumption) 1029 apply (erule ko_at_projectKO_opt) 1030 apply (clarsimp simp: typ_heap_simps tcb_queue_relation'_def) 1031 apply (case_tac x) 1032 apply (clarsimp simp: setEndpoint_def) 1033 apply (rule rev_bexI, rule setObject_eq, 1034 (simp add: objBits_simps')+) 1035 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 1036 packed_heap_update_collapse_hrs 1037 carch_state_relation_def 1038 fpu_null_state_heap_update_tag_disj_simps 1039 cmachine_state_relation_def) 1040 apply (clarsimp simp: cpspace_relation_def typ_heap_simps' 1041 update_ep_map_tos) 1042 apply (erule(1) cpspace_relation_ep_update_ep2) 1043 subgoal by (simp add: cendpoint_relation_def Let_def) 1044 subgoal by simp 1045 apply (clarsimp simp: tcb_at_not_NULL[OF pred_tcb_at'] 1046 setEndpoint_def) 1047 apply (rule rev_bexI, rule setObject_eq, 1048 (simp add: objBits_simps')+) 1049 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 1050 packed_heap_update_collapse_hrs 1051 carch_state_relation_def 1052 fpu_null_state_heap_update_tag_disj_simps 1053 cmachine_state_relation_def) 1054 apply (clarsimp simp: cpspace_relation_def typ_heap_simps' 1055 update_ep_map_tos) 1056 apply (erule(1) cpspace_relation_ep_update_ep2) 1057 apply (simp add: cendpoint_relation_def Let_def) 1058 apply (subgoal_tac "tcb_at' (last (a # list)) \<sigma> \<and> tcb_at' a \<sigma>") 1059 apply (clarsimp simp: is_aligned_neg_mask_eq[OF is_aligned_tcb_ptr_to_ctcb_ptr[where P=\<top>]]) 1060 apply (simp add: tcb_queue_relation'_def EPState_Send_def mask_def) 1061 apply (drule (1) tcb_and_not_mask_canonical[where n=2]) 1062 apply (simp (no_asm) add: tcbBlockSizeBits_def) 1063 subgoal by (simp add: mask_def) 1064 subgoal by (auto split: if_split) 1065 subgoal by simp 1066 apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def]) 1067 apply (rule hoare_pre, wp weak_sch_act_wf_lift_linear set_ep_valid_objs') 1068 apply (clarsimp simp: weak_sch_act_wf_def sch_act_wf_def) 1069 apply (fastforce simp: valid_ep'_def pred_tcb_at' split: list.splits) 1070 apply (simp add: guard_is_UNIV_def) 1071 apply (rule allI) 1072 apply (rename_tac a lista x) 1073 apply (rule iffD1 [OF ccorres_expand_while_iff_Seq]) 1074 apply (rule ccorres_init_tmp_lift2, ceqv) 1075 apply (rule ccorres_guard_imp2) 1076 apply (simp add: bind_assoc dc_def[symmetric] 1077 del: Collect_const) 1078 apply (rule ccorres_cond_true) 1079 apply (rule ccorres_rhs_assoc)+ 1080 apply (rule ccorres_pre_threadGet[where f=tcbState, folded getThreadState_def]) 1081 apply (rule ccorres_move_c_guard_tcb) 1082 apply csymbr 1083 apply (rule ccorres_abstract_cleanup) 1084 apply csymbr 1085 apply (rule ccorres_move_c_guard_tcb) 1086 apply (rule_tac P=\<top> 1087 and P'="{s. ep_queue_relation' (cslift s) (x @ a # lista) 1088 (head_C (queue_' s)) (end_C (queue_' s))}" 1089 and f'="\<lambda>s. s \<lparr> next___ptr_to_struct_tcb_C_' := (case lista of [] \<Rightarrow> tcb_Ptr 0 1090 | v # vs \<Rightarrow> tcb_ptr_to_ctcb_ptr v) \<rparr>" 1091 and xf'="next___ptr_to_struct_tcb_C_'" 1092 in ccorres_subst_basic_helper) 1093 apply (thin_tac "\<forall>x. P x" for P) 1094 apply (rule myvars.fold_congs, (rule refl)+) 1095 apply (clarsimp simp: tcb_queue_relation'_def use_tcb_queue_relation2 1096 tcb_queue_relation2_concat) 1097 apply (clarsimp simp: typ_heap_simps split: list.split) 1098 subgoal by (simp add: rf_sr_def) 1099 apply simp 1100 apply ceqv 1101 apply (rule_tac P="ret__unsigned_longlong=blockingIPCBadge rva" in ccorres_gen_asm2) 1102 apply (rule ccorres_if_bind, rule ccorres_if_lhs) 1103 apply (simp add: bind_assoc dc_def[symmetric]) 1104 apply (rule ccorres_rhs_assoc)+ 1105 apply (ctac add: setThreadState_ccorres) 1106 apply (ctac add: tcbSchedEnqueue_ccorres) 1107 apply (rule_tac P="\<lambda>s. \<forall>t \<in> set (x @ a # lista). tcb_at' t s" 1108 in ccorres_cross_over_guard) 1109 apply (rule ccorres_add_return, rule ccorres_split_nothrow[OF _ ceqv_refl]) 1110 apply (rule_tac rrel=dc and xf=xfdc 1111 and P="\<lambda>s. (\<forall>t \<in> set (x @ a # lista). tcb_at' t s) 1112 \<and> (\<forall>p. \<forall>t \<in> set (x @ a # lista). \<forall>rf. (t, rf) \<notin> {r \<in> state_refs_of' s p. snd r \<noteq> NTFNBound}) 1113 \<and> valid_queues s \<and> distinct (x @ a # lista) 1114 \<and> pspace_aligned' s \<and> pspace_distinct' s" 1115 and P'="{s. ep_queue_relation' (cslift s) (x @ a # lista) 1116 (head_C (queue_' s)) (end_C (queue_' s))}" 1117 in ccorres_from_vcg) 1118 apply (thin_tac "\<forall>x. P x" for P) 1119 apply (rule allI, rule conseqPre, vcg) 1120 apply (clarsimp simp: ball_Un) 1121 apply (rule exI, rule conjI) 1122 apply (rule exI, erule conjI) 1123 apply (intro conjI[rotated]) 1124 apply (assumption) 1125 apply (fold_subgoals (prefix))[3] 1126 subgoal premises prems using prems by (fastforce intro: pred_tcb_at')+ 1127 apply (clarsimp simp: return_def rf_sr_def cstate_relation_def Let_def) 1128 apply (rule conjI) 1129 apply (clarsimp simp: cpspace_relation_def) 1130 apply (rule conjI, erule ctcb_relation_null_queue_ptrs) 1131 apply (rule null_ep_queue) 1132 subgoal by (simp add: o_def) 1133 apply (rule conjI) 1134 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1135 apply clarsimp 1136 apply (rule cendpoint_relation_q_cong) 1137 apply (rule sym, erule restrict_map_eqI) 1138 apply (clarsimp simp: image_iff) 1139 apply (drule(2) map_to_ko_atI2) 1140 apply (drule ko_at_state_refs_ofD') 1141 apply clarsimp 1142 apply (drule_tac x=p in spec) 1143 subgoal by fastforce 1144 1145 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1146 apply clarsimp 1147 apply (drule(2) map_to_ko_atI2, drule ko_at_state_refs_ofD') 1148 1149 apply (rule cnotification_relation_q_cong) 1150 apply (rule sym, erule restrict_map_eqI) 1151 apply (clarsimp simp: image_iff) 1152 apply (drule_tac x=p in spec) 1153 subgoal by fastforce 1154 apply (rule conjI) 1155 apply (erule cready_queues_relation_not_queue_ptrs, 1156 auto dest: null_ep_schedD[unfolded o_def] simp: o_def)[1] 1157 apply (clarsimp simp: carch_state_relation_def cmachine_state_relation_def 1158 elim!: fpu_null_state_typ_heap_preservation) 1159 apply (rule ccorres_symb_exec_r2) 1160 apply (erule spec) 1161 apply vcg 1162 apply (vcg spec=modifies) 1163 apply wp 1164 apply simp 1165 apply vcg 1166 apply (wp hoare_vcg_const_Ball_lift tcbSchedEnqueue_ep_at 1167 sch_act_wf_lift) 1168 apply simp 1169 apply (vcg exspec=tcbSchedEnqueue_cslift_spec) 1170 apply (wp hoare_vcg_const_Ball_lift sts_st_tcb_at'_cases 1171 sts_sch_act sts_valid_queues setThreadState_oa_queued) 1172 apply (vcg exspec=setThreadState_cslift_spec) 1173 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 1174 apply (rule ccorres_symb_exec_r2) 1175 apply (drule_tac x="x @ [a]" in spec, simp add: dc_def[symmetric]) 1176 apply vcg 1177 apply (vcg spec=modifies) 1178 apply (thin_tac "\<forall>x. P x" for P) 1179 apply (clarsimp simp: pred_tcb_at' ball_Un) 1180 apply (rule conjI) 1181 apply (clarsimp split: if_split) 1182 subgoal by (fastforce simp: valid_tcb_state'_def valid_objs'_maxDomain 1183 valid_objs'_maxPriority dest: pred_tcb_at') 1184 apply (clarsimp simp: tcb_at_not_NULL [OF pred_tcb_at']) 1185 apply (clarsimp simp: typ_heap_simps st_tcb_at'_def) 1186 apply (drule(1) obj_at_cslift_tcb) 1187 apply (clarsimp simp: ctcb_relation_blocking_ipc_badge) 1188 apply (rule conjI, simp add: "StrictC'_thread_state_defs" mask_def) 1189 apply (rule conjI) 1190 apply clarsimp 1191 apply (frule rf_sr_cscheduler_relation) 1192 apply (clarsimp simp: cscheduler_action_relation_def st_tcb_at'_def 1193 split: scheduler_action.split_asm) 1194 apply (rename_tac word) 1195 apply (frule_tac x=word in tcbSchedEnqueue_cslift_precond_discharge) 1196 apply simp 1197 subgoal by clarsimp 1198 subgoal by clarsimp 1199 subgoal by clarsimp 1200 apply clarsimp 1201 apply (rule conjI) 1202 apply (frule(3) tcbSchedEnqueue_cslift_precond_discharge) 1203 subgoal by clarsimp 1204 apply clarsimp 1205 apply (rule context_conjI) 1206 apply (clarsimp simp: tcb_queue_relation'_def) 1207 apply (erule iffD2[OF ep_queue_relation_shift[rule_format], rotated -1]) 1208 subgoal by simp 1209 apply (rule_tac x="x @ a # lista" in exI) 1210 apply (clarsimp simp: ball_Un) 1211 apply (rule conjI, fastforce) 1212 subgoal by (clarsimp simp: remove1_append) 1213 apply vcg 1214 apply (rule conseqPre, vcg) 1215 apply clarsimp 1216 apply (wp hoare_vcg_const_Ball_lift) 1217 apply (wp obj_at_setObject3[where 'a=endpoint, folded setEndpoint_def]) 1218 apply (simp add: objBits_simps')+ 1219 apply (wp set_ep_valid_objs') 1220 apply vcg 1221 apply vcg 1222 apply (rule conseqPre, vcg) 1223 apply clarsimp 1224 apply (clarsimp simp: guard_is_UNIV_def) 1225 apply (erule cmap_relationE1[OF cmap_relation_ep], erule ko_at_projectKO_opt) 1226 apply (clarsimp simp: typ_heap_simps) 1227 apply (clarsimp simp: cendpoint_relation_def Let_def) 1228 subgoal by (clarsimp simp: tcb_queue_relation'_def neq_Nil_conv 1229 split: if_split_asm) 1230 apply clarsimp 1231 apply (frule ko_at_valid_objs', clarsimp) 1232 apply (simp add: projectKOs) 1233 apply (clarsimp simp: valid_obj'_def valid_ep'_def) 1234 apply (frule sym_refs_ko_atD', clarsimp) 1235 apply (clarsimp simp: st_tcb_at_refs_of_rev') 1236 apply (rule conjI) 1237 subgoal by (auto simp: isBlockedOnSend_def elim!: pred_tcb'_weakenE) 1238 apply (rule conjI) 1239 apply (clarsimp split: if_split) 1240 apply (drule sym_refsD, clarsimp) 1241 apply (drule(1) bspec)+ 1242 by (auto simp: obj_at'_def projectKOs state_refs_of'_def pred_tcb_at'_def tcb_bound_refs'_def 1243 dest!: symreftype_inverse') 1244 1245 1246lemma tcb_ptr_to_ctcb_ptr_force_fold: 1247 "x + 2 ^ ctcb_size_bits = ptr_val (tcb_ptr_to_ctcb_ptr x)" 1248 by (simp add: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def) 1249 1250 1251lemma access_ti_list_word8_array: 1252 "N \<le> CARD('a::finite) \<Longrightarrow> 1253 access_ti_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(8 word)) (\<lambda>x. x.[n]) 1254 (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<N]) 1255 (ARRAY x. 0::8 word['a]) xs = 1256 replicateHider N 0" 1257 apply (induct N arbitrary: xs) 1258 apply (simp add: replicateHider_def) 1259 apply (simp add: access_ti_append') 1260 apply (simp add: typ_info_word word_rsplit_0 word_rsplit_same replicateHider_def replicate_append_same) 1261 done 1262 1263lemma coerce_memset_to_heap_update: 1264 "heap_update_list x (replicateHider (size_of (TYPE (tcb_C))) 0) 1265 = heap_update (tcb_Ptr x) 1266 (tcb_C (arch_tcb_C (user_context_C (user_fpu_state_C (FCP (\<lambda>x. 0))) (FCP (\<lambda>x. 0)))) 1267 (thread_state_C (FCP (\<lambda>x. 0))) 1268 (NULL) 1269 (seL4_Fault_C (FCP (\<lambda>x. 0))) 1270 (lookup_fault_C (FCP (\<lambda>x. 0))) 1271 0 0 0 0 0 0 NULL NULL NULL NULL)" 1272 apply (intro ext, simp add: heap_update_def) 1273 apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) 1274 apply (simp add: to_bytes_def size_of_def typ_info_simps tcb_C_tag_def) 1275 apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def 1276 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) 1277 apply (simp add: typ_info_simps 1278 user_context_C_tag_def thread_state_C_tag_def seL4_Fault_C_tag_def 1279 lookup_fault_C_tag_def update_ti_t_ptr_0s arch_tcb_C_tag_def 1280 ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td 1281 ti_typ_combine_empty_ti ti_typ_combine_td 1282 align_of_def padup_def user_fpu_state_C_tag_def 1283 final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def 1284 align_td_array' size_td_array) 1285 apply (simp add: typ_info_array' access_ti_list_word8_array) 1286 apply (simp add: typ_info_word word_rsplit_0 upt_conv_Cons) 1287 apply (simp add: typ_info_word typ_info_ptr word_rsplit_0 1288 replicateHider_def) 1289 done 1290 1291lemma isArchObjectCap_capBits: 1292 "isArchObjectCap cap \<Longrightarrow> capBits cap = acapBits (capCap cap)" 1293 by (clarsimp simp: isCap_simps) 1294 1295declare Kernel_C.tcb_C_size [simp del] 1296 1297lemma cte_lift_ccte_relation: 1298 "cte_lift cte' = Some ctel' 1299 \<Longrightarrow> c_valid_cte cte' 1300 \<Longrightarrow> ccte_relation (cte_to_H ctel') cte'" 1301 by (simp add: ccte_relation_def) 1302 1303lemma updateFreeIndex_ccorres: 1304 "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' 1305 \<and> cteCap cte = cap' \<and> ccte_relation cte cte'}) 1306 c 1307 {t. \<exists>cap. cap_untyped_cap_lift cap = (cap_untyped_cap_lift 1308 (cte_C.cap_C (the (cslift s (cte_Ptr srcSlot))))) 1309 \<lparr> cap_untyped_cap_CL.capFreeIndex_CL := ((of_nat idx') >> 4) \<rparr> 1310 \<and> cap_get_tag cap = scast cap_untyped_cap 1311 \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cte_Ptr srcSlot) 1312 (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cte_Ptr srcSlot))))) 1313 (t_hrs_' (globals s)) 1314 \<and> t may_only_modify_globals s in [t_hrs] 1315 } 1316 \<Longrightarrow> ccorres dc xfdc 1317 (valid_objs' and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) 1318 \<and> cap' = (cteCap cte)) srcSlot 1319 and untyped_ranges_zero' 1320 and (\<lambda>_. is_aligned (of_nat idx' :: machine_word) 4 \<and> idx' \<le> 2 ^ (capBlockSize cap'))) 1321 {s. \<not> capIsDevice cap' 1322 \<longrightarrow> region_actually_is_zero_bytes (capPtr cap' + of_nat idx') (capFreeIndex cap' - idx') s} hs 1323 (updateFreeIndex srcSlot idx') c" 1324 (is "_ \<Longrightarrow> ccorres dc xfdc (valid_objs' and ?cte_wp_at' and _ and _) ?P' hs ?a c") 1325 apply (rule ccorres_gen_asm) 1326 apply (simp add: updateFreeIndex_def getSlotCap_def updateCap_def) 1327 apply (rule ccorres_guard_imp2) 1328 apply (rule ccorres_split_noop_lhs, rule_tac cap'=cap' in updateTrackedFreeIndex_noop_ccorres) 1329 apply (rule ccorres_pre_getCTE)+ 1330 apply (rename_tac cte cte2) 1331 apply (rule_tac P = "\<lambda>s. ?cte_wp_at' s \<and> cte2 = cte \<and> cte_wp_at' ((=) cte) srcSlot s" 1332 and P'="{s. \<exists>cte cte'. cslift s (cte_Ptr srcSlot) = Some cte' 1333 \<and> cteCap cte = cap' \<and> ccte_relation cte cte'} \<inter> ?P'" in ccorres_from_vcg) 1334 apply (rule allI, rule HoarePartial.conseq_exploit_pre, clarify) 1335 apply (drule_tac x=s in spec, rule conseqPre, erule conseqPost) 1336 defer 1337 apply clarsimp 1338 apply clarsimp 1339 apply (simp add: cte_wp_at_ctes_of) 1340 apply wp 1341 apply (clarsimp simp: isCap_simps cte_wp_at_ctes_of) 1342 apply (frule(1) rf_sr_ctes_of_clift) 1343 apply clarsimp 1344 apply (frule(1) cte_lift_ccte_relation) 1345 apply (rule exI, intro conjI[rotated], assumption, simp_all)[1] 1346 apply (clarsimp simp: cte_wp_at_ctes_of) 1347 apply (erule(1) rf_sr_ctes_of_cliftE) 1348 apply (frule(1) rf_sr_ctes_of_clift) 1349 apply clarsimp 1350 apply (subgoal_tac "ccap_relation (capFreeIndex_update (\<lambda>_. idx') 1351 (cteCap (the (ctes_of \<sigma> srcSlot)))) cap") 1352 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) 1353 apply (erule bexI [rotated]) 1354 apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def 1355 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] 1356 isCap_simps) 1357 apply (simp add:cpspace_relation_def) 1358 apply (clarsimp simp:typ_heap_simps' modify_map_def mex_def meq_def) 1359 apply (rule conjI) 1360 apply (rule cpspace_cte_relation_upd_capI, assumption+) 1361 apply (rule conjI) 1362 apply (rule setCTE_tcb_case, assumption+) 1363 apply (case_tac s', clarsimp) 1364 subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def 1365 fpu_null_state_heap_update_tag_disj_simps 1366 global_ioport_bitmap_heap_update_tag_disj_simps) 1367 1368 apply (clarsimp simp: isCap_simps) 1369 apply (drule(1) cte_lift_ccte_relation, 1370 drule ccte_relation_ccap_relation) 1371 apply (simp add: cte_to_H_def) 1372 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1373 apply (clarsimp simp: ccap_relation_def cap_lift_untyped_cap 1374 cap_to_H_simps cap_untyped_cap_lift_def 1375 is_aligned_shiftr_shiftl 1376 dest!: ccte_relation_ccap_relation) 1377 apply (rule unat_of_nat_eq unat_of_nat_eq[symmetric], 1378 erule order_le_less_trans, 1379 rule power_strict_increasing, simp_all) 1380 apply (rule unat_less_helper, rule order_le_less_trans[OF word_and_le1], simp add: mask_def) 1381 done 1382 1383end 1384 1385(* FIXME: Move *) 1386lemma ccap_relation_isDeviceCap: 1387 "\<lbrakk>ccap_relation cp cap; isUntypedCap cp 1388 \<rbrakk> \<Longrightarrow> to_bool (capIsDevice_CL (cap_untyped_cap_lift cap)) = (capIsDevice cp)" 1389 apply (frule cap_get_tag_UntypedCap) 1390 apply (simp add:cap_get_tag_isCap ) 1391 done 1392 1393lemma ccap_relation_isDeviceCap2: 1394 "\<lbrakk>ccap_relation cp cap; isUntypedCap cp 1395 \<rbrakk> \<Longrightarrow> (capIsDevice_CL (cap_untyped_cap_lift cap) = 0) = (\<not> (capIsDevice cp))" 1396 apply (frule cap_get_tag_UntypedCap) 1397 apply (simp add:cap_get_tag_isCap to_bool_def) 1398 done 1399 1400end 1401