diff --git a/prover/src/tables/bitwise.rs b/prover/src/tables/bitwise.rs index 4b1e99d09..6466e09bc 100644 --- a/prover/src/tables/bitwise.rs +++ b/prover/src/tables/bitwise.rs @@ -31,7 +31,7 @@ use std::sync::OnceLock; use math::fft::cpu::bit_reversing::in_place_bit_reverse_permute; use math::polynomial::Polynomial; use stark::config::{BatchedMerkleTree, Commitment}; -use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::proof::options::ProofOptions; use stark::prover::evaluate_polynomial_on_lde_domain; use stark::trace::{TraceTable, columns2rows}; @@ -546,9 +546,9 @@ impl BitwiseOperation { /// in the spec corresponds to receiving lookups from other tables). pub fn bus_interactions() -> Vec { vec![ - // AND_BYTE[X, Y] -> AND + // BITWISE_BYTE[X, Y, AND, op_type=0] -> AND (merged bus, op_type discriminant) BusInteraction::receiver( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU_AND), vec![ BusValue::Packed { @@ -563,11 +563,12 @@ pub fn bus_interactions() -> Vec { start_column: cols::AND, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], ), - // OR_BYTE[X, Y] -> OR + // BITWISE_BYTE[X, Y, OR, op_type=1] BusInteraction::receiver( - BusId::OrByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU_OR), vec![ BusValue::Packed { @@ -582,11 +583,12 @@ pub fn bus_interactions() -> Vec { start_column: cols::OR, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(1)]), ], ), - // XOR_BYTE[X, Y] -> XOR + // BITWISE_BYTE[X, Y, XOR, op_type=2] BusInteraction::receiver( - BusId::XorByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU_XOR), vec![ BusValue::Packed { @@ -601,6 +603,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::XOR, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(2)]), ], ), // MSB8[X] -> MSB8 diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index 19db00ea0..ce7f17948 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -244,10 +244,10 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), - // AND_BYTE[next_pc_low[0]; unmasked_low_byte, 254] + // BITWISE_BYTE[unmasked_low_byte, 254, next_pc_low[0], op_type=0(AND)] // Verifies: next_pc_low[0] = unmasked_low_byte & 0xFE BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU), vec![ BusValue::Packed { @@ -259,6 +259,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::NEXT_PC_LOW_0, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], ), // IS_HALFWORD[next_pc_high[0]] diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index e29ae1d57..e0d1bf199 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -42,7 +42,7 @@ //! - STORE ADD: for STORE (res = arg1 + imm, separate from main ADD) //! - SUB: for SUB, BEQ operations //! - LT: for SLT, BLT operations -//! - AND_BYTE, OR_BYTE, XOR_BYTE: for bitwise operations (×8 each) +//! - BITWISE_BYTE: for bitwise operations (×8, merged AND/OR/XOR with op_type discriminant) //! - SHIFT: for shift operations //! - MUL: for multiplication //! - DIVREM: for division/remainder @@ -941,7 +941,7 @@ fn linear_term(bit: u32, column: usize) -> LinearTerm { /// /// The CPU table sends to: /// - DECODE: instruction fetch (every row) -/// - AND_BYTE, OR_BYTE, XOR_BYTE: for bitwise operations (×8 each) +/// - BITWISE_BYTE: for bitwise operations (×8, merged AND/OR/XOR with op_type discriminant) /// /// Note: LT interaction is TODO - needs proper DWordHHW packing to match LT table receiver. pub fn bus_interactions() -> Vec { @@ -1024,60 +1024,16 @@ pub fn bus_interactions() -> Vec { // )); // ------------------------------------------------------------------------- - // AND_BYTE interactions (×8 for each byte) + // BITWISE_BYTE interactions (×8, merged AND/OR/XOR) // ------------------------------------------------------------------------- + // AND, OR, XOR are mutually exclusive per CPU cycle (enforced by DECODE). + // Merged into a single bus with op_type discriminant: + // op_type = 0*AND + 1*OR + 2*XOR + // multiplicity = AND + OR + XOR (at most 1) for i in 0..8 { interactions.push(BusInteraction::sender( - BusId::AndByte, - Multiplicity::Column(cols::AND), - vec![ - BusValue::Packed { - start_column: cols::ARG1[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::ARG2[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::RES[i], - packing: Packing::Direct, - }, - ], - )); - } - - // ------------------------------------------------------------------------- - // OR_BYTE interactions (×8) - // ------------------------------------------------------------------------- - for i in 0..8 { - interactions.push(BusInteraction::sender( - BusId::OrByte, - Multiplicity::Column(cols::OR), - vec![ - BusValue::Packed { - start_column: cols::ARG1[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::ARG2[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::RES[i], - packing: Packing::Direct, - }, - ], - )); - } - - // ------------------------------------------------------------------------- - // XOR_BYTE interactions (×8) - // ------------------------------------------------------------------------- - for i in 0..8 { - interactions.push(BusInteraction::sender( - BusId::XorByte, - Multiplicity::Column(cols::XOR), + BusId::BitwiseByte, + Multiplicity::Sum3(cols::AND, cols::OR, cols::XOR), vec![ BusValue::Packed { start_column: cols::ARG1[i], @@ -1091,6 +1047,16 @@ pub fn bus_interactions() -> Vec { start_column: cols::RES[i], packing: Packing::Direct, }, + BusValue::Linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::OR, + }, + LinearTerm::Column { + coefficient: 2, + column: cols::XOR, + }, + ]), ], )); } diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index 9014799e5..d20745690 100644 --- a/prover/src/tables/shift.rs +++ b/prover/src/tables/shift.rs @@ -396,9 +396,9 @@ pub fn bus_interactions() -> Vec { ], )); - // SHIFT-C1: AND_BYTE[shift, 15] → bit_shift | left (= μ - direction) + // SHIFT-C1: BITWISE_BYTE[shift, 15, bit_shift, op_type=0(AND)] → bit_shift | left (= μ - direction) interactions.push(BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Diff(cols::MU, cols::DIRECTION), vec![ BusValue::Packed { @@ -410,16 +410,17 @@ pub fn bus_interactions() -> Vec { start_column: cols::BIT_SHIFT, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )); - // SHIFT-C2: AND_BYTE[256 - zbs * 16 - shift, 15] → bit_shift | right (= direction) + // SHIFT-C2: BITWISE_BYTE[256 - zbs * 16 - shift, 15, bit_shift, op_type=0(AND)] → bit_shift | right (= direction) // 256 - shift would overflow a byte when shift = 0. Subtracting zbs * 16 keeps it in // [0,255]. // When zbs = 1, shift is a multiple of 16 (i.e. shift ∈ [0, 240]), so // 256 - 16 - shift ∈ [0,255]. interactions.push(BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(cols::DIRECTION), vec![ BusValue::linear(vec![ @@ -438,6 +439,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::BIT_SHIFT, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )); @@ -519,11 +521,11 @@ pub fn bus_interactions() -> Vec { ], )); - // SHIFT-C11: AND_BYTE[encoded_limb; shift, mask] | μ + // SHIFT-C11: BITWISE_BYTE[encoded_limb; shift, mask, op_type=0(AND)] | μ // encoded = (1 - ls[0]) + 15*ls[1] + 31*ls[2] + 47*ls[3] // mask = 48 - 32 * word_instr interactions.push(BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU), vec![ // first input: shift @@ -558,6 +560,8 @@ pub fn bus_interactions() -> Vec { column: cols::LIMB_SHIFT_RAW_2, }, ]), + // op_type = 0 (AND) + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )); diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index fcedf869a..820fa6b89 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -53,12 +53,9 @@ pub enum BusId { // ========================================================================= // Bitwise operations (BITWISE table provides) // ========================================================================= - /// Bitwise AND of two bytes: AND_BYTE[X, Y] -> X & Y - AndByte, - /// Bitwise OR of two bytes: OR_BYTE[X, Y] -> X | Y - OrByte, - /// Bitwise XOR of two bytes: XOR_BYTE[X, Y] -> X ^ Y - XorByte, + /// Merged bitwise bus: BITWISE_BYTE[X, Y, result, op_type] where + /// op_type = 0 (AND), 1 (OR), 2 (XOR) + BitwiseByte, /// Most significant bit of a byte: MSB8[X] -> (X >> 7) & 1 Msb8, /// Most significant bit of a halfword: MSB16[X] -> (X >> 15) & 1 @@ -118,9 +115,7 @@ impl BusId { BusId::IsByte => "IsByte", BusId::IsHalfword => "IsHalfword", BusId::IsB20 => "IsB20", - BusId::AndByte => "AndByte", - BusId::OrByte => "OrByte", - BusId::XorByte => "XorByte", + BusId::BitwiseByte => "BitwiseByte", BusId::Msb8 => "Msb8", BusId::Msb16 => "Msb16", BusId::Zero => "Zero", @@ -149,25 +144,23 @@ impl TryFrom for BusId { 0 => Ok(BusId::IsByte), 1 => Ok(BusId::IsHalfword), 2 => Ok(BusId::IsB20), - 3 => Ok(BusId::AndByte), - 4 => Ok(BusId::OrByte), - 5 => Ok(BusId::XorByte), - 6 => Ok(BusId::Msb8), - 7 => Ok(BusId::Msb16), - 8 => Ok(BusId::Zero), - 9 => Ok(BusId::Hwsl), - 10 => Ok(BusId::Lt), - 11 => Ok(BusId::Mul), - 12 => Ok(BusId::Dvrm), - 13 => Ok(BusId::Shift), - 14 => Ok(BusId::Memw), - 15 => Ok(BusId::Load), - 16 => Ok(BusId::Memory), - 17 => Ok(BusId::Branch), - 18 => Ok(BusId::Decode), - 19 => Ok(BusId::Ecall), - 20 => Ok(BusId::CommitNextByte), - 21 => Ok(BusId::Commit), + 3 => Ok(BusId::BitwiseByte), + 4 => Ok(BusId::Msb8), + 5 => Ok(BusId::Msb16), + 6 => Ok(BusId::Zero), + 7 => Ok(BusId::Hwsl), + 8 => Ok(BusId::Lt), + 9 => Ok(BusId::Mul), + 10 => Ok(BusId::Dvrm), + 11 => Ok(BusId::Shift), + 12 => Ok(BusId::Memw), + 13 => Ok(BusId::Load), + 14 => Ok(BusId::Memory), + 15 => Ok(BusId::Branch), + 16 => Ok(BusId::Decode), + 17 => Ok(BusId::Ecall), + 18 => Ok(BusId::CommitNextByte), + 19 => Ok(BusId::Commit), other => Err(other), } } diff --git a/prover/src/tests/bitwise_bus_tests.rs b/prover/src/tests/bitwise_bus_tests.rs index 317b22362..63531d52d 100644 --- a/prover/src/tests/bitwise_bus_tests.rs +++ b/prover/src/tests/bitwise_bus_tests.rs @@ -11,7 +11,7 @@ use math::field::element::FieldElement; use stark::constraints::transition::TransitionConstraintEvaluator; use stark::lookup::{ - AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, Multiplicity, + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, LinearTerm, Multiplicity, NullBoundaryConstraintBuilder, Packing, }; use stark::proof::options::ProofOptions; @@ -59,7 +59,7 @@ fn new_sender_air( let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: vec![BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(sender_cols::AND), vec![ BusValue::Packed { @@ -74,6 +74,7 @@ fn new_sender_air( start_column: sender_cols::AND_RESULT, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )], }; @@ -94,7 +95,7 @@ fn new_receiver_air( let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: vec![BusInteraction::receiver( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(receiver_cols::MU_AND), vec![ BusValue::Packed { @@ -109,6 +110,7 @@ fn new_receiver_air( start_column: receiver_cols::AND, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )], }; diff --git a/prover/src/tests/bitwise_tests.rs b/prover/src/tests/bitwise_tests.rs index 823813ca1..d212852e7 100644 --- a/prover/src/tests/bitwise_tests.rs +++ b/prover/src/tests/bitwise_tests.rs @@ -381,7 +381,7 @@ mod soundness_tests { use crypto::fiat_shamir::default_transcript::DefaultTranscript; use stark::constraints::transition::TransitionConstraintEvaluator; use stark::lookup::{ - AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, Multiplicity, + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, LinearTerm, Multiplicity, NullBoundaryConstraintBuilder, Packing, }; use stark::proof::options::ProofOptions; @@ -421,7 +421,7 @@ mod soundness_tests { let transition_constraints: Vec>> = vec![]; let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: vec![BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(sender_cols::FLAG), vec![ BusValue::Packed { @@ -436,6 +436,7 @@ mod soundness_tests { start_column: sender_cols::AND_RESULT, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )], }; @@ -472,7 +473,7 @@ mod soundness_tests { let transition_constraints: Vec>> = vec![]; let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: vec![BusInteraction::receiver( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(receiver_cols::MU_AND), vec![ BusValue::Packed { @@ -487,6 +488,7 @@ mod soundness_tests { start_column: receiver_cols::AND, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )], }; diff --git a/prover/src/tests/cpu_tests.rs b/prover/src/tests/cpu_tests.rs index d2c240293..a07ffafbe 100644 --- a/prover/src/tests/cpu_tests.rs +++ b/prover/src/tests/cpu_tests.rs @@ -310,9 +310,7 @@ fn test_bus_interactions_count() { let interactions = bus_interactions(); // Expected interactions: - // - 8 AND_BYTE - // - 8 OR_BYTE - // - 8 XOR_BYTE + // - 8 BITWISE_BYTE (merged AND/OR/XOR per byte, with op_type selector) // - 2 MSB16 (rv1_sign_bit, arg2_sign_bit) // - 1 MSB8 (res_sign_bit) // - 1 ZERO (is_equal for BEQ) @@ -330,8 +328,8 @@ fn test_bus_interactions_count() { // - 1 BRANCH (branch/jump target calculation) // - 1 ECALL (single shared bus for HALT and COMMIT, mult = ECALL) // - 27 IS_BYTE (byte range checks: RS1, RS2, RD, ARG1[0..7], ARG2[0..7], RES[0..7]) - // Total: 8 + 8 + 8 + 2 + 1 + 1 + 1 + 1 + 5 + 1 + 1 + 1 + 1 + 1 + 1 + 27 = 68 - assert_eq!(interactions.len(), 68); + // Total: 8 + 2 + 1 + 1 + 1 + 1 + 5 + 1 + 1 + 1 + 1 + 1 + 1 + 27 = 52 + assert_eq!(interactions.len(), 52); } #[test] diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index e51568279..f4df3f019 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1004,7 +1004,7 @@ fn test_debug_memory_bus_tokens() { let z: i128 = 1000; let alpha: i128 = 2; - let bus_id: i128 = 17; // BusId::Memory + let bus_id: i128 = 14; // BusId::Memory // Compute fingerprint for a token let fingerprint =