From 185cc9cc284490e66d874673e32b7c28de6289b0 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 16 Jul 2026 12:59:28 -0300 Subject: [PATCH] test(stark): cross-check OOD transition window against captured constraint IR --- crypto/stark/src/constraint_ir/ir.rs | 48 +++++++ .../src/tests/bus_tests/soundness_tests.rs | 127 ++++++++++++++++++ prover/src/tests/mod.rs | 2 + prover/src/tests/ood_window_ir_tests.rs | 117 ++++++++++++++++ 4 files changed, 294 insertions(+) create mode 100644 prover/src/tests/ood_window_ir_tests.rs diff --git a/crypto/stark/src/constraint_ir/ir.rs b/crypto/stark/src/constraint_ir/ir.rs index cc770fd06..22857be2c 100644 --- a/crypto/stark/src/constraint_ir/ir.rs +++ b/crypto/stark/src/constraint_ir/ir.rs @@ -111,4 +111,52 @@ impl ConstraintProgram { pub fn is_empty(&self) -> bool { self.nodes.is_empty() } + + /// The full-width `[main | aux]` trace-column indices that some transition + /// constraint in this program reads at the *next* row (frame offset ≥ 1), + /// sorted and deduplicated. A main-trace read maps to its column index; an + /// aux-trace read maps to `main_width + col` — the same concatenated + /// indexing the verifier's OOD frame uses (main columns first, then aux; + /// see [`crate::ood`] and the frame reconstruction in the verifier). + /// + /// This is the ground truth an AIR's + /// [`crate::traits::AIR::trace_ood_next_row_columns`] declaration must + /// cover: the verifier opens every trace column at `z` but prunes the `g·z` + /// (next-row) opening down to the *declared* set, reconstructing ZERO for + /// any column outside it. So every column this method returns that the + /// declaration omits is silently read as zero at the next row — a + /// soundness/completeness bug. Deriving the read set from the captured IR + /// lets a test cross-check the hand-maintained declaration instead of + /// trusting it. + /// + /// A leaf is counted as a next-row read when its frame `offset` (or its + /// intra-step `row`, always 0 in the single-row-step capture path) is + /// nonzero, so the derivation can never *under*-report a next-row read — the + /// dangerous direction for the `derived ⊆ declared` check that guards + /// soundness. + /// + /// For tests and tooling only: it walks the captured [`ConstraintProgram`], + /// which the verify/recursion path never materializes. + pub fn next_row_trace_reads(&self, main_width: usize) -> Vec { + let mut cols: Vec = self + .nodes + .iter() + .filter_map(|op| match *op { + Op::Var { + main, + offset, + row, + col, + } if offset >= 1 || row >= 1 => Some(if main { + col as usize + } else { + main_width + col as usize + }), + _ => None, + }) + .collect(); + cols.sort_unstable(); + cols.dedup(); + cols + } } diff --git a/crypto/stark/src/tests/bus_tests/soundness_tests.rs b/crypto/stark/src/tests/bus_tests/soundness_tests.rs index 7d8fab0ee..508606924 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/crypto/stark/src/tests/bus_tests/soundness_tests.rs @@ -13,6 +13,10 @@ use math::field::{ use crate::examples::multi_table_lookup::{ new_add_air_with_lookup, new_cpu_air_with_lookup, new_mul_air_with_lookup, }; +use crate::lookup::{ + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, Multiplicity, + NullBoundaryConstraintBuilder, Packing, +}; use crate::proof::options::ProofOptions; use crate::prover::{IsStarkProver, Prover}; use crate::table::Table; @@ -927,6 +931,129 @@ fn test_trace_ood_next_row_columns_is_accumulator_only() { } } +/// Cross-check an AIR's *declared* OOD transition window +/// ([`AIR::trace_ood_next_row_columns`]) against the next-row read set +/// *derived* from its captured constraint IR. +/// +/// The window declaration is load-bearing for soundness: the verifier opens +/// every trace column at `z`, but prunes the `g·z` (next-row) opening down to +/// exactly the declared columns and reconstructs ZERO for every other column at +/// the next row (see [`crate::ood`]). So a transition constraint that reads a +/// next-row column the declaration omits is fed zero there — a silent +/// soundness/completeness bug. The declaration is hand-synced to the LogUp +/// accumulator and ignores the wrapped constraint set, so nothing but a test +/// catches drift (the `debug_assert`s that would are compiled out under the +/// `--release` test profile this repo uses). +/// +/// Asserts, from the read set derived by +/// [`crate::constraint_ir::ConstraintProgram::next_row_trace_reads`]: +/// * `derived ⊆ declared` — the critical, soundness direction, checked for +/// every AIR: a derived column missing from the declaration is the bug above. +/// * exact equality when `exact` — every `AirWithBuses` should declare +/// *precisely* the accumulator column (or nothing, with no interactions); +/// over-declaration only bloats the proof, but for these AIRs the window is +/// exactly known, so drift in either direction is a defect. +fn assert_ood_window_matches_ir( + air: &dyn AIR, + exact: bool, + label: &str, +) { + let (main, aux) = air.trace_layout(); + + let mut declared = air.trace_ood_next_row_columns(); + declared.sort_unstable(); + declared.dedup(); + + // Derive the true next-row read set from the captured constraint program, + // which runs the wrapped constraint set AND the LogUp emission through one + // CaptureBuilder — so any next-row read a base constraint makes is included. + let derived = air.constraint_program().next_row_trace_reads(main); + + for &c in &derived { + assert!( + c < main + aux, + "[{label}] derived next-row column {c} out of concatenated width {main}+{aux}" + ); + assert!( + declared.contains(&c), + "[{label}] a transition constraint reads full-width column {c} at the next row, but \ + it is absent from trace_ood_next_row_columns() = {declared:?}; the verifier prunes \ + that g·z opening to ZERO — soundness bug" + ); + } + + if exact { + assert_eq!( + derived, declared, + "[{label}] declared next-row window {declared:?} is not exactly the IR-derived read \ + set {derived:?}: over-declaration bloats every g·z opening" + ); + } +} + +/// Generic counterpart to the hardcoded single-AIR expectation above: for every +/// `AirWithBuses` in the crate's examples, the declared OOD transition window +/// equals the next-row read set derived from its captured constraint IR. Covers +/// the structural shapes `split_interactions` can produce — 1 absorbed, 2 +/// absorbed, and a committed batched pair — so the hand-synced declaration is +/// validated against the real IR rather than a copy of itself. +#[test_log::test] +fn test_trace_ood_next_row_window_matches_captured_ir() { + let opts = ProofOptions::default_test_options(); + + // The multi-table lookup example AIRs the bus tests exercise: + // CPU sends on two buses (2 absorbed interactions, 0 committed pairs); + // ADD / MUL each receive on one bus (1 absorbed interaction). + assert_ood_window_matches_ir(&new_cpu_air_with_lookup(&opts), true, "CPU"); + assert_ood_window_matches_ir(&new_add_air_with_lookup(&opts), true, "ADD"); + assert_ood_window_matches_ir(&new_mul_air_with_lookup(&opts), true, "MUL"); + + // A committed-pair layout: 3 interactions split into 1 batched pair + 1 + // absorbed. The batched-term constraint reads only the current row, so the + // next-row window is still exactly the accumulator column — a case the three + // example AIRs (0 committed pairs) do not reach. + let committed = AirWithBuses::::new( + 6, + AuxiliaryTraceBuildData { + interactions: vec![ + BusInteraction::sender( + TEST_BUS, + Multiplicity::Column(0), + Packing::Direct.columns(&[1]), + ), + BusInteraction::sender( + TEST_BUS, + Multiplicity::Column(2), + Packing::Direct.columns(&[3]), + ), + BusInteraction::sender( + TEST_BUS, + Multiplicity::Column(4), + Packing::Direct.columns(&[5]), + ), + ], + }, + &opts, + 1, + EmptyConstraints, + ); + assert_ood_window_matches_ir(&committed, true, "committed_pair"); + + // A bus-less AIR: no interactions => no LogUp accumulator => an empty + // next-row window, derived and declared alike. + let busless = AirWithBuses::::new( + 3, + AuxiliaryTraceBuildData { + interactions: vec![], + }, + &opts, + 1, + EmptyConstraints, + ); + assert!(busless.trace_ood_next_row_columns().is_empty()); + assert_ood_window_matches_ir(&busless, true, "busless"); +} + /// The g·z pruning actually shrinks the proof: a LogUp table opens every column /// at z (the current-row block) but only the accumulator at the next row. #[test_log::test] diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index faabff35d..2d66692a9 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -65,6 +65,8 @@ pub mod memw_tests; #[cfg(test)] pub mod mul_tests; #[cfg(test)] +pub mod ood_window_ir_tests; +#[cfg(test)] pub mod page_tests; #[cfg(test)] pub mod prove_elfs_tests; diff --git a/prover/src/tests/ood_window_ir_tests.rs b/prover/src/tests/ood_window_ir_tests.rs new file mode 100644 index 000000000..b4ff5766c --- /dev/null +++ b/prover/src/tests/ood_window_ir_tests.rs @@ -0,0 +1,117 @@ +//! Cross-check every production table's declared OOD transition window against +//! the next-row read set derived from its captured constraint IR. +//! +//! [`stark::traits::AIR::trace_ood_next_row_columns`] declares which full-width +//! `[main | aux]` columns a transition constraint reads at the *next* row. The +//! verifier opens every trace column at `z` but prunes the `g·z` (next-row) +//! opening down to exactly that declared set, reconstructing ZERO for every +//! other column at the next row (see `stark::ood`). A constraint that reads a +//! next-row column the declaration omits is therefore fed zero there — a silent +//! soundness/completeness bug. +//! +//! For every VM table the window is the hand-synced `AirWithBuses` override +//! (empty, or exactly the LogUp accumulator column); it deliberately ignores the +//! wrapped constraint set, which could legally read the next row. The only guard +//! against that declaration drifting from the constraints is a test — the +//! `debug_assert`s that would otherwise catch it are compiled out under the +//! `--release` test profile this repo uses. This is that test: it derives the +//! true read set from the captured [`stark::constraint_ir::ConstraintProgram`] +//! (which runs the wrapped constraint set AND the LogUp emission through one +//! CaptureBuilder) and validates the declaration against it, so the check tracks +//! the real constraints rather than a copy of the declaration. +//! +//! It only CONSTRUCTS AIRs (no program execution, no ELF), so it runs anywhere. +//! The table list mirrors the enumeration in `constraint_program_tests.rs` — the +//! canonical per-table `create_*_air` constructors from `test_utils`; there is no +//! ELF-free registry to iterate (`VmAirs::air_refs` needs a real ELF plus +//! preprocessed-commitment builds), so a new table must be added here. + +use stark::proof::options::GoldilocksCubicProofOptions; +use stark::traits::AIR; + +use crate::tables::types::{GoldilocksExtension, GoldilocksField}; +use crate::test_utils::*; + +type Gl = GoldilocksField; +type Ext3 = GoldilocksExtension; + +/// Assert an AIR's declared next-row window equals / covers the IR-derived read +/// set. +/// +/// * `derived ⊆ declared` for every AIR — the soundness direction: a derived +/// column missing from the declaration is pruned to zero at the next row. +/// * exact equality when `exact` — every `AirWithBuses` should declare +/// *precisely* the accumulator column (or nothing); over-declaration only +/// bloats the `g·z` opening, but for these AIRs the window is exactly known. +fn assert_ood_window_matches_ir( + air: &dyn AIR, + exact: bool, + label: &str, +) { + let (main, aux) = air.trace_layout(); + + let mut declared = air.trace_ood_next_row_columns(); + declared.sort_unstable(); + declared.dedup(); + + // The production capture (lazy OnceLock behind the AIR): the wrapped + // constraint set spliced ahead of the LogUp suffix, so a next-row read by + // ANY constraint — base or LogUp — is in the derived set. + let derived = air.constraint_program().next_row_trace_reads(main); + + for &c in &derived { + assert!( + c < main + aux, + "[{label}] derived next-row column {c} out of concatenated width {main}+{aux}" + ); + assert!( + declared.contains(&c), + "[{label}] a transition constraint reads full-width column {c} at the next row, but \ + it is absent from trace_ood_next_row_columns() = {declared:?}; the verifier prunes \ + that g·z opening to ZERO — soundness bug" + ); + } + + if exact { + assert_eq!( + derived, declared, + "[{label}] declared next-row window {declared:?} is not exactly the IR-derived read \ + set {derived:?}: over-declaration bloats every g·z opening" + ); + } +} + +/// Every production table AIR declares an OOD transition window equal to the +/// next-row read set derived from its captured constraint IR. All VM tables are +/// `AirWithBuses`, whose window is exactly the accumulator column (or empty), so +/// equality is asserted for each. +#[test] +fn all_table_windows_match_captured_ir() { + let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid"); + + assert_ood_window_matches_ir(&create_cpu_air(&opts), true, "CPU"); + assert_ood_window_matches_ir(&create_bitwise_air(&opts), true, "BITWISE"); + assert_ood_window_matches_ir(&create_lt_air(&opts), true, "LT"); + assert_ood_window_matches_ir(&create_shift_air(&opts), true, "SHIFT"); + assert_ood_window_matches_ir(&create_eq_air(&opts), true, "EQ"); + assert_ood_window_matches_ir(&create_bytewise_air(&opts), true, "BYTEWISE"); + assert_ood_window_matches_ir(&create_store_air(&opts), true, "STORE"); + assert_ood_window_matches_ir(&create_cpu32_air(&opts), true, "CPU32"); + assert_ood_window_matches_ir(&create_memw_air(&opts), true, "MEMW"); + assert_ood_window_matches_ir(&create_memw_aligned_air(&opts), true, "MEMW_A"); + assert_ood_window_matches_ir(&create_memw_register_air(&opts), true, "MEMW_R"); + assert_ood_window_matches_ir(&create_load_air(&opts), true, "LOAD"); + assert_ood_window_matches_ir(&create_decode_air(&opts), true, "DECODE"); + assert_ood_window_matches_ir(&create_mul_air(&opts), true, "MUL"); + assert_ood_window_matches_ir(&create_dvrm_air(&opts), true, "DVRM"); + assert_ood_window_matches_ir(&create_branch_air(&opts), true, "BRANCH"); + assert_ood_window_matches_ir(&create_halt_air(&opts), true, "HALT"); + assert_ood_window_matches_ir(&create_commit_air(&opts), true, "COMMIT"); + assert_ood_window_matches_ir(&create_page_air(&opts, 0x1000), true, "PAGE"); + assert_ood_window_matches_ir(&create_register_air(&opts), true, "REGISTER"); + assert_ood_window_matches_ir(&create_keccak_air(&opts), true, "KECCAK"); + assert_ood_window_matches_ir(&create_keccak_rnd_air(&opts), true, "KECCAK_RND"); + assert_ood_window_matches_ir(&create_keccak_rc_air(&opts), true, "KECCAK_RC"); + assert_ood_window_matches_ir(&create_ecsm_air(&opts), true, "ECSM"); + assert_ood_window_matches_ir(&create_ecdas_air(&opts), true, "ECDAS"); +}