From d2fada9bf66960f9c30685d5a5809f82f921d8c1 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 26 Jan 2026 19:38:18 -0300 Subject: [PATCH 1/3] Simplify LT bus packing to 2 elements per operand --- prover/src/tables/cpu.rs | 101 +++++---------------------------------- prover/src/tables/lt.rs | 26 +++------- 2 files changed, 19 insertions(+), 108 deletions(-) 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..c14d0148d 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -278,35 +278,21 @@ pub fn bus_interactions() -> Vec { ), // 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, - }, - BusValue::Packed { - start_column: cols::LHS_1, - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::LHS_2, - packing: Packing::Direct, + packing: Packing::DWordHHW, }, - // 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 { From 30dbdc4b26087ed30db620e68d53a6704e7b5ed8 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 27 Jan 2026 14:55:56 -0300 Subject: [PATCH 2/3] Fix underconstrained table --- prover/src/tables/lt.rs | 22 +++++++++++++++++++++- prover/src/test_utils.rs | 20 +++++++++++++++++++- prover/src/tests/lt_tests.rs | 4 ++-- 3 files changed, 42 insertions(+), 4 deletions(-) diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index c14d0148d..5b7798def 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,6 +276,26 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), + // lt:c:range_lhs - IS_HALFWORD[lhs[1]] with multiplicity μ + // Soundness fix: Range check lhs[1] to ensure it's a valid halfword + BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(cols::MU), + vec![BusValue::Packed { + start_column: cols::LHS_1, + packing: Packing::Direct, + }], + ), + // lt:c:range_rhs - IS_HALFWORD[rhs[1]] with multiplicity μ + // Soundness fix: Range check rhs[1] to ensure it's a valid halfword + 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] diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 269419b0a..b336d893e 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) - soundness fix + 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) - soundness fix + 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); } From 0738d60c57101cea0471c52bc822eeb9909ee03b Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 27 Jan 2026 15:00:19 -0300 Subject: [PATCH 3/3] Fix comments --- prover/src/tables/lt.rs | 6 ++---- prover/src/test_utils.rs | 4 ++-- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index 5b7798def..40025c5bd 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -276,8 +276,7 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), - // lt:c:range_lhs - IS_HALFWORD[lhs[1]] with multiplicity μ - // Soundness fix: Range check lhs[1] to ensure it's a valid halfword + // IS_HALFWORD[lhs[1]] BusInteraction::sender( BusId::IsHalfword, Multiplicity::Column(cols::MU), @@ -286,8 +285,7 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), - // lt:c:range_rhs - IS_HALFWORD[rhs[1]] with multiplicity μ - // Soundness fix: Range check rhs[1] to ensure it's a valid halfword + // IS_HALFWORD[rhs[1]] BusInteraction::sender( BusId::IsHalfword, Multiplicity::Column(cols::MU), diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index b336d893e..2ed3fa937 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -220,7 +220,7 @@ pub fn collect_bitwise_lookups_from_lt(lt_ops: &[LtOperation]) -> Vec<(BitwiseLo )); } - // IS_HALFWORD for lhs[1] (bits 32-47 of lhs) - soundness fix + // IS_HALFWORD for lhs[1] (bits 32-47 of lhs) let lhs_1 = ((op.lhs >> 32) & 0xFFFF) as u16; lookups.push(( BitwiseLookup::IsHalf, @@ -229,7 +229,7 @@ pub fn collect_bitwise_lookups_from_lt(lt_ops: &[LtOperation]) -> Vec<(BitwiseLo 0, )); - // IS_HALFWORD for rhs[1] (bits 32-47 of rhs) - soundness fix + // IS_HALFWORD for rhs[1] (bits 32-47 of rhs) let rhs_1 = ((op.rhs >> 32) & 0xFFFF) as u16; lookups.push(( BitwiseLookup::IsHalf,