From 81f47f26e40ff94efac38c41818bd2e5586d0d9f Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 16 Jul 2026 12:12:22 -0300 Subject: [PATCH 1/3] fix(stark): review nits for forward-accumulation OOD pruning MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - lookup.rs: fix the logup_single_source_tests module doc — after forward accumulation the 2-absorbed branch no longer reads next-row aux(1, ·) cells; describe it by what it actually does (folds two absorbed interactions, degree 3). - ood.rs: reword the module doc so the offset illustration is not pinned to [0, 1] — offset 0 is the current-row block, every later offset contributes a next-row block (generic over transition_offsets.len()). - verifier.rs: use num_eval_points.saturating_sub(step_size) to match the shared ood.rs helper (defensive consistency; underflow unreachable). - ood.rs: harden build_pruned_trace_term_coeffs — drop the per-slot `if p < powers.len()` guards and promote the trailing power-count check from debug_assert_eq! to a hard assert_eq!. Both operands are pure functions of AIR metadata (invariant I3), never proof-controlled, so a mismatch is a programmer bug that must not be masked in release builds. --- crypto/stark/src/lookup.rs | 2 +- crypto/stark/src/ood.rs | 50 ++++++++++++++++++++++++------------ crypto/stark/src/verifier.rs | 2 +- 3 files changed, 36 insertions(+), 18 deletions(-) diff --git a/crypto/stark/src/lookup.rs b/crypto/stark/src/lookup.rs index cb498baf1..4a684b8df 100644 --- a/crypto/stark/src/lookup.rs +++ b/crypto/stark/src/lookup.rs @@ -2346,7 +2346,7 @@ mod logup_single_source_tests { //! (verifier) — all bit-for-bit. //! //! Coverage: the accumulated constraint's 1-absorbed AND 2-absorbed branches - //! (the latter reads `aux(1, ·)` next-row cells), the batched-term + //! (the latter folds two absorbed interactions, degree 3), the batched-term //! constraint, and every [`Packing`] variant's fingerprint contribution. use super::*; use crate::constraint_ir::{eval_program, eval_program_verifier}; diff --git a/crypto/stark/src/ood.rs b/crypto/stark/src/ood.rs index 3572836a2..322a099fb 100644 --- a/crypto/stark/src/ood.rs +++ b/crypto/stark/src/ood.rs @@ -1,11 +1,12 @@ //! Shared, prover = verifier-identical helpers for out-of-domain (OOD) trace //! opening pruning. //! -//! The frame OOD table has `num_offsets * step_size` rows (offsets `[0, 1]`, -//! offset-major: the first `step_size` rows are the current-row block, the rest -//! are next-row blocks) and one column per trace column. Only the columns a -//! transition constraint actually reads at the next row — the AIR's transition -//! window, [`crate::traits::AIR::trace_ood_next_row_columns`] — need to be +//! The frame OOD table has `num_offsets * step_size` rows (offset-major: the +//! first `step_size` rows are offset 0's current-row block, and every later +//! offset contributes a `step_size`-row next-row block) and one column per +//! trace column. Only the columns a transition constraint actually reads at the +//! next row — the AIR's transition window, +//! [`crate::traits::AIR::trace_ood_next_row_columns`] — need to be //! opened in the next-row block(s). Every other next-row entry is redundant and //! is pruned from the proof. //! @@ -44,11 +45,17 @@ pub fn num_surviving_trace_openings( /// Build the rectangular `num_total_cols x num_eval_points` DEEP trace-term /// coefficient grid from `powers` (the `num_surviving_trace_openings` gamma /// powers drained for the trace terms). Surviving positions receive a power in a -/// fixed order; pruned next-row positions receive zero. A rectangular DEEP +/// fixed order; pruned next-row positions stay zero. A rectangular DEEP /// evaluation over the full grid therefore yields the identical polynomial as /// summing only the survivors — which is what lets the prover keep its /// (GPU-friendly) rectangular DEEP unchanged. /// +/// Precondition: `powers.len() == num_surviving_trace_openings(num_total_cols, +/// num_eval_points, step_size, next_row_cols.len())` for the same layout args — +/// every power binds to exactly one surviving position and every surviving +/// position consumes exactly one power. The function asserts this; a mismatch is +/// a programmer bug in the layout (invariant I3), never a proof-controlled input. +/// /// Assignment order (mirrored exactly by [`num_surviving_trace_openings`]): /// 1. current-row block — for every column `j`, rows `0..step_size`; /// 2. next-row block — for each masked column `j`, rows `step_size..num_eval_points`. @@ -65,24 +72,28 @@ pub fn build_pruned_trace_term_coeffs( // Current-row block: all columns, rows 0..step_size. for col in coeffs.iter_mut() { for slot in col.iter_mut().take(step_size) { - if p < powers.len() { - *slot = powers[p].clone(); - p += 1; - } + *slot = powers[p].clone(); + p += 1; } } // Next-row block(s): masked columns only, rows step_size..num_eval_points. for (j, col) in coeffs.iter_mut().enumerate() { if flags[j] { for slot in col.iter_mut().take(num_eval_points).skip(step_size) { - if p < powers.len() { - *slot = powers[p].clone(); - p += 1; - } + *slot = powers[p].clone(); + p += 1; } } } - debug_assert_eq!(p, powers.len(), "power assignment must consume every power"); + // Both the number of assignments and `powers.len()` are pure functions of AIR + // shape metadata (invariant I3), never proof-controlled, so a mismatch is a + // programmer bug in an AIR's `trace_ood_next_row_columns` override — panic + // hard rather than silently leave surplus gammas unbound. + assert_eq!( + p, + powers.len(), + "power count must match num_surviving_trace_openings for this layout" + ); coeffs } @@ -226,7 +237,14 @@ mod tests { let full = Table::new(vec![fe(10), fe(11), fe(20), fe(21)], 2); let (b0, b1) = split_ood_blocks(&full, 1, &[]); assert_eq!(b1.width, 0); - let recon = reconstruct_ood_full(b0.row_major_data(), b0.width, b1.row_major_data(), 2, 1, &[]); + let recon = reconstruct_ood_full( + b0.row_major_data(), + b0.width, + b1.row_major_data(), + 2, + 1, + &[], + ); assert_eq!(recon.get_row(0), full.get_row(0)); assert_eq!(recon.get_row(1), &[Fe::zero(), Fe::zero()]); } diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index 522e63e74..3fe80f5a2 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -157,7 +157,7 @@ pub trait IsStarkVerifier< let expected_next_height = if expected_next_width == 0 { 0 } else { - num_eval_points - step_size + num_eval_points.saturating_sub(step_size) }; let ood_current = proof.trace_ood_evaluations(); let ood_next = proof.trace_ood_next_evaluations(); From 009f6de3c8e187168eec3a9bac44a680c76019b9 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 16 Jul 2026 12:21:03 -0300 Subject: [PATCH 2/3] fix(stark): clippy lints in forward-accumulation tests Pre-existing -D warnings clippy errors in test code added on the #823 branch; CI's `make lint` (cargo clippy --workspace --all-targets) flags them but a crate-scoped lib-only clippy did not. - lookup.rs accumulated_column_is_forward_and_circular: iterate `&term_columns` instead of `0..n_term_cols` (needless_range_loop, two sites) and deref the two `get_aux(..).clone()` reads (clone_on_copy; FieldElement is Copy). - logup_gpu.rs reference_accumulate: `out.push(acc.clone())` -> `out.push(acc)` (clone_on_copy). Only surfaces under the cuda-feature clippy pass, which the earlier passes stop short of. --- crypto/stark/src/logup_gpu.rs | 2 +- crypto/stark/src/lookup.rs | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/crypto/stark/src/logup_gpu.rs b/crypto/stark/src/logup_gpu.rs index 844b55279..3fd49134d 100644 --- a/crypto/stark/src/logup_gpu.rs +++ b/crypto/stark/src/logup_gpu.rs @@ -989,7 +989,7 @@ mod tests { let mut out = Vec::with_capacity(num_rows); for row in 0..num_rows { // Forward accumulation: acc[0] = 0, fold the current row afterwards. - out.push(acc.clone()); + out.push(acc); let mut rs = FieldElement::::zero(); for c in cols { rs = &rs + &c[row]; diff --git a/crypto/stark/src/lookup.rs b/crypto/stark/src/lookup.rs index 4a684b8df..8a89ea727 100644 --- a/crypto/stark/src/lookup.rs +++ b/crypto/stark/src/lookup.rs @@ -2432,11 +2432,11 @@ mod logup_single_source_tests { let n_fe = Fp3::from(n_rows as u64); for i in 0..n_rows { let mut row_sum = Fp3::zero(); - for c in 0..n_term_cols { - row_sum = row_sum + &term_columns[c][i]; + for col in &term_columns { + row_sum = row_sum + &col[i]; } - let acc_i = trace.get_aux(i, acc_col_idx).clone(); - let acc_next = trace.get_aux((i + 1) % n_rows, acc_col_idx).clone(); + let acc_i = *trace.get_aux(i, acc_col_idx); + let acc_next = *trace.get_aux((i + 1) % n_rows, acc_col_idx); let lhs = (acc_next - acc_i) * &n_fe; let rhs = row_sum * &n_fe - &l; assert_eq!(lhs, rhs, "forward circular recurrence broken at row {i}"); From a7ea155f63502a61f19205fe6e6f72fc9734f394 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 16 Jul 2026 12:23:48 -0300 Subject: [PATCH 3/3] fix(stark): keep debug-only power-count check in build_pruned_trace_term_coeffs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit build_pruned_trace_term_coeffs is a shared helper the verifier calls, and the verifier must never contain a panic path: an invalid proof is just a false proof, not a crash. Revert the hardening — restore the per-slot `if p < powers.len()` guards and the `debug_assert_eq!` power-count check. The doc comment still states the strict precondition (powers.len() == num_surviving_trace_openings for the same layout args); that is pure documentation and stays. --- crypto/stark/src/ood.rs | 28 ++++++++++++---------------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/crypto/stark/src/ood.rs b/crypto/stark/src/ood.rs index 322a099fb..a779d7851 100644 --- a/crypto/stark/src/ood.rs +++ b/crypto/stark/src/ood.rs @@ -45,7 +45,7 @@ pub fn num_surviving_trace_openings( /// Build the rectangular `num_total_cols x num_eval_points` DEEP trace-term /// coefficient grid from `powers` (the `num_surviving_trace_openings` gamma /// powers drained for the trace terms). Surviving positions receive a power in a -/// fixed order; pruned next-row positions stay zero. A rectangular DEEP +/// fixed order; pruned next-row positions receive zero. A rectangular DEEP /// evaluation over the full grid therefore yields the identical polynomial as /// summing only the survivors — which is what lets the prover keep its /// (GPU-friendly) rectangular DEEP unchanged. @@ -53,8 +53,8 @@ pub fn num_surviving_trace_openings( /// Precondition: `powers.len() == num_surviving_trace_openings(num_total_cols, /// num_eval_points, step_size, next_row_cols.len())` for the same layout args — /// every power binds to exactly one surviving position and every surviving -/// position consumes exactly one power. The function asserts this; a mismatch is -/// a programmer bug in the layout (invariant I3), never a proof-controlled input. +/// position consumes exactly one power. Both operands are AIR-metadata-derived +/// (invariant I3), so this holds for every real AIR; a debug build checks it. /// /// Assignment order (mirrored exactly by [`num_surviving_trace_openings`]): /// 1. current-row block — for every column `j`, rows `0..step_size`; @@ -72,28 +72,24 @@ pub fn build_pruned_trace_term_coeffs( // Current-row block: all columns, rows 0..step_size. for col in coeffs.iter_mut() { for slot in col.iter_mut().take(step_size) { - *slot = powers[p].clone(); - p += 1; + if p < powers.len() { + *slot = powers[p].clone(); + p += 1; + } } } // Next-row block(s): masked columns only, rows step_size..num_eval_points. for (j, col) in coeffs.iter_mut().enumerate() { if flags[j] { for slot in col.iter_mut().take(num_eval_points).skip(step_size) { - *slot = powers[p].clone(); - p += 1; + if p < powers.len() { + *slot = powers[p].clone(); + p += 1; + } } } } - // Both the number of assignments and `powers.len()` are pure functions of AIR - // shape metadata (invariant I3), never proof-controlled, so a mismatch is a - // programmer bug in an AIR's `trace_ood_next_row_columns` override — panic - // hard rather than silently leave surplus gammas unbound. - assert_eq!( - p, - powers.len(), - "power count must match num_surviving_trace_openings for this layout" - ); + debug_assert_eq!(p, powers.len(), "power assignment must consume every power"); coeffs }