diff --git a/prover/src/tables/bitwise.rs b/prover/src/tables/bitwise.rs index b5a0e21f1..4b1e99d09 100644 --- a/prover/src/tables/bitwise.rs +++ b/prover/src/tables/bitwise.rs @@ -16,8 +16,7 @@ //! - `ZERO[X]` -> whether X is zero //! //! ## Shift Helpers -//! - `HWSL[X, Z]` -> (X << Z) mod 2^16 -//! - `HWSLC[X, Z]` -> X >> (16 - Z) +//! - `HWSL[X, Z]` -> [(X << Z) mod 2^16, X >> (16 - Z)] //! //! ## Table Structure //! @@ -93,11 +92,9 @@ pub mod cols { pub const MU_IS_B20: usize = 19; /// Multiplicity for HWSL lookups pub const MU_HWSL: usize = 20; - /// Multiplicity for HWSLC lookups - pub const MU_HWSLC: usize = 21; /// Total number of columns - pub const NUM_COLUMNS: usize = 22; + pub const NUM_COLUMNS: usize = 21; } /// Number of rows in the BITWISE table: 256 * 256 * 16 = 2^20 @@ -385,7 +382,6 @@ pub fn update_multiplicities( BitwiseOperationType::IsHalf => cols::MU_IS_HALF, BitwiseOperationType::IsB20 => cols::MU_IS_B20, BitwiseOperationType::Hwsl => cols::MU_HWSL, - BitwiseOperationType::Hwslc => cols::MU_HWSLC, }; // Increment multiplicity @@ -422,7 +418,7 @@ pub(crate) fn trim_zero_rows( .filter(|&row| { let row_data = trace.main_table.get_row(row); // Check all multiplicity columns (indices 11-21) - (cols::MU_AND..=cols::MU_HWSLC).any(|col| row_data[col] != FE::zero()) + (cols::MU_AND..=cols::MU_HWSL).any(|col| row_data[col] != FE::zero()) }) .collect(); @@ -463,7 +459,6 @@ pub enum BitwiseOperationType { IsHalf, IsB20, Hwsl, - Hwslc, } /// A lookup request to the BITWISE precomputed table. @@ -475,14 +470,14 @@ pub enum BitwiseOperationType { /// - `lookup_type`: Which operation result to look up /// - `x`: Byte input (0-255) /// - `y`: Byte input (0-255) -/// - `z`: 4-bit value (0-15), shift amount for HWSL/HWSLC +/// - `z`: 4-bit value (0-15), shift amount for HWSL /// /// # How inputs map to operations /// - AND/OR/XOR: `x OP y` /// - MSB8: MSB of `x` /// - MSB16: MSB of halfword `x + y * 256` /// - IS_BYTE/IS_HALF: Range check on `x + y * 256` -/// - HWSL/HWSLC: Shift `x + y * 256` by `z` bits +/// - HWSL: Shift `x + y * 256` by `z` bits, returning [SLL, SLLC] as a pair #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct BitwiseOperation { pub lookup_type: BitwiseOperationType, @@ -528,7 +523,7 @@ impl BitwiseOperation { Self::new(BitwiseOperationType::Zero, x, y, z) } - /// Create an operation for shift ops (HWSL, HWSLC). + /// Create an operation for HWSL shift lookups. pub fn shift_op(lookup_type: BitwiseOperationType, x: u8, y: u8, z: u8) -> Self { Self::new(lookup_type, x, y, z) } @@ -715,7 +710,7 @@ pub fn bus_interactions() -> Vec { }, ])], ), - // HWSL[X + 256*Y, Z] -> SLL + // HWSL[X + 256*Y, Z] -> [SLL, SLLC] BusInteraction::receiver( BusId::Hwsl, Multiplicity::Column(cols::MU_HWSL), @@ -738,27 +733,6 @@ pub fn bus_interactions() -> Vec { start_column: cols::SLL, packing: Packing::Direct, }, - ], - ), - // HWSLC[X + 256*Y, Z] -> SLLC - BusInteraction::receiver( - BusId::Hwslc, - Multiplicity::Column(cols::MU_HWSLC), - vec![ - BusValue::linear(vec![ - stark::lookup::LinearTerm::Column { - coefficient: 1, - column: cols::X, - }, - stark::lookup::LinearTerm::Column { - coefficient: 256, - column: cols::Y, - }, - ]), - BusValue::Packed { - start_column: cols::Z, - packing: Packing::Direct, - }, BusValue::Packed { start_column: cols::SLLC, packing: Packing::Direct, diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index bf11b862f..49b28c211 100644 --- a/prover/src/tables/shift.rs +++ b/prover/src/tables/shift.rs @@ -3,17 +3,18 @@ //! Constrains: `out = in <>/>>> (shift mod (32 * (2 - word_instr)))`. //! //! Two-phase design: -//! 1. Intra-limb shift by `bit_shift = shift mod 16` using HWSL/HWSLC lookups. +//! 1. Intra-limb shift by `bit_shift = shift mod 16` using paired HWSL lookups (returning [SLL, SLLC]). //! 2. Full-limb shift by `limb_shift` (unary encoding of `shift >> 4`). //! -//! ## Columns (27 total) +//! ## Columns (26 total) //! - Input: `in[0..3]` (DWordHL), `shift` (Byte), `direction` (Bit), `signed` (Bit), `word_instr` (Bit) //! - Output: `out[0..1]` (DWordWL) -//! - Auxiliary: `is_negative`, `bit_shift`, `zbs`, `X[0..4]`, `Y[0..3]`, `limb_shift[0..3]` +//! - Auxiliary: `is_negative`, `bit_shift`, `zbs`, `X[0..4]`, `Y[0..3]`, `limb_shift_raw[0..2]` +//! - Virtual: `limb_shift[3] = 1 - limb_shift_raw[0] - limb_shift_raw[1] - limb_shift_raw[2]` //! - Multiplicity: `μ` //! -//! ## Bus Interactions (15 total) -//! - Senders: MSB16, AND_BYTE (×3), ZERO, HWSL (×5), HWSLC (×4) +//! ## Bus Interactions (11 total) +//! - Senders: MSB16, AND_BYTE (×3), ZERO, HWSL (×5) //! - Receiver: SHIFT (from CPU) use math::field::element::FieldElement; @@ -65,22 +66,22 @@ pub mod cols { pub const Y_2: usize = 20; pub const Y_3: usize = 21; - // limb_shift[0..3]: one-hot encoding of full-limb shift amount - pub const LIMB_SHIFT_0: usize = 22; - pub const LIMB_SHIFT_1: usize = 23; - pub const LIMB_SHIFT_2: usize = 24; - pub const LIMB_SHIFT_3: usize = 25; + // limb_shift_raw[0..2]: first 3 values of the one-hot limb_shift encoding. + // limb_shift[3] is virtual: 1 - limb_shift_raw[0] - limb_shift_raw[1] - limb_shift_raw[2] + pub const LIMB_SHIFT_RAW_0: usize = 22; + pub const LIMB_SHIFT_RAW_1: usize = 23; + pub const LIMB_SHIFT_RAW_2: usize = 24; // Multiplicity - pub const MU: usize = 26; + pub const MU: usize = 25; - pub const NUM_COLUMNS: usize = 27; + pub const NUM_COLUMNS: usize = 26; // Helpers for iteration pub const IN: [usize; 4] = [IN_0, IN_1, IN_2, IN_3]; pub const X: [usize; 5] = [X_0, X_1, X_2, X_3, X_4]; pub const Y: [usize; 4] = [Y_0, Y_1, Y_2, Y_3]; - pub const LIMB_SHIFT: [usize; 4] = [LIMB_SHIFT_0, LIMB_SHIFT_1, LIMB_SHIFT_2, LIMB_SHIFT_3]; + pub const LIMB_SHIFT_RAW: [usize; 3] = [LIMB_SHIFT_RAW_0, LIMB_SHIFT_RAW_1, LIMB_SHIFT_RAW_2]; } // ========================================================================= @@ -127,7 +128,8 @@ impl ShiftOperation { } } - /// Compute HWSLC: halfword >> (16 - z) + /// Compute the carry output of HWSL: halfword >> (16 - z) + /// This is the second element of the HWSL pair [SLL, SLLC]. fn hwslc(halfword: u16, z: u8) -> u16 { if z == 0 { 0 @@ -344,9 +346,10 @@ pub fn generate_shift_trace( for i in 0..4 { data[base + cols::Y[i]] = FE::from(aux.y[i] as u64); } - for i in 0..4 { - data[base + cols::LIMB_SHIFT[i]] = FE::from(aux.limb_shift[i] as u64); + for i in 0..3 { + data[base + cols::LIMB_SHIFT_RAW[i]] = FE::from(aux.limb_shift[i] as u64); } + // limb_shift[3] is virtual: not stored in the trace // μ = 1 for all active rows (Bit) data[base + cols::MU] = FE::one(); @@ -369,7 +372,7 @@ pub fn generate_shift_trace( /// Creates all bus interactions for the SHIFT table. pub fn bus_interactions() -> Vec { - let mut interactions = Vec::with_capacity(15); + let mut interactions = Vec::with_capacity(11); // SHIFT-C14: MSB16[in[3]] → is_negative | signed interactions.push(BusInteraction::sender( @@ -460,8 +463,8 @@ pub fn bus_interactions() -> Vec { ], )); - // SHIFT-C4.i: HWSL[in[i], bit_shift] → X[i] for i∈[0,3] | 1 - zbs - // HWSL receiver: [x + 256*y (halfword), z (shift amount), SLL (result)] + // SHIFT-C4.i: HWSL[in[i], bit_shift] → [X[i], Y[i]] for i∈[0,3] | 1 - zbs + // HWSL receiver: [x + 256*y (halfword), z (shift amount), SLL, SLLC] let one_minus_zbs = Multiplicity::Linear(vec![ LinearTerm::Constant(1), LinearTerm::Column { @@ -486,12 +489,17 @@ pub fn bus_interactions() -> Vec { start_column: cols::X[i], packing: Packing::Direct, }, + BusValue::Packed { + start_column: cols::Y[i], + packing: Packing::Direct, + }, ], )); } - // SHIFT-C6: HWSL[extension, bit_shift] → X[4] | 1 - zbs + // SHIFT-C7: HWSL[extension, bit_shift] → [X[4], extension - X[4]] | 1 - zbs // extension = 65535 * is_negative (virtual) + // second output = extension - X[4] (the carry, expressed as a linear combination) interactions.push(BusInteraction::sender( BusId::Hwsl, one_minus_zbs.clone(), @@ -508,30 +516,18 @@ pub fn bus_interactions() -> Vec { start_column: cols::X_4, packing: Packing::Direct, }, - ], - )); - - // SHIFT-C8.i: HWSLC[in[i], bit_shift] → Y[i] for i∈[0,3] | 1 - zbs - for i in 0..4 { - interactions.push(BusInteraction::sender( - BusId::Hwslc, - one_minus_zbs.clone(), - vec![ - BusValue::Packed { - start_column: cols::IN[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::BIT_SHIFT, - packing: Packing::Direct, + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 65535, + column: cols::IS_NEGATIVE, }, - BusValue::Packed { - start_column: cols::Y[i], - packing: Packing::Direct, + LinearTerm::Column { + coefficient: -1, + column: cols::X_4, }, - ], - )); - } + ]), + ], + )); // SHIFT-C11: AND_BYTE[encoded_limb; shift, mask] | μ // encoded = (1 - ls[0]) + 15*ls[1] + 31*ls[2] + 47*ls[3] @@ -554,23 +550,22 @@ pub fn bus_interactions() -> Vec { }, ]), // result: encoded limb_shift + // = (1 - ls[0]) + 15*ls[1] + 31*ls[2] + 47*ls[3] + // substituting ls[3] = 1 - ls_raw[0] - ls_raw[1] - ls_raw[2]: + // = 48 - 48*ls_raw[0] - 32*ls_raw[1] - 16*ls_raw[2] BusValue::linear(vec![ - LinearTerm::Constant(1), - LinearTerm::Column { - coefficient: -1, - column: cols::LIMB_SHIFT_0, - }, + LinearTerm::Constant(48), LinearTerm::Column { - coefficient: 15, - column: cols::LIMB_SHIFT_1, + coefficient: -48, + column: cols::LIMB_SHIFT_RAW_0, }, LinearTerm::Column { - coefficient: 31, - column: cols::LIMB_SHIFT_2, + coefficient: -32, + column: cols::LIMB_SHIFT_RAW_1, }, LinearTerm::Column { - coefficient: 47, - column: cols::LIMB_SHIFT_3, + coefficient: -16, + column: cols::LIMB_SHIFT_RAW_2, }, ]), ], @@ -669,9 +664,17 @@ impl ShiftConstraint { // Get X, Y, limb_shift, in columns let get_x = |i: usize| step.get_main_evaluation_element(0, cols::X[i]).clone(); let get_y = |i: usize| step.get_main_evaluation_element(0, cols::Y[i]).clone(); - let get_ls = |i: usize| { - step.get_main_evaluation_element(0, cols::LIMB_SHIFT[i]) - .clone() + let get_ls = |i: usize| -> FieldElement { + if i < 3 { + step.get_main_evaluation_element(0, cols::LIMB_SHIFT_RAW[i]) + .clone() + } else { + // limb_shift[3] is virtual: 1 - ls_raw[0] - ls_raw[1] - ls_raw[2] + FieldElement::::one() + - step.get_main_evaluation_element(0, cols::LIMB_SHIFT_RAW[0]) + - step.get_main_evaluation_element(0, cols::LIMB_SHIFT_RAW[1]) + - step.get_main_evaluation_element(0, cols::LIMB_SHIFT_RAW[2]) + } }; // intra_limb_left[i]: X[0] for i=0, X[i]+Y[i-1] for i>0 @@ -757,9 +760,16 @@ impl ShiftConstraint { } ShiftConstraintKind::LimbShiftIsBit(i) => { // limb_shift[i] * (1 - limb_shift[i]) = 0 - let ls = step - .get_main_evaluation_element(0, cols::LIMB_SHIFT[i]) - .clone(); + // limb_shift[3] is virtual: 1 - ls_raw[0] - ls_raw[1] - ls_raw[2] + let ls = if i < 3 { + step.get_main_evaluation_element(0, cols::LIMB_SHIFT_RAW[i]) + .clone() + } else { + one.clone() + - step.get_main_evaluation_element(0, cols::LIMB_SHIFT_RAW[0]) + - step.get_main_evaluation_element(0, cols::LIMB_SHIFT_RAW[1]) + - step.get_main_evaluation_element(0, cols::LIMB_SHIFT_RAW[2]) + }; &ls * (&one - &ls) } ShiftConstraintKind::OutputMatchesShifted(i) => { @@ -866,7 +876,7 @@ 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/HWSLC/AND_BYTE/MSB16/ZERO +/// Each unique operation (with its multiplicity) generates HWSL/AND_BYTE/MSB16/ZERO /// lookups. The lookups must be generated per-unique-operation (matching the SHIFT table's /// deduplication and μ column), and repeated `multiplicity` times. pub fn collect_bitwise_from_shift(operations: &[ShiftOperation]) -> Vec { @@ -912,7 +922,9 @@ pub fn collect_bitwise_from_shift(operations: &[ShiftOperation]) -> Vec Vec> 8) as u8; @@ -934,18 +946,6 @@ pub fn collect_bitwise_from_shift(operations: &[ShiftOperation]) -> Vec> 8) as u8; - bitwise_ops.push(BitwiseOperation::shift_op( - BitwiseOperationType::Hwslc, - x, - y, - aux.bit_shift, - )); - } } // C11: AND_BYTE[shift, mask] | μ (= 1) diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index bc9bd71e0..10567e943 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -69,10 +69,8 @@ pub enum BusId { // ========================================================================= // Shift helpers (BITWISE table provides) // ========================================================================= - /// Halfword shift left: HWSL[X, Z] -> (X << Z) & 0xFFFF + /// Halfword shift left: HWSL[X, Z] -> [(X << Z) & 0xFFFF, X >> (16 - Z)] Hwsl, - /// Halfword shift left carry: HWSLC[X, Z] -> X >> (16 - Z) - Hwslc, // ========================================================================= // Arithmetic operations (separate tables) @@ -126,7 +124,6 @@ impl BusId { BusId::Msb16 => "Msb16", BusId::Zero => "Zero", BusId::Hwsl => "Hwsl", - BusId::Hwslc => "Hwslc", BusId::Lt => "Lt", BusId::Mul => "Mul", BusId::Shift => "Shift", @@ -158,9 +155,9 @@ impl TryFrom for BusId { 7 => Ok(BusId::Msb16), 8 => Ok(BusId::Zero), 9 => Ok(BusId::Hwsl), - 10 => Ok(BusId::Hwslc), - 11 => Ok(BusId::Lt), - 12 => Ok(BusId::Mul), + 10 => Ok(BusId::Lt), + 11 => Ok(BusId::Mul), + 12 => Ok(BusId::Dvrm), 13 => Ok(BusId::Shift), 14 => Ok(BusId::Memw), 15 => Ok(BusId::Load), diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 113b0ce2b..c5f730559 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -380,7 +380,7 @@ pub fn generate_minimal_bitwise_trace(ops: &[BitwiseOperation]) -> TraceTable = HashMap::new(); + let mut row_data: HashMap<(u8, u8, u8), [u64; 10]> = HashMap::new(); for op in ops { let key = (op.x, op.y, op.z); @@ -395,9 +395,8 @@ pub fn generate_minimal_bitwise_trace(ops: &[BitwiseOperation]) -> TraceTable 7, BitwiseOperationType::IsB20 => 8, BitwiseOperationType::Hwsl => 9, - BitwiseOperationType::Hwslc => 10, }; - row_data.entry(key).or_insert([0; 11])[mu_idx] += 1; + row_data.entry(key).or_insert([0; 10])[mu_idx] += 1; } // Need at least 4 rows for FRI, pad to power of 2 @@ -455,7 +454,6 @@ pub fn generate_minimal_bitwise_trace(ops: &[BitwiseOperation]) -> TraceTable