diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index cd4954667..12ae7e3cc 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -1220,101 +1220,26 @@ pub fn bus_interactions() -> Vec { // ------------------------------------------------------------------------- // LT interaction (for SLT, BLT) // ------------------------------------------------------------------------- - // LT[arg1::DWordHHW, arg2::DWordHHW, signed] -> res[0] + // LT[arg1, arg2, signed] -> res[0] // multiplicity = SLT + BLT // - // DWordHHW format: [Word(0-31), Half(32-47), Half(48-63)] - // arg1/arg2 are DWordBL (8 bytes), need to repack: - // Word = byte[0] + 2^8*byte[1] + 2^16*byte[2] + 2^24*byte[3] - // Half1 = byte[4] + 2^8*byte[5] - // Half2 = byte[6] + 2^8*byte[7] + // LT bus uses 2 elements per 64-bit operand: [lo32, hi32] + // arg1/arg2 are DWordBL (8 bytes) - use Packing::DWordBL to produce 2 elements interactions.push(BusInteraction::sender( BusId::Lt, // SLT + BLT using Multiplicity::Sum Multiplicity::Sum(cols::SLT, cols::BLT), vec![ - // arg1[0]: Word (lower 32 bits) - BusValue::linear(vec![ - stark::lookup::LinearTerm::Column { - coefficient: 1, - column: cols::ARG1[0], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 8, - column: cols::ARG1[1], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 16, - column: cols::ARG1[2], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 24, - column: cols::ARG1[3], - }, - ]), - // arg1[1]: Half (bits 32-47) - BusValue::linear(vec![ - stark::lookup::LinearTerm::Column { - coefficient: 1, - column: cols::ARG1[4], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 8, - column: cols::ARG1[5], - }, - ]), - // arg1[2]: Half (bits 48-63) - BusValue::linear(vec![ - stark::lookup::LinearTerm::Column { - coefficient: 1, - column: cols::ARG1[6], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 8, - column: cols::ARG1[7], - }, - ]), - // arg2[0]: Word (lower 32 bits) - BusValue::linear(vec![ - stark::lookup::LinearTerm::Column { - coefficient: 1, - column: cols::ARG2[0], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 8, - column: cols::ARG2[1], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 16, - column: cols::ARG2[2], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 24, - column: cols::ARG2[3], - }, - ]), - // arg2[1]: Half (bits 32-47) - BusValue::linear(vec![ - stark::lookup::LinearTerm::Column { - coefficient: 1, - column: cols::ARG2[4], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 8, - column: cols::ARG2[5], - }, - ]), - // arg2[2]: Half (bits 48-63) - BusValue::linear(vec![ - stark::lookup::LinearTerm::Column { - coefficient: 1, - column: cols::ARG2[6], - }, - stark::lookup::LinearTerm::Column { - coefficient: 1 << 8, - column: cols::ARG2[7], - }, - ]), + // arg1 as DWordBL (8 bytes → 2 elements: [lo32, hi32]) + BusValue::Packed { + start_column: cols::ARG1[0], + packing: Packing::DWordBL, + }, + // arg2 as DWordBL (8 bytes → 2 elements: [lo32, hi32]) + BusValue::Packed { + start_column: cols::ARG2[0], + packing: Packing::DWordBL, + }, // signed flag BusValue::Packed { start_column: cols::SIGNED, diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index 75fc673b6..40025c5bd 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -22,7 +22,7 @@ //! //! ## Bus Interactions //! - Sender: MSB16 (×2 for lhs_msb, rhs_msb) -//! - Sender: IS_HALFWORD (×4 for lhs_sub_rhs range check) +//! - Sender: IS_HALFWORD (×6: ×4 for lhs_sub_rhs, ×1 for lhs[1], ×1 for rhs[1]) //! - Receiver: LT (provides less-than results to other tables) use math::field::element::FieldElement; @@ -276,37 +276,41 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), + // IS_HALFWORD[lhs[1]] + BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(cols::MU), + vec![BusValue::Packed { + start_column: cols::LHS_1, + packing: Packing::Direct, + }], + ), + // IS_HALFWORD[rhs[1]] + BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(cols::MU), + vec![BusValue::Packed { + start_column: cols::RHS_1, + packing: Packing::Direct, + }], + ), // LT[lhs, rhs, signed] -> lt (receiver) // lhs is DWordHHW, rhs is DWordHHW, signed is Bit, lt is Bit + // Uses DWordHHW packing: reads 3 columns (Word, Half, Half), produces 2 bus elements [lo32, hi32] + // This allows DWordWL senders (like MEMW timestamps) to match via Packing::DWordWL BusInteraction::receiver( BusId::Lt, Multiplicity::Column(cols::MU), vec![ - // lhs as DWordHHW (3 elements: Word, Half, Half) + // lhs as DWordHHW (reads 3 columns: Word, Half, Half; produces 2 elements: [lo32, hi32]) BusValue::Packed { start_column: cols::LHS_0, - packing: Packing::Direct, + packing: Packing::DWordHHW, }, - BusValue::Packed { - start_column: cols::LHS_1, - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::LHS_2, - packing: Packing::Direct, - }, - // rhs as DWordHHW (3 elements) + // rhs as DWordHHW (reads 3 columns, produces 2 elements) BusValue::Packed { start_column: cols::RHS_0, - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::RHS_1, - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::RHS_2, - packing: Packing::Direct, + packing: Packing::DWordHHW, }, // signed BusValue::Packed { diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 269419b0a..2ed3fa937 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -191,7 +191,7 @@ pub fn collect_lt_lookups_from_logs( /// /// The LT table sends: /// - MSB16 lookups (×2 per row: for lhs_msb and rhs_msb) -/// - IS_HALFWORD lookups (×4 per row: for lhs_sub_rhs range checks) +/// - IS_HALFWORD lookups (×6 per row: ×4 for lhs_sub_rhs, ×1 for lhs[1], ×1 for rhs[1]) pub fn collect_bitwise_lookups_from_lt(lt_ops: &[LtOperation]) -> Vec<(BitwiseLookup, u8, u8, u8)> { let mut lookups = Vec::new(); @@ -219,6 +219,24 @@ pub fn collect_bitwise_lookups_from_lt(lt_ops: &[LtOperation]) -> Vec<(BitwiseLo 0, )); } + + // IS_HALFWORD for lhs[1] (bits 32-47 of lhs) + let lhs_1 = ((op.lhs >> 32) & 0xFFFF) as u16; + lookups.push(( + BitwiseLookup::IsHalf, + (lhs_1 & 0xFF) as u8, + ((lhs_1 >> 8) & 0xFF) as u8, + 0, + )); + + // IS_HALFWORD for rhs[1] (bits 32-47 of rhs) + let rhs_1 = ((op.rhs >> 32) & 0xFFFF) as u16; + lookups.push(( + BitwiseLookup::IsHalf, + (rhs_1 & 0xFF) as u8, + ((rhs_1 >> 8) & 0xFF) as u8, + 0, + )); } lookups diff --git a/prover/src/tests/lt_tests.rs b/prover/src/tests/lt_tests.rs index b3d4784e4..859b2808f 100644 --- a/prover/src/tests/lt_tests.rs +++ b/prover/src/tests/lt_tests.rs @@ -162,6 +162,6 @@ fn test_multiplicity_different_signed_flags() { #[test] fn test_bus_interactions_count() { let interactions = bus_interactions(); - // MSB16 x2 + IS_HALFWORD x4 + LT x1 = 7 interactions - assert_eq!(interactions.len(), 7); + // MSB16 x2 + IS_HALFWORD x6 (lhs_sub_rhs x4 + lhs[1] + rhs[1]) + LT x1 = 9 interactions + assert_eq!(interactions.len(), 9); }