(** {1 Bit Vectors} *)

(** {2 Powers of two} *)

module Pow2int

  use int.Int

  function pow2 (i:int) : int

  axiom Power_0 : pow2 0 = 1
  meta "remove_unused:dependency" axiom Power_0, function pow2

  axiom Power_s : forall n: int. n >= 0 -> pow2 (n+1) = 2 * pow2 n
  meta "remove_unused:dependency" axiom Power_s, function pow2

  lemma Power_1 : pow2 1 = 2
  meta "remove_unused:dependency" lemma Power_1, function pow2

  lemma Power_sum :
    forall n m: int. n >= 0 /\ m >= 0 -> pow2 (n+m) = pow2 n * pow2 m
  meta "remove_unused:dependency" lemma Power_sum, function pow2

  lemma pow2pos: forall i:int. i >= 0 -> pow2 i > 0
  meta "remove_unused:dependency" lemma pow2pos, function pow2

  lemma pow2_0: pow2 0   =                  0x1
  lemma pow2_1: pow2 1   =                  0x2
  lemma pow2_2: pow2 2   =                  0x4
  lemma pow2_3: pow2 3   =                  0x8
  lemma pow2_4: pow2 4   =                 0x10
  lemma pow2_5: pow2 5   =                 0x20
  lemma pow2_6: pow2 6   =                 0x40
  lemma pow2_7: pow2 7   =                 0x80
  lemma pow2_8: pow2 8   =                0x100
  lemma pow2_9: pow2 9   =                0x200
  lemma pow2_10: pow2 10 =                0x400
  lemma pow2_11: pow2 11 =                0x800
  lemma pow2_12: pow2 12 =               0x1000
  lemma pow2_13: pow2 13 =               0x2000
  lemma pow2_14: pow2 14 =               0x4000
  lemma pow2_15: pow2 15 =               0x8000
  lemma pow2_16: pow2 16 =              0x10000
  lemma pow2_17: pow2 17 =              0x20000
  lemma pow2_18: pow2 18 =              0x40000
  lemma pow2_19: pow2 19 =              0x80000
  lemma pow2_20: pow2 20 =             0x100000
  lemma pow2_21: pow2 21 =             0x200000
  lemma pow2_22: pow2 22 =             0x400000
  lemma pow2_23: pow2 23 =             0x800000
  lemma pow2_24: pow2 24 =            0x1000000
  lemma pow2_25: pow2 25 =            0x2000000
  lemma pow2_26: pow2 26 =            0x4000000
  lemma pow2_27: pow2 27 =            0x8000000
  lemma pow2_28: pow2 28 =           0x10000000
  lemma pow2_29: pow2 29 =           0x20000000
  lemma pow2_30: pow2 30 =           0x40000000
  lemma pow2_31: pow2 31 =           0x80000000
  lemma pow2_32: pow2 32 =          0x100000000
  lemma pow2_33: pow2 33 =          0x200000000
  lemma pow2_34: pow2 34 =          0x400000000
  lemma pow2_35: pow2 35 =          0x800000000
  lemma pow2_36: pow2 36 =         0x1000000000
  lemma pow2_37: pow2 37 =         0x2000000000
  lemma pow2_38: pow2 38 =         0x4000000000
  lemma pow2_39: pow2 39 =         0x8000000000
  lemma pow2_40: pow2 40 =        0x10000000000
  lemma pow2_41: pow2 41 =        0x20000000000
  lemma pow2_42: pow2 42 =        0x40000000000
  lemma pow2_43: pow2 43 =        0x80000000000
  lemma pow2_44: pow2 44 =       0x100000000000
  lemma pow2_45: pow2 45 =       0x200000000000
  lemma pow2_46: pow2 46 =       0x400000000000
  lemma pow2_47: pow2 47 =       0x800000000000
  lemma pow2_48: pow2 48 =      0x1000000000000
  lemma pow2_49: pow2 49 =      0x2000000000000
  lemma pow2_50: pow2 50 =      0x4000000000000
  lemma pow2_51: pow2 51 =      0x8000000000000
  lemma pow2_52: pow2 52 =     0x10000000000000
  lemma pow2_53: pow2 53 =     0x20000000000000
  lemma pow2_54: pow2 54 =     0x40000000000000
  lemma pow2_55: pow2 55 =     0x80000000000000
  lemma pow2_56: pow2 56 =    0x100000000000000
  lemma pow2_57: pow2 57 =    0x200000000000000
  lemma pow2_58: pow2 58 =    0x400000000000000
  lemma pow2_59: pow2 59 =    0x800000000000000
  lemma pow2_60: pow2 60 =   0x1000000000000000
  lemma pow2_61: pow2 61 =   0x2000000000000000
  lemma pow2_62: pow2 62 =   0x4000000000000000
  lemma pow2_63: pow2 63 =   0x8000000000000000
  lemma pow2_64: pow2 64 =  0x10000000000000000

  meta "remove_unused:dependency" lemma pow2_0, function pow2
  meta "remove_unused:dependency" lemma pow2_1, function pow2
  meta "remove_unused:dependency" lemma pow2_2, function pow2
  meta "remove_unused:dependency" lemma pow2_3, function pow2
  meta "remove_unused:dependency" lemma pow2_4, function pow2
  meta "remove_unused:dependency" lemma pow2_5, function pow2
  meta "remove_unused:dependency" lemma pow2_6, function pow2
  meta "remove_unused:dependency" lemma pow2_7, function pow2
  meta "remove_unused:dependency" lemma pow2_8, function pow2
  meta "remove_unused:dependency" lemma pow2_9, function pow2
  meta "remove_unused:dependency" lemma pow2_10, function pow2
  meta "remove_unused:dependency" lemma pow2_11, function pow2
  meta "remove_unused:dependency" lemma pow2_12, function pow2
  meta "remove_unused:dependency" lemma pow2_13, function pow2
  meta "remove_unused:dependency" lemma pow2_14, function pow2
  meta "remove_unused:dependency" lemma pow2_15, function pow2
  meta "remove_unused:dependency" lemma pow2_16, function pow2
  meta "remove_unused:dependency" lemma pow2_17, function pow2
  meta "remove_unused:dependency" lemma pow2_18, function pow2
  meta "remove_unused:dependency" lemma pow2_19, function pow2
  meta "remove_unused:dependency" lemma pow2_20, function pow2
  meta "remove_unused:dependency" lemma pow2_21, function pow2
  meta "remove_unused:dependency" lemma pow2_22, function pow2
  meta "remove_unused:dependency" lemma pow2_23, function pow2
  meta "remove_unused:dependency" lemma pow2_24, function pow2
  meta "remove_unused:dependency" lemma pow2_25, function pow2
  meta "remove_unused:dependency" lemma pow2_26, function pow2
  meta "remove_unused:dependency" lemma pow2_27, function pow2
  meta "remove_unused:dependency" lemma pow2_28, function pow2
  meta "remove_unused:dependency" lemma pow2_29, function pow2
  meta "remove_unused:dependency" lemma pow2_30, function pow2
  meta "remove_unused:dependency" lemma pow2_31, function pow2
  meta "remove_unused:dependency" lemma pow2_32, function pow2
  meta "remove_unused:dependency" lemma pow2_33, function pow2
  meta "remove_unused:dependency" lemma pow2_34, function pow2
  meta "remove_unused:dependency" lemma pow2_35, function pow2
  meta "remove_unused:dependency" lemma pow2_36, function pow2
  meta "remove_unused:dependency" lemma pow2_37, function pow2
  meta "remove_unused:dependency" lemma pow2_38, function pow2
  meta "remove_unused:dependency" lemma pow2_39, function pow2
  meta "remove_unused:dependency" lemma pow2_40, function pow2
  meta "remove_unused:dependency" lemma pow2_41, function pow2
  meta "remove_unused:dependency" lemma pow2_42, function pow2
  meta "remove_unused:dependency" lemma pow2_43, function pow2
  meta "remove_unused:dependency" lemma pow2_44, function pow2
  meta "remove_unused:dependency" lemma pow2_45, function pow2
  meta "remove_unused:dependency" lemma pow2_46, function pow2
  meta "remove_unused:dependency" lemma pow2_47, function pow2
  meta "remove_unused:dependency" lemma pow2_48, function pow2
  meta "remove_unused:dependency" lemma pow2_49, function pow2
  meta "remove_unused:dependency" lemma pow2_50, function pow2
  meta "remove_unused:dependency" lemma pow2_51, function pow2
  meta "remove_unused:dependency" lemma pow2_52, function pow2
  meta "remove_unused:dependency" lemma pow2_53, function pow2
  meta "remove_unused:dependency" lemma pow2_54, function pow2
  meta "remove_unused:dependency" lemma pow2_55, function pow2
  meta "remove_unused:dependency" lemma pow2_56, function pow2
  meta "remove_unused:dependency" lemma pow2_57, function pow2
  meta "remove_unused:dependency" lemma pow2_58, function pow2
  meta "remove_unused:dependency" lemma pow2_59, function pow2
  meta "remove_unused:dependency" lemma pow2_60, function pow2
  meta "remove_unused:dependency" lemma pow2_61, function pow2
  meta "remove_unused:dependency" lemma pow2_62, function pow2
  meta "remove_unused:dependency" lemma pow2_63, function pow2
  meta "remove_unused:dependency" lemma pow2_64, function pow2


  (*** use int.EuclideanDivision

   lemma Div_pow: forall x i:int.
     i > 0 -> pow2 (i-1) <= x < pow2 i -> div x (pow2 (i-1)) = 1

   lemma Div_div_pow: forall x i j:int.
     i > 0 /\ j > 0 -> div (div x (pow2 i)) (pow2 j) = div x (pow2 (i+j))

   lemma Mod_pow2_gen: forall x i k :int.
     0 <= k < i -> mod (div (x + pow2 i) (pow2 k)) 2 = mod (div x (pow2 k)) 2
   *)

