(** {1 Program functions on bitvectors with preconditions}

    This module provides extra functions with pre-conditions ensuring
    the absence of overflows.

    Those pre-conditions are expressed in term of interpretation into
    mathematical integers, or using bitvectors of size 128.

*)

(** {2 Generic module, for a parametric size} *)

module BVCheck_Gen
  use int.Int

  type t

  constant size : int
  constant size_bv : t

  (* Overflow checks are performed using bitvectors of size 128. Thus
     this module cannot be cloned with a [size] > 64. *)
  axiom not_greater_than_64 : size <= 64

  constant two_power_size : int
  constant two_power_size_minus_one : int
  constant zeros           : t
  constant minus_one : t

  function to_uint t   : int
  function to_int t   : int
  function of_int  int : t

  function add  t t : t
  function sub  t t : t
  function mul  t t : t
  function udiv t t : t
  function urem t t : t
  function sdiv t t : t
  function srem t t : t

  function lsl    t int : t
  function lsl_bv t t   : t
  function lsr    t int : t
  function lsr_bv t t   : t
  function asr    t int : t
  function asr_bv t t   : t

  predicate ule t t
  predicate ult t t
  predicate uge t t
  predicate ugt t t

  predicate sle t t
  predicate slt t t
  predicate sge t t
  predicate sgt t t

  use bv.BV128 as BV128

  function sto_bv128 t : BV128.t
  function uto_bv128 t : BV128.t

  constant min_sint : t
  constant max_sint : t
  constant max_uint : t
  constant min_sint_as_bv128 : BV128.t = sto_bv128 min_sint
  constant max_sint_as_bv128 : BV128.t = sto_bv128 max_sint
  constant max_uint_as_bv128 : BV128.t = uto_bv128 max_uint

  (** unsigned addition forbidding overflows *)
  val u_add (a b:t) : t
    requires { [@expl:arithmetic overflow]
                  to_uint a + to_uint b < two_power_size
               \/ BV128.ule (BV128.add (uto_bv128 a) (uto_bv128 b)) max_uint_as_bv128 }
    ensures  { to_uint result = to_uint a + to_uint b }
    ensures  { result = add a b }

  (** signed addition forbidding overflows *)
  val s_add (a b:t) : t
    requires { [@expl:arithmetic overflow]
      - two_power_size_minus_one <= to_int a + to_int b < two_power_size_minus_one
      \/ let r = BV128.add (sto_bv128 a) (sto_bv128 b) in
         (BV128.sle min_sint_as_bv128 r /\ BV128.sle r max_sint_as_bv128) }
    ensures  { to_int result = to_int a + to_int b }
    ensures  { result = add a b }

  (** unsigned subtraction with overflow check *)
  val u_sub (a b:t) : t
    requires { [@expl:arithmetic overflow] to_uint a >= to_uint b \/ uge a b }
    ensures  { result = sub a b }
    ensures  { to_uint result = to_uint a - to_uint b }

  (** signed subtraction with overflow check *)
  val s_sub (a b:t) : t
    requires { [@expl:arithmetic overflow]
      - two_power_size_minus_one <= to_int a - to_int b < two_power_size_minus_one
      \/ let r = BV128.sub (sto_bv128 a) (sto_bv128 b) in
         (BV128.sle min_sint_as_bv128 r /\ BV128.sle r max_sint_as_bv128) }
    ensures  { result = sub a b }
    ensures  { to_int result = to_int a - to_int b }

  (** unsigned multiplication with overflow check *)
  val u_mul (a b:t) : t
    requires { [@expl:arithmetic overflow]
                  to_uint a * to_uint b < two_power_size
               \/ BV128.ule (BV128.mul (uto_bv128 a) (uto_bv128 b)) max_uint_as_bv128 }
    ensures  { result = mul a b }
    ensures  { to_int result = to_uint a * to_uint b }

  (** signed multiplication with overflow check *)
  val s_mul (a b:t) : t
    requires { [@expl:arithmetic overflow]
      - two_power_size_minus_one <= to_int a * to_int b < two_power_size_minus_one
      \/ let r = BV128.mul (sto_bv128 a) (sto_bv128 b) in
         (BV128.sle min_sint_as_bv128 r /\ BV128.sle r max_sint_as_bv128) }
    ensures  { result = mul a b }
    ensures  { to_int result = to_int a * to_int b }

  use bv.Pow2int

  (** A logical shift left requiring the second argument to be smaller than bitvector size.
      For this function we do not forbid overflow: bits can be ``lost'' on the left.
      This function corresponds to the left shifting [<<] of unsigned ints in C or Java *)
  val u_lsl (a b:t) : t
    requires { [@expl:out-of-bounds shifting]
                ult b size_bv \/ to_uint b < size }
    ensures  { result = lsl_bv a b }
    ensures  { result = lsl a (to_uint b) }

  (** Alternative logical shift left, still requiring the second argument to be smaller
      than bitvector size, but also forbidding overflow.
      This function corresponds to the left shifting [<<] of signed ints in C or Java *)
  val s_lsl (a b:t) : t
    requires { [@expl:out-of-bounds shifting]
                ult b size_bv \/ to_uint b < size }
    requires { [@expl:out-of-bounds shifting]
                sle zeros a \/ to_int a >= 0 }
    requires { [@expl:arithmetic overflow]
      (to_int a) * (pow2 (to_int b)) < two_power_size_minus_one
      \/ let r = BV128.lsl_bv (sto_bv128 a) (sto_bv128 b) in
         (BV128.sle min_sint_as_bv128 r /\ BV128.sle r max_sint_as_bv128) }
    ensures  { result = lsl_bv a b }
    ensures  { result = lsl a (to_uint b) }

  (** Logical shift right, requiring the second argument to be smaller than bitvector size.
      No overflow can occur anyway.
      This function corresponds to the (logical) right shifting [>>] of unsigned ints in C
      or Java. *)
  val u_lsr (a b:t) : t
    requires { [@expl:out-of-bounds shifting]
                ult b size_bv \/ to_uint b < size }
    ensures  { result = lsr_bv a b }
    ensures  { result = lsr a (to_uint b) }

  (** The so-called "arithmetic" shift right, requirings the second
      argument to be smaller than bitvector size.  This function
      corresponds to the arithmetic right shifting [>>>] of signed
      ints in Java, that does not exist in C. *)
  val s_asr (a b:t) : t
    requires { [@expl:out-of-bounds shifting]
                ult b size_bv \/ to_uint b < size }
    ensures  { result = asr_bv a b }
    ensures  { result = asr a (to_uint b) }

  (** The shift right function for signed int, requirings the second
      argument to be smaller than bitvector size, and that the first argument in non-negative.
      This function corresponds to the right shifting [>>] of signed ints in C. *)
  val s_asr_strict (a b:t) : t
    requires { [@expl:out-of-bounds shifting]
                ult b size_bv \/ to_uint b < size }
    requires { [@expl:out-of-bounds shifting]
                sge a zeros \/ to_int a >= 0 }
    ensures  { result = asr_bv a b }
    ensures  { result = asr a (to_uint b) }

  use int.EuclideanDivision as ED

  (** unsigned division requires the second argument to be non-zero *)
  val u_div (a b:t) : t
    requires { [@expl:division by zero] b <> zeros \/ to_uint b <> 0 }
    ensures  { to_uint result = ED.div (to_uint a) (to_uint b) }
    ensures  { result = udiv a b }

  (** unsigned remainder requires the second argument to be non-zero *)
  val u_rem (a b:t) : t
    requires { [@expl:remainder by zero] b <> zeros  \/ to_uint b <> 0 }
    ensures  { to_uint result = ED.mod (to_uint a) (to_uint b) }
    ensures  { result = urem a b }

  use int.ComputerDivision as CD

  (** signed division requires the second argument to be non-zero, but also that
      either the dividend is not [min_int] or the divisor is not [-1] *)
  val s_div (a b:t) : t
    requires { [@expl:division by zero] b <> zeros  \/ to_int b <> 0 }
    requires { [@expl:signed division overflow check] (a <> min_sint \/ b <> minus_one)
                \/ (to_int a <> to_int min_sint \/ to_int b <> -1)}
    ensures  { to_int result = CD.div (to_int a) (to_int b) }
    ensures  { result = sdiv a b }

  (** signed remainder requires the second argument to be non-zero *)
  val s_rem (a b:t) : t
    requires { [@expl:remainder by zero] b <> zeros \/ to_int b <> 0 }
    ensures  { to_int result = CD.mod (to_int a) (to_int b) }
    ensures  { result = srem a b }

  (** comparison operators have no preconditions *)
  val us_eq (a b:t) : bool
    ensures { result <-> a = b }

  val us_ne (a b:t) : bool
    ensures { result <-> a <> b }

  val u_le (a b:t) : bool
    ensures { result <-> to_uint a <= to_uint b }
    ensures { result <-> ule a b }

  val u_lt (a b:t) : bool
    ensures { result <-> to_uint a < to_uint b }
    ensures { result <-> ult a b }

  val u_ge (a b:t) : bool
    ensures { result <-> to_uint a >= to_uint b }
    ensures { result <-> uge a b }

  val u_gt (a b:t) : bool
    ensures { result <-> to_uint a > to_uint b }
    ensures { result <-> ugt a b }

  val s_le (a b:t) : bool
    ensures { result <-> to_int a <= to_int b }
    ensures { result <-> sle a b }

  val s_lt (a b:t) : bool
    ensures { result <-> to_int a < to_int b }
    ensures { result <-> slt a b }

  val s_ge (a b:t) : bool
    ensures { result <-> to_int a >= to_int b }
    ensures { result <-> sge a b }

  val s_gt (a b:t) : bool
    ensures { result <-> to_int a > to_int b }
    ensures { result <-> sgt a b }

