diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index c8cd5df62..e955d9201 100644 --- a/prover/src/tables/shift.rs +++ b/prover/src/tables/shift.rs @@ -990,11 +990,7 @@ pub fn shift_constraints(constraint_idx_start: usize) -> (Vec, use super::bitwise::{BitwiseOperation, BitwiseOperationType}; -/// Collect BITWISE table lookups needed by a set of unique shift operations. -/// -/// Each unique operation (with its multiplicity) generates HWSL/BYTE_ALU/MSB16/ZERO -/// lookups. The lookups must be generated per-unique-operation (matching the SHIFT table's -/// deduplication and μ column), and repeated `multiplicity` times. +/// Collect BITWISE table lookups needed by a set of shift operations. pub fn collect_bitwise_from_shift(operations: &[ShiftOperation]) -> Vec { // No deduplication: each operation has μ=1, matching generate_shift_trace. let mut bitwise_ops = Vec::new(); diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 04f675f6e..41e0104d8 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1452,8 +1452,15 @@ fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec { /// IS_HALF lookups for lhs/rhs input and lo/hi output range checks, /// and IS_B20 lookups for carry range checks. /// +/// IS_HALF and IS_B20 are emitted once per raw op. MSB16 is deduplicated +/// per `max_rows_mul` chunk, mirroring `chunk_and_generate` — a unique signed +/// op that spans two instances is sent twice and must be tallied twice. +/// /// Returns: Vec of bitwise lookups -fn collect_bitwise_from_mul(mul_ops: &[(MulOperation, bool)]) -> Vec { +pub(crate) fn collect_bitwise_from_mul( + mul_ops: &[(MulOperation, bool)], + max_rows_mul: usize, +) -> Vec { 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)) @@ -1504,28 +1511,28 @@ fn collect_bitwise_from_mul(mul_ops: &[(MulOperation, bool)]) -> Vec> 48) & 0xFFFF) as u16; - bitwise_ops.push(BitwiseOperation::halfword( - BitwiseOperationType::Msb16, - (lhs_3 & 0xFF) as u8, - (lhs_3 >> 8) as u8, - )); - } - if op.rhs_signed { - let rhs_3 = ((op.rhs >> 48) & 0xFFFF) as u16; - bitwise_ops.push(BitwiseOperation::halfword( - BitwiseOperationType::Msb16, - (rhs_3 & 0xFF) as u8, - (rhs_3 >> 8) as u8, - )); + // MSB16: dedup per chunk — the MUL AIR sends Msb16 once per unique signed row + // per instance, so the collector must mirror the same chunk boundary. + for chunk in mul_ops.chunks(max_rows_mul) { + let mut msb16_seen = std::collections::HashSet::new(); + for (op, _wants_hi) in chunk { + if msb16_seen.insert((op.lhs, op.lhs_signed, op.rhs, op.rhs_signed)) { + if op.lhs_signed { + let lhs_3 = ((op.lhs >> 48) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::Msb16, + (lhs_3 & 0xFF) as u8, + (lhs_3 >> 8) as u8, + )); + } + if op.rhs_signed { + let rhs_3 = ((op.rhs >> 48) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::Msb16, + (rhs_3 & 0xFF) as u8, + (rhs_3 >> 8) as u8, + )); + } } } } @@ -1536,14 +1543,21 @@ fn collect_bitwise_from_mul(mul_ops: &[(MulOperation, bool)]) -> Vec Vec { +pub(crate) fn collect_bitwise_from_dvrm( + dvrm_ops: &[(DvrmOperation, bool)], + max_rows_dvrm: usize, +) -> Vec { let mut bitwise_ops = Vec::with_capacity(dvrm_ops.len() * 24); for (op, _wants_remainder) in dvrm_ops { @@ -1624,77 +1638,77 @@ fn collect_bitwise_from_dvrm(dvrm_ops: &[(DvrmOperation, bool)]) -> Vec> 48) & 0xFFFF) as u16; - bitwise_ops.push(BitwiseOperation::halfword( - BitwiseOperationType::Msb16, - (n_3 & 0xFF) as u8, - (n_3 >> 8) as u8, - )); + // MSB16[n[3]] + let n_3 = ((op.n >> 48) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::Msb16, + (n_3 & 0xFF) as u8, + (n_3 >> 8) as u8, + )); - // MSB16[r[3]] - let r_3 = ((r >> 48) & 0xFFFF) as u16; - bitwise_ops.push(BitwiseOperation::halfword( - BitwiseOperationType::Msb16, - (r_3 & 0xFF) as u8, - (r_3 >> 8) as u8, - )); + // MSB16[r[3]] + let r_3 = ((r >> 48) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::Msb16, + (r_3 & 0xFF) as u8, + (r_3 >> 8) as u8, + )); - // MSB16[d[3]] - let d_3 = ((op.d >> 48) & 0xFFFF) as u16; - bitwise_ops.push(BitwiseOperation::halfword( - BitwiseOperationType::Msb16, - (d_3 & 0xFF) as u8, - (d_3 >> 8) as u8, - )); + // MSB16[d[3]] + let d_3 = ((op.d >> 48) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::Msb16, + (d_3 & 0xFF) as u8, + (d_3 >> 8) as u8, + )); + } } } - // ZERO lookups for NEG template: one per unique op where sign is set. - // C3 uses Multiplicity::Column(SIGN_R) = 1 per unique row where sign_r = 1. - // C5 uses Multiplicity::Column(SIGN_D) = 1 per unique row where sign_d = 1. - let mut zero_seen = std::collections::HashSet::new(); - for (op, _wants_remainder) in dvrm_ops { - if zero_seen.insert(op.clone()) { - // C3: NEG for r (when sign_r = 1) - if op.sign_r() { - let r = op.compute_remainder(); - let r_halves: [u32; 4] = [ - (r & 0xFFFF) as u32, - ((r >> 16) & 0xFFFF) as u32, - ((r >> 32) & 0xFFFF) as u32, - ((r >> 48) & 0xFFFF) as u32, - ]; - // C3a: ZERO[1-carry_r[0]; r[0]+r[1]] - bitwise_ops.push(BitwiseOperation::zero(r_halves[0] + r_halves[1])); - // C3b: ZERO[1-carry_r[1]; r[0]+r[1]+r[2]+r[3]] - bitwise_ops.push(BitwiseOperation::zero( - r_halves[0] + r_halves[1] + r_halves[2] + r_halves[3], - )); - } + // ZERO (NEG template): same — SIGN_R/SIGN_D are bits, dedup per chunk. + for chunk in dvrm_ops.chunks(max_rows_dvrm) { + let mut zero_seen = std::collections::HashSet::new(); + for (op, _wants_remainder) in chunk { + if zero_seen.insert(op.clone()) { + // C3: NEG for r (when sign_r = 1) + if op.sign_r() { + let r = op.compute_remainder(); + let r_halves: [u32; 4] = [ + (r & 0xFFFF) as u32, + ((r >> 16) & 0xFFFF) as u32, + ((r >> 32) & 0xFFFF) as u32, + ((r >> 48) & 0xFFFF) as u32, + ]; + // C3a: ZERO[1-carry_r[0]; r[0]+r[1]] + bitwise_ops.push(BitwiseOperation::zero(r_halves[0] + r_halves[1])); + // C3b: ZERO[1-carry_r[1]; r[0]+r[1]+r[2]+r[3]] + bitwise_ops.push(BitwiseOperation::zero( + r_halves[0] + r_halves[1] + r_halves[2] + r_halves[3], + )); + } - // C5: NEG for d (when sign_d = 1) - if op.sign_d() { - let d_halves: [u32; 4] = [ - (op.d & 0xFFFF) as u32, - ((op.d >> 16) & 0xFFFF) as u32, - ((op.d >> 32) & 0xFFFF) as u32, - ((op.d >> 48) & 0xFFFF) as u32, - ]; - // C5a: ZERO[1-carry_d[0]; d[0]+d[1]] - bitwise_ops.push(BitwiseOperation::zero(d_halves[0] + d_halves[1])); - // C5b: ZERO[1-carry_d[1]; d[0]+d[1]+d[2]+d[3]] - bitwise_ops.push(BitwiseOperation::zero( - d_halves[0] + d_halves[1] + d_halves[2] + d_halves[3], - )); + // C5: NEG for d (when sign_d = 1) + if op.sign_d() { + let d_halves: [u32; 4] = [ + (op.d & 0xFFFF) as u32, + ((op.d >> 16) & 0xFFFF) as u32, + ((op.d >> 32) & 0xFFFF) as u32, + ((op.d >> 48) & 0xFFFF) as u32, + ]; + // C5a: ZERO[1-carry_d[0]; d[0]+d[1]] + bitwise_ops.push(BitwiseOperation::zero(d_halves[0] + d_halves[1])); + // C5b: ZERO[1-carry_d[1]; d[0]+d[1]+d[2]+d[3]] + bitwise_ops.push(BitwiseOperation::zero( + d_halves[0] + d_halves[1] + d_halves[2] + d_halves[3], + )); + } } } } @@ -2737,8 +2751,11 @@ fn build_traces( // PHASE 4: All → Bitwise lookups // ===================================================================== bitwise_ops.extend(collect_bitwise_from_lt(<_ops)); - bitwise_ops.extend(collect_bitwise_from_mul(&mul_ops)); - bitwise_ops.extend(collect_bitwise_from_dvrm(&dvrm_ops)); + // MUL/DVRM dedup their per-unique bit-gated lookups PER CHIP INSTANCE, so pass + // the same chunk size used to split them into instances (see chunk_and_generate + // below) so the BITWISE multiplicity matches the per-instance sends. + bitwise_ops.extend(collect_bitwise_from_mul(&mul_ops, max_rows.mul)); + bitwise_ops.extend(collect_bitwise_from_dvrm(&dvrm_ops, max_rows.dvrm)); bitwise_ops.extend(collect_bitwise_from_branch(&branch_ops)); bitwise_ops.extend(shift::collect_bitwise_from_shift(&shift_ops)); // Auxiliary chips: BYTEWISE sends 8× BYTE_ALU/op; EQ sends 4× IS_HALF + ZERO. diff --git a/prover/src/tests/dvrm_tests.rs b/prover/src/tests/dvrm_tests.rs index 816549c3f..6dfbe34c5 100644 --- a/prover/src/tests/dvrm_tests.rs +++ b/prover/src/tests/dvrm_tests.rs @@ -463,3 +463,93 @@ fn test_dvrm_air_wires_in_chip_constraints() { ); assert_eq!(in_chip, dvrm_constraints(0).0.len()); } + +/// Regression test for the `Msb16` LogUp over-send bug. +/// +/// DVRM is split into chip instances of `max_rows.dvrm` raw ops (`chunk_and_generate`) +/// and each instance deduplicates only its own chunk, sending its three MSB16 sign +/// lookups once per unique signed op *per instance* (multiplicity = the `SIGNED` bit). +/// So `collect_bitwise_from_dvrm`, which feeds the BITWISE MSB16 multiplicity, must use +/// the *same* per-chunk dedup: a unique signed op spanning two instances is sent twice +/// but, with a single global dedup, would be tallied once — leaving the `Msb16` bus +/// unbalanced and verification failing for any block large enough to split DVRM. +#[test] +fn msb16_bitwise_multiplicity_matches_per_instance_sends() { + use crate::tables::bitwise::BitwiseOperationType; + use crate::tables::trace_builder::collect_bitwise_from_dvrm; + + let chunk = 4usize; + // One unique signed div op repeated so it spans two `chunk`-sized instances. + let op = DvrmOperation::new(0x0123_4567_89ab_cdef, 0x0000_0000_0001_0001, true); + let ops: Vec<(DvrmOperation, bool)> = std::iter::repeat_n((op, false), 6).collect(); + assert!( + ops.len() > chunk, + "scenario must split DVRM into >1 instance" + ); + + // The DVRM AIR sends three MSB16 lookups (n[3], r[3], d[3]) each with multiplicity + // Column(SIGNED) per row, so total sends = Σ rows (SIGNED) × 3. + let mut sends = 0usize; + for c in ops.chunks(chunk) { + let trace = generate_dvrm_trace(c); + for row in 0..trace.num_rows() { + if *trace.get_main(row, cols::SIGNED) == FE::one() { + sends += 3; + } + } + } + assert_eq!(sends, 6, "sanity: 2 instances × 3 MSB16 sends"); + + let tallied = collect_bitwise_from_dvrm(&ops, chunk) + .iter() + .filter(|b| matches!(b.lookup_type, BitwiseOperationType::Msb16)) + .count(); + assert_eq!( + tallied, sends, + "BITWISE MSB16 multiplicity ({tallied}) must equal total DVRM-instance MSB16 \ + sends ({sends}); a mismatch leaves the Msb16 bus unbalanced" + ); +} + +/// Regression test for the DVRM NEG-template ZERO lookups — the *other* per-unique +/// bit-gated loop the same fix converted to per-chunk dedup (the MSB16 test above +/// covers the first one). C3/C5 emit ZERO lookups gated by the `SIGN_R`/`SIGN_D` bits, +/// once per unique signed op, so they must deduplicate PER CHIP INSTANCE just like MSB16. +#[test] +fn neg_template_zero_lookups_dedup_per_chip_instance() { + use crate::tables::bitwise::BitwiseOperationType; + use crate::tables::trace_builder::collect_bitwise_from_dvrm; + + // Signed op with negative remainder AND negative divisor -> sign_r = sign_d = 1, so the + // NEG template (C3/C5) emits per-unique ZERO lookups gated by those bits. + let op = DvrmOperation::new((-20i64) as u64, (-3i64) as u64, SIGNED); + assert!( + op.sign_r() && op.sign_d(), + "scenario needs sign_r = sign_d = 1" + ); + let ops: Vec<(DvrmOperation, bool)> = std::iter::repeat_n((op, false), 6).collect(); + + let zero_lookups = |chunk: usize| { + collect_bitwise_from_dvrm(&ops, chunk) + .iter() + .filter(|b| matches!(b.lookup_type, BitwiseOperationType::Zero)) + .count() + }; + + // The per-raw ZERO lookups (C8/C20) are identical regardless of chunking; only the + // per-unique NEG-template ZEROs differ. A global dedup emits them once for the whole + // list, so the count would NOT change with chunk size; the per-instance fix emits them + // once per instance, so two instances must produce strictly more ZERO lookups than one. + // (Without the fix these are equal and this assertion fails.) + let one_instance = zero_lookups(ops.len()); // chunks(6) -> 1 chunk + let two_instances = zero_lookups(4); // chunks(4) -> [4],[2] -> 2 chunks + assert!( + one_instance > 0, + "expected NEG-template ZERO lookups to be emitted" + ); + assert!( + two_instances > one_instance, + "per-instance dedup of NEG-template ZERO lookups regressed: \ + {two_instances} (2 instances) must exceed {one_instance} (1 instance)" + ); +} diff --git a/prover/src/tests/mul_tests.rs b/prover/src/tests/mul_tests.rs index f5d2d2644..63f85c164 100644 --- a/prover/src/tests/mul_tests.rs +++ b/prover/src/tests/mul_tests.rs @@ -367,3 +367,50 @@ fn test_mul_range_checks_input_halves() { ); } } + +/// Regression test for the `Msb16` LogUp over-send bug. +/// +/// MUL is split into chip instances of `max_rows.mul` raw ops (`chunk_and_generate`) +/// and each instance deduplicates only its own chunk, sending the MSB16 sign lookup +/// once per unique signed op *per instance* (multiplicity = the `SIGNED` bit). So +/// `collect_bitwise_from_mul`, which feeds the BITWISE MSB16 multiplicity, must use +/// the *same* per-chunk dedup: a unique signed op spanning two instances is sent +/// twice but, with a single global dedup, would be tallied once — leaving the `Msb16` +/// bus unbalanced and verification failing for any block large enough to split MUL. +#[test] +fn msb16_bitwise_multiplicity_matches_per_instance_sends() { + use crate::tables::bitwise::BitwiseOperationType; + use crate::tables::trace_builder::collect_bitwise_from_mul; + + let chunk = 4usize; + // One unique signed mul op repeated so it spans two `chunk`-sized instances. + let op = MulOperation::new(0x1234_5678_9abc_def0, true, 0x0fed_cba9_8765_4321, true); + let ops: Vec<(MulOperation, bool)> = std::iter::repeat_n((op, false), 6).collect(); + assert!( + ops.len() > chunk, + "scenario must split MUL into >1 instance" + ); + + // Ground truth: each instance is one chunk, and the MUL AIR sends MSB16 with + // multiplicity Column(LHS_SIGNED) (lhs) and Column(RHS_SIGNED) (rhs) per row, so + // total sends = Σ rows (LHS_SIGNED + RHS_SIGNED). + let mut sends = 0usize; + for c in ops.chunks(chunk) { + let trace = generate_mul_trace(c); + for row in 0..trace.num_rows() { + sends += (*trace.get_main(row, cols::LHS_SIGNED) == FE::one()) as usize; + sends += (*trace.get_main(row, cols::RHS_SIGNED) == FE::one()) as usize; + } + } + assert_eq!(sends, 4, "sanity: 2 instances × (lhs + rhs) sends"); + + let tallied = collect_bitwise_from_mul(&ops, chunk) + .iter() + .filter(|b| matches!(b.lookup_type, BitwiseOperationType::Msb16)) + .count(); + assert_eq!( + tallied, sends, + "BITWISE MSB16 multiplicity ({tallied}) must equal total MUL-instance MSB16 \ + sends ({sends}); a mismatch leaves the Msb16 bus unbalanced" + ); +}