end

(** {2 Generic theory of Bit Vectors (arbitrary length)} *)

module BV_Gen

  use export bool.Bool
  use int.Int

  constant size : int
  axiom size_pos : size > 0

  type t

  (** `nth b n` is the `n`-th bit of `b`. Bit 0 is
      the least significant bit *)
  val function nth t int : bool

  axiom nth_out_of_bound: forall x n. n < 0 \/ n >= size -> nth x n = False
  meta "remove_unused:dependency" axiom nth_out_of_bound, function nth

  constant zeros : t
  axiom Nth_zeros:
    forall n:int. nth zeros n = False
  meta "remove_unused:dependency" axiom Nth_zeros, function zeros

  constant one : t

  constant ones : t
  axiom Nth_ones:
    forall n. 0 <= n < size -> nth ones n = True
  meta "remove_unused:dependency" axiom Nth_ones, function ones

  (** Bitwise operators *)

  (* /!\ NOTE : both bw_and and bw_or don't need guard on n because of
  nth out of bound axiom *)
  val function bw_and (v1 v2 : t) : t
  axiom Nth_bw_and:
    forall v1 v2:t, n:int. 0 <= n < size ->
      nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)
  meta "remove_unused:dependency" axiom Nth_bw_and, function bw_and

  val function bw_or (v1 v2 : t) : t
  axiom Nth_bw_or:
    forall v1 v2:t, n:int. 0 <= n < size ->
      nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)
  meta "remove_unused:dependency" axiom Nth_bw_or, function bw_or

  val function bw_xor (v1 v2 : t) : t
  axiom Nth_bw_xor:
    forall v1 v2:t, n:int. 0 <= n < size ->
      nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
  meta "remove_unused:dependency" axiom Nth_bw_xor, function bw_xor

  val function bw_not (v : t) : t
  axiom Nth_bw_not:
    forall v:t, n:int. 0 <= n < size ->
      nth (bw_not v) n = notb (nth v n)
  meta "remove_unused:dependency" axiom Nth_bw_not, function bw_not

  (** Shift operators *)

  (** Warning: shift operators of an amount greater than or equal to
      the size are specified here, in concordance with SMTLIB. This is
      not necessarily the case in hardware, where the amount of the
      shift might be taken modulo the size, eg. `lsr x 64` might be
      equal to `x`, whereas in this theory it is 0.
  *)

  val function lsr t int : t

  axiom Lsr_nth_low:
    forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s < size ->
      nth (lsr b s) n = nth b (n+s)
  meta "remove_unused:dependency" axiom Lsr_nth_low, function lsr

  axiom Lsr_nth_high:
    forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s >= size ->
      nth (lsr b s) n = False
  meta "remove_unused:dependency" axiom Lsr_nth_high, function lsr

  lemma lsr_zeros: forall x. lsr x 0 = x
  meta "remove_unused:dependency" lemma lsr_zeros, function lsr

  val function asr t int : t

  axiom Asr_nth_low:
    forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s < size ->
      nth (asr b s) n = nth b (n+s)
  meta "remove_unused:dependency" axiom Asr_nth_low, function asr

  axiom Asr_nth_high:
    forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s >= size ->
      nth (asr b s) n = nth b (size-1)
  meta "remove_unused:dependency" axiom Asr_nth_high, function asr

  lemma asr_zeros: forall x. asr x 0 = x
  meta "remove_unused:dependency" lemma asr_zeros, function asr

  val function lsl t int : t

  axiom Lsl_nth_high:
    forall b:t,n s:int. 0 <= s <= n < size ->
      nth (lsl b s) n = nth b (n-s)
  meta "remove_unused:dependency" axiom Lsl_nth_high, function lsl

  axiom Lsl_nth_low:
    forall b:t,n s:int. 0 <= n < s ->
      nth (lsl b s) n = False
  meta "remove_unused:dependency" axiom Lsl_nth_low, function lsl

  lemma lsl_zeros: forall x. lsl x 0 = x
  meta "remove_unused:dependency" lemma lsl_zeros, function lsl

  use int.EuclideanDivision
  use int.ComputerDivision as CD

  function rotate_right t int : t

  axiom Nth_rotate_right :
    forall v n i. 0 <= i < size -> 0 <= n ->
      nth (rotate_right v n) i = nth v (mod (i + n) size)
  meta "remove_unused:dependency" axiom Nth_rotate_right, function rotate_right

  function rotate_left t int : t

  axiom Nth_rotate_left :
    forall v n i. 0 <= i < size -> 0 <= n ->
      nth (rotate_left v n) i = nth v (mod (i - n) size)
  meta "remove_unused:dependency" axiom Nth_rotate_left, function rotate_left


  (** Conversions from/to integers *)

  use Pow2int

  constant two_power_size : int
  constant two_power_size_minus_one : int

  constant max_int : int

  axiom two_power_size_val : two_power_size = pow2 size
  axiom two_power_size_minus_one_val : two_power_size_minus_one = pow2 (size-1)

  axiom max_int_val : max_int = two_power_size - 1

  predicate is_signed_positive t

  function to_uint t : int
  val to_uint (x:t) : int  ensures { result = to_uint x }
  val function of_int int : t

  function to_int (x:t) : int =
    if (is_signed_positive x) then (to_uint x) else (- (two_power_size - (to_uint x)))
  val to_int (x:t) : int ensures { result = to_int x }

  axiom to_uint_extensionality :
    forall v,v':t. to_uint v = to_uint v' -> v = v'
  meta "remove_unused:dependency" axiom to_uint_extensionality, function to_uint

  axiom to_int_extensionality:
    forall v,v':t. to_int v = to_int v' -> v = v'
  meta "remove_unused:dependency" axiom to_int_extensionality, function to_int

