Add IsByte range checks and state_addr binding

  to keccak precompile, restore Commit syscall to
  64

Author: jotabulacios

executor/programs/asm/test_commit_4.s

@@ -2,7 +2,7 @@
 	.globl	main
 main:
 	# Store 4 bytes [0xAA, 0xBB, 0xCC, 0xDD] on the stack, then commit them.
-	# Commit syscall: x17=3, x10=1(fd), x11=buf_addr, x12=count
+	# Commit syscall: x17=64, x10=1(fd), x11=buf_addr, x12=count
 
 	addi	sp, sp, -16		# 1: allocate stack
 	addi	t0, zero, 0xAA		# 2: t0 = 0xAA (170)
@@ -18,7 +18,7 @@ main:
 	li	a0, 1			# 10: fd = 1 (stdout)
 	mv	a1, sp			# 11: buf_addr = sp
 	li	a2, 4			# 12: count = 4
-	li	a7, 3			# 13: syscall = Commit
+	li	a7, 64			# 13: syscall = Commit
 	ecall				# 14: commit
 
 	# Halt

executor/src/vm/instruction/execution.rs

@@ -10,8 +10,8 @@ const REGULAR_PC_UPDATE: u64 = 4;
 pub enum SyscallNumbers {
     Print = 1,
     Panic = 2,
-    Commit = 3,
     GetPrivateInputs = 4,
+    Commit = 64,
     Halt = 93,
     KeccakPermute = 94, // Actual syscall number is KECCAK_SYSCALL_NUMBER (u64::MAX - 1)
 }
