stdlib/bv.mlw

   1 (** {1 Bit Vectors} *)
   2
   3 (** {2 Powers of two} *)
   4
   5 module Pow2int
   6
   7   use int.Int
   8
   9   function pow2 (i:int) : int
  10
  11   axiom Power_0 : pow2 0 = 1
  12   meta "remove_unused:dependency" axiom Power_0, function pow2
  13
  14   axiom Power_s : forall n: int. n >= 0 -> pow2 (n+1) = 2 * pow2 n
  15   meta "remove_unused:dependency" axiom Power_s, function pow2
  16
  17   lemma Power_1 : pow2 1 = 2
  18   meta "remove_unused:dependency" lemma Power_1, function pow2
  19
  20   lemma Power_sum :
  21     forall n m: int. n >= 0 /\ m >= 0 -> pow2 (n+m) = pow2 n * pow2 m
  22   meta "remove_unused:dependency" lemma Power_sum, function pow2
  23
  24   lemma pow2pos: forall i:int. i >= 0 -> pow2 i > 0
  25   meta "remove_unused:dependency" lemma pow2pos, function pow2
  26
  27   lemma pow2_0: pow2 0   =                  0x1
  28   lemma pow2_1: pow2 1   =                  0x2
  29   lemma pow2_2: pow2 2   =                  0x4
  30   lemma pow2_3: pow2 3   =                  0x8
  31   lemma pow2_4: pow2 4   =                 0x10
  32   lemma pow2_5: pow2 5   =                 0x20
  33   lemma pow2_6: pow2 6   =                 0x40
  34   lemma pow2_7: pow2 7   =                 0x80
  35   lemma pow2_8: pow2 8   =                0x100
  36   lemma pow2_9: pow2 9   =                0x200
  37   lemma pow2_10: pow2 10 =                0x400
  38   lemma pow2_11: pow2 11 =                0x800
  39   lemma pow2_12: pow2 12 =               0x1000
  40   lemma pow2_13: pow2 13 =               0x2000
  41   lemma pow2_14: pow2 14 =               0x4000
  42   lemma pow2_15: pow2 15 =               0x8000
  43   lemma pow2_16: pow2 16 =              0x10000
  44   lemma pow2_17: pow2 17 =              0x20000
  45   lemma pow2_18: pow2 18 =              0x40000
  46   lemma pow2_19: pow2 19 =              0x80000
  47   lemma pow2_20: pow2 20 =             0x100000
  48   lemma pow2_21: pow2 21 =             0x200000
  49   lemma pow2_22: pow2 22 =             0x400000
  50   lemma pow2_23: pow2 23 =             0x800000
  51   lemma pow2_24: pow2 24 =            0x1000000
  52   lemma pow2_25: pow2 25 =            0x2000000
  53   lemma pow2_26: pow2 26 =            0x4000000
  54   lemma pow2_27: pow2 27 =            0x8000000
  55   lemma pow2_28: pow2 28 =           0x10000000
  56   lemma pow2_29: pow2 29 =           0x20000000
  57   lemma pow2_30: pow2 30 =           0x40000000
  58   lemma pow2_31: pow2 31 =           0x80000000
  59   lemma pow2_32: pow2 32 =          0x100000000
  60   lemma pow2_33: pow2 33 =          0x200000000
  61   lemma pow2_34: pow2 34 =          0x400000000
  62   lemma pow2_35: pow2 35 =          0x800000000
  63   lemma pow2_36: pow2 36 =         0x1000000000
  64   lemma pow2_37: pow2 37 =         0x2000000000
  65   lemma pow2_38: pow2 38 =         0x4000000000
  66   lemma pow2_39: pow2 39 =         0x8000000000
  67   lemma pow2_40: pow2 40 =        0x10000000000
  68   lemma pow2_41: pow2 41 =        0x20000000000
  69   lemma pow2_42: pow2 42 =        0x40000000000
  70   lemma pow2_43: pow2 43 =        0x80000000000
  71   lemma pow2_44: pow2 44 =       0x100000000000
  72   lemma pow2_45: pow2 45 =       0x200000000000
  73   lemma pow2_46: pow2 46 =       0x400000000000
  74   lemma pow2_47: pow2 47 =       0x800000000000
  75   lemma pow2_48: pow2 48 =      0x1000000000000
  76   lemma pow2_49: pow2 49 =      0x2000000000000
  77   lemma pow2_50: pow2 50 =      0x4000000000000
  78   lemma pow2_51: pow2 51 =      0x8000000000000
  79   lemma pow2_52: pow2 52 =     0x10000000000000
  80   lemma pow2_53: pow2 53 =     0x20000000000000
  81   lemma pow2_54: pow2 54 =     0x40000000000000
  82   lemma pow2_55: pow2 55 =     0x80000000000000
  83   lemma pow2_56: pow2 56 =    0x100000000000000
  84   lemma pow2_57: pow2 57 =    0x200000000000000
  85   lemma pow2_58: pow2 58 =    0x400000000000000
  86   lemma pow2_59: pow2 59 =    0x800000000000000
  87   lemma pow2_60: pow2 60 =   0x1000000000000000
  88   lemma pow2_61: pow2 61 =   0x2000000000000000
  89   lemma pow2_62: pow2 62 =   0x4000000000000000
  90   lemma pow2_63: pow2 63 =   0x8000000000000000
  91   lemma pow2_64: pow2 64 =  0x10000000000000000
  92
  93   meta "remove_unused:dependency" lemma pow2_0, function pow2
  94   meta "remove_unused:dependency" lemma pow2_1, function pow2
  95   meta "remove_unused:dependency" lemma pow2_2, function pow2
  96   meta "remove_unused:dependency" lemma pow2_3, function pow2
  97   meta "remove_unused:dependency" lemma pow2_4, function pow2
  98   meta "remove_unused:dependency" lemma pow2_5, function pow2
  99   meta "remove_unused:dependency" lemma pow2_6, function pow2
 100   meta "remove_unused:dependency" lemma pow2_7, function pow2
 101   meta "remove_unused:dependency" lemma pow2_8, function pow2
 102   meta "remove_unused:dependency" lemma pow2_9, function pow2
 103   meta "remove_unused:dependency" lemma pow2_10, function pow2
 104   meta "remove_unused:dependency" lemma pow2_11, function pow2
 105   meta "remove_unused:dependency" lemma pow2_12, function pow2
 106   meta "remove_unused:dependency" lemma pow2_13, function pow2
 107   meta "remove_unused:dependency" lemma pow2_14, function pow2
 108   meta "remove_unused:dependency" lemma pow2_15, function pow2
 109   meta "remove_unused:dependency" lemma pow2_16, function pow2
 110   meta "remove_unused:dependency" lemma pow2_17, function pow2
 111   meta "remove_unused:dependency" lemma pow2_18, function pow2
 112   meta "remove_unused:dependency" lemma pow2_19, function pow2
 113   meta "remove_unused:dependency" lemma pow2_20, function pow2
 114   meta "remove_unused:dependency" lemma pow2_21, function pow2
 115   meta "remove_unused:dependency" lemma pow2_22, function pow2
 116   meta "remove_unused:dependency" lemma pow2_23, function pow2
 117   meta "remove_unused:dependency" lemma pow2_24, function pow2
 118   meta "remove_unused:dependency" lemma pow2_25, function pow2
 119   meta "remove_unused:dependency" lemma pow2_26, function pow2
 120   meta "remove_unused:dependency" lemma pow2_27, function pow2
 121   meta "remove_unused:dependency" lemma pow2_28, function pow2
 122   meta "remove_unused:dependency" lemma pow2_29, function pow2
 123   meta "remove_unused:dependency" lemma pow2_30, function pow2
 124   meta "remove_unused:dependency" lemma pow2_31, function pow2
 125   meta "remove_unused:dependency" lemma pow2_32, function pow2
 126   meta "remove_unused:dependency" lemma pow2_33, function pow2
 127   meta "remove_unused:dependency" lemma pow2_34, function pow2
 128   meta "remove_unused:dependency" lemma pow2_35, function pow2
 129   meta "remove_unused:dependency" lemma pow2_36, function pow2
 130   meta "remove_unused:dependency" lemma pow2_37, function pow2
 131   meta "remove_unused:dependency" lemma pow2_38, function pow2
 132   meta "remove_unused:dependency" lemma pow2_39, function pow2
 133   meta "remove_unused:dependency" lemma pow2_40, function pow2
 134   meta "remove_unused:dependency" lemma pow2_41, function pow2
 135   meta "remove_unused:dependency" lemma pow2_42, function pow2
 136   meta "remove_unused:dependency" lemma pow2_43, function pow2
 137   meta "remove_unused:dependency" lemma pow2_44, function pow2
 138   meta "remove_unused:dependency" lemma pow2_45, function pow2
 139   meta "remove_unused:dependency" lemma pow2_46, function pow2
 140   meta "remove_unused:dependency" lemma pow2_47, function pow2
 141   meta "remove_unused:dependency" lemma pow2_48, function pow2
 142   meta "remove_unused:dependency" lemma pow2_49, function pow2
 143   meta "remove_unused:dependency" lemma pow2_50, function pow2
 144   meta "remove_unused:dependency" lemma pow2_51, function pow2
 145   meta "remove_unused:dependency" lemma pow2_52, function pow2
 146   meta "remove_unused:dependency" lemma pow2_53, function pow2
 147   meta "remove_unused:dependency" lemma pow2_54, function pow2
 148   meta "remove_unused:dependency" lemma pow2_55, function pow2
 149   meta "remove_unused:dependency" lemma pow2_56, function pow2
 150   meta "remove_unused:dependency" lemma pow2_57, function pow2
 151   meta "remove_unused:dependency" lemma pow2_58, function pow2
 152   meta "remove_unused:dependency" lemma pow2_59, function pow2
 153   meta "remove_unused:dependency" lemma pow2_60, function pow2
 154   meta "remove_unused:dependency" lemma pow2_61, function pow2
 155   meta "remove_unused:dependency" lemma pow2_62, function pow2
 156   meta "remove_unused:dependency" lemma pow2_63, function pow2
 157   meta "remove_unused:dependency" lemma pow2_64, function pow2
 158
 159
 160   (*** use int.EuclideanDivision
 161
 162    lemma Div_pow: forall x i:int.
 163      i > 0 -> pow2 (i-1) <= x < pow2 i -> div x (pow2 (i-1)) = 1
 164
 165    lemma Div_div_pow: forall x i j:int.
 166      i > 0 /\ j > 0 -> div (div x (pow2 i)) (pow2 j) = div x (pow2 (i+j))
 167
 168    lemma Mod_pow2_gen: forall x i k :int.
 169      0 <= k < i -> mod (div (x + pow2 i) (pow2 k)) 2 = mod (div x (pow2 k)) 2
 170    *)
 171
 172 end
 173
 174 (** {2 Generic theory of Bit Vectors (arbitrary length)} *)
 175
 176 module BV_Gen
 177
 178   use export bool.Bool
 179   use int.Int
 180
 181   constant size : int
 182   axiom size_pos : size > 0
 183
 184   type t
 185
 186   (** `nth b n` is the `n`-th bit of `b`. Bit 0 is
 187       the least significant bit *)
 188   val function nth t int : bool
 189
 190   axiom nth_out_of_bound: forall x n. n < 0 \/ n >= size -> nth x n = False
 191
 192   constant zeros : t
 193   axiom Nth_zeros:
 194     forall n:int. nth zeros n = False
 195   meta "remove_unused:dependency" axiom Nth_zeros, function zeros
 196
 197   constant one : t
 198
 199   constant ones : t
 200   axiom Nth_ones:
 201     forall n. 0 <= n < size -> nth ones n = True
 202   meta "remove_unused:dependency" axiom Nth_ones, function ones
 203
 204   (** Bitwise operators *)
 205
 206   (* /!\ NOTE : both bw_and and bw_or don't need guard on n because of
 207   nth out of bound axiom *)
 208   val function bw_and (v1 v2 : t) : t
 209   axiom Nth_bw_and:
 210     forall v1 v2:t, n:int. 0 <= n < size ->
 211       nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)
 212   meta "remove_unused:dependency" axiom Nth_bw_and, function bw_and
 213
 214   val function bw_or (v1 v2 : t) : t
 215   axiom Nth_bw_or:
 216     forall v1 v2:t, n:int. 0 <= n < size ->
 217       nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)
 218   meta "remove_unused:dependency" axiom Nth_bw_or, function bw_or
 219
 220   val function bw_xor (v1 v2 : t) : t
 221   axiom Nth_bw_xor:
 222     forall v1 v2:t, n:int. 0 <= n < size ->
 223       nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
 224   meta "remove_unused:dependency" axiom Nth_bw_xor, function bw_xor
 225
 226   val function bw_not (v : t) : t
 227   axiom Nth_bw_not:
 228     forall v:t, n:int. 0 <= n < size ->
 229       nth (bw_not v) n = notb (nth v n)
 230   meta "remove_unused:dependency" axiom Nth_bw_not, function bw_not
 231
 232   (** Shift operators *)
 233
 234   (** Warning: shift operators of an amount greater than or equal to
 235       the size are specified here, in concordance with SMTLIB. This is
 236       not necessarily the case in hardware, where the amount of the
 237       shift might be taken modulo the size, eg. `lsr x 64` might be
 238       equal to `x`, whereas in this theory it is 0.
 239   *)
 240
 241   val function lsr t int : t
 242
 243   axiom Lsr_nth_low:
 244     forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s < size ->
 245       nth (lsr b s) n = nth b (n+s)
 246   meta "remove_unused:dependency" axiom Lsr_nth_low, function lsr
 247
 248   axiom Lsr_nth_high:
 249     forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s >= size ->
 250       nth (lsr b s) n = False
 251   meta "remove_unused:dependency" axiom Lsr_nth_high, function lsr
 252
 253   lemma lsr_zeros: forall x. lsr x 0 = x
 254   meta "remove_unused:dependency" lemma lsr_zeros, function lsr
 255
 256   val function asr t int : t
 257
 258   axiom Asr_nth_low:
 259     forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s < size ->
 260       nth (asr b s) n = nth b (n+s)
 261   meta "remove_unused:dependency" axiom Asr_nth_low, function asr
 262
 263   axiom Asr_nth_high:
 264     forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s >= size ->
 265       nth (asr b s) n = nth b (size-1)
 266   meta "remove_unused:dependency" axiom Asr_nth_high, function asr
 267
 268   lemma asr_zeros: forall x. asr x 0 = x
 269   meta "remove_unused:dependency" lemma asr_zeros, function asr
 270
 271   val function lsl t int : t
 272
 273   axiom Lsl_nth_high:
 274     forall b:t,n s:int. 0 <= s <= n < size ->
 275       nth (lsl b s) n = nth b (n-s)
 276   meta "remove_unused:dependency" axiom Lsl_nth_high, function lsl
 277
 278   axiom Lsl_nth_low:
 279     forall b:t,n s:int. 0 <= n < s ->
 280       nth (lsl b s) n = False
 281   meta "remove_unused:dependency" axiom Lsl_nth_low, function lsl
 282
 283   lemma lsl_zeros: forall x. lsl x 0 = x
 284   meta "remove_unused:dependency" lemma lsl_zeros, function lsl
 285
 286   use int.EuclideanDivision
 287 (*  use int.ComputerDivision as CD*)
 288
 289   function rotate_right t int : t
 290
 291   axiom Nth_rotate_right :
 292     forall v n i. 0 <= i < size -> 0 <= n ->
 293       nth (rotate_right v n) i = nth v (mod (i + n) size)
 294   meta "remove_unused:dependency" axiom Nth_rotate_right, function rotate_right
 295
 296   function rotate_left t int : t
 297
 298   axiom Nth_rotate_left :
 299     forall v n i. 0 <= i < size -> 0 <= n ->
 300       nth (rotate_left v n) i = nth v (mod (i - n) size)
 301   meta "remove_unused:dependency" axiom Nth_rotate_left, function rotate_left
 302
 303
 304   (** Conversions from/to integers *)
 305
 306   use Pow2int
 307
 308   constant two_power_size : int
 309 (* not needed yet, since sdiv and srem are not yet realized
 310   constant two_power_size_minus_one : int
 311 *)
 312   constant max_int : int
 313
 314   axiom two_power_size_val : two_power_size = pow2 size
 315 (* not needed yet, since sdiv and srem are not yet realized
 316   axiom two_power_size_minus_one_val : two_power_size_minus_one = pow2 (size-1)
 317 *)
 318   axiom max_int_val : max_int = two_power_size - 1
 319
 320   predicate is_signed_positive t
 321
 322   function to_uint t : int
 323   val to_uint (x:t) : int  ensures { result = to_uint x }
 324   val function of_int int : t
 325
 326   function to_int (x:t) : int =
 327     if (is_signed_positive x) then (to_uint x) else (- (two_power_size - (to_uint x)))
 328   val to_int (x:t) : int ensures { result = to_int x }
 329
 330   axiom to_uint_extensionality :
 331     forall v,v':t. to_uint v = to_uint v' -> v = v'
 332   meta "remove_unused:dependency" axiom to_uint_extensionality, function to_uint
 333
 334   axiom to_int_extensionality:
 335     forall v,v':t. to_int v = to_int v' -> v = v'
 336   meta "remove_unused:dependency" axiom to_int_extensionality, function to_int
 337
 338 (*  *)
 339   predicate uint_in_range (i : int) = (Int.(<=) 0 i) /\ (Int.(<=) i max_int)
 340 (*  *)
 341
 342   axiom to_uint_bounds :
 343 (*
 344     forall v:t. uint_in_range (to_uint v)
 345 *)
 346     forall v:t. 0 <= to_uint v < two_power_size
 347   meta "remove_unused:dependency" axiom to_uint_bounds, function to_uint
 348
 349   axiom to_uint_of_int :
 350     forall i. 0 <= i < two_power_size -> to_uint (of_int i) = i
 351   meta "remove_unused:dependency" axiom to_uint_of_int, function to_uint
 352   meta "remove_unused:dependency" axiom to_uint_of_int, function of_int
 353
 354 (* not yet realized
 355   axiom to_int_bounds :
 356     forall v:t. - two_power_size_minus_one <= to_int v < two_power_size_minus_one
 357
 358   axiom to_int_of_int :
 359     forall i. - two_power_size_minus_one <= i < two_power_size_minus_one -> to_int (of_int i) = i
 360 *)
 361
 362   constant size_bv : t
 363
 364   axiom to_uint_size_bv : to_uint size_bv = size
 365   axiom to_uint_zeros   : to_uint zeros = 0
 366   axiom to_uint_one     : to_uint one = 1
 367   axiom to_uint_ones    : to_uint ones = max_int
 368
 369   (** comparison operators *)
 370
 371   use export why3.WellFounded.WellFounded
 372
 373   let predicate ult (x y : t) =
 374     Int.(<) (to_uint x) (to_uint y)
 375
 376   (* note : the following must be a lemma so that it is cloned in the instances *)
 377   lemma ult_wf : well_founded ult
 378   meta "vc:proved_wf" predicate ult, lemma ult_wf
 379   meta "remove_unused:dependency" lemma ult_wf, predicate ult
 380
 381   let predicate ule (x y : t) =
 382     Int.(<=) (to_uint x) (to_uint y)
 383
 384   let predicate ugt (x y : t) =
 385     Int.(>) (to_uint x) (to_uint y)
 386
 387   lemma ugt_wf : well_founded ugt
 388   meta "vc:proved_wf" predicate ugt, lemma ugt_wf
 389   meta "remove_unused:dependency" lemma ugt_wf, predicate ugt
 390
 391   let predicate uge (x y : t) =
 392     Int.(>=) (to_uint x) (to_uint y)
 393
 394   let predicate slt (v1 v2 : t) =
 395     Int.(<) (to_int v1) (to_int v2)
 396
 397   lemma slt_wf : well_founded slt
 398   meta "vc:proved_wf" predicate slt, lemma slt_wf
 399   meta "remove_unused:dependency" lemma slt_wf, predicate slt
 400
 401 let predicate sle (v1 v2 : t) =
 402     Int.(<=) (to_int v1) (to_int v2)
 403
 404   let predicate sgt (v1 v2 : t) =
 405     Int.(>) (to_int v1) (to_int v2)
 406
 407   lemma sgt_wf : well_founded sgt
 408   meta "vc:proved_wf" predicate sgt, lemma sgt_wf
 409   meta "remove_unused:dependency" lemma sgt_wf, predicate sgt
 410
 411   let predicate sge (v1 v2 : t) =
 412     Int.(>=) (to_int v1) (to_int v2)
 413
 414   axiom positive_is_ge_zeros:
 415     forall x. is_signed_positive x <-> sge x zeros
 416   meta "remove_unused:dependency" axiom positive_is_ge_zeros, predicate sge
 417   meta "remove_unused:dependency" axiom positive_is_ge_zeros, predicate is_signed_positive
 418
 419   (** Arithmetic operators *)
 420
 421   val function add (v1 v2 : t) : t
 422   axiom to_uint_add:
 423     forall v1 v2. to_uint (add v1 v2) =  mod (Int.(+) (to_uint v1) (to_uint v2)) two_power_size
 424   meta "remove_unused:dependency" axiom to_uint_add, function add
 425   lemma to_uint_add_bounded:
 426     forall v1 v2.
 427       to_uint v1 + to_uint v2 < two_power_size ->
 428       to_uint (add v1 v2) = to_uint v1 + to_uint v2
 429   meta "remove_unused:dependency" lemma to_uint_add_bounded, function add
 430   lemma to_uint_add_overflow:
 431     forall v1 v2.
 432       to_uint v1 + to_uint v2 >= two_power_size ->
 433       to_uint (add v1 v2) = to_uint v1 + to_uint v2 - two_power_size
 434   meta "remove_unused:dependency" lemma to_uint_add_overflow, function add
 435
 436   val function sub (v1 v2 : t) : t
 437   axiom to_uint_sub:
 438     forall v1 v2. to_uint (sub v1 v2) = mod (Int.(-) (to_uint v1) (to_uint v2)) two_power_size
 439   meta "remove_unused:dependency" axiom to_uint_sub  , function sub
 440   lemma to_uint_sub_bounded:
 441     forall v1 v2.
 442       0 <= to_uint v1 - to_uint v2 ->
 443       to_uint (sub v1 v2) = to_uint v1 - to_uint v2
 444   meta "remove_unused:dependency" lemma to_uint_sub_bounded, function sub
 445   lemma to_uint_sub_overflow:
 446     forall v1 v2.
 447       0 > to_uint v1 - to_uint v2 ->
 448       to_uint (sub v1 v2) = to_uint v1 - to_uint v2 + two_power_size
 449   meta "remove_unused:dependency" lemma to_uint_sub_overflow, function sub
 450
 451   val function neg (v1 : t) : t
 452   axiom to_uint_neg:
 453     forall v. to_uint (neg v) = mod (Int.(-_) (to_uint v)) two_power_size
 454   meta "remove_unused:dependency" axiom to_uint_neg, function neg
 455   lemma to_uint_neg_no_mod:
 456     forall v. to_uint (neg v) =
 457       if v = zeros then 0 else two_power_size - to_uint v
 458   meta "remove_unused:dependency" lemma to_uint_neg_no_mod, function neg
 459
 460   val function mul (v1 v2 : t) : t
 461   axiom to_uint_mul:
 462     forall v1 v2. to_uint (mul v1 v2) = mod (Int.( * ) (to_uint v1) (to_uint v2)) two_power_size
 463   meta "remove_unused:dependency" axiom to_uint_mul, function mul
 464   lemma to_uint_mul_bounded:
 465     forall v1 v2.
 466       to_uint v1 * to_uint v2 < two_power_size ->
 467       to_uint (mul v1 v2) = to_uint v1 * to_uint v2
 468   meta "remove_unused:dependency" lemma to_uint_mul_bounded, function mul
 469
 470   val function udiv (v1 v2 : t) : t
 471   axiom to_uint_udiv:
 472     forall v1 v2. to_uint (udiv v1 v2) = div (to_uint v1) (to_uint v2)
 473   meta "remove_unused:dependency" axiom to_uint_udiv, function udiv
 474
 475   val function urem (v1 v2 : t) : t
 476   axiom to_uint_urem:
 477     forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
 478   meta "remove_unused:dependency" axiom to_uint_urem, function urem
 479
 480   val function sdiv (v1 v2 : t) : t
 481 (* not yet realized
 482   axiom to_int_sdiv:
 483     forall v1 v2. to_int (sdiv v1 v2) = CD.mod (CD.div (to_int v1) (to_int v2)) two_power_size
 484   axiom to_int_sdiv_bounded:
 485     forall v1 v2.
 486     v1 <> (lsl one (size-1)) \/ v2 <> ones ->
 487     to_int (sdiv v1 v2) = CD.div (to_int v1) (to_int v2)
 488 *)
 489
 490   val function srem (v1 v2 : t) : t
 491 (* not yet realized
 492   axiom to_int_srem:
 493     forall v1 v2. to_int (srem v1 v2) = CD.mod (to_int v1) (to_int v2)
 494 *)
 495
 496   (** Bitvector alternatives for shifts, rotations and nth *)
 497
 498   (** logical shift right *)
 499   val function lsr_bv t t : t
 500
 501   axiom lsr_bv_is_lsr:
 502     forall x n.
 503       lsr_bv x n = lsr x (to_uint n)
 504   meta "remove_unused:dependency" axiom lsr_bv_is_lsr, function lsr_bv
 505
 506   axiom to_uint_lsr:
 507     forall v n : t.
 508       to_uint (lsr_bv v n) = div (to_uint v) (pow2 ( to_uint n ))
 509   meta "remove_unused:dependency" axiom to_uint_lsr, function lsr_bv
 510
 511   (** arithmetic shift right *)
 512   val function asr_bv t t : t
 513
 514   axiom asr_bv_is_asr:
 515     forall x n.
 516       asr_bv x n = asr x (to_uint n)
 517   meta "remove_unused:dependency" axiom asr_bv_is_asr, function asr_bv
 518
 519   (** logical shift left *)
 520   val function lsl_bv t t : t
 521
 522   axiom lsl_bv_is_lsl:
 523     forall x n.
 524       lsl_bv x n = lsl x (to_uint n)
 525   meta "remove_unused:dependency" axiom lsl_bv_is_lsl, function lsl_bv
 526
 527   axiom to_uint_lsl:
 528     forall v n : t.
 529          to_uint (lsl_bv v n) = mod (Int.( * ) (to_uint v) (pow2 (to_uint n))) two_power_size
 530   meta "remove_unused:dependency" axiom to_uint_lsl, function lsl_bv
 531
 532   (** rotations *)
 533
 534   val function rotate_right_bv (v n : t) : t
 535
 536   val function rotate_left_bv (v n : t) : t
 537
 538   axiom rotate_left_bv_is_rotate_left :
 539     forall v n. rotate_left_bv v n = rotate_left v (to_uint n)
 540   meta "remove_unused:dependency" axiom rotate_left_bv_is_rotate_left, function rotate_left_bv
 541   meta "remove_unused:dependency" axiom rotate_left_bv_is_rotate_left, function rotate_left
 542
 543   axiom rotate_right_bv_is_rotate_right :
 544     forall v n. rotate_right_bv v n = rotate_right v (to_uint n)
 545   meta "remove_unused:dependency" axiom rotate_right_bv_is_rotate_right, function rotate_right_bv
 546   meta "remove_unused:dependency" axiom rotate_right_bv_is_rotate_right, function rotate_right
 547
 548   val function nth_bv t t: bool
 549
 550   axiom nth_bv_def:
 551     forall x i.
 552       nth_bv x i = not (bw_and (lsr_bv x i) one = zeros)
 553   meta "remove_unused:dependency" axiom nth_bv_def, function nth_bv
 554
 555   axiom Nth_bv_is_nth:
 556     forall x i.
 557       nth x (to_uint i) = nth_bv x i
 558   meta "remove_unused:dependency" axiom Nth_bv_is_nth, function nth_bv
 559   meta "remove_unused:dependency" axiom Nth_bv_is_nth, function nth
 560
 561   axiom Nth_bv_is_nth2:
 562     forall x i. 0 <= i < two_power_size ->
 563       nth_bv x (of_int i) = nth x i
 564   meta "remove_unused:dependency" axiom Nth_bv_is_nth2, function nth_bv
 565   meta "remove_unused:dependency" axiom Nth_bv_is_nth2, function nth
 566
 567   (** equality axioms *)
 568
 569   predicate eq_sub_bv t t t t
 570
 571   axiom eq_sub_bv_def: forall a b i n.
 572     let mask = lsl_bv (sub (lsl_bv one n) one) i in
 573       eq_sub_bv a b i n = (bw_and b mask = bw_and a mask)
 574   meta "remove_unused:dependency" axiom eq_sub_bv_def, predicate eq_sub_bv
 575
 576   predicate eq_sub (a b:t) (i n:int) =
 577     forall j. i <= j < i + n -> nth a j = nth b j
 578
 579   axiom eq_sub_equiv: forall a b i n:t.
 580       eq_sub    a b (to_uint i) (to_uint n)
 581   <-> eq_sub_bv a b i n
 582   meta "remove_unused:dependency" axiom eq_sub_equiv, predicate eq_sub_bv
 583   meta "remove_unused:dependency" axiom eq_sub_equiv, predicate eq_sub
 584
 585   predicate (==) (v1 v2 : t) =
 586     eq_sub v1 v2 0 size
 587
 588   axiom Extensionality [@W:non_conservative_extension:N] :
 589     forall x y : t [x == y]. x == y -> x = y
 590   meta "remove_unused:dependency" axiom Extensionality, predicate (==)
 591
 592   val eq (v1 v2 : t) : bool
 593     ensures { result <-> v1 = v2 }
 594
 595 end
 596
 597 (** {2 Bit Vectors of common sizes, 8/16/32/64/128/256} *)
 598
 599 module BV256
 600   constant size           : int = 256
 601   constant two_power_size : int = 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000
 602
 603   use int.Int as Int (* needed to use range types *)
 604
 605   type t = < range 0 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF >
 606
 607   constant zeros : t = 0x0
 608   constant one : t = 0x1
 609   constant ones : t = 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF
 610
 611   clone export BV_Gen with
 612     type t = t,
 613     function to_uint = t'int,
 614     constant size = size,
 615     constant two_power_size = two_power_size,
 616     constant max_int = t'maxInt,
 617     constant zeros = zeros,
 618     constant one,
 619     constant ones,
 620     goal size_pos,
 621     goal two_power_size_val,
 622     goal max_int_val,
 623     axiom . (* should this be "lemma"? "goal"? *)
 624
 625 end
 626
 627 module BV128
 628   constant size           : int = 128
 629   constant two_power_size : int = 0x1_0000_0000_0000_0000_0000_0000_0000_0000
 630
 631   use int.Int as Int (* needed to use range types *)
 632
 633   type t = < range 0 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF >
 634
 635   constant zeros : t = 0x0
 636   constant one : t = 0x1
 637   constant ones : t = 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF
 638
 639   clone export BV_Gen with
 640     type t = t,
 641     function to_uint = t'int,
 642     constant size = size,
 643     constant two_power_size = two_power_size,
 644     constant max_int = t'maxInt,
 645     constant zeros,
 646     constant one,
 647     constant ones,
 648     goal size_pos,
 649     goal two_power_size_val,
 650     goal max_int_val,
 651     axiom . (* should this be "lemma"? "goal"? *)
 652
 653 end
 654
 655 module BV64
 656   constant size           : int = 64
 657   constant two_power_size : int = 0x1_0000_0000_0000_0000
 658
 659   use int.Int as Int (* needed to use range types *)
 660
 661   type t = < range 0 0xFFFF_FFFF_FFFF_FFFF >
 662
 663   constant zeros : t = 0x0
 664   constant one : t = 0x1
 665   constant ones : t = 0xFFFF_FFFF_FFFF_FFFF
 666
 667   clone export BV_Gen with
 668     type t = t,
 669     function to_uint = t'int,
 670     constant size = size,
 671     constant two_power_size = two_power_size,
 672     constant max_int = t'maxInt,
 673     constant zeros,
 674     constant one,
 675     constant ones,
 676     goal size_pos,
 677     goal two_power_size_val,
 678     goal max_int_val,
 679     axiom . (* should this be "lemma"? "goal"? *)
 680
 681 end
 682
 683 module BV32
 684   constant size           : int = 32
 685   constant two_power_size : int = 0x1_0000_0000
 686
 687   use int.Int as Int (* needed to use range types *)
 688
 689   type t = < range 0 0xFFFF_FFFF >
 690
 691   constant zeros : t = 0x0
 692   constant one : t = 0x1
 693   constant ones : t = 0xFFFF_FFFF
 694
 695   clone export BV_Gen with
 696     type t = t,
 697     function to_uint = t'int,
 698     constant size = size,
 699     constant two_power_size = two_power_size,
 700     constant max_int = t'maxInt,
 701     constant zeros,
 702     constant one,
 703     constant ones,
 704     goal size_pos,
 705     goal two_power_size_val,
 706     goal max_int_val,
 707     axiom . (* should this be "lemma"? "goal"? *)
 708
 709 end
 710
 711 module BV16
 712   constant size : int = 16
 713   constant two_power_size : int = 0x1_0000
 714
 715   use int.Int as Int (* needed to use range types *)
 716
 717   type t = < range 0 0xFFFF >
 718
 719   constant zeros : t = 0x0
 720   constant one : t = 0x1
 721   constant ones : t = 0xFFFF
 722
 723   clone export BV_Gen with
 724     type t = t,
 725     function to_uint = t'int,
 726     constant size = size,
 727     constant two_power_size = two_power_size,
 728     constant max_int = t'maxInt,
 729     constant zeros,
 730     constant one,
 731     constant ones,
 732     goal size_pos,
 733     goal two_power_size_val,
 734     goal max_int_val,
 735     axiom . (* should this be "lemma"? "goal"? *)
 736
 737 end
 738
 739 module BV8
 740   constant size           : int = 8
 741   constant two_power_size : int = 0x1_00
 742
 743   use int.Int as Int (* needed to use range types *)
 744
 745   type t = < range 0 0xFF >
 746
 747   constant zeros : t = 0x0
 748   constant one : t = 0x1
 749   constant ones : t = 0xFF
 750
 751   clone export BV_Gen with
 752     type t = t,
 753     function to_uint = t'int,
 754     constant size = size,
 755     constant two_power_size = two_power_size,
 756     constant max_int = t'maxInt,
 757     constant zeros,
 758     constant one,
 759     constant ones,
 760     goal size_pos,
 761     goal two_power_size_val,
 762     goal max_int_val,
 763     axiom . (* should this be "lemma"? "goal"? *)
 764
 765 end
 766
 767 (** {2 Generic Converter} *)
 768
 769 module BVConverter_Gen
 770
 771   type bigBV
 772   type smallBV
 773
 774   predicate in_small_range bigBV
 775
 776   function to_uint_small smallBV : int
 777   function to_uint_big bigBV : int
 778
 779   val function toBig smallBV : bigBV   (* unsigned, that is "zero extend" *)
 780   val function stoBig smallBV : bigBV  (* signed, that is "sign extend" *)
 781   val function toSmall bigBV : smallBV
 782
 783   axiom toSmall_to_uint :
 784     forall x:bigBV. in_small_range x ->
 785       to_uint_big x = to_uint_small (toSmall x)
 786
 787   axiom toBig_to_uint :
 788     forall x:smallBV.
 789       to_uint_small x = to_uint_big (toBig x)
 790
 791   (* TODO: specify stoBig by axioms too *)
 792
 793 end
 794
 795 (** {2 Converters of common size_bvs} *)
 796
 797 module BVConverter_128_256
 798   use BV128 as BV128
 799   use BV256 as BV256
 800
 801   predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF:BV256.t)
 802
 803   clone export BVConverter_Gen with
 804     type bigBV = BV256.t,
 805     type smallBV = BV128.t,
 806     predicate in_small_range = in_range,
 807     function to_uint_small = BV128.t'int,
 808     function to_uint_big = BV256.t'int,
 809     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 810     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 811 end
 812
 813 module BVConverter_64_256
 814   use BV64 as BV64
 815   use BV256 as BV256
 816
 817   predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF_FFFF_FFFF:BV256.t)
 818
 819   clone export BVConverter_Gen with
 820     type bigBV = BV256.t,
 821     type smallBV = BV64.t,
 822     predicate in_small_range = in_range,
 823     function to_uint_small = BV64.t'int,
 824     function to_uint_big = BV256.t'int,
 825     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 826     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 827 end
 828
 829 module BVConverter_32_256
 830   use BV32 as BV32
 831   use BV256 as BV256
 832
 833   predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF:BV256.t)
 834
 835   clone export BVConverter_Gen with
 836     type bigBV = BV256.t,
 837     type smallBV = BV32.t,
 838     predicate in_small_range = in_range,
 839     function to_uint_small = BV32.t'int,
 840     function to_uint_big = BV256.t'int,
 841     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 842     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 843 end
 844
 845 module BVConverter_16_256
 846   use BV16 as BV16
 847   use BV256 as BV256
 848
 849   predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF:BV256.t)
 850
 851   clone export BVConverter_Gen with
 852     type bigBV = BV256.t,
 853     type smallBV = BV16.t,
 854     predicate in_small_range = in_range,
 855     function to_uint_small = BV16.t'int,
 856     function to_uint_big = BV256.t'int,
 857     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 858     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 859 end
 860
 861 module BVConverter_8_256
 862   use BV8 as BV8
 863   use BV256 as BV256
 864
 865   predicate in_range (b : BV256.t) = BV256.ule b (0xFF:BV256.t)
 866
 867   clone export BVConverter_Gen with
 868     type bigBV = BV256.t,
 869     type smallBV = BV8.t,
 870     predicate in_small_range = in_range,
 871     function to_uint_small = BV8.t'int,
 872     function to_uint_big = BV256.t'int,
 873     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 874     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 875 end
 876
 877 module BVConverter_64_128
 878   use BV64 as BV64
 879   use BV128 as BV128
 880
 881   predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF_FFFF_FFFF_FFFF:BV128.t)
 882
 883   clone export BVConverter_Gen with
 884     type bigBV = BV128.t,
 885     type smallBV = BV64.t,
 886     predicate in_small_range = in_range,
 887     function to_uint_small = BV64.t'int,
 888     function to_uint_big = BV128.t'int,
 889     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 890     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 891 end
 892
 893 module BVConverter_32_128
 894   use BV32 as BV32
 895   use BV128 as BV128
 896
 897   predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF_FFFF:BV128.t)
 898
 899   clone export BVConverter_Gen with
 900     type bigBV = BV128.t,
 901     type smallBV = BV32.t,
 902     predicate in_small_range = in_range,
 903     function to_uint_small = BV32.t'int,
 904     function to_uint_big = BV128.t'int,
 905     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 906     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 907 end
 908
 909 module BVConverter_16_128
 910   use BV16 as BV16
 911   use BV128 as BV128
 912
 913   predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF:BV128.t)
 914
 915   clone export BVConverter_Gen with
 916     type bigBV = BV128.t,
 917     type smallBV = BV16.t,
 918     predicate in_small_range = in_range,
 919     function to_uint_small = BV16.t'int,
 920     function to_uint_big = BV128.t'int,
 921     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 922     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 923 end
 924
 925 module BVConverter_8_128
 926   use BV8 as BV8
 927   use BV128 as BV128
 928
 929   predicate in_range (b : BV128.t) = BV128.ule b (0xFF:BV128.t)
 930
 931   clone export BVConverter_Gen with
 932     type bigBV = BV128.t,
 933     type smallBV = BV8.t,
 934     predicate in_small_range = in_range,
 935     function to_uint_small = BV8.t'int,
 936     function to_uint_big = BV128.t'int,
 937     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 938     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 939 end
 940
 941 module BVConverter_32_64
 942   use BV32 as BV32
 943   use BV64 as BV64
 944
 945   predicate in_range (b : BV64.t) = BV64.ule b (0xFFFF_FFFF:BV64.t)
 946
 947   clone export BVConverter_Gen with
 948     type bigBV = BV64.t,
 949     type smallBV = BV32.t,
 950     predicate in_small_range = in_range,
 951     function to_uint_small = BV32.t'int,
 952     function to_uint_big = BV64.t'int,
 953     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 954     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 955 end
 956
 957 module BVConverter_16_64
 958   use BV16 as BV16
 959   use BV64 as BV64
 960
 961   predicate in_range (b : BV64.t) = BV64.ule b (0xFFFF:BV64.t)
 962
 963   clone export BVConverter_Gen with
 964     type bigBV = BV64.t,
 965     type smallBV = BV16.t,
 966     predicate in_small_range = in_range,
 967     function to_uint_small = BV16.t'int,
 968     function to_uint_big = BV64.t'int,
 969     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 970     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 971 end
 972
 973 module BVConverter_8_64
 974   use BV8 as BV8
 975   use BV64 as BV64
 976
 977   predicate in_range (b : BV64.t) = BV64.ule b (0xFF:BV64.t)
 978
 979   clone export BVConverter_Gen with
 980     type bigBV = BV64.t,
 981     type smallBV = BV8.t,
 982     predicate in_small_range = in_range,
 983     function to_uint_small = BV8.t'int,
 984     function to_uint_big = BV64.t'int,
 985     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
 986     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
 987 end
 988
 989 module BVConverter_16_32
 990   use BV16 as BV16
 991   use BV32 as BV32
 992
 993   predicate in_range (b : BV32.t) = BV32.ule b (0xFFFF:BV32.t)
 994
 995   clone export BVConverter_Gen with
 996     type bigBV = BV32.t,
 997     type smallBV = BV16.t,
 998     predicate in_small_range = in_range,
 999     function to_uint_small = BV16.t'int,
1000     function to_uint_big = BV32.t'int,
1001     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
1002     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
1003 end
1004
1005 module BVConverter_8_32
1006   use BV8 as BV8
1007   use BV32 as BV32
1008
1009   predicate in_range (b : BV32.t) = BV32.ule b (0xFF:BV32.t)
1010
1011   clone export BVConverter_Gen with
1012     type bigBV = BV32.t,
1013     type smallBV = BV8.t,
1014     predicate in_small_range = in_range,
1015     function to_uint_small = BV8.t'int,
1016     function to_uint_big = BV32.t'int,
1017     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
1018     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
1019 end
1020
1021 module BVConverter_8_16
1022   use BV8 as BV8
1023   use BV16 as BV16
1024
1025   predicate in_range (b : BV16.t) = BV16.ule b (0xFF:BV16.t)
1026
1027   clone export BVConverter_Gen with
1028     type bigBV = BV16.t,
1029     type smallBV = BV8.t,
1030     predicate in_small_range = in_range,
1031     function to_uint_small = BV8.t'int,
1032     function to_uint_big = BV16.t'int,
1033     axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
1034     axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
1035 end