(*  *)
  predicate uint_in_range (i : int) = (Int.(<=) 0 i) /\ (Int.(<=) i max_int)
(*  *)

  axiom to_uint_bounds :
(*
    forall v:t. uint_in_range (to_uint v)
*)
    forall v:t. 0 <= to_uint v < two_power_size
  meta "remove_unused:dependency" axiom to_uint_bounds, function to_uint

  axiom to_uint_of_int :
    forall i. 0 <= i < two_power_size -> to_uint (of_int i) = i
  meta "remove_unused:dependency" axiom to_uint_of_int, function to_uint
  meta "remove_unused:dependency" axiom to_uint_of_int, function of_int

  axiom to_int_bounds :
    forall v:t. - two_power_size_minus_one <= to_int v < two_power_size_minus_one
  meta "remove_unused:dependency" axiom to_int_bounds, function to_int

  axiom to_int_of_int :
    forall i. - two_power_size_minus_one <= i < two_power_size_minus_one -> to_int (of_int i) = i
  meta "remove_unused:dependency" axiom to_int_of_int, function of_int

  constant size_bv : t

  axiom to_uint_size_bv : to_uint size_bv = size
  axiom to_uint_zeros   : to_uint zeros = 0
  axiom to_uint_one     : to_uint one = 1
  axiom to_uint_ones    : to_uint ones = max_int

  (** comparison operators *)

  use export why3.WellFounded.WellFounded

  let predicate ult (x y : t) =
    Int.(<) (to_uint x) (to_uint y)

  (* note : the following must be a lemma so that it is cloned in the instances *)
  lemma ult_wf : well_founded ult
  meta "vc:proved_wf" predicate ult, lemma ult_wf
  meta "remove_unused:dependency" lemma ult_wf, predicate ult

  let predicate ule (x y : t) =
    Int.(<=) (to_uint x) (to_uint y)

  let predicate ugt (x y : t) =
    Int.(>) (to_uint x) (to_uint y)

  lemma ugt_wf : well_founded ugt
  meta "vc:proved_wf" predicate ugt, lemma ugt_wf
  meta "remove_unused:dependency" lemma ugt_wf, predicate ugt

  let predicate uge (x y : t) =
    Int.(>=) (to_uint x) (to_uint y)

  let predicate slt (v1 v2 : t) =
    Int.(<) (to_int v1) (to_int v2)

  lemma slt_wf : well_founded slt
  meta "vc:proved_wf" predicate slt, lemma slt_wf
  meta "remove_unused:dependency" lemma slt_wf, predicate slt

