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 64" 8 9theory Word_Lemmas_64 10imports 11 Word_Lemmas_Prefix 12 Word_Setup_64 13begin 14 15lemma ucast_8_64_inj: 16 "inj (ucast :: 8 word \<Rightarrow> 64 word)" 17 by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size) 18 19lemma upto_2_helper: 20 "{0..<2 :: 64 word} = {0, 1}" 21 by (safe; simp) unat_arith 22 23lemmas upper_bits_unset_is_l2p_64 = upper_bits_unset_is_l2p [where 'a=64, folded word_bits_def] 24lemmas le_2p_upper_bits_64 = le_2p_upper_bits [where 'a=64, folded word_bits_def] 25lemmas le2p_bits_unset_64 = le2p_bits_unset[where 'a=64, folded word_bits_def] 26 27lemma word_bits_len_of: 28 "len_of TYPE (64) = word_bits" 29 by (simp add: word_bits_conv) 30 31lemmas unat_power_lower64' = unat_power_lower[where 'a=64] 32lemmas unat_power_lower64 [simp] = unat_power_lower64'[unfolded word_bits_len_of] 33 34lemmas word64_less_sub_le' = word_less_sub_le[where 'a = 64] 35lemmas word64_less_sub_le[simp] = word64_less_sub_le' [folded word_bits_def] 36 37lemma word_bits_size: 38 "size (w::word64) = word_bits" 39 by (simp add: word_bits_def word_size) 40 41lemmas word64_power_less_1' = word_power_less_1[where 'a = 64] 42lemmas word64_power_less_1[simp] = word64_power_less_1'[folded word_bits_def] 43 44lemma of_nat64_0: 45 "\<lbrakk>of_nat n = (0::word64); 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 :: word64) < 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_nat64' = unat_of_nat_eq[where 'a=64] 56lemmas unat_of_nat64 = unat_of_nat64'[unfolded word_bits_len_of] 57 58lemmas word_power_nonzero_64 = word_power_nonzero [where 'a=64, folded word_bits_def] 59 60lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 64, unfolded word_bits_len_of]] 61 62lemmas div_power_helper_64 = div_power_helper [where 'a=64, folded word_bits_def] 63 64lemma n_less_word_bits: 65 "(n < word_bits) = (n < 64)" 66 by (simp add: word_bits_def) 67 68lemmas of_nat_less_pow_64 = of_nat_power [where 'a=64, 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 :: word64 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_word64' = unat_mask[where 'a=64] 81lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def] 82 83lemma unat_less_2p_word_bits: 84 "unat (x :: 64 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::word64)) = 2 ^ (min sz word_bits - 3)" 91 apply (case_tac "sz < word_bits") 92 apply (case_tac "3\<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=64 and sz=sz and us=3, 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_word64 min_def word_bits_def) 100 apply (case_tac nata, simp add: unat_word_ariths unat_mask_word64 word_bits_def) 101 apply simp 102 apply (simp add: unat_word_ariths 103 unat_mask_word64 min_def word_bits_def word_size_def) 104 done 105 106lemmas word64_minus_one_le' = word_minus_one_le[where 'a=64] 107lemmas word64_minus_one_le = word64_minus_one_le'[simplified] 108 109lemma ucast_not_helper: 110 fixes a::word8 111 assumes a: "a \<noteq> 0xFF" 112 shows "ucast a \<noteq> (0xFF::word64)" 113proof 114 assume "ucast a = (0xFF::word64)" 115 also 116 have "(0xFF::word64) = ucast (0xFF::word8)" by simp 117 finally 118 show False using a 119 apply - 120 apply (drule up_ucast_inj, simp) 121 apply simp 122 done 123qed 124 125lemma less_4_cases: 126 "(x::word64) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3" 127 apply clarsimp 128 apply (drule word_less_cases, erule disjE, simp, simp)+ 129 done 130 131lemma if_then_1_else_0: 132 "((if P then 1 else 0) = (0 :: word64)) = (\<not> P)" 133 by simp 134 135lemma if_then_0_else_1: 136 "((if P then 0 else 1) = (0 :: word64)) = (P)" 137 by simp 138 139lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0 140 141lemma ucast_le_ucast_8_64: 142 "(ucast x \<le> (ucast y :: word64)) = (x \<le> (y :: word8))" 143 by (simp add: ucast_le_ucast) 144 145lemma in_16_range: 146 "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: word64)) ` S" 147 "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: word64. r + x * 16) ` S" 148 by (clarsimp simp: image_def elim!: bexI[rotated])+ 149 150lemma eq_2_64_0: 151 "(2 ^ 64 :: word64) = 0" 152 by simp 153 154lemma x_less_2_0_1: 155 fixes x :: word64 shows 156 "x < 2 \<Longrightarrow> x = 0 \<or> x = 1" 157 by (rule x_less_2_0_1') auto 158 159lemmas mask_64_max_word = max_word_mask [symmetric, where 'a=64, simplified] 160 161lemma of_nat64_n_less_equal_power_2: 162 "n < 64 \<Longrightarrow> ((of_nat n)::64 word) < 2 ^ n" 163 by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size) 164 165lemma word_rsplit_0: 166 "word_rsplit (0 :: word64) = [0, 0, 0, 0, 0, 0, 0, 0 :: word8]" 167 apply (simp add: word_rsplit_def bin_rsplit_def Let_def) 168 done 169 170lemma unat_ucast_10_64 : 171 fixes x :: "10 word" 172 shows "unat (ucast x :: word64) = unat x" 173 unfolding ucast_def unat_def 174 apply (subst int_word_uint) 175 apply (subst mod_pos_pos_trivial) 176 apply simp 177 apply (rule lt2p_lem) 178 apply simp 179 apply simp 180 done 181 182lemma bool_mask [simp]: 183 fixes x :: word64 184 shows "(0 < x && 1) = (x && 1 = 1)" 185 by (rule bool_mask') auto 186 187lemma word64_bounds: 188 "- (2 ^ (size (x :: word64) - 1)) = (-9223372036854775808 :: int)" 189 "((2 ^ (size (x :: word64) - 1)) - 1) = (9223372036854775807 :: int)" 190 "- (2 ^ (size (y :: 64 signed word) - 1)) = (-9223372036854775808 :: int)" 191 "((2 ^ (size (y :: 64 signed word) - 1)) - 1) = (9223372036854775807 :: int)" 192 by (simp_all add: word_size) 193 194lemma word_ge_min:"sint (x::64 word) \<ge> -9223372036854775808" 195 by (metis sint_ge word64_bounds(1) word_size) 196 197lemmas signed_arith_ineq_checks_to_eq_word64' 198 = signed_arith_ineq_checks_to_eq[where 'a=64] 199 signed_arith_ineq_checks_to_eq[where 'a="64 signed"] 200 201lemmas signed_arith_ineq_checks_to_eq_word64 202 = signed_arith_ineq_checks_to_eq_word64' [unfolded word64_bounds] 203 204lemmas signed_mult_eq_checks64_to_64' 205 = signed_mult_eq_checks_double_size[where 'a=64 and 'b=64] 206 signed_mult_eq_checks_double_size[where 'a="64 signed" and 'b=64] 207 208lemmas signed_mult_eq_checks64_to_64 = signed_mult_eq_checks64_to_64'[simplified] 209 210lemmas sdiv_word64_max' = sdiv_word_max [where 'a=64] sdiv_word_max [where 'a="64 signed"] 211lemmas sdiv_word64_max = sdiv_word64_max'[simplified word_size, simplified] 212 213lemmas sdiv_word64_min' = sdiv_word_min [where 'a=64] sdiv_word_min [where 'a="64 signed"] 214lemmas sdiv_word64_min = sdiv_word64_min' [simplified word_size, simplified] 215 216lemmas sint64_of_int_eq' = sint_of_int_eq [where 'a=64] 217lemmas sint64_of_int_eq = sint64_of_int_eq' [simplified] 218 219lemma ucast_of_nats [simp]: 220 "(ucast (of_nat x :: word64) :: sword64) = (of_nat x)" 221 "(ucast (of_nat x :: word64) :: sword16) = (of_nat x)" 222 "(ucast (of_nat x :: word64) :: sword8) = (of_nat x)" 223 "(ucast (of_nat x :: word16) :: sword16) = (of_nat x)" 224 "(ucast (of_nat x :: word16) :: sword8) = (of_nat x)" 225 "(ucast (of_nat x :: word8) :: sword8) = (of_nat x)" 226 by (auto simp: ucast_of_nat is_down) 227 228lemmas signed_shift_guard_simpler_64' 229 = power_strict_increasing_iff[where b="2 :: nat" and y=31] 230lemmas signed_shift_guard_simpler_64 = signed_shift_guard_simpler_64'[simplified] 231 232lemma word64_31_less: 233 "31 < len_of TYPE (64 signed)" "31 > (0 :: nat)" 234 "31 < len_of TYPE (64)" "31 > (0 :: nat)" 235 by auto 236 237lemmas signed_shift_guard_to_word_64 238 = signed_shift_guard_to_word[OF word64_31_less(1-2)] 239 signed_shift_guard_to_word[OF word64_31_less(3-4)] 240 241lemma le_step_down_word_3: 242 fixes x :: "64 word" 243 shows "\<lbrakk>x \<le> y; x \<noteq> y; y < 2 ^ 64 - 1\<rbrakk> \<Longrightarrow> x \<le> y - 1" 244 by (rule le_step_down_word_2, assumption+) 245 246lemma shiftr_1: 247 "(x::word64) >> 1 = 0 \<Longrightarrow> x < 2" 248 by word_bitwise clarsimp 249 250lemma mask_step_down_64: 251 "(b::64word) && 0x1 = (1::64word) \<Longrightarrow> (\<exists>x. x < 64 \<and> mask x = b >> 1) \<Longrightarrow> (\<exists>x. mask x = b)" 252 apply clarsimp 253 apply (rule_tac x="x + 1" in exI) 254 apply (subgoal_tac "x \<le> 63") 255 apply (erule le_step_down_nat, clarsimp simp:mask_def, word_bitwise, clarsimp+)+ 256 apply (clarsimp simp:mask_def, word_bitwise, clarsimp) 257 apply clarsimp 258 done 259 260lemma unat_of_int_64: 261 "\<lbrakk>i \<ge> 0; i \<le> 2 ^ 63\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword64)) = nat i" 262 unfolding unat_def 263 apply (subst eq_nat_nat_iff, clarsimp+) 264 apply (simp add: word_of_int uint_word_of_int) 265 done 266 267lemmas word_ctz_not_minus_1_64 = word_ctz_not_minus_1[where 'a=64, simplified] 268 269(* Helper for packing then unpacking a 64-bit variable. *) 270lemma cast_chunk_assemble_id_64[simp]: 271 "(((ucast ((ucast (x::64 word))::32 word))::64 word) || (((ucast ((ucast (x >> 32))::32 word))::64 word) << 32)) = x" 272 by (simp add:cast_chunk_assemble_id) 273 274(* Another variant of packing and unpacking a 64-bit variable. *) 275lemma cast_chunk_assemble_id_64'[simp]: 276 "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x" 277 by (simp add:cast_chunk_scast_assemble_id) 278 279(* Specialisations of down_cast_same for adding to local simpsets. *) 280lemma cast_down_u64: "(scast::64 word \<Rightarrow> 32 word) = (ucast::64 word \<Rightarrow> 32 word)" 281 apply (subst down_cast_same[symmetric]) 282 apply (simp add:is_down)+ 283 done 284 285lemma cast_down_s64: "(scast::64 sword \<Rightarrow> 32 word) = (ucast::64 sword \<Rightarrow> 32 word)" 286 apply (subst down_cast_same[symmetric]) 287 apply (simp add:is_down)+ 288 done 289 290end 291