diff --git a/crates/flock/src/zerocheck/ntt/inv_table.rs b/crates/flock/src/zerocheck/ntt/inv_table.rs index 625992c2f..8d678db42 100644 --- a/crates/flock/src/zerocheck/ntt/inv_table.rs +++ b/crates/flock/src/zerocheck/ntt/inv_table.rs @@ -21,7 +21,7 @@ use super::AdditiveNttGf8; #[cfg(all(target_arch = "x86_64", target_feature = "avx2"))] use core::arch::x86_64::*; -use primitives::field::F8; +use primitives::field::{F8, F64, F192, phi8_192}; #[derive(Clone, Debug)] pub(crate) struct InvNttTableByteSingleGf8 { @@ -31,6 +31,9 @@ pub(crate) struct InvNttTableByteSingleGf8 { /// `data[w * ell .. (w+1) * ell]` = T_0[w], the XOR-sum of columns of `M` /// indexed by the set bits of `w`. data: Vec, + /// The same S/Λ butterflies, lifted through φ₈ into the base field, for + /// extending the reduced E-valued C vector without Boolean bit planes. + twiddles: Vec, } impl InvNttTableByteSingleGf8 { @@ -80,7 +83,67 @@ impl InvNttTableByteSingleGf8 { } } - Self { k, ell, n_chunks, data } + Self { + k, + ell, + n_chunks, + data, + twiddles: ntt_s + .twiddles + .iter() + .chain(&ntt_l.twiddles) + .map(|&t| F64(phi8_192(t).c0)) + .collect(), + } + } + + /// Extend E-valued evaluations from S to Λ in place. The GF8 embedding + /// lies in K, so each butterfly multiplies the three E limbs by one K + /// twiddle. These are the original GF8 domains and LCH basis, not the + /// polynomial-basis domains of the GF64 NTT. + pub(crate) fn extend_lifted(&self, v: &mut [F192]) { + assert_eq!(v.len(), self.ell); + let (twiddles_s, twiddles_l) = self.twiddles.split_at(self.ell - 1); + + // Inverse on S: children before parents in the twiddle tree. + for level in (0..self.k).rev() { + let nodes = 1usize << level; + let size = self.ell >> level; + let twiddles = &twiddles_s[nodes - 1..2 * nodes - 1]; + for (block, &lambda) in v.chunks_exact_mut(size).zip(twiddles) { + let (lo, hi) = block.split_at_mut(size / 2); + if lambda == F64::ZERO { + for (a, b) in lo.iter().zip(hi) { + *b += *a; + } + } else { + for (a, b) in lo.iter_mut().zip(hi) { + *b += *a; + *a += b.mul_base(lambda); + } + } + } + } + + // Forward on Λ: parents before children, with the same point order. + for level in 0..self.k { + let nodes = 1usize << level; + let size = self.ell >> level; + let twiddles = &twiddles_l[nodes - 1..2 * nodes - 1]; + for (block, &lambda) in v.chunks_exact_mut(size).zip(twiddles) { + let (lo, hi) = block.split_at_mut(size / 2); + if lambda == F64::ZERO { + for (a, b) in lo.iter().zip(hi) { + *b += *a; + } + } else { + for (a, b) in lo.iter_mut().zip(hi) { + *a += b.mul_base(lambda); + *b += *a; + } + } + } + } } /// Raw pointer to the table data (`256 × ell` bytes, row-major). Used by diff --git a/crates/flock/src/zerocheck/round1.rs b/crates/flock/src/zerocheck/round1.rs index 777ef0729..578008b1b 100644 --- a/crates/flock/src/zerocheck/round1.rs +++ b/crates/flock/src/zerocheck/round1.rs @@ -164,54 +164,13 @@ fn d_inv() -> F192 { /// Most high variables of a split eq table capped on its high side: few high weights keep the outer products cheap. pub(crate) const EQ_HIGH_VARS: usize = 7; -/// Extend a length-`ell` F192 vector from the input domain S to the extension -/// domain Λ using bit-plane decomposition: for each of the 192 bit positions -/// of F192, run the bit-input NTT (`inv_NTT_S` then `fwd_NTT_Λ` via the -/// precomputed table) on that bit-plane, scale by γ^b, and accumulate. -/// -/// Ports `ntt_extend_vec` (scalar form). The NTT is F_2-linear and -/// φ_8 commutes with that linearity, which is what makes the bit-by-bit -/// decomposition equal to the direct F_8-valued NTT extension. +/// Extend a length-`ell` F192 vector from S to Λ with the original GF8 +/// butterflies lifted through φ₈. Only the returned vector is allocated; +/// the Boolean A/B lookup table remains the bulk-row path. pub(crate) fn ntt_extend_vec(in_s: &[F192], inv_table: &InvNttTableByteSingleGf8) -> Vec { - let ell = inv_table.ell; - assert_eq!(in_s.len(), ell); - assert_eq!(ell, 1usize << inv_table.k); - - let mut out = vec![F192::ZERO; ell]; - let n_chunks = inv_table.n_chunks; - - let mut input_bits = vec![0u8; n_chunks]; - let mut out_bytes = vec![F8::ZERO; ell]; - - for b in 0..192 { - // Pack bit b of each in_s[z] into z-indexed LSB-first byte form. - input_bits.iter_mut().for_each(|x| *x = 0); - for z in 0..ell { - let bit = match b / 64 { - 0 => (in_s[z].c0 >> b) & 1, - 1 => (in_s[z].c1 >> (b - 64)) & 1, - 2 => (in_s[z].c2 >> (b - 128)) & 1, - _ => unreachable!(), - }; - if bit != 0 { - input_bits[z / 8] |= 1u8 << (z % 8); - } - } - - // Bit-input NTT. - inv_table.apply(&input_bits, &mut out_bytes); - - let basis = match b / 64 { - 0 => F192::new(1u64 << b, 0, 0), - 1 => F192::new(0, 1u64 << (b - 64), 0), - 2 => F192::new(0, 0, 1u64 << (b - 128)), - _ => unreachable!(), - }; - for lambda in 0..ell { - out[lambda] += basis * phi8_192(out_bytes[lambda]); - } - } - + assert_eq!(in_s.len(), inv_table.ell); + let mut out = in_s.to_vec(); + inv_table.extend_lifted(&mut out); out } @@ -1193,6 +1152,86 @@ pub(crate) mod tests { use primitives::multilinear::eq_table; use primitives::test_util::Rng; + /// Direct monomial Lagrange interpolation, independent of the NTT + /// recurrence, its LCH basis, and the collapsed Boolean lookup table. + fn lagrange_extension_matrix(k: usize, beta_s: F8, beta_l: F8) -> Vec> { + let ell = 1usize << k; + let s: Vec = (0..ell).map(|j| beta_s + F8(j as u8)).collect(); + let denominators: Vec = s + .iter() + .enumerate() + .map(|(j, &s_j)| { + s.iter() + .enumerate() + .filter(|&(h, _)| h != j) + .fold(F8::ONE, |acc, (_, &s_h)| acc * (s_j + s_h)) + .inv() + }) + .collect(); + (0..ell) + .map(|i| { + let x = beta_l + F8(i as u8); + let numerator = s.iter().fold(F8::ONE, |acc, &s_h| acc * (x + s_h)); + s.iter() + .zip(&denominators) + .map(|(&s_j, &denominator)| phi8_192(numerator * (x + s_j).inv() * denominator)) + .collect() + }) + .collect() + } + + #[test] + fn lifted_extension_matches_lagrange_arbitrary_e() { + let mut rng = Rng::new(0x0011_f7ed); + // All supported table sizes, including the byte-packing boundary and + // the two halves of the full GF8 domain. Reversing/offsetting the + // cosets also checks that we lift the supplied transforms' twiddles. + for k in 3..=7 { + for beta_s in [F8::ZERO, F8(0xff)] { + let beta_l = beta_s + F8(1u8 << k); + let ntt_s = AdditiveNttGf8::new(k, beta_s); + let ntt_l = AdditiveNttGf8::new(k, beta_l); + let table = InvNttTableByteSingleGf8::new(&ntt_s, &ntt_l); + let matrix = lagrange_extension_matrix(k, beta_s, beta_l); + for _ in 0..4 { + let input = rng.ext_vec(1 << k); + let expected: Vec = matrix + .iter() + .map(|row| { + row.iter() + .zip(&input) + .fold(F192::ZERO, |acc, (&weight, &value)| acc + weight * value) + }) + .collect(); + assert_eq!(ntt_extend_vec(&input, &table), expected, "k={k}, beta_s={beta_s:?}"); + } + } + } + } + + #[test] + fn lifted_extension_preserves_tower_basis() { + for k in 3..=7 { + let ell = 1usize << k; + let ntt_s = AdditiveNttGf8::new(k, F8::ZERO); + let ntt_l = AdditiveNttGf8::new(k, F8(ell as u8)); + let table = InvNttTableByteSingleGf8::new(&ntt_s, &ntt_l); + let matrix = lagrange_extension_matrix(k, F8::ZERO, F8(ell as u8)); + // Each of the 192 tower-coordinate bits, including both limb + // boundaries, and every evaluation position at each supported size. + for bit in 0..192 { + let mut limbs = [0u64; 3]; + limbs[bit / 64] = 1u64 << (bit % 64); + let basis = F192::new(limbs[0], limbs[1], limbs[2]); + let position = bit % ell; + let mut input = vec![F192::ZERO; ell]; + input[position] = basis; + let expected: Vec = matrix.iter().map(|row| basis * row[position]).collect(); + assert_eq!(ntt_extend_vec(&input, &table), expected, "k={k}, bit={bit}"); + } + } + } + /// Compute the round-1 prover message naively (no shift-reduce, no fused /// inner, no deferred reduction: direct algorithmic translation of the /// protocol formula). diff --git a/crates/pcs/src/ntt/additive_ntt_f64.rs b/crates/pcs/src/ntt/additive_ntt_f64.rs index e2e1f657b..275c908f4 100644 --- a/crates/pcs/src/ntt/additive_ntt_f64.rs +++ b/crates/pcs/src/ntt/additive_ntt_f64.rs @@ -873,6 +873,18 @@ fn butterfly_one(u: &mut F64, v: &mut F64, t: F64) { #[inline] fn lane_butterflies(top: &mut [F64], bot: &mut [F64], twiddle: F64) { debug_assert_eq!(top.len(), bot.len()); + if twiddle == F64::ZERO { + if TRANSPOSED { + for (u, v) in top.iter_mut().zip(bot) { + *u += *v; + } + } else { + for (u, v) in top.iter().zip(bot) { + *v += *u; + } + } + return; + } #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))] let done = { let vectors = top.len() / 8; diff --git a/crates/pcs/src/whir/induce.rs b/crates/pcs/src/whir/induce.rs index 6bb42e902..6bf912c7d 100644 --- a/crates/pcs/src/whir/induce.rs +++ b/crates/pcs/src/whir/induce.rs @@ -301,17 +301,6 @@ fn transposed_butterflies(t: F64, top: &mut [F192], bot: &mut [F192]) { transposed_butterfly_lanes(top, bot, t); } -/// Transposed forward additive NTT, `F^T`, in place over `2^log_d` E-values -/// with K-twiddles. Forward butterfly is `M = [[1, t], [1, t+1]]`; transpose -/// `M^T = [[1, 1], [t, t+1]]` is `s = a + b; top = s; bot = t*s + b` (here -/// `s.mul_base(t) + b`), applied in reverse layer order. Mirror of -/// `whir::transpose_forward_ntt` (one parallel sweep per layer). -fn transpose_forward_ntt_ext(ntt: &AdditiveNttF64, data: &mut [F192], log_d: usize) { - debug_assert_eq!(data.len(), 1usize << log_d); - debug_assert!(log_d <= ntt.log_domain_size()); - transpose_layers_ext(ntt, data, log_d, (0..log_d).rev()); -} - /// Elements per cache-resident window of the layer-blocked run below. const TRANSPOSE_CHUNK: usize = 1 << 16; @@ -364,13 +353,12 @@ fn transpose_layers_ext_windowed( }); } let rest = &layers[if blocked > 1 { blocked } else { 0 }..]; - // The layers left are those whose blocks exceed a window: the lowest ones, 2^g blocks or fewer. - // - // When they are exactly g - 1 .. 0, rows `r + i * 2^(d - g)` for i < 2^g pair only with each other. - // So one gathered pass runs them all, instead of one sweep each. + // Gather a contiguous suffix even when pruning stops above layer zero. + // Each of its 2^low outer blocks is independent; gather within that block. let g = rest.len(); - if (1..=GATHER_LOG).contains(&g) && rest.iter().copied().eq((0..g).rev()) { - transpose_low_layers_gathered(ntt, data, log_d, g); + let low = rest.last().copied().unwrap_or(0); + if (1..=GATHER_LOG).contains(&g) && rest.iter().copied().eq((low..low + g).rev()) { + transpose_low_layers_gathered(ntt, data, log_d, low, g); return; } for &layer in rest { @@ -402,30 +390,21 @@ const GATHER_LOG: usize = 6; /// Residues one gathered task takes: 32 residues of 64 rows is 48 KiB, which stays in L2. const GATHER_RESIDUES: usize = 32; -/// The transposed butterflies of layers `g - 1 .. 0`, in one pass over the data. -/// -/// # Algorithm -/// -/// With `step = 2^(d - g)`, layer `l < g` pairs rows `step * 2^(g - 1 - l)` apart. -/// -/// So the rows `r + i * step`, for `i < 2^g`, pair only with each other: -/// -/// ```text -/// d = 22, g = 6, step = 2^16: -/// -/// rows r, r + 2^16, r + 2 * 2^16, ..., r + 63 * 2^16 one group, for each r < 2^16 -/// ``` -/// -/// Row `r + i * step` sits in block `i >> (g - l)` of layer `l`, whatever `r`: its twiddle depends on `i` alone. +/// The transposed butterflies of layers `low + g - 1 .. low`, in one gathered pass. /// -/// A task gathers the groups of consecutive residues, runs every layer on them in cache, and scatters them back. -fn transpose_low_layers_gathered(ntt: &AdditiveNttF64, data: &mut [F192], log_d: usize, g: usize) { +/// The `2^low` outer blocks are independent. Within each, rows `r + i * step` +/// for `i < 2^g` pair only with each other, where `step = 2^(d - low - g)`. +/// A task gathers consecutive residues, runs every layer in cache, and scatters +/// them back. Its twiddles include the outer block's offset in the full domain. +fn transpose_low_layers_gathered(ntt: &AdditiveNttF64, data: &mut [F192], log_d: usize, low: usize, g: usize) { let rows = 1usize << g; - let step = 1usize << (log_d - g); + let step = 1usize << (log_d - low - g); let per_task = GATHER_RESIDUES.min(step); let base = SendPtr(data.as_mut_ptr()); - parallel::for_each(step / per_task, |task| { - let r0 = task * per_task; + let tasks_per_block = step / per_task; + parallel::for_each((1usize << low) * tasks_per_block, |task| { + let outer = task / tasks_per_block; + let r0 = outer * (1usize << (log_d - low)) + (task % tasks_per_block) * per_task; // Scratch index `i * per_task + j` holds row `r0 + j + i * step`. let mut scratch = [F192::ZERO; GATHER_RESIDUES << GATHER_LOG]; let scratch = &mut scratch[..rows * per_task]; @@ -436,11 +415,11 @@ fn transpose_low_layers_gathered(ntt: &AdditiveNttF64, data: &mut [F192], log_d: dst.copy_from_slice(unsafe { base.slice(r0 + i * step, per_task) }); } - // Layers g - 1 .. 0, each a butterfly between group rows `half` apart. + // Relative layers g - 1 .. 0 pair group rows `half` apart. for layer in (0..g).rev() { let half = 1usize << (g - 1 - layer); for block in 0..1usize << layer { - let t = ntt.twiddle(layer, block); + let t = ntt.twiddle(low + layer, (outer << layer) + block); let at = block * 2 * half * per_task; let (top, bot) = scratch[at..at + 2 * half * per_task].split_at_mut(half * per_task); transposed_butterflies(t, top, bot); @@ -455,19 +434,40 @@ fn transpose_low_layers_gathered(ntt: &AdditiveNttF64, data: &mut [F192], log_d: }); } -/// Sparse-prefix variant of [`transpose_forward_ntt_ext`]: the input has only -/// `positions.len()` nonzeros and the first `k` transpose steps (forward -/// layers `log_d-1 .. log_d-k`, pairing distances `1 .. 2^(k-1)`) mix only -/// WITHIN `2^k`-aligned windows. We process just the windows that contain a -/// nonzero (a dense `2^k` transpose each, disjoint so window-parallel), -/// densify, then run the remaining steps as full dense sweeps. Output is -/// identical to `transpose_forward_ntt_ext` on the scattered input. Mirror -/// of `whir::transpose_forward_ntt_sparse`. +/// XOR the `2^log_inv_rate` blocks into the retained first block. +/// +/// In the omitted transpose layers every retained output follows only top +/// butterfly outputs, `a + b`. Thus the suffix needs `N - n` E additions and +/// no E-by-K products, instead of `r*N` additions and `r*N/2` products. +fn fold_transpose_blocks(data: &mut [F192], log_inv_rate: usize) { + if log_inv_rate == 0 { + return; + } + let n = data.len() >> log_inv_rate; + let (retained, rest) = data.split_at_mut(n); + let chunk_len = parallel::recommended_chunk_size(n); + parallel::chunks_mut(retained, chunk_len, |chunk, out| { + let start = chunk * chunk_len; + for block in rest.chunks_exact(n) { + for (out, &value) in out.iter_mut().zip(&block[start..]) { + *out += value; + } + } + }); +} + +/// Sparse-prefix transposed forward additive NTT, retaining only the first +/// `2^(log_d - log_inv_rate)` outputs. The first `k` transpose steps mix only +/// within `2^k`-aligned windows, so only occupied windows are processed. +/// After densifying, run the surviving layers down through `log_inv_rate`, +/// then fold blocks in place instead of computing the discarded outputs. +/// The caller truncates the vector; the remaining entries are unspecified. fn transpose_forward_ntt_sparse_ext( ntt: &AdditiveNttF64, positions: &[usize], values: &[F192], log_d: usize, + log_inv_rate: usize, ) -> Vec { let _span = tracing::info_span!( "NTT", @@ -477,18 +477,19 @@ fn transpose_forward_ntt_sparse_ext( ) .entered(); + debug_assert!(log_inv_rate <= log_d); let n = 1usize << log_d; - // No prefix for small domains: just scatter + full dense transpose. + // Keep the existing window allocation, but stop its layers before the fold. let k = if log_d >= 12 { 8usize.min(log_d) } else { 0 }; + let prefix_steps = k.min(log_d - log_inv_rate); if k == 0 { let mut data = vec![F192::ZERO; n]; for (&p, &v) in positions.iter().zip(values) { data[p] += v; } - if log_d > 0 { - transpose_forward_ntt_ext(ntt, &mut data, log_d); - } + transpose_layers_ext(ntt, &mut data, log_d, (log_inv_rate..log_d).rev()); + fold_transpose_blocks(&mut data, log_inv_rate); return data; } @@ -500,12 +501,12 @@ fn transpose_forward_ntt_sparse_ext( buf[p & wmask] += v; } - // Steps s = 0..k-1 within each active window, in parallel (windows disjoint). + // Surviving prefix steps within each active window, in parallel (windows disjoint). let mut win_vec: Vec<(usize, Vec)> = windows.into_iter().collect(); parallel::chunks_mut(&mut win_vec, 1, |_, win| { let (w, buf) = &mut win[0]; let w = *w; - for s in 0..k { + for s in 0..prefix_steps { let layer = log_d - 1 - s; let bsh = 1usize << s; // pairing distance let block_size = bsh << 1; @@ -520,14 +521,15 @@ fn transpose_forward_ntt_sparse_ext( }); // Densify (active windows only; the rest stay zero, which is the correct - // post-step-(k-1) state for an all-zero window). + // post-prefix state for an all-zero window). let mut data = vec![F192::ZERO; n]; for (w, buf) in &win_vec { data[(w << k)..((w + 1) << k)].copy_from_slice(buf); } - // Remaining steps s = k..log_d-1 = forward layers (log_d-1-k) .. 0, dense. - transpose_layers_ext(ntt, &mut data, log_d, (0..(log_d - k)).rev()); + // Dense continuation stops before the layers replaced by the block fold. + transpose_layers_ext(ntt, &mut data, log_d, (log_inv_rate..(log_d - prefix_steps)).rev()); + fold_transpose_blocks(&mut data, log_inv_rate); data } @@ -566,7 +568,7 @@ pub(crate) fn induce_sumcheck_poly_via_ntt_base( c } else { let ntt = AdditiveNttF64::standard(log_block); - transpose_forward_ntt_sparse_ext(&ntt, queries, weights, log_block) + transpose_forward_ntt_sparse_ext(&ntt, queries, weights, log_block, log_inv_rate) }; coeffs.truncate(n); (coeffs, enforced_sum) @@ -613,17 +615,15 @@ mod tests { fn blocked_and_gathered_transposes_match_layer_by_layer() { // Invariant: the windowed prefix and the gathered tail compute the plain transposed NTT. let mut rng = Rng::new(0x7A55); - // Fixture state: a window of 2^(d - 6) elements leaves layers 5 .. 0 for the gathered pass. - // - // d = 12: step 2^6, 32 residues a task - // d = 8: step 2^2, 4 residues a task - for log_d in [12, 8] { + // Leave at most six surviving layers for gathering, including nonzero + // lower bounds, multiple outer blocks, and fewer than 32 residues. + for (log_d, low) in [(12, 0), (12, 1), (12, 3), (12, 6), (8, 0), (8, 2), (8, 7)] { let ntt = AdditiveNttF64::standard(log_d); let data: Vec = rng.ext_vec(1 << log_d); // Reference: one layer at a time, highest first, every block's butterflies in place. let mut want = data.clone(); - for layer in (0..log_d).rev() { + for layer in (low..log_d).rev() { let half = 1usize << (log_d - 1 - layer); for (block, chunk) in want.chunks_mut(2 * half).enumerate() { let t = ntt.twiddle(layer, block); @@ -636,8 +636,9 @@ mod tests { } let mut got = data; - transpose_layers_ext_windowed(&ntt, &mut got, log_d, (0..log_d).rev(), 1 << (log_d - 6)); - assert_eq!(got, want, "log_d={log_d}"); + let gathered = GATHER_LOG.min(log_d - low); + transpose_layers_ext_windowed(&ntt, &mut got, log_d, (low..log_d).rev(), 1 << (log_d - low - gathered)); + assert_eq!(got, want, "log_d={log_d}, low={low}"); } } } diff --git a/crates/pcs/src/whir/tests.rs b/crates/pcs/src/whir/tests.rs index 02664aada..2697fa41d 100644 --- a/crates/pcs/src/whir/tests.rs +++ b/crates/pcs/src/whir/tests.rs @@ -297,19 +297,41 @@ fn truncated_lanes_match_an_explicit_zero_tail() { } } -/// The sparse transposed-NTT induce must be byte-identical to the dense -/// LCH-expansion induce (same guarantee the original pins). Covers both -/// the windowed sparse-prefix path (log_block >= 12, k = 8) and the -/// scatter + full-dense-transpose path (log_block < 12, k = 0). +/// The pruned transposed NTT must match dense LCH expansion, including zero +/// rate, a rate overlapping or exhausting the sparse prefix, empty inputs, +/// and repeated queries accumulated in transcript order. #[test] fn induce_via_ntt_matches_dense() { let mut rng = Rng::new(9); - for (log_msg_cols, log_inv_rate, lanes_log, n_queries) in [(12usize, 1usize, 5usize, 130usize), (6, 2, 3, 40)] { + for (log_msg_cols, log_inv_rate, lanes_log, n_queries) in [ + (12usize, 1usize, 5usize, 130usize), + (6, 2, 3, 40), + (6, 0, 2, 16), + (12, 0, 1, 16), + (8, 4, 1, 16), + (5, 7, 1, 16), + (1, 11, 1, 16), + (0, 12, 0, 16), + (0, 0, 0, 1), + (0, 1, 0, 2), + (6, 2, 1, 0), + (5, 7, 1, 0), + (12, 1, 1, 0), + ] { let block_len = 1usize << (log_msg_cols + log_inv_rate); let lanes = 1usize << lanes_log; - // Distinct sorted query positions plus one aligned random row each. + // Include both domain endpoints, then append repeats after the + // sorted distinct queries to cover accumulation across sparse windows. let mut qs: Vec = Vec::new(); let mut seen = HashSet::new(); + if n_queries > 0 { + qs.push(0); + seen.insert(0); + } + if n_queries > 1 { + qs.push(block_len - 1); + seen.insert(block_len - 1); + } while qs.len() < n_queries { let q = (rng.next_u64() as usize) % block_len; if seen.insert(q) { @@ -317,6 +339,11 @@ fn induce_via_ntt_matches_dense() { } } qs.sort_unstable(); + if let Some(&first) = qs.first() { + qs.push(first); + qs.push(first); + } + let n_queries = qs.len(); let rows: Vec> = (0..n_queries) .map(|_| (0..lanes).map(|_| F64(rng.next_u64())).collect()) .collect(); @@ -327,8 +354,14 @@ fn induce_via_ntt_matches_dense() { let dense = induce_sumcheck_poly(log_msg_cols, &sks_vks, &rows, &v_challenges, &qs, &weights); let via_ntt = induce_sumcheck_poly_via_ntt_base(log_msg_cols, log_inv_rate, &rows, &v_challenges, &qs, &weights); - assert_eq!(dense.1, via_ntt.1, "enforced_sum mismatch"); - assert_eq!(&*dense.0, &*via_ntt.0, "basis_poly mismatch"); + assert_eq!( + dense.1, via_ntt.1, + "enforced_sum mismatch: cols={log_msg_cols}, rate={log_inv_rate}" + ); + assert_eq!( + &*dense.0, &*via_ntt.0, + "basis_poly mismatch: cols={log_msg_cols}, rate={log_inv_rate}, queries={n_queries}" + ); } } diff --git a/doc/leanvm/body/c-flock-protocol.tex b/doc/leanvm/body/c-flock-protocol.tex index 4ced568ba..e8d003a28 100644 --- a/doc/leanvm/body/c-flock-protocol.tex +++ b/doc/leanvm/body/c-flock-protocol.tex @@ -61,6 +61,8 @@ \subsection{Zerocheck}\label{flock:zerocheck} \end{equation} which lies in $\E[Y]$ and has degree at most $126$, the product contributing $2\times 63$ and the linear term $63$. If \eqref{flock:eq:r1cs} holds, then $P(h)=0$ for every $h\in\skipdom$. The prover sends $P|_{\skipcoset}$, $64$ values: together with the $64$ assumed zeros on $\skipdom$ that is a degree-below-$128$ polynomial's worth of evaluations, so the verifier interpolates $P$ over the $128$-point space $\skipdom\cup\skipcoset$. +The prover can extend the linear term from $\skipdom$ to $\skipcoset$ after reducing its other coordinates: apply the inverse additive NTT on $\skipdom$, then the forward additive NTT on $\skipcoset$, directly to the resulting $\E$-valued vector. The embedding $\fembed(\F_{2^8})$ lies in $\K\subset\E$, so the original small-field twiddles lift to $\K$ and each butterfly scales the three $\K$ limbs independently. This computes the same linear map as extending every Boolean coordinate plane separately, without that decomposition or general $\E$ multiplications. The input and output domains remain the embedded byte-basis domains above, not the polynomial-basis domains of the $\K$ NTT. + The verifier then samples $\zskip\in\E$ and reconstructs the claimed value \[ v_P \qeq P(\zskip). diff --git a/doc/leanvm/body/d-novel-basis.tex b/doc/leanvm/body/d-novel-basis.tex index 956bb4bbc..930d0d9a5 100644 --- a/doc/leanvm/body/d-novel-basis.tex +++ b/doc/leanvm/body/d-novel-basis.tex @@ -92,6 +92,8 @@ \subsection{The additive NTT}\label{sec:ntt} For $\ell \in \cube{d}$ let $\mpoly^{(d)}_{\ell} := \sum_{j < 2^{\kappa-d}} a_{\langle \ell \rangle + 2^d j} \novel^{(d)}_j$ collect the coefficients congruent to $\langle \ell \rangle$ modulo $2^d$. Downward induction on $d$ maintains the invariant that after stages $\kappa-1, \dots, d$, $\ \bfarr(v) = \mpoly^{(d)}_{(v_0,\dots,v_{d-1})}\bigl(\Wn{d}(x_v)\bigr)$, where by linearity $\Wn{d}(x_v) = v_d + t$ with $t$ the twiddle of the algorithm (coordinates $c < d$ lie in $\ker \Wn{d} = \subsp_d$, and $\Wn{d}(e_d) = 1$). The base $d = \kappa$ is the tiled initialization. For the step, let $\ell := (v_0, \dots, v_{d-1})$: the order-$(d{+}1)$ even and odd parts of $\mpoly^{(d)}_{\ell}$ are $\mpoly^{(d+1)}_{(\ell,0)}$ and $\mpoly^{(d+1)}_{(\ell,1)}$ (as $\langle \ell \rangle + 2^d(2j+\iota) = \langle (\ell,\iota) \rangle + 2^{d+1} j$), whose values at $\Wn{d+1}(x_v) = \Wn{d+1}(x_{v'})$ are the pre-stage entries $\bfarr(v)$ and $\bfarr(v')$; Lemma~\ref{lem:evenodd} at the fiber $\{t, t+1\}$ of $\ntmap_d$ over this point (Lemma~\ref{lem:chain}) gives $\mpoly^{(d)}_{\ell}(t) = \bfarr(v) + t\,\bfarr(v')$ and $\mpoly^{(d)}_{\ell}(t+1) = \mpoly^{(d)}_{\ell}(t) + \bfarr(v')$, exactly the butterfly. At $d = 0$, $\bfarr(v) = \mpoly(x_v)$. Each of the $\kappa$ stages does $\blen/2$ butterflies of one multiplication and two additions. \end{proof} +\paragraph{Implementation shortcuts.} A zero twiddle reduces a forward butterfly to its second addition, and a transposed butterfly to its first addition; neither needs a field multiplication. For the transpose of $\Enc_{\kappa,\rexp}$, reverse the $\kappa$ butterfly stages and then transpose the tiled initialization by summing its $2^\rexp$ blocks coordinate-wise. This final fold costs $\blen-2^\kappa$ additions and no multiplications. Equivalently, when starting from a full transform transpose and retaining only the first $2^\kappa$ outputs, the last $\rexp$ stages need only their top outputs, so their discarded products need not be computed. These shortcuts preserve the evaluation order and the column weights below. + \subsection{Column weights}\label{sec:ntt-weights} A codeword coordinate is a linear combination of the message coefficients. The following factorization lets the PCS verifier evaluate that combination's multilinear weight without running a transform.