Bitvector datatype, parameterized by width.

Get the underlying Integer representation from a BV. We guarantee that (\(BV.BV x) -> x) == BV.asUnsigned.

A runtime presentation of a type-level Nat.

This can be used for performing dynamic checks on a type-level natural numbers.

This generates a NatRepr from a type-level context.

Construct a bitvector with a particular width, where the width is provided as an explicit NatRepr argument. The input Integer, whether positive or negative, is silently truncated to fit into the number of bits demanded by the return type. The width cannot be arbitrarily large; it must be representable as an Int.

>>> mkBV (knownNat @4) 10
BV 10
>>> mkBV (knownNat @2) 10
BV 2
>>> mkBV (knownNat @4) (-2)
BV 14

Like mkBV, but returns Nothing if unsigned input integer cannot be represented in w bits.

Like mkBV, but returns Nothing if signed input integer cannot be represented in w bits.

unsignedClamp w i rounds i to the nearest value between 0 and 2^w - 1 (inclusive).

signedClamp w i rounds i to the nearest value between -2^(w-1) and 2^(w-1) - 1 (inclusive).

The minimum unsigned value for bitvector with given width (always 0).

The maximum unsigned value for bitvector with given width.

The minimum value for bitvector in two's complement with given width.

The maximum value for bitvector in two's complement with given width.

The zero bitvector of any width.

The bitvector with value 1, of any positive width.

The bitvector whose value is its own width, of any width.

Construct a BV from a Bool.

Construct a BV from a Word8.

Construct a BV from a Word16.

Construct a BV from a Word32.

Construct a BV from a Word64.

Construct a BV from an Int8.

Construct a BV from an Int16.

Construct a BV from an Int32.

Construct a BV from an Int64.

Construct a BV from a list of bits, in big endian order (bits with lower value index in the list are mapped to higher order bits in the output bitvector). Return the resulting BV along with its width.

>>> case bitsBE [True, False] of p -> (fstPair p, sndPair p)
(2,BV 2)

Construct a BV from a list of bits, in little endian order (bits with lower value index in the list are mapped to lower order bits in the output bitvector). Return the resulting BV along with its width.

>>> case bitsLE [True, False] of p -> (fstPair p, sndPair p)
(2,BV 1)

Construct a BV from a list of bytes, in big endian order (bytes with lower value index in the list are mapped to higher order bytes in the output bitvector).

>>> case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p)
(24,BV 257)

Construct a BV from a list of bytes, in little endian order (bytes with lower value index in the list are mapped to lower order bytes in the output bitvector).

>>> case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p)
(24,BV 65792)

Construct a BV from a big-endian bytestring.

>>> case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
(24,BV 257)

Construct a BV from a little-endian bytestring.

>>> case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
(24,BV 65792)

Signed interpretation of a bitvector as an Integer.

Unsigned interpretation of a bitvector as a positive Integer.

Unsigned interpretation of a bitvector as a Natural.

Convert a bitvector to a list of bits, in big endian order (higher order bits in the bitvector are mapped to lower indices in the output list).

>>> asBitsBE (knownNat @5) (mkBV knownNat 0b1101)
[False,True,True,False,True]

Convert a bitvector to a list of bits, in little endian order (lower order bits in the bitvector are mapped to lower indices in the output list).

>>> asBitsLE (knownNat @5) (mkBV knownNat 0b1101)
[True,False,True,True,False]

Convert a bitvector to a list of bytes, in big endian order (higher order bytes in the bitvector are mapped to lower indices in the output list). Return Nothing if the width is not a multiple of 8.

>>> asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd)
Just [170,187,204,221]

Convert a bitvector to a list of bytes, in little endian order (lower order bytes in the bitvector are mapped to lower indices in the output list). Return Nothing if the width is not a multiple of 8.

>>> asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd)
Just [221,204,187,170]

asBytesBE, but for bytestrings.

asBytesLE, but for bytestrings.

