Function verify_reduction 

pub fn verify_reduction<'a, F, C>(
    gamma: &C::Elem,
    tables: impl IntoIterator<Item = TableLookup<'a, C::Elem>>,
    channel: &mut C,
) -> Result<LogupOutput<C::Elem>, Error>
where
    F: Field + ExtensionField<BinaryField1b>,
    C: IPVerifierChannel<F>,
    C::Elem: From<F> + 'a,

Verify a logUp* indexed-lookup reduction over one or more tables, each with its own lookers.

Reduces the claims (I^* T)(r) = e to the claims in LogupOutput. Each table batches its own lookers by a random linear combination: its challenge gamma scales its looker i‘s numerator by gamma^i. A table’s pushforward Y is the gamma-weighted sum of its lookers’ pushforwards, and its product check binds <T, Y> to the gamma-combination of its lookers’ claims. Tables share nothing but the batching machinery.

Every fractional-addition circuit — one per looker over n variables, plus one per table over m — is an instance of one GKR of k + max(max n, max m) layers, where k = ceil(log2(#lookers + #tables)). Its top k layers add the per-instance root fractions together and its lower layers run the instances in a batch, with every shallower instance padded by zero fractions — that leaves a fractional sum unchanged and costs O(1) per round, so the layer count depends only on the deepest instance.

No column need agree with any other on a length: an instance over d variables is simply padded by max(max n, max m) - d. A looker’s reduced index claim lands on the last n coordinates of LogupOutput::index_eval_point.

Every table’s fraction enters that sum negated, so the circuit’s root is sum_lookers num/den - sum_tables num/den, whose numerator vanishes exactly when the lookup identities hold. The verifier therefore reads only the root denominator and supplies the zero numerator itself: the identities are enforced by the shape of the claim rather than by a separate check.

Why one logUp challenge per table

Each table is randomized by its own c, so table t’s contribution to the root fraction,

    f_t(c_t) = sum_i gamma_t^i sum_x eq_{r_i}(x)/(c_t - I_i(x))  -  sum_v Y_t(v)/(c_t - v)

is a rational function of c_t alone, vanishing as c_t grows. A sum of such functions in disjoint variables is identically zero only when every term is, so the one root check certifies every table separately. Under a single shared challenge that argument fails: two tables could miscount the same position in opposite directions and cancel inside the root numerator.

The logUp challenges are sampled against the committed I, T, and pushforwards Y. So the caller must absorb those commitments into the transcript before calling this routine, and must have sampled each table’s gamma before its pushforward commitment.

Arguments

• tables - One TableLookup per table, each carrying its batching challenge, its variable count, and its lookers’ claims.
• channel - The verifier channel for receiving prover messages and sampling challenges.

Transcript layout

The prover messages are consumed in this exact order:

    1. sample c                         (one logUp challenge per table)
    2. recv den_root                    (the root denominator; its numerator is 0)
    3. combined GKR, k + max(max n, max m) layers (see fracaddcheck::verify)
    4. recv per-looker index evaluations, then per-table Y (the non-transparent leaf halves)
    5. pushforward reduction:
       a. sample batch_coeff
       b. max m rounds of degree-2 sumcheck
       c. recv per-table [Y, T]         (evaluations at the challenge point)

The per-looker index evaluations arrive table by table, in the order the tables are given, and within a table in its own looker order.

The sumchecks are assumed to bind variables from the highest index to the lowest. This matches the convention of the fractional-addition GKR layers.

Preconditions

• tables is non-empty, every table has at least one variable so its GKR has a variable to split on, and every table has at least one looker.

Returns

The reduced LogupOutput claims on the tables, pushforwards, and index multilinears.

Errors

Returns an error when the proof is malformed or any verification identity fails:

• a GKR layer’s reduction is inconsistent, which is where a violated lookup identity surfaces,
• the transparent leaf numerators do not interpolate to the batch’s leaf numerator,
• the index and table denominators do not interpolate to the batch’s leaf denominator,
• the pushforward reduction is inconsistent.