Unsigned Integers

Unsigned integers are very much like field elements, except that they have fixed bit widths.

You can think of an unsigned integer of bit width w like an array of w Booleans. We can use these bits to represent numbers ranging from 0 to 2^w.

someByte :: UInt 8
someByte = 7

someWord :: UInt 32
someWord = 234

Type

An unsigned integer of bit width w would have type UInt w. This w is a type-level natural number.

To annotate type-level natural numbers with literals in your code, you'll need to enable the extension DataKinds like this at the top of your file:

{-# LANGUAGE DataKinds #-}

module YourModule where

Construction

This section describes ways to construct unsigned integers.

Note that the bits are arranged in little-endian fashion, meaning that the least significant bit has index 0.

Using constructors

Unsigned integers are constructed with the following constructor under the hood:

UInt :: Integer -> UInt w

Using literals

Unsigned integers implement the Num typeclass, making it possible to construct an instance using literals.

42 :: Uint 32

From inputs

Another way of acquiring an unsigned integer is from inputs:

{-# LANGUAGE TypeApplications #-}

example :: Comp (UInt 32)
example = inputUInt Public @32

@32 in the above example is a type application on inputUInt, which has type:

inputUInt :: Comp (UInt w)

Conversion

From Haskell Integer

A numeric literal represents the application of the function fromInteger to the appropriate value of type Integer.

fromInteger :: Integer -> Field

To Keelung Field

toField :: UInt w -> Comp Field

The toField statement converts an unsigned integer to a Field.

Bits outside the width of the underlying field will be discarded. For example, If the width of the underlying field is w, the the resulting value of the Field with be the value of the unsigned integer modulo 2^w.

Example usage:

example :: Comp Field
example = do
    x <- input Public :: Comp (UInt 8)
    toField x

From Keelung Field

fromField :: Width -> Field -> Comp (UInt w)

The fromField statement converts a Field to an unsigned integer. The value of the first argument needs to the same as the width of the resulting unsigned integer. Bits outside the width of the unsigned integer will be discarded.

Example usage:

example :: Comp (UInt 8)
example = do
    x <- input Public
    fromField 8 x

From Keelung Boolean

fromBools :: [Boolean] -> Comp (UInt w)

The fromBools statement converts a list of Boolean values to a unsigned integer, ordered from the least significant bit to the most significant bit.

When the length of the list is less than the width of the unsigned integer, the remaining bits are filled with false. When the length of the list is greater than the width of the unsigned integer, the extra bits are discarded.

Example usage:

example :: Comp (UInt 8)
example = do
    b <- inputBool
    fromBools [true, b, b .&. false, true, false]

To Keelung Boolean

See bit test.

Arithmetics

Since UInt w is an instance of Num, all methods of Num works on unsigned integers.

Addition

(+) :: UInt w -> UInt w -> UInt w

Example usage: 3 + 4

Subtraction

(-) :: UInt w -> UInt w -> UInt w

Example usage: 3 - 4

Multiplication

(*) :: UInt w -> UInt w -> UInt w

Example usage: 3 * 4

Full Sum Addition

add :: UInt w -> UInt w -> UInt (w + 1)

This function takes two UInt w and produces a slightly longer UInt (w + 1) that comes with the carry bit resulted from the addition.

Example usage:

example :: Comp (UInt 9)
example = do
    x <- input Public :: Comp (UInt 8)
    y <- input Public
    return (x `add` y)

Variable-width Batch Addition

addV :: [UInt w] -> UInt v

This is the most general form of addition, allowing you to sum a batch of unsigned integers and decide how many carry bits you want to preserve or discard. The result will be zero-extended if it is longer than expected, and truncated if it is shorter than actually produced.

Example usage:

example :: Comp (UInt 10)
example = do
    x <- input Public :: Comp (UInt 8)
    y <- input Public
    z <- input Public
    return [x, y, z]

Full Product Multiplication

mul :: UInt w -> UInt w -> UInt (w * 2)

This function takes two UInt w operands and produces a UInt (w * 2) of double length, preserving all carry bits from the multiplication.

Example usage:

example :: Comp (UInt 16)
example = do
    x <- input Public :: Comp (UInt 8)
    y <- input Public
    return (x `mul` y)

Variable-width Multiplication

mulV :: UInt w -> UInt w -> UInt v

Like addV, this is the most general form of multplication, allowing you to multiply two unsigned integers and decide how many carry bits you want to preserve or discard. The result will be zero-extended if it is longer than expected, and truncated if it is shorter than actually produced.

Example usage:

example :: Comp (UInt 32)
example = do
    x <- input Public :: Comp (UInt 8)
    y <- input Public
    return (x `mulV` y)

Carry-less Multiplication (Prime fields only)

(.*.) :: UInt w -> UInt w -> UInt w

Carry-less multiplication (also known as XOR multiplication) is similar to schoolbook long multiplication except that all carry numbers are discarded along the way.

This operator allows us to simulate multiplication of binary fields on prime fields. It's useful for implementing cryptographic primitives like the AES cipher.

Example usage: 3 .*. 4

Division

divU :: UInt w -> UInt w -> UInt w

divU x y takes two unsigned integers, with x as the dividend and y as the divisor, and returns the quotient of x and y.

Example usage: 3 `divU` 4

If you need to compute both quotient and remainder with divU and modU, as long as the arguments to both divU and modU are the same, there will be no extra overhead because they will share the same set of constraints after compilation.

Modulo

modU :: UInt w -> UInt w -> UInt w

modU x y takes two unsigned integers, with x as the dividend and y as the divisor, and returns the modulo of x and y.

Example usage: 3 `modU` 4

If you need to compute both quotient and remainder with divU and modU, as long as the arguments to both divU and modU are the same, there will be no extra overhead because they will share the same set of constraints after compilation.

Division with remainder statement

performDivMod :: UInt w -> UInt w -> Comp (UInt w, UInt w)

performDivMod x y takes two unsigned integers, with x as the dividend and y as the divisor, and returns a pair of unsigned integers, with the first one being the quotient and the second being the remainder.

Note that because performDivMod is a statement, it can only be executed in the Comp context , as shown in the example below:

{-# LANGUAGE DataKinds #-}

program :: Comp (UInt 32)
program = do
    dividend <- input Public
    divisor <- input Public
    (quotient, remainder) <- performDivMod dividend divisor
    return quotient

Division with remainder assertion

assertDivMod :: UInt w -> UInt w -> UInt w -> UInt w -> Comp ()

Instead of computing the quotient and remainder from the dividend and divisor, we can actually treat any of them as either input or output because division with remainder is more of a relation than a computation in Keelung.

For instance, we can both enforce the dividend to be an even number and obtain the quotient at the same time, as shown below:

{-# LANGUAGE DataKinds #-}

assertEven :: UInt 32 -> Comp (UInt 32)
assertEven dividend = do
    quotient <- freshVar
    assertDivMod dividend 2 quotient 0
    return quotient

Carry-less division with remainder (Prime fields only)

Here are the carry-less counterparts of performDivMod and assertCLDivMod:

performCLDivMod :: UInt w -> UInt w -> Comp (UInt w, UInt w)
assertCLDivMod :: UInt w -> UInt w -> UInt w -> UInt w -> Comp ()

Modular multiplicative inverse

modInv :: UInt w -> Integer -> UInt w

This operator computes the modular multiplicative inverse of a UInt with regard to some prime constant Integer. Example usage: modInv 123 2833

Logical/bitwise operation

Conjunction

(.&.) :: UInt w -> UInt w -> UInt w

Example usage: x .&. 3

Disjunction

(.|.) :: UInt w -> UInt w -> UInt w

Example usage: 42 .|. x

Exclusive disjunction

(.^.) :: UInt w -> UInt w -> UInt w

Example usage: y .^. x

Complement

complement :: UInt w -> UInt w

Example usage: complement x

Left rotate (circular shift)

rotate :: a -> Int -> a

rotate x i Rotates the bits of an unsigned integer x to the left by i bits is i is positive, or to the right by -i bits otherwise. During the rotation, the bit value at index n will be shifted to index n + i mod w, where w is the bit width of the unsigned integer.

Left shift

shift :: a -> Int -> a
shiftL :: a -> Int -> a
(.<<.) :: a -> Int -> a

These three functions are synonyms of each other. They behave like rotate, except that the vacated bits on the right are filled with zeroes (false).

Right shift

shiftR :: a -> Int -> a
(.>>.) :: a -> Int -> a

These functions work like left shift, but in the opposite direction.

Bit test

(!!!) :: UInt w -> Int -> Boolean

Bit test is a function that allows you to inspect the bit values in an unsigned integer.

Bits are packed in little-endian order, with the least significant bit having the smallest index and the most significant bit having the largest index.

If the index specified is larger than the bit width w of an unsigned integer or is smaller than zero, the index will be "wrapped" by performing a modulo operation. This allows you to access bits outside the normal range of indices and can be useful in certain situations.

Bit update

setBit :: UInt w -> Int -> Boolean -> UInt w

setBit takes an unsigned integer UInt w and returns a new UInt w with the bit at the specified index set to the provided Boolean value.

If the index specified in the setBit function is out of range, it will wrap around to a valid index by taking the remainder of the index divided by the bit width w.

Slice

slice :: UInt w -> (Int, Int) -> UInt v

slice takes an unsigned integer UInt w, along with a range, and returns a slice UInt v of that integer. The range is inclusive at the start and exclusive at the end. For instance, if x :: UInt 8, then slice x (2, 4) would return a UInt 2 representing the 3rd and 4th bits of x.

The type of the resulting integer has to be declared explicitly. Here's an example program:

program :: Comp (UInt 2)
program = do
  x <- input Public :: Comp (UInt 8)
  return $ slice x (2, 4)

Runtime exceptions are thrown under the following conditions:

• The starting index is negative.

• The ending index is less than the starting index.

• The ending index exceeds the width of the UInt.

• The expected width (as specified in the type) does not match the actual width derived from the range.

Join

join :: UInt u -> UInt v -> UInt (u + v)

The join function concatenates two unsigned integers, UInt u and UInt v, producing a new unsigned integer UInt (u + v). This function effectively combines the bit representations of the two input unsigned integers into a single unsigned integer whose width is the sum of the widths of the two inputs.

For example:

program :: Comp (UInt 8)
program = do
  u <- input Public :: Comp (UInt 2)
  v <- input Public :: Comp (UInt 6)
  return $ u `join` v

u `join` v is the same as join u v. Placing binary functions like join in between backticks allows you to treat them like binary operators.

Equality

Returns true when two unsigned integers are the same:

eq :: UInt w -> UInt w -> Boolean

Example usage: 3 `eq` 4 or eq 1 2.

Binary function such as eq can be treated like an infix operator by surrounding it with a pair of backticks`eq`

Inequality

Returns false when two Booleans are the same:

neq :: UInt w -> UInt w -> Boolean

neq is implemented as such under the hood:

neq x y = Not (x `eq` y)

Comparison

This series of predicates allows you to make comparisons between two unsigned integers and determine which one is larger or smaller.

lte :: UInt w -> UInt w -> Boolean
lt  :: UInt w -> UInt w -> Boolean
gte :: UInt w -> UInt w -> Boolean
gt  :: UInt w -> UInt w -> Boolean

For example, we can define a function that takes an unsigned integer as public input and see if it's greater than 42:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}

greaterThan42 :: Comp (UInt 32)
greaterThan42 = do
    x <- inputUInt @32 Public
    return $ x `gt` 42

Rather than computing the result of the comparison, we can also turn it into an assertion by passing the result to the assert statement. Assertions are typically less costly than computations in terms of the number of constraints generated.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}

greaterThan42 :: Comp ()
greaterThan42 = do
    x <- inputUInt @32 Public
    assert $ x `gt` 42