Module logup_star 

Verifier for the logUp* indexed-lookup reduction of knowledge.

logUp* proves an indexed lookup (I^* T)[i] = T[I[i]]. Unlike classic logUp, it never commits the looked-up vector I^* T. Multiple lookers may share one table (and one pushforward) by a random linear combination: a challenge gamma weights looker j by gamma^j, and the per-looker circuits run batched (see crate::fracaddcheck). Several tables may be read in one reduction, each looker naming the one it reads. Every table keeps its own pushforward and its own logUp challenge; only the batching machinery is shared. See Soukhanov25 for the construction.

What is being proved

The caller holds a claim about the looked-up vector at a point:

    (I^* T)(r) = e

The symbols are:

• T: the table multilinear, with m variables (2^m entries).
• I: the index multilinear, with n variables (2^n entries).
• r: the n-coordinate evaluation point.
• e: the claimed evaluation.

The reduction turns this one claim into three separate evaluation claims:

• one on the table T,
• one on the pushforward Y,
• one on the index I.

The caller verifies those three claims, which is out of scope here.

The pushforward trick

Let X = eq_r be the equality-indicator multilinear at the point r. Pullback and pushforward are dual under the inner product, which gives:

    (I^* T)(r) = <I^* T, eq_r> = <T, I_* eq_r> = <T, Y>

Here Y = I_* eq_r is the pushforward of eq_r along I. Y has only 2^m entries, which is cheap. The avoided vector I^* T has 2^n entries, which is expensive when n is large.

The two checks

First, pushforward correctness, via a logarithmic-derivative (logUp) identity for a random c:

    sum_{i in B_n} eq_r(i) / (c - I(i)) = sum_{j in B_m} Y(j) / (c - j)

• Each side is a sum of fractions.
• A fractional-addition GKR circuit collapses each side to a single root fraction.
• Equality of the two sums is the cross-multiplication of the two root fractions.

See crate::fracaddcheck for the GKR circuit.

Second, the product claim <T, Y> = e, proved by a product sumcheck over the m-variable cube.

Batching the last GKR layer with the product sumcheck

The table-side GKR circuit ends in an evaluation of Y. The product sumcheck also ends in an evaluation of Y. Run naively, these are two distinct evaluations at two distinct points.

Both reductions share the same final step:

• they split the leaf multilinears on the highest variable into two halves,
• they combine the halves over the same m-1 low variables,
• they finish with one line-fold over the highest variable.

So both can run as one (m-1)-variable sumcheck followed by one shared line-fold. That yields a single evaluation point, collapsing the two Y evaluations into one.

Transparent tables

A transparent (succinct) table is one the verifier evaluates itself, without a commitment. Against such a table the product sumcheck is not needed at all. Both of the claims it would reduce are linear relations on the one multilinear Y:

    <Y, eq_z> = Y(z)      the fractional-addition leaf claim
    <Y, T>    = e         the product claim

A caller holding Y as a committed oracle opens the two together against that one commitment. verify_reduction_transparent stops the reduction there and hands both claims back.

Soundness

• The logUp identity for a random c catches a wrong Y except with probability (n + m) / |F|.
• This is Lemma 2 of Soukhanov25: the identity holds only when Y = I_* eq_r.
• The two GKR circuits and the batched sumcheck add the usual sumcheck soundness error.
• The cross-multiplication of the root fractions assumes both root denominators are nonzero.
• A root denominator is a product of factors c - I(i) or c - j.
• That product is nonzero except with probability (n + m) / |F| over the random c.
• With several tables, each is randomized by its own challenge c_t, so its contribution to the root fraction is a rational function of c_t alone. A sum of such functions in disjoint variables vanishes only when each does, which is what lets the one root check certify every table. Under a shared challenge two tables’ errors could cancel.

Index embedding

Table positions j in 0..2^m and committed index values I[i] live in the same domain. A position is embedded into F through the GF(2)-linear basis:

    iota(j) = sum_{t : bit t of j is set} basis(t)

The table-side denominator multilinear is therefore J(x) = sum_t basis(t) * x_t. The verifier evaluates it by itself. This matches the index encoding used elsewhere in the Spartan verifier.

Structs

LogupOutput

The reduced output claims of a logUp* verification.

LogupTableOutput

The reduced claims belonging to one table.

LogupTransparentOutput

The open claims of a logUp* verification that leaves the table side unclosed.

LogupTransparentTableOutput

The open claims belonging to one table whose table side is left unclosed.

LookerClaim

One looker’s claim on its looked-up vector: (I^* T)(eval_point) = eval_claim.

TableLookup

One table together with the lookers that read it.

Enums

Error

VerificationError

Functions

verify_reduction

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

verify_reduction_transparent

Verify a logUp* reduction over transparent tables, leaving the table side open.