Skip to content

Creating Components

The critical sub-gadget

To make our lookup gadget we need a get_components gadget. The main inputs are the table column and the multiplicities which should be None only for the verifier. Most of the work we'll do in this gadget is prover work, in which case multiplicities will have a vector of length table_count, holding a multiplicity for each of the first table_count values in table. The ith component oracle returned will hold values that are the product of the table values and the bits had by taking the ith bit across the multiplicities.

The get_components gadget has the shape

fn get_components<U, F, FS, const LOG_MAX_MULTIPLICITY: usize>(
	builder: &mut ConstraintSystemBuilder<U, F>,
	table: OracleId,
	table_count: usize,
	multiplicities: Option<Vec<usize>>,
) -> Result<[OracleId; LOG_MAX_MULTIPLICITY], anyhow::Error>
where
	U: PackScalar<F> + PackScalar<FS> + PackScalar<BinaryField1b> + Pod,
	F: TowerField + ExtensionField<FS>,
	FS: TowerField + Pod,

Inside we measure the size of the table oracle, and then declare bits and components oracles.

let n_vars = builder.log_rows([table])?;
 
let bits: [OracleId; LOG_MAX_MULTIPLICITY] = builder
    .add_committed_multiple::<LOG_MAX_MULTIPLICITY>("bits", n_vars, BinaryField1b::TOWER_LEVEL);
 
let components: [OracleId; LOG_MAX_MULTIPLICITY] = builder
    .add_committed_multiple::<LOG_MAX_MULTIPLICITY>("components", n_vars, FS::TOWER_LEVEL);

Following the basic pattern, we will next have the prover populate these columns and then we will constrain them.

Populating Columns

All that follows in this subsection takes place in a prover-only block of the form.

if let Some(witness) = builder.witness() {
    // populate components
}

First we can confirm that, as the prover, our multiplicities Option object is not empty.

let multiplicities =
    multiplicities.ok_or_else(|| anyhow::anyhow!("multiplicities empty for prover"))?;

There should be exactly as many multiplicities as there are valid table elements, which is given by table_count.

debug_assert_eq!(table_count, multiplicities.len());

We can also check all multiplicities are below the threshold.

if multiplicities
    .iter()
    .any(|&multiplicity| multiplicity >= 1 << LOG_MAX_MULTIPLICITY)
{
    return Err(anyhow::anyhow!(
        "one or more multiplicities exceed `1 << LOG_MAX_MULTIPLICITY`"
    ));
}

To populate the bits columns we create EntryBuilders for them.

let mut bit_cols = bits.map(|bit| witness.new_column::<BinaryField1b>(bit));

Since we are working with oracles over BinaryField1b, and we wish to work with each element (of each oracle) independently, we will cast not to slices of u8, u16, or u32 value as done in bitwise, but rather to slices of packed field elements. That way we can use set_packed_slice to set each element independently rather than setting an element by selecting a u8 value and then setting the appropriate bit.

let mut packed_bit_cols: [&mut [PackedType<U, BinaryField1b>]; LOG_MAX_MULTIPLICITY] =
    bit_cols.each_mut().map(|bit_col| bit_col.packed());

We do similar for the components oracles.

let mut component_cols = components.map(|component| witness.new_column::<FS>(component));
let mut packed_component_cols = component_cols
    .each_mut()
    .map(|component_col| component_col.packed());

In order to populate the components we'll need access to the slice of table values.

let table_slice = witness.get::<FS>(table)?.as_slice::<FS>();

Now we'll zip together the table slice with the multiplicities and populate each index of each bit column and component column. The jth bit column at index i is set to equal the jth bit of the multiplicity for the table value at index i. If the bit is one, we set the jth component column at index i to equal the table value at index i. If the bit is zero, we set the jth component column at index i to be zero. This is consistent with having said previously that we'd set the jth component values to be the product of the jth bit values and the table values.

izip!(table_slice, multiplicities).enumerate().for_each(
    |(i, (table_val, multiplicity))| {
        for j in 0..LOG_MAX_MULTIPLICITY {
            let bit_set = multiplicity & (1 << j) != 0;
            // set the bit value
            set_packed_slice(
                packed_bit_cols[j],
                i,
                match bit_set {
                    true => BinaryField1b::ONE,
                    false => BinaryField1b::ZERO,
                },
            );
            // set the component value
            set_packed_slice(
                packed_component_cols[j],
                i,
                match bit_set {
                    true => *table_val,
                    false => FS::ZERO,
                },
            );
        }
    },
);

Constraining Columns

To constrain these component columns with respect to the bit columns and the table column we use zero-checks.

let expression = binius_macros::arith_expr!([table, bit, component] = component - bit * table);
(0..LOG_MAX_MULTIPLICITY).for_each(|i| {
    builder.assert_zero([table, bits[i], components[i]], expression.convert_field());
});

At this point we can return the component columns, completing our get_components gadget.

Ok(components)