1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory CommonOpsLemmas 8 9imports 10 "CommonOps" 11 "Word_Lib.WordSetup" 12begin 13 14lemma fold_all_htd_updates': 15 "ptr_retyp (p :: ('a :: c_type) ptr) 16 = all_htd_updates TYPE('a) 1 (ptr_val p) 1" 17 "(if P then (f :: heap_typ_desc \<Rightarrow> heap_typ_desc) else g) s 18 = (if P then f s else g s)" 19 "\<lbrakk> n < 2 ^ word_bits \<rbrakk> \<Longrightarrow> 20 ptr_retyps n p = all_htd_updates TYPE('a) 1 (ptr_val p) (of_nat n)" 21 "\<lbrakk> n < 2 ^ word_bits \<rbrakk> \<Longrightarrow> 22 ptr_retyps (2 ^ n) p = all_htd_updates TYPE('a) 3 (ptr_val p) (of_nat n)" 23 "n < 2 ^ word_bits \<Longrightarrow> typ_clear_region x n = all_htd_updates TYPE(machine_word) 0 x (of_nat n)" 24 "n < 2 ^ word_bits \<Longrightarrow> typ_region_bytes x n = all_htd_updates TYPE(machine_word) 2 x (of_nat n)" 25 "\<lbrakk> n < 2 ^ word_bits \<rbrakk> \<Longrightarrow> 26 ptr_arr_retyps n p = all_htd_updates TYPE('a) 4 (ptr_val p) (of_nat n)" 27 "\<lbrakk> n < 2 ^ word_bits \<rbrakk> \<Longrightarrow> 28 ptr_arr_retyps (2 ^ n) p = all_htd_updates TYPE('a) 5 (ptr_val p) (of_nat n)" 29 by (simp_all add: all_htd_updates_def unat_of_nat fun_eq_iff of_nat_neq_0 word_bits_conv) 30 31lemma upcast_unat_less_2p_length: 32 "is_up UCAST('a :: len \<rightarrow> 'b :: len) \<Longrightarrow> unat (x :: 'a word) < 2 ^ LENGTH('b)" 33 by (simp add: is_up unat_pow_le_intro) 34 35(* FIXME: this is a hack that happens to work on all arches. Use arch split. *) 36lemma is_up_u32_word_size: "is_up UCAST(32 \<rightarrow> machine_word_len)" 37 by (clarsimp simp add: is_up_def source_size target_size) 38 39lemma is_up_i32_word_size: "is_up UCAST(32 signed \<rightarrow> machine_word_len)" 40 by (clarsimp simp add: is_up_def source_size target_size) 41 42lemma unat_word32_less_2p_word_bits: "unat (x :: 32 word) < 2 ^ word_bits" 43 by (rule upcast_unat_less_2p_length[OF is_up_u32_word_size, simplified word_bits_def[symmetric]]) 44 45lemma unat_sword32_less_2p_word_bits: "unat (x :: 32 signed word) < 2 ^ word_bits" 46 by (rule upcast_unat_less_2p_length[OF is_up_i32_word_size, simplified word_bits_def[symmetric]]) 47 48lemmas fold_all_htd_updates_intermediate 49 = fold_all_htd_updates' 50 fold_all_htd_updates'(3-)[OF unat_less_2p_word_bits] 51 fold_all_htd_updates'(3-)[OF unat_word32_less_2p_word_bits] 52 fold_all_htd_updates'(3-)[OF unat_sword32_less_2p_word_bits] 53 54lemmas fold_all_htd_updates = fold_all_htd_updates_intermediate[simplified word_bits_conv] 55 56lemma signed_div_range_check: 57 assumes len: "size a > 1" 58 shows 59 "(sint a sdiv sint b = sint (a sdiv b)) 60 = (a \<noteq> (- (2 ^ (size a - 1))) \<or> b \<noteq> -1)" 61proof - 62 have sints: "(sint (1 :: 'a word)) = 1" 63 "(sint (-1 :: 'a word)) = -1" 64 "(sint (0 :: 'a word)) = 0" 65 using len 66 apply (simp_all add: word_size) 67 done 68 have abs_sint_gt_1: 69 "b \<noteq> 0 \<and> b \<noteq> 1 \<and> b \<noteq> -1 \<Longrightarrow> abs (sint b) > 1" 70 apply (fold word_sint.Rep_inject, 71 simp only: sints abs_if split: if_split) 72 apply arith 73 done 74 have mag: "(a \<noteq> (- (2 ^ (size a - 1))) \<or> (b \<noteq> -1 \<and> b \<noteq> 1)) 75 \<Longrightarrow> abs (abs (sint a) div abs (sint b)) < 2 ^ (size a - 1)" 76 using word_sint.Rep_inject[where x=a and y="- (2 ^ (size a - 1))"] 77 word_sint.Rep_inject[where x=b and y=1] 78 apply (simp add: word_size sint_int_min sints) 79 apply (simp add: nonneg_mod_div) 80 apply (cases "b = 0") 81 apply simp 82 apply (erule impCE) 83 apply (rule order_le_less_trans, rule zdiv_le_dividend, simp_all) 84 apply (cut_tac x=a in sint_range') 85 apply (clarsimp simp add: abs_if word_size) 86 apply (cases "a = 0", simp_all) 87 apply (rule order_less_le_trans, rule int_div_less_self, simp_all) 88 apply (rule abs_sint_gt_1, simp) 89 apply (cut_tac x=a in sint_range') 90 apply (clarsimp simp add: abs_if word_size) 91 done 92 show ?thesis using mag len 93 apply (cases "b = 1") 94 apply (case_tac "size a", simp_all)[1] 95 apply (case_tac nat, simp_all add: sint_word_ariths word_size)[1] 96 apply (simp add: sdiv_int_def sdiv_word_def sint_sbintrunc' 97 sbintrunc_eq_in_range range_sbintrunc sgn_if) 98 apply (safe, simp_all add: word_size sint_int_min) 99 done 100qed 101 102lemma ptr_add_assertion_uintD: 103 "ptr_add_assertion ptr (uint (x :: ('a :: len) word)) strong htd 104 \<longrightarrow> (x = 0 \<or> array_assertion ptr (if strong then unat (x + 1) else unat x) htd)" 105 using unat_lt2p[where x=x] 106 by (simp add: ptr_add_assertion_def uint_0_iff Word.unat_def[symmetric] 107 unat_plus_if_size linorder_not_less word_size 108 le_Suc_eq array_assertion_shrink_right 109 del: unat_lt2p) 110 111lemma sint_uint_sless_0_if: 112 "sint x = (if x <s 0 then - uint (- x) else uint (x :: ('a :: len) word))" 113 apply (simp add: word_sint_msb_eq word_sless_alt 114 word_size uint_word_ariths) 115 apply (clarsimp simp: zmod_zminus1_eq_if uint_0_iff) 116 done 117 118lemma ptr_add_assertion_sintD: 119 "ptr_add_assertion ptr (sint (x :: ('a :: len) word)) strong htd 120 \<longrightarrow> (x = 0 \<or> (x <s 0 \<and> array_assertion (ptr +\<^sub>p sint x) 121 (unat (- x)) htd) 122 \<or> (x \<noteq> 0 \<and> \<not> x <s 0 \<and> array_assertion ptr (if strong then unat (x + 1) else unat x) htd))" 123 using unat_lt2p[where x=x] 124 apply (simp add: ptr_add_assertion_def word_sless_alt 125 sint_uint_sless_0_if[THEN arg_cong[where f="\<lambda>x. - x"]] 126 sint_uint_sless_0_if[THEN arg_cong[where f=nat]] 127 Word.unat_def[symmetric] 128 unat_plus_if_size le_Suc_eq linorder_not_less 129 word_size 130 del: unat_lt2p) 131 apply (simp add: array_assertion_shrink_right) 132 apply (auto simp: linorder_not_less) 133 done 134 135\<comment> \<open> 136 Some lemmas used by both SimplExport and ProveGraphRefine. 137\<close> 138 139lemmas sdiv_word_max_ineq = sdiv_word_max[folded zle_diff1_eq, simplified] 140 141lemmas signed_mult_eq_checks_all = 142 signed_mult_eq_checks_double_size[where 'a="32" and 'b="64", simplified] 143 signed_mult_eq_checks_double_size[where 'a="32 signed" and 'b="64 signed", simplified] 144 signed_mult_eq_checks_double_size[where 'a="64" and 'b="128", simplified] 145 signed_mult_eq_checks_double_size[where 'a="64 signed" and 'b="128 signed", simplified] 146 147lemmas signed_arith_ineq_checks_to_eq_all = 148 signed_arith_ineq_checks_to_eq[where 'a="32"] 149 signed_arith_ineq_checks_to_eq[where 'a="32", simplified word_size, simplified] 150 signed_arith_ineq_checks_to_eq[where 'a="32 signed"] 151 signed_arith_ineq_checks_to_eq[where 'a="32 signed", simplified word_size, simplified] 152 signed_arith_ineq_checks_to_eq[where 'a="64"] 153 signed_arith_ineq_checks_to_eq[where 'a="64", simplified word_size, simplified] 154 signed_arith_ineq_checks_to_eq[where 'a="64 signed"] 155 signed_arith_ineq_checks_to_eq[where 'a="64 signed", simplified word_size, simplified] 156 157lemmas signed_div_range_check_all = 158 signed_div_range_check[where 'a="32", simplified word_size, simplified] 159 signed_div_range_check[where 'a="32 signed", simplified word_size, simplified] 160 signed_div_range_check[where 'a="64", simplified word_size, simplified] 161 signed_div_range_check[where 'a="64 signed", simplified word_size, simplified] 162 163lemma word32_31_less: 164 "31 < len_of TYPE (32 signed)" "31 > (0 :: nat)" 165 "31 < len_of TYPE (32)" "31 > (0 :: nat)" 166 by auto 167 168lemma word64_31_less: 169 "31 < len_of TYPE (64 signed)" "31 > (0 :: nat)" 170 "31 < len_of TYPE (64)" "31 > (0 :: nat)" 171 by auto 172 173lemmas signed_shift_guard_to_word_all = 174 signed_shift_guard_to_word[OF word32_31_less(1-2)] 175 signed_shift_guard_to_word[OF word32_31_less(3-4)] 176 signed_shift_guard_to_word[OF word64_31_less(1-2)] 177 signed_shift_guard_to_word[OF word64_31_less(3-4)] 178 179lemmas guard_arith_simps = 180 neg_le_iff_le 181 signed_arith_eq_checks_to_ord 182 signed_arith_ineq_checks_to_eq_all 183 signed_div_range_check_all 184 signed_mult_eq_checks_all 185 signed_shift_guard_to_word_all 186 sdiv_word_min[THEN eqTrueI] sdiv_word_max_ineq 187 188(* FIXME: move to word lib *) 189lemma small_downcasts: 190 "unat (x :: 'a :: len word) < 2 ^ LENGTH('b :: len) \<Longrightarrow> unat (UCAST('a \<rightarrow> 'b) x) = unat x" 191 apply (case_tac "LENGTH('a) \<le> LENGTH('b)", simp add: unat_ucast_up_simp) 192 apply (simp add: unat_ucast unat_less_power) 193 done 194 195(* FIXME: move to word lib *) 196lemma less_shift_makes_shift_cast_safe: 197 "y < (a :: 'a :: len word) >> unat (x :: 'b :: len word) \<Longrightarrow> 198 unat (UCAST('b \<rightarrow> 'a) x) = unat x" 199 apply (prop_tac "unat x < LENGTH('a)") 200 apply (rotate_tac) 201 apply (erule contrapos_pp; simp add: not_less) 202 apply (prop_tac "a >> unat x = 0") 203 apply (rule shiftr_eq_0; simp) 204 apply simp 205 apply (subst small_downcasts) 206 apply (meson le_less_trans n_less_equal_power_2 nat_less_le) 207 apply simp 208 done 209 210lemmas less_shift_makes_shift_cast_safe_arg_cong = 211 arg_cong[where f="f w" for f w, OF less_shift_makes_shift_cast_safe] 212 213\<comment> \<open> 214 @{thm less_shift_makes_shift_cast_safe} allows us to 215 remove the `ucast` in `unat (ucast x)`, but this loses potentially important 216 type information. These rules act as "lenses" to make sure we only modify 217 the relevant ucasts (the ones that show up in the guards of translated 218 nontrivial shifts). 219\<close> 220lemmas less_shift_targeted_cast_convs = 221 less_shift_makes_shift_cast_safe_arg_cong[where f=shiftr] 222 less_shift_makes_shift_cast_safe_arg_cong[where f="(^)"] 223 224end 225