Fix/soundness underconstrained chips (#652)

* register missing in-chip soundness constraints

* add underconstrained-chip soundness guard

* add underconstrained-chip soundness regression tests

* harden in_chip_constraint_count against
  unsigned-subtraction underflow

* Revert beyond-spec SHIFT/DVRM constraints

* Update stale comments and capacity estimate

* Fix stale bus-interaction comments left by soundness fixes

The IS_HALF/IS_HALFWORD senders added in this PR made several doc
comments and one capacity hint inaccurate; update them to match.

- dvrm.rs: module doc IS_HALF count ×16 -> ×20 (matches the function
  doc, which already said ×20 after n/d were added)
- mul.rs: module + bus_interactions docs IS_HALF ×8 -> ×16 and note the
  lhs/rhs input range checks, not just lo/hi outputs
- shift.rs: module doc "11 total" -> "15 total", add IS_HALFWORD (×4) to
  the sender list, and bump Vec::with_capacity(11) -> 15
- test_utils.rs: create_lt_air / create_mul_air now wire transition
  constraints, so their doc comments say "constraints and bus
  interactions" (matching create_shift_air / create_dvrm_air)

---------

Co-authored-by: Diego K <43053772+diegokingston@users.noreply.github.com>
Co-authored-by: MauroFab <maurotoscano2@gmail.com>

Author: 3 people

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: LT (×1 for abs_r < abs_d)
 //! - Sender: MUL (×2 for n_sub_r = d * q verification)
@@ -384,9 +384,34 @@ pub fn generate_dvrm_trace(
 pub fn bus_interactions() -> Vec<BusInteraction> {
     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

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: MUL (×2 for lo and hi results)
 
@@ -358,7 +358,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<BusInteraction> {
@@ -399,6 +399,31 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         ],
     ));
 
+    // -------------------------------------------------------------------------
+    // 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)
     // -------------------------------------------------------------------------

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;
@@ -377,7 +377,7 @@ pub fn generate_shift_trace(
 
 /// Creates all bus interactions for the SHIFT table.
 pub fn bus_interactions() -> Vec<BusInteraction> {
-    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(
@@ -599,6 +599,22 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         ],
     ));
 
+    // 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
 }
 
@@ -932,6 +948,16 @@ pub fn collect_bitwise_from_shift(operations: &[ShiftOperation]) -> Vec<BitwiseO
             op.shift,
             mask,
         ));
+
+        // 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

prover/src/tables/trace_builder.rs

@@ -1141,16 +1141,30 @@ fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec<BitwiseOperation> {
 /// 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<BitwiseOperation> {
-    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;
@@ -1213,16 +1227,32 @@ fn collect_bitwise_from_mul(mul_ops: &[(MulOperation, bool)]) -> Vec<BitwiseOper
 
 /// Collects bitwise lookups from DVRM operations.
 ///
-/// Generates: IS_HALF (×12), MSB16 (×3), ZERO (×2 per raw op + up to ×4 per unique signed op).
+/// Generates: IS_HALF (×20: n, d, r, n_sub_r, q) and ZERO (×2) per raw op, plus
+/// MSB16 (up to ×3) and NEG ZERO (up to ×4) per unique signed op.
 ///
-/// DVRM-A1 (IS_HALF[n]) and DVRM-A2 (IS_HALF[d]) are assumptions enforced by the CPU sender,
-/// not by the DVRM table. Only constraint-level IS_HALF lookups are generated here.
+/// DVRM-A1 (IS_HALF[n]) and DVRM-A2 (IS_HALF[d]) are range-checked by the DVRM
+/// table itself (n/d IS_HALF senders in dvrm::bus_interactions), so their lookups
+/// are collected here alongside the constraint-level ones.
 ///
 /// Returns: Vec of bitwise lookups
 fn collect_bitwise_from_dvrm(dvrm_ops: &[(DvrmOperation, bool)]) -> Vec<BitwiseOperation> {
-    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] {

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};
@@ -59,7 +63,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,
 };
@@ -71,15 +77,17 @@ 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,
 };
 use crate::tables::shift::{
     bus_interactions as shift_bus_interactions, cols as shift_cols, shift_constraints,
 };
-use crate::tables::types::{GoldilocksExtension, GoldilocksField};
+use crate::tables::types::{BusId, GoldilocksExtension, GoldilocksField};
 
 pub type F = GoldilocksField;
 pub type E = GoldilocksExtension;
@@ -108,6 +116,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<C: TransitionConstraint<F, E> + 'static>(
+    num_columns: usize,
+    constraints: Vec<C>,
+) -> 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<F, E>) -> 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<BusInteraction>,
+) -> usize {
+    let bus_only = AirWithBuses::<F, E, NullBoundaryConstraintBuilder, ()>::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<usize> {
+    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
 // =============================================================================
@@ -540,9 +621,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<Box<dyn TransitionConstraintEvaluator<F, E>>> = vec![];
+    let (constraints, _) = lt_constraints(0);
+    let transition_constraints: Vec<Box<dyn TransitionConstraintEvaluator<F, E>>> =
+        constraints.into_iter().map(|c| c.boxed()).collect();
 
     let auxiliary_trace_build_data = AuxiliaryTraceBuildData {
         interactions: lt_bus_interactions(),
@@ -680,9 +763,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<Box<dyn TransitionConstraintEvaluator<F, E>>> = vec![];
+    let (constraints, _) = mul_constraints(0);
+    let transition_constraints: Vec<Box<dyn TransitionConstraintEvaluator<F, E>>> =
+        constraints.into_iter().map(|c| c.boxed()).collect();
 
     let auxiliary_trace_build_data = AuxiliaryTraceBuildData {
         interactions: mul_bus_interactions(),