Skip to content

Constraining Columns

Ensuring the validity of the witness

There are several types of constraints that can be applied to columns. When we create virtual columns, we are imposing a constraint on what values they must contain in terms of other columns. We can also constrain relationships between columns by enforcing the rows of the columns satisfy an equation. Checking column values to be nonzero, and flushing column values into a channel, are two more ways to impose constraints on columns.

Having discussed virtual oracles previously, we focus this page on the other three types of constraints. To clarify, those three constraint types are:

  • Asserting a constraint on every row of a list of columns.
  • Asserting every value in a column is nonzero.
  • Flushing rows of a list of columns into a channel.

Columns may participate in more than one constraint and more than one kind of constraint. It could be possible, for example, to check a column vanishes on some expression, has all nonzero values, and also flush those values into a channel.

Asserting Zero

Suppose we have a set of k columns of equal height. We can imagine they are the columns of a table, and we'd like to impose a constraint on every row of this table. We can express that constraint with an arithmetic expression of k variables that should vanish on every row. Given a list of k oracles and a k-variate arithmetic expression, we can impose our constraint by calling assert_zero on the builder. Such a constraint is called a "zerocheck" constraint.

Let us show how to construct an arithmetic expression. Arithmetic expressions in Binius are symbolic expression trees, providing a convenient and flexible way to represent arithmetic expressions. With expressions structured as a tree, each node represents an operation or an operand.

  • Const(F): a constant.
  • Var(usize): a variable where the usize indicates the index of the variable among all variables in the expression.
  • Add, Mul: binary operations for addition and multiplication.
  • Pow: exponentiation with a base and an integer exponent.
  • ArithExpr::one() and ArithExpr::zero(): values one and zero.

Expressions can be constructed, combined, and manipulated symbolically without immediate evaluation. Overloading operators +, -, and * help make manipulation more intuitive.

For the simplest example, suppose we have an oracle bit that we wish to test has all values either zero or one. Of course this check is only non-trivial if bits is over a field other than BinaryField1b. Our arithmetic expression is

let var_0 = ArithExpr::Var(0);
let expression: ArithExpr<BinaryField1b> =
    (var_0.clone() - ArithExpr::zero()) * (var_0 - ArithExpr::one());

Then we make the assertion

builder.assert_zero([bits], expression.convert_field());

where the convert_field call is necessary to transform the expression from one over BinaryField1b into one over F.

For a case where we take advantage of symbolic manipulation rather than hardcoding the expression, let's check exponentiation. Imagine we have

  • a constant BASE in BinaryField8b
  • a list of three bit-valued oracles bit_0, bit_1, bit_2. Every row of these oracles we associate with an exponent in the range [0,7].
  • an oracle exp over BinaryField8b claimed hold the exponentiations of BASE raised to each exponent.

Our list of oracles for assert_zero is

let oracles = vec![bit_0, bit_1, bit_2, exp];

To construct the arithmetic expression we first generate powers of BASE, each of which will be conditionally selected by one of the bits.

let powers = std::iter::successors(Some(BASE), |prev| {
    Some(prev.clone() * prev.clone())
});

Now we will multiply together three terms. Each term i will correspond to one bit represented by variable ArithExpr::Var(i). If the bit is zero, the term should equal one, while if the bit is one, the term should equal BASE^{2^i}. To compute the product of these three terms, we take the first three powers values and use a fold operation, multiplying the accumulator with each term.

let correct_exp = powers.take(3).enumerate().fold(
    ArithExpr::one(),
    |acc, (i, power)| {
        acc * (ArithExpr::Var(i) * power + (ArithExpr::one() - ArithExpr::Var(i)))
    }
);

Our constraint may then be written as

builder.assert_zero(oracles, correct_exp.convert_field());

For convenience when working with arithmetic expressions, there is a macro arith_expr found in Binius macros that can reduce verbosity. For example, our expression constraining bits to take values zero or one could be written as

let expression = arith_expr!([bit] = (bit - 0) * (bit - 1));

Asserting Nonzero

The second type of constraint allows checking that a given column contains only nonzero values. For an oracle oracle, we simply call

builder.assert_nonzero(oracle);

This can be helpful for checking non-equality constraints. If two oracles must have non-equal values, we could create a virtual oracle with their difference and assert it to be everywhere nonzero.

Often we may populate a column with values only partially, wishing to disregard the padded values that serve to round up the column size to a power of two. Since columns are initialized by default with all zero values, this presents trouble if we wish to enforce that all non-padded values are nonzero. In order for assert_nonzero to pass, we must ensure the padding values are nonzero. While we could manually fill in padding values with something nonzero, the simpler solution is to create the column with all values initialized to some nonzero value. To do so, rather than calling new_column on the witness, we can call new_column_with_default, passing some (nonzero) default initializing value as a second argument after the oracle id. For example, we can always pad with value 1 like

witness.new_column_with_default::<BinaryField8b>(oracle, BinaryField8b::one())

Flushing

The third type of constraint we may apply to columns is flushing. See here for context on the role of flushing within arithmetization.

Before we can flush anything, we need a channel into which (or out of which) we can flush. A channel is created as

let channel = builder.add_channel();

where channel is simply a usize identifier for the channel. To flush into our channel we need three additional arguments (besides the channel):

  • The list of columns to flush. All columns must be of the same height. What will get flushed into the channel is each row of the table had by these columns. It is expected that all calls for flushing into a given channel have the same number of columns.
  • The flushing direction. We can FlushDirection::Push the rows into the channel, or FlushDirection::Pull the rows out of the channel.
  • The number of rows we wish to flush. There is a count parameter to a flush that limits how many rows (from the start or bottom of the columns) get flushed, ignoring all rows above count. This is for convenience to avoid the complications of flushing padding values.

Given these arguments we can flush (with pushing) like

builder.flush(FlushDirection::Push, channel, count, [oracle_0, oracle_1, oracle_2]);

For convenience there are methods send and receive that serve as syntactic sugar for calling flush with pushing and pulling, respectively. The flush call above can then be written as

builder.send(channel, count, [oracle_0, oracle_1, oracle_2]);