@@ -27,8 +27,8 @@ impl TryFrom<u64> for SyscallNumbers {
         match value {
             1 => Ok(SyscallNumbers::Print),
             2 => Ok(SyscallNumbers::Panic),
-            3 => Ok(SyscallNumbers::Commit),
             4 => Ok(SyscallNumbers::GetPrivateInputs),
+            64 => Ok(SyscallNumbers::Commit),
             93 => Ok(SyscallNumbers::Halt),
             v if v == KECCAK_SYSCALL_NUMBER => Ok(SyscallNumbers::KeccakPermute),
             _ => Err(()),

prover/src/tables/commit.rs

@@ -267,7 +267,7 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
     vec![
         // 1. Receive ECALL from CPU (mult = first)
         // Payload: [timestamp_lo, timestamp_hi, syscall_lo32, syscall_hi32]
-        // Hardcoded syscall number = 3 (Commit). Bus matching enforces CPU's rv1 == 3.
+        // Hardcoded syscall number = 64 (Commit). Bus matching enforces CPU's rv1 == 64.
         BusInteraction::receiver(
             BusId::EcallCommit,
             Multiplicity::Column(cols::FIRST),
@@ -280,8 +280,8 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
                     start_column: cols::TIMESTAMP_1,
                     packing: Packing::Direct,
                 },
-                BusValue::constant(3), // syscall number lo32 = Commit (3)
-                BusValue::constant(0), // syscall number hi32 = 0
+                BusValue::constant(64), // syscall number lo32 = Commit (64)
+                BusValue::constant(0),  // syscall number hi32 = 0
             ],
         ),
         // 2. Send to CommitNextByte (mult = mu - end)

prover/src/tables/cpu.rs

@@ -237,8 +237,14 @@ pub mod cols {
     /// branch_cond: Whether branch is taken
     pub const BRANCH_COND: usize = 75;
 
+    /// Keccak state address (DWordWL: lo32 and hi32).
+    /// Non-zero only for KeccakPermute ECALLs. Carried in the EcallKeccak bus
+    /// to directly bind the CPU's ECALL to the keccak chip's memory region.
+    pub const KECCAK_STATE_ADDR_0: usize = 76;
+    pub const KECCAK_STATE_ADDR_1: usize = 77;
+
     /// Total number of columns
-    pub const NUM_COLUMNS: usize = 76;
+    pub const NUM_COLUMNS: usize = 78;
 
     // -------------------------------------------------------------------------
     // Helper ranges for iteration
@@ -816,6 +822,10 @@ pub fn generate_cpu_trace(
         data[base + cols::ECALL] = FE::from(d.op_ecall as u64);
         data[base + cols::ECALL_COMMIT] = FE::from(op.ecall_commit as u64);
         data[base + cols::ECALL_KECCAK] = FE::from(op.ecall_keccak as u64);
+        data[base + cols::KECCAK_STATE_ADDR_0] =
+            FE::from(op.keccak_state_addr & 0xFFFF_FFFF);
+        data[base + cols::KECCAK_STATE_ADDR_1] =
+            FE::from(op.keccak_state_addr >> 32);
         data[base + cols::EBREAK] = FE::from(d.op_ebreak as u64);
 
         // Output columns
@@ -2087,7 +2097,11 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
     // -------------------------------------------------------------------------
     // Sends to the KECCAK table only for KeccakPermute ECALLs.
     // Payload matches the KECCAK receiver:
-    // [timestamp_lo, timestamp_hi, syscall_lo32, syscall_hi32]
+    // [timestamp_lo, timestamp_hi, syscall_lo32, syscall_hi32, state_addr_lo32, state_addr_hi32]
+    //
+    // Including state_addr directly binds the CPU's keccak ECALL to the keccak
+    // chip's memory region, rather than relying solely on transitive enforcement
+    // through the MEMW bus chain.
     interactions.push(BusInteraction::sender(
         BusId::EcallKeccak,
         Multiplicity::Column(cols::ECALL_KECCAK),
@@ -2111,6 +2125,14 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
                 start_column: cols::RV1_2,
                 packing: Packing::Direct,
             },
+            BusValue::Packed {
+                start_column: cols::KECCAK_STATE_ADDR_0,
+                packing: Packing::Direct,
+            },
+            BusValue::Packed {
+                start_column: cols::KECCAK_STATE_ADDR_1,
+                packing: Packing::Direct,
+            },
         ],
     ));
 

prover/src/tables/keccak.rs

@@ -1,6 +1,6 @@
 //! Keccak-f[1600] permutation chip.
 //!
-//! A single wide table (2,638 columns) that proves Keccak-f[1600] permutations.
+//! A single wide table (3,139 columns) that proves Keccak-f[1600] permutations.
 //! Each permutation uses 24 rows (one per round). All intermediate values are
 //! stored as columns and verified via purely polynomial constraints — no lookups.
 //!
@@ -961,11 +961,17 @@ pub fn create_constraints(
 /// - `EcallKeccak` receiver on the first row of each real permutation.
 /// - 25 `Memw` reads on `first`, binding the preimage to memory at `timestamp`.
 /// - 25 `Memw` writes on `export`, binding the final state to memory at `timestamp + 1`.
+/// - `IsByte` range checks on preimage bytes (on `first`) and output bytes (on `export`).
 pub fn bus_interactions() -> Vec<BusInteraction> {
-    let mut interactions = Vec::with_capacity(51);
+    // 1 EcallKeccak + 25 Memw reads + 25 Memw writes + 200 IsByte preimage + 200 IsByte output
+    let mut interactions = Vec::with_capacity(451);
     let syscall_lo = KECCAK_SYSCALL_NUMBER & 0xFFFF_FFFF;
     let syscall_hi = KECCAK_SYSCALL_NUMBER >> 32;
 
+    // EcallKeccak receiver: binds (timestamp, syscall_number, state_addr) from the CPU.
+    // Including state_addr provides a direct binding between the CPU's ECALL and the
+    // keccak permutation's memory region, rather than relying solely on transitive
+    // enforcement through the MEMW bus.
     interactions.push(BusInteraction::receiver(
         BusId::EcallKeccak,
         Multiplicity::Column(cols::FIRST),
@@ -980,9 +986,49 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
             },
             BusValue::constant(syscall_lo),
             BusValue::constant(syscall_hi),
+            BusValue::Packed {
+                start_column: cols::STATE_ADDR_0,
+                packing: Packing::Direct,
+            },
+            BusValue::Packed {
+                start_column: cols::STATE_ADDR_1,
+                packing: Packing::Direct,
+            },
         ],
     ));
 
+    // -------------------------------------------------------------------------
+    // IsByte range checks — defense in depth
+    // -------------------------------------------------------------------------
+    // Byte columns are already transitively range-checked through the MEMW bus
+    // (MEMW table enforces IsByte on its VALUE columns). These explicit checks
+    // ensure keccak byte columns remain sound even if MEMW range checks are
+    // refactored in the future.
+
+    // Preimage bytes: range-checked on `first` (where they enter the MEMW bus)
+    for i in 0..200 {
+        interactions.push(BusInteraction::sender(
+            BusId::IsByte,
+            Multiplicity::Column(cols::FIRST),
+            vec![BusValue::Packed {
+                start_column: cols::PREIMAGE_BYTES + i,
+                packing: Packing::Direct,
+            }],
+        ));
+    }
+
+    // Output bytes: range-checked on `export` (where they enter the MEMW bus)
+    for i in 0..200 {
+        interactions.push(BusInteraction::sender(
+            BusId::IsByte,
+            Multiplicity::Column(cols::EXPORT),
+            vec![BusValue::Packed {
+                start_column: cols::OUTPUT_BYTES + i,
+                packing: Packing::Direct,
+            }],
+        ));
+    }
+
     for lane_idx in 0..25 {
         let x = lane_idx % 5;
         let y = lane_idx / 5;

prover/src/tables/trace_builder.rs

@@ -1418,6 +1418,38 @@ fn expand_keccak_operations(cpu_ops: &[CpuOperation], elf: &Elf) -> Vec<KeccakOp
     expand_keccak_operations_from_state(cpu_ops, &initial_memory_state)
 }
 
+/// Collect IsByte lookups for keccak preimage and output bytes.
+///
+/// The keccak AIR sends IsByte for each of the 200 preimage bytes (on `first`)
+/// and 200 output bytes (on `export`). The bitwise table must account for these
+/// in its MU_IS_BYTE multiplicity column.
+fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec<BitwiseOperation> {
+    let mut ops = Vec::with_capacity(keccak_ops.len() * 400);
+    for op in keccak_ops {
+        // 200 preimage bytes (25 lanes × 8 bytes)
+        for lane in &op.input {
+            for byte_idx in 0..8u32 {
+                let byte_val = (lane >> (byte_idx * 8)) & 0xFF;
+                ops.push(BitwiseOperation::single_byte(
+                    BitwiseOperationType::IsByte,
+                    byte_val as u8,
+                ));
+            }
+        }
+        // 200 output bytes (25 lanes × 8 bytes)
+        for lane in &op.output {
+            for byte_idx in 0..8u32 {
+                let byte_val = (lane >> (byte_idx * 8)) & 0xFF;
+                ops.push(BitwiseOperation::single_byte(
+                    BitwiseOperationType::IsByte,
+                    byte_val as u8,
+                ));
+            }
+        }
+    }
+    ops
+}
+
 /// Collect bitwise lookups from COMMIT operations.
 ///
 /// The COMMIT table sends:
@@ -1867,6 +1899,8 @@ impl Traces {
 
         // Expand Keccak ECALL operations
         let keccak_ops = expand_keccak_operations(&cpu_ops, elf);
+        // KECCAK table sends IsByte for preimage and output bytes
+        bitwise_ops.extend(collect_bitwise_from_keccak(&keccak_ops));
 
         // CPU padding rows send IS_BYTE with all-zero values.
         // Add corresponding ops so the bitwise table multiplicities balance.
@@ -2089,6 +2123,10 @@ impl Traces {
         // COMMIT table sends IsByte and IsHalfword lookups
         bitwise_ops.extend(collect_bitwise_from_commit(&commit_ops));
 
+        // KECCAK table sends IsByte for preimage and output bytes
+        let keccak_ops = expand_keccak_operations_from_state(&cpu_ops, &MemoryState::new());
+        bitwise_ops.extend(collect_bitwise_from_keccak(&keccak_ops));
+
         // CPU padding rows send IS_BYTE with all-zero values.
         let num_padding_rows: usize = cpu_ops
             .chunks(max_rows.cpu)
@@ -2136,7 +2174,6 @@ impl Traces {
         let register_final_state = register_state.to_final_state_map();
 
         let commit_trace = commit::generate_commit_trace(&commit_ops);
-        let keccak_ops = expand_keccak_operations_from_state(&cpu_ops, &MemoryState::new());
         let keccak_trace = keccak::generate_keccak_trace(&keccak_ops);
 
         // Generate remaining traces in parallel (register, halt).

prover/src/tests/cpu_tests.rs

@@ -330,15 +330,15 @@ fn test_bus_interactions_count() {
     // - 1 BRANCH (branch/jump target calculation)
     // - 1 ECALL → HALT (send to HALT table, mult = ECALL - ECALL_COMMIT)
     // - 1 ECALL → COMMIT (send to COMMIT table, mult = ECALL_COMMIT)
+    // - 1 ECALL → KECCAK (send to KECCAK table, mult = ECALL_KECCAK)
     // - 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 + 1 + 27 = 69
-    // Note: ECALL → KECCAK interaction not yet implemented (pending MEMW bus integration)
-    assert_eq!(interactions.len(), 69);
+    // Total: 8 + 8 + 8 + 2 + 1 + 1 + 1 + 1 + 5 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 27 = 70
+    assert_eq!(interactions.len(), 70);
 }
 
 #[test]
 fn test_column_count() {
-    assert_eq!(cols::NUM_COLUMNS, 76);
+    assert_eq!(cols::NUM_COLUMNS, 78);
 }
 
 #[test]

syscalls/src/syscalls.rs

@@ -9,8 +9,8 @@ const MAX_PRIVATE_INPUT_SIZE: usize = 6700000;
 enum SyscallNumbers {
     Print = 1,
     Panic = 2,
-    Commit = 3,
     GetPrivateInputs = 4,
+    Commit = 64,
     Halt = 93,
 }