From 0779baeec3d5c04fc8651554f81679fc6f3953ca Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 5 Aug 2026 19:17:40 -0300 Subject: [PATCH 1/8] fix(verifier): pin each trace-opening column width to the AIR, not just their sum The verifier pinned only the SUM of a query opening's precomputed/main/aux column counts (against the AIR-pinned OOD width). Nothing pinned the split, and the Merkle leaf hash pins neither: hash_data_from_slices streams evaluations || evaluations_sym with no length prefix and no separator. Each of the three trees is transcript-bound at a different time, so both splits are exploitable: * precomputed<->main: a non-preprocessed AIR never absorbs the precomputed root, so columns declared 'precomputed' are bound by nothing. A prover can sample the round-2 challenges and then solve for them. * main<->aux: the aux root is absorbed after the shared LogUp challenges, so a column moved from main to aux is chosen after challenges it must precede. trace_opening_widths_well_formed pins all three widths, for both the regular and the symmetric slot, once per table before any opening is read. Co-Authored-By: diegokingston --- crypto/stark/src/verifier.rs | 117 ++++++++++++++++++++++++++++++++++- 1 file changed, 114 insertions(+), 3 deletions(-) diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index 64ae24363..75a0c507c 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -196,6 +196,82 @@ 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. + /// + /// Each query opening carries the trace row split into three vectors — + /// `precomputed ‖ main` (base field) and `aux` (extension field). Downstream + /// (`reconstruct_deep_composition_poly_evaluation_pair`) they are consumed as + /// one concatenated row `precomputed ‖ main ‖ aux`, so **only their sum** was + /// previously pinned (against the AIR-pinned OOD width). Nothing pinned the + /// individual terms, and neither Merkle leaf hash pins them either: + /// `hash_data_from_slices` streams `evaluations ‖ evaluations_sym` with no + /// length prefix and no separator, so a leaf can be re-split freely. + /// + /// Both splits are exploitable because each of the three trees is bound to the + /// transcript at a *different* time: + /// + /// * **precomputed↔main** — for a non-preprocessed AIR the precomputed root is + /// never absorbed at all (only the `is_preprocessed()` branch of round 1 + /// absorbs it). A prover that moves real trace columns into the "precomputed" + /// vector leaves them bound by nothing, samples the round-2 challenges, and + /// then solves for those columns — accepting a false statement. + /// * **main↔aux** — the aux root is absorbed only in round 1 phase C, *after* + /// the shared LogUp challenges are sampled. A column moved from `main` to + /// `aux` is likewise chosen after seeing challenges it should precede. + /// + /// So all three widths are pinned here, once per table, before any opening is + /// read. `evaluations()` and `evaluations_sym()` are checked independently: + /// they are separate prover-supplied vectors and the leaf hash pins neither. + 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 +619,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(), @@ -969,6 +1052,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 +1628,24 @@ 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 From 7fb83da25546bdcb7085f7753efe10e5e4d0279d Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 5 Aug 2026 19:37:14 -0300 Subject: [PATCH 2/8] test(verifier): regression tests for the trace-opening column split Six end-to-end cases against a hostile prover that declares one column 'precomputed' for an AIR that is not preprocessed, plus direct tests of the guard on a RAP proof covering all three widths in both the regular and the symmetric slot. On stock main, three of these fail (the proof is accepted): the honest trace under a split declaration, the adaptively forged trace, and a demonstrably false statement. The other three pass on both and are the non-vacuity controls - in particular a genuinely preprocessed table, which has num_precomputed_columns() > 0, must still verify. The end-to-end cases need TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB: a hostile prover does not absorb a root the verifier never reads, and without that the same proof is rejected for transcript divergence instead of for its split, which would prove nothing. Co-Authored-By: diegokingston --- crypto/stark/src/prover.rs | 12 +- crypto/stark/src/tests/mod.rs | 1 + crypto/stark/src/tests/opening_width_tests.rs | 636 ++++++++++++++++++ 3 files changed, 648 insertions(+), 1 deletion(-) create mode 100644 crypto/stark/src/tests/opening_width_tests.rs diff --git a/crypto/stark/src/prover.rs b/crypto/stark/src/prover.rs index 4047458bc..1c8af94cc 100644 --- a/crypto/stark/src/prover.rs +++ b/crypto/stark/src/prover.rs @@ -3194,7 +3194,17 @@ pub trait IsStarkProver< #[cfg(not(feature = "cuda"))] let (commit, cached_main) = result?; if let Some(ref pre_root) = commit.precomputed_root { - transcript.append_bytes(pre_root); + // Attacker simulation, tests only: a hostile prover skips this + // absorb, which is what makes a re-split opening exploitable + // (see `tests::opening_width_tests`). Always true otherwise. + #[cfg(test)] + let absorb = !crate::tests::opening_width_tests::TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB + .load(std::sync::atomic::Ordering::SeqCst); + #[cfg(not(test))] + let absorb = true; + if absorb { + transcript.append_bytes(pre_root); + } } transcript.append_bytes(&commit.root); main_commits.push(commit); diff --git a/crypto/stark/src/tests/mod.rs b/crypto/stark/src/tests/mod.rs index 15b64d45a..30d2c2306 100644 --- a/crypto/stark/src/tests/mod.rs +++ b/crypto/stark/src/tests/mod.rs @@ -6,6 +6,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..63faaf5b4 --- /dev/null +++ b/crypto/stark/src/tests/opening_width_tests.rs @@ -0,0 +1,636 @@ +//! 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. In particular, for a **non-preprocessed** AIR the verifier never +//! absorbs the precomputed root at all, so any column a prover declares +//! "precomputed" is bound by nothing and can be chosen *after* the round-2 +//! challenges — enough to accept a demonstrably false statement, which +//! `false_statement_under_split_declaration_is_rejected` exercises end to end. +//! +//! The end-to-end tests here need a hostile prover, simulated by +//! [`TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB`]: without it the same proof is +//! rejected for transcript divergence instead of for its split, which would +//! prove nothing. The `opening_widths_*` unit tests at the bottom need no such +//! switch — they call the guard directly on surgically re-split openings, and +//! cover the `evaluations_sym` slot, which is an independent attack surface. + +use std::marker::PhantomData; +use std::sync::atomic::{AtomicBool, Ordering}; +use std::sync::{Mutex, MutexGuard}; + +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::trace::TraceTable; +use crate::traits::{AIR, TransitionEvaluationContext}; +use crate::verifier::{IsStarkVerifier, Verifier}; +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use crypto::fiat_shamir::is_transcript::IsTranscript; +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; + +/// Attacker simulation, read only by the prover's round-1 commit loop under +/// `#[cfg(test)]`: skip absorbing the precomputed Merkle root. Nothing in the +/// protocol forces a hostile prover to absorb a root the verifier never reads — +/// a real attacker simply runs their own prover — but the in-repo prover is +/// honest, so the tests need this switch to build the proof an attacker would. +pub static TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB: AtomicBool = AtomicBool::new(false); + +/// The switch is process-global while the test harness runs tests in parallel, +/// so every test that proves anything takes this lock for its whole body. +static PROVER_MODE: Mutex<()> = Mutex::new(()); + +/// A failing test would otherwise poison the mutex and cascade into the rest. +fn lock_prover_mode() -> MutexGuard<'static, ()> { + PROVER_MODE.lock().unwrap_or_else(|e| e.into_inner()) +} + +fn set_hostile_prover(hostile: bool) { + TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB.store(hostile, Ordering::SeqCst); +} + +/// `Fibonacci2ColsAIR` with two knobs, both attacker-side: +/// +/// * `split` declares trace column 0 as *precomputed*, so the prover commits it +/// in a separate Merkle tree. The verifier is handed the `split == false` +/// instance, whose `is_preprocessed()` branch never absorbs that root. +/// * `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` makes the claimed +/// statement FALSE — that is what turns "an invalid witness is accepted" into +/// "a false statement is accepted". +pub struct FibonacciSplitAIR { + context: AirContext, + meta: Vec, + out: Option>, + split: bool, + 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 { + let mut air = Self::honest(proof_options, out); + air.split = true; + 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, + split: false, + 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.split + } + + fn num_precomputed_columns(&self) -> usize { + usize::from(self.split) + } + + fn precomputed_commitment(&self) -> Commitment { + self.precomputed_commitment + } +} + +type FibProof = StarkProof>; + +fn pub_inputs() -> FibonacciPublicInputs { + FibonacciPublicInputs { + a0: Felt::one(), + a1: Felt::one(), + } +} + +/// The transcript state the verifier reaches right before sampling the round-2 +/// challenge, for a single non-preprocessed table with no aux trace: absorb the +/// main root, then sample. Column 0 lives in the precomputed tree, so it does +/// not enter here — which is exactly the hole. +fn challenge_from_main_root(main_root: &Commitment) -> Felt { + let mut transcript = DefaultTranscript::::new(&[]); + transcript.append_bytes(main_root); + transcript.sample_field_element() +} + +/// Build a trace that is NOT a valid 2-column Fibonacci trace but whose +/// beta-combined transition constraint `c0 + beta*c1` vanishes on every row. +/// +/// `c0_i = A_{i+1} - A_i - B_i`, `c1_i = B_{i+1} - B_i - A_{i+1}`, so demanding +/// `c0_i + beta*c1_i = 0` gives +/// `A_{i+1} = [A_i + B_i(1 + beta) - beta*B_{i+1}] / (1 - beta)`. +fn forge_trace(b_col: &[Felt], a0: Felt, beta: &Felt) -> TraceTable { + let denom = (Felt::one() - beta).inv().expect("beta != 1"); + let mut a_col = vec![Felt::zero(); b_col.len()]; + a_col[0] = a0; + for i in 0..b_col.len() - 1 { + a_col[i + 1] = + (&a_col[i] + &b_col[i] * (Felt::one() + beta) - beta * &b_col[i + 1]) * &denom; + } + TraceTable::from_columns_main(vec![a_col, b_col.to_vec()], 1) +} + +/// How many rows of the trace violate the real Fibonacci constraints. +fn violations(trace: &TraceTable) -> usize { + let cols = trace.columns_main(); + let (a, b) = (&cols[0], &cols[1]); + (0..a.len() - 1) + .map(|i| { + usize::from(&a[i + 1] - &a[i] - &b[i] != Felt::zero()) + + usize::from(&b[i + 1] - &b[i] - &a[i + 1] != Felt::zero()) + }) + .sum() +} + +/// Attacker-chosen column 1. `b[0]` is pinned by the `a1` boundary; `b[last]` by +/// the public-output boundary when there is one; everything between is free. +fn attacker_b_column(a1: Felt, out: Option) -> Vec { + let free = if out.is_some() { + TRACE_LEN - 2 + } else { + TRACE_LEN - 1 + }; + let mut b = vec![a1]; + let mut x = Felt::from(987654321u64); + for _ in 0..free { + x = &x * Felt::from(1442695040u64) + Felt::from(1013904223u64); + b.push(x.clone()); + } + b.extend(out); + b +} + +/// Prove `trace` against the split declaration, with the hostile prover +/// (precomputed root never absorbed). Returns the proof a real attacker could +/// produce for the non-preprocessed AIR. +fn prove_with_split_declaration( + proof_options: &ProofOptions, + trace: &TraceTable, + out: Option, +) -> FibProof { + set_hostile_prover(true); + let reference = FibonacciSplitAIR::::honest(proof_options, out.clone()); + let commitment = Prover::compute_precomputed_commitment_for_testing(trace, &reference, 1) + .expect("precomputed commitment"); + let split_air = FibonacciSplitAIR::::split(proof_options, out, commitment); + let mut trace = trace.clone(); + Prover::prove( + &split_air, + &mut trace, + &pub_inputs(), + &mut DefaultTranscript::::new(&[]), + ) + .expect("prove under split declaration") +} + +/// The adaptive forgery: learn the round-2 challenge from a probe run (round 1 +/// binds only column 1), then solve for column 0. +fn forge_under_split_declaration(proof_options: &ProofOptions, out: Option) -> FibProof { + let b_col = attacker_b_column(pub_inputs().a1, out.clone()); + let probe_trace = + TraceTable::from_columns_main(vec![vec![Felt::zero(); TRACE_LEN], b_col.clone()], 1); + let probe = prove_with_split_declaration(proof_options, &probe_trace, out.clone()); + let beta = challenge_from_main_root(&probe.lde_trace_main_merkle_root); + + let forged = forge_trace(&b_col, pub_inputs().a0, &beta); + assert!( + violations(&forged) > 0, + "test precondition: the forged trace must violate the real constraints", + ); + let proof = prove_with_split_declaration(proof_options, &forged, out); + assert_eq!( + proof.lde_trace_main_merkle_root, probe.lde_trace_main_merkle_root, + "test precondition: round 1 must not bind column 0, else the attack is not adaptive", + ); + proof +} + +/// The cheapest discriminating case, and not a forgery: an *honest* trace proven +/// under the split declaration. `origin/main` accepts it against the plain +/// non-preprocessed AIR, because nothing pins the precomputed/main split of the +/// openings. Verification must not depend on a width the prover chose. +#[test_log::test] +fn honest_trace_under_split_declaration_is_rejected() { + let _prover_mode = lock_prover_mode(); + let proof_options = ProofOptions::default_test_options(); + let trace = compute_trace([Felt::one(), Felt::one()], TRACE_LEN); + let proof = prove_with_split_declaration(&proof_options, &trace, None); + + let honest_air = FibonacciSplitAIR::::honest(&proof_options, None); + assert!(!honest_air.is_preprocessed()); + assert_eq!( + proof.deep_poly_openings[0] + .precomputed_trace_polys + .as_ref() + .expect("split proof opens a precomputed tree") + .evaluations + .len(), + 1, + "test precondition: the proof declares one precomputed column", + ); + + assert!( + !Verifier::verify(&proof, &honest_air, &mut DefaultTranscript::::new(&[])), + "Verifier must reject an opening split the AIR does not declare", + ); +} + +/// The same split, now carrying an invalid witness chosen *after* the round-2 +/// challenge — the reason the split matters. +#[test_log::test] +fn forged_trace_under_split_declaration_is_rejected() { + let _prover_mode = lock_prover_mode(); + let proof_options = ProofOptions::default_test_options(); + let proof = forge_under_split_declaration(&proof_options, None); + let honest_air = FibonacciSplitAIR::::honest(&proof_options, None); + + assert!( + !Verifier::verify(&proof, &honest_air, &mut DefaultTranscript::::new(&[])), + "Verifier must reject a trace forged against the sampled challenge", + ); +} + +/// The strongest form: the claimed public output is unreachable from `(a0, a1)`, +/// so the statement has NO witness at all, and `origin/main` accepts it. +#[test_log::test] +fn false_statement_under_split_declaration_is_rejected() { + let _prover_mode = lock_prover_mode(); + let proof_options = ProofOptions::default_test_options(); + let honest_trace = compute_trace([Felt::one(), Felt::one()], TRACE_LEN); + let true_out = honest_trace.columns_main()[1][TRACE_LEN - 1].clone(); + let claimed_out = Felt::from(999u64); + assert_ne!( + true_out, claimed_out, + "test precondition: the claimed output must be unreachable, else the statement is true", + ); + + let honest_air = FibonacciSplitAIR::::honest(&proof_options, Some(claimed_out.clone())); + let proof = forge_under_split_declaration(&proof_options, Some(claimed_out)); + + assert!( + !Verifier::verify(&proof, &honest_air, &mut DefaultTranscript::::new(&[])), + "Verifier must reject a proof of a false statement", + ); +} + +/// The mirror shape: keep the re-split openings but drop the precomputed root, +/// so the presence guards see `None`. The reindexed columns still reach the DEEP +/// reconstruction, so the width check — not the root check — has to reject it. +#[test_log::test] +fn precomputed_openings_without_root_are_rejected() { + let _prover_mode = lock_prover_mode(); + let proof_options = ProofOptions::default_test_options(); + let mut proof = forge_under_split_declaration(&proof_options, None); + proof.lde_trace_precomputed_merkle_root = None; + assert!(proof.deep_poly_openings[0].precomputed_trace_polys.is_some()); + + let honest_air = FibonacciSplitAIR::::honest(&proof_options, None); + assert!( + !Verifier::verify(&proof, &honest_air, &mut DefaultTranscript::::new(&[])), + "Verifier must reject precomputed openings the AIR does not declare, root or no root", + ); +} + +/// 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 _prover_mode = lock_prover_mode(); + set_hostile_prover(false); + 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 _prover_mode = lock_prover_mode(); + set_hostile_prover(false); + 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].clone(); + 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 _prover_mode = lock_prover_mode(); + set_hostile_prover(false); + 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.clone()); + 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.clone()); + 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.clone()); + 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.clone()); + 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", + ); +} From 5243c9bdae806fdb23114d369a171bc451cc8f72 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 5 Aug 2026 19:40:21 -0300 Subject: [PATCH 3/8] style: cargo fmt + drop redundant clones flagged by clippy Co-Authored-By: diegokingston --- crypto/stark/src/prover.rs | 5 ++-- crypto/stark/src/tests/opening_width_tests.rs | 28 +++++++++++-------- crypto/stark/src/verifier.rs | 7 ++--- 3 files changed, 21 insertions(+), 19 deletions(-) diff --git a/crypto/stark/src/prover.rs b/crypto/stark/src/prover.rs index 1c8af94cc..5c0978424 100644 --- a/crypto/stark/src/prover.rs +++ b/crypto/stark/src/prover.rs @@ -3198,8 +3198,9 @@ pub trait IsStarkProver< // absorb, which is what makes a re-split opening exploitable // (see `tests::opening_width_tests`). Always true otherwise. #[cfg(test)] - let absorb = !crate::tests::opening_width_tests::TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB - .load(std::sync::atomic::Ordering::SeqCst); + let absorb = + !crate::tests::opening_width_tests::TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB + .load(std::sync::atomic::Ordering::SeqCst); #[cfg(not(test))] let absorb = true; if absorb { diff --git a/crypto/stark/src/tests/opening_width_tests.rs b/crypto/stark/src/tests/opening_width_tests.rs index 63faaf5b4..1e598d883 100644 --- a/crypto/stark/src/tests/opening_width_tests.rs +++ b/crypto/stark/src/tests/opening_width_tests.rs @@ -282,7 +282,7 @@ fn attacker_b_column(a1: Felt, out: Option) -> Vec { let mut x = Felt::from(987654321u64); for _ in 0..free { x = &x * Felt::from(1442695040u64) + Felt::from(1013904223u64); - b.push(x.clone()); + b.push(x); } b.extend(out); b @@ -297,7 +297,7 @@ fn prove_with_split_declaration( out: Option, ) -> FibProof { set_hostile_prover(true); - let reference = FibonacciSplitAIR::::honest(proof_options, out.clone()); + let reference = FibonacciSplitAIR::::honest(proof_options, out); let commitment = Prover::compute_precomputed_commitment_for_testing(trace, &reference, 1) .expect("precomputed commitment"); let split_air = FibonacciSplitAIR::::split(proof_options, out, commitment); @@ -314,10 +314,10 @@ fn prove_with_split_declaration( /// The adaptive forgery: learn the round-2 challenge from a probe run (round 1 /// binds only column 1), then solve for column 0. fn forge_under_split_declaration(proof_options: &ProofOptions, out: Option) -> FibProof { - let b_col = attacker_b_column(pub_inputs().a1, out.clone()); + let b_col = attacker_b_column(pub_inputs().a1, out); let probe_trace = TraceTable::from_columns_main(vec![vec![Felt::zero(); TRACE_LEN], b_col.clone()], 1); - let probe = prove_with_split_declaration(proof_options, &probe_trace, out.clone()); + let probe = prove_with_split_declaration(proof_options, &probe_trace, out); let beta = challenge_from_main_root(&probe.lde_trace_main_merkle_root); let forged = forge_trace(&b_col, pub_inputs().a0, &beta); @@ -385,14 +385,14 @@ fn false_statement_under_split_declaration_is_rejected() { let _prover_mode = lock_prover_mode(); let proof_options = ProofOptions::default_test_options(); let honest_trace = compute_trace([Felt::one(), Felt::one()], TRACE_LEN); - let true_out = honest_trace.columns_main()[1][TRACE_LEN - 1].clone(); + let true_out = honest_trace.columns_main()[1][TRACE_LEN - 1]; let claimed_out = Felt::from(999u64); assert_ne!( true_out, claimed_out, "test precondition: the claimed output must be unreachable, else the statement is true", ); - let honest_air = FibonacciSplitAIR::::honest(&proof_options, Some(claimed_out.clone())); + let honest_air = FibonacciSplitAIR::::honest(&proof_options, Some(claimed_out)); let proof = forge_under_split_declaration(&proof_options, Some(claimed_out)); assert!( @@ -410,7 +410,11 @@ fn precomputed_openings_without_root_are_rejected() { let proof_options = ProofOptions::default_test_options(); let mut proof = forge_under_split_declaration(&proof_options, None); proof.lde_trace_precomputed_merkle_root = None; - assert!(proof.deep_poly_openings[0].precomputed_trace_polys.is_some()); + assert!( + proof.deep_poly_openings[0] + .precomputed_trace_polys + .is_some() + ); let honest_air = FibonacciSplitAIR::::honest(&proof_options, None); assert!( @@ -455,7 +459,7 @@ fn honest_non_preprocessed_proof_still_verifies() { set_hostile_prover(false); 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].clone(); + let out = trace.columns_main()[1][TRACE_LEN - 1]; let air = FibonacciSplitAIR::::honest(&proof_options, Some(out)); let proof = Prover::prove( @@ -537,7 +541,7 @@ fn opening_widths_reject_every_mismatched_term() { tampered.deep_poly_openings[0] .main_trace_polys .evaluations - .push(extra.clone()); + .push(extra); assert!( !widths_well_formed(&air, &tampered), "an over-wide main opening must be rejected", @@ -557,7 +561,7 @@ fn opening_widths_reject_every_mismatched_term() { tampered.deep_poly_openings[0] .main_trace_polys .evaluations_sym - .push(extra.clone()); + .push(extra); assert!( !widths_well_formed(&air, &tampered), "an over-wide symmetric main opening must be rejected", @@ -569,7 +573,7 @@ fn opening_widths_reject_every_mismatched_term() { .as_mut() .expect("the RAP AIR has an aux trace") .evaluations - .push(extra.clone()); + .push(extra); assert!( !widths_well_formed(&air, &tampered), "an over-wide aux opening must be rejected", @@ -581,7 +585,7 @@ fn opening_widths_reject_every_mismatched_term() { .as_mut() .expect("the RAP AIR has an aux trace") .evaluations_sym - .push(extra.clone()); + .push(extra); assert!( !widths_well_formed(&air, &tampered), "an over-wide symmetric aux opening must be rejected", diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index 75a0c507c..152f96601 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -1636,11 +1636,8 @@ pub trait IsStarkVerifier< // 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, - ) { + 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; From c18411bdafd90471ac71976da448b5a67a6dceea Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 5 Aug 2026 19:58:53 -0300 Subject: [PATCH 4/8] test(verifier): regression tests for the main<->aux opening split (LogUp break) Ports the aux-instance PoC into a permanent regression: a hostile AIR declaring layout (4, 2) against LogReadOnlyRAP's honest (5, 1) moves the multiplicity column into the auxiliary tree, which is transcript-bound only AFTER the shared LogUp challenges. The prover then solves that column against the sampled z/alpha, and the multiset equality the AIR exists to enforce degenerates into one scalar equation. On stock main both break tests are accepted - the structural mis-split and a false memory read (address 3 carrying two values) - the latter also over the rkyv wire through multi_verify_archived, the recursion-guest path. Unlike the precomputed instance this needs no prover change at all: both sides absorb main-root-then-aux-root either way. Three controls (corrupted aux opening, the same lie without the split, the split without the challenge solve) plus an honest LogReadOnlyRAP round trip pass on both, so the harness discriminates and the pin is not vacuous. Co-Authored-By: diegokingston --- .../src/tests/aux_opening_width_tests.rs | 690 ++++++++++++++++++ crypto/stark/src/tests/mod.rs | 1 + 2 files changed, 691 insertions(+) create mode 100644 crypto/stark/src/tests/aux_opening_width_tests.rs 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..483b00754 --- /dev/null +++ b/crypto/stark/src/tests/aux_opening_width_tests.rs @@ -0,0 +1,690 @@ +//! 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::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", + ); +} + +// ============================================================================= +// 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", + ); + + // -------- 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 30d2c2306..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; From 4c19149abcf18977088c43c30279fee474e6eb9b Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 5 Aug 2026 20:00:18 -0300 Subject: [PATCH 5/8] docs(verifier): record the aux instance at verify_trace_openings and in the guard doc The aux arm authenticates against the aux root but constrains no width; say so, and point at the upstream pin. Same class of stale comment as the two this PR already corrects. Co-Authored-By: diegokingston --- crypto/stark/src/verifier.rs | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index 152f96601..b503e15d2 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -208,17 +208,23 @@ pub trait IsStarkVerifier< /// `hash_data_from_slices` streams `evaluations ‖ evaluations_sym` with no /// length prefix and no separator, so a leaf can be re-split freely. /// - /// Both splits are exploitable because each of the three trees is bound to the - /// transcript at a *different* time: + /// Both splits were exploitable — each demonstrated by a false statement the + /// unpinned verifier accepted — because each of the three trees is bound to + /// the transcript at a *different* time: /// /// * **precomputed↔main** — for a non-preprocessed AIR the precomputed root is /// never absorbed at all (only the `is_preprocessed()` branch of round 1 /// absorbs it). A prover that moves real trace columns into the "precomputed" /// vector leaves them bound by nothing, samples the round-2 challenges, and - /// then solves for those columns — accepting a false statement. + /// then solves for those columns (`tests::opening_width_tests`). /// * **main↔aux** — the aux root is absorbed only in round 1 phase C, *after* - /// the shared LogUp challenges are sampled. A column moved from `main` to - /// `aux` is likewise chosen after seeing challenges it should precede. + /// the shared LogUp challenges. A column moved from `main` to `aux` is + /// chosen after seeing `z`/`alpha`, which collapses LogUp's multiset + /// equality into one scalar equation the prover solves — no fingerprint + /// collision needed, and no prover modification either, since both sides + /// absorb main-root-then-aux-root regardless + /// (`tests::aux_opening_width_tests`). This one reaches the archived + /// (recursion-guest) path too. /// /// So all three widths are pinned here, once per table, before any opening is /// read. `evaluations()` and `evaluations_sym()` are checked independently: @@ -638,7 +644,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(), From 41e95cb8194a4b63ad0b1b2e874da6cde49ab7c7 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 5 Aug 2026 20:15:15 -0300 Subject: [PATCH 6/8] test(verifier): drop the prover hook - both instances now pin hook-free The precomputed regression no longer needs the #[cfg(test)] absorb switch in prover.rs. Handing the prover and the verifier AIRs that disagree about num_precomputed_columns, while both absorb the same commitment constant, keeps the transcripts in sync - so the honest in-repo prover builds a proof that stock main accepts and this branch rejects. prover.rs is back to stock: the whole change is now verifier + tests. What the dropped end-to-end tests covered is kept: the 'a non-preprocessed AIR must declare zero precomputed columns' direction is pinned by the direct guard tests (its end-to-end form is masked by transcript divergence and proves nothing on its own), and the aux file demonstrates an executed false statement. Adds a tripwire (precheck_the_width_pin_is_compiled_in) plus attribution asserts in the break tests, so a rejection cannot be read as evidence unless it comes from the guard - the failure mode that made a sibling PoC look non-reproducing. Co-Authored-By: diegokingston --- crypto/stark/src/prover.rs | 13 +- .../src/tests/aux_opening_width_tests.rs | 25 ++ crypto/stark/src/tests/opening_width_tests.rs | 333 ++++++------------ 3 files changed, 136 insertions(+), 235 deletions(-) diff --git a/crypto/stark/src/prover.rs b/crypto/stark/src/prover.rs index 5c0978424..4047458bc 100644 --- a/crypto/stark/src/prover.rs +++ b/crypto/stark/src/prover.rs @@ -3194,18 +3194,7 @@ pub trait IsStarkProver< #[cfg(not(feature = "cuda"))] let (commit, cached_main) = result?; if let Some(ref pre_root) = commit.precomputed_root { - // Attacker simulation, tests only: a hostile prover skips this - // absorb, which is what makes a re-split opening exploitable - // (see `tests::opening_width_tests`). Always true otherwise. - #[cfg(test)] - let absorb = - !crate::tests::opening_width_tests::TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB - .load(std::sync::atomic::Ordering::SeqCst); - #[cfg(not(test))] - let absorb = true; - if absorb { - transcript.append_bytes(pre_root); - } + transcript.append_bytes(pre_root); } transcript.append_bytes(&commit.root); main_commits.push(commit); diff --git a/crypto/stark/src/tests/aux_opening_width_tests.rs b/crypto/stark/src/tests/aux_opening_width_tests.rs index 483b00754..925f8111c 100644 --- a/crypto/stark/src/tests/aux_opening_width_tests.rs +++ b/crypto/stark/src/tests/aux_opening_width_tests.rs @@ -53,6 +53,7 @@ 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}; @@ -455,6 +456,18 @@ fn mis_split_aux_opening_is_rejected() { !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", + ); } // ============================================================================= @@ -546,6 +559,18 @@ fn false_memory_read_under_aux_split_is_rejected() { "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 diff --git a/crypto/stark/src/tests/opening_width_tests.rs b/crypto/stark/src/tests/opening_width_tests.rs index 1e598d883..be3898b6a 100644 --- a/crypto/stark/src/tests/opening_width_tests.rs +++ b/crypto/stark/src/tests/opening_width_tests.rs @@ -9,22 +9,25 @@ //! evaluations_sym` with no length prefix and no separator. //! //! That mattered because the three trees are transcript-bound at different -//! times. In particular, for a **non-preprocessed** AIR the verifier never -//! absorbs the precomputed root at all, so any column a prover declares -//! "precomputed" is bound by nothing and can be chosen *after* the round-2 -//! challenges — enough to accept a demonstrably false statement, which -//! `false_statement_under_split_declaration_is_rejected` exercises end to end. +//! 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`. //! -//! The end-to-end tests here need a hostile prover, simulated by -//! [`TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB`]: without it the same proof is -//! rejected for transcript divergence instead of for its split, which would -//! prove nothing. The `opening_widths_*` unit tests at the bottom need no such -//! switch — they call the guard directly on surgically re-split openings, and -//! cover the `evaluations_sym` slot, which is an independent attack surface. +//! 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 std::sync::atomic::{AtomicBool, Ordering}; -use std::sync::{Mutex, MutexGuard}; use crate::config::Commitment; use crate::constraints::{ @@ -42,11 +45,9 @@ use crate::proof::options::ProofOptions; use crate::proof::stark::StarkProof; 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 crypto::fiat_shamir::is_transcript::IsTranscript; use math::field::element::FieldElement; use math::field::goldilocks::GoldilocksField; use math::field::traits::IsFFTField; @@ -56,40 +57,19 @@ type Felt = FieldElement; const TRACE_LEN: usize = 16; -/// Attacker simulation, read only by the prover's round-1 commit loop under -/// `#[cfg(test)]`: skip absorbing the precomputed Merkle root. Nothing in the -/// protocol forces a hostile prover to absorb a root the verifier never reads — -/// a real attacker simply runs their own prover — but the in-repo prover is -/// honest, so the tests need this switch to build the proof an attacker would. -pub static TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB: AtomicBool = AtomicBool::new(false); - -/// The switch is process-global while the test harness runs tests in parallel, -/// so every test that proves anything takes this lock for its whole body. -static PROVER_MODE: Mutex<()> = Mutex::new(()); - -/// A failing test would otherwise poison the mutex and cascade into the rest. -fn lock_prover_mode() -> MutexGuard<'static, ()> { - PROVER_MODE.lock().unwrap_or_else(|e| e.into_inner()) -} - -fn set_hostile_prover(hostile: bool) { - TEST_ONLY_SKIP_PRECOMPUTED_ROOT_ABSORB.store(hostile, Ordering::SeqCst); -} - -/// `Fibonacci2ColsAIR` with two knobs, both attacker-side: +/// `Fibonacci2ColsAIR` with two declaration knobs: /// -/// * `split` declares trace column 0 as *precomputed*, so the prover commits it -/// in a separate Merkle tree. The verifier is handed the `split == false` -/// instance, whose `is_preprocessed()` branch never absorbs that root. +/// * `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` makes the claimed -/// statement FALSE — that is what turns "an invalid witness is accepted" into -/// "a false statement is accepted". +/// 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>, - split: bool, + precomputed_columns: usize, precomputed_commitment: Commitment, phantom: PhantomData, } @@ -108,9 +88,22 @@ impl FibonacciSplitAIR { 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.split = true; + air.precomputed_columns = precomputed_columns; air.precomputed_commitment = commitment; air } @@ -140,7 +133,7 @@ where context, meta, out: None, - split: false, + precomputed_columns: 0, precomputed_commitment: [0u8; 32], phantom: PhantomData, } @@ -210,11 +203,11 @@ where } fn is_preprocessed(&self) -> bool { - self.split + self.precomputed_columns > 0 } fn num_precomputed_columns(&self) -> usize { - usize::from(self.split) + self.precomputed_columns } fn precomputed_commitment(&self) -> Commitment { @@ -222,8 +215,6 @@ where } } -type FibProof = StarkProof>; - fn pub_inputs() -> FibonacciPublicInputs { FibonacciPublicInputs { a0: Felt::one(), @@ -231,195 +222,97 @@ fn pub_inputs() -> FibonacciPublicInputs { } } -/// The transcript state the verifier reaches right before sampling the round-2 -/// challenge, for a single non-preprocessed table with no aux trace: absorb the -/// main root, then sample. Column 0 lives in the precomputed tree, so it does -/// not enter here — which is exactly the hole. -fn challenge_from_main_root(main_root: &Commitment) -> Felt { - let mut transcript = DefaultTranscript::::new(&[]); - transcript.append_bytes(main_root); - transcript.sample_field_element() -} - -/// Build a trace that is NOT a valid 2-column Fibonacci trace but whose -/// beta-combined transition constraint `c0 + beta*c1` vanishes on every row. +/// 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. /// -/// `c0_i = A_{i+1} - A_i - B_i`, `c1_i = B_{i+1} - B_i - A_{i+1}`, so demanding -/// `c0_i + beta*c1_i = 0` gives -/// `A_{i+1} = [A_i + B_i(1 + beta) - beta*B_{i+1}] / (1 - beta)`. -fn forge_trace(b_col: &[Felt], a0: Felt, beta: &Felt) -> TraceTable { - let denom = (Felt::one() - beta).inv().expect("beta != 1"); - let mut a_col = vec![Felt::zero(); b_col.len()]; - a_col[0] = a0; - for i in 0..b_col.len() - 1 { - a_col[i + 1] = - (&a_col[i] + &b_col[i] * (Felt::one() + beta) - beta * &b_col[i + 1]) * &denom; - } - TraceTable::from_columns_main(vec![a_col, b_col.to_vec()], 1) -} - -/// How many rows of the trace violate the real Fibonacci constraints. -fn violations(trace: &TraceTable) -> usize { - let cols = trace.columns_main(); - let (a, b) = (&cols[0], &cols[1]); - (0..a.len() - 1) - .map(|i| { - usize::from(&a[i + 1] - &a[i] - &b[i] != Felt::zero()) - + usize::from(&b[i + 1] - &b[i] - &a[i + 1] != Felt::zero()) - }) - .sum() -} - -/// Attacker-chosen column 1. `b[0]` is pinned by the `a1` boundary; `b[last]` by -/// the public-output boundary when there is one; everything between is free. -fn attacker_b_column(a1: Felt, out: Option) -> Vec { - let free = if out.is_some() { - TRACE_LEN - 2 - } else { - TRACE_LEN - 1 - }; - let mut b = vec![a1]; - let mut x = Felt::from(987654321u64); - for _ in 0..free { - x = &x * Felt::from(1442695040u64) + Felt::from(1013904223u64); - b.push(x); - } - b.extend(out); - b -} - -/// Prove `trace` against the split declaration, with the hostile prover -/// (precomputed root never absorbed). Returns the proof a real attacker could -/// produce for the non-preprocessed AIR. -fn prove_with_split_declaration( - proof_options: &ProofOptions, - trace: &TraceTable, - out: Option, -) -> FibProof { - set_hostile_prover(true); - let reference = FibonacciSplitAIR::::honest(proof_options, out); - let commitment = Prover::compute_precomputed_commitment_for_testing(trace, &reference, 1) - .expect("precomputed commitment"); - let split_air = FibonacciSplitAIR::::split(proof_options, out, commitment); - let mut trace = trace.clone(); - Prover::prove( - &split_air, - &mut trace, - &pub_inputs(), - &mut DefaultTranscript::::new(&[]), - ) - .expect("prove under split declaration") -} - -/// The adaptive forgery: learn the round-2 challenge from a probe run (round 1 -/// binds only column 1), then solve for column 0. -fn forge_under_split_declaration(proof_options: &ProofOptions, out: Option) -> FibProof { - let b_col = attacker_b_column(pub_inputs().a1, out); - let probe_trace = - TraceTable::from_columns_main(vec![vec![Felt::zero(); TRACE_LEN], b_col.clone()], 1); - let probe = prove_with_split_declaration(proof_options, &probe_trace, out); - let beta = challenge_from_main_root(&probe.lde_trace_main_merkle_root); - - let forged = forge_trace(&b_col, pub_inputs().a0, &beta); +/// 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!( - violations(&forged) > 0, - "test precondition: the forged trace must violate the real constraints", + src.contains("fn trace_opening_widths_well_formed("), + "the opening-width guard is gone from the verifier compiled into this binary", ); - let proof = prove_with_split_declaration(proof_options, &forged, out); - assert_eq!( - proof.lde_trace_main_merkle_root, probe.lde_trace_main_merkle_root, - "test precondition: round 1 must not bind column 0, else the attack is not adaptive", + 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", ); - proof } -/// The cheapest discriminating case, and not a forgery: an *honest* trace proven -/// under the split declaration. `origin/main` accepts it against the plain -/// non-preprocessed AIR, because nothing pins the precomputed/main split of the -/// openings. Verification must not depend on a width the prover chose. +/// 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. For a real preprocessed table (bitwise, +/// decode, keccak_rc) that is the lookup table's own content becoming +/// prover-supplied. The round-1 root equality is a second line of defence here +/// only because an honest constant happens to be a root over exactly +/// `num_precomputed_columns()` columns — nothing states that, and nothing checks +/// it. This test pins the width directly. #[test_log::test] -fn honest_trace_under_split_declaration_is_rejected() { - let _prover_mode = lock_prover_mode(); +fn precomputed_opening_narrower_than_the_air_declares_is_rejected() { let proof_options = ProofOptions::default_test_options(); - let trace = compute_trace([Felt::one(), Felt::one()], TRACE_LEN); - let proof = prove_with_split_declaration(&proof_options, &trace, None); + 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 honest_air = FibonacciSplitAIR::::honest(&proof_options, None); - assert!(!honest_air.is_preprocessed()); + // 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("split proof opens a precomputed tree") + .expect("preprocessed proof opens a precomputed tree") .evaluations .len(), 1, - "test precondition: the proof declares one precomputed column", - ); - - assert!( - !Verifier::verify(&proof, &honest_air, &mut DefaultTranscript::::new(&[])), - "Verifier must reject an opening split the AIR does not declare", + "test precondition: the proof serves one precomputed column", ); -} - -/// The same split, now carrying an invalid witness chosen *after* the round-2 -/// challenge — the reason the split matters. -#[test_log::test] -fn forged_trace_under_split_declaration_is_rejected() { - let _prover_mode = lock_prover_mode(); - let proof_options = ProofOptions::default_test_options(); - let proof = forge_under_split_declaration(&proof_options, None); - let honest_air = FibonacciSplitAIR::::honest(&proof_options, None); + // 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, &honest_air, &mut DefaultTranscript::::new(&[])), - "Verifier must reject a trace forged against the sampled challenge", + !Verifier::verify(&proof, &verifier_air, &mut DefaultTranscript::::new(&[])), + "Verifier must reject a precomputed opening narrower than the AIR declares", ); -} - -/// The strongest form: the claimed public output is unreachable from `(a0, a1)`, -/// so the statement has NO witness at all, and `origin/main` accepts it. -#[test_log::test] -fn false_statement_under_split_declaration_is_rejected() { - let _prover_mode = lock_prover_mode(); - let proof_options = ProofOptions::default_test_options(); - let honest_trace = compute_trace([Felt::one(), Felt::one()], TRACE_LEN); - let true_out = honest_trace.columns_main()[1][TRACE_LEN - 1]; - let claimed_out = Felt::from(999u64); - assert_ne!( - true_out, claimed_out, - "test precondition: the claimed output must be unreachable, else the statement is true", - ); - - let honest_air = FibonacciSplitAIR::::honest(&proof_options, Some(claimed_out)); - let proof = forge_under_split_declaration(&proof_options, Some(claimed_out)); - - assert!( - !Verifier::verify(&proof, &honest_air, &mut DefaultTranscript::::new(&[])), - "Verifier must reject a proof of a false statement", - ); -} - -/// The mirror shape: keep the re-split openings but drop the precomputed root, -/// so the presence guards see `None`. The reindexed columns still reach the DEEP -/// reconstruction, so the width check — not the root check — has to reject it. -#[test_log::test] -fn precomputed_openings_without_root_are_rejected() { - let _prover_mode = lock_prover_mode(); - let proof_options = ProofOptions::default_test_options(); - let mut proof = forge_under_split_declaration(&proof_options, None); - proof.lde_trace_precomputed_merkle_root = None; - assert!( - proof.deep_poly_openings[0] - .precomputed_trace_polys - .is_some() - ); - - let honest_air = FibonacciSplitAIR::::honest(&proof_options, None); + // Attribution: the rejection is the width pin's, not an incidental failure + // elsewhere in verification. assert!( - !Verifier::verify(&proof, &honest_air, &mut DefaultTranscript::::new(&[])), - "Verifier must reject precomputed openings the AIR does not declare, root or no root", + !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", ); } @@ -429,8 +322,6 @@ fn precomputed_openings_without_root_are_rejected() { /// accepted. A guard that rejected every split would pass every test above. #[test_log::test] fn honest_preprocessed_proof_still_verifies() { - let _prover_mode = lock_prover_mode(); - set_hostile_prover(false); 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); @@ -455,8 +346,6 @@ fn honest_preprocessed_proof_still_verifies() { /// Non-vacuity for the plain path: the same AIR without any split declaration. #[test_log::test] fn honest_non_preprocessed_proof_still_verifies() { - let _prover_mode = lock_prover_mode(); - set_hostile_prover(false); 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]; @@ -489,8 +378,6 @@ fn honest_non_preprocessed_proof_still_verifies() { type RapProof = StarkProof>; fn make_valid_rap_proof() -> (FibonacciRAP, RapProof) { - let _prover_mode = lock_prover_mode(); - set_hostile_prover(false); let mut trace = fibonacci_rap_trace([Felt::one(), Felt::one()], TRACE_LEN); let proof_options = ProofOptions::default_test_options(); let pub_inputs = FibonacciRAPPublicInputs { From dcc7cfd27e5abefdbb9a8ae4cdc25d381aec2a92 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 11:12:31 -0300 Subject: [PATCH 7/8] docs(test): state precisely what the round-1 root check does and does not catch The precomputed-width test's comment implied real preprocessed tables are exploitable through this shape. They are not directly: an honest constant is a root over exactly num_precomputed_columns() columns, so a narrower tree hashes differently and round 1 rejects it. Say that, and say why the defence is incidental - nothing states the invariant, nothing checks it, and it is absent entirely for a non-preprocessed AIR. Co-Authored-By: diegokingston --- crypto/stark/src/tests/opening_width_tests.rs | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/crypto/stark/src/tests/opening_width_tests.rs b/crypto/stark/src/tests/opening_width_tests.rs index be3898b6a..db5764220 100644 --- a/crypto/stark/src/tests/opening_width_tests.rs +++ b/crypto/stark/src/tests/opening_width_tests.rs @@ -261,12 +261,17 @@ fn precheck_the_width_pin_is_compiled_in() { /// 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. For a real preprocessed table (bitwise, -/// decode, keccak_rc) that is the lookup table's own content becoming -/// prover-supplied. The round-1 root equality is a second line of defence here -/// only because an honest constant happens to be a root over exactly -/// `num_precomputed_columns()` columns — nothing states that, and nothing checks -/// it. This test pins the width directly. +/// 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(); From b7bc5eec53ec50a942ef084f19c7ab167b0a1ef0 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 12:58:53 -0300 Subject: [PATCH 8/8] docs(verifier): trim the opening-width doc to the invariant The header carried the two exploit narratives in full, at ~33 lines for a ~40 line function -- 3x the sibling ood_blocks_well_formed. The mechanics belong in the tests that demonstrate them and in the PR; the header only needs the invariant, why an unpinned split is exploitable at all, and where to look. Co-Authored-By: diegokingston --- crypto/stark/src/verifier.rs | 41 ++++++++++++------------------------ 1 file changed, 13 insertions(+), 28 deletions(-) diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index b503e15d2..ca6f15152 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -199,36 +199,21 @@ pub trait IsStarkVerifier< /// Soundness (I3, opening side): every query opening's column counts are a /// public function of the AIR, never of the (prover-controlled) proof. /// - /// Each query opening carries the trace row split into three vectors — - /// `precomputed ‖ main` (base field) and `aux` (extension field). Downstream - /// (`reconstruct_deep_composition_poly_evaluation_pair`) they are consumed as - /// one concatenated row `precomputed ‖ main ‖ aux`, so **only their sum** was - /// previously pinned (against the AIR-pinned OOD width). Nothing pinned the - /// individual terms, and neither Merkle leaf hash pins them either: - /// `hash_data_from_slices` streams `evaluations ‖ evaluations_sym` with no - /// length prefix and no separator, so a leaf can be re-split freely. + /// 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. /// - /// Both splits were exploitable — each demonstrated by a false statement the - /// unpinned verifier accepted — because each of the three trees is bound to - /// the transcript at a *different* time: + /// 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`. /// - /// * **precomputed↔main** — for a non-preprocessed AIR the precomputed root is - /// never absorbed at all (only the `is_preprocessed()` branch of round 1 - /// absorbs it). A prover that moves real trace columns into the "precomputed" - /// vector leaves them bound by nothing, samples the round-2 challenges, and - /// then solves for those columns (`tests::opening_width_tests`). - /// * **main↔aux** — the aux root is absorbed only in round 1 phase C, *after* - /// the shared LogUp challenges. A column moved from `main` to `aux` is - /// chosen after seeing `z`/`alpha`, which collapses LogUp's multiset - /// equality into one scalar equation the prover solves — no fingerprint - /// collision needed, and no prover modification either, since both sides - /// absorb main-root-then-aux-root regardless - /// (`tests::aux_opening_width_tests`). This one reaches the archived - /// (recursion-guest) path too. - /// - /// So all three widths are pinned here, once per table, before any opening is - /// read. `evaluations()` and `evaluations_sym()` are checked independently: - /// they are separate prover-supplied vectors and the leaf hash pins neither. + /// 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>,