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 StoreWord_C 12imports VSpace_C 13begin 14 15context kernel_m 16begin 17 18lemma in_doMachineOp: 19 "(a, s) \<in> fst (doMachineOp f s') = (\<exists>b. (a, b) \<in> fst (f (ksMachineState s')) \<and> s = s'\<lparr>ksMachineState := b\<rparr>)" 20 unfolding doMachineOp_def 21 by (simp add: in_monad select_f_def) 22 23lemma dom_heap_to_user_data: 24 "dom (heap_to_user_data hp uhp) = dom (map_to_user_data hp)" 25 unfolding heap_to_user_data_def by (simp add: Let_def dom_def) 26 27lemma dom_heap_to_device_data: 28 "dom (heap_to_device_data hp uhp) = dom (map_to_user_data_device hp)" 29 unfolding heap_to_device_data_def by (simp add: Let_def dom_def) 30 31lemma projectKO_opt_retyp_same: 32 assumes pko: "projectKO_opt ko = Some v" 33 shows "projectKO_opt \<circ>\<^sub>m 34 (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some ko else ksPSpace \<sigma> x) 35 = 36 (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (projectKO_opt \<circ>\<^sub>m (ksPSpace \<sigma>)) x)" 37 (is "?LHS = ?RHS") 38proof (rule ext) 39 fix x 40 41 show "?LHS x = ?RHS x" 42 proof (cases "x \<in> set (new_cap_addrs sz ptr ko)") 43 case True 44 thus ?thesis using pko by simp 45 next 46 case False 47 thus ?thesis by (simp add: map_comp_def) 48 qed 49qed 50 51lemma mask_pageBits_inner_beauty: 52 "is_aligned p 2 \<Longrightarrow> 53 (p && ~~ mask pageBits) + (ucast ((ucast (p && mask pageBits >> 2)):: 10 word) * 4) = (p::word32)" 54 apply (simp add: is_aligned_nth word_shift_by_2) 55 apply (subst word_plus_and_or_coroll) 56 apply (rule word_eqI) 57 apply (clarsimp simp: word_size word_ops_nth_size nth_ucast nth_shiftr nth_shiftl) 58 apply (rule word_eqI) 59 apply (clarsimp simp: word_size word_ops_nth_size nth_ucast nth_shiftr nth_shiftl 60 pageBits_def) 61 apply (rule iffI) 62 apply (erule disjE) 63 apply clarsimp 64 apply clarsimp 65 apply (subgoal_tac "Suc (Suc (n - 2)) = n") 66 apply simp 67 apply arith 68 apply clarsimp 69 apply (rule context_conjI) 70 apply (rule leI) 71 apply clarsimp 72 apply (subgoal_tac "Suc (Suc (n - 2)) = n") 73 apply simp 74 apply arith 75 done 76 77lemma more_pageBits_inner_beauty: 78 fixes x :: "10 word" 79 fixes p :: word32 80 assumes x: "x \<noteq> ucast (p && mask pageBits >> 2)" 81 shows "(p && ~~ mask pageBits) + (ucast x * 4) \<noteq> p" 82 apply clarsimp 83 apply (simp add: word_shift_by_2) 84 apply (subst (asm) word_plus_and_or_coroll) 85 apply (clarsimp simp: word_size word_ops_nth_size nth_ucast 86 nth_shiftl bang_eq) 87 apply (drule test_bit_size) 88 apply (clarsimp simp: word_size pageBits_def) 89 apply arith 90 apply (insert x) 91 apply (erule notE) 92 apply (rule word_eqI) 93 apply (clarsimp simp: word_size nth_ucast nth_shiftl nth_shiftr bang_eq) 94 apply (erule_tac x="n+2" in allE) 95 apply (clarsimp simp: word_ops_nth_size word_size) 96 apply (clarsimp simp: pageBits_def) 97 done 98 99declare unat_ucast_10_32[simp] 100 101lemma byte_to_word_heap_upd_outside_range: 102 "p \<notin> {(base + ucast off * 4)..+4} \<Longrightarrow> 103 byte_to_word_heap (m (p := v')) base off = byte_to_word_heap m base off" 104 apply (simp add: byte_to_word_heap_def Let_def) 105 apply (erule contrapos_np) 106 apply (clarsimp intro!: intvl_inter_le [where k=0 and ka=3, simplified, OF refl] 107 intvl_inter_le [where k=0 and ka=2, simplified, OF refl] 108 intvl_inter_le [where k=0 and ka=1, simplified, OF refl] 109 intvl_inter_le [where k=0 and ka=0, simplified, OF refl] 110 split: if_split_asm) 111 done 112 113lemma intvl_range_conv: 114 "\<lbrakk> is_aligned (ptr :: 'a :: len word) bits; bits < len_of TYPE('a) \<rbrakk> \<Longrightarrow> 115 {ptr ..+ 2 ^ bits} = {ptr .. ptr + 2 ^ bits - 1}" 116 by (rule upto_intvl_eq) 117 118lemma byte_to_word_heap_upd_neq: 119 assumes alb: "is_aligned base 2" 120 and alp: "is_aligned p 2" 121 and neq: "base + ucast off * 4 \<noteq> p" 122 and word_byte: "n < 4" 123 shows "byte_to_word_heap (m (p + n := v')) base off = byte_to_word_heap m base off" 124proof - 125 from alb have alw: "is_aligned (base + ucast off * 4) 2" 126 by (fastforce elim: aligned_add_aligned 127 intro: is_aligned_mult_triv2 [where n=2, simplified] 128 simp: word_bits_def) 129 130 from alp have p_intvl: "p + n \<in> {p .. p + 3}" 131 apply (clarsimp simp: word_byte) 132 apply (rule conjI) 133 apply (fastforce elim: is_aligned_no_wrap' simp: word_byte) 134 apply (subst word_plus_mono_right) 135 apply (clarsimp simp: word_byte word_le_make_less) 136 apply (simp add: word_bits_def is_aligned_no_overflow'[OF alp, simplified]) 137 apply simp 138 done 139 140 hence not_in_range: "p + n \<notin> {(base + ucast off * 4)..+4}" 141 apply (subst intvl_range_conv [OF alw, simplified]) 142 apply (simp add: word_bits_def) 143 apply (cut_tac aligned_neq_into_no_overlap [OF neq alw alp]) 144 apply (auto simp: field_simps range_inter)[1] 145 done 146 147 thus ?thesis 148 by (rule byte_to_word_heap_upd_outside_range) 149qed 150 151lemma update_ti_t_acc_foo: 152 "\<And>acc f v. \<lbrakk> \<And>a ys v. \<lbrakk> a \<in> set adjs; length ys = size_td_pair a \<rbrakk> 153 \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v); 154 \<And>a. size_td_pair (f a) = size_td_pair a \<rbrakk> \<Longrightarrow> 155 \<forall>xs. acc (update_ti_list_t adjs xs v) = update_ti_list_t (map f adjs) xs (acc v)" 156 apply (simp add: update_ti_list_t_def size_td_list_map2 split: if_split) 157 apply (induct adjs) 158 apply simp 159 apply clarsimp 160 done 161 162lemma nat_less_4_cases: 163 "i < (4::nat) ==> i = 0 | i = 1 | i = 2 | i = 3" 164 by auto 165 166lemma user_data_relation_upd: 167 assumes al: "is_aligned ptr 2" 168 shows "cuser_user_data_relation 169 (byte_to_word_heap 170 (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits)) 171 (the (cslift s (Ptr (ptr && ~~ mask pageBits)))) \<Longrightarrow> 172 cuser_user_data_relation 173 (byte_to_word_heap 174 ((underlying_memory (ksMachineState \<sigma>)) 175 (ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, 176 ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) 177 (ptr && ~~ mask pageBits)) 178 (user_data_C.words_C_update 179 (\<lambda>ws. Arrays.update ws (unat (ucast ((ptr && mask pageBits) >> 2):: 10 word)) w) 180 (the (cslift s (Ptr (ptr && ~~ mask pageBits)))))" 181 unfolding cuser_user_data_relation_def 182 apply - 183 apply (erule allEI) 184 apply (case_tac "off = ucast ((ptr && mask pageBits) >> 2)") 185 apply (clarsimp simp: mask_pageBits_inner_beauty [OF al] byte_to_word_heap_def) 186 apply (subst index_update) 187 apply (simp, unat_arith, simp) 188 apply (subgoal_tac "map ((!) (word_rsplit w)) [0,1,2,3] 189 = (word_rsplit w :: word8 list)") 190 apply (clarsimp simp: word_rcat_rsplit) 191 apply (cut_tac w=w and m=4 and 'a=8 192 in length_word_rsplit_even_size [OF refl]) 193 apply (simp add: word_size) 194 apply (rule nth_equalityI[symmetric]) 195 apply simp 196 apply (subgoal_tac "[0,1,2,3] = [0..<4]") 197 apply clarsimp 198 apply (rule nth_equalityI[symmetric]) 199 apply simp 200 apply (auto dest: nat_less_4_cases)[1] 201 apply (frule more_pageBits_inner_beauty) 202 apply (simp add: byte_to_word_heap_upd_neq aligned_already_mask al 203 byte_to_word_heap_upd_neq [where n=0, simplified]) 204 apply (subst index_update2) 205 apply (cut_tac x=off in unat_lt2p, simp) 206 apply simp 207 apply simp 208 done 209 210(* This lemma is true for trivial reason. 211 But it might become non-trivial if we change our way of modeling device memory *) 212lemma user_data_device_relation_upd: 213 assumes al: "is_aligned ptr 2" 214 shows "cuser_user_data_device_relation 215 (byte_to_word_heap 216 (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits)) 217 (the (cslift s (Ptr (ptr && ~~ mask pageBits)))) \<Longrightarrow> 218 cuser_user_data_device_relation 219 (byte_to_word_heap 220 ((underlying_memory (ksMachineState \<sigma>)) 221 (ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, 222 ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) 223 (ptr && ~~ mask pageBits)) 224 (user_data_device_C.words_C_update 225 (\<lambda>ws. Arrays.update ws (unat (ucast ((ptr && mask pageBits) >> 2):: 10 word)) w) 226 (the (cslift s (Ptr (ptr && ~~ mask pageBits)))))" 227 by (simp add:cuser_user_data_device_relation_def ) 228 (* If we use identity map, the following proof might be useful 229 unfolding cuser_user_data_device_relation_def 230 apply - 231 apply (erule allEI) 232 apply (case_tac "off = ucast ((ptr && mask pageBits) >> 2)") 233 apply (clarsimp simp: mask_pageBits_inner_beauty [OF al] byte_to_word_heap_def) 234 apply (subst index_update) 235 apply (simp, unat_arith, simp) 236 apply (subgoal_tac "map ((!) (word_rsplit w)) [0,1,2,3] 237 = (word_rsplit w :: word8 list)") 238 apply (clarsimp simp: word_rcat_rsplit) 239 apply (cut_tac w=w and m=4 and 'a=8 240 in length_word_rsplit_even_size [OF refl]) 241 apply (simp add: word_size) 242 apply (rule nth_equalityI[symmetric]) 243 apply simp 244 apply (subgoal_tac "[0,1,2,3] = [0..<4]") 245 apply clarsimp 246 apply (rule nth_equalityI[symmetric]) 247 apply simp 248 apply (auto dest: nat_less_4_cases)[1] 249 apply (frule more_pageBits_inner_beauty) 250 apply (simp add: byte_to_word_heap_upd_neq aligned_already_mask al 251 byte_to_word_heap_upd_neq [where n=0, simplified]) 252 apply (subst index_update2) 253 apply (cut_tac x=off in unat_lt2p, simp) 254 apply simp 255 apply simp 256 done 257 *) 258 259lemma deviceDataSeperate: 260 "\<lbrakk>\<not> pointerInDeviceData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserDataDevice\<rbrakk> 261 \<Longrightarrow> ptr \<noteq> x" 262 apply (rule ccontr,clarsimp) 263 apply (frule(1) pspace_alignedD') 264 apply (clarsimp simp: pointerInDeviceData_def objBits_simps typ_at'_def ko_wp_at'_def) 265 apply (frule(1) pspace_distinctD') 266 apply (clarsimp simp: objBits_simps) 267 done 268 269lemma userDataSeperate: 270 "\<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData\<rbrakk> 271 \<Longrightarrow> ptr \<noteq> x" 272 apply (rule ccontr,clarsimp) 273 apply (frule(1) pspace_alignedD') 274 apply (clarsimp simp: pointerInUserData_def objBits_simps typ_at'_def ko_wp_at'_def) 275 apply (frule(1) pspace_distinctD') 276 apply (clarsimp simp: objBits_simps) 277 done 278 279lemma pointerInUserData_whole_word[simp]: 280 "\<lbrakk>is_aligned ptr 2; n < 4\<rbrakk> \<Longrightarrow> pointerInUserData (ptr + n) \<sigma> = pointerInUserData ptr \<sigma>" 281 apply (simp add:pointerInUserData_def pageBits_def) 282 apply (subst and_not_mask_twice[symmetric,where m = 12 and n =2,simplified]) 283 apply (simp add: neg_mask_add_aligned[where n=2,simplified]) 284 done 285 286lemma pointerInDeviceData_whole_word[simp]: 287 "\<lbrakk>is_aligned ptr 2; n < 4\<rbrakk> \<Longrightarrow> pointerInDeviceData (ptr + n) \<sigma> = pointerInDeviceData ptr \<sigma>" 288 apply (simp add:pointerInDeviceData_def pageBits_def) 289 apply (subst and_not_mask_twice[symmetric,where m = 12 and n =2,simplified]) 290 apply (simp add: neg_mask_add_aligned[where n=2,simplified]) 291 done 292 293lemma du_ptr_disjoint: 294 "pointerInDeviceData ptr \<sigma> \<Longrightarrow> \<not> pointerInUserData ptr \<sigma>" 295 "pointerInUserData ptr \<sigma> \<Longrightarrow> \<not> pointerInDeviceData ptr \<sigma>" 296 by (auto simp: pointerInDeviceData_def pointerInUserData_def typ_at'_def ko_wp_at'_def) 297 298lemma heap_to_device_data_seperate: 299 "\<lbrakk> \<not> pointerInDeviceData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>\<rbrakk> 300 \<Longrightarrow> heap_to_device_data (ksPSpace \<sigma>) (fun_upd ms ptr a) x 301 = heap_to_device_data (ksPSpace \<sigma>) ms x" 302 apply (simp add : heap_to_device_data_def) 303 apply (case_tac "map_to_user_data_device (ksPSpace \<sigma>) x") 304 apply simp 305 apply simp 306 apply (clarsimp simp add: projectKO_opt_user_data_device map_comp_def 307 split: option.split_asm kernel_object.splits) 308 apply (frule deviceDataSeperate) 309 apply simp+ 310 apply (frule(1) pspace_alignedD') 311 apply (simp add: objBits_simps) 312 apply (rule ext) 313 apply (subst AND_NOT_mask_plus_AND_mask_eq[symmetric,where n =2]) 314 apply (subst byte_to_word_heap_upd_neq[where n = "ptr && mask 2",simplified]) 315 apply (erule is_aligned_weaken,simp add:pageBits_def) 316 apply simp+ 317 apply (clarsimp simp: pointerInDeviceData_def pageBits_def) 318 apply (subst(asm) and_not_mask_twice[symmetric,where m = 12 and n =2,simplified]) 319 apply (drule sym[where t=" ptr && ~~ mask 2"]) 320 apply simp 321 apply (subst(asm) neg_mask_add_aligned,assumption) 322 apply (rule word_less_power_trans2[where k = 2,simplified]) 323 apply (simp add: pageBits_def) 324 apply (rule less_le_trans[OF ucast_less],simp+) 325 apply (clarsimp simp: typ_at'_def ko_wp_at'_def pageBits_def objBits_simps 326 dest!: pspace_distinctD') 327 apply (rule word_and_less') 328 apply (simp add:mask_def) 329 apply simp 330 done 331 332lemma heap_to_user_data_seperate: 333 "\<lbrakk> \<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>\<rbrakk> 334 \<Longrightarrow> heap_to_user_data (ksPSpace \<sigma>) (fun_upd ms ptr a) x 335 = heap_to_user_data (ksPSpace \<sigma>) ms x" 336 apply (simp add : heap_to_user_data_def) 337 apply (case_tac "map_to_user_data (ksPSpace \<sigma>) x") 338 apply simp 339 apply simp 340 apply (clarsimp simp add: projectKO_opt_user_data map_comp_def 341 split: option.split_asm kernel_object.splits) 342 apply (frule userDataSeperate) 343 apply simp+ 344 apply (frule(1) pspace_alignedD') 345 apply (simp add:objBits_simps) 346 apply (rule ext) 347 apply (subst AND_NOT_mask_plus_AND_mask_eq[symmetric,where n =2]) 348 apply (subst byte_to_word_heap_upd_neq[where n = "ptr && mask 2",simplified]) 349 apply (erule is_aligned_weaken, simp add: pageBits_def) 350 apply simp+ 351 apply (clarsimp simp: pointerInUserData_def pageBits_def) 352 apply (subst(asm) and_not_mask_twice[symmetric,where m = 12 and n =2,simplified]) 353 apply (drule sym[where t=" ptr && ~~ mask 2"]) 354 apply simp 355 apply (subst(asm) neg_mask_add_aligned,assumption) 356 apply (rule word_less_power_trans2[where k = 2,simplified]) 357 apply (simp add: pageBits_def) 358 apply (rule less_le_trans[OF ucast_less],simp+) 359 apply (clarsimp simp: typ_at'_def ko_wp_at'_def pageBits_def objBits_simps 360 dest!: pspace_distinctD') 361 apply (rule word_and_less') 362 apply (simp add:mask_def) 363 apply simp 364 done 365 366lemma storeWordUser_rf_sr_upd': 367 shows "\<forall>\<sigma> s. 368 (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> 369 \<and> pointerInUserData ptr \<sigma> \<and> is_aligned ptr 2 \<longrightarrow> 370 (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. 371 m(ptr := word_rsplit (w::word32) ! 3, ptr + 1 := word_rsplit w ! 2, 372 ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) 373 (ksMachineState \<sigma>)\<rparr>, 374 s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (Ptr ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr" 375 (is "\<forall>\<sigma> s. ?P \<sigma> s \<longrightarrow> 376 (\<sigma>\<lparr>ksMachineState := ?ms \<sigma>\<rparr>, 377 s\<lparr>globals := globals s\<lparr>t_hrs_' := ?ks' s\<rparr>\<rparr>) \<in> rf_sr") 378proof (intro allI impI) 379 fix \<sigma> s 380 let ?thesis = "(\<sigma>\<lparr>ksMachineState := ?ms \<sigma>\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := ?ks' s\<rparr>\<rparr>) \<in> rf_sr" 381 let ?ms = "?ms \<sigma>" 382 let ?ks' = "?ks' s" 383 let ?ptr = "Ptr ptr :: word32 ptr" 384 let ?hp = "t_hrs_' (globals s)" 385 386 assume "?P \<sigma> s" 387 hence rf: "(\<sigma>, s) \<in> rf_sr" and al: "is_aligned ptr 2" 388 and pal: "pspace_aligned' \<sigma>" and pdst: "pspace_distinct' \<sigma>" 389 and piud: "pointerInUserData ptr \<sigma>" 390 by simp_all 391 392 define offset where "offset \<equiv> ucast ((ptr && mask pageBits) >> 2) :: 10 word" 393 define base where "base \<equiv> Ptr (ptr && ~~ mask pageBits) :: user_data_C ptr" 394 395 from piud 396 obtain old_w where 397 old_w: "heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (ptr_val base) = Some old_w" 398 apply (clarsimp simp: heap_to_user_data_def pointerInUserData_def Let_def) 399 apply (drule user_data_at_ko) 400 apply (drule ko_at_projectKO_opt) 401 apply (simp add: base_def) 402 done 403 404 from rf 405 obtain page :: user_data_C 406 where page: "cslift s base = Some page" 407 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) 408 apply (erule cmap_relationE1, rule old_w) 409 apply simp 410 done 411 412 from page 413 have page_def: "page = the (cslift s base)" by simp 414 415 have size_td_list_map[rule_format, OF order_refl]: 416 "\<And>f xs v S. set xs \<subseteq> S \<longrightarrow> (\<forall>x. x \<in> S \<longrightarrow> size_td_pair (f x) = v) 417 \<longrightarrow> size_td_list (map f xs) = v * length xs" 418 apply (induct_tac xs) 419 apply simp_all 420 done 421 422 have user_data_upd: 423 "\<And>A f v. heap_update base (user_data_C.words_C_update f v) = 424 heap_update (ptr_coerce base) (f (user_data_C.words_C v))" 425 apply (rule ext) 426 apply (simp add: heap_update_def to_bytes_def) 427 apply (simp add: user_data_C_typ_tag user_data_C_tag_def) 428 apply (simp add: final_pad_def Let_def) 429 apply (simp add: align_td_array' cong: if_cong) 430 apply (simp add: ti_typ_pad_combine_def Let_def ti_typ_combine_def adjust_ti_def empty_typ_info_def size_td_array cong: if_cong) 431 apply (simp add: padup_def) 432 apply (simp add: typ_info_array') 433 apply (simp add: size_of_def size_td_list_map) 434 done 435 436 have ud_split: "\<And>x z. user_data_C.words_C_update (\<lambda>_. x) z = user_data_C x" 437 by (case_tac z, simp) 438 439 have map_td_list_map: 440 "\<And>f xs. map_td_list f xs = map (map_td_pair f) xs" 441 by (induct_tac xs, simp_all) 442 443 have update_ti_t_Cons_foo: 444 "\<And>Cons upd adjs f v v'. \<lbrakk> v = Cons v'; \<And>a ys v. length ys = size_td_pair a 445 \<Longrightarrow> update_ti_pair (map_td_pair f a) ys (Cons v) = Cons (update_ti_pair a ys v) \<rbrakk> 446 \<Longrightarrow> \<forall>xs. update_ti_list_t (map_td_list f adjs) xs v 447 = Cons (update_ti_list_t adjs xs v')" 448 apply (simp add: update_ti_list_t_def split: if_split) 449 apply (induct_tac adjs) 450 apply simp 451 apply clarsimp 452 done 453 454 note if_cong[cong] 455 have hval: 456 "\<And>hp. h_val hp base = user_data_C (h_val hp (ptr_coerce base))" 457 apply (simp add: h_val_def base_def from_bytes_def) 458 apply (simp add: user_data_C_typ_tag user_data_C_tag_def) 459 apply (simp add: final_pad_def Let_def) 460 apply (simp add: align_td_array' cong: if_cong) 461 apply (simp add: ti_typ_pad_combine_def Let_def ti_typ_combine_def adjust_ti_def empty_typ_info_def size_td_array) 462 apply (simp add: padup_def size_of_def typ_info_array' size_td_list_map) 463 apply (simp add: map_td_list_map) 464 apply (rule injD[where f=user_data_C.words_C]) 465 apply (rule injI) 466 apply (case_tac x, case_tac y, simp) 467 apply (simp add: map_td_list_map del: map_map) 468 apply (rule trans, rule_tac acc=user_data_C.words_C 469 and f="map_td_pair (K (K (update_desc user_data_C (\<lambda>a b. user_data_C.words_C a))))" 470 in update_ti_t_acc_foo[rule_format]) 471 apply (clarsimp simp: map_td_list_map typ_info_word 472 adjust_ti_def update_desc_def) 473 apply simp 474 apply simp 475 apply (simp add: update_ti_list_array'[where g="\<lambda>n. typ_info_t TYPE(word32)", OF refl] 476 typ_info_word adjust_ti_def update_desc_def) 477 apply (rule Arrays.cart_eq[THEN iffD2], clarsimp) 478 apply (subst index_fold_update | clarsimp)+ 479 apply (subst if_P, arith)+ 480 apply simp 481 done 482 483 from and_mask_less_size [of pageBits ptr] 484 have ptr_mask_less: "ptr && mask pageBits >> 2 < 2^10" 485 apply - 486 apply (rule shiftr_less_t2n) 487 apply (simp add: pageBits_def word_size) 488 done 489 hence uoffset: 490 "unat offset = unat (ptr && mask pageBits >> 2)" 491 apply (simp add: offset_def) 492 apply (simp add: unat_ucast) 493 apply (simp add: word_less_nat_alt) 494 done 495 496 have heap_upd: 497 "heap_update ?ptr w = 498 (\<lambda>hp. heap_update base (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val hp base)) hp)" 499 apply (rule ext) 500 apply (subst user_data_upd) 501 apply (subst hval) 502 apply (unfold base_def uoffset) 503 apply simp 504 apply (subst heap_update_Array_element) 505 apply (insert ptr_mask_less)[1] 506 apply (simp add: word_less_nat_alt) 507 apply (simp add: ptr_add_def word_shift_by_2 shiftr_shiftl1) 508 apply (simp add: is_aligned_neg_mask_eq al is_aligned_andI1) 509 apply (simp add: word_plus_and_or_coroll2 add.commute) 510 done 511 512 have x': "\<And>x::10 word. (ucast x * 4::word32) && ~~ mask pageBits = 0" 513 proof - 514 fix x::"10 word" 515 have "ucast x * 4 = (ucast x << 2 :: word32)" 516 by (simp add: shiftl_t2n) 517 thus "?thesis x" 518 apply simp 519 apply (rule word_eqI) 520 apply (clarsimp simp: word_size nth_shiftl word_ops_nth_size nth_ucast) 521 apply (drule test_bit_size) 522 apply (clarsimp simp: word_size pageBits_def) 523 apply arith 524 done 525 qed 526 527 have x: "\<And>(x::word32) (y::10 word). 528 is_aligned x pageBits \<Longrightarrow> x + ucast y * 4 && ~~ mask pageBits = x" 529 apply (subst mask_out_add_aligned [symmetric], assumption) 530 apply (clarsimp simp: x') 531 done 532 533 from piud al 534 have relrl: "cmap_relation (heap_to_user_data (ksPSpace \<sigma>) 535 (underlying_memory (ksMachineState \<sigma>))) 536 (cslift s) Ptr cuser_user_data_relation 537 \<Longrightarrow> cmap_relation 538 (heap_to_user_data (ksPSpace \<sigma>) 539 ((underlying_memory (ksMachineState \<sigma>))( 540 ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, 541 ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0))) 542 (\<lambda>y. if ptr_val y = (ptr_val ?ptr) && ~~ mask pageBits 543 then Some (user_data_C.words_C_update 544 (\<lambda>ws. Arrays.update ws (unat (ucast ((ptr && mask pageBits) >> 2) :: 10 word)) w) 545 (the (cslift s y))) 546 else cslift s y) 547 Ptr cuser_user_data_relation" 548 apply - 549 apply (rule cmap_relationI) 550 apply (clarsimp simp: dom_heap_to_user_data cmap_relation_def dom_if_Some 551 intro!: Un_absorb1 [symmetric]) 552 apply (clarsimp simp: pointerInUserData_def) 553 apply (drule user_data_at_ko) 554 apply (drule ko_at_projectKO_opt) 555 apply (case_tac x) 556 apply clarsimp 557 apply fastforce 558 apply clarsimp 559 apply (case_tac "x = ptr && ~~ mask pageBits") 560 apply (fastforce simp: heap_to_user_data_def Let_def user_data_relation_upd cmap_relation_def 561 dest: bspec) 562 apply clarsimp 563 apply (subgoal_tac "Some v = heap_to_user_data (ksPSpace \<sigma>) 564 (underlying_memory (ksMachineState \<sigma>)) x") 565 apply (clarsimp simp: heap_to_user_data_def Let_def map_option_case 566 split: option.split_asm) 567 apply (fastforce simp: cmap_relation_def dest: bspec) 568 apply (clarsimp simp: heap_to_user_data_def Let_def) 569 apply (frule (1) cmap_relation_cs_atD) 570 apply simp 571 apply clarsimp 572 apply (drule map_to_ko_atI) 573 apply (rule pal) 574 apply (rule pdst) 575 apply (subgoal_tac "is_aligned x pageBits") 576 prefer 2 577 apply (clarsimp simp: obj_at'_def objBits_simps simp: projectKOs) 578 apply (subgoal_tac "is_aligned x 2") 579 prefer 2 580 apply (erule is_aligned_weaken) 581 apply (simp add: pageBits_def) 582 apply (rule ext) 583 apply (subst byte_to_word_heap_upd_neq, assumption+, clarsimp simp: x, simp)+ 584 apply (subst byte_to_word_heap_upd_neq [where n=0, simplified], assumption+) 585 apply (clarsimp simp: x) 586 apply simp 587 done 588 589 have hrs_mem: 590 "\<And>f hp'. 591 hrs_mem_update (\<lambda>hp. heap_update base (f (h_val hp base)) hp) hp' 592 = hrs_mem_update (heap_update base (f (h_val (hrs_mem hp') base))) hp'" 593 by (simp add: hrs_mem_update_def split_def hrs_mem_def) 594 595 from page 596 have rl': "typ_uinfo_t TYPE(user_data_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('t :: mem_type) \<Longrightarrow> 597 (clift (hrs_mem_update (heap_update ?ptr w) (t_hrs_' (globals s))) :: ('t :: mem_type) typ_heap) 598 = cslift s" 599 apply (subst heap_upd) 600 apply (subst hrs_mem) 601 apply (simp add: typ_heap_simps clift_heap_update_same) 602 done 603 604 have subset: "{ptr..+ 2 ^ 2} \<subseteq> {ptr && ~~ mask pageBits ..+ 2 ^ pageBits}" 605 apply (simp only: upto_intvl_eq al is_aligned_neg_mask2) 606 apply (cut_tac ptr="ptr && ~~ mask pageBits" and x="ptr && mask pageBits" 607 in aligned_range_offset_subset, rule is_aligned_neg_mask2) 608 apply (rule is_aligned_andI1[OF al]) 609 apply (simp add: pageBits_def) 610 apply (rule and_mask_less', simp add: pageBits_def) 611 apply (erule order_trans[rotated]) 612 apply (simp add: mask_out_sub_mask) 613 done 614 615 hence zr: "\<And>rs. zero_ranges_are_zero rs (hrs_mem_update (heap_update ?ptr w) (t_hrs_' (globals s))) 616 = zero_ranges_are_zero rs (t_hrs_' (globals s))" 617 using page 618 apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def 619 heap_update_def 620 intro!: ball_cong[OF refl] conj_cong[OF refl]) 621 apply (drule region_actually_is_bytes) 622 apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift]) 623 apply simp 624 apply (subst heap_list_update_disjoint_same, simp_all) 625 apply ((subst Int_commute)?, erule disjoint_subset2[rotated]) 626 apply (simp add: pageBits_def) 627 done 628 629 have cmap_relation_heap_cong: 630 "\<And>as cs cs' f rel. \<lbrakk> cmap_relation as cs f rel; cs = cs' \<rbrakk> \<Longrightarrow> cmap_relation as cs' f rel" 631 by simp 632 633 from rf have "cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s))" 634 unfolding rf_sr_def cstate_relation_def by (simp add: Let_def) 635 hence "cpspace_relation (ksPSpace \<sigma>) (underlying_memory ?ms) ?ks'" 636 unfolding cpspace_relation_def using page 637 apply - 638 apply (clarsimp simp: rl' tag_disj_via_td_name) 639 apply (drule relrl) 640 apply (simp add: heap_upd) 641 apply (subst hrs_mem) 642 apply (simp add: base_def offset_def) 643 apply (rule conjI) 644 apply (erule cmap_relation_heap_cong) 645 apply (simp add: typ_heap_simps') 646 apply (rule ext) 647 apply clarsimp 648 apply (case_tac y) 649 apply (clarsimp split: if_split) 650 apply (rule cmap_relationI) 651 apply (clarsimp simp: dom_heap_to_device_data cmap_relation_def dom_if_Some 652 intro!: Un_absorb1 [symmetric]) 653 using pal 654 apply (subst(asm) heap_to_device_data_seperate) 655 apply (simp add:piud al du_ptr_disjoint pal pdst)+ 656 apply (subst(asm) heap_to_device_data_seperate) 657 apply (simp add:piud al du_ptr_disjoint pal pdst)+ 658 apply (subst(asm) heap_to_device_data_seperate) 659 apply (simp add:piud al du_ptr_disjoint pal pdst)+ 660 apply (subst(asm) heap_to_device_data_seperate) 661 apply (simp add:piud al du_ptr_disjoint pal pdst)+ 662 apply (erule cmap_relation_relI[where rel = cuser_user_data_device_relation]) 663 apply simp+ 664 done 665 666 thus ?thesis using rf 667 apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name) 668 apply (simp add: carch_state_relation_def cmachine_state_relation_def carch_globals_def) 669 apply (simp add: rl' tag_disj_via_td_name zr) 670 done 671qed 672 673 674lemma storeWordDevice_rf_sr_upd': 675 shows "\<forall>\<sigma> s. 676 (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> 677 \<and> pointerInDeviceData ptr \<sigma> \<and> is_aligned ptr 2 \<longrightarrow> 678 (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. 679 m(ptr := word_rsplit (w::word32) ! 3, ptr + 1 := word_rsplit w ! 2, 680 ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0)) 681 (ksMachineState \<sigma>)\<rparr>, 682 s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (Ptr ptr) w) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr" 683 (is "\<forall>\<sigma> s. ?P \<sigma> s \<longrightarrow> 684 (\<sigma>\<lparr>ksMachineState := ?ms \<sigma>\<rparr>, 685 s\<lparr>globals := globals s\<lparr>t_hrs_' := ?ks' s\<rparr>\<rparr>) \<in> rf_sr") 686proof (intro allI impI) 687 fix \<sigma> s 688 let ?thesis = "(\<sigma>\<lparr>ksMachineState := ?ms \<sigma>\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := ?ks' s\<rparr>\<rparr>) \<in> rf_sr" 689 let ?ms = "?ms \<sigma>" 690 let ?ks' = "?ks' s" 691 let ?ptr = "Ptr ptr :: word32 ptr" 692 let ?hp = "t_hrs_' (globals s)" 693 694 assume "?P \<sigma> s" 695 hence rf: "(\<sigma>, s) \<in> rf_sr" and al: "is_aligned ptr 2" 696 and pal: "pspace_aligned' \<sigma>" and pdst: "pspace_distinct' \<sigma>" 697 and piud: "pointerInDeviceData ptr \<sigma>" 698 by simp_all 699 700 define offset where "offset \<equiv> ucast ((ptr && mask pageBits) >> 2) :: 10 word" 701 define base where "base \<equiv> Ptr (ptr && ~~ mask pageBits) :: user_data_device_C ptr" 702 703 from piud 704 obtain old_w where 705 old_w: "heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (ptr_val base) = Some old_w" 706 apply (clarsimp simp: heap_to_device_data_def pointerInDeviceData_def Let_def) 707 apply (drule device_data_at_ko) 708 apply (drule ko_at_projectKO_opt) 709 apply (simp add: base_def) 710 done 711 712 from rf 713 obtain page :: user_data_device_C 714 where page: "cslift s base = Some page" 715 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) 716 apply (erule cmap_relationE1, rule old_w) 717 apply simp 718 done 719 720 from page 721 have page_def: "page = the (cslift s base)" by simp 722 723 have size_td_list_map[rule_format, OF order_refl]: 724 "\<And>f xs v S. set xs \<subseteq> S \<longrightarrow> (\<forall>x. x \<in> S \<longrightarrow> size_td_pair (f x) = v) 725 \<longrightarrow> size_td_list (map f xs) = v * length xs" 726 apply (induct_tac xs) 727 apply simp_all 728 done 729 730 have user_data_upd: 731 "\<And>A f v. heap_update base (user_data_device_C.words_C_update f v) = 732 heap_update (ptr_coerce base) (f (user_data_device_C.words_C v))" 733 apply (rule ext) 734 apply (simp add: heap_update_def to_bytes_def) 735 apply (simp add: user_data_device_C_typ_tag user_data_device_C_tag_def) 736 apply (simp add: final_pad_def Let_def) 737 apply (simp add: align_td_array' cong: if_cong) 738 apply (simp add: ti_typ_pad_combine_def Let_def ti_typ_combine_def adjust_ti_def empty_typ_info_def size_td_array cong: if_cong) 739 apply (simp add: padup_def) 740 apply (simp add: typ_info_array') 741 apply (simp add: size_of_def size_td_list_map) 742 done 743 744 have ud_split: "\<And>x z. user_data_device_C.words_C_update (\<lambda>_. x) z = user_data_device_C x" 745 by (case_tac z, simp) 746 747 have map_td_list_map: 748 "\<And>f xs. map_td_list f xs = map (map_td_pair f) xs" 749 by (induct_tac xs, simp_all) 750 751 have update_ti_t_Cons_foo: 752 "\<And>Cons upd adjs f v v'. \<lbrakk> v = Cons v'; \<And>a ys v. length ys = size_td_pair a 753 \<Longrightarrow> update_ti_pair (map_td_pair f a) ys (Cons v) = Cons (update_ti_pair a ys v) \<rbrakk> 754 \<Longrightarrow> \<forall>xs. update_ti_list_t (map_td_list f adjs) xs v 755 = Cons (update_ti_list_t adjs xs v')" 756 apply (simp add: update_ti_list_t_def split: if_split) 757 apply (induct_tac adjs) 758 apply simp 759 apply clarsimp 760 done 761 762 note if_cong[cong] 763 have hval: 764 "\<And>hp. h_val hp base = user_data_device_C (h_val hp (ptr_coerce base))" 765 apply (simp add: h_val_def base_def from_bytes_def) 766 apply (simp add: user_data_device_C_typ_tag user_data_device_C_tag_def) 767 apply (simp add: final_pad_def Let_def) 768 apply (simp add: align_td_array' cong: if_cong) 769 apply (simp add: ti_typ_pad_combine_def Let_def ti_typ_combine_def adjust_ti_def empty_typ_info_def size_td_array) 770 apply (simp add: padup_def size_of_def typ_info_array' size_td_list_map) 771 apply (simp add: map_td_list_map) 772 apply (rule injD[where f=user_data_device_C.words_C]) 773 apply (rule injI) 774 apply (case_tac x, case_tac y, simp) 775 apply (simp add: map_td_list_map del: map_map) 776 apply (rule trans, rule_tac acc=user_data_device_C.words_C 777 and f="map_td_pair (K (K (update_desc user_data_device_C (\<lambda>a b. user_data_device_C.words_C a))))" 778 in update_ti_t_acc_foo[rule_format]) 779 apply (clarsimp simp: map_td_list_map typ_info_word 780 adjust_ti_def update_desc_def) 781 apply simp 782 apply simp 783 apply (simp add: update_ti_list_array'[where g="\<lambda>n. typ_info_t TYPE(word32)", OF refl] 784 typ_info_word adjust_ti_def update_desc_def) 785 apply (rule Arrays.cart_eq[THEN iffD2], clarsimp) 786 apply (subst index_fold_update | clarsimp)+ 787 apply (subst if_P, arith)+ 788 apply simp 789 done 790 791 from and_mask_less_size [of pageBits ptr] 792 have ptr_mask_less: "ptr && mask pageBits >> 2 < 2^10" 793 apply - 794 apply (rule shiftr_less_t2n) 795 apply (simp add: pageBits_def word_size) 796 done 797 hence uoffset: 798 "unat offset = unat (ptr && mask pageBits >> 2)" 799 apply (simp add: offset_def) 800 apply (simp add: unat_ucast) 801 apply (simp add: word_less_nat_alt) 802 done 803 804 have heap_upd: 805 "heap_update ?ptr w = 806 (\<lambda>hp. heap_update base (user_data_device_C.words_C_update (\<lambda>ws. Arrays.update ws (unat offset) w) (h_val hp base)) hp)" 807 apply (rule ext) 808 apply (subst user_data_upd) 809 apply (subst hval) 810 apply (unfold base_def uoffset) 811 apply simp 812 apply (subst heap_update_Array_element) 813 apply (insert ptr_mask_less)[1] 814 apply (simp add: word_less_nat_alt) 815 apply (simp add: ptr_add_def word_shift_by_2 shiftr_shiftl1) 816 apply (simp add: is_aligned_neg_mask_eq al is_aligned_andI1) 817 apply (simp add: word_plus_and_or_coroll2 add.commute) 818 done 819 820 have x': "\<And>x::10 word. (ucast x * 4::word32) && ~~ mask pageBits = 0" 821 proof - 822 fix x::"10 word" 823 have "ucast x * 4 = (ucast x << 2 :: word32)" 824 by (simp add: shiftl_t2n) 825 thus "?thesis x" 826 apply simp 827 apply (rule word_eqI) 828 apply (clarsimp simp: word_size nth_shiftl word_ops_nth_size nth_ucast) 829 apply (drule test_bit_size) 830 apply (clarsimp simp: word_size pageBits_def) 831 apply arith 832 done 833 qed 834 835 have x: "\<And>(x::word32) (y::10 word). 836 is_aligned x pageBits \<Longrightarrow> x + ucast y * 4 && ~~ mask pageBits = x" 837 apply (subst mask_out_add_aligned [symmetric], assumption) 838 apply (clarsimp simp: x') 839 done 840 841 from piud al 842 have relrl: "cmap_relation (heap_to_device_data (ksPSpace \<sigma>) 843 (underlying_memory (ksMachineState \<sigma>))) 844 (cslift s) Ptr cuser_user_data_device_relation 845 \<Longrightarrow> cmap_relation 846 (heap_to_device_data (ksPSpace \<sigma>) 847 ((underlying_memory (ksMachineState \<sigma>))( 848 ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, 849 ptr + 2 := word_rsplit w ! 1, ptr + 3 := word_rsplit w ! 0))) 850 (\<lambda>y. if ptr_val y = (ptr_val ?ptr) && ~~ mask pageBits 851 then Some (user_data_device_C.words_C_update 852 (\<lambda>ws. Arrays.update ws (unat (ucast ((ptr && mask pageBits) >> 2) :: 10 word)) w) 853 (the (cslift s y))) 854 else cslift s y) 855 Ptr cuser_user_data_device_relation" 856 apply - 857 apply (rule cmap_relationI) 858 apply (clarsimp simp: dom_heap_to_device_data cmap_relation_def dom_if_Some 859 intro!: Un_absorb1 [symmetric]) 860 apply (clarsimp simp: pointerInDeviceData_def) 861 apply (drule device_data_at_ko) 862 apply (drule ko_at_projectKO_opt) 863 apply (case_tac x) 864 apply clarsimp 865 apply fastforce 866 apply clarsimp 867 apply (case_tac "x = ptr && ~~ mask pageBits") 868 apply (fastforce simp: heap_to_device_data_def Let_def user_data_device_relation_upd cmap_relation_def 869 dest: bspec) 870 apply clarsimp 871 apply (subgoal_tac "Some v = heap_to_device_data (ksPSpace \<sigma>) 872 (underlying_memory (ksMachineState \<sigma>)) x") 873 apply (clarsimp simp: heap_to_device_data_def Let_def map_option_case 874 split: option.split_asm) 875 apply (fastforce simp: cmap_relation_def dest: bspec) 876 apply (clarsimp simp: heap_to_device_data_def Let_def) 877 apply (frule (1) cmap_relation_cs_atD) 878 apply simp 879 apply clarsimp 880 apply (drule map_to_ko_atI) 881 apply (rule pal) 882 apply (rule pdst) 883 apply (subgoal_tac "is_aligned x pageBits") 884 prefer 2 885 apply (clarsimp simp: obj_at'_def objBits_simps simp: projectKOs) 886 apply (subgoal_tac "is_aligned x 2") 887 prefer 2 888 apply (erule is_aligned_weaken) 889 apply (simp add: pageBits_def) 890 apply (rule ext) 891 apply (subst byte_to_word_heap_upd_neq, assumption+, clarsimp simp: x, simp)+ 892 apply (subst byte_to_word_heap_upd_neq [where n=0, simplified], assumption+) 893 apply (clarsimp simp: x) 894 apply simp 895 done 896 897 have hrs_mem: 898 "\<And>f hp'. 899 hrs_mem_update (\<lambda>hp. heap_update base (f (h_val hp base)) hp) hp' 900 = hrs_mem_update (heap_update base (f (h_val (hrs_mem hp') base))) hp'" 901 by (simp add: hrs_mem_update_def split_def hrs_mem_def) 902 903 from page 904 have rl': "typ_uinfo_t TYPE(user_data_device_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('t :: mem_type) \<Longrightarrow> 905 (clift (hrs_mem_update (heap_update ?ptr w) (t_hrs_' (globals s))) :: ('t :: mem_type) typ_heap) 906 = cslift s" 907 apply (subst heap_upd) 908 apply (subst hrs_mem) 909 apply (simp add: typ_heap_simps clift_heap_update_same) 910 done 911 912 have subset: "{ptr..+ 2 ^ 2} \<subseteq> {ptr && ~~ mask pageBits ..+ 2 ^ pageBits}" 913 apply (simp only: upto_intvl_eq al is_aligned_neg_mask2) 914 apply (cut_tac ptr="ptr && ~~ mask pageBits" and x="ptr && mask pageBits" 915 in aligned_range_offset_subset, rule is_aligned_neg_mask2) 916 apply (rule is_aligned_andI1[OF al]) 917 apply (simp add: pageBits_def) 918 apply (rule and_mask_less', simp add: pageBits_def) 919 apply (erule order_trans[rotated]) 920 apply (simp add: mask_out_sub_mask) 921 done 922 923 hence zr: "\<And>rs. zero_ranges_are_zero rs (hrs_mem_update (heap_update ?ptr w) (t_hrs_' (globals s))) 924 = zero_ranges_are_zero rs (t_hrs_' (globals s))" 925 using page 926 apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def 927 heap_update_def 928 intro!: ball_cong[OF refl] conj_cong[OF refl]) 929 apply (drule region_actually_is_bytes) 930 apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift]) 931 apply simp 932 apply (subst heap_list_update_disjoint_same, simp_all) 933 apply ((subst Int_commute)?, erule disjoint_subset2[rotated]) 934 apply (simp add: pageBits_def) 935 done 936 937 have cmap_relation_heap_cong: 938 "\<And>as cs cs' f rel. \<lbrakk> cmap_relation as cs f rel; cs = cs' \<rbrakk> \<Longrightarrow> cmap_relation as cs' f rel" 939 by simp 940 941 from rf have "cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals s))" 942 unfolding rf_sr_def cstate_relation_def by (simp add: Let_def) 943 hence "cpspace_relation (ksPSpace \<sigma>) (underlying_memory ?ms) ?ks'" 944 unfolding cpspace_relation_def using page 945 apply - 946 apply (clarsimp simp: rl' tag_disj_via_td_name) 947 apply (drule relrl) 948 apply (simp add: heap_upd) 949 apply (subst hrs_mem) 950 apply (simp add: base_def offset_def) 951 apply (rule conjI[rotated]) 952 apply (erule cmap_relation_heap_cong) 953 apply (simp add: typ_heap_simps') 954 apply (rule ext) 955 apply clarsimp 956 apply (case_tac y) 957 apply (clarsimp split: if_split) 958 apply (rule cmap_relationI) 959 apply (clarsimp simp: dom_heap_to_user_data cmap_relation_def dom_if_Some 960 intro!: Un_absorb1 [symmetric]) 961 using pal 962 apply (subst(asm) heap_to_user_data_seperate) 963 apply (simp add: piud al du_ptr_disjoint pal pdst)+ 964 apply (subst(asm) heap_to_user_data_seperate) 965 apply (simp add: piud al du_ptr_disjoint pal pdst)+ 966 apply (subst(asm) heap_to_user_data_seperate) 967 apply (simp add: piud al du_ptr_disjoint pal pdst)+ 968 apply (subst(asm) heap_to_user_data_seperate) 969 apply (simp add: piud al du_ptr_disjoint pal pdst)+ 970 apply (erule cmap_relation_relI[where rel = cuser_user_data_relation]) 971 apply simp+ 972 done 973 974 thus ?thesis using rf 975 apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name) 976 apply (simp add: carch_state_relation_def cmachine_state_relation_def carch_globals_def) 977 apply (simp add: rl' tag_disj_via_td_name zr) 978 done 979qed 980 981lemma storeWord_rf_sr_upd: 982 "\<lbrakk> (\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; 983 pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 984 (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. 985 m(ptr := word_rsplit (w::word32) ! 3, ptr + 1 := word_rsplit w ! 2, 986 ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) 987 (ksMachineState \<sigma>)\<rparr>, 988 globals_update (t_hrs_'_update (hrs_mem_update 989 (heap_update (Ptr ptr) w))) s) \<in> rf_sr" 990 apply (elim disjE) 991 apply (cut_tac storeWordUser_rf_sr_upd' [rule_format, where s=s and \<sigma>=\<sigma>]) 992 prefer 2 993 apply fastforce 994 apply simp 995 apply (erule iffD1 [OF rf_sr_upd, rotated -1], simp_all)[1] 996 apply (cut_tac storeWordDevice_rf_sr_upd' [rule_format, where s=s and \<sigma>=\<sigma>]) 997 prefer 2 998 apply fastforce 999 apply simp 1000 apply (erule iffD1 [OF rf_sr_upd, rotated -1], simp_all)[1] 1001 done 1002 1003(* The following should be also true for pointerInDeviceData, 1004 but the reason why it is true is different *) 1005lemma storeByteUser_rf_sr_upd: 1006 assumes asms: "(\<sigma>, s) \<in> rf_sr" "pspace_aligned' \<sigma>" "pspace_distinct' \<sigma>" 1007 "pointerInUserData ptr \<sigma>" 1008 shows "(ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, 1009 globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) 1010 \<in> rf_sr" 1011proof - 1012 have horrible_helper: 1013 "\<And>v p. v \<le> 3 \<Longrightarrow> (3 - unat (p && mask 2 :: word32) = v) = 1014 (p && mask 2 = 3 - of_nat v)" 1015 apply (simp add: unat_arith_simps unat_of_nat) 1016 apply (cut_tac p=p in unat_mask_2_less_4) 1017 apply arith 1018 done 1019 1020 have horrible_helper2: 1021 "\<And>n x p. n < 4 \<Longrightarrow> (unat (x - p :: word32) = n) = (x = (p + of_nat n))" 1022 apply (subst unat32_eq_of_nat) 1023 apply (simp add:word_bits_def) 1024 apply (simp only:field_simps) 1025 done 1026 1027 from asms 1028 show ?thesis 1029 apply (frule_tac ptr="ptr && ~~ mask 2" 1030 and w="word_rcat (list_update 1031 (map (underlying_memory (ksMachineState \<sigma>)) 1032 [(ptr && ~~ mask 2) + 3, 1033 (ptr && ~~ mask 2) + 2, 1034 (ptr && ~~ mask 2) + 1, 1035 (ptr && ~~ mask 2)]) 1036 (3 - unat (ptr && mask 2)) b)" 1037 in storeWord_rf_sr_upd) 1038 apply simp+ 1039 apply (simp add: pointerInUserData_def pointerInDeviceData_def mask_lower_twice pageBits_def) 1040 apply (simp add: Aligned.is_aligned_neg_mask) 1041 apply (erule iffD1[rotated], 1042 rule_tac f="\<lambda>a b. (a, b) \<in> rf_sr" and c="globals_update f s" 1043 for f s in arg_cong2) 1044 apply (rule kernel_state.fold_congs[OF refl refl], simp only:) 1045 apply (rule machine_state.fold_congs[OF refl refl], simp only:) 1046 apply (cut_tac p=ptr in unat_mask_2_less_4) 1047 apply (simp del: list_update.simps split del: if_split 1048 add: word_rsplit_rcat_size word_size nth_list_update 1049 horrible_helper) 1050 apply (subgoal_tac "(ptr && ~~ mask 2) + (ptr && mask 2) = ptr") 1051 apply (subgoal_tac "(ptr && mask 2) \<in> {0, 1, 2, 3}") 1052 apply (auto split: if_split simp: fun_upd_idem)[1] 1053 apply (simp add: word_unat.Rep_inject[symmetric] 1054 del: word_unat.Rep_inject) 1055 apply arith 1056 apply (subst add.commute, rule word_plus_and_or_coroll2) 1057 apply (rule StateSpace.state.fold_congs[OF refl refl]) 1058 apply (rule globals.fold_congs[OF refl refl]) 1059 apply (clarsimp simp: hrs_mem_update_def simp del: list_update.simps) 1060 apply (rule ext) 1061 apply (simp add: heap_update_def to_bytes_def typ_info_word 1062 word_rsplit_rcat_size word_size heap_update_list_value' 1063 nth_list_update nth_rev TWO 1064 del: list_update.simps) 1065 apply (subgoal_tac "length (rev ([underlying_memory (ksMachineState \<sigma>) 1066 ((ptr && ~~ mask 2) + 3), 1067 underlying_memory (ksMachineState \<sigma>) 1068 ((ptr && ~~ mask 2) + 2), 1069 underlying_memory (ksMachineState \<sigma>) 1070 ((ptr && ~~ mask 2) + 1), 1071 underlying_memory (ksMachineState \<sigma>) 1072 (ptr && ~~ mask 2)] 1073 [3 - unat (ptr && mask 2) := b])) 1074 < addr_card") 1075 prefer 2 1076 apply (simp add: addr_card del: list_update.simps) 1077 apply (simp add: heap_update_def to_bytes_def typ_info_word 1078 word_rsplit_rcat_size word_size heap_update_list_value' 1079 nth_list_update nth_rev TWO 1080 del: list_update.simps cong: if_cong) 1081 apply (simp only: If_rearrage) 1082 apply (subgoal_tac "P" for P) 1083 apply (rule if_cong) 1084 apply assumption 1085 apply simp 1086 apply (clarsimp simp: nth_list_update split: if_split) 1087 apply (frule_tac ptr=x in memory_cross_over, simp+) 1088 apply (clarsimp simp: pointerInUserData_def pointerInDeviceData_def) 1089 apply (cut_tac p="ptr && ~~ mask 2" and n=2 and d="x - (ptr && ~~ mask 2)" 1090 in is_aligned_add_helper) 1091 apply (simp add: Aligned.is_aligned_neg_mask) 1092 apply (simp add: word_less_nat_alt) 1093 apply clarsimp 1094 apply (cut_tac x=x in mask_lower_twice[where n=2 and m=pageBits]) 1095 apply (simp add: pageBits_def) 1096 apply (cut_tac x=ptr in mask_lower_twice[where n=2 and m=pageBits]) 1097 apply (simp add: pageBits_def) 1098 apply simp 1099 apply (auto simp add: eval_nat_numeral horrible_helper2 1100 elim!: less_SucE)[1] 1101 apply (rule iffI) 1102 apply clarsimp 1103 apply (cut_tac p=ptr in unat_mask_2_less_4) 1104 apply (subgoal_tac "unat (x - (ptr && ~~ mask 2)) = unat (ptr && mask 2)") 1105 prefer 2 1106 apply arith 1107 apply (simp add: unat_mask_2_less_4 field_simps word_plus_and_or_coroll2) 1108 apply (simp add: subtract_mask TWO unat_mask_2_less_4) 1109 done 1110qed 1111 1112lemma storeWord_ccorres': 1113 "ccorres dc xfdc 1114 (pspace_aligned' and pspace_distinct' and 1115 K (is_aligned ptr 2) and (\<lambda>s. pointerInUserData ptr s \<or> pointerInDeviceData ptr s)) 1116 (UNIV \<inter> {s. ptr' s = Ptr ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val}) hs 1117 (doMachineOp $ storeWord ptr val) 1118 (Basic (\<lambda>s. globals_update (t_hrs_'_update 1119 (hrs_mem_update (heap_update (ptr' s) (val' s)))) s))" 1120 apply (clarsimp simp: storeWordUser_def simp del: Collect_const 1121 split del: if_split) 1122 apply (rule ccorres_from_vcg_nofail) 1123 apply (rule allI) 1124 apply (rule conseqPre, vcg) 1125 apply (clarsimp split: if_split_asm) 1126 apply (rule bexI[rotated]) 1127 apply (subst in_doMachineOp) 1128 apply (fastforce simp: storeWord_def in_monad is_aligned_mask) 1129 apply simp 1130 apply (fold fun_upd_def)+ 1131 apply (fastforce elim: storeWord_rf_sr_upd) 1132 done 1133 1134lemma storeWord_ccorres: 1135 "ccorres dc xfdc 1136 (valid_pspace' and K (is_aligned ptr 2) and pointerInUserData ptr) 1137 (UNIV \<inter> {s. ptr' s = Ptr ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val}) hs 1138 (doMachineOp $ storeWord ptr val) 1139 (Basic (\<lambda>s. globals_update (t_hrs_'_update 1140 (hrs_mem_update (heap_update (ptr' s) (val' s)))) s))" 1141 apply (rule ccorres_guard_imp2, rule storeWord_ccorres') 1142 apply fastforce 1143 done 1144 1145lemma pointerInUserData_c_guard: 1146 "\<lbrakk> valid_pspace' s; pointerInUserData ptr s \<or> pointerInDeviceData ptr s ; is_aligned ptr 2 \<rbrakk> 1147 \<Longrightarrow> c_guard (Ptr ptr :: word32 ptr)" 1148 apply (simp add: pointerInUserData_def pointerInDeviceData_def) 1149 apply (simp add: c_guard_def ptr_aligned_def is_aligned_def c_null_guard_def) 1150 apply (fold is_aligned_def [where n=2, simplified])[1] 1151 apply (rule contra_subsetD) 1152 apply (rule order_trans [rotated]) 1153 apply (rule_tac x="ptr && mask pageBits" and y=4 and z=4096 in intvl_sub_offset) 1154 apply (cut_tac y=ptr and a="mask pageBits && (~~ mask 2)" in word_and_le1) 1155 apply (subst(asm) word_bw_assocs[symmetric], subst(asm) is_aligned_neg_mask_eq, 1156 erule is_aligned_andI1) 1157 apply (simp add: word_le_nat_alt mask_def pageBits_def) 1158 apply (subst word_plus_and_or_coroll2 [where w="~~ mask pageBits", simplified]) 1159 apply simp 1160 apply (fastforce dest: intvl_le_lower 1161 intro: is_aligned_no_overflow' [where n=12, simplified] 1162 is_aligned_andI2 1163 simp: mask_def pageBits_def is_aligned_def word_bits_def) 1164 done 1165 1166lemma pointerInUserData_h_t_valid: 1167 "\<lbrakk> valid_pspace' s; pointerInUserData ptr s ; 1168 is_aligned ptr 2; (s, s') \<in> rf_sr \<rbrakk> 1169 \<Longrightarrow> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t (Ptr ptr :: word32 ptr)" 1170 apply (frule_tac p=ptr in 1171 user_word_at_cross_over[rotated, OF _ refl]) 1172 apply (simp add: user_word_at_def) 1173 apply simp 1174 done 1175 1176lemma storeWordUser_ccorres: 1177 "ccorres dc xfdc (valid_pspace' and (\<lambda>_. is_aligned ptr 2)) 1178 (UNIV \<inter> {s. ptr' s = Ptr ptr} \<inter> {s. w' s = w}) hs 1179 (storeWordUser ptr w) 1180 (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>(\<lambda>s. ptr' s)\<rbrace> 1181 (Basic (\<lambda>s. globals_update (t_hrs_'_update 1182 (hrs_mem_update (heap_update (ptr' s) (w' s)))) s)))" 1183 apply (simp add: storeWordUser_def) 1184 apply (rule ccorres_symb_exec_l'[OF _ stateAssert_inv stateAssert_sp empty_fail_stateAssert]) 1185 apply (rule ccorres_guard_imp2) 1186 apply (rule ccorres_Guard) 1187 apply (rule storeWord_ccorres[unfolded fun_app_def]) 1188 apply (clarsimp simp: pointerInUserData_c_guard pointerInUserData_h_t_valid) 1189 done 1190 1191end 1192 1193end 1194