From fba6457339e73e355783c5e89ca969b7ee437e98 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 13:33:29 -0300 Subject: [PATCH 1/6] feat(executor): keccak sponge-absorb syscall (ECALL -4) New syscall keccak_absorb_blocks(state_ptr, data_ptr, n_blocks) at a7 = u64::MAX - 3 (spec ECALL -4). Per block k the executor XORs the 136-byte rate block into lanes 0..17 (little-endian dwords) and applies keccak-f[1600]; lanes 17..25 are untouched by the XOR. Padding stays guest-side: the chip only ever sees whole rate blocks. Rejections mirror the existing accelerator guards and are chosen so the prover chip's addressing model is total over accepted inputs: - both pointers 8-aligned, n_blocks > 0; - LAST byte of each region bounded against u64 overflow (checked_mul / checked_add) and against low-limb overflow ((addr % 2^32) + last_off < 2^32) - the chip models per-dword addresses as base_lo + offset with no carry into the high limb, like the ECSM operands (ecsm_addr_ok is generalized to accel_addr_low_limb_ok); - state/data regions disjoint: the trace builder issues the state read and every message read at the ecall timestamp, so an overlap would put two MEMW ops on one (address, timestamp) pair, which the memory argument cannot order (same rationale as EcsmOperandOverlap). The log carries state_addr/data_addr (src2/dst); n_blocks is recovered from x12 by the trace builder like the ECSM operand addresses. Tests: sponge differential vs tiny_keccak (n = 1, 2, 3, 5, 8, 13 with seeded pseudo-random state+data), a chained XOR+keccak_f1600 replay against the executor's own permutation, and one rejection test per guard including both boundary sides of the low-limb check. --- executor/src/tests/keccak_absorb_tests.rs | 212 ++++++++++++++++++++++ executor/src/tests/mod.rs | 1 + executor/src/vm/instruction/execution.rs | 132 +++++++++++++- 3 files changed, 340 insertions(+), 5 deletions(-) create mode 100644 executor/src/tests/keccak_absorb_tests.rs diff --git a/executor/src/tests/keccak_absorb_tests.rs b/executor/src/tests/keccak_absorb_tests.rs new file mode 100644 index 000000000..69bcc1844 --- /dev/null +++ b/executor/src/tests/keccak_absorb_tests.rs @@ -0,0 +1,212 @@ +//! Tests for the keccak sponge-absorb syscall (`KECCAK_ABSORB_SYSCALL_NUMBER`). +//! +//! The multi-block cases differentially test the executor's absorb loop +//! against an independent sponge replay built on `tiny_keccak::keccakf`. + +use crate::vm::instruction::decoding::Instruction; +use crate::vm::instruction::execution::{ + ExecutionError, KECCAK_ABSORB_SYSCALL_NUMBER, KECCAK_RATE_BYTES, +}; +use crate::vm::memory::Memory; +use crate::vm::registers::Registers; + +const STATE_ADDR: u64 = 0x1000; +const DATA_ADDR: u64 = 0x2000; + +/// Deterministic SplitMix64 for reproducible "random" data. +struct SplitMix64(u64); +impl SplitMix64 { + fn next_u64(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } +} + +/// Runs the absorb syscall over `n_blocks` blocks of deterministic data seeded +/// by `seed`, returning `(vm_state, reference_state)` where the reference is an +/// independent sponge replay over tiny-keccak's permutation. +fn run_absorb_differential(n_blocks: u64, seed: u64) -> ([u64; 25], [u64; 25]) { + let mut rng = SplitMix64(seed); + + let mut state: [u64; 25] = core::array::from_fn(|i| rng.next_u64() ^ (i as u64)); + let blocks: Vec<[u64; 17]> = (0..n_blocks) + .map(|_| core::array::from_fn(|_| rng.next_u64())) + .collect(); + + // Set up VM memory. + let mut pc = 0; + let mut registers = Registers::default(); + let mut memory = Memory::default(); + for (i, &lane) in state.iter().enumerate() { + memory + .store_doubleword(STATE_ADDR + (i as u64) * 8, lane) + .unwrap(); + } + for (k, block) in blocks.iter().enumerate() { + for (j, &dw) in block.iter().enumerate() { + memory + .store_doubleword( + DATA_ADDR + (k as u64) * KECCAK_RATE_BYTES + (j as u64) * 8, + dw, + ) + .unwrap(); + } + } + registers.write(17, KECCAK_ABSORB_SYSCALL_NUMBER).unwrap(); + registers.write(10, STATE_ADDR).unwrap(); + registers.write(11, DATA_ADDR).unwrap(); + registers.write(12, n_blocks).unwrap(); + + Instruction::EcallEbreak + .run(&mut pc, &mut registers, &mut memory) + .expect("absorb syscall failed"); + + let mut vm_state = [0u64; 25]; + for (i, lane) in vm_state.iter_mut().enumerate() { + *lane = memory.load_doubleword(STATE_ADDR + (i as u64) * 8).unwrap(); + } + + // Independent reference: sponge replay over tiny-keccak's permutation. + for block in &blocks { + for (lane, &m) in state.iter_mut().zip(block.iter()) { + *lane ^= m; + } + tiny_keccak::keccakf(&mut state); + } + + (vm_state, state) +} + +#[test] +fn test_absorb_single_block_matches_tiny_keccak() { + let (vm, reference) = run_absorb_differential(1, 0xA11C_E000_0000_0001); + assert_eq!(vm, reference, "1-block absorb diverges from tiny-keccak"); +} + +#[test] +fn test_absorb_two_blocks_matches_tiny_keccak() { + let (vm, reference) = run_absorb_differential(2, 0xA11C_E000_0000_0002); + assert_eq!(vm, reference, "2-block absorb diverges from tiny-keccak"); +} + +#[test] +fn test_absorb_many_blocks_matches_tiny_keccak() { + for n in [3u64, 5, 8, 13] { + let (vm, reference) = run_absorb_differential(n, 0xA11C_E000_0000_0100 ^ n); + assert_eq!(vm, reference, "{n}-block absorb diverges from tiny-keccak"); + } +} + +#[test] +fn test_absorb_matches_chained_permute_semantics() { + // The absorb over n blocks must equal n manual (XOR + keccak_f1600) steps + // with the executor's own permutation — guards the executor's loop + // structure independently of tiny-keccak. + use crate::vm::instruction::execution::keccak_f1600; + let (vm, _) = run_absorb_differential(4, 0xA11C_E000_0000_0200); + + let mut rng = SplitMix64(0xA11C_E000_0000_0200); + let mut state: [u64; 25] = core::array::from_fn(|i| rng.next_u64() ^ (i as u64)); + let blocks: Vec<[u64; 17]> = (0..4).map(|_| core::array::from_fn(|_| rng.next_u64())).collect(); + for block in &blocks { + for (lane, &m) in state.iter_mut().zip(block.iter()) { + *lane ^= m; + } + keccak_f1600(&mut state); + } + assert_eq!(vm, state); +} + +/// Sets up registers for a raw absorb call without touching memory content. +fn raw_call(state_addr: u64, data_addr: u64, n_blocks: u64) -> Result<(), ExecutionError> { + let mut pc = 0; + let mut registers = Registers::default(); + let mut memory = Memory::default(); + registers.write(17, KECCAK_ABSORB_SYSCALL_NUMBER).unwrap(); + registers.write(10, state_addr).unwrap(); + registers.write(11, data_addr).unwrap(); + registers.write(12, n_blocks).unwrap(); + Instruction::EcallEbreak + .run(&mut pc, &mut registers, &mut memory) + .map(|_| ()) +} + +#[test] +fn test_absorb_rejects_unaligned_state_addr() { + let err = raw_call(0x1001, DATA_ADDR, 1).unwrap_err(); + assert!(matches!( + err, + ExecutionError::UnalignedKeccakAbsorbStateAddress(0x1001) + )); +} + +#[test] +fn test_absorb_rejects_unaligned_data_addr() { + let err = raw_call(STATE_ADDR, 0x2004, 1).unwrap_err(); + assert!(matches!( + err, + ExecutionError::UnalignedKeccakAbsorbDataAddress(0x2004) + )); +} + +#[test] +fn test_absorb_rejects_zero_blocks() { + let err = raw_call(STATE_ADDR, DATA_ADDR, 0).unwrap_err(); + assert!(matches!(err, ExecutionError::KeccakAbsorbZeroBlocks)); +} + +#[test] +fn test_absorb_rejects_overflowing_state_range() { + let state_addr = u64::MAX - 191; // 8-aligned; last byte would overflow + let err = raw_call(state_addr, DATA_ADDR, 1).unwrap_err(); + assert!(matches!( + err, + ExecutionError::KeccakAbsorbStateAddressOverflow(a) if a == state_addr + )); +} + +#[test] +fn test_absorb_rejects_overflowing_data_range() { + let data_addr = u64::MAX - 127; // 8-aligned; last byte of one 136-byte block overflows + let err = raw_call(STATE_ADDR, data_addr, 1).unwrap_err(); + assert!(matches!( + err, + ExecutionError::KeccakAbsorbDataAddressOverflow(a) if a == data_addr + )); +} + +#[test] +fn test_absorb_rejects_overflowing_block_count() { + // n_blocks × 136 overflows u64. + let err = raw_call(STATE_ADDR, DATA_ADDR, u64::MAX / 8).unwrap_err(); + assert!(matches!( + err, + ExecutionError::KeccakAbsorbDataAddressOverflow(a) if a == DATA_ADDR + )); +} + +#[test] +fn test_absorb_rejects_low_limb_overflow() { + // Data region crosses the 2^32 low-limb boundary: last byte's low limb wraps. + let data_addr = (1u64 << 32) - 128; // 8-aligned; block's last byte is past 2^32 + let err = raw_call(STATE_ADDR, data_addr, 1).unwrap_err(); + assert!(matches!(err, ExecutionError::KeccakAbsorbAddressOverflow)); + // A block ending exactly AT the boundary (last byte 2^32 - 1) is accepted. + raw_call(STATE_ADDR, (1u64 << 32) - 136, 1) + .expect("block ending at the low-limb boundary must be accepted"); +} + +#[test] +fn test_absorb_rejects_overlapping_regions() { + // Data starts inside the 200-byte state region. + let err = raw_call(STATE_ADDR, STATE_ADDR + 192, 1).unwrap_err(); + assert!(matches!(err, ExecutionError::KeccakAbsorbOperandOverlap)); + // State starts inside the data region. + let err = raw_call(DATA_ADDR + 128, DATA_ADDR, 1).unwrap_err(); + assert!(matches!(err, ExecutionError::KeccakAbsorbOperandOverlap)); + // Adjacent regions (data immediately after state) are fine. + raw_call(STATE_ADDR, STATE_ADDR + 200, 1).expect("adjacent regions must be accepted"); +} diff --git a/executor/src/tests/mod.rs b/executor/src/tests/mod.rs index 456607433..81d2373f0 100644 --- a/executor/src/tests/mod.rs +++ b/executor/src/tests/mod.rs @@ -1,4 +1,5 @@ pub mod ecsm_tests; pub mod flamegraph_tests; +pub mod keccak_absorb_tests; pub mod keccak_tests; pub mod memory_tests; diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index c92c0ab88..3e16eb5f2 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -12,6 +12,8 @@ pub enum SyscallNumbers { KeccakPermute = 0, Print = 1, Panic = 2, + // Placeholder discriminant. The actual syscall value is KECCAK_ABSORB_SYSCALL_NUMBER. + KeccakAbsorbBlocks = 4, Commit = 64, Halt = 93, // Placeholder discriminant. The actual syscall value is ECSM_SYSCALL_NUMBER. @@ -24,6 +26,35 @@ pub enum SyscallNumbers { pub const KECCAK_SYSCALL_NUMBER: u64 = u64::MAX - 1; const KECCAK_STATE_BYTES: u64 = 25 * 8; +/// Syscall number for the keccak sponge-absorb accelerator +/// (spec ECALL `-4`; as unsigned that is `u64::MAX - 3 = 0xFFFF_FFFF_FFFF_FFFC`). +/// +/// ABI: +/// - `x10` (a0) = 8-byte-aligned pointer to the 200-byte keccak state, updated +/// in place; +/// - `x11` (a1) = 8-byte-aligned pointer to `n_blocks × 136` bytes of message +/// data (whole rate blocks only — the guest keeps the final `10*1`-padded +/// partial block on the classic per-permutation syscall); +/// - `x12` (a2) = `n_blocks` (must be non-zero). +/// +/// Semantics per block `k`: `state[0..17] ^= block_k` (lanewise little-endian +/// dwords), then `keccak_f1600(state)`. Lanes 17..25 are untouched by the XOR. +/// +/// Preconditions (rejected with an [`ExecutionError`] otherwise): +/// - both pointers 8-aligned, `n_blocks > 0`; +/// - neither region's LAST byte overflows `u64` **or** its lower 32-bit +/// address limb (the prover models per-dword addresses as +/// `base_lo + offset` without a carry into the high limb, exactly like the +/// ECSM operands); +/// - the state and data regions are disjoint (the trace builder issues all +/// message reads and the state read at the ecall's timestamp; an overlap +/// would put two MEMW ops on one `(address, timestamp)` pair, which the +/// memory argument cannot order — same rationale as the ECSM operand +/// overlap guard). +pub const KECCAK_ABSORB_SYSCALL_NUMBER: u64 = u64::MAX - 3; +/// Keccak rate in bytes for the absorb accelerator: 17 lanes × 8 bytes. +pub const KECCAK_RATE_BYTES: u64 = 17 * 8; + /// Syscall number for the ECSM (elliptic-curve scalar multiply) accelerator. /// /// The spec uses ECALL number `-11`; interpreted as an unsigned 64-bit value that is @@ -44,6 +75,7 @@ impl TryFrom for SyscallNumbers { 64 => Ok(SyscallNumbers::Commit), 93 => Ok(SyscallNumbers::Halt), v if v == KECCAK_SYSCALL_NUMBER => Ok(SyscallNumbers::KeccakPermute), + v if v == KECCAK_ABSORB_SYSCALL_NUMBER => Ok(SyscallNumbers::KeccakAbsorbBlocks), v if v == ECSM_SYSCALL_NUMBER => Ok(SyscallNumbers::Ecsm), _ => Err(()), } @@ -54,6 +86,7 @@ impl TryFrom for SyscallNumbers { #[derive(Clone, Copy, PartialEq, Eq, Debug)] pub enum Accelerator { Keccak, + KeccakAbsorb, Ecsm, } @@ -64,6 +97,7 @@ impl SyscallNumbers { pub fn accelerator(self) -> Option { match self { SyscallNumbers::KeccakPermute => Some(Accelerator::Keccak), + SyscallNumbers::KeccakAbsorbBlocks => Some(Accelerator::KeccakAbsorb), SyscallNumbers::Ecsm => Some(Accelerator::Ecsm), SyscallNumbers::Print | SyscallNumbers::Panic @@ -93,8 +127,13 @@ fn store_u256_le(memory: &mut Memory, addr: u64, bytes: &[u8; 32]) -> Result<(), Ok(()) } -/// Checks the ECSM address-alignment assumption: `(addr mod 2^32) + max_offset < 2^32`. -fn ecsm_addr_ok(addr: u64, max_offset: u64) -> bool { +/// Checks an accelerator operand's low-limb room: `(addr mod 2^32) + max_offset < 2^32`. +/// +/// The accelerator chips (ECSM, keccak sponge absorb) model per-access +/// addresses on the Memw bus as `base_lo + offset` with `base_hi` unchanged — +/// no carry into the high limb — so the whole operand must fit inside its low +/// 32-bit limb. `max_offset` is the offset of the region's LAST byte. +fn accel_addr_low_limb_ok(addr: u64, max_offset: u64) -> bool { (addr % LOW_LIMB) + max_offset < LOW_LIMB } @@ -421,6 +460,75 @@ impl Instruction { } src2_val = state_addr; } + SyscallNumbers::KeccakAbsorbBlocks => { + // Keccak sponge absorb (see KECCAK_ABSORB_SYSCALL_NUMBER): + // x10 = state (200 bytes, in place), x11 = message data + // (n_blocks × 136 bytes), x12 = n_blocks. + let state_addr = registers.read(10)?; + let data_addr = registers.read(11)?; + let n_blocks = registers.read(12)?; + + if !state_addr.is_multiple_of(8) { + return Err(ExecutionError::UnalignedKeccakAbsorbStateAddress( + state_addr, + )); + } + if !data_addr.is_multiple_of(8) { + return Err(ExecutionError::UnalignedKeccakAbsorbDataAddress( + data_addr, + )); + } + if n_blocks == 0 { + return Err(ExecutionError::KeccakAbsorbZeroBlocks); + } + // Bound the LAST byte of each region (state: +199; data: + // +n·136 − 1), both against u64 overflow and against the + // low-limb room the chip's linear addressing needs. + let state_end = state_addr + .checked_add(KECCAK_STATE_BYTES - 1) + .ok_or(ExecutionError::KeccakAbsorbStateAddressOverflow(state_addr))?; + let data_len = n_blocks + .checked_mul(KECCAK_RATE_BYTES) + .ok_or(ExecutionError::KeccakAbsorbDataAddressOverflow(data_addr))?; + let data_end = data_addr + .checked_add(data_len - 1) + .ok_or(ExecutionError::KeccakAbsorbDataAddressOverflow(data_addr))?; + if !accel_addr_low_limb_ok(state_addr, KECCAK_STATE_BYTES - 1) + || !accel_addr_low_limb_ok(data_addr, data_len - 1) + { + return Err(ExecutionError::KeccakAbsorbAddressOverflow); + } + // The regions must be disjoint: the trace builder reads + // the state and every message dword at the ecall's + // timestamp, so an overlap would put two MEMW ops on one + // (address, timestamp) pair, which the memory-consistency + // argument cannot order (same rationale as the ECSM + // operand-overlap guard — provability, not correctness). + // Compare via the (overflow-checked) inclusive end bytes. + if state_addr <= data_end && data_addr <= state_end { + return Err(ExecutionError::KeccakAbsorbOperandOverlap); + } + + let mut state = [0u64; 25]; + for (i, lane) in state.iter_mut().enumerate() { + *lane = memory.load_doubleword(state_addr + (i as u64) * 8)?; + } + for k in 0..n_blocks { + let block_base = data_addr + k * KECCAK_RATE_BYTES; + for (j, lane) in state.iter_mut().take(17).enumerate() { + *lane ^= memory.load_doubleword(block_base + (j as u64) * 8)?; + } + keccak_f1600(&mut state); + } + for (i, &lane) in state.iter().enumerate() { + memory.store_doubleword(state_addr + (i as u64) * 8, lane)?; + } + // Carry state_addr/data_addr in the CPU log; n_blocks is + // recovered from x12 by the trace builder's register-read + // path (like the ECSM operand addresses). + src2_val = state_addr; + dst_val = data_addr; + } SyscallNumbers::Ecsm => { // ECSM(-11): k×G on secp256k1. // x10 = addr to write xR, x11 = addr of xG, x12 = addr of k. @@ -429,9 +537,9 @@ impl Instruction { let addr_xr = registers.read(10)?; let addr_xg = registers.read(11)?; let addr_k = registers.read(12)?; - if !ecsm_addr_ok(addr_xg, 31) - || !ecsm_addr_ok(addr_xr, 31) - || !ecsm_addr_ok(addr_k, 31) + if !accel_addr_low_limb_ok(addr_xg, 31) + || !accel_addr_low_limb_ok(addr_xr, 31) + || !accel_addr_low_limb_ok(addr_k, 31) { return Err(ExecutionError::EcsmAddressOverflow); } @@ -630,6 +738,20 @@ pub enum ExecutionError { UnalignedKeccakStateAddress(u64), #[error("Keccak state address range overflows: {0:#018x}")] KeccakStateAddressOverflow(u64), + #[error("Unaligned Keccak-absorb state address: {0:#018x}")] + UnalignedKeccakAbsorbStateAddress(u64), + #[error("Unaligned Keccak-absorb data address: {0:#018x}")] + UnalignedKeccakAbsorbDataAddress(u64), + #[error("Keccak-absorb called with n_blocks = 0")] + KeccakAbsorbZeroBlocks, + #[error("Keccak-absorb state address range overflows: {0:#018x}")] + KeccakAbsorbStateAddressOverflow(u64), + #[error("Keccak-absorb data address range overflows: {0:#018x}")] + KeccakAbsorbDataAddressOverflow(u64), + #[error("Keccak-absorb operand range overflows the lower 32-bit address limb")] + KeccakAbsorbAddressOverflow, + #[error("Keccak-absorb state and data regions overlap")] + KeccakAbsorbOperandOverlap, #[error("ECSM address range overflows the lower 32-bit limb")] EcsmAddressOverflow, #[error("ECSM xG and k operand ranges overlap")] From 6f60c9315e548fc52c24075651185f363ecebd62 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 13:35:26 -0300 Subject: [PATCH 2/6] feat(syscalls,cli,spec): guest wrapper, cycle counter and spec entry for keccak absorb - syscalls: keccak_absorb_blocks(&mut [u64; 25], &[u8], n_blocks) guest wrapper (a7 = u64::MAX - 3). Documents the whole-rate-blocks contract (padding stays with the caller via keccak_permute) and debug-asserts the length and 8-byte data alignment the executor enforces. - cli --cycles: accel tuple (keccak, ecsm) -> (keccak, keccak_absorb, ecsm) with a 'KeccakAbsorb calls' line, via the existing accelerator_of confirmation path. - spec/about_ecalls.typ: register ECALL -4 (-3 is taken by the in-flight BLAKE3 accelerator PR). --- bin/cli/src/main.rs | 9 ++++++--- spec/about_ecalls.typ | 3 ++- syscalls/src/syscalls.rs | 34 ++++++++++++++++++++++++++++++++++ 3 files changed, 42 insertions(+), 4 deletions(-) diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index a04e920db..2b8f8e97d 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -412,7 +412,7 @@ fn cmd_execute( // below (the flamegraph path drives execution inside the executor and does // not expose per-log data). `None` means "not counted", so the accel lines // are omitted rather than printed as misleading zeros. - let mut accel_counts: Option<(u64, u64)> = None; + let mut accel_counts: Option<(u64, u64, u64)> = None; let cycle_count = if let Some(ref output_path) = flamegraph.path { // Shared execute+flamegraph path (executor::flamegraph) instead of @@ -479,6 +479,7 @@ fn cmd_execute( let mut cycle_count: u64 = 0; let mut keccak_calls: u64 = 0; + let mut keccak_absorb_calls: u64 = 0; let mut ecsm_calls: u64 = 0; // Reused per chunk: `(current_pc, a7)` for logs whose a7 matches an // accelerator syscall number. This is a cheap superset — a non-ECALL @@ -511,6 +512,7 @@ fn cmd_execute( for (pc, a7) in accel_candidates.drain(..) { match accelerator_of(executor.instructions.get(pc), a7) { Some(Accelerator::Keccak) => keccak_calls += 1, + Some(Accelerator::KeccakAbsorb) => keccak_absorb_calls += 1, Some(Accelerator::Ecsm) => ecsm_calls += 1, None => {} } @@ -526,15 +528,16 @@ fn cmd_execute( } if cycles { - accel_counts = Some((keccak_calls, ecsm_calls)); + accel_counts = Some((keccak_calls, keccak_absorb_calls, ecsm_calls)); } cycle_count }; if cycles { println!("Cycles: {}", cycle_count); - if let Some((keccak_calls, ecsm_calls)) = accel_counts { + if let Some((keccak_calls, keccak_absorb_calls, ecsm_calls)) = accel_counts { println!("Keccak calls: {}", keccak_calls); + println!("KeccakAbsorb calls: {}", keccak_absorb_calls); println!("Ecsm calls: {}", ecsm_calls); } } diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index 9b37d5f21..f09db672b 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -31,4 +31,5 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / 64: `write` (@commit) / 93: `exit` (@halt) / -1: `SHA256` (@sha256) -/ -2: `KECCAK` (@keccak) \ No newline at end of file +/ -2: `KECCAK` (@keccak) +/ -4: `KECCAK_ABSORB` — keccak sponge absorb: `a0` = 200-byte state (in place), `a1` = `a2` × 136-byte rate blocks; per block XOR into lanes 0..17 then keccak-f[1600]. Padding stays guest-side (final partial block goes through `KECCAK`). \ No newline at end of file diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index 7165dff81..28da3231c 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -29,6 +29,10 @@ pub enum SyscallNumbers { #[cfg(target_arch = "riscv64")] const KECCAK_SYSCALL_NUMBER: usize = usize::MAX - 1; +/// Syscall number for the keccak sponge-absorb accelerator (u64::MAX - 3, spec -4). +#[cfg(target_arch = "riscv64")] +const KECCAK_ABSORB_SYSCALL_NUMBER: usize = usize::MAX - 3; + /// Syscall number for the ECSM secp256k1 scalar-multiply accelerator (-11 as usize). #[cfg(target_arch = "riscv64")] const ECSM_SYSCALL_NUMBER: usize = usize::MAX - 10; @@ -165,6 +169,36 @@ pub fn keccak_permute(_state: &mut [u64; 25]) { unimplemented!("syscalls are only implemented for riscv64 targets"); } +#[cfg(target_arch = "riscv64")] +/// Absorb `n_blocks` whole 136-byte keccak rate blocks from `data` into +/// `state` in place: per block, `state[0..17] ^= block` (lanewise +/// little-endian dwords) followed by keccak-f[1600]. Padding stays with the +/// caller — hash the final `10*1`-padded partial block via [`keccak_permute`]. +/// +/// Requirements (executor-enforced, the call traps otherwise): `data` must be +/// 8-byte aligned and hold exactly `n_blocks * 136` bytes, `n_blocks > 0`, +/// and the data region must not overlap `state`. +pub fn keccak_absorb_blocks(state: &mut [u64; 25], data: &[u8], n_blocks: usize) { + debug_assert!(data.len() == n_blocks * 136, "data must be n_blocks × 136 bytes"); + debug_assert!(data.as_ptr().addr().is_multiple_of(8), "data must be 8-byte aligned"); + unsafe { + asm!( + "ecall", + in("a0") state.as_mut_ptr(), + in("a1") data.as_ptr(), + in("a2") n_blocks, + in("a7") KECCAK_ABSORB_SYSCALL_NUMBER, + ) + } +} + +#[cfg(not(target_arch = "riscv64"))] +/// Absorb `n_blocks` whole 136-byte keccak rate blocks from `data` into +/// `state` in place (XOR into lanes 0..17, then keccak-f[1600], per block). +pub fn keccak_absorb_blocks(_state: &mut [u64; 25], _data: &[u8], _n_blocks: usize) { + unimplemented!("syscalls are only implemented for riscv64 targets"); +} + #[cfg(target_arch = "riscv64")] /// Compute `xR = (k·G)_x` on secp256k1 via the ECSM accelerator. All values are 32-byte /// little-endian. Requires `0 < k < N` and a canonical valid `xG` curve coordinate. From 19cf6ce169a8a983b643a7587ad4bc1cd252b85c Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 13:51:54 -0300 Subject: [PATCH 3/6] feat(prover): KECCAK_SPONGE absorb chip, seq-keyed Keccak bus, full trace-builder wiring New table KECCAK_SPONGE (one row per absorbed 136-byte block, 690 main cols, 216 bus interactions, 7 transition constraints): - Row k of a call receives the running state over a new self-referential KeccakSponge chain bus (BusId 32), commits the block bytes, XORs them into lanes 0..17 via 136 ByteAlu[XOR] sends (which also range-check both operands and pin the outputs), passes lanes 17..25 through unchanged, and round-trips the absorbed state through the untouched KECCAK_RND chip over the Keccak bus (round 0 -> 24). - Bookends: the first row receives the ECALL, reads x10/x11/x12 and MEMW-reads the 25-lane state at ts; the last row MEMW-writes it back at ts+1 via write-only 16-element tuples (mu_first/mu_last flags). Soundness (the per-block keying landmine): all n permutations of one call share ONE CPU timestamp, and with the old (ts, round, state) Keccak-bus tuple a malicious prover could swap two blocks' permutation outputs with every tuple still appearing once per side - the bus BALANCES. Fix: the Keccak bus payload gains a seq element. The classic core chip sends seq = 0; sponge row k sends seq = k; KECCAK_RND carries seq through untouched like ts (new SEQ column, 1480 -> 1481 cols). SEQ is pinned by mu_first*SEQ = 0 plus the chain sender's SEQ+1, and the chain cannot wrap the field, so every permutation of a call gets a unique (ts, seq) key on both Keccak-bus legs. The chain also carries (n, state_ptr, block_base); the last row pins N_LO = SEQ+1 AND N_HI = 0 (word-level, closing the N = n + p mod-p alias), so a call has exactly x12 rows. Full attack walkthrough in the module docs. This extends the Keccak bus wire format: proof-breaking, noted for the PR. All eval constraints are degree <= 2 with IS_BIT on mu, mu_first, mu_last. Addressing deviates from the brief's keccak.rs DWordHL pointer apparatus in favor of the ECSM low-limb idiom (addresses as base_lo + offset linear elements; executor guarantees low-limb room; lying provers only produce unmatchable Memw/Memory tokens): the keccak apparatus would cost ~168 extra main cols + ~84 aux cols per BLOCK and defeat the accelerator's purpose. s_addr stays byte-decomposed (with AreBytes + the &7 alignment lookup) so alignment is enforced in-chip. Trace builder: collect_keccak_sponge_ops lowers one ecall into n sponge rows + n KeccakRoundOperations (seq = block index, input = absorbed state) + MEMW ops mirroring the chip send-for-send; the per-permutation round replay of collect_bitwise_from_keccak is factored into push_keccak_round_bitwise and shared with the new collect_bitwise_from_keccak_sponge; KECCAK_RC multiplicities now count classic + sponge permutations. FIXED_TABLE_COUNT 10 -> 11 (with the PR #871 always-on-AIR cost caveat), VmAirs/Traces wired in matching order on both prover and verifier lists. Tests: constraint-set exactly-once/degree/folder-capture agreement (check_table), program + device interpreter lists, a full sender <-> collector multiset-equality test (chip + KECCAK_RND sends evaluated off the generated traces vs the collector, over a 3-block call plus an n = 1 call), a no-IS_HALF guard, and an e2e prove+verify of a 3-block absorb asm guest cross-checked against a tiny-keccak sponge replay. --- executor/programs/asm/test_keccak_absorb.s | 50 ++ prover/src/lib.rs | 21 +- prover/src/tables/cpu.rs | 23 + prover/src/tables/keccak.rs | 12 +- prover/src/tables/keccak_rnd.rs | 41 +- prover/src/tables/keccak_sponge.rs | 726 ++++++++++++++++++ prover/src/tables/mod.rs | 1 + prover/src/tables/trace_builder.rs | 284 ++++++- prover/src/tables/types.rs | 18 +- prover/src/test_utils.rs | 18 + .../tests/constraint_program_device_tests.rs | 1 + prover/src/tests/constraint_program_tests.rs | 1 + prover/src/tests/constraint_set_tests_b.rs | 14 + prover/src/tests/keccak_rnd_tests.rs | 1 + prover/src/tests/keccak_sponge_tests.rs | 250 ++++++ prover/src/tests/mod.rs | 2 + prover/src/tests/prove_elfs_tests.rs | 43 ++ prover/src/tests/trace_builder_tests.rs | 1 + 18 files changed, 1480 insertions(+), 27 deletions(-) create mode 100644 executor/programs/asm/test_keccak_absorb.s create mode 100644 prover/src/tables/keccak_sponge.rs create mode 100644 prover/src/tests/keccak_sponge_tests.rs diff --git a/executor/programs/asm/test_keccak_absorb.s b/executor/programs/asm/test_keccak_absorb.s new file mode 100644 index 000000000..bc044b3e8 --- /dev/null +++ b/executor/programs/asm/test_keccak_absorb.s @@ -0,0 +1,50 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + # 608 bytes on the stack: 200-byte keccak state at sp, then + # 3 x 136-byte rate blocks at sp+200 (regions disjoint, both 8-aligned). + addi sp, sp, -608 + + # Deterministic non-zero state: lane[i] = i + 1 (25 lanes). + # The host test replays the sponge over tiny-keccak from this seed. + mv t0, sp + li t1, 1 + li t2, 26 +.Lstate_loop: + sd t1, 0(t0) + addi t0, t0, 8 + addi t1, t1, 1 + bne t1, t2, .Lstate_loop + + # Deterministic message data: dword[k] = k + 100 (51 dwords = 3 blocks). + addi t0, sp, 200 + li t1, 100 + li t2, 151 +.Ldata_loop: + sd t1, 0(t0) + addi t0, t0, 8 + addi t1, t1, 1 + bne t1, t2, .Ldata_loop + + # Absorb all 3 blocks in ONE ecall. + # a0 = state, a1 = data, a2 = n_blocks, a7 = u64::MAX - 3 (spec -4). + mv a0, sp + addi a1, sp, 200 + li a2, 3 + li a7, -4 + ecall + + # Commit the final 200-byte state. + li a0, 1 + mv a1, sp + li a2, 200 + li a7, 64 + ecall + + # Restore stack and halt. + addi sp, sp, 608 + li a0, 0 + li a7, 93 + ecall +.Lfunc_end0: + .size main, .Lfunc_end0-main diff --git a/prover/src/lib.rs b/prover/src/lib.rs index a8e89f989..939fb9728 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -54,9 +54,9 @@ use crate::test_utils::{ E, F, VmAir, create_bitwise_air, create_branch_air, create_bytewise_air, create_commit_air, create_cpu_air, create_cpu32_air, create_decode_air, create_dvrm_air, create_ecdas_air, create_ecsm_air, create_eq_air, create_halt_air, create_keccak_air, create_keccak_rc_air, - create_keccak_rnd_air, create_load_air, create_lt_air, create_memw_air, - create_memw_aligned_air, create_memw_register_air, create_mul_air, create_page_air, - create_register_air, create_shift_air, create_store_air, + create_keccak_rnd_air, create_keccak_sponge_air, create_load_air, create_lt_air, + create_memw_air, create_memw_aligned_air, create_memw_register_air, create_mul_air, + create_page_air, create_register_air, create_shift_air, create_store_air, }; // Re-exported for downstream hosts and verifier guests (e.g. the in-VM @@ -82,8 +82,14 @@ pub struct RuntimePageRange { /// Number of tables that always contribute exactly one sub-proof, regardless /// of `TableCounts`: bitwise, decode, halt, commit, keccak, keccak_rnd, -/// keccak_rc, register, ecsm, ecdas. -pub const FIXED_TABLE_COUNT: usize = 10; +/// keccak_rc, keccak_sponge, register, ecsm, ecdas. +/// +/// ⚠ Every always-on table costs every proof a near-empty AIR even when the +/// workload never touches it (the EC-campaign lesson, PR #871: three extra +/// near-empty always-on AIRs regressed prove time and peak heap by ~25%). +/// KECCAK_SPONGE adds one (min 4 rows × 690 main cols + ~108 aux cols); its +/// cost on sponge-free workloads must be ABBA-benched before this merges. +pub const FIXED_TABLE_COUNT: usize = 11; /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. @@ -515,6 +521,7 @@ pub(crate) struct VmAirs { pub keccak: VmAir, pub keccak_rnd: VmAir, pub keccak_rc: VmAir, + pub keccak_sponge: VmAir, pub ecsm: VmAir, pub ecdas: VmAir, pub register: VmAir, @@ -540,6 +547,7 @@ impl VmAirs { (self.keccak.as_ref(), &mut traces.keccak, &()), (self.keccak_rnd.as_ref(), &mut traces.keccak_rnd, &()), (self.keccak_rc.as_ref(), &mut traces.keccak_rc, &()), + (self.keccak_sponge.as_ref(), &mut traces.keccak_sponge, &()), (self.ecsm.as_ref(), &mut traces.ecsm, &()), (self.ecdas.as_ref(), &mut traces.ecdas, &()), (self.register.as_ref(), &mut traces.register, &()), @@ -614,6 +622,7 @@ impl VmAirs { self.keccak.as_ref(), self.keccak_rnd.as_ref(), self.keccak_rc.as_ref(), + self.keccak_sponge.as_ref(), self.ecsm.as_ref(), self.ecdas.as_ref(), self.register.as_ref(), @@ -771,6 +780,7 @@ impl VmAirs { tables::keccak_rc::preprocessed_commitment(proof_options), tables::keccak_rc::NUM_PRECOMPUTED_COLS, )); + let keccak_sponge: VmAir = Box::new(create_keccak_sponge_air(proof_options)); let ecsm: VmAir = Box::new(create_ecsm_air(proof_options)); let ecdas: VmAir = Box::new(create_ecdas_air(proof_options)); let register: VmAir = @@ -877,6 +887,7 @@ impl VmAirs { keccak, keccak_rnd, keccak_rc, + keccak_sponge, ecsm, ecdas, register, diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 781bb02b0..bff8f0c1f 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -186,6 +186,15 @@ pub struct CpuOperation { /// For KeccakPermute ECALLs: state address from x10. pub keccak_state_addr: u64, + /// Whether this ECALL is a KeccakAbsorbBlocks syscall. + pub ecall_keccak_absorb: bool, + /// For KeccakAbsorbBlocks ECALLs: state address from x10. + pub keccak_absorb_state_addr: u64, + /// For KeccakAbsorbBlocks ECALLs: message data address from x11. + /// (`n_blocks` is recovered from the x12 register state in the trace + /// builder, like the ECSM operand addresses.) + pub keccak_absorb_data_addr: u64, + /// Whether this ECALL is an ECSM (elliptic-curve scalar multiply) syscall pub ecall_ecsm: bool, } @@ -231,6 +240,14 @@ impl CpuOperation { let ecall_keccak = f.ecall && log.src1_val == executor::vm::instruction::execution::KECCAK_SYSCALL_NUMBER; let keccak_state_addr = if ecall_keccak { log.src2_val } else { 0 }; + let ecall_keccak_absorb = f.ecall + && log.src1_val + == executor::vm::instruction::execution::KECCAK_ABSORB_SYSCALL_NUMBER; + let (keccak_absorb_state_addr, keccak_absorb_data_addr) = if ecall_keccak_absorb { + (log.src2_val, log.dst_val) + } else { + (0, 0) + }; // The ECSM operand addresses (x10/x11/x12) are recovered from the register state // in the trace builder. let ecall_ecsm = @@ -252,6 +269,9 @@ impl CpuOperation { commit_count, ecall_keccak, keccak_state_addr, + ecall_keccak_absorb, + keccak_absorb_state_addr, + keccak_absorb_data_addr, decode, timestamp, ..Default::default() @@ -352,6 +372,9 @@ impl CpuOperation { commit_count, ecall_keccak, keccak_state_addr, + ecall_keccak_absorb, + keccak_absorb_state_addr, + keccak_absorb_data_addr, ecall_ecsm, } } diff --git a/prover/src/tables/keccak.rs b/prover/src/tables/keccak.rs index 7b84cbd48..d29ee14a7 100644 --- a/prover/src/tables/keccak.rs +++ b/prover/src/tables/keccak.rs @@ -261,10 +261,14 @@ pub fn bus_interactions() -> Vec { )); } - // 2. Keccak bus: send (timestamp, 0, input_state[200]) + // 2. Keccak bus: send (timestamp, 0, seq = 0, input_state[200]) // Per spec keccak.toml: input = ["timestamp", 0, "input_state"] where // input_state is [[[Byte, 8], 5], 5] — 200 Byte elements, each its own - // bus element (no packing). + // bus element (no packing). The `seq` element is a wire-format extension + // over the spec: KECCAK_SPONGE runs several permutations under ONE ecall + // timestamp and keys each with its block index so their outputs cannot be + // swapped (see `tables::keccak_sponge`); the classic one-permutation-per- + // ecall chip always sends seq = 0. { let mut values = vec![ BusValue::Packed { @@ -276,6 +280,7 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }, BusValue::constant(0), // round = 0 + BusValue::constant(0), // seq = 0 (single permutation per ecall) ]; for x in 0..5 { for y in 0..5 { @@ -294,7 +299,7 @@ pub fn bus_interactions() -> Vec { )); } - // 3. Keccak bus: receive (timestamp, 24, output_state[200]) + // 3. Keccak bus: receive (timestamp, 24, seq = 0, output_state[200]) { let mut values = vec![ BusValue::Packed { @@ -306,6 +311,7 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }, BusValue::constant(24), // round = 24 + BusValue::constant(0), // seq = 0 (single permutation per ecall) ]; for x in 0..5 { for y in 0..5 { diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index 51b7759f3..2a6988477 100644 --- a/prover/src/tables/keccak_rnd.rs +++ b/prover/src/tables/keccak_rnd.rs @@ -7,12 +7,13 @@ //! `KeccakRndConstraints`). ARE_BYTES range checks on the shift outputs and the //! IS_BIT constraint on the θ carry are load-bearing for the identities. //! -//! ## Column layout (1,480 columns) +//! ## Column layout (1,481 columns) //! //! | Group | Size | Description | //! |----------------|------|---------------------------------------------------| //! | timestamp | 2 | DWordWL | //! | round | 1 | Round index (0..23) | +//! | seq | 1 | Permutation index within the ecall (see below) | //! | start | 200 | Input state bytes [5][5][8] | //! | Cxz | 160 | Column parity chain [5][4][8] | //! | Cxz_left | 40 | Left component of rotated C [5][8] | @@ -31,6 +32,16 @@ //! constants derived from `KECCAK_RHO[x][y]`, not materialized as columns. //! `Cxz_right` is typed `[Bit, 4]` per spec d75944ee — a halfword rotate-by-1 //! carries out a single bit, range-checked via IS_BIT polynomial constraints. +//! +//! `seq` is carried through this chip untouched, exactly like `timestamp`: the +//! Keccak-bus receive and send both include it, so the whole 24-round chain of +//! one permutation is keyed by `(timestamp, seq)`. The classic KECCAK core +//! chip always uses `seq = 0`; KECCAK_SPONGE runs one permutation per absorbed +//! block under a single ecall timestamp and keys block `k` with `seq = k` — +//! without it, two blocks of one call would share the key and their outputs +//! could be swapped with the bus still balancing (see `tables::keccak_sponge`). +//! No constraint on `seq` is needed here: it participates in every bus tuple +//! of the chain, so any inconsistent value simply fails to match. use executor::vm::instruction::execution::{KECCAK_RC, KECCAK_RHO}; use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; @@ -87,12 +98,16 @@ pub mod cols { // iota[8] — χ[0][0] ⊕ rc pub const IOTA: usize = RC + 8; // 1471 + // seq — permutation index within the ecall (0 for the classic core chip, + // the block index for KECCAK_SPONGE). Carried through like timestamp. + pub const SEQ: usize = IOTA + 8; // 1479 + // mu — multiplicity flag. // rnc and rbc (spec [[variables.constant]]) are inlined as compile-time // constants from KECCAK_RHO, not allocated as columns. - pub const MU: usize = IOTA + 8; // 1479 + pub const MU: usize = SEQ + 1; // 1480 - pub const NUM_COLUMNS: usize = MU + 1; // 1480 + pub const NUM_COLUMNS: usize = MU + 1; // 1481 // ------------------------------------------------------------------------- // Index helpers @@ -211,6 +226,10 @@ pub mod cols { #[derive(Debug, Clone)] pub struct KeccakRoundOperation { pub timestamp: u64, + /// Permutation index within the ecall: 0 for the classic core chip, the + /// block index for KECCAK_SPONGE (which shares one timestamp across all + /// blocks of a call). + pub seq: u64, pub input: [u64; 25], pub output: [u64; 25], } @@ -261,9 +280,10 @@ pub fn generate_keccak_rnd_trace( for round in 0..24 { let row_idx = op_idx * 24 + round; - // Timestamp & round + // Timestamp, round & seq table.set_dword_wl(row_idx, cols::TIMESTAMP_0, op.timestamp); table.set_u64(row_idx, cols::ROUND, round as u64); + table.set_u64(row_idx, cols::SEQ, op.seq); // start = current state as bytes for x in 0..5 { @@ -447,9 +467,10 @@ pub fn bus_interactions() -> Vec { // --- IO group (3) --- - // 1. KECCAK bus: receive (timestamp, round, start[200]) + // 1. KECCAK bus: receive (timestamp, round, seq, start[200]) // Per spec keccak_round.toml: input = ["timestamp", "round", "start"] where // start is [[[Byte, 8], 5], 5] — 200 Byte elements, each its own bus element. + // `seq` is a wire-format extension over the spec (see the module docs). { let mut values = vec![ BusValue::Packed { @@ -464,6 +485,10 @@ pub fn bus_interactions() -> Vec { start_column: cols::ROUND, packing: Packing::Direct, }, + BusValue::Packed { + start_column: cols::SEQ, + packing: Packing::Direct, + }, ]; for x in 0..5 { for y in 0..5 { @@ -482,7 +507,7 @@ pub fn bus_interactions() -> Vec { )); } - // 2. KECCAK bus: send (timestamp, round+1, out[200]) + // 2. KECCAK bus: send (timestamp, round+1, seq, out[200]) // out[0][0] = iota, out[x][y] = chi for (x,y) != (0,0) { let mut values = vec![ @@ -501,6 +526,10 @@ pub fn bus_interactions() -> Vec { }, LinearTerm::Constant(1), ]), + BusValue::Packed { + start_column: cols::SEQ, + packing: Packing::Direct, + }, ]; for x in 0..5 { for y in 0..5 { diff --git a/prover/src/tables/keccak_sponge.rs b/prover/src/tables/keccak_sponge.rs new file mode 100644 index 000000000..aab4478a0 --- /dev/null +++ b/prover/src/tables/keccak_sponge.rs @@ -0,0 +1,726 @@ +//! KECCAK_SPONGE chip — the sponge-absorb accelerator (`ECALL -4`). +//! +//! One row per absorbed 136-byte rate block. An absorb call over `n` blocks +//! occupies `n` rows that all share the ecall's CPU timestamp: the first row +//! receives the ECALL, reads the three operand registers and MEMW-reads the +//! 25-lane state; every row MEMW-reads its 17 message dwords, XORs the block +//! into lanes 0..17 via `ByteAlu[XOR]` lookups and round-trips the absorbed +//! state through the shared KECCAK_RND chip over the `Keccak` bus; the last +//! row MEMW-writes the final state back. Between rows, the running state and +//! the call's registers travel over the self-referential `KeccakSponge` chain +//! bus (same shape as COMMIT's `CommitNextByte` and the ECDAS sequence bus). +//! +//! ## Why every permutation is keyed by `(timestamp, seq)` — the swap attack +//! +//! All `n` permutations of one call share ONE CPU timestamp (the ecall is a +//! single cycle). The `Keccak` bus tuple used to be `(ts, round, state)` and +//! the round chip echoes `ts` through its 24-round chain. With two blocks A +//! and B at the same `ts`, a malicious prover could feed the round chip +//! `perm-input(A)` and `perm-input(B)` and hand A's permutation output to B's +//! row and vice versa: every tuple still appears exactly once per side, so +//! **the bus balances** and the forged sponge "absorbs" the blocks against +//! swapped intermediate states. The chain equality between rows does not save +//! this on its own — it only forces *some* consistent assignment of outputs +//! to rows, not the right one — unless the keys on the Keccak-bus legs are +//! unique per permutation. +//! +//! The fix: the `Keccak` bus carries an extra `seq` element. The classic +//! KECCAK core chip (one permutation per ecall) sends `seq = 0`; sponge row +//! `k` sends `seq = SEQ = k`; KECCAK_RND carries `seq` through untouched, +//! exactly like it carries `ts`. `SEQ` itself is pinned by the chain: +//! +//! - `μ_first · SEQ = 0` anchors the first row of a call at `SEQ = 0`; +//! - the chain sender emits `SEQ + 1` and the receiver consumes `SEQ`, so +//! every non-first row's `SEQ` is its predecessor's `SEQ + 1`. A chain can +//! never wrap the field (that would need `p ≈ 2^64` rows), so `SEQ` values +//! along one call are exactly `0, 1, …, n−1` — distinct, hence every +//! permutation of the call has a unique `(ts, seq)` key on both Keccak-bus +//! legs, and the swap above unbalances the bus. +//! +//! Chain-shape soundness (why the rows of one call form a simple path): +//! - exactly one `μ_first` row per call: the CPU sends ONE Ecall token per +//! ecall; two first rows would consume it twice and unbalance the bus; +//! - no forks/merges: every chain token is emitted once (`μ − μ_last`) and +//! consumed once (`μ − μ_first`); duplicating a link propagates back to a +//! duplicated Ecall consumption (and forward to a duplicated state write on +//! one `(address, timestamp)` pair, which the memory argument rejects); +//! - exactly `n = x12` rows: the first row reads `x12` into `(N_LO, N_HI)`, +//! the chain carries them unchanged, and the last row pins +//! `N_LO = SEQ + 1`, `N_HI = 0`. Pinning the WORDS (not the recombined +//! field value) closes the mod-p alias `N = n + p`: a register value of +//! `n + p` has `N_HI = 2^32 − 1 ≠ 0`. This bounds provable calls to +//! `n < 2^32`, which is vacuous — `n` real rows must exist in this table, +//! so `n` is bounded by the trace size long before `2^32`; +//! - a call can never end early or run forever: a non-last row's chain token +//! must be consumed and a last row must satisfy `N_LO = SEQ + 1`, so +//! `n = 0` (which the executor also rejects) admits no witness at all. +//! +//! ## Addressing (ECSM low-limb idiom, NOT the KECCAK pointer apparatus) +//! +//! The classic KECCAK core chip materializes one DWordHL pointer per lane +//! (100 columns + 100 IS_HALF sends per row). That is affordable at one row +//! per *call* but would double this chip's per-block cost, so the sponge uses +//! the ECSM operand idiom instead: per-access addresses go on the Memw bus as +//! `base_lo + offset` with `base_hi` unchanged — no carry into the low limb — +//! and the executor guarantees the room (`(base % 2^32) + last_offset < +//! 2^32`, see `KECCAK_ABSORB_SYSCALL_NUMBER`). Soundness is fail-closed: a +//! block base whose low limb has drifted out of range yields Memw/Memory +//! tokens with no matching PAGE/REGISTER cell, unbalancing the bus (the same +//! argument `memw.rs` makes for its virtual `address_add` carries). +//! +//! - `state_ptr` is materialized as 8 range-checked bytes (`S_ADDR`, DWordBL) +//! so the `addr & 7 = 0` alignment lookup has the low byte; lane `i` of the +//! state lives at `(s_lo + 8i, s_hi)` with `s_lo/s_hi` the byte recombines. +//! - the current block base is carried as two words `(D_LO, D_HI)`; message +//! dword `j` lives at `(D_LO + 8j, D_HI)`; the chain sender advances the +//! base by one rate block as the *linear* element `D_LO + 136` (sound +//! because the executor's low-limb guarantee covers the whole data region, +//! and a lying prover only produces unmatchable Memw tokens, per the +//! fail-closed argument above). +//! +//! ## Memory model (must mirror `collect_keccak_sponge_memw_ops` op-for-op) +//! +//! - first row, at `ts`: register reads x10/x11/x12 (24-element read tuples) +//! and 25 pure lane reads of the state (`old = value = STATE_IN`); +//! - every row, at `ts`: 17 pure dword reads of the block (`old = value`); +//! - last row, at `ts + 1`: 25 write-only lane writes (16-element tuples; the +//! MEMW table materializes `old` itself — the pre-write content is the +//! first row's `STATE_IN`, re-written at `ts` by the lane reads). Reads at +//! `ts` / write at `ts + 1` keeps every `(address, timestamp)` pair unique, +//! which the memory argument's strict `old_ts < ts` ordering requires; the +//! executor's region-overlap rejection guarantees the state and data +//! regions never collide at `ts`. +//! +//! ## Byte range checks +//! +//! `STATE_IN[0..136]` and `BLOCK` are operands of the `ByteAlu[XOR]` lookups, +//! which simultaneously range-check both operands and pin the output — +//! `XORED` needs no extra check. `STATE_IN[136..200]` is bound element-wise +//! either to memory bytes (first row, MEMW read) or to the previous row's +//! `STATE_OUT` (chain), and `STATE_OUT` is bound element-wise to KECCAK_RND's +//! χ/ι columns, themselves XOR-lookup outputs — so every state byte is +//! transitively range-checked without further sends. `S_ADDR` gets explicit +//! `AreBytes` pairs (its cells feed linear address recombines). +//! +//! ## Column layout (690 columns) +//! +//! | Group | Size | Description | +//! |-------------|------|----------------------------------------------------| +//! | timestamp | 2 | DWordWL, the ecall's CPU timestamp | +//! | seq | 1 | Block index within the call (0-based) | +//! | n | 2 | x12 (n_blocks) as DWordWL words | +//! | s_addr | 8 | state_ptr as DWordBL bytes | +//! | d | 2 | current block base (data_ptr + 136·seq) as words | +//! | state_in | 200 | running state entering this block [lane][byte] | +//! | block | 136 | message block bytes [lane][byte] | +//! | xored | 136 | state_in[i] ^ block[i] for the absorbed region | +//! | state_out | 200 | permuted state [lane][byte] | +//! | μ, μ_first, μ_last | 3 | multiplicity / bookend flags | + +use executor::vm::instruction::execution::{KECCAK_ABSORB_SYSCALL_NUMBER, KECCAK_RATE_BYTES}; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; + +use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; +use crate::constraints::templates::emit_is_bit; + +/// Bytes of one rate block (17 lanes × 8). +pub const RATE_BYTES: usize = KECCAK_RATE_BYTES as usize; +/// Lanes of one rate block. +pub const RATE_LANES: usize = 17; + +// ========================================================================= +// Column indices +// ========================================================================= + +pub mod cols { + use super::RATE_BYTES; + + pub const TIMESTAMP_0: usize = 0; + pub const TIMESTAMP_1: usize = 1; + + /// Block index within the call (0-based). + pub const SEQ: usize = 2; + + /// x12 (n_blocks) as DWordWL words, carried unchanged along the chain. + pub const N_LO: usize = 3; + pub const N_HI: usize = 4; + + /// state_ptr as DWordBL (8 bytes), carried along the chain. + pub const S_ADDR: usize = 5; + + /// Current block base address (data_ptr + 136·seq) as DWordWL words. + pub const D_LO: usize = S_ADDR + 8; // 13 + pub const D_HI: usize = D_LO + 1; // 14 + + /// state_in[25][8] — running state entering this block. + pub const STATE_IN: usize = D_HI + 1; // 15 + + /// block[17][8] — the message block. + pub const BLOCK: usize = STATE_IN + 200; // 215 + + /// xored[17][8] — state_in ^ block over the absorbed region. + pub const XORED: usize = BLOCK + RATE_BYTES; // 351 + + /// state_out[25][8] — the permuted state. + pub const STATE_OUT: usize = XORED + RATE_BYTES; // 487 + + /// μ: 1 on real rows. + pub const MU: usize = STATE_OUT + 200; // 687 + /// μ_first: 1 on the first row of a call (receives the ECALL). + pub const MU_FIRST: usize = MU + 1; // 688 + /// μ_last: 1 on the last row of a call (writes the state back). + pub const MU_LAST: usize = MU_FIRST + 1; // 689 + + pub const NUM_COLUMNS: usize = MU_LAST + 1; // 690 + + // ------------------------------------------------------------------------- + // Index helpers (lane = x + 5y, matching the KECCAK core chip layout) + // ------------------------------------------------------------------------- + + #[inline] + pub const fn s_addr(byte: usize) -> usize { + S_ADDR + byte + } + + #[inline] + pub const fn state_in(lane: usize, byte: usize) -> usize { + STATE_IN + lane * 8 + byte + } + + #[inline] + pub const fn block(lane: usize, byte: usize) -> usize { + BLOCK + lane * 8 + byte + } + + #[inline] + pub const fn xored(lane: usize, byte: usize) -> usize { + XORED + lane * 8 + byte + } + + #[inline] + pub const fn state_out(lane: usize, byte: usize) -> usize { + STATE_OUT + lane * 8 + byte + } +} + +// ========================================================================= +// Operation struct +// ========================================================================= + +/// One absorbed block (= one row) of a keccak sponge-absorb call. +#[derive(Debug, Clone)] +pub struct KeccakSpongeOperation { + /// The ecall's CPU timestamp (shared by every block of the call). + pub timestamp: u64, + /// Block index within the call (0-based). + pub seq: u64, + /// Total blocks of the call (the x12 register value). + pub n_blocks: u64, + /// state_ptr (the x10 register value). + pub state_addr: u64, + /// This block's base address: data_ptr + 136·seq. + pub block_addr: u64, + /// Running state entering this block. + pub state_in: [u64; 25], + /// The 136 message bytes of this block. + pub block: [u8; RATE_BYTES], + /// The permuted state leaving this block. + pub state_out: [u64; 25], + /// First row of the call. + pub first: bool, + /// Last row of the call. + pub last: bool, +} + +// ========================================================================= +// Trace generation +// ========================================================================= + +pub fn generate_keccak_sponge_trace( + ops: &[KeccakSpongeOperation], +) -> TraceTable { + let n = ops.len(); + let num_rows = n.next_power_of_two().max(4); + let mut trace = TraceTable::new_main( + crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let table = &mut trace.main_table; + + for (row_idx, op) in ops.iter().enumerate() { + table.set_dword_wl(row_idx, cols::TIMESTAMP_0, op.timestamp); + table.set_u64(row_idx, cols::SEQ, op.seq); + table.set_dword_wl(row_idx, cols::N_LO, op.n_blocks); + table.set_dword_bl(row_idx, cols::s_addr(0), op.state_addr); + table.set_dword_wl(row_idx, cols::D_LO, op.block_addr); + + for (lane, &v) in op.state_in.iter().enumerate() { + table.set_dword_bl(row_idx, cols::state_in(lane, 0), v); + } + table.set_bytes(row_idx, cols::block(0, 0), &op.block); + for i in 0..RATE_BYTES { + let state_byte = ((op.state_in[i / 8] >> ((i % 8) * 8)) & 0xFF) as u8; + table.set_byte(row_idx, cols::XORED + i, state_byte ^ op.block[i]); + } + for (lane, &v) in op.state_out.iter().enumerate() { + table.set_dword_bl(row_idx, cols::state_out(lane, 0), v); + } + + table.set_fe(row_idx, cols::MU, FE::one()); + table.set_bool(row_idx, cols::MU_FIRST, op.first); + table.set_bool(row_idx, cols::MU_LAST, op.last); + } + + // Padding rows stay all-zero: μ = μ_first = μ_last = 0 gates every bus + // interaction, and all seven transition constraints hold at zero. + trace +} + +// ========================================================================= +// Bus value helpers +// ========================================================================= + +fn packed(col: usize) -> BusValue { + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + } +} + +/// `s_addr`'s low word as a linear byte recombine, plus a constant offset. +fn s_lo_plus(offset: i64) -> BusValue { + let mut terms: Vec = (0..4) + .map(|i| LinearTerm::Column { + coefficient: 1i64 << (8 * i), + column: cols::s_addr(i), + }) + .collect(); + if offset != 0 { + terms.push(LinearTerm::Constant(offset)); + } + BusValue::linear(terms) +} + +/// `s_addr`'s high word as a linear byte recombine. +fn s_hi() -> BusValue { + BusValue::linear( + (0..4) + .map(|i| LinearTerm::Column { + coefficient: 1i64 << (8 * i), + column: cols::s_addr(4 + i), + }) + .collect(), + ) +} + +/// `[old[8], is_register, base_lo, base_hi, value[8], ts_lo, ts_hi, w2, w4, w8]` +/// — a 24-element MEMW **read** tuple (`old == value`), as in `ecsm.rs`. +fn memw_read( + value: [BusValue; 8], + is_register: u64, + base_lo: BusValue, + base_hi: BusValue, + ts_lo: BusValue, + ts_hi: BusValue, + w2: u64, + w8: u64, +) -> Vec { + let mut v = Vec::with_capacity(24); + v.extend(value.clone()); // old == value (read) + v.push(BusValue::constant(is_register)); + v.push(base_lo); + v.push(base_hi); + v.extend(value); + v.push(ts_lo); + v.push(ts_hi); + v.push(BusValue::constant(w2)); + v.push(BusValue::constant(0)); + v.push(BusValue::constant(w8)); + v +} + +/// `[is_register, base_lo, base_hi, value[8], ts_lo, ts_hi, w2, w4, w8]` — +/// a 16-element MEMW **write** tuple (the MEMW table supplies `old`). +fn memw_write( + value: [BusValue; 8], + base_lo: BusValue, + base_hi: BusValue, + ts_lo: BusValue, + ts_hi: BusValue, +) -> Vec { + let mut v = Vec::with_capacity(16); + v.push(BusValue::constant(0)); // is_register = 0 (memory) + v.push(base_lo); + v.push(base_hi); + v.extend(value); + v.push(ts_lo); + v.push(ts_hi); + v.push(BusValue::constant(0)); // w2 + v.push(BusValue::constant(0)); // w4 + v.push(BusValue::constant(1)); // w8 + v +} + +/// A register value `[lo, hi, 0, 0, 0, 0, 0, 0]` as MEMW value elements. +fn register_value(lo: BusValue, hi: BusValue) -> [BusValue; 8] { + let mut v: [BusValue; 8] = std::array::from_fn(|_| BusValue::constant(0)); + v[0] = lo; + v[1] = hi; + v +} + +/// The 8 bytes of trace lane `col + 8*lane .. +8` as MEMW value elements. +fn lane_bytes(base_col: usize, lane: usize) -> [BusValue; 8] { + std::array::from_fn(|b| packed(base_col + lane * 8 + b)) +} + +/// The call-state elements shared by the chain receive/send: +/// `[n_lo, n_hi, s_lo, s_hi, d_lo(+offset), d_hi]`. +fn chain_registers(d_lo_offset: i64) -> Vec { + let d_lo = if d_lo_offset == 0 { + packed(cols::D_LO) + } else { + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::D_LO, + }, + LinearTerm::Constant(d_lo_offset), + ]) + }; + vec![ + packed(cols::N_LO), + packed(cols::N_HI), + s_lo_plus(0), + s_hi(), + d_lo, + packed(cols::D_HI), + ] +} + +// ========================================================================= +// Bus interactions (216 total) +// ========================================================================= + +pub fn bus_interactions() -> Vec { + let syscall_lo = KECCAK_ABSORB_SYSCALL_NUMBER & 0xFFFF_FFFF; + let syscall_hi = KECCAK_ABSORB_SYSCALL_NUMBER >> 32; + let mu = || Multiplicity::Column(cols::MU); + let mu_first = || Multiplicity::Column(cols::MU_FIRST); + let mu_last = || Multiplicity::Column(cols::MU_LAST); + let ts_lo = || packed(cols::TIMESTAMP_0); + let ts_hi = || packed(cols::TIMESTAMP_1); + let ts_lo_plus_1 = || { + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::TIMESTAMP_0, + }, + LinearTerm::Constant(1), + ]) + }; + + let mut interactions = Vec::with_capacity(216); + + // 1. ECALL receiver (mult = μ_first): [ts_lo, ts_hi, syscall_lo32, syscall_hi32]. + interactions.push(BusInteraction::receiver( + BusId::Ecall, + mu_first(), + vec![ + ts_lo(), + ts_hi(), + BusValue::constant(syscall_lo), + BusValue::constant(syscall_hi), + ], + )); + + // 2-4. Register reads at ts (mult = μ_first): x10 = state_ptr, + // x11 = data_ptr (= this row's block base, since SEQ = 0 on first rows), + // x12 = n_blocks. All pure 24-element reads (old == value). + interactions.push(BusInteraction::sender( + BusId::Memw, + mu_first(), + memw_read( + register_value(s_lo_plus(0), s_hi()), + 1, + BusValue::constant(2 * 10), + BusValue::constant(0), + ts_lo(), + ts_hi(), + 1, + 0, + ), + )); + interactions.push(BusInteraction::sender( + BusId::Memw, + mu_first(), + memw_read( + register_value(packed(cols::D_LO), packed(cols::D_HI)), + 1, + BusValue::constant(2 * 11), + BusValue::constant(0), + ts_lo(), + ts_hi(), + 1, + 0, + ), + )); + interactions.push(BusInteraction::sender( + BusId::Memw, + mu_first(), + memw_read( + register_value(packed(cols::N_LO), packed(cols::N_HI)), + 1, + BusValue::constant(2 * 12), + BusValue::constant(0), + ts_lo(), + ts_hi(), + 1, + 0, + ), + )); + + // 5. Chain receive (mult = μ − μ_first): + // [ts, seq, n, s_addr, block_base, state_in[200]]. + { + let mut values = vec![ts_lo(), ts_hi(), packed(cols::SEQ)]; + values.extend(chain_registers(0)); + for i in 0..200 { + values.push(packed(cols::STATE_IN + i)); + } + interactions.push(BusInteraction::receiver( + BusId::KeccakSponge, + Multiplicity::Diff(cols::MU, cols::MU_FIRST), + values, + )); + } + + // 6. Chain send (mult = μ − μ_last): + // [ts, seq + 1, n, s_addr, block_base + 136, state_out[200]]. + { + let mut values = vec![ + ts_lo(), + ts_hi(), + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::SEQ, + }, + LinearTerm::Constant(1), + ]), + ]; + values.extend(chain_registers(RATE_BYTES as i64)); + for i in 0..200 { + values.push(packed(cols::STATE_OUT + i)); + } + interactions.push(BusInteraction::sender( + BusId::KeccakSponge, + Multiplicity::Diff(cols::MU, cols::MU_LAST), + values, + )); + } + + // 7. Keccak bus: send (ts, round = 0, seq, absorbed_state[200]). + // The absorbed state is XORED over lanes 0..17 and STATE_IN pass-through + // over lanes 17..25. Element order must match KECCAK_RND's receiver: + // x outer, y inner, lane = x + 5y. + { + let mut values = vec![ts_lo(), ts_hi(), BusValue::constant(0), packed(cols::SEQ)]; + for x in 0..5 { + for y in 0..5 { + let lane = x + 5 * y; + for b in 0..8 { + let col = if lane < RATE_LANES { + cols::xored(lane, b) + } else { + cols::state_in(lane, b) + }; + values.push(packed(col)); + } + } + } + interactions.push(BusInteraction::sender(BusId::Keccak, mu(), values)); + } + + // 8. Keccak bus: receive (ts, round = 24, seq, state_out[200]). + { + let mut values = vec![ts_lo(), ts_hi(), BusValue::constant(24), packed(cols::SEQ)]; + for x in 0..5 { + for y in 0..5 { + let lane = x + 5 * y; + for b in 0..8 { + values.push(packed(cols::state_out(lane, b))); + } + } + } + interactions.push(BusInteraction::receiver(BusId::Keccak, mu(), values)); + } + + // 9. Absorb XORs (136, mult = μ): XORED[i] = STATE_IN[i] ^ BLOCK[i]. + // The lookup simultaneously range-checks both operands and pins the output. + for i in 0..RATE_BYTES { + interactions.push(BusInteraction::sender( + BusId::ByteAlu, + mu(), + vec![ + BusValue::constant(alu_op::XOR as u64), + packed(cols::STATE_IN + i), + packed(cols::BLOCK + i), + packed(cols::XORED + i), + ], + )); + } + + // 10. Alignment: s_addr[0] & 7 = 0 (mult = μ). + interactions.push(BusInteraction::sender( + BusId::ByteAlu, + mu(), + vec![ + BusValue::constant(alu_op::AND as u64), + packed(cols::s_addr(0)), + BusValue::constant(7), + BusValue::constant(0), + ], + )); + + // 11. Range-check the s_addr bytes (4 ARE_BYTES pairs, mult = μ): the + // cells feed the linear s_lo/s_hi recombines, so without per-byte checks + // a prover could encode non-byte values that keep the recombined field + // value (and hence the MEMW tuples) intact while dodging the alignment + // lookup (same rationale as the KECCAK core chip's addr checks). + for i in 0..4 { + interactions.push(BusInteraction::sender( + BusId::AreBytes, + mu(), + vec![packed(cols::s_addr(2 * i)), packed(cols::s_addr(2 * i + 1))], + )); + } + + // 12. Message dword reads (17, mult = μ): pure reads of block dword j at + // (D_LO + 8j, D_HI), timestamp ts. + for j in 0..RATE_LANES { + let base_lo = if j == 0 { + packed(cols::D_LO) + } else { + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::D_LO, + }, + LinearTerm::Constant((8 * j) as i64), + ]) + }; + interactions.push(BusInteraction::sender( + BusId::Memw, + mu(), + memw_read( + lane_bytes(cols::BLOCK, j), + 0, + base_lo, + packed(cols::D_HI), + ts_lo(), + ts_hi(), + 0, + 1, + ), + )); + } + + // 13. State lane reads (25, mult = μ_first): pure reads of the pre-call + // state at (s_lo + 8·lane, s_hi), timestamp ts. + for lane in 0..25 { + interactions.push(BusInteraction::sender( + BusId::Memw, + mu_first(), + memw_read( + lane_bytes(cols::STATE_IN, lane), + 0, + s_lo_plus((8 * lane) as i64), + s_hi(), + ts_lo(), + ts_hi(), + 0, + 1, + ), + )); + } + + // 14. State lane writes (25, mult = μ_last): write-only tuples of the + // final state at (s_lo + 8·lane, s_hi), timestamp ts + 1 (the MEMW table + // materializes old = the value the μ_first lane reads re-wrote at ts). + for lane in 0..25 { + interactions.push(BusInteraction::sender( + BusId::Memw, + mu_last(), + memw_write( + lane_bytes(cols::STATE_OUT, lane), + s_lo_plus((8 * lane) as i64), + s_hi(), + ts_lo_plus_1(), + ts_hi(), + ), + )); + } + + interactions +} + +// ========================================================================= +// Single-source constraint set (ConstraintBuilder front-end) +// ========================================================================= + +/// The KECCAK_SPONGE table's 7 transition constraints as a single +/// [`ConstraintSet`]: +/// - idx 0-2: `IS_BIT` on `μ`, `μ_first`, `μ_last` (unconditional; padding +/// rows are all-zero); +/// - idx 3: `(μ_first + μ_last)·(1 − μ) = 0` (bookends imply μ; a row may +/// be both when n = 1); +/// - idx 4: `μ_first · SEQ = 0` (a call's chain starts at block 0 — the +/// anchor of the `(ts, seq)` permutation keying, see the module docs); +/// - idx 5: `μ_last · (N_LO − SEQ − 1) = 0` (the call has exactly +/// `n_blocks` rows); +/// - idx 6: `μ_last · N_HI = 0` (pins the x12 WORDS, not the recombined +/// field value — closes the `N = n + p` mod-p alias). +/// +/// Everything else is bus-enforced: XOR/range checks via ByteAlu/AreBytes, +/// the chain increment via the `KeccakSponge` sender's `SEQ + 1` / +/// `D_LO + 136` linear elements, and the permutation via the Keccak bus. +#[derive(Clone, Copy)] +pub struct KeccakSpongeConstraints; + +impl ConstraintSet for KeccakSpongeConstraints { + fn eval>(&self, b: &mut B) { + // idx 0-2: IS_BIT on μ, μ_first, μ_last. + emit_is_bit(b, 0, cols::MU, None); + emit_is_bit(b, 1, cols::MU_FIRST, None); + emit_is_bit(b, 2, cols::MU_LAST, None); + + // idx 3: (μ_first + μ_last) · (1 − μ) = 0. + let one = b.one(); + let first = b.main(0, cols::MU_FIRST); + let last = b.main(0, cols::MU_LAST); + let mu = b.main(0, cols::MU); + b.emit_base(3, (first + last) * (one - mu)); + + // idx 4: μ_first · SEQ = 0. + let first = b.main(0, cols::MU_FIRST); + let seq = b.main(0, cols::SEQ); + b.emit_base(4, first * seq); + + // idx 5: μ_last · (N_LO − SEQ − 1) = 0. + let last = b.main(0, cols::MU_LAST); + let n_lo = b.main(0, cols::N_LO); + let seq = b.main(0, cols::SEQ); + let one = b.one(); + b.emit_base(5, last * (n_lo - seq - one)); + + // idx 6: μ_last · N_HI = 0. + let last = b.main(0, cols::MU_LAST); + let n_hi = b.main(0, cols::N_HI); + b.emit_base(6, last * n_hi); + } +} diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index 0a86e4149..7fe0ca7b7 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -37,6 +37,7 @@ pub mod halt; pub mod keccak; pub mod keccak_rc; pub mod keccak_rnd; +pub mod keccak_sponge; pub mod load; pub mod local_to_global; pub mod lt; diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 5ec9fa566..9c194219b 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -54,6 +54,7 @@ use super::halt; use super::keccak::{self, KeccakOperation}; use super::keccak_rc; use super::keccak_rnd::{self, KeccakRoundOperation}; +use super::keccak_sponge::{self, KeccakSpongeOperation}; use super::load::{self, LoadOperation}; use super::local_to_global; use super::lt::{self, LtOperation}; @@ -532,7 +533,7 @@ fn build_reg_fallback( /// MEMW and LOAD collection requires sequential processing with state tracking. /// /// Returns: (memw_buckets, load_ops, lt_ops, shift_ops, bitwise_ops, commit_ops, -/// keccak_ops, cpu32_ops, ecsm_ops, ecdas_ops) +/// keccak_ops, keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops) #[allow(clippy::type_complexity)] fn collect_ops_from_cpu( cpu_ops: &[CpuOperation], @@ -546,6 +547,7 @@ fn collect_ops_from_cpu( Vec, Vec, Vec, + Vec, Vec, Vec, Vec, @@ -557,6 +559,7 @@ fn collect_ops_from_cpu( let mut bitwise_ops = Vec::with_capacity(cpu_ops.len() * 4); let mut commit_ops = Vec::new(); let mut keccak_ops = Vec::new(); + let mut keccak_sponge_ops = Vec::new(); let mut cpu32_ops = Vec::new(); let mut ecsm_ops = Vec::new(); let mut ecdas_ops = Vec::new(); @@ -645,6 +648,16 @@ fn collect_ops_from_cpu( }); } + // Collect KeccakAbsorbBlocks ECALL operations: one KECCAK_SPONGE row + // per absorbed 136-byte block (collect_keccak_sponge_ops handles the + // MEMW ops and the memory/register state updates). + if op.ecall_keccak_absorb { + let (sponge_memw_ops, sponge_rows) = + collect_keccak_sponge_ops(op, memory_state, register_state); + memw.extend_ops(sponge_memw_ops); + keccak_sponge_ops.extend(sponge_rows); + } + // Collect ECSM ecall operations (memory I/O + the two table row sets) if op.ecall_ecsm { let (ecsm_memw, ecsm_op, ecdas_rows) = @@ -706,6 +719,7 @@ fn collect_ops_from_cpu( bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, @@ -1417,6 +1431,128 @@ fn collect_keccak_memw_ops( memw_ops } +/// Collect the MEMW ops and per-block table rows for a KeccakAbsorbBlocks +/// ECALL. Mirrors `keccak_sponge::bus_interactions` op-for-op: +/// +/// - at `ts`: three pure register reads (x10/x11/x12), 25 pure lane reads of +/// the pre-call state, and `n × 17` pure dword reads of the message blocks +/// (the executor rejects state/data overlap, so every `(address, ts)` pair +/// is unique); +/// - at `ts + 1`: 25 lane writes of the final state (write-only; `old` is the +/// value the lane reads re-wrote at `ts`). +/// +/// `n_blocks` is recovered from the x12 register state (the CPU log only +/// carries the state/data addresses), like the ECSM operand addresses. +fn collect_keccak_sponge_ops( + op: &CpuOperation, + memory_state: &mut MemoryState, + register_state: &mut RegisterState, +) -> (Vec, Vec) { + use super::keccak_sponge::RATE_BYTES; + + let ts = op.timestamp; + let state_addr = op.keccak_absorb_state_addr; + let data_addr = op.keccak_absorb_data_addr; + let n_blocks = register_state.read(12).0; + debug_assert!(n_blocks > 0, "executor rejects n_blocks = 0"); + + let mut memw_ops = Vec::with_capacity(3 + 25 + 25 + (n_blocks as usize) * 17); + + // Pure register reads of x10/x11/x12 at ts (value re-written unchanged so + // the register's timestamp advances, as in the other accelerator arms). + for (reg, expected) in [(10u8, state_addr), (11, data_addr), (12, n_blocks)] { + let (val, old_ts) = register_state.read(reg); + debug_assert_eq!(val, expected, "sponge ecall register x{reg} drifted"); + let value = pack_register_value(val); + memw_ops.push( + MemwOperation::new(true, 2 * reg as u64, value, ts, 2, true) + .with_old(value, [old_ts, old_ts, 0, 0, 0, 0, 0, 0]), + ); + register_state.write(reg, val, ts); + } + + let overflow_msg = "keccak-absorb address ranges must be validated by the executor"; + + // Pure lane reads of the pre-call state at ts. + let mut state = [0u64; 25]; + for (lane, slot) in state.iter_mut().enumerate() { + let lane_addr = state_addr.checked_add(lane as u64 * 8).expect(overflow_msg); + let (values, old_ts) = memory_state.read_bytes(lane_addr, 8); + let mut dword = 0u64; + for (b, &v) in values.iter().enumerate() { + dword |= (v as u64) << (b * 8); + } + memw_ops + .push(MemwOperation::new(false, lane_addr, values, ts, 8, true).with_old(values, old_ts)); + memory_state.write_bytes(lane_addr, dword, 8, ts); + *slot = dword; + } + + // Per block: 17 pure dword reads at ts, then XOR + permute. + let mut sponge_ops = Vec::with_capacity(n_blocks as usize); + for k in 0..n_blocks { + let block_addr = data_addr + .checked_add(k * RATE_BYTES as u64) + .expect(overflow_msg); + let mut block = [0u8; RATE_BYTES]; + for j in 0..17u64 { + let dword_addr = block_addr.checked_add(j * 8).expect(overflow_msg); + let (values, old_ts) = memory_state.read_bytes(dword_addr, 8); + let mut dword = 0u64; + for (b, &v) in values.iter().enumerate() { + dword |= (v as u64) << (b * 8); + block[(j as usize) * 8 + b] = v as u8; + } + memw_ops.push( + MemwOperation::new(false, dword_addr, values, ts, 8, true) + .with_old(values, old_ts), + ); + memory_state.write_bytes(dword_addr, dword, 8, ts); + } + + let state_in = state; + for (j, lane) in state.iter_mut().take(17).enumerate() { + let mut m = 0u64; + for b in 0..8 { + m |= (block[j * 8 + b] as u64) << (b * 8); + } + *lane ^= m; + } + executor::vm::instruction::execution::keccak_f1600(&mut state); + + sponge_ops.push(KeccakSpongeOperation { + timestamp: ts, + seq: k, + n_blocks, + state_addr, + block_addr, + state_in, + block, + state_out: state, + first: k == 0, + last: k == n_blocks - 1, + }); + } + + // Lane writes of the final state at ts + 1 (old = the value the lane + // reads above re-wrote at ts). + for (lane, &out) in state.iter().enumerate() { + let lane_addr = state_addr.checked_add(lane as u64 * 8).expect(overflow_msg); + let mut value = [0u32; 8]; + for (b, v) in value.iter_mut().enumerate() { + *v = ((out >> (b * 8)) & 0xFF) as u32; + } + let (old_vals, old_ts) = memory_state.read_bytes(lane_addr, 8); + debug_assert_eq!(old_ts, [ts; 8], "state lanes were re-written at ts above"); + memw_ops.push( + MemwOperation::new(false, lane_addr, value, ts + 1, 8, false).with_old(old_vals, old_ts), + ); + memory_state.write_bytes(lane_addr, out, 8, ts + 1); + } + + (memw_ops, sponge_ops) +} + /// /// From spec memw.md: /// - MEMW-C4 through MEMW-C7: old_timestamp[i] < timestamp (based on width) @@ -2342,8 +2478,6 @@ pub(crate) fn collect_bitwise_from_ecdas(ops: &[ecdas::EcdasOperation]) -> Vec Vec { - use executor::vm::instruction::execution::{KECCAK_RC, KECCAK_RHO}; - let mut ops = Vec::new(); for kop in keccak_ops { @@ -2385,7 +2519,22 @@ pub(crate) fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec } // Replay keccak round computation to extract bitwise lookups - let mut state = kop.input; + push_keccak_round_bitwise(&kop.input, &mut ops); + } + + ops +} + +/// Replay one keccak-f[1600] permutation (24 rounds) and push the BYTE_ALU / +/// ARE_BYTES lookups the KECCAK_RND chip sends for it. Shared by the classic +/// KECCAK core collector and the KECCAK_SPONGE collector — both drive the same +/// round chip, one permutation per (core row / absorbed block). +#[allow(clippy::needless_range_loop)] +pub(crate) fn push_keccak_round_bitwise(input: &[u64; 25], ops: &mut Vec) { + use executor::vm::instruction::execution::{KECCAK_RC, KECCAK_RHO}; + + { + let mut state = *input; for round in 0..24 { // --- theta: Cxz chain BYTE_ALU[XOR] (160) --- let mut cxz = [[[0u8; 8]; 4]; 5]; @@ -2575,6 +2724,67 @@ pub(crate) fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec state = chi_lanes; } } +} + +/// Collect BITWISE lookups generated by the KECCAK_SPONGE chip. +/// +/// Mirrors `keccak_sponge::bus_interactions` send-for-send, per row (= per +/// absorbed block): +/// - 136 `BYTE_ALU[XOR]` for `xored = state_in ^ block` over the absorbed +/// region; +/// - 1 `BYTE_ALU[AND]` alignment check on `s_addr[0] & 7`; +/// - 4 paired `ARE_BYTES` on the `s_addr` bytes; +/// - the 24-round replay of the ABSORBED state (the round chip's lookups for +/// this block's permutation), shared with the classic collector via +/// [`push_keccak_round_bitwise`]. +/// +/// No IS_HALF lookups: the sponge chip uses linear low-limb addressing (see +/// its module docs), not the KECCAK core chip's DWordHL pointer apparatus. +pub(crate) fn collect_bitwise_from_keccak_sponge( + ops_in: &[KeccakSpongeOperation], +) -> Vec { + let mut ops = Vec::new(); + + for sop in ops_in { + // Alignment: s_addr[0] & 7 = 0. + ops.push(BitwiseOperation::byte_op( + BitwiseOperationType::ByteAluAnd, + (sop.state_addr & 0xFF) as u8, + 7, + )); + + // s_addr byte range checks, paired as (s_addr[2i], s_addr[2i+1]). + for i in 0..4 { + let lo = ((sop.state_addr >> (2 * i * 8)) & 0xFF) as u8; + let hi = ((sop.state_addr >> ((2 * i + 1) * 8)) & 0xFF) as u8; + ops.push(BitwiseOperation::byte_op( + BitwiseOperationType::AreBytes, + lo, + hi, + )); + } + + // Absorb XORs: xored[i] = state_in[i] ^ block[i] over 136 bytes. + let mut absorbed = sop.state_in; + for (i, &m) in sop.block.iter().enumerate() { + let s = ((sop.state_in[i / 8] >> ((i % 8) * 8)) & 0xFF) as u8; + ops.push(BitwiseOperation::byte_op( + BitwiseOperationType::ByteAluXor, + s, + m, + )); + } + for (j, lane) in absorbed.iter_mut().take(17).enumerate() { + let mut m = 0u64; + for b in 0..8 { + m |= (sop.block[j * 8 + b] as u64) << (b * 8); + } + *lane ^= m; + } + + // The round chip's lookups for this block's permutation. + push_keccak_round_bitwise(&absorbed, &mut ops); + } ops } @@ -2761,6 +2971,9 @@ pub struct Traces { /// KECCAK_RC precomputed round constant table (32 rows) pub keccak_rc: TraceTable, + /// KECCAK_SPONGE absorb table (one row per absorbed 136-byte block) + pub keccak_sponge: TraceTable, + /// ECSM core table (one row per scalar-multiplication ecall) pub ecsm: TraceTable, @@ -2801,6 +3014,7 @@ struct CollectedOps { dvrm_ops: Vec<(DvrmOperation, bool)>, commit_ops: Vec, keccak_ops: Vec, + keccak_sponge_ops: Vec, // Auxiliary ALU / memory / CPU32 dispatch chips (driven by the CPU ALU/MEMORY dispatch). eq_ops: Vec, bytewise_ops: Vec, @@ -2860,6 +3074,7 @@ fn collect_all_ops( mut bitwise_ops: Vec, commit_ops: Vec, keccak_ops: Vec, + keccak_sponge_ops: Vec, cpu32_ops: Vec, ecsm_ops: Vec, ecdas_ops: Vec, @@ -2999,6 +3214,7 @@ fn collect_all_ops( dvrm_ops, commit_ops, keccak_ops, + keccak_sponge_ops, eq_ops, bytewise_ops, store_ops, @@ -3042,6 +3258,7 @@ fn build_traces( dvrm_ops, commit_ops, keccak_ops, + keccak_sponge_ops, eq_ops, bytewise_ops, store_ops, @@ -3121,6 +3338,7 @@ fn build_traces( Box::new(|h| h.add_ops(&collect_bitwise_from_memw_aligned(&memw_aligned_ops))), Box::new(|h| h.add_ops(&collect_bitwise_from_commit(&commit_ops))), Box::new(|h| h.add_ops(&collect_bitwise_from_keccak(&keccak_ops))), + Box::new(|h| h.add_ops(&collect_bitwise_from_keccak_sponge(&keccak_sponge_ops))), Box::new(|h| h.add_ops(&collect_bitwise_from_ecsm(&ecsm_ops))), Box::new(|h| h.add_ops(&collect_bitwise_from_ecdas(&ecdas_ops))), Box::new(|h| add_padding_byte_checks(h, num_padding_rows)), @@ -3379,20 +3597,47 @@ fn build_traces( }; let gen_commit = || commit::generate_commit_trace(&commit_ops); let gen_keccak = || keccak::generate_keccak_trace(&keccak_ops); + let gen_keccak_sponge = || keccak_sponge::generate_keccak_sponge_trace(&keccak_sponge_ops); + // The round chip serves BOTH keccak front-ends: one permutation per classic + // core row (seq = 0) and one per sponge block (seq = the block index; the + // absorbed state — state_in XOR block over lanes 0..17 — is the round + // chip's input, matching the sponge chip's round-0 Keccak-bus send). let gen_keccak_rnd = || { - let keccak_rnd_ops: Vec = keccak_ops - .iter() - .map(|op| KeccakRoundOperation { + let mut keccak_rnd_ops: Vec = Vec::with_capacity( + keccak_ops.len() + keccak_sponge_ops.len(), + ); + keccak_rnd_ops.extend(keccak_ops.iter().map(|op| KeccakRoundOperation { + timestamp: op.timestamp, + seq: 0, + input: op.input, + output: op.output, + })); + keccak_rnd_ops.extend(keccak_sponge_ops.iter().map(|op| { + let mut absorbed = op.state_in; + for (j, lane) in absorbed.iter_mut().take(17).enumerate() { + let mut m = 0u64; + for b in 0..8 { + m |= (op.block[j * 8 + b] as u64) << (b * 8); + } + *lane ^= m; + } + KeccakRoundOperation { timestamp: op.timestamp, - input: op.input, - output: op.output, - }) - .collect(); + seq: op.seq, + input: absorbed, + output: op.state_out, + } + })); keccak_rnd::generate_keccak_rnd_trace(&keccak_rnd_ops) }; let gen_keccak_rc = || { let mut keccak_rc_trace = keccak_rc::generate_keccak_rc_trace(); - keccak_rc::update_multiplicities(&mut keccak_rc_trace, keccak_ops.len()); + // One permutation (= 24 round-constant lookups) per classic core row + // AND per sponge block. + keccak_rc::update_multiplicities( + &mut keccak_rc_trace, + keccak_ops.len() + keccak_sponge_ops.len(), + ); keccak_rc_trace }; let gen_pages = || match initial_image { @@ -3417,6 +3662,7 @@ fn build_traces( (None, None, None, None); let (mut commit_slot, mut keccak_slot, mut keccak_rnd_slot, mut keccak_rc_slot) = (None, None, None, None); + let mut keccak_sponge_slot = None; let (mut pages_slot, mut register_slot, mut halt_slot) = (None, None, None); let (mut eqs_slot, mut bytewises_slot, mut stores_slot, mut cpu32s_slot) = (None, None, None, None); @@ -3453,6 +3699,7 @@ fn build_traces( spawn_into!(keccak_slot, gen_keccak); spawn_into!(keccak_rnd_slot, gen_keccak_rnd); spawn_into!(keccak_rc_slot, gen_keccak_rc); + spawn_into!(keccak_sponge_slot, gen_keccak_sponge); spawn_into!(commit_slot, gen_commit); spawn_into!(register_slot, gen_register); spawn_into!(halt_slot, gen_halt); @@ -3480,6 +3727,7 @@ fn build_traces( keccak_slot = Some(gen_keccak()); keccak_rnd_slot = Some(gen_keccak_rnd()); keccak_rc_slot = Some(gen_keccak_rc()); + keccak_sponge_slot = Some(gen_keccak_sponge()); pages_slot = Some(gen_pages()); register_slot = Some(gen_register()); halt_slot = Some(gen_halt()); @@ -3515,6 +3763,7 @@ fn build_traces( let keccak_trace = keccak_slot.expect(PHASE5_RAN); let keccak_rnd_trace = keccak_rnd_slot.expect(PHASE5_RAN); let keccak_rc_trace = keccak_rc_slot.expect(PHASE5_RAN); + let keccak_sponge_trace = keccak_sponge_slot.expect(PHASE5_RAN); #[allow(unused_mut)] let (mut pages, page_configs) = pages_slot.expect(PHASE5_RAN); #[allow(unused_mut)] @@ -3588,6 +3837,7 @@ fn build_traces( keccak: keccak_trace, keccak_rnd: keccak_rnd_trace, keccak_rc: keccak_rc_trace, + keccak_sponge: keccak_sponge_trace, ecsm: ecsm_trace, ecdas: ecdas_trace, memw_registers, @@ -3856,6 +4106,7 @@ impl Traces { use super::keccak_rc::NUM_PRECOMPUTED_COLS as KECCAK_RC_PRECOMPUTED; use super::keccak_rc::cols::NUM_COLUMNS as KECCAK_RC_COLS; use super::keccak_rnd::cols::NUM_COLUMNS as KECCAK_RND_COLS; + use super::keccak_sponge::cols::NUM_COLUMNS as KECCAK_SPONGE_COLS; use super::load::cols::NUM_COLUMNS as LOAD_COLS; use super::lt::cols::NUM_COLUMNS as LT_COLS; use super::memw::cols::NUM_COLUMNS as MEMW_COLS; @@ -3888,6 +4139,7 @@ impl Traces { keccak, keccak_rnd, keccak_rc, + keccak_sponge, ecsm, ecdas, memw_registers, @@ -3943,6 +4195,7 @@ impl Traces { total += (keccak.num_rows() * KECCAK_COLS) as u64; total += (keccak_rnd.num_rows() * KECCAK_RND_COLS) as u64; total += (keccak_rc.num_rows() * (KECCAK_RC_COLS - KECCAK_RC_PRECOMPUTED)) as u64; + total += (keccak_sponge.num_rows() * KECCAK_SPONGE_COLS) as u64; for t in eqs { total += (t.num_rows() * EQ_COLS) as u64; } @@ -3992,6 +4245,7 @@ impl Traces { let n_keccak = aux_cols(super::keccak::bus_interactions().len()); let n_keccak_rnd = aux_cols(super::keccak_rnd::bus_interactions().len()); let n_keccak_rc = aux_cols(super::keccak_rc::bus_interactions().len()); + let n_keccak_sponge = aux_cols(super::keccak_sponge::bus_interactions().len()); let n_eq = aux_cols(super::eq::bus_interactions().len()); let n_bytewise = aux_cols(super::bytewise::bus_interactions().len()); let n_store = aux_cols(super::store::bus_interactions().len()); @@ -4018,6 +4272,7 @@ impl Traces { keccak, keccak_rnd, keccak_rc, + keccak_sponge, ecsm, ecdas, memw_registers, @@ -4073,6 +4328,7 @@ impl Traces { total += (keccak.num_rows() * n_keccak) as u64; total += (keccak_rnd.num_rows() * n_keccak_rnd) as u64; total += (keccak_rc.num_rows() * n_keccak_rc) as u64; + total += (keccak_sponge.num_rows() * n_keccak_sponge) as u64; for t in eqs { total += (t.num_rows() * n_eq) as u64; } @@ -4357,6 +4613,7 @@ impl Traces { bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, @@ -4375,6 +4632,7 @@ impl Traces { bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, @@ -4468,6 +4726,7 @@ impl Traces { bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, @@ -4482,6 +4741,7 @@ impl Traces { bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index fab4aabff..c708aa98b 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -314,7 +314,11 @@ pub enum BusId { /// COMMIT output bus: verifier computes the receiver contribution externally /// from `VmProof.public_output` using the shared LogUp challenges Commit = 21, - /// Keccak core ↔ round chip: (timestamp, round, state[200 bytes]) + /// Keccak core/sponge ↔ round chip: (timestamp, round, seq, state[200 bytes]). + /// `seq` keys the permutation within one ecall: the classic core chip + /// always sends 0; KECCAK_SPONGE sends the block index (all blocks of one + /// absorb call share the ecall's timestamp, so without `seq` two blocks' + /// permutation outputs could be swapped with the bus still balancing). Keccak = 22, /// Keccak round ↔ RC lookup: (round, rc[8 bytes]) KeccakRc = 23, @@ -359,6 +363,16 @@ pub enum BusId { /// Cross-epoch memory bus: the local-to-global table's per-cell init/fini /// boundary claims, matched across epochs by the final aggregation LogUp. GlobalMemory = 31, + + // ========================================================================= + // Keccak sponge absorb accelerator + // ========================================================================= + /// KECCAK_SPONGE self-referential block chain: row k of an absorb call + /// hands the permuted state (plus the call's registers) to row k+1 as + /// `(timestamp, seq+1, n, state_ptr, block_base+136, state[200 bytes])`. + /// The `(timestamp, seq)` key makes every link of one call unique — see + /// the swap-attack note in `tables::keccak_sponge`. + KeccakSponge = 32, } impl BusId { @@ -388,6 +402,7 @@ impl BusId { BusId::Ecdas => "Ecdas", BusId::Bit => "Bit", BusId::GlobalMemory => "GlobalMemory", + BusId::KeccakSponge => "KeccakSponge", } } } @@ -420,6 +435,7 @@ impl TryFrom for BusId { 28 => Ok(BusId::Ecdas), 30 => Ok(BusId::Bit), 31 => Ok(BusId::GlobalMemory), + 32 => Ok(BusId::KeccakSponge), other => Err(other), } } diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index d7969612f..b0998d652 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -75,6 +75,10 @@ use crate::tables::keccak_rc::{ use crate::tables::keccak_rnd::{ KeccakRndConstraints, bus_interactions as keccak_rnd_bus_interactions, cols as keccak_rnd_cols, }; +use crate::tables::keccak_sponge::{ + KeccakSpongeConstraints, bus_interactions as keccak_sponge_bus_interactions, + cols as keccak_sponge_cols, +}; use crate::tables::load::{ LoadConstraints, bus_interactions as load_bus_interactions, cols as load_cols, }; @@ -978,6 +982,20 @@ pub fn create_keccak_rc_air(proof_options: &ProofOptions) -> ConcreteVmAir ConcreteVmAir { + build_air( + keccak_sponge_cols::NUM_COLUMNS, + keccak_sponge_bus_interactions(), + proof_options, + 1, + KeccakSpongeConstraints, + "KECCAK_SPONGE", + ) +} + /// Create ECSM core AIR (secp256k1 scalar-multiplication orchestrator). pub fn create_ecsm_air(proof_options: &ProofOptions) -> ConcreteVmAir { build_air( diff --git a/prover/src/tests/constraint_program_device_tests.rs b/prover/src/tests/constraint_program_device_tests.rs index a2863b2f0..1532408e1 100644 --- a/prover/src/tests/constraint_program_device_tests.rs +++ b/prover/src/tests/constraint_program_device_tests.rs @@ -179,6 +179,7 @@ fn all_table_programs_lower_and_match_folders() { check_air_device(&create_keccak_air(&opts), "KECCAK"); check_air_device(&create_keccak_rnd_air(&opts), "KECCAK_RND"); check_air_device(&create_keccak_rc_air(&opts), "KECCAK_RC"); + check_air_device(&create_keccak_sponge_air(&opts), "KECCAK_SPONGE"); check_air_device(&create_ecsm_air(&opts), "ECSM"); check_air_device(&create_ecdas_air(&opts), "ECDAS"); } diff --git a/prover/src/tests/constraint_program_tests.rs b/prover/src/tests/constraint_program_tests.rs index 3ae46494d..e0e858e78 100644 --- a/prover/src/tests/constraint_program_tests.rs +++ b/prover/src/tests/constraint_program_tests.rs @@ -177,6 +177,7 @@ fn all_table_programs_match_folders() { check_air(&create_keccak_air(&opts), "KECCAK"); check_air(&create_keccak_rnd_air(&opts), "KECCAK_RND"); check_air(&create_keccak_rc_air(&opts), "KECCAK_RC"); + check_air(&create_keccak_sponge_air(&opts), "KECCAK_SPONGE"); check_air(&create_ecsm_air(&opts), "ECSM"); check_air(&create_ecdas_air(&opts), "ECDAS"); } diff --git a/prover/src/tests/constraint_set_tests_b.rs b/prover/src/tests/constraint_set_tests_b.rs index 0348c2b70..64f2b42f1 100644 --- a/prover/src/tests/constraint_set_tests_b.rs +++ b/prover/src/tests/constraint_set_tests_b.rs @@ -269,6 +269,20 @@ mod keccak_rnd { } } +// ============================================================================= +// keccak_sponge.rs +// ============================================================================= + +mod keccak_sponge { + use super::*; + use crate::tables::keccak_sponge::{KeccakSpongeConstraints, cols}; + + #[test] + fn keccak_sponge_constraint_set_folder_capture_agree() { + check_table("keccak_sponge", &KeccakSpongeConstraints, cols::NUM_COLUMNS); + } +} + // ============================================================================= // cpu32.rs // ============================================================================= diff --git a/prover/src/tests/keccak_rnd_tests.rs b/prover/src/tests/keccak_rnd_tests.rs index 230ef6065..e3069b5d7 100644 --- a/prover/src/tests/keccak_rnd_tests.rs +++ b/prover/src/tests/keccak_rnd_tests.rs @@ -17,6 +17,7 @@ fn test_pi_virtual_matches_rotate() { keccak_f1600(&mut output); let op = KeccakRoundOperation { timestamp: 42, + seq: 0, input, output, }; diff --git a/prover/src/tests/keccak_sponge_tests.rs b/prover/src/tests/keccak_sponge_tests.rs new file mode 100644 index 000000000..c133a01c8 --- /dev/null +++ b/prover/src/tests/keccak_sponge_tests.rs @@ -0,0 +1,250 @@ +//! KECCAK_SPONGE chip unit tests. +//! +//! The main test is a full sender ↔ collector **multiset equality**: the +//! BITWISE lookups tallied by `collect_bitwise_from_keccak_sponge` (which fill +//! the BITWISE table's multiplicities) must equal, as a multiset of concrete +//! `(bus, tuple)` values, exactly what the KECCAK_SPONGE chip and the +//! KECCAK_RND rows it drives *send* on the ByteAlu/AreBytes buses — evaluated +//! off the real generated traces, not re-derived from the op structure. Any +//! drift between `bus_interactions()` and the collector leaves those buses +//! unbalanced and every sponge proof invalid. + +use std::collections::HashMap; + +use stark::lookup::{BusValue, LinearTerm, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use crate::tables::bitwise::{BitwiseOperation, BitwiseOperationType}; +use crate::tables::keccak_rnd::{self, KeccakRoundOperation}; +use crate::tables::keccak_sponge::{ + self, KeccakSpongeOperation, RATE_BYTES, generate_keccak_sponge_trace, +}; +use crate::tables::trace_builder::collect_bitwise_from_keccak_sponge; +use crate::tables::types::{BusId, FE, GoldilocksExtension, GoldilocksField, alu_op}; + +/// Deterministic SplitMix64. +struct SplitMix64(u64); +impl SplitMix64 { + fn next_u64(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } +} + +/// Build one synthetic absorb call of `n_blocks` blocks with seeded +/// pseudo-random state and data, using the executor's permutation (the same +/// construction as `collect_keccak_sponge_ops`). +fn synthetic_call(n_blocks: u64, timestamp: u64, seed: u64) -> Vec { + let mut rng = SplitMix64(seed); + let state_addr = 0x0001_2340u64; + let data_addr = 0x0002_0000u64; + + let mut state: [u64; 25] = core::array::from_fn(|i| rng.next_u64() ^ (i as u64)); + let mut ops = Vec::with_capacity(n_blocks as usize); + for k in 0..n_blocks { + let mut block = [0u8; RATE_BYTES]; + for chunk in block.chunks_mut(8) { + chunk.copy_from_slice(&rng.next_u64().to_le_bytes()); + } + let state_in = state; + for (j, lane) in state.iter_mut().take(17).enumerate() { + let mut m = 0u64; + for b in 0..8 { + m |= (block[j * 8 + b] as u64) << (b * 8); + } + *lane ^= m; + } + executor::vm::instruction::execution::keccak_f1600(&mut state); + ops.push(KeccakSpongeOperation { + timestamp, + seq: k, + n_blocks, + state_addr, + block_addr: data_addr + k * RATE_BYTES as u64, + state_in, + block, + state_out: state, + first: k == 0, + last: k == n_blocks - 1, + }); + } + ops +} + +/// Evaluate one bus element on a trace row. +fn eval_bus_value( + v: &BusValue, + trace: &TraceTable, + row: usize, +) -> FE { + match v { + BusValue::Packed { + start_column, + packing: Packing::Direct, + } => *trace.get_main(row, *start_column), + BusValue::Packed { .. } => panic!("unexpected non-Direct packing in a lookup tuple"), + BusValue::Linear(terms) => terms.iter().fold(FE::zero(), |acc, t| { + acc + match t { + LinearTerm::Column { + coefficient, + column, + } => { + let cell = *trace.get_main(row, *column); + if *coefficient >= 0 { + cell * FE::from(*coefficient as u64) + } else { + -(cell * FE::from(coefficient.unsigned_abs())) + } + } + LinearTerm::ColumnUnsigned { + coefficient, + column, + } => *trace.get_main(row, *column) * FE::from(*coefficient), + LinearTerm::Constant(c) => { + if *c >= 0 { + FE::from(*c as u64) + } else { + -FE::from(c.unsigned_abs()) + } + } + } + }), + } +} + +type LookupKey = (u64, Vec); + +/// Tally every ByteAlu/AreBytes SEND of `interactions` evaluated over the +/// real rows of `trace` into `sends` (key = (bus_id, canonical tuple)). +fn tally_lookup_sends( + interactions: &[stark::lookup::BusInteraction], + trace: &TraceTable, + sends: &mut HashMap, +) { + let lookup_buses = [BusId::ByteAlu as u64, BusId::AreBytes as u64]; + for interaction in interactions { + if !lookup_buses.contains(&interaction.bus_id) { + continue; + } + assert!(interaction.is_sender, "lookup interactions are sends"); + let mult_col = match interaction.multiplicity { + Multiplicity::Column(c) => c, + _ => panic!("sponge/rnd lookup sends use Multiplicity::Column"), + }; + for row in 0..trace.num_rows() { + let mult = trace.get_main(row, mult_col).canonical_u64(); + if mult == 0 { + continue; + } + let tuple: Vec = interaction + .values + .iter() + .map(|v| eval_bus_value(v, trace, row).canonical_u64()) + .collect(); + *sends.entry((interaction.bus_id, tuple)).or_default() += mult as i64; + } + } +} + +/// Canonicalize a collected `BitwiseOperation` into the same key space as the +/// evaluated sends. +fn collected_key(op: &BitwiseOperation) -> LookupKey { + let (x, y) = (op.x as u64, op.y as u64); + match op.lookup_type { + BitwiseOperationType::ByteAluXor => ( + BusId::ByteAlu as u64, + vec![alu_op::XOR as u64, x, y, x ^ y], + ), + BitwiseOperationType::ByteAluAnd => ( + BusId::ByteAlu as u64, + vec![alu_op::AND as u64, x, y, x & y], + ), + BitwiseOperationType::AreBytes => (BusId::AreBytes as u64, vec![x, y]), + other => panic!("KECCAK_SPONGE collector emitted unexpected lookup type {other:?}"), + } +} + +/// The multiset of BITWISE lookups the collector tallies must equal the +/// multiset the KECCAK_SPONGE chip + its KECCAK_RND rows actually send, +/// evaluated off the generated traces. Exercises multi-block calls (bookend +/// rows AND interior rows) plus an n = 1 call (a row that is both first and +/// last) sharing the table with it. +#[test] +fn sponge_bitwise_multiset_matches_chip_sends() { + let mut ops = synthetic_call(3, 4, 0x5EED_0001); + ops.extend(synthetic_call(1, 8, 0x5EED_0002)); + + // The KECCAK_RND rows this sponge workload drives: one permutation per + // block, input = the absorbed state (mirrors `gen_keccak_rnd`). + let rnd_ops: Vec = ops + .iter() + .map(|op| { + let mut absorbed = op.state_in; + for (j, lane) in absorbed.iter_mut().take(17).enumerate() { + let mut m = 0u64; + for b in 0..8 { + m |= (op.block[j * 8 + b] as u64) << (b * 8); + } + *lane ^= m; + } + KeccakRoundOperation { + timestamp: op.timestamp, + seq: op.seq, + input: absorbed, + output: op.state_out, + } + }) + .collect(); + + let sponge_trace = generate_keccak_sponge_trace(&ops); + let rnd_trace = keccak_rnd::generate_keccak_rnd_trace(&rnd_ops); + + let mut sends: HashMap = HashMap::new(); + tally_lookup_sends(&keccak_sponge::bus_interactions(), &sponge_trace, &mut sends); + tally_lookup_sends(&keccak_rnd::bus_interactions(), &rnd_trace, &mut sends); + + let mut collected: HashMap = HashMap::new(); + for op in collect_bitwise_from_keccak_sponge(&ops) { + *collected.entry(collected_key(&op)).or_default() += 1; + } + + // Compare as full multisets, reporting the first divergence legibly. + for (key, &count) in &sends { + assert_eq!( + collected.get(key).copied().unwrap_or(0), + count, + "collector under/over-tallies chip send {key:?}" + ); + } + for (key, &count) in &collected { + assert_eq!( + sends.get(key).copied().unwrap_or(0), + count, + "collector tallies a lookup the chip never sends: {key:?}" + ); + } +} + +/// The sponge chip must not send IS_HALF (it uses linear low-limb addressing, +/// not the KECCAK core chip's DWordHL pointer apparatus), and the collector +/// must mirror that. +#[test] +fn sponge_sends_no_is_half() { + let is_half = BusId::IsHalfword as u64; + assert!( + keccak_sponge::bus_interactions() + .iter() + .all(|i| i.bus_id != is_half), + "sponge chip unexpectedly sends IS_HALF" + ); + let ops = synthetic_call(2, 4, 0x5EED_0003); + assert!( + collect_bitwise_from_keccak_sponge(&ops) + .iter() + .all(|op| op.lookup_type != BitwiseOperationType::IsHalf), + "sponge collector unexpectedly tallies IS_HALF" + ); +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index a3326bcd1..7a38c0298 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -51,6 +51,8 @@ pub mod ir_stats_dump; #[cfg(test)] pub mod keccak_rnd_tests; #[cfg(test)] +pub mod keccak_sponge_tests; +#[cfg(test)] pub mod load_tests; #[cfg(test)] pub mod local_to_global_bus_tests; diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index ffe9071b2..5bc8df7c5 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1102,6 +1102,49 @@ fn test_prove_elfs_keccak_multi_call() { ); } +#[test] +fn test_prove_elfs_keccak_absorb() { + let _ = env_logger::builder().is_test(true).try_init(); + + let elf_bytes = crate::test_utils::asm_elf_bytes("test_keccak_absorb"); + let elf = Elf::load(&elf_bytes).expect("Failed to load ELF"); + let executor = + executor::vm::execution::Executor::new(&elf, vec![]).expect("Failed to create executor"); + let result = executor.run().expect("Failed to run program"); + + // The guest seeds lane[i] = i + 1, seeds 3 rate blocks with dword[k] = + // k + 100 and absorbs all three in ONE ecall. Cross-check the committed + // state against an independent sponge replay over tiny-keccak. + let mut expected_state: [u64; 25] = core::array::from_fn(|i| (i + 1) as u64); + for k in 0..3u64 { + for (j, lane) in expected_state.iter_mut().take(17).enumerate() { + *lane ^= 100 + k * 17 + j as u64; + } + tiny_keccak::keccakf(&mut expected_state); + } + let mut expected_bytes = Vec::with_capacity(200); + for lane in expected_state { + expected_bytes.extend_from_slice(&lane.to_le_bytes()); + } + assert_eq!( + result.return_values.memory_values, expected_bytes, + "committed state must match a tiny-keccak sponge replay over 3 absorbed blocks" + ); + + // Must use from_elf_and_logs (stack RAM needs PAGE tables, like keccak). + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); + assert_eq!( + traces.public_output_bytes, + result.return_values.memory_values + ); + + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "keccak absorb prove/verify failed" + ); +} + #[test] fn test_prove_elfs_ecsm() { let _ = env_logger::builder().is_test(true).try_init(); diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index 428fd4700..637c3697d 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -589,6 +589,7 @@ mod keccak_tests { }; let rop = KeccakRoundOperation { timestamp: 42, + seq: 0, input, output, }; From f958f4c9c8ab4eac93c07c16aa1b857faffb5c7c Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 13:56:46 -0300 Subject: [PATCH 4/6] chore(bench,lint): keccak-absorb bench guest generator + fmt/clippy cleanup scripts/gen_keccak_absorb_bench.sh builds a sponge-saturated guest: CALLS absorb ecalls of DATA_BLOCKS blocks each (all blocks through ONE ecall, ~7-cycle loop body), state chained across calls, output committed, count-gated via the CLI's 'KeccakAbsorb calls' line. KECCAK_SPONGE commits one row per block, so sweep points are CALLS x DATA_BLOCKS = 2^k. Smoke-tested: 4x8 build executes with 'KeccakAbsorb calls: 4' at 691 cycles. Also: cargo fmt over the touched packages and an allow(too_many_arguments) on the sponge memw_read helper (mirrors the ecsm.rs helper it copies). --- executor/src/tests/keccak_absorb_tests.rs | 4 +- prover/src/tables/cpu.rs | 3 +- prover/src/tables/keccak_sponge.rs | 1 + prover/src/tables/trace_builder.rs | 16 +-- prover/src/tests/keccak_sponge_tests.rs | 20 ++-- scripts/gen_keccak_absorb_bench.sh | 119 ++++++++++++++++++++++ syscalls/src/syscalls.rs | 10 +- 7 files changed, 151 insertions(+), 22 deletions(-) create mode 100755 scripts/gen_keccak_absorb_bench.sh diff --git a/executor/src/tests/keccak_absorb_tests.rs b/executor/src/tests/keccak_absorb_tests.rs index 69bcc1844..cb27ba32c 100644 --- a/executor/src/tests/keccak_absorb_tests.rs +++ b/executor/src/tests/keccak_absorb_tests.rs @@ -110,7 +110,9 @@ fn test_absorb_matches_chained_permute_semantics() { let mut rng = SplitMix64(0xA11C_E000_0000_0200); let mut state: [u64; 25] = core::array::from_fn(|i| rng.next_u64() ^ (i as u64)); - let blocks: Vec<[u64; 17]> = (0..4).map(|_| core::array::from_fn(|_| rng.next_u64())).collect(); + let blocks: Vec<[u64; 17]> = (0..4) + .map(|_| core::array::from_fn(|_| rng.next_u64())) + .collect(); for block in &blocks { for (lane, &m) in state.iter_mut().zip(block.iter()) { *lane ^= m; diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index bff8f0c1f..5b5196b78 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -241,8 +241,7 @@ impl CpuOperation { f.ecall && log.src1_val == executor::vm::instruction::execution::KECCAK_SYSCALL_NUMBER; let keccak_state_addr = if ecall_keccak { log.src2_val } else { 0 }; let ecall_keccak_absorb = f.ecall - && log.src1_val - == executor::vm::instruction::execution::KECCAK_ABSORB_SYSCALL_NUMBER; + && log.src1_val == executor::vm::instruction::execution::KECCAK_ABSORB_SYSCALL_NUMBER; let (keccak_absorb_state_addr, keccak_absorb_data_addr) = if ecall_keccak_absorb { (log.src2_val, log.dst_val) } else { diff --git a/prover/src/tables/keccak_sponge.rs b/prover/src/tables/keccak_sponge.rs index aab4478a0..0bbcd31cd 100644 --- a/prover/src/tables/keccak_sponge.rs +++ b/prover/src/tables/keccak_sponge.rs @@ -319,6 +319,7 @@ fn s_hi() -> BusValue { /// `[old[8], is_register, base_lo, base_hi, value[8], ts_lo, ts_hi, w2, w4, w8]` /// — a 24-element MEMW **read** tuple (`old == value`), as in `ecsm.rs`. +#[allow(clippy::too_many_arguments)] fn memw_read( value: [BusValue; 8], is_register: u64, diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 9c194219b..0f9c0103d 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1482,8 +1482,9 @@ fn collect_keccak_sponge_ops( for (b, &v) in values.iter().enumerate() { dword |= (v as u64) << (b * 8); } - memw_ops - .push(MemwOperation::new(false, lane_addr, values, ts, 8, true).with_old(values, old_ts)); + memw_ops.push( + MemwOperation::new(false, lane_addr, values, ts, 8, true).with_old(values, old_ts), + ); memory_state.write_bytes(lane_addr, dword, 8, ts); *slot = dword; } @@ -1504,8 +1505,7 @@ fn collect_keccak_sponge_ops( block[(j as usize) * 8 + b] = v as u8; } memw_ops.push( - MemwOperation::new(false, dword_addr, values, ts, 8, true) - .with_old(values, old_ts), + MemwOperation::new(false, dword_addr, values, ts, 8, true).with_old(values, old_ts), ); memory_state.write_bytes(dword_addr, dword, 8, ts); } @@ -1545,7 +1545,8 @@ fn collect_keccak_sponge_ops( let (old_vals, old_ts) = memory_state.read_bytes(lane_addr, 8); debug_assert_eq!(old_ts, [ts; 8], "state lanes were re-written at ts above"); memw_ops.push( - MemwOperation::new(false, lane_addr, value, ts + 1, 8, false).with_old(old_vals, old_ts), + MemwOperation::new(false, lane_addr, value, ts + 1, 8, false) + .with_old(old_vals, old_ts), ); memory_state.write_bytes(lane_addr, out, 8, ts + 1); } @@ -3603,9 +3604,8 @@ fn build_traces( // absorbed state — state_in XOR block over lanes 0..17 — is the round // chip's input, matching the sponge chip's round-0 Keccak-bus send). let gen_keccak_rnd = || { - let mut keccak_rnd_ops: Vec = Vec::with_capacity( - keccak_ops.len() + keccak_sponge_ops.len(), - ); + let mut keccak_rnd_ops: Vec = + Vec::with_capacity(keccak_ops.len() + keccak_sponge_ops.len()); keccak_rnd_ops.extend(keccak_ops.iter().map(|op| KeccakRoundOperation { timestamp: op.timestamp, seq: 0, diff --git a/prover/src/tests/keccak_sponge_tests.rs b/prover/src/tests/keccak_sponge_tests.rs index c133a01c8..fc034f6bd 100644 --- a/prover/src/tests/keccak_sponge_tests.rs +++ b/prover/src/tests/keccak_sponge_tests.rs @@ -154,14 +154,12 @@ fn tally_lookup_sends( fn collected_key(op: &BitwiseOperation) -> LookupKey { let (x, y) = (op.x as u64, op.y as u64); match op.lookup_type { - BitwiseOperationType::ByteAluXor => ( - BusId::ByteAlu as u64, - vec![alu_op::XOR as u64, x, y, x ^ y], - ), - BitwiseOperationType::ByteAluAnd => ( - BusId::ByteAlu as u64, - vec![alu_op::AND as u64, x, y, x & y], - ), + BitwiseOperationType::ByteAluXor => { + (BusId::ByteAlu as u64, vec![alu_op::XOR as u64, x, y, x ^ y]) + } + BitwiseOperationType::ByteAluAnd => { + (BusId::ByteAlu as u64, vec![alu_op::AND as u64, x, y, x & y]) + } BitwiseOperationType::AreBytes => (BusId::AreBytes as u64, vec![x, y]), other => panic!("KECCAK_SPONGE collector emitted unexpected lookup type {other:?}"), } @@ -203,7 +201,11 @@ fn sponge_bitwise_multiset_matches_chip_sends() { let rnd_trace = keccak_rnd::generate_keccak_rnd_trace(&rnd_ops); let mut sends: HashMap = HashMap::new(); - tally_lookup_sends(&keccak_sponge::bus_interactions(), &sponge_trace, &mut sends); + tally_lookup_sends( + &keccak_sponge::bus_interactions(), + &sponge_trace, + &mut sends, + ); tally_lookup_sends(&keccak_rnd::bus_interactions(), &rnd_trace, &mut sends); let mut collected: HashMap = HashMap::new(); diff --git a/scripts/gen_keccak_absorb_bench.sh b/scripts/gen_keccak_absorb_bench.sh new file mode 100755 index 000000000..c014025ed --- /dev/null +++ b/scripts/gen_keccak_absorb_bench.sh @@ -0,0 +1,119 @@ +#!/usr/bin/env bash +# +# gen_keccak_absorb_bench.sh — generate + compile a keccak-sponge-absorb +# saturated guest. +# +# The guest seeds a 200-byte keccak state and a DATA_BLOCKS × 136-byte message +# region, then fires the absorb ecall (a7 = u64::MAX - 3, spec -4) CALLS times, +# absorbing ALL DATA_BLOCKS blocks through ONE ecall each time, commits the +# 200-byte state and halts. Total absorbed blocks (= KECCAK_SPONGE rows = +# permutations) is N = CALLS × DATA_BLOCKS. +# +# Why a loop of large calls: the accelerator's win is the per-block guest glue +# it deletes, so the interesting shape is few ecalls × many blocks — the loop +# body is ~7 cycles per CALL regardless of DATA_BLOCKS, keeping the trace +# sponge-saturated. The calls deliberately reuse the same data region (the +# prover's cost per block is identical either way — no layer dedupes rows, the +# (ts, seq) keys differ per call) and chain the state across calls, so the +# absorbed content differs every call at zero extra cycles. +# +# Count-gate the run via the CLI counter before benching: +# cargo run -p cli --release -- execute BENCH.elf --cycles +# -> "KeccakAbsorb calls: CALLS" +# +# KECCAK_SPONGE commits one row per absorbed block, so padding-flush sweep +# points are powers of two: pick CALLS × DATA_BLOCKS = 2^k. +# +# Usage: scripts/gen_keccak_absorb_bench.sh CALLS DATA_BLOCKS OUT.elf +# Honors CLANG / ASM_CFLAGS / ASM_LDFLAGS like the Makefile's asm rule. + +set -euo pipefail + +CALLS="${1:?usage: gen_keccak_absorb_bench.sh CALLS DATA_BLOCKS out.elf}" +DATA_BLOCKS="${2:?usage: gen_keccak_absorb_bench.sh CALLS DATA_BLOCKS out.elf}" +OUT="${3:?usage: gen_keccak_absorb_bench.sh CALLS DATA_BLOCKS out.elf}" + +if ! [[ "$CALLS" =~ ^[0-9]+$ ]] || [ "$CALLS" -lt 1 ]; then + echo "gen_keccak_absorb_bench.sh: CALLS must be a positive integer, got '$CALLS'" >&2 + exit 1 +fi +if ! [[ "$DATA_BLOCKS" =~ ^[0-9]+$ ]] || [ "$DATA_BLOCKS" -lt 1 ]; then + echo "gen_keccak_absorb_bench.sh: DATA_BLOCKS must be a positive integer, got '$DATA_BLOCKS'" >&2 + exit 1 +fi + +CLANG="${CLANG:-clang}" +ASM_CFLAGS="${ASM_CFLAGS:---target=riscv64 -march=rv64im -mabi=lp64}" +ASM_LDFLAGS="${ASM_LDFLAGS:--fuse-ld=lld -nostdlib -Wl,-e,main}" + +if ! command -v "$CLANG" >/dev/null 2>&1; then + echo "gen_keccak_absorb_bench.sh: '$CLANG' not found; run 'make deps' or set CLANG=..." >&2 + exit 1 +fi + +DATA_BYTES=$((DATA_BLOCKS * 136)) +DATA_DWORDS=$((DATA_BLOCKS * 17)) +# 200-byte state + data region, rounded up to 16 for stack hygiene. +FRAME=$(((200 + DATA_BYTES + 15) / 16 * 16)) + +SRC="$(mktemp "${TMPDIR:-/tmp}/keccak_absorb_bench.XXXXXX.s")" +trap 'rm -f "$SRC"' EXIT + +cat > "$SRC" < 0`, /// and the data region must not overlap `state`. pub fn keccak_absorb_blocks(state: &mut [u64; 25], data: &[u8], n_blocks: usize) { - debug_assert!(data.len() == n_blocks * 136, "data must be n_blocks × 136 bytes"); - debug_assert!(data.as_ptr().addr().is_multiple_of(8), "data must be 8-byte aligned"); + debug_assert!( + data.len() == n_blocks * 136, + "data must be n_blocks × 136 bytes" + ); + debug_assert!( + data.as_ptr().addr().is_multiple_of(8), + "data must be 8-byte aligned" + ); unsafe { asm!( "ecall", From d16dcee4990ef31285f8e3cf8de025b4b215927b Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 14:01:03 -0300 Subject: [PATCH 5/6] chore(debug): extend the bus-ID legend to cover all live buses The debug-checks legend stopped at ID 21, silently omitting Keccak(22) through GlobalMemory(31) and the new KeccakSponge(32); print the full range (TryFrom skips the reserved gaps). --- prover/src/debug_report.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prover/src/debug_report.rs b/prover/src/debug_report.rs index 81e71441c..a654ca161 100644 --- a/prover/src/debug_report.rs +++ b/prover/src/debug_report.rs @@ -9,7 +9,7 @@ use crate::tables::types::BusId; /// Print a legend mapping numeric bus IDs to their names. pub fn print_bus_legend() { eprintln!("=== BUS ID LEGEND ==="); - for id in 0u64..=21 { + for id in 0u64..=32 { if let Ok(bus) = BusId::try_from(id) { eprintln!(" Bus {:2} = {}", id, bus.name()); } From 861d2714f4d047d315e0eb31d8433e2f9b40ec5a Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 14:03:59 -0300 Subject: [PATCH 6/6] test(prover): update the keccak column-count pin for the seq column and pin KECCAK_SPONGE KECCAK_RND is 1481 columns since the seq permutation key was added (carried through untouched for KECCAK_SPONGE, like timestamp); also pin the new KECCAK_SPONGE table at 690 columns in the same guard. --- prover/src/tests/trace_builder_tests.rs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index 637c3697d..dc13ec8be 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -753,10 +753,16 @@ mod keccak_tests { assert_eq!(core_cols::NUM_COLUMNS, 511, "KECCAK core columns"); assert_eq!( rnd_cols::NUM_COLUMNS, - 1480, - "KECCAK_RND columns (rnc/rbc inlined; pi virtual; Cxz_right Bit-typed)" + 1481, + "KECCAK_RND columns (rnc/rbc inlined; pi virtual; Cxz_right Bit-typed; \ + + the seq permutation key carried for KECCAK_SPONGE)" ); assert_eq!(keccak_rc::cols::NUM_COLUMNS, 10, "KECCAK_RC columns"); + assert_eq!( + crate::tables::keccak_sponge::cols::NUM_COLUMNS, + 690, + "KECCAK_SPONGE columns" + ); } #[test]