end

(** {2 Modules for specific sizes} obtained by cloning the previous generic module *)

module BVCheck8
  use export bv.BV8

  constant minus_one : t = 0xFF
  constant min_sint : t = 0x80
  constant max_sint : t = 0x7F
  constant max_uint : t = 0xFF

  use bv.BVConverter_8_128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_size_minus_one = two_power_size_minus_one,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    function to_uint = t'int,
    function to_int = to_int,
    function of_int = of_int,
    function add = add,
    function sub = sub,
    function mul = mul,
    function udiv = udiv,
    function urem = urem,
    function sdiv = sdiv,
    function srem = srem,
    function lsl = lsl,
    function lsl_bv = lsl_bv,
    function lsr = lsr,
    function lsr_bv = lsr_bv,
    function asr = asr,
    function asr_bv = asr_bv,
    predicate ule = ule,
    predicate ult = ult,
    predicate uge = uge,
    predicate ugt = ugt,
    predicate sle = sle,
    predicate slt = slt,
    predicate sge = sge,
    predicate sgt = sgt,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end


module BVCheck16
  use export bv.BV16

  constant minus_one : t = 0xFFFF
  constant min_sint : t = 0x8000
  constant max_sint : t = 0x7FFF
  constant max_uint : t = 0xFFFF

  use bv.BVConverter_16_128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_size_minus_one = two_power_size_minus_one,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    function to_uint = t'int,
    function to_int = to_int,
    function of_int = of_int,
    function add = add,
    function sub = sub,
    function mul = mul,
    function udiv = udiv,
    function urem = urem,
    function sdiv = sdiv,
    function srem = srem,
    function lsl = lsl,
    function lsl_bv = lsl_bv,
    function lsr = lsr,
    function lsr_bv = lsr_bv,
    function asr = asr,
    function asr_bv = asr_bv,
    predicate ule = ule,
    predicate ult = ult,
    predicate uge = uge,
    predicate ugt = ugt,
    predicate sle = sle,
    predicate slt = slt,
    predicate sge = sge,
    predicate sgt = sgt,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end

