diff --git a/crypto/stark/src/tests/aux_opening_width_tests.rs b/crypto/stark/src/tests/aux_opening_width_tests.rs new file mode 100644 index 000000000..925f8111c --- /dev/null +++ b/crypto/stark/src/tests/aux_opening_width_tests.rs @@ -0,0 +1,715 @@ +//! Regression tests for the **main↔aux** term of the opening-width pin +//! (`verifier::trace_opening_widths_well_formed`); the precomputed↔main term and +//! the direct guard tests live in `tests::opening_width_tests`. +//! +//! Everything here is attacker-side — a hostile AIR *declaration* plus the trace +//! it implies. Unlike the precomputed instance, this one needs **no prover +//! change at all**: both sides absorb main-root-then-aux-root either way, so the +//! transcripts agree and an untouched prover produces the forgery. +//! +//! Mechanism +//! --------- +//! `verify_trace_openings` only Merkle-checks each of the three trace openings +//! against its own root; it never compared the aux opening width against +//! `air.num_auxiliary_rap_columns()`. The only width constraint was, in +//! `reconstruct_deep_composition_poly_evaluation_pair`: +//! +//! num_base + num_aux == ood_width +//! +//! with `num_base` and `num_aux` read off the *prover-supplied openings*. The +//! **total** is pinned (`ood_blocks_well_formed`) but the **split** was not, so a +//! prover could commit the last `k` main columns in the AUXILIARY tree instead. +//! +//! Why that breaks LogUp: the main root is absorbed in round 1 phase A, the +//! shared LogUp challenges `z`/`alpha` are sampled immediately after, and the aux +//! root only in phase C. A column moved into the aux tree is therefore chosen +//! AFTER `z` and `alpha` are known, which collapses the multiset equality into a +//! single scalar equation the prover solves — no fingerprint collision needed. +//! +//! Vehicle: `LogReadOnlyRAP`, the in-repo continuous read-only-memory AIR whose +//! memory consistency rests entirely on LogUp. Honest layout (5, 1): +//! main = [a, v, a', v', m], aux = [s]. The attacker declares (4, 2): +//! main = [a, v, a', v'], aux = [m, s] — same global column order, same +//! constraints, same OOD width, so an unpinned verifier cannot tell. The +//! multiplicity column `m` is then picked after `z`/`alpha`. The moved column is +//! the multiplicity column on purpose: `traits.rs:182-188` documents the trailing +//! main columns of every preprocessed table as exactly the multiplicities. +//! +//! On stock `main` the two break tests below are ACCEPTED, including over the +//! rkyv wire through `multi_verify_archived` (the recursion-guest path). The +//! three controls are rejected on both, and discriminate the harness. + +use std::marker::PhantomData; + +use crate::constraints::{ + boundary::{BoundaryConstraint, BoundaryConstraints}, + builder::{ + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, + run_transition_prover, run_transition_verifier, + }, +}; +use crate::context::AirContext; +use crate::examples::read_only_memory_logup::{ + LogReadOnlyPublicInputs, LogReadOnlyRAP, read_only_logup_trace, +}; +use crate::proof::options::ProofOptions; +use crate::proof::view::StarkProofView; +use crate::prover::{IsStarkProver, Prover}; +use crate::trace::TraceTable; +use crate::traits::{AIR, TransitionEvaluationContext}; +use crate::verifier::{IsStarkVerifier, Verifier}; +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use math::field::element::FieldElement; +use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField; +use math::field::goldilocks::GoldilocksField; + +type F = GoldilocksField; +type E = Degree3GoldilocksExtensionField; +type Felt = FieldElement; +type Ext = FieldElement; + +// ============================================================================= +// The hostile constraint body: byte-for-byte `LogReadOnlyRAPConstraints` with +// the multiplicity column re-addressed from main[4] to aux[0] and the LogUp +// accumulator from aux[0] to aux[1]. Same values, same degrees, same meta. +// ============================================================================= + +pub struct SplitLogUpConstraints; + +impl ConstraintSet for SplitLogUpConstraints { + fn eval>(&self, b: &mut B) { + let a_sorted_0 = b.main(0, 2); + let a_sorted_1 = b.main(1, 2); + let v_sorted_0 = b.main(0, 3); + let v_sorted_1 = b.main(1, 3); + let one = b.one(); + let addr_diff = a_sorted_1 - a_sorted_0; + + b.emit_base_rows( + 0, + RowDomain::except_last(1), + addr_diff.clone() * (addr_diff.clone() - one.clone()), + ); + b.emit_base_rows( + 1, + RowDomain::except_last(1), + (v_sorted_1 - v_sorted_0) * (addr_diff - one), + ); + + // ---- the only difference: s is aux[1], m is aux[0] (was main[4]) ---- + let s0 = b.aux(0, 1); + let s1 = b.aux(1, 1); + let z = b.challenge(0); + let alpha = b.challenge(1); + let a1 = b.main(1, 0); + let v1 = b.main(1, 1); + let a_sorted_1 = b.main(1, 2); + let v_sorted_1 = b.main(1, 3); + let m = b.aux(1, 0); + let unsorted_term = -(a1 + v1 * alpha.clone()) + z.clone(); + let sorted_term = -(a_sorted_1 + v_sorted_1 * alpha) + z; + b.emit_ext_rows( + 2, + RowDomain::except_last(1), + s0 * unsorted_term.clone() * sorted_term.clone() + m * unsorted_term.clone() + - sorted_term.clone() + - s1 * unsorted_term * sorted_term, + ); + } +} + +/// How the attacker fills the moved multiplicity column. +#[derive(Clone)] +pub enum MPlan { + /// Honest multiplicities, merely committed in the wrong tree. + Honest(Vec), + /// Honest multiplicities except index `idx`, which is SOLVED after `z`, + /// `alpha` are known so the LogUp accumulator still lands on zero. + Forge { base: Vec, idx: usize }, +} + +pub struct SplitLogUpAIR { + context: AirContext, + meta: Vec, + plan: MPlan, + /// Records the challenge-dependent multiplicity the attack solved for. + pub forged_value: std::sync::Mutex>, + /// Records the committed multiplicity column and the (z, alpha) it was + /// solved against, so a test can replay the LogUp identity off-protocol. + pub committed_m: std::sync::Mutex, Ext, Ext)>>, + phantom: PhantomData<(F, E)>, +} + +impl SplitLogUpAIR { + pub fn with_plan(proof_options: &ProofOptions, plan: MPlan) -> Self { + let mut air = ::new(proof_options); + air.plan = plan; + air + } +} + +impl AIR for SplitLogUpAIR { + type Field = F; + type FieldExtension = E; + type PublicInputs = LogReadOnlyPublicInputs; + + fn step_size(&self) -> usize { + 1 + } + + fn new(proof_options: &ProofOptions) -> Self { + let meta = ConstraintSet::::meta(&SplitLogUpConstraints); + let context = AirContext { + proof_options: proof_options.clone(), + trace_columns: 6, + transition_offsets: vec![0, 1], + num_transition_constraints: meta.len(), + }; + Self { + context, + meta, + plan: MPlan::Honest(Vec::new()), + forged_value: std::sync::Mutex::new(None), + committed_m: std::sync::Mutex::new(None), + phantom: PhantomData, + } + } + + /// Runs AFTER the main root is absorbed and AFTER `z`, `alpha` are sampled. + /// Fills aux[0] = m (the moved main column) and aux[1] = s. + fn build_auxiliary_trace( + &self, + trace: &mut TraceTable, + challenges: &[Ext], + ) -> Option> { + let cols = trace.columns_main(); + let (a, v, a_sorted, v_sorted) = (&cols[0], &cols[1], &cols[2], &cols[3]); + let z = &challenges[0]; + let alpha = &challenges[1]; + let n = trace.num_rows(); + + // u_i = 1/(z - (a_i + alpha*v_i)) ; t_i = 1/(z - (a'_i + alpha*v'_i)) + let u: Vec = (0..n) + .map(|i| (-(&a[i] + &v[i] * alpha) + z).inv().unwrap()) + .collect(); + let t: Vec = (0..n) + .map(|i| (-(&a_sorted[i] + &v_sorted[i] * alpha) + z).inv().unwrap()) + .collect(); + + let m: Vec = match &self.plan { + MPlan::Honest(base) => base.iter().map(|x| x.to_extension()).collect(), + MPlan::Forge { base, idx } => { + let mut m: Vec = base.iter().map(|x| x.to_extension()).collect(); + // Solve sum_i m_i t_i = sum_i u_i for m_idx. + let mut rhs = u.iter().fold(Ext::zero(), |acc, x| acc + x); + for i in 0..n { + if i != *idx { + rhs = rhs - &m[i] * &t[i]; + } + } + let solved = rhs * t[*idx].inv().unwrap(); + *self.forged_value.lock().unwrap() = Some(solved); + m[*idx] = solved; + m + } + }; + + *self.committed_m.lock().unwrap() = Some((m.clone(), *z, *alpha)); + + let mut s = Vec::with_capacity(n); + s.push(&m[0] * &t[0] - &u[0]); + for i in 0..n - 1 { + let next = &s[i] + &m[i + 1] * &t[i + 1] - &u[i + 1]; + s.push(next); + } + + for i in 0..n { + trace.set_aux(i, 0, m[i]); + trace.set_aux(i, 1, s[i]); + } + None + } + + /// The lie: 4 main columns, 2 aux columns (honest AIR says 5 and 1). + fn trace_layout(&self) -> (usize, usize) { + (4, 2) + } + + fn boundary_constraints( + &self, + pub_inputs: &Self::PublicInputs, + rap_challenges: &[Ext], + _bus_public_inputs: Option<&crate::lookup::BusPublicInputs>, + trace_length: usize, + ) -> BoundaryConstraints { + let a0 = &pub_inputs.a0; + let v0 = &pub_inputs.v0; + let a_sorted_0 = &pub_inputs.a_sorted_0; + let v_sorted_0 = &pub_inputs.v_sorted_0; + let m0 = &pub_inputs.m0; + let z = &rap_challenges[0]; + let alpha = &rap_challenges[1]; + + let c1 = BoundaryConstraint::new_main(0, 0, a0.to_extension()); + let c2 = BoundaryConstraint::new_main(1, 0, v0.to_extension()); + let c3 = BoundaryConstraint::new_main(2, 0, a_sorted_0.to_extension()); + let c4 = BoundaryConstraint::new_main(3, 0, v_sorted_0.to_extension()); + // main[4] under the honest layout -> aux[0] here. Same GLOBAL index 4, + // which is all the verifier's `main_trace_width + col` mapping sees. + let c5 = BoundaryConstraint::new_aux(0, 0, m0.to_extension()); + + let unsorted_term = (-(a0 + v0 * alpha) + z).inv().unwrap(); + let sorted_term = (-(a_sorted_0 + v_sorted_0 * alpha) + z).inv().unwrap(); + let p0_value = m0 * sorted_term - unsorted_term; + + let c_aux1 = BoundaryConstraint::new_aux(1, 0, p0_value); + let c_aux2 = BoundaryConstraint::new_aux(1, trace_length - 1, Ext::zero()); + + BoundaryConstraints::from_constraints(vec![c1, c2, c3, c4, c5, c_aux1, c_aux2]) + } + + fn constraints_meta(&self) -> &[ConstraintMeta] { + &self.meta + } + + fn compute_transition_prover( + &self, + evaluation_context: &TransitionEvaluationContext, + base_evals: &mut [Felt], + ext_evals: &mut [Ext], + ) { + run_transition_prover( + &SplitLogUpConstraints, + evaluation_context, + base_evals, + ext_evals, + ); + } + + fn compute_transition( + &self, + evaluation_context: &TransitionEvaluationContext, + ) -> Vec { + run_transition_verifier( + &SplitLogUpConstraints, + evaluation_context, + self.num_base_transition_constraints(), + self.num_transition_constraints(), + ) + } + + fn num_base_transition_constraints(&self) -> usize { + num_base_from_meta(&ConstraintSet::::meta(&SplitLogUpConstraints)) + } + + fn context(&self) -> &AirContext { + &self.context + } + + fn composition_poly_degree_bound(&self, trace_length: usize) -> usize { + trace_length * 2 + } +} + +// ============================================================================= +// Fixtures +// ============================================================================= + +/// The exact data of the in-repo happy-path test +/// (`air_tests.rs::test_prove_read_only_memory_logup`): a continuous read-only +/// memory over addresses 1..=5. +fn honest_reads() -> (Vec, Vec) { + ( + vec![3, 2, 2, 3, 4, 5, 1, 3] + .into_iter() + .map(Felt::from) + .collect(), + vec![30, 20, 20, 30, 40, 50, 10, 30] + .into_iter() + .map(Felt::from) + .collect(), + ) +} + +fn public_inputs() -> LogReadOnlyPublicInputs { + LogReadOnlyPublicInputs { + a0: Felt::from(3), + v0: Felt::from(30), + a_sorted_0: Felt::from(1), + v_sorted_0: Felt::from(10), + m0: Felt::from(1), + } +} + +/// Split an honest 5-main-column LogUp trace into the attacker's shape: +/// 4 main columns + 2 (zeroed) aux columns. Returns the m column separately. +fn split_trace(addresses: Vec, values: Vec) -> (TraceTable, Vec) { + let honest: TraceTable = read_only_logup_trace(addresses, values); + let cols = honest.columns_main(); + let n = cols[0].len(); + let m = cols[4].clone(); + let main = vec![ + cols[0].clone(), + cols[1].clone(), + cols[2].clone(), + cols[3].clone(), + ]; + let aux = vec![vec![Ext::zero(); n], vec![Ext::zero(); n]]; + (TraceTable::from_columns(main, aux, 1), m) +} + +fn opts() -> ProofOptions { + ProofOptions::default_test_options() +} + +fn honest_air() -> LogReadOnlyRAP { + LogReadOnlyRAP::::new(&opts()) +} + +fn tr() -> DefaultTranscript { + DefaultTranscript::::new(&[]) +} + +// ============================================================================= +// The two AIRs are indistinguishable to the verifier except for the split, so +// nothing but an explicit width pin can tell them apart. +// ============================================================================= + +#[test_log::test] +fn split_declaration_differs_from_the_honest_air_only_in_the_layout() { + let h = honest_air(); + let a = SplitLogUpAIR::with_plan(&opts(), MPlan::Honest(Vec::new())); + assert_eq!( + format!("{:?}", h.constraints_meta()), + format!("{:?}", a.constraints_meta()), + "meta must match" + ); + assert_eq!(h.context().trace_columns, a.context().trace_columns); + assert_eq!( + h.context().transition_offsets, + a.context().transition_offsets + ); + assert_eq!( + h.num_transition_constraints(), + a.num_transition_constraints() + ); + assert_eq!( + h.num_base_transition_constraints(), + a.num_base_transition_constraints() + ); + assert_eq!( + h.trace_ood_next_row_columns(), + a.trace_ood_next_row_columns() + ); + assert_eq!( + h.composition_poly_degree_bound(8), + a.composition_poly_degree_bound(8) + ); + assert_eq!(h.has_aux_trace(), a.has_aux_trace()); + assert_eq!(h.has_trace_interaction(), a.has_trace_interaction()); + // The ONLY divergence: + assert_eq!(h.trace_layout(), (5, 1)); + assert_eq!(a.trace_layout(), (4, 2)); + assert_eq!(h.num_auxiliary_rap_columns(), 1); + assert_eq!(a.num_auxiliary_rap_columns(), 2); + println!("AUXSPLIT/0 honest layout (5,1) attacker layout (4,2) — everything else identical"); +} + +// ============================================================================= +// The structural case: a proof whose aux opening is 2 columns wide, verified +// against an AIR that declares exactly 1. Accepted on stock `main`, and it needs +// no forgery at all — the trace here is honest. +// ============================================================================= + +#[test_log::test] +fn mis_split_aux_opening_is_rejected() { + let (addr, val) = honest_reads(); + let (mut trace, m) = split_trace(addr, val); + let pi = public_inputs(); + let attack_air = SplitLogUpAIR::with_plan(&opts(), MPlan::Honest(m)); + + let proof = Prover::prove(&attack_air, &mut trace, &pi, &mut tr()).expect("prove"); + + let aux_w = proof.deep_poly_openings[0] + .aux_trace_polys + .as_ref() + .unwrap() + .evaluations + .len(); + let main_w = proof.deep_poly_openings[0] + .main_trace_polys + .evaluations + .len(); + let h = honest_air(); + println!( + "AUXSPLIT/1 opening widths: main={main_w} aux={aux_w} AIR declares main={} aux={}", + h.trace_layout().0, + h.num_auxiliary_rap_columns() + ); + assert_eq!(main_w, 4); + assert_eq!(aux_w, 2); + assert_ne!(aux_w, h.num_auxiliary_rap_columns()); + + let accepted = Verifier::verify(&proof, &h, &mut tr()); + println!("AUXSPLIT/1 STOCK VERIFIER ACCEPTED MIS-SPLIT PROOF = {accepted}"); + assert!( + !accepted, + "the verifier must reject an aux opening wider than the AIR declares", + ); + + // Attribution: the rejection is the width pin's, not an incidental failure + // elsewhere in verification. A "rejected" verdict is only evidence if it + // comes from the guard under test. + assert!( + !Verifier::trace_opening_widths_well_formed( + &h, + StarkProofView::Owned(&proof), + h.options().fri_number_of_queries, + ), + "the rejection above must come from the opening-width guard", + ); +} + +// ============================================================================= +// CONTROL — the harness discriminates: corrupting one value in the (wrongly +// wide) aux opening must be rejected. Passes on stock `main` too. +// ============================================================================= + +#[test_log::test] +fn corrupted_aux_opening_is_rejected() { + let (addr, val) = honest_reads(); + let (mut trace, m) = split_trace(addr, val); + let pi = public_inputs(); + let attack_air = SplitLogUpAIR::with_plan(&opts(), MPlan::Honest(m)); + let proof = Prover::prove(&attack_air, &mut trace, &pi, &mut tr()).expect("prove"); + + let mut corrupted = proof.clone(); + corrupted.deep_poly_openings[0] + .aux_trace_polys + .as_mut() + .unwrap() + .evaluations[0] += Ext::one(); + let accepted = Verifier::verify(&corrupted, &honest_air(), &mut tr()); + println!("AUXSPLIT/CONTROL-A corrupted aux opening accepted = {accepted}"); + assert!(!accepted, "harness must discriminate"); +} + +// ============================================================================= +// The break: a FALSE statement, accepted on stock `main`. +// +// The read column contains address 3 -> 30 (rows 0, 3) AND address 3 -> 999999 +// (row 7). No single-valued read-only memory can serve both, so the LogUp +// multiset equality that this AIR exists to enforce is FALSE. With `m` moved +// into the aux tree the prover solves for m[1] AFTER seeing z, alpha, and the +// stock verifier accepts. +// ============================================================================= + +const BOGUS: u64 = 999999; + +#[test_log::test] +fn false_memory_read_under_aux_split_is_rejected() { + let (addr, mut val) = honest_reads(); + // Honest sorted memory table, built from the HONEST reads. + let (_, honest_m) = split_trace(addr.clone(), val.clone()); + let honest_trace: TraceTable = read_only_logup_trace(addr.clone(), val.clone()); + let sorted_a = honest_trace.columns_main()[2].clone(); + let sorted_v = honest_trace.columns_main()[3].clone(); + + // The lie: read #7 (address 3) now claims value 999999. + val[7] = Felt::from(BOGUS); + + // Sanity: the read multiset is now impossible for a single-valued memory. + let mut same_addr_values: Vec = Vec::new(); + for i in 0..addr.len() { + if addr[i] == Felt::from(3) && !same_addr_values.contains(&val[i]) { + same_addr_values.push(val[i]); + } + } + println!( + "AUXSPLIT/2 reads at address 3 claim {} distinct values: {same_addr_values:?}", + same_addr_values.len() + ); + assert!( + same_addr_values.len() > 1, + "the statement must be false: address 3 must carry two different values" + ); + + let n = addr.len(); + let main = vec![addr.clone(), val.clone(), sorted_a, sorted_v]; + let aux = vec![vec![Ext::zero(); n], vec![Ext::zero(); n]]; + let mut trace = TraceTable::::from_columns(main, aux, 1); + + let pi = public_inputs(); + let attack_air = SplitLogUpAIR::with_plan( + &opts(), + MPlan::Forge { + base: honest_m, + idx: 1, + }, + ); + let proof = Prover::prove(&attack_air, &mut trace, &pi, &mut tr()).expect("prove"); + + let forged = attack_air.forged_value.lock().unwrap().unwrap(); + println!("AUXSPLIT/2 solved multiplicity m[1] (challenge-dependent) = {forged:?}"); + + let accepted = Verifier::verify(&proof, &honest_air(), &mut tr()); + println!("AUXSPLIT/2 FALSE STATEMENT ACCEPTED BY STOCK VERIFIER = {accepted}"); + assert!( + !accepted, + "the verifier must reject a false statement carried by an aux mis-split", + ); + + // Attribution: the rejection is the width pin's, not an incidental failure + // elsewhere in verification. A "rejected" verdict is only evidence if it + // comes from the guard under test. + assert!( + !Verifier::trace_opening_widths_well_formed( + &honest_air(), + StarkProofView::Owned(&proof), + honest_air().options().fri_number_of_queries, + ), + "the rejection above must come from the opening-width guard", + ); + + // -------- the same forgery over the WIRE: rkyv-serialize and verify + // through `multi_verify_archived`, the read-in-place path the recursion + // guest uses. Proves this is a transmissible proof, not an in-process + // artefact, and that the archived path shares the hole. ----------------- + let multi = crate::proof::stark::MultiProof { + proofs: vec![proof.clone()], + }; + let bytes = rkyv::to_bytes::(&multi).unwrap(); + println!("AUXSPLIT/2 serialized forged proof: {} bytes", bytes.len()); + let archived = rkyv::access::< + crate::proof::stark::ArchivedMultiProof>, + rkyv::rancor::Error, + >(&bytes) + .unwrap(); + let h = honest_air(); + let airs: Vec< + &dyn AIR>, + > = vec![&h]; + let accepted_archived = + Verifier::multi_verify_archived(&airs, archived, &mut tr(), &Ext::zero()); + println!("AUXSPLIT/2 ARCHIVED (wire) PATH ACCEPTED = {accepted_archived}"); + assert!( + !accepted_archived, + "the archived (recursion-guest) path must reject it too", + ); + + // -------- diagnostic: the accepted LogUp identity is NOT a multiset + // equality, it holds only at the protocol's own (z, alpha). ------------- + let (m_committed, z, alpha) = attack_air.committed_m.lock().unwrap().clone().unwrap(); + let cols = trace.columns_main(); + let logup_residual = |z: &Ext, alpha: &Ext| -> Ext { + let mut acc = Ext::zero(); + for i in 0..n { + let u = (-(&cols[0][i] + &cols[1][i] * alpha) + z).inv().unwrap(); + let t = (-(&cols[2][i] + &cols[3][i] * alpha) + z).inv().unwrap(); + acc = acc + &m_committed[i] * t - u; + } + acc + }; + let at_protocol = logup_residual(&z, &alpha); + let z2 = z + Ext::from(7u64); + let a2 = alpha + Ext::from(11u64); + let at_fresh = logup_residual(&z2, &a2); + println!("AUXSPLIT/2 LogUp residual at the protocol's (z,alpha) = {at_protocol:?}"); + println!("AUXSPLIT/2 LogUp residual at a FRESH (z',alpha') = {at_fresh:?}"); + assert_eq!( + at_protocol, + Ext::zero(), + "the attack balances the bus at the sampled challenges" + ); + assert_ne!( + at_fresh, + Ext::zero(), + "…but not as a rational identity: the two multisets genuinely differ" + ); +} + +// ============================================================================= +// CONTROL — the SAME false trace, proven WITHOUT the split (honest layout, +// honest multiplicities in the main tree). `m` is then bound before z/alpha and +// the bus cannot be made to balance: the proof must be rejected (or the prover +// must refuse). Shows the acceptance above comes from the split, not from a hole +// in the AIR. Passes on stock `main` too. +// ============================================================================= + +#[test_log::test] +fn same_false_read_without_the_split_is_rejected() { + let (addr, mut val) = honest_reads(); + let honest_trace: TraceTable = read_only_logup_trace(addr.clone(), val.clone()); + let sorted_a = honest_trace.columns_main()[2].clone(); + let sorted_v = honest_trace.columns_main()[3].clone(); + let m = honest_trace.columns_main()[4].clone(); + val[7] = Felt::from(BOGUS); + + let n = addr.len(); + let main = vec![addr, val, sorted_a, sorted_v, m]; + let aux = vec![vec![Ext::zero(); n]]; + let mut trace = TraceTable::::from_columns(main, aux, 1); + let pi = public_inputs(); + let h = honest_air(); + + match Prover::prove(&h, &mut trace, &pi, &mut tr()) { + Ok(proof) => { + let accepted = Verifier::verify(&proof, &h, &mut tr()); + println!("AUXSPLIT/CONTROL-B no-split false trace accepted = {accepted}"); + assert!(!accepted, "control must be rejected"); + } + Err(e) => println!("AUXSPLIT/CONTROL-B no-split prover refused: {e:?}"), + } +} + +// ============================================================================= +// CONTROL — the split path is not a free pass: the SAME split declaration with +// HONEST multiplicities over the FALSE read column must be rejected. Only the +// challenge-dependent solve makes the forgery go through. Passes on stock `main` +// too. +// ============================================================================= + +#[test_log::test] +fn aux_split_without_the_challenge_solve_is_rejected() { + let (addr, mut val) = honest_reads(); + let honest_trace: TraceTable = read_only_logup_trace(addr.clone(), val.clone()); + let sorted_a = honest_trace.columns_main()[2].clone(); + let sorted_v = honest_trace.columns_main()[3].clone(); + let m = honest_trace.columns_main()[4].clone(); + val[7] = Felt::from(BOGUS); + + let n = addr.len(); + let main = vec![addr, val, sorted_a, sorted_v]; + let aux = vec![vec![Ext::zero(); n], vec![Ext::zero(); n]]; + let mut trace = TraceTable::::from_columns(main, aux, 1); + let pi = public_inputs(); + let attack_air = SplitLogUpAIR::with_plan(&opts(), MPlan::Honest(m)); + + match Prover::prove(&attack_air, &mut trace, &pi, &mut tr()) { + Ok(proof) => { + let accepted = Verifier::verify(&proof, &honest_air(), &mut tr()); + println!("AUXSPLIT/CONTROL-C split + honest m over false reads accepted = {accepted}"); + assert!(!accepted, "control must be rejected"); + } + Err(e) => println!("AUXSPLIT/CONTROL-C prover refused: {e:?}"), + } +} + +// ============================================================================= +// NON-VACUITY — the honest `LogReadOnlyRAP` (layout (5, 1), aux width 1) must +// still verify. A pin that rejected every aux opening would satisfy every +// rejection test above. +// ============================================================================= + +#[test_log::test] +fn honest_logup_rap_proof_still_verifies() { + let (addr, val) = honest_reads(); + let mut trace: TraceTable = read_only_logup_trace(addr, val); + let air = honest_air(); + let proof = Prover::prove(&air, &mut trace, &public_inputs(), &mut tr()).expect("prove"); + + assert!( + Verifier::verify(&proof, &air, &mut tr()), + "an honest LogUp proof must verify", + ); +} diff --git a/crypto/stark/src/tests/mod.rs b/crypto/stark/src/tests/mod.rs index 15b64d45a..468a4cd3c 100644 --- a/crypto/stark/src/tests/mod.rs +++ b/crypto/stark/src/tests/mod.rs @@ -1,4 +1,5 @@ pub mod air_tests; +pub mod aux_opening_width_tests; #[cfg(feature = "debug-checks")] pub mod bus_debug_tests; pub mod bus_tests; @@ -6,6 +7,7 @@ pub mod commitment_tests; pub mod domain_cache_stats; pub mod fri_tests; pub mod grinding_tests; +pub mod opening_width_tests; pub mod proof_options_tests; pub mod prove_verify_roundtrip_tests; pub mod prover_tests; diff --git a/crypto/stark/src/tests/opening_width_tests.rs b/crypto/stark/src/tests/opening_width_tests.rs new file mode 100644 index 000000000..db5764220 --- /dev/null +++ b/crypto/stark/src/tests/opening_width_tests.rs @@ -0,0 +1,532 @@ +//! Negative tests for the trace-opening column split +//! (`verifier::trace_opening_widths_well_formed`). +//! +//! A query opening carries the trace row as three prover-supplied vectors — +//! `precomputed ‖ main` (base field) and `aux` (extension field) — which the +//! DEEP reconstruction consumes as one concatenated row. Only their *sum* used +//! to be pinned (against the AIR-pinned OOD width), and the Merkle leaf hash +//! pins neither split: `hash_data_from_slices` streams `evaluations ‖ +//! evaluations_sym` with no length prefix and no separator. +//! +//! That mattered because the three trees are transcript-bound at different +//! times. This file covers the **precomputed↔main** term; the main↔aux term — +//! the LogUp break, and the instance with an executed false statement — lives in +//! `tests::aux_opening_width_tests`. +//! +//! Two layers, both free of any prover modification: +//! +//! * `precomputed_opening_narrower_than_the_air_declares_is_rejected` — end to +//! end through `Verifier::verify`, accepted on stock `main`. The prover and +//! the verifier's AIR disagree about how many columns the precomputed +//! commitment pins, while both absorb the same constant, so the transcripts +//! agree and the honest in-repo prover builds the proof. +//! * `opening_widths_*` — the guard called directly on surgically re-split +//! openings. These reach what no end-to-end test can: the `evaluations_sym` +//! slot (a separate prover-supplied vector the leaf hash does not pin apart +//! from `evaluations`) and the "a non-preprocessed AIR must declare zero +//! precomputed columns" direction, whose end-to-end form is masked by +//! transcript divergence and so proves nothing on its own. + +use std::marker::PhantomData; + +use crate::config::Commitment; +use crate::constraints::{ + boundary::{BoundaryConstraint, BoundaryConstraints}, + builder::{ + ConstraintMeta, ConstraintSet, num_base_from_meta, run_transition_prover, + run_transition_verifier, + }, +}; +use crate::context::AirContext; +use crate::examples::fibonacci_2_columns::{Fibonacci2ColsConstraints, compute_trace}; +use crate::examples::fibonacci_rap::{FibonacciRAP, FibonacciRAPPublicInputs, fibonacci_rap_trace}; +use crate::examples::simple_fibonacci::FibonacciPublicInputs; +use crate::proof::options::ProofOptions; +use crate::proof::stark::StarkProof; +use crate::proof::view::StarkProofView; +use crate::prover::{IsStarkProver, Prover}; +use crate::traits::{AIR, TransitionEvaluationContext}; +use crate::verifier::{IsStarkVerifier, Verifier}; +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use math::field::element::FieldElement; +use math::field::goldilocks::GoldilocksField; +use math::field::traits::IsFFTField; + +type F = GoldilocksField; +type Felt = FieldElement; + +const TRACE_LEN: usize = 16; + +/// `Fibonacci2ColsAIR` with two declaration knobs: +/// +/// * `precomputed_columns` — how many leading columns the AIR claims live in the +/// precomputed tree (0 = not preprocessed). Prover and verifier are handed +/// instances that disagree about this, which is the whole point. +/// * `out`, when set, adds a public-output boundary on the last row of column 1. +/// Since `(a0, a1)` determine the whole trace, a wrong `out` would make the +/// claimed statement FALSE. +pub struct FibonacciSplitAIR { + context: AirContext, + meta: Vec, + out: Option>, + precomputed_columns: usize, + precomputed_commitment: Commitment, + phantom: PhantomData, +} + +impl FibonacciSplitAIR { + /// The AIR as the verifier sees it: plain, non-preprocessed. + fn honest(proof_options: &ProofOptions, out: Option>) -> Self { + let mut air = ::new(proof_options); + air.out = out; + air + } + + /// The AIR the hostile prover proves against: same width, same constraints, + /// same boundary constraints — only the precomputed declaration differs. + fn split( + proof_options: &ProofOptions, + out: Option>, + commitment: Commitment, + ) -> Self { + Self::preprocessed_declaring(proof_options, out, 1, commitment) + } + + /// A preprocessed declaration with an explicit precomputed-column count. + /// Handing the verifier a different count than the prover used is how the + /// hook-free test below reaches the precomputed term of the guard: both + /// sides still absorb the same commitment, so the transcripts agree. + fn preprocessed_declaring( + proof_options: &ProofOptions, + out: Option>, + precomputed_columns: usize, + commitment: Commitment, + ) -> Self { + let mut air = Self::honest(proof_options, out); + air.precomputed_columns = precomputed_columns; + air.precomputed_commitment = commitment; + air + } +} + +impl AIR for FibonacciSplitAIR +where + F: IsFFTField + Send + Sync + 'static, +{ + type Field = F; + type FieldExtension = F; + type PublicInputs = FibonacciPublicInputs; + + fn step_size(&self) -> usize { + 1 + } + + fn new(proof_options: &ProofOptions) -> Self { + let meta = Fibonacci2ColsConstraints::::default().meta(); + let context = AirContext { + proof_options: proof_options.clone(), + transition_offsets: vec![0, 1], + num_transition_constraints: meta.len(), + trace_columns: 2, + }; + Self { + context, + meta, + out: None, + precomputed_columns: 0, + precomputed_commitment: [0u8; 32], + phantom: PhantomData, + } + } + + fn boundary_constraints( + &self, + pub_inputs: &Self::PublicInputs, + _rap_challenges: &[FieldElement], + _bus_public_inputs: Option<&crate::lookup::BusPublicInputs>, + _trace_length: usize, + ) -> BoundaryConstraints { + let mut constraints = vec![ + BoundaryConstraint::new_main(0, 0, pub_inputs.a0.clone()), + BoundaryConstraint::new_main(1, 0, pub_inputs.a1.clone()), + ]; + if let Some(out) = &self.out { + constraints.push(BoundaryConstraint::new_main(1, TRACE_LEN - 1, out.clone())); + } + BoundaryConstraints::from_constraints(constraints) + } + + fn constraints_meta(&self) -> &[ConstraintMeta] { + &self.meta + } + + fn compute_transition_prover( + &self, + evaluation_context: &TransitionEvaluationContext, + base_evals: &mut [FieldElement], + ext_evals: &mut [FieldElement], + ) { + run_transition_prover( + &Fibonacci2ColsConstraints::default(), + evaluation_context, + base_evals, + ext_evals, + ); + } + + fn compute_transition( + &self, + evaluation_context: &TransitionEvaluationContext, + ) -> Vec> { + run_transition_verifier( + &Fibonacci2ColsConstraints::default(), + evaluation_context, + self.num_base_transition_constraints(), + self.num_transition_constraints(), + ) + } + + fn num_base_transition_constraints(&self) -> usize { + num_base_from_meta(&Fibonacci2ColsConstraints::::default().meta()) + } + + fn context(&self) -> &AirContext { + &self.context + } + + fn composition_poly_degree_bound(&self, trace_length: usize) -> usize { + trace_length + } + + fn trace_layout(&self) -> (usize, usize) { + (2, 0) + } + + fn is_preprocessed(&self) -> bool { + self.precomputed_columns > 0 + } + + fn num_precomputed_columns(&self) -> usize { + self.precomputed_columns + } + + fn precomputed_commitment(&self) -> Commitment { + self.precomputed_commitment + } +} + +fn pub_inputs() -> FibonacciPublicInputs { + FibonacciPublicInputs { + a0: Felt::one(), + a1: Felt::one(), + } +} + +/// Tripwire. Every break test in this file and in +/// `tests::aux_opening_width_tests` asserts a *rejection*, and a rejection is +/// only evidence if it comes from the width pin — a verifier that rejected +/// everything, or that rejected these proofs for some incidental reason, would +/// satisfy them just as well. A sibling PoC was once misread exactly that way, +/// off a worktree whose verifier was not the one being claimed about. +/// +/// So: the guard must be *defined and called*, not merely present. Deleting the +/// call site while keeping the function — the plausible bad refactor — fails +/// here rather than silently turning the whole file green for the wrong reason. +/// The break tests additionally assert attribution behaviourally, by calling the +/// guard on the very proof they reject. +/// +/// (The prosecution PoC pinned a hash of the whole verifier source. That is +/// right for a throwaway branch and wrong in-repo, where it would break on every +/// unrelated verifier edit.) +#[test_log::test] +fn precheck_the_width_pin_is_compiled_in() { + let src = include_str!("../verifier.rs"); + assert!( + src.contains("fn trace_opening_widths_well_formed("), + "the opening-width guard is gone from the verifier compiled into this binary", + ); + assert!( + src.contains("Self::trace_opening_widths_well_formed("), + "the opening-width guard is defined but never called: every rejection \ + asserted in this file would then be proving something else", + ); +} + +/// The precomputed term, end to end and **hook-free**: the prover commits ONE +/// column in the precomputed tree; the verifier's AIR declares TWO. Both sides +/// absorb the same commitment (the AIR's constant is the tree the prover built), +/// so the transcripts agree and the honest in-repo prover produces the proof — +/// no attacker-side prover switch involved. +/// +/// Stock `main` accepts it: the widths sum to the OOD width and the DEEP +/// reconstruction reads the same concatenated row either way. What the verifier +/// is wrong about is *which* columns the hardcoded commitment pins — it believes +/// two, and only one is in that tree, so the other is prover-supplied while the +/// verifier treats it as fixed. +/// +/// For a *real* preprocessed table (bitwise, decode, keccak_rc) the round-1 root +/// equality would also catch this, since an honest constant is a root over +/// exactly `num_precomputed_columns()` columns and a narrower tree hashes +/// differently. That defence is incidental: nothing states the invariant and +/// nothing checks it, and it does not exist at all for a non-preprocessed AIR, +/// where the root is never absorbed and the same re-split lets a prover choose +/// trace columns after the round-2 challenge. This test pins the width itself, +/// which is the property the reconstruction actually depends on. +#[test_log::test] +fn precomputed_opening_narrower_than_the_air_declares_is_rejected() { + let proof_options = ProofOptions::default_test_options(); + let mut trace = compute_trace([Felt::one(), Felt::one()], TRACE_LEN); + let reference = FibonacciSplitAIR::::honest(&proof_options, None); + let commitment = Prover::compute_precomputed_commitment_for_testing(&trace, &reference, 1) + .expect("precomputed commitment"); + + // Prover: one precomputed column, one main column. + let prover_air = + FibonacciSplitAIR::::preprocessed_declaring(&proof_options, None, 1, commitment); + let proof = Prover::prove( + &prover_air, + &mut trace, + &pub_inputs(), + &mut DefaultTranscript::::new(&[]), + ) + .expect("prove"); + assert_eq!( + proof.deep_poly_openings[0] + .precomputed_trace_polys + .as_ref() + .expect("preprocessed proof opens a precomputed tree") + .evaluations + .len(), + 1, + "test precondition: the proof serves one precomputed column", + ); + + // Verifier: same commitment constant, but the AIR declares two precomputed + // columns — so the second is served from the main tree, not the pinned one. + let verifier_air = + FibonacciSplitAIR::::preprocessed_declaring(&proof_options, None, 2, commitment); + assert!( + !Verifier::verify(&proof, &verifier_air, &mut DefaultTranscript::::new(&[])), + "Verifier must reject a precomputed opening narrower than the AIR declares", + ); + // Attribution: the rejection is the width pin's, not an incidental failure + // elsewhere in verification. + assert!( + !Verifier::trace_opening_widths_well_formed( + &verifier_air, + StarkProofView::Owned(&proof), + verifier_air.options().fri_number_of_queries, + ), + "the rejection above must come from the opening-width guard", + ); +} + +/// Non-vacuity, and the completeness case that matters: a table that genuinely +/// IS preprocessed has `num_precomputed_columns() > 0`, and its proof — with the +/// honest prover, verified against the same preprocessed AIR — must still be +/// accepted. A guard that rejected every split would pass every test above. +#[test_log::test] +fn honest_preprocessed_proof_still_verifies() { + let proof_options = ProofOptions::default_test_options(); + let mut trace = compute_trace([Felt::one(), Felt::one()], TRACE_LEN); + let reference = FibonacciSplitAIR::::honest(&proof_options, None); + let commitment = Prover::compute_precomputed_commitment_for_testing(&trace, &reference, 1) + .expect("precomputed commitment"); + let split_air = FibonacciSplitAIR::::split(&proof_options, None, commitment); + + let proof = Prover::prove( + &split_air, + &mut trace, + &pub_inputs(), + &mut DefaultTranscript::::new(&[]), + ) + .expect("prove"); + + assert!( + Verifier::verify(&proof, &split_air, &mut DefaultTranscript::::new(&[])), + "a genuinely preprocessed table must still verify", + ); +} + +/// Non-vacuity for the plain path: the same AIR without any split declaration. +#[test_log::test] +fn honest_non_preprocessed_proof_still_verifies() { + let proof_options = ProofOptions::default_test_options(); + let mut trace = compute_trace([Felt::one(), Felt::one()], TRACE_LEN); + let out = trace.columns_main()[1][TRACE_LEN - 1]; + let air = FibonacciSplitAIR::::honest(&proof_options, Some(out)); + + let proof = Prover::prove( + &air, + &mut trace, + &pub_inputs(), + &mut DefaultTranscript::::new(&[]), + ) + .expect("prove"); + + assert!( + Verifier::verify(&proof, &air, &mut DefaultTranscript::::new(&[])), + "an honest proof of a true statement must verify", + ); +} + +// --------------------------------------------------------------------------- +// Direct tests of the guard, on a RAP proof (2 main + 1 aux columns). +// +// These reach the cases no end-to-end test can: the `evaluations_sym` slot is a +// separate prover-supplied vector that the leaf hash does not pin apart from +// `evaluations` (`hash_data_from_slices` concatenates them), and the aux width +// has its own transcript-timing problem (the aux root is absorbed only after +// the shared LogUp challenges). +// --------------------------------------------------------------------------- + +type RapProof = StarkProof>; + +fn make_valid_rap_proof() -> (FibonacciRAP, RapProof) { + let mut trace = fibonacci_rap_trace([Felt::one(), Felt::one()], TRACE_LEN); + let proof_options = ProofOptions::default_test_options(); + let pub_inputs = FibonacciRAPPublicInputs { + steps: TRACE_LEN, + a0: Felt::one(), + a1: Felt::one(), + }; + let air = FibonacciRAP::::new(&proof_options); + let proof = Prover::prove( + &air, + &mut trace, + &pub_inputs, + &mut DefaultTranscript::::new(&[]), + ) + .expect("prove"); + (air, proof) +} + +fn widths_well_formed(air: &FibonacciRAP, proof: &RapProof) -> bool { + Verifier::trace_opening_widths_well_formed( + air, + StarkProofView::Owned(proof), + air.options().fri_number_of_queries, + ) +} + +/// Baseline: the honest proof's split is the AIR's split. +#[test_log::test] +fn opening_widths_accept_an_honest_rap_proof() { + let (air, proof) = make_valid_rap_proof(); + assert_eq!(air.trace_layout(), (2, 1)); + assert!(!air.is_preprocessed()); + assert!( + widths_well_formed(&air, &proof), + "the guard must accept an honest proof", + ); +} + +/// Each of the three widths, in each of the two slots, must be pinned. Every +/// mutation below keeps the *total* column count reachable by the old sum check +/// out of scope — the point is that the individual terms are now checked. +#[test_log::test] +fn opening_widths_reject_every_mismatched_term() { + let (air, proof) = make_valid_rap_proof(); + let extra = Felt::one(); + + let mut tampered = proof.clone(); + tampered.deep_poly_openings[0] + .main_trace_polys + .evaluations + .push(extra); + assert!( + !widths_well_formed(&air, &tampered), + "an over-wide main opening must be rejected", + ); + + let mut tampered = proof.clone(); + tampered.deep_poly_openings[0] + .main_trace_polys + .evaluations + .pop(); + assert!( + !widths_well_formed(&air, &tampered), + "an under-wide main opening must be rejected", + ); + + let mut tampered = proof.clone(); + tampered.deep_poly_openings[0] + .main_trace_polys + .evaluations_sym + .push(extra); + assert!( + !widths_well_formed(&air, &tampered), + "an over-wide symmetric main opening must be rejected", + ); + + let mut tampered = proof.clone(); + tampered.deep_poly_openings[0] + .aux_trace_polys + .as_mut() + .expect("the RAP AIR has an aux trace") + .evaluations + .push(extra); + assert!( + !widths_well_formed(&air, &tampered), + "an over-wide aux opening must be rejected", + ); + + let mut tampered = proof.clone(); + tampered.deep_poly_openings[0] + .aux_trace_polys + .as_mut() + .expect("the RAP AIR has an aux trace") + .evaluations_sym + .push(extra); + assert!( + !widths_well_formed(&air, &tampered), + "an over-wide symmetric aux opening must be rejected", + ); + + let mut tampered = proof.clone(); + tampered.deep_poly_openings[0].aux_trace_polys = None; + assert!( + !widths_well_formed(&air, &tampered), + "a missing aux opening must be rejected when the AIR declares aux columns", + ); + + let mut tampered = proof.clone(); + let mut precomputed = tampered.deep_poly_openings[0].main_trace_polys.clone(); + precomputed.evaluations.truncate(1); + precomputed.evaluations_sym.truncate(1); + tampered.deep_poly_openings[0].precomputed_trace_polys = Some(precomputed); + assert!( + !widths_well_formed(&air, &tampered), + "precomputed openings must be rejected for a non-preprocessed AIR", + ); +} + +/// The guard covers every query the FRI phase will read, not just the first. +#[test_log::test] +fn opening_widths_are_checked_for_every_query() { + let (air, proof) = make_valid_rap_proof(); + let last = air.options().fri_number_of_queries - 1; + assert!(last > 0, "test precondition: more than one query"); + + let mut tampered = proof.clone(); + tampered.deep_poly_openings[last] + .main_trace_polys + .evaluations + .push(Felt::one()); + assert!( + !widths_well_formed(&air, &tampered), + "a mismatched split in the last query's opening must be rejected", + ); +} + +/// Fewer openings than queries is rejected rather than indexed past the end. +#[test_log::test] +fn opening_widths_reject_a_truncated_opening_list() { + let (air, proof) = make_valid_rap_proof(); + let mut tampered = proof.clone(); + tampered.deep_poly_openings.pop(); + assert!( + !widths_well_formed(&air, &tampered), + "an opening list shorter than the query count must be rejected", + ); +} diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index 64ae24363..ca6f15152 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -196,6 +196,73 @@ pub trait IsStarkVerifier< && next.height() == expected_next_height } + /// Soundness (I3, opening side): every query opening's column counts are a + /// public function of the AIR, never of the (prover-controlled) proof. + /// + /// An opening splits the trace row into `precomputed ‖ main` (base) and `aux` + /// (extension), which the DEEP reconstruction consumes as one concatenated + /// row — so only their *sum* was pinned, against the AIR-pinned OOD width. + /// The leaf hash pins neither split either: `hash_data_from_slices` streams + /// `evaluations ‖ evaluations_sym` with no length prefix or separator. + /// + /// That is exploitable because the three trees are absorbed at different + /// times: the precomputed root not at all for a non-preprocessed AIR, and the + /// aux root only after the LogUp challenges. An unpinned split therefore lets + /// a prover pick columns *after* challenges they must precede. Both variants + /// accepted a false statement before this check; see `tests::opening_width_tests` + /// and `tests::aux_opening_width_tests`. + /// + /// Runs once per table, before any opening is read. Both slots are checked: + /// they are separate prover-supplied vectors. + fn trace_opening_widths_well_formed( + air: &dyn AIR, + proof: StarkProofView<'_, Field, FieldExtension, PI>, + num_queries: usize, + ) -> bool { + // A non-preprocessed AIR has no precomputed tree, so its openings must + // declare zero precomputed columns — `num_precomputed_columns()` is + // documented as meaningful only under `is_preprocessed()`. + let expected_precomputed = if air.is_preprocessed() { + air.num_precomputed_columns() + } else { + 0 + }; + // Preprocessed tables commit columns `0..n` in the precomputed tree and + // the remaining main columns (the multiplicities) in the main tree. + let expected_main = match air.trace_layout().0.checked_sub(expected_precomputed) { + Some(n) => n, + // An AIR declaring more precomputed columns than it has main columns + // is malformed; no proof can be well formed against it. + None => return false, + }; + let expected_aux = air.num_auxiliary_rap_columns(); + + if proof.deep_poly_openings_len() < num_queries { + return false; + } + (0..num_queries).all(|i| { + let opening = proof.deep_poly_opening(i); + // Absent optional openings count as zero columns, matching how the + // reconstruction reads them (`.unwrap_or(&[])`). + let (precomputed, precomputed_sym) = match opening.precomputed_trace_polys() { + Some(p) => (p.evaluations().len(), p.evaluations_sym().len()), + None => (0, 0), + }; + let (aux, aux_sym) = match opening.aux_trace_polys() { + Some(a) => (a.evaluations().len(), a.evaluations_sym().len()), + None => (0, 0), + }; + let main = opening.main_trace_polys(); + + precomputed == expected_precomputed + && precomputed_sym == expected_precomputed + && main.evaluations().len() == expected_main + && main.evaluations_sym().len() == expected_main + && aux == expected_aux + && aux_sym == expected_aux + }) + } + fn step_2_verify_claimed_composition_polynomial( air: &dyn AIR, proof: StarkProofView<'_, Field, FieldExtension, PI>, @@ -543,9 +610,16 @@ pub trait IsStarkVerifier< iota, ); - // Precomputed trace (preprocessed tables only). Mismatched presence is - // unreachable in practice (multi_verify rejects such proofs upstream), - // but a defensive check keeps this function self-contained. + // Precomputed trace (preprocessed tables only). Mismatched presence: + // `(Some(root), None)` and any `(None, Some(opening))` carrying at least + // one column are rejected upstream by `trace_opening_widths_well_formed` + // (which pins the precomputed opening width to the AIR — zero for a + // non-preprocessed AIR) and, for the missing-root case, by the round-1 + // preprocessed-commitment check. What is left for this arm is the + // degenerate `(None, Some(opening))` with a zero-width opening, which + // upstream cannot distinguish from an absent one. Keep it: this is the + // only site that rejects that shape, and the check keeps the function + // self-contained. ok &= match ( proof.lde_trace_precomputed_merkle_root(), deep_poly_openings.precomputed_trace_polys(), @@ -555,7 +629,13 @@ pub trait IsStarkVerifier< _ => false, }; - // Auxiliary trace. + // Auxiliary trace. This authenticates the opening against the aux root; + // it does NOT constrain how many columns that opening has. Nothing here + // did, and that was a live break: the aux root is absorbed only after the + // shared LogUp challenges, so a prover that moved main columns into the + // aux tree got to choose them after seeing `z`/`alpha` + // (`tests::aux_opening_width_tests`). The width is pinned upstream by + // `trace_opening_widths_well_formed`; do not re-derive it from the proof. ok &= match ( proof.lde_trace_aux_merkle_root(), deep_poly_openings.aux_trace_polys(), @@ -969,6 +1049,16 @@ pub trait IsStarkVerifier< // whose column count does not match the OOD table width, or whose // regular/symmetric base-column split disagree. Without these checks // the indexing below would panic in release builds. + // + // These are panic guards on the *sum* only, and are redundant for proofs + // that reached here through `verify_rounds_2_to_4`: + // `trace_opening_widths_well_formed` already pinned each of the three + // widths (precomputed, main, aux) to the AIR, for both the regular and + // the symmetric slot. That is the authoritative check — soundness must + // not be argued from the sum alone, since the precomputed↔main and + // main↔aux splits move columns between trees that are transcript-bound at + // different times. This function has no AIR, so it keeps the weaker + // guards to stay panic-free on its own. if num_base != num_base_sym { return None; } @@ -1535,6 +1625,21 @@ pub trait IsStarkVerifier< return false; } + // Pin every query opening's precomputed/main/aux column split to the AIR + // before anything reads an opening (step 3 is the first consumer). The + // sum of the three widths was already pinned downstream; the individual + // terms were not, and each tree is transcript-bound at a different time — + // see `trace_opening_widths_well_formed`. Checked over the openings the + // query phase will actually use, which is exactly what the adjacent + // `query_list_len` guard counts (`sample_query_indexes` draws + // `fri_number_of_queries` iotas). + if !Self::trace_opening_widths_well_formed(air, proof, air.options().fri_number_of_queries) + { + #[cfg(not(feature = "test_fiat_shamir"))] + error!("Trace opening column split does not match the AIR"); + 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