Skip to content
109 changes: 108 additions & 1 deletion crypto/stark/src/tests/small_trace_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,11 @@ use crate::{
},
proof::options::ProofOptions,
prover::{IsStarkProver, Prover},
tests::trace_test_helpers::make_valid_simple_proof,
tests::trace_test_helpers::{make_valid_logup_proof, make_valid_simple_proof},
traits::AIR,
verifier::{IsStarkVerifier, Verifier},
};
use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField;

type Felt = FieldElement<GoldilocksField>;

Expand Down Expand Up @@ -382,6 +383,112 @@ fn test_verify_rejects_opening_column_count_mismatch() {
);
}

/// A malformed proof whose symmetric opening splits its columns between the
/// base and auxiliary segments differently from the regular opening, while
/// keeping the same total column count.
///
/// `reconstruct_deep_composition_poly_evaluation_pair` bounds its base-column
/// branch by the REGULAR `num_base` but resolves the symmetric column through
/// `base_at_sym`, which indexes the SYMMETRIC slices. The
/// `num_base != num_base_sym` guard is the only thing standing between this
/// proof and an out-of-bounds index panic in release builds, and it runs in
/// step 3 — before step 4's Merkle openings could reject the tampering.
///
/// The total width is deliberately preserved (one column moved from the
/// symmetric main trace to the symmetric aux trace) so that the width guards
/// cannot fire: only the base/aux split guard can reject this.
#[test_log::test]
fn test_verify_rejects_asymmetric_base_aux_split() {
let (air, mut proof) = make_valid_logup_proof();

// Sanity: the unmodified proof must verify first.
assert!(
Verifier::verify(
&proof,
&air,
&mut DefaultTranscript::<Degree3GoldilocksExtensionField>::new(&[])
),
"precondition: valid LogUp proof must verify"
);

let opening = proof
.deep_poly_openings
.first_mut()
.expect("test precondition: a valid proof has at least one deep poly opening");
let aux = opening
.aux_trace_polys
.as_mut()
.expect("test precondition: the LogUp RAP has an auxiliary trace segment");

// Move one column from the symmetric main trace into the symmetric aux
// trace: `num_base_sym` drops by one while `num_base_sym + aux_sym.len()`
// still equals the OOD table width.
let moved = opening
.main_trace_polys
.evaluations_sym
.pop()
.expect("test precondition: the main trace opening has at least one column");
aux.evaluations_sym.push(moved.to_extension());

assert!(
!Verifier::verify(
&proof,
&air,
&mut DefaultTranscript::<Degree3GoldilocksExtensionField>::new(&[])
),
"Verifier must reject when the regular and symmetric base-column counts disagree"
);
}

/// A malformed proof whose symmetric composition-poly opening is shorter than
/// the proof-level `number_of_parts`.
///
/// The composition loop in `reconstruct_deep_composition_poly_evaluation_pair`
/// is bounded by `number_of_parts` (derived from
/// `composition_poly_parts_ood_evaluation`) and indexes both the regular and
/// symmetric per-query slices with it, so a short symmetric slice would index
/// out of bounds and panic in release builds. The length guard is the sole
/// protection and runs before step 4's Merkle openings.
///
/// Uses the LogUp RAP (`composition_poly_degree_bound == 2 * trace_length`) so
/// the multi-part loop is exercised rather than the degenerate one-part case.
#[test_log::test]
fn test_verify_rejects_truncated_symmetric_composition_opening() {
let (air, mut proof) = make_valid_logup_proof();

// Sanity: the unmodified proof must verify first.
assert!(
Verifier::verify(
&proof,
&air,
&mut DefaultTranscript::<Degree3GoldilocksExtensionField>::new(&[])
),
"precondition: valid LogUp proof must verify"
);
assert!(
proof.composition_poly_parts_ood_evaluation.len() > 1,
"test precondition: the LogUp RAP must have more than one composition part, \
so the multi-part loop is covered"
);

// Drop one symmetric part so the per-query opening is shorter than the
// proof-level part count the loop is bounded by.
proof.deep_poly_openings[0]
.composition_poly
.evaluations_sym
.pop()
.expect("test precondition: the composition opening has at least one part");

assert!(
!Verifier::verify(
&proof,
&air,
&mut DefaultTranscript::<Degree3GoldilocksExtensionField>::new(&[])
),
"Verifier must reject when a symmetric composition opening is shorter than number_of_parts"
);
}

// ---------------------------------------------------------------------------
// Helpers shared by the FRI early-termination soundness tests below.
// ---------------------------------------------------------------------------
Expand Down
50 changes: 50 additions & 0 deletions crypto/stark/src/tests/trace_test_helpers.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
use crate::examples::read_only_memory_logup::{
LogReadOnlyPublicInputs, LogReadOnlyRAP, read_only_logup_trace,
};
use crate::examples::simple_addition::{
SimpleAdditionAIR, SimpleAdditionPublicInputs, simple_addition_trace,
};
Expand All @@ -10,6 +13,7 @@ use crypto::fiat_shamir::default_transcript::DefaultTranscript;
use itertools::Itertools;
use math::field::{
element::FieldElement,
extensions_goldilocks::Degree3GoldilocksExtensionField,
goldilocks::GoldilocksField,
traits::{IsField, IsSubFieldOf},
};
Expand Down Expand Up @@ -46,6 +50,52 @@ pub fn make_valid_simple_proof() -> (
(air, proof)
}

/// Builds a valid 8-row `LogReadOnlyRAP` proof. Unlike
/// [`make_valid_simple_proof`], this AIR has both auxiliary trace columns
/// (`trace_layout() == (5, 1)`) and more than one composition part
/// (`composition_poly_degree_bound() == 2 * trace_length`), which the deep
/// composition rejection tests in `small_trace_tests` need in order to reach
/// the base/aux split and the multi-part composition loop.
pub type LogupProof = crate::proof::stark::StarkProof<
GoldilocksField,
Degree3GoldilocksExtensionField,
LogReadOnlyPublicInputs<GoldilocksField>,
>;

pub fn make_valid_logup_proof() -> (
LogReadOnlyRAP<GoldilocksField, Degree3GoldilocksExtensionField>,
LogupProof,
) {
let address_col: Vec<FieldElement<GoldilocksField>> = [3u64, 2, 2, 3, 4, 5, 1, 3]
.iter()
.map(|a| (*a).into())
.collect();
let value_col: Vec<FieldElement<GoldilocksField>> = [30u64, 20, 20, 30, 40, 50, 10, 30]
.iter()
.map(|v| (*v).into())
.collect();

let pub_inputs = LogReadOnlyPublicInputs {
a0: FieldElement::from(3u64),
v0: FieldElement::from(30u64),
a_sorted_0: FieldElement::from(1u64),
v_sorted_0: FieldElement::from(10u64),
m0: FieldElement::from(1u64),
};
let mut trace = read_only_logup_trace(address_col, value_col);
let proof_options = ProofOptions::default_test_options();
let air =
LogReadOnlyRAP::<GoldilocksField, Degree3GoldilocksExtensionField>::new(&proof_options);
let proof = Prover::prove(
&air,
&mut trace,
&pub_inputs,
&mut DefaultTranscript::<Degree3GoldilocksExtensionField>::new(&[]),
)
.expect("prover must succeed on the LogUp read-only-memory RAP");
(air, proof)
}

/// Reference Horner-based trace-evaluation used as an oracle by the prover
/// tests (`tests::prover_tests`). The production prover uses the LDE-based
/// barycentric `get_trace_evaluations_from_lde`; the two are
Expand Down
Loading
Loading