1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Word_Lemmas_32_Internal 8imports Word_Lemmas_32 9begin 10 11lemmas sint_eq_uint_32 = sint_eq_uint_2pl[where 'a=32, simplified] 12 13lemmas sle_positive_32 = sle_le_2pl[where 'a=32, simplified] 14 15lemmas sless_positive_32 = sless_less_2pl[where 'a=32, simplified] 16 17lemma zero_le_sint_32: 18 "\<lbrakk> 0 \<le> (a :: word32); a < 0x80000000 \<rbrakk> 19 \<Longrightarrow> 0 \<le> sint a" 20 by (clarsimp simp: sint_eq_uint_32 unat_less_helper) 21 22lemmas unat_add_simple = iffD1[OF unat_add_lem[where 'a = 32, folded word_bits_def]] 23 24lemma upto_enum_inc_1: 25 "a < 2 ^ word_bits - 1 26 \<Longrightarrow> [(0:: 'a :: len word) .e. 1 + a] = [0.e.a] @ [(1+a)]" 27 using upper_trivial upto_enum_inc_1_len by force 28 29lemmas upt_enum_offset_trivial = 30 upt_enum_offset_trivial[where 'a=32, folded word_bits_def] 31 32lemmas unat32_eq_of_nat = unat_eq_of_nat[where 'a=32, folded word_bits_def] 33 34declare mask_32_max_word[simp] 35 36lemma le_32_mask_eq: 37 "(bits :: word32) \<le> 32 \<Longrightarrow> bits && mask 6 = bits" 38 by (fastforce elim: le_less_trans intro: less_mask_eq) 39 40lemmas scast_1_32[simp] = scast_1[where 'a=32] 41 42lemmas mask_32_id[simp] = mask_len_id[where 'a=32, folded word_bits_def] 43 44lemmas t2p_shiftr_32 = t2p_shiftr[where 'a=32, folded word_bits_def] 45 46lemma mask_eq1_nochoice: 47 "(x :: word32) && 1 = x 48 \<Longrightarrow> x = 0 \<or> x = 1" 49 using mask_eq1_nochoice len32 by force 50 51lemmas const_le_unat_word_32 = const_le_unat[where 'a=32, folded word_bits_def] 52 53lemmas createNewCaps_guard_helper = 54 createNewCaps_guard[where 'a=32, folded word_bits_def] 55 56lemma word_log2_max_word32[simp]: 57 "word_log2 (w :: 32 word) < 32" 58 using word_log2_max[where w=w] 59 by (simp add: word_size) 60 61(* FIXME: specialize using pow_sub_less_word *) 62lemma mapping_two_power_16_64_inequality: 63 assumes sz: "sz \<le> 4" and len: "unat (len :: word32) = 2 ^ sz" 64 shows "unat (len * 8 - 1) \<le> 127" 65 using pow_sub_less[where 'a=32 and b=3, simplified] 66proof - 67 have len2: "len = 2 ^ sz" 68 apply (rule word_unat.Rep_eqD, simp only: len) 69 using sz 70 apply simp 71 done 72 73 show ?thesis using two_power_increasing_less_1[where 'a=32 and n="sz + 3" and m=7] 74 by (simp add: word_le_nat_alt sz power_add len2 field_simps) 75qed 76 77lemmas pre_helper2_32 = pre_helper2[where 'a=32, folded word_bits_def] 78 79lemmas of_nat_shift_distinct_helper_machine = 80 of_nat_shift_distinct_helper[where 'a=32, folded word_bits_def] 81 82lemmas ptr_add_distinct_helper_32 = 83 ptr_add_distinct_helper[where 'a=32, folded word_bits_def] 84 85lemmas mask_out_eq_0_32 = mask_out_eq_0[where 'a=32, folded word_bits_def] 86 87lemmas neg_mask_mask_unat_32 = neg_mask_mask_unat[where 'a=32, folded word_bits_def] 88 89lemmas unat_less_iff_32 = unat_less_iff[where 'a=32, folded word_bits_def] 90 91lemmas is_aligned_no_overflow3_32 = is_aligned_no_overflow3[where 'a=32, folded word_bits_def] 92 93lemmas unat_ucast_16_32 = unat_signed_ucast_less_ucast[where 'a=16 and 'b=32, simplified] 94 95(* FIXME: generalize? *) 96lemma scast_mask_8: 97 "scast (mask 8 :: sword32) = (mask 8 :: word32)" 98 by (clarsimp simp: mask_def) 99 100lemmas ucast_le_8_32_equiv = ucast_le_up_down_iff[where 'a=8 and 'b=32, simplified] 101 102lemma signed_unat_minus_one_32: 103 "unat (-1 :: 32 signed word) = 4294967295" 104 by (simp del: word_pow_0 diff_0 add: unat_sub_if' minus_one_word) 105 106lemmas two_bits_cases_32 = two_bits_cases[where 'a=32, simplified] 107 108lemmas word_ctz_not_minus_1_32 = word_ctz_not_minus_1[where 'a=32, simplified] 109 110lemmas sint_ctz_32 = sint_ctz[where 'a=32, simplified] 111 112(* FIXME: inline these? *) 113lemmas scast_specific_plus32 = 114 scast_of_nat_signed_to_unsigned_add[where 'a=32 and x="word_ctz x" and y="0x20" for x, 115 simplified] 116lemmas scast_specific_plus32_signed = 117 scast_of_nat_unsigned_to_signed_add[where 'a=32 and x="word_ctz x" and y="0x20" for x, 118 simplified] 119 120lemma neq_0_unat: "x \<noteq> 0 \<Longrightarrow> 0 < unat x" for x::machine_word 121 by (simp add: unat_gt_0) 122 123end