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