From f6e656ddecf9bf3a2fcd2d59811b137ea156e5e9 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 15 Jul 2026 15:04:15 -0300 Subject: [PATCH 1/3] harden(verifier): derive OOD table shape from AIR metadata, not the proof MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). --- .../src/tests/bus_tests/soundness_tests.rs | 77 +++++++++++++++++++ crypto/stark/src/verifier.rs | 20 ++++- 2 files changed, 95 insertions(+), 2 deletions(-) diff --git a/crypto/stark/src/tests/bus_tests/soundness_tests.rs b/crypto/stark/src/tests/bus_tests/soundness_tests.rs index 652f5e87d..5c5558a02 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,82 @@ 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" + ); +} + // ============================================================================= // Invalid bus public inputs // ============================================================================= diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index fdee3d2ff..9212294ea 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -107,6 +107,21 @@ pub trait IsStarkVerifier< { crate::profile_markers::STEP_VERIFY_CLAIMED_COMPOSITION_POLYNOMIAL }, >(); let trace_length = proof.trace_length; + + // Soundness: the OOD trace-evaluation table's shape is a public function + // of the AIR, never of the (prover-controlled) proof. Reject any proof + // whose table is not exactly the expected size, so a malicious prover + // cannot reshape it — e.g. drop a column to dodge a constraint check, or + // mis-size it and desync the frame reconstruction below. Every later use + // of the table derives its shape from the AIR, not from the proof. + let expected_ood_width = air.trace_layout().0 + air.num_auxiliary_rap_columns(); + let expected_ood_height = air.context().transition_offsets.len() * air.step_size(); + if proof.trace_ood_evaluations.width != expected_ood_width + || proof.trace_ood_evaluations.height != expected_ood_height + { + return false; + } + let boundary_constraints = air.boundary_constraints( &proof.public_inputs, &challenges.rap_challenges, @@ -167,8 +182,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 { From 2234ded89cb1e06b6c48fb5c59025167e453e63e Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 15 Jul 2026 15:17:02 -0300 Subject: [PATCH 2/3] =?UTF-8?q?feat(air):=20trace=5Food=5Fnext=5Frow=5Fcol?= =?UTF-8?q?umns=20=E2=80=94=20the=20per-column=20transition=20window?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). --- crypto/stark/src/lookup.rs | 13 +++++++++++ .../src/tests/bus_tests/soundness_tests.rs | 23 +++++++++++++++++++ crypto/stark/src/traits.rs | 15 ++++++++++++ 3 files changed, 51 insertions(+) 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/tests/bus_tests/soundness_tests.rs b/crypto/stark/src/tests/bus_tests/soundness_tests.rs index 5c5558a02..074ccaa4e 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/crypto/stark/src/tests/bus_tests/soundness_tests.rs @@ -904,6 +904,29 @@ fn test_malformed_ood_table_shape_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}" + ); + } +} + // ============================================================================= // Invalid bus public inputs // ============================================================================= diff --git a/crypto/stark/src/traits.rs b/crypto/stark/src/traits.rs index c28f831a2..4b1c18a9e 100644 --- a/crypto/stark/src/traits.rs +++ b/crypto/stark/src/traits.rs @@ -198,6 +198,21 @@ 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 + /// empty: a single-row transition window with no next-row reads. + fn trace_ood_next_row_columns(&self) -> Vec { + Vec::new() + } + fn composition_poly_degree_bound(&self, trace_length: usize) -> usize; /// Evaluates the transitions corresponding to an evaluation frame at the From 32337b8558096649df9962db0d002c7197db2946 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 15 Jul 2026 20:07:49 -0300 Subject: [PATCH 3/3] =?UTF-8?q?feat(stark):=20prune=20redundant=20g=C2=B7z?= =?UTF-8?q?=20(next-row)=20trace-OOD=20openings?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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/ood.rs | 224 ++++++++++++++++++ crypto/stark/src/proof/stark.rs | 6 +- crypto/stark/src/prover.rs | 52 +++- .../src/tests/bus_tests/soundness_tests.rs | 65 +++++ crypto/stark/src/traits.rs | 12 +- crypto/stark/src/verifier.rs | 129 ++++++++-- 7 files changed, 447 insertions(+), 42 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/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 074ccaa4e..f14907a9d 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/crypto/stark/src/tests/bus_tests/soundness_tests.rs @@ -927,6 +927,71 @@ fn test_trace_ood_next_row_columns_is_accumulator_only() { } } +/// 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 4b1c18a9e..0aec97a2a 100644 --- a/crypto/stark/src/traits.rs +++ b/crypto/stark/src/traits.rs @@ -207,10 +207,16 @@ pub trait AIR: Send + Sync { /// 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 - /// empty: a single-row transition window with no next-row reads. + /// 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 { - Vec::new() + let (main, aux) = self.trace_layout(); + (0..main + aux).collect() } fn composition_poly_degree_bound(&self, trace_length: usize) -> usize; diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index 9212294ea..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"))] @@ -108,20 +109,41 @@ pub trait IsStarkVerifier< >(); let trace_length = proof.trace_length; - // Soundness: the OOD trace-evaluation table's shape is a public function - // of the AIR, never of the (prover-controlled) proof. Reject any proof - // whose table is not exactly the expected size, so a malicious prover - // cannot reshape it — e.g. drop a column to dodge a constraint check, or - // mis-size it and desync the frame reconstruction below. Every later use - // of the table derives its shape from the AIR, not from the proof. + // 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 expected_ood_height = air.context().transition_offsets.len() * air.step_size(); + 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 != expected_ood_height + || 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, @@ -207,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, @@ -285,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, @@ -626,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(); @@ -678,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. @@ -702,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, @@ -715,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 @@ -749,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 @@ -1063,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) @@ -1080,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: 𝛾, 𝛾' @@ -1090,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;