lib/isabelle/Why3_BV.thy.2021-1

   1 theory Why3_BV
   2 imports
   3   Why3_Int
   4   "HOL-Library.Word"
   5 begin
   6
   7 abbreviation (input) pow2 :: "int \<Rightarrow> int"
   8 where "pow2 i \<equiv> 2 ^ nat i"
   9
  10 why3_open "bv/Pow2int.xml"
  11   constants
  12     pow2=pow2
  13
  14 why3_vc Power_0 by simp
  15
  16 why3_vc Power_s using assms by (simp add: Power_s)
  17
  18 why3_vc Power_1 by simp
  19
  20 why3_vc Power_sum using assms by (simp add: Power_sum)
  21
  22 why3_vc pow2pos using assms by simp
  23
  24 why3_vc pow2_0 by simp
  25 why3_vc pow2_1 by simp
  26 why3_vc pow2_2 by simp
  27 why3_vc pow2_3 by simp
  28 why3_vc pow2_4 by simp
  29 why3_vc pow2_5 by simp
  30 why3_vc pow2_6 by simp
  31 why3_vc pow2_7 by simp
  32 why3_vc pow2_8 by simp
  33 why3_vc pow2_9 by simp
  34 why3_vc pow2_10 by simp
  35 why3_vc pow2_11 by simp
  36 why3_vc pow2_12 by simp
  37 why3_vc pow2_13 by simp
  38 why3_vc pow2_14 by simp
  39 why3_vc pow2_15 by simp
  40 why3_vc pow2_16 by simp
  41 why3_vc pow2_17 by simp
  42 why3_vc pow2_18 by simp
  43 why3_vc pow2_19 by simp
  44 why3_vc pow2_20 by simp
  45 why3_vc pow2_21 by simp
  46 why3_vc pow2_22 by simp
  47 why3_vc pow2_23 by simp
  48 why3_vc pow2_24 by simp
  49 why3_vc pow2_25 by simp
  50 why3_vc pow2_26 by simp
  51 why3_vc pow2_27 by simp
  52 why3_vc pow2_28 by simp
  53 why3_vc pow2_29 by simp
  54 why3_vc pow2_30 by simp
  55 why3_vc pow2_31 by simp
  56 why3_vc pow2_32 by simp
  57 why3_vc pow2_33 by simp
  58 why3_vc pow2_34 by simp
  59 why3_vc pow2_35 by simp
  60 why3_vc pow2_36 by simp
  61 why3_vc pow2_37 by simp
  62 why3_vc pow2_38 by simp
  63 why3_vc pow2_39 by simp
  64 why3_vc pow2_40 by simp
  65 why3_vc pow2_41 by simp
  66 why3_vc pow2_42 by simp
  67 why3_vc pow2_43 by simp
  68 why3_vc pow2_44 by simp
  69 why3_vc pow2_45 by simp
  70 why3_vc pow2_46 by simp
  71 why3_vc pow2_47 by simp
  72 why3_vc pow2_48 by simp
  73 why3_vc pow2_49 by simp
  74 why3_vc pow2_50 by simp
  75 why3_vc pow2_51 by simp
  76 why3_vc pow2_52 by simp
  77 why3_vc pow2_53 by simp
  78 why3_vc pow2_54 by simp
  79 why3_vc pow2_55 by simp
  80 why3_vc pow2_56 by simp
  81 why3_vc pow2_57 by simp
  82 why3_vc pow2_58 by simp
  83 why3_vc pow2_59 by simp
  84 why3_vc pow2_60 by simp
  85 why3_vc pow2_61 by simp
  86 why3_vc pow2_62 by simp
  87 why3_vc pow2_63 by simp
  88 why3_vc pow2_64 by simp
  89
  90 why3_end
  91
  92
  93 lemma rotate1_nth:
  94   assumes "0 < length xs"
  95   shows "rotate1 xs ! (i mod length xs) = xs ! (Suc i mod length xs)"
  96 proof (cases xs)
  97   case Nil
  98   with `0 < length xs` show ?thesis by simp
  99 next
 100   case (Cons y ys)
 101   with mod_less_divisor [of "Suc (length ys)" i]
 102   show ?thesis
 103     by (auto simp add: nth_append mod_Suc simp del: mod_less_divisor)
 104 qed
 105
 106 lemma word_rotl_0: "word_rotl 0 w = w"
 107   by transfer simp
 108
 109 lemma word_rotr_0: "word_rotr 0 w = w"
 110   by transfer simp
 111
 112 lemma rotl_nth:
 113   "bit (word_rotl j w) (((i + j) mod len_of TYPE('a))) = bit (w::'a::len word) (i mod len_of TYPE('a))"
 114 proof -
 115   have "bit (word_rotl j w) (((i + j) mod len_of TYPE('a))) =
 116     bit (word_roti (- int j) w) (((i + j) mod len_of TYPE('a)))"
 117     by (simp add: word_rotl_0 word_rotr_0)
 118   then show ?thesis
 119     apply (simp only: bit_word_roti_iff)
 120     apply (simp add: zmod_int mod_diff_left_eq)
 121     apply (simp add: zmod_int [symmetric])
 122     done
 123 qed
 124
 125 lemma rotr_nth:
 126   "bit (word_rotr j w) (i mod len_of TYPE('a)) = bit (w::'a::len word) ((i + j) mod len_of TYPE('a))"
 127   by (simp add: bit_word_rotr_iff mod_add_left_eq)
 128
 129 lemma uint_pow: "uint ((b::'a::len word) ^ n) = uint b ^ n mod 2 ^ len_of TYPE('a)"
 130   by (induct n) (simp_all add: uint_word_ariths mod_mult_right_eq)
 131
 132 context
 133   includes bit_operations_syntax
 134 begin
 135
 136 lemma eq_sub_equiv_aux:
 137   "(\<forall>j. uint i \<le> j \<and> j < uint i + uint n \<longrightarrow>
 138       (0 \<le> j \<and> bit a (nat j)) = (0 \<le> j \<and> bit b (nat j))) =
 139    ((b::('a::len) word) AND (push_bit (unat i) (mask (unat n))) = a AND (push_bit (unat i) (mask (unat n))))"
 140   apply (simp add: bit_eq_iff bit_and_iff bit_push_bit_iff)
 141   apply (rule iffI)
 142   apply (rule allI)
 143   apply (drule_tac x="int na" in spec)
 144   apply (auto simp add: uint_nat bit_mask_iff simp del: of_nat_unat)[1]
 145   apply (rule allI)
 146   apply (drule_tac x="nat j" in spec)
 147   apply (auto simp add: uint_nat bit_mask_iff simp del: of_nat_unat dest: bit_imp_le_length)
 148   done
 149
 150 end
 151
 152 lemma int_minus_mod: "((i::int) - j) mod n = (i + (n - j mod n)) mod n"
 153 proof -
 154   have "(i + (n - j mod n)) mod n = (i mod n + (n - j mod n) mod n) mod n"
 155     by (simp only: mod_add_eq)
 156   also have "(n - j mod n) mod n = (n mod n - j mod n) mod n"
 157     by simp
 158   finally show ?thesis by (simp add: mod_minus_eq mod_add_eq)
 159 qed
 160
 161 lemma nat_minus_mod:
 162   assumes "0 < (n::nat)"
 163   shows "((n - i mod n) + i) mod n = 0"
 164 proof -
 165   have "((n - i mod n) + i) mod n = (i + (n - i mod n)) mod n"
 166     by (simp add: add_ac)
 167   also have "\<dots> = (i mod n + (n - i mod n)) mod n"
 168     by (simp add: mod_add_left_eq)
 169   also from assms have "\<dots> = (n mod n + (i mod n - i mod n)) mod n"
 170     by (simp add: add_ac)
 171   finally show ?thesis by simp
 172 qed
 173
 174 lemma nat_minus_mod':
 175   assumes "0 < (n::nat)"
 176   shows "(i + (n - j mod n) + j) mod n = i mod n"
 177 proof -
 178   have "(i + (n - j mod n) + j) mod n = (i + ((n - j mod n) + j)) mod n"
 179     by (simp add: add_ac)
 180   also have "\<dots> = (i mod n + ((n - j mod n) + j) mod n) mod n"
 181     by (simp add: mod_add_left_eq mod_add_right_eq)
 182   also note nat_minus_mod [OF assms]
 183   finally show ?thesis by simp
 184 qed
 185
 186
 187 definition bv_nth :: "'a::len word \<Rightarrow> int \<Rightarrow> bool"
 188 where "bv_nth bv i \<equiv> 0 \<le> i \<and> bit bv (nat i)"
 189
 190 abbreviation (input) nth_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool"
 191 where "nth_bv bv bv' \<equiv> bit bv (unat bv')"
 192
 193 abbreviation (input) lsr :: "'a::len word \<Rightarrow> int \<Rightarrow> 'a word"
 194 where "lsr v i \<equiv> drop_bit (nat i) v"
 195
 196 abbreviation (input) lsr_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
 197 where "lsr_bv v n \<equiv> drop_bit (unat n) v"
 198
 199 abbreviation (input) asr :: "'a::len word \<Rightarrow> int \<Rightarrow> 'a word"
 200 where "asr v i \<equiv> signed_drop_bit (nat i) v"
 201
 202 abbreviation (input) asr_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
 203 where "asr_bv v n \<equiv> signed_drop_bit (unat n) v"
 204
 205 abbreviation (input) lsl :: "'a::len word \<Rightarrow> int \<Rightarrow> 'a word"
 206 where "lsl v i \<equiv> push_bit (nat i) v"
 207
 208 abbreviation (input) lsl_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
 209 where "lsl_bv v n \<equiv> push_bit (unat n) v"
 210
 211 abbreviation (input) rotate_left :: "'a::len word \<Rightarrow> int \<Rightarrow> 'a word"
 212 where "rotate_left v n \<equiv> word_rotl (nat n) v"
 213
 214 abbreviation (input) rotate_right :: "'a::len word \<Rightarrow> int \<Rightarrow> 'a word"
 215 where "rotate_right v n \<equiv> word_rotr (nat n) v"
 216
 217 abbreviation (input) rotate_left_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
 218 where "rotate_left_bv v n \<equiv> word_rotl (unat n) v"
 219
 220 abbreviation (input) rotate_right_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
 221 where "rotate_right_bv v n \<equiv> word_rotr (unat n) v"
 222
 223 context
 224   includes bit_operations_syntax
 225 begin
 226
 227 definition eq_sub_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
 228   eq_sub_bv_defn: "eq_sub_bv a b i n =
 229     (b AND (push_bit (unat i) (mask (unat n))) = a AND (push_bit (unat i) (mask (unat n))))"
 230
 231 end
 232
 233 definition size_bv :: "'a::len word" where
 234   "size_bv = of_nat LENGTH('a)"
 235
 236 definition is_signed_positive :: "'a::len word \<Rightarrow> bool" where
 237   "is_signed_positive w = (0 \<le> sint w)"
 238
 239 lemma to_int_eq:
 240   "sint (x::'a::len word) =
 241    (if is_signed_positive x then uint x else - (2 ^ LENGTH('a) - uint x))"
 242 proof (cases "0 \<le> sint x")
 243   case True
 244   note sint_lt [of x]
 245   also have "(2::int) ^ (LENGTH('a) - 1) < 2 ^ LENGTH('a)"
 246     by (rule power_strict_increasing) simp_all
 247   finally have "sint x < 2 ^ LENGTH('a)" .
 248   with True show ?thesis
 249     by (simp add: is_signed_positive_def uint_sint take_bit_eq_mod)
 250 next
 251   case False
 252   from sint_ge [of x]
 253   have "- sint x \<le> 2 ^ (LENGTH('a) - 1)" by simp
 254   also have "(2::int) ^ (LENGTH('a) - 1) < 2 ^ LENGTH('a)"
 255     by (rule power_strict_increasing) simp_all
 256   finally have "- sint x < 2 ^ LENGTH('a)" .
 257   then have "- (2 ^ LENGTH('a)) < sint x" by simp
 258   moreover from False have "0 < - sint x" by simp
 259   ultimately have "- sint x = - sint x mod 2 ^ LENGTH('a)"
 260     by simp
 261   also have "sint x mod 2 ^ LENGTH('a) \<noteq> 0"
 262   proof
 263     assume "sint x mod 2 ^ LENGTH('a) = 0"
 264     then obtain y where y: "sint x = y * 2 ^ LENGTH('a)" by auto
 265     with False have "\<not> 0 \<le> y" by auto
 266     then have "y \<le> - 1" by simp
 267     then have "y * 2 ^ LENGTH('a) \<le> - 1 * 2 ^ LENGTH('a)"
 268       by (rule mult_right_mono) simp
 269     with y have "sint x \<le> - (2 ^ LENGTH('a))" by simp
 270     with \<open>- (2 ^ LENGTH('a)) < sint x\<close> show False by simp
 271   qed
 272   then have "- sint x mod 2 ^ LENGTH('a) = 2 ^ LENGTH('a) - sint x mod 2 ^ LENGTH('a)"
 273     by (simp add: zmod_zminus1_eq_if)
 274   finally show ?thesis using False
 275     by (simp add: is_signed_positive_def uint_sint take_bit_eq_mod)
 276 qed
 277
 278 lemma shiftr_div_2n: "uint (drop_bit n v) = uint v div 2 ^ n"
 279   apply (auto simp add: uint_div_distrib uint_pow exp_mod_exp drop_bit_eq_div)
 280   apply (rule div_pos_pos_trivial)
 281   apply simp
 282   apply (rule less_le_trans)
 283   apply (rule uint_bounded)
 284   apply simp
 285   apply (rule div_pos_pos_trivial)
 286   apply simp
 287   apply (rule less_le_trans)
 288   apply (rule uint_bounded)
 289   apply (rule power_increasing)
 290   apply simp_all
 291   done
 292
 293 lemma shiftl_aux: "uint (push_bit n (v::'a word)) = (uint v * 2 ^ n) mod 2 ^ LENGTH('a::len)"
 294   by (auto simp add: uint_word_ariths uint_pow mod_mult_right_eq push_bit_eq_mult)
 295     (simp add:
 296        mod_mult_eq [of "uint v", symmetric]
 297        power_mod [of 2 2 n, symmetric]
 298        power_mult_distrib [symmetric])
 299
 300 type_synonym word8 = "8 word"
 301
 302 abbreviation (input) max_word :: "'a::len word"
 303 where "max_word \<equiv> - 1"
 304
 305 why3_open "bv/BV8.xml"
 306   constants
 307     zeros=zero_class.zero
 308     ones=max_word
 309     bw_and="and"
 310     bw_or=or
 311     bw_xor=xor
 312     bw_not=not
 313     add=plus
 314     sub=minus
 315     neg=uminus
 316     mul=times
 317     udiv=divide
 318     urem=modulo
 319     lsr=lsr
 320     asr=asr
 321     lsl=lsl
 322     lsr_bv=lsr_bv
 323     asr_bv=asr_bv
 324     lsl_bv=lsl_bv
 325     rotate_left=rotate_left
 326     rotate_right=rotate_right
 327     rotate_left_bv=rotate_left_bv
 328     rotate_right_bv=rotate_right_bv
 329     nth=bv_nth
 330     nth_bv=nth_bv
 331     tqtint=uint
 332     of_int=of_int
 333     eq_sub_bv=eq_sub_bv
 334     size_bv=size_bv
 335     one=one_class.one
 336     is_signed_positive=is_signed_positive
 337   types
 338     t=word8
 339
 340 why3_vc nth_out_of_bound
 341   using assms
 342   by (auto simp add: bv_nth_def dest: bit_imp_le_length)
 343
 344 why3_vc Nth_zeros by (simp add: bv_nth_def)
 345
 346 why3_vc Nth_ones
 347   using assms
 348   by (simp add: bv_nth_def)
 349
 350 why3_vc Nth_bw_and
 351   using assms
 352   by (simp add: bv_nth_def bit_and_iff)
 353
 354 why3_vc Nth_bw_or
 355   using assms
 356   by (simp add: bv_nth_def bit_or_iff)
 357
 358 why3_vc Nth_bw_xor
 359   using assms
 360   by (simp add: bv_nth_def bit_xor_iff)
 361
 362 why3_vc Nth_bw_not
 363   using assms
 364   by (simp add: bv_nth_def bit_not_iff nat_less_iff)
 365
 366 why3_vc Lsr_nth_low
 367   using assms
 368   by (simp add: bv_nth_def bit_drop_bit_eq nat_add_distrib add_ac)
 369
 370 why3_vc Lsr_nth_high
 371   using assms
 372   by (simp add: bv_nth_def bit_drop_bit_eq)
 373     (simp add: bit_word.rep_eq nat_add_distrib [symmetric] nat_less_iff)
 374
 375 why3_vc lsr_zeros by simp
 376
 377 why3_vc Asr_nth_low
 378   using assms
 379   by (simp add: bv_nth_def bit_signed_drop_bit_iff)
 380     (auto simp add: nat_add_distrib [symmetric] add_ac)
 381
 382 why3_vc Asr_nth_high
 383   using assms
 384   by (simp add: bv_nth_def bit_signed_drop_bit_iff)
 385     (auto simp add: nat_add_distrib [symmetric])
 386
 387 why3_vc asr_zeros by (simp add: bit_signed_drop_bit_iff)
 388
 389 why3_vc Lsl_nth_high
 390   using assms
 391   by (simp add: bv_nth_def bit_push_bit_iff nat_diff_distrib nat_less_iff nat_le_eq_zle)
 392
 393 why3_vc Lsl_nth_low
 394   using assms
 395   by (simp add: bv_nth_def bit_push_bit_iff nat_le_eq_zle)
 396
 397 why3_vc lsl_zeros by simp
 398
 399 why3_vc to_uint_extensionality using assms by (simp add: word_uint_eq_iff)
 400
 401 why3_vc to_intqtdef by (simp add: to_int_eq)
 402
 403 why3_vc to_int_extensionality using assms by (simp add: signed_word_eqI)
 404
 405 why3_vc positive_is_ge_zeros
 406   by (simp add: is_signed_positive_def sge_def)
 407
 408 why3_vc to_uint_bounds
 409   using uint_ge_0 [of v] uint_bounded [of v]
 410   by simp_all
 411
 412 why3_vc to_uint_of_int
 413   using assms
 414   by (simp add: uint_in_range_def uint_word_of_int)
 415
 416 why3_vc nth_bv_def
 417   by (simp add: bit_eq_iff bit_and_iff)
 418     (simp add: bit_1_iff bit_drop_bit_eq del: bit_0)
 419
 420 why3_vc Nth_bv_is_nth
 421   by (simp add: bv_nth_def)
 422
 423 why3_vc Nth_bv_is_nth2
 424   using assms
 425   by (simp add: bv_nth_def unat_eq_nat_uint to_uint_of_int uint_in_range_def)
 426
 427 why3_vc to_uint_size_bv by (simp add: size_bv_def)
 428
 429 why3_vc to_uint_zeros by simp
 430
 431 why3_vc to_uint_one by simp
 432
 433 why3_vc to_uint_ones by (simp add: uint_word_ariths)
 434
 435 why3_vc to_uint_add
 436   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 437
 438 why3_vc to_uint_add_bounded
 439   using assms
 440   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 441
 442 why3_vc to_uint_sub
 443   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 444
 445 why3_vc to_uint_sub_bounded
 446   using assms
 447   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 448
 449 why3_vc to_uint_neg
 450   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 451
 452 why3_vc to_uint_mul
 453   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 454
 455 why3_vc to_uint_mul_bounded
 456   using assms
 457   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 458
 459 why3_vc to_uint_udiv
 460   by (cases "uint v2 = 0")
 461     (auto simp add: uint_div ediv_def)
 462
 463 why3_vc to_uint_urem
 464   by (simp add: uint_mod emod_def)
 465
 466 why3_vc Nth_rotate_left
 467   using assms rotl_nth [of "nat n" v "nat i + (size v - nat n mod size v)"]
 468   by (simp add: emod_def bv_nth_def word_size nat_minus_mod' int_minus_mod
 469     nat_mod_distrib nat_add_distrib nat_diff_distrib del: add_diff_assoc)
 470
 471 why3_vc Nth_rotate_right
 472   using assms rotr_nth [of "nat n" v "nat i"]
 473   by (simp add: emod_def bv_nth_def nat_mod_distrib nat_add_distrib)
 474
 475 why3_vc rotate_left_bv_is_rotate_left by simp
 476
 477 why3_vc rotate_right_bv_is_rotate_right by simp
 478
 479 why3_vc lsr_bv_is_lsr by simp
 480
 481 why3_vc to_uint_lsr
 482   by (simp add: ediv_def shiftr_div_2n)
 483
 484 why3_vc asr_bv_is_asr by simp
 485
 486 why3_vc lsl_bv_is_lsl by simp
 487
 488 why3_vc to_uint_lsl
 489   by (simp add: emod_def shiftl_aux)
 490
 491 why3_vc Extensionality
 492   using assms
 493   by (simp add: eq_sub_def bv_nth_def bit_eq_iff all_nat)
 494
 495 why3_vc eq_sub_equiv
 496   by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
 497
 498 why3_vc eq_sub_bv_def
 499   by (simp add: eq_sub_bv_defn mask_eq_exp_minus_1)
 500
 501 why3_end
 502
 503
 504 type_synonym word16 = "16 word"
 505
 506 why3_open "bv/BV16.xml"
 507   constants
 508     zeros=zero_class.zero
 509     ones=max_word
 510     bw_and="and"
 511     bw_or=or
 512     bw_xor=xor
 513     bw_not=not
 514     add=plus
 515     sub=minus
 516     neg=uminus
 517     mul=times
 518     udiv=divide
 519     urem=modulo
 520     lsr=lsr
 521     asr=asr
 522     lsl=lsl
 523     lsr_bv=lsr_bv
 524     asr_bv=asr_bv
 525     lsl_bv=lsl_bv
 526     rotate_left=rotate_left
 527     rotate_right=rotate_right
 528     rotate_left_bv=rotate_left_bv
 529     rotate_right_bv=rotate_right_bv
 530     nth=bv_nth
 531     nth_bv=nth_bv
 532     tqtint=uint
 533     of_int=of_int
 534     eq_sub_bv=eq_sub_bv
 535     size_bv=size_bv
 536     one=one_class.one
 537     is_signed_positive=is_signed_positive
 538   types
 539     t=word16
 540
 541 why3_vc nth_out_of_bound
 542   using assms
 543   by (auto simp add: bv_nth_def dest: bit_imp_le_length)
 544
 545 why3_vc Nth_zeros by (simp add: bv_nth_def)
 546
 547 why3_vc Nth_ones
 548   using assms
 549   by (simp add: bv_nth_def)
 550
 551 why3_vc Nth_bw_and
 552   using assms
 553   by (simp add: bv_nth_def bit_and_iff)
 554
 555 why3_vc Nth_bw_or
 556   using assms
 557   by (simp add: bv_nth_def bit_or_iff)
 558
 559 why3_vc Nth_bw_xor
 560   using assms
 561   by (simp add: bv_nth_def bit_xor_iff)
 562
 563 why3_vc Nth_bw_not
 564   using assms
 565   by (simp add: bv_nth_def bit_not_iff nat_less_iff)
 566
 567 why3_vc Lsr_nth_low
 568   using assms
 569   by (simp add: bv_nth_def bit_drop_bit_eq nat_add_distrib add_ac)
 570
 571 why3_vc Lsr_nth_high
 572   using assms
 573   by (simp add: bv_nth_def bit_drop_bit_eq)
 574     (simp add: bit_word.rep_eq nat_add_distrib [symmetric] nat_less_iff)
 575
 576 why3_vc lsr_zeros by simp
 577
 578 why3_vc Asr_nth_low
 579   using assms
 580   by (simp add: bv_nth_def bit_signed_drop_bit_iff)
 581     (auto simp add: nat_add_distrib [symmetric] add_ac)
 582
 583 why3_vc Asr_nth_high
 584   using assms
 585   by (simp add: bv_nth_def bit_signed_drop_bit_iff)
 586     (auto simp add: nat_add_distrib [symmetric])
 587
 588 why3_vc asr_zeros by (simp add: bit_signed_drop_bit_iff)
 589
 590 why3_vc Lsl_nth_high
 591   using assms
 592   by (simp add: bv_nth_def bit_push_bit_iff nat_diff_distrib nat_less_iff nat_le_eq_zle)
 593
 594 why3_vc Lsl_nth_low
 595   using assms
 596   by (simp add: bv_nth_def bit_push_bit_iff nat_le_eq_zle)
 597
 598 why3_vc lsl_zeros by simp
 599
 600 why3_vc to_uint_extensionality using assms by (simp add: word_uint_eq_iff)
 601
 602 why3_vc to_intqtdef by (simp add: to_int_eq)
 603
 604 why3_vc to_int_extensionality using assms by (simp add: signed_word_eqI)
 605
 606 why3_vc positive_is_ge_zeros
 607   by (simp add: is_signed_positive_def sge_def)
 608
 609 why3_vc to_uint_bounds
 610   using uint_ge_0 [of v] uint_bounded [of v]
 611   by simp_all
 612
 613 why3_vc to_uint_of_int
 614   using assms
 615   by (simp add: uint_in_range_def uint_word_of_int)
 616
 617 why3_vc nth_bv_def
 618   by (simp add: bit_eq_iff bit_and_iff)
 619     (simp add: bit_1_iff bit_drop_bit_eq del: bit_0)
 620
 621 why3_vc Nth_bv_is_nth
 622   by (simp add: bv_nth_def)
 623
 624 why3_vc Nth_bv_is_nth2
 625   using assms
 626   by (simp add: bv_nth_def unat_eq_nat_uint to_uint_of_int uint_in_range_def)
 627
 628 why3_vc to_uint_size_bv by (simp add: size_bv_def)
 629
 630 why3_vc to_uint_zeros by simp
 631
 632 why3_vc to_uint_one by simp
 633
 634 why3_vc to_uint_ones by (simp add: uint_word_ariths)
 635
 636 why3_vc to_uint_add
 637   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 638
 639 why3_vc to_uint_add_bounded
 640   using assms
 641   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 642
 643 why3_vc to_uint_sub
 644   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 645
 646 why3_vc to_uint_sub_bounded
 647   using assms
 648   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 649
 650 why3_vc to_uint_neg
 651   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 652
 653 why3_vc to_uint_mul
 654   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 655
 656 why3_vc to_uint_mul_bounded
 657   using assms
 658   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 659
 660 why3_vc to_uint_udiv
 661   by (cases "uint v2 = 0")
 662     (auto simp add: uint_div ediv_def)
 663
 664 why3_vc to_uint_urem
 665   by (simp add: uint_mod emod_def)
 666
 667 why3_vc Nth_rotate_left
 668   using assms rotl_nth [of "nat n" v "nat i + (size v - nat n mod size v)"]
 669   by (simp add: emod_def bv_nth_def word_size nat_minus_mod' int_minus_mod
 670     nat_mod_distrib nat_add_distrib nat_diff_distrib del: add_diff_assoc)
 671
 672 why3_vc Nth_rotate_right
 673   using assms rotr_nth [of "nat n" v "nat i"]
 674   by (simp add: emod_def bv_nth_def nat_mod_distrib nat_add_distrib)
 675
 676 why3_vc rotate_left_bv_is_rotate_left by simp
 677
 678 why3_vc rotate_right_bv_is_rotate_right by simp
 679
 680 why3_vc lsr_bv_is_lsr by simp
 681
 682 why3_vc to_uint_lsr
 683   by (simp add: ediv_def shiftr_div_2n)
 684
 685 why3_vc asr_bv_is_asr by simp
 686
 687 why3_vc lsl_bv_is_lsl by simp
 688
 689 why3_vc to_uint_lsl
 690   by (simp add: emod_def shiftl_aux)
 691
 692 why3_vc Extensionality
 693   using assms
 694   by (simp add: eq_sub_def bv_nth_def bit_eq_iff all_nat)
 695
 696 why3_vc eq_sub_equiv
 697   by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
 698
 699 why3_vc eq_sub_bv_def
 700   by (simp add: eq_sub_bv_defn mask_eq_exp_minus_1)
 701
 702 why3_end
 703
 704
 705 type_synonym word32 = "32 word"
 706
 707 why3_open "bv/BV32.xml"
 708   constants
 709     zeros=zero_class.zero
 710     ones=max_word
 711     bw_and="and"
 712     bw_or=or
 713     bw_xor=xor
 714     bw_not=not
 715     add=plus
 716     sub=minus
 717     neg=uminus
 718     mul=times
 719     udiv=divide
 720     urem=modulo
 721     lsr=lsr
 722     asr=asr
 723     lsl=lsl
 724     lsr_bv=lsr_bv
 725     asr_bv=asr_bv
 726     lsl_bv=lsl_bv
 727     rotate_left=rotate_left
 728     rotate_right=rotate_right
 729     rotate_left_bv=rotate_left_bv
 730     rotate_right_bv=rotate_right_bv
 731     nth=bv_nth
 732     nth_bv=nth_bv
 733     tqtint=uint
 734     of_int=of_int
 735     eq_sub_bv=eq_sub_bv
 736     size_bv=size_bv
 737     one=one_class.one
 738     is_signed_positive=is_signed_positive
 739   types
 740     t=word32
 741
 742 why3_vc nth_out_of_bound
 743   using assms
 744   by (auto simp add: bv_nth_def dest: bit_imp_le_length)
 745
 746 why3_vc Nth_zeros by (simp add: bv_nth_def)
 747
 748 why3_vc Nth_ones
 749   using assms
 750   by (simp add: bv_nth_def)
 751
 752 why3_vc Nth_bw_and
 753   using assms
 754   by (simp add: bv_nth_def bit_and_iff)
 755
 756 why3_vc Nth_bw_or
 757   using assms
 758   by (simp add: bv_nth_def bit_or_iff)
 759
 760 why3_vc Nth_bw_xor
 761   using assms
 762   by (simp add: bv_nth_def bit_xor_iff)
 763
 764 why3_vc Nth_bw_not
 765   using assms
 766   by (simp add: bv_nth_def bit_not_iff nat_less_iff)
 767
 768 why3_vc Lsr_nth_low
 769   using assms
 770   by (simp add: bv_nth_def bit_drop_bit_eq nat_add_distrib add_ac)
 771
 772 why3_vc Lsr_nth_high
 773   using assms
 774   by (simp add: bv_nth_def bit_drop_bit_eq)
 775     (simp add: bit_word.rep_eq nat_add_distrib [symmetric] nat_less_iff)
 776
 777 why3_vc lsr_zeros by simp
 778
 779 why3_vc Asr_nth_low
 780   using assms
 781   by (simp add: bv_nth_def bit_signed_drop_bit_iff)
 782     (auto simp add: nat_add_distrib [symmetric] add_ac)
 783
 784 why3_vc Asr_nth_high
 785   using assms
 786   by (simp add: bv_nth_def bit_signed_drop_bit_iff)
 787     (auto simp add: nat_add_distrib [symmetric])
 788
 789 why3_vc asr_zeros by (simp add: bit_signed_drop_bit_iff)
 790
 791 why3_vc Lsl_nth_high
 792   using assms
 793   by (simp add: bv_nth_def bit_push_bit_iff nat_diff_distrib nat_less_iff nat_le_eq_zle)
 794
 795 why3_vc Lsl_nth_low
 796   using assms
 797   by (simp add: bv_nth_def bit_push_bit_iff nat_le_eq_zle)
 798
 799 why3_vc lsl_zeros by simp
 800
 801 why3_vc to_uint_extensionality using assms by (simp add: word_uint_eq_iff)
 802
 803 why3_vc to_intqtdef by (simp add: to_int_eq)
 804
 805 why3_vc to_int_extensionality using assms by (simp add: signed_word_eqI)
 806
 807 why3_vc positive_is_ge_zeros
 808   by (simp add: is_signed_positive_def sge_def)
 809
 810 why3_vc to_uint_bounds
 811   using uint_ge_0 [of v] uint_bounded [of v]
 812   by simp_all
 813
 814 why3_vc to_uint_of_int
 815   using assms
 816   by (simp add: uint_in_range_def uint_word_of_int)
 817
 818 why3_vc nth_bv_def
 819   by (simp add: bit_eq_iff bit_and_iff)
 820     (simp add: bit_1_iff bit_drop_bit_eq del: bit_0)
 821
 822 why3_vc Nth_bv_is_nth
 823   by (simp add: bv_nth_def)
 824
 825 why3_vc Nth_bv_is_nth2
 826   using assms
 827   by (simp add: bv_nth_def unat_eq_nat_uint to_uint_of_int uint_in_range_def)
 828
 829 why3_vc to_uint_size_bv by (simp add: size_bv_def)
 830
 831 why3_vc to_uint_zeros by simp
 832
 833 why3_vc to_uint_one by simp
 834
 835 why3_vc to_uint_ones by (simp add: uint_word_ariths)
 836
 837 why3_vc to_uint_add
 838   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 839
 840 why3_vc to_uint_add_bounded
 841   using assms
 842   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 843
 844 why3_vc to_uint_sub
 845   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 846
 847 why3_vc to_uint_sub_bounded
 848   using assms
 849   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 850
 851 why3_vc to_uint_neg
 852   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 853
 854 why3_vc to_uint_mul
 855   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
 856
 857 why3_vc to_uint_mul_bounded
 858   using assms
 859   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
 860
 861 why3_vc to_uint_udiv
 862   by (cases "uint v2 = 0")
 863     (auto simp add: uint_div ediv_def)
 864
 865 why3_vc to_uint_urem
 866   by (simp add: uint_mod emod_def)
 867
 868 why3_vc Nth_rotate_left
 869   using assms rotl_nth [of "nat n" v "nat i + (size v - nat n mod size v)"]
 870   by (simp add: emod_def bv_nth_def word_size nat_minus_mod' int_minus_mod
 871     nat_mod_distrib nat_add_distrib nat_diff_distrib del: add_diff_assoc)
 872
 873 why3_vc Nth_rotate_right
 874   using assms rotr_nth [of "nat n" v "nat i"]
 875   by (simp add: emod_def bv_nth_def nat_mod_distrib nat_add_distrib)
 876
 877 why3_vc rotate_left_bv_is_rotate_left by simp
 878
 879 why3_vc rotate_right_bv_is_rotate_right by simp
 880
 881 why3_vc lsr_bv_is_lsr by simp
 882
 883 why3_vc to_uint_lsr
 884   by (simp add: ediv_def shiftr_div_2n)
 885
 886 why3_vc asr_bv_is_asr by simp
 887
 888 why3_vc lsl_bv_is_lsl by simp
 889
 890 why3_vc to_uint_lsl
 891   by (simp add: emod_def shiftl_aux)
 892
 893 why3_vc Extensionality
 894   using assms
 895   by (simp add: eq_sub_def bv_nth_def bit_eq_iff all_nat)
 896
 897 why3_vc eq_sub_equiv
 898   by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
 899
 900 why3_vc eq_sub_bv_def
 901   by (simp add: eq_sub_bv_defn mask_eq_exp_minus_1)
 902
 903 why3_end
 904
 905
 906 type_synonym word64 = "64 word"
 907
 908 why3_open "bv/BV64.xml"
 909   constants
 910     zeros=zero_class.zero
 911     ones=max_word
 912     bw_and="and"
 913     bw_or=or
 914     bw_xor=xor
 915     bw_not=not
 916     add=plus
 917     sub=minus
 918     neg=uminus
 919     mul=times
 920     udiv=divide
 921     urem=modulo
 922     lsr=lsr
 923     asr=asr
 924     lsl=lsl
 925     lsr_bv=lsr_bv
 926     asr_bv=asr_bv
 927     lsl_bv=lsl_bv
 928     rotate_left=rotate_left
 929     rotate_right=rotate_right
 930     rotate_left_bv=rotate_left_bv
 931     rotate_right_bv=rotate_right_bv
 932     nth=bv_nth
 933     nth_bv=nth_bv
 934     tqtint=uint
 935     of_int=of_int
 936     eq_sub_bv=eq_sub_bv
 937     size_bv=size_bv
 938     one=one_class.one
 939     is_signed_positive=is_signed_positive
 940   types
 941     t=word64
 942
 943 why3_vc nth_out_of_bound
 944   using assms
 945   by (auto simp add: bv_nth_def dest: bit_imp_le_length)
 946
 947 why3_vc Nth_zeros by (simp add: bv_nth_def)
 948
 949 why3_vc Nth_ones
 950   using assms
 951   by (simp add: bv_nth_def)
 952
 953 why3_vc Nth_bw_and
 954   using assms
 955   by (simp add: bv_nth_def bit_and_iff)
 956
 957 why3_vc Nth_bw_or
 958   using assms
 959   by (simp add: bv_nth_def bit_or_iff)
 960
 961 why3_vc Nth_bw_xor
 962   using assms
 963   by (simp add: bv_nth_def bit_xor_iff)
 964
 965 why3_vc Nth_bw_not
 966   using assms
 967   by (simp add: bv_nth_def bit_not_iff nat_less_iff)
 968
 969 why3_vc Lsr_nth_low
 970   using assms
 971   by (simp add: bv_nth_def bit_drop_bit_eq nat_add_distrib add_ac)
 972
 973 why3_vc Lsr_nth_high
 974   using assms
 975   by (simp add: bv_nth_def bit_drop_bit_eq)
 976     (simp add: bit_word.rep_eq nat_add_distrib [symmetric] nat_less_iff)
 977
 978 why3_vc lsr_zeros by simp
 979
 980 why3_vc Asr_nth_low
 981   using assms
 982   by (simp add: bv_nth_def bit_signed_drop_bit_iff)
 983     (auto simp add: nat_add_distrib [symmetric] add_ac)
 984
 985 why3_vc Asr_nth_high
 986   using assms
 987   by (simp add: bv_nth_def bit_signed_drop_bit_iff)
 988     (auto simp add: nat_add_distrib [symmetric])
 989
 990 why3_vc asr_zeros by (simp add: bit_signed_drop_bit_iff)
 991
 992 why3_vc Lsl_nth_high
 993   using assms
 994   by (simp add: bv_nth_def bit_push_bit_iff nat_diff_distrib nat_less_iff nat_le_eq_zle)
 995
 996 why3_vc Lsl_nth_low
 997   using assms
 998   by (simp add: bv_nth_def bit_push_bit_iff nat_le_eq_zle)
 999
1000 why3_vc lsl_zeros by simp
1001
1002 why3_vc to_uint_extensionality using assms by (simp add: word_uint_eq_iff)
1003
1004 why3_vc to_intqtdef by (simp add: to_int_eq)
1005
1006 why3_vc to_int_extensionality using assms by (simp add: signed_word_eqI)
1007
1008 why3_vc positive_is_ge_zeros
1009   by (simp add: is_signed_positive_def sge_def)
1010
1011 why3_vc to_uint_bounds
1012   using uint_ge_0 [of v] uint_bounded [of v]
1013   by simp_all
1014
1015 why3_vc to_uint_of_int
1016   using assms
1017   by (simp add: uint_in_range_def uint_word_of_int)
1018
1019 why3_vc nth_bv_def
1020   by (simp add: bit_eq_iff bit_and_iff)
1021     (simp add: bit_1_iff bit_drop_bit_eq del: bit_0)
1022
1023 why3_vc Nth_bv_is_nth
1024   by (simp add: bv_nth_def)
1025
1026 why3_vc Nth_bv_is_nth2
1027   using assms
1028   by (simp add: bv_nth_def unat_eq_nat_uint to_uint_of_int uint_in_range_def)
1029
1030 why3_vc to_uint_size_bv by (simp add: size_bv_def)
1031
1032 why3_vc to_uint_zeros by simp
1033
1034 why3_vc to_uint_one by simp
1035
1036 why3_vc to_uint_ones by (simp add: uint_word_ariths)
1037
1038 why3_vc to_uint_add
1039   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
1040
1041 why3_vc to_uint_add_bounded
1042   using assms
1043   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
1044
1045 why3_vc to_uint_sub
1046   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
1047
1048 why3_vc to_uint_sub_bounded
1049   using assms
1050   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
1051
1052 why3_vc to_uint_neg
1053   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
1054
1055 why3_vc to_uint_mul
1056   by (simp add: uint_word_arith_bintrs take_bit_eq_mod emod_def)
1057
1058 why3_vc to_uint_mul_bounded
1059   using assms
1060   by (simp add: uint_word_arith_bintrs take_bit_eq_mod)
1061
1062 why3_vc to_uint_udiv
1063   by (cases "uint v2 = 0")
1064     (auto simp add: uint_div ediv_def)
1065
1066 why3_vc to_uint_urem
1067   by (simp add: uint_mod emod_def)
1068
1069 why3_vc Nth_rotate_left
1070   using assms rotl_nth [of "nat n" v "nat i + (size v - nat n mod size v)"]
1071   by (simp add: emod_def bv_nth_def word_size nat_minus_mod' int_minus_mod
1072     nat_mod_distrib nat_add_distrib nat_diff_distrib del: add_diff_assoc)
1073
1074 why3_vc Nth_rotate_right
1075   using assms rotr_nth [of "nat n" v "nat i"]
1076   by (simp add: emod_def bv_nth_def nat_mod_distrib nat_add_distrib)
1077
1078 why3_vc rotate_left_bv_is_rotate_left by simp
1079
1080 why3_vc rotate_right_bv_is_rotate_right by simp
1081
1082 why3_vc lsr_bv_is_lsr by simp
1083
1084 why3_vc to_uint_lsr
1085   by (simp add: ediv_def shiftr_div_2n)
1086
1087 why3_vc asr_bv_is_asr by simp
1088
1089 why3_vc lsl_bv_is_lsl by simp
1090
1091 why3_vc to_uint_lsl
1092   by (simp add: emod_def shiftl_aux)
1093
1094 why3_vc Extensionality
1095   using assms
1096   by (simp add: eq_sub_def bv_nth_def bit_eq_iff all_nat)
1097
1098 why3_vc eq_sub_equiv
1099   by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
1100
1101 why3_vc eq_sub_bv_def
1102   by (simp add: eq_sub_bv_defn mask_eq_exp_minus_1)
1103
1104 why3_end
1105
1106
1107 why3_open "bv/BVConverter_32_64.xml"
1108   constants
1109     toBig = ucast
1110     toSmall = ucast
1111
1112 why3_vc toSmall_to_uint
1113   using assms
1114   by (simp add: BV64.ule_def ucast_eq uint_word_of_int del: of_int_uint)
1115
1116 why3_vc toBig_to_uint
1117   by (simp add: uint_up_ucast is_up)
1118
1119 why3_end
1120
1121
1122 why3_open "bv/BVConverter_16_64.xml"
1123   constants
1124     toBig = ucast
1125     toSmall = ucast
1126
1127 why3_vc toSmall_to_uint
1128   using assms
1129   by (simp add: BV64.ule_def ucast_eq uint_word_of_int del: of_int_uint)
1130
1131 why3_vc toBig_to_uint
1132   by (simp add: uint_up_ucast is_up)
1133
1134 why3_end
1135
1136
1137 why3_open "bv/BVConverter_8_64.xml"
1138   constants
1139     toBig = ucast
1140     toSmall = ucast
1141
1142 why3_vc toSmall_to_uint
1143   using assms
1144   by (simp add: BV64.ule_def ucast_eq uint_word_of_int del: of_int_uint)
1145
1146 why3_vc toBig_to_uint
1147   by (simp add: uint_up_ucast is_up)
1148
1149 why3_end
1150
1151
1152 why3_open "bv/BVConverter_16_32.xml"
1153   constants
1154     toBig = ucast
1155     toSmall = ucast
1156
1157 why3_vc toSmall_to_uint
1158   using assms
1159   by (simp add: BV32.ule_def ucast_eq uint_word_of_int del: of_int_uint)
1160
1161 why3_vc toBig_to_uint
1162   by (simp add: uint_up_ucast is_up)
1163
1164 why3_end
1165
1166
1167 why3_open "bv/BVConverter_8_32.xml"
1168   constants
1169     toBig = ucast
1170     toSmall = ucast
1171
1172 why3_vc toSmall_to_uint
1173   using assms
1174   by (simp add: BV32.ule_def ucast_eq uint_word_of_int del: of_int_uint)
1175
1176 why3_vc toBig_to_uint
1177   by (simp add: uint_up_ucast is_up)
1178
1179 why3_end
1180
1181
1182 why3_open "bv/BVConverter_8_16.xml"
1183   constants
1184     toBig = ucast
1185     toSmall = ucast
1186
1187 why3_vc toSmall_to_uint
1188   using assms
1189   by (simp add: BV16.ule_def ucast_eq uint_word_of_int del: of_int_uint)
1190
1191 why3_vc toBig_to_uint
1192   by (simp add: uint_up_ucast is_up)
1193
1194 why3_end
1195
1196 end