Module logup 

LogUp (logarithmic-derivative lookup) argument soundness.

The p3-lookup crate fingerprints each bus message into a single extension-field denominator

    denom = alpha + (bus + 1)·beta^W − Σ_k beta^k · payload_k

and enforces a running sum Σ ± multiplicity / denom = 0 over the trace. Soundness is a Schwartz–Zippel argument in the Fiat–Shamir pair (alpha, beta), sampled after the main commitment: an unbalanced multiset stays unbalanced unless (alpha, beta) is a root of the cleared fingerprint polynomial.

Cleared of denominators, that polynomial has degree ≤ N in alpha and ≤ N·W in beta, where N = num_interactions · trace_length is the number of denominator factors (interactions summed over all buses) and W = max_message_width is the widest payload. Sampling both challenges independently and uniformly from the challenge field EF, the per-variable union bound puts a numerator root at N·(W + 1) / |EF|.

A root of the numerator is not the only way through. A vanishing denominator degenerates the batched transition identity: with denom_j = 0 the common denominator itself is 0, so the constraint common_denominator · frac_local − numerator = 0 no longer pins the fraction column — frac_local is multiplied away and left completely unconstrained on that row, letting a prover write any value into it and have the accumulator absorb it. Each denominator is monic in alpha, so for any beta exactly one alpha annihilates it — that event costs N / |EF|, not N·W / |EF|.

Together

    ε_logup ≤ N·(W + 1) / |EF| + N / |EF| = N·(W + 2) / |EF|.

Bus batching is subsumed: N already sums interactions over every bus, and the beta^W bus offset is injective by construction (p3_lookup’s Challenges), so it contributes no separate error term. The multiplicity height bound (Σ wᵢ·hᵢ < p) is enforced in-circuit and is not modeled here.

The resulting term is passed to crate::stark::proven_security_report or crate::stark::conjectured_security_report as an extras SecurityTerm by the protocol call site; it is not wired into the composite automatically, since not every STARK uses lookups. In the conjectured composite it is often the binding term at large trace lengths: N grows linearly in the trace while the query-phase error does not.

References

• Haböck, Multivariate lookups based on logarithmic derivatives (2022/1530).

Structs

LogUpAir

Shape of a LogUp lookup argument, as seen by its soundness bound.

Constants

LOGUP_LABEL

Label for the LogUp fingerprint term in a crate::report::SecurityReport.

Functions

fingerprint_error

-log2(ε_logup) in bits, following ε_logup ≤ N·(W + 2) / |EF| with N = num_interactions · 2^log_trace_length and W = max_message_width.

security_term

The LogUp fingerprint term for use in extras, or None when the AIR has no interactions (no lookup argument, hence no term).