let predicate sle (v1 v2 : t) =
    Int.(<=) (to_int v1) (to_int v2)

  let predicate sgt (v1 v2 : t) =
    Int.(>) (to_int v1) (to_int v2)

  lemma sgt_wf : well_founded sgt
  meta "vc:proved_wf" predicate sgt, lemma sgt_wf
  meta "remove_unused:dependency" lemma sgt_wf, predicate sgt

  let predicate sge (v1 v2 : t) =
    Int.(>=) (to_int v1) (to_int v2)

  axiom positive_is_ge_zeros:
    forall x. is_signed_positive x <-> sge x zeros
  meta "remove_unused:dependency" axiom positive_is_ge_zeros, predicate sge
  meta "remove_unused:dependency" axiom positive_is_ge_zeros, predicate is_signed_positive

  (** Arithmetic operators *)

  val function add (v1 v2 : t) : t
  axiom to_uint_add:
    forall v1 v2. to_uint (add v1 v2) =  mod (Int.(+) (to_uint v1) (to_uint v2)) two_power_size
  meta "remove_unused:dependency" axiom to_uint_add, function add
  lemma to_uint_add_bounded:
    forall v1 v2.
      to_uint v1 + to_uint v2 < two_power_size ->
      to_uint (add v1 v2) = to_uint v1 + to_uint v2
  meta "remove_unused:dependency" lemma to_uint_add_bounded, function add
  lemma to_uint_add_overflow:
    forall v1 v2.
      to_uint v1 + to_uint v2 >= two_power_size ->
      to_uint (add v1 v2) = to_uint v1 + to_uint v2 - two_power_size
  meta "remove_unused:dependency" lemma to_uint_add_overflow, function add

  val function sub (v1 v2 : t) : t
  axiom to_uint_sub:
    forall v1 v2. to_uint (sub v1 v2) = mod (Int.(-) (to_uint v1) (to_uint v2)) two_power_size
  meta "remove_unused:dependency" axiom to_uint_sub  , function sub
  lemma to_uint_sub_bounded:
    forall v1 v2.
      0 <= to_uint v1 - to_uint v2 ->
      to_uint (sub v1 v2) = to_uint v1 - to_uint v2
  meta "remove_unused:dependency" lemma to_uint_sub_bounded, function sub
  lemma to_uint_sub_overflow:
    forall v1 v2.
      0 > to_uint v1 - to_uint v2 ->
      to_uint (sub v1 v2) = to_uint v1 - to_uint v2 + two_power_size
  meta "remove_unused:dependency" lemma to_uint_sub_overflow, function sub

  val function neg (v1 : t) : t
  axiom to_uint_neg:
    forall v. to_uint (neg v) = mod (Int.(-_) (to_uint v)) two_power_size
  meta "remove_unused:dependency" axiom to_uint_neg, function neg
  lemma to_uint_neg_no_mod:
    forall v. to_uint (neg v) =
      if v = zeros then 0 else two_power_size - to_uint v
  meta "remove_unused:dependency" lemma to_uint_neg_no_mod, function neg

  val function mul (v1 v2 : t) : t
  axiom to_uint_mul:
    forall v1 v2. to_uint (mul v1 v2) = mod (Int.( * ) (to_uint v1) (to_uint v2)) two_power_size
  meta "remove_unused:dependency" axiom to_uint_mul, function mul
  lemma to_uint_mul_bounded:
    forall v1 v2.
      to_uint v1 * to_uint v2 < two_power_size ->
      to_uint (mul v1 v2) = to_uint v1 * to_uint v2
  meta "remove_unused:dependency" lemma to_uint_mul_bounded, function mul

  val function udiv (v1 v2 : t) : t
  axiom to_uint_udiv:
    forall v1 v2. to_uint (udiv v1 v2) = div (to_uint v1) (to_uint v2)
  meta "remove_unused:dependency" axiom to_uint_udiv, function udiv

  val function urem (v1 v2 : t) : t
  axiom to_uint_urem:
    forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
  meta "remove_unused:dependency" axiom to_uint_urem, function urem

  val function sdiv (v1 v2 : t) : t
  axiom to_int_sdiv:
    forall v1 v2. to_int (sdiv v1 v2) = CD.mod (CD.div (to_int v1) (to_int v2)) two_power_size
  meta "remove_unused:dependency" axiom to_int_sdiv, function sdiv
  axiom to_int_sdiv_bounded:
    forall v1 v2.
    v1 <> (lsl one (size-1)) \/ v2 <> ones ->
    to_int (sdiv v1 v2) = CD.div (to_int v1) (to_int v2)
  meta "remove_unused:dependency" axiom to_int_sdiv_bounded, function sdiv

  val function srem (v1 v2 : t) : t
  axiom to_int_srem:
    forall v1 v2. to_int (srem v1 v2) = CD.mod (to_int v1) (to_int v2)
  meta "remove_unused:dependency" axiom to_int_srem, function srem

  (** Bitvector alternatives for shifts, rotations and nth *)

  (** logical shift right *)
  val function lsr_bv t t : t

  axiom lsr_bv_is_lsr:
    forall x n.
      lsr_bv x n = lsr x (to_uint n)
  meta "remove_unused:dependency" axiom lsr_bv_is_lsr, function lsr_bv

  axiom to_uint_lsr:
    forall v n : t.
      to_uint (lsr_bv v n) = div (to_uint v) (pow2 ( to_uint n ))
  meta "remove_unused:dependency" axiom to_uint_lsr, function lsr_bv

  (** arithmetic shift right *)
  val function asr_bv t t : t

  axiom asr_bv_is_asr:
    forall x n.
      asr_bv x n = asr x (to_uint n)
  meta "remove_unused:dependency" axiom asr_bv_is_asr, function asr_bv

  (** logical shift left *)
  val function lsl_bv t t : t

  axiom lsl_bv_is_lsl:
    forall x n.
      lsl_bv x n = lsl x (to_uint n)
  meta "remove_unused:dependency" axiom lsl_bv_is_lsl, function lsl_bv

  axiom to_uint_lsl:
    forall v n : t.
         to_uint (lsl_bv v n) = mod (Int.( * ) (to_uint v) (pow2 (to_uint n))) two_power_size
  meta "remove_unused:dependency" axiom to_uint_lsl, function lsl_bv

  (** rotations *)

  val function rotate_right_bv (v n : t) : t

  val function rotate_left_bv (v n : t) : t

  axiom rotate_left_bv_is_rotate_left :
    forall v n. rotate_left_bv v n = rotate_left v (to_uint n)
  meta "remove_unused:dependency" axiom rotate_left_bv_is_rotate_left, function rotate_left_bv
  meta "remove_unused:dependency" axiom rotate_left_bv_is_rotate_left, function rotate_left

  axiom rotate_right_bv_is_rotate_right :
    forall v n. rotate_right_bv v n = rotate_right v (to_uint n)
  meta "remove_unused:dependency" axiom rotate_right_bv_is_rotate_right, function rotate_right_bv
  meta "remove_unused:dependency" axiom rotate_right_bv_is_rotate_right, function rotate_right

  val function nth_bv t t: bool

  axiom nth_bv_def:
    forall x i.
      nth_bv x i = not (bw_and (lsr_bv x i) one = zeros)
  meta "remove_unused:dependency" axiom nth_bv_def, function nth_bv

  axiom Nth_bv_is_nth:
    forall x i.
      nth x (to_uint i) = nth_bv x i
  meta "remove_unused:dependency" axiom Nth_bv_is_nth, function nth_bv
  meta "remove_unused:dependency" axiom Nth_bv_is_nth, function nth

  axiom Nth_bv_is_nth2:
    forall x i. 0 <= i < two_power_size ->
      nth_bv x (of_int i) = nth x i
  meta "remove_unused:dependency" axiom Nth_bv_is_nth2, function nth_bv
  meta "remove_unused:dependency" axiom Nth_bv_is_nth2, function nth

  (** equality axioms *)

  predicate eq_sub_bv t t t t

  axiom eq_sub_bv_def: forall a b i n.
    let mask = lsl_bv (sub (lsl_bv one n) one) i in
      eq_sub_bv a b i n = (bw_and b mask = bw_and a mask)
  meta "remove_unused:dependency" axiom eq_sub_bv_def, predicate eq_sub_bv

  predicate eq_sub (a b:t) (i n:int) =
    forall j. i <= j < i + n -> nth a j = nth b j

  axiom eq_sub_equiv: forall a b i n:t.
      eq_sub    a b (to_uint i) (to_uint n)
  <-> eq_sub_bv a b i n
  meta "remove_unused:dependency" axiom eq_sub_equiv, predicate eq_sub_bv
  meta "remove_unused:dependency" axiom eq_sub_equiv, predicate eq_sub

  predicate (==) (v1 v2 : t) =
    eq_sub v1 v2 0 size

  axiom Extensionality [@W:non_conservative_extension:N] :
    forall x y : t [x == y]. x == y -> x = y
  meta "remove_unused:dependency" axiom Extensionality, predicate (==)