Bitwise and.

Bitwise or.

Bitwise xor.

Bitwise complement (flip every bit).

Left shift by positive Natural.

Right logical shift by positive Natural.

Right arithmetic shift by positive Natural.

Bitwise rotate left.

Bitwise rotate right.

The BV that has a particular bit set, and is 0 everywhere else.

Like bit, but without the requirement that the index bit refers to an actual bit in the output BV. If it is out of range, just silently return the zero bitvector.

setBit bv ix is the same as or bv (bit knownNat ix).

Like setBit, but without the requirement that the index bit refers to an actual bit in the input BV. If it is out of range, just silently return the original input.

clearBit w bv ix is the same as and bv (complement (bit w ix)).

Like clearBit, but without the requirement that the index bit refers to an actual bit in the input BV. If it is out of range, just silently return the original input.

complementBit bv ix is the same as xor bv (bit knownNat ix).

Like complementBit, but without the requirement that the index bit refers to an actual bit in the input BV. If it is out of range, just silently return the original input.

Test if a particular bit is set.

Like testBit, but takes a Natural for the bit index. If the index is out of bounds, return False.

Get the number of 1 bits in a BV.

Count trailing zeros in a BV.

Count leading zeros in a BV.

Truncate a bitvector to a particular width given at runtime, while keeping the type-level width constant.

Bitvector add.

Bitvector subtract.

Bitvector multiply.

Bitvector division (unsigned). Rounds to zero. Division by zero yields a runtime error.

Bitvector division (signed). Rounds to zero. Division by zero yields a runtime error.

Bitvector division (signed). Rounds to negative infinity. Division by zero yields a runtime error.

Bitvector remainder after division (unsigned), when rounded to zero. Division by zero yields a runtime error.

Bitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.

Bitvector remainder after division (signed), when rounded to negative infinity. Division by zero yields a runtime error.

uquot and urem returned as a pair.

squot and srem returned as a pair.

sdiv and smod returned as a pair.

Bitvector absolute value. Returns the 2's complement magnitude of the bitvector.

2's complement bitvector negation.

Get the sign bit as a BV.

Return 1 if positive, -1 if negative, and 0 if 0.

Signed less than.

Signed less than or equal.

Unsigned less than.

Unsigned less than or equal.

Unsigned minimum of two bitvectors.

Unsigned maximum of two bitvectors.

Signed minimum of two bitvectors.

Signed maximum of two bitvectors.

Concatenate two bitvectors. The first argument gets placed in the higher order bits.

>>> concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)
BV 6
>>> :type it
it :: BV 5

Slice out a smaller bitvector from a larger one.

>>> select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)
BV 3
>>> :type it
it :: BV 4

Like select, but takes a Natural as the index to start selecting from. Neither the index nor the output width is checked to ensure the resulting BV lies entirely within the bounds of the original bitvector. Any bits "selected" from beyond the bounds of the input bitvector will be 0.

>>> select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110)
BV 6
>>> :type it
it :: BV 4

Zero-extend a bitvector to one of strictly greater width.

>>> zext (knownNat @8) (mkBV (knownNat @4) 0b1101)
BV 13
>>> :type it
it :: BV 8

Sign-extend a bitvector to one of strictly greater width.

Truncate a bitvector to one of strictly smaller width.

Like trunc, but allows the input width to be greater than or equal to the output width, in which case it just performs a zero extension.

Wide multiply of two bitvectors.

Unsigned successor. succUnsigned w (maxUnsigned w) returns Nothing.

Signed successor. succSigned w (maxSigned w) returns Nothing.

Unsigned predecessor. predUnsigned w zero returns Nothing.

Signed predecessor. predSigned w (minSigned w) returns Nothing.

List of all unsigned bitvectors from a lower to an upper bound, inclusive.

List of all signed bitvectors from a lower to an upper bound, inclusive.

Pretty print in hex

Pretty print in binary

Pretty print in octal

Pretty print in decimal