# Module `Bitvec`

`type t`

abstract representation of a fixed size bitvector

`type 'a m`

a computation in some modulo

`type modulus`

type denoting the arithmetic modulus

`val modulus : int -> modulus`

`modulus s` is the modulus of bitvectors with size `s`.

This is a number \$2^s-1\$, also known as a Mersenne number.

`val m1 : modulus`

`m1 = modulus 1` = \$1\$ is the modulus of bitvectors with size `1`

`val m8 : modulus`

`m8 = modulus 8` = \$255\$ is the modulus of bitvectors with size `8`

`val m16 : modulus`

`m16 = modulus 16` = \$65535\$ is the modulus of bitvectors with size `16`

• since 2.5.0
`val m32 : modulus`

`m32 = modulus 32` = \$2^32-1\$ is the modulus of bitvectors with size `32`

`val m64 : modulus`

`m64 = modulus 64` = \$2^64-1\$ is the modulus of bitvectors with size `64`

`val (mod) : 'a m -> modulus -> 'a`

`(x <op> y) mod m` applies operation `<op>` modulo `m`.

Example: `(x + y) mod m` returns the sum of `x` and `y` modulo `m`.

Note: the `mod` function is declared as a primitive to enable support for inlining in non flambda versions of OCaml. Indeed, underneath the hood the `'a m` type is defined as the reader monad `modulus -> 'a`, however we don't want to create a closure every time we compute an operation over bitvectors. With this trick, all versions of OCaml no matter the optimization options will inline `(x+y) mod m` and won't create any closures, even if `m` is not known at compile time.

`module type S = sig ... end`
`val compare : t -> t -> int`

`compare x y` compares `x` and `y` as unsigned integers, i.e., `compare x y` = `compare (to_nat x) (to_nat y)`

`val equal : t -> t -> bool`

`equal x y` is true if `x` and `y` represent the same integers

`val (<) : t -> t -> bool`

`x < y` iff `compare x y = -1`

`val (>) : t -> t -> bool`

`x < y` iff `compare x y = -1`

`x > y` iff `compare x y = 1`

`val (=) : t -> t -> bool`

`x > y` iff `compare x y = 1`

`x = y` iff `compare x y = 0`

`val (<>) : t -> t -> bool`

`x = y` iff `compare x y = 0`

`x <> y` iff `compare x y <> 0`

`val (<=) : t -> t -> bool`

`x <> y` iff `compare x y <> 0`

`x <= y` iff `compare x y <= 0`

`val (>=) : t -> t -> bool`

`x <= y` iff `compare x y <= 0`

`x >= y` iff `compare x y >= 0`

`val hash : t -> int`

`hash x` returns such `z` that forall `y` s.t. `x=y`, `hash y = z`

`val pp : Stdlib.Format.formatter -> t -> unit`

`pp ppf x` is a pretty printer for the bitvectors.

Could be used standalone or as an argument to the `%a` format specificator, e.g.,

``Format.fprintf "0xBEEF != %a" Bitvec.pp !\$"0xBEAF"``
`val to_binary : t -> string`

`to_binary x` returns a canonical binary representation of `x`

`val of_binary : string -> t`

`of_binary s` returns a bitvector `x` s.t. `to_binary x = s`.

`val to_string : t -> string`

`to_string x` returns a textual (human readable) representation of the bitvector `x`.

`val of_string : string -> t`

`of_string s` returns a bitvector that corresponds to `s`.

The set of accepted strings is defined by the following EBNF grammar:

```       valid-numbers ::=
| "0b", bin-digit, {bin-digit}
| "0o", oct-digit, {oct-digit}
| "0x", hex-digit, {hex-digit}
| dec-digit, {dec-digit}

bin-digit ::= '0' | '1'
oct-digit ::= '0'-'7'
dec-digit ::= '0'-'9'
hex-digit ::= '0'-'9' |'a'-'f'|'A'-'F'```
• raises Invalid_argument

if the string `s` is not recognized as `valid-numbers`.

`val bigint_unsafe : Z.t -> t`

`bigint_unsafe x` directly interprets a zarith value as bitvector.

The function is safe only if `x` is the result of `to_bigint`, otherwise the resulting value is unpredictable.

• since 2.5.0
`val of_substring : ?pos:int -> ?len:int -> string -> t`

`of_substring ~pos ~len s` is a bitvector that corresponds to a substring of `s` designated by the start position `pos` and length `len`.

The result is the same as `of_string (String.sub s pos len)`, except that no intermediate substring is created.

• parameter pos

is the starting position of the substring (defaults to `0`)

• parameter len