(* not a good idea to apply extensionality systematically here, since provers with built-in bitvectors will prefer using `=` directly
  this meta could be added in drivers though.

  meta extensionality predicate (==)
*)

  val eq (v1 v2 : t) : bool
    ensures { result <-> v1 = v2 }

end

(** {2 Bit Vectors of common sizes, 8/16/32/64/128/256} *)

module BV256
  constant size           : int = 256
  constant two_power_size : int =
    0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000
  constant two_power_size_minus_one : int =
      0x8000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000

  use int.Int as Int (* needed to use range types *)

  type t = < range 0 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF >

  constant zeros : t = 0x0
  constant one : t = 0x1
  constant ones : t = 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF

  clone export BV_Gen with
    type t = t,
    function to_uint = t'int,
    constant size = size,
    constant two_power_size = two_power_size,
    constant two_power_size_minus_one = two_power_size_minus_one,
    constant max_int = t'maxInt,
    constant zeros = zeros,
    constant one,
    constant ones,
    goal size_pos,
    goal two_power_size_val,
    goal two_power_size_minus_one_val,
    goal max_int_val,
    axiom . (* should this be "lemma"? "goal"? *)

end

module BV128
  constant size           : int = 128
  constant two_power_size : int =
    0x1_0000_0000_0000_0000_0000_0000_0000_0000
  constant two_power_size_minus_one : int =
      0x8000_0000_0000_0000_0000_0000_0000_0000

  use int.Int as Int (* needed to use range types *)

  type t = < range 0 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF >

  constant zeros : t = 0x0
  constant one : t = 0x1
  constant ones : t = 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF

  clone export BV_Gen with
    type t = t,
    function to_uint = t'int,
    constant size = size,
    constant two_power_size = two_power_size,
    constant two_power_size_minus_one = two_power_size_minus_one,
    constant max_int = t'maxInt,
    constant zeros,
    constant one,
    constant ones,
    goal size_pos,
    goal two_power_size_val,
    goal two_power_size_minus_one_val,
    goal max_int_val,
    axiom . (* should this be "lemma"? "goal"? *)

