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/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/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/logup_gpu.rs b/crypto/stark/src/logup_gpu.rs index bc9e88302..3fd49134d 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); 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 abd3218b8..8a89ea727 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() } @@ -1266,17 +1279,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(), )); } @@ -1718,9 +1731,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( @@ -1751,15 +1765,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")] @@ -2156,9 +2172,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) @@ -2171,30 +2190,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 }; @@ -2324,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}; @@ -2375,6 +2397,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 col in &term_columns { + row_sum = row_sum + &col[i]; + } + 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}"); + } + } + /// 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`] diff --git a/crypto/stark/src/ood.rs b/crypto/stark/src/ood.rs new file mode 100644 index 000000000..d5f17d159 --- /dev/null +++ b/crypto/stark/src/ood.rs @@ -0,0 +1,459 @@ +//! Shared, prover = verifier-identical helpers for out-of-domain (OOD) trace +//! opening pruning. +//! +//! 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. +//! +//! 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. +/// +/// 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`. +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 width` OOD table from the two pruned +/// proof blocks, given as row-major slices (a [`Table`]'s `row_major_data()` or a +/// [`crate::proof::view::StarkTableView`]'s, so this stays decoupled from owned +/// vs. rkyv-archived proofs). Current-row rows come straight from `current_block`; +/// each next-row row scatters the masked values from `next_block` 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. +/// +/// Reads are bounds-checked (`.get`): a malformed archive whose advertised +/// dimensions disagree with its data length yields a zero-filled grid rather than +/// a panic, and fails the downstream consistency checks instead. +pub fn reconstruct_ood_full( + current_block: &[FieldElement], + width: usize, + next_block: &[FieldElement], + num_eval_points: usize, + step_size: usize, + next_row_cols: &[usize], +) -> Table { + let mask_width = next_row_cols.len(); + let mut data = Vec::with_capacity(num_eval_points * width); + + for r in 0..step_size { + for c in 0..width { + data.push( + current_block + .get(r * width + c) + .cloned() + .unwrap_or_else(FieldElement::::zero), + ); + } + } + + // 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(); + } + } + } + + 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::*; + 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.row_major_data(), + b0.width, + b1.row_major_data(), + 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.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()]); + } + + #[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}. + 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 + } + + #[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/proof/stark.rs b/crypto/stark/src/proof/stark.rs index 960594866..ba4aca2dc 100644 --- a/crypto/stark/src/proof/stark.rs +++ b/crypto/stark/src/proof/stark.rs @@ -81,8 +81,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/proof/view.rs b/crypto/stark/src/proof/view.rs index e2f84f711..6eb8cedaf 100644 --- a/crypto/stark/src/proof/view.rs +++ b/crypto/stark/src/proof/view.rs @@ -367,6 +367,17 @@ where } } + /// The pruned next-row (g·z) OOD block: only the transition-window columns + /// the AIR reads at the next row (empty when it reads none). Parallels + /// [`Self::trace_ood_evaluations`]; the verifier scatters these back into the + /// full grid via [`crate::ood::reconstruct_ood_full`]. + pub fn trace_ood_next_evaluations(&self) -> StarkTableView<'a, E> { + match self { + Self::Owned(p) => StarkTableView::Owned(&p.trace_ood_next_evaluations), + Self::Archived(p) => StarkTableView::Archived(&p.trace_ood_next_evaluations), + } + } + pub fn composition_poly_root(&self) -> &'a Commitment { match self { Self::Owned(p) => &p.composition_poly_root, @@ -498,6 +509,7 @@ fn assert_stark_proof_view_is_exhaustive, E: IsField, PI>( lde_trace_aux_merkle_root: _, lde_trace_precomputed_merkle_root: _, trace_ood_evaluations: _, + trace_ood_next_evaluations: _, composition_poly_root: _, composition_poly_parts_ood_evaluation: _, fri_layers_merkle_roots: _, diff --git a/crypto/stark/src/prover.rs b/crypto/stark/src/prover.rs index 7fa560e5c..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,8 +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_terms_trace = - air.context().transition_offsets.len() * air.step_size() * air.context().trace_columns; + // g·z pruning: only the current-row block (all columns) plus the masked + // next-row columns get an opening / DEEP coefficient. + let layout = Self::ood_layout(air); + let num_terms_trace = layout.num_surviving(); // <<<< Receive challenges: 𝛾, 𝛾' let mut deep_composition_coefficients: Vec<_> = @@ -1467,12 +1486,13 @@ 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 = layout.build_trace_term_coeffs(&trace_term_powers); // <<<< Receive challenges: 𝛾ⱼ, 𝛾ⱼ' let gammas = deep_composition_coefficients; @@ -3103,11 +3123,17 @@ 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_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() { + transcript.append_field_element(elem); + } } } @@ -3161,8 +3187,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..8327aafb2 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/crypto/stark/src/tests/bus_tests/soundness_tests.rs @@ -13,8 +13,13 @@ 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; use crate::test_utils::multi_prove_ram; use crate::trace::TraceTable; use crate::traits::AIR; @@ -827,6 +832,459 @@ 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" + ); +} + +/// 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. +#[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}" + ); + } +} + +/// 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] +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 (owned path). + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &add_air, &mul_air]; + assert!(Verifier::multi_verify( + &airs, + &multi_proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + )); + + // ...and through the rkyv-archived, read-in-place path — the same path the + // recursion guest uses. This exercises the new `trace_ood_next_evaluations` + // field's archival and the `StarkTableView::Archived` reads of the pruned + // next-row block, which the owned path above does not cover. + let bytes = rkyv::to_bytes::(&multi_proof).unwrap(); + let archived = rkyv::access::< + crate::proof::stark::ArchivedMultiProof, + rkyv::rancor::Error, + >(&bytes) + .unwrap(); + assert!(Verifier::multi_verify_archived( + &airs, + &archived.proofs, + &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 f78bf6e34..ae26afbe9 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -13,7 +13,9 @@ use crate::{ proof::stark::{ArchivedStarkProof, MultiProof}, proof::view::{ DeepPolynomialOpeningView, FriDecommitmentView, PolynomialOpeningsView, StarkProofView, + StarkTableView, }, + table::Table, }; use crypto::fiat_shamir::is_transcript::IsStarkTranscript; use crypto::merkle_tree::proof::{verify_merkle_path, verify_merkle_path_from_leaf_hash}; @@ -90,8 +92,11 @@ pub struct QueryInvariantDeepTerms where FieldExtension: Send + Sync + IsField, { - /// `ood_row_sum[row] = sum_col trace_term_coeffs[col][row] * ood(row, col)`. + /// `ood_row_sum[row] = sum_col trace_term_coeffs[col][row] * ood(row, col)`, + /// over the reconstructed full OOD grid (g·z-pruned positions are zero). ood_row_sum: Vec>, + /// Width of the reconstructed full OOD grid (= full trace width). + ood_width: usize, /// Derived from `proof.composition_poly_parts_ood_evaluation().len()`. number_of_parts: usize, /// `challenges.z.pow(number_of_parts)`. @@ -136,15 +141,74 @@ 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 + /// 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>, 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 }, @@ -155,6 +219,7 @@ pub trait IsStarkVerifier< let bus_public_inputs = proof .bus_table_contribution() .map(BusPublicInputs::from_contribution); + let boundary_constraints = air.boundary_constraints( public_inputs, &challenges.rap_challenges, @@ -217,7 +282,9 @@ pub trait IsStarkVerifier< .fold(FieldElement::::zero(), |acc, x| acc + x); // A malformed archive can advertise fewer OOD columns than the AIR's - // aux count; reject instead of underflowing. + // aux count; reject instead of underflowing. The current-row block keeps + // the full trace width even under g·z pruning, so this still yields the + // main width. let num_main_trace_columns = match trace_ood_evaluations .width() .checked_sub(air.num_auxiliary_rap_columns()) @@ -247,7 +314,11 @@ pub trait IsStarkVerifier< None => FieldElement::zero(), }; - let ood_frame = 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. + // `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); let transition_evaluation_context = TransitionEvaluationContext::new_verifier( &ood_frame, &challenges.rap_challenges, @@ -318,6 +389,12 @@ 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, @@ -326,7 +403,12 @@ pub trait IsStarkVerifier< crate::profile_markers::step_marker::<{ crate::profile_markers::STEP_VERIFY_FRI }>(); 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_cols, + step_size, ) { Some(pair) => pair, None => return false, @@ -668,14 +750,22 @@ pub trait IsStarkVerifier< /// Sums that depend only on `challenges` and proof-level OOD/gamma data — /// identical for every FRI query — computed once instead of once per /// query. + /// + /// g·z pruning: the trace OOD values come from the reconstructed full grid + /// `ood_full` (current-row block plus the scattered next-row window, zeros + /// elsewhere), not from `proof.trace_ood_evaluations()` which now carries + /// only the current-row block. Pruned positions are zero in both the grid + /// and `trace_term_coeffs`, so next rows sum only the window columns. fn compute_query_invariant_deep_terms( challenges: &Challenges, proof: StarkProofView<'_, Field, FieldExtension, PI>, + ood_full: &Table, + next_row_cols: &[usize], + step_size: usize, ) -> Option> { - let trace_ood_evaluations = proof.trace_ood_evaluations(); - let ood_evaluations_table_height = trace_ood_evaluations.height(); - let ood_evaluations_table_width = trace_ood_evaluations.width(); - let ood_data = trace_ood_evaluations.row_major_data(); + let ood_evaluations_table_height = ood_full.height; + let ood_evaluations_table_width = ood_full.width; + let ood_data = ood_full.row_major_data(); let trace_term_coeffs = &challenges.trace_term_coeffs; if trace_term_coeffs.is_empty() @@ -690,8 +780,16 @@ pub trait IsStarkVerifier< let ood_row = &ood_data[row_idx * ood_evaluations_table_width ..(row_idx + 1) * ood_evaluations_table_width]; let mut sum = FieldElement::::zero(); - for col_idx in 0..ood_evaluations_table_width { - sum += &trace_term_coeffs[col_idx][row_idx] * &ood_row[col_idx]; + if row_idx < step_size { + for col_idx in 0..ood_evaluations_table_width { + sum += &trace_term_coeffs[col_idx][row_idx] * &ood_row[col_idx]; + } + } else { + // Next-row row: off-window columns contribute coeff·0 with a + // zero coeff too, so the window-only sum is exact. + for &col_idx in next_row_cols { + sum += &trace_term_coeffs[col_idx][row_idx] * &ood_row[col_idx]; + } } ood_row_sum.push(sum); } @@ -713,6 +811,7 @@ pub trait IsStarkVerifier< Some(QueryInvariantDeepTerms { ood_row_sum, + ood_width: ood_evaluations_table_width, number_of_parts, z_pow, h_sum_zpow, @@ -723,6 +822,9 @@ pub trait IsStarkVerifier< challenges: &Challenges, domain: &VerifierDomain, proof: StarkProofView<'_, Field, FieldExtension, PI>, + ood_full: &Table, + next_row_cols: &[usize], + step_size: usize, ) -> Option> { let num_queries = challenges.iotas.len(); @@ -746,7 +848,13 @@ pub trait IsStarkVerifier< let primitive_root = &Field::get_primitive_root_of_unity(domain.root_order as u64) .expect("verifier domain root_order is a valid power of two"); - let query_invariant_terms = Self::compute_query_invariant_deep_terms(challenges, proof)?; + let query_invariant_terms = Self::compute_query_invariant_deep_terms( + challenges, + proof, + ood_full, + next_row_cols, + step_size, + )?; for (i, iota) in challenges.iotas.iter().enumerate() { let opening = proof.deep_poly_opening(i); @@ -782,12 +890,13 @@ pub trait IsStarkVerifier< Self::query_challenge_to_evaluation_point(*iota, true, domain); let (evaluation, evaluation_sym) = Self::reconstruct_deep_composition_poly_evaluation_pair( - proof, &evaluation_point, &evaluation_point_sym, primitive_root, challenges, &query_invariant_terms, + next_row_cols, + step_size, lde_precomputed, lde_main, lde_aux, @@ -809,14 +918,18 @@ pub trait IsStarkVerifier< /// isolates `coeff*ood` (identical for both points, hoisted into /// `query_invariant_terms`) from `coeff*base` (per-point), so both points /// share the OOD walk and a single batch-inverse for their denominators. + /// g·z pruning restricts next rows (`row_idx >= step_size`) to the + /// transition-window columns `next_row_cols` — all other next-row + /// coefficients are zero, so those terms vanish from both sums. #[allow(clippy::too_many_arguments)] fn reconstruct_deep_composition_poly_evaluation_pair<'b>( - proof: StarkProofView<'_, Field, FieldExtension, PI>, evaluation_point: &FieldElement, evaluation_point_sym: &FieldElement, primitive_root: &FieldElement, challenges: &Challenges, query_invariant_terms: &QueryInvariantDeepTerms, + next_row_cols: &[usize], + step_size: usize, lde_trace_precomputed_evaluations: &'b [FieldElement], lde_trace_main_evaluations: &'b [FieldElement], lde_trace_aux_evaluations: &[FieldElement], @@ -827,7 +940,7 @@ pub trait IsStarkVerifier< lde_composition_poly_parts_evaluation_sym: &[FieldElement], ) -> Option<(FieldElement, FieldElement)> { let ood_evaluations_table_height = query_invariant_terms.ood_row_sum.len(); - let ood_evaluations_table_width = proof.trace_ood_evaluations().width(); + let ood_evaluations_table_width = query_invariant_terms.ood_width; let trace_term_coeffs = &challenges.trace_term_coeffs; // Base columns are supplied as two slices (precomputed ‖ main) that the @@ -888,16 +1001,35 @@ pub trait IsStarkVerifier< let ood_row_sum = &query_invariant_terms.ood_row_sum[row_idx]; let mut base_row_sum = FieldElement::::zero(); let mut base_row_sum_sym = FieldElement::::zero(); - for (col_idx, coeff_col) in trace_term_coeffs.iter().enumerate() { - let coeff = &coeff_col[row_idx]; - if col_idx < num_base { - // F: IsSubFieldOf gives the cheap asymmetric F * E -> E product. - base_row_sum += base_at(col_idx) * coeff; - base_row_sum_sym += base_at_sym(col_idx) * coeff; - } else { - let aux_idx = col_idx - num_base; - base_row_sum += coeff * &lde_trace_aux_evaluations[aux_idx]; - base_row_sum_sym += coeff * &lde_trace_aux_evaluations_sym[aux_idx]; + if row_idx < step_size { + for (col_idx, coeff_col) in trace_term_coeffs.iter().enumerate() { + let coeff = &coeff_col[row_idx]; + if col_idx < num_base { + // F: IsSubFieldOf gives the cheap asymmetric F * E -> E product. + base_row_sum += base_at(col_idx) * coeff; + base_row_sum_sym += base_at_sym(col_idx) * coeff; + } else { + let aux_idx = col_idx - num_base; + base_row_sum += coeff * &lde_trace_aux_evaluations[aux_idx]; + base_row_sum_sym += coeff * &lde_trace_aux_evaluations_sym[aux_idx]; + } + } + } else { + // g·z pruning: the next-row block opens only transition-window + // columns; every other column's coefficient is zero + // (`build_pruned_trace_term_coeffs`), so summing the window + // alone is exact — and skipping the rest is where the + // verifier/recursion cycle saving lands. + for &col_idx in next_row_cols { + let coeff = &trace_term_coeffs[col_idx][row_idx]; + if col_idx < num_base { + base_row_sum += base_at(col_idx) * coeff; + base_row_sum_sym += base_at_sym(col_idx) * coeff; + } else { + let aux_idx = col_idx - num_base; + base_row_sum += coeff * &lde_trace_aux_evaluations[aux_idx]; + base_row_sum_sym += coeff * &lde_trace_aux_evaluations_sym[aux_idx]; + } } } trace_term += &denoms_trace[row_idx] * &(&base_row_sum - ood_row_sum); @@ -1033,32 +1165,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() { @@ -1245,6 +1360,7 @@ pub trait IsStarkVerifier< domain: &VerifierDomain, transcript: &mut impl IsStarkTranscript, rap_challenges: Vec>, + layout: &crate::ood::OodLayout, ) -> Challenges where FieldElement: AsBytes, @@ -1295,13 +1411,18 @@ pub trait IsStarkVerifier< &domain.coset_offset, ); - // <<<< Receive values: tⱼ(zgᵏ) - // Column-major append (matches `Table::columns()` order) reading the + // <<<< 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), each column-major (matching `Table::columns()` order) reading // rows in place, without materializing transposed columns. - let ood = proof.trace_ood_evaluations(); - for col_idx in 0..ood.width() { - for row_idx in 0..ood.height() { - transcript.append_field_element(&ood.get_row(row_idx)[col_idx]); + for ood in [ + proof.trace_ood_evaluations(), + proof.trace_ood_next_evaluations(), + ] { + for col_idx in 0..ood.width() { + for row_idx in 0..ood.height() { + transcript.append_field_element(&ood.get_row(row_idx)[col_idx]); + } } } // <<<< Receive value: Hᵢ(z^N) @@ -1314,8 +1435,10 @@ 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; + // 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 = layout.num_surviving(); let gamma = transcript.sample_field_element(); // <<<< Receive challenges: 𝛾, 𝛾' @@ -1324,12 +1447,10 @@ 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 = layout.build_trace_term_coeffs(&trace_term_powers); // <<<< Receive challenges: 𝛾ⱼ, 𝛾ⱼ' let gammas = deep_composition_coefficients; @@ -1411,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")] @@ -1423,6 +1550,7 @@ pub trait IsStarkVerifier< &domain, transcript, rap_challenges, + &layout, ); // verify grinding @@ -1449,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"); @@ -1470,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; 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"); +}