Skip to content

Example Application

Multiplying unsigned integers using lookups

Let us make use of our lookup gadget plain_lookup. The lookup relation we wish to illustrate is the multiplication of two u8 values into a u16 value. First we'll create a testing function test_u8_mul_lookup that accepts a log_lookup_count parameter for how many random lookups to perform, and returns a boundary value. Then we'll write prover and verifier functions to invoke test_u8_mul_lookup and use the boundary value returned in verification.

We first choose what parameters the prover and verifier will share.

const MAX_LOG_MULTIPLICITY: usize = 18;
let log_lookup_count = 19;
 
let log_inv_rate = 1;
let security_bits = 20;

The Tester

A lookup claim consists of the two 8-bit inputs concatenated with the 16-bit output into a 32-bit BinaryField32b element.

fn into_lookup_claim(x: u8, y: u8, z: u16) -> u32 {
	((z as u32) << 16) | ((y as u32) << 8) | (x as u32)
}

Our lookup will take place with FS as BinaryField32b.

Before we invoke the lookup gadget, we generate the lookup table.

fn generate_u8_mul_table() -> Vec<u32> {
	let mut result = Vec::with_capacity(1 << 16);
	for x in 0..=255u8 {
		for y in 0..=255u8 {
			let product = x as u16 * y as u16;
			result.push(into_lookup_claim(x, y, product));
		}
	}
	result
}

For values to lookup, we can generate them randomly.

fn generate_random_u8_mul_claims(vals: &mut [u32]) {
	use rand::Rng;
	vals.par_iter_mut().for_each(|val| {
		let mut rng = rand::thread_rng();
		let x = rng.gen_range(0..=255u8);
		let y = rng.gen_range(0..=255u8);
		let product = x as u16 * y as u16;
		*val = into_lookup_claim(x, y, product);
	});
}

Before looking inside test_u8_mul_lookup we see the signature to be

pub fn test_u8_mul_lookup<U, F, const LOG_MAX_MULTIPLICITY: usize>(
	builder: &mut ConstraintSystemBuilder<U, F>,
	log_lookup_count: usize,
) -> Result<Boundary<F>, anyhow::Error>
where
	U: PackScalar<F> + PackScalar<BinaryField1b> + PackScalar<BinaryField32b> + Pod,
	F: TowerField + ExtensionField<BinaryField32b>,

Inside this test we can first generate the table and create a transparent oracle for it.

let table_values = generate_u8_mul_table();
let table = transparent::make_transparent(
    builder,
    "u8_mul_table",
    bytemuck::cast_slice::<_, BinaryField32b>(&table_values),
)?;

We also need an oracle holding the values to lookup, and this will be a committed oracle containing arbitrary prover-chosen lookup values.

let lookup_values =
    builder.add_committed("lookup_values", log_lookup_count, BinaryField32b::TOWER_LEVEL);

The lookup gadget accepts table_count and lookup_values_count parameters, both of usize, to dictate how many values in the table column are to be taken as valid table values, and how many values in lookup_values are to be looked up.

let table_count = table_values.len();
let lookup_values_count = 1 << log_lookup_count;

Here we've set them to their fullest, where all values in table are valid values, and all values in lookup_values are to be looked up.

To populate the committed lookup_values column we make a prover-only block in which we create a new column, cast it to a mutable slice, and pass part of it to generate_random_u8_mul_claims for filling with random lookup claims.

if let Some(witness) = builder.witness() {
    let mut lookup_values_col = witness.new_column::<BinaryField32b>(lookup_values);
    let mut_slice = lookup_values_col.as_mut_slice::<u32>();
    generate_random_u8_mul_claims(&mut mut_slice[0..lookup_values_count]);
}

Lastly we invoke the plain_lookup gadget, receiving back a boundary value, and we return that boundary value from our test so it can be used by the verifier.

The Prover

The prover executes and obtains the proof as follows.

let proof = {
    let allocator = bumpalo::Bump::new();
    let mut builder = ConstraintSystemBuilder::<U, F>::new_with_witness(&allocator);
 
    let _boundary = plain_lookup::test_u8_mul_lookup::<_, _, MAX_LOG_MULTIPLICITY>(
        &mut builder,
        log_lookup_count,
    )
    .unwrap();
 
    let witness = builder.take_witness().unwrap();
    let constraint_system = builder.build().unwrap();
    // validating witness with `validate_witness` is too slow for large transparents like the `table`
 
    let domain_factory = DefaultEvaluationDomainFactory::default();
    let backend = make_portable_backend();
 
    constraint_system::prove::<
        U,
        CanonicalTowerFamily,
        BinaryField64b,
        _,
        _,
        GroestlHasher<BinaryField128b>,
        GroestlDigestCompression<BinaryField8b>,
        HasherChallenger<groestl_crypto::Groestl256>,
        _,
    >(&constraint_system, log_inv_rate, security_bits, witness, &domain_factory, &backend)
    .unwrap()
};

The Verifier

The verifier verifies the proof as follows.

{
    let mut builder = ConstraintSystemBuilder::<U, F>::new();
 
    let boundary = plain_lookup::test_u8_mul_lookup::<_, _, MAX_LOG_MULTIPLICITY>(
        &mut builder,
        log_lookup_count,
    )
    .unwrap();
 
    let constraint_system = builder.build().unwrap();
 
    constraint_system::verify::<
        U,
        CanonicalTowerFamily,
        _,
        GroestlHasher<BinaryField128b>,
        GroestlDigestCompression<BinaryField8b>,
        HasherChallenger<Groestl256>,
    >(&constraint_system, log_inv_rate, security_bits, vec![boundary], proof)
    .unwrap();
}

See the full code example here.