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