From a1973bbd65d88ee07de90b8132cb142de8b9adb2 Mon Sep 17 00:00:00 2001 From: Joaquin Carletti Date: Thu, 21 May 2026 12:32:58 -0300 Subject: [PATCH 1/3] add are_bytes --- prover/src/tables/bitwise.rs | 25 ++++---- prover/src/tables/branch.rs | 8 +-- prover/src/tables/cpu.rs | 36 ++++++------ prover/src/tables/keccak.rs | 2 +- prover/src/tables/keccak_rnd.rs | 14 ++--- prover/src/tables/page.rs | 10 ++-- prover/src/tables/trace_builder.rs | 86 ++++++++++++++-------------- prover/src/tables/types.rs | 10 ++-- prover/src/test_utils.rs | 6 +- prover/src/tests/cpu_tests.rs | 6 +- prover/src/tests/prove_elfs_tests.rs | 36 ++++++------ 11 files changed, 120 insertions(+), 119 deletions(-) diff --git a/prover/src/tables/bitwise.rs b/prover/src/tables/bitwise.rs index 455f696f2..a4d821e8b 100644 --- a/prover/src/tables/bitwise.rs +++ b/prover/src/tables/bitwise.rs @@ -3,7 +3,8 @@ //! This table provides 10 different lookup types used by other tables: //! //! ## Range Checks -//! - `IS_BYTE[X, Y]` - X and Y are valid bytes [0, 256) +//! - `ARE_BYTES[X, Y]` - X and Y are valid bytes [0, 256). Spec template +//! `IS_BYTE` is implemented by sending `ARE_BYTES[X, 0]`. //! - `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,9 +85,9 @@ pub mod cols { pub const MU_MSB16: usize = 15; /// Multiplicity for ZERO lookups pub const MU_ZERO: usize = 16; - /// 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 ARE_BYTES lookups. Each lookup checks X and Y; pass Y=0 + /// for a single-byte range check (spec template `IS_BYTE`). + pub const MU_ARE_BYTES: usize = 17; /// Multiplicity for IS_HALF lookups pub const MU_IS_HALF: usize = 18; /// Multiplicity for IS_B20 lookups @@ -378,7 +379,7 @@ pub fn update_multiplicities( BitwiseOperationType::Msb8 => cols::MU_MSB8, BitwiseOperationType::Msb16 => cols::MU_MSB16, BitwiseOperationType::Zero => cols::MU_ZERO, - BitwiseOperationType::IsByte => cols::MU_IS_BYTE, + BitwiseOperationType::AreBytes => cols::MU_ARE_BYTES, BitwiseOperationType::IsHalf => cols::MU_IS_HALF, BitwiseOperationType::IsB20 => cols::MU_IS_B20, BitwiseOperationType::Hwsl => cols::MU_HWSL, @@ -455,7 +456,7 @@ pub enum BitwiseOperationType { Msb8, Msb16, Zero, - IsByte, + AreBytes, IsHalf, IsB20, Hwsl, @@ -476,7 +477,7 @@ pub enum BitwiseOperationType { /// - AND/OR/XOR: `x OP y` /// - MSB8: MSB of `x` /// - MSB16: MSB of halfword `x + y * 256` -/// - IS_BYTE: Range check both `x` and `y`; use `y = 0` for a single byte +/// - ARE_BYTES: 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)] @@ -504,7 +505,7 @@ impl BitwiseOperation { Self::new(lookup_type, x, y, 0) } - /// Create an operation for single-byte ops (MSB8, IS_BYTE). + /// Create an operation for single-byte ops (MSB8, ARE_BYTES with y=0). pub fn single_byte(lookup_type: BitwiseOperationType, x: u8) -> Self { Self::new(lookup_type, x, 0, 0) } @@ -668,11 +669,11 @@ pub fn bus_interactions() -> Vec { }, ], ), - // IS_BYTE[X, Y] - range check two byte values, no output. - // Single-byte checks send the second argument as 0. + // ARE_BYTES[X, Y] - range check two byte values, no output. + // Single-byte checks (spec template `IS_BYTE`) send Y=0. BusInteraction::receiver( - BusId::IsByte, - Multiplicity::Column(cols::MU_IS_BYTE), + BusId::AreBytes, + Multiplicity::Column(cols::MU_ARE_BYTES), vec![ BusValue::Packed { start_column: cols::X, diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index d505ee60b..1a4cff20c 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -21,7 +21,7 @@ //! - `carry[0]`, `carry[1]`: Carries from 64-bit addition //! //! ## Bus Interactions -//! - Sender: IS_BYTE (×1 for next_pc_low[1]) +//! - Sender: ARE_BYTES (×1 for `[next_pc_low[1], 0]`, spec template `IS_BYTE`) //! - Sender: AND_BYTE (×1 for masking LSB) //! - Sender: IS_HALFWORD (×3 for next_pc_high[0..3]) //! - Receiver: BRANCH (provides branch targets to CPU) @@ -229,15 +229,15 @@ pub fn generate_branch_trace( /// Creates all bus interactions for the BRANCH table. /// /// The BRANCH table: -/// - **Sends** IS_BYTE lookup for next_pc_low[1] range check +/// - **Sends** ARE_BYTES lookup for next_pc_low[1] range check (Y=0) /// - **Sends** AND_BYTE lookup for LSB masking (next_pc_low[0] = unmasked_low_byte & 254) /// - **Sends** IS_HALFWORD lookups for next_pc_high[0..3] range checks /// - **Receives** BRANCH lookups from CPU table pub fn bus_interactions() -> Vec { vec![ - // IS_BYTE[next_pc_low[1], 0] - range check bits 8-15 + // ARE_BYTES[next_pc_low[1], 0] - range check bits 8-15 BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::Column(cols::MU), vec![ BusValue::Packed { diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 57f207d4d..86c82ce14 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, and arg1/arg2/res byte pairs +//! - ARE_BYTES: 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) @@ -501,9 +501,9 @@ impl CpuOperation { /// Collects CPU range-check lookups for register indices and byte pairs. /// /// 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 + /// - 1 ARE_BYTES lookup for (RS1, RS2) batched as a pair + /// - 1 ARE_BYTES lookup for RD encoded as (RD, 0) + /// - 12 ARE_BYTES lookups for adjacent byte pairs in ARG1, ARG2, and RES pub fn collect_byte_check_ops(&self) -> Vec { use super::bitwise::{BitwiseOperation, BitwiseOperationType}; @@ -515,16 +515,16 @@ impl CpuOperation { // Batch RS1+RS2 as a pair; RD stays single with Y=0. ops.push(BitwiseOperation::byte_op( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, self.decode.rs1, self.decode.rs2, )); ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, self.decode.rd, )); - // 12 IS_BYTE lookups for ARG1/ARG2/RES byte pairs + // 12 ARE_BYTES 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] { @@ -532,7 +532,7 @@ impl CpuOperation { let lo = ((value >> (i * 16)) & 0xFF) as u8; let hi = ((value >> (i * 16 + 8)) & 0xFF) as u8; ops.push(BitwiseOperation::byte_op( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, lo, hi, )); @@ -547,7 +547,7 @@ impl CpuOperation { use super::bitwise::{BitwiseOperation, BitwiseOperationType}; let mut lookups = Vec::new(); - // Range checks: 14 IS_BYTE ops (RS1+RS2 paired, RD single with Y=0, + // Range checks: 14 ARE_BYTES ops (RS1+RS2 paired, RD single with Y=0, // plus 12 ARG1/ARG2/RES byte pairs). lookups.extend(self.collect_byte_check_ops()); @@ -1991,19 +1991,19 @@ pub fn bus_interactions() -> Vec { // ------------------------------------------------------------------------- // 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) + // CPU-CR29: ARE_BYTES[rs1, rs2], CPU-CR30: ARE_BYTES[rd, 0] + // CPU-CR31.i: ARE_BYTES[arg1[2i], arg1[2i+1]] (i=0..3) + // CPU-CR32.i: ARE_BYTES[arg2[2i], arg2[2i+1]] (i=0..3) + // CPU-CR33.i: ARE_BYTES[res[2i], res[2i+1]] (i=0..3) // ------------------------------------------------------------------------- - // RS1 and RS2 share one IS_BYTE check; RD uses 0 as the second argument. + // RS1 and RS2 share one ARE_BYTES 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 + // batched into ARE_BYTES 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. interactions.push(BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::One, vec![ BusValue::Packed { @@ -2017,7 +2017,7 @@ pub fn bus_interactions() -> Vec { ], )); interactions.push(BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::One, vec![ BusValue::Packed { @@ -2030,7 +2030,7 @@ pub fn bus_interactions() -> Vec { for arr in [&cols::ARG1, &cols::ARG2, &cols::RES] { for i in 0..4 { interactions.push(BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::One, vec![ BusValue::Packed { diff --git a/prover/src/tables/keccak.rs b/prover/src/tables/keccak.rs index 87e8dc122..4b9603fa8 100644 --- a/prover/src/tables/keccak.rs +++ b/prover/src/tables/keccak.rs @@ -375,7 +375,7 @@ pub fn bus_interactions() -> Vec { // addr[1]=V_lo * 256^{-1} mod p), bypassing the alignment check. for b in 0..8 { interactions.push(BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::Column(cols::MU), vec![BusValue::Packed { start_column: cols::addr(b), diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index 277281583..c923589d9 100644 --- a/prover/src/tables/keccak_rnd.rs +++ b/prover/src/tables/keccak_rnd.rs @@ -1,7 +1,7 @@ //! KECCAK_RND: Round chip for Keccak-f[1600] permutation. //! //! One row per round (24 rows per keccak call). All bitwise operations are -//! delegated to BITWISE lookup tables (XOR_BYTE, AND_BYTE, HWSL, IS_BYTE). +//! delegated to BITWISE lookup tables (XOR_BYTE, AND_BYTE, HWSL, ARE_BYTES). //! //! ## Column layout (1,480 columns) //! @@ -637,12 +637,12 @@ pub fn bus_interactions() -> Vec { } } - // --- Theta: IS_BYTE range checks on Cxz_left (40) --- + // --- Theta: ARE_BYTES range checks on Cxz_left (40) --- // Cxz_right uses IS_BIT polynomial constraints (see create_constraints). for x in 0..5 { for b in 0..8 { interactions.push(BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::Column(cols::MU), vec![BusValue::Packed { start_column: cols::cxz_left(x, b), @@ -761,12 +761,12 @@ pub fn bus_interactions() -> Vec { } } - // --- Rho: IS_BYTE range checks on rot_left + rot_right (400) --- + // --- Rho: ARE_BYTES range checks on rot_left + rot_right (400) --- for x in 0..5 { for y in 0..5 { for b in 0..8 { interactions.push(BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::Column(cols::MU), vec![BusValue::Packed { start_column: cols::rot_left(x, y, b), @@ -774,7 +774,7 @@ pub fn bus_interactions() -> Vec { }], )); interactions.push(BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::Column(cols::MU), vec![BusValue::Packed { start_column: cols::rot_right(x, y, b), @@ -902,7 +902,7 @@ pub fn bus_interactions() -> Vec { /// - pi is a spec [[variables.virtual]] inlined in chi bus interactions. /// - rnc/rbc are spec [[variables.constant]] inlined as compile-time constants. /// -/// All other checks (XOR, AND, HWSL, IS_BYTE, IS_HALF, KECCAK, KECCAK_RC) are +/// All other checks (XOR, AND, HWSL, ARE_BYTES, IS_HALF, KECCAK, KECCAK_RC) are /// enforced via bus interactions against the BITWISE/KECCAK_RC chips. pub fn create_constraints( constraint_idx_start: usize, diff --git a/prover/src/tables/page.rs b/prover/src/tables/page.rs index a4597e1b8..475ab5279 100644 --- a/prover/src/tables/page.rs +++ b/prover/src/tables/page.rs @@ -26,7 +26,7 @@ //! //! | Tag | Bus | Signature | Multiplicity | //! |-----|-----|-----------|--------------| -//! | PAGE-C1+C2 | IS_BYTE | `[init, fini]` | 1 (sender) | +//! | PAGE-C1+C2 | ARE_BYTES | `[init, fini]` | 1 (sender) | //! | PAGE-C3 | Memory | `[0, address, 0, init]` | -1 (receiver) | //! | PAGE-C4 | Memory | `[0, address, timestamp, fini]` | 1 (sender) | @@ -317,7 +317,7 @@ pub fn precomputed_commitment_cached(config: &PageConfig, options: &ProofOptions /// /// ## Bus Interactions /// -/// - PAGE-C1+C2: IS_BYTE[init, fini] - sender, multiplicity 1 (batched range check) +/// - PAGE-C1+C2: ARE_BYTES[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 /// @@ -341,9 +341,9 @@ pub fn bus_interactions(page_base: u64) -> Vec { let address_hi = BusValue::constant(page_base_hi); vec![ - // PAGE-C1+C2: IS_BYTE[init, fini] - range check both byte values in one interaction + // PAGE-C1+C2: ARE_BYTES[init, fini] - range check both byte values in one interaction BusInteraction::sender( - BusId::IsByte, + BusId::AreBytes, Multiplicity::One, vec![ BusValue::Packed { @@ -527,7 +527,7 @@ mod tests { #[test] fn test_bus_interactions() { let interactions = bus_interactions(0x1000); // page_base - assert_eq!(interactions.len(), 3); // C1+C2 (batched IS_BYTE), C3, C4 + assert_eq!(interactions.len(), 3); // C1+C2 (batched ARE_BYTES), C3, C4 } #[test] diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index f83763280..280640934 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1367,7 +1367,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], 0] - range check for byte value + // ARE_BYTES[next_pc_low[1], 0] - range check for byte value bitwise_ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, next_pc_low_1, )); @@ -1426,14 +1426,14 @@ fn collect_bitwise_from_branch(branch_ops: &[BranchOperation]) -> Vec Vec { if num_padding_rows == 0 { return Vec::new(); @@ -1441,21 +1441,21 @@ fn collect_byte_check_ops_for_padding(num_padding_rows: usize) -> Vec Vec Vec { let mut lookups = Vec::new(); @@ -1667,7 +1667,7 @@ fn collect_bitwise_from_commit(commit_ops: &[CommitOperation]) -> Vec Vec> (b * 8)) & 0xFF) as u8; ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, byte, )); } @@ -1742,7 +1742,7 @@ fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec Vec> 8) & 0xFF) as u8, 1, )); - // IS_BYTE for cxz_left bytes + // ARE_BYTES for cxz_left bytes ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, (shifted & 0xFF) as u8, )); ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, ((shifted >> 8) & 0xFF) as u8, )); } @@ -1823,7 +1823,7 @@ fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec Vec> 8) & 0xFF) as u8, rnc_val, )); - // IS_BYTE for rot_left + // ARE_BYTES for rot_left ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, (shifted & 0xFF) as u8, )); ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, ((shifted >> 8) & 0xFF) as u8, )); - // IS_BYTE for rot_right + // ARE_BYTES for rot_right ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, (carry & 0xFF) as u8, )); ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::IsByte, + BitwiseOperationType::AreBytes, ((carry >> 8) & 0xFF) as u8, )); } @@ -2260,7 +2260,7 @@ fn build_traces( bitwise_ops.extend(collect_bitwise_from_memw_aligned(&memw_aligned_ops)); // MEMW_R sends IS_HALFWORD[timestamp_0 - old_timestamp_lo - 1] bitwise_ops.extend(collect_bitwise_from_memw_register(&memw_register_ops)); - // PAGE tables do a batched IS_BYTE[init, fini] lookup per row (C1+C2) + // PAGE tables do a batched ARE_BYTES[init, fini] lookup per row (C1+C2) if let Some(elf) = elf { bitwise_ops.extend(collect_bitwise_from_page(elf, memory_state, private_input)); } @@ -2270,12 +2270,12 @@ fn build_traces( .filter(|op| !op.end) .map(|op| op.value) .collect(); - // COMMIT table sends IsByte and IsHalfword lookups + // COMMIT table sends AreBytes and IsHalfword lookups bitwise_ops.extend(collect_bitwise_from_commit(&commit_ops)); - // KECCAK_RND sends XOR/AND/IS_BYTE/HWSL; KECCAK core sends IS_HALF + // KECCAK_RND sends XOR/AND/ARE_BYTES/HWSL; KECCAK core sends IS_HALF bitwise_ops.extend(collect_bitwise_from_keccak(&keccak_ops)); - // CPU padding rows send IS_BYTE with all-zero values. + // CPU padding rows send ARE_BYTES with all-zero values. // Add corresponding ops so the bitwise table multiplicities balance. let num_padding_rows: usize = cpu_ops .chunks(max_rows.cpu) @@ -3275,9 +3275,9 @@ mod keccak_tests { .iter() .filter(|o| o.lookup_type == BitwiseOperationType::AndByte) .count(); - let is_byte = ops + let are_bytes = ops .iter() - .filter(|o| o.lookup_type == BitwiseOperationType::IsByte) + .filter(|o| o.lookup_type == BitwiseOperationType::AreBytes) .count(); let hwsl = ops .iter() @@ -3290,9 +3290,9 @@ mod keccak_tests { assert_eq!(xor, 24 * 608, "XorByte count"); assert_eq!(and, 24 * 200 + 1, "AndByte count"); - // Cxz_right Byte→Bit (spec d75944ee): drops 40 IS_BYTE per round. + // Cxz_right Byte→Bit (spec d75944ee): drops 40 ARE_BYTES per round. // +8 per call to range-check the addr bytes used in alignment / no-overflow. - assert_eq!(is_byte, 24 * 440 + 8, "IsByte count"); + assert_eq!(are_bytes, 24 * 440 + 8, "AreBytes count"); assert_eq!(hwsl, 24 * 120, "Hwsl count"); assert_eq!(is_half, 100, "IsHalf count"); assert_eq!(ops.len(), 109 + 24 * 1368, "Total bitwise ops"); @@ -3396,13 +3396,13 @@ mod keccak_tests { assert_eq!( keccak::bus_interactions().len(), 138, - "KECCAK core: 1 ECALL + 1 MEMW read_addr + 25 MEMW lanes + 100 IS_HALF + 1 AND_BYTE alignment + 8 IS_BYTE addr + 1 Keccak send + 1 Keccak recv" + "KECCAK core: 1 ECALL + 1 MEMW read_addr + 25 MEMW lanes + 100 IS_HALF + 1 AND_BYTE alignment + 8 ARE_BYTES addr + 1 Keccak send + 1 Keccak recv" ); assert_eq!( keccak_rnd::bus_interactions().len(), 1371, "KECCAK_RND: 3 IO + 460 theta + 500 rho + 400 chi + 8 iota \ - (Cxz_right Byte→Bit drops 40 IS_BYTE per spec d75944ee)" + (Cxz_right Byte→Bit drops 40 ARE_BYTES per spec d75944ee)" ); assert_eq!( keccak_rc::bus_interactions().len(), diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index 70aa6813d..ceefbbc60 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -43,9 +43,9 @@ pub enum BusId { // ========================================================================= // Range checks (BITWISE table provides) // ========================================================================= - /// Range check: both values are valid bytes [0, 256). - /// Single-byte checks send the second value as 0. - IsByte = 0, + /// `ARE_BYTES[X, Y]`: range check that both X and Y are valid bytes [0, 256). + /// Single-byte checks (spec template `IS_BYTE`) send the second value as 0. + AreBytes = 0, /// Range check: value is a valid halfword [0, 2^16) IsHalfword, /// Range check: value is a 20-bit value [0, 2^20) @@ -120,7 +120,7 @@ impl BusId { /// Human-readable name for debug output. pub fn name(&self) -> &'static str { match self { - BusId::IsByte => "IsByte", + BusId::AreBytes => "AreBytes", BusId::IsHalfword => "IsHalfword", BusId::IsB20 => "IsB20", BusId::AndByte => "AndByte", @@ -153,7 +153,7 @@ impl TryFrom for BusId { fn try_from(value: u64) -> Result { match value { - 0 => Ok(BusId::IsByte), + 0 => Ok(BusId::AreBytes), 1 => Ok(BusId::IsHalfword), 2 => Ok(BusId::IsB20), 3 => Ok(BusId::AndByte), diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 83386a417..1b608034c 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -419,7 +419,7 @@ pub fn generate_minimal_bitwise_trace(ops: &[BitwiseOperation]) -> TraceTable 3, BitwiseOperationType::Msb16 => 4, BitwiseOperationType::Zero => 5, - BitwiseOperationType::IsByte => 6, + BitwiseOperationType::AreBytes => 6, BitwiseOperationType::IsHalf => 7, BitwiseOperationType::IsB20 => 8, BitwiseOperationType::Hwsl => 9, @@ -478,7 +478,7 @@ pub fn generate_minimal_bitwise_trace(ops: &[BitwiseOperation]) -> TraceTable VmAir { /// /// The PAGE table has no transition constraints (it's a pure lookup table). /// It interacts with: -/// - IS_BYTE bus: range checks for init/fini values +/// - ARE_BYTES bus: range checks for init/fini values /// - Memory bus: provides initial and final memory tokens pub fn create_page_air(proof_options: &ProofOptions, page_base: u64) -> VmAir { let transition_constraints: Vec>> = vec![]; diff --git a/prover/src/tests/cpu_tests.rs b/prover/src/tests/cpu_tests.rs index 9004d24c0..f05d1005c 100644 --- a/prover/src/tests/cpu_tests.rs +++ b/prover/src/tests/cpu_tests.rs @@ -329,9 +329,9 @@ fn test_bus_interactions_count() { // - 1 SHIFT (shift operations) // - 1 BRANCH (branch/jump target calculation) // - 1 ECALL (shared bus for HALT, COMMIT, and KECCAK, mult = ECALL) - // - 1 IS_BYTE for (RS1, RS2) paired - // - 1 IS_BYTE for (RD, 0) - // - 12 IS_BYTE (ARG1/ARG2/RES byte pairs: 4 pairs × 3 arrays) + // - 1 ARE_BYTES for (RS1, RS2) paired + // - 1 ARE_BYTES for (RD, 0) + // - 12 ARE_BYTES (ARG1/ARG2/RES byte pairs: 4 pairs × 3 arrays) // Inline PC replaces CM54: -1 CM54, +4 inline PC → net +3 vs pre-PR main. // Total: 8 + 8 + 8 + 2 + 1 + 1 + 1 + 1 + 5 + 4 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 12 = 58 assert_eq!(interactions.len(), 58); diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 53149a943..6219e766f 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -781,7 +781,7 @@ fn test_prove_elfs_keccak_multi_call() { /// Verifier REJECTS a forged trace where an addr byte cell is set to a /// non-byte field element. /// -/// Without the IS_BYTE range checks on addr(0..7), an attacker could keep +/// Without the ARE_BYTES range checks on addr(0..7), an attacker could keep /// `addr_lo = b0 + 256·b1 + 65536·b2 + 2^24·b3` equal to an unaligned target /// address as a field element while setting addr(0)=0 (passing the AndByte /// alignment check) and folding the carry into addr(1) as a non-byte @@ -802,8 +802,8 @@ fn test_prove_elfs_keccak_unaligned_state_addr() { Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); // Tamper the first real keccak row: replace addr(1) (a byte cell) with a - // value outside [0, 256). The new IS_BYTE bus sender will emit this - // value with multiplicity MU=1; the IS_BYTE preprocessed table only + // value outside [0, 256). The new ARE_BYTES bus sender will emit this + // value with multiplicity MU=1; the ARE_BYTES preprocessed table only // contains 0..256, so the bus cannot balance. traces.keccak.main_table.set( 0, @@ -1493,8 +1493,8 @@ fn test_debug_memory_tokens_sb_sh() { println!("Found {} imbalanced memory tokens", imbalanced); } - // === Count IS_BYTE lookups from PAGE (batched [init, fini] per row) === - println!("\n=== IS_BYTE Lookup Counts (from PAGE tables) ==="); + // === Count ARE_BYTES lookups from PAGE (batched [init, fini] per row) === + println!("\n=== ARE_BYTES Lookup Counts (from PAGE tables) ==="); let mut page_pair_counts: HashMap<(u8, u8), u64> = 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() { @@ -1505,46 +1505,46 @@ fn test_debug_memory_tokens_sb_sh() { *page_pair_counts.entry((init, fini)).or_insert(0) += 1; } } - let page_is_byte_total: u64 = page_pair_counts.values().sum(); + let page_are_bytes_total: u64 = page_pair_counts.values().sum(); println!( - "Total PAGE rows: {}, Expected IS_BYTE (1 per row): {}", + "Total PAGE rows: {}, Expected ARE_BYTES (1 per row): {}", total_page_rows, total_page_rows, ); println!( - "IS_BYTE[0, 0] from PAGE: {} lookups (most rows are (0,0))", + "ARE_BYTES[0, 0] from PAGE: {} lookups (most rows are (0,0))", page_pair_counts.get(&(0, 0)).copied().unwrap_or(0) ); - // BITWISE row for IS_BYTE[X, Y] at Z=0 is X + 256*Y. We only sum + // BITWISE row for ARE_BYTES[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 + // (e.g. CPU's paired ARE_BYTES checks) also bump this same MU_ARE_BYTES // 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_over_page_pairs: u64 = page_pair_counts + let bitwise_are_bytes_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(row, bitwise_cols::MU_IS_BYTE) + .get(row, bitwise_cols::MU_ARE_BYTES) .to_raw() }) .sum(); println!( - "Bitwise IS_BYTE mult summed over PAGE (init, fini) rows: {}", - bitwise_is_byte_mult_over_page_pairs + "Bitwise ARE_BYTES mult summed over PAGE (init, fini) rows: {}", + bitwise_are_bytes_mult_over_page_pairs ); println!( - "Total IS_BYTE lookups from PAGE (counted): {}", - page_is_byte_total + "Total ARE_BYTES lookups from PAGE (counted): {}", + page_are_bytes_total ); - // Note: this can be >= 0 because CPU byte-pair IS_BYTE senders may also + // Note: this can be >= 0 because CPU byte-pair ARE_BYTES senders may also // hit some of the same (init, fini) rows. It should never be negative. println!( "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 + bitwise_are_bytes_mult_over_page_pairs as i64 - page_are_bytes_total as i64 ); // === Verify PAGE AIR uses correct page_base === From 41bb3ad317b5ce31c22d5d82605a78c1009ab34d Mon Sep 17 00:00:00 2001 From: Joaquin Carletti Date: Thu, 21 May 2026 12:46:09 -0300 Subject: [PATCH 2/3] fix keccak --- prover/src/tables/keccak.rs | 31 ++++++++++------- prover/src/tables/keccak_rnd.rs | 47 +++++++++++++++----------- prover/src/tables/trace_builder.rs | 54 ++++++++++++++---------------- 3 files changed, 73 insertions(+), 59 deletions(-) diff --git a/prover/src/tables/keccak.rs b/prover/src/tables/keccak.rs index 4b9603fa8..4d5e72834 100644 --- a/prover/src/tables/keccak.rs +++ b/prover/src/tables/keccak.rs @@ -366,21 +366,28 @@ pub fn bus_interactions() -> Vec { ], )); - // 6. Range-check every addr byte. The addr columns are reconstructed as a - // linear combination (addr_lo = b0 + 256*b1 + 65536*b2 + 2^24*b3, etc.) - // for the MEMW lookup and the no-overflow / alignment constraints. Without - // an explicit byte range check on each cell, an attacker can keep the - // field-element value of that linear combination correct while encoding - // arbitrary non-byte values in the individual cells (e.g. addr[0]=0, - // addr[1]=V_lo * 256^{-1} mod p), bypassing the alignment check. - for b in 0..8 { + // 6. Range-check every addr byte (4 ARE_BYTES pairs). The addr columns are + // reconstructed as a linear combination (addr_lo = b0 + 256*b1 + 65536*b2 + + // 2^24*b3, etc.) for the MEMW lookup and the no-overflow / alignment + // constraints. Without an explicit byte range check on each cell, an + // attacker can keep the field-element value of that linear combination + // correct while encoding arbitrary non-byte values in the individual cells + // (e.g. addr[0]=0, addr[1]=V_lo * 256^{-1} mod p), bypassing the alignment + // check. Spec emits 8 IS_BYTE templates; we merge `(addr[2i], addr[2i+1])`. + for i in 0..4 { interactions.push(BusInteraction::sender( BusId::AreBytes, Multiplicity::Column(cols::MU), - vec![BusValue::Packed { - start_column: cols::addr(b), - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: cols::addr(2 * i), + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::addr(2 * i + 1), + packing: Packing::Direct, + }, + ], )); } diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index c923589d9..75e174463 100644 --- a/prover/src/tables/keccak_rnd.rs +++ b/prover/src/tables/keccak_rnd.rs @@ -637,17 +637,26 @@ pub fn bus_interactions() -> Vec { } } - // --- Theta: ARE_BYTES range checks on Cxz_left (40) --- + // --- Theta: ARE_BYTES range checks on Cxz_left (20 pairs) --- + // Spec emits 40 `IS_BYTE` templates; we merge adjacent + // byte pairs (z=2i, z=2i+1) into ARE_BYTES interactions per the + // implementation guidance in spec/is_byte.typ. // Cxz_right uses IS_BIT polynomial constraints (see create_constraints). for x in 0..5 { - for b in 0..8 { + for i in 0..4 { interactions.push(BusInteraction::sender( BusId::AreBytes, Multiplicity::Column(cols::MU), - vec![BusValue::Packed { - start_column: cols::cxz_left(x, b), - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: cols::cxz_left(x, 2 * i), + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::cxz_left(x, 2 * i + 1), + packing: Packing::Direct, + }, + ], )); } } @@ -761,25 +770,25 @@ pub fn bus_interactions() -> Vec { } } - // --- Rho: ARE_BYTES range checks on rot_left + rot_right (400) --- + // --- Rho: ARE_BYTES range checks on rot_left + rot_right (200 pairs) --- + // Spec emits 400 IS_BYTE templates (200 per side); we merge each + // (rot_left[x][y][b], rot_right[x][y][b]) into one ARE_BYTES interaction. for x in 0..5 { for y in 0..5 { for b in 0..8 { interactions.push(BusInteraction::sender( BusId::AreBytes, Multiplicity::Column(cols::MU), - vec![BusValue::Packed { - start_column: cols::rot_left(x, y, b), - packing: Packing::Direct, - }], - )); - interactions.push(BusInteraction::sender( - BusId::AreBytes, - Multiplicity::Column(cols::MU), - vec![BusValue::Packed { - start_column: cols::rot_right(x, y, b), - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: cols::rot_left(x, y, b), + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::rot_right(x, y, b), + packing: Packing::Direct, + }, + ], )); } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 280640934..a1c883b10 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1688,11 +1688,14 @@ fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec> (b * 8)) & 0xFF) as u8; - ops.push(BitwiseOperation::single_byte( + // 4 paired ops matching the (addr[2i], addr[2i+1]) sender pairing. + for i in 0..4 { + let lo = ((state_addr >> (2 * i * 8)) & 0xFF) as u8; + let hi = ((state_addr >> ((2 * i + 1) * 8)) & 0xFF) as u8; + ops.push(BitwiseOperation::byte_op( BitwiseOperationType::AreBytes, - byte, + lo, + hi, )); } @@ -1757,13 +1760,11 @@ fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec> 8) & 0xFF) as u8, 1, )); - // ARE_BYTES for cxz_left bytes - ops.push(BitwiseOperation::single_byte( + // ARE_BYTES for cxz_left bytes: paired (low, high) of the halfword, + // matching `(cxz_left[x][2i], cxz_left[x][2i+1])` sender pairing. + ops.push(BitwiseOperation::byte_op( BitwiseOperationType::AreBytes, (shifted & 0xFF) as u8, - )); - ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::AreBytes, ((shifted >> 8) & 0xFF) as u8, )); } @@ -1842,22 +1843,17 @@ fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec> 8) & 0xFF) as u8, rnc_val, )); - // ARE_BYTES for rot_left - ops.push(BitwiseOperation::single_byte( + // ARE_BYTES paired as (rot_left[b], rot_right[b]) for + // each byte of the halfword, matching the sender pairing + // in keccak_rnd::bus_interactions. + ops.push(BitwiseOperation::byte_op( BitwiseOperationType::AreBytes, (shifted & 0xFF) as u8, - )); - ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::AreBytes, - ((shifted >> 8) & 0xFF) as u8, - )); - // ARE_BYTES for rot_right - ops.push(BitwiseOperation::single_byte( - BitwiseOperationType::AreBytes, (carry & 0xFF) as u8, )); - ops.push(BitwiseOperation::single_byte( + ops.push(BitwiseOperation::byte_op( BitwiseOperationType::AreBytes, + ((shifted >> 8) & 0xFF) as u8, ((carry >> 8) & 0xFF) as u8, )); } @@ -3291,11 +3287,12 @@ mod keccak_tests { assert_eq!(xor, 24 * 608, "XorByte count"); assert_eq!(and, 24 * 200 + 1, "AndByte count"); // Cxz_right Byte→Bit (spec d75944ee): drops 40 ARE_BYTES per round. - // +8 per call to range-check the addr bytes used in alignment / no-overflow. - assert_eq!(are_bytes, 24 * 440 + 8, "AreBytes count"); + // Spec emits one IS_BYTE template per byte; ops pair adjacent bytes + // into ARE_BYTES (20 cxz_left + 200 rho per round, 4 addr per call). + assert_eq!(are_bytes, 24 * 220 + 4, "AreBytes count"); assert_eq!(hwsl, 24 * 120, "Hwsl count"); assert_eq!(is_half, 100, "IsHalf count"); - assert_eq!(ops.len(), 109 + 24 * 1368, "Total bitwise ops"); + assert_eq!(ops.len(), 105 + 24 * 1148, "Total bitwise ops"); } #[test] @@ -3395,14 +3392,15 @@ mod keccak_tests { fn test_keccak_bus_interaction_counts() { assert_eq!( keccak::bus_interactions().len(), - 138, - "KECCAK core: 1 ECALL + 1 MEMW read_addr + 25 MEMW lanes + 100 IS_HALF + 1 AND_BYTE alignment + 8 ARE_BYTES addr + 1 Keccak send + 1 Keccak recv" + 134, + "KECCAK core: 1 ECALL + 1 MEMW read_addr + 25 MEMW lanes + 100 IS_HALF + 1 AND_BYTE alignment + 4 ARE_BYTES addr pairs + 1 Keccak send + 1 Keccak recv" ); assert_eq!( keccak_rnd::bus_interactions().len(), - 1371, - "KECCAK_RND: 3 IO + 460 theta + 500 rho + 400 chi + 8 iota \ - (Cxz_right Byte→Bit drops 40 ARE_BYTES per spec d75944ee)" + 1151, + "KECCAK_RND: 3 IO + 440 theta + 300 rho + 400 chi + 8 iota \ + (Cxz_right Byte→Bit drops 40 ARE_BYTES per spec d75944ee; \ + ARE_BYTES sends are paired per spec ARE_BYTES interaction signature)" ); assert_eq!( keccak_rc::bus_interactions().len(), From 236534795faf62dfdb587a9a259cf67bb4207b7e Mon Sep 17 00:00:00 2001 From: diegokingston Date: Thu, 21 May 2026 15:23:37 -0300 Subject: [PATCH 3/3] docs: fix stale ARE_BYTES counts in keccak bitwise-op comments Addresses review feedback on PR #600: the two comments in `collect_bitwise_from_keccak` were renamed IS_BYTE -> ARE_BYTES but kept the pre-pairing counts. After pairing adjacent bytes into ARE_BYTES interactions the per-round counts halve: - theta: ARE_BYTES on Cxz_left is 20 pairs, not 40. - rho: ARE_BYTES is 200 pairs, not 400. These now match the `are_bytes = 24 * 220 + 4` test assertion (220/round = 20 theta + 200 rho). Comment-only; no behavior change. --- prover/src/tables/trace_builder.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index a1c883b10..5e787a700 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1745,7 +1745,7 @@ fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec Vec