test(stark): cross-check OOD transition window against captured constraint IR

crypto/stark/src/constraint_ir/ir.rs

@@ -111,4 +111,52 @@ impl<F: IsField, E: IsField> ConstraintProgram<F, E> {
     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<usize> {
+        let mut cols: Vec<usize> = 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
+    }
 }

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<Field = F, FieldExtension = E, PublicInputs = ()>,
+    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::<F, E, NullBoundaryConstraintBuilder, (), _>::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::<F, E, NullBoundaryConstraintBuilder, (), _>::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]

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;

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<Field = Gl, FieldExtension = Ext3, PublicInputs = ()>,
+    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");
+}