module BVCheck32
  use export bv.BV32

  constant minus_one : t = 0xFFFF_FFFF
  constant min_sint : t = 0x8000_0000
  constant max_sint : t = 0x7FFF_FFFF
  constant max_uint : t = 0xFFFF_FFFF

  use bv.BVConverter_32_128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_size_minus_one = two_power_size_minus_one,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    function to_uint = t'int,
    function to_int = to_int,
    function of_int = of_int,
    function add = add,
    function sub = sub,
    function mul = mul,
    function udiv = udiv,
    function urem = urem,
    function sdiv = sdiv,
    function srem = srem,
    function lsl = lsl,
    function lsl_bv = lsl_bv,
    function lsr = lsr,
    function lsr_bv = lsr_bv,
    function asr = asr,
    function asr_bv = asr_bv,
    predicate ule = ule,
    predicate ult = ult,
    predicate uge = uge,
    predicate ugt = ugt,
    predicate sle = sle,
    predicate slt = slt,
    predicate sge = sge,
    predicate sgt = sgt,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end

module BVCheck64
  use export bv.BV64

  constant minus_one : t = 0xFFFF_FFFF_FFFF_FFFF
  constant min_sint : t = 0x8000_0000_0000_0000
  constant max_sint : t = 0x7FFF_FFFF_FFFF_FFFF
  constant max_uint : t = 0xFFFF_FFFF_FFFF_FFFF

  use bv.BVConverter_64_128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_size_minus_one = two_power_size_minus_one,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    function to_uint = t'int,
    function to_int = to_int,
    function of_int = of_int,
    function add = add,
    function sub = sub,
    function mul = mul,
    function udiv = udiv,
    function urem = urem,
    function sdiv = sdiv,
    function srem = srem,
    function lsl = lsl,
    function lsl_bv = lsl_bv,
    function lsr = lsr,
    function lsr_bv = lsr_bv,
    function asr = asr,
    function asr_bv = asr_bv,
    predicate ule = ule,
    predicate ult = ult,
    predicate uge = uge,
    predicate ugt = ugt,
    predicate sle = sle,
    predicate slt = slt,
    predicate sge = sge,
    predicate sgt = sgt,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end