diff --git a/prover/src/tables/dvrm.rs b/prover/src/tables/dvrm.rs index 3329bf273..b74416010 100644 --- a/prover/src/tables/dvrm.rs +++ b/prover/src/tables/dvrm.rs @@ -22,7 +22,7 @@ //! - `sign_n`, `sign_d`, `sign_q`, `sign_r`: Bit - sign bits //! //! ## Bus Interactions -//! - Sender: IS_HALF (×16: n, d, r, n_sub_r, q) +//! - Sender: IS_HALF (×20: n, d, r, n_sub_r, q) //! - Sender: MSB16 (×3 for sign extraction: n, d, r) //! - Sender: ALU (×3, on the unified bus: ×1 LT-flavored for `|r| < |d|`, //! ×2 MUL-flavored for `n - r = d * q` lo/hi) @@ -384,9 +384,34 @@ pub fn generate_dvrm_trace( pub fn bus_interactions() -> Vec { let mut interactions = Vec::new(); - // DVRM-A1.i (IS_HALF[n[i]]) and DVRM-A2.i (IS_HALF[d[i]]) are assumptions: - // the CPU (sender) is responsible for range-checking n and d before sending - // to DVRM. The DVRM table does NOT send these IS_HALF lookups. + // ------------------------------------------------------------------------- + // DVRM-A1.i: IS_HALF[n[i]] (×4) and DVRM-A2.i: IS_HALF[d[i]] (×4), + // multiplicity: μ_q + μ_r. + // The bus binds only the packed 32-bit words (DWordHL/DWordBL emit two + // words, not the four halves), so without these the input halves are free: + // a prover could supply non-canonical halves that re-pack to the same word + // yet sum to 0 in the field, forging div_by_zero (DVRM-C17 keys on the + // half-sum) for a nonzero denominator. Range-checking each half closes that. + // ------------------------------------------------------------------------- + for col in [ + cols::N_0, + cols::N_1, + cols::N_2, + cols::N_3, + cols::D_0, + cols::D_1, + cols::D_2, + cols::D_3, + ] { + interactions.push(BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Sum(cols::MU_Q, cols::MU_R), + vec![BusValue::Packed { + start_column: col, + packing: Packing::Direct, + }], + )); + } // ------------------------------------------------------------------------- // DVRM-C13.i: IS_HALF[r[i]] (×4), multiplicity: μ_q + μ_r diff --git a/prover/src/tables/mul.rs b/prover/src/tables/mul.rs index 6e5ca3a72..ac2329ebd 100644 --- a/prover/src/tables/mul.rs +++ b/prover/src/tables/mul.rs @@ -25,7 +25,7 @@ //! //! ## Bus Interactions //! - Sender: MSB16 (×2 for sign extraction) -//! - Sender: IS_HALF (×8 for lo/hi range checks) +//! - Sender: IS_HALF (×16 for lhs/rhs input and lo/hi output range checks) //! - Sender: IS_B20 (×4 for carry range checks) //! - Receiver: ALU (×2 for lo and hi results — every MUL lookup, CPU //! MUL/MULH dispatch and dvrm's internal `d*q` consistency) @@ -370,7 +370,7 @@ pub fn generate_mul_trace( /// /// The MUL table: /// - **Sends** MSB16 lookups for sign bit extraction (×2) -/// - **Sends** IS_HALF lookups for lo/hi range checks (×8) +/// - **Sends** IS_HALF lookups for lhs/rhs input and lo/hi output range checks (×16) /// - **Sends** IS_B20 lookups for carry range checks (×4) /// - **Receives** MUL lookups from CPU table (×2: lo and hi) pub fn bus_interactions() -> Vec { @@ -411,6 +411,31 @@ pub fn bus_interactions() -> Vec { ], )); + // ------------------------------------------------------------------------- + // IS_HALF lookups for lhs/rhs INPUT range checks (multiplicity: mu_lo + mu_hi). + // The bus binds only the packed 32-bit words, so without these the input + // half-limbs are free (non-canonical halves re-packing to the same word). + // ------------------------------------------------------------------------- + for col in [ + cols::LHS_0, + cols::LHS_1, + cols::LHS_2, + cols::LHS_3, + cols::RHS_0, + cols::RHS_1, + cols::RHS_2, + cols::RHS_3, + ] { + interactions.push(BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Sum(cols::MU_LO, cols::MU_HI), + vec![BusValue::Packed { + start_column: col, + packing: Packing::Direct, + }], + )); + } + // ------------------------------------------------------------------------- // IS_HALF lookups for lo range checks (multiplicity: mu_lo + mu_hi) // ------------------------------------------------------------------------- diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index 20f66ff90..0e5f86fe5 100644 --- a/prover/src/tables/shift.rs +++ b/prover/src/tables/shift.rs @@ -13,8 +13,8 @@ //! - Virtual: `limb_shift[3] = 1 - limb_shift_raw[0] - limb_shift_raw[1] - limb_shift_raw[2]` //! - Multiplicity: `μ` //! -//! ## Bus Interactions (11 total) -//! - Senders: MSB16, AND_BYTE (×3), ZERO, HWSL (×5) +//! ## Bus Interactions (15 total) +//! - Senders: MSB16, AND_BYTE (×3), ZERO, HWSL (×5), IS_HALFWORD (×4) //! - Receiver: SHIFT (from CPU) use math::field::element::FieldElement; @@ -419,7 +419,7 @@ pub fn generate_shift_trace( /// Creates all bus interactions for the SHIFT table. pub fn bus_interactions() -> Vec { - let mut interactions = Vec::with_capacity(11); + let mut interactions = Vec::with_capacity(15); // SHIFT-C14: MSB16[in[3]] → is_negative | signed interactions.push(BusInteraction::sender( @@ -701,6 +701,22 @@ pub fn bus_interactions() -> Vec { }], )); + // VM-3: range-check every input half `in[i]` as a 16-bit value, unconditionally + // on every active row. The SHIFT bus carries only the *packed* operand, so + // without these a non-canonical half-decomposition that wraps in the field + // (keeping the packed word constant) would be invisible to the caller while + // still changing the shifted output. + for input_col in cols::IN { + interactions.push(BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(cols::MU), + vec![BusValue::Packed { + start_column: input_col, + packing: Packing::Direct, + }], + )); + } + interactions } @@ -1055,6 +1071,16 @@ pub fn collect_bitwise_from_shift(operations: &[ShiftOperation]) -> Vec> 8) as u8, )); + + // VM-3: IS_HALF[in[i]] for the four input halves, unconditional on every + // active row — matches the four IS_HALF senders added in `bus_interactions`. + for i in 0..4 { + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (op.in_halves[i] & 0xFF) as u8, + (op.in_halves[i] >> 8) as u8, + )); + } } bitwise_ops diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 3da58cf44..d342b6e16 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1304,16 +1304,30 @@ fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec { /// Collects bitwise lookups from MUL operations (MSB16 for sign bits). /// /// MUL sends MSB16 lookups when signed=1 to extract sign bits, -/// IS_HALF lookups for lo/hi range checks, and IS_B20 lookups for carry range checks. +/// IS_HALF lookups for lhs/rhs input and lo/hi output range checks, +/// and IS_B20 lookups for carry range checks. /// /// Returns: Vec of bitwise lookups fn collect_bitwise_from_mul(mul_ops: &[(MulOperation, bool)]) -> Vec { - let mut bitwise_ops = Vec::with_capacity(mul_ops.len() * 14); + let mut bitwise_ops = Vec::with_capacity(mul_ops.len() * 20); // IS_HALF and IS_B20: one set per raw op (multiplicity Sum(MU_LO, MU_HI)) for (op, _wants_hi) in mul_ops { let (lo, hi) = op.compute_product(); + // IS_HALF for lhs/rhs INPUT halfwords (matches the lhs/rhs IS_HALF senders + // in mul::bus_interactions). + for word in [op.lhs, op.rhs] { + for shift in [0, 16, 32, 48] { + let half = ((word >> shift) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (half & 0xFF) as u8, + (half >> 8) as u8, + )); + } + } + // IS_HALF for lo halfwords for shift in [0, 16, 32, 48] { let half = ((lo >> shift) & 0xFFFF) as u16; @@ -1376,16 +1390,32 @@ fn collect_bitwise_from_mul(mul_ops: &[(MulOperation, bool)]) -> Vec Vec { - let mut bitwise_ops = Vec::with_capacity(dvrm_ops.len() * 16); + let mut bitwise_ops = Vec::with_capacity(dvrm_ops.len() * 24); for (op, _wants_remainder) in dvrm_ops { + // IS_HALF for n[0..4] and d[0..4] (DVRM-A1/A2): range-check the input + // half-limbs so a prover cannot supply non-canonical halves (matches the + // n/d IS_HALF senders in dvrm::bus_interactions). + for word in [op.n, op.d] { + for shift in [0, 16, 32, 48] { + let half = ((word >> shift) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (half & 0xFF) as u8, + (half >> 8) as u8, + )); + } + } + // IS_HALF for r[0..4] (DVRM-C13) let r = op.compute_remainder(); for shift in [0, 16, 32, 48] { diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index b4c93f27d..0b9a94e36 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -20,7 +20,11 @@ use executor::vm::logs::Log; use executor::vm::memory::U64HashMap; use math::field::element::FieldElement; use stark::constraints::transition::{TransitionConstraint, TransitionConstraintEvaluator}; -use stark::lookup::{AirWithBuses, AuxiliaryTraceBuildData, NullBoundaryConstraintBuilder}; +use stark::debug::validate_trace; +use stark::domain::Domain; +use stark::lookup::{ + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, NullBoundaryConstraintBuilder, +}; use stark::proof::options::ProofOptions; use stark::proof::stark::MultiProof; use stark::prover::{IsStarkProver, Prover, ProvingError}; @@ -66,7 +70,9 @@ use crate::tables::keccak_rnd::{ use crate::tables::load::{ bus_interactions as load_bus_interactions, cols as load_cols, constraints as load_constraints, }; -use crate::tables::lt::{LtOperation, bus_interactions as lt_bus_interactions, cols as lt_cols}; +use crate::tables::lt::{ + LtOperation, bus_interactions as lt_bus_interactions, cols as lt_cols, lt_constraints, +}; use crate::tables::memw::{ bus_interactions as memw_bus_interactions, cols as memw_cols, constraints as memw_constraints, }; @@ -78,7 +84,9 @@ use crate::tables::memw_register::{ bus_interactions as memw_register_bus_interactions, cols as memw_register_cols, constraints as memw_register_constraints, }; -use crate::tables::mul::{bus_interactions as mul_bus_interactions, cols as mul_cols}; +use crate::tables::mul::{ + bus_interactions as mul_bus_interactions, cols as mul_cols, mul_constraints, +}; use crate::tables::page::{bus_interactions as page_bus_interactions, cols as page_cols}; use crate::tables::register::{ bus_interactions as register_bus_interactions, cols as register_cols, @@ -89,7 +97,7 @@ use crate::tables::shift::{ use crate::tables::store::{ bus_interactions as store_bus_interactions, cols as store_cols, store_constraints, }; -use crate::tables::types::{GoldilocksExtension, GoldilocksField}; +use crate::tables::types::{BusId, GoldilocksExtension, GoldilocksField}; pub type F = GoldilocksField; pub type E = GoldilocksExtension; @@ -118,6 +126,79 @@ where ) } +// ============================================================================= +// Soundness regression helpers (negative AIR tests) +// ============================================================================= + +/// Build a bus-less AIR carrying only the given in-chip transition constraints. +/// With zero bus interactions, `AirWithBuses::new` appends no LogUp constraints +/// and allocates no aux columns, so `validate_trace` evaluates exactly the chip's +/// transition constraints over a main-only trace. +pub fn busless_air + 'static>( + num_columns: usize, + constraints: Vec, +) -> VmAir { + let transition_constraints = constraints.into_iter().map(|c| c.boxed()).collect(); + AirWithBuses::new( + num_columns, + AuxiliaryTraceBuildData { + interactions: vec![], + }, + &ProofOptions::default_test_options(), + 1, + transition_constraints, + ) +} + +/// Run `validate_trace` for a bus-less chip AIR over a main-only trace. +/// Returns `true` iff every transition constraint holds on every row. +pub fn validate_busless(air: &VmAir, trace: &TraceTable) -> bool { + let domain = Domain::new(air, trace.num_rows()); + validate_trace(air, &(), trace, &domain, &[], None) +} + +/// Number of transition constraints a production builder registers on top of its +/// bus constraints, as a delta against a bus-only AIR with the same interactions +/// but no in-chip constraints. Isolates the in-chip count even though +/// `AirWithBuses::new` also appends LogUp constraints, so a plain count cannot. +pub fn in_chip_constraint_count( + wired: usize, + num_columns: usize, + buses: Vec, +) -> usize { + let bus_only = AirWithBuses::::new( + num_columns, + AuxiliaryTraceBuildData { + interactions: buses, + }, + &ProofOptions::default_test_options(), + 1, + vec![], + ) + .num_transition_constraints(); + wired + .checked_sub(bus_only) + .expect("wired (in-chip + bus constraints) must be >= bus-only constraint count") +} + +/// Collect the `start_column`s of every `IS_HALFWORD` sender in `interactions`. +/// Used to assert input/operand half-limbs are range-checked. Scope: only +/// single-column `Packed` senders (which is how every current IS_HALFWORD sender is +/// declared); it does not inspect `Linear` senders or sender multiplicities. +pub fn is_halfword_sender_columns(interactions: &[BusInteraction]) -> Vec { + let id: u64 = BusId::IsHalfword.into(); + interactions + .iter() + .filter(|i| i.is_sender && i.bus_id == id) + .flat_map(|i| { + i.values.iter().filter_map(|v| match v { + BusValue::Packed { start_column, .. } => Some(*start_column), + BusValue::Linear(_) => None, + }) + }) + .collect() +} + // ============================================================================= // ELF Execution Helpers // ============================================================================= @@ -556,9 +637,11 @@ pub fn create_bitwise_air(proof_options: &ProofOptions) -> VmAir { .with_name("BITWISE") } -/// Create LT AIR with bus interactions. +/// Create LT AIR with constraints and bus interactions. pub fn create_lt_air(proof_options: &ProofOptions) -> VmAir { - let transition_constraints: Vec>> = vec![]; + let (constraints, _) = lt_constraints(0); + let transition_constraints: Vec>> = + constraints.into_iter().map(|c| c.boxed()).collect(); let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: lt_bus_interactions(), @@ -760,9 +843,11 @@ pub fn create_decode_air(proof_options: &ProofOptions) -> VmAir { .with_name("DECODE") } -/// Create MUL AIR with bus interactions. +/// Create MUL AIR with constraints and bus interactions. pub fn create_mul_air(proof_options: &ProofOptions) -> VmAir { - let transition_constraints: Vec>> = vec![]; + let (constraints, _) = mul_constraints(0); + let transition_constraints: Vec>> = + constraints.into_iter().map(|c| c.boxed()).collect(); let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: mul_bus_interactions(), diff --git a/prover/src/tests/dvrm_tests.rs b/prover/src/tests/dvrm_tests.rs index 2ed37b968..816549c3f 100644 --- a/prover/src/tests/dvrm_tests.rs +++ b/prover/src/tests/dvrm_tests.rs @@ -1,7 +1,16 @@ //! Tests for the DVRM (Division/Remainder) table. -use crate::tables::dvrm::{DvrmOperation, bus_interactions, cols, generate_dvrm_trace}; +use stark::proof::options::ProofOptions; +use stark::traits::AIR; + +use crate::tables::dvrm::{ + DvrmOperation, bus_interactions, cols, dvrm_constraints, generate_dvrm_trace, +}; use crate::tables::types::FE; +use crate::test_utils::{ + busless_air, create_dvrm_air, in_chip_constraint_count, is_halfword_sender_columns, + validate_busless, +}; /// Signed comparison flag const SIGNED: bool = true; @@ -295,14 +304,15 @@ fn test_different_signed_flags_separate_rows() { fn test_bus_interactions_count() { let interactions = bus_interactions(); // Expected interactions: - // - 12x IS_HALF senders (r×4, n_sub_r×4, q×4) — n and d are assumptions (A1, A2) + // - 8x IS_HALF senders for inputs (n×4, d×4) — A1/A2 now enforced, not assumed + // - 12x IS_HALF senders (r×4, n_sub_r×4, q×4) // - 3x MSB16 senders (sign_n, sign_r, sign_d) // - 1x LT sender (|r| < |d|) // - 2x MUL senders (n_sub_r = d*q lo + hi) // - 6x ZERO senders (C3×2 NEG r, C5×2 NEG d, C8 overflow, C17 div_by_zero) // - 2x DVRM receivers (quotient, remainder) - // Total: 12 + 3 + 1 + 2 + 6 + 2 = 26 - assert_eq!(interactions.len(), 26, "Expected 26 bus interactions"); + // Total: 8 + 12 + 3 + 1 + 2 + 6 + 2 = 34 + assert_eq!(interactions.len(), 34, "Expected 34 bus interactions"); } #[test] @@ -399,3 +409,57 @@ fn test_padding_row() { assert_eq!(row[cols::MU_Q], FE::zero()); assert_eq!(row[cols::MU_R], FE::zero()); } + +// Div-by-zero remainder: a division-by-zero row must return the numerator as the +// remainder. This holds via the existing carry-chain / equality constraints +// (`n_sub_r + r = n`); an explicit `div_by_zero => r = n` constraint is a spec-level +// addition the spec does not mandate, so it is intentionally not added here. + +/// Enforcement: on a division-by-zero row, forging `r != n` is rejected by the +/// carry-chain constraints (`n_sub_r + r = n`), evaluated in isolation over a bus-less +/// AIR — no explicit div-by-zero remainder constraint is needed. +#[test] +fn test_dvrm_rejects_false_div_by_zero_remainder() { + let air = busless_air(cols::NUM_COLUMNS, dvrm_constraints(0).0); + // numerator = 20, denominator = 0 => div-by-zero, honest remainder = 20. + let mut trace = generate_dvrm_trace(&[(DvrmOperation::new(20, 0, UNSIGNED), true)]); + assert!( + validate_busless(&air, &trace), + "honest div-by-zero row (r = n = 20) must validate" + ); + + trace.set_main(0, cols::R_0, FE::from(999u64)); + assert!( + !validate_busless(&air, &trace), + "a forged remainder on div-by-zero must be rejected by the carry-chain constraints" + ); +} + +// Soundness regression (VM-5): the denominator halves must be IS_HALFWORD +// range-checked so a prover cannot forge `div_by_zero` via non-canonical halves. + +/// Presence: the denominator halves are range-checked via IS_HALFWORD senders. +#[test] +fn test_dvrm_range_checks_denominator_halves() { + let cols_checked = is_halfword_sender_columns(&bus_interactions()); + for c in [cols::D_0, cols::D_1, cols::D_2, cols::D_3] { + assert!( + cols_checked.contains(&c), + "DVRM must IS_HALF range-check denominator half column {c}" + ); + } +} + +/// Wiring: `create_dvrm_air` registers its in-chip constraints on top of its bus +/// constraints. Catches a revert to `transition_constraints = vec![]` or a dropped +/// constraint. +#[test] +fn test_dvrm_air_wires_in_chip_constraints() { + let air = create_dvrm_air(&ProofOptions::default_test_options()); + let in_chip = in_chip_constraint_count( + air.num_transition_constraints(), + cols::NUM_COLUMNS, + bus_interactions(), + ); + assert_eq!(in_chip, dvrm_constraints(0).0.len()); +} diff --git a/prover/src/tests/lt_tests.rs b/prover/src/tests/lt_tests.rs index 21ce549aa..c63ac29ad 100644 --- a/prover/src/tests/lt_tests.rs +++ b/prover/src/tests/lt_tests.rs @@ -1,7 +1,11 @@ //! Tests for the LT (Less-Than) table. -use crate::tables::lt::{LtOperation, bus_interactions, cols, generate_lt_trace}; +use stark::proof::options::ProofOptions; +use stark::traits::AIR; + +use crate::tables::lt::{LtOperation, bus_interactions, cols, generate_lt_trace, lt_constraints}; use crate::tables::types::FE; +use crate::test_utils::{busless_air, create_lt_air, in_chip_constraint_count, validate_busless}; /// Signed comparison flag const SIGNED: bool = true; @@ -168,3 +172,40 @@ fn test_bus_interactions_count() { // timestamp / |r|<|d| checks) = 9. assert_eq!(interactions.len(), 9); } + +// Soundness regression: `lt` must equal `(lhs < rhs)`. The in-chip constraints were +// dead code until they were wired into the production `create_lt_air`, so a prover +// could certify a false comparison (and, via the memory-timestamp LT bus, forge +// memory consistency). These guard against reintroducing that hole. + +/// Enforcement: a forged `lt = 1` for `20