Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 1 addition & 5 deletions prover/src/tables/shift.rs
Original file line number Diff line number Diff line change
Expand Up @@ -990,11 +990,7 @@ pub fn shift_constraints(constraint_idx_start: usize) -> (Vec<ShiftConstraint>,

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<BitwiseOperation> {
// No deduplication: each operation has μ=1, matching generate_shift_trace.
let mut bitwise_ops = Vec::new();
Expand Down
199 changes: 108 additions & 91 deletions prover/src/tables/trace_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1452,8 +1452,15 @@ fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec<BitwiseOperation> {
/// 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<BitwiseOperation> {
pub(crate) fn collect_bitwise_from_mul(
mul_ops: &[(MulOperation, bool)],
max_rows_mul: usize,
) -> Vec<BitwiseOperation> {
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))
Expand Down Expand Up @@ -1504,28 +1511,28 @@ fn collect_bitwise_from_mul(mul_ops: &[(MulOperation, bool)]) -> Vec<BitwiseOper
}
}

// MSB16: one per unique signed op (multiplicity Column(LHS_SIGNED) / Column(RHS_SIGNED))
// The MUL table sends MSB16 with multiplicity = value of the SIGNED column (0 or 1)
// per unique row, so we must generate exactly one MSB16 per unique MUL operation,
// not per raw op.
let mut msb16_seen = std::collections::HashSet::new();
for (op, _wants_hi) in mul_ops {
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,
));
// 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,
));
}
}
}
}
Expand All @@ -1536,14 +1543,21 @@ fn collect_bitwise_from_mul(mul_ops: &[(MulOperation, bool)]) -> Vec<BitwiseOper
/// Collects bitwise lookups from DVRM operations.
///
/// 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.
/// MSB16 (up to ×3) and NEG ZERO (up to ×4) per unique signed op per chunk.
///
/// 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.
///
/// IS_HALF and ZERO (C8/C20) are emitted once per raw op. MSB16 and the
/// NEG-template ZERO lookups (C3/C5) are deduplicated per `max_rows_dvrm`
/// chunk, mirroring `chunk_and_generate`.
///
/// Returns: Vec of bitwise lookups
fn collect_bitwise_from_dvrm(dvrm_ops: &[(DvrmOperation, bool)]) -> Vec<BitwiseOperation> {
pub(crate) fn collect_bitwise_from_dvrm(
dvrm_ops: &[(DvrmOperation, bool)],
max_rows_dvrm: usize,
) -> Vec<BitwiseOperation> {
let mut bitwise_ops = Vec::with_capacity(dvrm_ops.len() * 24);

for (op, _wants_remainder) in dvrm_ops {
Expand Down Expand Up @@ -1624,77 +1638,77 @@ fn collect_bitwise_from_dvrm(dvrm_ops: &[(DvrmOperation, bool)]) -> Vec<BitwiseO
bitwise_ops.push(BitwiseOperation::zero(d_sum));
}

// MSB16 lookups: one per unique signed op (not per raw op).
// The DVRM bus interaction uses Multiplicity::Column(SIGNED)=1, so we
// must emit exactly one MSB16 per unique signed (n, d) combo.
let mut msb16_seen = std::collections::HashSet::new();
for (op, _wants_remainder) in dvrm_ops {
if op.signed && msb16_seen.insert(op.clone()) {
let r = op.compute_remainder();
// MSB16: same per-chunk dedup as MUL (Column(SIGNED) is a bit, not a count).
for chunk in dvrm_ops.chunks(max_rows_dvrm) {
let mut msb16_seen = std::collections::HashSet::new();
for (op, _wants_remainder) in chunk {
if op.signed && msb16_seen.insert(op.clone()) {
let r = op.compute_remainder();

// 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[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],
));
}
}
}
}
Expand Down Expand Up @@ -2737,8 +2751,11 @@ fn build_traces(
// PHASE 4: All → Bitwise lookups
// =====================================================================
bitwise_ops.extend(collect_bitwise_from_lt(&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.
Expand Down
90 changes: 90 additions & 0 deletions prover/src/tests/dvrm_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)"
);
}
Loading
Loading