1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7section "L4V-Internal Word Lemmas" 8 9text \<open> 10 This is a holding area for Word utility lemmas that are too specific or unpolished for the 11 AFP, but which are reusable enough to be collected together for the rest of L4V. New 12 utility lemmas that only prove facts about words should be added here (in preference to being 13 kept where they were first needed). 14\<close> 15 16theory Word_Lemmas_Internal 17imports Word_Lemmas 18begin 19 20lemma signed_ge_zero_scast_eq_ucast: 21 "0 <=s x \<Longrightarrow> scast x = ucast x" 22 by (simp add: scast_eq_ucast word_sle_msb_le) 23 24(* FIXME: move out of Word_Lib *) 25lemma disjCI2: 26 "(\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q" 27 by blast 28 29(* FIXME: move out of Word_Lib *) 30lemma nat_diff_diff_le_lhs: 31 "a + c - b \<le> d \<Longrightarrow> a - (b - c) \<le> (d :: nat)" 32 by arith 33 34lemma is_aligned_obvious_no_wrap': 35 "\<lbrakk> is_aligned ptr sz; x = 2 ^ sz - 1 \<rbrakk> 36 \<Longrightarrow> ptr \<le> ptr + x" 37 by (fastforce simp: field_simps intro: is_aligned_no_overflow) 38 39lemmas add_ge0_weak = add_increasing[where 'a=int and b=0] 40 41lemmas aligned_sub_aligned = Aligned.aligned_sub_aligned' 42 43lemma minus_minus_swap: 44 "\<lbrakk> a \<le> c; b \<le> d; b \<le> a; d \<le> c ; (d :: nat) - b = c - a \<rbrakk> 45 \<Longrightarrow> a - b = c - d" 46 by arith 47 48lemma minus_minus_swap': 49 "\<lbrakk> c \<le> a; d \<le> b; b \<le> a; d \<le> c ; (b :: nat) - d = a - c \<rbrakk> 50 \<Longrightarrow> a - b = c - d" 51 by arith 52 53lemmas word_le_mask_eq = le_mask_imp_and_mask 54 55lemma int_and_leR: 56 "0 \<le> b \<Longrightarrow> a AND b \<le> (b :: int)" 57 by (rule AND_upper2) 58 59lemma int_and_leL: 60 "0 \<le> a \<Longrightarrow> a AND b \<le> (a :: int)" 61 by (rule AND_upper1) 62 63lemma if_then_1_else_0: 64 "(if P then 1 else 0) = (0 :: 'a :: zero_neq_one) \<longleftrightarrow> \<not>P" 65 by (simp split: if_split) 66 67lemma if_then_0_else_1: 68 "(if P then 0 else 1) = (0 :: 'a :: zero_neq_one) \<longleftrightarrow> P" 69 by simp 70 71lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0 72 73lemma createNewCaps_guard: 74 fixes x :: "'a :: len word" 75 shows "\<lbrakk> unat x = c; b < 2 ^ LENGTH('a) \<rbrakk> 76 \<Longrightarrow> (n < of_nat b \<and> n < x) = (n < of_nat (min (min b c) c))" 77 apply (erule subst) 78 apply (simp add: min.assoc) 79 apply (rule iffI) 80 apply (simp add: min_def word_less_nat_alt split: if_split) 81 apply (simp add: min_def word_less_nat_alt not_le le_unat_uoi split: if_split_asm) 82 by (simp add: of_nat_inverse) 83 84lemma bits_2_subtract_ineq: 85 "i < (n :: ('a :: len) word) 86 \<Longrightarrow> 2 ^ bits + 2 ^ bits * unat (n - (1 + i)) = unat (n - i) * 2 ^ bits" 87 apply (simp add: unat_sub word_minus_one_le_leq) 88 apply (subst unatSuc) 89 apply clarsimp 90 apply unat_arith 91 apply (simp only: mult_Suc_right[symmetric]) 92 apply (rule trans[OF mult.commute], rule arg_cong2[where f="(*)"], simp_all) 93 apply (simp add: word_less_nat_alt) 94 done 95 96lemmas double_neg_mask = neg_mask_combine 97 98lemmas int_unat = uint_nat[symmetric] 99 100lemmas word_sub_mono3 = word_plus_mcs_4' 101 102lemma shift_distinct_helper: 103 "\<lbrakk> (x :: 'a :: len word) < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 104 bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 \<rbrakk> 105 \<Longrightarrow> P" 106 apply (cases "n = 0") 107 apply simp 108 apply (drule word_plus_mono_right[where x=1]) 109 apply simp_all 110 apply (subst word_le_sub1) 111 apply (rule power_not_zero) 112 apply simp 113 apply simp 114 apply (drule(1) order_less_le_trans)+ 115 apply (clarsimp simp: bang_eq) 116 apply (drule_tac x="na + n" in spec) 117 apply (simp add: nth_shiftl) 118 apply (case_tac "na + n < LENGTH('a)", simp_all) 119 apply safe 120 apply (drule(1) nth_bounded) 121 apply simp 122 apply simp 123 apply (drule(1) nth_bounded) 124 apply simp 125 apply simp 126 done 127 128lemma of_nat_shift_distinct_helper: 129 "\<lbrakk> x < bnd; y < bnd; x \<noteq> y; (of_nat x :: 'a :: len word) << n = of_nat y << n; 130 n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n) \<rbrakk> 131 \<Longrightarrow> P" 132 apply (cases "n = 0") 133 apply (simp add: word_unat.Abs_inject unats_def) 134 apply (subgoal_tac "bnd < 2 ^ LENGTH('a)") 135 apply (erule(1) shift_distinct_helper[rotated, rotated, rotated]) 136 defer 137 apply (erule(1) of_nat_mono_maybe[rotated]) 138 apply (erule(1) of_nat_mono_maybe[rotated]) 139 apply (simp add: word_unat.Abs_inject unats_def) 140 apply (erule order_le_less_trans) 141 apply (rule power_strict_increasing) 142 apply simp 143 apply simp 144 apply (simp add: word_less_nat_alt) 145 apply (simp add: unat_minus_one [OF of_nat_neq_0] 146 word_unat.Abs_inverse unats_def) 147 done 148 149lemmas pre_helper2 = add_mult_in_mask_range[folded add_mask_fold] 150 151lemma ptr_add_distinct_helper: 152 "\<lbrakk> ptr_add (p :: 'a :: len word) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \<noteq> y; 153 x < bnd; y < bnd; n < LENGTH('a); 154 bnd \<le> 2 ^ (LENGTH('a) - n) \<rbrakk> 155 \<Longrightarrow> P" 156 apply (clarsimp simp: ptr_add_def word_unat_power[symmetric] 157 shiftl_t2n[symmetric, simplified mult.commute]) 158 using of_nat_shift_distinct_helper 159 by blast 160 161lemma unat_sub_le_strg: 162 "unat v \<le> v2 \<and> x \<le> v \<and> y \<le> v \<and> y < (x :: ('a :: len) word) 163 \<longrightarrow> unat (x + (- 1 - y)) \<le> v2" 164 apply clarsimp 165 apply (erule order_trans[rotated]) 166 apply (fold word_le_nat_alt) 167 apply (rule order_trans[rotated], assumption) 168 apply (rule order_trans[rotated], rule word_sub_le[where y="y + 1"]) 169 apply (erule Word.inc_le) 170 apply (simp add: field_simps) 171 done 172 173lemma multi_lessD: 174 "\<lbrakk> (a :: nat) * b < c; 0 < a; 0 < b \<rbrakk> 175 \<Longrightarrow> a < c \<and> b < c" 176 by (cases a, simp_all,cases b,simp_all) 177 178lemmas leq_high_bits_shiftr_low_bits_leq_bits = 179 leq_high_bits_shiftr_low_bits_leq_bits_mask[unfolded mask_2pm1[of high_bits]] 180 181lemmas unat_le_helper = word_unat_less_le 182 183lemmas word_of_nat_plus = of_nat_add[where 'a="'a :: len word"] 184lemmas word_of_nat_minus = of_nat_diff[where 'a="'a :: len word"] 185 186(* this is a bit deceptive: 2 ^ len.. = 0, so really this is relying on 'word_n1_ge': ptr \<le> -1 *) 187lemma word_up_bound: 188 "(ptr :: 'a :: len word) \<le> 2 ^ LENGTH('a) - 1 " 189 by auto 190 191lemma base_length_minus_one_inequality: 192 assumes foo: "wbase \<le> 2 ^ sz - 1" 193 "1 \<le> (wlength :: ('a :: len) word)" 194 "wlength \<le> 2 ^ sz - wbase" 195 "sz < LENGTH ('a)" 196 shows "wbase \<le> wbase + wlength - 1" 197proof - 198 199 note sz_less = power_strict_increasing[OF foo(4), where a=2] 200 201 from foo have plus: "unat wbase + unat wlength < 2 ^ LENGTH('a)" 202 apply - 203 apply (rule order_le_less_trans[rotated], rule sz_less, simp) 204 apply (simp add: unat_arith_simps split: if_split_asm) 205 done 206 207 from foo show ?thesis 208 by (simp add: unat_arith_simps plus) 209qed 210 211lemmas from_bool_to_bool_and_1 = from_to_bool_last_bit[where x=r for r] 212 213lemmas max_word_neq_0 = max_word_not_0 214 215lemmas word_le_p2m1 = word_up_bound[where ptr=w for w] 216 217lemma inj_ucast: 218 "\<lbrakk> uc = ucast; is_up uc \<rbrakk> 219 \<Longrightarrow> inj uc" 220 using down_ucast_inj is_up_down by blast 221 222lemma ucast_eq_0[OF refl]: 223 "\<lbrakk> c = ucast; is_up c \<rbrakk> 224 \<Longrightarrow> (c x = 0) = (x = 0)" 225 by (metis uint_0_iff uint_up_ucast) 226 227lemmas is_up_compose' = is_up_compose 228 229lemma uint_is_up_compose: 230 fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word" 231 and uc' :: "'b word \<Rightarrow> 'c :: len sword" 232 assumes "uc = ucast" 233 and "uc' = ucast" 234 and " uuc = uc' \<circ> uc" 235 shows "\<lbrakk> is_up uc; is_up uc' \<rbrakk> 236 \<Longrightarrow> uint (uuc b) = uint b" 237 apply (simp add: assms) 238 apply (frule is_up_compose) 239 apply (simp_all ) 240 apply (simp only: Word.uint_up_ucast) 241 done 242 243lemma uint_is_up_compose_pred: 244 fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word" 245 and uc' :: "'b word \<Rightarrow> 'c :: len sword" 246 assumes "uc = ucast" and "uc' = ucast" and " uuc = uc' \<circ> uc" 247 shows "\<lbrakk> is_up uc; is_up uc' \<rbrakk> 248 \<Longrightarrow> P (uint (uuc b)) \<longleftrightarrow> P( uint b)" 249 apply (simp add: assms) 250 apply (frule is_up_compose) 251 apply (simp_all ) 252 apply (simp only: Word.uint_up_ucast) 253 done 254 255lemma is_down_up_sword: 256 fixes uc :: "'a :: len word \<Rightarrow> 'b :: len sword" 257 shows "\<lbrakk> uc = ucast; LENGTH('a) < LENGTH('b) \<rbrakk> 258 \<Longrightarrow> is_up uc = (\<not> is_down uc)" 259 by (simp add: target_size source_size is_up_def is_down_def ) 260 261lemma is_not_down_compose: 262 fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word" 263 and uc' :: "'b word \<Rightarrow> 'c :: len sword" 264 shows "\<lbrakk> uc = ucast; uc' = ucast; LENGTH('a) < LENGTH('c) \<rbrakk> 265 \<Longrightarrow> \<not> is_down (uc' \<circ> uc)" 266 unfolding is_down_def 267 by (simp add: Word.target_size Word.source_size) 268 269lemma sint_ucast_uint: 270 fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word" 271 and uc' :: "'b word \<Rightarrow> 'c :: len sword" 272 assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc " 273 and "LENGTH('a) < LENGTH('c signed)" 274 shows "\<lbrakk> is_up uc; is_up uc'\<rbrakk> 275 \<Longrightarrow> sint (uuc b) = uint b" 276 apply (simp add: assms) 277 apply (frule is_up_compose') 278 apply simp_all 279 apply (simp add: ucast_ucast_b) 280 apply (rule sint_ucast_eq_uint) 281 apply (insert assms) 282 apply (simp add: is_down_def target_size source_size) 283 done 284 285lemma sint_ucast_uint_pred: 286 fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word" 287 and uc' :: "'b word \<Rightarrow> 'c :: len sword" 288 and uuc :: "'a word \<Rightarrow> 'c sword" 289 assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc " 290 and "LENGTH('a) < LENGTH('c )" 291 shows "\<lbrakk> is_up uc; is_up uc' \<rbrakk> 292 \<Longrightarrow> P (uint b) \<longleftrightarrow> P (sint (uuc b))" 293 apply (simp add: assms ) 294 apply (insert sint_ucast_uint[where uc=uc and uc'=uc' and uuc=uuc and b = b]) 295 apply (simp add: assms) 296 done 297 298lemma sint_uucast_uint_uucast_pred: 299 fixes uc :: "'a :: len word \<Rightarrow> 'b :: len word" 300 and uc' :: "'b word \<Rightarrow> 'c :: len sword" 301 assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc " 302 and "LENGTH('a) < LENGTH('c )" 303 shows "\<lbrakk> is_up uc; is_up uc' \<rbrakk> 304 \<Longrightarrow> P (uint(uuc b)) \<longleftrightarrow> P (sint (uuc b))" 305 apply (simp add: assms ) 306 apply (insert sint_ucast_uint[where uc=uc and uc'=uc' and uuc=uuc and b = b]) 307 apply (insert uint_is_up_compose_pred[where uc=uc and uc'=uc' and uuc=uuc and b=b]) 308 apply (simp add: assms uint_is_up_compose_pred) 309 done 310 311lemma unat_minus': 312 fixes x :: "'a :: len word" 313 shows "x \<noteq> 0 \<Longrightarrow> unat (-x) = 2 ^ LENGTH('a) - unat x" 314 by (simp add: unat_minus wsst_TYs(3)) 315 316lemma word_nth_neq: 317 "n < LENGTH('a) \<Longrightarrow> (~~ x :: 'a :: len word) !! n = (\<not> x !! n)" 318 by (simp add: word_size word_ops_nth_size) 319 320lemma word_wrap_of_natD: 321 fixes x :: "'a :: len word" 322 assumes wraps: "\<not> x \<le> x + of_nat n" 323 shows "\<exists>k. x + of_nat k = 0 \<and> k \<le> n" 324proof - 325 show ?thesis 326 proof (rule exI [where x = "unat (- x)"], intro conjI) 327 show "x + of_nat (unat (-x)) = 0" 328 by simp 329 next 330 show "unat (-x) \<le> n" 331 proof (subst unat_minus') 332 from wraps show "x \<noteq> 0" 333 by (rule contrapos_pn, simp add: not_le) 334 next 335 show "2 ^ LENGTH('a) - unat x \<le> n" using wraps 336 apply (simp add: no_olen_add_nat le_diff_conv not_less) 337 apply (erule order_trans) 338 apply (simp add: unat_of_nat) 339 done 340 qed 341 qed 342qed 343 344lemma two_bits_cases: 345 "\<lbrakk> LENGTH('a) > 2; (x :: 'a :: len word) && 3 = 0 \<Longrightarrow> P; x && 3 = 1 \<Longrightarrow> P; 346 x && 3 = 2 \<Longrightarrow> P; x && 3 = 3 \<Longrightarrow> P \<rbrakk> 347 \<Longrightarrow> P" 348 apply (frule and_mask_cases[where n=2 and x=x, simplified mask_def]) 349 using upt_conv_Cons by auto[1] 350 351lemma zero_OR_eq: 352 "y = 0 \<Longrightarrow> (x || y) = x" 353 by simp 354 355declare is_aligned_neg_mask_eq[simp] 356declare is_aligned_neg_mask_weaken[simp] 357 358lemmas mask_in_range = neg_mask_in_mask_range[folded add_mask_fold] 359lemmas aligned_range_offset_mem = aligned_offset_in_range[folded add_mask_fold] 360lemmas range_to_bl' = mask_range_to_bl'[folded add_mask_fold] 361lemmas range_to_bl = mask_range_to_bl[folded add_mask_fold] 362lemmas aligned_ranges_subset_or_disjoint = aligned_mask_range_cases[folded add_mask_fold] 363lemmas aligned_range_offset_subset = aligned_mask_range_offset_subset[folded add_mask_fold] 364lemmas aligned_diff = aligned_mask_diff[unfolded mask_2pm1] 365lemmas aligned_ranges_subset_or_disjoint_coroll = aligned_mask_ranges_disjoint[folded add_mask_fold] 366lemmas distinct_aligned_addresses_accumulate = aligned_mask_ranges_disjoint2[folded add_mask_fold] 367 368lemmas bang_big = test_bit_over 369 370lemma unat_and_mask_le: 371 fixes x::"'a::len word" 372 assumes "n < LENGTH('a)" 373 shows "unat (x && mask n) \<le> 2^n" 374proof - 375 from assms 376 have "2^n-1 \<le> (2^n :: 'a word)" 377 using word_1_le_power word_le_imp_diff_le by blast 378 then 379 have "unat (x && mask n) \<le> unat (2^n::'a word)" 380 apply (fold word_le_nat_alt) 381 apply (rule order_trans, rule word_and_le1) 382 apply (simp add: mask_def) 383 done 384 with assms 385 show ?thesis by (simp add: unat_2tp_if) 386qed 387 388lemma sign_extend_less_mask_idem: 389 "\<lbrakk> w \<le> mask n; n < size w \<rbrakk> \<Longrightarrow> sign_extend n w = w" 390 apply (simp add: sign_extend_def le_mask_imp_and_mask) 391 apply (simp add: le_mask_high_bits) 392 done 393 394lemma word_and_le: 395 "a \<le> c \<Longrightarrow> (a :: 'a :: len word) && b \<le> c" 396 by (subst word_bool_alg.conj.commute) 397 (erule word_and_le') 398 399lemma le_smaller_mask: 400 "\<lbrakk> x \<le> mask n; n \<le> m \<rbrakk> \<Longrightarrow> x \<le> mask m" 401 by (erule (1) order.trans[OF _ mask_mono]) 402 403(* The strange phrasing and ordering of assumptions is to support using this as a 404 conditional simp rule when y is a concrete value. For example, as a simp rule, 405 it will solve a goal of the form: 406 UCAST(8 \<rightarrow> 32) x < 0x20 \<Longrightarrow> unat x < 32 407 This is used in an obscure corner of SimplExportAndRefine. *) 408lemma upcast_less_unat_less: 409 assumes less: "UCAST('a \<rightarrow> 'b) x < UCAST('a \<rightarrow> 'b) (of_nat y)" 410 assumes len: "LENGTH('a::len) \<le> LENGTH('b::len)" 411 assumes bound: "y < 2 ^ LENGTH('a)" 412 shows "unat x < y" 413 by (rule unat_mono[OF less, simplified unat_ucast_up_simp[OF len] unat_of_nat_eq[OF bound]]) 414 415end 416