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

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 allowss 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 with remainder

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

Currently, the division and modulo operators exist as statements rather than values. However, we plan to make them pure in the future, so that you can use them in expressions just like the other arithmetic operators.

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 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.

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