end

module BV64
  constant size           : int = 64
  constant two_power_size : int = 0x1_0000_0000_0000_0000
  constant two_power_size_minus_one : int = 0x8000_0000_0000_0000

  use int.Int as Int (* needed to use range types *)

  type t = < range 0 0xFFFF_FFFF_FFFF_FFFF >

  constant zeros : t = 0x0
  constant one : t = 0x1
  constant ones : t = 0xFFFF_FFFF_FFFF_FFFF

  clone export BV_Gen with
    type t = t,
    function to_uint = t'int,
    constant size = size,
    constant two_power_size = two_power_size,
    constant two_power_size_minus_one = two_power_size_minus_one,
    constant max_int = t'maxInt,
    constant zeros,
    constant one,
    constant ones,
    goal size_pos,
    goal two_power_size_val,
    goal two_power_size_minus_one_val,
    goal max_int_val,
    axiom . (* should this be "lemma"? "goal"? *)

end

module BV32
  constant size           : int = 32
  constant two_power_size : int = 0x1_0000_0000
  constant two_power_size_minus_one : int = 0x8000_0000

  use int.Int as Int (* needed to use range types *)

  type t = < range 0 0xFFFF_FFFF >

  constant zeros : t = 0x0
  constant one : t = 0x1
  constant ones : t = 0xFFFF_FFFF

  clone export BV_Gen with
    type t = t,
    function to_uint = t'int,
    constant size = size,
    constant two_power_size = two_power_size,
    constant two_power_size_minus_one = two_power_size_minus_one,
    constant max_int = t'maxInt,
    constant zeros,
    constant one,
    constant ones,
    goal size_pos,
    goal two_power_size_val,
    goal two_power_size_minus_one_val,
    goal max_int_val,
    axiom . (* should this be "lemma"? "goal"? *)

