1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7section "Word Alignment" 8 9theory Aligned 10imports 11 Word_Lib 12 HOL_Lemmas 13 More_Divides 14begin 15 16 17definition 18 is_aligned :: "'a :: len word \<Rightarrow> nat \<Rightarrow> bool" where 19 "is_aligned ptr n \<equiv> 2^n dvd unat ptr" 20 21 22lemma is_aligned_mask: "(is_aligned w n) = (w && mask n = 0)" 23 unfolding is_aligned_def by (rule and_mask_dvd_nat) 24 25 26lemma is_aligned_to_bl: 27 "is_aligned (w :: 'a :: len word) n = (True \<notin> set (drop (size w - n) (to_bl w)))" 28 apply (simp add: is_aligned_mask eq_zero_set_bl) 29 apply (clarsimp simp: in_set_conv_nth word_size) 30 apply (simp add: to_bl_nth word_size cong: conj_cong) 31 apply (simp add: diff_diff_less) 32 apply safe 33 apply (case_tac "n \<le> LENGTH('a)") 34 prefer 2 35 apply (rule_tac x=i in exI) 36 apply clarsimp 37 apply (subgoal_tac "\<exists>j < LENGTH('a). j < n \<and> LENGTH('a) - n + j = i") 38 apply (erule exE) 39 apply (rule_tac x=j in exI) 40 apply clarsimp 41 apply (thin_tac "w !! t" for t) 42 apply (rule_tac x="i + n - LENGTH('a)" in exI) 43 apply clarsimp 44 apply arith 45 apply (rule_tac x="LENGTH('a) - n + i" in exI) 46 apply clarsimp 47 apply arith 48 done 49 50lemma unat_power_lower [simp]: 51 assumes nv: "n < LENGTH('a::len)" 52 shows "unat ((2::'a::len word) ^ n) = 2 ^ n" 53 by (simp add: assms nat_power_eq uint_2p_alt unat_def) 54 55lemma power_overflow: 56 "n \<ge> LENGTH('a) \<Longrightarrow> 2 ^ n = (0 :: 'a::len word)" 57 by simp 58 59lemma is_alignedI [intro?]: 60 fixes x::"'a::len word" 61 assumes xv: "x = 2 ^ n * k" 62 shows "is_aligned x n" 63proof cases 64 assume nv: "n < LENGTH('a)" 65 show ?thesis 66 unfolding is_aligned_def 67 proof (rule dvdI [where k = "unat k mod 2 ^ (LENGTH('a) - n)"]) 68 from xv 69 have "unat x = (unat (2::word32) ^ n * unat k) mod 2 ^ LENGTH('a)" 70 using nv 71 by (subst (asm) word_unat.Rep_inject [symmetric], simp, 72 subst unat_word_ariths, simp) 73 74 also have "\<dots> = 2 ^ n * (unat k mod 2 ^ (LENGTH('a) - n))" using nv 75 by (simp add: mult_mod_right power_add [symmetric] add_diff_inverse) 76 77 finally show "unat x = 2 ^ n * (unat k mod 2 ^ (LENGTH('a) - n))" . 78 qed 79next 80 assume "\<not> n < LENGTH('a)" 81 with xv 82 show ?thesis by (simp add: not_less power_overflow is_aligned_def) 83qed 84 85lemma is_aligned_weaken: 86 "\<lbrakk> is_aligned w x; x \<ge> y \<rbrakk> \<Longrightarrow> is_aligned w y" 87 unfolding is_aligned_def 88 by (erule dvd_trans [rotated]) (simp add: le_imp_power_dvd) 89 90lemma nat_power_less_diff: 91 assumes lt: "(2::nat) ^ n * q < 2 ^ m" 92 shows "q < 2 ^ (m - n)" 93 using lt 94proof (induct n arbitrary: m) 95 case 0 96 then show ?case by simp 97next 98 case (Suc n) 99 100 have ih: "\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n)" 101 and prem: "2 ^ Suc n * q < 2 ^ m" by fact+ 102 103 show ?case 104 proof (cases m) 105 case 0 106 then show ?thesis using Suc by simp 107 next 108 case (Suc m') 109 then show ?thesis using prem 110 by (simp add: ac_simps ih) 111 qed 112qed 113 114lemma is_alignedE_pre: 115 fixes w::"'a::len word" 116 assumes aligned: "is_aligned w n" 117 shows rl: "\<exists>q. w = 2 ^ n * (of_nat q) \<and> q < 2 ^ (LENGTH('a) - n)" 118proof - 119 from aligned obtain q where wv: "unat w = 2 ^ n * q" 120 unfolding is_aligned_def .. 121 122 show ?thesis 123 proof (rule exI, intro conjI) 124 show "q < 2 ^ (LENGTH('a) - n)" 125 proof (rule nat_power_less_diff) 126 have "unat w < 2 ^ size w" unfolding word_size .. 127 then have "unat w < 2 ^ LENGTH('a)" by simp 128 with wv show "2 ^ n * q < 2 ^ LENGTH('a)" by simp 129 qed 130 131 have r: "of_nat (2 ^ n) = (2::word32) ^ n" 132 by (induct n) simp+ 133 134 from wv have "of_nat (unat w) = of_nat (2 ^ n * q)" by simp 135 then have "w = of_nat (2 ^ n * q)" by (subst word_unat.Rep_inverse [symmetric]) 136 then show "w = 2 ^ n * (of_nat q)" by (simp add: r) 137 qed 138qed 139 140lemma is_alignedE: 141 "\<lbrakk>is_aligned (w::'a::len word) n; 142 \<And>q. \<lbrakk>w = 2 ^ n * (of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 143 by (auto dest: is_alignedE_pre) 144 145lemma is_aligned_replicate: 146 fixes w::"'a::len word" 147 assumes aligned: "is_aligned w n" 148 and nv: "n \<le> LENGTH('a)" 149 shows "to_bl w = (take (LENGTH('a) - n) (to_bl w)) @ replicate n False" 150proof - 151 from nv have rl: "\<And>q. q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> 152 to_bl (2 ^ n * (of_nat q :: 'a word)) = 153 drop n (to_bl (of_nat q :: 'a word)) @ replicate n False" 154 by (metis bl_shiftl le_antisym min_def shiftl_t2n wsst_TYs(3)) 155 show ?thesis using aligned 156 by (auto simp: rl elim: is_alignedE) 157qed 158 159lemma is_aligned_drop: 160 fixes w::"'a::len word" 161 assumes "is_aligned w n" "n \<le> LENGTH('a)" 162 shows "drop (LENGTH('a) - n) (to_bl w) = replicate n False" 163proof - 164 have "to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False" 165 by (rule is_aligned_replicate) fact+ 166 then have "drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) \<dots>" by simp 167 also have "\<dots> = replicate n False" by simp 168 finally show ?thesis . 169qed 170 171lemma less_is_drop_replicate: 172 fixes x::"'a::len word" 173 assumes lt: "x < 2 ^ n" 174 shows "to_bl x = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl x)" 175 by (metis assms bl_and_mask' less_mask_eq) 176 177lemma is_aligned_add_conv: 178 fixes off::"'a::len word" 179 assumes aligned: "is_aligned w n" 180 and offv: "off < 2 ^ n" 181 shows "to_bl (w + off) = 182 (take (LENGTH('a) - n) (to_bl w)) @ (drop (LENGTH('a) - n) (to_bl off))" 183proof cases 184 assume nv: "n \<le> LENGTH('a)" 185 show ?thesis 186 proof (subst aligned_bl_add_size, simp_all only: word_size) 187 show "drop (LENGTH('a) - n) (to_bl w) = replicate n False" 188 by (subst is_aligned_replicate [OF aligned nv]) (simp add: word_size) 189 190 from offv show "take (LENGTH('a) - n) (to_bl off) = 191 replicate (LENGTH('a) - n) False" 192 by (subst less_is_drop_replicate, assumption) simp 193 qed fact 194next 195 assume "\<not> n \<le> LENGTH('a)" 196 with offv show ?thesis by (simp add: power_overflow) 197qed 198 199lemma aligned_add_aligned: 200 fixes x::"'a::len word" 201 assumes aligned1: "is_aligned x n" 202 and aligned2: "is_aligned y m" 203 and lt: "m \<le> n" 204 shows "is_aligned (x + y) m" 205proof cases 206 assume nlt: "n < LENGTH('a)" 207 show ?thesis 208 unfolding is_aligned_def dvd_def 209 proof - 210 from aligned2 obtain q2 where yv: "y = 2 ^ m * of_nat q2" 211 and q2v: "q2 < 2 ^ (LENGTH('a) - m)" 212 by (auto elim: is_alignedE) 213 214 from lt obtain k where kv: "m + k = n" by (auto simp: le_iff_add) 215 with aligned1 obtain q1 where xv: "x = 2 ^ (m + k) * of_nat q1" 216 and q1v: "q1 < 2 ^ (LENGTH('a) - (m + k))" 217 by (auto elim: is_alignedE) 218 219 have l1: "2 ^ (m + k) * q1 < 2 ^ LENGTH('a)" 220 by (rule nat_less_power_trans [OF q1v]) 221 (subst kv, rule order_less_imp_le [OF nlt]) 222 223 have l2: "2 ^ m * q2 < 2 ^ LENGTH('a)" 224 by (rule nat_less_power_trans [OF q2v], 225 rule order_less_imp_le [OF order_le_less_trans]) 226 fact+ 227 228 have "x = of_nat (2 ^ (m + k) * q1)" using xv 229 by simp 230 231 moreover have "y = of_nat (2 ^ m * q2)" using yv 232 by simp 233 234 ultimately have upls: "unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)" 235 proof - 236 have f1: "unat x = 2 ^ (m + k) * q1" 237 by (metis (no_types) \<open>x = of_nat (2 ^ (m + k) * q1)\<close> l1 nat_mod_lem word_unat.inverse_norm 238 zero_less_numeral zero_less_power) 239 have "unat y = 2 ^ m * q2" 240 by (metis (no_types) \<open>y = of_nat (2 ^ m * q2)\<close> l2 nat_mod_lem word_unat.inverse_norm 241 zero_less_numeral zero_less_power) 242 then show ?thesis 243 using f1 by (simp add: power_add semiring_normalization_rules(34)) 244 qed 245 246 (* (2 ^ k * q1 + q2) *) 247 show "\<exists>d. unat (x + y) = 2 ^ m * d" 248 proof (cases "unat x + unat y < 2 ^ LENGTH('a)") 249 case True 250 251 have "unat (x + y) = unat x + unat y" 252 by (subst unat_plus_if', rule if_P) fact 253 254 also have "\<dots> = 2 ^ m * (2 ^ k * q1 + q2)" by (rule upls) 255 finally show ?thesis .. 256 next 257 case False 258 then have "unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)" 259 by (subst unat_word_ariths(1)) simp 260 261 also have "\<dots> = (2 ^ m * (2 ^ k * q1 + q2)) mod 2 ^ LENGTH('a)" 262 by (subst upls, rule refl) 263 264 also 265 have "\<dots> = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))" 266 proof - 267 have "m \<le> len_of (TYPE('a))" 268 by (meson le_trans less_imp_le_nat lt nlt) 269 then show ?thesis 270 by (metis mult_mod_right ordered_cancel_comm_monoid_diff_class.add_diff_inverse power_add) 271 qed 272 273 finally show ?thesis .. 274 qed 275 qed 276next 277 assume "\<not> n < LENGTH('a)" 278 with assms 279 show ?thesis by (simp add: not_less power_overflow is_aligned_mask mask_def) 280qed 281 282corollary aligned_sub_aligned: 283 "\<lbrakk>is_aligned (x::'a::len word) n; is_aligned y m; m \<le> n\<rbrakk> 284 \<Longrightarrow> is_aligned (x - y) m" 285 apply (simp del: add_uminus_conv_diff add:diff_conv_add_uminus) 286 apply (erule aligned_add_aligned, simp_all) 287 apply (erule is_alignedE) 288 apply (rule_tac k="- of_nat q" in is_alignedI) 289 apply simp 290 done 291 292lemma is_aligned_shift: 293 fixes k::"'a::len word" 294 shows "is_aligned (k << m) m" 295proof cases 296 assume mv: "m < LENGTH('a)" 297 from mv obtain q where mq: "m + q = LENGTH('a)" and "0 < q" 298 by (auto dest: less_imp_add_positive) 299 300 have "(2::nat) ^ m dvd unat (k << m)" 301 proof 302 have kv: "(unat k div 2 ^ q) * 2 ^ q + unat k mod 2 ^ q = unat k" 303 by (rule div_mult_mod_eq) 304 305 have "unat (k << m) = unat (2 ^ m * k)" by (simp add: shiftl_t2n) 306 also have "\<dots> = (2 ^ m * unat k) mod (2 ^ LENGTH('a))" using mv 307 by (subst unat_word_ariths(2))+ simp 308 also have "\<dots> = 2 ^ m * (unat k mod 2 ^ q)" 309 by (subst mq [symmetric], subst power_add, subst mod_mult2_eq) simp 310 finally show "unat (k << m) = 2 ^ m * (unat k mod 2 ^ q)" . 311 qed 312 313 then show ?thesis by (unfold is_aligned_def) 314next 315 assume "\<not> m < LENGTH('a)" 316 then show ?thesis 317 by (simp add: not_less power_overflow is_aligned_mask mask_def 318 shiftl_zero_size word_size) 319qed 320 321lemma word_mod_by_0: "k mod (0::'a::len word) = k" 322 by (simp add: word_arith_nat_mod) 323 324lemma aligned_mod_eq_0: 325 fixes p::"'a::len word" 326 assumes al: "is_aligned p sz" 327 shows "p mod 2 ^ sz = 0" 328proof cases 329 assume szv: "sz < LENGTH('a)" 330 with al 331 show ?thesis 332 unfolding is_aligned_def 333 by (simp add: and_mask_dvd_nat p2_gt_0 word_mod_2p_is_mask) 334next 335 assume "\<not> sz < LENGTH('a)" 336 with al show ?thesis 337 by (simp add: not_less power_overflow is_aligned_mask mask_def word_mod_by_0) 338qed 339 340lemma is_aligned_triv: "is_aligned (2 ^ n ::'a::len word) n" 341 by (rule is_alignedI [where k = 1], simp) 342 343lemma is_aligned_mult_triv1: "is_aligned (2 ^ n * x ::'a::len word) n" 344 by (rule is_alignedI [OF refl]) 345 346lemma is_aligned_mult_triv2: "is_aligned (x * 2 ^ n ::'a::len word) n" 347 by (subst mult.commute, simp add: is_aligned_mult_triv1) 348 349lemma word_power_less_0_is_0: 350 fixes x :: "'a::len word" 351 shows "x < a ^ 0 \<Longrightarrow> x = 0" by simp 352 353lemma nat_add_offset_less: 354 fixes x :: nat 355 assumes yv: "y < 2 ^ n" 356 and xv: "x < 2 ^ m" 357 and mn: "sz = m + n" 358 shows "x * 2 ^ n + y < 2 ^ sz" 359proof (subst mn) 360 from yv obtain qy where "y + qy = 2 ^ n" and "0 < qy" 361 by (auto dest: less_imp_add_positive) 362 363 have "x * 2 ^ n + y < x * 2 ^ n + 2 ^ n" by simp fact+ 364 also have "\<dots> = (x + 1) * 2 ^ n" by simp 365 also have "\<dots> \<le> 2 ^ (m + n)" using xv 366 by (subst power_add) (rule mult_le_mono1, simp) 367 finally show "x * 2 ^ n + y < 2 ^ (m + n)" . 368qed 369 370lemma is_aligned_no_wrap: 371 fixes off :: "'a::len word" 372 fixes ptr :: "'a::len word" 373 assumes al: "is_aligned ptr sz" 374 and off: "off < 2 ^ sz" 375 shows "unat ptr + unat off < 2 ^ LENGTH('a)" 376proof - 377 have szv: "sz < LENGTH('a)" 378 using off p2_gt_0 word_neq_0_conv by fastforce 379 380 from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and 381 qv: "q < 2 ^ (LENGTH('a) - sz)" by (auto elim: is_alignedE) 382 383 show ?thesis 384 proof (cases "sz = 0") 385 case True 386 then show ?thesis using off ptrq qv by clarsimp 387 next 388 case False 389 then have sne: "0 < sz" .. 390 391 show ?thesis 392 proof - 393 have uq: "unat (of_nat q ::'a::len word) = q" 394 apply (subst unat_of_nat) 395 apply (rule mod_less) 396 apply (rule order_less_trans [OF qv]) 397 apply (rule power_strict_increasing [OF diff_less [OF sne]]) 398 apply (simp_all) 399 done 400 401 have uptr: "unat ptr = 2 ^ sz * q" 402 apply (subst ptrq) 403 apply (subst iffD1 [OF unat_mult_lem]) 404 apply (subst unat_power_lower [OF szv]) 405 apply (subst uq) 406 apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]]) 407 apply (subst uq) 408 apply (subst unat_power_lower [OF szv]) 409 apply simp 410 done 411 412 show "unat ptr + unat off < 2 ^ LENGTH('a)" using szv 413 apply (subst uptr) 414 apply (subst mult.commute, rule nat_add_offset_less [OF _ qv]) 415 apply (rule order_less_le_trans [OF unat_mono [OF off] order_eq_refl]) 416 apply simp_all 417 done 418 qed 419 qed 420qed 421 422lemma is_aligned_no_wrap': 423 fixes ptr :: "'a::len word" 424 assumes al: "is_aligned ptr sz" 425 and off: "off < 2 ^ sz" 426 shows "ptr \<le> ptr + off" 427 by (subst no_plus_overflow_unat_size, subst word_size, rule is_aligned_no_wrap) fact+ 428 429lemma is_aligned_no_overflow': 430 fixes p :: "'a::len word" 431 assumes al: "is_aligned p n" 432 shows "p \<le> p + (2 ^ n - 1)" 433proof cases 434 assume "n<LENGTH('a)" 435 with al 436 have "2^n - (1::'a::len word) < 2^n" 437 by (simp add: word_less_nat_alt unat_sub_if_size) 438 with al 439 show ?thesis by (rule is_aligned_no_wrap') 440next 441 assume "\<not> n<LENGTH('a)" 442 with al 443 show ?thesis 444 by (simp add: not_less power_overflow is_aligned_mask mask_2pm1) 445qed 446 447lemma is_aligned_no_overflow: 448 "is_aligned ptr sz \<Longrightarrow> ptr \<le> ptr + 2^sz - 1" 449 by (drule is_aligned_no_overflow') (simp add: field_simps) 450 451lemma replicate_not_True: 452 "\<And>n. xs = replicate n False \<Longrightarrow> True \<notin> set xs" 453 by (induct xs) auto 454 455lemma is_aligned_replicateI: 456 "to_bl p = addr @ replicate n False \<Longrightarrow> is_aligned (p::'a::len word) n" 457 apply (simp add: is_aligned_to_bl word_size) 458 apply (subgoal_tac "length addr = LENGTH('a) - n") 459 apply (simp add: replicate_not_True) 460 apply (drule arg_cong [where f=length]) 461 apply simp 462 done 463 464lemma to_bl_2p: 465 "n < LENGTH('a) \<Longrightarrow> 466 to_bl ((2::'a::len word) ^ n) = 467 replicate (LENGTH('a) - Suc n) False @ True # replicate n False" 468 apply (subst shiftl_1 [symmetric]) 469 apply (subst bl_shiftl) 470 apply (simp add: to_bl_1 min_def word_size) 471 done 472 473lemma map_zip_replicate_False_xor: 474 "n = length xs \<Longrightarrow> map (\<lambda>(x, y). x = (\<not> y)) (zip xs (replicate n False)) = xs" 475 by (induct xs arbitrary: n, auto) 476 477lemma drop_minus_lem: 478 "\<lbrakk> n \<le> length xs; 0 < n; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs" 479proof (induct xs arbitrary: n n') 480 case Nil then show ?case by simp 481next 482 case (Cons y ys) 483 from Cons.prems 484 show ?case 485 apply simp 486 apply (cases "n = Suc (length ys)") 487 apply (simp add: nth_append) 488 apply (simp add: Suc_diff_le Cons.hyps nth_append) 489 apply clarsimp 490 apply arith 491 done 492qed 493 494lemma drop_minus: 495 "\<lbrakk> n < length xs; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - Suc n) xs = rev xs ! n # drop (n' - n) xs" 496 apply (subst drop_minus_lem) 497 apply simp 498 apply simp 499 apply simp 500 apply simp 501 apply (cases "length xs", simp) 502 apply (simp add: Suc_diff_le) 503 done 504 505lemma xor_2p_to_bl: 506 fixes x::"'a::len word" 507 shows "to_bl (x xor 2^n) = 508 (if n < LENGTH('a) 509 then take (LENGTH('a)-Suc n) (to_bl x) @ (\<not>rev (to_bl x)!n) # drop (LENGTH('a)-n) (to_bl x) 510 else to_bl x)" 511proof - 512 have x: "to_bl x = take (LENGTH('a)-Suc n) (to_bl x) @ drop (LENGTH('a)-Suc n) (to_bl x)" 513 by simp 514 515 show ?thesis 516 apply simp 517 apply (rule conjI) 518 apply (clarsimp simp: word_size) 519 apply (simp add: bl_word_xor to_bl_2p) 520 apply (subst x) 521 apply (subst zip_append) 522 apply simp 523 apply (simp add: map_zip_replicate_False_xor drop_minus) 524 apply (auto simp add: word_size nth_w2p intro!: word_eqI) 525 done 526qed 527 528lemma aligned_add_xor: 529 assumes al: "is_aligned (x::'a::len word) n'" and le: "n < n'" 530 shows "(x + 2^n) xor 2^n = x" 531proof cases 532 assume "n' < LENGTH('a)" 533 with assms show ?thesis 534 apply - 535 apply (rule word_bl.Rep_eqD) 536 apply (subst xor_2p_to_bl) 537 apply simp 538 apply (subst is_aligned_add_conv, simp, simp add: word_less_nat_alt)+ 539 apply (simp add: to_bl_2p nth_append) 540 apply (cases "n' = Suc n") 541 apply simp 542 apply (subst is_aligned_replicate [where n="Suc n", simplified, symmetric]; simp) 543 apply (subgoal_tac "\<not> LENGTH('a) - Suc n \<le> LENGTH('a) - n'") 544 prefer 2 545 apply arith 546 apply (subst replicate_Suc [symmetric]) 547 apply (subst replicate_add [symmetric]) 548 apply (simp add: is_aligned_replicate [simplified, symmetric]) 549 done 550next 551 assume "\<not> n' < LENGTH('a)" 552 with al show ?thesis 553 by (simp add: is_aligned_mask mask_def not_less power_overflow) 554qed 555 556lemma is_aligned_0 [simp]: 557 "is_aligned p 0" 558 by (simp add: is_aligned_def) 559 560lemma is_aligned_replicateD: 561 "\<lbrakk> is_aligned (w::'a::len word) n; n \<le> LENGTH('a) \<rbrakk> 562 \<Longrightarrow> \<exists>xs. to_bl w = xs @ replicate n False 563 \<and> length xs = size w - n" 564 apply (subst is_aligned_replicate, assumption+) 565 apply (rule exI, rule conjI, rule refl) 566 apply (simp add: word_size) 567 done 568 569lemma is_aligned_add_mult_multI: 570 fixes p :: "'a::len word" 571 shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n * z) n'" 572 apply (erule aligned_add_aligned) 573 apply (auto intro: is_alignedI [where k="x*z"]) 574 done 575 576lemma is_aligned_add_multI: 577 fixes p :: "'a::len word" 578 shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n) n'" 579 apply (erule aligned_add_aligned) 580 apply (auto intro: is_alignedI [where k="x"]) 581 done 582 583lemma unat_of_nat_len: 584 "x < 2 ^ LENGTH('a) \<Longrightarrow> unat (of_nat x :: 'a::len word) = x" 585 by (simp add: word_size unat_of_nat) 586 587lemma is_aligned_no_wrap''': 588 fixes ptr :: "'a::len word" 589 shows"\<lbrakk> is_aligned ptr sz; sz < LENGTH('a); off < 2 ^ sz \<rbrakk> 590 \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)" 591 apply (drule is_aligned_no_wrap[where off="of_nat off"]) 592 apply (simp add: word_less_nat_alt) 593 apply (erule order_le_less_trans[rotated]) 594 apply (subst unat_of_nat) 595 apply (rule mod_less_eq_dividend) 596 apply (subst(asm) unat_of_nat_len) 597 apply (erule order_less_trans) 598 apply (erule power_strict_increasing) 599 apply simp 600 apply assumption 601 done 602 603lemma is_aligned_get_word_bits: 604 fixes p :: "'a::len word" 605 shows "\<lbrakk> is_aligned p n; \<lbrakk> is_aligned p n; n < LENGTH('a) \<rbrakk> \<Longrightarrow> P; 606 \<lbrakk> p = 0; n \<ge> LENGTH('a) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 607 apply (cases "n < LENGTH('a)") 608 apply simp 609 apply simp 610 apply (erule meta_mp) 611 apply (clarsimp simp: is_aligned_mask mask_def power_add 612 power_overflow) 613 done 614 615lemma aligned_small_is_0: 616 "\<lbrakk> is_aligned x n; x < 2 ^ n \<rbrakk> \<Longrightarrow> x = 0" 617 apply (erule is_aligned_get_word_bits) 618 apply (frule is_aligned_add_conv [rotated, where w=0]) 619 apply (simp add: is_aligned_def) 620 apply simp 621 apply (drule is_aligned_replicateD) 622 apply simp 623 apply (clarsimp simp: word_size) 624 apply (subst (asm) replicate_add [symmetric]) 625 apply (drule arg_cong[where f="of_bl :: bool list \<Rightarrow> 'a::len word"]) 626 apply simp 627 apply (simp only: replicate.simps[symmetric, where x=False] 628 drop_replicate) 629 done 630 631corollary is_aligned_less_sz: 632 "\<lbrakk>is_aligned a sz; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> a < 2 ^ sz" 633 by (rule notI, drule(1) aligned_small_is_0, erule(1) notE) 634 635lemma aligned_at_least_t2n_diff: 636 "\<lbrakk>is_aligned x n; is_aligned y n; x < y\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n" 637 apply (erule is_aligned_get_word_bits[where p=y]) 638 apply (rule ccontr) 639 apply (clarsimp simp: linorder_not_le) 640 apply (subgoal_tac "y - x = 0") 641 apply clarsimp 642 apply (rule aligned_small_is_0) 643 apply (erule(1) aligned_sub_aligned) 644 apply simp 645 apply unat_arith 646 apply simp 647 done 648 649lemma word_sub_1_le: 650 "x \<noteq> 0 \<Longrightarrow> x - 1 \<le> (x :: ('a :: len) word)" 651 apply (subst no_ulen_sub) 652 apply simp 653 apply (cases "uint x = 0") 654 apply (simp add: uint_0_iff) 655 apply (insert uint_ge_0[where x=x]) 656 apply arith 657 done 658 659lemma is_aligned_no_overflow'': 660 "\<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n" 661 apply (frule is_aligned_no_overflow') 662 apply (erule order_trans) 663 apply (simp add: field_simps) 664 apply (erule word_sub_1_le) 665 done 666 667lemma is_aligned_nth: 668 "is_aligned p m = (\<forall>n < m. \<not>p !! n)" 669 apply (clarsimp simp: is_aligned_mask bang_eq word_size) 670 apply (rule iffI) 671 apply clarsimp 672 apply (case_tac "n < size p") 673 apply (simp add: word_size) 674 apply (drule test_bit_size) 675 apply simp 676 apply clarsimp 677 done 678 679lemma range_inter: 680 "({a..b} \<inter> {c..d} = {}) = (\<forall>x. \<not>(a \<le> x \<and> x \<le> b \<and> c \<le> x \<and> x \<le> d))" 681 by auto 682 683lemma aligned_inter_non_empty: 684 "\<lbrakk> {p..p + (2 ^ n - 1)} \<inter> {p..p + 2 ^ m - 1} = {}; 685 is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False" 686 apply (clarsimp simp only: range_inter) 687 apply (erule_tac x=p in allE) 688 apply simp 689 apply (erule impE) 690 apply (erule is_aligned_no_overflow') 691 apply (erule notE) 692 apply (erule is_aligned_no_overflow) 693 done 694 695lemma not_aligned_mod_nz: 696 assumes al: "\<not> is_aligned a n" 697 shows "a mod 2 ^ n \<noteq> 0" 698proof cases 699 assume "n < LENGTH('a)" 700 with al 701 show ?thesis 702 apply (simp add: is_aligned_def dvd_eq_mod_eq_0 word_arith_nat_mod) 703 apply (erule of_nat_neq_0) 704 apply (rule order_less_trans) 705 apply (rule mod_less_divisor) 706 apply simp 707 apply simp 708 done 709next 710 assume "\<not> n < LENGTH('a)" 711 with al 712 show ?thesis 713 by (simp add: is_aligned_mask mask_def not_less power_overflow 714 word_less_nat_alt word_mod_by_0) 715qed 716 717lemma nat_add_offset_le: 718 fixes x :: nat 719 assumes yv: "y \<le> 2 ^ n" 720 and xv: "x < 2 ^ m" 721 and mn: "sz = m + n" 722 shows "x * 2 ^ n + y \<le> 2 ^ sz" 723proof (subst mn) 724 from yv obtain qy where "y + qy = 2 ^ n" 725 by (auto simp: le_iff_add) 726 727 have "x * 2 ^ n + y \<le> x * 2 ^ n + 2 ^ n" 728 using yv xv by simp 729 also have "\<dots> = (x + 1) * 2 ^ n" by simp 730 also have "\<dots> \<le> 2 ^ (m + n)" using xv 731 by (subst power_add) (rule mult_le_mono1, simp) 732 finally show "x * 2 ^ n + y \<le> 2 ^ (m + n)" . 733qed 734 735lemma is_aligned_no_wrap_le: 736 fixes ptr::"'a::len word" 737 assumes al: "is_aligned ptr sz" 738 and szv: "sz < LENGTH('a)" 739 and off: "off \<le> 2 ^ sz" 740 shows "unat ptr + off \<le> 2 ^ LENGTH('a)" 741proof - 742 from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and 743 qv: "q < 2 ^ (LENGTH('a) - sz)" by (auto elim: is_alignedE) 744 745 show ?thesis 746 proof (cases "sz = 0") 747 case True 748 then show ?thesis using off ptrq qv 749 apply (clarsimp) 750 apply (erule le_SucE) 751 apply (simp add: unat_of_nat) 752 apply (simp add: less_eq_Suc_le [symmetric] unat_of_nat) 753 done 754 next 755 case False 756 then have sne: "0 < sz" .. 757 758 show ?thesis 759 proof - 760 have uq: "unat (of_nat q :: 'a word) = q" 761 apply (subst unat_of_nat) 762 apply (rule mod_less) 763 apply (rule order_less_trans [OF qv]) 764 apply (rule power_strict_increasing [OF diff_less [OF sne]]) 765 apply simp_all 766 done 767 768 have uptr: "unat ptr = 2 ^ sz * q" 769 apply (subst ptrq) 770 apply (subst iffD1 [OF unat_mult_lem]) 771 apply (subst unat_power_lower [OF szv]) 772 apply (subst uq) 773 apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]]) 774 apply (subst uq) 775 apply (subst unat_power_lower [OF szv]) 776 apply simp 777 done 778 779 show "unat ptr + off \<le> 2 ^ LENGTH('a)" using szv 780 apply (subst uptr) 781 apply (subst mult.commute, rule nat_add_offset_le [OF off qv]) 782 apply simp 783 done 784 qed 785 qed 786qed 787 788lemma is_aligned_neg_mask: 789 "m \<le> n \<Longrightarrow> is_aligned (x && ~~ (mask n)) m" 790 by (metis and_not_mask is_aligned_shift is_aligned_weaken) 791 792lemma unat_minus: 793 "unat (- (x :: 'a :: len word)) = (if x = 0 then 0 else 2 ^ size x - unat x)" 794 using unat_sub_if_size[where x="2 ^ size x" and y=x] 795 by (simp add: unat_eq_0 word_size) 796 797lemma is_aligned_minus: 798 "is_aligned p n \<Longrightarrow> is_aligned (- p) n" 799 apply (clarsimp simp: is_aligned_def unat_minus word_size word_neq_0_conv) 800 apply (rule dvd_diff_nat, simp_all) 801 apply (rule le_imp_power_dvd) 802 apply (fold is_aligned_def) 803 apply (erule_tac Q="0<p" in contrapos_pp) 804 apply (clarsimp simp add: is_aligned_mask mask_def power_overflow) 805 done 806 807lemma add_mask_lower_bits: 808 "\<lbrakk>is_aligned (x :: 'a :: len word) n; 809 \<forall>n' \<ge> n. n' < LENGTH('a) \<longrightarrow> \<not> p !! n'\<rbrakk> \<Longrightarrow> x + p && ~~ (mask n) = x" 810 apply (subst word_plus_and_or_coroll) 811 apply (rule word_eqI) 812 apply (clarsimp simp: word_size is_aligned_nth) 813 apply (erule_tac x=na in allE)+ 814 apply simp 815 apply (rule word_eqI) 816 apply (clarsimp simp: word_size is_aligned_nth word_ops_nth_size le_def) 817 apply blast 818 done 819 820lemma is_aligned_andI1: 821 "is_aligned x n \<Longrightarrow> is_aligned (x && y) n" 822 by (simp add: is_aligned_nth) 823 824lemma is_aligned_andI2: 825 "is_aligned y n \<Longrightarrow> is_aligned (x && y) n" 826 by (simp add: is_aligned_nth) 827 828lemma is_aligned_shiftl: 829 "is_aligned w (n - m) \<Longrightarrow> is_aligned (w << m) n" 830 by (simp add: is_aligned_nth nth_shiftl) 831 832lemma is_aligned_shiftr: 833 "is_aligned w (n + m) \<Longrightarrow> is_aligned (w >> m) n" 834 by (simp add: is_aligned_nth nth_shiftr) 835 836lemma is_aligned_shiftl_self: 837 "is_aligned (p << n) n" 838 by (rule is_aligned_shift) 839 840lemma is_aligned_neg_mask_eq: 841 "is_aligned p n \<Longrightarrow> p && ~~ (mask n) = p" 842 by (metis add.left_neutral is_aligned_mask word_plus_and_or_coroll2) 843 844lemma is_aligned_shiftr_shiftl: 845 "is_aligned w n \<Longrightarrow> w >> n << n = w" 846 by (metis and_not_mask is_aligned_neg_mask_eq) 847 848lemma aligned_shiftr_mask_shiftl: 849 "is_aligned x n \<Longrightarrow> ((x >> n) && mask v) << n = x && mask (v + n)" 850 apply (rule word_eqI) 851 apply (simp add: word_size nth_shiftl nth_shiftr) 852 apply (subgoal_tac "\<forall>m. x !! m \<longrightarrow> m \<ge> n") 853 apply auto[1] 854 apply (clarsimp simp: is_aligned_mask) 855 apply (drule_tac x=m in word_eqD) 856 apply (frule test_bit_size) 857 apply (simp add: word_size) 858 done 859 860lemma mask_zero: 861 "is_aligned x a \<Longrightarrow> x && mask a = 0" 862 by (metis is_aligned_mask) 863 864lemma is_aligned_neg_mask_eq_concrete: 865 "\<lbrakk> is_aligned p n; msk && ~~(mask n) = ~~(mask n) \<rbrakk> 866 \<Longrightarrow> p && msk = p" 867 by (metis word_bw_assocs(1) word_bw_comms(1) is_aligned_neg_mask_eq) 868 869lemma is_aligned_and_not_zero: 870 "\<lbrakk> is_aligned n k; n \<noteq> 0 \<rbrakk> \<Longrightarrow> 2 ^ k \<le> n" 871 using is_aligned_less_sz leI by blast 872 873lemma is_aligned_and_2_to_k: 874 "(n && 2 ^ k - 1) = 0 \<Longrightarrow> is_aligned (n :: 'a :: len word) k" 875 by (simp add: is_aligned_mask mask_def) 876 877lemma is_aligned_power2: 878 "b \<le> a \<Longrightarrow> is_aligned (2 ^ a) b" 879 by (metis is_aligned_triv is_aligned_weaken) 880 881lemma aligned_sub_aligned': 882 "\<lbrakk> is_aligned (a :: 'a :: len word) n; is_aligned b n; n < LENGTH('a) \<rbrakk> 883 \<Longrightarrow> is_aligned (a - b) n" 884 by (simp add: aligned_sub_aligned) 885 886lemma is_aligned_neg_mask_weaken: 887 "\<lbrakk> is_aligned p n; m \<le> n \<rbrakk> \<Longrightarrow> p && ~~(mask m) = p" 888 using is_aligned_neg_mask_eq is_aligned_weaken by blast 889 890lemma is_aligned_neg_mask2[simp]: 891 "is_aligned (a && ~~(mask n)) n" 892 by (simp add: and_not_mask is_aligned_shift) 893 894end 895