diff --git a/prover/src/tables/bitwise.rs b/prover/src/tables/bitwise.rs index 4b1e99d09..455f696f2 100644 --- a/prover/src/tables/bitwise.rs +++ b/prover/src/tables/bitwise.rs @@ -1,9 +1,9 @@ //! BITWISE precomputed lookup table. //! -//! This table provides 11 different lookup types used by other tables: +//! This table provides 10 different lookup types used by other tables: //! //! ## Range Checks -//! - `IS_BYTE[X]` - X is a valid byte [0, 256) +//! - `IS_BYTE[X, Y]` - X and Y are valid bytes [0, 256) //! - `IS_HALF[X]` - X is a valid halfword [0, 2^16) //! - `IS_B20[X]` - X is a valid 20-bit value [0, 2^20) //! @@ -84,7 +84,8 @@ pub mod cols { pub const MU_MSB16: usize = 15; /// Multiplicity for ZERO lookups pub const MU_ZERO: usize = 16; - /// Multiplicity for IS_BYTE lookups + /// Multiplicity for IS_BYTE lookups. Each lookup checks X and Y; pass Y=0 + /// for a single-byte range check. pub const MU_IS_BYTE: usize = 17; /// Multiplicity for IS_HALF lookups pub const MU_IS_HALF: usize = 18; @@ -92,7 +93,6 @@ pub mod cols { pub const MU_IS_B20: usize = 19; /// Multiplicity for HWSL lookups pub const MU_HWSL: usize = 20; - /// Total number of columns pub const NUM_COLUMNS: usize = 21; } @@ -417,7 +417,7 @@ pub(crate) fn trim_zero_rows( let kept_rows: Vec = (0..num_rows) .filter(|&row| { let row_data = trace.main_table.get_row(row); - // Check all multiplicity columns (indices 11-21) + // Check all multiplicity columns (indices 11-20) (cols::MU_AND..=cols::MU_HWSL).any(|col| row_data[col] != FE::zero()) }) .collect(); @@ -476,7 +476,8 @@ pub enum BitwiseOperationType { /// - 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` +/// - IS_BYTE: Range check both `x` and `y`; use `y = 0` for a single byte +/// - IS_HALF: Range check on `x + y * 256` /// - HWSL: Shift `x + y * 256` by `z` bits, returning [SLL, SLLC] as a pair #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct BitwiseOperation { @@ -667,14 +668,21 @@ pub fn bus_interactions() -> Vec { }, ], ), - // IS_BYTE[X] - range check, no output + // IS_BYTE[X, Y] - range check two byte values, no output. + // Single-byte checks send the second argument as 0. BusInteraction::receiver( BusId::IsByte, Multiplicity::Column(cols::MU_IS_BYTE), - vec![BusValue::Packed { - start_column: cols::X, - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: cols::X, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::Y, + packing: Packing::Direct, + }, + ], ), // IS_HALF[X + 256*Y] - range check for halfword BusInteraction::receiver( diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index 19db00ea0..d505ee60b 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -235,14 +235,17 @@ pub fn generate_branch_trace( /// - **Receives** BRANCH lookups from CPU table pub fn bus_interactions() -> Vec { vec![ - // IS_BYTE[next_pc_low[1]] - range check bits 8-15 + // IS_BYTE[next_pc_low[1], 0] - range check bits 8-15 BusInteraction::sender( BusId::IsByte, Multiplicity::Column(cols::MU), - vec![BusValue::Packed { - start_column: cols::NEXT_PC_LOW_1, - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: cols::NEXT_PC_LOW_1, + packing: Packing::Direct, + }, + BusValue::constant(0), + ], ), // AND_BYTE[next_pc_low[0]; unmasked_low_byte, 254] // Verifies: next_pc_low[0] = unmasked_low_byte & 0xFE diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index e29ae1d57..055742101 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -36,7 +36,7 @@ //! //! ### Senders (CPU sends to other tables) //! - DECODE: instruction fetch -//! - IS_BYTE: range checks for rs1, rs2, rd, arg1[i], arg2[i], res[i] +//! - IS_BYTE: range checks for rs1, rs2, rd, and arg1/arg2/res byte pairs //! - IS_BIT: range checks for flags (via templates) //! - ADD: for ADD, LOAD, JALR operations //! - STORE ADD: for STORE (res = arg1 + imm, separate from main ADD) @@ -484,10 +484,12 @@ impl CpuOperation { } } - /// Collects IS_BYTE lookups for CPU byte range checks. + /// Collects CPU range-check lookups for register indices and byte pairs. /// - /// The CPU has 27 byte columns that must be range-checked: RS1, RS2, RD, - /// ARG1[0..7], ARG2[0..7], RES[0..7]. Each generates one IS_BYTE lookup. + /// The CPU sends: + /// - 1 IS_BYTE lookup for (RS1, RS2) batched as a pair + /// - 1 IS_BYTE lookup for RD encoded as (RD, 0) + /// - 12 IS_BYTE lookups for adjacent byte pairs in ARG1, ARG2, and RES pub fn collect_byte_check_ops(&self) -> Vec { use super::bitwise::{BitwiseOperation, BitwiseOperationType}; @@ -495,15 +497,12 @@ impl CpuOperation { let arg2 = self.compute_arg2(); let res = self.compute_res(); - let mut ops = Vec::with_capacity(27); + let mut ops = Vec::with_capacity(14); - // Register indices - ops.push(BitwiseOperation::single_byte( + // Batch RS1+RS2 as a pair; RD stays single with Y=0. + ops.push(BitwiseOperation::byte_op( BitwiseOperationType::IsByte, self.decode.rs1, - )); - ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, self.decode.rs2, )); ops.push(BitwiseOperation::single_byte( @@ -511,24 +510,19 @@ impl CpuOperation { self.decode.rd, )); - // ARG1[0..7], ARG2[0..7], RES[0..7] - for i in 0..8 { - ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, - ((arg1 >> (i * 8)) & 0xFF) as u8, - )); - } - for i in 0..8 { - ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, - ((arg2 >> (i * 8)) & 0xFF) as u8, - )); - } - for i in 0..8 { - ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, - ((res >> (i * 8)) & 0xFF) as u8, - )); + // 12 IS_BYTE lookups for ARG1/ARG2/RES byte pairs + // Each pair sends [lo, hi] as two separate bus values, so the LogUp + // fingerprint forces each byte to match individually against BITWISE X, Y. + for value in [arg1, arg2, res] { + for i in 0..4 { + let lo = ((value >> (i * 16)) & 0xFF) as u8; + let hi = ((value >> (i * 16 + 8)) & 0xFF) as u8; + ops.push(BitwiseOperation::byte_op( + BitwiseOperationType::IsByte, + lo, + hi, + )); + } } ops @@ -539,7 +533,8 @@ impl CpuOperation { use super::bitwise::{BitwiseOperation, BitwiseOperationType}; let mut lookups = Vec::new(); - // Byte range checks: 27 IS_BYTE + // Range checks: 14 IS_BYTE ops (RS1+RS2 paired, RD single with Y=0, + // plus 12 ARG1/ARG2/RES byte pairs). lookups.extend(self.collect_byte_check_ops()); // MSB16 lookups for sign bit extraction (when word_instr=1) @@ -1949,50 +1944,60 @@ pub fn bus_interactions() -> Vec { )); // ------------------------------------------------------------------------- - // IS_BYTE interactions (byte range checks, 27 total) - // CPU-CR29: IS_BYTE[rs1], CPU-CR30: IS_BYTE[rs2], CPU-CR31: IS_BYTE[rd] - // CPU-CR32.i: IS_BYTE[arg1[i]], CPU-CR33.i: IS_BYTE[arg2[i]], CPU-CR34.i: IS_BYTE[res[i]] + // Range checks (14 total): + // CPU-CR29: IS_BYTE[rs1, rs2], CPU-CR30: IS_BYTE[rd, 0] + // CPU-CR31.i: IS_BYTE[arg1[2i], arg1[2i+1]] (i=0..3) + // CPU-CR32.i: IS_BYTE[arg2[2i], arg2[2i+1]] (i=0..3) + // CPU-CR33.i: IS_BYTE[res[2i], res[2i+1]] (i=0..3) // ------------------------------------------------------------------------- - // Range-check all 27 byte columns: RS1, RS2, RD, ARG1[0..7], ARG2[0..7], RES[0..7]. + // RS1 and RS2 share one IS_BYTE check; RD uses 0 as the second argument. + // ARG1/ARG2/RES are 8-byte little-endian values — adjacent byte pairs are + // batched into IS_BYTE checks. Each pair sends two separate bus values + // [lo, hi], so the LogUp fingerprint forces each byte to match individually + // against the BITWISE table's X in [0,255] and Y in [0,255]. // Every CPU row (including padding) sends with Multiplicity::One. - let byte_columns: [usize; 27] = [ - cols::RS1, - cols::RS2, - cols::RD, - cols::ARG1[0], - cols::ARG1[1], - cols::ARG1[2], - cols::ARG1[3], - cols::ARG1[4], - cols::ARG1[5], - cols::ARG1[6], - cols::ARG1[7], - cols::ARG2[0], - cols::ARG2[1], - cols::ARG2[2], - cols::ARG2[3], - cols::ARG2[4], - cols::ARG2[5], - cols::ARG2[6], - cols::ARG2[7], - cols::RES[0], - cols::RES[1], - cols::RES[2], - cols::RES[3], - cols::RES[4], - cols::RES[5], - cols::RES[6], - cols::RES[7], - ]; - for col in byte_columns { - interactions.push(BusInteraction::sender( - BusId::IsByte, - Multiplicity::One, - vec![BusValue::Packed { - start_column: col, + interactions.push(BusInteraction::sender( + BusId::IsByte, + Multiplicity::One, + vec![ + BusValue::Packed { + start_column: cols::RS1, packing: Packing::Direct, - }], - )); + }, + BusValue::Packed { + start_column: cols::RS2, + packing: Packing::Direct, + }, + ], + )); + interactions.push(BusInteraction::sender( + BusId::IsByte, + Multiplicity::One, + vec![ + BusValue::Packed { + start_column: cols::RD, + packing: Packing::Direct, + }, + BusValue::constant(0), + ], + )); + for arr in [&cols::ARG1, &cols::ARG2, &cols::RES] { + for i in 0..4 { + interactions.push(BusInteraction::sender( + BusId::IsByte, + Multiplicity::One, + vec![ + BusValue::Packed { + start_column: arr[2 * i], + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: arr[2 * i + 1], + packing: Packing::Direct, + }, + ], + )); + } } // ECALL interaction (single shared bus for HALT and COMMIT) diff --git a/prover/src/tables/page.rs b/prover/src/tables/page.rs index 8d3c9c6b9..872b8d553 100644 --- a/prover/src/tables/page.rs +++ b/prover/src/tables/page.rs @@ -26,10 +26,9 @@ //! //! | Tag | Bus | Signature | Multiplicity | //! |-----|-----|-----------|--------------| -//! | PAGE-C1 | IS_BYTE | `[init]` | 1 (sender) | -//! | PAGE-C2 | IS_BYTE | `[fini]` | 1 (sender) | -//! | PAGE-C3 | Memory | `[0, address, 0, init]` | -1 (receiver) | -//! | PAGE-C4 | Memory | `[0, address, timestamp, fini]` | 1 (sender) | +//! | PAGE-C1+C2 | IS_BYTE | `[init, fini]` | 1 (sender) | +//! | PAGE-C3 | Memory | `[0, address, 0, init]` | -1 (receiver) | +//! | PAGE-C4 | Memory | `[0, address, timestamp, fini]` | 1 (sender) | use std::collections::HashMap; use std::sync::OnceLock; @@ -297,8 +296,7 @@ pub fn precomputed_commitment_cached(config: &PageConfig, options: &ProofOptions /// /// ## Bus Interactions /// -/// - PAGE-C1: IS_BYTE[init] - sender, multiplicity 1 (range check) -/// - PAGE-C2: IS_BYTE[fini] - sender, multiplicity 1 (range check) +/// - PAGE-C1+C2: IS_BYTE[init, fini] - sender, multiplicity 1 (batched range check) /// - PAGE-C3: memory[0, address, 0, init] - receiver, multiplicity -1 /// - PAGE-C4: memory[0, address, timestamp, fini] - sender, multiplicity 1 /// @@ -322,25 +320,22 @@ pub fn bus_interactions(page_base: u64) -> Vec { let address_hi = BusValue::constant(page_base_hi); vec![ - // PAGE-C1: IS_BYTE[init] - range check initial value + // PAGE-C1+C2: IS_BYTE[init, fini] - range check both byte values in one interaction BusInteraction::sender( BusId::IsByte, Multiplicity::One, - vec![BusValue::Packed { - start_column: cols::INIT, - packing: Packing::Direct, - }], - ), - // PAGE-C2: IS_BYTE[fini] - range check final value - BusInteraction::sender( - BusId::IsByte, - Multiplicity::One, - vec![BusValue::Packed { - start_column: cols::FINI, - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: cols::INIT, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::FINI, + packing: Packing::Direct, + }, + ], ), - // PAGE-C3: memory[0, address, 0, init] - receive initial token + // PAGE-C3: memory[0, address, 0, init] - receive initial memory token BusInteraction::receiver( BusId::Memory, Multiplicity::One, @@ -511,7 +506,7 @@ mod tests { #[test] fn test_bus_interactions() { let interactions = bus_interactions(0x1000); // page_base - assert_eq!(interactions.len(), 4); // C1, C2, C3, C4 + assert_eq!(interactions.len(), 3); // C1+C2 (batched IS_BYTE), C3, C4 } #[test] @@ -519,6 +514,6 @@ mod tests { // Test with high address like stack region let stack_page = STACK_TOP & !(DEFAULT_PAGE_SIZE as u64 - 1); let interactions = bus_interactions(stack_page); - assert_eq!(interactions.len(), 4); + assert_eq!(interactions.len(), 3); } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index dd0e8c821..b1af698de 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1240,7 +1240,7 @@ fn collect_bitwise_from_dvrm(dvrm_ops: &[(DvrmOperation, bool)]) -> Vec Vec> 48) & 0xFFFF) as u16; let unmasked_low_byte = (next_pc_unmasked & 0xFF) as u8; - // IS_BYTE[next_pc_low[1]] - range check for byte value + // IS_BYTE[next_pc_low[1], 0] - range check for byte value bitwise_ops.push(BitwiseOperation::single_byte( BitwiseOperationType::IsByte, next_pc_low_1, @@ -1302,21 +1302,35 @@ fn collect_bitwise_from_branch(branch_ops: &[BranchOperation]) -> Vec Vec { if num_padding_rows == 0 { return Vec::new(); } - let mut ops = Vec::with_capacity(num_padding_rows * 27); + let mut ops = Vec::with_capacity(num_padding_rows * 14); for _ in 0..num_padding_rows { - for _ in 0..27 { - ops.push(BitwiseOperation::single_byte( + // IS_BYTE[RS1, RS2] pair (both zero in padding) + ops.push(BitwiseOperation::byte_op( + BitwiseOperationType::IsByte, + 0, + 0, + )); + // IS_BYTE[RD, 0] single (zero in padding) + ops.push(BitwiseOperation::single_byte( + BitwiseOperationType::IsByte, + 0, + )); + // 12 IS_BYTE lookups for ARG1/ARG2/RES byte pairs (all zero in padding) + for _ in 0..12 { + ops.push(BitwiseOperation::byte_op( BitwiseOperationType::IsByte, 0, + 0, )); } } @@ -1325,9 +1339,8 @@ fn collect_byte_check_ops_for_padding(num_padding_rows: usize) -> Vec Vec { @@ -1383,15 +1396,10 @@ fn collect_bitwise_from_page(elf: &Elf, memory_state: &MemoryState) -> Vec = HashMap::new(); let total_page_rows: usize = traces.pages.iter().map(|p| p.num_rows()).sum(); for (page_idx, page_trace) in traces.pages.iter().enumerate() { let page_size = traces.page_configs[page_idx].page_size; for row in 0..page_trace.num_rows().min(page_size) { - let init = page_trace.main_table.get(row, page_cols::INIT).to_raw() as usize; - let fini = page_trace.main_table.get(row, page_cols::FINI).to_raw() as usize; - is_byte_from_page[init] += 1; // C1 - is_byte_from_page[fini] += 1; // C2 + let init = page_trace.main_table.get(row, page_cols::INIT).to_raw() as u8; + let fini = page_trace.main_table.get(row, page_cols::FINI).to_raw() as u8; + *page_pair_counts.entry((init, fini)).or_insert(0) += 1; } } + let page_is_byte_total: u64 = page_pair_counts.values().sum(); println!( - "Total PAGE rows: {}, Expected IS_BYTE: {} (2 per row)", - total_page_rows, - total_page_rows * 2 + "Total PAGE rows: {}, Expected IS_BYTE (1 per row): {}", + total_page_rows, total_page_rows, ); println!( - "IS_BYTE[0]: {} lookups (most bytes are 0)", - is_byte_from_page[0] + "IS_BYTE[0, 0] from PAGE: {} lookups (most rows are (0,0))", + page_pair_counts.get(&(0, 0)).copied().unwrap_or(0) ); - // Check if bitwise table has matching multiplicities for IS_BYTE - // IS_BYTE uses rows 0..255 for each byte value, MU_IS_BYTE is column 17 + // BITWISE row for IS_BYTE[X, Y] at Z=0 is X + 256*Y. We only sum + // multiplicity at the (X, Y) pairs PAGE actually touches. Other senders + // (e.g. CPU's paired IS_BYTE checks) also bump this same MU_IS_BYTE + // column and may hit the same (X, Y) rows, so this is a coarse sanity + // check (BITWISE mult >= PAGE's contribution), not an exact balance. use crate::tables::bitwise::cols as bitwise_cols; - let bitwise_is_byte_mult: u64 = (0..256usize) - .map(|byte_val| { - // IS_BYTE lookup is at row with X=byte_val, Y=0, Z=0 - // Row index = X + Y*256 + Z*256*256 = X (for Y=0, Z=0) + let bitwise_is_byte_mult_over_page_pairs: u64 = page_pair_counts + .keys() + .map(|&(x, y)| { + let row = x as usize + 256 * y as usize; traces .bitwise .main_table - .get(byte_val, bitwise_cols::MU_IS_BYTE) + .get(row, bitwise_cols::MU_IS_BYTE) .to_raw() }) .sum(); println!( - "Bitwise IS_BYTE total multiplicity: {}", - bitwise_is_byte_mult + "Bitwise IS_BYTE mult summed over PAGE (init, fini) rows: {}", + bitwise_is_byte_mult_over_page_pairs ); - - // Also count total IS_BYTE lookups expected from collect_bitwise_from_page - let is_byte_total_from_page: u64 = is_byte_from_page.iter().sum(); println!( "Total IS_BYTE lookups from PAGE (counted): {}", - is_byte_total_from_page + page_is_byte_total ); + // Note: this can be >= 0 because CPU byte-pair IS_BYTE senders may also + // hit some of the same (init, fini) rows. It should never be negative. println!( - "Difference: {} (should be 0 if PAGE IS_BYTE matches Bitwise)", - bitwise_is_byte_mult as i64 - is_byte_total_from_page as i64 + "Difference: {} (>= 0 expected; PAGE pairs may also receive from CPU)", + bitwise_is_byte_mult_over_page_pairs as i64 - page_is_byte_total as i64 ); // === Verify PAGE AIR uses correct page_base ===