Skip to content

Bitwise Constraints

A simple example of a constraint system

An introductory example is programming a constraint system for a simple function. The prover is to commit to the inputs and the outputs of the function, and we must impose the appropriate constraints. We must also act as the prover and generate the correct witness.

We will use the gadget pattern, which means we will write a function that receives oracles holding the inputs to the function, and we are to create and return an output oracle ensuring proper constraints are place.

Let the function be the bitwise AND of two input oracles. The pattern presented is easily generalized to other bitwise operations. We write the function and below to accept the input oracles and create an output oracle constrained to holding the correct output values. We begin by writing the signature of the function as

fn and<U, F>(
	builder: &mut ConstraintSystemBuilder<U, F>,
	name: impl ToString,
	xin: OracleId,
	yin: OracleId,
) -> Result<OracleId, anyhow::Error>
where
	U: UnderlierType + Pod + PackScalar<F> + PackScalar<BinaryField1b>,
	F: TowerField

where xin and yin are our input oracles, and name will be given to the output oracle.

Within our and function, we first check that the inputs have the same size, and we must learn that size to create the output oracle. We can write

let log_rows = builder.log_rows([xin, yin]);

to ensure that the two input oracles have the same log size, and obtain that log size. Then to create the output oracle we write

let zout = builder.add_committed(name, log_rows, BinaryField1b::TOWER_LEVEL);

which creates a committed column with 1 << log_rows rows over the field BinaryField1b.

At this point we have created the output oracle. Two tasks remain:

  • Populating the output oracle: If the prover is the one building, we must materialize this oracle with correct output values and update the witness.
  • Constraining the output oracle: We must constrain the output oracle to hold the correct values.

Populating the Output Oracle

In order to detect whether building for the prover or verifier, and obtain the witness if building for the prover, we call builder.witness().

if let Some(witness) = builder.witness() {
    // work with witness
}

Once having the witness we query for access to the input oracles. Calling witness.get::<BinaryField1b>(xin)? we get a WitnessEntry, and now we must use this witness entry to conveniently access the input values. In memory there is a contiguous sequence of BinaryField1b field elements, i.e. a sequence of bits, and we wish to access these bits to compute an AND. Most conveniently, we can cast this contiguous slice of bits to a slice of u32 values, and then compute an AND with each of those values. We make this cast by calling as_slice::<u32>() on the witness entry. Thus we write

let xin_u32 = witness.get::<BinaryField1b>(xin)?.as_slice::<u32>();
let yin_u32 = witness.get::<BinaryField1b>(yin)?.as_slice::<u32>();

In order to create the output column, we call witness.new_column::<BinaryField1b>(zout) which creates an EntryBuilder for our previously created oracle zout. Once we are done populating the new column, this EntryBuilder will turn into an entry in our witness such that we can access a WitnessEntry for zout the way we did for the input oracles.

let zout_col = witness.new_column::<BinaryField1b>(zout);

To populate this new column using mutable u32 values, we will call as_mut_slice::<u32>() on the entry builder. Now we iterate (or parallel iterate for speed) through the inputs and outputs all casted as u32 slices, we read the inputs, compute their AND, and write results to the output.

(xin_u32, yin_u32, zout_col.as_mut_slice::<u32>())
    .into_par_iter()
    .for_each(|(xin: &u32, yin: &u32, zout: &mut u32)| {
        *zout = (*xin) & (*yin);
    });

Constraining the Output Oracle

From the verifier's perspective, we have so far only declared zout to be the committed output oracle. Nothing constrains zout to contain the correct output values. In order to constraint zout, we can ask that the three values occupying every row of these three oracles satisfies an equation. The equation is xin * yin - zout = 0, where the variables represent BinaryField1b elements and multiplication takes place in the field BinaryField1b. We enforce an equation by enforcing that an arithmetic expression have the value zero. Using the macro binius_macros::arith_expr we can create an arithmetic expression as

let expr = arith_expr!([x, y, z] = x * y - z);

While this expression is over BinaryField1b, we'll need it over F, so we'll call a conversion method convert_field on it before we use it.

To assert this expression has the value zero everywhere, we call builder.assert_zero. The first argument to this assertion specifies the oracles upon which the arithmetic expression must evaluate to zero. The second argument is the arithmetic expression itself. In our case we write

builder.assert_zero([xin, yin, zout], expr.convert_field());

Finally, having let the prover fill zout with values and let the verifier constrain zout to be correct, we may return the oracle to the caller as Ok(zout).

The Full Example

For completeness we write the full gadget below.

fn and<U, F>(
	builder: &mut ConstraintSystemBuilder<U, F>,
	name: impl ToString,
	xin: OracleId,
	yin: OracleId,
) -> Result<OracleId, anyhow::Error>
where
	U: UnderlierType + Pod + PackScalar<F> + PackScalar<BinaryField1b>,
	F: TowerField,
{
	let log_rows = builder.log_rows([xin, yin])?;
	let zout = builder.add_committed(name, log_rows, BinaryField1b::TOWER_LEVEL);
	if let Some(witness) = builder.witness() {
        let xin_u32 = witness.get::<BinaryField1b>(xin)?.as_slice::<u32>();
        let yin_u32 = witness.get::<BinaryField1b>(yin)?.as_slice::<u32>();
		let mut zout_col = witness.new_column::<BinaryField1b>(zout);
		(xin_u32, yin_u32, zout_col.as_mut_slice::<u32>())
			.into_par_iter()
			.for_each(|(xin, yin, zout)| {
				*zout = (*xin) & (*yin);
			});
	}
 
	let expr = arith_expr!([x, y, z] = x * y - z);
 
	builder.assert_zero([xin, yin, zout], expr.convert_field());
 
	Ok(zout)
}

To see this example and other bitwise examples for XOR and OR, visit Binius examples.