1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7section "Lemmas for Word Length 32" 8 9theory Word_Lemmas_32 10imports 11 Word_Lemmas_Prefix 12 Word_Setup_32 13begin 14 15lemma ucast_8_32_inj: 16 "inj (ucast :: 8 word \<Rightarrow> 32 word)" 17 by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size) 18 19lemma upto_2_helper: 20 "{0..<2 :: 32 word} = {0, 1}" 21 by (safe; simp) unat_arith 22 23lemmas upper_bits_unset_is_l2p_32 = upper_bits_unset_is_l2p [where 'a=32, folded word_bits_def] 24lemmas le_2p_upper_bits_32 = le_2p_upper_bits [where 'a=32, folded word_bits_def] 25lemmas le2p_bits_unset_32 = le2p_bits_unset[where 'a=32, folded word_bits_def] 26 27lemma word_bits_len_of: 28 "len_of TYPE (32) = word_bits" 29 by (simp add: word_bits_conv) 30 31lemmas unat_power_lower32' = unat_power_lower[where 'a=32] 32lemmas unat_power_lower32 [simp] = unat_power_lower32'[unfolded word_bits_len_of] 33 34lemmas word32_less_sub_le' = word_less_sub_le[where 'a = 32] 35lemmas word32_less_sub_le[simp] = word32_less_sub_le' [folded word_bits_def] 36 37lemma word_bits_size: 38 "size (w::word32) = word_bits" 39 by (simp add: word_bits_def word_size) 40 41lemmas word32_power_less_1' = word_power_less_1[where 'a = 32] 42lemmas word32_power_less_1[simp] = word32_power_less_1'[folded word_bits_def] 43 44lemma of_nat32_0: 45 "\<lbrakk>of_nat n = (0::word32); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0" 46 by (erule of_nat_0, simp add: word_bits_def) 47 48lemma unat_mask_2_less_4: 49 "unat (p && mask 2 :: word32) < 4" 50 apply (rule unat_less_helper) 51 apply (rule order_le_less_trans, rule word_and_le1) 52 apply (simp add: mask_def) 53 done 54 55lemmas unat_of_nat32' = unat_of_nat_eq[where 'a=32] 56lemmas unat_of_nat32 = unat_of_nat32'[unfolded word_bits_len_of] 57 58lemmas word_power_nonzero_32 = word_power_nonzero [where 'a=32, folded word_bits_def] 59 60lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 32, unfolded word_bits_len_of]] 61 62lemmas div_power_helper_32 = div_power_helper [where 'a=32, folded word_bits_def] 63 64lemma n_less_word_bits: 65 "(n < word_bits) = (n < 32)" 66 by (simp add: word_bits_def) 67 68lemmas of_nat_less_pow_32 = of_nat_power [where 'a=32, folded word_bits_def] 69 70lemma lt_word_bits_lt_pow: 71 "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits" 72 by (simp add: word_bits_conv) 73 74lemma unat_less_word_bits: 75 fixes y :: word32 76 shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits" 77 unfolding word_bits_def 78 by (rule order_less_trans [OF _ unat_lt2p]) 79 80lemmas unat_mask_word32' = unat_mask[where 'a=32] 81lemmas unat_mask_word32 = unat_mask_word32'[folded word_bits_def] 82 83lemma unat_less_2p_word_bits: 84 "unat (x :: 32 word) < 2 ^ word_bits" 85 apply (simp only: word_bits_def) 86 apply (rule unat_lt2p) 87 done 88 89lemma Suc_unat_mask_div: 90 "Suc (unat (mask sz div word_size::word32)) = 2 ^ (min sz word_bits - 2)" 91 apply (case_tac "sz < word_bits") 92 apply (case_tac "2\<le>sz") 93 apply (clarsimp simp: word_size_def word_bits_def min_def mask_def) 94 apply (drule (2) Suc_div_unat_helper 95 [where 'a=32 and sz=sz and us=2, simplified, symmetric]) 96 apply (simp add: not_le word_size_def word_bits_def) 97 apply (case_tac sz, simp add: unat_word_ariths) 98 apply (case_tac nat, simp add: unat_word_ariths 99 unat_mask_word32 min_def word_bits_def) 100 apply simp 101 apply (simp add: unat_word_ariths 102 unat_mask_word32 min_def word_bits_def word_size_def) 103 done 104 105lemmas word32_minus_one_le' = word_minus_one_le[where 'a=32] 106lemmas word32_minus_one_le = word32_minus_one_le'[simplified] 107 108lemma ucast_not_helper: 109 fixes a::word8 110 assumes a: "a \<noteq> 0xFF" 111 shows "ucast a \<noteq> (0xFF::word32)" 112proof 113 assume "ucast a = (0xFF::word32)" 114 also 115 have "(0xFF::word32) = ucast (0xFF::word8)" by simp 116 finally 117 show False using a 118 apply - 119 apply (drule up_ucast_inj, simp) 120 apply simp 121 done 122qed 123 124lemma less_4_cases: 125 "(x::word32) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3" 126 apply clarsimp 127 apply (drule word_less_cases, erule disjE, simp, simp)+ 128 done 129 130lemma unat_ucast_8_32: 131 fixes x :: "word8" 132 shows "unat (ucast x :: word32) = unat x" 133 unfolding ucast_def unat_def 134 apply (subst int_word_uint) 135 apply (subst mod_pos_pos_trivial) 136 apply simp 137 apply (rule lt2p_lem) 138 apply simp 139 apply simp 140 done 141 142lemma if_then_1_else_0: 143 "((if P then 1 else 0) = (0 :: word32)) = (\<not> P)" 144 by simp 145 146lemma if_then_0_else_1: 147 "((if P then 0 else 1) = (0 :: word32)) = (P)" 148 by simp 149 150lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0 151 152lemma ucast_le_ucast_8_32: 153 "(ucast x \<le> (ucast y :: word32)) = (x \<le> (y :: word8))" 154 by (simp add: ucast_le_ucast) 155 156lemma in_16_range: 157 "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: word32)) ` S" 158 "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: word32. r + x * 16) ` S" 159 by (clarsimp simp: image_def elim!: bexI[rotated])+ 160 161lemma eq_2_32_0: 162 "(2 ^ 32 :: word32) = 0" 163 by simp 164 165lemma x_less_2_0_1: 166 fixes x :: word32 shows 167 "x < 2 \<Longrightarrow> x = 0 \<or> x = 1" 168 by (rule x_less_2_0_1') auto 169 170lemmas mask_32_max_word = max_word_mask [symmetric, where 'a=32, simplified] 171 172lemma of_nat32_n_less_equal_power_2: 173 "n < 32 \<Longrightarrow> ((of_nat n)::32 word) < 2 ^ n" 174 by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size) 175 176lemma word_rsplit_0: 177 "word_rsplit (0 :: word32) = [0, 0, 0, 0 :: word8]" 178 apply (simp add: word_rsplit_def bin_rsplit_def Let_def) 179 done 180 181lemma unat_ucast_10_32 : 182 fixes x :: "10 word" 183 shows "unat (ucast x :: word32) = unat x" 184 unfolding ucast_def unat_def 185 apply (subst int_word_uint) 186 apply (subst mod_pos_pos_trivial) 187 apply simp 188 apply (rule lt2p_lem) 189 apply simp 190 apply simp 191 done 192 193lemma bool_mask [simp]: 194 fixes x :: word32 195 shows "(0 < x && 1) = (x && 1 = 1)" 196 by (rule bool_mask') auto 197 198lemma word32_bounds: 199 "- (2 ^ (size (x :: word32) - 1)) = (-2147483648 :: int)" 200 "((2 ^ (size (x :: word32) - 1)) - 1) = (2147483647 :: int)" 201 "- (2 ^ (size (y :: 32 signed word) - 1)) = (-2147483648 :: int)" 202 "((2 ^ (size (y :: 32 signed word) - 1)) - 1) = (2147483647 :: int)" 203 by (simp_all add: word_size) 204 205lemma word_ge_min:"sint (x::32 word) \<ge> -2147483648" 206 by (metis sint_ge word32_bounds(1) word_size) 207 208lemmas signed_arith_ineq_checks_to_eq_word32' 209 = signed_arith_ineq_checks_to_eq[where 'a=32] 210 signed_arith_ineq_checks_to_eq[where 'a="32 signed"] 211 212lemmas signed_arith_ineq_checks_to_eq_word32 213 = signed_arith_ineq_checks_to_eq_word32' [unfolded word32_bounds] 214 215lemmas signed_mult_eq_checks32_to_64' 216 = signed_mult_eq_checks_double_size[where 'a=32 and 'b=64] 217 signed_mult_eq_checks_double_size[where 'a="32 signed" and 'b=64] 218 219lemmas signed_mult_eq_checks32_to_64 = signed_mult_eq_checks32_to_64'[simplified] 220 221lemmas sdiv_word32_max' = sdiv_word_max [where 'a=32] sdiv_word_max [where 'a="32 signed"] 222lemmas sdiv_word32_max = sdiv_word32_max'[simplified word_size, simplified] 223 224lemmas sdiv_word32_min' = sdiv_word_min [where 'a=32] sdiv_word_min [where 'a="32 signed"] 225lemmas sdiv_word32_min = sdiv_word32_min' [simplified word_size, simplified] 226 227lemmas sint32_of_int_eq' = sint_of_int_eq [where 'a=32] 228lemmas sint32_of_int_eq = sint32_of_int_eq' [simplified] 229 230lemma ucast_of_nats [simp]: 231 "(ucast (of_nat x :: word32) :: sword32) = (of_nat x)" 232 "(ucast (of_nat x :: word32) :: sword16) = (of_nat x)" 233 "(ucast (of_nat x :: word32) :: sword8) = (of_nat x)" 234 "(ucast (of_nat x :: word16) :: sword16) = (of_nat x)" 235 "(ucast (of_nat x :: word16) :: sword8) = (of_nat x)" 236 "(ucast (of_nat x :: word8) :: sword8) = (of_nat x)" 237 by (auto simp: ucast_of_nat is_down) 238 239lemmas signed_shift_guard_simpler_32' 240 = power_strict_increasing_iff[where b="2 :: nat" and y=31] 241lemmas signed_shift_guard_simpler_32 = signed_shift_guard_simpler_32'[simplified] 242 243lemma word32_31_less: 244 "31 < len_of TYPE (32 signed)" "31 > (0 :: nat)" 245 "31 < len_of TYPE (32)" "31 > (0 :: nat)" 246 by auto 247 248lemmas signed_shift_guard_to_word_32 249 = signed_shift_guard_to_word[OF word32_31_less(1-2)] 250 signed_shift_guard_to_word[OF word32_31_less(3-4)] 251 252lemma le_step_down_word_3: 253 fixes x :: "32 word" 254 shows "\<lbrakk>x \<le> y; x \<noteq> y; y < 2 ^ 32 - 1\<rbrakk> \<Longrightarrow> x \<le> y - 1" 255 by (rule le_step_down_word_2, assumption+) 256 257lemma shiftr_1: 258 "(x::word32) >> 1 = 0 \<Longrightarrow> x < 2" 259 by word_bitwise clarsimp 260 261lemma has_zero_byte: 262 "~~ (((((v::word32) && 0x7f7f7f7f) + 0x7f7f7f7f) || v) || 0x7f7f7f7f) \<noteq> 0 263 \<Longrightarrow> v && 0xff000000 = 0 \<or> v && 0xff0000 = 0 \<or> v && 0xff00 = 0 \<or> v && 0xff = 0" 264 apply clarsimp 265 apply word_bitwise 266 by metis 267 268lemma mask_step_down_32: 269 "(b::32word) && 0x1 = (1::32word) \<Longrightarrow> (\<exists>x. x < 32 \<and> mask x = b >> 1) \<Longrightarrow> (\<exists>x. mask x = b)" 270 apply clarsimp 271 apply (rule_tac x="x + 1" in exI) 272 apply (subgoal_tac "x \<le> 31") 273 apply (erule le_step_down_nat, clarsimp simp:mask_def, word_bitwise, clarsimp+)+ 274 apply (clarsimp simp:mask_def, word_bitwise, clarsimp) 275 apply clarsimp 276 done 277 278lemma unat_of_int_32: 279 "\<lbrakk>i \<ge> 0; i \<le>2 ^ 31\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword32)) = nat i" 280 unfolding unat_def 281 apply (subst eq_nat_nat_iff, clarsimp+) 282 apply (simp add: word_of_int uint_word_of_int) 283 done 284 285lemmas word_ctz_not_minus_1_32 = word_ctz_not_minus_1[where 'a=32, simplified] 286 287(* Helper for packing then unpacking a 64-bit variable. *) 288lemma cast_chunk_assemble_id_64[simp]: 289 "(((ucast ((ucast (x::64 word))::32 word))::64 word) || (((ucast ((ucast (x >> 32))::32 word))::64 word) << 32)) = x" 290 by (simp add:cast_chunk_assemble_id) 291 292(* Another variant of packing and unpacking a 64-bit variable. *) 293lemma cast_chunk_assemble_id_64'[simp]: 294 "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x" 295 by (simp add:cast_chunk_scast_assemble_id) 296 297(* Specialisations of down_cast_same for adding to local simpsets. *) 298lemma cast_down_u64: "(scast::64 word \<Rightarrow> 32 word) = (ucast::64 word \<Rightarrow> 32 word)" 299 apply (subst down_cast_same[symmetric]) 300 apply (simp add:is_down)+ 301 done 302 303lemma cast_down_s64: "(scast::64 sword \<Rightarrow> 32 word) = (ucast::64 sword \<Rightarrow> 32 word)" 304 apply (subst down_cast_same[symmetric]) 305 apply (simp add:is_down)+ 306 done 307 308end 309