Skip to content

Fix: Simplify LT bus packing to 2 elements per operand #240

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MauroToscano merged 3 commits into from
Jan 27, 2026
Merged

Fix: Simplify LT bus packing to 2 elements per operand #240

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d2fada9
Simplify LT bus packing to 2 elements per operand
MauroToscano Jan 26, 2026
30dbdc4
Fix underconstrained table
MauroToscano Jan 27, 2026
0738d60
Fix comments
MauroToscano Jan 27, 2026
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
101 changes: 13 additions & 88 deletions prover/src/tables/cpu.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1220,101 +1220,26 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
// -------------------------------------------------------------------------
// 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,
Expand Down
46 changes: 25 additions & 21 deletions prover/src/tables/lt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -276,37 +276,41 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
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 {
Expand Down
20 changes: 19 additions & 1 deletion prover/src/test_utils.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();

Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions prover/src/tests/lt_tests.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}