end

module BV16
  constant size : int = 16
  constant two_power_size : int = 0x1_0000
  constant two_power_size_minus_one : int = 0x8000

  use int.Int as Int (* needed to use range types *)

  type t = < range 0 0xFFFF >

  constant zeros : t = 0x0
  constant one : t = 0x1
  constant ones : t = 0xFFFF

  clone export BV_Gen with
    type t = t,
    function to_uint = t'int,
    constant size = size,
    constant two_power_size = two_power_size,
    constant two_power_size_minus_one = two_power_size_minus_one,
    constant max_int = t'maxInt,
    constant zeros,
    constant one,
    constant ones,
    goal size_pos,
    goal two_power_size_val,
    goal two_power_size_minus_one_val,
    goal max_int_val,
    axiom . (* should this be "lemma"? "goal"? *)

end

module BV8
  constant size           : int = 8
  constant two_power_size : int = 0x1_00
  constant two_power_size_minus_one : int = 0x80

  use int.Int as Int (* needed to use range types *)

  type t = < range 0 0xFF >

  constant zeros : t = 0x0
  constant one : t = 0x1
  constant ones : t = 0xFF

  clone export BV_Gen with
    type t = t,
    function to_uint = t'int,
    constant size = size,
    constant two_power_size = two_power_size,
    constant two_power_size_minus_one = two_power_size_minus_one,
    constant max_int = t'maxInt,
    constant zeros,
    constant one,
    constant ones,
    goal size_pos,
    goal two_power_size_val,
    goal two_power_size_minus_one_val,
    goal max_int_val,
    axiom . (* should this be "lemma"? "goal"? *)

end

(** {2 Generic Converter} *)

module BVConverter_Gen

  type bigBV
  type smallBV

  predicate in_small_range bigBV

  function to_uint_small smallBV : int
  function to_uint_big bigBV : int

  val function toBig smallBV : bigBV   (* unsigned, that is "zero extend" *)
  val function stoBig smallBV : bigBV  (* signed, that is "sign extend" *)
  val function toSmall bigBV : smallBV

  axiom toSmall_to_uint :
    forall x:bigBV. in_small_range x ->
      to_uint_big x = to_uint_small (toSmall x)

  axiom toBig_to_uint :
    forall x:smallBV.
      to_uint_small x = to_uint_big (toBig x)

  (* TODO: specify stoBig by axioms too *)

end

(** {2 Converters of common size_bvs} *)

