refactor(prover): align byte range-checks with ARE_BYTES spec

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<X>` 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<X>`).
+    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<BusInteraction> {
                 },
             ],
         ),
-        // 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<X>`) 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,

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<next_pc_low[1]>`)
 //! - 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<BusInteraction> {
     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 {

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<super::bitwise::BitwiseOperation> {
         use super::bitwise::{BitwiseOperation, BitwiseOperationType};
 
@@ -515,24 +515,24 @@ 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] {
             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,
+                    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<BusInteraction> {
 
     // -------------------------------------------------------------------------
     // 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<BusInteraction> {
         ],
     ));
     interactions.push(BusInteraction::sender(
-        BusId::IsByte,
+        BusId::AreBytes,
         Multiplicity::One,
         vec![
             BusValue::Packed {
@@ -2030,7 +2030,7 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
     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 {

prover/src/tables/keccak.rs

@@ -366,21 +366,28 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         ],
     ));
 
-    // 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::IsByte,
+            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,
+                },
+            ],
         ));
     }
 

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,17 +637,26 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
         }
     }
 
-    // --- Theta: IS_BYTE range checks on Cxz_left (40) ---
+    // --- Theta: ARE_BYTES range checks on Cxz_left (20 pairs) ---
+    // Spec emits 40 `IS_BYTE<Cxz_left[x][z]>` 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::IsByte,
+                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<BusInteraction> {
         }
     }
 
-    // --- Rho: IS_BYTE 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::IsByte,
+                    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::IsByte,
-                    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,
+                        },
+                    ],
                 ));
             }
         }
@@ -902,7 +911,7 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
 /// - 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,

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<BusInteraction> {
     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]