v0.23.0

What’s New?

Introducing 4 new arithmetic operators for UInt!

add :: UInt w -> UInt w -> UInt (w + 1)
addV :: [UInt w] -> UInt v
mul :: UInt w -> UInt w -> UInt (w * 2)
mulV :: UInt w -> UInt w -> UInt v

There are two operators for addition and two for multiplication.

You can probably guess the functions of these operators from their type signatures.

Limitation of the existing operators

The existing addition and multiplication operators have type signatures as follows:

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

These operators produce unsigned integers with fixed widths that must match those of their operands. This can lead to overflow if the values of the operands are too large, with no means to salvage the overflowed bits. That's why we're introducing new operators that allow you to choose the result widths for addressing these limitations.

Let’s take a closer look.

Full Sum Addition

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

As the name suggests, this function produces a slightly longer unsigned integer with the carry bit preserved.

Example usage:

example :: Comp (UInt 9)
example = do
    x <- input Public
    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

Similar to add, but for multiplication. It produces an unsigned integer double the width of its operands, allowing the full product of multiplication to be preserved.

Example usage:

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

Variable-width Multiplication

This is the most general form of multiplication, 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 12)
example = do
    x <- input Public :: Comp (UInt 8)
    y <- input Public
    return (x `mulV` y) -- 4 higher bits discarded

What Else?

As always, bug fixes and performance improvements!

Noticeably, unsigned integer division/modulo should produce less number of constraints that before.

What’s Next?

• User-defined datatypes with (automatically) structured input/output: Instead of using lists for representing input/output, we want something more structured, like JSON values!
• Smarter witness generation + user-programmable hints for witness generation.