is the length of the substring (defaults to the length of `s`.

• raises Invalid_argument

if `pos` and `len` together do not define a valid substring of `s` or if the substring is not a sequence of numbers of the base `b`.

`val of_string_base : int -> string -> t`

`of_string_base b x` is a bitvector that corresponds to `s` represented in base `b`.

The base `b` must be between `2` and `16`. The textual representation shall not contain a prefix that designates the base and must be a sequence of digits that are less than `b`.

Examples

Valid inputs:

• `of_string_base 16 "DEADBEEF"`;
• `of_string_base 2 "010110"`;
• `of_string_base 11 "AAAAAA"`.

Invalid inputs:

• `of_string_base 16 "0xDEADBEEF"`;
• `of_string_base 2 "-010100"`;
• `of_string_base 10 "AAAAA"`.
`val of_substring_base : ?pos:int -> ?len:int -> int -> string -> t`

`of_substring_base b x` is a bitvector that corresponds to a substring of `s` designated by the start position `pos` and length `len` that is a sequence of digits in base `b`.

The result is the same as ```of_string_base b x (String.sub s pos len)```, except that no intermediate substring is created.

• parameter pos

is the starting position of the substring (default to `0`)

• parameter len

is the length of the substring (defaults to the length of `s`.

• raises Invalid_argument

if `pos` and `len` together do not define a valid substring of `s` or if the substring is not a sequence of numbers of the base `b`.

`val fits_int : t -> bool`

`fits_int x` is `true` if `x` could be represented with the OCaml `int` type.

Note: it is not always true that `fits_int (int x mod m)`, since depending on `m` a negative number might not fit into the OCaml representation. For positive numbers it is true, however.

`val to_int : t -> int`

`to_int x` returns an OCaml integer that has the same representation as `x`.

The function is undefined if `not (fits_int x)`.

`val fits_int32 : t -> bool`

`fits_int32 x` is `true` if `x` could be represented with the OCaml `int` type.

Note: it is not always true that `fits_int32 (int32 x mod m)`, since depending on `m` the negative `x` may not fit back into the `int32` representation. For positive numbers it is true, however.

`val to_int32 : t -> int32`

`to_int32 x` returns an OCaml integer that has the same representation as `x`.

The function is undefined if `not (fits_int32 x)`.

`val fits_int64 : t -> bool`

`fits_int64 x` is `true` if `x` could be represented with the OCaml `int` type.

Note: it is not always true that `fits_int64 (int64 x mod m)`, since depending on `m` the negative `x` might not fit back into the `int64` representation. For positive numbers it is true, however.

`val to_int64 : t -> int64`

`to_int64 x` returns an OCaml integer that has the same representation as `x`.

The function is undefined if `not (fits_int64 x)`.

`val to_bigint : t -> Z.t`

`to_bigint x` returns a natural number that corresponds to `x`.

The returned value is always positive.

`val extract : hi:int -> lo:int -> t -> t`

`extract ~hi ~lo x` extracts bits from `lo` to `hi`.

The operation is effectively equivalent to `(x lsr lo) mod (hi-lo+1)`

`val select : int list -> t -> t`

`select bits x` builds a bitvector from `bits` of `x`.

Returns a bitvector `y` such that `nth` bit of it is equal to `List.nth bits n` bit of `x`.

Returns `zero` if `bits` are empty.

`val append : int -> int -> t -> t -> t`

`append m n x y` takes `m` bits of `x` and `n` bits of `y` and returns their concatenation. The result has `m+n` bits.

Examples:

• `append 16 16 !\$"0xdead" !\$"0xbeef" = !\$"0xdeadbeef"`;
• `append 12 20 !\$"0xbadadd" !\$"0xbadbeef" = !\$"0xadddbeef"`;;
`val repeat : int -> times:int -> t -> t`

`repeat m ~times:n x` repeats `m` bits of `x` `n` times.

The result has `m*n` bits.

`val concat : int -> t list -> t`

`concat m xs` concatenates `m` bits of each `x` in `xs`.

The operation is the reduction of the `append` operation with `m=n`. The result has `m * List.length xs` bits and is equal to `0` if `xs` is empty.

`include S with type 'a m := 'a m`
`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 `n`th 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 `n`th 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 `n`th 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 m`is `npred x n mod m`

`module type Modulus = sig ... end`
`module Make (M : Modulus) : sig ... end`

`module Mx = Make(Modulus)` produces a module `Mx` which implements all operation in `S` modulo `Modulus.modulus`, so that all operations return a bitvector directly.

`module type D = S with type 'a m = 'a`
`module M1 : D`

`M1` specializes `Make(struct let modulus = m1 end)`

`module M8 : D`

`M8` specializes `Make(struct let modulus = m8 end)`

`module M16 : D`

`M16` specializes `Make(struct let modulus = m16 end)`

`module M32 : D`

`M32` specializes `Make(struct let modulus = m32 end)`

`module M64 : D`

`M64` specializes `Make(struct let modulus = m64 end)`

`val modular : int -> (module D)`

`modular n` returns a module `M`, which implements all operations in `S` modulo the bitwidth `n`.

• since 2.5.0