From 2ecdd36d74108ff5dc178d99ce130c531ef5e4f4 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 30 Jul 2026 11:37:50 -0300 Subject: [PATCH 1/2] logup: chained partial accumulators, no committed inverses MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the committed-inverse logUp layout with chained partial accumulators. Stage 2 previously committed (1 + L) extension columns per circuit — a running accumulator plus one message inverse per lookup — tied together by L message-inverse constraints and three accumulator constraints (first row, transition, last row). Now it commits max(L, 1) columns: acc_j (slot j) is the running sum ENTERING lookup j's step on that row, and each step asserts acc_{j+1} - acc_j = mult_j/m_j multiplied through by the message: interior (j < L-1): m_j * (acc_{j+1} - acc_j) - mult_j = 0 wrap (j = L-1): m_j * (acc_0' - acc_j + is_last_row*D) - mult_j = 0 where acc_0' is the next row's first slot and D = acc_final - acc_initial (the existing publics, slots 3 and 2). The wrap step needs no transition selector: on the trace subgroup "next row" is rotation by the generator, so the chain is a CYCLE. Telescoping the steps around the cycle cancels every accumulator term and forces the circuit's multiset sum to zero; the is_last_row*D term perturbs exactly one link, turning that into "the multiset sum equals the public accumulator difference". No first/transition/last-row constraints remain, and the committed accumulator is gauge-free (only differences are constrained; the prover starts it at zero). The wrap step consumes is_last_row ADDITIVELY, so it must be the NORMALIZED last-row Lagrange selector: p3's is_last_row is the unnormalized numerator (x^n - 1)/(x - g^{-1}) whose value at the last row is n*g (pinned by a new test against the textbook Lagrange product). The prover and verifier now normalize is_first_row by 1/n and is_last_row by 1/(n*g); vanishing-form user constraints are unaffected by the rescale, and the witness-side lookup evaluation already used indicator values 1. Effects: - stage-2 width (1+L)*D -> max(L,1)*D; logUp constraints L+3 -> L. - Degrees are uniform: every step is max(deg(args)+1, deg(mult)) (the injection is selector*publics, degree multiple 1, absorbed by add = max) — never above the old profile, lower where the old last-row constraint peaked. - Witness build: same batch inversion, then a single pass with one multiply-add per (row, lookup), pushing each partial accumulator; the circuit's local sum feeds the global public chain. - Zero-multiplicity (padding) rows force the accumulators to ride through unchanged. Benchmarked against the pre-change rev (2501b4f) with identical instrumentation (lookup-heavy circuit, 16 lookups x 4 args, 2^14 rows): stage-2 build ~9.6 ms on both; quotient constraint eval ~19.0 ms vs ~18.9 ms — no regression, with one fewer committed column and fewer alpha terms. 29/29 tests (pin test re-derived against the new spec; even/odd e2e exercises a nonzero per-circuit accumulator difference, pinning the selector normalization through a real proof); clippy/fmt clean. --- src/lookup.rs | 374 ++++++++++++++++++++++++++++++++---------------- src/prover.rs | 20 ++- src/verifier.rs | 24 +++- 3 files changed, 285 insertions(+), 133 deletions(-) diff --git a/src/lookup.rs b/src/lookup.rs index 06314ed..1be1be9 100644 --- a/src/lookup.rs +++ b/src/lookup.rs @@ -14,10 +14,15 @@ //! //! - **Publics** (each an extension value, stored as `d` base coordinates): //! slot 0 = β (lookup challenge), 1 = γ (fingerprint challenge), -//! 2 = current accumulator, 3 = next accumulator. So `num_publics = 4·d`. -//! - **Stage-2 columns** (extension values, flattened to base): slot 0 = the -//! running accumulator, slots `1..=L` = the message inverse of each lookup, -//! in lookup order. So `stage2_width = (1 + L)·d` base columns. +//! 2 = the accumulator entering the circuit (`acc_initial`), 3 = the +//! accumulator leaving it (`acc_final`). So `num_publics = 4·d`. +//! - **Stage-2 columns** (extension values, flattened to base): slot `j` = +//! the partial accumulator entering lookup `j`'s chained step (a single +//! pass-through accumulator when the circuit has no lookups). So +//! `stage2_width = max(L, 1)·d` base columns. No message inverses are +//! committed — see `synthesize_lookups` for how the chained-accumulator +//! argument works. The committed accumulator is gauge-free (only +//! differences are constrained); the prover starts it at zero. use p3_field::{ Algebra, ExtensionField, Field, PrimeCharacteristicRing, batch_multiplicative_inverse, @@ -79,18 +84,18 @@ pub fn num_publics(d: usize) -> usize { } /// Stage-2 trace width (flattened base columns) for `num_lookups` lookups -/// at extension degree `d`: one accumulator column plus one inverse column -/// per lookup. +/// at extension degree `d`: one partial-accumulator column per lookup +/// (`acc_j` entering lookup `j`'s step), or a single pass-through +/// accumulator column when the circuit has no lookups. pub fn stage2_width(num_lookups: usize, d: usize) -> usize { - (1 + num_lookups) * d + num_lookups.max(1) * d } /// Number of base-field constraint values the logUp argument contributes: -/// one extension constraint per lookup (message · inverse = 1) plus the -/// three accumulator constraints (first/transition/last row), each expanded -/// into `d` coordinates. +/// one chained-accumulator step per lookup (or the single pass-through +/// constraint when there are none), each expanded into `d` coordinates. pub fn logup_constraint_count(num_lookups: usize, d: usize) -> usize { - (num_lookups + 3) * d + num_lookups.max(1) * d } /// Coordinate product in the binomial extension `X^d = w`, schoolbook: @@ -124,21 +129,23 @@ fn mul2 + Copy>(a: (A, A), b: (A, A), w: F) -> (A, A) { /// Directly evaluates the logUp constraint values at one evaluation context, /// in the canonical protocol order: for each lookup (in order) the `d` -/// coordinates of `(β + fingerprint(γ, args)) · inv − 1`, then the `d` -/// coordinates each of the first-row, transition, and last-row accumulator -/// constraints. Semantically identical to compiling -/// [`synthesize_lookups`]'s constraints and evaluating their roots (see the -/// pin test), without materializing them. +/// coordinates of its chained-accumulator step — interior steps +/// `m_j·(acc_{j+1} − acc_j) − mult_j`, the wrap step carrying the +/// `is_last_row·Δ` boundary injection (see [`synthesize_lookups`] for the full +/// derivation). Semantically identical to compiling the synthesized +/// constraints and evaluating their roots (see the pin test), without +/// materializing them. /// /// Everything is base-field coordinate arithmetic, so the working type `A` /// is generic: `PackedVal` on the prover's quotient domain, the challenge /// field at ζ for the verifier — both sides share this one implementation. /// /// Layout contracts (see the module docs): `publics` holds the 4·d base -/// coordinates of (β, γ, acc, next_acc); `stage2` / `stage2_next` are the -/// flattened stage-2 base columns, slot 0 the accumulator, slot `1+j` the -/// message inverse of lookup `j`. `lookups` carries the evaluated lookup -/// expressions (multiplicity and args embed in coordinate 0). +/// coordinates of (β, γ, acc_initial, acc_final); `stage2` / `stage2_next` +/// are the flattened stage-2 base columns, slot `j` the partial accumulator +/// entering lookup `j`'s step. `is_last_row` is the NORMALIZED last-row +/// selector value. `lookups` carries node ids into `node_vals` (multiplicity +/// and args embed in coordinate 0). #[allow(clippy::too_many_arguments)] pub fn logup_constraint_values + Copy>( lookups: &[Lookup], @@ -146,9 +153,7 @@ pub fn logup_constraint_values + Copy>( stage2: &[A], stage2_next: &[A], publics: &[A], - is_first_row: A, is_last_row: A, - is_transition: A, w: F, d: usize, out: &mut Vec, @@ -160,49 +165,78 @@ pub fn logup_constraint_values + Copy>( let nv = |id: crate::graph::NodeId| node_vals[id.index()]; let beta = (publics[0], publics[1]); let gamma = (publics[2], publics[3]); - let acc = (publics[4], publics[5]); - let next_acc = (publics[6], publics[7]); - let acc_col = (stage2[0], stage2[1]); - let next_acc_col = (stage2_next[0], stage2_next[1]); + // The boundary injection: is_last_row·(acc_final − acc_initial). + let inj = ( + is_last_row * (publics[6] - publics[4]), + is_last_row * (publics[7] - publics[5]), + ); + + if lookups.is_empty() { + // Pass-through accumulator: acc′ − acc + is_last_row·Δ = 0. + out.push(stage2_next[0] - stage2[0] + inj.0); + out.push(stage2_next[1] - stage2[1] + inj.1); + return; + } - let mut acc_expr = acc_col; + let last = lookups.len() - 1; for (j, lookup) in lookups.iter().enumerate() { - let inv = (stage2[2 + 2 * j], stage2[3 + 2 * j]); + let source = (stage2[2 * j], stage2[2 * j + 1]); + let target = if j < last { + (stage2[2 * j + 2], stage2[2 * j + 3]) + } else { + (stage2_next[0] + inj.0, stage2_next[1] + inj.1) + }; // fingerprint = Σ_i args[i] · γ^i, Horner over the reversed args. let mut f = (A::ZERO, A::ZERO); for &arg in lookup.args.iter().rev() { f = mul2(f, gamma, w); f.0 += nv(arg); } - // message = β + fingerprint; constraint: message · inv − 1 = 0. - let c = mul2((f.0 + beta.0, f.1 + beta.1), inv, w); - out.push(c.0 - A::ONE); + // step: (β + fingerprint)·(target − source) − mult = 0. + let c = mul2( + (f.0 + beta.0, f.1 + beta.1), + (target.0 - source.0, target.1 - source.1), + w, + ); + out.push(c.0 - nv(lookup.multiplicity)); out.push(c.1); - let m = nv(lookup.multiplicity); - acc_expr.0 += inv.0 * m; - acc_expr.1 += inv.1 * m; } - out.push(is_first_row * (acc_col.0 - acc.0)); - out.push(is_first_row * (acc_col.1 - acc.1)); - out.push(is_transition * (acc_expr.0 - next_acc_col.0)); - out.push(is_transition * (acc_expr.1 - next_acc_col.1)); - out.push(is_last_row * (acc_expr.0 - next_acc.0)); - out.push(is_last_row * (acc_expr.1 - next_acc.1)); return; } let beta = &publics[..d]; let gamma = &publics[d..2 * d]; - let acc = &publics[2 * d..3 * d]; - let next_acc = &publics[3 * d..4 * d]; - let acc_col = &stage2[..d]; - let next_acc_col = &stage2_next[..d]; - - // acc_expr = acc_col + Σ_j multiplicity_j · inv_j, built alongside the - // message constraints exactly as `synthesize_lookups` does. - let mut acc_expr: Vec = acc_col.to_vec(); + let acc_initial = &publics[2 * d..3 * d]; + let acc_final = &publics[3 * d..4 * d]; + // The boundary injection: is_last_row·(acc_final − acc_initial). + let inj: Vec = acc_final + .iter() + .zip(acc_initial) + .map(|(&f, &i)| is_last_row * (f - i)) + .collect(); + + if lookups.is_empty() { + for k in 0..d { + out.push(stage2_next[k] - stage2[k] + inj[k]); + } + return; + } + + let last = lookups.len() - 1; for (j, lookup) in lookups.iter().enumerate() { - let inv = &stage2[(1 + j) * d..(2 + j) * d]; + let source = &stage2[j * d..(j + 1) * d]; + let mut target: Vec = if j < last { + stage2[(j + 1) * d..(j + 2) * d].to_vec() + } else { + stage2_next[..d] + .iter() + .zip(&inj) + .map(|(&t, &i)| t + i) + .collect() + }; + for (t, &s) in target.iter_mut().zip(source) { + *t -= s; + } // fingerprint = Σ_i args[i] · γ^i, via Horner over the reversed args // (base values embed in coordinate 0). @@ -212,32 +246,14 @@ pub fn logup_constraint_values + Copy>( fingerprint[0] += node_vals[arg.index()]; } - // message = β + fingerprint; constraint: message · inv − 1 = 0. + // step: (β + fingerprint)·(target − source) − mult = 0. let mut message = fingerprint; for (m, &b) in message.iter_mut().zip(beta) { *m += b; } - let mut constraint = coord_mul(&message, inv, w); - constraint[0] -= A::ONE; + let mut constraint = coord_mul(&message, &target, w); + constraint[0] -= node_vals[lookup.multiplicity.index()]; out.extend_from_slice(&constraint); - - let mv = node_vals[lookup.multiplicity.index()]; - for (a, &i) in acc_expr.iter_mut().zip(inv) { - *a += i * mv; - } - } - - // First row: acc_col = acc. - for k in 0..d { - out.push(is_first_row * (acc_col[k] - acc[k])); - } - // Transition: acc_expr = next row's accumulator column. - for k in 0..d { - out.push(is_transition * (acc_expr[k] - next_acc_col[k])); - } - // Last row: acc_expr = next_acc. - for k in 0..d { - out.push(is_last_row * (acc_expr[k] - next_acc[k])); } } @@ -247,48 +263,92 @@ pub fn logup_constraint_values + Copy>( /// IsFirstRow/IsLastRow 1, add = max, mul = sum). pub fn logup_max_degree(graph: &crate::graph::ConstraintGraph) -> u32 { let node_degree = |id: crate::graph::NodeId| graph.degrees[id.index()]; - // acc_expr = acc_col (deg 1) + Σ mult·inv (deg mult + 1). - let acc_degree = graph - .lookups - .iter() - .map(|l| node_degree(l.multiplicity) + 1) - .max() - .unwrap_or(0) - .max(1); - // Per lookup: (β + fingerprint(args)) · inv, degree = max arg degree + 1. - let message_degree = graph + // Every step is m_j·(accumulator difference) − mult_j, and the + // difference — including the wrap step's is_last_row·Δ injection + // (selector·publics) — has degree multiple 1. So per lookup: + // max(max arg degree + 1, mult degree); a lookup-free circuit's + // pass-through constraint is degree 1. + graph .lookups .iter() - .map(|l| l.args.iter().map(|&a| node_degree(a)).max().unwrap_or(0) + 1) + .map(|l| { + let message_degree = l.args.iter().map(|&a| node_degree(a)).max().unwrap_or(0); + (message_degree + 1).max(node_degree(l.multiplicity)) + }) .max() - .unwrap_or(0); - // First row: 1 + 1; transition: 0 + acc; last: 1 + acc. - message_degree.max(2).max(acc_degree + 1) + .unwrap_or(1) } -/// Builds the logUp stage-2 constraints for `lookups` at extension degree -/// `d`. Order: the per-lookup message/inverse constraints in lookup order, -/// then the first-row, transition, and last-row accumulator constraints. +/// Builds the chained-accumulator logUp constraints for `lookups` at +/// extension degree `d` (the executable specification that +/// [`logup_constraint_values`] is pinned against in tests; it is not +/// compiled into the circuit graph). +/// +/// # How the chained-accumulator argument works /// -/// Since the direct-evaluation change this is no longer compiled into the -/// circuit graph; it remains as the executable specification that -/// [`logup_constraint_values`] is pinned against in tests. +/// Stage 2 commits one partial accumulator per lookup: `acc_j` (slot `j`) +/// is the running sum entering lookup `j`'s step on that row. Each step +/// asserts `acc_{j+1} − acc_j = mult_j / m_j`, multiplied through by the +/// message `m_j = β + fingerprint(γ, args_j)` to stay polynomial: +/// +/// ```text +/// interior (j < L−1): m_j · (acc_{j+1} − acc_j) − mult_j = 0 +/// wrap (j = L−1): m_j · (acc_0′ − acc_j + is_last_row·Δ) − mult_j = 0 +/// ``` +/// +/// where `acc_0′` is the NEXT row's first slot, `Δ = acc_final − +/// acc_initial` (publics slots 3 and 2), and `is_last_row` is the NORMALIZED +/// last-row Lagrange selector (value exactly 1 on the last row — see the +/// selector-normalization pin test). +/// +/// The wrap step needs no transition selector: on the trace subgroup +/// "next row" is rotation by the generator, so the last row's `acc_0′` IS +/// the first row's `acc_0` and the chain is a cycle. Telescoping the step +/// constraints around that cycle cancels every accumulator term, leaving +/// `Σ_rows Σ_j mult_j/m_j = Δ` — the injected `is_last_row·Δ` perturbs +/// exactly one link, converting "the multiset sum is zero" into "the +/// multiset sum is the public accumulator difference". No first-row, +/// transition, or last-row constraints remain: the committed accumulator +/// is gauge-free (only differences are constrained; the prover starts it +/// at zero by convention). +/// +/// A circuit with no lookups gets a single pass-through column with +/// `acc′ − acc + is_last_row·Δ = 0`, forcing `Δ = 0`. +/// +/// Zero-multiplicity rows (padding) force `acc_{j+1} = acc_j` through a +/// (whp) nonzero message — the accumulators simply ride through. +/// +/// Degrees are uniform: every constraint is `max(deg(args)+1, deg(mult))` +/// (the injected term is selector·publics, degree multiple 1, absorbed by +/// `add = max`). pub fn synthesize_lookups(lookups: &[Lookup>], d: usize) -> Vec> { let d = u32::try_from(d).expect("extension degree exceeds u32"); let beta = ExtExpr::public(0, d); let gamma = ExtExpr::public(1, d); - let acc = ExtExpr::public(2, d); - let next_acc = ExtExpr::public(3, d); - let acc_col = ExtExpr::stage2(0, d, RowOffset::Current); - let next_acc_col = ExtExpr::stage2(0, d, RowOffset::Next); - - let mut constraints = Vec::with_capacity(lookups.len() + 3); - // acc_expr = acc_col + Σ_j multiplicity_j · inv_j, built once and reused - // by the transition and last-row constraints (the interner shares it). - let mut acc_expr = acc_col.clone(); + let acc_initial = ExtExpr::public(2, d); + let acc_final = ExtExpr::public(3, d); + // The boundary injection: is_last_row·Δ. `Expr::IsLastRow` is the + // normalized last-row selector protocol-wide. + let injection = ExtExpr::from(Expr::IsLastRow) * (acc_final - acc_initial); + + if lookups.is_empty() { + // Pass-through accumulator: acc′ − acc + is_last_row·Δ = 0. + return vec![ + ExtExpr::stage2(0, d, RowOffset::Next) - ExtExpr::stage2(0, d, RowOffset::Current) + + injection, + ]; + } + + let last = lookups.len() - 1; + let mut constraints = Vec::with_capacity(lookups.len()); for (j, lookup) in lookups.iter().enumerate() { - let slot = 1 + u32::try_from(j).expect("lookup count exceeds u32"); - let inv = ExtExpr::stage2(slot, d, RowOffset::Current); + let slot = u32::try_from(j).expect("lookup count exceeds u32"); + let source = ExtExpr::stage2(slot, d, RowOffset::Current); + let target = if j < last { + ExtExpr::stage2(slot + 1, d, RowOffset::Current) + } else { + ExtExpr::stage2(0, d, RowOffset::Next) + injection.clone() + }; // fingerprint = Σ_i args[i] · γ^i, via Horner over the reversed args. let mut coeffs = lookup.args.iter().rev(); @@ -300,20 +360,11 @@ pub fn synthesize_lookups(lookups: &[Lookup>], d: usize) -> Ve fingerprint = fingerprint * gamma.clone() + arg.clone(); } - // message = β + fingerprint; constraint: message · inv − 1 = 0. + // message = β + fingerprint; step: m·(target − source) − mult = 0. let message = beta.clone() + fingerprint; - constraints.push(message * inv.clone() - Expr::constant(F::ONE)); - - acc_expr = acc_expr + lookup.multiplicity.clone() * inv; + constraints.push(message * (target - source) - lookup.multiplicity.clone()); } - // First row: acc_col = acc. - constraints.push(Expr::IsFirstRow * (acc_col - acc)); - // Transition: acc_expr = next row's accumulator column. - constraints.push(Expr::IsTransition * (acc_expr.clone() - next_acc_col)); - // Last row: acc_expr = next_acc. - constraints.push(Expr::IsLastRow * (acc_expr - next_acc)); - constraints } @@ -462,28 +513,36 @@ impl LookupValues { offset += num_circuit_messages; let vec = if circuit.num_lookups == 0 { - // No row lookup. Just repeat the accumulator for each row. - vec![accumulator; circuit.height] + // Pass-through accumulator column; the committed values are + // gauge-free (only differences are constrained), zero by + // convention. + vec![EF::ZERO; circuit.height] } else { - // Flatten each row accumulator followed by the inverse of the message - // associated with each row lookup. - let mut vec = Vec::with_capacity(circuit.height * (1 + circuit.num_lookups)); + // One partial accumulator per lookup slot: `acc_j` is the + // running sum ENTERING lookup j's step; the last step's + // result carries into the next row's slot 0. Single pass, + // one multiply-add per (row, lookup). The column is + // gauge-free, so it starts at zero regardless of the global + // accumulator; the circuit's total contribution is added to + // the global chain at the end. + let mut vec = Vec::with_capacity(circuit.height * circuit.num_lookups); + let mut local = EF::ZERO; for (row_multiplicities, row_messages_inverses) in circuit .multiplicities .chunks_exact(circuit.num_lookups) .zip(circuit_messages_inverses.chunks_exact(circuit.num_lookups)) { - vec.push(accumulator); for (&multiplicity, &message_inverse) in row_multiplicities.iter().zip(row_messages_inverses) { - accumulator += EF::from(multiplicity) * message_inverse; - vec.push(message_inverse); + vec.push(local); + local += EF::from(multiplicity) * message_inverse; } } + accumulator += local; vec }; - let width = 1 + circuit.num_lookups; + let width = circuit.num_lookups.max(1); debug_assert_eq!(vec.len() % width, 0); let trace = RowMajorMatrix::new(vec, width); intermediate_accumulators.push(accumulator); @@ -626,6 +685,74 @@ mod tests { use super::*; + /// The selector `p3` provides is the UNNORMALIZED Lagrange numerator + /// `is_last_row(x) = (x^n − 1)/(x − g^{−1})`; its value at the last row + /// is `n·g` (the zerofier derivative there). The chained logUp wrap + /// constraint uses the selector additively, so it must be normalized to + /// value exactly 1 at the last row: `is_last_row/(n·g)` has value 1 there. + /// This pins that constant (and `1/n` for the first row) against the + /// textbook Lagrange basis product, at arbitrary points, several sizes. + #[test] + fn selector_normalization_constants() { + use crate::config::StarkGenericConfig; + use crate::types::ExtVal; + use p3_commit::PolynomialSpace; + use p3_field::{PrimeCharacteristicRing, TwoAdicField}; + + let config = GoldilocksBlake3Config::new( + CommitmentParameters { + log_blowup: 1, + cap_height: 0, + }, + FriParameters { + log_final_poly_len: 0, + max_log_arity: 1, + num_queries: 1, + commit_proof_of_work_bits: 0, + query_proof_of_work_bits: 0, + }, + ); + for log_n in [2usize, 3, 5, 8] { + let n = 1usize << log_n; + let g = Val::two_adic_generator(log_n); + let domain: crate::types::Domain = >::natural_domain_for_degree( + config.pcs(), n + ); + for seed in [3u64, 12345, 0xdead_beef] { + let zeta: ExtVal = + ExtVal::from_u64(seed).exp_u64(7) + ExtVal::from_u64(seed * 31 + 1); + let sels = domain.selectors_at_point(zeta); + // Textbook Lagrange basis of the last row: + // Π_{i≠n−1} (ζ − g^i)/(g^{n−1} − g^i). + let last = g.exp_u64((n - 1) as u64); + let mut ref_last = ExtVal::ONE; + for i in 0..n - 1 { + let gi = g.exp_u64(i as u64); + ref_last *= (zeta - ExtVal::from(gi)) * ExtVal::from(last - gi).inverse(); + } + let norm = (Val::from_usize(n) * g).inverse(); + assert_eq!( + sels.is_last_row * ExtVal::from(norm), + ref_last, + "last-row normalization, log_n={log_n}" + ); + let mut ref_first = ExtVal::ONE; + for i in 1..n { + let gi = g.exp_u64(i as u64); + ref_first *= (zeta - ExtVal::from(gi)) * ExtVal::from(Val::ONE - gi).inverse(); + } + assert_eq!( + sels.is_first_row * ExtVal::from(Val::from_usize(n).inverse()), + ref_first, + "first-row normalization, log_n={log_n}" + ); + } + } + } + /// Pin: `logup_constraint_values` (the direct evaluation the prover and /// verifier run) computes exactly the values of the constraints /// `synthesize_lookups` specifies, coordinate for coordinate, in order — @@ -718,9 +845,10 @@ mod tests { &s2_cur, &s2_next, &publics, - isf, + // the (normalized) last-row selector value; the + // reference evaluation reads the same value through the view's + // `is_last_row`, so any value pins the identity. isl, - ist, w, d, &mut direct, diff --git a/src/prover.rs b/src/prover.rs index c18993a..6b60ac4 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -31,7 +31,8 @@ //! `acc = Σ (β + fingerprint(γ, claim_i))⁻¹`. //! //! 3. **Stage 2 — Lookup traces**: For each circuit, the lookup traces are computed -//! (running accumulator and message inverses per row) and committed via PCS. Each +//! (one chained partial accumulator per lookup; no message inverses are +//! committed) and committed via PCS. Each //! circuit produces an intermediate accumulator value recording where its running //! sum ended up; these are observed into the challenger, and the verifier will //! check that the last one is zero. @@ -71,7 +72,7 @@ //! - a = max_log_arity — FRI folding arity (log₂) //! //! Derived quantities: -//! - w2_i = 1 + L_i — stage 2 width in extension field elements +//! - w2_i = max(L_i, 1) — stage 2 width in extension field elements //! - W_i = w_i + w2_i · D + q_i · D — total committed width per circuit (base field) //! - H = max_i(n_i) · B — largest LDE height //! - R = ⌈(log₂ H − log_final_poly_len) / a⌉ — FRI folding rounds @@ -616,6 +617,17 @@ where let stage_2_width = circuit.stage_2_width; let preprocessed_width = circuit.preprocessed_width; let mut sels = trace_domain.selectors_on_coset(quotient_domain); + // Normalize the Lagrange selectors to value exactly 1 at their row + // (p3's are unnormalized: L_first(1) = n, L_last(g^{n−1}) = n·g; see + // the selector-normalization pin test). The logUp wrap constraint + // consumes is_last_row ADDITIVELY, so its scale is load-bearing; + // vanishing-form user constraints are unaffected. + let n_val = Val::::from_usize(trace_domain.size()); + let g = Val::::two_adic_generator(log2_strict_usize(trace_domain.size())); + let first_norm = n_val.inverse(); + let last_norm = (n_val * g).inverse(); + sels.is_first_row.iter_mut().for_each(|v| *v *= first_norm); + sels.is_last_row.iter_mut().for_each(|v| *v *= last_norm); let qdb = log2_strict_usize(quotient_domain.size()) - log2_strict_usize(trace_domain.size()); let next_step = 1 << qdb; @@ -752,9 +764,9 @@ where stage_2_cur, stage_2_next, publics_packed, - is_first_row, + // the NORMALIZED last-row selector (scaled in + // `quotient_values` above). is_last_row, - is_transition, ext_w, ext_degree, &mut constraint_values, diff --git a/src/verifier.rs b/src/verifier.rs index b113c37..d004b0f 100644 --- a/src/verifier.rs +++ b/src/verifier.rs @@ -168,7 +168,7 @@ use crate::system::System; use p3_challenger::{CanObserve, FieldChallenger}; use p3_commit::{Pcs, PolynomialSpace}; -use p3_field::{BasedVectorSpace, ExtensionField, Field, PrimeCharacteristicRing}; +use p3_field::{BasedVectorSpace, ExtensionField, Field, PrimeCharacteristicRing, TwoAdicField}; use p3_util::log2_strict_usize; /// Errors that can occur during proof verification. @@ -197,7 +197,10 @@ impl System { &self, claim: &[Val], proof: &Proof, - ) -> Result<(), VerificationError>> { + ) -> Result<(), VerificationError>> + where + Val: TwoAdicField, + { self.verify_multiple_claims(&[claim], proof) } @@ -206,7 +209,10 @@ impl System { &self, claims: &[&[Val]], proof: &Proof, - ) -> Result<(), VerificationError>> { + ) -> Result<(), VerificationError>> + where + Val: TwoAdicField, + { let Proof { active, commitments, @@ -418,7 +424,14 @@ impl System { let quotient_degree = quotient_degrees[pos]; let next_acc = intermediate_accumulators[pos]; let trace_domain = pcs.natural_domain_for_degree(degree); - let sels = trace_domain.selectors_at_point(zeta); + let mut sels = trace_domain.selectors_at_point(zeta); + // Normalize the Lagrange selectors to value exactly 1 at their + // row, mirroring the prover (the logUp wrap constraint consumes + // is_last_row additively). + let n_val = Val::::from_usize(degree); + let g = Val::::two_adic_generator(usize::from(log_degrees[pos])); + sels.is_first_row *= SC::Challenge::from(n_val.inverse()); + sels.is_last_row *= SC::Challenge::from((n_val * g).inverse()); // The four lookup publics (β, γ, acc, next_acc) as base // coordinates embedded into the challenge field. @@ -469,9 +482,8 @@ impl System { view.stage2[0], view.stage2[1], &publics, - view.is_first_row, + // the normalized last-row selector (value 1 at the last row). view.is_last_row, - view.is_transition, crate::system::extension_params::().w, extension_d, &mut constraint_values, From a6f54416bb4560a1f99a1a0f5303a85f7f11c1fd Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 30 Jul 2026 12:17:55 -0300 Subject: [PATCH 2/2] logup: absorb the selector normalization constant into the injection MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The wrap constraint consumes the last-row selector additively, which previously meant rescaling the is_first_row/is_last_row selector vectors over the whole quotient domain, per circuit — two extra full vector passes inside the quotient phase. But the selector only needs its normalized VALUE where it multiplies the boundary injection, and the injected difference is constant across the domain: is_last_norm * delta == is_last_raw * (delta / (n*g)) so the constant is now absorbed into delta once per circuit (two field multiplies) and the selectors stay exactly as p3 provides them — standard unnormalized semantics for user constraints, zero per-point normalization work. logup_constraint_values takes the pre-scaled delta alongside the raw selector; the pin test passes delta raw with an arbitrary selector value, since the identity holds for any scale and the normalization is a caller contract. Constraint values, proofs, and the transcript are unchanged for the logUp argument itself (identical products); user constraints see p3's raw selector values again. 29/29 tests, clippy/fmt clean. --- src/lookup.rs | 52 ++++++++++++++++++++++++++++--------------------- src/prover.rs | 34 +++++++++++++++++++++----------- src/verifier.rs | 18 ++++++++++------- 3 files changed, 64 insertions(+), 40 deletions(-) diff --git a/src/lookup.rs b/src/lookup.rs index 1be1be9..f1ec600 100644 --- a/src/lookup.rs +++ b/src/lookup.rs @@ -143,9 +143,11 @@ fn mul2 + Copy>(a: (A, A), b: (A, A), w: F) -> (A, A) { /// Layout contracts (see the module docs): `publics` holds the 4·d base /// coordinates of (β, γ, acc_initial, acc_final); `stage2` / `stage2_next` /// are the flattened stage-2 base columns, slot `j` the partial accumulator -/// entering lookup `j`'s step. `is_last_row` is the NORMALIZED last-row -/// selector value. `lookups` carries node ids into `node_vals` (multiplicity -/// and args embed in coordinate 0). +/// entering lookup `j`'s step. `is_last_row` is p3's RAW (unnormalized) +/// selector value; `delta_scaled` is `(acc_final − acc_initial)/(n·g)` — the +/// normalization constant pre-absorbed by the caller, valid because Δ is +/// constant across the domain. `lookups` carries node ids into `node_vals` +/// (multiplicity and args embed in coordinate 0). #[allow(clippy::too_many_arguments)] pub fn logup_constraint_values + Copy>( lookups: &[Lookup], @@ -153,6 +155,7 @@ pub fn logup_constraint_values + Copy>( stage2: &[A], stage2_next: &[A], publics: &[A], + delta_scaled: &[A], is_last_row: A, w: F, d: usize, @@ -165,11 +168,11 @@ pub fn logup_constraint_values + Copy>( let nv = |id: crate::graph::NodeId| node_vals[id.index()]; let beta = (publics[0], publics[1]); let gamma = (publics[2], publics[3]); - // The boundary injection: is_last_row·(acc_final − acc_initial). - let inj = ( - is_last_row * (publics[6] - publics[4]), - is_last_row * (publics[7] - publics[5]), - ); + // The boundary injection: the caller supplies Δ with the last-row + // selector's normalization constant pre-absorbed + // (`delta_scaled = (acc_final − acc_initial)/(n·g)`), so the raw + // p3 selector value is used directly. + let inj = (is_last_row * delta_scaled[0], is_last_row * delta_scaled[1]); if lookups.is_empty() { // Pass-through accumulator: acc′ − acc + is_last_row·Δ = 0. @@ -206,14 +209,9 @@ pub fn logup_constraint_values + Copy>( let beta = &publics[..d]; let gamma = &publics[d..2 * d]; - let acc_initial = &publics[2 * d..3 * d]; - let acc_final = &publics[3 * d..4 * d]; - // The boundary injection: is_last_row·(acc_final − acc_initial). - let inj: Vec = acc_final - .iter() - .zip(acc_initial) - .map(|(&f, &i)| is_last_row * (f - i)) - .collect(); + // The boundary injection: Δ arrives with the normalization constant + // pre-absorbed (see the fast path above). + let inj: Vec = delta_scaled.iter().map(|&x| is_last_row * x).collect(); if lookups.is_empty() { for k in 0..d { @@ -297,9 +295,13 @@ pub fn logup_max_degree(graph: &crate::graph::ConstraintGraph) -> u /// ``` /// /// where `acc_0′` is the NEXT row's first slot, `Δ = acc_final − -/// acc_initial` (publics slots 3 and 2), and `is_last_row` is the NORMALIZED -/// last-row Lagrange selector (value exactly 1 on the last row — see the -/// selector-normalization pin test). +/// acc_initial` (publics slots 3 and 2), and `is_last_row·Δ` denotes the +/// NORMALIZED last-row Lagrange selector (value exactly 1 on the last row) +/// times Δ. In the implementation the normalization constant is absorbed +/// into Δ — `is_last_norm·Δ = is_last_raw·(Δ/(n·g))`, valid because Δ is +/// constant across the domain — so the selectors stay exactly as p3 +/// provides them (unnormalized; `L_last(last) = n·g`, pinned by the +/// selector-normalization test). /// /// The wrap step needs no transition selector: on the trace subgroup /// "next row" is rotation by the generator, so the last row's `acc_0′` IS @@ -838,6 +840,14 @@ mod tests { args: l.args.iter().map(|a| fresh(eval_expr(a, &view))).collect(), }) .collect(); + // The reference spec expresses the injection as + // IsLastRow·(acc_final − acc_initial), so the pin passes Δ raw and + // the view's is_last_row value directly — the identity holds for + // any selector value; the normalization constant is a CALLER + // contract (callers pass p3's raw selector with Δ/(n·g)). + let delta: Vec = (0..d) + .map(|k| publics[3 * d + k] - publics[2 * d + k]) + .collect(); let mut direct: Vec = vec![]; logup_constraint_values( &lookup_ids, @@ -845,9 +855,7 @@ mod tests { &s2_cur, &s2_next, &publics, - // the (normalized) last-row selector value; the - // reference evaluation reads the same value through the view's - // `is_last_row`, so any value pins the identity. + &delta, isl, w, d, diff --git a/src/prover.rs b/src/prover.rs index 6b60ac4..7ba4829 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -617,17 +617,15 @@ where let stage_2_width = circuit.stage_2_width; let preprocessed_width = circuit.preprocessed_width; let mut sels = trace_domain.selectors_on_coset(quotient_domain); - // Normalize the Lagrange selectors to value exactly 1 at their row - // (p3's are unnormalized: L_first(1) = n, L_last(g^{n−1}) = n·g; see - // the selector-normalization pin test). The logUp wrap constraint - // consumes is_last_row ADDITIVELY, so its scale is load-bearing; - // vanishing-form user constraints are unaffected. + // The logUp wrap constraint consumes the last-row selector ADDITIVELY, + // so its normalization matters — but the selector multiplies Δ, which + // is constant across the domain, so the normalization constant + // 1/(n·g) is absorbed into Δ once per circuit instead of rescaling + // the selector vectors (p3's unnormalized L_last has value n·g at the + // last row; see the selector-normalization pin test). let n_val = Val::::from_usize(trace_domain.size()); let g = Val::::two_adic_generator(log2_strict_usize(trace_domain.size())); - let first_norm = n_val.inverse(); - let last_norm = (n_val * g).inverse(); - sels.is_first_row.iter_mut().for_each(|v| *v *= first_norm); - sels.is_last_row.iter_mut().for_each(|v| *v *= last_norm); + let inj_norm = (n_val * g).inverse(); let qdb = log2_strict_usize(quotient_domain.size()) - log2_strict_usize(trace_domain.size()); let next_step = 1 << qdb; @@ -659,6 +657,17 @@ where .map(|&c| PackedVal::::from(c)) .collect(); + // Δ/(n·g) per coordinate, broadcast: the logUp boundary injection with + // the last-row selector's normalization constant pre-absorbed. + let ext_d = >>::DIMENSION; + let delta_scaled: Vec> = (0..ext_d) + .map(|k| { + PackedVal::::from( + (lookup_publics[3 * ext_d + k] - lookup_publics[2 * ext_d + k]) * inj_norm, + ) + }) + .collect(); + let ext_params = crate::system::extension_params::(); let inner = |i_start: usize| { quotient_values_inner::( @@ -672,6 +681,7 @@ where stage_2_width, preprocessed_width, &publics_packed, + &delta_scaled, &decomposed_alpha_powers, next_step, i_start, @@ -708,6 +718,7 @@ fn quotient_values_inner( stage_2_width: usize, preprocessed_width: usize, publics_packed: &[PackedVal], + delta_scaled: &[PackedVal], decomposed_alpha_powers: &[Vec>], next_step: usize, i_start: usize, @@ -764,8 +775,9 @@ where stage_2_cur, stage_2_next, publics_packed, - // the NORMALIZED last-row selector (scaled in - // `quotient_values` above). + delta_scaled, + // p3's (unnormalized) last-row selector; the normalization + // constant is pre-absorbed into `delta_scaled`. is_last_row, ext_w, ext_degree, diff --git a/src/verifier.rs b/src/verifier.rs index d004b0f..e80ed0a 100644 --- a/src/verifier.rs +++ b/src/verifier.rs @@ -424,14 +424,13 @@ impl System { let quotient_degree = quotient_degrees[pos]; let next_acc = intermediate_accumulators[pos]; let trace_domain = pcs.natural_domain_for_degree(degree); - let mut sels = trace_domain.selectors_at_point(zeta); - // Normalize the Lagrange selectors to value exactly 1 at their - // row, mirroring the prover (the logUp wrap constraint consumes - // is_last_row additively). + let sels = trace_domain.selectors_at_point(zeta); + // The logUp boundary injection absorbs the last-row selector's + // normalization constant into Δ (mirroring the prover): p3's + // unnormalized L_last has value n·g at the last row. let n_val = Val::::from_usize(degree); let g = Val::::two_adic_generator(usize::from(log_degrees[pos])); - sels.is_first_row *= SC::Challenge::from(n_val.inverse()); - sels.is_last_row *= SC::Challenge::from((n_val * g).inverse()); + let inj_norm = SC::Challenge::from((n_val * g).inverse()); // The four lookup publics (β, γ, acc, next_acc) as base // coordinates embedded into the challenge field. @@ -476,13 +475,18 @@ impl System { let mut buf = Vec::new(); circuit.graph.sweep(&view, &mut buf); let mut constraint_values = circuit.graph.constraint_values(&buf); + let delta_scaled: Vec = (0..extension_d) + .map(|k| (publics[3 * extension_d + k] - publics[2 * extension_d + k]) * inj_norm) + .collect(); crate::lookup::logup_constraint_values( &circuit.graph.lookups, &buf, view.stage2[0], view.stage2[1], &publics, - // the normalized last-row selector (value 1 at the last row). + &delta_scaled, + // p3's (unnormalized) last-row selector; the normalization + // constant is pre-absorbed into `delta_scaled`. view.is_last_row, crate::system::extension_params::().w, extension_d,