diff --git a/crypto/stark/src/lib.rs b/crypto/stark/src/lib.rs index caa1c73a0..6f8e7c82e 100644 --- a/crypto/stark/src/lib.rs +++ b/crypto/stark/src/lib.rs @@ -23,6 +23,7 @@ pub mod instruments; #[cfg(feature = "cuda")] pub mod logup_gpu; pub mod lookup; +pub mod ood; pub(crate) mod par; pub mod profile_markers; pub mod proof; diff --git a/crypto/stark/src/lookup.rs b/crypto/stark/src/lookup.rs index 07fc4c382..d52624980 100644 --- a/crypto/stark/src/lookup.rs +++ b/crypto/stark/src/lookup.rs @@ -1003,6 +1003,19 @@ where self.trace_layout } + fn trace_ood_next_row_columns(&self) -> Vec { + // The only transition constraint that reads the next row is the circular + // LogUp accumulator, and after forward accumulation it reads only the + // accumulated column there (all committed terms and absorbed operands + // read the current row). Its full-width index is the main width plus the + // accumulated column's aux index. No interactions => no next-row reads. + if self.auxiliary_trace_build_data.interactions.is_empty() { + Vec::new() + } else { + vec![self.trace_layout.0 + self.logup.acc_column_idx] + } + } + fn has_trace_interaction(&self) -> bool { !self.auxiliary_trace_build_data.interactions.is_empty() } diff --git a/crypto/stark/src/ood.rs b/crypto/stark/src/ood.rs new file mode 100644 index 000000000..f9dfc6e35 --- /dev/null +++ b/crypto/stark/src/ood.rs @@ -0,0 +1,224 @@ +//! Shared, prover = verifier-identical helpers for out-of-domain (OOD) trace +//! opening pruning. +//! +//! The frame OOD table has `num_offsets * step_size` rows (offsets `[0, 1]`, +//! offset-major: the first `step_size` rows are the current-row block, the rest +//! are next-row blocks) and one column per trace column. Only the columns a +//! transition constraint actually reads at the next row — the AIR's transition +//! window, [`crate::traits::AIR::trace_ood_next_row_columns`] — need to be +//! opened in the next-row block(s). Every other next-row entry is redundant and +//! is pruned from the proof. +//! +//! Everything here is a pure function of public AIR shape metadata (`step_size`, +//! the column count, and the next-row column set), so the prover and verifier +//! derive the identical layout without trusting proof dimensions (invariant I3). + +use crate::table::Table; +use math::field::{element::FieldElement, traits::IsField}; + +/// Per-column flags: `flags[c] == true` iff column `c` is opened at the next +/// row. Indices outside `0..num_total_cols` are ignored. +pub fn next_row_col_flags(num_total_cols: usize, next_row_cols: &[usize]) -> Vec { + let mut flags = vec![false; num_total_cols]; + for &c in next_row_cols { + if c < num_total_cols { + flags[c] = true; + } + } + flags +} + +/// Number of surviving trace openings: the current-row block opens every column +/// (`step_size * num_total_cols`), and each next-row row opens only the masked +/// columns (`(num_eval_points - step_size) * num_next_row_cols`). +pub fn num_surviving_trace_openings( + num_total_cols: usize, + num_eval_points: usize, + step_size: usize, + num_next_row_cols: usize, +) -> usize { + let next_rows = num_eval_points.saturating_sub(step_size); + step_size * num_total_cols + next_rows * num_next_row_cols +} + +/// Build the rectangular `num_total_cols x num_eval_points` DEEP trace-term +/// coefficient grid from `powers` (the `num_surviving_trace_openings` gamma +/// powers drained for the trace terms). Surviving positions receive a power in a +/// fixed order; pruned next-row positions receive zero. A rectangular DEEP +/// evaluation over the full grid therefore yields the identical polynomial as +/// summing only the survivors — which is what lets the prover keep its +/// (GPU-friendly) rectangular DEEP unchanged. +/// +/// Assignment order (mirrored exactly by [`num_surviving_trace_openings`]): +/// 1. current-row block — for every column `j`, rows `0..step_size`; +/// 2. next-row block — for each masked column `j`, rows `step_size..num_eval_points`. +pub fn build_pruned_trace_term_coeffs( + powers: &[FieldElement], + num_total_cols: usize, + num_eval_points: usize, + step_size: usize, + next_row_cols: &[usize], +) -> Vec>> { + let flags = next_row_col_flags(num_total_cols, next_row_cols); + let mut coeffs = vec![vec![FieldElement::::zero(); num_eval_points]; num_total_cols]; + let mut p = 0usize; + // Current-row block: all columns, rows 0..step_size. + for col in coeffs.iter_mut() { + for slot in col.iter_mut().take(step_size) { + if p < powers.len() { + *slot = powers[p].clone(); + p += 1; + } + } + } + // Next-row block(s): masked columns only, rows step_size..num_eval_points. + for (j, col) in coeffs.iter_mut().enumerate() { + if flags[j] { + for slot in col.iter_mut().take(num_eval_points).skip(step_size) { + if p < powers.len() { + *slot = powers[p].clone(); + p += 1; + } + } + } + } + debug_assert_eq!(p, powers.len(), "power assignment must consume every power"); + coeffs +} + +/// Split the full `num_eval_points x num_total_cols` OOD table (computed by the +/// prover) into the two blocks carried by the proof: +/// * block 0 — the current-row block, `step_size x num_total_cols` (all columns); +/// * block 1 — the next-row block, `next_rows x num_next_row_cols`, holding only +/// the masked columns in `next_row_cols` order. +/// +/// Block 1 has width 0 (an empty table) when the AIR reads no next-row columns. +pub fn split_ood_blocks( + full: &Table, + step_size: usize, + next_row_cols: &[usize], +) -> (Table, Table) { + let w = full.width; + + let mut b0 = Vec::with_capacity(step_size * w); + for r in 0..step_size { + b0.extend_from_slice(full.get_row(r)); + } + let block0 = Table::new(b0, w); + + let mut b1 = Vec::with_capacity((full.height.saturating_sub(step_size)) * next_row_cols.len()); + for r in step_size..full.height { + let row = full.get_row(r); + for &c in next_row_cols { + b1.push(row[c].clone()); + } + } + let block1 = Table::new(b1, next_row_cols.len()); + + (block0, block1) +} + +/// Rebuild the full `num_eval_points x num_total_cols` OOD table from the two +/// pruned proof blocks. Current-row rows come straight from `block0`; each +/// next-row row scatters the masked values from `block1` into their columns and +/// leaves every other column zero. Those zero entries are never read — no +/// transition constraint references a pruned column at the next row, and DEEP +/// skips them — so the reconstruction is exact where it matters. +pub fn reconstruct_ood_full( + block0: &Table, + block1: &Table, + num_eval_points: usize, + step_size: usize, + next_row_cols: &[usize], +) -> Table { + let w = block0.width; + let mut data = Vec::with_capacity(num_eval_points * w); + + for r in 0..step_size { + data.extend_from_slice(block0.get_row(r)); + } + + for r in step_size..num_eval_points { + let has_next = block1.width > 0 && (r - step_size) < block1.height; + for c in 0..w { + let mut val = FieldElement::::zero(); + if has_next { + for (m, &mc) in next_row_cols.iter().enumerate() { + if mc == c { + val = block1.get_row(r - step_size)[m].clone(); + break; + } + } + } + data.push(val); + } + } + + Table::new(data, w) +} + +#[cfg(test)] +mod tests { + use super::*; + use math::field::goldilocks::GoldilocksField as Gl; + + type Fe = FieldElement; + + fn fe(x: u64) -> Fe { + Fe::from(x) + } + + #[test] + fn surviving_count_matches_layout() { + // 3 columns, 2 eval points (step_size 1), 1 next-row column: + // current-row opens 3, next-row opens 1 => 4. + assert_eq!(num_surviving_trace_openings(3, 2, 1, 1), 4); + // No next-row columns => only the current-row block survives. + assert_eq!(num_surviving_trace_openings(3, 2, 1, 0), 3); + // Every column open at the next row => full 2*W grid. + assert_eq!(num_surviving_trace_openings(3, 2, 1, 3), 6); + } + + #[test] + fn split_then_reconstruct_preserves_survivors_and_zeros_pruned() { + // Full 2x3 OOD table: row 0 (current row), row 1 (next row). + let full = Table::new(vec![fe(10), fe(11), fe(12), fe(20), fe(21), fe(22)], 3); + let next_row_cols = [1usize]; // only column 1 opens at the next row + let step_size = 1; + + let (b0, b1) = split_ood_blocks(&full, step_size, &next_row_cols); + assert_eq!((b0.width, b0.height), (3, 1)); + assert_eq!((b1.width, b1.height), (1, 1)); + assert_eq!(b1.get_row(0)[0], fe(21)); // full[1][1] + + let recon = reconstruct_ood_full(&b0, &b1, 2, step_size, &next_row_cols); + assert_eq!(recon.get_row(0), full.get_row(0)); // current row is exact + assert_eq!(recon.get_row(1)[1], fe(21)); // survivor placed + assert_eq!(recon.get_row(1)[0], Fe::zero()); // pruned -> zero + assert_eq!(recon.get_row(1)[2], Fe::zero()); // pruned -> zero + } + + #[test] + fn empty_next_row_block_reconstructs_to_zeros() { + let full = Table::new(vec![fe(10), fe(11), fe(20), fe(21)], 2); + let (b0, b1) = split_ood_blocks(&full, 1, &[]); + assert_eq!(b1.width, 0); + let recon = reconstruct_ood_full(&b0, &b1, 2, 1, &[]); + assert_eq!(recon.get_row(0), full.get_row(0)); + assert_eq!(recon.get_row(1), &[Fe::zero(), Fe::zero()]); + } + + #[test] + fn pruned_coeffs_are_zero_off_the_window() { + // 4 surviving powers for W=3, num_eval_points=2, mask={1}. + let powers: Vec = (1..=4).map(fe).collect(); + let coeffs = build_pruned_trace_term_coeffs(&powers, 3, 2, 1, &[1]); + // Current-row row (k=0) is fully populated; next-row row (k=1) only col 1. + assert_ne!(coeffs[0][0], Fe::zero()); + assert_ne!(coeffs[1][0], Fe::zero()); + assert_ne!(coeffs[2][0], Fe::zero()); + assert_ne!(coeffs[1][1], Fe::zero()); // masked column, next row + assert_eq!(coeffs[0][1], Fe::zero()); // pruned + assert_eq!(coeffs[2][1], Fe::zero()); // pruned + } +} diff --git a/crypto/stark/src/proof/stark.rs b/crypto/stark/src/proof/stark.rs index 675160837..6e2a55870 100644 --- a/crypto/stark/src/proof/stark.rs +++ b/crypto/stark/src/proof/stark.rs @@ -49,8 +49,12 @@ pub struct StarkProof, E: IsField, PI> { // For preprocessed tables: commitment to precomputed columns only. // Verifier checks this matches the hardcoded commitment from AIR. pub lde_trace_precomputed_merkle_root: Option, - // tⱼ(zgᵏ) + // tⱼ(zgᵏ) for the current-row block (offset 0): every trace column at z. pub trace_ood_evaluations: Table, + // tⱼ(zgᵏ) for the next-row block(s) (offset >= 1), pruned to only the columns + // a transition constraint reads at the next row (the AIR transition window). + // Empty (width 0) when the AIR reads no next-row columns. + pub trace_ood_next_evaluations: Table, // Commitments to Hᵢ pub composition_poly_root: Commitment, // Hᵢ(z^N) diff --git a/crypto/stark/src/prover.rs b/crypto/stark/src/prover.rs index 7fa560e5c..69fab1619 100644 --- a/crypto/stark/src/prover.rs +++ b/crypto/stark/src/prover.rs @@ -1458,8 +1458,16 @@ pub trait IsStarkProver< let gamma = transcript.sample_field_element(); let n_terms_composition_poly = round_2_result.lde_composition_poly_evaluations.len(); - let num_terms_trace = - air.context().transition_offsets.len() * air.step_size() * air.context().trace_columns; + let num_eval_points = air.context().transition_offsets.len() * air.step_size(); + let next_row_cols = air.trace_ood_next_row_columns(); + // g·z pruning: only the current-row block (all columns) plus the masked + // next-row columns get an opening / DEEP coefficient. + let num_terms_trace = crate::ood::num_surviving_trace_openings( + air.context().trace_columns, + num_eval_points, + air.step_size(), + next_row_cols.len(), + ); // <<<< Receive challenges: 𝛾, 𝛾' let mut deep_composition_coefficients: Vec<_> = @@ -1467,12 +1475,19 @@ pub trait IsStarkProver< .take(n_terms_composition_poly + num_terms_trace) .collect(); - let trace_term_coeffs: Vec<_> = deep_composition_coefficients + let trace_term_powers: Vec<_> = deep_composition_coefficients .drain(..num_terms_trace) - .collect::>() - .chunks(air.context().transition_offsets.len() * air.step_size()) - .map(|chunk| chunk.to_vec()) .collect(); + // Rectangular W×num_eval_points grid with the sampled powers at surviving + // positions and zeros at pruned next-row positions, so the DEEP loop + // below (and the GPU path) stay unchanged — zero-coefficient terms vanish. + let trace_term_coeffs = crate::ood::build_pruned_trace_term_coeffs( + &trace_term_powers, + air.context().trace_columns, + num_eval_points, + air.step_size(), + &next_row_cols, + ); // <<<< Receive challenges: 𝛾ⱼ, 𝛾ⱼ' let gammas = deep_composition_coefficients; @@ -3103,11 +3118,21 @@ pub trait IsStarkProver< #[cfg(feature = "instruments")] let round_3_dur = t_r3.elapsed(); - // >>>> Send values: tⱼ(zgᵏ) - let trace_ood_evaluations_columns = round_3_result.trace_ood_evaluations.columns(); - for col in trace_ood_evaluations_columns.iter() { - for elem in col.iter() { - transcript.append_field_element(elem); + // >>>> Send values: tⱼ(zgᵏ). g·z pruning: split the full OOD table into + // the current-row block (all columns) and the pruned next-row block + // (masked columns only), and absorb only the surviving values — the + // verifier absorbs the identical two blocks in the same order. + let ood_next_row_cols = air.trace_ood_next_row_columns(); + let (ood_block0, ood_block1) = crate::ood::split_ood_blocks( + &round_3_result.trace_ood_evaluations, + air.step_size(), + &ood_next_row_cols, + ); + for block in [&ood_block0, &ood_block1] { + for col in block.columns().iter() { + for elem in col.iter() { + transcript.append_field_element(elem); + } } } @@ -3161,8 +3186,9 @@ pub trait IsStarkProver< lde_trace_aux_merkle_root: round_1_result.aux.as_ref().map(|x| x.root), // For preprocessed tables: commitment to precomputed columns only lde_trace_precomputed_merkle_root: round_1_result.main.precomputed_root, - // tⱼ(zgᵏ) - trace_ood_evaluations: round_3_result.trace_ood_evaluations, + // tⱼ(zgᵏ): current-row block + pruned next-row block. + trace_ood_evaluations: ood_block0, + trace_ood_next_evaluations: ood_block1, // [H₁] and [H₂] composition_poly_root: round_2_result.composition_poly_root, // Hᵢ(z^N) diff --git a/crypto/stark/src/tests/bus_tests/soundness_tests.rs b/crypto/stark/src/tests/bus_tests/soundness_tests.rs index 652f5e87d..f14907a9d 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/crypto/stark/src/tests/bus_tests/soundness_tests.rs @@ -15,6 +15,7 @@ use crate::examples::multi_table_lookup::{ }; use crate::proof::options::ProofOptions; use crate::prover::{IsStarkProver, Prover}; +use crate::table::Table; use crate::test_utils::multi_prove_ram; use crate::trace::TraceTable; use crate::traits::AIR; @@ -827,6 +828,170 @@ fn test_tampered_acc_ood_evaluation() { ); } +/// A proof whose OOD trace-evaluation table has the wrong shape is rejected. +/// +/// The table's dimensions are a public function of the AIR (transition offsets +/// x step_size rows, main+aux columns), so the verifier derives the expected +/// shape from AIR metadata and refuses any proof whose table does not match -- +/// a malicious prover cannot reshape it (e.g. drop a column) to dodge a check. +#[test_log::test] +fn test_malformed_ood_table_shape_rejected() { + // Same valid trace as `test_tampered_acc_ood_evaluation`: CPU sends (5,3,8). + let mut cpu_trace = TraceTable::from_columns_main( + vec![ + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // add_flag + vec![FE::zero(); 4], // mul_flag + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + ], + 1, + ); + let mut add_trace = TraceTable::from_columns_main( + vec![ + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // multiplicity = 1 + ], + 1, + ); + let mut mul_trace = TraceTable::from_columns_main(vec![vec![FE::zero(); 4]; 4], 1); + + let proof_options = ProofOptions::default_test_options(); + let cpu_air = new_cpu_air_with_lookup(&proof_options); + let add_air = new_add_air_with_lookup(&proof_options); + let mul_air = new_mul_air_with_lookup(&proof_options); + + let air_trace_pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&cpu_air, &mut cpu_trace, &()), + (&add_air, &mut add_trace, &()), + (&mul_air, &mut mul_trace, &()), + ]; + + let mut multi_proof = + multi_prove_ram(air_trace_pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + + // Drop one column from the ADD table's OOD evaluations while keeping the + // table internally consistent (data length matches the new width), so the + // rejection is the AIR-shape guard, not an out-of-bounds panic. + let add_proof = &mut multi_proof.proofs[1]; + let old = &add_proof.trace_ood_evaluations; + assert!(old.width >= 1, "OOD table must have at least one column"); + let new_width = old.width - 1; + let mut new_data = Vec::with_capacity(new_width * old.height); + for row in 0..old.height { + let full = old.get_row(row); + new_data.extend_from_slice(&full[..new_width]); + } + add_proof.trace_ood_evaluations = Table::new(new_data, new_width); + + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &add_air, &mul_air]; + + assert!( + !Verifier::multi_verify( + &airs, + &multi_proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + ), + "Proof with a wrong-shaped OOD table must be rejected" + ); +} + +/// The transition window (`trace_ood_next_row_columns`) of a LogUp table is +/// exactly the accumulator column — the sole column read at the next row after +/// forward accumulation — expressed as a full-width `[main | aux]` index. +#[test_log::test] +fn test_trace_ood_next_row_columns_is_accumulator_only() { + let proof_options = ProofOptions::default_test_options(); + let add_air = new_add_air_with_lookup(&proof_options); + let (main, aux) = add_air.trace_layout(); + + // All ADD interactions are absorbed, so the single aux column is the + // accumulator; its full-width index is `main + (aux - 1)`. + let next = add_air.trace_ood_next_row_columns(); + assert_eq!(next, vec![main + (aux - 1)]); + + // Every returned index addresses a real column within the concatenated width. + for &c in &next { + assert!( + c < main + aux, + "next-row column {c} out of width {main}+{aux}" + ); + } +} + +/// The g·z pruning actually shrinks the proof: a LogUp table opens every column +/// at z (the current-row block) but only the accumulator at the next row. +#[test_log::test] +fn test_gz_pruning_reduces_next_row_openings() { + let mut cpu_trace = TraceTable::from_columns_main( + vec![ + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // add_flag + vec![FE::zero(); 4], // mul_flag + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + ], + 1, + ); + let mut add_trace = TraceTable::from_columns_main( + vec![ + vec![FE::from(5), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(3), FE::zero(), FE::zero(), FE::zero()], + vec![FE::from(8), FE::zero(), FE::zero(), FE::zero()], + vec![FE::one(), FE::zero(), FE::zero(), FE::zero()], // multiplicity = 1 + ], + 1, + ); + let mut mul_trace = TraceTable::from_columns_main(vec![vec![FE::zero(); 4]; 4], 1); + + let proof_options = ProofOptions::default_test_options(); + let cpu_air = new_cpu_air_with_lookup(&proof_options); + let add_air = new_add_air_with_lookup(&proof_options); + let mul_air = new_mul_air_with_lookup(&proof_options); + + let air_trace_pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&cpu_air, &mut cpu_trace, &()), + (&add_air, &mut add_trace, &()), + (&mul_air, &mut mul_trace, &()), + ]; + + let multi_proof = + multi_prove_ram(air_trace_pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + + // ADD table: 4 main + 1 aux (accumulator). The current-row block opens all + // columns; the next-row block opens only the accumulator. + let add_proof = &multi_proof.proofs[1]; + let (main, aux) = add_air.trace_layout(); + assert_eq!(add_proof.trace_ood_evaluations.width, main + aux); + assert_eq!(add_proof.trace_ood_next_evaluations.width, 1); + assert!( + add_proof.trace_ood_next_evaluations.width < add_proof.trace_ood_evaluations.width, + "next-row OOD block must be pruned below the full width" + ); + + // The pruned proof still verifies. + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &add_air, &mul_air]; + assert!(Verifier::multi_verify( + &airs, + &multi_proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + )); +} + // ============================================================================= // Invalid bus public inputs // ============================================================================= diff --git a/crypto/stark/src/traits.rs b/crypto/stark/src/traits.rs index c28f831a2..0aec97a2a 100644 --- a/crypto/stark/src/traits.rs +++ b/crypto/stark/src/traits.rs @@ -198,6 +198,27 @@ pub trait AIR: Send + Sync { self.trace_layout().1 } + /// The full-width trace column indices that transition constraints read at + /// the *next* row (offset 1) — lambda_vm's fine-grained analogue of + /// Plonky3's transition window (a whole-row "does this AIR use the next + /// row?" flag). Only these columns need an OOD opening at `g·z`; every other + /// column is opened solely at `z`. The set is a public function of the AIR, + /// computed identically by prover and verifier, so the pruned OOD shape is + /// never taken from the (prover-controlled) proof. + /// + /// Indices are into the concatenated `[main | aux]` column space and must be + /// strictly less than `trace_layout().0 + trace_layout().1`. + /// + /// The default is **conservative**: every column is opened at the next row, + /// i.e. no pruning, matching the pre-pruning behaviour. An AIR that reads the + /// next row therefore stays correct without overriding. Override with the + /// exact read set only when you know which columns a transition constraint + /// references at offset 1 — returning too small a set is a soundness bug. + fn trace_ood_next_row_columns(&self) -> Vec { + let (main, aux) = self.trace_layout(); + (0..main + aux).collect() + } + fn composition_poly_degree_bound(&self, trace_length: usize) -> usize; /// Evaluates the transitions corresponding to an evaluation frame at the diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index fdee3d2ff..38663ad78 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -11,6 +11,7 @@ use crate::{ domain::new_verifier_domain, lookup::{LOGUP_CHALLENGE_ALPHA, LOGUP_NUM_CHALLENGES, compute_alpha_powers}, proof::stark::{DeepPolynomialOpening, MultiProof, PolynomialOpenings}, + table::Table, }; use crypto::{fiat_shamir::is_transcript::IsStarkTranscript, merkle_tree::proof::Proof}; #[cfg(not(feature = "test_fiat_shamir"))] @@ -107,6 +108,42 @@ pub trait IsStarkVerifier< { crate::profile_markers::STEP_VERIFY_CLAIMED_COMPOSITION_POLYNOMIAL }, >(); let trace_length = proof.trace_length; + + // Soundness (I3): both OOD blocks' shapes are a public function of the + // AIR, never of the (prover-controlled) proof. The current-row block + // opens every column over `step_size` rows; the next-row block opens only + // the transition-window columns over the remaining rows (and is empty + // when there are none). Reject any mismatch before using either block, so + // a malicious prover cannot reshape them to dodge a check or desync the + // frame reconstruction below. + let expected_ood_width = air.trace_layout().0 + air.num_auxiliary_rap_columns(); + let step_size = air.step_size(); + let num_eval_points = air.context().transition_offsets.len() * step_size; + let next_row_cols = air.trace_ood_next_row_columns(); + let expected_next_width = next_row_cols.len(); + let expected_next_height = if expected_next_width == 0 { + 0 + } else { + num_eval_points - step_size + }; + if proof.trace_ood_evaluations.width != expected_ood_width + || proof.trace_ood_evaluations.height != step_size + || proof.trace_ood_next_evaluations.width != expected_next_width + || proof.trace_ood_next_evaluations.height != expected_next_height + { + return false; + } + + // Reconstruct the full current+next-row OOD grid (surviving values placed, + // pruned next-row entries zero -- those are never read by any constraint). + let ood_full = crate::ood::reconstruct_ood_full( + &proof.trace_ood_evaluations, + &proof.trace_ood_next_evaluations, + num_eval_points, + step_size, + &next_row_cols, + ); + let boundary_constraints = air.boundary_constraints( &proof.public_inputs, &challenges.rap_challenges, @@ -167,8 +204,9 @@ pub trait IsStarkVerifier< .map(|((num, den), beta)| num * den * beta) .fold(FieldElement::::zero(), |acc, x| acc + x); - let num_main_trace_columns = - proof.trace_ood_evaluations.width - air.num_auxiliary_rap_columns(); + // Shape is AIR-derived (validated against the proof above), so use the + // AIR's main width directly rather than trusting the proof dimensions. + let num_main_trace_columns = main_trace_width; let logup_alpha_powers: Vec> = if challenges.rap_challenges.len() > LOGUP_CHALLENGE_ALPHA { @@ -191,8 +229,9 @@ pub trait IsStarkVerifier< None => FieldElement::zero(), }; - let ood_frame = - (proof.trace_ood_evaluations).into_frame(num_main_trace_columns, air.step_size()); + // Frame from the reconstructed full grid: the next-row step reads only + // its transition-window columns; the zero-filled remainder is never read. + let ood_frame = ood_full.into_frame(num_main_trace_columns, step_size); let transition_evaluation_context = TransitionEvaluationContext::new_verifier( &ood_frame, &challenges.rap_challenges, @@ -269,9 +308,27 @@ pub trait IsStarkVerifier< FieldElement: AsBytes + Sync + Send, { crate::profile_markers::step_marker::<{ crate::profile_markers::STEP_VERIFY_FRI }>(); + // g·z pruning: rebuild the full OOD grid from the two proof blocks so + // the DEEP reconstruction can skip pruned next-row openings. + let step_size = air.step_size(); + let num_eval_points = air.context().transition_offsets.len() * step_size; + let next_row_cols = air.trace_ood_next_row_columns(); + let ood_full = crate::ood::reconstruct_ood_full( + &proof.trace_ood_evaluations, + &proof.trace_ood_next_evaluations, + num_eval_points, + step_size, + &next_row_cols, + ); + let next_row_flags = crate::ood::next_row_col_flags(ood_full.width, &next_row_cols); let (deep_poly_evaluations, deep_poly_evaluations_sym) = match Self::reconstruct_deep_composition_poly_evaluations_for_all_queries( - challenges, domain, proof, + challenges, + domain, + proof, + &ood_full, + &next_row_flags, + step_size, ) { Some(pair) => pair, None => return false, @@ -610,10 +667,14 @@ pub trait IsStarkVerifier< openings_ok & terminal_ok } + #[allow(clippy::too_many_arguments)] fn reconstruct_deep_composition_poly_evaluations_for_all_queries( challenges: &Challenges, domain: &VerifierDomain, proof: &StarkProof, + ood_full: &Table, + next_row_flags: &[bool], + step_size: usize, ) -> Option> { let num_queries = challenges.iotas.len(); @@ -662,6 +723,9 @@ pub trait IsStarkVerifier< &lde_base, lde_aux, &opening.composition_poly.evaluations, + ood_full, + next_row_flags, + step_size, )?); // Mirror for the symmetric query point. @@ -686,11 +750,15 @@ pub trait IsStarkVerifier< &lde_base_sym, lde_aux_sym, &opening.composition_poly.evaluations_sym, + ood_full, + next_row_flags, + step_size, )?); } Some((deep_poly_evaluations, deep_poly_evaluations_sym)) } + #[allow(clippy::too_many_arguments)] fn reconstruct_deep_composition_poly_evaluation( proof: &StarkProof, evaluation_point: &FieldElement, @@ -699,9 +767,12 @@ pub trait IsStarkVerifier< lde_trace_base_evaluations: &[FieldElement], lde_trace_aux_evaluations: &[FieldElement], lde_composition_poly_parts_evaluation: &[FieldElement], + ood_full: &Table, + next_row_flags: &[bool], + step_size: usize, ) -> Option> { - let ood_evaluations_table_height = proof.trace_ood_evaluations.height; - let ood_evaluations_table_width = proof.trace_ood_evaluations.width; + let ood_evaluations_table_height = ood_full.height; + let ood_evaluations_table_width = ood_full.width; let trace_term_coeffs = &challenges.trace_term_coeffs; // Runtime guard: a malformed proof may supply opening evaluations whose @@ -733,10 +804,18 @@ pub trait IsStarkVerifier< let trace_term = (0..ood_evaluations_table_width) .zip(&challenges.trace_term_coeffs) .fold(FieldElement::zero(), |trace_terms, (col_idx, coeff_row)| { + let opened_next_row = next_row_flags[col_idx]; let trace_i = (0..ood_evaluations_table_height).zip(coeff_row).fold( FieldElement::zero(), |trace_t, (row_idx, coeff)| { - let ood_val = &proof.trace_ood_evaluations.get_row(row_idx)[col_idx]; + // g·z pruning: the next-row block opens only transition- + // window columns. Skip every other next-row opening — its + // coefficient is zero, so the term is vacuous, and skipping + // it is where the verifier/recursion cycle saving lands. + if row_idx >= step_size && !opened_next_row { + return trace_t; + } + let ood_val = &ood_full.get_row(row_idx)[col_idx]; // Stay in base when we can: F: IsSubFieldOf gives F - E -> E. let diff: FieldElement = if col_idx < num_base { &lde_trace_base_evaluations[col_idx] - ood_val @@ -1047,11 +1126,16 @@ pub trait IsStarkVerifier< &domain.coset_offset, ); - // <<<< Receive values: tⱼ(zgᵏ) - let trace_ood_evaluations_columns = proof.trace_ood_evaluations.columns(); - for col in trace_ood_evaluations_columns.iter() { - for elem in col.iter() { - transcript.append_field_element(elem); + // <<<< Receive values: tⱼ(zgᵏ). Absorb the two pruned OOD blocks in the + // same order the prover sent them (current-row block, then next-row block). + for block in [ + &proof.trace_ood_evaluations, + &proof.trace_ood_next_evaluations, + ] { + for col in block.columns().iter() { + for elem in col.iter() { + transcript.append_field_element(elem); + } } } // <<<< Receive value: Hᵢ(z^N) @@ -1064,8 +1148,15 @@ pub trait IsStarkVerifier< // =================================== let num_terms_composition_poly = proof.composition_poly_parts_ood_evaluation.len(); - let num_terms_trace = - air.context().transition_offsets.len() * air.step_size() * air.context().trace_columns; + let num_eval_points = air.context().transition_offsets.len() * air.step_size(); + let next_row_cols = air.trace_ood_next_row_columns(); + // Must match the prover's g·z pruning exactly (same AIR metadata). + let num_terms_trace = crate::ood::num_surviving_trace_openings( + air.context().trace_columns, + num_eval_points, + air.step_size(), + next_row_cols.len(), + ); let gamma = transcript.sample_field_element(); // <<<< Receive challenges: 𝛾, 𝛾' @@ -1074,12 +1165,16 @@ pub trait IsStarkVerifier< .take(num_terms_composition_poly + num_terms_trace) .collect(); - let trace_term_coeffs: Vec<_> = deep_composition_coefficients + let trace_term_powers: Vec<_> = deep_composition_coefficients .drain(..num_terms_trace) - .collect::>() - .chunks(air.context().transition_offsets.len() * air.step_size()) - .map(|chunk| chunk.to_vec()) .collect(); + let trace_term_coeffs = crate::ood::build_pruned_trace_term_coeffs( + &trace_term_powers, + air.context().trace_columns, + num_eval_points, + air.step_size(), + &next_row_cols, + ); // <<<< Receive challenges: 𝛾ⱼ, 𝛾ⱼ' let gammas = deep_composition_coefficients;