module BVConverter_128_256
  use BV128 as BV128
  use BV256 as BV256

  predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF:BV256.t)

  clone export BVConverter_Gen with
    type bigBV = BV256.t,
    type smallBV = BV128.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV128.t'int,
    function to_uint_big = BV256.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_64_256
  use BV64 as BV64
  use BV256 as BV256

  predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF_FFFF_FFFF:BV256.t)

  clone export BVConverter_Gen with
    type bigBV = BV256.t,
    type smallBV = BV64.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV64.t'int,
    function to_uint_big = BV256.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_32_256
  use BV32 as BV32
  use BV256 as BV256

  predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF_FFFF:BV256.t)

  clone export BVConverter_Gen with
    type bigBV = BV256.t,
    type smallBV = BV32.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV32.t'int,
    function to_uint_big = BV256.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_16_256
  use BV16 as BV16
  use BV256 as BV256

  predicate in_range (b : BV256.t) = BV256.ule b (0xFFFF:BV256.t)

  clone export BVConverter_Gen with
    type bigBV = BV256.t,
    type smallBV = BV16.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV16.t'int,
    function to_uint_big = BV256.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_8_256
  use BV8 as BV8
  use BV256 as BV256

  predicate in_range (b : BV256.t) = BV256.ule b (0xFF:BV256.t)

  clone export BVConverter_Gen with
    type bigBV = BV256.t,
    type smallBV = BV8.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV8.t'int,
    function to_uint_big = BV256.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_64_128
  use BV64 as BV64
  use BV128 as BV128

  predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF_FFFF_FFFF_FFFF:BV128.t)

  clone export BVConverter_Gen with
    type bigBV = BV128.t,
    type smallBV = BV64.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV64.t'int,
    function to_uint_big = BV128.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_32_128
  use BV32 as BV32
  use BV128 as BV128

  predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF_FFFF:BV128.t)

  clone export BVConverter_Gen with
    type bigBV = BV128.t,
    type smallBV = BV32.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV32.t'int,
    function to_uint_big = BV128.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_16_128
  use BV16 as BV16
  use BV128 as BV128

  predicate in_range (b : BV128.t) = BV128.ule b (0xFFFF:BV128.t)

  clone export BVConverter_Gen with
    type bigBV = BV128.t,
    type smallBV = BV16.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV16.t'int,
    function to_uint_big = BV128.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_8_128
  use BV8 as BV8
  use BV128 as BV128

  predicate in_range (b : BV128.t) = BV128.ule b (0xFF:BV128.t)

  clone export BVConverter_Gen with
    type bigBV = BV128.t,
    type smallBV = BV8.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV8.t'int,
    function to_uint_big = BV128.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_32_64
  use BV32 as BV32
  use BV64 as BV64

  predicate in_range (b : BV64.t) = BV64.ule b (0xFFFF_FFFF:BV64.t)

  clone export BVConverter_Gen with
    type bigBV = BV64.t,
    type smallBV = BV32.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV32.t'int,
    function to_uint_big = BV64.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_16_64
  use BV16 as BV16
  use BV64 as BV64

  predicate in_range (b : BV64.t) = BV64.ule b (0xFFFF:BV64.t)

  clone export BVConverter_Gen with
    type bigBV = BV64.t,
    type smallBV = BV16.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV16.t'int,
    function to_uint_big = BV64.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_8_64
  use BV8 as BV8
  use BV64 as BV64

  predicate in_range (b : BV64.t) = BV64.ule b (0xFF:BV64.t)

  clone export BVConverter_Gen with
    type bigBV = BV64.t,
    type smallBV = BV8.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV8.t'int,
    function to_uint_big = BV64.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_16_32
  use BV16 as BV16
  use BV32 as BV32

  predicate in_range (b : BV32.t) = BV32.ule b (0xFFFF:BV32.t)

  clone export BVConverter_Gen with
    type bigBV = BV32.t,
    type smallBV = BV16.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV16.t'int,
    function to_uint_big = BV32.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_8_32
  use BV8 as BV8
  use BV32 as BV32

  predicate in_range (b : BV32.t) = BV32.ule b (0xFF:BV32.t)

  clone export BVConverter_Gen with
    type bigBV = BV32.t,
    type smallBV = BV8.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV8.t'int,
    function to_uint_big = BV32.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end

module BVConverter_8_16
  use BV8 as BV8
  use BV16 as BV16

  predicate in_range (b : BV16.t) = BV16.ule b (0xFF:BV16.t)

  clone export BVConverter_Gen with
    type bigBV = BV16.t,
    type smallBV = BV8.t,
    predicate in_small_range = in_range,
    function to_uint_small = BV8.t'int,
    function to_uint_big = BV16.t'int,
    axiom toSmall_to_uint, (* TODO: "lemma"? "goal"? *)
    axiom toBig_to_uint    (* TODO: "lemma"? "goal"? *)
end