Function plain_lookup

pub fn plain_lookup<U, F, FS, const LOG_MAX_MULTIPLICITY: usize>(
    builder: &mut ConstraintSystemBuilder<'_, U, F>,
    table: OracleId,
    table_count: usize,
    balancer_value: FS,
    lookup_values: OracleId,
    lookup_values_count: usize,
) -> Result<Boundary<F>, Error>
where
    U: PackScalar<F> + PackScalar<FS> + PackScalar<BinaryField1b> + Pod,
    F: TowerField + 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.
• table_count: only the first table_count values of table are considered valid lookup values.
• balancer_value: any valid table value, needed for balancing the channel.
• 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.

Constraints

• no value in lookup_values can be looked only less than 1 << LOG_MAX_MULTIPLICITY times, limiting completeness not soundness.

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 commits columns holding the bit-decomposition of the multiplicities. Using these bit columns we create component columns the same height as the table, which select the table value where a multiplicity bit is 1 and select balancer_value where the bit is 0. Pulling these component columns out of the channel with appropriate multiplicities, we pull out each table value from the channel with the multiplicity requested by the prover. Due to the balancer_value appearing in the component columns, however, we will also pull the table value balancer_value from the channel many more times than needed. To rectify this we put balancer_value in a boundary value and push this boundary value to the channel with a multiplicity that will balance the channel. This boundary value is returned from the gadget.