1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory LemmaBucket_C 8imports 9 "Lib.Lib" 10 "Word_Lib.WordSetup" 11 TypHeapLib 12 "CParser.ArrayAssertion" 13begin 14 15declare word_neq_0_conv [simp del] 16 17lemma Ptr_not_null_pointer_not_zero: "(Ptr p \<noteq> NULL)=(p\<noteq>0)" 18 by simp 19 20lemma hrs_mem_f: "f (hrs_mem s) = hrs_mem (hrs_mem_update f s)" 21 apply (cases s) 22 apply (clarsimp simp: hrs_mem_def hrs_mem_update_def) 23 done 24 25lemma hrs_mem_heap_update: 26 "heap_update p v (hrs_mem s) = hrs_mem (hrs_mem_update (heap_update p v) s)" 27 apply (rule hrs_mem_f) 28 done 29 30lemma addr_card_wb: 31 "addr_card = 2 ^ word_bits" 32 by (simp add: addr_card_def card_word word_bits_conv) 33 34lemma surj_Ptr [simp]: 35 "surj Ptr" 36 by (rule surjI [where f = ptr_val], simp) 37 38lemma inj_Ptr [simp]: 39 "inj Ptr" 40 apply (rule injI) 41 apply simp 42 done 43 44lemma bij_Ptr : 45 "bij Ptr" 46 by (simp add: bijI) 47 48lemma exec_Guard: 49 "(G \<turnstile> \<langle>Guard Err S c, Normal s\<rangle> \<Rightarrow> s') 50 = (if s \<in> S then G \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> s' 51 else s' = Fault Err)" 52 by (auto split: if_split elim!: exec_elim_cases intro: exec.intros) 53 54lemma to_bytes_word8: 55 "to_bytes (v :: word8) xs = [v]" 56 by (simp add: to_bytes_def typ_info_word word_rsplit_same) 57 58lemma byte_ptr_guarded:"ptr_val (x::8 word ptr) \<noteq> 0 \<Longrightarrow> c_guard x" 59 unfolding c_guard_def c_null_guard_def ptr_aligned_def 60 by (clarsimp simp: intvl_Suc) 61 62lemma heap_update_list_append: 63 fixes v :: word8 64 shows "heap_update_list s (xs @ ys) hp = 65 heap_update_list (s + of_nat (length xs)) ys (heap_update_list s xs hp)" 66proof (induct xs arbitrary: ys rule: rev_induct) 67 case Nil 68 show ?case by simp 69next 70 case (snoc v' vs') 71 show ?case 72 apply (simp add: snoc.hyps field_simps) 73 apply (rule arg_cong [where f = "heap_update_list (1 + (s + of_nat (length vs'))) ys"]) 74 apply (rule ext) 75 apply simp 76 done 77qed 78 79lemma intvl_aligned_bottom_eq: 80 fixes p :: "'a::len word" 81 assumes al1: "is_aligned x n" 82 and al2: "is_aligned p bits" 83 and nb: "\<not> n < bits" 84 and off: "off \<le> 2 ^ bits" "off \<noteq> 0" 85 shows "(x \<in> {p ..+ off}) = (x = p)" 86proof (rule iffI) 87 assume "x = p" 88 thus "x \<in> {p ..+ off}" using off 89 by (simp add: intvl_self) 90next 91 assume x_in_intvl: "x \<in> {p ..+ off}" 92 93 show "x = p" 94 proof cases 95 assume wb: "bits < len_of TYPE('a)" 96 97 from x_in_intvl obtain kp where xp: "x = p + of_nat kp" and kp: "kp < off" 98 by (clarsimp dest!: intvlD) 99 100 hence "is_aligned (p + of_nat kp) n" using al1 by simp 101 hence "2 ^ n dvd unat (p + of_nat kp)" unfolding is_aligned_def . 102 hence "2 ^ n dvd unat p + kp" using kp off wb 103 apply - 104 apply (subst (asm) iffD1 [OF unat_plus_simple]) 105 apply (rule is_aligned_no_wrap' [OF al2]) 106 apply (rule of_nat_power) 107 apply simp_all[2] 108 apply (subst (asm) unat_of_nat) 109 apply (subst (asm) mod_less) 110 apply (erule order_less_le_trans) 111 apply (erule order_trans) 112 apply simp 113 apply simp 114 done 115 116 moreover from al2 obtain q2 where pbits: "p = 2 ^ bits * of_nat q2" 117 and q2: "q2 < 2 ^ (len_of TYPE('a) - bits)" 118 by (rule is_alignedE) 119 120 moreover from nb obtain kn where nbits: "n = bits + kn" 121 by (clarsimp simp: linorder_not_less le_iff_add) 122 123 ultimately have "2 ^ bits dvd 2 ^ bits * q2 + kp" 124 apply (simp add: power_add) 125 apply (simp add: unat_mult_power_lem [OF q2]) 126 apply (erule dvd_mult_left) 127 done 128 129 hence "2 ^ bits dvd kp" by (simp add: dvd_reduce_multiple) 130 with kp have "kp = 0" 131 apply - 132 apply (erule contrapos_pp) 133 apply (simp add: linorder_not_less) 134 apply (drule (1) dvd_imp_le) 135 apply (erule order_trans [OF off(1)]) 136 done 137 138 thus ?thesis using xp by simp 139 next 140 assume wb: "\<not> bits < len_of TYPE('a)" 141 with assms 142 show ?thesis by (simp add: is_aligned_mask mask_def power_overflow) 143 qed 144qed 145 146lemma intvl_mem_weaken: "x \<in> {p..+a - n} \<Longrightarrow> x \<in> {p..+a}" 147 apply - 148 apply (drule intvlD) 149 apply clarsimp 150 apply (rule intvlI) 151 apply simp 152 done 153 154 155lemma upto_intvl_eq: 156 fixes x :: "'a::len word" 157 assumes al: "is_aligned x n" 158 shows "{x..+2 ^ n} = {x .. x + 2 ^ n - 1}" 159proof cases 160 assume "n < len_of TYPE('a)" 161 with assms show ?thesis 162 unfolding intvl_def 163 apply simp 164 apply rule 165 apply clarsimp 166 apply (subgoal_tac "of_nat k < (2 :: 'a word) ^ n") 167 apply (intro conjI) 168 apply (erule (1) is_aligned_no_wrap') 169 apply (subst p_assoc_help) 170 apply (rule word_plus_mono_right) 171 apply (simp add: word_less_sub_1) 172 apply (simp add: field_simps is_aligned_no_overflow) 173 apply (simp add: of_nat_power) 174 apply clarsimp 175 apply (rule_tac x = "unat (xa - x)" in exI) 176 apply clarsimp 177 apply (rule unat_less_power, assumption) 178 apply (subst word_less_sub_le [symmetric]) 179 apply assumption 180 apply (rule word_diff_ls'(4)) 181 apply (simp add: field_simps) 182 apply assumption 183 done 184next 185 assume "\<not> n < len_of TYPE('a)" 186 with assms show ?thesis 187 apply (simp add: is_aligned_mask mask_def power_overflow intvl_def) 188 apply (rule set_eqI) 189 apply clarsimp 190 apply (rename_tac w) 191 apply (case_tac w) 192 apply (rename_tac m) 193 apply (rule_tac x=m in exI) 194 apply simp 195 apply (erule order_less_le_trans) 196 apply simp 197 done 198qed 199 200lemma upto_intvl_eq': 201 fixes x :: "'a :: len word" 202 shows "\<lbrakk> x \<le> x + (of_nat b - 1); b \<noteq> 0; b \<le> 2 ^ len_of TYPE('a)\<rbrakk> \<Longrightarrow> {x..+b} = {x .. x + of_nat b - 1}" 203 unfolding intvl_def 204 apply rule 205 apply clarsimp 206 apply (subgoal_tac "of_nat k \<le> (of_nat (b - 1) :: 'a word)") 207 apply (intro conjI) 208 apply (erule word_random) 209 apply simp 210 apply (subst field_simps [symmetric], rule word_plus_mono_right) 211 apply simp 212 apply assumption 213 apply (subst Word_Lemmas.of_nat_mono_maybe_le [symmetric]) 214 apply simp 215 apply simp 216 apply simp 217 apply clarsimp 218 apply (rule_tac x = "unat (xa - x)" in exI) 219 apply simp 220 apply (simp add: unat_sub) 221 apply (rule nat_diff_less) 222 apply (subst (asm) word_le_nat_alt, erule order_le_less_trans) 223 apply (subst add_diff_eq[symmetric], subst unat_plus_if') 224 apply (simp add: no_olen_add_nat) 225 apply (simp add: le_eq_less_or_eq) 226 apply (erule disjE) 227 apply (subst unat_minus_one) 228 apply (erule (1) of_nat_neq_0) 229 apply (simp add: unat_of_nat) 230 apply (erule ssubst, rule unat_lt2p) 231 apply (simp add: word_le_nat_alt) 232 done 233 234lemma intvl_aligned_top: 235 fixes x :: "'a::len word" 236 assumes al1: "is_aligned x n" 237 and al2: "is_aligned p bits" 238 and nb: "n \<le> bits" 239 and offn: "off < 2 ^ n" 240 and wb: "bits < len_of TYPE('a)" 241 shows "(x \<in> {p ..+ 2 ^ bits - off}) = (x \<in> {p ..+ 2 ^ bits})" 242proof (rule iffI) 243 assume "x \<in> {p..+2 ^ bits - off}" 244 thus "x \<in> {p..+2 ^ bits}" by (rule intvl_mem_weaken) 245next 246 assume asm: "x \<in> {p..+2 ^ bits}" 247 248 show "x \<in> {p..+2 ^ bits - off}" 249 proof (cases "n = 0") 250 case True 251 with offn asm show ?thesis by simp 252 next 253 case False 254 255 from asm have "x \<in> {p .. p + 2 ^ bits - 1}" 256 by (simp add: upto_intvl_eq [OF al2]) 257 then obtain q where xp: "x = p + of_nat (q * 2 ^ n)" and qb: "q < 2 ^ (bits - n)" using False nb 258 by (fastforce dest!: is_aligned_diff[OF al1 al2 wb,simplified field_simps]) 259 260 have "q * 2 ^ n < 2 ^ bits - off" 261 proof - 262 show ?thesis using offn qb nb 263 apply (simp add: less_diff_conv) 264 apply (erule (1) nat_add_offset_less) 265 apply arith 266 done 267 qed 268 269 with xp show ?thesis 270 apply - 271 apply (erule ssubst) 272 apply (erule intvlI) 273 done 274 qed 275qed 276 277lemma intvl_nowrap: 278 fixes x :: "'a::len word" 279 shows "\<lbrakk>y \<noteq> 0; unat y + z \<le> 2 ^ len_of TYPE('a)\<rbrakk> \<Longrightarrow> x \<notin> {x + y ..+ z}" 280 apply clarsimp 281 apply (drule intvlD) 282 apply clarsimp 283 apply (simp add: unat_arith_simps) 284 apply (simp split: if_split_asm) 285 apply (simp add: unat_of_nat) 286 done 287 288lemma heap_update_list_update: 289 fixes v :: word8 290 shows "x \<noteq> y \<Longrightarrow> heap_update_list s xs (hp(y := v)) x = heap_update_list s xs hp x" 291 apply (induct xs rule: rev_induct) 292 apply simp 293 apply (simp add: heap_update_list_append cong: if_cong) 294 done 295 296(* FIXME: generalise *) 297lemma heap_update_list_append2: 298 "length xs + length ys < 2 ^ word_bits \<Longrightarrow> 299 heap_update_list s (xs @ ys) hp 300 = heap_update_list s xs (heap_update_list (s + of_nat (length xs)) ys hp)" 301proof (induct xs arbitrary: hp s) 302 case Nil 303 show ?case by simp 304next 305 case (Cons v' vs') 306 307 have "(1 :: addr) + of_nat (length vs') = of_nat (length (v' # vs'))" 308 by simp 309 also have "\<dots> \<noteq> 0" using Cons.prems 310 apply - 311 apply (rule of_nat_neq_0) 312 apply simp 313 apply (simp add: word_bits_conv) 314 done 315 finally have neq0: "(1 :: addr) + of_nat (length vs') \<noteq> 0" . 316 317 have "(1 :: addr) + of_nat (length vs') = of_nat (length (v' # vs'))" 318 by simp 319 also have "unat \<dots> + length ys < 2 ^ word_bits" using Cons.prems 320 apply (subst unat_of_nat) 321 apply (simp add: word_bits_conv) 322 done 323 finally have lt: "unat ((1 :: addr) + of_nat (length vs')) + length ys < 2 ^ word_bits" . 324 325 from Cons.prems have "length vs' + length ys < 2 ^ word_bits" by simp 326 thus ?case 327 apply simp 328 apply (subst Cons.hyps, assumption) 329 apply (rule arg_cong [where f = "heap_update_list (s + 1) vs'"]) 330 apply (rule ext) 331 apply (case_tac "x = s") 332 apply simp 333 apply (subst heap_update_nmem_same) 334 apply (subst add.assoc) 335 apply (rule intvl_nowrap[OF neq0 order_less_imp_le 336 [OF lt[unfolded word_bits_def]]]) 337 apply simp 338 apply (clarsimp simp: heap_update_list_update field_simps) 339 done 340qed 341 342lemma heap_update_word8: 343 "heap_update p (v :: word8) hp = hp(ptr_val p := v)" 344 unfolding heap_update_def by (simp add: to_bytes_word8) 345 346lemma index_foldr_update2: 347 "\<lbrakk> n \<le> i; i < CARD('b::finite) \<rbrakk> \<Longrightarrow> index (foldr (\<lambda>n arr. Arrays.update arr n m) [0..<n] (x :: ('a,'b) array)) i = index x i" 348 apply (induct n arbitrary: x) 349 apply simp 350 apply simp 351 done 352 353lemma index_foldr_update: 354 "\<lbrakk> i < n; n \<le> CARD('b::finite) \<rbrakk> \<Longrightarrow> index (foldr (\<lambda>n arr. Arrays.update arr n m) [0..<n] (x :: ('a,'b) array)) i = m" 355 apply (induct n arbitrary: x) 356 apply simp 357 apply simp 358 apply (erule less_SucE) 359 apply simp 360 apply simp 361 apply (subst index_foldr_update2) 362 apply simp 363 apply simp 364 apply simp 365 done 366 367lemma intvl_disjoint1: 368 fixes a :: "'a :: len word" 369 assumes abc: "a + of_nat b \<le> c" 370 and alb: "a \<le> a + of_nat b" 371 and cld: "c \<le> c + of_nat d" 372 and blt: "b < 2 ^ len_of TYPE('a)" 373 and dlt: "d < 2 ^ len_of TYPE('a)" 374 shows "{a..+b} \<inter> {c..+d} = {}" 375proof (rule disjointI, rule notI) 376 fix x y 377 assume x: "x \<in> {a..+b}" and y: "y \<in> {c..+d}" and xy: "x = y" 378 379 from x obtain kx where "x = a + of_nat kx" and kx: "kx < b" 380 by (clarsimp dest!: intvlD) 381 382 moreover from y obtain ky where "y = c + of_nat ky" and ky: "ky < d" 383 by (clarsimp dest!: intvlD) 384 385 ultimately have ac: "a + of_nat kx = c + of_nat ky" using xy by simp 386 387 have "of_nat kx < (of_nat b :: 'a word)" using blt kx 388 by (rule of_nat_mono_maybe) 389 hence "a + of_nat kx < a + of_nat b" using alb 390 by (rule word_plus_strict_mono_right) 391 392 also have "\<dots> \<le> c" by (rule abc) 393 also have "\<dots> \<le> c + of_nat ky" using cld dlt ky 394 by - (rule word_random [OF _ iffD1 [OF Word_Lemmas.of_nat_mono_maybe_le]], simp+ ) 395 finally show False using ac by simp 396qed 397 398lemma intvl_disjoint2: 399 fixes a :: "'a :: len word" 400 assumes abc: "a + of_nat b \<le> c" 401 and alb: "a \<le> a + of_nat b" 402 and cld: "c \<le> c + of_nat d" 403 and blt: "b < 2 ^ len_of TYPE('a)" 404 and dlt: "d < 2 ^ len_of TYPE('a)" 405 shows "{c..+d} \<inter> {a..+b} = {}" 406 using abc alb cld blt dlt 407 by (subst Int_commute, rule intvl_disjoint1) 408 409 410lemma intvl_off_disj: 411 fixes x :: addr 412 assumes ylt: "y \<le> off" 413 and zoff: "z + off < 2 ^ word_bits" 414 shows "{x ..+ y} \<inter> {x + of_nat off ..+ z} = {}" 415 using ylt zoff 416 apply (cases "off = 0") 417 apply simp 418 apply (rule contrapos_pp [OF TrueI]) 419 apply (drule intvl_inter) 420 apply (erule disjE) 421 apply (cut_tac intvl_nowrap [where x = x and y = "of_nat off :: addr" and z = z]) 422 apply simp 423 apply (rule of_nat_neq_0) 424 apply simp 425 apply (unfold word_bits_len_of) 426 apply simp 427 apply (simp add: unat_of_nat word_bits_conv) 428 apply (drule intvlD) 429 apply clarsimp 430 apply (drule (1) order_less_le_trans) 431 apply (drule unat_cong) 432 apply (simp add: unat_of_nat word_bits_conv) 433 done 434 435 436lemma list_map_comono: 437 assumes s: "list_map m \<subseteq>\<^sub>m list_map n" 438 shows "m \<le> n" 439 using s 440proof (induct m arbitrary: n rule: rev_induct) 441 case Nil thus ?case unfolding list_map_def by simp 442next 443 case (snoc x xs) 444 445 from snoc.prems have 446 sm: "[length xs \<mapsto> x] ++ list_map xs \<subseteq>\<^sub>m list_map n" 447 unfolding list_map_def by simp 448 449 hence xsn: "xs \<le> n" 450 by (rule snoc.hyps [OF map_add_le_mapE]) 451 452 have "list_map n (length xs) = Some x" using sm 453 by (simp add: map_le_def list_map_def merge_dom2 set_zip) 454 455 hence "length xs < length n" and "x = n ! length xs" 456 by (auto simp add: list_map_eq split: if_split_asm) 457 458 thus "xs @ [x] \<le> n" using xsn 459 by (simp add: append_one_prefix less_eq_list_def) 460qed 461 462lemma typ_slice_t_self: 463 "td \<in> fst ` set (typ_slice_t td m)" 464 apply (cases td) 465 apply (simp split: if_split) 466 done 467 468lemma drop_heap_list_le2: 469 "heap_list h n (x + of_nat k) 470 = drop k (heap_list h (n + k) x)" 471 by (simp add: drop_heap_list_le) 472 473lemma index_fold_update: 474 "\<lbrakk> distinct xs; set xs \<subseteq> {..< card (UNIV :: 'b set)}; n < card (UNIV :: 'b set) \<rbrakk> \<Longrightarrow> 475 index (foldr (\<lambda>n (arr :: 'a['b :: finite]). Arrays.update arr n (f n (index arr n))) xs v) n 476 = (if n \<in> set xs then f n (index v n) else index v n)" 477 apply (induct xs) 478 apply simp 479 apply (rename_tac x xs) 480 apply (case_tac "x = n"; simp) 481 done 482 483lemma heap_update_list_id: 484 "heap_list hp n ptr = xs \<Longrightarrow> heap_update_list ptr xs hp = hp" 485 apply (induct xs arbitrary: ptr n) 486 apply simp 487 apply simp 488 apply (case_tac n, simp_all) 489 apply (clarsimp simp add: fun_upd_idem) 490 done 491 492lemma size_td_list_map2: "\<And>f adjs. \<lbrakk> \<And>a. size_td_pair (f a) = size_td_pair a \<rbrakk> 493 \<Longrightarrow> size_td_list (map f adjs) = size_td_list adjs" 494 by (induct_tac adjs, simp_all) 495 496lemma hrs_mem_update_cong: 497 "\<lbrakk> \<And>x. f x = f' x \<rbrakk> \<Longrightarrow> hrs_mem_update f = hrs_mem_update f'" 498 by (simp add: hrs_mem_update_def) 499 500lemma Guard_no_cong: 501 "\<lbrakk> A=A'; c=c' \<rbrakk> \<Longrightarrow> Guard A P c = Guard A' P c'" 502 by simp 503 504lemma heap_update_list_concat_fold: 505 assumes "ptr' = ptr + of_nat (length ys)" 506 shows "heap_update_list ptr' xs (heap_update_list ptr ys s) 507 = heap_update_list ptr (ys @ xs) s" 508 unfolding assms 509 apply (induct ys arbitrary: ptr s) 510 apply simp 511 apply simp 512 apply (elim meta_allE) 513 apply (erule trans[rotated]) 514 apply (simp add: field_simps) 515 done 516 517lemma heap_update_list_concat_fold_hrs_mem: 518 "ptr' = ptr + of_nat (length ys) \<Longrightarrow> 519 hrs_mem_update (heap_update_list ptr' xs) 520 (hrs_mem_update (heap_update_list ptr ys) s) 521 = hrs_mem_update (heap_update_list ptr (ys @ xs)) s" 522 by (simp add: hrs_mem_update_def split_def 523 heap_update_list_concat_fold) 524 525lemmas heap_update_list_concat_unfold 526 = heap_update_list_concat_fold[OF refl, symmetric] 527 528lemma coerce_heap_update_to_heap_updates: 529 assumes n: "n = chunk * m" and len: "length xs = n" 530 shows "heap_update_list x xs 531 = (\<lambda>s. foldl (\<lambda>s n. heap_update_list (x + (of_nat n * of_nat chunk)) 532 (take chunk (drop (n * chunk) xs)) s) 533 s [0 ..< m])" 534 using len[simplified n] 535 apply (induct m arbitrary: x xs) 536 apply (rule ext, simp) 537 apply (rule ext) 538 apply (simp only: upt_conv_Cons map_Suc_upt[symmetric]) 539 apply (subgoal_tac "\<exists>ys zs. length ys = chunk \<and> xs = ys @ zs") 540 apply (clarsimp simp: heap_update_list_concat_unfold foldl_map 541 field_simps) 542 apply (rule_tac x="take chunk xs" in exI) 543 apply (rule_tac x="drop chunk xs" in exI) 544 apply simp 545 done 546 547lemma update_ti_list_array': 548 "\<lbrakk> update_ti_list_t (map f [0 ..< n]) xs v = y; 549 \<forall>n. size_td_pair (f n) = v3; length xs = v3 * n; 550 \<forall>m xs v'. length xs = v3 \<and> m < n \<longrightarrow> 551 update_ti_pair_t (f m) xs v' = Arrays.update v' m (update_ti_t (g m) xs (index v' m)) \<rbrakk> 552 \<Longrightarrow> y = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (g n) (take v3 (drop (v3 * n) xs)) (index arr n))) [0 ..< n] v" 553 apply (subgoal_tac "\<forall>ys. size_td_list (map f ys) = v3 * length ys") 554 prefer 2 555 apply (rule allI, induct_tac ys, simp+) 556 apply (induct n arbitrary: xs y v) 557 apply simp 558 apply (simp add: access_ti_append) 559 apply (elim meta_allE, drule(1) meta_mp) 560 apply simp 561 apply (rule foldr_cong, (rule refl)+) 562 apply (simp add: take_drop) 563 apply (subst min.absorb1) 564 apply (fold mult_Suc_right, rule mult_le_mono2) 565 apply simp 566 apply simp 567 done 568 569lemma update_ti_list_array: 570 "\<lbrakk> update_ti_list_t (map f [0 ..< n]) xs v = (y :: 'a['b :: finite]); 571 \<forall>n. size_td_pair (f n) = v3; length xs = v3 * n; 572 \<forall>m xs v'. length xs = v3 \<and> m < n \<longrightarrow> 573 update_ti_pair_t (f m) xs v' = Arrays.update v' m (update_ti_t (g m) xs (index v' m)); 574 n \<le> card (UNIV :: 'b set) \<rbrakk> 575 \<Longrightarrow> \<forall>m < n. update_ti_t (g m) (take v3 (drop (v3 * m) xs)) (index v m) = index y m" 576 apply (subst update_ti_list_array'[where y=y], assumption+) 577 apply clarsimp 578 apply (subst index_fold_update) 579 apply clarsimp+ 580 done 581 582lemma access_in_array: 583 fixes y :: "('a :: c_type)['b :: finite]" 584 assumes assms: "h_val hp x = y" 585 "n < card (UNIV :: 'b set)" 586 and subst: "\<forall>xs v. length xs = size_of TYPE('a) 587 \<longrightarrow> update_ti_t (typ_info_t TYPE('a)) xs v = f xs" 588 shows "h_val hp 589 (Ptr (ptr_val x + of_nat (n * size_of TYPE('a)))) = index y n" 590 using assms 591 apply (simp add: h_val_def drop_heap_list_le2 del: of_nat_mult) 592 apply (subst take_heap_list_le[symmetric, where n="card (UNIV :: 'b set) * size_of TYPE ('a)"]) 593 apply (fold mult_Suc, rule mult_le_mono1) 594 apply simp 595 apply (simp add: from_bytes_def typ_info_array') 596 apply (drule update_ti_list_array, simp+) 597 apply (simp add: size_of_def) 598 apply (clarsimp simp: update_ti_s_adjust_ti) 599 apply (rule refl) 600 apply simp 601 apply (drule spec, drule(1) mp) 602 apply (simp add: size_of_def ac_simps drop_take) 603 apply (subgoal_tac "length v = size_of TYPE('a)" for v) 604 apply (subst subst, assumption) 605 apply (subst(asm) subst, assumption) 606 apply simp 607 apply (simp add: size_of_def) 608 apply (subst le_diff_conv2) 609 apply simp 610 apply (fold mult_Suc, rule mult_le_mono1) 611 apply simp 612 done 613 614lemma access_ti_list_array: 615 "\<lbrakk> \<forall>n. size_td_pair (f n) = v3; length xs = v3 * n; 616 \<forall>m. m < n \<and> v3 \<le> length (drop (v3 * m) xs) 617 \<longrightarrow> access_ti_pair (f m) (FCP g) (take v3 (drop (v3 * m) xs)) = (h m) 618 \<rbrakk> \<Longrightarrow> 619 access_ti_list (map f [0 ..< n]) (FCP g) xs 620 = foldl (@) [] (map h [0 ..< n])" 621 apply (subgoal_tac "\<forall>ys. size_td_list (map f ys) = v3 * length ys") 622 prefer 2 623 apply (rule allI, induct_tac ys, simp+) 624 apply (induct n arbitrary: xs) 625 apply simp 626 apply (simp add: access_ti_append) 627 apply (erule_tac x="take (v3 * n) xs" in meta_allE) 628 apply simp 629 apply (frule spec, drule mp, rule conjI, rule lessI) 630 apply simp 631 apply simp 632 apply (erule meta_mp) 633 apply (auto simp add: drop_take) 634 done 635 636lemma take_drop_foldl_concat: 637 "\<lbrakk> \<And>y. y < m \<Longrightarrow> length (f y) = n; x < m \<rbrakk> 638 \<Longrightarrow> take n (drop (x * n) (foldl (@) [] (map f [0 ..< m]))) = f x" 639 apply (subst split_upt_on_n, assumption) 640 apply (simp only: foldl_concat_concat map_append) 641 apply (subst drop_append_miracle) 642 apply (induct x, simp_all)[1] 643 apply simp 644 done 645 646definition 647 array_ptr_index :: "(('a :: c_type)['b :: finite]) ptr \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> 'a ptr" 648where 649 "array_ptr_index p coerce n = CTypesDefs.ptr_add (ptr_coerce p) 650 (if coerce \<and> n \<ge> CARD ('b) then 0 else of_nat n)" 651 652lemmas array_ptr_index_simps 653 = array_ptr_index_def[where coerce=False, simplified] 654 array_ptr_index_def[where coerce=True, simplified] 655 656lemma heap_update_Array: 657 "heap_update (p ::('a::packed_type['b::finite]) ptr) arr 658 = (\<lambda>s. foldl (\<lambda>s n. heap_update (array_ptr_index p False n) 659 (Arrays.index arr n) s) s [0 ..< card (UNIV :: 'b set)])" 660 apply (rule ext, simp add: heap_update_def) 661 apply (subst coerce_heap_update_to_heap_updates 662 [OF _ refl, where chunk="size_of TYPE('a)" and m="card (UNIV :: 'b set)"]) 663 apply simp 664 apply (rule foldl_cong[OF refl refl]) 665 apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def) 666 apply (rule_tac f="\<lambda>xs. heap_update_list p xs s" for p s in arg_cong) 667 apply (simp add: to_bytes_def size_of_def 668 packed_type_access_ti) 669 apply (simp add: typ_info_array') 670 apply (subst fcp_eta[symmetric], subst access_ti_list_array) 671 apply simp 672 apply simp 673 apply (simp add: packed_type_access_ti size_of_def) 674 apply fastforce 675 apply (rule take_drop_foldl_concat) 676 apply (simp add: size_of_def) 677 apply simp 678 done 679 680lemma from_bytes_Array_element: 681 fixes p :: "('a::mem_type['b::finite]) ptr" 682 assumes less: "of_nat n < card (UNIV :: 'b set)" 683 assumes len: "length bs = size_of TYPE('a) * CARD('b)" 684 shows 685 "index (from_bytes bs :: 'a['b]) n 686 = from_bytes (take (size_of TYPE('a)) (drop (n * size_of TYPE('a)) bs))" 687 using less 688 apply (simp add: from_bytes_def size_of_def typ_info_array') 689 apply (subst update_ti_list_array'[OF refl]) 690 apply simp 691 apply (simp add: len size_of_def) 692 apply (clarsimp simp: update_ti_s_adjust_ti) 693 apply (rule refl) 694 apply (simp add: split_upt_on_n[OF less]) 695 apply (rule trans, rule foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"]) 696 apply simp+ 697 apply (subst foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"]) 698 apply simp 699 apply (simp add: mult.commute) 700 apply (frule Suc_leI) 701 apply (drule_tac k="size_of TYPE('a)" in mult_le_mono2) 702 apply (rule upd_rf) 703 apply (simp add: size_of_def len mult.commute) 704 done 705 706lemma heap_access_Array_element': 707 fixes p :: "('a::mem_type['b::finite]) ptr" 708 assumes less: "of_nat n < card (UNIV :: 'b set)" 709 shows 710 "index (h_val hp p) n 711 = h_val hp (array_ptr_index p False n)" 712 using less 713 apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def h_val_def) 714 apply (simp add: from_bytes_Array_element) 715 apply (simp add: drop_heap_list_le take_heap_list_le) 716 apply (subst take_heap_list_le) 717 apply (simp add: le_diff_conv2) 718 apply (drule Suc_leI) 719 apply (drule_tac k="size_of TYPE('a)" in mult_le_mono2) 720 apply (simp add: mult.commute) 721 apply simp 722 done 723 724lemmas heap_access_Array_element 725 = heap_access_Array_element'[simplified array_ptr_index_simps] 726 727lemma heap_update_id: 728 "h_val hp ptr = (v :: 'a :: packed_type) 729 \<Longrightarrow> heap_update ptr v hp = hp" 730 apply (simp add: h_val_def heap_update_def) 731 apply (rule heap_update_list_id[where n="size_of TYPE('a)"]) 732 apply clarsimp 733 apply (simp add: from_bytes_def to_bytes_def update_ti_t_def 734 size_of_def field_access_update_same 735 td_fafu_idem) 736 done 737 738lemma fold_cong': 739 "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs =simp=> f x = g x) 740 \<Longrightarrow> fold f xs a = fold g ys b" 741 unfolding simp_implies_def 742 by (metis fold_cong) 743 744lemma intvl_empty2: 745 "({p ..+ n} = {}) = (n = 0)" 746 by (auto simp add: intvl_def) 747 748lemma heap_update_list_commute: 749 "{p ..+ length xs} \<inter> {q ..+ length ys} = {} 750 \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) 751 = heap_update_list q ys (heap_update_list p xs hp)" 752 apply (cases "length xs < addr_card") 753 apply (cases "length ys < addr_card") 754 apply (rule ext, simp add: heap_update_list_value) 755 apply blast 756 apply (simp_all add: addr_card intvl_overflow intvl_empty2) 757 done 758 759lemma heap_update_commute: 760 "\<lbrakk> {ptr_val p ..+ size_of TYPE('a)} \<inter> {ptr_val q ..+ size_of TYPE('b)} = {}; 761 wf_fd (typ_info_t TYPE('a)); wf_fd (typ_info_t TYPE('b)) \<rbrakk> 762 \<Longrightarrow> heap_update p v (heap_update q (u :: 'b :: c_type) h) 763 = heap_update q u (heap_update p (v :: 'a :: c_type) h)" 764 apply (simp add: heap_update_def) 765 apply (simp add: heap_update_list_commute heap_list_update_disjoint_same 766 to_bytes_def length_fa_ti size_of_def Int_commute) 767 done 768 769lemma heap_update_Array_update: 770 assumes n: "n < CARD('b :: finite)" 771 assumes size: "CARD('b) * size_of TYPE('a :: packed_type) < 2 ^ addr_bitsize" 772 shows "heap_update p (Arrays.update (arr :: 'a['b]) n v) hp 773 = heap_update (array_ptr_index p False n) v (heap_update p arr hp)" 774proof - 775 776 have P: "\<And>x k. \<lbrakk> x < CARD('b); k < size_of TYPE('a) \<rbrakk> 777 \<Longrightarrow> unat (of_nat x * of_nat (size_of TYPE('a)) + (of_nat k :: addr)) 778 = x * size_of TYPE('a) + k" 779 using size 780 apply (case_tac "size_of TYPE('a)", simp_all) 781 apply (case_tac "CARD('b)", simp_all) 782 apply (subst unat_add_lem[THEN iffD1]) 783 apply (simp add: unat_word_ariths unat_of_nat less_Suc_eq_le) 784 apply (subgoal_tac "Suc x * size_of TYPE('a) < 2 ^ addr_bitsize", simp_all) 785 apply (erule order_le_less_trans[rotated], simp add: add_mono) 786 apply (subst unat_mult_lem[THEN iffD1]) 787 apply (simp add: unat_of_nat unat_add_lem[THEN iffD1]) 788 apply (rule order_less_le_trans, erule order_le_less_trans[rotated], 789 rule add_mono, simp+) 790 apply (simp add: less_Suc_eq_le trans_le_add2) 791 apply simp 792 apply (simp add: unat_of_nat unat_add_lem[THEN iffD1]) 793 done 794 795 let ?key_upd = "heap_update (array_ptr_index p False n) v" 796 note commute = fold_commute_apply[where h="?key_upd" 797 and xs="[Suc n ..< CARD('b)]", where g=f' and f=f' for f'] 798 799 show ?thesis using n 800 apply (simp add: heap_update_Array split_upt_on_n[OF n] 801 foldl_conv_fold) 802 apply (subst commute) 803 apply (simp_all add: packed_heap_update_collapse 804 cong: fold_cong') 805 apply (rule ext, simp) 806 apply (rule heap_update_commute, simp_all add: ptr_add_def) 807 apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def intvl_def Suc_le_eq) 808 apply (rule set_eqI, clarsimp) 809 apply (drule word_unat.Rep_inject[THEN iffD2]) 810 apply (clarsimp simp: P nat_eq_add_iff1) 811 apply (case_tac x, simp_all add: less_Suc_eq_le Suc_diff_le) 812 done 813qed 814 815lemma heap_update_id_Array: 816 fixes arr :: "('a :: packed_type)['b :: finite]" 817 shows "arr = h_val hp p 818 \<Longrightarrow> heap_update p arr hp = hp" 819 apply (simp add: heap_update_Array) 820 apply (rule foldl_does_nothing[where s=hp]) 821 apply (simp add: heap_access_Array_element' heap_update_id) 822 done 823 824lemma heap_update_Array_element'': 825 fixes p' :: "(('a :: packed_type)['b::finite]) ptr" 826 fixes p :: "('a :: packed_type) ptr" 827 fixes hp w 828 assumes p: "p = array_ptr_index p' False n" 829 assumes n: "n < CARD('b)" 830 assumes size: "CARD('b) * size_of TYPE('a) < 2 ^ addr_bitsize" 831 shows "heap_update p' (Arrays.update (h_val hp p') n w) hp 832 = heap_update p w hp" 833 apply (subst heap_update_Array_update[OF n size]) 834 apply (simp add: heap_update_id_Array p) 835 done 836 837lemmas heap_update_Array_element' 838 = heap_update_Array_element''[simplified array_ptr_index_simps] 839 840lemma array_count_size: 841 "CARD('b :: array_max_count) * size_of TYPE('a :: array_outer_max_size) < 2 ^ addr_bitsize" 842 using array_outer_max_size_ax[where 'a='a] array_max_count_ax[where 'a='b] 843 apply (clarsimp dest!: nat_le_Suc_less_imp) 844 apply (drule(1) mult_mono, simp+) 845 done 846 847lemmas heap_update_Array_element 848 = heap_update_Array_element'[OF refl _ array_count_size] 849 850lemma typ_slice_list_cut: 851 "\<lbrakk> (\<forall>x \<in> set xs. size_td (dt_fst x) = m); m \<noteq> 0; n < (length xs * m) \<rbrakk> 852 \<Longrightarrow> typ_slice_list xs n = 853 typ_slice_pair (xs ! (n div m)) (n mod m)" 854 apply (induct xs arbitrary: n, simp_all) 855 apply (intro conjI impI) 856 apply simp 857 apply (subgoal_tac "\<exists>n'. n = n' + m") 858 apply clarsimp 859 apply (rule_tac x="n - m" in exI) 860 apply simp 861 done 862 863lemma typ_slice_t_array: 864 "\<lbrakk> n < CARD('b); y < size_of TYPE('a) \<rbrakk> 865 \<Longrightarrow> typ_slice_t (export_uinfo (typ_info_t TYPE('a))) y \<le> 866 typ_slice_t (export_uinfo (array_tag TYPE('a['b :: finite]))) 867 (y + size_of TYPE('a :: mem_type) * n)" 868 apply (simp add: array_tag_def array_tag_n_eq 869 split del: if_split) 870 apply (rule disjI2) 871 apply (subgoal_tac "y + (size_of TYPE('a) * n) < CARD('b) * size_of TYPE('a)") 872 apply (simp add: typ_slice_list_cut[where m="size_of TYPE('a)"] 873 map_td_list_map o_def size_of_def 874 sz_nzero[unfolded size_of_def]) 875 apply (simp add: export_uinfo_def[symmetric]) 876 apply (rule_tac y="Suc n * size_of TYPE('a)" in order_less_le_trans) 877 apply (simp add: size_of_def) 878 apply (simp only: size_of_def mult_le_mono1) 879 done 880 881lemma h_t_valid_Array_element': 882 "\<lbrakk> htd \<Turnstile>\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); coerce \<or> n < CARD('b) \<rbrakk> 883 \<Longrightarrow> htd \<Turnstile>\<^sub>t array_ptr_index p coerce n" 884 apply (clarsimp simp only: h_t_valid_def valid_footprint_def Let_def 885 c_guard_def c_null_guard_def) 886 apply (subgoal_tac "\<exists>offs. array_ptr_index p coerce n = ptr_add (ptr_coerce p) (of_nat offs) 887 \<and> offs < CARD ('b)") 888 apply (clarsimp simp: size_td_array size_of_def typ_uinfo_t_def 889 typ_info_array array_tag_def) 890 apply (intro conjI) 891 apply (clarsimp simp: CTypesDefs.ptr_add_def 892 field_simps) 893 apply (drule_tac x="offs * size_of TYPE('a) + y" in spec) 894 apply (drule mp) 895 apply (rule_tac y="Suc offs * size_of TYPE('a)" in order_less_le_trans) 896 apply (simp add: size_of_def) 897 apply (simp only: size_of_def mult_le_mono1) 898 apply (clarsimp simp: field_simps) 899 apply (erule map_le_trans[rotated]) 900 apply (rule list_map_mono) 901 apply (subst mult.commute, rule typ_slice_t_array[unfolded array_tag_def]) 902 apply assumption 903 apply (simp add: size_of_def) 904 apply (simp add: ptr_aligned_def align_of_def align_td_array 905 array_ptr_index_def 906 CTypesDefs.ptr_add_def unat_word_ariths unat_of_nat) 907 using align_size_of[where 'a='a] align[where 'a='a] 908 apply (simp add: align_of_def size_of_def addr_card_def card_word) 909 apply (simp add: dvd_mod) 910 apply (thin_tac "\<forall>x. P x" for P) 911 apply (clarsimp simp: intvl_def) 912 apply (drule_tac x="offs * size_of TYPE('a) + k" in spec) 913 apply (drule mp) 914 apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def field_simps) 915 apply (erule notE) 916 apply (rule_tac y="Suc offs * size_of TYPE('a)" in order_less_le_trans) 917 apply (simp add: size_of_def) 918 apply (simp only: size_of_def mult_le_mono1) 919 apply (auto simp add: array_ptr_index_def intro: exI[where x=0]) 920 done 921 922lemma h_t_valid_Array_element: 923 "\<lbrakk> htd \<Turnstile>\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); 0 \<le> n; n < int CARD('b) \<rbrakk> 924 \<Longrightarrow> htd \<Turnstile>\<^sub>t ((ptr_coerce p :: 'a ptr) +\<^sub>p n)" 925 apply (drule_tac n="nat n" and coerce=False in h_t_valid_Array_element') 926 apply simp 927 apply (simp add: array_ptr_index_def) 928 done 929 930lemma ptr_safe_Array_element: 931 "\<lbrakk> ptr_safe (p :: (('a :: mem_type)['b :: finite]) ptr) htd; coerce \<or> n < CARD('b) \<rbrakk> 932 \<Longrightarrow> ptr_safe (array_ptr_index p coerce n) htd" 933 apply (simp add: ptr_safe_def) 934 apply (erule order_trans[rotated]) 935 apply (subgoal_tac "\<exists>offs. array_ptr_index p coerce n = ptr_add (ptr_coerce p) (of_nat offs) 936 \<and> offs < CARD ('b)") 937 prefer 2 938 apply (auto simp: array_ptr_index_def intro: exI[where x=0])[1] 939 apply (clarsimp simp: s_footprint_def s_footprint_untyped_def 940 CTypesDefs.ptr_add_def 941 size_td_array size_of_def) 942 apply (rule_tac x="offs * size_of TYPE('a) + x" in exI) 943 apply (simp add: size_of_def) 944 apply (rule conjI) 945 apply (rule_tac y="Suc offs * size_of TYPE('a)" in order_less_le_trans) 946 apply (simp add: size_of_def) 947 apply (simp only: size_of_def) 948 apply (rule mult_le_mono1) 949 apply simp 950 apply (thin_tac "coerce \<or> P" for P) 951 apply (elim disjE exE conjE, simp_all add: typ_uinfo_t_def) 952 apply (erule order_less_le_trans) 953 apply (rule prefix_length_le) 954 apply (rule order_trans, erule typ_slice_t_array) 955 apply (simp add: size_of_def) 956 apply (simp add: size_of_def field_simps typ_info_array) 957 done 958 959lemma from_bytes_eq: 960 "from_bytes [x] = x" 961 apply (clarsimp simp:from_bytes_def update_ti_t_def typ_info_word) 962 apply (simp add:word_rcat_def) 963 apply (simp add:bin_rcat_def) 964 by (metis len8 word_of_int_uint word_ubin.Abs_norm) 965 966lemma bytes_disjoint:"(x::('a::c_type) ptr) \<noteq> y \<Longrightarrow> {ptr_val x + a ..+ 1} \<inter> {ptr_val y + a ..+ 1} = {}" 967 by (clarsimp simp:intvl_def) 968 969lemma byte_ptrs_disjoint:"(x::('a::c_type) ptr) \<noteq> y \<Longrightarrow> \<forall>i < of_nat (size_of TYPE('a)). ptr_val x + i \<noteq> ptr_val y + i" 970 by force 971 972lemma le_step:"\<lbrakk>(x::('a::len) word) < y + 1; x \<noteq> y\<rbrakk> \<Longrightarrow> x < y" 973 by (metis less_x_plus_1 max_word_max order_less_le) 974 975lemma ptr_add_disjoint: 976 "\<lbrakk> ptr_val y \<notin> {ptr_val x ..+ size_of TYPE('a)}; 977 ptr_val (x::('a::c_type) ptr) < ptr_val (y::('b::c_type) ptr); 978 a < of_nat (size_of TYPE('a)) \<rbrakk> \<Longrightarrow> 979 ptr_val x + a < ptr_val y" 980 apply (erule swap) 981 apply (rule intvl_inter_le [where k=0 and ka="unat (ptr_val y - ptr_val x)"]) 982 apply clarsimp 983 apply (metis (hide_lams, mono_tags) add_diff_cancel2 add_diff_inverse diff_add_cancel 984 trans_less_add1 unat_less_helper word_le_less_eq word_less_add_right 985 word_of_nat_less word_unat.Rep_inverse) 986 apply simp 987 done 988 989lemma ptr_add_disjoint2: 990 "\<lbrakk> ptr_val x \<notin> {ptr_val y ..+ size_of TYPE('a)}; 991 ptr_val (y::('b::c_type) ptr) < ptr_val (x::('a::c_type) ptr); 992 a < of_nat (size_of TYPE('a)) \<rbrakk> \<Longrightarrow> 993 ptr_val y + a < ptr_val x" 994 apply (erule swap) 995 apply (rule intvl_inter_le[where k=0 and ka="unat (ptr_val x - ptr_val y)"]) 996 apply clarsimp 997 apply (metis (no_types, hide_lams) add.commute less_imp_le less_le_trans not_le unat_less_helper 998 word_diff_ls'(4)) 999 apply simp 1000 done 1001 1002lemma ptr_aligned_is_aligned:"\<lbrakk>ptr_aligned (x::('a::c_type) ptr); align_of TYPE('a) = 2 ^ n\<rbrakk> \<Longrightarrow> is_aligned (ptr_val x) n" 1003 by (clarsimp simp: ptr_aligned_def is_aligned_def) 1004 1005lemma intvl_no_overflow: 1006 assumes no_overflow: "unat a + b < 2 ^ len_of TYPE('a::len)" 1007 shows "(x \<in> {(a :: 'a word) ..+ b}) = (a \<le> x \<and> x < (a + of_nat b))" 1008proof - 1009 obtain "sk" :: "'a word \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> nat" 1010 where f1: "\<And>x y z. x \<notin> {y..+z} \<or> x = y + of_nat (sk x y z) \<and> sk x y z < z" 1011 using [[metis_new_skolem]] by (metis intvlD) 1012 1013 have f2: "\<And>x. a + x < a + of_nat b \<or> \<not> x < of_nat b" 1014 using no_overflow 1015 by (metis PackedTypes.of_nat_mono_maybe_le add_lessD1 le_add1 1016 add.commute olen_add_eqv unat_of_nat_eq word_arith_nat_add 1017 word_plus_strict_mono_right) 1018 1019 have f3: "\<forall>x y. y \<notin> {x..+b} \<or> of_nat (sk y x b) < (of_nat b :: 'a word)" 1020 using no_overflow f1 1021 by (metis add_lessD1 add.commute of_nat_mono_maybe) 1022 1023 have "x < a + of_nat b \<or> \<not> of_nat (sk x a b) < (of_nat b :: 'a word) \<or> ?thesis" 1024 using f1 f2 by metis 1025 1026 hence "x < a + of_nat b \<or> ?thesis" 1027 using f3 by metis 1028 1029 thus "?thesis" 1030 apply (rule disjE) 1031 apply (rule iffI) 1032 apply (clarsimp simp: intvl_def) 1033 apply (clarsimp simp: unat_sub_if_size word_le_nat_alt word_less_nat_alt) 1034 apply (cut_tac no_overflow) 1035 apply (subgoal_tac "k + (b + unat a) < 2 ^ len_of (TYPE('a)) + b") 1036 apply (subgoal_tac "k + unat a < 2 ^ len_of (TYPE('a))") 1037 apply (metis add_lessD1 le_def less_not_refl2 add.commute unat_eq_of_nat word_arith_nat_add) 1038 apply clarsimp 1039 apply clarsimp 1040 apply (clarsimp simp: intvl_def) 1041 apply (rule exI [where x="unat (x - a)"]) 1042 apply (clarsimp simp: unat_sub_if_size word_le_nat_alt word_less_nat_alt) 1043 apply (cut_tac no_overflow) 1044 apply (metis diff_le_self le_add_diff_inverse le_diff_conv le_eq_less_or_eq le_unat_uoi add.commute nat_neq_iff unat_of_nat_eq word_arith_nat_add) 1045 apply simp 1046 done 1047qed 1048 1049(* arg_cong specified for FCP because it does not apply as is. *) 1050lemma FCP_arg_cong:"f = g \<Longrightarrow> FCP f = FCP g" 1051 by simp 1052 1053lemma h_val_id: 1054 "h_val (hrs_mem (hrs_mem_update (heap_update x y) s)) x = (y::'a::mem_type)" 1055 apply (subst hrs_mem_update) 1056 apply (rule h_val_heap_update) 1057 done 1058 1059lemma heap_update_id2: 1060 "hrs_mem_update (heap_update p ((h_val (hrs_mem s) p)::'a::packed_type)) s = s" 1061 apply (clarsimp simp:hrs_mem_update_def case_prod_beta) 1062 apply (subst heap_update_id) 1063 apply (simp add:hrs_mem_def)+ 1064 done 1065 1066lemma intvlI_unat:"unat b < unat c \<Longrightarrow> a + b \<in> {a ..+ unat c}" 1067 by (metis intvlI word_unat.Rep_inverse) 1068 1069lemma neq_imp_bytes_disjoint: 1070 "\<lbrakk> c_guard (x::'a::c_type ptr); c_guard y; unat j < align_of TYPE('a); 1071 unat i < align_of TYPE('a); x \<noteq> y; 2 ^ n = align_of TYPE('a); n < 32\<rbrakk> \<Longrightarrow> 1072 ptr_val x + j \<noteq> ptr_val y + i" 1073 apply (rule ccontr) 1074 apply (subgoal_tac "is_aligned (ptr_val x) n") 1075 apply (subgoal_tac "is_aligned (ptr_val y) n") 1076 apply (subgoal_tac "(ptr_val x + j && ~~ mask n) = (ptr_val y + i && ~~ mask n)") 1077 apply (subst (asm) neg_mask_add_aligned, simp, simp add: word_less_nat_alt) 1078 apply (subst (asm) neg_mask_add_aligned, simp, simp add: word_less_nat_alt) 1079 apply (clarsimp simp: is_aligned_neg_mask_eq) 1080 apply simp 1081 apply (clarsimp simp: c_guard_def ptr_aligned_def is_aligned_def) 1082 apply (clarsimp simp: c_guard_def ptr_aligned_def is_aligned_def) 1083 done 1084 1085lemma heap_update_list_base':"heap_update_list p [] = id" 1086 by (rule ext, simp) 1087 1088lemma hrs_mem_update_id3: "hrs_mem_update id = id" 1089 unfolding hrs_mem_update_def by simp 1090 1091abbreviation 1092 ptr_span :: "'a::mem_type ptr \<Rightarrow> addr set" where 1093 "ptr_span p \<equiv> {ptr_val p ..+ size_of TYPE('a)}" 1094 1095abbreviation (input) 1096 cptr_type :: "('a :: c_type) ptr \<Rightarrow> 'a itself" 1097where 1098 "cptr_type p \<equiv> TYPE('a)" 1099 1100lemma ptr_retyp_valid_footprint_disjoint2: 1101 "\<lbrakk>valid_footprint (ptr_retyp (q::'b::mem_type ptr) d) p s; {p..+size_td s} \<inter> {ptr_val q..+size_of TYPE('b)} = {} \<rbrakk> 1102 \<Longrightarrow> valid_footprint d p s" 1103 apply(clarsimp simp: valid_footprint_def Let_def) 1104 apply (drule spec, drule (1) mp) 1105 apply(subgoal_tac "p + of_nat y \<in> {p..+size_td s}") 1106 apply (subst (asm) ptr_retyp_d) 1107 apply clarsimp 1108 apply fast 1109 apply (clarsimp simp add: ptr_retyp_d_eq_fst split: if_split_asm) 1110 apply fast 1111 apply (erule intvlI) 1112 done 1113 1114lemma ptr_retyp_disjoint2: 1115 "\<lbrakk>ptr_retyp (p::'a::mem_type ptr) d,g \<Turnstile>\<^sub>t q; 1116 {ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {} \<rbrakk> 1117 \<Longrightarrow> d,g \<Turnstile>\<^sub>t (q::'b::mem_type ptr)" 1118apply(clarsimp simp: h_t_valid_def) 1119apply(erule ptr_retyp_valid_footprint_disjoint2) 1120apply(simp add: size_of_def) 1121apply fast 1122done 1123 1124lemma ptr_retyp_disjoint_iff: 1125 "{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {} 1126 \<Longrightarrow> ptr_retyp (p::'a::mem_type ptr) d,g \<Turnstile>\<^sub>t q = d,g \<Turnstile>\<^sub>t (q::'b::mem_type ptr)" 1127 apply rule 1128 apply (erule (1) ptr_retyp_disjoint2) 1129 apply (erule (1) ptr_retyp_disjoint) 1130 done 1131 1132lemma h_t_valid_ptr_retyp_eq: 1133 "\<not> cptr_type p <\<^sub>\<tau> cptr_type p' \<Longrightarrow> h_t_valid (ptr_retyp p td) g p' 1134 = (if ptr_span p \<inter> ptr_span p' = {} then h_t_valid td g p' 1135 else field_of_t p' p \<and> g p')" 1136 apply (clarsimp simp: ptr_retyp_disjoint_iff split: if_split) 1137 apply (cases "g p'") 1138 apply (rule iffI) 1139 apply (rule ccontr, drule h_t_valid_neq_disjoint, rule ptr_retyp_h_t_valid, simp+) 1140 apply (simp add: Int_commute) 1141 apply (clarsimp simp: field_of_t_def field_of_def) 1142 apply (drule sub_h_t_valid[where p=p, rotated], rule ptr_retyp_h_t_valid, simp, simp) 1143 apply (erule(1) h_t_valid_guard_subst) 1144 apply (simp add: h_t_valid_def) 1145 done 1146 1147lemma field_lookup_list_Some_again: 1148 "dt_snd (xs ! i) = f 1149 \<Longrightarrow> i < length xs 1150 \<Longrightarrow> f \<notin> dt_snd ` set ((take i xs)) 1151 \<Longrightarrow> field_lookup_list xs [f] n 1152 = Some (dt_fst (xs ! i), n + sum_list (map (size_td o dt_fst) (take i xs)))" 1153 apply (induct xs arbitrary: i n, simp_all) 1154 apply (case_tac x1, simp) 1155 apply (case_tac i, auto split: if_split) 1156 done 1157 1158lemma field_lookup_array: 1159 "n < CARD('b) \<Longrightarrow> field_lookup (typ_info_t TYPE(('a :: c_type)['b :: finite])) 1160 [replicate n (CHR ''1'')] i = Some (adjust_ti (typ_info_t TYPE('a)) 1161 (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x), i + n * size_of TYPE ('a))" 1162 apply (simp add: typ_info_array array_tag_def array_tag_n_eq) 1163 apply (subst field_lookup_list_Some_again[where i=n], 1164 auto simp add: take_map o_def sum_list_triv size_of_def) 1165 done 1166 1167lemma field_of_t_refl: 1168 "field_of_t p p' = (p = p')" 1169 apply (safe, simp_all add: field_of_t_def) 1170 apply (simp add: field_of_def) 1171 apply (drule td_set_size_lte) 1172 apply (simp add: unat_eq_0) 1173 done 1174 1175lemma ptr_retyp_same_cleared_region: 1176 fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr" 1177 assumes ht: "ptr_retyp p td, g \<Turnstile>\<^sub>t p'" 1178 shows "p = p' \<or> {ptr_val p..+ size_of TYPE('a)} \<inter> {ptr_val p' ..+ size_of TYPE('a)} = {}" 1179 using ht 1180 by (simp add: h_t_valid_ptr_retyp_eq[where p=p and p'=p'] field_of_t_refl 1181 split: if_split_asm) 1182 1183lemma h_t_valid_ptr_retyp_inside_eq: 1184 fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr" 1185 assumes inside: "ptr_val p' \<in> {ptr_val p ..+ size_of TYPE('a)}" 1186 and ht: "ptr_retyp p td, g \<Turnstile>\<^sub>t p'" 1187 shows "p = p'" 1188 using ptr_retyp_same_cleared_region[OF ht] inside mem_type_self[where p=p'] 1189 by blast 1190 1191lemma typ_slice_t_self_nth: 1192 "\<exists>n < length (typ_slice_t td m). \<exists>b. typ_slice_t td m ! n = (td, b)" 1193 using typ_slice_t_self [where td = td and m = m] 1194 by (fastforce simp add: in_set_conv_nth) 1195 1196lemma ptr_retyp_other_cleared_region: 1197 fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr" 1198 assumes ht: "ptr_retyp p td, g \<Turnstile>\<^sub>t p'" 1199 and tdisj: "typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b :: mem_type)" 1200 and clear: "\<forall>x \<in> {ptr_val p ..+ size_of TYPE('a)}. \<forall>n b. snd (td x) n \<noteq> Some (typ_uinfo_t TYPE('b), b)" 1201 shows "{ptr_val p'..+ size_of TYPE('b)} \<inter> {ptr_val p ..+ size_of TYPE('a)} = {}" 1202proof (rule classical) 1203 assume asm: "{ptr_val p'..+ size_of TYPE('b)} \<inter> {ptr_val p ..+ size_of TYPE('a)} \<noteq> {}" 1204 then obtain mv where mvp: "mv \<in> {ptr_val p..+size_of TYPE('a)}" 1205 and mvp': "mv \<in> {ptr_val p'..+size_of TYPE('b)}" 1206 by blast 1207 1208 then obtain k' where mv: "mv = ptr_val p' + of_nat k'" and klt: "k' < size_td (typ_info_t TYPE('b))" 1209 by (clarsimp dest!: intvlD simp: size_of_def typ_uinfo_size) 1210 1211 let ?mv = "ptr_val p' + of_nat k'" 1212 1213 obtain n b where nl: "n < length (typ_slice_t (typ_uinfo_t TYPE('b)) k')" 1214 and tseq: "typ_slice_t (typ_uinfo_t TYPE('b)) k' ! n = (typ_uinfo_t TYPE('b), b)" 1215 using typ_slice_t_self_nth [where td = "typ_uinfo_t TYPE('b)" and m = k'] 1216 by clarsimp 1217 1218 with ht have "snd (ptr_retyp p td ?mv) n = Some (typ_uinfo_t TYPE('b), b)" 1219 unfolding h_t_valid_def 1220 apply - 1221 apply (clarsimp simp: valid_footprint_def Let_def) 1222 apply (drule spec, drule mp [OF _ klt]) 1223 apply (clarsimp simp: map_le_def) 1224 apply (drule bspec) 1225 apply simp 1226 apply simp 1227 done 1228 1229 moreover { 1230 assume "snd (ptr_retyp p empty_htd ?mv) n = Some (typ_uinfo_t TYPE('b), b)" 1231 hence "(typ_uinfo_t TYPE('b)) \<in> fst ` set (typ_slice_t (typ_uinfo_t TYPE('a)) 1232 (unat (ptr_val p' + of_nat k' - ptr_val p)))" 1233 using asm mv mvp 1234 apply - 1235 apply (rule_tac x = "(typ_uinfo_t TYPE('b), b)" in image_eqI) 1236 apply simp 1237 apply (fastforce simp add: ptr_retyp_footprint list_map_eq in_set_conv_nth split: if_split_asm) 1238 done 1239 1240 with typ_slice_set have "(typ_uinfo_t TYPE('b)) \<in> fst ` td_set (typ_uinfo_t TYPE('a)) 0" 1241 by (rule subsetD) 1242 1243 hence False using tdisj by (clarsimp simp: tag_disj_def typ_tag_le_def) 1244 } ultimately show ?thesis using mvp mvp' mv unfolding h_t_valid_def valid_footprint_def 1245 apply - 1246 apply (subst (asm) ptr_retyp_d_eq_snd) 1247 apply (auto simp add: map_add_Some_iff clear) 1248 done 1249qed 1250 1251end 1252