Function plain_lookup

pub fn plain_lookup<FS, const LOG_MAX_MULTIPLICITY: usize>(
    builder: &mut ConstraintSystemBuilder<'_>,
    table: OracleId,
    lookup_values: OracleId,
    lookup_values_count: usize,
) -> Result<(), Error>
where
    U: PackScalar<FS> + Pod,
    F: ExtensionField<FS>,
    FS: TowerField + Pod,

Checks values in lookup_values to be in table.

Introduction

This is a gadget for performing a “lookup”, wherein a set of values are claimed by the prover to be a subset of a set of values known to the verifier. We call the set of values known to the verifier as the “table”, and we call the set of values held by the prover as the “lookup values.” We represent these sets using oracles table and lookup_values as lists of values. This gadget performs the lookup by verifying that every value in the oracle lookup_vales appears somewhere in the oracle table.

Parameters

• builder: a mutable reference to the ConstraintSystemBuilder.
• table: an oracle holding the table of valid lookup values.
• lookup_values: an oracle holding the values to be looked up.
• lookup_values_count: only the first lookup_values_count values in lookup_values will be looked up.

How this Works

We create a single channel for this lookup. We let the prover push all values in lookup_values, that is all values to be looked up, into the channel. We also must pull valid table values (i.e. values that appear in table) from the channel if the channel is to balance. By ensuring that only valid table values get pulled from the channel, and observing the channel to balance, we ensure that only valid table values get pushed (by the prover) into the channel. Therefore our construction is sound. In order for the construction to be complete, allowing an honest prover to pass, we must pull each table value from the channel with exactly the same multiplicity (duplicate count) that the prover pushed that table value into the channel. To do so, we allow the prover to commit information on the multiplicity of each table value.

The prover counts the multiplicity of each table value, and creates a bit column for each of the LOG_MAX_MULTIPLICITY bits in the bit-decomposition of the multiplicities. Then we flush the table values LOG_MAX_MULTIPLICITY times, each time using a different bit column as the ‘selector’ oracle to select which values in the table actually get pushed into the channel flushed. When flushing the table with the i’th bit column as the selector, we flush with multiplicity 1 << i.