Module Bitvec.M16

M16 specializes Make(struct let modulus = m16 end)

This specialization relies on a fact, that 16 bitvectors always fit into OCaml integer representation, so it avoids calls to the underlying arbitrary precision arithmetic library.

type 'a m = 'a

an abstract representation of an operation modulo some number.

val bool : bool -> t

bool x returns one if x and zero otherwise.

val int : int -> t m

int n mod m is n modulo m.

val int32 : int32 -> t m

int32 n mod m is n modulo m.

val int64 : int64 -> t m

int64 n mod m is n modulo m.

val bigint : Z.t -> t m

bigint n mod m is n modulo m.

val zero : t

zero is 0.

val one : t

one is 1.

val ones : t m

ones mod m is a bitvector of size m with all bits set

val succ : t -> t m

succ x mod m is the successor of x modulo m

val nsucc : t -> int -> t m

nsucc x n mod m is the nth successor of x modulo m

val pred : t -> t m

pred x mod m is the predecessor of x modulo m

val npred : t -> int -> t m

npred x n mod m is the nth predecessor of x modulo m

val neg : t -> t m

neg x mod m is the 2-complement of x modulo m.

val lnot : t -> t m

lnot x is the 1-complement of x modulo m.

val abs : t -> t m

abs x mod m absolute value of x modulo m.

The absolute value of x is equal to neg x if msb x and to x otherwise.

val add : t -> t -> t m

add x y mod m is x + y modulo m

val sub : t -> t -> t m

sub x y mod m is x - y modulo m

val mul : t -> t -> t m

mul x y mod m is x * y modulo m

val div : t -> t -> t m

div x y mod m is x / y modulo m,

where / is the truncating towards zero division, that returns ones m if y = 0.

val sdiv : t -> t -> t m

sdiv x y mod m is signed division of x by y modulo m,

The signed division operator is defined in terms of the div operator as follows:

                        /
                        | div x y mod m : if not mx /\ not my
                        | neg (div (neg x) y) mod m if mx /\ not my
      x sdiv y mod m = <
                        | neg (div x (neg y)) mod m if not mx /\ my
                        | div (neg x) (neg y) mod m if mx /\ my
                        \

      where mx = msb x mod m,
        and my = msb y mod m.
val rem : t -> t -> t m

rem x y mod m is the remainder of x / y modulo m.

val srem : t -> t -> t m

srem x y mod m is the signed remainder x / y modulo m.

This version of the signed remainder where the sign follows the dividend, and is defined via the rem operation as follows

                        /
                        | rem x y mod m : if not mx /\ not my
                        | neg (rem (neg x) y) mod m if mx /\ not my
      x srem y mod m = <
                        | neg (rem x (neg y)) mod m if not mx /\ my
                        | neg (rem (neg x) (neg y)) mod m if mx /\ my
                        \

      where mx = msb x mod m,
        and my = msb y mod m.
val smod : t -> t -> t m

smod x y mod m is the signed remainder of x / y modulo m.

This version of the signed remainder where the sign follows the divisor, and is defined in terms of the rem operation as follows:

                        /
                        | u if u = 0
      x smod y mod m = <
                        | v if u <> 0
                        \

                        /
                        | u if not mx /\ not my
                        | add (neg u) y mod m if mx /\ not my
                   v = <
                        | add u x mod m if not mx /\ my
                        | neg u mod m if mx /\ my
                        \

      where mx = msb x mod m,
        and my = msb y mod m,
        and u = rem s t mod m.
val nth : t -> int -> bool m

nth x n mod m is true if nth bit of x is set.

Returns msb x mod m if n >= m and lsb x mod m if n < 0

val msb : t -> bool m

msb x mod m returns the most significand bit of x.

val lsb : t -> bool m

lsb x mod m returns the least significand bit of x.

val logand : t -> t -> t m

logand x y mod m is a bitwise logical and of x and y modulo m

val logor : t -> t -> t m

logor x y mod m is a bitwise logical or of x and y modulo m.

val logxor : t -> t -> t m

logxor x y mod m is exclusive or between x and y modulo m

val lshift : t -> t -> t m

lshift x y mod m shifts x to left by y. Returns 0 is y >= m.

val rshift : t -> t -> t m

rshift x y mod m shifts x right by y bits. Returns 0 if y >= m

val arshift : t -> t -> t m

arshift x y mod m shifts x right by y with msb x filling.

Returns ones mod m if y >= m /\ msb x mod m and zero if y >= m /\ msb x mod m = 0

val gcd : t -> t -> t m

gcd x y mod m returns the greatest common divisor modulo m

gcd x y is the meet operation of the divisibility lattice, with 0 being the top of the lattice and 1 being the bottom, therefore gcd x 0 = gcd x 0 = x.

val lcm : t -> t -> t m

lcm x y mod returns the least common multiplier modulo m.

lcm x y is the meet operation of the divisibility lattice, with 0 being the top of the lattice and 1 being the bottom, therefore lcm x 0 = lcm 0 x = 0

val gcdext : t -> t -> (t * t * t) m

(g,a,b) = gcdext x y mod m, where

  • g = gcd x y mod m,
  • g = (a * x + b * y) mod m.

The operation is well defined if one or both operands are equal to 0, in particular:

  • (x,1,0) = gcdext(x,0),
  • (x,0,1) = gcdext(0,x).
val (!$) : string -> t

!$x is of_string x

val (!!) : int -> t m

!!x mod m is int x mod m

val (~-) : t -> t m

~-x mod m is neg x mod m

val (~~) : t -> t m

~~x mod m is lnot x mod m

val (+) : t -> t -> t m

(x + y) mod m is add x y mod m

val (-) : t -> t -> t m

(x - y) mod m is sub x y mod m

val (*) : t -> t -> t m

(x * y) mod m is mul x y mod m

val (/) : t -> t -> t m

(x / y) mod m is div x y mod m

val (/$) : t -> t -> t m

x /$ y mod m is sdiv x y mod m

val (%) : t -> t -> t m

(x % y) mod m is rem x y mod m

val (%$) : t -> t -> t m

(x %$ y) mod m is smod x y mod m

val (%^) : t -> t -> t m

(x %^ y) mod m is srem x y mod m

val (land) : t -> t -> t m

(x land y) mod m is logand x y mod m

val (lor) : t -> t -> t m

(x lor y) mod m is logor x y mod m

val (lxor) : t -> t -> t m

(x lxor y) mod m is logxor x y mod m

val (lsl) : t -> t -> t m

(x lsl y) mod m lshift x y mod m

val (lsr) : t -> t -> t m

(x lsr y) mod m is rshift x y mod m

val (asr) : t -> t -> t m

(x asr y) = arshift x y

val (++) : t -> int -> t m

(x ++ n) mod m is nsucc x n mod m

val (--) : t -> int -> t m

(x -- n) mod mis npred x n mod m