Base library contains basic useful templates and functions. The library is split into several collections described in the sections below.
WARNING: All templates in this library are guaranteed to return correct result only when inputs are correct. For bit inputs, “correct” means that input value is either zero or one. For binary number inputs, “correct” means that all digits are bits. In case all inputs are correct, but correct output does not exist, templates are guaranteed to fail, i.e. produce set of constraints that could not be satisfied.
Assert collection contains assertion functions.
function assert (condition)
Fail processing in case given condition is zero.
Binary collection contains templates that deal with binary numbers with arbitrary bit width.
template BinaryAdd (n, m)
signal input x [m][n]
signal output result [n]
Calculate sum of m n-bit wide binary numbers x[0]...x[n-1].
Return lowest n bits of the sum as result[0]...result[n-1].
template BinaryAddConstant (n, c)
signal input x [n]
signal output result [n]
Add constant c to an n-bit wide binary number x[0]...x[n-1].
Return lowest n bits of the sum as result[0]...result[n-1].
template BinaryCompare (n, l, e, g)
signal input x [n]
signal input y [n]
signal output result
Compare two n-bit wide binary numbers: x[0]...x[n-1] and y[0]...y[n-1].
Return as result l, e, or g if the first binary number is less than, equal to, or greater than the second binary number respectively.
template BinaryCompareConstant (n, threshold, l, e, g)
signal input x [n]
signal output result
Compare n-bit wide binary number: x[0]...x[n-1] with constant c.
Return as result l, e, or g if the binary number is less than, equal to, or greater than the constant respectively.
template BinaryMultiplexor (n)
signal input index [n]
signal input values [2 ** n]
signal output result
Pick element of values array whose index is denoted by n-bit wide binary number index[0]...index[n-1] and return it as result.
template BinaryNegate (n)
signal input x [n]
signal output result [n]
Calculate binary-complement negation of n-bit wide binary number x[0]...x[n-1] and return is as result[0]...result[n-1].
template BinaryResizeSigned (n, m)
signal input x [n]
signal output result [m]
Resize n-bit wide signed binary number x[0]...x[n-1] to m bits, and return it as result[0]...result[m-1].
Fail in case resize would lead to loss of information.
template BinaryResizeUnsigned (n, m)
signal input x [n]
signal output result [m]
Resize n-bit wide unsigned binary number x[0]...x[n-1] to m bits, and return it as result[0]...result[m-1].
Fail in case resize would lead to loss of information.
template BinarySubtract (n)
signal input x [n]
signal input y [n]
signal output result [n]
Subtract n-bit wide binary number y[0]...y[n-1] from n-bit wide binary number x[0]...x[n-1].
Return lowest n bits of subtraction result as result[0]...result[n-1].
template BinarySubtractConstant (n, c)
signal input x [n]
signal output result [n]
Subtract constant c from n-bit wide binary number x[0]...x[n-1].
Return lowest n bits of subtraction result as result[0]...result[n-1].
template BinarySubtractFromConstant (n, c)
signal input x [n]
signal output result [n]
Subtract n-bit wide binary number x[0]...x[n-1] from constant c.
Return lowest n bits of subtraction result as result[0]...result[n-1].
template FromBinary (n)
signal input x [n]
signal output result
Convert n-bit wide binary number x[0]...x[n-1] into a signal as return it as result.
Fail in case given binary number cannot be converted to a signal without loss of information.
template ToBinary (n)
signal input x
signal output result [n]
Convert signal x into n-bit wide binary number and return it as result[0]...result[n-1].
Fail in case given signal cannot be converted to n-bit wide binary number without loss of information.
Bit Collection contains template for manipulations with bits.
template BitAnd ()
signal input x
signal input y
signal output result
Calculate logical “and” of bits x and y.
Return calculation result as result.
template BitImplies ()
signal input x
signal input y
signal output result
Calculate logical implication of two bits: x implies y.
Return calculation result as result.
template BitNand ()
signal input x
signal input y
signal output result
Calculate inverted logical “and” of bits x and y.
Return calculation result as result.
template BitNimplies ()
signal input x
signal input y
signal output result
Calculate inverted logical implication of two bits: x does not imply y.
Return calculation result as result.
template BitNor ()
signal input x
signal input y
signal output result
Calculate inverted logical “or” of bits x and y.
Return calculation result as result.
template BitOr ()
signal input x
signal input y
signal output result
Calculate logical “or” of bits x and y .
Return calculation result as result.
template BitXnor ()
signal input x
signal input y
signal output result
Calculate inverted logical exclusive “or” of bits x and y.
Return calculation result as result.
template BitXor ()
signal input x
signal input y
signal output result
Calculate logical exclusive “or” of bits x and y.
Return calculation result as result.
template CheckBit ()
signal input x
Ensure that signal x is a bit.
Fail in case it is not.
template InvertBit ()
signal input x
signal output result
Calculate logical inversion of a bit: not x.
Return calculation result as result.
template IsBit ()
signal input x
signal output result
Tell whether signal x is a bit.
Return as result one if x is a bit and one zero otherwise.
Compare Collection contains templates for comparing signals.
template CheckEqual ()
signal input x
signal input y
Ensure that signals x and y are equal.
Fail if they are not.
template CheckNonZero ()
signal input x
Ensure that signal x is non zero.
Fail if it is.
template CheckNotEqual ()
signal input x
signal input y
Ensure that signals x and y are not equal.
Fail if they are.
template CheckZero ()
signal input x
Ensure that signal x is zero.
Fail if it is not.
template IsEqual ()
signal input x
signal input y
signal output result
Tell whether signals x and y are equal.
Return as result one if they are and zero if they are not.
template IsNonZero ()
signal input x
signal output result
Tell whether signal x is non zero.
Return as result one if it isand zero if it is not.
template IsNotEqual ()
signal input x
signal input y
signal output result
Tell whether signals x and y are not equal.
Return as result one if they are not equal and zero if they are equal.
template IsZero ()
signal input x
signal output result
Tell whether signal x is zero.
Return as result one if it is and zero if it is not.
Constants collection contains functions that return various useful constants.
function maxSignal ()
Return maximum signal value.
function maxSignalWidth ()
Return width in bits of maximum signal value.
Field collection contains templates for performing calculations with field elements.
template FieldDivide ()
signal input x
signal input y
signal output result
Divide field element x by field element y.
Return division result as result.
template FieldDivideByConstant (c)
signal input x
signal output result
Divide field element x by constant c.
Return division result as result.
template FieldDivideConstant (c)
signal input x
signal output result
Divide constant c by field element x.
Return division result as result.
template FieldSqrt ()
signal input x
signal output result
Calculate and return as result square root of field element x.
This template always returns lowest of two possible square root values, but generated constraints treat both root values as valid.
Utils collection contains various useful functions.
function max (x, y)
Calculate maximum of two signal values: x and y.
function min (x, y) {
Calculate minimum of two signal values: x and y.
function signalWidth (x)
Calculate width in bits of signal value x.