From 3d232929c4f9d2c677befa35480dd60e5e7e2674 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 15 Jul 2026 14:29:37 -0300 Subject: [PATCH 1/7] refactor(logup): forward accumulation so acc is the sole next-row OOD read MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The circular LogUp accumulator previously summed each row's terms at the NEXT frame row: `acc[i+1] − acc[i] = terms[i+1] − L/N`. That made the committed term columns AND the absorbed interactions' main-trace columns (multiplicity + bus values) all next-row (offset-1) reads, so the OOD opening had to send the full trace width at g·z. Switch to forward accumulation — `acc[i+1] − acc[i] = terms[i] − L/N`, `acc[0] = 0` — by reading the committed-term sum and the absorbed multiplicity/fingerprint operands at the CURRENT row (offset 0) in `emit_logup_accumulated`, and writing `acc[row]` before folding in the current row's terms in `build_accumulated_column_from_terms`. `acc_next` stays the one offset-1 operand. Since `emit_logup_accumulated` is now the sole accumulator path (monomorphized into ProverEvalFolder / VerifierEvalFolder and mirrored by the constraint_ir interpreter), the single edit covers prover and verifier identically. `acc` is thus the ONLY column any constraint reads at the next row across the whole system — the enabler for pruning the g·z trace-OOD block down to one column in a follow-up. Soundness: unchanged. The circular transition telescopes to force `Σterms = N·(L/N) = L` regardless of the accumulator's constant offset; the boundary pin (moved from `acc[N-1]=0` to `acc[0]=0`) only removes that constant-shift DOF. `table_contribution` L and the cross-table bus-balance check are untouched. Corrupting the acc OOD is still rejected. GPU: the on-device accumulate (`logup.cu` `logup_finalize_accum_ext3`) switches from an inclusive to an exclusive prefix scan (`acc[i] = scan[i-1] − i·offset`, `acc[0]=0`); the parity reference in `logup_gpu.rs` mirrors it. The CUDA path needs GPU-server validation (not buildable in CI without the toolchain). Tests: full `stark` suite (190) green, including LogUp completeness (real proofs verify — which structurally require `acc[0]=0`), soundness negatives, and the prover/verifier/IR three-way folder-equivalence regression on the 1- and 2-absorbed branches. Added a focused forward-accumulation contract test on the build function. Inline prover prove+verify modules (bitwise/lt/branch/l2g/bitwise-bus) all green; the only failures in this env are missing prebuilt ELF artifacts. --- crypto/math-cuda/kernels/logup.cu | 14 +++-- crypto/stark/src/logup_gpu.rs | 3 +- crypto/stark/src/lookup.rs | 99 ++++++++++++++++++++++++------- 3 files changed, 89 insertions(+), 27 deletions(-) diff --git a/crypto/math-cuda/kernels/logup.cu b/crypto/math-cuda/kernels/logup.cu index 0c01a2f46..33218f143 100644 --- a/crypto/math-cuda/kernels/logup.cu +++ b/crypto/math-cuda/kernels/logup.cu @@ -115,7 +115,7 @@ extern "C" __global__ void logup_term_ext3( // Accumulated column (K4): running sum of the term columns, on device. // row_sum[i] = sum over all term columns of term[col][i] // S = inclusive prefix scan of row_sum ; L = S[n-1] ; offset = L / N -// acc[i] = S[i] - (i+1) * offset (matches build_accumulated_column_from_terms) +// acc[i] = S[i-1] - i * offset (acc[0]=0) (matches build_accumulated_column_from_terms) // Additive 3-phase Hillis-Steele scan (mirrors inverse.cu, add not mul). // =========================================================================== @@ -193,7 +193,10 @@ extern "C" __global__ void logup_apply_offsets_add_ext3( scan_inout[o + 2] = v.c; } -// acc[i] = scan[i] - (i+1) * (L * inv_N), L = scan[n-1]. inv_N is ext3 (1/N). +// Forward accumulation (matches build_accumulated_column_from_terms): +// acc[i] = scan_exclusive[i] - i * (L * inv_N), L = scan[n-1], inv_N = 1/N. +// scan is the INCLUSIVE prefix scan, so scan_exclusive[i] = scan[i-1] and +// acc[0] = 0. This is the exclusive-scan analogue of the old inclusive form. extern "C" __global__ void logup_finalize_accum_ext3( const uint64_t *__restrict__ scan, uint64_t n, uint64_t inv0, uint64_t inv1, uint64_t inv2, uint64_t *__restrict__ acc) { @@ -203,8 +206,11 @@ extern "C" __global__ void logup_finalize_accum_ext3( uint64_t lo = (n - 1) * 3; Fe3 L = make(scan[lo], scan[lo + 1], scan[lo + 2]); Fe3 offset = mul(L, make(inv0, inv1, inv2)); - Fe3 s = make(scan[i * 3], scan[i * 3 + 1], scan[i * 3 + 2]); - Fe3 a = sub(s, mul_base(offset, i + 1)); + // Exclusive prefix: row 0 has no predecessor, so acc[0] = 0. + Fe3 s = (i == 0) ? zero() + : make(scan[(i - 1) * 3], scan[(i - 1) * 3 + 1], + scan[(i - 1) * 3 + 2]); + Fe3 a = sub(s, mul_base(offset, i)); acc[i * 3] = a.a; acc[i * 3 + 1] = a.b; acc[i * 3 + 2] = a.c; diff --git a/crypto/stark/src/logup_gpu.rs b/crypto/stark/src/logup_gpu.rs index bc9e88302..844b55279 100644 --- a/crypto/stark/src/logup_gpu.rs +++ b/crypto/stark/src/logup_gpu.rs @@ -988,12 +988,13 @@ mod tests { let mut acc = FieldElement::::zero(); 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()); let mut rs = FieldElement::::zero(); for c in cols { rs = &rs + &c[row]; } acc = &acc + &rs - &offset; - out.push(acc); } (out, total) } diff --git a/crypto/stark/src/lookup.rs b/crypto/stark/src/lookup.rs index 4273f29a7..07fc4c382 100644 --- a/crypto/stark/src/lookup.rs +++ b/crypto/stark/src/lookup.rs @@ -1266,17 +1266,17 @@ where pub_inputs: &Self::PublicInputs, rap_challenges: &[FieldElement], _bus_public_inputs: Option<&BusPublicInputs>, - trace_length: usize, + _trace_length: usize, ) -> BoundaryConstraints { let mut boundary_constraints = B::boundary_constraints(pub_inputs, rap_challenges); - // Pin acc[N-1] = 0 to remove the constant-shift degree of freedom - // in the circular transition constraint. + // Pin acc[0] = 0 to remove the constant-shift degree of freedom in the + // circular transition constraint (forward accumulation starts at 0). if !self.auxiliary_trace_build_data.interactions.is_empty() { let acc_col_idx = self.trace_layout.1 - 1; // last aux column = accumulated boundary_constraints.push(BoundaryConstraint::new_aux( acc_col_idx, - trace_length - 1, + 0, FieldElement::zero(), )); } @@ -1685,9 +1685,10 @@ where /// Builds the circular accumulated column from pre-computed term columns. /// -/// For the circular constraint: acc[(i+1) mod N] - acc[i] - terms[(i+1) mod N] + L/N = 0 -/// We build: acc[0] = terms[0] - L/N, acc[i] = acc[i-1] + terms[i] - L/N -/// Result: acc[N-1] = L - N*(L/N) = 0 +/// For the circular constraint: acc[(i+1) mod N] - acc[i] - terms[i] + L/N = 0 +/// (forward accumulation: the increment at transition i→i+1 uses the CURRENT +/// row's terms). We build: acc[0] = 0, acc[i] = acc[i-1] + terms[i-1] - L/N. +/// Result: the running sum returns to acc[0] since Σterms - N*(L/N) = 0. /// /// Returns L (table_contribution = sum of all terms across all rows). fn build_accumulated_column_from_terms( @@ -1718,15 +1719,17 @@ where let n = FieldElement::::from(trace_len as u64); let offset_per_row = &table_contribution * n.inv().unwrap(); - // Build circular accumulated column + // Build circular accumulated column (forward accumulation: write acc[row] + // BEFORE folding in the current row's terms, so acc[0] = 0 and + // acc[row+1] - acc[row] = row_sum[row] - L/N). let mut accumulated = FieldElement::::zero(); for row in 0..trace_len { + trace.set_aux(row, acc_column_idx, accumulated.clone()); let mut row_sum = FieldElement::::zero(); for col in term_columns { row_sum = row_sum + &col[row]; } accumulated = &accumulated + &row_sum - &offset_per_row; - trace.set_aux(row, acc_column_idx, accumulated.clone()); } #[cfg(feature = "instruments")] @@ -2123,9 +2126,12 @@ where } /// Emit the accumulated constraint (with 1–2 absorbed interactions). -/// `acc_curr` reads row 0; `acc_next`, -/// the committed-term sum and the absorbed fingerprints/multiplicities all read -/// the NEXT row (offset 1). +/// `acc_next` reads the NEXT row (offset 1) — the *only* next-row read in the +/// whole constraint system. `acc_curr`, the committed-term sum and the absorbed +/// fingerprints/multiplicities all read the CURRENT row (offset 0), so the +/// forward recurrence is `acc[i+1] − acc[i] = Σterms[i] + absorbed[i] − L/N`. +/// Keeping every non-`acc` operand on the current row lets the OOD opening send +/// only `acc` at `g·z`, not the whole trace width. /// /// - 1 absorbed: `(acc_next − acc_curr − Σterms + L/N)·f − sign·m` (degree 2) /// - 2 absorbed: `(…)·f₁·f₂ − sign₁·m₁·f₂ − sign₂·m₂·f₁` (degree 3) @@ -2138,30 +2144,33 @@ where let acc_curr = b.aux(0, layout.acc_column_idx); let acc_next = b.aux(1, layout.acc_column_idx); - // delta = acc_next − acc_curr − Σ committed_terms(next) + L/N + // delta = acc_next − acc_curr − Σ committed_terms(curr) + L/N. + // Committed terms read the current row (offset 0) so that `acc_next` is the + // sole next-row operand (see the doc comment). let mut delta = acc_next - acc_curr; for i in 0..layout.num_term_columns { - delta = delta - b.aux(1, i); + delta = delta - b.aux(0, i); } delta = delta + b.table_offset(); let absorbed = layout.absorbed(); let root = match absorbed.len() { 1 => { - // delta · f − sign · m - let m = emit_multiplicity::(b, &absorbed[0].multiplicity, 1); - let f = emit_fingerprint::(b, &absorbed[0], 1); + // delta · f − sign · m; absorbed operands read the current row. + let m = emit_multiplicity::(b, &absorbed[0].multiplicity, 0); + let f = emit_fingerprint::(b, &absorbed[0], 0); let mt = if absorbed[0].is_sender { m } else { -m }; // delta · f is ext; `mt` is base. The tower only implements base − // ext (base operand LEFT), so write `delta·f − mt` as `−(mt − delta·f)`. -(mt - delta * f) } 2 => { - // delta · f1 · f2 − sign1·m1·f2 − sign2·m2·f1 - let m1 = emit_multiplicity::(b, &absorbed[0].multiplicity, 1); - let m2 = emit_multiplicity::(b, &absorbed[1].multiplicity, 1); - let f1 = emit_fingerprint::(b, &absorbed[0], 1); - let f2 = emit_fingerprint::(b, &absorbed[1], 1); + // delta · f1 · f2 − sign1·m1·f2 − sign2·m2·f1; absorbed operands + // read the current row (offset 0). + let m1 = emit_multiplicity::(b, &absorbed[0].multiplicity, 0); + let m2 = emit_multiplicity::(b, &absorbed[1].multiplicity, 0); + let f1 = emit_fingerprint::(b, &absorbed[0], 0); + let f2 = emit_fingerprint::(b, &absorbed[1], 0); let term1 = m1 * f2.clone(); let term1 = if absorbed[0].is_sender { term1 } else { -term1 }; @@ -2342,6 +2351,52 @@ mod logup_single_source_tests { ]) } + /// Forward-accumulation contract for [`build_accumulated_column_from_terms`]: + /// `acc[0] = 0` and the circular recurrence tied to the CURRENT row's terms + /// holds on EVERY row, including the wraparound (which closes the cycle back + /// to `acc[0]`). This is the invariant the OOD pruning relies on — only + /// `acc` is read at the next row; every term is read at the current row. + #[test] + fn accumulated_column_is_forward_and_circular() { + let mut rng = SplitMix64::new(0xC0FF_EE12_3456_789A); + let n_rows = 8usize; + let n_term_cols = 2usize; + + let term_columns: Vec> = (0..n_term_cols) + .map(|_| (0..n_rows).map(|_| rand_fp3(&mut rng)).collect()) + .collect(); + + // Accumulated column follows the committed term columns. + let acc_col_idx = n_term_cols; + let mut trace = TraceTable::::new_main(vec![Fp::zero(); n_rows], 1, 1); + trace.allocate_aux_table(n_term_cols + 1); + + let l = build_accumulated_column_from_terms(acc_col_idx, &term_columns, &mut trace); + + // Forward accumulation starts at zero. + assert_eq!( + *trace.get_aux(0, acc_col_idx), + Fp3::zero(), + "acc[0] must be 0 under forward accumulation" + ); + + // Circular recurrence tied to the CURRENT row's terms, on every row. + // Multiplied through by N to avoid dividing L by N: + // (acc[(i+1) mod N] - acc[i]) * N == (Σ terms[i]) * N - L + 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]; + } + 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 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}"); + } + } + /// The permanent regression check for one layout, on `TRIALS` random /// two-step frames: the LogUp body run three ways from ONE definition must /// agree bit-for-bit — [`ProverEvalFolder`] == capture→[`eval_program`] From 6939c359aaf2936ea977092262af69c3f7336b1b Mon Sep 17 00:00:00 2001 From: Diego K <43053772+diegokingston@users.noreply.github.com> Date: Wed, 15 Jul 2026 20:36:03 -0300 Subject: [PATCH 2/7] =?UTF-8?q?feat(stark):=20prune=20redundant=20g=C2=B7z?= =?UTF-8?q?=20(next-row)=20trace-OOD=20openings=20(#827)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * harden(verifier): derive OOD table shape from AIR metadata, not the proof The verifier read the trace-OOD table's shape from the (prover-controlled) proof dimensions (`num_main = trace_ood_evaluations.width - num_aux`), only indirectly cross-checked. Reject any proof whose OOD table is not exactly the AIR-derived size — height = transition_offsets.len() * step_size, width = main + aux — before any use of the table, and take the main width from the AIR rather than the proof. A malicious prover can no longer reshape the table (e.g. drop a column) to dodge a constraint check or trigger an out-of-bounds read in the frame reconstruction. This is the shape-from-metadata invariant (I3) that the upcoming g·z OOD pruning relies on: once the next-row block is pruned to just the accumulator column, the verifier must reconstruct the reduced shape purely from public AIR metadata, identically to the prover. Test: `test_malformed_ood_table_shape_rejected` (drop a column from an otherwise-valid ADD proof's OOD table → rejected). Full stark suite green (192). * feat(air): trace_ood_next_row_columns — the per-column transition window Adds an AIR-metadata method (default empty) naming the full-width `[main|aux]` column indices that transition constraints read at the NEXT row (offset 1) — lambda_vm's fine-grained analogue of Plonky3's transition window (a whole-row "uses next row?" flag). `AirWithBuses` overrides it to return exactly the accumulator column, the sole next-row read after forward accumulation. This is the public, prover=verifier-identical source of truth for which OOD openings survive at g·z. The upcoming pruning consumes it on both sides so the reduced OOD shape is derived from AIR metadata, never from the proof. Test: `test_trace_ood_next_row_columns_is_accumulator_only`. stark suite green (193). * feat(stark): prune redundant g·z (next-row) trace-OOD openings Only the columns a transition constraint reads at the next row (the AIR transition window, `trace_ood_next_row_columns`) need an OOD opening at g·z. After forward accumulation that is just the LogUp accumulator, so the next-row half of the trace-OOD collapses from the full width W to one column per bus table — a smaller proof and, more importantly, ~halved DEEP trace-term work in the verifier / recursion guest (the cycle win). Design (CUDA-safe — the GPU DEEP kernel is untouched): - New `crate::ood` module of pure, prover=verifier-identical helpers deriving the surviving-opening layout from public AIR metadata (invariant I3). - Fiat-Shamir: both sides sample `num_surviving_trace_openings` DEEP gamma powers (was `2·step_size·W`). The gamma is one field element either way, so transcript consumption is unchanged; only the trace/composition split moves. - Prover keeps its rectangular W×(2·step_size) DEEP (CPU and GPU) by scattering the sampled powers into the full grid with ZEROS at pruned positions — zero terms vanish, so the DEEP polynomial is identical with no kernel change. The proof carries only the two surviving blocks (`trace_ood_evaluations` = current-row S×W, new `trace_ood_next_evaluations` = next-row S×|window|), and the transcript absorbs only those. - Verifier reconstructs the full grid from the two blocks and SKIPS pruned next-row terms in the DEEP loop (the cycle saving), after validating both block shapes against AIR metadata (extends the I3 guard). Default `trace_ood_next_row_columns` is conservative (every column — no pruning), so any AIR that reads the next row stays correct without overriding; `AirWithBuses` overrides to the accumulator column. Proof is bincode/serde, so the wire change is transparent; the recursion guest recompiles the same source. Tests: full stark suite green (198) incl. multi_prove_ram roundtrips (pruned proofs verify), soundness negatives (tampered/mis-shaped OOD rejected), a `test_gz_pruning_reduces_next_row_openings` win check (next-row block = 1 col vs full width, still verifies), and `ood` unit tests. Inline VM-table prove+ verify (bitwise/lt/branch/bus) green. GPU DEEP path unchanged (no cuda build here; kernel needs no change by construction). --- crypto/stark/src/lib.rs | 1 + crypto/stark/src/lookup.rs | 13 + crypto/stark/src/ood.rs | 224 ++++++++++++++++++ crypto/stark/src/proof/stark.rs | 6 +- crypto/stark/src/prover.rs | 52 +++- .../src/tests/bus_tests/soundness_tests.rs | 165 +++++++++++++ crypto/stark/src/traits.rs | 21 ++ crypto/stark/src/verifier.rs | 133 +++++++++-- 8 files changed, 582 insertions(+), 33 deletions(-) create mode 100644 crypto/stark/src/ood.rs diff --git a/crypto/stark/src/lib.rs b/crypto/stark/src/lib.rs index caa1c73a0..6f8e7c82e 100644 --- a/crypto/stark/src/lib.rs +++ b/crypto/stark/src/lib.rs @@ -23,6 +23,7 @@ pub mod instruments; #[cfg(feature = "cuda")] pub mod logup_gpu; pub mod lookup; +pub mod ood; pub(crate) mod par; pub mod profile_markers; pub mod proof; diff --git a/crypto/stark/src/lookup.rs b/crypto/stark/src/lookup.rs index 07fc4c382..d52624980 100644 --- a/crypto/stark/src/lookup.rs +++ b/crypto/stark/src/lookup.rs @@ -1003,6 +1003,19 @@ where self.trace_layout } + fn trace_ood_next_row_columns(&self) -> Vec { + // The only transition constraint that reads the next row is the circular + // LogUp accumulator, and after forward accumulation it reads only the + // accumulated column there (all committed terms and absorbed operands + // read the current row). Its full-width index is the main width plus the + // accumulated column's aux index. No interactions => no next-row reads. + if self.auxiliary_trace_build_data.interactions.is_empty() { + Vec::new() + } else { + vec![self.trace_layout.0 + self.logup.acc_column_idx] + } + } + fn has_trace_interaction(&self) -> bool { !self.auxiliary_trace_build_data.interactions.is_empty() } diff --git a/crypto/stark/src/ood.rs b/crypto/stark/src/ood.rs new file mode 100644 index 000000000..f9dfc6e35 --- /dev/null +++ b/crypto/stark/src/ood.rs @@ -0,0 +1,224 @@ +//! 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 +//! opened in the next-row block(s). Every other next-row entry is redundant and +//! is pruned from the proof. +//! +//! Everything here is a pure function of public AIR shape metadata (`step_size`, +//! the column count, and the next-row column set), so the prover and verifier +//! derive the identical layout without trusting proof dimensions (invariant I3). + +use crate::table::Table; +use math::field::{element::FieldElement, traits::IsField}; + +/// Per-column flags: `flags[c] == true` iff column `c` is opened at the next +/// row. Indices outside `0..num_total_cols` are ignored. +pub fn next_row_col_flags(num_total_cols: usize, next_row_cols: &[usize]) -> Vec { + let mut flags = vec![false; num_total_cols]; + for &c in next_row_cols { + if c < num_total_cols { + flags[c] = true; + } + } + flags +} + +/// Number of surviving trace openings: the current-row block opens every column +/// (`step_size * num_total_cols`), and each next-row row opens only the masked +/// columns (`(num_eval_points - step_size) * num_next_row_cols`). +pub fn num_surviving_trace_openings( + num_total_cols: usize, + num_eval_points: usize, + step_size: usize, + num_next_row_cols: usize, +) -> usize { + let next_rows = num_eval_points.saturating_sub(step_size); + step_size * num_total_cols + next_rows * num_next_row_cols +} + +/// 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 +/// 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. +/// +/// 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`. +pub fn build_pruned_trace_term_coeffs( + powers: &[FieldElement], + num_total_cols: usize, + num_eval_points: usize, + step_size: usize, + next_row_cols: &[usize], +) -> Vec>> { + let flags = next_row_col_flags(num_total_cols, next_row_cols); + let mut coeffs = vec![vec![FieldElement::::zero(); num_eval_points]; num_total_cols]; + let mut p = 0usize; + // 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; + } + } + } + // 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; + } + } + } + } + debug_assert_eq!(p, powers.len(), "power assignment must consume every power"); + coeffs +} + +/// Split the full `num_eval_points x num_total_cols` OOD table (computed by the +/// prover) into the two blocks carried by the proof: +/// * block 0 — the current-row block, `step_size x num_total_cols` (all columns); +/// * block 1 — the next-row block, `next_rows x num_next_row_cols`, holding only +/// the masked columns in `next_row_cols` order. +/// +/// Block 1 has width 0 (an empty table) when the AIR reads no next-row columns. +pub fn split_ood_blocks( + full: &Table, + step_size: usize, + next_row_cols: &[usize], +) -> (Table, Table) { + let w = full.width; + + let mut b0 = Vec::with_capacity(step_size * w); + for r in 0..step_size { + b0.extend_from_slice(full.get_row(r)); + } + let block0 = Table::new(b0, w); + + let mut b1 = Vec::with_capacity((full.height.saturating_sub(step_size)) * next_row_cols.len()); + for r in step_size..full.height { + let row = full.get_row(r); + for &c in next_row_cols { + b1.push(row[c].clone()); + } + } + let block1 = Table::new(b1, next_row_cols.len()); + + (block0, block1) +} + +/// Rebuild the full `num_eval_points x num_total_cols` OOD table from the two +/// pruned proof blocks. Current-row rows come straight from `block0`; each +/// next-row row scatters the masked values from `block1` into their columns and +/// leaves every other column zero. Those zero entries are never read — no +/// transition constraint references a pruned column at the next row, and DEEP +/// skips them — so the reconstruction is exact where it matters. +pub fn reconstruct_ood_full( + block0: &Table, + block1: &Table, + num_eval_points: usize, + step_size: usize, + next_row_cols: &[usize], +) -> Table { + let w = block0.width; + let mut data = Vec::with_capacity(num_eval_points * w); + + for r in 0..step_size { + data.extend_from_slice(block0.get_row(r)); + } + + for r in step_size..num_eval_points { + let has_next = block1.width > 0 && (r - step_size) < block1.height; + for c in 0..w { + let mut val = FieldElement::::zero(); + if has_next { + for (m, &mc) in next_row_cols.iter().enumerate() { + if mc == c { + val = block1.get_row(r - step_size)[m].clone(); + break; + } + } + } + data.push(val); + } + } + + Table::new(data, w) +} + +#[cfg(test)] +mod tests { + use super::*; + use math::field::goldilocks::GoldilocksField as Gl; + + type Fe = FieldElement; + + fn fe(x: u64) -> Fe { + Fe::from(x) + } + + #[test] + fn surviving_count_matches_layout() { + // 3 columns, 2 eval points (step_size 1), 1 next-row column: + // current-row opens 3, next-row opens 1 => 4. + assert_eq!(num_surviving_trace_openings(3, 2, 1, 1), 4); + // No next-row columns => only the current-row block survives. + assert_eq!(num_surviving_trace_openings(3, 2, 1, 0), 3); + // Every column open at the next row => full 2*W grid. + assert_eq!(num_surviving_trace_openings(3, 2, 1, 3), 6); + } + + #[test] + fn split_then_reconstruct_preserves_survivors_and_zeros_pruned() { + // Full 2x3 OOD table: row 0 (current row), row 1 (next row). + let full = Table::new(vec![fe(10), fe(11), fe(12), fe(20), fe(21), fe(22)], 3); + let next_row_cols = [1usize]; // only column 1 opens at the next row + let step_size = 1; + + let (b0, b1) = split_ood_blocks(&full, step_size, &next_row_cols); + assert_eq!((b0.width, b0.height), (3, 1)); + assert_eq!((b1.width, b1.height), (1, 1)); + assert_eq!(b1.get_row(0)[0], fe(21)); // full[1][1] + + let recon = reconstruct_ood_full(&b0, &b1, 2, step_size, &next_row_cols); + assert_eq!(recon.get_row(0), full.get_row(0)); // current row is exact + assert_eq!(recon.get_row(1)[1], fe(21)); // survivor placed + assert_eq!(recon.get_row(1)[0], Fe::zero()); // pruned -> zero + assert_eq!(recon.get_row(1)[2], Fe::zero()); // pruned -> zero + } + + #[test] + fn empty_next_row_block_reconstructs_to_zeros() { + 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, &b1, 2, 1, &[]); + assert_eq!(recon.get_row(0), full.get_row(0)); + assert_eq!(recon.get_row(1), &[Fe::zero(), Fe::zero()]); + } + + #[test] + fn pruned_coeffs_are_zero_off_the_window() { + // 4 surviving powers for W=3, num_eval_points=2, mask={1}. + let powers: Vec = (1..=4).map(fe).collect(); + let coeffs = build_pruned_trace_term_coeffs(&powers, 3, 2, 1, &[1]); + // Current-row row (k=0) is fully populated; next-row row (k=1) only col 1. + assert_ne!(coeffs[0][0], Fe::zero()); + assert_ne!(coeffs[1][0], Fe::zero()); + assert_ne!(coeffs[2][0], Fe::zero()); + assert_ne!(coeffs[1][1], Fe::zero()); // masked column, next row + assert_eq!(coeffs[0][1], Fe::zero()); // pruned + assert_eq!(coeffs[2][1], Fe::zero()); // pruned + } +} diff --git a/crypto/stark/src/proof/stark.rs b/crypto/stark/src/proof/stark.rs index 675160837..6e2a55870 100644 --- a/crypto/stark/src/proof/stark.rs +++ b/crypto/stark/src/proof/stark.rs @@ -49,8 +49,12 @@ pub struct StarkProof, E: IsField, PI> { // For preprocessed tables: commitment to precomputed columns only. // Verifier checks this matches the hardcoded commitment from AIR. pub lde_trace_precomputed_merkle_root: Option, - // tⱼ(zgᵏ) + // tⱼ(zgᵏ) for the current-row block (offset 0): every trace column at z. pub trace_ood_evaluations: Table, + // tⱼ(zgᵏ) for the next-row block(s) (offset >= 1), pruned to only the columns + // a transition constraint reads at the next row (the AIR transition window). + // Empty (width 0) when the AIR reads no next-row columns. + pub trace_ood_next_evaluations: Table, // Commitments to Hᵢ pub composition_poly_root: Commitment, // Hᵢ(z^N) diff --git a/crypto/stark/src/prover.rs b/crypto/stark/src/prover.rs index 7fa560e5c..69fab1619 100644 --- a/crypto/stark/src/prover.rs +++ b/crypto/stark/src/prover.rs @@ -1458,8 +1458,16 @@ pub trait IsStarkProver< let gamma = transcript.sample_field_element(); let n_terms_composition_poly = round_2_result.lde_composition_poly_evaluations.len(); - let num_terms_trace = - air.context().transition_offsets.len() * air.step_size() * air.context().trace_columns; + let num_eval_points = air.context().transition_offsets.len() * air.step_size(); + let next_row_cols = air.trace_ood_next_row_columns(); + // g·z pruning: only the current-row block (all columns) plus the masked + // next-row columns get an opening / DEEP coefficient. + let num_terms_trace = crate::ood::num_surviving_trace_openings( + air.context().trace_columns, + num_eval_points, + air.step_size(), + next_row_cols.len(), + ); // <<<< Receive challenges: 𝛾, 𝛾' let mut deep_composition_coefficients: Vec<_> = @@ -1467,12 +1475,19 @@ pub trait IsStarkProver< .take(n_terms_composition_poly + num_terms_trace) .collect(); - let trace_term_coeffs: Vec<_> = deep_composition_coefficients + let trace_term_powers: Vec<_> = deep_composition_coefficients .drain(..num_terms_trace) - .collect::>() - .chunks(air.context().transition_offsets.len() * air.step_size()) - .map(|chunk| chunk.to_vec()) .collect(); + // Rectangular W×num_eval_points grid with the sampled powers at surviving + // positions and zeros at pruned next-row positions, so the DEEP loop + // below (and the GPU path) stay unchanged — zero-coefficient terms vanish. + let trace_term_coeffs = crate::ood::build_pruned_trace_term_coeffs( + &trace_term_powers, + air.context().trace_columns, + num_eval_points, + air.step_size(), + &next_row_cols, + ); // <<<< Receive challenges: 𝛾ⱼ, 𝛾ⱼ' let gammas = deep_composition_coefficients; @@ -3103,11 +3118,21 @@ pub trait IsStarkProver< #[cfg(feature = "instruments")] let round_3_dur = t_r3.elapsed(); - // >>>> Send values: tⱼ(zgᵏ) - let trace_ood_evaluations_columns = round_3_result.trace_ood_evaluations.columns(); - for col in trace_ood_evaluations_columns.iter() { - for elem in col.iter() { - transcript.append_field_element(elem); + // >>>> Send values: tⱼ(zgᵏ). g·z pruning: split the full OOD table into + // the current-row block (all columns) and the pruned next-row block + // (masked columns only), and absorb only the surviving values — the + // verifier absorbs the identical two blocks in the same order. + let ood_next_row_cols = air.trace_ood_next_row_columns(); + let (ood_block0, ood_block1) = crate::ood::split_ood_blocks( + &round_3_result.trace_ood_evaluations, + air.step_size(), + &ood_next_row_cols, + ); + for block in [&ood_block0, &ood_block1] { + for col in block.columns().iter() { + for elem in col.iter() { + transcript.append_field_element(elem); + } } } @@ -3161,8 +3186,9 @@ pub trait IsStarkProver< lde_trace_aux_merkle_root: round_1_result.aux.as_ref().map(|x| x.root), // For preprocessed tables: commitment to precomputed columns only lde_trace_precomputed_merkle_root: round_1_result.main.precomputed_root, - // tⱼ(zgᵏ) - trace_ood_evaluations: round_3_result.trace_ood_evaluations, + // tⱼ(zgᵏ): current-row block + pruned next-row block. + trace_ood_evaluations: ood_block0, + trace_ood_next_evaluations: ood_block1, // [H₁] and [H₂] composition_poly_root: round_2_result.composition_poly_root, // Hᵢ(z^N) diff --git a/crypto/stark/src/tests/bus_tests/soundness_tests.rs b/crypto/stark/src/tests/bus_tests/soundness_tests.rs index 652f5e87d..f14907a9d 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/crypto/stark/src/tests/bus_tests/soundness_tests.rs @@ -15,6 +15,7 @@ use crate::examples::multi_table_lookup::{ }; use crate::proof::options::ProofOptions; use crate::prover::{IsStarkProver, Prover}; +use crate::table::Table; use crate::test_utils::multi_prove_ram; use crate::trace::TraceTable; use crate::traits::AIR; @@ -827,6 +828,170 @@ fn test_tampered_acc_ood_evaluation() { ); } +/// A proof whose OOD trace-evaluation table has the wrong shape is rejected. +/// +/// The table's dimensions are a public function of the AIR (transition offsets +/// x step_size rows, main+aux columns), so the verifier derives the expected +/// shape from AIR metadata and refuses any proof whose table does not match -- +/// a malicious prover cannot reshape it (e.g. drop a column) to dodge a check. +#[test_log::test] +fn test_malformed_ood_table_shape_rejected() { + // Same valid trace as `test_tampered_acc_ood_evaluation`: CPU sends (5,3,8). + let mut cpu_trace = TraceTable::from_columns_main( + vec![ + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // add_flag + vec![FE::zero(); 4], // mul_flag + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + ], + 1, + ); + let mut add_trace = TraceTable::from_columns_main( + vec![ + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // multiplicity = 1 + ], + 1, + ); + let mut mul_trace = TraceTable::from_columns_main(vec![vec![FE::zero(); 4]; 4], 1); + + let proof_options = ProofOptions::default_test_options(); + let cpu_air = new_cpu_air_with_lookup(&proof_options); + let add_air = new_add_air_with_lookup(&proof_options); + let mul_air = new_mul_air_with_lookup(&proof_options); + + let air_trace_pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&cpu_air, &mut cpu_trace, &()), + (&add_air, &mut add_trace, &()), + (&mul_air, &mut mul_trace, &()), + ]; + + let mut multi_proof = + multi_prove_ram(air_trace_pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + + // Drop one column from the ADD table's OOD evaluations while keeping the + // table internally consistent (data length matches the new width), so the + // rejection is the AIR-shape guard, not an out-of-bounds panic. + let add_proof = &mut multi_proof.proofs[1]; + let old = &add_proof.trace_ood_evaluations; + assert!(old.width >= 1, "OOD table must have at least one column"); + let new_width = old.width - 1; + let mut new_data = Vec::with_capacity(new_width * old.height); + for row in 0..old.height { + let full = old.get_row(row); + new_data.extend_from_slice(&full[..new_width]); + } + add_proof.trace_ood_evaluations = Table::new(new_data, new_width); + + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &add_air, &mul_air]; + + assert!( + !Verifier::multi_verify( + &airs, + &multi_proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + ), + "Proof with a wrong-shaped OOD table must be rejected" + ); +} + +/// The transition window (`trace_ood_next_row_columns`) of a LogUp table is +/// exactly the accumulator column — the sole column read at the next row after +/// forward accumulation — expressed as a full-width `[main | aux]` index. +#[test_log::test] +fn test_trace_ood_next_row_columns_is_accumulator_only() { + let proof_options = ProofOptions::default_test_options(); + let add_air = new_add_air_with_lookup(&proof_options); + let (main, aux) = add_air.trace_layout(); + + // All ADD interactions are absorbed, so the single aux column is the + // accumulator; its full-width index is `main + (aux - 1)`. + let next = add_air.trace_ood_next_row_columns(); + assert_eq!(next, vec![main + (aux - 1)]); + + // Every returned index addresses a real column within the concatenated width. + for &c in &next { + assert!( + c < main + aux, + "next-row column {c} out of width {main}+{aux}" + ); + } +} + +/// The g·z pruning actually shrinks the proof: a LogUp table opens every column +/// at z (the current-row block) but only the accumulator at the next row. +#[test_log::test] +fn test_gz_pruning_reduces_next_row_openings() { + let mut cpu_trace = TraceTable::from_columns_main( + vec![ + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // add_flag + vec![FE::zero(); 4], // mul_flag + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + ], + 1, + ); + let mut add_trace = TraceTable::from_columns_main( + vec![ + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // multiplicity = 1 + ], + 1, + ); + let mut mul_trace = TraceTable::from_columns_main(vec![vec![FE::zero(); 4]; 4], 1); + + let proof_options = ProofOptions::default_test_options(); + let cpu_air = new_cpu_air_with_lookup(&proof_options); + let add_air = new_add_air_with_lookup(&proof_options); + let mul_air = new_mul_air_with_lookup(&proof_options); + + let air_trace_pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&cpu_air, &mut cpu_trace, &()), + (&add_air, &mut add_trace, &()), + (&mul_air, &mut mul_trace, &()), + ]; + + let multi_proof = + multi_prove_ram(air_trace_pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + + // ADD table: 4 main + 1 aux (accumulator). The current-row block opens all + // columns; the next-row block opens only the accumulator. + let add_proof = &multi_proof.proofs[1]; + let (main, aux) = add_air.trace_layout(); + assert_eq!(add_proof.trace_ood_evaluations.width, main + aux); + assert_eq!(add_proof.trace_ood_next_evaluations.width, 1); + assert!( + add_proof.trace_ood_next_evaluations.width < add_proof.trace_ood_evaluations.width, + "next-row OOD block must be pruned below the full width" + ); + + // The pruned proof still verifies. + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &add_air, &mul_air]; + assert!(Verifier::multi_verify( + &airs, + &multi_proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + )); +} + // ============================================================================= // Invalid bus public inputs // ============================================================================= diff --git a/crypto/stark/src/traits.rs b/crypto/stark/src/traits.rs index c28f831a2..0aec97a2a 100644 --- a/crypto/stark/src/traits.rs +++ b/crypto/stark/src/traits.rs @@ -198,6 +198,27 @@ pub trait AIR: Send + Sync { self.trace_layout().1 } + /// The full-width trace column indices that transition constraints read at + /// the *next* row (offset 1) — lambda_vm's fine-grained analogue of + /// Plonky3's transition window (a whole-row "does this AIR use the next + /// row?" flag). Only these columns need an OOD opening at `g·z`; every other + /// column is opened solely at `z`. The set is a public function of the AIR, + /// computed identically by prover and verifier, so the pruned OOD shape is + /// never taken from the (prover-controlled) proof. + /// + /// Indices are into the concatenated `[main | aux]` column space and must be + /// strictly less than `trace_layout().0 + trace_layout().1`. + /// + /// The default is **conservative**: every column is opened at the next row, + /// i.e. no pruning, matching the pre-pruning behaviour. An AIR that reads the + /// next row therefore stays correct without overriding. Override with the + /// exact read set only when you know which columns a transition constraint + /// references at offset 1 — returning too small a set is a soundness bug. + fn trace_ood_next_row_columns(&self) -> Vec { + let (main, aux) = self.trace_layout(); + (0..main + aux).collect() + } + fn composition_poly_degree_bound(&self, trace_length: usize) -> usize; /// Evaluates the transitions corresponding to an evaluation frame at the diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index fdee3d2ff..38663ad78 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -11,6 +11,7 @@ use crate::{ domain::new_verifier_domain, lookup::{LOGUP_CHALLENGE_ALPHA, LOGUP_NUM_CHALLENGES, compute_alpha_powers}, proof::stark::{DeepPolynomialOpening, MultiProof, PolynomialOpenings}, + table::Table, }; use crypto::{fiat_shamir::is_transcript::IsStarkTranscript, merkle_tree::proof::Proof}; #[cfg(not(feature = "test_fiat_shamir"))] @@ -107,6 +108,42 @@ pub trait IsStarkVerifier< { crate::profile_markers::STEP_VERIFY_CLAIMED_COMPOSITION_POLYNOMIAL }, >(); let trace_length = proof.trace_length; + + // Soundness (I3): both OOD blocks' shapes are a public function of the + // AIR, never of the (prover-controlled) proof. The current-row block + // opens every column over `step_size` rows; the next-row block opens only + // the transition-window columns over the remaining rows (and is empty + // when there are none). Reject any mismatch before using either block, so + // a malicious prover cannot reshape them to dodge a check or desync the + // frame reconstruction below. + let expected_ood_width = air.trace_layout().0 + air.num_auxiliary_rap_columns(); + let step_size = air.step_size(); + let num_eval_points = air.context().transition_offsets.len() * step_size; + let next_row_cols = air.trace_ood_next_row_columns(); + let expected_next_width = next_row_cols.len(); + let expected_next_height = if expected_next_width == 0 { + 0 + } else { + num_eval_points - step_size + }; + if proof.trace_ood_evaluations.width != expected_ood_width + || proof.trace_ood_evaluations.height != step_size + || proof.trace_ood_next_evaluations.width != expected_next_width + || proof.trace_ood_next_evaluations.height != expected_next_height + { + return false; + } + + // Reconstruct the full current+next-row OOD grid (surviving values placed, + // pruned next-row entries zero -- those are never read by any constraint). + let ood_full = crate::ood::reconstruct_ood_full( + &proof.trace_ood_evaluations, + &proof.trace_ood_next_evaluations, + num_eval_points, + step_size, + &next_row_cols, + ); + let boundary_constraints = air.boundary_constraints( &proof.public_inputs, &challenges.rap_challenges, @@ -167,8 +204,9 @@ pub trait IsStarkVerifier< .map(|((num, den), beta)| num * den * beta) .fold(FieldElement::::zero(), |acc, x| acc + x); - let num_main_trace_columns = - proof.trace_ood_evaluations.width - air.num_auxiliary_rap_columns(); + // Shape is AIR-derived (validated against the proof above), so use the + // AIR's main width directly rather than trusting the proof dimensions. + let num_main_trace_columns = main_trace_width; let logup_alpha_powers: Vec> = if challenges.rap_challenges.len() > LOGUP_CHALLENGE_ALPHA { @@ -191,8 +229,9 @@ pub trait IsStarkVerifier< None => FieldElement::zero(), }; - let ood_frame = - (proof.trace_ood_evaluations).into_frame(num_main_trace_columns, air.step_size()); + // Frame from the reconstructed full grid: the next-row step reads only + // its transition-window columns; the zero-filled remainder is never read. + let ood_frame = ood_full.into_frame(num_main_trace_columns, step_size); let transition_evaluation_context = TransitionEvaluationContext::new_verifier( &ood_frame, &challenges.rap_challenges, @@ -269,9 +308,27 @@ pub trait IsStarkVerifier< FieldElement: AsBytes + Sync + Send, { crate::profile_markers::step_marker::<{ crate::profile_markers::STEP_VERIFY_FRI }>(); + // g·z pruning: rebuild the full OOD grid from the two proof blocks so + // the DEEP reconstruction can skip pruned next-row openings. + let step_size = air.step_size(); + let num_eval_points = air.context().transition_offsets.len() * step_size; + let next_row_cols = air.trace_ood_next_row_columns(); + let ood_full = crate::ood::reconstruct_ood_full( + &proof.trace_ood_evaluations, + &proof.trace_ood_next_evaluations, + num_eval_points, + step_size, + &next_row_cols, + ); + let next_row_flags = crate::ood::next_row_col_flags(ood_full.width, &next_row_cols); let (deep_poly_evaluations, deep_poly_evaluations_sym) = match Self::reconstruct_deep_composition_poly_evaluations_for_all_queries( - challenges, domain, proof, + challenges, + domain, + proof, + &ood_full, + &next_row_flags, + step_size, ) { Some(pair) => pair, None => return false, @@ -610,10 +667,14 @@ pub trait IsStarkVerifier< openings_ok & terminal_ok } + #[allow(clippy::too_many_arguments)] fn reconstruct_deep_composition_poly_evaluations_for_all_queries( challenges: &Challenges, domain: &VerifierDomain, proof: &StarkProof, + ood_full: &Table, + next_row_flags: &[bool], + step_size: usize, ) -> Option> { let num_queries = challenges.iotas.len(); @@ -662,6 +723,9 @@ pub trait IsStarkVerifier< &lde_base, lde_aux, &opening.composition_poly.evaluations, + ood_full, + next_row_flags, + step_size, )?); // Mirror for the symmetric query point. @@ -686,11 +750,15 @@ pub trait IsStarkVerifier< &lde_base_sym, lde_aux_sym, &opening.composition_poly.evaluations_sym, + ood_full, + next_row_flags, + step_size, )?); } Some((deep_poly_evaluations, deep_poly_evaluations_sym)) } + #[allow(clippy::too_many_arguments)] fn reconstruct_deep_composition_poly_evaluation( proof: &StarkProof, evaluation_point: &FieldElement, @@ -699,9 +767,12 @@ pub trait IsStarkVerifier< lde_trace_base_evaluations: &[FieldElement], lde_trace_aux_evaluations: &[FieldElement], lde_composition_poly_parts_evaluation: &[FieldElement], + ood_full: &Table, + next_row_flags: &[bool], + step_size: usize, ) -> Option> { - let ood_evaluations_table_height = proof.trace_ood_evaluations.height; - let ood_evaluations_table_width = proof.trace_ood_evaluations.width; + let ood_evaluations_table_height = ood_full.height; + let ood_evaluations_table_width = ood_full.width; let trace_term_coeffs = &challenges.trace_term_coeffs; // Runtime guard: a malformed proof may supply opening evaluations whose @@ -733,10 +804,18 @@ pub trait IsStarkVerifier< let trace_term = (0..ood_evaluations_table_width) .zip(&challenges.trace_term_coeffs) .fold(FieldElement::zero(), |trace_terms, (col_idx, coeff_row)| { + let opened_next_row = next_row_flags[col_idx]; let trace_i = (0..ood_evaluations_table_height).zip(coeff_row).fold( FieldElement::zero(), |trace_t, (row_idx, coeff)| { - let ood_val = &proof.trace_ood_evaluations.get_row(row_idx)[col_idx]; + // g·z pruning: the next-row block opens only transition- + // window columns. Skip every other next-row opening — its + // coefficient is zero, so the term is vacuous, and skipping + // it is where the verifier/recursion cycle saving lands. + if row_idx >= step_size && !opened_next_row { + return trace_t; + } + let ood_val = &ood_full.get_row(row_idx)[col_idx]; // Stay in base when we can: F: IsSubFieldOf gives F - E -> E. let diff: FieldElement = if col_idx < num_base { &lde_trace_base_evaluations[col_idx] - ood_val @@ -1047,11 +1126,16 @@ pub trait IsStarkVerifier< &domain.coset_offset, ); - // <<<< Receive values: tⱼ(zgᵏ) - let trace_ood_evaluations_columns = proof.trace_ood_evaluations.columns(); - for col in trace_ood_evaluations_columns.iter() { - for elem in col.iter() { - transcript.append_field_element(elem); + // <<<< Receive values: tⱼ(zgᵏ). Absorb the two pruned OOD blocks in the + // same order the prover sent them (current-row block, then next-row block). + for block in [ + &proof.trace_ood_evaluations, + &proof.trace_ood_next_evaluations, + ] { + for col in block.columns().iter() { + for elem in col.iter() { + transcript.append_field_element(elem); + } } } // <<<< Receive value: Hᵢ(z^N) @@ -1064,8 +1148,15 @@ pub trait IsStarkVerifier< // =================================== let num_terms_composition_poly = proof.composition_poly_parts_ood_evaluation.len(); - let num_terms_trace = - air.context().transition_offsets.len() * air.step_size() * air.context().trace_columns; + let num_eval_points = air.context().transition_offsets.len() * air.step_size(); + let next_row_cols = air.trace_ood_next_row_columns(); + // Must match the prover's g·z pruning exactly (same AIR metadata). + let num_terms_trace = crate::ood::num_surviving_trace_openings( + air.context().trace_columns, + num_eval_points, + air.step_size(), + next_row_cols.len(), + ); let gamma = transcript.sample_field_element(); // <<<< Receive challenges: 𝛾, 𝛾' @@ -1074,12 +1165,16 @@ pub trait IsStarkVerifier< .take(num_terms_composition_poly + num_terms_trace) .collect(); - let trace_term_coeffs: Vec<_> = deep_composition_coefficients + let trace_term_powers: Vec<_> = deep_composition_coefficients .drain(..num_terms_trace) - .collect::>() - .chunks(air.context().transition_offsets.len() * air.step_size()) - .map(|chunk| chunk.to_vec()) .collect(); + let trace_term_coeffs = crate::ood::build_pruned_trace_term_coeffs( + &trace_term_powers, + air.context().trace_columns, + num_eval_points, + air.step_size(), + &next_row_cols, + ); // <<<< Receive challenges: 𝛾ⱼ, 𝛾ⱼ' let gammas = deep_composition_coefficients; From 9c5a4491c6f9f0fd5ea4d3d13646ef4a22253e72 Mon Sep 17 00:00:00 2001 From: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com> Date: Thu, 16 Jul 2026 12:27:01 -0300 Subject: [PATCH 3/7] fix(stark): review follow-ups for OOD pruning (docs, saturating_sub, hard assert) (#833) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * fix(stark): review nits for forward-accumulation OOD pruning - 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. * 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. * fix(stark): keep debug-only power-count check in build_pruned_trace_term_coeffs 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/logup_gpu.rs | 2 +- crypto/stark/src/lookup.rs | 10 +++++----- crypto/stark/src/ood.rs | 26 ++++++++++++++++++++------ crypto/stark/src/verifier.rs | 2 +- 4 files changed, 27 insertions(+), 13 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 cb498baf1..8a89ea727 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}; @@ -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}"); diff --git a/crypto/stark/src/ood.rs b/crypto/stark/src/ood.rs index 3572836a2..a779d7851 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. //! @@ -49,6 +50,12 @@ pub fn num_surviving_trace_openings( /// 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. 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`; /// 2. next-row block — for each masked column `j`, rows `step_size..num_eval_points`. @@ -226,7 +233,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 2ecb1991ad537f07b0e7c2ec75c870e6064c17de Mon Sep 17 00:00:00 2001 From: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com> Date: Thu, 16 Jul 2026 13:21:50 -0300 Subject: [PATCH 4/7] fix(verifier): validate next-row OOD block shape before transcript absorption (#835) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * fix(verifier): validate next-row OOD block shape before transcript absorption The next-row (g·z) OOD block (`trace_ood_next_evaluations`, new with OOD pruning) is absorbed into the transcript in Round 3 via `get_row` -- an unchecked `data[start..start + width]` slice -- BEFORE step_2's shape guard runs. rkyv bytecheck does not enforce `width * height == data.len()`, so a hostile archive advertising e.g. width=1000/height=1000 with a single data element panics the verifier out of bounds (guest trap / host crash) instead of being rejected as a false proof. Extend the Round-1 Phase A guard in `multi_verify_views` (where block0 is already validated) with the block1 shape check, derived from AIR metadata only and mirroring step_2 exactly (width, height, dimensions_consistent). Constant per-proof integer comparisons, no loop over data -- the verifier stays cycle-lean and never panics on a malformed proof. step_2's own post-absorption guard is left in place as defense-in-depth. Tests (soundness_tests.rs): a next-row block whose advertised dims disagree with its backing data is rejected, not panicked, on both the owned and archived paths. Confirmed the archived case panics in table.rs `get_row` without this guard. * refactor(verifier): fold both OOD shape checks into one helper step_2 and the pre-absorption guard in multi_verify_views each derived step_size, num_eval_points and the expected next-row dims, then ran the same three checks on the next-row block. Extract ood_blocks_well_formed and call it from both; the comment keeps only what the code cannot say (the Round 3 absorption ordering, and why the width check is load-bearing). The pre-absorption guard also still described the pre-split table: it accepted any nonzero height that was a multiple of step_size, which was correct when trace_ood_evaluations held the whole OOD grid. Since the current/next split, block0 is exactly step_size rows tall -- what step_2 already required. Both sites now use the stricter equality, which also subsumes the height-0 case as no AIR reports step_size 0. Net -23 lines; stark suite 195 passing. --- .../src/tests/bus_tests/soundness_tests.rs | 149 ++++++++++++++++++ crypto/stark/src/verifier.rs | 99 ++++++------ 2 files changed, 200 insertions(+), 48 deletions(-) diff --git a/crypto/stark/src/tests/bus_tests/soundness_tests.rs b/crypto/stark/src/tests/bus_tests/soundness_tests.rs index 7d8fab0ee..9cae880e1 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/crypto/stark/src/tests/bus_tests/soundness_tests.rs @@ -904,6 +904,155 @@ fn test_malformed_ood_table_shape_rejected() { ); } +/// A next-row (g·z) OOD block whose advertised dimensions disagree with its +/// backing data must be rejected, not panic. Unlike the current-row block +/// (`test_malformed_ood_table_shape_rejected`), the next-row block is absorbed +/// into the transcript via `get_row` in Round 3 BEFORE step_2's own shape guard +/// runs, so without a pre-absorption guard a lying shape is an out-of-bounds +/// slice panic rather than a `false` verdict. Owned path. +#[test_log::test] +fn test_malformed_ood_next_block_shape_rejected_owned() { + // Same valid trace as `test_malformed_ood_table_shape_rejected`. + let mut cpu_trace = TraceTable::from_columns_main( + vec![ + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // add_flag + vec![FE::zero(); 4], // mul_flag + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + ], + 1, + ); + let mut add_trace = TraceTable::from_columns_main( + vec![ + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // multiplicity = 1 + ], + 1, + ); + let mut mul_trace = TraceTable::from_columns_main(vec![vec![FE::zero(); 4]; 4], 1); + + let proof_options = ProofOptions::default_test_options(); + let cpu_air = new_cpu_air_with_lookup(&proof_options); + let add_air = new_add_air_with_lookup(&proof_options); + let mul_air = new_mul_air_with_lookup(&proof_options); + + let air_trace_pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&cpu_air, &mut cpu_trace, &()), + (&add_air, &mut add_trace, &()), + (&mul_air, &mut mul_trace, &()), + ]; + + let mut multi_proof = + multi_prove_ram(air_trace_pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + + // Forge the ADD table's next-row OOD block to advertise a far larger shape + // than its data backs (the canonical hostile archive: width/height huge, one + // data element). `get_row` would slice `data[0..width]` out of bounds during + // Round-3 absorption; the Phase A guard must reject before that. + let add_proof = &mut multi_proof.proofs[1]; + assert!( + add_proof.trace_ood_next_evaluations.width >= 1, + "next-row OOD block must open at least one column for this to be an OOB test" + ); + add_proof.trace_ood_next_evaluations.width = 1000; + add_proof.trace_ood_next_evaluations.height = 1000; + + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &add_air, &mul_air]; + + assert!( + !Verifier::multi_verify( + &airs, + &multi_proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + ), + "Proof with a lying next-row OOD block shape must be rejected, not panic" + ); +} + +/// The same attack through the rkyv-archived, read-in-place path — the real +/// attack surface, since the recursion guest verifies archived proofs. +/// `ArchivedTable::get_row` is the same unchecked slice, and rkyv's bytecheck +/// does NOT enforce `width * height == data.len()`, so a forged archive reaches +/// absorption. The Phase A guard must reject it; it must never panic. +#[test_log::test] +fn test_malformed_ood_next_block_shape_rejected_archived() { + // Same valid trace as the owned variant above. + let mut cpu_trace = TraceTable::from_columns_main( + vec![ + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // add_flag + vec![FE::zero(); 4], // mul_flag + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + ], + 1, + ); + let mut add_trace = TraceTable::from_columns_main( + vec![ + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // multiplicity = 1 + ], + 1, + ); + let mut mul_trace = TraceTable::from_columns_main(vec![vec![FE::zero(); 4]; 4], 1); + + let proof_options = ProofOptions::default_test_options(); + let cpu_air = new_cpu_air_with_lookup(&proof_options); + let add_air = new_add_air_with_lookup(&proof_options); + let mul_air = new_mul_air_with_lookup(&proof_options); + + let air_trace_pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&cpu_air, &mut cpu_trace, &()), + (&add_air, &mut add_trace, &()), + (&mul_air, &mut mul_trace, &()), + ]; + + let mut multi_proof = + multi_prove_ram(air_trace_pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + + // Forge before serialization: rkyv archives `data` (by its real length), + // `width`, and `height` as independent fields, so a width/height that + // disagree with the data survive `to_bytes` and surface on the archived + // table exactly as a hostile prover would craft them. + multi_proof.proofs[1].trace_ood_next_evaluations.width = 1000; + multi_proof.proofs[1].trace_ood_next_evaluations.height = 1000; + + let bytes = rkyv::to_bytes::(&multi_proof).unwrap(); + let archived = rkyv::access::< + crate::proof::stark::ArchivedMultiProof, + rkyv::rancor::Error, + >(&bytes) + .unwrap(); + + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &add_air, &mul_air]; + + assert!( + !Verifier::multi_verify_archived( + &airs, + &archived.proofs, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + ), + "Archived proof with a lying next-row OOD block shape must be rejected, not panic" + ); +} + /// The transition window (`trace_ood_next_row_columns`) of a LogUp table is /// exactly the accumulator column — the sole column read at the next row after /// forward accumulation — expressed as a full-width `[main | aux]` index. diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index 3fe80f5a2..c4a8eeb7d 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -125,6 +125,42 @@ pub trait IsStarkVerifier< /// Checks whether the purported evaluations of the composition polynomial parts and the trace /// polynomials at the out-of-domain challenge are consistent. /// See https://lambdaclass.github.io/lambdaworks/starks/protocol.html#step-2-verify-claimed-composition-polynomial + /// Soundness (I3): both OOD blocks' shapes are a public function of the AIR, + /// never of the (prover-controlled) proof. The current-row block opens every + /// column over `step_size` rows; the next-row block opens only the + /// transition-window columns over the remaining rows, and is empty when the + /// AIR reads none. + /// + /// Must run before Round 3, which absorbs the next-row block through + /// `get_row` — an unchecked `data[start..start + width]` slice. A hostile + /// archive whose advertised dims disagree with its data length would panic + /// there rather than be rejected as a false proof; `dimensions_consistent()` + /// closes that gap, which rkyv's bytecheck leaves open. + fn ood_blocks_well_formed( + air: &dyn AIR, + proof: StarkProofView<'_, Field, FieldExtension, PI>, + ) -> bool { + let step_size = air.step_size(); + let num_eval_points = air.context().transition_offsets.len() * step_size; + let expected_next_width = air.trace_ood_next_row_columns().len(); + let expected_next_height = if expected_next_width == 0 { + 0 + } else { + num_eval_points.saturating_sub(step_size) + }; + let current = proof.trace_ood_evaluations(); + let next = proof.trace_ood_next_evaluations(); + + // `height == step_size` also rejects a height-0 current block: every AIR + // reports `step_size >= 1`. + current.dimensions_consistent() + && current.width() == air.trace_layout().0 + air.num_auxiliary_rap_columns() + && current.height() == step_size + && next.dimensions_consistent() + && next.width() == expected_next_width + && next.height() == expected_next_height + } + fn step_2_verify_claimed_composition_polynomial( air: &dyn AIR, proof: StarkProofView<'_, Field, FieldExtension, PI>, @@ -142,33 +178,17 @@ pub trait IsStarkVerifier< .bus_table_contribution() .map(BusPublicInputs::from_contribution); - // Soundness (I3): both OOD blocks' shapes are a public function of the - // AIR, never of the (prover-controlled) proof. The current-row block - // opens every column over `step_size` rows; the next-row block opens only - // the transition-window columns over the remaining rows (and is empty - // when there are none). Reject any mismatch (including an archive whose - // advertised dims disagree with its data length) before using either - // block, so a malicious prover cannot reshape them to dodge a check or - // desync the frame reconstruction below. + // Reject either OOD block whose shape disagrees with the AIR before + // reading it, so a malicious prover cannot reshape them to dodge a check + // or desync the frame reconstruction below. + if !Self::ood_blocks_well_formed(air, proof) { + return false; + } let step_size = air.step_size(); let num_eval_points = air.context().transition_offsets.len() * step_size; let next_row_cols = air.trace_ood_next_row_columns(); - let expected_next_width = next_row_cols.len(); - let expected_next_height = if expected_next_width == 0 { - 0 - } else { - num_eval_points.saturating_sub(step_size) - }; let ood_current = proof.trace_ood_evaluations(); let ood_next = proof.trace_ood_next_evaluations(); - if ood_current.height() != step_size - || !ood_current.dimensions_consistent() - || ood_next.width() != expected_next_width - || ood_next.height() != expected_next_height - || !ood_next.dimensions_consistent() - { - return false; - } // Reconstruct the full current+next-row OOD grid (surviving values placed, // pruned next-row entries zero -- those are never read by any constraint). @@ -1017,32 +1037,15 @@ pub trait IsStarkVerifier< { return false; } - // The archive is read in place without validation; reject an OOD - // table whose advertised dimensions disagree with its data length, - // has no rows, whose width doesn't match the AIR's column layout, or - // whose height isn't a whole number of AIR steps (which `into_frame` - // below only `debug_assert!`s, not checks) — all before any row - // access indexes into it. - // - // The width check is load-bearing and prevents two distinct faults: - // (a) the AIR-derived column index `main_trace_width + c.col` in - // `step_2_verify_claimed_composition_polynomial` indexing past a - // too-narrow OOD row (a release-mode out-of-bounds panic), and - // (b) a width-0 table, whose `width * height == 0 == data.len()` - // satisfies `dimensions_consistent()` for an arbitrary advertised - // height and would otherwise slip through this guard entirely. - // An honest proof always commits exactly `main_trace_width + num_aux` - // OOD columns (the same quantities `column_idx` and the `checked_sub` - // boundary use), so exact equality never rejects a valid proof. - let trace_ood_evaluations = proof.trace_ood_evaluations(); - let expected_ood_width = air.trace_layout().0 + air.num_auxiliary_rap_columns(); - if !trace_ood_evaluations.dimensions_consistent() - || trace_ood_evaluations.height() == 0 - || trace_ood_evaluations.width() != expected_ood_width - || !trace_ood_evaluations - .height() - .is_multiple_of(air.step_size()) - { + // The archive is read in place without validation, so both OOD blocks + // must be shape-checked here — before Round 3 absorbs the next-row + // block and before any row access indexes into either. The width check + // is load-bearing: it stops the AIR-derived column index + // `main_trace_width + c.col` in `step_2_verify_claimed_composition_polynomial` + // from indexing past a too-narrow OOD row, and it rejects a width-0 + // table, whose `width * height == 0 == data.len()` would otherwise + // satisfy `dimensions_consistent()` for any advertised height. + if !Self::ood_blocks_well_formed(*air, proof) { return false; } if air.is_preprocessed() { From c9a9244e1bb19206c6cdd41425b246982e9bb8dd Mon Sep 17 00:00:00 2001 From: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com> Date: Thu, 16 Jul 2026 14:40:55 -0300 Subject: [PATCH 5/7] refactor(stark): direct scatter in reconstruct_ood_full (#838) The next-row fill loop scanned next_row_cols per output cell (O(width x mask_width) per row, degrading toward O(width^2) for AIRs using the conservative all-columns next-row window). Replace it with a zero-fill followed by a direct scatter of each masked value into its column. Preserves the documented never-panic contract (bounds-checked reads via .get, malformed/short archives yield zero-filled cells) and silently ignores out-of-range indices in next_row_cols. The scatter is last-write-wins on duplicate indices where the old scan was first-match-wins; both agree in practice because split_ood_blocks never emits duplicate indices with differing values, but the two are not bit-identical for a pathologically malformed next_row_cols. Adds unit tests for out-of-range next_row_cols indices and a short/truncated next_block, both exercising the no-panic path. --- crypto/stark/src/ood.rs | 52 ++++++++++++++++++++++++++++++----------- 1 file changed, 38 insertions(+), 14 deletions(-) diff --git a/crypto/stark/src/ood.rs b/crypto/stark/src/ood.rs index a779d7851..56bb84c48 100644 --- a/crypto/stark/src/ood.rs +++ b/crypto/stark/src/ood.rs @@ -159,21 +159,23 @@ pub fn reconstruct_ood_full( } } - for r in step_size..num_eval_points { - let next_row = r - step_size; - for c in 0..width { - let mut val = FieldElement::::zero(); - if mask_width > 0 { - for (m, &mc) in next_row_cols.iter().enumerate() { - if mc == c { - if let Some(v) = next_block.get(next_row * mask_width + m) { - val = v.clone(); - } - break; - } - } + // Zero-fill the next-row rows, then scatter the surviving masked values + // directly into their columns instead of scanning `next_row_cols` per + // cell. `.max` keeps the current-row block intact even if + // `num_eval_points < step_size` (defensive only: for a well-formed AIR + // `num_eval_points` is always a positive multiple of `step_size`). + data.resize( + data.len().max(num_eval_points * width), + FieldElement::::zero(), + ); + for next_row in 0..num_eval_points.saturating_sub(step_size) { + let row_base = (step_size + next_row) * width; + for (m, &mc) in next_row_cols.iter().enumerate() { + if mc < width + && let Some(v) = next_block.get(next_row * mask_width + m) + { + data[row_base + mc] = v.clone(); } - data.push(val); } } @@ -245,6 +247,28 @@ mod tests { assert_eq!(recon.get_row(1), &[Fe::zero(), Fe::zero()]); } + #[test] + fn out_of_range_next_row_col_is_ignored_not_panicking() { + // width = 3, but next_row_cols advertises column 5 -- out of range. + let current_block = vec![fe(1), fe(2), fe(3)]; + let next_block = vec![fe(99)]; // would-be value for the bogus column + let recon = reconstruct_ood_full(¤t_block, 3, &next_block, 2, 1, &[5]); + assert_eq!(recon.get_row(0), &[fe(1), fe(2), fe(3)]); + assert_eq!(recon.get_row(1), &[Fe::zero(), Fe::zero(), Fe::zero()]); + } + + #[test] + fn short_next_block_leaves_missing_cells_zero_not_panicking() { + // width = 3, 3 eval points (step_size 1) => 2 next rows, mask = {0, 2} + // so the mask implies 4 next-row values, but next_block only has 1. + let current_block = vec![fe(1), fe(2), fe(3)]; + let next_block = vec![fe(99)]; + let recon = reconstruct_ood_full(¤t_block, 3, &next_block, 3, 1, &[0, 2]); + assert_eq!(recon.get_row(0), &[fe(1), fe(2), fe(3)]); + assert_eq!(recon.get_row(1), &[fe(99), Fe::zero(), Fe::zero()]); // only present value scattered + assert_eq!(recon.get_row(2), &[Fe::zero(), Fe::zero(), Fe::zero()]); // fully missing -> zero + } + #[test] fn pruned_coeffs_are_zero_off_the_window() { // 4 surviving powers for W=3, num_eval_points=2, mask={1}. From 18ef1fae3c18529e54057a65002432c9c2a473e0 Mon Sep 17 00:00:00 2001 From: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com> Date: Thu, 16 Jul 2026 14:42:37 -0300 Subject: [PATCH 6/7] refactor(stark): compute OOD pruning layout once and thread it through verify (#837) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR #823 added g·z OOD trace-opening pruning. The layout metadata and the full-grid reconstruction were then derived redundantly at several sites that had to be kept in lockstep by hand: - `num_eval_points`/`next_row_cols` + `num_surviving_trace_openings` + `build_pruned_trace_term_coeffs` recomputed in the verifier round-4 transcript replay and prover round-4. - `reconstruct_ood_full` built TWICE per verify — once in `step_2` (after the `ood_blocks_well_formed` shape guard) and again, unguarded, in `step_3`, which silently relied on `step_2`/Phase A having validated the shapes first. - `split_ood_blocks` args recomputed in prover round-3. Introduce `ood::OodLayout`, a small struct bundling the AIR-derived layout (`num_total_cols`, `num_eval_points`, `step_size`, `next_row_cols`) with methods that forward to the existing free functions (`num_surviving`, `flags`, `build_trace_term_coeffs`, `split_full`, `reconstruct_full`, plus `expected_next_{width,height}` and a `next_row_cols`/`step_size` accessor). The free functions and their pub API are unchanged; the struct only wraps them and adds no new arithmetic. It stays decoupled from the AIR trait — a one-line `ood_layout` helper per crate reads the four raw values and hands them to `OodLayout::new`. `verify_rounds_2_to_4` now builds the layout, runs the `ood_blocks_well_formed` guard, reconstructs the full grid ONCE, and passes borrows into `step_2` and `step_3` (which now take `ood_full`/`step_size`, and `ood_full`/`next_row_cols`/ `step_size` respectively — extending the precedent #826 set when it threaded these through the fused `reconstruct_deep_composition_poly_evaluations_for_all_queries` and `compute_query_invariant_deep_terms`). The guard runs before both steps (same check, same `return false` semantics, same "Composition Polynomial verification failed" log on failure, same order relative to grinding), removing the hidden step_2-before-step_3 ordering dependency and doing one reconstruction instead of two — a small guest-cycle saving on the recursion verifier. The transcript-replay and prover metadata sites derive from the same struct. `ood_blocks_well_formed` is left as-is: its width check uses `trace_layout().0 + num_auxiliary_rap_columns()` (an overridable metadata source I cannot prove equals `trace_columns`), so folding it fully onto OodLayout is not provably behavior-preserving, and a partial fold would force a layout construction in the Phase A hot loop for no net simplification. Zero behavior change: Fiat-Shamir absorption/sampling order is untouched; the metadata sites keep using `trace_columns`; the DEEP reconstruction keeps reading `next_row_cols` on the reconstructed grid exactly as before. The verifier gains no new panics/asserts/unwraps and every `return false` path is preserved; net work strictly decreases (one reconstruction instead of two, no added allocations). Validated with the full `cargo test --release -p stark` suite (196 passed, incl. a new `OodLayout`-delegates-to-free-functions test) and `make lint` (fmt + all four clippy passes incl. cuda) at exit 0. --- crypto/stark/src/ood.rs | 174 +++++++++++++++++++++++++++++++++++ crypto/stark/src/prover.rs | 43 ++++----- crypto/stark/src/verifier.rs | 132 +++++++++++++++----------- 3 files changed, 272 insertions(+), 77 deletions(-) diff --git a/crypto/stark/src/ood.rs b/crypto/stark/src/ood.rs index 56bb84c48..d5f17d159 100644 --- a/crypto/stark/src/ood.rs +++ b/crypto/stark/src/ood.rs @@ -182,6 +182,135 @@ pub fn reconstruct_ood_full( Table::new(data, width) } +/// The pruned-OOD trace-opening layout, derived once from public AIR shape +/// metadata and shared by every site that used to recompute it. Every field is +/// a pure function of the AIR (`trace_columns`, `step_size`, the +/// transition-offset count, and the next-row column set), so the prover and the +/// verifier build the identical layout without trusting any proof dimension +/// (invariant I3). This struct only bundles those values and forwards to the +/// free functions above; it adds no new arithmetic. +/// +/// It stays decoupled from the `AIR` trait: callers that have an AIR in scope +/// read the four raw values once (see the `ood_layout` helpers in the verifier +/// and prover) and pass them to [`OodLayout::new`]. +#[derive(Clone, Debug)] +pub struct OodLayout { + /// Total trace columns (`main + aux`), i.e. the full current-row block width. + num_total_cols: usize, + /// Rows in the full OOD grid: `num_transition_offsets * step_size`. + num_eval_points: usize, + /// Rows per offset block. + step_size: usize, + /// Full-width column indices opened at the next row (the transition window). + next_row_cols: Vec, +} + +impl OodLayout { + /// Build from raw AIR-metadata values. `num_eval_points` is + /// `num_transition_offsets * step_size`; keeping it a plain argument lets the + /// single AIR-reading expression live in the verifier/prover, not here. + pub fn new( + num_total_cols: usize, + num_eval_points: usize, + step_size: usize, + next_row_cols: Vec, + ) -> Self { + Self { + num_total_cols, + num_eval_points, + step_size, + next_row_cols, + } + } + + /// Rows per offset block. + pub fn step_size(&self) -> usize { + self.step_size + } + + /// Full-width column indices opened at the next row (the transition window), + /// in the order the DEEP reconstruction sums them. + pub fn next_row_cols(&self) -> &[usize] { + &self.next_row_cols + } + + /// Width of the pruned next-row proof block: one column per transition-window + /// column (the current-row block always keeps every column). + pub fn expected_next_width(&self) -> usize { + self.next_row_cols.len() + } + + /// Height of the pruned next-row proof block: the non-current rows, or 0 when + /// the AIR reads no next-row column (then the block is empty). + pub fn expected_next_height(&self) -> usize { + if self.next_row_cols.is_empty() { + 0 + } else { + self.num_eval_points.saturating_sub(self.step_size) + } + } + + /// Number of surviving trace openings under g·z pruning; see + /// [`num_surviving_trace_openings`]. + pub fn num_surviving(&self) -> usize { + num_surviving_trace_openings( + self.num_total_cols, + self.num_eval_points, + self.step_size, + self.next_row_cols.len(), + ) + } + + /// Per-column next-row open flags for a table of `grid_width` columns; see + /// [`next_row_col_flags`]. The width is that of the table being indexed — the + /// reconstructed OOD grid, whose width is the current-row block's width — and + /// need not equal `num_total_cols`; the free function ignores any next-row + /// index that falls outside `grid_width`. + pub fn flags(&self, grid_width: usize) -> Vec { + next_row_col_flags(grid_width, &self.next_row_cols) + } + + /// Build the rectangular DEEP trace-term coefficient grid; see + /// [`build_pruned_trace_term_coeffs`]. + pub fn build_trace_term_coeffs( + &self, + powers: &[FieldElement], + ) -> Vec>> { + build_pruned_trace_term_coeffs( + powers, + self.num_total_cols, + self.num_eval_points, + self.step_size, + &self.next_row_cols, + ) + } + + /// Split a full prover OOD table into the two pruned proof blocks; see + /// [`split_ood_blocks`]. + pub fn split_full(&self, full: &Table) -> (Table, Table) { + split_ood_blocks(full, self.step_size, &self.next_row_cols) + } + + /// Rebuild the full OOD grid from the two pruned proof blocks; see + /// [`reconstruct_ood_full`]. `current_width` is the (proof-supplied) + /// current-row block width and becomes the reconstructed grid's width. + pub fn reconstruct_full( + &self, + current_block: &[FieldElement], + current_width: usize, + next_block: &[FieldElement], + ) -> Table { + reconstruct_ood_full( + current_block, + current_width, + next_block, + self.num_eval_points, + self.step_size, + &self.next_row_cols, + ) + } +} + #[cfg(test)] mod tests { use super::*; @@ -282,4 +411,49 @@ mod tests { assert_eq!(coeffs[0][1], Fe::zero()); // pruned assert_eq!(coeffs[2][1], Fe::zero()); // pruned } + + #[test] + fn ood_layout_delegates_to_free_functions() { + // W=3 cols, num_eval_points=2 (step_size 1, 2 offsets), next-row mask {1}. + let layout = OodLayout::new(3, 2, 1, vec![1]); + + assert_eq!(layout.step_size(), 1); + assert_eq!(layout.expected_next_width(), 1); + assert_eq!(layout.expected_next_height(), 1); + assert_eq!( + layout.num_surviving(), + num_surviving_trace_openings(3, 2, 1, 1) + ); + + // Empty next-row mask => empty next-row block. + let empty = OodLayout::new(3, 2, 1, vec![]); + assert_eq!(empty.expected_next_width(), 0); + assert_eq!(empty.expected_next_height(), 0); + + // flags(), build_trace_term_coeffs(), split_full() and reconstruct_full() + // must be bit-identical to the free functions they forward to. + assert_eq!(layout.flags(3), next_row_col_flags(3, &[1])); + let powers: Vec = (1..=4).map(fe).collect(); + assert_eq!( + layout.build_trace_term_coeffs(&powers), + build_pruned_trace_term_coeffs(&powers, 3, 2, 1, &[1]) + ); + + let full = Table::new(vec![fe(10), fe(11), fe(12), fe(20), fe(21), fe(22)], 3); + let (lb0, lb1) = layout.split_full(&full); + let (fb0, fb1) = split_ood_blocks(&full, 1, &[1]); + assert_eq!(lb0.row_major_data(), fb0.row_major_data()); + assert_eq!(lb1.row_major_data(), fb1.row_major_data()); + + let recon = layout.reconstruct_full(lb0.row_major_data(), lb0.width, lb1.row_major_data()); + let free_recon = reconstruct_ood_full( + fb0.row_major_data(), + fb0.width, + fb1.row_major_data(), + 2, + 1, + &[1], + ); + assert_eq!(recon.row_major_data(), free_recon.row_major_data()); + } } diff --git a/crypto/stark/src/prover.rs b/crypto/stark/src/prover.rs index 69fab1619..8c44c42a9 100644 --- a/crypto/stark/src/prover.rs +++ b/crypto/stark/src/prover.rs @@ -1438,6 +1438,23 @@ pub trait IsStarkProver< } } + /// The pruned-OOD layout for this AIR — the single place in the prover that + /// reads the shape metadata (`trace_columns`, `step_size`, the + /// transition-offset count, and the next-row column set). The round-3 block + /// split and the round-4 DEEP-coefficient assignment both derive from the + /// returned [`crate::ood::OodLayout`], which the verifier rebuilds identically + /// (invariant I3). + fn ood_layout( + air: &dyn AIR, + ) -> crate::ood::OodLayout { + crate::ood::OodLayout::new( + air.context().trace_columns, + air.context().transition_offsets.len() * air.step_size(), + air.step_size(), + air.trace_ood_next_row_columns(), + ) + } + /// Returns the result of the fourth round of the STARK Prove protocol. fn round_4_compute_and_run_fri_on_the_deep_composition_polynomial( air: &dyn AIR, @@ -1458,16 +1475,10 @@ pub trait IsStarkProver< let gamma = transcript.sample_field_element(); let n_terms_composition_poly = round_2_result.lde_composition_poly_evaluations.len(); - let num_eval_points = air.context().transition_offsets.len() * air.step_size(); - let next_row_cols = air.trace_ood_next_row_columns(); // g·z pruning: only the current-row block (all columns) plus the masked // next-row columns get an opening / DEEP coefficient. - let num_terms_trace = crate::ood::num_surviving_trace_openings( - air.context().trace_columns, - num_eval_points, - air.step_size(), - next_row_cols.len(), - ); + let layout = Self::ood_layout(air); + let num_terms_trace = layout.num_surviving(); // <<<< Receive challenges: 𝛾, 𝛾' let mut deep_composition_coefficients: Vec<_> = @@ -1481,13 +1492,7 @@ pub trait IsStarkProver< // Rectangular W×num_eval_points grid with the sampled powers at surviving // positions and zeros at pruned next-row positions, so the DEEP loop // below (and the GPU path) stay unchanged — zero-coefficient terms vanish. - let trace_term_coeffs = crate::ood::build_pruned_trace_term_coeffs( - &trace_term_powers, - air.context().trace_columns, - num_eval_points, - air.step_size(), - &next_row_cols, - ); + let trace_term_coeffs = layout.build_trace_term_coeffs(&trace_term_powers); // <<<< Receive challenges: 𝛾ⱼ, 𝛾ⱼ' let gammas = deep_composition_coefficients; @@ -3122,12 +3127,8 @@ pub trait IsStarkProver< // the current-row block (all columns) and the pruned next-row block // (masked columns only), and absorb only the surviving values — the // verifier absorbs the identical two blocks in the same order. - let ood_next_row_cols = air.trace_ood_next_row_columns(); - let (ood_block0, ood_block1) = crate::ood::split_ood_blocks( - &round_3_result.trace_ood_evaluations, - air.step_size(), - &ood_next_row_cols, - ); + let (ood_block0, ood_block1) = + Self::ood_layout(air).split_full(&round_3_result.trace_ood_evaluations); for block in [&ood_block0, &ood_block1] { for col in block.columns().iter() { for elem in col.iter() { diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index be0313bd5..ae26afbe9 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -141,6 +141,22 @@ pub trait IsStarkVerifier< .collect::>() } + /// The pruned-OOD layout for this AIR — the single place in the verifier that + /// reads the shape metadata (`trace_columns`, `step_size`, the + /// transition-offset count, and the next-row column set). Everything that used + /// to recompute these values now derives them from the returned + /// [`crate::ood::OodLayout`]. Pure AIR metadata, never a proof dimension. + fn ood_layout( + air: &dyn AIR, + ) -> crate::ood::OodLayout { + crate::ood::OodLayout::new( + air.context().trace_columns, + air.context().transition_offsets.len() * air.step_size(), + air.step_size(), + air.trace_ood_next_row_columns(), + ) + } + /// Checks whether the purported evaluations of the composition polynomial parts and the trace /// polynomials at the out-of-domain challenge are consistent. /// See https://lambdaclass.github.io/lambdaworks/starks/protocol.html#step-2-verify-claimed-composition-polynomial @@ -186,6 +202,13 @@ pub trait IsStarkVerifier< public_inputs: &PI, domain: &VerifierDomain, challenges: &Challenges, + // The full current+next-row OOD grid, shape-checked and reconstructed once + // by the caller (after `ood_blocks_well_formed`) and shared with + // `step_3_verify_fri`. Its pruned next-row entries are zero — those are + // never read by any constraint. `step_size` accompanies it for the frame + // split below. + ood_full: &Table, + step_size: usize, ) -> bool { crate::profile_markers::step_marker::< { crate::profile_markers::STEP_VERIFY_CLAIMED_COMPOSITION_POLYNOMIAL }, @@ -197,29 +220,6 @@ pub trait IsStarkVerifier< .bus_table_contribution() .map(BusPublicInputs::from_contribution); - // Reject either OOD block whose shape disagrees with the AIR before - // reading it, so a malicious prover cannot reshape them to dodge a check - // or desync the frame reconstruction below. - if !Self::ood_blocks_well_formed(air, proof) { - return false; - } - let step_size = air.step_size(); - let num_eval_points = air.context().transition_offsets.len() * step_size; - let next_row_cols = air.trace_ood_next_row_columns(); - let ood_current = proof.trace_ood_evaluations(); - let ood_next = proof.trace_ood_next_evaluations(); - - // Reconstruct the full current+next-row OOD grid (surviving values placed, - // pruned next-row entries zero -- those are never read by any constraint). - let ood_full = crate::ood::reconstruct_ood_full( - ood_current.row_major_data(), - ood_current.width(), - ood_next.row_major_data(), - num_eval_points, - step_size, - &next_row_cols, - ); - let boundary_constraints = air.boundary_constraints( public_inputs, &challenges.rap_challenges, @@ -318,7 +318,7 @@ pub trait IsStarkVerifier< // its transition-window columns; the zero-filled remainder is never read. // `into_frame` lives on the borrowed table view, so wrap the owned grid. let ood_frame = - StarkTableView::Owned(&ood_full).into_frame(num_main_trace_columns, step_size); + StarkTableView::Owned(ood_full).into_frame(num_main_trace_columns, step_size); let transition_evaluation_context = TransitionEvaluationContext::new_verifier( &ood_frame, &challenges.rap_challenges, @@ -389,33 +389,25 @@ pub trait IsStarkVerifier< proof: StarkProofView<'_, Field, FieldExtension, PI>, domain: &VerifierDomain, challenges: &Challenges, + // g·z pruning: the full OOD grid (reconstructed once by the caller and + // shared with `step_2`) plus the transition-window column indices, so the + // DEEP reconstruction can skip pruned next-row openings. + ood_full: &Table, + next_row_cols: &[usize], + step_size: usize, ) -> bool where FieldElement: AsBytes + Sync + Send, FieldElement: AsBytes + Sync + Send, { crate::profile_markers::step_marker::<{ crate::profile_markers::STEP_VERIFY_FRI }>(); - // g·z pruning: rebuild the full OOD grid from the two proof blocks so - // the DEEP reconstruction can skip pruned next-row openings. - let step_size = air.step_size(); - let num_eval_points = air.context().transition_offsets.len() * step_size; - let next_row_cols = air.trace_ood_next_row_columns(); - let ood_current = proof.trace_ood_evaluations(); - let ood_full = crate::ood::reconstruct_ood_full( - ood_current.row_major_data(), - ood_current.width(), - proof.trace_ood_next_evaluations().row_major_data(), - num_eval_points, - step_size, - &next_row_cols, - ); let (deep_poly_evaluations, deep_poly_evaluations_sym) = match Self::reconstruct_deep_composition_poly_evaluations_for_all_queries( challenges, domain, proof, - &ood_full, - &next_row_cols, + ood_full, + next_row_cols, step_size, ) { Some(pair) => pair, @@ -1368,6 +1360,7 @@ pub trait IsStarkVerifier< domain: &VerifierDomain, transcript: &mut impl IsStarkTranscript, rap_challenges: Vec>, + layout: &crate::ood::OodLayout, ) -> Challenges where FieldElement: AsBytes, @@ -1442,17 +1435,10 @@ pub trait IsStarkVerifier< // =================================== let num_terms_composition_poly = proof.composition_poly_parts_ood_evaluation().len(); - let num_eval_points = air.context().transition_offsets.len() * air.step_size(); - let next_row_cols = air.trace_ood_next_row_columns(); // Must match the prover's g·z pruning exactly (same AIR metadata): the // current-row block opens every column, the next-row block only the // transition-window columns. - let num_terms_trace = crate::ood::num_surviving_trace_openings( - air.context().trace_columns, - num_eval_points, - air.step_size(), - next_row_cols.len(), - ); + let num_terms_trace = layout.num_surviving(); let gamma = transcript.sample_field_element(); // <<<< Receive challenges: 𝛾, 𝛾' @@ -1464,13 +1450,7 @@ pub trait IsStarkVerifier< let trace_term_powers: Vec<_> = deep_composition_coefficients .drain(..num_terms_trace) .collect(); - let trace_term_coeffs = crate::ood::build_pruned_trace_term_coeffs( - &trace_term_powers, - air.context().trace_columns, - num_eval_points, - air.step_size(), - &next_row_cols, - ); + let trace_term_coeffs = layout.build_trace_term_coeffs(&trace_term_powers); // <<<< Receive challenges: 𝛾ⱼ, 𝛾ⱼ' let gammas = deep_composition_coefficients; @@ -1552,6 +1532,12 @@ pub trait IsStarkVerifier< return false; } + // The pruned-OOD layout, read from the AIR once and shared by the round-4 + // challenge replay, the block-shape guard, the single grid reconstruction, + // and both verify steps below — one reconstruction instead of the previous + // two, and no chance of the sites drifting apart. + let layout = Self::ood_layout(air); + #[cfg(feature = "instruments")] println!("- Started step 1: Recover challenges"); #[cfg(feature = "instruments")] @@ -1564,6 +1550,7 @@ pub trait IsStarkVerifier< &domain, transcript, rap_challenges, + &layout, ); // verify grinding @@ -1590,12 +1577,37 @@ pub trait IsStarkVerifier< #[cfg(feature = "instruments")] let timer2 = Instant::now(); + // Reject either OOD block whose shape disagrees with the AIR before + // reconstructing or using it, so a malicious prover cannot reshape them + // to dodge a check or desync the frame reconstruction. This guard used to + // run at the top of `step_2`; `step_3` silently relied on it. Now it runs + // once here, before both steps, and the full grid is reconstructed once + // and shared with them (one reconstruction instead of two). The Phase A + // loop in `multi_verify_views` runs the same guard even earlier, before + // Round 3 absorbs the next-row block. + if !Self::ood_blocks_well_formed(air, proof) { + #[cfg(not(feature = "test_fiat_shamir"))] + error!("Composition Polynomial verification failed"); + return false; + } + let ood_current = proof.trace_ood_evaluations(); + let ood_next = proof.trace_ood_next_evaluations(); + // Full current+next-row OOD grid (surviving values placed, pruned next-row + // entries zero — those are never read by any constraint). + let ood_full = layout.reconstruct_full( + ood_current.row_major_data(), + ood_current.width(), + ood_next.row_major_data(), + ); + if !Self::step_2_verify_claimed_composition_polynomial( air, proof, public_inputs, &domain, &challenges, + &ood_full, + layout.step_size(), ) { #[cfg(not(feature = "test_fiat_shamir"))] error!("Composition Polynomial verification failed"); @@ -1611,7 +1623,15 @@ pub trait IsStarkVerifier< #[cfg(feature = "instruments")] let timer3 = Instant::now(); - if !Self::step_3_verify_fri(air, proof, &domain, &challenges) { + if !Self::step_3_verify_fri( + air, + proof, + &domain, + &challenges, + &ood_full, + layout.next_row_cols(), + layout.step_size(), + ) { #[cfg(not(feature = "test_fiat_shamir"))] error!("FRI verification failed"); return false; From 2cab554ed65698dd8e6a4ce6fd69687d25dc00f6 Mon Sep 17 00:00:00 2001 From: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com> Date: Thu, 16 Jul 2026 14:43:14 -0300 Subject: [PATCH 7/7] test(stark): cross-check OOD transition window against captured constraint IR (#836) --- crypto/stark/src/constraint_ir/ir.rs | 48 +++++++ .../src/tests/bus_tests/soundness_tests.rs | 127 ++++++++++++++++++ prover/src/tests/mod.rs | 2 + prover/src/tests/ood_window_ir_tests.rs | 117 ++++++++++++++++ 4 files changed, 294 insertions(+) create mode 100644 prover/src/tests/ood_window_ir_tests.rs diff --git a/crypto/stark/src/constraint_ir/ir.rs b/crypto/stark/src/constraint_ir/ir.rs index cc770fd06..22857be2c 100644 --- a/crypto/stark/src/constraint_ir/ir.rs +++ b/crypto/stark/src/constraint_ir/ir.rs @@ -111,4 +111,52 @@ impl ConstraintProgram { pub fn is_empty(&self) -> bool { self.nodes.is_empty() } + + /// The full-width `[main | aux]` trace-column indices that some transition + /// constraint in this program reads at the *next* row (frame offset ≥ 1), + /// sorted and deduplicated. A main-trace read maps to its column index; an + /// aux-trace read maps to `main_width + col` — the same concatenated + /// indexing the verifier's OOD frame uses (main columns first, then aux; + /// see [`crate::ood`] and the frame reconstruction in the verifier). + /// + /// This is the ground truth an AIR's + /// [`crate::traits::AIR::trace_ood_next_row_columns`] declaration must + /// cover: the verifier opens every trace column at `z` but prunes the `g·z` + /// (next-row) opening down to the *declared* set, reconstructing ZERO for + /// any column outside it. So every column this method returns that the + /// declaration omits is silently read as zero at the next row — a + /// soundness/completeness bug. Deriving the read set from the captured IR + /// lets a test cross-check the hand-maintained declaration instead of + /// trusting it. + /// + /// A leaf is counted as a next-row read when its frame `offset` (or its + /// intra-step `row`, always 0 in the single-row-step capture path) is + /// nonzero, so the derivation can never *under*-report a next-row read — the + /// dangerous direction for the `derived ⊆ declared` check that guards + /// soundness. + /// + /// For tests and tooling only: it walks the captured [`ConstraintProgram`], + /// which the verify/recursion path never materializes. + pub fn next_row_trace_reads(&self, main_width: usize) -> Vec { + let mut cols: Vec = self + .nodes + .iter() + .filter_map(|op| match *op { + Op::Var { + main, + offset, + row, + col, + } if offset >= 1 || row >= 1 => Some(if main { + col as usize + } else { + main_width + col as usize + }), + _ => None, + }) + .collect(); + cols.sort_unstable(); + cols.dedup(); + cols + } } diff --git a/crypto/stark/src/tests/bus_tests/soundness_tests.rs b/crypto/stark/src/tests/bus_tests/soundness_tests.rs index 9cae880e1..8327aafb2 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/crypto/stark/src/tests/bus_tests/soundness_tests.rs @@ -13,6 +13,10 @@ use math::field::{ use crate::examples::multi_table_lookup::{ new_add_air_with_lookup, new_cpu_air_with_lookup, new_mul_air_with_lookup, }; +use crate::lookup::{ + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, Multiplicity, + NullBoundaryConstraintBuilder, Packing, +}; use crate::proof::options::ProofOptions; use crate::prover::{IsStarkProver, Prover}; use crate::table::Table; @@ -1076,6 +1080,129 @@ fn test_trace_ood_next_row_columns_is_accumulator_only() { } } +/// Cross-check an AIR's *declared* OOD transition window +/// ([`AIR::trace_ood_next_row_columns`]) against the next-row read set +/// *derived* from its captured constraint IR. +/// +/// The window declaration is load-bearing for soundness: the verifier opens +/// every trace column at `z`, but prunes the `g·z` (next-row) opening down to +/// exactly the declared columns and reconstructs ZERO for every other column at +/// the next row (see [`crate::ood`]). So a transition constraint that reads a +/// next-row column the declaration omits is fed zero there — a silent +/// soundness/completeness bug. The declaration is hand-synced to the LogUp +/// accumulator and ignores the wrapped constraint set, so nothing but a test +/// catches drift (the `debug_assert`s that would are compiled out under the +/// `--release` test profile this repo uses). +/// +/// Asserts, from the read set derived by +/// [`crate::constraint_ir::ConstraintProgram::next_row_trace_reads`]: +/// * `derived ⊆ declared` — the critical, soundness direction, checked for +/// every AIR: a derived column missing from the declaration is the bug above. +/// * exact equality when `exact` — every `AirWithBuses` should declare +/// *precisely* the accumulator column (or nothing, with no interactions); +/// over-declaration only bloats the proof, but for these AIRs the window is +/// exactly known, so drift in either direction is a defect. +fn assert_ood_window_matches_ir( + air: &dyn AIR, + exact: bool, + label: &str, +) { + let (main, aux) = air.trace_layout(); + + let mut declared = air.trace_ood_next_row_columns(); + declared.sort_unstable(); + declared.dedup(); + + // Derive the true next-row read set from the captured constraint program, + // which runs the wrapped constraint set AND the LogUp emission through one + // CaptureBuilder — so any next-row read a base constraint makes is included. + let derived = air.constraint_program().next_row_trace_reads(main); + + for &c in &derived { + assert!( + c < main + aux, + "[{label}] derived next-row column {c} out of concatenated width {main}+{aux}" + ); + assert!( + declared.contains(&c), + "[{label}] a transition constraint reads full-width column {c} at the next row, but \ + it is absent from trace_ood_next_row_columns() = {declared:?}; the verifier prunes \ + that g·z opening to ZERO — soundness bug" + ); + } + + if exact { + assert_eq!( + derived, declared, + "[{label}] declared next-row window {declared:?} is not exactly the IR-derived read \ + set {derived:?}: over-declaration bloats every g·z opening" + ); + } +} + +/// Generic counterpart to the hardcoded single-AIR expectation above: for every +/// `AirWithBuses` in the crate's examples, the declared OOD transition window +/// equals the next-row read set derived from its captured constraint IR. Covers +/// the structural shapes `split_interactions` can produce — 1 absorbed, 2 +/// absorbed, and a committed batched pair — so the hand-synced declaration is +/// validated against the real IR rather than a copy of itself. +#[test_log::test] +fn test_trace_ood_next_row_window_matches_captured_ir() { + let opts = ProofOptions::default_test_options(); + + // The multi-table lookup example AIRs the bus tests exercise: + // CPU sends on two buses (2 absorbed interactions, 0 committed pairs); + // ADD / MUL each receive on one bus (1 absorbed interaction). + assert_ood_window_matches_ir(&new_cpu_air_with_lookup(&opts), true, "CPU"); + assert_ood_window_matches_ir(&new_add_air_with_lookup(&opts), true, "ADD"); + assert_ood_window_matches_ir(&new_mul_air_with_lookup(&opts), true, "MUL"); + + // A committed-pair layout: 3 interactions split into 1 batched pair + 1 + // absorbed. The batched-term constraint reads only the current row, so the + // next-row window is still exactly the accumulator column — a case the three + // example AIRs (0 committed pairs) do not reach. + let committed = AirWithBuses::::new( + 6, + AuxiliaryTraceBuildData { + interactions: vec![ + BusInteraction::sender( + TEST_BUS, + Multiplicity::Column(0), + Packing::Direct.columns(&[1]), + ), + BusInteraction::sender( + TEST_BUS, + Multiplicity::Column(2), + Packing::Direct.columns(&[3]), + ), + BusInteraction::sender( + TEST_BUS, + Multiplicity::Column(4), + Packing::Direct.columns(&[5]), + ), + ], + }, + &opts, + 1, + EmptyConstraints, + ); + assert_ood_window_matches_ir(&committed, true, "committed_pair"); + + // A bus-less AIR: no interactions => no LogUp accumulator => an empty + // next-row window, derived and declared alike. + let busless = AirWithBuses::::new( + 3, + AuxiliaryTraceBuildData { + interactions: vec![], + }, + &opts, + 1, + EmptyConstraints, + ); + assert!(busless.trace_ood_next_row_columns().is_empty()); + assert_ood_window_matches_ir(&busless, true, "busless"); +} + /// The g·z pruning actually shrinks the proof: a LogUp table opens every column /// at z (the current-row block) but only the accumulator at the next row. #[test_log::test] diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index faabff35d..2d66692a9 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -65,6 +65,8 @@ pub mod memw_tests; #[cfg(test)] pub mod mul_tests; #[cfg(test)] +pub mod ood_window_ir_tests; +#[cfg(test)] pub mod page_tests; #[cfg(test)] pub mod prove_elfs_tests; diff --git a/prover/src/tests/ood_window_ir_tests.rs b/prover/src/tests/ood_window_ir_tests.rs new file mode 100644 index 000000000..b4ff5766c --- /dev/null +++ b/prover/src/tests/ood_window_ir_tests.rs @@ -0,0 +1,117 @@ +//! Cross-check every production table's declared OOD transition window against +//! the next-row read set derived from its captured constraint IR. +//! +//! [`stark::traits::AIR::trace_ood_next_row_columns`] declares which full-width +//! `[main | aux]` columns a transition constraint reads at the *next* row. The +//! verifier opens every trace column at `z` but prunes the `g·z` (next-row) +//! opening down to exactly that declared set, reconstructing ZERO for every +//! other column at the next row (see `stark::ood`). A constraint that reads a +//! next-row column the declaration omits is therefore fed zero there — a silent +//! soundness/completeness bug. +//! +//! For every VM table the window is the hand-synced `AirWithBuses` override +//! (empty, or exactly the LogUp accumulator column); it deliberately ignores the +//! wrapped constraint set, which could legally read the next row. The only guard +//! against that declaration drifting from the constraints is a test — the +//! `debug_assert`s that would otherwise catch it are compiled out under the +//! `--release` test profile this repo uses. This is that test: it derives the +//! true read set from the captured [`stark::constraint_ir::ConstraintProgram`] +//! (which runs the wrapped constraint set AND the LogUp emission through one +//! CaptureBuilder) and validates the declaration against it, so the check tracks +//! the real constraints rather than a copy of the declaration. +//! +//! It only CONSTRUCTS AIRs (no program execution, no ELF), so it runs anywhere. +//! The table list mirrors the enumeration in `constraint_program_tests.rs` — the +//! canonical per-table `create_*_air` constructors from `test_utils`; there is no +//! ELF-free registry to iterate (`VmAirs::air_refs` needs a real ELF plus +//! preprocessed-commitment builds), so a new table must be added here. + +use stark::proof::options::GoldilocksCubicProofOptions; +use stark::traits::AIR; + +use crate::tables::types::{GoldilocksExtension, GoldilocksField}; +use crate::test_utils::*; + +type Gl = GoldilocksField; +type Ext3 = GoldilocksExtension; + +/// Assert an AIR's declared next-row window equals / covers the IR-derived read +/// set. +/// +/// * `derived ⊆ declared` for every AIR — the soundness direction: a derived +/// column missing from the declaration is pruned to zero at the next row. +/// * exact equality when `exact` — every `AirWithBuses` should declare +/// *precisely* the accumulator column (or nothing); over-declaration only +/// bloats the `g·z` opening, but for these AIRs the window is exactly known. +fn assert_ood_window_matches_ir( + air: &dyn AIR, + exact: bool, + label: &str, +) { + let (main, aux) = air.trace_layout(); + + let mut declared = air.trace_ood_next_row_columns(); + declared.sort_unstable(); + declared.dedup(); + + // The production capture (lazy OnceLock behind the AIR): the wrapped + // constraint set spliced ahead of the LogUp suffix, so a next-row read by + // ANY constraint — base or LogUp — is in the derived set. + let derived = air.constraint_program().next_row_trace_reads(main); + + for &c in &derived { + assert!( + c < main + aux, + "[{label}] derived next-row column {c} out of concatenated width {main}+{aux}" + ); + assert!( + declared.contains(&c), + "[{label}] a transition constraint reads full-width column {c} at the next row, but \ + it is absent from trace_ood_next_row_columns() = {declared:?}; the verifier prunes \ + that g·z opening to ZERO — soundness bug" + ); + } + + if exact { + assert_eq!( + derived, declared, + "[{label}] declared next-row window {declared:?} is not exactly the IR-derived read \ + set {derived:?}: over-declaration bloats every g·z opening" + ); + } +} + +/// Every production table AIR declares an OOD transition window equal to the +/// next-row read set derived from its captured constraint IR. All VM tables are +/// `AirWithBuses`, whose window is exactly the accumulator column (or empty), so +/// equality is asserted for each. +#[test] +fn all_table_windows_match_captured_ir() { + let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid"); + + assert_ood_window_matches_ir(&create_cpu_air(&opts), true, "CPU"); + assert_ood_window_matches_ir(&create_bitwise_air(&opts), true, "BITWISE"); + assert_ood_window_matches_ir(&create_lt_air(&opts), true, "LT"); + assert_ood_window_matches_ir(&create_shift_air(&opts), true, "SHIFT"); + assert_ood_window_matches_ir(&create_eq_air(&opts), true, "EQ"); + assert_ood_window_matches_ir(&create_bytewise_air(&opts), true, "BYTEWISE"); + assert_ood_window_matches_ir(&create_store_air(&opts), true, "STORE"); + assert_ood_window_matches_ir(&create_cpu32_air(&opts), true, "CPU32"); + assert_ood_window_matches_ir(&create_memw_air(&opts), true, "MEMW"); + assert_ood_window_matches_ir(&create_memw_aligned_air(&opts), true, "MEMW_A"); + assert_ood_window_matches_ir(&create_memw_register_air(&opts), true, "MEMW_R"); + assert_ood_window_matches_ir(&create_load_air(&opts), true, "LOAD"); + assert_ood_window_matches_ir(&create_decode_air(&opts), true, "DECODE"); + assert_ood_window_matches_ir(&create_mul_air(&opts), true, "MUL"); + assert_ood_window_matches_ir(&create_dvrm_air(&opts), true, "DVRM"); + assert_ood_window_matches_ir(&create_branch_air(&opts), true, "BRANCH"); + assert_ood_window_matches_ir(&create_halt_air(&opts), true, "HALT"); + assert_ood_window_matches_ir(&create_commit_air(&opts), true, "COMMIT"); + assert_ood_window_matches_ir(&create_page_air(&opts, 0x1000), true, "PAGE"); + assert_ood_window_matches_ir(&create_register_air(&opts), true, "REGISTER"); + assert_ood_window_matches_ir(&create_keccak_air(&opts), true, "KECCAK"); + assert_ood_window_matches_ir(&create_keccak_rnd_air(&opts), true, "KECCAK_RND"); + assert_ood_window_matches_ir(&create_keccak_rc_air(&opts), true, "KECCAK_RC"); + assert_ood_window_matches_ir(&create_ecsm_air(&opts), true, "ECSM"); + assert_ood_window_matches_ir(&create_ecdas_air(&opts), true, "ECDAS"); +}